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 = (xn+1)  x0⇙⇗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  xi x0⇙⇗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: "x0⇙⇗Suc n x0⇙⇗Suc n Suc n  i"
      using aa1 by fastforce
    have ff2: "x1. x0⇙⇗n+ x1  x0⇙⇗Suc n Suc n  i"
      using ff1 powsum2 by auto
    have "xi x0⇙⇗Suc n⇖"
      by (metis Suc.hyps Suc.prems ff2 le_Suc_eq local.dual_order.trans local.join.le_supE)
  }
  thus "xi x0⇙⇗Suc n⇖"
    using local.less_eq_def local.powsum_split_var2 by blast
qed
qed

lemma C14_aux: "m  n   xm (xn) = (xn)  xm⇖"
proof -
  assume assm: "m  n"
  hence "xm  (xn) =  xm (xn-m xm)"
    by (metis (full_types) le_add_diff_inverse2 power_add)
  also have "... = (xn-m xm)   xm⇖"
    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 = xn⇖"
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 = xm⇙⇗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 = x0⇙⇗n (xn+1)"
proof -
  have "x =  (xn+1)  x0⇙⇗n⇖"
    by (rule C14)
  also have "... = (xn+1)  (i=0..n. x^i)"
    by (subst powsum_def, auto)
  also have "... = (i=0..n. (xn+1)  x^i)"
    by (metis le0 sum_interval_distl)
  also have "... = (i=0..n. x^i  (xn+1))"
    by (auto intro: sum_interval_cong simp only:C14_aux)
  also have "... = x0⇙⇗n (xn+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: "xn x" 
  by (induct n, simp_all add: star_ref prod_star_closure star_ext) 

lemma star_power_slide: 
  assumes "k  n" 
  shows "xk (xn) = (xn)  xk⇖"  
proof -
  from assms have "xk (xn) = (xk xn-k)  xk⇖"
    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: "xm⇙⇗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 "x0⇙⇗m (xn) = (xn)  x0⇙⇗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 "x0⇙⇗Suc m (xn) = (x0⇙⇗m+ xSuc m)  (xn)"
    by (simp add:powsum2)
  also have "... = x0⇙⇗m (xn) + xSuc m (xn)"
    by (metis distrib_right')
  also have "... = (xn)  x0⇙⇗m+ xSuc m (xn)"
    by (metis Suc.hyps Suc.prems Suc_leD)
  also have "... = (xn)  x0⇙⇗m+ (xn)  xSuc m⇖"
    by (metis Suc.prems star_power_slide) 
  also have "... = (xn)  (x0⇙⇗m+ xSuc 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: "(xn+1)  x0⇙⇗n (xn+1)  x0⇙⇗n= (xn+1)  x0⇙⇗n⇖"
proof (cases n)
  case 0 thus ?thesis
    by simp
next
  case (Suc m) thus ?thesis
  proof -
    assume assm: "n = Suc m"
    have "(xm+2)  x0⇙⇗m+1 (xm+2)  x0⇙⇗m+1= (xm+2)  (xm+2)  x0⇙⇗m+1 x0⇙⇗m+1⇖"
      by (subgoal_tac "m + 1  m + 2", metis mult.assoc star_sum_power_slide, simp)
    also have "...  = (xm+2)  x0⇙⇗m+1 x0⇙⇗m+1⇖"
      by (metis star_trans_eq)
    also have "...  =  (xm+2)  x0⇙⇗(Suc m)+(Suc m)⇖"
      by (simp add: mult.assoc powsum_prod)
    also have "... =  (xm+2)  (x0⇙⇗Suc m+ xm + 2⇙⇗m)"
      by (metis monoid_add_class.add.left_neutral powsum_split_var3 add_2_eq_Suc')
    also have "... =  (xm+2)  x0⇙⇗Suc m+ (xm+2)  x(m + 2)+ 0⇙⇗m⇖"
     by (simp add: local.distrib_left)
    also have "... =  (xm+2)  x0⇙⇗Suc m+ (xm+2)  xm+2 x0⇙⇗m⇖"
      by (subst powsum_shift[THEN sym], metis mult.assoc)
   also have "... =  (xm+2)  (x0⇙⇗m+  xm+1) + (xm+2)  xm+2 x0⇙⇗m⇖"
     by (simp add:powsum2)
   also have "... =  (xm+2)  x0⇙⇗m+ (xm+2)  xm+2 x0⇙⇗m+ (xm+2)  xm+1⇖"
     by (metis add.assoc add.commute add.left_commute distrib_left mult.assoc)
   also have "... =  (xm+2)  x0⇙⇗m+ (xm+2)  x0⇙⇗m+ (xm+2)  xm+1⇖"
     by (metis add_idem' distrib_right' star_subsum)
   also have "... =  (xm+2)  (x0⇙⇗m+ xm+1)"
     by (metis add_idem' distrib_left)
    also have "... = (xm+2)  x0⇙⇗m+1⇖"
      by (simp add:powsum2)
    finally  show ?thesis 
      by (simp add: assm)
  qed
qed

lemma conway_powerstar2: "1 + x  (xn+1)  x0⇙⇗n⇖"
proof (cases n)
  case 0 show ?thesis
    using "0" local.B21 by auto
next
  case (Suc m) show ?thesis
  proof -
    have one: "x  (xm+2)  x0⇙⇗m+1⇖"
      by (metis Suc_eq_plus1 powsum_ext  mult_isor mult_onel order_trans star_ref)
    have two: "1  (xm+2)  x0⇙⇗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 = (xn+1)  x0⇙⇗n⇖"
proof (rule order.antisym) 
  show "x  (xn+1)  x0⇙⇗n⇖"
    by (metis conway_powerstar1 conway_powerstar2 mult.assoc B23)
  have "(xn+1)  x0⇙⇗n (x)  x0⇙⇗n⇖"
    by (metis mult_isor power_le_star star_iso)
  also have "... = x  x0⇙⇗n⇖"
    by (metis star_invol)
  also have "...  x  x"
    by (simp add: local.prod_star_closure powsum_le_star)
  finally show "(xn+1)  x0⇙⇗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) "xx = 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   { xk| k. ik = j}"

notation
  boffa_pair ("__,_")

abbreviation conway_assms where
  "conway_assms x  ( i j. (xi xj xij)  (xi,i) = xi,i)"

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

definition conway_assm1 where "conway_assm1 x = ( i j. xi xj xij)" 
definition conway_assm2 where "conway_assm2 x = (i. xi,i = xi,i)"

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

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

lemma conway_monoid_split: 
  assumes "conway_assm2 x"
  shows " {xi| i . i  UNIV} = 1 +  {xi| i . i  UNIV}"
proof -
  have " {xi| i . i  UNIV} =  {xi| 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 "... = x1+  (Rep_boffa_mon x ` (UNIV - {1}))"
    by (subst sum_fun_insert, auto)
  also have "... = x1+  { xi| i. i(UNIV - {1})}"
    by (metis fset_to_im)
  also from assms have unfld:"... = 1 + x1+  { xi| 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: "{xij| i j. i  UNIV  j  UNIV} = {xi| 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; aA. bB. a  b   A  B"
  by (metis sum_intro)  

lemma boffa_aux2: 
  "conway_assm1 x 
  {xixj| i j. i  UNIV  j  UNIV}  {xij| 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 "( {xi| i. iUNIV}) + ( {xi xj| i j . iUNIV  jUNIV}) = ( {xi| i. iUNIV})"
proof -
  from assms 
  have "( {xi| i. iUNIV}) + ( {xi xj| i j . iUNIV  jUNIV})  ( {xi| i. iUNIV})+( {xij| i j . iUNIV  jUNIV})"
    apply (subst add_iso_r)
    apply (subst boffa_aux2)
    by simp_all
  also have "... = ( {xi| i. iUNIV})"
    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 "( {xi|i. iUNIV}) = ( {xi| i. iUNIV})"
proof -
  have one:"( {xi|i. iUNIV})  ( {xi|i. iUNIV}) = (1 + ( {xi|i. iUNIV}))  (1 + ( {xi|i. iUNIV}))"
    by (metis (mono_tags) assms(2) conway_monoid_split)
  also have "... = 1 + ( {xi|i. iUNIV}) + (( {xi|i. iUNIV})  ( {xi|i. iUNIV}))"
    by (metis (lifting, no_types) calculation less_eq_def mult_isol mult_isol_equiv_subdistl mult_oner)
  also have "... = 1 + ( {xi|i. iUNIV}) + ( {xi xj| i j. iUNIV  jUNIV})"
    by (simp only: dioid_sum_prod finite_UNIV)
  finally have " {xi|i. i  UNIV}   {xi|i. i  UNIV} =  {xi|i. i  UNIV}"
    apply (simp only:)
proof -
  assume a1: "{xi|i. i  UNIV}  {xi|i. i  UNIV} = 1 + {xi|i. i  UNIV} + {xi xj|i j. i  UNIV  j  UNIV}"
  hence "{xR|R. R  UNIV}  {xR|R. R  UNIV} = {xR|R. R  UNIV}"
    using assms(1) assms(2) boffa_aux3 conway_monoid_split by fastforce
  thus "1 + {xi|i. i  UNIV} + {xi xj|i j. i  UNIV  j  UNIV} = {xi|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"
    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"
    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"
    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 = 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"
    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  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 = xy x = xy"
  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"
      by (simp add: r1)
    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