[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.firstname.lastname@example.org>, <BAY167-W1086A25A3C2791880694439B69E0@phx.gbl>
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?
This archive was generated by a fusion of
Pipermail (Mailman edition) and