Theory Two_Quantale

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

section ‹2-Quantales›

theory Two_Quantale
  imports Quantales_Converse.Modal_Quantale Two_Kleene_Algebra

begin

class quantale0 = complete_lattice + monoid_mult0 +
  assumes Sup_distl0: "x ⋅⇩0 ⨆Y = (⨆y ∈ Y. x ⋅⇩0 y)" 
  assumes Sup_distr0: "⨆X ⋅⇩0 y = (⨆x ∈ X. x ⋅⇩0 y)"

sublocale quantale0 ⊆ q0q: unital_quantale "1⇩0" "(⋅⇩0)" _ _ _ _ _ _ _ _ 
  apply unfold_locales using local.Sup_distr0 local.Sup_distl0 by auto

definition (in quantale0) "qstar0 = q0q.qstar"

lemma (in quantale0) qstar0_unfold: "qstar0 x = (⨆i. mm0.power x i)"
  by (simp add: local.q0q.qstar_def local.qstar0_def)

sublocale quantale0 ⊆ dq0s0: dioid0 "(⊔)" "(≤)" "(<)" "⊥" "(⋅⇩0)" "1⇩0"
  by unfold_locales (simp_all add: local.q0q.sup_distl)

sublocale quantale0 ⊆ dq0ka0: kleene_algebra0 "(⊔)" "(≤)" "(<)" "⊥"  "(⋅⇩0)" "1⇩0" qstar0
  by unfold_locales (simp_all add: local.qstar0_def local.q0q.uwqlka.star_inductl local.q0q.uqka.star_inductr')

class domain_quantale0 = quantale0 + dom0_op +
  assumes dom0_absorb: "x ≤ dom⇩0 x ⋅⇩0 x"
  and dom0_local: "dom⇩0 (x ⋅⇩0 dom⇩0 y) = dom⇩0 (x ⋅⇩0 y)"
  and dom0_add: "dom⇩0 (x ⊔ y) = dom⇩0 x ⊔ dom⇩0 y"
  and dom0_subid: "dom⇩0 x ≤ 1⇩0"
  and dom0_zero: "dom⇩0 ⊥ = ⊥"

sublocale domain_quantale0 ⊆ dq0dq: domain_quantale "dom⇩0" "1⇩0" "(⋅⇩0)" _ _ _ _ _ _ _ _
  by unfold_locales (simp_all add: local.dom0_absorb local.dom0_local local.dom0_add local.dom0_subid dom0_zero)

sublocale domain_quantale0 ⊆ dq0ds0: domain_semiring0 "(⊔)" "(≤)" "(<)" "⊥"  "(⋅⇩0)" "1⇩0" "dom⇩0"
  by unfold_locales (simp_all add: local.dom0_local local.dom0_add local.dom0_subid dom0_zero)

class codomain_quantale0 = quantale0 + cod0_op +
  assumes cod0_absorb: "x ≤ x ⋅⇩0 cod⇩0 x" 
  and cod0_local: "cod⇩0 (cod⇩0 x ⋅⇩0 y) = cod⇩0 (x ⋅⇩0 y)"
  and cod0_add: "cod⇩0 (x ⊔ y) = cod⇩0 x ⊔ cod⇩0 y"
  and cod0_subid: "cod⇩0 x ≤ 1⇩0"
  and cod0_zero: "cod⇩0 ⊥ = ⊥"

sublocale codomain_quantale0 ⊆ cdq0cdq: codomain_quantale "1⇩0" "(⋅⇩0)" _ _ _ _ _ _ _ _ "cod⇩0"
  by (unfold_locales, simp_all add: local.cod0_absorb local.cod0_local local.cod0_add local.cod0_subid cod0_zero)

sublocale codomain_quantale0 ⊆ cdq0dcs0: codomain_semiring0 "cod⇩0" "(⊔)"  "(≤)" "(<)" "⊥" "(⋅⇩0)" "1⇩0"
  by (unfold_locales, simp_all add: local.cod0_absorb local.cod0_local local.cod0_add local.cod0_subid cod0_zero)

class modal_quantale0 = domain_quantale0 + codomain_quantale0 +
  assumes dc_compat: "dom⇩0 (cod⇩0 x) = cod⇩0 x" 
  and cd_compat: "cod⇩0 (dom⇩0 x) = dom⇩0 x" 

sublocale modal_quantale0 ⊆ mq0mq: dc_modal_quantale "1⇩0" "(⋅⇩0)" _ _ _ _ _ _ _ _  "cod⇩0" "dom⇩0"
  by (unfold_locales, simp_all add: dc_compat cd_compat)

sublocale modal_quantale0 ⊆ mq0mka: modal_kleene_algebra0 "(⊔)" "(≤)" "(<)" "⊥" "(⋅⇩0)" "1⇩0" qstar0 "cod⇩0" "dom⇩0"
  by unfold_locales simp_all

sublocale modal_quantale0 ⊆ mq0dual: modal_quantale0 "dom⇩0" _ _ _ _ _ _ _ _ "λx y. y ⋅⇩0 x" _ "cod⇩0"
  by unfold_locales (simp_all add: local.cdq0cdq.coddual.Sup_distl local.Sup_distl0)


class quantale1 = complete_lattice + monoid_mult1 +
  assumes Sup_distl1: "x ⋅⇩1 ⨆Y = (⨆y ∈ Y. x ⋅⇩1 y)" 
  assumes Sup_distr1: "⨆X ⋅⇩1 y = (⨆x ∈ X. x ⋅⇩1 y)"

sublocale quantale1 ⊆ q1q: unital_quantale "1⇩1" "(⋅⇩1)" _ _ _ _ _ _ _ _ 
  by (unfold_locales, auto simp: local.Sup_distl1 local.Sup_distr1)

definition (in quantale1) "qstar1 = q1q.qstar"

lemma (in quantale1) qstar1_unfold: "qstar1 x = (⨆i. mm1.power x i)"
  by (simp add: local.q1q.qstar_def local.qstar1_def)

sublocale quantale1 ⊆ dq1s1: dioid1 "(⊔)" "(≤)" "(<)" "⊥" "(⋅⇩1)" "1⇩1"
  by unfold_locales (simp_all add: local.q1q.wswq.distrib_left)

sublocale quantale1 ⊆ dq0ka1: kleene_algebra1 "(⊔)" "(≤)" "(<)" "⊥" "(⋅⇩1)" "1⇩1" qstar1
  by unfold_locales (simp_all add: local.qstar1_def local.q1q.uwqlka.star_inductl local.q1q.uqka.star_inductr')

class domain_quantale1 = quantale1 + dom1_op +
  assumes dom1_absorb: "x ≤ dom⇩1 x ⋅⇩1 x"
  and dom1_local: "dom⇩1 (x ⋅⇩1 dom⇩1 y) = dom⇩1 (x ⋅⇩1 y)"
  and dom1_add: "dom⇩1 (x ⊔ y) = dom⇩1 x ⊔ dom⇩1 y"
  and dom1_subid: "dom⇩1 x ≤ 1⇩1"
  and dom1_zero: "dom⇩1 ⊥ = ⊥"

sublocale domain_quantale1 ⊆ dq1dq: domain_quantale "dom⇩1" "1⇩1" "(⋅⇩1)" _ _ _ _ _ _ _ _
  by (unfold_locales, simp_all add: local.dom1_absorb local.dom1_local local.dom1_add local.dom1_subid dom1_zero)

sublocale domain_quantale1 ⊆ dq1ds1: domain_semiring1 "(⊔)" "(≤)" "(<)" "⊥"  "(⋅⇩1)" "1⇩1" "dom⇩1"
  by (unfold_locales, simp_all add: local.dom1_local local.dom1_add local.dom1_subid dom1_zero)
 
class codomain_quantale1 = quantale1 + cod1_op +
  assumes cod1_absorb: "x ≤ x ⋅⇩1 cod⇩1 x" 
  and cod1_local: "cod⇩1 (cod⇩1 x ⋅⇩1 y) = cod⇩1 (x ⋅⇩1 y)"
  and cod1_add: "cod⇩1 (x ⊔ y) = cod⇩1 x ⊔ cod⇩1 y"
  and cod1_subid: "cod⇩1 x ≤ 1⇩1"
  and cod1_zero: "cod⇩1 ⊥ = ⊥"

sublocale codomain_quantale1 ⊆ cdq1cdq: codomain_quantale "1⇩1" "(⋅⇩1)" _ _ _ _ _ _ _ _ "cod⇩1"
  by (unfold_locales, simp_all add: local.cod1_absorb local.cod1_local local.cod1_add local.cod1_subid cod1_zero)

sublocale codomain_quantale1 ⊆ cdq1dcs1: codomain_semiring1 "cod⇩1" "(⊔)" "(≤)" "(<)" "⊥" "(⋅⇩1)" "1⇩1"
  by (unfold_locales, simp_all add: local.cod1_absorb local.cod1_local local.cod1_add local.cod1_subid cod1_zero)

class modal_quantale1 = domain_quantale1 + codomain_quantale1 +
  assumes dc_compat: "dom⇩1 (cod⇩1 x) = cod⇩1 x" 
  and cd_compat: "cod⇩1 (dom⇩1 x) = dom⇩1 x" 

sublocale modal_quantale1 ⊆ mq1mq: dc_modal_quantale "1⇩1" "(⋅⇩1)" _ _ _ _ _ _ _ _ "cod⇩1" "dom⇩1"
  by (unfold_locales, simp_all add: local.dc_compat local.cd_compat)

sublocale modal_quantale1 ⊆ mq1mka: modal_kleene_algebra1 "(⊔)" "(≤)" "(<)" "⊥"  "(⋅⇩1)" "1⇩1" qstar1 "cod⇩1" "dom⇩1"
  by unfold_locales simp_all

sublocale modal_quantale1 ⊆ mq1dual: modal_quantale1 "dom⇩1" _ _ _ _ _ _ _ _ "λx y. y ⋅⇩1 x" _ "cod⇩1"
  by unfold_locales (simp_all add: local.Sup_distr1 local.Sup_distl1)

class two_quantale = modal_quantale0 + modal_quantale1 +
  assumes interchange: "(w ⋅⇩1 x) ⋅⇩0 (y ⋅⇩1 z) ≤ (w ⋅⇩0 y) ⋅⇩1 (x ⋅⇩0 z)"
  and d1_hom: "dom⇩1 (x ⋅⇩0 y) ≤ dom⇩1 x ⋅⇩0 dom⇩1 y"
  and c1_hom: "cod⇩1 (x ⋅⇩0 y) ≤ cod⇩1 x ⋅⇩0 cod⇩1 y"
  and d0_weak_hom: "dom⇩0 (x ⋅⇩1 y) ≤ dom⇩0 x ⋅⇩1 dom⇩0 y"
  and c0_weak_hom: "cod⇩0 (x ⋅⇩1 y) ≤ cod⇩0 x ⋅⇩1 cod⇩0 y"
  and d1d0 [simp]: "dom⇩1 (dom⇩0 x) = dom⇩0 x"

class strong_two_quantale = two_quantale +
  assumes d1_strong_hom [simp]: "dom⇩1 (x ⋅⇩0 y) = dom⇩1 x ⋅⇩0 dom⇩1 y"
  and c1_strong_hom [simp]: "cod⇩1 (x ⋅⇩0 y) = cod⇩1 x ⋅⇩0 cod⇩1 y"

sublocale two_quantale ⊆ tgqs: two_semiring "cod⇩0" "(⊔)" "(≤)" "(<)" "⊥" "(⋅⇩0)" "1⇩0" "dom⇩0"  "cod⇩1" "(⋅⇩1)" "1⇩1" "dom⇩1"
  by (unfold_locales, simp_all add: local.mq0mq.mqs.msrdual.cd_compat local.mq0mq.mqs.msrdual.dc_compat local.dc_compat local.cd_compat local.interchange local.c0_weak_hom local.c1_hom local.d0_weak_hom local.d1_hom)

sublocale strong_two_quantale ⊆ stgqs: strong_two_semiring "cod⇩0" "(⊔)" "(≤)" "(<)" "⊥" "(⋅⇩0)" "1⇩0" "dom⇩0"  "cod⇩1" "(⋅⇩1)" "1⇩1" "dom⇩1"
  by unfold_locales simp_all

sublocale two_quantale ⊆ tgqs: two_kleene_algebra "(⊔)" "(≤)" "(<)" "⊥"  "(⋅⇩0)" "1⇩0" qstar0 "(⋅⇩1)"  "1⇩1" qstar1 "cod⇩0" "dom⇩0" "cod⇩1" "dom⇩1" ..

sublocale strong_two_quantale ⊆ tgqs: strong_two_kleene_algebra "(⊔)" "(≤)" "(<)" "⊥" "(⋅⇩0)" "1⇩0" qstar0 "(⋅⇩1)"  "1⇩1" qstar1 "cod⇩0" "dom⇩0" "cod⇩1" "dom⇩1" ..

lemma (in strong_two_quantale) id0_le_id1: "1⇩0 = 1⇩1"
  (* nitpick [expect = genuine] *)
  oops

context two_quantale
begin

lemma qstar0_aux: "mm0.power (x ⋅⇩1 y) i ≤ mm0.power x i ⋅⇩1 mm0.power y i"
proof (induct i)
  case 0
  then show ?case by simp
next
  case (Suc i)
  fix i 
  assume h: "mm0.power (x ⋅⇩1 y) i ≤ mm0.power x i ⋅⇩1 mm0.power y i"
  have "mm0.power (x ⋅⇩1 y) (Suc i) = (x ⋅⇩1 y) ⋅⇩0 mm0.power (x ⋅⇩1 y) i"
    by simp
  also have "… ≤ (x ⋅⇩1 y) ⋅⇩0 (mm0.power x i ⋅⇩1 mm0.power y i)"
    by (simp add: h local.q0q.psrpq.mult_isol)
  also have "… ≤ (x ⋅⇩0 mm0.power x i) ⋅⇩1 (y ⋅⇩0 mm0.power y i)"
    by (simp add: local.interchange)
  also have "… = mm0.power x (Suc i) ⋅⇩1 mm0.power y (Suc i)"
    by simp
  finally show "mm0.power (x ⋅⇩1 y) (Suc i) ≤ mm0.power x (Suc i) ⋅⇩1 mm0.power y (Suc i)".
qed

lemma qstar0_oplax: "qstar0 (x ⋅⇩1 y) ≤ qstar0 x ⋅⇩1 qstar0 y"
  by (simp add: local.tgqs.star0_comp1)

lemma qstar1_distl0: "x ⋅⇩0 (qstar1 y) = (⨆i. x ⋅⇩0 mm1.power y i)"
  by (simp add: image_image local.Sup_distl0 local.qstar1_unfold)

lemma qstar1_distr0: "(qstar1 x) ⋅⇩0 y = (⨆i. mm1.power x i ⋅⇩0 y)"
  by (simp add: image_image local.Sup_distr0 local.qstar1_unfold)

lemma qstar0_distl1: "x ⋅⇩1 (qstar0 y) = (⨆i. x ⋅⇩1 mm0.power y i)"
  by (simp add: image_image local.Sup_distl1 local.qstar0_unfold)

lemma qstar0_distr1: "(qstar0 x) ⋅⇩1 y = (⨆i. mm0.power x i ⋅⇩1 y)"
  by (smt (verit, best) image_image local.SUP_cong local.Sup_distr1 local.qstar0_unfold)

lemma star1_laxl_aux_var: "dom⇩0 x ⋅⇩0 mm1.power y i ≤ mm1.power (dom⇩0 x ⋅⇩0 y) i"
proof (induct i)
  case 0
  have "dom⇩0 x ⋅⇩0 1⇩1 = dom⇩1 (dom⇩0 x) ⋅⇩0 1⇩1"
    by simp
  also have "… ≤ 1⇩1 ⋅⇩0 1⇩1"
    using local.dom1_subid local.q0q.nsrnq.mult_isor by blast
  finally have "dom⇩0 x ⋅⇩0 1⇩1 ≤ 1⇩1"
    by (simp add: local.dq0dq.dqmsr.dom_subid_aux2)
  thus "dom⇩0 x ⋅⇩0 mm1.power y 0 ≤ mm1.power (dom⇩0 x ⋅⇩0 y) 0"
    by simp
next
  case (Suc i)
  fix i
  assume h: "dom⇩0 x ⋅⇩0 mm1.power y i ≤ mm1.power (dom⇩0 x ⋅⇩0 y) i"
  have "dom⇩0 x ⋅⇩0 mm1.power y (Suc i) = dom⇩0 x ⋅⇩0 (y ⋅⇩1  mm1.power y i)"
    by simp
  also have "… = (dom⇩0 x ⋅⇩1 dom⇩0 x) ⋅⇩0 (y ⋅⇩1 mm1.power y i)"
    by simp
  also have "… ≤ (dom⇩0 x ⋅⇩0 y) ⋅⇩1 (dom⇩0 x ⋅⇩0 mm1.power y i)"
    using local.interchange by blast
  also have "… ≤ (dom⇩0 x ⋅⇩0 y) ⋅⇩1 mm1.power (dom⇩0 x ⋅⇩0 y) i"
    by (simp add: h local.q1q.psrpq.mult_isol)
  finally show "dom⇩0 x ⋅⇩0 mm1.power y (Suc i) ≤ mm1.power (dom⇩0 x ⋅⇩0 y) (Suc i)"
    by simp
qed
 
lemma star1_laxl_var: "dom⇩0 x ⋅⇩0 qstar1 y ≤ qstar1 (dom⇩0 x ⋅⇩0 y)"  
proof-
  have "dom⇩0 x ⋅⇩0 qstar1 y = (⨆i. dom⇩0 x ⋅⇩0 mm1.power y i)"
    using local.qstar1_distl0 by auto
  also have "… ≤ (⨆i. mm1.power (dom⇩0 x ⋅⇩0 y) i)"
    by (simp add: local.SUP_mono' local.star1_laxl_aux_var)
  finally show ?thesis
    by (simp add: local.qstar1_unfold)
qed

lemma star1_laxr_aux_var: "mm1.power x i ⋅⇩0 cod⇩0 y ≤ mm1.power (x ⋅⇩0 cod⇩0 y) i"
proof (induct i)
  case 0 show ?case
    by (simp add: local.cdq0cdq.coddual.dqmsr.dom_subid_aux2)
next
  case (Suc i)
  fix i
  assume h: "mm1.power x i ⋅⇩0 cod⇩0 y ≤ mm1.power (x ⋅⇩0 cod⇩0 y) i"
  have "mm1.power x (Suc i) ⋅⇩0 cod⇩0 y = (x ⋅⇩1 mm1.power x i ) ⋅⇩0 (cod⇩0 y ⋅⇩1 cod⇩0 y)"
    by simp
  also have "…  ≤ (x ⋅⇩0 cod⇩0 y) ⋅⇩1 (mm1.power x i ⋅⇩0 cod⇩0 y)"
    by (simp add: local.tgqs.tgsdual.d0_comp1)
  finally show "mm1.power x (Suc i) ⋅⇩0 cod⇩0 y ≤ mm1.power (x ⋅⇩0 cod⇩0 y) (Suc i)"
    by (simp add: h local.q0q.h_w2 local.q1q.psrpq.mult_isol)
qed
 
lemma qstar1_laxr_var: "qstar1 x ⋅⇩0 cod⇩0 y ≤ qstar1 (x ⋅⇩0 cod⇩0 y)"  
proof-
  have "qstar1 x ⋅⇩0 cod⇩0 y = (⨆i. mm1.power x i ⋅⇩0 cod⇩0 y)"
    using local.qstar1_distr0 by auto
  also have "… ≤ (⨆i. mm1.power (x ⋅⇩0 cod⇩0 y) i)"
    by (simp add: local.SUP_mono' local.star1_laxr_aux_var)
  finally show ?thesis
    by (simp add: local.qstar1_unfold)
qed

lemma qstar_1_power: "qstar1 x ⋅⇩0 qstar1 y = (⨆i j. mm1.power x i ⋅⇩0 mm1.power y j)"
proof-
  have "qstar1 x ⋅⇩0 qstar1 y = qstar1 x ⋅⇩0( ⨆j. mm1.power y j)"
    using bot_nat_0.extremum local.qstar1_unfold by presburger
  also have "… = (⨆j. qstar1 x ⋅⇩0 mm1.power y j)"
    using calculation local.qstar1_distl0 by auto
  also have "… = (⨆j. (⨆i. mm1.power x i) ⋅⇩0 mm1.power y j)"
    unfolding qstar1_def q1q.qstar_def by (simp add: full_SetCompr_eq)
  also have "… = (⨆i j. mm1.power x i ⋅⇩0 mm1.power y j)"
    by (smt (verit, ccfv_SIG) Sup.SUP_cong calculation local.qstar1_distl0 local.qstar1_distr0)
  finally show ?thesis.
qed

end

context strong_two_quantale
begin

lemma star1_laxl_aux: "dom⇩1 x ⋅⇩0 mm1.power y i ≤ mm1.power (dom⇩1 x ⋅⇩0 y) i"
proof (induct i)
  case 0
  have "dom⇩1 x ⋅⇩0 1⇩1 ≤ 1⇩1 ⋅⇩0 1⇩1"
    using local.dom1_subid local.q0q.nsrnq.mult_isor by blast
  thus "dom⇩1 x ⋅⇩0 mm1.power y 0 ≤ mm1.power (dom⇩1 x ⋅⇩0 y) 0"
    by simp
next
  case (Suc i)
  fix i
  assume h: "dom⇩1 x ⋅⇩0 mm1.power y i ≤ mm1.power (dom⇩1 x ⋅⇩0 y) i"
  have "dom⇩1 x ⋅⇩0 mm1.power y (Suc i) = dom⇩1 x ⋅⇩0 (y ⋅⇩1  mm1.power y i)"
    by simp
  also have "… = (dom⇩1 x ⋅⇩1 dom⇩1 x) ⋅⇩0 (y ⋅⇩1 mm1.power y i)"
    by simp
  also have "…  ≤ (dom⇩1 x ⋅⇩0 y) ⋅⇩1 (dom⇩1 x ⋅⇩0 mm1.power y i)"
    using local.interchange by blast
  also have "…  ≤ (dom⇩1 x ⋅⇩0 y) ⋅⇩1 mm1.power (dom⇩1 x ⋅⇩0 y) i"
    by (simp add: h local.q1q.psrpq.mult_isol)
  finally show "dom⇩1 x ⋅⇩0 mm1.power y (Suc i) ≤ mm1.power (dom⇩1 x ⋅⇩0 y) (Suc i)"
    by simp
qed

lemma star1_laxl: "dom⇩1 x ⋅⇩0 qstar1 y ≤ qstar1 (dom⇩1 x ⋅⇩0 y)" 
proof-
  have "dom⇩1 x ⋅⇩0 qstar1 y = (⨆i. dom⇩1 x ⋅⇩0 mm1.power y i)"
    using local.qstar1_distl0 by auto
  also have "… ≤ (⨆i. mm1.power (dom⇩1 x ⋅⇩0 y) i)"
    by (simp add: local.SUP_mono' local.star1_laxl_aux)
  finally show ?thesis
    by (simp add: local.qstar1_unfold)
qed

lemma star1_laxr_aux: "mm1.power x i ⋅⇩0 cod⇩1 y ≤ mm1.power (x ⋅⇩0 cod⇩1 y) i"
  apply (induct i)
   apply (metis local.cod1_subid local.mm1.power.power_0 local.q0q.psrpq.mult_isol local.stgqs.stgsdual.id1_comp0_eq)
  by (smt (verit, ccfv_SIG) local.dual_order.trans local.q1q.psrpq.mult_isol local.tgqs.tgsdual.d1_comp1 power.power.power_Suc)

lemma qstar1_laxr: "qstar1 x ⋅⇩0 cod⇩1 y ≤ qstar1 (x ⋅⇩0 cod⇩1 y)"  
proof-
  have "qstar1 x ⋅⇩0 cod⇩1 y = (⨆i. mm1.power x i ⋅⇩0 cod⇩1 y)"
    using local.qstar1_distr0 by auto
  also have "… ≤ (⨆i. mm1.power (x ⋅⇩0 cod⇩1 y) i)"
    by (simp add: local.SUP_mono' local.star1_laxr_aux)
  finally show ?thesis
    by (simp add: local.qstar1_unfold)
qed

lemma qstar1_aux: "mm1.power x i ⋅⇩0 mm1.power y i ≤ mm1.power (x ⋅⇩0 y) i"
proof (induct i)
  case 0
  then show ?case
    by simp
next
  case (Suc i)
 fix i 
  assume h: "mm1.power x i ⋅⇩0 mm1.power y i ≤ mm1.power (x ⋅⇩0 y) i" 
  have "mm1.power x (Suc i) ⋅⇩0 mm1.power y (Suc i) = (x ⋅⇩1 mm1.power x i) ⋅⇩0 (y ⋅⇩1 mm1.power y i)"
    by simp
  also have "… ≤ (x ⋅⇩0 y) ⋅⇩1 (mm1.power x i ⋅⇩0 mm1.power y i)"
    using local.interchange by force
  also have "… ≤ (x ⋅⇩0 y) ⋅⇩1 mm1.power (x ⋅⇩0 y) i"
    by (simp add: h local.q1q.psrpq.mult_isol)
  also have "… = mm1.power (x ⋅⇩0 y) (Suc i)"
    by simp
  finally show "mm1.power x (Suc i) ⋅⇩0 mm1.power y (Suc i) ≤ mm1.power (x ⋅⇩0 y) (Suc i)".
qed

lemma "qstar1 x ⋅⇩0 qstar1 y ≤ qstar0 (x ⋅⇩1 y)"
  (* no proof, no counterexample *)
  oops

lemma "qstar1 x ⋅⇩0 qstar1 y ≤ qstar1 (x ⋅⇩1 y)"
  (* no proof, no counterexample *)
  oops

lemma "qstar1 (x ⋅⇩1 y) ≤ qstar1 x ⋅⇩0 qstar1 y"
  (* no proof, no counterexample *)
  oops

lemma "qstar1 x ⋅⇩0 qstar1 y ≤ qstar1 (x ⋅⇩0 y)"
  (* no proof, no counterexample *)
  oops

lemma "qstar1 (x ⋅⇩0 y) ≤ qstar1 x ⋅⇩0 qstar1 y"
  (* no proof, no counterexample *)
  oops

lemma "qstar0 x ⋅⇩1 qstar0 y ≤ qstar0 (x ⋅⇩0 y)"
  (* no proof, no counterexample *)
  oops

end

lemma (in strong_two_kleene_algebra) "qstar0 x ⋅⇩1 qstar0 y ≤ qstar0 (x ⋅⇩1 y)"
  (* no proof, no counterexample *)
  oops

lemma (in strong_two_kleene_algebra) "qstar0 (x ⋅⇩1 y) ≤ qstar0 x ⋅⇩1 qstar0 y"
  (* no proof, no counterexample *)
  oops

class two_quantale_lmcs = modal_quantale0 + modal_quantale1 +
  assumes interchange: "(w ⋅⇩1 x) ⋅⇩0 (y ⋅⇩1 z) ≤ (w ⋅⇩0 y) ⋅⇩1 (x ⋅⇩0 z)"
  and d1_hom: "dom⇩1 (x ⋅⇩0 y) = dom⇩1 x ⋅⇩0 dom⇩1 y"
  and c1_hom: "cod⇩1 (x ⋅⇩0 y) = cod⇩1 x ⋅⇩0 cod⇩1 y"
  and d1d0 [simp]: "dom⇩1 (dom⇩0 x) = dom⇩0 x"
 and c1d0 [simp]: "cod⇩1 (dom⇩0 x) = dom⇩0 x"
 and d1c0 [simp]: "dom⇩1 (cod⇩0 x) = cod⇩0 x"
 and c1c0 [simp]: "cod⇩1 (cod⇩0 x) = cod⇩0 x"
  and d0d1 [simp]: "dom⇩0 (dom⇩1 x) = dom⇩0 x"
 and c0d1 [simp]: "cod⇩0 (dom⇩1 x) = dom⇩0 x"
 and d0c1 [simp]: "dom⇩0 (cod⇩1 x) = cod⇩0 x"
 and c0c1 [simp]: "cod⇩0 (cod⇩1 x) = cod⇩0 x"

begin

lemma "dom⇩0 (x ⋅⇩1 y) ≤ dom⇩0 x ⋅⇩1 dom⇩0 y"
  (* no proof no counterexample *)
  oops

lemma  "cod⇩0 (x ⋅⇩1 y) ≤ cod⇩0 x ⋅⇩1 cod⇩0 y"
  (* no proof no counterexample *)
  oops

end

end