Theory Kleisli_Quantaloid
section ‹The Quantaloid of Kleisli Arrows›
theory Kleisli_Quantaloid
imports Kleisli_Transformers
begin
text ‹This component formalises the quantalic structure of Kleisli arrows or state transformers, that is,
the homset of the Kleisli category. Of course, by the previous isomorphisms, this is reflected at least
partially in the Eilenberg-Moore algebras, via the comparison functor. The main result is that Kleisli arrows
form a quantaloid, hence essentially a typed quantale. Some emphasis is on the star. This component thus complements
that in which the quantaloid structure of Sup- and Inf-preserving transformers has been formalised.›
text ‹The first set of lemmas shows that Kleisli arrows form a typed dioid, that is, a typed idempotent semiring.›
lemma ksup_assoc: "((f::'a ⇒ 'b set) ⊔ g) ⊔ h = f ⊔ (g ⊔ h)"
unfolding sup.assoc by simp
lemma ksup_comm: "(f::'a => 'b set) ⊔ g = g ⊔ f"
by (simp add: sup.commute)
lemma ksup_idem [simp]: "(f::'a ⇒ 'b set) ⊔ f = f"
by simp
lemma kcomp_distl: "f ∘⇩K (g ⊔ h) = (f ∘⇩K g) ⊔ (f ∘⇩K h)"
unfolding kcomp_klift fun_eq_iff comp_def sup_fun_def by (simp add: UN_Un_distrib klift_prop)
lemma kcomp_distr: "(f ⊔ g) ∘⇩K h = (f ∘⇩K h) ⊔ (g ∘⇩K h)"
by (simp add: kcomp_klift fun_eq_iff klift_def)
lemma ksup_zerol [simp]: "ζ ⊔ f = f"
by force
lemma ksup_annil [simp]: "ζ ∘⇩K f = ζ"
by (force simp: kcomp_klift klift_def)
lemma ksup_annir [simp]: "f ∘⇩K ζ = ζ"
by (force simp: kcomp_klift klift_def)
text ‹Associativity of Kleisli composition has already been proved.›
text ‹The next laws establish typed quantales --- or quantaloids.›
lemma kSup_distl: "f ∘⇩K (⨆G) = (⨆g ∈ G. f ∘⇩K g)"
proof-
have "f ∘⇩K (⨆G) = ((klift ∘ Sup) G) ∘ f"
by (simp add: kcomp_klift)
also have "... = (⨆g ∈ G. (klift g)) ∘ f"
by (simp add: fbd_Sup_pres fun_eq_iff)
also have "... = (⨆g ∈ G. (klift g) ∘ f)"
by auto
finally show ?thesis
by (simp add: kcomp_klift)
qed
lemma kSup_distr: "(⨆F) ∘⇩K g = (⨆f ∈ F. f ∘⇩K g)"
unfolding kcomp_klift fun_eq_iff comp_def by (simp add: klift_prop)
lemma kcomp_isol: "f ≤ g ⟹ h ∘⇩K f ≤ h ∘⇩K g"
by (force simp: kcomp_klift le_fun_def klift_def)
lemma kcomp_isor: "f ≤ g ⟹ f ∘⇩K h ≤ g ∘⇩K h"
by (force simp: kcomp_klift le_fun_def klift_def)
subsection ‹Kleene Star›
text ‹The Kleene star can be defined in any quantale or quantaloid by iteration. For Kleisli arrows,
laws for the star can be obtained via the isomorphism to binary relations, where the star is the reflexive-transitive
closure operation.›
abbreviation "kpower ≡ kmon.power"
lemma r2f_pow: "ℱ (R ^^ i) = kpower (ℱ R) i"
by (induct i, simp, metis power.power.power_Suc r2f_comp_pres relpow.simps(2) relpow_commute)
lemma f2r_kpower: "ℛ (kpower f i) = (ℛ f) ^^ i"
by (induct i, simp, metis f2r2f_inv2 pointfree_idE r2f2r_inv1 r2f_pow)
definition "kstar f = (⨆i. kpower f i)"
lemma r2f_rtrancl_hom: "ℱ (rtrancl R) = kstar (ℱ R)"
proof-
have "ℱ (rtrancl R) = ℱ (⋃i. R ^^ i)"
by (simp add: full_SetCompr_eq rtrancl_is_UN_relpow)
also have "... = (⨆i. kpower (ℱ R) i)"
by (auto simp: r2f_Sup_pres_var r2f_pow)
finally show ?thesis
by (simp add: kstar_def)
qed
lemma r2f_rtrancl_hom_var: "ℱ ∘ rtrancl = kstar ∘ ℱ"
by standard (simp add: r2f_rtrancl_hom)
lemma f2r_kstar_hom: "ℛ (kstar f) = rtrancl (ℛ f)"
by (metis r2f_f2r_galois r2f_rtrancl_hom)
lemma f2r_kstar_hom_var: "ℛ ∘ kstar = rtrancl ∘ ℛ"
by standard (simp add: f2r_kstar_hom)
lemma kstar_unfoldl_eq: "η ⊔ f ∘⇩K kstar f = kstar f"
proof -
have "ℛ (kstar f) = (ℛ η) ∪ (ℛ f)⇧* ; ℛ f"
using f2r_kstar_hom rtrancl_unfold
by (metis f2r_eta_pres)
thus ?thesis
by (metis f2r_kcomp_pres f2r_kstar_hom f2r_sup_pres r2f_inj_iff r_comp_rtrancl_eq)
qed
lemma kstar_unfoldl: "η ⊔ f ∘⇩K kstar f ≤ kstar f"
by (simp add: kstar_unfoldl_eq)
lemma kstar_unfoldr_eq: "η ⊔ (kstar f) ∘⇩K f = kstar f"
by (metis (no_types) f2r2f_inv2 f2r_kcomp_pres f2r_kstar_hom kstar_unfoldl_eq pointfree_idE r_comp_rtrancl_eq)
lemma kstar_unfoldr: "η ⊔ (kstar f) ∘⇩K f ≤ kstar f"
by (simp add: kstar_unfoldr_eq)
text ‹Relational induction laws seem to be missing in Isabelle Main. So I derive functional laws directly.›
lemma kpower_inductl: "f ∘⇩K g ≤ g ⟹ kpower f i ∘⇩K g ≤ g"
by (induct i, simp_all add: kcomp_assoc kcomp_isol order_subst2)
lemma kpower_inductl_var: "h ⊔ f ∘⇩K g ≤ g ⟹ kpower f i ∘⇩K h ≤ g"
proof -
assume h1: "h ⊔ f ∘⇩K g ≤ g"
then have h2: "f ∘⇩K g ≤ g"
using le_sup_iff by blast
have "h ≤ g"
using h1 by simp
then show ?thesis
using h2 kcomp_isol kpower_inductl order_trans by blast
qed
lemma kstar_inductl: "h ⊔ f ∘⇩K g ≤ g ⟹ kstar f ∘⇩K h ≤ g"
apply (simp add: kstar_def kSup_distr, rule Sup_least)
using kpower_inductl_var by fastforce
lemma kpower_inductr: "g ∘⇩K f ≤ g ⟹ g ∘⇩K kpower f i ≤ g"
apply (induct i, simp_all)
by (metis (mono_tags, lifting) dual_order.trans kcomp_assoc kcomp_isor)
lemma kpower_inductr_var: "h ⊔ g ∘⇩K f ≤ g ⟹ h ∘⇩K kpower f i ≤ g"
by (metis (no_types) dual_order.trans kcomp_isor kpower_inductr le_sup_iff)
lemma kstar_inductr: "h ⊔ g ∘⇩K f ≤ g ⟹ h ∘⇩K kstar f ≤ g"
apply (simp add: kstar_def kSup_distl, rule Sup_least)
using kpower_inductr_var by fastforce
lemma kpower_prop: "f ≤ η ⟹ kpower f i ≤ η"
by (metis kcomp_idl kpower_inductr)
lemma kstar_prop: "f ≤ η ⟹ kstar f ≤ η"
by (simp add: SUP_le_iff kpower_prop kstar_def)
subsection ‹Antidomain›
text ‹Next I define an antidomain operation and prove the axioms of antidomain semirings~\<^cite>‹"GomesGHSW16" and "DesharnaisS11"›.›
definition "kad f = (λx. if (f x = {}) then {x} else {})"
definition "ad_rel R = {(x,x) |x. ¬(∃y. (x,y) ∈ R)}"
lemma f2r_ad_fun_hom: "ℛ (kad f) = ad_rel (ℛ f)"
apply (simp add: kad_def ad_rel_def f2r_def, safe)
by simp_all (meson empty_iff singletonD)
lemma f2r_ad_fun_hom_var:"ℛ ∘ kad = ad_rel ∘ ℛ"
by standard (simp add: f2r_ad_fun_hom)
lemma r2f_ad_rel_hom: "ℱ (ad_rel R) = kad (ℱ R)"
by (force simp add: kad_def ad_rel_def r2f_def fun_eq_iff)
lemma r2f_ad_rel_hom_var:"ℱ ∘ ad_rel = kad ∘ ℱ"
by standard (simp add: r2f_ad_rel_hom)
lemma ad_fun_as1 [simp]: "(kad f) ∘⇩K f = ζ"
by (simp add: kad_def kcomp_def fun_eq_iff)
lemma ad_fun_as2 [simp]: "kad (f ∘⇩K g) ⊔ kad (f ∘⇩K kad (kad g)) = kad (f ∘⇩K kad (kad g))"
by (force simp: kad_def kcomp_def fun_eq_iff)
lemma ad_fun_as3 [simp]: "kad (kad f) ⊔ kad f = η"
by (simp add: kad_def fun_eq_iff)
definition "set2fun X = (λx. if (x ∈ X) then {x} else {})"
definition "p2fun = set2fun ∘ Collect"
lemma ffb_ad_fun: "fb⇩ℱ f X = {x. (kad (f ∘⇩K kad (set2fun X))) x ≠ {}}"
unfolding ffb_prop_var klift_def kop_def fun_eq_iff comp_def f2r_def r2f_def converse_def kad_def kcomp_def set2fun_def
by auto
lemma ffb_ad_fun2: "set2fun (fb⇩ℱ f X) = kad (f ∘⇩K kad (set2fun X))"
by standard (subst ffb_ad_fun, subst set2fun_def, simp add: kad_def)
text ‹The final statements check that the relational forward diamond is consistent with the Kleene-algebraic definition.›
lemma fb_ad_rel: "fb⇩ℛ R X = Domain (ad_rel (R ; ad_rel (Id_on X)))"
unfolding rfb_def ffb_prop_var klift_def comp_def r2f_def kop_def f2r_def converse_def Domain_def Id_on_def ad_rel_def
by auto
lemma fb_ad_rel2: "Id_on (fb⇩ℛ R X) = ad_rel (R ; ad_rel (Id_on X))"
unfolding rfb_def ffb_prop_var klift_def comp_def r2f_def kop_def f2r_def converse_def Domain_def Id_on_def ad_rel_def
by auto
end