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

*To*: "isabelle-users at cl.cam.ac.uk" <isabelle-users at cl.cam.ac.uk>
*Subject*: [isabelle] which libraries are needed to help to write lemma for operation in functional programming
*From*: M A <tesleft at hotmail.com>
*Date*: Tue, 28 Oct 2014 16:34:12 +0800
*Importance*: Normal
*In-reply-to*: <BAY167-W1086A25A3C2791880694439B69E0@phx.gbl>
*References*: <BAY167-W3024082D992B681F64185DB69E0@phx.gbl>, , <BAY167-W27953B618A80B2575F3851B69E0@phx.gbl>, , , <16FFFE45-32C8-44B9-8908-A9471D2F4C7D@uibk.ac.at>, , <BAY167-W1074477050F04D10DA461BBB69E0@phx.gbl>, , <alpine.LNX.2.00.1410272003580.59545@lxbroy10.informatik.tu-muenchen.de>, <BAY167-W1086A25A3C2791880694439B69E0@phx.gbl>

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