various refinements
authorhaftmann
Fri Mar 05 17:51:29 2010 +0100 (2010-03-05)
changeset 35602e814157560e8
parent 35565 56b070cd7ab3
child 35603 c0db094d0d80
various refinements
src/HOL/Library/RBT.thy
     1.1 --- a/src/HOL/Library/RBT.thy	Thu Mar 04 11:22:06 2010 +0100
     1.2 +++ b/src/HOL/Library/RBT.thy	Fri Mar 05 17:51:29 2010 +0100
     1.3 @@ -7,9 +7,22 @@
     1.4  
     1.5  (*<*)
     1.6  theory RBT
     1.7 -imports Main AssocList
     1.8 +imports Main
     1.9  begin
    1.10  
    1.11 +lemma map_sorted_distinct_set_unique: (*FIXME move*)
    1.12 +  assumes "inj_on f (set xs \<union> set ys)"
    1.13 +  assumes "sorted (map f xs)" "distinct (map f xs)"
    1.14 +    "sorted (map f ys)" "distinct (map f ys)"
    1.15 +  assumes "set xs = set ys"
    1.16 +  shows "xs = ys"
    1.17 +proof -
    1.18 +  from assms have "map f xs = map f ys"
    1.19 +    by (simp add: sorted_distinct_set_unique)
    1.20 +  moreover with `inj_on f (set xs \<union> set ys)` show "xs = ys"
    1.21 +    by (blast intro: map_inj_on)
    1.22 +qed
    1.23 +
    1.24  subsection {* Datatype of RB trees *}
    1.25  
    1.26  datatype color = R | B
    1.27 @@ -54,6 +67,10 @@
    1.28    then show ?thesis by (simp add: keys_def)
    1.29  qed
    1.30  
    1.31 +lemma keys_entries:
    1.32 +  "k \<in> set (keys t) \<longleftrightarrow> (\<exists>v. (k, v) \<in> set (entries t))"
    1.33 +  by (auto intro: entry_in_tree_keys) (auto simp add: keys_def)
    1.34 +
    1.35  
    1.36  subsubsection {* Search tree properties *}
    1.37  
    1.38 @@ -144,9 +161,6 @@
    1.39  lemma lookup_tree_greater[simp]: "k \<guillemotleft>| t \<Longrightarrow> lookup t k = None"
    1.40  by (induct t) auto
    1.41  
    1.42 -lemma lookup_in_tree: "sorted t \<Longrightarrow> (lookup t k = Some v) = entry_in_tree k v t"
    1.43 -by (induct t) (auto simp: tree_less_prop tree_greater_prop entry_in_tree_keys)
    1.44 -
    1.45  lemma lookup_Empty: "lookup Empty = empty"
    1.46  by (rule ext) simp
    1.47  
    1.48 @@ -215,36 +229,45 @@
    1.49    finally show ?case .
    1.50  qed
    1.51  
    1.52 -(*lemma map_of_inject:
    1.53 -  assumes distinct: "distinct (map fst xs)" "distinct (map fst ys)"
    1.54 -  shows "map_of xs = map_of ys \<longleftrightarrow> set xs = set ys"
    1.55 +lemma lookup_in_tree: "sorted t \<Longrightarrow> lookup t k = Some v \<longleftrightarrow> (k, v) \<in> set (entries t)"
    1.56 +  by (simp_all add: lookup_map_of_entries distinct_entries)
    1.57 +
    1.58 +lemma set_entries_inject:
    1.59 +  assumes sorted: "sorted t1" "sorted t2" 
    1.60 +  shows "set (entries t1) = set (entries t2) \<longleftrightarrow> entries t1 = entries t2"
    1.61 +proof -
    1.62 +  from sorted have "distinct (map fst (entries t1))"
    1.63 +    "distinct (map fst (entries t2))"
    1.64 +    by (auto intro: distinct_entries)
    1.65 +  with sorted show ?thesis
    1.66 +    by (auto intro: map_sorted_distinct_set_unique sorted_entries simp add: distinct_map)
    1.67 +qed
    1.68  
    1.69  lemma entries_eqI:
    1.70    assumes sorted: "sorted t1" "sorted t2" 
    1.71    assumes lookup: "lookup t1 = lookup t2"
    1.72 -  shows entries: "entries t1 = entries t2"
    1.73 +  shows "entries t1 = entries t2"
    1.74  proof -
    1.75    from sorted lookup have "map_of (entries t1) = map_of (entries t2)"
    1.76 -    by (simp_all add: lookup_map_of_entries)
    1.77 -qed*)
    1.78 +    by (simp add: lookup_map_of_entries)
    1.79 +  with sorted have "set (entries t1) = set (entries t2)"
    1.80 +    by (simp add: map_of_inject_set distinct_entries)
    1.81 +  with sorted show ?thesis by (simp add: set_entries_inject)
    1.82 +qed
    1.83  
    1.84 -(* a kind of extensionality *)
    1.85 +lemma entries_lookup:
    1.86 +  assumes "sorted t1" "sorted t2" 
    1.87 +  shows "entries t1 = entries t2 \<longleftrightarrow> lookup t1 = lookup t2"
    1.88 +  using assms by (auto intro: entries_eqI simp add: lookup_map_of_entries)
    1.89 +
    1.90  lemma lookup_from_in_tree: 
    1.91 -  assumes sorted: "sorted t1" "sorted t2" 
    1.92 -  and eq: "\<And>v. entry_in_tree (k\<Colon>'a\<Colon>linorder) v t1 = entry_in_tree k v t2" 
    1.93 +  assumes "sorted t1" "sorted t2" 
    1.94 +  and "\<And>v. (k\<Colon>'a\<Colon>linorder, v) \<in> set (entries t1) \<longleftrightarrow> (k, v) \<in> set (entries t2)" 
    1.95    shows "lookup t1 k = lookup t2 k"
    1.96 -proof (cases "lookup t1 k")
    1.97 -  case None
    1.98 -  then have "\<And>v. \<not> entry_in_tree k v t1"
    1.99 -    by (simp add: lookup_in_tree[symmetric] sorted)
   1.100 -  with None show ?thesis
   1.101 -    by (cases "lookup t2 k") (auto simp: lookup_in_tree sorted eq)
   1.102 -next
   1.103 -  case (Some a)
   1.104 -  then show ?thesis
   1.105 -    apply (cases "lookup t2 k")
   1.106 -    apply (auto simp: lookup_in_tree sorted eq)
   1.107 -    by (auto simp add: lookup_in_tree[symmetric] sorted Some)
   1.108 +proof -
   1.109 +  from assms have "k \<in> dom (lookup t1) \<longleftrightarrow> k \<in> dom (lookup t2)"
   1.110 +    by (simp add: keys_entries lookup_keys)
   1.111 +  with assms show ?thesis by (auto simp add: lookup_in_tree [symmetric])
   1.112  qed
   1.113  
   1.114  
   1.115 @@ -984,32 +1007,36 @@
   1.116  subsection {* Modifying existing entries *}
   1.117  
   1.118  primrec
   1.119 -  map_entry :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a\<Colon>linorder) \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"
   1.120 +  map_entry :: "'a\<Colon>linorder \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt"
   1.121  where
   1.122 -  "map_entry f k Empty = Empty"
   1.123 -| "map_entry f k (Branch c lt x v rt) = (if k < x then (Branch c (map_entry f k lt) x v rt) else if k > x then (Branch c lt x v (map_entry f k rt)) else (Branch c lt x (f x v) rt))"
   1.124 +  "map_entry k f Empty = Empty"
   1.125 +| "map_entry k f (Branch c lt x v rt) =
   1.126 +    (if k < x then Branch c (map_entry k f lt) x v rt
   1.127 +    else if k > x then (Branch c lt x v (map_entry k f rt))
   1.128 +    else Branch c lt x (f v) rt)"
   1.129  
   1.130 -lemma map_entrywk_color_of: "color_of (map_entry f k t) = color_of t" by (induct t) simp+
   1.131 -lemma map_entrywk_inv1: "inv1 (map_entry f k t) = inv1 t" by (induct t) (simp add: map_entrywk_color_of)+
   1.132 -lemma map_entrywk_inv2: "inv2 (map_entry f k t) = inv2 t" "bheight (map_entry f k t) = bheight t" by (induct t) simp+
   1.133 -lemma map_entrywk_tree_greater: "tree_greater k (map_entry f kk t) = tree_greater k t" by (induct t) simp+
   1.134 -lemma map_entrywk_tree_less: "tree_less k (map_entry f kk t) = tree_less k t" by (induct t) simp+
   1.135 -lemma map_entrywk_sorted: "sorted (map_entry f k t) = sorted t" by (induct t) (simp add: map_entrywk_tree_less map_entrywk_tree_greater)+
   1.136 +lemma map_entry_color_of: "color_of (map_entry k f t) = color_of t" by (induct t) simp+
   1.137 +lemma map_entry_inv1: "inv1 (map_entry k f t) = inv1 t" by (induct t) (simp add: map_entry_color_of)+
   1.138 +lemma map_entry_inv2: "inv2 (map_entry k f t) = inv2 t" "bheight (map_entry k f t) = bheight t" by (induct t) simp+
   1.139 +lemma map_entry_tree_greater: "tree_greater a (map_entry k f t) = tree_greater a t" by (induct t) simp+
   1.140 +lemma map_entry_tree_less: "tree_less a (map_entry k f t) = tree_less a t" by (induct t) simp+
   1.141 +lemma map_entry_sorted: "sorted (map_entry k f t) = sorted t"
   1.142 +  by (induct t) (simp_all add: map_entry_tree_less map_entry_tree_greater)
   1.143  
   1.144 -theorem map_entrywk_is_rbt [simp]: "is_rbt (map_entry f k t) = is_rbt t" 
   1.145 -unfolding is_rbt_def by (simp add: map_entrywk_inv2 map_entrywk_color_of map_entrywk_sorted map_entrywk_inv1 )
   1.146 +theorem map_entry_is_rbt [simp]: "is_rbt (map_entry k f t) = is_rbt t" 
   1.147 +unfolding is_rbt_def by (simp add: map_entry_inv2 map_entry_color_of map_entry_sorted map_entry_inv1 )
   1.148  
   1.149  theorem map_entry_map [simp]:
   1.150 -  "lookup (map_entry f k t) x = 
   1.151 -  (if x = k then case lookup t x of None \<Rightarrow> None | Some y \<Rightarrow> Some (f k y)
   1.152 +  "lookup (map_entry k f t) x = 
   1.153 +  (if x = k then case lookup t x of None \<Rightarrow> None | Some y \<Rightarrow> Some (f y)
   1.154              else lookup t x)"
   1.155 -by (induct t arbitrary: x) (auto split:option.splits)
   1.156 +  by (induct t arbitrary: x) (auto split:option.splits)
   1.157  
   1.158  
   1.159  subsection {* Mapping all entries *}
   1.160  
   1.161  primrec
   1.162 -  map :: "('a::linorder \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'c) rbt"
   1.163 +  map :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'c) rbt"
   1.164  where
   1.165    "map f Empty = Empty"
   1.166  | "map f (Branch c lt k v rt) = Branch c (map f lt) k (f k v) (map f rt)"