Theory Quantale_Modules

(* Title: Quantale Modules and Semidirect Products 
   Author: Georg Struth
   Maintainer: Georg Struth <g.struth@sheffield.ac.uk> 
*)

section ‹Quantale Modules and Semidirect Products›

theory Quantale_Modules
  imports Quantale_Star

begin

subsection ‹Quantale Modules›
  
text ‹Quantale modules are extensions of semigroup actions in that a quantale acts on a complete lattice.
These have been investigated by Abramsky and Vickers~cite"AbramskyV93" and others, predominantly in the context
of pointfree topology.›
  
locale unital_quantale_module = 
  fixes act :: "'a::unital_quantale  'b::complete_lattice_with_dual  'b" ("α")
  assumes act1: "α (x  y) p = α x (α y p)"
    and act2 [simp]: "α 1 p = p" 
    and act3: "α (X) p = (x  X. α x p)"
    and act4: "α x (P) = (p  P. α x 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 [simp]: "α 1 = id"
  by (simp add: fun_eq_iff)
  
lemma emp_act [simp]: "α ({}) p = "
  by (simp only: act3, force)
    
lemma emp_act_var [simp]: "α  p = "
  using emp_act by auto

lemma act_emp [simp]: "α x ({}) = "
  by (simp only: act4, force)
    
lemma act_emp_var [simp]: "α x  = "
  using act_emp by auto
  
lemma act_sup_distl: "α x (p  q) = (α x p)  (α x q)"
  by (metis (mono_tags, lifting) act4 image_insert image_is_empty sup_Sup)
  
lemma act_sup_distr: "α (x  y) p = (α x p)  (α y p)"
  by (metis (no_types, lifting) SUP_insert Sup_empty Sup_insert act3 sup_bot_right)
  
lemma act_sup_distr_var: "α (x  y) = (α x)  (α y)"
  by (simp add: fun_eq_iff act_sup_distr)

subsection ‹Semidirect Products and Weak Quantales›
    
text ‹Next, the semidirect product of a  unital quantale and a complete lattice is defined. ›
  
definition "sd_prod x y = (fst x  fst y, snd x  α (fst x) (snd y))"
   
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 ((x  X. fst x), (x  X. snd x)) y"
    by (simp add: Sup_prod_def)
  also have "... = ((x  X. fst x)  fst y, (x  X. snd x)  (α (x  X. fst x) (snd y)))"
    by (simp add: sd_prod_def)
  also have "... = ((x  X. (fst x  fst y)), (x  X. snd x)  (α (x  X. fst x) (snd y)))"
    by (simp add: Sup_distr image_comp)
  also have "... = ((x  X. (fst x  fst y)), (x  X. snd x)  (x  X. (α (fst x) (snd y))))"
    by (simp add: act3 image_comp)
  also have "... = ((x  X. (fst x  fst y)), (x  X. (snd x  (α (fst x) (snd y)))))"
    using complete_lattice_class.SUP_sup_distrib by fastforce
  also have "... = Sup_prod {(fst x  fst y, snd x  (α (fst x) (snd y))) |x. x  X}"
    apply (unfold Sup_prod_def, safe)
    by ( simp add: SUP_Sup_eq, rule_tac f=Sup in arg_cong, force)+
  finally show ?thesis
    by (simp add: sd_prod_def)
qed
  
lemma sd_distl_aux: "Y  {}  p  (y  Y. α x (snd y)) = (y  Y. p  α x (snd y))"
  apply (rule antisym)
   apply (rule sup_least, metis SUP_bot_conv(2) SUP_const SUP_upper2 sup_ge1)
   apply (rule Sup_least, force simp: SUP_upper2 image_iff)
  by (rule Sup_least, safe, metis Sup_upper image_iff sup.idem sup.mono sup_ge2)

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 ((y  Y. fst y), (y  Y. snd y))"
    by (simp add: Sup_prod_def)
  also have "... = ((fst x)  (y  Y. fst y), (snd x  (α (fst x) (y  Y. snd y))))"
    by (simp add: sd_prod_def)
  also have "... = ((y  Y. fst x  fst y), (snd x  (α (fst x) (y  Y. snd y))))"
    by (simp add: Sup_distl image_comp)
  also have "... = ((y  Y. fst x  fst y), (snd x  (y  Y. α (fst x) (snd y))))"
    by (simp add: act4 image_comp)
  also have "... = ((y  Y. fst x  fst y), (y  Y. snd x  (α (fst x) (snd 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}"
    apply (unfold Sup_prod_def, safe)
    by ( simp add: SUP_Sup_eq, rule_tac f=Sup in arg_cong, force)+
  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"
  by (simp add: sd_prod_def sd_unit_def)

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 one can show that semidirect products of (unital) quantales with complete lattices form weak (unital) quantales. 
This provides an example of how weak quantales arise quite naturally.›
    
sublocale dp_quantale: weak_quantale sd_prod Inf_prod Sup_prod inf_prod less_eq_prod less_prod sup_prod bot_prod top_prod
  apply unfold_locales
    apply (simp add: act1 act_sup_distl mult.assoc sd_prod_def sup_assoc)
   apply (metis Setcompr_eq_image sd_distr)
  by (metis Setcompr_eq_image sd_distl) 

sublocale 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 unfold_locales simp_all

subsection ‹The Star in Semidirect Products›

text ‹I define the star operation for a semidirect product of a quantale and a complete lattice, 
and prove a characteristic property.›

abbreviation "sd_power  dpu_quantale.power"

abbreviation "sd_star  dpu_quantale.qstar"    

lemma sd_power_zero [simp]: "sd_power x 0 = (1,)"
  using sd_unit_def by simp

lemma sd_power_prop_aux: "α (x ^ 0) y  ({α (x ^ k) y |k.  0 < k  k  Suc i}) = {α (x ^ k) y |k. k  Suc i}"
  apply (rule antisym)
  apply (rule sup_least, intro Sup_upper, blast, intro Sup_mono, blast)
  apply (rule Sup_least, safe)
  by (metis (mono_tags, lifting) Sup_insert Sup_upper insert_iff le_0_eq linorder_not_le mem_Collect_eq)

lemma sd_power_prop1 [simp]: "sd_power (x,y) (Suc i) = (x ^ (Suc i), {α (x ^ k) y|k. k  i})"
proof (induct i)
  case 0 thus ?case 
    by auto
next
  case (Suc i) thus ?case
  proof-
    assume "sd_power (x,y) (Suc i) = (x ^ Suc i, {α (x ^ k) y |k. k  i})"
    hence "sd_power (x,y) (Suc (Suc i)) = (x ^ Suc (Suc i), α (x ^ 0) y  ({α (x ^ (Suc k)) y |k. k  i}))"
      apply (simp add: sd_prod_def act1 act4)
      apply safe
      by (metis act4 image_Collect image_image)
    also have "... = (x ^ Suc (Suc i), α (x ^ 0) y  ({α (x ^ k) y |k.  0 < k  k  Suc i}))"
      by (metis (no_types, opaque_lifting) Suc_le_eq Suc_le_mono le_0_eq not0_implies_Suc zero_less_Suc)
    finally show ?thesis 
      using sd_power_prop_aux by simp
  qed
qed

lemma sd_power_prop2 [simp]: "sd_power (x,y) i = (x ^ i, {α (x ^ k) y|k. k < i})"
  apply (case_tac i)
  using sd_unit_def apply force
  using le_simps(2) unital_quantale_module.sd_power_prop1 unital_quantale_module_axioms by fastforce

lemma sdstar_prop: "sd_star (x,y) = (qstar x, α (qstar x) y)"
proof -
  have "sd_star (x,y) = sup_prod (1,) (Sup_prod {sd_power (x,y) (Suc i) |i. True})"
    by (metis dpu_quantale.Sup_iter_unfold dpu_quantale.qstar_def full_SetCompr_eq sd_power_zero)
  also have "... = sup_prod (1,) (Sup_prod {(x^(Suc i), {α (x ^ k) y|k. k  i}) |i. True})"
    using sd_power_prop1 by auto 
  also have "... = (1 ( i. x ^ (Suc i)), (i. {α (x ^ k) y|k. k  i}))"
    apply (unfold sup_prod_def Sup_prod_def, safe)
     apply (simp, rule_tac f="λx. 1  x" in arg_cong)
    by (simp add: SUP_Sup_eq, rule_tac f=Sup in arg_cong, force)+
  also have "... = (qstar x, (i. {α (x ^ k) y|k. k  i}))"
    by (safe, metis (no_types) fSup_unfold power_0 qstar_def)
  also have "... = (qstar x, (i. α (x ^ i) y))" 
    apply safe
    apply (rule antisym)
     apply (safe intro!: Sup_least, simp add: Sup_upper)
    by (metis (mono_tags, lifting) SUP_upper2 Sup_upper mem_Collect_eq order_refl)
  finally show ?thesis
    by (simp add: qstar_def act3 image_comp)
qed

end

end