Hi Florian,<br>Thanks for your help.<br>I tried prf, but it gave only an "?", when it was outside the proof, and failed when it was inside the proof.<br>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.<br>

<br><blockquote style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;" class="gmail_quote"><span style="font-family: courier new,monospace;">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))"</span><br style="font-family: courier new,monospace;">

<span style="font-family: courier new,monospace;">by auto</span><br style="font-family: courier new,monospace;"><span style="font-family: courier new,monospace;">prf test</span><br></blockquote><br>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.<br>

The trace simplifier is too exhaustive for my needs.<br><br>If you've heard of a solution, I'm interested !<br>Many thanks,<br clear="all">Mikaël<br>
<br><br><div class="gmail_quote">2009/10/2 Florian Haftmann <span dir="ltr"><<a href="mailto:florian.haftmann@informatik.tu-muenchen.de">florian.haftmann@informatik.tu-muenchen.de</a>></span><br><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">

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


<br>
</font></blockquote></div><br>