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



Dear Yannick,

On 08/06/2012 12:27 PM, Yannick Duchêne (Hibou57) wrote:
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?
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





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