*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Things identified via `rewrites` not treated as identical*From*: Wolfgang Jeltsch <wolfgang-it at jeltsch.info>*Date*: Sun, 28 Jul 2019 16:01:51 +0300*In-reply-to*: <CALaF1UJ9Uy0vGCu4WkBmbfuPDxG7nFm8hfeCMP+O3g7_5CQ0Bw@mail.gmail.com>*References*: <CALaF1UJ9Uy0vGCu4WkBmbfuPDxG7nFm8hfeCMP+O3g7_5CQ0Bw@mail.gmail.com>

Am Sonntag, den 28.07.2019, 13:38 +0300 schrieb mailing-list anonymous: > 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. Thanks a lot for your explanation. I cannot say that I fully understand what’s going on, but I think I have at least some idea. Apparently, the problem has more to do with rewriting in general than with rewriting introduced by `rewrites` clauses. I understand that defining `(⊖)` as an abbreviation via `x ⊖ y ≡ x ⊕ ((⊖) y)` doesn’t play well with using a partial application of it in the rewrite rule `(⊖) 𝟬 = neg`. While `(⊖) 𝟬` looks like an innocent partial application, it i s in fact `λy. 𝟬 ⊕ ((⊖) y)`, and thus the rewrite rule doesn’t match i n places where `(⊖)` is fully applied, because full applications of abbreviations don’t use `λ`. When using `definition` instead of `abbreviation`, rewriting takes place in all your above four examples. I think I’ll fix my issue by switching from `abbreviation` to `definition` for `(⊖)`. All the best, Wolfgang

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

- Previous by Date: Re: [isabelle] Things identified via `rewrites` not treated as identical
- Next by Date: [isabelle] Meta: replying to the existing threads in "The Cl-isabelle-users Archives"
- Previous by Thread: Re: [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