Theory Transformer_Semantics.Kleisli_Transformers

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

section ‹State Transformers and Predicate Transformers Based on the Powerset Monad›

theory Kleisli_Transformers

imports Powerset_Monad 
        Sup_Inf_Preserving_Transformers
begin          


subsection ‹Backward Diamonds from Kleisli Arrows›

text ‹First I verify the embedding of the Kleisli category of the powerset functor into its Eilenberg-Moore category. 
This functor maps sets to their mus and functions to their Kleisli liftings. But this is just functoriality of dagger!. 
I model it as a backward diamond operator in the sense of dynamic logic. It corresponds to a strongest postcondition 
operator. In the parlance of program semantics, this is an embedding of state into prediate transformers.›

notation klift (‹bdℱ›)

text ‹bd stands for backward diamond, the index indicates the setting of Kleisli arrows or nondeterministic 
functions. ifbd is its inverse.›

abbreviation ifbd :: "('a set ⇒ 'b set) ⇒ 'a ⇒ 'b set" (‹bd-ℱ›) where 
  "bd-ℱ ≡ (λφ. φ ∘ η)"

lemma fbd_set: "bdℱ f X = {y. ∃x. y ∈ f x ∧ x ∈ X}"
  by (force simp: klift_prop) 
 
lemma ifbd_set: "bd-ℱ φ x = {y. y ∈ φ {x}}"
  by simp

text ‹The two functors form a bijective pair.›

lemma fbd_ifbd_inv2: "Sup_pres φ ⟹ (bdℱ ∘ bd-ℱ) φ = φ" 
proof -
  assume h: "Sup_pres φ"
  have "(bdℱ ∘ bd-ℱ) φ = Sup ∘ 𝒫 (φ ∘ η)"
    unfolding klift_def by simp
  also have "... = Sup ∘ 𝒫 φ ∘ 𝒫 η"
    by (simp add: comp_assoc P_func1)
  also have "... = φ ∘ Sup ∘ 𝒫 η"
    by (simp add: h)
  also have "... = φ ∘ id"
    by force
  finally show ?thesis
    by simp
qed

lemma fbd_ifbd_inv2_inv: "(bdℱ ∘ bd-ℱ) φ = φ ⟹ Sup_pres φ" 
  unfolding fun_eq_iff comp_def by (metis (no_types, lifting) Inf.INF_cong UN_extend_simps(8) klift_prop)

lemma fbd_ifbd_inv2_iff: "((bdℱ ∘ bd-ℱ) φ = φ) = (Sup_pres φ)"
  using fbd_ifbd_inv2 fbd_ifbd_inv2_inv by force

lemma fbd_inj: "inj bdℱ"
  by (meson inj_on_inverseI klift_eta_inv1)

lemma fbd_inj_iff: "(bdℱ f = bdℱ g) = (f = g)"
  by (meson injD fbd_inj)

lemma ifbd_inj: "Sup_pres φ ⟹ Sup_pres ψ ⟹ bd-ℱ φ = bd-ℱ ψ ⟹ φ = ψ"
proof-
  assume h1: "Sup_pres φ"
  and h2: "Sup_pres ψ" 
  and "bd-ℱ φ = bd-ℱ ψ"
  hence "(bdℱ ∘ bd-ℱ) φ = (bdℱ ∘ bd-ℱ) ψ"
    by simp
  thus ?thesis
    by (metis h1 h2 fbd_ifbd_inv2)
qed

lemma ifbd_inj_iff: "Sup_pres φ ⟹ Sup_pres ψ ⟹ (bd-ℱ φ = bd-ℱ ψ) = (φ = ψ)"
  using ifbd_inj by force

lemma fbd_ifbd_galois: "Sup_pres φ ⟹ (bd-ℱ φ = f) = (bdℱ f = φ)"
  using fbd_ifbd_inv2 by force

lemma fbd_surj: "Sup_pres φ ⟹ (∃f. bdℱ f = φ)"
  using fbd_ifbd_inv2 by auto 

lemma ifbd_surj: "surj bd-ℱ"
  unfolding surj_def by (metis klift_eta_inv1)

text ‹In addition they preserve the Sup-quantale structure of the powerset algebra. This means that
morphisms preserve compositions, units and Sups, but not Infs, hence also bottom but not top.›

lemma fbd_comp_pres: "bdℱ (f ∘K g) = bdℱ g ∘ bdℱ f"
  unfolding kcomp_klift klift_prop1 by simp

lemma fbd_Sup_pres: "Sup_pres bdℱ"
  by (force simp: fun_eq_iff klift_def)

lemma fbd_sup_pres: "sup_pres bdℱ"
  using Sup_sup_pres fbd_Sup_pres by blast

lemma fbd_Disj: "Sup_pres (bdℱ f)"
  by (simp add: fbd_ifbd_inv2_inv)

lemma fbd_disj: "sup_pres (bdℱ f)"
  by (simp add: klift_prop)

lemma fbd_bot_pres: "bot_pres bdℱ"
  unfolding klift_def by fastforce

lemma fbd_zero_pres2 [simp]: "bdℱ f {} = {}"
  by (simp add: klift_prop)

lemma fbd_iso: "X ⊆ Y ⟶ bdℱ f X ⊆ bdℱ f Y"
  by (metis fbd_disj le_iff_sup)

text ‹The following counterexamples show that Infs are not preserved.›

lemma "top_pres bdℱ" (*nitpick*)
  oops

lemma "inf_pres bdℱ" (*nitpick*)
  oops

text ‹Dual preservation statements hold for ifbd ... and even Inf-preservation.›

lemma ifbd_comp_pres: "Sup_pres φ ⟹ bd-ℱ (φ ∘ ψ) = bd-ℱ ψ ∘K bd-ℱ φ"
  by (smt fbd_ifbd_galois fun.map_comp kcomp_def klift_def)

lemma ifbd_Sup_pres: "Sup_pres bd-ℱ"   
  by (simp add: fun_eq_iff)

lemma ifbd_sup_pres: "sup_pres bd-ℱ"
  by force

lemma ifbd_Inf_pres: "Inf_pres bd-ℱ"
  by (simp add: fun_eq_iff)

lemma ifbd_inf_pres: "inf_pres bd-ℱ"
  by force

lemma ifbd_bot_pres: "bot_pres bd-ℱ"
  by auto

lemma ifbd_top_pres: "top_pres bd-ℱ"
  by auto

text ‹Preservation of units by the Kleisli lifting has been proved in klift-prop3.›

text ‹These results estabilish the isomorphism between state and predicate transformers given by backward diamonds.
The isomorphism preserves the Sup-quantale structure, but not Infs.›
 


subsection ‹Backward Diamonds from Relations›

text ‹Using the isomorphism between binary relations and Kleisli arrows (or state transformers), it is straightforward
to define backward diamonds from relations, by composing isomorphisms. It follows that Sup-quantales of binary relations 
(under relational composition, the identity relation and Sups) are isomorphic to the Sup-quantales of predicate transformers.
Once again, Infs are not preserved.›

definition rbd :: "('a × 'b) set ⇒ 'a set ⇒ 'b set"  (‹bdℛ›) where
  "bdℛ = bdℱ ∘ ℱ"

definition irbd :: "('a set ⇒ 'b set) ⇒ ('a × 'b) set"  (‹bd-ℛ›) where
  "bd-ℛ = ℛ ∘ bd-ℱ"

lemma rbd_Im: "bdℛ = (``)"
  unfolding rbd_def klift_def r2f_def fun_eq_iff by force

lemma rbd_set: "bdℛ R X = {y. ∃x ∈ X. (x,y) ∈ R}"
  by (force simp: rbd_Im Image_def)
  
lemma irbd_set: "bd-ℛ φ = {(x,y). y ∈ (φ ∘ η) x}"
  by (simp add: irbd_def f2r_def o_def)

lemma irbd_set_var: "bd-ℛ φ = {(x,y). y ∈ φ {x}}"
  by (simp add: irbd_def f2r_def o_def)

lemma rbd_irbd_inv1 [simp]: "bd-ℛ ∘ bdℛ = id"
  by (metis (no_types, lifting) comp_eq_dest_lhs eq_id_iff fbd_Disj fbd_ifbd_galois irbd_def r2f_f2r_galois rbd_def)

lemma irbd_rbd_inv2: "Sup_pres φ ⟹ (bdℛ ∘ bd-ℛ) φ = φ"
  by (metis comp_apply fbd_ifbd_galois irbd_def r2f_f2r_galois rbd_def)

lemma irbd_rbd_inv2_inv: "(bdℛ ∘ bd-ℛ) φ = φ ⟹ Sup_pres φ"
  by (simp add: rbd_def irbd_def, metis fbd_Disj)

lemma irbd_rbd_inv2_iff: "((bdℛ ∘ bd-ℛ) φ = φ) = (Sup_pres φ)"
  using irbd_rbd_inv2 irbd_rbd_inv2_inv by blast

lemma rbd_inj: "inj bdℛ"
  by (simp add: fbd_inj inj_compose r2f_inj rbd_def)

lemma rbd_translate: "(bdℛ R = bdℛ S) = (R = S)"
  by (simp add: rbd_inj inj_eq)

lemma irbd_inj: "Sup_pres φ ⟹ Sup_pres ψ ⟹ bd-ℛ φ = bd-ℛ ψ ⟹ φ = ψ"
  by (metis rbd_Im comp_eq_dest_lhs irbd_rbd_inv2)

lemma irbd_inj_iff: "Sup_pres φ ⟹ Sup_pres ψ ⟹ (bd-ℛ φ = bd-ℛ ψ) = (φ = ψ)"
  using irbd_inj by force

lemma rbd_surj: "Sup_pres φ ⟹ (∃R. bdℛ R = φ)"
  using irbd_rbd_inv2 by force

lemma irbd_surj: "surj bd-ℛ"
  by (metis UNIV_I fun.set_map imageE rbd_irbd_inv1 surj_def surj_id)

lemma rbd_irbd_galois: "Sup_pres φ ⟹ (φ = bdℛ R) = (R = bd-ℛ φ)"
  by (smt comp_apply fbd_ifbd_galois irbd_def r2f_f2r_galois rbd_def)

lemma rbd_comp_pres: "bdℛ (R ; S) = bdℛ S ∘ bdℛ R"
  by (simp add: rbd_def r2f_comp_pres fbd_comp_pres)

lemma rbd_Id_pres: "bdℛ Id = id"
  unfolding rbd_def by simp

lemma rbd_Un_pres: "Sup_pres bdℛ"
  by (simp add: rbd_def Sup_pres_comp fbd_Sup_pres r2f_Sup_pres)

lemma rbd_un_pres: "sup_pres bdℛ"
  by (simp add: rbd_def fbd_sup_pres r2f_sup_pres)

lemma "inf_pres bdℛ" (*nitpick*)
  oops

lemma rbd_disj: "Sup_pres (bdℛ R)"
  by (simp add: rbd_def fbd_Disj)

lemma rbd_disj2: "sup_pres (bdℛ R)"
  by (simp add: Image_Un rbd_Im)

lemma rbd_bot_pres: "bot_pres bdℛ"
  by (simp add: fbd_bot_pres r2f_bot_pres rbd_def)

lemma rbd_zero_pres2 [simp]: "bdℛ R {} = {}"
  by (simp add: rbd_Im)

lemma rbd_univ: "bdℛ R UNIV = Range R"
  unfolding rbd_def fun_eq_iff klift_def r2f_def by force

lemma rbd_iso: "X ⊆ Y ⟹ bdℛ R X ⊆ bdℛ R Y"
  by (metis le_iff_sup rbd_disj2)

lemma irbd_comp_pres: "Sup_pres φ ⟹ bd-ℛ (φ ∘ ψ) = bd-ℛ ψ ; bd-ℛ φ"
  by (simp add: ifbd_comp_pres f2r_kcomp_pres irbd_def)

lemma irbd_id_pres [simp]: "bd-ℛ id = Id"
  unfolding irbd_def by simp

lemma irbd_Sup_pres: "Sup_pres bd-ℛ"
  by (simp add: irbd_def Sup_pres_comp ifbd_Sup_pres f2r_Sup_pres)

lemma irbd_sup_pres: "sup_pres bd-ℛ"
  by (simp add: irbd_def ifbd_sup_pres f2r_sup_pres)  

lemma irbd_Inf_pres: "Inf_pres bd-ℛ"
  by (auto simp: fun_eq_iff irbd_def f2r_def)

lemma irbd_inf_pres: "inf_pres bd-ℛ"
  by (auto simp: fun_eq_iff irbd_def f2r_def)

lemma irbd_bot_pres: "bot_pres bd-ℛ"
  by (metis comp_def ifbd_bot_pres f2r_bot_pres irbd_def)

text ‹This shows that relations are isomorphic to disjunctive forward predicate transformers. In many cases Isabelle picks up
the composition of morphisms in proofs.›


subsection ‹Forward Boxes on Kleisli Arrows›

text ‹Forward box operators correspond to weakest liberal preconditions in program semantics. Here, 
Kleisli arrows are mapped to the opposite of the Eilenberg-Moore category, that is, Inf-lattices. 
It follows that the Inf-quantale structure is preserved. Modelling opposition is based on the fact 
that Kleisli arrows can be swapped by going through relations.›

definition ffb :: "('a ⇒ 'b set) ⇒ 'b set ⇒ 'a set" (‹fbℱ›) where
  "fbℱ = ∂F ∘ bdℱ ∘ opK" 

text ‹Here, $\partial_F$ is map-dual, which amounts to De Morgan duality. Hence the forward box operator is
obtained from the backward diamond by taking the opposite Kleisli arrow, applying the backward diamond, and then De Morgan
duality.›

lemma ffb_prop: "fbℱ f = ∂ ∘ bdℱ (opK f) ∘ ∂"
  by (simp add: ffb_def map_dual_def)

lemma ffb_prop_var: "fbℱ f = uminus ∘ bdℱ (opK f) ∘ uminus"
  by (simp add: dual_set_def ffb_prop)
 
lemma ffb_fbd_dual: "∂ ∘ fbℱ f = bdℱ (opK f) ∘ ∂"
  by (simp add: ffb_prop o_assoc)

text ‹I give a set-theoretic definition of iffb, because the algebraic one below depends on Inf-preservation.›

definition iffb :: "('b set ⇒ 'a set) ⇒ 'a ⇒ 'b set" (‹fb-ℱ›) where
  "fb-ℱ φ = (λx. ⋂{X. x ∈ φ X})"

lemma ffb_set: "fbℱ f = (λY. {x. f x ⊆ Y})" 
  by (force simp: fun_eq_iff ffb_prop_var kop_def klift_def f2r_def r2f_def)

text ‹Forward boxes and backward diamonds are adjoints.›

lemma ffb_fbd_galois: "(bdℱ f) ⊣ (fbℱ f)"
  unfolding adj_def ffb_set klift_prop by blast

lemma iffb_inv1: "fb-ℱ ∘ fbℱ = id"
  unfolding fun_eq_iff ffb_set iffb_def by force

lemma iffb_inv2_aux: "Inf_pres φ ⟹ ⨅{X. x ∈ φ X} ⊆ Y ⟹ x ∈ φ Y"
proof-
  assume "Inf_pres φ"
    and h1: "⨅{X. x ∈ φ X} ⊆ Y"
  hence h2: "∀X. φ (⨅X) = (⋂x ∈ X. φ x)"
    by (metis comp_eq_dest)
  hence "φ (⨅{X. x ∈ φ X}) ⊆ φ Y"
    by (metis h1 INF_lower2 cInf_eq_minimum mem_Collect_eq order_refl)
  hence "(⨅{φ X |X. x ∈ φ X}) ⊆ φ Y" 
    by (metis h2 setcompr_eq_image)
  thus ?thesis
    by (force simp add: subset_iff)
qed

lemma iffb_inv2: "Inf_pres φ ⟹ (fbℱ ∘ fb-ℱ) φ = φ"
proof-
  assume h: "Inf_pres φ"
  {fix Y
  have "(fbℱ ∘ fb-ℱ) φ Y = {x. ⨅{X. x ∈ φ X} ⊆ Y}"
    by (simp add: ffb_set iffb_def)
  hence "⋀x. x ∈ (fbℱ ∘ fb-ℱ) φ Y ⟷ ⨅{X. x ∈ φ X} ⊆ Y"
    by auto
  hence "⋀x. x ∈ (fbℱ ∘ fb-ℱ) φ Y ⟷ x ∈ φ Y" 
    by (auto simp: h iffb_inv2_aux)
  hence  "(fbℱ ∘ fb-ℱ) φ Y = φ Y"
    by (simp add: fun_eq_iff set_eq_iff)}
  thus ?thesis
    unfolding fun_eq_iff by simp
qed

lemma iffb_inv2_inv: "(fbℱ ∘ fb-ℱ) φ = φ ⟹ Inf_pres φ"
  by (auto simp: fun_eq_iff ffb_set iffb_def)

lemma iffb_inv2_iff: "((fbℱ ∘ fb-ℱ) φ = φ) = (Inf_pres φ)"
  using iffb_inv2 iffb_inv2_inv by blast

lemma ffb_inj: "inj fbℱ"
  unfolding inj_def by (metis iffb_inv1 pointfree_idE)

lemma ffb_inj_iff: "(fbℱ f = fbℱ g) = (f = g)"
  by (simp add: ffb_inj inj_eq)

lemma ffb_iffb_galois: "Inf_pres φ ⟹ (fb-ℱ φ = f) = (fbℱ f = φ)"
  using ffb_inj_iff iffb_inv2 by force

lemma iffb_inj: "Inf_pres φ ⟹ Inf_pres ψ ⟹ fb-ℱ φ = fb-ℱ ψ  ⟹ φ = ψ"
  by (metis ffb_iffb_galois)

lemma iffb_inj_iff: "Inf_pres φ ⟹ Inf_pres ψ ⟹ (fb-ℱ φ = fb-ℱ ψ) = (φ = ψ)"
  using iffb_inj by blast

lemma ffb_surj: "Inf_pres φ  ⟹ (∃f. fbℱ f = φ)"
  using iffb_inv2 by auto

lemma iffb_surj: "surj fb-ℱ" 
  using surj_def by (metis comp_apply iffb_inv1 surj_id) 

text ‹This is now the explicit "definition" of iffb, for Inf-preserving transformers.›

lemma iffb_ifbd_dual: "Inf_pres φ ⟹ fb-ℱ φ = (opK ∘ bd-ℱ ∘ ∂F) φ" 
proof-
  assume h: "Inf_pres φ"
  {fix f
    have "(fb-ℱ φ = f) = ((∂F ∘ bdℱ ∘ opK) f = φ)"
      by (simp add: ffb_def ffb_iffb_galois h)
    also have "... = (opK f = (bd-ℱ ∘ ∂F) φ)"
      by (metis (mono_tags, lifting) comp_apply map_dual_dual ffb_def ffb_surj h klift_eta_inv1 map_dual_dual)
    finally have "(fb-ℱ φ = f) = (f = (opK ∘ bd-ℱ ∘ ∂F) φ)"
      using kop_galois by auto}
  thus ?thesis
    by blast
qed

lemma fbd_ffb_dual: "∂F ∘ fbℱ ∘ opK = bdℱ"
proof-
  have "∂F ∘ fbℱ ∘ opK = ∂F ∘ ∂F ∘ bdℱ ∘ (opK ∘ opK)"
    by (simp add: comp_def ffb_def)
  thus ?thesis
    by simp
qed

lemma ffbd_ffb_dual_var: "∂ ∘ bdℱ f = fbℱ (opK f) ∘ ∂"
  by (metis ffb_prop fun_dual1 kop_galois)

lemma ifbd_iffb_dual: "Sup_pres φ ⟹ bd-ℱ φ = (opK ∘ fb-ℱ ∘ ∂F) φ" 
proof-
  assume h: "Sup_pres φ"
  hence "Inf_pres (∂F φ)"
    using Sup_pres_Inf_pres by blast
  hence "(opK ∘ fb-ℱ ∘ ∂F) φ = (opK ∘ (opK ∘ bd-ℱ ∘ ∂F) ∘ ∂F) φ"
    by (simp add: iffb_ifbd_dual)
  thus ?thesis
    by (metis comp_def kop_galois map_dual_dual)
qed

lemma ffb_kcomp_pres: "fbℱ (f ∘K g) = fbℱ f ∘ fbℱ g"
proof-
  have "fbℱ (f ∘K g) = ∂F (bdℱ (opK (f ∘K g)))"
    by (simp add: ffb_def)
  also have "... = ∂F (bdℱ (opK g ∘K opK f))"
    by (simp add: kop_contrav)
  also have "... = ∂F (bdℱ (opK f) ∘ bdℱ (opK g))"
    by (simp add: fbd_comp_pres)
  also have "... = ∂F (bdℱ (opK f)) ∘ ∂F (bdℱ (opK g))"
    by (simp add: map_dual_func1)
  finally show ?thesis
    by (simp add: ffb_def)
qed

lemma ffb_eta_pres: "fbℱ η = id"
  unfolding ffb_def by simp

lemma ffb_Sup_dual: "Sup_dual fbℱ"
  unfolding ffb_prop_var comp_def fun_eq_iff klift_prop kop_def f2r_def r2f_def converse_def by fastforce

lemma ffb_Sup_dual_var: "fbℱ (⨆F) = (⨅f ∈ F. fbℱ f)"
  unfolding ffb_prop_var comp_def fun_eq_iff klift_prop kop_def f2r_def r2f_def converse_def by fastforce

lemma ffb_sup_dual: "sup_dual fbℱ"
  using ffb_Sup_dual Sup_sup_dual by force

lemma ffb_zero_dual: "fbℱ ζ = (λX. UNIV)" 
  unfolding ffb_prop_var kop_def klift_prop fun_eq_iff f2r_def r2f_def by simp

lemma "inf_dual ffb" (*nitpick*)
  oops

text ‹Once again, only the Sup-quantale structure is preserved.›

lemma iffb_comp_pres:
  assumes "Inf_pres φ"
  assumes "Inf_pres ψ"
  shows "fb-ℱ (φ ∘ ψ) = fb-ℱ φ ∘K fb-ℱ ψ"
    by (metis assms Inf_pres_comp ffb_iffb_galois ffb_kcomp_pres)

lemma iffb_id_pres: "fb-ℱ id = η"
  unfolding iffb_def by force

lemma iffb_Inf_dual: 
  assumes "∀φ ∈ Φ. Inf_pres φ"
  shows "(fb-ℱ ∘ Inf) Φ = (Sup ∘ 𝒫 fb-ℱ) Φ" 
proof-
  have "Inf_pres (⨅Φ)"
    using Inf_pres_Inf assms by blast
  hence "(fbℱ ∘ fb-ℱ) (⨅Φ) = ⨅(𝒫 (fbℱ ∘ fb-ℱ) Φ)"
    by (metis (mono_tags, lifting) INF_cong INF_identity_eq assms iffb_inv2)
  hence "(fbℱ ∘ fb-ℱ) (⨅Φ) = fbℱ (⨆(𝒫 fb-ℱ Φ))"
    by (simp add: Setcompr_eq_image ffb_Sup_dual_var image_comp)
  thus ?thesis
    by (simp add: ffb_inj_iff)
qed  

lemma iffb_Sup_dual: "Sup_dual fb-ℱ"
  by (auto simp: iffb_def fun_eq_iff)
 
lemma iffb_inf_dual: 
  assumes "Inf_pres φ" 
  and "Inf_pres ψ"
shows "fb-ℱ (φ ⊓ ψ) = fb-ℱ φ ⊔ fb-ℱ ψ"
proof -
  have f1: "φ ⊓ ψ = fbℱ (fb-ℱ φ) ⊓ fbℱ (fb-ℱ ψ)"
    using assms iffb_inv2 by fastforce
  have "φ ⊓ ψ ∘ Inter = Inter ∘ 𝒫 (φ ⊓ ψ)"
    using assms Inf_pres_inf by blast
  thus ?thesis
    by (simp add: f1 ffb_iffb_galois ffb_sup_dual)
qed 

lemma  iffb_sup_dual: "fb-ℱ (φ ⊔ ψ) = fb-ℱ φ ⊓ fb-ℱ ψ"
  unfolding iffb_def by fastforce

lemma iffb_top_pres [simp]: "fb-ℱ ⊤ = ζ"
  unfolding iffb_def by simp

text ‹This establishes the duality between state transformers and weakest liberal preconditions.›


subsection ‹Forward Box Operators from Relations›

text ‹Once again one can compose isomorphisms, linking weakest liberal preconditions with relational semantics.
The isomorphism obtained should by now be obvious.›

definition rfb :: "('a × 'b) set ⇒ 'b set ⇒ 'a set"  (‹fbℛ›) where
  "fbℛ = fbℱ ∘ ℱ"

definition irfb :: "('b set ⇒ 'a set) ⇒ ('a × 'b) set" (‹fb-ℛ›) where
  "fb-ℛ = ℛ ∘ fb-ℱ"

lemma rfb_rbd_dual: "fbℛ R = ∂F (bdℛ (R¯))" 
  by (simp add: rfb_def rbd_def kop_def ffb_def, metis r2f_f2r_galois)

lemma rbd_rfb_dual: "bdℛ R = ∂F (fbℛ (R¯))"
  by (simp add: rfb_def rbd_def kop_def ffb_def, metis converse_converse map_dual_dual r2f_f2r_galois)
  
lemma irfb_irbd_dual: "Inf_pres φ ⟹ fb-ℛ φ = ((⌣) ∘ bd-ℛ  ∘ ∂F) φ"
  by (simp add: irfb_def irbd_def iffb_ifbd_dual kop_def r2f_f2r_galois)

lemma irbd_irfb_dual: "Sup_pres φ ⟹ bd-ℛ φ = ((⌣) ∘ fb-ℛ ∘ ∂F) φ"
  by (simp add: irfb_def irbd_def ifbd_iffb_dual kop_def r2f_f2r_galois)

lemma rfb_set: "fbℛ R Y = {x. ∀y. (x,y) ∈ R ⟶ y ∈ Y}"
  unfolding rfb_def ffb_prop_var comp_def klift_def f2r_def r2f_def kop_def by force

lemma rfb_rbd_galois: "(bdℛ R) ⊣ (fbℛ R)"
  by (simp add: ffb_fbd_galois rbd_def rfb_def)

lemma irfb_set: "fb-ℛ φ = {(x, y). ∀Y. x ∈ φ Y ⟶ y ∈ Y}"
  by (simp add: irfb_def iffb_def f2r_def)

lemma irfb_inv1 [simp]: "fb-ℛ ∘ fbℛ = id"
  by (simp add: fun_eq_iff rfb_def irfb_def iffb_inv1 pointfree_idE)

lemma irfb_inv2: "Inf_pres φ ⟹ (fbℛ ∘ fb-ℛ) φ = φ"
  by (simp add: rfb_def irfb_def, metis ffb_iffb_galois r2f_f2r_galois)

lemma rfb_inj: "inj fbℛ"
  by (simp add: rfb_def ffb_inj inj_compose r2f_inj)

lemma rfb_inj_iff: "(fbℛ R = fbℛ S) = (R = S)"
  by (simp add: rfb_inj inj_eq)

lemma irfb_inj: "Inf_pres φ ⟹ Inf_pres ψ ⟹ fb-ℛ φ = fb-ℛ ψ ⟹ φ = ψ"
  unfolding irfb_def using iffb_inj r2f_inj_iff by fastforce

lemma irfb_inf_iff: "Inf_pres φ ⟹ Inf_pres ψ ⟹ (fb-ℛ φ = fb-ℛ ψ) = (φ = ψ)"
  using irfb_inj by auto

lemma rfb_surj: "Inf_pres φ ⟹ (∃R. fbℛ R = φ)"
  using irfb_inv2 by fastforce

lemma irfb_surj: "surj fb-ℛ" 
  by (simp add: irfb_def comp_surj f2r_surj iffb_surj cong del: image_cong_simp)

lemma rfb_irfb_galois: "Inf_pres φ ⟹ (fb-ℛ φ = R) = (fbℛ R = φ)"
  by (simp add: irfb_def rfb_def, metis ffb_iffb_galois r2f_f2r_galois)

lemma rfb_comp_pres: "fbℛ (R ; S) = fbℛ R ∘ fbℛ S"
  by (simp add: ffb_kcomp_pres r2f_comp_pres rfb_def)

lemma rfb_Id_pres [simp]: "fbℛ Id = id"
  unfolding rfb_def ffb_prop by force

lemma rfb_Sup_dual: "Sup_dual fbℛ"
proof- 
  have "fbℛ ∘ μ = fbℱ ∘ ℱ ∘ Sup"
    by (simp add: rfb_def)
  also have "... = fbℱ ∘ Sup ∘ 𝒫 ℱ"
    by (metis fun.map_comp r2f_Sup_pres)
  also have "... = Inf ∘ 𝒫 fbℱ ∘ 𝒫 ℱ"
    by (simp add: ffb_Sup_dual)
  also have "... = Inf ∘ 𝒫 (fbℱ ∘ ℱ)"
    by (simp add: P_func1 comp_assoc)
  finally show ?thesis
    by (simp add: rfb_def)
qed

lemma rfb_Sup_dual_var: "fbℛ (⨆φ) = ⨅(𝒫 fbℛ) φ"
  by (meson comp_eq_dest rfb_Sup_dual)

lemma rfb_sup_dual: "sup_dual fbℛ"
  by (simp add: rfb_def ffb_sup_dual r2f_sup_pres)

lemma "inf_dual fbℛ" (*nitpick*)
  oops

lemma rfb_Inf_pres: "Inf_pres (fbℛ R)"
  unfolding rfb_def ffb_prop_var comp_def fun_eq_iff klift_def kop_def f2r_def r2f_def converse_def by auto

lemma rfb_inf_pres: "inf_pres (fbℛ R)"
  unfolding rfb_def ffb_prop_var comp_def fun_eq_iff klift_def kop_def f2r_def r2f_def converse_def by auto

lemma rfb_zero_pres [simp]: "fbℛ {} X = UNIV"
 unfolding rfb_def ffb_prop_var comp_def fun_eq_iff klift_def kop_def f2r_def r2f_def converse_def by auto

lemma rfb_zero_pres2 [simp]: "fbℛ R {} = - Domain R"
 unfolding rfb_def ffb_prop_var comp_def fun_eq_iff klift_def kop_def f2r_def r2f_def converse_def by auto

lemma rfb_univ [simp]: "fbℛ R UNIV = UNIV"
  unfolding rfb_def ffb_prop_var comp_def fun_eq_iff klift_def kop_def f2r_def r2f_def converse_def by auto

lemma rfb_iso: "X ⊆ Y ⟹ fbℛ R X ⊆ fbℛ R Y"
  unfolding rfb_def ffb_prop_var comp_def fun_eq_iff klift_def kop_def f2r_def r2f_def converse_def by auto

lemma irfb_comp_pres: 
  assumes "Inf_pres φ"
  assumes "Inf_pres ψ"
  shows "fb-ℛ (φ ∘ ψ) = fb-ℛ φ ; fb-ℛ ψ"
  by (metis assms rfb_Inf_pres rfb_comp_pres rfb_irfb_galois)

lemma irfb_id_pres [simp]: "fb-ℛ id = Id"
  by (simp add: rfb_irfb_galois)

lemma irfb_Sup_dual: "Sup_dual fb-ℛ"
  by (auto simp: fun_eq_iff irfb_def iffb_def f2r_def)

lemma irfb_Inf_dual: 
  assumes "∀φ ∈ Φ. Inf_pres φ"
  shows "(fb-ℛ ∘ Inf) Φ = (Sup ∘ 𝒫 fb-ℛ) Φ" 
proof-
  have "Inf_pres (⨅Φ)"
    using Inf_pres_Inf assms by blast
  hence  "(fbℛ ∘ fb-ℛ) (⨅Φ) = ⨅(𝒫 (fbℛ ∘ fb-ℛ) Φ)"
    by (smt INF_identity_eq Sup.SUP_cong assms irfb_inv2)
  also have "... = ⨅(𝒫 fbℛ (𝒫 fb-ℛ Φ))"
    by (simp add: image_comp)
  also have "... = fbℛ (⨆(𝒫 fb-ℛ Φ))"
    by (simp add: rfb_Sup_dual_var)
  finally have "(fbℛ ∘ fb-ℛ) (⨅Φ) = fbℛ (⨆(𝒫 fb-ℛ Φ))".
  thus ?thesis
    by (simp add: rfb_inj_iff)
qed  

lemma irfb_sup_dual: "sup_dual fb-ℛ"
  by (force simp: fun_eq_iff irfb_def iffb_def f2r_def)

lemma irfb_inf_dual: 
  assumes "Inf_pres φ" 
  and "Inf_pres ψ"
  shows "fb-ℛ (φ ⊓ ψ) = fb-ℛ φ ⊔ fb-ℛ ψ"
  by (metis assms rfb_Inf_pres rfb_irfb_galois rfb_sup_dual)

lemma irfb_top_pres [simp]: "bd-ℛ ⊤ = UNIV"
  unfolding irbd_def f2r_def by auto

text ‹Finally, the adjunctions between the predicate transformers considered so far are revisited.›

lemma ffb_fbd_galois_var: "(bdℱ f X ⊆ Y) = (X ⊆ fbℱ f Y)"
  by (meson adj_def ffb_fbd_galois)

lemma rfb_rbd_galois_var: "(bdℛ R X ⊆ Y) = (X ⊆ fbℛ R Y)"
  by (meson adj_def rfb_rbd_galois)

lemma ffb_fbd: "fbℱ f Y = ⋃{X. bdℱ f X ⊆ Y}"
  using ffb_fbd_galois_var by fastforce

lemma rfb_rbd: "fbℛ R Y = ⋃{X. bdℛ R X ⊆ Y}"
  using rfb_rbd_galois_var by fastforce 

lemma fbd_ffb: "bdℱ f X = ⋂{Y. X ⊆ fbℱ f Y}"
  using ffb_fbd_galois_var by fastforce 

lemma rbd_rfb: "bdℛ R X = ⋂{Y. X ⊆ fbℛ R Y}"
  using rfb_rbd_galois_var by fastforce 


subsection ‹The Remaining Modalities›

text ‹Finally I set up the remaining dual transformers: forward diamonds and backward boxes. 
Most properties are not repeated, only some symmetries and dualities are spelled out.›

text ‹First, forward diamond operators are introduced, from state transformers and relations; together
with their inverses.›

definition ffd :: "('a ⇒ 'b set) ⇒ 'b set ⇒ 'a set" (‹fdℱ›) where 
  "fdℱ = bdℱ ∘ opK"

definition iffd :: "('b set ⇒ 'a set) ⇒ 'a ⇒ 'b set" (‹fd-ℱ›) where 
  "fd-ℱ = opK ∘ bd-ℱ"

definition rfd :: "('a × 'b) set ⇒ 'b set ⇒ 'a set" (‹fdℛ›) where 
  "fdℛ = fdℱ ∘ ℱ"

definition irfd :: "('b set ⇒ 'a set) ⇒ ('a × 'b) set" (‹fd-ℛ›) where 
  "fd-ℛ = ℛ ∘ fd-ℱ"

text ‹Second, I introduce forward boxes and their inverses.›

definition fbb :: "('a ⇒ 'b set) ⇒ 'a set ⇒ 'b set" (‹bbℱ›) where 
  "bbℱ = fbℱ ∘ opK"

definition ifbb :: "('a  set ⇒ 'b set) ⇒ 'a ⇒ 'b set" (‹bb-ℱ›) where 
 "bb-ℱ = opK ∘ fb-ℱ"

definition rbb :: "('a × 'b) set ⇒ 'a set ⇒ 'b set" (‹bbℛ›) where 
  "bbℛ = bbℱ ∘ ℱ"

definition irbb :: "('a  set ⇒ 'b set) ⇒ ('a × 'b) set" (‹bb-ℛ›) where 
  "bb-ℛ = ℛ ∘ bb-ℱ"

text ‹Forward and backward operators of the same type (box or diamond) are related by opposition.›

lemma rfd_rbd: "fdℛ = bdℛ ∘ (⌣)"
  by (simp add: rfd_def rbd_def ffd_def kop_def comp_assoc)

lemma irfd_irbd: "fd-ℛ = (⌣) ∘ bd-ℛ"
  by (simp add: irfd_def iffd_def kop_def irbd_def comp_assoc[symmetric])

lemma fbd_ffd: "bdℱ = fdℱ ∘ opK"
  by (simp add: ffd_def kop_def converse_def f2r_def r2f_def klift_def fun_eq_iff)

lemma rbb_rfb: "bbℛ = fbℛ ∘ (⌣)"
  by (simp add: rfb_def rbb_def, metis fbb_def kop_def r2f_f2r_galois_var2 rewriteR_comp_comp2)

lemma irbb_irfb: "bb-ℛ = (⌣) ∘ fb-ℛ"
proof-
  have "bb-ℛ = ℛ ∘ opK ∘ fb-ℱ"
    by (simp add: irbb_def ifbb_def o_assoc)
  also have "... = ℛ ∘ ℱ ∘ (⌣) ∘ ℛ ∘ fb-ℱ"
    by (simp add: kop_def o_assoc)
  also have "... = (⌣) ∘ fb-ℛ"
    by (simp add: comp_assoc irfb_def)
  finally show ?thesis.
qed

text ‹Complementation is a natural isomorphism between forwards and backward operators of different type.›

lemma ffd_ffb_demorgan: "∂ ∘ fdℱ f = fbℱ f ∘ ∂"
  by (simp add: comp_assoc ffb_prop ffd_def)

lemma iffd_iffb_demorgan: "Sup_pres φ ⟹ fd-ℱ φ = (fb-ℱ ∘ ∂F) φ"
  by (smt Sup_pres_Inf_pres comp_apply iffb_ifbd_dual iffd_def map_dual_dual)

lemma ffb_ffd_demorgan: "∂ ∘ fbℱ f = fdℱ f ∘ ∂"
  by (simp add: ffb_prop ffd_def rewriteL_comp_comp)

lemma iffb_iffd_demorgan: "Inf_pres φ ⟹ fb-ℱ φ = (fd-ℱ ∘ ∂F) φ"
  by (simp add: iffb_ifbd_dual iffd_def)

lemma rfd_rfb_demorgan: "∂ ∘ fdℛ R = fbℛ R ∘ ∂"
  by (simp add: rfb_def rfd_def ffd_ffb_demorgan)

lemma irfd_irfb_demorgan: "Sup_pres φ ⟹ fd-ℛ φ = (fb-ℛ ∘ ∂F) φ"
  by (simp add: irfb_def irfd_def iffd_iffb_demorgan)

lemma rfb_rfd_demorgan: "∂ ∘ fbℛ R = fdℛ R ∘ ∂"
  by (simp add: ffb_ffd_demorgan rfb_def rfd_def)

lemma irfb_irfd_demorgan: "Inf_pres φ ⟹ fb-ℛ φ  = (fd-ℛ ∘ ∂F) φ"
  by (simp add: irfb_irbd_dual irfd_irbd)

lemma fbd_fbb_demorgan: "∂ ∘ bdℱ f = bbℱ f ∘ ∂"   
  by (simp add: fbb_def fbd_ffd ffd_ffb_demorgan)

lemma ifbd_ifbb_demorgan: "Sup_pres φ ⟹ bd-ℱ φ = (bb-ℱ ∘ ∂F) φ"
  by (simp add: ifbd_iffb_dual ifbb_def)  

lemma fbb_fbd_demorgan: "∂ ∘ bbℱ R = bdℱ R ∘ ∂"
  by (simp add: fbb_def fbd_ffd ffb_ffd_demorgan)

lemma ifbb_ifbd_demorgan: "Inf_pres φ ⟹ bb-ℱ φ = (bd-ℱ ∘ ∂F) φ"
proof-
  assume h: "Inf_pres φ"
  have "bb-ℱ φ = (opK ∘ fb-ℱ) φ"
    by (simp add: ifbb_def)
  also have "... = (opK ∘ opK ∘ bd-ℱ) (∂F φ)"
    by (metis comp_apply h iffb_ifbd_dual) 
  also have "... = (bd-ℱ ∘ ∂F) φ"
    by auto
  finally show ?thesis.
qed

lemma rbd_rbb_demorgan: "∂ ∘ bdℛ R = bbℛ R ∘ ∂"
  by (simp add: rbb_def rbd_def fbd_fbb_demorgan)

lemma irbd_irbb_demorgan: "Sup_pres φ ⟹ bd-ℛ φ = (bb-ℛ ∘ ∂F) φ"
  by (simp add: irbb_irfb irbd_irfb_dual)

lemma rbb_rbd_demorgan: "∂ ∘ bbℛ R = bdℛ R ∘ ∂"
  by (simp add: rbb_def rbd_def fbb_fbd_demorgan)

lemma irbb_irbd_demorgan: "Inf_pres φ ⟹ bb-ℛ φ = (bd-ℛ ∘ ∂F) φ"
  by (simp add: irbb_def irbd_def ifbb_ifbd_demorgan)

text ‹Further symmetries arise by combination.›

lemma ffd_fbb_dual: "∂ ∘ fdℱ f = bbℱ (opK f) ∘ ∂"
  by (simp add: fbd_fbb_demorgan ffd_def)

lemma iffd_ifbb_dual: "Sup_pres φ ⟹ fd-ℱ φ = (opK ∘ bb-ℱ ∘ ∂F) φ"
  by (simp add: ifbd_ifbb_demorgan iffd_def)  

lemma fbb_ffd_dual: "∂ ∘ bbℱ f = fdℱ (opK f) ∘ ∂"
  by (simp add: fbd_ffd fbb_fbd_demorgan) 

lemma ifbb_iffd_dual: "Inf_pres φ ⟹ bb-ℱ φ = (opK ∘ fd-ℱ ∘ ∂F) φ"
  by (simp add: ifbb_def iffb_iffd_demorgan)

lemma rfd_rbb_dual: "∂ ∘ fdℛ R = bbℛ (R¯) ∘ ∂"
  by (metis fun_dual1 map_dual_def rbd_rbb_demorgan rfb_rbd_dual rfd_rfb_demorgan)

lemma ifd_ibb_dual: "Sup_pres φ ⟹ fd-ℛ φ = ((⌣) ∘ bb-ℛ ∘ ∂F) φ"
  by (simp add: irbb_irfb irbd_irfb_dual irfd_irbd)
 
lemma rbb_rfd_dual: "∂ ∘ bbℛ R = fdℛ (R¯) ∘ ∂"
  by (simp add: rbb_rfb rfb_rfd_demorgan)

lemma irbb_irfd_dual: "Inf_pres φ ⟹ bb-ℛ φ = ((⌣) ∘ fd-ℛ ∘ ∂F) φ"
  by (simp add: irbb_irfb irfb_irbd_dual irfd_irbd)

lemma ffd_iffd_galois: "Sup_pres φ ⟹ (φ = fdℱ f) = (f = fd-ℱ φ)"
  unfolding ffd_def iffd_def by (metis comp_apply fbd_surj klift_eta_inv1 kop_galois)

lemma rfd_irfd_galois: "Sup_pres φ ⟹ (φ = fdℛ R) = (R = fd-ℛ φ)"
  unfolding irfd_def rfd_def by (metis comp_apply ffd_iffd_galois r2f_f2r_galois)

lemma fbb_ifbb_galois: "Inf_pres φ ⟹ (φ = bbℱ f) = (f = bb-ℱ φ)"
  unfolding fbb_def iffb_def by (metis (no_types, lifting) comp_apply ffb_iffb_galois ifbb_ifbd_demorgan iffb_ifbd_dual kop_galois)

lemma rbb_irbb_galois: "Inf_pres φ ⟹ (φ = bbℛ R) = (R = bb-ℛ φ)"
  apply (simp add: rbb_def irbb_def) using fbb_ifbb_galois r2f_f2r_galois by blast

text ‹Next I spell out the missing adjunctions.›

lemma ffd_ffb_adj: "fdℱ f ⊣ bbℱ f"
  by (simp add: fbb_def ffb_fbd_galois ffd_def)

lemma ffd_fbb_galois: "(fdℱ f X ⊆ Y) = (X ⊆ bbℱ f Y)"
  by (simp add: fbb_def ffb_fbd_galois_var ffd_def)

lemma rfd_rfb_adj: "fdℛ f ⊣ bbℛ f"
  by (simp add: ffd_ffb_adj rbb_def rfd_def)

lemma rfd_rbb_galois: "(fdℛ R X ⊆ Y) = (X ⊆ bbℛ R Y)"
  by (simp add: ffd_fbb_galois rbb_def rfd_def)

text ‹Finally, forward and backward operators of the same type are linked by conjugation.›

lemma ffd_fbd_conjugation: "(fdℱ f X ∩ Y = {}) = (X ∩ bdℱ f Y = {})"
proof-
  have "(fdℱ f X ∩ Y = {}) = (fdℱ f X ⊆ -Y)"
    by (simp add: disjoint_eq_subset_Compl)
  also have "... = (X ⊆ bbℱ f (-Y))"
    by (simp add: ffd_fbb_galois)
  also have "... = (X ∩ - bbℱ f (-Y) = {})"
    by (simp add: disjoint_eq_subset_Compl)
  also have "... = (X ∩ ∂ (bbℱ f (∂ Y)) = {})"
    by (simp add: dual_set_def)
  finally show ?thesis
    by (metis (no_types, opaque_lifting) comp_apply fbb_fbd_demorgan invol_dual_var)
qed

lemma rfd_rbd_conjugation: "((fdℛ R X) ∩ Y = {}) = (X ∩ (bdℛ R Y) = {})"
  by (simp add: rbd_def rfd_def ffd_fbd_conjugation) 

lemma ffb_fbb_conjugation: "((fbℱ f X) ∪ Y = UNIV) = (X ∪ (bbℱ f Y) = UNIV)" 
proof-
  have "((fbℱ f X) ∪ Y = UNIV) = (-Y ⊆ fbℱ f X)"
    by blast
  also have "... = (bdℱ f (∂ Y) ⊆ X)"
    by (simp add: ffb_fbd_galois_var dual_set_def)
  also have "... = (∂ (bbℱ f Y) ⊆ X)"
    by (metis comp_def fbb_fbd_demorgan)
  also have "... = (X ∪ (bbℱ f Y) = UNIV)"
    by (metis compl_le_swap2 dual_set_def sup_shunt)
    finally show ?thesis.
qed

lemma rfb_rbb_conjugation: "((fbℛ R X) ∪ Y = UNIV) = (X ∪ (bbℛ R Y) = UNIV)" 
  by (simp add: rfb_def rbb_def ffb_fbb_conjugation) 

end