# Theory Regular_Algebra_Variants

```(* 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 ‹Variants of Regular Algebra›

theory Regular_Algebra_Variants
imports Regular_Algebras Pratts_Counterexamples
begin

text ‹Replacing Kozen's induction axioms by Boffa's leads to incompleteness.›

lemma (in star_dioid)
assumes "⋀x. 1 + x ⋅ x⇧⋆ =  x⇧⋆"
and "⋀x. 1 + x⇧⋆ ⋅ x =  x⇧⋆"
and "⋀x. x ⋅ x = x ⟹ x⇧⋆ = 1 + x"
shows "⋀x y. (x + y)⇧⋆ = x⇧⋆ ⋅ (y ⋅ x⇧⋆)⇧⋆"
(*  nitpick [expect=genuine] --"5-element counterexample"*)
oops

lemma (in star_dioid)
assumes "⋀x. 1 + x ⋅ x⇧⋆ =  x⇧⋆"
and "⋀x. 1 + x⇧⋆ ⋅ x =  x⇧⋆"
and "⋀x. x ⋅ x = x ⟹ x⇧⋆ = 1 + x"
shows "⋀x y. x ≤ y ⟶ x⇧⋆ ≤ y⇧⋆"
(*  nitpick [expect=genuine] --"5-element counterexample"*)
oops

lemma (in star_dioid)
assumes "⋀x. 1 + x ⋅ x⇧⋆ =  x⇧⋆"
and "⋀x. 1 + x⇧⋆ ⋅ x =  x⇧⋆"
and "⋀x y. 1 + x ≤ y ∧ y ⋅ y ≤ y ⟶ x⇧⋆ ≤ y"
shows "⋀x. 1 + x ≤ x⇧⋆"
by (metis add_iso_r assms(1) mult_oner subdistl)

lemma (in star_dioid)
assumes "⋀x. 1 + x ⋅ x⇧⋆ =  x⇧⋆"
and "⋀x. 1 + x⇧⋆ ⋅ x =  x⇧⋆"
and "⋀x y. 1 + x ≤ y ∧ y ⋅ y ≤ y ⟶ x⇧⋆ ≤ y"
shows "⋀x. x⇧⋆ = (1 + x)⇧⋆"
oops ― ‹need to reconsider this›

lemma (in star_dioid)
assumes "⋀x. 1 + x ⋅ x⇧⋆ =  x⇧⋆"
and "⋀x. 1 + x⇧⋆ ⋅ x =  x⇧⋆"
and "⋀x y. 1 + x + y ⋅ y ≤ y ⟹ x⇧⋆ ≤ y"
shows "⋀x. x⇧⋆ ⋅ x⇧⋆ ≤ x⇧⋆"
oops

lemma (in star_dioid)
assumes "⋀x. 1 + x ⋅ x⇧⋆ =  x⇧⋆"
and "⋀x. 1 + x⇧⋆ ⋅ x =  x⇧⋆"
and "⋀x y z. x ⋅ y = y ⋅ z ⟹ x⇧⋆ ⋅ y = y ⋅ z⇧⋆"
shows "1⇧⋆ = 1"
(*  nitpick -- "3-element counterexample"*)
oops

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

lemma (in star_dioid)
assumes "⋀x. 1 + x ⋅ x⇧⋆ =  x⇧⋆"
and "⋀x. 1 + x⇧⋆ ⋅ x =  x⇧⋆"
and "⋀x y. x = y ⋅ x ⟹ x = y⇧⋆ ⋅ x"
and "⋀x y. x = x ⋅ y ⟹ x = x ⋅ y⇧⋆"
shows "⋀x y. y ⋅ x ≤ y ⟹ y ⋅ x⇧⋆ ≤ y"
oops

class C3l_var = conway_dioid +
assumes C3l_var: "z + x ⋅ y ≤ y ⟹ x⇧⋆ ⋅ z ≤ y"

class C3r_var = conway_dioid +
assumes C3r_var: "z + y ⋅ x ≤ y ⟹ z ⋅ x⇧⋆ ≤ y"

class C3_var = C3l_var + C3r_var

sublocale C3l_var ⊆ C3l_algebra
apply unfold_locales
by (simp add: local.C3l_var)

sublocale C3l_algebra ⊆ C3l_var
by (unfold_locales, metis star_inductl_var)

sublocale C3_var ⊆ C3_algebra
apply unfold_locales
by (simp add: local.C3r_var)

sublocale C3_algebra ⊆ C3_var
by (unfold_locales, metis star_inductr_var)

class Brtc_algebra = star_dioid +
assumes rtc1: "1 + x⇧⋆ ⋅ x⇧⋆ + x ≤ x⇧⋆"
and rtc2: "1 + x + y ⋅ y ≤ y ⟹ x⇧⋆ ≤ y"

sublocale B2_algebra ⊆ Brtc_algebra
proof
fix x y
show "1 + x⇧⋆ ⋅ x⇧⋆ + x ≤ x⇧⋆"
by (simp add: local.star_ext)
show "1 + x + y ⋅ y ≤ y ⟹ x⇧⋆ ≤ y"
by (metis B23 local.join.le_sup_iff order.eq_iff mult_1_right subdistl)
qed

sublocale Brtc_algebra ⊆ B2_algebra
proof
fix x y
show "1 + x ≤ x⇧⋆"
by (metis rtc1 join.le_sup_iff)
show "x⇧⋆ ⋅ x⇧⋆ = x⇧⋆"
proof (rule order.antisym)
show "x⇧⋆ ⋅ x⇧⋆ ≤ x⇧⋆"
by (metis rtc1 join.le_sup_iff)
show "x⇧⋆ ≤ x⇧⋆ ⋅ x⇧⋆"
by (metis rtc1 add.commute join.le_sup_iff less_eq_def mult_isor mult_onel)
qed
show "⟦ 1 + x ≤ y; y ⋅ y = y ⟧ ⟹ x⇧⋆ ≤ y"
by (metis rtc2 eq_refl less_eq_def)
qed

class wB1_algebra = conway_dioid +
assumes wR: "x ⋅ x ≤ x ⟹ x⇧⋆ = 1 + x"

sublocale wB1_algebra ⊆ B1_algebra
by (unfold_locales, metis order_refl wR)

lemma (in B1_algebra) one_plus_star:  "x⇧⋆ = (1 + x)⇧⋆"
by (metis C11_var R add_idem' mult_onel mult_oner)

sublocale B1_algebra ⊆ wB1_algebra
proof unfold_locales
fix x :: 'a
assume "x ⋅ x ≤ x"
hence "x ⋅ (1 + x) = x"
by (simp add: local.distrib_left local.join.sup_absorb1)
hence "(1 + x) ⋅ (1 + x) = 1 + x"
using add.left_commute distrib_right' by simp
thus "x⇧⋆ = 1 + x"
by (metis R add_assoc' add_idem' one_plus_star)
qed

end
```