71414
|
1 |
(* Author: Bohua Zhan, with modifications by Tobias Nipkow *)
|
|
2 |
|
|
3 |
section \<open>Interval Trees\<close>
|
|
4 |
|
|
5 |
theory Interval_Tree
|
|
6 |
imports
|
|
7 |
"HOL-Data_Structures.Cmp"
|
|
8 |
"HOL-Data_Structures.List_Ins_Del"
|
|
9 |
"HOL-Data_Structures.Isin2"
|
|
10 |
"HOL-Data_Structures.Set_Specs"
|
|
11 |
begin
|
|
12 |
|
|
13 |
subsection \<open>Intervals\<close>
|
|
14 |
|
|
15 |
text \<open>The following definition of intervals uses the \<^bold>\<open>typedef\<close> command
|
|
16 |
to define the type of non-empty intervals as a subset of the type of pairs \<open>p\<close>
|
|
17 |
where @{prop "fst p \<le> snd p"}:\<close>
|
|
18 |
|
|
19 |
typedef (overloaded) 'a::linorder ivl =
|
|
20 |
"{p :: 'a \<times> 'a. fst p \<le> snd p}" by auto
|
|
21 |
|
|
22 |
text \<open>More precisely, @{typ "'a ivl"} is isomorphic with that subset via the function
|
|
23 |
@{const Rep_ivl}. Hence the basic interval properties are not immediate but
|
|
24 |
need simple proofs:\<close>
|
|
25 |
|
|
26 |
definition low :: "'a::linorder ivl \<Rightarrow> 'a" where
|
|
27 |
"low p = fst (Rep_ivl p)"
|
|
28 |
|
|
29 |
definition high :: "'a::linorder ivl \<Rightarrow> 'a" where
|
|
30 |
"high p = snd (Rep_ivl p)"
|
|
31 |
|
|
32 |
lemma ivl_is_interval: "low p \<le> high p"
|
|
33 |
by (metis Rep_ivl high_def low_def mem_Collect_eq)
|
|
34 |
|
|
35 |
lemma ivl_inj: "low p = low q \<Longrightarrow> high p = high q \<Longrightarrow> p = q"
|
|
36 |
by (metis Rep_ivl_inverse high_def low_def prod_eqI)
|
|
37 |
|
|
38 |
text \<open>Now we can forget how exactly intervals were defined.\<close>
|
|
39 |
|
|
40 |
|
|
41 |
instantiation ivl :: (linorder) linorder begin
|
|
42 |
|
71415
|
43 |
definition ivl_less: "(x < y) = (low x < low y | (low x = low y \<and> high x < high y))"
|
|
44 |
definition ivl_less_eq: "(x \<le> y) = (low x < low y | (low x = low y \<and> high x \<le> high y))"
|
71414
|
45 |
|
|
46 |
instance proof
|
|
47 |
fix x y z :: "'a ivl"
|
|
48 |
show a: "(x < y) = (x \<le> y \<and> \<not> y \<le> x)"
|
71415
|
49 |
using ivl_less ivl_less_eq by force
|
71414
|
50 |
show b: "x \<le> x"
|
71415
|
51 |
by (simp add: ivl_less_eq)
|
71414
|
52 |
show c: "x \<le> y \<Longrightarrow> y \<le> z \<Longrightarrow> x \<le> z"
|
71415
|
53 |
by (smt ivl_less_eq dual_order.trans less_trans)
|
71414
|
54 |
show d: "x \<le> y \<Longrightarrow> y \<le> x \<Longrightarrow> x = y"
|
71415
|
55 |
using ivl_less_eq a ivl_inj ivl_less by fastforce
|
71414
|
56 |
show e: "x \<le> y \<or> y \<le> x"
|
71415
|
57 |
by (meson ivl_less_eq leI not_less_iff_gr_or_eq)
|
71414
|
58 |
qed end
|
|
59 |
|
|
60 |
|
|
61 |
definition overlap :: "('a::linorder) ivl \<Rightarrow> 'a ivl \<Rightarrow> bool" where
|
|
62 |
"overlap x y \<longleftrightarrow> (high x \<ge> low y \<and> high y \<ge> low x)"
|
|
63 |
|
|
64 |
definition has_overlap :: "('a::linorder) ivl set \<Rightarrow> 'a ivl \<Rightarrow> bool" where
|
|
65 |
"has_overlap S y \<longleftrightarrow> (\<exists>x\<in>S. overlap x y)"
|
|
66 |
|
|
67 |
|
|
68 |
subsection \<open>Interval Trees\<close>
|
|
69 |
|
|
70 |
type_synonym 'a ivl_tree = "('a ivl * 'a) tree"
|
|
71 |
|
|
72 |
fun max_hi :: "('a::order_bot) ivl_tree \<Rightarrow> 'a" where
|
|
73 |
"max_hi Leaf = bot" |
|
|
74 |
"max_hi (Node _ (_,m) _) = m"
|
|
75 |
|
|
76 |
definition max3 :: "('a::linorder) ivl \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a" where
|
|
77 |
"max3 a m n = max (high a) (max m n)"
|
|
78 |
|
|
79 |
fun inv_max_hi :: "('a::{linorder,order_bot}) ivl_tree \<Rightarrow> bool" where
|
|
80 |
"inv_max_hi Leaf \<longleftrightarrow> True" |
|
|
81 |
"inv_max_hi (Node l (a, m) r) \<longleftrightarrow> (inv_max_hi l \<and> inv_max_hi r \<and> m = max3 a (max_hi l) (max_hi r))"
|
|
82 |
|
|
83 |
lemma max_hi_is_max:
|
|
84 |
"inv_max_hi t \<Longrightarrow> a \<in> set_tree t \<Longrightarrow> high a \<le> max_hi t"
|
|
85 |
by (induct t, auto simp add: max3_def max_def)
|
|
86 |
|
|
87 |
lemma max_hi_exists:
|
|
88 |
"inv_max_hi t \<Longrightarrow> t \<noteq> Leaf \<Longrightarrow> \<exists>a\<in>set_tree t. high a = max_hi t"
|
|
89 |
proof (induction t rule: tree2_induct)
|
|
90 |
case Leaf
|
|
91 |
then show ?case by auto
|
|
92 |
next
|
|
93 |
case N: (Node l v m r)
|
|
94 |
then show ?case
|
|
95 |
proof (cases l rule: tree2_cases)
|
|
96 |
case Leaf
|
|
97 |
then show ?thesis
|
|
98 |
using N.prems(1) N.IH(2) by (cases r, auto simp add: max3_def max_def le_bot)
|
|
99 |
next
|
|
100 |
case Nl: Node
|
|
101 |
then show ?thesis
|
|
102 |
proof (cases r rule: tree2_cases)
|
|
103 |
case Leaf
|
|
104 |
then show ?thesis
|
|
105 |
using N.prems(1) N.IH(1) Nl by (auto simp add: max3_def max_def le_bot)
|
|
106 |
next
|
|
107 |
case Nr: Node
|
|
108 |
obtain p1 where p1: "p1 \<in> set_tree l" "high p1 = max_hi l"
|
|
109 |
using N.IH(1) N.prems(1) Nl by auto
|
|
110 |
obtain p2 where p2: "p2 \<in> set_tree r" "high p2 = max_hi r"
|
|
111 |
using N.IH(2) N.prems(1) Nr by auto
|
|
112 |
then show ?thesis
|
|
113 |
using p1 p2 N.prems(1) by (auto simp add: max3_def max_def)
|
|
114 |
qed
|
|
115 |
qed
|
|
116 |
qed
|
|
117 |
|
|
118 |
|
|
119 |
subsection \<open>Insertion and Deletion\<close>
|
|
120 |
|
|
121 |
definition node where
|
|
122 |
[simp]: "node l a r = Node l (a, max3 a (max_hi l) (max_hi r)) r"
|
|
123 |
|
|
124 |
fun insert :: "'a::{linorder,order_bot} ivl \<Rightarrow> 'a ivl_tree \<Rightarrow> 'a ivl_tree" where
|
|
125 |
"insert x Leaf = Node Leaf (x, high x) Leaf" |
|
|
126 |
"insert x (Node l (a, m) r) =
|
|
127 |
(case cmp x a of
|
|
128 |
EQ \<Rightarrow> Node l (a, m) r |
|
|
129 |
LT \<Rightarrow> node (insert x l) a r |
|
|
130 |
GT \<Rightarrow> node l a (insert x r))"
|
|
131 |
|
|
132 |
lemma inorder_insert:
|
|
133 |
"sorted (inorder t) \<Longrightarrow> inorder (insert x t) = ins_list x (inorder t)"
|
|
134 |
by (induct t rule: tree2_induct) (auto simp: ins_list_simps)
|
|
135 |
|
|
136 |
lemma inv_max_hi_insert:
|
|
137 |
"inv_max_hi t \<Longrightarrow> inv_max_hi (insert x t)"
|
|
138 |
by (induct t rule: tree2_induct) (auto simp add: max3_def)
|
|
139 |
|
|
140 |
fun split_min :: "'a::{linorder,order_bot} ivl_tree \<Rightarrow> 'a ivl \<times> 'a ivl_tree" where
|
|
141 |
"split_min (Node l (a, m) r) =
|
|
142 |
(if l = Leaf then (a, r)
|
|
143 |
else let (x,l') = split_min l in (x, node l' a r))"
|
|
144 |
|
|
145 |
fun delete :: "'a::{linorder,order_bot} ivl \<Rightarrow> 'a ivl_tree \<Rightarrow> 'a ivl_tree" where
|
|
146 |
"delete x Leaf = Leaf" |
|
|
147 |
"delete x (Node l (a, m) r) =
|
|
148 |
(case cmp x a of
|
|
149 |
LT \<Rightarrow> node (delete x l) a r |
|
|
150 |
GT \<Rightarrow> node l a (delete x r) |
|
|
151 |
EQ \<Rightarrow> if r = Leaf then l else
|
|
152 |
let (a', r') = split_min r in node l a' r')"
|
|
153 |
|
|
154 |
lemma split_minD:
|
|
155 |
"split_min t = (x,t') \<Longrightarrow> t \<noteq> Leaf \<Longrightarrow> x # inorder t' = inorder t"
|
|
156 |
by (induct t arbitrary: t' rule: split_min.induct)
|
|
157 |
(auto simp: sorted_lems split: prod.splits if_splits)
|
|
158 |
|
|
159 |
lemma inorder_delete:
|
|
160 |
"sorted (inorder t) \<Longrightarrow> inorder (delete x t) = del_list x (inorder t)"
|
|
161 |
by (induct t)
|
|
162 |
(auto simp: del_list_simps split_minD Let_def split: prod.splits)
|
|
163 |
|
|
164 |
lemma inv_max_hi_split_min:
|
|
165 |
"\<lbrakk> t \<noteq> Leaf; inv_max_hi t \<rbrakk> \<Longrightarrow> inv_max_hi (snd (split_min t))"
|
|
166 |
by (induct t) (auto split: prod.splits)
|
|
167 |
|
|
168 |
lemma inv_max_hi_delete:
|
|
169 |
"inv_max_hi t \<Longrightarrow> inv_max_hi (delete x t)"
|
|
170 |
apply (induct t)
|
|
171 |
apply simp
|
|
172 |
using inv_max_hi_split_min by (fastforce simp add: Let_def split: prod.splits)
|
|
173 |
|
|
174 |
|
|
175 |
subsection \<open>Search\<close>
|
|
176 |
|
|
177 |
text \<open>Does interval \<open>x\<close> overlap with any interval in the tree?\<close>
|
|
178 |
|
|
179 |
fun search :: "'a::{linorder,order_bot} ivl_tree \<Rightarrow> 'a ivl \<Rightarrow> bool" where
|
|
180 |
"search Leaf x = False" |
|
|
181 |
"search (Node l (a, m) r) x =
|
|
182 |
(if overlap x a then True
|
|
183 |
else if l \<noteq> Leaf \<and> max_hi l \<ge> low x then search l x
|
|
184 |
else search r x)"
|
|
185 |
|
|
186 |
lemma search_correct:
|
|
187 |
"inv_max_hi t \<Longrightarrow> sorted (inorder t) \<Longrightarrow> search t x = has_overlap (set_tree t) x"
|
|
188 |
proof (induction t rule: tree2_induct)
|
|
189 |
case Leaf
|
|
190 |
then show ?case by (auto simp add: has_overlap_def)
|
|
191 |
next
|
|
192 |
case (Node l a m r)
|
|
193 |
have search_l: "search l x = has_overlap (set_tree l) x"
|
|
194 |
using Node.IH(1) Node.prems by (auto simp: sorted_wrt_append)
|
|
195 |
have search_r: "search r x = has_overlap (set_tree r) x"
|
|
196 |
using Node.IH(2) Node.prems by (auto simp: sorted_wrt_append)
|
|
197 |
show ?case
|
|
198 |
proof (cases "overlap a x")
|
|
199 |
case True
|
|
200 |
thus ?thesis by (auto simp: overlap_def has_overlap_def)
|
|
201 |
next
|
|
202 |
case a_disjoint: False
|
|
203 |
then show ?thesis
|
|
204 |
proof cases
|
|
205 |
assume [simp]: "l = Leaf"
|
|
206 |
have search_eval: "search (Node l (a, m) r) x = search r x"
|
|
207 |
using a_disjoint overlap_def by auto
|
|
208 |
show ?thesis
|
|
209 |
unfolding search_eval search_r
|
|
210 |
by (auto simp add: has_overlap_def a_disjoint)
|
|
211 |
next
|
|
212 |
assume "l \<noteq> Leaf"
|
|
213 |
then show ?thesis
|
|
214 |
proof (cases "max_hi l \<ge> low x")
|
|
215 |
case max_hi_l_ge: True
|
|
216 |
have "inv_max_hi l"
|
|
217 |
using Node.prems(1) by auto
|
|
218 |
then obtain p where p: "p \<in> set_tree l" "high p = max_hi l"
|
|
219 |
using \<open>l \<noteq> Leaf\<close> max_hi_exists by auto
|
|
220 |
have search_eval: "search (Node l (a, m) r) x = search l x"
|
|
221 |
using a_disjoint \<open>l \<noteq> Leaf\<close> max_hi_l_ge by (auto simp: overlap_def)
|
|
222 |
show ?thesis
|
|
223 |
proof (cases "low p \<le> high x")
|
|
224 |
case True
|
|
225 |
have "overlap p x"
|
|
226 |
unfolding overlap_def using True p(2) max_hi_l_ge by auto
|
|
227 |
then show ?thesis
|
|
228 |
unfolding search_eval search_l
|
|
229 |
using p(1) by(auto simp: has_overlap_def overlap_def)
|
|
230 |
next
|
|
231 |
case False
|
|
232 |
have "\<not>overlap x rp" if asm: "rp \<in> set_tree r" for rp
|
|
233 |
proof -
|
|
234 |
have "p \<in> set (inorder l)" using p(1) by (simp)
|
|
235 |
moreover have "rp \<in> set (inorder r)" using asm by (simp)
|
|
236 |
ultimately have "low p \<le> low rp"
|
71415
|
237 |
using Node(4) by(fastforce simp: sorted_wrt_append ivl_less)
|
71414
|
238 |
then show ?thesis
|
|
239 |
using False by (auto simp: overlap_def)
|
|
240 |
qed
|
|
241 |
then show ?thesis
|
|
242 |
unfolding search_eval search_l
|
|
243 |
using a_disjoint by (fastforce simp: has_overlap_def overlap_def)
|
|
244 |
qed
|
|
245 |
next
|
|
246 |
case False
|
|
247 |
have search_eval: "search (Node l (a, m) r) x = search r x"
|
|
248 |
using a_disjoint False by (auto simp: overlap_def)
|
|
249 |
have "\<not>overlap x lp" if asm: "lp \<in> set_tree l" for lp
|
|
250 |
using asm False Node.prems(1) max_hi_is_max
|
|
251 |
by (fastforce simp: overlap_def)
|
|
252 |
then show ?thesis
|
|
253 |
unfolding search_eval search_r
|
|
254 |
using a_disjoint by (fastforce simp: has_overlap_def overlap_def)
|
|
255 |
qed
|
|
256 |
qed
|
|
257 |
qed
|
|
258 |
qed
|
|
259 |
|
|
260 |
definition empty :: "'a ivl_tree" where
|
|
261 |
"empty = Leaf"
|
|
262 |
|
|
263 |
|
|
264 |
subsection \<open>Specification\<close>
|
|
265 |
|
|
266 |
locale Interval_Set = Set +
|
|
267 |
fixes has_overlap :: "'t \<Rightarrow> 'a::linorder ivl \<Rightarrow> bool"
|
|
268 |
assumes set_overlap: "invar s \<Longrightarrow> has_overlap s x = Interval_Tree.has_overlap (set s) x"
|
|
269 |
|
|
270 |
interpretation S: Interval_Set
|
|
271 |
where empty = Leaf and insert = insert and delete = delete
|
|
272 |
and has_overlap = search and isin = isin and set = set_tree
|
|
273 |
and invar = "\<lambda>t. inv_max_hi t \<and> sorted (inorder t)"
|
|
274 |
proof (standard, goal_cases)
|
|
275 |
case 1
|
|
276 |
then show ?case by auto
|
|
277 |
next
|
|
278 |
case 2
|
|
279 |
then show ?case by (simp add: isin_set_inorder)
|
|
280 |
next
|
|
281 |
case 3
|
|
282 |
then show ?case by(simp add: inorder_insert set_ins_list flip: set_inorder)
|
|
283 |
next
|
|
284 |
case 4
|
|
285 |
then show ?case by(simp add: inorder_delete set_del_list flip: set_inorder)
|
|
286 |
next
|
|
287 |
case 5
|
|
288 |
then show ?case by auto
|
|
289 |
next
|
|
290 |
case 6
|
|
291 |
then show ?case by (simp add: inorder_insert inv_max_hi_insert sorted_ins_list)
|
|
292 |
next
|
|
293 |
case 7
|
|
294 |
then show ?case by (simp add: inorder_delete inv_max_hi_delete sorted_del_list)
|
|
295 |
next
|
|
296 |
case 8
|
|
297 |
then show ?case by (simp add: search_correct)
|
|
298 |
qed
|
|
299 |
|
|
300 |
end
|