# 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"

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"

lemma fdia_im: "( |R⟩ f x) = ⨆(f ` R `` {x})"
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"
by (clarsimp simp: fun_eq_iff fdia_im SUP_union Un_Image)

lemma fdia_Un_rel: "( |⋃ℛ⟩ f x) = ⨆{|R⟩ f x |R. R ∈ ℛ}"
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 (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)

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"

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 (rule antisym)
apply (rule Sup_least)
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 (rule antisym)
apply (rule INF_greatest; rule Inf_lower)
apply auto[1]
apply (rule Inf_greatest)

lemma bdia_bbox_demorgan: "(⟨R| (f::'b ⇒ 'c::complete_boolean_algebra) x) = - [R| (λy. -f y) x"
apply (rule antisym)
apply (rule Sup_least)
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 (rule antisym)
apply (rule INF_greatest; rule Inf_lower)
apply auto[1]
apply (rule Inf_greatest)

lemma fdia_bdia_conv: "( |R⟩ f x) = ⟨converse R| f x"

lemma fbox_bbox_conv: "( |R] f x) = [converse R| f x"

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)"
also have "... ⟷ (∀x. -g x ≤ - |R⟩ (λy. -f y) x)"
also have "... ⟷ (∀x. ( |R⟩ (λy. -f y) x) ≤ g x)"
by simp
also have "... ⟷ (∀x. -f x ≤ [R| g x)"