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