Email Gateway (Aug 19 2022 at 08:31): Email Gateway (Aug 19 2022 at 08:31):From: "Yannick Duchêne (Hibou57 )" <yannick_duchene@yahoo.fr>
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?
Email Gateway (Aug 19 2022 at 08:31):From: Christian Sternagel <c-sterna@jaist.ac.jp>
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
Email Gateway (Aug 19 2022 at 08:31):From: "Yannick Duchêne (Hibou57 )" <yannick_duchene@yahoo.fr>
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?
I will try your suggestion now (and further read your comment too,
obviously).
Email Gateway (Aug 19 2022 at 08:32):From: Christian Sternagel <c-sterna@jaist.ac.jp>
Dear Yannick,
Well, it depends on what you want to achieve (which I might have
misinterpreted in your previous mail):
Your above theory fragment is a typical application of locales: in a
locale you specify some abstract properties (in assumes) that have to be
satisfied by parameters (from fixes) and for every specific
interpretation you have to prove that those properties are indeed
satisfied. What you gain is the ability to prove lemmas abstractly
(inside the locale) on obtain them for free in special cases as soon as
you successfully establish an interpretation.
The other thing is to merely instantiate a given lemma (i.e., make it
more specific), which does not require to prove any assumptions. And
that is what my suggestion was about. To use a locale in such a case
would just be overkill. But after reading your previous mail again I
think you might be in the above setting.
cheers
chris
Last updated: Apr 24 2024 at 20:16 UTC