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



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'.)

However, such specialization can be applied ad hoc (which is often preferable since it avoids to generate many "redundant" lemmas). E.g., wherever you would want to use 'equal_obligation' you could instead directly use 'obligation [where f = equal]' (or shorter) 'obligation [of equal]'. The second variant is more robust w.r.t. renaming (since variables are just instantiated by their position from left to right), whereas the first variant is more robust w.r.t. to reordering (which in my experience is not as frequent as renaming and most of the time combined with renaming anyway; thus I would consider the "of" variant more useful in practice... but that is just personal taste I guess).

cheers

chris





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