merged

--- a/src/HOL/Library/RBT_Impl.thy	Wed Oct 10 16:19:52 2012 +0200
+++ b/src/HOL/Library/RBT_Impl.thy	Wed Oct 10 16:41:19 2012 +0200
@@ -1076,8 +1076,8 @@
   by (simp_all add: fold_def fun_eq_iff)
 
 lemma fold_code [code]:
-  "fold f Empty c = c"
-  "fold f (Branch c lt k v rt) c = fold f rt (f k v (fold f lt c))"
+  "fold f Empty x = x"
+  "fold f (Branch c lt k v rt) x = fold f rt (f k v (fold f lt x))"
 by(simp_all)
 
 (* fold with continuation predicate *)
@@ -1725,10 +1725,9 @@
   "skip_red (Branch color.R l k v r) = l"
 | "skip_red t = t"
 
-fun skip_black :: "('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt"
+definition skip_black :: "('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt"
 where
-  "skip_black (Branch color.B l k v r) = l"
-| "skip_black t = t"
+  "skip_black t = (let t' = skip_red t in case t' of Branch color.B l k v r \<Rightarrow> l | _ \<Rightarrow> t')"
 
 datatype compare = LT | GT | EQ
 
@@ -1761,9 +1760,9 @@
   compare.eq.refl compare.eq.simps
   compare.EQ_def compare.GT_def compare.LT_def
   equal_compare_def
-  skip_red_def skip_red.simps skip_red.induct 
-  skip_black_def skip_black.simps skip_black.induct
-  compare_height.simps
+  skip_red_def skip_red.simps skip_red.cases skip_red.induct 
+  skip_black_def
+  compare_height_def compare_height.simps
 
 subsection {* union and intersection of sorted associative lists *}
 

--- a/src/HOL/List.thy	Wed Oct 10 16:19:52 2012 +0200
+++ b/src/HOL/List.thy	Wed Oct 10 16:41:19 2012 +0200
@@ -5514,8 +5514,22 @@
   "list_ex P [i..j] \<longleftrightarrow> \<not> (all_interval_int (Not \<circ> P) i j)"
   by (simp add: list_ex_iff all_interval_int_def)
 
-hide_const (open) member null maps map_filter all_interval_nat all_interval_int
-
+text {* optimized code (tail-recursive) for @{term length} *}
+
+definition gen_length :: "nat \<Rightarrow> 'a list \<Rightarrow> nat"
+where "gen_length n xs = n + length xs"
+
+lemma gen_length_code [code]:
+  "gen_length n [] = n"
+  "gen_length n (x # xs) = gen_length (Suc n) xs"
+by(simp_all add: gen_length_def)
+
+declare list.size(3-4)[code del]
+
+lemma length_code [code]: "length = gen_length 0"
+by(simp add: gen_length_def fun_eq_iff)
+
+hide_const (open) member null maps map_filter all_interval_nat all_interval_int gen_length
 
 subsubsection {* Pretty lists *}