Re: [isabelle] Things identified via `rewrites` not treated as identical



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





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