Theory RTSConstructions
theory RTSConstructions
imports Main RTS2_Preliminaries
begin
section "Injective Images of RTS's"
text‹
Here we show that the image of an RTS ‹A› at type @{typ 'a}, under a function from @{typ 'a}
to @{typ 'b} that is injective on the set of arrows, is an RTS at type @{typ 'b} that is
isomorphic to ‹A›. We will use this, together with the universe assumptions, to obtain
isomorphic images, of constructions such as product and exponential RTS, that yield results
that ``live'' at the same type as their arguments.
›
locale inj_image_rts =
A: rts A
for map :: "'a ⇒ 'b"
and A :: "'a resid" (infix ‹\⇩A› 70) +
assumes inj_map: "inj_on map (Collect A.arr ∪ {A.null})"
begin
notation A.con (infix ‹⌢⇩A› 50)
notation A.prfx (infix ‹≲⇩A› 50)
notation A.cong (infix ‹∼⇩A› 50)
abbreviation Null
where "Null ≡ map A.null"
abbreviation Arr
where "Arr t ≡ t ∈ map ` Collect A.arr"
abbreviation map'
where "map' t ≡ inv_into (Collect A.arr) map t"
definition resid :: "'b resid" (infix ‹\› 70)
where "t \\ u = (if Arr t ∧ Arr u then map (map' t \\⇩A map' u) else Null)"
lemma inj_map':
shows "inj_on map (Collect A.arr)"
using inj_map by auto
lemma map_null:
shows "map A.null ∉ map ` Collect A.arr"
using inj_map by simp
lemma map'_map [simp]:
assumes "A.arr t"
shows "map' (map t) = t"
using assms inj_map by simp
lemma map_map' [simp]:
assumes "Arr t"
shows "map (map' t) = t"
using assms f_inv_into_f by metis
sublocale ResiduatedTransitionSystem.partial_magma resid
by (metis ResiduatedTransitionSystem.partial_magma.intro map_null resid_def)
lemma null_char:
shows "null = Null"
by (metis map_null null_is_zero(2) resid_def)
sublocale residuation resid
proof
show "⋀t u. t \\ u ≠ null ⟹ u \\ t ≠ null"
unfolding resid_def null_char
by (metis A.arr_resid A.conI A.con_sym imageI map_null mem_Collect_eq)
show "⋀t u. t \\ u ≠ null ⟹ (t \\ u) \\ (t \\ u) ≠ null"
unfolding resid_def null_char inj_map
apply simp
by (metis CollectI A.arr_resid A.conI A.con_imp_arr_resid imageI
map'_map map_null)
show "⋀v t u. (v \\ t) \\ (u \\ t) ≠ null
⟹ (v \\ t) \\ (u \\ t) = (v \\ u) \\ (t \\ u)"
proof -
fix t u v
assume vt_ut: "(v \\ t) \\ (u \\ t) ≠ null"
have 1: "Arr t ∧ Arr u ∧ Arr v"
using vt_ut
by (metis map_null null_char resid_def)
have "(v \\ t) \\ (u \\ t) = map ((map' v \\⇩A map' t) \\⇩A (map' u \\⇩A map' t))"
using 1 null_char resid_def vt_ut
apply auto[1]
by (metis A.arr_resid A.conI map'_map map_null vt_ut)
also have
"... = map ((map' v \\⇩A map' u) \\⇩A (map' t \\⇩A map' u))"
using A.cube by simp
also have "... = (v \\ u) \\ (t \\ u)"
using 1 null_char resid_def
apply auto[1]
apply (metis CollectI A.conI image_eqI map'_map map_null A.arr_resid)
apply (metis A.conI A.con_implies_arr(1) image_eqI mem_Collect_eq)
by (metis CollectI A.conI A.con_implies_arr(2) image_eqI)
finally show "(v \\ t) \\ (u \\ t) = (v \\ u) \\ (t \\ u)"
by blast
qed
qed
notation con (infix ‹⌢› 50)
lemma con_char:
shows "t ⌢ u ⟷ Arr t ∧ Arr u ∧ map' t ⌢⇩A map' u"
using null_char con_def inj_map resid_def A.con_def
by (metis (full_types) image_eqI map_null mem_Collect_eq A.arr_resid)
lemma arr_char:
shows "arr t ⟷ Arr t"
using arr_def con_char inj_map by auto
lemma ide_char⇩I⇩I:
shows "ide t ⟷ Arr t ∧ A.ide (map' t)"
unfolding ide_def resid_def con_char
using inj_map' f_inv_into_f
by (metis A.ide_def inv_into_f_f mem_Collect_eq A.arr_resid)
lemma trg_char:
shows "trg t = (if Arr t then map (A.trg (map' t)) else null)"
unfolding trg_def resid_def A.trg_def null_char by simp
sublocale rts resid
proof
show "⋀t. arr t ⟹ ide (trg t)"
using ide_char⇩I⇩I inj_map trg_char trg_def by fastforce
show 1: "⋀a t. ⟦ide a; t ⌢ a⟧ ⟹ t \\ a = t"
by (simp add: A.resid_arr_ide con_char f_inv_into_f ide_char⇩I⇩I resid_def)
show "⋀a t. ⟦ide a; a ⌢ t⟧ ⟹ ide (a \\ t)"
by (metis 1 arrE arr_resid con_sym cube ideE ideI)
show "⋀t u. t ⌢ u ⟹ ∃a. ide a ∧ a ⌢ t ∧ a ⌢ u"
by (metis (full_types) CollectI A.con_imp_coinitial_ax ide_char⇩I⇩I
image_eqI inj_image_rts.con_char inj_image_rts_axioms map'_map
A.ide_implies_arr)
show "⋀t u v. ⟦ide (t \\ u); u ⌢ v⟧ ⟹ t \\ u ⌢ v \\ u"
proof -
fix t u v
assume ide: "ide (t \\ u)"
assume con: "u ⌢ v"
have "Arr t ∧ Arr u ∧ Arr v"
using ide con ide_char⇩I⇩I con_char
by (metis arr_resid_iff_con ide_implies_arr)
moreover have "A.arr (map' t \\⇩A map' u)"
using ide ide_char⇩I⇩I resid_def
by (meson A.arr_resid arr_resid_iff_con con_char ide_implies_arr)
moreover have "A.arr (map' v \\⇩A map' u)"
using con con_char
by (meson A.arr_resid A.con_sym)
ultimately show "t \\ u ⌢ v \\ u"
using ide con ide_char⇩I⇩I con_char resid_def A.con_target by simp
qed
qed
notation prfx (infix ‹≲› 50)
notation cong (infix ‹∼› 50)
text‹
The function @{term map} and its inverse (both suitably extensionalized) determine an
isomorphism between ‹A› and its image.
›
abbreviation map⇩e⇩x⇩t
where "map⇩e⇩x⇩t t ≡ if A.arr t then map t else null"
abbreviation map'⇩e⇩x⇩t
where "map'⇩e⇩x⇩t t ≡ if Arr t then map' t else A.null"
sublocale Map: simulation A resid map⇩e⇩x⇩t
using con_char A.con_implies_arr resid_def
by unfold_locales auto
sublocale Map': simulation resid A map'⇩e⇩x⇩t
using arr_char con_char resid_def
by unfold_locales auto
sublocale inverse_simulations resid A map⇩e⇩x⇩t map'⇩e⇩x⇩t
using arr_char map_null null_char
by unfold_locales auto
lemma invertible_simulation_map:
shows "invertible_simulation A resid map⇩e⇩x⇩t"
using inverse_simulations_axioms inverse_simulations_sym invertible_simulation_def'
by fast
lemma invertible_simulation_map':
shows "invertible_simulation resid A map'⇩e⇩x⇩t"
using inverse_simulations_axioms inverse_simulations_sym invertible_simulation_def'
by fast
lemma inj_on_map:
shows "inj_on map⇩e⇩x⇩t (Collect A.arr)"
using induce_bij_betw_arr_sets bij_betw_def by blast
lemma range_map':
shows "map'⇩e⇩x⇩t ` (Collect arr) = Collect A.arr"
by (metis (no_types, lifting) bij_betw_imp_surj_on
inverse_simulations.induce_bij_betw_arr_sets
inverse_simulations_axioms inverse_simulations_sym)
lemma cong_char⇩I⇩I:
shows "t ∼ u ⟷ Arr t ∧ Arr u ∧ map' t ∼⇩A map' u"
by (metis (full_types) Map'.preserves_resid Map.preserves_ide con_def
ide_char⇩I⇩I not_arr_null null_char resid_def residuation.ide_implies_arr
residuation_axioms)
lemma preserves_weakly_extensional_rts:
assumes "weakly_extensional_rts A"
shows "weakly_extensional_rts resid"
by (metis assms cong_char⇩I⇩I ide_char⇩I⇩I inv_into_injective rts_axioms
weakly_extensional_rts.intro weakly_extensional_rts.weak_extensionality
weakly_extensional_rts_axioms.intro)
lemma preserves_extensional_rts:
assumes "extensional_rts A"
shows "extensional_rts resid"
proof
interpret A: extensional_rts A
using assms by blast
show "⋀t u. t ∼ u ⟹ t = u"
using cong_char⇩I⇩I ide_char⇩I⇩I
by (meson A.extensionality inv_into_injective)
qed
end
lemma inj_image_rts_comp:
fixes F :: "'a ⇒ 'b" and G :: "'b ⇒ 'c"
assumes "inj F" and "inj G"
assumes "rts X"
shows "inj_image_rts.resid (G ∘ F) X =
inj_image_rts.resid G (inj_image_rts.resid F X)"
proof -
interpret X: rts X
using assms(3) by blast
interpret FX: inj_image_rts F X
by (metis X.rts_axioms assms(1)
inj_image_rts_axioms_def inj_image_rts_def inj_on_subset top_greatest)
interpret GFX: inj_image_rts G FX.resid
by (metis (mono_tags, lifting) FX.rts_axioms assms(2) inj_def
inj_image_rts_axioms_def inj_image_rts_def inj_onI)
interpret GoF_X: inj_image_rts ‹G o F› X
by (metis (no_types, opaque_lifting) X.rts_axioms
assms(1-2) inj_compose inj_image_rts_axioms_def
inj_image_rts_def inj_on_subset top_greatest)
show "GoF_X.resid = GFX.resid"
proof -
have "⋀t u. GoF_X.resid t u = GFX.resid t u"
unfolding GoF_X.resid_def GFX.resid_def
using FX.arr_char FX.null_char FX.resid_def GoF_X.map'_map by auto
thus ?thesis by blast
qed
qed
lemma inj_image_rts_map_comp:
fixes F :: "'a ⇒ 'b" and G :: "'b ⇒ 'c"
assumes "inj F" and "inj G"
assumes "rts X"
shows "inj_image_rts.map⇩e⇩x⇩t (G ∘ F) X =
inj_image_rts.map⇩e⇩x⇩t G (inj_image_rts.resid F X) ∘
(inj_image_rts.map⇩e⇩x⇩t F X)"
and "inj_image_rts.map'⇩e⇩x⇩t (G ∘ F) X =
inj_image_rts.map'⇩e⇩x⇩t F X ∘
inj_image_rts.map'⇩e⇩x⇩t G (inj_image_rts.resid F X)"
proof -
interpret X: rts X
using assms(3) by blast
interpret FX: inj_image_rts F X
by (metis X.rts_axioms assms(1) inj_image_rts_axioms_def inj_image_rts_def
inj_on_subset top_greatest)
interpret GFX: inj_image_rts G FX.resid
by (metis FX.rts_axioms Int_UNIV_right assms(2) inj_image_rts.intro
inj_image_rts_axioms.intro inj_on_Int)
interpret GoF_X: inj_image_rts ‹G o F› X
by (metis (no_types, opaque_lifting) X.rts_axioms assms(1-2) inj_compose
inj_image_rts_axioms_def inj_image_rts_def inj_on_subset top_greatest)
show "GoF_X.map⇩e⇩x⇩t = GFX.map⇩e⇩x⇩t ∘ FX.map⇩e⇩x⇩t"
using FX.null_char GFX.null_char GoF_X.null_char by fastforce
show "GoF_X.map'⇩e⇩x⇩t = FX.map'⇩e⇩x⇩t ∘ GFX.map'⇩e⇩x⇩t"
using FX.arr_char FX.not_arr_null GoF_X.map'_map by fastforce
qed
section "Empty RTS"
text‹
For any type, there exists an empty RTS having that type as its arrow type.
Since types in HOL are nonempty, we may use the guaranteed element @{term undefined}
as the null value.
›
locale empty_rts
begin
definition resid :: "'e resid"
where "resid t u = undefined"
sublocale ResiduatedTransitionSystem.partial_magma resid
by unfold_locales (metis resid_def)
lemma null_char:
shows "null = undefined"
by (metis null_is_zero(1) resid_def)
sublocale residuation resid
apply unfold_locales
by (metis resid_def)+
lemma arr_char:
shows "arr t ⟷ False"
using null_char resid_def
by (metis arrE conE)
lemma ide_char⇩E⇩R⇩T⇩S:
shows "ide t ⟷ False"
using arr_char by force
lemma con_char:
shows "con t u ⟷ False"
by (simp add: con_def null_char resid_def)
lemma trg_char:
shows "trg t = null"
by (simp add: null_char resid_def trg_def)
sublocale rts resid
apply unfold_locales
apply (metis arr_char)
by (metis con_char)+
lemma cong_char⇩E⇩R⇩T⇩S:
shows "cong t u ⟷ False"
by (simp add: ide_char⇩E⇩R⇩T⇩S)
sublocale extensional_rts resid
by unfold_locales (simp add: cong_char⇩E⇩R⇩T⇩S)
lemma is_extensional_rts:
shows "extensional_rts resid"
..
lemma src_char:
shows "src t = null"
by (simp add: arr_char src_def)
lemma prfx_char:
shows "prfx t u ⟷ False"
using ide_char⇩E⇩R⇩T⇩S by metis
lemma composite_of_char:
shows "composite_of t u v ⟷ False"
using composite_of_def prfx_char by metis
lemma composable_char:
shows "composable t u ⟷ False"
using composable_def composite_of_char by metis
lemma seq_char:
shows "seq t u ⟷ False"
using arr_char by (metis seqE)
sublocale rts_with_composites resid
by unfold_locales (simp add: composable_char seq_char)
lemma is_rts_with_composites:
shows "rts_with_composites resid"
..
sublocale extensional_rts_with_composites resid ..
lemma is_extensional_rts_with_composites:
shows "extensional_rts_with_composites resid"
..
lemma comp_char:
shows "comp t u = null"
by (meson composable_char composable_iff_comp_not_null)
text‹
There is a unique simulation from an empty RTS to any other RTS.
›
definition initiator :: "'e resid ⇒ 'a ⇒ 'e"
where "initiator A ≡ (λt. ResiduatedTransitionSystem.partial_magma.null A)"
lemma initiator_is_simulation:
assumes "rts A"
shows "simulation resid A (initiator A)"
using assms initiator_def con_char
by (metis rts_axioms simulation_axioms.intro simulation_def)
lemma universality:
assumes "rts A"
shows "∃!F. simulation resid A F"
proof
show "simulation resid A (initiator A)"
using assms initiator_is_simulation by blast
show "⋀F. simulation resid A F ⟹ F = initiator A"
by (metis HOL.ext initiator_def arr_char simulation.extensionality)
qed
end
section "One-Transition RTS"
text ‹
We will call a type ``nondegenerate'' if it has at least two elements.
This means that the type admits RTS's with a non-empty set of arrows
(after using one of the elements for the required null value).
›
locale nondegenerate =
fixes type :: "'a itself"
assumes is_nondegenerate: "∃x y :: 'a. x ≠ y"
text‹
For any type having at least two elements, there exists a one-transition RTS
having that type as its arrow type. We use the already-distinguished element
@{term undefined} as the null value and some value distinct from @{term undefined}
as the single transition.
›
locale one_arr_rts =
nondegenerate arr_type
for arr_type :: "'t itself"
begin
definition the_arr :: 't
where "the_arr ≡ SOME t. t ≠ undefined"
definition resid :: "'t resid" (infix ‹\⇩1› 70)
where "resid t u = (if t = the_arr ∧ u = the_arr then the_arr else undefined)"
sublocale ResiduatedTransitionSystem.partial_magma resid
using resid_def
by unfold_locales metis
lemma null_char:
shows "null = undefined"
by (metis null_is_zero(1) resid_def)
sublocale residuation resid
using null_char resid_def
by unfold_locales metis+
notation con (infix ‹⌢⇩1› 50)
lemma arr_char:
shows "arr t ⟷ t = the_arr"
using null_char resid_def is_nondegenerate
by (metis (mono_tags, lifting) arr_def con_def someI_ex the_arr_def)
lemma ide_char⇩1⇩R⇩T⇩S:
shows "ide t ⟷ t = the_arr"
using arr_char ide_def resid_def by auto
lemma con_char:
shows "con t u ⟷ arr t ∧ arr u"
by (metis arr_char con_arr_self con_implies_arr(2) con_sym)
lemma trg_char:
shows "trg t = (if arr t then t else null)"
by (simp add: arr_char null_char resid_def trg_def)
sublocale rts resid
using con_char arr_char ide_char⇩1⇩R⇩T⇩S trg_char ideE
by unfold_locales metis+
notation prfx (infix ‹≲⇩1› 50)
notation cong (infix ‹∼⇩1› 50)
lemma cong_char⇩1⇩R⇩T⇩S:
shows "t ≲⇩1 u ⟷ arr t ∧ arr u"
using arr_char ide_char⇩1⇩R⇩T⇩S not_ide_null null_char resid_def by force
sublocale extensional_rts resid
using arr_char cong_char⇩1⇩R⇩T⇩S
by unfold_locales auto
lemma is_extensional_rts:
shows "extensional_rts resid"
..
lemma src_char:
shows "src t = (if t = the_arr then t else null)"
using arr_char ide_char⇩1⇩R⇩T⇩S src_def src_ide by presburger
lemma prfx_char:
shows "t ≲⇩1 u ⟷ arr t ∧ arr u"
by (metis cong_char⇩1⇩R⇩T⇩S)
lemma composite_of_char:
shows "composite_of t u v ⟷ arr t ∧ arr u ∧ arr v"
using composite_of_def
by (metis composite_of_ide_self prfx_char)
lemma composable_char:
shows "composable t u ⟷ arr t ∧ arr u"
using composable_def composite_of_char by auto
lemma seq_char:
shows "seq t u ⟷ arr t ∧ arr u"
using arr_char composable_char composable_imp_seq by auto
sublocale rts_with_composites resid
by unfold_locales (simp add: composable_char seq_char)
lemma is_rts_with_composites:
shows "rts_with_composites resid"
..
sublocale extensional_rts_with_composites resid ..
lemma is_extensional_rts_with_composites:
shows "extensional_rts_with_composites resid"
..
lemma comp_char:
shows "comp t u = (if arr t ∧ arr u then the_arr else null)"
using arr_char composable_iff_comp_not_null trg_char by auto
text‹
For an arbitrary RTS ‹A›, there is a unique simulation from ‹A› to the one-transition RTS.
›
definition terminator :: "'a resid ⇒ 'a ⇒ 't"
where "terminator A ≡ (λt. if residuation.arr A t then the_arr else null)"
lemma terminator_is_simulation:
assumes "rts A"
shows "simulation A resid (terminator A)"
proof -
interpret A: rts A
using assms by blast
show ?thesis
unfolding terminator_def
using assms ide_char⇩1⇩R⇩T⇩S ideE A.con_implies_arr
apply (unfold_locales)
by auto metis
qed
lemma universality:
assumes "rts A"
shows "∃!F. simulation A resid F"
proof
show "simulation A resid (terminator A)"
using assms terminator_is_simulation by blast
show "⋀F. simulation A resid F ⟹ F = terminator A"
unfolding terminator_def
by (meson arr_char simulation.extensionality
simulation.preserves_reflects_arr)
qed
text‹
A ``global transition'' of an RTS ‹A› is a transformation from the one-arrow RTS
to ‹A›. An important fact is that equality of simulations and of transformations
is determined by their compositions with global transitions.
›
lemma eq_simulation_iff:
assumes "weakly_extensional_rts A"
and "simulation A B F" and "simulation A B G"
shows "F = G ⟷
(∀Q R T. transformation resid A Q R T ⟶ F ∘ T = G ∘ T)"
proof
interpret A: weakly_extensional_rts A
using assms(1) simulation_def by blast
interpret F: simulation A B F
using assms(2) by blast
interpret G: simulation A B G
using assms(3) by blast
show "F = G ⟹
∀Q R T. transformation resid A Q R T ⟶ F ∘ T = G ∘ T"
by blast
show "∀Q R T. transformation resid A Q R T ⟶ F ∘ T = G ∘ T
⟹ F = G"
proof -
have "F ≠ G ⟹
(∃Q R T. transformation resid A Q R T ∧ F ∘ T ≠ G ∘ T)"
proof -
assume 1: "F ≠ G"
obtain t where t: "A.arr t ∧ F t ≠ G t"
using 1 F.extensionality G.extensionality by fastforce
interpret T: constant_transformation resid A t
using t by unfold_locales blast
have "transformation resid A T.F T.G T.map"
using T.transformation_axioms by simp
moreover have "F ∘ T.map ≠ G ∘ T.map"
by (metis (mono_tags, lifting) arr_char comp_apply t)
ultimately show "∃Q R T. transformation resid A Q R T ∧
F ∘ T ≠ G ∘ T"
by blast
qed
thus "∀Q R T. transformation resid A Q R T ⟶ F ∘ T = G ∘ T
⟹ F = G"
by blast
qed
qed
lemma eq_transformation_iff:
assumes "weakly_extensional_rts A" and "weakly_extensional_rts B"
and "transformation A B F G U" and "transformation A B F G V"
shows "U = V ⟷
(∀Q R T. transformation resid A Q R T ⟶ U ∘ T = V ∘ T)"
proof
interpret A: weakly_extensional_rts A
using assms(1) simulation_def by blast
interpret B: weakly_extensional_rts B
using assms(2) simulation_def by blast
interpret U: transformation A B F G U
using assms(3) by blast
interpret V: transformation A B F G V
using assms(4) by blast
show "U = V ⟹
∀Q R T. transformation resid A Q R T ⟶ U ∘ T = V ∘ T"
by blast
show "∀Q R T. transformation resid A Q R T ⟶ U ∘ T = V ∘ T
⟹ U = V"
proof -
have "U ≠ V ⟹
(∃Q R T. transformation resid A Q R T ∧ U ∘ T ≠ V ∘ T)"
proof -
assume 1: "U ≠ V"
obtain t where t: "A.arr t ∧ U t ≠ V t"
using 1 U.extensionality V.extensionality by fastforce
interpret T: constant_transformation resid A t
using t by unfold_locales blast
have "transformation resid A T.F T.G T.map"
using T.transformation_axioms by simp
moreover have "U ∘ T.map ≠ V ∘ T.map"
by (metis (mono_tags, lifting) arr_char comp_apply t)
ultimately show "∃Q R T. transformation resid A Q R T ∧
U ∘ T ≠ V ∘ T"
by blast
qed
thus "∀Q R T. transformation resid A Q R T ⟶ U ∘ T = V ∘ T
⟹ U = V"
by blast
qed
qed
end
section "Fiber Product RTS"
locale fiber_product_rts =
A: rts A +
B: rts B +
C: weakly_extensional_rts C +
F: simulation A C F +
G: simulation B C G
for A :: "'a resid" (infix ‹\⇩A› 70)
and B :: "'b resid" (infix ‹\⇩B› 70)
and C :: "'c resid" (infix ‹\⇩C› 70)
and F :: "'a ⇒ 'c"
and G :: "'b ⇒ 'c"
begin
notation A.con (infix ‹⌢⇩A› 50)
notation B.con (infix ‹⌢⇩B› 50)
notation C.con (infix ‹⌢⇩C› 50)
notation A.prfx (infix ‹≲⇩A› 50)
notation B.prfx (infix ‹≲⇩B› 50)
notation C.prfx (infix ‹≲⇩C› 50)
notation A.cong (infix ‹∼⇩A› 50)
notation B.cong (infix ‹∼⇩B› 50)
notation C.cong (infix ‹∼⇩C› 50)
abbreviation Arr
where "Arr ≡ λtu. A.arr (fst tu) ∧ B.arr (snd tu) ∧ F (fst tu) = G (snd tu)"
abbreviation Ide
where "Ide ≡ λtu. A.ide (fst tu) ∧ B.ide (snd tu) ∧ F (fst tu) = G (snd tu)"
abbreviation Con
where "Con ≡ λtu vw. fst tu ⌢⇩A fst vw ∧ snd tu ⌢⇩B snd vw ∧
F (fst tu) = G (snd tu) ∧ F (fst vw) = G (snd vw)"
definition resid :: "('a * 'b) resid" (infix ‹\› 70)
where "tu \\ vw =
(if Con tu vw then (fst tu \\⇩A fst vw, snd tu \\⇩B snd vw)
else (A.null, B.null))"
sublocale ResiduatedTransitionSystem.partial_magma resid
using resid_def
by unfold_locales
(metis B.arr_resid_iff_con B.ex_un_null B.not_arr_null
B.null_is_zero(2) snd_conv)
lemma null_char:
shows "null = (A.null, B.null)"
unfolding null_def
using ex_un_null resid_def
the1_equality [of "λn. ∀f. n \\ f = n ∧ f \\ n = n" "(A.null, B.null)"]
by simp
sublocale residuation resid
proof
show "⋀t u. t \\ u ≠ null ⟹ u \\ t ≠ null"
by (metis A.con_sym B.con_sym B.residuation_axioms null_char prod.inject
resid_def residuation.con_def)
show "⋀t u. t \\ u ≠ null ⟹ (t \\ u) \\ (t \\ u) ≠ null"
by (metis (no_types, lifting) A.conE A.conI A.con_imp_arr_resid B.con_def
B.con_imp_arr_resid F.preserves_resid G.preserves_resid fst_conv null_char
resid_def snd_conv)
show "⋀v t u. (v \\ t) \\ (u \\ t) ≠ null ⟹ (v \\ t) \\ (u \\ t) = (v \\ u) \\ (t \\ u)"
proof -
fix v t u
assume 1: "(v \\ t) \\ (u \\ t) ≠ null"
have 2: "(v \\ t) \\ (u \\ t) =
((fst v \\⇩A fst t) \\⇩A (fst u \\⇩A fst t),
(snd v \\⇩B snd t) \\⇩B (snd u \\⇩B snd t))"
using 1 resid_def null_char by auto
also have "... = ((fst v \\⇩A fst u) \\⇩A (fst t \\⇩A fst u),
(snd v \\⇩B snd u) \\⇩B (snd t \\⇩B snd u))"
using A.cube B.cube by simp
also have "... = (v \\ u) \\ (t \\ u)"
proof -
have "Con (v \\ u) (t \\ u)"
proof -
have "fst v \\⇩A fst u ⌢⇩A fst t \\⇩A fst u"
using 1 2 A.cube
by (metis (no_types, lifting) A.con_def fst_conv null_char resid_def)
moreover have "snd v \\⇩B snd u ⌢⇩B snd t \\⇩B snd u"
using 1 2 B.cube
by (metis (no_types, lifting) B.con_def null_char resid_def snd_conv)
ultimately show ?thesis
using 1 resid_def
by (metis (no_types, lifting) A.conI A.con_implies_arr(1) A.not_arr_null
A.not_con_null(2) B.conI B.con_implies_arr(1) B.not_arr_null
B.not_con_null(2) F.preserves_resid G.preserves_resid fst_eqD
null_char snd_eqD)
qed
thus ?thesis
using resid_def null_char by auto
qed
finally show "(v \\ t) \\ (u \\ t) = (v \\ u) \\ (t \\ u)"
by blast
qed
qed
notation con (infix ‹⌢› 50)
lemma arr_char:
shows "arr t ⟷ Arr t"
by (metis B.arr_def B.conE Pair_inject conE conI null_char resid_def
A.arr_def arr_def)
lemma con_char:
shows "t ⌢ u ⟷ Con t u"
by (metis B.conE null_char resid_def con_def snd_conv)
lemma ide_char⇩F⇩P:
shows "ide t ⟷ Ide t"
unfolding ide_def
using con_char resid_def
by (metis (no_types, lifting) A.ide_def fst_conv prod.exhaust_sel
B.ide_def snd_conv)
lemma trg_char:
shows "trg t = (if arr t then (A.trg (fst t), B.trg (snd t)) else null)"
by (simp add: A.trg_def B.trg_def con_char null_char resid_def
arr_def trg_def)
sublocale rts resid
proof
show "⋀t. arr t ⟹ ide (trg t)"
using trg_char ide_char⇩F⇩P arr_char F.preserves_trg G.preserves_trg
apply simp
using F.preserves_trg G.preserves_trg by metis
show 1: "⋀a t. ⟦ide a; t ⌢ a⟧ ⟹ t \\ a = t"
by (simp add: A.resid_arr_ide B.resid_arr_ide con_char ide_char⇩F⇩P
resid_def)
show "⋀a t. ⟦ide a; a ⌢ t⟧ ⟹ ide (a \\ t)"
by (metis 1 arr_resid_iff_con con_sym cube ide_def)
show "⋀t u. t ⌢ u ⟹ ∃a. ide a ∧ a ⌢ t ∧ a ⌢ u"
proof -
fix t u
assume con: "t ⌢ u"
obtain a where a: "A.ide a ∧ a ⌢⇩A fst t ∧ a ⌢⇩A fst u"
using con con_char A.con_imp_coinitial_ax by fastforce
obtain b where b: "B.ide b ∧ b ⌢⇩B snd t ∧ b ⌢⇩B snd u"
using con con_char B.con_imp_coinitial_ax by fastforce
have "F a = G b"
by (metis C.src_eqI F.preserves_con F.preserves_ide G.preserves_con
G.preserves_ide a b con con_char)
thus "∃a. ide a ∧ a ⌢ t ∧ a ⌢ u"
using a b ide_char⇩F⇩P con con_char by auto
qed
show "⋀t u v. ⟦ide (t \\ u); u ⌢ v⟧ ⟹ t \\ u ⌢ v \\ u"
by (metis (no_types, lifting) A.con_target B.con_target arr_char
arr_resid_iff_con con_char con_sym fst_conv ide_char⇩F⇩P
ide_implies_arr resid_def snd_conv)
qed
notation prfx (infix ‹≲› 50)
notation cong (infix ‹∼› 50)
lemma prfx_char:
shows "t ≲ u ⟷ F (fst t) = G (snd t) ∧ F (fst u) = G (snd u) ∧
fst t ≲⇩A fst u ∧ snd t ≲⇩B snd u"
using A.prfx_implies_con B.prfx_implies_con ide_char⇩F⇩P resid_def
by auto
lemma cong_char⇩F⇩P:
shows "t ∼ u ⟷ F (fst t) = G (snd t) ∧ F (fst u) = G (snd u) ∧
fst t ∼⇩A fst u ∧ snd t ∼⇩B snd u"
using prfx_char by auto
lemma sources_char:
shows "sources t =
{a. F (fst t) = G (snd t) ∧ F (fst a) = G (snd a) ∧
fst a ∈ A.sources (fst t) ∧ snd a ∈ B.sources (snd t)}"
using con_char ide_char⇩F⇩P sources_def by auto
lemma targets_char⇩F⇩P:
shows "targets t =
{a. F (fst t) = G (snd t) ∧ F (fst a) = G (snd a) ∧
fst a ∈ A.targets (fst t) ∧ snd a ∈ B.targets (snd t)}"
proof
show "targets t ⊆ {a. F (fst t) = G (snd t) ∧ F (fst a) = G (snd a) ∧
fst a ∈ A.targets (fst t) ∧ snd a ∈ B.targets (snd t)}"
using arr_char arr_iff_has_target ide_char⇩F⇩P
apply auto[1]
apply (metis arr_char arr_composite_of composite_of_arr_ide in_targetsE
trg_def)
apply (metis A.in_targetsI con_char con_implies_arr(1) fst_conv
in_targetsE not_arr_null trg_char)
by (metis B.in_targetsI con_char con_implies_arr(1) in_targetsE
not_arr_null snd_conv trg_char)
show "{a. F (fst t) = G (snd t) ∧ F (fst a) = G (snd a) ∧
fst a ∈ A.targets (fst t) ∧ snd a ∈ B.targets (snd t)} ⊆ targets t"
using A.arr_iff_has_target B.arr_iff_has_target arr_char con_char
ide_char⇩F⇩P ide_trg targets_def trg_char
by auto
qed
definition P⇩0 :: "'a × 'b ⇒ 'b"
where "P⇩0 t ≡ if arr t then snd t else B.null"
definition P⇩1 :: "'a × 'b ⇒ 'a"
where "P⇩1 t ≡ if arr t then fst t else A.null"
sublocale P⇩0: simulation resid B P⇩0
using P⇩0_def con_char resid_def arr_resid con_implies_arr(1-2)
by unfold_locales auto
lemma P⇩0_is_simulation:
shows "simulation resid B P⇩0"
..
sublocale P⇩1: simulation resid A P⇩1
using P⇩1_def con_char resid_def arr_resid con_implies_arr(1-2)
by unfold_locales auto
lemma P⇩1_is_simulation:
shows "simulation resid A P⇩1"
..
lemma commutativity:
shows "F o P⇩1 = G o P⇩0"
using F.extensionality G.extensionality P⇩1_def P⇩0_def arr_char by auto
definition tuple :: "'x resid ⇒ ('x ⇒ 'a) ⇒ ('x ⇒ 'b) ⇒ 'x ⇒ 'a × 'b"
where "tuple X H K ≡ λt. if residuation.arr X t then (H t, K t) else null"
lemma universality:
assumes "rts X" and "simulation X A H" and "simulation X B K"
and "F o H = G o K"
shows [intro]: "simulation X resid (tuple X H K)"
and "P⇩1 ∘ tuple X H K = H" and "P⇩0 ∘ tuple X H K = K"
and "∃!HK. simulation X resid HK ∧ P⇩1 o HK = H ∧ P⇩0 o HK = K"
proof -
interpret X: rts X
using assms(1) by blast
interpret H: simulation X A H
using assms(2) by blast
interpret K: simulation X B K
using assms(3) by blast
let ?HK = "tuple X H K"
interpret HK: simulation X resid ?HK
proof
show "⋀t. ¬ X.arr t ⟹ ?HK t = null"
unfolding tuple_def by simp
fix t u
assume con: "X.con t u"
have 1: "X.arr t ∧ X.arr u"
using con X.con_implies_arr(1) X.con_implies_arr(2) by force
show 2: "con (?HK t) (?HK u)"
by (metis 1 assms(4) comp_apply con con_char fst_conv tuple_def
H.preserves_con K.preserves_con snd_conv)
show "?HK (X t u) = resid (?HK t) (?HK u)"
using 1 2 con resid_def null_char con_char arr_char
by (simp add: tuple_def)
qed
show "simulation X resid (tuple X H K)"
..
show "P⇩1 ∘ ?HK = H"
proof
fix t
show "(P⇩1 ∘ ?HK) t = H t"
using P⇩1_def HK.preserves_reflects_arr
by (simp add: H.extensionality tuple_def)
qed
moreover show "P⇩0 ∘ ?HK = K"
proof
fix t
show "(P⇩0 ∘ ?HK) t = K t"
using P⇩0_def HK.preserves_reflects_arr
by (simp add: K.extensionality tuple_def)
qed
ultimately
have "simulation X resid ?HK ∧ P⇩1 ∘ ?HK = H ∧ P⇩0 ∘ ?HK = K"
using HK.simulation_axioms by simp
moreover have "⋀M. simulation X resid M ∧ P⇩1 ∘ M = H ∧ P⇩0 ∘ M = K
⟹ M = ?HK"
unfolding P⇩1_def P⇩0_def tuple_def
using simulation.extensionality simulation.preserves_reflects_arr
by fastforce
ultimately show "∃!HK. simulation X resid HK ∧
P⇩1 o HK = H ∧ P⇩0 o HK = K"
by auto
qed
lemma preserves_weakly_extensional_rts:
assumes "weakly_extensional_rts A" and "weakly_extensional_rts B"
shows "weakly_extensional_rts resid"
using assms
by unfold_locales
(metis con_char ide_char⇩F⇩P prod.exhaust_sel prfx_implies_con
weakly_extensional_rts.con_ide_are_eq)
lemma preserves_extensional_rts:
assumes "extensional_rts A" and "extensional_rts B"
shows "extensional_rts resid"
using assms
by unfold_locales
(metis (no_types, lifting) extensional_rts.extensionality fst_conv ide_char⇩F⇩P
ide_implies_arr not_arr_null null_char prod.exhaust_sel resid_def snd_conv)
end
locale fiber_product_of_weakly_extensional_rts =
A: weakly_extensional_rts A +
B: weakly_extensional_rts B +
fiber_product_rts
begin
sublocale weakly_extensional_rts resid
using A.weakly_extensional_rts_axioms B.weakly_extensional_rts_axioms
preserves_weakly_extensional_rts
by auto
lemma is_weakly_extensional_rts:
shows "weakly_extensional_rts resid"
..
lemma src_char:
shows "src t = (if arr t then (A.src (fst t), B.src (snd t)) else null)"
proof (cases "arr t")
show "¬ arr t ⟹ ?thesis"
using src_def by presburger
assume t: "arr t"
show ?thesis
proof (intro src_eqI)
show "ide (if arr t then (A.src (fst t), B.src (snd t)) else null)"
using t ide_char⇩F⇩P
by simp (metis A.src_eqI B.src_eqI con_arr_src(2) con_char ide_src)
show "(if arr t then (A.src (fst t), B.src (snd t)) else null) ⌢ t"
using t con_char arr_char
by simp
(metis A.arr_def A.src_eqI B.arr_def B.src_eqI
con_imp_coinitial_ax ide_char⇩F⇩P)
qed
qed
end
locale fiber_product_of_extensional_rts =
A: extensional_rts A +
B: extensional_rts B +
fiber_product_of_weakly_extensional_rts
begin
sublocale fiber_product_of_weakly_extensional_rts A B ..
sublocale extensional_rts resid
using A.extensional_rts_axioms B.extensional_rts_axioms preserves_extensional_rts
by blast
lemma is_extensional_rts:
shows "extensional_rts resid"
..
end
section "Product RTS"
text‹
It is possible to define a product construction for RTS's as a special case of the
fiber product, but some inconveniences result from that approach.
In addition, we have already defined a product construction in
@{theory ResiduatedTransitionSystem.ResiduatedTransitionSystem}.
So, we will build on that existing construction.
›
notation product_rts.resid (infixr ‹⨂› 51)
definition pointwise_tuple :: "('x ⇒ 'a) ⇒ ('x ⇒ 'b) ⇒ 'x ⇒ 'a × 'b" (‹⟨⟨_, _⟩⟩›)
where "pointwise_tuple H K ≡ (λt. (H t, K t))"
context product_rts
begin
definition P⇩0 :: "'a × 'b ⇒ 'b"
where "P⇩0 t ≡ if arr t then snd t else B.null"
definition P⇩1 :: "'a × 'b ⇒ 'a"
where "P⇩1 t ≡ if arr t then fst t else A.null"
sublocale P⇩0: simulation resid B P⇩0
using P⇩0_def con_char resid_def arr_resid con_implies_arr(1-2)
by unfold_locales auto
lemma P⇩0_is_simulation:
shows "simulation resid B P⇩0"
..
sublocale P⇩1: simulation resid A P⇩1
using P⇩1_def con_char resid_def arr_resid con_implies_arr(1-2)
by unfold_locales auto
lemma P⇩1_is_simulation:
shows "simulation resid A P⇩1"
..
abbreviation tuple :: "('x ⇒ 'a) ⇒ ('x ⇒ 'b) ⇒ 'x ⇒ 'a × 'b"
where "tuple ≡ pointwise_tuple"
lemma universality:
assumes "simulation X A H" and "simulation X B K"
shows [intro]: "simulation X resid ⟨⟨H, K⟩⟩"
and "P⇩1 ∘ ⟨⟨H, K⟩⟩ = H" and "P⇩0 ∘ ⟨⟨H, K⟩⟩ = K"
and "∃!HK. simulation X resid HK ∧ P⇩1 o HK = H ∧ P⇩0 o HK = K"
proof -
interpret H: simulation X A H
using assms(1) by blast
interpret K: simulation X B K
using assms(2) by blast
interpret HK: simulation X resid ‹⟨⟨H, K⟩⟩›
proof
show "⋀t. ¬ H.A.arr t ⟹ ⟨⟨H, K⟩⟩ t = null"
by (simp add: H.extensionality K.extensionality pointwise_tuple_def)
fix t u
assume con: "H.A.con t u"
have 1: "H.A.arr t ∧ H.A.arr u"
using con H.A.con_implies_arr(1-2) by force
show "con (⟨⟨H, K⟩⟩ t) (⟨⟨H, K⟩⟩ u)"
using 1 con con_char H.preserves_con K.preserves_con pointwise_tuple_def
by (metis fst_conv snd_conv)
thus "⟨⟨H, K⟩⟩ (X t u) = resid (⟨⟨H, K⟩⟩ t) (⟨⟨H, K⟩⟩ u)"
unfolding pointwise_tuple_def
using 1 con resid_def null_char con_char arr_char
by simp
qed
show "simulation X resid ⟨⟨H, K⟩⟩" ..
show "P⇩1 ∘ ⟨⟨H, K⟩⟩ = H"
unfolding pointwise_tuple_def
using P⇩1_def HK.preserves_reflects_arr
by (auto simp add: H.extensionality)
moreover show "P⇩0 ∘ ⟨⟨H, K⟩⟩ = K"
unfolding pointwise_tuple_def
using P⇩0_def HK.preserves_reflects_arr
by (auto simp add: K.extensionality)
ultimately have "simulation X resid ⟨⟨H, K⟩⟩ ∧
P⇩1 ∘ ⟨⟨H, K⟩⟩ = H ∧ P⇩0 ∘ ⟨⟨H, K⟩⟩ = K"
using HK.simulation_axioms by simp
moreover have "⋀M. simulation X resid M ∧ P⇩1 ∘ M = H ∧ P⇩0 ∘ M = K
⟹ M = ⟨⟨H, K⟩⟩"
proof
fix M t
assume 1: "simulation X resid M ∧ P⇩1 ∘ M = H ∧ P⇩0 ∘ M = K"
interpret M: simulation X resid M
using 1 by blast
show "M t = ⟨⟨H, K⟩⟩ t"
using 1 M.extensionality M.preserves_reflects_arr
unfolding P⇩1_def P⇩0_def pointwise_tuple_def
by force
qed
ultimately
show "∃!HK. simulation X resid HK ∧ P⇩1 o HK = H ∧ P⇩0 o HK = K"
by auto
qed
lemma proj_joint_monic:
assumes "simulation X resid F" and "simulation X resid G"
and "P⇩0 ∘ F = P⇩0 ∘ G" and "P⇩1 ∘ F = P⇩1 ∘ G"
shows "F = G"
using assms(1-4) P⇩0_is_simulation P⇩1_is_simulation universality(4)
by blast
lemma tuple_proj:
assumes "simulation X resid F"
shows "⟨⟨P⇩1 ∘ F, P⇩0 ∘ F⟩⟩ = F"
by (meson P⇩0_is_simulation P⇩1_is_simulation proj_joint_monic assms
universality(1-3) simulation_comp)
lemma proj_tuple:
assumes "simulation X A F" and "simulation X B G"
shows "P⇩1 ∘ ⟨⟨F, G⟩⟩ = F" and "P⇩0 ∘ ⟨⟨F, G⟩⟩ = G"
using assms(1-2) universality(2-3) by auto
lemma preserves_weakly_extensional_rts:
assumes "weakly_extensional_rts A" and "weakly_extensional_rts B"
shows "weakly_extensional_rts resid"
by (metis assms(1-2) ide_char prfx_char prod.exhaust_sel rts_axioms
weakly_extensional_rts.intro weakly_extensional_rts.weak_extensionality
weakly_extensional_rts_axioms.intro)
lemma preserves_extensional_rts:
assumes "extensional_rts A" and "extensional_rts B"
shows "extensional_rts resid"
proof -
interpret A: extensional_rts A
using assms(1) by blast
interpret B: extensional_rts B
using assms(2) by blast
show ?thesis
by unfold_locales
(metis A.extensionality B.extensionality cong_char prod.collapse)
qed
lemma preserves_rts_with_composites:
assumes "rts_with_composites A" and "rts_with_composites B"
shows "rts_with_composites resid"
proof
fix t u
assume seq: "seq t u"
have 1: "A.seq (fst t) (fst u)"
using seq sources_char targets_char
apply (elim seqE, intro A.seqI)
apply auto[1]
by (simp add: A.arr_iff_has_target B.arr_iff_has_target times_eq_iff)
have 2: "B.seq (snd t) (snd u)"
using seq sources_char targets_char
apply (elim seqE, intro B.seqI)
apply auto[1]
by (simp add: A.arr_iff_has_target B.arr_iff_has_target times_eq_iff)
obtain fv where fv: "A.composite_of (fst t) (fst u) fv"
using 1
by (meson assms(1) rts_with_composites.obtains_composite_of)
obtain sv where sv: "B.composite_of (snd t) (snd u) sv"
using 2
by (meson assms(2) rts_with_composites.obtains_composite_of)
have "composite_of t u (fv, sv)"
proof
show "t ≲ (fv, sv)"
using fv prfx_char sv by auto
show "(fv, sv) \\ t ∼ u"
proof
show "(fv, sv) \\ t ≲ u"
using fv sv
apply (elim A.composite_ofE B.composite_ofE)
by (metis A.con_implies_arr(1) A.not_arr_null A.residuation_axioms
B.con_sym fst_conv prfx_char resid_def residuation.conI snd_conv)
show "u ≲ (fv, sv) \\ t"
using fv sv
apply (elim A.composite_ofE B.composite_ofE)
by (simp add: A.con_sym A.prfx_implies_con B.con_sym B.prfx_implies_con
product_rts.resid_def product_rts_axioms)
qed
qed
thus "composable t u"
using composable_def by auto
qed
lemma preserves_extensional_rts_with_composites:
assumes "extensional_rts_with_composites A" and "extensional_rts_with_composites B"
shows "extensional_rts_with_composites resid"
using assms preserves_extensional_rts preserves_rts_with_composites
by (simp add: extensional_rts_with_composites_def)
end
locale product_of_extensional_rts =
A: extensional_rts A +
B: extensional_rts B +
product_rts
begin
sublocale product_of_weakly_extensional_rts A B ..
sublocale extensional_rts resid
using A.extensional_rts_axioms B.extensional_rts_axioms preserves_extensional_rts
by blast
lemma is_extensional_rts:
shows "extensional_rts resid"
..
lemma proj_tuple2:
assumes "transformation X A F G S" and "transformation X B H K T"
shows "P⇩1 ∘ ⟨⟨S, T⟩⟩ = S" and "P⇩0 ∘ ⟨⟨S, T⟩⟩ = T"
proof -
interpret S: transformation X A F G S
using assms(1) by blast
interpret T: transformation X B H K T
using assms(2) by blast
show "P⇩1 ∘ ⟨⟨S, T⟩⟩ = S"
proof
fix t
show "(P⇩1 ∘ ⟨⟨S, T⟩⟩) t = S t"
unfolding pointwise_tuple_def P⇩1_def
using S.extensionality S.preserves_arr T.preserves_arr
apply auto[1]
by metis+
qed
show "P⇩0 ∘ ⟨⟨S, T⟩⟩ = T"
proof
fix t
show "(P⇩0 ∘ ⟨⟨S, T⟩⟩) t = T t"
unfolding pointwise_tuple_def P⇩0_def
using T.extensionality S.preserves_arr T.preserves_arr
apply auto[1]
by metis+
qed
qed
lemma universality2:
assumes "simulation X resid F" and "simulation X resid G"
and "transformation X A (P⇩1 ∘ F) (P⇩1 ∘ G) S"
and "transformation X B (P⇩0 ∘ F) (P⇩0 ∘ G) T"
shows [intro]: "transformation X resid F G ⟨⟨S, T⟩⟩"
and "P⇩1 ∘ ⟨⟨S, T⟩⟩ = S" and "P⇩0 ∘ ⟨⟨S, T⟩⟩ = T"
and "∃!ST. transformation X resid F G ST ∧ P⇩1 o ST = S ∧ P⇩0 o ST = T"
proof -
interpret X: rts X
using assms(1) simulation_def by auto
interpret A: weakly_extensional_rts A
using assms(3) transformation_def by blast
interpret B: weakly_extensional_rts B
using assms(4) transformation_def by blast
interpret X: rts X
using assms(4) transformation_def by blast
interpret F: simulation X resid F
using assms(1) by blast
interpret F: simulation_to_weakly_extensional_rts X resid F ..
interpret G: simulation X resid G
using assms(2) by blast
interpret G: simulation_to_weakly_extensional_rts X resid G ..
interpret P⇩1oF: composite_simulation X resid A F P⇩1 ..
interpret P⇩1oF: simulation_to_weakly_extensional_rts X A P⇩1oF.map ..
interpret P⇩1oG: composite_simulation X resid A G P⇩1 ..
interpret P⇩1oG: simulation_to_weakly_extensional_rts X A P⇩1oF.map ..
interpret P⇩0oF: composite_simulation X resid B F P⇩0 ..
interpret P⇩0oF: simulation_to_weakly_extensional_rts X A P⇩1oF.map ..
interpret P⇩0oG: composite_simulation X resid B G P⇩0 ..
interpret P⇩0oF: simulation_to_weakly_extensional_rts X A P⇩1oF.map ..
interpret S: transformation X A ‹P⇩1 ∘ F› ‹P⇩1 ∘ G› S
using assms(3) by blast
interpret S: transformation_to_extensional_rts X A ‹P⇩1 ∘ F› ‹P⇩1 ∘ G› S ..
interpret T: transformation X B ‹P⇩0 ∘ F› ‹P⇩0 ∘ G› T
using assms(4) by blast
interpret T: transformation_to_extensional_rts X B ‹P⇩0 ∘ F› ‹P⇩0 ∘ G› T ..
interpret ST: transformation X resid F G ‹⟨⟨S, T⟩⟩›
proof
show "⋀t. ¬ X.arr t ⟹ ⟨⟨S, T⟩⟩ t = null"
by (simp add: S.extensionality T.extensionality pointwise_tuple_def)
fix t
assume t: "X.ide t"
have arr: "arr (⟨⟨S, T⟩⟩ t)"
unfolding pointwise_tuple_def
using t S.preserves_arr T.preserves_arr by auto
show "src (⟨⟨S, T⟩⟩ t) = F t"
proof -
have "F t = ((P⇩1 ∘ F) t, (P⇩0 ∘ F) t)"
using t tuple_proj F.simulation_axioms pointwise_tuple_def
by metis
thus ?thesis
using arr src_char arr_char
by (simp add: S.preserves_src T.preserves_src t pointwise_tuple_def)
qed
show "trg (⟨⟨S, T⟩⟩ t) = G t"
proof -
have "G t = ((P⇩1 ∘ G) t, (P⇩0 ∘ G) t)"
using t tuple_proj G.simulation_axioms pointwise_tuple_def
by metis
thus ?thesis
using arr trg_char arr_char
by (simp add: S.preserves_trg T.preserves_trg t pointwise_tuple_def)
qed
show "⋀a a'. ⟦X.ide a; X.cong a a'⟧ ⟹ tuple S T a = tuple S T a'"
by (simp add: S.respects_cong_ide T.respects_cong_ide pointwise_tuple_def)
next
fix a t
assume t: "a ∈ X.sources t"
have con1: "S a ⌢⇩A P⇩1 (F t)"
proof -
have "S t = A.join (S a) (P⇩1 (F t))"
by (metis A.join_is_join_of A.join_of_unique A.joinable_def S.naturality3
comp_apply t)
hence "A.prfx (S a) (S t) ∧ A.prfx (P⇩1 (F t)) (S t)"
by (metis A.composite_ofE S.naturality1' S.preserves_prfx X.con_implies_arr(1)
X.in_sourcesE X.source_is_prfx o_apply t)
thus ?thesis
using A.con_prfx(1) A.prfx_implies_con by blast
qed
moreover have con0: "T a ⌢⇩B P⇩0 (F t)"
proof -
have "T t = B.join (T a) (P⇩0 (F t))"
by (metis B.join_is_join_of B.join_of_unique B.joinable_def T.naturality3
o_apply t)
hence "B.prfx (T a) (T t) ∧ B.prfx (P⇩0 (F t)) (T t)"
by (metis B.arr_prfx_join_self B.join_def B.join_sym B.null_is_zero(2)
T.preserves_prfx X.source_is_prfx t)
thus ?thesis
using B.con_prfx(1) B.prfx_implies_con by blast
qed
show "⟨⟨S, T⟩⟩ a \\ F t = ⟨⟨S, T⟩⟩ (X a t)"
proof -
have "⟨⟨S, T⟩⟩ a \\ F t =
(S a, T a) \\ (P⇩1 (F t), P⇩0 (F t))"
using t tuple_proj [of X F] F.simulation_axioms
pointwise_tuple_def [of S T]
pointwise_tuple_def [of P⇩1oF.map P⇩0oF.map]
apply auto[1]
by metis
also have "... = (S a \\⇩A P⇩1 (F t), T a \\⇩B P⇩0 (F t))"
using t con0 con1 resid_def by auto
also have "... = (S (X a t), T (X a t))"
using S.naturality1_ax T.naturality1_ax t by force
also have "... = ⟨⟨S, T⟩⟩ (X a t)"
using t pointwise_tuple_def by metis
finally show ?thesis by force
qed
show "F t \\ ⟨⟨S, T⟩⟩ a = G t"
proof -
have "F t \\ ⟨⟨S, T⟩⟩ a =
(P⇩1 (F t), P⇩0 (F t)) \\ (S a, T a)"
using t tuple_proj [of X F] F.simulation_axioms
pointwise_tuple_def [of S T]
pointwise_tuple_def [of P⇩1oF.map P⇩0oF.map]
apply auto[1]
by metis
also have "... = (P⇩1 (F t) \\⇩A S a, P⇩0 (F t) \\⇩B T a)"
by (simp add: A.con_sym B.con_sym con0 con1 resid_def)
also have "... = (P⇩1oG.map t, P⇩0oG.map t)"
using S.naturality2_ax T.naturality2_ax t by auto
also have "... = G t"
using t tuple_proj G.simulation_axioms pointwise_tuple_def by metis
finally show ?thesis by blast
qed
show "join_of (⟨⟨S, T⟩⟩ a) (F t) (⟨⟨S, T⟩⟩ t)"
proof -
have "A.join_of (S a) (P⇩1oF.map t) (S t)"
using t con1 S.naturality3 by blast
moreover have "B.join_of (T a) (P⇩0oF.map t) (T t)"
using T.naturality3 t by blast
ultimately show ?thesis
unfolding pointwise_tuple_def
by (metis (mono_tags, lifting) A.con_implies_arr(2) P⇩0_def
P⇩1.preserves_reflects_arr P⇩1_def comp_apply con1 fst_conv
join_of_char(1) snd_conv)
qed
qed
show 1: "transformation X (\\) F G ⟨⟨S, T⟩⟩" ..
show 2: "P⇩1 ∘ ⟨⟨S, T⟩⟩ = S" and 3: "P⇩0 ∘ ⟨⟨S, T⟩⟩ = T"
using proj_tuple2 S.transformation_axioms T.transformation_axioms
by blast+
show "∃!ST. transformation X (\\) F G ST ∧ P⇩1 ∘ ST = S ∧ P⇩0 ∘ ST = T"
proof -
have "⋀ST. ⟦transformation X (\\) F G ST; P⇩1 ∘ ST = S; P⇩0 ∘ ST = T⟧
⟹ ST = ⟨⟨S, T⟩⟩"
proof -
fix ST
assume ST: "transformation X resid F G ST"
assume 0: "P⇩0 ∘ ST = T"
assume 1: "P⇩1 ∘ ST = S"
interpret ST: transformation X resid F G ST
using ST by blast
show "ST = ⟨⟨S, T⟩⟩"
proof
fix t
show "ST t = ⟨⟨S, T⟩⟩ t"
unfolding pointwise_tuple_def
using 0 1 ST.preserves_arr ST.extensionality P⇩0_def P⇩1_def
apply auto[1]
by (metis prod.exhaust_sel)
qed
qed
thus ?thesis
using 1 2 3 by metis
qed
qed
lemma proj_joint_monic2:
assumes "transformation X resid F G S" and "transformation X resid F G T"
and "P⇩0 ∘ S = P⇩0 ∘ T" and "P⇩1 ∘ S = P⇩1 ∘ T"
shows "S = T"
using assms transformation_whisker_left [of X resid F G S] universality2(4)
A.weakly_extensional_rts_axioms B.weakly_extensional_rts_axioms
P⇩1.simulation_axioms P⇩0.simulation_axioms
by (metis transformation_def)
lemma join_char:
shows "join t u =
(if joinable t u
then (A.join (fst t) (fst u), B.join (snd t) (snd u))
else null)"
by (metis A.join_is_join_of B.join_is_join_of fst_conv join_is_join_of
join_of_char(1-2) join_of_unique joinable_iff_join_not_null snd_conv)
lemma join_simp:
assumes "joinable t u"
shows "join t u = (A.join (fst t) (fst u), B.join (snd t) (snd u))"
using assms join_char by auto
end
lemma simulation_tuple [intro]:
assumes "simulation X A H" and "simulation X B K"
and "Y = A ⨂ B"
shows "simulation X Y ⟨⟨H, K⟩⟩"
using assms product_rts.universality(1) [of A B X H K]
by (simp add: product_rts.intro simulation_def)
lemma simulation_product [intro]:
assumes "simulation A B H" and "simulation C D K"
and "X = A ⨂ C" and "Y = B ⨂ D"
shows "simulation X Y (product_simulation.map A C H K)"
using assms
by (meson product_rts_def product_rts_def product_simulation.intro
product_simulation.is_simulation simulation_def simulation_def)
lemma comp_pointwise_tuple:
shows "⟨⟨H, K⟩⟩ ∘ L = ⟨⟨H ∘ L, K ∘ L⟩⟩"
unfolding pointwise_tuple_def
by auto
lemma comp_product_simulation_tuple2:
assumes "simulation A A' F" and "simulation B B' G"
and "transformation X A H⇩0 H⇩1 H" and "transformation X B K⇩0 K⇩1 K"
shows "product_simulation.map A B F G ∘ ⟨⟨H, K⟩⟩ = ⟨⟨F ∘ H, G ∘ K⟩⟩"
proof -
interpret X: rts X
using assms(3) transformation.axioms(1) by blast
interpret A: rts A
using assms(1) simulation.axioms(1) by blast
interpret B: rts B
using assms(2) simulation.axioms(1) by blast
interpret A': rts A'
using assms(1) simulation.axioms(2) by blast
interpret B': rts B'
using assms(2) simulation.axioms(2) by blast
interpret AxB: product_rts A B ..
interpret A'xB': product_rts A' B' ..
interpret F: simulation A A' F
using assms by blast
interpret G: simulation B B' G
using assms by blast
interpret FxG: product_simulation A B A' B' F G ..
interpret H: transformation X A H⇩0 H⇩1 H
using assms(3) by blast
interpret K: transformation X B K⇩0 K⇩1 K
using assms(4) by blast
show ?thesis
proof
fix x
show "(FxG.map ∘ ⟨⟨H, K⟩⟩) x = ⟨⟨F ∘ H, G ∘ K⟩⟩ x"
using FxG.extensionality pointwise_tuple_def F.extensionality G.extensionality
H.extensionality K.extensionality H.preserves_arr K.preserves_arr
by (cases "X.arr x") (auto simp add: pointwise_tuple_def)
qed
qed
lemma comp_product_simulation_tuple:
assumes "simulation A A' F" and "simulation B B' G"
and "simulation X A H" and "simulation X B K"
shows "product_simulation.map A B F G ∘ ⟨⟨H, K⟩⟩ = ⟨⟨F ∘ H, G ∘ K⟩⟩"
proof -
interpret X: rts X
using assms(3) simulation.axioms(1) by blast
interpret A: rts A
using assms(1) simulation.axioms(1) by blast
interpret B: rts B
using assms(2) simulation.axioms(1) by blast
interpret A': rts A'
using assms(1) simulation.axioms(2) by blast
interpret B': rts B'
using assms(2) simulation.axioms(2) by blast
interpret AxB: product_rts A B ..
interpret A'xB': product_rts A' B' ..
interpret F: simulation A A' F
using assms by blast
interpret G: simulation B B' G
using assms by blast
interpret FxG: product_simulation A B A' B' F G ..
interpret H: simulation X A H
using assms(3) by blast
interpret K: simulation X B K
using assms(4) by blast
show ?thesis
proof
fix x
show "(FxG.map ∘ ⟨⟨H, K⟩⟩) x = ⟨⟨F ∘ H, G ∘ K⟩⟩ x"
using FxG.extensionality pointwise_tuple_def F.extensionality G.extensionality
H.extensionality K.extensionality H.preserves_reflects_arr
K.preserves_reflects_arr
by (cases "X.arr x") (auto simp add: pointwise_tuple_def)
qed
qed
locale product_transformation =
A1: rts A1 +
A0: rts A0 +
B1: extensional_rts B1 +
B0: extensional_rts B0 +
A1xA0: product_rts A1 A0 +
B1xB0: product_rts B1 B0 +
F1: simulation A1 B1 F1 +
F0: simulation A0 B0 F0 +
G1: simulation A1 B1 G1 +
G0: simulation A0 B0 G0 +
T1: transformation A1 B1 F1 G1 T1 +
T0: transformation A0 B0 F0 G0 T0
for A1 :: "'a1 resid" (infix ‹\⇩A⇩1› 70)
and A0 :: "'a0 resid" (infix ‹\⇩A⇩0› 70)
and B1 :: "'b1 resid" (infix ‹\⇩B⇩1› 70)
and B0 :: "'b0 resid" (infix ‹\⇩B⇩0› 70)
and F1 :: "'a1 ⇒ 'b1"
and F0 :: "'a0 ⇒ 'b0"
and G1 :: "'a1 ⇒ 'b1"
and G0 :: "'a0 ⇒ 'b0"
and T1 :: "'a1 ⇒ 'b1"
and T0 :: "'a0 ⇒ 'b0"
begin
sublocale F1: simulation_to_weakly_extensional_rts A1 B1 F1 ..
sublocale F0: simulation_to_weakly_extensional_rts A0 B0 F0 ..
sublocale G1: simulation_to_weakly_extensional_rts A1 B1 G1 ..
sublocale G0: simulation_to_weakly_extensional_rts A0 B0 G0 ..
sublocale A1xA0: product_rts A1 A0 ..
sublocale B1xB0: product_of_extensional_rts B1 B0 ..
sublocale F1xF0: product_simulation A1 A0 B1 B0 F1 F0 ..
sublocale G1xG0: product_simulation A1 A0 B1 B0 G1 G0 ..
abbreviation (input) map⇩0 :: "'a1 × 'a0 ⇒ 'b1 × 'b0"
where "map⇩0 ≡ (λa. (T1 (fst a), T0 (snd a)))"
sublocale TC: transformation_by_components
A1xA0.resid B1xB0.resid F1xF0.map G1xG0.map map⇩0
proof
show "⋀a. A1xA0.ide a ⟹ B1xB0.src (map⇩0 a) = F1xF0.map a"
unfolding F1xF0.map_def
using T1.preserves_arr T0.preserves_arr T1.preserves_src T0.preserves_src
B1xB0.src_char
by auto
show "⋀a. A1xA0.ide a ⟹ B1xB0.trg (map⇩0 a) = G1xG0.map a"
unfolding G1xG0.map_def
using T1.preserves_arr T0.preserves_arr T1.preserves_trg T0.preserves_trg
B1xB0.trg_char
by auto
show "⋀a a'. ⟦A1xA0.ide a; A1xA0.cong a a'⟧
⟹ (T1 (fst a), T0 (snd a)) = (T1 (fst a'), T0 (snd a'))"
using A1xA0.cong_char T0.respects_cong_ide T1.respects_cong_ide by auto
fix a t
assume t: "a ∈ A1xA0.sources t"
show "B1xB0.resid (map⇩0 a) (F1xF0.map t) = map⇩0 (A1xA0.resid a t)"
proof -
have "B1xB0.resid (map⇩0 a) (F1xF0.map t) =
(T1 (fst a) \\⇩B⇩1 F1 (fst t), T0 (snd a) \\⇩B⇩0 F0 (snd t))"
using t F1xF0.map_def B1xB0.resid_def
apply simp
by (meson A1xA0.arr_char A1xA0.con_char A1xA0.con_implies_arr(1)
A1xA0.in_sourcesE A1xA0.prfx_implies_con A1xA0.source_is_prfx
T0.preserves_con(2) T1.preserves_con(2))
also have "... = map⇩0 (A1xA0.resid a t)"
unfolding A1xA0.resid_def
using t A0.prfx_implies_con A1.prfx_implies_con A1xA0.prfx_char
A1xA0.source_is_prfx T0.naturality1_ax T1.naturality1_ax
by auto
finally show ?thesis by blast
qed
show "B1xB0.resid (F1xF0.map t) (map⇩0 a) =
G1xG0.map t"
using t F1xF0.map_def G1xG0.map_def B1xB0.resid_def
apply simp
by (metis (no_types, opaque_lifting) A0.in_sourcesI A0.not_arr_null
A1.in_sourcesI A1.not_arr_null A1xA0.con_char A1xA0.ide_char
A1xA0.in_sourcesE B0.arr_resid_iff_con B0.not_con_null(1)
B1.arr_resid_iff_con F0.extensionality G0.extensionality
G0.preserves_reflects_arr G1.extensionality G1.preserves_reflects_arr
T0.naturality2_ax T1.naturality2_ax)
show "B1xB0.joinable (map⇩0 a) (F1xF0.map t)"
using t F1xF0.map_def T1.naturality3 T0.naturality3
apply simp
by (metis (no_types, opaque_lifting) A0.con_implies_arr(1) A0.in_sourcesI
A1.con_implies_arr(1) A1.in_sourcesI A1xA0.con_char A1xA0.ide_char
A1xA0.in_sourcesE B0.joinable_def B1.joinable_def B1xB0.join_of_char(2)
fst_conv snd_conv)
qed
definition map :: "'a1 × 'a0 ⇒ 'b1 × 'b0"
where "map ≡ TC.map"
sublocale transformation
A1xA0.resid B1xB0.resid F1xF0.map G1xG0.map map
unfolding map_def ..
lemma is_transformation:
shows "transformation A1xA0.resid B1xB0.resid F1xF0.map G1xG0.map map"
..
lemma map_simp:
shows "map t = B1xB0.join (map⇩0 (A1xA0.src t)) (F1xF0.map t)"
unfolding map_def TC.map_def by blast
lemma map_simp_ide:
assumes "A1xA0.ide t"
shows "map t = map⇩0 (A1xA0.src t)"
unfolding map_def
using A1xA0.src_cong_ide TC.map_simp_ide TC.respects_cong_ide assms
by presburger
end
lemma comp_product_transformation_tuple:
assumes "transformation_to_extensional_rts A1 B1 F1 G1 T1"
and "transformation_to_extensional_rts A0 B0 F0 G0 T0"
and "simulation X A1 H1" and "simulation X A0 H0"
shows "product_transformation.map A1 A0 B1 B0 F1 F0 T1 T0 ∘ ⟨⟨H1, H0⟩⟩ =
⟨⟨T1 ∘ H1, T0 ∘ H0⟩⟩"
proof -
interpret X: rts X
using assms(3) simulation.axioms(1) by blast
interpret A1: rts A1
using assms(1) transformation_to_extensional_rts.axioms(1)
transformation.axioms(1)
by blast
interpret A0: rts A0
using assms(2) transformation_to_extensional_rts.axioms(1)
transformation.axioms(1)
by blast
interpret B1: extensional_rts B1
using assms(1) transformation_to_extensional_rts.axioms(2) by blast
interpret B0: extensional_rts B0
using assms(2) transformation_to_extensional_rts.axioms(2) by blast
interpret F1: simulation A1 B1 F1
using assms(1) transformation_to_extensional_rts.axioms(1)
transformation.axioms(3) simulation.axioms(3)
by blast
interpret F0: simulation A0 B0 F0
using assms(2) transformation_to_extensional_rts.axioms(1)
transformation.axioms(3) simulation.axioms(3)
by blast
interpret G1: simulation A1 B1 G1
using assms(1) transformation_to_extensional_rts.axioms(1)
transformation.axioms(4) simulation.axioms(3)
by blast
interpret G0: simulation A0 B0 G0
using assms(2) transformation_to_extensional_rts.axioms(1)
transformation.axioms(4) simulation.axioms(3)
by blast
interpret T1: transformation_to_extensional_rts A1 B1 F1 G1 T1
using assms(1) by blast
interpret T0: transformation_to_extensional_rts A0 B0 F0 G0 T0
using assms(2) by blast
interpret A1xA0: product_rts A1 A0 ..
interpret B1xB0: product_of_extensional_rts B1 B0 ..
interpret F1xF0: product_simulation A1 A0 B1 B0 F1 F0 ..
interpret G1xG0: product_simulation A1 A0 B1 B0 G1 G0 ..
interpret T1xT0: product_transformation A1 A0 B1 B0 F1 F0 G1 G0 T1 T0
..
interpret H1: simulation X A1 H1
using assms(3) by blast
interpret H0: simulation X A0 H0
using assms(4) by blast
show ?thesis
proof
fix x
show "(T1xT0.map ∘ ⟨⟨H1, H0⟩⟩) x = ⟨⟨T1 ∘ H1, T0 ∘ H0⟩⟩ x"
proof -
have "X.arr x ⟹
B1xB0.join
(T1 (fst (A1xA0.src (H1 x, H0 x))),
T0 (snd (A1xA0.src (H1 x, H0 x))))
(F1 (H1 x), F0 (H0 x)) =
(T1 (H1 x), T0 (H0 x))"
proof -
assume x: "X.arr x"
have "B1xB0.join
(T1 (fst (A1xA0.src (H1 x, H0 x))),
T0 (snd (A1xA0.src (H1 x, H0 x))))
(F1 (H1 x), F0 (H0 x)) =
B1xB0.join
(T1 (A1.src (H1 x)), T0 (A0.src (H0 x)))
(F1 (H1 x), F0 (H0 x))"
by (metis A0.src_congI A1.src_congI A1xA0.arr_char A1xA0.con_arr_src(2)
A1xA0.con_char A1xA0.ide_char A1xA0.ide_src H0.preserves_reflects_arr
H1.preserves_reflects_arr T0.respects_cong_ide T1.respects_cong_ide
fst_conv snd_conv x)
also have "... = (T1 (H1 x), T0 (H0 x))"
using x B1xB0.join_char
by (simp add: B1xB0.join_of_char(2) T0.naturality3'⇩E(1-2)
T1.naturality3'⇩E(1-2))
finally show ?thesis by blast
qed
thus ?thesis
using pointwise_tuple_def H1.extensionality H0.extensionality
T1.extensionality T0.extensionality T1xT0.extensionality T1xT0.map_def
T1xT0.TC.map_def comp_product_simulation_tuple
F1xF0.product_simulation_axioms G1xG0.product_simulation_axioms
by (cases "X.arr x") (auto simp add: pointwise_tuple_def)
qed
qed
qed
lemma simulation_interchange:
assumes "simulation A A' F" and "simulation B B' G"
and "simulation A' A'' F'" and "simulation B' B'' G'"
shows "product_simulation.map A B (F' ∘ F) (G' ∘ G) =
product_simulation.map A' B' F' G' ∘ product_simulation.map A B F G"
proof -
interpret F: simulation A A' F
using assms(1) by blast
interpret G: simulation B B' G
using assms(2) by blast
interpret F': simulation A' A'' F'
using assms(3) by blast
interpret G': simulation B' B'' G'
using assms(4) by blast
interpret F'oF: composite_simulation A A' A'' F F' ..
interpret G'oG: composite_simulation B B' B'' G G' ..
interpret FxG: product_simulation A B A' B' F G ..
interpret F'xG': product_simulation A' B' A'' B'' F' G' ..
interpret F'oFxG'oG: product_simulation A B A'' B'' ‹F' ∘ F› ‹G' ∘ G› ..
show "F'oFxG'oG.map = F'xG'.map ∘ FxG.map"
unfolding F'oFxG'oG.map_def FxG.map_def F'xG'.map_def
using F.extensionality G.extensionality F'.extensionality G'.extensionality by auto
qed
subsection "Associators"
text ‹
For any RTS's ‹A›, ‹B›, and ‹C›, there exists an invertible ``associator'' simulation
from the product RTS ‹(A × B) × C)› to the product RTS ‹A × (B × C)›.
›
locale ASSOC =
A: rts A +
B: rts B +
C: rts C
for A :: "'a resid"
and B :: "'b resid"
and C :: "'c resid"
begin
sublocale AxB: product_rts A B ..
sublocale BxC: product_rts B C ..
sublocale AxB_xC: product_rts AxB.resid C ..
sublocale Ax_BxC: product_rts A BxC.resid ..
text ‹
The following definition is expressed in a form that makes it evident that it
defines a simulation.
›
definition map :: "('a × 'b) × 'c ⇒ 'a × 'b × 'c"
where "map ≡ Ax_BxC.tuple
(AxB.P⇩1 ∘ AxB_xC.P⇩1)
(BxC.tuple (AxB.P⇩0 ∘ AxB_xC.P⇩1) AxB_xC.P⇩0)"
sublocale simulation AxB_xC.resid Ax_BxC.resid map
unfolding map_def
using AxB.P⇩0.simulation_axioms AxB.P⇩1.simulation_axioms
AxB_xC.P⇩0.simulation_axioms AxB_xC.P⇩1.simulation_axioms
by (intro simulation_tuple simulation_comp) auto
lemma is_simulation:
shows "simulation AxB_xC.resid Ax_BxC.resid map"
..
text ‹
The following explicit formula is more convenient for calculations.
›
lemma map_eq:
shows "map = (λx. if AxB_xC.arr x
then (fst (fst x), (snd (fst x), snd x))
else Ax_BxC.null)"
unfolding map_def pointwise_tuple_def AxB.P⇩0_def AxB.P⇩1_def
AxB_xC.P⇩0_def AxB_xC.P⇩1_def
by auto
definition map' :: "'a × 'b × 'c ⇒ ('a × 'b) × 'c"
where "map' ≡ AxB_xC.tuple
(AxB.tuple Ax_BxC.P⇩1 (BxC.P⇩1 ∘ Ax_BxC.P⇩0))
(BxC.P⇩0 ∘ Ax_BxC.P⇩0)"
sublocale inv: simulation Ax_BxC.resid AxB_xC.resid map'
unfolding map'_def
using BxC.P⇩0.simulation_axioms BxC.P⇩1.simulation_axioms
Ax_BxC.P⇩0.simulation_axioms Ax_BxC.P⇩1.simulation_axioms
by (intro simulation_tuple simulation_comp) auto
lemma inv_is_simulation:
shows "simulation Ax_BxC.resid AxB_xC.resid map'"
..
lemma map'_eq:
shows "map' =
(λx. if Ax_BxC.arr x
then ((fst x, fst (snd x)), snd (snd x))
else AxB_xC.null)"
unfolding map'_def pointwise_tuple_def BxC.P⇩0_def BxC.P⇩1_def
Ax_BxC.P⇩0_def Ax_BxC.P⇩1_def
by auto
lemma inverse_simulations_map'_map:
shows "inverse_simulations AxB_xC.resid Ax_BxC.resid map' map"
proof
show "map ∘ map' = Id Ax_BxC.resid"
unfolding map_eq map'_eq by auto
show "map' ∘ map = Id AxB_xC.resid"
unfolding map_eq map'_eq by auto
qed
end
section "Sum RTS"
locale sum_rts =
A: rts A +
B: rts B
for A :: "'a resid" (infix ‹\⇩A› 70)
and B :: "'b resid" (infix ‹\⇩B› 70)
begin
notation A.con (infix ‹⌢⇩A› 50)
notation A.prfx (infix ‹≲⇩A› 50)
notation A.cong (infix ‹∼⇩A› 50)
notation B.con (infix ‹⌢⇩B› 50)
notation B.prfx (infix ‹≲⇩B› 50)
notation B.cong (infix ‹∼⇩B› 50)