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 (simp add: Abs_iso_inverse fiter_fun_exp qiter_fun_exp sup_iso.rep_eq times_iso.rep_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"
  unfolding fpower_distr fun_mon.power_commutes by (rule 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, opaque_lifting) 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, opaque_lifting) 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