Re: [isabelle] how to know which rules to apply before apply(auto)?

Hi  is it fact_filter to give hints about what lemma to be used? what is the correct command to return hints about which lemmas to be used? after tried, it seems same as giving hints about rules, however not lemmas. Sometimes it do not have immediate response, I do not know whether it start or running or not start. "remote_vampire": Cannot connect to remote server. 
"spass": Try this: by (metis list.inject) (0 ms).
(No structured proof available -- proof too simple.) 
"e": Try this: by (metis the_elem_set) (0 ms).
(No structured proof available -- proof too simple.) theory ts
imports Main
lemma "[a] = [b] ==> a = b"
sledgehammer fact_filter = <"[a] = [b] ==> a = b">  {smart} Regards, Martin > From: noschinl at
> Date: Sun, 26 Oct 2014 11:12:12 +0100
> To: tesleft at; isabelle-users at
> Subject: Re: [isabelle] how to know which rules to apply before apply(auto)?
> When proving something in Isabelle, you should have an idea how you would prove it on paper first: This should give you an idea which properties you need for the proof.
> Isabelle offers you a few tools to discover useful lemmas: Sledgehammer can search for a proof and gives you a list of lemmas it needed for a proof. Inspecting this list often helps to give the right lemmas to auto (and similar tools), so they can find a proof.
> Very helpful is also the "find theorems" tool which is found in the query panel: You can search for lemmas containing certain constants or having a specific shape. In particular, you can also search for lemmas which are applicable by rule (using the intro, elim, dest  keywords).
> It is important to keep in mind that lemmas are often formulated a bit differently than in maths, to make them work better with the various proof tools.
> There is no manual of all rules. Rather, the lemmas available can be either discovered by browsing the theories or (more directly) by the use of find theorems.
> In many cases, "apply(a,b)" and "apply a apply b" are equivalent, but there are some differences: Some proof methods (e.g. rule) don't return a single proof step but potentially a sequence of multiple proof steps (try applying the "back" command). In the (a,b) case, when the second proof method fails, Isabelle backtracks and tries the next proof step produced by a. Also, if there are chained facts (from using then, from, using or similar) then these facts are available to both proof methods. This is usually not what you want.
> Best regards, Lars
> Am 26. Oktober 2014 10:11:41 MEZ, schrieb M A <tesleft at>:
> >Hi
> >1. how to know which rules to apply before apply(auto)?2. any manual to
> >show all the rules that can be applied for each library when import
> >them?3. is there any difference to apply rules in one statement or
> >apply one by one?
> >a. apply(a)apply(b)done
> >b.apply(a,b)done
> >
> >Regards,
> >Martin 		 	   		  

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.