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?
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).
This archive was generated by a fusion of
Pipermail (Mailman edition) and