Theory Omega_Quantale

(* 
Title: Omega-Quantales
Author: Georg Struth
Maintainer: Georg Struth <g.struth at sheffield.ac.uk>
*)

section ‹$\omega$-Quantales›

theory Omega_Quantale
  imports Quantales_Converse.Modal_Quantale Omega_Kleene_Algebra

begin

class iquantale = complete_lattice + imonoid_mult +
  assumes Sup_distl: "x ⋅⇘i⇙ ⨆Y = (⨆y ∈ Y. x ⋅⇘i⇙ y)" 
  assumes Sup_distr: "⨆X ⋅⇘i⇙ y = (⨆x ∈ X. x ⋅⇘i⇙ y)"

sublocale iquantale ⊆ qiq: unital_quantale "un i" "λx y. x ⋅⇘i⇙ y" _ _ _ _ _ _ _ _ 
  apply unfold_locales using local.Sup_distr local.Sup_distl by auto

definition (in iquantale) "istar = qiq.qstar"

lemma (in iquantale) istar_unfold: "istar i x = (⨆k. mm.power i x k)"
  unfolding local.qiq.qstar_def local.istar_def by simp

sublocale iquantale ⊆ dqisi: idioid "(⊔)" "(≤)" "(<)" "⊥" icomp un
  by unfold_locales (simp_all add: local.qiq.sup_distl)

sublocale iquantale ⊆ dqikai: ikleene_algebra "(⊔)" "(≤)" "(<)" "⊥" icomp un istar
  by unfold_locales (simp_all add: local.istar_def local.qiq.uwqlka.star_inductl local.qiq.uqka.star_inductr')

class idomain_quantale = iquantale + idom_op +
  assumes do_absorb: "x ≤ do i x ⋅⇘i⇙ x"
  and do_local [simp]: "do i (x ⋅⇘i⇙ do i y) = do i (x ⋅⇘i⇙ y)"
  and do_add: "do i (x ⊔ y) = do i x ⊔ do i y"
  and do_subid: "do i x ≤ un i"
  and do_zero [simp]: "do i ⊥ = ⊥"

sublocale idomain_quantale ⊆ dqidq: domain_quantale "do i" "un i" "λx y. x ⋅⇘i⇙ y" _ _ _ _ _ _ _ _
  by (unfold_locales, simp_all add: local.do_absorb local.do_add local.do_subid)

sublocale idomain_quantale ⊆ dqidsi: idomain_semiring "(⊔)" "(≤)" "(<)" "⊥"  icomp un do
  by (unfold_locales, simp_all add: local.do_add local.do_subid)

class icodomain_quantale = iquantale + icod_op +
  assumes cd_absorb: "x ≤ x ⋅⇘i⇙ cd i x" 
  and cd_local [simp]: "cd i (cd i x ⋅⇘i⇙ y) = cd i (x ⋅⇘i⇙ y)"
  and cd_add: "cd i (x ⊔ y) = cd i x ⊔ cd i y"
  and cd_subid: "cd i x ≤ un i"
  and cd_zero [simp]: "cd i ⊥ = ⊥"

sublocale icodomain_quantale ⊆ cdqicdq: codomain_quantale "un i" "λx y. x ⋅⇘i⇙ y" _ _ _ _ _ _ _ _ "cd i"
  by (unfold_locales, simp_all add: local.cd_absorb local.cd_add local.cd_subid)

sublocale icodomain_quantale ⊆ cdqidcsi: icodomain_semiring cd "(⊔)"  "(≤)" "(<)" "⊥" icomp un
  by (unfold_locales, simp_all add: local.cd_absorb local.cd_add local.cd_subid)

class imodal_quantale = idomain_quantale + icodomain_quantale +
  assumes dc_compat [simp]: "do i (cd i x) = cd i x" 
  and cd_compat [simp]: "cd i (do i x) = do i x" 

sublocale imodal_quantale ⊆ mqimq: dc_modal_quantale "un i" "λx y. x ⋅⇘i⇙ y" _ _ _ _ _ _ _ _  "cd i" "do i"
  by unfold_locales simp_all

sublocale imodal_quantale ⊆ mqimka: imodal_kleene_algebra "(⊔)" "(≤)" "(<)" "⊥" icomp un istar cd do
  by unfold_locales simp_all

sublocale imodal_quantale ⊆ mqidual: imodal_quantale do _ _ _ _ _ _ _ _ "λx i y. y ⋅⇘i⇙ x" _ cd
  by unfold_locales (simp_all add: local.cdqicdq.coddual.Sup_distl local.Sup_distl)

class omega_quantale = imodal_quantale +
  assumes interchange: "i < j ⟹ (w ⋅⇘j⇙ x) ⋅⇘i⇙ (y ⋅⇘j⇙ z) ≤ (w ⋅⇘i⇙ y) ⋅⇘j⇙ (x ⋅⇘i⇙ z)"
  and dj_hom: "i ≠ j ⟹ do j (x ⋅⇘i⇙ y) ≤ do j x ⋅⇘i⇙ do j y"
  and cj_hom: "i ≠ j ⟹ cd j (x ⋅⇘i⇙ y) ≤ cd j x ⋅⇘i⇙ cd j y"
  and djdi: "i < j ⟹ do j (do i x) = do i x"

class strong_omega_quantale = omega_quantale +
  assumes dj_strong_hom: "i < j ⟹ do j (x ⋅⇘i⇙ y) = do j x ⋅⇘i⇙ do j y"
  and cj_strong_hom: "i < j ⟹ cd j (x ⋅⇘i⇙ y) = cd j x ⋅⇘i⇙ cd j y"

sublocale omega_quantale ⊆ tgqs: omega_semiring cd "(⊔)" "(≤)" "(<)" "⊥" icomp un do
  by unfold_locales (simp_all add: local.interchange local.dj_hom local.cj_hom local.djdi)

sublocale strong_omega_quantale ⊆ stgqs: strong_omega_semiring cd "(⊔)" "(≤)" "(<)" "⊥" icomp un do
  by unfold_locales (simp_all add: local.dj_strong_hom local.cj_strong_hom) 

sublocale omega_quantale ⊆ tgqs: omega_kleene_algebra "(⊔)" "(≤)" "(<)" "⊥"  icomp un istar cd do ..

sublocale strong_omega_quantale ⊆ tgqs: strong_omega_kleene_algebra "(⊔)" "(≤)" "(<)" "⊥" icomp un  istar cd do  ..

context omega_quantale
begin

lemma istar_aux: "i < j ⟹ mm.power i (x ⋅⇘j⇙ y) k ≤ mm.power i x k ⋅⇘j⇙ mm.power i y k"
proof (induct k)
  case 0
  then show ?case
    by (simp add: tgqs.uni_compj_eq)
next
  case (Suc k)
  fix k 
  assume "i < j"
  assume h: "i < j ⟹ mm.power i (x ⋅⇘j⇙ y) k ≤ mm.power i x k ⋅⇘j⇙ mm.power i y k"
  have "mm.power i (x ⋅⇘j⇙ y) (Suc k) = (x ⋅⇘j⇙ y) ⋅⇘i⇙ mm.power i (x ⋅⇘j⇙ y) k"
    by simp
  also have "… ≤ (x ⋅⇘j⇙ y) ⋅⇘i⇙ (mm.power i x k ⋅⇘j⇙ mm.power i y k)"
    by (simp add: Suc.prems h local.qiq.psrpq.mult_isol)
  also have "… ≤ (x ⋅⇘i⇙ mm.power i x k) ⋅⇘j⇙ (y ⋅⇘i⇙ mm.power i y k)"
    by (simp add: Suc.prems local.tgqs.tgsdual.interchange)
  also have "… = mm.power i x (Suc k) ⋅⇘j⇙ mm.power i y (Suc k)"
    by simp
  finally show "mm.power i (x ⋅⇘j⇙ y) (Suc k) ≤ mm.power i x (Suc k) ⋅⇘j⇙ mm.power i y (Suc k)".
qed

lemma istar_oplax: "i < j ⟹ istar i (x ⋅⇘j⇙ y) ≤ istar i x ⋅⇘j⇙ istar i y"
  by (simp add: local.tgqs.star_compj)

lemma istar_distli: "i < j ⟹ x ⋅⇘i⇙ (istar j y) = (⨆k. x ⋅⇘i⇙ (mm.power j y k))"
  by (simp add: image_image local.qiq.Sup_distl local.istar_unfold)

lemma istar_distri: "i < j ⟹ (istar j x) ⋅⇘i⇙ y = (⨆k. mm.power j x k ⋅⇘i⇙ y)"
  by (simp add: image_image local.qiq.Sup_distr local.istar_unfold)

lemma istar_distlj: "i < j ⟹ x ⋅⇘j⇙ (istar i y) = (⨆k. x ⋅⇘j⇙ (mm.power i y k))"
  by (simp add: image_image local.Sup_distl local.istar_unfold)

lemma istar_distrj: "i < j ⟹ (istar i x) ⋅⇘j⇙ y = (⨆k. mm.power i x k ⋅⇘j⇙ y)"
  by (simp add: image_image local.qiq.Sup_distr local.istar_unfold)

lemma istar_laxl_aux_var: "i < j ⟹ do i x ⋅⇘i⇙ mm.power j y k ≤ mm.power j (do i x ⋅⇘i⇙ y) k"
proof (induct k)
  case 0
  assume "i < j"
  have "do i x ⋅⇘i⇙ un j = do j (do i x) ⋅⇘i⇙ un j"
    by (simp add: "0" local.djdi)
  also have "… ≤ un j ⋅⇘i⇙ un j"
    by (simp add: local.qiq.nsrnq.mult_isor)
  finally have "do i x ⋅⇘i⇙ un j ≤ un j"
    by (simp add: local.dqidq.dqmsr.dom_subid_aux2)
  thus "do i x ⋅⇘i⇙ mm.power j y 0 ≤ mm.power j (do i x ⋅⇘i⇙ y) 0"
    by simp
next
  case (Suc k)
  fix k
  assume "i < j"
  assume h: "i < j ⟹ do i x ⋅⇘i⇙ mm.power j y k ≤ mm.power j (do i x ⋅⇘i⇙ y) k"
  have "do i x ⋅⇘i⇙ mm.power j y (Suc k) = do i x ⋅⇘i⇙ (y ⋅⇘j⇙  mm.power j y k)"
    by simp
  also have "… = (do i x ⋅⇘j⇙ do i x) ⋅⇘i⇙ (y ⋅⇘j⇙ mm.power j y k)"
    using Suc.prems less_imp_add_positive by fastforce
  also have "…  ≤ (do i x ⋅⇘i⇙ y) ⋅⇘j⇙ (do i x ⋅⇘i⇙ mm.power j y k)"
    by (simp add: Suc.prems local.interchange)
  also have "…  ≤ (do i x ⋅⇘i⇙ y) ⋅⇘j⇙ mm.power j (do i x ⋅⇘i⇙ y) k"
    by (simp add: Suc.prems h local.qiq.psrpq.mult_isol)
  finally show "do i x ⋅⇘i⇙ mm.power j y (Suc k) ≤ mm.power j (do i x ⋅⇘i⇙ y) (Suc k)"
    by simp
qed

lemma istar_laxl_var: 
  assumes "i < j"
  shows "do i x ⋅⇘i⇙ istar j y ≤ istar j (do i x ⋅⇘i⇙ y)"  
proof-
  have "do i x ⋅⇘i⇙ istar j y = (⨆k. do i x ⋅⇘i⇙ mm.power j y k)"
    by (simp add: image_image local.Sup_distl local.istar_unfold)
  also have "… ≤ (⨆k. mm.power j (do i x ⋅⇘i⇙ y) k)"
    by (simp add: assms local.SUP_mono' local.istar_laxl_aux_var)
  finally show ?thesis
    using local.istar_unfold by auto
qed

lemma istar_laxl_var2: "do i x ⋅⇘i⇙ istar (i + k + 1) y ≤ istar (i + k + 1) (do i x ⋅⇘i⇙ y)"
  using istar_laxl_var by force  

lemma istar_laxr_aux_var: "i < j ⟹ mm.power j x k ⋅⇘i⇙ cd i y ≤ mm.power j (x ⋅⇘i⇙ cd i y) k"
proof (induct k)
  case 0 show ?case
    by (simp add: local.cdqicdq.coddual.dqmsr.dom_subid_aux2)
next
  case (Suc k)
  assume h0: "i < j"
  fix k
  assume h: "i < j ⟹ mm.power j x k ⋅⇘i⇙ cd i y ≤ mm.power j (x ⋅⇘i⇙ cd i y) k"
  have "mm.power j x (Suc k) ⋅⇘i⇙ cd i y = (x ⋅⇘j⇙ mm.power j x k) ⋅⇘i⇙ (cd i y ⋅⇘j⇙ cd i y)"
    using h0 less_imp_add_positive by fastforce
  also have "…  ≤ (x ⋅⇘i⇙ cd i y) ⋅⇘j⇙ (mm.power j x k ⋅⇘i⇙ cd i y)"
    by (simp add: h0 local.tgqs.tgsdual.interchange)
  finally show "mm.power j x (Suc k) ⋅⇘i⇙ cd i y ≤ mm.power j (x ⋅⇘i⇙ cd i y) (Suc k)"
    by (simp add: h h0 local.qiq.h_w2 local.qiq.psrpq.mult_isol)
qed
 
lemma istar_laxr_var: 
  assumes "i < j"
  shows "istar j x ⋅⇘i⇙ cd i y ≤ istar j (x ⋅⇘i⇙ cd i y)"
proof-
  have "istar j x ⋅⇘i⇙ cd i y = (⨆k. mm.power j x k ⋅⇘i⇙ cd i y)"
    using assms istar_distri by presburger
  also have "… ≤ (⨆k. mm.power j (x ⋅⇘i⇙ cd i y) k)"
    by (simp add: assms local.SUP_mono' local.istar_laxr_aux_var)
  finally show ?thesis
    by (simp add: local.istar_unfold)
qed

lemma istar_laxr_var2: "istar (i + k + 1) x ⋅⇘i⇙ cd i y ≤ istar (i + k + 1) (x ⋅⇘i⇙ cd i y)"
  using istar_laxr_var by force

lemma istar_prop:
  assumes "i < j"
  shows "istar j x ⋅⇘i⇙ istar j y = (⨆k l. mm.power j x k ⋅⇘i⇙ mm.power j y l)"
proof-
  have "istar j x ⋅⇘i⇙ istar j y = istar j x ⋅⇘i⇙ ( ⨆k. mm.power j y k)"
    using local.istar_unfold by auto
  also have "… = (⨆l. istar j x ⋅⇘i⇙ mm.power j y l)"
    by (simp add: image_image local.Sup_distl)
  also have "… = (⨆l. (⨆k. mm.power j x k) ⋅⇘i⇙ mm.power j y l)"
    unfolding istar_def qiq.qstar_def by (simp add: full_SetCompr_eq)
  also have "… = (⨆l. (⨆k. mm.power j x k ⋅⇘i⇙ mm.power j y l))"
    using assms istar_distri local.istar_unfold by auto
  also have "… = (⨆k l. mm.power j x k ⋅⇘i⇙ mm.power j y l)"
    using local.SUP_commute by force
  finally show ?thesis.
qed

end

context strong_omega_quantale
begin

lemma istar_laxl_aux: "i < j ⟹ do j x ⋅⇘i⇙ mm.power j y k ≤ mm.power j (do j x ⋅⇘i⇙ y) k"
proof (induct k)
  case 0
  assume "i < j"
  have "do i x ⋅⇘i⇙ un j ≤ un j ⋅⇘i⇙ un j"
    using "0" local.dqidq.dqmsr.dom_subid_aux2 local.stgqs.stgsdual.idj_compi_eq by force
  thus "do j x ⋅⇘i⇙ mm.power j y 0 ≤ mm.power j (do j x ⋅⇘i⇙ y) 0"
    by (metis "0" local.do_subid local.mm.power.power_0 local.qiq.nsrnq.mult_isor local.stgqs.stgsdual.idj_compi_eq)
next
  case (Suc k)
  assume "i < j"
  fix k
  assume h: "i < j ⟹ do j x ⋅⇘i⇙ mm.power j y k ≤ mm.power j (do j x ⋅⇘i⇙ y) k"
  have "do j x ⋅⇘i⇙ mm.power j y (Suc k) = do j x ⋅⇘i⇙ (y ⋅⇘j⇙  mm.power j y k)"
    by simp
  also have "… = (do j x ⋅⇘j⇙ do j x) ⋅⇘i⇙ (y ⋅⇘j⇙ mm.power j y k)"
    by simp
  also have "…  ≤ (do j x ⋅⇘i⇙ y) ⋅⇘j⇙ (do j x ⋅⇘i⇙ mm.power j y k)"
    using Suc.prems local.interchange by blast
  also have "…  ≤ (do j x ⋅⇘i⇙ y) ⋅⇘j⇙ mm.power j (do j x ⋅⇘i⇙ y) k"
    by (simp add: Suc.prems h local.qiq.psrpq.mult_isol)
  finally show "do j x ⋅⇘i⇙ mm.power j y (Suc k) ≤ mm.power j (do j x ⋅⇘i⇙ y) (Suc k)"
    by simp
qed

lemma istar_laxl: 
  assumes "i < j"
  shows "do j x ⋅⇘i⇙ istar j y ≤ istar j (do j x ⋅⇘i⇙ y)" 
proof-
  have "do j x ⋅⇘i⇙ istar j y = (⨆k. do j x ⋅⇘i⇙ mm.power j y k)"
    using assms local.istar_distli by force
  also have "… ≤ (⨆k. mm.power j (do j x ⋅⇘i⇙ y) k)"
    by (simp add: assms istar_laxl_aux local.SUP_mono')
  finally show ?thesis
    by (simp add: local.istar_unfold)
qed

lemma istar_laxr_aux: "i < j ⟹ mm.power j x k ⋅⇘i⇙ cd j y ≤ mm.power j (x ⋅⇘i⇙ cd j y) k"
proof (induct k)
  case 0 thus ?case
    by (metis local.cd_subid local.mm.power.power_0 local.qiq.psrpq.mult_isol local.stgqs.stgsdual.idj_compi_eq)
next
  case (Suc k)
  assume "i < j"
  fix k
  assume h: "i < j ⟹ mm.power j x k ⋅⇘i⇙ cd j y ≤ mm.power j (x ⋅⇘i⇙ cd j y) k"
  have "mm.power j x (Suc k) ⋅⇘i⇙ cd j y = (x ⋅⇘j⇙  mm.power j x k) ⋅⇘i⇙ cd j y"
    by simp
  also have "… = (x ⋅⇘j⇙ mm.power j x k) ⋅⇘i⇙ (cd j y ⋅⇘j⇙ cd j y)"
    by simp
  also have "…  ≤ (x ⋅⇘i⇙ cd j y) ⋅⇘j⇙ (mm.power j x k ⋅⇘i⇙ cd j y)"
    using Suc.prems local.interchange by blast
  also have "…  ≤  (x ⋅⇘i⇙ cd j y) ⋅⇘j⇙ mm.power j (x  ⋅⇘i⇙ cd j y) k"
    by (simp add: Suc.prems h local.qiq.psrpq.mult_isol)
  finally show "mm.power j x (Suc k) ⋅⇘i⇙ cd j y ≤ mm.power j (x ⋅⇘i⇙ cd j y) (Suc k)"
    by simp
qed

lemma iqstar_laxr: 
  assumes "i < j"
  shows "istar j x ⋅⇘i⇙ cd j y ≤ istar j (x ⋅⇘i⇙ cd j y)"  
proof-
  have "istar j x ⋅⇘i⇙ cd j y = (⨆k. mm.power j x k ⋅⇘i⇙ cd j y)"
    using assms local.istar_distri by force
  also have "… ≤ (⨆k. mm.power j (x ⋅⇘i⇙ cd j y) k)"
    by (simp add: assms istar_laxr_aux local.SUP_mono')
  finally show ?thesis
    by (simp add: local.istar_unfold)
qed

lemma qstar1_aux: "i < j ⟹ mm.power j x k ⋅⇘i⇙ mm.power j y k ≤ mm.power j (x ⋅⇘i⇙ y) k"
proof (induct k)
  case 0
  then show ?case
    using local.stgqs.stgsdual.idj_compi_eq by force
next
  case (Suc k)
  assume "i < j"
 fix k
  assume h: "i < j ⟹ mm.power j x k ⋅⇘i⇙ mm.power j y k ≤ mm.power j (x ⋅⇘i⇙ y) k" 
  have "mm.power j x (Suc k) ⋅⇘i⇙ mm.power j y (Suc k) = (x ⋅⇘j⇙ mm.power j x k) ⋅⇘i⇙ (y ⋅⇘j⇙ mm.power j y k)"
    by simp
  also have "… ≤ (x ⋅⇘i⇙ y) ⋅⇘j⇙ (mm.power j x k ⋅⇘i⇙ mm.power j y k)"
    using Suc.prems local.interchange by force
  also have "… ≤ (x ⋅⇘i⇙ y) ⋅⇘j⇙ mm.power j (x ⋅⇘i⇙ y) k"
    by (simp add: Suc.prems h local.qiq.psrpq.mult_isol)
  also have "… = mm.power j (x ⋅⇘i⇙ y) (Suc k)"
    by simp
  finally show "mm.power j x (Suc k) ⋅⇘i⇙ mm.power j y (Suc k) ≤ mm.power j (x ⋅⇘i⇙ y) (Suc k)".
qed

end

end