Automated merge with ssh://macbroy25.informatik.tu-muenchen.de//home/isabelle-repository/repos/isabelle
1.1 --- a/NEWS Fri Apr 13 12:09:25 2012 +0200
1.2 +++ b/NEWS Fri Apr 13 13:30:27 2012 +0200
1.3 @@ -338,6 +338,116 @@
1.4 * Theory HOL/Library/Diagonalize has been removed. INCOMPATIBILITY,
1.5 use theory HOL/Library/Nat_Bijection instead.
1.6
1.7 +* Theory HOL/Library/RBT_Impl: Backing implementation of red-black trees is
1.8 +now inside the type class' local context. Names of affected operations and lemmas
1.9 +have been prefixed by rbt_. INCOMPATIBILITY for theories working directly with
1.10 +raw red-black trees, adapt the names as follows:
1.11 +
1.12 + Operations:
1.13 + bulkload -> rbt_bulkload
1.14 + del_from_left -> rbt_del_from_left
1.15 + del_from_right -> rbt_del_from_right
1.16 + del -> rbt_del
1.17 + delete -> rbt_delete
1.18 + ins -> rbt_ins
1.19 + insert -> rbt_insert
1.20 + insertw -> rbt_insert_with
1.21 + insert_with_key -> rbt_insert_with_key
1.22 + map_entry -> rbt_map_entry
1.23 + lookup -> rbt_lookup
1.24 + sorted -> rbt_sorted
1.25 + tree_greater -> rbt_greater
1.26 + tree_less -> rbt_less
1.27 + tree_less_symbol -> rbt_less_symbol
1.28 + union -> rbt_union
1.29 + union_with -> rbt_union_with
1.30 + union_with_key -> rbt_union_with_key
1.31 +
1.32 + Lemmas:
1.33 + balance_left_sorted -> balance_left_rbt_sorted
1.34 + balance_left_tree_greater -> balance_left_rbt_greater
1.35 + balance_left_tree_less -> balance_left_rbt_less
1.36 + balance_right_sorted -> balance_right_rbt_sorted
1.37 + balance_right_tree_greater -> balance_right_rbt_greater
1.38 + balance_right_tree_less -> balance_right_rbt_less
1.39 + balance_sorted -> balance_rbt_sorted
1.40 + balance_tree_greater -> balance_rbt_greater
1.41 + balance_tree_less -> balance_rbt_less
1.42 + bulkload_is_rbt -> rbt_bulkload_is_rbt
1.43 + combine_sorted -> combine_rbt_sorted
1.44 + combine_tree_greater -> combine_rbt_greater
1.45 + combine_tree_less -> combine_rbt_less
1.46 + delete_in_tree -> rbt_delete_in_tree
1.47 + delete_is_rbt -> rbt_delete_is_rbt
1.48 + del_from_left_tree_greater -> rbt_del_from_left_rbt_greater
1.49 + del_from_left_tree_less -> rbt_del_from_left_rbt_less
1.50 + del_from_right_tree_greater -> rbt_del_from_right_rbt_greater
1.51 + del_from_right_tree_less -> rbt_del_from_right_rbt_less
1.52 + del_in_tree -> rbt_del_in_tree
1.53 + del_inv1_inv2 -> rbt_del_inv1_inv2
1.54 + del_sorted -> rbt_del_rbt_sorted
1.55 + del_tree_greater -> rbt_del_rbt_greater
1.56 + del_tree_less -> rbt_del_rbt_less
1.57 + dom_lookup_Branch -> dom_rbt_lookup_Branch
1.58 + entries_lookup -> entries_rbt_lookup
1.59 + finite_dom_lookup -> finite_dom_rbt_lookup
1.60 + insert_sorted -> rbt_insert_rbt_sorted
1.61 + insertw_is_rbt -> rbt_insertw_is_rbt
1.62 + insertwk_is_rbt -> rbt_insertwk_is_rbt
1.63 + insertwk_sorted -> rbt_insertwk_rbt_sorted
1.64 + insertw_sorted -> rbt_insertw_rbt_sorted
1.65 + ins_sorted -> ins_rbt_sorted
1.66 + ins_tree_greater -> ins_rbt_greater
1.67 + ins_tree_less -> ins_rbt_less
1.68 + is_rbt_sorted -> is_rbt_rbt_sorted
1.69 + lookup_balance -> rbt_lookup_balance
1.70 + lookup_bulkload -> rbt_lookup_rbt_bulkload
1.71 + lookup_delete -> rbt_lookup_rbt_delete
1.72 + lookup_Empty -> rbt_lookup_Empty
1.73 + lookup_from_in_tree -> rbt_lookup_from_in_tree
1.74 + lookup_in_tree -> rbt_lookup_in_tree
1.75 + lookup_ins -> rbt_lookup_ins
1.76 + lookup_insert -> rbt_lookup_rbt_insert
1.77 + lookup_insertw -> rbt_lookup_rbt_insertw
1.78 + lookup_insertwk -> rbt_lookup_rbt_insertwk
1.79 + lookup_keys -> rbt_lookup_keys
1.80 + lookup_map -> rbt_lookup_map
1.81 + lookup_map_entry -> rbt_lookup_rbt_map_entry
1.82 + lookup_tree_greater -> rbt_lookup_rbt_greater
1.83 + lookup_tree_less -> rbt_lookup_rbt_less
1.84 + lookup_union -> rbt_lookup_rbt_union
1.85 + map_entry_color_of -> rbt_map_entry_color_of
1.86 + map_entry_inv1 -> rbt_map_entry_inv1
1.87 + map_entry_inv2 -> rbt_map_entry_inv2
1.88 + map_entry_is_rbt -> rbt_map_entry_is_rbt
1.89 + map_entry_sorted -> rbt_map_entry_rbt_sorted
1.90 + map_entry_tree_greater -> rbt_map_entry_rbt_greater
1.91 + map_entry_tree_less -> rbt_map_entry_rbt_less
1.92 + map_tree_greater -> map_rbt_greater
1.93 + map_tree_less -> map_rbt_less
1.94 + map_sorted -> map_rbt_sorted
1.95 + paint_sorted -> paint_rbt_sorted
1.96 + paint_lookup -> paint_rbt_lookup
1.97 + paint_tree_greater -> paint_rbt_greater
1.98 + paint_tree_less -> paint_rbt_less
1.99 + sorted_entries -> rbt_sorted_entries
1.100 + tree_greater_eq_trans -> rbt_greater_eq_trans
1.101 + tree_greater_nit -> rbt_greater_nit
1.102 + tree_greater_prop -> rbt_greater_prop
1.103 + tree_greater_simps -> rbt_greater_simps
1.104 + tree_greater_trans -> rbt_greater_trans
1.105 + tree_less_eq_trans -> rbt_less_eq_trans
1.106 + tree_less_nit -> rbt_less_nit
1.107 + tree_less_prop -> rbt_less_prop
1.108 + tree_less_simps -> rbt_less_simps
1.109 + tree_less_trans -> rbt_less_trans
1.110 + tree_ord_props -> rbt_ord_props
1.111 + union_Branch -> rbt_union_Branch
1.112 + union_is_rbt -> rbt_union_is_rbt
1.113 + unionw_is_rbt -> rbt_unionw_is_rbt
1.114 + unionwk_is_rbt -> rbt_unionwk_is_rbt
1.115 + unionwk_sorted -> rbt_unionwk_rbt_sorted
1.116 +
1.117 * Session HOL-Word: Discontinued many redundant theorems specific to
1.118 type 'a word. INCOMPATIBILITY, use the corresponding generic theorems
1.119 instead.
2.1 --- a/src/HOL/Imperative_HOL/ex/SatChecker.thy Fri Apr 13 12:09:25 2012 +0200
2.2 +++ b/src/HOL/Imperative_HOL/ex/SatChecker.thy Fri Apr 13 13:30:27 2012 +0200
2.3 @@ -675,21 +675,21 @@
2.4 primrec tres_thm :: "(ClauseId, Clause) RBT_Impl.rbt \<Rightarrow> Lit \<times> ClauseId \<Rightarrow> Clause \<Rightarrow> Clause Heap"
2.5 where
2.6 "tres_thm t (l, j) cli =
2.7 - (case (RBT_Impl.lookup t j) of
2.8 + (case (rbt_lookup t j) of
2.9 None \<Rightarrow> raise (''MiniSatChecked.res_thm: No resolvant clause in thms array for Conflict step.'')
2.10 | Some clj \<Rightarrow> res_thm' l cli clj)"
2.11
2.12 fun tdoProofStep :: " ProofStep \<Rightarrow> ((ClauseId, Clause) RBT_Impl.rbt * Clause list) \<Rightarrow> ((ClauseId, Clause) RBT_Impl.rbt * Clause list) Heap"
2.13 where
2.14 "tdoProofStep (Conflict saveTo (i, rs)) (t, rcl) =
2.15 - (case (RBT_Impl.lookup t i) of
2.16 + (case (rbt_lookup t i) of
2.17 None \<Rightarrow> raise (''MiniSatChecked.doProofStep: No starting clause in thms array for Conflict step.'')
2.18 | Some cli \<Rightarrow> do {
2.19 result \<leftarrow> foldM (tres_thm t) rs cli;
2.20 - return ((RBT_Impl.insert saveTo result t), rcl)
2.21 + return ((rbt_insert saveTo result t), rcl)
2.22 })"
2.23 -| "tdoProofStep (Delete cid) (t, rcl) = return ((RBT_Impl.delete cid t), rcl)"
2.24 -| "tdoProofStep (Root cid clause) (t, rcl) = return (RBT_Impl.insert cid (sort clause) t, (remdups(sort clause)) # rcl)"
2.25 +| "tdoProofStep (Delete cid) (t, rcl) = return ((rbt_delete cid t), rcl)"
2.26 +| "tdoProofStep (Root cid clause) (t, rcl) = return (rbt_insert cid (sort clause) t, (remdups(sort clause)) # rcl)"
2.27 | "tdoProofStep (Xstep cid1 cid2) (t, rcl) = raise ''MiniSatChecked.doProofStep: Xstep constructor found.''"
2.28 | "tdoProofStep (ProofDone b) (t, rcl) = raise ''MiniSatChecked.doProofStep: ProofDone constructor found.''"
2.29
2.30 @@ -698,7 +698,7 @@
2.31 "tchecker n p i =
2.32 do {
2.33 rcs \<leftarrow> foldM (tdoProofStep) p (RBT_Impl.Empty, []);
2.34 - (if (RBT_Impl.lookup (fst rcs) i) = Some [] then return (snd rcs)
2.35 + (if (rbt_lookup (fst rcs) i) = Some [] then return (snd rcs)
2.36 else raise(''No empty clause''))
2.37 }"
2.38
3.1 --- a/src/HOL/Library/RBT.thy Fri Apr 13 12:09:25 2012 +0200
3.2 +++ b/src/HOL/Library/RBT.thy Fri Apr 13 13:30:27 2012 +0200
3.3 @@ -35,7 +35,7 @@
3.4 subsection {* Primitive operations *}
3.5
3.6 definition lookup :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'a \<rightharpoonup> 'b" where
3.7 - [code]: "lookup t = RBT_Impl.lookup (impl_of t)"
3.8 + [code]: "lookup t = rbt_lookup (impl_of t)"
3.9
3.10 definition empty :: "('a\<Colon>linorder, 'b) rbt" where
3.11 "empty = RBT RBT_Impl.Empty"
3.12 @@ -45,17 +45,17 @@
3.13 by (simp add: empty_def RBT_inverse)
3.14
3.15 definition insert :: "'a\<Colon>linorder \<Rightarrow> 'b \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt" where
3.16 - "insert k v t = RBT (RBT_Impl.insert k v (impl_of t))"
3.17 + "insert k v t = RBT (rbt_insert k v (impl_of t))"
3.18
3.19 lemma impl_of_insert [code abstract]:
3.20 - "impl_of (insert k v t) = RBT_Impl.insert k v (impl_of t)"
3.21 + "impl_of (insert k v t) = rbt_insert k v (impl_of t)"
3.22 by (simp add: insert_def RBT_inverse)
3.23
3.24 definition delete :: "'a\<Colon>linorder \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt" where
3.25 - "delete k t = RBT (RBT_Impl.delete k (impl_of t))"
3.26 + "delete k t = RBT (rbt_delete k (impl_of t))"
3.27
3.28 lemma impl_of_delete [code abstract]:
3.29 - "impl_of (delete k t) = RBT_Impl.delete k (impl_of t)"
3.30 + "impl_of (delete k t) = rbt_delete k (impl_of t)"
3.31 by (simp add: delete_def RBT_inverse)
3.32
3.33 definition entries :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a \<times> 'b) list" where
3.34 @@ -65,17 +65,17 @@
3.35 [code]: "keys t = RBT_Impl.keys (impl_of t)"
3.36
3.37 definition bulkload :: "('a\<Colon>linorder \<times> 'b) list \<Rightarrow> ('a, 'b) rbt" where
3.38 - "bulkload xs = RBT (RBT_Impl.bulkload xs)"
3.39 + "bulkload xs = RBT (rbt_bulkload xs)"
3.40
3.41 lemma impl_of_bulkload [code abstract]:
3.42 - "impl_of (bulkload xs) = RBT_Impl.bulkload xs"
3.43 + "impl_of (bulkload xs) = rbt_bulkload xs"
3.44 by (simp add: bulkload_def RBT_inverse)
3.45
3.46 definition map_entry :: "'a \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a, 'b) rbt" where
3.47 - "map_entry k f t = RBT (RBT_Impl.map_entry k f (impl_of t))"
3.48 + "map_entry k f t = RBT (rbt_map_entry k f (impl_of t))"
3.49
3.50 lemma impl_of_map_entry [code abstract]:
3.51 - "impl_of (map_entry k f t) = RBT_Impl.map_entry k f (impl_of t)"
3.52 + "impl_of (map_entry k f t) = rbt_map_entry k f (impl_of t)"
3.53 by (simp add: map_entry_def RBT_inverse)
3.54
3.55 definition map :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a, 'b) rbt" where
3.56 @@ -98,11 +98,11 @@
3.57 subsection {* Abstract lookup properties *}
3.58
3.59 lemma lookup_RBT:
3.60 - "is_rbt t \<Longrightarrow> lookup (RBT t) = RBT_Impl.lookup t"
3.61 + "is_rbt t \<Longrightarrow> lookup (RBT t) = rbt_lookup t"
3.62 by (simp add: lookup_def RBT_inverse)
3.63
3.64 lemma lookup_impl_of:
3.65 - "RBT_Impl.lookup (impl_of t) = lookup t"
3.66 + "rbt_lookup (impl_of t) = lookup t"
3.67 by (simp add: lookup_def)
3.68
3.69 lemma entries_impl_of:
3.70 @@ -119,11 +119,11 @@
3.71
3.72 lemma lookup_insert [simp]:
3.73 "lookup (insert k v t) = (lookup t)(k \<mapsto> v)"
3.74 - by (simp add: insert_def lookup_RBT lookup_insert lookup_impl_of)
3.75 + by (simp add: insert_def lookup_RBT rbt_lookup_rbt_insert lookup_impl_of)
3.76
3.77 lemma lookup_delete [simp]:
3.78 "lookup (delete k t) = (lookup t)(k := None)"
3.79 - by (simp add: delete_def lookup_RBT RBT_Impl.lookup_delete lookup_impl_of restrict_complement_singleton_eq)
3.80 + by (simp add: delete_def lookup_RBT rbt_lookup_rbt_delete lookup_impl_of restrict_complement_singleton_eq)
3.81
3.82 lemma map_of_entries [simp]:
3.83 "map_of (entries t) = lookup t"
3.84 @@ -131,19 +131,19 @@
3.85
3.86 lemma entries_lookup:
3.87 "entries t1 = entries t2 \<longleftrightarrow> lookup t1 = lookup t2"
3.88 - by (simp add: entries_def lookup_def entries_lookup)
3.89 + by (simp add: entries_def lookup_def entries_rbt_lookup)
3.90
3.91 lemma lookup_bulkload [simp]:
3.92 "lookup (bulkload xs) = map_of xs"
3.93 - by (simp add: bulkload_def lookup_RBT RBT_Impl.lookup_bulkload)
3.94 + by (simp add: bulkload_def lookup_RBT rbt_lookup_rbt_bulkload)
3.95
3.96 lemma lookup_map_entry [simp]:
3.97 "lookup (map_entry k f t) = (lookup t)(k := Option.map f (lookup t k))"
3.98 - by (simp add: map_entry_def lookup_RBT RBT_Impl.lookup_map_entry lookup_impl_of)
3.99 + by (simp add: map_entry_def lookup_RBT rbt_lookup_rbt_map_entry lookup_impl_of)
3.100
3.101 lemma lookup_map [simp]:
3.102 "lookup (map f t) k = Option.map (f k) (lookup t k)"
3.103 - by (simp add: map_def lookup_RBT RBT_Impl.lookup_map lookup_impl_of)
3.104 + by (simp add: map_def lookup_RBT rbt_lookup_map lookup_impl_of)
3.105
3.106 lemma fold_fold:
3.107 "fold f t = List.fold (prod_case f) (entries t)"
3.108 @@ -154,7 +154,7 @@
3.109 by (simp add: rbt_eq_iff is_empty_def impl_of_empty split: rbt.split)
3.110
3.111 lemma RBT_lookup_empty [simp]: (*FIXME*)
3.112 - "RBT_Impl.lookup t = Map.empty \<longleftrightarrow> t = RBT_Impl.Empty"
3.113 + "rbt_lookup t = Map.empty \<longleftrightarrow> t = RBT_Impl.Empty"
3.114 by (cases t) (auto simp add: fun_eq_iff)
3.115
3.116 lemma lookup_empty_empty [simp]:
3.117 @@ -163,7 +163,7 @@
3.118
3.119 lemma sorted_keys [iff]:
3.120 "sorted (keys t)"
3.121 - by (simp add: keys_def RBT_Impl.keys_def sorted_entries)
3.122 + by (simp add: keys_def RBT_Impl.keys_def rbt_sorted_entries)
3.123
3.124 lemma distinct_keys [iff]:
3.125 "distinct (keys t)"
4.1 --- a/src/HOL/Library/RBT_Impl.thy Fri Apr 13 12:09:25 2012 +0200
4.2 +++ b/src/HOL/Library/RBT_Impl.thy Fri Apr 13 13:30:27 2012 +0200
4.3 @@ -1,4 +1,4 @@
4.4 -(* Title: HOL/Library/RBT_Impl.thy
4.5 +(* Title: RBT_Impl.thy
4.6 Author: Markus Reiter, TU Muenchen
4.7 Author: Alexander Krauss, TU Muenchen
4.8 *)
4.9 @@ -65,202 +65,221 @@
4.10
4.11 subsubsection {* Search tree properties *}
4.12
4.13 -definition tree_less :: "'a\<Colon>order \<Rightarrow> ('a, 'b) rbt \<Rightarrow> bool"
4.14 +context ord begin
4.15 +
4.16 +definition rbt_less :: "'a \<Rightarrow> ('a, 'b) rbt \<Rightarrow> bool"
4.17 where
4.18 - tree_less_prop: "tree_less k t \<longleftrightarrow> (\<forall>x\<in>set (keys t). x < k)"
4.19 + rbt_less_prop: "rbt_less k t \<longleftrightarrow> (\<forall>x\<in>set (keys t). x < k)"
4.20
4.21 -abbreviation tree_less_symbol (infix "|\<guillemotleft>" 50)
4.22 -where "t |\<guillemotleft> x \<equiv> tree_less x t"
4.23 +abbreviation rbt_less_symbol (infix "|\<guillemotleft>" 50)
4.24 +where "t |\<guillemotleft> x \<equiv> rbt_less x t"
4.25
4.26 -definition tree_greater :: "'a\<Colon>order \<Rightarrow> ('a, 'b) rbt \<Rightarrow> bool" (infix "\<guillemotleft>|" 50)
4.27 +definition rbt_greater :: "'a \<Rightarrow> ('a, 'b) rbt \<Rightarrow> bool" (infix "\<guillemotleft>|" 50)
4.28 where
4.29 - tree_greater_prop: "tree_greater k t = (\<forall>x\<in>set (keys t). k < x)"
4.30 + rbt_greater_prop: "rbt_greater k t = (\<forall>x\<in>set (keys t). k < x)"
4.31
4.32 -lemma tree_less_simps [simp]:
4.33 - "tree_less k Empty = True"
4.34 - "tree_less k (Branch c lt kt v rt) \<longleftrightarrow> kt < k \<and> tree_less k lt \<and> tree_less k rt"
4.35 - by (auto simp add: tree_less_prop)
4.36 +lemma rbt_less_simps [simp]:
4.37 + "Empty |\<guillemotleft> k = True"
4.38 + "Branch c lt kt v rt |\<guillemotleft> k \<longleftrightarrow> kt < k \<and> lt |\<guillemotleft> k \<and> rt |\<guillemotleft> k"
4.39 + by (auto simp add: rbt_less_prop)
4.40
4.41 -lemma tree_greater_simps [simp]:
4.42 - "tree_greater k Empty = True"
4.43 - "tree_greater k (Branch c lt kt v rt) \<longleftrightarrow> k < kt \<and> tree_greater k lt \<and> tree_greater k rt"
4.44 - by (auto simp add: tree_greater_prop)
4.45 +lemma rbt_greater_simps [simp]:
4.46 + "k \<guillemotleft>| Empty = True"
4.47 + "k \<guillemotleft>| (Branch c lt kt v rt) \<longleftrightarrow> k < kt \<and> k \<guillemotleft>| lt \<and> k \<guillemotleft>| rt"
4.48 + by (auto simp add: rbt_greater_prop)
4.49
4.50 -lemmas tree_ord_props = tree_less_prop tree_greater_prop
4.51 +lemmas rbt_ord_props = rbt_less_prop rbt_greater_prop
4.52
4.53 -lemmas tree_greater_nit = tree_greater_prop entry_in_tree_keys
4.54 -lemmas tree_less_nit = tree_less_prop entry_in_tree_keys
4.55 +lemmas rbt_greater_nit = rbt_greater_prop entry_in_tree_keys
4.56 +lemmas rbt_less_nit = rbt_less_prop entry_in_tree_keys
4.57
4.58 -lemma tree_less_eq_trans: "l |\<guillemotleft> u \<Longrightarrow> u \<le> v \<Longrightarrow> l |\<guillemotleft> v"
4.59 - and tree_less_trans: "t |\<guillemotleft> x \<Longrightarrow> x < y \<Longrightarrow> t |\<guillemotleft> y"
4.60 - and tree_greater_eq_trans: "u \<le> v \<Longrightarrow> v \<guillemotleft>| r \<Longrightarrow> u \<guillemotleft>| r"
4.61 - and tree_greater_trans: "x < y \<Longrightarrow> y \<guillemotleft>| t \<Longrightarrow> x \<guillemotleft>| t"
4.62 - by (auto simp: tree_ord_props)
4.63 +lemma (in order)
4.64 + shows rbt_less_eq_trans: "l |\<guillemotleft> u \<Longrightarrow> u \<le> v \<Longrightarrow> l |\<guillemotleft> v"
4.65 + and rbt_less_trans: "t |\<guillemotleft> x \<Longrightarrow> x < y \<Longrightarrow> t |\<guillemotleft> y"
4.66 + and rbt_greater_eq_trans: "u \<le> v \<Longrightarrow> v \<guillemotleft>| r \<Longrightarrow> u \<guillemotleft>| r"
4.67 + and rbt_greater_trans: "x < y \<Longrightarrow> y \<guillemotleft>| t \<Longrightarrow> x \<guillemotleft>| t"
4.68 + by (auto simp: rbt_ord_props)
4.69
4.70 -primrec sorted :: "('a::linorder, 'b) rbt \<Rightarrow> bool"
4.71 +primrec rbt_sorted :: "('a, 'b) rbt \<Rightarrow> bool"
4.72 where
4.73 - "sorted Empty = True"
4.74 -| "sorted (Branch c l k v r) = (l |\<guillemotleft> k \<and> k \<guillemotleft>| r \<and> sorted l \<and> sorted r)"
4.75 + "rbt_sorted Empty = True"
4.76 +| "rbt_sorted (Branch c l k v r) = (l |\<guillemotleft> k \<and> k \<guillemotleft>| r \<and> rbt_sorted l \<and> rbt_sorted r)"
4.77
4.78 -lemma sorted_entries:
4.79 - "sorted t \<Longrightarrow> List.sorted (List.map fst (entries t))"
4.80 +end
4.81 +
4.82 +context linorder begin
4.83 +
4.84 +lemma rbt_sorted_entries:
4.85 + "rbt_sorted t \<Longrightarrow> List.sorted (List.map fst (entries t))"
4.86 by (induct t)
4.87 - (force simp: sorted_append sorted_Cons tree_ord_props
4.88 + (force simp: sorted_append sorted_Cons rbt_ord_props
4.89 dest!: entry_in_tree_keys)+
4.90
4.91 lemma distinct_entries:
4.92 - "sorted t \<Longrightarrow> distinct (List.map fst (entries t))"
4.93 + "rbt_sorted t \<Longrightarrow> distinct (List.map fst (entries t))"
4.94 by (induct t)
4.95 - (force simp: sorted_append sorted_Cons tree_ord_props
4.96 + (force simp: sorted_append sorted_Cons rbt_ord_props
4.97 dest!: entry_in_tree_keys)+
4.98
4.99 -
4.100 subsubsection {* Tree lookup *}
4.101
4.102 -primrec lookup :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'a \<rightharpoonup> 'b"
4.103 +primrec (in ord) rbt_lookup :: "('a, 'b) rbt \<Rightarrow> 'a \<rightharpoonup> 'b"
4.104 where
4.105 - "lookup Empty k = None"
4.106 -| "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)"
4.107 + "rbt_lookup Empty k = None"
4.108 +| "rbt_lookup (Branch _ l x y r) k =
4.109 + (if k < x then rbt_lookup l k else if x < k then rbt_lookup r k else Some y)"
4.110
4.111 -lemma lookup_keys: "sorted t \<Longrightarrow> dom (lookup t) = set (keys t)"
4.112 - by (induct t) (auto simp: dom_def tree_greater_prop tree_less_prop)
4.113 +lemma rbt_lookup_keys: "rbt_sorted t \<Longrightarrow> dom (rbt_lookup t) = set (keys t)"
4.114 + by (induct t) (auto simp: dom_def rbt_greater_prop rbt_less_prop)
4.115
4.116 -lemma dom_lookup_Branch:
4.117 - "sorted (Branch c t1 k v t2) \<Longrightarrow>
4.118 - dom (lookup (Branch c t1 k v t2))
4.119 - = Set.insert k (dom (lookup t1) \<union> dom (lookup t2))"
4.120 +lemma dom_rbt_lookup_Branch:
4.121 + "rbt_sorted (Branch c t1 k v t2) \<Longrightarrow>
4.122 + dom (rbt_lookup (Branch c t1 k v t2))
4.123 + = Set.insert k (dom (rbt_lookup t1) \<union> dom (rbt_lookup t2))"
4.124 proof -
4.125 - assume "sorted (Branch c t1 k v t2)"
4.126 - moreover from this have "sorted t1" "sorted t2" by simp_all
4.127 - ultimately show ?thesis by (simp add: lookup_keys)
4.128 + assume "rbt_sorted (Branch c t1 k v t2)"
4.129 + moreover from this have "rbt_sorted t1" "rbt_sorted t2" by simp_all
4.130 + ultimately show ?thesis by (simp add: rbt_lookup_keys)
4.131 qed
4.132
4.133 -lemma finite_dom_lookup [simp, intro!]: "finite (dom (lookup t))"
4.134 +lemma finite_dom_rbt_lookup [simp, intro!]: "finite (dom (rbt_lookup t))"
4.135 proof (induct t)
4.136 case Empty then show ?case by simp
4.137 next
4.138 case (Branch color t1 a b t2)
4.139 - let ?A = "Set.insert a (dom (lookup t1) \<union> dom (lookup t2))"
4.140 - have "dom (lookup (Branch color t1 a b t2)) \<subseteq> ?A" by (auto split: split_if_asm)
4.141 - moreover from Branch have "finite (insert a (dom (lookup t1) \<union> dom (lookup t2)))" by simp
4.142 + let ?A = "Set.insert a (dom (rbt_lookup t1) \<union> dom (rbt_lookup t2))"
4.143 + have "dom (rbt_lookup (Branch color t1 a b t2)) \<subseteq> ?A" by (auto split: split_if_asm)
4.144 + moreover from Branch have "finite (insert a (dom (rbt_lookup t1) \<union> dom (rbt_lookup t2)))" by simp
4.145 ultimately show ?case by (rule finite_subset)
4.146 qed
4.147
4.148 -lemma lookup_tree_less[simp]: "t |\<guillemotleft> k \<Longrightarrow> lookup t k = None"
4.149 +end
4.150 +
4.151 +context ord begin
4.152 +
4.153 +lemma rbt_lookup_rbt_less[simp]: "t |\<guillemotleft> k \<Longrightarrow> rbt_lookup t k = None"
4.154 by (induct t) auto
4.155
4.156 -lemma lookup_tree_greater[simp]: "k \<guillemotleft>| t \<Longrightarrow> lookup t k = None"
4.157 +lemma rbt_lookup_rbt_greater[simp]: "k \<guillemotleft>| t \<Longrightarrow> rbt_lookup t k = None"
4.158 by (induct t) auto
4.159
4.160 -lemma lookup_Empty: "lookup Empty = empty"
4.161 +lemma rbt_lookup_Empty: "rbt_lookup Empty = empty"
4.162 by (rule ext) simp
4.163
4.164 +end
4.165 +
4.166 +context linorder begin
4.167 +
4.168 lemma map_of_entries:
4.169 - "sorted t \<Longrightarrow> map_of (entries t) = lookup t"
4.170 + "rbt_sorted t \<Longrightarrow> map_of (entries t) = rbt_lookup t"
4.171 proof (induct t)
4.172 - case Empty thus ?case by (simp add: lookup_Empty)
4.173 + case Empty thus ?case by (simp add: rbt_lookup_Empty)
4.174 next
4.175 case (Branch c t1 k v t2)
4.176 - have "lookup (Branch c t1 k v t2) = lookup t2 ++ [k\<mapsto>v] ++ lookup t1"
4.177 + have "rbt_lookup (Branch c t1 k v t2) = rbt_lookup t2 ++ [k\<mapsto>v] ++ rbt_lookup t1"
4.178 proof (rule ext)
4.179 fix x
4.180 - from Branch have SORTED: "sorted (Branch c t1 k v t2)" by simp
4.181 - let ?thesis = "lookup (Branch c t1 k v t2) x = (lookup t2 ++ [k \<mapsto> v] ++ lookup t1) x"
4.182 + from Branch have RBT_SORTED: "rbt_sorted (Branch c t1 k v t2)" by simp
4.183 + let ?thesis = "rbt_lookup (Branch c t1 k v t2) x = (rbt_lookup t2 ++ [k \<mapsto> v] ++ rbt_lookup t1) x"
4.184
4.185 - have DOM_T1: "!!k'. k'\<in>dom (lookup t1) \<Longrightarrow> k>k'"
4.186 + have DOM_T1: "!!k'. k'\<in>dom (rbt_lookup t1) \<Longrightarrow> k>k'"
4.187 proof -
4.188 fix k'
4.189 - from SORTED have "t1 |\<guillemotleft> k" by simp
4.190 - with tree_less_prop have "\<forall>k'\<in>set (keys t1). k>k'" by auto
4.191 - moreover assume "k'\<in>dom (lookup t1)"
4.192 - ultimately show "k>k'" using lookup_keys SORTED by auto
4.193 + from RBT_SORTED have "t1 |\<guillemotleft> k" by simp
4.194 + with rbt_less_prop have "\<forall>k'\<in>set (keys t1). k>k'" by auto
4.195 + moreover assume "k'\<in>dom (rbt_lookup t1)"
4.196 + ultimately show "k>k'" using rbt_lookup_keys RBT_SORTED by auto
4.197 qed
4.198
4.199 - have DOM_T2: "!!k'. k'\<in>dom (lookup t2) \<Longrightarrow> k<k'"
4.200 + have DOM_T2: "!!k'. k'\<in>dom (rbt_lookup t2) \<Longrightarrow> k<k'"
4.201 proof -
4.202 fix k'
4.203 - from SORTED have "k \<guillemotleft>| t2" by simp
4.204 - with tree_greater_prop have "\<forall>k'\<in>set (keys t2). k<k'" by auto
4.205 - moreover assume "k'\<in>dom (lookup t2)"
4.206 - ultimately show "k<k'" using lookup_keys SORTED by auto
4.207 + from RBT_SORTED have "k \<guillemotleft>| t2" by simp
4.208 + with rbt_greater_prop have "\<forall>k'\<in>set (keys t2). k<k'" by auto
4.209 + moreover assume "k'\<in>dom (rbt_lookup t2)"
4.210 + ultimately show "k<k'" using rbt_lookup_keys RBT_SORTED by auto
4.211 qed
4.212
4.213 {
4.214 assume C: "x<k"
4.215 - hence "lookup (Branch c t1 k v t2) x = lookup t1 x" by simp
4.216 + hence "rbt_lookup (Branch c t1 k v t2) x = rbt_lookup t1 x" by simp
4.217 moreover from C have "x\<notin>dom [k\<mapsto>v]" by simp
4.218 - moreover have "x\<notin>dom (lookup t2)" proof
4.219 - assume "x\<in>dom (lookup t2)"
4.220 + moreover have "x \<notin> dom (rbt_lookup t2)"
4.221 + proof
4.222 + assume "x \<in> dom (rbt_lookup t2)"
4.223 with DOM_T2 have "k<x" by blast
4.224 with C show False by simp
4.225 qed
4.226 ultimately have ?thesis by (simp add: map_add_upd_left map_add_dom_app_simps)
4.227 } moreover {
4.228 assume [simp]: "x=k"
4.229 - hence "lookup (Branch c t1 k v t2) x = [k \<mapsto> v] x" by simp
4.230 - moreover have "x\<notin>dom (lookup t1)" proof
4.231 - assume "x\<in>dom (lookup t1)"
4.232 + hence "rbt_lookup (Branch c t1 k v t2) x = [k \<mapsto> v] x" by simp
4.233 + moreover have "x \<notin> dom (rbt_lookup t1)"
4.234 + proof
4.235 + assume "x \<in> dom (rbt_lookup t1)"
4.236 with DOM_T1 have "k>x" by blast
4.237 thus False by simp
4.238 qed
4.239 ultimately have ?thesis by (simp add: map_add_upd_left map_add_dom_app_simps)
4.240 } moreover {
4.241 assume C: "x>k"
4.242 - hence "lookup (Branch c t1 k v t2) x = lookup t2 x" by (simp add: less_not_sym[of k x])
4.243 + hence "rbt_lookup (Branch c t1 k v t2) x = rbt_lookup t2 x" by (simp add: less_not_sym[of k x])
4.244 moreover from C have "x\<notin>dom [k\<mapsto>v]" by simp
4.245 - moreover have "x\<notin>dom (lookup t1)" proof
4.246 - assume "x\<in>dom (lookup t1)"
4.247 + moreover have "x\<notin>dom (rbt_lookup t1)" proof
4.248 + assume "x\<in>dom (rbt_lookup t1)"
4.249 with DOM_T1 have "k>x" by simp
4.250 with C show False by simp
4.251 qed
4.252 ultimately have ?thesis by (simp add: map_add_upd_left map_add_dom_app_simps)
4.253 } ultimately show ?thesis using less_linear by blast
4.254 qed
4.255 - also from Branch have "lookup t2 ++ [k \<mapsto> v] ++ lookup t1 = map_of (entries (Branch c t1 k v t2))" by simp
4.256 + also from Branch
4.257 + have "rbt_lookup t2 ++ [k \<mapsto> v] ++ rbt_lookup t1 = map_of (entries (Branch c t1 k v t2))" by simp
4.258 finally show ?case by simp
4.259 qed
4.260
4.261 -lemma lookup_in_tree: "sorted t \<Longrightarrow> lookup t k = Some v \<longleftrightarrow> (k, v) \<in> set (entries t)"
4.262 +lemma rbt_lookup_in_tree: "rbt_sorted t \<Longrightarrow> rbt_lookup t k = Some v \<longleftrightarrow> (k, v) \<in> set (entries t)"
4.263 by (simp add: map_of_entries [symmetric] distinct_entries)
4.264
4.265 lemma set_entries_inject:
4.266 - assumes sorted: "sorted t1" "sorted t2"
4.267 + assumes rbt_sorted: "rbt_sorted t1" "rbt_sorted t2"
4.268 shows "set (entries t1) = set (entries t2) \<longleftrightarrow> entries t1 = entries t2"
4.269 proof -
4.270 - from sorted have "distinct (map fst (entries t1))"
4.271 + from rbt_sorted have "distinct (map fst (entries t1))"
4.272 "distinct (map fst (entries t2))"
4.273 by (auto intro: distinct_entries)
4.274 - with sorted show ?thesis
4.275 - by (auto intro: map_sorted_distinct_set_unique sorted_entries simp add: distinct_map)
4.276 + with rbt_sorted show ?thesis
4.277 + by (auto intro: map_sorted_distinct_set_unique rbt_sorted_entries simp add: distinct_map)
4.278 qed
4.279
4.280 lemma entries_eqI:
4.281 - assumes sorted: "sorted t1" "sorted t2"
4.282 - assumes lookup: "lookup t1 = lookup t2"
4.283 + assumes rbt_sorted: "rbt_sorted t1" "rbt_sorted t2"
4.284 + assumes rbt_lookup: "rbt_lookup t1 = rbt_lookup t2"
4.285 shows "entries t1 = entries t2"
4.286 proof -
4.287 - from sorted lookup have "map_of (entries t1) = map_of (entries t2)"
4.288 + from rbt_sorted rbt_lookup have "map_of (entries t1) = map_of (entries t2)"
4.289 by (simp add: map_of_entries)
4.290 - with sorted have "set (entries t1) = set (entries t2)"
4.291 + with rbt_sorted have "set (entries t1) = set (entries t2)"
4.292 by (simp add: map_of_inject_set distinct_entries)
4.293 - with sorted show ?thesis by (simp add: set_entries_inject)
4.294 + with rbt_sorted show ?thesis by (simp add: set_entries_inject)
4.295 qed
4.296
4.297 -lemma entries_lookup:
4.298 - assumes "sorted t1" "sorted t2"
4.299 - shows "entries t1 = entries t2 \<longleftrightarrow> lookup t1 = lookup t2"
4.300 +lemma entries_rbt_lookup:
4.301 + assumes "rbt_sorted t1" "rbt_sorted t2"
4.302 + shows "entries t1 = entries t2 \<longleftrightarrow> rbt_lookup t1 = rbt_lookup t2"
4.303 using assms by (auto intro: entries_eqI simp add: map_of_entries [symmetric])
4.304
4.305 -lemma lookup_from_in_tree:
4.306 - assumes "sorted t1" "sorted t2"
4.307 - and "\<And>v. (k\<Colon>'a\<Colon>linorder, v) \<in> set (entries t1) \<longleftrightarrow> (k, v) \<in> set (entries t2)"
4.308 - shows "lookup t1 k = lookup t2 k"
4.309 +lemma rbt_lookup_from_in_tree:
4.310 + assumes "rbt_sorted t1" "rbt_sorted t2"
4.311 + and "\<And>v. (k, v) \<in> set (entries t1) \<longleftrightarrow> (k, v) \<in> set (entries t2)"
4.312 + shows "rbt_lookup t1 k = rbt_lookup t2 k"
4.313 proof -
4.314 - from assms have "k \<in> dom (lookup t1) \<longleftrightarrow> k \<in> dom (lookup t2)"
4.315 - by (simp add: keys_entries lookup_keys)
4.316 - with assms show ?thesis by (auto simp add: lookup_in_tree [symmetric])
4.317 + from assms have "k \<in> dom (rbt_lookup t1) \<longleftrightarrow> k \<in> dom (rbt_lookup t2)"
4.318 + by (simp add: keys_entries rbt_lookup_keys)
4.319 + with assms show ?thesis by (auto simp add: rbt_lookup_in_tree [symmetric])
4.320 qed
4.321
4.322 +end
4.323
4.324 subsubsection {* Red-black properties *}
4.325
4.326 @@ -290,15 +309,18 @@
4.327 "inv2 Empty = True"
4.328 | "inv2 (Branch c lt k v rt) = (inv2 lt \<and> inv2 rt \<and> bheight lt = bheight rt)"
4.329
4.330 -definition is_rbt :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> bool" where
4.331 - "is_rbt t \<longleftrightarrow> inv1 t \<and> inv2 t \<and> color_of t = B \<and> sorted t"
4.332 +context ord begin
4.333
4.334 -lemma is_rbt_sorted [simp]:
4.335 - "is_rbt t \<Longrightarrow> sorted t" by (simp add: is_rbt_def)
4.336 +definition is_rbt :: "('a, 'b) rbt \<Rightarrow> bool" where
4.337 + "is_rbt t \<longleftrightarrow> inv1 t \<and> inv2 t \<and> color_of t = B \<and> rbt_sorted t"
4.338 +
4.339 +lemma is_rbt_rbt_sorted [simp]:
4.340 + "is_rbt t \<Longrightarrow> rbt_sorted t" by (simp add: is_rbt_def)
4.341
4.342 theorem Empty_is_rbt [simp]:
4.343 "is_rbt Empty" by (simp add: is_rbt_def)
4.344
4.345 +end
4.346
4.347 subsection {* Insertion *}
4.348
4.349 @@ -324,61 +346,65 @@
4.350 using assms
4.351 by (induct l k v r rule: balance.induct) auto
4.352
4.353 -lemma balance_tree_greater[simp]: "(v \<guillemotleft>| balance a k x b) = (v \<guillemotleft>| a \<and> v \<guillemotleft>| b \<and> v < k)"
4.354 +context ord begin
4.355 +
4.356 +lemma balance_rbt_greater[simp]: "(v \<guillemotleft>| balance a k x b) = (v \<guillemotleft>| a \<and> v \<guillemotleft>| b \<and> v < k)"
4.357 by (induct a k x b rule: balance.induct) auto
4.358
4.359 -lemma balance_tree_less[simp]: "(balance a k x b |\<guillemotleft> v) = (a |\<guillemotleft> v \<and> b |\<guillemotleft> v \<and> k < v)"
4.360 +lemma balance_rbt_less[simp]: "(balance a k x b |\<guillemotleft> v) = (a |\<guillemotleft> v \<and> b |\<guillemotleft> v \<and> k < v)"
4.361 by (induct a k x b rule: balance.induct) auto
4.362
4.363 -lemma balance_sorted:
4.364 - fixes k :: "'a::linorder"
4.365 - assumes "sorted l" "sorted r" "l |\<guillemotleft> k" "k \<guillemotleft>| r"
4.366 - shows "sorted (balance l k v r)"
4.367 +end
4.368 +
4.369 +lemma (in linorder) balance_rbt_sorted:
4.370 + fixes k :: "'a"
4.371 + assumes "rbt_sorted l" "rbt_sorted r" "l |\<guillemotleft> k" "k \<guillemotleft>| r"
4.372 + shows "rbt_sorted (balance l k v r)"
4.373 using assms proof (induct l k v r rule: balance.induct)
4.374 case ("2_2" a x w b y t c z s va vb vd vc)
4.375 hence "y < z \<and> z \<guillemotleft>| Branch B va vb vd vc"
4.376 - by (auto simp add: tree_ord_props)
4.377 - hence "tree_greater y (Branch B va vb vd vc)" by (blast dest: tree_greater_trans)
4.378 + by (auto simp add: rbt_ord_props)
4.379 + hence "y \<guillemotleft>| (Branch B va vb vd vc)" by (blast dest: rbt_greater_trans)
4.380 with "2_2" show ?case by simp
4.381 next
4.382 case ("3_2" va vb vd vc x w b y s c z)
4.383 - from "3_2" have "x < y \<and> tree_less x (Branch B va vb vd vc)"
4.384 + from "3_2" have "x < y \<and> Branch B va vb vd vc |\<guillemotleft> x"
4.385 by simp
4.386 - hence "tree_less y (Branch B va vb vd vc)" by (blast dest: tree_less_trans)
4.387 + hence "Branch B va vb vd vc |\<guillemotleft> y" by (blast dest: rbt_less_trans)
4.388 with "3_2" show ?case by simp
4.389 next
4.390 case ("3_3" x w b y s c z t va vb vd vc)
4.391 - from "3_3" have "y < z \<and> tree_greater z (Branch B va vb vd vc)" by simp
4.392 - hence "tree_greater y (Branch B va vb vd vc)" by (blast dest: tree_greater_trans)
4.393 + from "3_3" have "y < z \<and> z \<guillemotleft>| Branch B va vb vd vc" by simp
4.394 + hence "y \<guillemotleft>| Branch B va vb vd vc" by (blast dest: rbt_greater_trans)
4.395 with "3_3" show ?case by simp
4.396 next
4.397 case ("3_4" vd ve vg vf x w b y s c z t va vb vii vc)
4.398 - hence "x < y \<and> tree_less x (Branch B vd ve vg vf)" by simp
4.399 - hence 1: "tree_less y (Branch B vd ve vg vf)" by (blast dest: tree_less_trans)
4.400 - from "3_4" have "y < z \<and> tree_greater z (Branch B va vb vii vc)" by simp
4.401 - hence "tree_greater y (Branch B va vb vii vc)" by (blast dest: tree_greater_trans)
4.402 + hence "x < y \<and> Branch B vd ve vg vf |\<guillemotleft> x" by simp
4.403 + hence 1: "Branch B vd ve vg vf |\<guillemotleft> y" by (blast dest: rbt_less_trans)
4.404 + from "3_4" have "y < z \<and> z \<guillemotleft>| Branch B va vb vii vc" by simp
4.405 + hence "y \<guillemotleft>| Branch B va vb vii vc" by (blast dest: rbt_greater_trans)
4.406 with 1 "3_4" show ?case by simp
4.407 next
4.408 case ("4_2" va vb vd vc x w b y s c z t dd)
4.409 - hence "x < y \<and> tree_less x (Branch B va vb vd vc)" by simp
4.410 - hence "tree_less y (Branch B va vb vd vc)" by (blast dest: tree_less_trans)
4.411 + hence "x < y \<and> Branch B va vb vd vc |\<guillemotleft> x" by simp
4.412 + hence "Branch B va vb vd vc |\<guillemotleft> y" by (blast dest: rbt_less_trans)
4.413 with "4_2" show ?case by simp
4.414 next
4.415 case ("5_2" x w b y s c z t va vb vd vc)
4.416 - hence "y < z \<and> tree_greater z (Branch B va vb vd vc)" by simp
4.417 - hence "tree_greater y (Branch B va vb vd vc)" by (blast dest: tree_greater_trans)
4.418 + hence "y < z \<and> z \<guillemotleft>| Branch B va vb vd vc" by simp
4.419 + hence "y \<guillemotleft>| Branch B va vb vd vc" by (blast dest: rbt_greater_trans)
4.420 with "5_2" show ?case by simp
4.421 next
4.422 case ("5_3" va vb vd vc x w b y s c z t)
4.423 - hence "x < y \<and> tree_less x (Branch B va vb vd vc)" by simp
4.424 - hence "tree_less y (Branch B va vb vd vc)" by (blast dest: tree_less_trans)
4.425 + hence "x < y \<and> Branch B va vb vd vc |\<guillemotleft> x" by simp
4.426 + hence "Branch B va vb vd vc |\<guillemotleft> y" by (blast dest: rbt_less_trans)
4.427 with "5_3" show ?case by simp
4.428 next
4.429 case ("5_4" va vb vg vc x w b y s c z t vd ve vii vf)
4.430 - hence "x < y \<and> tree_less x (Branch B va vb vg vc)" by simp
4.431 - hence 1: "tree_less y (Branch B va vb vg vc)" by (blast dest: tree_less_trans)
4.432 - from "5_4" have "y < z \<and> tree_greater z (Branch B vd ve vii vf)" by simp
4.433 - hence "tree_greater y (Branch B vd ve vii vf)" by (blast dest: tree_greater_trans)
4.434 + hence "x < y \<and> Branch B va vb vg vc |\<guillemotleft> x" by simp
4.435 + hence 1: "Branch B va vb vg vc |\<guillemotleft> y" by (blast dest: rbt_less_trans)
4.436 + from "5_4" have "y < z \<and> z \<guillemotleft>| Branch B vd ve vii vf" by simp
4.437 + hence "y \<guillemotleft>| Branch B vd ve vii vf" by (blast dest: rbt_greater_trans)
4.438 with 1 "5_4" show ?case by simp
4.439 qed simp+
4.440
4.441 @@ -394,11 +420,11 @@
4.442 "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"
4.443 by (auto simp add: keys_def)
4.444
4.445 -lemma lookup_balance[simp]:
4.446 -fixes k :: "'a::linorder"
4.447 -assumes "sorted l" "sorted r" "l |\<guillemotleft> k" "k \<guillemotleft>| r"
4.448 -shows "lookup (balance l k v r) x = lookup (Branch B l k v r) x"
4.449 -by (rule lookup_from_in_tree) (auto simp:assms balance_in_tree balance_sorted)
4.450 +lemma (in linorder) rbt_lookup_balance[simp]:
4.451 +fixes k :: "'a"
4.452 +assumes "rbt_sorted l" "rbt_sorted r" "l |\<guillemotleft> k" "k \<guillemotleft>| r"
4.453 +shows "rbt_lookup (balance l k v r) x = rbt_lookup (Branch B l k v r) x"
4.454 +by (rule rbt_lookup_from_in_tree) (auto simp:assms balance_in_tree balance_rbt_sorted)
4.455
4.456 primrec paint :: "color \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"
4.457 where
4.458 @@ -409,95 +435,112 @@
4.459 lemma paint_inv1[simp]: "inv1l t \<Longrightarrow> inv1 (paint B t)" by (cases t) auto
4.460 lemma paint_inv2[simp]: "inv2 t \<Longrightarrow> inv2 (paint c t)" by (cases t) auto
4.461 lemma paint_color_of[simp]: "color_of (paint B t) = B" by (cases t) auto
4.462 -lemma paint_sorted[simp]: "sorted t \<Longrightarrow> sorted (paint c t)" by (cases t) auto
4.463 lemma paint_in_tree[simp]: "entry_in_tree k x (paint c t) = entry_in_tree k x t" by (cases t) auto
4.464 -lemma paint_lookup[simp]: "lookup (paint c t) = lookup t" by (rule ext) (cases t, auto)
4.465 -lemma paint_tree_greater[simp]: "(v \<guillemotleft>| paint c t) = (v \<guillemotleft>| t)" by (cases t) auto
4.466 -lemma paint_tree_less[simp]: "(paint c t |\<guillemotleft> v) = (t |\<guillemotleft> v)" by (cases t) auto
4.467 +
4.468 +context ord begin
4.469 +
4.470 +lemma paint_rbt_sorted[simp]: "rbt_sorted t \<Longrightarrow> rbt_sorted (paint c t)" by (cases t) auto
4.471 +lemma paint_rbt_lookup[simp]: "rbt_lookup (paint c t) = rbt_lookup t" by (rule ext) (cases t, auto)
4.472 +lemma paint_rbt_greater[simp]: "(v \<guillemotleft>| paint c t) = (v \<guillemotleft>| t)" by (cases t) auto
4.473 +lemma paint_rbt_less[simp]: "(paint c t |\<guillemotleft> v) = (t |\<guillemotleft> v)" by (cases t) auto
4.474
4.475 fun
4.476 - ins :: "('a\<Colon>linorder \<Rightarrow> 'b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"
4.477 + rbt_ins :: "('a \<Rightarrow> 'b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"
4.478 where
4.479 - "ins f k v Empty = Branch R Empty k v Empty" |
4.480 - "ins f k v (Branch B l x y r) = (if k < x then balance (ins f k v l) x y r
4.481 - else if k > x then balance l x y (ins f k v r)
4.482 - else Branch B l x (f k y v) r)" |
4.483 - "ins f k v (Branch R l x y r) = (if k < x then Branch R (ins f k v l) x y r
4.484 - else if k > x then Branch R l x y (ins f k v r)
4.485 - else Branch R l x (f k y v) r)"
4.486 + "rbt_ins f k v Empty = Branch R Empty k v Empty" |
4.487 + "rbt_ins f k v (Branch B l x y r) = (if k < x then balance (rbt_ins f k v l) x y r
4.488 + else if k > x then balance l x y (rbt_ins f k v r)
4.489 + else Branch B l x (f k y v) r)" |
4.490 + "rbt_ins f k v (Branch R l x y r) = (if k < x then Branch R (rbt_ins f k v l) x y r
4.491 + else if k > x then Branch R l x y (rbt_ins f k v r)
4.492 + else Branch R l x (f k y v) r)"
4.493
4.494 lemma ins_inv1_inv2:
4.495 assumes "inv1 t" "inv2 t"
4.496 - shows "inv2 (ins f k x t)" "bheight (ins f k x t) = bheight t"
4.497 - "color_of t = B \<Longrightarrow> inv1 (ins f k x t)" "inv1l (ins f k x t)"
4.498 + shows "inv2 (rbt_ins f k x t)" "bheight (rbt_ins f k x t) = bheight t"
4.499 + "color_of t = B \<Longrightarrow> inv1 (rbt_ins f k x t)" "inv1l (rbt_ins f k x t)"
4.500 using assms
4.501 - by (induct f k x t rule: ins.induct) (auto simp: balance_inv1 balance_inv2 balance_bheight)
4.502 + by (induct f k x t rule: rbt_ins.induct) (auto simp: balance_inv1 balance_inv2 balance_bheight)
4.503
4.504 -lemma ins_tree_greater[simp]: "(v \<guillemotleft>| ins f k x t) = (v \<guillemotleft>| t \<and> k > v)"
4.505 - by (induct f k x t rule: ins.induct) auto
4.506 -lemma ins_tree_less[simp]: "(ins f k x t |\<guillemotleft> v) = (t |\<guillemotleft> v \<and> k < v)"
4.507 - by (induct f k x t rule: ins.induct) auto
4.508 -lemma ins_sorted[simp]: "sorted t \<Longrightarrow> sorted (ins f k x t)"
4.509 - by (induct f k x t rule: ins.induct) (auto simp: balance_sorted)
4.510 +end
4.511
4.512 -lemma keys_ins: "set (keys (ins f k v t)) = { k } \<union> set (keys t)"
4.513 - by (induct f k v t rule: ins.induct) auto
4.514 +context linorder begin
4.515
4.516 -lemma lookup_ins:
4.517 - fixes k :: "'a::linorder"
4.518 - assumes "sorted t"
4.519 - shows "lookup (ins f k v t) x = ((lookup t)(k |-> case lookup t k of None \<Rightarrow> v
4.520 - | Some w \<Rightarrow> f k w v)) x"
4.521 -using assms by (induct f k v t rule: ins.induct) auto
4.522 +lemma ins_rbt_greater[simp]: "(v \<guillemotleft>| rbt_ins f (k :: 'a) x t) = (v \<guillemotleft>| t \<and> k > v)"
4.523 + by (induct f k x t rule: rbt_ins.induct) auto
4.524 +lemma ins_rbt_less[simp]: "(rbt_ins f k x t |\<guillemotleft> v) = (t |\<guillemotleft> v \<and> k < v)"
4.525 + by (induct f k x t rule: rbt_ins.induct) auto
4.526 +lemma ins_rbt_sorted[simp]: "rbt_sorted t \<Longrightarrow> rbt_sorted (rbt_ins f k x t)"
4.527 + by (induct f k x t rule: rbt_ins.induct) (auto simp: balance_rbt_sorted)
4.528
4.529 -definition
4.530 - insert_with_key :: "('a\<Colon>linorder \<Rightarrow> 'b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"
4.531 -where
4.532 - "insert_with_key f k v t = paint B (ins f k v t)"
4.533 +lemma keys_ins: "set (keys (rbt_ins f k v t)) = { k } \<union> set (keys t)"
4.534 + by (induct f k v t rule: rbt_ins.induct) auto
4.535
4.536 -lemma insertwk_sorted: "sorted t \<Longrightarrow> sorted (insert_with_key f k x t)"
4.537 - by (auto simp: insert_with_key_def)
4.538 +lemma rbt_lookup_ins:
4.539 + fixes k :: "'a"
4.540 + assumes "rbt_sorted t"
4.541 + shows "rbt_lookup (rbt_ins f k v t) x = ((rbt_lookup t)(k |-> case rbt_lookup t k of None \<Rightarrow> v
4.542 + | Some w \<Rightarrow> f k w v)) x"
4.543 +using assms by (induct f k v t rule: rbt_ins.induct) auto
4.544
4.545 -theorem insertwk_is_rbt:
4.546 +end
4.547 +
4.548 +context ord begin
4.549 +
4.550 +definition rbt_insert_with_key :: "('a \<Rightarrow> 'b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"
4.551 +where "rbt_insert_with_key f k v t = paint B (rbt_ins f k v t)"
4.552 +
4.553 +definition rbt_insertw_def: "rbt_insert_with f = rbt_insert_with_key (\<lambda>_. f)"
4.554 +
4.555 +definition rbt_insert :: "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt" where
4.556 + "rbt_insert = rbt_insert_with_key (\<lambda>_ _ nv. nv)"
4.557 +
4.558 +end
4.559 +
4.560 +context linorder begin
4.561 +
4.562 +lemma rbt_insertwk_rbt_sorted: "rbt_sorted t \<Longrightarrow> rbt_sorted (rbt_insert_with_key f (k :: 'a) x t)"
4.563 + by (auto simp: rbt_insert_with_key_def)
4.564 +
4.565 +theorem rbt_insertwk_is_rbt:
4.566 assumes inv: "is_rbt t"
4.567 - shows "is_rbt (insert_with_key f k x t)"
4.568 + shows "is_rbt (rbt_insert_with_key f k x t)"
4.569 using assms
4.570 -unfolding insert_with_key_def is_rbt_def
4.571 +unfolding rbt_insert_with_key_def is_rbt_def
4.572 by (auto simp: ins_inv1_inv2)
4.573
4.574 -lemma lookup_insertwk:
4.575 - assumes "sorted t"
4.576 - shows "lookup (insert_with_key f k v t) x = ((lookup t)(k |-> case lookup t k of None \<Rightarrow> v
4.577 +lemma rbt_lookup_rbt_insertwk:
4.578 + assumes "rbt_sorted t"
4.579 + shows "rbt_lookup (rbt_insert_with_key f k v t) x = ((rbt_lookup t)(k |-> case rbt_lookup t k of None \<Rightarrow> v
4.580 | Some w \<Rightarrow> f k w v)) x"
4.581 -unfolding insert_with_key_def using assms
4.582 -by (simp add:lookup_ins)
4.583 +unfolding rbt_insert_with_key_def using assms
4.584 +by (simp add:rbt_lookup_ins)
4.585
4.586 -definition
4.587 - insertw_def: "insert_with f = insert_with_key (\<lambda>_. f)"
4.588 +lemma rbt_insertw_rbt_sorted: "rbt_sorted t \<Longrightarrow> rbt_sorted (rbt_insert_with f k v t)"
4.589 + by (simp add: rbt_insertwk_rbt_sorted rbt_insertw_def)
4.590 +theorem rbt_insertw_is_rbt: "is_rbt t \<Longrightarrow> is_rbt (rbt_insert_with f k v t)"
4.591 + by (simp add: rbt_insertwk_is_rbt rbt_insertw_def)
4.592
4.593 -lemma insertw_sorted: "sorted t \<Longrightarrow> sorted (insert_with f k v t)" by (simp add: insertwk_sorted insertw_def)
4.594 -theorem insertw_is_rbt: "is_rbt t \<Longrightarrow> is_rbt (insert_with f k v t)" by (simp add: insertwk_is_rbt insertw_def)
4.595 +lemma rbt_lookup_rbt_insertw:
4.596 + assumes "is_rbt t"
4.597 + shows "rbt_lookup (rbt_insert_with f k v t) = (rbt_lookup t)(k \<mapsto> (if k:dom (rbt_lookup t) then f (the (rbt_lookup t k)) v else v))"
4.598 +using assms
4.599 +unfolding rbt_insertw_def
4.600 +by (rule_tac ext) (cases "rbt_lookup t k", auto simp:rbt_lookup_rbt_insertwk dom_def)
4.601
4.602 -lemma lookup_insertw:
4.603 +lemma rbt_insert_rbt_sorted: "rbt_sorted t \<Longrightarrow> rbt_sorted (rbt_insert k v t)"
4.604 + by (simp add: rbt_insertwk_rbt_sorted rbt_insert_def)
4.605 +theorem rbt_insert_is_rbt [simp]: "is_rbt t \<Longrightarrow> is_rbt (rbt_insert k v t)"
4.606 + by (simp add: rbt_insertwk_is_rbt rbt_insert_def)
4.607 +
4.608 +lemma rbt_lookup_rbt_insert:
4.609 assumes "is_rbt t"
4.610 - 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))"
4.611 + shows "rbt_lookup (rbt_insert k v t) = (rbt_lookup t)(k\<mapsto>v)"
4.612 +unfolding rbt_insert_def
4.613 using assms
4.614 -unfolding insertw_def
4.615 -by (rule_tac ext) (cases "lookup t k", auto simp:lookup_insertwk dom_def)
4.616 +by (rule_tac ext) (simp add: rbt_lookup_rbt_insertwk split:option.split)
4.617
4.618 -definition insert :: "'a\<Colon>linorder \<Rightarrow> 'b \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt" where
4.619 - "insert = insert_with_key (\<lambda>_ _ nv. nv)"
4.620 -
4.621 -lemma insert_sorted: "sorted t \<Longrightarrow> sorted (insert k v t)" by (simp add: insertwk_sorted insert_def)
4.622 -theorem insert_is_rbt [simp]: "is_rbt t \<Longrightarrow> is_rbt (insert k v t)" by (simp add: insertwk_is_rbt insert_def)
4.623 -
4.624 -lemma lookup_insert:
4.625 - assumes "is_rbt t"
4.626 - shows "lookup (insert k v t) = (lookup t)(k\<mapsto>v)"
4.627 -unfolding insert_def
4.628 -using assms
4.629 -by (rule_tac ext) (simp add: lookup_insertwk split:option.split)
4.630 -
4.631 +end
4.632
4.633 subsection {* Deletion *}
4.634
4.635 @@ -532,26 +575,31 @@
4.636 lemma balance_left_inv1l: "\<lbrakk> inv1l lt; inv1 rt \<rbrakk> \<Longrightarrow> inv1l (balance_left lt k x rt)"
4.637 by (induct lt k x rt rule: balance_left.induct) (auto simp: balance_inv1)
4.638
4.639 -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)"
4.640 +lemma (in linorder) balance_left_rbt_sorted:
4.641 + "\<lbrakk> rbt_sorted l; rbt_sorted r; rbt_less k l; k \<guillemotleft>| r \<rbrakk> \<Longrightarrow> rbt_sorted (balance_left l k v r)"
4.642 apply (induct l k v r rule: balance_left.induct)
4.643 -apply (auto simp: balance_sorted)
4.644 -apply (unfold tree_greater_prop tree_less_prop)
4.645 +apply (auto simp: balance_rbt_sorted)
4.646 +apply (unfold rbt_greater_prop rbt_less_prop)
4.647 by force+
4.648
4.649 -lemma balance_left_tree_greater:
4.650 - fixes k :: "'a::order"
4.651 +context order begin
4.652 +
4.653 +lemma balance_left_rbt_greater:
4.654 + fixes k :: "'a"
4.655 assumes "k \<guillemotleft>| a" "k \<guillemotleft>| b" "k < x"
4.656 shows "k \<guillemotleft>| balance_left a x t b"
4.657 using assms
4.658 by (induct a x t b rule: balance_left.induct) auto
4.659
4.660 -lemma balance_left_tree_less:
4.661 - fixes k :: "'a::order"
4.662 +lemma balance_left_rbt_less:
4.663 + fixes k :: "'a"
4.664 assumes "a |\<guillemotleft> k" "b |\<guillemotleft> k" "x < k"
4.665 shows "balance_left a x t b |\<guillemotleft> k"
4.666 using assms
4.667 by (induct a x t b rule: balance_left.induct) auto
4.668
4.669 +end
4.670 +
4.671 lemma balance_left_in_tree:
4.672 assumes "inv1l l" "inv1 r" "bheight l + 1 = bheight r"
4.673 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)"
4.674 @@ -578,24 +626,29 @@
4.675 lemma balance_right_inv1l: "\<lbrakk> inv1 lt; inv1l rt \<rbrakk> \<Longrightarrow>inv1l (balance_right lt k x rt)"
4.676 by (induct lt k x rt rule: balance_right.induct) (auto simp: balance_inv1)
4.677
4.678 -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)"
4.679 +lemma (in linorder) balance_right_rbt_sorted:
4.680 + "\<lbrakk> rbt_sorted l; rbt_sorted r; rbt_less k l; k \<guillemotleft>| r \<rbrakk> \<Longrightarrow> rbt_sorted (balance_right l k v r)"
4.681 apply (induct l k v r rule: balance_right.induct)
4.682 -apply (auto simp:balance_sorted)
4.683 -apply (unfold tree_less_prop tree_greater_prop)
4.684 +apply (auto simp:balance_rbt_sorted)
4.685 +apply (unfold rbt_less_prop rbt_greater_prop)
4.686 by force+
4.687
4.688 -lemma balance_right_tree_greater:
4.689 - fixes k :: "'a::order"
4.690 +context order begin
4.691 +
4.692 +lemma balance_right_rbt_greater:
4.693 + fixes k :: "'a"
4.694 assumes "k \<guillemotleft>| a" "k \<guillemotleft>| b" "k < x"
4.695 shows "k \<guillemotleft>| balance_right a x t b"
4.696 using assms by (induct a x t b rule: balance_right.induct) auto
4.697
4.698 -lemma balance_right_tree_less:
4.699 - fixes k :: "'a::order"
4.700 +lemma balance_right_rbt_less:
4.701 + fixes k :: "'a"
4.702 assumes "a |\<guillemotleft> k" "b |\<guillemotleft> k" "x < k"
4.703 shows "balance_right a x t b |\<guillemotleft> k"
4.704 using assms by (induct a x t b rule: balance_right.induct) auto
4.705
4.706 +end
4.707 +
4.708 lemma balance_right_in_tree:
4.709 assumes "inv1 l" "inv1l r" "bheight l = bheight r + 1" "inv2 l" "inv2 r"
4.710 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)"
4.711 @@ -607,11 +660,11 @@
4.712 "combine Empty x = x"
4.713 | "combine x Empty = x"
4.714 | "combine (Branch R a k x b) (Branch R c s y d) = (case (combine b c) of
4.715 - Branch R b2 t z c2 \<Rightarrow> (Branch R (Branch R a k x b2) t z (Branch R c2 s y d)) |
4.716 - bc \<Rightarrow> Branch R a k x (Branch R bc s y d))"
4.717 + Branch R b2 t z c2 \<Rightarrow> (Branch R (Branch R a k x b2) t z (Branch R c2 s y d)) |
4.718 + bc \<Rightarrow> Branch R a k x (Branch R bc s y d))"
4.719 | "combine (Branch B a k x b) (Branch B c s y d) = (case (combine b c) of
4.720 - Branch R b2 t z c2 \<Rightarrow> Branch R (Branch B a k x b2) t z (Branch B c2 s y d) |
4.721 - bc \<Rightarrow> balance_left a k x (Branch B bc s y d))"
4.722 + Branch R b2 t z c2 \<Rightarrow> Branch R (Branch B a k x b2) t z (Branch B c2 s y d) |
4.723 + bc \<Rightarrow> balance_left a k x (Branch B bc s y d))"
4.724 | "combine a (Branch R b k x c) = Branch R (combine a b) k x c"
4.725 | "combine (Branch R a k x b) c = Branch R a k x (combine b c)"
4.726
4.727 @@ -630,26 +683,28 @@
4.728 by (induct lt rt rule: combine.induct)
4.729 (auto simp: balance_left_inv1 split: rbt.splits color.splits)
4.730
4.731 -lemma combine_tree_greater[simp]:
4.732 - fixes k :: "'a::linorder"
4.733 +context linorder begin
4.734 +
4.735 +lemma combine_rbt_greater[simp]:
4.736 + fixes k :: "'a"
4.737 assumes "k \<guillemotleft>| l" "k \<guillemotleft>| r"
4.738 shows "k \<guillemotleft>| combine l r"
4.739 using assms
4.740 by (induct l r rule: combine.induct)
4.741 - (auto simp: balance_left_tree_greater split:rbt.splits color.splits)
4.742 + (auto simp: balance_left_rbt_greater split:rbt.splits color.splits)
4.743
4.744 -lemma combine_tree_less[simp]:
4.745 - fixes k :: "'a::linorder"
4.746 +lemma combine_rbt_less[simp]:
4.747 + fixes k :: "'a"
4.748 assumes "l |\<guillemotleft> k" "r |\<guillemotleft> k"
4.749 shows "combine l r |\<guillemotleft> k"
4.750 using assms
4.751 by (induct l r rule: combine.induct)
4.752 - (auto simp: balance_left_tree_less split:rbt.splits color.splits)
4.753 + (auto simp: balance_left_rbt_less split:rbt.splits color.splits)
4.754
4.755 -lemma combine_sorted:
4.756 - fixes k :: "'a::linorder"
4.757 - assumes "sorted l" "sorted r" "l |\<guillemotleft> k" "k \<guillemotleft>| r"
4.758 - shows "sorted (combine l r)"
4.759 +lemma combine_rbt_sorted:
4.760 + fixes k :: "'a"
4.761 + assumes "rbt_sorted l" "rbt_sorted r" "l |\<guillemotleft> k" "k \<guillemotleft>| r"
4.762 + shows "rbt_sorted (combine l r)"
4.763 using assms proof (induct l r rule: combine.induct)
4.764 case (3 a x v b c y w d)
4.765 hence ineqs: "a |\<guillemotleft> x" "x \<guillemotleft>| b" "b |\<guillemotleft> k" "k \<guillemotleft>| c" "c |\<guillemotleft> y" "y \<guillemotleft>| d"
4.766 @@ -657,48 +712,52 @@
4.767 with 3
4.768 show ?case
4.769 by (cases "combine b c" rule: rbt_cases)
4.770 - (auto, (metis combine_tree_greater combine_tree_less ineqs ineqs tree_less_simps(2) tree_greater_simps(2) tree_greater_trans tree_less_trans)+)
4.771 + (auto, (metis combine_rbt_greater combine_rbt_less ineqs ineqs rbt_less_simps(2) rbt_greater_simps(2) rbt_greater_trans rbt_less_trans)+)
4.772 next
4.773 case (4 a x v b c y w d)
4.774 - hence "x < k \<and> tree_greater k c" by simp
4.775 - hence "tree_greater x c" by (blast dest: tree_greater_trans)
4.776 - with 4 have 2: "tree_greater x (combine b c)" by (simp add: combine_tree_greater)
4.777 - from 4 have "k < y \<and> tree_less k b" by simp
4.778 - hence "tree_less y b" by (blast dest: tree_less_trans)
4.779 - with 4 have 3: "tree_less y (combine b c)" by (simp add: combine_tree_less)
4.780 + hence "x < k \<and> rbt_greater k c" by simp
4.781 + hence "rbt_greater x c" by (blast dest: rbt_greater_trans)
4.782 + with 4 have 2: "rbt_greater x (combine b c)" by (simp add: combine_rbt_greater)
4.783 + from 4 have "k < y \<and> rbt_less k b" by simp
4.784 + hence "rbt_less y b" by (blast dest: rbt_less_trans)
4.785 + with 4 have 3: "rbt_less y (combine b c)" by (simp add: combine_rbt_less)
4.786 show ?case
4.787 proof (cases "combine b c" rule: rbt_cases)
4.788 case Empty
4.789 - from 4 have "x < y \<and> tree_greater y d" by auto
4.790 - hence "tree_greater x d" by (blast dest: tree_greater_trans)
4.791 - 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
4.792 - with Empty show ?thesis by (simp add: balance_left_sorted)
4.793 + from 4 have "x < y \<and> rbt_greater y d" by auto
4.794 + hence "rbt_greater x d" by (blast dest: rbt_greater_trans)
4.795 + with 4 Empty have "rbt_sorted a" and "rbt_sorted (Branch B Empty y w d)"
4.796 + and "rbt_less x a" and "rbt_greater x (Branch B Empty y w d)" by auto
4.797 + with Empty show ?thesis by (simp add: balance_left_rbt_sorted)
4.798 next
4.799 case (Red lta va ka rta)
4.800 - with 2 4 have "x < va \<and> tree_less x a" by simp
4.801 - hence 5: "tree_less va a" by (blast dest: tree_less_trans)
4.802 - from Red 3 4 have "va < y \<and> tree_greater y d" by simp
4.803 - hence "tree_greater va d" by (blast dest: tree_greater_trans)
4.804 + with 2 4 have "x < va \<and> rbt_less x a" by simp
4.805 + hence 5: "rbt_less va a" by (blast dest: rbt_less_trans)
4.806 + from Red 3 4 have "va < y \<and> rbt_greater y d" by simp
4.807 + hence "rbt_greater va d" by (blast dest: rbt_greater_trans)
4.808 with Red 2 3 4 5 show ?thesis by simp
4.809 next
4.810 case (Black lta va ka rta)
4.811 - from 4 have "x < y \<and> tree_greater y d" by auto
4.812 - hence "tree_greater x d" by (blast dest: tree_greater_trans)
4.813 - 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
4.814 - with Black show ?thesis by (simp add: balance_left_sorted)
4.815 + from 4 have "x < y \<and> rbt_greater y d" by auto
4.816 + hence "rbt_greater x d" by (blast dest: rbt_greater_trans)
4.817 + with Black 2 3 4 have "rbt_sorted a" and "rbt_sorted (Branch B (combine b c) y w d)"
4.818 + and "rbt_less x a" and "rbt_greater x (Branch B (combine b c) y w d)" by auto
4.819 + with Black show ?thesis by (simp add: balance_left_rbt_sorted)
4.820 qed
4.821 next
4.822 case (5 va vb vd vc b x w c)
4.823 - hence "k < x \<and> tree_less k (Branch B va vb vd vc)" by simp
4.824 - hence "tree_less x (Branch B va vb vd vc)" by (blast dest: tree_less_trans)
4.825 - with 5 show ?case by (simp add: combine_tree_less)
4.826 + hence "k < x \<and> rbt_less k (Branch B va vb vd vc)" by simp
4.827 + hence "rbt_less x (Branch B va vb vd vc)" by (blast dest: rbt_less_trans)
4.828 + with 5 show ?case by (simp add: combine_rbt_less)
4.829 next
4.830 case (6 a x v b va vb vd vc)
4.831 - hence "x < k \<and> tree_greater k (Branch B va vb vd vc)" by simp
4.832 - hence "tree_greater x (Branch B va vb vd vc)" by (blast dest: tree_greater_trans)
4.833 - with 6 show ?case by (simp add: combine_tree_greater)
4.834 + hence "x < k \<and> rbt_greater k (Branch B va vb vd vc)" by simp
4.835 + hence "rbt_greater x (Branch B va vb vd vc)" by (blast dest: rbt_greater_trans)
4.836 + with 6 show ?case by (simp add: combine_rbt_greater)
4.837 qed simp+
4.838
4.839 +end
4.840 +
4.841 lemma combine_in_tree:
4.842 assumes "inv2 l" "inv2 r" "bheight l = bheight r" "inv1 l" "inv1 r"
4.843 shows "entry_in_tree k v (combine l r) = (entry_in_tree k v l \<or> entry_in_tree k v r)"
4.844 @@ -721,29 +780,43 @@
4.845 qed
4.846 qed (auto split: rbt.splits color.splits)
4.847
4.848 +context ord begin
4.849 +
4.850 fun
4.851 - del_from_left :: "('a\<Colon>linorder) \<Rightarrow> ('a,'b) rbt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt" and
4.852 - del_from_right :: "('a\<Colon>linorder) \<Rightarrow> ('a,'b) rbt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt" and
4.853 - del :: "('a\<Colon>linorder) \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"
4.854 + rbt_del_from_left :: "'a \<Rightarrow> ('a,'b) rbt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt" and
4.855 + rbt_del_from_right :: "'a \<Rightarrow> ('a,'b) rbt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt" and
4.856 + rbt_del :: "'a\<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"
4.857 where
4.858 - "del x Empty = Empty" |
4.859 - "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))" |
4.860 - "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" |
4.861 - "del_from_left x a y s b = Branch R (del x a) y s b" |
4.862 - "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))" |
4.863 - "del_from_right x a y s b = Branch R a y s (del x b)"
4.864 + "rbt_del x Empty = Empty" |
4.865 + "rbt_del x (Branch c a y s b) =
4.866 + (if x < y then rbt_del_from_left x a y s b
4.867 + else (if x > y then rbt_del_from_right x a y s b else combine a b))" |
4.868 + "rbt_del_from_left x (Branch B lt z v rt) y s b = balance_left (rbt_del x (Branch B lt z v rt)) y s b" |
4.869 + "rbt_del_from_left x a y s b = Branch R (rbt_del x a) y s b" |
4.870 + "rbt_del_from_right x a y s (Branch B lt z v rt) = balance_right a y s (rbt_del x (Branch B lt z v rt))" |
4.871 + "rbt_del_from_right x a y s b = Branch R a y s (rbt_del x b)"
4.872 +
4.873 +end
4.874 +
4.875 +context linorder begin
4.876
4.877 lemma
4.878 assumes "inv2 lt" "inv1 lt"
4.879 shows
4.880 "\<lbrakk>inv2 rt; bheight lt = bheight rt; inv1 rt\<rbrakk> \<Longrightarrow>
4.881 - 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))"
4.882 + inv2 (rbt_del_from_left x lt k v rt) \<and>
4.883 + bheight (rbt_del_from_left x lt k v rt) = bheight lt \<and>
4.884 + (color_of lt = B \<and> color_of rt = B \<and> inv1 (rbt_del_from_left x lt k v rt) \<or>
4.885 + (color_of lt \<noteq> B \<or> color_of rt \<noteq> B) \<and> inv1l (rbt_del_from_left x lt k v rt))"
4.886 and "\<lbrakk>inv2 rt; bheight lt = bheight rt; inv1 rt\<rbrakk> \<Longrightarrow>
4.887 - 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))"
4.888 - 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)
4.889 - \<or> color_of lt = B \<and> bheight (del x lt) = bheight lt - 1 \<and> inv1l (del x lt))"
4.890 + inv2 (rbt_del_from_right x lt k v rt) \<and>
4.891 + bheight (rbt_del_from_right x lt k v rt) = bheight lt \<and>
4.892 + (color_of lt = B \<and> color_of rt = B \<and> inv1 (rbt_del_from_right x lt k v rt) \<or>
4.893 + (color_of lt \<noteq> B \<or> color_of rt \<noteq> B) \<and> inv1l (rbt_del_from_right x lt k v rt))"
4.894 + and rbt_del_inv1_inv2: "inv2 (rbt_del x lt) \<and> (color_of lt = R \<and> bheight (rbt_del x lt) = bheight lt \<and> inv1 (rbt_del x lt)
4.895 + \<or> color_of lt = B \<and> bheight (rbt_del x lt) = bheight lt - 1 \<and> inv1l (rbt_del x lt))"
4.896 using assms
4.897 -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)
4.898 +proof (induct x lt k v rt and x lt k v rt and x lt rule: rbt_del_from_left_rbt_del_from_right_rbt_del.induct)
4.899 case (2 y c _ y')
4.900 have "y = y' \<or> y < y' \<or> y > y'" by auto
4.901 thus ?case proof (elim disjE)
4.902 @@ -767,55 +840,55 @@
4.903 qed auto
4.904
4.905 lemma
4.906 - 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)"
4.907 - 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)"
4.908 - and del_tree_less: "tree_less v lt \<Longrightarrow> tree_less v (del x lt)"
4.909 -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)
4.910 - (auto simp: balance_left_tree_less balance_right_tree_less)
4.911 + rbt_del_from_left_rbt_less: "\<lbrakk> lt |\<guillemotleft> v; rt |\<guillemotleft> v; k < v\<rbrakk> \<Longrightarrow> rbt_del_from_left x lt k y rt |\<guillemotleft> v"
4.912 + and rbt_del_from_right_rbt_less: "\<lbrakk>lt |\<guillemotleft> v; rt |\<guillemotleft> v; k < v\<rbrakk> \<Longrightarrow> rbt_del_from_right x lt k y rt |\<guillemotleft> v"
4.913 + and rbt_del_rbt_less: "lt |\<guillemotleft> v \<Longrightarrow> rbt_del x lt |\<guillemotleft> v"
4.914 +by (induct x lt k y rt and x lt k y rt and x lt rule: rbt_del_from_left_rbt_del_from_right_rbt_del.induct)
4.915 + (auto simp: balance_left_rbt_less balance_right_rbt_less)
4.916
4.917 -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)"
4.918 - 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)"
4.919 - and del_tree_greater: "tree_greater v lt \<Longrightarrow> tree_greater v (del x lt)"
4.920 -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)
4.921 - (auto simp: balance_left_tree_greater balance_right_tree_greater)
4.922 +lemma rbt_del_from_left_rbt_greater: "\<lbrakk>v \<guillemotleft>| lt; v \<guillemotleft>| rt; k > v\<rbrakk> \<Longrightarrow> v \<guillemotleft>| rbt_del_from_left x lt k y rt"
4.923 + and rbt_del_from_right_rbt_greater: "\<lbrakk>v \<guillemotleft>| lt; v \<guillemotleft>| rt; k > v\<rbrakk> \<Longrightarrow> v \<guillemotleft>| rbt_del_from_right x lt k y rt"
4.924 + and rbt_del_rbt_greater: "v \<guillemotleft>| lt \<Longrightarrow> v \<guillemotleft>| rbt_del x lt"
4.925 +by (induct x lt k y rt and x lt k y rt and x lt rule: rbt_del_from_left_rbt_del_from_right_rbt_del.induct)
4.926 + (auto simp: balance_left_rbt_greater balance_right_rbt_greater)
4.927
4.928 -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)"
4.929 - 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)"
4.930 - and del_sorted: "sorted lt \<Longrightarrow> sorted (del x lt)"
4.931 -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)
4.932 +lemma "\<lbrakk>rbt_sorted lt; rbt_sorted rt; lt |\<guillemotleft> k; k \<guillemotleft>| rt\<rbrakk> \<Longrightarrow> rbt_sorted (rbt_del_from_left x lt k y rt)"
4.933 + and "\<lbrakk>rbt_sorted lt; rbt_sorted rt; lt |\<guillemotleft> k; k \<guillemotleft>| rt\<rbrakk> \<Longrightarrow> rbt_sorted (rbt_del_from_right x lt k y rt)"
4.934 + and rbt_del_rbt_sorted: "rbt_sorted lt \<Longrightarrow> rbt_sorted (rbt_del x lt)"
4.935 +proof (induct x lt k y rt and x lt k y rt and x lt rule: rbt_del_from_left_rbt_del_from_right_rbt_del.induct)
4.936 case (3 x lta zz v rta yy ss bb)
4.937 - from 3 have "tree_less yy (Branch B lta zz v rta)" by simp
4.938 - hence "tree_less yy (del x (Branch B lta zz v rta))" by (rule del_tree_less)
4.939 - with 3 show ?case by (simp add: balance_left_sorted)
4.940 + from 3 have "Branch B lta zz v rta |\<guillemotleft> yy" by simp
4.941 + hence "rbt_del x (Branch B lta zz v rta) |\<guillemotleft> yy" by (rule rbt_del_rbt_less)
4.942 + with 3 show ?case by (simp add: balance_left_rbt_sorted)
4.943 next
4.944 case ("4_2" x vaa vbb vdd vc yy ss bb)
4.945 - hence "tree_less yy (Branch R vaa vbb vdd vc)" by simp
4.946 - hence "tree_less yy (del x (Branch R vaa vbb vdd vc))" by (rule del_tree_less)
4.947 + hence "Branch R vaa vbb vdd vc |\<guillemotleft> yy" by simp
4.948 + hence "rbt_del x (Branch R vaa vbb vdd vc) |\<guillemotleft> yy" by (rule rbt_del_rbt_less)
4.949 with "4_2" show ?case by simp
4.950 next
4.951 case (5 x aa yy ss lta zz v rta)
4.952 - hence "tree_greater yy (Branch B lta zz v rta)" by simp
4.953 - hence "tree_greater yy (del x (Branch B lta zz v rta))" by (rule del_tree_greater)
4.954 - with 5 show ?case by (simp add: balance_right_sorted)
4.955 + hence "yy \<guillemotleft>| Branch B lta zz v rta" by simp
4.956 + hence "yy \<guillemotleft>| rbt_del x (Branch B lta zz v rta)" by (rule rbt_del_rbt_greater)
4.957 + with 5 show ?case by (simp add: balance_right_rbt_sorted)
4.958 next
4.959 case ("6_2" x aa yy ss vaa vbb vdd vc)
4.960 - hence "tree_greater yy (Branch R vaa vbb vdd vc)" by simp
4.961 - hence "tree_greater yy (del x (Branch R vaa vbb vdd vc))" by (rule del_tree_greater)
4.962 + hence "yy \<guillemotleft>| Branch R vaa vbb vdd vc" by simp
4.963 + hence "yy \<guillemotleft>| rbt_del x (Branch R vaa vbb vdd vc)" by (rule rbt_del_rbt_greater)
4.964 with "6_2" show ?case by simp
4.965 -qed (auto simp: combine_sorted)
4.966 +qed (auto simp: combine_rbt_sorted)
4.967
4.968 -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)))"
4.969 - 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)))"
4.970 - 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))"
4.971 -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)
4.972 +lemma "\<lbrakk>rbt_sorted lt; rbt_sorted rt; lt |\<guillemotleft> kt; kt \<guillemotleft>| rt; inv1 lt; inv1 rt; inv2 lt; inv2 rt; bheight lt = bheight rt; x < kt\<rbrakk> \<Longrightarrow> entry_in_tree k v (rbt_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)))"
4.973 + and "\<lbrakk>rbt_sorted lt; rbt_sorted rt; lt |\<guillemotleft> kt; kt \<guillemotleft>| rt; inv1 lt; inv1 rt; inv2 lt; inv2 rt; bheight lt = bheight rt; x > kt\<rbrakk> \<Longrightarrow> entry_in_tree k v (rbt_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)))"
4.974 + and rbt_del_in_tree: "\<lbrakk>rbt_sorted t; inv1 t; inv2 t\<rbrakk> \<Longrightarrow> entry_in_tree k v (rbt_del x t) = (False \<or> (x \<noteq> k \<and> entry_in_tree k v t))"
4.975 +proof (induct x lt kt y rt and x lt kt y rt and x t rule: rbt_del_from_left_rbt_del_from_right_rbt_del.induct)
4.976 case (2 xx c aa yy ss bb)
4.977 have "xx = yy \<or> xx < yy \<or> xx > yy" by auto
4.978 from this 2 show ?case proof (elim disjE)
4.979 assume "xx = yy"
4.980 with 2 show ?thesis proof (cases "xx = k")
4.981 case True
4.982 - from 2 `xx = yy` `xx = k` have "sorted (Branch c aa yy ss bb) \<and> k = yy" by simp
4.983 - hence "\<not> entry_in_tree k v aa" "\<not> entry_in_tree k v bb" by (auto simp: tree_less_nit tree_greater_prop)
4.984 + from 2 `xx = yy` `xx = k` have "rbt_sorted (Branch c aa yy ss bb) \<and> k = yy" by simp
4.985 + hence "\<not> entry_in_tree k v aa" "\<not> entry_in_tree k v bb" by (auto simp: rbt_less_nit rbt_greater_prop)
4.986 with `xx = yy` 2 `xx = k` show ?thesis by (simp add: combine_in_tree)
4.987 qed (simp add: combine_in_tree)
4.988 qed simp+
4.989 @@ -823,143 +896,147 @@
4.990 case (3 xx lta zz vv rta yy ss bb)
4.991 def mt[simp]: mt == "Branch B lta zz vv rta"
4.992 from 3 have "inv2 mt \<and> inv1 mt" by simp
4.993 - 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)
4.994 - 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)
4.995 + hence "inv2 (rbt_del xx mt) \<and> (color_of mt = R \<and> bheight (rbt_del xx mt) = bheight mt \<and> inv1 (rbt_del xx mt) \<or> color_of mt = B \<and> bheight (rbt_del xx mt) = bheight mt - 1 \<and> inv1l (rbt_del xx mt))" by (blast dest: rbt_del_inv1_inv2)
4.996 + with 3 have 4: "entry_in_tree k v (rbt_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)
4.997 thus ?case proof (cases "xx = k")
4.998 case True
4.999 - from 3 True have "tree_greater yy bb \<and> yy > k" by simp
4.1000 - hence "tree_greater k bb" by (blast dest: tree_greater_trans)
4.1001 - with 3 4 True show ?thesis by (auto simp: tree_greater_nit)
4.1002 + from 3 True have "yy \<guillemotleft>| bb \<and> yy > k" by simp
4.1003 + hence "k \<guillemotleft>| bb" by (blast dest: rbt_greater_trans)
4.1004 + with 3 4 True show ?thesis by (auto simp: rbt_greater_nit)
4.1005 qed auto
4.1006 next
4.1007 case ("4_1" xx yy ss bb)
4.1008 show ?case proof (cases "xx = k")
4.1009 case True
4.1010 - with "4_1" have "tree_greater yy bb \<and> k < yy" by simp
4.1011 - hence "tree_greater k bb" by (blast dest: tree_greater_trans)
4.1012 + with "4_1" have "yy \<guillemotleft>| bb \<and> k < yy" by simp
4.1013 + hence "k \<guillemotleft>| bb" by (blast dest: rbt_greater_trans)
4.1014 with "4_1" `xx = k`
4.1015 - have "entry_in_tree k v (Branch R Empty yy ss bb) = entry_in_tree k v Empty" by (auto simp: tree_greater_nit)
4.1016 + have "entry_in_tree k v (Branch R Empty yy ss bb) = entry_in_tree k v Empty" by (auto simp: rbt_greater_nit)
4.1017 thus ?thesis by auto
4.1018 qed simp+
4.1019 next
4.1020 case ("4_2" xx vaa vbb vdd vc yy ss bb)
4.1021 thus ?case proof (cases "xx = k")
4.1022 case True
4.1023 - with "4_2" have "k < yy \<and> tree_greater yy bb" by simp
4.1024 - hence "tree_greater k bb" by (blast dest: tree_greater_trans)
4.1025 - with True "4_2" show ?thesis by (auto simp: tree_greater_nit)
4.1026 + with "4_2" have "k < yy \<and> yy \<guillemotleft>| bb" by simp
4.1027 + hence "k \<guillemotleft>| bb" by (blast dest: rbt_greater_trans)
4.1028 + with True "4_2" show ?thesis by (auto simp: rbt_greater_nit)
4.1029 qed auto
4.1030 next
4.1031 case (5 xx aa yy ss lta zz vv rta)
4.1032 def mt[simp]: mt == "Branch B lta zz vv rta"
4.1033 from 5 have "inv2 mt \<and> inv1 mt" by simp
4.1034 - 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)
4.1035 - 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)
4.1036 + hence "inv2 (rbt_del xx mt) \<and> (color_of mt = R \<and> bheight (rbt_del xx mt) = bheight mt \<and> inv1 (rbt_del xx mt) \<or> color_of mt = B \<and> bheight (rbt_del xx mt) = bheight mt - 1 \<and> inv1l (rbt_del xx mt))" by (blast dest: rbt_del_inv1_inv2)
4.1037 + with 5 have 3: "entry_in_tree k v (rbt_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)
4.1038 thus ?case proof (cases "xx = k")
4.1039 case True
4.1040 - from 5 True have "tree_less yy aa \<and> yy < k" by simp
4.1041 - hence "tree_less k aa" by (blast dest: tree_less_trans)
4.1042 - with 3 5 True show ?thesis by (auto simp: tree_less_nit)
4.1043 + from 5 True have "aa |\<guillemotleft> yy \<and> yy < k" by simp
4.1044 + hence "aa |\<guillemotleft> k" by (blast dest: rbt_less_trans)
4.1045 + with 3 5 True show ?thesis by (auto simp: rbt_less_nit)
4.1046 qed auto
4.1047 next
4.1048 case ("6_1" xx aa yy ss)
4.1049 show ?case proof (cases "xx = k")
4.1050 case True
4.1051 - with "6_1" have "tree_less yy aa \<and> k > yy" by simp
4.1052 - hence "tree_less k aa" by (blast dest: tree_less_trans)
4.1053 - with "6_1" `xx = k` show ?thesis by (auto simp: tree_less_nit)
4.1054 + with "6_1" have "aa |\<guillemotleft> yy \<and> k > yy" by simp
4.1055 + hence "aa |\<guillemotleft> k" by (blast dest: rbt_less_trans)
4.1056 + with "6_1" `xx = k` show ?thesis by (auto simp: rbt_less_nit)
4.1057 qed simp
4.1058 next
4.1059 case ("6_2" xx aa yy ss vaa vbb vdd vc)
4.1060 thus ?case proof (cases "xx = k")
4.1061 case True
4.1062 - with "6_2" have "k > yy \<and> tree_less yy aa" by simp
4.1063 - hence "tree_less k aa" by (blast dest: tree_less_trans)
4.1064 - with True "6_2" show ?thesis by (auto simp: tree_less_nit)
4.1065 + with "6_2" have "k > yy \<and> aa |\<guillemotleft> yy" by simp
4.1066 + hence "aa |\<guillemotleft> k" by (blast dest: rbt_less_trans)
4.1067 + with True "6_2" show ?thesis by (auto simp: rbt_less_nit)
4.1068 qed auto
4.1069 qed simp
4.1070
4.1071 +definition (in ord) rbt_delete where
4.1072 + "rbt_delete k t = paint B (rbt_del k t)"
4.1073
4.1074 -definition delete where
4.1075 - delete_def: "delete k t = paint B (del k t)"
4.1076 -
4.1077 -theorem delete_is_rbt [simp]: assumes "is_rbt t" shows "is_rbt (delete k t)"
4.1078 +theorem rbt_delete_is_rbt [simp]: assumes "is_rbt t" shows "is_rbt (rbt_delete k t)"
4.1079 proof -
4.1080 from assms have "inv2 t" and "inv1 t" unfolding is_rbt_def by auto
4.1081 - 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)
4.1082 - hence "inv2 (del k t) \<and> inv1l (del k t)" by (cases "color_of t") auto
4.1083 + hence "inv2 (rbt_del k t) \<and> (color_of t = R \<and> bheight (rbt_del k t) = bheight t \<and> inv1 (rbt_del k t) \<or> color_of t = B \<and> bheight (rbt_del k t) = bheight t - 1 \<and> inv1l (rbt_del k t))" by (rule rbt_del_inv1_inv2)
4.1084 + hence "inv2 (rbt_del k t) \<and> inv1l (rbt_del k t)" by (cases "color_of t") auto
4.1085 with assms show ?thesis
4.1086 - unfolding is_rbt_def delete_def
4.1087 - by (auto intro: paint_sorted del_sorted)
4.1088 + unfolding is_rbt_def rbt_delete_def
4.1089 + by (auto intro: paint_rbt_sorted rbt_del_rbt_sorted)
4.1090 qed
4.1091
4.1092 -lemma delete_in_tree:
4.1093 +lemma rbt_delete_in_tree:
4.1094 assumes "is_rbt t"
4.1095 - shows "entry_in_tree k v (delete x t) = (x \<noteq> k \<and> entry_in_tree k v t)"
4.1096 - using assms unfolding is_rbt_def delete_def
4.1097 - by (auto simp: del_in_tree)
4.1098 + shows "entry_in_tree k v (rbt_delete x t) = (x \<noteq> k \<and> entry_in_tree k v t)"
4.1099 + using assms unfolding is_rbt_def rbt_delete_def
4.1100 + by (auto simp: rbt_del_in_tree)
4.1101
4.1102 -lemma lookup_delete:
4.1103 +lemma rbt_lookup_rbt_delete:
4.1104 assumes is_rbt: "is_rbt t"
4.1105 - shows "lookup (delete k t) = (lookup t)|`(-{k})"
4.1106 + shows "rbt_lookup (rbt_delete k t) = (rbt_lookup t)|`(-{k})"
4.1107 proof
4.1108 fix x
4.1109 - show "lookup (delete k t) x = (lookup t |` (-{k})) x"
4.1110 + show "rbt_lookup (rbt_delete k t) x = (rbt_lookup t |` (-{k})) x"
4.1111 proof (cases "x = k")
4.1112 assume "x = k"
4.1113 with is_rbt show ?thesis
4.1114 - by (cases "lookup (delete k t) k") (auto simp: lookup_in_tree delete_in_tree)
4.1115 + by (cases "rbt_lookup (rbt_delete k t) k") (auto simp: rbt_lookup_in_tree rbt_delete_in_tree)
4.1116 next
4.1117 assume "x \<noteq> k"
4.1118 thus ?thesis
4.1119 - by auto (metis is_rbt delete_is_rbt delete_in_tree is_rbt_sorted lookup_from_in_tree)
4.1120 + by auto (metis is_rbt rbt_delete_is_rbt rbt_delete_in_tree is_rbt_rbt_sorted rbt_lookup_from_in_tree)
4.1121 qed
4.1122 qed
4.1123
4.1124 +end
4.1125
4.1126 subsection {* Union *}
4.1127
4.1128 -primrec
4.1129 - union_with_key :: "('a\<Colon>linorder \<Rightarrow> 'b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"
4.1130 +context ord begin
4.1131 +
4.1132 +primrec rbt_union_with_key :: "('a \<Rightarrow> 'b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"
4.1133 where
4.1134 - "union_with_key f t Empty = t"
4.1135 -| "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"
4.1136 + "rbt_union_with_key f t Empty = t"
4.1137 +| "rbt_union_with_key f t (Branch c lt k v rt) = rbt_union_with_key f (rbt_union_with_key f (rbt_insert_with_key f k v t) lt) rt"
4.1138
4.1139 -lemma unionwk_sorted: "sorted lt \<Longrightarrow> sorted (union_with_key f lt rt)"
4.1140 - by (induct rt arbitrary: lt) (auto simp: insertwk_sorted)
4.1141 -theorem unionwk_is_rbt[simp]: "is_rbt lt \<Longrightarrow> is_rbt (union_with_key f lt rt)"
4.1142 - by (induct rt arbitrary: lt) (simp add: insertwk_is_rbt)+
4.1143 +definition rbt_union_with where
4.1144 + "rbt_union_with f = rbt_union_with_key (\<lambda>_. f)"
4.1145
4.1146 -definition
4.1147 - union_with where
4.1148 - "union_with f = union_with_key (\<lambda>_. f)"
4.1149 +definition rbt_union where
4.1150 + "rbt_union = rbt_union_with_key (%_ _ rv. rv)"
4.1151
4.1152 -theorem unionw_is_rbt: "is_rbt lt \<Longrightarrow> is_rbt (union_with f lt rt)" unfolding union_with_def by simp
4.1153 +end
4.1154
4.1155 -definition union where
4.1156 - "union = union_with_key (%_ _ rv. rv)"
4.1157 +context linorder begin
4.1158
4.1159 -theorem union_is_rbt: "is_rbt lt \<Longrightarrow> is_rbt (union lt rt)" unfolding union_def by simp
4.1160 +lemma rbt_unionwk_rbt_sorted: "rbt_sorted lt \<Longrightarrow> rbt_sorted (rbt_union_with_key f lt rt)"
4.1161 + by (induct rt arbitrary: lt) (auto simp: rbt_insertwk_rbt_sorted)
4.1162 +theorem rbt_unionwk_is_rbt[simp]: "is_rbt lt \<Longrightarrow> is_rbt (rbt_union_with_key f lt rt)"
4.1163 + by (induct rt arbitrary: lt) (simp add: rbt_insertwk_is_rbt)+
4.1164
4.1165 -lemma union_Branch[simp]:
4.1166 - "union t (Branch c lt k v rt) = union (union (insert k v t) lt) rt"
4.1167 - unfolding union_def insert_def
4.1168 +theorem rbt_unionw_is_rbt: "is_rbt lt \<Longrightarrow> is_rbt (rbt_union_with f lt rt)" unfolding rbt_union_with_def by simp
4.1169 +
4.1170 +theorem rbt_union_is_rbt: "is_rbt lt \<Longrightarrow> is_rbt (rbt_union lt rt)" unfolding rbt_union_def by simp
4.1171 +
4.1172 +lemma (in ord) rbt_union_Branch[simp]:
4.1173 + "rbt_union t (Branch c lt k v rt) = rbt_union (rbt_union (rbt_insert k v t) lt) rt"
4.1174 + unfolding rbt_union_def rbt_insert_def
4.1175 by simp
4.1176
4.1177 -lemma lookup_union:
4.1178 - assumes "is_rbt s" "sorted t"
4.1179 - shows "lookup (union s t) = lookup s ++ lookup t"
4.1180 +lemma rbt_lookup_rbt_union:
4.1181 + assumes "is_rbt s" "rbt_sorted t"
4.1182 + shows "rbt_lookup (rbt_union s t) = rbt_lookup s ++ rbt_lookup t"
4.1183 using assms
4.1184 proof (induct t arbitrary: s)
4.1185 - case Empty thus ?case by (auto simp: union_def)
4.1186 + case Empty thus ?case by (auto simp: rbt_union_def)
4.1187 next
4.1188 case (Branch c l k v r s)
4.1189 - then have "sorted r" "sorted l" "l |\<guillemotleft> k" "k \<guillemotleft>| r" by auto
4.1190 + then have "rbt_sorted r" "rbt_sorted l" "l |\<guillemotleft> k" "k \<guillemotleft>| r" by auto
4.1191
4.1192 - have meq: "lookup s(k \<mapsto> v) ++ lookup l ++ lookup r =
4.1193 - lookup s ++
4.1194 - (\<lambda>a. if a < k then lookup l a
4.1195 - else if k < a then lookup r a else Some v)" (is "?m1 = ?m2")
4.1196 + have meq: "rbt_lookup s(k \<mapsto> v) ++ rbt_lookup l ++ rbt_lookup r =
4.1197 + rbt_lookup s ++
4.1198 + (\<lambda>a. if a < k then rbt_lookup l a
4.1199 + else if k < a then rbt_lookup r a else Some v)" (is "?m1 = ?m2")
4.1200 proof (rule ext)
4.1201 fix a
4.1202
4.1203 @@ -967,7 +1044,7 @@
4.1204 thus "?m1 a = ?m2 a"
4.1205 proof (elim disjE)
4.1206 assume "k < a"
4.1207 - with `l |\<guillemotleft> k` have "l |\<guillemotleft> a" by (rule tree_less_trans)
4.1208 + with `l |\<guillemotleft> k` have "l |\<guillemotleft> a" by (rule rbt_less_trans)
4.1209 with `k < a` show ?thesis
4.1210 by (auto simp: map_add_def split: option.splits)
4.1211 next
4.1212 @@ -976,52 +1053,57 @@
4.1213 show ?thesis by (auto simp: map_add_def)
4.1214 next
4.1215 assume "a < k"
4.1216 - from this `k \<guillemotleft>| r` have "a \<guillemotleft>| r" by (rule tree_greater_trans)
4.1217 + from this `k \<guillemotleft>| r` have "a \<guillemotleft>| r" by (rule rbt_greater_trans)
4.1218 with `a < k` show ?thesis
4.1219 by (auto simp: map_add_def split: option.splits)
4.1220 qed
4.1221 qed
4.1222
4.1223 - from Branch have is_rbt: "is_rbt (RBT_Impl.union (RBT_Impl.insert k v s) l)"
4.1224 - by (auto intro: union_is_rbt insert_is_rbt)
4.1225 + from Branch have is_rbt: "is_rbt (RBT_Impl.rbt_union (RBT_Impl.rbt_insert k v s) l)"
4.1226 + by (auto intro: rbt_union_is_rbt rbt_insert_is_rbt)
4.1227 with Branch have IHs:
4.1228 - "lookup (union (union (insert k v s) l) r) = lookup (union (insert k v s) l) ++ lookup r"
4.1229 - "lookup (union (insert k v s) l) = lookup (insert k v s) ++ lookup l"
4.1230 + "rbt_lookup (rbt_union (rbt_union (rbt_insert k v s) l) r) = rbt_lookup (rbt_union (rbt_insert k v s) l) ++ rbt_lookup r"
4.1231 + "rbt_lookup (rbt_union (rbt_insert k v s) l) = rbt_lookup (rbt_insert k v s) ++ rbt_lookup l"
4.1232 by auto
4.1233
4.1234 with meq show ?case
4.1235 - by (auto simp: lookup_insert[OF Branch(3)])
4.1236 + by (auto simp: rbt_lookup_rbt_insert[OF Branch(3)])
4.1237
4.1238 qed
4.1239
4.1240 +end
4.1241
4.1242 subsection {* Modifying existing entries *}
4.1243
4.1244 +context ord begin
4.1245 +
4.1246 primrec
4.1247 - map_entry :: "'a\<Colon>linorder \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt"
4.1248 + rbt_map_entry :: "'a \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt"
4.1249 where
4.1250 - "map_entry k f Empty = Empty"
4.1251 -| "map_entry k f (Branch c lt x v rt) =
4.1252 - (if k < x then Branch c (map_entry k f lt) x v rt
4.1253 - else if k > x then (Branch c lt x v (map_entry k f rt))
4.1254 + "rbt_map_entry k f Empty = Empty"
4.1255 +| "rbt_map_entry k f (Branch c lt x v rt) =
4.1256 + (if k < x then Branch c (rbt_map_entry k f lt) x v rt
4.1257 + else if k > x then (Branch c lt x v (rbt_map_entry k f rt))
4.1258 else Branch c lt x (f v) rt)"
4.1259
4.1260 -lemma map_entry_color_of: "color_of (map_entry k f t) = color_of t" by (induct t) simp+
4.1261 -lemma map_entry_inv1: "inv1 (map_entry k f t) = inv1 t" by (induct t) (simp add: map_entry_color_of)+
4.1262 -lemma map_entry_inv2: "inv2 (map_entry k f t) = inv2 t" "bheight (map_entry k f t) = bheight t" by (induct t) simp+
4.1263 -lemma map_entry_tree_greater: "tree_greater a (map_entry k f t) = tree_greater a t" by (induct t) simp+
4.1264 -lemma map_entry_tree_less: "tree_less a (map_entry k f t) = tree_less a t" by (induct t) simp+
4.1265 -lemma map_entry_sorted: "sorted (map_entry k f t) = sorted t"
4.1266 - by (induct t) (simp_all add: map_entry_tree_less map_entry_tree_greater)
4.1267
4.1268 -theorem map_entry_is_rbt [simp]: "is_rbt (map_entry k f t) = is_rbt t"
4.1269 -unfolding is_rbt_def by (simp add: map_entry_inv2 map_entry_color_of map_entry_sorted map_entry_inv1 )
4.1270 +lemma rbt_map_entry_color_of: "color_of (rbt_map_entry k f t) = color_of t" by (induct t) simp+
4.1271 +lemma rbt_map_entry_inv1: "inv1 (rbt_map_entry k f t) = inv1 t" by (induct t) (simp add: rbt_map_entry_color_of)+
4.1272 +lemma rbt_map_entry_inv2: "inv2 (rbt_map_entry k f t) = inv2 t" "bheight (rbt_map_entry k f t) = bheight t" by (induct t) simp+
4.1273 +lemma rbt_map_entry_rbt_greater: "rbt_greater a (rbt_map_entry k f t) = rbt_greater a t" by (induct t) simp+
4.1274 +lemma rbt_map_entry_rbt_less: "rbt_less a (rbt_map_entry k f t) = rbt_less a t" by (induct t) simp+
4.1275 +lemma rbt_map_entry_rbt_sorted: "rbt_sorted (rbt_map_entry k f t) = rbt_sorted t"
4.1276 + by (induct t) (simp_all add: rbt_map_entry_rbt_less rbt_map_entry_rbt_greater)
4.1277
4.1278 -theorem lookup_map_entry:
4.1279 - "lookup (map_entry k f t) = (lookup t)(k := Option.map f (lookup t k))"
4.1280 +theorem rbt_map_entry_is_rbt [simp]: "is_rbt (rbt_map_entry k f t) = is_rbt t"
4.1281 +unfolding is_rbt_def by (simp add: rbt_map_entry_inv2 rbt_map_entry_color_of rbt_map_entry_rbt_sorted rbt_map_entry_inv1 )
4.1282 +
4.1283 +end
4.1284 +
4.1285 +theorem (in linorder) rbt_lookup_rbt_map_entry:
4.1286 + "rbt_lookup (rbt_map_entry k f t) = (rbt_lookup t)(k := Option.map f (rbt_lookup t k))"
4.1287 by (induct t) (auto split: option.splits simp add: fun_eq_iff)
4.1288
4.1289 -
4.1290 subsection {* Mapping all entries *}
4.1291
4.1292 primrec
4.1293 @@ -1033,18 +1115,28 @@
4.1294 lemma map_entries [simp]: "entries (map f t) = List.map (\<lambda>(k, v). (k, f k v)) (entries t)"
4.1295 by (induct t) auto
4.1296 lemma map_keys [simp]: "keys (map f t) = keys t" by (simp add: keys_def split_def)
4.1297 -lemma map_tree_greater: "tree_greater k (map f t) = tree_greater k t" by (induct t) simp+
4.1298 -lemma map_tree_less: "tree_less k (map f t) = tree_less k t" by (induct t) simp+
4.1299 -lemma map_sorted: "sorted (map f t) = sorted t" by (induct t) (simp add: map_tree_less map_tree_greater)+
4.1300 lemma map_color_of: "color_of (map f t) = color_of t" by (induct t) simp+
4.1301 lemma map_inv1: "inv1 (map f t) = inv1 t" by (induct t) (simp add: map_color_of)+
4.1302 lemma map_inv2: "inv2 (map f t) = inv2 t" "bheight (map f t) = bheight t" by (induct t) simp+
4.1303 +
4.1304 +context ord begin
4.1305 +
4.1306 +lemma map_rbt_greater: "rbt_greater k (map f t) = rbt_greater k t" by (induct t) simp+
4.1307 +lemma map_rbt_less: "rbt_less k (map f t) = rbt_less k t" by (induct t) simp+
4.1308 +lemma map_rbt_sorted: "rbt_sorted (map f t) = rbt_sorted t" by (induct t) (simp add: map_rbt_less map_rbt_greater)+
4.1309 theorem map_is_rbt [simp]: "is_rbt (map f t) = is_rbt t"
4.1310 -unfolding is_rbt_def by (simp add: map_inv1 map_inv2 map_sorted map_color_of)
4.1311 +unfolding is_rbt_def by (simp add: map_inv1 map_inv2 map_rbt_sorted map_color_of)
4.1312
4.1313 -theorem lookup_map: "lookup (map f t) x = Option.map (f x) (lookup t x)"
4.1314 - by (induct t) auto
4.1315 +end
4.1316
4.1317 +theorem (in linorder) rbt_lookup_map: "rbt_lookup (map f t) x = Option.map (f x) (rbt_lookup t x)"
4.1318 + apply(induct t)
4.1319 + apply auto
4.1320 + apply(subgoal_tac "x = a")
4.1321 + apply auto
4.1322 + done
4.1323 + (* FIXME: simproc "antisym less" does not work for linorder context, only for linorder type class
4.1324 + by (induct t) auto *)
4.1325
4.1326 subsection {* Folding over entries *}
4.1327
4.1328 @@ -1059,26 +1151,73 @@
4.1329
4.1330 subsection {* Bulkloading a tree *}
4.1331
4.1332 -definition bulkload :: "('a \<times> 'b) list \<Rightarrow> ('a\<Colon>linorder, 'b) rbt" where
4.1333 - "bulkload xs = foldr (\<lambda>(k, v). insert k v) xs Empty"
4.1334 +definition (in ord) rbt_bulkload :: "('a \<times> 'b) list \<Rightarrow> ('a, 'b) rbt" where
4.1335 + "rbt_bulkload xs = foldr (\<lambda>(k, v). rbt_insert k v) xs Empty"
4.1336
4.1337 -lemma bulkload_is_rbt [simp, intro]:
4.1338 - "is_rbt (bulkload xs)"
4.1339 - unfolding bulkload_def by (induct xs) auto
4.1340 +context linorder begin
4.1341
4.1342 -lemma lookup_bulkload:
4.1343 - "lookup (bulkload xs) = map_of xs"
4.1344 +lemma rbt_bulkload_is_rbt [simp, intro]:
4.1345 + "is_rbt (rbt_bulkload xs)"
4.1346 + unfolding rbt_bulkload_def by (induct xs) auto
4.1347 +
4.1348 +lemma rbt_lookup_rbt_bulkload:
4.1349 + "rbt_lookup (rbt_bulkload xs) = map_of xs"
4.1350 proof -
4.1351 obtain ys where "ys = rev xs" by simp
4.1352 have "\<And>t. is_rbt t \<Longrightarrow>
4.1353 - lookup (List.fold (prod_case insert) ys t) = lookup t ++ map_of (rev ys)"
4.1354 - by (induct ys) (simp_all add: bulkload_def lookup_insert prod_case_beta)
4.1355 + rbt_lookup (List.fold (prod_case rbt_insert) ys t) = rbt_lookup t ++ map_of (rev ys)"
4.1356 + by (induct ys) (simp_all add: rbt_bulkload_def rbt_lookup_rbt_insert prod_case_beta)
4.1357 from this Empty_is_rbt have
4.1358 - "lookup (List.fold (prod_case insert) (rev xs) Empty) = lookup Empty ++ map_of xs"
4.1359 + "rbt_lookup (List.fold (prod_case rbt_insert) (rev xs) Empty) = rbt_lookup Empty ++ map_of xs"
4.1360 by (simp add: `ys = rev xs`)
4.1361 - then show ?thesis by (simp add: bulkload_def lookup_Empty foldr_conv_fold)
4.1362 + then show ?thesis by (simp add: rbt_bulkload_def rbt_lookup_Empty foldr_conv_fold)
4.1363 qed
4.1364
4.1365 -hide_const (open) R B Empty insert delete entries keys bulkload lookup map_entry map fold union sorted
4.1366 +end
4.1367 +
4.1368 +lemmas [code] =
4.1369 + ord.rbt_less_prop
4.1370 + ord.rbt_greater_prop
4.1371 + ord.rbt_sorted.simps
4.1372 + ord.rbt_lookup.simps
4.1373 + ord.is_rbt_def
4.1374 + ord.rbt_ins.simps
4.1375 + ord.rbt_insert_with_key_def
4.1376 + ord.rbt_insertw_def
4.1377 + ord.rbt_insert_def
4.1378 + ord.rbt_del_from_left.simps
4.1379 + ord.rbt_del_from_right.simps
4.1380 + ord.rbt_del.simps
4.1381 + ord.rbt_delete_def
4.1382 + ord.rbt_union_with_key.simps
4.1383 + ord.rbt_union_with_def
4.1384 + ord.rbt_union_def
4.1385 + ord.rbt_map_entry.simps
4.1386 + ord.rbt_bulkload_def
4.1387 +
4.1388 +text {* Restore original type constraints for constants *}
4.1389 +setup {*
4.1390 + fold Sign.add_const_constraint
4.1391 + [(@{const_name rbt_less}, SOME @{typ "('a :: order) \<Rightarrow> ('a, 'b) rbt \<Rightarrow> bool"}),
4.1392 + (@{const_name rbt_greater}, SOME @{typ "('a :: order) \<Rightarrow> ('a, 'b) rbt \<Rightarrow> bool"}),
4.1393 + (@{const_name rbt_sorted}, SOME @{typ "('a :: linorder, 'b) rbt \<Rightarrow> bool"}),
4.1394 + (@{const_name rbt_lookup}, SOME @{typ "('a :: linorder, 'b) rbt \<Rightarrow> 'a \<rightharpoonup> 'b"}),
4.1395 + (@{const_name is_rbt}, SOME @{typ "('a :: linorder, 'b) rbt \<Rightarrow> bool"}),
4.1396 + (@{const_name rbt_ins}, SOME @{typ "('a\<Colon>linorder \<Rightarrow> 'b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"}),
4.1397 + (@{const_name rbt_insert_with_key}, SOME @{typ "('a\<Colon>linorder \<Rightarrow> 'b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"}),
4.1398 + (@{const_name rbt_insert_with}, SOME @{typ "('b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a :: linorder) \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"}),
4.1399 + (@{const_name rbt_insert}, SOME @{typ "('a :: linorder) \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"}),
4.1400 + (@{const_name rbt_del_from_left}, SOME @{typ "('a\<Colon>linorder) \<Rightarrow> ('a,'b) rbt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"}),
4.1401 + (@{const_name rbt_del_from_right}, SOME @{typ "('a\<Colon>linorder) \<Rightarrow> ('a,'b) rbt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"}),
4.1402 + (@{const_name rbt_del}, SOME @{typ "('a\<Colon>linorder) \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"}),
4.1403 + (@{const_name rbt_delete}, SOME @{typ "('a\<Colon>linorder) \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"}),
4.1404 + (@{const_name rbt_union_with_key}, SOME @{typ "('a\<Colon>linorder \<Rightarrow> 'b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"}),
4.1405 + (@{const_name rbt_union_with}, SOME @{typ "('b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a\<Colon>linorder,'b) rbt \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"}),
4.1406 + (@{const_name rbt_union}, SOME @{typ "('a\<Colon>linorder,'b) rbt \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"}),
4.1407 + (@{const_name rbt_map_entry}, SOME @{typ "'a\<Colon>linorder \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"}),
4.1408 + (@{const_name rbt_bulkload}, SOME @{typ "('a \<times> 'b) list \<Rightarrow> ('a\<Colon>linorder,'b) rbt"})]
4.1409 +*}
4.1410 +
4.1411 +hide_const (open) R B Empty entries keys map fold
4.1412
4.1413 end
5.1 --- a/src/HOL/Library/RBT_Mapping.thy Fri Apr 13 12:09:25 2012 +0200
5.2 +++ b/src/HOL/Library/RBT_Mapping.thy Fri Apr 13 13:30:27 2012 +0200
5.3 @@ -40,7 +40,7 @@
5.4
5.5 lemma keys_Mapping [code]:
5.6 "Mapping.keys (Mapping t) = set (keys t)"
5.7 - by (simp add: RBT.keys_def Mapping_def Mapping.keys_def lookup_def lookup_keys)
5.8 + by (simp add: RBT.keys_def Mapping_def Mapping.keys_def lookup_def rbt_lookup_keys)
5.9
5.10 lemma ordered_keys_Mapping [code]:
5.11 "Mapping.ordered_keys (Mapping t) = keys t"
5.12 @@ -144,22 +144,22 @@
5.13 @{thm Empty_is_rbt}\hfill(@{text "Empty_is_rbt"})
5.14
5.15 \noindent
5.16 - @{thm insert_is_rbt}\hfill(@{text "insert_is_rbt"})
5.17 + @{thm rbt_insert_is_rbt}\hfill(@{text "rbt_insert_is_rbt"})
5.18
5.19 \noindent
5.20 - @{thm delete_is_rbt}\hfill(@{text "delete_is_rbt"})
5.21 + @{thm rbt_delete_is_rbt}\hfill(@{text "delete_is_rbt"})
5.22
5.23 \noindent
5.24 - @{thm bulkload_is_rbt}\hfill(@{text "bulkload_is_rbt"})
5.25 + @{thm rbt_bulkload_is_rbt}\hfill(@{text "bulkload_is_rbt"})
5.26
5.27 \noindent
5.28 - @{thm map_entry_is_rbt}\hfill(@{text "map_entry_is_rbt"})
5.29 + @{thm rbt_map_entry_is_rbt}\hfill(@{text "map_entry_is_rbt"})
5.30
5.31 \noindent
5.32 @{thm map_is_rbt}\hfill(@{text "map_is_rbt"})
5.33
5.34 \noindent
5.35 - @{thm union_is_rbt}\hfill(@{text "union_is_rbt"})
5.36 + @{thm rbt_union_is_rbt}\hfill(@{text "union_is_rbt"})
5.37 *}
5.38
5.39
6.1 --- a/src/HOL/Quotient_Examples/Lift_RBT.thy Fri Apr 13 12:09:25 2012 +0200
6.2 +++ b/src/HOL/Quotient_Examples/Lift_RBT.thy Fri Apr 13 13:30:27 2012 +0200
6.3 @@ -37,16 +37,16 @@
6.4
6.5 setup_lifting type_definition_rbt
6.6
6.7 -lift_definition lookup :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'a \<rightharpoonup> 'b" is "RBT_Impl.lookup"
6.8 +lift_definition lookup :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'a \<rightharpoonup> 'b" is "rbt_lookup"
6.9 by simp
6.10
6.11 lift_definition empty :: "('a\<Colon>linorder, 'b) rbt" is RBT_Impl.Empty
6.12 by (simp add: empty_def)
6.13
6.14 -lift_definition insert :: "'a\<Colon>linorder \<Rightarrow> 'b \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt" is "RBT_Impl.insert"
6.15 +lift_definition insert :: "'a\<Colon>linorder \<Rightarrow> 'b \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt" is "rbt_insert"
6.16 by simp
6.17
6.18 -lift_definition delete :: "'a\<Colon>linorder \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt" is "RBT_Impl.delete"
6.19 +lift_definition delete :: "'a\<Colon>linorder \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt" is "rbt_delete"
6.20 by simp
6.21
6.22 lift_definition entries :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a \<times> 'b) list" is RBT_Impl.entries
6.23 @@ -55,10 +55,10 @@
6.24 lift_definition keys :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'a list" is RBT_Impl.keys
6.25 by simp
6.26
6.27 -lift_definition bulkload :: "('a\<Colon>linorder \<times> 'b) list \<Rightarrow> ('a, 'b) rbt" is "RBT_Impl.bulkload"
6.28 +lift_definition bulkload :: "('a\<Colon>linorder \<times> 'b) list \<Rightarrow> ('a, 'b) rbt" is "rbt_bulkload"
6.29 by simp
6.30
6.31 -lift_definition map_entry :: "'a \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a, 'b) rbt" is RBT_Impl.map_entry
6.32 +lift_definition map_entry :: "'a \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a, 'b) rbt" is rbt_map_entry
6.33 by simp
6.34
6.35 lift_definition map :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a, 'b) rbt" is RBT_Impl.map
6.36 @@ -80,11 +80,11 @@
6.37 (* TODO: obtain the following lemmas by lifting existing theorems. *)
6.38
6.39 lemma lookup_RBT:
6.40 - "is_rbt t \<Longrightarrow> lookup (RBT t) = RBT_Impl.lookup t"
6.41 + "is_rbt t \<Longrightarrow> lookup (RBT t) = rbt_lookup t"
6.42 by (simp add: lookup_def RBT_inverse)
6.43
6.44 lemma lookup_impl_of:
6.45 - "RBT_Impl.lookup (impl_of t) = lookup t"
6.46 + "rbt_lookup (impl_of t) = lookup t"
6.47 by (simp add: lookup_def)
6.48
6.49 lemma entries_impl_of:
6.50 @@ -101,11 +101,11 @@
6.51
6.52 lemma lookup_insert [simp]:
6.53 "lookup (insert k v t) = (lookup t)(k \<mapsto> v)"
6.54 - by (simp add: insert_def lookup_RBT lookup_insert lookup_impl_of)
6.55 + by (simp add: insert_def lookup_RBT rbt_lookup_rbt_insert lookup_impl_of)
6.56
6.57 lemma lookup_delete [simp]:
6.58 "lookup (delete k t) = (lookup t)(k := None)"
6.59 - by (simp add: delete_def lookup_RBT RBT_Impl.lookup_delete lookup_impl_of restrict_complement_singleton_eq)
6.60 + by (simp add: delete_def lookup_RBT rbt_lookup_rbt_delete lookup_impl_of restrict_complement_singleton_eq)
6.61
6.62 lemma map_of_entries [simp]:
6.63 "map_of (entries t) = lookup t"
6.64 @@ -113,19 +113,19 @@
6.65
6.66 lemma entries_lookup:
6.67 "entries t1 = entries t2 \<longleftrightarrow> lookup t1 = lookup t2"
6.68 - by (simp add: entries_def lookup_def entries_lookup)
6.69 + by (simp add: entries_def lookup_def entries_rbt_lookup)
6.70
6.71 lemma lookup_bulkload [simp]:
6.72 "lookup (bulkload xs) = map_of xs"
6.73 - by (simp add: bulkload_def lookup_RBT RBT_Impl.lookup_bulkload)
6.74 + by (simp add: bulkload_def lookup_RBT rbt_lookup_rbt_bulkload)
6.75
6.76 lemma lookup_map_entry [simp]:
6.77 "lookup (map_entry k f t) = (lookup t)(k := Option.map f (lookup t k))"
6.78 - by (simp add: map_entry_def lookup_RBT RBT_Impl.lookup_map_entry lookup_impl_of)
6.79 + by (simp add: map_entry_def lookup_RBT rbt_lookup_rbt_map_entry lookup_impl_of)
6.80
6.81 lemma lookup_map [simp]:
6.82 "lookup (map f t) k = Option.map (f k) (lookup t k)"
6.83 - by (simp add: map_def lookup_RBT RBT_Impl.lookup_map lookup_impl_of)
6.84 + by (simp add: map_def lookup_RBT rbt_lookup_map lookup_impl_of)
6.85
6.86 lemma fold_fold:
6.87 "fold f t = List.fold (prod_case f) (entries t)"
6.88 @@ -140,7 +140,7 @@
6.89 by (simp add: rbt_eq_iff is_empty_def impl_of_empty split: rbt.split)
6.90
6.91 lemma RBT_lookup_empty [simp]: (*FIXME*)
6.92 - "RBT_Impl.lookup t = Map.empty \<longleftrightarrow> t = RBT_Impl.Empty"
6.93 + "rbt_lookup t = Map.empty \<longleftrightarrow> t = RBT_Impl.Empty"
6.94 by (cases t) (auto simp add: fun_eq_iff)
6.95
6.96 lemma lookup_empty_empty [simp]:
6.97 @@ -149,7 +149,7 @@
6.98
6.99 lemma sorted_keys [iff]:
6.100 "sorted (keys t)"
6.101 - by (simp add: keys_def RBT_Impl.keys_def sorted_entries)
6.102 + by (simp add: keys_def RBT_Impl.keys_def rbt_sorted_entries)
6.103
6.104 lemma distinct_keys [iff]:
6.105 "distinct (keys t)"