# HG changeset patch
# User wenzelm
# Date 1248728531 -7200
# Node ID 2a3ffaf00de4ba1789c9a9c9cecddbedc4631627
# Parent  74ae5e9f312cd227f6aceddb836ad1b0c13bb688# Parent  d2a99fdddd691306047f2c019c21e32d49035c02
merged

diff -r d2a99fdddd69 -r 2a3ffaf00de4 src/HOL/Library/Kleene_Algebra.thy
--- a/src/HOL/Library/Kleene_Algebra.thy	Mon Jul 27 22:25:29 2009 +0200
+++ b/src/HOL/Library/Kleene_Algebra.thy	Mon Jul 27 23:02:11 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)
diff -r d2a99fdddd69 -r 2a3ffaf00de4 src/HOL/Library/RBT.thy
--- a/src/HOL/Library/RBT.thy	Mon Jul 27 22:25:29 2009 +0200
+++ b/src/HOL/Library/RBT.thy	Mon Jul 27 23:02:11 2009 +0200
@@ -916,9 +916,72 @@
   "alist_of Empty = []"
 | "alist_of (Tr _ l k v r) = alist_of l @ (k,v) # alist_of r"
 
+lemma map_of_alist_of_aux: "st (Tr c t1 k v t2) \<Longrightarrow> RBT.map_of (Tr c t1 k v t2) = RBT.map_of t2 ++ [k\<mapsto>v] ++ RBT.map_of t1"
+proof (rule ext)
+  fix x
+  assume ST: "st (Tr c t1 k v t2)"
+  let ?thesis = "RBT.map_of (Tr c t1 k v t2) x = (RBT.map_of t2 ++ [k \<mapsto> v] ++ RBT.map_of t1) x"
+
+  have DOM_T1: "!!k'. k'\<in>dom (RBT.map_of t1) \<Longrightarrow> k>k'"
+  proof -
+    fix k'
+    from ST have "t1 |\<guillemotleft> k" by simp
+    with tlt_prop have "\<forall>k'\<in>keys t1. k>k'" by auto
+    moreover assume "k'\<in>dom (RBT.map_of t1)"
+    ultimately show "k>k'" using RBT.mapof_keys ST by auto
+  qed
+
+  have DOM_T2: "!!k'. k'\<in>dom (RBT.map_of t2) \<Longrightarrow> k<k'"
+  proof -
+    fix k'
+    from ST have "k \<guillemotleft>| t2" by simp
+    with tgt_prop have "\<forall>k'\<in>keys t2. k<k'" by auto
+    moreover assume "k'\<in>dom (RBT.map_of t2)"
+    ultimately show "k<k'" using RBT.mapof_keys ST by auto
+  qed
+
+  {
+    assume C: "x<k"
+    hence "RBT.map_of (Tr c t1 k v t2) x = RBT.map_of t1 x" by simp
+    moreover from C have "x\<notin>dom [k\<mapsto>v]" by simp
+    moreover have "x\<notin>dom (RBT.map_of t2)" proof
+      assume "x\<in>dom (RBT.map_of t2)"
+      with DOM_T2 have "k<x" by blast
+      with C show False by simp
+    qed
+    ultimately have ?thesis by (simp add: map_add_upd_left map_add_dom_app_simps)
+  } moreover {
+    assume [simp]: "x=k"
+    hence "RBT.map_of (Tr c t1 k v t2) x = [k \<mapsto> v] x" by simp
+    moreover have "x\<notin>dom (RBT.map_of t1)" proof
+      assume "x\<in>dom (RBT.map_of t1)"
+      with DOM_T1 have "k>x" by blast
+      thus False by simp
+    qed
+    ultimately have ?thesis by (simp add: map_add_upd_left map_add_dom_app_simps)
+  } moreover {
+    assume C: "x>k"
+    hence "RBT.map_of (Tr c t1 k v t2) x = RBT.map_of t2 x" by (simp add: less_not_sym[of k x])
+    moreover from C have "x\<notin>dom [k\<mapsto>v]" by simp
+    moreover have "x\<notin>dom (RBT.map_of t1)" proof
+      assume "x\<in>dom (RBT.map_of t1)"
+      with DOM_T1 have "k>x" by simp
+      with C show False by simp
+    qed
+    ultimately have ?thesis by (simp add: map_add_upd_left map_add_dom_app_simps)
+  } ultimately show ?thesis using less_linear by blast
+qed
+
 lemma map_of_alist_of:
   shows "st t \<Longrightarrow> Map.map_of (alist_of t) = map_of t"
-  oops
+proof (induct t)
+  case Empty thus ?case by (simp add: RBT.map_of_Empty)
+next
+  case (Tr c t1 k v t2)
+  hence "Map.map_of (alist_of (Tr c t1 k v t2)) = RBT.map_of t2 ++ [k \<mapsto> v] ++ RBT.map_of t1" by simp
+  also note map_of_alist_of_aux[OF Tr.prems,symmetric]
+  finally show ?case .
+qed
 
 lemma fold_alist_fold:
   "foldwithkey f t x = foldl (\<lambda>x (k,v). f k v x) x (alist_of t)"
diff -r d2a99fdddd69 -r 2a3ffaf00de4 src/HOL/Map.thy
--- a/src/HOL/Map.thy	Mon Jul 27 22:25:29 2009 +0200
+++ b/src/HOL/Map.thy	Mon Jul 27 23:02:11 2009 +0200
@@ -307,6 +307,9 @@
 lemma map_add_upds[simp]: "m1 ++ (m2(xs[\<mapsto>]ys)) = (m1++m2)(xs[\<mapsto>]ys)"
 by (simp add: map_upds_def)
 
+lemma map_add_upd_left: "m\<notin>dom e2 \<Longrightarrow> e1(m \<mapsto> u1) ++ e2 = (e1 ++ e2)(m \<mapsto> u1)"
+by (rule ext) (auto simp: map_add_def dom_def split: option.split)
+
 lemma map_of_append[simp]: "map_of (xs @ ys) = map_of ys ++ map_of xs"
 unfolding map_add_def
 apply (induct xs)
@@ -508,6 +511,12 @@
 lemma map_add_comm: "dom m1 \<inter> dom m2 = {} \<Longrightarrow> m1++m2 = m2++m1"
 by (rule ext) (force simp: map_add_def dom_def split: option.split)
 
+lemma map_add_dom_app_simps:
+  "\<lbrakk> m\<in>dom l2 \<rbrakk> \<Longrightarrow> (l1++l2) m = l2 m"
+  "\<lbrakk> m\<notin>dom l1 \<rbrakk> \<Longrightarrow> (l1++l2) m = l2 m"
+  "\<lbrakk> m\<notin>dom l2 \<rbrakk> \<Longrightarrow> (l1++l2) m = l1 m"
+by (auto simp add: map_add_def split: option.split_asm)
+
 lemma dom_const [simp]:
   "dom (\<lambda>x. Some y) = UNIV"
   by auto