Theory RTSCatx
section "The RTS-Category of RTS's and Transformations"
theory RTSCatx
imports Main ConcreteRTSCategory
begin
text‹
In this section we apply the @{locale concrete_rts_category} construction to create an
RTS-category, taking the set of all small extensional RTS's at a given arrow type as
the objects and the exponential RTS's formed from these as the hom's, so that the
arrows correspond to transformations and the arrows that are identities with respect to
the residuation correspond to simulations. We prove that the resulting category,
which we will refer to in informal text as ‹❙R❙T❙S⇧†›, is cartesian closed.
For that to hold, we need to start with the assumption that the underlying arrow type
is a universe.
›
locale rtscatx =
universe arr_type
for arr_type :: "'A itself"
begin
sublocale concrete_rts_category
‹TYPE('A resid)› ‹TYPE(('A, 'A) exponential_rts.arr)›
‹Collect extensional_rts ∩ Collect small_rts›
‹λA B. exponential_rts.resid A B›
‹λA. exponential_rts.MkArr (I A) (I A) (I A)›
‹λA B C f g. COMP.map A B C (f, g)›
proof (intro concrete_rts_category.intro)
show "⋀A B. ⟦A ∈ Collect extensional_rts ∩ Collect small_rts;
B ∈ Collect extensional_rts ∩ Collect small_rts⟧
⟹ extensional_rts (exponential_rts.resid A B)"
by (metis CollectD Int_Collect exponential_rts.intro
exponential_rts.is_extensional_rts extensional_rts.extensional
small_rts.axioms(1) weakly_extensional_rts.intro
weakly_extensional_rts_axioms.intro)
show "⋀A. A ∈ Collect extensional_rts ∩ Collect small_rts ⟹
residuation.ide (exponential_rts.resid A A)
(exponential_rts.MkArr (I A) (I A) (I A))"
proof -
fix A :: "'a resid"
assume A: "A ∈ Collect extensional_rts ∩ Collect small_rts"
show "residuation.ide (exponential_rts.resid A A)
(exponential_rts.MkIde (I A))"
proof -
interpret A: extensional_rts A using A by blast
interpret I: identity_simulation A ..
interpret AA: exponential_rts A A ..
show "AA.ide (AA.MkIde (I A))"
using AA.ide_MkIde I.simulation_axioms by blast
qed
qed
fix A :: "'a resid" and B :: "'a resid"
assume A: "A ∈ Collect extensional_rts ∩ Collect small_rts"
and B: "B ∈ Collect extensional_rts ∩ Collect small_rts"
interpret A: extensional_rts A using A by blast
interpret B: extensional_rts B using B by blast
interpret IA: identity_simulation A ..
interpret IA: simulation_as_transformation A A ‹I A› ..
interpret IB: identity_simulation B ..
interpret IB: simulation_as_transformation B B ‹I B› ..
interpret AA: exponential_rts A A ..
interpret BB: exponential_rts B B ..
interpret AB: exponential_rts A B ..
interpret Cmp_AAB: COMP A A B ..
interpret Cmp_ABB: COMP A B B ..
show "⋀t. AB.arr t ⟹ Cmp_AAB.map (t, AA.MkIde (I A)) = t"
proof -
fix t
assume t: "AB.arr t"
interpret t: transformation A B ‹AB.Dom t› ‹AB.Cod t› ‹AB.Map t›
using t AB.arr_char by blast
show "Cmp_AAB.map (t, AA.MkIde (I A)) = t"
proof -
have "AB.Dom t ∘ AA.Dom (AA.MkIde (I A)) = AB.Dom t"
using t.F.simulation_axioms comp_simulation_identity by auto
moreover have "AB.Cod t ∘ AA.Cod (AA.MkIde (I A)) = AB.Cod t"
using t.G.simulation_axioms comp_simulation_identity by auto
moreover have "AB.Map t ∘ AA.Map (AA.MkIde (I A)) = AB.Map t"
using t.extensional by auto
ultimately show ?thesis
using t Cmp_AAB.map_eq AB.MkArr_Map AB.arr_char
IA.transformation_axioms
by auto
qed
qed
show "⋀u. AB.arr u ⟹ Cmp_ABB.map (BB.MkIde (I B), u) = u"
proof -
fix u
assume u: "AB.arr u"
interpret u: transformation A B ‹AB.Dom u› ‹AB.Cod u› ‹AB.Map u›
using u AB.arr_char by blast
show "Cmp_ABB.map (BB.MkIde (I B), u) = u"
proof -
have "BB.Dom (BB.MkIde (I B)) ∘ AB.Dom u = AB.Dom u"
using u.F.simulation_axioms comp_identity_simulation by auto
moreover have "BB.Cod (BB.MkIde (I B)) ∘ AB.Cod u = AB.Cod u"
using u.G.simulation_axioms comp_identity_simulation by auto
moreover have "BB.Map (BB.MkIde (I B)) ∘ AB.Map u = AB.Map u"
proof
fix x
show "(BB.Map (BB.MkIde (I B)) ∘ AB.Map u) x = AB.Map u x"
using u.extensional u.preserves_arr by auto metis
qed
ultimately show ?thesis
using u Cmp_ABB.map_eq AB.MkArr_Map AB.arr_char
IB.transformation_axioms
by auto
qed
qed
fix C :: "'a resid"
assume C: "C ∈ Collect extensional_rts ∩ Collect small_rts"
interpret C: extensional_rts C using C by blast
interpret BC: exponential_rts B C ..
interpret AC: exponential_rts A C ..
interpret BCxAB: product_rts BC.resid AB.resid ..
interpret Cmp_ABC: COMP A B C ..
show "binary_simulation BC.resid AB.resid AC.resid
(λ(t, u). Cmp_ABC.map (t, u))"
using Cmp_ABC.simulation_axioms BCxAB.product_rts_axioms
BC.rts_axioms AB.rts_axioms AC.rts_axioms binary_simulation.intro
by auto
fix D :: "'a resid"
assume D: "D ∈ Collect extensional_rts ∩ Collect small_rts"
interpret D: extensional_rts D using D by blast
interpret BD: exponential_rts B D ..
interpret CD: exponential_rts C D ..
interpret Cmp_ABD: COMP A B D ..
interpret Cmp_BCD: COMP B C D ..
interpret Cmp_ACD: COMP A C D ..
show "⋀t u v. ⟦CD.arr t; BC.arr u; AB.arr v⟧ ⟹
COMP.map A B D (COMP.map B C D (t, u), v) =
COMP.map A C D (t, COMP.map A B C (u, v))"
proof -
fix t u v
assume t: "CD.arr t" and u: "BC.arr u" and v: "AB.arr v"
have "transformation A C
(AC.Dom u ∘ AC.Dom v) (AC.Cod u ∘ AC.Cod v)
(AC.Map u ∘ AC.Map v)"
using t u v Preliminaries.horizontal_composite
by (metis A.extensional_rts_axioms AB.arrE B.extensional_rts_axioms
BC.arrE C.extensional_rts_axioms)
moreover
have "transformation B D
(BD.Dom t ∘ BD.Dom u) (BD.Cod t ∘ BD.Cod u)
(BD.Map t ∘ BD.Map u)"
using t u v Preliminaries.horizontal_composite
by (metis B.extensional_rts_axioms BC.arrE C.extensional_rts_axioms
CD.arrE D.extensional_rts_axioms)
ultimately
show "COMP.map A B D (COMP.map B C D (t, u), v) =
COMP.map A C D (t, COMP.map A B C (u, v))"
using t u v Cmp_ABD.map_eq Cmp_BCD.map_eq Cmp_ACD.map_eq
Cmp_ABC.map_eq
by auto
qed
qed
type_synonym 'a arr =
"('a resid, ('a, 'a) exponential_rts.arr) concrete_rts_category.arr"
notation resid (infix "\\" 70)
notation hcomp (infixr "⋆" 53)
text‹
The mapping @{term Trn} that takes arrow ‹t ∈ H.hom a b› to the underlying transition of the
exponential RTS ‹[Dom a, Dom b]›, is injective.
›
lemma inj_Trn:
assumes "obj a" and "obj b"
shows "Trn ∈ H.hom a b →
Collect (residuation.arr (exponential_rts.resid (Dom a) (Dom b)))"
and "inj_on Trn (H.hom a b)"
proof
interpret A: extensional_rts ‹Dom a›
using assms obj_char arr_char by blast
interpret B: extensional_rts ‹Dom b›
using assms obj_char arr_char by blast
interpret AB: exponential_rts ‹Dom a› ‹Dom b› ..
show "⋀x. x ∈ H.hom a b ⟹ Trn x ∈ Collect AB.arr"
using assms arr_char H.in_homE by auto
show "inj_on Trn (H.hom a b)"
proof
fix t u
assume t: "t ∈ H.hom a b" and u: "u ∈ H.hom a b"
assume tu: "Trn t = Trn u"
show "t = u"
using t u tu AB.arr_eqI
apply auto[1]
by (metis H.comp_arr_dom H.comp_cod_arr H.in_homE H_seq_char
MkArr_Trn)
qed
qed
sublocale locally_small_rts_category resid hcomp
proof
fix a b
assume a: "obj a" and b: "obj b"
interpret A: extensional_rts ‹Dom a›
using a obj_char arr_char by blast
interpret A: small_rts ‹Dom a›
using a obj_char arr_char by blast
interpret B: extensional_rts ‹Dom b›
using b obj_char arr_char by blast
interpret B: small_rts ‹Dom b›
using b obj_char arr_char by blast
interpret AB: exponential_of_small_rts ‹Dom a› ‹Dom b› ..
have "Trn ` H.hom a b ⊆ Collect AB.arr"
using H_arr_char image_subset_iff by auto
moreover have "inj_on Trn (H.hom a b)"
using a b inj_Trn by blast
ultimately show "small (H.hom a b)"
using a b AB.small smaller_than_small small_image_iff inj_Trn by metis
qed
abbreviation sta_in_hom ("«_ : _ →⇩s⇩t⇩a _»")
where "sta_in_hom f a b ≡ H.in_hom f a b ∧ sta f"
abbreviation trn_to ("«_ : _ ⇒ _»")
where "trn_to t f g ≡ arr t ∧ src t = f ∧ trg t = g"
definition mkarr :: "'A resid ⇒ 'A resid ⇒
('A ⇒ 'A) ⇒ ('A ⇒ 'A) ⇒ ('A ⇒ 'A) ⇒
'A arr"
where "mkarr A B F G τ ≡
MkArr A B (exponential_rts.MkArr F G τ)"
abbreviation mksta
where "mksta A B F ≡ mkarr A B F F F"
lemma Dom_mkarr [simp]:
shows "Dom (mkarr A B F G τ) = A"
unfolding mkarr_def by simp
lemma Cod_mkarr [simp]:
shows "Cod (mkarr A B F G τ) = B"
unfolding mkarr_def by simp
lemma arr_mkarr [intro]:
assumes "small_rts A" and "extensional_rts A"
and "small_rts B" and "extensional_rts B"
and "transformation A B F G τ"
shows "arr (mkarr A B F G τ)"
and "src (mkarr A B F G τ) = mksta A B F"
and "trg (mkarr A B F G τ) = mksta A B G"
and "dom (mkarr A B F G τ) = mkobj A"
and "cod (mkarr A B F G τ) = mkobj B"
proof -
interpret A: extensional_rts A
using assms by simp
interpret B: extensional_rts B
using assms by simp
interpret AB: exponential_rts A B ..
interpret τ: transformation A B F G τ
using assms(5) by blast
show 1: "arr (mkarr A B F G τ)"
unfolding mkarr_def
using assms arr_char by auto
show "src (mkarr A B F G τ) = mksta A B F"
and "trg (mkarr A B F G τ) = mksta A B G"
and "dom (mkarr A B F G τ) = mkobj A"
and "cod (mkarr A B F G τ) = mkobj B"
unfolding mkarr_def
using assms 1 src_char trg_char AB.src_char AB.trg_char
dom_char cod_char
by auto
qed
lemma mkarr_simps [simp]:
assumes "arr (mkarr A B F G σ)"
shows "dom (mkarr A B F G σ) = mkobj A"
and "cod (mkarr A B F G σ) = mkobj B"
and "src (mkarr A B F G σ) = mksta A B F"
and "trg (mkarr A B F G σ) = mksta A B G"
using assms arr_mkarr dom_char cod_char apply auto[4]
by (metis (no_types, lifting) Cod_mkarr CollectD Dom_mkarr Int_Collect
Trn.simps(1) arrE exponential_rts.arr_MkArr exponential_rts.intro
extensional_rts.axioms(1) extensional_rts.extensional mkarr_def
weakly_extensional_rts.intro weakly_extensional_rts_axioms.intro)+
lemma sta_mksta [intro]:
assumes "small_rts A" and "extensional_rts A"
and "small_rts B" and "extensional_rts B"
and "simulation A B F"
shows "sta (mksta A B F)"
and "dom (mksta A B F) = mkobj A" and "cod (mksta A B F) = mkobj B"
proof -
interpret A: extensional_rts A
using assms by blast
interpret B: extensional_rts B
using assms by blast
interpret F: simulation A B F
using assms by blast
interpret F: simulation_as_transformation A B F ..
show "sta (mksta A B F)"
using assms F.transformation_axioms arr_mkarr V.ide_iff_src_self
by presburger
show "dom (mksta A B F) = mkobj A"
using assms F.transformation_axioms arr_mkarr(4) by blast
show "cod (mksta A B F) = mkobj B"
using assms F.transformation_axioms arr_mkarr(5) by blast
qed
abbreviation Src
where "Src ≡ exponential_rts.Dom ∘ Trn"
abbreviation Trg
where "Trg ≡ exponential_rts.Cod ∘ Trn"
abbreviation Map
where "Map ≡ exponential_rts.Map ∘ Trn"
lemma Src_mkarr [simp]:
assumes "arr (mkarr A B F G σ)"
shows "Src (mkarr A B F G σ) = F"
using assms
by (metis (mono_tags, lifting) Int_Collect Trn.simps(1) arrE comp_apply
exponential_rts.Dom.simps(1) exponential_rts.intro
extensional_rts.axioms(1) extensional_rts.extensional mem_Collect_eq
mkarr_def weakly_extensional_rts.intro
weakly_extensional_rts_axioms.intro)
lemma Trg_mkarr [simp]:
assumes "arr (mkarr A B F G σ)"
shows "Trg (mkarr A B F G σ) = G"
using assms
by (metis (mono_tags, lifting) Int_Collect Trn.simps(1) arrE comp_apply
exponential_rts.Cod.simps(1) exponential_rts.intro
extensional_rts.axioms(1) extensional_rts.extensional mem_Collect_eq
mkarr_def weakly_extensional_rts.intro
weakly_extensional_rts_axioms.intro)
lemma Map_simps [simp]:
assumes "arr t"
shows "Map (dom t) = I (Dom t)"
and "Map (cod t) = I (Cod t)"
and "Map (src t) = Src t"
and "Map (trg t) = Trg t"
proof -
interpret A: extensional_rts ‹Dom t›
using assms arr_char by blast
interpret B: extensional_rts ‹Cod t›
using assms arr_char by blast
interpret AB: exponential_rts ‹Dom t› ‹Cod t› ..
show "Map (dom t) = I (Dom t)"
using assms dom_char by simp
show "Map (cod t) = I (Cod t)"
using assms cod_char by simp
show "Map (src t) = Src t"
using assms arr_char src_char by simp
show "Map (trg t) = Trg t"
using assms arr_char trg_char by simp
qed
lemma src_simp:
assumes "arr t"
shows "src t = mksta (Dom t) (Cod t) (Src t)"
proof -
interpret A: extensional_rts ‹Dom t›
using assms arr_char by blast
interpret B: extensional_rts ‹Cod t›
using assms arr_char by blast
interpret AB: exponential_rts ‹Dom t› ‹Cod t› ..
show ?thesis
using assms mkarr_def src_char AB.src_char by auto
qed
lemma trg_simp:
assumes "arr t"
shows "trg t = mksta (Dom t) (Cod t) (Trg t)"
proof -
interpret A: extensional_rts ‹Dom t›
using assms arr_char by blast
interpret B: extensional_rts ‹Cod t›
using assms arr_char by blast
interpret AB: exponential_rts ‹Dom t› ‹Cod t› ..
show ?thesis
using assms mkarr_def trg_char AB.trg_char by auto
qed
text‹
The mapping @{term Map} that takes a transition to its underlying transformation,
is a bijection, which cuts down to a bijection between states and simulations.
›
lemma bij_mkarr:
assumes "small_rts A" and "extensional_rts A"
and "small_rts B" and "extensional_rts B"
and "simulation A B F" and "simulation A B G"
shows "mkarr A B F G ∈ Collect (transformation A B F G)
→ {t. «t : mksta A B F ⇒ mksta A B G»}"
and "Map ∈ {t. «t : mksta A B F ⇒ mksta A B G»}
→ Collect (transformation A B F G)"
and [simp]: "Map (mkarr A B F G τ) = τ"
and [simp]: "t ∈ {t. «t : mksta A B F ⇒ mksta A B G»}
⟹ mkarr A B F G (Map t) = t"
and "bij_betw (mkarr A B F G) (Collect (transformation A B F G))
{t. «t : mksta A B F ⇒ mksta A B G»}"
and "bij_betw Map {t. «t : mksta A B F ⇒ mksta A B G»}
(Collect (transformation A B F G))"
proof -
interpret A: extensional_rts A
using assms by simp
interpret B: extensional_rts B
using assms by simp
interpret AB: exponential_rts A B ..
show 1: "mkarr A B F G ∈
Collect (transformation A B F G)
→ {t. «t : mksta A B F ⇒ mksta A B G»}"
using assms(1,3) src_char A.extensional_rts_axioms
B.extensional_rts_axioms arr_mkarr(1-3)
by auto
show 2: "Map ∈ {t. «t : mksta A B F ⇒ mksta A B G»}
→ Collect (transformation A B F G)"
using assms arr_char src_char trg_char mkarr_def
apply auto[1]
by (metis AB.Map.simps(1) AB.Map_src AB.Map_trg AB.arr_char)
show 3: "⋀τ. Map (mkarr A B F G τ) = τ"
using mkarr_def by simp
show 4: "⋀t. t ∈ {t. «t : mksta A B F ⇒ mksta A B G»}
⟹ mkarr A B F G (Map t) = t"
using AB.MkArr_Map AB.arr_char MkArr_Trn arr_char src_char trg_char
mkarr_def
apply auto[1]
by (metis AB.Map.simps(1) AB.Map_src AB.Map_trg)
show "bij_betw (mkarr A B F G) (Collect (transformation A B F G))
{t. «t : mksta A B F ⇒ mksta A B G»}"
using 1 2 3 4 by (intro bij_betwI)
show "bij_betw Map {t. «t : mksta A B F ⇒ mksta A B G»}
(Collect (transformation A B F G))"
using 1 2 3 4 by (intro bij_betwI)
qed
lemma bij_mksta:
assumes "small_rts A" and "extensional_rts A"
and "small_rts B" and "extensional_rts B"
shows "mksta A B ∈ Collect (simulation A B)
→ {t. «t : mkobj A →⇩s⇩t⇩a mkobj B»}"
and "Map ∈ {t. «t : mkobj A →⇩s⇩t⇩a mkobj B»}
→ Collect (simulation A B)"
and [simp]: "Map (mksta A B F) = F"
and [simp]: "t ∈ {t. «t : mkobj A →⇩s⇩t⇩a mkobj B»}
⟹ mksta A B (Map t) = t"
and "bij_betw (mksta A B) (Collect (simulation A B))
{t. «t : mkobj A →⇩s⇩t⇩a mkobj B»}"
and "bij_betw Map {t. «t : mkobj A →⇩s⇩t⇩a mkobj B»}
(Collect (simulation A B))"
proof -
interpret A: extensional_rts A
using assms by simp
interpret A: small_rts A
using assms by simp
interpret B: extensional_rts B
using assms by simp
interpret B: small_rts B
using assms by simp
interpret AB: exponential_rts A B ..
show 1: " mksta A B ∈ Collect (simulation A B)
→ {t. «t : mkobj A →⇩s⇩t⇩a mkobj B»}"
proof
fix F
assume F: "F ∈ Collect (simulation A B)"
interpret F: simulation A B F
using F by blast
interpret F: simulation_as_transformation A B F ..
show "mksta A B F ∈ {t. «t : mkobj A →⇩s⇩t⇩a mkobj B»}"
using assms F sta_mksta A.small_rts_axioms F.transformation_axioms
by auto
qed
show 2: "Map ∈ {t. «t : mkobj A →⇩s⇩t⇩a mkobj B»}
→ Collect (simulation A B)"
using AB.ide_char⇩E⇩R⇩T⇩S cod_char dom_char mkobj_def sta_char by auto
show 3: "⋀F. Map (mksta A B F) = F"
using mkarr_def by auto
show 4: "⋀t. t ∈ {t. «t : mkobj A →⇩s⇩t⇩a mkobj B»}
⟹ mksta A B (Map t) = t"
using AB.Map.simps(1) Trn.simps(1) AB.MkArr_Map AB.arr_char mkarr_def
apply auto[1]
by (metis (no_types, lifting) AB.MkIde_Map Dom_cod Dom_dom H.in_homE
MkArr_Trn V.ide_implies_arr mkobj_simps(1) sta_char)
show "bij_betw (mksta A B) (Collect (simulation A B))
{t. «t : mkobj A →⇩s⇩t⇩a mkobj B»}"
using assms 1 2 3 4 sta_mksta
apply (intro bij_betwI)
by (auto simp add: dom_char cod_char)
show "bij_betw Map {t. «t : mkobj A →⇩s⇩t⇩a mkobj B»}
(Collect (simulation A B))"
using assms 1 2 3 4 sta_mksta
apply (intro bij_betwI)
by (auto simp add: dom_char cod_char)
qed
lemma mkarr_comp:
assumes "small_rts A" and "extensional_rts A"
and "small_rts B" and "extensional_rts B"
and "small_rts C" and "extensional_rts C"
and "transformation A B F G σ"
and "transformation B C H K τ"
shows "mkarr A C (H ∘ F) (K ∘ G) (τ ∘ σ) =
mkarr B C H K τ ⋆ mkarr A B F G σ"
proof -
interpret COMP: COMP A B C
using assms COMP.intro by blast
interpret σ: transformation A B F G σ
using assms by simp
interpret τ: transformation B C H K τ
using assms by simp
show ?thesis
unfolding hcomp_def mkarr_def
using assms sta_mksta COMP.map_eq by auto
qed
lemma mkarr_resid:
assumes "small_rts A ∧ extensional_rts A"
and "small_rts B ∧ extensional_rts B"
and "consistent_transformations A B F G H σ τ"
shows "mkarr A B F G σ ⌢ mkarr A B F H τ"
and "mkarr A B H (consistent_transformations.apex A B H σ τ)
(consistent_transformations.resid A B H σ τ) =
mkarr A B F G σ \\ mkarr A B F H τ"
proof -
interpret A: extensional_rts A
using assms by simp
interpret B: extensional_rts B
using assms by simp
interpret AB: exponential_rts A B ..
interpret στ: consistent_transformations A B F G H σ τ
using assms by blast
show 1: "mkarr A B F G σ ⌢ mkarr A B F H τ"
using assms στ.con con_char AB.con_char mkarr_def
by (simp add: στ.σ.transformation_axioms στ.τ.transformation_axioms)
show "mkarr A B H στ.apex στ.resid =
mkarr A B F G σ \\ mkarr A B F H τ"
unfolding mkarr_def
using assms Trn_resid AB.resid_def AB.Apex_def AB.con_char
στ.σ.transformation_axioms στ.τ.transformation_axioms
στ.con
by (intro arr_eqI) auto
qed
lemma Map_hcomp:
assumes "H.seq t u"
shows "Map (t ⋆ u) = Map t ∘ Map u"
proof -
interpret COMP ‹Dom u› ‹Cod u› ‹Cod t›
using assms arr_char COMP.intro H_seq_char by auto
have t: "arr t" and u: "arr u"
using assms by fastforce+
have tu: "Dom t = Cod u"
using assms H_seq_char by blast
show ?thesis
unfolding hcomp_def
using assms tu t u map_eq H.ext arr_char by auto
qed
lemma Map_resid:
assumes "V.con t u"
shows "consistent_transformations (Dom t) (Cod t)
(Src t) (Trg t) (Trg u) (Map t) (Map u)"
and "Map (t \\ u) =
consistent_transformations.resid (Dom t) (Cod t) (Trg u)
(Map t) (Map u)"
proof -
interpret A: extensional_rts ‹Dom t›
using assms arr_char V.con_implies_arr by blast
interpret B: extensional_rts ‹Cod t›
using assms arr_char V.con_implies_arr by blast
interpret AB: exponential_rts ‹Dom t› ‹Cod t› ..
have 1: "Dom t = Dom u" and "Cod t = Cod u"
using assms con_implies_Par(1-2) by auto
have 2: "Src t = Src u"
using assms con_char AB.con_char by simp
interpret T: transformation ‹Dom t› ‹Cod t›
‹Src t› ‹Trg t› ‹Map t›
using assms arr_char AB.arr_char [of "Trn t"] V.con_implies_arr
by simp
interpret U: transformation ‹Dom t› ‹Cod t›
‹Src t› ‹Trg u› ‹Map u›
using assms 1 2 con_char arr_char [of u] AB.arr_char V.con_implies_arr
by simp
interpret TU: consistent_transformations ‹Dom t› ‹Cod t›
‹Src t› ‹Trg t› ‹Trg u›
‹Map t› ‹Map u›
using assms con_char AB.con_char
by unfold_locales auto
show "consistent_transformations (Dom t) (Cod t)
(Src t) (Trg t) (Trg u)
(Map t) (Map u)"
..
show "Map (t \\ u) =
consistent_transformations.resid (Dom t) (Cod t) (Trg u)
(Map t) (Map u)"
using assms con_char AB.con_char AB.Map_resid by auto
qed
lemma simulation_Map_sta:
assumes "sta f"
shows "simulation (Dom f) (Cod f) (Map f)"
by (metis Map_resid(1) Map_simps(3) V.ideE V.ide_implies_arr
V.src_ide assms consistent_transformations.axioms(6)
transformation.axioms(3))
lemma transformation_Map_arr:
assumes "arr t"
shows "transformation (Dom t) (Cod t) (Src t) (Trg t) (Map t)"
by (meson Map_resid(1) V.arrE assms
consistent_transformations.axioms(6))
lemma iso_char:
shows "H.iso t ⟷ arr t ∧ Src t = Map t ∧ Trg t = Map t ∧
invertible_simulation (Dom t) (Cod t) (Map t)"
proof
assume t: "H.iso t"
have 1: "arr t"
using t H.iso_is_arr by simp
interpret A: extensional_rts ‹Dom t›
using 1 arr_char by blast
interpret B: extensional_rts ‹Cod t›
using 1 arr_char by blast
interpret AB: exponential_rts ‹Dom t› ‹Cod t› ..
interpret BA: exponential_rts ‹Cod t› ‹Dom t› ..
show "arr t ∧ Src t = Map t ∧ Trg t = Map t ∧
invertible_simulation (Dom t) (Cod t) (Map t)"
proof (intro conjI)
show "arr t" by fact
obtain u where tu: "H.inverse_arrows t u"
using t H.iso_def by blast
have 2: "V.ide t ∧ V.ide u"
using tu iso_implies_sta by auto
have 3: "Dom u = Cod t ∧ Cod u = Dom t"
using tu
by (metis (no_types, lifting) H.inverse_arrowsE H_composable_char
V.not_ide_null obj_is_sta)
show "Src t = Map t" and "Trg t = Map t"
using 2 sta_char AB.ide_char⇩E⇩R⇩T⇩S by auto
let ?T = "Map t" and ?U = "Map u"
interpret T: simulation ‹Dom t› ‹Cod t› ?T
using 2 sta_char AB.ide_char⇩E⇩R⇩T⇩S by simp
interpret U: simulation ‹Cod t› ‹Dom t› ?U
using 2 3 sta_char BA.ide_char⇩E⇩R⇩T⇩S by simp
have "inverse_simulations (Dom t) (Cod t) ?U ?T"
proof
show "?T ∘ ?U = I (Cod t)"
by (metis (no_types, lifting) 2 H.ide_compE H.inverse_arrowsE
Map_hcomp Map_simps(2) V.ide_implies_arr tu)
show "?U ∘ ?T = I (Dom t)"
by (metis (no_types, lifting) 2 H.ide_compE H.inverse_arrowsE
Map_hcomp Map_simps(1) V.ide_implies_arr tu)
qed
thus "invertible_simulation (Dom t) (Cod t) (Map t)"
using invertible_simulation_def' by blast
qed
next
assume t: "arr t ∧ Src t = Map t ∧ Trg t = Map t ∧
invertible_simulation (Dom t) (Cod t) (Map t)"
interpret A: extensional_rts ‹Dom t›
using t arr_char by blast
interpret A: small_rts ‹Dom t›
using t arr_char by blast
interpret B: extensional_rts ‹Cod t›
using t arr_char by blast
interpret B: small_rts ‹Cod t›
using t arr_char by blast
interpret AB: exponential_rts ‹Dom t› ‹Cod t› ..
interpret BA: exponential_rts ‹Cod t› ‹Dom t› ..
interpret AA: exponential_rts ‹Dom t› ‹Dom t› ..
interpret BB: exponential_rts ‹Cod t› ‹Cod t› ..
interpret C: COMP ‹Dom t› ‹Cod t› ‹Dom t› ..
interpret C': COMP ‹Cod t› ‹Dom t› ‹Cod t› ..
interpret T: invertible_simulation ‹Dom t› ‹Cod t› ‹Map t›
using t by auto
show "H.iso t"
proof -
obtain U where U: "inverse_simulations (Dom t) (Cod t) U (Map t)"
using T.invertible by blast
interpret U: simulation ‹Cod t› ‹Dom t› U
using U inverse_simulations_def by blast
interpret U: simulation_as_transformation ‹Cod t› ‹Dom t› U ..
interpret TU: inverse_simulations ‹Dom t› ‹Cod t› U ‹Map t›
using U by blast
let ?u = "mksta (Cod t) (Dom t) U"
have u: "V.ide ?u ∧ «?u : cod t → dom t»"
using t sta_mksta U.simulation_axioms A.small_rts_axioms
A.extensional_rts_axioms B.small_rts_axioms
B.extensional_rts_axioms dom_char cod_char
by auto
have seq: "H.seq ?u t ∧ H.seq t ?u"
using t u H.seqI by auto
have "H.inverse_arrows t ?u"
proof
show "obj (hcomp ?u t)"
proof -
have "hcomp ?u t = dom t"
proof (intro arr_eqI)
show "mksta (Cod t) (Dom t) U ⋆ t ≠ Null"
using t U.transformation_axioms sta_mksta V.not_arr_null
null_char seq
by force
show "dom t ≠ Null"
using t arr_char by blast
show "Dom (mksta (Cod t) (Dom t) U ⋆ t) = Dom (dom t)"
using t u sta_mksta mkarr_def by simp
show "Cod (mksta (Cod t) (Dom t) U ⋆ t) = Cod (dom t)"
using t u sta_mksta mkarr_def by simp
show "Trn (mksta (Cod t) (Dom t) U ⋆ t) = Trn (dom t)"
proof -
have "Trn (mksta (Cod t) (Dom t) U ⋆ t) =
C.map (BA.MkIde U, Trn t)"
using t u Trn_hcomp mkarr_def by auto
also have "... = C'.Currying.A_BC.MkArr
(U ∘ Src t) (U ∘ Trg t) (U ∘ Map t)"
unfolding C.map_eq
using t U.transformation_axioms arr_char by auto
also have "... = Trn (dom t)"
using t U inverse_simulations.inv' dom_char mkobj_simps(3)
by auto
finally show ?thesis by blast
qed
qed
thus ?thesis
using t H.ide_dom by auto
qed
show "obj (hcomp t ?u)"
proof -
have "hcomp t ?u = cod t"
proof (intro arr_eqI)
show "t ⋆ mksta (Cod t) (Dom t) U ≠ Null"
using t U.transformation_axioms sta_mksta V.not_arr_null
null_char seq
by force
show "cod t ≠ Null"
using t arr_char by blast
show "Dom (t ⋆ mksta (Cod t) (Dom t) U) = Dom (cod t)"
using t u sta_mksta mkarr_def by simp
show "Cod (t ⋆ mksta (Cod t) (Dom t) U) = Cod (cod t)"
using t u sta_mksta mkarr_def by simp
show "Trn (t ⋆ mksta (Cod t) (Dom t) U) = Trn (cod t)"
proof -
have "Trn (t ⋆ mksta (Cod t) (Dom t) U) =
C'.map (Trn t, BA.MkIde U)"
using t u Trn_hcomp mkarr_def by auto
also have "... = C.Currying.A_BC.MkArr
(Src t ∘ U) (Trg t ∘ U) (Map t ∘ U)"
unfolding C'.map_eq
using t U.transformation_axioms arr_char by auto
also have "... = Trn (cod t)"
using t U inverse_simulations.inv cod_char mkobj_simps(3)
by auto
finally show ?thesis by blast
qed
qed
thus ?thesis
using t H.ide_cod by auto
qed
qed
thus "H.iso t" by blast
qed
qed
end
subsection "Terminal Object"
text‹
The object corresponding to the one-arrow RTS is a terminal object.
We don't want too much clutter in @{locale rtscatx}, so we prove everything
in a separate locale and then transfer only what we want to @{locale rtscatx}.
›
locale terminal_object_in_rtscat =
rtscatx arr_type
for arr_type :: "'A itself"
begin
sublocale One: one_arr_rts arr_type ..
interpretation I⇩1: identity_simulation One.resid ..
abbreviation one ("❙𝟭")
where "one ≡ mkobj One.resid"
lemma obj_one:
shows "obj ❙𝟭"
using obj_mkobj One.is_extensional_rts One.small_rts_axioms by blast
definition trm
where "trm a ≡ MkArr (Dom a) One.resid
(exponential_rts.MkIde
(constant_simulation.map (Dom a) One.resid One.the_arr))"
lemma one_universality:
assumes "obj a"
shows "«trm a : a → ❙𝟭»"
and "⋀t. «t : a → ❙𝟭» ⟹ t = trm a"
and "∃!t. «t : a → ❙𝟭»"
proof -
interpret A: extensional_rts ‹Dom a›
using assms obj_char arr_char by blast
interpret A: small_rts ‹Dom a›
using assms obj_char arr_char by blast
interpret A_One: exponential_rts ‹Dom a› One.resid ..
interpret Trm: constant_simulation ‹Dom a› One.resid One.the_arr
using One.ide_char⇩1⇩R⇩T⇩S
by unfold_locales auto
interpret Trm: simulation_as_transformation ‹Dom a› One.resid Trm.map ..
have Dom_trm: "Dom (trm a) = Dom a"
using trm_def by simp
have Cod_trm: "Cod (trm a) = One.resid"
using trm_def by auto
show 1: "«trm a : a → ❙𝟭»"
proof -
have a: "mksta (Dom a) (Dom a) (I (Dom a)) = a"
using assms bij_mkobj(4) [of a] mkobj_def mkarr_def by auto
have t: "arr (trm a)"
using assms obj_char arr_char One.is_extensional_rts One.small_rts_axioms
A_One.ide_MkIde A_One.ide_implies_arr Trm.transformation_axioms
by (unfold trm_def, intro arr_MkArr) auto
show ?thesis
using a t dom_char cod_char Dom_trm Cod_trm mkobj_def mkarr_def
by (intro H.in_homI) auto
qed
show "⋀t. «t : a → ❙𝟭» ⟹ t = trm a"
proof (intro arr_eqI)
fix t
assume t: "«t : a → ❙𝟭»"
show "t ≠ Null"
using t arr_char [of t] by auto
show "trm a ≠ Null"
using 1 arr_char [of "trm a"] by auto
show "Dom t = Dom (trm a)"
using t 1 trm_def dom_char by auto
show "Cod t = Cod (trm a)"
using t 1 cod_char mkobj_def
by (metis (no_types, lifting) Cod.simps(1) H.in_homE)
show "Trn t = Trn (trm a)"
proof (intro A_One.arr_eqI)
have 2: "⋀F G. ⟦simulation (Dom a) One.resid F;
simulation (Dom a) One.resid G⟧
⟹ F = G"
using A.rts_axioms One.universality by blast
show 3: "A_One.arr (Trn t)"
using assms t arr_char mkobj_def
by (metis (no_types, lifting) H.ideD(1-2) H.in_homE
H_arr_char cod_char dom_char arr.simps(1))
show 4: "A_One.arr (Trn (trm a))"
using 1 trm_def H.in_homE H_arr_char by auto
show "A_One.Dom (Trn t) = A_One.Dom (Trn (trm a))"
using 2 3 4 trm_def A_One.ide_MkIde A_One.ide_src A_One.src_simp
by metis
show "A_One.Cod (Trn t) = A_One.Cod (Trn (trm a))"
using 2 3 4 trm_def A_One.arr_char transformation.axioms(4)
by metis
show "⋀x. A.ide x ⟹
A_One.Map (Trn t) x = A_One.Map (Trn (trm a)) x"
using 3 trm_def A_One.con_char One.arr_char One.con_char by force
qed
qed
thus "∃!t. «t : a → ❙𝟭»"
using 1 by blast
qed
lemma terminal_one:
shows "H.terminal ❙𝟭"
using one_universality H.terminal_def obj_one by blast
lemma trm_in_hom [intro, simp]:
assumes "obj a"
shows "«trm a : a → ❙𝟭»"
using assms one_universality by simp
lemma terminal_arrow_is_sta:
assumes "«t : a → ❙𝟭»"
shows "sta t"
proof -
have "src t = t"
using assms H.ide_dom one_universality(3)
by (metis (no_types, lifting) H.in_homE H.terminal_arr_unique
cod_src dom_src src.preserves_arr terminal_one)
thus ?thesis
using assms
by (metis (no_types, lifting) H.arrI V.ide_iff_src_self arr_coincidence)
qed
text‹
For any object ‹a› we have an RTS isomorphism ‹Dom a ≅ HOM ❙𝟭 a›.
Note that these are \emph{not} at the same type.
›
abbreviation UP :: "'A arr ⇒ 'A ⇒ 'A arr"
where "UP a ≡ MkArr⇩e⇩x⇩t (\\⇩1) (Dom a) ∘ exponential_by_One.Up (Dom a)"
abbreviation DN :: "'A arr ⇒ 'A arr ⇒ 'A"
where "DN a ≡ exponential_by_One.Dn (Dom a) ∘ Trn⇩e⇩x⇩t ❙𝟭 a"
lemma inverse_simulations_DN_UP:
assumes "obj a"
shows "inverse_simulations (Dom a) (HOM ❙𝟭 a) (DN a) (UP a)"
and "isomorphic_rts (Dom a) (HOM ❙𝟭 a)"
proof -
interpret A: extensional_rts ‹Dom a›
using assms obj_char arr_char by blast
interpret A: small_rts ‹Dom a›
using assms obj_char arr_char by blast
interpret Exp: exponential_rts One.resid ‹Dom a› ..
interpret HOM: sub_rts resid ‹λt. «t : ❙𝟭 → a»›
using assms sub_rts_HOM by blast
interpret exponential_by_One arr_type ‹Dom a› ..
interpret Dom_Exp: inverse_simulations ‹Dom a› Exp.resid Dn Up
using inverse_simulations_Dn_Up by blast
interpret Trn_MkArr: inverse_simulations Exp.resid HOM.resid
‹Trn⇩e⇩x⇩t ❙𝟭 a› ‹MkArr⇩e⇩x⇩t One.resid (Dom a)›
using assms inverse_simulations_Trn_MkArr [of One.resid "Dom a"]
bij_mkobj(4) [of a] A.extensional_rts_axioms A.small_rts_axioms
One.extensional_rts_axioms One.small_rts_axioms mkobj_def
apply auto[1]
by metis
show "inverse_simulations (Dom a) HOM.resid
(Dn ∘ Trn⇩e⇩x⇩t ❙𝟭 a) (MkArr⇩e⇩x⇩t One.resid (Dom a) ∘ Up)"
using inverse_simulations_compose Dom_Exp.inverse_simulations_axioms
Trn_MkArr.inverse_simulations_axioms
by blast
thus "isomorphic_rts (Dom a) (HOM ❙𝟭 a)"
using isomorphic_rts_def by blast
qed
lemma terminal_char:
shows "H.terminal x ⟷ obj x ∧ (∃!t. residuation.arr (Dom x) t)"
proof (intro iffI conjI)
assume x: "H.terminal x"
show obj_x: "obj x"
using x H.terminal_def by fastforce
interpret X: extensional_rts ‹Dom x›
using obj_x obj_char arr_char by blast
have 1: "H.isomorphic x ❙𝟭"
using x obj_char terminal_one H.terminal_objs_isomorphic by force
obtain f where f: "«f : x → ❙𝟭» ∧ H.iso f"
using 1 H.isomorphic_def by auto
have ide_f: "sta f"
using f iso_implies_sta by blast
show "∃!t. residuation.arr (Dom x) t"
proof -
have "card (Collect (residuation.arr (Dom x))) = 1"
proof -
have "bij_betw (Map f) (Collect X.arr) (Collect One.arr)"
proof -
have "Dom f = Dom x" and "Cod f = One.resid"
using f dom_char cod_char mkobj_def by auto
thus ?thesis
by (metis (no_types, lifting) f
invertible_simulation.is_bijection_betw_arr_sets iso_char)
qed
moreover have "card (Collect One.arr) = 1"
by (simp add: Collect_cong One.arr_char)
ultimately show ?thesis
by (simp add: bij_betw_same_card)
qed
thus ?thesis
by (metis CollectI Collect_empty_eq One_nat_def card_1_singleton_iff
card_eq_0_iff singleton_iff zero_neq_one)
qed
next
assume x: "obj x ∧ (∃!t. residuation.arr (Dom x) t)"
interpret X: extensional_rts ‹Dom x›
using x obj_char arr_char by blast
interpret T: simulation ‹Dom x› One.resid ‹One.terminator (Dom x)›
using x One.terminator_is_simulation obj_char arr_char small_rts_def
by blast
have "bij_betw (One.terminator (Dom x)) (Collect X.arr) (Collect One.arr)"
proof (unfold bij_betw_def, intro conjI)
show "inj_on (One.terminator (Dom x)) (Collect X.arr)"
using x T.simulation_axioms
by (intro inj_onI) auto
show "One.terminator (Dom x) ` Collect X.arr = Collect One.arr"
proof
show "One.terminator (Dom x) ` Collect X.arr ⊆ Collect One.arr"
by auto
show "Collect One.arr ⊆ One.terminator (Dom x) ` Collect X.arr"
using x T.simulation_axioms One.arr_char T.preserves_reflects_arr
by (metis (no_types, lifting) CollectD CollectI image_iff subsetI)
qed
qed
hence 2: "invertible_simulation (Dom x) One.resid (One.terminator (Dom x))"
using invertible_simulation_iff
[of "Dom x" One.resid "One.terminator (Dom x)"]
One.con_implies_arr
by (metis T.simulation_axioms X.arrE T.preserves_reflects_arr x)
have 3: "sta (mksta (Dom x) One.resid (One.terminator (Dom x)))"
using x T.simulation_axioms obj_char iso_char sta_mksta(1)
arr_char One.small_rts_axioms One.extensional_rts_axioms
invertible_simulation_def
by blast
have 4: "H.iso (mksta (Dom x) One.resid (One.terminator (Dom x)))"
unfolding iso_char
using 2 3 bij_mksta(3) sta_char mkarr_def
by (metis Cod_mkarr Dom_mkarr Map_simps(4) Src_mkarr Trg_mkarr
V.ide_implies_arr V.trg_ide)
interpret T: simulation_as_transformation
‹Dom x› One.resid ‹One.terminator (Dom x)›
..
have "H.isomorphic x ❙𝟭"
using x 4 obj_char arr_char mkarr_simps(1-2) One.small_rts_axioms
One.extensional_rts_axioms T.transformation_axioms
H.isomorphicI [of "mksta (Dom x) (\\⇩1) (One.terminator (Dom x))"]
by (simp add: arr_mkarr(4-5))
thus "H.terminal x"
using H.isomorphic_symmetric H.isomorphic_to_terminal_is_terminal
terminal_one
by blast
qed
end
text‹
The above was all carried out in a separate locale. Here we transfer to
@{locale rtscatx} just the final definitions and facts that we want.
›
context rtscatx
begin
sublocale One: one_arr_rts arr_type ..
definition one ("❙𝟭")
where "one ≡ terminal_object_in_rtscat.one"
definition trm
where "trm = terminal_object_in_rtscat.trm"
interpretation Trm: terminal_object_in_rtscat ..
no_notation Trm.one ("❙𝟭")
lemma obj_one [intro, simp]:
shows "obj one"
unfolding one_def
using Trm.obj_one by blast
lemma trm_simps' [simp]:
assumes "obj a"
shows "arr (trm a)" and "dom (trm a) = a" and "cod (trm a) = ❙𝟭"
and "src (trm a) = trm a" and "trg (trm a) = trm a"
and "sta (trm a)"
proof -
show "arr (trm a)" and "dom (trm a) = a" and "cod (trm a) = ❙𝟭"
unfolding trm_def one_def
using assms Trm.terminal_arrow_is_sta H.in_homE
by auto blast+
show "src (trm a) = trm a" and "trg (trm a) = trm a" and "sta (trm a)"
using Trm.terminal_arrow_is_sta Trm.trm_in_hom V.src_ide
V.trg_ide assms trm_def
by (metis (no_types, lifting))+
qed
sublocale category_with_terminal_object hcomp
using Trm.terminal_one H.terminal_def Trm.obj_one
by unfold_locales auto
sublocale elementary_category_with_terminal_object hcomp one trm
using Trm.obj_one Trm.trm_in_hom
by unfold_locales
(auto simp add: Trm.one_universality(2) one_def trm_def)
lemma is_elementary_category_with_terminal_object:
shows "elementary_category_with_terminal_object hcomp one trm"
..
lemma terminal_char:
shows "H.terminal x ⟷ obj x ∧ (∃!t. residuation.arr (Dom x) t)"
using Trm.terminal_char by simp
lemma Map_trm:
assumes "obj a"
shows "Map (trm a) =
constant_simulation.map (Dom a) One.resid One.the_arr"
proof -
interpret A: extensional_rts ‹Dom a›
using assms obj_char arr_char by blast
interpret A1: exponential_rts ‹Dom a› One.resid ..
show ?thesis
using assms trm_def Trm.trm_def
by (metis A1.Map.simps(1) Trn.simps(1) comp_apply)
qed
lemma inverse_simulations_DN_UP:
assumes "obj a"
shows "inverse_simulations (Dom a) (HOM ❙𝟭 a) (Trm.DN a) (Trm.UP a)"
and "isomorphic_rts (Dom a) (HOM ❙𝟭 a)"
unfolding one_def
using assms Trm.inverse_simulations_DN_UP by auto
abbreviation UP⇩r⇩t⇩s :: "'A arr ⇒ 'A ⇒ 'A arr"
where "UP⇩r⇩t⇩s a ≡ MkArr⇩e⇩x⇩t (\\⇩1) (Dom a) ∘ exponential_by_One.Up (Dom a)"
abbreviation DN⇩r⇩t⇩s :: "'A arr ⇒ 'A arr ⇒ 'A"
where "DN⇩r⇩t⇩s a ≡ exponential_by_One.Dn (Dom a) ∘ Trn⇩e⇩x⇩t ❙𝟭 a"
lemma UP_DN_naturality:
assumes "arr t"
shows "DN⇩r⇩t⇩s (cod t) ∘ cov_HOM ❙𝟭 t = Map t ∘ DN⇩r⇩t⇩s (dom t)"
and "UP⇩r⇩t⇩s (cod t) ∘ Map t = cov_HOM ❙𝟭 t ∘ UP⇩r⇩t⇩s (dom t)"
and "cov_HOM ❙𝟭 t = UP⇩r⇩t⇩s (cod t) ∘ Map t ∘ DN⇩r⇩t⇩s (dom t)"
and "Map t = DN⇩r⇩t⇩s (cod t) ∘ cov_HOM ❙𝟭 t ∘ UP⇩r⇩t⇩s (dom t)"
proof -
let ?a = "dom t" and ?b = "cod t"
let ?A = "Dom t" and ?B = "Cod t"
have a: "obj ?a" and b: "obj ?b"
using assms by auto
have t: "«t : ?a → ?b»"
using assms by auto
have a_simp: "mksta ?A ?A (I ?A) = ?a"
using assms a bij_mkobj(4) dom_char mkobj_def mkarr_def by simp
have b_simp: "mksta ?B ?B (I ?B) = ?b"
using assms b bij_mkobj(4) cod_char mkobj_def mkarr_def by simp
have one_simp: "mksta One.resid One.resid (I One.resid) = one"
unfolding one_def mkarr_def
by (simp add: mkobj_def)
interpret A: extensional_rts ?A
using assms by blast
interpret A: small_rts ?A
using assms by blast
interpret B: extensional_rts ?B
using assms by blast
interpret B: small_rts ?B
using assms by blast
interpret OneA: exponential_by_One arr_type ?A ..
interpret OneB: exponential_by_One arr_type ?B ..
interpret HOM_1a: sub_rts resid ‹λt. «t: ❙𝟭 → ?a»›
using a sub_rts_HOM by blast
interpret HOM_1a: sub_rts_of_extensional_rts resid ‹λt. «t: ❙𝟭 → ?a»› ..
interpret HOM_1b: sub_rts resid ‹λt. «t: ❙𝟭 → ?b»›
using b sub_rts_HOM by blast
interpret HOM_1b: sub_rts_of_extensional_rts resid ‹λt. «t: ❙𝟭 → ?b»› ..
interpret Trn_MkArr_a: inverse_simulations OneA.resid ‹HOM ❙𝟭 ?a›
‹Trn⇩e⇩x⇩t ❙𝟭 ?a› ‹MkArr⇩e⇩x⇩t One.resid ?A›
proof -
show "inverse_simulations OneA.resid (HOM ❙𝟭 ?a)
(Trn⇩e⇩x⇩t ❙𝟭 ?a) (MkArr⇩e⇩x⇩t One.resid ?A)"
using assms inverse_simulations_Trn_MkArr(1) [of One.resid ?A]
unfolding one_def mkobj_def
apply simp
by (metis A.extensional_rts_axioms A.small_rts_axioms
One.is_extensional_rts One.small_rts_axioms a_simp mkarr_def)
qed
interpret Trn_MkArr_b: inverse_simulations OneB.resid ‹HOM ❙𝟭 ?b›
‹Trn⇩e⇩x⇩t ❙𝟭 ?b› ‹MkArr⇩e⇩x⇩t One.resid ?B›
proof -
show "inverse_simulations OneB.resid (HOM ❙𝟭 ?b)
(Trn⇩e⇩x⇩t ❙𝟭 ?b) (MkArr⇩e⇩x⇩t One.resid ?B)"
using assms inverse_simulations_Trn_MkArr(1) [of One.resid ?B]
unfolding one_def mkobj_def
apply simp
by (metis B.extensional_rts_axioms B.small_rts_axioms
One.is_extensional_rts One.small_rts_axioms b_simp mkarr_def)
qed
have UP_a: "UP⇩r⇩t⇩s ?a = MkArr⇩e⇩x⇩t (\\⇩1) ?A ∘ OneA.Up"
using assms t Dom_dom by presburger
have UP_b: "UP⇩r⇩t⇩s ?b = MkArr⇩e⇩x⇩t (\\⇩1) ?B ∘ OneB.Up"
using assms t Dom_cod by presburger
have DN_a: "DN⇩r⇩t⇩s ?a = OneA.Dn ∘ Trn⇩e⇩x⇩t ❙𝟭 ?a"
using assms t Dom_dom by presburger
have DN_b: "DN⇩r⇩t⇩s ?b = OneB.Dn ∘ Trn⇩e⇩x⇩t ❙𝟭 ?b"
using assms t Dom_cod by presburger
interpret UP_DN_a: inverse_simulations ?A HOM_1a.resid
‹DN⇩r⇩t⇩s ?a› ‹UP⇩r⇩t⇩s ?a›
using a t DN_a UP_a OneA.inverse_simulations_Dn_Up
Trn_MkArr_a.inverse_simulations_axioms
inverse_simulations_compose
by fastforce
interpret UP_DN_b: inverse_simulations ?B HOM_1b.resid
‹DN⇩r⇩t⇩s ?b› ‹UP⇩r⇩t⇩s ?b›
using b t DN_b UP_b OneB.inverse_simulations_Dn_Up
Trn_MkArr_b.inverse_simulations_axioms
inverse_simulations_compose
by fastforce
interpret T: transformation ?A ?B ‹Src t› ‹Trg t› ‹Map t›
using assms(1) arr_char [of t]
by (simp add: A.rts_axioms A.weak_extensionality B.extensional_rts_axioms
exponential_rts.arr_char exponential_rts.intro
weakly_extensional_rts.intro weakly_extensional_rts_axioms.intro)
interpret T': transformation ‹HOM ❙𝟭 ?a› ‹HOM ❙𝟭 ?b›
‹cov_HOM ❙𝟭 (src t)› ‹cov_HOM ❙𝟭 (trg t)› ‹cov_HOM ❙𝟭 t›
using assms(1) transformation_cov_HOM_arr [of "❙𝟭" t] obj_one by blast
interpret LHS: transformation ‹HOM ❙𝟭 ?a› ?B
‹DN⇩r⇩t⇩s ?b ∘ cov_HOM ❙𝟭 (src t)›
‹DN⇩r⇩t⇩s ?b ∘ cov_HOM ❙𝟭 (trg t)›
‹DN⇩r⇩t⇩s ?b ∘ cov_HOM ❙𝟭 t›
using assms transformation_whisker_left UP_DN_b.F.simulation_axioms
T'.F.simulation_axioms T'.G.simulation_axioms T'.transformation_axioms
B.weakly_extensional_rts_axioms DN_b
by fastforce
interpret RHS: transformation ‹HOM ❙𝟭 ?a› ?B
‹Src t ∘ DN⇩r⇩t⇩s ?a› ‹Trg t ∘ DN⇩r⇩t⇩s ?a› ‹Map t ∘ DN⇩r⇩t⇩s ?a›
using assms
transformation_whisker_right
[of ?A ?B "Src t" "Trg t" "Map t" HOM_1a.resid "DN⇩r⇩t⇩s ?a"]
UP_DN_a.F.simulation_axioms T.transformation_axioms
HOM_1a.weakly_extensional_rts_axioms DN_a
by auto
show 1: "DN⇩r⇩t⇩s ?b ∘ cov_HOM ❙𝟭 t = Map t ∘ DN⇩r⇩t⇩s ?a"
proof
fix x
show "(DN⇩r⇩t⇩s ?b ∘ cov_HOM ❙𝟭 t) x = (Map t ∘ DN⇩r⇩t⇩s ?a) x"
proof (cases "HOM_1a.arr x")
show "¬ HOM_1a.arr x ⟹ ?thesis"
using LHS.extensional RHS.extensional by auto
assume x: "HOM_1a.arr x"
have Trn_x: "OneA.arr (Trn x)"
using Trn_MkArr_a.F.preserves_reflects_arr x by presburger
have Trn_tx: "OneB.arr (Trn (t ⋆ x))"
using x t T'.preserves_arr Trn_MkArr_b.F.preserves_reflects_arr
by presburger
show ?thesis
using assms x Map_hcomp Trn_tx Dom_cod T'.preserves_arr
HOM_1b.arr_char HOM_1b.inclusion T'.preserves_arr Trn_x
by (auto simp add: one_def)
qed
qed
show "cov_HOM ❙𝟭 t = UP⇩r⇩t⇩s ?b ∘ Map t ∘ DN⇩r⇩t⇩s ?a"
proof -
have "cov_HOM ❙𝟭 t = (UP⇩r⇩t⇩s ?b ∘ DN⇩r⇩t⇩s ?b) ∘ cov_HOM ❙𝟭 t"
using b t comp_identity_transformation [of HOM_1a.resid HOM_1b.resid]
T'.transformation_axioms UP_DN_b.inv UP_b DN_b
by force
also have "... = UP⇩r⇩t⇩s ?b ∘ (DN⇩r⇩t⇩s ?b ∘ cov_HOM ❙𝟭 t)"
by auto
also have "... = UP⇩r⇩t⇩s ?b ∘ (Map t ∘ DN⇩r⇩t⇩s ?a)"
using 1 by simp
also have "... = UP⇩r⇩t⇩s ?b ∘ Map t ∘ DN⇩r⇩t⇩s ?a"
by auto
finally show ?thesis by blast
qed
show 2: "UP⇩r⇩t⇩s ?b ∘ Map t = cov_HOM ❙𝟭 t ∘ UP⇩r⇩t⇩s ?a"
proof -
have "UP⇩r⇩t⇩s ?b ∘ Map t = UP⇩r⇩t⇩s ?b ∘ (Map t ∘ (DN⇩r⇩t⇩s ?a ∘ UP⇩r⇩t⇩s ?a))"
using a t T.transformation_axioms UP_a DN_a
UP_DN_a.inverse_simulations_axioms
by (simp add: comp_transformation_identity inverse_simulations.inv')
also have "... = UP⇩r⇩t⇩s ?b ∘ (DN⇩r⇩t⇩s ?b ∘ cov_HOM ❙𝟭 t ∘ UP⇩r⇩t⇩s ?a)"
using 1 by auto
also have "... = UP⇩r⇩t⇩s ?b ∘ (DN⇩r⇩t⇩s ?b ∘ (cov_HOM ❙𝟭 t ∘ UP⇩r⇩t⇩s ?a))"
using Fun.comp_assoc [of "DN⇩r⇩t⇩s ?b" "cov_HOM ❙𝟭 t" "UP⇩r⇩t⇩s ?a"] by force
also have "... = (UP⇩r⇩t⇩s ?b ∘ DN⇩r⇩t⇩s ?b) ∘ (cov_HOM ❙𝟭 t ∘ UP⇩r⇩t⇩s ?a)"
using Fun.comp_assoc [of "UP⇩r⇩t⇩s ?b" "DN⇩r⇩t⇩s ?b" "cov_HOM ❙𝟭 t ∘ UP⇩r⇩t⇩s ?a"]
by force
also have "... = I HOM_1b.resid ∘ (cov_HOM ❙𝟭 t ∘ UP⇩r⇩t⇩s ?a)"
using UP_DN_b.inv by force
also have "... = I HOM_1b.resid ∘ cov_HOM ❙𝟭 t ∘ UP⇩r⇩t⇩s ?a"
using Fun.comp_assoc [of "I HOM_1b.resid" "cov_HOM ❙𝟭 t" "UP⇩r⇩t⇩s ?a"]
by force
also have "... = cov_HOM ❙𝟭 t ∘ UP⇩r⇩t⇩s ?a"
using comp_identity_transformation
[of HOM_1a.resid HOM_1b.resid "cov_HOM ❙𝟭 (src t)"
"cov_HOM ❙𝟭 (trg t)" "cov_HOM ❙𝟭 t"]
T'.transformation_axioms
by fastforce
finally show ?thesis by blast
qed
show "Map t = DN⇩r⇩t⇩s ?b ∘ cov_HOM ❙𝟭 t ∘ UP⇩r⇩t⇩s ?a"
proof -
have "Map t = DN⇩r⇩t⇩s ?b ∘ UP⇩r⇩t⇩s ?b ∘ Map t"
proof -
have "Map t = I (Cod t) ∘ Map t"
using T.transformation_axioms
comp_identity_transformation [of "Dom t" "Cod t"]
by auto
also have "... = DN⇩r⇩t⇩s ?b ∘ UP⇩r⇩t⇩s ?b ∘ Map t"
using b UP_b DN_b UP_DN_b.inverse_simulations_axioms
inverse_simulations.inv'
by (metis (no_types, lifting))
finally show ?thesis by blast
qed
also have "... = DN⇩r⇩t⇩s ?b ∘ (UP⇩r⇩t⇩s ?b ∘ Map t)"
by auto
also have "... = DN⇩r⇩t⇩s ?b ∘ (cov_HOM ❙𝟭 t ∘ UP⇩r⇩t⇩s ?a)"
using 2 by simp
also have "... = DN⇩r⇩t⇩s ?b ∘ cov_HOM ❙𝟭 t ∘ UP⇩r⇩t⇩s ?a"
using comp_assoc [of "DN⇩r⇩t⇩s ?b" "cov_HOM ❙𝟭 t" "UP⇩r⇩t⇩s ?a"] by metis
finally show ?thesis by blast
qed
qed
text‹
Equality of parallel arrows ‹«u : a → b»› and ‹«v : a → b»› is determined by
their compositions with global transitions ‹«t : ❙𝟭 → a»›.
›
lemma arr_extensionality:
assumes "«u : a → b»" and "«v : a → b»" and "src u = src v" and "trg u = trg v"
shows "u = v ⟷ (∀t. «t : ❙𝟭 → a» ⟶ u ⋆ t = v ⋆ t)"
proof
have a: "obj a" and b: "obj b"
using assms(1) by auto
have A: "small_rts (Dom a) ∧ extensional_rts (Dom a)"
and B: "small_rts (Dom b) ∧ extensional_rts (Dom b)"
using a b obj_char arr_char by blast+
interpret A: extensional_rts ‹Dom a›
using A by blast
interpret B: extensional_rts ‹Dom b›
using B by blast
interpret AB: exponential_rts ‹Dom a› ‹Dom b› ..
have "Dom u = Dom a" and "Cod u = Dom b"
using assms(1) Dom_dom Dom_cod by auto
have "Dom v = Dom a" and "Cod v = Dom b"
using assms(2) Dom_dom Dom_cod by auto
have "Map (src u) = Src u" and "Map (trg u) = Trg u"
using assms(1) Map_simps(3-4) by fastforce+
have "Map (src v) = Src v" and "Map (trg v) = Trg v"
using assms(2) Map_simps(3-4) by fastforce+
interpret U: transformation ‹Dom a› ‹Dom b›
‹Map (src u)› ‹Map (trg u)› ‹Map u›
using assms(1) arr_char [of u] AB.arr_char [of "Trn u"]
‹Dom u = Dom a› ‹Cod u = Dom b›
‹Map (src u) = Src u› ‹Map (trg u) = Trg u›
by auto
interpret V: transformation ‹Dom a› ‹Dom b›
‹Map (src v)› ‹Map (trg v)› ‹Map v›
using assms(2) arr_char [of v] AB.arr_char [of "Trn v"]
‹Dom v = Dom a› ‹Cod v = Dom b›
‹Map (src v) = Src v› ‹Map (trg v) = Trg v›
by auto
show "u = v ⟹ ∀t. «t : ❙𝟭 → a» ⟶ u ⋆ t = v ⋆ t"
by blast
show "∀t. «t : one → a» ⟶ u ⋆ t = v ⋆ t ⟹ u = v"
proof (intro arr_eqI)
assume 1: "∀t. «t : ❙𝟭 → a» ⟶ u ⋆ t = v ⋆ t"
show "u ≠ Null"
using assms(1) arr_char by fastforce
show "v ≠ Null"
using assms(2) arr_char by fastforce
show "Dom u = Dom v"
using ‹Dom u = Dom a› ‹Dom v = Dom a› by auto
show "Cod u = Cod v"
using ‹Cod u = Dom b› ‹Cod v = Dom b› by presburger
show "Trn u = Trn v"
proof (intro AB.arr_eqI)
show "AB.arr (Trn u)"
using assms(1) arr_char [of u] ‹Dom u = Dom a› ‹Cod u = Dom b›
by auto
show "AB.arr (Trn v)"
using assms(2) arr_char [of v] ‹Dom v = Dom a› ‹Cod v = Dom b›
by auto
show "AB.Dom (Trn u) = AB.Dom (Trn v)"
using assms(3) arr_char arr_char ‹Map (src u) = Src u›
‹Map (src v) = Src v›
by auto
show "AB.Cod (Trn u) = AB.Cod (Trn v)"
using assms(4) arr_char arr_char ‹Map (trg u) = Trg u›
‹Map (trg v) = Trg v›
by auto
have "Map u = Map v"
proof -
have "⋀Q R T. transformation One.resid (Dom a) Q R T
⟹ Map u ∘ T = Map v ∘ T"
proof -
fix Q R T
assume 2: "transformation One.resid (Dom a) Q R T"
interpret T: transformation One.resid ‹Dom a› Q R T
using 2 by blast
let ?t = "mkarr One.resid (Dom a) Q R T"
have t: "«?t : ❙𝟭 → a»"
by (metis (no_types, lifting) "2" A H.ideD(2) H.ideD(3) H.ide_in_hom
H.in_homI One.is_extensional_rts One.small_rts_axioms Trm.obj_one
Trm.one_universality(2) a arr_coincidence arr_mkarr(1) arr_mkarr(5)
mkarr_simps(1) mkobj_Dom trm_def trm_simps(3))
show "Map u ∘ T = Map v ∘ T"
by (metis (no_types, lifting) "1" AB.Map.simps(1) H.seqI' mkarr_def
Map_hcomp Trn.simps(1) assms(1) comp_def t)
qed
thus "Map u = Map v"
using assms(3-4)
One.eq_transformation_iff U.transformation_axioms V.transformation_axioms
A.weakly_extensional_rts_axioms B.weakly_extensional_rts_axioms
‹Map (src u) = Src u› ‹Map (trg u) = Trg u›
‹Map (src v) = Src v› ‹Map (trg v) = Trg v›
by metis
qed
thus "⋀a. A.ide a ⟹ AB.Map (Trn u) a = AB.Map (Trn v) a" by simp
qed
qed
qed
lemma sta_extensionality:
assumes "«f : a →⇩s⇩t⇩a b»" and "«g : a →⇩s⇩t⇩a b»"
shows "f = g ⟷ (∀t. «t : ❙𝟭 → a» ⟶ f ⋆ t = g ⋆ t)"
proof
have a: "obj a" and b: "obj b"
using assms(1) by auto
have A: "small_rts (Dom a) ∧ extensional_rts (Dom a)"
and B: "small_rts (Dom b) ∧ extensional_rts (Dom b)"
using a b obj_char arr_char by blast+
interpret A: extensional_rts ‹Dom a›
using A by blast
interpret B: extensional_rts ‹Dom b›
using B by blast
interpret AB: exponential_rts ‹Dom a› ‹Dom b› ..
have "Dom f = Dom a" and "Cod f = Dom b"
using assms(1) Dom_dom Dom_cod by auto
have "Dom g = Dom a" and "Cod g = Dom b"
using assms(2) Dom_dom Dom_cod by auto
interpret F: simulation ‹Dom a› ‹Dom b› ‹Map f›
using assms(1) sta_char [of f] AB.ide_char⇩E⇩R⇩T⇩S [of "Trn f"]
‹Dom f = Dom a› ‹Cod f = Dom b›
by simp
interpret G: simulation ‹Dom a› ‹Dom b› ‹Map g›
using assms(2) sta_char [of g] AB.ide_char⇩E⇩R⇩T⇩S [of "Trn g"]
‹Dom g = Dom a› ‹Cod g = Dom b›
by simp
show "f = g ⟹ ∀t. «t : ❙𝟭 → a» ⟶ f ⋆ t = g ⋆ t"
by blast
show "∀t. «t : ❙𝟭 → a» ⟶ f ⋆ t = g ⋆ t ⟹ f = g"
proof -
assume 1: "∀t. «t : ❙𝟭 → a» ⟶ f ⋆ t = g ⋆ t"
have "⋀Q R T. transformation One.resid (Dom a) Q R T
⟹ Map f ∘ T = Map g ∘ T"
proof -
fix Q R T
assume 2: "transformation One.resid (Dom a) Q R T"
interpret T: transformation One.resid ‹Dom a› Q R T
using 2 by blast
let ?t = "mkarr One.resid (Dom a) Q R T"
have t: "«?t : ❙𝟭 → a»"
by (metis (no_types, lifting) "2" A H.ideD(2) H.ideD(3) H.ide_in_hom
H.in_homI One.is_extensional_rts One.small_rts_axioms Trm.obj_one
Trm.one_universality(2) a arr_coincidence arr_mkarr(1) arr_mkarr(5)
mkarr_simps(1) mkobj_Dom trm_def trm_simps(3))
show "Map f ∘ T = Map g ∘ T"
by (metis (no_types, lifting) "1" AB.Map.simps(1) H.seqI' mkarr_def
Map_hcomp Trn.simps(1) assms(1) comp_apply t)
qed
hence 2: "Map f = Map g"
using One.eq_simulation_iff F.simulation_axioms G.simulation_axioms
A.weakly_extensional_rts_axioms B.weakly_extensional_rts_axioms
by blast
have "f = mksta (Dom a) (Dom b) (Map f)"
using assms(1) a b A B obj_char arr_char bij_mksta(4) by fastforce
also have "... = mksta (Dom a) (Dom b) (Map g)"
using 2 by simp
also have "... = g"
using assms(2) a b A B obj_char arr_char bij_mksta(4) by fastforce
finally show "f = g" by auto
qed
qed
text‹
The mapping @{term "HOM ❙𝟭"}, like @{term Dom}, takes each object to a corresponding RTS,
but unlike @{term Dom} it stays at type ‹'A arr›, rather than decreasing
the type from @{typ "'A arr"} to @{typ 'A}.
›
lemma HOM1_mapsto:
shows "HOM ❙𝟭 ∈ Collect obj → Collect extensional_rts ∩ Collect small_rts"
proof
fix a
assume a: "a ∈ Collect obj"
have A: "extensional_rts (HOM ❙𝟭 a)"
using a extensional_rts_HOM by blast
interpret HOM_1A: sub_rts resid ‹λt. «t : ❙𝟭 → a»›
using a sub_rts_HOM by simp
have "small_rts HOM_1A.resid"
proof -
have "Collect HOM_1A.arr ⊆ H.hom ❙𝟭 a"
using HOM_1A.arr_char by blast
moreover have "small (H.hom ❙𝟭 a)"
using a small_homs by blast
ultimately show ?thesis
using smaller_than_small small_rts_def HOM_1A.rts_axioms
small_rts_axioms_def
by blast
qed
moreover have "extensional_rts HOM_1A.resid"
using A by blast
ultimately show "HOM ❙𝟭 a ∈ Collect extensional_rts ∩ Collect small_rts"
by blast
qed
text‹
The mapping @{term "HOM ❙𝟭"} is not necessarily injective, but it is essentially so.
›
lemma HOM1_reflects_isomorphic:
assumes "obj a" and "obj b" and "isomorphic_rts (HOM ❙𝟭 a) (HOM ❙𝟭 b)"
shows "H.isomorphic a b"
proof -
have 1: "isomorphic_rts (Dom a) (Dom b)"
proof -
have "isomorphic_rts (Dom a) (HOM ❙𝟭 a)"
using assms(1) inverse_simulations_DN_UP(2) by blast
also have "isomorphic_rts ... (HOM ❙𝟭 b)"
using assms(3) by blast
also have "isomorphic_rts ... (Dom b)"
using assms(2) inverse_simulations_DN_UP(2) isomorphic_rts_symmetric
by blast
finally show ?thesis by blast
qed
obtain F G where FG: "inverse_simulations (Dom b) (Dom a) F G"
using 1 isomorphic_rts_def isomorphic_rts_symmetric by blast
interpret FG: inverse_simulations ‹Dom b› ‹Dom a› F G
using FG by blast
let ?f = "mksta (Dom a) (Dom b) F"
let ?g = "mksta (Dom b) (Dom a) G"
have f: "«?f : a →⇩s⇩t⇩a b»" and g: "«?g : b →⇩s⇩t⇩a a» ∧ sta ?g"
using assms(1-2) FG.F.simulation_axioms FG.G.simulation_axioms
bij_mksta(1) obj_char [of a] obj_char [of b]
obj_is_sta sta_char sta_mksta(1-3)
by auto
have "H.inverse_arrows ?f ?g"
proof
show "obj (?g ⋆ ?f)"
proof -
have "?g ⋆ ?f = a"
proof -
have gf: "«?g ⋆ ?f : a →⇩s⇩t⇩a a»"
using f g Cod.simps(1) Dom.simps(1) H.cod_comp H.dom_comp H_seqI
V.ide_implies_arr sta_hcomp
by blast
have "?g ⋆ ?f = mksta (Dom a) (Dom a) (Map (?g ⋆ ?f))"
using f g gf
by (metis (no_types, lifting) Cod_mkarr Dom_mkarr Int_Collect
Src_mkarr Trg_mkarr V.ide_implies_arr assms(1-2) bij_mksta(3)
inf_idem mkarr_comp objE transformation_Map_arr)
also have "... = mksta (Dom a) (Dom a) (Map ?g ∘ Map ?f)"
using gf H.arrI Map_hcomp by force
also have "... = mksta (Dom a) (Dom a) (G ∘ F)"
using assms obj_char arr_char FG.F.simulation_axioms
FG.G.simulation_axioms bij_mksta(3)
by auto
also have "... = mksta (Dom a) (Dom a) (I (Dom a))"
using FG.inv by simp
also have "... = a"
using assms obj_char mkobj_def mkarr_def by simp
finally show ?thesis by blast
qed
thus "obj (?g ⋆ ?f)"
using assms by simp
qed
show "obj (?f ⋆ ?g)"
proof -
have "?f ⋆ ?g = b"
proof -
have fg: "«?f ⋆ ?g : b →⇩s⇩t⇩a b»"
using f g Cod.simps(1) Dom.simps(1) H.cod_comp H.dom_comp H_seqI
V.ide_implies_arr sta_hcomp
by blast
have "?f ⋆ ?g = mksta (Dom b) (Dom b) (Map (?f ⋆ ?g))"
using f g fg
by (metis (no_types, lifting) Cod_mkarr Dom_mkarr Int_Collect
Src_mkarr Trg_mkarr V.ide_implies_arr assms(1-2) bij_mksta(3)
inf_idem mkarr_comp objE transformation_Map_arr)
also have "... = mksta (Dom b) (Dom b) (Map ?f ∘ Map ?g)"
using fg H.arrI Map_hcomp by force
also have "... = mksta (Dom b) (Dom b) (F ∘ G)"
using assms obj_char arr_char FG.F.simulation_axioms
FG.G.simulation_axioms bij_mksta(3)
by auto
also have "... = mksta (Dom b) (Dom b) (I (Dom b))"
using FG.inv' by simp
also have "... = b"
using assms obj_char mkobj_def mkarr_def by simp
finally show ?thesis by blast
qed
thus "obj (?f ⋆ ?g)"
using assms by simp
qed
qed
hence "«?f : a → b» ∧ H.iso ?f"
using f by blast
thus ?thesis
using H.isomorphic_def by blast
qed
end
subsection "Products"
text‹
In this section we show that the category ‹❙R❙T❙S⇧†› has products.
A product of objects ‹a› and ‹b› is obtained by constructing the product
‹Dom a × Dom b› of their underlying RTS's and then showing that there exists an
object ‹a ⊗ b› such that ‹Dom (a ⊗ b)› is isomorphic to ‹Dom a × Dom b›.
Since ‹Dom (a ⊗ b)› will have arrow type @{typ 'A}, but ‹Dom a ⊗ Dom b› has arrow type
@{typ "'A * 'A"}, we need a way to reduce the arrow type of ‹Dom a ⊗ Dom b› from
@{typ "'A * 'A"} to @{typ 'A}. This is done by using the assumption that the type @{typ 'A}
admits pairing to obtain an injective map from @{typ "'A * 'A"} to @{typ 'A}, and then
applying the injective image construction to obtain an RTS with arrow type @{typ 'A}
that is isomorphic to ‹Dom a ⊗ Dom b›.
›
locale product_in_rtscat =
rtscatx arr_type
for arr_type :: "'A itself"
and a
and b +
assumes obj_a: "obj a"
and obj_b: "obj b"
begin
notation hcomp (infixr "⋆" 53)
interpretation A: extensional_rts ‹Dom a›
using obj_a bij_mkobj obj_char by blast
interpretation A: small_rts ‹Dom a›
using obj_a bij_mkobj obj_char by blast
interpretation B: extensional_rts ‹Dom b›
using obj_b bij_mkobj obj_char by blast
interpretation B: small_rts ‹Dom b›
using obj_b bij_mkobj obj_char by blast
interpretation AB: exponential_rts ‹Dom a› ‹Dom b› ..
sublocale PROD: product_rts ‹Dom a› ‹Dom b› ..
sublocale PROD: product_of_extensional_rts ‹Dom a› ‹Dom b› ..
sublocale PROD: product_of_small_rts ‹Dom a› ‹Dom b› ..
sublocale Prod: inj_image_rts pairing.some_pair PROD.resid
by (metis (no_types, opaque_lifting) PROD.rts_axioms
inj_image_rts_axioms_def inj_image_rts_def inj_on_subset
inj_some_pair top_greatest)
sublocale Prod: small_rts Prod.resid
using PROD.small_rts_axioms Prod.preserves_reflects_small_rts
by unfold_locales (simp add: small_rts.small)
sublocale Prod: extensional_rts Prod.resid
using PROD.extensional_rts_axioms Prod.preserves_extensional_rts
by unfold_locales (simp add: extensional_rts.extensional)
text‹
The injective image construction on RTS's gives us invertible simulations between
‹Prod.resid› and ‹PROD.resid›.
›
abbreviation Pack :: "'A × 'A ⇒ 'A"
where "Pack ≡ Prod.map⇩e⇩x⇩t"
abbreviation Unpack :: "'A ⇒ 'A × 'A"
where "Unpack ≡ Prod.map'⇩e⇩x⇩t"
interpretation P⇩1: composite_simulation Prod.resid PROD.resid ‹Dom a›
Unpack PROD.P⇩1
..
interpretation P⇩0: composite_simulation Prod.resid PROD.resid ‹Dom b›
Unpack PROD.P⇩0
..
abbreviation prod :: "'A arr"
where "prod ≡ mkobj Prod.resid"
lemma obj_prod:
shows "obj prod"
using obj_mkobj Prod.extensional_rts_axioms Prod.small_rts_axioms by blast
lemma Dom_prod [simp]:
shows "Dom prod = Prod.resid"
by (simp add: Prod.extensional_rts_axioms Prod.small_rts_axioms)
definition p⇩0 :: "'A arr"
where "p⇩0 ≡ mksta Prod.resid (Dom b) P⇩0.map"
definition p⇩1 :: "'A arr"
where "p⇩1 ≡ mksta Prod.resid (Dom a) P⇩1.map"
lemma p⇩0_simps [simp]:
shows "sta p⇩0" and "dom p⇩0 = prod" and "cod p⇩0 = b"
and "Dom p⇩0 = Prod.resid" and "Cod p⇩0 = Dom b"
and "Trn p⇩0 = exponential_rts.MkIde P⇩0.map"
using p⇩0_def obj_b B.extensional_rts_axioms B.small_rts_axioms
P⇩0.simulation_axioms Prod.extensional_rts_axioms
Prod.small_rts_axioms sta_mksta(1) H.dom_eqI H.cod_eqI
H_seqI obj_char obj_prod mkarr_def
by auto
lemma p⇩1_simps [simp]:
shows "sta p⇩1" and "dom p⇩1 = prod" and "cod p⇩1 = a"
and "Dom p⇩1 = Prod.resid" and "Cod p⇩1 = Dom a"
and "Trn p⇩1 = exponential_rts.MkIde P⇩1.map"
using p⇩1_def obj_a A.extensional_rts_axioms A.small_rts_axioms
P⇩1.simulation_axioms Prod.extensional_rts_axioms
Prod.small_rts_axioms sta_mksta(1) H.dom_eqI H.cod_eqI
H_seqI obj_char obj_prod mkarr_def
by auto
lemma p⇩0_in_hom [intro]:
shows "«p⇩0 : prod → b»"
by auto
lemma p⇩1_in_hom [intro]:
shows "«p⇩1 : prod → a»"
by auto
text‹
It should be noted that the length of the proof of the following result is partly
due to the fact that it is proving something rather stronger than one might
expect at first blush. The category we are working with here is analogous to a
2-category in the sense that there are essentially two classes of arrows:
\emph{states}, which correspond to simulations between RTS's, and \emph{transitions},
which correspond to transformations. The class of states is included
in the class of transitions. The universality result below shows the universality
of the product for the full class of arrows, so it is in that sense analogous to
showing that the category has 2-products, rather than just ordinary products.
›
lemma universality:
assumes "«h : x → a»" and "«k : x → b»"
shows "∃!m. p⇩1 ⋆ m = h ∧ p⇩0 ⋆ m = k"
proof
interpret X: extensional_rts ‹Dom x›
using assms(1) H.in_homE H_arr_char dom_char by auto
interpret X: small_rts ‹Dom x›
using assms(1) H.in_homE H_arr_char dom_char by auto
interpret A: extensional_rts ‹Dom a›
using assms(1) H.in_homE H_arr_char cod_char by auto
interpret A: small_rts ‹Dom a›
using assms(1) H.in_homE H_arr_char cod_char by auto
interpret B: extensional_rts ‹Dom b›
using assms(2) H.in_homE H_arr_char cod_char by auto
interpret B: small_rts ‹Dom b›
using assms(2) H.in_homE H_arr_char cod_char by auto
interpret XA: exponential_rts ‹Dom x› ‹Dom a› ..
interpret XB: exponential_rts ‹Dom x› ‹Dom b› ..
have *: "Dom h = Dom x ∧ Cod h = Dom a ∧
Dom k = Dom x ∧ Cod k = Dom b"
using assms(1-2) dom_char cod_char by auto
interpret H⇩0: simulation ‹Dom x› ‹Dom a› ‹Map (src h)›
by (metis (mono_tags, lifting) * H.arrI H_arr_char Trn.simps(1)
XA.ide_char⇩E⇩R⇩T⇩S XA.ide_src arr_char assms(1) comp_apply src_char)
interpret H⇩1: simulation ‹Dom x› ‹Dom a› ‹Map (trg h)›
by (metis (mono_tags, lifting) * H.arrI H_arr_char Trn.simps(1)
XA.ide_char⇩E⇩R⇩T⇩S XA.ide_trg arr_char assms(1) comp_apply trg_char)
interpret K⇩0: simulation ‹Dom x› ‹Dom b› ‹Map (src k)›
by (metis (mono_tags, lifting) "*" H.arrI H_arr_char Map_simps(3)
XB.arrE arr_char assms(2) comp_apply transformation_def)
interpret K⇩1: simulation ‹Dom x› ‹Dom b› ‹Map (trg k)›
by (metis (mono_tags, lifting) "*" H.arrI H_arr_char Map_simps(4)
XB.arrE arr_char assms(2) comp_apply transformation_def)
interpret H: transformation ‹Dom x› ‹Dom a›
‹Map (src h)› ‹Map (trg h)› ‹Map h›
using "*" Map_simps(3) Map_simps(4) XA.arr_char arr_char assms(1)
by (metis H.arrI H_arr_char transformation_Map_arr)
interpret K: transformation ‹Dom x› ‹Dom b›
‹Map (src k)› ‹Map (trg k)› ‹Map k›
using "*" Map_simps(3) Map_simps(4) XB.arr_char arr_char assms(2)
H.arrI
by force
interpret HK⇩0: simulation ‹Dom x› PROD.resid
‹⟨⟨Map (src h), Map (src k)⟩⟩›
using assms PROD.universality(1) [of "Dom h" "Map (src h)" "Map (src k)"]
H⇩0.simulation_axioms K⇩0.simulation_axioms
by blast
interpret HK⇩1: simulation ‹Dom x› PROD.resid
‹⟨⟨Map (trg h), Map (trg k)⟩⟩›
using assms PROD.universality(1) [of "Dom h" "Map (trg h)" "Map (trg k)"]
H⇩1.simulation_axioms K⇩1.simulation_axioms
by blast
interpret PROD.P⇩1: simulation_as_transformation PROD.resid ‹Dom a›
PROD.P⇩1
..
interpret PROD.P⇩0: simulation_as_transformation PROD.resid ‹Dom b›
PROD.P⇩0
..
interpret P⇩1: simulation_as_transformation Prod.resid ‹Dom a› P⇩1.map ..
interpret P⇩0: simulation_as_transformation Prod.resid ‹Dom b› P⇩0.map ..
interpret P⇩0oHK⇩0: composite_simulation ‹Dom x› PROD.resid ‹Dom b›
‹⟨⟨Map (src h), Map (src k)⟩⟩› PROD.P⇩0
..
interpret P⇩0oHK⇩1: composite_simulation ‹Dom x› PROD.resid ‹Dom b›
‹⟨⟨Map (trg h), Map (trg k)⟩⟩› PROD.P⇩0
..
interpret P⇩1oHK⇩0: composite_simulation ‹Dom x› PROD.resid ‹Dom a›
‹⟨⟨Map (src h), Map (src k)⟩⟩› PROD.P⇩1
..
interpret P⇩1oHK⇩1: composite_simulation ‹Dom x› PROD.resid ‹Dom a›
‹⟨⟨Map (trg h), Map (trg k)⟩⟩› PROD.P⇩1
..
interpret HK: transformation ‹Dom x› PROD.resid
‹⟨⟨Map (src h), Map (src k)⟩⟩›
‹⟨⟨Map (trg h), Map (trg k)⟩⟩›
‹⟨⟨Map h, Map k⟩⟩›
using assms HK⇩0.simulation_axioms HK⇩1.simulation_axioms
H.transformation_axioms K.transformation_axioms
by (metis H⇩0.simulation_axioms H⇩1.simulation_axioms
K⇩0.simulation_axioms K⇩1.simulation_axioms PROD.proj_tuple(1)
PROD.universality2(1) PROD.universality(3))
interpret Pack_o_HK: transformation ‹Dom h› Prod.resid
‹Pack ∘ ⟨⟨Map (src h), Map (src k)⟩⟩›
‹Pack ∘ ⟨⟨Map (trg h), Map (trg k)⟩⟩›
‹Pack ∘ ⟨⟨Map h, Map k⟩⟩›
using assms transformation_whisker_left
Prod.weakly_extensional_rts_axioms HK.transformation_axioms
Prod.Map.simulation_axioms dom_char
by fastforce
let ?hk = "mkarr (Dom h) Prod.resid
(Pack ∘ ⟨⟨Map (src h), Map (src k)⟩⟩)
(Pack ∘ ⟨⟨Map (trg h), Map (trg k)⟩⟩)
(Pack ∘ ⟨⟨Map h, Map k⟩⟩)"
have hk: "«?hk : dom h → prod»"
using assms arr_mkarr arr_char Pack_o_HK.transformation_axioms
X.extensional_rts_axioms X.small_rts_axioms
Prod.extensional_rts_axioms Prod.small_rts_axioms
dom_char cod_char
by auto
show "p⇩1 ⋆ ?hk = h ∧ p⇩0 ⋆ ?hk = k"
proof
have seq0: "H.seq p⇩0 ?hk"
using hk by blast
have seq1: "H.seq p⇩1 ?hk"
using hk by blast
show "p⇩1 ⋆ ?hk = h"
proof (intro arr_eqI)
show "p⇩1 ⋆ ?hk ≠ Null"
using seq1 arr_char by auto
show "h ≠ Null"
using assms arr_char [of h] by auto
show Dom: "Dom (p⇩1 ⋆ ?hk) = Dom h"
using seq1 H_seq_char mkarr_def by fastforce
show Cod: "Cod (p⇩1 ⋆ ?hk) = Cod h"
using "*" H.arrI hk mkarr_def by auto
show "Trn (p⇩1 ⋆ ?hk) = Trn h"
proof -
interpret C: COMP ‹Dom x› Prod.resid ‹Dom a› ..
have "Trn (p⇩1 ⋆ ?hk) =
COMP.map (Dom ?hk) (Cod ?hk) (Cod p⇩1) (Trn p⇩1, Trn ?hk)"
using assms seq1 Trn_hcomp hk H.seqE mkarr_def by auto
also have "... =
COMP.map (Dom x) Prod.resid (Dom a) (Trn p⇩1, Trn ?hk)"
using assms hk dom_char mkarr_def by auto
also have "... =
C.BC.MkArr
((P⇩1.map ∘ Pack) ∘
⟨⟨C.BC.Map (Trn (src h)), C.BC.Map (Trn (src k))⟩⟩)
((P⇩1.map ∘ Pack) ∘
⟨⟨C.BC.Map (Trn (trg h)), C.BC.Map (Trn (trg k))⟩⟩)
((P⇩1.map ∘ Pack) ∘
⟨⟨C.BC.Map (Trn h), C.BC.Map (Trn k)⟩⟩)"
unfolding p⇩1_def C.map_eq
using assms hk C.map_eq P⇩1.transformation_axioms
Pack_o_HK.transformation_axioms dom_char cod_char mkarr_def
by auto
also have "... =
C.BC.MkArr
(PROD.P⇩1 ∘
⟨⟨C.BC.Map (Trn (src h)), C.BC.Map (Trn (src k))⟩⟩)
(PROD.P⇩1 ∘
⟨⟨C.BC.Map (Trn (trg h)), C.BC.Map (Trn (trg k))⟩⟩)
(PROD.P⇩1 ∘
⟨⟨C.BC.Map (Trn h), C.BC.Map (Trn k)⟩⟩)"
proof -
have "P⇩1.map ∘ Pack = PROD.P⇩1"
using PROD.P⇩1.extensional Prod.map_null Prod.null_char by auto
thus ?thesis by simp
qed
also have "... = C.BC.MkArr
(C.BC.Map (Trn (src h))) (C.BC.Map (Trn (trg h)))
(C.BC.Map (Trn h))"
using PROD.proj_tuple2(1-2) PROD.proj_tuple(1-2)
H.transformation_axioms K.transformation_axioms
H⇩0.simulation_axioms H⇩1.simulation_axioms
K⇩0.simulation_axioms K⇩1.simulation_axioms
by auto
also have "... = Trn h"
using assms C.BC.MkArr_Map "*" Map_simps(3-4) XA.arr_char arr_char
by (metis (no_types, lifting) H.arrI H_arr_char comp_def)
finally show ?thesis by blast
qed
qed
show "p⇩0 ⋆ ?hk = k"
proof (intro arr_eqI)
show "p⇩0 ⋆ ?hk ≠ Null"
using seq0 arr_char by auto
show "k ≠ Null"
using assms arr_char [of k] by auto
show Dom: "Dom (p⇩0 ⋆ ?hk) = Dom k"
using "*" H_seq_char seq1 mkarr_def by auto
show Cod: "Cod (p⇩0 ⋆ ?hk) = Cod k"
using "*" H_seq_char seq0 by auto
show "Trn (p⇩0 ⋆ ?hk) = Trn k"
proof -
interpret C: COMP ‹Dom x› Prod.resid ‹Dom b› ..
have "Trn (p⇩0 ⋆ ?hk) =
COMP.map (Dom ?hk) (Cod ?hk) (Cod p⇩0) (Trn p⇩0, Trn ?hk)"
using assms seq0 Trn_hcomp [of p⇩0 ?hk] hk H.seqE mkarr_def by auto
also have "... =
COMP.map (Dom x) Prod.resid (Dom b) (Trn p⇩0, Trn ?hk)"
using assms hk dom_char mkarr_def by auto
also have "... =
C.BC.MkArr
((P⇩0.map ∘ Pack) ∘
⟨⟨C.BC.Map (Trn (src h)), C.BC.Map (Trn (src k))⟩⟩)
((P⇩0.map ∘ Pack) ∘
⟨⟨C.BC.Map (Trn (trg h)), C.BC.Map (Trn (trg k))⟩⟩)
((P⇩0.map ∘ Pack) ∘
⟨⟨C.BC.Map (Trn h), C.BC.Map (Trn k)⟩⟩)"
unfolding p⇩0_def C.map_eq
using assms hk C.map_eq P⇩0.transformation_axioms
Pack_o_HK.transformation_axioms dom_char cod_char mkarr_def
by auto
also have "... =
C.BC.MkArr
(PROD.P⇩0 ∘
⟨⟨C.BC.Map (Trn (src h)), C.BC.Map (Trn (src k))⟩⟩)
(PROD.P⇩0 ∘
⟨⟨C.BC.Map (Trn (trg h)), C.BC.Map (Trn (trg k))⟩⟩)
(PROD.P⇩0 ∘
⟨⟨C.BC.Map (Trn h), C.BC.Map (Trn k)⟩⟩)"
proof -
have "P⇩0.map ∘ Pack = PROD.P⇩0"
using PROD.P⇩0.extensional Prod.map_null Prod.null_char by auto
thus ?thesis by simp
qed
also have "... = C.BC.MkArr
(C.BC.Map (Trn (src k))) (C.BC.Map (Trn (trg k)))
(C.BC.Map (Trn k))"
using PROD.proj_tuple2(1-2) PROD.proj_tuple(1-2)
H.transformation_axioms K.transformation_axioms
H⇩0.simulation_axioms H⇩1.simulation_axioms
K⇩0.simulation_axioms K⇩1.simulation_axioms
by auto
also have "... = Trn k"
using assms C.BC.MkArr_Map [of "Trn k"] "*" Map_simps(3-4)
XB.arr_char arr_char
by (metis (no_types, lifting) H.arrI H_arr_char comp_apply)
finally show ?thesis by blast
qed
qed
qed
fix m
assume m: "p⇩1 ⋆ m = h ∧ p⇩0 ⋆ m = k"
have arr_m: "arr m"
using assms m by fastforce
have Dom_m: "Dom m = Dom x"
using assms m dom_char by fastforce
have Cod_m: "Cod m = Prod.resid"
using assms m cod_char
using H_seq_char by auto
interpret X_Prod: exponential_rts ‹Dom x› Prod.resid ..
interpret M: transformation ‹Dom x› Prod.resid
‹Map (src m)› ‹Map (trg m)› ‹Map m›
using Cod_m Dom_m Map_simps(3) Map_simps(4) arr_char arr_m by auto
interpret UnpackoM: transformation ‹Dom h› PROD.resid
‹Unpack ∘ Map (src m)›
‹Unpack ∘ Map (trg m)›
‹Unpack ∘ Map m›
using "*" M.transformation_axioms PROD.weakly_extensional_rts_axioms
Prod.Map'.simulation_axioms transformation_whisker_left
by fastforce
show "m = ?hk"
proof (intro arr_eqI)
show "m ≠ Null"
using assms m null_char by fastforce
show "?hk ≠ Null"
using hk mkarr_def by auto
show 2: "Dom m = Dom ?hk"
using assms m hk cod_char "*" Dom.simps(1) Dom_m mkarr_def
by presburger
show 3: "Cod m = Cod ?hk"
using assms m hk cod_char mkarr_def
by (simp add: Cod_m)
show "Trn m = Trn ?hk"
proof (intro X_Prod.arr_eqI)
interpret COMPa: COMP ‹Dom x› Prod.resid ‹Dom a› ..
interpret COMPb: COMP ‹Dom x› Prod.resid ‹Dom b› ..
show 4: "X_Prod.arr (Trn m)"
using assms arr_m Dom_m Cod_m arr_char by simp
show 5: "X_Prod.arr (Trn ?hk)"
using "2" Dom_m H_arr_char hk mkarr_def by force
show 6: "X_Prod.Dom (Trn m) = X_Prod.Dom (Trn ?hk)"
proof -
have "PROD.P⇩1 ∘ (Unpack ∘ X_Prod.Dom (Trn ?hk)) =
PROD.P⇩1 ∘ (Unpack ∘ X_Prod.Dom (Trn m))"
proof -
have "PROD.P⇩1 ∘ (Unpack ∘ X_Prod.Dom (Trn ?hk)) =
PROD.P⇩1 ∘ (Unpack ∘ Pack) ∘
⟨⟨COMPa.BC.Map (Trn (src h)),
COMPa.BC.Map (Trn (src k))⟩⟩"
using mkarr_def by auto
also have "... = COMPa.BC.Map (Trn (src h))"
proof
fix x
show "(PROD.P⇩1 ∘ (Unpack ∘ Pack) ∘
⟨⟨COMPa.BC.Map (Trn (src h)),
COMPa.BC.Map (Trn (src k))⟩⟩) x =
COMPa.BC.Map (Trn (src h)) x"
using PROD.P⇩1_def
apply (auto simp add: pointwise_tuple_def)[1]
apply (metis A.not_arr_null PROD.null_char
Prod.null_char first_conv)
apply (metis (no_types, opaque_lifting) H⇩0.extensional
H⇩0.simulation_axioms comp_apply
simulation.preserves_reflects_arr)
apply (metis B.not_arr_null PROD.null_char Prod.null_char
second_conv)
by (metis (no_types, opaque_lifting) A.not_arr_null
H⇩0.extensional P⇩1oHK⇩0.preserves_reflects_arr comp_def
pointwise_tuple_def)
qed
also have "... = COMPa.BC.Map (Trn (src (p⇩1 ⋆ m)))"
using m by blast
also have "... = COMPa.BC.Map (Trn (p⇩1 ⋆ src m))"
using assms m by auto
also have "... =
COMPa.BC.Map (COMPa.map (Trn p⇩1, Trn (src m)))"
using arr_m Dom_m Cod_m Trn_hcomp by simp
also have "... =
COMPa.BC.Map (Trn p⇩1) ∘ COMPa.BC.Map (Trn (src m))"
proof -
have "COMPa.BCxAB.arr (COMPa.BC.MkIde P⇩1.map, Trn m)"
using assms arr_m Dom_m Cod_m arr_char arr_char p⇩1_simps(1)
P⇩1.transformation_axioms
by auto
thus ?thesis
unfolding COMPa.map_eq
using assms m arr_m Dom_m Cod_m arr_char [of "src m"] by simp
qed
also have "... =
(PROD.P⇩1 ∘ Unpack) ∘ COMPa.BC.Map (Trn (src m))"
by simp
also have "... = PROD.P⇩1 ∘ (Unpack ∘ X_Prod.Dom (Trn m))"
by (auto simp add: 4 Cod_m Dom_m arr_m src_char)
finally show ?thesis by blast
qed
moreover have "PROD.P⇩0 ∘ (Unpack ∘ X_Prod.Dom (Trn ?hk)) =
PROD.P⇩0 ∘ (Unpack ∘ X_Prod.Dom (Trn m))"
proof -
have "PROD.P⇩0 ∘ (Unpack ∘ X_Prod.Dom (Trn ?hk)) =
PROD.P⇩0 ∘ (Unpack ∘ Pack) ∘
⟨⟨COMPb.BC.Map (Trn (src h)),
COMPb.BC.Map (Trn (src k))⟩⟩"
using mkarr_def by auto
also have "... = COMPb.BC.Map (Trn (src k))"
proof
fix x
show "(PROD.P⇩0 ∘ (Unpack ∘ Pack) ∘
⟨⟨COMPb.BC.Map (Trn (src h)),
COMPb.BC.Map (Trn (src k))⟩⟩) x =
COMPb.BC.Map (Trn (src k)) x"
using PROD.P⇩0_def H⇩0.preserves_reflects_arr K⇩0.extensional
PROD.null_char Prod.null_char
apply (auto simp add: pointwise_tuple_def)[1]
apply (metis second_conv)
apply (metis A.not_arr_null PROD.null_char first_conv)
by (metis (no_types, opaque_lifting) B.not_arr_null
P⇩0oHK⇩0.preserves_reflects_arr comp_def pointwise_tuple_def)
qed
also have "... = COMPb.BC.Map (Trn (src (p⇩0 ⋆ m)))"
using m by blast
also have "... = COMPb.BC.Map (Trn (p⇩0 ⋆ src m))"
using assms m by auto
also have "... = COMPb.BC.Map (COMPb.map (Trn p⇩0, Trn (src m)))"
using arr_m Dom_m Cod_m Trn_hcomp by simp
also have "... = COMPb.BC.Map (Trn p⇩0) ∘
COMPb.BC.Map (Trn (src m))"
proof -
have "COMPb.BCxAB.arr (COMPb.BC.MkIde P⇩0.map, Trn m)"
using assms arr_m Dom_m Cod_m arr_char arr_char p⇩0_simps(1)
P⇩0.transformation_axioms
by auto
thus ?thesis
unfolding COMPb.map_eq
using assms m arr_m Dom_m Cod_m arr_char [of "src m"]
by simp
qed
also have "... =
(PROD.P⇩0 ∘ Unpack) ∘ COMPb.BC.Map (Trn (src m))"
by simp
also have "... = PROD.P⇩0 ∘ (Unpack ∘ X_Prod.Dom (Trn m))"
by (auto simp add: 4 Cod_m Dom_m arr_m src_char)
finally show ?thesis by blast
qed
moreover have "simulation (Dom x) PROD.resid
(Unpack ∘ X_Prod.Dom (Trn ?hk))"
using hk arr_char 2 Pack_o_HK.F.simulation_axioms Dom_m
Prod.Map'.simulation_axioms simulation_comp mkarr_def
by auto
moreover have "simulation (Dom x) PROD.resid
(Unpack ∘ X_Prod.Dom (Trn m))"
using 4 X_Prod.ide_src Prod.Map'.simulation_axioms
simulation_comp
by auto
ultimately have "Unpack ∘ X_Prod.Dom (Trn ?hk) =
Unpack ∘ X_Prod.Dom (Trn m)"
using PROD.proj_joint_monic by blast
moreover have "simulation (Dom x) Prod.resid (X_Prod.Dom (Trn ?hk))"
using hk arr_char X_Prod.ide_src "2" Pack_o_HK.F.simulation_axioms
Dom_m mkarr_def
by fastforce
moreover have "simulation (Dom x) Prod.resid (X_Prod.Dom (Trn m))"
using 4 X_Prod.ide_src by auto
ultimately show ?thesis
using invertible_simulation_cancel_left
by (metis (no_types, lifting) Prod.invertible_simulation_map')
qed
show 7: "X_Prod.Cod (Trn m) = X_Prod.Cod (Trn ?hk)"
proof -
have "PROD.P⇩1 ∘ (Unpack ∘ X_Prod.Cod (Trn ?hk)) =
PROD.P⇩1 ∘ (Unpack ∘ X_Prod.Cod (Trn m))"
proof -
have "PROD.P⇩1 ∘ (Unpack ∘ X_Prod.Cod (Trn ?hk)) =
PROD.P⇩1 ∘ (Unpack ∘ Pack) ∘
⟨⟨COMPa.BC.Map (Trn (trg h)),
COMPa.BC.Map (Trn (trg k))⟩⟩"
using mkarr_def by auto
also have "... = COMPa.BC.Map (Trn (trg h))"
proof
fix x
show "(PROD.P⇩1 ∘ (Unpack ∘ Pack) ∘
⟨⟨COMPa.BC.Map (Trn (trg h)),
COMPa.BC.Map (Trn (trg k))⟩⟩) x =
COMPa.BC.Map (Trn (trg h)) x"
using PROD.P⇩1_def
apply (auto simp add: pointwise_tuple_def)[1]
subgoal by (metis A.not_arr_null PROD.null_char Prod.null_char
first_conv)
subgoal using H⇩1.extensional H⇩1.preserves_reflects_arr by auto
subgoal by (metis B.not_arr_null PROD.null_char Prod.null_char
second_conv)
subgoal by (metis (mono_tags, lifting) H⇩1.simulation_axioms
K⇩1.simulation_axioms comp_def simulation.extensional
simulation.preserves_reflects_arr)
done
qed
also have "... = COMPa.BC.Map (Trn (trg (p⇩1 ⋆ m)))"
using m by blast
also have "... = COMPa.BC.Map (Trn (p⇩1 ⋆ trg m))"
using assms m by auto
also have "... = COMPa.BC.Map (COMPa.map (Trn p⇩1, Trn (trg m)))"
using arr_m Dom_m Cod_m by simp
also have "... =
COMPa.BC.Map (Trn p⇩1) ∘ COMPa.BC.Map (Trn (trg m))"
proof -
have "COMPa.BCxAB.arr (COMPa.BC.MkIde P⇩1.map, Trn m)"
using assms arr_m Dom_m Cod_m arr_char arr_char p⇩1_simps(1)
P⇩1.transformation_axioms
by auto
thus ?thesis
unfolding COMPa.map_eq
using assms m arr_m Dom_m Cod_m arr_char [of "trg m"] by simp
qed
also have "... =
(PROD.P⇩1 ∘ Unpack) ∘ COMPa.BC.Map (Trn (trg m))"
by simp
also have "... = PROD.P⇩1 ∘ (Unpack ∘ X_Prod.Cod (Trn m))"
by (auto simp add: 4 Cod_m Dom_m arr_m trg_char)
finally show ?thesis by blast
qed
moreover have "PROD.P⇩0 ∘ (Unpack ∘ X_Prod.Cod (Trn ?hk)) =
PROD.P⇩0 ∘ (Unpack ∘ X_Prod.Cod (Trn m))"
proof -
have "PROD.P⇩0 ∘ (Unpack ∘ X_Prod.Cod (Trn ?hk)) =
PROD.P⇩0 ∘ (Unpack ∘ Pack) ∘
⟨⟨COMPb.BC.Map (Trn (trg h)),
COMPb.BC.Map (Trn (trg k))⟩⟩"
using mkarr_def by auto
also have "... = COMPb.BC.Map (Trn (trg k))"
proof
fix x
show "(PROD.P⇩0 ∘ (Unpack ∘ Pack) ∘
⟨⟨COMPb.BC.Map (Trn (trg h)),
COMPb.BC.Map (Trn (trg k))⟩⟩) x =
COMPb.BC.Map (Trn (trg k)) x"
using PROD.P⇩0_def H⇩0.preserves_reflects_arr K⇩0.extensional
K⇩1.extensional PROD.null_char Prod.null_char
H⇩1.preserves_reflects_arr second_conv
apply (auto simp add: pointwise_tuple_def)[1]
apply metis
apply (metis B.not_arr_null)
using K⇩1.extensional K⇩1.preserves_reflects_arr by fastforce
qed
also have "... = COMPb.BC.Map (Trn (trg (p⇩0 ⋆ m)))"
using m by blast
also have "... = COMPb.BC.Map (Trn (p⇩0 ⋆ trg m))"
using assms m by auto
also have "... =
COMPb.BC.Map (COMPb.map (Trn p⇩0, Trn (trg m)))"
using arr_m Dom_m Cod_m by simp
also have "... =
COMPb.BC.Map (Trn p⇩0) ∘ COMPb.BC.Map (Trn (trg m))"
proof -
have "COMPb.BCxAB.arr (COMPb.BC.MkIde P⇩0.map, Trn m)"
using assms arr_m Dom_m Cod_m arr_char arr_char p⇩0_simps(1)
P⇩0.transformation_axioms
by auto
thus ?thesis
unfolding COMPb.map_eq
using assms m arr_m Dom_m Cod_m arr_char [of "trg m"]
by simp
qed
also have "... = (PROD.P⇩0 ∘ Unpack) ∘ COMPb.BC.Map (Trn (trg m))"
by simp
also have "... = PROD.P⇩0 ∘ (Unpack ∘ X_Prod.Cod (Trn m))"
by (auto simp add: 4 Cod_m Dom_m arr_m trg_char)
finally show ?thesis by blast
qed
moreover have "simulation (Dom x) PROD.resid
(Unpack ∘ X_Prod.Cod (Trn ?hk))"
using hk arr_char 2 Pack_o_HK.G.simulation_axioms Dom_m
Prod.Map'.simulation_axioms simulation_comp
using mkarr_def by auto
moreover have "simulation (Dom x) PROD.resid
(Unpack ∘ X_Prod.Cod (Trn m))"
using X_Prod.ide_trg ‹X_Prod.arr (Trn m)›
Prod.Map'.simulation_axioms simulation_comp
by auto
ultimately have "Unpack ∘ X_Prod.Cod (Trn ?hk) =
Unpack ∘ X_Prod.Cod (Trn m)"
using PROD.proj_joint_monic by blast
moreover have "simulation (Dom x) Prod.resid
(X_Prod.Cod (Trn ?hk))"
using hk 2 arr_char X_Prod.ide_trg Dom_m mkarr_def
Pack_o_HK.F.simulation_axioms Pack_o_HK.G.simulation_axioms
by force
moreover have "simulation (Dom x) Prod.resid
(X_Prod.Cod (Trn m))"
using 4 X_Prod.ide_trg by auto
ultimately show ?thesis
using invertible_simulation_cancel_left
by (metis (no_types, lifting) Prod.invertible_simulation_map')
qed
show "⋀x. X.ide x ⟹ X_Prod.Map (Trn m) x = X_Prod.Map (Trn ?hk) x"
proof -
have "PROD.P⇩1 ∘ (Unpack ∘ X_Prod.Map (Trn ?hk)) =
PROD.P⇩1 ∘ (Unpack ∘ X_Prod.Map (Trn m))"
proof -
have "PROD.P⇩1 ∘ (Unpack ∘ X_Prod.Map (Trn ?hk)) =
PROD.P⇩1 ∘ (Unpack ∘ Pack) ∘
⟨⟨COMPa.BC.Map (Trn h), COMPa.BC.Map (Trn k)⟩⟩"
using mkarr_def by auto
also have "... = COMPa.BC.Map (Trn h)"
proof
fix x
show "(PROD.P⇩1 ∘ (Unpack ∘ Pack) ∘
⟨⟨COMPa.BC.Map (Trn h),
COMPa.BC.Map (Trn k)⟩⟩) x =
COMPa.BC.Map (Trn h) x"
using PROD.P⇩1_def
apply (auto simp add: pointwise_tuple_def)[1]
apply (metis A.not_arr_null PROD.null_char Prod.null_char
first_conv)
apply (metis (mono_tags, lifting) H.transformation_axioms
K.transformation_axioms PROD.P⇩1.extensional
PROD.P⇩1.preserves_arr PROD.proj_tuple2(1) comp_apply)
apply (metis B.not_arr_null PROD.null_char Prod.null_char
second_conv)
by (metis H.extensional K.preserves_arr comp_apply)
qed
also have "... = COMPa.BC.Map (Trn (p⇩1 ⋆ m))"
using m by blast
also have "... = COMPa.BC.Map (COMPa.map (Trn p⇩1, Trn m))"
using arr_m Dom_m Cod_m Trn_hcomp by simp
also have "... = COMPa.BC.Map (Trn p⇩1) ∘ COMPa.BC.Map (Trn m)"
proof -
have "COMPa.BCxAB.arr (COMPa.BC.MkIde P⇩1.map, Trn m)"
using assms arr_m Dom_m Cod_m arr_char arr_char p⇩1_simps(1)
P⇩1.transformation_axioms
by auto
thus ?thesis
unfolding COMPa.map_eq
using assms m arr_m Dom_m Cod_m by simp
qed
also have "... = (PROD.P⇩1 ∘ Unpack) ∘ COMPa.BC.Map (Trn m)"
by simp
also have "... = PROD.P⇩1 ∘ (Unpack ∘ X_Prod.Map (Trn m))"
by (auto simp add: 4 Cod_m Dom_m arr_m src_char)
finally show ?thesis by blast
qed
moreover have "PROD.P⇩0 ∘ (Unpack ∘ X_Prod.Map (Trn ?hk)) =
PROD.P⇩0 ∘ (Unpack ∘ X_Prod.Map (Trn m))"
proof -
have "PROD.P⇩0 ∘ (Unpack ∘ X_Prod.Map (Trn ?hk)) =
PROD.P⇩0 ∘ (Unpack ∘ Pack) ∘
⟨⟨COMPb.BC.Map (Trn h),
COMPb.BC.Map (Trn k)⟩⟩"
using mkarr_def by auto
also have "... = COMPb.BC.Map (Trn k)"
proof
fix x
show "(PROD.P⇩0 ∘ (Unpack ∘ Pack) ∘
⟨⟨COMPb.BC.Map (Trn h), COMPb.BC.Map (Trn k)⟩⟩) x =
COMPb.BC.Map (Trn k) x"
using PROD.P⇩0_def H⇩0.preserves_reflects_arr K⇩0.extensional
PROD.null_char Prod.null_char
apply (auto simp add: pointwise_tuple_def)[1]
apply (metis B.not_arr_null second_conv)
apply (metis H.preserves_arr K.extensional comp_apply)
apply (metis A.not_arr_null PROD.null_char first_conv)
by (metis K.extensional K.preserves_arr comp_apply)
qed
also have "... = COMPb.BC.Map (Trn (p⇩0 ⋆ m))"
using m by blast
also have "... = COMPb.BC.Map (COMPb.map (Trn p⇩0, Trn m))"
using arr_m Dom_m Cod_m Trn_hcomp by simp
also have "... =
COMPb.BC.Map (Trn p⇩0) ∘ COMPb.BC.Map (Trn m)"
proof -
have "COMPb.BCxAB.arr (COMPb.BC.MkIde P⇩0.map, Trn m)"
using assms arr_m Dom_m Cod_m arr_char p⇩0_simps(1)
P⇩0.transformation_axioms
by auto
thus ?thesis
unfolding COMPb.map_eq
using assms m arr_m Dom_m Cod_m by simp
qed
also have "... =
(PROD.P⇩0 ∘ Unpack) ∘ COMPb.BC.Map (Trn m)"
by simp
also have "... = PROD.P⇩0 ∘ (Unpack ∘ X_Prod.Map (Trn m))"
by (auto simp add: 4 Cod_m Dom_m arr_m src_char)
finally show ?thesis by blast
qed
moreover have "transformation (Dom x) PROD.resid
(Unpack ∘ Map (src m)) (Unpack ∘ Map (trg m))
(Unpack ∘ X_Prod.Map (Trn m))"
by (metis "*" UnpackoM.transformation_axioms comp_def)
moreover have "transformation (Dom x) PROD.resid
(Unpack ∘ Map (src m)) (Unpack ∘ Map (trg m))
(Unpack ∘ X_Prod.Map (Trn ?hk))"
proof -
have "Map (src m) = X_Prod.Dom (Trn m) ∧ Map (trg m) = X_Prod.Cod (Trn m)"
by (metis Map_simps(3-4) arr_m comp_def)
hence "Map (src m) = X_Prod.Dom (Trn ?hk) ∧ Map (trg m) = X_Prod.Cod (Trn ?hk)"
using 6 7 by simp
thus ?thesis
using 5 Prod.Map'.simulation_axioms X_Prod.arr_char [of "Trn ?hk"]
PROD.weakly_extensional_rts_axioms
transformation_whisker_left
[of "Dom x" Prod.resid "Map (src m)" "Map (trg m)"
"X_Prod.Map (Trn ?hk)" PROD.resid Unpack]
by metis
qed
ultimately have "Unpack ∘ X_Prod.Map (Trn ?hk) =
Unpack ∘ X_Prod.Map (Trn m)"
using 4 5 X_Prod.arr_char
PROD.proj_joint_monic2
[of "Dom x" "Unpack ∘ Map (src m)" "Unpack ∘ Map (trg m)"
"Unpack ∘ X_Prod.Map (Trn ?hk)" "Unpack ∘ X_Prod.Map (Trn m)"]
by metis
moreover have "Pack ∘ ⟨⟨Map (src h), Map (src k)⟩⟩ = Map (src m)"
by (simp add: 4 Cod_m Dom_m
‹COMPb.BC.Dom (Trn m) = COMPb.BC.Dom (Trn ?hk)›
arr_m src_char mkarr_def)
moreover have "Pack ∘ ⟨⟨Map (trg h), Map (trg k)⟩⟩ = Map (trg m)"
by (simp add: 4 Cod_m Dom_m
‹COMPb.BC.Cod (Trn m) = COMPb.BC.Cod (Trn ?hk)›
arr_m trg_char mkarr_def)
ultimately have "X_Prod.Map (Trn ?hk) = X_Prod.Map (Trn m)"
using assms 2 Dom_m Prod.invertible_simulation_map'
invertible_simulation_cancel_left'
M.transformation_axioms Pack_o_HK.transformation_axioms
mkarr_def
by simp
thus "⋀x. X.ide x ⟹
X_Prod.Map (Trn m) x = X_Prod.Map (Trn ?hk) x"
by simp
qed
qed
qed
qed
lemma has_as_binary_product:
shows "H.has_as_binary_product a b p⇩1 p⇩0"
proof
show "H.span p⇩1 p⇩0" and "cod p⇩1 = a" and"cod p⇩0 = b"
by auto
fix x f g
assume f: "«f : x → a»" and g: "«g : x → b»"
have 1: "∃!h. p⇩1 ⋆ h = f ∧ p⇩0 ⋆ h = g"
using f g universality by blast
show "∃!h. «h : x → dom p⇩1» ∧ p⇩1 ⋆ h = f ∧ p⇩0 ⋆ h = g"
using 1 f by blast
qed
sublocale binary_product hcomp a b p⇩1 p⇩0
using has_as_binary_product
by unfold_locales blast
lemma preserves_extensional_rts:
assumes "extensional_rts (Dom a)" and "extensional_rts (Dom b)"
shows "extensional_rts Prod.resid"
using PROD.preserves_extensional_rts
Prod.preserves_extensional_rts assms(1-2)
by fastforce
lemma preserves_small_rts:
assumes "small_rts (Dom a)" and "small_rts (Dom b)"
shows "small_rts Prod.resid"
using PROD.preserves_small_rts
Prod.preserves_reflects_small_rts assms(1-2)
by fastforce
lemma sta_tuple:
assumes "H.span t u" and "cod t = a" and "cod u = b" and "sta t" and "sta u"
shows "sta (tuple t u)"
proof -
have 0: "«tuple t u : dom t → prod»"
using assms tuple_props(1)
by (simp add: product_def)
have "src (tuple t u) = tuple t u"
by (metis (no_types, lifting) H.arr_iff_in_hom V.src_ide assms(1-5)
p⇩0_simps(1) p⇩1_simps(1) src_hcomp tuple_props(6) universality)
thus ?thesis
using 0 V.ide_iff_src_self by auto
qed
lemma Map_p⇩0:
shows "Map p⇩0 = PROD.P⇩0 ∘ Unpack"
by simp
lemma Map_p⇩1:
shows "Map p⇩1 = PROD.P⇩1 ∘ Unpack"
by simp
lemma Map_tuple:
assumes "«t : x → a»" and "«u : x → b»"
shows "Map (tuple t u) = Pack ∘ ⟨⟨Map t, Map u⟩⟩"
proof -
have *: "Dom t = Dom x ∧ Cod t = Dom a ∧
Dom u = Dom x ∧ Cod u = Dom b"
using assms dom_char cod_char by auto
interpret X: extensional_rts ‹Dom x›
using assms(1) arr_char [of t] dom_char by auto
interpret XA: exponential_rts ‹Dom x› ‹Dom a› ..
interpret XB: exponential_rts ‹Dom x› ‹Dom b› ..
interpret AB: exponential_rts ‹Dom a› ‹Dom b› ..
interpret aXb: extensional_rts ‹Dom prod›
using obj_prod obj_char arr_char [of prod] by blast
interpret X_aXb: exponential_rts ‹Dom x› Prod.resid ..
interpret aXb_A: exponential_rts Prod.resid ‹Dom a› ..
interpret aXb_B: exponential_rts Prod.resid ‹Dom b› ..
interpret COMP⇩1: COMP ‹Dom x› Prod.resid ‹Dom a› ..
interpret COMP⇩0: COMP ‹Dom x› Prod.resid ‹Dom b› ..
have span: "H.span t u"
using assms by blast
have 1: "arr (tuple t u)"
using assms span tuple_props [of t u]
by (elim H.in_homE) auto
have 2: "Dom (tuple t u) = Dom x"
by (metis (no_types, lifting) "1" Dom_dom H.in_homE
assms(1-2) tuple_props(2))
have 3: "Cod (tuple t u) = Prod.resid"
by (metis (no_types, lifting) H.in_homE H_seq_char
assms(1-2) p⇩1_simps(4) tuple_props(4))
have 4: "COMP⇩1.BCxAB.arr (Trn p⇩1, Trn (tuple t u))"
by (metis (no_types, lifting) "*" "1" "2" "3"
COMP⇩1.extensional H.in_homE H_arr_char Trn_hcomp
V.ide_implies_arr XA.not_arr_null assms(1-2)
p⇩1_simps(1) p⇩1_simps(4) p⇩1_simps(5) tuple_props(4))
interpret P⇩1: simulation_as_transformation Prod.resid ‹Dom a› P⇩1.map ..
interpret P⇩0: simulation_as_transformation Prod.resid ‹Dom b› P⇩0.map ..
interpret T: transformation ‹Dom x› ‹Dom a›
‹XA.Dom (Trn t)› ‹XA.Cod (Trn t)› ‹XA.Map (Trn t)›
using assms(1) * arr_char [of t] XA.arr_char [of "Trn t"] by auto
interpret U: transformation ‹Dom x› ‹Dom b›
‹XB.Dom (Trn u)› ‹XB.Cod (Trn u)› ‹XB.Map (Trn u)›
using assms(2) * arr_char [of u] XB.arr_char [of "Trn u"] H.arrI
by auto
have "Map t = PROD.P⇩1 ∘ (Unpack ∘ X_aXb.Map (Trn (tuple t u)))"
by (metis (no_types, lifting) H.in_homE Map_hcomp Map_p⇩1 assms(1-2)
comp_assoc o_apply tuple_props(4))
moreover
have "Map u = PROD.P⇩0 ∘ (Unpack ∘ X_aXb.Map (Trn (tuple t u)))"
by (metis (no_types, lifting) H.in_homE Map_hcomp Map_p⇩0 assms(1-2)
comp_assoc comp_def tuple_props(5))
moreover have "Map t = PROD.P⇩1 ∘ ⟨⟨Map t, Map u⟩⟩"
using T.transformation_axioms U.transformation_axioms
PROD.proj_tuple2 [of "Dom x"]
by simp
moreover have "Map u = PROD.P⇩0 ∘ ⟨⟨Map t, Map u⟩⟩"
using T.transformation_axioms U.transformation_axioms
PROD.proj_tuple2 [of "Dom x"]
by simp
ultimately
have 5: "Unpack ∘ X_aXb.Map (Trn (tuple t u)) = ⟨⟨Map t, Map u⟩⟩"
by (metis (no_types, lifting) PROD.tuple_proj
Prod.Map'.simulation_axioms comp_assoc comp_pointwise_tuple)
show ?thesis
proof -
have "X_aXb.Map (Trn (tuple t u)) =
Pack ∘ Unpack ∘ X_aXb.Map (Trn (tuple t u))"
using 1 2 3 arr_char [of "tuple t u"]
X_aXb.arr_char [of "Trn (tuple t u)"]
Prod.inv' comp_identity_transformation
by fastforce
also have "... = Pack ∘ (Unpack ∘ X_aXb.Map (Trn (tuple t u)))"
by auto
also have "... = Pack ∘ ⟨⟨Map t, Map u⟩⟩"
using 5 by simp
finally show ?thesis by simp
qed
qed
end
text‹
Now we transfer to @{locale rtscatx} just the definitions and facts we want from
@{locale product_in_rtscat}, generalized to all pairs of objects rather than a fixed pair.
›
context rtscatx
begin
definition p⇩0
where "p⇩0 ≡ product_in_rtscat.p⇩0"
definition p⇩1
where "p⇩1 ≡ product_in_rtscat.p⇩1"
lemma sta_p⇩0:
assumes "obj a" and "obj b"
shows "sta (p⇩0 a b)"
by (simp add: assms(1-2) p⇩0_def product_in_rtscat.p⇩0_simps(1)
product_in_rtscat_axioms.intro product_in_rtscat_def
rtscatx.intro universe_axioms)
lemma sta_p⇩1:
assumes "obj a" and "obj b"
shows "sta (p⇩1 a b)"
by (simp add: assms(1-2) p⇩1_def product_in_rtscat.p⇩1_simps(1)
product_in_rtscat_axioms.intro product_in_rtscat_def
rtscatx.intro universe_axioms)
lemma has_binary_products:
assumes "obj a" and "obj b"
shows "H.has_as_binary_product a b (p⇩1 a b) (p⇩0 a b)"
by (simp add: assms(1-2) p⇩0_def p⇩1_def
product_in_rtscat.has_as_binary_product product_in_rtscat_axioms_def
product_in_rtscat_def rtscatx.intro universe_axioms)
interpretation category_with_binary_products hcomp
using H.has_binary_products_def has_binary_products
by unfold_locales auto
proposition is_category_with_binary_products:
shows "category_with_binary_products hcomp"
..
lemma extends_to_elementary_category_with_binary_products:
shows "elementary_category_with_binary_products hcomp p⇩0 p⇩1"
proof
fix a b
assume a: "obj a" and b: "obj b"
interpret axb: product_in_rtscat arr_type a b
using a b by unfold_locales
show "H.span (p⇩1 a b) (p⇩0 a b)" and "cod (p⇩1 a b) = a" and "cod (p⇩0 a b) = b"
unfolding p⇩0_def p⇩1_def
using a b by auto
next
fix t u
assume tu: "H.span t u"
interpret axb: product_in_rtscat arr_type ‹cod t› ‹cod u›
using tu H.ide_cod
by unfold_locales auto
show "∃!l. p⇩1 (cod t) (cod u) ⋆ l = t ∧
p⇩0 (cod t) (cod u) ⋆ l = u"
unfolding p⇩0_def p⇩1_def
using tu axb.universality by blast
qed
interpretation elementary_category_with_binary_products hcomp p⇩0 p⇩1
using extends_to_elementary_category_with_binary_products by blast
notation p⇩0 ("𝔭⇩0[_, _]")
notation p⇩1 ("𝔭⇩1[_, _]")
notation tuple ("⟨_, _⟩")
notation prod (infixr "⊗" 51)
lemma prod_eq:
assumes "obj a" and "obj b"
shows "a ⊗ b = product_in_rtscat.prod a b"
proof -
interpret axb: product_in_rtscat arr_type a b
using assms by unfold_locales auto
show "a ⊗ b = axb.prod"
using assms
by (metis (no_types, lifting) axb.p⇩1_simps(2) p⇩1_def pr_simps(5))
qed
lemma sta_tuple [simp]:
assumes "H.span t u" and "sta t" and "sta u"
shows "sta ⟨t, u⟩"
proof -
let ?a = "cod t" and ?b = "cod u"
have a: "obj ?a" and b: "obj ?b"
using assms by auto
interpret axb: product_in_rtscat arr_type ?a ?b
using assms
by unfold_locales auto
have "⟨t, u⟩ = axb.tuple t u"
using assms(1-2) a b H.in_homE axb.tuple_props(4-5)
tuple_pr_arr p⇩0_def p⇩1_def
by (metis (no_types, lifting))
thus ?thesis
using assms axb.sta_tuple by auto
qed
lemma sta_prod:
assumes "sta t" and "sta u"
shows "sta (t ⊗ u)"
proof -
have "H.span (t ⋆ p⇩1 (dom t) (dom u)) (u ⋆ p⇩0 (dom t) (dom u))"
using H.seqI assms(1-2) pr_simps(1,4) by force
moreover have "V.ide (t ⋆ p⇩1 (dom t) (dom u))"
using assms pr_in_hom sta_p⇩1 H_seq_char calculation by auto
moreover have "V.ide (u ⋆ p⇩0 (dom t) (dom u))"
using assms pr_in_hom sta_p⇩0 H_seq_char calculation by auto
ultimately show ?thesis
unfolding prod_def
using assms sta_tuple by blast
qed
definition Pack :: "'A arr ⇒ 'A arr ⇒ 'A × 'A ⇒ 'A"
where "Pack ≡ product_in_rtscat.Pack"
definition Unpack :: "'A arr ⇒ 'A arr ⇒ 'A ⇒ 'A × 'A"
where "Unpack ≡ product_in_rtscat.Unpack"
lemma inverse_simulations_Pack_Unpack:
assumes "obj a" and "obj b"
shows "inverse_simulations (Dom (a ⊗ b)) (product_rts.resid (Dom a) (Dom b))
(Pack a b) (Unpack a b)"
proof -
interpret axb: product_in_rtscat arr_type a b
using assms by unfold_locales auto
show ?thesis
unfolding Pack_def Unpack_def
using p⇩0_def p⇩1_def
by (metis (no_types, lifting) axb.Dom_prod
axb.Prod.inverse_simulations_axioms axb.obj_a axb.obj_b
axb.p⇩0_simps(2) pr_simps(2))
qed
lemma simulation_Pack:
assumes "obj a" and "obj b"
shows "simulation (product_rts.resid (Dom a) (Dom b)) (Dom (a ⊗ b))
(Pack a b)"
using assms inverse_simulations_Pack_Unpack [of a b]
inverse_simulations_def
by fast
lemma simulation_Unpack:
assumes "obj a" and "obj b"
shows "simulation (Dom (a ⊗ b)) (product_rts.resid (Dom a) (Dom b))
(Unpack a b)"
using assms inverse_simulations_Pack_Unpack [of a b]
inverse_simulations_def
by fast
lemma Pack_o_Unpack:
assumes "obj a" and "obj b"
shows "Pack a b ∘ Unpack a b = I (Dom (a ⊗ b))"
proof -
interpret PU: inverse_simulations
‹Dom (a ⊗ b)› ‹product_rts.resid (Dom a) (Dom b)›
‹Pack a b› ‹Unpack a b›
using assms inverse_simulations_Pack_Unpack by blast
show ?thesis
using assms PU.inv' by simp
qed
lemma Unpack_o_Pack:
assumes "obj a" and "obj b"
shows "Unpack a b ∘ Pack a b = I (product_rts.resid (Dom a) (Dom b))"
proof -
interpret PU: inverse_simulations
‹Dom (a ⊗ b)› ‹product_rts.resid (Dom a) (Dom b)›
‹Pack a b› ‹Unpack a b›
using assms inverse_simulations_Pack_Unpack by blast
show ?thesis
using assms PU.inv by simp
qed
lemma Pack_Unpack [simp]:
assumes "obj a" and "obj b"
and "residuation.arr (Dom (a ⊗ b)) t"
shows "Pack a b (Unpack a b t) = t"
by (meson assms(1-3) inverse_simulations.inv'_simp
inverse_simulations_Pack_Unpack)
lemma Unpack_Pack [simp]:
assumes "obj a" and "obj b"
and "residuation.arr (product_rts.resid (Dom a) (Dom b)) t"
shows "Unpack a b (Pack a b t) = t"
by (metis (no_types, lifting) Unpack_o_Pack assms(1-3) o_apply)
lemma src_tuple [simp]:
assumes "H.span t u"
shows "src ⟨t, u⟩ = ⟨src t, src u⟩"
using assms sta_p⇩0 sta_p⇩1 tuple_simps(1) src_hcomp H.seqI
src_hcomp [of "p⇩0 (cod t) (cod u)" "tuple t u"]
src_hcomp [of "p⇩1 (cod t) (cod u)" "tuple t u"]
by (intro tuple_eqI) auto
lemma trg_tuple [simp]:
assumes "H.span t u"
shows "trg ⟨t, u⟩ = ⟨trg t, trg u⟩"
using assms sta_p⇩0 sta_p⇩1 tuple_simps(1) src_hcomp H.seqI
trg_hcomp [of "p⇩0 (cod t) (cod u)" "tuple t u"]
trg_hcomp [of "p⇩1 (cod t) (cod u)" "tuple t u"]
by (intro tuple_eqI) auto
lemma Map_p⇩0:
assumes "obj a" and "obj b"
shows "Map 𝔭⇩0[a, b] = product_rts.P⇩0 (Dom a) (Dom b) ∘ Unpack a b"
proof -
interpret axb: product_in_rtscat arr_type a b
using assms by unfold_locales auto
show ?thesis
unfolding Unpack_def p⇩0_def
using axb.Map_p⇩0 by blast
qed
lemma Map_p⇩1:
assumes "obj a" and "obj b"
shows "Map 𝔭⇩1[a, b] = product_rts.P⇩1 (Dom a) (Dom b) ∘ Unpack a b"
proof -
interpret axb: product_in_rtscat arr_type a b
using assms by unfold_locales auto
show ?thesis
unfolding Unpack_def p⇩1_def
using axb.Map_p⇩1 by blast
qed
lemma Map_tuple:
assumes "«t : x → a»" and "«u : x → b»"
shows "Map ⟨t, u⟩ = Pack a b ∘ ⟨⟨Map t, Map u⟩⟩"
proof -
interpret axb: product_in_rtscat arr_type a b
using assms by unfold_locales auto
show ?thesis
unfolding Pack_def
using assms axb.Map_tuple [of t x u] p⇩0_def p⇩1_def
by (metis (no_types, lifting) H.in_homE axb.tuple_props(6) pr_tuple(1-2))
qed
lemma assoc_expansion:
assumes "obj a" and "obj b" and "obj c"
shows "assoc a b c =
⟨𝔭⇩1[a, b] ⋆ 𝔭⇩1[a ⊗ b, c], ⟨𝔭⇩0[a, b] ⋆ 𝔭⇩1[a ⊗ b, c], 𝔭⇩0[a ⊗ b, c]⟩ ⟩"
using assms assoc_def by blast
end
subsection "Exponentials"
text‹
In this section we show that the category ‹❙R❙T❙S⇧†› has exponentials.
The strategy is the same as for products: given objects ‹b› and ‹c›, construct the
exponential RTS ‹[Dom b, Dom c]›, apply an injective map on the arrows to obtain an
isomorphic RTS with arrow type @{typ 'A}, then let ‹exp b c› be the object corresponding
to this RTS. In order for the type-reducing injection to exist, we use the assumption
that the type @{typ 'A} admits exponentiation, but this is also where we use the
assumption that the RTS's ‹Dom b› and ‹Dom c› are small, so that the exponential RTS
‹[Dom b, Dom c]› is also small.
›
context rtscatx
begin
definition inj_exp :: "('A, 'A) exponential_rts.arr ⇒ 'A"
where "inj_exp ≡ λ exponential_rts.MkArr F G T ⇒
lifting.some_lift
(Some (pairing.some_pair
(exponentiation.some_inj F,
pairing.some_pair
(exponentiation.some_inj G,
exponentiation.some_inj T))))
| exponential_rts.Null ⇒ lifting.some_lift None"
lemma inj_inj_exp:
assumes "small_rts A" and "extensional_rts A"
and "small_rts B" and "extensional_rts B"
shows "inj_on inj_exp
(Collect (residuation.arr (exponential_rts.resid A B)) ∪ {exponential_rts.Null})"
proof
interpret A: small_rts A
using assms by blast
interpret A: extensional_rts A
using assms by blast
interpret B: small_rts B
using assms by blast
interpret B: extensional_rts B
using assms by blast
interpret AB: exponential_rts A B ..
fix x y
assume x: "x ∈ Collect AB.arr ∪ {AB.Null}"
and y: "y ∈ Collect AB.arr ∪ {AB.Null}"
assume eq: "inj_exp x = inj_exp y"
show "x = y"
proof (cases x; cases y)
show "⟦x = AB.Null; y = AB.Null⟧ ⟹ x = y"
by blast
show "⋀F' G' T'. ⟦x = AB.Null; y = AB.MkArr F' G' T'⟧ ⟹ x = y"
using x y eq inj_some_lift
unfolding inj_exp_def inj_def
by simp blast
show "⋀F G T. ⟦x = AB.MkArr F G T; y = AB.Null⟧ ⟹ x = y"
using x y eq inj_some_lift
unfolding inj_exp_def inj_def
by simp blast
fix F G T F' G' T'
show "⟦x = AB.MkArr F G T; y = AB.MkArr F' G' T'⟧ ⟹ x = y"
proof -
assume x_eq: "x = AB.MkArr F G T" and y_eq: "y = AB.MkArr F' G' T'"
have "some_lift
(Some
(some_pair
(some_inj F, some_pair (some_inj G, some_inj T)))) =
some_lift
(Some
(some_pair
(some_inj F', some_pair (some_inj G', some_inj T'))))"
using eq x_eq y_eq
unfolding inj_exp_def
by simp
hence "Some
(some_pair
(some_inj F, some_pair (some_inj G, some_inj T))) =
Some
(some_pair
(some_inj F', some_pair (some_inj G', some_inj T')))"
using inj_some_lift inj_def by metis
hence "some_pair (some_inj F, some_pair (some_inj G, some_inj T)) =
some_pair (some_inj F', some_pair (some_inj G', some_inj T'))"
by simp
hence "some_inj F = some_inj F' ∧
some_pair (some_inj G, some_inj T) =
some_pair (some_inj G', some_inj T')"
using inj_some_pair inj_def [of some_pair] by blast
hence 1: "some_inj F = some_inj F' ∧ some_inj G = some_inj G' ∧
some_inj T = some_inj T'"
using inj_some_pair inj_def [of some_pair] by blast
have "F = F' ∧ G = G' ∧ T = T'"
proof -
have "small_function F ∧ small_function F' ∧
small_function G ∧ small_function G'"
using x_eq x y_eq y AB.arr_char small_function_simulation
transformation_def
by (metis A.small_rts_axioms AB.arr.simps(2)
AB.arr_MkArr B.small_rts_axioms UnE mem_Collect_eq singletonD)
moreover have "small_function T ∧ small_function T'"
using assms x_eq x y_eq y AB.arr_char small_function_transformation
by fast
ultimately show ?thesis
using 1 inj_some_inj inj_on_def [of some_inj] by auto
qed
thus "x = y"
using x_eq y_eq by auto
qed
qed
qed
end
locale exponential_in_rtscat =
rtscatx arr_type
for arr_type :: "'A itself"
and b :: "'A rtscatx.arr"
and c :: "'A rtscatx.arr" +
assumes obj_b: "obj b"
and obj_c: "obj c"
begin
sublocale elementary_category_with_binary_products hcomp p⇩0 p⇩1
using extends_to_elementary_category_with_binary_products by blast
notation hcomp (infixr "⋆" 53)
notation p⇩0 ("𝔭⇩0[_, _]")
notation p⇩1 ("𝔭⇩1[_, _]")
notation tuple ("⟨_, _⟩")
notation prod (infixr "⊗" 51)
sublocale B: extensional_rts ‹Dom b›
using obj_b bij_mkobj obj_char by blast
sublocale B: small_rts ‹Dom b›
using obj_b bij_mkobj obj_char by blast
sublocale C: extensional_rts ‹Dom c›
using obj_c bij_mkobj obj_char by blast
sublocale C: small_rts ‹Dom c›
using obj_c bij_mkobj obj_char by blast
sublocale EXP: exponential_rts ‹Dom b› ‹Dom c› ..
sublocale EXP: exponential_of_small_rts ‹Dom b› ‹Dom c› ..
lemma small_function_Map:
assumes "EXP.arr t"
shows "small_function (EXP.Dom t)" and "small_function (EXP.Cod t)"
and "small_function (EXP.Map t)"
using assms small_function_simulation small_function_transformation
transformation_def B.small_rts_axioms C.small_rts_axioms
EXP.con_arr_src(2) EXP.con_char
by metis+
text ‹
Sublocale ‹Exp› refers to the isomorphic image of the RTS ‹EXP› under the type-reducing
injective map ‹inj_exp›. These are connected by simulation ‹Func›, which maps ‹Exp›
to ‹EXP›, and its inverse ‹Unfunc›, which maps ‹EXP› to ‹Exp›.
›
sublocale Exp: inj_image_rts inj_exp EXP.resid
using inj_inj_exp [of "Dom b" "Dom c"] EXP.null_char
B.small_rts_axioms B.extensional_rts_axioms
C.small_rts_axioms C.extensional_rts_axioms
by unfold_locales argo
sublocale Exp: extensional_rts Exp.resid
using EXP.is_extensional_rts Exp.preserves_extensional_rts by blast
sublocale Exp: small_rts Exp.resid
using EXP.small_rts_axioms Exp.preserves_reflects_small_rts by blast
lemma is_extensional_rts:
shows "extensional_rts Exp.resid"
..
lemma is_small_rts:
shows "small_rts Exp.resid"
..
abbreviation Func :: "'A ⇒ ('A, 'A) EXP.arr"
where "Func ≡ Exp.map'⇩e⇩x⇩t"
abbreviation Unfunc :: "('A, 'A) EXP.arr ⇒ 'A"
where "Unfunc ≡ Exp.map⇩e⇩x⇩t"
text ‹
We define ‹exp› to be the object of the category ‹❙R❙T❙S⇧†› having ‹Exp› as its
underlying RTS.
›
definition exp
where "exp ≡ mkobj Exp.resid"
lemma obj_exp:
shows "obj exp"
using exp_def Exp.rts_axioms is_small_rts is_extensional_rts bij_mkobj by auto
text‹
The fact that @{term "Dom exp"} and @{term Exp.resid} are equal, but not identical,
poses a minor inconvenience for the moment.
›
lemma Dom_exp [simp]:
shows "Dom exp = Exp.resid"
unfolding exp_def by fastforce
sublocale EXPxB: product_rts EXP.resid ‹Dom b› ..
sublocale ExpxB: product_rts Exp.resid ‹Dom b› ..
sublocale B: identity_simulation ‹Dom b› ..
sublocale B: simulation_as_transformation ‹Dom b› ‹Dom b› B.map ..
sublocale B: transformation_to_extensional_rts
‹Dom b› ‹Dom b› B.map B.map B.map ..
sublocale UnfuncxB: product_simulation
EXP.resid ‹Dom b› Exp.resid ‹Dom b› Unfunc B.map ..
sublocale FuncxB: product_simulation
Exp.resid ‹Dom b› EXP.resid ‹Dom b› Func B.map ..
sublocale inverse_simulations EXPxB.resid ExpxB.resid
FuncxB.map UnfuncxB.map
using UnfuncxB.map_def FuncxB.map_def Exp.arr_char Exp.not_arr_null
by unfold_locales force+
lemma obj_expxb:
shows "obj (exp ⊗ b)"
using obj_exp obj_b by blast
text ‹
We now have a simulation ‹FuncxB_o_Unpack›, which refers to the result of composing
the isomorphism ‹Unpack exp b› from ‹Dom expxb› to ‹ExpxB›, with the isomorphism
‹FuncxB› from ‹ExpxB› to ‹EXPxB›. This composite essentially ``unpacks''
the RTS ‹Dom expxb›, which underlies the product object ‹expxb›,
to expose its construction as an application of the exponential RTS construction,
followed by an application of the product RTS construction.
›
sublocale FuncxB_o_Unpack: composite_simulation
‹Dom (exp ⊗ b)› ExpxB.resid EXPxB.resid
‹Unpack exp b› FuncxB.map
proof -
have "product_rts.resid (Dom exp) (Dom b) = ExpxB.resid"
by simp
thus "composite_simulation (Dom (exp ⊗ b)) ExpxB.resid EXPxB.resid
(Unpack exp b) FuncxB.map"
using FuncxB.simulation_axioms simulation_Unpack [of exp b]
simulation_comp
by (simp add: composite_simulation_def obj_b obj_exp)
qed
text ‹
We construct the evaluation map associated with ‹ExpxB› by composing the evaluation
map ‹Eval.map› from ‹EXPxB› to ‹C›, derived from the exponential RTS construction,
with the isomorphism ‹FuncxB_o_Unpack› from ‹Dom expxb.prod› to ‹EXPxB›
and then obtain the corresponding arrow of the category.
›
sublocale Eval: evaluation_map ‹Dom b› ‹Dom c› ..
sublocale Eval: evaluation_map_between_extensional_rts ‹Dom b› ‹Dom c› ..
sublocale Eval_o_FuncxB_o_Unpack:
composite_simulation
‹Dom (exp ⊗ b)› EXPxB.resid ‹Dom c›
FuncxB_o_Unpack.map Eval.map
using Eval.simulation_axioms FuncxB_o_Unpack.simulation_axioms
composite_simulation_def
by fastforce
lemma EvaloFuncxB_o_Unpack_is_simulation:
shows "simulation (Dom (exp ⊗ b)) (Dom c) Eval_o_FuncxB_o_Unpack.map"
using Eval_o_FuncxB_o_Unpack.simulation_axioms by blast
definition eval
where "eval ≡ mksta (Dom (exp ⊗ b)) (Dom c) Eval_o_FuncxB_o_Unpack.map"
lemma eval_simps [simp]:
shows "sta eval" and "dom eval = exp ⊗ b" and "cod eval = c"
and "Dom eval = Dom (exp ⊗ b)" and "Cod eval = Dom c"
and "Trn eval = exponential_rts.MkIde Eval_o_FuncxB_o_Unpack.map"
proof -
show 1: "sta eval"
unfolding eval_def
using sta_mksta [of "Dom (exp ⊗ b)" "Dom c" Eval_o_FuncxB_o_Unpack.map]
obj_b obj_c obj_exp obj_char arr_char Eval_o_FuncxB_o_Unpack.is_simulation
by blast
show 2: "Dom eval = Dom (exp ⊗ b)" and 3: "Cod eval = Dom c"
unfolding eval_def mkarr_def by auto
show "Trn eval = exponential_rts.MkIde Eval_o_FuncxB_o_Unpack.map"
unfolding eval_def mkarr_def by auto
have 4: "(λa. if FuncxB_o_Unpack.F.A.arr a then a
else ResiduatedTransitionSystem.partial_magma.null
(Dom eval)) =
I (Dom (exp ⊗ b))"
using "2" by presburger
have 5: "(λt. if C.arr t then t
else ResiduatedTransitionSystem.partial_magma.null
(Cod eval)) =
I (Dom c)"
using 3 by presburger
show "dom eval = exp ⊗ b"
using 1 2 4 dom_char obj_char obj_expxb by auto
show "cod eval = c"
using 1 3 5 cod_char obj_char obj_c by auto
qed
lemma eval_in_hom [intro]:
shows "«eval : exp ⊗ b → c»"
using eval_simps by auto
lemma Map_eval:
shows "Map eval = Eval.map ∘ (FuncxB.map ∘ Unpack exp b)"
unfolding eval_def mkarr_def by simp
end
text‹
Now we transfer the definitions and facts we want to @{locale rtscatx}.
›
context rtscatx
begin
interpretation elementary_category_with_binary_products hcomp p⇩0 p⇩1
using extends_to_elementary_category_with_binary_products by blast
notation prod (infixr "⊗" 51)
definition exp
where "exp b c ≡ exponential_in_rtscat.exp b c"
lemma obj_exp:
assumes "obj b" and "obj c"
shows "obj (exp b c)"
proof -
interpret bc: exponential_in_rtscat arr_type b c
using assms by unfold_locales auto
show ?thesis
unfolding exp_def
using bc.obj_exp by blast
qed
definition eval
where "eval b c ≡ exponential_in_rtscat.eval b c"
lemma eval_simps [simp]:
assumes "obj b" and "obj c"
shows "sta (eval b c)"
and "dom (eval b c) = exp b c ⊗ b"
and "cod (eval b c) = c"
proof -
interpret bc: exponential_in_rtscat arr_type b c
using assms by unfold_locales auto
show "sta (eval b c)"
and "dom (eval b c) = exp b c ⊗ b"
and "cod (eval b c) = c"
unfolding eval_def exp_def
using bc.eval_simps by auto
qed
lemma eval_in_hom⇩R⇩C⇩R [intro]:
assumes "obj b" and "obj c"
shows "«eval b c : exp b c ⊗ b → c»"
using assms eval_simps by auto
definition Func :: "'a arr ⇒ 'a arr ⇒ 'a ⇒ ('a, 'a) exponential_rts.arr"
where "Func ≡ exponential_in_rtscat.Func"
definition Unfunc :: "'a arr ⇒ 'a arr ⇒ ('a, 'a) exponential_rts.arr ⇒ 'a"
where "Unfunc ≡ exponential_in_rtscat.Unfunc"
lemma inverse_simulations_Func_Unfunc:
assumes "obj b" and "obj c"
shows "inverse_simulations
(exponential_rts.resid (Dom b) (Dom c)) (Dom (exp b c))
(Func b c) (Unfunc b c)"
proof -
interpret bc: exponential_in_rtscat arr_type b c
using assms by unfold_locales blast
have "bc.Exp.resid = Dom (exp b c)"
using assms exp_def bc.Dom_exp by metis
thus ?thesis
unfolding Func_def Unfunc_def
using bc.Exp.inverse_simulations_axioms inverse_simulations_sym by auto
qed
lemma simulation_Func:
assumes "obj b" and "obj c"
shows "simulation (Dom (exp b c)) (exponential_rts.resid (Dom b) (Dom c))
(Func b c)"
using assms inverse_simulations_Func_Unfunc [of b c]
inverse_simulations_def
by fast
lemma simulation_Unfunc:
assumes "obj b" and "obj c"
shows "simulation (exponential_rts.resid (Dom b) (Dom c)) (Dom (exp b c))
(Unfunc b c)"
using assms inverse_simulations_Func_Unfunc [of b c]
inverse_simulations_def
by fast
lemma Func_o_Unfunc:
assumes "obj b" and "obj c"
shows "Func b c ∘ Unfunc b c = I (exponential_rts.resid (Dom b) (Dom c))"
proof -
interpret FU: inverse_simulations
‹exponential_rts.resid (Dom b) (Dom c)› ‹Dom (exp b c)›
‹Func b c› ‹Unfunc b c›
using assms inverse_simulations_Func_Unfunc by blast
show ?thesis
using assms FU.inv' by simp
qed
lemma Unfunc_o_Func:
assumes "obj b" and "obj c"
shows "Unfunc b c ∘ Func b c = I (Dom (exp b c))"
proof -
interpret FU: inverse_simulations
‹exponential_rts.resid (Dom b) (Dom c)› ‹Dom (exp b c)›
‹Func b c› ‹Unfunc b c›
using assms inverse_simulations_Func_Unfunc by blast
show ?thesis
using assms FU.inv by simp
qed
lemma Func_Unfunc [simp]:
assumes "obj b" and "obj c"
and "residuation.arr (exponential_rts.resid (Dom b) (Dom c)) t"
shows "Func b c (Unfunc b c t) = t"
by (meson assms(1-3) inverse_simulations.inv'_simp
inverse_simulations_Func_Unfunc)
lemma Unfunc_Func [simp]:
assumes "obj b" and "obj c"
and "residuation.arr (Dom (exp b c)) t"
shows "Unfunc b c (Func b c t) = t"
proof -
have "Unfunc b c (Func b c t) = (Unfunc b c ∘ Func b c) t"
using assms by simp
also have "... = t"
using assms Unfunc_o_Func [of b c] by auto
finally show ?thesis by auto
qed
lemma Map_eval:
assumes "obj b" and "obj c"
shows "Map (eval b c) =
evaluation_map.map (Dom b) (Dom c) ∘
(product_simulation.map
(Dom (exp b c)) (Dom b) (Func b c) (I (Dom b)) ∘
Unpack (exp b c) b)"
proof -
interpret bc: exponential_in_rtscat arr_type b c
using assms by unfold_locales blast
have "Map (eval b c) = bc.Eval.map ∘ (bc.FuncxB.map ∘ Unpack (exp b c) b)"
using assms bc.Map_eval comp_assoc exp_def local.eval_def
by (simp add: exp_def eval_def)
thus ?thesis
unfolding Func_def
by (simp add: exp_def)
qed
end
locale currying_in_rtscat =
exponential_in_rtscat arr_type b c
for arr_type :: "'A itself"
and a :: "'A rtscatx.arr"
and b :: "'A rtscatx.arr"
and c :: "'A rtscatx.arr" +
assumes obj_a: "obj a"
begin
sublocale A: extensional_rts ‹Dom a›
using obj_a obj_char arr_char by blast
sublocale A: small_rts ‹Dom a›
using obj_a obj_char arr_char by blast
sublocale B: extensional_rts ‹Dom b›
using obj_b obj_char arr_char by blast
sublocale B: small_rts ‹Dom b›
using obj_b obj_char arr_char by blast
sublocale AxB: product_of_extensional_rts ‹Dom a› ‹Dom b› ..
sublocale A_Exp: exponential_rts ‹Dom a› Exp.resid ..
sublocale aXb: extensional_rts ‹Dom (a ⊗ b)›
using obj_a obj_b obj_char arr_char by blast
sublocale aXb: small_rts ‹Dom (a ⊗ b)›
using obj_a obj_b obj_char arr_char by blast
sublocale expXb: exponential_rts Exp.resid ‹Dom b› ..
sublocale aXb_C: exponential_rts ‹Dom (a ⊗ b)› ‹Dom c› ..
sublocale Currying ‹Dom a› ‹Dom b› ‹Dom c› ..
definition curry :: "'A arr ⇒ 'A arr"
where "curry f = mkarr (Dom a) Exp.resid
(Unfunc ∘ Curry3 (aXb_C.Dom (Trn f) ∘ Pack a b))
(Unfunc ∘ Curry3 (aXb_C.Cod (Trn f) ∘ Pack a b))
(Unfunc ∘ Curry (aXb_C.Dom (Trn f) ∘ Pack a b)
(aXb_C.Cod (Trn f) ∘ Pack a b)
(aXb_C.Map (Trn f) ∘ Pack a b))"
lemma curry_in_hom [intro]:
assumes "«f : a ⊗ b → c»"
shows "«curry f : a → exp»"
proof -
have Dom: "Dom f = Dom (a ⊗ b)" and Cod: "Cod f = Dom c"
using assms
apply (metis (no_types, lifting) Dom_dom H.in_homE H_arr_char arr_char)
using cod_char assms by fastforce
interpret F: transformation ‹Dom (a ⊗ b)› ‹Dom c›
‹aXb_C.Dom (Trn f)› ‹aXb_C.Cod (Trn f)› ‹aXb_C.Map (Trn f)›
using assms arr_char aXb_C.arr_char dom_char cod_char H.in_homE Dom
by auto
let ?Src = "Unfunc ∘ Curry3 (aXb_C.Dom (Trn f) ∘ Pack a b)"
let ?Trg = "Unfunc ∘ Curry3 (aXb_C.Cod (Trn f) ∘ Pack a b)"
let ?Map = "Unfunc ∘ Curry (aXb_C.Dom (Trn f) ∘ Pack a b)
(aXb_C.Cod (Trn f) ∘ Pack a b)
(aXb_C.Map (Trn f) ∘ Pack a b)"
interpret Src: simulation ‹Dom a› Exp.resid ?Src
using obj_a obj_b simulation_Pack F.F.simulation_axioms
Exp.Map.simulation_axioms
by (intro simulation_comp) auto
interpret Trg: simulation ‹Dom a› Exp.resid ?Trg
using obj_a obj_b simulation_Pack F.G.simulation_axioms
Exp.Map.simulation_axioms
by (intro simulation_comp) auto
interpret Map: transformation ‹Dom a› Exp.resid ?Src ?Trg ?Map
proof -
interpret FoMap: transformation AxB.resid ‹Dom c›
‹aXb_C.Dom (Trn f) ∘ Pack a b›
‹aXb_C.Cod (Trn f) ∘ Pack a b›
‹aXb_C.Map (Trn f) ∘ Pack a b›
using obj_a obj_b F.transformation_axioms simulation_Pack
transformation_whisker_right
[of "Dom (a ⊗ b)" "Dom c"
"aXb_C.Dom (Trn f)" "aXb_C.Cod (Trn f)"
"aXb_C.Map (Trn f)" AxB.resid "Pack a b"]
AxB.weakly_extensional_rts_axioms
by blast
have "transformation (Dom a) EXP.resid
(Eval.coext (Dom a) (aXb_C.Dom (Trn f) ∘ Pack a b))
(Eval.coext (Dom a) (aXb_C.Cod (Trn f) ∘ Pack a b))
(Curry (aXb_C.Dom (Trn f) ∘ Pack a b)
(aXb_C.Cod (Trn f) ∘ Pack a b)
(aXb_C.Map (Trn f) ∘ Pack a b))"
using Curry_preserves_transformations FoMap.transformation_axioms
by blast
thus "transformation (Dom a) Exp.resid ?Src ?Trg ?Map"
using Exp.Map.simulation_axioms Exp.weakly_extensional_rts_axioms
transformation_whisker_left
by fastforce
qed
show ?thesis
unfolding curry_def exp_def
using obj_a obj_exp obj_char arr_char Map.transformation_axioms arr_mkarr
by (intro H.in_homI) auto
qed
lemma curry_simps [simp]:
assumes "«t : a ⊗ b → c»"
shows "arr (curry t)" and "dom (curry t) = a" and "cod (curry t) = exp"
and "Dom (curry t) = Dom a" and "Cod (curry t) = Exp.resid"
and "src (curry t) = curry (src t)" and "trg (curry t) = curry (trg t)"
and "Map (curry t) =
(Unfunc ∘ Curry (aXb_C.Dom (Trn t) ∘ Pack a b)
(aXb_C.Cod (Trn t) ∘ Pack a b)
(aXb_C.Map (Trn t) ∘ Pack a b))"
proof -
let ?Src = "Unfunc ∘ Curry3 (aXb_C.Dom (Trn t) ∘ Pack a b)"
let ?Trg = "Unfunc ∘ Curry3 (aXb_C.Cod (Trn t) ∘ Pack a b)"
let ?Map = "Unfunc ∘ Curry (aXb_C.Dom (Trn t) ∘ Pack a b)
(aXb_C.Cod (Trn t) ∘ Pack a b)
(aXb_C.Map (Trn t) ∘ Pack a b)"
show "arr (curry t)" and "dom (curry t) = a" and "cod (curry t) = exp"
and "Dom (curry t) = Dom a" and "Cod (curry t) = Exp.resid"
and "Map (curry t) = ?Map"
using assms obj_a curry_in_hom sta_mksta H.in_homE H_arr_char arr_char
A.extensional_rts_axioms A.small_rts_axioms
Exp.extensional_rts_axioms Exp.small_rts_axioms
apply (auto simp add: curry_def mkarr_def)[6]
by (metis (no_types, lifting) A_Exp.arr_MkArr
Cod.simps(1) Dom.simps(1) Trn.simps(1))
have 1: "transformation (Dom a) Exp.resid ?Src ?Trg ?Map"
using ‹arr (curry t)› A_Exp.src_char curry_def curry_in_hom
arr_char mkarr_def
by simp
show "src (curry t) = curry (src t)"
proof -
have "src (curry t) =
MkArr (Dom a) (Exp.resid) (A_Exp.src (Trn (curry t)))"
unfolding src_char
using assms ‹arr (curry t)› ‹Dom (curry t) = Dom a›
‹Cod (curry t) = Exp.resid›
by simp
also have "... = mksta (Dom a) Exp.resid ?Src"
using 1 A_Exp.src_char curry_def curry_in_hom arr_char
aXb_C.arr_char mkarr_def
by auto
also have "... = curry (src t)"
unfolding src_char curry_def mkarr_def
using assms
apply auto[1]
apply (metis (no_types, lifting) Dom_cod Dom_dom H.in_homE
H_arr_char aXb_C.Dom.simps(1) aXb_C.src_simp)
apply (metis (no_types, lifting) Cod_cod Cod_dom H.ide_char
H.in_homE H_arr_char aXb_C.MkIde_Dom expXb.Cod.simps(1)
ide_prod obj_a obj_b obj_c obj_char)
by (metis (no_types, lifting) Cod_cod Cod_dom H.ide_char
H.in_homE H_arr_char aXb_C.Map_src aXb_C.src_simp
expXb.Cod.simps(1) expXb.Dom.simps(1) ide_prod
obj_a obj_b obj_c obj_char)
finally show ?thesis by blast
qed
show "trg (curry t) = curry (trg t)"
proof -
have "trg (curry t) =
MkArr (Dom a) (Exp.resid) (A_Exp.trg (Trn (curry t)))"
unfolding trg_char
using assms ‹arr (curry t)› ‹Dom (curry t) = Dom a›
‹Cod (curry t) = Exp.resid›
by simp
also have "... = mksta (Dom a) Exp.resid ?Trg"
using 1 A_Exp.trg_char curry_def curry_in_hom arr_char
aXb_C.arr_char mkarr_def
by auto
also have "... = curry (trg t)"
proof -
have "arr t"
using assms by auto
moreover have "aXb_C.Dom (Trn (trg t)) = aXb_C.Map (Trn (trg t)) ∧
aXb_C.Cod (Trn (trg t)) = aXb_C.Map (Trn (trg t))"
by (metis (no_types, lifting) Cod_trg Dom_cod Dom_dom Dom_trg
H.in_homE aXb_C.ide_char⇩E⇩R⇩T⇩S assms calculation ide_trg staE)
moreover have "aXb_C.Cod (Trn t) =
aXb_C.Map
(residuation.trg
(exponential_rts.resid (Dom t) (Cod t)) (Trn t))"
by (metis (no_types, lifting) Dom_cod Dom_dom H.in_homE H_arr_char
aXb_C.Map_trg arr_char assms)
ultimately show ?thesis
unfolding curry_def
using assms trg_char by simp
qed
finally show ?thesis by blast
qed
qed
lemma sta_curry:
assumes "«f : a ⊗ b → c»" and "sta f"
shows "sta (curry f)"
using assms V.ide_iff_src_self [of "curry f"] by auto
definition uncurry :: "'A arr ⇒ 'A arr"
where "uncurry g = mkarr (Dom (a ⊗ b)) (Dom c)
(Uncurry (Func ∘ exponential_rts.Dom (Trn g)) ∘ Unpack a b)
(Uncurry (Func ∘ exponential_rts.Cod (Trn g)) ∘ Unpack a b)
(Uncurry (Func ∘ exponential_rts.Map (Trn g)) ∘ Unpack a b)"
lemma uncurry_in_hom [intro]:
assumes "«g : a → exp»"
shows "«uncurry g : a ⊗ b → c»"
proof -
interpret G: transformation ‹Dom a› Exp.resid
‹A_Exp.Dom (Trn g)› ‹A_Exp.Cod (Trn g)› ‹A_Exp.Map (Trn g)›
using assms arr_char exp_def A_Exp.arr_char dom_char cod_char
by (metis (no_types, lifting) H.in_homE H_arr_char
mkobj_simps(2) obj_a obj_char)
interpret Cmp'oG: transformation ‹Dom a› EXP.resid
‹Func ∘ A_Exp.Dom (Trn g)›
‹Func ∘ A_Exp.Cod (Trn g)›
‹Func ∘ A_Exp.Map (Trn g)›
using Exp.Map'.simulation_axioms G.transformation_axioms
EXP.weakly_extensional_rts_axioms transformation_whisker_left
by simp
have "transformation AxB.resid (Dom c)
(Uncurry (Func ∘ A_Exp.Dom (Trn g)))
(Uncurry (Func ∘ A_Exp.Cod (Trn g)))
(Uncurry (Func ∘ A_Exp.Map (Trn g)))"
using Cmp'oG.transformation_axioms Uncurry_preserves_transformations
by blast
hence "transformation (Dom (a ⊗ b)) (Dom c)
(Uncurry (Func ∘ A_Exp.Dom (Trn g)) ∘ Unpack a b)
(Uncurry (Func ∘ A_Exp.Cod (Trn g)) ∘ Unpack a b)
(Uncurry (Func ∘ A_Exp.Map (Trn g)) ∘ Unpack a b)"
using obj_a obj_b simulation_Unpack [of a b]
aXb.weakly_extensional_rts_axioms transformation_whisker_right
by auto
thus ?thesis
unfolding uncurry_def
using obj_c obj_char arr_char aXb.extensional_rts_axioms
aXb.small_rts_axioms arr_mkarr
apply (intro H.in_homI)
apply auto[3]
using obj_a obj_b by blast
qed
lemma uncurry_simps [simp]:
assumes "«u : a → exp»"
shows "arr (uncurry u)"
and "dom (uncurry u) = a ⊗ b" and "cod (uncurry u) = c"
and "Dom (uncurry u) = Dom (a ⊗ b)" and "Cod (uncurry u) = Dom c"
and "Map (uncurry u) =
Uncurry (Func ∘ exponential_rts.Map (Trn u)) ∘ Unpack a b"
and "src (uncurry u) = uncurry (src u)"
and "trg (uncurry u) = uncurry (trg u)"
proof -
show 0: "arr (uncurry u)"
and "dom (uncurry u) = a ⊗ b" and "cod (uncurry u) = c"
using assms uncurry_in_hom [of u] by auto
show "Dom (uncurry u) = Dom (a ⊗ b)" and "Cod (uncurry u) = Dom c"
using 0 ‹dom (uncurry u) = a ⊗ b› ‹cod (uncurry u) = c›
by (metis Dom_dom Dom_cod)+
show "Map (uncurry u) =
Uncurry (Func ∘ exponential_rts.Map (Trn u)) ∘ Unpack a b"
unfolding uncurry_def mkarr_def by simp
have 1: "transformation (Dom (a ⊗ b)) (Dom c)
(Uncurry (Func ∘ aXb_C.Dom (Trn u)) ∘ Unpack a b)
(Uncurry (Func ∘ aXb_C.Cod (Trn u)) ∘ Unpack a b)
(Uncurry (Func ∘ aXb_C.Map (Trn u)) ∘ Unpack a b)"
using 0 A_Exp.src_char uncurry_def uncurry_in_hom arr_char mkarr_def
by simp
show "src (uncurry u) = uncurry (src u)"
proof -
have "src (uncurry u) =
MkArr (Dom (a ⊗ b)) (Dom c) (aXb_C.src (Trn (uncurry u)))"
unfolding src_char
using assms 0 ‹Dom (uncurry u) = Dom (a ⊗ b)›
‹Cod (uncurry u) = Dom c›
by simp
also have "... = uncurry (src u)"
unfolding uncurry_def mkarr_def
using assms 1 src_char aXb_C.src_char
apply auto[1]
apply (metis (no_types, lifting) A_Exp.src_simp Dom_cod Dom_dom
Dom_exp H.in_homE arrE expXb.Dom.simps(1))
apply (metis (no_types, lifting) A_Exp.src_simp Dom_cod Dom_dom
Dom_exp H.in_homE arrE expXb.Cod.simps(1))
by (metis (no_types, lifting) A_Exp.Map_src Dom_cod Dom_dom
Dom_exp H.in_homE arrE)
finally show ?thesis by blast
qed
show "trg (uncurry u) = uncurry (trg u)"
proof -
have "trg (uncurry u) =
MkArr (Dom (a ⊗ b)) (Dom c) (aXb_C.trg (Trn (uncurry u)))"
unfolding trg_char
using assms ‹arr (uncurry u)› ‹Dom (uncurry u) = Dom (a ⊗ b)›
‹Cod (uncurry u) = Dom c›
by simp
also have "... = uncurry (trg u)"
unfolding uncurry_def mkarr_def trg_char
using assms 1 trg_char aXb_C.trg_char
apply auto[1]
apply (metis (no_types, lifting) A_Exp.trg_char Dom_cod Dom_dom
Dom_exp H.in_homE arrE expXb.Dom.simps(1))
apply (metis (no_types, lifting) A_Exp.trg_char Dom_cod Dom_dom
Dom_exp H.in_homE arrE expXb.Cod.simps(1))
by (metis (no_types, lifting) A_Exp.Map_trg Dom_cod Dom_dom
Dom_exp H.in_homE arrE)
finally show ?thesis by blast
qed
qed
lemma sta_uncurry:
assumes "«g : a → exp»" and "sta g"
shows "sta (uncurry g)"
using assms V.ide_iff_src_self [of "uncurry g"] by auto
lemma uncurry_curry:
assumes "obj a" and "obj b"
and "«t : a ⊗ b → c»"
shows "uncurry (curry t) = t"
proof -
have "mkarr (Dom (a ⊗ b)) (Dom c)
(Uncurry
(Func ∘
(Unfunc ∘
Curry3 (aXb_C.Dom (Trn t) ∘ Pack a b))) ∘
Unpack a b)
(Uncurry
(Func ∘
(Unfunc ∘
Curry3 (aXb_C.Cod (Trn t) ∘ Pack a b))) ∘
Unpack a b)
(Uncurry
(Func ∘
(Unfunc ∘
Curry (aXb_C.Dom (Trn t) ∘ Pack a b)
(aXb_C.Cod (Trn t) ∘ Pack a b)
(aXb_C.Map (Trn t) ∘ Pack a b))) ∘
Unpack a b) =
t"
(is "mkarr (Dom (a ⊗ b)) (Dom c) ?Src ?Trg ?Map = t")
proof -
interpret Dom: simulation ‹Dom (a ⊗ b)› ‹Dom c› ‹aXb_C.Dom (Trn t)›
using assms(3) arr_char aXb_C.arr_char Dom_dom Dom_cod
transformation_def
by (metis (no_types, lifting) H.in_homE arr_coincidence)
interpret Cod: simulation ‹Dom (a ⊗ b)› ‹Dom c› ‹aXb_C.Cod (Trn t)›
using assms(3) arr_char aXb_C.arr_char Dom_dom Dom_cod
transformation_def
by (metis (no_types, lifting) H.in_homE arr_coincidence)
interpret T: transformation ‹Dom (a ⊗ b)› ‹Dom c›
‹aXb_C.Dom (Trn t)› ‹aXb_C.Cod (Trn t)›
‹aXb_C.Map (Trn t)›
using assms(3) arr_char aXb_C.arr_char Dom_dom Dom_cod
by (metis (no_types, lifting) H.in_homE arr_coincidence)
interpret Dom_o_Pack: composite_simulation
AxB.resid ‹Dom (a ⊗ b)› ‹Dom c›
‹Pack a b› ‹aXb_C.Dom (Trn t)›
by intro_locales
(simp add: obj_a obj_b simulation.axioms(3) simulation_Pack)
interpret Dom_o_Pack: simulation_as_transformation
AxB.resid ‹Dom c› Dom_o_Pack.map
..
interpret Cod_o_Pack: composite_simulation
AxB.resid ‹Dom (a ⊗ b)› ‹Dom c›
‹Pack a b› ‹aXb_C.Cod (Trn t)›
..
interpret Cod_o_Pack: simulation_as_transformation
AxB.resid ‹Dom c› Cod_o_Pack.map
..
interpret T_o_Pack: transformation AxB.resid ‹Dom c›
Dom_o_Pack.map Cod_o_Pack.map
‹aXb_C.Map (Trn t) ∘ Pack a b›
using obj_a obj_b T.transformation_axioms simulation_Pack
AxB.weakly_extensional_rts_axioms
transformation_whisker_right
[of "Dom (a ⊗ b)" "Dom c" "aXb_C.Dom (Trn t)"
"aXb_C.Cod (Trn t)" "aXb_C.Map (Trn t)"
AxB.resid "Pack a b"]
by auto
interpret Curry_T_o_Pack: transformation ‹Dom a› EXP.resid
‹Curry3 Dom_o_Pack.map›
‹Curry3 Cod_o_Pack.map›
‹Curry
Dom_o_Pack.map
Cod_o_Pack.map
(aXb_C.Map (Trn t) ∘ Pack a b)›
using T_o_Pack.transformation_axioms Curry_preserves_transformations
by blast
have "?Src = aXb_C.Dom (Trn t)"
proof -
have "?Src =
Uncurry
((Func ∘ Unfunc) ∘
Curry3 (aXb_C.Dom (Trn t) ∘ Pack a b)) ∘
Unpack a b"
using comp_assoc by metis
also have "... =
Uncurry
(Curry3 (aXb_C.Dom (Trn t) ∘ Pack a b)) ∘
Unpack a b"
using Exp.inv Curry_T_o_Pack.transformation_axioms
comp_identity_simulation
[of "Dom a" EXP.resid "Curry3 Dom_o_Pack.map"]
by (auto simp add: transformation_def)
also have "... = aXb_C.Dom (Trn t) ∘ (Pack a b ∘ Unpack a b)"
using Dom_o_Pack.transformation_axioms Uncurry_Curry by auto
also have "... = aXb_C.Dom (Trn t) ∘ I (Dom (a ⊗ b))"
using assms Pack_o_Unpack by simp
also have "... = aXb_C.Dom (Trn t)"
using assms Dom.simulation_axioms comp_simulation_identity
by auto
finally show ?thesis by auto
qed
moreover
have "?Trg = aXb_C.Cod (Trn t)"
proof -
have "?Trg =
Uncurry
((Func ∘ Exp.map⇩e⇩x⇩t) ∘
Curry3 (aXb_C.Cod (Trn t) ∘ Pack a b)) ∘
Unpack a b"
using comp_assoc by metis
also have "... =
Uncurry
(Curry3 (aXb_C.Cod (Trn t) ∘ Pack a b)) ∘
Unpack a b"
using Exp.inv Curry_T_o_Pack.transformation_axioms
comp_identity_simulation
[of "Dom a" EXP.resid "Curry Cod_o_Pack.map
Cod_o_Pack.map Cod_o_Pack.map"]
by (auto simp add: transformation_def)
also have "... = aXb_C.Cod (Trn t) ∘ (Pack a b ∘ Unpack a b)"
using Cod_o_Pack.transformation_axioms Uncurry_Curry by auto
also have "... = aXb_C.Cod (Trn t) ∘ I (Dom (a ⊗ b))"
using assms Pack_o_Unpack by simp
also have "... = aXb_C.Cod (Trn t)"
using assms Cod.simulation_axioms comp_simulation_identity
by auto
finally show ?thesis by auto
qed
moreover
have "?Map = aXb_C.Map (Trn t)"
proof -
have "?Map =
Uncurry
((Func ∘ Unfunc) ∘
Curry (aXb_C.Dom (Trn t) ∘ Pack a b)
(aXb_C.Cod (Trn t) ∘ Pack a b)
(aXb_C.Map (Trn t) ∘ Pack a b)) ∘
Unpack a b"
using comp_assoc by metis
also have "... =
Uncurry
(Curry (aXb_C.Dom (Trn t) ∘ Pack a b)
(aXb_C.Cod (Trn t) ∘ Pack a b)
(aXb_C.Map (Trn t) ∘ Pack a b)) ∘
Unpack a b"
using Exp.inv Curry_T_o_Pack.transformation_axioms
comp_identity_transformation [of "Dom a" EXP.resid]
by (auto simp add: transformation_def)
also have "... = aXb_C.Map (Trn t) ∘ (Pack a b ∘ Unpack a b)"
using T_o_Pack.transformation_axioms Uncurry_Curry by auto
also have "... = aXb_C.Map (Trn t) ∘ I (Dom (a ⊗ b))"
using assms Pack_o_Unpack by simp
also have "... = aXb_C.Map (Trn t)"
using assms T.transformation_axioms comp_transformation_identity
by blast
finally show ?thesis by auto
qed
ultimately have "mkarr (Dom (a ⊗ b)) (Dom c) ?Src ?Trg ?Map =
mkarr (Dom (a ⊗ b)) (Dom c)
(aXb_C.Dom (Trn t)) (aXb_C.Cod (Trn t))
(aXb_C.Map (Trn t))"
by simp
also have "... = t"
by (metis (no_types, lifting) Dom_cod Dom_dom H.in_homE
H_arr_char mkarr_def MkArr_Trn aXb_C.arrE aXb_C.null_char
arr_char assms(3) expXb.MkArr_Map)
finally show ?thesis
using curry_def uncurry_def by simp
qed
thus ?thesis
using assms curry_def uncurry_def mkarr_def by simp
qed
lemma curry_uncurry:
assumes "«u : a → exp»"
shows "curry (uncurry u) = u"
proof -
have "mkarr (Dom a) Exp.resid
(Exp.map⇩e⇩x⇩t ∘
Curry3
((Uncurry (Func ∘ A_Exp.Dom (Trn u)) ∘ Unpack a b) ∘ Pack a b))
(Exp.map⇩e⇩x⇩t ∘
Curry3
((Uncurry (Func ∘ A_Exp.Cod (Trn u)) ∘ Unpack a b) ∘ Pack a b))
(Exp.map⇩e⇩x⇩t ∘
Curry
((Uncurry (Func ∘ A_Exp.Dom (Trn u)) ∘ Unpack a b) ∘ Pack a b)
((Uncurry (Func ∘ A_Exp.Cod (Trn u)) ∘ Unpack a b) ∘ Pack a b)
((Uncurry (Func ∘ A_Exp.Map (Trn u)) ∘ Unpack a b) ∘ Pack a b))
= u"
(is "?LHS = u")
proof -
interpret Dom: simulation ‹Dom a› Exp.resid ‹A_Exp.Dom (Trn u)›
using assms(1) arr_char A_Exp.arr_char transformation_def
by (metis Dom_cod Dom_dom Dom_exp H.in_homE arr_coincidence)
interpret Cod: simulation ‹Dom a› Exp.resid ‹A_Exp.Cod (Trn u)›
using assms(1) arr_char A_Exp.arr_char transformation_def
by (metis (mono_tags, lifting) Dom_cod Dom_dom Dom_exp
H.in_homE arr_coincidence)
interpret U: transformation ‹Dom a› Exp.resid
‹A_Exp.Dom (Trn u)› ‹A_Exp.Cod (Trn u)›
‹A_Exp.Map (Trn u)›
using assms(1) arr_char A_Exp.arr_char H.in_homE dom_char cod_char
by (metis (no_types, lifting) Dom_cod Dom_dom Dom_exp arr_coincidence)
interpret FuncoDom: composite_simulation
‹Dom a› Exp.resid EXP.resid
‹A_Exp.Dom (Trn u)› Func
..
interpret FuncoDom: simulation_as_transformation
‹Dom a› EXP.resid ‹Func ∘ A_Exp.Dom (Trn u)›
..
interpret FuncoCod: composite_simulation
‹Dom a› Exp.resid EXP.resid
‹A_Exp.Cod (Trn u)› Func
..
interpret FuncoCod: simulation_as_transformation
‹Dom a› EXP.resid ‹Func ∘ A_Exp.Cod (Trn u)›
..
interpret FuncoU: transformation ‹Dom a› EXP.resid
FuncoDom.map FuncoCod.map
‹Func ∘ A_Exp.Map (Trn u)›
using U.transformation_axioms Exp.Map'.simulation_axioms
EXP.weakly_extensional_rts_axioms transformation_whisker_left
by blast
have 1: "transformation AxB.resid (Dom c)
(Uncurry FuncoDom.map) (Uncurry FuncoCod.map)
(Uncurry (Func ∘ aXb_C.Map (Trn u)))"
using Uncurry_preserves_transformations FuncoU.transformation_axioms
by simp
have 2: "(Uncurry (Func ∘ A_Exp.Dom (Trn u)) ∘ Unpack a b) ∘
Pack a b =
Uncurry (Func ∘ A_Exp.Dom (Trn u))"
proof -
have "(Uncurry (Func ∘ A_Exp.Dom (Trn u)) ∘ Unpack a b) ∘ Pack a b =
Uncurry (Func ∘ A_Exp.Dom (Trn u)) ∘ (Unpack a b ∘ Pack a b)"
using comp_assoc by metis
also have "... = Uncurry (Func ∘ A_Exp.Dom (Trn u)) ∘ I AxB.resid"
using obj_a obj_b Unpack_o_Pack by auto
also have "... = Uncurry (Func ∘ A_Exp.Dom (Trn u))"
using 1 transformation_def comp_simulation_identity by blast
finally show ?thesis by simp
qed
have 3: "(Uncurry (Func ∘ A_Exp.Cod (Trn u)) ∘ Unpack a b) ∘ Pack a b =
Uncurry (Func ∘ A_Exp.Cod (Trn u))"
proof -
have "(Uncurry (Func ∘ A_Exp.Cod (Trn u)) ∘ Unpack a b) ∘ Pack a b =
Uncurry (Func ∘ A_Exp.Cod (Trn u)) ∘ (Unpack a b ∘ Pack a b)"
using comp_assoc by metis
also have "... = Uncurry (Func ∘ A_Exp.Cod (Trn u)) ∘ I AxB.resid"
using obj_a obj_b Unpack_o_Pack by auto
also have "... = Uncurry (Func ∘ A_Exp.Cod (Trn u))"
using 1 transformation_def comp_simulation_identity by blast
finally show ?thesis by simp
qed
have 4: "(Uncurry (Func ∘ A_Exp.Map (Trn u)) ∘ Unpack a b) ∘ Pack a b =
Uncurry (Func ∘ A_Exp.Map (Trn u))"
proof -
have "(Uncurry (Func ∘ A_Exp.Map (Trn u)) ∘ Unpack a b) ∘ Pack a b =
Uncurry (Func ∘ A_Exp.Map (Trn u)) ∘ (Unpack a b ∘ Pack a b)"
using comp_assoc by metis
also have "... = Uncurry (Func ∘ A_Exp.Map (Trn u)) ∘ I AxB.resid"
using obj_a obj_b Unpack_o_Pack by auto
also have "... = Uncurry (Func ∘ A_Exp.Map (Trn u))"
using 1 transformation_def comp_transformation_identity by blast
finally show ?thesis by simp
qed
have "?LHS = mkarr (Dom a) Exp.resid
(Exp.map⇩e⇩x⇩t ∘ Exp.map'⇩e⇩x⇩t ∘ A_Exp.Dom (Trn u))
(Exp.map⇩e⇩x⇩t ∘ Exp.map'⇩e⇩x⇩t ∘ A_Exp.Cod (Trn u))
(Exp.map⇩e⇩x⇩t ∘ Exp.map'⇩e⇩x⇩t ∘ A_Exp.Map (Trn u))"
using 2 3 4 FuncoDom.transformation_axioms
FuncoCod.transformation_axioms FuncoU.transformation_axioms
Curry_Uncurry mkarr_def
by auto
also have "... = mkarr (Dom a) Exp.resid
(A_Exp.Dom (Trn u)) (A_Exp.Cod (Trn u))
(A_Exp.Map (Trn u))"
using Dom.simulation_axioms Cod.simulation_axioms
U.transformation_axioms comp_identity_transformation
comp_identity_simulation [of "Dom a" Exp.resid]
Exp.inv' mkarr_def
by simp
also have "... = u"
proof -
have "Exp.resid = Cod u"
using assms Dom_exp cod_char
by (metis (no_types, lifting) Dom_cod H.in_homE
H_arr_char arr_char)
moreover have "Trn u =
A_Exp.MkArr
(A_Exp.Dom (Trn u)) (A_Exp.Cod (Trn u))
(A_Exp.Map (Trn u))"
using assms arr_char [of u] A_Exp.MkArr_Map
apply auto[1]
by (metis (no_types, lifting) A.weakly_extensional_rts_axioms
Dom_dom H.in_homE exponential_rts.arr_char
exponential_rts.intro)
ultimately show ?thesis
using assms U.transformation_axioms null_char arr_char
A_Exp.arr_char A_Exp.null_char dom_char
cod_char mkarr_def
by (intro arr_eqI) auto
qed
finally show ?thesis by auto
qed
thus ?thesis
unfolding curry_def uncurry_def mkarr_def
by simp
qed
text‹
We are not yet quite where we want to go, because to establish the naturality
of the curry/uncurry bijection we have to show how uncurry relates to evaluation.
›
lemma uncurry_expansion:
assumes "«u : a → exp»"
shows "uncurry u = eval ⋆ ⟨u ⋆ 𝔭⇩1[a, b], 𝔭⇩0[a, b]⟩"
proof (intro arr_eqI)
interpret AxB: identity_simulation AxB.resid ..
interpret P⇩0: simulation_as_transformation AxB.resid ‹Dom b› AxB.P⇩0 ..
interpret P⇩1: simulation_as_transformation AxB.resid ‹Dom a› AxB.P⇩1 ..
interpret U: transformation ‹Dom a› ‹Dom exp›
‹A_Exp.Dom (Trn u)› ‹A_Exp.Cod (Trn u)› ‹A_Exp.Map (Trn u)›
using assms Dom_dom Dom_cod [of u] arr_char A_Exp.arr_char
by (metis (no_types, lifting) Dom_exp H.in_homE arr_coincidence)
have a: "obj a"
using assms H.ide_dom by blast
have src_u: "«src u : a →⇩s⇩t⇩a exp»"
using assms by fastforce
have 0: "«eval ⋆ ⟨u ⋆ 𝔭⇩1[a, b], 𝔭⇩0[a, b]⟩ : a ⊗ b → c»"
using assms obj_a obj_b by auto
have 00: "«eval ⋆ ⟨src u ⋆ 𝔭⇩1[a, b], 𝔭⇩0[a, b]⟩ : a ⊗ b → c»"
using src_u obj_a obj_b by auto
have Dom: "Dom (eval ⋆ ⟨u ⋆ 𝔭⇩1[a, b], 𝔭⇩0[a, b]⟩) = Dom (a ⊗ b)"
using 0 Dom_dom [of "eval ⋆ ⟨u ⋆ 𝔭⇩1[a, b], 𝔭⇩0[a, b]⟩"] by auto
have Cod: "Cod (eval ⋆ ⟨u ⋆ 𝔭⇩1[a, b], 𝔭⇩0[a, b]⟩) = Dom c"
using 0 Cod_dom [of "eval ⋆ ⟨u ⋆ 𝔭⇩1[a, b], 𝔭⇩0[a, b]⟩"]
by (metis (no_types, lifting) Dom_cod H.in_homE H_arr_char arr_char)
show "uncurry u ≠ Null"
using assms uncurry_simps(1) V.not_arr_null null_char by metis
show "eval ⋆ ⟨u ⋆ 𝔭⇩1[a, b], 𝔭⇩0[a, b]⟩ ≠ Null"
using assms eval_in_hom null_char tuple_in_hom pr_in_hom
by (metis (no_types, lifting) H.comp_in_homI H.seqI' V.not_arr_null
arr_coincidence obj_a obj_b)
show 1: "Dom (uncurry u) = Dom (eval ⋆ ⟨u ⋆ 𝔭⇩1[a, b], 𝔭⇩0[a, b]⟩)"
by (simp add: Dom assms)
show 2: "Cod (uncurry u) = Cod (eval ⋆ ⟨u ⋆ 𝔭⇩1[a, b], 𝔭⇩0[a, b]⟩)"
by (simp add: Cod assms)
show "Trn (uncurry u) = Trn (eval ⋆ ⟨u ⋆ 𝔭⇩1[a, b], 𝔭⇩0[a, b]⟩)"
proof (intro aXb_C.arr_eqI)
show "aXb_C.arr (Trn (uncurry u))"
using assms arr_char [of "uncurry u"] by auto
show "aXb_C.arr (Trn (eval ⋆ ⟨u ⋆ 𝔭⇩1[a, b], 𝔭⇩0[a, b]⟩))"
using assms(1) 0 1 2 arr_char [of "eval ⋆ ⟨u ⋆ 𝔭⇩1[a, b], 𝔭⇩0[a, b]⟩"]
Dom_dom Dom_cod
by auto
show "aXb_C.Dom (Trn (uncurry u)) =
aXb_C.Dom (Trn (eval ⋆ ⟨u ⋆ 𝔭⇩1[a, b], 𝔭⇩0[a, b]⟩))"
proof -
have 4: "arr (eval ⋆ ⟨u ⋆ 𝔭⇩1[a, b], 𝔭⇩0[a, b]⟩)"
using 0 by blast
have 5: "sta ⟨src u ⋆ 𝔭⇩1[a, b], 𝔭⇩0[a, b]⟩"
using assms 00 sta_tuple sta_p⇩0 sta_p⇩1
by (metis (no_types, lifting) H.dom_comp H.in_homE
H.seqI cod_pr1 obj_a obj_b pr_simps(1-2,4-5)
src_u sta_hcomp)
have "aXb_C.Dom (Trn (uncurry u)) =
Eval.map ∘
product_simulation.map (Dom a) (Dom b)
(Func ∘ Map (src u)) B.map ∘
Unpack a b"
proof -
have "aXb_C.Dom (Trn (uncurry u)) =
aXb_C.Map (aXb_C.src (Trn (uncurry u)))"
by (simp add: ‹aXb_C.arr (Trn (uncurry u))›)
also have "... = Map (src (uncurry u))"
using assms(1) src_char by force
also have "... = Map (uncurry (src u))"
using assms(1) uncurry_simps by simp
also have "... = Uncurry (Func ∘ Map (src u)) ∘ Unpack a b"
unfolding uncurry_def mkarr_def by simp
also have "... = Eval.map ∘
product_simulation.map (Dom a) (Dom b)
(Func ∘ Map (src u)) B.map ∘
Unpack a b"
proof -
have "simulation (Dom a) EXP.resid (Func ∘ A_Exp.Map (Trn (src u)))"
using assms Exp.Map'.simulation_axioms sta_char
A_Exp.ide_char⇩E⇩R⇩T⇩S simulation_comp
by (metis (no_types, lifting) Cod_src Dom_cod Dom_dom
Dom_exp Dom_src H.in_homE V.ide_src arr_coincidence)
thus ?thesis
using Eval.Uncurry_simulation_expansion
[of "Dom a" "Exp.map'⇩e⇩x⇩t ∘ A_Exp.Map (Trn (src u))"]
A.weakly_extensional_rts_axioms
by auto
qed
finally show ?thesis by simp
qed
moreover
have "aXb_C.Dom (Trn (eval ⋆ ⟨u ⋆ 𝔭⇩1[a, b], 𝔭⇩0[a, b]⟩)) =
Eval.map ∘
product_simulation.map (Dom a) (Dom b)
(Func ∘ Map (src u)) B.map ∘
Unpack a b"
proof -
have "aXb_C.Dom (Trn (eval ⋆ ⟨u ⋆ 𝔭⇩1[a, b], 𝔭⇩0[a, b]⟩)) =
aXb_C.Map (aXb_C.src (Trn (eval ⋆ ⟨u ⋆ 𝔭⇩1[a, b], 𝔭⇩0[a, b]⟩)))"
using assms(1) 0 4 Dom Cod arr_char by auto
also have "... = aXb_C.Map (Trn (src (eval ⋆ ⟨u ⋆ 𝔭⇩1[a, b], 𝔭⇩0[a, b]⟩)))"
using 4 src_char Cod Dom Trn.simps(1) by presburger
also have "... = Map (eval ⋆ ⟨src u ⋆ 𝔭⇩1[a, b], 𝔭⇩0[a, b]⟩)"
proof -
have "H.seq eval ⟨u ⋆ 𝔭⇩1[a, b], 𝔭⇩0[a, b]⟩"
by (simp add: 4)
moreover have "H.span (u ⋆ 𝔭⇩1[a, b]) 𝔭⇩0[a, b]"
by (metis (no_types, lifting) H.not_arr_null H_seq_char
arr_coincidence calculation tuple_ext)
ultimately show ?thesis
using obj_a obj_b sta_p⇩0 sta_p⇩1 by auto
qed
also have "... = Map eval ∘ Map ⟨src u ⋆ 𝔭⇩1[a, b], 𝔭⇩0[a, b]⟩"
using "00" Map_hcomp by blast
also have "... = Map eval ∘
(Pack exp b ∘
⟨⟨Map (src u ⋆ 𝔭⇩1[a, b]), AxB.P⇩0 ∘ Unpack a b⟩⟩)"
using assms(1) obj_a obj_b Map_p⇩0
Map_tuple [of "src u ⋆ 𝔭⇩1[a, b]" "a ⊗ b" exp "𝔭⇩0[a, b]" b]
by (metis (no_types, lifting) H.comp_in_homI pr_in_hom(1-2) src_u)
also have "... = Map eval ∘
(Pack exp b ∘
⟨⟨Map (src u) ∘ (AxB.P⇩1 ∘ Unpack a b),
AxB.P⇩0 ∘ Unpack a b⟩⟩)"
using H.seqI Map_hcomp Map_p⇩1 assms obj_b pr_simps(4) by auto
also have "... = Map eval ∘
Pack exp b ∘
⟨⟨Map (src u) ∘ (AxB.P⇩1 ∘ Unpack a b),
AxB.P⇩0 ∘ Unpack a b⟩⟩"
using comp_assoc by metis
also have "... = (Eval.map ∘
(FuncxB.map ∘
(Unpack exp b ∘ Pack exp b)) ∘
⟨⟨Map (src u) ∘ AxB.P⇩1, AxB.P⇩0⟩⟩) ∘
Unpack a b"
using Map_eval
comp_pointwise_tuple
[of "Map (src u) ∘ AxB.P⇩1" AxB.P⇩0 "Unpack a b"]
by (simp add: comp_assoc)
also have "... = (Eval.map ∘
FuncxB.map ∘
⟨⟨Map (src u) ∘ AxB.P⇩1, AxB.P⇩0⟩⟩) ∘
Unpack a b"
using obj_b obj_exp Unpack_o_Pack Dom_exp
FuncxB.simulation_axioms comp_simulation_identity
[of ExpxB.resid EXPxB.resid FuncxB.map]
by presburger
also have "... = Eval.map ∘
(FuncxB.map ∘
⟨⟨Map (src u) ∘ AxB.P⇩1, AxB.P⇩0⟩⟩) ∘
Unpack a b"
by auto
also have "... = Eval.map ∘
⟨⟨Func ∘ Map (src u) ∘ AxB.P⇩1,
B.map ∘ AxB.P⇩0⟩⟩ ∘
Unpack a b"
proof -
have 1: "Src u = Map (src u)"
using assms Map_simps(3) by fastforce
interpret src_uoP⇩1: simulation AxB.resid Exp.resid
‹Map (src u) ∘ AxB.P⇩1›
using 1 AxB.P⇩1.simulation_axioms U.F.simulation_axioms
simulation_comp
by auto
interpret src_uoP⇩1: simulation_as_transformation
AxB.resid Exp.resid
‹Map (src u) ∘ AxB.P⇩1›
..
show ?thesis
using src_uoP⇩1.transformation_axioms B.simulation_axioms
Exp.Map'.simulation_axioms P⇩0.transformation_axioms
comp_product_simulation_tuple2
[of Exp.resid EXP.resid Func "Dom b" "Dom b" B.map
AxB.resid _ _ "Map (src u) ∘ AxB.P⇩1" _ _ AxB.P⇩0]
by (simp add: comp_assoc)
qed
also have "... = Eval.map ∘
(product_simulation.map (Dom a) (Dom b)
(Func ∘ Map (src u)) B.map ∘
⟨⟨AxB.P⇩1, AxB.P⇩0⟩⟩) ∘
Unpack a b"
proof -
have "simulation (Dom a) EXP.resid (Func ∘ Map (src u))"
using Exp.Map'.simulation_axioms U.F.simulation_axioms
simulation_comp Dom_exp H.arrI Map_simps(3) assms
by auto
thus ?thesis
using B.simulation_axioms P⇩0.transformation_axioms
P⇩1.transformation_axioms
comp_product_simulation_tuple2
[of "Dom a" EXP.resid "Func ∘ Map (src u)"
"Dom b" "Dom b" B.map AxB.resid
AxB.P⇩1 AxB.P⇩1 AxB.P⇩1 AxB.P⇩0 AxB.P⇩0 AxB.P⇩0]
simulation_as_transformation.intro
AxB.weakly_extensional_rts_axioms
A.weakly_extensional_rts_axioms
B.weakly_extensional_rts_axioms
by simp
qed
also have "... = Eval.map ∘
product_simulation.map (Dom a) (Dom b)
(Func ∘ Map (src u)) B.map ∘
(⟨⟨AxB.P⇩1, AxB.P⇩0⟩⟩ ∘ Unpack a b)"
by auto
also have "... = Eval.map ∘
(product_simulation.map (Dom a) (Dom b)
(Func ∘ Map (src u)) B.map) ∘
Unpack a b"
proof -
interpret AxB: identity_simulation AxB.resid ..
have "⟨⟨AxB.P⇩1, AxB.P⇩0⟩⟩ = I AxB.resid"
using AxB.tuple_proj [of AxB.resid "I AxB.resid"]
AxB.simulation_axioms
comp_simulation_identity [of AxB.resid "Dom b" AxB.P⇩0]
comp_simulation_identity [of AxB.resid "Dom a" AxB.P⇩1]
AxB.P⇩0.simulation_axioms AxB.P⇩1.simulation_axioms
by simp
thus ?thesis
using obj_a obj_b simulation_Unpack
comp_identity_simulation
[of "Dom (a ⊗ b)" AxB.resid "Unpack a b"]
by auto
qed
finally show ?thesis by blast
qed
ultimately show ?thesis by simp
qed
show "aXb_C.Cod (Trn (uncurry u)) =
aXb_C.Cod (Trn (eval ⋆ ⟨u ⋆ 𝔭⇩1[a, b], 𝔭⇩0[a, b]⟩))"
proof -
have "aXb_C.Cod (Trn (uncurry u)) =
aXb_C.Map (aXb_C.trg (Trn (uncurry u)))"
by (simp add: ‹aXb_C.arr (Trn (uncurry u))›)
also have "... = Map (trg (uncurry u))"
using assms(1) trg_char by force
also have "... = Map (uncurry (trg u))"
using assms(1) uncurry_simps by simp
also have "... = Uncurry (Func ∘ Map (trg u)) ∘ Unpack a b"
unfolding uncurry_def mkarr_def by simp
also have "... = Eval.map ∘
product_simulation.map (Dom a) (Dom b)
(Func ∘ Map (trg u)) B.map ∘
Unpack a b"
proof -
have "simulation (Dom a) EXP.resid (Func ∘ A_Exp.Map (Trn (trg u)))"
using assms Exp.Map'.simulation_axioms sta_char A_Exp.ide_char⇩E⇩R⇩T⇩S
simulation_comp
[of "Dom a" Exp.resid "A_Exp.Map (Trn (trg u))"
EXP.resid Func]
by (metis (no_types, lifting) Cod_trg Dom_cod Dom_exp Dom_trg
H.in_homE H.seqI H_seq_char cod_pr1 ide_trg obj_a pr_simps(4))
thus ?thesis
using Eval.Uncurry_simulation_expansion
[of "Dom a" "Exp.map'⇩e⇩x⇩t ∘ A_Exp.Map (Trn (trg u))"]
A.weakly_extensional_rts_axioms
by auto
qed
also have "... = Eval.map ∘
product_simulation.map (Dom a) (Dom b)
(Func ∘ Map (trg u)) B.map ∘
(⟨⟨AxB.P⇩1, AxB.P⇩0⟩⟩ ∘ Unpack a b)"
by (metis (no_types, lifting) AxB.tuple_proj
comp_pointwise_tuple obj_a obj_b simulation_Unpack)
also have "... = Eval.map ∘
(product_simulation.map (Dom a) (Dom b)
(Func ∘ Map (trg u)) B.map ∘
⟨⟨AxB.P⇩1, AxB.P⇩0⟩⟩) ∘
Unpack a b"
by auto
also have "... = Eval.map ∘
⟨⟨Func ∘ Map (trg u) ∘ AxB.P⇩1, B.map ∘ AxB.P⇩0⟩⟩ ∘
Unpack a b"
proof -
have "simulation (Dom a) EXP.resid (Func ∘ Map (trg u))"
using Exp.Map'.simulation_axioms U.G.simulation_axioms
simulation_comp Dom_exp H.arrI Map_simps(4) assms
by auto
thus ?thesis
using B.simulation_axioms P⇩0.transformation_axioms
P⇩1.transformation_axioms
comp_product_simulation_tuple2
[of "Dom a" EXP.resid "Func ∘ Map (trg u)"
"Dom b" "Dom b" B.map
AxB.resid AxB.P⇩1 AxB.P⇩1 AxB.P⇩1 AxB.P⇩0 AxB.P⇩0 AxB.P⇩0]
by (simp add: comp_assoc)
qed
also have "... = Eval.map ∘
(FuncxB.map ∘
⟨⟨Map (trg u) ∘ AxB.P⇩1, AxB.P⇩0⟩⟩) ∘
Unpack a b"
proof -
have 1: "Trg u = Map (trg u)"
using assms Map_simps(4) by fastforce
interpret trg_uoP⇩1: simulation AxB.resid Exp.resid
‹Map (trg u) ∘ AxB.P⇩1›
using 1 AxB.P⇩1.simulation_axioms U.G.simulation_axioms
simulation_comp
by auto
interpret src_uoP⇩1: simulation_as_transformation AxB.resid Exp.resid
‹Map (trg u) ∘ AxB.P⇩1›
..
interpret P⇩0: simulation_as_transformation AxB.resid ‹Dom b› AxB.P⇩0
..
show ?thesis
using src_uoP⇩1.transformation_axioms B.simulation_axioms
Exp.Map'.simulation_axioms P⇩0.transformation_axioms
comp_product_simulation_tuple2
[of Exp.resid EXP.resid Func "Dom b" "Dom b" B.map
AxB.resid _ _ "Map (trg u) ∘ AxB.P⇩1" _ _ AxB.P⇩0]
by (simp add: comp_assoc)
qed
also have "... = (Eval.map ∘
FuncxB.map ∘
⟨⟨Map (trg u) ∘ AxB.P⇩1, AxB.P⇩0⟩⟩) ∘
Unpack a b"
by auto
also have "... = (Eval.map ∘
(FuncxB.map ∘
(Unpack exp b ∘ Pack exp b)) ∘
⟨⟨Map (trg u) ∘ AxB.P⇩1, AxB.P⇩0⟩⟩) ∘
Unpack a b"
using obj_b obj_exp Unpack_o_Pack Dom_exp FuncxB.simulation_axioms
comp_simulation_identity [of ExpxB.resid EXPxB.resid FuncxB.map]
by presburger
also have "... = Map eval ∘
Pack exp b ∘
⟨⟨Map (trg u) ∘ AxB.P⇩1 ∘ Unpack a b,
AxB.P⇩0 ∘ Unpack a b⟩⟩"
using Map_eval
comp_pointwise_tuple
[of "Map (trg u) ∘ AxB.P⇩1" AxB.P⇩0 "Unpack a b"]
by (simp add: comp_assoc)
also have "... = Map eval ∘
(Pack exp b ∘
⟨⟨Map (trg u) ∘ AxB.P⇩1 ∘ Unpack a b,
AxB.P⇩0 ∘ Unpack a b⟩⟩)"
using comp_assoc by metis
also have "... = Map eval ∘
(Pack exp b ∘
⟨⟨Map (trg u ⋆ p⇩1 a b),
AxB.P⇩0 ∘ Unpack a b⟩⟩)"
by (metis (no_types, lifting) H.in_homE H.seqI Map_hcomp
Map_p⇩1 assms cod_pr1 comp_assoc dom_trg obj_a obj_b
pr_simps(4) trg.preserves_arr)
also have "... = Map eval ∘ Map ⟨trg u ⋆ 𝔭⇩1[a, b], 𝔭⇩0[a, b]⟩"
proof -
have "«trg u ⋆ 𝔭⇩1[a, b] : a ⊗ b → exp»"
using assms(1) obj_a obj_b sta_p⇩0 [of a b] sta_p⇩1 [of a b] H.seqI
by auto
moreover have "«𝔭⇩0[a, b] : a ⊗ b → b»"
using obj_a obj_b by blast
ultimately show ?thesis
using assms(1) obj_a obj_b Map_p⇩0
Map_tuple [of "trg u ⋆ 𝔭⇩1[a, b]" "a ⊗ b" exp "𝔭⇩0[a, b]" b]
by auto
qed
also have "... = Map (eval ⋆ ⟨trg u ⋆ 𝔭⇩1[a, b], 𝔭⇩0[a, b]⟩)"
using assms 0 Map_eval Map_hcomp H.cod_comp H.dom_comp H.seqI
cod_pr0 cod_pr1 cod_trg cod_tuple dom_trg eval_in_hom
obj_a obj_b pr_simps(1-2,4-5) trg.preserves_arr tuple_simps(1)
by (elim H.in_homE) presburger
also have "... = Map (trg (eval ⋆ ⟨u ⋆ 𝔭⇩1[a, b], 𝔭⇩0[a, b]⟩))"
proof -
have "H.seq eval ⟨u ⋆ 𝔭⇩1[a, b], 𝔭⇩0[a, b]⟩"
using 0 by blast
moreover have "H.span (u ⋆ 𝔭⇩1[a, b]) 𝔭⇩0[a, b]"
by (metis (no_types, lifting) H.not_arr_null H_seq_char
arr_coincidence calculation tuple_ext)
ultimately show ?thesis
using obj_a obj_b sta_p⇩0 sta_p⇩1 by auto
qed
also have "... = Trg (eval ⋆ ⟨u ⋆ 𝔭⇩1[a, b], 𝔭⇩0[a, b]⟩)"
using 0 trg_char Cod Dom Trn.simps(1) H.arrI Map_simps(4) by blast
also have "... = aXb_C.Cod (Trn (eval ⋆ ⟨u ⋆ 𝔭⇩1[a, b], 𝔭⇩0[a, b]⟩))"
by simp
finally show ?thesis by simp
qed
fix x
assume x: "aXb.ide x"
show "aXb_C.Map (Trn (uncurry u)) x =
aXb_C.Map (Trn (eval ⋆ ⟨u ⋆ 𝔭⇩1[a, b], 𝔭⇩0[a, b]⟩)) x"
proof -
have "aXb_C.Map (Trn (uncurry u)) x =
(Uncurry (Func ∘ Map u) ∘ Unpack a b) x"
unfolding uncurry_def mkarr_def by simp
also have "... = (Eval.map ∘
product_transformation.map (Dom a) (Dom b)
EXP.resid (Dom b)
(Func ∘ A_Exp.Dom (Trn u)) B.map
(Func ∘ A_Exp.Map (Trn u)) B.map ∘
Unpack a b) x"
proof -
have "transformation (Dom a) EXP.resid
(Func ∘ A_Exp.Dom (Trn u)) (Func ∘ A_Exp.Cod (Trn u))
(Func ∘ A_Exp.Map (Trn u))"
using assms Exp.Map'.simulation_axioms arr_char A_Exp.ide_char⇩E⇩R⇩T⇩S
EXP.weakly_extensional_rts_axioms Dom_exp
U.transformation_axioms transformation_whisker_left
by simp
thus ?thesis
using Eval.Uncurry_transformation_expansion
[of "Dom a" "Func ∘ A_Exp.Dom (Trn u)"
"Func ∘ A_Exp.Cod (Trn u)" "Func ∘ A_Exp.Map (Trn u)"]
A.weakly_extensional_rts_axioms
by auto
qed
also have "... = (Eval.map ∘
product_transformation.map (Dom a) (Dom b)
EXP.resid (Dom b)
(Func ∘ A_Exp.Dom (Trn u)) B.map
(Func ∘ Map u) B.map ∘
(⟨⟨AxB.P⇩1, AxB.P⇩0⟩⟩ ∘ Unpack a b)) x"
proof -
have "pointwise_tuple AxB.P⇩1 AxB.P⇩0 = I AxB.resid"
using AxB.tuple_proj [of AxB.resid "I AxB.resid"]
comp_simulation_identity [of AxB.resid "Dom b" AxB.P⇩0]
comp_simulation_identity [of AxB.resid "Dom a" AxB.P⇩1]
AxB.P⇩0.simulation_axioms AxB.P⇩1.simulation_axioms
AxB.simulation_axioms
by simp
thus ?thesis
using obj_a obj_b simulation_Unpack
comp_identity_simulation
[of "Dom (a ⊗ b)" AxB.resid "Unpack a b"]
by auto
qed
also have "... = (Eval.map ∘
((product_transformation.map (Dom a) (Dom b)
EXP.resid (Dom b)
(Func ∘ Src u) B.map
(Func ∘ Map u) B.map ∘
⟨⟨AxB.P⇩1, AxB.P⇩0⟩⟩) ∘
Unpack a b)) x"
by auto
also have "... = (Eval.map ∘
(⟨⟨Func ∘ (Map u ∘ AxB.P⇩1), B.map ∘ AxB.P⇩0⟩⟩ ∘
Unpack a b)) x"
proof -
have "transformation (Dom a) EXP.resid
(Func ∘ Src u) (Func ∘ Trg u) (Func ∘ Map u)"
using assms Exp.Map'.simulation_axioms U.transformation_axioms
EXP.weakly_extensional_rts_axioms Dom_exp H.arrI
Map_simps(4) transformation_whisker_left
by auto
hence "transformation_to_extensional_rts (Dom a) EXP.resid
(Func ∘ Src u) (Func ∘ Trg u) (Func ∘ Map u)"
using EXP.extensional_rts_axioms
transformation_to_extensional_rts.intro
by blast
thus ?thesis
using B.simulation_axioms AxB.P⇩0_is_simulation
AxB.P⇩1_is_simulation
B.transformation_to_extensional_rts_axioms
comp_product_transformation_tuple
[of "Dom a" EXP.resid
"Func ∘ Src u" "Func ∘ Trg u" "Func ∘ Map u"
"Dom b" "Dom b" B.map B.map B.map
AxB.resid AxB.P⇩1 AxB.P⇩0]
by (simp add: comp_assoc)
qed
also have "... = (Eval.map ∘
(FuncxB.map ∘
⟨⟨Map u ∘ AxB.P⇩1, AxB.P⇩0⟩⟩) ∘
Unpack a b) x"
proof -
have "transformation (\\⇩A⇩x⇩B) Exp.resid
(Src u ∘ AxB.P⇩1) (Trg u ∘ AxB.P⇩1) (Map u ∘ AxB.P⇩1)"
using transformation_whisker_right AxB.P⇩1.simulation_axioms
U.transformation_axioms Dom_exp
AxB.weakly_extensional_rts_axioms
by auto
thus ?thesis
using B.simulation_axioms Exp.Map'.simulation_axioms
P⇩0.transformation_axioms P⇩1.transformation_axioms
comp_product_simulation_tuple2
[of Exp.resid EXP.resid Func "Dom b" "Dom b" B.map
AxB.resid _ _ "Map u ∘ AxB.P⇩1" _ _ AxB.P⇩0]
by simp
qed
also have "... = ((Eval.map ∘
FuncxB.map ∘
⟨⟨Map u ∘ AxB.P⇩1, AxB.P⇩0⟩⟩) ∘
Unpack a b) x"
by auto
also have "... = ((Eval.map ∘
(FuncxB.map ∘
(Unpack exp b ∘ Pack exp b)) ∘
⟨⟨Map u ∘ AxB.P⇩1, AxB.P⇩0⟩⟩) ∘
Unpack a b) x"
using obj_b obj_exp Unpack_o_Pack Dom_exp FuncxB.simulation_axioms
comp_simulation_identity
[of ExpxB.resid EXPxB.resid FuncxB.map]
by presburger
also have "... = (Map eval ∘
Pack exp b ∘
⟨⟨Map u ∘ AxB.P⇩1 ∘ Unpack a b,
AxB.P⇩0 ∘ Unpack a b⟩⟩) x"
using Map_eval
comp_pointwise_tuple [of "Map u ∘ AxB.P⇩1" AxB.P⇩0 "Unpack a b"]
by (simp add: comp_assoc)
also have "... = (Map eval ∘
(Pack exp b ∘
⟨⟨Map u ∘ (AxB.P⇩1 ∘ Unpack a b),
AxB.P⇩0 ∘ Unpack a b⟩⟩)) x"
using comp_assoc by metis
also have "... = (Map eval ∘
(Pack exp b ∘
⟨⟨Map (u ⋆ p⇩1 a b),
AxB.P⇩0 ∘ Unpack a b⟩⟩)) x"
by (metis (no_types, lifting) H.seqI' Map_p⇩1
Map_hcomp arr_coincidence assms obj_a obj_b pr_in_hom(2))
also have "... = (Map eval ∘ Map ⟨u ⋆ 𝔭⇩1[a, b], 𝔭⇩0[a, b]⟩) x"
by (metis (mono_tags, lifting) H.comp_in_homI Map_p⇩0 Map_tuple
assms obj_a obj_b pr_in_hom(1) pr_in_hom(2))
also have "... = (aXb_C.Map (Trn (eval ⋆ ⟨u ⋆ 𝔭⇩1[a, b], 𝔭⇩0[a, b]⟩))) x"
using 0 Map_eval Map_hcomp by auto
finally show ?thesis by simp
qed
qed
qed
end
text‹
Once again, we transfer the things we want to @{locale rtscatx}.
›
context rtscatx
begin
interpretation elementary_category_with_binary_products hcomp p⇩0 p⇩1
using extends_to_elementary_category_with_binary_products by blast
notation hcomp (infixr "⋆" 53)
notation p⇩0 ("𝔭⇩0[_, _]")
notation p⇩1 ("𝔭⇩1[_, _]")
notation tuple ("⟨_, _⟩")
notation prod (infixr "⊗" 51)
definition curry :: "'A arr ⇒ 'A arr ⇒ 'A arr ⇒ 'A arr ⇒ 'A arr"
where "curry ≡ currying_in_rtscat.curry"
definition uncurry :: "'A arr ⇒ 'A arr ⇒ 'A arr ⇒ 'A arr ⇒ 'A arr"
where "uncurry ≡ currying_in_rtscat.uncurry"
lemma curry_in_hom [intro, simp]:
assumes "obj a" and "obj b"
and "«f : a ⊗ b → c»"
shows "«curry a b c f : a → exp b c»"
proof -
interpret Currying: currying_in_rtscat arr_type a b c
using assms by unfold_locales auto
show ?thesis
unfolding curry_def exp_def
using assms Currying.curry_in_hom by blast
qed
lemma curry_simps [simp]:
assumes "obj a" and "obj b"
and "«f : a ⊗ b → c»"
shows "arr (curry a b c f)"
and "dom (curry a b c f) = a" and "cod (curry a b c f) = exp b c"
and "src (curry a b c f) = curry a b c (src f)"
and "trg (curry a b c f) = curry a b c (trg f)"
proof -
interpret Currying: currying_in_rtscat arr_type a b c
using assms by unfold_locales auto
show "arr (curry a b c f)"
and "dom (curry a b c f) = a" and "cod (curry a b c f) = exp b c"
using assms curry_in_hom H.in_homE H_arr_char arr_char
apply (metis (no_types, lifting))
by (metis (no_types, lifting) H.in_homE assms curry_in_hom)+
show "src (curry a b c f) = curry a b c (src f)"
and "trg (curry a b c f) = curry a b c (trg f)"
unfolding curry_def
using assms by auto
qed
lemma sta_curry:
assumes "obj a" and "obj b"
and "«f : a ⊗ b → c»" and "sta f"
shows "sta (curry a b c f)"
using assms V.ide_iff_src_self [of "curry a b c f"] by auto
lemma uncurry_in_hom [intro, simp]:
assumes "obj b" and "obj c"
and "«g : a → exp b c»"
shows "«uncurry a b c g : a ⊗ b → c»"
proof -
interpret Currying: currying_in_rtscat arr_type a b c
using assms by unfold_locales auto
show ?thesis
using assms
unfolding uncurry_def exp_def
using Currying.uncurry_in_hom by blast
qed
lemma uncurry_simps [simp]:
assumes "obj b" and "obj c"
and "«g : a → exp b c»"
shows "arr (uncurry a b c g)"
and "dom (uncurry a b c g) = a ⊗ b" and "cod (uncurry a b c g) = c"
and "src (uncurry a b c g) = uncurry a b c (src g)"
and "trg (uncurry a b c g) = uncurry a b c (trg g)"
proof -
interpret Currying: currying_in_rtscat arr_type a b c
using assms by unfold_locales auto
show "arr (uncurry a b c g)"
and "dom (uncurry a b c g) = a ⊗ b" and "cod (uncurry a b c g) = c"
using assms uncurry_in_hom H.in_homE H_arr_char arr_char
apply (metis (no_types, lifting))
by (metis (no_types, lifting) H.in_homE assms uncurry_in_hom)+
show "src (uncurry a b c g) = uncurry a b c (src g)"
and "trg (uncurry a b c g) = uncurry a b c (trg g)"
using assms
by (auto simp add: uncurry_def exp_def)
qed
lemma sta_uncurry:
assumes "obj b" and "obj c"
and "«g : a → exp b c»" and "sta g"
shows "sta (uncurry a b c g)"
using assms V.ide_iff_src_self [of "uncurry a b c g"] by auto
lemma uncurry_curry:
assumes "obj a" and "obj b"
and "«t : a ⊗ b → c»"
shows "uncurry a b c (curry a b c t) = t"
proof -
interpret Currying: currying_in_rtscat arr_type a b c
using assms by unfold_locales auto
show ?thesis
unfolding curry_def uncurry_def
using assms Currying.uncurry_curry by blast
qed
lemma curry_uncurry:
assumes "obj b" and "obj c"
and "«u : a → exp b c»"
shows "curry a b c (uncurry a b c u) = u"
proof -
interpret Currying: currying_in_rtscat arr_type a b c
using assms by unfold_locales auto
show ?thesis
using assms
unfolding curry_def uncurry_def exp_def
using Currying.curry_uncurry by blast
qed
lemma uncurry_expansion:
assumes "obj b" and "obj c"
and "«u : a → exp b c»"
shows "uncurry a b c u = eval b c ⋆ (u ⊗ b)"
proof -
have a: "obj a"
using assms(3) by auto
interpret Currying: currying_in_rtscat arr_type a b c
using assms by unfold_locales auto
have "uncurry a b c u = eval b c ⋆ ⟨u ⋆ 𝔭⇩1[a, b], 𝔭⇩0[a, b]⟩"
using assms
unfolding curry_def uncurry_def exp_def eval_def
using Currying.uncurry_expansion by blast
also have "... = eval b c ⋆ (u ⊗ b) ⋆ ⟨𝔭⇩1[a, b], 𝔭⇩0[a, b]⟩"
proof -
have "b ⋆ 𝔭⇩0[a, b] = 𝔭⇩0[a, b]"
using assms a sta_p⇩0
by (simp add: H.comp_cod_arr)
moreover have "H.seq u 𝔭⇩1[a, b]"
using assms sta_p⇩1 [of a b]
by (intro H.seqI) auto
ultimately show ?thesis
using assms prod_tuple [of "𝔭⇩1[a, b]" "𝔭⇩0[a, b]" u b]
sta_p⇩0 [of a b] sta_p⇩1 [of a b]
by auto
qed
also have "... = eval b c ⋆ (u ⊗ b)"
using assms a tuple_pr [of a b] H.comp_arr_ide
by (metis (no_types, lifting) H.comp_arr_dom H.comp_ide_self H.ideD(1)
H.in_homE interchange)
finally show ?thesis by blast
qed
lemma Map_curry:
assumes "obj a" and "obj b" and "obj c"
shows "Map (curry a b c f) =
Unfunc b c ∘
Currying.Curry (Dom a) (Dom b) (Dom c)
(Src f ∘ Pack a b) (Trg f ∘ Pack a b) (Map f ∘ Pack a b)"
proof -
interpret Currying: currying_in_rtscat arr_type a b c
using assms by unfold_locales auto
show ?thesis
unfolding curry_def Currying.curry_def Unfunc_def mkarr_def by simp
qed
lemma Map_uncurry:
assumes "obj a" and "obj b" and "obj c"
shows "Map (uncurry a b c g) =
Currying.Uncurry (Dom a) (Dom b) (Dom c)
(Func b c ∘ exponential_rts.Map (Trn g)) ∘ Unpack a b"
proof -
interpret Currying: currying_in_rtscat arr_type a b c
using assms by unfold_locales auto
show ?thesis
unfolding uncurry_def Currying.uncurry_def Func_def mkarr_def by simp
qed
end
subsection "Cartesian Closure"
text‹
We can now show that the category ‹❙R❙T❙S⇧†› is cartesian closed.
›
context rtscatx
begin
interpretation elementary_category_with_binary_products hcomp p⇩0 p⇩1
using extends_to_elementary_category_with_binary_products by blast
notation prod (infixr "⊗" 51)
interpretation elementary_cartesian_closed_category
hcomp p⇩0 p⇩1 one trm exp eval curry
proof
fix b c
assume b: "obj b" and c: "obj c"
show "«eval b c : exp b c ⊗ b → c»"
using b c eval_in_hom⇩R⇩C⇩R by blast
show "obj (exp b c)"
using b c obj_exp by blast
fix a
assume a: "obj a"
show "⋀t. «t : a ⊗ b → c» ⟹ «curry a b c t : a → exp b c»"
using a b c curry_in_hom by blast
show "⋀t. «t : a ⊗ b → c» ⟹ eval b c ⋆ (curry a b c t ⊗ b) = t"
by (metis ‹⋀t. «t : a ⊗ b → c» ⟹ «curry a b c t : a → exp b c»›
a b c uncurry_curry uncurry_expansion)
show "⋀u. «u : a → exp b c» ⟹ curry a b c (eval b c ⋆ (u ⊗ b)) = u"
using b c curry_uncurry uncurry_expansion by force
qed
lemma is_elementary_cartesian_closed_category:
shows "elementary_cartesian_closed_category
hcomp p⇩0 p⇩1 one trm exp eval curry"
..
theorem is_cartesian_closed_category:
shows "cartesian_closed_category hcomp"
..
end
subsection "Repleteness"
context rtscatx
begin
text‹
We have shown that the RTS-category ‹❙R❙T❙S⇧†› has objects that
are in bijective correspondence with small extensional RTS's, states (identities for
the vertical residuation) that are in bijective correspondence with simulations,
and arrows that are in bijective correspondence with transformations. These results
allow us to pass back and forth between external constructions on RTS's and internal
structure of the RTS-category, as was demonstrated in the proof of cartesian closure.
However, these results make use of extra structure beyond that of an RTS-category;
namely the mapping @{term Dom} that takes an object to its underlying RTS.
We would like to have a characterization of ‹❙R❙T❙S⇧†› in terms that make sense
for an abstract RTS-category without additional structure. It seems that it should
be possible to do this, because as we have shown, for any object ‹a› the RTS ‹Dom a›
is isomorphic to ‹Hom ❙𝟭 a›. So we ought to be able to dispense with the extrinsic
mapping @{term Dom} and work instead with the intrinsic mapping @{term "Hom ❙𝟭"}.
However, there is an issue here to do with types. The mapping @{term Dom} takes an object
‹a› to a small extensional RTS ‹Dom a› having arrow type @{typ 'A}. On the other hand,
the RTS ‹Hom ❙𝟭 a› has arrow type @{typ "'A rtscatx.arr"}. So one thing that needs to be
done in order to carry out this program is to express the ``object repleteness''
of ‹❙R❙T❙S⇧†› in terms of small extensional RTS's with arrow type
@{typ "'A rtscatx.arr"}, as opposed to small extensional RTS's with arrow type @{typ 'A}.
However, the type @{typ "'A rtscatx.arr"} is larger than the type @{typ 'A},
and consequently it could admit a larger class of small extensional RTS's than
type @{typ 'A} does. It is possible, though, to define a mapping from
@{typ "'A rtscatx.arr"} to @{typ 'A} whose restriction to the set of arrows (and null)
of @{locale rtscatx} is injective. This will allow us to take any small extensional
RTS ‹A› with arrow type @{typ "'A rtscatx.arr"}, as long as its arrows
and null are drawn from the set of arrows and null of @{locale rtscatx} as a whole,
and obtain an isomorphic image of it with arrow type @{typ 'A}.
›
text‹
We first define the required mapping from @{typ "'A arr"} to @{typ 'A}.
›
fun inj_arr :: "'A arr ⇒ 'A"
where "inj_arr (MkArr A B F) =
lifting.some_lift
(Some (pairing.some_pair
(some_inj_resid A,
pairing.some_pair
(some_inj_resid B, inj_exp F))))"
| "inj_arr Null = lifting.some_lift None"
text‹
The mapping @{term inj_arr} has the required injectiveness property.
›
lemma inj_inj_arr:
fixes A :: "'A arr resid"
assumes "small_rts A" and "extensional_rts A"
and "Collect (residuation.arr A) ∪
{ResiduatedTransitionSystem.partial_magma.null A} ⊆
Collect arr ∪ {Null}"
shows "inj_on inj_arr
(Collect (residuation.arr A) ∪
{ResiduatedTransitionSystem.partial_magma.null A})"
proof
interpret A: small_rts A
using assms(1) by blast
interpret A: extensional_rts A
using assms(2) by blast
fix x y :: "'A arr"
assume x: "x ∈ Collect A.arr ∪ {A.null}"
assume y: "y ∈ Collect A.arr ∪ {A.null}"
assume eq: "inj_arr x = inj_arr y"
show "x = y"
proof -
have "⟦x = Null; y ≠ Null⟧ ⟹ ?thesis"
using eq
apply (cases x; cases y)
by (auto simp add: inj_eq inj_some_lift)
moreover have "⟦x ≠ Null; y = Null⟧ ⟹ ?thesis"
using eq
apply (cases x; cases y)
by (auto simp add: inj_eq inj_some_lift)
moreover have "⟦x ≠ Null; y ≠ Null⟧ ⟹ x = y"
proof -
assume x': "x ≠ Null" and y': "y ≠ Null"
have "lifting.some_lift
(Some (pairing.some_pair
(some_inj_resid (Dom x),
pairing.some_pair
(some_inj_resid (Cod x), inj_exp (Trn x))))) =
lifting.some_lift
(Some (pairing.some_pair
(some_inj_resid (Dom y),
pairing.some_pair
(some_inj_resid (Cod y), inj_exp (Trn y)))))"
using eq x' y'
by (cases x; cases y) auto
hence "Some (pairing.some_pair
(some_inj_resid (Dom x),
pairing.some_pair
(some_inj_resid (Cod x), inj_exp (Trn x)))) =
Some (pairing.some_pair
(some_inj_resid (Dom y),
pairing.some_pair
(some_inj_resid (Cod y), inj_exp (Trn y))))"
using inj_some_lift injD by metis
hence "pairing.some_pair
(some_inj_resid (Dom x),
pairing.some_pair
(some_inj_resid (Cod x), inj_exp (Trn x))) =
pairing.some_pair
(some_inj_resid (Dom x),
pairing.some_pair
(some_inj_resid (Cod x), inj_exp (Trn x)))"
by auto
hence "some_inj_resid (Dom x) = some_inj_resid (Dom y) ∧
pairing.some_pair (some_inj_resid (Cod x), inj_exp (Trn x)) =
pairing.some_pair (some_inj_resid (Cod x), inj_exp (Trn y))"
using inj_some_pair
by (metis ‹Some (some_pair
(some_inj_resid (Dom x),
some_pair (some_inj_resid (Cod x), inj_exp (Trn x)))) =
Some (some_pair
(some_inj_resid (Dom y),
some_pair (some_inj_resid (Cod y), inj_exp (Trn y))))›
first_conv option.inject second_conv)
hence 1: "some_inj_resid (Dom x) = some_inj_resid (Dom y) ∧
some_inj_resid (Cod x) = some_inj_resid (Cod y) ∧
inj_exp (Trn x) = inj_exp (Trn y)"
using inj_some_pair
by (metis Pair_inject
‹Some (some_pair (some_inj_resid (Dom x),
some_pair (some_inj_resid (Cod x), inj_exp (Trn x)))) =
Some (some_pair (some_inj_resid (Dom y),
some_pair (some_inj_resid (Cod y), inj_exp (Trn y))))›
injD option.inject)
have "Dom x = Dom y ∧ Cod x = Cod y ∧ Trn x = Trn y"
proof -
have 2: "small_rts (Dom x) ∧ small_rts (Dom y) ∧
small_rts (Cod x) ∧ small_rts (Cod y)"
using assms x y x' y' 1 arr_char inj_on_some_inj_resid small_function_resid
by blast
have 3: "Dom x = Dom y ∧ Cod x = Cod y"
using 1 2 inj_on_some_inj_resid inj_on_def
by (metis mem_Collect_eq)
moreover have "Trn x = Trn y"
proof -
have "residuation.arr (exponential_rts.resid (Dom x) (Cod x)) (Trn x) ∧
residuation.arr (exponential_rts.resid (Dom x) (Cod x)) (Trn y)"
by (metis (no_types, lifting) Un_insert_right arrE assms(3) calculation
insertE mem_Collect_eq subsetD sup_bot.right_neutral x x' y y')
thus ?thesis
using 1 2 inj_inj_exp inj_on_def [of inj_exp]
arr_char assms(3) x x'
by auto
qed
ultimately show ?thesis by blast
qed
thus "x = y"
apply (cases x; cases y)
apply auto[4]
using x' y' by blast+
qed
ultimately show ?thesis by blast
qed
qed
text‹
The following result says that, for any small extensional RTS ‹A› whose arrows
inhabit type @{typ "'A arr resid"} and are drawn from among the arrows and null
of @{locale rtscatx}, there is an object ‹a› of @{locale rtscatx} such that the
RTS ‹HOM ❙𝟭 a› is isomorphic to ‹A›. It is expressed in terms that are intrinsic
to ‹❙R❙T❙S⇧†› as an abstract RTS-category, as opposed to the fact ‹bij_mkobj›,
which uses the extrinsically given mapping @{term Dom}.
The result is proved by taking an isomorphic image of the given RTS ‹A› under the
injective mapping ‹inj_arr :: 'A arr ⇒ 'A›, then applying ‹bij_mkobj›
to obtain the corresponding object ‹a›, and finally using the isomorphism
‹Dom a ≅ HOM ❙𝟭 a› to conclude that ‹HOM ❙𝟭 a ≅ A›.
›
lemma obj_replete:
fixes A :: "'A arr resid"
assumes "small_rts A ∧ extensional_rts A"
and "Collect (residuation.arr A) ∪
{ResiduatedTransitionSystem.partial_magma.null A}
⊆ Collect arr ∪ {null}"
shows "∃a. obj a ∧ isomorphic_rts A (HOM ❙𝟭 a)"
proof -
interpret A: small_rts A
using assms by blast
interpret A: extensional_rts A
using assms by blast
obtain ι :: "'A arr ⇒ 'A"
where ι: "inj_on ι (Collect A.arr ∪ {A.null})"
using assms inj_inj_arr [of A] null_char by auto
interpret ιA: inj_image_rts ι A
using ι by unfold_locales blast
have "small_rts ιA.resid ∧ extensional_rts ιA.resid"
using assms ιA.preserves_reflects_small_rts ιA.preserves_extensional_rts
by blast
have ιA: "isomorphic_rts A ιA.resid"
using ιA.F.invertible isomorphic_rts_def by blast
let ?a = "mkobj ιA.resid"
have a: "obj ?a ∧ Dom ?a = ιA.resid"
using ‹small_rts ιA.resid ∧ extensional_rts ιA.resid› bij_mkobj by auto
hence "obj ?a ∧ isomorphic_rts ιA.resid (HOM ❙𝟭 ?a)"
using inverse_simulations_DN_UP [of ?a] isomorphic_rts_def by auto
hence "obj ?a ∧ isomorphic_rts A (HOM ❙𝟭 ?a)"
using ιA isomorphic_rts_transitive by blast
thus ?thesis by blast
qed
text‹
We now turn our attention to showing that, for any given objects ‹a› and ‹b›,
the states from ‹a› to ‹b› correspond bijectively (via the ``covariant hom''
mapping @{term cov_HOM}) to simulations from ‹HOM ❙𝟭 a› to ‹HOM ❙𝟭 b› and the arrows
from ‹a› to ‹b› correspond bijectively to the transformations between such simulations.
›
lemma HOM1_faithful_for_sta:
assumes "«f : a →⇩s⇩t⇩a b»" and "«g : a →⇩s⇩t⇩a b»"
and "cov_HOM ❙𝟭 f = cov_HOM ❙𝟭 g"
shows "f = g"
proof -
interpret A: extensional_rts ‹Dom a›
using assms(1) obj_char arr_char
by (metis (no_types, lifting) H.ide_dom H.in_homE Int_Collect mem_Collect_eq)
interpret A: small_rts ‹Dom a›
using assms(1) obj_char arr_char
by (metis (no_types, lifting) H.ide_dom H.in_homE Int_Collect)
interpret B: extensional_rts ‹Dom b›
using assms(1) obj_char arr_char
by (metis (no_types, lifting) H.ide_cod H.in_homE Int_Collect mem_Collect_eq)
interpret AB: exponential_rts ‹Dom a› ‹Dom b› ..
interpret HOM_1a: sub_rts resid ‹λt. «t : ❙𝟭 → a»›
using sub_rts_HOM by simp
interpret F: simulation ‹Dom a› ‹Dom b› ‹AB.Map (Trn f)›
using assms(1) sta_char
by (metis (no_types, lifting) AB.ide_char⇩E⇩R⇩T⇩S Dom_cod Dom_dom
H.in_homE V.residuation_axioms residuation.ide_implies_arr)
interpret G: simulation ‹Dom a› ‹Dom b› ‹AB.Map (Trn g)›
using assms(2) sta_char
by (metis (no_types, lifting) AB.ide_char⇩E⇩R⇩T⇩S Dom_cod Dom_dom
H.in_homE V.residuation_axioms residuation.ide_implies_arr)
have "⋀Q R T. transformation (\\⇩1) (Dom a) Q R T
⟹ AB.Map (Trn f) ∘ T = AB.Map (Trn g) ∘ T"
proof -
fix Q R T
assume T: "transformation (\\⇩1) (Dom a) Q R T"
interpret T: transformation ‹(\⇩1)› ‹Dom a› Q R T
using T by blast
let ?t = "mkarr One.resid (Dom a) Q R T"
have t: "«?t : ❙𝟭 → a»"
proof
show "H.arr ?t"
using A.extensional_rts_axioms A.small_rts_axioms One.is_extensional_rts
One.small_rts_axioms T
by auto
show "dom ?t = ❙𝟭"
by (simp add: A.extensional_rts_axioms A.small_rts_axioms
One.is_extensional_rts One.small_rts_axioms T arr_mkarr(4) one_def)
show "cod ?t = a"
using One.is_extensional_rts One.small_rts_axioms T assms(1) dom_char
by fastforce
qed
hence "HOM_1a.arr ?t"
using assms HOM_1a.arr_char by blast
moreover have "dom f = a" and "dom g = a"
using assms by blast+
ultimately have 1: "f ⋆ ?t = g ⋆ ?t"
using assms
by auto meson
have "AB.Map (Trn f) ∘ T = Map f ∘ T"
by simp
also have "... = Map (f ⋆ ?t)"
by (metis (no_types, lifting) A.extensional_rts_axioms
A.small_rts_axioms H.seqI' Map_hcomp One.is_extensional_rts
One.small_rts_axioms T assms(1) bij_mkarr(3) t transformation_def)
also have "... = Map (g ⋆ ?t)"
using 1 by simp
also have "... = Map g ∘ T"
using assms t Map_hcomp [of g ?t] mkarr_def by auto
also have "... = AB.Map (Trn g) ∘ T"
by simp
finally show "AB.Map (Trn f) ∘ T = AB.Map (Trn g) ∘ T" by blast
qed
thus ?thesis
using One.eq_simulation_iff A.weakly_extensional_rts_axioms
B.weakly_extensional_rts_axioms F.simulation_axioms
G.simulation_axioms
by (metis (no_types, lifting) AB.MkIde_Map Dom_cod Dom_dom H.in_homE
MkArr_Trn V.ide_implies_arr assms(1-2) sta_char)
qed
lemma HOM1_faithful_for_arr:
assumes "arr t" and "arr u" and "src t = src u" and "trg t = trg u"
and "cov_HOM ❙𝟭 t = cov_HOM ❙𝟭 u"
shows "t = u"
proof (intro arr_eqI)
let ?a = "dom t" and ?b = "cod t"
have a: "dom t = ?a ∧ dom u = ?a"
using assms dom_src [of t] by auto
have b: "cod t = ?b ∧ cod u = ?b"
using assms cod_src [of t] by auto
let ?A = "Dom t" and ?B = "Cod t"
have A: "Dom t = ?A ∧ Dom u = ?A"
using assms Dom_src [of t] by auto
have B: "Cod t = ?B ∧ Cod u = ?B"
using assms Cod_src [of t] by auto
interpret A: extensional_rts ?A
using assms(1) arr_char by blast
interpret A: small_rts ?A
using assms(1) arr_char by auto
interpret B: extensional_rts ?B
using assms(1) arr_char by auto
interpret AB: exponential_rts ?A ?B ..
interpret HOM_1a: sub_rts resid ‹λx. «x : ❙𝟭 → dom t»›
using sub_rts_HOM by blast
interpret HOM_1b: sub_rts resid ‹λx. «x : ❙𝟭 → cod t»›
using sub_rts_HOM by blast
have *: "⋀Q R X. transformation (\\⇩1) ?A Q R X
⟹ AB.Map (Trn t) ∘ X = AB.Map (Trn u) ∘ X"
proof -
fix Q R X
assume X: "transformation (\\⇩1) ?A Q R X"
interpret X: transformation ‹(\⇩1)› ?A Q R X
using X by blast
let ?x = "mkarr One.resid ?A Q R X"
have x: "«?x : ❙𝟭 → ?a»"
proof
show 1: "H.arr (mkarr (\\⇩1) (Dom t) Q R X)"
using X arr_mkarr(1) [of One.resid ?A Q R X]
One.small_rts_axioms One.extensional_rts_axioms
A.small_rts_axioms A.extensional_rts_axioms
by simp
show "dom (mkarr (\\⇩1) (Dom t) Q R X) = ❙𝟭"
using X arr_mkarr(4) [of One.resid ?A Q R X] one_def
One.small_rts_axioms One.extensional_rts_axioms
A.small_rts_axioms A.extensional_rts_axioms
by metis
show "cod (mkarr (\\⇩1) (Dom t) Q R X) = ?a"
proof -
have "(λta. if A.arr ta then ta
else ResiduatedTransitionSystem.partial_magma.null
(Dom (dom t))) =
I (Dom t)"
using assms(1) Dom_dom by presburger
thus ?thesis
using assms(1) X arr_mkarr(5) obj_char [of ?a] Dom_dom
One.small_rts_axioms One.extensional_rts_axioms
A.small_rts_axioms A.extensional_rts_axioms
by simp
qed
qed
have 1: "t ⋆ ?x = u ⋆ ?x"
proof -
have "HOM_1a.arr ?x"
using assms x HOM_1a.arr_char by blast
moreover have "dom t = ?a" and "dom u = ?a"
using a by blast+
ultimately show ?thesis
using assms
by auto meson
qed
have "AB.Map (Trn t) ∘ X = Map t ∘ X"
by simp
also have "... = Map (t ⋆ ?x)"
proof -
have "H.seq t ?x"
using assms x H.seqI by auto
thus ?thesis
using assms x Map_hcomp mkarr_def by simp
qed
also have "... = Map (u ⋆ ?x)"
using 1 by simp
also have "... = Map u ∘ X"
proof -
have "H.seq u ?x"
by (metis (no_types, lifting) "1" H.arr_cod_iff_arr H.dom_null
H.ext H.in_homE H.seqI dom_char x)
thus ?thesis
using assms x Map_hcomp mkarr_def by simp
qed
also have "... = AB.Map (Trn u) ∘ X"
by simp
finally show "AB.Map (Trn t) ∘ X = AB.Map (Trn u) ∘ X" by blast
qed
show "t ≠ Null" and "u ≠ Null"
using assms(1-2) arr_char by blast+
show "Dom t = Dom u" and "Cod t = Cod u"
using A B by auto
show "Trn t = Trn u"
proof (intro AB.arr_eqI)
show "AB.arr (Trn t)" and "AB.arr (Trn u)"
using assms(1-2) A B arr_char by auto
show Dom: "AB.Dom (Trn t) = AB.Dom (Trn u)"
using assms(1-3) arr_char Map_simps
apply auto[1]
by (metis (no_types, lifting))
show Cod: "AB.Cod (Trn t) = AB.Cod (Trn u)"
using assms(1-2,4) arr_char Map_simps
apply auto[1]
by (metis (no_types, lifting))
have "AB.Map (Trn t) = AB.Map (Trn u)"
using assms(1-2) * Dom Cod A B arr_char arr_char
AB.arr_char AB.arr_char
One.eq_transformation_iff
[of ?A ?B "AB.Dom (Trn t)" "AB.Cod (Trn t)"
"AB.Map (Trn t)" "AB.Map (Trn u)"]
A.weakly_extensional_rts_axioms
B.weakly_extensional_rts_axioms
by simp
thus "⋀a. A.ide a ⟹ AB.Map (Trn t) a = AB.Map (Trn u) a" by simp
qed
qed
lemma HOM1_full_for_sta:
assumes "obj a" and "obj b" and "simulation (HOM ❙𝟭 a) (HOM ❙𝟭 b) F"
shows "∃f. «f : a → b» ∧ sta f ∧ cov_HOM ❙𝟭 f = F"
proof -
interpret A: extensional_rts ‹Dom a›
using assms obj_char arr_char by blast
interpret A: small_rts ‹Dom a›
using assms obj_char arr_char by blast
interpret B: extensional_rts ‹Dom b›
using assms obj_char arr_char by blast
interpret B: small_rts ‹Dom b›
using assms obj_char arr_char by blast
interpret A1: exponential_by_One arr_type ‹Dom a› ..
interpret B1: exponential_by_One arr_type ‹Dom b› ..
interpret HOM_1a: sub_rts resid ‹λt. «t: ❙𝟭 → a»›
using assms sub_rts_HOM by blast
interpret HOM_1b: sub_rts resid ‹λt. «t: ❙𝟭 → b»›
using assms sub_rts_HOM by blast
interpret UP_DN_a: inverse_simulations
‹Dom a› HOM_1a.resid ‹DN⇩r⇩t⇩s a› ‹UP⇩r⇩t⇩s a›
using assms inverse_simulations_DN_UP [of a] dom_char
by (metis one_def)
interpret UP_DN_b: inverse_simulations
‹Dom b› HOM_1b.resid ‹DN⇩r⇩t⇩s b› ‹UP⇩r⇩t⇩s b›
using assms inverse_simulations_DN_UP [of b] dom_char
by (metis one_def)
interpret F: simulation ‹HOM ❙𝟭 a› ‹HOM ❙𝟭 b› F
using assms by blast
interpret F': simulation ‹Dom a› ‹Dom b› ‹DN⇩r⇩t⇩s b ∘ F ∘ UP⇩r⇩t⇩s a›
using simulation_comp UP_DN_a.G.simulation_axioms
UP_DN_b.F.simulation_axioms F.simulation_axioms
by blast
interpret F': simulation_as_transformation
‹Dom a› ‹Dom b› ‹DN⇩r⇩t⇩s b ∘ F ∘ UP⇩r⇩t⇩s a› ..
show "∃f. «f : a → b» ∧ sta f ∧ cov_HOM ❙𝟭 f = F"
proof -
define f
where f_def: "f = mksta (Dom a) (Dom b) (DN⇩r⇩t⇩s b ∘ F ∘ UP⇩r⇩t⇩s a)"
have sta_f: "sta f"
unfolding f_def
using sta_mksta(1) F'.simulation_axioms
A.small_rts_axioms A.extensional_rts_axioms
B.small_rts_axioms B.extensional_rts_axioms
by blast
moreover have f: "«f : a → b»"
using assms sta_f f_def
by (intro H.in_homI) auto
moreover have "cov_HOM ❙𝟭 f = F"
proof -
have "cov_HOM ❙𝟭 f = UP⇩r⇩t⇩s b ∘ Map f ∘ DN⇩r⇩t⇩s a"
using f sta_f dom_char cod_char UP_DN_naturality(3) [of f]
by auto
also have "... = (UP⇩r⇩t⇩s b ∘ DN⇩r⇩t⇩s b) ∘ F ∘ (UP⇩r⇩t⇩s a ∘ DN⇩r⇩t⇩s a)"
proof -
have "... = UP⇩r⇩t⇩s b ∘ (DN⇩r⇩t⇩s b ∘ F ∘ UP⇩r⇩t⇩s a) ∘ DN⇩r⇩t⇩s a"
using f_def mkarr_def by auto
thus ?thesis
using comp_assoc by (metis (no_types, lifting))
qed
also have "... = F ∘ (UP⇩r⇩t⇩s a ∘ DN⇩r⇩t⇩s a)"
using comp_identity_simulation [of HOM_1a.resid HOM_1b.resid F]
F.simulation_axioms UP_DN_b.inv
by auto
also have "... = F"
using comp_simulation_identity [of HOM_1a.resid HOM_1b.resid F]
F.simulation_axioms UP_DN_a.inv
by auto
finally show ?thesis by blast
qed
ultimately show ?thesis by blast
qed
qed
lemma HOM1_full_for_arr:
assumes "sta f" and "sta g" and "H.par f g"
and "transformation (HOM ❙𝟭 (dom f)) (HOM ❙𝟭 (cod f))
(cov_HOM ❙𝟭 f) (cov_HOM ❙𝟭 g) T"
shows "∃t. arr t ∧ src t = f ∧ trg t = g ∧ cov_HOM ❙𝟭 t = T"
proof -
let ?a = "dom f" and ?b = "cod f"
have a: "obj ?a" and b: "obj ?b"
using assms by auto
have f: "«f : ?a → ?b»" and g: "«g : ?a → ?b»"
using assms by auto
let ?A = "Dom ?a" and ?B = "Dom ?b"
have 0: "Dom f = ?A ∧ Cod f = ?B ∧ Dom g = ?A ∧ Cod g = ?B"
using assms f dom_char cod_char
by (metis (no_types, lifting) Dom_cod Dom_dom arr_coincidence)
have A: "small_rts ?A ∧ extensional_rts ?A"
using assms arr_char by auto
have B: "small_rts ?B ∧ extensional_rts ?B"
using assms arr_char by auto
interpret A: extensional_rts ?A using A by blast
interpret A: small_rts ?A using A by blast
interpret B: extensional_rts ?B using B by blast
interpret B: small_rts ?B using B by blast
interpret AB: exponential_rts ?A ?B ..
interpret HOM_1a: sub_rts resid ‹λt. «t: ❙𝟭 → ?a»›
using a sub_rts_HOM by blast
interpret HOM_1a: sub_rts_of_extensional_rts resid ‹λt. «t: ❙𝟭 → ?a»› ..
interpret HOM_1a: small_rts ‹HOM ❙𝟭 ?a›
proof -
have "Collect HOM_1a.arr ⊆ H.hom ❙𝟭 ?a"
using HOM_1a.arr_char by blast
thus "small_rts (HOM ❙𝟭 ?a)"
using assms obj_one H.terminal_def small_homs [of "❙𝟭" ?a]
smaller_than_small
by unfold_locales auto
qed
interpret HOM_1b: sub_rts resid ‹λt. «t: ❙𝟭 → ?b»›
using b sub_rts_HOM by blast
interpret HOM_1b: sub_rts_of_extensional_rts resid ‹λt. «t: ❙𝟭 → ?b»› ..
interpret HOM_1b: small_rts ‹HOM ❙𝟭 ?b›
proof -
have "Collect HOM_1b.arr ⊆ H.hom ❙𝟭 ?b"
using HOM_1b.arr_char by blast
thus "small_rts (HOM ❙𝟭 ?b)"
using assms obj_one H.terminal_def small_homs [of "❙𝟭" ?b]
smaller_than_small
by unfold_locales auto
qed
interpret UP_DN_a: inverse_simulations
?A HOM_1a.resid ‹DN⇩r⇩t⇩s ?a› ‹UP⇩r⇩t⇩s ?a›
using assms a inverse_simulations_DN_UP [of ?a] dom_char one_def
by metis
interpret UP_DN_b: inverse_simulations
?B HOM_1b.resid ‹DN⇩r⇩t⇩s ?b› ‹UP⇩r⇩t⇩s ?b›
using assms b inverse_simulations_DN_UP [of ?b] dom_char one_def
by metis
interpret T: transformation
‹HOM ❙𝟭 ?a› ‹HOM ❙𝟭 ?b› ‹cov_HOM ❙𝟭 f› ‹cov_HOM ❙𝟭 g› T
using assms(4) by blast
interpret F': simulation ?A ?B ‹DN⇩r⇩t⇩s ?b ∘ cov_HOM ❙𝟭 f ∘ UP⇩r⇩t⇩s ?a›
using simulation_comp UP_DN_a.G.simulation_axioms
UP_DN_b.F.simulation_axioms T.F.simulation_axioms
by blast
interpret G': simulation ?A ?B ‹DN⇩r⇩t⇩s ?b ∘ cov_HOM ❙𝟭 g ∘ UP⇩r⇩t⇩s ?a›
using simulation_comp UP_DN_a.G.simulation_axioms
UP_DN_b.F.simulation_axioms T.G.simulation_axioms
by blast
interpret DN_T: transformation HOM_1a.resid ?B
‹DN⇩r⇩t⇩s ?b ∘ cov_HOM ❙𝟭 f› ‹DN⇩r⇩t⇩s ?b ∘ cov_HOM ❙𝟭 g›
‹DN⇩r⇩t⇩s ?b ∘ T›
using UP_DN_a.G.simulation_axioms UP_DN_b.F.simulation_axioms
T.transformation_axioms F'.simulation_axioms G'.simulation_axioms
transformation_whisker_left B.weakly_extensional_rts_axioms
by fastforce
interpret T': transformation ?A ?B
‹DN⇩r⇩t⇩s ?b ∘ cov_HOM ❙𝟭 f ∘ UP⇩r⇩t⇩s ?a›
‹DN⇩r⇩t⇩s ?b ∘ cov_HOM ❙𝟭 g ∘ UP⇩r⇩t⇩s ?a›
‹DN⇩r⇩t⇩s ?b ∘ T ∘ UP⇩r⇩t⇩s ?a›
using UP_DN_a.G.simulation_axioms UP_DN_b.F.simulation_axioms
T.transformation_axioms DN_T.transformation_axioms
DN_T.F.simulation_axioms DN_T.G.simulation_axioms
transformation_whisker_right A.weakly_extensional_rts_axioms
by fastforce
define t
where t_def: "t = mkarr ?A ?B
(DN⇩r⇩t⇩s ?b ∘ cov_HOM ❙𝟭 f ∘ UP⇩r⇩t⇩s ?a)
(DN⇩r⇩t⇩s ?b ∘ cov_HOM ❙𝟭 g ∘ UP⇩r⇩t⇩s ?a)
(DN⇩r⇩t⇩s ?b ∘ T ∘ UP⇩r⇩t⇩s ?a)"
have t: "«t : ?a → ?b»"
proof
show t: "H.arr t"
proof -
have "V.arr t"
unfolding t_def
using arr_mkarr(1) T'.transformation_axioms
F'.simulation_axioms G'.simulation_axioms
A.small_rts_axioms A.extensional_rts_axioms
B.small_rts_axioms B.extensional_rts_axioms
by blast
thus ?thesis by auto
qed
show "dom t = ?a"
using assms(3) a t f dom_char t_def by auto
show "cod t = ?b"
using assms(3) b t f cod_char t_def by auto
qed
have 1: "arr t"
using t by auto
moreover have "src t = f"
proof -
have 2: "src t = mksta ?A ?B (DN⇩r⇩t⇩s ?b ∘ cov_HOM ❙𝟭 f ∘ UP⇩r⇩t⇩s ?a)"
using t t_def mkarr_simps(3) A.small_rts_axioms A.extensional_rts_axioms
B.small_rts_axioms B.extensional_rts_axioms T'.transformation_axioms
by blast
also have "... = f"
proof (intro arr_eqI)
show "mksta ?A ?B (DN⇩r⇩t⇩s ?b ∘ cov_HOM ❙𝟭 f ∘ UP⇩r⇩t⇩s ?a) ≠ Null"
unfolding mkarr_def by blast
show "f ≠ Null"
using f H_arr_char by blast
show "Dom (mksta ?A ?B (DN⇩r⇩t⇩s ?b ∘ cov_HOM ❙𝟭 f ∘ UP⇩r⇩t⇩s ?a)) =
Dom f"
using f dom_char mkarr_def by auto
show "Cod (mksta ?A ?B (DN⇩r⇩t⇩s ?b ∘ cov_HOM ❙𝟭 f ∘ UP⇩r⇩t⇩s ?a)) =
Cod f"
using f cod_char mkarr_def by auto
show "Trn (mksta ?A ?B (DN⇩r⇩t⇩s ?b ∘ cov_HOM ❙𝟭 f ∘ UP⇩r⇩t⇩s ?a)) =
Trn f"
proof -
have "Trn (mksta ?A ?B (DN⇩r⇩t⇩s ?b ∘ cov_HOM ❙𝟭 f ∘ UP⇩r⇩t⇩s ?a)) =
AB.MkIde (DN⇩r⇩t⇩s ?b ∘ cov_HOM ❙𝟭 f ∘ UP⇩r⇩t⇩s ?a)"
using mkarr_def by simp
also have "... = Trn f"
proof (intro AB.arr_eqI)
show "AB.arr (AB.MkIde (DN⇩r⇩t⇩s ?b ∘ cov_HOM ❙𝟭 f ∘ UP⇩r⇩t⇩s ?a))"
proof -
have "arr (src t)"
using 1 V.arr_src_iff_arr by blast
thus ?thesis
using 2 arr_char mkarr_def by auto
qed
show "AB.arr (Trn f)"
using f arr_char [of f] dom_char cod_char by auto
show "AB.Dom (AB.MkIde (DN⇩r⇩t⇩s ?b ∘ cov_HOM ❙𝟭 f ∘ UP⇩r⇩t⇩s ?a)) =
AB.Dom (Trn f)"
proof -
have "AB.Dom (AB.MkIde (DN⇩r⇩t⇩s ?b ∘ cov_HOM ❙𝟭 f ∘ UP⇩r⇩t⇩s ?a)) =
DN⇩r⇩t⇩s ?b ∘ cov_HOM ❙𝟭 f ∘ UP⇩r⇩t⇩s ?a"
by simp
also have "... = AB.Map (Trn f)"
using assms f 0 UP_DN_naturality(4) by simp
also have "... = AB.Dom (Trn f)"
using assms sta_char dom_char cod_char AB.ide_char⇩E⇩R⇩T⇩S
by fastforce
finally show ?thesis by blast
qed
show "AB.Cod (AB.MkIde (DN⇩r⇩t⇩s ?b ∘ cov_HOM ❙𝟭 f ∘ UP⇩r⇩t⇩s ?a)) =
AB.Cod (Trn f)"
proof -
have "AB.Cod (AB.MkIde (DN⇩r⇩t⇩s ?b ∘ cov_HOM ❙𝟭 f ∘ UP⇩r⇩t⇩s ?a)) =
DN⇩r⇩t⇩s ?b ∘ cov_HOM ❙𝟭 f ∘ UP⇩r⇩t⇩s ?a"
by simp
also have "... = AB.Map (Trn f)"
using assms f 0 UP_DN_naturality(4) by simp
also have "... = AB.Cod (Trn f)"
using assms sta_char dom_char cod_char AB.ide_char⇩E⇩R⇩T⇩S
by fastforce
finally show ?thesis by blast
qed
show "⋀x. A.ide x ⟹
AB.Map
(AB.MkIde (DN⇩r⇩t⇩s ?b ∘ cov_HOM ❙𝟭 f ∘ UP⇩r⇩t⇩s ?a)) x =
AB.Map (Trn f) x"
proof -
fix x
assume x: "A.ide x"
have "AB.Map
(AB.MkIde (DN⇩r⇩t⇩s ?b ∘ cov_HOM ❙𝟭 f ∘ UP⇩r⇩t⇩s ?a)) x =
(DN⇩r⇩t⇩s ?b ∘ cov_HOM ❙𝟭 f ∘ UP⇩r⇩t⇩s ?a) x"
by simp
also have "... = AB.Map (Trn f) x"
using assms f 0 UP_DN_naturality(4) [of f] by simp
finally
show "AB.Map
(AB.MkIde (DN⇩r⇩t⇩s ?b ∘ cov_HOM ❙𝟭 f ∘ UP⇩r⇩t⇩s ?a)) x =
AB.Map (Trn f) x"
by blast
qed
qed
finally show ?thesis by blast
qed
qed
finally show ?thesis by blast
qed
moreover have "trg t = g"
proof -
have 2: "trg t = mksta ?A ?B (DN⇩r⇩t⇩s ?b ∘ cov_HOM ❙𝟭 g ∘ UP⇩r⇩t⇩s ?a)"
using t t_def mkarr_simps(4) A.small_rts_axioms A.extensional_rts_axioms
B.small_rts_axioms B.extensional_rts_axioms T'.transformation_axioms
by blast
also have "... = g"
proof (intro arr_eqI)
show "mksta ?A ?B (DN⇩r⇩t⇩s ?b ∘ cov_HOM ❙𝟭 g ∘ UP⇩r⇩t⇩s ?a) ≠ Null"
unfolding mkarr_def by blast
show "g ≠ Null"
using g H_arr_char by blast
show "Dom (mksta ?A ?B (DN⇩r⇩t⇩s ?b ∘ cov_HOM ❙𝟭 g ∘ UP⇩r⇩t⇩s ?a)) =
Dom g"
using assms g dom_char mkarr_def by auto
show "Cod (mksta ?A ?B (DN⇩r⇩t⇩s ?b ∘ cov_HOM ❙𝟭 g ∘ UP⇩r⇩t⇩s ?a)) = Cod g"
using assms g cod_char mkarr_def by auto
show "Trn (mksta ?A ?B (DN⇩r⇩t⇩s ?b ∘ cov_HOM ❙𝟭 g ∘ UP⇩r⇩t⇩s ?a)) = Trn g"
proof -
have 3: "DN⇩r⇩t⇩s ?b ∘ cov_HOM ❙𝟭 g ∘ UP⇩r⇩t⇩s ?a = AB.Map (Trn g)"
using assms g 0 UP_DN_naturality(4)
apply simp
by presburger
have "Trn (mksta ?A ?B (DN⇩r⇩t⇩s ?b ∘ cov_HOM ❙𝟭 g ∘ UP⇩r⇩t⇩s ?a)) =
AB.MkIde (DN⇩r⇩t⇩s ?b ∘ cov_HOM ❙𝟭 g ∘ UP⇩r⇩t⇩s ?a)"
using mkarr_def by simp
also have "... = Trn g"
proof (intro AB.arr_eqI)
show "AB.arr (AB.MkIde (DN⇩r⇩t⇩s ?b ∘ cov_HOM ❙𝟭 g ∘ UP⇩r⇩t⇩s ?a))"
using AB.ide_implies_arr G'.simulation_axioms by blast
show "AB.arr (Trn g)"
using assms g arr_char [of g] dom_char cod_char by auto
show "AB.Dom (AB.MkIde (DN⇩r⇩t⇩s ?b ∘ cov_HOM ❙𝟭 g ∘ UP⇩r⇩t⇩s ?a)) =
AB.Dom (Trn g)"
using assms 3 sta_char AB.ide_char⇩E⇩R⇩T⇩S by simp
show "AB.Cod (AB.MkIde (DN⇩r⇩t⇩s ?b ∘ cov_HOM ❙𝟭 g ∘ UP⇩r⇩t⇩s ?a)) =
AB.Cod (Trn g)"
using assms 3 sta_char AB.ide_char⇩E⇩R⇩T⇩S by simp
show "⋀x. A.ide x ⟹
AB.Map
(AB.MkIde (DN⇩r⇩t⇩s ?b ∘ cov_HOM ❙𝟭 g ∘ UP⇩r⇩t⇩s ?a)) x =
AB.Map (Trn g) x"
using 3 by simp
qed
finally show ?thesis by blast
qed
qed
finally show ?thesis by blast
qed
moreover have "cov_HOM ❙𝟭 t = T"
proof -
have "cov_HOM ❙𝟭 t = UP⇩r⇩t⇩s ?b ∘ Map t ∘ DN⇩r⇩t⇩s ?a"
proof -
have "arr t ∧ dom f = dom t ∧ cod f = cod t"
using f t by auto
thus ?thesis
using UP_DN_naturality(3) [of t] by presburger
qed
also have "... = UP⇩r⇩t⇩s ?b ∘ (DN⇩r⇩t⇩s ?b ∘ T ∘ UP⇩r⇩t⇩s ?a) ∘ DN⇩r⇩t⇩s ?a"
unfolding t_def mkarr_def by simp
also have "... = (UP⇩r⇩t⇩s ?b ∘ DN⇩r⇩t⇩s ?b) ∘ T ∘ (UP⇩r⇩t⇩s ?a ∘ DN⇩r⇩t⇩s ?a)"
using comp_assoc by smt
also have "... = T ∘ (UP⇩r⇩t⇩s ?a ∘ DN⇩r⇩t⇩s ?a)"
using comp_identity_transformation
[of HOM_1a.resid HOM_1b.resid _ _ T]
T.transformation_axioms UP_DN_b.inv
by auto
also have "... = T"
using comp_transformation_identity
[of HOM_1a.resid HOM_1b.resid _ _ T]
T.transformation_axioms UP_DN_a.inv
by auto
finally show ?thesis by blast
qed
ultimately show ?thesis by blast
qed
lemma bij_HOM1_sta:
assumes "obj a" and "obj b"
shows "bij_betw (cov_HOM ❙𝟭) {f. «f : a →⇩s⇩t⇩a b»}
(Collect (simulation (HOM ❙𝟭 a) (HOM ❙𝟭 b)))"
proof -
interpret HOM_1a: sub_rts resid ‹λt. «t : ❙𝟭 → a»›
using assms(1) sub_rts_HOM by blast
interpret HOM_1b: sub_rts resid ‹λt. «t : ❙𝟭 → b»›
using assms(2) sub_rts_HOM by blast
have 1: "cov_HOM ❙𝟭 ∈ {f. «f : a →⇩s⇩t⇩a b»}
→ Collect (simulation (HOM ❙𝟭 a) (HOM ❙𝟭 b))"
proof
fix f
assume f: "f ∈ {f. «f : a →⇩s⇩t⇩a b»}"
have "sta f ∧ dom f = a ∧ cod f = b"
using f by auto
thus "cov_HOM ❙𝟭 f ∈ Collect (simulation (HOM ❙𝟭 a) (HOM ❙𝟭 b))"
using simulation_cov_HOM_sta [of "❙𝟭" f] by blast
qed
show "bij_betw (cov_HOM ❙𝟭) {f. «f : a →⇩s⇩t⇩a b»}
(Collect (simulation (HOM ❙𝟭 a) (HOM ❙𝟭 b)))"
proof (unfold bij_betw_def, intro conjI)
show "inj_on (cov_HOM ❙𝟭) {f. «f : a →⇩s⇩t⇩a b»}"
using assms HOM1_faithful_for_sta [of _ a b]
unfolding inj_on_def
by auto
show "cov_HOM ❙𝟭 ` {f. «f : a →⇩s⇩t⇩a b»} =
Collect (simulation (HOM ❙𝟭 a) (HOM ❙𝟭 b))"
proof
show "cov_HOM ❙𝟭 ` {f. «f : a →⇩s⇩t⇩a b»}
⊆ Collect (simulation HOM_1a.resid HOM_1b.resid)"
using 1 by blast
show "Collect (simulation HOM_1a.resid HOM_1b.resid)
⊆ cov_HOM ❙𝟭 ` {f. «f : a →⇩s⇩t⇩a b»}"
proof
fix F
assume F: "F ∈ Collect (simulation HOM_1a.resid HOM_1b.resid)"
obtain f where f: "«f : a →⇩s⇩t⇩a b» ∧ cov_HOM ❙𝟭 f = F"
using assms F HOM1_full_for_sta [of a b F]
HOM_1a.arr_char HOM_1b.arr_char
by auto
show "F ∈ cov_HOM ❙𝟭 ` {f. «f : a →⇩s⇩t⇩a b»}"
using f by blast
qed
qed
qed
qed
lemma bij_HOM1_arr:
assumes "«f : a →⇩s⇩t⇩a b»" and "«g : a →⇩s⇩t⇩a b»"
shows "bij_betw (cov_HOM ❙𝟭) {t. «t : f ⇒ g»}
(Collect (transformation (HOM ❙𝟭 a) (HOM ❙𝟭 b)
(cov_HOM ❙𝟭 f) (cov_HOM ❙𝟭 g)))"
proof -
interpret HOM_1a: sub_rts resid ‹λt. «t : ❙𝟭 → a»›
using assms(1) sub_rts_HOM by blast
interpret HOM_1b: sub_rts resid ‹λt. «t : ❙𝟭 → b»›
using assms(2) sub_rts_HOM by blast
have 1: "cov_HOM ❙𝟭 ∈
{t. «t : f ⇒ g»}
→ Collect (transformation
(HOM ❙𝟭 a) (HOM ❙𝟭 b) (cov_HOM ❙𝟭 f) (cov_HOM ❙𝟭 g))"
proof
fix t
assume t: "t ∈ {t. «t : f ⇒ g»}"
thus "cov_HOM ❙𝟭 t ∈ Collect (transformation (HOM ❙𝟭 a) (HOM ❙𝟭 b)
(cov_HOM ❙𝟭 f) (cov_HOM ❙𝟭 g))"
using assms(1) t transformation_cov_HOM_arr [of "❙𝟭" t] obj_one by auto
qed
show "bij_betw (cov_HOM ❙𝟭) {t. «t : f ⇒ g»}
(Collect (transformation (HOM ❙𝟭 a) (HOM ❙𝟭 b)
(cov_HOM ❙𝟭 f) (cov_HOM ❙𝟭 g)))"
proof (unfold bij_betw_def, intro conjI)
show "inj_on (cov_HOM ❙𝟭) {t. «t : f ⇒ g»}"
using assms HOM1_faithful_for_arr
unfolding inj_on_def
by auto
show "cov_HOM ❙𝟭 ` {t. «t : f ⇒ g»} =
Collect (transformation HOM_1a.resid HOM_1b.resid
(cov_HOM ❙𝟭 f) (cov_HOM ❙𝟭 g))"
proof
show "cov_HOM ❙𝟭 ` {t. «t : f ⇒ g»} ⊆
Collect (transformation HOM_1a.resid HOM_1b.resid
(cov_HOM ❙𝟭 f) (cov_HOM ❙𝟭 g))"
using 1 by blast
show "Collect (transformation HOM_1a.resid HOM_1b.resid
(cov_HOM ❙𝟭 f) (cov_HOM ❙𝟭 g)) ⊆
cov_HOM ❙𝟭 ` {t. «t : f ⇒ g»}"
proof
fix T
assume T: "T ∈ Collect (transformation HOM_1a.resid HOM_1b.resid
(cov_HOM ❙𝟭 f) (cov_HOM ❙𝟭 g))"
obtain t where t: "«t : f ⇒ g» ∧ cov_HOM ❙𝟭 t = T"
using assms T HOM1_full_for_arr [of f g T] arr_char
HOM_1a.arr_char HOM_1b.arr_char
by blast
show "T ∈ cov_HOM ❙𝟭 ` {t. arr t ∧ src t = f ∧ trg t = g}"
using t by blast
qed
qed
qed
qed
text‹
My original objective for the results in this section was to obtain a characterization
up to equivalence of the RTS-category ‹❙R❙T❙S⇧†› in terms of intrinsic notions that make
sense for any RTS-category, and to carry out the proof of cartesian closure using
@{term "HOM ❙𝟭"} in place of @{term Dom}. This can probably be done, and I did push the
idea through the construction of products, but for exponentials there were some
technicalities that started to get messy and become distractions from the main things
that I was trying to do. So I decided to leave this program for future work.
›
end
end