Theory Quantales

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

section Quantales
  
text This entry will be merged eventually with other quantale entries and become a standalone one.
  
theory Quantales
  imports Main

begin
  
notation sup (infixl "" 60)
  and inf (infixl "" 55)
  and top ("")
  and bot ("")
  and relcomp (infixl ";" 70) 
  and times (infixl "" 70)
  and Sup ("_" [900] 900)  
  and Inf ("_" [900] 900)
  
subsection Properties of Complete Lattices
  
lemma (in complete_lattice) Sup_sup_pred: "x  {y. P y} = {y. y = x  P y}"
  apply (rule order.antisym)
   apply (simp add: Collect_mono Sup_subset_mono Sup_upper)
  using Sup_least Sup_upper sup.coboundedI2 by force

lemma (in complete_lattice) sup_Sup: "x  y = {x,y}"
  by simp
    
lemma (in complete_lattice) sup_Sup_var: "x  y = {z. z  {x,y}}"
  by (metis Collect_mem_eq sup_Sup)
    
lemma (in complete_boolean_algebra) shunt1: "x  y  z  x  -y  z"
proof standard
  assume "x  y  z"
  hence  "-y  (x  y)  -y  z"
    using sup.mono by blast
  hence "-y  x  -y  z"
    by (simp add: sup_inf_distrib1)
  thus "x  -y  z"
    by simp
next
  assume "x  - y  z"
  hence "x  y  (-y  z)  y"
    using inf_mono by auto
  thus  "x  y  z"
    using inf.boundedE inf_sup_distrib2 by auto
qed
  
lemma (in complete_boolean_algebra) meet_shunt: "x  y =   x  -y"
  by (metis bot_least inf_absorb2 inf_compl_bot_left2 shunt1 sup_absorb1)
  
lemma (in complete_boolean_algebra) join_shunt: "x  y =   -x  y"
  by (metis compl_sup compl_top_eq double_compl meet_shunt)
    

subsection  Familes of Proto-Quantales
  
text Proto-Quanales are complete lattices equipped with an operation of composition or multiplication
that need not be associative.
  
class proto_near_quantale = complete_lattice + times + 
  assumes Sup_distr: "X  y = {x  y |x. x  X}"
    
begin
  
lemma mult_botl [simp]: "  x = "
  using Sup_distr[where X="{}"] by auto
  
lemma sup_distr: "(x  y)  z = (x  z)  (y  z)"
  using Sup_distr[where X="{x, y}"] by (fastforce intro!: Sup_eqI)
    
lemma mult_isor: "x  y  x  z  y  z"
  by (metis sup.absorb_iff1 sup_distr)
    
definition bres :: "'a  'a  'a" (infixr "" 60) where 
  "x  z = {y. x  y  z}"

definition fres :: "'a  'a  'a" (infixl "" 60) where 
  "z  y = {x. x  y  z}"

lemma bres_galois_imp: "x  y  z  y  x  z"
  by (simp add: Sup_upper bres_def)
    
lemma fres_galois: "x  y  z  x  z  y"
proof 
  show "x  y  z  x  z  y"
    by (simp add: Sup_upper fres_def)
next
  assume "x  z  y"
  hence "x  y  {x. x  y  z}  y"
    by (simp add: fres_def mult_isor)
  also have "... = {x  y |x. x  y  z}"
    by (simp add: Sup_distr)
  also have "...  z"
    by (rule Sup_least, auto)
  finally show "x  y  z" .
qed
  
end
  
class proto_pre_quantale = proto_near_quantale + 
  assumes Sup_subdistl: "{x  y | y . y  Y}  x  Y"
    
begin

lemma sup_subdistl: "(x  y)  (x  z)  x  (y  z)"
  using Sup_subdistl[where Y="{y, z}"] Sup_le_iff by auto

lemma mult_isol: "x  y  z  x  z  y"
  by (metis le_iff_sup le_sup_iff sup_subdistl)

end
    
class weak_proto_quantale = proto_near_quantale +
  assumes weak_Sup_distl: "Y  {}  x  Y = {x  y |y. y  Y}" 
  
begin

subclass proto_pre_quantale
proof standard
  have a: "x Y. Y = {}  {x  y |y. y  Y}  x  Y"
    by simp
  have b: "x Y. Y  {}  {x  y |y. y  Y}  x  Y"
    by (simp add: weak_Sup_distl)
  show  "x Y. {x  y |y. y  Y}  x  Y"
    using a b by blast 
qed
  
lemma  sup_distl: "x  (y  z) = (x  y)  (x  z)"  
  using weak_Sup_distl[where Y="{y, z}"] by (fastforce intro!: Sup_eqI)

lemma "y  x  z  x  y  z" (* nitpick [expect = genuine] *)
oops

end
  
class proto_quantale = proto_near_quantale +
  assumes Sup_distl: "x  Y = {x  y |y. y  Y}"  

begin
  
subclass weak_proto_quantale
  by standard (simp add: Sup_distl)
    
lemma bres_galois: "x  y  z  y  x  z"
proof 
  show "x  y  z  y  x  z"
    by (simp add: Sup_upper bres_def)
next
  assume "y  x  z"
  hence "x  y  x  {y. x  y  z}"
    by (simp add: bres_def mult_isol)
  also have "... = {x  y |y. x  y  z}"
    by (simp add: Sup_distl)
  also have "...  z"
    by (rule Sup_least, auto)
  finally show "x  y  z" .
qed

end 
  
  
subsection Families of Quantales
  
class near_quantale = proto_near_quantale + semigroup_mult 
  
class unital_near_quantale = near_quantale + monoid_mult

begin

definition iter :: "'a  'a" where
  "iter x  {y. i. y = x ^ i}"

lemma iter_ref [simp]: "iter x  1"
  apply (simp add: iter_def)
  by (metis (mono_tags, lifting) Inf_lower local.power.power_0 mem_Collect_eq)
    
lemma le_top: "x    x"
  by (metis mult_isor mult.monoid_axioms top_greatest monoid.left_neutral)

end
  
class pre_quantale = proto_pre_quantale + semigroup_mult 
  
subclass (in pre_quantale) near_quantale ..
  
class unital_pre_quantale = pre_quantale + monoid_mult
  
subclass (in unital_pre_quantale) unital_near_quantale ..
    
class weak_quantale = weak_proto_quantale + semigroup_mult
  
subclass (in weak_quantale) pre_quantale ..
    
text The following counterexample shows an important consequence of weakness: 
the absence of right annihilation.
    
lemma (in weak_quantale) "x   = " (*nitpick[expect=genuine]*)
  oops
    
class unital_weak_quantale = weak_quantale + monoid_mult
  
lemma (in unital_weak_quantale) "x   = " (*nitpick[expect=genuine]*)
  oops
  
subclass (in unital_weak_quantale) unital_pre_quantale ..
    
class quantale = proto_quantale + semigroup_mult 
  
begin
  
subclass weak_quantale ..   

lemma mult_botr [simp]: "x   = "
  using Sup_distl[where Y="{}"] by auto

end
  
class unital_quantale = quantale + monoid_mult

subclass (in unital_quantale) unital_weak_quantale ..

class ab_quantale = quantale + ab_semigroup_mult

begin

lemma bres_fres_eq: "x  y = y  x" 
  by (simp add: fres_def bres_def mult_commute)

end

class ab_unital_quantale = ab_quantale + unital_quantale
  
class distrib_quantale = quantale + complete_distrib_lattice
  
class bool_quantale = quantale + complete_boolean_algebra 
  
class distrib_unital_quantale = unital_quantale + complete_distrib_lattice
  
class bool_unital_quantale = unital_quantale + complete_boolean_algebra 
  
class distrib_ab_quantale = distrib_quantale + ab_quantale
  
class bool_ab_quantale = bool_quantale + ab_quantale
  
class distrib_ab_unital_quantale = distrib_quantale + unital_quantale
  
class bool_ab_unital_quantale = bool_ab_quantale + unital_quantale
  
  
subsection Quantales of Booleans and Complete Boolean Algebras
  
instantiation bool :: bool_ab_unital_quantale
begin
  
definition "one_bool = True"
  
definition "times_bool = (λx y. x  y)"
  
instance
  by standard (auto simp: times_bool_def one_bool_def)
    
end
  
context complete_distrib_lattice
begin
  
interpretation cdl_quantale: distrib_quantale _ _ _ _ _ _ _ _ inf
  by standard (simp_all add: inf.assoc Setcompr_eq_image Sup_inf inf_Sup)
    
end

context complete_boolean_algebra
begin

interpretation cba_quantale: bool_ab_unital_quantale inf _ _ _ _ _ _ _ _ _ _ top
  apply standard
  apply (simp add: inf.assoc)
  apply (simp add: inf.commute)
  apply (simp add: Setcompr_eq_image Sup_inf)
  apply (simp add: Setcompr_eq_image inf_Sup)
  by simp_all
    
text In this setting, residuation can be translated like classical implication.
  
lemma cba_bres1: "x  y  z  x  cba_quantale.bres y z"
  using cba_quantale.bres_galois inf.commute by fastforce
    
lemma cba_bres2: "x  -y  z  x  cba_quantale.bres y z"
  using cba_bres1 shunt1 by auto
    
lemma cba_bres_prop: "cba_quantale.bres x y = -x  y"
  using cba_bres2 order.eq_iff by blast
  
end
  
text Other models will follow.
  
   
subsection Products of Quantales
  
definition "Inf_prod X = ({fst x |x. x  X}, {snd x |x.  x  X})"
  
definition "inf_prod x y = (fst x  fst y, snd x  snd y)"

definition "bot_prod = (bot,bot)"
  
definition "Sup_prod X = ({fst x |x. x  X}, {snd x |x.  x  X})"
    
definition "sup_prod x y = (fst x  fst y, snd x  snd y)"
    
definition "top_prod = (top,top)"
    
definition "less_eq_prod x y  less_eq (fst x) (fst y)  less_eq (snd x) (snd y)"

definition "less_prod x y  less_eq (fst x) (fst y)  less_eq (snd x) (snd y)  x  y"
  
definition "times_prod' x y = (fst x  fst y, snd x  snd y)"

definition "one_prod = (1,1)"
  
interpretation prod: complete_lattice Inf_prod Sup_prod inf_prod less_eq_prod less_prod sup_prod bot_prod "top_prod :: ('a::complete_lattice × 'b::complete_lattice)"
  apply standard
     apply (simp_all add: Inf_prod_def Sup_prod_def inf_prod_def sup_prod_def bot_prod_def top_prod_def less_eq_prod_def less_prod_def Sup_distl Sup_distr)
        apply force+
     apply (rule conjI, (rule Inf_lower, force)+)
    apply (rule conjI, (rule Inf_greatest, force)+)
   apply (rule conjI, (rule Sup_upper, force)+)
  by (rule conjI, (rule Sup_least, force)+)

interpretation prod: proto_near_quantale Inf_prod Sup_prod inf_prod less_eq_prod less_prod sup_prod bot_prod "top_prod :: ('a::proto_near_quantale × 'b::proto_near_quantale)" times_prod'
  apply (standard, simp add: times_prod'_def Sup_prod_def)
  by (rule conjI, (simp add: Sup_distr, clarify, metis)+)
    
interpretation prod: proto_quantale Inf_prod Sup_prod inf_prod less_eq_prod less_prod sup_prod bot_prod "top_prod :: ('a::proto_quantale × 'b::proto_quantale)" times_prod'
  apply (standard, simp add: times_prod'_def Sup_prod_def less_eq_prod_def)
  by (rule conjI, (simp add: Sup_distl, metis)+)

interpretation prod: unital_quantale one_prod times_prod' Inf_prod Sup_prod inf_prod less_eq_prod less_prod sup_prod bot_prod "top_prod :: ('a::unital_quantale × 'b::unital_quantale)" 
  by standard (simp_all add: one_prod_def times_prod'_def mult.assoc)
    

subsection Quantale Modules and Semidirect Products
  
text Quantale modules are extensions of semigroup actions in that a quantale acts on a complete lattice.
  
locale unital_quantale_module = 
  fixes act :: "'a::unital_quantale  'b::complete_lattice  'b" ("α")
  assumes act1: "α (x  y) p = α x (α y p)"
    and act2 [simp]: "α 1 p = p" 
    and act3: "α (X) p = {α x p |x. x  X}"
    and act4: "α x (P) = {α x p |p. p  P}"

context unital_quantale_module
begin
  
text Actions are morphisms. The curried notation is particularly convenient for this.
  
lemma act_morph1: "α (x  y) = (α x)  (α y)"
  by (simp add: fun_eq_iff act1)
    
lemma act_morph2: "α 1 = id"
  by (simp add: fun_eq_iff)
  
lemma emp_act: "α ({}) p = "
  by (simp only: act3, force)
    
lemma emp_act_var: "α  p = "
  using emp_act by auto

lemma act_emp: "α x ({}) = "
  by (simp only: act4, force)
    
lemma act_emp_var: "α x  = "
  using act_emp by auto
  
lemma act_sup_distl: "α x (p  q) = (α x p)  (α x q)"
proof-
  have "α x (p  q) = α x ({p,q})"
    by simp
  also have "... = {α x y |y. y  {p,q}}"
    by (rule act4)
  also have "... = {v. v = α x p  v = α x q}"
    by (metis empty_iff insert_iff)
  finally show ?thesis
    by (metis Collect_disj_eq Sup_insert ccpo_Sup_singleton insert_def singleton_conv)
qed
  
lemma act_sup_distr: "α (x  y) p = (α x p)  (α y p)"
  proof-
  have "α (x  y) p  = α ({x,y}) p"
    by simp
  also have "... = {α v p |v. v  {x,y}}"
    by (rule act3)
  also have "... = {v. v = α x p  v = α y p}"
    by (metis empty_iff insert_iff)
  finally show ?thesis
    by (metis Collect_disj_eq Sup_insert ccpo_Sup_singleton insert_def singleton_conv)
qed
  
lemma act_sup_distr_var: "α (x  y) = (α x)  (α y)"
  by (simp add: fun_eq_iff act_sup_distr)
    
text Next we define the semidirect product of a  unital quantale and a complete lattice. 
  
definition "sd_prod x y = (fst x  fst y, snd x  α (fst x) (snd y))"
   
lemma sd_distr_aux: 
  "{snd x |x. x  X}  {α (fst x) p |x. x  X} = {snd x  α (fst x) p |x. x  X}"
proof (rule antisym, rule sup_least) 
  show "{snd x |x. x  X}  {snd x  α (fst x) p |x. x  X}"
  proof (rule Sup_least)
    fix x :: 'b
    assume "x  {snd x |x. x  X}"
    hence "b pa. x  b = snd pa  α (fst pa) p  pa  X"
      by blast
    hence "b. x  b  {snd pa  α (fst pa) p |pa. pa  X}"
      by blast
    thus "x  {snd pa  α (fst pa) p |pa. pa  X}"
      by (meson Sup_upper sup.bounded_iff)
  qed  
next
  show "{α (fst x) p |x. x  X}  {snd x  α (fst x) p |x. x  X}"
  proof (rule Sup_least)
    fix x :: 'b
    assume "x  {α (fst x) p |x. x  X}"
    then have "b pa. b  x = snd pa  α (fst pa) p  pa  X"
      by blast
    then have "b. b  x  {snd pa  α (fst pa) p |pa. pa  X}"
      by blast
    then show "x  {snd pa  α (fst pa) p |pa. pa  X}"
      by (meson Sup_upper le_supE)
  qed
next
  show "{snd x  α (fst x) p |x. x  X}  {snd x |x. x  X}  {α (fst x) p |x. x  X}"
    apply (rule Sup_least)
    apply safe 
    apply (rule sup_least)
    apply (metis (mono_tags, lifting) Sup_upper mem_Collect_eq sup.coboundedI1)
    by (metis (mono_tags, lifting) Sup_upper mem_Collect_eq sup.coboundedI2)
qed

lemma sd_distr: "sd_prod (Sup_prod X) y = Sup_prod {sd_prod x y |x. x  X}"
proof -
  have "sd_prod (Sup_prod X) y = sd_prod ({fst x |x. x  X}, {snd x |x. x  X}) y"
    by (simp add: Sup_prod_def)
  also have 
    "... = (({fst x |x. x  X})  fst y, ({snd x |x. x  X})  (α ({fst x | x. x  X})  (snd y)))"
    by (simp add: sd_prod_def)
  also have 
    "... = ({fst x  fst y|x. x  X}, ({snd x |x. x  X})  (α ({fst x | x. x  X})  (snd y)))"
    by (simp add: Sup_distr)
  also have 
    "... = ({fst x  fst y|x. x  X}, ( {snd x |x. x  X})  ({α (fst x) (snd y) | x. x  X}))"
    by (simp add: act3)
  also have "... = ({fst x  fst y|x. x  X}, {snd x  (α (fst x) (snd y)) | x. x  X})"
    by (simp only: sd_distr_aux)
  also have "... = Sup_prod {(fst x  fst y, snd x  (α (fst x) (snd y))) |x. x  X}"
    by (simp add: Sup_prod_def, metis)
  finally show ?thesis
    by (simp add: sd_prod_def)
qed
  
lemma sd_distl_aux: "Y  {}  p  ({α x (snd y) |y. y  Y}) = {p  α x (snd y) |y. y  Y}"
proof (rule antisym, rule sup_least)
  show "Y  {}  p  {p  α x (snd y) |y. y  Y}"
  proof -
    assume "Y  {}"
    hence "b. b  {p  α x (snd pa) |pa. pa  Y}  p  b"
      by fastforce
    thus "p  {p  α x (snd pa) |pa. pa  Y}"
      by (meson Sup_upper2)
  qed
next
  show "Y  {}  {α x (snd y) |y. y  Y}  {p  α x (snd y) |y. y  Y}"  
    apply (rule Sup_least)
  proof -
    fix xa :: 'b
    assume "xa  {α x (snd y) |y. y  Y}"
    then have "b. (pa. b = p  α x (snd pa)  pa  Y)  xa  b"
      by fastforce
    then have "b. b  {p  α x (snd pa) |pa. pa  Y}  xa  b"
      by blast
    then show "xa  {p  α x (snd pa) |pa. pa  Y}"
      by (meson Sup_upper2)
  qed
next
  show "Y  {}  {p  α x (snd y) |y. y  Y}  p  {α x (snd y) |y. y  Y}"
    apply (rule Sup_least)
    apply safe
    by (metis (mono_tags, lifting) Sup_le_iff le_sup_iff mem_Collect_eq sup_ge1 sup_ge2)
qed

lemma sd_distl: "Y  {}  sd_prod x (Sup_prod Y) = Sup_prod {sd_prod x y |y. y  Y}"
proof -
  assume a: "Y  {}"
  have "sd_prod x (Sup_prod Y) = sd_prod x ({fst y |y. y  Y}, {snd y |y. y  Y})"
    by (simp add: Sup_prod_def)
  also have "... = ((fst x)  ({fst y |y. y  Y}), (snd x  (α (fst x) ({snd y |y. y  Y}))))"
    by (simp add: sd_prod_def)
  also have "... = ({fst x  fst y |y. y  Y}, (snd x  (α (fst x) ({snd y |y. y  Y}))))"
    by (simp add: Sup_distl)
  also have "... = ({fst x  fst y |y. y  Y}, (snd x  ({α (fst x) (snd y) |y. y  Y})))"
    by (simp add: act4, meson)
  also have "... = ({fst x  fst y |y. y  Y}, {snd x  (α (fst x) (snd y)) |y. y  Y})"
    using a sd_distl_aux by blast
  also have "... = Sup_prod {(fst x  fst y, snd x  (α (fst x) (snd y))) |y. y  Y}"
    by (simp add: Sup_prod_def, metis)
  finally show ?thesis
    by (simp add: sd_prod_def)
qed
  
definition "sd_unit = (1,)"
 
lemma sd_unitl [simp]: "sd_prod sd_unit x = x"
  by (simp add: sd_prod_def sd_unit_def)    
    
lemma sd_unitr [simp]: "sd_prod x sd_unit = x"
  apply (simp add: sd_prod_def sd_unit_def)
  using act_emp by force
   
text The following counterexamples rule out that semidirect products of quantales and complete lattices form quantales.
The reason is that the right annihilation law fails.
  
lemma "sd_prod x (Sup_prod Y) = Sup_prod {sd_prod x y |y. y  Y}" (*nitpick[show_all,expect=genuine]*)
  oops
  
lemma "sd_prod x bot_prod = bot_prod" (*nitpick[show_all,expect=genuine]*)
  oops
    
text However we can show that semidirect products of (unital) quantales with complete lattices form weak (unital) quantales. 
    
interpretation dp_quantale: weak_quantale sd_prod Inf_prod Sup_prod inf_prod less_eq_prod less_prod sup_prod bot_prod top_prod
  apply standard 
  apply (simp_all add: sd_distl sd_distr)
  apply (simp_all add: sd_prod_def Inf_prod_def Sup_prod_def bot_prod_def sup_prod_def top_prod_def inf_prod_def less_eq_prod_def less_prod_def)
  by (rule conjI, simp add: mult.assoc, simp add: act1 act_sup_distl sup_assoc) 
    
interpretation dpu_quantale: unital_weak_quantale sd_unit sd_prod Inf_prod Sup_prod inf_prod less_eq_prod less_prod sup_prod bot_prod top_prod
  by (standard; simp_all)

end

end