(* 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)