--- a/src/HOL/Library/Kleene_Algebras.thy Mon Jul 16 21:22:43 2007 +0200
+++ b/src/HOL/Library/Kleene_Algebras.thy Mon Jul 16 21:26:35 2007 +0200
@@ -248,22 +248,11 @@
qed
-lemma star_mono:
- fixes x y :: "'a :: kleene"
- assumes "x \<le> y"
- shows "star x \<le> star y"
- oops
-
lemma star_idemp:
fixes x :: "'a :: kleene"
shows "star (star x) = star x"
oops
-lemma zero_star[simp]:
- shows "star (0::'a::kleene) = 1"
- oops
-
-
lemma star_unfold_left:
fixes a :: "'a :: kleene"
shows "1 + a * star a = star a"
@@ -295,7 +284,9 @@
thus "star a \<le> 1 + star a * a" by simp
qed
-
+lemma star_zero[simp]:
+ shows "star (0::'a::kleene) = 1"
+ by (rule star_unfold_left[of 0, simplified])
lemma star_commute:
fixes a b x :: "'a :: kleene"
@@ -339,14 +330,12 @@
by (simp add:left_distrib mult_assoc)
qed
qed
-qed
-
-
+qed
lemma star_assoc:
fixes c d :: "'a :: kleene"
shows "star (c * d) * c = c * star (d * c)"
- oops
+ by (auto simp:mult_assoc star_commute)
lemma star_dist:
fixes a b :: "'a :: kleene"
@@ -357,13 +346,24 @@
fixes a p p' :: "'a :: kleene"
assumes "p * p' = 1" and "p' * p = 1"
shows "p' * star a * p = star (p' * a * p)"
+proof -
+ from assms
+ have "p' * star a * p = p' * star (p * p' * a) * p"
+ by simp
+ also have "\<dots> = p' * p * star (p' * a * p)"
+ by (simp add: mult_assoc star_assoc)
+ also have "\<dots> = star (p' * a * p)"
+ by (simp add: assms)
+ finally show ?thesis .
+qed
+
+lemma star_mono:
+ fixes x y :: "'a :: kleene"
+ assumes "x \<le> y"
+ shows "star x \<le> star y"
oops
-lemma star_zero:
- "star (0::'a::kleene) = 1"
- by (rule star_unfold_left[of 0, simplified])
-
(* Own lemmas *)