# Re: [isabelle] Kind of generic lemmas: possible?

Le Mon, 06 Aug 2012 05:03:20 +0200, Christian Sternagel <c-sterna at jaist.ac.jp> a écrit:
```
```
```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 self explanatory:
```

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.

```
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?

```
```

--
“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

```

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.