Theory Transformer_Semantics.Powerset_Monad

(* 
  Title: The Powerset Monad, State Transformers and Predicate Transformers
  Author: Georg Struth 
  Maintainer: Georg Struth <g.struth@sheffield.ac.uk> 
*)

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

sublocale smap_Sup_lat: Sup_lattice smap sleq sle
  by unfold_locales (simp_all add: sleq_refl sleq_antisym sleq_trans smap_ub smap_lub)

text ‹Hence every complete lattice is an Eilenberg-Moore algebra of $\mathcal{P}$.›

no_notation Sup ("σ")

end


subsection ‹Isomorphism between Kleisli Category and Rel›

text ‹This is again well known---the isomorphism is essentially curry vs uncurry. Kleisli arrows are nondeterministic functions; 
they are also known as state transformers.  Binary relations are very well developed in Isabelle; Kleisli composition of Kleisli 
arrows isn't. Ideally one should therefore use the isomorphism to transport theorems from relations to Kleisli arrows automatically. 
I spell out the isomorphisms and prove that the full quantalic structure, that is, complete lattices plus compositions, 
is preserved by the isomorphisms.›

abbreviation kzero :: "'a  'b set" ("ζ") where
  "ζ  (λx::'a. {})"

text ‹First I define the morphisms. The second one is nothing but the graph of a function.›

definition r2f :: "('a × 'b) set  'a  'b set" ("") where
  " R = Image R  η" 

definition f2r :: "('a  'b set)  ('a × 'b) set" ("") where
  " f = {(x,y). y  f x}"

text ‹The functors form a bijective pair.›

lemma r2f2r_inv1 [simp]: "   = id"
  unfolding f2r_def r2f_def by force

lemma f2r2f_inv2 [simp]: "   = id"
  unfolding f2r_def r2f_def by force

lemma r2f_f2r_galois: "( f = R) = ( R = f)"
  by (force simp: f2r_def r2f_def)

lemma r2f_f2r_galois_var: "(  f = R) = (  R = f)"
  by (force simp: f2r_def r2f_def)

lemma r2f_f2r_galois_var2: "(f   = R) = (R   = f)"
  by (metis (no_types, opaque_lifting) comp_id f2r2f_inv2 map_fun_def o_assoc r2f2r_inv1)

lemma r2f_inj: "inj "
  by (meson inj_on_inverseI r2f_f2r_galois)

lemma f2r_inj: "inj "
  unfolding inj_def using r2f_f2r_galois by metis

lemma r2f_mono: "f g.   f =   g  f = g"
  by (force simp: fun_eq_iff r2f_def)

lemma f2r_mono: "f g.   f =   g  f = g" 
  by (force simp: fun_eq_iff f2r_def)

lemma r2f_mono_iff: "(  f =   g) = (f = g)"
  using r2f_mono by blast

lemma f2r_mono_iff : "(  f =   g) = (f = g)"
  using f2r_mono by blast

lemma r2f_inj_iff: "( f =  g) = (f = g)"
  by (simp add: f2r_inj inj_eq)

lemma f2r_inj_iff: "( R =  S) = (R = S)"
  by (simp add: r2f_inj inj_eq)

lemma r2f_surj: "surj "
  by (metis r2f_f2r_galois surj_def)

lemma f2r_surj: "surj "
  using r2f_f2r_galois by auto

lemma r2f_epi: "f g. f   = g    f = g"
  by (metis r2f_f2r_galois_var2)

lemma f2r_epi: "f g. f   = g    f = g"
  by (metis r2f_f2r_galois_var2)

lemma r2f_epi_iff: "(f   = g  ) = (f = g)"
  using r2f_epi by blast

lemma f2r_epi_iff: "(f   = g  ) = (f = g)"
  using f2r_epi by blast

lemma r2f_bij: "bij "
  by (simp add: bijI r2f_inj r2f_surj)

lemma f2r_bij: "bij "
  by (simp add: bij_def f2r_inj f2r_surj)

text ‹r2f is essentially curry and f2r is uncurry, yet in Isabelle the type of sets and predicates 
(boolean-valued functions) are different. Collect transforms predicates into sets and the following function
sets into predicates:›

abbreviation "s2p X  (λx. x  X)"

lemma r2f_curry: "r2f R = Collect  (curry  s2p) R"
  by (force simp: r2f_def fun_eq_iff curry_def)

lemma f2r_uncurry: "f2r f = (Collect  case_prod) (s2p  f)"
  by (force simp: fun_eq_iff f2r_def)

text ‹Uncurry is case-prod in Isabelle.›

text ‹f2r and r2f preserve the quantalic structures of relations and Kleisli arrows. In particular they are functors.›

lemma r2f_comp_pres: " (R ; S) =  R K  S"
  unfolding fun_eq_iff r2f_def kcomp_def by force

lemma r2f_Id_pres [simp]: " Id = η"
  unfolding fun_eq_iff r2f_def by simp

lemma r2f_Sup_pres: "Sup_pres "
  unfolding fun_eq_iff r2f_def by force

lemma r2f_Sup_pres_var: " (R) = (r  R.  r)" 
  unfolding r2f_def by force

lemma r2f_sup_pres: "sup_pres "
  unfolding r2f_def by force

lemma r2f_Inf_pres: "Inf_pres "
  unfolding fun_eq_iff r2f_def by force

lemma r2f_Inf_pres_var: " (R) = (r  R.  r)" 
  unfolding r2f_def by force

lemma r2f_inf_pres: "inf_pres "
  unfolding r2f_def by force

lemma r2f_bot_pres: "bot_pres "
  by (metis SUP_empty Sup_empty r2f_Sup_pres_var)

lemma r2f_top_pres: "top_pres "
  by (metis Sup_UNIV r2f_Sup_pres_var r2f_surj)

lemma r2f_leq: "(R  S) = ( R   S)"
  by (metis le_iff_sup r2f_f2r_galois r2f_sup_pres)

text ‹Dual statements for f2r hold. Can one automate this?›
 
lemma f2r_kcomp_pres: " (f K g) =  f ;  g"
  by (simp add: r2f_f2r_galois r2f_comp_pres pointfree_idE)

lemma f2r_eta_pres [simp]: " η = Id"
  by (simp add: r2f_f2r_galois) 

lemma f2r_Sup_pres:"Sup_pres "
  by (auto simp: r2f_f2r_galois_var comp_assoc[symmetric] r2f_Sup_pres image_comp)

lemma f2r_Sup_pres_var: " (F) = (f  F.  f)"
  by (simp add: r2f_f2r_galois r2f_Sup_pres_var image_comp)

lemma f2r_sup_pres: "sup_pres "
  by (simp add: r2f_f2r_galois r2f_sup_pres pointfree_idE)

lemma f2r_Inf_pres: "Inf_pres "
  by (auto simp: r2f_f2r_galois_var comp_assoc[symmetric] r2f_Inf_pres image_comp)

lemma f2r_Inf_pres_var: " (F) = (f  F.  f)"
  by (simp add: r2f_f2r_galois r2f_Inf_pres_var image_comp)

lemma f2r_inf_pres: "inf_pres "
  by (simp add: r2f_f2r_galois r2f_inf_pres pointfree_idE)

lemma f2r_bot_pres: "bot_pres "
  by (simp add: r2f_bot_pres r2f_f2r_galois)

lemma f2r_top_pres: "top_pres "
  by (simp add: r2f_f2r_galois r2f_top_pres)

lemma f2r_leq: "(f  g) = ( f   g)"
  by (metis r2f_f2r_galois r2f_leq)

text ‹Relational subidentities are isomorphic to particular Kleisli arrows.›

lemma r2f_Id_on1: " (Id_on X) = (λx. if x  X then {x} else {})"
  by (force simp add: fun_eq_iff r2f_def Id_on_def)

lemma r2f_Id_on2: " (Id_on X) K f = (λx. if x  X then f x else {})"
  unfolding fun_eq_iff Id_on_def r2f_def kcomp_def by auto

lemma r2f_Id_on3: "f K  (Id_on X) = (λx. X  f x)"
  unfolding kcomp_def r2f_def Id_on_def fun_eq_iff by auto


subsection ‹The opposite Kleisli Category›

text ‹Opposition is funtamental for categories; yet hard to realise in Isabelle in general. Due to the access to relations,
the Kleisli category of the powerset functor is an exception.›

notation converse ("")

definition kop :: "('a  'b set)  'b  'a set" ("opK") where
  "opK =   ()  "

text ‹Kop is a contravariant functor.›

lemma kop_contrav: "opK (f K g) = opK g K opK f"
  unfolding kop_def r2f_def f2r_def converse_def kcomp_def fun_eq_iff comp_def by fastforce

lemma kop_func2 [simp]: "opK η = η"
  unfolding kop_def r2f_def f2r_def converse_def comp_def fun_eq_iff by fastforce

lemma converse_idem [simp]: "()  () = id"
  using comp_def by auto

lemma converse_galois: "(()  f = g) = (()  g = f)"
  by auto

lemma converse_galois2: "(f  () = g) = (g  () = f)"
  apply (simp add: fun_eq_iff)
  by (metis converse_converse)

lemma converse_mono_iff: "(()  f = ()  g) = (f = g)"
  using converse_galois by force

lemma converse_epi_iff: "(f  () = g  ()) = (f = g)"
  using converse_galois2 by force

lemma kop_idem [simp]: "opK  opK = id" 
  unfolding kop_def comp_def fun_eq_iff by (metis converse_converse id_apply r2f_f2r_galois)

lemma kop_galois: "(opK f = g) = (opK g = f)"
  by (metis kop_idem pointfree_idE)

lemma kop_galois_var: "(opK  f = g) = (opK  g = f)"
  by (auto simp: kop_def f2r_def r2f_def converse_def fun_eq_iff)   

lemma kop_galois_var2: "(f  opK = g) = (g  opK = f)"
  by (metis (no_types, opaque_lifting) comp_assoc comp_id kop_idem)

lemma kop_inj: "inj opK"
  unfolding inj_def by (simp add: f2r_inj_iff kop_def r2f_inj_iff)

lemma kop_inj_iff: "(opK f = opK g) = (f = g)"
  by (simp add: inj_eq kop_inj)

lemma kop_surj: "surj opK"
  unfolding surj_def by (metis kop_galois)

lemma kop_bij: "bij opK"
  by (simp add: bij_def kop_inj kop_surj)

lemma kop_mono: "(opK  f = opK  g)  (f = g)"
  by (simp add: fun.inj_map inj_eq kop_inj)

lemma kop_mono_iff: "(opK  f = opK  g) = (f = g)"
  using kop_mono by blast

lemma kop_epi: "(f  opK = g  opK)  (f = g)"
  by (metis kop_galois_var2)

lemma kop_epi_iff: "(f  opK = g  opK) = (f = g)"
  using kop_epi by blast

lemma Sup_pres_kop: "Sup_pres opK"
  unfolding kop_def fun_eq_iff comp_def r2f_def f2r_def converse_def by auto

lemma Inf_pres_kop: "Inf_pres opK"
  unfolding kop_def fun_eq_iff comp_def r2f_def f2r_def converse_def by auto

end