src/HOL/Library/RBT_Impl.thy
changeset 55414 eab03e9cee8a
parent 55412 eb2caacf3ba4
child 55417 01fbfb60c33e
     1.1 --- a/src/HOL/Library/RBT_Impl.thy	Wed Feb 12 08:35:56 2014 +0100
     1.2 +++ b/src/HOL/Library/RBT_Impl.thy	Wed Feb 12 08:35:57 2014 +0100
     1.3 @@ -1067,7 +1067,7 @@
     1.4  subsection {* Folding over entries *}
     1.5  
     1.6  definition fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a, 'b) rbt \<Rightarrow> 'c \<Rightarrow> 'c" where
     1.7 -  "fold f t = List.fold (prod_case f) (entries t)"
     1.8 +  "fold f t = List.fold (case_prod f) (entries t)"
     1.9  
    1.10  lemma fold_simps [simp]:
    1.11    "fold f Empty = id"
    1.12 @@ -1110,10 +1110,10 @@
    1.13  proof -
    1.14    obtain ys where "ys = rev xs" by simp
    1.15    have "\<And>t. is_rbt t \<Longrightarrow>
    1.16 -    rbt_lookup (List.fold (prod_case rbt_insert) ys t) = rbt_lookup t ++ map_of (rev ys)"
    1.17 -      by (induct ys) (simp_all add: rbt_bulkload_def rbt_lookup_rbt_insert prod_case_beta)
    1.18 +    rbt_lookup (List.fold (case_prod rbt_insert) ys t) = rbt_lookup t ++ map_of (rev ys)"
    1.19 +      by (induct ys) (simp_all add: rbt_bulkload_def rbt_lookup_rbt_insert case_prod_beta)
    1.20    from this Empty_is_rbt have
    1.21 -    "rbt_lookup (List.fold (prod_case rbt_insert) (rev xs) Empty) = rbt_lookup Empty ++ map_of xs"
    1.22 +    "rbt_lookup (List.fold (case_prod rbt_insert) (rev xs) Empty) = rbt_lookup Empty ++ map_of xs"
    1.23       by (simp add: `ys = rev xs`)
    1.24    then show ?thesis by (simp add: rbt_bulkload_def rbt_lookup_Empty foldr_conv_fold)
    1.25  qed