diff --git a/thys/Quantales_Converse/Kleene_Algebra_Converse.thy b/thys/Quantales_Converse/Kleene_Algebra_Converse.thy
new file mode 100644
--- /dev/null
+++ b/thys/Quantales_Converse/Kleene_Algebra_Converse.thy
@@ -0,0 +1,159 @@
+(* 
+Title: Kleene algebra with converse
+Author: Cameron Calk, Georg Struth
+Maintainer: Georg Struth <g.struth at sheffield.ac.uk>
+*)
+
+section \<open>Kleene algebra with converse\<close>
+
+theory "Kleene_Algebra_Converse"
+  imports Kleene_Algebra.Kleene_Algebra
+
+begin
+
+text \<open>We start from involutive dioids and Kleene algebra and then add a so-called strong Gelfand property 
+to obtain an operation of converse that is closer to algebras of paths and relations.\<close>
+
+subsection \<open>Involutive Kleene algebra\<close>
+
+class invol_op = 
+  fixes invol :: "'a \<Rightarrow> 'a" ("_\<^sup>\<circ>" [101] 100)
+
+class involutive_dioid = dioid_one_zero + invol_op +
+  assumes inv_invol [simp]: "(x\<^sup>\<circ>)\<^sup>\<circ> = x"
+  and inv_contrav [simp]: "(x \<cdot> y)\<^sup>\<circ> = y\<^sup>\<circ> \<cdot> x\<^sup>\<circ>"
+  and inv_sup [simp]: "(x + y)\<^sup>\<circ> = x\<^sup>\<circ> + y\<^sup>\<circ>"
+
+begin
+
+lemma inv_zero [simp]: "0\<^sup>\<circ> = 0"
+proof-
+  have "0\<^sup>\<circ> = (0\<^sup>\<circ> \<cdot> 0)\<^sup>\<circ>"
+    by simp
+  also have "\<dots> = 0\<^sup>\<circ> \<cdot> (0\<^sup>\<circ>)\<^sup>\<circ>"
+    using local.inv_contrav by blast
+  also have "\<dots> =  0\<^sup>\<circ> \<cdot> 0"
+    by simp
+  also have "\<dots> = 0"
+    by simp
+  finally show ?thesis.
+qed
+
+lemma inv_one [simp]: "1\<^sup>\<circ> = 1"
+proof-
+  have "1\<^sup>\<circ> = 1\<^sup>\<circ> \<cdot> (1\<^sup>\<circ>)\<^sup>\<circ>"
+    by simp
+  also have "\<dots> = (1\<^sup>\<circ> \<cdot> 1)\<^sup>\<circ>"
+    using local.inv_contrav by presburger
+  also have "\<dots> = (1\<^sup>\<circ>)\<^sup>\<circ>"
+    by simp
+  also have "\<dots> = 1"
+    by simp
+  finally show ?thesis.
+qed
+
+lemma inv_iso: "x \<le> y \<Longrightarrow> x\<^sup>\<circ> \<le> y\<^sup>\<circ>"
+  by (metis local.inv_sup local.less_eq_def)
+
+lemma inv_adj: "(x\<^sup>\<circ> \<le> y) = (x \<le> y\<^sup>\<circ>)"
+  using inv_iso by fastforce
+
+end
+
+text \<open>Here is an equivalent axiomatisation from Doornbos, Backhouse and van der Woude's paper
+on a calculational approach to mathematical induction.\<close>
+
+class involutive_dioid_alt = dioid_one_zero +
+  fixes inv_alt :: "'a \<Rightarrow> 'a" 
+  assumes inv_alt: "(inv_alt x \<le> y) = (x \<le> inv_alt y)"
+  and inv_alt_contrav [simp]: "inv_alt (x \<cdot> y) = inv_alt y \<cdot> inv_alt x"
+
+begin 
+
+lemma inv_alt_invol [simp]: "inv_alt (inv_alt x) = x"
+proof-
+  have "inv_alt (inv_alt x) \<le> x"
+    by (simp add: inv_alt)
+  thus ?thesis
+    by (meson inv_alt order_antisym)
+qed
+
+lemma inv_alt_add: "inv_alt (x + y) = inv_alt x + inv_alt y"
+proof-
+  {fix z
+  have "(inv_alt (x + y) \<le> z) = (x + y \<le> inv_alt z)"
+    by (simp add: inv_alt)
+  also have "\<dots> = (x \<le> inv_alt z \<and> y \<le> inv_alt z)"
+    by simp
+  also have "\<dots> = (inv_alt x \<le> z \<and> inv_alt y \<le> z)"
+    by (simp add: inv_alt)
+  also have "\<dots> = (inv_alt x + inv_alt y \<le> z)"
+    by force
+  finally have "(inv_alt (x + y) \<le> z) = (inv_alt x + inv_alt y \<le> z)".}
+  thus ?thesis
+    using order_antisym by blast
+qed
+
+sublocale altinv: involutive_dioid _ _ _ _ _ _ inv_alt
+  by unfold_locales (simp_all add: inv_alt_add)
+
+end
+
+sublocale involutive_dioid \<subseteq> altinv: involutive_dioid_alt _ _ _ _ _ _ invol
+  by unfold_locales (simp_all add: local.inv_adj) 
+
+class involutive_kleene_algebra = involutive_dioid + kleene_algebra
+
+begin
+
+lemma inv_star: "(x\<^sup>\<star>)\<^sup>\<circ> = (x\<^sup>\<circ>)\<^sup>\<star>"
+proof (rule order.antisym)
+  have "((x\<^sup>\<circ>)\<^sup>\<star>)\<^sup>\<circ> = (1 + (x\<^sup>\<circ>)\<^sup>\<star> \<cdot> x\<^sup>\<circ>)\<^sup>\<circ>"
+    by simp
+  also have "\<dots> = 1 + (x\<^sup>\<circ>)\<^sup>\<circ> \<cdot> ((x\<^sup>\<circ>)\<^sup>\<star>)\<^sup>\<circ>"
+    using local.inv_contrav local.inv_one local.inv_sup by presburger
+  finally have "1 + x \<cdot> ((x\<^sup>\<circ>)\<^sup>\<star>)\<^sup>\<circ> \<le> ((x\<^sup>\<circ>)\<^sup>\<star>)\<^sup>\<circ>"
+    by simp
+  hence "x\<^sup>\<star> \<le> ((x\<^sup>\<circ>)\<^sup>\<star>)\<^sup>\<circ>"
+    using local.star_inductl by force
+  thus "(x\<^sup>\<star>)\<^sup>\<circ> \<le> (x\<^sup>\<circ>)\<^sup>\<star>" 
+    by (simp add: local.inv_adj)
+next
+  have "(x\<^sup>\<star>)\<^sup>\<circ> = (1 + x\<^sup>\<star> \<cdot> x)\<^sup>\<circ>"
+    by simp
+  also have "\<dots> = 1 + x\<^sup>\<circ> \<cdot> (x\<^sup>\<star>)\<^sup>\<circ>"
+    using local.inv_contrav local.inv_one local.inv_sup by presburger
+  finally have "1 + x\<^sup>\<circ> \<cdot> (x\<^sup>\<star>)\<^sup>\<circ> \<le> (x\<^sup>\<star>)\<^sup>\<circ>"
+    by simp
+  thus "(x\<^sup>\<circ>)\<^sup>\<star> \<le> (x\<^sup>\<star>)\<^sup>\<circ>"
+    using local.star_inductl by force
+qed
+
+end
+
+
+subsection \<open>Kleene algebra with converse\<close>
+
+text \<open>The name "strong Gelfand property" has been borrowed from Palmigiano and Re.\<close>
+
+class dioid_converse = involutive_dioid +
+  assumes strong_gelfand: "x \<le> x \<cdot> x\<^sup>\<circ> \<cdot> x"
+
+lemma (in dioid_converse) subid_conv: "x \<le> 1 \<Longrightarrow> x\<^sup>\<circ> = x"
+proof (rule order.antisym)
+  assume h: "x \<le> 1"
+  have "x \<le> x \<cdot> x\<^sup>\<circ> \<cdot> x"
+    by (simp add: local.strong_gelfand)
+  also have "\<dots> \<le> 1 \<cdot> x\<^sup>\<circ> \<cdot> 1"
+    using h local.mult_isol_var by blast
+  also have "\<dots> =  x\<^sup>\<circ>"
+    by simp
+  finally show "x \<le> x\<^sup>\<circ>"
+    by simp
+  thus "x\<^sup>\<circ> \<le> x"
+    by (simp add: local.inv_adj)
+qed
+
+class kleene_algebra_converse = involutive_kleene_algebra + dioid_converse
+
+end
diff --git a/thys/Quantales_Converse/Modal_Kleene_Algebra_Converse.thy b/thys/Quantales_Converse/Modal_Kleene_Algebra_Converse.thy
new file mode 100644
--- /dev/null
+++ b/thys/Quantales_Converse/Modal_Kleene_Algebra_Converse.thy
@@ -0,0 +1,131 @@
+(* 
+Title: Modal Kleene Algebra with converse
+Author: Cameron Calk, Georg Struth
+Maintainer: Georg Struth <g.struth at sheffield.ac.uk>
+*)
+
+section \<open>Modal Kleene algebra with converse\<close>
+
+theory "Modal_Kleene_Algebra_Converse"
+  imports Modal_Kleene_Algebra_Var Kleene_Algebra_Converse
+
+begin
+
+text \<open>Here we mainly study the interaction of converse with domain and codomain.\<close>
+
+subsection \<open>Involutive modal Kleene algebras\<close>
+
+class involutive_domain_semiring = domain_semiring + involutive_dioid
+
+begin
+
+notation domain_op ("dom")
+
+lemma strong_conv_conv: "dom x \<le> x \<cdot> x\<^sup>\<circ> \<Longrightarrow> x \<le> x \<cdot> x\<^sup>\<circ> \<cdot> x"
+proof-
+  assume h: "dom x \<le> x \<cdot> x\<^sup>\<circ>"
+  have "x = dom x \<cdot> x"
+    by simp
+  also have "\<dots> \<le>  x \<cdot> x\<^sup>\<circ> \<cdot> x"
+    using h local.mult_isor by presburger
+  finally show ?thesis.
+qed
+
+end
+
+class involutive_dr_modal_semiring  = dr_modal_semiring + involutive_dioid
+
+class involutive_dr_modal_kleene_algebra = involutive_dr_modal_semiring + kleene_algebra
+
+
+subsection \<open>Modal semirings algebras with converse\<close>
+
+class dr_modal_semiring_converse = dr_modal_semiring + dioid_converse
+
+begin
+
+lemma d_conv [simp]: "(dom x)\<^sup>\<circ> = dom x"
+proof-
+  have "dom x \<le> dom x \<cdot> (dom x)\<^sup>\<circ> \<cdot> dom x"
+    by (simp add: local.strong_gelfand)
+  also have  "\<dots> \<le> 1 \<cdot> (dom x)\<^sup>\<circ> \<cdot> 1"
+    by (simp add: local.subid_conv)
+  finally have a: "dom x \<le> (dom x)\<^sup>\<circ>"
+    by simp
+  hence "(dom x)\<^sup>\<circ> \<le> dom x"
+    by (simp add: local.inv_adj)
+  thus ?thesis
+    using a by auto
+qed
+
+lemma cod_conv: "(cod x)\<^sup>\<circ> = cod x"
+  by (metis d_conv local.dc_compat)
+
+lemma d_conv_cod [simp]: "dom (x\<^sup>\<circ>) = cod x"
+proof-
+  have "dom (x\<^sup>\<circ>) = dom ((x \<cdot> cod x)\<^sup>\<circ>)"
+    by simp
+  also have "\<dots> = dom ((cod x)\<^sup>\<circ> \<cdot> x\<^sup>\<circ>)"
+    using local.inv_contrav by presburger
+  also have "\<dots> = dom (cod x \<cdot> x\<^sup>\<circ>)"
+    by (simp add: cod_conv)
+  also have "\<dots> = dom (dom (cod x) \<cdot> x\<^sup>\<circ>)"
+    by simp
+  also have "\<dots> = dom (cod x) \<cdot> dom (x\<^sup>\<circ>)"
+    using local.dsg3 by blast
+  also have "\<dots> = cod x \<cdot> dom (x\<^sup>\<circ>)"
+    by simp
+  also have "\<dots> = cod x \<cdot> cod (dom (x\<^sup>\<circ>))"
+    by simp
+  also have "\<dots> = cod (x \<cdot> cod (dom (x\<^sup>\<circ>)))"
+    using local.rdual.dsg3 by presburger
+  also have "\<dots> = cod (x \<cdot> dom (x\<^sup>\<circ>))"
+    by simp
+  also have "\<dots> = cod ((x\<^sup>\<circ>)\<^sup>\<circ> \<cdot> (dom (x\<^sup>\<circ>))\<^sup>\<circ>)"
+    by simp
+  also have "\<dots> = cod ((dom (x\<^sup>\<circ>) \<cdot> x\<^sup>\<circ>)\<^sup>\<circ>)"
+    using local.inv_contrav by presburger
+  also have "\<dots> = cod ((x\<^sup>\<circ>)\<^sup>\<circ>)"
+    by simp
+  also have "\<dots> = cod x"
+    by simp
+  finally show ?thesis.
+qed
+
+lemma cod_conv_d: "cod (x\<^sup>\<circ>) = dom x"
+  by (metis d_conv_cod local.inv_invol)
+
+lemma "dom y = y \<Longrightarrow> fd (x\<^sup>\<circ>) y = bd x y"
+proof-
+  assume h: "dom y = y"
+  have "fd (x\<^sup>\<circ>) y = dom (x\<^sup>\<circ> \<cdot> dom y)"
+    by (simp add: local.fd_def)
+  also have "\<dots> = dom ((dom y \<cdot> x)\<^sup>\<circ>)"
+    by simp
+  also have "\<dots> = cod (dom y \<cdot> x)"
+    using d_conv_cod by blast
+  also have "\<dots> = bd x y"
+    by (simp add: h local.bd_def)
+  finally show ?thesis.
+qed
+
+lemma "dom y = y \<Longrightarrow> bd (x\<^sup>\<circ>) y = fd x y"
+  by (metis cod_conv_d d_conv local.bd_def local.fd_def local.inv_contrav)
+
+end
+
+
+subsection \<open>Modal Kleene algebras with converse\<close>
+
+class dr_modal_kleene_algebra_converse = dr_modal_semiring_converse + kleene_algebra
+
+class dr_modal_semiring_strong_converse = involutive_dr_modal_semiring + 
+  assumes weak_dom_def: "dom x \<le> x \<cdot> x\<^sup>\<circ>"
+  and weak_cod_def: "cod x \<le> x\<^sup>\<circ> \<cdot> x"
+
+subclass (in dr_modal_semiring_strong_converse) dr_modal_semiring_converse
+  by unfold_locales (metis local.ddual.mult_isol_var local.dsg1 local.eq_refl local.weak_dom_def)
+
+class dr_modal_kleene_algebra_strong_converse = dr_modal_semiring_strong_converse + kleene_algebra
+
+end
diff --git a/thys/Quantales_Converse/Modal_Kleene_Algebra_Var.thy b/thys/Quantales_Converse/Modal_Kleene_Algebra_Var.thy
new file mode 100644
--- /dev/null
+++ b/thys/Quantales_Converse/Modal_Kleene_Algebra_Var.thy
@@ -0,0 +1,51 @@
+(* 
+Title: Modal Kleene algebra based on domain and range semirings
+Author: Georg Struth
+Maintainer: Georg Struth <g.struth at sheffield.ac.uk>
+*)
+
+section \<open>Modal Kleene algebra based on domain and range semirings\<close>
+
+theory "Modal_Kleene_Algebra_Var"
+  imports KAD.Domain_Semiring KAD.Range_Semiring
+
+begin
+
+notation domain_op ("dom") 
+notation range_op ("cod") 
+
+subclass (in domain_semiring) dioid_one_zero..
+
+subclass (in range_semiring) dioid_one_zero
+  by unfold_locales simp
+
+subsection \<open>Modal semirings\<close>
+
+text \<open>The following modal semirings are based on domain and range semirings instead of antidomain and antirange semirings,
+as in the AFP entry for Kleene algebra with domain.\<close>
+
+class dr_modal_semiring = domain_semiring + range_semiring +
+  assumes dc_compat [simp]: "dom (cod x) = cod x" 
+  and cd_compat [simp]: "cod (dom x) = dom x" 
+
+begin 
+
+sublocale msrdual: dr_modal_semiring "(+)" "\<lambda>x y. y \<cdot> x" 1 0 cod "(\<le>)" "(<)" dom
+  by unfold_locales simp_all
+
+lemma d_cod_fix: "(dom x = x) = (x = cod x)"
+  by (metis local.cd_compat local.dc_compat)
+
+lemma local_var: "(x \<cdot> y = 0) = (cod x \<cdot> dom y = 0)"
+  using local.dom_weakly_local local.rdual.dom_weakly_local by force
+
+lemma fbdia_conjugation: "(fd x (dom p) \<cdot> dom q = 0) = (dom p \<cdot> bd x (dom q) = 0)"
+  by (metis local.bd_def local.cd_compat local.ddual.mult_assoc local.dom_weakly_local local.fd_def local.rdual.dom_weakly_local local.rdual.dsg4)
+
+end
+
+subsection \<open>Modal Kleene algebra\<close>
+
+class dr_modal_kleene_algebra = dr_modal_semiring + kleene_algebra
+
+end
diff --git a/thys/Quantales_Converse/Modal_Quantale.thy b/thys/Quantales_Converse/Modal_Quantale.thy
new file mode 100644
--- /dev/null
+++ b/thys/Quantales_Converse/Modal_Quantale.thy
@@ -0,0 +1,329 @@
+(* 
+Title: Modal quantales
+Author: Georg Struth
+Maintainer: Georg Struth <g.struth at sheffield.ac.uk>
+*)
+
+section \<open>Modal quantales\<close>
+
+theory Modal_Quantale
+  imports Quantales.Quantale_Star Modal_Kleene_Algebra_Var KAD.Modal_Kleene_Algebra
+
+begin
+
+subsection \<open>Simplified modal semirings and Kleene algebras\<close>
+
+text \<open>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.\<close>
+
+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 \<cdot> d (r x) = 0"
+    using local.ads_d_def local.ars_r_def local.dpdz.dom_weakly_local by auto
+  have "r x \<cdot> d (r x) \<cdot> ar x \<le> r x \<cdot> ar x"
+    by (simp add: local.a_subid_aux2 local.ads_d_def local.mult_isor)
+  hence b: "r x \<cdot> d (r x) \<cdot> 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) \<cdot> d (r x)"
+    using local.add_comm local.ardual.ans3 local.ars_r_def local.mult_1_left by presburger
+  also have "\<dots> = ar x \<cdot> d (r x) + r x \<cdot> d (r x)"
+    by simp
+  also have "\<dots> = r x \<cdot> d (r x)"
+    by (simp add: a)
+  also have "\<dots> = r x \<cdot> d (r x) \<cdot> (ar x + r x)"
+    using local.add_comm local.ardual.ans3 local.ars_r_def by auto
+  also have "\<dots> = r x \<cdot> d (r x) \<cdot> ar x + r x \<cdot> d (r x) \<cdot> r x"
+    by simp
+  also have "\<dots> = r x \<cdot> d (r x) \<cdot> r x"
+    using b by auto
+  also have "\<dots> = 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 \<open>Domain quantales\<close>
+
+class domain_quantale = unital_quantale + domain_op +
+  assumes dom_absorb: "x \<le> dom x \<cdot> x"
+  and dom_local: "dom (x \<cdot> dom y) = dom (x \<cdot> y)"
+  and dom_add: "dom (x \<squnion> y) = dom x \<squnion> dom y"
+  and dom_subid: "dom x \<le> 1"
+  and dom_zero [simp]: "dom \<bottom> = \<bottom>"
+
+text \<open>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.\<close>
+
+sublocale domain_quantale \<subseteq> dqmsr: domain_semiring "(\<squnion>)" "(\<cdot>)" 1 \<bottom> dom "(\<le>)" "(<)"
+  by unfold_locales (simp_all add: dom_add dom_local dom_absorb sup.absorb2 dom_subid)
+
+sublocale domain_quantale \<subseteq> dqmka: domain_kleene_algebra "(\<squnion>)" "(\<cdot>)" 1 \<bottom>  dom "(\<le>)" "(<)" 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 \<Rightarrow> 'a d_element \<Rightarrow> bool" is "(\<le>)" .
+
+lift_definition less_d_element :: "'a d_element \<Rightarrow> 'a d_element \<Rightarrow> bool" is "(<)" .
+
+lift_definition bot_d_element :: "'a d_element" is \<bottom>
+  by simp
+
+lift_definition top_d_element :: "'a d_element" is 1
+  by simp
+
+lift_definition inf_d_element :: "'a d_element \<Rightarrow> 'a d_element \<Rightarrow> 'a d_element" is "(\<cdot>)"
+  by (metis dqmsr.dom_mult_closed)
+
+lift_definition sup_d_element :: "'a d_element \<Rightarrow> 'a d_element \<Rightarrow> 'a d_element" is "(\<squnion>)"
+  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 \<top> = 1"
+proof-
+  have "1 \<le> \<top>"
+    by simp
+  hence "dom 1 \<le> dom \<top>"
+    using local.dqmsr.d_iso by blast
+  thus ?thesis
+    by (simp add: local.dual_order.antisym)
+qed
+
+lemma dom_top2: "x \<cdot> \<top> \<le> dom x \<cdot> \<top>"
+proof-
+  have "x \<cdot> \<top> = dom x \<cdot> x \<cdot> \<top>"
+    by simp
+  also have "\<dots> \<le> dom x \<cdot> \<top> \<cdot> \<top>"
+    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 \<cdot> dom y \<le> dom (x \<cdot> y) \<cdot> x"
+  using local.dqmsr.fd_def local.dqmsr.fdemodalisation2 local.eq_refl by blast
+
+lemma dom_meet: "dom x \<cdot> dom y = dom x \<sqinter> 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 \<sqinter> dom y) = dom x \<sqinter> dom y"
+  using dom_meet local.dqmsr.dom_mult_closed by presburger
+
+lemma dom_meet_distl: "dom x \<cdot> (y \<sqinter> z) = (dom x \<cdot> y) \<sqinter> (dom x \<cdot> z)"
+proof-
+  have a: "dom x \<cdot> (y \<sqinter> z) \<le> (dom x \<cdot> y) \<sqinter> (dom x \<cdot> z)"
+    using local.mult_isol by force
+  have "(dom x \<cdot> y) \<sqinter> (dom x \<cdot> z) = dom ((dom x \<cdot> y) \<sqinter> (dom x \<cdot> z)) \<cdot> ((dom x \<cdot> y) \<sqinter> (dom x \<cdot> z))"
+    by simp
+  also have "\<dots> \<le> dom ((dom x \<cdot> y)) \<cdot> ((dom x \<cdot> y) \<sqinter> (dom x \<cdot> z))"
+    using calculation local.dqmsr.dom_iso local.dqmsr.dom_llp2 local.inf.cobounded1 by presburger
+  also have "\<dots> \<le> dom x \<cdot> ((dom x \<cdot> y) \<sqinter> (dom x \<cdot> z))"
+    by (metis local.dqmsr.domain_1'' local.dqmsr.domain_invol local.mult_isor)
+  also have "\<dots> \<le> dom x \<cdot> (y \<sqinter> 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 \<cdot> y) \<sqinter> (dom x \<cdot> z)) \<le> dom x"
+  by (metis dom_meet_distl local.dqmsr.domain_1'' local.dqmsr.domain_invol)
+
+lemma dom_inf_pres_aux: "Y \<noteq> {} \<Longrightarrow> dom (\<Sqinter>y \<in> Y. dom x \<cdot> y) \<le> dom x"
+proof-
+  assume "Y \<noteq> {}"
+  have "\<forall>z\<in>Y. dom (\<Sqinter>y \<in> Y. dom x \<cdot> y) \<le> dom (dom x \<cdot> z)"
+    by (meson local.INF_lower local.dqmsr.dom_iso)
+  hence "\<forall>z\<in>Y. dom (\<Sqinter>y \<in> Y. dom x \<cdot> y) \<le> dom x \<cdot> dom z"
+    by fastforce
+  hence "\<forall>z\<in>Y. dom (\<Sqinter>y \<in> Y. dom x \<cdot> y) \<le> dom x"
+    using dom_meet by fastforce
+  thus "dom (\<Sqinter>y \<in> Y. dom x \<cdot> y) \<le> dom x"
+    using \<open>Y \<noteq> {}\<close> by blast
+qed
+
+lemma dom_inf_pres_aux2: "(\<Sqinter>y \<in> Y. dom x \<cdot> y) \<le> \<Sqinter>Y"
+  by (simp add: local.INF_lower2 local.dqmsr.dom_subid_aux2 local.le_Inf_iff)
+
+lemma dom_inf_pres: "Y \<noteq> {} \<Longrightarrow> dom x \<cdot> (\<Sqinter>Y) = (\<Sqinter>y \<in> Y. dom x \<cdot> y)"
+proof-
+  assume hyp: "Y \<noteq> {}"
+  have a: "dom x \<cdot> (\<Sqinter>Y) \<le> (\<Sqinter>y \<in> Y. dom x \<cdot> y)"
+    by (simp add: Setcompr_eq_image local.Inf_subdistl)
+  have "(\<Sqinter>y \<in> Y. dom x \<cdot> y) = dom (\<Sqinter>y \<in> Y. dom x \<cdot> y) \<cdot> (\<Sqinter>y \<in> Y. dom x \<cdot> y)"
+    by simp
+  also have "\<dots> \<le> dom x \<cdot> (\<Sqinter>y \<in> Y. dom x \<cdot> y)"
+    using dom_inf_pres_aux hyp local.mult_isor by blast
+  also have "\<dots> \<le> dom x \<cdot> \<Sqinter>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 (\<Sqinter>X) \<le> \<Sqinter> (dom ` X)"
+  by (simp add: local.INF_greatest local.Inf_lower local.dqmsr.dom_iso)
+
+text \<open>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.\<close>
+
+lemma dom_top_pres: "(x \<le> dom y \<cdot> x) = (x \<le> dom y \<cdot> \<top>)"
+  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 \<le> dom y) = (x \<le> dom y \<cdot> \<top>)"
+  using dom_top_pres local.dqmsr.dom_llp by force
+
+lemma "dom (1 \<sqinter> x) = 1 \<sqinter> x \<Longrightarrow> x \<le> 1 \<Longrightarrow> dom x = x"
+  using local.inf_absorb2 by force
+
+lemma dom_meet_sub: "dom (x \<sqinter> y) \<le> dom x \<sqinter> dom y"
+  by (simp add: local.dqmsr.d_iso)
+
+lemma dom_dist1: "dom x \<squnion> (dom y \<sqinter> dom z) = (dom x \<squnion> dom y) \<sqinter> (dom x \<squnion> dom z)"
+  by (metis dom_meet local.dom_add local.dqmsr.dom_distrib)
+
+lemma dom_dist2: "dom x \<sqinter> (dom y \<squnion> dom z) = (dom x \<sqinter> dom y) \<squnion> (dom x \<sqinter> dom z)"
+  by (metis dom_meet local.dom_add local.sup_distl)
+
+abbreviation "fd' \<equiv> dqmsr.fd"
+
+definition "bb x y = \<Squnion>{dom z |z. fd' x z \<le> dom y}"
+
+lemma fd'_bb_galois_aux: "fd' x (dom p) \<le> dom q \<Longrightarrow> dom p \<le> bb x (dom q)"
+  by (simp add: bb_def local.SUP_upper setcompr_eq_image)
+
+lemma dom_iso_var: "(\<Squnion>x \<in> X. dom x) \<le> dom (\<Squnion>x \<in> X. dom x)"
+  by (meson local.SUP_le_iff local.dom_subid local.dqmsr.domain_subid)
+
+lemma dom_iso_var2: "(\<Squnion>x \<in> X. dom x) \<le> dom (\<Squnion>x \<in> X. x)"
+  by (simp add: local.SUP_le_iff local.Sup_upper local.dqmsr.dom_iso)
+
+end
+
+
+subsection \<open>Codomain quantales\<close>
+
+class codomain_quantale = unital_quantale + range_op +
+  assumes cod_absorb: "x \<le> x \<cdot> cod x" 
+  and cod_local: "cod (cod x \<cdot> y) = cod (x \<cdot> y)"
+  and cod_add: "cod (x \<squnion> y) = cod x \<squnion> cod y"
+  and cod_subid: "cod x \<le> 1"
+  and cod_zero: "cod \<bottom> = \<bottom>"
+
+sublocale codomain_quantale \<subseteq> coddual: domain_quantale range_op _ "\<lambda>x y. y \<cdot> 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' \<equiv> coddual.fd'"
+
+definition (in codomain_quantale) "fb x y = \<Squnion>{cod z |z. bd' x z \<le> cod y}"
+
+lemma (in codomain_quantale) bd'_fb_galois_aux: "bd' x (cod p) \<le> cod q \<Longrightarrow> cod p \<le> fb x (cod q)"
+  using local.coddual.bb_def local.coddual.fd'_bb_galois_aux local.fb_def by auto
+
+
+subsection \<open>Modal quantales\<close>
+
+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 \<subseteq> mqs: dr_modal_kleene_algebra "(\<squnion>)" "(\<cdot>)" 1 \<bottom> "(\<le>)" "(<)" qstar dom cod
+  by unfold_locales simp_all
+
+sublocale dc_modal_quantale \<subseteq> mqdual: dc_modal_quantale _ "\<lambda>x y. y \<cdot> x" _ _ _ _ _ _ _ _  dom cod
+  by unfold_locales simp_all
+
+lemma (in dc_modal_quantale) "x \<cdot> \<top> = dom x \<cdot> \<top>"
+(*  nitpick[expect=genuine] *)
+  oops 
+
+lemma (in dc_modal_quantale) "\<top> \<cdot> x = \<top> \<cdot> cod x"
+(*  nitpick[expect=genuine] *)
+  oops 
+
+
+subsection \<open>Antidomain and anticodomain quantales\<close>
+
+notation antidomain_op ("adom") 
+
+class antidomain_quantale = unital_quantale + antidomain_op +
+  assumes as1 [simp]: "adom x \<cdot> x = \<bottom>"
+  and as2 [simp]: "adom (x \<cdot> y) \<le> adom (x \<cdot> adom (adom y))"
+  and as3 [simp]: "adom (adom x) \<squnion> adom x = 1"
+
+definition (in antidomain_quantale) "ddom = adom \<circ> adom"
+
+sublocale antidomain_quantale \<subseteq> adqmsr: antidomain_semiring adom "(\<squnion>)" "(\<cdot>)" 1 \<bottom> "(\<le>)" "(<)"
+  by unfold_locales (simp_all add: local.sup.absorb2)
+
+sublocale antidomain_quantale \<subseteq> adqmka: antidomain_kleene_algebra adom "(\<squnion>)" "(\<cdot>)" 1 \<bottom> "(\<le>)" "(<)" qstar..
+
+sublocale antidomain_quantale \<subseteq> 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 \<cdot> acod x = \<bottom>"
+  and ars2 [simp]: "acod (x \<cdot> y) \<le> acod (acod (acod x) \<cdot> y)"
+  and ars3 [simp]: "acod (acod x) \<squnion> acod x = 1"
+
+sublocale anticodomain_quantale \<subseteq> acoddual: antidomain_quantale acod _ "\<lambda>x y. y \<cdot> x" _ _ _ _ _ _ _ _
+  by unfold_locales (auto simp: mult_assoc Sup_distl Sup_distr)
+
+definition (in anticodomain_quantale) "ccod = acod \<circ> acod"
+
+sublocale anticodomain_quantale \<subseteq> acdqmsr: antirange_semiring "(\<squnion>)" "(\<cdot>)" 1 \<bottom> acod "(\<le>)" "(<)"..
+
+sublocale anticodomain_quantale \<subseteq> acdqmka: antirange_kleene_algebra "(\<squnion>)" "(\<cdot>)" 1 \<bottom> "(\<le>)" "(<)" qstar acod..
+
+sublocale anticodomain_quantale \<subseteq> acddq: codomain_quantale _ _ _ _ _ _ _ _ _ _ "\<lambda> 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 \<subseteq> mmqs: modal_kleene_algebra_simp "(\<squnion>)" "(\<cdot>)" 1 \<bottom> "(\<le>)" "(<)" qstar adom acod..
+
+sublocale modal_quantale \<subseteq> mmqdual: modal_quantale _ "\<lambda>x y. y \<cdot> x" _ _ _ _ _ _ _ _ adom acod
+  by unfold_locales simp_all
+
+end
+
+
+
diff --git a/thys/Quantales_Converse/Quantale_Converse.thy b/thys/Quantales_Converse/Quantale_Converse.thy
new file mode 100644
--- /dev/null
+++ b/thys/Quantales_Converse/Quantale_Converse.thy
@@ -0,0 +1,1583 @@
+(* 
+Title: Quantales with converse
+Author: Cameron Calk, Georg Struth
+Maintainer: Georg Struth <g.struth at sheffield.ac.uk>
+*)
+
+section \<open>Quantales with converse\<close>
+
+theory Quantale_Converse
+  imports Modal_Quantale Modal_Kleene_Algebra_Converse 
+
+begin
+
+subsection \<open>Properties of unital quantales\<close>
+
+text \<open>These properties should eventually added to the quantales AFP entry.\<close>
+
+lemma (in quantale) bres_bot_top [simp]: "\<bottom> \<rightarrow> \<top> = \<top>"
+  by (simp add: local.bres_galois_imp local.order.antisym)
+
+lemma (in quantale) fres_top_bot [simp]: "\<top> \<leftarrow> \<bottom> = \<top>"
+  by (meson local.fres_galois local.order_antisym local.top_greatest)
+
+lemma (in unital_quantale) bres_top_top2 [simp]: "(x \<rightarrow> y \<cdot> \<top>) \<cdot> \<top> = x \<rightarrow> y \<cdot> \<top>"
+proof-
+  have "(x \<rightarrow> y \<cdot> \<top>) \<cdot> \<top> \<le> x \<rightarrow> y \<cdot> \<top> \<cdot> \<top>"
+    by (simp add: local.bres_interchange)
+  hence "(x \<rightarrow> y \<cdot> \<top>) \<cdot> \<top> \<le> x \<rightarrow> y \<cdot> \<top>"
+    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]: "\<top> \<cdot> (\<top> \<cdot> y \<leftarrow> x) =  \<top> \<cdot> y \<leftarrow> 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]: "\<top> \<rightarrow> \<bottom> = \<bottom>"
+  by (metis local.bot_least local.bres_canc1 local.le_top local.order.antisym)
+
+lemma (in unital_quantale) fres_bot_top [simp]: "\<bottom> \<leftarrow> \<top> = \<bottom>"
+  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 \<cdot> \<top> = \<bottom>) = (x = \<bottom>)"
+  by (metis local.fres_bot_top local.fres_canc2 local.le_bot local.mult_botl)
+
+
+subsection \<open>Involutive quantales\<close>
+
+text \<open>The following axioms for involutive quantales are standard.\<close>
+
+class involutive_quantale = unital_quantale + invol_op +
+  assumes inv_invol [simp]: "(x\<^sup>\<circ>)\<^sup>\<circ> = x"
+  and inv_contrav: "(x \<cdot> y)\<^sup>\<circ> = y\<^sup>\<circ> \<cdot> x\<^sup>\<circ>"
+  and inv_sup [simp]: "(\<Squnion>X)\<^sup>\<circ> = (\<Squnion>x \<in> X. x\<^sup>\<circ>)"
+
+context involutive_quantale
+begin
+
+lemma inv_binsup [simp]: "(x \<squnion> y)\<^sup>\<circ> = x\<^sup>\<circ> \<squnion> y\<^sup>\<circ>"
+proof-
+  have "(x \<squnion> y)\<^sup>\<circ> = (\<Squnion>z \<in> {x,y}. z\<^sup>\<circ>)"
+    using local.inv_sup local.sup_Sup by presburger
+  also have "\<dots> = (\<Squnion>z \<in> {x\<^sup>\<circ>,y\<^sup>\<circ>}. z)"
+    by simp
+  also have "\<dots> = x\<^sup>\<circ> \<squnion> y\<^sup>\<circ>"
+    by fastforce
+  finally show ?thesis.
+qed
+
+lemma inv_iso: "x \<le> y \<Longrightarrow> x\<^sup>\<circ> \<le> y\<^sup>\<circ>"
+  by (metis inv_binsup local.sup.absorb_iff1)
+
+lemma inv_galois: "(x\<^sup>\<circ> \<le> y) = (x \<le> y\<^sup>\<circ>)"
+  using local.inv_iso by fastforce
+
+lemma bres_fres_conv: "(y\<^sup>\<circ> \<leftarrow> x\<^sup>\<circ>)\<^sup>\<circ> = x \<rightarrow> y"
+proof-
+  have "(y\<^sup>\<circ> \<leftarrow> x\<^sup>\<circ>)\<^sup>\<circ> = (\<Squnion>{z. z \<cdot> x\<^sup>\<circ> \<le> y\<^sup>\<circ>})\<^sup>\<circ>"
+    by (simp add: local.fres_def)
+  also have "\<dots> = \<Squnion>{z\<^sup>\<circ> |z. z \<cdot> x\<^sup>\<circ> \<le> y\<^sup>\<circ>}"
+    by (simp add: image_Collect)
+  also have "\<dots> = \<Squnion>{z. z\<^sup>\<circ> \<cdot> x\<^sup>\<circ> \<le> y\<^sup>\<circ>}"
+    by (metis local.inv_invol)
+  also have "\<dots> = \<Squnion>{z. (x \<cdot> z)\<^sup>\<circ> \<le> y\<^sup>\<circ>}"
+    by (simp add: local.inv_contrav)
+  also have "\<dots> = \<Squnion>{z. x \<cdot> z \<le> y}"
+    by (metis local.inv_invol local.inv_iso)
+  also have "\<dots> = x \<rightarrow> y"
+    by (simp add: local.bres_def)
+  finally show ?thesis.
+qed
+
+lemma fres_bres_conv: "(y\<^sup>\<circ> \<rightarrow> x\<^sup>\<circ>)\<^sup>\<circ> = x \<leftarrow> y"
+  by (metis bres_fres_conv local.inv_invol)
+
+sublocale invqka: involutive_kleene_algebra "(\<squnion>)" "(\<cdot>)" 1 \<bottom> "(\<le>)" "(<)" qstar invol
+  by unfold_locales (simp_all add: local.inv_contrav)
+
+lemma inv_binf [simp]: "(x \<sqinter> y)\<^sup>\<circ> = x\<^sup>\<circ> \<sqinter> y\<^sup>\<circ>"
+proof-
+  {fix z
+  have "(z \<le> (x \<sqinter> y)\<^sup>\<circ>) = (z\<^sup>\<circ> \<le> x \<sqinter> y)"
+    using invqka.inv_adj by blast
+  also have "\<dots> = (z\<^sup>\<circ> \<le> x \<and> z\<^sup>\<circ> \<le> y)"
+    by simp
+  also have "\<dots> = (z \<le> x\<^sup>\<circ> \<and> z \<le> y\<^sup>\<circ>)"
+    by (simp add: invqka.inv_adj)
+  also have "\<dots> = (z \<le> x\<^sup>\<circ> \<sqinter> y\<^sup>\<circ>)"
+    by simp
+  finally have "(z \<le> (x \<sqinter> y)\<^sup>\<circ>) = (z \<le> x\<^sup>\<circ> \<sqinter> y\<^sup>\<circ>)".}
+  thus ?thesis
+    using local.dual_order.antisym by blast
+qed
+
+lemma inv_inf [simp]: "(\<Sqinter>X)\<^sup>\<circ> = (\<Sqinter>x \<in> X. x\<^sup>\<circ>)"
+  by (metis invqka.inv_adj local.INF_eqI local.Inf_greatest local.Inf_lower local.inv_invol)
+
+lemma inv_top [simp]: "\<top>\<^sup>\<circ> = \<top>"
+proof-
+  have a: "\<top>\<^sup>\<circ> \<le> \<top>"
+    by simp
+  hence "(\<top>\<^sup>\<circ>)\<^sup>\<circ> \<le> \<top>\<^sup>\<circ>"
+    using local.inv_iso by blast
+  hence "\<top> \<le> \<top>\<^sup>\<circ>"
+    by simp
+  thus ?thesis
+    by (simp add: local.top_le)
+qed
+
+lemma inv_qstar_aux [simp]: "(x ^ i)\<^sup>\<circ> = (x\<^sup>\<circ>) ^ i"
+  by (induct i, simp_all add: local.power_commutes)
+
+lemma inv_conjugate: "(x\<^sup>\<circ> \<sqinter> y = \<bottom>) = (x \<sqinter> y\<^sup>\<circ> = \<bottom>)"
+  using inv_binf invqka.inv_zero by fastforce
+
+text \<open>We define domain and codomain as in relation algebra and compare with the domain 
+and codomain axioms above.\<close>
+
+definition do :: "'a \<Rightarrow> 'a" where 
+  "do x = 1 \<sqinter> (x \<cdot> x\<^sup>\<circ>)"
+
+definition cd :: "'a \<Rightarrow> 'a" where
+  "cd x = 1 \<sqinter> (x\<^sup>\<circ> \<cdot> x)"
+
+lemma do_inv: "do (x\<^sup>\<circ>) = cd x"
+proof-
+  have "do (x\<^sup>\<circ>) = 1 \<sqinter> (x\<^sup>\<circ> \<cdot> (x\<^sup>\<circ>)\<^sup>\<circ>)"
+    by (simp add: do_def)
+  also have "\<dots> = 1 \<sqinter> (x\<^sup>\<circ> \<cdot> x)"
+    by simp
+  also have "\<dots> = cd x"
+    by (simp add: cd_def)
+  finally show ?thesis.
+qed
+
+lemma cd_inv: "cd (x\<^sup>\<circ>) = do x"
+  by (simp add: cd_def do_def)
+
+lemma do_le_top: "do x \<le> 1 \<sqinter> (x \<cdot> \<top>)"
+  by (simp add: do_def local.inf.coboundedI2 local.mult_isol)
+
+lemma do_subid: "do x \<le> 1"
+  by (simp add: do_def)
+
+lemma cd_subid: "cd x \<le> 1"
+  by (simp add: cd_def)
+
+lemma do_bot [simp]: "do \<bottom> = \<bottom>"
+  by (simp add: do_def)
+
+lemma cd_bot [simp]: "cd \<bottom> = \<bottom>"
+  by (simp add: cd_def)
+
+lemma do_iso: "x \<le> y \<Longrightarrow> do x \<le> do y"
+  by (simp add: do_def local.inf.coboundedI2 local.inv_iso local.psrpq.mult_isol_var)
+
+lemma cd_iso: "x \<le> y \<Longrightarrow> cd x \<le> 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 \<squnion> do y \<le> do (x \<squnion> y)"
+proof-
+  have "do x \<le> do (x \<squnion> y)" and "do y \<le> do (x \<squnion> y)"
+    by (simp_all add: do_iso)
+  thus ?thesis
+    by simp
+qed
+
+lemma cd_subdist: "cd x \<squnion> cd y \<le> cd (x \<squnion> y)"
+  by (simp add: cd_iso)
+
+lemma inv_do [simp]: "(do x)\<^sup>\<circ> = do x"
+  by (simp add: do_def)
+
+lemma inv_cd [simp]: "(cd x)\<^sup>\<circ> = cd x"
+  by (metis do_inv inv_do)
+
+lemma dedekind_modular:
+  assumes "(x \<cdot> y) \<sqinter> z \<le> (x \<sqinter> (z \<cdot> y\<^sup>\<circ>)) \<cdot> (y \<sqinter> (x\<^sup>\<circ> \<cdot> z))"
+  shows "(x \<cdot> y) \<sqinter> z \<le> (x \<sqinter> (z \<cdot> y\<^sup>\<circ>)) \<cdot> y"
+  using assms local.inf.cobounded1 local.mult_isol local.order_trans by blast
+
+lemma modular_eq1: 
+  assumes "\<forall>x y z w. (y \<sqinter> (z \<cdot> x\<^sup>\<circ>) \<le> w \<longrightarrow> (y \<cdot> x) \<sqinter> z \<le> w \<cdot> x)"
+  shows "\<forall>x y z. (x \<cdot> y) \<sqinter> z \<le> (x \<sqinter> (z \<cdot> y\<^sup>\<circ>)) \<cdot> y"
+  using assms by blast
+
+lemma "do x \<cdot> do y = do x \<sqinter> do y" (* nitpick[expect=genuine]*)
+  oops
+
+lemma "p \<le> 1 \<Longrightarrow> q \<le> 1 \<Longrightarrow> p \<cdot> q = p \<sqinter> q" (* nitpick[expect=genuine]*)
+  oops
+
+end
+
+sublocale ab_unital_quantale \<subseteq> 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 "\<forall>x y. x\<^sup>\<circ> \<cdot> -(x \<cdot> y) \<le> -y"
+  shows  "((x \<cdot> y) \<sqinter> z\<^sup>\<circ> = \<bottom>) = ((y \<cdot> z) \<sqinter> x\<^sup>\<circ> = \<bottom>)"
+proof
+  assume "(x \<cdot> y) \<sqinter> z\<^sup>\<circ> = \<bottom>"
+  hence "z\<^sup>\<circ> \<le> -(x \<cdot> y)"
+    by (simp add: local.inf.commute local.inf_shunt)
+  thus "(y \<cdot> z) \<sqinter> x\<^sup>\<circ> = \<bottom>"
+    by (metis assms local.inf_shunt local.inv_conjugate local.inv_contrav local.inv_invol local.mult_isol local.order.trans)
+next 
+  assume "(y \<cdot> z) \<sqinter> x\<^sup>\<circ> = \<bottom>"
+  hence "x\<^sup>\<circ> \<le> -(y \<cdot> z)"
+    using local.compl_le_swap1 local.inf_shunt by blast
+  thus "(x \<cdot> y) \<sqinter> z\<^sup>\<circ> = \<bottom>"
+    by (metis assms local.dual_order.trans local.inf_shunt local.inv_conjugate local.inv_contrav local.mult_isol)
+qed
+
+lemma res_schroeder1: 
+  assumes "\<forall>x y. x\<^sup>\<circ> \<cdot> -(x \<cdot> y) \<le> -y"
+  shows "((x \<cdot> y) \<sqinter> z = \<bottom>) = (y \<sqinter> (x\<^sup>\<circ> \<cdot> z) = \<bottom>)"
+proof
+  assume h: "(x \<cdot> y) \<sqinter> z = \<bottom>"
+  hence "z \<le> -(x \<cdot> y)"
+    by (simp add: local.inf.commute local.inf_shunt)
+  thus "y \<sqinter> (x\<^sup>\<circ> \<cdot> z) = \<bottom>"
+    by (metis assms local.dual_order.trans local.inf.commute local.inf_shunt local.mult_isol)
+next 
+  assume "y \<sqinter> (x\<^sup>\<circ> \<cdot> z) = \<bottom>"
+  hence "y \<le> -(x\<^sup>\<circ> \<cdot> z)"
+    by (simp add: local.inf_shunt)
+  thus "(x \<cdot> y) \<sqinter> z = \<bottom>"
+    by (metis assms local.inf_shunt local.inv_invol local.order_trans mult_isol)
+qed
+
+lemma res_schroeder2: 
+  assumes "\<forall>x y. x\<^sup>\<circ> \<cdot> -(x \<cdot> y) \<le> -y"
+  shows "((x \<cdot> y) \<sqinter> z = \<bottom>) = (x \<sqinter> (z \<cdot> y\<^sup>\<circ>) = \<bottom>)"
+  by (metis assms local.inv_invol local.res_peirce local.res_schroeder1)
+
+lemma res_mod:
+  assumes  "\<forall>x y. x\<^sup>\<circ> \<cdot> -(x \<cdot> y) \<le> -y"
+  shows "(x \<cdot> y) \<sqinter> z \<le> (x \<sqinter> (z \<cdot> y\<^sup>\<circ>)) \<cdot> y"
+proof-
+  have "(x \<cdot> y) \<sqinter> z = ((x \<sqinter> ((z \<cdot> y\<^sup>\<circ>) \<squnion> -(z \<cdot> y\<^sup>\<circ>))) \<cdot> y) \<sqinter> z"
+    by simp
+  also have "\<dots> = (((x \<sqinter> (z \<cdot> y\<^sup>\<circ>)) \<cdot> y) \<sqinter> z) \<squnion> (((x \<sqinter> -(z \<cdot> y\<^sup>\<circ>)) \<cdot> y) \<sqinter> z)"
+    using local.chaq.wswq.distrib_left local.inf.commute local.sup_distr by presburger
+  also have "\<dots> \<le> ((x \<sqinter> (z \<cdot> y\<^sup>\<circ>)) \<cdot> y) \<squnion> ((x \<cdot> y) \<sqinter> (-(z \<cdot> y\<^sup>\<circ>)) \<cdot> y \<sqinter> z)"
+    by (metis assms local.inf.commute local.inf_compl_bot_right local.sup.orderI local.sup_inf_absorb res_schroeder2)
+  also have "\<dots> \<le> ((x \<sqinter> (z \<cdot> y\<^sup>\<circ>)) \<cdot> y) \<squnion> ((x \<cdot> y) \<sqinter> -z  \<sqinter> z)"
+    by (metis assms local.dual_order.eq_iff local.inf.commute local.inf_compl_bot_right res_schroeder2)
+  also have "\<dots> \<le> ((x \<sqinter> (z \<cdot> y\<^sup>\<circ>)) \<cdot> y)"
+    by (simp add: local.inf.commute)
+  finally show ?thesis.
+qed
+
+end
+
+text \<open>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.\<close>
+
+class quantale_converse = involutive_quantale +
+  assumes strong_gelfand: "x \<le> x \<cdot> x\<^sup>\<circ> \<cdot> x"
+
+begin
+
+lemma do_gelfand [simp]: "do x \<cdot> do x \<cdot> 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 \<cdot> cd x \<cdot> cd x = cd x"
+  by (metis do_gelfand local.do_inv)
+
+lemma do_idem [simp]: "do x \<cdot> 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 \<cdot> 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 \<sqinter> (do x \<cdot> do x)"
+    using local.do_def local.inv_do by force
+  also have "\<dots> = 1 \<sqinter> do x"
+    by simp
+  also have "\<dots> = 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\<^sup>\<circ>))"
+    by (simp add: local.do_inv)
+  also have "\<dots> = do (x\<^sup>\<circ>)"
+    by simp
+  also have "\<dots> = 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 \<subseteq> convqka: kleene_algebra_converse "(\<squnion>)" "(\<cdot>)" 1 \<bottom> "(\<le>)" "(<)" invol qstar
+  by unfold_locales (simp add: local.strong_gelfand)
+
+
+subsection \<open>Dedekind quantales\<close>
+
+class dedekind_quantale = involutive_quantale +
+  assumes modular_law: "(x \<cdot> y) \<sqinter> z \<le> (x \<sqinter> (z \<cdot> y\<^sup>\<circ>)) \<cdot> y"
+
+begin
+
+sublocale convdqka: kleene_algebra_converse  "(\<squnion>)" "(\<cdot>)" 1 \<bottom> "(\<le>)" "(<)" 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 \<sqinter> (z \<cdot> y\<^sup>\<circ>)) \<cdot> y) \<sqinter> z = (x \<cdot> y) \<sqinter> 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 \<cdot> (y \<sqinter> (x\<^sup>\<circ> \<cdot> z))) \<sqinter> z = (x \<cdot> y) \<sqinter> z"
+  by (metis local.inv_binf local.inv_contrav local.inv_invol modular_2)
+
+lemma modular3: "(x \<cdot> y) \<sqinter> z \<le> x \<cdot> (y \<sqinter> (x\<^sup>\<circ> \<cdot> z))"
+  by (metis local.inf.cobounded1 modular_1)
+
+text \<open>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).\<close>
+
+lemma dedekind: "(x \<cdot> y) \<sqinter> z \<le> (x \<sqinter> (z \<cdot> y\<^sup>\<circ>)) \<cdot> (y \<sqinter> (x\<^sup>\<circ> \<cdot> z))"
+proof-
+  have  "(x \<cdot> y) \<sqinter> z = (x \<cdot> (y \<sqinter> (x\<^sup>\<circ> \<cdot> z))) \<sqinter> z"
+    by simp
+  also have "\<dots> \<le> (x \<sqinter> (z \<cdot> (y \<sqinter> (x\<^sup>\<circ> \<cdot> z))\<^sup>\<circ>)) \<cdot> (y \<sqinter> (x\<^sup>\<circ> \<cdot> z))"
+    using local.modular_law by presburger
+  also have "\<dots> = (x \<sqinter> (z \<cdot> (y\<^sup>\<circ> \<sqinter> (z\<^sup>\<circ> \<cdot> x)))) \<cdot> (y \<sqinter> (x\<^sup>\<circ> \<cdot> z))"
+    by simp
+  also have "\<dots> \<le> (x \<sqinter> (z \<cdot> y\<^sup>\<circ>)) \<cdot> (y \<sqinter> (x\<^sup>\<circ> \<cdot> z))"
+    using local.inf.commute modular_1 by fastforce
+  finally show ?thesis.
+qed
+
+lemma peirce: "((x \<cdot> y) \<sqinter> z\<^sup>\<circ> = \<bottom>) = ((y \<cdot> z) \<sqinter> x\<^sup>\<circ> = \<bottom>)"
+proof
+  assume "(x \<cdot> y) \<sqinter> z\<^sup>\<circ> = \<bottom>"
+  hence "((x \<cdot> y) \<sqinter> z\<^sup>\<circ>) \<cdot> y\<^sup>\<circ> = \<bottom>"
+    by simp
+  hence "(z\<^sup>\<circ> \<cdot> y\<^sup>\<circ>) \<sqinter> x = \<bottom>"
+    by (metis local.inf.commute local.inv_invol local.le_bot local.modular_law)
+  hence "((y \<cdot> z) \<sqinter> x\<^sup>\<circ>)\<^sup>\<circ> = \<bottom>\<^sup>\<circ>"
+    by simp
+  thus "(y \<cdot> z) \<sqinter> x\<^sup>\<circ> = \<bottom>"
+    by (metis local.inv_invol)
+next
+  assume h: "(y \<cdot> z) \<sqinter> x\<^sup>\<circ> = \<bottom>"
+  hence "z\<^sup>\<circ> \<cdot> ((y \<cdot> z) \<sqinter> x\<^sup>\<circ>) = \<bottom>"
+    by simp
+  hence "(y\<^sup>\<circ> \<cdot> x\<^sup>\<circ>) \<sqinter> z = \<bottom>"
+    by (metis h local.inf.commute local.inv_invol local.le_bot local.mult_botr modular3)
+   hence "((x \<cdot> y) \<sqinter> z\<^sup>\<circ>)\<^sup>\<circ> = \<bottom>\<^sup>\<circ>"
+    by simp
+  thus "(x \<cdot> y) \<sqinter> z\<^sup>\<circ> = \<bottom>"
+    by (metis local.inv_invol)
+qed
+
+lemma schroeder_1: "((x \<cdot> y) \<sqinter> z = \<bottom>) = (y \<sqinter> (x\<^sup>\<circ> \<cdot> z) = \<bottom>)"
+  by (metis local.inf.commute local.inf_bot_right local.inv_invol local.mult_botr modular_1)
+
+lemma schroeder_2: "((x \<cdot> y) \<sqinter> z = \<bottom>) = (x \<sqinter> (z \<cdot> y\<^sup>\<circ>) = \<bottom>)"
+  by (metis local.inv_invol peirce schroeder_1)
+
+lemma modular_eq2: "y \<sqinter> (z \<cdot> x\<^sup>\<circ>) \<le> w \<Longrightarrow> (y \<cdot> x) \<sqinter> z \<le> w \<cdot> x"
+  by (meson local.dual_order.trans local.eq_refl local.h_w1 local.modular_law)
+
+lemma lla_top_aux: "p \<le> 1 \<Longrightarrow> ((x \<le> p \<cdot> x) = (x \<le> p \<cdot> \<top>))"
+proof
+  assume h: "p \<le> 1"
+  and h1: "x \<le> p \<cdot> x"
+  thus "x \<le> p \<cdot> \<top>"
+    by (meson local.mult_isol local.order_trans local.top_greatest)
+next 
+  assume h: "p \<le> 1"
+  and "x \<le> p \<cdot> \<top>"
+  hence "x = (p \<cdot> \<top>) \<sqinter> x"
+    using local.inf.absorb_iff2 by auto
+  also have "\<dots> \<le> p \<cdot> (\<top> \<sqinter> (p\<^sup>\<circ> \<cdot> x))"
+    using modular3 by blast
+  also have "\<dots> = p \<cdot> p \<cdot> x"
+    by (simp add: h local.convdqka.subid_conv mult_assoc)
+  finally show "x \<le> p \<cdot> x"
+    by (metis h local.dual_order.trans local.mult_isor local.nsrnqo.mult_onel)
+qed
+
+text \<open>Next we turn to properties of domain and codomain in Dedekind quantales.\<close>
+
+lemma lra_top_aux: "p \<le> 1 \<Longrightarrow> ((x \<le> x \<cdot> p ) = (x \<le> \<top> \<cdot> 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 \<le> 1 \<Longrightarrow> ((do x \<le> p) = (x \<le> p \<cdot> \<top>))"
+proof 
+  assume a1: "x \<le> p \<cdot> \<top>"
+  assume a2: "p \<le> 1"
+  have f3: "x \<cdot> \<top> \<le> p \<cdot> \<top> \<cdot> \<top>"
+    by (simp add: a1 local.mult_isor)
+  have f4: "p \<cdot> do x \<le> p"
+    by (simp add: local.do_subid local.uqka.star_inductr_var_equiv local.uwqlka.star_subid)
+  have "x \<cdot> \<top> \<le> p \<cdot> \<top>"
+    using f3 by (simp add: local.mult.semigroup_axioms semigroup.assoc)
+  thus "do x \<le> 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 \<le> p"
+  assume a2: "p \<le> 1"
+  hence  "do x \<cdot> x \<le> p \<cdot> x"
+    by (simp add: a1 local.mult_isor)
+  hence "x \<le> p \<cdot> x"
+    using a1 local.do_def modular_eq2 by fastforce
+  thus "x \<le> p \<cdot> \<top>"
+    by (simp add: a2 lla_top_aux)
+qed
+
+lemma lla_Inf: "do x = \<Sqinter>{p. x \<le> p \<cdot> \<top> \<and> p \<le> 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 \<le> 1 \<Longrightarrow> ((cd x \<le> p) = (x \<le> \<top> \<cdot> 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 = \<Sqinter>{p. x \<le> \<top> \<cdot> p \<and> p \<le> 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 \<le> 1 \<Longrightarrow> ((do x \<le> p) = (x \<le> p \<cdot> x))"
+  by (simp add: lla lla_top_aux)
+
+lemma lla_Inf_var: "do x = \<Sqinter>{p. x \<le> p \<cdot> x \<and> p \<le> 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 \<le> 1 \<Longrightarrow> ((cd x \<le> p) = (x \<le> x \<cdot> p))"
+  by (simp add: lra lra_top_aux)
+
+lemma lra_Inf_var: "cd x = \<Sqinter>{p. x \<le> x \<cdot> p \<and> p \<le> 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 \<sqinter> (x \<cdot> \<top>)"
+proof-
+  have "1 \<sqinter> (x \<cdot> \<top>) = 1 \<sqinter> (x \<cdot> (\<top> \<sqinter> x\<^sup>\<circ> \<cdot> 1))"
+    by (metis local.inf.commute local.inf_top.left_neutral modular_1)
+  also have "\<dots> = do x"
+    by (simp add: local.do_def)
+  finally show ?thesis..
+qed
+
+lemma cd_top: "cd x = 1 \<sqinter> (\<top> \<cdot> 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 \<open>We start deriving the axioms of modal semirings and modal quantales.\<close>
+
+lemma do_absorp: "x \<le> do x \<cdot> x"
+  using lla_var local.do_subid by blast
+
+lemma cd_absorp: "x \<le> x \<cdot> cd x"
+  using local.cd_subid lra_var by blast
+
+lemma do_absorp_eq [simp]: "do x \<cdot> x = x"
+  using do_absorp local.do_subid local.dual_order.antisym local.h_w1 by fastforce
+
+lemma cd_absorp_eq [simp]: "x \<cdot> 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 \<cdot> \<top> = do x \<cdot> \<top>"
+proof (rule order.antisym)
+  have "x \<cdot> \<top> = do x \<cdot> x \<cdot> \<top>"
+    by simp
+  also have "\<dots> \<le> do x \<cdot> \<top> \<cdot> \<top>"
+    using local.psrpq.mult_double_iso local.top_greatest by presburger
+  also have "\<dots> = do x \<cdot> \<top>"
+    by (simp add: local.mult.semigroup_axioms semigroup.assoc)
+  finally show "x \<cdot> \<top> \<le> do x \<cdot> \<top>".
+  have "do x \<cdot> \<top> = (1 \<sqinter> (x \<cdot> \<top>)) \<cdot> \<top>"
+    by (simp add: do_top)
+  also have "\<dots> \<le> (1 \<cdot> \<top>) \<sqinter> (x \<cdot> \<top> \<cdot> \<top>)"
+    by (simp add: local.mult_isor)
+  also have "\<dots> = x \<cdot> \<top>"
+    by (simp add: mult_assoc)
+  finally show "do x \<cdot> \<top> \<le> x \<cdot> \<top>".
+qed
+
+lemma cd_top2: "\<top> \<cdot> x  = \<top> \<cdot> 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 \<cdot> do y) = do (x \<cdot> y)"
+proof-
+  have "do (x \<cdot> do y) = 1 \<sqinter> (x \<cdot> do y \<cdot> \<top>)"
+    using do_top by force
+  also have "\<dots> = 1 \<sqinter> (x \<cdot> y \<cdot> \<top>)"
+    using do_top2 mult_assoc by force
+  also have "\<dots> = do (x \<cdot> y)"
+    by (simp add: do_top)
+  finally show ?thesis
+    by force
+qed
+
+lemma cd_local [simp]: "cd (cd x \<cdot> y) = cd (x \<cdot> y)"
+  by (metis cd_top cd_top2 mult_assoc)
+
+lemma do_fix_subid: "(do x = x) = (x \<le> 1)"
+proof
+  assume "do x = x"
+  thus "x \<le> 1"
+    by (metis local.do_subid)
+next 
+  assume a: "x \<le> 1"
+  hence "x = do x \<cdot> x"
+    by simp
+  hence b: "x \<le> do x"
+    by (metis a local.mult_isol local.nsrnqo.mult_oner)
+  have "x \<cdot> x \<le> x"
+    using a local.mult_isor by fastforce
+  hence  "do x \<le> 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 \<le> 1)"
+  by (metis local.convdqka.subid_conv local.do_inv local.do_fix_subid local.docd_compat)
+
+lemma do_inf2: "do (do x \<sqinter> do y) = do x \<sqinter> do y"
+  using do_top local.do_fix_subid local.inf.assoc by auto
+
+lemma do_inf_comp: "do x \<cdot> do y = do x \<sqinter> 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 \<cdot> cd y = cd x \<sqinter> cd y"
+  by (metis do_inf_comp local.docd_compat)
+
+lemma subid_mult_meet: "p \<le> 1 \<Longrightarrow> q \<le> 1 \<Longrightarrow> p \<cdot> q = p \<sqinter> q"
+  by (metis do_inf_comp local.do_fix_subid)
+
+lemma dodo_sup: "do (do x \<squnion> do y) = do x \<squnion> do y"
+proof-
+  have "do (do x \<squnion> do y) = 1 \<sqinter> ((do x \<squnion> do y) \<cdot> (do x \<squnion> do y)\<^sup>\<circ>)"
+    using local.do_def by blast
+  also have "\<dots> = 1 \<sqinter> ((do x \<squnion> do y) \<cdot> (do x \<squnion> do y))"
+    by simp
+  also have "\<dots> = 1 \<sqinter> (do x \<squnion> do y)"
+    using local.do_subid local.dodo local.inf.idem local.le_supI subid_mult_meet by presburger
+  also have "\<dots> = do x \<squnion> do y"
+    by (simp add: local.do_def local.inf_absorb2)
+  finally show ?thesis.
+qed
+
+lemma do_sup [simp]: "do (x \<squnion> y) = do x \<squnion> do y"
+proof-
+  have "do (x \<squnion> y) = 1 \<sqinter> ((x \<squnion> y) \<cdot> \<top>)"
+    by (simp add: do_top)
+  also have "\<dots> = 1 \<sqinter> (x \<cdot> \<top> \<squnion> y \<cdot> \<top>)"
+    by simp
+  also have "\<dots> = 1 \<sqinter> (do x \<cdot> \<top> \<squnion> do y \<cdot> \<top>)"
+    using do_top2 by force
+  also have "\<dots> = 1 \<sqinter> ((do x \<squnion> do y) \<cdot> \<top>)"
+    by simp
+  also have "\<dots> = do (do x \<squnion> do y)"
+    by (simp add: do_top)
+  finally show ?thesis
+    by (simp add: dodo_sup)
+qed
+
+lemma cdcd_sup: "cd (cd x \<squnion> cd y) = cd x \<squnion> cd y"
+  using local.cd_fix_subid by fastforce
+
+lemma cd_sup [simp]: "cd (x \<squnion> y) = cd x \<squnion> cd y"
+  by (metis do_sup local.do_inv local.inv_binsup)
+
+text \<open>Next we show that Dedekind quantales are modal quantales, hence also modal semirings.\<close>
+
+sublocale dmq: dc_modal_quantale 1 "(\<cdot>)" Inf Sup "(\<sqinter>)" "(\<le>)" "(<)" "(\<squnion>)" "\<bottom>" "\<top>" cd do
+proof
+  show "\<And>x. cd x \<le> 1"
+    by (simp add: cd_top)
+  show "\<And>x. do x \<le> 1"
+    by (simp add: do_top)
+qed simp_all
+
+lemma do_top3 [simp]: "do (x \<cdot> \<top>) = do x"
+  using dmq.coddual.le_top dmq.dqmsr.domain_1'' local.do_iso local.order.antisym by presburger
+
+lemma cd_top3 [simp]: "cd (\<top> \<cdot> x) = cd x"
+  by (simp add: cd_top dmq.coddual.mult_assoc)
+
+lemma dodo_Sup_pres: "do (\<Squnion>x \<in> X. do x) = (\<Squnion>x \<in> X. do x)"
+  by (simp add: local.SUP_least local.do_fix_subid)
+
+text \<open>The domain elements form a complete Heyting algebra.\<close>
+
+lemma do_complete_heyting: "do x \<sqinter> (\<Squnion>y \<in> Y. do y) = (\<Squnion>y \<in> Y. do x \<sqinter> do y)"
+proof-
+  have "do x \<sqinter> (\<Squnion>y \<in> Y. do y) = do x \<cdot> (\<Squnion>y \<in> Y. do y)"
+    by (metis do_inf_comp dodo_Sup_pres)
+  also have "\<dots> = (\<Squnion>y \<in> Y. do x \<cdot> do y)"
+    by (simp add: dmq.coddual.Sup_distr image_image)
+  also have "\<dots> = (\<Squnion>y \<in> Y. do x \<sqinter> do y)"
+    using do_inf_comp by force
+  finally show ?thesis.
+qed
+
+lemma cdcd_Sup_pres: "cd (\<Squnion>x \<in> X. cd x) = (\<Squnion>x \<in> X. cd x)"
+  by (simp add: local.SUP_least local.cd_fix_subid)
+
+lemma cd_complete_heyting: "cd x \<sqinter> (\<Squnion>y \<in> Y. cd y) = (\<Squnion>y \<in> Y. cd x \<sqinter> cd y)"
+proof-
+  have "cd x \<sqinter> (\<Squnion>y \<in> Y. cd y) = cd x \<cdot> (\<Squnion>y \<in> Y. cd y)"
+    by (metis cd_inf_comp cdcd_Sup_pres)
+  also have "\<dots> = (\<Squnion>y \<in> Y. cd x \<cdot> cd y)"
+    by (simp add: dmq.coddual.Sup_distr image_image)
+  also have "\<dots> = (\<Squnion>y \<in> Y. cd x \<sqinter> cd y)"
+    using cd_inf_comp by force
+  finally show ?thesis.
+qed
+
+lemma subid_complete_heyting: 
+  assumes "p \<le> 1"
+  and "\<forall>q \<in> Q. q \<le> 1"
+  shows "p \<sqinter> (\<Squnion>Q) = (\<Squnion>q \<in> Q. p \<sqinter> q)"
+proof-
+  have a: "do p = p"
+    by (simp add: assms(1) local.do_fix_subid)
+  have b: "\<forall>q \<in> Q. do q = q"
+    using assms(2) local.do_fix_subid by presburger
+  hence "p \<sqinter> (\<Squnion>Q) = do p \<sqinter> (\<Squnion>q \<in> Q. do q)"
+    by (simp add: a)
+  also have "\<dots> = (\<Squnion>q \<in> Q. do p \<sqinter> do q)"
+    using do_complete_heyting by blast
+  also have "\<dots> = (\<Squnion>q \<in> Q. p \<sqinter> q)"
+    using a b by force
+  finally show ?thesis.
+qed
+
+text \<open>Next we show that domain and codomain preserve arbitrary Sups.\<close>
+
+lemma do_Sup_pres_aux: "(\<Squnion>x \<in> X. do x \<cdot> \<top>) = (\<Squnion>x \<in> do ` X. x \<cdot> \<top>)"
+  by (smt (verit, best) Sup.SUP_cong image_image)
+
+lemma do_Sup_pres: "do (\<Squnion>x \<in> X. x) = (\<Squnion>x \<in> X. do x)"
+proof-
+  have "do (\<Squnion>x \<in> X. x) = 1 \<sqinter> ((\<Squnion>x \<in> X. x) \<cdot> \<top>)"
+    by (simp add: do_top)
+  also have "\<dots> = 1 \<sqinter> (\<Squnion>x \<in> X. x \<cdot> \<top>)"
+    by (simp add: dmq.coddual.Sup_distl)
+  also have "\<dots> = 1 \<sqinter> (\<Squnion>x \<in> X. do x \<cdot> \<top>)"
+    using do_top2 by force
+  also have "\<dots> = 1 \<sqinter> (\<Squnion>x \<in> do ` X. x \<cdot> \<top>)"
+    using do_Sup_pres_aux by presburger
+  also have "\<dots> = 1 \<sqinter> ((\<Squnion>x \<in> X. do x) \<cdot> \<top>)"
+    using dmq.coddual.Sup_distl by presburger
+  also have "\<dots> = do (\<Squnion>x \<in> X. do x)"
+    by (simp add: do_top)
+  finally show ?thesis
+    using dodo_Sup_pres by presburger
+qed
+
+lemma cd_Sup_pres: "cd (\<Squnion>x \<in> X. x) = (\<Squnion>x \<in> X. cd x)"
+proof-
+  have "cd (\<Squnion>x \<in> X. x) = do ((\<Squnion>x \<in> X. x)\<^sup>\<circ>)"
+    using local.do_inv by presburger
+  also have "\<dots> = do (\<Squnion>x \<in> X. x\<^sup>\<circ>)"
+    by simp
+  also have "\<dots> = (\<Squnion>x \<in> X. do (x\<^sup>\<circ>))"
+    by (metis do_Sup_pres image_ident image_image)
+  also have "\<dots> = (\<Squnion>x \<in> X. cd x)"
+    using local.do_inv by presburger
+  finally show ?thesis.
+qed
+
+lemma do_inf: "do (x \<sqinter> y) = 1 \<sqinter> (y \<cdot> x\<^sup>\<circ>)"
+  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 \<sqinter> y) = 1 \<sqinter> (y\<^sup>\<circ> \<cdot> x)"
+  by (metis do_inf local.do_inv local.inv_binf local.inv_invol)
+
+lemma do_bres_prop: "p \<le> 1 \<Longrightarrow> do (x \<rightarrow> p \<cdot> \<top>) = 1 \<sqinter> (x \<rightarrow> p \<cdot> \<top>)"
+  by (simp add: do_top)
+
+lemma cd_fres_prop: "p \<le> 1 \<Longrightarrow> cd (\<top> \<cdot> p \<leftarrow> x) = 1 \<sqinter> (\<top> \<cdot> p \<leftarrow> x)"
+  by (simp add: cd_top)
+
+lemma do_meet_prop: "(do p \<cdot> x) \<sqinter> (x \<cdot> do q) = do p \<cdot> x \<cdot> do q"
+proof (rule order.antisym)
+  have "x \<sqinter> (do p \<cdot> x \<cdot> do q) \<le> do p \<cdot> x"
+    by (simp add: dmq.dqmsr.dom_subid_aux2'' local.inf.coboundedI2)
+  thus  "(do p \<cdot> x) \<sqinter> (x \<cdot> do q) \<le> do p \<cdot> x \<cdot> do q"
+    by (simp add: local.inf.commute modular_eq2)
+next
+  have "do p \<cdot> x \<cdot> do q = (do p \<cdot> x \<cdot> do q) \<sqinter> (do p \<cdot> x \<cdot> do q)"
+    by simp
+  also have "\<dots> \<le> (do p \<cdot> x) \<sqinter> (x \<cdot> do q)"
+    using dmq.dqmsr.dom_subid_aux2 dmq.dqmsr.dom_subid_aux2'' local.psrpq.mult_isol_var by auto
+  finally show "do p \<cdot> x \<cdot> do q \<le> (do p \<cdot> x) \<sqinter> (x \<cdot> do q)".
+qed
+
+lemma subid_meet_prop: "p \<le> 1 \<Longrightarrow> q \<le> 1 \<Longrightarrow> (p \<cdot> x) \<sqinter> (x \<cdot> q) = p \<cdot> x \<cdot> q"
+  by (metis do_fix_subid do_meet_prop)
+
+text \<open>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.\<close>
+
+abbreviation "do_dia \<equiv> dmq.fd'"
+
+abbreviation "cd_dia \<equiv> dmq.bd'"
+
+abbreviation "do_box \<equiv> dmq.bb"
+
+abbreviation "cd_box \<equiv> dmq.fb"
+
+text \<open>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.\<close>
+
+lemma do_dia_cd_dia_conv: "p \<le> 1 \<Longrightarrow> do_dia (x\<^sup>\<circ>) 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 \<le> 1 \<Longrightarrow> cd_dia (x\<^sup>\<circ>) p = do_dia x p"
+  by (metis do_dia_cd_dia_conv local.inv_invol)
+
+text \<open>Diamonds preserve sups in both arguments.\<close>
+
+lemma do_dia_Sup: "do_dia (\<Squnion>X) p = (\<Squnion>x \<in> X. do_dia x p)"
+proof-
+  have "do_dia (\<Squnion>X) p = do ((\<Squnion>X) \<cdot> p)"
+    by (simp add: dmq.dqmsr.fd_def)
+  also have "\<dots> = do (\<Squnion>x \<in> X. x \<cdot> p)"
+    using local.Sup_distr by fastforce
+ also have "\<dots> = (\<Squnion>x \<in> X. do (x \<cdot> p))"
+   by (metis do_Sup_pres image_ident image_image)
+  also have "\<dots> = (\<Squnion>x \<in> X. do_dia x p)"
+    using dmq.dqmsr.fd_def by fastforce
+  finally show ?thesis.
+qed
+
+lemma do_dia_Sup2: "do_dia x (\<Squnion>P) = (\<Squnion>p \<in> P. do_dia x p)"
+proof-
+  have  "do_dia x (\<Squnion>P) = do (x \<cdot> (\<Squnion>P))"
+    by (simp add: dmq.dqmsr.fd_def)
+  also have "\<dots> = (\<Squnion>p \<in> P. do (x \<cdot> p))"
+    by (metis dmq.coddual.Sup_distr do_Sup_pres image_ident image_image)
+  also have "\<dots> = (\<Squnion>p \<in> P. do_dia x p)"
+    using dmq.dqmsr.fd_def by auto
+  finally show ?thesis.
+qed
+
+lemma cd_dia_Sup: "cd_dia (\<Squnion>X) p = (\<Squnion>x \<in> X. cd_dia x p)"
+proof-
+  have "cd_dia (\<Squnion>X) p = cd (p \<cdot> (\<Squnion>X))"
+    by (simp add: dmq.coddual.dqmsr.fd_def)
+  also have "\<dots> = cd (\<Squnion>x \<in> X. p \<cdot> x)"
+    using dmq.coddual.Sup_distr by auto
+ also have "\<dots> = (\<Squnion>x \<in> X. cd (p \<cdot> x))"
+   by (metis cd_Sup_pres image_ident image_image)
+  also have "\<dots> = (\<Squnion>x \<in> X. cd_dia x p)"
+    using dmq.coddual.dqmsr.fd_def by force
+  finally show ?thesis.
+qed
+
+lemma cd_dia_Sup2: "cd_dia x (\<Squnion>P) = (\<Squnion>p \<in> P. cd_dia x p)"
+proof-
+  have  "cd_dia x (\<Squnion>P) = cd ((\<Squnion>P) \<cdot> x)"
+    by (simp add: dmq.coddual.dqmsr.fd_def)
+  also have "\<dots> = (\<Squnion>p \<in> P. cd (p \<cdot> x))"
+    by (metis cd_Sup_pres dmq.coddual.Sup_distl image_ident image_image)
+  also have "\<dots> = (\<Squnion>p \<in> P. cd_dia x p)"
+    using dmq.coddual.dqmsr.fd_def by auto
+  finally show ?thesis.
+qed
+
+text \<open>The domain-based box is a forward operator, the codomain-based on a backward one. These interact
+again with respect to converse.\<close>
+
+lemma do_box_var: "p \<le> 1 \<Longrightarrow> do_box x p = \<Squnion>{q. do_dia x q \<le> p \<and> q \<le> 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 \<le> 1 \<Longrightarrow> cd_box x p = \<Squnion>{q. cd_dia x q \<le> p \<and> q \<le> 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 \<le> 1 \<Longrightarrow> do_box (x\<^sup>\<circ>) p = cd_box x p"
+proof-
+  assume a: "p \<le> 1"
+  hence "do_box (x\<^sup>\<circ>) p = \<Squnion>{q. do_dia (x\<^sup>\<circ>) q \<le> p \<and> q \<le> 1}"
+    by (simp add: do_box_var)
+  also have "\<dots> =  \<Squnion>{q. cd_dia x q \<le> p \<and> q \<le> 1}"
+    by (metis do_dia_cd_dia_conv)
+  also have "\<dots> = cd_box x p"
+    using a cd_box_var by auto
+  finally show ?thesis.
+qed
+
+lemma cd_box_do_box_conv: "p \<le> 1 \<Longrightarrow> cd_box (x\<^sup>\<circ>) p = do_box x p"
+  by (metis do_box_cd_box_conv local.inv_invol)
+
+lemma do_box_subid: "do_box x p \<le> 1"
+  using dmq.bb_def local.Sup_le_iff by force
+
+lemma cd_box_subid: "p \<le> 1 \<Longrightarrow> cd_box x p \<le> 1"
+  by (metis do_box_subid local.do_box_cd_box_conv)
+
+text \<open>Next we prove that boxes and diamonds are adjoints, and then demodalisation laws known 
+from modal semirings.\<close>
+
+lemma do_dia_do_box_galois: 
+  assumes "p \<le> 1"
+  and "q \<le> 1" 
+  shows "(do_dia x p \<le> q) = (p \<le> do_box x q)"
+proof
+  show "do_dia x p \<le> q \<Longrightarrow> p \<le> do_box x q"
+    by (simp add: assms do_box_var local.Sup_upper)
+next
+  assume "p \<le> do_box x q"
+  hence "do_dia x p \<le> do (x \<cdot> \<Squnion>{t. do_dia x t \<le> q \<and> t \<le> 1})"
+    by (simp add: assms(2) local.dmq.dqmsr.fd_def local.do_box_var local.do_iso local.mult_isol)
+  also have "\<dots> = \<Squnion>{do (x \<cdot> t) |t. do_dia x t \<le> q \<and> t \<le> 1}"
+    by (metis do_Sup_pres image_ident image_image local.Sup_distl setcompr_eq_image)
+  also have "\<dots> = \<Squnion>{do_dia x t |t. do_dia x t \<le> q \<and> t \<le> 1}"
+    using local.dmq.dqmsr.fd_def by fastforce
+  also have "\<dots> \<le> q"
+    using local.Sup_le_iff by blast
+  finally have "do_dia x p \<le> q".
+  thus "p \<le> do_box x q \<Longrightarrow> do_dia x p \<le> q".
+qed
+
+lemma cd_dia_cd_box_galois: 
+  assumes "p \<le> 1"
+  and "q \<le> 1"
+shows "(cd_dia x p \<le> q) = (p \<le> 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 \<le> 1" 
+  and "q \<le> 1"
+shows "(do_dia x p \<le> q) = (x \<cdot> p \<le> q \<cdot> x)"
+  by (metis assms dmq.dqmsr.fdemodalisation2 local.do_fix_subid)
+
+text \<open>The demodalisation laws have variants based on residuals.\<close>
+
+lemma do_dia_demod_subid_fres: 
+  assumes "p \<le> 1" 
+  and "q \<le> 1"
+  shows "(do_dia x p \<le> q) = (p \<le> x \<rightarrow> q \<cdot> x)"
+  by (simp add: assms do_dia_demod_subid local.bres_galois)
+
+lemma do_dia_demod_subid_var: 
+  assumes "p \<le> 1" 
+  and "q \<le> 1"
+shows "(do_dia x p \<le> q) = (x \<cdot> p \<le> q \<cdot> \<top>)"
+  by (simp add: assms(2) dmq.dqmsr.fd_def lla)
+
+lemma do_dia_demod_subid_var_fres: 
+  assumes "p \<le> 1" 
+  and "q \<le> 1"
+shows "(do_dia x p \<le> q) = (p \<le> x \<rightarrow> q \<cdot> \<top>)"
+  by (simp add: assms do_dia_demod_subid_var local.bres_galois)
+
+lemma cd_dia_demod_subid: 
+  assumes "p \<le> 1" 
+  and "q \<le> 1"
+shows "(cd_dia x p \<le> q) = (p \<cdot> x \<le> x \<cdot> q)"
+  by (metis assms dmq.coddual.dqmsr.fdemodalisation2 local.cd_fix_subid)
+
+lemma cd_dia_demod_subid_fres: 
+  assumes "p \<le> 1" 
+  and "q \<le> 1"
+shows "(cd_dia x p \<le> q) = (p \<le> x \<cdot> q \<leftarrow> x)"
+  by (simp add: assms cd_dia_demod_subid local.fres_galois)
+
+lemma cd_dia_demod_subid_var: 
+  assumes "p \<le> 1" 
+  and "q \<le> 1"
+shows "(cd_dia x p \<le> q) = (p \<cdot> x \<le> \<top> \<cdot> q)"
+  by (simp add: assms(2) dmq.coddual.dqmsr.fd_def lra)
+
+lemma cd_dia_demod_subid_var_fres: 
+  assumes "p \<le> 1" 
+  and "q \<le> 1"
+shows "(cd_dia x p \<le> q) = (p \<le> \<top> \<cdot> q \<leftarrow> x)"
+  by (simp add: assms cd_dia_demod_subid_var local.fres_galois)
+
+lemma do_box_iso: 
+  assumes "p \<le> 1"
+  and "q \<le> 1" 
+  and "p \<le> q" 
+shows "do_box x p \<le> 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 \<le> 1"
+  and "q \<le> 1" 
+  and "p \<le> q" 
+shows "cd_box x p \<le> cd_box x q"
+  by (metis assms do_box_cd_box_conv do_box_iso)
+
+lemma do_box_demod_subid: 
+  assumes "p \<le> 1" 
+  and "q \<le> 1"
+  shows "(p \<le> do_box x q) = (x \<cdot> p \<le> q \<cdot> x)"
+  using assms do_dia_do_box_galois local.do_dia_demod_subid by force
+
+lemma do_box_demod_subid_bres: 
+  assumes "p \<le> 1" 
+  and "q \<le> 1"
+  shows "(p \<le> do_box x q) = (p \<le> x \<rightarrow> q \<cdot> x)"
+  by (simp add: assms do_box_demod_subid local.bres_galois)
+
+lemma do_box_demod_subid_var: 
+  assumes "p \<le> 1" 
+  and "q \<le> 1"
+  shows "(p \<le> do_box x q) = (x \<cdot> p \<le> q \<cdot> \<top>)"
+  using assms do_dia_demod_subid_var do_dia_do_box_galois by auto
+
+lemma do_box_demod_subid_var_bres: 
+  assumes "p \<le> 1" 
+  and "q \<le> 1"
+  shows "(p \<le> do_box x q) = (p \<le> x \<rightarrow> q \<cdot> \<top>)"
+  by (simp add: assms do_box_demod_subid_var local.bres_galois)
+
+lemma do_box_demod_subid_var_bres_do: 
+  assumes "p \<le> 1" 
+  and "q \<le> 1"
+  shows "(p \<le> do_box x q) = (p \<le> do (x \<rightarrow> q \<cdot> \<top>))"
+  by (simp add: assms do_box_demod_subid_var_bres do_top)
+
+lemma cd_box_demod_subid: 
+  assumes "p \<le> 1" 
+  and "q \<le> 1"
+  shows "(p \<le> cd_box x q) = (p \<cdot> x \<le> x \<cdot> q)"
+  using assms local.cd_dia_cd_box_galois local.cd_dia_demod_subid by force
+
+lemma cd_box_demod_subid_fres: 
+  assumes "p \<le> 1" 
+  and "q \<le> 1"
+  shows "(p \<le> cd_box x q) = (p \<le> x \<cdot> q \<leftarrow> x)"
+  by (simp add: assms cd_box_demod_subid local.fres_galois)
+
+lemma cd_box_demod_subid_var: 
+  assumes "p \<le> 1" 
+  and "q \<le> 1"
+  shows "(p \<le> cd_box x q) = (p \<cdot> x \<le> \<top> \<cdot> q)"
+  using assms cd_dia_cd_box_galois cd_dia_demod_subid_var by force
+
+lemma cd_box_demod_subid_var_fres: 
+  assumes "p \<le> 1" 
+  and "q \<le> 1"
+  shows "(p \<le> cd_box x q) = (p \<le> \<top> \<cdot> q \<leftarrow> x)"
+  by (simp add: assms cd_box_demod_subid_var local.fres_galois)
+
+text \<open>We substitute demodalisation inequalities for diamonds in the definitions of boxes.\<close> 
+
+lemma do_box_var2: "p \<le> 1 \<Longrightarrow> do_box x p = \<Squnion>{q. x \<cdot> q \<le> p \<cdot> x \<and> q \<le> 1}"
+  unfolding do_box_var by (meson do_dia_demod_subid)
+
+lemma do_box_bres1: "p \<le> 1 \<Longrightarrow> do_box x p = \<Squnion>{q. q \<le> x \<rightarrow> p \<cdot> x \<and> q \<le> 1}"
+  unfolding do_box_var by (meson do_dia_demod_subid_fres)
+
+lemma do_box_bres2: "p \<le> 1 \<Longrightarrow> do_box x p = \<Squnion>{q. q \<le> x \<rightarrow> p \<cdot> \<top> \<and> q \<le> 1}"
+  unfolding do_box_var by (simp add: dmq.dqmsr.fd_def lla local.bres_galois) 
+
+lemma do_box_var3: "p \<le> 1 \<Longrightarrow> do_box x p = \<Squnion>{q. x \<cdot> q \<le> p \<cdot> \<top> \<and> q \<le> 1}"
+  unfolding do_box_var using dmq.dqmsr.fd_def lla by force
+
+lemma cd_box_var2: "p \<le> 1 \<Longrightarrow> cd_box x p = \<Squnion>{q. q \<cdot> x \<le> x \<cdot> p \<and> q \<le> 1}"
+  unfolding cd_box_var by (metis cd_dia_demod_subid)
+
+lemma cd_box_var3: "p \<le> 1 \<Longrightarrow> cd_box x p = \<Squnion>{q. q \<cdot> x \<le> \<top> \<cdot> p \<and> q \<le> 1}"
+  unfolding cd_box_var by (simp add: dmq.coddual.dqmsr.fd_def lra)
+
+text \<open>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.\<close>
+
+lemma bres_do_box: "p \<le> 1 \<Longrightarrow> do_box x p = do (x \<rightarrow> p \<cdot> \<top>)"
+  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 \<le> 1 \<Longrightarrow> do_box x p = 1 \<sqinter> (x \<rightarrow> p \<cdot> \<top>)"
+  using bres_do_box do_bres_prop by force
+
+lemma bres_do_box_top: "p \<le> 1 \<Longrightarrow> (do_box x p) \<cdot> \<top> = x \<rightarrow> p \<cdot> \<top>"
+  using bres_do_box do_top2 by auto
+
+lemma fres_cd_box: "p \<le> 1 \<Longrightarrow> cd_box x p = cd (\<top> \<cdot> p \<leftarrow> x)"
+proof-
+  assume h0: "p \<le> 1"
+  {fix q 
+  assume h1: "q \<le> 1"
+  have "(q \<le> cd_box x p) = (q \<cdot> x \<le> \<top> \<cdot> p)"
+    by (simp add: cd_box_demod_subid_var h0 h1)
+  also have "\<dots> = (q \<le> \<top> \<cdot> p \<leftarrow> x)"
+    by (simp add: local.fres_galois)
+  also have "\<dots> = (q \<le> 1 \<sqinter> (\<top> \<cdot> p \<leftarrow> x))"
+    by (simp add: h1)
+  also have "\<dots> = (q \<le> cd (\<top> \<cdot> p \<leftarrow> x))"
+    by (simp add: cd_fres_prop h0)
+  finally have "(q \<le> cd_box x p) = (q \<le> cd (\<top> \<cdot> p \<leftarrow> x))".}
+  hence "\<forall>y. y \<le> cd_box x p \<longleftrightarrow> y \<le> cd (\<top> \<cdot> p \<leftarrow> 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 \<le> 1 \<Longrightarrow> cd_box x p = 1 \<sqinter> (\<top> \<cdot> p \<leftarrow> x)"
+  by (simp add: cd_fres_prop fres_cd_box)
+
+lemma fres_cd_box_top: "p \<le> 1 \<Longrightarrow> \<top> \<cdot> cd_box x p = \<top> \<cdot> p \<leftarrow> x"
+  using cd_top2 fres_cd_box by auto
+
+
+text \<open>Next we show that the box operators act on the complete Heyting algebra of subidentities.\<close>
+
+lemma cd_box_act:
+  assumes "p \<le> 1"
+  shows "cd_box (x \<cdot> y) p = cd_box x (cd_box y p)"
+proof-
+  {fix q
+    assume a: "q \<le> 1"
+    hence "(q \<le> cd_box (x \<cdot> y) p) = (cd_dia (x \<cdot> y) q \<le> p)"
+      by (simp add: assms cd_dia_cd_box_galois)
+    also have "\<dots> = (cd_dia y (cd_dia x q) \<le> p)"
+      by (simp add: local.dmq.coddual.dqmsr.fdia_mult)
+    also have "\<dots> = (cd_dia x q \<le> cd_box y p)"
+      using assms cd_dia_cd_box_galois cd_top dmq.coddual.dqmsr.fd_def by force
+    also have "\<dots> = (q \<le> cd_box x (cd_box y p))"
+      by (simp add: a assms cd_dia_cd_box_galois local.cd_box_subid)
+    finally have "(q \<le> cd_box (x \<cdot> y) p) = (q \<le> 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 \<le> 1"
+  shows "do_box (x \<cdot> 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 \<open>Next we show that the box operators are Sup reversing in the first and Inf preserving 
+in the second argument.\<close>
+
+lemma do_box_sup_inf: "p \<le> 1 \<Longrightarrow> do_box (x \<squnion> y) p = do_box x p \<cdot> do_box y p"
+proof-
+  assume h1: "p \<le> 1" 
+  {fix q
+  assume h2: "q \<le> 1"
+  hence "(q \<le> do_box (x \<squnion> y) p) = (do_dia (x \<squnion> y) q \<le> p)"
+    by (simp add: do_dia_do_box_galois h1)
+  also have "\<dots> = (do_dia x q \<le> p \<and> do_dia y q \<le> p)"
+    by (simp add: dmq.dqmsr.fdia_add2)
+  also have "\<dots> = (q \<le> do_box x p \<and> q \<le> do_box y p)"
+    by (simp add: do_dia_do_box_galois h1 h2)
+  also have "\<dots> = (q \<le> do_box x p \<cdot> do_box y p)"
+    by (simp add: do_box_subid subid_mult_meet)
+  finally have "(q \<le> do_box (x \<squnion> y) p) = (q \<le> do_box x p \<cdot> do_box y p)".}
+  hence "\<forall>z. z \<le> do_box (x \<squnion> y) p \<longleftrightarrow> z \<le> do_box x p \<cdot> 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 \<le> 1 \<Longrightarrow> do_box (x \<squnion> y) p = do_box x p \<sqinter> do_box y p"
+  by (simp add: do_box_subid do_box_sup_inf subid_mult_meet)
+
+lemma do_box_Sup_Inf: 
+  assumes "X \<noteq> {}"
+  and "p \<le> 1"
+  shows "do_box (\<Squnion>X) p = (\<Sqinter>x \<in> X. do_box x p)"
+proof-
+  {fix q
+    assume h: "q \<le> 1"
+    hence "(q \<le> do_box (\<Squnion>X) p) = (do_dia (\<Squnion>X) q \<le> p)"
+    by (simp add: do_dia_do_box_galois assms(2))
+  also have "\<dots> = ((\<Squnion>x \<in> X. do_dia x q) \<le> p)"
+    using do_dia_Sup by force
+  also have "\<dots> = (\<forall>x \<in> X. do_dia x q \<le> p)"
+    by (simp add: local.SUP_le_iff)
+  also have "\<dots> = (\<forall>x \<in> X. q \<le> do_box x p)"
+    using do_dia_do_box_galois assms(2) h by blast
+  also have "\<dots> = (q \<le> (\<Sqinter>x \<in> X. do_box x p))"
+    by (simp add: local.le_INF_iff)
+  finally have "(q \<le> do_box (\<Squnion>X) p) = (q \<le> (\<Sqinter>x \<in> X. do_box x p))".}
+  hence "\<forall>y. y \<le> do_box (\<Squnion>X) p \<longleftrightarrow> y \<le> (\<Sqinter>x \<in> 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 \<noteq> {}"
+  and "\<forall>p \<in> P. p \<le> 1"
+  shows "do_box x (\<Sqinter>P) = (\<Sqinter>p \<in> P. do_box x p)"
+proof-
+  have h0: "(\<Sqinter>p \<in> P. do_box x p) \<le> 1"
+  by (meson all_not_in_conv assms(1) do_box_subid local.INF_lower2)
+  {fix q
+    assume h1: "q \<le> 1"
+    hence "(q \<le> do_box x (\<Sqinter>P)) = (do_dia x q \<le> \<Sqinter>P)"
+      by (simp add: assms do_dia_do_box_galois local.Inf_less_eq)
+    also have "\<dots> = (\<forall>p \<in> P. do_dia x q \<le> p)"
+      using local.le_Inf_iff by blast
+    also have "\<dots> = (\<forall>p \<in> P. q \<le> do_box x p)"
+      using assms(2) do_dia_do_box_galois h1 by auto
+    also have "\<dots> = (q \<le> (\<Sqinter>p \<in> P. do_box x p))"
+      by (simp add: local.le_INF_iff)
+    finally have "(q \<le> do_box x (\<Sqinter>P)) = (q \<le> (\<Sqinter>p \<in> 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 \<le> 1 \<Longrightarrow> cd_box (x \<squnion> y) p = cd_box x p \<cdot> 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 \<le> 1 \<Longrightarrow> cd_box (x \<squnion> y) p = cd_box x p \<sqinter> cd_box y p"
+  by (simp add: cd_box_subid cd_box_sup_inf subid_mult_meet)
+
+lemma cd_box_Sup_Inf: 
+  assumes "X \<noteq> {}"
+  and "p \<le> 1"
+shows "cd_box (\<Squnion>X) p = (\<Sqinter>x \<in> X. cd_box x p)"
+proof-
+  have "cd_box (\<Squnion>X) p = do_box ((\<Squnion>X)\<^sup>\<circ>) p"
+    using assms(2) do_box_cd_box_conv by presburger
+  also have "\<dots> = (\<Sqinter>y \<in> {x\<^sup>\<circ>|x. x \<in> X}. do_box y p)"
+    by (simp add: Setcompr_eq_image assms do_box_Sup_Inf)
+  also have "\<dots> = (\<Sqinter>x \<in> X. do_box (x\<^sup>\<circ>) p)"
+    by (simp add: Setcompr_eq_image image_image)
+  also have "\<dots> = (\<Sqinter>x \<in> 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 \<noteq> {}"
+  and "\<forall>p \<in> P. p \<le> 1"
+shows "cd_box x (\<Sqinter>P) = (\<Sqinter>p \<in> P. cd_box x p)"
+proof-
+  have "cd_box x (\<Sqinter>P) = do_box (x\<^sup>\<circ>) (\<Sqinter>P)"
+    by (simp add: assms do_box_cd_box_conv local.Inf_less_eq)
+  also have "\<dots> = (\<Sqinter>p \<in> P. do_box (x\<^sup>\<circ>) p)"
+    using assms do_box_Sup_Inf2 by presburger
+  also have "\<dots> = (\<Sqinter>p \<in> P. cd_box x p)"
+    using assms(2) do_box_cd_box_conv by force
+  finally show ?thesis.
+qed
+
+text \<open>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.\<close>
+
+definition "ado x = \<Squnion>{p. p \<cdot> x = \<bottom> \<and> p \<le> 1}"
+
+definition "acd x = \<Squnion>{p. x \<cdot> p = \<bottom> \<and> p \<le> 1}"
+
+lemma ado_acd: "ado (x\<^sup>\<circ>) = 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\<^sup>\<circ>) = 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 \<cdot> x = \<bottom>"
+  unfolding ado_def
+  using dmq.coddual.Sup_distl by auto
+
+lemma acd_right_zero [simp]: "x \<cdot> acd x = \<bottom>"
+  unfolding acd_def
+  by (simp add: dmq.coddual.h_Sup local.dual_order.antisym)
+
+lemma ado_greatest: "p \<le> 1 \<Longrightarrow> p \<cdot> x = \<bottom> \<Longrightarrow> p \<le> ado x"
+  by (simp add: ado_def local.Sup_upper)
+
+lemma acd_greatest: "p \<le> 1 \<Longrightarrow> x \<cdot> p = \<bottom> \<Longrightarrow> p \<le> acd x"
+  by (simp add: acd_def local.Sup_upper)
+
+lemma ado_subid: "ado x \<le> 1"
+  using ado_def local.Sup_le_iff by force
+
+lemma acd_subid: "acd x \<le> 1"
+  by (simp add: acd_def local.Sup_le_iff)
+
+lemma ado_left_zero_iff: "p \<le> 1 \<Longrightarrow> (p \<le> ado x) = (p \<cdot> x = \<bottom>)"
+  by (metis ado_greatest ado_left_zero local.bot_unique local.mult_isor)
+
+lemma acd_right_zero_iff: "p \<le> 1 \<Longrightarrow> (p \<le> acd x) = (x \<cdot> p = \<bottom>)"
+  by (metis acd_greatest acd_right_zero local.bot_unique local.mult_isol)
+
+text \<open>This gives an eqational characterisation of antidomain and anticodomain.\<close>
+
+lemma ado_cd_bot: "ado x = cd (\<bottom> \<leftarrow> x)"
+proof-
+  {fix p
+  assume  h: "p \<le> 1"
+  hence "(p \<le> ado x) = (p \<cdot> x = \<bottom>)"
+    by (simp add: ado_left_zero_iff) 
+  also have "\<dots> = (p \<le> \<bottom> \<leftarrow> x)"
+    using local.bot_unique local.fres_galois by blast
+  also have "\<dots> = (p \<le> 1 \<sqinter> (\<bottom> \<leftarrow> x))"
+    by (simp add: h)
+  also have "\<dots> = (p \<le> cd (\<bottom> \<leftarrow> x))"
+    by (metis cd_fres_prop local.bot_least local.mult_botr)
+  finally have "(p \<le> ado x) = (p \<le> cd (\<bottom> \<leftarrow> x))".}
+  hence "\<forall>y. y \<le> ado x \<longleftrightarrow> y \<le> cd (\<bottom> \<leftarrow> 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 \<rightarrow> \<bottom>)"
+  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 \<sqinter> (\<bottom> \<leftarrow> 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 \<sqinter> (x \<rightarrow> \<bottom>)"
+  by (metis acd_do_bot do_bres_prop local.bot_least local.mult_botl)
+
+lemma ado_cd_bot_var: "ado x = cd (\<bottom> \<leftarrow> 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 \<rightarrow> \<bottom>)"
+  by (metis acd_do_bot cd_top2 local.bres_curry local.bres_top_bot)
+
+lemma ado_do_bot: "ado x = do (do x \<rightarrow> \<bottom>)"
+  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 (\<bottom> \<leftarrow> cd x)"
+  by (metis ado_acd ado_cd_bot_var local.cd_inv local.inv_invol)
+
+lemma ado_do_bot_var: "ado x = 1 \<sqinter> (do x \<rightarrow> \<bottom>)"
+  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 \<sqinter> (\<bottom> \<leftarrow> cd x)"
+   by (metis acd_cd_bot acd_right_zero cd_top local.fres_top_top2)
+
+
+text \<open>Domain and codomain are compatible with the boxes.\<close>
+
+lemma cd_box_ado: "cd_box x \<bottom> = ado x"
+  by (simp add: ado_cd_bot fres_cd_box)
+
+lemma do_box_acd: "do_box x \<bottom> = acd x"
+  by (simp add: acd_do_bot bres_do_box)
+
+lemma ado_subid_prop: "p \<le> 1 \<Longrightarrow> ado p = 1 \<sqinter> (p \<rightarrow> \<bottom>)"
+  by (metis ado_do_bot_var do_fix_subid)
+
+lemma ado_do: "p \<le> 1 \<Longrightarrow> ado p = do (p \<rightarrow> \<bottom>)"
+  using ado_do_bot do_fix_subid by force
+
+lemma ado_do_compl: "ado x \<cdot> do x = \<bottom>"
+  using dmq.dqmsr.dom_weakly_local by force
+
+lemma "ado x \<squnion> do x = \<top>" (* nitpick[expect = genuine]*)
+  oops
+
+lemma "\<forall>x p. \<exists>f. 1 \<sqinter> (\<top> \<cdot> p \<leftarrow> x) = 1 \<sqinter> (\<bottom> \<leftarrow> (x \<rightarrow> p \<cdot> \<top>))" (* nitpick[expect=genuine]*)
+  oops
+
+lemma "cd_box x p = ado (x \<cdot> ado p)" (* nitpick[expect=genuine]*)
+  oops
+
+lemma ad_do_bot [simp]: "(1 \<sqinter> (do x \<rightarrow> \<bottom>)) \<cdot> do x = \<bottom>"
+  using ado_do_bot_var ado_left_zero dmq.dqmsr.dom_weakly_local by presburger
+ 
+lemma do_heyting_galois: "(do x \<cdot> do y \<le> do z) = (do x \<le> 1 \<sqinter> (do y \<rightarrow> 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 \<cdot> do y \<le> do z) = (do x \<le> 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 \<open>Antidomain is therefore Heyting negation.\<close>
+
+lemma ado_heyting_negation: "ado (do x) = cd_box (do x) \<bottom>"
+  by (simp add: cd_box_ado)
+
+lemma ad_ax1 [simp]: "(1 \<sqinter> (do x \<rightarrow> \<bottom>)) \<cdot> x = \<bottom>"
+  by (simp add: local.dmq.dqmsr.dom_weakly_local)
+
+lemma "1 \<sqinter> (do (1 \<sqinter> (do x \<rightarrow> \<bottom>)) \<rightarrow> \<bottom>) = do x" (* nitpick[expect=genuine]*)
+  oops
+
+lemma "p \<le> 1 \<Longrightarrow> do_dia x p = 1 \<sqinter> (cd_box x (1 \<sqinter> (p \<rightarrow> \<bottom>)) \<rightarrow> \<bottom>)" (* nitpick[expect=genuine]*)
+  oops
+
+lemma  "p \<le> 1 \<Longrightarrow> cd_box x p = 1 \<sqinter> (do_dia x (1 \<sqinter> (p \<rightarrow> \<bottom>)) \<rightarrow> \<bottom>)" (* nitpick[expect=genuine]*)
+  oops
+
+lemma "p \<le> 1 \<Longrightarrow> cd_dia x p = 1 \<sqinter> (do_box x (1 \<sqinter> (p \<rightarrow> \<bottom>)) \<rightarrow> \<bottom>)" (* nitpick[expect=genuine]*)
+  oops
+
+lemma "p \<le> 1 \<Longrightarrow> do_box x p = 1 \<sqinter> (cd_dia x (1 \<sqinter> (p \<rightarrow> \<bottom>)) \<rightarrow> \<bottom>)" (* nitpick[expect=genuine]*)
+  oops
+
+end
+
+subsection \<open>Boolean Dedekind quantales\<close>
+
+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) \<cdot> do x = \<bottom>"
+  by (simp add: local.diff_eq local.inf_shunt local.subid_mult_meet)
+
+lemma ad_ax1 [simp]: "(1 - do x) \<cdot> x = \<bottom>"
+  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 "\<dots> = 1 \<sqinter> -(1 \<sqinter> - do x)"
+    by (simp add: local.diff_eq)
+  also have "\<dots> = do x"
+    by (simp add: local.chaq.wswq.distrib_left local.do_top)
+  finally show ?thesis.
+qed
+
+lemma ad_ax2: "1 - do (x \<cdot> y) \<squnion> (1 - do (x \<cdot> (1 - do (1 - do y)))) = 1 - do (x \<cdot> (1 - do (1 - do y)))"
+  by simp
+
+lemma ad_ax3 [simp]: "do x \<squnion> (1 - do x) = 1"
+proof-
+  have "do x \<squnion> (1 - do x) = do x \<squnion> (1 \<sqinter> -do x)"
+    using local.diff_eq by force
+  also have "\<dots> = 1 \<sqinter> (do x \<squnion> -do x)"
+    by (simp add: local.chaq.wswq.distrib_left local.do_top)
+  also have "\<dots> = 1"
+    by simp
+  finally show ?thesis.
+qed
+
+sublocale bdad: antidomain_semiring "\<lambda>x. 1 - do x" "(\<squnion>)" "(\<cdot>)" 1 \<bottom> _ _ 
+  by unfold_locales simp_all
+
+sublocale bdadka: antidomain_kleene_algebra "\<lambda>x. 1 - do x" "(\<squnion>)" "(\<cdot>)" 1 \<bottom> _ _ qstar..
+
+sublocale bdar: antirange_semiring "(\<squnion>)" "(\<cdot>)" 1 \<bottom> "\<lambda>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 "(\<squnion>)" "(\<cdot>)" 1 \<bottom> _ _ qstar "\<lambda>x. 1 - cd x"..
+
+sublocale bmod: modal_semiring_simp "\<lambda>x. 1 - do x" "(\<squnion>)" "(\<cdot>)" 1 \<bottom> _ _ "\<lambda>x. 1 - cd x"..
+
+sublocale bmod: modal_kleene_algebra_simp "(\<squnion>)" "(\<cdot>)" 1 \<bottom> _ _ qstar "\<lambda>x. 1 - do x" "\<lambda>x. 1 - cd x"..
+
+lemma inv_neg: "(-x)\<^sup>\<circ> = -(x\<^sup>\<circ>)"
+  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\<^sup>\<circ> \<cdot> -(x \<cdot> y) \<le> -y"
+  by (metis local.inf.commute local.inf_compl_bot local.inf_shunt local.schroeder_1)
+
+lemma bres_prop: "x \<rightarrow> y = -(x\<^sup>\<circ> \<cdot> -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 \<leftarrow> y = -(-x \<cdot> y\<^sup>\<circ>)"
+  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 \<le> 1 \<Longrightarrow> 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 \<le> 1 \<Longrightarrow> 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 \<le> 1 \<Longrightarrow> 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 \<le> 1 \<Longrightarrow> 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 \<le> 1 \<Longrightarrow> do_box x p = bdar.bbox x p"
+proof-
+  assume a: "p \<le> 1"
+  {fix q
+  assume b: "q \<le> 1"
+  hence "(q \<le> do_box x p) = (x \<cdot> q \<le> p \<cdot> x)"
+    by (simp add: a local.do_box_demod_subid)
+  also have "\<dots> = (x \<cdot> cd q \<le> cd p \<cdot> x)"
+    by (metis a b local.cd_fix_subid)
+  also have "\<dots> = (cd q \<le> 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 "\<dots> = (q \<le> bdar.bbox x p)"
+    using b local.cd_fix_subid by force
+  finally have "(q \<le> do_box x p) = (q \<le> 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 \<le> 1 \<Longrightarrow> 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 \<le> 1 \<Longrightarrow> 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 \<le> 1 \<Longrightarrow> 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 \<le> 1 \<Longrightarrow> 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 \<le> 1 \<Longrightarrow> 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 "(\<squnion>)" "(\<cdot>)" 1 \<bottom> "(\<le>)" "(<)" qstar invol dom cod..
+
+lemma do_approx_dom: "do x \<le> dom x"
+proof -
+  have "do x = dom (do x) \<cdot> do x"
+    by simp
+  also have "\<dots> \<le> dom (1 \<sqinter> (x \<cdot> x\<^sup>\<circ>))"
+    by (simp add: local.do_def local.dqmsr.domain_subid)
+  also have "\<dots> \<le> dom 1 \<sqinter> dom (x \<cdot>  x\<^sup>\<circ>)"
+    using local.dom_meet_sub by presburger
+  also have "\<dots> \<le> dom (x \<cdot> dom (x\<^sup>\<circ>))"
+    by simp
+  also have "\<dots> \<le> 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 \<subseteq> invmqmka: dr_modal_kleene_algebra_converse  "(\<squnion>)" "(\<cdot>)" 1 \<bottom> "(\<le>)" "(<)" qstar invol dom cod..
+
+class dc_modal_quantale_strong_converse = dc_involutive_modal_quantale +  
+  assumes weak_dom_def: "dom x \<le> x \<cdot> x\<^sup>\<circ>"
+  and weak_cod_def: "cod x \<le> x\<^sup>\<circ> \<cdot> x"
+
+begin
+
+sublocale invmqmka: dr_modal_kleene_algebra_strong_converse  "(\<squnion>)" "(\<cdot>)" 1 \<bottom> "(\<le>)" "(<)" qstar invol dom cod
+  by (unfold_locales, simp_all add: local.weak_dom_def local.weak_cod_def)
+
+lemma dom_def: "dom x = 1 \<sqinter> (x \<cdot> x\<^sup>\<circ>)"
+  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 \<sqinter> (x\<^sup>\<circ> \<cdot> 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 \<le> 1 \<Longrightarrow> p \<cdot> p = p"
+  by (simp add: local.subid_mult_meet)
+
+lemma subid_comm: "p \<le> 1 \<Longrightarrow> q \<le> 1 \<Longrightarrow> p \<cdot> q = q \<cdot> p"
+  using local.inf.commute local.subid_mult_meet by force
+
+lemma subid_meet_comp: "p \<le> 1 \<Longrightarrow> q \<le> 1 \<Longrightarrow> p \<sqinter> q = p \<cdot> q"
+  by (simp add: local.subid_mult_meet)
+
+lemma subid_dom: "p \<le> 1 \<Longrightarrow> dom p = p"
+proof-
+  assume h: "p \<le> 1"
+  have a: "p \<squnion> (1 \<sqinter> -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 \<sqinter> -p) \<sqinter> p = \<bottom>"
+    by (simp add: local.inf.commute)
+  hence "dom p = (p \<squnion> (1 \<sqinter> -p)) \<cdot> dom p"
+    by (simp add: a)
+  also have "\<dots> = p \<cdot> dom p \<squnion> dom ((1 \<sqinter> -p) \<cdot> dom p) \<cdot> (1 \<sqinter> -p) \<cdot> dom p"
+    using local.dqmsr.dsg1 local.wswq.distrib_right mult_assoc by presburger
+  also have "\<dots> \<le> p \<squnion> dom ((1 \<sqinter> -p) \<cdot> 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 "\<dots> = p \<squnion> dom ((1 \<sqinter> -p) \<cdot> p)"
+    by simp
+  also have "\<dots> = p \<squnion> dom \<bottom>"
+    using b h subid_meet_comp by fastforce
+  also have "\<dots> = p"
+    by simp
+  finally have "dom p \<le> p".
+  thus ?thesis
+    using h local.dqmsr.domain_subid local.dual_order.antisym by presburger
+qed
+
+lemma do_prop: "(do x \<le> do y) = (x \<le> do y \<cdot> \<top>)"
+  by (simp add: local.lla)
+
+lemma do_lla: "(do x \<le> do y) = (x \<le> do y \<cdot> x)"
+  by (simp add: local.lla_var)
+
+lemma lla_subid: "p \<le> 1 \<Longrightarrow> ((dom x \<le> p) = (x \<le> p \<cdot> x))"
+  by (metis local.dqmsr.dom_llp subid_dom)
+
+lemma dom_do: "dom x = do x"
+proof-
+  have "x \<le> do x \<cdot> x"
+    by simp
+  hence "dom x \<le> 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
+
diff --git a/thys/Quantales_Converse/ROOT b/thys/Quantales_Converse/ROOT
new file mode 100644
--- /dev/null
+++ b/thys/Quantales_Converse/ROOT
@@ -0,0 +1,20 @@
+chapter AFP
+
+session "Quantales_Converse" (AFP) = HOL +
+  options [timeout = 600]
+
+  sessions
+   Kleene_Algebra
+   KAD 
+   Quantales 
+   
+  theories
+    Modal_Kleene_Algebra_Var
+    Kleene_Algebra_Converse
+    Modal_Kleene_Algebra_Converse
+    Modal_Quantale
+    Quantale_Converse
+    
+  document_files
+   "root.tex"
+   "root.bib"
diff --git a/thys/Quantales_Converse/document/root.bib b/thys/Quantales_Converse/document/root.bib
new file mode 100644
--- /dev/null
+++ b/thys/Quantales_Converse/document/root.bib
@@ -0,0 +1,126 @@
+@article{ArmstrongSW13,
+  author       = {Alasdair Armstrong and
+                  Georg Struth and
+                  Tjark Weber},
+  title        = {Kleene Algebra},
+  journal      = {Archive of Formal Proofs},
+  year         = {2013},
+  url          = {https://www.isa-afp.org/entries/Kleene\_Algebra.shtml},
+  timestamp    = {Mon, 25 May 2020 09:13:27 +0200},
+  biburl       = {https://dblp.org/rec/journals/afp/ArmstrongSW13.bib},
+  bibsource    = {dblp computer science bibliography, https://dblp.org}
+}
+
+@article{CalkGMS22,
+  author       = {Cameron Calk and
+                  Eric Goubault and
+                  Philippe Malbos and
+                  Georg Struth},
+  title        = {Algebraic coherent confluence and higher globular {K}leene algebras},
+  journal      = {Logical Methods in Computer Science},
+  volume       = {18},
+  number       = {4},
+  year         = {2022},
+  url          = {https://doi.org/10.46298/lmcs-18(4:9)2022},
+  doi          = {10.46298/lmcs-18(4:9)2022},
+  timestamp    = {Tue, 24 Jan 2023 10:48:24 +0100},
+  biburl       = {https://dblp.org/rec/journals/lmcs/CalkGMS22.bib},
+  bibsource    = {dblp computer science bibliography, https://dblp.org}
+}
+
+@article{CalkMPS23,
+Author = {Cameron Calk and Philippe Malbos and Damien Pous and Georg Struth},
+Title = {Higher Catoids, Higher Quantales and their Correspondences},
+Year = {2023},
+journal = {arXiv},
+volume = {2307.09253},
+}
+
+@article{FahrenbergJSZ23,
+  author    = {Fahrenberg, Uli and
+               Johansen, Christian and
+               Struth, Georg and
+               Ziemia{\'n}ski, Krzysztof},
+  title     = {Catoids and Modal Convolution Algebras},
+  journal   = {Algebra Universalis},
+  volume = {84},
+  pages = {10},
+  year      = {2023}
+}
+
+@article{GomesGHSW16,
+  author       = {Victor B. F. Gomes and
+                  Walter Guttmann and
+                  Peter H{\"{o}}fner and
+                  Georg Struth and
+                  Tjark Weber},
+  title        = {Kleene Algebras with Domain},
+  journal      = {Archive of Formal Proofs},
+  year         = {2016},
+  url          = {https://www.isa-afp.org/entries/KAD.shtml},
+  timestamp    = {Mon, 25 May 2020 09:13:24 +0200},
+  biburl       = {https://dblp.org/rec/journals/afp/GomesGHSW16.bib},
+  bibsource    = {dblp computer science bibliography, https://dblp.org}
+}
+
+@inproceedings{GomesS16,
+  author       = {Victor B. F. Gomes and Georg Struth},
+  title        = {Modal {K}leene Algebra Applied to Program Correctness},
+  booktitle    = {{FM} 2016},
+  series       = {LNCS},
+  volume       = {9995},
+  pages        = {310--325},
+  year         = {2016},
+  url          = {https://doi.org/10.1007/978-3-319-48989-6\_19},
+  doi          = {10.1007/978-3-319-48989-6\_19},
+  timestamp    = {Tue, 14 May 2019 10:00:46 +0200},
+  biburl       = {https://dblp.org/rec/conf/fm/GomesS16.bib},
+  bibsource    = {dblp computer science bibliography, https://dblp.org}
+}
+
+@Unpublished{PousS23,
+  author = 	 {Damien Pous and Georg Struth},
+  title = 	 {Dedekind Quantaloids as Intuitionistic Modal Algebras},
+  note = 	 {In preparation},
+  year = 	 2023}
+
+@Article{Resende18,
+  author = 	 {Pedro Resende},
+  title = 	 {Open Maps of Involutive Quantales},
+  journal = 	 {Applied Categorical Structures},
+  year = 	 2018,
+  volume = 	 26,
+  pages = 	 {631-644}}
+
+@Book{Rosenthal90,
+  author = 	 {Rosenthal, Kimmo. I.},
+  title = 	 {Quantales and Their Applications},
+  publisher = 	 {Longman Scientific $\&$ Technical},
+  year = 	 1990}
+
+@Book{Rosenthal96,
+  author = 	 {Rosenthal, K. I.},
+  title = 	 {The Theory of Quantaloids},
+  publisher = 	 {Addison Wesley Longman Limited},
+  year = 	 1996}
+
+@article{Struth18,
+  author       = {Georg Struth},
+  title        = {Quantales},
+  journal      = {Archive of Formal Proofs},
+  year         = {2018},
+  url          = {https://www.isa-afp.org/entries/Quantales.html},
+  timestamp    = {Mon, 25 May 2020 09:13:16 +0200},
+  biburl       = {https://dblp.org/rec/journals/afp/Struth18a.bib},
+  bibsource    = {dblp computer science bibliography, https://dblp.org}
+}
+
+@Article{Tarski41,
+  author = 	 {Alfred Tarski},
+  title = 	 {On the Calculus of Relations},
+  journal = 	 {Journal of Symbolic Logic},
+  year = 	 1941,
+  volume = 	 6,
+  number = 	 3,
+  pages = 	 {73--89}}
+
diff --git a/thys/Quantales_Converse/document/root.tex b/thys/Quantales_Converse/document/root.tex
new file mode 100644
--- /dev/null
+++ b/thys/Quantales_Converse/document/root.tex
@@ -0,0 +1,121 @@
+\documentclass[11pt,a4paper]{article}
+\usepackage[T1]{fontenc}
+\usepackage{isabelle,isabellesym}
+
+% further packages required for unusual symbols (see also
+% isabellesym.sty), use only when needed
+
+%\usepackage{amssymb}
+  %for \<leadsto>, \<box>, \<diamond>, \<sqsupset>, \<mho>, \<Join>,
+  %\<lhd>, \<lesssim>, \<greatersim>, \<lessapprox>, \<greaterapprox>,
+  %\<triangleq>, \<yen>, \<lozenge>
+
+%\usepackage{eurosym}
+  %for \<euro>
+
+\usepackage[only,bigsqcap,bigparallel,fatsemi,interleave,sslash]{stmaryrd}
+  %for \<Sqinter>, \<Parallel>, \<Zsemi>, \<Parallel>, \<sslash>
+
+%\usepackage{eufrak}
+  %for \<AA> ... \<ZZ>, \<aa> ... \<zz> (also included in amssymb)
+
+%\usepackage{textcomp}
+  %for \<onequarter>, \<onehalf>, \<threequarters>, \<degree>, \<cent>,
+  %\<currency>
+
+% this should be the last package used
+\usepackage{pdfsetup}
+
+% urls in roman style, theory text in math-similar italics
+\urlstyle{rm}
+\isabellestyle{it}
+
+% for uniform font size
+%\renewcommand{\isastyle}{\isastyleminor}
+
+\begin{document}
+
+\title{Modal quantales, involutive Quantales, Dedekind Quantales}
+\author{Cameron Calk and Georg Struth}
+\maketitle
+
+\begin{abstract}
+  This AFP entry provides mathematical components for modal quantales,
+  involutive quantales and Dedekind quantales. Modal quantales are
+  simple extensions of modal Kleene algebras useful for the
+  verification of recursive programs. Involutive quantales appear in
+  the study of $C^\ast$-algebras. Dedekind quantales are relatives of
+  Tarski's relation algebras, hence relevant to program verification
+  and beyond that to higher  rewriting. We also provide
+  components for weaker variants such as Kleene algebras with converse
+  and modal Kleene algebras with converse.
+\end{abstract}
+
+\tableofcontents
+
+% sane default for proof documents
+\parindent 0pt\parskip 0.5ex
+
+% generated text of all theories
+
+\section{Introductory Remarks}
+
+In this AFP entry we provide mathematical components for modal
+quantales, involutive quantales and Dedekind quantales. Modal
+quantales are simple extensions of modal Kleene algebras that can be
+used in the verification of recursive
+programs~\cite{GomesS16}. Involutive quantales appear in the study of
+$C^\ast$-algebras~\cite{Resende18}. Dedekind quantales,
+categorifications of which are known as \emph{modular
+  quantaloids}~\cite{Rosenthal96}, are relatives of Tarski's relation
+algebras~\cite{Tarski41}, and hence relevant to program verification
+as well. We also provide components for weaker variants such as Kleene
+algebras and modal Kleene algebras with converse.
+
+Our main interest in these structures comes from recent applications
+in higher-dimensional rewriting~\cite{CalkGMS22,CalkMPS23}, where they
+are used in coherence proofs for rewriting systems based on computads
+or polygraphs. This includes proofs of coherent Church-Rosser theorems
+and coherent Newman's lemmas. A more long-term programme considers
+the formalisation of algebraic aspects of higher rewriting with proof
+assistants.
+
+  Modal quantales have previously been studied
+  in~\cite{FahrenbergJSZ23}, where it is shown, for instance, that any
+  category can be lifted to a modal quantale at powerset level. Such
+  lifting results will be formalised in a companion AFP entry.
+
+  Dedekind quantales give also rise to intuitionistic modal algebras,
+  as the results in this AFP entry show. In particular, the set of all
+  subidentities or coreflexives of a Dedekind quantale forms a
+  complete Heyting algebra (aka frame or locale), on which modal box
+  and diamond operators can be defined. A paper explaining these
+  results is in preparation~\cite{PousS23}. A further application of
+  Dedekind quantales lies once again in higher-dimensional
+  rewriting~\cite{CalkGMS22,CalkMPS23}. Any groupoid, in particular,
+  can be lifted to a Dedekind quantale at powerset level, a result
+  which will once again be formalised in a companion AFP entry.
+
+  Our components build on extant AFP components for Kleene
+  algebras~\cite{ArmstrongSW13}, modal Kleene
+  algebras~\cite{GomesGHSW16} and quantales~\cite{Struth18}.
+
+  \vspace{\baselineskip}
+
+  Georg Struth is grateful for an invited professorship at École
+  polytechnique and a fellowship at the Collegium de Lyon, Institute
+  of Advanced Study, during which most of this formalisation work
+  has been done.
+
+\input{session}
+
+% optional bibliography
+\bibliographystyle{abbrv}
+\bibliography{root}
+
+\end{document}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: t
+%%% End:
diff --git a/thys/ROOTS b/thys/ROOTS
--- a/thys/ROOTS
+++ b/thys/ROOTS
@@ -1,757 +1,758 @@
 ABY3_Protocols
 ADS_Functor
 AI_Planning_Languages_Semantics
 AODV
 AOT
 AVL-Trees
 AWN
 Abortable_Linearizable_Modules
 Abs_Int_ITP2012
 Abstract-Hoare-Logics
 Abstract-Rewriting
 Abstract_Completeness
 Abstract_Soundness
 Ackermanns_not_PR
 Actuarial_Mathematics
 Adaptive_State_Counting
 Affine_Arithmetic
 Aggregation_Algebras
 Akra_Bazzi
 Algebraic_Numbers
 Algebraic_VCs
 Allen_Calculus
 Amicable_Numbers
 Amortized_Complexity
 AnselmGod
 Applicative_Lifting
 Approximation_Algorithms
 Architectural_Design_Patterns
 Aristotles_Assertoric_Syllogistic
 Arith_Prog_Rel_Primes
 ArrowImpossibilityGS
 Attack_Trees
 Auto2_HOL
 Auto2_Imperative_HOL
 AutoFocus-Stream
 Automated_Stateful_Protocol_Verification
 Automatic_Refinement
 AxiomaticCategoryTheory
 BDD
 BD_Security_Compositional
 BNF_CC
 BNF_Operations
 BTree
 Balog_Szemeredi_Gowers
 Banach_Steinhaus
 Belief_Revision
 Bell_Numbers_Spivey
 BenOr_Kozen_Reif
 Berlekamp_Zassenhaus
 Bernoulli
 Bertrands_Postulate
 Bicategory
 BinarySearchTree
 Binary_Code_Imprimitive
 Binding_Syntax_Theory
 Binomial-Heaps
 Binomial-Queues
 BirdKMP
 Birkhoff_Finite_Distributive_Lattices
 Blue_Eyes
 Bondy
 Boolean_Expression_Checkers
 Boolos_Curious_Inference
 Boolos_Curious_Inference_Automated
 Bounded_Deducibility_Security
 Buchi_Complementation
 Budan_Fourier
 Buffons_Needle
 Buildings
 BytecodeLogicJmlTypes
 C2KA_DistributedSystems
 CAVA_Automata
 CAVA_LTL_Modelchecker
 CCS
 CHERI-C_Memory_Model
 CISC-Kernel
 CRDT
 CRYSTALS-Kyber
 CSP_RefTK
 CVP_Hardness
 CYK
 CZH_Elementary_Categories
 CZH_Foundations
 CZH_Universal_Constructions
 CakeML
 CakeML_Codegen
 Call_Arity
 Card_Equiv_Relations
 Card_Multisets
 Card_Number_Partitions
 Card_Partitions
 Cartan_FP
 Case_Labeling
 Catalan_Numbers
 Category
 Category2
 Category3
 Cauchy
 Cayley_Hamilton
 Certification_Monads
 Chandy_Lamport
 Chord_Segments
 Circus
 Clean
 Clique_and_Monotone_Circuits
 ClockSynchInst
 Closest_Pair_Points
 CoCon
 CoSMeDis
 CoSMed
 CofGroups
 Coinductive
 Coinductive_Languages
 Collections
 Combinable_Wands
 Combinatorial_Enumeration_Algorithms
 Combinatorics_Words
 Combinatorics_Words_Graph_Lemma
 Combinatorics_Words_Lyndon
 CommCSL
 Commuting_Hermitian
 Comparison_Sort_Lower_Bound
 Compiling-Exceptions-Correctly
 Complete_Non_Orders
 Completeness
 Complex_Bounded_Operators
 Complex_Geometry
 Complx
 ComponentDependencies
 ConcurrentGC
 ConcurrentIMP
 Concurrent_Ref_Alg
 Concurrent_Revisions
 Conditional_Simplification
 Conditional_Transfer_Rule
 Consensus_Refined
 Constructive_Cryptography
 Constructive_Cryptography_CM
 Constructor_Funs
 Containers
 Cook_Levin
 CoreC++
 Core_DOM
 Core_SC_DOM
 Correctness_Algebras
 Cotangent_PFD_Formula
 Count_Complex_Roots
 CryptHOL
 CryptoBasedCompositionalProperties
 Crypto_Standards
 Cubic_Quartic_Equations
 DCR-ExecutionEquivalence
 DFS_Framework
 DOM_Components
 DPRM_Theorem
 DPT-SAT-Solver
 DataRefinementIBP
 Datatype_Order_Generator
 Decl_Sem_Fun_PL
 Decreasing-Diagrams
 Decreasing-Diagrams-II
 Dedekind_Real
 Deep_Learning
 Delta_System_Lemma
 Density_Compiler
 Dependent_SIFUM_Refinement
 Dependent_SIFUM_Type_Systems
 Depth-First-Search
 Derangements
 Deriving
 Descartes_Sign_Rule
 Design_Theory
 Dict_Construction
 Differential_Dynamic_Logic
 Differential_Game_Logic
 DigitsInBase
 Digit_Expansions
 Dijkstra_Shortest_Path
 Diophantine_Eqns_Lin_Hom
 Dirichlet_L
 Dirichlet_Series
 DiscretePricing
 Discrete_Summation
 DiskPaxos
 Distributed_Distinct_Elements
 Dominance_CHK
 DynamicArchitectures
 Dynamic_Tables
 E_Transcendental
 Earley_Parser
 Echelon_Form
 EdmondsKarp_Maxflow
 Edwards_Elliptic_Curves_Group
 Efficient-Mergesort
 Efficient_Weighted_Path_Order
 Elliptic_Curves_Group_Law
 Encodability_Process_Calculi
 Epistemic_Logic
 Equivalence_Relation_Enumeration
 Ergodic_Theory
 Error_Function
 Euler_MacLaurin
 Euler_Partition
 Eval_FO
 Example-Submission
 Executable_Randomized_Algorithms
 Expander_Graphs
 Extended_Finite_State_Machine_Inference
 Extended_Finite_State_Machines
 FFT
 FLP
 FOL-Fitting
 FOL_Axiomatic
 FOL_Harrison
 FOL_Seq_Calc1
 FOL_Seq_Calc2
 FOL_Seq_Calc3
 FO_Theory_Rewriting
 FSM_Tests
 Factor_Algebraic_Polynomial
 Factored_Transition_System_Bounding
 Falling_Factorial_Sum
 Farkas
 FeatherweightJava
 Featherweight_OCL
 Fermat3_4
 FileRefinement
 FinFun
 Finger-Trees
 Finite-Map-Extras
 Finite_Automata_HF
 Finite_Fields
 Finitely_Generated_Abelian_Groups
 First_Order_Terms
 First_Welfare_Theorem
 Fishburn_Impossibility
 Fisher_Yates
 Fishers_Inequality
 Flow_Networks
 Floyd_Warshall
 Flyspeck-Tame
 FocusStreamsCaseStudies
 Forcing
 Formal_Puiseux_Series
 Formal_SSA
 Formula_Derivatives
 Foundation_of_geometry
 Fourier
 Free-Boolean-Algebra
 Free-Groups
 Frequency_Moments
 Fresh_Identifiers
 FunWithFunctions
 FunWithTilings
 Functional-Automata
 Functional_Ordered_Resolution_Prover
 Furstenberg_Topology
 GPU_Kernel_PL
 Gabow_SCC
 GaleStewart_Games
 Gale_Shapley
 Game_Based_Crypto
 Gauss-Jordan-Elim-Fun
 Gauss_Jordan
 Gauss_Sums
 Gaussian_Integers
 GenClock
 General-Triangle
 Generalized_Counting_Sort
 Generic_Deriving
 Generic_Join
 GewirthPGCProof
 Girth_Chromatic
 Given_Clause_Loops
 GoedelGod
 Goedel_HFSet_Semantic
 Goedel_HFSet_Semanticless
 Goedel_Incompleteness
 Goodstein_Lambda
 GraphMarkingIBP
 Graph_Saturation
 Graph_Theory
 Gray_Codes
 Green
 Groebner_Bases
 Groebner_Macaulay
 Gromov_Hyperbolicity
 Grothendieck_Schemes
 Group-Ring-Module
 HOL-CSP
 HOLCF-Prelude
 HRB-Slicing
 Hahn_Jordan_Decomposition
 Hales_Jewett
 Heard_Of
 Hello_World
 HereditarilyFinite
 Hermite
 Hermite_Lindemann
 Hidden_Markov_Models
 Higher_Order_Terms
 HoareForDivergence
 Hoare_Time
 Hood_Melville_Queue
 HotelKeyCards
 Huffman
 Hybrid_Logic
 Hybrid_Multi_Lane_Spatial_Logic
 Hybrid_Systems_VCs
 HyperCTL
 HyperHoareLogic
 Hyperdual
 IEEE_Floating_Point
 IFC_Tracking
 IMAP-CRDT
 IMO2019
 IMP2
 IMP2_Binary_Heap
 IMP_Compiler
 IMP_Compiler_Reuse
 IP_Addresses
 Imperative_Insertion_Sort
 Implicational_Logic
 Impossible_Geometry
 Incompleteness
 Incredible_Proof_Machine
 Independence_CH
 Inductive_Confidentiality
 Inductive_Inference
 InfPathElimination
 InformationFlowSlicing
 InformationFlowSlicing_Inter
 Integration
 Interpolation_Polynomials_HOL_Algebra
 Interpreter_Optimizations
 Interval_Arithmetic_Word32
 Intro_Dest_Elim
 Involutions2Squares
 Iptables_Semantics
 Irrational_Series_Erdos_Straus
 Irrationality_J_Hancl
 Irrationals_From_THEBOOK
 IsaGeoCoq
 IsaNet
 Isabelle_C
 Isabelle_Marries_Dirac
 Isabelle_Meta_Model
 Jacobson_Basic_Algebra
 Jinja
 JinjaDCI
 JinjaThreads
 JiveDataStoreModel
 Jordan_Hoelder
 Jordan_Normal_Form
 KAD
 KAT_and_DRA
 KBPs
 KD_Tree
 Key_Agreement_Strong_Adversaries
 Khovanskii_Theorem
 Kleene_Algebra
 Kneser_Cauchy_Davenport
 Knights_Tour
 Knot_Theory
 Knuth_Bendix_Order
 Knuth_Morris_Pratt
 Koenigsberg_Friendship
 Kruskal
 Kuratowski_Closure_Complement
 LLL_Basis_Reduction
 LLL_Factorization
 LOFT
 LP_Duality
 LTL
 LTL_Master_Theorem
 LTL_Normal_Form
 LTL_to_DRA
 LTL_to_GBA
 Lam-ml-Normalization
 LambdaAuth
 LambdaMu
 Lambda_Free_EPO
 Lambda_Free_KBOs
 Lambda_Free_RPOs
 Lambert_W
 Landau_Symbols
 Laplace_Transform
 Latin_Square
 LatticeProperties
 Launchbury
 Laws_of_Large_Numbers
 Lazy-Lists-II
 Lazy_Case
 Lehmer
 Lifting_Definition_Option
 Lifting_the_Exponent
 LightweightJava
 LinearQuantifierElim
 Linear_Inequalities
 Linear_Programming
 Linear_Recurrences
 Liouville_Numbers
 List-Index
 List-Infinite
 List_Interleaving
 List_Inversions
 List_Update
 LocalLexing
 Localization_Ring
 Locally-Nameless-Sigma
 Logging_Independent_Anonymity
 Lowe_Ontological_Argument
 Lower_Semicontinuous
 Lp
 Lucas_Theorem
 MDP-Algorithms
 MDP-Rewards
 MFMC_Countable
 MFODL_Monitor_Optimized
 MFOTL_Monitor
 MSO_Regex_Equivalence
 Markov_Models
 Marriage
 Mason_Stothers
 Matrices_for_ODEs
 Matrix
 Matrix_Tensor
 Matroids
 Max-Card-Matching
 Maximum_Segment_Sum
 Median_Method
 Median_Of_Medians_Selection
 Menger
 Mereology
 Mersenne_Primes
 Metalogic_ProofChecker
 MHComputation
 MiniML
 MiniSail
 Minimal_SSA
 Minkowskis_Theorem
 Minsky_Machines
 MLSS_Decision_Proc
 Modal_Logics_for_NTS
 Modular_Assembly_Kit_Security
 Modular_arithmetic_LLL_and_HNF_algorithms
 Monad_Memo_DP
 Monad_Normalisation
 MonoBoolTranAlgebra
 MonoidalCategory
 Monomorphic_Monad
 MuchAdoAboutTwo
 Multi_Party_Computation
 Multirelations
 Multirelations_Heterogeneous
 Multiset_Ordering_NPC
 Multitape_To_Singletape_TM
 Myhill-Nerode
 Name_Carrying_Type_Inference
 Nano_JSON
 Nash_Williams
 Nat-Interval-Logic
 Native_Word
 Nested_Multisets_Ordinals
 Network_Security_Policy_Verification
 Neumann_Morgenstern_Utility
 No_FTL_observers
 No_FTL_observers_Gen_Rel
 Nominal2
 Noninterference_CSP
 Noninterference_Concurrent_Composition
 Noninterference_Generic_Unwinding
 Noninterference_Inductive_Unwinding
 Noninterference_Ipurge_Unwinding
 Noninterference_Sequential_Composition
 NormByEval
 Nullstellensatz
 Number_Theoretic_Transform
 Octonions
 OpSets
 Open_Induction
 Optics
 Optimal_BST
 Orbit_Stabiliser
 Order_Lattice_Props
 Ordered_Resolution_Prover
 Ordinal
 Ordinal_Partitions
 Ordinals_and_Cardinals
 Ordinary_Differential_Equations
 PAC_Checker
 PAL
 PAPP_Impossibility
 PCF
 PLM
 POPLmark-deBruijn
 PSemigroupsConvolution
 Package_logic
 Padic_Field
 Padic_Ints
 Pairing_Heap
 Paraconsistency
 Parity_Game
 Partial_Function_MR
 Partial_Order_Reduction
 Password_Authentication_Protocol
 Pell
 Perfect-Number-Thm
 Perron_Frobenius
 Physical_Quantities
 Pi_Calculus
 Pi_Transcendental
 Planarity_Certificates
 Pluennecke_Ruzsa_Inequality
 Poincare_Bendixson
 Poincare_Disc
 Polynomial_Factorization
 Polynomial_Interpolation
 Polynomials
 Pop_Refinement
 Posix-Lexing
 Possibilistic_Noninterference
 Power_Sum_Polynomials
 Pratt_Certificate
 Prefix_Free_Code_Combinators
 Presburger-Automata
 Prim_Dijkstra_Simple
 Prime_Distribution_Elementary
 Prime_Harmonic_Series
 Prime_Number_Theorem
 Priority_Queue_Braun
 Priority_Search_Trees
 Probabilistic_Noninterference
 Probabilistic_Prime_Tests
 Probabilistic_System_Zoo
 Probabilistic_Timed_Automata
 Probabilistic_While
 Probability_Inequality_Completeness
 Program-Conflict-Analysis
 Progress_Tracking
 Projective_Geometry
 Projective_Measurements
 Promela
 Proof_Strategy_Language
 PropResPI
 Propositional_Logic_Class
 Propositional_Proof_Systems
 Prpu_Maxflow
 PseudoHoops
 Psi_Calculi
 Ptolemys_Theorem
 Public_Announcement_Logic
 QHLProver
 QR_Decomposition
 Quantales
+Quantales_Converse
 Quantifier_Elimination_Hybrid
 Quasi_Borel_Spaces
 Quaternions
 Query_Optimization
 Quick_Sort_Cost
 RIPEMD-160-SPARK
 ROBDD
 RSAPSS
 Ramsey-Infinite
 Random_BSTs
 Random_Graph_Subgraph_Threshold
 Randomised_BSTs
 Randomised_Social_Choice
 Rank_Nullity_Theorem
 Real_Impl
 Real_Power
 Real_Time_Deque
 Recursion-Addition
 Recursion-Theory-I
 Refine_Imperative_HOL
 Refine_Monadic
 RefinementReactive
 Regex_Equivalence
 Registers
 Regression_Test_Selection
 Regular-Sets
 Regular_Algebras
 Regular_Tree_Relations
 Relation_Algebra
 Relational-Incorrectness-Logic
 Relational_Disjoint_Set_Forests
 Relational_Forests
 Relational_Method
 Relational_Minimum_Spanning_Trees
 Relational_Paths
 Rensets
 Rep_Fin_Groups
 ResiduatedTransitionSystem
 Residuated_Lattices
 Resolution_FOL
 Rewrite_Properties_Reduction
 Rewriting_Z
 Ribbon_Proofs
 Risk_Free_Lending
 Robbins-Conjecture
 Robinson_Arithmetic
 Root_Balanced_Tree
 Roth_Arithmetic_Progressions
 Routing
 Roy_Floyd_Warshall
 SATSolverVerification
 SCC_Bloemen_Sequential
 SC_DOM_Components
 SDS_Impossibility
 SIFPL
 SIFUM_Type_Systems
 SPARCv8
 Safe_Distance
 Safe_OCL
 Safe_Range_RC
 Saturation_Framework
 Saturation_Framework_Extensions
 Sauer_Shelah_Lemma
 Schutz_Spacetime
 Schwartz_Zippel
 Secondary_Sylow
 Security_Protocol_Refinement
 Selection_Heap_Sort
 SenSocialChoice
 Separata
 Separation_Algebra
 Separation_Logic_Imperative_HOL
 Separation_Logic_Unbounded
 SequentInvertibility
 Shadow_DOM
 Shadow_SC_DOM
 Shivers-CFA
 ShortestPath
 Show
 Sigma_Commit_Crypto
 Signature_Groebner
 Simpl
 Simple_Clause_Learning
 Simple_Firewall
 Simplex
 Simplicial_complexes_and_boolean_functions
 SimplifiedOntologicalArgument
 Skew_Heap
 Skip_Lists
 Slicing
 Sliding_Window_Algorithm
 Smith_Normal_Form
 Smooth_Manifolds
 Solidity
 Sophomores_Dream
 Sort_Encodings
 Source_Coding_Theorem
 SpecCheck
 Special_Function_Bounds
 Splay_Tree
 Sqrt_Babylonian
 Stable_Matching
 Stalnaker_Logic
 Statecharts
 Stateful_Protocol_Composition_and_Typing
 Stellar_Quorums
 Stern_Brocot
 Stewart_Apollonius
 Stirling_Formula
 Stochastic_Matrices
 Stone_Algebras
 Stone_Kleene_Relation_Algebras
 Stone_Relation_Algebras
 Store_Buffer_Reduction
 Stream-Fusion
 Stream_Fusion_Code
 StrictOmegaCategories
 Strong_Security
 Sturm_Sequences
 Sturm_Tarski
 Stuttering_Equivalence
 Subresultants
 Subset_Boolean_Algebras
 SumSquares
 Sunflowers
 SuperCalc
 Suppes_Theorem
 Surprise_Paradox
 Symmetric_Polynomials
 Syntax_Independent_Logic
 Synthetic_Completeness
 Szemeredi_Regularity
 Szpilrajn
 TESL_Language
 TLA
 Tail_Recursive_Functions
 Tarskis_Geometry
 Taylor_Models
 Three_Circles
 Three_Squares
 Timed_Automata
 Topological_Semantics
 Topology
 TortoiseHare
 TsirelsonBound
 Transcendence_Series_Hancl_Rucki
 Transformer_Semantics
 Transition_Systems_and_Automata
 Transitive-Closure
 Transitive-Closure-II
 Transitive_Models
 Treaps
 Tree-Automata
 Tree_Decomposition
 Tree_Enumeration
 Triangle
 Trie
 Turans_Graph_Theorem
 Twelvefold_Way
 Two_Generated_Word_Monoids_Intersection
 Tycon
 Types_Tableaus_and_Goedels_God
 Types_To_Sets_Extension
 UPF
 UPF_Firewall
 UTP
 Undirected_Graph_Theory
 Universal_Hash_Families
 Universal_Turing_Machine
 UpDown_Scheme
 VYDRA_MDL
 Valuation
 Van_Emde_Boas_Trees
 Van_der_Waerden
 VectorSpace
 VeriComp
 Verified-Prover
 Verified_SAT_Based_AI_Planning
 VerifyThis2018
 VerifyThis2019
 Vickrey_Clarke_Groves
 Virtual_Substitution
 VolpanoSmith
 WHATandWHERE_Security
 WOOT_Strong_Eventual_Consistency
 WebAssembly
 Weight_Balanced_Trees
 Weighted_Arithmetic_Geometric_Mean
 Weighted_Path_Order
 Well_Quasi_Orders
 Wetzels_Problem
 Winding_Number_Eval
 Word_Lib
 WorkerWrapper
 X86_Semantics
 XML
 Youngs_Inequality
 ZFC_in_HOL
 Zeckendorf
 Zeta_3_Irrational
 Zeta_Function
 pGCL