Re: [isabelle] is it possible to find the function from lemmas and which command can do?



Hi 
 
I find that need to observe subgoals and then with little guess to write function body.
 
have a little hope to understand the key to create new function from a wild design of lemma.
 
Regards,
 
Martin
 
 
> From: tesleft at hotmail.com
> To: isabelle-users at cl.cam.ac.uk
> Date: Mon, 27 Oct 2014 08:08:43 +0800
> Subject: [isabelle] is it possible to find the function from lemmas and which command can do?
> 
> Hi 
>  
> is it possible to find the function from lemmas and which command can do?
> would like to try which lemma can result in fold function
>  
> primrec rev
>  
> lemma app_Nil2 [simp]: "xs @ [] = xs"
> apply(induct_tac xs)
> apply(auto)
> done
> lemma app_assoc [simp]: "(xs @ ys) @ zs = xs @ (ys @ zs)"
> apply(induct_tac xs)
> apply(auto)
> done
> lemma rev_app [simp]: "rev(xs @ ys) = (rev ys) @ (rev xs)"
> apply(induct_tac xs)
> apply(auto)
> done
> theorem rev_rev [simp]: "rev (rev xs) = xs"
> apply(induct_tac xs)
> apply(auto)
> done
>  
> Regards,
>  
> Martin
>  		 	   		  
 		 	   		  


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