# HG changeset patch # User haftmann # Date 1174077135 -3600 # Node ID 8469640e1489af070f0f4e95a81cc16e17a48f99 # Parent bd4379c9b4d0e6d80e7b80ef00c9002f8f2fcd94 added "class"es diff -r bd4379c9b4d0 -r 8469640e1489 src/HOL/Library/Kleene_Algebras.thy --- a/src/HOL/Library/Kleene_Algebras.thy Fri Mar 16 21:32:14 2007 +0100 +++ b/src/HOL/Library/Kleene_Algebras.thy Fri Mar 16 21:32:15 2007 +0100 @@ -12,16 +12,16 @@ class star = fixes star :: "'a \ 'a" -axclass idem_add \ ab_semigroup_add - add_idem[simp]: "x + x = x" +class idem_add = ab_semigroup_add + + assumes add_idem [simp]: "x \<^loc>+ x = x" lemma add_idem2[simp]: "(x::'a::idem_add) + (x + y) = x + y" unfolding add_assoc[symmetric] by simp -axclass order_by_add \ idem_add, ord - order_def: "a \ b \ a + b = b" - strict_order_def: "a < b \ a \ b \ a \ b" +class order_by_add = idem_add + ord + + assumes order_def: "a \ b \ a \<^loc>+ b = b" + assumes strict_order_def: "a \ b \ a \ b \ a \ b" lemma ord_simp1[simp]: "(x::'a::order_by_add) \ y \ x + y = y" unfolding order_def . @@ -51,7 +51,7 @@ qed -axclass pre_kleene \ semiring_1, order_by_add +class pre_kleene = semiring_1 + order_by_add instance pre_kleene \ pordered_semiring proof @@ -79,38 +79,32 @@ qed qed -axclass kleene \ pre_kleene, star - star1: "1 + a * star a \ star a" - star2: "1 + star a * a \ star a" - star3: "a * x \ x \ star a * x \ x" - star4: "x * a \ x \ x * star a \ x" +class kleene = pre_kleene + star + + assumes star1: "\<^loc>1 \<^loc>+ a \<^loc>* star a \ star a" + and star2: "\<^loc>1 \<^loc>+ star a \<^loc>* a \ star a" + and star3: "a \<^loc>* x \ x \ star a \<^loc>* x \ x" + and star4: "x \<^loc>* a \ x \ x \<^loc>* star a \ x" -axclass kleene_by_comp_lat \ - pre_kleene, comp_lat, recpower, star - - star_cont: "a * star b * c = (SUP n. a * b ^ n * c)" - +class kleene_by_complete_lattice = + pre_kleene + complete_lattice + recpower + star + + assumes star_cont: "a \<^loc>* star b \<^loc>* c = (SUP n. a \<^loc>* b ^ n \<^loc>* c)" lemma plus_leI: fixes x :: "'a :: order_by_add" shows "x \ z \ y \ z \ x + y \ z" unfolding order_def by (simp add:add_assoc) - - - lemma le_SUPI': - fixes l :: "'a :: comp_lat" + fixes l :: "'a :: complete_lattice" assumes "l \ M i" shows "l \ (SUP i. M i)" using prems by (rule order_trans) (rule le_SUPI [OF UNIV_I]) - lemma zero_minimum[simp]: "(0::'a::pre_kleene) \ x" unfolding order_def by simp -instance kleene_by_comp_lat \ kleene +instance kleene_by_complete_lattice \ kleene proof fix a x :: 'a @@ -454,22 +448,4 @@ unfolding tcl_def by (auto simp:star_commute) - - - - end - - - - - - - - - - - - - -