Theory Quantales_Converse.Modal_Quantale

(*
Title: Modal quantales
Author: Georg Struth
Maintainer: Georg Struth <g.struth at sheffield.ac.uk>
*)

section ‹Modal quantales›

theory Modal_Quantale
  imports Quantales.Quantale_Star Modal_Kleene_Algebra_Var KAD.Modal_Kleene_Algebra

begin

subsection ‹Simplified modal semirings and Kleene algebras›

text ‹The previous formalisation of modal Kleene algebra in the AFP adds two compatibility axioms between domain and codomain
when combining an antidomain semiring with an antirange semiring. But these are unnecessary. They are derivable from the other
axioms. Thus I provide a simpler axiomatisation that should eventually replace the one in the AFP.›

class modal_semiring_simp = antidomain_semiring + antirange_semiring

lemma (in modal_semiring_simp) dr_compat [simp]: "d (r x) = r x"
proof-
  have a: "ar x ⋅ d (r x) = 0"
    using local.ads_d_def local.ars_r_def local.dpdz.dom_weakly_local by auto
  have "r x ⋅ d (r x) ⋅ ar x ≤ r x ⋅ ar x"
    by (simp add: local.a_subid_aux2 local.ads_d_def local.mult_isor)
  hence b: "r x ⋅ d (r x) ⋅ ar x = 0"
    by (simp add: local.ardual.am2 local.ars_r_def local.join.bot_unique)
  have "d (r x) = (ar x + r x) ⋅ d (r x)"
    using local.add_comm local.ardual.ans3 local.ars_r_def local.mult_1_left by presburger
  also have "… = ar x ⋅ d (r x) + r x ⋅ d (r x)"
    by simp
  also have "… = r x ⋅ d (r x)"
    by (simp add: a)
  also have "… = r x ⋅ d (r x) ⋅ (ar x + r x)"
    using local.add_comm local.ardual.ans3 local.ars_r_def by auto
  also have "… = r x ⋅ d (r x) ⋅ ar x + r x ⋅ d (r x) ⋅ r x"
    by simp
  also have "… = r x ⋅ d (r x) ⋅ r x"
    using b by auto
  also have "… = r x"
    by (metis local.ads_d_def local.am3 local.ardual.a_mult_idem local.ars_r_def local.ds.ddual.mult_assoc)
  finally show ?thesis
    by simp
qed

lemma (in modal_semiring_simp) rd_compat [simp]: "r (d x) = d x"
  by (smt (verit) local.a_mult_idem local.ads_d_def local.am2 local.ardual.dpdz.dom_weakly_local local.ars_r_def local.dr_compat local.kat_3_equiv')

subclass (in modal_semiring_simp) modal_semiring
  apply unfold_locales by simp_all

class modal_kleene_algebra_simp = modal_semiring_simp + kleene_algebra

subclass (in modal_kleene_algebra_simp) modal_kleene_algebra..


subsection ‹Domain quantales›

class domain_quantale = unital_quantale + domain_op +
  assumes dom_absorb: "x ≤ dom x ⋅ x"
  and dom_local: "dom (x ⋅ dom y) = dom (x ⋅ y)"
  and dom_add: "dom (x ⊔ y) = dom x ⊔ dom y"
  and dom_subid: "dom x ≤ 1"
  and dom_zero [simp]: "dom ⊥ = ⊥"

text ‹The definition is that of a domain semiring. I cannot extend the quantale class with respect to domain semirings
because of different operations are used for addition/sup. The following sublocale statement brings all those properties into scope.›

sublocale domain_quantale ⊆ dqmsr: domain_semiring "(⊔)" "(⋅)" 1 ⊥ dom "(≤)" "(<)"
  by unfold_locales (simp_all add: dom_add dom_local dom_absorb sup.absorb2 dom_subid)

sublocale domain_quantale ⊆ dqmka: domain_kleene_algebra "(⊔)" "(⋅)" 1 ⊥  dom "(≤)" "(<)" qstar..

typedef (overloaded)  'a d_element = "{x :: 'a :: domain_quantale. dom x = x}"
  using dqmsr.dom_one by blast

setup_lifting type_definition_d_element

instantiation d_element :: (domain_quantale) bounded_lattice

begin

lift_definition less_eq_d_element :: "'a d_element ⇒ 'a d_element ⇒ bool" is "(≤)" .

lift_definition less_d_element :: "'a d_element ⇒ 'a d_element ⇒ bool" is "(<)" .

lift_definition bot_d_element :: "'a d_element" is ⊥
  by simp

lift_definition top_d_element :: "'a d_element" is 1
  by simp

lift_definition inf_d_element :: "'a d_element ⇒ 'a d_element ⇒ 'a d_element" is "(⋅)"
  by (metis dqmsr.dom_mult_closed)

lift_definition sup_d_element :: "'a d_element ⇒ 'a d_element ⇒ 'a d_element" is "(⊔)"
  by simp

instance
  apply (standard; transfer)
             apply (simp_all add: less_le_not_le)
     apply (metis dqmsr.dom_subid_aux2'')
    apply (metis dqmsr.dom_subid_aux1'')
   apply (metis dqmsr.dom_glb_eq)
  by (metis dqmsr.dom_subid)

end

instance d_element :: (domain_quantale) distrib_lattice
  by (standard, transfer, metis dqmsr.dom_distrib)

context domain_quantale
begin

lemma dom_top [simp]: "dom ⊤ = 1"
proof-
  have "1 ≤ ⊤"
    by simp
  hence "dom 1 ≤ dom ⊤"
    using local.dqmsr.d_iso by blast
  thus ?thesis
    by (simp add: local.dual_order.antisym)
qed

lemma dom_top2: "x ⋅ ⊤ ≤ dom x ⋅ ⊤"
proof-
  have "x ⋅ ⊤ = dom x ⋅ x ⋅ ⊤"
    by simp
  also have "… ≤ dom x ⋅ ⊤ ⋅ ⊤"
    using local.dqmsr.d_restrict_iff_1 local.top_greatest local.top_times_top mult_assoc by presburger
  finally show ?thesis
    by (simp add: local.mult.semigroup_axioms semigroup.assoc)
qed

lemma weak_twisted: "x ⋅ dom y ≤ dom (x ⋅ y) ⋅ x"
  using local.dqmsr.fd_def local.dqmsr.fdemodalisation2 local.eq_refl by blast

lemma dom_meet: "dom x ⋅ dom y = dom x ⊓ dom y"
  apply (rule order.antisym)
   apply (simp add: local.dqmsr.dom_subid_aux2 local.dqmsr.dom_subid_aux2'')
  by (smt (z3) local.dom_absorb local.dqmsr.dom_iso local.dqmsr.dom_subid_aux2 local.dqmsr.dsg3 local.dqmsr.dsg4 local.dual_order.antisym local.inf.cobounded1 local.inf.cobounded2 local.psrpq.mult_isol_var)

lemma dom_meet_pres: "dom (dom x ⊓ dom y) = dom x ⊓ dom y"
  using dom_meet local.dqmsr.dom_mult_closed by presburger

lemma dom_meet_distl: "dom x ⋅ (y ⊓ z) = (dom x ⋅ y) ⊓ (dom x ⋅ z)"
proof-
  have a: "dom x ⋅ (y ⊓ z) ≤ (dom x ⋅ y) ⊓ (dom x ⋅ z)"
    using local.mult_isol by force
  have "(dom x ⋅ y) ⊓ (dom x ⋅ z) = dom ((dom x ⋅ y) ⊓ (dom x ⋅ z)) ⋅ ((dom x ⋅ y) ⊓ (dom x ⋅ z))"
    by simp
  also have "… ≤ dom ((dom x ⋅ y)) ⋅ ((dom x ⋅ y) ⊓ (dom x ⋅ z))"
    using calculation local.dqmsr.dom_iso local.dqmsr.dom_llp2 local.inf.cobounded1 by presburger
  also have "… ≤ dom x ⋅ ((dom x ⋅ y) ⊓ (dom x ⋅ z))"
    by (metis local.dqmsr.domain_1'' local.dqmsr.domain_invol local.mult_isor)
  also have "… ≤ dom x ⋅ (y ⊓ z)"
    by (meson local.dqmsr.dom_subid_aux2 local.inf_mono local.order_refl local.psrpq.mult_isol_var)
  finally show ?thesis
    using a local.dual_order.antisym by blast
qed

lemma dom_meet_approx: "dom ((dom x ⋅ y) ⊓ (dom x ⋅ z)) ≤ dom x"
  by (metis dom_meet_distl local.dqmsr.domain_1'' local.dqmsr.domain_invol)

lemma dom_inf_pres_aux: "Y ≠ {} ⟹ dom (⨅y ∈ Y. dom x ⋅ y) ≤ dom x"
proof-
  assume "Y ≠ {}"
  have "∀z∈Y. dom (⨅y ∈ Y. dom x ⋅ y) ≤ dom (dom x ⋅ z)"
    by (meson local.INF_lower local.dqmsr.dom_iso)
  hence "∀z∈Y. dom (⨅y ∈ Y. dom x ⋅ y) ≤ dom x ⋅ dom z"
    by fastforce
  hence "∀z∈Y. dom (⨅y ∈ Y. dom x ⋅ y) ≤ dom x"
    using dom_meet by fastforce
  thus "dom (⨅y ∈ Y. dom x ⋅ y) ≤ dom x"
    using ‹Y ≠ {}› by blast
qed

lemma dom_inf_pres_aux2: "(⨅y ∈ Y. dom x ⋅ y) ≤ ⨅Y"
  by (simp add: local.INF_lower2 local.dqmsr.dom_subid_aux2 local.le_Inf_iff)

lemma dom_inf_pres: "Y ≠ {} ⟹ dom x ⋅ (⨅Y) = (⨅y ∈ Y. dom x ⋅ y)"
proof-
  assume hyp: "Y ≠ {}"
  have a: "dom x ⋅ (⨅Y) ≤ (⨅y ∈ Y. dom x ⋅ y)"
    by (simp add: Setcompr_eq_image local.Inf_subdistl)
  have "(⨅y ∈ Y. dom x ⋅ y) = dom (⨅y ∈ Y. dom x ⋅ y) ⋅ (⨅y ∈ Y. dom x ⋅ y)"
    by simp
  also have "… ≤ dom x ⋅ (⨅y ∈ Y. dom x ⋅ y)"
    using dom_inf_pres_aux hyp local.mult_isor by blast
  also have "… ≤ dom x ⋅ ⨅Y"
    by (simp add: dom_inf_pres_aux2 local.psrpq.mult_isol_var)
  finally show ?thesis
    using a order.antisym by blast
qed

lemma "dom (⨅X) ≤ ⨅ (dom ` X)"
  by (simp add: local.INF_greatest local.Inf_lower local.dqmsr.dom_iso)

text ‹The domain operation need not preserve arbitrary sups, though this property holds, for instance,
in quantales of binary relations. I do not aim at a stronger axiomatisation in this theory.›

lemma dom_top_pres: "(x ≤ dom y ⋅ x) = (x ≤ dom y ⋅ ⊤)"
  apply standard
   apply (meson local.dqmsr.ddual.mult_isol_var local.dual_order.eq_iff local.dual_order.trans local.top_greatest)
  using local.dqmsr.dom_iso local.dqmsr.dom_llp by fastforce

lemma dom_lla_var: "(dom x ≤ dom y) = (x ≤ dom y ⋅ ⊤)"
  using dom_top_pres local.dqmsr.dom_llp by force

lemma "dom (1 ⊓ x) = 1 ⊓ x ⟹ x ≤ 1 ⟹ dom x = x"
  using local.inf_absorb2 by force

lemma dom_meet_sub: "dom (x ⊓ y) ≤ dom x ⊓ dom y"
  by (simp add: local.dqmsr.d_iso)

lemma dom_dist1: "dom x ⊔ (dom y ⊓ dom z) = (dom x ⊔ dom y) ⊓ (dom x ⊔ dom z)"
  by (metis dom_meet local.dom_add local.dqmsr.dom_distrib)

lemma dom_dist2: "dom x ⊓ (dom y ⊔ dom z) = (dom x ⊓ dom y) ⊔ (dom x ⊓ dom z)"
  by (metis dom_meet local.dom_add local.sup_distl)

abbreviation "fd' ≡ dqmsr.fd"

definition "bb x y = ⨆{dom z |z. fd' x z ≤ dom y}"

lemma fd'_bb_galois_aux: "fd' x (dom p) ≤ dom q ⟹ dom p ≤ bb x (dom q)"
  by (simp add: bb_def local.SUP_upper setcompr_eq_image)

lemma dom_iso_var: "(⨆x ∈ X. dom x) ≤ dom (⨆x ∈ X. dom x)"
  by (meson local.SUP_le_iff local.dom_subid local.dqmsr.domain_subid)

lemma dom_iso_var2: "(⨆x ∈ X. dom x) ≤ dom (⨆x ∈ X. x)"
  by (simp add: local.SUP_le_iff local.Sup_upper local.dqmsr.dom_iso)

end


subsection ‹Codomain quantales›

class codomain_quantale = unital_quantale + range_op +
  assumes cod_absorb: "x ≤ x ⋅ cod x"
  and cod_local: "cod (cod x ⋅ y) = cod (x ⋅ y)"
  and cod_add: "cod (x ⊔ y) = cod x ⊔ cod y"
  and cod_subid: "cod x ≤ 1"
  and cod_zero: "cod ⊥ = ⊥"

sublocale codomain_quantale ⊆ coddual: domain_quantale range_op _ "λx y. y ⋅ x" _ _ _ _ _ _ _ _
  by unfold_locales (auto simp: mult_assoc cod_subid cod_zero cod_add cod_local cod_absorb Sup_distr Sup_distl)

abbreviation (in codomain_quantale) "bd' ≡ coddual.fd'"

definition (in codomain_quantale) "fb x y = ⨆{cod z |z. bd' x z ≤ cod y}"

lemma (in codomain_quantale) bd'_fb_galois_aux: "bd' x (cod p) ≤ cod q ⟹ cod p ≤ fb x (cod q)"
  using local.coddual.bb_def local.coddual.fd'_bb_galois_aux local.fb_def by auto


subsection ‹Modal quantales›

class dc_modal_quantale = domain_quantale + codomain_quantale +
  assumes dc_compat [simp]: "dom (cod x) = cod x"
  and cd_compat [simp]: "cod (dom x) = dom x"

sublocale dc_modal_quantale ⊆ mqs: dr_modal_kleene_algebra "(⊔)" "(⋅)" 1 ⊥ "(≤)" "(<)" qstar dom cod
  by unfold_locales simp_all

sublocale dc_modal_quantale ⊆ mqdual: dc_modal_quantale _ "λx y. y ⋅ x" _ _ _ _ _ _ _ _  dom cod
  by unfold_locales simp_all

lemma (in dc_modal_quantale) "x ⋅ ⊤ = dom x ⋅ ⊤"
(*  nitpick[expect=genuine] *)
  oops

lemma (in dc_modal_quantale) "⊤ ⋅ x = ⊤ ⋅ cod x"
(*  nitpick[expect=genuine] *)
  oops


subsection ‹Antidomain and anticodomain quantales›

notation antidomain_op ("adom")

class antidomain_quantale = unital_quantale + antidomain_op +
  assumes as1 [simp]: "adom x ⋅ x = ⊥"
  and as2 [simp]: "adom (x ⋅ y) ≤ adom (x ⋅ adom (adom y))"
  and as3 [simp]: "adom (adom x) ⊔ adom x = 1"

definition (in antidomain_quantale) "ddom = adom ∘ adom"

sublocale antidomain_quantale ⊆ adqmsr: antidomain_semiring adom "(⊔)" "(⋅)" 1 ⊥ "(≤)" "(<)"
  by unfold_locales (simp_all add: local.sup.absorb2)

sublocale antidomain_quantale ⊆ adqmka: antidomain_kleene_algebra adom "(⊔)" "(⋅)" 1 ⊥ "(≤)" "(<)" qstar..

sublocale antidomain_quantale ⊆ addq: domain_quantale ddom
  by unfold_locales (simp_all add: ddom_def local.adqmsr.ans_d_def)

notation antirange_op ("acod")

class anticodomain_quantale = unital_quantale + antirange_op +
  assumes ars1 [simp]: "x ⋅ acod x = ⊥"
  and ars2 [simp]: "acod (x ⋅ y) ≤ acod (acod (acod x) ⋅ y)"
  and ars3 [simp]: "acod (acod x) ⊔ acod x = 1"

sublocale anticodomain_quantale ⊆ acoddual: antidomain_quantale acod _ "λx y. y ⋅ x" _ _ _ _ _ _ _ _
  by unfold_locales (auto simp: mult_assoc Sup_distl Sup_distr)

definition (in anticodomain_quantale) "ccod = acod ∘ acod"

sublocale anticodomain_quantale ⊆ acdqmsr: antirange_semiring "(⊔)" "(⋅)" 1 ⊥ acod "(≤)" "(<)"..

sublocale anticodomain_quantale ⊆ acdqmka: antirange_kleene_algebra "(⊔)" "(⋅)" 1 ⊥ "(≤)" "(<)" qstar acod..

sublocale anticodomain_quantale ⊆ acddq: codomain_quantale _ _ _ _ _ _ _ _ _ _ "λ x. acod (acod x)"
  by unfold_locales (simp_all add: local.acoddual.adqmsr.ans_d_def)

class modal_quantale = antidomain_quantale + anticodomain_quantale

sublocale modal_quantale ⊆ mmqs: modal_kleene_algebra_simp "(⊔)" "(⋅)" 1 ⊥ "(≤)" "(<)" qstar adom acod..

sublocale modal_quantale ⊆ mmqdual: modal_quantale _ "λx y. y ⋅ x" _ _ _ _ _ _ _ _ adom acod
  by unfold_locales simp_all

end