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



Hi ,
I just think to apply all the rules at one time and then apply(auto) to see which rules it use in debug rather than guess by observation and trial and error.It seems think out essential number of lemmas in order before theorem already a miracle. apply(a,b,c,d,e,f,g.......etc)apply(auto)
Regards,
Martin



> From: lp15 at cam.ac.uk
> Date: Sun, 26 Oct 2014 11:36:06 +0000
> To: tesleft at hotmail.com
> CC: isabelle-users at cl.cam.ac.uk
> Subject: Re: [isabelle] how to know which rules to apply before apply(auto)?
> 
> Becoming an expert at Isabelle takes time and cannot be rushed. It sounds like you simply need to work through the tutorials, doing small examples to begin with. Before attempting to prove a theorem, you need to have an intuitive grasp of the key steps of the proof. Don’t expect “auto” to work miracles. 
> 
> Larry Paulson
> 
> 
> > On 26 Oct 2014, at 09:11, M A <tesleft at hotmail.com> wrote:
> > 
> > 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.