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



Dear Wolfgang,

The problem is that you have abbreviations on the left-hand sides of your rewrites instead of definitions. Abbreviations are just for pretty-printing; in the underlying term representation, abbreviations are unfolded (and implicitly beta-reduced). If you change the abbreviations into definitions, then the rewriting works as expected. Let's look into what's happening:


The term sub in zero_subtraction expands to λx y. (+) x (uminus y).
So the rewrite rule "zero_subtraction.neg zero sub = neg" becomes in the interpretation

  λx. int.sub 0 x = uminus

This has a lambda on the left, i.e., it is not a proper higher-order rewrite rule. It will only kick in if there is a lambda abstraction in the term. However, in the theorem neg_zero, the beta redex "(λx. int.sub 0 x) 0" has already been reduced so int.sub 0 0. So the rewrite rule will not trigger. If you turn the abbreviations into definitions, there will be no trouble with implicit beta-reductions and eta-expansions.

Alternatively, you can add the eta-expanded version of the rewrite rule:

    sublocale zero_subtraction zero sub
      rewrites "zero_subtraction.neg zero sub = neg"
        and "zero_subtraction.neg zero sub x = neg x"

Then it works as expected.

Hope this helps
Andreas


On 27/07/2019 00: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







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