[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.