author krauss Mon, 16 Jul 2007 21:26:35 +0200 changeset 23820 8290cd33c4d5 parent 23819 2040846d1bbe child 23821 2acd9d79d855
more proofs
```--- 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 @@
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)"
+  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 *)
```