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