Re: [isabelle] Amending an existing locale interpretation with additional rewrite rules

This feature is only available internally, for use by the class package, and only for what corresponds to the "interpretation" command, not for "sublocale".

Making it available in Isar for "interpretation" would be straightforward. For "sublocale" the matter is more involved: the sublocale graph is labelled with morphisms, and I was never able to convince myself that amending these morphisms in the described manner would be robust enough. It is conceivable that such an amendment could break the locale hierarchy in unexpected cases. For symmetry, the feature is not provided for "interpretation" either.


On 2019-09-20 19:02, mailing-list anonymous wrote:
Dear All,

I would like to amend a locale interpretation with additional rewrite
rules. A (nearly) minimal example in the code listing below summarises the
problem. I also make an attempt to explain my problem explicitly in the
form of the following enumerated list:

1. I create locales A and B and provide an interpretation of A in B via
   the command sublocale.
2. After the interpretation, I provide several new constants with the intention to state additional theorems about these constants in the context
   of A.
   3. Once the constants are introduced, I would like to add additional
rewrite rules (for these constants) to the existing interpretation of A in B in a way such that the theorems stated in the context of A after the introduction of the rewrite rules appear in their rewritten form in the
   context of B. I would like to know if this is something that can be
achieved using the existing technology: a naive approach of reinterpreting
   A in B with the new rewrite rules fails.

section ‹Example›
theory example
  imports Main

locale ord =
  fixes le :: "'a ⇒ 'a ⇒ bool" (infix "≤⇩T" 50)
    and ls :: "'a ⇒ 'a ⇒ bool" (infix "<⇩T" 50)

  le ("'(≤⇩T')") and
  le (infix "≤⇩T" 50) and
  ls ("'(<⇩T')") and
  ls (infix "<⇩T" 50)

abbreviation (input) ge (infix "≥⇩T" 50)
  where "x ≥⇩T y ≡ y ≤⇩T x"
abbreviation (input) gt (infix ">⇩T" 50)
  where "x >⇩T y ≡ y <⇩T x"


locale preorder = ord le ls for le ls +
  assumes less_le_not_le: "ls x y ⟷ le x y ∧ ¬ (le y x)"
    and order_refl[iff]: "le x x"
    and order_trans: "le x y ⟹ le y z ⟹ le x z"

locale preorder_dual = preorder

context preorder_dual

(* if the following interpretation is deleted,
then the desired behaviour is achieved *)
sublocale dual: preorder ge gt
  apply unfold_locales
  subgoal using less_le_not_le by blast
  subgoal by auto
  subgoal using order_trans by blast


(* new definitions *)
definition min :: "('a ⇒ 'a ⇒ bool) ⇒ 'a ⇒ 'a ⇒ 'a" where
  "min le a b = (if le a b then a else b)"
definition max :: "('a ⇒ 'a ⇒ bool) ⇒ 'a ⇒ 'a ⇒ 'a" where
  "max le a b = (if le b a then a else b)"

(* an attempt to reinterpret preorder in preorder_dual *)
context preorder_dual

sublocale dual: preorder ge gt
  rewrites "min ge ≡ max le"


(* new theorems in preorder *)
context preorder

lemma min_absorb1: "x ≤⇩T y ⟹ min le x y = x"
  by (simp add: min_def)

(*at this point dual.min_absorb1 does not exist *)


(*Demonstration of the failed attempt to introduce an additional rewrite
context preorder_dual

thm dual.min_absorb1

thm dual.min_absorb1 returns

y ≤⇩T x ⟹ min (λx y. y ≤⇩T x) x y = x

instead of the desired

y ≤⇩T x ⟹ max le x y = x




Thank you

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