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



Le Mon, 06 Aug 2012 05:03:20 +0200, Christian Sternagel <c-sterna at jaist.ac.jp> a écrit:

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


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


--
“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University






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