*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Kind of generic lemmas: possible?*From*: Yannick Duchêne (Hibou57) <yannick_duchene at yahoo.fr>*Date*: Mon, 06 Aug 2012 05:27:08 +0200*Organization*: Ada @ Home*References*: <op.willhltkule2fv@douda-yannick> <501F33F8.8060506@jaist.ac.jp>*User-agent*: Opera Mail/12.01 (Linux)

On 08/06/2012 11:35 AM, Yannick Duchêne (Hibou57) wrote:Hi people out there,Here is a naive attempt I've just made for testing. It is selfexplanatory:lemma obligation: "f x y ⟹ f y x" sorry fun equal :: "nat ⇒ nat ⇒ bool" where "equal x y = (x = y)" thm obligation [where f = equal] lemma equal_obligation: obligation [where f = equal] The “thm” line is OK, but not the last lemma. Is this just stupid in an Isabelle context or is there another way to achieve the same purpose?Try lemmas equal_obligation = obligation [where f = equal] (Note the trailing 's' in 'lemmas'.)

Will try it, thanks.

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?

-- “Syntactic sugar causes cancer of the semi-colons.” [1] “Structured Programming supports the law of the excluded muddle.” [1] [1]: Epigrams on Programming — Alan J. — P. Yale University

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

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

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

- Previous by Date: Re: [isabelle] Kind of generic lemmas: possible?
- Next by Date: Re: [isabelle] Kind of generic lemmas: possible?
- Previous by Thread: Re: [isabelle] Kind of generic lemmas: possible?
- Next by Thread: Re: [isabelle] Kind of generic lemmas: possible?
- 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