*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Kind of generic lemmas: possible?*From*: Christian Sternagel <c-sterna at jaist.ac.jp>*Date*: Mon, 06 Aug 2012 12:55:15 +0900*In-reply-to*: <op.wilnvircule2fv@douda-yannick>*References*: <op.willhltkule2fv@douda-yannick> <501F33F8.8060506@jaist.ac.jp> <op.wilnvircule2fv@douda-yannick>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:14.0) Gecko/20120717 Thunderbird/14.0

Dear Yannick, On 08/06/2012 12:27 PM, Yannick Duchêne (Hibou57) wrote:

I came back to post something I tried. Suspecting the answer may be an area of Isabelle I don't already know, I opened the Locales Tutorial, had a very quick overview, and ended with this: locale obligations = fixes f :: "'a ⇒ 'a ⇒ bool" assumes first_obligation: "f x y ⟹ f y x" fun equal :: "nat ⇒ nat ⇒ bool" where "equal x y = (x = y)" interpretation obligations equal proof fix x y assume "equal x y" then show "equal y x" by simp qed Is this OK or is this abusing what the concept of locale is?

cheers chris

**References**:**[isabelle] Kind of generic lemmas: possible?***From:*Yannick Duchêne (Hibou57)

**Re: [isabelle] Kind of generic lemmas: possible?***From:*Christian Sternagel

**Re: [isabelle] Kind of generic lemmas: possible?***From:*Yannick Duchêne (Hibou57)

- Previous by Date: Re: [isabelle] Kind of generic lemmas: possible?
- Next by Date: Re: [isabelle] Words in Markus document's, I don't understand
- Previous by Thread: Re: [isabelle] Kind of generic lemmas: possible?
- Next by Thread: [isabelle] Elbe 1.6 - Theory Viewer
- Cl-isabelle-users August 2012 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