# Theory Isotone_Transformers

(*
Title: Isotone Transformers Between Complete Lattices
Author: Georg Struth
Maintainer: Georg Struth <g.struth@sheffield.ac.uk>
*)

section ‹Isotone Transformers Between Complete Lattices›

theory Isotone_Transformers
imports "Order_Lattice_Props.Fixpoint_Fusion"
"Quantales.Quantale_Star"

begin

text ‹A transformer is a function between lattices; an isotone transformer preserves the order (or is monotone). In this component,
statements are developed in a type-driven way. Statements are developed in more general contexts or even the most general one.›

subsection ‹Basic Properties›

text ‹First I show that some basic transformers are isotone...›

lemma iso_id: "mono id"
by (simp add: monoI)

lemma iso_botf: "mono ⊥"
by (simp add: monoI)

lemma iso_topf: "mono ⊤"
by (simp add: monoI)

text ‹... and that compositions, Infs and Sups preserve isotonicity.›

lemma iso_fcomp: "mono f ⟹ mono g ⟹ mono (f ∘ g)"
by (simp add: mono_def)

lemma iso_fSup:
fixes F :: "('a::order ⇒ 'b::complete_lattice) set"
shows "(∀f ∈ F. mono f) ⟹ mono (⨆F)"
by (simp add: mono_def SUP_subset_mono)

lemma iso_fsup: "mono f ⟹ mono g ⟹ mono (f ⊔ g)"
unfolding mono_def using sup_mono by fastforce

lemma iso_fInf:
fixes F :: "('a::order ⇒ 'b::complete_lattice) set"
shows "∀f ∈ F. mono f ⟹ mono (⨅F)"
by (simp add: mono_def, safe, rule Inf_greatest, auto simp: INF_lower2)

lemma iso_finf: "mono f ⟹ mono g ⟹ mono (f ⊓ g)"
unfolding mono_def using inf_mono by fastforce

lemma fun_isol: "mono f ⟹ g ≤ h ⟹ (f ∘ g) ≤ (f ∘ h)"
by (simp add: le_fun_def monoD)

lemma fun_isor: "mono f ⟹ g ≤ h ⟹ (g ∘ f) ≤ (h ∘ f)"
by (simp add: le_fun_def monoD)

subsection ‹Pre-Quantale of Isotone Transformers›

text ‹It is well known, and has been formalised within Isabelle, that functions into complete lattices form complete lattices.
In the following proof, this needs to be replayed because isotone functions are considered and closure conditions
need to be respected.

Functions must now be restricted to a single type.›

instantiation iso :: (complete_lattice) unital_pre_quantale
begin

lift_definition one_iso :: "'a::complete_lattice iso" is id
by (simp add: iso_id)

lift_definition times_iso :: "'a::complete_lattice iso ⇒ 'a iso ⇒ 'a iso" is "(∘)"
by (simp add: iso_fcomp)

instance
by (intro_classes; transfer, simp_all add: comp_assoc fInf_distr_var fInf_subdistl_var)

end

text ‹I have previously worked in (pre)quantales with many types or quantaloids. Formally, these are categories
enriched over the category of Sup-lattices (complete lattices with Sup-preserving functions). An advantage
of the single-typed approach is that the definition of the Kleene star for (pre)quantales is available in this setting.›

subsection ‹Propositional Hoare Logic for Transformers without Star›

text ‹The rules of an abstract Propositional Hoare logic are derivable.›

lemma H_iso_cond1: "(x::'a::preorder) ≤ y ⟹ y ≤ f z ⟹ x ≤ f z"
using order_trans by auto

lemma H_iso_cond2: "mono f ⟹ y ≤ z ⟹ x ≤ f y ⟹ x ≤ f z"
by (meson mono_def order_subst1)

lemma H_iso_seq: "mono f ⟹ x ≤ f y ⟹ y ≤ g z ⟹ x ≤ f (g z)"
using H_iso_cond2 by force

lemma H_iso_seq_var: "mono f ⟹ x ≤ f y ⟹ y ≤ g z ⟹ x ≤ (f ∘ g) z"
by (simp add: H_iso_cond2)

lemma H_iso_fInf:
fixes F :: "('a ⇒ 'b::complete_lattice) set"
shows "(∀f ∈ F. x ≤ f y) ⟹ x ≤ (⨅F) y"
by (simp add: le_INF_iff)

lemma H_iso_fSup:
fixes F :: "('a ⇒ 'b::complete_lattice) set"
shows "F ≠ {} ⟹ (∀f ∈ F. x ≤ f y) ⟹ x ≤ (⨆F) y"
using SUP_upper2 by fastforce

text ‹These rules are suitable for weakest liberal preconditions. Order-dual ones, in which the order relation is swapped,
are consistent with other kinds of transformers. In the context of dynamic logic, the first set corresponds to box modalities
whereas the second one would correspond to diamonds.›

subsection ‹Kleene Star of Isotone Transformers›

text ‹The Hoare rule for loops requires some preparation. On the way I verify some Kleene-algebra-style axioms for iteration.›

text ‹First I show that functions form monoids.›

interpretation fun_mon: monoid_mult "id::'a ⇒ 'a" "(∘)"
by unfold_locales auto

definition fiter_fun :: "('a ⇒ 'c::semilattice_inf) ⇒ ('b ⇒ 'c) ⇒ ('a ⇒ 'b) ⇒ 'a ⇒ 'c" where
"fiter_fun f g = (⊓) f ∘ (∘) g"

definition fiter :: "('a ⇒ 'b::complete_lattice) ⇒ ('b ⇒ 'b) ⇒ 'a ⇒ 'b" where
"fiter f g = gfp (fiter_fun f g)"

definition fiter_id :: "('a::complete_lattice ⇒ 'a) ⇒ 'a ⇒ 'a" where
"fiter_id = fiter id"

abbreviation "fpower ≡ fun_mon.power"

definition fstar :: "('a::complete_lattice ⇒ 'a) ⇒ 'a ⇒ 'a" where
"fstar f = (⨅i. fpower f i)"

text ‹The types in the following statements are often more general than those in the prequantale setting. I develop them generally,
instead of inheriting (most of them) with more restrictive types from the quantale components.›

lemma fiter_fun_exp: "fiter_fun f g h = f ⊓ (g ∘ h)"
unfolding fiter_fun_def by simp

text ‹The two lemmas that follow set up the relationship between the star for transformers and those in quantales.›

lemma fiter_qiter1: "Abs_iso (fiter_fun (Rep_iso f) (Rep_iso g) (Rep_iso h)) = qiter_fun f g h"
unfolding fiter_fun_def qiter_fun_def by (metis Rep_iso_inverse comp_def sup_iso.rep_eq times_iso.rep_eq)

lemma fiter_qiter4: "mono f ⟹ mono g ⟹ mono h ⟹ Rep_iso (qiter_fun (Abs_iso f) (Abs_iso g) (Abs_iso h)) = fiter_fun f g h"
by (metis Abs_iso_inverse fiter_fun_exp fiter_qiter1 iso_fcomp iso_finf mem_Collect_eq)

text ‹The type coercions are needed to deal with isotone (monotone) functions, which had to be redefined to one single type above,
in order to cooperate with the type classes for quantales. Having to deal with these coercions would be another drawback of using the
quantale-based setting for the development.›

lemma iso_fiter_fun: "mono f ⟹ mono (fiter_fun f)"
by (simp add: fiter_fun_exp le_fun_def mono_def inf.coboundedI2)

lemma iso_fiter_fun2: "mono f ⟹ mono g ⟹ mono (fiter_fun f g)"
by (simp add: fiter_fun_exp le_fun_def mono_def inf.coboundedI2)

lemma fiter_unfoldl:
fixes f :: "'a::complete_lattice ⇒ 'a"
shows "mono f ⟹ mono g ⟹ f ⊓ (g ∘ fiter f g) = fiter f g"
by (metis fiter_def fiter_fun_exp gfp_unfold iso_fiter_fun2)

lemma fiter_inductl:
fixes f :: "'a::complete_lattice ⇒ 'a"
shows "mono f ⟹ mono g ⟹ h ≤ f ⊓ (g ∘ h) ⟹ h ≤ fiter f g"
by (simp add: fiter_def fiter_fun_def gfp_upperbound)

lemma fiter_fusion:
fixes f :: "'a::complete_lattice ⇒ 'a"
assumes "mono f"
and "mono g"
shows "fiter f g = fiter_id g ∘ f"
proof-
have h1: "mono (fiter_fun id g)"
by (simp add: assms(2) iso_fiter_fun2 iso_id)
have h2: "mono (fiter_fun f g)"
by (simp add: assms(1) assms(2) iso_fiter_fun2)
have h3: "Inf ∘ image (λx. x ∘ f) = (λx. x ∘ f) ∘ Inf"
by (simp add: fun_eq_iff image_comp)
have "(λx. x ∘ f) ∘ (fiter_fun id g) = (fiter_fun f g) ∘ (λx. x ∘ f)"
by (simp add: fun_eq_iff fiter_fun_def)
thus ?thesis
using gfp_fusion_inf_pres
by (metis fiter_def fiter_id_def h1 h2 h3)
qed

lemma fpower_supdistl:
fixes f :: "'a::complete_lattice ⇒ 'b::complete_lattice"
shows "mono f ⟹ f ∘ fstar g ≤ (⨅i. f ∘ fpower g i)"
by (simp add: Isotone_Transformers.fun_isol fstar_def mono_INF mono_def)

lemma fpower_distr: "fstar f ∘ g = (⨅i. fpower f i ∘ g)"
by (auto simp: fstar_def image_comp)

lemma fpower_Sup_subcomm: "mono f ⟹ f ∘ fstar f ≤ fstar f ∘ f"
by (metis (mono_tags, lifting) fun_mon.power_commutes le_INF_iff fpower_distr fpower_supdistl)

lemma fpower_inductl:
fixes f :: "'a::complete_lattice ⇒ 'a"
shows "mono f ⟹ mono g ⟹ h ≤ g ⊓ (f ∘ h) ⟹ h ≤ fpower f i ∘ g"
apply (induct i, simp_all) by (metis (no_types, hide_lams) fun.map_comp fun_isol order_trans)

lemma fpower_inductr:
fixes f :: "'a::complete_lattice ⇒ 'a"
shows "mono f ⟹ mono g ⟹ h ≤ g ⊓ (h ∘ f) ⟹ h ≤ g ∘ fpower f i"
by (induct i, simp_all add: le_fun_def, metis comp_eq_elim fun_mon.power_commutes order_trans)

lemma fiter_fstar: "mono f ⟹ fiter_id f ≤ fstar f"
by (metis (no_types, lifting) fiter_id_def fiter_unfoldl fpower_inductl fstar_def iso_id le_INF_iff o_id order_refl)

lemma iso_fiter_ext:
fixes f :: "'a::order ⇒ 'b::complete_lattice"
shows "mono f ⟹ mono (λx. y ⊓ f x)"
by (simp add: le_infI2 mono_def)

lemma fstar_pred_char:
fixes f :: "'a::complete_lattice ⇒ 'a"
shows "mono f ⟹ fiter_id f x = gfp (λy. x ⊓ f y)"
proof -
assume hyp: "mono f"
have "∀g. (id ⊓ (f ∘ g)) x = x ⊓ f (g x)"
by simp
hence "∀g. fiter_fun id f g x = (λy. x ⊓ f y) (g x)"
unfolding fiter_fun_def by simp
thus ?thesis
by (simp add: fiter_id_def fiter_def gfp_fusion_var hyp iso_fiter_fun2 iso_id iso_fiter_ext)
qed

subsection ‹Propositional Hoare Logic Completed›

lemma H_weak_loop: "mono f ⟹ x ≤ f x ⟹ x ≤ fiter_id f x"
by (force simp: fstar_pred_char gfp_def intro: Sup_upper)

lemma iso_fiter: "mono f ⟹ mono (fiter_id f)"
unfolding mono_def by (subst fstar_pred_char, simp add: mono_def)+ (auto intro: gfp_mono inf_mono)

text ‹As already mentioned, a dual Hoare logic can be built for the dual lattice. In this case, weak iteration is defined with respect to Sup.›

text ‹The following standard construction lifts elements of (meet semi)lattices to transformers.
I allow a more general type.›

definition fqtran :: "'a::inf ⇒ 'a ⇒ 'a" where
"fqtran x ≡ λy. x ⊓ y"

text ‹The following standard construction lifts elements of boolean algebras to transformers.›

definition bqtran :: "'a::boolean_algebra ⇒ 'a ⇒ 'a" ("⌊_⌋") where
"⌊x⌋ y = -x ⊔ y"

text ‹The conditional and while rule of Hoare logic are now derivable.›

lemma bqtran_iso: "mono ⌊x⌋"
by (metis bqtran_def monoI order_refl sup.mono)

lemma cond_iso: "mono f ⟹ mono g ⟹ mono (⌊x⌋ ∘ f ⊓ ⌊y⌋ ∘ g)"
by (simp add: bqtran_iso iso_fcomp iso_finf)

lemma loop_iso: "mono f ⟹ mono (fiter_id (⌊x⌋ ∘ f) ∘ ⌊y⌋)"
by (simp add: bqtran_iso iso_fcomp iso_fiter)

lemma H_iso_cond: "mono f ⟹ mono g ⟹  p ⊓ x ≤ f y ⟹ q ⊓ x ≤ g y ⟹ x ≤ (inf (⌊p⌋ ∘ f) (⌊q⌋ ∘ g)) y"
by (metis (full_types) bqtran_def comp_apply inf_apply inf_commute le_inf_iff shunt1)

lemma H_iso_loop: "mono f ⟹ p ⊓ x ≤ f x ⟹ x ≤ ((fiter_id (⌊p⌋ ∘ f)) ∘ ⌊q⌋) (x ⊓ q)"
proof-
assume a: "mono f"
and "p ⊓ x ≤ f x"
hence "x ≤ (⌊p⌋ ∘ f) x"
using H_iso_cond by fastforce
hence "x ≤ (fiter_id (⌊p⌋ ∘ f)) x"
by (simp add: H_weak_loop a bqtran_iso iso_fcomp)
also have "... ≤ (fiter_id (⌊p⌋ ∘ f)) (-q ⊔ (x ⊓ q))"
by (meson a bqtran_iso dual_order.refl iso_fcomp iso_fiter monoD shunt1)
finally show "x ≤ ((fiter_id (⌊p⌋ ∘ f)) ∘ ⌊q⌋) (x ⊓ q)"
by (simp add: bqtran_def)
qed

lemma btran_spec: "x ≤ ⌊y⌋ (x ⊓ y)"
by (simp add: bqtran_def sup_inf_distrib1)

lemma btran_neg_spec: "x ≤ ⌊-y⌋ (x - y)"
by (simp add: btran_spec diff_eq)

subsection ‹A Propositional Refinement Calculus›

text ‹Next I derive the laws of an abstract Propositional Refinement Calculus, Morgan-style.
These are given without the co-called frames, which capture information about local and global variables in variants of this calculus.›

definition "Ri x y z = ⨅{f z |f. x ≤ f y ∧ mono (f::'a::order ⇒ 'b::complete_lattice)}"

lemma Ri_least: "mono f ⟹ x ≤ f y ⟹ Ri x y z ≤ f z"
unfolding Ri_def by (metis (mono_tags, lifting) Inf_lower mem_Collect_eq)

lemma Ri_spec: "x ≤ Ri x y y"
unfolding Ri_def by (rule Inf_greatest, safe)

lemma Ri_spec_var: "(∀z. Ri x y z ≤ f z) ⟹ x ≤ f y"
using Ri_spec dual_order.trans by blast

lemma Ri_prop: "mono f ⟹ x ≤ f y ⟷ (∀z. Ri x y z ≤ f z)"
using Ri_least Ri_spec_var by blast

lemma iso_Ri: "mono (Ri x y)"
unfolding mono_def Ri_def by (auto intro!: Inf_mono)

lemma Ri_weaken: "x ≤ x' ⟹  y' ≤ y ⟹ Ri x y z ≤ Ri x' y' z"
by (meson H_iso_cond2 Ri_least Ri_spec iso_Ri order.trans)

lemma Ri_seq: "Ri x y z ≤ Ri x w (Ri w y z)"
by (metis (no_types, hide_lams) H_iso_cond2 Ri_prop Ri_spec iso_Ri iso_fcomp o_apply)

lemma Ri_seq_var: "Ri x y z ≤ ((Ri x w) ∘ (Ri w y)) z"
by (simp add: Ri_seq)

lemma Ri_Inf: " Ri (⨅ X) y z ≤ ⨅{Ri x y z |x. x ∈ X}"
by (safe intro!: Inf_greatest, simp add: Ri_weaken Inf_lower)

lemma Ri_weak_iter: "Ri x x y  ≤ fiter_id (Ri x x) y"
by (simp add: H_weak_loop Ri_least Ri_spec iso_Ri iso_fiter)

lemma Ri_cond: "Ri x y z ≤ (inf (⌊p⌋ ∘ (Ri (p ⊓ x) y)) ((⌊q⌋ ∘ (Ri (q ⊓ x) y)))) z"
by (meson H_iso_cond Ri_least Ri_spec bqtran_iso iso_Ri iso_fcomp iso_finf)

lemma Ri_loop: "Ri x (q ⊓ x) y ≤ ((fiter_id (⌊p⌋ ∘ (Ri (x ⊓ p) x))) ∘ ⌊q⌋) (q ⊓ y)"
proof-
have "(p ⊓ x) ≤ Ri (p ⊓ x) x x"
by (simp add: Ri_spec)
hence "x ≤ ((fiter_id (⌊p⌋ ∘ (Ri (x ⊓ p) x))) ∘ ⌊q⌋) (q ⊓ x)"
by (metis H_iso_loop inf_commute iso_Ri)
thus ?thesis
apply (subst Ri_least, safe, simp_all add: mono_def)
by (metis bqtran_iso inf_mono iso_Ri iso_fcomp iso_fiter mono_def order_refl)
qed

end


# Theory Sup_Inf_Preserving_Transformers

(*
Title: Sup- and Inf-Preserving Transformers Between Complete Lattices
Author: Georg Struth
Maintainer: Georg Struth <g.struth@sheffield.ac.uk>
*)

section ‹Sup- and Inf-Preserving Transformers between Complete Lattices›

theory Sup_Inf_Preserving_Transformers
imports Isotone_Transformers

begin

subsection ‹Basic Properties›

text ‹Definitions and basic properties of Sup-preserving and Inf-preserving functions can be found in the Lattice components.
The main purose of the lemmas that follow is to bring properties of isotone transformers into scope.›

lemma Sup_pres_iso:
fixes f :: "'a::complete_lattice ⇒ 'b::complete_lattice"
shows "Sup_pres f ⟹ mono f"
by (simp add: Sup_supdistl_iso)

lemma Inf_pres_iso:
fixes f :: "'a::complete_lattice ⇒ 'b::complete_lattice"
shows "Inf_pres f ⟹ mono f"
by (simp add: Inf_subdistl_iso)

lemma sup_pres_iso:
fixes f :: "'a::lattice ⇒ 'b::lattice"
shows "sup_pres f ⟹ mono f"
by (metis le_iff_sup mono_def)

lemma inf_pres_iso:
fixes f :: "'a::lattice ⇒ 'b::lattice"
shows "inf_pres f ⟹ mono f"
by (metis inf.absorb_iff2 monoI)

lemma Sup_sup_dual:
fixes f :: "'a::complete_lattice ⇒ 'b::complete_lattice"
shows "Sup_dual f ⟹ sup_dual f"
by (smt comp_eq_elim image_empty image_insert inf_Inf sup_Sup)

lemma Inf_inf_dual:
fixes f :: "'a::complete_lattice ⇒ 'b::complete_lattice"
shows "Inf_dual f ⟹ inf_dual f"
by (smt comp_eq_elim image_empty image_insert inf_Inf sup_Sup)

lemma Sup_bot_dual:
fixes f :: "'a::complete_lattice ⇒ 'b::complete_lattice"
shows"Sup_dual f ⟹ bot_dual f"
by (metis INF_empty Sup_empty comp_eq_elim)

lemma Inf_top_dual:
fixes f :: "'a::complete_lattice ⇒ 'b::complete_lattice"
shows "Inf_dual f ⟹ top_dual f"
by (metis Inf_empty SUP_empty comp_eq_elim)

text ‹Next I show some basic preservation properties.›

lemma Sup_dual2: "Sup_dual f ⟹ Inf_dual g ⟹ Sup_pres (g ∘ f)"
by (simp add: fun_eq_iff image_comp)

lemma Inf_dual2: "Sup_dual f ⟹ Inf_dual g ⟹ Inf_pres (f ∘ g)"
by (simp add: fun_eq_iff image_comp)

lemma Sup_pres_id: "Sup_pres id"
by simp

lemma Inf_pres_id: "Inf_pres id"
by simp

lemma Sup_pres_comp: "Sup_pres f ⟹ Sup_pres g ⟹ Sup_pres (f ∘ g)"
by (simp add: fun_eq_iff image_comp)

lemma Inf_pres_comp: "Inf_pres f ⟹ Inf_pres g ⟹ Inf_pres(f ∘ g)"
by (simp add: fun_eq_iff image_comp)

lemma Sup_pres_Sup:
fixes F :: "('a::complete_lattice ⇒ 'b::complete_lattice) set"
shows "∀f ∈ F. Sup_pres f ⟹ Sup_pres (⨆F)"
proof-
assume h: "∀f ∈ F. f ∘ Sup = Sup ∘ image f"
hence "∀f ∈ F. f ∘ Sup ≤ Sup ∘ image (⨆F)"
by (simp add: SUP_subset_mono Sup_upper le_fun_def)
hence "(⨆F) ∘ Sup ≤ Sup ∘ image (⨆F)"
by (simp add: SUP_le_iff le_fun_def)
thus ?thesis
by (simp add: Sup_pres_iso h antisym iso_Sup_supdistl iso_fSup)
qed

lemma Inf_pres_Inf:
fixes F :: "('a::complete_lattice ⇒ 'b::complete_lattice) set"
shows "∀f ∈ F. Inf_pres f ⟹ Inf_pres (⨅F)"
proof-
assume h: "∀f ∈ F. f ∘ Inf = Inf ∘ image f"
hence "∀f ∈ F. Inf ∘ image (⨅F) ≤ f ∘ Inf"
by (simp add: le_fun_def, safe, meson INF_lower INF_mono)
hence "Inf ∘ image (⨅F) ≤ (⨅F) ∘ Inf"
by (simp add: le_INF_iff le_fun_def)
thus ?thesis
by (simp add: Inf_pres_iso h antisym iso_Inf_subdistl iso_fInf)
qed

lemma Sup_pres_sup:
fixes f :: "'a::complete_lattice ⇒ 'b::complete_lattice"
shows "Sup_pres f ⟹ Sup_pres g ⟹ Sup_pres (f ⊔ g)"
by (metis Sup_pres_Sup insert_iff singletonD sup_Sup)

lemma Inf_pres_inf:
fixes f :: "'a::complete_lattice ⇒ 'b::complete_lattice"
shows "Inf_pres f ⟹ Inf_pres g ⟹ Inf_pres (f ⊓ g)"
by (metis Inf_pres_Inf inf_Inf insert_iff singletonD)

lemma Sup_pres_botf: "Sup_pres (λx. ⊥::'a::complete_lattice)"
by (simp add: fun_eq_iff)

text ‹It is important to note that $\lambda x. \bot$ is not Inf-preserving and that $\lambda x. \top$ is not Sup-preserving.›

lemma "Inf_pres (λx. ⊥::'a::complete_lattice)" (*nitpick[show_all]*)
oops

lemma "Sup_pres (λx. ⊤::'a::complete_lattice)" (*nitpick[show_all]*)
oops

lemma Inf_pres_topf: "Inf_pres (λx. ⊤::'a::complete_lattice)"
by (simp add: fun_eq_iff)

text ‹In complete boolean algebras, complementation yields an explicit variant of duality, which
can be expressed within the language.›

lemma uminus_galois:
fixes f :: "'a::complete_boolean_algebra ⇒ 'b::complete_boolean_algebra_alt"
shows "(uminus f = g) = (uminus g = f)"
using double_compl by force

lemma uminus_galois_var:
fixes f :: "'a::complete_boolean_algebra_alt_with_dual ⇒ 'b::complete_boolean_algebra_alt_with_dual"
shows "(∂ ∘ f = g) = (∂ ∘ g = f)"
by force

lemma uminus_galois_var2:
fixes f :: "'a::complete_boolean_algebra_alt_with_dual ⇒ 'b::complete_boolean_algebra_alt_with_dual"
shows "(f ∘ ∂ = g) = (g ∘ ∂ = f)"
by force

lemma uminus_mono_iff:
fixes f :: "'a::complete_boolean_algebra_alt_with_dual ⇒ 'b::complete_boolean_algebra_alt_with_dual"
shows "(∂ ∘ f = ∂ ∘ g) = (f = g)"
using uminus_galois_var by force

lemma uminus_epi_iff:
fixes f :: "'a::complete_boolean_algebra_alt_with_dual ⇒ 'b::complete_boolean_algebra_alt_with_dual"
shows "(f ∘ ∂ = g ∘ ∂) = (f = g)"
using uminus_galois_var2 by force

lemma Inf_pres_Sup_pres:
fixes f :: "'a::complete_boolean_algebra_alt_with_dual ⇒ 'b::complete_boolean_algebra_alt_with_dual"
shows "(Inf_pres f) = (Sup_pres (∂⇩F f))"
by (simp add: Inf_pres_map_dual_var)

lemma Sup_pres_Inf_pres:
fixes f :: "'a::complete_boolean_algebra_alt_with_dual ⇒ 'b::complete_boolean_algebra_alt_with_dual"
shows "(Sup_pres f) = (Inf_pres (∂⇩F f))"
by (simp add: Sup_pres_map_dual_var)

subsection ‹Properties of the Kleene Star›

text ‹I develop the star for Inf-preserving functions only. This is suitable for weakest liberal preconditions.
The case of sup-preserving functions is dual, and straightforward. The main difference to isotone transformers is that Kleene's fixpoint theorem
now applies, that is, the star can be represented by iteration.›

lemma  H_Inf_pres_fpower:
fixes f :: "'a::complete_lattice ⇒ 'a"
shows "Inf_pres f ⟹ x ≤ f x ⟹ x ≤ fpower f i x"
apply (induct i, simp_all) using H_iso_cond2 Inf_pres_iso by blast

lemma H_Inf_pres_fstar:
fixes f :: "'a::complete_lattice ⇒ 'a"
shows "Inf_pres f ⟹ x ≤ f x ⟹ x ≤ fstar f x"
by (simp add: H_Inf_pres_fpower fstar_def le_INF_iff)

lemma fpower_Inf_pres: "Inf_pres f ⟹ Inf_pres (fpower f i)"
by (induct i, simp_all add: Inf_pres_comp)

lemma fstar_Inf_pres:
fixes f :: "'a::complete_lattice ⇒ 'a"
shows "Inf_pres f ⟹ Inf_pres (fstar f)"
by (simp add: fstar_def Inf_pres_Inf fpower_Inf_pres)

lemma fstar_unfoldl_var [simp]:
fixes f :: "'a::complete_lattice ⇒ 'a"
shows "Inf_pres f ⟹ x ⊓ f (fstar f x) = fstar f x"
proof-
assume hyp: "Inf_pres f"
have "x ⊓ f (fstar f x) = fpower f 0 x ⊓ (⨅n. fpower f (Suc n) x)"
by (simp add: fstar_def image_comp) (metis (no_types) comp_apply hyp image_image)
also have "... = (⨅n. fpower f n x)"
by (subst fInf_unfold, auto)
finally show ?thesis
by (simp add: fstar_def image_comp)
qed

lemma fstar_fiter_id: "Inf_pres f ⟹ fstar f = fiter_id f"
proof-
assume hyp: "Inf_pres f"
{fix x::"'a::complete_lattice"
have "fstar f x = x ⊓ f (fstar f x)"
by (simp add: hyp)
hence a: "fstar f x ≤ gfp (λy. x ⊓ f y)"
by (metis gfp_upperbound order_refl)
have "∀y. y ≤ x ⊓ f y ⟶ y ≤ fstar f x"
by (meson H_Inf_pres_fstar H_iso_cond2 Inf_pres_iso fstar_Inf_pres hyp le_infE)
hence "fstar f x = gfp (λy. x ⊓ f y)"
by (metis a antisym gfp_least)}
thus ?thesis
by (simp add: fun_eq_iff Inf_pres_iso fstar_pred_char hyp)
qed

lemma fstar_unfoldl [simp]:
fixes f :: "'a::complete_lattice ⇒ 'a"
shows "Inf_pres f ⟹ id ⊓ (f ∘ fstar f) = fstar f"
by (simp add: fun_eq_iff)

lemma fpower_Inf_comm:
fixes f :: "'a::complete_lattice ⇒ 'a"
shows "Inf_pres f ⟹ f (⨅i. fpower f i x) = (⨅i. fpower f i (f x))"
proof-
assume "Inf_pres f"
hence "f (⨅i. fpower f i x) = (⨅i. fpower f (Suc i) x)"
by (simp add: fun_eq_iff image_comp)
also have "... =  (⨅i. fpower f i (f x))"
by (metis comp_eq_dest_lhs fun_mon.power_Suc2)
finally show ?thesis .
qed

lemma fstar_comm:
fixes f :: "'a::complete_lattice ⇒ 'a"
shows "Inf_pres f ⟹ f ∘ fstar f = fstar f ∘ f"
apply (simp add: fun_eq_iff fstar_def image_comp)
by (metis (mono_tags, lifting) INF_cong comp_eq_dest fun_mon.power_commutes)

lemma fstar_unfoldr [simp]:
fixes f :: "'a::complete_lattice ⇒ 'a"
shows "Inf_pres f ⟹ id ⊓ (fstar f ∘ f) = fstar f"
using fstar_comm fstar_unfoldl by fastforce

subsection ‹Quantales of Inf- and Top-Preserving Transformers›

text ‹As for itotone transformers, types must now be restricted to a single one. It is well known that Inf-preserving transformers need not be
top-preserving, and that Sup-preserving transformers need not be bot-preserving. This has been shown elsewhere. This does not affect the following proof,
but it has an impact on how elements are represented. I show only the result for Inf-preserving transformers; that for Sup-preserving ones is dual.›

typedef (overloaded) 'a Inf_pres = "{f::'a::complete_lattice ⇒ 'a. Inf_pres f}"
using Inf_pres_topf by blast

setup_lifting type_definition_Inf_pres

instantiation Inf_pres :: (complete_lattice) unital_Sup_quantale
begin

lift_definition one_Inf_pres :: "'a::complete_lattice Inf_pres" is id
by (simp add: iso_id)

lift_definition times_Inf_pres :: "'a::complete_lattice Inf_pres ⇒ 'a Inf_pres ⇒ 'a Inf_pres" is "(∘)"
by (simp add: Inf_pres_comp)

lift_definition Sup_Inf_pres :: "'a::complete_lattice Inf_pres set ⇒ 'a Inf_pres" is Inf
by (simp add: Inf_pres_Inf)

lift_definition less_eq_Inf_pres :: "'a Inf_pres ⇒ 'a Inf_pres ⇒ bool" is "(≥)".

lift_definition  less_Inf_pres :: "'a Inf_pres ⇒ 'a Inf_pres ⇒ bool" is "(>)".

instance
by (intro_classes; transfer, simp_all add: o_assoc Inf_lower Inf_greatest fInf_distr_var fInf_distl_var)

end

text ‹Three comments seem worth making. Firstly, the result bakes in duality by considering Infs in the function space as
Sups in the quantale, hence as Infs in the dual quantale. Secondly, the use of Sup-quantales not only reduces the number of proof obligations.
It also copes with the fact that Sups and top are not represented faithfully by this construction. They are generally different from
those in the super-quantale of isotone transformers. But of course they can be defined from Infs as usual. Alternatively, I could have
proved the results for Inf-quantales, which may have been more straightforward. But Sup-lattices are more conventional.
Thirdly, as in the case of isotone transformers, the proof depends on a restriction to one single type, whereas previous results have
been obtained for poly-typed quantales or quantaloids.›

end


(*
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›

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" ("_⇧†"  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, hide_lams) 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" ("op⇩K") where
"op⇩K = ℱ ∘ (⌣) ∘ ℛ"

text ‹Kop is a contravariant functor.›

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

lemma kop_func2 [simp]: "op⇩K η = η"
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]: "op⇩K ∘ op⇩K = id"
unfolding kop_def comp_def fun_eq_iff by (metis converse_converse id_apply r2f_f2r_galois)

lemma kop_galois: "(op⇩K f = g) = (op⇩K g = f)"
by (metis kop_idem pointfree_idE)

lemma kop_galois_var: "(op⇩K ∘ f = g) = (op⇩K ∘ g = f)"
by (auto simp: kop_def f2r_def r2f_def converse_def fun_eq_iff)

lemma kop_galois_var2: "(f ∘ op⇩K = g) = (g ∘ op⇩K = f)"
by (metis (no_types, hide_lams) comp_assoc comp_id kop_idem)

lemma kop_inj: "inj op⇩K"
unfolding inj_def by (simp add: f2r_inj_iff kop_def r2f_inj_iff)

lemma kop_inj_iff: "(op⇩K f = op⇩K g) = (f = g)"
by (simp add: inj_eq kop_inj)

lemma kop_surj: "surj op⇩K"
unfolding surj_def by (metis kop_galois)

lemma kop_bij: "bij op⇩K"
by (simp add: bij_def kop_inj kop_surj)

lemma kop_mono: "(op⇩K ∘ f = op⇩K ∘ g) ⟹ (f = g)"
by (simp add: fun.inj_map inj_eq kop_inj)

lemma kop_mono_iff: "(op⇩K ∘ f = op⇩K ∘ g) = (f = g)"
using kop_mono by blast

lemma kop_epi: "(f ∘ op⇩K = g ∘ op⇩K) ⟹ (f = g)"
by (metis kop_galois_var2)

lemma kop_epi_iff: "(f ∘ op⇩K = g ∘ op⇩K) = (f = g)"
using kop_epi by blast

lemma Sup_pres_kop: "Sup_pres op⇩K"
unfolding kop_def fun_eq_iff comp_def r2f_def f2r_def converse_def by auto

lemma Inf_pres_kop: "Inf_pres op⇩K"
unfolding kop_def fun_eq_iff comp_def r2f_def f2r_def converse_def by auto

end

# Theory 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

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⇩ℱ ∘ op⇩K"

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⇩ℱ (op⇩K f) ∘ ∂"
by (simp add: ffb_def map_dual_def)

lemma ffb_prop_var: "fb⇩ℱ f = uminus ∘ bd⇩ℱ (op⇩K f) ∘ uminus"
by (simp add: dual_set_def ffb_prop)

lemma ffb_fbd_dual: "∂ ∘ fb⇩ℱ f = bd⇩ℱ (op⇩K 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⇧-⇩ℱ φ = (op⇩K ∘ bd⇧-⇩ℱ ∘ ∂⇩F) φ"
proof-
assume h: "Inf_pres φ"
{fix f
have "(fb⇧-⇩ℱ φ = f) = ((∂⇩F ∘ bd⇩ℱ ∘ op⇩K) f = φ)"
by (simp add: ffb_def ffb_iffb_galois h)
also have "... = (op⇩K 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 = (op⇩K ∘ bd⇧-⇩ℱ ∘ ∂⇩F) φ)"
using kop_galois by auto}
thus ?thesis
by blast
qed

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

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

lemma ifbd_iffb_dual: "Sup_pres φ ⟹ bd⇧-⇩ℱ φ = (op⇩K ∘ fb⇧-⇩ℱ ∘ ∂⇩F) φ"
proof-
assume h: "Sup_pres φ"
hence "Inf_pres (∂⇩F φ)"
using Sup_pres_Inf_pres by blast
hence "(op⇩K ∘ fb⇧-⇩ℱ ∘ ∂⇩F) φ = (op⇩K ∘ (op⇩K ∘ 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⇩ℱ (op⇩K (f ∘⇩K g)))"
by (simp add: ffb_def)
also have "... = ∂⇩F (bd⇩ℱ (op⇩K g ∘⇩K op⇩K f))"
by (simp add: kop_contrav)
also have "... = ∂⇩F (bd⇩ℱ (op⇩K f) ∘ bd⇩ℱ (op⇩K g))"
by (simp add: fbd_comp_pres)
also have "... = ∂⇩F (bd⇩ℱ (op⇩K f)) ∘ ∂⇩F (bd⇩ℱ (op⇩K 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⇩ℱ ∘ op⇩K"

definition iffd :: "('b set ⇒ 'a set) ⇒ 'a ⇒ 'b set" ("fd⇧-⇩ℱ") where
"fd⇧-⇩ℱ = op⇩K ∘ 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⇩ℱ ∘ op⇩K"

definition ifbb :: "('a  set ⇒ 'b set) ⇒ 'a ⇒ 'b set" ("bb⇧-⇩ℱ") where
"bb⇧-⇩ℱ = op⇩K ∘ 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⇩ℱ ∘ op⇩K"
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⇧-⇩ℛ = ℛ ∘ op⇩K ∘ 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⇧-⇩ℱ φ = (op⇩K ∘ fb⇧-⇩ℱ) φ"
by (simp add: ifbb_def)
also have "... = (op⇩K ∘ op⇩K ∘ 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⇩ℱ (op⇩K f) ∘ ∂"
by (simp add: fbd_fbb_demorgan ffd_def)

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

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

lemma ifbb_iffd_dual: "Inf_pres φ ⟹ bb⇧-⇩ℱ φ = (op⇩K ∘ 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"

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, hide_lams) 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 join_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

# Theory Kleisli_Quantaloid

(*
Title: The Quantaloid of Kleisli Arrows
Author: Georg Struth
Maintainer: Georg Struth <g.struth@sheffield.ac.uk>
*)

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,DesharnaisS11}.›

definition "kad f = (λx. if (f x = {}) then {x} else {})"

definition "ad_rel R = {(x,x) |x. ¬(∃y. (x,y) ∈ R)}"

by simp_all (meson empty_iff singletonD)

lemma ad_fun_as1 [simp]: "(kad f) ∘⇩K f = ζ"

by (force simp: kad_def kcomp_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))"

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



# Theory Kleisli_Quantale

(*
Title: The Quantale of Kleisli Arrows
Author: Georg Struth
Maintainer: Georg Struth <g.struth@sheffield.ac.uk>
*)

section ‹The Quantale of Kleisli Arrows›

theory Kleisli_Quantale
imports Kleisli_Quantaloid
"Quantales.Quantale_Star"

begin

text ‹This component revisits the results of the quantaloid one in the single-typed setting, that is, in
the context of quantales. An instance proof, showing that Kleisli arrows (or state transformers) form quantales, is
its main result. Facts proved for quantales are thus made available for state transformers.›

typedef 'a nd_fun = "{f::'a ⇒ 'a set. f ∈ UNIV}"
by simp

setup_lifting type_definition_nd_fun

text ‹Definitions are lifted to gain access to the Kleisli categories.›

lift_definition r2fnd :: "'a rel ⇒ 'a nd_fun" is "Abs_nd_fun ∘ ℱ".

lift_definition f2rnd :: "'a nd_fun ⇒ 'a rel" is "ℛ ∘ Rep_nd_fun".

declare Rep_nd_fun_inverse [simp]

lemma r2f2r_inv: "r2fnd ∘ f2rnd = id"
by transfer (simp add: fun_eq_iff pointfree_idE)

lemma f2r2f_inv: "f2rnd ∘ r2fnd = id"
by transfer (simp add: fun_eq_iff r2f_def f2r_def Abs_nd_fun_inverse)

instantiation nd_fun :: (type) monoid_mult
begin

lift_definition one_nd_fun :: "'a nd_fun" is "Abs_nd_fun η".

lift_definition times_nd_fun :: "'a::type nd_fun ⇒ 'a::type nd_fun ⇒ 'a::type nd_fun" is "λf g. Abs_nd_fun (Rep_nd_fun f ∘⇩K Rep_nd_fun g)".

instance
by intro_classes (transfer, simp add: Abs_nd_fun_inverse kcomp_assoc)+

end

instantiation nd_fun :: (type) order_lean
begin

lift_definition less_eq_nd_fun :: "'a nd_fun ⇒ 'a nd_fun ⇒ bool" is "λf g. Rep_nd_fun f ≤ Rep_nd_fun g".

lift_definition less_nd_fun :: "'a nd_fun ⇒ 'a nd_fun ⇒ bool" is "λf g. Rep_nd_fun f ≤ Rep_nd_fun g ∧ f ≠ g".

instance
apply intro_classes
apply (transfer, simp)
apply transfer using order.trans apply blast
by (simp add: Rep_nd_fun_inject less_eq_nd_fun.abs_eq)

end

instantiation nd_fun :: (type) Sup_lattice
begin

lift_definition Sup_nd_fun :: "'a nd_fun set ⇒ 'a nd_fun" is "Abs_nd_fun ∘ Sup ∘ 𝒫 Rep_nd_fun".

instance
by (intro_classes; transfer, simp_all add: Abs_nd_fun_inverse Sup_upper sup_absorb2 Sup_le_iff)

end

lemma Abs_comp_hom: "Abs_nd_fun (f ∘⇩K g) = Abs_nd_fun f ⋅ Abs_nd_fun g"
by transfer (simp add: Abs_nd_fun_inverse)

lemma Rep_comp_hom: "Rep_nd_fun (f ⋅ g) = Rep_nd_fun f ∘⇩K Rep_nd_fun g"
by (simp add: Abs_nd_fun_inverse times_nd_fun.abs_eq)

instance nd_fun :: (type) unital_Sup_quantale
by (intro_classes; transfer, simp_all) (smt Abs_comp_hom Rep_comp_hom Rep_nd_fun_inverse SUP_cong image_image kSup_distr kSup_distl)+

text ‹Unfortunately, this is not it yet. To benefit from Isabelle's theorems for orderings, lattices,
Kleene algebras and quantales, Isabelle's complete lattices need to be in scope. Somewhat annoyingly, this
requires more work...›

instantiation nd_fun :: (type) complete_lattice
begin

lift_definition Inf_nd_fun :: "'a nd_fun set ⇒ 'a nd_fun" is "Abs_nd_fun ∘ Inf ∘ 𝒫 Rep_nd_fun".

lift_definition bot_nd_fun :: "'a::type nd_fun" is "Abs_nd_fun (Sup {})".

lift_definition sup_nd_fun :: "'a::type nd_fun ⇒ 'a::type nd_fun ⇒ 'a::type nd_fun" is "λf g. Abs_nd_fun (Rep_nd_fun f ⊔ Rep_nd_fun g)".

lift_definition top_nd_fun :: "'a::type nd_fun" is "Abs_nd_fun (Inf {})".

lift_definition inf_nd_fun :: "'a::type nd_fun ⇒ 'a::type nd_fun ⇒ 'a::type nd_fun" is "λf g. Abs_nd_fun (Rep_nd_fun f ⊓ Rep_nd_fun g)".

instance
apply intro_classes
apply transfer using Rep_nd_fun_inject dual_order.antisym apply blast
apply (transfer, simp)
apply (transfer, simp)
apply (simp add: Abs_nd_fun_inverse)
by (transfer; simp_all add: Abs_nd_fun_inverse Sup_le_iff SUP_upper2 le_INF_iff Inf_lower)+

end

instance nd_fun :: (type) unital_quantale
apply intro_classes
using supq.Sup_distr apply fastforce
by (simp add: supq.Sup_distl)

text ‹Now, theorems for the Kleene star, which come from quantales, are finally in scope.›

lemma fun_star_unfoldl_eq: "(1::'a nd_fun) ⊔ f ⋅ qstar f = qstar f"
by (simp add: qstar_comm)

lemma fun_star_unfoldl: "(1::'a nd_fun) ⊔ f ⋅ qstar f ≤ qstar f"
using qstar_unfoldl by blast

lemma fun_star_unfoldr_eq: "(1::'a nd_fun) ⊔ (qstar f) ⋅ f = qstar f"
by simp

lemma fun_star_unfoldr: "(1::'a nd_fun) ⊔ qstar f ⋅ f ≤ qstar f"
by (simp add: fun_star_unfoldr_eq)

lemma fun_star_inductl: "(h::'a nd_fun) ⊔ f ⋅ g ≤ g ⟹ qstar f ⋅  h ≤ g"
using qstar_inductl by blast

lemma fun_star_inductr: "(h::'a nd_fun) ⊔ g ⋅ f ≤ g ⟹ h ⋅ qstar f ≤ g"
by (simp add: qstar_inductr)

end