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 hotmail.com>:
>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.