Theory Regular_Algebras
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"
by (metis add_idem)
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"
by (metis add_zerol)
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"
by (metis add_idem)
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"
by (metis add_zerol)
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]
oops
lemma (in conway_dioid) "(x⇧⋆)⇧⋆ = x⇧⋆"
nitpick [expect=genuine]
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⇖)⇧⋆"
by (metis (full_types) le_add_diff_inverse2 power_add)
also have "... = (x⇗n-m⇖ ⋅ x⇗m⇖)⇧⋆ ⋅ x⇗m⇖"
by (metis (opaque_lifting, mono_tags) C_slide ab_semigroup_add_class.add.commute power_add)
finally show ?thesis
by (metis (full_types) assm le_add_diff_inverse ab_semigroup_add_class.add.commute power_add)
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}"
by (induction n, simp_all add:opp_power_def)
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"
by (metis add_idem)
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"
by (metis add_zerol)
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"
by (metis add_idem)
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"
by (metis add_zerol)
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⇧⋆)"
by (metis add_assoc' add_idem' distrib_left mult.assoc mult_onel mult_oner)
also have "... = 1 + x ⋅ x⇧⋆"
by (metis add.assoc add.commute distrib_left less_eq_def mult.assoc star_1l star_trans_eq)
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)"
by (metis add.assoc add_idem' distrib_left mult_1_left mult_1_right mult.assoc)
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
by (simp add: local.B23)
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"
by (metis add.commute add_idem' add.left_commute assms distrib_left mult_onel mult_oner distrib_right')
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⇧⋆"
by (metis B23 add_assoc' mult.assoc)
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⇧⋆)⇧⋆"
by (metis add_comm star_denest)
lemma star_denest_var_5: "x⇧⋆ ⋅ (y ⋅ x⇧⋆)⇧⋆ = y⇧⋆ ⋅ (x ⋅ y⇧⋆)⇧⋆"
by (metis add.commute star_denest_var)
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)⇧⋆"
by (metis add.assoc add_idem' mult.assoc star_slide star_trans_eq)
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)⇧⋆"
by (metis add_comm add_idem' add.left_commute star_unfoldl_eq)
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"
by (metis add_zeror star2 star_one)
lemma star_subsum [simp]: "x⇧⋆ + x⇧⋆ ⋅ x = x⇧⋆"
by (metis add.assoc add_idem star_slide_var star_unfoldl_eq)
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⇖"
by (metis (full_types) le_add_diff_inverse2 power_add star_slide)
with assms show ?thesis
by (metis (full_types) le_add_diff_inverse2 ab_semigroup_add_class.add.commute power_add)
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⇖)⇧⋆"
by (simp add:powsum2)
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
by (simp add:powsum2)
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⇧⋆"
by (metis (mono_tags) One_nat_def add.commute add_iso mult_1_right power_one_right star_plus_one subdistl)
thus ?case
by (metis assms order_trans)
next
case (Suc n)
have "y ⋅ x + z ≤ (y ⋅ x⇗(Suc n) ⇖+ z ⋅ x⇧⋆) ⋅ x + z"
by (metis Suc add_iso mult_isor)
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)⇖"
by (simp add: mult.assoc powsum_prod)
also have "... = (x⇗m+2⇖)⇧⋆ ⋅ (x⇘0⇙⇗Suc m ⇖+ x⇘m + 2⇙⇗m⇖)"
by (metis monoid_add_class.add.left_neutral powsum_split_var3 add_2_eq_Suc')
also have "... = (x⇗m+2⇖)⇧⋆ ⋅ x⇘0⇙⇗Suc m ⇖+ (x⇗m+2⇖)⇧⋆ ⋅ x⇘(m + 2)+ 0⇙⇗m⇖"
by (simp add: local.distrib_left)
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⇖"
by (simp add:powsum2)
also have "... = (x⇗m+2⇖)⇧⋆ ⋅ x⇘0⇙⇗m ⇖+ (x⇗m+2⇖)⇧⋆ ⋅ x⇗m+2 ⇖⋅ x⇘0⇙⇗m ⇖+ (x⇗m+2⇖)⇧⋆ ⋅ x⇗m+1⇖"
by (metis add.assoc add.commute add.left_commute distrib_left mult.assoc)
also have "... = (x⇗m+2⇖)⇧⋆ ⋅ x⇘0⇙⇗m ⇖+ (x⇗m+2⇖)⇧⋆ ⋅ x⇘0⇙⇗m ⇖+ (x⇗m+2⇖)⇧⋆ ⋅ x⇗m+1⇖"
by (metis add_idem' distrib_right' star_subsum)
also have "... = (x⇗m+2⇖)⇧⋆ ⋅ (x⇘0⇙⇗m ⇖+ x⇗m+1⇖)"
by (metis add_idem' distrib_left)
also have "... = (x⇗m+2⇖)⇧⋆ ⋅ x⇘0⇙⇗m+1⇖"
by (simp add:powsum2)
finally show ?thesis
by (simp add: assm)
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⇧⋆"
by (simp add: local.prod_star_closure powsum_le_star)
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
using [[simproc add: finite_Collect]]
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 add_iso_r)
apply (subst boffa_aux2)
by simp_all
also have "... = (∑ {x⇘i⇙ | i. i∈UNIV})"
by (metis (mono_tags) add_idem boffa_mon_aux1)
ultimately show ?thesis
by (simp add: dual_order.antisym)
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"