theory RBT with abstract type of red-black trees backed by implementation RBT_Impl
1.1 --- a/NEWS Wed Apr 14 22:18:10 2010 +0200
1.2 +++ b/NEWS Thu Apr 15 12:27:14 2010 +0200
1.3 @@ -74,6 +74,8 @@
1.4
1.5 *** Pure ***
1.6
1.7 +* Code generator: simple concept for abstract datatypes obeying invariants.
1.8 +
1.9 * Local theory specifications may depend on extra type variables that
1.10 are not present in the result type -- arguments TYPE('a) :: 'a itself
1.11 are added internally. For example:
1.12 @@ -106,6 +108,10 @@
1.13
1.14 *** HOL ***
1.15
1.16 +* Library theory 'RBT' renamed to 'RBT_Impl'; new library theory 'RBT'
1.17 +provides abstract red-black tree type which is backed by RBT_Impl
1.18 +as implementation. INCOMPATIBILTY.
1.19 +
1.20 * Command 'typedef' now works within a local theory context -- without
1.21 introducing dependencies on parameters or assumptions, which is not
1.22 possible in Isabelle/Pure/HOL. Note that the logical environment may
2.1 --- a/src/HOL/Imperative_HOL/ex/SatChecker.thy Wed Apr 14 22:18:10 2010 +0200
2.2 +++ b/src/HOL/Imperative_HOL/ex/SatChecker.thy Thu Apr 15 12:27:14 2010 +0200
2.3 @@ -5,7 +5,7 @@
2.4 header {* An efficient checker for proofs from a SAT solver *}
2.5
2.6 theory SatChecker
2.7 -imports RBT Sorted_List "~~/src/HOL/Imperative_HOL/Imperative_HOL"
2.8 +imports RBT_Impl Sorted_List "~~/src/HOL/Imperative_HOL/Imperative_HOL"
2.9 begin
2.10
2.11 section{* General settings and functions for our representation of clauses *}
2.12 @@ -635,24 +635,24 @@
2.13
2.14 section {* Functional version with RedBlackTrees *}
2.15
2.16 -fun tres_thm :: "(ClauseId, Clause) rbt \<Rightarrow> Lit \<times> ClauseId \<Rightarrow> Clause \<Rightarrow> Clause Heap"
2.17 +fun tres_thm :: "(ClauseId, Clause) RBT_Impl.rbt \<Rightarrow> Lit \<times> ClauseId \<Rightarrow> Clause \<Rightarrow> Clause Heap"
2.18 where
2.19 "tres_thm t (l, j) cli =
2.20 - (case (RBT.lookup t j) of
2.21 + (case (RBT_Impl.lookup t j) of
2.22 None \<Rightarrow> raise (''MiniSatChecked.res_thm: No resolvant clause in thms array for Conflict step.'')
2.23 | Some clj \<Rightarrow> res_thm' l cli clj)"
2.24
2.25 -fun tdoProofStep :: " ProofStep \<Rightarrow> ((ClauseId, Clause) rbt * Clause list) \<Rightarrow> ((ClauseId, Clause) rbt * Clause list) Heap"
2.26 +fun tdoProofStep :: " ProofStep \<Rightarrow> ((ClauseId, Clause) RBT_Impl.rbt * Clause list) \<Rightarrow> ((ClauseId, Clause) RBT_Impl.rbt * Clause list) Heap"
2.27 where
2.28 "tdoProofStep (Conflict saveTo (i, rs)) (t, rcl) =
2.29 - (case (RBT.lookup t i) of
2.30 + (case (RBT_Impl.lookup t i) of
2.31 None \<Rightarrow> raise (''MiniSatChecked.doProofStep: No starting clause in thms array for Conflict step.'')
2.32 | Some cli \<Rightarrow> (do
2.33 result \<leftarrow> foldM (tres_thm t) rs cli;
2.34 - return ((RBT.insert saveTo result t), rcl)
2.35 + return ((RBT_Impl.insert saveTo result t), rcl)
2.36 done))"
2.37 -| "tdoProofStep (Delete cid) (t, rcl) = return ((RBT.delete cid t), rcl)"
2.38 -| "tdoProofStep (Root cid clause) (t, rcl) = return (RBT.insert cid (sort clause) t, (remdups(sort clause)) # rcl)"
2.39 +| "tdoProofStep (Delete cid) (t, rcl) = return ((RBT_Impl.delete cid t), rcl)"
2.40 +| "tdoProofStep (Root cid clause) (t, rcl) = return (RBT_Impl.insert cid (sort clause) t, (remdups(sort clause)) # rcl)"
2.41 | "tdoProofStep (Xstep cid1 cid2) (t, rcl) = raise ''MiniSatChecked.doProofStep: Xstep constructor found.''"
2.42 | "tdoProofStep (ProofDone b) (t, rcl) = raise ''MiniSatChecked.doProofStep: ProofDone constructor found.''"
2.43
2.44 @@ -660,8 +660,8 @@
2.45 where
2.46 "tchecker n p i =
2.47 (do
2.48 - rcs \<leftarrow> foldM (tdoProofStep) p (RBT.Empty, []);
2.49 - (if (RBT.lookup (fst rcs) i) = Some [] then return (snd rcs)
2.50 + rcs \<leftarrow> foldM (tdoProofStep) p (RBT_Impl.Empty, []);
2.51 + (if (RBT_Impl.lookup (fst rcs) i) = Some [] then return (snd rcs)
2.52 else raise(''No empty clause''))
2.53 done)"
2.54
3.1 --- a/src/HOL/IsaMakefile Wed Apr 14 22:18:10 2010 +0200
3.2 +++ b/src/HOL/IsaMakefile Thu Apr 15 12:27:14 2010 +0200
3.3 @@ -1,3 +1,4 @@
3.4 +
3.5 #
3.6 # IsaMakefile for HOL
3.7 #
3.8 @@ -406,14 +407,15 @@
3.9 Library/Library/ROOT.ML Library/Library/document/root.tex \
3.10 Library/Library/document/root.bib \
3.11 Library/Transitive_Closure_Table.thy Library/While_Combinator.thy \
3.12 - Library/Product_ord.thy Library/Char_nat.thy Library/Table.thy \
3.13 + Library/Product_ord.thy Library/Char_nat.thy \
3.14 Library/Sublist_Order.thy Library/List_lexord.thy \
3.15 Library/AssocList.thy Library/Formal_Power_Series.thy \
3.16 Library/Binomial.thy Library/Eval_Witness.thy Library/Code_Char.thy \
3.17 Library/Code_Char_chr.thy Library/Code_Integer.thy \
3.18 Library/Mapping.thy Library/Numeral_Type.thy Library/Reflection.thy \
3.19 Library/Boolean_Algebra.thy Library/Countable.thy \
3.20 - Library/Diagonalize.thy Library/RBT.thy Library/Univ_Poly.thy \
3.21 + Library/Diagonalize.thy Library/RBT.thy Library/RBT_Impl.thy \
3.22 + Library/Univ_Poly.thy \
3.23 Library/Poly_Deriv.thy Library/Polynomial.thy Library/Preorder.thy \
3.24 Library/Product_plus.thy Library/Product_Vector.thy \
3.25 Library/Enum.thy Library/Float.thy Library/Quotient_List.thy \
4.1 --- a/src/HOL/Library/Library.thy Wed Apr 14 22:18:10 2010 +0200
4.2 +++ b/src/HOL/Library/Library.thy Thu Apr 15 12:27:14 2010 +0200
4.3 @@ -57,7 +57,6 @@
4.4 SML_Quickcheck
4.5 State_Monad
4.6 Sum_Of_Squares
4.7 - Table
4.8 Transitive_Closure_Table
4.9 Univ_Poly
4.10 While_Combinator
5.1 --- a/src/HOL/Library/RBT.thy Wed Apr 14 22:18:10 2010 +0200
5.2 +++ b/src/HOL/Library/RBT.thy Thu Apr 15 12:27:14 2010 +0200
5.3 @@ -1,1100 +1,253 @@
5.4 -(* Title: RBT.thy
5.5 - Author: Markus Reiter, TU Muenchen
5.6 - Author: Alexander Krauss, TU Muenchen
5.7 -*)
5.8 +(* Author: Florian Haftmann, TU Muenchen *)
5.9
5.10 -header {* Red-Black Trees *}
5.11 +header {* Abstract type of Red-Black Trees *}
5.12
5.13 (*<*)
5.14 theory RBT
5.15 -imports Main
5.16 +imports Main RBT_Impl Mapping
5.17 begin
5.18
5.19 -subsection {* Datatype of RB trees *}
5.20 +subsection {* Type definition *}
5.21
5.22 -datatype color = R | B
5.23 -datatype ('a, 'b) rbt = Empty | Branch color "('a, 'b) rbt" 'a 'b "('a, 'b) rbt"
5.24 -
5.25 -lemma rbt_cases:
5.26 - obtains (Empty) "t = Empty"
5.27 - | (Red) l k v r where "t = Branch R l k v r"
5.28 - | (Black) l k v r where "t = Branch B l k v r"
5.29 -proof (cases t)
5.30 - case Empty with that show thesis by blast
5.31 -next
5.32 - case (Branch c) with that show thesis by (cases c) blast+
5.33 +typedef (open) ('a, 'b) rbt = "{t :: ('a\<Colon>linorder, 'b) RBT_Impl.rbt. is_rbt t}"
5.34 + morphisms impl_of RBT
5.35 +proof -
5.36 + have "RBT_Impl.Empty \<in> ?rbt" by simp
5.37 + then show ?thesis ..
5.38 qed
5.39
5.40 -subsection {* Tree properties *}
5.41 +lemma is_rbt_impl_of [simp, intro]:
5.42 + "is_rbt (impl_of t)"
5.43 + using impl_of [of t] by simp
5.44
5.45 -subsubsection {* Content of a tree *}
5.46 +lemma rbt_eq:
5.47 + "t1 = t2 \<longleftrightarrow> impl_of t1 = impl_of t2"
5.48 + by (simp add: impl_of_inject)
5.49
5.50 -primrec entries :: "('a, 'b) rbt \<Rightarrow> ('a \<times> 'b) list"
5.51 -where
5.52 - "entries Empty = []"
5.53 -| "entries (Branch _ l k v r) = entries l @ (k,v) # entries r"
5.54 +lemma [code abstype]:
5.55 + "RBT (impl_of t) = t"
5.56 + by (simp add: impl_of_inverse)
5.57
5.58 -abbreviation (input) entry_in_tree :: "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b) rbt \<Rightarrow> bool"
5.59 -where
5.60 - "entry_in_tree k v t \<equiv> (k, v) \<in> set (entries t)"
5.61
5.62 -definition keys :: "('a, 'b) rbt \<Rightarrow> 'a list" where
5.63 - "keys t = map fst (entries t)"
5.64 +subsection {* Primitive operations *}
5.65
5.66 -lemma keys_simps [simp, code]:
5.67 - "keys Empty = []"
5.68 - "keys (Branch c l k v r) = keys l @ k # keys r"
5.69 - by (simp_all add: keys_def)
5.70 +definition lookup :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'a \<rightharpoonup> 'b" where
5.71 + [code]: "lookup t = RBT_Impl.lookup (impl_of t)"
5.72
5.73 -lemma entry_in_tree_keys:
5.74 - assumes "(k, v) \<in> set (entries t)"
5.75 - shows "k \<in> set (keys t)"
5.76 -proof -
5.77 - from assms have "fst (k, v) \<in> fst ` set (entries t)" by (rule imageI)
5.78 - then show ?thesis by (simp add: keys_def)
5.79 -qed
5.80 +definition empty :: "('a\<Colon>linorder, 'b) rbt" where
5.81 + "empty = RBT RBT_Impl.Empty"
5.82
5.83 -lemma keys_entries:
5.84 - "k \<in> set (keys t) \<longleftrightarrow> (\<exists>v. (k, v) \<in> set (entries t))"
5.85 - by (auto intro: entry_in_tree_keys) (auto simp add: keys_def)
5.86 +lemma impl_of_empty [code abstract]:
5.87 + "impl_of empty = RBT_Impl.Empty"
5.88 + by (simp add: empty_def RBT_inverse)
5.89
5.90 +definition insert :: "'a\<Colon>linorder \<Rightarrow> 'b \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt" where
5.91 + "insert k v t = RBT (RBT_Impl.insert k v (impl_of t))"
5.92
5.93 -subsubsection {* Search tree properties *}
5.94 +lemma impl_of_insert [code abstract]:
5.95 + "impl_of (insert k v t) = RBT_Impl.insert k v (impl_of t)"
5.96 + by (simp add: insert_def RBT_inverse)
5.97
5.98 -definition tree_less :: "'a\<Colon>order \<Rightarrow> ('a, 'b) rbt \<Rightarrow> bool"
5.99 -where
5.100 - tree_less_prop: "tree_less k t \<longleftrightarrow> (\<forall>x\<in>set (keys t). x < k)"
5.101 +definition delete :: "'a\<Colon>linorder \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt" where
5.102 + "delete k t = RBT (RBT_Impl.delete k (impl_of t))"
5.103
5.104 -abbreviation tree_less_symbol (infix "|\<guillemotleft>" 50)
5.105 -where "t |\<guillemotleft> x \<equiv> tree_less x t"
5.106 +lemma impl_of_delete [code abstract]:
5.107 + "impl_of (delete k t) = RBT_Impl.delete k (impl_of t)"
5.108 + by (simp add: delete_def RBT_inverse)
5.109
5.110 -definition tree_greater :: "'a\<Colon>order \<Rightarrow> ('a, 'b) rbt \<Rightarrow> bool" (infix "\<guillemotleft>|" 50)
5.111 -where
5.112 - tree_greater_prop: "tree_greater k t = (\<forall>x\<in>set (keys t). k < x)"
5.113 +definition entries :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a \<times> 'b) list" where
5.114 + [code]: "entries t = RBT_Impl.entries (impl_of t)"
5.115
5.116 -lemma tree_less_simps [simp]:
5.117 - "tree_less k Empty = True"
5.118 - "tree_less k (Branch c lt kt v rt) \<longleftrightarrow> kt < k \<and> tree_less k lt \<and> tree_less k rt"
5.119 - by (auto simp add: tree_less_prop)
5.120 +definition keys :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'a list" where
5.121 + [code]: "keys t = RBT_Impl.keys (impl_of t)"
5.122
5.123 -lemma tree_greater_simps [simp]:
5.124 - "tree_greater k Empty = True"
5.125 - "tree_greater k (Branch c lt kt v rt) \<longleftrightarrow> k < kt \<and> tree_greater k lt \<and> tree_greater k rt"
5.126 - by (auto simp add: tree_greater_prop)
5.127 +definition bulkload :: "('a\<Colon>linorder \<times> 'b) list \<Rightarrow> ('a, 'b) rbt" where
5.128 + "bulkload xs = RBT (RBT_Impl.bulkload xs)"
5.129
5.130 -lemmas tree_ord_props = tree_less_prop tree_greater_prop
5.131 +lemma impl_of_bulkload [code abstract]:
5.132 + "impl_of (bulkload xs) = RBT_Impl.bulkload xs"
5.133 + by (simp add: bulkload_def RBT_inverse)
5.134
5.135 -lemmas tree_greater_nit = tree_greater_prop entry_in_tree_keys
5.136 -lemmas tree_less_nit = tree_less_prop entry_in_tree_keys
5.137 +definition map_entry :: "'a \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a, 'b) rbt" where
5.138 + "map_entry k f t = RBT (RBT_Impl.map_entry k f (impl_of t))"
5.139
5.140 -lemma tree_less_eq_trans: "l |\<guillemotleft> u \<Longrightarrow> u \<le> v \<Longrightarrow> l |\<guillemotleft> v"
5.141 - and tree_less_trans: "t |\<guillemotleft> x \<Longrightarrow> x < y \<Longrightarrow> t |\<guillemotleft> y"
5.142 - and tree_greater_eq_trans: "u \<le> v \<Longrightarrow> v \<guillemotleft>| r \<Longrightarrow> u \<guillemotleft>| r"
5.143 - and tree_greater_trans: "x < y \<Longrightarrow> y \<guillemotleft>| t \<Longrightarrow> x \<guillemotleft>| t"
5.144 - by (auto simp: tree_ord_props)
5.145 +lemma impl_of_map_entry [code abstract]:
5.146 + "impl_of (map_entry k f t) = RBT_Impl.map_entry k f (impl_of t)"
5.147 + by (simp add: map_entry_def RBT_inverse)
5.148
5.149 -primrec sorted :: "('a::linorder, 'b) rbt \<Rightarrow> bool"
5.150 -where
5.151 - "sorted Empty = True"
5.152 -| "sorted (Branch c l k v r) = (l |\<guillemotleft> k \<and> k \<guillemotleft>| r \<and> sorted l \<and> sorted r)"
5.153 +definition map :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a, 'b) rbt" where
5.154 + "map f t = RBT (RBT_Impl.map f (impl_of t))"
5.155
5.156 -lemma sorted_entries:
5.157 - "sorted t \<Longrightarrow> List.sorted (List.map fst (entries t))"
5.158 -by (induct t)
5.159 - (force simp: sorted_append sorted_Cons tree_ord_props
5.160 - dest!: entry_in_tree_keys)+
5.161 +lemma impl_of_map [code abstract]:
5.162 + "impl_of (map f t) = RBT_Impl.map f (impl_of t)"
5.163 + by (simp add: map_def RBT_inverse)
5.164
5.165 -lemma distinct_entries:
5.166 - "sorted t \<Longrightarrow> distinct (List.map fst (entries t))"
5.167 -by (induct t)
5.168 - (force simp: sorted_append sorted_Cons tree_ord_props
5.169 - dest!: entry_in_tree_keys)+
5.170 +definition fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'c \<Rightarrow> 'c" where
5.171 + [code]: "fold f t = RBT_Impl.fold f (impl_of t)"
5.172
5.173
5.174 -subsubsection {* Tree lookup *}
5.175 +subsection {* Derived operations *}
5.176
5.177 -primrec lookup :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'a \<rightharpoonup> 'b"
5.178 -where
5.179 - "lookup Empty k = None"
5.180 -| "lookup (Branch _ l x y r) k = (if k < x then lookup l k else if x < k then lookup r k else Some y)"
5.181 +definition is_empty :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> bool" where
5.182 + [code]: "is_empty t = (case impl_of t of RBT_Impl.Empty \<Rightarrow> True | _ \<Rightarrow> False)"
5.183
5.184 -lemma lookup_keys: "sorted t \<Longrightarrow> dom (lookup t) = set (keys t)"
5.185 - by (induct t) (auto simp: dom_def tree_greater_prop tree_less_prop)
5.186
5.187 -lemma dom_lookup_Branch:
5.188 - "sorted (Branch c t1 k v t2) \<Longrightarrow>
5.189 - dom (lookup (Branch c t1 k v t2))
5.190 - = Set.insert k (dom (lookup t1) \<union> dom (lookup t2))"
5.191 -proof -
5.192 - assume "sorted (Branch c t1 k v t2)"
5.193 - moreover from this have "sorted t1" "sorted t2" by simp_all
5.194 - ultimately show ?thesis by (simp add: lookup_keys)
5.195 -qed
5.196 +subsection {* Abstract lookup properties *}
5.197
5.198 -lemma finite_dom_lookup [simp, intro!]: "finite (dom (lookup t))"
5.199 -proof (induct t)
5.200 - case Empty then show ?case by simp
5.201 -next
5.202 - case (Branch color t1 a b t2)
5.203 - let ?A = "Set.insert a (dom (lookup t1) \<union> dom (lookup t2))"
5.204 - have "dom (lookup (Branch color t1 a b t2)) \<subseteq> ?A" by (auto split: split_if_asm)
5.205 - moreover from Branch have "finite (insert a (dom (lookup t1) \<union> dom (lookup t2)))" by simp
5.206 - ultimately show ?case by (rule finite_subset)
5.207 -qed
5.208 +lemma lookup_RBT:
5.209 + "is_rbt t \<Longrightarrow> lookup (RBT t) = RBT_Impl.lookup t"
5.210 + by (simp add: lookup_def RBT_inverse)
5.211
5.212 -lemma lookup_tree_less[simp]: "t |\<guillemotleft> k \<Longrightarrow> lookup t k = None"
5.213 -by (induct t) auto
5.214 +lemma lookup_impl_of:
5.215 + "RBT_Impl.lookup (impl_of t) = lookup t"
5.216 + by (simp add: lookup_def)
5.217
5.218 -lemma lookup_tree_greater[simp]: "k \<guillemotleft>| t \<Longrightarrow> lookup t k = None"
5.219 -by (induct t) auto
5.220 +lemma entries_impl_of:
5.221 + "RBT_Impl.entries (impl_of t) = entries t"
5.222 + by (simp add: entries_def)
5.223
5.224 -lemma lookup_Empty: "lookup Empty = empty"
5.225 -by (rule ext) simp
5.226 +lemma keys_impl_of:
5.227 + "RBT_Impl.keys (impl_of t) = keys t"
5.228 + by (simp add: keys_def)
5.229
5.230 -lemma map_of_entries:
5.231 - "sorted t \<Longrightarrow> map_of (entries t) = lookup t"
5.232 -proof (induct t)
5.233 - case Empty thus ?case by (simp add: lookup_Empty)
5.234 -next
5.235 - case (Branch c t1 k v t2)
5.236 - have "lookup (Branch c t1 k v t2) = lookup t2 ++ [k\<mapsto>v] ++ lookup t1"
5.237 - proof (rule ext)
5.238 - fix x
5.239 - from Branch have SORTED: "sorted (Branch c t1 k v t2)" by simp
5.240 - let ?thesis = "lookup (Branch c t1 k v t2) x = (lookup t2 ++ [k \<mapsto> v] ++ lookup t1) x"
5.241 +lemma lookup_empty [simp]:
5.242 + "lookup empty = Map.empty"
5.243 + by (simp add: empty_def lookup_RBT expand_fun_eq)
5.244
5.245 - have DOM_T1: "!!k'. k'\<in>dom (lookup t1) \<Longrightarrow> k>k'"
5.246 - proof -
5.247 - fix k'
5.248 - from SORTED have "t1 |\<guillemotleft> k" by simp
5.249 - with tree_less_prop have "\<forall>k'\<in>set (keys t1). k>k'" by auto
5.250 - moreover assume "k'\<in>dom (lookup t1)"
5.251 - ultimately show "k>k'" using lookup_keys SORTED by auto
5.252 - qed
5.253 -
5.254 - have DOM_T2: "!!k'. k'\<in>dom (lookup t2) \<Longrightarrow> k<k'"
5.255 - proof -
5.256 - fix k'
5.257 - from SORTED have "k \<guillemotleft>| t2" by simp
5.258 - with tree_greater_prop have "\<forall>k'\<in>set (keys t2). k<k'" by auto
5.259 - moreover assume "k'\<in>dom (lookup t2)"
5.260 - ultimately show "k<k'" using lookup_keys SORTED by auto
5.261 - qed
5.262 -
5.263 - {
5.264 - assume C: "x<k"
5.265 - hence "lookup (Branch c t1 k v t2) x = lookup t1 x" by simp
5.266 - moreover from C have "x\<notin>dom [k\<mapsto>v]" by simp
5.267 - moreover have "x\<notin>dom (lookup t2)" proof
5.268 - assume "x\<in>dom (lookup t2)"
5.269 - with DOM_T2 have "k<x" by blast
5.270 - with C show False by simp
5.271 - qed
5.272 - ultimately have ?thesis by (simp add: map_add_upd_left map_add_dom_app_simps)
5.273 - } moreover {
5.274 - assume [simp]: "x=k"
5.275 - hence "lookup (Branch c t1 k v t2) x = [k \<mapsto> v] x" by simp
5.276 - moreover have "x\<notin>dom (lookup t1)" proof
5.277 - assume "x\<in>dom (lookup t1)"
5.278 - with DOM_T1 have "k>x" by blast
5.279 - thus False by simp
5.280 - qed
5.281 - ultimately have ?thesis by (simp add: map_add_upd_left map_add_dom_app_simps)
5.282 - } moreover {
5.283 - assume C: "x>k"
5.284 - hence "lookup (Branch c t1 k v t2) x = lookup t2 x" by (simp add: less_not_sym[of k x])
5.285 - moreover from C have "x\<notin>dom [k\<mapsto>v]" by simp
5.286 - moreover have "x\<notin>dom (lookup t1)" proof
5.287 - assume "x\<in>dom (lookup t1)"
5.288 - with DOM_T1 have "k>x" by simp
5.289 - with C show False by simp
5.290 - qed
5.291 - ultimately have ?thesis by (simp add: map_add_upd_left map_add_dom_app_simps)
5.292 - } ultimately show ?thesis using less_linear by blast
5.293 - qed
5.294 - also from Branch have "lookup t2 ++ [k \<mapsto> v] ++ lookup t1 = map_of (entries (Branch c t1 k v t2))" by simp
5.295 - finally show ?case by simp
5.296 -qed
5.297 +lemma lookup_insert [simp]:
5.298 + "lookup (insert k v t) = (lookup t)(k \<mapsto> v)"
5.299 + by (simp add: insert_def lookup_RBT lookup_insert lookup_impl_of)
5.300
5.301 -lemma lookup_in_tree: "sorted t \<Longrightarrow> lookup t k = Some v \<longleftrightarrow> (k, v) \<in> set (entries t)"
5.302 - by (simp add: map_of_entries [symmetric] distinct_entries)
5.303 +lemma lookup_delete [simp]:
5.304 + "lookup (delete k t) = (lookup t)(k := None)"
5.305 + by (simp add: delete_def lookup_RBT RBT_Impl.lookup_delete lookup_impl_of restrict_complement_singleton_eq)
5.306
5.307 -lemma set_entries_inject:
5.308 - assumes sorted: "sorted t1" "sorted t2"
5.309 - shows "set (entries t1) = set (entries t2) \<longleftrightarrow> entries t1 = entries t2"
5.310 -proof -
5.311 - from sorted have "distinct (map fst (entries t1))"
5.312 - "distinct (map fst (entries t2))"
5.313 - by (auto intro: distinct_entries)
5.314 - with sorted show ?thesis
5.315 - by (auto intro: map_sorted_distinct_set_unique sorted_entries simp add: distinct_map)
5.316 -qed
5.317 -
5.318 -lemma entries_eqI:
5.319 - assumes sorted: "sorted t1" "sorted t2"
5.320 - assumes lookup: "lookup t1 = lookup t2"
5.321 - shows "entries t1 = entries t2"
5.322 -proof -
5.323 - from sorted lookup have "map_of (entries t1) = map_of (entries t2)"
5.324 - by (simp add: map_of_entries)
5.325 - with sorted have "set (entries t1) = set (entries t2)"
5.326 - by (simp add: map_of_inject_set distinct_entries)
5.327 - with sorted show ?thesis by (simp add: set_entries_inject)
5.328 -qed
5.329 +lemma map_of_entries [simp]:
5.330 + "map_of (entries t) = lookup t"
5.331 + by (simp add: entries_def map_of_entries lookup_impl_of)
5.332
5.333 lemma entries_lookup:
5.334 - assumes "sorted t1" "sorted t2"
5.335 - shows "entries t1 = entries t2 \<longleftrightarrow> lookup t1 = lookup t2"
5.336 - using assms by (auto intro: entries_eqI simp add: map_of_entries [symmetric])
5.337 + "entries t1 = entries t2 \<longleftrightarrow> lookup t1 = lookup t2"
5.338 + by (simp add: entries_def lookup_def entries_lookup)
5.339
5.340 -lemma lookup_from_in_tree:
5.341 - assumes "sorted t1" "sorted t2"
5.342 - and "\<And>v. (k\<Colon>'a\<Colon>linorder, v) \<in> set (entries t1) \<longleftrightarrow> (k, v) \<in> set (entries t2)"
5.343 - shows "lookup t1 k = lookup t2 k"
5.344 -proof -
5.345 - from assms have "k \<in> dom (lookup t1) \<longleftrightarrow> k \<in> dom (lookup t2)"
5.346 - by (simp add: keys_entries lookup_keys)
5.347 - with assms show ?thesis by (auto simp add: lookup_in_tree [symmetric])
5.348 -qed
5.349 +lemma lookup_bulkload [simp]:
5.350 + "lookup (bulkload xs) = map_of xs"
5.351 + by (simp add: bulkload_def lookup_RBT RBT_Impl.lookup_bulkload)
5.352
5.353 +lemma lookup_map_entry [simp]:
5.354 + "lookup (map_entry k f t) = (lookup t)(k := Option.map f (lookup t k))"
5.355 + by (simp add: map_entry_def lookup_RBT lookup_map_entry lookup_impl_of)
5.356
5.357 -subsubsection {* Red-black properties *}
5.358 +lemma lookup_map [simp]:
5.359 + "lookup (map f t) k = Option.map (f k) (lookup t k)"
5.360 + by (simp add: map_def lookup_RBT lookup_map lookup_impl_of)
5.361
5.362 -primrec color_of :: "('a, 'b) rbt \<Rightarrow> color"
5.363 -where
5.364 - "color_of Empty = B"
5.365 -| "color_of (Branch c _ _ _ _) = c"
5.366 +lemma fold_fold:
5.367 + "fold f t = (\<lambda>s. foldl (\<lambda>s (k, v). f k v s) s (entries t))"
5.368 + by (simp add: fold_def expand_fun_eq RBT_Impl.fold_def entries_impl_of)
5.369
5.370 -primrec bheight :: "('a,'b) rbt \<Rightarrow> nat"
5.371 -where
5.372 - "bheight Empty = 0"
5.373 -| "bheight (Branch c lt k v rt) = (if c = B then Suc (bheight lt) else bheight lt)"
5.374 +lemma is_empty_empty [simp]:
5.375 + "is_empty t \<longleftrightarrow> t = empty"
5.376 + by (simp add: rbt_eq is_empty_def impl_of_empty split: rbt.split)
5.377
5.378 -primrec inv1 :: "('a, 'b) rbt \<Rightarrow> bool"
5.379 -where
5.380 - "inv1 Empty = True"
5.381 -| "inv1 (Branch c lt k v rt) \<longleftrightarrow> inv1 lt \<and> inv1 rt \<and> (c = B \<or> color_of lt = B \<and> color_of rt = B)"
5.382 +lemma RBT_lookup_empty [simp]: (*FIXME*)
5.383 + "RBT_Impl.lookup t = Map.empty \<longleftrightarrow> t = RBT_Impl.Empty"
5.384 + by (cases t) (auto simp add: expand_fun_eq)
5.385
5.386 -primrec inv1l :: "('a, 'b) rbt \<Rightarrow> bool" -- {* Weaker version *}
5.387 -where
5.388 - "inv1l Empty = True"
5.389 -| "inv1l (Branch c l k v r) = (inv1 l \<and> inv1 r)"
5.390 -lemma [simp]: "inv1 t \<Longrightarrow> inv1l t" by (cases t) simp+
5.391 +lemma lookup_empty_empty [simp]:
5.392 + "lookup t = Map.empty \<longleftrightarrow> t = empty"
5.393 + by (cases t) (simp add: empty_def lookup_def RBT_inject RBT_inverse)
5.394
5.395 -primrec inv2 :: "('a, 'b) rbt \<Rightarrow> bool"
5.396 -where
5.397 - "inv2 Empty = True"
5.398 -| "inv2 (Branch c lt k v rt) = (inv2 lt \<and> inv2 rt \<and> bheight lt = bheight rt)"
5.399 +lemma sorted_keys [iff]:
5.400 + "sorted (keys t)"
5.401 + by (simp add: keys_def RBT_Impl.keys_def sorted_entries)
5.402
5.403 -definition is_rbt :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> bool" where
5.404 - "is_rbt t \<longleftrightarrow> inv1 t \<and> inv2 t \<and> color_of t = B \<and> sorted t"
5.405 +lemma distinct_keys [iff]:
5.406 + "distinct (keys t)"
5.407 + by (simp add: keys_def RBT_Impl.keys_def distinct_entries)
5.408
5.409 -lemma is_rbt_sorted [simp]:
5.410 - "is_rbt t \<Longrightarrow> sorted t" by (simp add: is_rbt_def)
5.411
5.412 -theorem Empty_is_rbt [simp]:
5.413 - "is_rbt Empty" by (simp add: is_rbt_def)
5.414 +subsection {* Implementation of mappings *}
5.415
5.416 +definition Mapping :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a, 'b) mapping" where
5.417 + "Mapping t = Mapping.Mapping (lookup t)"
5.418
5.419 -subsection {* Insertion *}
5.420 +code_datatype Mapping
5.421
5.422 -fun (* slow, due to massive case splitting *)
5.423 - balance :: "('a,'b) rbt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"
5.424 -where
5.425 - "balance (Branch R a w x b) s t (Branch R c y z d) = Branch R (Branch B a w x b) s t (Branch B c y z d)" |
5.426 - "balance (Branch R (Branch R a w x b) s t c) y z d = Branch R (Branch B a w x b) s t (Branch B c y z d)" |
5.427 - "balance (Branch R a w x (Branch R b s t c)) y z d = Branch R (Branch B a w x b) s t (Branch B c y z d)" |
5.428 - "balance a w x (Branch R b s t (Branch R c y z d)) = Branch R (Branch B a w x b) s t (Branch B c y z d)" |
5.429 - "balance a w x (Branch R (Branch R b s t c) y z d) = Branch R (Branch B a w x b) s t (Branch B c y z d)" |
5.430 - "balance a s t b = Branch B a s t b"
5.431 +lemma lookup_Mapping [simp, code]:
5.432 + "Mapping.lookup (Mapping t) = lookup t"
5.433 + by (simp add: Mapping_def)
5.434
5.435 -lemma balance_inv1: "\<lbrakk>inv1l l; inv1l r\<rbrakk> \<Longrightarrow> inv1 (balance l k v r)"
5.436 - by (induct l k v r rule: balance.induct) auto
5.437 +lemma empty_Mapping [code]:
5.438 + "Mapping.empty = Mapping empty"
5.439 + by (rule mapping_eqI) simp
5.440
5.441 -lemma balance_bheight: "bheight l = bheight r \<Longrightarrow> bheight (balance l k v r) = Suc (bheight l)"
5.442 - by (induct l k v r rule: balance.induct) auto
5.443 +lemma is_empty_Mapping [code]:
5.444 + "Mapping.is_empty (Mapping t) \<longleftrightarrow> is_empty t"
5.445 + by (simp add: rbt_eq Mapping.is_empty_empty Mapping_def)
5.446
5.447 -lemma balance_inv2:
5.448 - assumes "inv2 l" "inv2 r" "bheight l = bheight r"
5.449 - shows "inv2 (balance l k v r)"
5.450 - using assms
5.451 - by (induct l k v r rule: balance.induct) auto
5.452 +lemma insert_Mapping [code]:
5.453 + "Mapping.update k v (Mapping t) = Mapping (insert k v t)"
5.454 + by (rule mapping_eqI) simp
5.455
5.456 -lemma balance_tree_greater[simp]: "(v \<guillemotleft>| balance a k x b) = (v \<guillemotleft>| a \<and> v \<guillemotleft>| b \<and> v < k)"
5.457 - by (induct a k x b rule: balance.induct) auto
5.458 +lemma delete_Mapping [code]:
5.459 + "Mapping.delete k (Mapping xs) = Mapping (delete k xs)"
5.460 + by (rule mapping_eqI) simp
5.461
5.462 -lemma balance_tree_less[simp]: "(balance a k x b |\<guillemotleft> v) = (a |\<guillemotleft> v \<and> b |\<guillemotleft> v \<and> k < v)"
5.463 - by (induct a k x b rule: balance.induct) auto
5.464 +lemma keys_Mapping [code]:
5.465 + "Mapping.keys (Mapping t) = set (keys t)"
5.466 + by (simp add: keys_def Mapping_def Mapping.keys_def lookup_def lookup_keys)
5.467
5.468 -lemma balance_sorted:
5.469 - fixes k :: "'a::linorder"
5.470 - assumes "sorted l" "sorted r" "l |\<guillemotleft> k" "k \<guillemotleft>| r"
5.471 - shows "sorted (balance l k v r)"
5.472 -using assms proof (induct l k v r rule: balance.induct)
5.473 - case ("2_2" a x w b y t c z s va vb vd vc)
5.474 - hence "y < z \<and> z \<guillemotleft>| Branch B va vb vd vc"
5.475 - by (auto simp add: tree_ord_props)
5.476 - hence "tree_greater y (Branch B va vb vd vc)" by (blast dest: tree_greater_trans)
5.477 - with "2_2" show ?case by simp
5.478 -next
5.479 - case ("3_2" va vb vd vc x w b y s c z)
5.480 - from "3_2" have "x < y \<and> tree_less x (Branch B va vb vd vc)"
5.481 - by simp
5.482 - hence "tree_less y (Branch B va vb vd vc)" by (blast dest: tree_less_trans)
5.483 - with "3_2" show ?case by simp
5.484 -next
5.485 - case ("3_3" x w b y s c z t va vb vd vc)
5.486 - from "3_3" have "y < z \<and> tree_greater z (Branch B va vb vd vc)" by simp
5.487 - hence "tree_greater y (Branch B va vb vd vc)" by (blast dest: tree_greater_trans)
5.488 - with "3_3" show ?case by simp
5.489 -next
5.490 - case ("3_4" vd ve vg vf x w b y s c z t va vb vii vc)
5.491 - hence "x < y \<and> tree_less x (Branch B vd ve vg vf)" by simp
5.492 - hence 1: "tree_less y (Branch B vd ve vg vf)" by (blast dest: tree_less_trans)
5.493 - from "3_4" have "y < z \<and> tree_greater z (Branch B va vb vii vc)" by simp
5.494 - hence "tree_greater y (Branch B va vb vii vc)" by (blast dest: tree_greater_trans)
5.495 - with 1 "3_4" show ?case by simp
5.496 -next
5.497 - case ("4_2" va vb vd vc x w b y s c z t dd)
5.498 - hence "x < y \<and> tree_less x (Branch B va vb vd vc)" by simp
5.499 - hence "tree_less y (Branch B va vb vd vc)" by (blast dest: tree_less_trans)
5.500 - with "4_2" show ?case by simp
5.501 -next
5.502 - case ("5_2" x w b y s c z t va vb vd vc)
5.503 - hence "y < z \<and> tree_greater z (Branch B va vb vd vc)" by simp
5.504 - hence "tree_greater y (Branch B va vb vd vc)" by (blast dest: tree_greater_trans)
5.505 - with "5_2" show ?case by simp
5.506 -next
5.507 - case ("5_3" va vb vd vc x w b y s c z t)
5.508 - hence "x < y \<and> tree_less x (Branch B va vb vd vc)" by simp
5.509 - hence "tree_less y (Branch B va vb vd vc)" by (blast dest: tree_less_trans)
5.510 - with "5_3" show ?case by simp
5.511 -next
5.512 - case ("5_4" va vb vg vc x w b y s c z t vd ve vii vf)
5.513 - hence "x < y \<and> tree_less x (Branch B va vb vg vc)" by simp
5.514 - hence 1: "tree_less y (Branch B va vb vg vc)" by (blast dest: tree_less_trans)
5.515 - from "5_4" have "y < z \<and> tree_greater z (Branch B vd ve vii vf)" by simp
5.516 - hence "tree_greater y (Branch B vd ve vii vf)" by (blast dest: tree_greater_trans)
5.517 - with 1 "5_4" show ?case by simp
5.518 -qed simp+
5.519 +lemma ordered_keys_Mapping [code]:
5.520 + "Mapping.ordered_keys (Mapping t) = keys t"
5.521 + by (rule sorted_distinct_set_unique) (simp_all add: ordered_keys_def keys_Mapping)
5.522
5.523 -lemma entries_balance [simp]:
5.524 - "entries (balance l k v r) = entries l @ (k, v) # entries r"
5.525 - by (induct l k v r rule: balance.induct) auto
5.526 +lemma Mapping_size_card_keys: (*FIXME*)
5.527 + "Mapping.size m = card (Mapping.keys m)"
5.528 + by (simp add: Mapping.size_def Mapping.keys_def)
5.529
5.530 -lemma keys_balance [simp]:
5.531 - "keys (balance l k v r) = keys l @ k # keys r"
5.532 - by (simp add: keys_def)
5.533 +lemma size_Mapping [code]:
5.534 + "Mapping.size (Mapping t) = length (keys t)"
5.535 + by (simp add: Mapping_size_card_keys keys_Mapping distinct_card)
5.536
5.537 -lemma balance_in_tree:
5.538 - "entry_in_tree k x (balance l v y r) \<longleftrightarrow> entry_in_tree k x l \<or> k = v \<and> x = y \<or> entry_in_tree k x r"
5.539 - by (auto simp add: keys_def)
5.540 +lemma tabulate_Mapping [code]:
5.541 + "Mapping.tabulate ks f = Mapping (bulkload (List.map (\<lambda>k. (k, f k)) ks))"
5.542 + by (rule mapping_eqI) (simp add: map_of_map_restrict)
5.543
5.544 -lemma lookup_balance[simp]:
5.545 -fixes k :: "'a::linorder"
5.546 -assumes "sorted l" "sorted r" "l |\<guillemotleft> k" "k \<guillemotleft>| r"
5.547 -shows "lookup (balance l k v r) x = lookup (Branch B l k v r) x"
5.548 -by (rule lookup_from_in_tree) (auto simp:assms balance_in_tree balance_sorted)
5.549 +lemma bulkload_Mapping [code]:
5.550 + "Mapping.bulkload vs = Mapping (bulkload (List.map (\<lambda>n. (n, vs ! n)) [0..<length vs]))"
5.551 + by (rule mapping_eqI) (simp add: map_of_map_restrict expand_fun_eq)
5.552
5.553 -primrec paint :: "color \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"
5.554 -where
5.555 - "paint c Empty = Empty"
5.556 -| "paint c (Branch _ l k v r) = Branch c l k v r"
5.557 +lemma [code, code del]: "HOL.eq (x :: (_, _) mapping) y \<longleftrightarrow> x = y" by (fact eq_equals) (*FIXME*)
5.558
5.559 -lemma paint_inv1l[simp]: "inv1l t \<Longrightarrow> inv1l (paint c t)" by (cases t) auto
5.560 -lemma paint_inv1[simp]: "inv1l t \<Longrightarrow> inv1 (paint B t)" by (cases t) auto
5.561 -lemma paint_inv2[simp]: "inv2 t \<Longrightarrow> inv2 (paint c t)" by (cases t) auto
5.562 -lemma paint_color_of[simp]: "color_of (paint B t) = B" by (cases t) auto
5.563 -lemma paint_sorted[simp]: "sorted t \<Longrightarrow> sorted (paint c t)" by (cases t) auto
5.564 -lemma paint_in_tree[simp]: "entry_in_tree k x (paint c t) = entry_in_tree k x t" by (cases t) auto
5.565 -lemma paint_lookup[simp]: "lookup (paint c t) = lookup t" by (rule ext) (cases t, auto)
5.566 -lemma paint_tree_greater[simp]: "(v \<guillemotleft>| paint c t) = (v \<guillemotleft>| t)" by (cases t) auto
5.567 -lemma paint_tree_less[simp]: "(paint c t |\<guillemotleft> v) = (t |\<guillemotleft> v)" by (cases t) auto
5.568 +lemma eq_Mapping [code]:
5.569 + "HOL.eq (Mapping t1) (Mapping t2) \<longleftrightarrow> entries t1 = entries t2"
5.570 + by (simp add: eq Mapping_def entries_lookup)
5.571
5.572 -fun
5.573 - ins :: "('a\<Colon>linorder \<Rightarrow> 'b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"
5.574 -where
5.575 - "ins f k v Empty = Branch R Empty k v Empty" |
5.576 - "ins f k v (Branch B l x y r) = (if k < x then balance (ins f k v l) x y r
5.577 - else if k > x then balance l x y (ins f k v r)
5.578 - else Branch B l x (f k y v) r)" |
5.579 - "ins f k v (Branch R l x y r) = (if k < x then Branch R (ins f k v l) x y r
5.580 - else if k > x then Branch R l x y (ins f k v r)
5.581 - else Branch R l x (f k y v) r)"
5.582 -
5.583 -lemma ins_inv1_inv2:
5.584 - assumes "inv1 t" "inv2 t"
5.585 - shows "inv2 (ins f k x t)" "bheight (ins f k x t) = bheight t"
5.586 - "color_of t = B \<Longrightarrow> inv1 (ins f k x t)" "inv1l (ins f k x t)"
5.587 - using assms
5.588 - by (induct f k x t rule: ins.induct) (auto simp: balance_inv1 balance_inv2 balance_bheight)
5.589 -
5.590 -lemma ins_tree_greater[simp]: "(v \<guillemotleft>| ins f k x t) = (v \<guillemotleft>| t \<and> k > v)"
5.591 - by (induct f k x t rule: ins.induct) auto
5.592 -lemma ins_tree_less[simp]: "(ins f k x t |\<guillemotleft> v) = (t |\<guillemotleft> v \<and> k < v)"
5.593 - by (induct f k x t rule: ins.induct) auto
5.594 -lemma ins_sorted[simp]: "sorted t \<Longrightarrow> sorted (ins f k x t)"
5.595 - by (induct f k x t rule: ins.induct) (auto simp: balance_sorted)
5.596 -
5.597 -lemma keys_ins: "set (keys (ins f k v t)) = { k } \<union> set (keys t)"
5.598 - by (induct f k v t rule: ins.induct) auto
5.599 -
5.600 -lemma lookup_ins:
5.601 - fixes k :: "'a::linorder"
5.602 - assumes "sorted t"
5.603 - shows "lookup (ins f k v t) x = ((lookup t)(k |-> case lookup t k of None \<Rightarrow> v
5.604 - | Some w \<Rightarrow> f k w v)) x"
5.605 -using assms by (induct f k v t rule: ins.induct) auto
5.606 -
5.607 -definition
5.608 - insert_with_key :: "('a\<Colon>linorder \<Rightarrow> 'b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"
5.609 -where
5.610 - "insert_with_key f k v t = paint B (ins f k v t)"
5.611 -
5.612 -lemma insertwk_sorted: "sorted t \<Longrightarrow> sorted (insert_with_key f k x t)"
5.613 - by (auto simp: insert_with_key_def)
5.614 -
5.615 -theorem insertwk_is_rbt:
5.616 - assumes inv: "is_rbt t"
5.617 - shows "is_rbt (insert_with_key f k x t)"
5.618 -using assms
5.619 -unfolding insert_with_key_def is_rbt_def
5.620 -by (auto simp: ins_inv1_inv2)
5.621 -
5.622 -lemma lookup_insertwk:
5.623 - assumes "sorted t"
5.624 - shows "lookup (insert_with_key f k v t) x = ((lookup t)(k |-> case lookup t k of None \<Rightarrow> v
5.625 - | Some w \<Rightarrow> f k w v)) x"
5.626 -unfolding insert_with_key_def using assms
5.627 -by (simp add:lookup_ins)
5.628 -
5.629 -definition
5.630 - insertw_def: "insert_with f = insert_with_key (\<lambda>_. f)"
5.631 -
5.632 -lemma insertw_sorted: "sorted t \<Longrightarrow> sorted (insert_with f k v t)" by (simp add: insertwk_sorted insertw_def)
5.633 -theorem insertw_is_rbt: "is_rbt t \<Longrightarrow> is_rbt (insert_with f k v t)" by (simp add: insertwk_is_rbt insertw_def)
5.634 -
5.635 -lemma lookup_insertw:
5.636 - assumes "is_rbt t"
5.637 - shows "lookup (insert_with f k v t) = (lookup t)(k \<mapsto> (if k:dom (lookup t) then f (the (lookup t k)) v else v))"
5.638 -using assms
5.639 -unfolding insertw_def
5.640 -by (rule_tac ext) (cases "lookup t k", auto simp:lookup_insertwk dom_def)
5.641 -
5.642 -definition insert :: "'a\<Colon>linorder \<Rightarrow> 'b \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt" where
5.643 - "insert = insert_with_key (\<lambda>_ _ nv. nv)"
5.644 -
5.645 -lemma insert_sorted: "sorted t \<Longrightarrow> sorted (insert k v t)" by (simp add: insertwk_sorted insert_def)
5.646 -theorem insert_is_rbt [simp]: "is_rbt t \<Longrightarrow> is_rbt (insert k v t)" by (simp add: insertwk_is_rbt insert_def)
5.647 -
5.648 -lemma lookup_insert:
5.649 - assumes "is_rbt t"
5.650 - shows "lookup (insert k v t) = (lookup t)(k\<mapsto>v)"
5.651 -unfolding insert_def
5.652 -using assms
5.653 -by (rule_tac ext) (simp add: lookup_insertwk split:option.split)
5.654 -
5.655 -
5.656 -subsection {* Deletion *}
5.657 -
5.658 -lemma bheight_paintR'[simp]: "color_of t = B \<Longrightarrow> bheight (paint R t) = bheight t - 1"
5.659 -by (cases t rule: rbt_cases) auto
5.660 -
5.661 -fun
5.662 - balance_left :: "('a,'b) rbt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"
5.663 -where
5.664 - "balance_left (Branch R a k x b) s y c = Branch R (Branch B a k x b) s y c" |
5.665 - "balance_left bl k x (Branch B a s y b) = balance bl k x (Branch R a s y b)" |
5.666 - "balance_left bl k x (Branch R (Branch B a s y b) t z c) = Branch R (Branch B bl k x a) s y (balance b t z (paint R c))" |
5.667 - "balance_left t k x s = Empty"
5.668 -
5.669 -lemma balance_left_inv2_with_inv1:
5.670 - assumes "inv2 lt" "inv2 rt" "bheight lt + 1 = bheight rt" "inv1 rt"
5.671 - shows "bheight (balance_left lt k v rt) = bheight lt + 1"
5.672 - and "inv2 (balance_left lt k v rt)"
5.673 -using assms
5.674 -by (induct lt k v rt rule: balance_left.induct) (auto simp: balance_inv2 balance_bheight)
5.675 -
5.676 -lemma balance_left_inv2_app:
5.677 - assumes "inv2 lt" "inv2 rt" "bheight lt + 1 = bheight rt" "color_of rt = B"
5.678 - shows "inv2 (balance_left lt k v rt)"
5.679 - "bheight (balance_left lt k v rt) = bheight rt"
5.680 -using assms
5.681 -by (induct lt k v rt rule: balance_left.induct) (auto simp add: balance_inv2 balance_bheight)+
5.682 -
5.683 -lemma balance_left_inv1: "\<lbrakk>inv1l a; inv1 b; color_of b = B\<rbrakk> \<Longrightarrow> inv1 (balance_left a k x b)"
5.684 - by (induct a k x b rule: balance_left.induct) (simp add: balance_inv1)+
5.685 -
5.686 -lemma balance_left_inv1l: "\<lbrakk> inv1l lt; inv1 rt \<rbrakk> \<Longrightarrow> inv1l (balance_left lt k x rt)"
5.687 -by (induct lt k x rt rule: balance_left.induct) (auto simp: balance_inv1)
5.688 -
5.689 -lemma balance_left_sorted: "\<lbrakk> sorted l; sorted r; tree_less k l; tree_greater k r \<rbrakk> \<Longrightarrow> sorted (balance_left l k v r)"
5.690 -apply (induct l k v r rule: balance_left.induct)
5.691 -apply (auto simp: balance_sorted)
5.692 -apply (unfold tree_greater_prop tree_less_prop)
5.693 -by force+
5.694 -
5.695 -lemma balance_left_tree_greater:
5.696 - fixes k :: "'a::order"
5.697 - assumes "k \<guillemotleft>| a" "k \<guillemotleft>| b" "k < x"
5.698 - shows "k \<guillemotleft>| balance_left a x t b"
5.699 -using assms
5.700 -by (induct a x t b rule: balance_left.induct) auto
5.701 -
5.702 -lemma balance_left_tree_less:
5.703 - fixes k :: "'a::order"
5.704 - assumes "a |\<guillemotleft> k" "b |\<guillemotleft> k" "x < k"
5.705 - shows "balance_left a x t b |\<guillemotleft> k"
5.706 -using assms
5.707 -by (induct a x t b rule: balance_left.induct) auto
5.708 -
5.709 -lemma balance_left_in_tree:
5.710 - assumes "inv1l l" "inv1 r" "bheight l + 1 = bheight r"
5.711 - shows "entry_in_tree k v (balance_left l a b r) = (entry_in_tree k v l \<or> k = a \<and> v = b \<or> entry_in_tree k v r)"
5.712 -using assms
5.713 -by (induct l k v r rule: balance_left.induct) (auto simp: balance_in_tree)
5.714 -
5.715 -fun
5.716 - balance_right :: "('a,'b) rbt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"
5.717 -where
5.718 - "balance_right a k x (Branch R b s y c) = Branch R a k x (Branch B b s y c)" |
5.719 - "balance_right (Branch B a k x b) s y bl = balance (Branch R a k x b) s y bl" |
5.720 - "balance_right (Branch R a k x (Branch B b s y c)) t z bl = Branch R (balance (paint R a) k x b) s y (Branch B c t z bl)" |
5.721 - "balance_right t k x s = Empty"
5.722 -
5.723 -lemma balance_right_inv2_with_inv1:
5.724 - assumes "inv2 lt" "inv2 rt" "bheight lt = bheight rt + 1" "inv1 lt"
5.725 - shows "inv2 (balance_right lt k v rt) \<and> bheight (balance_right lt k v rt) = bheight lt"
5.726 -using assms
5.727 -by (induct lt k v rt rule: balance_right.induct) (auto simp: balance_inv2 balance_bheight)
5.728 -
5.729 -lemma balance_right_inv1: "\<lbrakk>inv1 a; inv1l b; color_of a = B\<rbrakk> \<Longrightarrow> inv1 (balance_right a k x b)"
5.730 -by (induct a k x b rule: balance_right.induct) (simp add: balance_inv1)+
5.731 -
5.732 -lemma balance_right_inv1l: "\<lbrakk> inv1 lt; inv1l rt \<rbrakk> \<Longrightarrow>inv1l (balance_right lt k x rt)"
5.733 -by (induct lt k x rt rule: balance_right.induct) (auto simp: balance_inv1)
5.734 -
5.735 -lemma balance_right_sorted: "\<lbrakk> sorted l; sorted r; tree_less k l; tree_greater k r \<rbrakk> \<Longrightarrow> sorted (balance_right l k v r)"
5.736 -apply (induct l k v r rule: balance_right.induct)
5.737 -apply (auto simp:balance_sorted)
5.738 -apply (unfold tree_less_prop tree_greater_prop)
5.739 -by force+
5.740 -
5.741 -lemma balance_right_tree_greater:
5.742 - fixes k :: "'a::order"
5.743 - assumes "k \<guillemotleft>| a" "k \<guillemotleft>| b" "k < x"
5.744 - shows "k \<guillemotleft>| balance_right a x t b"
5.745 -using assms by (induct a x t b rule: balance_right.induct) auto
5.746 -
5.747 -lemma balance_right_tree_less:
5.748 - fixes k :: "'a::order"
5.749 - assumes "a |\<guillemotleft> k" "b |\<guillemotleft> k" "x < k"
5.750 - shows "balance_right a x t b |\<guillemotleft> k"
5.751 -using assms by (induct a x t b rule: balance_right.induct) auto
5.752 -
5.753 -lemma balance_right_in_tree:
5.754 - assumes "inv1 l" "inv1l r" "bheight l = bheight r + 1" "inv2 l" "inv2 r"
5.755 - shows "entry_in_tree x y (balance_right l k v r) = (entry_in_tree x y l \<or> x = k \<and> y = v \<or> entry_in_tree x y r)"
5.756 -using assms by (induct l k v r rule: balance_right.induct) (auto simp: balance_in_tree)
5.757 -
5.758 -fun
5.759 - combine :: "('a,'b) rbt \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"
5.760 -where
5.761 - "combine Empty x = x"
5.762 -| "combine x Empty = x"
5.763 -| "combine (Branch R a k x b) (Branch R c s y d) = (case (combine b c) of
5.764 - Branch R b2 t z c2 \<Rightarrow> (Branch R (Branch R a k x b2) t z (Branch R c2 s y d)) |
5.765 - bc \<Rightarrow> Branch R a k x (Branch R bc s y d))"
5.766 -| "combine (Branch B a k x b) (Branch B c s y d) = (case (combine b c) of
5.767 - Branch R b2 t z c2 \<Rightarrow> Branch R (Branch B a k x b2) t z (Branch B c2 s y d) |
5.768 - bc \<Rightarrow> balance_left a k x (Branch B bc s y d))"
5.769 -| "combine a (Branch R b k x c) = Branch R (combine a b) k x c"
5.770 -| "combine (Branch R a k x b) c = Branch R a k x (combine b c)"
5.771 -
5.772 -lemma combine_inv2:
5.773 - assumes "inv2 lt" "inv2 rt" "bheight lt = bheight rt"
5.774 - shows "bheight (combine lt rt) = bheight lt" "inv2 (combine lt rt)"
5.775 -using assms
5.776 -by (induct lt rt rule: combine.induct)
5.777 - (auto simp: balance_left_inv2_app split: rbt.splits color.splits)
5.778 -
5.779 -lemma combine_inv1:
5.780 - assumes "inv1 lt" "inv1 rt"
5.781 - shows "color_of lt = B \<Longrightarrow> color_of rt = B \<Longrightarrow> inv1 (combine lt rt)"
5.782 - "inv1l (combine lt rt)"
5.783 -using assms
5.784 -by (induct lt rt rule: combine.induct)
5.785 - (auto simp: balance_left_inv1 split: rbt.splits color.splits)
5.786 -
5.787 -lemma combine_tree_greater[simp]:
5.788 - fixes k :: "'a::linorder"
5.789 - assumes "k \<guillemotleft>| l" "k \<guillemotleft>| r"
5.790 - shows "k \<guillemotleft>| combine l r"
5.791 -using assms
5.792 -by (induct l r rule: combine.induct)
5.793 - (auto simp: balance_left_tree_greater split:rbt.splits color.splits)
5.794 -
5.795 -lemma combine_tree_less[simp]:
5.796 - fixes k :: "'a::linorder"
5.797 - assumes "l |\<guillemotleft> k" "r |\<guillemotleft> k"
5.798 - shows "combine l r |\<guillemotleft> k"
5.799 -using assms
5.800 -by (induct l r rule: combine.induct)
5.801 - (auto simp: balance_left_tree_less split:rbt.splits color.splits)
5.802 -
5.803 -lemma combine_sorted:
5.804 - fixes k :: "'a::linorder"
5.805 - assumes "sorted l" "sorted r" "l |\<guillemotleft> k" "k \<guillemotleft>| r"
5.806 - shows "sorted (combine l r)"
5.807 -using assms proof (induct l r rule: combine.induct)
5.808 - case (3 a x v b c y w d)
5.809 - hence ineqs: "a |\<guillemotleft> x" "x \<guillemotleft>| b" "b |\<guillemotleft> k" "k \<guillemotleft>| c" "c |\<guillemotleft> y" "y \<guillemotleft>| d"
5.810 - by auto
5.811 - with 3
5.812 - show ?case
5.813 - by (cases "combine b c" rule: rbt_cases)
5.814 - (auto, (metis combine_tree_greater combine_tree_less ineqs ineqs tree_less_simps(2) tree_greater_simps(2) tree_greater_trans tree_less_trans)+)
5.815 -next
5.816 - case (4 a x v b c y w d)
5.817 - hence "x < k \<and> tree_greater k c" by simp
5.818 - hence "tree_greater x c" by (blast dest: tree_greater_trans)
5.819 - with 4 have 2: "tree_greater x (combine b c)" by (simp add: combine_tree_greater)
5.820 - from 4 have "k < y \<and> tree_less k b" by simp
5.821 - hence "tree_less y b" by (blast dest: tree_less_trans)
5.822 - with 4 have 3: "tree_less y (combine b c)" by (simp add: combine_tree_less)
5.823 - show ?case
5.824 - proof (cases "combine b c" rule: rbt_cases)
5.825 - case Empty
5.826 - from 4 have "x < y \<and> tree_greater y d" by auto
5.827 - hence "tree_greater x d" by (blast dest: tree_greater_trans)
5.828 - with 4 Empty have "sorted a" and "sorted (Branch B Empty y w d)" and "tree_less x a" and "tree_greater x (Branch B Empty y w d)" by auto
5.829 - with Empty show ?thesis by (simp add: balance_left_sorted)
5.830 - next
5.831 - case (Red lta va ka rta)
5.832 - with 2 4 have "x < va \<and> tree_less x a" by simp
5.833 - hence 5: "tree_less va a" by (blast dest: tree_less_trans)
5.834 - from Red 3 4 have "va < y \<and> tree_greater y d" by simp
5.835 - hence "tree_greater va d" by (blast dest: tree_greater_trans)
5.836 - with Red 2 3 4 5 show ?thesis by simp
5.837 - next
5.838 - case (Black lta va ka rta)
5.839 - from 4 have "x < y \<and> tree_greater y d" by auto
5.840 - hence "tree_greater x d" by (blast dest: tree_greater_trans)
5.841 - with Black 2 3 4 have "sorted a" and "sorted (Branch B (combine b c) y w d)" and "tree_less x a" and "tree_greater x (Branch B (combine b c) y w d)" by auto
5.842 - with Black show ?thesis by (simp add: balance_left_sorted)
5.843 - qed
5.844 -next
5.845 - case (5 va vb vd vc b x w c)
5.846 - hence "k < x \<and> tree_less k (Branch B va vb vd vc)" by simp
5.847 - hence "tree_less x (Branch B va vb vd vc)" by (blast dest: tree_less_trans)
5.848 - with 5 show ?case by (simp add: combine_tree_less)
5.849 -next
5.850 - case (6 a x v b va vb vd vc)
5.851 - hence "x < k \<and> tree_greater k (Branch B va vb vd vc)" by simp
5.852 - hence "tree_greater x (Branch B va vb vd vc)" by (blast dest: tree_greater_trans)
5.853 - with 6 show ?case by (simp add: combine_tree_greater)
5.854 -qed simp+
5.855 -
5.856 -lemma combine_in_tree:
5.857 - assumes "inv2 l" "inv2 r" "bheight l = bheight r" "inv1 l" "inv1 r"
5.858 - shows "entry_in_tree k v (combine l r) = (entry_in_tree k v l \<or> entry_in_tree k v r)"
5.859 -using assms
5.860 -proof (induct l r rule: combine.induct)
5.861 - case (4 _ _ _ b c)
5.862 - hence a: "bheight (combine b c) = bheight b" by (simp add: combine_inv2)
5.863 - from 4 have b: "inv1l (combine b c)" by (simp add: combine_inv1)
5.864 -
5.865 - show ?case
5.866 - proof (cases "combine b c" rule: rbt_cases)
5.867 - case Empty
5.868 - with 4 a show ?thesis by (auto simp: balance_left_in_tree)
5.869 - next
5.870 - case (Red lta ka va rta)
5.871 - with 4 show ?thesis by auto
5.872 - next
5.873 - case (Black lta ka va rta)
5.874 - with a b 4 show ?thesis by (auto simp: balance_left_in_tree)
5.875 - qed
5.876 -qed (auto split: rbt.splits color.splits)
5.877 -
5.878 -fun
5.879 - del_from_left :: "('a\<Colon>linorder) \<Rightarrow> ('a,'b) rbt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt" and
5.880 - del_from_right :: "('a\<Colon>linorder) \<Rightarrow> ('a,'b) rbt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt" and
5.881 - del :: "('a\<Colon>linorder) \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"
5.882 -where
5.883 - "del x Empty = Empty" |
5.884 - "del x (Branch c a y s b) = (if x < y then del_from_left x a y s b else (if x > y then del_from_right x a y s b else combine a b))" |
5.885 - "del_from_left x (Branch B lt z v rt) y s b = balance_left (del x (Branch B lt z v rt)) y s b" |
5.886 - "del_from_left x a y s b = Branch R (del x a) y s b" |
5.887 - "del_from_right x a y s (Branch B lt z v rt) = balance_right a y s (del x (Branch B lt z v rt))" |
5.888 - "del_from_right x a y s b = Branch R a y s (del x b)"
5.889 -
5.890 -lemma
5.891 - assumes "inv2 lt" "inv1 lt"
5.892 - shows
5.893 - "\<lbrakk>inv2 rt; bheight lt = bheight rt; inv1 rt\<rbrakk> \<Longrightarrow>
5.894 - inv2 (del_from_left x lt k v rt) \<and> bheight (del_from_left x lt k v rt) = bheight lt \<and> (color_of lt = B \<and> color_of rt = B \<and> inv1 (del_from_left x lt k v rt) \<or> (color_of lt \<noteq> B \<or> color_of rt \<noteq> B) \<and> inv1l (del_from_left x lt k v rt))"
5.895 - and "\<lbrakk>inv2 rt; bheight lt = bheight rt; inv1 rt\<rbrakk> \<Longrightarrow>
5.896 - inv2 (del_from_right x lt k v rt) \<and> bheight (del_from_right x lt k v rt) = bheight lt \<and> (color_of lt = B \<and> color_of rt = B \<and> inv1 (del_from_right x lt k v rt) \<or> (color_of lt \<noteq> B \<or> color_of rt \<noteq> B) \<and> inv1l (del_from_right x lt k v rt))"
5.897 - and del_inv1_inv2: "inv2 (del x lt) \<and> (color_of lt = R \<and> bheight (del x lt) = bheight lt \<and> inv1 (del x lt)
5.898 - \<or> color_of lt = B \<and> bheight (del x lt) = bheight lt - 1 \<and> inv1l (del x lt))"
5.899 -using assms
5.900 -proof (induct x lt k v rt and x lt k v rt and x lt rule: del_from_left_del_from_right_del.induct)
5.901 -case (2 y c _ y')
5.902 - have "y = y' \<or> y < y' \<or> y > y'" by auto
5.903 - thus ?case proof (elim disjE)
5.904 - assume "y = y'"
5.905 - with 2 show ?thesis by (cases c) (simp add: combine_inv2 combine_inv1)+
5.906 - next
5.907 - assume "y < y'"
5.908 - with 2 show ?thesis by (cases c) auto
5.909 - next
5.910 - assume "y' < y"
5.911 - with 2 show ?thesis by (cases c) auto
5.912 - qed
5.913 -next
5.914 - case (3 y lt z v rta y' ss bb)
5.915 - thus ?case by (cases "color_of (Branch B lt z v rta) = B \<and> color_of bb = B") (simp add: balance_left_inv2_with_inv1 balance_left_inv1 balance_left_inv1l)+
5.916 -next
5.917 - case (5 y a y' ss lt z v rta)
5.918 - thus ?case by (cases "color_of a = B \<and> color_of (Branch B lt z v rta) = B") (simp add: balance_right_inv2_with_inv1 balance_right_inv1 balance_right_inv1l)+
5.919 -next
5.920 - case ("6_1" y a y' ss) thus ?case by (cases "color_of a = B \<and> color_of Empty = B") simp+
5.921 -qed auto
5.922 -
5.923 -lemma
5.924 - del_from_left_tree_less: "\<lbrakk>tree_less v lt; tree_less v rt; k < v\<rbrakk> \<Longrightarrow> tree_less v (del_from_left x lt k y rt)"
5.925 - and del_from_right_tree_less: "\<lbrakk>tree_less v lt; tree_less v rt; k < v\<rbrakk> \<Longrightarrow> tree_less v (del_from_right x lt k y rt)"
5.926 - and del_tree_less: "tree_less v lt \<Longrightarrow> tree_less v (del x lt)"
5.927 -by (induct x lt k y rt and x lt k y rt and x lt rule: del_from_left_del_from_right_del.induct)
5.928 - (auto simp: balance_left_tree_less balance_right_tree_less)
5.929 -
5.930 -lemma del_from_left_tree_greater: "\<lbrakk>tree_greater v lt; tree_greater v rt; k > v\<rbrakk> \<Longrightarrow> tree_greater v (del_from_left x lt k y rt)"
5.931 - and del_from_right_tree_greater: "\<lbrakk>tree_greater v lt; tree_greater v rt; k > v\<rbrakk> \<Longrightarrow> tree_greater v (del_from_right x lt k y rt)"
5.932 - and del_tree_greater: "tree_greater v lt \<Longrightarrow> tree_greater v (del x lt)"
5.933 -by (induct x lt k y rt and x lt k y rt and x lt rule: del_from_left_del_from_right_del.induct)
5.934 - (auto simp: balance_left_tree_greater balance_right_tree_greater)
5.935 -
5.936 -lemma "\<lbrakk>sorted lt; sorted rt; tree_less k lt; tree_greater k rt\<rbrakk> \<Longrightarrow> sorted (del_from_left x lt k y rt)"
5.937 - and "\<lbrakk>sorted lt; sorted rt; tree_less k lt; tree_greater k rt\<rbrakk> \<Longrightarrow> sorted (del_from_right x lt k y rt)"
5.938 - and del_sorted: "sorted lt \<Longrightarrow> sorted (del x lt)"
5.939 -proof (induct x lt k y rt and x lt k y rt and x lt rule: del_from_left_del_from_right_del.induct)
5.940 - case (3 x lta zz v rta yy ss bb)
5.941 - from 3 have "tree_less yy (Branch B lta zz v rta)" by simp
5.942 - hence "tree_less yy (del x (Branch B lta zz v rta))" by (rule del_tree_less)
5.943 - with 3 show ?case by (simp add: balance_left_sorted)
5.944 -next
5.945 - case ("4_2" x vaa vbb vdd vc yy ss bb)
5.946 - hence "tree_less yy (Branch R vaa vbb vdd vc)" by simp
5.947 - hence "tree_less yy (del x (Branch R vaa vbb vdd vc))" by (rule del_tree_less)
5.948 - with "4_2" show ?case by simp
5.949 -next
5.950 - case (5 x aa yy ss lta zz v rta)
5.951 - hence "tree_greater yy (Branch B lta zz v rta)" by simp
5.952 - hence "tree_greater yy (del x (Branch B lta zz v rta))" by (rule del_tree_greater)
5.953 - with 5 show ?case by (simp add: balance_right_sorted)
5.954 -next
5.955 - case ("6_2" x aa yy ss vaa vbb vdd vc)
5.956 - hence "tree_greater yy (Branch R vaa vbb vdd vc)" by simp
5.957 - hence "tree_greater yy (del x (Branch R vaa vbb vdd vc))" by (rule del_tree_greater)
5.958 - with "6_2" show ?case by simp
5.959 -qed (auto simp: combine_sorted)
5.960 -
5.961 -lemma "\<lbrakk>sorted lt; sorted rt; tree_less kt lt; tree_greater kt rt; inv1 lt; inv1 rt; inv2 lt; inv2 rt; bheight lt = bheight rt; x < kt\<rbrakk> \<Longrightarrow> entry_in_tree k v (del_from_left x lt kt y rt) = (False \<or> (x \<noteq> k \<and> entry_in_tree k v (Branch c lt kt y rt)))"
5.962 - and "\<lbrakk>sorted lt; sorted rt; tree_less kt lt; tree_greater kt rt; inv1 lt; inv1 rt; inv2 lt; inv2 rt; bheight lt = bheight rt; x > kt\<rbrakk> \<Longrightarrow> entry_in_tree k v (del_from_right x lt kt y rt) = (False \<or> (x \<noteq> k \<and> entry_in_tree k v (Branch c lt kt y rt)))"
5.963 - and del_in_tree: "\<lbrakk>sorted t; inv1 t; inv2 t\<rbrakk> \<Longrightarrow> entry_in_tree k v (del x t) = (False \<or> (x \<noteq> k \<and> entry_in_tree k v t))"
5.964 -proof (induct x lt kt y rt and x lt kt y rt and x t rule: del_from_left_del_from_right_del.induct)
5.965 - case (2 xx c aa yy ss bb)
5.966 - have "xx = yy \<or> xx < yy \<or> xx > yy" by auto
5.967 - from this 2 show ?case proof (elim disjE)
5.968 - assume "xx = yy"
5.969 - with 2 show ?thesis proof (cases "xx = k")
5.970 - case True
5.971 - from 2 `xx = yy` `xx = k` have "sorted (Branch c aa yy ss bb) \<and> k = yy" by simp
5.972 - hence "\<not> entry_in_tree k v aa" "\<not> entry_in_tree k v bb" by (auto simp: tree_less_nit tree_greater_prop)
5.973 - with `xx = yy` 2 `xx = k` show ?thesis by (simp add: combine_in_tree)
5.974 - qed (simp add: combine_in_tree)
5.975 - qed simp+
5.976 -next
5.977 - case (3 xx lta zz vv rta yy ss bb)
5.978 - def mt[simp]: mt == "Branch B lta zz vv rta"
5.979 - from 3 have "inv2 mt \<and> inv1 mt" by simp
5.980 - hence "inv2 (del xx mt) \<and> (color_of mt = R \<and> bheight (del xx mt) = bheight mt \<and> inv1 (del xx mt) \<or> color_of mt = B \<and> bheight (del xx mt) = bheight mt - 1 \<and> inv1l (del xx mt))" by (blast dest: del_inv1_inv2)
5.981 - with 3 have 4: "entry_in_tree k v (del_from_left xx mt yy ss bb) = (False \<or> xx \<noteq> k \<and> entry_in_tree k v mt \<or> (k = yy \<and> v = ss) \<or> entry_in_tree k v bb)" by (simp add: balance_left_in_tree)
5.982 - thus ?case proof (cases "xx = k")
5.983 - case True
5.984 - from 3 True have "tree_greater yy bb \<and> yy > k" by simp
5.985 - hence "tree_greater k bb" by (blast dest: tree_greater_trans)
5.986 - with 3 4 True show ?thesis by (auto simp: tree_greater_nit)
5.987 - qed auto
5.988 -next
5.989 - case ("4_1" xx yy ss bb)
5.990 - show ?case proof (cases "xx = k")
5.991 - case True
5.992 - with "4_1" have "tree_greater yy bb \<and> k < yy" by simp
5.993 - hence "tree_greater k bb" by (blast dest: tree_greater_trans)
5.994 - with "4_1" `xx = k`
5.995 - have "entry_in_tree k v (Branch R Empty yy ss bb) = entry_in_tree k v Empty" by (auto simp: tree_greater_nit)
5.996 - thus ?thesis by auto
5.997 - qed simp+
5.998 -next
5.999 - case ("4_2" xx vaa vbb vdd vc yy ss bb)
5.1000 - thus ?case proof (cases "xx = k")
5.1001 - case True
5.1002 - with "4_2" have "k < yy \<and> tree_greater yy bb" by simp
5.1003 - hence "tree_greater k bb" by (blast dest: tree_greater_trans)
5.1004 - with True "4_2" show ?thesis by (auto simp: tree_greater_nit)
5.1005 - qed auto
5.1006 -next
5.1007 - case (5 xx aa yy ss lta zz vv rta)
5.1008 - def mt[simp]: mt == "Branch B lta zz vv rta"
5.1009 - from 5 have "inv2 mt \<and> inv1 mt" by simp
5.1010 - hence "inv2 (del xx mt) \<and> (color_of mt = R \<and> bheight (del xx mt) = bheight mt \<and> inv1 (del xx mt) \<or> color_of mt = B \<and> bheight (del xx mt) = bheight mt - 1 \<and> inv1l (del xx mt))" by (blast dest: del_inv1_inv2)
5.1011 - with 5 have 3: "entry_in_tree k v (del_from_right xx aa yy ss mt) = (entry_in_tree k v aa \<or> (k = yy \<and> v = ss) \<or> False \<or> xx \<noteq> k \<and> entry_in_tree k v mt)" by (simp add: balance_right_in_tree)
5.1012 - thus ?case proof (cases "xx = k")
5.1013 - case True
5.1014 - from 5 True have "tree_less yy aa \<and> yy < k" by simp
5.1015 - hence "tree_less k aa" by (blast dest: tree_less_trans)
5.1016 - with 3 5 True show ?thesis by (auto simp: tree_less_nit)
5.1017 - qed auto
5.1018 -next
5.1019 - case ("6_1" xx aa yy ss)
5.1020 - show ?case proof (cases "xx = k")
5.1021 - case True
5.1022 - with "6_1" have "tree_less yy aa \<and> k > yy" by simp
5.1023 - hence "tree_less k aa" by (blast dest: tree_less_trans)
5.1024 - with "6_1" `xx = k` show ?thesis by (auto simp: tree_less_nit)
5.1025 - qed simp
5.1026 -next
5.1027 - case ("6_2" xx aa yy ss vaa vbb vdd vc)
5.1028 - thus ?case proof (cases "xx = k")
5.1029 - case True
5.1030 - with "6_2" have "k > yy \<and> tree_less yy aa" by simp
5.1031 - hence "tree_less k aa" by (blast dest: tree_less_trans)
5.1032 - with True "6_2" show ?thesis by (auto simp: tree_less_nit)
5.1033 - qed auto
5.1034 -qed simp
5.1035 -
5.1036 -
5.1037 -definition delete where
5.1038 - delete_def: "delete k t = paint B (del k t)"
5.1039 -
5.1040 -theorem delete_is_rbt [simp]: assumes "is_rbt t" shows "is_rbt (delete k t)"
5.1041 -proof -
5.1042 - from assms have "inv2 t" and "inv1 t" unfolding is_rbt_def by auto
5.1043 - hence "inv2 (del k t) \<and> (color_of t = R \<and> bheight (del k t) = bheight t \<and> inv1 (del k t) \<or> color_of t = B \<and> bheight (del k t) = bheight t - 1 \<and> inv1l (del k t))" by (rule del_inv1_inv2)
5.1044 - hence "inv2 (del k t) \<and> inv1l (del k t)" by (cases "color_of t") auto
5.1045 - with assms show ?thesis
5.1046 - unfolding is_rbt_def delete_def
5.1047 - by (auto intro: paint_sorted del_sorted)
5.1048 -qed
5.1049 -
5.1050 -lemma delete_in_tree:
5.1051 - assumes "is_rbt t"
5.1052 - shows "entry_in_tree k v (delete x t) = (x \<noteq> k \<and> entry_in_tree k v t)"
5.1053 - using assms unfolding is_rbt_def delete_def
5.1054 - by (auto simp: del_in_tree)
5.1055 -
5.1056 -lemma lookup_delete:
5.1057 - assumes is_rbt: "is_rbt t"
5.1058 - shows "lookup (delete k t) = (lookup t)|`(-{k})"
5.1059 -proof
5.1060 - fix x
5.1061 - show "lookup (delete k t) x = (lookup t |` (-{k})) x"
5.1062 - proof (cases "x = k")
5.1063 - assume "x = k"
5.1064 - with is_rbt show ?thesis
5.1065 - by (cases "lookup (delete k t) k") (auto simp: lookup_in_tree delete_in_tree)
5.1066 - next
5.1067 - assume "x \<noteq> k"
5.1068 - thus ?thesis
5.1069 - by auto (metis is_rbt delete_is_rbt delete_in_tree is_rbt_sorted lookup_from_in_tree)
5.1070 - qed
5.1071 -qed
5.1072 -
5.1073 -
5.1074 -subsection {* Union *}
5.1075 -
5.1076 -primrec
5.1077 - union_with_key :: "('a\<Colon>linorder \<Rightarrow> 'b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"
5.1078 -where
5.1079 - "union_with_key f t Empty = t"
5.1080 -| "union_with_key f t (Branch c lt k v rt) = union_with_key f (union_with_key f (insert_with_key f k v t) lt) rt"
5.1081 -
5.1082 -lemma unionwk_sorted: "sorted lt \<Longrightarrow> sorted (union_with_key f lt rt)"
5.1083 - by (induct rt arbitrary: lt) (auto simp: insertwk_sorted)
5.1084 -theorem unionwk_is_rbt[simp]: "is_rbt lt \<Longrightarrow> is_rbt (union_with_key f lt rt)"
5.1085 - by (induct rt arbitrary: lt) (simp add: insertwk_is_rbt)+
5.1086 -
5.1087 -definition
5.1088 - union_with where
5.1089 - "union_with f = union_with_key (\<lambda>_. f)"
5.1090 -
5.1091 -theorem unionw_is_rbt: "is_rbt lt \<Longrightarrow> is_rbt (union_with f lt rt)" unfolding union_with_def by simp
5.1092 -
5.1093 -definition union where
5.1094 - "union = union_with_key (%_ _ rv. rv)"
5.1095 -
5.1096 -theorem union_is_rbt: "is_rbt lt \<Longrightarrow> is_rbt (union lt rt)" unfolding union_def by simp
5.1097 -
5.1098 -lemma union_Branch[simp]:
5.1099 - "union t (Branch c lt k v rt) = union (union (insert k v t) lt) rt"
5.1100 - unfolding union_def insert_def
5.1101 - by simp
5.1102 -
5.1103 -lemma lookup_union:
5.1104 - assumes "is_rbt s" "sorted t"
5.1105 - shows "lookup (union s t) = lookup s ++ lookup t"
5.1106 -using assms
5.1107 -proof (induct t arbitrary: s)
5.1108 - case Empty thus ?case by (auto simp: union_def)
5.1109 -next
5.1110 - case (Branch c l k v r s)
5.1111 - then have "sorted r" "sorted l" "l |\<guillemotleft> k" "k \<guillemotleft>| r" by auto
5.1112 -
5.1113 - have meq: "lookup s(k \<mapsto> v) ++ lookup l ++ lookup r =
5.1114 - lookup s ++
5.1115 - (\<lambda>a. if a < k then lookup l a
5.1116 - else if k < a then lookup r a else Some v)" (is "?m1 = ?m2")
5.1117 - proof (rule ext)
5.1118 - fix a
5.1119 -
5.1120 - have "k < a \<or> k = a \<or> k > a" by auto
5.1121 - thus "?m1 a = ?m2 a"
5.1122 - proof (elim disjE)
5.1123 - assume "k < a"
5.1124 - with `l |\<guillemotleft> k` have "l |\<guillemotleft> a" by (rule tree_less_trans)
5.1125 - with `k < a` show ?thesis
5.1126 - by (auto simp: map_add_def split: option.splits)
5.1127 - next
5.1128 - assume "k = a"
5.1129 - with `l |\<guillemotleft> k` `k \<guillemotleft>| r`
5.1130 - show ?thesis by (auto simp: map_add_def)
5.1131 - next
5.1132 - assume "a < k"
5.1133 - from this `k \<guillemotleft>| r` have "a \<guillemotleft>| r" by (rule tree_greater_trans)
5.1134 - with `a < k` show ?thesis
5.1135 - by (auto simp: map_add_def split: option.splits)
5.1136 - qed
5.1137 - qed
5.1138 -
5.1139 - from Branch have is_rbt: "is_rbt (RBT.union (RBT.insert k v s) l)"
5.1140 - by (auto intro: union_is_rbt insert_is_rbt)
5.1141 - with Branch have IHs:
5.1142 - "lookup (union (union (insert k v s) l) r) = lookup (union (insert k v s) l) ++ lookup r"
5.1143 - "lookup (union (insert k v s) l) = lookup (insert k v s) ++ lookup l"
5.1144 - by auto
5.1145 -
5.1146 - with meq show ?case
5.1147 - by (auto simp: lookup_insert[OF Branch(3)])
5.1148 -
5.1149 -qed
5.1150 -
5.1151 -
5.1152 -subsection {* Modifying existing entries *}
5.1153 -
5.1154 -primrec
5.1155 - map_entry :: "'a\<Colon>linorder \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt"
5.1156 -where
5.1157 - "map_entry k f Empty = Empty"
5.1158 -| "map_entry k f (Branch c lt x v rt) =
5.1159 - (if k < x then Branch c (map_entry k f lt) x v rt
5.1160 - else if k > x then (Branch c lt x v (map_entry k f rt))
5.1161 - else Branch c lt x (f v) rt)"
5.1162 -
5.1163 -lemma map_entry_color_of: "color_of (map_entry k f t) = color_of t" by (induct t) simp+
5.1164 -lemma map_entry_inv1: "inv1 (map_entry k f t) = inv1 t" by (induct t) (simp add: map_entry_color_of)+
5.1165 -lemma map_entry_inv2: "inv2 (map_entry k f t) = inv2 t" "bheight (map_entry k f t) = bheight t" by (induct t) simp+
5.1166 -lemma map_entry_tree_greater: "tree_greater a (map_entry k f t) = tree_greater a t" by (induct t) simp+
5.1167 -lemma map_entry_tree_less: "tree_less a (map_entry k f t) = tree_less a t" by (induct t) simp+
5.1168 -lemma map_entry_sorted: "sorted (map_entry k f t) = sorted t"
5.1169 - by (induct t) (simp_all add: map_entry_tree_less map_entry_tree_greater)
5.1170 -
5.1171 -theorem map_entry_is_rbt [simp]: "is_rbt (map_entry k f t) = is_rbt t"
5.1172 -unfolding is_rbt_def by (simp add: map_entry_inv2 map_entry_color_of map_entry_sorted map_entry_inv1 )
5.1173 -
5.1174 -theorem lookup_map_entry:
5.1175 - "lookup (map_entry k f t) = (lookup t)(k := Option.map f (lookup t k))"
5.1176 - by (induct t) (auto split: option.splits simp add: expand_fun_eq)
5.1177 -
5.1178 -
5.1179 -subsection {* Mapping all entries *}
5.1180 -
5.1181 -primrec
5.1182 - map :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'c) rbt"
5.1183 -where
5.1184 - "map f Empty = Empty"
5.1185 -| "map f (Branch c lt k v rt) = Branch c (map f lt) k (f k v) (map f rt)"
5.1186 -
5.1187 -lemma map_entries [simp]: "entries (map f t) = List.map (\<lambda>(k, v). (k, f k v)) (entries t)"
5.1188 - by (induct t) auto
5.1189 -lemma map_keys [simp]: "keys (map f t) = keys t" by (simp add: keys_def split_def)
5.1190 -lemma map_tree_greater: "tree_greater k (map f t) = tree_greater k t" by (induct t) simp+
5.1191 -lemma map_tree_less: "tree_less k (map f t) = tree_less k t" by (induct t) simp+
5.1192 -lemma map_sorted: "sorted (map f t) = sorted t" by (induct t) (simp add: map_tree_less map_tree_greater)+
5.1193 -lemma map_color_of: "color_of (map f t) = color_of t" by (induct t) simp+
5.1194 -lemma map_inv1: "inv1 (map f t) = inv1 t" by (induct t) (simp add: map_color_of)+
5.1195 -lemma map_inv2: "inv2 (map f t) = inv2 t" "bheight (map f t) = bheight t" by (induct t) simp+
5.1196 -theorem map_is_rbt [simp]: "is_rbt (map f t) = is_rbt t"
5.1197 -unfolding is_rbt_def by (simp add: map_inv1 map_inv2 map_sorted map_color_of)
5.1198 -
5.1199 -theorem lookup_map: "lookup (map f t) x = Option.map (f x) (lookup t x)"
5.1200 - by (induct t) auto
5.1201 -
5.1202 -
5.1203 -subsection {* Folding over entries *}
5.1204 -
5.1205 -definition fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a, 'b) rbt \<Rightarrow> 'c \<Rightarrow> 'c" where
5.1206 - "fold f t s = foldl (\<lambda>s (k, v). f k v s) s (entries t)"
5.1207 -
5.1208 -lemma fold_simps [simp, code]:
5.1209 - "fold f Empty = id"
5.1210 - "fold f (Branch c lt k v rt) = fold f rt \<circ> f k v \<circ> fold f lt"
5.1211 - by (simp_all add: fold_def expand_fun_eq)
5.1212 -
5.1213 -
5.1214 -subsection {* Bulkloading a tree *}
5.1215 -
5.1216 -definition bulkload :: "('a \<times> 'b) list \<Rightarrow> ('a\<Colon>linorder, 'b) rbt" where
5.1217 - "bulkload xs = foldr (\<lambda>(k, v). RBT.insert k v) xs RBT.Empty"
5.1218 -
5.1219 -lemma bulkload_is_rbt [simp, intro]:
5.1220 - "is_rbt (bulkload xs)"
5.1221 - unfolding bulkload_def by (induct xs) auto
5.1222 -
5.1223 -lemma lookup_bulkload:
5.1224 - "RBT.lookup (bulkload xs) = map_of xs"
5.1225 -proof -
5.1226 - obtain ys where "ys = rev xs" by simp
5.1227 - have "\<And>t. is_rbt t \<Longrightarrow>
5.1228 - RBT.lookup (foldl (\<lambda>t (k, v). RBT.insert k v t) t ys) = RBT.lookup t ++ map_of (rev ys)"
5.1229 - by (induct ys) (simp_all add: bulkload_def split_def RBT.lookup_insert)
5.1230 - from this Empty_is_rbt have
5.1231 - "RBT.lookup (foldl (\<lambda>t (k, v). RBT.insert k v t) RBT.Empty (rev xs)) = RBT.lookup RBT.Empty ++ map_of xs"
5.1232 - by (simp add: `ys = rev xs`)
5.1233 - then show ?thesis by (simp add: bulkload_def foldl_foldr lookup_Empty split_def)
5.1234 -qed
5.1235 -
5.1236 -hide (open) const Empty insert delete entries bulkload lookup map_entry map fold union sorted
5.1237 +hide (open) const impl_of lookup empty insert delete
5.1238 + entries keys bulkload map_entry map fold
5.1239 (*>*)
5.1240
5.1241 text {*
5.1242 - This theory defines purely functional red-black trees which can be
5.1243 - used as an efficient representation of finite maps.
5.1244 + This theory defines abstract red-black trees as an efficient
5.1245 + representation of finite maps, backed by the implementation
5.1246 + in @{theory RBT_Impl}.
5.1247 *}
5.1248
5.1249 -
5.1250 subsection {* Data type and invariant *}
5.1251
5.1252 text {*
5.1253 - The type @{typ "('k, 'v) rbt"} denotes red-black trees with keys of
5.1254 - type @{typ "'k"} and values of type @{typ "'v"}. To function
5.1255 - properly, the key type musorted belong to the @{text "linorder"} class.
5.1256 + The type @{typ "('k, 'v) RBT_Impl.rbt"} denotes red-black trees with
5.1257 + keys of type @{typ "'k"} and values of type @{typ "'v"}. To function
5.1258 + properly, the key type musorted belong to the @{text "linorder"}
5.1259 + class.
5.1260
5.1261 A value @{term t} of this type is a valid red-black tree if it
5.1262 - satisfies the invariant @{text "is_rbt t"}.
5.1263 - This theory provides lemmas to prove that the invariant is
5.1264 - satisfied throughout the computation.
5.1265 + satisfies the invariant @{text "is_rbt t"}. The abstract type @{typ
5.1266 + "('k, 'v) rbt"} always obeys this invariant, and for this reason you
5.1267 + should only use this in our application. Going back to @{typ "('k,
5.1268 + 'v) RBT_Impl.rbt"} may be necessary in proofs if not yet proven
5.1269 + properties about the operations must be established.
5.1270
5.1271 The interpretation function @{const "RBT.lookup"} returns the partial
5.1272 map represented by a red-black tree:
5.1273 @@ -1106,15 +259,12 @@
5.1274 $O(\log n)$.
5.1275 *}
5.1276
5.1277 -
5.1278 subsection {* Operations *}
5.1279
5.1280 -print_antiquotations
5.1281 -
5.1282 text {*
5.1283 Currently, the following operations are supported:
5.1284
5.1285 - @{term_type [display] "RBT.Empty"}
5.1286 + @{term_type [display] "RBT.empty"}
5.1287 Returns the empty tree. $O(1)$
5.1288
5.1289 @{term_type [display] "RBT.insert"}
5.1290 @@ -1137,9 +287,6 @@
5.1291
5.1292 @{term_type [display] "RBT.fold"}
5.1293 Folds over all entries in a tree. $O(n)$
5.1294 -
5.1295 - @{term_type [display] "RBT.union"}
5.1296 - Forms the union of two trees, preferring entries from the first one.
5.1297 *}
5.1298
5.1299
5.1300 @@ -1173,8 +320,8 @@
5.1301
5.1302 text {*
5.1303 \noindent
5.1304 - \underline{@{text "lookup_Empty"}}
5.1305 - @{thm [display] lookup_Empty}
5.1306 + \underline{@{text "lookup_empty"}}
5.1307 + @{thm [display] lookup_empty}
5.1308 \vspace{1ex}
5.1309
5.1310 \noindent
5.1311 @@ -1196,11 +343,6 @@
5.1312 \underline{@{text "lookup_map"}}
5.1313 @{thm [display] lookup_map}
5.1314 \vspace{1ex}
5.1315 -
5.1316 - \noindent
5.1317 - \underline{@{text "lookup_union"}}
5.1318 - @{thm [display] lookup_union}
5.1319 - \vspace{1ex}
5.1320 *}
5.1321
5.1322 end
6.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
6.2 +++ b/src/HOL/Library/RBT_Impl.thy Thu Apr 15 12:27:14 2010 +0200
6.3 @@ -0,0 +1,1084 @@
6.4 +(* Title: RBT_Impl.thy
6.5 + Author: Markus Reiter, TU Muenchen
6.6 + Author: Alexander Krauss, TU Muenchen
6.7 +*)
6.8 +
6.9 +header {* Implementation of Red-Black Trees *}
6.10 +
6.11 +theory RBT_Impl
6.12 +imports Main
6.13 +begin
6.14 +
6.15 +text {*
6.16 + For applications, you should use theory @{text RBT} which defines
6.17 + an abstract type of red-black tree obeying the invariant.
6.18 +*}
6.19 +
6.20 +subsection {* Datatype of RB trees *}
6.21 +
6.22 +datatype color = R | B
6.23 +datatype ('a, 'b) rbt = Empty | Branch color "('a, 'b) rbt" 'a 'b "('a, 'b) rbt"
6.24 +
6.25 +lemma rbt_cases:
6.26 + obtains (Empty) "t = Empty"
6.27 + | (Red) l k v r where "t = Branch R l k v r"
6.28 + | (Black) l k v r where "t = Branch B l k v r"
6.29 +proof (cases t)
6.30 + case Empty with that show thesis by blast
6.31 +next
6.32 + case (Branch c) with that show thesis by (cases c) blast+
6.33 +qed
6.34 +
6.35 +subsection {* Tree properties *}
6.36 +
6.37 +subsubsection {* Content of a tree *}
6.38 +
6.39 +primrec entries :: "('a, 'b) rbt \<Rightarrow> ('a \<times> 'b) list"
6.40 +where
6.41 + "entries Empty = []"
6.42 +| "entries (Branch _ l k v r) = entries l @ (k,v) # entries r"
6.43 +
6.44 +abbreviation (input) entry_in_tree :: "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b) rbt \<Rightarrow> bool"
6.45 +where
6.46 + "entry_in_tree k v t \<equiv> (k, v) \<in> set (entries t)"
6.47 +
6.48 +definition keys :: "('a, 'b) rbt \<Rightarrow> 'a list" where
6.49 + "keys t = map fst (entries t)"
6.50 +
6.51 +lemma keys_simps [simp, code]:
6.52 + "keys Empty = []"
6.53 + "keys (Branch c l k v r) = keys l @ k # keys r"
6.54 + by (simp_all add: keys_def)
6.55 +
6.56 +lemma entry_in_tree_keys:
6.57 + assumes "(k, v) \<in> set (entries t)"
6.58 + shows "k \<in> set (keys t)"
6.59 +proof -
6.60 + from assms have "fst (k, v) \<in> fst ` set (entries t)" by (rule imageI)
6.61 + then show ?thesis by (simp add: keys_def)
6.62 +qed
6.63 +
6.64 +lemma keys_entries:
6.65 + "k \<in> set (keys t) \<longleftrightarrow> (\<exists>v. (k, v) \<in> set (entries t))"
6.66 + by (auto intro: entry_in_tree_keys) (auto simp add: keys_def)
6.67 +
6.68 +
6.69 +subsubsection {* Search tree properties *}
6.70 +
6.71 +definition tree_less :: "'a\<Colon>order \<Rightarrow> ('a, 'b) rbt \<Rightarrow> bool"
6.72 +where
6.73 + tree_less_prop: "tree_less k t \<longleftrightarrow> (\<forall>x\<in>set (keys t). x < k)"
6.74 +
6.75 +abbreviation tree_less_symbol (infix "|\<guillemotleft>" 50)
6.76 +where "t |\<guillemotleft> x \<equiv> tree_less x t"
6.77 +
6.78 +definition tree_greater :: "'a\<Colon>order \<Rightarrow> ('a, 'b) rbt \<Rightarrow> bool" (infix "\<guillemotleft>|" 50)
6.79 +where
6.80 + tree_greater_prop: "tree_greater k t = (\<forall>x\<in>set (keys t). k < x)"
6.81 +
6.82 +lemma tree_less_simps [simp]:
6.83 + "tree_less k Empty = True"
6.84 + "tree_less k (Branch c lt kt v rt) \<longleftrightarrow> kt < k \<and> tree_less k lt \<and> tree_less k rt"
6.85 + by (auto simp add: tree_less_prop)
6.86 +
6.87 +lemma tree_greater_simps [simp]:
6.88 + "tree_greater k Empty = True"
6.89 + "tree_greater k (Branch c lt kt v rt) \<longleftrightarrow> k < kt \<and> tree_greater k lt \<and> tree_greater k rt"
6.90 + by (auto simp add: tree_greater_prop)
6.91 +
6.92 +lemmas tree_ord_props = tree_less_prop tree_greater_prop
6.93 +
6.94 +lemmas tree_greater_nit = tree_greater_prop entry_in_tree_keys
6.95 +lemmas tree_less_nit = tree_less_prop entry_in_tree_keys
6.96 +
6.97 +lemma tree_less_eq_trans: "l |\<guillemotleft> u \<Longrightarrow> u \<le> v \<Longrightarrow> l |\<guillemotleft> v"
6.98 + and tree_less_trans: "t |\<guillemotleft> x \<Longrightarrow> x < y \<Longrightarrow> t |\<guillemotleft> y"
6.99 + and tree_greater_eq_trans: "u \<le> v \<Longrightarrow> v \<guillemotleft>| r \<Longrightarrow> u \<guillemotleft>| r"
6.100 + and tree_greater_trans: "x < y \<Longrightarrow> y \<guillemotleft>| t \<Longrightarrow> x \<guillemotleft>| t"
6.101 + by (auto simp: tree_ord_props)
6.102 +
6.103 +primrec sorted :: "('a::linorder, 'b) rbt \<Rightarrow> bool"
6.104 +where
6.105 + "sorted Empty = True"
6.106 +| "sorted (Branch c l k v r) = (l |\<guillemotleft> k \<and> k \<guillemotleft>| r \<and> sorted l \<and> sorted r)"
6.107 +
6.108 +lemma sorted_entries:
6.109 + "sorted t \<Longrightarrow> List.sorted (List.map fst (entries t))"
6.110 +by (induct t)
6.111 + (force simp: sorted_append sorted_Cons tree_ord_props
6.112 + dest!: entry_in_tree_keys)+
6.113 +
6.114 +lemma distinct_entries:
6.115 + "sorted t \<Longrightarrow> distinct (List.map fst (entries t))"
6.116 +by (induct t)
6.117 + (force simp: sorted_append sorted_Cons tree_ord_props
6.118 + dest!: entry_in_tree_keys)+
6.119 +
6.120 +
6.121 +subsubsection {* Tree lookup *}
6.122 +
6.123 +primrec lookup :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'a \<rightharpoonup> 'b"
6.124 +where
6.125 + "lookup Empty k = None"
6.126 +| "lookup (Branch _ l x y r) k = (if k < x then lookup l k else if x < k then lookup r k else Some y)"
6.127 +
6.128 +lemma lookup_keys: "sorted t \<Longrightarrow> dom (lookup t) = set (keys t)"
6.129 + by (induct t) (auto simp: dom_def tree_greater_prop tree_less_prop)
6.130 +
6.131 +lemma dom_lookup_Branch:
6.132 + "sorted (Branch c t1 k v t2) \<Longrightarrow>
6.133 + dom (lookup (Branch c t1 k v t2))
6.134 + = Set.insert k (dom (lookup t1) \<union> dom (lookup t2))"
6.135 +proof -
6.136 + assume "sorted (Branch c t1 k v t2)"
6.137 + moreover from this have "sorted t1" "sorted t2" by simp_all
6.138 + ultimately show ?thesis by (simp add: lookup_keys)
6.139 +qed
6.140 +
6.141 +lemma finite_dom_lookup [simp, intro!]: "finite (dom (lookup t))"
6.142 +proof (induct t)
6.143 + case Empty then show ?case by simp
6.144 +next
6.145 + case (Branch color t1 a b t2)
6.146 + let ?A = "Set.insert a (dom (lookup t1) \<union> dom (lookup t2))"
6.147 + have "dom (lookup (Branch color t1 a b t2)) \<subseteq> ?A" by (auto split: split_if_asm)
6.148 + moreover from Branch have "finite (insert a (dom (lookup t1) \<union> dom (lookup t2)))" by simp
6.149 + ultimately show ?case by (rule finite_subset)
6.150 +qed
6.151 +
6.152 +lemma lookup_tree_less[simp]: "t |\<guillemotleft> k \<Longrightarrow> lookup t k = None"
6.153 +by (induct t) auto
6.154 +
6.155 +lemma lookup_tree_greater[simp]: "k \<guillemotleft>| t \<Longrightarrow> lookup t k = None"
6.156 +by (induct t) auto
6.157 +
6.158 +lemma lookup_Empty: "lookup Empty = empty"
6.159 +by (rule ext) simp
6.160 +
6.161 +lemma map_of_entries:
6.162 + "sorted t \<Longrightarrow> map_of (entries t) = lookup t"
6.163 +proof (induct t)
6.164 + case Empty thus ?case by (simp add: lookup_Empty)
6.165 +next
6.166 + case (Branch c t1 k v t2)
6.167 + have "lookup (Branch c t1 k v t2) = lookup t2 ++ [k\<mapsto>v] ++ lookup t1"
6.168 + proof (rule ext)
6.169 + fix x
6.170 + from Branch have SORTED: "sorted (Branch c t1 k v t2)" by simp
6.171 + let ?thesis = "lookup (Branch c t1 k v t2) x = (lookup t2 ++ [k \<mapsto> v] ++ lookup t1) x"
6.172 +
6.173 + have DOM_T1: "!!k'. k'\<in>dom (lookup t1) \<Longrightarrow> k>k'"
6.174 + proof -
6.175 + fix k'
6.176 + from SORTED have "t1 |\<guillemotleft> k" by simp
6.177 + with tree_less_prop have "\<forall>k'\<in>set (keys t1). k>k'" by auto
6.178 + moreover assume "k'\<in>dom (lookup t1)"
6.179 + ultimately show "k>k'" using lookup_keys SORTED by auto
6.180 + qed
6.181 +
6.182 + have DOM_T2: "!!k'. k'\<in>dom (lookup t2) \<Longrightarrow> k<k'"
6.183 + proof -
6.184 + fix k'
6.185 + from SORTED have "k \<guillemotleft>| t2" by simp
6.186 + with tree_greater_prop have "\<forall>k'\<in>set (keys t2). k<k'" by auto
6.187 + moreover assume "k'\<in>dom (lookup t2)"
6.188 + ultimately show "k<k'" using lookup_keys SORTED by auto
6.189 + qed
6.190 +
6.191 + {
6.192 + assume C: "x<k"
6.193 + hence "lookup (Branch c t1 k v t2) x = lookup t1 x" by simp
6.194 + moreover from C have "x\<notin>dom [k\<mapsto>v]" by simp
6.195 + moreover have "x\<notin>dom (lookup t2)" proof
6.196 + assume "x\<in>dom (lookup t2)"
6.197 + with DOM_T2 have "k<x" by blast
6.198 + with C show False by simp
6.199 + qed
6.200 + ultimately have ?thesis by (simp add: map_add_upd_left map_add_dom_app_simps)
6.201 + } moreover {
6.202 + assume [simp]: "x=k"
6.203 + hence "lookup (Branch c t1 k v t2) x = [k \<mapsto> v] x" by simp
6.204 + moreover have "x\<notin>dom (lookup t1)" proof
6.205 + assume "x\<in>dom (lookup t1)"
6.206 + with DOM_T1 have "k>x" by blast
6.207 + thus False by simp
6.208 + qed
6.209 + ultimately have ?thesis by (simp add: map_add_upd_left map_add_dom_app_simps)
6.210 + } moreover {
6.211 + assume C: "x>k"
6.212 + hence "lookup (Branch c t1 k v t2) x = lookup t2 x" by (simp add: less_not_sym[of k x])
6.213 + moreover from C have "x\<notin>dom [k\<mapsto>v]" by simp
6.214 + moreover have "x\<notin>dom (lookup t1)" proof
6.215 + assume "x\<in>dom (lookup t1)"
6.216 + with DOM_T1 have "k>x" by simp
6.217 + with C show False by simp
6.218 + qed
6.219 + ultimately have ?thesis by (simp add: map_add_upd_left map_add_dom_app_simps)
6.220 + } ultimately show ?thesis using less_linear by blast
6.221 + qed
6.222 + also from Branch have "lookup t2 ++ [k \<mapsto> v] ++ lookup t1 = map_of (entries (Branch c t1 k v t2))" by simp
6.223 + finally show ?case by simp
6.224 +qed
6.225 +
6.226 +lemma lookup_in_tree: "sorted t \<Longrightarrow> lookup t k = Some v \<longleftrightarrow> (k, v) \<in> set (entries t)"
6.227 + by (simp add: map_of_entries [symmetric] distinct_entries)
6.228 +
6.229 +lemma set_entries_inject:
6.230 + assumes sorted: "sorted t1" "sorted t2"
6.231 + shows "set (entries t1) = set (entries t2) \<longleftrightarrow> entries t1 = entries t2"
6.232 +proof -
6.233 + from sorted have "distinct (map fst (entries t1))"
6.234 + "distinct (map fst (entries t2))"
6.235 + by (auto intro: distinct_entries)
6.236 + with sorted show ?thesis
6.237 + by (auto intro: map_sorted_distinct_set_unique sorted_entries simp add: distinct_map)
6.238 +qed
6.239 +
6.240 +lemma entries_eqI:
6.241 + assumes sorted: "sorted t1" "sorted t2"
6.242 + assumes lookup: "lookup t1 = lookup t2"
6.243 + shows "entries t1 = entries t2"
6.244 +proof -
6.245 + from sorted lookup have "map_of (entries t1) = map_of (entries t2)"
6.246 + by (simp add: map_of_entries)
6.247 + with sorted have "set (entries t1) = set (entries t2)"
6.248 + by (simp add: map_of_inject_set distinct_entries)
6.249 + with sorted show ?thesis by (simp add: set_entries_inject)
6.250 +qed
6.251 +
6.252 +lemma entries_lookup:
6.253 + assumes "sorted t1" "sorted t2"
6.254 + shows "entries t1 = entries t2 \<longleftrightarrow> lookup t1 = lookup t2"
6.255 + using assms by (auto intro: entries_eqI simp add: map_of_entries [symmetric])
6.256 +
6.257 +lemma lookup_from_in_tree:
6.258 + assumes "sorted t1" "sorted t2"
6.259 + and "\<And>v. (k\<Colon>'a\<Colon>linorder, v) \<in> set (entries t1) \<longleftrightarrow> (k, v) \<in> set (entries t2)"
6.260 + shows "lookup t1 k = lookup t2 k"
6.261 +proof -
6.262 + from assms have "k \<in> dom (lookup t1) \<longleftrightarrow> k \<in> dom (lookup t2)"
6.263 + by (simp add: keys_entries lookup_keys)
6.264 + with assms show ?thesis by (auto simp add: lookup_in_tree [symmetric])
6.265 +qed
6.266 +
6.267 +
6.268 +subsubsection {* Red-black properties *}
6.269 +
6.270 +primrec color_of :: "('a, 'b) rbt \<Rightarrow> color"
6.271 +where
6.272 + "color_of Empty = B"
6.273 +| "color_of (Branch c _ _ _ _) = c"
6.274 +
6.275 +primrec bheight :: "('a,'b) rbt \<Rightarrow> nat"
6.276 +where
6.277 + "bheight Empty = 0"
6.278 +| "bheight (Branch c lt k v rt) = (if c = B then Suc (bheight lt) else bheight lt)"
6.279 +
6.280 +primrec inv1 :: "('a, 'b) rbt \<Rightarrow> bool"
6.281 +where
6.282 + "inv1 Empty = True"
6.283 +| "inv1 (Branch c lt k v rt) \<longleftrightarrow> inv1 lt \<and> inv1 rt \<and> (c = B \<or> color_of lt = B \<and> color_of rt = B)"
6.284 +
6.285 +primrec inv1l :: "('a, 'b) rbt \<Rightarrow> bool" -- {* Weaker version *}
6.286 +where
6.287 + "inv1l Empty = True"
6.288 +| "inv1l (Branch c l k v r) = (inv1 l \<and> inv1 r)"
6.289 +lemma [simp]: "inv1 t \<Longrightarrow> inv1l t" by (cases t) simp+
6.290 +
6.291 +primrec inv2 :: "('a, 'b) rbt \<Rightarrow> bool"
6.292 +where
6.293 + "inv2 Empty = True"
6.294 +| "inv2 (Branch c lt k v rt) = (inv2 lt \<and> inv2 rt \<and> bheight lt = bheight rt)"
6.295 +
6.296 +definition is_rbt :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> bool" where
6.297 + "is_rbt t \<longleftrightarrow> inv1 t \<and> inv2 t \<and> color_of t = B \<and> sorted t"
6.298 +
6.299 +lemma is_rbt_sorted [simp]:
6.300 + "is_rbt t \<Longrightarrow> sorted t" by (simp add: is_rbt_def)
6.301 +
6.302 +theorem Empty_is_rbt [simp]:
6.303 + "is_rbt Empty" by (simp add: is_rbt_def)
6.304 +
6.305 +
6.306 +subsection {* Insertion *}
6.307 +
6.308 +fun (* slow, due to massive case splitting *)
6.309 + balance :: "('a,'b) rbt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"
6.310 +where
6.311 + "balance (Branch R a w x b) s t (Branch R c y z d) = Branch R (Branch B a w x b) s t (Branch B c y z d)" |
6.312 + "balance (Branch R (Branch R a w x b) s t c) y z d = Branch R (Branch B a w x b) s t (Branch B c y z d)" |
6.313 + "balance (Branch R a w x (Branch R b s t c)) y z d = Branch R (Branch B a w x b) s t (Branch B c y z d)" |
6.314 + "balance a w x (Branch R b s t (Branch R c y z d)) = Branch R (Branch B a w x b) s t (Branch B c y z d)" |
6.315 + "balance a w x (Branch R (Branch R b s t c) y z d) = Branch R (Branch B a w x b) s t (Branch B c y z d)" |
6.316 + "balance a s t b = Branch B a s t b"
6.317 +
6.318 +lemma balance_inv1: "\<lbrakk>inv1l l; inv1l r\<rbrakk> \<Longrightarrow> inv1 (balance l k v r)"
6.319 + by (induct l k v r rule: balance.induct) auto
6.320 +
6.321 +lemma balance_bheight: "bheight l = bheight r \<Longrightarrow> bheight (balance l k v r) = Suc (bheight l)"
6.322 + by (induct l k v r rule: balance.induct) auto
6.323 +
6.324 +lemma balance_inv2:
6.325 + assumes "inv2 l" "inv2 r" "bheight l = bheight r"
6.326 + shows "inv2 (balance l k v r)"
6.327 + using assms
6.328 + by (induct l k v r rule: balance.induct) auto
6.329 +
6.330 +lemma balance_tree_greater[simp]: "(v \<guillemotleft>| balance a k x b) = (v \<guillemotleft>| a \<and> v \<guillemotleft>| b \<and> v < k)"
6.331 + by (induct a k x b rule: balance.induct) auto
6.332 +
6.333 +lemma balance_tree_less[simp]: "(balance a k x b |\<guillemotleft> v) = (a |\<guillemotleft> v \<and> b |\<guillemotleft> v \<and> k < v)"
6.334 + by (induct a k x b rule: balance.induct) auto
6.335 +
6.336 +lemma balance_sorted:
6.337 + fixes k :: "'a::linorder"
6.338 + assumes "sorted l" "sorted r" "l |\<guillemotleft> k" "k \<guillemotleft>| r"
6.339 + shows "sorted (balance l k v r)"
6.340 +using assms proof (induct l k v r rule: balance.induct)
6.341 + case ("2_2" a x w b y t c z s va vb vd vc)
6.342 + hence "y < z \<and> z \<guillemotleft>| Branch B va vb vd vc"
6.343 + by (auto simp add: tree_ord_props)
6.344 + hence "tree_greater y (Branch B va vb vd vc)" by (blast dest: tree_greater_trans)
6.345 + with "2_2" show ?case by simp
6.346 +next
6.347 + case ("3_2" va vb vd vc x w b y s c z)
6.348 + from "3_2" have "x < y \<and> tree_less x (Branch B va vb vd vc)"
6.349 + by simp
6.350 + hence "tree_less y (Branch B va vb vd vc)" by (blast dest: tree_less_trans)
6.351 + with "3_2" show ?case by simp
6.352 +next
6.353 + case ("3_3" x w b y s c z t va vb vd vc)
6.354 + from "3_3" have "y < z \<and> tree_greater z (Branch B va vb vd vc)" by simp
6.355 + hence "tree_greater y (Branch B va vb vd vc)" by (blast dest: tree_greater_trans)
6.356 + with "3_3" show ?case by simp
6.357 +next
6.358 + case ("3_4" vd ve vg vf x w b y s c z t va vb vii vc)
6.359 + hence "x < y \<and> tree_less x (Branch B vd ve vg vf)" by simp
6.360 + hence 1: "tree_less y (Branch B vd ve vg vf)" by (blast dest: tree_less_trans)
6.361 + from "3_4" have "y < z \<and> tree_greater z (Branch B va vb vii vc)" by simp
6.362 + hence "tree_greater y (Branch B va vb vii vc)" by (blast dest: tree_greater_trans)
6.363 + with 1 "3_4" show ?case by simp
6.364 +next
6.365 + case ("4_2" va vb vd vc x w b y s c z t dd)
6.366 + hence "x < y \<and> tree_less x (Branch B va vb vd vc)" by simp
6.367 + hence "tree_less y (Branch B va vb vd vc)" by (blast dest: tree_less_trans)
6.368 + with "4_2" show ?case by simp
6.369 +next
6.370 + case ("5_2" x w b y s c z t va vb vd vc)
6.371 + hence "y < z \<and> tree_greater z (Branch B va vb vd vc)" by simp
6.372 + hence "tree_greater y (Branch B va vb vd vc)" by (blast dest: tree_greater_trans)
6.373 + with "5_2" show ?case by simp
6.374 +next
6.375 + case ("5_3" va vb vd vc x w b y s c z t)
6.376 + hence "x < y \<and> tree_less x (Branch B va vb vd vc)" by simp
6.377 + hence "tree_less y (Branch B va vb vd vc)" by (blast dest: tree_less_trans)
6.378 + with "5_3" show ?case by simp
6.379 +next
6.380 + case ("5_4" va vb vg vc x w b y s c z t vd ve vii vf)
6.381 + hence "x < y \<and> tree_less x (Branch B va vb vg vc)" by simp
6.382 + hence 1: "tree_less y (Branch B va vb vg vc)" by (blast dest: tree_less_trans)
6.383 + from "5_4" have "y < z \<and> tree_greater z (Branch B vd ve vii vf)" by simp
6.384 + hence "tree_greater y (Branch B vd ve vii vf)" by (blast dest: tree_greater_trans)
6.385 + with 1 "5_4" show ?case by simp
6.386 +qed simp+
6.387 +
6.388 +lemma entries_balance [simp]:
6.389 + "entries (balance l k v r) = entries l @ (k, v) # entries r"
6.390 + by (induct l k v r rule: balance.induct) auto
6.391 +
6.392 +lemma keys_balance [simp]:
6.393 + "keys (balance l k v r) = keys l @ k # keys r"
6.394 + by (simp add: keys_def)
6.395 +
6.396 +lemma balance_in_tree:
6.397 + "entry_in_tree k x (balance l v y r) \<longleftrightarrow> entry_in_tree k x l \<or> k = v \<and> x = y \<or> entry_in_tree k x r"
6.398 + by (auto simp add: keys_def)
6.399 +
6.400 +lemma lookup_balance[simp]:
6.401 +fixes k :: "'a::linorder"
6.402 +assumes "sorted l" "sorted r" "l |\<guillemotleft> k" "k \<guillemotleft>| r"
6.403 +shows "lookup (balance l k v r) x = lookup (Branch B l k v r) x"
6.404 +by (rule lookup_from_in_tree) (auto simp:assms balance_in_tree balance_sorted)
6.405 +
6.406 +primrec paint :: "color \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"
6.407 +where
6.408 + "paint c Empty = Empty"
6.409 +| "paint c (Branch _ l k v r) = Branch c l k v r"
6.410 +
6.411 +lemma paint_inv1l[simp]: "inv1l t \<Longrightarrow> inv1l (paint c t)" by (cases t) auto
6.412 +lemma paint_inv1[simp]: "inv1l t \<Longrightarrow> inv1 (paint B t)" by (cases t) auto
6.413 +lemma paint_inv2[simp]: "inv2 t \<Longrightarrow> inv2 (paint c t)" by (cases t) auto
6.414 +lemma paint_color_of[simp]: "color_of (paint B t) = B" by (cases t) auto
6.415 +lemma paint_sorted[simp]: "sorted t \<Longrightarrow> sorted (paint c t)" by (cases t) auto
6.416 +lemma paint_in_tree[simp]: "entry_in_tree k x (paint c t) = entry_in_tree k x t" by (cases t) auto
6.417 +lemma paint_lookup[simp]: "lookup (paint c t) = lookup t" by (rule ext) (cases t, auto)
6.418 +lemma paint_tree_greater[simp]: "(v \<guillemotleft>| paint c t) = (v \<guillemotleft>| t)" by (cases t) auto
6.419 +lemma paint_tree_less[simp]: "(paint c t |\<guillemotleft> v) = (t |\<guillemotleft> v)" by (cases t) auto
6.420 +
6.421 +fun
6.422 + ins :: "('a\<Colon>linorder \<Rightarrow> 'b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"
6.423 +where
6.424 + "ins f k v Empty = Branch R Empty k v Empty" |
6.425 + "ins f k v (Branch B l x y r) = (if k < x then balance (ins f k v l) x y r
6.426 + else if k > x then balance l x y (ins f k v r)
6.427 + else Branch B l x (f k y v) r)" |
6.428 + "ins f k v (Branch R l x y r) = (if k < x then Branch R (ins f k v l) x y r
6.429 + else if k > x then Branch R l x y (ins f k v r)
6.430 + else Branch R l x (f k y v) r)"
6.431 +
6.432 +lemma ins_inv1_inv2:
6.433 + assumes "inv1 t" "inv2 t"
6.434 + shows "inv2 (ins f k x t)" "bheight (ins f k x t) = bheight t"
6.435 + "color_of t = B \<Longrightarrow> inv1 (ins f k x t)" "inv1l (ins f k x t)"
6.436 + using assms
6.437 + by (induct f k x t rule: ins.induct) (auto simp: balance_inv1 balance_inv2 balance_bheight)
6.438 +
6.439 +lemma ins_tree_greater[simp]: "(v \<guillemotleft>| ins f k x t) = (v \<guillemotleft>| t \<and> k > v)"
6.440 + by (induct f k x t rule: ins.induct) auto
6.441 +lemma ins_tree_less[simp]: "(ins f k x t |\<guillemotleft> v) = (t |\<guillemotleft> v \<and> k < v)"
6.442 + by (induct f k x t rule: ins.induct) auto
6.443 +lemma ins_sorted[simp]: "sorted t \<Longrightarrow> sorted (ins f k x t)"
6.444 + by (induct f k x t rule: ins.induct) (auto simp: balance_sorted)
6.445 +
6.446 +lemma keys_ins: "set (keys (ins f k v t)) = { k } \<union> set (keys t)"
6.447 + by (induct f k v t rule: ins.induct) auto
6.448 +
6.449 +lemma lookup_ins:
6.450 + fixes k :: "'a::linorder"
6.451 + assumes "sorted t"
6.452 + shows "lookup (ins f k v t) x = ((lookup t)(k |-> case lookup t k of None \<Rightarrow> v
6.453 + | Some w \<Rightarrow> f k w v)) x"
6.454 +using assms by (induct f k v t rule: ins.induct) auto
6.455 +
6.456 +definition
6.457 + insert_with_key :: "('a\<Colon>linorder \<Rightarrow> 'b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"
6.458 +where
6.459 + "insert_with_key f k v t = paint B (ins f k v t)"
6.460 +
6.461 +lemma insertwk_sorted: "sorted t \<Longrightarrow> sorted (insert_with_key f k x t)"
6.462 + by (auto simp: insert_with_key_def)
6.463 +
6.464 +theorem insertwk_is_rbt:
6.465 + assumes inv: "is_rbt t"
6.466 + shows "is_rbt (insert_with_key f k x t)"
6.467 +using assms
6.468 +unfolding insert_with_key_def is_rbt_def
6.469 +by (auto simp: ins_inv1_inv2)
6.470 +
6.471 +lemma lookup_insertwk:
6.472 + assumes "sorted t"
6.473 + shows "lookup (insert_with_key f k v t) x = ((lookup t)(k |-> case lookup t k of None \<Rightarrow> v
6.474 + | Some w \<Rightarrow> f k w v)) x"
6.475 +unfolding insert_with_key_def using assms
6.476 +by (simp add:lookup_ins)
6.477 +
6.478 +definition
6.479 + insertw_def: "insert_with f = insert_with_key (\<lambda>_. f)"
6.480 +
6.481 +lemma insertw_sorted: "sorted t \<Longrightarrow> sorted (insert_with f k v t)" by (simp add: insertwk_sorted insertw_def)
6.482 +theorem insertw_is_rbt: "is_rbt t \<Longrightarrow> is_rbt (insert_with f k v t)" by (simp add: insertwk_is_rbt insertw_def)
6.483 +
6.484 +lemma lookup_insertw:
6.485 + assumes "is_rbt t"
6.486 + shows "lookup (insert_with f k v t) = (lookup t)(k \<mapsto> (if k:dom (lookup t) then f (the (lookup t k)) v else v))"
6.487 +using assms
6.488 +unfolding insertw_def
6.489 +by (rule_tac ext) (cases "lookup t k", auto simp:lookup_insertwk dom_def)
6.490 +
6.491 +definition insert :: "'a\<Colon>linorder \<Rightarrow> 'b \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt" where
6.492 + "insert = insert_with_key (\<lambda>_ _ nv. nv)"
6.493 +
6.494 +lemma insert_sorted: "sorted t \<Longrightarrow> sorted (insert k v t)" by (simp add: insertwk_sorted insert_def)
6.495 +theorem insert_is_rbt [simp]: "is_rbt t \<Longrightarrow> is_rbt (insert k v t)" by (simp add: insertwk_is_rbt insert_def)
6.496 +
6.497 +lemma lookup_insert:
6.498 + assumes "is_rbt t"
6.499 + shows "lookup (insert k v t) = (lookup t)(k\<mapsto>v)"
6.500 +unfolding insert_def
6.501 +using assms
6.502 +by (rule_tac ext) (simp add: lookup_insertwk split:option.split)
6.503 +
6.504 +
6.505 +subsection {* Deletion *}
6.506 +
6.507 +lemma bheight_paintR'[simp]: "color_of t = B \<Longrightarrow> bheight (paint R t) = bheight t - 1"
6.508 +by (cases t rule: rbt_cases) auto
6.509 +
6.510 +fun
6.511 + balance_left :: "('a,'b) rbt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"
6.512 +where
6.513 + "balance_left (Branch R a k x b) s y c = Branch R (Branch B a k x b) s y c" |
6.514 + "balance_left bl k x (Branch B a s y b) = balance bl k x (Branch R a s y b)" |
6.515 + "balance_left bl k x (Branch R (Branch B a s y b) t z c) = Branch R (Branch B bl k x a) s y (balance b t z (paint R c))" |
6.516 + "balance_left t k x s = Empty"
6.517 +
6.518 +lemma balance_left_inv2_with_inv1:
6.519 + assumes "inv2 lt" "inv2 rt" "bheight lt + 1 = bheight rt" "inv1 rt"
6.520 + shows "bheight (balance_left lt k v rt) = bheight lt + 1"
6.521 + and "inv2 (balance_left lt k v rt)"
6.522 +using assms
6.523 +by (induct lt k v rt rule: balance_left.induct) (auto simp: balance_inv2 balance_bheight)
6.524 +
6.525 +lemma balance_left_inv2_app:
6.526 + assumes "inv2 lt" "inv2 rt" "bheight lt + 1 = bheight rt" "color_of rt = B"
6.527 + shows "inv2 (balance_left lt k v rt)"
6.528 + "bheight (balance_left lt k v rt) = bheight rt"
6.529 +using assms
6.530 +by (induct lt k v rt rule: balance_left.induct) (auto simp add: balance_inv2 balance_bheight)+
6.531 +
6.532 +lemma balance_left_inv1: "\<lbrakk>inv1l a; inv1 b; color_of b = B\<rbrakk> \<Longrightarrow> inv1 (balance_left a k x b)"
6.533 + by (induct a k x b rule: balance_left.induct) (simp add: balance_inv1)+
6.534 +
6.535 +lemma balance_left_inv1l: "\<lbrakk> inv1l lt; inv1 rt \<rbrakk> \<Longrightarrow> inv1l (balance_left lt k x rt)"
6.536 +by (induct lt k x rt rule: balance_left.induct) (auto simp: balance_inv1)
6.537 +
6.538 +lemma balance_left_sorted: "\<lbrakk> sorted l; sorted r; tree_less k l; tree_greater k r \<rbrakk> \<Longrightarrow> sorted (balance_left l k v r)"
6.539 +apply (induct l k v r rule: balance_left.induct)
6.540 +apply (auto simp: balance_sorted)
6.541 +apply (unfold tree_greater_prop tree_less_prop)
6.542 +by force+
6.543 +
6.544 +lemma balance_left_tree_greater:
6.545 + fixes k :: "'a::order"
6.546 + assumes "k \<guillemotleft>| a" "k \<guillemotleft>| b" "k < x"
6.547 + shows "k \<guillemotleft>| balance_left a x t b"
6.548 +using assms
6.549 +by (induct a x t b rule: balance_left.induct) auto
6.550 +
6.551 +lemma balance_left_tree_less:
6.552 + fixes k :: "'a::order"
6.553 + assumes "a |\<guillemotleft> k" "b |\<guillemotleft> k" "x < k"
6.554 + shows "balance_left a x t b |\<guillemotleft> k"
6.555 +using assms
6.556 +by (induct a x t b rule: balance_left.induct) auto
6.557 +
6.558 +lemma balance_left_in_tree:
6.559 + assumes "inv1l l" "inv1 r" "bheight l + 1 = bheight r"
6.560 + shows "entry_in_tree k v (balance_left l a b r) = (entry_in_tree k v l \<or> k = a \<and> v = b \<or> entry_in_tree k v r)"
6.561 +using assms
6.562 +by (induct l k v r rule: balance_left.induct) (auto simp: balance_in_tree)
6.563 +
6.564 +fun
6.565 + balance_right :: "('a,'b) rbt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"
6.566 +where
6.567 + "balance_right a k x (Branch R b s y c) = Branch R a k x (Branch B b s y c)" |
6.568 + "balance_right (Branch B a k x b) s y bl = balance (Branch R a k x b) s y bl" |
6.569 + "balance_right (Branch R a k x (Branch B b s y c)) t z bl = Branch R (balance (paint R a) k x b) s y (Branch B c t z bl)" |
6.570 + "balance_right t k x s = Empty"
6.571 +
6.572 +lemma balance_right_inv2_with_inv1:
6.573 + assumes "inv2 lt" "inv2 rt" "bheight lt = bheight rt + 1" "inv1 lt"
6.574 + shows "inv2 (balance_right lt k v rt) \<and> bheight (balance_right lt k v rt) = bheight lt"
6.575 +using assms
6.576 +by (induct lt k v rt rule: balance_right.induct) (auto simp: balance_inv2 balance_bheight)
6.577 +
6.578 +lemma balance_right_inv1: "\<lbrakk>inv1 a; inv1l b; color_of a = B\<rbrakk> \<Longrightarrow> inv1 (balance_right a k x b)"
6.579 +by (induct a k x b rule: balance_right.induct) (simp add: balance_inv1)+
6.580 +
6.581 +lemma balance_right_inv1l: "\<lbrakk> inv1 lt; inv1l rt \<rbrakk> \<Longrightarrow>inv1l (balance_right lt k x rt)"
6.582 +by (induct lt k x rt rule: balance_right.induct) (auto simp: balance_inv1)
6.583 +
6.584 +lemma balance_right_sorted: "\<lbrakk> sorted l; sorted r; tree_less k l; tree_greater k r \<rbrakk> \<Longrightarrow> sorted (balance_right l k v r)"
6.585 +apply (induct l k v r rule: balance_right.induct)
6.586 +apply (auto simp:balance_sorted)
6.587 +apply (unfold tree_less_prop tree_greater_prop)
6.588 +by force+
6.589 +
6.590 +lemma balance_right_tree_greater:
6.591 + fixes k :: "'a::order"
6.592 + assumes "k \<guillemotleft>| a" "k \<guillemotleft>| b" "k < x"
6.593 + shows "k \<guillemotleft>| balance_right a x t b"
6.594 +using assms by (induct a x t b rule: balance_right.induct) auto
6.595 +
6.596 +lemma balance_right_tree_less:
6.597 + fixes k :: "'a::order"
6.598 + assumes "a |\<guillemotleft> k" "b |\<guillemotleft> k" "x < k"
6.599 + shows "balance_right a x t b |\<guillemotleft> k"
6.600 +using assms by (induct a x t b rule: balance_right.induct) auto
6.601 +
6.602 +lemma balance_right_in_tree:
6.603 + assumes "inv1 l" "inv1l r" "bheight l = bheight r + 1" "inv2 l" "inv2 r"
6.604 + shows "entry_in_tree x y (balance_right l k v r) = (entry_in_tree x y l \<or> x = k \<and> y = v \<or> entry_in_tree x y r)"
6.605 +using assms by (induct l k v r rule: balance_right.induct) (auto simp: balance_in_tree)
6.606 +
6.607 +fun
6.608 + combine :: "('a,'b) rbt \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"
6.609 +where
6.610 + "combine Empty x = x"
6.611 +| "combine x Empty = x"
6.612 +| "combine (Branch R a k x b) (Branch R c s y d) = (case (combine b c) of
6.613 + Branch R b2 t z c2 \<Rightarrow> (Branch R (Branch R a k x b2) t z (Branch R c2 s y d)) |
6.614 + bc \<Rightarrow> Branch R a k x (Branch R bc s y d))"
6.615 +| "combine (Branch B a k x b) (Branch B c s y d) = (case (combine b c) of
6.616 + Branch R b2 t z c2 \<Rightarrow> Branch R (Branch B a k x b2) t z (Branch B c2 s y d) |
6.617 + bc \<Rightarrow> balance_left a k x (Branch B bc s y d))"
6.618 +| "combine a (Branch R b k x c) = Branch R (combine a b) k x c"
6.619 +| "combine (Branch R a k x b) c = Branch R a k x (combine b c)"
6.620 +
6.621 +lemma combine_inv2:
6.622 + assumes "inv2 lt" "inv2 rt" "bheight lt = bheight rt"
6.623 + shows "bheight (combine lt rt) = bheight lt" "inv2 (combine lt rt)"
6.624 +using assms
6.625 +by (induct lt rt rule: combine.induct)
6.626 + (auto simp: balance_left_inv2_app split: rbt.splits color.splits)
6.627 +
6.628 +lemma combine_inv1:
6.629 + assumes "inv1 lt" "inv1 rt"
6.630 + shows "color_of lt = B \<Longrightarrow> color_of rt = B \<Longrightarrow> inv1 (combine lt rt)"
6.631 + "inv1l (combine lt rt)"
6.632 +using assms
6.633 +by (induct lt rt rule: combine.induct)
6.634 + (auto simp: balance_left_inv1 split: rbt.splits color.splits)
6.635 +
6.636 +lemma combine_tree_greater[simp]:
6.637 + fixes k :: "'a::linorder"
6.638 + assumes "k \<guillemotleft>| l" "k \<guillemotleft>| r"
6.639 + shows "k \<guillemotleft>| combine l r"
6.640 +using assms
6.641 +by (induct l r rule: combine.induct)
6.642 + (auto simp: balance_left_tree_greater split:rbt.splits color.splits)
6.643 +
6.644 +lemma combine_tree_less[simp]:
6.645 + fixes k :: "'a::linorder"
6.646 + assumes "l |\<guillemotleft> k" "r |\<guillemotleft> k"
6.647 + shows "combine l r |\<guillemotleft> k"
6.648 +using assms
6.649 +by (induct l r rule: combine.induct)
6.650 + (auto simp: balance_left_tree_less split:rbt.splits color.splits)
6.651 +
6.652 +lemma combine_sorted:
6.653 + fixes k :: "'a::linorder"
6.654 + assumes "sorted l" "sorted r" "l |\<guillemotleft> k" "k \<guillemotleft>| r"
6.655 + shows "sorted (combine l r)"
6.656 +using assms proof (induct l r rule: combine.induct)
6.657 + case (3 a x v b c y w d)
6.658 + hence ineqs: "a |\<guillemotleft> x" "x \<guillemotleft>| b" "b |\<guillemotleft> k" "k \<guillemotleft>| c" "c |\<guillemotleft> y" "y \<guillemotleft>| d"
6.659 + by auto
6.660 + with 3
6.661 + show ?case
6.662 + by (cases "combine b c" rule: rbt_cases)
6.663 + (auto, (metis combine_tree_greater combine_tree_less ineqs ineqs tree_less_simps(2) tree_greater_simps(2) tree_greater_trans tree_less_trans)+)
6.664 +next
6.665 + case (4 a x v b c y w d)
6.666 + hence "x < k \<and> tree_greater k c" by simp
6.667 + hence "tree_greater x c" by (blast dest: tree_greater_trans)
6.668 + with 4 have 2: "tree_greater x (combine b c)" by (simp add: combine_tree_greater)
6.669 + from 4 have "k < y \<and> tree_less k b" by simp
6.670 + hence "tree_less y b" by (blast dest: tree_less_trans)
6.671 + with 4 have 3: "tree_less y (combine b c)" by (simp add: combine_tree_less)
6.672 + show ?case
6.673 + proof (cases "combine b c" rule: rbt_cases)
6.674 + case Empty
6.675 + from 4 have "x < y \<and> tree_greater y d" by auto
6.676 + hence "tree_greater x d" by (blast dest: tree_greater_trans)
6.677 + with 4 Empty have "sorted a" and "sorted (Branch B Empty y w d)" and "tree_less x a" and "tree_greater x (Branch B Empty y w d)" by auto
6.678 + with Empty show ?thesis by (simp add: balance_left_sorted)
6.679 + next
6.680 + case (Red lta va ka rta)
6.681 + with 2 4 have "x < va \<and> tree_less x a" by simp
6.682 + hence 5: "tree_less va a" by (blast dest: tree_less_trans)
6.683 + from Red 3 4 have "va < y \<and> tree_greater y d" by simp
6.684 + hence "tree_greater va d" by (blast dest: tree_greater_trans)
6.685 + with Red 2 3 4 5 show ?thesis by simp
6.686 + next
6.687 + case (Black lta va ka rta)
6.688 + from 4 have "x < y \<and> tree_greater y d" by auto
6.689 + hence "tree_greater x d" by (blast dest: tree_greater_trans)
6.690 + with Black 2 3 4 have "sorted a" and "sorted (Branch B (combine b c) y w d)" and "tree_less x a" and "tree_greater x (Branch B (combine b c) y w d)" by auto
6.691 + with Black show ?thesis by (simp add: balance_left_sorted)
6.692 + qed
6.693 +next
6.694 + case (5 va vb vd vc b x w c)
6.695 + hence "k < x \<and> tree_less k (Branch B va vb vd vc)" by simp
6.696 + hence "tree_less x (Branch B va vb vd vc)" by (blast dest: tree_less_trans)
6.697 + with 5 show ?case by (simp add: combine_tree_less)
6.698 +next
6.699 + case (6 a x v b va vb vd vc)
6.700 + hence "x < k \<and> tree_greater k (Branch B va vb vd vc)" by simp
6.701 + hence "tree_greater x (Branch B va vb vd vc)" by (blast dest: tree_greater_trans)
6.702 + with 6 show ?case by (simp add: combine_tree_greater)
6.703 +qed simp+
6.704 +
6.705 +lemma combine_in_tree:
6.706 + assumes "inv2 l" "inv2 r" "bheight l = bheight r" "inv1 l" "inv1 r"
6.707 + shows "entry_in_tree k v (combine l r) = (entry_in_tree k v l \<or> entry_in_tree k v r)"
6.708 +using assms
6.709 +proof (induct l r rule: combine.induct)
6.710 + case (4 _ _ _ b c)
6.711 + hence a: "bheight (combine b c) = bheight b" by (simp add: combine_inv2)
6.712 + from 4 have b: "inv1l (combine b c)" by (simp add: combine_inv1)
6.713 +
6.714 + show ?case
6.715 + proof (cases "combine b c" rule: rbt_cases)
6.716 + case Empty
6.717 + with 4 a show ?thesis by (auto simp: balance_left_in_tree)
6.718 + next
6.719 + case (Red lta ka va rta)
6.720 + with 4 show ?thesis by auto
6.721 + next
6.722 + case (Black lta ka va rta)
6.723 + with a b 4 show ?thesis by (auto simp: balance_left_in_tree)
6.724 + qed
6.725 +qed (auto split: rbt.splits color.splits)
6.726 +
6.727 +fun
6.728 + del_from_left :: "('a\<Colon>linorder) \<Rightarrow> ('a,'b) rbt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt" and
6.729 + del_from_right :: "('a\<Colon>linorder) \<Rightarrow> ('a,'b) rbt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt" and
6.730 + del :: "('a\<Colon>linorder) \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"
6.731 +where
6.732 + "del x Empty = Empty" |
6.733 + "del x (Branch c a y s b) = (if x < y then del_from_left x a y s b else (if x > y then del_from_right x a y s b else combine a b))" |
6.734 + "del_from_left x (Branch B lt z v rt) y s b = balance_left (del x (Branch B lt z v rt)) y s b" |
6.735 + "del_from_left x a y s b = Branch R (del x a) y s b" |
6.736 + "del_from_right x a y s (Branch B lt z v rt) = balance_right a y s (del x (Branch B lt z v rt))" |
6.737 + "del_from_right x a y s b = Branch R a y s (del x b)"
6.738 +
6.739 +lemma
6.740 + assumes "inv2 lt" "inv1 lt"
6.741 + shows
6.742 + "\<lbrakk>inv2 rt; bheight lt = bheight rt; inv1 rt\<rbrakk> \<Longrightarrow>
6.743 + inv2 (del_from_left x lt k v rt) \<and> bheight (del_from_left x lt k v rt) = bheight lt \<and> (color_of lt = B \<and> color_of rt = B \<and> inv1 (del_from_left x lt k v rt) \<or> (color_of lt \<noteq> B \<or> color_of rt \<noteq> B) \<and> inv1l (del_from_left x lt k v rt))"
6.744 + and "\<lbrakk>inv2 rt; bheight lt = bheight rt; inv1 rt\<rbrakk> \<Longrightarrow>
6.745 + inv2 (del_from_right x lt k v rt) \<and> bheight (del_from_right x lt k v rt) = bheight lt \<and> (color_of lt = B \<and> color_of rt = B \<and> inv1 (del_from_right x lt k v rt) \<or> (color_of lt \<noteq> B \<or> color_of rt \<noteq> B) \<and> inv1l (del_from_right x lt k v rt))"
6.746 + and del_inv1_inv2: "inv2 (del x lt) \<and> (color_of lt = R \<and> bheight (del x lt) = bheight lt \<and> inv1 (del x lt)
6.747 + \<or> color_of lt = B \<and> bheight (del x lt) = bheight lt - 1 \<and> inv1l (del x lt))"
6.748 +using assms
6.749 +proof (induct x lt k v rt and x lt k v rt and x lt rule: del_from_left_del_from_right_del.induct)
6.750 +case (2 y c _ y')
6.751 + have "y = y' \<or> y < y' \<or> y > y'" by auto
6.752 + thus ?case proof (elim disjE)
6.753 + assume "y = y'"
6.754 + with 2 show ?thesis by (cases c) (simp add: combine_inv2 combine_inv1)+
6.755 + next
6.756 + assume "y < y'"
6.757 + with 2 show ?thesis by (cases c) auto
6.758 + next
6.759 + assume "y' < y"
6.760 + with 2 show ?thesis by (cases c) auto
6.761 + qed
6.762 +next
6.763 + case (3 y lt z v rta y' ss bb)
6.764 + thus ?case by (cases "color_of (Branch B lt z v rta) = B \<and> color_of bb = B") (simp add: balance_left_inv2_with_inv1 balance_left_inv1 balance_left_inv1l)+
6.765 +next
6.766 + case (5 y a y' ss lt z v rta)
6.767 + thus ?case by (cases "color_of a = B \<and> color_of (Branch B lt z v rta) = B") (simp add: balance_right_inv2_with_inv1 balance_right_inv1 balance_right_inv1l)+
6.768 +next
6.769 + case ("6_1" y a y' ss) thus ?case by (cases "color_of a = B \<and> color_of Empty = B") simp+
6.770 +qed auto
6.771 +
6.772 +lemma
6.773 + del_from_left_tree_less: "\<lbrakk>tree_less v lt; tree_less v rt; k < v\<rbrakk> \<Longrightarrow> tree_less v (del_from_left x lt k y rt)"
6.774 + and del_from_right_tree_less: "\<lbrakk>tree_less v lt; tree_less v rt; k < v\<rbrakk> \<Longrightarrow> tree_less v (del_from_right x lt k y rt)"
6.775 + and del_tree_less: "tree_less v lt \<Longrightarrow> tree_less v (del x lt)"
6.776 +by (induct x lt k y rt and x lt k y rt and x lt rule: del_from_left_del_from_right_del.induct)
6.777 + (auto simp: balance_left_tree_less balance_right_tree_less)
6.778 +
6.779 +lemma del_from_left_tree_greater: "\<lbrakk>tree_greater v lt; tree_greater v rt; k > v\<rbrakk> \<Longrightarrow> tree_greater v (del_from_left x lt k y rt)"
6.780 + and del_from_right_tree_greater: "\<lbrakk>tree_greater v lt; tree_greater v rt; k > v\<rbrakk> \<Longrightarrow> tree_greater v (del_from_right x lt k y rt)"
6.781 + and del_tree_greater: "tree_greater v lt \<Longrightarrow> tree_greater v (del x lt)"
6.782 +by (induct x lt k y rt and x lt k y rt and x lt rule: del_from_left_del_from_right_del.induct)
6.783 + (auto simp: balance_left_tree_greater balance_right_tree_greater)
6.784 +
6.785 +lemma "\<lbrakk>sorted lt; sorted rt; tree_less k lt; tree_greater k rt\<rbrakk> \<Longrightarrow> sorted (del_from_left x lt k y rt)"
6.786 + and "\<lbrakk>sorted lt; sorted rt; tree_less k lt; tree_greater k rt\<rbrakk> \<Longrightarrow> sorted (del_from_right x lt k y rt)"
6.787 + and del_sorted: "sorted lt \<Longrightarrow> sorted (del x lt)"
6.788 +proof (induct x lt k y rt and x lt k y rt and x lt rule: del_from_left_del_from_right_del.induct)
6.789 + case (3 x lta zz v rta yy ss bb)
6.790 + from 3 have "tree_less yy (Branch B lta zz v rta)" by simp
6.791 + hence "tree_less yy (del x (Branch B lta zz v rta))" by (rule del_tree_less)
6.792 + with 3 show ?case by (simp add: balance_left_sorted)
6.793 +next
6.794 + case ("4_2" x vaa vbb vdd vc yy ss bb)
6.795 + hence "tree_less yy (Branch R vaa vbb vdd vc)" by simp
6.796 + hence "tree_less yy (del x (Branch R vaa vbb vdd vc))" by (rule del_tree_less)
6.797 + with "4_2" show ?case by simp
6.798 +next
6.799 + case (5 x aa yy ss lta zz v rta)
6.800 + hence "tree_greater yy (Branch B lta zz v rta)" by simp
6.801 + hence "tree_greater yy (del x (Branch B lta zz v rta))" by (rule del_tree_greater)
6.802 + with 5 show ?case by (simp add: balance_right_sorted)
6.803 +next
6.804 + case ("6_2" x aa yy ss vaa vbb vdd vc)
6.805 + hence "tree_greater yy (Branch R vaa vbb vdd vc)" by simp
6.806 + hence "tree_greater yy (del x (Branch R vaa vbb vdd vc))" by (rule del_tree_greater)
6.807 + with "6_2" show ?case by simp
6.808 +qed (auto simp: combine_sorted)
6.809 +
6.810 +lemma "\<lbrakk>sorted lt; sorted rt; tree_less kt lt; tree_greater kt rt; inv1 lt; inv1 rt; inv2 lt; inv2 rt; bheight lt = bheight rt; x < kt\<rbrakk> \<Longrightarrow> entry_in_tree k v (del_from_left x lt kt y rt) = (False \<or> (x \<noteq> k \<and> entry_in_tree k v (Branch c lt kt y rt)))"
6.811 + and "\<lbrakk>sorted lt; sorted rt; tree_less kt lt; tree_greater kt rt; inv1 lt; inv1 rt; inv2 lt; inv2 rt; bheight lt = bheight rt; x > kt\<rbrakk> \<Longrightarrow> entry_in_tree k v (del_from_right x lt kt y rt) = (False \<or> (x \<noteq> k \<and> entry_in_tree k v (Branch c lt kt y rt)))"
6.812 + and del_in_tree: "\<lbrakk>sorted t; inv1 t; inv2 t\<rbrakk> \<Longrightarrow> entry_in_tree k v (del x t) = (False \<or> (x \<noteq> k \<and> entry_in_tree k v t))"
6.813 +proof (induct x lt kt y rt and x lt kt y rt and x t rule: del_from_left_del_from_right_del.induct)
6.814 + case (2 xx c aa yy ss bb)
6.815 + have "xx = yy \<or> xx < yy \<or> xx > yy" by auto
6.816 + from this 2 show ?case proof (elim disjE)
6.817 + assume "xx = yy"
6.818 + with 2 show ?thesis proof (cases "xx = k")
6.819 + case True
6.820 + from 2 `xx = yy` `xx = k` have "sorted (Branch c aa yy ss bb) \<and> k = yy" by simp
6.821 + hence "\<not> entry_in_tree k v aa" "\<not> entry_in_tree k v bb" by (auto simp: tree_less_nit tree_greater_prop)
6.822 + with `xx = yy` 2 `xx = k` show ?thesis by (simp add: combine_in_tree)
6.823 + qed (simp add: combine_in_tree)
6.824 + qed simp+
6.825 +next
6.826 + case (3 xx lta zz vv rta yy ss bb)
6.827 + def mt[simp]: mt == "Branch B lta zz vv rta"
6.828 + from 3 have "inv2 mt \<and> inv1 mt" by simp
6.829 + hence "inv2 (del xx mt) \<and> (color_of mt = R \<and> bheight (del xx mt) = bheight mt \<and> inv1 (del xx mt) \<or> color_of mt = B \<and> bheight (del xx mt) = bheight mt - 1 \<and> inv1l (del xx mt))" by (blast dest: del_inv1_inv2)
6.830 + with 3 have 4: "entry_in_tree k v (del_from_left xx mt yy ss bb) = (False \<or> xx \<noteq> k \<and> entry_in_tree k v mt \<or> (k = yy \<and> v = ss) \<or> entry_in_tree k v bb)" by (simp add: balance_left_in_tree)
6.831 + thus ?case proof (cases "xx = k")
6.832 + case True
6.833 + from 3 True have "tree_greater yy bb \<and> yy > k" by simp
6.834 + hence "tree_greater k bb" by (blast dest: tree_greater_trans)
6.835 + with 3 4 True show ?thesis by (auto simp: tree_greater_nit)
6.836 + qed auto
6.837 +next
6.838 + case ("4_1" xx yy ss bb)
6.839 + show ?case proof (cases "xx = k")
6.840 + case True
6.841 + with "4_1" have "tree_greater yy bb \<and> k < yy" by simp
6.842 + hence "tree_greater k bb" by (blast dest: tree_greater_trans)
6.843 + with "4_1" `xx = k`
6.844 + have "entry_in_tree k v (Branch R Empty yy ss bb) = entry_in_tree k v Empty" by (auto simp: tree_greater_nit)
6.845 + thus ?thesis by auto
6.846 + qed simp+
6.847 +next
6.848 + case ("4_2" xx vaa vbb vdd vc yy ss bb)
6.849 + thus ?case proof (cases "xx = k")
6.850 + case True
6.851 + with "4_2" have "k < yy \<and> tree_greater yy bb" by simp
6.852 + hence "tree_greater k bb" by (blast dest: tree_greater_trans)
6.853 + with True "4_2" show ?thesis by (auto simp: tree_greater_nit)
6.854 + qed auto
6.855 +next
6.856 + case (5 xx aa yy ss lta zz vv rta)
6.857 + def mt[simp]: mt == "Branch B lta zz vv rta"
6.858 + from 5 have "inv2 mt \<and> inv1 mt" by simp
6.859 + hence "inv2 (del xx mt) \<and> (color_of mt = R \<and> bheight (del xx mt) = bheight mt \<and> inv1 (del xx mt) \<or> color_of mt = B \<and> bheight (del xx mt) = bheight mt - 1 \<and> inv1l (del xx mt))" by (blast dest: del_inv1_inv2)
6.860 + with 5 have 3: "entry_in_tree k v (del_from_right xx aa yy ss mt) = (entry_in_tree k v aa \<or> (k = yy \<and> v = ss) \<or> False \<or> xx \<noteq> k \<and> entry_in_tree k v mt)" by (simp add: balance_right_in_tree)
6.861 + thus ?case proof (cases "xx = k")
6.862 + case True
6.863 + from 5 True have "tree_less yy aa \<and> yy < k" by simp
6.864 + hence "tree_less k aa" by (blast dest: tree_less_trans)
6.865 + with 3 5 True show ?thesis by (auto simp: tree_less_nit)
6.866 + qed auto
6.867 +next
6.868 + case ("6_1" xx aa yy ss)
6.869 + show ?case proof (cases "xx = k")
6.870 + case True
6.871 + with "6_1" have "tree_less yy aa \<and> k > yy" by simp
6.872 + hence "tree_less k aa" by (blast dest: tree_less_trans)
6.873 + with "6_1" `xx = k` show ?thesis by (auto simp: tree_less_nit)
6.874 + qed simp
6.875 +next
6.876 + case ("6_2" xx aa yy ss vaa vbb vdd vc)
6.877 + thus ?case proof (cases "xx = k")
6.878 + case True
6.879 + with "6_2" have "k > yy \<and> tree_less yy aa" by simp
6.880 + hence "tree_less k aa" by (blast dest: tree_less_trans)
6.881 + with True "6_2" show ?thesis by (auto simp: tree_less_nit)
6.882 + qed auto
6.883 +qed simp
6.884 +
6.885 +
6.886 +definition delete where
6.887 + delete_def: "delete k t = paint B (del k t)"
6.888 +
6.889 +theorem delete_is_rbt [simp]: assumes "is_rbt t" shows "is_rbt (delete k t)"
6.890 +proof -
6.891 + from assms have "inv2 t" and "inv1 t" unfolding is_rbt_def by auto
6.892 + hence "inv2 (del k t) \<and> (color_of t = R \<and> bheight (del k t) = bheight t \<and> inv1 (del k t) \<or> color_of t = B \<and> bheight (del k t) = bheight t - 1 \<and> inv1l (del k t))" by (rule del_inv1_inv2)
6.893 + hence "inv2 (del k t) \<and> inv1l (del k t)" by (cases "color_of t") auto
6.894 + with assms show ?thesis
6.895 + unfolding is_rbt_def delete_def
6.896 + by (auto intro: paint_sorted del_sorted)
6.897 +qed
6.898 +
6.899 +lemma delete_in_tree:
6.900 + assumes "is_rbt t"
6.901 + shows "entry_in_tree k v (delete x t) = (x \<noteq> k \<and> entry_in_tree k v t)"
6.902 + using assms unfolding is_rbt_def delete_def
6.903 + by (auto simp: del_in_tree)
6.904 +
6.905 +lemma lookup_delete:
6.906 + assumes is_rbt: "is_rbt t"
6.907 + shows "lookup (delete k t) = (lookup t)|`(-{k})"
6.908 +proof
6.909 + fix x
6.910 + show "lookup (delete k t) x = (lookup t |` (-{k})) x"
6.911 + proof (cases "x = k")
6.912 + assume "x = k"
6.913 + with is_rbt show ?thesis
6.914 + by (cases "lookup (delete k t) k") (auto simp: lookup_in_tree delete_in_tree)
6.915 + next
6.916 + assume "x \<noteq> k"
6.917 + thus ?thesis
6.918 + by auto (metis is_rbt delete_is_rbt delete_in_tree is_rbt_sorted lookup_from_in_tree)
6.919 + qed
6.920 +qed
6.921 +
6.922 +
6.923 +subsection {* Union *}
6.924 +
6.925 +primrec
6.926 + union_with_key :: "('a\<Colon>linorder \<Rightarrow> 'b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"
6.927 +where
6.928 + "union_with_key f t Empty = t"
6.929 +| "union_with_key f t (Branch c lt k v rt) = union_with_key f (union_with_key f (insert_with_key f k v t) lt) rt"
6.930 +
6.931 +lemma unionwk_sorted: "sorted lt \<Longrightarrow> sorted (union_with_key f lt rt)"
6.932 + by (induct rt arbitrary: lt) (auto simp: insertwk_sorted)
6.933 +theorem unionwk_is_rbt[simp]: "is_rbt lt \<Longrightarrow> is_rbt (union_with_key f lt rt)"
6.934 + by (induct rt arbitrary: lt) (simp add: insertwk_is_rbt)+
6.935 +
6.936 +definition
6.937 + union_with where
6.938 + "union_with f = union_with_key (\<lambda>_. f)"
6.939 +
6.940 +theorem unionw_is_rbt: "is_rbt lt \<Longrightarrow> is_rbt (union_with f lt rt)" unfolding union_with_def by simp
6.941 +
6.942 +definition union where
6.943 + "union = union_with_key (%_ _ rv. rv)"
6.944 +
6.945 +theorem union_is_rbt: "is_rbt lt \<Longrightarrow> is_rbt (union lt rt)" unfolding union_def by simp
6.946 +
6.947 +lemma union_Branch[simp]:
6.948 + "union t (Branch c lt k v rt) = union (union (insert k v t) lt) rt"
6.949 + unfolding union_def insert_def
6.950 + by simp
6.951 +
6.952 +lemma lookup_union:
6.953 + assumes "is_rbt s" "sorted t"
6.954 + shows "lookup (union s t) = lookup s ++ lookup t"
6.955 +using assms
6.956 +proof (induct t arbitrary: s)
6.957 + case Empty thus ?case by (auto simp: union_def)
6.958 +next
6.959 + case (Branch c l k v r s)
6.960 + then have "sorted r" "sorted l" "l |\<guillemotleft> k" "k \<guillemotleft>| r" by auto
6.961 +
6.962 + have meq: "lookup s(k \<mapsto> v) ++ lookup l ++ lookup r =
6.963 + lookup s ++
6.964 + (\<lambda>a. if a < k then lookup l a
6.965 + else if k < a then lookup r a else Some v)" (is "?m1 = ?m2")
6.966 + proof (rule ext)
6.967 + fix a
6.968 +
6.969 + have "k < a \<or> k = a \<or> k > a" by auto
6.970 + thus "?m1 a = ?m2 a"
6.971 + proof (elim disjE)
6.972 + assume "k < a"
6.973 + with `l |\<guillemotleft> k` have "l |\<guillemotleft> a" by (rule tree_less_trans)
6.974 + with `k < a` show ?thesis
6.975 + by (auto simp: map_add_def split: option.splits)
6.976 + next
6.977 + assume "k = a"
6.978 + with `l |\<guillemotleft> k` `k \<guillemotleft>| r`
6.979 + show ?thesis by (auto simp: map_add_def)
6.980 + next
6.981 + assume "a < k"
6.982 + from this `k \<guillemotleft>| r` have "a \<guillemotleft>| r" by (rule tree_greater_trans)
6.983 + with `a < k` show ?thesis
6.984 + by (auto simp: map_add_def split: option.splits)
6.985 + qed
6.986 + qed
6.987 +
6.988 + from Branch have is_rbt: "is_rbt (RBT_Impl.union (RBT_Impl.insert k v s) l)"
6.989 + by (auto intro: union_is_rbt insert_is_rbt)
6.990 + with Branch have IHs:
6.991 + "lookup (union (union (insert k v s) l) r) = lookup (union (insert k v s) l) ++ lookup r"
6.992 + "lookup (union (insert k v s) l) = lookup (insert k v s) ++ lookup l"
6.993 + by auto
6.994 +
6.995 + with meq show ?case
6.996 + by (auto simp: lookup_insert[OF Branch(3)])
6.997 +
6.998 +qed
6.999 +
6.1000 +
6.1001 +subsection {* Modifying existing entries *}
6.1002 +
6.1003 +primrec
6.1004 + map_entry :: "'a\<Colon>linorder \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt"
6.1005 +where
6.1006 + "map_entry k f Empty = Empty"
6.1007 +| "map_entry k f (Branch c lt x v rt) =
6.1008 + (if k < x then Branch c (map_entry k f lt) x v rt
6.1009 + else if k > x then (Branch c lt x v (map_entry k f rt))
6.1010 + else Branch c lt x (f v) rt)"
6.1011 +
6.1012 +lemma map_entry_color_of: "color_of (map_entry k f t) = color_of t" by (induct t) simp+
6.1013 +lemma map_entry_inv1: "inv1 (map_entry k f t) = inv1 t" by (induct t) (simp add: map_entry_color_of)+
6.1014 +lemma map_entry_inv2: "inv2 (map_entry k f t) = inv2 t" "bheight (map_entry k f t) = bheight t" by (induct t) simp+
6.1015 +lemma map_entry_tree_greater: "tree_greater a (map_entry k f t) = tree_greater a t" by (induct t) simp+
6.1016 +lemma map_entry_tree_less: "tree_less a (map_entry k f t) = tree_less a t" by (induct t) simp+
6.1017 +lemma map_entry_sorted: "sorted (map_entry k f t) = sorted t"
6.1018 + by (induct t) (simp_all add: map_entry_tree_less map_entry_tree_greater)
6.1019 +
6.1020 +theorem map_entry_is_rbt [simp]: "is_rbt (map_entry k f t) = is_rbt t"
6.1021 +unfolding is_rbt_def by (simp add: map_entry_inv2 map_entry_color_of map_entry_sorted map_entry_inv1 )
6.1022 +
6.1023 +theorem lookup_map_entry:
6.1024 + "lookup (map_entry k f t) = (lookup t)(k := Option.map f (lookup t k))"
6.1025 + by (induct t) (auto split: option.splits simp add: expand_fun_eq)
6.1026 +
6.1027 +
6.1028 +subsection {* Mapping all entries *}
6.1029 +
6.1030 +primrec
6.1031 + map :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'c) rbt"
6.1032 +where
6.1033 + "map f Empty = Empty"
6.1034 +| "map f (Branch c lt k v rt) = Branch c (map f lt) k (f k v) (map f rt)"
6.1035 +
6.1036 +lemma map_entries [simp]: "entries (map f t) = List.map (\<lambda>(k, v). (k, f k v)) (entries t)"
6.1037 + by (induct t) auto
6.1038 +lemma map_keys [simp]: "keys (map f t) = keys t" by (simp add: keys_def split_def)
6.1039 +lemma map_tree_greater: "tree_greater k (map f t) = tree_greater k t" by (induct t) simp+
6.1040 +lemma map_tree_less: "tree_less k (map f t) = tree_less k t" by (induct t) simp+
6.1041 +lemma map_sorted: "sorted (map f t) = sorted t" by (induct t) (simp add: map_tree_less map_tree_greater)+
6.1042 +lemma map_color_of: "color_of (map f t) = color_of t" by (induct t) simp+
6.1043 +lemma map_inv1: "inv1 (map f t) = inv1 t" by (induct t) (simp add: map_color_of)+
6.1044 +lemma map_inv2: "inv2 (map f t) = inv2 t" "bheight (map f t) = bheight t" by (induct t) simp+
6.1045 +theorem map_is_rbt [simp]: "is_rbt (map f t) = is_rbt t"
6.1046 +unfolding is_rbt_def by (simp add: map_inv1 map_inv2 map_sorted map_color_of)
6.1047 +
6.1048 +theorem lookup_map: "lookup (map f t) x = Option.map (f x) (lookup t x)"
6.1049 + by (induct t) auto
6.1050 +
6.1051 +
6.1052 +subsection {* Folding over entries *}
6.1053 +
6.1054 +definition fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a, 'b) rbt \<Rightarrow> 'c \<Rightarrow> 'c" where
6.1055 + "fold f t s = foldl (\<lambda>s (k, v). f k v s) s (entries t)"
6.1056 +
6.1057 +lemma fold_simps [simp, code]:
6.1058 + "fold f Empty = id"
6.1059 + "fold f (Branch c lt k v rt) = fold f rt \<circ> f k v \<circ> fold f lt"
6.1060 + by (simp_all add: fold_def expand_fun_eq)
6.1061 +
6.1062 +
6.1063 +subsection {* Bulkloading a tree *}
6.1064 +
6.1065 +definition bulkload :: "('a \<times> 'b) list \<Rightarrow> ('a\<Colon>linorder, 'b) rbt" where
6.1066 + "bulkload xs = foldr (\<lambda>(k, v). insert k v) xs Empty"
6.1067 +
6.1068 +lemma bulkload_is_rbt [simp, intro]:
6.1069 + "is_rbt (bulkload xs)"
6.1070 + unfolding bulkload_def by (induct xs) auto
6.1071 +
6.1072 +lemma lookup_bulkload:
6.1073 + "lookup (bulkload xs) = map_of xs"
6.1074 +proof -
6.1075 + obtain ys where "ys = rev xs" by simp
6.1076 + have "\<And>t. is_rbt t \<Longrightarrow>
6.1077 + lookup (foldl (\<lambda>t (k, v). insert k v t) t ys) = lookup t ++ map_of (rev ys)"
6.1078 + by (induct ys) (simp_all add: bulkload_def split_def lookup_insert)
6.1079 + from this Empty_is_rbt have
6.1080 + "lookup (foldl (\<lambda>t (k, v). insert k v t) Empty (rev xs)) = lookup Empty ++ map_of xs"
6.1081 + by (simp add: `ys = rev xs`)
6.1082 + then show ?thesis by (simp add: bulkload_def foldl_foldr lookup_Empty split_def)
6.1083 +qed
6.1084 +
6.1085 +hide (open) const Empty insert delete entries keys bulkload lookup map_entry map fold union sorted
6.1086 +
6.1087 +end
7.1 --- a/src/HOL/Library/Table.thy Wed Apr 14 22:18:10 2010 +0200
7.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
7.3 @@ -1,229 +0,0 @@
7.4 -(* Author: Florian Haftmann, TU Muenchen *)
7.5 -
7.6 -header {* Tables: finite mappings implemented by red-black trees *}
7.7 -
7.8 -theory Table
7.9 -imports Main RBT Mapping
7.10 -begin
7.11 -
7.12 -subsection {* Type definition *}
7.13 -
7.14 -typedef (open) ('a, 'b) table = "{t :: ('a\<Colon>linorder, 'b) rbt. is_rbt t}"
7.15 - morphisms tree_of Table
7.16 -proof -
7.17 - have "RBT.Empty \<in> ?table" by simp
7.18 - then show ?thesis ..
7.19 -qed
7.20 -
7.21 -lemma is_rbt_tree_of [simp, intro]:
7.22 - "is_rbt (tree_of t)"
7.23 - using tree_of [of t] by simp
7.24 -
7.25 -lemma table_eq:
7.26 - "t1 = t2 \<longleftrightarrow> tree_of t1 = tree_of t2"
7.27 - by (simp add: tree_of_inject)
7.28 -
7.29 -lemma [code abstype]:
7.30 - "Table (tree_of t) = t"
7.31 - by (simp add: tree_of_inverse)
7.32 -
7.33 -
7.34 -subsection {* Primitive operations *}
7.35 -
7.36 -definition lookup :: "('a\<Colon>linorder, 'b) table \<Rightarrow> 'a \<rightharpoonup> 'b" where
7.37 - [code]: "lookup t = RBT.lookup (tree_of t)"
7.38 -
7.39 -definition empty :: "('a\<Colon>linorder, 'b) table" where
7.40 - "empty = Table RBT.Empty"
7.41 -
7.42 -lemma tree_of_empty [code abstract]:
7.43 - "tree_of empty = RBT.Empty"
7.44 - by (simp add: empty_def Table_inverse)
7.45 -
7.46 -definition update :: "'a\<Colon>linorder \<Rightarrow> 'b \<Rightarrow> ('a, 'b) table \<Rightarrow> ('a, 'b) table" where
7.47 - "update k v t = Table (RBT.insert k v (tree_of t))"
7.48 -
7.49 -lemma tree_of_update [code abstract]:
7.50 - "tree_of (update k v t) = RBT.insert k v (tree_of t)"
7.51 - by (simp add: update_def Table_inverse)
7.52 -
7.53 -definition delete :: "'a\<Colon>linorder \<Rightarrow> ('a, 'b) table \<Rightarrow> ('a, 'b) table" where
7.54 - "delete k t = Table (RBT.delete k (tree_of t))"
7.55 -
7.56 -lemma tree_of_delete [code abstract]:
7.57 - "tree_of (delete k t) = RBT.delete k (tree_of t)"
7.58 - by (simp add: delete_def Table_inverse)
7.59 -
7.60 -definition entries :: "('a\<Colon>linorder, 'b) table \<Rightarrow> ('a \<times> 'b) list" where
7.61 - [code]: "entries t = RBT.entries (tree_of t)"
7.62 -
7.63 -definition keys :: "('a\<Colon>linorder, 'b) table \<Rightarrow> 'a list" where
7.64 - [code]: "keys t = RBT.keys (tree_of t)"
7.65 -
7.66 -definition bulkload :: "('a\<Colon>linorder \<times> 'b) list \<Rightarrow> ('a, 'b) table" where
7.67 - "bulkload xs = Table (RBT.bulkload xs)"
7.68 -
7.69 -lemma tree_of_bulkload [code abstract]:
7.70 - "tree_of (bulkload xs) = RBT.bulkload xs"
7.71 - by (simp add: bulkload_def Table_inverse)
7.72 -
7.73 -definition map_entry :: "'a \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a\<Colon>linorder, 'b) table \<Rightarrow> ('a, 'b) table" where
7.74 - "map_entry k f t = Table (RBT.map_entry k f (tree_of t))"
7.75 -
7.76 -lemma tree_of_map_entry [code abstract]:
7.77 - "tree_of (map_entry k f t) = RBT.map_entry k f (tree_of t)"
7.78 - by (simp add: map_entry_def Table_inverse)
7.79 -
7.80 -definition map :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a\<Colon>linorder, 'b) table \<Rightarrow> ('a, 'b) table" where
7.81 - "map f t = Table (RBT.map f (tree_of t))"
7.82 -
7.83 -lemma tree_of_map [code abstract]:
7.84 - "tree_of (map f t) = RBT.map f (tree_of t)"
7.85 - by (simp add: map_def Table_inverse)
7.86 -
7.87 -definition fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a\<Colon>linorder, 'b) table \<Rightarrow> 'c \<Rightarrow> 'c" where
7.88 - [code]: "fold f t = RBT.fold f (tree_of t)"
7.89 -
7.90 -
7.91 -subsection {* Derived operations *}
7.92 -
7.93 -definition is_empty :: "('a\<Colon>linorder, 'b) table \<Rightarrow> bool" where
7.94 - [code]: "is_empty t = (case tree_of t of RBT.Empty \<Rightarrow> True | _ \<Rightarrow> False)"
7.95 -
7.96 -
7.97 -subsection {* Abstract lookup properties *}
7.98 -
7.99 -lemma lookup_Table:
7.100 - "is_rbt t \<Longrightarrow> lookup (Table t) = RBT.lookup t"
7.101 - by (simp add: lookup_def Table_inverse)
7.102 -
7.103 -lemma lookup_tree_of:
7.104 - "RBT.lookup (tree_of t) = lookup t"
7.105 - by (simp add: lookup_def)
7.106 -
7.107 -lemma entries_tree_of:
7.108 - "RBT.entries (tree_of t) = entries t"
7.109 - by (simp add: entries_def)
7.110 -
7.111 -lemma keys_tree_of:
7.112 - "RBT.keys (tree_of t) = keys t"
7.113 - by (simp add: keys_def)
7.114 -
7.115 -lemma lookup_empty [simp]:
7.116 - "lookup empty = Map.empty"
7.117 - by (simp add: empty_def lookup_Table expand_fun_eq)
7.118 -
7.119 -lemma lookup_update [simp]:
7.120 - "lookup (update k v t) = (lookup t)(k \<mapsto> v)"
7.121 - by (simp add: update_def lookup_Table lookup_insert lookup_tree_of)
7.122 -
7.123 -lemma lookup_delete [simp]:
7.124 - "lookup (delete k t) = (lookup t)(k := None)"
7.125 - by (simp add: delete_def lookup_Table RBT.lookup_delete lookup_tree_of restrict_complement_singleton_eq)
7.126 -
7.127 -lemma map_of_entries [simp]:
7.128 - "map_of (entries t) = lookup t"
7.129 - by (simp add: entries_def map_of_entries lookup_tree_of)
7.130 -
7.131 -lemma entries_lookup:
7.132 - "entries t1 = entries t2 \<longleftrightarrow> lookup t1 = lookup t2"
7.133 - by (simp add: entries_def lookup_def entries_lookup)
7.134 -
7.135 -lemma lookup_bulkload [simp]:
7.136 - "lookup (bulkload xs) = map_of xs"
7.137 - by (simp add: bulkload_def lookup_Table RBT.lookup_bulkload)
7.138 -
7.139 -lemma lookup_map_entry [simp]:
7.140 - "lookup (map_entry k f t) = (lookup t)(k := Option.map f (lookup t k))"
7.141 - by (simp add: map_entry_def lookup_Table lookup_map_entry lookup_tree_of)
7.142 -
7.143 -lemma lookup_map [simp]:
7.144 - "lookup (map f t) k = Option.map (f k) (lookup t k)"
7.145 - by (simp add: map_def lookup_Table lookup_map lookup_tree_of)
7.146 -
7.147 -lemma fold_fold:
7.148 - "fold f t = (\<lambda>s. foldl (\<lambda>s (k, v). f k v s) s (entries t))"
7.149 - by (simp add: fold_def expand_fun_eq RBT.fold_def entries_tree_of)
7.150 -
7.151 -lemma is_empty_empty [simp]:
7.152 - "is_empty t \<longleftrightarrow> t = empty"
7.153 - by (simp add: table_eq is_empty_def tree_of_empty split: rbt.split)
7.154 -
7.155 -lemma RBT_lookup_empty [simp]: (*FIXME*)
7.156 - "RBT.lookup t = Map.empty \<longleftrightarrow> t = RBT.Empty"
7.157 - by (cases t) (auto simp add: expand_fun_eq)
7.158 -
7.159 -lemma lookup_empty_empty [simp]:
7.160 - "lookup t = Map.empty \<longleftrightarrow> t = empty"
7.161 - by (cases t) (simp add: empty_def lookup_def Table_inject Table_inverse)
7.162 -
7.163 -lemma sorted_keys [iff]:
7.164 - "sorted (keys t)"
7.165 - by (simp add: keys_def RBT.keys_def sorted_entries)
7.166 -
7.167 -lemma distinct_keys [iff]:
7.168 - "distinct (keys t)"
7.169 - by (simp add: keys_def RBT.keys_def distinct_entries)
7.170 -
7.171 -
7.172 -subsection {* Implementation of mappings *}
7.173 -
7.174 -definition Mapping :: "('a\<Colon>linorder, 'b) table \<Rightarrow> ('a, 'b) mapping" where
7.175 - "Mapping t = Mapping.Mapping (lookup t)"
7.176 -
7.177 -code_datatype Mapping
7.178 -
7.179 -lemma lookup_Mapping [simp, code]:
7.180 - "Mapping.lookup (Mapping t) = lookup t"
7.181 - by (simp add: Mapping_def)
7.182 -
7.183 -lemma empty_Mapping [code]:
7.184 - "Mapping.empty = Mapping empty"
7.185 - by (rule mapping_eqI) simp
7.186 -
7.187 -lemma is_empty_Mapping [code]:
7.188 - "Mapping.is_empty (Mapping t) \<longleftrightarrow> is_empty t"
7.189 - by (simp add: table_eq Mapping.is_empty_empty Mapping_def)
7.190 -
7.191 -lemma update_Mapping [code]:
7.192 - "Mapping.update k v (Mapping t) = Mapping (update k v t)"
7.193 - by (rule mapping_eqI) simp
7.194 -
7.195 -lemma delete_Mapping [code]:
7.196 - "Mapping.delete k (Mapping xs) = Mapping (delete k xs)"
7.197 - by (rule mapping_eqI) simp
7.198 -
7.199 -lemma keys_Mapping [code]:
7.200 - "Mapping.keys (Mapping t) = set (keys t)"
7.201 - by (simp add: keys_def Mapping_def Mapping.keys_def lookup_def lookup_keys)
7.202 -
7.203 -lemma ordered_keys_Mapping [code]:
7.204 - "Mapping.ordered_keys (Mapping t) = keys t"
7.205 - by (rule sorted_distinct_set_unique) (simp_all add: ordered_keys_def keys_Mapping)
7.206 -
7.207 -lemma Mapping_size_card_keys: (*FIXME*)
7.208 - "Mapping.size m = card (Mapping.keys m)"
7.209 - by (simp add: Mapping.size_def Mapping.keys_def)
7.210 -
7.211 -lemma size_Mapping [code]:
7.212 - "Mapping.size (Mapping t) = length (keys t)"
7.213 - by (simp add: Mapping_size_card_keys keys_Mapping distinct_card)
7.214 -
7.215 -lemma tabulate_Mapping [code]:
7.216 - "Mapping.tabulate ks f = Mapping (bulkload (List.map (\<lambda>k. (k, f k)) ks))"
7.217 - by (rule mapping_eqI) (simp add: map_of_map_restrict)
7.218 -
7.219 -lemma bulkload_Mapping [code]:
7.220 - "Mapping.bulkload vs = Mapping (bulkload (List.map (\<lambda>n. (n, vs ! n)) [0..<length vs]))"
7.221 - by (rule mapping_eqI) (simp add: map_of_map_restrict expand_fun_eq)
7.222 -
7.223 -lemma [code, code del]: "HOL.eq (x :: (_, _) mapping) y \<longleftrightarrow> x = y" by (fact eq_equals) (*FIXME*)
7.224 -
7.225 -lemma eq_Mapping [code]:
7.226 - "HOL.eq (Mapping t1) (Mapping t2) \<longleftrightarrow> entries t1 = entries t2"
7.227 - by (simp add: eq Mapping_def entries_lookup)
7.228 -
7.229 -hide (open) const tree_of lookup empty update delete
7.230 - entries keys bulkload map_entry map fold
7.231 -
7.232 -end
8.1 --- a/src/HOL/ex/Codegenerator_Candidates.thy Wed Apr 14 22:18:10 2010 +0200
8.2 +++ b/src/HOL/ex/Codegenerator_Candidates.thy Thu Apr 15 12:27:14 2010 +0200
8.3 @@ -20,8 +20,8 @@
8.4 "~~/src/HOL/Number_Theory/Primes"
8.5 Product_ord
8.6 "~~/src/HOL/ex/Records"
8.7 + RBT
8.8 SetsAndFunctions
8.9 - Table
8.10 While_Combinator
8.11 Word
8.12 begin