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

```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" ("⊖ _"  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" ("⊖ _"  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`.

negation neg for neg :: "'a ⇒ 'a" ("⊖ _"  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 = _")
also have "… = ⊖ (⊖ y)"
also have "… = y" (is "_ = ?r")
using neg_neg .
finally show "?l = ?r" .
next
fix x
have "x ⊕ (⊖ 𝟬) = (⊖ (⊖ x)) ⊕ (⊖ 𝟬)" (is "?l = _")
also have "… = ⊖ (⊖ x ⊕ 𝟬)"
also have "… = ⊖ (⊖ x)"
also have "… = x" (is "_ = ?r")
using neg_neg .
finally show "?l = ?r" .
next
show "(λx. 𝟬 ⊕ (⊖ x)) = (λx. ⊖ x)"
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

```

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