Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] which libraries are needed to help to write le...

Email Gateway (Aug 19 2022 at 16:11):

From: M A <tesleft@hotmail.com>
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

Email Gateway (Aug 19 2022 at 16:11):

From: Lawrence Paulson <lp15@cam.ac.uk>
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

Email Gateway (Aug 19 2022 at 16:11):

From: M A <tesleft@hotmail.com>
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

Email Gateway (Aug 19 2022 at 16:11):

From: M A <tesleft@hotmail.com>
Hi

I means the application code for lattice such as addition of lattice, multiply of lattice and use which collection such as list for storing lattice for creating lattice in Haskell code and change meet and join definition into Haskell code

Regards,

Martin

Last updated: Nov 21 2024 at 12:39 UTC