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



Dear Wolfgang Jeltsch,

Given that there has not been an official answer for more than one day, at
least, I can offer a plausible practical solution. Nevertheless, please
keep in mind that I am not familiar with the implementation details of the
locale interpretation and the associated rewrite algorithms (if you still
insist on getting to the heart of the matter, it should possible to debug
the source code).

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.

It would be useful for me if someone who knows the details of the
implementation could confirm/correct/provide further explanation of any
aspects of what is stated above.

Thank you

locale negation =
  fixes neg :: "'a ⇒ 'a" ("⊖ _" [81] 80)
  assumes neg_neg: "⊖ (⊖ x) = x"

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

definition neg :: "'a ⇒ 'a" ("⊖ _" [81] 80) where
  "⊖ x ≡ 𝟬 ⊖ x"

sublocale negation neg
proof
  fix x
  show "⊖ (⊖ x) = x" unfolding neg_def using sub_sub .
qed

lemma neg_zero:
  shows "⊖ 𝟬 = 𝟬"
  unfolding neg_def using sub_zero_2 .

end

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)"

lemma zs: "zero_subtraction zero sub"
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" .
qed

sublocale zero_subtraction zero sub
  rewrites "zero_subtraction.neg zero sub = neg"
apply(rule zs)
unfolding zero_subtraction.neg_def[OF zs]
by (simp add: add_zero_1)

thm neg_zero (* ⊖ 𝟬 = 𝟬 *)

end

interpretation int:
  negation_zero_addition ‹uminus :: int ⇒ int› ‹0› ‹(+)›
  by unfold_locales simp_all

thm int.neg_zero (* - 0 = 0 *)


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

-- 
Please accept my apologies for posting anonymously. This is done to protect
my privacy. I can make my identity and my real contact details available
upon request in private communication under the condition that they are not
to be mentioned on the mailing list.



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