*To*: Wolfgang Jeltsch <wolfgang-it at jeltsch.info>, isabelle-users at cl.cam.ac.uk*Subject*: Re: [isabelle] Things identified via `rewrites` not treated as identical*From*: Andreas Lochbihler <mail at andreas-lochbihler.de>*Date*: Sun, 28 Jul 2019 14:24:19 +0200*In-reply-to*: <b2be31f09caa353771fe2f01256690113966f565.camel@jeltsch.info>*References*: <b2be31f09caa353771fe2f01256690113966f565.camel@jeltsch.info>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:60.0) Gecko/20100101 Thunderbird/60.8.0

Dear Wolfgang,

The term sub in zero_subtraction expands to λx y. (+) x (uminus y). So the rewrite rule "zero_subtraction.neg zero sub = neg" becomes in the interpretation λx. int.sub 0 x = uminus

Alternatively, you can add the eta-expanded version of the rewrite rule: sublocale zero_subtraction zero sub rewrites "zero_subtraction.neg zero sub = neg" and "zero_subtraction.neg zero sub x = neg x" Then it works as expected. Hope this helps Andreas On 27/07/2019 00:14, Wolfgang Jeltsch wrote:

Hi! In my work on formalizing process calculi I tripped over an issue with Isabelle’s locale support that I don’t fully understand. I’d like to illustrate this issue here with some example code that is much simpler than my actual code but still illustrates the point. Let’s first introduce a locale that describes an involution, which we call negation. locale negation = fixes neg :: "'a ⇒ 'a" ("⊖ _" [81] 80) assumes neg_neg: "⊖ (⊖ x) = x" Next, we define a locale that captures structures with a zero and a subtraction. Any such structure gives rise to a negation and this negation has the property that it turns zero into zero. locale zero_subtraction = fixes zero :: 'a ("𝟬") fixes sub :: "['a, 'a] ⇒ 'a" (infixl "⊖" 65) assumes sub_sub: "x ⊖ (x ⊖ y) = y" assumes sub_zero_2: "x ⊖ 𝟬 = x" beginabbreviation neg :: "'a ⇒ 'a" ("⊖ _" [81] 80) where"⊖ x ≡ 𝟬 ⊖ x"sublocale negation negproof fix x show "𝟬 ⊖ (𝟬 ⊖ x) = x" using sub_sub . qedlemma neg_zero:shows "⊖ 𝟬 = 𝟬" using sub_zero_2 .endFinally, we introduce a locale that captures structures with a negation, a zero, and an addition. We import the `negation` locale to provide the negation structure. Since we can construct subtraction from negation and addition, we introduce a corresponding sublocale relationship. This would give us another instance of the `negation` locale through the `zero_subtraction` locale, albeit with the same negation operator. To prevent this, we use `rewrites`. locale negation_zero_addition = negation neg for neg :: "'a ⇒ 'a" ("⊖ _" [81] 80) + fixes zero :: 'a ("𝟬") fixes add :: "['a, 'a] ⇒ 'a" (infixl "⊕" 65) assumes add_zero_1: "𝟬 ⊕ x = x" assumes add_zero_2: "x ⊕ 𝟬 = x" assumes neg_add: "⊖ (x ⊕ y) = (⊖ x) ⊕ (⊖ y)" assumes add_cancel: "x ⊕ ((⊖ x) ⊕ y) = y" beginabbreviation sub :: "['a, 'a] ⇒ 'a" (infixl "⊖" 65) where"x ⊖ y ≡ x ⊕ (⊖ y)"sublocale zero_subtraction zero subrewrites "zero_subtraction.neg zero sub = neg" proof unfold_locales fix x and y have "x ⊕ (⊖ (x ⊕ (⊖ y))) = x ⊕ ((⊖ x) ⊕ (⊖ (⊖ y)))" (is "?l = _") by (simp add: neg_add) also have "… = ⊖ (⊖ y)" using add_cancel . also have "… = y" (is "_ = ?r") using neg_neg . finally show "?l = ?r" . next fix x have "x ⊕ (⊖ 𝟬) = (⊖ (⊖ x)) ⊕ (⊖ 𝟬)" (is "?l = _") by (simp add: neg_neg) also have "… = ⊖ (⊖ x ⊕ 𝟬)" by (simp add: neg_add) also have "… = ⊖ (⊖ x)" by (simp add: add_zero_2) also have "… = x" (is "_ = ?r") using neg_neg . finally show "?l = ?r" . next show "(λx. 𝟬 ⊕ (⊖ x)) = (λx. ⊖ x)" by (simp add: add_zero_1) qedendNow let’s have an interpretation. interpretation int: negation_zero_addition ‹uminus :: int ⇒ int› ‹0› ‹(+)› by unfold_locales simp_all I would like to prove that integer negation applied to the integer 0 is the integer 0 again, using `neg_zero`. However, that doesn’t work. lemma "- (0 :: int) = 0" using int.neg_zero oops The problem is that the goal refers to the negation operator of `int`, while `int.neg_zero` refers to the negation operator that is derived from zero and subtraction (where subtraction in turn is derived from negation and addition). Both negation operators are equal, and I have communicated this equality by means of `rewrites`, but Isabelle apparently doesn’t make use of it. How can I use facts like `int.neg_zero` in proofs of lemmas like the above one? All the best, Wolfgang

**Follow-Ups**:**Re: [isabelle] Things identified via `rewrites` not treated as identical***From:*Wolfgang Jeltsch

**References**:**[isabelle] Things identified via `rewrites` not treated as identical***From:*Wolfgang Jeltsch

- Previous by Date: Re: [isabelle] Things identified via `rewrites` not treated as identical
- Next by Date: Re: [isabelle] Things identified via `rewrites` not treated as identical
- Previous by Thread: [isabelle] Things identified via `rewrites` not treated as identical
- Next by Thread: Re: [isabelle] Things identified via `rewrites` not treated as identical
- Cl-isabelle-users July 2019 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list