# HG changeset patch
# User krauss
# Date 1248728019 -7200
# Node ID 74ae5e9f312cd227f6aceddb836ad1b0c13bb688
# Parent  cdc76a42fed4e57091e753a4f237c815d5c3213c
added proof of Kleene_Algebra.star_decomp

diff -r cdc76a42fed4 -r 74ae5e9f312c src/HOL/Library/Kleene_Algebra.thy
--- a/src/HOL/Library/Kleene_Algebra.thy	Mon Jul 27 22:50:04 2009 +0200
+++ b/src/HOL/Library/Kleene_Algebra.thy	Mon Jul 27 22:53:39 2009 +0200
@@ -274,7 +274,19 @@
 oops
 
 lemma star_decomp: "star (a + b) = star a * star (b * star a)"
-oops
+proof (rule antisym)
+  have "1 + (a + b) * star a * star (b * star a) \<le>
+    1 + a * star a * star (b * star a) + b * star a * star (b * star a)"
+    by (metis add_commute add_left_commute eq_iff left_distrib mult_assoc)
+  also have "\<dots> \<le> star a * star (b * star a)"
+    by (metis add_commute add_est1 add_left_commute ka18 plus_leI star_unfold_left x_less_star)
+  finally show "star (a + b) \<le> star a * star (b * star a)"
+    by (metis mult_1_right mult_assoc star3')
+next
+  show "star a * star (b * star a) \<le> star (a + b)"
+    by (metis add_assoc add_est1 add_est2 add_left_commute less_star mult_mono'
+      star_absorb_one star_absorb_one' star_idemp star_mono star_mult_idem zero_minimum)
+qed
 
 lemma ka22: "y * star x \<le> star x * star y \<Longrightarrow>  star y * star x \<le> star x * star y"
 by (metis mult_assoc mult_right_mono plus_leI star3' star_mult_idem x_less_star zero_minimum)