Theory Quantale_Converse

(*
Title: Quantales with converse
Author: Cameron Calk, Georg Struth
Maintainer: Georg Struth <g.struth at sheffield.ac.uk>
*)

section ‹Quantales with converse›

theory Quantale_Converse
  imports Modal_Quantale Modal_Kleene_Algebra_Converse

begin

subsection ‹Properties of unital quantales›

text ‹These properties should eventually added to the quantales AFP entry.›

lemma (in quantale) bres_bot_top [simp]: "⊥ → ⊤ = ⊤"
  by (simp add: local.bres_galois_imp local.order.antisym)

lemma (in quantale) fres_top_bot [simp]: "⊤ ← ⊥ = ⊤"
  by (meson local.fres_galois local.order_antisym local.top_greatest)

lemma (in unital_quantale) bres_top_top2 [simp]: "(x → y ⋅ ⊤) ⋅ ⊤ = x → y ⋅ ⊤"
proof-
  have "(x → y ⋅ ⊤) ⋅ ⊤ ≤ x → y ⋅ ⊤ ⋅ ⊤"
    by (simp add: local.bres_interchange)
  hence "(x → y ⋅ ⊤) ⋅ ⊤ ≤ x → y ⋅ ⊤"
    by (simp add: mult_assoc)
  thus ?thesis
    by (metis local.mult_1_right local.order_eq_iff local.psrpq.subdistl local.sup_top_right)
qed

lemma (in unital_quantale) fres_top_top2 [simp]: "⊤ ⋅ (⊤ ⋅ y ← x) =  ⊤ ⋅ y ← x"
  by (metis local.dual_order.antisym local.fres_interchange local.le_top local.top_greatest mult_assoc)

lemma (in unital_quantale) bres_top_bot [simp]: "⊤ → ⊥ = ⊥"
  by (metis local.bot_least local.bres_canc1 local.le_top local.order.antisym)

lemma (in unital_quantale) fres_bot_top [simp]: "⊥ ← ⊤ = ⊥"
  by (metis local.bot_unique local.fres_canc1 local.top_le local.uqka.independence2 local.uwqlka.star_ext)

lemma (in unital_quantale) top_bot_iff: "(x ⋅ ⊤ = ⊥) = (x = ⊥)"
  by (metis local.fres_bot_top local.fres_canc2 local.le_bot local.mult_botl)


subsection ‹Involutive quantales›

text ‹The following axioms for involutive quantales are standard.›

class involutive_quantale = unital_quantale + invol_op +
  assumes inv_invol [simp]: "(x∘)∘ = x"
  and inv_contrav: "(x ⋅ y)∘ = y∘ ⋅ x∘"
  and inv_sup [simp]: "(⨆X)∘ = (⨆x ∈ X. x∘)"

context involutive_quantale
begin

lemma inv_binsup [simp]: "(x ⊔ y)∘ = x∘ ⊔ y∘"
proof-
  have "(x ⊔ y)∘ = (⨆z ∈ {x,y}. z∘)"
    using local.inv_sup local.sup_Sup by presburger
  also have "… = (⨆z ∈ {x∘,y∘}. z)"
    by simp
  also have "… = x∘ ⊔ y∘"
    by fastforce
  finally show ?thesis.
qed

lemma inv_iso: "x ≤ y ⟹ x∘ ≤ y∘"
  by (metis inv_binsup local.sup.absorb_iff1)

lemma inv_galois: "(x∘ ≤ y) = (x ≤ y∘)"
  using local.inv_iso by fastforce

lemma bres_fres_conv: "(y∘ ← x∘)∘ = x → y"
proof-
  have "(y∘ ← x∘)∘ = (⨆{z. z ⋅ x∘ ≤ y∘})∘"
    by (simp add: local.fres_def)
  also have "… = ⨆{z∘ |z. z ⋅ x∘ ≤ y∘}"
    by (simp add: image_Collect)
  also have "… = ⨆{z. z∘ ⋅ x∘ ≤ y∘}"
    by (metis local.inv_invol)
  also have "… = ⨆{z. (x ⋅ z)∘ ≤ y∘}"
    by (simp add: local.inv_contrav)
  also have "… = ⨆{z. x ⋅ z ≤ y}"
    by (metis local.inv_invol local.inv_iso)
  also have "… = x → y"
    by (simp add: local.bres_def)
  finally show ?thesis.
qed

lemma fres_bres_conv: "(y∘ → x∘)∘ = x ← y"
  by (metis bres_fres_conv local.inv_invol)

sublocale invqka: involutive_kleene_algebra "(⊔)" "(⋅)" 1 ⊥ "(≤)" "(<)" qstar invol
  by unfold_locales (simp_all add: local.inv_contrav)

lemma inv_binf [simp]: "(x ⊓ y)∘ = x∘ ⊓ y∘"
proof-
  {fix z
  have "(z ≤ (x ⊓ y)∘) = (z∘ ≤ x ⊓ y)"
    using invqka.inv_adj by blast
  also have "… = (z∘ ≤ x ∧ z∘ ≤ y)"
    by simp
  also have "… = (z ≤ x∘ ∧ z ≤ y∘)"
    by (simp add: invqka.inv_adj)
  also have "… = (z ≤ x∘ ⊓ y∘)"
    by simp
  finally have "(z ≤ (x ⊓ y)∘) = (z ≤ x∘ ⊓ y∘)".}
  thus ?thesis
    using local.dual_order.antisym by blast
qed

lemma inv_inf [simp]: "(⨅X)∘ = (⨅x ∈ X. x∘)"
  by (metis invqka.inv_adj local.INF_eqI local.Inf_greatest local.Inf_lower local.inv_invol)

lemma inv_top [simp]: "⊤∘ = ⊤"
proof-
  have a: "⊤∘ ≤ ⊤"
    by simp
  hence "(⊤∘)∘ ≤ ⊤∘"
    using local.inv_iso by blast
  hence "⊤ ≤ ⊤∘"
    by simp
  thus ?thesis
    by (simp add: local.top_le)
qed

lemma inv_qstar_aux [simp]: "(x ^ i)∘ = (x∘) ^ i"
  by (induct i, simp_all add: local.power_commutes)

lemma inv_conjugate: "(x∘ ⊓ y = ⊥) = (x ⊓ y∘ = ⊥)"
  using inv_binf invqka.inv_zero by fastforce

text ‹We define domain and codomain as in relation algebra and compare with the domain
and codomain axioms above.›

definition do :: "'a ⇒ 'a" where
  "do x = 1 ⊓ (x ⋅ x∘)"

definition cd :: "'a ⇒ 'a" where
  "cd x = 1 ⊓ (x∘ ⋅ x)"

lemma do_inv: "do (x∘) = cd x"
proof-
  have "do (x∘) = 1 ⊓ (x∘ ⋅ (x∘)∘)"
    by (simp add: do_def)
  also have "… = 1 ⊓ (x∘ ⋅ x)"
    by simp
  also have "… = cd x"
    by (simp add: cd_def)
  finally show ?thesis.
qed

lemma cd_inv: "cd (x∘) = do x"
  by (simp add: cd_def do_def)

lemma do_le_top: "do x ≤ 1 ⊓ (x ⋅ ⊤)"
  by (simp add: do_def local.inf.coboundedI2 local.mult_isol)

lemma do_subid: "do x ≤ 1"
  by (simp add: do_def)

lemma cd_subid: "cd x ≤ 1"
  by (simp add: cd_def)

lemma do_bot [simp]: "do ⊥ = ⊥"
  by (simp add: do_def)

lemma cd_bot [simp]: "cd ⊥ = ⊥"
  by (simp add: cd_def)

lemma do_iso: "x ≤ y ⟹ do x ≤ do y"
  by (simp add: do_def local.inf.coboundedI2 local.inv_iso local.psrpq.mult_isol_var)

lemma cd_iso: "x ≤ y ⟹ cd x ≤ cd y"
  using cd_def local.eq_refl local.inf_mono local.inv_iso local.psrpq.mult_isol_var by presburger

lemma do_subdist: "do x ⊔ do y ≤ do (x ⊔ y)"
proof-
  have "do x ≤ do (x ⊔ y)" and "do y ≤ do (x ⊔ y)"
    by (simp_all add: do_iso)
  thus ?thesis
    by simp
qed

lemma cd_subdist: "cd x ⊔ cd y ≤ cd (x ⊔ y)"
  by (simp add: cd_iso)

lemma inv_do [simp]: "(do x)∘ = do x"
  by (simp add: do_def)

lemma inv_cd [simp]: "(cd x)∘ = cd x"
  by (metis do_inv inv_do)

lemma dedekind_modular:
  assumes "(x ⋅ y) ⊓ z ≤ (x ⊓ (z ⋅ y∘)) ⋅ (y ⊓ (x∘ ⋅ z))"
  shows "(x ⋅ y) ⊓ z ≤ (x ⊓ (z ⋅ y∘)) ⋅ y"
  using assms local.inf.cobounded1 local.mult_isol local.order_trans by blast

lemma modular_eq1:
  assumes "∀x y z w. (y ⊓ (z ⋅ x∘) ≤ w ⟶ (y ⋅ x) ⊓ z ≤ w ⋅ x)"
  shows "∀x y z. (x ⋅ y) ⊓ z ≤ (x ⊓ (z ⋅ y∘)) ⋅ y"
  using assms by blast

lemma "do x ⋅ do y = do x ⊓ do y" (* nitpick[expect=genuine]*)
  oops

lemma "p ≤ 1 ⟹ q ≤ 1 ⟹ p ⋅ q = p ⊓ q" (* nitpick[expect=genuine]*)
  oops

end

sublocale ab_unital_quantale ⊆ ciq: involutive_quantale id _ _ _ _ _ _ _ _ _ _
  by unfold_locales (simp_all add: mult_commute)

class distributive_involutive_quantale = involutive_quantale + distrib_unital_quantale

class boolean_involutive_quantale = involutive_quantale + bool_unital_quantale

begin

lemma res_peirce:
  assumes "∀x y. x∘ ⋅ -(x ⋅ y) ≤ -y"
  shows  "((x ⋅ y) ⊓ z∘ = ⊥) = ((y ⋅ z) ⊓ x∘ = ⊥)"
proof
  assume "(x ⋅ y) ⊓ z∘ = ⊥"
  hence "z∘ ≤ -(x ⋅ y)"
    by (simp add: local.inf.commute local.inf_shunt)
  thus "(y ⋅ z) ⊓ x∘ = ⊥"
    by (metis assms local.inf_shunt local.inv_conjugate local.inv_contrav local.inv_invol local.mult_isol local.order.trans)
next
  assume "(y ⋅ z) ⊓ x∘ = ⊥"
  hence "x∘ ≤ -(y ⋅ z)"
    using local.compl_le_swap1 local.inf_shunt by blast
  thus "(x ⋅ y) ⊓ z∘ = ⊥"
    by (metis assms local.dual_order.trans local.inf_shunt local.inv_conjugate local.inv_contrav local.mult_isol)
qed

lemma res_schroeder1:
  assumes "∀x y. x∘ ⋅ -(x ⋅ y) ≤ -y"
  shows "((x ⋅ y) ⊓ z = ⊥) = (y ⊓ (x∘ ⋅ z) = ⊥)"
proof
  assume h: "(x ⋅ y) ⊓ z = ⊥"
  hence "z ≤ -(x ⋅ y)"
    by (simp add: local.inf.commute local.inf_shunt)
  thus "y ⊓ (x∘ ⋅ z) = ⊥"
    by (metis assms local.dual_order.trans local.inf.commute local.inf_shunt local.mult_isol)
next
  assume "y ⊓ (x∘ ⋅ z) = ⊥"
  hence "y ≤ -(x∘ ⋅ z)"
    by (simp add: local.inf_shunt)
  thus "(x ⋅ y) ⊓ z = ⊥"
    by (metis assms local.inf_shunt local.inv_invol local.order_trans mult_isol)
qed

lemma res_schroeder2:
  assumes "∀x y. x∘ ⋅ -(x ⋅ y) ≤ -y"
  shows "((x ⋅ y) ⊓ z = ⊥) = (x ⊓ (z ⋅ y∘) = ⊥)"
  by (metis assms local.inv_invol local.res_peirce local.res_schroeder1)

lemma res_mod:
  assumes  "∀x y. x∘ ⋅ -(x ⋅ y) ≤ -y"
  shows "(x ⋅ y) ⊓ z ≤ (x ⊓ (z ⋅ y∘)) ⋅ y"
proof-
  have "(x ⋅ y) ⊓ z = ((x ⊓ ((z ⋅ y∘) ⊔ -(z ⋅ y∘))) ⋅ y) ⊓ z"
    by simp
  also have "… = (((x ⊓ (z ⋅ y∘)) ⋅ y) ⊓ z) ⊔ (((x ⊓ -(z ⋅ y∘)) ⋅ y) ⊓ z)"
    using local.chaq.wswq.distrib_left local.inf.commute local.sup_distr by presburger
  also have "… ≤ ((x ⊓ (z ⋅ y∘)) ⋅ y) ⊔ ((x ⋅ y) ⊓ (-(z ⋅ y∘)) ⋅ y ⊓ z)"
    by (metis assms local.inf.commute local.inf_compl_bot_right local.sup.orderI local.sup_inf_absorb res_schroeder2)
  also have "… ≤ ((x ⊓ (z ⋅ y∘)) ⋅ y) ⊔ ((x ⋅ y) ⊓ -z  ⊓ z)"
    by (metis assms local.dual_order.eq_iff local.inf.commute local.inf_compl_bot_right res_schroeder2)
  also have "… ≤ ((x ⊓ (z ⋅ y∘)) ⋅ y)"
    by (simp add: local.inf.commute)
  finally show ?thesis.
qed

end

text ‹The strong Gelfand property (name by Palmigiano and Re) is important for dioids and Kleene algebras.
The modular law is a convenient axiom for relational quantales, in a setting where the underlying
lattice is not boolean.›

class quantale_converse = involutive_quantale +
  assumes strong_gelfand: "x ≤ x ⋅ x∘ ⋅ x"

begin

lemma do_gelfand [simp]: "do x ⋅ do x ⋅ do x = do x"
  apply (rule order.antisym)
  using local.do_subid local.h_seq local.mult_isol apply fastforce
  by (metis local.inv_do local.strong_gelfand)

lemma cd_gelfand [simp]: "cd x ⋅ cd x ⋅ cd x = cd x"
  by (metis do_gelfand local.do_inv)

lemma do_idem [simp]: "do x ⋅ do x  = do x"
  apply (rule order.antisym)
  using local.do_subid local.mult_isol apply fastforce
  by (metis do_gelfand local.do_subid local.eq_refl local.nsrnqo.mult_oner local.psrpq.mult_isol_var)

lemma cd_idem [simp]: "cd x ⋅ cd x  = cd x"
  by (metis do_idem local.do_inv)

lemma dodo [simp]: "do (do x) = do x"
proof-
  have "do (do x) = 1 ⊓ (do x ⋅ do x)"
    using local.do_def local.inv_do by force
  also have "… = 1 ⊓ do x"
    by simp
  also have "… = do x"
    by (simp add: local.do_def)
  finally show ?thesis.
qed

lemma cdcd [simp]: "cd (cd x) = cd x"
  using cd_idem local.cd_def local.inv_cd by force

lemma docd_compat [simp]: "do (cd x) = cd x"
proof-
  have "do (cd x) = do (do (x∘))"
    by (simp add: local.do_inv)
  also have "… = do (x∘)"
    by simp
  also have "… = cd x"
    by (simp add: local.do_inv)
  finally show ?thesis.
qed

lemma cddo_compat [simp]: "cd (do x) = do x"
  by (metis docd_compat local.cd_inv local.inv_do)

end

sublocale quantale_converse ⊆ convqka: kleene_algebra_converse "(⊔)" "(⋅)" 1 ⊥ "(≤)" "(<)" invol qstar
  by unfold_locales (simp add: local.strong_gelfand)


subsection ‹Dedekind quantales›

class dedekind_quantale = involutive_quantale +
  assumes modular_law: "(x ⋅ y) ⊓ z ≤ (x ⊓ (z ⋅ y∘)) ⋅ y"

begin

sublocale convdqka: kleene_algebra_converse  "(⊔)" "(⋅)" 1 ⊥ "(≤)" "(<)" invol qstar
  by unfold_locales (metis local.inf.absorb2 local.le_top local.modular_law local.top_greatest)

subclass quantale_converse
  by unfold_locales (simp add: local.convdqka.strong_gelfand)

lemma modular_2 [simp]: "((x ⊓ (z ⋅ y∘)) ⋅ y) ⊓ z = (x ⋅ y) ⊓ z"
  apply (rule order.antisym)
  using local.inf.cobounded1 local.inf_mono local.mult_isor local.order_refl apply presburger
  by (simp add: local.modular_law)

lemma modular_1 [simp]: "(x ⋅ (y ⊓ (x∘ ⋅ z))) ⊓ z = (x ⋅ y) ⊓ z"
  by (metis local.inv_binf local.inv_contrav local.inv_invol modular_2)

lemma modular3: "(x ⋅ y) ⊓ z ≤ x ⋅ (y ⊓ (x∘ ⋅ z))"
  by (metis local.inf.cobounded1 modular_1)

text ‹The name Dedekind quantale owes to the following formula, which is equivalent to the modular law. Dedekind quantales
are called modular quantales in Rosenthal's book on quantaloids (to be precise: he discusses modular quantaloids, but the
notion of modular quantale is then obvious).›

lemma dedekind: "(x ⋅ y) ⊓ z ≤ (x ⊓ (z ⋅ y∘)) ⋅ (y ⊓ (x∘ ⋅ z))"
proof-
  have  "(x ⋅ y) ⊓ z = (x ⋅ (y ⊓ (x∘ ⋅ z))) ⊓ z"
    by simp
  also have "… ≤ (x ⊓ (z ⋅ (y ⊓ (x∘ ⋅ z))∘)) ⋅ (y ⊓ (x∘ ⋅ z))"
    using local.modular_law by presburger
  also have "… = (x ⊓ (z ⋅ (y∘ ⊓ (z∘ ⋅ x)))) ⋅ (y ⊓ (x∘ ⋅ z))"
    by simp
  also have "… ≤ (x ⊓ (z ⋅ y∘)) ⋅ (y ⊓ (x∘ ⋅ z))"
    using local.inf.commute modular_1 by fastforce
  finally show ?thesis.
qed

lemma peirce: "((x ⋅ y) ⊓ z∘ = ⊥) = ((y ⋅ z) ⊓ x∘ = ⊥)"
proof
  assume "(x ⋅ y) ⊓ z∘ = ⊥"
  hence "((x ⋅ y) ⊓ z∘) ⋅ y∘ = ⊥"
    by simp
  hence "(z∘ ⋅ y∘) ⊓ x = ⊥"
    by (metis local.inf.commute local.inv_invol local.le_bot local.modular_law)
  hence "((y ⋅ z) ⊓ x∘)∘ = ⊥∘"
    by simp
  thus "(y ⋅ z) ⊓ x∘ = ⊥"
    by (metis local.inv_invol)
next
  assume h: "(y ⋅ z) ⊓ x∘ = ⊥"
  hence "z∘ ⋅ ((y ⋅ z) ⊓ x∘) = ⊥"
    by simp
  hence "(y∘ ⋅ x∘) ⊓ z = ⊥"
    by (metis h local.inf.commute local.inv_invol local.le_bot local.mult_botr modular3)
   hence "((x ⋅ y) ⊓ z∘)∘ = ⊥∘"
    by simp
  thus "(x ⋅ y) ⊓ z∘ = ⊥"
    by (metis local.inv_invol)
qed

lemma schroeder_1: "((x ⋅ y) ⊓ z = ⊥) = (y ⊓ (x∘ ⋅ z) = ⊥)"
  by (metis local.inf.commute local.inf_bot_right local.inv_invol local.mult_botr modular_1)

lemma schroeder_2: "((x ⋅ y) ⊓ z = ⊥) = (x ⊓ (z ⋅ y∘) = ⊥)"
  by (metis local.inv_invol peirce schroeder_1)

lemma modular_eq2: "y ⊓ (z ⋅ x∘) ≤ w ⟹ (y ⋅ x) ⊓ z ≤ w ⋅ x"
  by (meson local.dual_order.trans local.eq_refl local.h_w1 local.modular_law)

lemma lla_top_aux: "p ≤ 1 ⟹ ((x ≤ p ⋅ x) = (x ≤ p ⋅ ⊤))"
proof
  assume h: "p ≤ 1"
  and h1: "x ≤ p ⋅ x"
  thus "x ≤ p ⋅ ⊤"
    by (meson local.mult_isol local.order_trans local.top_greatest)
next
  assume h: "p ≤ 1"
  and "x ≤ p ⋅ ⊤"
  hence "x = (p ⋅ ⊤) ⊓ x"
    using local.inf.absorb_iff2 by auto
  also have "… ≤ p ⋅ (⊤ ⊓ (p∘ ⋅ x))"
    using modular3 by blast
  also have "… = p ⋅ p ⋅ x"
    by (simp add: h local.convdqka.subid_conv mult_assoc)
  finally show "x ≤ p ⋅ x"
    by (metis h local.dual_order.trans local.mult_isor local.nsrnqo.mult_onel)
qed

text ‹Next we turn to properties of domain and codomain in Dedekind quantales.›

lemma lra_top_aux: "p ≤ 1 ⟹ ((x ≤ x ⋅ p ) = (x ≤ ⊤ ⋅ p))"
  by (metis convdqka.subid_conv local.inf.absorb_iff2 local.mult_1_right local.psrpq.subdistl local.sup.absorb_iff2 local.top_greatest modular_eq2)

lemma lla: "p ≤ 1 ⟹ ((do x ≤ p) = (x ≤ p ⋅ ⊤))"
proof
  assume a1: "x ≤ p ⋅ ⊤"
  assume a2: "p ≤ 1"
  have f3: "x ⋅ ⊤ ≤ p ⋅ ⊤ ⋅ ⊤"
    by (simp add: a1 local.mult_isor)
  have f4: "p ⋅ do x ≤ p"
    by (simp add: local.do_subid local.uqka.star_inductr_var_equiv local.uwqlka.star_subid)
  have "x ⋅ ⊤ ≤ p ⋅ ⊤"
    using f3 by (simp add: local.mult.semigroup_axioms semigroup.assoc)
  thus "do x ≤ p"
    using f4 a2 lla_top_aux local.do_le_top local.inf.bounded_iff local.order_trans by blast
next
  assume a1: "do x ≤ p"
  assume a2: "p ≤ 1"
  hence  "do x ⋅ x ≤ p ⋅ x"
    by (simp add: a1 local.mult_isor)
  hence "x ≤ p ⋅ x"
    using a1 local.do_def modular_eq2 by fastforce
  thus "x ≤ p ⋅ ⊤"
    by (simp add: a2 lla_top_aux)
qed

lemma lla_Inf: "do x = ⨅{p. x ≤ p ⋅ ⊤ ∧ p ≤ 1}"
  apply (rule order.antisym)
  using lla local.Inf_greatest apply fastforce
  by (metis CollectI lla local.Inf_lower local.do_subid local.order.refl)

lemma lra: "p ≤ 1 ⟹ ((cd x ≤ p) = (x ≤ ⊤ ⋅ p))"
  by (metis invqka.inv_adj lla local.convdqka.subid_conv local.do_inv local.inv_contrav local.inv_top)

lemma lra_Inf: "cd x = ⨅{p. x ≤ ⊤ ⋅ p ∧ p ≤ 1}"
  apply (rule order.antisym)
  using local.Inf_greatest lra apply fastforce
  by (metis CollectI local.Inf_lower local.cd_subid local.order.refl lra)

lemma lla_var: "p ≤ 1 ⟹ ((do x ≤ p) = (x ≤ p ⋅ x))"
  by (simp add: lla lla_top_aux)

lemma lla_Inf_var: "do x = ⨅{p. x ≤ p ⋅ x ∧ p ≤ 1}"
  apply (rule order.antisym)
  using lla_var local.Inf_greatest apply fastforce
  by (metis CollectI lla_var local.Inf_lower local.do_subid local.order.refl)

lemma lra_var: "p ≤ 1 ⟹ ((cd x ≤ p) = (x ≤ x ⋅ p))"
  by (simp add: lra lra_top_aux)

lemma lra_Inf_var: "cd x = ⨅{p. x ≤ x ⋅ p ∧ p ≤ 1}"
  apply (rule order.antisym)
  using local.Inf_greatest lra_var apply fastforce
  by (metis CollectI local.Inf_lower local.cd_subid local.order.refl lra_var)

lemma do_top: "do x = 1 ⊓ (x ⋅ ⊤)"
proof-
  have "1 ⊓ (x ⋅ ⊤) = 1 ⊓ (x ⋅ (⊤ ⊓ x∘ ⋅ 1))"
    by (metis local.inf.commute local.inf_top.left_neutral modular_1)
  also have "… = do x"
    by (simp add: local.do_def)
  finally show ?thesis..
qed

lemma cd_top: "cd x = 1 ⊓ (⊤ ⋅ x)"
  by (metis do_top invqka.inv_one local.do_inv local.inv_binf local.inv_cd local.inv_contrav local.inv_invol local.inv_top)

text ‹We start deriving the axioms of modal semirings and modal quantales.›

lemma do_absorp: "x ≤ do x ⋅ x"
  using lla_var local.do_subid by blast

lemma cd_absorp: "x ≤ x ⋅ cd x"
  using local.cd_subid lra_var by blast

lemma do_absorp_eq [simp]: "do x ⋅ x = x"
  using do_absorp local.do_subid local.dual_order.antisym local.h_w1 by fastforce

lemma cd_absorp_eq [simp]: "x ⋅ cd x = x"
  by (metis do_top local.do_inv local.inf_top.right_neutral local.nsrnqo.mult_oner modular_1)

lemma do_top2: "x ⋅ ⊤ = do x ⋅ ⊤"
proof (rule order.antisym)
  have "x ⋅ ⊤ = do x ⋅ x ⋅ ⊤"
    by simp
  also have "… ≤ do x ⋅ ⊤ ⋅ ⊤"
    using local.psrpq.mult_double_iso local.top_greatest by presburger
  also have "… = do x ⋅ ⊤"
    by (simp add: local.mult.semigroup_axioms semigroup.assoc)
  finally show "x ⋅ ⊤ ≤ do x ⋅ ⊤".
  have "do x ⋅ ⊤ = (1 ⊓ (x ⋅ ⊤)) ⋅ ⊤"
    by (simp add: do_top)
  also have "… ≤ (1 ⋅ ⊤) ⊓ (x ⋅ ⊤ ⋅ ⊤)"
    by (simp add: local.mult_isor)
  also have "… = x ⋅ ⊤"
    by (simp add: mult_assoc)
  finally show "do x ⋅ ⊤ ≤ x ⋅ ⊤".
qed

lemma cd_top2: "⊤ ⋅ x  = ⊤ ⋅ cd x"
  by (metis do_top2 local.do_inv local.inv_cd local.inv_contrav local.inv_invol local.inv_top)

lemma do_local [simp]: "do (x ⋅ do y) = do (x ⋅ y)"
proof-
  have "do (x ⋅ do y) = 1 ⊓ (x ⋅ do y ⋅ ⊤)"
    using do_top by force
  also have "… = 1 ⊓ (x ⋅ y ⋅ ⊤)"
    using do_top2 mult_assoc by force
  also have "… = do (x ⋅ y)"
    by (simp add: do_top)
  finally show ?thesis
    by force
qed

lemma cd_local [simp]: "cd (cd x ⋅ y) = cd (x ⋅ y)"
  by (metis cd_top cd_top2 mult_assoc)

lemma do_fix_subid: "(do x = x) = (x ≤ 1)"
proof
  assume "do x = x"
  thus "x ≤ 1"
    by (metis local.do_subid)
next
  assume a: "x ≤ 1"
  hence "x = do x ⋅ x"
    by simp
  hence b: "x ≤ do x"
    by (metis a local.mult_isol local.nsrnqo.mult_oner)
  have "x ⋅ x ≤ x"
    using a local.mult_isor by fastforce
  hence  "do x ≤ x"
    by (simp add: a lla_var local.le_top lra_top_aux)
  thus "do x = x"
    by (simp add: b local.dual_order.antisym)
qed

lemma cd_fix_subid: "(cd x = x) = (x ≤ 1)"
  by (metis local.convdqka.subid_conv local.do_inv local.do_fix_subid local.docd_compat)

lemma do_inf2: "do (do x ⊓ do y) = do x ⊓ do y"
  using do_top local.do_fix_subid local.inf.assoc by auto

lemma do_inf_comp: "do x ⋅ do y = do x ⊓ do y"
  by (smt (verit, best) local.do_def local.do_idem local.do_fix_subid local.dodo local.dual_order.trans local.inf_commute local.inf_idem local.inv_contrav local.inv_do local.mult_1_right local.mult_isol modular_1 mult_assoc)

lemma cd_inf_comp: "cd x ⋅ cd y = cd x ⊓ cd y"
  by (metis do_inf_comp local.docd_compat)

lemma subid_mult_meet: "p ≤ 1 ⟹ q ≤ 1 ⟹ p ⋅ q = p ⊓ q"
  by (metis do_inf_comp local.do_fix_subid)

lemma dodo_sup: "do (do x ⊔ do y) = do x ⊔ do y"
proof-
  have "do (do x ⊔ do y) = 1 ⊓ ((do x ⊔ do y) ⋅ (do x ⊔ do y)∘)"
    using local.do_def by blast
  also have "… = 1 ⊓ ((do x ⊔ do y) ⋅ (do x ⊔ do y))"
    by simp
  also have "… = 1 ⊓ (do x ⊔ do y)"
    using local.do_subid local.dodo local.inf.idem local.le_supI subid_mult_meet by presburger
  also have "… = do x ⊔ do y"
    by (simp add: local.do_def local.inf_absorb2)
  finally show ?thesis.
qed

lemma do_sup [simp]: "do (x ⊔ y) = do x ⊔ do y"
proof-
  have "do (x ⊔ y) = 1 ⊓ ((x ⊔ y) ⋅ ⊤)"
    by (simp add: do_top)
  also have "… = 1 ⊓ (x ⋅ ⊤ ⊔ y ⋅ ⊤)"
    by simp
  also have "… = 1 ⊓ (do x ⋅ ⊤ ⊔ do y ⋅ ⊤)"
    using do_top2 by force
  also have "… = 1 ⊓ ((do x ⊔ do y) ⋅ ⊤)"
    by simp
  also have "… = do (do x ⊔ do y)"
    by (simp add: do_top)
  finally show ?thesis
    by (simp add: dodo_sup)
qed

lemma cdcd_sup: "cd (cd x ⊔ cd y) = cd x ⊔ cd y"
  using local.cd_fix_subid by fastforce

lemma cd_sup [simp]: "cd (x ⊔ y) = cd x ⊔ cd y"
  by (metis do_sup local.do_inv local.inv_binsup)

text ‹Next we show that Dedekind quantales are modal quantales, hence also modal semirings.›

sublocale dmq: dc_modal_quantale 1 "(⋅)" Inf Sup "(⊓)" "(≤)" "(<)" "(⊔)" "⊥" "⊤" cd do
proof
  show "⋀x. cd x ≤ 1"
    by (simp add: cd_top)
  show "⋀x. do x ≤ 1"
    by (simp add: do_top)
qed simp_all

lemma do_top3 [simp]: "do (x ⋅ ⊤) = do x"
  using dmq.coddual.le_top dmq.dqmsr.domain_1'' local.do_iso local.order.antisym by presburger

lemma cd_top3 [simp]: "cd (⊤ ⋅ x) = cd x"
  by (simp add: cd_top dmq.coddual.mult_assoc)

lemma dodo_Sup_pres: "do (⨆x ∈ X. do x) = (⨆x ∈ X. do x)"
  by (simp add: local.SUP_least local.do_fix_subid)

text ‹The domain elements form a complete Heyting algebra.›

lemma do_complete_heyting: "do x ⊓ (⨆y ∈ Y. do y) = (⨆y ∈ Y. do x ⊓ do y)"
proof-
  have "do x ⊓ (⨆y ∈ Y. do y) = do x ⋅ (⨆y ∈ Y. do y)"
    by (metis do_inf_comp dodo_Sup_pres)
  also have "… = (⨆y ∈ Y. do x ⋅ do y)"
    by (simp add: dmq.coddual.Sup_distr image_image)
  also have "… = (⨆y ∈ Y. do x ⊓ do y)"
    using do_inf_comp by force
  finally show ?thesis.
qed

lemma cdcd_Sup_pres: "cd (⨆x ∈ X. cd x) = (⨆x ∈ X. cd x)"
  by (simp add: local.SUP_least local.cd_fix_subid)

lemma cd_complete_heyting: "cd x ⊓ (⨆y ∈ Y. cd y) = (⨆y ∈ Y. cd x ⊓ cd y)"
proof-
  have "cd x ⊓ (⨆y ∈ Y. cd y) = cd x ⋅ (⨆y ∈ Y. cd y)"
    by (metis cd_inf_comp cdcd_Sup_pres)
  also have "… = (⨆y ∈ Y. cd x ⋅ cd y)"
    by (simp add: dmq.coddual.Sup_distr image_image)
  also have "… = (⨆y ∈ Y. cd x ⊓ cd y)"
    using cd_inf_comp by force
  finally show ?thesis.
qed

lemma subid_complete_heyting:
  assumes "p ≤ 1"
  and "∀q ∈ Q. q ≤ 1"
  shows "p ⊓ (⨆Q) = (⨆q ∈ Q. p ⊓ q)"
proof-
  have a: "do p = p"
    by (simp add: assms(1) local.do_fix_subid)
  have b: "∀q ∈ Q. do q = q"
    using assms(2) local.do_fix_subid by presburger
  hence "p ⊓ (⨆Q) = do p ⊓ (⨆q ∈ Q. do q)"
    by (simp add: a)
  also have "… = (⨆q ∈ Q. do p ⊓ do q)"
    using do_complete_heyting by blast
  also have "… = (⨆q ∈ Q. p ⊓ q)"
    using a b by force
  finally show ?thesis.
qed

text ‹Next we show that domain and codomain preserve arbitrary Sups.›

lemma do_Sup_pres_aux: "(⨆x ∈ X. do x ⋅ ⊤) = (⨆x ∈ do ` X. x ⋅ ⊤)"
  by (smt (verit, best) Sup.SUP_cong image_image)

lemma do_Sup_pres: "do (⨆x ∈ X. x) = (⨆x ∈ X. do x)"
proof-
  have "do (⨆x ∈ X. x) = 1 ⊓ ((⨆x ∈ X. x) ⋅ ⊤)"
    by (simp add: do_top)
  also have "… = 1 ⊓ (⨆x ∈ X. x ⋅ ⊤)"
    by (simp add: dmq.coddual.Sup_distl)
  also have "… = 1 ⊓ (⨆x ∈ X. do x ⋅ ⊤)"
    using do_top2 by force
  also have "… = 1 ⊓ (⨆x ∈ do ` X. x ⋅ ⊤)"
    using do_Sup_pres_aux by presburger
  also have "… = 1 ⊓ ((⨆x ∈ X. do x) ⋅ ⊤)"
    using dmq.coddual.Sup_distl by presburger
  also have "… = do (⨆x ∈ X. do x)"
    by (simp add: do_top)
  finally show ?thesis
    using dodo_Sup_pres by presburger
qed

lemma cd_Sup_pres: "cd (⨆x ∈ X. x) = (⨆x ∈ X. cd x)"
proof-
  have "cd (⨆x ∈ X. x) = do ((⨆x ∈ X. x)∘)"
    using local.do_inv by presburger
  also have "… = do (⨆x ∈ X. x∘)"
    by simp
  also have "… = (⨆x ∈ X. do (x∘))"
    by (metis do_Sup_pres image_ident image_image)
  also have "… = (⨆x ∈ X. cd x)"
    using local.do_inv by presburger
  finally show ?thesis.
qed

lemma do_inf: "do (x ⊓ y) = 1 ⊓ (y ⋅ x∘)"
  by (smt (z3) do_absorp_eq invqka.inv_one local.do_def local.inf_commute local.inv_binf local.inv_contrav local.inv_invol local.mult_1_right modular_1 modular_2 mult_assoc)

lemma cd_inf: "cd (x ⊓ y) = 1 ⊓ (y∘ ⋅ x)"
  by (metis do_inf local.do_inv local.inv_binf local.inv_invol)

lemma do_bres_prop: "p ≤ 1 ⟹ do (x → p ⋅ ⊤) = 1 ⊓ (x → p ⋅ ⊤)"
  by (simp add: do_top)

lemma cd_fres_prop: "p ≤ 1 ⟹ cd (⊤ ⋅ p ← x) = 1 ⊓ (⊤ ⋅ p ← x)"
  by (simp add: cd_top)

lemma do_meet_prop: "(do p ⋅ x) ⊓ (x ⋅ do q) = do p ⋅ x ⋅ do q"
proof (rule order.antisym)
  have "x ⊓ (do p ⋅ x ⋅ do q) ≤ do p ⋅ x"
    by (simp add: dmq.dqmsr.dom_subid_aux2'' local.inf.coboundedI2)
  thus  "(do p ⋅ x) ⊓ (x ⋅ do q) ≤ do p ⋅ x ⋅ do q"
    by (simp add: local.inf.commute modular_eq2)
next
  have "do p ⋅ x ⋅ do q = (do p ⋅ x ⋅ do q) ⊓ (do p ⋅ x ⋅ do q)"
    by simp
  also have "… ≤ (do p ⋅ x) ⊓ (x ⋅ do q)"
    using dmq.dqmsr.dom_subid_aux2 dmq.dqmsr.dom_subid_aux2'' local.psrpq.mult_isol_var by auto
  finally show "do p ⋅ x ⋅ do q ≤ (do p ⋅ x) ⊓ (x ⋅ do q)".
qed

lemma subid_meet_prop: "p ≤ 1 ⟹ q ≤ 1 ⟹ (p ⋅ x) ⊓ (x ⋅ q) = p ⋅ x ⋅ q"
  by (metis do_fix_subid do_meet_prop)

text ‹Next we consider box and diamond operators like in modal semirings and modal quantales.
These are inherited from domain quantales. Diamonds are defined with respect to domain and codomain.
The box operators are defined as Sups and hence right adjoints of diamonds.›

abbreviation "do_dia ≡ dmq.fd'"

abbreviation "cd_dia ≡ dmq.bd'"

abbreviation "do_box ≡ dmq.bb"

abbreviation "cd_box ≡ dmq.fb"

text ‹In the sense of modal logic, the domain-based diamond is a backward operator, the codomain-based
one a forward operator. These are related by opposition/converse.›

lemma do_dia_cd_dia_conv: "p ≤ 1 ⟹ do_dia (x∘) p = cd_dia x p"
  by (simp add: convdqka.subid_conv dmq.coddual.dqmsr.fd_def dmq.dqmsr.fd_def local.cd_def local.do_def)

lemma cd_dia_do_dia_conv: "p ≤ 1 ⟹ cd_dia (x∘) p = do_dia x p"
  by (metis do_dia_cd_dia_conv local.inv_invol)

text ‹Diamonds preserve sups in both arguments.›

lemma do_dia_Sup: "do_dia (⨆X) p = (⨆x ∈ X. do_dia x p)"
proof-
  have "do_dia (⨆X) p = do ((⨆X) ⋅ p)"
    by (simp add: dmq.dqmsr.fd_def)
  also have "… = do (⨆x ∈ X. x ⋅ p)"
    using local.Sup_distr by fastforce
 also have "… = (⨆x ∈ X. do (x ⋅ p))"
   by (metis do_Sup_pres image_ident image_image)
  also have "… = (⨆x ∈ X. do_dia x p)"
    using dmq.dqmsr.fd_def by fastforce
  finally show ?thesis.
qed

lemma do_dia_Sup2: "do_dia x (⨆P) = (⨆p ∈ P. do_dia x p)"
proof-
  have  "do_dia x (⨆P) = do (x ⋅ (⨆P))"
    by (simp add: dmq.dqmsr.fd_def)
  also have "… = (⨆p ∈ P. do (x ⋅ p))"
    by (metis dmq.coddual.Sup_distr do_Sup_pres image_ident image_image)
  also have "… = (⨆p ∈ P. do_dia x p)"
    using dmq.dqmsr.fd_def by auto
  finally show ?thesis.
qed

lemma cd_dia_Sup: "cd_dia (⨆X) p = (⨆x ∈ X. cd_dia x p)"
proof-
  have "cd_dia (⨆X) p = cd (p ⋅ (⨆X))"
    by (simp add: dmq.coddual.dqmsr.fd_def)
  also have "… = cd (⨆x ∈ X. p ⋅ x)"
    using dmq.coddual.Sup_distr by auto
 also have "… = (⨆x ∈ X. cd (p ⋅ x))"
   by (metis cd_Sup_pres image_ident image_image)
  also have "… = (⨆x ∈ X. cd_dia x p)"
    using dmq.coddual.dqmsr.fd_def by force
  finally show ?thesis.
qed

lemma cd_dia_Sup2: "cd_dia x (⨆P) = (⨆p ∈ P. cd_dia x p)"
proof-
  have  "cd_dia x (⨆P) = cd ((⨆P) ⋅ x)"
    by (simp add: dmq.coddual.dqmsr.fd_def)
  also have "… = (⨆p ∈ P. cd (p ⋅ x))"
    by (metis cd_Sup_pres dmq.coddual.Sup_distl image_ident image_image)
  also have "… = (⨆p ∈ P. cd_dia x p)"
    using dmq.coddual.dqmsr.fd_def by auto
  finally show ?thesis.
qed

text ‹The domain-based box is a forward operator, the codomain-based on a backward one. These interact
again with respect to converse.›

lemma do_box_var: "p ≤ 1 ⟹ do_box x p = ⨆{q. do_dia x q ≤ p ∧ q ≤ 1}"
  by (smt (verit, best) Collect_cong dmq.bb_def dmq.dqmsr.fdia_d_simp local.do_fix_subid local.dodo)

lemma cd_box_var: "p ≤ 1 ⟹ cd_box x p = ⨆{q. cd_dia x q ≤ p ∧ q ≤ 1}"
  by (smt (verit, best) Collect_cong dmq.coddual.dqmsr.fdia_d_simp dmq.fb_def local.cd_fix_subid local.cdcd)

lemma do_box_cd_box_conv: "p ≤ 1 ⟹ do_box (x∘) p = cd_box x p"
proof-
  assume a: "p ≤ 1"
  hence "do_box (x∘) p = ⨆{q. do_dia (x∘) q ≤ p ∧ q ≤ 1}"
    by (simp add: do_box_var)
  also have "… =  ⨆{q. cd_dia x q ≤ p ∧ q ≤ 1}"
    by (metis do_dia_cd_dia_conv)
  also have "… = cd_box x p"
    using a cd_box_var by auto
  finally show ?thesis.
qed

lemma cd_box_do_box_conv: "p ≤ 1 ⟹ cd_box (x∘) p = do_box x p"
  by (metis do_box_cd_box_conv local.inv_invol)

lemma do_box_subid: "do_box x p ≤ 1"
  using dmq.bb_def local.Sup_le_iff by force

lemma cd_box_subid: "p ≤ 1 ⟹ cd_box x p ≤ 1"
  by (metis do_box_subid local.do_box_cd_box_conv)

text ‹Next we prove that boxes and diamonds are adjoints, and then demodalisation laws known
from modal semirings.›

lemma do_dia_do_box_galois:
  assumes "p ≤ 1"
  and "q ≤ 1"
  shows "(do_dia x p ≤ q) = (p ≤ do_box x q)"
proof
  show "do_dia x p ≤ q ⟹ p ≤ do_box x q"
    by (simp add: assms do_box_var local.Sup_upper)
next
  assume "p ≤ do_box x q"
  hence "do_dia x p ≤ do (x ⋅ ⨆{t. do_dia x t ≤ q ∧ t ≤ 1})"
    by (simp add: assms(2) local.dmq.dqmsr.fd_def local.do_box_var local.do_iso local.mult_isol)
  also have "… = ⨆{do (x ⋅ t) |t. do_dia x t ≤ q ∧ t ≤ 1}"
    by (metis do_Sup_pres image_ident image_image local.Sup_distl setcompr_eq_image)
  also have "… = ⨆{do_dia x t |t. do_dia x t ≤ q ∧ t ≤ 1}"
    using local.dmq.dqmsr.fd_def by fastforce
  also have "… ≤ q"
    using local.Sup_le_iff by blast
  finally have "do_dia x p ≤ q".
  thus "p ≤ do_box x q ⟹ do_dia x p ≤ q".
qed

lemma cd_dia_cd_box_galois:
  assumes "p ≤ 1"
  and "q ≤ 1"
shows "(cd_dia x p ≤ q) = (p ≤ cd_box x q)"
  by (metis assms do_box_cd_box_conv do_dia_cd_dia_conv do_dia_do_box_galois)

lemma do_dia_demod_subid:
  assumes "p ≤ 1"
  and "q ≤ 1"
shows "(do_dia x p ≤ q) = (x ⋅ p ≤ q ⋅ x)"
  by (metis assms dmq.dqmsr.fdemodalisation2 local.do_fix_subid)

text ‹The demodalisation laws have variants based on residuals.›

lemma do_dia_demod_subid_fres:
  assumes "p ≤ 1"
  and "q ≤ 1"
  shows "(do_dia x p ≤ q) = (p ≤ x → q ⋅ x)"
  by (simp add: assms do_dia_demod_subid local.bres_galois)

lemma do_dia_demod_subid_var:
  assumes "p ≤ 1"
  and "q ≤ 1"
shows "(do_dia x p ≤ q) = (x ⋅ p ≤ q ⋅ ⊤)"
  by (simp add: assms(2) dmq.dqmsr.fd_def lla)

lemma do_dia_demod_subid_var_fres:
  assumes "p ≤ 1"
  and "q ≤ 1"
shows "(do_dia x p ≤ q) = (p ≤ x → q ⋅ ⊤)"
  by (simp add: assms do_dia_demod_subid_var local.bres_galois)

lemma cd_dia_demod_subid:
  assumes "p ≤ 1"
  and "q ≤ 1"
shows "(cd_dia x p ≤ q) = (p ⋅ x ≤ x ⋅ q)"
  by (metis assms dmq.coddual.dqmsr.fdemodalisation2 local.cd_fix_subid)

lemma cd_dia_demod_subid_fres:
  assumes "p ≤ 1"
  and "q ≤ 1"
shows "(cd_dia x p ≤ q) = (p ≤ x ⋅ q ← x)"
  by (simp add: assms cd_dia_demod_subid local.fres_galois)

lemma cd_dia_demod_subid_var:
  assumes "p ≤ 1"
  and "q ≤ 1"
shows "(cd_dia x p ≤ q) = (p ⋅ x ≤ ⊤ ⋅ q)"
  by (simp add: assms(2) dmq.coddual.dqmsr.fd_def lra)

lemma cd_dia_demod_subid_var_fres:
  assumes "p ≤ 1"
  and "q ≤ 1"
shows "(cd_dia x p ≤ q) = (p ≤ ⊤ ⋅ q ← x)"
  by (simp add: assms cd_dia_demod_subid_var local.fres_galois)

lemma do_box_iso:
  assumes "p ≤ 1"
  and "q ≤ 1"
  and "p ≤ q"
shows "do_box x p ≤ do_box x q"
  by (meson assms do_box_subid do_dia_do_box_galois local.order.refl local.order.trans)

lemma cd_box_iso:
  assumes "p ≤ 1"
  and "q ≤ 1"
  and "p ≤ q"
shows "cd_box x p ≤ cd_box x q"
  by (metis assms do_box_cd_box_conv do_box_iso)

lemma do_box_demod_subid:
  assumes "p ≤ 1"
  and "q ≤ 1"
  shows "(p ≤ do_box x q) = (x ⋅ p ≤ q ⋅ x)"
  using assms do_dia_do_box_galois local.do_dia_demod_subid by force

lemma do_box_demod_subid_bres:
  assumes "p ≤ 1"
  and "q ≤ 1"
  shows "(p ≤ do_box x q) = (p ≤ x → q ⋅ x)"
  by (simp add: assms do_box_demod_subid local.bres_galois)

lemma do_box_demod_subid_var:
  assumes "p ≤ 1"
  and "q ≤ 1"
  shows "(p ≤ do_box x q) = (x ⋅ p ≤ q ⋅ ⊤)"
  using assms do_dia_demod_subid_var do_dia_do_box_galois by auto

lemma do_box_demod_subid_var_bres:
  assumes "p ≤ 1"
  and "q ≤ 1"
  shows "(p ≤ do_box x q) = (p ≤ x → q ⋅ ⊤)"
  by (simp add: assms do_box_demod_subid_var local.bres_galois)

lemma do_box_demod_subid_var_bres_do:
  assumes "p ≤ 1"
  and "q ≤ 1"
  shows "(p ≤ do_box x q) = (p ≤ do (x → q ⋅ ⊤))"
  by (simp add: assms do_box_demod_subid_var_bres do_top)

lemma cd_box_demod_subid:
  assumes "p ≤ 1"
  and "q ≤ 1"
  shows "(p ≤ cd_box x q) = (p ⋅ x ≤ x ⋅ q)"
  using assms local.cd_dia_cd_box_galois local.cd_dia_demod_subid by force

lemma cd_box_demod_subid_fres:
  assumes "p ≤ 1"
  and "q ≤ 1"
  shows "(p ≤ cd_box x q) = (p ≤ x ⋅ q ← x)"
  by (simp add: assms cd_box_demod_subid local.fres_galois)

lemma cd_box_demod_subid_var:
  assumes "p ≤ 1"
  and "q ≤ 1"
  shows "(p ≤ cd_box x q) = (p ⋅ x ≤ ⊤ ⋅ q)"
  using assms cd_dia_cd_box_galois cd_dia_demod_subid_var by force

lemma cd_box_demod_subid_var_fres:
  assumes "p ≤ 1"
  and "q ≤ 1"
  shows "(p ≤ cd_box x q) = (p ≤ ⊤ ⋅ q ← x)"
  by (simp add: assms cd_box_demod_subid_var local.fres_galois)

text ‹We substitute demodalisation inequalities for diamonds in the definitions of boxes.›

lemma do_box_var2: "p ≤ 1 ⟹ do_box x p = ⨆{q. x ⋅ q ≤ p ⋅ x ∧ q ≤ 1}"
  unfolding do_box_var by (meson do_dia_demod_subid)

lemma do_box_bres1: "p ≤ 1 ⟹ do_box x p = ⨆{q. q ≤ x → p ⋅ x ∧ q ≤ 1}"
  unfolding do_box_var by (meson do_dia_demod_subid_fres)

lemma do_box_bres2: "p ≤ 1 ⟹ do_box x p = ⨆{q. q ≤ x → p ⋅ ⊤ ∧ q ≤ 1}"
  unfolding do_box_var by (simp add: dmq.dqmsr.fd_def lla local.bres_galois)

lemma do_box_var3: "p ≤ 1 ⟹ do_box x p = ⨆{q. x ⋅ q ≤ p ⋅ ⊤ ∧ q ≤ 1}"
  unfolding do_box_var using dmq.dqmsr.fd_def lla by force

lemma cd_box_var2: "p ≤ 1 ⟹ cd_box x p = ⨆{q. q ⋅ x ≤ x ⋅ p ∧ q ≤ 1}"
  unfolding cd_box_var by (metis cd_dia_demod_subid)

lemma cd_box_var3: "p ≤ 1 ⟹ cd_box x p = ⨆{q. q ⋅ x ≤ ⊤ ⋅ p ∧ q ≤ 1}"
  unfolding cd_box_var by (simp add: dmq.coddual.dqmsr.fd_def lra)

text ‹Using these results we get a simple characterisation of boxes via domain and codomain.
Similar laws can be found implicitly in Doornbos, Backhouse and van der Woude's paper on a calculational
approach to mathematical induction, which speaks about wlp operators instead  modal operators.›

lemma bres_do_box: "p ≤ 1 ⟹ do_box x p = do (x → p ⋅ ⊤)"
  by (meson do_box_demod_subid_var_bres_do do_box_subid local.cd_fix_subid local.cddo_compat local.dual_order.antisym local.eq_refl)

lemma bres_do_box_var: "p ≤ 1 ⟹ do_box x p = 1 ⊓ (x → p ⋅ ⊤)"
  using bres_do_box do_bres_prop by force

lemma bres_do_box_top: "p ≤ 1 ⟹ (do_box x p) ⋅ ⊤ = x → p ⋅ ⊤"
  using bres_do_box do_top2 by auto

lemma fres_cd_box: "p ≤ 1 ⟹ cd_box x p = cd (⊤ ⋅ p ← x)"
proof-
  assume h0: "p ≤ 1"
  {fix q
  assume h1: "q ≤ 1"
  have "(q ≤ cd_box x p) = (q ⋅ x ≤ ⊤ ⋅ p)"
    by (simp add: cd_box_demod_subid_var h0 h1)
  also have "… = (q ≤ ⊤ ⋅ p ← x)"
    by (simp add: local.fres_galois)
  also have "… = (q ≤ 1 ⊓ (⊤ ⋅ p ← x))"
    by (simp add: h1)
  also have "… = (q ≤ cd (⊤ ⋅ p ← x))"
    by (simp add: cd_fres_prop h0)
  finally have "(q ≤ cd_box x p) = (q ≤ cd (⊤ ⋅ p ← x))".}
  hence "∀y. y ≤ cd_box x p ⟷ y ≤ cd (⊤ ⋅ p ← x)"
    by (meson cd_box_subid dmq.coddual.dqmsr.dpd3 h0 local.dual_order.trans)
  thus ?thesis
    using local.dual_order.antisym by blast
qed

lemma fres_cd_box_var: "p ≤ 1 ⟹ cd_box x p = 1 ⊓ (⊤ ⋅ p ← x)"
  by (simp add: cd_fres_prop fres_cd_box)

lemma fres_cd_box_top: "p ≤ 1 ⟹ ⊤ ⋅ cd_box x p = ⊤ ⋅ p ← x"
  using cd_top2 fres_cd_box by auto


text ‹Next we show that the box operators act on the complete Heyting algebra of subidentities.›

lemma cd_box_act:
  assumes "p ≤ 1"
  shows "cd_box (x ⋅ y) p = cd_box x (cd_box y p)"
proof-
  {fix q
    assume a: "q ≤ 1"
    hence "(q ≤ cd_box (x ⋅ y) p) = (cd_dia (x ⋅ y) q ≤ p)"
      by (simp add: assms cd_dia_cd_box_galois)
    also have "… = (cd_dia y (cd_dia x q) ≤ p)"
      by (simp add: local.dmq.coddual.dqmsr.fdia_mult)
    also have "… = (cd_dia x q ≤ cd_box y p)"
      using assms cd_dia_cd_box_galois cd_top dmq.coddual.dqmsr.fd_def by force
    also have "… = (q ≤ cd_box x (cd_box y p))"
      by (simp add: a assms cd_dia_cd_box_galois local.cd_box_subid)
    finally have "(q ≤ cd_box (x ⋅ y) p) = (q ≤ cd_box x (cd_box y p))".}
  thus ?thesis
    by (meson assms local.cd_box_subid local.dual_order.eq_iff)
qed

lemma do_box_act:
  assumes "p ≤ 1"
  shows "do_box (x ⋅ y) p = do_box y (do_box x p)"
  by (smt (verit) assms cd_box_act local.cd_box_do_box_conv local.do_box_subid local.inv_contrav)

text ‹Next we show that the box operators are Sup reversing in the first and Inf preserving
in the second argument.›

lemma do_box_sup_inf: "p ≤ 1 ⟹ do_box (x ⊔ y) p = do_box x p ⋅ do_box y p"
proof-
  assume h1: "p ≤ 1"
  {fix q
  assume h2: "q ≤ 1"
  hence "(q ≤ do_box (x ⊔ y) p) = (do_dia (x ⊔ y) q ≤ p)"
    by (simp add: do_dia_do_box_galois h1)
  also have "… = (do_dia x q ≤ p ∧ do_dia y q ≤ p)"
    by (simp add: dmq.dqmsr.fdia_add2)
  also have "… = (q ≤ do_box x p ∧ q ≤ do_box y p)"
    by (simp add: do_dia_do_box_galois h1 h2)
  also have "… = (q ≤ do_box x p ⋅ do_box y p)"
    by (simp add: do_box_subid subid_mult_meet)
  finally have "(q ≤ do_box (x ⊔ y) p) = (q ≤ do_box x p ⋅ do_box y p)".}
  hence "∀z. z ≤ do_box (x ⊔ y) p ⟷ z ≤ do_box x p ⋅ do_box y p"
    by (metis do_box_subid local.dual_order.trans local.inf.boundedE subid_mult_meet)
  thus ?thesis
    using local.dual_order.antisym by blast
qed

lemma do_box_sup_inf_var: "p ≤ 1 ⟹ do_box (x ⊔ y) p = do_box x p ⊓ do_box y p"
  by (simp add: do_box_subid do_box_sup_inf subid_mult_meet)

lemma do_box_Sup_Inf:
  assumes "X ≠ {}"
  and "p ≤ 1"
  shows "do_box (⨆X) p = (⨅x ∈ X. do_box x p)"
proof-
  {fix q
    assume h: "q ≤ 1"
    hence "(q ≤ do_box (⨆X) p) = (do_dia (⨆X) q ≤ p)"
    by (simp add: do_dia_do_box_galois assms(2))
  also have "… = ((⨆x ∈ X. do_dia x q) ≤ p)"
    using do_dia_Sup by force
  also have "… = (∀x ∈ X. do_dia x q ≤ p)"
    by (simp add: local.SUP_le_iff)
  also have "… = (∀x ∈ X. q ≤ do_box x p)"
    using do_dia_do_box_galois assms(2) h by blast
  also have "… = (q ≤ (⨅x ∈ X. do_box x p))"
    by (simp add: local.le_INF_iff)
  finally have "(q ≤ do_box (⨆X) p) = (q ≤ (⨅x ∈ X. do_box x p))".}
  hence "∀y. y ≤ do_box (⨆X) p ⟷ y ≤ (⨅x ∈ X. do_box x p)"
    by (smt (verit, ccfv_threshold) assms(1) do_box_subid local.INF_le_SUP local.SUP_least local.order_trans)
  thus ?thesis
    using local.dual_order.antisym by blast
qed

lemma do_box_Sup_Inf2:
  assumes "P ≠ {}"
  and "∀p ∈ P. p ≤ 1"
  shows "do_box x (⨅P) = (⨅p ∈ P. do_box x p)"
proof-
  have h0: "(⨅p ∈ P. do_box x p) ≤ 1"
  by (meson all_not_in_conv assms(1) do_box_subid local.INF_lower2)
  {fix q
    assume h1: "q ≤ 1"
    hence "(q ≤ do_box x (⨅P)) = (do_dia x q ≤ ⨅P)"
      by (simp add: assms do_dia_do_box_galois local.Inf_less_eq)
    also have "… = (∀p ∈ P. do_dia x q ≤ p)"
      using local.le_Inf_iff by blast
    also have "… = (∀p ∈ P. q ≤ do_box x p)"
      using assms(2) do_dia_do_box_galois h1 by auto
    also have "… = (q ≤ (⨅p ∈ P. do_box x p))"
      by (simp add: local.le_INF_iff)
    finally have "(q ≤ do_box x (⨅P)) = (q ≤ (⨅p ∈ P. do_box x p))".}
  thus ?thesis
    using do_box_subid h0 local.dual_order.antisym by blast
qed

lemma cd_box_sup_inf: "p ≤ 1 ⟹ cd_box (x ⊔ y) p = cd_box x p ⋅ cd_box y p"
  by (metis do_box_cd_box_conv do_box_sup_inf local.inv_binsup)

lemma cd_box_sup_inf_var: "p ≤ 1 ⟹ cd_box (x ⊔ y) p = cd_box x p ⊓ cd_box y p"
  by (simp add: cd_box_subid cd_box_sup_inf subid_mult_meet)

lemma cd_box_Sup_Inf:
  assumes "X ≠ {}"
  and "p ≤ 1"
shows "cd_box (⨆X) p = (⨅x ∈ X. cd_box x p)"
proof-
  have "cd_box (⨆X) p = do_box ((⨆X)∘) p"
    using assms(2) do_box_cd_box_conv by presburger
  also have "… = (⨅y ∈ {x∘|x. x ∈ X}. do_box y p)"
    by (simp add: Setcompr_eq_image assms do_box_Sup_Inf)
  also have "… = (⨅x ∈ X. do_box (x∘) p)"
    by (simp add: Setcompr_eq_image image_image)
  also have "… = (⨅x ∈ X. cd_box x p)"
    using assms(2) do_box_cd_box_conv by force
  finally show ?thesis.
qed

lemma cd_box_Sup_Inf2:
  assumes "P ≠ {}"
  and "∀p ∈ P. p ≤ 1"
shows "cd_box x (⨅P) = (⨅p ∈ P. cd_box x p)"
proof-
  have "cd_box x (⨅P) = do_box (x∘) (⨅P)"
    by (simp add: assms do_box_cd_box_conv local.Inf_less_eq)
  also have "… = (⨅p ∈ P. do_box (x∘) p)"
    using assms do_box_Sup_Inf2 by presburger
  also have "… = (⨅p ∈ P. cd_box x p)"
    using assms(2) do_box_cd_box_conv by force
  finally show ?thesis.
qed

text ‹Next we define an antidomain operation in the style of modal semirings. A natural condition is
that the antidomain of an element is the greatest test that cannot be left-composed with that elements,
and hence a greatest left annihilator. The definition of anticodomain is similar. As we are not in a
boolean domain algebra, we cannot expect that the antidomain of the antidomain yields the domain or
that the union of a domain element with the corresponding antidomain element equals one.›

definition "ado x = ⨆{p. p ⋅ x = ⊥ ∧ p ≤ 1}"

definition "acd x = ⨆{p. x ⋅ p = ⊥ ∧ p ≤ 1}"

lemma ado_acd: "ado (x∘) = acd x"
  unfolding ado_def acd_def
  by (metis convdqka.subid_conv invqka.inv_zero local.inv_contrav local.inv_invol)

lemma acd_ado: "acd (x∘) = ado x"
  unfolding ado_def acd_def
  by (metis acd_def ado_acd ado_def local.inv_invol)

lemma ado_left_zero [simp]: "ado x ⋅ x = ⊥"
  unfolding ado_def
  using dmq.coddual.Sup_distl by auto

lemma acd_right_zero [simp]: "x ⋅ acd x = ⊥"
  unfolding acd_def
  by (simp add: dmq.coddual.h_Sup local.dual_order.antisym)

lemma ado_greatest: "p ≤ 1 ⟹ p ⋅ x = ⊥ ⟹ p ≤ ado x"
  by (simp add: ado_def local.Sup_upper)

lemma acd_greatest: "p ≤ 1 ⟹ x ⋅ p = ⊥ ⟹ p ≤ acd x"
  by (simp add: acd_def local.Sup_upper)

lemma ado_subid: "ado x ≤ 1"
  using ado_def local.Sup_le_iff by force

lemma acd_subid: "acd x ≤ 1"
  by (simp add: acd_def local.Sup_le_iff)

lemma ado_left_zero_iff: "p ≤ 1 ⟹ (p ≤ ado x) = (p ⋅ x = ⊥)"
  by (metis ado_greatest ado_left_zero local.bot_unique local.mult_isor)

lemma acd_right_zero_iff: "p ≤ 1 ⟹ (p ≤ acd x) = (x ⋅ p = ⊥)"
  by (metis acd_greatest acd_right_zero local.bot_unique local.mult_isol)

text ‹This gives an eqational characterisation of antidomain and anticodomain.›

lemma ado_cd_bot: "ado x = cd (⊥ ← x)"
proof-
  {fix p
  assume  h: "p ≤ 1"
  hence "(p ≤ ado x) = (p ⋅ x = ⊥)"
    by (simp add: ado_left_zero_iff)
  also have "… = (p ≤ ⊥ ← x)"
    using local.bot_unique local.fres_galois by blast
  also have "… = (p ≤ 1 ⊓ (⊥ ← x))"
    by (simp add: h)
  also have "… = (p ≤ cd (⊥ ← x))"
    by (metis cd_fres_prop local.bot_least local.mult_botr)
  finally have "(p ≤ ado x) = (p ≤ cd (⊥ ← x))".}
  hence "∀y. y ≤ ado x ⟷ y ≤ cd (⊥ ← x)"
    using ado_subid local.cd_subid local.dual_order.trans by blast
  thus ?thesis
    using local.dual_order.antisym by blast
qed

lemma acd_do_bot: "acd x = do (x → ⊥)"
  by (metis ado_acd ado_cd_bot invqka.inv_zero local.bres_fres_conv local.cd_inv local.inv_invol)

lemma ado_cd_bot_id: "ado x = 1 ⊓ (⊥ ← x)"
  by (metis ado_cd_bot cd_fres_prop local.cd_bot local.cd_subid local.mult_botr)

lemma acd_do_bot_id: "acd x = 1 ⊓ (x → ⊥)"
  by (metis acd_do_bot do_bres_prop local.bot_least local.mult_botl)

lemma ado_cd_bot_var: "ado x = cd (⊥ ← do x)"
  by (metis ado_cd_bot do_top2 local.fres_bot_top local.fres_curry)

lemma acd_do_bot_var: "acd x = do (cd x → ⊥)"
  by (metis acd_do_bot cd_top2 local.bres_curry local.bres_top_bot)

lemma ado_do_bot: "ado x = do (do x → ⊥)"
  using acd_ado acd_do_bot_var local.cd_inv by auto

lemma "do x = ado (ado x)" (* nitpick[expect=genuine]*)
  oops

lemma acd_cd_bot: "acd x = cd (⊥ ← cd x)"
  by (metis ado_acd ado_cd_bot_var local.cd_inv local.inv_invol)

lemma ado_do_bot_var: "ado x = 1 ⊓ (do x → ⊥)"
  by (metis ado_do_bot do_bres_prop local.bot_unique local.bres_bot_bot local.bres_canc1 local.do_bot local.do_subid)

 lemma acd_cd_bot_var: "acd x = 1 ⊓ (⊥ ← cd x)"
   by (metis acd_cd_bot acd_right_zero cd_top local.fres_top_top2)


text ‹Domain and codomain are compatible with the boxes.›

lemma cd_box_ado: "cd_box x ⊥ = ado x"
  by (simp add: ado_cd_bot fres_cd_box)

lemma do_box_acd: "do_box x ⊥ = acd x"
  by (simp add: acd_do_bot bres_do_box)

lemma ado_subid_prop: "p ≤ 1 ⟹ ado p = 1 ⊓ (p → ⊥)"
  by (metis ado_do_bot_var do_fix_subid)

lemma ado_do: "p ≤ 1 ⟹ ado p = do (p → ⊥)"
  using ado_do_bot do_fix_subid by force

lemma ado_do_compl: "ado x ⋅ do x = ⊥"
  using dmq.dqmsr.dom_weakly_local by force

lemma "ado x ⊔ do x = ⊤" (* nitpick[expect = genuine]*)
  oops

lemma "∀x p. ∃f. 1 ⊓ (⊤ ⋅ p ← x) = 1 ⊓ (⊥ ← (x → p ⋅ ⊤))" (* nitpick[expect=genuine]*)
  oops

lemma "cd_box x p = ado (x ⋅ ado p)" (* nitpick[expect=genuine]*)
  oops

lemma ad_do_bot [simp]: "(1 ⊓ (do x → ⊥)) ⋅ do x = ⊥"
  using ado_do_bot_var ado_left_zero dmq.dqmsr.dom_weakly_local by presburger

lemma do_heyting_galois: "(do x ⋅ do y ≤ do z) = (do x ≤ 1 ⊓ (do y → do z))"
  by (metis dmq.dqmsr.dsg4 dmq.mqdual.cod_subid local.bres_galois local.le_inf_iff)

lemma do_heyting_galois_var: "(do x ⋅ do y ≤ do z) = (do x ≤ cd_box (do y) (do z))"
  by (metis cd_dia_cd_box_galois cd_fix_subid dmq.coddual.dqmsr.fd_def dmq.dqmsr.dom_mult_closed local.do_subid)

text ‹Antidomain is therefore Heyting negation.›

lemma ado_heyting_negation: "ado (do x) = cd_box (do x) ⊥"
  by (simp add: cd_box_ado)

lemma ad_ax1 [simp]: "(1 ⊓ (do x → ⊥)) ⋅ x = ⊥"
  by (simp add: local.dmq.dqmsr.dom_weakly_local)

lemma "1 ⊓ (do (1 ⊓ (do x → ⊥)) → ⊥) = do x" (* nitpick[expect=genuine]*)
  oops

lemma "p ≤ 1 ⟹ do_dia x p = 1 ⊓ (cd_box x (1 ⊓ (p → ⊥)) → ⊥)" (* nitpick[expect=genuine]*)
  oops

lemma  "p ≤ 1 ⟹ cd_box x p = 1 ⊓ (do_dia x (1 ⊓ (p → ⊥)) → ⊥)" (* nitpick[expect=genuine]*)
  oops

lemma "p ≤ 1 ⟹ cd_dia x p = 1 ⊓ (do_box x (1 ⊓ (p → ⊥)) → ⊥)" (* nitpick[expect=genuine]*)
  oops

lemma "p ≤ 1 ⟹ do_box x p = 1 ⊓ (cd_dia x (1 ⊓ (p → ⊥)) → ⊥)" (* nitpick[expect=genuine]*)
  oops

end

subsection ‹Boolean Dedekind quantales›

class distributive_dedekind_quantale = distrib_unital_quantale + dedekind_quantale

class boolean_dedekind_quantale = bool_unital_quantale + distributive_dedekind_quantale

begin

lemma ad_do_bot [simp]: "(1 - do x) ⋅ do x = ⊥"
  by (simp add: local.diff_eq local.inf_shunt local.subid_mult_meet)

lemma ad_ax1 [simp]: "(1 - do x) ⋅ x = ⊥"
  by (simp add: local.dmq.dqmsr.dom_weakly_local)

lemma ad_do [simp]: "1 - do (1 - do x) = do x"
proof-
  have "1 - do (1 - do x) = 1 - (1 - do x)"
    by (metis local.diff_eq local.do_fix_subid local.inf.cobounded1)
  also have "… = 1 ⊓ -(1 ⊓ - do x)"
    by (simp add: local.diff_eq)
  also have "… = do x"
    by (simp add: local.chaq.wswq.distrib_left local.do_top)
  finally show ?thesis.
qed

lemma ad_ax2: "1 - do (x ⋅ y) ⊔ (1 - do (x ⋅ (1 - do (1 - do y)))) = 1 - do (x ⋅ (1 - do (1 - do y)))"
  by simp

lemma ad_ax3 [simp]: "do x ⊔ (1 - do x) = 1"
proof-
  have "do x ⊔ (1 - do x) = do x ⊔ (1 ⊓ -do x)"
    using local.diff_eq by force
  also have "… = 1 ⊓ (do x ⊔ -do x)"
    by (simp add: local.chaq.wswq.distrib_left local.do_top)
  also have "… = 1"
    by simp
  finally show ?thesis.
qed

sublocale bdad: antidomain_semiring "λx. 1 - do x" "(⊔)" "(⋅)" 1 ⊥ _ _
  by unfold_locales simp_all

sublocale bdadka: antidomain_kleene_algebra "λx. 1 - do x" "(⊔)" "(⋅)" 1 ⊥ _ _ qstar..

sublocale bdar: antirange_semiring "(⊔)" "(⋅)" 1 ⊥ "λx. 1 - cd x" _ _
  apply unfold_locales
    apply (metis ad_ax1 ad_do dmq.mqs.local_var local.docd_compat)
   apply (metis ad_do local.cddo_compat local.dmq.coddual.dqmsr.dsr2 local.docd_compat local.sup.idem)
  by (metis bdad.a_subid' bdad.as3 local.convdqka.subid_conv local.do_inv)

sublocale bdaka: antirange_kleene_algebra "(⊔)" "(⋅)" 1 ⊥ _ _ qstar "λx. 1 - cd x"..

sublocale bmod: modal_semiring_simp "λx. 1 - do x" "(⊔)" "(⋅)" 1 ⊥ _ _ "λx. 1 - cd x"..

sublocale bmod: modal_kleene_algebra_simp "(⊔)" "(⋅)" 1 ⊥ _ _ qstar "λx. 1 - do x" "λx. 1 - cd x"..

lemma inv_neg: "(-x)∘ = -(x∘)"
  by (metis local.diff_eq local.diff_shunt_var local.dual_order.eq_iff local.inf.commute local.inv_conjugate local.inv_galois)

lemma residuation: "x∘ ⋅ -(x ⋅ y) ≤ -y"
  by (metis local.inf.commute local.inf_compl_bot local.inf_shunt local.schroeder_1)

lemma bres_prop: "x → y = -(x∘ ⋅ -y)"
  by (metis local.ba_dual.dual_iff local.bres_canc1 local.bres_galois_imp local.compl_le_swap1 local.dmq.coddual.h_w1 local.dual_order.antisym local.inv_invol residuation)

lemma fres_prop: "x ← y = -(-x ⋅ y∘)"
  using bres_prop inv_neg local.fres_bres_conv by auto

lemma do_dia_fdia: "do_dia x p = bdad.fdia x p"
  by (simp add: local.bdad.fdia_def local.dmq.dqmsr.fd_def)

lemma cd_dia_bdia: "cd_dia x p = bdar.bdia x p"
  by (metis ad_do bdar.ardual.a_subid' bdar.bdia_def local.cd_fix_subid local.dmq.coddual.dqmsr.fd_def local.docd_compat)

lemma do_dia_fbox_de_morgan: "p ≤ 1 ⟹ do_dia x p = 1 - bdad.fbox x (1 - p)"
  by (smt (verit, ccfv_SIG) ad_do bdad.a_closure bdad.am_d_def bdad.fbox_def local.dmq.dqmsr.fd_def local.do_fix_subid)

lemma fbox_do_dia_de_morgan: "p ≤ 1 ⟹ bdad.fbox x p = 1 - do_dia x (1 - p)"
  using bdad.fbox_def local.dmq.dqmsr.fd_def local.do_fix_subid by force

lemma cd_dia_bbox_de_morgan: "p ≤ 1 ⟹ cd_dia x p = 1 - bdar.bbox x (1 - p)"
  by (smt (verit, best) ad_do bdar.bbox_def bdar.bdia_def cd_dia_bdia local.cd_fix_subid local.do_subid local.docd_compat)

lemma bbox_cd_dia_de_morgan: "p ≤ 1 ⟹ bdar.bbox x p = 1 - cd_dia x (1 - p)"
  using bdar.bbox_def local.cd_fix_subid local.dmq.coddual.dqmsr.fd_def by force

lemma do_box_bbox: "p ≤ 1 ⟹ do_box x p = bdar.bbox x p"
proof-
  assume a: "p ≤ 1"
  {fix q
  assume b: "q ≤ 1"
  hence "(q ≤ do_box x p) = (x ⋅ q ≤ p ⋅ x)"
    by (simp add: a local.do_box_demod_subid)
  also have "… = (x ⋅ cd q ≤ cd p ⋅ x)"
    by (metis a b local.cd_fix_subid)
  also have "… = (cd q ≤ bdar.bbox x p)"
   by (metis bdar.bbox_def bdar.bdia_def cd_dia_bdia local.bdar.ardual.a_closure' local.bdar.ardual.ans_d_def local.bdar.ardual.dnsz.dsg1 local.bdar.ardual.fbox_demodalisation3 local.bdar.ardual.fbox_one local.dmq.coddual.dqmsr.fd_def local.nsrnqo.mult_oner)
  also have "… = (q ≤ bdar.bbox x p)"
    using b local.cd_fix_subid by force
  finally have "(q ≤ do_box x p) = (q ≤ bdar.bbox x p)".}
  thus ?thesis
    by (metis bdar.bbox_def local.bdar.ardual.a_subid' local.do_box_subid local.dual_order.antisym local.eq_refl)
qed

lemma cd_box_fbox: "p ≤ 1 ⟹ cd_box x p = bdad.fbox x p"
  by (smt (verit, ccfv_SIG) bdar.bbox_def do_box_bbox local.bdad.fbox_def local.cd_dia_do_dia_conv local.cd_inv local.cd_fix_subid local.cd_top local.diff_eq local.dmq.bb_def local.dmq.coddual.dqmsr.fd_def local.dmq.coddual.mult_assoc local.dmq.dqmsr.fd_def local.dmq.fb_def local.do_box_cd_box_conv local.do_fix_subid local.do_top local.inf.cobounded1)

lemma do_dia_cd_box_de_morgan: "p ≤ 1 ⟹ do_dia x p = 1 - cd_box x (1 - p)"
  by (simp add: cd_box_fbox local.diff_eq local.do_dia_fbox_de_morgan)

lemma cd_box_do_dia_de_morgan: "p ≤ 1 ⟹ cd_box x p = 1 - do_dia x (1 - p)"
  by (simp add: cd_box_fbox local.fbox_do_dia_de_morgan)

lemma cd_dia_do_box_de_morgan: "p ≤ 1 ⟹ cd_dia x p = 1 - do_box x (1 - p)"
  by (simp add: do_box_bbox local.cd_dia_bbox_de_morgan local.diff_eq)

lemma do_box_cd_dia_de_morgan: "p ≤ 1 ⟹ do_box x p = 1 - cd_dia x (1 - p)"
  by (simp add: do_box_bbox local.bbox_cd_dia_de_morgan)

end

class dc_involutive_modal_quantale = dc_modal_quantale + involutive_quantale

begin

sublocale invmqmka: involutive_dr_modal_kleene_algebra "(⊔)" "(⋅)" 1 ⊥ "(≤)" "(<)" qstar invol dom cod..

lemma do_approx_dom: "do x ≤ dom x"
proof -
  have "do x = dom (do x) ⋅ do x"
    by simp
  also have "… ≤ dom (1 ⊓ (x ⋅ x∘))"
    by (simp add: local.do_def local.dqmsr.domain_subid)
  also have "… ≤ dom 1 ⊓ dom (x ⋅  x∘)"
    using local.dom_meet_sub by presburger
  also have "… ≤ dom (x ⋅ dom (x∘))"
    by simp
  also have "… ≤ dom x"
    by (simp add: local.dqmsr.domain_1'')
  finally show ?thesis.
qed

end

class dc_modal_quantale_converse = dc_involutive_modal_quantale + quantale_converse

sublocale dc_modal_quantale_converse ⊆ invmqmka: dr_modal_kleene_algebra_converse  "(⊔)" "(⋅)" 1 ⊥ "(≤)" "(<)" qstar invol dom cod..

class dc_modal_quantale_strong_converse = dc_involutive_modal_quantale +
  assumes weak_dom_def: "dom x ≤ x ⋅ x∘"
  and weak_cod_def: "cod x ≤ x∘ ⋅ x"

begin

sublocale invmqmka: dr_modal_kleene_algebra_strong_converse  "(⊔)" "(⋅)" 1 ⊥ "(≤)" "(<)" qstar invol dom cod
  by (unfold_locales, simp_all add: local.weak_dom_def local.weak_cod_def)

lemma dom_def: "dom x = 1 ⊓ (x ⋅ x∘)"
  using local.do_approx_dom local.do_def local.dual_order.eq_iff local.weak_dom_def by force

lemma cod_def: "cod x = 1 ⊓ (x∘ ⋅ x)"
  using local.dom_def local.invmqmka.d_conv_cod by auto

lemma do_dom: "do x = dom x"
  by (simp add: local.do_def local.dom_def)

lemma cd_cod: "cd x = cod x"
  by (simp add: local.cd_def local.cod_def)

end

class dc_modal_dedekind_quantale = dc_involutive_modal_quantale + dedekind_quantale

class cd_distributive_modal_dedekind_quantale = dc_modal_dedekind_quantale + distrib_unital_quantale

class dc_boolean_modal_dedekind_quantale = dc_modal_dedekind_quantale + bool_unital_quantale

begin

lemma subid_idem: "p ≤ 1 ⟹ p ⋅ p = p"
  by (simp add: local.subid_mult_meet)

lemma subid_comm: "p ≤ 1 ⟹ q ≤ 1 ⟹ p ⋅ q = q ⋅ p"
  using local.inf.commute local.subid_mult_meet by force

lemma subid_meet_comp: "p ≤ 1 ⟹ q ≤ 1 ⟹ p ⊓ q = p ⋅ q"
  by (simp add: local.subid_mult_meet)

lemma subid_dom: "p ≤ 1 ⟹ dom p = p"
proof-
  assume h: "p ≤ 1"
  have a: "p ⊔ (1 ⊓ -p) = 1"
    by (metis h local.inf_sup_absorb local.sup.commute local.sup.orderE local.sup_compl_top local.sup_inf_distrib1)
  have b: "(1 ⊓ -p) ⊓ p = ⊥"
    by (simp add: local.inf.commute)
  hence "dom p = (p ⊔ (1 ⊓ -p)) ⋅ dom p"
    by (simp add: a)
  also have "… = p ⋅ dom p ⊔ dom ((1 ⊓ -p) ⋅ dom p) ⋅ (1 ⊓ -p) ⋅ dom p"
    using local.dqmsr.dsg1 local.wswq.distrib_right mult_assoc by presburger
  also have "… ≤ p ⊔ dom ((1 ⊓ -p) ⋅ dom p)"
    by (metis b h local.dom_subid local.dom_zero local.inf.cobounded1 local.mqdual.cod_local local.mult_botr local.sup.mono subid_comm subid_meet_comp)
  also have "… = p ⊔ dom ((1 ⊓ -p) ⋅ p)"
    by simp
  also have "… = p ⊔ dom ⊥"
    using b h subid_meet_comp by fastforce
  also have "… = p"
    by simp
  finally have "dom p ≤ p".
  thus ?thesis
    using h local.dqmsr.domain_subid local.dual_order.antisym by presburger
qed

lemma do_prop: "(do x ≤ do y) = (x ≤ do y ⋅ ⊤)"
  by (simp add: local.lla)

lemma do_lla: "(do x ≤ do y) = (x ≤ do y ⋅ x)"
  by (simp add: local.lla_var)

lemma lla_subid: "p ≤ 1 ⟹ ((dom x ≤ p) = (x ≤ p ⋅ x))"
  by (metis local.dqmsr.dom_llp subid_dom)

lemma dom_do: "dom x = do x"
proof-
  have "x ≤ do x ⋅ x"
    by simp
  hence "dom x ≤ do x"
    using lla_subid local.do_subid local.dodo by presburger
  thus ?thesis
    by (simp add: local.antisym_conv local.do_approx_dom)
qed

end

end