*To*: Lawrence Paulson <lp15 at cam.ac.uk>*Subject*: Re: [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 22:37:44 +0800*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*Importance*: Normal*In-reply-to*: <1CB72DF7-D6CA-4562-BDD4-6AD53315529F@cam.ac.uk>*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>, <BAY167-W92FD07BC2D40E96EABAC38B69F0@phx.gbl>, <1CB72DF7-D6CA-4562-BDD4-6AD53315529F@cam.ac.uk>

Hi Lawrence, 1. I mean that by writing some lemmas and observe the subgoal when prove lemma for lattice, hope to see the function body about writing lattice application in Haskell 2. can multiple lemmas write into one lemma to be proved and observe the subgoals to know the function body? Regards, Martin > From: lp15 at cam.ac.uk > Date: Tue, 28 Oct 2014 12:31:31 +0000 > To: tesleft at hotmail.com > CC: isabelle-users at cl.cam.ac.uk > Subject: Re: [isabelle] which libraries are needed to help to write lemma for operation in functional programming > > I’m afraid that your questions are not very clear. This is partly because of your use of English and partly because you seem to have an unusual application. > > I think that you will need to find a colleague who can help you express your questions more clearly. > > Larry Paulson > > > > On 28 Oct 2014, at 08:34, M A <tesleft at hotmail.com> wrote: > > > > 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 > >

**Follow-Ups**:

**References**:**[isabelle] is it possible to find the function from lemmas and which command can do?***From:*M A

**[isabelle] how to type logical and and logical or operators in Isabelle***From:*M A

**[isabelle] where is "Isabelle/Show me .../Facts" menu in window version of Isabelle***From:*M A

**Re: [isabelle] where is "Isabelle/Show me .../Facts" menu in window version of Isabelle***From:*Makarius

**Re: [isabelle] where is "Isabelle/Show me .../Facts" menu in window version of Isabelle***From:*M A

**[isabelle] which libraries are needed to help to write lemma for operation in functional programming***From:*M A

**Re: [isabelle] which libraries are needed to help to write lemma for operation in functional programming***From:*Lawrence Paulson

- Previous by Date: Re: [isabelle] which libraries are needed to help to write lemma for operation in functional programming
- Next by Date: Re: [isabelle] which libraries are needed to help to write lemma for operation in functional programming
- Previous by Thread: Re: [isabelle] which libraries are needed to help to write lemma for operation in functional programming
- Next by Thread: Re: [isabelle] which libraries are needed to help to write lemma for operation in functional programming
- Cl-isabelle-users October 2014 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list