[isabelle-dev] Explicit behaviour of apply(auto) ?

[Mikaël Mayer]

Hi Florian,
Thanks for your help.
I tried prf, but it gave only an "?", when it was outside the proof, and
failed when it was inside the proof.
What I would like to know, is what were the rules that it used, that is,
what kind of "apply(....)" should I write to get the same result.

lemma test: "\<forall>x. (P(x) \<and> (\<exists>z. Q(x, z)) \<and>
> (\<forall>x z. Q(x, z)=Q(f(x), z)))\<longrightarrow> (\<exists>z. Q(f(x),
> z))"
> by auto
> prf test
>

In this case, the auto method works fine, but in other quite similar cases,
it is extremely long (especially when you have arithmetic), and once it
finds the proof, I would like to insert it directly into the document to get
faster next time.
The trace simplifier is too exhaustive for my needs.

If you've heard of a solution, I'm interested !
Many thanks,
Mikaël


2009/10/2 Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>

> Hi Mikaël,
>
> > Can someone tell we how I can *retrieve the lemmas/rules used by
> > apply(auto)* , i.e. what were the steps I should have used if I did not
> > have this auto method ?
> > Same question for *apply(blast)*
>
> Although it is technically possible, it will usually waste some time and
> energy to derive useful information:  display the proof term
> corresponding to lemma "foo" with
>
>        prf "foo"
>
> Another possibility is to turn "trace simplifier" in the Isabelle
> options menu in PG on before invoking simp (don't forget to turn it off
> afterwards!).  This obviously will not give any hints about intro/elim
> rules used during auto or blast.
>
> Perhaps the best relevance retrieval mechanism can be found in
> sledgehammer (http://isabelle.in.tum.de/sledgehammer.html).
>
> Hope this helps
>        Florian
>
> --
>
> Home:
> http://www.in.tum.de/~haftmann <http://www.in.tum.de/%7Ehaftmann>
>
> PGP available:
>
> http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20091002/9ba7b3eb/attachment.html>