src/HOL/Library/RBT_Impl.thy
changeset 37458 4a76497f2eaa
parent 36176 3fe7e97ccca8
child 37591 d3daea901123
     1.1 --- a/src/HOL/Library/RBT_Impl.thy	Fri Jun 18 09:21:41 2010 +0200
     1.2 +++ b/src/HOL/Library/RBT_Impl.thy	Fri Jun 18 15:03:20 2010 +0200
     1.3 @@ -6,7 +6,7 @@
     1.4  header {* Implementation of Red-Black Trees *}
     1.5  
     1.6  theory RBT_Impl
     1.7 -imports Main
     1.8 +imports Main More_List
     1.9  begin
    1.10  
    1.11  text {*
    1.12 @@ -1049,7 +1049,7 @@
    1.13  subsection {* Folding over entries *}
    1.14  
    1.15  definition fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a, 'b) rbt \<Rightarrow> 'c \<Rightarrow> 'c" where
    1.16 -  "fold f t s = foldl (\<lambda>s (k, v). f k v s) s (entries t)"
    1.17 +  "fold f t = More_List.fold (prod_case f) (entries t)"
    1.18  
    1.19  lemma fold_simps [simp, code]:
    1.20    "fold f Empty = id"
    1.21 @@ -1071,12 +1071,12 @@
    1.22  proof -
    1.23    obtain ys where "ys = rev xs" by simp
    1.24    have "\<And>t. is_rbt t \<Longrightarrow>
    1.25 -    lookup (foldl (\<lambda>t (k, v). insert k v t) t ys) = lookup t ++ map_of (rev ys)"
    1.26 -      by (induct ys) (simp_all add: bulkload_def split_def lookup_insert)
    1.27 +    lookup (More_List.fold (prod_case insert) ys t) = lookup t ++ map_of (rev ys)"
    1.28 +      by (induct ys) (simp_all add: bulkload_def lookup_insert prod_case_beta)
    1.29    from this Empty_is_rbt have
    1.30 -    "lookup (foldl (\<lambda>t (k, v). insert k v t) Empty (rev xs)) = lookup Empty ++ map_of xs"
    1.31 +    "lookup (More_List.fold (prod_case insert) (rev xs) Empty) = lookup Empty ++ map_of xs"
    1.32       by (simp add: `ys = rev xs`)
    1.33 -  then show ?thesis by (simp add: bulkload_def foldl_foldr lookup_Empty split_def)
    1.34 +  then show ?thesis by (simp add: bulkload_def lookup_Empty foldr_fold_rev prod_case_split)
    1.35  qed
    1.36  
    1.37  hide_const (open) Empty insert delete entries keys bulkload lookup map_entry map fold union sorted