*To*: cl-isabelle-users <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] Things identified via `rewrites` not treated as identical*From*: mailing-list anonymous <mailing.list.anonymous at gmail.com>*Date*: Sun, 28 Jul 2019 13:38:59 +0300*Cc*: wolfgang-it at jeltsch.info

Dear Wolfgang Jeltsch, Given that there has not been an official answer for more than one day, at least, I can offer a plausible practical solution. Nevertheless, please keep in mind that I am not familiar with the implementation details of the locale interpretation and the associated rewrite algorithms (if you still insist on getting to the heart of the matter, it should possible to debug the source code). Using only the abbreviation ⊖ from negation_zero_addition, the suggested rewrite rule is 'zero_subtraction.neg 𝟬 sub=neg', which stands for '(⊖) 𝟬=neg' (see print_abbrevs). The theorem neg_zero is '((⊖) 𝟬) 𝟬 = 𝟬' after the interpretation inside the context of negation_zero_addition. Trying to (for example) unfold '((⊖) 𝟬) 𝟬 = 𝟬' with '(⊖) 𝟬=neg' leaves the theorem in the same state: lemma subst1: "(⊖) 𝟬 ≡ neg" by (simp add: add_zero_1) lemma subst2: "(⊖) 𝟬 x ≡ neg x" by (simp add: add_zero_1) lemma thm1: "((⊖) 𝟬) 𝟬 ≡ 𝟬" sorry lemma thm2: "f ((⊖) 𝟬) ≡ f ((⊖) 𝟬)" by simp thm thm1[unfolded subst1] (*unfold 'fails': ((⊖) 𝟬) 𝟬 ≡ 𝟬*) thm thm1[unfolded subst2] (*unfold 'succeeds': ⊖ 𝟬 ≡ 𝟬*) thm thm2[unfolded subst1] (*unfold 'succeeds': ?f neg ≡ ?f neg*) thm thm2[unfolded subst2] (*unfold 'succeeds': ?f neg ≡ ?f neg*) I can only speculate as to whether the mechanism used for rewriting during the locale interpretation is not entirely different from the technique used in the example above. As you can also see from the code listing above, the rewrite rule '(⊖) 𝟬 x ≡ neg x' achieves the desired effect. Using the abbreviation zero_subtraction.neg, this rule becomes 'zero_subtraction.neg 𝟬 sub x= neg x'. However, it may be even safer to replace the abbreviation zero_subtraction.neg with a predefined constant (see the code listing below). In this case, 'zero_subtraction.neg 𝟬 sub= neg' is, most likely, the best available option: I expect that with this rule all plausible algorithms would agree on the intuitively desired solution unanimously. It would be useful for me if someone who knows the details of the implementation could confirm/correct/provide further explanation of any aspects of what is stated above. Thank you locale negation = fixes neg :: "'a ⇒ 'a" ("⊖ _" [81] 80) assumes neg_neg: "⊖ (⊖ x) = x" 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 definition neg :: "'a ⇒ 'a" ("⊖ _" [81] 80) where "⊖ x ≡ 𝟬 ⊖ x" sublocale negation neg proof fix x show "⊖ (⊖ x) = x" unfolding neg_def using sub_sub . qed lemma neg_zero: shows "⊖ 𝟬 = 𝟬" unfolding neg_def using sub_zero_2 . end 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)" lemma zs: "zero_subtraction zero sub" 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" . qed sublocale zero_subtraction zero sub rewrites "zero_subtraction.neg zero sub = neg" apply(rule zs) unfolding zero_subtraction.neg_def[OF zs] by (simp add: add_zero_1) thm neg_zero (* ⊖ 𝟬 = 𝟬 *) end interpretation int: negation_zero_addition ‹uminus :: int ⇒ int› ‹0› ‹(+)› by unfold_locales simp_all thm int.neg_zero (* - 0 = 0 *) On 27/07/2019 01: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" > 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 > -- Please accept my apologies for posting anonymously. This is done to protect my privacy. I can make my identity and my real contact details available upon request in private communication under the condition that they are not to be mentioned on the mailing list.

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

**Re: [isabelle] Things identified via `rewrites` not treated as identical***From:*mailing-list anonymous

- Previous by Date: [isabelle] New AFP entry: Szpilrajn Extension Theorem
- Next by Date: Re: [isabelle] Things identified via `rewrites` not treated as identical
- Previous by Thread: [isabelle] New AFP entry: Szpilrajn Extension Theorem
- 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