# Theory Regular_Algebras

```(* Title:      Regular Algebras
Author:     Simon Foster, Georg Struth
Maintainer: Simon Foster <s.foster at york.ac.uk>
Georg Struth <g.struth at sheffield.ac.uk>
*)

section ‹Regular Algebras›

theory Regular_Algebras
imports Dioid_Power_Sum Kleene_Algebra.Finite_Suprema Kleene_Algebra.Kleene_Algebra
begin

subsection ‹Conway's Classical Axioms›

text ‹Conway's classical axiomatisation of Regular Algebra from~\<^cite>‹"Conway"›.›

class star_dioid = dioid_one_zero + star_op + plus_ord

class conway_dioid = star_dioid +
assumes C11: "(x + y)⇧⋆ = (x⇧⋆ ⋅ y)⇧⋆ ⋅ x⇧⋆"
and C12: "(x ⋅ y)⇧⋆ = 1 + x ⋅(y ⋅ x)⇧⋆ ⋅ y"

class strong_conway_dioid = conway_dioid +
assumes  C13: "(x⇧⋆)⇧⋆ = x⇧⋆"

class C_algebra = strong_conway_dioid +
assumes C14: "x⇧⋆ = (x⇗n+1⇖)⇧⋆ ⋅ x⇘0⇙⇗n⇖"

text ‹We tried to dualise using sublocales, but this causes an infinite loop on dual.dual.dual....›

lemma (in conway_dioid) C11_var: "(x + y)⇧⋆ = x⇧⋆ ⋅ (y ⋅ x⇧⋆)⇧⋆"
proof -
have "x⇧⋆ ⋅ (y ⋅ x⇧⋆)⇧⋆ = x⇧⋆ + x⇧⋆ ⋅ y ⋅ (x⇧⋆ ⋅ y)⇧⋆ ⋅ x⇧⋆"
by (metis C12 distrib_left mult.assoc mult_oner)
also have "... = (1 +  x⇧⋆ ⋅ y ⋅ (x⇧⋆ ⋅ y)⇧⋆) ⋅ x⇧⋆"
by (metis distrib_right mult.assoc mult_onel)
finally show ?thesis
by (metis C11 C12 mult_onel mult_oner)
qed

lemma (in conway_dioid) dual_conway_dioid:
"class.conway_dioid (+) (⊙) 1 0 (≤) (<) star"
proof
fix x y z :: 'a
show "(x ⊙ y) ⊙ z = x ⊙(y ⊙ z)"
by (metis mult.assoc opp_mult_def)
show "(x + y) ⊙ z = x ⊙ z + y ⊙ z"
by (metis distrib_left opp_mult_def)
show "x + x = x"
show "1 ⊙ x = x"
by (metis mult_oner opp_mult_def)
show "x ⊙ 1 = x"
by (metis mult_onel opp_mult_def)
show "0 + x = x"
show "0 ⊙ x = 0"
by (metis annir times.opp_mult_def)
show "x ⊙ (y + z) = x ⊙ y + x ⊙ z"
by (metis opp_mult_def distrib_right')
show "x ⊙ 0 = 0"
by (metis annil opp_mult_def)
show "(x + y)⇧⋆ = (x⇧⋆ ⊙ y)⇧⋆ ⊙ x⇧⋆"
by (metis C11_var opp_mult_def)
show "(x ⊙ y)⇧⋆ = 1 + x ⊙ (y ⊙ x)⇧⋆ ⊙ y"
by (metis C12 mult.assoc opp_mult_def)
qed

lemma (in strong_conway_dioid) dual_strong_conway_dioid: "class.strong_conway_dioid ((+) ) ((⊙) ) 1 0 (≤) (<) star"
proof
fix x y z :: 'a
show "(x ⊙ y) ⊙ z = x ⊙ (y ⊙ z)"
by (metis mult.assoc opp_mult_def)
show "(x + y) ⊙ z = x ⊙ z + y ⊙ z"
by (metis distrib_left opp_mult_def)
show "x + x = x"
show "1 ⊙ x = x"
by (metis mult_oner opp_mult_def)
show "x ⊙ 1 = x"
by (metis mult_onel opp_mult_def)
show "0 + x = x"
show "0 ⊙  x = 0"
by (metis annir opp_mult_def)
show "x ⊙ (y + z) = x ⊙ y + x ⊙ z"
by (metis opp_mult_def distrib_right')
show "x ⊙ 0 = 0"
by (metis annil opp_mult_def)
show "(x + y)⇧⋆ = (x⇧⋆ ⊙ y)⇧⋆ ⊙ x⇧⋆"
by (metis C11_var opp_mult_def)
show "(x ⊙ y)⇧⋆ = 1 + x ⊙ (y ⊙ x)⇧⋆ ⊙ y"
by (metis C12 mult.assoc opp_mult_def)
show "(x⇧⋆)⇧⋆ = x⇧⋆"
by (metis C13)
qed

text‹Nitpick finds counterexamples to the following claims.›

lemma (in conway_dioid) "1⇧⋆ = 1"
nitpick [expect=genuine] ― ‹3-element counterexample›
oops

lemma (in conway_dioid) "(x⇧⋆)⇧⋆ = x⇧⋆"
nitpick [expect=genuine] ― ‹3-element counterexample›
oops

context C_algebra
begin

lemma C_unfoldl [simp]: "1 + x ⋅  x⇧⋆ =  x⇧⋆"
by (metis C12 mult_onel mult_oner)

lemma C_slide: "(x ⋅ y)⇧⋆ ⋅ x = x ⋅ (y ⋅ x)⇧⋆"
proof-
have "(x ⋅ y)⇧⋆ ⋅ x = x + x ⋅ (y ⋅ x)⇧⋆ ⋅ y ⋅ x"
by (metis C12 mult_onel distrib_right')
also have "... = x ⋅ (1 + (y ⋅ x)⇧⋆ ⋅ y ⋅ x)"
by (metis distrib_left mult.assoc mult_oner)
finally show ?thesis
by (metis C12 mult.assoc mult_onel mult_oner)
qed

lemma powsum_ub: "i ≤ n ⟹ x⇗i⇖ ≤ x⇘0⇙⇗n⇖"
proof (induct n)
case 0 show ?case
by (metis (opaque_lifting, mono_tags) "0.prems" order.eq_iff le_0_eq power_0 powsum_00)
next
case (Suc n) show ?case
proof -
{ assume aa1: "Suc n ≠ i"
have ff1: "x⇘0⇙⇗Suc n⇖ ≤ x⇘0⇙⇗Suc n⇖ ∧ Suc n ≠ i"
using aa1 by fastforce
have ff2: "∃x⇩1. x⇘0⇙⇗n⇖ + x⇩1 ≤ x⇘0⇙⇗Suc n⇖ ∧ Suc n ≠ i"
using ff1 powsum2 by auto
have "x⇗i⇖ ≤ x⇘0⇙⇗Suc n⇖"
by (metis Suc.hyps Suc.prems ff2 le_Suc_eq local.dual_order.trans local.join.le_supE)
}
thus "x⇗i⇖ ≤ x⇘0⇙⇗Suc n⇖"
using local.less_eq_def local.powsum_split_var2 by blast
qed
qed

lemma C14_aux: "m ≤ n ⟹  x⇗m⇖ ⋅ (x⇗n⇖)⇧⋆ = (x⇗n⇖)⇧⋆ ⋅ x⇗m⇖"
proof -
assume assm: "m ≤ n"
hence "x⇗m⇖ ⋅  (x⇗n⇖)⇧⋆ =  x⇗m⇖ ⋅ (x⇗n-m⇖ ⋅ x⇗m⇖)⇧⋆"
also have "... = (x⇗n-m⇖ ⋅ x⇗m⇖)⇧⋆ ⋅  x⇗m⇖"
finally show ?thesis
qed

end

context dioid_one_zero
begin

lemma opp_power_def:
"power.power 1 (⊙) x n = x⇗n⇖"
proof (induction n)
case 0 thus ?case
by (metis power.power.power_0)
next
case (Suc n) thus ?case
by (metis power.power.power_Suc power_Suc2 times.opp_mult_def)
qed

lemma opp_powsum_def:
"dioid_one_zero.powsum (+) (⊙) 1 0 x m n = x⇘m⇙⇗n⇖"
proof -
have "sum (power.power 1 (⊙) x) {m..n + m} = sum ((^) x) {m..n + m}"
thus ?thesis
by (simp add: dioid_one_zero.powsum_def[of _ _ _ _ "(≤)" "(<)"] dual_dioid_one_zero powsum_def)
qed

end

lemma C14_dual:
fixes x::"'a::C_algebra"
shows "x⇧⋆ = x⇘0⇙⇗n⇖ ⋅ (x⇗n+1⇖)⇧⋆"
proof -
have "x⇧⋆ =  (x⇗n+1⇖)⇧⋆ ⋅ x⇘0⇙⇗n⇖"
by (rule C14)
also have "... = (x⇗n+1⇖)⇧⋆ ⋅ (∑i=0..n. x^i)"
by (subst powsum_def, auto)
also have "... = (∑i=0..n. (x⇗n+1⇖)⇧⋆ ⋅ x^i)"
by (metis le0 sum_interval_distl)
also have "... = (∑i=0..n. x^i ⋅ (x⇗n+1⇖)⇧⋆)"
by (auto intro: sum_interval_cong simp only:C14_aux)
also have "... = x⇘0⇙⇗n⇖ ⋅ (x⇗n+1⇖)⇧⋆"
by (simp only: sum_interval_distr[THEN sym] powsum_def Nat.add_0_right)
finally show ?thesis .
qed

lemma C_algebra: "class.C_algebra (+) (⊙) (1::'a::C_algebra) 0 (≤) (<) star"
proof
fix x y :: 'a and n :: nat
show "(x + y)⇧⋆ = (x⇧⋆ ⊙ y)⇧⋆ ⊙ x⇧⋆"
by (metis C11_var opp_mult_def)
show "(x ⊙ y)⇧⋆ = 1 + x ⊙ (y ⊙ x)⇧⋆ ⊙ y"
by (metis C12 mult.assoc opp_mult_def)
show "(x⇧⋆)⇧⋆ = x⇧⋆"
by (metis C13)
show "x⇧⋆ = power.power 1 (⊙) x (n + 1)⇧⋆ ⊙ dioid_one_zero.powsum (+) (⊙) 1 0 x 0 n"
by (metis C14_dual opp_mult_def opp_power_def opp_powsum_def)
qed (simp_all add: opp_mult_def mult.assoc distrib_left)

subsection ‹Boffa's Axioms›

text ‹Boffa's two axiomatisations of Regular Algebra from~\<^cite>‹"Boffa1" and "Boffa2"›.›

class B1_algebra = conway_dioid +
assumes R: "x ⋅ x = x ⟹ x⇧⋆ = 1 + x"

class B2_algebra = star_dioid +
assumes B21: "1 + x ≤ x⇧⋆"
and B22 [simp]: "x⇧⋆ ⋅ x⇧⋆ = x⇧⋆"
and B23: "⟦ 1 + x ≤ y; y ⋅ y = y ⟧ ⟹ x⇧⋆ ≤ y"

lemma (in B1_algebra) B1_algebra:
"class.B1_algebra (+) (⊙) 1 0 (≤) (<) star"
proof
fix x y z :: 'a
show "x ⊙ y ⊙ z = x ⊙ (y ⊙ z)"
by (metis mult.assoc opp_mult_def)
show "(x + y) ⊙ z = x ⊙ z + y ⊙ z"
by (metis distrib_left opp_mult_def)
show "x + x = x"
show "1 ⊙ x = x"
by (metis mult_oner opp_mult_def)
show "x ⊙ 1 = x"
by (metis mult_onel opp_mult_def)
show "0 + x = x"
show "0 ⊙ x = 0"
by (metis annir opp_mult_def)
show "x ⊙ (y + z) = x ⊙ y + x ⊙ z"
by (metis distrib_right opp_mult_def)
show "x ⊙ 0 = 0"
by (metis annil opp_mult_def)
show "(x + y)⇧⋆ = (x⇧⋆ ⊙ y)⇧⋆ ⊙ x⇧⋆"
by (metis C11_var opp_mult_def)
show "(x ⊙ y)⇧⋆ = 1 + x ⊙ (y ⊙ x)⇧⋆ ⊙ y"
by (metis C12 mult.assoc opp_mult_def)
show "x ⊙ x = x ⟹ x⇧⋆ = 1 + x"
by (metis R opp_mult_def)
qed

lemma (in B2_algebra) B2_algebra:
"class.B2_algebra (+) (⊙) 1 0 (≤) (<) star"
proof
fix x y z :: 'a
show "x ⊙ y ⊙ z = x ⊙ (y ⊙ z)"
by (metis mult.assoc opp_mult_def)
show "(x + y) ⊙ z = x ⊙ z + y ⊙ z"
by (metis distrib_left times.opp_mult_def)
show "x + x = x"
show "1 ⊙ x = x"
by (metis mult_oner opp_mult_def)
show "x ⊙ 1 = x"
by (metis mult_onel opp_mult_def)
show "0 + x = x"
show "0 ⊙ x = 0"
by (metis annir opp_mult_def)
show "x ⊙ (y + z) = x ⊙ y + x ⊙ z"
by (metis distrib_right opp_mult_def)
show "x ⊙ 0 = 0"
by (metis annil opp_mult_def)
show "1 + x ≤ x⇧⋆"
by (metis B21)
show "x⇧⋆ ⊙ x⇧⋆ = x⇧⋆"
by (metis B22 opp_mult_def)
show "⟦ 1 + x ≤ y; y ⊙ y = y ⟧ ⟹ x⇧⋆ ≤ y"
by (metis B23 opp_mult_def)
qed

instance B1_algebra ⊆ B2_algebra
proof
fix x y :: 'a
show "1 + x ≤ x⇧⋆"
by (metis C12 add_iso_r distrib_right join.sup.cobounded1 mult_onel)
show two: "x⇧⋆ ⋅ x⇧⋆ = x⇧⋆"
by (metis (no_types, lifting) C11_var C12 R add_idem' mult_onel mult_oner)
show "⟦ 1 + x ≤ y; y ⋅ y = y ⟧ ⟹ x⇧⋆ ≤ y"
by (metis (no_types, lifting) C11_var R two distrib_left join.sup.bounded_iff less_eq_def mult.assoc mult.right_neutral)
qed

context B2_algebra
begin

lemma star_ref: "1 ≤ x⇧⋆"
using local.B21 by auto

lemma star_plus_one [simp]: "1 + x⇧⋆ = x⇧⋆"
by (metis less_eq_def star_ref)

lemma star_trans: "x⇧⋆ ⋅ x⇧⋆ ≤ x⇧⋆"
by (metis B22 order_refl)

lemma star_trans_eq [simp]: "x⇧⋆ ⋅ x⇧⋆ = x⇧⋆"
by (metis B22)

lemma star_invol [simp]: "(x⇧⋆)⇧⋆ = x⇧⋆"
by (metis B21 B22 B23 order.antisym star_plus_one)

lemma star_1l: "x ⋅ x⇧⋆ ≤ x⇧⋆"
by (metis local.B21 local.join.sup.boundedE local.mult_isor local.star_trans_eq)

lemma star_one [simp]: "1⇧⋆ = 1"
by (metis B23 add_idem order.antisym mult_oner order_refl star_ref)

lemma star_subdist:  "x⇧⋆ ≤ (x + y)⇧⋆"
by (meson local.B21 local.B23 local.join.sup.bounded_iff local.star_trans_eq)

lemma star_iso: "x ≤ y ⟹ x⇧⋆ ≤ y⇧⋆"
by (metis less_eq_def star_subdist)

lemma star2: "(1 + x)⇧⋆ = x⇧⋆"
by (metis B21 add.commute less_eq_def star_invol star_subdist)

lemma star_unfoldl: "1 + x ⋅ x⇧⋆ ≤ x⇧⋆"
by (metis local.join.sup.bounded_iff star_1l star_ref)

lemma star_unfoldr: "1 + x⇧⋆ ⋅ x ≤ x⇧⋆"
by (metis (full_types) B21 local.join.sup.bounded_iff mult_isol star_trans_eq)

lemma star_ext: "x ≤ x⇧⋆"
by (metis B21 local.join.sup.bounded_iff)

lemma star_1r: "x⇧⋆ ⋅ x ≤ x⇧⋆"
by (metis mult_isol star_ext star_trans_eq)

lemma star_unfoldl_eq [simp]: "1 + x ⋅ x⇧⋆ = x⇧⋆"
proof -
have "(1 + x ⋅ x⇧⋆) ⋅ (1 + x ⋅ x⇧⋆) = 1 ⋅ (1 + x ⋅ x⇧⋆) + x ⋅ x⇧⋆ ⋅ (1 + x ⋅ x⇧⋆)"
by (metis distrib_right)
also have "... = 1 + x ⋅ x⇧⋆ + (x ⋅ x⇧⋆ ⋅ x ⋅ x⇧⋆)"
also have "... = 1 + x ⋅ x⇧⋆"
finally show ?thesis
by (metis B23 local.join.sup.mono local.join.sup.cobounded1 distrib_left order.eq_iff mult_1_right star_plus_one star_unfoldl)
qed

lemma star_unfoldr_eq [simp]: "1 + x⇧⋆ ⋅ x = x⇧⋆"
proof -
have "(1 + x⇧⋆ ⋅ x) ⋅ (1 + x⇧⋆ ⋅ x) = 1 ⋅ (1 + x⇧⋆ ⋅ x) + x⇧⋆ ⋅ x ⋅ (1 + x⇧⋆ ⋅ x)"
by (metis distrib_right)
also have "... = 1 + x⇧⋆ ⋅ x + (x⇧⋆ ⋅ x ⋅ x⇧⋆ ⋅ x)"
also have "... = 1 + x⇧⋆ ⋅x"
by (metis add_assoc' distrib_left mult.assoc mult_oner distrib_right' star_trans_eq star_unfoldl_eq)
finally show ?thesis
by (metis B21 B23 add.commute local.join.sup.mono local.join.sup.cobounded1 order.eq_iff eq_refl mult_1_left distrib_right' star_unfoldl_eq star_unfoldr)
qed

lemma star_prod_unfold_le: "(x ⋅ y)⇧⋆ ≤ 1 + x ⋅ (y ⋅ x)⇧⋆ ⋅ y"
proof -
have "(1 + x ⋅ (y ⋅ x)⇧⋆ ⋅ y) ⋅ (1 + x ⋅ (y ⋅ x)⇧⋆ ⋅ y) =
1 ⋅ (1 + x ⋅ (y ⋅ x)⇧⋆ ⋅ y) + (x ⋅ (y ⋅ x)⇧⋆ ⋅ y) ⋅ (1 + x ⋅ (y ⋅ x)⇧⋆ ⋅ y)"
by (metis distrib_right')
also have "... = 1 + x ⋅(y ⋅ x)⇧⋆ ⋅ y + x ⋅ (y ⋅ x)⇧⋆ ⋅ y ⋅ x ⋅ (y ⋅ x)⇧⋆ ⋅ y"
by (metis add.assoc local.join.sup.cobounded1  distrib_left less_eq_def mult_1_right mult.assoc mult_onel)
finally have "(1 + x ⋅ (y ⋅ x)⇧⋆ ⋅ y) ⋅ (1 + x ⋅ (y ⋅ x)⇧⋆ ⋅ y) = 1 + x ⋅ (y ⋅ x)⇧⋆ ⋅ y"
by (metis add.assoc  distrib_left distrib_right mult.assoc mult_oner star_trans_eq star_unfoldr_eq)
moreover have "(x ⋅ y) ≤ 1 + x ⋅ (y ⋅ x)⇧⋆ ⋅ y"
by (metis local.join.sup.cobounded2 mult_1_left mult.assoc mult_double_iso order_trans star_ref)
ultimately show ?thesis
qed

lemma star_prod_unfold [simp]: " 1 + x ⋅ (y ⋅ x)⇧⋆ ⋅ y = (x ⋅ y)⇧⋆"
proof -
have "1 + x ⋅ (y ⋅ x)⇧⋆ ⋅ y ≤ 1 + x ⋅ (1 + y ⋅ (x ⋅ y)⇧⋆ ⋅ x) ⋅ y"
by (metis local.join.sup.mono mult_double_iso order_refl star_prod_unfold_le)
also have "... = 1 + x ⋅ y + x ⋅ y ⋅ (x ⋅ y)⇧⋆ ⋅ x ⋅ y"
by (metis add.assoc distrib_left mult_1_left mult.assoc distrib_right')
finally have "1 + x ⋅ (y ⋅ x)⇧⋆ ⋅ y ≤ (x ⋅ y)⇧⋆"
by (metis add.assoc distrib_left mult_1_right mult.assoc star_unfoldl_eq star_unfoldr_eq)
thus ?thesis
by (metis order.antisym star_prod_unfold_le)
qed

lemma star_slide1: "(x ⋅ y)⇧⋆ ⋅ x ≤ x ⋅ (y ⋅ x)⇧⋆"
proof -
have "(x ⋅ y)⇧⋆ ⋅ x = (1 + x ⋅ (y ⋅ x)⇧⋆ ⋅ y) ⋅ x"
by (metis star_prod_unfold)
also have "... = (x + x ⋅ (y ⋅ x)⇧⋆ ⋅ y ⋅ x)"
by (metis mult_onel distrib_right')
also have "... = x ⋅ (1 + (y ⋅ x)⇧⋆ ⋅ y ⋅ x)"
by (metis distrib_left mult.assoc mult_oner)
finally show ?thesis
by (metis eq_refl mult.assoc star_unfoldr_eq)
qed

lemma star_slide_var1: "x⇧⋆ ⋅ x ≤ x ⋅ x⇧⋆"
by (metis mult_onel mult_oner star_slide1)

lemma star_slide: "(x ⋅ y)⇧⋆ ⋅ x = x ⋅ (y ⋅ x)⇧⋆"
proof (rule order.antisym)
show "(x ⋅ y)⇧⋆ ⋅ x ≤ x ⋅ (y ⋅ x)⇧⋆"
by (metis star_slide1)
have "x ⋅ (y ⋅ x)⇧⋆ = x ⋅ (1 + y ⋅ (x ⋅ y)⇧⋆ ⋅ x)"
by (metis star_prod_unfold)
also have "... = x + x ⋅ y ⋅ (x ⋅ y)⇧⋆ ⋅ x"
by (metis distrib_left mult.assoc mult_oner)
also have "... = (1 + x ⋅ y ⋅ (x ⋅ y)⇧⋆) ⋅ x"
by (metis mult_onel distrib_right')
finally show "x ⋅ (y ⋅ x)⇧⋆ ≤ (x ⋅ y)⇧⋆ ⋅ x"
by (metis mult_isor star_unfoldl)
qed

lemma star_rtc1: "1 + x + x⇧⋆ ⋅ x⇧⋆ ≤ x⇧⋆"
using local.B21 local.join.sup_least local.star_trans by blast

lemma star_rtc1_eq: "1 + x + x⇧⋆ ⋅ x⇧⋆ = x⇧⋆"
by (metis B21 B22 less_eq_def)

lemma star_subdist_var_1: "x ≤ (x + y)⇧⋆"
using local.join.le_supE local.star_ext by blast

lemma star_subdist_var_2: "x ⋅ y ≤ (x + y)⇧⋆"
by (metis (full_types) local.join.le_supE mult_isol_var star_ext star_trans_eq)

lemma star_subdist_var_3: "x⇧⋆ ⋅ y⇧⋆ ≤ (x + y)⇧⋆"
by (metis add.commute mult_isol_var star_subdist star_trans_eq)

lemma R_lemma:
assumes "x ⋅ x = x"
shows "x⇧⋆ = 1 + x"
proof (rule order.antisym)
show "1 + x ≤ x⇧⋆"
by (metis B21)
have "(1 + x) ⋅ (1 + x) = 1 + x"
thus "x⇧⋆ ≤ 1 + x"
by (metis B23 order_refl)
qed

lemma star_denest_var_0: "(x + y)⇧⋆ = (x⇧⋆ ⋅ y)⇧⋆ ⋅ x⇧⋆"
proof (rule order.antisym)
have one_below: "1 ≤ (x⇧⋆ ⋅ y)⇧⋆ ⋅ x⇧⋆"
by (metis mult_isol_var star_one star_ref star_trans_eq)
have x_below: "x ≤ (x⇧⋆ ⋅ y)⇧⋆ ⋅ x⇧⋆"
by (metis mult_isol mult_oner order_trans star_ext star_ref star_slide)
have y_below: "y ≤ (x⇧⋆ ⋅ y)⇧⋆ ⋅ x⇧⋆"
by (metis mult_isol_var mult_onel mult_oner order_trans star_ext star_slide star_unfoldl_eq subdistl)
from one_below x_below y_below have "1 + x + y ≤ (x⇧⋆ ⋅ y)⇧⋆ ⋅ x⇧⋆"
by simp
moreover have "(x⇧⋆ ⋅ y)⇧⋆ ⋅ x⇧⋆ ⋅ (x⇧⋆ ⋅ y)⇧⋆ ⋅ x⇧⋆ = (x⇧⋆ ⋅ y)⇧⋆ ⋅ x⇧⋆"
by (metis star_trans_eq star_slide mult.assoc)
ultimately show "(x + y)⇧⋆ ≤ (x⇧⋆ ⋅ y)⇧⋆ ⋅ x⇧⋆"
show "(x⇧⋆ ⋅ y)⇧⋆ ⋅ x⇧⋆ ≤ (x + y)⇧⋆"
by (metis (full_types) add.commute mult_isol_var star_invol star_iso star_subdist_var_1 star_trans_eq)
qed

lemma star_denest: "(x + y)⇧⋆ = (x⇧⋆ ⋅ y⇧⋆)⇧⋆"
by (metis R_lemma add.commute star_denest_var_0 star_plus_one star_prod_unfold star_slide star_trans_eq)

lemma star_sum_var: "(x + y)⇧⋆  = (x⇧⋆ + y⇧⋆)⇧⋆"
by (metis star_denest star_invol)

lemma star_denest_var: "(x + y)⇧⋆ = x⇧⋆ ⋅ (y ⋅ x⇧⋆)⇧⋆"
by (metis star_denest_var_0 star_slide)

lemma star_denest_var_2: "(x⇧⋆ ⋅ y⇧⋆)⇧⋆ = x⇧⋆ ⋅ (y ⋅ x⇧⋆)⇧⋆"
by (metis star_denest star_denest_var)

lemma star_denest_var_3: "(x⇧⋆ ⋅ y⇧⋆)⇧⋆ = x⇧⋆ ⋅ (y⇧⋆ ⋅ x⇧⋆)⇧⋆"
by (metis B22 add_comm mult.assoc star_denest star_denest_var_2)

lemma star_denest_var_4:  "(x⇧⋆ ⋅ y⇧⋆)⇧⋆ = (y⇧⋆ ⋅ x⇧⋆)⇧⋆"

lemma star_denest_var_5: "x⇧⋆ ⋅ (y ⋅ x⇧⋆)⇧⋆ = y⇧⋆ ⋅ (x ⋅ y⇧⋆)⇧⋆"

lemma star_denest_var_6: "(x + y)⇧⋆ = x⇧⋆ ⋅ y⇧⋆ ⋅ (x + y)⇧⋆"
by (metis mult.assoc star_denest star_denest_var_3)

lemma star_denest_var_7: "(x + y)⇧⋆ = (x + y)⇧⋆ ⋅ x⇧⋆ ⋅ y⇧⋆"
by (metis star_denest star_denest_var star_denest_var_3 star_denest_var_5 star_slide)

lemma star_denest_var_8: "(x⇧⋆ ⋅ y⇧⋆)⇧⋆ = x⇧⋆ ⋅ y⇧⋆ ⋅ (x⇧⋆ ⋅ y⇧⋆)⇧⋆"
by (metis star_denest star_denest_var_6)

lemma star_denest_var_9: " (x⇧⋆ ⋅ y⇧⋆)⇧⋆ = (x ⇧⋆ ⋅ y⇧⋆)⇧⋆ ⋅ x⇧⋆ ⋅ y⇧⋆"
by (metis star_denest star_denest_var_7)

lemma star_slide_var: "x⇧⋆ ⋅ x = x ⋅ x⇧⋆"
by (metis mult_1_left mult_oner star_slide)

lemma star_sum_unfold: "(x + y)⇧⋆ = x⇧⋆ + x⇧⋆ ⋅ y ⋅ (x + y)⇧⋆"
by (metis distrib_left mult_1_right mult.assoc star_denest_var star_unfoldl_eq)

lemma troeger: "x⇧⋆ ⋅ (y ⋅ ((x + y)⇧⋆ ⋅ z) + z) = (x + y)⇧⋆ ⋅ z"
proof -
have "x⇧⋆ ⋅ (y ⋅ ((x + y)⇧⋆ ⋅ z) + z) = (x⇧⋆ + x⇧⋆ ⋅ y ⋅ (x + y)⇧⋆) ⋅ z"
by (metis add_comm distrib_left mult.assoc distrib_right')
thus ?thesis
by (metis star_sum_unfold)
qed

lemma meyer_1: "x⇧⋆ = (1 + x) ⋅ (x ⋅ x)⇧⋆"
proof (rule order.antisym)
have "(1 + x) ⋅ (x ⋅ x)⇧⋆ ⋅ (1 + x) ⋅ (x ⋅ x)⇧⋆ = ((x ⋅ x)⇧⋆ + x ⋅ (x ⋅ x)⇧⋆) ⋅ ((x ⋅ x)⇧⋆ + x ⋅ (x ⋅ x)⇧⋆)"
by (metis mult.assoc mult_onel distrib_right')
also have "... = ((x ⋅ x)⇧⋆ + x ⋅ (x ⋅ x)⇧⋆) ⋅ (x ⋅ x)⇧⋆ + ((x ⋅ x)⇧⋆ + x ⋅ (x ⋅ x)⇧⋆) ⋅ x ⋅ (x ⋅ x)⇧⋆"
by (metis distrib_left mult.assoc)
also have "... = (x ⋅ x) ⇧⋆ ⋅ (x ⋅ x)⇧⋆ + x ⋅ (x ⋅ x)⇧⋆ ⋅ (x ⋅ x)⇧⋆ + (x ⋅ x)⇧⋆ ⋅ x ⋅ (x ⋅ x)⇧⋆ + x ⋅ (x ⋅ x)⇧⋆ ⋅ x ⋅ (x ⋅ x)⇧⋆"
by (metis combine_common_factor distrib_right)
also have "... = (x ⋅ x)⇧⋆ + x ⋅ (x ⋅ x)⇧⋆ + x ⋅ x ⋅ (x ⋅ x)⇧⋆"
also have "... = 1 + x ⋅ x ⋅ (x ⋅ x)⇧⋆ + x ⋅ (x ⋅ x)⇧⋆ + x ⋅ x ⋅ (x ⋅ x)⇧⋆"
by (metis star_unfoldl_eq)
also have "... = (x ⋅ x)⇧⋆ + x ⋅ (x ⋅ x)⇧⋆"
finally have "(1 + x) ⋅ (x ⋅ x)⇧⋆ ⋅ (1 + x) ⋅ (x ⋅ x)⇧⋆ = (1 + x) ⋅ (x ⋅ x)⇧⋆"
by (metis mult_1_left distrib_right')
moreover have "1 + x ≤ (1 + x) ⋅ (x ⋅ x)⇧⋆"
by (metis mult_1_right star_unfoldl_eq subdistl)
ultimately show "x⇧⋆ ≤ (1 + x) ⋅ (x ⋅ x)⇧⋆"
by (metis B23 mult.assoc)
next
have "(1 + x) ⋅ (x ⋅ x)⇧⋆ = (x ⋅ x)⇧⋆ + x ⋅ (x ⋅ x)⇧⋆"
by (metis mult_1_left distrib_right')
thus "(1 + x) ⋅ (x ⋅ x)⇧⋆ ≤ x⇧⋆"
by (metis local.add_zeror local.join.sup_least local.mult_isol_var local.mult_oner local.star_ext local.star_invol local.star_iso local.star_subdist_var_2 local.star_trans_eq local.subdistl_eq)
qed

lemma star_zero [simp]: "0⇧⋆ = 1"

lemma star_subsum [simp]: "x⇧⋆ + x⇧⋆ ⋅ x = x⇧⋆"

lemma prod_star_closure: "x ≤ z⇧⋆ ⟹ y ≤ z⇧⋆ ⟹ x ⋅ y ≤ z⇧⋆"
by (metis mult_isol_var star_trans_eq)

end

sublocale B2_algebra ⊆ B1_algebra
by unfold_locales (metis star_denest_var_0, metis star_prod_unfold, metis R_lemma)

context B2_algebra
begin

lemma power_le_star: "x⇗n⇖ ≤ x⇧⋆"
by (induct n, simp_all add: star_ref prod_star_closure star_ext)

lemma star_power_slide:
assumes "k ≤ n"
shows "x⇗k ⇖⋅ (x⇗n⇖)⇧⋆ = (x⇗n⇖)⇧⋆ ⋅ x⇗k⇖"
proof -
from assms have "x⇗k ⇖⋅ (x⇗n⇖)⇧⋆ = (x⇗k ⇖⋅ x⇗n-k⇖)⇧⋆ ⋅ x⇗k⇖"
with assms show ?thesis
qed

lemma powsum_le_star: "x⇘m⇙⇗n⇖ ≤ x⇧⋆"
by (induct n, simp_all add:  powsum2, metis power_le_star, metis  power_Suc power_le_star)

lemma star_sum_power_slide:
assumes "m ≤ n"
shows "x⇘0⇙⇗m  ⇖⋅ (x⇗n⇖)⇧⋆ = (x⇗n⇖)⇧⋆ ⋅ x⇘0⇙⇗m⇖"
using assms
proof (induct m)
case 0 thus ?case
by (metis mult_onel mult_oner powsum_00)
next
case (Suc m) note hyp = this
have "x⇘0⇙⇗Suc m⇖ ⋅ (x⇗n⇖)⇧⋆ = (x⇘0⇙⇗m⇖ + x⇗Suc m⇖) ⋅ (x⇗n⇖)⇧⋆"
also have "... = x⇘0⇙⇗m ⇖⋅ (x⇗n⇖)⇧⋆ + x⇗Suc m ⇖⋅ (x⇗n⇖)⇧⋆"
by (metis distrib_right')
also have "... = (x⇗n⇖)⇧⋆ ⋅ x⇘0⇙⇗m⇖ + x⇗Suc m ⇖⋅ (x⇗n⇖)⇧⋆"
by (metis Suc.hyps Suc.prems Suc_leD)
also have "... = (x⇗n⇖)⇧⋆ ⋅ x⇘0⇙⇗m⇖ + (x⇗n⇖)⇧⋆ ⋅ x⇗Suc m⇖"
by (metis Suc.prems star_power_slide)
also have "... = (x⇗n⇖)⇧⋆ ⋅ (x⇘0⇙⇗m⇖ + x⇗Suc m⇖)"
by (metis distrib_left)
finally show ?case
qed

lemma aarden_aux:
assumes "y ≤ y ⋅ x + z"
shows "y ≤ y ⋅ x⇗(Suc n) ⇖+ z ⋅ x⇧⋆"
proof (induct n)
case 0
have "y ⋅ x + z ≤ y ⋅ x⇗(Suc 0)⇖+ z ⋅ x⇧⋆"
thus ?case
by (metis assms order_trans)
next
case (Suc n)
have "y ⋅ x + z ≤ (y ⋅ x⇗(Suc n) ⇖+ z ⋅ x⇧⋆) ⋅ x + z"
also have "... = y ⋅ x⇗(Suc n) ⇖⋅ x + z ⋅ (x⇧⋆ ⋅ x + 1)"
by (subst distrib_right, metis add_assoc' distrib_left mult.assoc mult_oner)
finally show ?case
by (metis add.commute assms mult.assoc order_trans power_Suc2 star_unfoldr_eq)
qed

lemma conway_powerstar1: "(x⇗n+1⇖)⇧⋆ ⋅ x⇘0⇙⇗n ⇖⋅ (x⇗n+1⇖)⇧⋆ ⋅ x⇘0⇙⇗n⇖  = (x⇗n+1⇖)⇧⋆ ⋅ x⇘0⇙⇗n⇖"
proof (cases n)
case 0 thus ?thesis
by simp
next
case (Suc m) thus ?thesis
proof -
assume assm: "n = Suc m"
have "(x⇗m+2⇖)⇧⋆ ⋅ x⇘0⇙⇗m+1 ⇖⋅ (x⇗m+2⇖)⇧⋆ ⋅ x⇘0⇙⇗m+1⇖  = (x⇗m+2⇖)⇧⋆ ⋅ (x⇗m+2⇖)⇧⋆ ⋅ x⇘0⇙⇗m+1 ⇖⋅ x⇘0⇙⇗m+1⇖"
by (subgoal_tac "m + 1 ≤ m + 2", metis mult.assoc star_sum_power_slide, simp)
also have "...  = (x⇗m+2⇖)⇧⋆ ⋅ x⇘0⇙⇗m+1 ⇖⋅ x⇘0⇙⇗m+1⇖"
by (metis star_trans_eq)
also have "...  =  (x⇗m+2⇖)⇧⋆ ⋅ x⇘0⇙⇗(Suc m)+(Suc m)⇖"
also have "... =  (x⇗m+2⇖)⇧⋆ ⋅ (x⇘0⇙⇗Suc m ⇖+ x⇘m + 2⇙⇗m⇖)"
also have "... =  (x⇗m+2⇖)⇧⋆ ⋅ x⇘0⇙⇗Suc m ⇖+ (x⇗m+2⇖)⇧⋆ ⋅ x⇘(m + 2)+ 0⇙⇗m⇖"
also have "... =  (x⇗m+2⇖)⇧⋆ ⋅ x⇘0⇙⇗Suc m ⇖+ (x⇗m+2⇖)⇧⋆ ⋅ x⇗m+2 ⇖⋅ x⇘0⇙⇗m⇖"
by (subst powsum_shift[THEN sym], metis mult.assoc)
also have "... =  (x⇗m+2⇖)⇧⋆ ⋅ (x⇘0⇙⇗m ⇖+  x⇗m+1⇖) + (x⇗m+2⇖)⇧⋆ ⋅ x⇗m+2 ⇖⋅ x⇘0⇙⇗m⇖"
also have "... =  (x⇗m+2⇖)⇧⋆ ⋅ x⇘0⇙⇗m ⇖+ (x⇗m+2⇖)⇧⋆ ⋅ x⇗m+2 ⇖⋅ x⇘0⇙⇗m ⇖+ (x⇗m+2⇖)⇧⋆ ⋅ x⇗m+1⇖"
also have "... =  (x⇗m+2⇖)⇧⋆ ⋅ x⇘0⇙⇗m ⇖+ (x⇗m+2⇖)⇧⋆ ⋅ x⇘0⇙⇗m ⇖+ (x⇗m+2⇖)⇧⋆ ⋅ x⇗m+1⇖"
also have "... =  (x⇗m+2⇖)⇧⋆ ⋅ (x⇘0⇙⇗m ⇖+ x⇗m+1⇖)"
also have "... = (x⇗m+2⇖)⇧⋆ ⋅ x⇘0⇙⇗m+1⇖"
finally  show ?thesis
qed
qed

lemma conway_powerstar2: "1 + x ≤ (x⇗n+1⇖)⇧⋆ ⋅ x⇘0⇙⇗n⇖"
proof (cases n)
case 0 show ?thesis
using "0" local.B21 by auto
next
case (Suc m) show ?thesis
proof -
have one: "x ≤ (x⇗m+2⇖)⇧⋆ ⋅ x⇘0⇙⇗m+1⇖"
by (metis Suc_eq_plus1 powsum_ext  mult_isor mult_onel order_trans star_ref)
have two: "1 ≤ (x⇗m+2⇖)⇧⋆ ⋅ x⇘0⇙⇗m+1⇖"
by (metis Suc_eq_plus1 local.join.le_supE mult_isor mult_onel powsum_split_var1 star_ref)
from one two show ?thesis
by (metis Suc Suc_eq_plus1 add_2_eq_Suc' local.join.sup_least)
qed
qed

theorem powerstar: "x⇧⋆ = (x⇗n+1⇖)⇧⋆ ⋅ x⇘0⇙⇗n⇖"
proof (rule order.antisym)
show "x⇧⋆ ≤ (x⇗n+1⇖)⇧⋆ ⋅ x⇘0⇙⇗n⇖"
by (metis conway_powerstar1 conway_powerstar2 mult.assoc B23)
have "(x⇗n+1⇖)⇧⋆ ⋅ x⇘0⇙⇗n⇖ ≤ (x⇧⋆)⇧⋆ ⋅ x⇘0⇙⇗n⇖"
by (metis mult_isor power_le_star star_iso)
also have "... = x⇧⋆ ⋅ x⇘0⇙⇗n⇖"
by (metis star_invol)
also have "... ≤ x⇧⋆ ⋅ x⇧⋆"
finally show "(x⇗n+1⇖)⇧⋆ ⋅ x⇘0⇙⇗n ⇖≤ x⇧⋆"
by (metis star_trans_eq)
qed

end

sublocale B2_algebra ⊆ strong_conway_dioid
by  unfold_locales (metis star_invol)

sublocale B2_algebra ⊆ C_algebra
by unfold_locales (metis powerstar)

text ‹The following fact could neither be verified nor falsified in Isabelle. It does not hold for other reasons.›

lemma (in C_algebra) "x⋅x = x ⟶ x⇧⋆ = 1+x"
oops

subsection ‹Boffa Monoid Identities›

typedef ('a , 'b) boffa_mon = "{f :: 'a::{finite,monoid_mult}  ⇒ 'b::B1_algebra. True}"
by auto

notation
Rep_boffa_mon ("_⇘_⇙")

lemma "finite (range (Rep_boffa_mon M))"
by (metis finite_code finite_imageI)

abbreviation boffa_pair :: "('a, 'b) boffa_mon ⇒ 'a::{finite,monoid_mult} ⇒ 'a ⇒ 'b::B1_algebra" where
"boffa_pair x i j ≡ ∑ { x⇘k⇙ | k. i⋅k = j}"

notation
boffa_pair ("_⇘_,_⇙")

abbreviation conway_assms where
"conway_assms x ≡ (∀ i j. (x⇘i ⇙⋅ x⇘j⇙ ≤ x⇘i⋅j⇙) ∧ (x⇘i,i⇙)⇧⋆ = x⇘i,i⇙)"

lemma pair_one: "x⇘1,1⇙ = x⇘1⇙"
by (simp)

definition conway_assm1 where "conway_assm1 x = (∀ i j. x⇘i ⇙⋅ x⇘j⇙ ≤ x⇘i⋅j⇙)"
definition conway_assm2 where "conway_assm2 x = (∀i. x⇘i,i⇙⇧⋆ = x⇘i,i⇙)"

lemma pair_star:
assumes "conway_assm2 x"
shows "x⇘1⇙⇧⋆ = x⇘1⇙"
proof -
have "x⇘1⇙⇧⋆ = x⇘1,1⇙⇧⋆"
by simp
also from assms have "... = x⇘1,1⇙"
by (metis (mono_tags) conway_assm2_def)
finally show ?thesis
by simp
qed

lemma conway_monoid_one:
assumes "conway_assm2 x"
shows "x⇘1⇙ = 1 + x⇘1⇙"
proof -
from assms have "x⇘1⇙ = x⇘1⇙⇧⋆"
by (metis pair_star)
thus ?thesis
by (metis star_plus_one)
qed

lemma conway_monoid_split:
assumes "conway_assm2 x"
shows "∑ {x⇘i ⇙| i . i ∈ UNIV} = 1 + ∑ {x⇘i ⇙| i . i ∈ UNIV}"
proof -
have "∑ {x⇘i ⇙| i . i ∈ UNIV} = ∑ {x⇘i ⇙| i . i ∈ (insert 1 (UNIV - {1}))}"
by (metis UNIV_I insert_Diff_single insert_absorb)
also have "... = ∑ (Rep_boffa_mon x ` (insert 1 (UNIV - {1})))"
by (metis fset_to_im)
also have "... = x⇘1⇙ + ∑ (Rep_boffa_mon x ` (UNIV - {1}))"
by (subst sum_fun_insert, auto)
also have "... = x⇘1⇙ + ∑ { x⇘i⇙ | i. i∈(UNIV - {1})}"
by (metis fset_to_im)
also from assms have unfld:"... = 1 + x⇘1⇙ + ∑ { x⇘i⇙ | i. i∈(UNIV - {1})}"
by (metis (lifting, no_types) conway_monoid_one)
finally show ?thesis
by (metis (lifting, no_types) ac_simps unfld)
qed

lemma boffa_mon_aux1: "{x⇘i⋅j ⇙| i j. i ∈ UNIV ∧ j ∈ UNIV} = {x⇘i⇙ | i. i ∈ UNIV}"
by (auto, metis monoid_mult_class.mult.left_neutral)

lemma sum_intro' [intro]:
"⟦finite (A :: 'a::join_semilattice_zero set); finite B; ∀a∈A. ∃b∈B. a ≤ b ⟧ ⟹ ∑A ≤ ∑B"
by (metis sum_intro)

lemma boffa_aux2:
"conway_assm1 x ⟹
∑{x⇘i⇙⋅x⇘j ⇙| i j. i ∈ UNIV ∧ j ∈ UNIV} ≤ ∑{x⇘i⋅j⇙ | i j. i ∈ UNIV ∧ j ∈ UNIV}"
unfolding conway_assm1_def
by force

lemma boffa_aux3:
assumes "conway_assm1 x"
shows "(∑ {x⇘i⇙ | i. i∈UNIV}) + (∑ {x⇘i ⇙⋅ x⇘j⇙ | i j . i∈UNIV ∧ j∈UNIV}) = (∑ {x⇘i⇙ | i. i∈UNIV})"
proof -
from assms
have "(∑ {x⇘i⇙ | i. i∈UNIV}) + (∑ {x⇘i ⇙⋅ x⇘j⇙ | i j . i∈UNIV ∧ j∈UNIV}) ≤ (∑ {x⇘i⇙ | i. i∈UNIV})+(∑ {x⇘i⋅j⇙ | i j . i∈UNIV ∧ j∈UNIV})"
apply (subst boffa_aux2)
by simp_all
also have "... = (∑ {x⇘i⇙ | i. i∈UNIV})"
ultimately show ?thesis
qed

lemma conway_monoid_identity:
assumes "conway_assm1 x" "conway_assm2 x"
shows "(∑ {x⇘i⇙|i. i∈UNIV})⇧⋆ = (∑ {x⇘i⇙| i. i∈UNIV})"
proof -
have one:"(∑ {x⇘i⇙|i. i∈UNIV}) ⋅ (∑ {x⇘i⇙|i. i∈UNIV}) = (1 + (∑ {x⇘i⇙|i. i∈UNIV})) ⋅ (1 + (∑ {x⇘i⇙|i. i∈UNIV}))"
by (metis (mono_tags) assms(2) conway_monoid_split)
also have "... = 1 + (∑ {x⇘i⇙|i. i∈UNIV}) + ((∑ {x⇘i⇙|i. i∈UNIV}) ⋅ (∑ {x⇘i⇙|i. i∈UNIV}))"
by (metis (lifting, no_types) calculation less_eq_def mult_isol mult_isol_equiv_subdistl mult_oner)
also have "... = 1 + (∑ {x⇘i⇙|i. i∈UNIV}) + (∑ {x⇘i ⇙⋅ x⇘j⇙ | i j. i∈UNIV ∧ j∈UNIV})"
by (simp only: dioid_sum_prod finite_UNIV)
finally have "∑ {x⇘i⇙ |i. i ∈ UNIV} ⋅ ∑ {x⇘i⇙ |i. i ∈ UNIV} = ∑ {x⇘i⇙ |i. i ∈ UNIV}"
apply (simp only:)
proof -
assume a1: "∑{x⇘i⇙ |i. i ∈ UNIV} ⋅ ∑{x⇘i⇙ |i. i ∈ UNIV} = 1 + ∑{x⇘i⇙ |i. i ∈ UNIV} + ∑{x⇘i⇙ ⋅ x⇘j⇙ |i j. i ∈ UNIV ∧ j ∈ UNIV}"
hence "∑{x⇘R⇙ |R. R ∈ UNIV} ⋅ ∑{x⇘R⇙ |R. R ∈ UNIV} = ∑{x⇘R⇙ |R. R ∈ UNIV}"
using assms(1) assms(2) boffa_aux3 conway_monoid_split by fastforce
thus "1 + ∑{x⇘i⇙ |i. i ∈ UNIV} + ∑{x⇘i⇙ ⋅ x⇘j⇙ |i j. i ∈ UNIV ∧ j ∈ UNIV} = ∑{x⇘i⇙ |i. i ∈ UNIV}"
using a1 by simp
qed
thus ?thesis
by (metis (mono_tags) one B1_algebra_class.R star_trans_eq)
qed

subsection ‹Conway's Conjectures›

class C0_algebra = strong_conway_dioid +
assumes C0:  "x ⋅ y = y ⋅ z ⟹ x⇧⋆ ⋅ y = y ⋅ z⇧⋆"

class C1l_algebra = strong_conway_dioid +
assumes C1l:  "x ⋅ y ≤ y ⋅ z ⟹ x⇧⋆ ⋅ y ≤ y ⋅ z⇧⋆"

class C1r_algebra = strong_conway_dioid +
assumes C1r:  "y ⋅ x ≤ z ⋅ y ⟹ y ⋅ x⇧⋆ ≤ z⇧⋆ ⋅ y"

class C2l_algebra = conway_dioid +
assumes C2l: "x = y ⋅ x ⟹ x = y⇧⋆ ⋅ x"

class C2r_algebra = conway_dioid +
assumes C2r: "x = x ⋅ y ⟹ x = x ⋅ y⇧⋆"

class C3l_algebra = conway_dioid +
assumes C3l:  "x ⋅ y ≤ y ⟹ x⇧⋆ ⋅ y ≤ y"

class C3r_algebra = conway_dioid +
assumes C3r:  "y ⋅ x ≤ y ⟹ y ⋅ x⇧⋆ ≤ y"

sublocale C1r_algebra ⊆ dual: C1l_algebra
"(+)" "(⊙)" "1" "0" "(≤)" "(<)" "star"
proof
fix x y z :: 'a
show "x ⊙ y ⊙ z = x ⊙ (y ⊙ z)"
by (metis mult.assoc opp_mult_def)
show "(x + y) ⊙ z = x ⊙ z + y ⊙ z"
by (metis distrib_left opp_mult_def)
show "x + x = x"
show "1 ⊙ x = x"
by (metis mult_oner opp_mult_def)
show "x ⊙ 1 = x"
by (metis mult_onel opp_mult_def)
show "0 + x = x"
show "0 ⊙ x = 0"
by (metis annir opp_mult_def)
show "x ⊙ (y + z) = x ⊙ y + x ⊙ z"
by (metis distrib_right opp_mult_def)
show "x ⊙ 0 = 0"
by (metis annil opp_mult_def)
show "(x + y)⇧⋆ = (x⇧⋆ ⊙ y)⇧⋆ ⊙ x⇧⋆"
by (metis C11_var opp_mult_def)
show "(x ⊙ y)⇧⋆ = 1 + x ⊙ (y ⊙ x)⇧⋆ ⊙ y"
by (metis C12 mult.assoc opp_mult_def)
show "(x⇧⋆)⇧⋆ = x⇧⋆"
by (metis C13)
show "x ⊙ y ≤ y ⊙ z ⟹ x⇧⋆ ⊙ y ≤ y ⊙ z⇧⋆"
by (metis C1r opp_mult_def)
qed

sublocale C2r_algebra ⊆ dual: C2l_algebra
"(+)" "(⊙)" "1" "0" "(≤)" "(<)" "star"
proof
fix x y z :: 'a
show "x ⊙ y ⊙ z = x ⊙ (y ⊙ z)"
by (metis mult.assoc opp_mult_def)
show "(x + y) ⊙ z = x ⊙ z + y ⊙ z"
by (metis distrib_left opp_mult_def)
show "x + x = x"
show "1 ⊙ x = x"
by (metis mult_oner opp_mult_def)
show "x ⊙ 1 = x"
by (metis mult_onel opp_mult_def)
show "0 + x = x"
show "0 ⊙ x = 0"
by (metis annir opp_mult_def)
show "x ⊙ (y + z) = x ⊙ y + x ⊙ z"
by (metis distrib_right opp_mult_def)
show "x ⊙ 0 = 0"
by (metis annil opp_mult_def)
show "(x + y)⇧⋆ = (x⇧⋆ ⊙ y)⇧⋆ ⊙ x⇧⋆"
by (metis C11_var opp_mult_def)
show "(x ⊙ y)⇧⋆ = 1 + x ⊙ (y ⊙ x)⇧⋆ ⊙ y"
by (metis C12 mult.assoc opp_mult_def)
show "x = y ⊙ x ⟹ x = y⇧⋆ ⊙ x"
by (metis C2r opp_mult_def)
qed

sublocale C3r_algebra ⊆ dual: C3l_algebra
"(+)" "(⊙)" "1" "0" "(≤)" "(<)" "star"
proof
fix x y z :: 'a
show "x ⊙ y ⊙ z = x ⊙ (y ⊙ z)"
by (metis mult.assoc opp_mult_def)
show "(x + y) ⊙ z = x ⊙ z + y ⊙ z"
by (metis distrib_left opp_mult_def)
show "x + x = x"
show "1 ⊙ x = x"
by (metis mult_oner opp_mult_def)
show "x ⊙ 1 = x"
by (metis mult_onel opp_mult_def)
show "0 + x = x"
show "0 ⊙ x = 0"
by (metis annir opp_mult_def)
show "x ⊙ (y + z) = x ⊙ y + x ⊙ z"
by (metis distrib_right opp_mult_def)
show "x ⊙ 0 = 0"
by (metis annil opp_mult_def)
show "(x + y)⇧⋆ = (x⇧⋆ ⊙ y)⇧⋆ ⊙ x⇧⋆"
by (metis C11_var opp_mult_def)
show "(x ⊙ y)⇧⋆ = 1 + x ⊙ (y ⊙ x)⇧⋆ ⊙ y"
by (metis C12 mult.assoc opp_mult_def)
show " x ⊙ y ≤ y ⟹ x⇧⋆ ⊙ y ≤ y"
by (metis C3r opp_mult_def)
qed

lemma (in C3l_algebra) k2_var: "z + x ⋅ y ≤ y ⟹ x⇧⋆ ⋅ z ≤ y"
by (metis local.C3l local.join.le_supE local.join.sup.absorb2 local.subdistl)

instance C2l_algebra ⊆ B1_algebra
by (intro_classes, metis C2l monoid_mult_class.mult.left_neutral mult_oner conway_dioid_class.C12)

instance C2r_algebra ⊆  B1_algebra
by (intro_classes, metis C2r conway_dioid_class.C12)

text ‹The following claims are refuted by Nitpick›

lemma (in conway_dioid)
assumes "x ⋅ y = y ⋅ z ⟹ x⇧⋆ ⋅ y = y ⋅ z⇧⋆"
shows "1⇧⋆ = 1"
(*  nitpick [expect=genuine] -- "3-element counterexample"*)
oops

lemma (in conway_dioid)
assumes "x ⋅ y ≤ y ⋅ z ⟹ x⇧⋆ ⋅ y ≤ y ⋅ z⇧⋆"
shows "1⇧⋆ = 1"
(*  nitpick [expect=genuine] -- "3-element counterexample"*)
oops

text ‹The following fact could not be refuted by Nitpick or Quickcheck; but an infinite counterexample exists.›

lemma (in B1_algebra) "x = x⋅y⟶ x = x⋅y⇧⋆"
oops

instance C3l_algebra ⊆ C2l_algebra
by (intro_classes, metis C3l conway_dioid_class.C12 dual_order.antisym join.sup.cobounded1 mult_isol_var mult_onel order_refl)

sublocale C2l_algebra ⊆ C3l_algebra
proof
fix x y
show "x ⋅ y ≤ y ⟹ x⇧⋆ ⋅ y ≤ y"
proof -
assume "x ⋅ y ≤ y"
hence "(x + 1) ⋅ y = y"
by (metis less_eq_def mult_onel distrib_right')
hence "(x + 1)⇧⋆ ⋅ y = y"
by (metis C2l)
hence "x⇧⋆ ⋅ y = y"
by (metis C11 C2l add_comm mult_1_left mult_1_right)
thus "x⇧⋆ ⋅ y ≤ y"
by (metis eq_refl)
qed
qed

sublocale C1l_algebra ⊆ C3l_algebra
by unfold_locales (metis  mult_oner C1l C12 C13 add_zeror annir)

sublocale C3l_algebra ⊆ C1l_algebra
proof
fix x y z
show "(x⇧⋆)⇧⋆ = x⇧⋆"
by (metis local.C11_var local.C12 local.C3l order.eq_iff local.eq_refl local.join.sup.absorb2 local.join.sup_ge1 local.mult_onel local.mult_oner)
show "x ⋅ y ≤ y ⋅ z ⟹ x⇧⋆ ⋅ y ≤ y ⋅ z⇧⋆"
proof -
assume assm: "x ⋅ y ≤ y ⋅ z"
have r1:"y ≤ y ⋅ z⇧⋆"
by (metis C12 mult_isol mult_oner order_prop)
from assm have "x ⋅ y ⋅ z⇧⋆ ≤ y ⋅ z ⋅z⇧⋆"
by (metis mult_isor)
also have "... ≤ y ⋅ z⇧⋆"
by (metis local.C12 local.join.sup_commute local.mult_onel local.mult_oner local.subdistl mult_assoc)
finally have "y + x ⋅ y ⋅ z⇧⋆ ≤ y ⋅ z⇧⋆"
thus "x⇧⋆ ⋅ y ≤ y ⋅ z⇧⋆"
by (metis k2_var mult.assoc)
qed
qed

sublocale C1l_algebra ⊆ C2l_algebra
by (unfold_locales, metis C12 C3l add.commute  local.join.sup.cobounded1 distrib_right less_eq_def mult_1_left order_refl)

sublocale C3r_algebra ⊆ C2r_algebra
by (unfold_locales, metis C12 C3r add.commute  local.join.sup.cobounded1 distrib_left less_eq_def mult_1_right order_refl)

sublocale C2r_algebra ⊆ C3r_algebra
by unfold_locales (metis dual.C3l opp_mult_def)

sublocale C1r_algebra ⊆ C3r_algebra
by unfold_locales (metis dual.C3l opp_mult_def)

sublocale C3r_algebra ⊆ C1r_algebra
by (unfold_locales, metis dual.C13, metis dual.C1l opp_mult_def)

class C1_algebra = C1l_algebra + C1r_algebra

class C2_algebra = C2l_algebra + C2r_algebra

class C3_algebra = C3l_algebra + C3r_algebra

sublocale C0_algebra ⊆ C2_algebra
by unfold_locales (metis C12 C13 add_zeror annil mult_oner mult_onel C0)+

sublocale C2_algebra ⊆ C0_algebra
by unfold_locales (metis C1l C1r order.eq_iff)

sublocale C2_algebra ⊆ C1_algebra ..

sublocale C1_algebra ⊆ C2_algebra ..

sublocale C2_algebra ⊆ C3_algebra ..

sublocale C3_algebra ⊆ C2_algebra ..

subsection ‹Kozen's Kleene Algebras›

text ‹Kozen's Kleene Algebras~\<^cite>‹"Kozen" and "Kozensemi"›.›

class Kl_base = star_dioid +
assumes Kl: "1 + x ⋅ x⇧⋆ ≤ x⇧⋆"

class Kr_base = star_dioid +
assumes Kr: "1 + x⇧⋆ ⋅ x ≤ x⇧⋆"

class K1l_algebra = Kl_base +
assumes star_inductl: "x ⋅ y ≤ y ⟹ x⇧⋆ ⋅ y ≤ y"

class K1r_algebra = Kr_base +
assumes star_inductr: "y ⋅ x ≤ y ⟹ y ⋅ x⇧⋆ ≤ y"

class K2l_algebra = Kl_base +
assumes star_inductl_var: "z + x ⋅ y ≤ y ⟹ x⇧⋆ ⋅ z ≤ y"

class K2r_algebra = Kr_base +
assumes star_inductr_var: "z + y ⋅ x ≤ y ⟹ z ⋅ x⇧⋆ ≤ y"

class K1_algebra = K1l_algebra + K1r_algebra

class K2_algebra = K2l_algebra + K2r_algebra

```