author  haftmann 
Sat, 17 Oct 2015 13:18:43 +0200  
changeset 61433  a4c0de1df3d8 
parent 61225  1a690dce8cfc 
child 61585  a9599d3d7610 
permissions  rwrr 
47455  1 
(* Title: HOL/Library/RBT_Impl.thy 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

2 
Author: Markus Reiter, TU Muenchen 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

3 
Author: Alexander Krauss, TU Muenchen 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

4 
*) 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

5 

60500  6 
section \<open>Implementation of RedBlack Trees\<close> 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

7 

36147
b43b22f63665
theory RBT with abstract type of redblack trees backed by implementation RBT_Impl
haftmann
parents:
35618
diff
changeset

8 
theory RBT_Impl 
45990
b7b905b23b2a
incorporated More_Set and More_List into the Main body  to be consolidated later
haftmann
parents:
41959
diff
changeset

9 
imports Main 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

10 
begin 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

11 

60500  12 
text \<open> 
36147
b43b22f63665
theory RBT with abstract type of redblack trees backed by implementation RBT_Impl
haftmann
parents:
35618
diff
changeset

13 
For applications, you should use theory @{text RBT} which defines 
b43b22f63665
theory RBT with abstract type of redblack trees backed by implementation RBT_Impl
haftmann
parents:
35618
diff
changeset

14 
an abstract type of redblack tree obeying the invariant. 
60500  15 
\<close> 
36147
b43b22f63665
theory RBT with abstract type of redblack trees backed by implementation RBT_Impl
haftmann
parents:
35618
diff
changeset

16 

60500  17 
subsection \<open>Datatype of RB trees\<close> 
35550  18 

58310  19 
datatype color = R  B 
20 
datatype ('a, 'b) rbt = Empty  Branch color "('a, 'b) rbt" 'a 'b "('a, 'b) rbt" 

35534  21 

22 
lemma rbt_cases: 

23 
obtains (Empty) "t = Empty" 

24 
 (Red) l k v r where "t = Branch R l k v r" 

25 
 (Black) l k v r where "t = Branch B l k v r" 

26 
proof (cases t) 

27 
case Empty with that show thesis by blast 

28 
next 

29 
case (Branch c) with that show thesis by (cases c) blast+ 

30 
qed 

31 

60500  32 
subsection \<open>Tree properties\<close> 
35534  33 

60500  34 
subsubsection \<open>Content of a tree\<close> 
35550  35 

36 
primrec entries :: "('a, 'b) rbt \<Rightarrow> ('a \<times> 'b) list" 

35534  37 
where 
38 
"entries Empty = []" 

39 
 "entries (Branch _ l k v r) = entries l @ (k,v) # entries r" 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

40 

35550  41 
abbreviation (input) entry_in_tree :: "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b) rbt \<Rightarrow> bool" 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

42 
where 
35550  43 
"entry_in_tree k v t \<equiv> (k, v) \<in> set (entries t)" 
44 

45 
definition keys :: "('a, 'b) rbt \<Rightarrow> 'a list" where 

46 
"keys t = map fst (entries t)" 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

47 

35550  48 
lemma keys_simps [simp, code]: 
49 
"keys Empty = []" 

50 
"keys (Branch c l k v r) = keys l @ k # keys r" 

51 
by (simp_all add: keys_def) 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

52 

35534  53 
lemma entry_in_tree_keys: 
35550  54 
assumes "(k, v) \<in> set (entries t)" 
55 
shows "k \<in> set (keys t)" 

56 
proof  

57 
from assms have "fst (k, v) \<in> fst ` set (entries t)" by (rule imageI) 

58 
then show ?thesis by (simp add: keys_def) 

59 
qed 

60 

35602  61 
lemma keys_entries: 
62 
"k \<in> set (keys t) \<longleftrightarrow> (\<exists>v. (k, v) \<in> set (entries t))" 

63 
by (auto intro: entry_in_tree_keys) (auto simp add: keys_def) 

64 

48621
877df57629e3
a couple of additions to RBT formalization to allow us to implement RBT_Set
kuncar
parents:
47455
diff
changeset

65 
lemma non_empty_rbt_keys: 
877df57629e3
a couple of additions to RBT formalization to allow us to implement RBT_Set
kuncar
parents:
47455
diff
changeset

66 
"t \<noteq> rbt.Empty \<Longrightarrow> keys t \<noteq> []" 
877df57629e3
a couple of additions to RBT formalization to allow us to implement RBT_Set
kuncar
parents:
47455
diff
changeset

67 
by (cases t) simp_all 
35550  68 

60500  69 
subsubsection \<open>Search tree properties\<close> 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

70 

47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

71 
context ord begin 
35534  72 

47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

73 
definition rbt_less :: "'a \<Rightarrow> ('a, 'b) rbt \<Rightarrow> bool" 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

74 
where 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

75 
rbt_less_prop: "rbt_less k t \<longleftrightarrow> (\<forall>x\<in>set (keys t). x < k)" 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

76 

47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

77 
abbreviation rbt_less_symbol (infix "\<guillemotleft>" 50) 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

78 
where "t \<guillemotleft> x \<equiv> rbt_less x t" 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

79 

2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

80 
definition rbt_greater :: "'a \<Rightarrow> ('a, 'b) rbt \<Rightarrow> bool" (infix "\<guillemotleft>" 50) 
35534  81 
where 
47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

82 
rbt_greater_prop: "rbt_greater k t = (\<forall>x\<in>set (keys t). k < x)" 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

83 

47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

84 
lemma rbt_less_simps [simp]: 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

85 
"Empty \<guillemotleft> k = True" 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

86 
"Branch c lt kt v rt \<guillemotleft> k \<longleftrightarrow> kt < k \<and> lt \<guillemotleft> k \<and> rt \<guillemotleft> k" 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

87 
by (auto simp add: rbt_less_prop) 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

88 

47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

89 
lemma rbt_greater_simps [simp]: 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

90 
"k \<guillemotleft> Empty = True" 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

91 
"k \<guillemotleft> (Branch c lt kt v rt) \<longleftrightarrow> k < kt \<and> k \<guillemotleft> lt \<and> k \<guillemotleft> rt" 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

92 
by (auto simp add: rbt_greater_prop) 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

93 

47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

94 
lemmas rbt_ord_props = rbt_less_prop rbt_greater_prop 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

95 

2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

96 
lemmas rbt_greater_nit = rbt_greater_prop entry_in_tree_keys 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

97 
lemmas rbt_less_nit = rbt_less_prop entry_in_tree_keys 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

98 

47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

99 
lemma (in order) 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

100 
shows rbt_less_eq_trans: "l \<guillemotleft> u \<Longrightarrow> u \<le> v \<Longrightarrow> l \<guillemotleft> v" 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

101 
and rbt_less_trans: "t \<guillemotleft> x \<Longrightarrow> x < y \<Longrightarrow> t \<guillemotleft> y" 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

102 
and rbt_greater_eq_trans: "u \<le> v \<Longrightarrow> v \<guillemotleft> r \<Longrightarrow> u \<guillemotleft> r" 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

103 
and rbt_greater_trans: "x < y \<Longrightarrow> y \<guillemotleft> t \<Longrightarrow> x \<guillemotleft> t" 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

104 
by (auto simp: rbt_ord_props) 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

105 

47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

106 
primrec rbt_sorted :: "('a, 'b) rbt \<Rightarrow> bool" 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

107 
where 
47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

108 
"rbt_sorted Empty = True" 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

109 
 "rbt_sorted (Branch c l k v r) = (l \<guillemotleft> k \<and> k \<guillemotleft> r \<and> rbt_sorted l \<and> rbt_sorted r)" 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

110 

2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

111 
end 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

112 

47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

113 
context linorder begin 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

114 

2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

115 
lemma rbt_sorted_entries: 
49770
cf6a78acf445
efficient construction of red black trees from sorted associative lists
Andreas Lochbihler
parents:
49480
diff
changeset

116 
"rbt_sorted t \<Longrightarrow> List.sorted (map fst (entries t))" 
35550  117 
by (induct t) 
47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

118 
(force simp: sorted_append sorted_Cons rbt_ord_props 
35550  119 
dest!: entry_in_tree_keys)+ 
120 

121 
lemma distinct_entries: 

49770
cf6a78acf445
efficient construction of red black trees from sorted associative lists
Andreas Lochbihler
parents:
49480
diff
changeset

122 
"rbt_sorted t \<Longrightarrow> distinct (map fst (entries t))" 
35550  123 
by (induct t) 
47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

124 
(force simp: sorted_append sorted_Cons rbt_ord_props 
35550  125 
dest!: entry_in_tree_keys)+ 
126 

48621
877df57629e3
a couple of additions to RBT formalization to allow us to implement RBT_Set
kuncar
parents:
47455
diff
changeset

127 
lemma distinct_keys: 
877df57629e3
a couple of additions to RBT formalization to allow us to implement RBT_Set
kuncar
parents:
47455
diff
changeset

128 
"rbt_sorted t \<Longrightarrow> distinct (keys t)" 
877df57629e3
a couple of additions to RBT formalization to allow us to implement RBT_Set
kuncar
parents:
47455
diff
changeset

129 
by (simp add: distinct_entries keys_def) 
877df57629e3
a couple of additions to RBT formalization to allow us to implement RBT_Set
kuncar
parents:
47455
diff
changeset

130 

877df57629e3
a couple of additions to RBT formalization to allow us to implement RBT_Set
kuncar
parents:
47455
diff
changeset

131 

60500  132 
subsubsection \<open>Tree lookup\<close> 
35550  133 

47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

134 
primrec (in ord) rbt_lookup :: "('a, 'b) rbt \<Rightarrow> 'a \<rightharpoonup> 'b" 
35534  135 
where 
47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

136 
"rbt_lookup Empty k = None" 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

137 
 "rbt_lookup (Branch _ l x y r) k = 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

138 
(if k < x then rbt_lookup l k else if x < k then rbt_lookup r k else Some y)" 
35534  139 

47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

140 
lemma rbt_lookup_keys: "rbt_sorted t \<Longrightarrow> dom (rbt_lookup t) = set (keys t)" 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

141 
by (induct t) (auto simp: dom_def rbt_greater_prop rbt_less_prop) 
35550  142 

47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

143 
lemma dom_rbt_lookup_Branch: 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

144 
"rbt_sorted (Branch c t1 k v t2) \<Longrightarrow> 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

145 
dom (rbt_lookup (Branch c t1 k v t2)) 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

146 
= Set.insert k (dom (rbt_lookup t1) \<union> dom (rbt_lookup t2))" 
35550  147 
proof  
47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

148 
assume "rbt_sorted (Branch c t1 k v t2)" 
53374
a14d2a854c02
tuned proofs  clarified flow of facts wrt. calculation;
wenzelm
parents:
49810
diff
changeset

149 
then show ?thesis by (simp add: rbt_lookup_keys) 
35550  150 
qed 
151 

47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

152 
lemma finite_dom_rbt_lookup [simp, intro!]: "finite (dom (rbt_lookup t))" 
35550  153 
proof (induct t) 
154 
case Empty then show ?case by simp 

155 
next 

156 
case (Branch color t1 a b t2) 

47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

157 
let ?A = "Set.insert a (dom (rbt_lookup t1) \<union> dom (rbt_lookup t2))" 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

158 
have "dom (rbt_lookup (Branch color t1 a b t2)) \<subseteq> ?A" by (auto split: split_if_asm) 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

159 
moreover from Branch have "finite (insert a (dom (rbt_lookup t1) \<union> dom (rbt_lookup t2)))" by simp 
35550  160 
ultimately show ?case by (rule finite_subset) 
161 
qed 

162 

47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

163 
end 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

164 

2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

165 
context ord begin 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

166 

2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

167 
lemma rbt_lookup_rbt_less[simp]: "t \<guillemotleft> k \<Longrightarrow> rbt_lookup t k = None" 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

168 
by (induct t) auto 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

169 

47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

170 
lemma rbt_lookup_rbt_greater[simp]: "k \<guillemotleft> t \<Longrightarrow> rbt_lookup t k = None" 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

171 
by (induct t) auto 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

172 

47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

173 
lemma rbt_lookup_Empty: "rbt_lookup Empty = empty" 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

174 
by (rule ext) simp 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

175 

47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

176 
end 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

177 

2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

178 
context linorder begin 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

179 

35618  180 
lemma map_of_entries: 
47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

181 
"rbt_sorted t \<Longrightarrow> map_of (entries t) = rbt_lookup t" 
35550  182 
proof (induct t) 
47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

183 
case Empty thus ?case by (simp add: rbt_lookup_Empty) 
35550  184 
next 
185 
case (Branch c t1 k v t2) 

47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

186 
have "rbt_lookup (Branch c t1 k v t2) = rbt_lookup t2 ++ [k\<mapsto>v] ++ rbt_lookup t1" 
35550  187 
proof (rule ext) 
188 
fix x 

47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

189 
from Branch have RBT_SORTED: "rbt_sorted (Branch c t1 k v t2)" by simp 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

190 
let ?thesis = "rbt_lookup (Branch c t1 k v t2) x = (rbt_lookup t2 ++ [k \<mapsto> v] ++ rbt_lookup t1) x" 
35550  191 

47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

192 
have DOM_T1: "!!k'. k'\<in>dom (rbt_lookup t1) \<Longrightarrow> k>k'" 
35550  193 
proof  
194 
fix k' 

47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

195 
from RBT_SORTED have "t1 \<guillemotleft> k" by simp 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

196 
with rbt_less_prop have "\<forall>k'\<in>set (keys t1). k>k'" by auto 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

197 
moreover assume "k'\<in>dom (rbt_lookup t1)" 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

198 
ultimately show "k>k'" using rbt_lookup_keys RBT_SORTED by auto 
35550  199 
qed 
200 

47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

201 
have DOM_T2: "!!k'. k'\<in>dom (rbt_lookup t2) \<Longrightarrow> k<k'" 
35550  202 
proof  
203 
fix k' 

47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

204 
from RBT_SORTED have "k \<guillemotleft> t2" by simp 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

205 
with rbt_greater_prop have "\<forall>k'\<in>set (keys t2). k<k'" by auto 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

206 
moreover assume "k'\<in>dom (rbt_lookup t2)" 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

207 
ultimately show "k<k'" using rbt_lookup_keys RBT_SORTED by auto 
35550  208 
qed 
209 

210 
{ 

211 
assume C: "x<k" 

47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

212 
hence "rbt_lookup (Branch c t1 k v t2) x = rbt_lookup t1 x" by simp 
35550  213 
moreover from C have "x\<notin>dom [k\<mapsto>v]" by simp 
47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

214 
moreover have "x \<notin> dom (rbt_lookup t2)" 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

215 
proof 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

216 
assume "x \<in> dom (rbt_lookup t2)" 
35550  217 
with DOM_T2 have "k<x" by blast 
218 
with C show False by simp 

219 
qed 

220 
ultimately have ?thesis by (simp add: map_add_upd_left map_add_dom_app_simps) 

221 
} moreover { 

222 
assume [simp]: "x=k" 

47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

223 
hence "rbt_lookup (Branch c t1 k v t2) x = [k \<mapsto> v] x" by simp 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

224 
moreover have "x \<notin> dom (rbt_lookup t1)" 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

225 
proof 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

226 
assume "x \<in> dom (rbt_lookup t1)" 
35550  227 
with DOM_T1 have "k>x" by blast 
228 
thus False by simp 

229 
qed 

230 
ultimately have ?thesis by (simp add: map_add_upd_left map_add_dom_app_simps) 

231 
} moreover { 

232 
assume C: "x>k" 

47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

233 
hence "rbt_lookup (Branch c t1 k v t2) x = rbt_lookup t2 x" by (simp add: less_not_sym[of k x]) 
35550  234 
moreover from C have "x\<notin>dom [k\<mapsto>v]" by simp 
47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

235 
moreover have "x\<notin>dom (rbt_lookup t1)" proof 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

236 
assume "x\<in>dom (rbt_lookup t1)" 
35550  237 
with DOM_T1 have "k>x" by simp 
238 
with C show False by simp 

239 
qed 

240 
ultimately have ?thesis by (simp add: map_add_upd_left map_add_dom_app_simps) 

241 
} ultimately show ?thesis using less_linear by blast 

242 
qed 

47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

243 
also from Branch 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

244 
have "rbt_lookup t2 ++ [k \<mapsto> v] ++ rbt_lookup t1 = map_of (entries (Branch c t1 k v t2))" by simp 
35618  245 
finally show ?case by simp 
35550  246 
qed 
247 

47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

248 
lemma rbt_lookup_in_tree: "rbt_sorted t \<Longrightarrow> rbt_lookup t k = Some v \<longleftrightarrow> (k, v) \<in> set (entries t)" 
35618  249 
by (simp add: map_of_entries [symmetric] distinct_entries) 
35602  250 

251 
lemma set_entries_inject: 

47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

252 
assumes rbt_sorted: "rbt_sorted t1" "rbt_sorted t2" 
35602  253 
shows "set (entries t1) = set (entries t2) \<longleftrightarrow> entries t1 = entries t2" 
254 
proof  

47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

255 
from rbt_sorted have "distinct (map fst (entries t1))" 
35602  256 
"distinct (map fst (entries t2))" 
257 
by (auto intro: distinct_entries) 

47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

258 
with rbt_sorted show ?thesis 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

259 
by (auto intro: map_sorted_distinct_set_unique rbt_sorted_entries simp add: distinct_map) 
35602  260 
qed 
35550  261 

262 
lemma entries_eqI: 

47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

263 
assumes rbt_sorted: "rbt_sorted t1" "rbt_sorted t2" 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

264 
assumes rbt_lookup: "rbt_lookup t1 = rbt_lookup t2" 
35602  265 
shows "entries t1 = entries t2" 
35550  266 
proof  
47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

267 
from rbt_sorted rbt_lookup have "map_of (entries t1) = map_of (entries t2)" 
35618  268 
by (simp add: map_of_entries) 
47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

269 
with rbt_sorted have "set (entries t1) = set (entries t2)" 
35602  270 
by (simp add: map_of_inject_set distinct_entries) 
47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

271 
with rbt_sorted show ?thesis by (simp add: set_entries_inject) 
35602  272 
qed 
35550  273 

47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

274 
lemma entries_rbt_lookup: 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

275 
assumes "rbt_sorted t1" "rbt_sorted t2" 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

276 
shows "entries t1 = entries t2 \<longleftrightarrow> rbt_lookup t1 = rbt_lookup t2" 
35618  277 
using assms by (auto intro: entries_eqI simp add: map_of_entries [symmetric]) 
35602  278 

47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

279 
lemma rbt_lookup_from_in_tree: 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

280 
assumes "rbt_sorted t1" "rbt_sorted t2" 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

281 
and "\<And>v. (k, v) \<in> set (entries t1) \<longleftrightarrow> (k, v) \<in> set (entries t2)" 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

282 
shows "rbt_lookup t1 k = rbt_lookup t2 k" 
35602  283 
proof  
47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

284 
from assms have "k \<in> dom (rbt_lookup t1) \<longleftrightarrow> k \<in> dom (rbt_lookup t2)" 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

285 
by (simp add: keys_entries rbt_lookup_keys) 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

286 
with assms show ?thesis by (auto simp add: rbt_lookup_in_tree [symmetric]) 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

287 
qed 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

288 

47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

289 
end 
35550  290 

60500  291 
subsubsection \<open>Redblack properties\<close> 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

292 

35534  293 
primrec color_of :: "('a, 'b) rbt \<Rightarrow> color" 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

294 
where 
35534  295 
"color_of Empty = B" 
296 
 "color_of (Branch c _ _ _ _) = c" 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

297 

35534  298 
primrec bheight :: "('a,'b) rbt \<Rightarrow> nat" 
299 
where 

300 
"bheight Empty = 0" 

301 
 "bheight (Branch c lt k v rt) = (if c = B then Suc (bheight lt) else bheight lt)" 

302 

303 
primrec inv1 :: "('a, 'b) rbt \<Rightarrow> bool" 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

304 
where 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

305 
"inv1 Empty = True" 
35534  306 
 "inv1 (Branch c lt k v rt) \<longleftrightarrow> inv1 lt \<and> inv1 rt \<and> (c = B \<or> color_of lt = B \<and> color_of rt = B)" 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

307 

60500  308 
primrec inv1l :: "('a, 'b) rbt \<Rightarrow> bool"  \<open>Weaker version\<close> 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

309 
where 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

310 
"inv1l Empty = True" 
35534  311 
 "inv1l (Branch c l k v r) = (inv1 l \<and> inv1 r)" 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

312 
lemma [simp]: "inv1 t \<Longrightarrow> inv1l t" by (cases t) simp+ 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

313 

35534  314 
primrec inv2 :: "('a, 'b) rbt \<Rightarrow> bool" 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

315 
where 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

316 
"inv2 Empty = True" 
35534  317 
 "inv2 (Branch c lt k v rt) = (inv2 lt \<and> inv2 rt \<and> bheight lt = bheight rt)" 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

318 

47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

319 
context ord begin 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

320 

47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

321 
definition is_rbt :: "('a, 'b) rbt \<Rightarrow> bool" where 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

322 
"is_rbt t \<longleftrightarrow> inv1 t \<and> inv2 t \<and> color_of t = B \<and> rbt_sorted t" 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

323 

2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

324 
lemma is_rbt_rbt_sorted [simp]: 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

325 
"is_rbt t \<Longrightarrow> rbt_sorted t" by (simp add: is_rbt_def) 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

326 

35534  327 
theorem Empty_is_rbt [simp]: 
328 
"is_rbt Empty" by (simp add: is_rbt_def) 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

329 

47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

330 
end 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

331 

60500  332 
subsection \<open>Insertion\<close> 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

333 

61225  334 
text \<open>The function definitions are based on the book by Okasaki.\<close> 
335 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

336 
fun (* slow, due to massive case splitting *) 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

337 
balance :: "('a,'b) rbt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt" 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

338 
where 
35534  339 
"balance (Branch R a w x b) s t (Branch R c y z d) = Branch R (Branch B a w x b) s t (Branch B c y z d)"  
340 
"balance (Branch R (Branch R a w x b) s t c) y z d = Branch R (Branch B a w x b) s t (Branch B c y z d)"  

341 
"balance (Branch R a w x (Branch R b s t c)) y z d = Branch R (Branch B a w x b) s t (Branch B c y z d)"  

342 
"balance a w x (Branch R b s t (Branch R c y z d)) = Branch R (Branch B a w x b) s t (Branch B c y z d)"  

343 
"balance a w x (Branch R (Branch R b s t c) y z d) = Branch R (Branch B a w x b) s t (Branch B c y z d)"  

344 
"balance a s t b = Branch B a s t b" 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

345 

52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

346 
lemma balance_inv1: "\<lbrakk>inv1l l; inv1l r\<rbrakk> \<Longrightarrow> inv1 (balance l k v r)" 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

347 
by (induct l k v r rule: balance.induct) auto 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

348 

35534  349 
lemma balance_bheight: "bheight l = bheight r \<Longrightarrow> bheight (balance l k v r) = Suc (bheight l)" 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

350 
by (induct l k v r rule: balance.induct) auto 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

351 

52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

352 
lemma balance_inv2: 
35534  353 
assumes "inv2 l" "inv2 r" "bheight l = bheight r" 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

354 
shows "inv2 (balance l k v r)" 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

355 
using assms 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

356 
by (induct l k v r rule: balance.induct) auto 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

357 

47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

358 
context ord begin 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

359 

2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

360 
lemma balance_rbt_greater[simp]: "(v \<guillemotleft> balance a k x b) = (v \<guillemotleft> a \<and> v \<guillemotleft> b \<and> v < k)" 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

361 
by (induct a k x b rule: balance.induct) auto 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

362 

47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

363 
lemma balance_rbt_less[simp]: "(balance a k x b \<guillemotleft> v) = (a \<guillemotleft> v \<and> b \<guillemotleft> v \<and> k < v)" 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

364 
by (induct a k x b rule: balance.induct) auto 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

365 

47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

366 
end 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

367 

2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

368 
lemma (in linorder) balance_rbt_sorted: 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

369 
fixes k :: "'a" 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

370 
assumes "rbt_sorted l" "rbt_sorted r" "l \<guillemotleft> k" "k \<guillemotleft> r" 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

371 
shows "rbt_sorted (balance l k v r)" 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

372 
using assms proof (induct l k v r rule: balance.induct) 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

373 
case ("2_2" a x w b y t c z s va vb vd vc) 
35534  374 
hence "y < z \<and> z \<guillemotleft> Branch B va vb vd vc" 
47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

375 
by (auto simp add: rbt_ord_props) 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

376 
hence "y \<guillemotleft> (Branch B va vb vd vc)" by (blast dest: rbt_greater_trans) 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

377 
with "2_2" show ?case by simp 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

378 
next 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

379 
case ("3_2" va vb vd vc x w b y s c z) 
47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

380 
from "3_2" have "x < y \<and> Branch B va vb vd vc \<guillemotleft> x" 
35534  381 
by simp 
47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

382 
hence "Branch B va vb vd vc \<guillemotleft> y" by (blast dest: rbt_less_trans) 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

383 
with "3_2" show ?case by simp 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

384 
next 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

385 
case ("3_3" x w b y s c z t va vb vd vc) 
47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

386 
from "3_3" have "y < z \<and> z \<guillemotleft> Branch B va vb vd vc" by simp 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

387 
hence "y \<guillemotleft> Branch B va vb vd vc" by (blast dest: rbt_greater_trans) 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

388 
with "3_3" show ?case by simp 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

389 
next 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

390 
case ("3_4" vd ve vg vf x w b y s c z t va vb vii vc) 
47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

391 
hence "x < y \<and> Branch B vd ve vg vf \<guillemotleft> x" by simp 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

392 
hence 1: "Branch B vd ve vg vf \<guillemotleft> y" by (blast dest: rbt_less_trans) 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

393 
from "3_4" have "y < z \<and> z \<guillemotleft> Branch B va vb vii vc" by simp 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

394 
hence "y \<guillemotleft> Branch B va vb vii vc" by (blast dest: rbt_greater_trans) 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

395 
with 1 "3_4" show ?case by simp 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

396 
next 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

397 
case ("4_2" va vb vd vc x w b y s c z t dd) 
47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

398 
hence "x < y \<and> Branch B va vb vd vc \<guillemotleft> x" by simp 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

399 
hence "Branch B va vb vd vc \<guillemotleft> y" by (blast dest: rbt_less_trans) 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

400 
with "4_2" show ?case by simp 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

401 
next 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

402 
case ("5_2" x w b y s c z t va vb vd vc) 
47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

403 
hence "y < z \<and> z \<guillemotleft> Branch B va vb vd vc" by simp 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

404 
hence "y \<guillemotleft> Branch B va vb vd vc" by (blast dest: rbt_greater_trans) 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

405 
with "5_2" show ?case by simp 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

406 
next 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

407 
case ("5_3" va vb vd vc x w b y s c z t) 
47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

408 
hence "x < y \<and> Branch B va vb vd vc \<guillemotleft> x" by simp 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

409 
hence "Branch B va vb vd vc \<guillemotleft> y" by (blast dest: rbt_less_trans) 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

410 
with "5_3" show ?case by simp 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

411 
next 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

412 
case ("5_4" va vb vg vc x w b y s c z t vd ve vii vf) 
47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

413 
hence "x < y \<and> Branch B va vb vg vc \<guillemotleft> x" by simp 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

414 
hence 1: "Branch B va vb vg vc \<guillemotleft> y" by (blast dest: rbt_less_trans) 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

415 
from "5_4" have "y < z \<and> z \<guillemotleft> Branch B vd ve vii vf" by simp 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

416 
hence "y \<guillemotleft> Branch B vd ve vii vf" by (blast dest: rbt_greater_trans) 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

417 
with 1 "5_4" show ?case by simp 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

418 
qed simp+ 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

419 

35550  420 
lemma entries_balance [simp]: 
421 
"entries (balance l k v r) = entries l @ (k, v) # entries r" 

422 
by (induct l k v r rule: balance.induct) auto 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

423 

35550  424 
lemma keys_balance [simp]: 
425 
"keys (balance l k v r) = keys l @ k # keys r" 

426 
by (simp add: keys_def) 

427 

428 
lemma balance_in_tree: 

429 
"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" 

430 
by (auto simp add: keys_def) 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

431 

47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

432 
lemma (in linorder) rbt_lookup_balance[simp]: 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

433 
fixes k :: "'a" 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

434 
assumes "rbt_sorted l" "rbt_sorted r" "l \<guillemotleft> k" "k \<guillemotleft> r" 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

435 
shows "rbt_lookup (balance l k v r) x = rbt_lookup (Branch B l k v r) x" 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

436 
by (rule rbt_lookup_from_in_tree) (auto simp:assms balance_in_tree balance_rbt_sorted) 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

437 

52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

438 
primrec paint :: "color \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt" 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

439 
where 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

440 
"paint c Empty = Empty" 
35534  441 
 "paint c (Branch _ l k v r) = Branch c l k v r" 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

442 

52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

443 
lemma paint_inv1l[simp]: "inv1l t \<Longrightarrow> inv1l (paint c t)" by (cases t) auto 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

444 
lemma paint_inv1[simp]: "inv1l t \<Longrightarrow> inv1 (paint B t)" by (cases t) auto 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

445 
lemma paint_inv2[simp]: "inv2 t \<Longrightarrow> inv2 (paint c t)" by (cases t) auto 
35534  446 
lemma paint_color_of[simp]: "color_of (paint B t) = B" by (cases t) auto 
35550  447 
lemma paint_in_tree[simp]: "entry_in_tree k x (paint c t) = entry_in_tree k x t" by (cases t) auto 
47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

448 

2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

449 
context ord begin 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

450 

2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

451 
lemma paint_rbt_sorted[simp]: "rbt_sorted t \<Longrightarrow> rbt_sorted (paint c t)" by (cases t) auto 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

452 
lemma paint_rbt_lookup[simp]: "rbt_lookup (paint c t) = rbt_lookup t" by (rule ext) (cases t, auto) 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

453 
lemma paint_rbt_greater[simp]: "(v \<guillemotleft> paint c t) = (v \<guillemotleft> t)" by (cases t) auto 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

454 
lemma paint_rbt_less[simp]: "(paint c t \<guillemotleft> v) = (t \<guillemotleft> v)" by (cases t) auto 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

455 

52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

456 
fun 
47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

457 
rbt_ins :: "('a \<Rightarrow> 'b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt" 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

458 
where 
47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

459 
"rbt_ins f k v Empty = Branch R Empty k v Empty"  
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

460 
"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 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

461 
else if k > x then balance l x y (rbt_ins f k v r) 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

462 
else Branch B l x (f k y v) r)"  
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

463 
"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 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

464 
else if k > x then Branch R l x y (rbt_ins f k v r) 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

465 
else Branch R l x (f k y v) r)" 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

466 

52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

467 
lemma ins_inv1_inv2: 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

468 
assumes "inv1 t" "inv2 t" 
47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

469 
shows "inv2 (rbt_ins f k x t)" "bheight (rbt_ins f k x t) = bheight t" 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

470 
"color_of t = B \<Longrightarrow> inv1 (rbt_ins f k x t)" "inv1l (rbt_ins f k x t)" 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

471 
using assms 
47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

472 
by (induct f k x t rule: rbt_ins.induct) (auto simp: balance_inv1 balance_inv2 balance_bheight) 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

473 

2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

474 
end 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

475 

2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

476 
context linorder begin 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

477 

47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

478 
lemma ins_rbt_greater[simp]: "(v \<guillemotleft> rbt_ins f (k :: 'a) x t) = (v \<guillemotleft> t \<and> k > v)" 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

479 
by (induct f k x t rule: rbt_ins.induct) auto 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

480 
lemma ins_rbt_less[simp]: "(rbt_ins f k x t \<guillemotleft> v) = (t \<guillemotleft> v \<and> k < v)" 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

481 
by (induct f k x t rule: rbt_ins.induct) auto 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

482 
lemma ins_rbt_sorted[simp]: "rbt_sorted t \<Longrightarrow> rbt_sorted (rbt_ins f k x t)" 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

483 
by (induct f k x t rule: rbt_ins.induct) (auto simp: balance_rbt_sorted) 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

484 

47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

485 
lemma keys_ins: "set (keys (rbt_ins f k v t)) = { k } \<union> set (keys t)" 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

486 
by (induct f k v t rule: rbt_ins.induct) auto 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

487 

47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

488 
lemma rbt_lookup_ins: 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

489 
fixes k :: "'a" 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

490 
assumes "rbt_sorted t" 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

491 
shows "rbt_lookup (rbt_ins f k v t) x = ((rbt_lookup t)(k > case rbt_lookup t k of None \<Rightarrow> v 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

492 
 Some w \<Rightarrow> f k w v)) x" 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

493 
using assms by (induct f k v t rule: rbt_ins.induct) auto 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

494 

2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

495 
end 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

496 

2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

497 
context ord begin 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

498 

2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

499 
definition rbt_insert_with_key :: "('a \<Rightarrow> 'b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt" 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

500 
where "rbt_insert_with_key f k v t = paint B (rbt_ins f k v t)" 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

501 

2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

502 
definition rbt_insertw_def: "rbt_insert_with f = rbt_insert_with_key (\<lambda>_. f)" 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

503 

47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

504 
definition rbt_insert :: "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt" where 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

505 
"rbt_insert = rbt_insert_with_key (\<lambda>_ _ nv. nv)" 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

506 

2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

507 
end 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

508 

2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

509 
context linorder begin 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

510 

47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

511 
lemma rbt_insertwk_rbt_sorted: "rbt_sorted t \<Longrightarrow> rbt_sorted (rbt_insert_with_key f (k :: 'a) x t)" 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

512 
by (auto simp: rbt_insert_with_key_def) 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

513 

47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

514 
theorem rbt_insertwk_is_rbt: 
35534  515 
assumes inv: "is_rbt t" 
47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

516 
shows "is_rbt (rbt_insert_with_key f k x t)" 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

517 
using assms 
47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

518 
unfolding rbt_insert_with_key_def is_rbt_def 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

519 
by (auto simp: ins_inv1_inv2) 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

520 

47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

521 
lemma rbt_lookup_rbt_insertwk: 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

522 
assumes "rbt_sorted t" 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

523 
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 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

524 
 Some w \<Rightarrow> f k w v)) x" 
47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

525 
unfolding rbt_insert_with_key_def using assms 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

526 
by (simp add:rbt_lookup_ins) 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

527 

47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

528 
lemma rbt_insertw_rbt_sorted: "rbt_sorted t \<Longrightarrow> rbt_sorted (rbt_insert_with f k v t)" 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

529 
by (simp add: rbt_insertwk_rbt_sorted rbt_insertw_def) 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

530 
theorem rbt_insertw_is_rbt: "is_rbt t \<Longrightarrow> is_rbt (rbt_insert_with f k v t)" 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

531 
by (simp add: rbt_insertwk_is_rbt rbt_insertw_def) 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

532 

47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

533 
lemma rbt_lookup_rbt_insertw: 
35534  534 
assumes "is_rbt t" 
47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

535 
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))" 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

536 
using assms 
47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

537 
unfolding rbt_insertw_def 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

538 
by (rule_tac ext) (cases "rbt_lookup t k", auto simp:rbt_lookup_rbt_insertwk dom_def) 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

539 

47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

540 
lemma rbt_insert_rbt_sorted: "rbt_sorted t \<Longrightarrow> rbt_sorted (rbt_insert k v t)" 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

541 
by (simp add: rbt_insertwk_rbt_sorted rbt_insert_def) 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

542 
theorem rbt_insert_is_rbt [simp]: "is_rbt t \<Longrightarrow> is_rbt (rbt_insert k v t)" 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

543 
by (simp add: rbt_insertwk_is_rbt rbt_insert_def) 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

544 

47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

545 
lemma rbt_lookup_rbt_insert: 
35534  546 
assumes "is_rbt t" 
47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

547 
shows "rbt_lookup (rbt_insert k v t) = (rbt_lookup t)(k\<mapsto>v)" 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

548 
unfolding rbt_insert_def 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

549 
using assms 
47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

550 
by (rule_tac ext) (simp add: rbt_lookup_rbt_insertwk split:option.split) 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

551 

47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

552 
end 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

553 

60500  554 
subsection \<open>Deletion\<close> 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

555 

35534  556 
lemma bheight_paintR'[simp]: "color_of t = B \<Longrightarrow> bheight (paint R t) = bheight t  1" 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

557 
by (cases t rule: rbt_cases) auto 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

558 

61225  559 
text \<open>The function definitions are based on the Haskell code by Stefan Kahrs 
560 
at @{url "http://www.cs.ukc.ac.uk/people/staff/smk/redblack/rb.html"} .\<close> 

561 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

562 
fun 
35550  563 
balance_left :: "('a,'b) rbt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt" 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

564 
where 
35550  565 
"balance_left (Branch R a k x b) s y c = Branch R (Branch B a k x b) s y c"  
566 
"balance_left bl k x (Branch B a s y b) = balance bl k x (Branch R a s y b)"  

567 
"balance_left bl k x (Branch R (Branch B a s y b) t z c) = Branch R (Branch B bl k x a) s y (balance b t z (paint R c))"  

568 
"balance_left t k x s = Empty" 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

569 

35550  570 
lemma balance_left_inv2_with_inv1: 
35534  571 
assumes "inv2 lt" "inv2 rt" "bheight lt + 1 = bheight rt" "inv1 rt" 
35550  572 
shows "bheight (balance_left lt k v rt) = bheight lt + 1" 
573 
and "inv2 (balance_left lt k v rt)" 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

574 
using assms 
35550  575 
by (induct lt k v rt rule: balance_left.induct) (auto simp: balance_inv2 balance_bheight) 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

576 

35550  577 
lemma balance_left_inv2_app: 
35534  578 
assumes "inv2 lt" "inv2 rt" "bheight lt + 1 = bheight rt" "color_of rt = B" 
35550  579 
shows "inv2 (balance_left lt k v rt)" 
580 
"bheight (balance_left lt k v rt) = bheight rt" 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

581 
using assms 
35550  582 
by (induct lt k v rt rule: balance_left.induct) (auto simp add: balance_inv2 balance_bheight)+ 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

583 

35550  584 
lemma balance_left_inv1: "\<lbrakk>inv1l a; inv1 b; color_of b = B\<rbrakk> \<Longrightarrow> inv1 (balance_left a k x b)" 
585 
by (induct a k x b rule: balance_left.induct) (simp add: balance_inv1)+ 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

586 

35550  587 
lemma balance_left_inv1l: "\<lbrakk> inv1l lt; inv1 rt \<rbrakk> \<Longrightarrow> inv1l (balance_left lt k x rt)" 
588 
by (induct lt k x rt rule: balance_left.induct) (auto simp: balance_inv1) 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

589 

47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

590 
lemma (in linorder) balance_left_rbt_sorted: 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

591 
"\<lbrakk> rbt_sorted l; rbt_sorted r; rbt_less k l; k \<guillemotleft> r \<rbrakk> \<Longrightarrow> rbt_sorted (balance_left l k v r)" 
35550  592 
apply (induct l k v r rule: balance_left.induct) 
47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

593 
apply (auto simp: balance_rbt_sorted) 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

594 
apply (unfold rbt_greater_prop rbt_less_prop) 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

595 
by force+ 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

596 

47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

597 
context order begin 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

598 

2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

599 
lemma balance_left_rbt_greater: 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

600 
fixes k :: "'a" 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

601 
assumes "k \<guillemotleft> a" "k \<guillemotleft> b" "k < x" 
35550  602 
shows "k \<guillemotleft> balance_left a x t b" 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

603 
using assms 
35550  604 
by (induct a x t b rule: balance_left.induct) auto 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

605 

47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

606 
lemma balance_left_rbt_less: 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

607 
fixes k :: "'a" 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

608 
assumes "a \<guillemotleft> k" "b \<guillemotleft> k" "x < k" 
35550  609 
shows "balance_left a x t b \<guillemotleft> k" 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

610 
using assms 
35550  611 
by (induct a x t b rule: balance_left.induct) auto 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

612 

47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

613 
end 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

614 

35550  615 
lemma balance_left_in_tree: 
35534  616 
assumes "inv1l l" "inv1 r" "bheight l + 1 = bheight r" 
35550  617 
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)" 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

618 
using assms 
35550  619 
by (induct l k v r rule: balance_left.induct) (auto simp: balance_in_tree) 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

620 

52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

621 
fun 
35550  622 
balance_right :: "('a,'b) rbt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt" 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

623 
where 
35550  624 
"balance_right a k x (Branch R b s y c) = Branch R a k x (Branch B b s y c)"  
625 
"balance_right (Branch B a k x b) s y bl = balance (Branch R a k x b) s y bl"  

626 
"balance_right (Branch R a k x (Branch B b s y c)) t z bl = Branch R (balance (paint R a) k x b) s y (Branch B c t z bl)"  

627 
"balance_right t k x s = Empty" 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

628 

35550  629 
lemma balance_right_inv2_with_inv1: 
35534  630 
assumes "inv2 lt" "inv2 rt" "bheight lt = bheight rt + 1" "inv1 lt" 
35550  631 
shows "inv2 (balance_right lt k v rt) \<and> bheight (balance_right lt k v rt) = bheight lt" 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

632 
using assms 
35550  633 
by (induct lt k v rt rule: balance_right.induct) (auto simp: balance_inv2 balance_bheight) 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

634 

35550  635 
lemma balance_right_inv1: "\<lbrakk>inv1 a; inv1l b; color_of a = B\<rbrakk> \<Longrightarrow> inv1 (balance_right a k x b)" 
636 
by (induct a k x b rule: balance_right.induct) (simp add: balance_inv1)+ 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

637 

35550  638 
lemma balance_right_inv1l: "\<lbrakk> inv1 lt; inv1l rt \<rbrakk> \<Longrightarrow>inv1l (balance_right lt k x rt)" 
639 
by (induct lt k x rt rule: balance_right.induct) (auto simp: balance_inv1) 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

640 

47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

641 
lemma (in linorder) balance_right_rbt_sorted: 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

642 
"\<lbrakk> rbt_sorted l; rbt_sorted r; rbt_less k l; k \<guillemotleft> r \<rbrakk> \<Longrightarrow> rbt_sorted (balance_right l k v r)" 
35550  643 
apply (induct l k v r rule: balance_right.induct) 
47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

644 
apply (auto simp:balance_rbt_sorted) 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

645 
apply (unfold rbt_less_prop rbt_greater_prop) 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

646 
by force+ 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

647 

47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

648 
context order begin 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

649 

2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

650 
lemma balance_right_rbt_greater: 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

651 
fixes k :: "'a" 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

652 
assumes "k \<guillemotleft> a" "k \<guillemotleft> b" "k < x" 
35550  653 
shows "k \<guillemotleft> balance_right a x t b" 
654 
using assms by (induct a x t b rule: balance_right.induct) auto 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

655 

47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

656 
lemma balance_right_rbt_less: 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

657 
fixes k :: "'a" 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

658 
assumes "a \<guillemotleft> k" "b \<guillemotleft> k" "x < k" 
35550  659 
shows "balance_right a x t b \<guillemotleft> k" 
660 
using assms by (induct a x t b rule: balance_right.induct) auto 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

661 

47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

662 
end 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

663 

35550  664 
lemma balance_right_in_tree: 
35534  665 
assumes "inv1 l" "inv1l r" "bheight l = bheight r + 1" "inv2 l" "inv2 r" 
35550  666 
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)" 
667 
using assms by (induct l k v r rule: balance_right.induct) (auto simp: balance_in_tree) 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

668 

52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

669 
fun 
35550  670 
combine :: "('a,'b) rbt \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt" 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

671 
where 
35550  672 
"combine Empty x = x" 
673 
 "combine x Empty = x" 

674 
 "combine (Branch R a k x b) (Branch R c s y d) = (case (combine b c) of 

47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

675 
Branch R b2 t z c2 \<Rightarrow> (Branch R (Branch R a k x b2) t z (Branch R c2 s y d))  
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

676 
bc \<Rightarrow> Branch R a k x (Branch R bc s y d))" 
35550  677 
 "combine (Branch B a k x b) (Branch B c s y d) = (case (combine b c) of 
47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

678 
Branch R b2 t z c2 \<Rightarrow> Branch R (Branch B a k x b2) t z (Branch B c2 s y d)  
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

679 
bc \<Rightarrow> balance_left a k x (Branch B bc s y d))" 
35550  680 
 "combine a (Branch R b k x c) = Branch R (combine a b) k x c" 
681 
 "combine (Branch R a k x b) c = Branch R a k x (combine b c)" 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

682 

35550  683 
lemma combine_inv2: 
35534  684 
assumes "inv2 lt" "inv2 rt" "bheight lt = bheight rt" 
35550  685 
shows "bheight (combine lt rt) = bheight lt" "inv2 (combine lt rt)" 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

686 
using assms 
35550  687 
by (induct lt rt rule: combine.induct) 
688 
(auto simp: balance_left_inv2_app split: rbt.splits color.splits) 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

689 

35550  690 
lemma combine_inv1: 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

691 
assumes "inv1 lt" "inv1 rt" 
35550  692 
shows "color_of lt = B \<Longrightarrow> color_of rt = B \<Longrightarrow> inv1 (combine lt rt)" 
693 
"inv1l (combine lt rt)" 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

694 
using assms 
35550  695 
by (induct lt rt rule: combine.induct) 
696 
(auto simp: balance_left_inv1 split: rbt.splits color.splits) 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

697 

47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

698 
context linorder begin 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

699 

2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

700 
lemma combine_rbt_greater[simp]: 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

701 
fixes k :: "'a" 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

702 
assumes "k \<guillemotleft> l" "k \<guillemotleft> r" 
35550  703 
shows "k \<guillemotleft> combine l r" 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

704 
using assms 
35550  705 
by (induct l r rule: combine.induct) 
47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

706 
(auto simp: balance_left_rbt_greater split:rbt.splits color.splits) 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

707 

47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

708 
lemma combine_rbt_less[simp]: 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

709 
fixes k :: "'a" 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

710 
assumes "l \<guillemotleft> k" "r \<guillemotleft> k" 
35550  711 
shows "combine l r \<guillemotleft> k" 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

712 
using assms 
35550  713 
by (induct l r rule: combine.induct) 
47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

714 
(auto simp: balance_left_rbt_less split:rbt.splits color.splits) 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

715 

47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

716 
lemma combine_rbt_sorted: 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

717 
fixes k :: "'a" 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

718 
assumes "rbt_sorted l" "rbt_sorted r" "l \<guillemotleft> k" "k \<guillemotleft> r" 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

719 
shows "rbt_sorted (combine l r)" 
35550  720 
using assms proof (induct l r rule: combine.induct) 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

721 
case (3 a x v b c y w d) 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

722 
hence ineqs: "a \<guillemotleft> x" "x \<guillemotleft> b" "b \<guillemotleft> k" "k \<guillemotleft> c" "c \<guillemotleft> y" "y \<guillemotleft> d" 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

723 
by auto 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

724 
with 3 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

725 
show ?case 
35550  726 
by (cases "combine b c" rule: rbt_cases) 
47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

727 
(auto, (metis combine_rbt_greater combine_rbt_less ineqs ineqs rbt_less_simps(2) rbt_greater_simps(2) rbt_greater_trans rbt_less_trans)+) 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

728 
next 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

729 
case (4 a x v b c y w d) 
47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

730 
hence "x < k \<and> rbt_greater k c" by simp 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

731 
hence "rbt_greater x c" by (blast dest: rbt_greater_trans) 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

732 
with 4 have 2: "rbt_greater x (combine b c)" by (simp add: combine_rbt_greater) 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

733 
from 4 have "k < y \<and> rbt_less k b" by simp 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

734 
hence "rbt_less y b" by (blast dest: rbt_less_trans) 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

735 
with 4 have 3: "rbt_less y (combine b c)" by (simp add: combine_rbt_less) 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

736 
show ?case 
35550  737 
proof (cases "combine b c" rule: rbt_cases) 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

738 
case Empty 
47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

739 
from 4 have "x < y \<and> rbt_greater y d" by auto 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

740 
hence "rbt_greater x d" by (blast dest: rbt_greater_trans) 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

741 
with 4 Empty have "rbt_sorted a" and "rbt_sorted (Branch B Empty y w d)" 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

742 
and "rbt_less x a" and "rbt_greater x (Branch B Empty y w d)" by auto 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

743 
with Empty show ?thesis by (simp add: balance_left_rbt_sorted) 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

744 
next 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

745 
case (Red lta va ka rta) 
47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

746 
with 2 4 have "x < va \<and> rbt_less x a" by simp 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

747 
hence 5: "rbt_less va a" by (blast dest: rbt_less_trans) 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

748 
from Red 3 4 have "va < y \<and> rbt_greater y d" by simp 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

749 
hence "rbt_greater va d" by (blast dest: rbt_greater_trans) 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

750 
with Red 2 3 4 5 show ?thesis by simp 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

751 
next 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

752 
case (Black lta va ka rta) 
47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

753 
from 4 have "x < y \<and> rbt_greater y d" by auto 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

754 
hence "rbt_greater x d" by (blast dest: rbt_greater_trans) 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

755 
with Black 2 3 4 have "rbt_sorted a" and "rbt_sorted (Branch B (combine b c) y w d)" 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

756 
and "rbt_less x a" and "rbt_greater x (Branch B (combine b c) y w d)" by auto 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

757 
with Black show ?thesis by (simp add: balance_left_rbt_sorted) 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

758 
qed 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

759 
next 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

760 
case (5 va vb vd vc b x w c) 
47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

761 
hence "k < x \<and> rbt_less k (Branch B va vb vd vc)" by simp 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

762 
hence "rbt_less x (Branch B va vb vd vc)" by (blast dest: rbt_less_trans) 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

763 
with 5 show ?case by (simp add: combine_rbt_less) 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

764 
next 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

765 
case (6 a x v b va vb vd vc) 
47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

766 
hence "x < k \<and> rbt_greater k (Branch B va vb vd vc)" by simp 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

767 
hence "rbt_greater x (Branch B va vb vd vc)" by (blast dest: rbt_greater_trans) 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

768 
with 6 show ?case by (simp add: combine_rbt_greater) 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

769 
qed simp+ 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

770 

47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

771 
end 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

772 

35550  773 
lemma combine_in_tree: 
35534  774 
assumes "inv2 l" "inv2 r" "bheight l = bheight r" "inv1 l" "inv1 r" 
35550  775 
shows "entry_in_tree k v (combine l r) = (entry_in_tree k v l \<or> entry_in_tree k v r)" 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

776 
using assms 
35550  777 
proof (induct l r rule: combine.induct) 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

778 
case (4 _ _ _ b c) 
35550  779 
hence a: "bheight (combine b c) = bheight b" by (simp add: combine_inv2) 
780 
from 4 have b: "inv1l (combine b c)" by (simp add: combine_inv1) 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

781 

52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

782 
show ?case 
35550  783 
proof (cases "combine b c" rule: rbt_cases) 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

784 
case Empty 
35550  785 
with 4 a show ?thesis by (auto simp: balance_left_in_tree) 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

786 
next 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

787 
case (Red lta ka va rta) 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

788 
with 4 show ?thesis by auto 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

789 
next 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

790 
case (Black lta ka va rta) 
35550  791 
with a b 4 show ?thesis by (auto simp: balance_left_in_tree) 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

792 
qed 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

793 
qed (auto split: rbt.splits color.splits) 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

794 

47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

795 
context ord begin 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

796 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

797 
fun 
47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

798 
rbt_del_from_left :: "'a \<Rightarrow> ('a,'b) rbt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt" and 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

799 
rbt_del_from_right :: "'a \<Rightarrow> ('a,'b) rbt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt" and 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

800 
rbt_del :: "'a\<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt" 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

801 
where 
47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

802 
"rbt_del x Empty = Empty"  
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

803 
"rbt_del x (Branch c a y s b) = 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

804 
(if x < y then rbt_del_from_left x a y s b 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

805 
else (if x > y then rbt_del_from_right x a y s b else combine a b))"  
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

806 
"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"  
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

807 
"rbt_del_from_left x a y s b = Branch R (rbt_del x a) y s b"  
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

808 
"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))"  
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

809 
"rbt_del_from_right x a y s b = Branch R a y s (rbt_del x b)" 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

810 

2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

811 
end 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

812 

2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

813 
context linorder begin 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

814 

52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

815 
lemma 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

816 
assumes "inv2 lt" "inv1 lt" 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

817 
shows 
35534  818 
"\<lbrakk>inv2 rt; bheight lt = bheight rt; inv1 rt\<rbrakk> \<Longrightarrow> 
47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

819 
inv2 (rbt_del_from_left x lt k v rt) \<and> 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

820 
bheight (rbt_del_from_left x lt k v rt) = bheight lt \<and> 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

821 
(color_of lt = B \<and> color_of rt = B \<and> inv1 (rbt_del_from_left x lt k v rt) \<or> 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

822 
(color_of lt \<noteq> B \<or> color_of rt \<noteq> B) \<and> inv1l (rbt_del_from_left x lt k v rt))" 
35534  823 
and "\<lbrakk>inv2 rt; bheight lt = bheight rt; inv1 rt\<rbrakk> \<Longrightarrow> 
47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

824 
inv2 (rbt_del_from_right x lt k v rt) \<and> 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

825 
bheight (rbt_del_from_right x lt k v rt) = bheight lt \<and> 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

826 
(color_of lt = B \<and> color_of rt = B \<and> inv1 (rbt_del_from_right x lt k v rt) \<or> 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

827 
(color_of lt \<noteq> B \<or> color_of rt \<noteq> B) \<and> inv1l (rbt_del_from_right x lt k v rt))" 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

828 
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) 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

829 
\<or> color_of lt = B \<and> bheight (rbt_del x lt) = bheight lt  1 \<and> inv1l (rbt_del x lt))" 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

830 
using assms 
47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

831 
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) 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

832 
case (2 y c _ y') 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

833 
have "y = y' \<or> y < y' \<or> y > y'" by auto 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

834 
thus ?case proof (elim disjE) 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

835 
assume "y = y'" 
35550  836 
with 2 show ?thesis by (cases c) (simp add: combine_inv2 combine_inv1)+ 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

837 
next 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

838 
assume "y < y'" 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

839 
with 2 show ?thesis by (cases c) auto 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

840 
next 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

841 
assume "y' < y" 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

842 
with 2 show ?thesis by (cases c) auto 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

843 
qed 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

844 
next 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

845 
case (3 y lt z v rta y' ss bb) 
35550  846 
thus ?case by (cases "color_of (Branch B lt z v rta) = B \<and> color_of bb = B") (simp add: balance_left_inv2_with_inv1 balance_left_inv1 balance_left_inv1l)+ 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

847 
next 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

848 
case (5 y a y' ss lt z v rta) 
35550  849 
thus ?case by (cases "color_of a = B \<and> color_of (Branch B lt z v rta) = B") (simp add: balance_right_inv2_with_inv1 balance_right_inv1 balance_right_inv1l)+ 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

850 
next 
35534  851 
case ("6_1" y a y' ss) thus ?case by (cases "color_of a = B \<and> color_of Empty = B") simp+ 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

852 
qed auto 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

853 

52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

854 
lemma 
47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

855 
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" 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

856 
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" 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

857 
and rbt_del_rbt_less: "lt \<guillemotleft> v \<Longrightarrow> rbt_del x lt \<guillemotleft> v" 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

858 
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) 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

859 
(auto simp: balance_left_rbt_less balance_right_rbt_less) 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

860 

47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

861 
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" 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

862 
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" 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

863 
and rbt_del_rbt_greater: "v \<guillemotleft> lt \<Longrightarrow> v \<guillemotleft> rbt_del x lt" 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

864 
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) 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

865 
(auto simp: balance_left_rbt_greater balance_right_rbt_greater) 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

866 

47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

867 
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)" 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

868 
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)" 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

869 
and rbt_del_rbt_sorted: "rbt_sorted lt \<Longrightarrow> rbt_sorted (rbt_del x lt)" 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

870 
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) 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

871 
case (3 x lta zz v rta yy ss bb) 
47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

872 
from 3 have "Branch B lta zz v rta \<guillemotleft> yy" by simp 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

873 
hence "rbt_del x (Branch B lta zz v rta) \<guillemotleft> yy" by (rule rbt_del_rbt_less) 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

874 
with 3 show ?case by (simp add: balance_left_rbt_sorted) 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

875 
next 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

876 
case ("4_2" x vaa vbb vdd vc yy ss bb) 
47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

877 
hence "Branch R vaa vbb vdd vc \<guillemotleft> yy" by simp 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

878 
hence "rbt_del x (Branch R vaa vbb vdd vc) \<guillemotleft> yy" by (rule rbt_del_rbt_less) 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

879 
with "4_2" show ?case by simp 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

880 
next 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

881 
case (5 x aa yy ss lta zz v rta) 
47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

882 
hence "yy \<guillemotleft> Branch B lta zz v rta" by simp 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

883 
hence "yy \<guillemotleft> rbt_del x (Branch B lta zz v rta)" by (rule rbt_del_rbt_greater) 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

884 
with 5 show ?case by (simp add: balance_right_rbt_sorted) 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

885 
next 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

886 
case ("6_2" x aa yy ss vaa vbb vdd vc) 
47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

887 
hence "yy \<guillemotleft> Branch R vaa vbb vdd vc" by simp 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

888 
hence "yy \<guillemotleft> rbt_del x (Branch R vaa vbb vdd vc)" by (rule rbt_del_rbt_greater) 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

889 
with "6_2" show ?case by simp 
47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

890 
qed (auto simp: combine_rbt_sorted) 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

891 

47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

892 
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)))" 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

893 
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)))" 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

894 
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))" 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

895 
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) 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

896 
case (2 xx c aa yy ss bb) 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

897 
have "xx = yy \<or> xx < yy \<or> xx > yy" by auto 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

898 
from this 2 show ?case proof (elim disjE) 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

899 
assume "xx = yy" 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

900 
with 2 show ?thesis proof (cases "xx = k") 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

901 
case True 
60500  902 
from 2 \<open>xx = yy\<close> \<open>xx = k\<close> have "rbt_sorted (Branch c aa yy ss bb) \<and> k = yy" by simp 
47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

903 
hence "\<not> entry_in_tree k v aa" "\<not> entry_in_tree k v bb" by (auto simp: rbt_less_nit rbt_greater_prop) 
60500  904 
with \<open>xx = yy\<close> 2 \<open>xx = k\<close> show ?thesis by (simp add: combine_in_tree) 
35550  905 
qed (simp add: combine_in_tree) 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

906 
qed simp+ 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

907 
next 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

908 
case (3 xx lta zz vv rta yy ss bb) 
35534  909 
def mt[simp]: mt == "Branch B lta zz vv rta" 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

910 
from 3 have "inv2 mt \<and> inv1 mt" by simp 
47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

911 
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) 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

912 
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) 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

913 
thus ?case proof (cases "xx = k") 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

914 
case True 
47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

915 
from 3 True have "yy \<guillemotleft> bb \<and> yy > k" by simp 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

916 
hence "k \<guillemotleft> bb" by (blast dest: rbt_greater_trans) 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

917 
with 3 4 True show ?thesis by (auto simp: rbt_greater_nit) 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

918 
qed auto 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

919 
next 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

920 
case ("4_1" xx yy ss bb) 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

921 
show ?case proof (cases "xx = k") 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

922 
case True 
47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

923 
with "4_1" have "yy \<guillemotleft> bb \<and> k < yy" by simp 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

924 
hence "k \<guillemotleft> bb" by (blast dest: rbt_greater_trans) 
60500  925 
with "4_1" \<open>xx = k\<close> 
47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

926 
have "entry_in_tree k v (Branch R Empty yy ss bb) = entry_in_tree k v Empty" by (auto simp: rbt_greater_nit) 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

927 
thus ?thesis by auto 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

928 
qed simp+ 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

929 
next 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

930 
case ("4_2" xx vaa vbb vdd vc yy ss bb) 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

931 
thus ?case proof (cases "xx = k") 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

932 
case True 
47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

933 
with "4_2" have "k < yy \<and> yy \<guillemotleft> bb" by simp 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

934 
hence "k \<guillemotleft> bb" by (blast dest: rbt_greater_trans) 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

935 
with True "4_2" show ?thesis by (auto simp: rbt_greater_nit) 
35550  936 
qed auto 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

937 
next 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

938 
case (5 xx aa yy ss lta zz vv rta) 
35534  939 
def mt[simp]: mt == "Branch B lta zz vv rta" 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

940 
from 5 have "inv2 mt \<and> inv1 mt" by simp 
47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

941 
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) 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

942 
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) 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

943 
thus ?case proof (cases "xx = k") 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

944 
case True 
47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

945 
from 5 True have "aa \<guillemotleft> yy \<and> yy < k" by simp 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

946 
hence "aa \<guillemotleft> k" by (blast dest: rbt_less_trans) 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

947 
with 3 5 True show ?thesis by (auto simp: rbt_less_nit) 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

948 
qed auto 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

949 
next 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

950 
case ("6_1" xx aa yy ss) 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

951 
show ?case proof (cases "xx = k") 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

952 
case True 
47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

953 
with "6_1" have "aa \<guillemotleft> yy \<and> k > yy" by simp 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

954 
hence "aa \<guillemotleft> k" by (blast dest: rbt_less_trans) 
60500  955 
with "6_1" \<open>xx = k\<close> show ?thesis by (auto simp: rbt_less_nit) 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

956 
qed simp 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

957 
next 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

958 
case ("6_2" xx aa yy ss vaa vbb vdd vc) 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

959 
thus ?case proof (cases "xx = k") 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

960 
case True 
47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

961 
with "6_2" have "k > yy \<and> aa \<guillemotleft> yy" by simp 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

962 
hence "aa \<guillemotleft> k" by (blast dest: rbt_less_trans) 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

963 
with True "6_2" show ?thesis by (auto simp: rbt_less_nit) 
35550  964 
qed auto 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

965 
qed simp 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

966 

47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

967 
definition (in ord) rbt_delete where 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

968 
"rbt_delete k t = paint B (rbt_del k t)" 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

969 

47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

970 
theorem rbt_delete_is_rbt [simp]: assumes "is_rbt t" shows "is_rbt (rbt_delete k t)" 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

971 
proof  
35534  972 
from assms have "inv2 t" and "inv1 t" unfolding is_rbt_def by auto 
47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

973 
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) 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

974 
hence "inv2 (rbt_del k t) \<and> inv1l (rbt_del k t)" by (cases "color_of t") auto 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

975 
with assms show ?thesis 
47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

976 
unfolding is_rbt_def rbt_delete_def 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

977 
by (auto intro: paint_rbt_sorted rbt_del_rbt_sorted) 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

978 
qed 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

979 

47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

980 
lemma rbt_delete_in_tree: 
35534  981 
assumes "is_rbt t" 
47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

982 
shows "entry_in_tree k v (rbt_delete x t) = (x \<noteq> k \<and> entry_in_tree k v t)" 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

983 
using assms unfolding is_rbt_def rbt_delete_def 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

984 
by (auto simp: rbt_del_in_tree) 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

985 

47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

986 
lemma rbt_lookup_rbt_delete: 
35534  987 
assumes is_rbt: "is_rbt t" 
47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

988 
shows "rbt_lookup (rbt_delete k t) = (rbt_lookup t)`({k})" 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

989 
proof 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

990 
fix x 
47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

991 
show "rbt_lookup (rbt_delete k t) x = (rbt_lookup t ` ({k})) x" 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

992 
proof (cases "x = k") 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

993 
assume "x = k" 
35534  994 
with is_rbt show ?thesis 
47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

995 
by (cases "rbt_lookup (rbt_delete k t) k") (auto simp: rbt_lookup_in_tree rbt_delete_in_tree) 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

996 
next 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

997 
assume "x \<noteq> k" 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

998 
thus ?thesis 
47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

999 
by auto (metis is_rbt rbt_delete_is_rbt rbt_delete_in_tree is_rbt_rbt_sorted rbt_lookup_from_in_tree) 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

1000 
qed 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

1001 
qed 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

1002 

47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

1003 
end 
35550  1004 

60500  1005 
subsection \<open>Modifying existing entries\<close> 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

1006 

47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

1007 
context ord begin 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

1008 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

1009 
primrec 
47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

1010 
rbt_map_entry :: "'a \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt" 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

1011 
where 
47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

1012 
"rbt_map_entry k f Empty = Empty" 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

1013 
 "rbt_map_entry k f (Branch c lt x v rt) = 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

1014 
(if k < x then Branch c (rbt_map_entry k f lt) x v rt 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

1015 
else if k > x then (Branch c lt x v (rbt_map_entry k f rt)) 
35602  1016 
else Branch c lt x (f v) rt)" 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

1017 

47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

1018 

2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

1019 
lemma rbt_map_entry_color_of: "color_of (rbt_map_entry k f t) = color_of t" by (induct t) simp+ 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

1020 
lemma rbt_map_entry_inv1: "inv1 (rbt_map_entry k f t) = inv1 t" by (induct t) (simp add: rbt_map_entry_color_of)+ 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

1021 
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+ 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

1022 
lemma rbt_map_entry_rbt_greater: "rbt_greater a (rbt_map_entry k f t) = rbt_greater a t" by (induct t) simp+ 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

1023 
lemma rbt_map_entry_rbt_less: "rbt_less a (rbt_map_entry k f t) = rbt_less a t" by (induct t) simp+ 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

1024 
lemma rbt_map_entry_rbt_sorted: "rbt_sorted (rbt_map_entry k f t) = rbt_sorted t" 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

1025 
by (induct t) (simp_all add: rbt_map_entry_rbt_less rbt_map_entry_rbt_greater) 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

1026 

47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

1027 
theorem rbt_map_entry_is_rbt [simp]: "is_rbt (rbt_map_entry k f t) = is_rbt t" 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

1028 
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 ) 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

1029 

47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

1030 
end 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

1031 

2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

1032 
theorem (in linorder) rbt_lookup_rbt_map_entry: 
55466  1033 
"rbt_lookup (rbt_map_entry k f t) = (rbt_lookup t)(k := map_option f (rbt_lookup t k))" 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

1034 
by (induct t) (auto split: option.splits simp add: fun_eq_iff) 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

1035 

60500  1036 
subsection \<open>Mapping all entries\<close> 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

1037 

52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

1038 
primrec 
35602  1039 
map :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'c) rbt" 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

1040 
where 
35550  1041 
"map f Empty = Empty" 
1042 
 "map f (Branch c lt k v rt) = Branch c (map f lt) k (f k v) (map f rt)" 

32237
cdc76a42fed4
added missing proof of RBT.map_of_alist_of (contributed by Peter Lammich)
krauss
parents:
30738
diff
changeset

1043 

35550  1044 
lemma map_entries [simp]: "entries (map f t) = List.map (\<lambda>(k, v). (k, f k v)) (entries t)" 
1045 
by (induct t) auto 

1046 
lemma map_keys [simp]: "keys (map f t) = keys t" by (simp add: keys_def split_def) 

1047 
lemma map_color_of: "color_of (map f t) = color_of t" by (induct t) simp+ 

1048 
lemma map_inv1: "inv1 (map f t) = inv1 t" by (induct t) (simp add: map_color_of)+ 

1049 
lemma map_inv2: "inv2 (map f t) = inv2 t" "bheight (map f t) = bheight t" by (induct t) simp+ 

47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

1050 

2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

1051 
context ord begin 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

1052 

2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

1053 
lemma map_rbt_greater: "rbt_greater k (map f t) = rbt_greater k t" by (induct t) simp+ 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

1054 
lemma map_rbt_less: "rbt_less k (map f t) = rbt_less k t" by (induct t) simp+ 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

1055 
lemma map_rbt_sorted: "rbt_sorted (map f t) = rbt_sorted t" by (induct t) (simp add: map_rbt_less map_rbt_greater)+ 
35550  1056 
theorem map_is_rbt [simp]: "is_rbt (map f t) = is_rbt t" 
47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

1057 
unfolding is_rbt_def by (simp add: map_inv1 map_inv2 map_rbt_sorted map_color_of) 
32237
cdc76a42fed4
added missing proof of RBT.map_of_alist_of (contributed by Peter Lammich)
krauss
parents:
30738
diff
changeset

1058 

47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

1059 
end 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

1060 

55466  1061 
theorem (in linorder) rbt_lookup_map: "rbt_lookup (map f t) x = map_option (f x) (rbt_lookup t x)" 
47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

1062 
apply(induct t) 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

1063 
apply auto 
58257  1064 
apply(rename_tac a b c, subgoal_tac "x = a") 
47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

1065 
apply auto 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

1066 
done 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

1067 
(* FIXME: simproc "antisym less" does not work for linorder context, only for linorder type class 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

1068 
by (induct t) auto *) 
35550  1069 

49770
cf6a78acf445
efficient construction of red black trees from sorted associative lists
Andreas Lochbihler
parents:
49480
diff
changeset

1070 
hide_const (open) map 
cf6a78acf445
efficient construction of red black trees from sorted associative lists
Andreas Lochbihler
parents:
49480
diff
changeset

1071 

60500  1072 
subsection \<open>Folding over entries\<close> 
35550  1073 

1074 
definition fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a, 'b) rbt \<Rightarrow> 'c \<Rightarrow> 'c" where 

55414
eab03e9cee8a
renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents:
55412
diff
changeset

1075 
"fold f t = List.fold (case_prod f) (entries t)" 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

1076 

49770
cf6a78acf445
efficient construction of red black trees from sorted associative lists
Andreas Lochbihler
parents:
49480
diff
changeset

1077 
lemma fold_simps [simp]: 
35550  1078 
"fold f Empty = id" 
1079 
"fold f (Branch c lt k v rt) = fold f rt \<circ> f k v \<circ> fold f lt" 

39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

1080 
by (simp_all add: fold_def fun_eq_iff) 
35534  1081 

49770
cf6a78acf445
efficient construction of red black trees from sorted associative lists
Andreas Lochbihler
parents:
49480
diff
changeset

1082 
lemma fold_code [code]: 
49810  1083 
"fold f Empty x = x" 
1084 
"fold f (Branch c lt k v rt) x = fold f rt (f k v (fold f lt x))" 

49770
cf6a78acf445
efficient construction of red black trees from sorted associative lists
Andreas Lochbihler
parents:
49480
diff
changeset

1085 
by(simp_all) 
cf6a78acf445
efficient construction of red black trees from sorted associative lists
Andreas Lochbihler
parents:
49480
diff
changeset

1086 

48621
877df57629e3
a couple of additions to RBT formalization to allow us to implement RBT_Set
kuncar
parents:
47455
diff
changeset

1087 
(* fold with continuation predicate *) 
877df57629e3
a couple of additions to RBT formalization to allow us to implement RBT_Set
kuncar
parents:
47455
diff
changeset

1088 

877df57629e3
a couple of additions to RBT formalization to allow us to implement RBT_Set
kuncar
parents:
47455
diff
changeset

1089 
fun foldi :: "('c \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a :: linorder, 'b) rbt \<Rightarrow> 'c \<Rightarrow> 'c" 
877df57629e3
a couple of additions to RBT formalization to allow us to implement RBT_Set
kuncar
parents:
47455
diff
changeset

1090 
where 
877df57629e3
a couple of additions to RBT formalization to allow us to implement RBT_Set
kuncar
parents:
47455
diff
changeset

1091 
"foldi c f Empty s = s"  
877df57629e3
a couple of additions to RBT formalization to allow us to implement RBT_Set
kuncar
parents:
47455
diff
changeset

1092 
"foldi c f (Branch col l k v r) s = ( 
877df57629e3
a couple of additions to RBT formalization to allow us to implement RBT_Set
kuncar
parents:
47455
diff
changeset

1093 
if (c s) then 
877df57629e3
a couple of additions to RBT formalization to allow us to implement RBT_Set
kuncar
parents:
47455
diff
changeset

1094 
let s' = foldi c f l s in 
877df57629e3
a couple of additions to RBT formalization to allow us to implement RBT_Set
kuncar
parents:
47455
diff
changeset

1095 
if (c s') then 
877df57629e3
a couple of additions to RBT formalization to allow us to implement RBT_Set
kuncar
parents:
47455
diff
changeset

1096 
foldi c f r (f k v s') 
877df57629e3
a couple of additions to RBT formalization to allow us to implement RBT_Set
kuncar
parents:
47455
diff
changeset

1097 
else s' 
877df57629e3
a couple of additions to RBT formalization to allow us to implement RBT_Set
kuncar
parents:
47455
diff
changeset

1098 
else 
877df57629e3
a couple of additions to RBT formalization to allow us to implement RBT_Set
kuncar
parents:
47455
diff
changeset

1099 
s 
877df57629e3
a couple of additions to RBT formalization to allow us to implement RBT_Set
kuncar
parents:
47455
diff
changeset

1100 
)" 
35606  1101 

60500  1102 
subsection \<open>Bulkloading a tree\<close> 
35606  1103 

47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

1104 
definition (in ord) rbt_bulkload :: "('a \<times> 'b) list \<Rightarrow> ('a, 'b) rbt" where 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

1105 
"rbt_bulkload xs = foldr (\<lambda>(k, v). rbt_insert k v) xs Empty" 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

1106 

2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

1107 
context linorder begin 
35606  1108 

47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

1109 
lemma rbt_bulkload_is_rbt [simp, intro]: 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

1110 
"is_rbt (rbt_bulkload xs)" 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

1111 
unfolding rbt_bulkload_def by (induct xs) auto 
35606  1112 

47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

1113 
lemma rbt_lookup_rbt_bulkload: 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

1114 
"rbt_lookup (rbt_bulkload xs) = map_of xs" 
35606  1115 
proof  
1116 
obtain ys where "ys = rev xs" by simp 

1117 
have "\<And>t. is_rbt t \<Longrightarrow> 

55414
eab03e9cee8a
renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents:
55412
diff
changeset

1118 
rbt_lookup (List.fold (case_prod rbt_insert) ys t) = rbt_lookup t ++ map_of (rev ys)" 
eab03e9cee8a
renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents:
55412
diff
changeset

1119 
by (induct ys) (simp_all add: rbt_bulkload_def rbt_lookup_rbt_insert case_prod_beta) 
35606  1120 
from this Empty_is_rbt have 
55414
eab03e9cee8a
renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents:
55412
diff
changeset

1121 
"rbt_lookup (List.fold (case_prod rbt_insert) (rev xs) Empty) = rbt_lookup Empty ++ map_of xs" 
60500  1122 
by (simp add: \<open>ys = rev xs\<close>) 
47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

1123 
then show ?thesis by (simp add: rbt_bulkload_def rbt_lookup_Empty foldr_conv_fold) 
35606  1124 
qed 
1125 

47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

1126 
end 
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
47397
diff
changeset

1127 

49770
cf6a78acf445
efficient construction of red black trees from sorted associative lists
Andreas Lochbihler
parents:
49480
diff
changeset

1128 

cf6a78acf445
efficient construction of red black trees from sorted associative lists
Andreas Lochbihler
parents:
49480
diff
changeset

1129 

60500  1130 
subsection \<open>Building a RBT from a sorted list\<close> 
49770
cf6a78acf445
efficient construction of red black trees from sorted associative lists
Andreas Lochbihler
parents:
49480
diff
changeset

1131 

60500  1132 
text \<open> 
49770
cf6a78acf445
efficient construction of red black trees from sorted associative lists
Andreas Lochbihler
parents:
49480
diff
changeset

1133 
These functions have been adapted from 
cf6a78acf445
efficient construction of red black trees from sorted associative lists
Andreas Lochbihler
parents:
49480
diff
changeset

1134 
Andrew W. Appel, Efficient Verified RedBlack Trees (September 2011) 
60500  1135 
\<close> 
49770
cf6a78acf445
efficient construction of red black trees from sorted associative lists
Andreas Lochbihler
parents:
49480
diff
changeset

1136 

cf6a78acf445
efficient construction of red black trees from sorted associative lists
Andreas Lochbihler
parents:
49480
diff
changeset

1137 
fun rbtreeify_f :: "nat \<Rightarrow> ('a \<times> 'b) list \<Rightarrow> ('a, 'b) rbt \<times> ('a \<times> 'b) list" 
cf6a78acf445
efficient construction of red black trees from sorted associative lists
Andreas Lochbihler
parents:
49480
diff
changeset

1138 
and rbtreeify_g :: "nat \<Rightarrow> ('a \<times> 'b) list \<Rightarrow> ('a, 'b) rbt \<times> ('a \<times> 'b) list" 
cf6a78acf445
efficient construction of red black trees from sorted associative lists
Andreas Lochbihler
parents:
49480
diff
changeset

1139 
where 
cf6a78acf445
efficient construction of red black trees from sorted associative lists
Andreas Lochbihler
parents:
49480
diff
changeset

1140 
"rbtreeify_f n kvs = 
cf6a78acf445
efficient construction of red black trees from sorted associative lists
Andreas Lochbihler
parents:
49480
diff
changeset

1141 
(if n = 0 then (Empty, kvs) 
cf6a78acf445
efficient construction of red black trees from sorted associative lists
Andreas Lochbihler
parents:
49480
diff
changeset

1142 
else if n = 1 then 
cf6a78acf445
efficient construction of red black trees from sorted associative lists
Andreas Lochbihler
parents:
49480
diff
changeset

1143 
case kvs of (k, v) # kvs' \<Rightarrow> (Branch R Empty k v Empty, kvs') 
cf6a78acf445
efficient construction of red black trees from sorted associative lists
Andreas Lochbihler
parents:
49480
diff
changeset

1144 
else if (n mod 2 = 0) then 
cf6a78acf445
efficient construction of red black trees from sorted associative lists
Andreas Lochbihler
parents:
49480
diff
changeset

1145 
case rbtreeify_f (n div 2) kvs of (t1, (k, v) # kvs') \<Rightarrow> 
cf6a78acf445
efficient construction of red black trees from sorted associative lists
Andreas Lochbihler
parents:
49480
diff
changeset

1146 
apfst (Branch B t1 k v) (rbtreeify_g (n div 2) kvs') 
cf6a78acf445
efficient construction of red black trees from sorted associative lists
Andreas Lochbihler
parents:
49480
diff
changeset

1147 
else case rbtreeify_f (n div 2) kvs of (t1, (k, v) # kvs') \<Rightarrow> 
cf6a78acf445
efficient construction of red black trees from sorted associative lists
Andreas Lochbihler
parents:
49480
diff
changeset

1148 
apfst (Branch B t1 k v) (rbtreeify_f (n div 2) kvs'))" 
cf6a78acf445
efficient construction of red black trees from sorted associative lists
Andreas Lochbihler
parents:
49480
diff
changeset

1149 

cf6a78acf445
efficient construction of red black trees from sorted associative lists
Andreas Lochbihler
parents:
49480
diff
changeset

1150 
 "rbtreeify_g n kvs = 
cf6a78acf445
efficient construction of red black trees from sorted associative lists
Andreas Lochbihler
parents:
49480
diff
changeset

1151 
(if n = 0 \<or> n = 1 then (Empty, kvs) 
cf6a78acf445
efficient construction of red black trees from sorted associative lists
Andreas Lochbihler
parents:
49480
diff
changeset

1152 
else if n mod 2 = 0 then 
cf6a78acf445
efficient construction of red black trees from sorted associative lists
Andreas Lochbihler
parents:
49480
diff
changeset

1153 
case rbtreeify_g (n div 2) kvs of (t1, (k, v) # kvs') \<Rightarrow> 
cf6a78acf445
efficient construction of red black trees from sorted associative lists
Andreas Lochbihler
parents:
49480
diff
changeset

1154 
apfst (Branch B t1 k v) (rbtreeify_g (n div 2) kvs') 
cf6a78acf445
efficient construction of red black trees from sorted associative lists
Andreas Lochbihler
parents:
49480
diff
changeset

1155 
else case rbtreeify_f (n div 2) kvs of (t1, (k, v) # kvs') \<Rightarrow> 
cf6a78acf445
efficient construction of red black trees from sorted associative lists
Andreas Lochbihler
parents:
49480
diff
changeset

1156 
apfst (Branch B t1 k v) (rbtreeify_g (n div 2) kvs'))" 
cf6a78acf445
efficient construction of red black trees from sorted associative lists
Andreas Lochbihler
parents:
49480
diff
changeset

1157 

cf6a78acf445
efficient construction of red black trees from sorted associative lists
Andreas Lochbihler
parents:
49480
diff
changeset

1158 
definition rbtreeify :: "('a \<times> 'b) list \<Rightarrow> ('a, 'b) rbt" 
cf6a78acf445
efficient construction of red black trees from sorted associative lists
Andreas Lochbihler
parents:
49480
diff
changeset

1159 
where "rbtreeify kvs = fst (rbtreeify_g (Suc (length kvs)) kvs)" 
cf6a78acf445
efficient construction of red black trees from sorted associative lists
Andreas Lochbihler
parents:
49480
diff
changeset

1160 

cf6a78acf445
efficient construction of red black trees from sorted associative lists
Andreas Lochbihler
parents:
49480
diff
changeset

1161 
declare rbtreeify_f.simps [simp del] rbtreeify_g.simps [simp del] 
cf6a78acf445
efficient construction of red black trees from sorted associative lists
Andreas Lochbihler
parents:
49480
diff
changeset

1162 

cf6a78acf445
efficient construction of red black trees from sorted associative lists
Andreas Lochbihler
parents:
49480
diff
changeset

1163 
lemma rbtreeify_f_code [code]: 
cf6a78acf445
efficient construction of red black trees from sorted associative lists
Andreas Lochbihler
parents:
49480
diff
changeset

1164 
"rbtreeify_f n kvs = 
cf6a78acf445
efficient construction of red black trees from sorted associative lists
Andreas Lochbihler
parents:
49480
diff
changeset

1165 
(if n = 0 then (Empty, kvs) 
cf6a78acf445
efficient construction of red black trees from sorted associative lists
Andreas Lochbihler
parents:
49480
diff
changeset

1166 
else if n = 1 then 
cf6a78acf445
efficient construction of red black trees from sorted associative lists
Andreas Lochbihler
parents:
49480
diff
changeset

1167 
case kvs of (k, v) # kvs' \<Rightarrow> 
cf6a78acf445
efficient construction of red black trees from sorted associative lists
Andreas Lochbihler
parents:
49480
diff
changeset

1168 
(Branch R Empty k v Empty, kvs') 
61433
a4c0de1df3d8
qualify some names stemming from internal bootstrap constructions
haftmann
parents:
61225
diff
changeset

1169 
else let (n', r) = Divides.divmod_nat n 2 in 
49770
cf6a78acf445
efficient construction of red black trees from sorted associative lists
Andreas Lochbihler
parents:
49480
diff
changeset

1170 
if r = 0 then 
cf6a78acf445
efficient construction of red black trees from sorted associative lists
Andreas Lochbihler
parents:
49480
diff
changeset

1171 
case rbtreeify_f n' kvs of (t1, (k, v) # kvs') \<Rightarrow> 
cf6a78acf445
efficient construction of red black trees from sorted associative lists
Andreas Lochbihler
parents:
49480
diff
changeset

1172 
apfst (Branch B t1 k v) (rbtreeify_g n' kvs') 
cf6a78acf445
efficient construction of red black trees from sorted associative lists
Andreas Lochbihler
parents:
49480
diff
changeset

1173 
else case rbtreeify_f n' kvs of (t1, (k, v) # kvs') \<Rightarrow> 
cf6a78acf445
efficient construction of red black trees from sorted associative lists
Andreas Lochbihler
parents:
49480
diff
changeset

1174 
apfst (Branch B t1 k v) (rbtreeify_f n' kvs'))" 
55412
eb2caacf3ba4
avoid old 'prod.simps'  better be more specific
blanchet
parents:
53374
diff
changeset

1175 
by (subst rbtreeify_f.simps) (simp only: Let_def divmod_nat_div_mod prod.case) 
49770
cf6a78acf445
efficient construction of red black trees from sorted associative lists
Andreas Lochbihler
parents:
49480
diff
changeset

1176 

cf6a78acf445
efficient construction of red black trees from sorted associative lists
Andreas Lochbihler
parents:
49480
diff
changeset

1177 
lemma rbtreeify_g_code [code]: 
cf6a78acf445
efficient construction of red black trees from sorted associative lists
Andreas Lochbihler
parents:
49480
diff
changeset

1178 
"rbtreeify_g n kvs = 
cf6a78acf445
efficient construction of red black trees from sorted associative lists
Andreas Lochbihler
parents:
49480
diff
changeset

1179 
(if n = 0 \<or> n = 1 then (Empty, kvs) 
61433
a4c0de1df3d8
qualify some names stemming from internal bootstrap constructions
haftmann
parents:
61225
diff
changeset

1180 
else let (n', r) = Divides.divmod_nat n 2 in 
49770
cf6a78acf445
efficient construction of red black trees from sorted associative lists
Andreas Lochbihler
parents:
49480
diff
changeset

1181 
if r = 0 then 
cf6a78acf445
efficient construction of red black trees from sorted associative lists
Andreas Lochbihler
parents:
49480
diff
changeset

1182 
case rbtreeify_g n' kvs of (t1, (k, v) # kvs') \<Rightarrow> 
cf6a78acf445
efficient construction of red black trees from sorted associative lists
Andreas Lochbihler
parents:
49480
diff
changeset

1183 
apfst (Branch B t1 k v) (rbtreeify_g n' kvs') 
cf6a78acf445
efficient construction of red black trees from sorted associative lists
Andreas Lochbihler
parents:
49480
diff
changeset

1184 
else case rbtreeify_f n' kvs of (t1, (k, v) # kvs') \<Rightarrow> 
cf6a78acf445
efficient construction of red black trees from sorted associative lists
Andreas Lochbihler
parents:
49480
diff
changeset

1185 
apfst (Branch B t1 k v) (rbtreeify_g n' kvs'))" 
55412
eb2caacf3ba4
avoid old 'prod.simps'  better be more specific
blanchet
parents:
53374
diff
changeset

1186 
by(subst rbtreeify_g.simps)(simp only: Let_def divmod_nat_div_mod prod.case) 
49770
cf6a78acf445
efficient construction of red black trees from sorted associative lists
Andreas Lochbihler
parents:
49480
diff
changeset

1187 

cf6a78acf445
efficient construction of red black trees from sorted associative lists
Andreas Lochbihler
parents:
49480
diff
changeset

1188 
lemma Suc_double_half: "Suc (2 * n) div 2 = n" 
cf6a78acf445
efficient construction of red black trees from sorted associative lists
Andreas Lochbihler
parents:
49480
diff
changeset

1189 
by simp 
cf6a78acf445
efficient construction of red black trees from sorted associative lists
Andreas Lochbihler
parents:
49480
diff
changeset

1190 

cf6a78acf445
efficient construction of red black trees from sorted associative lists
Andreas Lochbihler
parents:
49480
diff
changeset

1191 
lemma div2_plus_div2: "n div 2 + n div 2 = (n :: nat)  n mod 2" 
cf6a78acf445
efficient construction of red black trees from sorted associative lists
Andreas Lochbihler
parents:
49480
diff
changeset

1192 
by arith 
cf6a78acf445
efficient construction of red black trees from sorted associative lists
Andreas Lochbihler
parents:
49480
diff
changeset

1193 

cf6a78acf445
efficient construction of red black trees from sorted associative lists
Andreas Lochbihler
parents:
49480
diff
changeset

1194 
lemma rbtreeify_f_rec_aux_lemma: 
cf6a78acf445
efficient construction of red black trees from sorted associative lists
Andreas Lochbihler
parents:
49480
diff
changeset

1195 
"\<lbrakk>k  n div 2 = Suc k'; n \<le> k; n mod 2 = Suc 0\<rbrakk> 
cf6a78acf445
efficient construction of red black trees from sorted associative lists
Andreas Lochbihler
parents:
49480
diff
changeset

1196 
\<Longrightarrow> k'  n div 2 = k  n" 
cf6a78acf445
efficient construction of red black trees from sorted associative lists
Andreas Lochbihler
parents:
49480
diff
changeset

1197 
apply(rule add_right_imp_eq[where a = "n  n div 2"]) 
cf6a78acf445
efficient construction of red black trees from sorted associative lists
Andreas Lochbihler
parents:
49480
diff
changeset

1198 
apply(subst add_diff_assoc2, arith) 
cf6a78acf445
efficient construction of red black trees from sorted associative lists
Andreas Lochbihler
parents:
49480
diff
changeset

1199 
apply(simp add: div2_plus_div2) 
cf6a78acf445
efficient construction of red black trees from sorted associative lists
Andreas Lochbihler
parents:
49480
diff
changeset

1200 
done 
cf6a78acf445
efficient construction of red black trees from sorted associative lists
Andreas Lochbihler
parents:
49480
diff
changeset

1201 

cf6a78acf445
efficient construction of red black trees from sorted associative lists
Andreas Lochbihler
parents:
49480
diff
changeset

1202 
lemma rbtreeify_f_simps: 
59575
55f5e1cbf2a7
removed needless (and inconsistent) qualifier that messes up with Mirabelle
blanchet
parents:
59554
diff
changeset

1203 
"rbtreeify_f 0 kvs = (Empty, kvs)" 
49770
cf6a78acf445
efficient construction of red black trees from sorted associative lists
Andreas Lochbihler
parents:
49480
diff
changeset

1204 
"rbtreeify_f (Suc 0) ((k, v) # kvs) = 
cf6a78acf445
efficient construction of red black trees from sorted associative lists
Andreas Lochbihler
parents:
49480
diff
changeset

1205 
(Branch R Empty k v Empty, kvs)" 
cf6a78acf445
efficient construction of red black trees from sorted associative lists
Andreas Lochbihler
parents:
49480
diff
changeset

1206 
"0 < n \<Longrightarrow> rbtreeify_f (2 * n) kvs = 
cf6a78acf445
efficient construction of red black trees from sorted associative lists
Andreas Lochbihler
parents:
49480
diff
changeset

1207 
(case rbtreeify_f n kvs of (t1, (k, v) # kvs') \<Rightarrow> 
cf6a78acf445
efficient construction of red black trees from sorted associative lists
Andreas Lochbihler
parents:
49480
diff
changeset

1208 
apfst (Branch B t1 k v) (rbtreeify_g n kvs'))" 
cf6a78acf445
efficient construction of red black trees from sorted associative lists
Andreas Lochbihler
parents:
49480
diff
changeset

1209 
"0 < n \<Longrightarrow> rbtreeify_f (Suc (2 * n)) kvs = 
cf6a78acf445
efficient construction of red black trees from sorted associative lists
Andreas Lochbihler
parents:
49480
diff
changeset

1210 
(case rbtreeify_f n kvs of (t1, (k, v) # kvs') \<Rightarrow> 
cf6a78acf445
efficient construction of red black trees from sorted associative lists
Andreas Lochbihler
parents:
49480
diff
changeset

1211 
apfst (Branch B t1 k v) (rbtreeify_f n kvs'))" 
cf6a78acf445
efficient construction of red black trees from sorted associative lists
Andreas Lochbihler
parents:
49480
diff
changeset

1212 
by(subst (1) rbtreeify_f.simps, simp add: Suc_double_half)+ 
cf6a78acf445
efficient construction of red black trees from sorted associative lists
Andreas Lochbihler
parents:
49480
diff
changeset

1213 

cf6a78acf445
efficient construction of red black trees from sorted associative lists
Andreas Lochbihler
parents:
49480
diff
changeset

1214 
lemma rbtreeify_g_simps: 
cf6a78acf445
efficient construction of red black trees from sorted associative lists
Andreas Lochbihler
parents:
49480
diff
changeset

1215 
"rbtreeify_g 0 kvs = (Empty, kvs)" 
cf6a78acf445
efficient construction of red black trees from sorted associative lists
Andreas Lochbihler
parents:
49480
diff
changeset

1216 
"rbtreeify_g (Suc 0) kvs = (Empty, kvs)" 
cf6a78acf445
efficient construction of red black trees from sorted associative lists
Andreas Lochbihler
parents:
49480
diff
changeset

1217 
"0 < n \<Longrightarrow> rbtreeify_g (2 * n) kvs = 
cf6a78acf445
efficient construction of red black trees from sorted associative lists
Andreas Lochbihler
parents:
49480
diff
changeset

1218 
(case rbtreeify_g n kvs of (t1, (k, v) # kvs') \<Rightarrow> 
cf6a78acf445
efficient construction of red black trees from sorted associative lists
Andreas Lochbihler
parents:
49480
diff
changeset

1219 
apfst (Branch B t1 k v) (rbtreeify_g n kvs'))" 
cf6a78acf445
efficient construction of red black trees from sorted associative lists
Andreas Lochbihler
parents:
49480
diff
changeset

1220 
"0 < n \<Longrightarrow> rbtreeify_g (Suc (2 * n)) kvs = 
cf6a78acf445
efficient construction of red black trees from sorted associative lists
Andreas Lochbihler
parents:
49480
diff
changeset

1221 
(case rbtreeify_f n kvs of (t1, (k, v) # kvs') \<Rightarrow> 
cf6a78acf445
efficient construction of red black trees from sorted associative lists
Andreas Lochbihler
parents:
49480
diff
changeset

1222 
apfst (Branch B t1 k v) (rbtreeify_g n kvs'))" 