Theory Unary_Modalities

(* Title: Unary Modalities
   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 Unary Modalities

theory Unary_Modalities
  imports Binary_Modalities
begin
  
text Unary modalites arise as specialisations of the binary ones; and as generalisations of the 
standard (multi-)modal operators from predicates to functions into complete lattices. They are interesting, for instance, 
in combination with partial semigroups or monoids, for modelling the Halpern-Shoham modalities in interval logics. 
  
subsection Forward and Backward Diamonds

definition fdia :: "('a × 'b) set  ('b  'c::complete_lattice)  'a  'c" ("( |_ _ _)" [61,81] 82) where
  "( |R f x) = {f y|y. (x,y)  R}" 

definition bdia :: "('a × 'b) set  ('a  'c::complete_lattice)  'b  'c" ("( _| _ _)" [61,81] 82)where
  "(R| f y) = {f x |x. (x,y)  R}"  

definition c1 :: "'a  'b::unital_quantale" where
  "c1 x = 1"
  
text The relationship with binary modalities is as follows.
  
lemma fdia_bmod_comp: "( |R f x) =  (λx y z. (x,y)  R) f c1 x"
  by (simp add: fdia_def bmod_comp_def c1_def)

lemma bdia_bmod_comp: "(R| f x) =  (λy x z. (x,y)  R) f c1 x"
  by (simp add: bdia_def bmod_comp_def c1_def)

lemma bmod_fdia_comp: " R f g x = |{(x,(y,z)) |x y z. R x y z} (λ(x,y). (f x)  (g y)) x"
  by (simp add: fdia_def bmod_comp_def)

lemma bmod_fdia_comp_var: 
  " R f g x = |{(x,(y,z)) |x y z. R x y z} (λ(x,y). (λ(v,w).(v  w)) (f x,g y)) x"
  by (simp add: fdia_def bmod_comp_def)

lemma fdia_im: "( |R f x) = (f ` R `` {x})"
  apply (simp add: fdia_def)
  apply (rule antisym)
  apply (intro Sup_least, clarsimp simp: SUP_upper)
  by (intro SUP_least Sup_upper, force)

lemma fdia_un_rel: "fdia (R  S) = fdia R  fdia S" 
  apply (simp add: fun_eq_iff)
  by (clarsimp simp: fun_eq_iff fdia_im SUP_union Un_Image)

lemma fdia_Un_rel: "( | f x) = {|R f x |R. R  }" 
  apply (simp add: fdia_im)
  apply (rule antisym)
  apply (intro SUP_least, safe)
  apply (rule Sup_upper2, force)
  apply (rule SUP_upper, simp)
  apply (rule Sup_least)
  by (clarsimp simp: Image_mono SUP_subset_mono Sup_upper)

lemma fdia_sup_fun: "fdia R (f  g) = fdia R f  fdia R g" 
  by (simp add: fun_eq_iff fdia_im complete_lattice_class.SUP_sup_distrib)
    
lemma fdia_Sup_fun: "( |R () x) = {|R f x |f. f  } "
  apply (simp add: fdia_im)
  apply (rule antisym) 
  apply (rule SUP_least)+
  apply (rule Sup_upper2, force)
  apply (rule SUP_upper, simp) 
  apply (rule Sup_least, safe)
  apply (rule SUP_least)
  by (simp add: SUP_upper2)

lemma fdia_seq: "fdia (R ; S) f x  = fdia R (fdia S f) x"
  by (simp add: fdia_im relcomp_Image, metis Image_eq_UN SUP_UNION) 

lemma fdia_Id [simp]: "( |Id f x) = f x"
  by (simp add: fdia_def)
    
    
subsection Forward and Backward Boxes
  
definition fbox :: "('a × 'b) set  ('b  'c::complete_lattice)  'a  'c" ("|_] _ _" [61,81] 82) where
  "( |R] f x) = {f y|y. (x,y)  R}" 

definition bbox :: "('a × 'b) set  ('a  'c::complete_lattice)  'b  'c" ("[_| _ _" [61,81] 82)where
  "([R| f y) = {f x |x. (x,y)  R}"  
  
  
subsection Symmetries and Dualities
  
lemma fdia_fbox_demorgan: "( |R (f::'b  'c::complete_boolean_algebra) x) = - |R] (λy. -f y) x"
  apply (simp add: fbox_def fdia_def)
  apply (rule antisym)
   apply (rule Sup_least)
   apply (simp add: Inf_lower compl_le_swap1)
  apply (simp add: uminus_Inf)
  apply (rule SUP_least; intro Sup_upper)
  by auto

lemma fbox_fdia_demorgan: "( |R] (f::'b  'c::complete_boolean_algebra) x) = - |R (λy. -f y) x"  
  apply (simp add: fbox_def fdia_def)
  apply (rule antisym)
   apply (simp add: uminus_Sup)
   apply (rule INF_greatest; rule Inf_lower)
   apply auto[1]
  apply (rule Inf_greatest)
  by (simp add: Sup_upper compl_le_swap2)
    
lemma bdia_bbox_demorgan: "(R| (f::'b  'c::complete_boolean_algebra) x) = - [R| (λy. -f y) x"
  apply (simp add: bbox_def bdia_def)
  apply (rule antisym)
   apply (rule Sup_least)
   apply (simp add: Inf_lower compl_le_swap1)
  apply (simp add: uminus_Inf)
  apply (rule SUP_least; intro Sup_upper)
  by auto
    
lemma bbox_bdia_demorgan: "( [R| (f::'b  'c::complete_boolean_algebra) x) = - R| (λy. -f y) x"  
  apply (simp add: bbox_def bdia_def)
  apply (rule antisym)
   apply (simp add: uminus_Sup)
   apply (rule INF_greatest; rule Inf_lower)
   apply auto[1]
  apply (rule Inf_greatest)
  by (simp add: Sup_upper compl_le_swap2)
 
lemma fdia_bdia_conv: "( |R f x) = converse R| f x"
  by (simp add: fdia_def bdia_def) 

lemma fbox_bbox_conv: "( |R] f x) = [converse R| f x"
  by (simp add: fbox_def bbox_def)
    
lemma fdia_bbox_galois: "(x. ( |R f x)  g x)  (x. f x  [R| g x)"
  apply (standard, simp_all add: fdia_def bbox_def)
   apply safe
   apply (rule Inf_greatest)
   apply (force simp: Sup_le_iff)  
  apply (rule Sup_least)
  by (force simp: le_Inf_iff)  
    
lemma bdia_fbox_galois: "(x. (R| f x)  g x)  (x. f x  |R] g x)"
  apply (standard, simp_all add: bdia_def fbox_def)
   apply safe
   apply (rule Inf_greatest)
   apply (force simp: Sup_le_iff)  
  apply (rule Sup_least)
  by (force simp: le_Inf_iff)  
  
lemma dia_conjugate: 
  "(x. ( |R (f::'b  'c::complete_boolean_algebra) x)  g x = )  (x. f x  (R| g x) = )"
  by (simp add: meet_shunt fdia_bbox_galois bdia_bbox_demorgan)
    
lemma box_conjugate: 
  "(x. ( |R] (f::'b  'c::complete_boolean_algebra) x)  g x = )  (x. f x  ([R| g x) = )"
proof-
  have "(x. ( |R] f x)  g x = )  (x. -g x  |R] f x)"
    by (simp add: join_shunt sup_commute)
  also have "...  (x. -g x  - |R (λy. -f y) x)"
    by (simp add: fbox_fdia_demorgan) 
  also have "...  (x. ( |R (λy. -f y) x)  g x)"      
    by simp
  also have "...  (x. -f x  [R| g x)"
    by (simp add: fdia_bbox_galois)  
  finally show ?thesis
    by (simp add: join_shunt)
qed
  
end