# HG changeset patch
# User krauss
# Date 1184613995 -7200
# Node ID 8290cd33c4d5ee8708931535ff46e1a62c20a27d
# Parent  2040846d1bbef34c6cb7b197a6a005c6407ae872
more proofs

diff -r 2040846d1bbe -r 8290cd33c4d5 src/HOL/Library/Kleene_Algebras.thy
--- 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 *)