Theory RTSConstructions
theory RTSConstructions
imports Main Preliminaries ZFC_in_HOL.ZFC_Cardinals
begin
section "Notation"
text ‹
Some of the theories in the HOL library that we depend on define global notation involving
generic symbols that we would like to use here. It would be best if there were some way
to import these theories without also having to import this notation, but for now the best
we can do is to uninstall the notation involving the symbols at issue.
›
no_notation Equipollence.eqpoll (infixl "≈" 50)
no_notation Equipollence.lepoll (infixl "≲" 50)
no_notation Lattices.sup_class.sup (infixl "⊔" 65)
no_notation ZFC_Cardinals.cmult (infixl ‹⊗› 70)
no_syntax "_Tuple" :: "[V, Vs] ⇒ V" ("⟨(_,/ _)⟩")
no_syntax "_hpattern" :: "[pttrn, patterns] ⇒ pttrn" ("⟨(_,/ _)⟩")
section "Some Constraints on a Type"
subsection "Nondegenerate"
text ‹
We will call a type ``nondegenerate'' if it has at least two elements.
This means that the type admits RTS's with a non-empty set of arrows
(after using one of the elements for the required null value).
›
locale nondegenerate =
fixes type :: "'a itself"
assumes is_nondegenerate: "∃x y :: 'a. x ≠ y"
subsection "Lifting"
text ‹
A type ‹'a› ``admits lifting'' if there is an injection from the type ‹'a option› to ‹'a›.
›
locale lifting =
fixes type :: "'a itself"
assumes admits_lifting: "∃l :: 'a option ⇒ 'a. inj l"
begin
definition some_lift :: "'a option ⇒ 'a"
where "some_lift ≡ SOME l :: 'a option ⇒ 'a. inj l"
lemma inj_some_lift:
shows "inj some_lift"
using admits_lifting someI_ex [of "λl. inj l"] some_lift_def by fastforce
text ‹
A type that admits lifting is obviously nondegenerate.
›
sublocale nondegenerate
proof (unfold_locales, intro exI)
show "some_lift None ≠ some_lift (Some (some_lift None))"
using injD inj_some_lift by fastforce
qed
end
subsection "Pairing"
text ‹
A type ‹'a› ``admits pairing'' if there exists an injective ``pairing function'' from
‹'a * 'a› to ‹'a›. This allows us to encode pairs of elements of ‹'a› without
having to pass to a higher type.
›
locale pairing =
fixes type :: "'a itself"
assumes admits_pairing: "∃p :: 'a * 'a ⇒ 'a. inj p"
begin
definition some_pair :: "'a * 'a ⇒ 'a"
where "some_pair ≡ SOME p :: 'a * 'a ⇒ 'a. inj p"
abbreviation is_pair
where "is_pair x ≡ x ∈ range some_pair"
definition first :: "'a ⇒ 'a"
where "first x ≡ fst (inv some_pair x)"
definition second :: "'a ⇒ 'a"
where "second x = snd (inv some_pair x)"
lemma inj_some_pair:
shows "inj some_pair"
using admits_pairing someI_ex [of "λp. inj p"] some_pair_def by fastforce
lemma first_conv:
shows "first (some_pair (x, y)) = x"
using first_def inj_some_pair by auto
lemma second_conv:
shows "second (some_pair (x, y)) = y"
using second_def inj_some_pair by auto
lemma pair_conv:
assumes "is_pair x"
shows "some_pair (first x, second x) = x"
using assms first_def second_def inj_some_pair by force
end
text ‹
A type that is nondegenerate and admits pairing also admits lifting.
›
locale nondegenerate_and_pairing =
nondegenerate + pairing
begin
sublocale lifting type
proof
obtain c :: 'a where c: "∀x. c ≠ some_pair (c, x)"
using is_nondegenerate inj_some_pair
by (metis (full_types) first_conv second_conv)
let ?f = "λNone ⇒ c | Some x ⇒ some_pair (c, x)"
have "inj ?f"
unfolding inj_def
by (metis (no_types, lifting) c option.case_eq_if option.collapse
second_conv)
thus "∃l :: 'a option ⇒ 'a. inj l"
by blast
qed
end
subsection "Exponentiation"
text ‹
In order to define the exponential ‹[A, B]› of an RTS ‹A› and an RTS ‹B›
at a type ‹'a› without having to pass to a higher type, we need the type ‹'a›
to be large enough to embed the set of all extensional
functions that have ``small'' sets as their domains. Here we are using the
notion of ``small'' provided by the @{session ZFC_in_HOL} extension to HOL.
Now, the standard Isabelle/HOL definition of ``extensional'' uses the specific chosen
value ‹undefined› as the default value for an extensional function outside of its domain,
but here we need to apply this concept in cases where the value could be something else
(the null value for an RTS, in particular). So, we define a notion of a function
that has at most one ``popular value'' in its range, where a popular value is one with a
``large'' preimage. If such a function in addition has a small range, then it in some
sense has a small encoding, which consists of its graph restricted to its domain
(which must then necessarily be small), paired with the single default value that it
takes outside its domain.
›
abbreviation popular_value :: "('a ⇒ 'b) ⇒ 'b ⇒ bool"
where "popular_value F y ≡ ¬ small {x. F x = y}"
definition some_popular_value :: "('a ⇒ 'b) ⇒ 'b"
where "some_popular_value F ≡ SOME y. popular_value F y"
abbreviation at_most_one_popular_value
where "at_most_one_popular_value F ≡ ∃⇩≤⇩1 y. popular_value F y"
definition small_function
where "small_function F ≡ small (range F) ∧ at_most_one_popular_value F"
lemma small_preimage_unpopular:
fixes F :: "'a ⇒ 'b"
assumes "small_function F"
shows "small {x. F x ≠ some_popular_value F}"
proof (cases "∃y. popular_value F y")
assume 1: "¬ (∃y. popular_value F y)"
have "⋀y. small {x. F x = y}"
using 1 by blast
moreover have "UNIV = (⋃y∈range F. {x. F x = y})"
by auto
ultimately have "small (UNIV :: 'a set)"
using assms(1) small_function_def by (metis small_UN)
thus ?thesis
using smaller_than_small by blast
next
assume 1: "∃y. popular_value F y"
have "popular_value F (some_popular_value F)"
using 1 someI_ex [of "λy. popular_value F y"] some_popular_value_def by metis
hence 2: "⋀y. y ≠ some_popular_value F ⟹ small {x. F x = y}"
using assms
unfolding small_function_def
by (meson Uniq_D)
moreover have "{x. F x ≠ some_popular_value F} =
(⋃y∈{y. y ∈ range F ∧ y ≠ some_popular_value F}. {x. F x = y})"
by auto
ultimately show ?thesis
using assms
unfolding small_function_def
by auto
qed
text ‹
A type ‹'a› ``admits exponentiation'' if there is an injective function that maps
each small function from ‹'a› to ‹'a› back into ‹'a›.
›
locale exponentiation =
fixes type :: "'a itself"
assumes admits_exponentiation:
"∃e :: ('a ⇒ 'a) ⇒ 'a. inj_on e (Collect small_function)"
begin
definition "some_inj" :: "('a ⇒ 'a) ⇒ 'a"
where "some_inj ≡ SOME e :: ('a ⇒ 'a) ⇒ 'a. inj_on e (Collect small_function)"
lemma inj_some_inj:
shows "inj_on some_inj (Collect small_function)"
using some_inj_def admits_exponentiation
someI_ex [of "λe :: ('a ⇒ 'a) ⇒ 'a. inj_on e (Collect small_function)"]
unfolding small_function_def
by presburger
definition app :: "'a ⇒ 'a ⇒ 'a"
where "app f ≡ inv_into
{F. small (range F) ∧
at_most_one_popular_value F} some_inj f"
lemma app_some_inj:
assumes "small_function F"
shows "app (some_inj F) = F"
by (metis (mono_tags, lifting) Collect_cong assms inv_into_f_f app_def
inj_some_inj mem_Collect_eq small_function_def)
lemma some_inj_lam_app:
assumes "f ∈ some_inj ` Collect small_function"
shows "some_inj (λx. app f x) = f"
using assms f_inv_into_f
unfolding small_function_def
by (metis (no_types, lifting) app_def)
end
context
begin
text ‹
The type @{typ V} (axiomatized in @{theory "ZFC_in_HOL.ZFC_in_HOL"}) admits exponentiation.
We show this by exhibiting a ``small encoding'' for small functions. We provide this fact
as evidence of the nontriviality of the subsequent development, in the sense that if the
existence of the type @{typ V} is consistent with HOL, then the existence of infinite types
satisfying the locale assumptions for @{locale exponentiation} is also consistent with HOL.
›
interpretation exponentiation ‹TYPE(V)›
proof
show "∃e :: (V ⇒ V) ⇒ V. inj_on e (Collect small_function)"
proof
let ?e = "λF. vpair (some_popular_value F)
(set ((λa. vpair a (F a)) ` {x. F x ≠ some_popular_value F}))"
show "inj_on ?e (Collect small_function)"
proof (intro inj_onI)
fix F F' :: "V ⇒ V"
assume F: "F ∈ Collect small_function"
assume F': "F' ∈ Collect small_function"
assume eq:
"vpair (some_popular_value F)
(set ((λa. vpair a (F a)) ` {x. F x ≠ some_popular_value F})) =
vpair (some_popular_value F')
(set ((λa. vpair a (F' a)) ` {x. F' x ≠ some_popular_value F'}))"
have 1: "some_popular_value F = some_popular_value F' ∧
set ((λa. vpair a (F a)) ` {x. F x ≠ some_popular_value F}) =
set ((λa. vpair a (F' a)) ` {x. F' x ≠ some_popular_value F'})"
using eq by blast
have 2: "(λa. vpair a (F a)) ` {x. F x ≠ some_popular_value F} =
(λa. vpair a (F' a)) ` {x. F' x ≠ some_popular_value F'}"
proof -
have "small {x. F x ≠ some_popular_value F}"
using F small_preimage_unpopular by blast
hence "small ((λa. vpair a (F a)) ` {x. F x ≠ some_popular_value F})"
by blast
thus ?thesis
by (metis (full_types) 1 F' mem_Collect_eq replacement set_injective
small_preimage_unpopular)
qed
show "F = F'"
proof
fix x
show "F x = F' x"
using 1 2
by (cases "F x = some_popular_value F") force+
qed
qed
qed
qed
lemma V_admits_exponentiation:
shows "exponentiation TYPE(V)"
..
end
subsection "Universe"
locale universe = nondegenerate_and_pairing + exponentiation
text‹
The type @{typ V} axiomatized in @{theory "ZFC_in_HOL.ZFC_in_HOL"} is a universe.
›
context
begin
interpretation nondegenerate ‹TYPE(V)›
proof
obtain f :: "bool ⇒ V" where f: "inj f"
using inj_compose inj_ord_of_nat by blast
show "∃x y :: V. x ≠ y"
by (metis Inl_Inr_iff)
qed
lemma V_is_nondegenerate:
shows "nondegenerate TYPE(V)"
..
interpretation pairing ‹TYPE(V)›
apply unfold_locales
using inj_on_vpair by blast
lemma V_admits_pairing:
shows "pairing TYPE(V)"
..
interpretation exponentiation ‹TYPE(V)›
using V_admits_exponentiation by blast
interpretation universe ‹TYPE(V)›
..
lemma V_is_universe:
shows "universe TYPE(V)"
..
end
section "Small RTS's"
text‹
We will call an RTS ``small'' if its set of arrows is a small set.
›
locale small_rts =
rts +
assumes small: "small (Collect arr)"
lemma isomorphic_to_small_rts_is_small_rts:
assumes "small_rts A" and "isomorphic_rts A B"
shows "small_rts B"
proof -
interpret A: small_rts A
using assms by blast
interpret B: rts B
using assms isomorphic_rts_def inverse_simulations_def by blast
obtain F G where FG: "inverse_simulations A B F G"
using assms isomorphic_rts_def by blast
interpret FG: inverse_simulations A B F G
using FG by blast
show "small_rts B"
using A.small FG.G.is_bijection_betw_arr_sets
apply unfold_locales
by (metis bij_betw_imp_surj_on replacement)
qed
lemma small_function_transformation:
assumes "small_rts A" and "small_rts B" and "transformation A B F G T"
shows "small_function T"
proof -
interpret A: small_rts A
using assms(1) by blast
interpret B: small_rts B
using assms(2) by blast
interpret T: transformation A B F G T
using assms(3) by blast
have 1: "range T ⊆ Collect B.arr ∪ {B.null}"
using T.extensional T.preserves_arr by blast
show ?thesis
proof (unfold small_function_def, intro conjI)
show "small (range T)"
using assms(2) 1 B.small smaller_than_small by blast
show "at_most_one_popular_value T"
proof -
have "⋀v. popular_value T v ⟹ v = B.null"
proof -
fix v
assume v: "popular_value T v"
have "v ≠ B.null ⟹ v ∈ range T"
using v
by (metis (mono_tags, lifting) empty_Collect_eq rangeI small_empty)
thus "v = B.null"
by (metis (mono_tags, lifting) A.small Collect_mono T.extensional
smaller_than_small v)
qed
thus ?thesis
using Uniq_def by blast
qed
qed
qed
text ‹
We can't simply use the previous fact to prove the following, because our
definition of transformation includes extensionality conditions that are
not part of the definition of simulation. So, we have to repeat the proof.
›
lemma small_function_simulation:
assumes "small_rts A" and "small_rts B" and "simulation A B F"
shows "small_function F"
proof -
interpret A: small_rts A
using assms(1) by blast
interpret B: small_rts B
using assms(2) by blast
interpret F: simulation A B F
using assms(3) by blast
have 1: "range F ⊆ Collect B.arr ∪ {B.null}"
using F.extensional F.preserves_reflects_arr by blast
show ?thesis
proof (unfold small_function_def, intro conjI)
show "small (range F)"
using assms(2) 1 B.small smaller_than_small by blast
show "at_most_one_popular_value F"
proof -
have "⋀v. popular_value F v ⟹ v = B.null"
proof -
fix v
assume v: "popular_value F v"
have "v ≠ B.null ⟹ v ∈ range F"
using v
by (metis (mono_tags, lifting) empty_Collect_eq rangeI small_empty)
thus "v = B.null"
by (metis (mono_tags, lifting) A.small Collect_mono F.extensional
smaller_than_small v)
qed
thus ?thesis
using Uniq_def by blast
qed
qed
qed
lemma small_function_resid:
fixes A :: "'a resid"
assumes "small_rts A"
shows "small_function A"
and "⋀t. small_function (A t)"
proof -
interpret A: small_rts A
using assms by blast
show 1: "small_function A"
proof (unfold small_function_def, intro conjI)
show "small (range A)"
proof -
have "range A ⊆ A ` Collect A.arr ∪ A ` {x. ¬ A.arr x}"
by blast
moreover have "small (A ` Collect A.arr)"
using A.small by blast
moreover have "small (A ` {x. ¬ A.arr x})"
proof -
have "⋀x. ¬ A.arr x ⟹ A x = (λx. A.null)"
using A.con_implies_arr(1) by blast
hence "A ` {x. ¬ A.arr x} ⊆ {λx. A.null}"
by blast
thus ?thesis
by (meson small_empty small_insert smaller_than_small)
qed
ultimately show ?thesis
by (meson small_Un smaller_than_small)
qed
show "at_most_one_popular_value A"
proof -
have "⋀v. popular_value A v ⟹ v ∈ A ` {x. ¬ A.arr x}"
proof -
fix v
assume v: "popular_value A v"
have "¬ small {x. ¬ A.arr x ∧ A x = v}"
proof -
have "¬ small ({x. A x = v} - {x. A.arr x ∧ A x = v})"
by (metis (mono_tags, lifting) A.small Collect_mono
Un_Diff_cancel small_Un smaller_than_small sup_ge2 v)
moreover have "{x. A x = v} - {x. A.arr x ∧ A x = v} =
{x. ¬ A.arr x ∧ A x = v}"
by blast
ultimately show ?thesis by metis
qed
hence "v ∈ A ` {x. ¬ A.arr x ∧ A x = v}"
by (metis (mono_tags, lifting) empty_Collect_eq image_eqI
mem_Collect_eq small_empty)
thus "v ∈ A ` {x. ¬ A.arr x}" by blast
qed
moreover have "A ` {x. ¬ A.arr x} ⊆ {λx. A.null}"
proof -
have "⋀x. ¬ A.arr x ⟹ A x = (λx. A.null)"
using A.con_implies_arr(1) by blast
thus ?thesis by blast
qed
ultimately show ?thesis
by (metis (no_types, lifting) Uniq_def empty_iff singletonD
subset_singleton_iff)
qed
qed
show 2: "⋀t. small_function (A t)"
proof -
fix t
show "small_function (A t)"
proof (unfold small_function_def, intro conjI)
show "small (range (A t))"
proof -
have "range (A t) ⊆ Collect A.arr ∪ {A.null}"
using A.arr_resid by blast
moreover have "small (Collect A.arr ∪ {A.null})"
using A.small by simp
ultimately show ?thesis
using smaller_than_small by blast
qed
show "at_most_one_popular_value (A t)"
proof -
have "⋀v. popular_value (A t) v ⟹ v = A.null"
proof -
fix v
assume v: "popular_value (A t) v"
have "¬ small {u. A t u = v}"
using v by blast
hence "¬ ({u. A t u = v} ⊆ Collect A.arr)"
using A.small smaller_than_small by blast
hence "∃u. A t u = v ∧ ¬ A.arr u"
by blast
thus "v = A.null"
using A.con_implies_arr(2) by blast
qed
thus ?thesis
using Uniq_def by blast
qed
qed
qed
qed
context exponentiation
begin
lemma small_function_some_inj_resid:
fixes A :: "'a resid"
assumes "small_rts A"
shows "small_function (λt. some_inj (A t))"
proof -
interpret A: small_rts A
using assms by blast
show "small_function (λt. some_inj (A t))"
proof (unfold small_function_def, intro conjI)
show "small (range (λt. some_inj (A t)))"
proof -
have "range (λt. some_inj (A t)) = some_inj ` range (λt. A t)"
by auto
moreover have "small ..."
using assms small_function_resid(1)
by (metis replacement small_function_def)
ultimately show ?thesis by auto
qed
show "at_most_one_popular_value (λt. some_inj (A t))"
proof -
have 3: "⋀t v. popular_value (λt. some_inj (A t)) v
⟹ v ∈ some_inj ` Collect (popular_value A)"
proof -
fix t v
assume v: "popular_value (λt. some_inj (A t)) v"
have "¬ small {t. A t = inv_into (Collect small_function) some_inj v}"
proof -
have 1: "⋀t. A.arr t ⟷ some_inj (A t) ≠ v"
proof
have 2: "⋀t. A.arr t ⟷ A t ≠ (λu. A.null)"
using A.con_implies_arr(1) by fastforce
have 3: "v = some_inj (λu. A.null)"
using v 2
by (metis (mono_tags, lifting) A.small Collect_mono
smaller_than_small)
show "⋀t. some_inj (A t) ≠ v ⟹ A.arr t"
using 2 3 by force
show "⋀t. A.arr t ⟹ some_inj (A t) ≠ v"
using assms 2 3 inj_some_inj app_some_inj small_function_resid(2)
by (metis A.not_arr_null)
qed
have "{t. A t = inv_into (Collect small_function) some_inj v} =
{t. ¬ A.arr t}"
using 1
by (metis (no_types, lifting) A.not_arr_null CollectD CollectI
app_some_inj assms f_inv_into_f image_eqI inv_into_into
small_function_resid(2))
thus ?thesis
using v 1 by auto
qed
hence "inv_into (Collect small_function) some_inj v
∈ Collect (popular_value A)"
by auto
moreover have "some_inj
(inv_into (Collect small_function) some_inj v) = v"
using assms v inj_some_inj
f_inv_into_f [of v some_inj "Collect small_function"]
by (metis (mono_tags) small_function_resid(2) empty_Collect_eq
inv_into_f_f mem_Collect_eq small_empty)
ultimately show "v ∈ some_inj ` Collect (popular_value A)"
by force
qed
show ?thesis
proof
fix u v
assume u: "popular_value (λx. some_inj (A x)) u"
assume v: "popular_value (λx. some_inj (A x)) v"
obtain f where f: "popular_value A f ∧ some_inj f = u"
using u 3 by blast
obtain g where g: "popular_value A g ∧ some_inj g = v"
using v 3 by blast
have "f = g"
using assms f g small_function_resid(1) Uniq_D
unfolding small_function_def
by auto fastforce
thus "u = v"
using f g by blast
qed
qed
qed
qed
fun some_inj_resid :: "'a resid ⇒ 'a"
where "some_inj_resid A = (some_inj (λt. some_inj (A t)))"
lemma inj_on_some_inj_resid:
shows "inj_on some_inj_resid {A :: 'a resid. small_rts A}"
proof
fix A B :: "'a resid"
assume A: "A ∈ {A. small_rts A}" and B: "B ∈ {B. small_rts B}"
assume eq: "some_inj_resid A = some_inj_resid B"
interpret A: small_rts A
using A by blast
interpret B: small_rts B
using B by blast
show "A = B"
proof -
have "some_inj (λt. some_inj (A t)) = some_inj (λt. some_inj (B t))"
using A B eq by simp
moreover have "small_function (λt. some_inj (A t))"
using A small_function_some_inj_resid by auto
moreover have "small_function (λt. some_inj (B t))"
using B small_function_some_inj_resid by auto
ultimately have "(λt. some_inj (A t)) = (λt. some_inj (B t))"
using A B inj_some_inj
by (simp add: inj_onD)
hence "⋀t. A t = B t"
using A B inj_some_inj small_function_resid(2)
by (metis app_some_inj mem_Collect_eq)
thus "A = B" by blast
qed
qed
end
section "Injective Images of RTS's"
text‹
Here we show that the image of an RTS ‹A› at type @{typ 'a}, under a function from @{typ 'a}
to @{typ 'b} that is injective on the set of arrows, is an RTS at type @{typ 'b} that is
isomorphic to ‹A›. We will use this, together with the universe assumptions, to obtain
isomorphic images, of constructions such as product and exponential RTS, that yield results
that ``live'' at the same type as their arguments.
›
locale inj_image_rts =
A: rts A
for map :: "'a ⇒ 'b"
and A :: "'a resid" (infix "\\⇩A" 70) +
assumes inj_map: "inj_on map (Collect A.arr ∪ {A.null})"
begin
notation A.con (infix "⌢⇩A" 50)
notation A.prfx (infix "≲⇩A" 50)
notation A.cong (infix "∼⇩A" 50)
abbreviation Null
where "Null ≡ map A.null"
abbreviation Arr
where "Arr t ≡ t ∈ map ` Collect A.arr"
abbreviation map'
where "map' t ≡ inv_into (Collect A.arr) map t"
definition resid :: "'b resid" (infix "\\" 70)
where "t \\ u = (if Arr t ∧ Arr u then map (map' t \\⇩A map' u) else Null)"
lemma inj_map':
shows "inj_on map (Collect A.arr)"
using inj_map by auto
lemma map_null:
shows "map A.null ∉ map ` Collect A.arr"
using inj_map by simp
lemma map'_map [simp]:
assumes "A.arr t"
shows "map' (map t) = t"
using assms inj_map by simp
lemma map_map' [simp]:
assumes "Arr t"
shows "map (map' t) = t"
using assms f_inv_into_f by metis
sublocale ResiduatedTransitionSystem.partial_magma resid
by (metis ResiduatedTransitionSystem.partial_magma.intro map_null resid_def)
lemma null_char:
shows "null = Null"
by (metis map_null null_is_zero(2) resid_def)
sublocale residuation resid
proof
show "⋀t u. t \\ u ≠ null ⟹ u \\ t ≠ null"
unfolding resid_def null_char
by (metis A.arr_resid A.conI A.con_sym imageI map_null mem_Collect_eq)
show "⋀t u. t \\ u ≠ null ⟹ (t \\ u) \\ (t \\ u) ≠ null"
unfolding resid_def null_char inj_map
apply simp
by (metis CollectI A.arr_resid A.conI A.con_imp_arr_resid imageI
map'_map map_null)
show "⋀v t u. (v \\ t) \\ (u \\ t) ≠ null
⟹ (v \\ t) \\ (u \\ t) = (v \\ u) \\ (t \\ u)"
proof -
fix t u v
assume vt_ut: "(v \\ t) \\ (u \\ t) ≠ null"
have 1: "Arr t ∧ Arr u ∧ Arr v"
using vt_ut
by (metis map_null null_char resid_def)
have "(v \\ t) \\ (u \\ t) = map ((map' v \\⇩A map' t) \\⇩A (map' u \\⇩A map' t))"
using 1 null_char resid_def vt_ut
apply auto[1]
by (metis A.arr_resid A.conI map'_map map_null vt_ut)
also have
"... = map ((map' v \\⇩A map' u) \\⇩A (map' t \\⇩A map' u))"
using A.cube by simp
also have "... = (v \\ u) \\ (t \\ u)"
using 1 null_char resid_def
apply auto[1]
apply (metis CollectI A.conI image_eqI map'_map map_null A.arr_resid)
apply (metis A.conI A.con_implies_arr(1) image_eqI mem_Collect_eq)
by (metis CollectI A.conI A.con_implies_arr(2) image_eqI)
finally show "(v \\ t) \\ (u \\ t) = (v \\ u) \\ (t \\ u)"
by blast
qed
qed
notation con (infix "⌢" 50)
lemma con_char:
shows "t ⌢ u ⟷ Arr t ∧ Arr u ∧ map' t ⌢⇩A map' u"
using null_char con_def inj_map resid_def A.con_def
by (metis (full_types) image_eqI map_null mem_Collect_eq A.arr_resid)
lemma arr_char:
shows "arr t ⟷ Arr t"
using arr_def con_char inj_map by auto
lemma ide_char⇩I⇩I:
shows "ide t ⟷ Arr t ∧ A.ide (map' t)"
unfolding ide_def resid_def con_char
using inj_map' f_inv_into_f
by (metis A.ide_def inv_into_f_f mem_Collect_eq A.arr_resid)
lemma trg_char:
shows "trg t = (if Arr t then map (A.trg (map' t)) else null)"
unfolding trg_def resid_def A.trg_def null_char by simp
sublocale rts resid
proof
show "⋀t. arr t ⟹ ide (trg t)"
using ide_char⇩I⇩I inj_map trg_char trg_def by fastforce
show 1: "⋀a t. ⟦ide a; t ⌢ a⟧ ⟹ t \\ a = t"
by (simp add: A.resid_arr_ide con_char f_inv_into_f ide_char⇩I⇩I resid_def)
show "⋀a t. ⟦ide a; a ⌢ t⟧ ⟹ ide (a \\ t)"
by (metis 1 arrE arr_resid con_sym cube ideE ideI)
show "⋀t u. t ⌢ u ⟹ ∃a. ide a ∧ a ⌢ t ∧ a ⌢ u"
by (metis (full_types) CollectI A.con_imp_coinitial_ax ide_char⇩I⇩I
image_eqI inj_image_rts.con_char inj_image_rts_axioms map'_map
A.ide_implies_arr)
show "⋀t u v. ⟦ide (t \\ u); u ⌢ v⟧ ⟹ t \\ u ⌢ v \\ u"
proof -
fix t u v
assume ide: "ide (t \\ u)"
assume con: "u ⌢ v"
have "Arr t ∧ Arr u ∧ Arr v"
using ide con ide_char⇩I⇩I con_char
by (metis arr_resid_iff_con ide_implies_arr)
moreover have "A.arr (map' t \\⇩A map' u)"
using ide ide_char⇩I⇩I resid_def
by (meson A.arr_resid arr_resid_iff_con con_char ide_implies_arr)
moreover have "A.arr (map' v \\⇩A map' u)"
using con con_char
by (meson A.arr_resid A.con_sym)
ultimately show "t \\ u ⌢ v \\ u"
using ide con ide_char⇩I⇩I con_char resid_def A.con_target by simp
qed
qed
notation prfx (infix "≲" 50)
notation cong (infix "∼" 50)
text‹
The function @{term map} and its inverse (both suitably extensionalized) determine an
isomorphism between ‹A› and its image.
›
abbreviation map⇩e⇩x⇩t
where "map⇩e⇩x⇩t t ≡ if A.arr t then map t else null"
abbreviation map'⇩e⇩x⇩t
where "map'⇩e⇩x⇩t t ≡ if Arr t then map' t else A.null"
sublocale Map: simulation A resid map⇩e⇩x⇩t
using con_char A.con_implies_arr resid_def
by unfold_locales auto
sublocale Map': simulation resid A map'⇩e⇩x⇩t
using arr_char con_char resid_def
by unfold_locales auto
sublocale inverse_simulations resid A map⇩e⇩x⇩t map'⇩e⇩x⇩t
using arr_char map_null null_char
by unfold_locales auto
lemma invertible_simulation_map:
shows "invertible_simulation A resid map⇩e⇩x⇩t"
using inverse_simulations_axioms inverse_simulations_sym invertible_simulation_def'
by fast
lemma invertible_simulation_map':
shows "invertible_simulation resid A map'⇩e⇩x⇩t"
using inverse_simulations_axioms inverse_simulations_sym invertible_simulation_def'
by fast
lemma inj_on_map:
shows "inj_on map⇩e⇩x⇩t (Collect A.arr)"
using induce_bij_betw_arr_sets bij_betw_def by blast
lemma range_map':
shows "map'⇩e⇩x⇩t ` (Collect arr) = Collect A.arr"
by (metis (no_types, lifting) bij_betw_imp_surj_on
inverse_simulations.induce_bij_betw_arr_sets
inverse_simulations_axioms inverse_simulations_sym)
lemma cong_char⇩I⇩I:
shows "t ∼ u ⟷ Arr t ∧ Arr u ∧ map' t ∼⇩A map' u"
by (metis (full_types) Map'.preserves_resid Map.preserves_ide con_def
ide_char⇩I⇩I not_arr_null null_char resid_def residuation.ide_implies_arr
residuation_axioms)
lemma preserves_weakly_extensional_rts:
assumes "weakly_extensional_rts A"
shows "weakly_extensional_rts resid"
by (metis assms cong_char⇩I⇩I ide_char⇩I⇩I inv_into_injective rts_axioms
weakly_extensional_rts.intro weakly_extensional_rts.weak_extensionality
weakly_extensional_rts_axioms.intro)
lemma preserves_extensional_rts:
assumes "extensional_rts A"
shows "extensional_rts resid"
proof
interpret A: extensional_rts A
using assms by blast
show "⋀t u. t ∼ u ⟹ t = u"
using cong_char⇩I⇩I ide_char⇩I⇩I
by (meson A.extensional inv_into_injective)
qed
lemma preserves_reflects_small_rts:
shows "small_rts A ⟷ small_rts resid"
using induce_bij_betw_arr_sets
by (metis (no_types, lifting) A.rts_axioms bij_betw_def rts_axioms
small_image_iff small_rts.intro small_rts.small small_rts_axioms_def)
end
lemma inj_image_rts_comp:
fixes F :: "'a ⇒ 'b" and G :: "'b ⇒ 'c"
assumes "inj F" and "inj G"
assumes "rts X"
shows "inj_image_rts.resid (G ∘ F) X =
inj_image_rts.resid G (inj_image_rts.resid F X)"
proof -
interpret X: rts X
using assms(3) by blast
interpret FX: inj_image_rts F X
by (metis X.rts_axioms assms(1)
inj_image_rts_axioms_def inj_image_rts_def inj_on_subset top_greatest)
interpret GFX: inj_image_rts G FX.resid
by (metis (mono_tags, lifting) FX.rts_axioms assms(2) inj_def
inj_image_rts_axioms_def inj_image_rts_def inj_onI)
interpret GoF_X: inj_image_rts ‹G o F› X
by (metis (no_types, opaque_lifting) X.rts_axioms
assms(1-2) inj_compose inj_image_rts_axioms_def
inj_image_rts_def inj_on_subset top_greatest)
show "GoF_X.resid = GFX.resid"
proof -
have "⋀t u. GoF_X.resid t u = GFX.resid t u"
unfolding GoF_X.resid_def GFX.resid_def
using FX.arr_char FX.null_char FX.resid_def GoF_X.map'_map by auto
thus ?thesis by blast
qed
qed
lemma inj_image_rts_map_comp:
fixes F :: "'a ⇒ 'b" and G :: "'b ⇒ 'c"
assumes "inj F" and "inj G"
assumes "rts X"
shows "inj_image_rts.map⇩e⇩x⇩t (G ∘ F) X =
inj_image_rts.map⇩e⇩x⇩t G (inj_image_rts.resid F X) ∘
(inj_image_rts.map⇩e⇩x⇩t F X)"
and "inj_image_rts.map'⇩e⇩x⇩t (G ∘ F) X =
inj_image_rts.map'⇩e⇩x⇩t F X ∘
inj_image_rts.map'⇩e⇩x⇩t G (inj_image_rts.resid F X)"
proof -
interpret X: rts X
using assms(3) by blast
interpret FX: inj_image_rts F X
by (metis X.rts_axioms assms(1) inj_image_rts_axioms_def inj_image_rts_def
inj_on_subset top_greatest)
interpret GFX: inj_image_rts G FX.resid
by (metis FX.rts_axioms Int_UNIV_right assms(2) inj_image_rts.intro
inj_image_rts_axioms.intro inj_on_Int)
interpret GoF_X: inj_image_rts ‹G o F› X
by (metis (no_types, opaque_lifting) X.rts_axioms assms(1-2) inj_compose
inj_image_rts_axioms_def inj_image_rts_def inj_on_subset top_greatest)
show "GoF_X.map⇩e⇩x⇩t = GFX.map⇩e⇩x⇩t ∘ FX.map⇩e⇩x⇩t"
using FX.null_char GFX.null_char GoF_X.null_char by fastforce
show "GoF_X.map'⇩e⇩x⇩t = FX.map'⇩e⇩x⇩t ∘ GFX.map'⇩e⇩x⇩t"
using FX.arr_char FX.not_arr_null GoF_X.map'_map by fastforce
qed
section "Empty RTS"
text‹
For any type, there exists an empty RTS having that type as its arrow type.
Since types in HOL are nonempty, we may use the guaranteed element @{term undefined}
as the null value.
›
locale empty_rts
begin
definition resid :: "'e resid"
where "resid t u = undefined"
sublocale ResiduatedTransitionSystem.partial_magma resid
by unfold_locales (metis resid_def)
lemma null_char:
shows "null = undefined"
by (metis null_is_zero(1) resid_def)
sublocale residuation resid
apply unfold_locales
by (metis resid_def)+
lemma arr_char:
shows "arr t ⟷ False"
using null_char resid_def
by (metis arrE conE)
lemma ide_char⇩E⇩R⇩T⇩S:
shows "ide t ⟷ False"
using arr_char by force
lemma con_char:
shows "con t u ⟷ False"
by (simp add: con_def null_char resid_def)
lemma trg_char:
shows "trg t = null"
by (simp add: null_char resid_def trg_def)
sublocale rts resid
apply unfold_locales
apply (metis arr_char)
by (metis con_char)+
lemma cong_char⇩E⇩R⇩T⇩S:
shows "cong t u ⟷ False"
by (simp add: ide_char⇩E⇩R⇩T⇩S)
sublocale small_rts resid
apply unfold_locales
by (metis Collect_empty_eq arr_char small_empty)
lemma is_small_rts:
shows "small_rts resid"
..
sublocale extensional_rts resid
by unfold_locales (simp add: cong_char⇩E⇩R⇩T⇩S)
lemma is_extensional_rts:
shows "extensional_rts resid"
..
lemma src_char:
shows "src t = null"
by (simp add: arr_char src_def)
lemma prfx_char:
shows "prfx t u ⟷ False"
using ide_char⇩E⇩R⇩T⇩S by metis
lemma composite_of_char:
shows "composite_of t u v ⟷ False"
using composite_of_def prfx_char by metis
lemma composable_char:
shows "composable t u ⟷ False"
using composable_def composite_of_char by metis
lemma seq_char:
shows "seq t u ⟷ False"
using arr_char by (metis seqE)
sublocale rts_with_composites resid
by unfold_locales (simp add: composable_char seq_char)
lemma is_rts_with_composites:
shows "rts_with_composites resid"
..
sublocale extensional_rts_with_composites resid ..
lemma is_extensional_rts_with_composites:
shows "extensional_rts_with_composites resid"
..
lemma comp_char:
shows "comp t u = null"
by (meson composable_char composable_iff_comp_not_null)
text‹
There is a unique simulation from an empty RTS to any other RTS.
›
definition initiator :: "'e resid ⇒ 'a ⇒ 'e"
where "initiator A ≡ (λt. ResiduatedTransitionSystem.partial_magma.null A)"
lemma initiator_is_simulation:
assumes "rts A"
shows "simulation resid A (initiator A)"
using assms initiator_def con_char
by (metis rts_axioms simulation_axioms.intro simulation_def)
lemma universality:
assumes "rts A"
shows "∃!F. simulation resid A F"
proof
show "simulation resid A (initiator A)"
using assms initiator_is_simulation by blast
show "⋀F. simulation resid A F ⟹ F = initiator A"
by (metis HOL.ext initiator_def arr_char simulation.extensional)
qed
end
section "One-Transition RTS"
text‹
For any type having at least two elements, there exists a one-transition RTS
having that type as its arrow type. We use the already-distinguished element
@{term undefined} as the null value and some value distinct from @{term undefined}
as the single transition.
›
locale one_arr_rts =
nondegenerate arr_type
for arr_type :: "'t itself"
begin
definition the_arr :: 't
where "the_arr ≡ SOME t. t ≠ undefined"
definition resid :: "'t resid" (infix "\\⇩1" 70)
where "resid t u = (if t = the_arr ∧ u = the_arr then the_arr else undefined)"
sublocale ResiduatedTransitionSystem.partial_magma resid
using resid_def
by unfold_locales metis
lemma null_char:
shows "null = undefined"
by (metis null_is_zero(1) resid_def)
sublocale residuation resid
using null_char resid_def
by unfold_locales metis+
notation con (infix "⌢⇩1" 50)
lemma arr_char:
shows "arr t ⟷ t = the_arr"
using null_char resid_def is_nondegenerate
by (metis (mono_tags, lifting) arr_def con_def someI_ex the_arr_def)
lemma ide_char⇩1⇩R⇩T⇩S:
shows "ide t ⟷ t = the_arr"
using arr_char ide_def resid_def by auto
lemma con_char:
shows "con t u ⟷ arr t ∧ arr u"
by (metis arr_char con_arr_self con_implies_arr(2) con_sym)
lemma trg_char:
shows "trg t = (if arr t then t else null)"
by (simp add: arr_char null_char resid_def trg_def)
sublocale rts resid
using con_char arr_char ide_char⇩1⇩R⇩T⇩S trg_char ideE
by unfold_locales metis+
notation prfx (infix "≲⇩1" 50)
notation cong (infix "∼⇩1" 50)
lemma cong_char⇩1⇩R⇩T⇩S:
shows "t ≲⇩1 u ⟷ arr t ∧ arr u"
using arr_char ide_char⇩1⇩R⇩T⇩S not_ide_null null_char resid_def by force
sublocale extensional_rts resid
using arr_char cong_char⇩1⇩R⇩T⇩S
by unfold_locales auto
lemma is_extensional_rts:
shows "extensional_rts resid"
..
lemma src_char:
shows "src t = (if t = the_arr then t else null)"
using arr_char ide_char⇩1⇩R⇩T⇩S src_def src_ide by presburger
lemma prfx_char:
shows "t ≲⇩1 u ⟷ arr t ∧ arr u"
by (metis cong_char⇩1⇩R⇩T⇩S)
lemma composite_of_char:
shows "composite_of t u v ⟷ arr t ∧ arr u ∧ arr v"
using composite_of_def
by (metis composite_of_ide_self prfx_char)
lemma composable_char:
shows "composable t u ⟷ arr t ∧ arr u"
using composable_def composite_of_char by auto
lemma seq_char:
shows "seq t u ⟷ arr t ∧ arr u"
using arr_char composable_char composable_imp_seq by auto
sublocale rts_with_composites resid
by unfold_locales (simp add: composable_char seq_char)
lemma is_rts_with_composites:
shows "rts_with_composites resid"
..
sublocale extensional_rts_with_composites resid ..
lemma is_extensional_rts_with_composites:
shows "extensional_rts_with_composites resid"
..
sublocale small_rts resid
by (simp add: Collect_cong arr_char rts_axioms small_rts.intro
small_rts_axioms.intro)
lemma is_small_rts:
shows "small_rts resid"
..
lemma comp_char:
shows "comp t u = (if arr t ∧ arr u then the_arr else null)"
using arr_char composable_iff_comp_not_null trg_char by auto
text‹
For an arbitrary RTS ‹A›, there is a unique simulation from ‹A› to the one-transition RTS.
›
definition terminator :: "'a resid ⇒ 'a ⇒ 't"
where "terminator A ≡ (λt. if residuation.arr A t then the_arr else null)"
lemma terminator_is_simulation:
assumes "rts A"
shows "simulation A resid (terminator A)"
proof -
interpret A: rts A
using assms by blast
show ?thesis
unfolding terminator_def
using assms ide_char⇩1⇩R⇩T⇩S ideE A.con_implies_arr
apply (unfold_locales)
by auto metis
qed
lemma universality:
assumes "rts A"
shows "∃!F. simulation A resid F"
proof
show "simulation A resid (terminator A)"
using assms terminator_is_simulation by blast
show "⋀F. simulation A resid F ⟹ F = terminator A"
unfolding terminator_def
by (meson arr_char simulation.extensional
simulation.preserves_reflects_arr)
qed
text‹
A ``global transition'' of an RTS ‹A› is a transformation from the one-arrow RTS
to ‹A›. An important fact is that equality of simulations and of transformations
is determined by their compositions with global transitions.
›
lemma eq_simulation_iff:
assumes "weakly_extensional_rts A"
and "simulation A B F" and "simulation A B G"
shows "F = G ⟷
(∀Q R T. transformation resid A Q R T ⟶ F ∘ T = G ∘ T)"
proof
interpret A: weakly_extensional_rts A
using assms(1) simulation_def by blast
interpret F: simulation A B F
using assms(2) by blast
interpret G: simulation A B G
using assms(3) by blast
show "F = G ⟹
∀Q R T. transformation resid A Q R T ⟶ F ∘ T = G ∘ T"
by blast
show "∀Q R T. transformation resid A Q R T ⟶ F ∘ T = G ∘ T
⟹ F = G"
proof -
have "F ≠ G ⟹
(∃Q R T. transformation resid A Q R T ∧ F ∘ T ≠ G ∘ T)"
proof -
assume 1: "F ≠ G"
obtain t where t: "A.arr t ∧ F t ≠ G t"
using 1 F.extensional G.extensional by fastforce
interpret T: constant_transformation resid A t
using t by unfold_locales blast
have "transformation resid A T.F T.G T.map"
using T.transformation_axioms by simp
moreover have "F ∘ T.map ≠ G ∘ T.map"
by (metis (mono_tags, lifting) arr_char comp_apply t)
ultimately show "∃Q R T. transformation resid A Q R T ∧
F ∘ T ≠ G ∘ T"
by blast
qed
thus "∀Q R T. transformation resid A Q R T ⟶ F ∘ T = G ∘ T
⟹ F = G"
by blast
qed
qed
lemma eq_transformation_iff:
assumes "weakly_extensional_rts A" and "weakly_extensional_rts B"
and "transformation A B F G U" and "transformation A B F G V"
shows "U = V ⟷
(∀Q R T. transformation resid A Q R T ⟶ U ∘ T = V ∘ T)"
proof
interpret A: weakly_extensional_rts A
using assms(1) simulation_def by blast
interpret B: weakly_extensional_rts B
using assms(2) simulation_def by blast
interpret U: transformation A B F G U
using assms(3) by blast
interpret V: transformation A B F G V
using assms(4) by blast
show "U = V ⟹
∀Q R T. transformation resid A Q R T ⟶ U ∘ T = V ∘ T"
by blast
show "∀Q R T. transformation resid A Q R T ⟶ U ∘ T = V ∘ T
⟹ U = V"
proof -
have "U ≠ V ⟹
(∃Q R T. transformation resid A Q R T ∧ U ∘ T ≠ V ∘ T)"
proof -
assume 1: "U ≠ V"
obtain t where t: "A.arr t ∧ U t ≠ V t"
using 1 U.extensional V.extensional by fastforce
interpret T: constant_transformation resid A t
using t by unfold_locales blast
have "transformation resid A T.F T.G T.map"
using T.transformation_axioms by simp
moreover have "U ∘ T.map ≠ V ∘ T.map"
by (metis (mono_tags, lifting) arr_char comp_apply t)
ultimately show "∃Q R T. transformation resid A Q R T ∧
U ∘ T ≠ V ∘ T"
by blast
qed
thus "∀Q R T. transformation resid A Q R T ⟶ U ∘ T = V ∘ T
⟹ U = V"
by blast
qed
qed
end
section "Sub-RTS"
text‹
A sub-RTS of an RTS ‹R› may be determined by specifying a subset of the transitions
of ‹R› that is closed under residuation and in addition includes some common source
for every consistent pair of transitions contained in it.
›
locale sub_rts =
R: rts R
for R :: "'a resid" (infix "\\⇩R" 70)
and Arr :: "'a ⇒ bool" +
assumes inclusion: "Arr t ⟹ R.arr t"
and resid_closed: "⟦Arr t; Arr u; R.con t u⟧ ⟹ Arr (t \\⇩R u)"
and enough_sources: "⟦Arr t; Arr u; R.con t u⟧ ⟹
∃a. Arr a ∧ a ∈ R.sources t ∧ a ∈ R.sources u"
begin
definition resid :: "'a resid" (infix "\\" 70)
where "resid t u ≡ if Arr t ∧ Arr u ∧ R.con t u then t \\⇩R u else R.null"
sublocale ResiduatedTransitionSystem.partial_magma resid
using R.not_con_null(2) R.null_is_zero(1) resid_def
by unfold_locales metis
lemma null_char:
shows "null = R.null"
by (metis R.not_arr_null inclusion null_eqI resid_def)
sublocale residuation resid
using R.conE R.con_sym R.not_con_null(1) null_is_zero(1) resid_def
apply unfold_locales
apply metis
apply (metis R.con_def R.con_imp_arr_resid resid_closed)
by (metis (no_types, lifting) R.con_def R.cube resid_closed)
lemma arr_char:
shows "arr t ⟷ Arr t"
by (metis R.con_arr_self R.con_def R.not_arr_null arrE con_def inclusion
null_is_zero(2) resid_def residuation.con_implies_arr(1) residuation_axioms)
lemma ide_char:
shows "ide t ⟷ Arr t ∧ R.ide t"
by (metis R.ide_def arrI arr_char con_def ide_def not_arr_null resid_def)
lemma con_char:
shows "con t u ⟷ Arr t ∧ Arr u ∧ R.con t u"
by (metis R.conE arr_char con_def not_arr_null null_is_zero(1) resid_def)
lemma trg_char:
shows "trg = (λt. if arr t then R.trg t else null)"
using arr_char trg_def R.trg_def resid_def by fastforce
sublocale rts resid
using arr_char ide_char con_char trg_char resid_def resid_closed inclusion
apply unfold_locales
using R.prfx_reflexive trg_def apply force
apply (simp add: R.resid_arr_ide)
apply simp
apply (meson R.con_sym R.in_sourcesE enough_sources)
by (metis (no_types, lifting) R.con_target arr_resid_iff_con con_sym_ax null_char)
lemma prfx_char:
shows "prfx t u ⟷ Arr t ∧ Arr u ∧ R.prfx t u"
using arr_char con_char ide_char
by (metis R.prfx_implies_con prfx_implies_con resid_closed resid_def)
lemma cong_char:
shows "cong t u ⟷ Arr t ∧ Arr u ∧ R.cong t u"
using prfx_char by blast
lemma composite_of_char:
shows "composite_of t u v ⟷ Arr t ∧ Arr u ∧ Arr v ∧ R.composite_of t u v"
proof
show "composite_of t u v ⟹ Arr t ∧ Arr u ∧ Arr v ∧ R.composite_of t u v"
by (metis RTSConstructions.sub_rts.resid_def R.composite_of_def
R.con_sym composite_ofE con_char prfx_char prfx_implies_con sub_rts_axioms)
show "Arr t ∧ Arr u ∧ Arr v ∧ R.composite_of t u v ⟹ composite_of t u v"
by (metis (full_types) RTSConstructions.sub_rts.resid_def R.composite_of_def
R.con_sym R.rts_axioms composite_ofI prfx_char resid_closed
rts.prfx_implies_con sub_rts_axioms)
qed
lemma join_of_char:
shows "join_of t u v ⟷ Arr t ∧ Arr u ∧ Arr v ∧ R.join_of t u v"
using composite_of_char
by (metis R.bounded_imp_con R.join_of_def join_of_def resid_closed resid_def)
lemma preserves_weakly_extensional_rts:
assumes "weakly_extensional_rts R"
shows "weakly_extensional_rts resid"
by (metis assms cong_char ide_char rts_axioms weakly_extensional_rts.intro
weakly_extensional_rts.weak_extensionality weakly_extensional_rts_axioms.intro)
lemma preserves_extensional_rts:
assumes "extensional_rts R"
shows "extensional_rts resid"
by (meson assms extensional_rts.cong_char extensional_rts.intro
extensional_rts_axioms.intro prfx_char rts_axioms)
end
locale sub_rts_of_weakly_extensional_rts =
R: weakly_extensional_rts R +
sub_rts R Arr
for R :: "'a resid" (infix "\\⇩R" 70)
and Arr :: "'a ⇒ bool"
begin
sublocale weakly_extensional_rts resid
using R.weakly_extensional_rts_axioms preserves_weakly_extensional_rts
by blast
lemma src_char:
shows "src = (λt. if arr t then R.src t else null)"
proof
fix t
show "src t = (if arr t then R.src t else null)"
by (metis R.src_eqI con_arr_src(2) con_char ide_char ide_src src_def)
qed
lemma targets_char:
assumes "arr t"
shows "targets t = {R.trg t}"
using assms trg_char trg_in_targets arr_has_un_target by auto
end
locale sub_rts_of_extensional_rts =
R: extensional_rts R +
sub_rts R Arr
for R :: "'a resid" (infix "\\⇩R" 70)
and Arr :: "'a ⇒ bool"
begin
sublocale sub_rts_of_weakly_extensional_rts ..
sublocale extensional_rts resid
using R.extensional_rts_axioms preserves_extensional_rts
by blast
end
section "Fibered Product RTS"
locale fibered_product_rts =
A: rts A +
B: rts B +
C: weakly_extensional_rts C +
F: simulation A C F +
G: simulation B C G
for A :: "'a resid" (infix "\\⇩A" 70)
and B :: "'b resid" (infix "\\⇩B" 70)
and C :: "'c resid" (infix "\\⇩C" 70)
and F :: "'a ⇒ 'c"
and G :: "'b ⇒ 'c"
begin
notation A.con (infix "⌢⇩A" 50)
notation B.con (infix "⌢⇩B" 50)
notation C.con (infix "⌢⇩C" 50)
notation A.prfx (infix "≲⇩A" 50)
notation B.prfx (infix "≲⇩B" 50)
notation C.prfx (infix "≲⇩C" 50)
notation A.cong (infix "∼⇩A" 50)
notation B.cong (infix "∼⇩B" 50)
notation C.cong (infix "∼⇩C" 50)
abbreviation Arr
where "Arr ≡ λtu. A.arr (fst tu) ∧ B.arr (snd tu) ∧ F (fst tu) = G (snd tu)"
abbreviation Ide
where "Ide ≡ λtu. A.ide (fst tu) ∧ B.ide (snd tu) ∧ F (fst tu) = G (snd tu)"
abbreviation Con
where "Con ≡ λtu vw. fst tu ⌢⇩A fst vw ∧ snd tu ⌢⇩B snd vw ∧
F (fst tu) = G (snd tu) ∧ F (fst vw) = G (snd vw)"
definition resid :: "('a * 'b) resid" (infix "\\" 70)
where "tu \\ vw =
(if Con tu vw then (fst tu \\⇩A fst vw, snd tu \\⇩B snd vw)
else (A.null, B.null))"
sublocale ResiduatedTransitionSystem.partial_magma resid
using resid_def
by unfold_locales
(metis B.arr_resid_iff_con B.ex_un_null B.not_arr_null
B.null_is_zero(2) snd_conv)
lemma null_char:
shows "null = (A.null, B.null)"
unfolding null_def
using ex_un_null resid_def
the1_equality [of "λn. ∀f. n \\ f = n ∧ f \\ n = n" "(A.null, B.null)"]
by simp
sublocale residuation resid
proof
show "⋀t u. t \\ u ≠ null ⟹ u \\ t ≠ null"
by (metis A.con_sym B.con_sym B.residuation_axioms null_char prod.inject
resid_def residuation.con_def)
show "⋀t u. t \\ u ≠ null ⟹ (t \\ u) \\ (t \\ u) ≠ null"
by (metis (no_types, lifting) A.conE A.conI A.con_imp_arr_resid B.con_def
B.con_imp_arr_resid F.preserves_resid G.preserves_resid fst_conv null_char
resid_def snd_conv)
show "⋀v t u. (v \\ t) \\ (u \\ t) ≠ null ⟹ (v \\ t) \\ (u \\ t) = (v \\ u) \\ (t \\ u)"
proof -
fix v t u
assume 1: "(v \\ t) \\ (u \\ t) ≠ null"
have 2: "(v \\ t) \\ (u \\ t) =
((fst v \\⇩A fst t) \\⇩A (fst u \\⇩A fst t),
(snd v \\⇩B snd t) \\⇩B (snd u \\⇩B snd t))"
using 1 resid_def null_char by auto
also have "... = ((fst v \\⇩A fst u) \\⇩A (fst t \\⇩A fst u),
(snd v \\⇩B snd u) \\⇩B (snd t \\⇩B snd u))"
using A.cube B.cube by simp
also have "... = (v \\ u) \\ (t \\ u)"
proof -
have "Con (v \\ u) (t \\ u)"
proof -
have "fst v \\⇩A fst u ⌢⇩A fst t \\⇩A fst u"
using 1 2 A.cube
by (metis (no_types, lifting) A.con_def fst_conv null_char resid_def)
moreover have "snd v \\⇩B snd u ⌢⇩B snd t \\⇩B snd u"
using 1 2 B.cube
by (metis (no_types, lifting) B.con_def null_char resid_def snd_conv)
ultimately show ?thesis
using 1 resid_def
by (metis (no_types, lifting) A.conI A.con_implies_arr(1) A.not_arr_null
A.not_con_null(2) B.conI B.con_implies_arr(1) B.not_arr_null
B.not_con_null(2) F.preserves_resid G.preserves_resid fst_eqD
null_char snd_eqD)
qed
thus ?thesis
using resid_def null_char by auto
qed
finally show "(v \\ t) \\ (u \\ t) = (v \\ u) \\ (t \\ u)"
by blast
qed
qed
notation con (infix "⌢" 50)
lemma arr_char:
shows "arr t ⟷ Arr t"
by (metis B.arr_def B.conE Pair_inject conE conI null_char resid_def
A.arr_def arr_def)
lemma con_char:
shows "t ⌢ u ⟷ Con t u"
by (metis B.conE null_char resid_def con_def snd_conv)
lemma ide_char⇩F⇩P:
shows "ide t ⟷ Ide t"
unfolding ide_def
using con_char resid_def
by (metis (no_types, lifting) A.ide_def fst_conv prod.exhaust_sel
B.ide_def snd_conv)
lemma trg_char:
shows "trg t = (if arr t then (A.trg (fst t), B.trg (snd t)) else null)"
by (simp add: A.trg_def B.trg_def con_char null_char resid_def
arr_def trg_def)
sublocale rts resid
proof
show "⋀t. arr t ⟹ ide (trg t)"
using trg_char ide_char⇩F⇩P arr_char F.preserves_trg G.preserves_trg
apply simp
using F.preserves_trg G.preserves_trg by metis
show 1: "⋀a t. ⟦ide a; t ⌢ a⟧ ⟹ t \\ a = t"
by (simp add: A.resid_arr_ide B.resid_arr_ide con_char ide_char⇩F⇩P
resid_def)
show "⋀a t. ⟦ide a; a ⌢ t⟧ ⟹ ide (a \\ t)"
by (metis 1 arr_resid_iff_con con_sym cube ide_def)
show "⋀t u. t ⌢ u ⟹ ∃a. ide a ∧ a ⌢ t ∧ a ⌢ u"
proof -
fix t u
assume con: "t ⌢ u"
obtain a where a: "A.ide a ∧ a ⌢⇩A fst t ∧ a ⌢⇩A fst u"
using con con_char A.con_imp_coinitial_ax by fastforce
obtain b where b: "B.ide b ∧ b ⌢⇩B snd t ∧ b ⌢⇩B snd u"
using con con_char B.con_imp_coinitial_ax by fastforce
have "F a = G b"
by (metis C.src_eqI F.preserves_con F.preserves_ide G.preserves_con
G.preserves_ide a b con con_char)
thus "∃a. ide a ∧ a ⌢ t ∧ a ⌢ u"
using a b ide_char⇩F⇩P con con_char by auto
qed
show "⋀t u v. ⟦ide (t \\ u); u ⌢ v⟧ ⟹ t \\ u ⌢ v \\ u"
by (metis (no_types, lifting) A.con_target B.con_target arr_char
arr_resid_iff_con con_char con_sym fst_conv ide_char⇩F⇩P
ide_implies_arr resid_def snd_conv)
qed
notation prfx (infix "≲" 50)
notation cong (infix "∼" 50)
lemma prfx_char:
shows "t ≲ u ⟷ F (fst t) = G (snd t) ∧ F (fst u) = G (snd u) ∧
fst t ≲⇩A fst u ∧ snd t ≲⇩B snd u"
using A.prfx_implies_con B.prfx_implies_con ide_char⇩F⇩P resid_def
by auto
lemma cong_char⇩F⇩P:
shows "t ∼ u ⟷ F (fst t) = G (snd t) ∧ F (fst u) = G (snd u) ∧
fst t ∼⇩A fst u ∧ snd t ∼⇩B snd u"
using prfx_char by auto
lemma sources_char:
shows "sources t =
{a. F (fst t) = G (snd t) ∧ F (fst a) = G (snd a) ∧
fst a ∈ A.sources (fst t) ∧ snd a ∈ B.sources (snd t)}"
using con_char ide_char⇩F⇩P sources_def by auto
lemma targets_char⇩F⇩P:
shows "targets t =
{a. F (fst t) = G (snd t) ∧ F (fst a) = G (snd a) ∧
fst a ∈ A.targets (fst t) ∧ snd a ∈ B.targets (snd t)}"
proof
show "targets t ⊆ {a. F (fst t) = G (snd t) ∧ F (fst a) = G (snd a) ∧
fst a ∈ A.targets (fst t) ∧ snd a ∈ B.targets (snd t)}"
using arr_char arr_iff_has_target ide_char⇩F⇩P
apply auto[1]
apply (metis arr_char arr_composite_of composite_of_arr_ide in_targetsE
trg_def)
apply (metis A.in_targetsI con_char con_implies_arr(1) fst_conv
in_targetsE not_arr_null trg_char)
by (metis B.in_targetsI con_char con_implies_arr(1) in_targetsE
not_arr_null snd_conv trg_char)
show "{a. F (fst t) = G (snd t) ∧ F (fst a) = G (snd a) ∧
fst a ∈ A.targets (fst t) ∧ snd a ∈ B.targets (snd t)} ⊆ targets t"
using A.arr_iff_has_target B.arr_iff_has_target arr_char con_char
ide_char⇩F⇩P ide_trg targets_def trg_char
by auto
qed
definition P⇩0 :: "'a × 'b ⇒ 'b"
where "P⇩0 t ≡ if arr t then snd t else B.null"
definition P⇩1 :: "'a × 'b ⇒ 'a"
where "P⇩1 t ≡ if arr t then fst t else A.null"
sublocale P⇩0: simulation resid B P⇩0
using P⇩0_def con_char resid_def arr_resid con_implies_arr(1-2)
by unfold_locales auto
lemma P⇩0_is_simulation:
shows "simulation resid B P⇩0"
..
sublocale P⇩1: simulation resid A P⇩1
using P⇩1_def con_char resid_def arr_resid con_implies_arr(1-2)
by unfold_locales auto
lemma P⇩1_is_simulation:
shows "simulation resid A P⇩1"
..
lemma commutativity:
shows "F o P⇩1 = G o P⇩0"
using F.extensional G.extensional P⇩1_def P⇩0_def arr_char by auto
definition tuple :: "'x resid ⇒ ('x ⇒ 'a) ⇒ ('x ⇒ 'b) ⇒ 'x ⇒ 'a × 'b"
where "tuple X H K ≡ λt. if residuation.arr X t then (H t, K t) else null"
lemma universality:
assumes "rts X" and "simulation X A H" and "simulation X B K"
and "F o H = G o K"
shows [intro]: "simulation X resid (tuple X H K)"
and "P⇩1 ∘ tuple X H K = H" and "P⇩0 ∘ tuple X H K = K"
and "∃!HK. simulation X resid HK ∧ P⇩1 o HK = H ∧ P⇩0 o HK = K"
proof -
interpret X: rts X
using assms(1) by blast
interpret H: simulation X A H
using assms(2) by blast
interpret K: simulation X B K
using assms(3) by blast
let ?HK = "tuple X H K"
interpret HK: simulation X resid ?HK
proof
show "⋀t. ¬ X.arr t ⟹ ?HK t = null"
unfolding tuple_def by simp
fix t u
assume con: "X.con t u"
have 1: "X.arr t ∧ X.arr u"
using con X.con_implies_arr(1) X.con_implies_arr(2) by force
show 2: "con (?HK t) (?HK u)"
by (metis 1 assms(4) comp_apply con con_char fst_conv tuple_def
H.preserves_con K.preserves_con snd_conv)
show "?HK (X t u) = resid (?HK t) (?HK u)"
using 1 2 con resid_def null_char con_char arr_char
by (simp add: tuple_def)
qed
show "simulation X resid (tuple X H K)"
..
show "P⇩1 ∘ ?HK = H"
proof
fix t
show "(P⇩1 ∘ ?HK) t = H t"
using P⇩1_def HK.preserves_reflects_arr
by (simp add: H.extensional tuple_def)
qed
moreover show "P⇩0 ∘ ?HK = K"
proof
fix t
show "(P⇩0 ∘ ?HK) t = K t"
using P⇩0_def HK.preserves_reflects_arr
by (simp add: K.extensional tuple_def)
qed
ultimately
have "simulation X resid ?HK ∧ P⇩1 ∘ ?HK = H ∧ P⇩0 ∘ ?HK = K"
using HK.simulation_axioms by simp
moreover have "⋀M. simulation X resid M ∧ P⇩1 ∘ M = H ∧ P⇩0 ∘ M = K
⟹ M = ?HK"
unfolding P⇩1_def P⇩0_def tuple_def
using simulation.extensional simulation.preserves_reflects_arr
by fastforce
ultimately show "∃!HK. simulation X resid HK ∧
P⇩1 o HK = H ∧ P⇩0 o HK = K"
by auto
qed
lemma preserves_weakly_extensional_rts:
assumes "weakly_extensional_rts A" and "weakly_extensional_rts B"
shows "weakly_extensional_rts resid"
using assms
by unfold_locales
(metis con_char ide_char⇩F⇩P prod.exhaust_sel prfx_implies_con
weakly_extensional_rts.con_ide_are_eq)
lemma preserves_extensional_rts:
assumes "extensional_rts A" and "extensional_rts B"
shows "extensional_rts resid"
using assms
by unfold_locales
(metis (no_types, lifting) extensional_rts.extensional fst_conv ide_char⇩F⇩P
ide_implies_arr not_arr_null null_char prod.exhaust_sel resid_def snd_conv)
lemma preserves_small_rts:
assumes "small_rts A" and "small_rts B"
shows "small_rts resid"
proof
interpret A: small_rts A
using assms(1) by blast
interpret B: small_rts B
using assms(2) by blast
show "small (Collect arr)"
proof -
have 1: "Collect arr ⊆ {t. A.arr (fst t) ∧ B.arr (snd t)}"
using arr_char by blast
obtain φ
where φ: "inj_on φ (Collect A.arr) ∧ φ ` Collect A.arr ∈ range elts"
using A.small small_def by metis
obtain ψ
where ψ: "inj_on ψ (Collect B.arr) ∧ ψ ` Collect B.arr ∈ range elts"
using B.small small_def by metis
let ?φψ = "λab. vpair (φ (fst ab)) (ψ (snd ab))"
have "inj_on ?φψ (Collect arr)"
using 1 φ ψ arr_char inj_on_def [of φ "Collect A.arr"]
inj_on_def [of ψ "Collect B.arr"] prod.expand
by (intro inj_onI) force
moreover have "?φψ ` Collect arr ∈ range elts"
proof -
have "?φψ ` Collect arr ⊆
elts (vtimes (set (φ ` Collect A.arr)) (set (ψ ` Collect B.arr)))"
using A.small B.small arr_char by auto
thus ?thesis
by (meson down_raw)
qed
ultimately show ?thesis
by (meson small_def)
qed
qed
end
locale fibered_product_of_weakly_extensional_rts =
A: weakly_extensional_rts A +
B: weakly_extensional_rts B +
fibered_product_rts
begin
sublocale weakly_extensional_rts resid
using A.weakly_extensional_rts_axioms B.weakly_extensional_rts_axioms
preserves_weakly_extensional_rts
by auto
lemma is_weakly_extensional_rts:
shows "weakly_extensional_rts resid"
..
lemma src_char:
shows "src t = (if arr t then (A.src (fst t), B.src (snd t)) else null)"
proof (cases "arr t")
show "¬ arr t ⟹ ?thesis"
using src_def by presburger
assume t: "arr t"
show ?thesis
proof (intro src_eqI)
show "ide (if arr t then (A.src (fst t), B.src (snd t)) else null)"
using t ide_char⇩F⇩P
by simp (metis A.src_eqI B.src_eqI con_arr_src(2) con_char ide_src)
show "(if arr t then (A.src (fst t), B.src (snd t)) else null) ⌢ t"
using t con_char arr_char
by simp
(metis A.arr_def A.src_eqI B.arr_def B.src_eqI
con_imp_coinitial_ax ide_char⇩F⇩P)
qed
qed
end
locale fibered_product_of_extensional_rts =
A: extensional_rts A +
B: extensional_rts B +
fibered_product_of_weakly_extensional_rts
begin
sublocale fibered_product_of_weakly_extensional_rts A B ..
sublocale extensional_rts resid
using A.extensional_rts_axioms B.extensional_rts_axioms preserves_extensional_rts
by blast
lemma is_extensional_rts:
shows "extensional_rts resid"
..
end
locale fibered_product_of_small_rts =
A: small_rts A +
B: small_rts B +
fibered_product_rts
begin
sublocale small_rts resid
by (simp add: A.small_rts_axioms B.small_rts_axioms preserves_small_rts)
lemma is_small_rts:
shows "small_rts resid"
..
end
section "Product RTS"
text‹
It is possible to define a product construction for RTS's as a special case of the
fibered product, but some inconveniences result from that approach.
In addition, we have already defined a product construction in
@{theory ResiduatedTransitionSystem.ResiduatedTransitionSystem}.
So, we will build on that existing construction.
›
definition pointwise_tuple :: "('x ⇒ 'a) ⇒ ('x ⇒ 'b) ⇒ 'x ⇒ 'a × 'b" ("⟨⟨_, _⟩⟩")
where "pointwise_tuple H K ≡ (λt. (H t, K t))"
context product_rts
begin
definition P⇩0 :: "'a × 'b ⇒ 'b"
where "P⇩0 t ≡ if arr t then snd t else B.null"
definition P⇩1 :: "'a × 'b ⇒ 'a"
where "P⇩1 t ≡ if arr t then fst t else A.null"
sublocale P⇩0: simulation resid B P⇩0
using P⇩0_def con_char resid_def arr_resid con_implies_arr(1-2)
by unfold_locales auto
lemma P⇩0_is_simulation:
shows "simulation resid B P⇩0"
..
sublocale P⇩1: simulation resid A P⇩1
using P⇩1_def con_char resid_def arr_resid con_implies_arr(1-2)
by unfold_locales auto
lemma P⇩1_is_simulation:
shows "simulation resid A P⇩1"
..
abbreviation tuple :: "('x ⇒ 'a) ⇒ ('x ⇒ 'b) ⇒ 'x ⇒ 'a × 'b"
where "tuple ≡ pointwise_tuple"
lemma universality:
assumes "simulation X A H" and "simulation X B K"
shows [intro]: "simulation X resid ⟨⟨H, K⟩⟩"
and "P⇩1 ∘ ⟨⟨H, K⟩⟩ = H" and "P⇩0 ∘ ⟨⟨H, K⟩⟩ = K"
and "∃!HK. simulation X resid HK ∧ P⇩1 o HK = H ∧ P⇩0 o HK = K"
proof -
interpret H: simulation X A H
using assms(1) by blast
interpret K: simulation X B K
using assms(2) by blast
interpret HK: simulation X resid ‹⟨⟨H, K⟩⟩›
proof
show "⋀t. ¬ H.A.arr t ⟹ ⟨⟨H, K⟩⟩ t = null"
by (simp add: H.extensional K.extensional pointwise_tuple_def)
fix t u
assume con: "H.A.con t u"
have 1: "H.A.arr t ∧ H.A.arr u"
using con H.A.con_implies_arr(1-2) by force
show "con (⟨⟨H, K⟩⟩ t) (⟨⟨H, K⟩⟩ u)"
using 1 con con_char H.preserves_con K.preserves_con pointwise_tuple_def
by (metis fst_conv snd_conv)
thus "⟨⟨H, K⟩⟩ (X t u) = resid (⟨⟨H, K⟩⟩ t) (⟨⟨H, K⟩⟩ u)"
unfolding pointwise_tuple_def
using 1 con resid_def null_char con_char arr_char
by simp
qed
show "simulation X resid ⟨⟨H, K⟩⟩" ..
show "P⇩1 ∘ ⟨⟨H, K⟩⟩ = H"
unfolding pointwise_tuple_def
using P⇩1_def HK.preserves_reflects_arr
by (auto simp add: H.extensional)
moreover show "P⇩0 ∘ ⟨⟨H, K⟩⟩ = K"
unfolding pointwise_tuple_def
using P⇩0_def HK.preserves_reflects_arr
by (auto simp add: K.extensional)
ultimately have "simulation X resid ⟨⟨H, K⟩⟩ ∧
P⇩1 ∘ ⟨⟨H, K⟩⟩ = H ∧ P⇩0 ∘ ⟨⟨H, K⟩⟩ = K"
using HK.simulation_axioms by simp
moreover have "⋀M. simulation X resid M ∧ P⇩1 ∘ M = H ∧ P⇩0 ∘ M = K
⟹ M = ⟨⟨H, K⟩⟩"
proof
fix M t
assume 1: "simulation X resid M ∧ P⇩1 ∘ M = H ∧ P⇩0 ∘ M = K"
interpret M: simulation X resid M
using 1 by blast
show "M t = ⟨⟨H, K⟩⟩ t"
using 1 M.extensional M.preserves_reflects_arr
unfolding P⇩1_def P⇩0_def pointwise_tuple_def
by force
qed
ultimately
show "∃!HK. simulation X resid HK ∧ P⇩1 o HK = H ∧ P⇩0 o HK = K"
by auto
qed
lemma proj_joint_monic:
assumes "simulation X resid F" and "simulation X resid G"
and "P⇩0 ∘ F = P⇩0 ∘ G" and "P⇩1 ∘ F = P⇩1 ∘ G"
shows "F = G"
using assms(1-4) P⇩0_is_simulation P⇩1_is_simulation universality(4)
by blast
lemma tuple_proj:
assumes "simulation X resid F"
shows "⟨⟨P⇩1 ∘ F, P⇩0 ∘ F⟩⟩ = F"
by (meson P⇩0_is_simulation P⇩1_is_simulation proj_joint_monic assms
universality(1-3) simulation_comp)
lemma proj_tuple:
assumes "simulation X A F" and "simulation X B G"
shows "P⇩1 ∘ ⟨⟨F, G⟩⟩ = F" and "P⇩0 ∘ ⟨⟨F, G⟩⟩ = G"
using assms(1-2) universality(2-3) by auto
lemma preserves_weakly_extensional_rts:
assumes "weakly_extensional_rts A" and "weakly_extensional_rts B"
shows "weakly_extensional_rts resid"
by (metis assms(1-2) ide_char prfx_char prod.exhaust_sel rts_axioms
weakly_extensional_rts.intro weakly_extensional_rts.weak_extensionality
weakly_extensional_rts_axioms.intro)
lemma preserves_extensional_rts:
assumes "extensional_rts A" and "extensional_rts B"
shows "extensional_rts resid"
proof -
interpret A: extensional_rts A
using assms(1) by blast
interpret B: extensional_rts B
using assms(2) by blast
show ?thesis
by unfold_locales
(metis A.extensional B.extensional cong_char prod.collapse)
qed
lemma preserves_small_rts:
assumes "small_rts A" and "small_rts B"
shows "small_rts resid"
proof
interpret A: small_rts A
using assms(1) by blast
interpret B: small_rts B
using assms(2) by blast
show "small (Collect arr)"
proof -
interpret One: one_arr_rts ‹TYPE(bool)›
by unfold_locales auto
interpret simulation A One.resid ‹One.terminator A›
using One.terminator_is_simulation A.rts_axioms by blast
interpret simulation B One.resid ‹One.terminator B›
using One.terminator_is_simulation B.rts_axioms by blast
interpret AxB: fibered_product_of_small_rts A B One.resid
‹One.terminator A› ‹One.terminator B› ..
have "Collect arr ⊆ Collect AxB.arr"
using AxB.arr_char arr_char One.terminator_def
by (metis Collect_mono)
moreover have "small (Collect AxB.arr)"
using AxB.small by blast
ultimately show ?thesis
using smaller_than_small by blast
qed
qed
end
locale product_of_extensional_rts =
A: extensional_rts A +
B: extensional_rts B +
product_rts
begin
sublocale product_of_weakly_extensional_rts A B ..
sublocale extensional_rts resid
using A.extensional_rts_axioms B.extensional_rts_axioms preserves_extensional_rts
by blast
lemma is_extensional_rts:
shows "extensional_rts resid"
..
lemma proj_tuple2:
assumes "transformation X A F G S" and "transformation X B H K T"
shows "P⇩1 ∘ ⟨⟨S, T⟩⟩ = S" and "P⇩0 ∘ ⟨⟨S, T⟩⟩ = T"
proof -
interpret S: transformation X A F G S
using assms(1) by blast
interpret T: transformation X B H K T
using assms(2) by blast
show "P⇩1 ∘ ⟨⟨S, T⟩⟩ = S"
proof
fix t
show "(P⇩1 ∘ ⟨⟨S, T⟩⟩) t = S t"
unfolding pointwise_tuple_def P⇩1_def
using S.extensional S.preserves_arr T.preserves_arr
apply auto[1]
by metis+
qed
show "P⇩0 ∘ ⟨⟨S, T⟩⟩ = T"
proof
fix t
show "(P⇩0 ∘ ⟨⟨S, T⟩⟩) t = T t"
unfolding pointwise_tuple_def P⇩0_def
using T.extensional S.preserves_arr T.preserves_arr
apply auto[1]
by metis+
qed
qed
lemma universality2:
assumes "simulation X resid F" and "simulation X resid G"
and "transformation X A (P⇩1 ∘ F) (P⇩1 ∘ G) S"
and "transformation X B (P⇩0 ∘ F) (P⇩0 ∘ G) T"
shows [intro]: "transformation X resid F G ⟨⟨S, T⟩⟩"
and "P⇩1 ∘ ⟨⟨S, T⟩⟩ = S" and "P⇩0 ∘ ⟨⟨S, T⟩⟩ = T"
and "∃!ST. transformation X resid F G ST ∧ P⇩1 o ST = S ∧ P⇩0 o ST = T"
proof -
interpret X: rts X
using assms(1) simulation_def by auto
interpret A: weakly_extensional_rts A
using assms(3) transformation_def by blast
interpret B: weakly_extensional_rts B
using assms(4) transformation_def by blast
interpret X: weakly_extensional_rts X
using assms(4) transformation_def by blast
interpret F: simulation X resid F
using assms(1) by blast
interpret F: simulation_to_weakly_extensional_rts X resid F ..
interpret G: simulation X resid G
using assms(2) by blast
interpret G: simulation_to_weakly_extensional_rts X resid G ..
interpret P⇩1oF: composite_simulation X resid A F P⇩1 ..
interpret P⇩1oF: simulation_to_weakly_extensional_rts X A P⇩1oF.map ..
interpret P⇩1oG: composite_simulation X resid A G P⇩1 ..
interpret P⇩1oG: simulation_to_weakly_extensional_rts X A P⇩1oF.map ..
interpret P⇩0oF: composite_simulation X resid B F P⇩0 ..
interpret P⇩0oF: simulation_to_weakly_extensional_rts X A P⇩1oF.map ..
interpret P⇩0oG: composite_simulation X resid B G P⇩0 ..
interpret P⇩0oF: simulation_to_weakly_extensional_rts X A P⇩1oF.map ..
interpret S: transformation X A ‹P⇩1 ∘ F› ‹P⇩1 ∘ G› S
using assms(3) by blast
interpret S: transformation_to_extensional_rts X A ‹P⇩1 ∘ F› ‹P⇩1 ∘ G› S ..
interpret T: transformation X B ‹P⇩0 ∘ F› ‹P⇩0 ∘ G› T
using assms(4) by blast
interpret T: transformation_to_extensional_rts X B ‹P⇩0 ∘ F› ‹P⇩0 ∘ G› T ..
interpret ST: transformation X resid F G ‹⟨⟨S, T⟩⟩›
proof
show "⋀t. ¬ X.arr t ⟹ ⟨⟨S, T⟩⟩ t = null"
by (simp add: S.extensional T.extensional pointwise_tuple_def)
fix t
assume t: "X.ide t"
have arr: "arr (⟨⟨S, T⟩⟩ t)"
unfolding pointwise_tuple_def
using t S.preserves_arr T.preserves_arr by auto
show "src (⟨⟨S, T⟩⟩ t) = F t"
proof -
have "F t = ((P⇩1 ∘ F) t, (P⇩0 ∘ F) t)"
using t tuple_proj F.simulation_axioms pointwise_tuple_def
by metis
thus ?thesis
using arr src_char arr_char
by (simp add: S.preserves_src T.preserves_src t pointwise_tuple_def)
qed
show "trg (⟨⟨S, T⟩⟩ t) = G t"
proof -
have "G t = ((P⇩1 ∘ G) t, (P⇩0 ∘ G) t)"
using t tuple_proj G.simulation_axioms pointwise_tuple_def
by metis
thus ?thesis
using arr trg_char arr_char
by (simp add: S.preserves_trg T.preserves_trg t pointwise_tuple_def)
qed
next
fix t
assume t: "X.arr t"
have con1: "S (X.src t) ⌢⇩A P⇩1 (F t)"
proof -
have "S t = A.join (S (X.src t)) (P⇩1 (F t))"
using t S.naturality3'⇩E by auto
hence "A.prfx (S (X.src t)) (S t) ∧ A.prfx (P⇩1 (F t)) (S t)"
using t A.join_sym A.arr_prfx_join_self S.preserves_arr
A.joinable_iff_arr_join
by metis
thus ?thesis
using t S.preserves_arr A.con_arr_self A.con_prfx(1-2) by blast
qed
moreover have con0: "T (X.src t) ⌢⇩B P⇩0 (F t)"
proof -
have "T t = B.join (T (X.src t)) (P⇩0 (F t))"
using t T.naturality3'⇩E by auto
hence "B.prfx (T (X.src t)) (T t) ∧ B.prfx (P⇩0 (F t)) (T t)"
using t B.join_sym B.arr_prfx_join_self T.preserves_arr
B.joinable_iff_arr_join
by metis
thus ?thesis
using t T.preserves_arr B.con_arr_self B.con_prfx(1-2) by blast
qed
show "⟨⟨S, T⟩⟩ (X.src t) \\ F t = ⟨⟨S, T⟩⟩ (X.trg t)"
proof -
have "⟨⟨S, T⟩⟩ (X.src t) \\ F t =
(S (X.src t), T (X.src t)) \\ (P⇩1 (F t), P⇩0 (F t))"
using t tuple_proj [of X F] F.simulation_axioms
pointwise_tuple_def [of S T]
pointwise_tuple_def [of P⇩1oF.map P⇩0oF.map]
apply auto[1]
by metis
also have "... = (S (X.src t) \\⇩A P⇩1 (F t), T (X.src t) \\⇩B P⇩0 (F t))"
using t con0 con1 resid_def by auto
also have "... = (S (X.trg t), T (X.trg t))"
using t S.naturality1 T.naturality1 by auto
also have "... = ⟨⟨S, T⟩⟩ (X.trg t)"
using t pointwise_tuple_def by metis
finally show ?thesis by blast
qed
show "F t \\ ⟨⟨S, T⟩⟩ (X.src t) = G t"
proof -
have "F t \\ ⟨⟨S, T⟩⟩ (X.src t) =
(P⇩1 (F t), P⇩0 (F t)) \\ (S (X.src t), T (X.src t))"
using t tuple_proj [of X F] F.simulation_axioms
pointwise_tuple_def [of S T]
pointwise_tuple_def [of P⇩1oF.map P⇩0oF.map]
apply auto[1]
by metis
also have "... = (P⇩1 (F t) \\⇩A S (X.src t), P⇩0 (F t) \\⇩B T (X.src t))"
using t con0 con1 resid_def A.con_sym B.con_sym by auto
also have "... = (P⇩1oG.map t, P⇩0oG.map t)"
using t S.naturality2 T.naturality2 by auto
also have "... = G t"
using t tuple_proj G.simulation_axioms pointwise_tuple_def by metis
finally show ?thesis by blast
qed
show "join_of (⟨⟨S, T⟩⟩ (X.src t)) (F t) (⟨⟨S, T⟩⟩ t)"
proof -
have "A.join_of (S (X.src t)) (P⇩1oF.map t) (S t)"
using t con1 S.naturality3 [of t] by blast
moreover have "B.join_of (T (X.src t)) (P⇩0oF.map t) (T t)"
using t con0 T.naturality3 [of t] by blast
ultimately show ?thesis
unfolding pointwise_tuple_def
using t join_of_char(1-2) F.preserves_reflects_arr P⇩0_def P⇩1_def
by auto
qed
qed
show 1: "transformation X (\\) F G ⟨⟨S, T⟩⟩" ..
show 2: "P⇩1 ∘ ⟨⟨S, T⟩⟩ = S" and 3: "P⇩0 ∘ ⟨⟨S, T⟩⟩ = T"
using proj_tuple2 S.transformation_axioms T.transformation_axioms
by blast+
show "∃!ST. transformation X (\\) F G ST ∧ P⇩1 ∘ ST = S ∧ P⇩0 ∘ ST = T"
proof -
have "⋀ST. ⟦transformation X (\\) F G ST; P⇩1 ∘ ST = S; P⇩0 ∘ ST = T⟧
⟹ ST = ⟨⟨S, T⟩⟩"
proof -
fix ST
assume ST: "transformation X resid F G ST"
assume 0: "P⇩0 ∘ ST = T"
assume 1: "P⇩1 ∘ ST = S"
interpret ST: transformation X resid F G ST
using ST by blast
show "ST = ⟨⟨S, T⟩⟩"
proof
fix t
show "ST t = ⟨⟨S, T⟩⟩ t"
unfolding pointwise_tuple_def
using 0 1 ST.preserves_arr ST.extensional P⇩0_def P⇩1_def
apply auto[1]
by (metis prod.exhaust_sel)
qed
qed
thus ?thesis
using 1 2 3 by metis
qed
qed
lemma proj_joint_monic2:
assumes "transformation X resid F G S" and "transformation X resid F G T"
and "P⇩0 ∘ S = P⇩0 ∘ T" and "P⇩1 ∘ S = P⇩1 ∘ T"
shows "S = T"
using assms transformation_whisker_left [of X resid F G S] universality2(4)
A.weakly_extensional_rts_axioms B.weakly_extensional_rts_axioms
P⇩1.simulation_axioms P⇩0.simulation_axioms
by (metis transformation_def)
lemma join_char:
shows "join t u =
(if joinable t u
then (A.join (fst t) (fst u), B.join (snd t) (snd u))
else null)"
by (metis A.join_is_join_of B.join_is_join_of fst_conv join_is_join_of
join_of_char(1-2) join_of_unique joinable_iff_join_not_null snd_conv)
lemma join_simp:
assumes "joinable t u"
shows "join t u = (A.join (fst t) (fst u), B.join (snd t) (snd u))"
using assms join_char by auto
end
locale product_of_small_rts =
A: small_rts A +
B: small_rts B +
product_rts
begin
sublocale small_rts resid
using A.small_rts_axioms B.small_rts_axioms preserves_small_rts
by blast
lemma is_small_rts:
shows "small_rts resid"
..
end
lemma simulation_tuple [intro]:
assumes "simulation X A H" and "simulation X B K"
and "Y = product_rts.resid A B"
shows "simulation X Y ⟨⟨H, K⟩⟩"
using assms product_rts.universality(1) [of A B X H K]
by (simp add: product_rts.intro simulation_def)
lemma simulation_product [intro]:
assumes "simulation A B H" and "simulation C D K"
and "X = product_rts.resid A C" and "Y = product_rts.resid B D"
shows "simulation X Y (product_simulation.map A C H K)"
using assms
by (meson product_rts_def product_rts_def product_simulation.intro
product_simulation.is_simulation simulation_def simulation_def)
lemma comp_pointwise_tuple:
shows "⟨⟨H, K⟩⟩ ∘ L = ⟨⟨H ∘ L, K ∘ L⟩⟩"
unfolding pointwise_tuple_def
by auto
lemma comp_product_simulation_tuple2:
assumes "simulation A A' F" and "simulation B B' G"
and "transformation X A H⇩0 H⇩1 H" and "transformation X B K⇩0 K⇩1 K"
shows "product_simulation.map A B F G ∘ ⟨⟨H, K⟩⟩ = ⟨⟨F ∘ H, G ∘ K⟩⟩"
proof -
interpret X: weakly_extensional_rts X
using assms(3) transformation.axioms(1) by blast
interpret A: rts A
using assms(1) simulation.axioms(1) by blast
interpret B: rts B
using assms(2) simulation.axioms(1) by blast
interpret A': rts A'
using assms(1) simulation.axioms(2) by blast
interpret B': rts B'
using assms(2) simulation.axioms(2) by blast
interpret AxB: product_rts A B ..
interpret A'xB': product_rts A' B' ..
interpret F: simulation A A' F
using assms by blast
interpret G: simulation B B' G
using assms by blast
interpret FxG: product_simulation A B A' B' F G ..
interpret H: transformation X A H⇩0 H⇩1 H
using assms(3) by blast
interpret K: transformation X B K⇩0 K⇩1 K
using assms(4) by blast
show ?thesis
proof
fix x
show "(FxG.map ∘ ⟨⟨H, K⟩⟩) x = ⟨⟨F ∘ H, G ∘ K⟩⟩ x"
using FxG.extensional pointwise_tuple_def F.extensional G.extensional
H.extensional K.extensional H.preserves_arr K.preserves_arr
by (cases "X.arr x") (auto simp add: pointwise_tuple_def)
qed
qed
lemma comp_product_simulation_tuple:
assumes "simulation A A' F" and "simulation B B' G"
and "simulation X A H" and "simulation X B K"
shows "product_simulation.map A B F G ∘ ⟨⟨H, K⟩⟩ = ⟨⟨F ∘ H, G ∘ K⟩⟩"
proof -
interpret X: rts X
using assms(3) simulation.axioms(1) by blast
interpret A: rts A
using assms(1) simulation.axioms(1) by blast
interpret B: rts B
using assms(2) simulation.axioms(1) by blast
interpret A': rts A'
using assms(1) simulation.axioms(2) by blast
interpret B': rts B'
using assms(2) simulation.axioms(2) by blast
interpret AxB: product_rts A B ..
interpret A'xB': product_rts A' B' ..
interpret F: simulation A A' F
using assms by blast
interpret G: simulation B B' G
using assms by blast
interpret FxG: product_simulation A B A' B' F G ..
interpret H: simulation X A H
using assms(3) by blast
interpret K: simulation X B K
using assms(4) by blast
show ?thesis
proof
fix x
show "(FxG.map ∘ ⟨⟨H, K⟩⟩) x = ⟨⟨F ∘ H, G ∘ K⟩⟩ x"
using FxG.extensional pointwise_tuple_def F.extensional G.extensional
H.extensional K.extensional H.preserves_reflects_arr
K.preserves_reflects_arr
by (cases "X.arr x") (auto simp add: pointwise_tuple_def)
qed
qed
locale product_transformation =
A1: weakly_extensional_rts A1 +
A0: weakly_extensional_rts A0 +
B1: extensional_rts B1 +
B0: extensional_rts B0 +
A1xA0: product_rts A1 A0 +
B1xB0: product_rts B1 B0 +
F1: simulation A1 B1 F1 +
F0: simulation A0 B0 F0 +
G1: simulation A1 B1 G1 +
G0: simulation A0 B0 G0 +
T1: transformation A1 B1 F1 G1 T1 +
T0: transformation A0 B0 F0 G0 T0
for A1 :: "'a1 resid" (infix "\\⇩A⇩1" 70)
and A0 :: "'a0 resid" (infix "\\⇩A⇩0" 70)
and B1 :: "'b1 resid" (infix "\\⇩B⇩1" 70)
and B0 :: "'b0 resid" (infix "\\⇩B⇩0" 70)
and F1 :: "'a1 ⇒ 'b1"
and F0 :: "'a0 ⇒ 'b0"
and G1 :: "'a1 ⇒ 'b1"
and G0 :: "'a0 ⇒ 'b0"
and T1 :: "'a1 ⇒ 'b1"
and T0 :: "'a0 ⇒ 'b0"
begin
sublocale F1: simulation_to_weakly_extensional_rts A1 B1 F1 ..
sublocale F0: simulation_to_weakly_extensional_rts A0 B0 F0 ..
sublocale G1: simulation_to_weakly_extensional_rts A1 B1 G1 ..
sublocale G0: simulation_to_weakly_extensional_rts A0 B0 G0 ..
sublocale A1xA0: product_of_weakly_extensional_rts A1 A0 ..
sublocale B1xB0: product_of_extensional_rts B1 B0 ..
sublocale F1xF0: product_simulation A1 A0 B1 B0 F1 F0 ..
sublocale G1xG0: product_simulation A1 A0 B1 B0 G1 G0 ..
abbreviation (input) map⇩0 :: "'a1 × 'a0 ⇒ 'b1 × 'b0"
where "map⇩0 ≡ (λa. (T1 (fst a), T0 (snd a)))"
sublocale TC: transformation_by_components
A1xA0.resid B1xB0.resid F1xF0.map G1xG0.map map⇩0
proof
show "⋀a. A1xA0.ide a ⟹ B1xB0.src (map⇩0 a) = F1xF0.map a"
unfolding F1xF0.map_def
using T1.preserves_arr T0.preserves_arr T1.preserves_src T0.preserves_src
B1xB0.src_char
by auto
show "⋀a. A1xA0.ide a ⟹ B1xB0.trg (map⇩0 a) = G1xG0.map a"
unfolding G1xG0.map_def
using T1.preserves_arr T0.preserves_arr T1.preserves_trg T0.preserves_trg
B1xB0.trg_char
by auto
fix t
assume t: "A1xA0.arr t"
show "B1xB0.resid (map⇩0 (A1xA0.src t)) (F1xF0.map t) =
map⇩0 (A1xA0.trg t)"
unfolding F1xF0.map_def
using t B1xB0.resid_def A1xA0.src_char A1xA0.trg_char
T1.naturality1 T0.naturality1 A1.con_arr_src(2) T1.preserves_con(2)
A0.con_arr_src(2) T0.preserves_con(2)
by auto
show "B1xB0.resid (F1xF0.map t) (map⇩0 (A1xA0.src t)) =
G1xG0.map t"
unfolding F1xF0.map_def G1xG0.map_def
using t B1xB0.resid_def A1xA0.src_char A1xA0.trg_char
T1.naturality2 T0.naturality2
apply auto[1]
apply (metis B1.conI B1.not_arr_null G1.preserves_reflects_arr)
by (metis B0.conI B0.not_arr_null G0.preserves_reflects_arr)
show "B1xB0.joinable (map⇩0 (A1xA0.src t)) (F1xF0.map t)"
unfolding F1xF0.map_def
using t A1xA0.src_char T1.naturality3 T0.naturality3
apply auto[1]
by (metis B0.joinable_def B1.joinable_def B1xB0.join_of_char(2)
fst_eqD snd_eqD)
qed
definition map :: "'a1 × 'a0 ⇒ 'b1 × 'b0"
where "map ≡ TC.map"
sublocale transformation
A1xA0.resid B1xB0.resid F1xF0.map G1xG0.map map
unfolding map_def ..
lemma is_transformation:
shows "transformation A1xA0.resid B1xB0.resid F1xF0.map G1xG0.map map"
..
lemma map_simp:
shows "map t = B1xB0.join (map⇩0 (A1xA0.src t)) (F1xF0.map t)"
unfolding map_def TC.map_def by blast
lemma map_simp_ide:
assumes "A1xA0.ide t"
shows "map t = map⇩0 (A1xA0.src t)"
unfolding map_def
using assms TC.map_simp_ide by simp
end
lemma comp_product_transformation_tuple:
assumes "transformation_to_extensional_rts A1 B1 F1 G1 T1"
and "transformation_to_extensional_rts A0 B0 F0 G0 T0"
and "simulation X A1 H1" and "simulation X A0 H0"
shows "product_transformation.map A1 A0 B1 B0 F1 F0 T1 T0 ∘ ⟨⟨H1, H0⟩⟩ =
⟨⟨T1 ∘ H1, T0 ∘ H0⟩⟩"
proof -
interpret X: rts X
using assms(3) simulation.axioms(1) by blast
interpret A1: weakly_extensional_rts A1
using assms(1) transformation_to_extensional_rts.axioms(1)
transformation.axioms(1)
by blast
interpret A0: weakly_extensional_rts A0
using assms(2) transformation_to_extensional_rts.axioms(1)
transformation.axioms(1)
by blast
interpret B1: extensional_rts B1
using assms(1) transformation_to_extensional_rts.axioms(2) by blast
interpret B0: extensional_rts B0
using assms(2) transformation_to_extensional_rts.axioms(2) by blast
interpret F1: simulation A1 B1 F1
using assms(1) transformation_to_extensional_rts.axioms(1)
transformation.axioms(3) simulation.axioms(3)
by blast
interpret F0: simulation A0 B0 F0
using assms(2) transformation_to_extensional_rts.axioms(1)
transformation.axioms(3) simulation.axioms(3)
by blast
interpret G1: simulation A1 B1 G1
using assms(1) transformation_to_extensional_rts.axioms(1)
transformation.axioms(4) simulation.axioms(3)
by blast
interpret G0: simulation A0 B0 G0
using assms(2) transformation_to_extensional_rts.axioms(1)
transformation.axioms(4) simulation.axioms(3)
by blast
interpret T1: transformation_to_extensional_rts A1 B1 F1 G1 T1
using assms(1) by blast
interpret T0: transformation_to_extensional_rts A0 B0 F0 G0 T0
using assms(2) by blast
interpret A1xA0: product_of_weakly_extensional_rts A1 A0 ..
interpret B1xB0: product_of_extensional_rts B1 B0 ..
interpret F1xF0: product_simulation A1 A0 B1 B0 F1 F0 ..
interpret G1xG0: product_simulation A1 A0 B1 B0 G1 G0 ..
interpret T1xT0: product_transformation A1 A0 B1 B0 F1 F0 G1 G0 T1 T0
..
interpret H1: simulation X A1 H1
using assms(3) by blast
interpret H0: simulation X A0 H0
using assms(4) by blast
show ?thesis
proof
fix x
show "(T1xT0.map ∘ ⟨⟨H1, H0⟩⟩) x = ⟨⟨T1 ∘ H1, T0 ∘ H0⟩⟩ x"
proof -
have "X.arr x ⟹
B1xB0.join
(T1 (fst (A1xA0.src (H1 x, H0 x))),
T0 (snd (A1xA0.src (H1 x, H0 x))))
(F1 (H1 x), F0 (H0 x)) =
(T1 (H1 x), T0 (H0 x))"
proof -
assume x: "X.arr x"
have "B1xB0.join
(T1 (fst (A1xA0.src (H1 x, H0 x))),
T0 (snd (A1xA0.src (H1 x, H0 x))))
(F1 (H1 x), F0 (H0 x)) =
B1xB0.join
(T1 (A1.src (H1 x)), T0 (A0.src (H0 x)))
(F1 (H1 x), F0 (H0 x))"
using x A1xA0.src_char by auto
also have "... = (T1 (H1 x), T0 (H0 x))"
using x B1xB0.join_char
by (simp add: B1xB0.join_of_char(2) T0.naturality3'⇩E(1-2)
T1.naturality3'⇩E(1-2))
finally show ?thesis by blast
qed
thus ?thesis
using pointwise_tuple_def H1.extensional H0.extensional
T1.extensional T0.extensional T1xT0.extensional T1xT0.map_def
T1xT0.TC.map_def comp_product_simulation_tuple
F1xF0.product_simulation_axioms G1xG0.product_simulation_axioms
by (cases "X.arr x") (auto simp add: pointwise_tuple_def)
qed
qed
qed
lemma simulation_interchange:
assumes "simulation A A' F" and "simulation B B' G"
and "simulation A' A'' F'" and "simulation B' B'' G'"
shows "product_simulation.map A B (F' ∘ F) (G' ∘ G) =
product_simulation.map A' B' F' G' ∘ product_simulation.map A B F G"
proof -
interpret F: simulation A A' F
using assms(1) by blast
interpret G: simulation B B' G
using assms(2) by blast
interpret F': simulation A' A'' F'
using assms(3) by blast
interpret G': simulation B' B'' G'
using assms(4) by blast
interpret F'oF: composite_simulation A A' A'' F F' ..
interpret G'oG: composite_simulation B B' B'' G G' ..
interpret FxG: product_simulation A B A' B' F G ..
interpret F'xG': product_simulation A' B' A'' B'' F' G' ..
interpret F'oFxG'oG: product_simulation A B A'' B'' ‹F' ∘ F› ‹G' ∘ G› ..
show "F'oFxG'oG.map = F'xG'.map ∘ FxG.map"
unfolding F'oFxG'oG.map_def FxG.map_def F'xG'.map_def
using F.extensional G.extensional F'.extensional G'.extensional by auto
qed
subsection "Associators"
text ‹
For any RTS's ‹A›, ‹B›, and ‹C›, there exists an invertible ``associator'' simulation
from the product RTS ‹(A × B) × C)› to the product RTS ‹A × (B × C)›.
›
locale ASSOC =
A: rts A +
B: rts B +
C: rts C
for A :: "'a resid"
and B :: "'b resid"
and C :: "'c resid"
begin
sublocale AxB: product_rts A B ..
sublocale BxC: product_rts B C ..
sublocale AxB_xC: product_rts AxB.resid C ..
sublocale Ax_BxC: product_rts A BxC.resid ..
text ‹
The following definition is expressed in a form that makes it evident that it
defines a simulation.
›
definition map :: "('a × 'b) × 'c ⇒ 'a × 'b × 'c"
where "map ≡ Ax_BxC.tuple
(AxB.P⇩1 ∘ AxB_xC.P⇩1)
(BxC.tuple (AxB.P⇩0 ∘ AxB_xC.P⇩1) AxB_xC.P⇩0)"
sublocale simulation AxB_xC.resid Ax_BxC.resid map
unfolding map_def
using AxB.P⇩0.simulation_axioms AxB.P⇩1.simulation_axioms
AxB_xC.P⇩0.simulation_axioms AxB_xC.P⇩1.simulation_axioms
by (intro simulation_tuple simulation_comp) auto
lemma is_simulation:
shows "simulation AxB_xC.resid Ax_BxC.resid map"
..
text ‹
The following explicit formula is more convenient for calculations.
›
lemma map_eq:
shows "map = (λx. if AxB_xC.arr x
then (fst (fst x), (snd (fst x), snd x))
else Ax_BxC.null)"
unfolding map_def pointwise_tuple_def AxB.P⇩0_def AxB.P⇩1_def
AxB_xC.P⇩0_def AxB_xC.P⇩1_def
by auto
definition map' :: "'a × 'b × 'c ⇒ ('a × 'b) × 'c"
where "map' ≡ AxB_xC.tuple
(AxB.tuple Ax_BxC.P⇩1 (BxC.P⇩1 ∘ Ax_BxC.P⇩0))
(BxC.P⇩0 ∘ Ax_BxC.P⇩0)"
sublocale inv: simulation Ax_BxC.resid AxB_xC.resid map'
unfolding map'_def
using BxC.P⇩0.simulation_axioms BxC.P⇩1.simulation_axioms
Ax_BxC.P⇩0.simulation_axioms Ax_BxC.P⇩1.simulation_axioms
by (intro simulation_tuple simulation_comp) auto
lemma inv_is_simulation:
shows "simulation Ax_BxC.resid AxB_xC.resid map'"
..
lemma map'_eq:
shows "map' =
(λx. if Ax_BxC.arr x
then ((fst x, fst (snd x)), snd (snd x))
else AxB_xC.null)"
unfolding map'_def pointwise_tuple_def BxC.P⇩0_def BxC.P⇩1_def
Ax_BxC.P⇩0_def Ax_BxC.P⇩1_def
by auto
lemma inverse_simulations_map'_map:
shows "inverse_simulations AxB_xC.resid Ax_BxC.resid map' map"
proof
show "map ∘ map' = I Ax_BxC.resid"
unfolding map_eq map'_eq by auto
show "map' ∘ map = I AxB_xC.resid"
unfolding map_eq map'_eq by auto
qed
end
section "Exponential RTS"
text ‹
The exponential ‹[A, B]› of RTS's ‹A› and ‹B› has states corresponding to simulations
from ‹A› to ‹B› and transitions corresponding to transformations between such simulations.
Since our definition of transformation has assumed that ‹A› and ‹B› are weakly extensional,
we need to include those assumptions here. In addition, the definition of residuation
for the exponential RTS uses the assumption of uniqueness of joins, so we actually assume
that ‹B› is extensional. Things become rather inconvenient if this assumption is not made,
and I have not investigated whether relaxing it is possible.
›
locale consistent_transformations =
A: weakly_extensional_rts A +
B: extensional_rts B +
F: simulation A B F +
G: simulation A B G +
H: simulation A B H +
σ: transformation A B F G σ +
τ: transformation A B F H τ
for A :: "'a resid" (infix "\\⇩A" 70)
and B :: "'b resid" (infix "\\⇩B" 70)
and F :: "'a ⇒ 'b"
and G :: "'a ⇒ 'b"
and H :: "'a ⇒ 'b"
and σ :: "'a ⇒ 'b"
and τ :: "'a ⇒ 'b" +
assumes con: "A.ide a ⟶ B.con (σ a) (τ a)"
begin
sublocale σ: transformation_to_extensional_rts A B F G σ ..
sublocale τ: transformation_to_extensional_rts A B F H τ ..
sublocale sym: consistent_transformations A B F H G τ σ
by (meson B.residuation_axioms con consistent_transformations_axioms
consistent_transformations_axioms.intro consistent_transformations_def
residuation.con_sym)
text ‹
The ``apex'' determined by consistent transformations ‹σ› and ‹τ› is the simulation
whose value at a transition ‹t› of ‹A› may be visualized as the apex of a rectangular
parallelepiped, which is formed with ‹t› as its base, the components at ‹src c› of the
transformations associated with the two transitions and their residuals,
and the images of ‹t› under these transformations.
›
abbreviation apex :: "'a ⇒ 'b"
where "apex ≡ (λt. if A.arr t
then H t \\⇩B (σ (A.src t) \\⇩B τ (A.src t))
else B.null)"
abbreviation resid :: "'a ⇒ 'b"
where "resid ≡ (λt. if A.arr t
then B.join (σ (A.src t) \\⇩B τ (A.src t)) (H t)
else B.null)"
end
text‹
For unknown reasons, it is necessary to close and re-open the context here in order
to obtain access to ‹sym› as a sublocale.
›
context consistent_transformations
begin
lemma sym_apex_eq:
shows "sym.apex = apex"
proof
fix t
show "sym.apex t = apex t"
by (metis (full_types) σ.naturality2 τ.naturality2 B.cube)
qed
text‹
The apex associated with two consistent transformations is a simulation.
The proof that it preserves residuation can be visualized in terms of a
three-dimensional figure consisting of four rectangular parallelepipeds connected
into an overall diamond shape, with ‹Dom τ t› and ‹Dom σ u› (which is equal to ‹Dom τ u›)
and their residuals at the base of the overall diamond and with ‹Apex σ τ t›
and ‹Apex σ τ u› at its peak.
›
interpretation apex: simulation A B apex
proof
show "⋀t. ¬ A.arr t ⟹ apex t = B.null"
by simp
show "⋀t u. t ⌢⇩A u ⟹ apex t ⌢⇩B apex u"
proof -
fix t u
assume con: "t ⌢⇩A u"
have "apex t ⌢⇩B apex u ⟷
H t \\⇩B (σ (A.src t) \\⇩B τ (A.src t)) ⌢⇩B
H u \\⇩B (σ (A.src u) \\⇩B τ (A.src u))"
using A.con_implies_arr(1-2) con by simp
also have "... ⟷ (F t \\⇩B τ (A.src t)) \\⇩B
(σ (A.src t) \\⇩B τ (A.src t)) ⌢⇩B
(F u \\⇩B τ (A.src t)) \\⇩B
(σ (A.src t) \\⇩B τ (A.src t))"
using A.con_implies_arr(1-2) τ.naturality2 con A.con_imp_eq_src
by (metis (mono_tags, lifting))
also have "... ⟷ (F t \\⇩B F u) \\⇩B τ (A.trg u) ⌢⇩B
(σ (A.src t) \\⇩B F u) \\⇩B τ (A.trg u)"
using A.con_imp_eq_src τ.naturality1 con B.con_def B.cube by presburger
also have "... ⟷ (F t \\⇩B F u) \\⇩B τ (A.trg u) ⌢⇩B
σ (A.trg u) \\⇩B τ (A.trg u)"
using A.con_imp_eq_src σ.naturality1 con by presburger
also have "... ⟷ F (t \\⇩A u) \\⇩B τ (A.trg u) ⌢⇩B
σ (A.trg u) \\⇩B τ (A.trg u)"
using F.preserves_resid con by presburger
also have "... ⟷ True"
by (metis A.arr_resid A.ide_trg A.src_resid B.con_def B.con_sym
B.cube σ.naturality1 τ.naturality1 con sym.con)
finally show "apex t ⌢⇩B apex u" by blast
qed
show "⋀t u. t ⌢⇩A u ⟹ apex (t \\⇩A u) = apex t \\⇩B apex u"
using σ.naturality1 τ.naturality1 τ.naturality2 B.cube A.arr_resid A.arr_src_iff_arr
A.con_imp_eq_src A.con_implies_arr(1-2) A.src_resid H.preserves_resid
by auto (metis (mono_tags, lifting))
qed
lemma simulation_apex:
shows "simulation A B apex"
..
lemma resid_ide:
assumes "A.ide a"
shows "resid a = σ a \\⇩B τ a"
by (metis (full_types) A.arr_def A.ideE A.weakly_extensional_rts_axioms
B.join_prfx(2) apex.preserves_ide assms weakly_extensional_rts.src_ide)
interpretation resid: transformation ‹(\⇩A)› ‹(\⇩B)› H apex resid
proof -
have 2: "⋀f. A.ide f ⟹ B.joinable (σ (A.src f) \\⇩B τ (A.src f)) (H f)"
using B.joinable_iff_arr_join con resid_ide by auto
show "transformation (\\⇩A) (\\⇩B) H apex resid"
proof
show "⋀f. ¬ A.arr f ⟹ resid f = B.null"
by force
show 3: "⋀f. A.ide f ⟹ B.src (resid f) = H f"
using 2 B.src_join τ.preserves_trg con by auto
show "⋀f. A.ide f ⟹ B.trg (resid f) = apex f"
using B.apex_arr_prfx(2) apex.preserves_ide resid_ide by force
show "⋀f. A.arr f ⟹ H f \\⇩B resid (A.src f) = apex f"
using resid_ide by force
show "⋀f. A.arr f ⟹ resid (A.src f) \\⇩B H f = resid (A.trg f)"
using A.ide_src A.ide_trg B.cube σ.naturality1 τ.naturality1
τ.naturality2 resid_ide
by auto metis
show "⋀f. A.arr f ⟹ B.join_of (resid (A.src f)) (H f) (resid f)"
proof -
fix f
assume f: "A.arr f"
have 1: "B.joinable (σ (A.src f) \\⇩B τ (A.src f)) (H f)"
proof -
have "(σ (A.src f) ⊔⇩B F f) \\⇩B τ (A.src f) =
(σ (A.src f) \\⇩B τ (A.src f)) ⊔⇩B (F f \\⇩B τ (A.src f))"
by (metis A.prfx_reflexive A.trg_def B.conI B.con_with_join_if(2)
B.not_arr_null B.resid_join⇩E(3) H.preserves_reflects_arr
σ.naturality1_ax σ.naturality3'⇩E(2) τ.naturality1_ax τ.naturality2
f sym.con)
hence "B.join_of (σ (A.src f) \\⇩B τ (A.src f)) (H f)
((σ (A.src f) \\⇩B τ (A.src f)) ⊔⇩B (F f \\⇩B τ (A.src f)))"
using f A.ide_trg B.arr_resid_iff_con B.conE B.con_sym B.con_with_join_if(1)
B.join_def B.join_is_join_of H.preserves_reflects_arr σ.naturality1
σ.naturality3'⇩E(2) τ.naturality1 τ.naturality2
by (metis sym.con)
thus ?thesis
using B.joinable_def by blast
qed
show "B.join_of (resid (A.src f)) (H f) (resid f)"
using 1 A.ide_src B.join_is_join_of resid_ide f by auto
qed
qed
qed
lemma transformation_resid:
shows "transformation (\\⇩A) (\\⇩B) H apex resid"
..
end
text‹
Now we can define the exponential ‹[A, B]› of RTS's ‹A› and ‹B›.
›
locale exponential_rts =
A: weakly_extensional_rts A +
B: extensional_rts B
for A :: "'a resid" (infix "\\⇩A" 70)
and B :: "'b resid" (infix "\\⇩B" 70)
begin
notation A.con (infix "⌢⇩A" 50)
notation A.prfx (infix "≲⇩A" 50)
notation B.con (infix "⌢⇩B" 50)
notation B.join (infix "⊔⇩B" 52)
notation B.prfx (infix "≲⇩B" 50)