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://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20091002/9ba7b3eb/attachment.htm>
