Theory Domain_Quantale

(* Title: Domain Quantales
   Author: Victor Gomes, Georg Struth
   Maintainer: Victor Gomes <victor.gomes@cl.cam.ac.uk>
               Georg Struth <g.struth@sheffield.ac.uk> 
*)

section ‹Component for Recursive Programs›

theory Domain_Quantale
  imports KAD.Modal_Kleene_Algebra

begin

text ‹This component supports the verification and step-wise refinement of recursive programs
in a partial correctness setting.›

notation
  times (infixl "⋅" 70) and
  bot ("⊥") and
  top ("⊤") and
  inf (infixl "⊓" 65) and
  sup (infixl "⊔" 65)

subsection ‹Lattice-Ordered Monoids with Domain›

class bd_lattice_ordered_monoid = bounded_lattice + distrib_lattice + monoid_mult +
  assumes left_distrib: "x ⋅ (y ⊔ z) = x ⋅ y ⊔ x ⋅ z"
  and right_distrib: "(x ⊔ y) ⋅ z = x ⋅ z ⊔ y ⋅ z"
  and bot_annil [simp]: "⊥ ⋅ x = ⊥"
  and bot_annir [simp]: "x ⋅ ⊥ = ⊥"

begin

sublocale semiring_one_zero "(⊔)" "(⋅)" "1" "bot" 
  by (standard, auto simp: sup.assoc sup.commute sup_left_commute left_distrib right_distrib sup_absorb1)   

sublocale dioid_one_zero "(⊔)" "(⋅)" "1" bot "(≤)" "(<)"
  by (standard, simp add: le_iff_sup, auto)

end

no_notation ads_d ("d")
  and ars_r ("r")
  and antirange_op ("ar _" [999] 1000)

class domain_bdlo_monoid = bd_lattice_ordered_monoid +
  assumes rdv: "(z ⊓ x ⋅ top) ⋅ y = z ⋅ y ⊓ x ⋅ top"  

begin 

definition "d x = 1 ⊓ x ⋅ ⊤"

sublocale ds: domain_semiring "(⊔)" "(⋅)" "1" "⊥" "d" "(≤)" "(<)"
proof standard
  fix x y
  show "x ⊔ d x ⋅ x = d x ⋅ x"
    by (metis d_def inf_sup_absorb left_distrib mult_1_left mult_1_right rdv sup.absorb_iff1 sup.idem sup.left_commute top_greatest)
  show "d (x ⋅ d y) = d (x ⋅ y)"
    by (simp add: d_def inf_absorb2 rdv  mult_assoc)
  show "d x ⊔ 1 = 1"
    by (simp add: d_def sup.commute)
  show "d bot = bot"
    by (simp add: d_def inf.absorb1 inf.commute)
  show "d (x ⊔ y) = d x ⊔ d y"
    by (simp add: d_def inf_sup_distrib1)
qed

end

subsection‹Boolean Monoids with Domain›

class boolean_monoid = boolean_algebra + monoid_mult +  
  assumes left_distrib': "x ⋅ (y ⊔ z) = x ⋅ y ⊔ x ⋅ z"
  and right_distrib': "(x ⊔ y) ⋅ z = x ⋅ z ⊔ y ⋅ z"
  and bot_annil' [simp]: "⊥ ⋅ x = ⊥"
  and bot_annir' [simp]: "x ⋅ ⊥ = ⊥"

begin

subclass bd_lattice_ordered_monoid
  by (standard, simp_all add: left_distrib' right_distrib')

lemma inf_bot_iff_le: "x ⊓ y = ⊥ ⟷ x ≤ -y"
  by (metis le_iff_inf inf_sup_distrib1 inf_top_right sup_bot.left_neutral sup_compl_top compl_inf_bot inf.assoc inf_bot_right)

end

class domain_boolean_monoid = boolean_monoid + 
  assumes rdv': "(z ⊓ x ⋅ ⊤) ⋅ y = z ⋅ y ⊓ x ⋅ ⊤"     

begin

sublocale dblo: domain_bdlo_monoid "1" "(⋅)" "(⊓)" "(≤)" "(<)" "(⊔)" "⊥" "⊤"
  by (standard, simp add: rdv')

definition "a x = 1 ⊓ -(dblo.d x)"
                                
lemma a_d_iff: "a x = 1 ⊓ -(x ⋅ ⊤)"
  by (clarsimp simp: a_def dblo.d_def inf_sup_distrib1) 

lemma topr: "-(x ⋅ ⊤) ⋅ ⊤ = -(x ⋅ ⊤)" 
proof (rule order.antisym)
  show "-(x ⋅ ⊤) ≤ -(x ⋅ ⊤) ⋅ ⊤"
    by (metis mult_isol_var mult_oner order_refl top_greatest)
  have "-(x ⋅ ⊤) ⊓ (x ⋅ ⊤) = ⊥"
    by simp
  hence "(-(x ⋅ ⊤) ⊓ (x ⋅ ⊤)) ⋅ ⊤  = ⊥"
    by simp 
  hence "-(x ⋅ ⊤) ⋅ ⊤ ⊓ (x ⋅ ⊤)  = ⊥"
    by (metis rdv') 
  thus "-(x ⋅ ⊤) ⋅ ⊤ ≤ -(x ⋅ ⊤)"
    by (simp add: inf_bot_iff_le)
qed

lemma dd_a: "dblo.d x = a (a x)"
  by (metis a_d_iff dblo.d_def double_compl inf_top.left_neutral mult_1_left rdv' topr)

lemma ad_a [simp]: "a (dblo.d x) = a x"
  by (simp add: a_def)

lemma da_a [simp]: "dblo.d (a x) = a x"
  using ad_a dd_a by auto

lemma a1 [simp]: "a x ⋅ x = ⊥"
proof -
  have "a x ⋅ x ⋅ ⊤ = ⊥"
    by (metis a_d_iff inf_compl_bot mult_1_left rdv' topr)
  then show ?thesis
    by (metis (no_types) dblo.d_def dblo.ds.domain_very_strict inf_bot_right)
qed

lemma a2 [simp]: "a (x ⋅ y) ⊔ a (x ⋅ a (a y)) = a (x ⋅ a (a y))"
  by (metis a_def dblo.ds.dsr2 dd_a sup.idem)

lemma a3 [simp]: "a (a x) ⊔ a x = 1"
  by (metis a_def da_a inf.commute sup.commute sup_compl_top sup_inf_absorb sup_inf_distrib1)

subclass domain_bdlo_monoid ..

text ‹The next statement shows that every boolean monoid with domain is an antidomain semiring. 
In this setting the domain operation has been defined explicitly.›

sublocale ad: antidomain_semiring a "(⊔)" "(⋅)" "1" "⊥" "(≤)" "(<)"
  rewrites ad_eq: "ad.ads_d x = d x"
proof -
  show "class.antidomain_semiring a (⊔) (⋅) 1 ⊥ (≤) (<)"
    by (standard, simp_all)
  then interpret ad: antidomain_semiring a "(⊔)" "(⋅)" "1" "⊥" "(≤)" "(<)" .
  show "ad.ads_d x = d x"
    by (simp add: ad.ads_d_def dd_a)
qed

end 

subsection‹Boolean Monoids with Range›

class range_boolean_monoid = boolean_monoid + 
  assumes ldv': "y ⋅ (z ⊓ ⊤ ⋅ x) = y ⋅ z ⊓ ⊤ ⋅ x"

begin

definition "r x = 1 ⊓ ⊤ ⋅ x"

definition "ar x = 1 ⊓ -(r x)"
                                
lemma ar_r_iff: "ar x = 1 ⊓ -(⊤ ⋅ x)"
  by (simp add: ar_def inf_sup_distrib1 r_def)

lemma topl: "⊤⋅(-(⊤ ⋅ x)) = -(⊤ ⋅ x)" 
proof (rule order.antisym)
  show "⊤ ⋅ - (⊤ ⋅ x) ≤ - (⊤ ⋅ x)"
    by (metis bot_annir' compl_inf_bot inf_bot_iff_le ldv')
  show "- (⊤ ⋅ x) ≤ ⊤ ⋅ - (⊤ ⋅ x)"
    by (metis inf_le2 inf_top.right_neutral mult_1_left mult_isor)
qed

lemma r_ar: "r x = ar (ar x)"
  by (metis ar_r_iff double_compl inf.commute inf_top.right_neutral ldv' mult_1_right r_def topl)

lemma ar_ar [simp]: "ar (r x) = ar x"
  by (simp add: ar_def ldv' r_def)

lemma rar_ar [simp]: "r (ar x) = ar x"
  using r_ar ar_ar by force

lemma ar1 [simp]: "x ⋅ ar x = ⊥"
proof -
  have "⊤ ⋅ x ⋅ ar x = ⊥"
    by (metis ar_r_iff inf_compl_bot ldv' mult_oner topl)
  then show ?thesis
    by (metis inf_bot_iff_le inf_le2 inf_top.right_neutral mult_1_left mult_isor mult_oner topl)
qed

lemma ars: "r (r x ⋅ y) = r (x ⋅ y)"
  by (metis inf.commute inf_top.right_neutral ldv' mult_oner mult_assoc r_def)

lemma ar2 [simp]: "ar (x ⋅ y) ⊔ ar (ar (ar x) ⋅ y) = ar (ar (ar x) ⋅ y)"
  by (metis ar_def ars r_ar sup.idem)
                         
lemma ar3 [simp]: "ar (ar x) ⊔ ar x = 1 "
  by (metis ar_def rar_ar inf.commute sup.commute sup_compl_top sup_inf_absorb sup_inf_distrib1)

sublocale ar: antirange_semiring "(⊔)" "(⋅)" "1" "⊥" ar "(≤)" "(<)"
  rewrites ar_eq: "ar.ars_r x = r x"
proof -
  show "class.antirange_semiring (⊔) (⋅) 1 ⊥ ar (≤) (<)"
    by (standard, simp_all)
  then interpret ar: antirange_semiring "(⊔)" "(⋅)" "1" "⊥" ar "(≤)" "(<)" .
  show "ar.ars_r x = r x"
    by (simp add: ar.ars_r_def r_ar)
qed

end

subsection ‹Quantales›

text ‹This part will eventually move into an AFP quantale entry.› 

class quantale = complete_lattice + monoid_mult +
  assumes Sup_distr: "Sup X ⋅ y = Sup {z. ∃x ∈ X. z = x ⋅ y}"
  and Sup_distl: "x ⋅ Sup Y = Sup {z. ∃y ∈ Y. z = x ⋅ y}"       

begin

lemma bot_annil'' [simp]: "⊥ ⋅ x = ⊥"
  using Sup_distr[where X="{}"] by auto

lemma bot_annirr'' [simp]: "x ⋅ ⊥ = ⊥"
  using Sup_distl[where Y="{}"] by auto

lemma sup_distl: "x ⋅ (y ⊔ z) = x ⋅ y ⊔ x ⋅ z"
  using Sup_distl[where Y="{y, z}"] by (fastforce intro!: Sup_eqI)

lemma sup_distr: "(x ⊔ y) ⋅ z = x ⋅ z ⊔ y ⋅ z"
  using Sup_distr[where X="{x, y}"] by (fastforce intro!: Sup_eqI)

sublocale semiring_one_zero "(⊔)" "(⋅)" "1" "⊥" 
  by (standard, auto simp: sup.assoc sup.commute sup_left_commute sup_distl sup_distr)     

sublocale dioid_one_zero "(⊔)" "(⋅)" "1" "⊥" "(≤)" "(<)"
  by (standard, simp add: le_iff_sup, auto)

lemma Sup_sup_pred: "x ⊔ Sup{y. P y} = Sup{y. y = x ∨ P y}"
  apply (rule order.antisym)
  apply (simp add: Collect_mono Sup_subset_mono Sup_upper) 
  using Sup_least Sup_upper le_supI2 by fastforce

definition star :: "'a ⇒ 'a" where
  "star x = (SUP i. x ^ i)"

lemma star_def_var1: "star x = Sup{y. ∃i. y = x ^ i}"
  by (simp add: star_def full_SetCompr_eq)

lemma star_def_var2: "star x = Sup{x ^ i |i. True}"
  by (simp add: star_def full_SetCompr_eq)

lemma star_unfoldl' [simp]: "1 ⊔ x ⋅ (star x) = star x"
proof -
  have "1 ⊔ x ⋅ (star x) = x ^ 0 ⊔ x ⋅ Sup{y. ∃i. y = x ^ i}"
    by (simp add: star_def_var1)
  also have "... = x ^ 0 ⊔ Sup{y. ∃i. y = x ^ (i + 1)}"
    by (simp add: Sup_distl, metis)
  also have "... = Sup{y. y = x ^ 0 ∨ (∃i. y = x ^ (i + 1))}"
    using Sup_sup_pred by simp
  also have "... = Sup{y. ∃i. y = x ^ i}"
    by (metis Suc_eq_plus1 power.power.power_Suc power.power_eq_if)
  finally show ?thesis
    by (simp add: star_def_var1)
qed

lemma star_unfoldr' [simp]: "1 ⊔ (star x) ⋅ x = star x"
proof -
  have "1 ⊔ (star x) ⋅ x = x ^ 0 ⊔ Sup{y. ∃i. y = x ^ i} ⋅ x"
    by (simp add: star_def_var1)
  also have "... = x ^ 0 ⊔ Sup{y. ∃i. y = x ^ i ⋅ x}"
    by (simp add: Sup_distr, metis)
  also have "... = x ^ 0 ⊔ Sup{y. ∃i. y = x ^ (i + 1)}"
    using power_Suc2 by simp 
   also have "... = Sup{y. y = x ^ 0 ∨ (∃i. y = x ^ (i + 1))}"
    using Sup_sup_pred by simp
  also have "... = Sup{y. ∃i. y = x ^ i}"
    by (metis Suc_eq_plus1 power.power.power_Suc power.power_eq_if)
  finally show ?thesis
    by (simp add: star_def_var1)
qed

lemma (in dioid_one_zero) power_inductl: "z + x ⋅ y ≤ y ⟹ (x ^ n) ⋅ z ≤ y"
proof (induct n)
  case 0 show ?case
    using "0.prems" by simp
  case Suc thus ?case
    by (simp, metis mult.assoc mult_isol order_trans)
qed

lemma (in dioid_one_zero) power_inductr: "z + y ⋅ x ≤ y ⟹ z ⋅ (x ^ n) ≤ y"
proof (induct n)
  case 0 show ?case
    using "0.prems" by auto
  case Suc
  {
    fix n
    assume "z + y ⋅ x ≤ y ⟹ z ⋅ x ^ n ≤ y"
      and "z + y ⋅ x ≤ y"
    hence "z ⋅ x ^ n ≤ y"
      by simp
    also have "z ⋅ x ^ Suc n = z ⋅ x ⋅ x ^ n"
      by (metis mult.assoc power_Suc)
    moreover have "... = (z ⋅ x ^ n) ⋅ x"
      by (metis mult.assoc power_commutes)
    moreover have "... ≤ y ⋅ x"
      by (metis calculation(1) mult_isor)
    moreover have "... ≤ y"
      using ‹z + y ⋅ x ≤ y› by simp
    ultimately have "z ⋅ x ^ Suc n ≤ y" by simp
  }
  thus ?case
    by (metis Suc)
qed

lemma star_inductl': "z ⊔ x ⋅ y ≤ y ⟹ (star x) ⋅ z ≤ y" 
proof -
  assume "z ⊔ x ⋅ y ≤ y"
  hence "∀i. x ^ i ⋅ z ≤ y"
    by (simp add: power_inductl)
  hence "Sup{w. ∃i. w = x ^ i ⋅ z} ≤ y"
    by (intro Sup_least, fast)
  hence "Sup{w. ∃i. w = x ^ i} ⋅ z ≤ y"
    using Sup_distr Sup_le_iff by auto
  thus "(star x) ⋅ z ≤ y"
    by (simp add: star_def_var1)
qed

lemma star_inductr': "z ⊔ y ⋅ x ≤ y ⟹ z ⋅ (star x) ≤ y" 
proof -
  assume "z ⊔ y ⋅ x ≤ y"
  hence "∀i. z ⋅ x ^ i  ≤ y"
    by (simp add: power_inductr)
  hence "Sup{w. ∃i. w = z ⋅ x ^ i} ≤ y"
    by (intro Sup_least, fast)
  hence "z ⋅ Sup{w. ∃i. w = x ^ i} ≤ y"
    using Sup_distl Sup_le_iff by auto
  thus "z ⋅ (star x) ≤ y"
    by (simp add: star_def_var1)
qed

sublocale ka: kleene_algebra "(⊔)" "(⋅)" "1" "⊥" "(≤)" "(<)" star
  by standard (simp_all add: star_inductl' star_inductr')

end

text ‹Distributive quantales are often assumed to satisfy infinite distributivity laws between
joins and meets, but finite ones suffice for our purposes.›

class distributive_quantale = quantale + distrib_lattice 

begin

subclass bd_lattice_ordered_monoid
  by (standard, simp_all add: distrib_left)

lemma "(1 ⊓ x ⋅ ⊤) ⋅ x = x"
(* nitpick [expect=genuine]*)
oops

end 

subsection ‹Domain Quantales›

class domain_quantale = distributive_quantale +
  assumes rdv'': "(z ⊓ x ⋅ ⊤) ⋅ y = z ⋅ y ⊓ x ⋅ ⊤"  

begin

subclass domain_bdlo_monoid 
  by (standard, simp add: rdv'')

end

class range_quantale = distributive_quantale +
  assumes ldv'': "y ⋅ (z ⊓ ⊤ ⋅ x) = y ⋅ z ⊓ ⊤ ⋅ x"

class boolean_quantale = quantale + complete_boolean_algebra

begin

subclass boolean_monoid
  by (standard, simp_all add: sup_distl)

lemma "(1 ⊓ x ⋅ ⊤) ⋅ x = x"
(*nitpick[expect=genuine]*)
oops

lemma "(1 ⊓ -(x ⋅ ⊤)) ⋅ x = ⊥"
(*nitpick[expect=genuine]*)
oops

end

subsection‹Boolean Domain Quantales› 

class domain_boolean_quantale = domain_quantale + boolean_quantale

begin

subclass domain_boolean_monoid
  by (standard, simp add: rdv'')

lemma fbox_eq: "ad.fbox x q = Sup{d p |p. d p ⋅ x ≤ x ⋅ d q}"
  apply (rule Sup_eqI[symmetric])
  apply clarsimp
  using ad.fbox_demodalisation3 ad.fbox_simp apply auto[1]
  apply clarsimp
  by (metis ad.fbox_def ad.fbox_demodalisation3 ad.fbox_simp da_a eq_refl)

lemma fdia_eq: "ad.fdia x p = Inf{d q |q. x ⋅ d p ≤ d q ⋅ x}"
  apply (rule Inf_eqI[symmetric])
  apply clarsimp
  using ds.fdemodalisation2 apply auto[1]
  apply clarsimp
  by (metis ad.fd_eq_fdia ad.fdia_def da_a double_compl ds.fdemodalisation2 inf_bot_iff_le inf_compl_bot)

text ‹The specification statement can be defined explicitly.›

definition R :: "'a ⇒ 'a ⇒ 'a" where
  "R p q ≡ Sup{x. (d p) ⋅ x ≤ x ⋅ d q}"

lemma "x ≤ R p q ⟹ d p ≤ ad.fbox x (d q)"
proof (simp add: R_def ad.kat_1_equiv ad.kat_2_equiv)
  assume "x ≤ Sup{x. d p ⋅ x ⋅ a q = ⊥}"
  hence "d p ⋅ x ⋅ a q ≤ d p ⋅ Sup{x. d p ⋅ x ⋅ a q = ⊥} ⋅ a q "
    using mult_double_iso by blast
  also have "... = Sup{d p ⋅ x ⋅ a q |x. d p ⋅ x ⋅ a q = ⊥}"
    apply (subst Sup_distl)
    apply (subst Sup_distr)
    apply clarsimp
    by metis
  also have "... = ⊥"
    by (auto simp: Sup_eqI)
  finally show ?thesis
    using ad.fbox_demodalisation3 ad.kat_3 ad.kat_4 le_bot by blast
qed

lemma "d p ≤ ad.fbox x (d q) ⟹ x ≤ R p q"
  apply (simp add: R_def)
  apply (rule Sup_upper)
  apply simp
  using ad.fbox_demodalisation3 ad.fbox_simp apply auto[1]
done

end

subsection‹Relational Model of Boolean Domain Quantales›

interpretation rel_dbq: domain_boolean_quantale
  ‹(-)› uminus ‹(∩)› ‹(⊆)› ‹(⊂)› ‹(∪)› ‹{}› UNIV ‹⋂› ‹⋃› Id ‹(O)›
  by standard auto


subsection‹Modal Boolean Quantales›

class range_boolean_quantale = range_quantale + boolean_quantale

begin

subclass range_boolean_monoid
  by (standard, simp add: ldv'')

lemma fbox_eq: "ar.bbox x (r q) = Sup{r p |p. x ⋅ r p ≤ (r q) ⋅ x}"
  apply (rule Sup_eqI[symmetric])
  apply clarsimp
  using ar.ardual.fbox_demodalisation3 ar.ardual.fbox_simp apply auto[1]
  apply clarsimp
  by (metis ar.ardual.fbox_def ar.ardual.fbox_demodalisation3 eq_refl rar_ar)

lemma fdia_eq: "ar.bdia x (r p) = Inf{r q |q. (r p) ⋅ x ≤ x ⋅ r q}"
  apply (rule Inf_eqI[symmetric])
  apply clarsimp
  using ar.ars_r_def ar.ardual.fdemodalisation22 ar.ardual.kat_3_equiv_opp ar.ardual.kat_4_equiv_opp apply auto[1]
  apply clarsimp
  using ar.bdia_def ar.ardual.ds.fdemodalisation2 r_ar by fastforce

end

class modal_boolean_quantale = domain_boolean_quantale + range_boolean_quantale +
  assumes domrange' [simp]: "d (r x) = r x"
  and rangedom' [simp]: "r (d x) = d x"

begin

sublocale mka: modal_kleene_algebra "(⊔)" "(⋅)" 1 ⊥ "(≤)" "(<)" star a ar
  by standard (simp_all add: ar_eq ad_eq)

end

no_notation fbox ("( |_] _)" [61,81] 82)
  and antidomain_semiringl_class.fbox ("( |_] _)" [61,81] 82)

notation ad.fbox ("( |_] _)" [61,81] 82)

subsection ‹Recursion Rule›

lemma recursion: "mono (f :: 'a ⇒ 'a :: domain_boolean_quantale) ⟹ 
  (⋀x. d p ≤ |x] d q ⟹ d p ≤ |f x] d q) ⟹  d p ≤ |lfp f] d q"
  apply (erule lfp_ordinal_induct [where f=f], simp)
  by (auto simp: ad.addual.ardual.fbox_demodalisation3 Sup_distr Sup_distl intro: Sup_mono)

text ‹We have already tested this rule in the context of test quantales~cite‹"ArmstrongGS15"›, which is based
on a formalisation of quantales that is currently not in the AFP. The two theories will be merged as
soon as the quantale is available in the AFP.›

end