Theory Powerset_Monad
section ‹The Powerset Monad, State Transformers and Predicate Transformers›
theory Powerset_Monad
imports "Order_Lattice_Props.Order_Lattice_Props"
begin
notation relcomp (infixl ‹;› 75)
and image (‹𝒫›)
subsection ‹The Powerset Monad›
text ‹First I recall functoriality of the powerset functor.›
lemma P_func1: "𝒫 (f ∘ g) = 𝒫 f ∘ 𝒫 g"
unfolding fun_eq_iff by force
lemma P_func2: "𝒫 id = id"
by simp
text ‹Isabelle' type systems doesn't allow formalising arbitrary monads, but instances such as the powerset monad
can still be developed.›
abbreviation eta :: "'a ⇒ 'a set" (‹η›) where
"η ≡ (λx. {x})"
abbreviation mu :: "'a set set ⇒ 'a set" (‹μ›) where
"μ ≡ Union"
text ‹$\eta$ and $\mu$ are natural transformations.›
lemma eta_nt: "𝒫 f ∘ η = η ∘ id f"
by fastforce
lemma mu_nt: "μ ∘ (𝒫 ∘ 𝒫) f = (𝒫 f) ∘ μ"
by fastforce
text ‹They satisfy the following coherence conditions. Explicit typing clarifies that $\eta$ and $\mu$ have different type in these expressions.›
lemma pow_assoc: "(μ::'a set set ⇒ 'a set) ∘ 𝒫 (μ::'a set set ⇒ 'a set) = (μ ::'a set set ⇒ 'a set) ∘ (μ::'a set set set ⇒ 'a set set)"
using fun_eq_iff by fastforce
lemma pow_un1: "(μ::'a set set ⇒ 'a set) ∘ (𝒫 (η:: 'a ⇒ 'a set)) = (id::'a set ⇒ 'a set)"
using fun_eq_iff by fastforce
lemma pow_un2: "(μ::'a set set ⇒ 'a set) ∘ (η::'a set ⇒ 'a set set) = (id::'a set ⇒ 'a set)"
using fun_eq_iff by fastforce
text ‹Thus the powerset monad is indeed a monad.›
subsection ‹Kleisli Category of the Powerset Monad›
text ‹Next I define the Kleisli composition and Kleisli lifting (Kleisli extension) of Kleisli arrows.
The Kleisli lifting turns Kleisli arrows into forward predicate transformers.›
definition kcomp :: "('a ⇒ 'b set) ⇒ ('b ⇒ 'c set) ⇒ ('a ⇒ 'c set)" (infixl ‹∘⇩K› 75) where
"f ∘⇩K g = μ ∘ 𝒫 g ∘ f"
lemma kcomp_prop: "(f ∘⇩K g) x = (⨆y ∈ f x. g y)"
by (simp add: kcomp_def)
definition klift :: "('a ⇒ 'b set) ⇒ 'a set ⇒ 'b set" (‹_⇧†› [101] 100) where
"f⇧† = μ ∘ 𝒫 f"
lemma klift_prop: "(f⇧†) X = (⨆x ∈ X. f x)"
by (simp add: klift_def)
lemma kcomp_klift: "f ∘⇩K g = g⇧† ∘ f"
unfolding kcomp_def klift_def by simp
lemma klift_prop1: "(f⇧† ∘ g)⇧† = f⇧† ∘ g⇧†"
unfolding fun_eq_iff klift_def by simp
lemma klift_eta_inv1 [simp]: "f⇧† ∘ η = f"
unfolding fun_eq_iff klift_def by simp
lemma klift_eta_pres [simp]: "η⇧† = (id::'a set ⇒ 'a set)"
unfolding fun_eq_iff klift_def by simp
lemma klift_id_pres [simp]: "id⇧† = μ"
unfolding klift_def by simp
lemma kcomp_assoc: "(f ∘⇩K g) ∘⇩K h = f ∘⇩K (g ∘⇩K h)"
unfolding kcomp_klift klift_prop1 by force
lemma kcomp_idl [simp]: "η ∘⇩K f = f"
unfolding kcomp_klift by simp
lemma kcomp_idr [simp]: "f ∘⇩K η = f"
unfolding kcomp_klift by simp
text ‹In the following interpretation statement, types are restricted.
This is needed for defining iteration.›
interpretation kmon: monoid_mult "η" "(∘⇩K)"
by unfold_locales (simp_all add: kcomp_assoc)
text ‹Next I show that $\eta$ is a (contravariant) functor from Set into the Kleisli category of the powerset monad.
It simply turns functions into Kleisli arrows.›
lemma eta_func1: "η ∘ (f ∘ g) = (η ∘ g) ∘⇩K (η ∘ f)"
unfolding fun_eq_iff kcomp_def by simp
subsection ‹Eilenberg-Moore Algebra›
text ‹It is well known that the Eilenberg-Moore algebras of the powerset monad form complete join semilattices (hence Sup-lattices).›
text ‹First I verify that every complete lattice with structure map Sup satisfies the laws of Eilenberg-Moore algebras.›
notation Sup (‹σ›)
lemma em_assoc [simp]: "σ ∘ 𝒫 (σ::'a::complete_lattice set ⇒ 'a) = σ ∘ μ"
apply (standard, rule antisym)
apply (simp add: SUP_least Sup_subset_mono Sup_upper)
by (metis (no_types, lifting) SUP_upper2 Sup_least Sup_upper UnionE comp_def)
lemma em_id [simp]: "σ ∘ η = (id::'a::complete_lattice ⇒ 'a)"
by (simp add: fun_eq_iff)
text‹Hence every Sup-lattice is an Eilenberg-Moore algebra for the powerset monad.
The morphisms between Eilenberg-Moore algebras of the powerset monad are Sup-preserving maps.
In particular, powersets with structure map $\mu$ form an Eilenberg-Moore algebra (in fact the free one):›
lemma em_mu_assoc [simp]: "μ ∘ 𝒫 μ = μ ∘ μ"
by simp
lemma em_mu_id [simp]: "μ ∘ η = id"
by simp
text ‹Next I show that every Eilenberg-Moore algebras for the
powerset functor is a Sup-lattice.›
class eilenberg_moore_pow =
fixes smap :: "'a set ⇒ 'a"
assumes smap_assoc: "smap ∘ 𝒫 smap = smap ∘ μ"
and smap_id: "smap ∘ η = id"
begin
definition "sleq = (λx y. smap {x,y} = y)"
definition "sle = (λx y. sleq x y ∧ y ≠ x)"
lemma smap_un1: "smap {x, smap Y} = smap ({x} ∪ Y)"
proof-
have "smap {x, smap Y} = smap {smap {x}, smap Y}"
by (metis comp_apply id_apply smap_id)
also have "... = (smap ∘ 𝒫 smap) {{x}, Y}"
by simp
finally show ?thesis
using local.smap_assoc by auto
qed
lemma smap_comm: "smap {x, smap Y} = smap {smap Y, x}"
by (simp add: insert_commute)
lemma smap_un2: "smap {smap X, y} = smap (X ∪ {y})"
using smap_comm smap_un1 by auto
lemma sleq_refl: "sleq x x"
by (metis id_apply insert_absorb2 local.smap_id o_apply sleq_def)
lemma sleq_trans: "sleq x y ⟹ sleq y z ⟹ sleq x z"
by (metis (no_types, lifting) sleq_def smap_un1 smap_un2 sup_assoc)
lemma sleq_antisym: "sleq x y ⟹ sleq y x ⟹ x = y"
by (simp add: insert_commute sleq_def)
lemma smap_ub: "x ∈ A ⟹ sleq x (smap A)"
using insert_absorb sleq_def smap_un1 by fastforce
lemma smap_lub: "(⋀x. x ∈ A ⟹ sleq x z) ⟹ sleq (smap A) z"
proof-
assume h: "⋀x. x ∈ A ⟹ sleq x z"
have "smap {smap A, z} = smap (A ∪ {z})"
by (simp add: smap_un2)
also have "... = smap ((⋃x ∈ A. {x,z}) ∪ {z})"
by (rule_tac f=smap in arg_cong, auto)
also have "... = smap {(smap ∘ μ) {{x,z} |x. x ∈ A}, z}"
by (simp add: Setcompr_eq_image smap_un2)
also have "... = smap {(smap ∘ 𝒫 smap) {{x,z} |x. x ∈ A}, z}"
by (simp add: local.smap_assoc)
also have "... = smap {smap {smap {x,z} |x. x ∈ A}, z}"
by (simp add: Setcompr_eq_image image_image)
also have "... = smap {smap {z |x. x ∈ A}, z}"
by (metis h sleq_def)
also have "... = smap ({z |x. x ∈ A} ∪ {z})"
by (simp add: smap_un2)
also have "... = smap {z}"
by (rule_tac f=smap in arg_cong, auto)
finally show ?thesis
using sleq_def sleq_refl by auto
qed