Re: [isabelle] Kind of generic lemmas: possible?
On 08/06/2012 12:27 PM, Yannick Duchêne (Hibou57) wrote:
Well, it depends on what you want to achieve (which I might have
misinterpreted in your previous mail):
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
fix x y
assume "equal x y"
then show "equal y x" by simp
Is this OK or is this abusing what the concept of locale is?
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and