[isabelle-dev] Explicit behaviour of apply(auto) ?
mmikael222 at gmail.com
Fri Oct 2 12:14:57 CEST 2009
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),
> 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 !
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
> http://www.in.tum.de/~haftmann <http://www.in.tum.de/%7Ehaftmann>
> PGP available:
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the isabelle-dev