Email Gateway (Aug 22 2022 at 20:36): Email Gateway (Aug 22 2022 at 20:36):From: mailing-list anonymous <mailing.list.anonymous@gmail.com>
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
begin
locale ord =
fixes le :: "'a ⇒ 'a ⇒ bool" (infix "≤⇩T" 50)
and ls :: "'a ⇒ 'a ⇒ bool" (infix "<⇩T" 50)
begin
notation
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"
end
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
begin
(* 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
done
end
(* 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
begin
sublocale dual: preorder ge gt
rewrites "min ge ≡ max le"
sorry
end
(* new theorems in preorder *)
context preorder
begin
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 *)
end
(*Demonstration of the failed attempt to introduce an additional rewrite
rule*)
context preorder_dual
begin
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
*)
end
end
Thank you
Email Gateway (Aug 22 2022 at 20:38):From: Clemens Ballarin <ballarin@in.tum.de>
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.
Clemens
Email Gateway (Aug 22 2022 at 20:38):From: mailing-list anonymous <mailing.list.anonymous@gmail.com>
Dear Clemens Ballarin,
Thank you for your reply. My personal opinion is that a possibility to
amend an interpretation with new rewrite rules could be a very useful
feature for the locale infrastructure, provided that it becomes available
both for 'interpretation' and 'sublocale'. However, of course, I appreciate
that enabling it may be involved and I will proceed based on the assumption
that it will not become available in the foreseeable future.
Thank you
Last updated: Apr 26 2024 at 12:28 UTC