[isabelle] Kind of generic lemmas: possible?

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?

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