*To*: isabelle-users at cl.cam.ac.uk*Subject*: [isabelle] Things identified via `rewrites` not treated as identical*From*: Wolfgang Jeltsch <wolfgang-it at jeltsch.info>*Date*: Sat, 27 Jul 2019 01:14:23 +0300

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" begin abbreviation neg :: "'a ⇒ 'a" ("⊖ _" [81] 80) where "⊖ x ≡ 𝟬 ⊖ x" sublocale negation neg proof fix x show "𝟬 ⊖ (𝟬 ⊖ x) = x" using sub_sub . qed lemma neg_zero: shows "⊖ 𝟬 = 𝟬" using sub_zero_2 . end Finally, 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" begin abbreviation sub :: "['a, 'a] ⇒ 'a" (infixl "⊖" 65) where "x ⊖ y ≡ x ⊕ (⊖ y)" sublocale zero_subtraction zero sub rewrites "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) qed end Now 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:*Andreas Lochbihler

- Previous by Date: Re: [isabelle] Why is Monad_Syntax.bind right and not left associative?
- Next by Date: Re: [isabelle] Why is Monad_Syntax.bind right and not left associative?
- Previous by Thread: Re: [isabelle] Why is Monad_Syntax.bind right and not left associative?
- 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