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





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