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

Mikaël Mayer mmikael222 at gmail.com
Fri Oct 2 12:14:57 CEST 2009

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,

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>

More information about the isabelle-dev mailing list