Theory RTSCat
section "The Category of RTS's and Simulations"
text‹
In this section, we show that the subcategory of ‹❙R❙T❙S⇧†›, comprised of the arrows that are
identities with respect to the residuation, is also cartesian closed. In informal text,
we will refer to this category as ‹❙R❙T❙S›. In a later section, we will show that the entire
structure of the RTS-category ‹❙R❙T❙S⇧†› is already determined by the ordinary subcategory ‹❙R❙T❙S›.
›
theory RTSCat
imports Main RTSCatx EnrichedCategoryBasics.CartesianClosedMonoidalCategory
begin
locale rtscat =
universe arr_type
for arr_type :: "'A itself"
begin
sublocale One: one_arr_rts arr_type ..
interpretation RTSx: rtscatx arr_type ..
interpretation RTSx: elementary_category_with_binary_products
RTSx.hcomp RTSx.p⇩0 RTSx.p⇩1
using RTSx.extends_to_elementary_category_with_binary_products by blast
interpretation RTS⇩S: subcategory RTSx.hcomp RTSx.sta
using RTSx.dom.preserves_ide RTSx.cod.preserves_ide RTSx.sta_hcomp
RTSx.arr_hcomp RTSx.H.seqI
by unfold_locales auto
type_synonym 'a arr = "'a rtscatx.arr"
definition comp :: "'A arr comp" (infixr "⋅" 53)
where "comp ≡ subcategory.comp RTSx.hcomp RTSx.sta"
sublocale category comp
unfolding comp_def
using RTS⇩S.is_category by blast
notation in_hom ("«_ : _ → _»")
lemma ide_iff_RTS_obj:
shows "ide a ⟷ RTSx.obj a"
using RTSx.obj_is_sta RTS⇩S.ideI⇩S⇩b⇩C RTS⇩S.ide_char⇩S⇩b⇩C comp_def by auto
lemma arr_iff_RTS_sta:
shows "arr f ⟷ RTSx.sta f"
by (simp add: RTS⇩S.arr_char⇩S⇩b⇩C comp_def)
text‹
We want @{locale rtscat} to stand on its own, so here we embark on an
extended development designed to bootstrap away from dependence on the
supporting locale @{locale rtscatx}.
›
abbreviation Obj
where "Obj A ≡ extensional_rts A ∧ small_rts A"
definition mkide :: "'A resid ⇒ 'A arr"
where "mkide ≡ RTSx.mkobj"
definition mkarr :: "'A resid ⇒ 'A resid ⇒ ('A ⇒ 'A) ⇒ 'A arr"
where "mkarr ≡ RTSx.mksta"
definition Rts :: "'A arr ⇒ 'A resid"
where "Rts ≡ RTSx.Dom"
abbreviation Dom :: "'A arr ⇒ 'A resid"
where "Dom t ≡ Rts (dom t)"
abbreviation Cod :: "'A arr ⇒ 'A resid"
where "Cod t ≡ Rts (cod t)"
definition Map :: "'A arr ⇒ 'A ⇒ 'A"
where "Map ≡ RTSx.Map"
lemma ideD⇩R⇩T⇩S⇩C [intro, simp]:
assumes "ide a"
shows "Obj (Rts a)"
using assms Rts_def RTS⇩S.arr_char⇩S⇩b⇩C ideD(1) comp_def by auto
lemma ide_mkide [intro, simp]:
assumes "Obj A"
shows "ide (mkide A)"
using assms comp_def mkide_def RTSx.obj_implies_sta RTSx.obj_mkobj
RTS⇩S.ideI⇩S⇩b⇩C
by simp
lemma Rts_mkide [simp]:
shows "Rts (mkide A) = A"
by (simp add: Rts_def mkide_def)
lemma mkide_Rts [simp]:
assumes "ide a"
shows "mkide (Rts a) = a"
using assms RTSx.bij_mkobj(4) Rts_def ide_iff_RTS_obj mkide_def
by force
lemma Dom_mkide [simp]:
assumes "ide (mkide A)"
shows "Dom (mkide A) = A"
using assms by force
lemma Cod_mkide [simp]:
assumes "ide (mkide A)"
shows "Cod (mkide A) = A"
using assms by force
lemma Map_mkide [simp]:
assumes "ide (mkide A)"
shows "Map (mkide A) = I A"
using assms mkide_def RTSx.mkobj_def Map_def RTSx.bij_mksta(3)
RTSx.mkarr_def Rts_def ideD⇩R⇩T⇩S⇩C
by fastforce
lemma bij_mkide:
shows "mkide ∈ Collect Obj → Collect ide"
and "Rts ∈ Collect ide → Collect Obj"
and "Rts (mkide A) = A"
and "ide a ⟹ mkide (Rts a) = a"
and "bij_betw mkide (Collect Obj) (Collect ide)"
and "bij_betw Rts (Collect ide) (Collect Obj)"
proof -
show "mkide ∈ Collect Obj → Collect ide" by simp
show "Rts ∈ Collect ide → Collect Obj" by simp
show "Rts (mkide A) = A" by simp
show "ide a ⟹ mkide (Rts a) = a" by simp
show "bij_betw mkide (Collect Obj) (Collect ide)"
unfolding bij_betw_def
apply auto[1]
apply (metis RTSx.mkobj_simps(1) inj_on_inverseI mkide_def)
by (metis (no_types, lifting) CollectI ideD⇩R⇩T⇩S⇩C image_eqI mkide_Rts)
show "bij_betw Rts (Collect ide) (Collect Obj)"
unfolding bij_betw_def
apply auto[1]
apply (metis CollectD inj_onI mkide_Rts)
using image_iff by fastforce
qed
lemma arrD:
assumes "arr f"
shows "Obj (Rts (dom f))" and "Obj (Rts (cod f))"
and "simulation (Rts (dom f)) (Rts (cod f)) (Map f)"
proof -
interpret A: extensional_rts ‹Rts (dom f)›
by (simp add: assms)
interpret A: small_rts ‹Rts (dom f)›
by (simp add: assms)
interpret B: extensional_rts ‹Rts (cod f)›
by (simp add: assms)
interpret B: small_rts ‹Rts (cod f)›
by (simp add: assms)
interpret AB: exponential_rts ‹Rts (dom f)› ‹Rts (cod f)› ..
have 1: "mkarr (Rts (dom f)) (Rts (cod f)) (Map f) = f"
using assms comp_def mkarr_def Rts_def RTSx.mkarr_def
by (metis (no_types, lifting) Map_def RTSx.Dom_cod RTSx.Dom_dom
RTSx.Map_simps(4) RTSx.V.ide_implies_arr RTSx.V.trg_ide
RTSx.trg_simp RTS⇩S.cod_char⇩S⇩b⇩C RTS⇩S.dom_char⇩S⇩b⇩C arr_iff_RTS_sta)
show "Obj (Rts (dom f))"
using A.extensional_rts_axioms A.small_rts_axioms by simp
show "Obj (Rts (cod f))"
using B.extensional_rts_axioms B.small_rts_axioms by simp
show "simulation (Rts (dom f)) (Rts (cod f)) (Map f)"
using assms 1 RTSx.sta_char RTSx.simulation_Map_sta
RTS⇩S.arr_char⇩S⇩b⇩C RTS⇩S.cod_simp RTS⇩S.dom_simp comp_def
by (simp add: Map_def Rts_def)
qed
lemma arr_mkarr [intro, simp]:
assumes "Obj A" and "Obj B" and "simulation A B F"
shows "arr (mkarr A B F)"
unfolding mkarr_def comp_def
using assms RTS⇩S.arr_char⇩S⇩b⇩C by blast
lemma arrI⇩R⇩T⇩S⇩C:
assumes "f ∈ mkarr A B ` Collect (simulation A B)"
and "Obj A" and "Obj B"
shows "arr f"
using assms arr_mkarr by blast
lemma Dom_mkarr [simp]:
assumes "arr (mkarr A B F)"
shows "Dom (mkarr A B F) = A"
using assms
by (simp add: RTS⇩S.arrE RTS⇩S.dom_simp Rts_def comp_def mkarr_def)
lemma Cod_mkarr [simp]:
assumes "arr (mkarr A B F)"
shows "Cod (mkarr A B F) = B"
using assms
by (simp add: RTS⇩S.arrE RTS⇩S.cod_simp Rts_def comp_def mkarr_def)
lemma Map_mkarr [simp]:
assumes "arr (mkarr A B F)"
shows "Map (mkarr A B F) = F"
using assms mkarr_def RTSx.mkarr_def
by (metis Cod_mkarr Dom_mkarr Map_def RTSx.bij_mksta(3) arrD(1-2))
lemma mkarr_Map [simp]:
assumes "Obj A" and "Obj B" and "t ∈ {t. «t : mkide A → mkide B»}"
shows "mkarr A B (Map t) = t"
using assms mkarr_def Map_def comp_def mkide_def
by (metis (no_types, lifting) RTS⇩S.arrE RTS⇩S.in_hom_char⇩S⇩b⇩C
RTSx.bij_mksta(4) mem_Collect_eq)
lemma dom_mkarr [simp]:
assumes "arr (mkarr A B F)"
shows "dom (mkarr A B F) = mkide A"
using assms
by (metis Dom_mkarr ide_dom mkide_Rts)
lemma cod_mkarr [simp]:
assumes "arr (mkarr A B F)"
shows "cod (mkarr A B F) = mkide B"
using assms
by (metis Cod_mkarr ide_cod mkide_Rts)
lemma mkarr_in_hom [intro]:
assumes "simulation A B F" and "Rts a = A" and "Rts b = B"
and "ide a" and "ide b"
shows "«mkarr A B F : a → b»"
using assms by auto
lemma bij_mkarr:
assumes "Obj A" and "Obj B"
shows "mkarr A B ∈ Collect (simulation A B)
→ {t. «t : mkide A → mkide B»}"
and "Map ∈ {t. «t : mkide A → mkide B»} → Collect (simulation A B)"
and "Map (mkarr A B F) = F"
and "t ∈ {t. «t : mkide A → mkide B»} ⟹ mkarr A B (Map t) = t"
and "bij_betw (mkarr A B) (Collect (simulation A B))
{t. «t : mkide A → mkide B»}"
and "bij_betw Map {t. «t : mkide A → mkide B»}
(Collect (simulation A B))"
proof -
show 1: "mkarr A B ∈ Collect (simulation A B) → hom (mkide A) (mkide B)"
by (simp add: assms in_homI)
show 2: "Map ∈ {t. «t : mkide A → mkide B»} → Collect (simulation A B)"
using arrD(3) by fastforce
show 3: "Map (mkarr A B F) = F"
using assms
by (metis Map_def RTSx.bij_mksta(3) mkarr_def)
show 4: "t ∈ {t. «t : mkide A → mkide B»} ⟹ mkarr A B (Map t) = t"
using assms by auto
show "bij_betw (mkarr A B) (Collect (simulation A B))
{t. «t : mkide A → mkide B»}"
using assms 1 2 3 4 by (intro bij_betwI) auto
show "bij_betw Map {t. «t : mkide A → mkide B»} (Collect (simulation A B))"
using assms 1 2 3 4 by (intro bij_betwI) auto
qed
lemma arr_eqI:
assumes "par f g" and "Map f = Map g"
shows "f = g"
proof (intro RTSx.arr_eqI)
show "f ≠ RTSx.Null"
using assms RTS⇩S.null_char RTSx.null_char not_arr_null comp_def by force
show "g ≠ RTSx.Null"
using assms RTS⇩S.null_char RTSx.null_char not_arr_null comp_def by force
show 1: "RTSx.Dom f = RTSx.Dom g"
using assms comp_def
by (metis RTSx.Dom_dom RTSx.V.ide_implies_arr RTS⇩S.arrE RTS⇩S.dom_simp)
show 2: "RTSx.Cod f = RTSx.Cod g"
using assms comp_def
by (metis RTSx.Dom_cod RTSx.V.ide_implies_arr RTS⇩S.arrE RTS⇩S.cod_char⇩S⇩b⇩C)
interpret A: extensional_rts ‹RTSx.Dom f›
using assms RTS⇩S.arrE comp_def by auto
interpret B: extensional_rts ‹RTSx.Cod f›
using assms RTS⇩S.arrE comp_def by auto
interpret AB: exponential_rts ‹RTSx.Dom f› ‹RTSx.Cod f› ..
show "RTSx.Trn f = RTSx.Trn g"
using assms 1 2 comp_def Map_def
by (metis (no_types, lifting) AB.ide_implies_arr RTSx.Map_simps(4)
RTSx.V.trg_ide RTSx.arr_char RTSx.sta_char RTSx.trg_simp
RTS⇩S.arr_char⇩S⇩b⇩C)
qed
lemma Map_ide:
assumes "ide a"
shows "Map a = I (Rts a)"
using assms Map_mkide [of "Rts a"] by simp
lemma Map_comp:
assumes "seq g f"
shows "Map (g ⋅ f) = Map g ∘ Map f"
using assms Map_def comp_def RTSx.Map_hcomp RTS⇩S.arr_char⇩S⇩b⇩C RTS⇩S.comp_def
by auto
lemma comp_mkarr:
assumes "arr (mkarr A B F)" and "arr (mkarr B C G)"
shows "mkarr B C G ⋅ mkarr A B F = mkarr A C (G ∘ F)"
proof (intro arr_eqI)
have 1: "arr (mkarr A C (G ∘ F))"
using assms arrD simulation_comp bij_mkarr(3) Cod_mkarr Dom_mkarr
arr_mkarr
by metis
show "par (mkarr B C G ⋅ mkarr A B F) (mkarr A C (G ∘ F))"
using assms 1 by auto
show "Map (mkarr B C G ⋅ mkarr A B F) = Map (mkarr A C (G ∘ F))"
using assms 1 Map_comp Map_mkarr by auto
qed
lemma iso_char:
shows "iso t ⟷ arr t ∧ invertible_simulation (Dom t) (Cod t) (Map t)"
using Map_def comp_def Rts_def RTSx.iso_char RTSx.iso_implies_sta
by (metis (no_types, lifting) RTSx.Dom_cod RTSx.Dom_dom
RTSx.H.iso_inv_iso RTSx.Map_simps(3-4)
RTSx.V.ide_iff_src_self RTSx.V.ide_implies_arr RTSx.V.trg_ide
RTS⇩S.arr_char⇩S⇩b⇩C RTS⇩S.cod_simp RTS⇩S.dom_char⇩S⇩b⇩C RTS⇩S.iso_char⇩S⇩b⇩C)
lemma isomorphic_char:
shows "isomorphic a b ⟷
ide a ∧ ide b ∧ (∃F. invertible_simulation (Rts a) (Rts b) F)"
proof
show "isomorphic a b ⟹
ide a ∧ ide b ∧ (∃F. invertible_simulation (Rts a) (Rts b) F)"
by (metis (no_types, lifting) ide_cod ide_dom in_homE iso_char
isomorphicE)
show "ide a ∧ ide b ∧ (∃F. invertible_simulation (Rts a) (Rts b) F)
⟹ isomorphic a b"
by (metis arr_mkarr cod_mkarr dom_mkarr ideD⇩R⇩T⇩S⇩C isomorphic_def
iso_char invertible_simulation.axioms(1) mkarr_in_hom mkide_Rts
Map_mkarr)
qed
subsection "Terminal Object"
definition one ("❙𝟭")
where "one ≡ RTSx.one"
no_notation RTSx.one ("❙𝟭")
definition trm
where "trm ≡ RTSx.trm"
lemma Rts_one [simp]:
shows "Rts ❙𝟭 = One.resid"
unfolding one_def Rts_def RTSx.one_def by simp
lemma mkide_One [simp]:
shows "mkide One.resid = ❙𝟭"
unfolding one_def mkide_def RTSx.one_def by simp
sublocale elementary_category_with_terminal_object comp one trm
proof
show "ide ❙𝟭"
unfolding one_def
using RTSx.obj_one RTSx.obj_is_sta RTS⇩S.ideI⇩S⇩b⇩C comp_def by force
show "⋀a. ide a ⟹ «trm a : a → ❙𝟭»"
using RTS⇩S.arr_char⇩S⇩b⇩C RTS⇩S.ide_char⇩S⇩b⇩C RTS⇩S.in_hom_char⇩S⇩b⇩C comp_def
by (metis (no_types, lifting) RTSx.trm_in_hom RTSx.trm_simps'(6)
‹ide ❙𝟭› one_def trm_def)
show "⋀a f. ⟦ide a; «f : a → ❙𝟭»⟧ ⟹ f = trm a"
by (metis RTSx.trm_eqI RTS⇩S.ide_char⇩S⇩b⇩C RTS⇩S.in_hom_char⇩S⇩b⇩C comp_def
one_def trm_def)
qed
lemma Map_trm:
assumes "ide a"
shows "Map (trm a) = constant_simulation.map (Rts a) One.resid One.the_arr"
unfolding Map_def trm_def Rts_def
using assms RTSx.Map_trm RTS⇩S.ide_char⇩S⇩b⇩C comp_def by fastforce
lemma terminal_char:
shows "terminal x ⟷ ide x ∧ (∃!t. residuation.arr (Rts x) t)"
proof -
have "⋀x. terminal x ⟷ RTSx.H.terminal x"
proof -
fix x
have 1: "terminal x ⟷ isomorphic x one"
using terminal_one terminal_objs_isomorphic
by (meson isomorphic_symmetric isomorphic_to_terminal_is_terminal)
also have "... ⟷ RTSx.obj x ∧ isomorphic_rts (RTSx.Dom x) One.resid"
using Rts_one ide_one isomorphic_char Rts_def ide_iff_RTS_obj
isomorphic_rts_def [of "Rts x" One.resid]
invertible_simulation_def' [of "Rts x" "Rts ❙𝟭"]
by auto
also have "... ⟷ RTSx.H.terminal x"
by (metis (mono_tags, lifting) 1 RTS⇩S.arrI⇩S⇩b⇩C RTS⇩S.in_hom_char⇩S⇩b⇩C
RTS⇩S.iso_char⇩S⇩b⇩C RTS⇩S.isomorphic_def RTSx.H.iso_inv_iso
RTSx.H.isomorphic_def RTSx.H.isomorphic_symmetric
RTSx.H.isomorphic_to_terminal_is_terminal RTSx.H.terminal_def
RTSx.iso_implies_sta RTSx.obj_implies_sta RTSx.terminal_one
calculation comp_def one_def RTSx.H.terminal_objs_isomorphic)
finally show "terminal x ⟷ RTSx.H.terminal x" by blast
qed
thus ?thesis
using RTSx.terminal_char Rts_def ide_iff_RTS_obj by presburger
qed
subsection "Products"
definition p⇩0 :: "'A arr ⇒ 'A arr ⇒ 'A arr"
where "p⇩0 ≡ RTSx.p⇩0"
definition p⇩1 :: "'A arr ⇒ 'A arr ⇒ 'A arr"
where "p⇩1 ≡ RTSx.p⇩1"
no_notation RTSx.p⇩0 ("𝔭⇩0[_, _]")
no_notation RTSx.p⇩1 ("𝔭⇩1[_, _]")
notation p⇩0 ("𝔭⇩0[_, _]")
notation p⇩1 ("𝔭⇩1[_, _]")
sublocale elementary_cartesian_category comp p⇩0 p⇩1 one trm
proof
fix a b
assume a: "ide a" and b: "ide b"
show 1: "span 𝔭⇩1[a, b] 𝔭⇩0[a, b]"
using a b RTSx.sta_p⇩0 RTSx.sta_p⇩1 RTS⇩S.arr_char⇩S⇩b⇩C RTS⇩S.dom_simp
RTS⇩S.ide_char⇩S⇩b⇩C
by (simp add: comp_def p⇩0_def p⇩1_def)
show "cod 𝔭⇩0[a, b] = b"
using a b 1 RTS⇩S.cod_simp RTSx.cod_pr0 ide_iff_RTS_obj comp_def
p⇩0_def
by metis
show "cod 𝔭⇩1[a, b] = a"
using a b 1 RTS⇩S.cod_simp RTSx.cod_pr1 ide_iff_RTS_obj comp_def
p⇩1_def
by metis
next
fix f g
assume fg: "span f g"
have a: "ide (cod f)" and b: "ide (cod g)"
using fg by auto
have 1: "RTSx.H.span f g"
using fg RTS⇩S.arrE RTS⇩S.dom_simp comp_def by force
have 2: "RTSx.cod f = cod f ∧ RTSx.cod g = cod g"
using fg by (simp add: RTS⇩S.cod_char⇩S⇩b⇩C comp_def)
show "∃!l. 𝔭⇩1[cod f, cod g] ⋅ l = f ∧ 𝔭⇩0[cod f, cod g] ⋅ l = g"
proof -
have "∃l. 𝔭⇩1[cod f, cod g] ⋅ l = f ∧ 𝔭⇩0[cod f, cod g] ⋅ l = g"
proof -
let ?l = "RTSx.tuple f g"
have "𝔭⇩1[cod f, cod g] ⋅ ?l = f ∧ 𝔭⇩0[cod f, cod g] ⋅ ?l = g"
using a b fg 1 2 RTSx.sta_p⇩0 RTSx.sta_p⇩1 arr_iff_RTS_sta
ide_iff_RTS_obj
by (simp add: comp_def RTS⇩S.comp_def p⇩0_def p⇩1_def)
thus "∃l. 𝔭⇩1[cod f, cod g] ⋅ l = f ∧ 𝔭⇩0[cod f, cod g] ⋅ l = g"
by blast
qed
moreover
have "⋀l l'. ⟦𝔭⇩1[cod f, cod g] ⋅ l = f ∧ 𝔭⇩0[cod f, cod g] ⋅ l = g;
𝔭⇩1[cod f, cod g] ⋅ l' = f ∧ 𝔭⇩0[cod f, cod g] ⋅ l' = g⟧
⟹ l' = l"
by (metis (no_types, lifting) 1 RTSx.tuple_eqI RTS⇩S.comp_simp
a b fg ide_iff_RTS_obj comp_def p⇩0_def p⇩1_def)
ultimately show ?thesis by blast
qed
qed
notation prod (infixr "⊗" 51)
notation tuple ("⟨_, _⟩")
notation dup ("𝖽[_]")
notation assoc ("𝖺[_, _, _]")
notation assoc' ("𝖺⇧-⇧1[_, _, _]")
notation lunit ("𝗅[_]")
notation lunit' ("𝗅⇧-⇧1[_]")
notation runit ("𝗋[_]")
notation runit' ("𝗋⇧-⇧1[_]")
lemma tuple_char:
shows "tuple = (λf g. if span f g then RTSx.tuple f g else null)"
proof -
have "⋀f g. ⟨f, g⟩ = (if span f g then RTSx.tuple f g else null)"
proof -
fix f g
show "⟨f, g⟩ = (if span f g then RTSx.tuple f g else null)"
proof (cases "span f g")
case True
have "RTSx.tuple f g = ⟨f, g⟩"
by (metis (no_types, lifting) RTSx.tuple_pr_arr RTS⇩S.comp_simp
RTS⇩S.seq_char⇩S⇩b⇩C True ide_cod ide_iff_RTS_obj comp_def
p⇩0_def p⇩1_def tuple_eqI universal)
thus "⟨f, g⟩ = (if span f g then RTSx.tuple f g else null)"
using True by auto
next
case False
show "⟨f, g⟩ = (if span f g then RTSx.tuple f g else null)"
using False tuple_ext by auto
qed
qed
thus ?thesis by blast
qed
lemma prod_char:
shows "(⊗) = (λf g. if arr f ∧ arr g then RTSx.prod f g else null)"
proof -
have "⋀f g. f ⊗ g = (if arr f ∧ arr g then RTSx.prod f g else null)"
proof -
fix f g
have "¬ arr f ⟹ f ⊗ g = (if arr f ∧ arr g then RTSx.prod f g else null)"
using prod_def tuple_def by auto
moreover
have "¬ arr g ⟹ f ⊗ g = (if arr f ∧ arr g then RTSx.prod f g else null)"
using prod_def tuple_def by auto
moreover have "⟦arr f; arr g⟧
⟹ f ⊗ g = (if arr f ∧ arr g then RTSx.prod f g else null)"
proof -
assume f: "arr f" and g: "arr g"
have "f ⊗ g = ⟨f ⋅ 𝔭⇩1[dom f, dom g], g ⋅ 𝔭⇩0[dom f, dom g]⟩"
unfolding prod_def by simp
also have "... = ⟨f ⋅ 𝔭⇩1[RTSx.dom f, RTSx.dom g],
g ⋅ 𝔭⇩0[RTSx.dom f, RTSx.dom g]⟩"
using f g RTS⇩S.dom_char⇩S⇩b⇩C comp_def by force
also have "... = ⟨RTSx.hcomp f 𝔭⇩1[RTSx.dom f, RTSx.dom g],
RTSx.hcomp g 𝔭⇩0[RTSx.dom f, RTSx.dom g]⟩"
using f g RTS⇩S.comp_char RTS⇩S.arr_char⇩S⇩b⇩C
by (metis (no_types, lifting) RTS⇩S.null_char calculation
comp_def not_arr_null prod_simps(1) tuple_ext)
also have "... = RTSx.tuple
(RTSx.hcomp f 𝔭⇩1[RTSx.dom f, RTSx.dom g])
(RTSx.hcomp g 𝔭⇩0[RTSx.dom f, RTSx.dom g])"
by (metis (no_types, lifting) calculation f g not_arr_null
prod_simps(1) tuple_char)
also have "... = RTSx.prod f g"
using RTSx.prod_def by (simp add: p⇩0_def p⇩1_def)
finally show ?thesis
using f g by auto
qed
ultimately show "f ⊗ g = (if arr f ∧ arr g then RTSx.prod f g else null)"
by blast
qed
thus ?thesis by blast
qed
definition Pack :: "'A arr ⇒ 'A arr ⇒ 'A × 'A ⇒ 'A"
where "Pack ≡ RTSx.Pack"
definition Unpack :: "'A arr ⇒ 'A arr ⇒ 'A ⇒ 'A × 'A"
where "Unpack ≡ RTSx.Unpack"
lemma inverse_simulations_Pack_Unpack:
assumes "ide a" and "ide b"
shows "inverse_simulations (Rts (a ⊗ b)) (product_rts.resid (Rts a) (Rts b))
(Pack a b) (Unpack a b)"
using Pack_def RTSx.inverse_simulations_Pack_Unpack Rts_def Unpack_def
assms(1-2) ide_iff_RTS_obj prod_char
by force
lemma simulation_Pack:
assumes "ide a" and "ide b"
shows "simulation
(product_rts.resid (Rts a) (Rts b)) (Rts (a ⊗ b)) (Pack a b)"
using assms inverse_simulations_Pack_Unpack inverse_simulations_def
by fast
lemma simulation_Unpack:
assumes "ide a" and "ide b"
shows "simulation
(Rts (a ⊗ b)) (product_rts.resid (Rts a) (Rts b)) (Unpack a b)"
using assms inverse_simulations_Pack_Unpack inverse_simulations_def
by fast
lemma Pack_o_Unpack:
assumes "ide a" and "ide b"
shows "Pack a b ∘ Unpack a b = I (Rts (a ⊗ b))"
unfolding Pack_def Unpack_def Rts_def
using assms RTSx.Pack_o_Unpack ide_iff_RTS_obj prod_char by auto
lemma Unpack_o_Pack:
assumes "ide a" and "ide b"
shows "Unpack a b ∘ Pack a b = I (product_rts.resid (Rts a) (Rts b))"
unfolding Pack_def Unpack_def Rts_def
using assms RTSx.Unpack_o_Pack ide_iff_RTS_obj prod_char by auto
lemma Pack_Unpack [simp]:
assumes "ide a" and "ide b"
and "residuation.arr (Rts (a ⊗ b)) t"
shows "Pack a b (Unpack a b t) = t"
using assms by (metis Pack_o_Unpack comp_apply)
lemma Unpack_Pack [simp]:
assumes "ide a" and "ide b"
and "residuation.arr (product_rts.resid (Rts a) (Rts b)) t"
shows "Unpack a b (Pack a b t) = t"
using assms by (metis Unpack_o_Pack comp_apply)
lemma Map_p⇩0:
assumes "ide a" and "ide b"
shows "Map 𝔭⇩0[a, b] = product_rts.P⇩0 (Rts a) (Rts b) ∘ Unpack a b"
unfolding Map_def p⇩0_def Unpack_def
using assms RTSx.Map_p⇩0 Rts_def ide_iff_RTS_obj by auto
lemma Map_p⇩1:
assumes "ide a" and "ide b"
shows "Map 𝔭⇩1[a, b] = product_rts.P⇩1 (Rts a) (Rts b) ∘ Unpack a b"
unfolding Map_def p⇩1_def Unpack_def
using assms RTSx.Map_p⇩1 Rts_def ide_iff_RTS_obj by auto
lemma Map_tuple:
assumes "«f : x → a»" and "«g : x → b»"
shows "Map ⟨f, g⟩ = Pack a b ∘ ⟨⟨Map f, Map g⟩⟩"
unfolding Map_def Pack_def comp_def
using assms RTSx.Map_tuple
by (metis (no_types, lifting) RTS⇩S.in_hom_char⇩S⇩b⇩C in_homE comp_def
tuple_char)
corollary Map_dup:
assumes "ide a"
shows "Map 𝖽[a] = Pack a a ∘ ⟨⟨Map a, Map a⟩⟩"
using assms Map_tuple ide_in_hom by blast
proposition Map_lunit:
assumes "ide a"
shows "Map 𝗅[a] = product_rts.P⇩0 (Rts ❙𝟭) (Rts a) ∘ Unpack ❙𝟭 a"
using assms Map_p⇩0 ide_one by auto
proposition Map_runit:
assumes "ide a"
shows "Map 𝗋[a] = product_rts.P⇩1 (Rts a) (Rts ❙𝟭) ∘ Unpack a ❙𝟭"
using assms Map_p⇩1 ide_one by auto
lemma assoc_expansion:
assumes "ide a" and "ide b" and "ide c"
shows "𝖺[a, b, c] =
⟨𝔭⇩1[a, b] ⋅ 𝔭⇩1[a ⊗ b, c], ⟨𝔭⇩0[a, b] ⋅ 𝔭⇩1[a ⊗ b, c], 𝔭⇩0[a ⊗ b, c]⟩ ⟩"
using assms RTSx.assoc_expansion assoc_def p⇩0_def p⇩1_def by simp
lemma Unpack_naturality:
assumes "arr f" and "arr g"
shows "Unpack (cod f) (cod g) ∘ Map (f ⊗ g) =
product_simulation.map (Rts (dom f)) (Rts (dom g)) (Map f) (Map g) ∘
Unpack (dom f) (dom g)"
proof -
interpret Dom_f: extensional_rts ‹Rts (dom f)›
by (simp add: assms(1))
interpret Dom_g: extensional_rts ‹Rts (dom g)›
by (simp add: assms(2))
interpret Cod_f: extensional_rts ‹Rts (cod f)›
by (simp add: assms(1))
interpret Cod_g: extensional_rts ‹Rts (cod g)›
by (simp add: assms(2))
interpret Dom: product_rts ‹Rts (dom f)› ‹Rts (dom g)› ..
interpret Cod: product_rts ‹Rts (cod f)› ‹Rts (cod g)› ..
interpret Dom: extensional_rts Dom.resid
using Dom.preserves_extensional_rts Dom_f.extensional_rts_axioms
Dom_g.extensional_rts_axioms
by simp
interpret Unpack: simulation
‹Rts (dom f ⊗ dom g)› Dom.resid ‹Unpack (dom f) (dom g)›
using assms simulation_Unpack [of "dom f" "dom g"] by simp
interpret Unpack.A: extensional_rts ‹Rts (dom f ⊗ dom g)›
by (simp add: assms)
interpret Unpack: simulation_as_transformation
‹Rts (dom f ⊗ dom g)› Dom.resid ‹Unpack (dom f) (dom g)›
..
have "Unpack (cod f) (cod g) ∘ Map (f ⊗ g) =
Unpack (cod f) (cod g) ∘
Map ⟨f ⋅ 𝔭⇩1[dom f, dom g], g ⋅ 𝔭⇩0[dom f, dom g]⟩"
using assms prod_def by force
also have "... = Unpack (cod f) (cod g) ∘
Pack (cod f) (cod g) ∘
(Cod.tuple (Map (f ⋅ 𝔭⇩1[dom f, dom g]))
(Map (g ⋅ 𝔭⇩0[dom f, dom g])))"
using assms Map_tuple
by (metis (no_types, lifting) Fun.comp_assoc cod_pr0 cod_pr1
comp_in_homI' ide_dom pr_simps(1-2,4-5))
also have "... = I (Cod.resid) ∘
Cod.tuple (Map (f ⋅ 𝔭⇩1[dom f, dom g]))
(Map (g ⋅ 𝔭⇩0[dom f, dom g]))"
using assms Unpack_o_Pack by auto
also have "... = Cod.tuple (Map (f ⋅ 𝔭⇩1[dom f, dom g]))
(Map (g ⋅ 𝔭⇩0[dom f, dom g]))"
proof -
have "simulation (Rts (dom f ⊗ dom g)) Cod.resid
(Cod.tuple
(Map (f ⋅ 𝔭⇩1[dom f, dom g]))
(Map (g ⋅ 𝔭⇩0[dom f, dom g])))"
by (metis arrD(3) assms(1-2) cod_comp cod_pr0 cod_pr1 dom_comp
ide_dom pr_simps(1-2,4-5) seqI simulation_tuple)
thus ?thesis
using assms comp_identity_simulation by blast
qed
also have "... = Cod.tuple
(Map f ∘ (Dom.P⇩1 ∘ Unpack (dom f) (dom g)))
(Map g ∘ (Dom.P⇩0 ∘ Unpack (dom f) (dom g)))"
using assms Map_comp Map_p⇩1 Map_p⇩0 by auto
also have "... = product_simulation.map (Rts f) (Rts g) (Map f) (Map g) ∘
Dom.tuple
(Dom.P⇩1 ∘ Unpack (dom f) (dom g))
(Dom.P⇩0 ∘ Unpack (dom f) (dom g))"
proof -
interpret P⇩1oUnpack: simulation ‹Rts (dom f ⊗ dom g)› ‹Rts (dom f)›
‹Dom.P⇩1 ∘ Unpack (dom f) (dom g)›
using assms Dom.P⇩1_is_simulation simulation_comp
simulation_Unpack [of "dom f" "dom g"]
by auto
interpret P⇩1oUnpack: simulation_as_transformation
‹Rts (dom f ⊗ dom g)› ‹Rts (dom f)›
‹Dom.P⇩1 ∘ Unpack (dom f) (dom g)›
..
interpret P⇩0oUnpack: simulation ‹Rts (dom f ⊗ dom g)› ‹Rts (dom g)›
‹Dom.P⇩0 ∘ Unpack (dom f) (dom g)›
using assms Dom.P⇩0_is_simulation simulation_comp
simulation_Unpack [of "dom f" "dom g"]
by auto
interpret P⇩0oUnpack: simulation_as_transformation
‹Rts (dom f ⊗ dom g)› ‹Rts (dom g)›
‹Dom.P⇩0 ∘ Unpack (dom f) (dom g)›
..
show ?thesis
by (metis (no_types, lifting) P⇩0oUnpack.transformation_axioms
P⇩1oUnpack.transformation_axioms RTSx.Dom_dom RTSx.V.ide_implies_arr
RTS⇩S.dom_char⇩S⇩b⇩C Rts_def arrD(3) arr_iff_RTS_sta assms(1-2)
comp_product_simulation_tuple2 comp_def)
qed
also have "... = product_simulation.map
(Rts (dom f)) (Rts (dom g)) (Map f) (Map g) ∘
Unpack (dom f) (dom g)"
using assms Unpack.simulation_axioms Dom.tuple_proj RTSx.arr_char
by (metis (no_types, lifting) RTSx.Dom_dom RTSx.V.ide_implies_arr
RTS⇩S.arrE RTS⇩S.dom_char⇩S⇩b⇩C Rts_def comp_def)
finally show ?thesis by blast
qed
lemma Map_prod:
assumes "arr f" and "arr g"
shows "Map (f ⊗ g) =
Pack (cod f) (cod g) ∘
product_simulation.map (Rts (dom f)) (Rts (dom g)) (Map f) (Map g) ∘
Unpack (dom f) (dom g)"
proof -
have "Map (f ⊗ g) =
Pack (cod f) (cod g) ∘ (Unpack (cod f) (cod g) ∘ Map (f ⊗ g))"
proof -
have "Map (f ⊗ g) =
(Pack (cod f) (cod g) ∘ (Unpack (cod f) (cod g)) ∘ Map (f ⊗ g))"
using assms Pack_o_Unpack [of "cod f" "cod g"] arrD(3) [of "f ⊗ g"]
by (simp add: comp_identity_simulation)
thus ?thesis
using Fun.comp_assoc by metis
qed
also have "... =
Pack (cod f) (cod g) ∘
(product_simulation.map
(Rts (dom f)) (Rts (dom g)) (Map f) (Map g) ∘
Unpack (dom f) (dom g))"
using assms Unpack_naturality [of f g] by auto
also have "... = Pack (cod f) (cod g) ∘
product_simulation.map
(Rts (dom f)) (Rts (dom g)) (Map f) (Map g) ∘
Unpack (dom f) (dom g)"
by auto
finally show ?thesis by blast
qed
subsection "Exponentials"
definition exp :: "'A arr ⇒ 'A arr ⇒ 'A arr"
where "exp ≡ RTSx.exp"
definition eval :: "'A arr ⇒ 'A arr ⇒ 'A arr"
where "eval ≡ RTSx.eval"
definition curry :: "'A arr ⇒ 'A arr ⇒ 'A arr ⇒ 'A arr ⇒ 'A arr"
where "curry ≡ RTSx.curry"
definition uncurry :: "'A arr ⇒ 'A arr ⇒ 'A arr ⇒ 'A arr ⇒ 'A arr"
where "uncurry ≡ RTSx.uncurry"
definition Func :: "'A arr ⇒ 'A arr ⇒ 'A ⇒ ('A, 'A) exponential_rts.arr"
where "Func ≡ RTSx.Func"
definition Unfunc :: "'A arr ⇒ 'A arr ⇒ ('A, 'A) exponential_rts.arr ⇒ 'A"
where "Unfunc ≡ RTSx.Unfunc"
lemma inverse_simulations_Func_Unfunc:
assumes "ide b" and "ide c"
shows "inverse_simulations
(exponential_rts.resid (Rts b) (Rts c)) (Rts (exp b c))
(Func b c) (Unfunc b c)"
unfolding Func_def Unfunc_def Rts_def exp_def
using assms RTSx.inverse_simulations_Func_Unfunc ide_iff_RTS_obj by blast
lemma simulation_Func:
assumes "ide b" and "ide c"
shows "simulation
(Rts (exp b c)) (exponential_rts.resid (Rts b) (Rts c)) (Func b c)"
using assms inverse_simulations_Func_Unfunc inverse_simulations_def
by fast
lemma simulation_Unfunc:
assumes "ide b" and "ide c"
shows "simulation
(exponential_rts.resid (Rts b) (Rts c)) (Rts (exp b c)) (Unfunc b c)"
using assms inverse_simulations_Func_Unfunc inverse_simulations_def
by fast
lemma Func_o_Unfunc:
assumes "ide b" and "ide c"
shows "Func b c ∘ Unfunc b c = I (exponential_rts.resid (Rts b) (Rts c))"
using assms
by (meson inverse_simulations.inv' inverse_simulations_Func_Unfunc)
lemma Unfunc_o_Func:
assumes "ide b" and "ide c"
shows "Unfunc b c ∘ Func b c = I (Rts (exp b c))"
using assms
by (meson inverse_simulations.inv inverse_simulations_Func_Unfunc)
lemma Func_Unfunc [simp]:
assumes "ide b" and "ide c"
and "residuation.arr (exponential_rts.resid (Rts b) (Rts c)) t"
shows "Func b c (Unfunc b c t) = t"
using assms
by (meson inverse_simulations.inv'_simp inverse_simulations_Func_Unfunc)
lemma Unfunc_Func [simp]:
assumes "ide b" and "ide c"
and "residuation.arr (Rts (exp b c)) t"
shows "Unfunc b c (Func b c t) = t"
using assms
by (meson inverse_simulations.inv_simp inverse_simulations_Func_Unfunc)
lemma Map_eval:
assumes "ide b" and "ide c"
shows "Map (eval b c) =
evaluation_map.map (Rts b) (Rts c) ∘
product_simulation.map (Rts (exp b c)) (Rts b) (Func b c) (I (Rts b)) ∘
Unpack (exp b c) b"
unfolding Map_def eval_def Rts_def exp_def Func_def Unpack_def
using assms RTSx.Map_eval [of b c] ide_iff_RTS_obj by force
lemma Map_curry:
assumes "ide a" and "ide b" and "«f : a ⊗ b → c»"
shows "Map (curry a b c f) =
Unfunc b c ∘
Currying.Curry3 (Rts a) (Rts b) (Rts c) (Map f ∘ Pack a b)"
unfolding Map_def curry_def Unfunc_def Rts_def Pack_def
using assms RTSx.Map_curry [of a b c f] ide_iff_RTS_obj arr_iff_RTS_sta
by (metis (no_types, lifting) RTSx.H.category_axioms RTSx.Map_simps(3-4)
RTSx.V.ide_iff_src_self RTSx.V.trg_ide RTSx.arr_coincidence⇩C⇩R⇩C
RTS⇩S.ide_cod RTS⇩S.in_hom_char⇩S⇩b⇩C category.in_homE category_axioms
comp_def)
lemma Map_uncurry:
assumes "ide b" and "ide c" and "«g : a → exp b c»"
shows "Map (uncurry a b c g) =
Currying.Uncurry (Rts a) (Rts b) (Rts c) (Func b c ∘ Map g) ∘
Unpack a b"
unfolding Map_def uncurry_def Func_def Rts_def Unpack_def
using assms RTSx.Map_uncurry ide_iff_RTS_obj arr_iff_RTS_sta ide_dom
by auto
subsection "Cartesian Closure"
sublocale elementary_cartesian_closed_category
comp p⇩0 p⇩1 one trm exp eval curry
proof
fix b c
assume b: "ide b" and c: "ide c"
show "«eval b c : exp b c ⊗ b → c»"
unfolding eval_def exp_def
using b c RTSx.eval_in_hom⇩R⇩C⇩R prod_char ide_iff_RTS_obj
arr_iff_RTS_sta RTSx.obj_is_sta
by (simp add: RTSx.obj_exp RTS⇩S.in_hom_char⇩S⇩b⇩C comp_def)
show "ide (exp b c)"
unfolding exp_def
using b c ide_iff_RTS_obj RTSx.obj_exp by simp
fix a
assume a: "ide a"
fix g
assume g: "«g : a ⊗ b → c»"
show 1: "«curry a b c g : a → exp b c»"
unfolding curry_def
using a b c g ide_char prod_char ide_iff_RTS_obj
RTS⇩S.arr_char⇩S⇩b⇩C RTS⇩S.in_hom_char⇩S⇩b⇩C ‹ide (exp b c)›
exp_def comp_def RTSx.curry_in_hom RTSx.sta_curry
by (metis (no_types, lifting))
show "eval b c ⋅ (curry a b c g ⊗ b) = g"
using a b c g 1 RTSx.uncurry_curry RTSx.uncurry_expansion
arr_iff_RTS_sta ide_iff_RTS_obj RTS⇩S.comp_char
RTS⇩S.in_hom_char⇩S⇩b⇩C ideD(1)
apply (auto simp add: exp_def comp_def curry_def eval_def)[1]
apply (metis (no_types, lifting) comp_def prod_char)
apply (metis comp_def prod_simps(1))
by (metis (no_types, lifting) RTSx.H.ext RTSx.arr_coincidence⇩C⇩R⇩C
RTSx.null_coincidence⇩C⇩R⇩C comp_def prod_char)
next
fix a b c h
assume a: "ide a" and b: "ide b" and c: "ide c"
and h: "«h : a → exp b c»"
show "curry a b c (eval b c ⋅ (h ⊗ b)) = h"
using a b c h prod_char RTSx.curry_uncurry ide_iff_RTS_obj
RTSx.uncurry_expansion RTS⇩S.comp_char RTS⇩S.in_hom_char⇩S⇩b⇩C
RTSx.obj_is_sta RTSx.sta_prod RTS⇩S.arr_char⇩S⇩b⇩C
apply (auto simp add: eval_def curry_def comp_def exp_def)[1]
by (metis (no_types, lifting) RTSx.H.ext RTSx.arr_coincidence⇩C⇩R⇩C
RTSx.null_coincidence⇩C⇩R⇩C)
qed
theorem is_elementary_cartesian_closed_category:
shows "elementary_cartesian_closed_category
comp p⇩0 p⇩1 one trm exp eval curry"
..
end
subsection "Associators"
text ‹
Here we expose the relationship between the associators internal to ‹❙R❙T❙S› and those
external to it.
›
locale Association =
rtscat arr_type
for arr_type :: "'A itself"
and a :: "'A rtscat.arr"
and b :: "'A rtscat.arr"
and c :: "'A rtscat.arr" +
assumes a: "ide a"
and b: "ide b"
and c: "ide c"
begin
interpretation A: extensional_rts ‹Rts a›
using a by simp
interpretation B: extensional_rts ‹Rts b›
using b by simp
interpretation C: extensional_rts ‹Rts c›
using c by simp
interpretation A: identity_simulation ‹Rts a› ..
interpretation B: identity_simulation ‹Rts b› ..
interpretation C: identity_simulation ‹Rts c› ..
interpretation AxB: product_rts ‹Rts a› ‹Rts b› ..
interpretation AxB_xC: product_rts AxB.resid ‹Rts c› ..
interpretation BxC: product_rts ‹Rts b› ‹Rts c› ..
interpretation Ax_BxC: product_rts ‹Rts a› BxC.resid ..
interpretation AxB: extensional_rts AxB.resid
using A.extensional_rts_axioms B.extensional_rts_axioms
AxB.preserves_extensional_rts
by blast
interpretation BxC: extensional_rts BxC.resid
using B.extensional_rts_axioms C.extensional_rts_axioms
BxC.preserves_extensional_rts
by blast
interpretation AxB_xC: extensional_rts AxB_xC.resid
using AxB.extensional_rts_axioms C.extensional_rts_axioms
AxB_xC.preserves_extensional_rts
by blast
interpretation Ax_BxC: extensional_rts Ax_BxC.resid
using A.extensional_rts_axioms BxC.extensional_rts_axioms
Ax_BxC.preserves_extensional_rts
by blast
sublocale ASSOC: ASSOC ‹Rts a› ‹Rts b› ‹Rts c› ..
interpretation axb: extensional_rts ‹Rts (a ⊗ b)›
using a b by simp
interpretation bxc: extensional_rts ‹Rts (b ⊗ c)›
using b c by simp
interpretation axb_xc: extensional_rts ‹Rts ((a ⊗ b) ⊗ c)›
using a b c by simp
interpretation ax_bxc: extensional_rts ‹Rts (a ⊗ (b ⊗ c))›
using a b c by simp
interpretation PU_ab: inverse_simulations
‹Rts (a ⊗ b)› AxB.resid ‹Pack a b› ‹Unpack a b›
using a b inverse_simulations_Pack_Unpack [of a b] by fastforce
interpretation PU_bc: inverse_simulations
‹Rts (b ⊗ c)› BxC.resid ‹Pack b c› ‹Unpack b c›
using b c inverse_simulations_Pack_Unpack [of b c] by fastforce
interpretation Axbc: product_rts ‹Rts a› ‹Rts (b ⊗ c)› ..
interpretation Axbc: identity_simulation Axbc.resid ..
interpretation abxC: product_rts ‹Rts (a ⊗ b)› ‹Rts c› ..
interpretation abxC: identity_simulation abxC.resid ..
interpretation AxPack_bc:
product_simulation ‹Rts a› BxC.resid ‹Rts a› ‹Rts (b ⊗ c)›
‹I (Rts a)› ‹Pack b c› ..
interpretation AxUnpack_bc:
product_simulation ‹Rts a› ‹Rts (b ⊗ c)› ‹Rts a› BxC.resid
‹I (Rts a)› ‹Unpack b c› ..
interpretation Unpack_abxC:
product_simulation ‹Rts (a ⊗ b)› ‹Rts c› AxB.resid ‹Rts c›
‹Unpack a b› ‹I (Rts c)› ..
sublocale PU_Axbc: inverse_simulations Axbc.resid Ax_BxC.resid
AxPack_bc.map AxUnpack_bc.map
proof
show "AxPack_bc.map ∘ AxUnpack_bc.map = Axbc.map"
proof -
have "AxPack_bc.map ∘ AxUnpack_bc.map =
product_simulation.map (Rts a) (Rts (b ⊗ c))
(A.map ∘ A.map) (Pack b c ∘ Unpack b c)"
using A.simulation_axioms PU_bc.F.simulation_axioms
PU_bc.G.simulation_axioms PU_bc.inv'
simulation_interchange
[of "Rts a" "Rts a" A.map "Rts (b ⊗ c)"
BxC.resid "Unpack b c" "Rts a"
A.map "Rts (b ⊗ c)" "Pack b c"]
by simp
also have "... =
product_simulation.map (Rts a) (Rts (b ⊗ c))
A.map (I (Rts (b ⊗ c)))"
using PU_bc.inv' A.simulation_axioms
comp_identity_simulation [of "Rts a" "Rts a" A.map]
by simp
also have "... = Axbc.map"
using product_identity_simulation A.rts_axioms bxc.rts_axioms
by blast
finally show ?thesis by blast
qed
show "AxUnpack_bc.map ∘ AxPack_bc.map = I Ax_BxC.resid"
proof -
have "AxUnpack_bc.map ∘ AxPack_bc.map =
product_simulation.map (Rts a) BxC.resid
(A.map ∘ A.map) (Unpack b c ∘ Pack b c)"
using A.simulation_axioms PU_bc.F.simulation_axioms
PU_bc.G.simulation_axioms PU_bc.inv
simulation_interchange
[of "Rts a" "Rts a" "A.map" BxC.resid "Rts (b ⊗ c)"
"Pack b c" "Rts a" A.map BxC.resid "Unpack b c"]
by simp
also have "... =
product_simulation.map (Rts a) BxC.resid
A.map (I BxC.resid)"
using PU_bc.inv A.simulation_axioms
comp_identity_simulation [of "Rts a" "Rts a" A.map]
by simp
also have "... = I Ax_BxC.resid"
using product_identity_simulation A.rts_axioms BxC.rts_axioms
by blast
finally show ?thesis by blast
qed
qed
text ‹
The following shows that the simulation ‹Map 𝖺[a, b, c]› underlying an internal associator
‹𝖺[a, b, c]› is transformed into a corresponding external associator ‹ASSOC.map› via
invertible simulations that ``unpack'' product objects in ‹❙R❙T❙S› into corresponding
product RTS's.
›
lemma Unpack_o_Map_assoc:
shows "(AxUnpack_bc.map ∘ Unpack a (b ⊗ c)) ∘ Map 𝖺[a, b, c] =
ASSOC.map ∘ (Unpack_abxC.map ∘ Unpack (a ⊗ b) c)"
proof -
have "(AxUnpack_bc.map ∘ Unpack a (b ⊗ c)) ∘ Map 𝖺[a, b, c] =
(AxUnpack_bc.map ∘ Unpack a (b ⊗ c)) ∘
Pack a (b ⊗ c) ∘
(Axbc.tuple
(Map (𝔭⇩1[a, b] ⋅ 𝔭⇩1[a ⊗ b, c]))
(Map ⟨𝔭⇩0[a, b] ⋅ 𝔭⇩1[a ⊗ b, c], 𝔭⇩0[a ⊗ b, c]⟩))"
using a b c
Map_tuple
[of "𝔭⇩1[a, b] ⋅ 𝔭⇩1[a ⊗ b, c]" "(a ⊗ b) ⊗ c" a
"⟨𝔭⇩0[a, b] ⋅ 𝔭⇩1[a ⊗ b, c], 𝔭⇩0[a ⊗ b, c]⟩" "b ⊗ c"]
assoc_expansion [of a b c]
by auto
also have "... = AxUnpack_bc.map ∘
(Unpack a (b ⊗ c) ∘ Pack a (b ⊗ c)) ∘
(Axbc.tuple
(Map (𝔭⇩1[a, b] ⋅ 𝔭⇩1[a ⊗ b, c]))
(Map ⟨𝔭⇩0[a, b] ⋅ 𝔭⇩1[a ⊗ b, c], 𝔭⇩0[a ⊗ b, c]⟩))"
by force
also have "... = AxUnpack_bc.map ∘
I Axbc.resid ∘
(Axbc.tuple
(Map (𝔭⇩1[a, b] ⋅ 𝔭⇩1[a ⊗ b, c]))
(Map ⟨𝔭⇩0[a, b] ⋅ 𝔭⇩1[a ⊗ b, c], 𝔭⇩0[a ⊗ b, c]⟩))"
using a b c Unpack_o_Pack [of a "b ⊗ c"] by fastforce
also have "... = AxUnpack_bc.map ∘
(Axbc.tuple
(Map (𝔭⇩1[a, b] ⋅ 𝔭⇩1[a ⊗ b, c]))
(Map ⟨𝔭⇩0[a, b] ⋅ 𝔭⇩1[a ⊗ b, c], 𝔭⇩0[a ⊗ b, c]⟩))"
using comp_simulation_identity
[of Axbc.resid Ax_BxC.resid AxUnpack_bc.map]
AxUnpack_bc.simulation_axioms
by simp
also have "... = Ax_BxC.tuple
(I (Rts a) ∘ Map (𝔭⇩1[a, b] ⋅ 𝔭⇩1[a ⊗ b, c]))
(Unpack b c ∘ Map ⟨𝔭⇩0[a, b] ⋅ 𝔭⇩1[a ⊗ b, c], 𝔭⇩0[a ⊗ b, c]⟩)"
proof -
have "simulation (Rts ((a ⊗ b) ⊗ c)) (Rts a) (Map (𝔭⇩1[a, b] ⋅ 𝔭⇩1[a ⊗ b, c]))"
using a b c
by (metis (no_types, lifting) arrD(3) cod_comp cod_pr1 dom_comp ide_prod
pr_simps(4) pr_simps(5) seqI)
moreover have "simulation (Rts ((a ⊗ b) ⊗ c)) (Rts (b ⊗ c))
(Map ⟨𝔭⇩0[a, b] ⋅ 𝔭⇩1[a ⊗ b, c], 𝔭⇩0[a ⊗ b, c]⟩)"
proof -
have "«⟨𝔭⇩0[a, b] ⋅ 𝔭⇩1[a ⊗ b, c], 𝔭⇩0[a ⊗ b, c]⟩ : (a ⊗ b) ⊗ c → b ⊗ c»"
using a b c by blast
thus ?thesis
using arrD(3) by fastforce
qed
ultimately show ?thesis
using PU_bc.G.simulation_axioms A.simulation_axioms
simulation_as_transformation.intro
comp_product_simulation_tuple
[of "Rts a" "Rts a" A.map "Rts (b ⊗ c)" BxC.resid "Unpack b c"
"Rts ((a ⊗ b) ⊗ c)" "Map (𝔭⇩1[a, b] ⋅ 𝔭⇩1[a ⊗ b, c])"
"Map ⟨𝔭⇩0[a, b] ⋅ 𝔭⇩1[a ⊗ b, c], 𝔭⇩0[a ⊗ b, c]⟩"]
by blast
qed
also have "... = Ax_BxC.tuple
(Map (𝔭⇩1[a, b] ⋅ 𝔭⇩1[a ⊗ b, c]))
(Unpack b c ∘ Map ⟨𝔭⇩0[a, b] ⋅ 𝔭⇩1[a ⊗ b, c], 𝔭⇩0[a ⊗ b, c]⟩)"
proof -
have "«p⇩1 a b ⋅ p⇩1 (a ⊗ b) c : (a ⊗ b) ⊗ c → a»"
using a b c by blast
hence "simulation (Rts ((a ⊗ b) ⊗ c)) (Rts a)
(Map (𝔭⇩1[a, b] ⋅ 𝔭⇩1[a ⊗ b, c]))"
using arrD(3) by (metis (no_types, lifting) in_homE)
thus ?thesis
using comp_identity_simulation
[of "Rts ((a ⊗ b) ⊗ c)" "Rts a" "Map (𝔭⇩1[a, b] ⋅ 𝔭⇩1[a ⊗ b, c])"]
by fastforce
qed
also have "... = Ax_BxC.tuple
(Map 𝔭⇩1[a, b] ∘ Map 𝔭⇩1[a ⊗ b, c])
(Unpack b c ∘ Map ⟨𝔭⇩0[a, b] ⋅ 𝔭⇩1[a ⊗ b, c], 𝔭⇩0[a ⊗ b, c]⟩)"
using a b c Map_comp by auto
also have "... = Ax_BxC.tuple
(Map 𝔭⇩1[a, b] ∘ Map 𝔭⇩1[a ⊗ b, c])
(Unpack b c ∘
(Pack b c ∘
abxC.tuple
(Map (𝔭⇩0[a, b] ⋅ 𝔭⇩1[a ⊗ b, c]))
(Map 𝔭⇩0[a ⊗ b, c])))"
using a b c Map_tuple
by (metis (no_types, lifting) comp_in_homI ide_prod pr_in_hom(1-2))
also have "... = Ax_BxC.tuple
(Map 𝔭⇩1[a, b] ∘ Map 𝔭⇩1[a ⊗ b, c])
((Unpack b c ∘ Pack b c) ∘
abxC.tuple
(Map (𝔭⇩0[a, b] ⋅ 𝔭⇩1[a ⊗ b, c]))
(Map 𝔭⇩0[a ⊗ b, c]))"
using fun.map_comp by metis
also have "... = Ax_BxC.tuple
(Map 𝔭⇩1[a, b] ∘ Map 𝔭⇩1[a ⊗ b, c])
(I BxC.resid ∘
BxC.tuple
(Map (𝔭⇩0[a, b] ⋅ 𝔭⇩1[a ⊗ b, c]))
(Map 𝔭⇩0[a ⊗ b, c]))"
using PU_bc.inv by simp
also have "... = Ax_BxC.tuple
(Map 𝔭⇩1[a, b] ∘ Map 𝔭⇩1[a ⊗ b, c])
(BxC.tuple
(Map 𝔭⇩0[a, b] ∘ Map 𝔭⇩1[a ⊗ b, c])
(Map 𝔭⇩0[a ⊗ b, c]))"
proof -
have "«𝔭⇩0[a, b] ⋅ 𝔭⇩1[a ⊗ b, c] : (a ⊗ b) ⊗ c → b» ∧
«𝔭⇩0[a ⊗ b, c] : (a ⊗ b) ⊗ c → c»"
using a b c by blast
hence "simulation (Rts ((a ⊗ b) ⊗ c)) BxC.resid
(pointwise_tuple (Map (𝔭⇩0[a, b] ⋅ 𝔭⇩1[a ⊗ b, c])) (Map 𝔭⇩0[a ⊗ b, c]))"
using a b c arrD(3) simulation_tuple in_homE by metis
thus ?thesis
using a b c Map_comp
comp_identity_simulation
[of "Rts ((a ⊗ b) ⊗ c)" BxC.resid
"BxC.tuple
(Map (𝔭⇩0[a, b] ⋅ 𝔭⇩1[a ⊗ b, c]))
(Map 𝔭⇩0[a ⊗ b, c])"]
by auto
qed
also have "... = Ax_BxC.tuple
((AxB.P⇩1 ∘ Unpack a b) ∘
(abxC.P⇩1 ∘ Unpack (a ⊗ b) c))
(BxC.tuple
((AxB.P⇩0 ∘ Unpack a b) ∘
(abxC.P⇩1 ∘ Unpack (a ⊗ b) c))
(abxC.P⇩0 ∘ Unpack (a ⊗ b) c))"
using a b c Map_p⇩1 Map_p⇩0 by auto
also have "... = Ax_BxC.tuple
(AxB.P⇩1 ∘ (Unpack a b ∘ abxC.P⇩1) ∘ Unpack (a ⊗ b) c)
(BxC.tuple
(AxB.P⇩0 ∘ (Unpack a b ∘ abxC.P⇩1) ∘ Unpack (a ⊗ b) c)
(abxC.P⇩0 ∘ Unpack (a ⊗ b) c))"
using fun.map_comp by metis
also have "... = Ax_BxC.tuple
(AxB.P⇩1 ∘ (AxB_xC.P⇩1 ∘ Unpack_abxC.map) ∘
Unpack (a ⊗ b) c)
(BxC.tuple
(AxB.P⇩0 ∘ (AxB_xC.P⇩1 ∘ Unpack_abxC.map) ∘
Unpack (a ⊗ b) c)
(abxC.P⇩0 ∘ Unpack (a ⊗ b) c))"
proof -
have "Unpack a b ∘ abxC.P⇩1 = AxB_xC.P⇩1 ∘ Unpack_abxC.map"
proof
fix x
show "(Unpack a b ∘ abxC.P⇩1) x =
(AxB_xC.P⇩1 ∘ Unpack_abxC.map) x"
proof (cases "abxC.arr x")
show "¬ abxC.arr x ⟹ ?thesis"
using Unpack_abxC.extensional AxB_xC.P⇩1.extensional
abxC.P⇩1.extensional PU_ab.G.extensional
by auto
assume x: "abxC.arr x"
show ?thesis
using x a b c abxC.P⇩1_def Unpack_abxC.map_def AxB_xC.P⇩1_def
apply auto[1]
using AxB.arr_char by blast+
qed
qed
thus ?thesis by simp
qed
also have "... = Ax_BxC.tuple
(AxB.P⇩1 ∘ AxB_xC.P⇩1 ∘ Unpack_abxC.map ∘
Unpack (a ⊗ b) c)
(BxC.tuple
(AxB.P⇩0 ∘ AxB_xC.P⇩1 ∘ Unpack_abxC.map ∘
Unpack (a ⊗ b) c)
(abxC.P⇩0 ∘ Unpack (a ⊗ b) c))"
proof -
have "AxB.P⇩1 ∘ (AxB_xC.P⇩1 ∘ Unpack_abxC.map) ∘ Unpack (a ⊗ b) c =
AxB.P⇩1 ∘ AxB_xC.P⇩1 ∘ Unpack_abxC.map ∘ Unpack (a ⊗ b) c"
by auto
moreover have "AxB.P⇩0 ∘ (AxB_xC.P⇩1 ∘ Unpack_abxC.map) ∘
Unpack (a ⊗ b) c =
AxB.P⇩0 ∘ AxB_xC.P⇩1 ∘ Unpack_abxC.map ∘
Unpack (a ⊗ b) c"
by auto
ultimately show ?thesis by simp
qed
also have "... = Ax_BxC.tuple
(AxB.P⇩1 ∘ AxB_xC.P⇩1 ∘ Unpack_abxC.map)
(BxC.tuple
(AxB.P⇩0 ∘ AxB_xC.P⇩1 ∘ Unpack_abxC.map)
abxC.P⇩0) ∘
Unpack (a ⊗ b) c"
by (simp add: comp_pointwise_tuple)
also have "... = Ax_BxC.tuple
(AxB.P⇩1 ∘ AxB_xC.P⇩1 ∘ Unpack_abxC.map)
(BxC.tuple
(AxB.P⇩0 ∘ AxB_xC.P⇩1 ∘ Unpack_abxC.map)
(AxB_xC.P⇩0 ∘ Unpack_abxC.map)) ∘
Unpack (a ⊗ b) c"
proof -
have "AxB_xC.P⇩0 ∘ Unpack_abxC.map = abxC.P⇩0"
proof
fix x
show "(AxB_xC.P⇩0 ∘ Unpack_abxC.map) x = abxC.P⇩0 x"
using a b c abxC.P⇩0_def Unpack_abxC.map_def AxB_xC.P⇩0_def
PU_ab.G.preserves_reflects_arr abxC.arr_char PU_ab.G.extensional
abxC.P⇩1.extensional axb.not_arr_null AxB_xC.P⇩1.extensional
AxB_xC.not_arr_null
by auto
qed
thus ?thesis by simp
qed
also have "... = Ax_BxC.tuple
(AxB.P⇩1 ∘ AxB_xC.P⇩1)
(BxC.tuple (AxB.P⇩0 ∘ AxB_xC.P⇩1) AxB_xC.P⇩0) ∘
Unpack_abxC.map ∘ Unpack (a ⊗ b) c"
by (simp add: comp_pointwise_tuple)
also have "... = ASSOC.map ∘ (Unpack_abxC.map ∘ Unpack (a ⊗ b) c)"
unfolding ASSOC.map_def by auto
finally show ?thesis by blast
qed
text ‹
As a corollary, we obtain an explicit formula for ‹Map 𝖺[a, b, c]› in terms of
the external associator ‹ASSOC.map› and packing and unpacking isomorphisms.
›
corollary Map_assoc:
shows "Map 𝖺[a, b, c] =
(Pack a (b ⊗ c) ∘ AxPack_bc.map) ∘
ASSOC.map ∘
(Unpack_abxC.map ∘ Unpack (a ⊗ b) c)"
proof -
interpret PU_axbc: inverse_simulations
‹Rts (a ⊗ (b ⊗ c))› Axbc.resid
‹Pack a (b ⊗ c)› ‹Unpack a (b ⊗ c)›
using a b c
inverse_simulations_Pack_Unpack [of a "b ⊗ c"]
by force
interpret PU_abxc: inverse_simulations
‹Rts ((a ⊗ b) ⊗ c)› abxC.resid
‹Pack (a ⊗ b) c› ‹Unpack (a ⊗ b) c›
using a b c
inverse_simulations_Pack_Unpack [of "a ⊗ b" c]
by force
interpret PoAxP: composite_simulation
Ax_BxC.resid Axbc.resid ‹Rts (a ⊗ b ⊗ c)›
AxPack_bc.map ‹Pack a (b ⊗ c)› ..
interpret UxCoU: composite_simulation
‹Rts ((a ⊗ b) ⊗ c)› abxC.resid AxB_xC.resid
‹Unpack (a ⊗ b) c› Unpack_abxC.map ..
interpret AxUoU: composite_simulation
‹Rts (a ⊗ b ⊗ c)› Axbc.resid Ax_BxC.resid
‹Unpack a (b ⊗ c)› AxUnpack_bc.map ..
have *: "inverse_simulations (Rts (a ⊗ b ⊗ c)) Ax_BxC.resid
(Pack a (b ⊗ c) ∘ AxPack_bc.map)
(AxUnpack_bc.map ∘ Unpack a (b ⊗ c))"
proof
show "AxUoU.map ∘ PoAxP.map = I Ax_BxC.resid"
proof -
have "AxUoU.map ∘ PoAxP.map =
AxUnpack_bc.map ∘ (Unpack a (b ⊗ c) ∘ Pack a (b ⊗ c)) ∘
AxPack_bc.map"
using fun.map_comp by force
also have "... = AxUnpack_bc.map ∘ I Axbc.resid ∘ AxPack_bc.map"
using PU_axbc.inv by simp
also have "... = AxUnpack_bc.map ∘ AxPack_bc.map"
using comp_simulation_identity AxUnpack_bc.simulation_axioms
by fastforce
also have "... = I Ax_BxC.resid"
using PU_Axbc.inv by blast
finally show ?thesis by blast
qed
show "PoAxP.map ∘ AxUoU.map = I (Rts (a ⊗ b ⊗ c))"
proof -
have "PoAxP.map ∘ AxUoU.map =
Pack a (b ⊗ c) ∘ (AxPack_bc.map ∘ AxUnpack_bc.map) ∘
Unpack a (b ⊗ c)"
using fun.map_comp by auto
also have "... = Pack a (b ⊗ c) ∘ I Axbc.resid ∘ Unpack a (b ⊗ c)"
using PU_Axbc.inv' by simp
also have "... = Pack a (b ⊗ c) ∘ Unpack a (b ⊗ c)"
using comp_simulation_identity PU_axbc.F.simulation_axioms
by fastforce
also have "... = I (Rts (a ⊗ b ⊗ c))"
using PU_axbc.inv' by blast
finally show ?thesis by blast
qed
qed
have "simulation (Rts ((a ⊗ b) ⊗ c)) (Rts (a ⊗ b ⊗ c)) (Map 𝖺[a, b, c]) "
using a b c arrD(3)
by (metis (no_types, lifting) assoc_simps(1-3))
hence "Map 𝖺[a, b, c] = I (Rts (a ⊗ b ⊗ c)) ∘ Map 𝖺[a, b, c]"
using a b c
comp_identity_simulation
[of "Rts ((a ⊗ b) ⊗ c)" "Rts (a ⊗ b ⊗ c)" "Map 𝖺[a, b, c]"]
by auto
also have "... = PoAxP.map ∘ AxUoU.map ∘ Map 𝖺[a, b, c]"
using a b c * inverse_simulations.inv' by fastforce
also have "... = PoAxP.map ∘ (AxUoU.map ∘ Map 𝖺[a, b, c])"
using fun.map_comp by fastforce
also have "... = PoAxP.map ∘ (ASSOC.map ∘ UxCoU.map)"
using Unpack_o_Map_assoc by simp
also have "... = PoAxP.map ∘ ASSOC.map ∘ UxCoU.map"
using fun.map_comp by fastforce
finally show ?thesis by blast
qed
end
context rtscat
begin
proposition Map_assoc:
assumes "ide a" and "ide b" and "ide c"
shows "Map 𝖺[a, b, c] =
Pack a (b ⊗ c) ∘
product_simulation.map (Rts a) (product_rts.resid (Rts b) (Rts c))
(I (Rts a)) (Pack b c) ∘
ASSOC.map (Rts a) (Rts b) (Rts c) ∘
(product_simulation.map
(Rts (a ⊗ b)) (Rts c) (Unpack a b) (I (Rts c)) ∘
Unpack (a ⊗ b) c)"
proof -
interpret A: Association arr_type a b c
using assms by unfold_locales auto
show ?thesis
using assms A.Map_assoc by force
qed
end
subsection "Compositors"
text ‹
Here we expose the relationship between the compositors internal to ‹❙R❙T❙S›
(inherited from @{locale closed_monoidal_category}) and those external to it
(given by horizontal composition of simulations).
›
context rtscat
begin
sublocale CMC: cartesian_monoidal_category comp Prod α ι
using extends_to_cartesian_monoidal_category⇩E⇩C⇩C by blast
sublocale ECMC: elementary_closed_monoidal_category comp Prod α ι
exp eval curry
using extends_to_elementary_closed_monoidal_category⇩E⇩C⇩C⇩C by blast
end
locale Composition =
rtscat arr_type
for arr_type :: "'A itself"
and a :: "'A rtscat.arr"
and b :: "'A rtscat.arr"
and c :: "'A rtscat.arr" +
assumes a: "ide a"
and b: "ide b"
and c: "ide c"
begin
abbreviation EXP
where "EXP ≡ λa b. Rts (exp a b)"
interpretation A: extensional_rts ‹Rts a›
using a by simp
interpretation B: extensional_rts ‹Rts b›
using b by simp
interpretation C: extensional_rts ‹Rts c›
using c by simp
interpretation AxB: product_rts ‹Rts a› ‹Rts b› ..
interpretation BxC: product_rts ‹Rts b› ‹Rts c› ..
interpretation AB: exponential_rts ‹Rts a› ‹Rts b› ..
interpretation BC: exponential_rts ‹Rts b› ‹Rts c› ..
interpretation AC: exponential_rts ‹Rts a› ‹Rts c› ..
interpretation ABxA: product_rts AB.resid ‹Rts a› ..
interpretation BCxAB: product_rts BC.resid AB.resid ..
interpretation BCxAB: extensional_rts BCxAB.resid
using AB.is_extensional_rts BC.is_extensional_rts
BCxAB.preserves_extensional_rts
by fastforce
interpretation BCxAB_x_A: product_rts BCxAB.resid ‹Rts a› ..
interpretation ab: extensional_rts ‹EXP a b›
using a b ide_exp_ax by simp
interpretation bc: extensional_rts ‹EXP b c›
using b c ide_exp_ax by simp
interpretation bcxab: product_of_extensional_rts ‹EXP b c› ‹EXP a b› ..
interpretation abxA: product_rts ‹EXP a b› ‹Rts a› ..
interpretation bcxB: product_rts ‹EXP b c› ‹Rts b› ..
interpretation bc_x_abxA: product_rts ‹EXP b c› abxA.resid ..
interpretation bcxab_x_A: product_rts bcxab.resid ‹Rts a› ..
interpretation ASSOC: ASSOC BC.resid AB.resid ‹Rts a› ..
interpretation COMP: COMP ‹Rts a› ‹Rts b› ‹Rts c› ..
interpretation Assoc_abc: Association arr_type a b c
using a b c by unfold_locales
interpretation Assoc_bc_ab_a: Association arr_type ‹exp b c› ‹exp a b› a
using a b c ide_exp_ax by unfold_locales
interpretation Func_Unfunc_ab: inverse_simulations AB.resid ‹EXP a b›
‹Func a b› ‹Unfunc a b›
using a b inverse_simulations_Func_Unfunc [of a b] by blast
interpretation Func_Unfunc_bc: inverse_simulations BC.resid ‹EXP b c›
‹Func b c› ‹Unfunc b c›
using a b c inverse_simulations_Func_Unfunc [of b c] by blast
interpretation Func_bcxFunc_ab: product_simulation
‹EXP b c› ‹EXP a b› BC.resid AB.resid
‹Func b c› ‹Func a b› ..
text ‹
The following shows that the simulation ‹Map (Comp a b c)› underlying an internal
compositor ‹Comp a b c› is transformed into a corresponding external compositor ‹COMP.map›
by invertible simulations that ``unpack'' product and exponential objects in ‹RTS⇩S› into
corresponding RTS products and exponentials.
›
lemma Func_o_Map_Comp:
shows "Func a c ∘ Map (ECMC.Comp a b c) =
COMP.map ∘ (Func_bcxFunc_ab.map ∘ Unpack (exp b c) (exp a b))"
proof -
interpret A: identity_simulation ‹Rts a› ..
interpret B: identity_simulation ‹Rts b› ..
interpret BC: identity_simulation BC.resid ..
interpret ABxA: identity_simulation ABxA.resid ..
interpret BCxB: product_rts BC.resid ‹Rts b› ..
interpret abxa: extensional_rts ‹Rts (exp a b ⊗ a)›
using a b ide_exp_ax by simp
interpret eval_ab: simulation ‹Rts (exp a b ⊗ a)› ‹Rts b› ‹Map (eval a b)›
using a b ide_exp_ax arrD eval_in_hom_ax [of a b] by force
interpret bc: identity_simulation ‹EXP b c› ..
interpret bcxeval: product_simulation
‹EXP b c› ‹Rts (exp a b ⊗ a)› ‹EXP b c› ‹Rts b›
bc.map ‹Map (eval a b)› ..
interpret bcxab': extensional_rts ‹Rts (exp b c ⊗ exp a b)›
using a b c ide_exp_ax by simp
interpret bcxab'_x_A: product_rts ‹Rts (exp b c ⊗ exp a b)› ‹Rts a› ..
interpret bcxab: identity_simulation bcxab.resid ..
interpret bcxab_x_A: product_simulation bcxab.resid ‹Rts a›
bcxab.resid ‹Rts a› bcxab.map A.map ..
interpret bcxab: extensional_rts ‹Rts (exp b c ⊗ exp a b)›
using a b c ide_exp_ax by simp
interpret PU_abxa: inverse_simulations ‹Rts (exp a b ⊗ a)› abxA.resid
‹Pack (exp a b) a› ‹Unpack (exp a b) a›
using a b c inverse_simulations_Pack_Unpack [of "exp a b" a] by blast
interpret PU_bcxab_xa: inverse_simulations
‹Rts ((exp b c ⊗ exp a b) ⊗ a)› bcxab'_x_A.resid
‹Pack (exp b c ⊗ exp a b) a›
‹Unpack (exp b c ⊗ exp a b) a›
using a b c ide_exp_ax inverse_simulations_Pack_Unpack by simp
interpret PU_bcxab: inverse_simulations ‹Rts (exp b c ⊗ exp a b)› bcxab.resid
‹Pack (exp b c) (exp a b)›
‹Unpack (exp b c) (exp a b)›
using a b c inverse_simulations_Pack_Unpack [of "exp b c" "exp a b"] by blast
interpret FU_ac: inverse_simulations AC.resid ‹EXP a c›
‹Func a c› ‹Unfunc a c›
using a c inverse_simulations_Func_Unfunc [of a c] by blast
interpret Func_bcxB: product_simulation
‹EXP b c› ‹Rts b› BC.resid ‹Rts b›
‹Func b c› ‹I (Rts b)›
..
interpret UnpackxA: product_simulation
‹Rts (exp b c ⊗ exp a b)› ‹Rts a› bcxab.resid ‹Rts a›
‹Unpack (exp b c) (exp a b)› A.map ..
interpret Func_abxA: product_simulation
‹EXP a b› ‹Rts a› AB.resid ‹Rts a›
‹Func a b› ‹I (Rts a)›
..
interpret Func_bcxFunc_ab_x_A: product_simulation
bcxab.resid ‹Rts a› BCxAB.resid ‹Rts a›
Func_bcxFunc_ab.map A.map ..
interpret Func_bc_x_Func_abxA: product_simulation
‹EXP b c› abxA.resid BC.resid ABxA.resid
‹Func b c› Func_abxA.map ..
interpret E_AB: RTSConstructions.evaluation_map ‹Rts a› ‹Rts b› ..
interpret E_BC: RTSConstructions.evaluation_map ‹Rts b› ‹Rts c› ..
interpret BCxE_AB: product_simulation BC.resid ABxA.resid
BC.resid ‹Rts b› BC.map E_AB.map ..
interpret E_ABoFunc_abxA: composite_simulation
abxA.resid ABxA.resid ‹Rts b›
Func_abxA.map E_AB.map ..
interpret bc_x_E_ABoFunc_abxA: product_simulation
‹EXP b c› abxA.resid ‹EXP b c› ‹Rts b›
bc.map ‹E_AB.map ∘ Func_abxA.map› ..
have bc_map: "bc.map ∘ bc.map = bc.map"
by auto
have 1: "«eval b c ⋅ (exp b c ⊗ eval a b) ⋅ 𝖺[exp b c, exp a b, a] :
(exp b c ⊗ exp a b) ⊗ a → c»"
using a b c eval_in_hom_ax [of b c] eval_in_hom_ax [of a b] ide_exp_ax
by fastforce
have "Func a c ∘ Map (ECMC.Comp a b c) =
Func a c ∘ Map (curry (exp b c ⊗ exp a b) a c
(eval b c ⋅ (exp b c ⊗ eval a b) ⋅
𝖺[exp b c, exp a b, a]))"
unfolding ECMC.Comp_def
using Assoc_bc_ab_a.a Assoc_bc_ab_a.b a assoc_agreement by auto
also have "... = Func a c ∘
Unfunc a c ∘
COMP.Currying.E.coext (Rts (exp b c ⊗ exp a b))
(Map (eval b c ⋅ (exp b c ⊗ eval a b) ⋅
𝖺[exp b c, exp a b, a]) ∘
Pack (exp b c ⊗ exp a b) a)"
proof -
have "ide (exp b c ⊗ exp a b)"
using a b c ide_exp_ax by blast
moreover have "«eval b c ⋅ (exp b c ⊗ eval a b) ⋅
𝖺[exp b c, exp a b, a] :
(exp b c ⊗ exp a b) ⊗ a → c»"
using a b c eval_in_hom_ax eval_in_hom_ax ide_exp_ax
by fastforce
ultimately show ?thesis
using a Map_curry fun.map_comp by auto
qed
also have "... = I AC.resid ∘
COMP.Currying.E.coext (Rts (exp b c ⊗ exp a b))
(Map (eval b c ⋅ (exp b c ⊗ eval a b) ⋅
𝖺[exp b c, exp a b, a]) ∘
Pack (exp b c ⊗ exp a b) a)"
using FU_ac.inv' by simp
also have "... = I AC.resid ∘
COMP.Currying.E.coext (Rts (exp b c ⊗ exp a b))
(Map (eval b c) ∘
Map (exp b c ⊗ eval a b) ∘
Map 𝖺[exp b c, exp a b, a] ∘
Pack (exp b c ⊗ exp a b) a)"
proof -
have "Map (eval b c ⋅ (exp b c ⊗ eval a b) ⋅ 𝖺[exp b c, exp a b, a]) =
Map (eval b c) ∘ Map (exp b c ⊗ eval a b) ∘ Map 𝖺[exp b c, exp a b, a]"
using 1 Map_comp by fastforce
thus ?thesis by auto
qed
also have "... = COMP.Currying.E.coext (Rts (exp b c ⊗ exp a b))
(E_BC.map ∘ Func_bcxB.map ∘ Unpack (exp b c) b ∘
Map (exp b c ⊗ eval a b) ∘
Map 𝖺[exp b c, exp a b, a] ∘
Pack (exp b c ⊗ exp a b) a)"
proof -
have "simulation bcxab'_x_A.resid (Rts c)
(Map (eval b c) ∘
Map (exp b c ⊗ eval a b) ∘
Map 𝖺[exp b c, exp a b, a] ∘
Pack (exp b c ⊗ exp a b) a)"
proof (intro simulation_comp)
show "simulation (Rts (exp b c ⊗ b)) (Rts c) (Map (eval b c))"
using a b c eval_in_hom_ax [of b c] arrD(3) by force
show "simulation (Rts (exp b c ⊗ exp a b ⊗ a)) (Rts (exp b c ⊗ b))
(Map (exp b c ⊗ eval a b))"
proof -
have "«exp b c ⊗ eval a b : exp b c ⊗ exp a b ⊗ a → exp b c ⊗ b»"
using a b c Assoc_bc_ab_a.a eval_in_hom_ax eval_in_hom_ax
by auto
thus ?thesis
using arrD(3) by fastforce
qed
show "simulation bcxab'_x_A.resid (Rts ((exp b c ⊗ exp a b) ⊗ a))
(Pack (exp b c ⊗ exp a b) a)"
using a b c PU_bcxab_xa.F.simulation_axioms by blast
show "simulation (Rts ((exp b c ⊗ exp a b) ⊗ a))
(Rts (exp b c ⊗ exp a b ⊗ a))
(Map 𝖺[exp b c, exp a b, a])"
using a b c ide_exp_ax arrD(3) [of "𝖺[exp b c, exp a b, a]"] by auto
qed
moreover have "Currying (Rts (exp b c ⊗ exp a b)) (Rts a) (Rts c)" ..
ultimately have "simulation (Rts (exp b c ⊗ exp a b)) AC.resid
(COMP.Currying.E.coext (Rts (exp b c ⊗ exp a b))
(Map (eval b c) ∘
Map (exp b c ⊗ eval a b) ∘
Map 𝖺[exp b c, exp a b, a] ∘
Pack (exp b c ⊗ exp a b) a))"
using Currying.Curry_preserves_simulations by fastforce
thus ?thesis
using b c Assoc_abc.Map_assoc Map_eval comp_identity_simulation
by auto
qed
also have "... = COMP.Currying.E.coext (Rts (exp b c ⊗ exp a b))
(E_BC.map ∘ Func_bcxB.map ∘ Unpack (exp b c) b ∘
(Pack (exp b c) b ∘
bcxeval.map ∘
Unpack (dom (exp b c)) (dom (eval a b))) ∘
Map 𝖺[exp b c, exp a b, a] ∘
Pack (exp b c ⊗ exp a b) a)"
proof -
have "bcxeval.map = product_simulation.map
(Dom (exp b c)) (Dom (eval a b))
(Map (exp b c)) (Map (eval a b))"
proof -
have "Dom (eval a b) = Rts (exp a b ⊗ a)"
using a b eval_in_hom_ax by fastforce
thus ?thesis
using a b c Map_ide ide_exp_ax by auto
qed
hence "Map (exp b c ⊗ eval a b) =
Pack (exp b c) b ∘
bcxeval.map ∘
Unpack (dom (exp b c)) (dom (eval a b))"
using a b c Map_prod ide_exp_ax eval_in_hom_ax by fastforce
thus ?thesis by simp
qed
also have "... = COMP.Currying.E.coext (Rts (exp b c ⊗ exp a b))
(E_BC.map ∘ Func_bcxB.map ∘ Unpack (exp b c) b ∘
(Pack (exp b c) b ∘
bcxeval.map ∘
Unpack (exp b c) (exp a b ⊗ a)) ∘
Map 𝖺[exp b c, exp a b, a] ∘
Pack (exp b c ⊗ exp a b) a)"
using a b c ide_exp_ax eval_in_hom_ax by auto
also have "... = COMP.Currying.E.coext (Rts (exp b c ⊗ exp a b))
(E_BC.map ∘ (Func_bcxB.map ∘
(Unpack (exp b c) b ∘ Pack (exp b c) b)) ∘
bcxeval.map ∘
Unpack (exp b c) (exp a b ⊗ a) ∘
Map 𝖺[exp b c, exp a b, a] ∘
Pack (exp b c ⊗ exp a b) a)"
using fun.map_comp by metis
also have "... = COMP.Currying.E.coext (Rts (exp b c ⊗ exp a b))
(E_BC.map ∘ (Func_bcxB.map ∘ I bcxB.resid) ∘
bcxeval.map ∘
Unpack (exp b c) (exp a b ⊗ a) ∘
Map 𝖺[exp b c, exp a b, a] ∘
Pack (exp b c ⊗ exp a b) a)"
using b c Unpack_o_Pack ide_exp_ax by auto
also have "... = COMP.Currying.E.coext (Rts (exp b c ⊗ exp a b))
(E_BC.map ∘ Func_bcxB.map ∘
bcxeval.map ∘
Unpack (exp b c) (exp a b ⊗ a) ∘
Map 𝖺[exp b c, exp a b, a] ∘
Pack (exp b c ⊗ exp a b) a)"
using comp_simulation_identity [of bcxB.resid BCxB.resid Func_bcxB.map]
Func_bcxB.simulation_axioms
by auto
also have "... = COMP.Currying.E.coext (Rts (exp b c ⊗ exp a b))
(E_BC.map ∘ Func_bcxB.map ∘
product_simulation.map (EXP b c) (Rts (exp a b ⊗ a))
bc.map
(E_AB.map ∘ Func_abxA.map ∘ Unpack (exp a b) a) ∘
Unpack (exp b c) (exp a b ⊗ a) ∘
Map 𝖺[exp b c, exp a b, a] ∘
Pack (exp b c ⊗ exp a b) a)"
using a b c Map_eval eval_in_hom_ax by auto
also have "... = COMP.Currying.E.coext (Rts (exp b c ⊗ exp a b))
(E_BC.map ∘ Func_bcxB.map ∘
((product_simulation.map
(EXP b c) ABxA.resid bc.map E_AB.map ∘
product_simulation.map
(EXP b c) abxA.resid bc.map Func_abxA.map) ∘
product_simulation.map
(EXP b c) (Rts (exp a b ⊗ a))
bc.map (Unpack (exp a b) a)) ∘
Unpack (exp b c) (exp a b ⊗ a) ∘
Map 𝖺[exp b c, exp a b, a] ∘
Pack (exp b c ⊗ exp a b) a)"
proof -
have "product_simulation.map (EXP b c) (Rts (exp a b ⊗ a))
bc.map (E_AB.map ∘ Func_abxA.map ∘ Unpack (exp a b) a) =
product_simulation.map
(EXP b c) abxA.resid bc.map (E_AB.map ∘ Func_abxA.map) ∘
product_simulation.map
(EXP b c) (Rts (exp a b ⊗ a)) bc.map (Unpack (exp a b) a)"
using bc_map Func_abxA.simulation_axioms E_AB.simulation_axioms
bc.simulation_axioms E_ABoFunc_abxA.simulation_axioms
PU_abxa.G.simulation_axioms
simulation_interchange
[of "EXP b c" "EXP b c" bc.map
"Rts (exp a b ⊗ a)" abxA.resid "Unpack (exp a b) a"
"EXP b c" bc.map "Rts b" "E_AB.map ∘ Func_abxA.map"]
by simp
also have "... = product_simulation.map
(EXP b c) ABxA.resid bc.map E_AB.map ∘
product_simulation.map
(EXP b c) abxA.resid bc.map Func_abxA.map ∘
product_simulation.map (EXP b c) (Rts (exp a b ⊗ a))
bc.map (Unpack (exp a b) a)"
using a b c bc_map Func_abxA.simulation_axioms E_AB.simulation_axioms
bc.simulation_axioms
simulation_interchange
[of "EXP b c" "EXP b c" bc.map
abxA.resid ABxA.resid Func_abxA.map
"EXP b c" bc.map "Rts b" E_AB.map]
by simp
finally show ?thesis by simp
qed
also have "... = COMP.Currying.E.coext (Rts (exp b c ⊗ exp a b))
(E_BC.map ∘ Func_bcxB.map ∘
(bc_x_E_ABoFunc_abxA.map ∘
product_simulation.map (EXP b c) (Rts (exp a b ⊗ a))
bc.map (Unpack (exp a b) a)) ∘
Unpack (exp b c) (exp a b ⊗ a) ∘
Map 𝖺[exp b c, exp a b, a] ∘
Pack (exp b c ⊗ exp a b) a)"
using a b c E_AB.simulation_axioms Func_abxA.simulation_axioms
bc.simulation_axioms bc_map
simulation_interchange
[of "EXP b c" "EXP b c" bc.map
abxA.resid ABxA.resid Func_abxA.map
"EXP b c" bc.map "Rts b" E_AB.map]
by simp
also have "... = COMP.Currying.E.coext (Rts (exp b c ⊗ exp a b))
((E_BC.map ∘ Func_bcxB.map ∘
product_simulation.map
(EXP b c) abxA.resid
bc.map (E_AB.map ∘ Func_abxA.map)) ∘
(product_simulation.map
(EXP b c) (Rts (exp a b ⊗ a))
bc.map (Unpack (exp a b) a) ∘
Unpack (exp b c) (exp a b ⊗ a) ∘
Map 𝖺[exp b c, exp a b, a] ∘
Pack (exp b c ⊗ exp a b) a))"
proof -
have "E_BC.map ∘ Func_bcxB.map ∘
(product_simulation.map
(EXP b c) abxA.resid bc.map (E_AB.map ∘ Func_abxA.map) ∘
product_simulation.map
(EXP b c) (Rts (exp a b ⊗ a))
bc.map (Unpack (exp a b) a)) ∘
Unpack (exp b c) (exp a b ⊗ a) ∘
Map 𝖺[exp b c, exp a b, a] ∘
Pack (exp b c ⊗ exp a b) a =
(E_BC.map ∘ Func_bcxB.map ∘
product_simulation.map
(EXP b c) abxA.resid bc.map (E_AB.map ∘ Func_abxA.map)) ∘
(product_simulation.map
(EXP b c) (Rts (exp a b ⊗ a)) bc.map (Unpack (exp a b) a) ∘
Unpack (exp b c) (exp a b ⊗ a) ∘
Map 𝖺[exp b c, exp a b, a] ∘
Pack (exp b c ⊗ exp a b) a)"
using fun.map_comp by auto
thus ?thesis by simp
qed
also have "... = COMP.Currying.E.coext (Rts (exp b c ⊗ exp a b))
((E_BC.map ∘ Func_bcxB.map ∘ bc_x_E_ABoFunc_abxA.map) ∘
(Assoc_bc_ab_a.ASSOC.map ∘ UnpackxA.map))"
proof -
have "product_simulation.map
(EXP b c) (Rts (exp a b ⊗ a)) bc.map (Unpack (exp a b) a) ∘
Unpack (exp b c) (exp a b ⊗ a) ∘
Map 𝖺[exp b c, exp a b, a] ∘
Pack (exp b c ⊗ exp a b) a =
product_simulation.map
(EXP b c) (Rts (exp a b ⊗ a)) bc.map (Unpack (exp a b) a) ∘
Unpack (exp b c) (exp a b ⊗ a) ∘
(Pack (exp b c) (exp a b ⊗ a) ∘
product_simulation.map
(EXP b c) abxA.resid bc.map (Pack (exp a b) a) ∘
Assoc_bc_ab_a.ASSOC.map ∘
(UnpackxA.map ∘
Unpack (exp b c ⊗ exp a b) a)) ∘
Pack (exp b c ⊗ exp a b) a"
using Assoc_bc_ab_a.Map_assoc by simp
also have "... =
product_simulation.map
(EXP b c) (Rts (exp a b ⊗ a))
bc.map (Unpack (exp a b) a) ∘
(Unpack (exp b c) (exp a b ⊗ a) ∘ Pack (exp b c) (exp a b ⊗ a)) ∘
product_simulation.map
(EXP b c) abxA.resid bc.map (Pack (exp a b) a) ∘
Assoc_bc_ab_a.ASSOC.map ∘
(UnpackxA.map ∘
(Unpack (exp b c ⊗ exp a b) a ∘
Pack (exp b c ⊗ exp a b) a))"
using fun.map_comp by auto
also have "... = I bc_x_abxA.resid ∘
Assoc_bc_ab_a.ASSOC.map ∘
(UnpackxA.map ∘ I bcxab'_x_A.resid)"
proof -
have "product_simulation.map
(EXP b c) (Rts (exp a b ⊗ a))
bc.map (Unpack (exp a b) a) ∘
(Unpack (exp b c) (exp a b ⊗ a) ∘
Pack (exp b c) (exp a b ⊗ a)) ∘
product_simulation.map
(EXP b c) abxA.resid bc.map (Pack (exp a b) a) =
product_simulation.map
(EXP b c) (Rts (exp a b ⊗ a)) bc.map (Unpack (exp a b) a) ∘
(I bcxeval.A1xA0.resid) ∘
product_simulation.map
(EXP b c) abxA.resid bc.map (Pack (exp a b) a)"
using a b c Unpack_o_Pack [of "exp b c" "exp a b ⊗ a"] by force
also have "... = product_simulation.map
(EXP b c) (Rts (exp a b ⊗ a))
bc.map (Unpack (exp a b) a) ∘
product_simulation.map (EXP b c) abxA.resid
bc.map (Pack (exp a b) a)"
using comp_simulation_identity
[of bcxeval.A1xA0.resid bc_x_abxA.resid
"product_simulation.map (EXP b c) (Rts (exp a b ⊗ a))
bc.map (Unpack (exp a b) a)"]
Assoc_bc_ab_a.PU_Axbc.G.simulation_axioms
by fastforce
also have "... =
product_simulation.map
(EXP b c) abxA.resid (bc.map ∘ bc.map)
(Unpack (exp a b) a ∘ Pack (exp a b) a)"
using simulation_interchange
PU_abxa.F.simulation_axioms PU_abxa.G.simulation_axioms
bc.simulation_axioms
by fastforce
also have "... = product_simulation.map (EXP b c) abxA.resid
bc.map (I abxA.resid)"
using a b bc_map Unpack_o_Pack ide_exp_ax by simp
also have "... = I bc_x_abxA.resid"
using product_identity_simulation abxA.rts_axioms bc.rts_axioms
by fastforce
finally have "product_simulation.map
(EXP b c) (Rts (exp a b ⊗ a))
bc.map (Unpack (exp a b) a) ∘
(Unpack (exp b c) (exp a b ⊗ a) ∘
Pack (exp b c) (exp a b ⊗ a)) ∘
product_simulation.map
(EXP b c) abxA.resid bc.map (Pack (exp a b) a) =
I bc_x_abxA.resid"
by blast
moreover have "Unpack (exp b c ⊗ exp a b) a ∘
Pack (exp b c ⊗ exp a b) a =
I bcxab'_x_A.resid"
using a b c Unpack_o_Pack [of "exp b c ⊗ exp a b" a] by blast
ultimately show ?thesis by simp
qed
also have "... = Assoc_bc_ab_a.ASSOC.map ∘ UnpackxA.map"
using comp_identity_simulation [of _ bc_x_abxA.resid Assoc_bc_ab_a.ASSOC.map]
comp_simulation_identity [of bcxab'_x_A.resid _ UnpackxA.map]
Assoc_bc_ab_a.ASSOC.simulation_axioms UnpackxA.simulation_axioms
by simp
finally show ?thesis by simp
qed
also have "... =
COMP.Currying.E.coext (Rts (exp b c ⊗ exp a b))
(E_BC.map ∘ BCxE_AB.map ∘
(Func_bc_x_Func_abxA.map ∘ Assoc_bc_ab_a.ASSOC.map ∘
UnpackxA.map))"
proof -
have "E_BC.map ∘ Func_bcxB.map ∘ bc_x_E_ABoFunc_abxA.map =
E_BC.map ∘ Func_bcxB.map ∘
(product_simulation.map (EXP b c) ABxA.resid bc.map E_AB.map ∘
product_simulation.map (EXP b c) abxA.resid bc.map Func_abxA.map)"
using bc_map Func_abxA.simulation_axioms E_AB.simulation_axioms
bc.simulation_axioms
simulation_interchange
[of "EXP b c" "EXP b c" bc.map abxA.resid ABxA.resid Func_abxA.map
"EXP b c" bc.map "Rts b" E_AB.map]
by simp
also have "... = E_BC.map ∘
(Func_bcxB.map ∘
product_simulation.map (EXP b c) ABxA.resid
bc.map E_AB.map) ∘
product_simulation.map
(EXP b c) abxA.resid bc.map Func_abxA.map"
using fun.map_comp by auto
also have "... = E_BC.map ∘
(product_simulation.map
BC.resid ABxA.resid BC.map E_AB.map ∘
product_simulation.map
(EXP b c) ABxA.resid (Func b c) ABxA.map) ∘
product_simulation.map
(EXP b c) abxA.resid bc.map Func_abxA.map"
proof -
have "Func_bcxB.map ∘
product_simulation.map (EXP b c) ABxA.resid
bc.map E_AB.map =
product_simulation.map (EXP b c) ABxA.resid (Func b c) E_AB.map"
using simulation_interchange
[of "EXP b c" "EXP b c" bc.map ABxA.resid "Rts b" E_AB.map
BC.resid"Func b c" "Rts b" B.map]
E_AB.simulation_axioms Func_Unfunc_bc.G.simulation_axioms
B.simulation_axioms bc.simulation_axioms
comp_simulation_identity [of "EXP b c" BC.resid "Func b c"]
comp_identity_simulation [of ABxA.resid "Rts b" E_AB.map]
Func_Unfunc_bc.F.simulation_axioms
by auto
also have "... = product_simulation.map
BC.resid ABxA.resid BC.map E_AB.map ∘
product_simulation.map
(EXP b c) ABxA.resid (Func b c) ABxA.map"
using ABxA.simulation_axioms BC.simulation_axioms
E_AB.simulation_axioms Func_Unfunc_bc.G.simulation_axioms
comp_simulation_identity [of ABxA.resid "Rts b" E_AB.map]
comp_identity_simulation [of "EXP b c" BC.resid "Func b c"]
simulation_interchange
[of "EXP b c" BC.resid "Func b c"
ABxA.resid ABxA.resid ABxA.map
BC.resid BC.map "Rts b" E_AB.map]
Func_Unfunc_bc.F.simulation_axioms
by auto
finally have "Func_bcxB.map ∘
product_simulation.map (EXP b c) ABxA.resid
bc.map E_AB.map =
BCxE_AB.map ∘
product_simulation.map (EXP b c) ABxA.resid
(Func b c) ABxA.map"
by blast
thus ?thesis by simp
qed
also have "... = E_BC.map ∘
(product_simulation.map BC.resid ABxA.resid
BC.map E_AB.map) ∘
(product_simulation.map
(EXP b c) ABxA.resid (Func b c) ABxA.map ∘
product_simulation.map
(EXP b c) abxA.resid bc.map Func_abxA.map)"
using fun.map_comp by auto
also have "... = E_BC.map ∘ BCxE_AB.map ∘ Func_bc_x_Func_abxA.map"
using simulation_interchange
[of "EXP b c" "EXP b c" bc.map abxA.resid ABxA.resid Func_abxA.map
BC.resid "Func b c" ABxA.resid ABxA.map]
bc.simulation_axioms Func_abxA.simulation_axioms ABxA.simulation_axioms
Func_Unfunc_bc.G.simulation_axioms
comp_simulation_identity [of _ _ "Func b c"]
comp_identity_simulation [of _ ABxA.resid Func_abxA.map]
Func_Unfunc_bc.F.simulation_axioms
by auto
finally have "E_BC.map ∘ Func_bcxB.map ∘ bc_x_E_ABoFunc_abxA.map =
E_BC.map ∘ BCxE_AB.map ∘ Func_bc_x_Func_abxA.map"
by blast
thus ?thesis
using fun.map_comp by metis
qed
also have "... = COMP.Currying.E.coext (Rts (exp b c ⊗ exp a b))
(E_BC.map ∘ BCxE_AB.map ∘ ASSOC.map ∘
(Func_bcxFunc_ab_x_A.map ∘ UnpackxA.map))"
proof -
have 1: "Func_bc_x_Func_abxA.map ∘ Assoc_bc_ab_a.ASSOC.map =
ASSOC.map ∘ Func_bcxFunc_ab_x_A.map"
proof -
have "Func_bc_x_Func_abxA.map ∘ Assoc_bc_ab_a.ASSOC.map =
Func_bc_x_Func_abxA.map ∘
⟨⟨bcxab.P⇩1 ∘ bcxab_x_A.P⇩1,
AxB.tuple (bcxab.P⇩0 ∘ bcxab_x_A.P⇩1) bcxab_x_A.P⇩0⟩⟩"
unfolding Assoc_bc_ab_a.ASSOC.map_def by blast
also have "... = ⟨⟨Func b c ∘ (bcxab.P⇩1 ∘ bcxab_x_A.P⇩1),
Func_abxA.map ∘
(AxB.tuple (bcxab.P⇩0 ∘ bcxab_x_A.P⇩1) bcxab_x_A.P⇩0)⟩⟩"
using comp_product_simulation_tuple
[of "EXP b c" BC.resid "Func b c" abxA.resid ABxA.resid
Func_abxA.map bcxab_x_A.resid "bcxab.P⇩1 ∘ bcxab_x_A.P⇩1"
"AxB.tuple (bcxab.P⇩0 ∘ bcxab_x_A.P⇩1) bcxab_x_A.P⇩0"]
Func_Unfunc_bc.F.simulation_axioms Func_abxA.simulation_axioms
bcxab_x_A.P⇩1.simulation_axioms bcxab_x_A.P⇩0.simulation_axioms
bcxab.P⇩1.simulation_axioms bcxab.P⇩0.simulation_axioms
simulation_comp simulation_tuple
by auto
also have "... = ⟨⟨Func b c ∘ (bcxab.P⇩1 ∘ bcxab_x_A.P⇩1),
⟨⟨Func a b ∘ (bcxab.P⇩0 ∘ bcxab_x_A.P⇩1),
bcxab_x_A.P⇩0⟩⟩ ⟩⟩"
using comp_product_simulation_tuple
[of "EXP a b" AB.resid "Func a b" "Rts a" "Rts a" A.map
bcxab_x_A.resid "bcxab.P⇩0 ∘ bcxab_x_A.P⇩1" bcxab_x_A.P⇩0]
comp_identity_simulation [of bcxab_x_A.resid "Rts a" bcxab_x_A.P⇩0]
A.simulation_axioms Func_Unfunc_ab.F.simulation_axioms
bcxab.P⇩0.simulation_axioms bcxab_x_A.P⇩0.simulation_axioms
bcxab_x_A.P⇩1.simulation_axioms
simulation_comp [of _ _ bcxab_x_A.P⇩1 _ bcxab.P⇩0]
by simp
also have "... = ⟨⟨BCxAB.P⇩1 ∘ BCxAB_x_A.P⇩1 ∘ Func_bcxFunc_ab_x_A.map,
⟨⟨BCxAB.P⇩0 ∘ BCxAB_x_A.P⇩1 ∘ Func_bcxFunc_ab_x_A.map,
BCxAB_x_A.P⇩0 ∘ Func_bcxFunc_ab_x_A.map⟩⟩ ⟩⟩"
proof -
have "Func b c ∘ (bcxab.P⇩1 ∘ bcxab_x_A.P⇩1) =
BCxAB.P⇩1 ∘ BCxAB_x_A.P⇩1 ∘ Func_bcxFunc_ab_x_A.map"
using Func_Unfunc_bc.F.extensional BCxAB_x_A.P⇩1.extensional
bcxab_x_A.map_def bcxab_x_A.P⇩1_def bcxab.P⇩1_def
Func_bcxFunc_ab_x_A.map_def Func_bcxFunc_ab.map_def
BCxAB_x_A.P⇩1_def BCxAB.P⇩1_def
by auto
moreover have "Func a b ∘ (bcxab.P⇩0 ∘ bcxab_x_A.P⇩1) =
(BCxAB.P⇩0 ∘ BCxAB_x_A.P⇩1) ∘ Func_bcxFunc_ab_x_A.map"
using BCxAB.P⇩0_def BCxAB_x_A.P⇩1_def bcxab.P⇩0_def bcxab_x_A.P⇩1_def
Func_bcxFunc_ab_x_A.map_def Func_bcxFunc_ab.map_def
Func_bcxFunc_ab_x_A.extensional Func_Unfunc_ab.F.extensional
by auto
moreover have "bcxab_x_A.P⇩0 =
BCxAB_x_A.P⇩0 ∘ Func_bcxFunc_ab_x_A.map"
using BCxAB.P⇩0_def BCxAB_x_A.P⇩0_def bcxab_x_A.P⇩0_def
Func_bcxFunc_ab_x_A.map_def Func_bcxFunc_ab.map_def
Func_bcxFunc_ab_x_A.extensional
by auto
ultimately show ?thesis by simp
qed
also have "... = ⟨⟨BCxAB.P⇩1 ∘ BCxAB_x_A.P⇩1,
⟨⟨BCxAB.P⇩0 ∘ BCxAB_x_A.P⇩1, BCxAB_x_A.P⇩0⟩⟩ ⟩⟩ ∘
Func_bcxFunc_ab_x_A.map"
by (simp add: comp_pointwise_tuple)
also have "... = ASSOC.map ∘ Func_bcxFunc_ab_x_A.map"
unfolding ASSOC.map_def by simp
finally show ?thesis by blast
qed
have "COMP.E_BC_o_BCxE_AB.map ∘
(Func_bc_x_Func_abxA.map ∘ Assoc_bc_ab_a.ASSOC.map ∘
UnpackxA.map) =
COMP.E_BC_o_BCxE_AB.map ∘
(ASSOC.map ∘ Func_bcxFunc_ab_x_A.map ∘ UnpackxA.map)"
using 1 by simp
also have "... = COMP.E_BC_o_BCxE_AB.map ∘ ASSOC.map ∘
(Func_bcxFunc_ab_x_A.map ∘ UnpackxA.map)"
by auto
finally show ?thesis by simp
qed
also have "... = COMP.Currying.E.coext BCxAB.resid
(E_BC.map ∘ BCxE_AB.map ∘ ASSOC.map) ∘
(Func_bcxFunc_ab.map ∘ Unpack (exp b c) (exp a b))"
proof -
have "COMP.Currying.E.coext (Rts (exp b c ⊗ exp a b))
(COMP.E_BC_o_BCxE_AB.map ∘ ASSOC.map ∘
(Func_bcxFunc_ab_x_A.map ∘ UnpackxA.map)) =
COMP.Currying.E.coext (Rts (exp b c ⊗ exp a b))
(COMP.E_BC_o_BCxE_AB.map ∘ ASSOC.map ∘
(product_simulation.map (Rts (exp b c ⊗ exp a b)) (Rts a)
(Func_bcxFunc_ab.map ∘ Unpack (exp b c) (exp a b)) A.map))"
proof -
have "A.map ∘ A.map = A.map"
using comp_identity_simulation [of "Rts a" "Rts a" A.map]
A.simulation_axioms
by simp
hence "Func_bcxFunc_ab_x_A.map ∘ UnpackxA.map =
product_simulation.map (Rts (exp b c ⊗ exp a b)) (Rts a)
(Func_bcxFunc_ab.map ∘ Unpack (exp b c) (exp a b)) A.map"
using simulation_interchange
[of "Rts (exp b c ⊗ exp a b)" bcxab.resid
"Unpack (exp b c) (exp a b)"
"Rts a" "Rts a" A.map BCxAB.resid Func_bcxFunc_ab.map
"Rts a" A.map]
Func_bcxFunc_ab.simulation_axioms PU_bcxab.G.simulation_axioms
A.simulation_axioms
by simp
thus ?thesis by simp
qed
also have "... = COMP.Currying.E.coext BCxAB.resid
(E_BC.map ∘ BCxE_AB.map ∘ ASSOC.map) ∘
(Func_bcxFunc_ab.map ∘ Unpack (exp b c) (exp a b))"
proof -
have "simulation (Rts (exp b c ⊗ exp a b)) BCxAB.resid
(Func_bcxFunc_ab.map ∘ Unpack (exp b c) (exp a b))"
using simulation_comp Func_bcxFunc_ab.simulation_axioms
PU_bcxab.G.simulation_axioms
by auto
moreover have "simulation BCxAB_x_A.resid (Rts c)
(COMP.E_BC_o_BCxE_AB.map ∘ ASSOC.map)"
using simulation_comp COMP.E_BC_o_BCxE_AB.simulation_axioms
ASSOC.simulation_axioms
by auto
ultimately show ?thesis
using COMP.Currying.E.comp_coext_simulation
[of "Rts (exp b c ⊗ exp a b)" BCxAB.resid
"Func_bcxFunc_ab.map ∘ Unpack (exp b c) (exp a b)"
"E_BC.map ∘ BCxE_AB.map ∘ ASSOC.map"]
BCxAB.weakly_extensional_rts_axioms
bcxab'.weakly_extensional_rts_axioms
by fastforce
qed
finally show ?thesis by blast
qed
also have "... = COMP.map ∘
(Func_bcxFunc_ab.map ∘ Unpack (exp b c) (exp a b))"
unfolding COMP.map_def by simp
finally show ?thesis by simp
qed
text ‹
We obtain as a corollary an explicit formula for ‹Map (Comp a b c)› in terms of
the external compositor ‹COMP.map› and packing and unpacking isomorphisms.
›
corollary Map_Comp:
shows "Map (ECMC.Comp a b c) =
Unfunc a c ∘ COMP.map ∘
(Func_bcxFunc_ab.map ∘ Unpack (exp b c) (exp a b))"
proof -
have "Map (ECMC.Comp a b c) =
I (EXP a c) ∘ Map (ECMC.Comp a b c)"
using a b c ECMC.Comp_in_hom arrD(3) [of "ECMC.Comp a b c"]
comp_identity_simulation
[of "Rts (exp b c ⊗ exp a b)" "EXP a c" "Map (ECMC.Comp a b c)"]
by simp
also have "... = Unfunc a c ∘ Func a c ∘ Map (ECMC.Comp a b c)"
using a c Unfunc_o_Func by simp
also have "... = Unfunc a c ∘ (Func a c ∘ Map (ECMC.Comp a b c))"
by auto
also have "... = Unfunc a c ∘
COMP.map ∘
(Func_bcxFunc_ab.map ∘ Unpack (exp b c) (exp a b))"
using Func_o_Map_Comp by auto
finally show ?thesis by blast
qed
end
context rtscat
begin
abbreviation EXP
where "EXP ≡ λa b. Rts (exp a b)"
proposition Map_Comp:
assumes "ide a" and "ide b" and "ide c"
shows "Map (ECMC.Comp a b c) =
Unfunc a c ∘ COMP.map (Rts a) (Rts b) (Rts c) ∘
(product_simulation.map (EXP b c) (EXP a b)
(Func b c) (Func a b) ∘
Unpack (exp b c) (exp a b))"
proof -
interpret Comp: Composition
using assms by unfold_locales
show ?thesis
using Comp.Map_Comp by blast
qed
end
end