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
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:
I would like to amend a locale interpretation with additional rewrite
rules. A (nearly) minimal example in the code listing below summarises
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
the command sublocale.
2. After the interpretation, I provide several new constants with
intention to state additional theorems about these constants in the
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
introduction of the rewrite rules appear in their rewritten form in
context of B. I would like to know if this is something that can be
achieved using the existing technology: a naive approach of
A in B with the new rewrite rules fails.
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
(* if the following interpretation is deleted,
then the desired behaviour is achieved *)
sublocale dual: preorder ge gt
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 *)
sublocale dual: preorder ge gt
rewrites "min ge ≡ max le"
(* new theorems in 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
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
This archive was generated by a fusion of
Pipermail (Mailman edition) and