src/HOL/Library/RBT_Impl.thy
changeset 55466 786edc984c98
parent 55417 01fbfb60c33e
child 55642 63beb38e9258
     1.1 --- a/src/HOL/Library/RBT_Impl.thy	Fri Feb 14 07:53:45 2014 +0100
     1.2 +++ b/src/HOL/Library/RBT_Impl.thy	Fri Feb 14 07:53:46 2014 +0100
     1.3 @@ -1025,7 +1025,7 @@
     1.4  end
     1.5  
     1.6  theorem (in linorder) rbt_lookup_rbt_map_entry:
     1.7 -  "rbt_lookup (rbt_map_entry k f t) = (rbt_lookup t)(k := Option.map f (rbt_lookup t k))"
     1.8 +  "rbt_lookup (rbt_map_entry k f t) = (rbt_lookup t)(k := map_option f (rbt_lookup t k))"
     1.9    by (induct t) (auto split: option.splits simp add: fun_eq_iff)
    1.10  
    1.11  subsection {* Mapping all entries *}
    1.12 @@ -1053,7 +1053,7 @@
    1.13  
    1.14  end
    1.15  
    1.16 -theorem (in linorder) rbt_lookup_map: "rbt_lookup (map f t) x = Option.map (f x) (rbt_lookup t x)"
    1.17 +theorem (in linorder) rbt_lookup_map: "rbt_lookup (map f t) x = map_option (f x) (rbt_lookup t x)"
    1.18    apply(induct t)
    1.19    apply auto
    1.20    apply(subgoal_tac "x = a")
    1.21 @@ -1855,9 +1855,9 @@
    1.22  lemma map_of_sinter_with:
    1.23    "\<lbrakk> sorted (map fst xs); sorted (map fst ys) \<rbrakk>
    1.24    \<Longrightarrow> map_of (sinter_with f xs ys) k = 
    1.25 -  (case map_of xs k of None \<Rightarrow> None | Some v \<Rightarrow> Option.map (f k v) (map_of ys k))"
    1.26 +  (case map_of xs k of None \<Rightarrow> None | Some v \<Rightarrow> map_option (f k v) (map_of ys k))"
    1.27  apply(induct f xs ys rule: sinter_with.induct)
    1.28 -apply(auto simp add: sorted_Cons Option.map_def split: option.splits dest: map_of_SomeD bspec)
    1.29 +apply(auto simp add: sorted_Cons map_option_case split: option.splits dest: map_of_SomeD bspec)
    1.30  done
    1.31  
    1.32  end
    1.33 @@ -1866,11 +1866,11 @@
    1.34  by(induct xs)(auto 4 3 simp add: map_add_def intro!: ext split: option.split intro: rev_image_eqI)
    1.35  
    1.36  lemma map_map_filter: 
    1.37 -  "map f (List.map_filter g xs) = List.map_filter (Option.map f \<circ> g) xs"
    1.38 +  "map f (List.map_filter g xs) = List.map_filter (map_option f \<circ> g) xs"
    1.39  by(auto simp add: List.map_filter_def)
    1.40  
    1.41 -lemma map_filter_option_map_const: 
    1.42 -  "List.map_filter (\<lambda>x. Option.map (\<lambda>y. f x) (g (f x))) xs = filter (\<lambda>x. g x \<noteq> None) (map f xs)"
    1.43 +lemma map_filter_map_option_const: 
    1.44 +  "List.map_filter (\<lambda>x. map_option (\<lambda>y. f x) (g (f x))) xs = filter (\<lambda>x. g x \<noteq> None) (map f xs)"
    1.45  by(auto simp add: map_filter_def filter_map o_def)
    1.46  
    1.47  lemma set_map_filter: "set (List.map_filter P xs) = the ` (P ` set xs - {None})"
    1.48 @@ -1897,8 +1897,8 @@
    1.49    "rbt_inter_with_key f t1 t2 =
    1.50    (case RBT_Impl.compare_height t1 t1 t2 t2 
    1.51     of compare.EQ \<Rightarrow> rbtreeify (sinter_with f (entries t1) (entries t2))
    1.52 -    | compare.LT \<Rightarrow> rbtreeify (List.map_filter (\<lambda>(k, v). Option.map (\<lambda>w. (k, f k v w)) (rbt_lookup t2 k)) (entries t1))
    1.53 -    | compare.GT \<Rightarrow> rbtreeify (List.map_filter (\<lambda>(k, v). Option.map (\<lambda>w. (k, f k w v)) (rbt_lookup t1 k)) (entries t2)))"
    1.54 +    | compare.LT \<Rightarrow> rbtreeify (List.map_filter (\<lambda>(k, v). map_option (\<lambda>w. (k, f k v w)) (rbt_lookup t2 k)) (entries t1))
    1.55 +    | compare.GT \<Rightarrow> rbtreeify (List.map_filter (\<lambda>(k, v). map_option (\<lambda>w. (k, f k w v)) (rbt_lookup t1 k)) (entries t2)))"
    1.56  
    1.57  definition rbt_inter_with where
    1.58    "rbt_inter_with f = rbt_inter_with_key (\<lambda>_. f)"
    1.59 @@ -1971,7 +1971,7 @@
    1.60  
    1.61  lemma rbt_interwk_is_rbt [simp]:
    1.62    "\<lbrakk> rbt_sorted t1; rbt_sorted t2 \<rbrakk> \<Longrightarrow> is_rbt (rbt_inter_with_key f t1 t2)"
    1.63 -by(auto simp add: rbt_inter_with_key_def Let_def map_map_filter split_def o_def option_map_comp map_filter_option_map_const sorted_filter[where f=id, simplified] rbt_sorted_entries distinct_entries intro: is_rbt_rbtreeify split: compare.split)
    1.64 +by(auto simp add: rbt_inter_with_key_def Let_def map_map_filter split_def o_def option.map_comp map_filter_map_option_const sorted_filter[where f=id, simplified] rbt_sorted_entries distinct_entries intro: is_rbt_rbtreeify split: compare.split)
    1.65  
    1.66  lemma rbt_interw_is_rbt:
    1.67    "\<lbrakk> rbt_sorted t1; rbt_sorted t2 \<rbrakk> \<Longrightarrow> is_rbt (rbt_inter_with f t1 t2)"
    1.68 @@ -1987,7 +1987,7 @@
    1.69    (case rbt_lookup t1 k of None \<Rightarrow> None 
    1.70     | Some v \<Rightarrow> case rbt_lookup t2 k of None \<Rightarrow> None
    1.71                 | Some w \<Rightarrow> Some (f k v w))"
    1.72 -by(auto 4 3 simp add: rbt_inter_with_key_def Let_def map_of_entries[symmetric] rbt_lookup_rbtreeify map_map_filter split_def o_def option_map_comp map_filter_option_map_const sorted_filter[where f=id, simplified] rbt_sorted_entries distinct_entries map_of_sinter_with map_of_eq_None_iff set_map_filter split: option.split compare.split intro: rev_image_eqI dest: rbt_sorted_entries_right_unique)
    1.73 +by(auto 4 3 simp add: rbt_inter_with_key_def Let_def map_of_entries[symmetric] rbt_lookup_rbtreeify map_map_filter split_def o_def option.map_comp map_filter_map_option_const sorted_filter[where f=id, simplified] rbt_sorted_entries distinct_entries map_of_sinter_with map_of_eq_None_iff set_map_filter split: option.split compare.split intro: rev_image_eqI dest: rbt_sorted_entries_right_unique)
    1.74  
    1.75  lemma rbt_lookup_rbt_inter:
    1.76    "\<lbrakk> rbt_sorted t1; rbt_sorted t2 \<rbrakk>