[isabelle] which libraries are needed to help to write lemma for operation in functional programming



Hi 
1. which libraries are needed to write lemma to find subgoal to observe some functional code?for example, can we import list and complete_lattice or lattice and write associative and distributive lemma and find some subgoals to do functional programming in haskell code for lattice ?
2. can three lemmas write into one statement by lemma "(A) ^ (B) V (C)" in order to find algorithms for using 3 lemmas by observe the subgoals? 
Regards,
Martin 		 	   		  


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