(* 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" 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] ― ‹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⇖)⇧^{⋆}" 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"