ltreeScript.sml
1(*
2 This file defines a rose tree data structure as a co-inductive
3 datatype called 'a ltree, which is short for lazy tree. This
4 co-datatype has one constructor, called Branch that has type:
5
6 Branch : 'a -> 'a ltree llist -> 'a ltree
7
8 Note that this tree data structure allows for both infinite depth
9 and infinite breadth.
10*)
11Theory ltree
12Ancestors
13 arithmetic list rich_list llist alist option pred_set relation
14 pair combin set_relation iterate
15Libs
16 hurdUtils tautLib monadsyntax
17
18val _ = enable_monadsyntax ();
19val _ = enable_monad "option";
20
21(* make type definition *)
22Type ltree_rep[local] = ``:num list -> 'a # num option``;
23
24Overload NOTHING[local] = ``(ARB:'a, SOME (0:num))``;
25
26Definition ltree_rep_ok_def:
27 ltree_rep_ok f <=>
28 !path x n.
29 f path = (x, SOME n) ==>
30 !pos rest. f (path ++ pos::rest) <> NOTHING ==> pos < n
31End
32
33Theorem type_inhabited[local]:
34 ?f. ltree_rep_ok f
35Proof
36 qexists_tac `\p. NOTHING` \\ fs [ltree_rep_ok_def] \\ rw []
37QED
38
39val ltree_tydef = new_type_definition ("ltree", type_inhabited);
40
41val repabs_fns = define_new_type_bijections
42 { name = "ltree_absrep",
43 ABS = "ltree_abs",
44 REP = "ltree_rep",
45 tyax = ltree_tydef};
46
47(* prove basic theorems about rep and abs functions *)
48val ltree_absrep = CONJUNCT1 repabs_fns
49val ltree_repabs = CONJUNCT2 repabs_fns
50
51Theorem ltree_rep_ok_ltree_rep[local,simp]:
52 ltree_rep_ok (ltree_rep f)
53Proof
54 fs [ltree_repabs, ltree_absrep]
55QED
56
57Theorem ltree_abs_11[local]:
58 ltree_rep_ok r1 /\ ltree_rep_ok r2 ==>
59 (ltree_abs r1 = ltree_abs r2 <=> r1 = r2)
60Proof
61 fs [ltree_repabs, EQ_IMP_THM] \\ metis_tac []
62QED
63
64Theorem ltree_rep_11[local]:
65 (ltree_rep t1 = ltree_rep t2) = (t1 = t2)
66Proof
67 fs [EQ_IMP_THM] \\ metis_tac [ltree_absrep]
68QED
69
70Theorem every_ltree_rep_ok[local]:
71 !ts. every ltree_rep_ok (LMAP ltree_rep ts)
72Proof
73 rw [] \\ qspec_then `ts` strip_assume_tac fromList_fromSeq
74 \\ rw [LMAP_fromList,every_fromList_EVERY,EVERY_MEM,MEM_MAP]
75 \\ fs [ltree_rep_ok_ltree_rep]
76QED
77
78Theorem LMAP_ltree_rep_11[local]:
79 LMAP ltree_rep ts1 = LMAP ltree_rep ts2 <=> ts1 = ts2
80Proof
81 rw []
82 \\ qspec_then `ts1` strip_assume_tac fromList_fromSeq \\ rw []
83 \\ qspec_then `ts2` strip_assume_tac fromList_fromSeq \\ rw []
84 \\ fs [LMAP_fromList]
85 \\ fs [Once FUN_EQ_THM,ltree_rep_11] \\ fs [FUN_EQ_THM]
86 \\ rename [`MAP _ l1 = MAP _ l2`]
87 \\ qid_spec_tac `l1`
88 \\ qid_spec_tac `l2`
89 \\ Induct \\ Cases_on `l1` \\ fs [ltree_rep_11]
90QED
91
92Theorem LMAP_ltree_rep_ltree_abs[local]:
93 every ltree_rep_ok ts ==>
94 LMAP ltree_rep (LMAP ltree_abs ts) = ts
95Proof
96 rw [] \\ qspec_then `ts` strip_assume_tac fromList_fromSeq
97 \\ fs [LMAP_fromList,every_fromList_EVERY,MEM_MAP,
98 LMAP_fromList,MAP_MAP_o]
99 \\ rw [ltree_repabs,FUN_EQ_THM] \\ fs [ltree_repabs]
100 \\ Induct_on `l` \\ fs [ltree_repabs]
101QED
102
103(* define the only constructor: Branch *)
104Definition Branch_rep_def:
105 Branch_rep (x:'a) (xs:('a ltree_rep) llist) =
106 \path. case path of
107 | [] => (x, LLENGTH xs)
108 | (n::rest) => case LNTH n xs of SOME t => t rest | NONE => NOTHING
109End
110
111Definition Branch:
112 Branch a ts = ltree_abs (Branch_rep a (LMAP ltree_rep ts))
113End
114
115Theorem ltree_rep_ok_Branch_rep_every[local]:
116 ltree_rep_ok (Branch_rep a ts) = every ltree_rep_ok ts
117Proof
118 fs [Branch_rep_def,ltree_rep_ok_def]
119 \\ rw [] \\ reverse (qspec_then `ts` strip_assume_tac fromList_fromSeq)
120 \\ rw [ltree_rep_ok_def]
121 \\ eq_tac \\ rpt strip_tac
122 THEN1
123 (first_x_assum (qspecl_then [`i::path`,`x`,`n`] mp_tac)
124 \\ fs [] \\ disch_then drule \\ fs [])
125 THEN1
126 (fs[AllCaseEqs()] >> rfs[] >> first_x_assum (drule_then irule) >>
127 RULE_ASSUM_TAC (REWRITE_RULE [GSYM APPEND_ASSOC, APPEND]) >> metis_tac[])
128 \\ fs [every_fromList_EVERY,LNTH_fromList]
129 THEN1
130 (rw [EVERY_EL,ltree_rep_ok_def]
131 \\ first_x_assum (qspec_then `n::path` mp_tac) \\ fs []
132 \\ disch_then drule \\ fs [])
133 \\ fs [EVERY_EL,ltree_rep_ok_def]
134 \\ Cases_on `path` \\ fs []
135 \\ rw [] \\ fs [AllCaseEqs()]
136 \\ res_tac \\ fs [] >> metis_tac[]
137QED
138
139Theorem ltree_rep_ok_Branch_rep[local]:
140 every ltree_rep_ok ts ==> ltree_rep_ok (Branch_rep a ts)
141Proof
142 fs [ltree_rep_ok_Branch_rep_every]
143QED
144
145Theorem ltree_rep_ok_Branch_rep_IMP[local]:
146 ltree_rep_ok (Branch_rep a ts) ==> every ltree_rep_ok ts
147Proof
148 fs [ltree_rep_ok_Branch_rep_every]
149QED
150
151(* prove injectivity *)
152Theorem Branch_rep_11[local]:
153 !a1 a2 ts1 ts2. Branch_rep a1 ts1 = Branch_rep a2 ts2 <=> a1 = a2 /\ ts1 = ts2
154Proof
155 fs [Branch_rep_def,FUN_EQ_THM]
156 \\ rpt gen_tac \\ eq_tac \\ simp []
157 \\ strip_tac
158 \\ first_assum (qspec_then `[]` assume_tac) \\ fs [] \\ rw []
159 \\ reverse (qspec_then `ts1` strip_assume_tac fromList_fromSeq) \\ rw []
160 \\ reverse (qspec_then `ts2` strip_assume_tac fromList_fromSeq) \\ rw []
161 \\ fs [LLENGTH_fromSeq,LLENGTH_fromList]
162 THEN1
163 (fs [FUN_EQ_THM] \\ rw []
164 \\ first_x_assum (qspec_then `x::x'` mp_tac) \\ fs [])
165 \\ fs [LNTH_fromList]
166 \\ fs [LIST_EQ_REWRITE] \\ rw []
167 \\ rw [FUN_EQ_THM]
168 \\ first_x_assum (qspec_then `x::x'` mp_tac) \\ fs []
169QED
170
171Theorem Branch_11:
172 !a1 a2 ts1 ts2. Branch a1 ts1 = Branch a2 ts2 <=> a1 = a2 /\ ts1 = ts2
173Proof
174 rw [Branch] \\ eq_tac \\ strip_tac \\ fs []
175 \\ qspec_then `ts1` assume_tac every_ltree_rep_ok
176 \\ drule ltree_rep_ok_Branch_rep
177 \\ qspec_then `ts2` assume_tac every_ltree_rep_ok
178 \\ drule ltree_rep_ok_Branch_rep
179 \\ strip_tac \\ strip_tac
180 \\ fs [ltree_abs_11]
181 \\ fs [LMAP_ltree_rep_11,Branch_rep_11]
182QED
183
184(* prove cases theorem *)
185Theorem Branch_rep_exists[local]:
186 ltree_rep_ok f ==> ?a ts. f = Branch_rep a ts
187Proof
188 fs [ltree_rep_ok_def] \\ rw []
189 \\ Cases_on `f []` \\ fs []
190 \\ rename [`_ = (a,ts)`]
191 \\ qexists_tac `a`
192 \\ qexists_tac `LGENLIST (\n path. f (n::path)) ts`
193 \\ fs [Branch_rep_def,FUN_EQ_THM]
194 \\ Cases \\ fs [LNTH_LGENLIST]
195 \\ Cases_on `f (h::t)` \\ fs []
196 \\ Cases_on `ts` \\ fs []
197 \\ IF_CASES_TAC \\ fs []
198 \\ first_x_assum drule \\ fs []
199 \\ disch_then (qspecl_then [`h`,`t`] mp_tac) \\ fs []
200QED
201
202Theorem ltree_cases:
203 !t. ?a ts. t = Branch a ts
204Proof
205 fs [Branch] \\ fs [GSYM ltree_rep_11] \\ rw []
206 \\ qspec_then `ts1` assume_tac every_ltree_rep_ok
207 \\ qabbrev_tac `f = ltree_rep t`
208 \\ `ltree_rep_ok f` by fs [Abbr`f`]
209 \\ drule Branch_rep_exists \\ rw []
210 \\ qexists_tac `a` \\ qexists_tac `LMAP ltree_abs ts`
211 \\ imp_res_tac ltree_rep_ok_Branch_rep_IMP
212 \\ fs [LMAP_ltree_rep_ltree_abs,ltree_repabs]
213QED
214
215(* define ltree_CASE constant *)
216Definition dest_Branch_rep_def:
217 dest_Branch_rep (l:'a ltree_rep) =
218 let (x,len) = l [] in
219 (x, LGENLIST (\n path. l (n::path)) len)
220End
221
222Theorem dest_Branch_rep_Branch_rep[local]:
223 dest_Branch_rep (Branch_rep x xs) = (x,xs)
224Proof
225 fs [Branch_rep_def,dest_Branch_rep_def]
226 \\ qspec_then `xs` strip_assume_tac fromList_fromSeq \\ fs []
227 \\ fs [LGENLIST_EQ_fromSeq,FUN_EQ_THM,LGENLIST_EQ_fromList]
228 \\ fs [LNTH_fromList]
229 \\ CONV_TAC (RAND_CONV (ONCE_REWRITE_CONV [GSYM GENLIST_ID]))
230 \\ fs [GENLIST_FUN_EQ,FUN_EQ_THM]
231QED
232
233Definition ltree_CASE[nocompute]:
234 ltree_CASE t f =
235 let (a,ts) = dest_Branch_rep (ltree_rep t) in
236 f a (LMAP ltree_abs ts)
237End
238
239Theorem ltree_CASE[compute,allow_rebind]:
240 ltree_CASE (Branch a ts) f = f a ts
241Proof
242 fs [ltree_CASE,Branch]
243 \\ qspec_then `ts` assume_tac every_ltree_rep_ok
244 \\ drule ltree_rep_ok_Branch_rep
245 \\ fs [ltree_repabs,dest_Branch_rep_Branch_rep]
246 \\ fs [LMAP_MAP] \\ rw [] \\ AP_TERM_TAC
247 \\ qspec_then `ts` strip_assume_tac fromList_fromSeq
248 \\ fs [LMAP_fromList,LMAP_fromSeq,FUN_EQ_THM,ltree_absrep]
249 \\ rpt (pop_assum kall_tac)
250 \\ Induct_on `l` \\ fs [ltree_absrep]
251QED
252
253Theorem ltree_CASE_eq:
254 ltree_CASE t f = v <=> ?a ts. t = Branch a ts /\ f a ts = v
255Proof
256 qspec_then `t` strip_assume_tac ltree_cases \\ rw []
257 \\ fs [Branch_11,ltree_CASE]
258QED
259
260Theorem ltree_CASE_elim:
261 !f'. f'(ltree_CASE t f) <=> ?a ts. t = Branch a ts /\ f'(f a ts)
262Proof
263 qspec_then `t` strip_assume_tac ltree_cases \\ rw []
264 \\ fs [Branch_11,ltree_CASE]
265QED
266
267(* ltree generator *)
268Definition path_ok_def:
269 path_ok path f <=>
270 !xs n ys k a.
271 path = xs ++ n::ys /\ f xs = (a,SOME k) ==> n < k
272End
273
274Definition make_ltree_rep_def:
275 make_ltree_rep f =
276 \path. if path_ok path f then f path else NOTHING
277End
278
279Theorem ltree_rep_ok_make_ltree_rep[local]:
280 !f. ltree_rep_ok (make_ltree_rep f)
281Proof
282 fs [ltree_rep_ok_def,make_ltree_rep_def] \\ rw []
283 THEN1
284 (fs [AllCaseEqs()] \\ fs []
285 \\ fs [path_ok_def] \\ metis_tac [])
286 \\ fs [AllCaseEqs()] \\ fs []
287 \\ CCONTR_TAC \\ fs [] \\ fs []
288 \\ fs [path_ok_def] \\ rw []
289 \\ first_x_assum (qspecl_then [`xs`,`n`,`ys ++ pos::rest`] mp_tac)
290 \\ fs []
291QED
292
293Definition gen_ltree_def[nocompute]:
294 gen_ltree f = ltree_abs (make_ltree_rep f)
295End
296
297Theorem gen_ltree:
298 gen_ltree f =
299 let (a,len) = f [] in
300 Branch a (LGENLIST (\n. gen_ltree (\path. f (n::path))) len)
301Proof
302 fs [UNCURRY,gen_ltree_def,Branch,o_DEF]
303 \\ qspec_then `f` assume_tac ltree_rep_ok_make_ltree_rep
304 \\ fs [REWRITE_RULE [ltree_rep_ok_make_ltree_rep]
305 (Q.SPEC `make_ltree_rep f` ltree_repabs)]
306 \\ AP_TERM_TAC \\ Cases_on `f []` \\ fs []
307 \\ fs [Branch_rep_def,FUN_EQ_THM]
308 \\ Cases \\ fs []
309 THEN1 fs [make_ltree_rep_def,path_ok_def]
310 \\ Cases_on `r` \\ fs []
311 \\ fs [LNTH_LGENLIST]
312 THEN1
313 (fs [make_ltree_rep_def]
314 \\ AP_THM_TAC \\ AP_THM_TAC \\ AP_TERM_TAC
315 \\ fs [path_ok_def]
316 \\ rw [] \\ eq_tac \\ rw []
317 THEN1
318 (first_x_assum match_mp_tac
319 \\ goal_assum (first_assum o mp_then.mp_then mp_then.Any mp_tac)
320 \\ qexists_tac `ys` \\ fs [])
321 \\ Cases_on `xs` \\ fs [] \\ rw []
322 \\ metis_tac [])
323 \\ fs [make_ltree_rep_def]
324 \\ reverse (Cases_on `h < x`) \\ fs []
325 THEN1 (rw [] \\ fs [path_ok_def] \\ metis_tac [APPEND])
326 \\ AP_THM_TAC \\ AP_THM_TAC \\ AP_TERM_TAC
327 \\ fs [path_ok_def]
328 \\ rw [] \\ eq_tac \\ rw []
329 THEN1
330 (first_x_assum match_mp_tac
331 \\ goal_assum (first_assum o mp_then.mp_then mp_then.Any mp_tac)
332 \\ qexists_tac `ys` \\ fs [])
333 \\ Cases_on `xs` \\ fs [] \\ rw []
334 \\ metis_tac []
335QED
336
337Theorem gen_ltree_LNIL:
338 gen_ltree f = Branch a LNIL <=> f [] = (a, SOME 0)
339Proof
340 simp [Once gen_ltree,UNCURRY]
341 \\ Cases_on `f []` \\ fs [Branch_11]
342QED
343
344
345(* ltree unfold *)
346Definition make_unfold_def:
347 make_unfold f seed [] =
348 (let (a,seeds) = f seed in (a,LLENGTH seeds)) /\
349 make_unfold f seed (n::path) =
350 let (a,seeds) = f seed in
351 make_unfold f (THE (LNTH n seeds)) path
352End
353
354Definition ltree_unfold:
355 ltree_unfold f seed =
356 gen_ltree (make_unfold f seed)
357End
358
359Theorem ltree_unfold[allow_rebind]:
360 ltree_unfold f seed =
361 let (a,seeds) = f seed in
362 Branch a (LMAP (ltree_unfold f) seeds)
363Proof
364 fs [ltree_unfold]
365 \\ once_rewrite_tac [gen_ltree]
366 \\ simp [Once make_unfold_def]
367 \\ Cases_on `f seed`
368 \\ fs [Branch_11]
369 \\ reverse (qspec_then `r` strip_assume_tac fromList_fromSeq)
370 \\ fs [LGENLIST_EQ_fromSeq]
371 THEN1
372 (fs [FUN_EQ_THM,ltree_unfold] \\ rw []
373 \\ AP_TERM_TAC \\ fs [FUN_EQ_THM] \\ rw []
374 \\ fs [make_unfold_def])
375 \\ fs [LGENLIST_EQ_fromList,LMAP_fromList]
376 \\ fs [LIST_EQ_REWRITE,EL_MAP] \\ rw []
377 \\ rw [ltree_unfold] \\ rw []
378 \\ AP_TERM_TAC \\ fs [FUN_EQ_THM] \\ rw []
379 \\ fs [make_unfold_def,LNTH_fromList]
380QED
381
382(* ltree_el returns the tree node (with the number of children) at given path *)
383Definition ltree_el_def:
384 ltree_el t [] =
385 ltree_CASE t (\a ts. SOME (a, LLENGTH ts)) /\
386 ltree_el t (n::ns) =
387 ltree_CASE t (\a ts.
388 case LNTH n ts of
389 | NONE => NONE
390 | SOME t => ltree_el t ns)
391End
392
393Theorem ltree_el_def[allow_rebind]:
394 ltree_el (Branch a ts) [] = SOME (a, LLENGTH ts) /\
395 ltree_el (Branch a ts) (n::ns) =
396 case LNTH n ts of
397 | NONE => NONE
398 | SOME t => ltree_el t ns
399Proof
400 qspec_then `t` strip_assume_tac ltree_cases
401 \\ fs [ltree_el_def,ltree_CASE]
402QED
403
404Theorem ltree_el_eqv:
405 !t1 t2. t1 = t2 <=> !path. ltree_el t1 path = ltree_el t2 path
406Proof
407 rw [] \\ eq_tac \\ rw []
408 \\ fs [GSYM ltree_rep_11,FUN_EQ_THM] \\ rw []
409 \\ pop_assum mp_tac
410 \\ qid_spec_tac `t1` \\ qid_spec_tac `t2`
411 \\ Induct_on `x` \\ rw []
412 \\ `ltree_rep_ok (ltree_rep t1) /\ ltree_rep_ok (ltree_rep t2)`
413 by fs [ltree_rep_ok_ltree_rep]
414 \\ qspec_then `t1` strip_assume_tac ltree_cases
415 \\ qspec_then `t2` strip_assume_tac ltree_cases
416 \\ rpt BasicProvers.var_eq_tac \\ simp [Branch]
417 \\ `ltree_rep_ok (Branch_rep a (LMAP ltree_rep ts)) /\
418 ltree_rep_ok (Branch_rep a' (LMAP ltree_rep ts'))` by
419 (rw [ltree_rep_ok_Branch_rep_every]
420 \\ rename [`LMAP _ ts2`]
421 \\ qspec_then `ts2` strip_assume_tac fromList_fromSeq \\ fs []
422 \\ fs [LMAP_fromList,every_fromList_EVERY,EVERY_MEM]
423 \\ fs [MEM_MAP,PULL_EXISTS])
424 \\ fs [ltree_repabs]
425 \\ simp [Branch_rep_def,LLENGTH_MAP]
426 \\ last_assum (qspec_then `[]` mp_tac)
427 \\ rewrite_tac [ltree_el_def] \\ fs [] \\ rw []
428 \\ Cases_on `LNTH h ts` \\ Cases_on `LNTH h ts'` \\ fs []
429 THEN1 (qspec_then `ts` strip_assume_tac fromList_fromSeq
430 \\ qspec_then `ts'` strip_assume_tac fromList_fromSeq
431 \\ rw [] \\ fs [LNTH_fromList])
432 THEN1 (qspec_then `ts` strip_assume_tac fromList_fromSeq
433 \\ qspec_then `ts'` strip_assume_tac fromList_fromSeq
434 \\ rw [] \\ fs [LNTH_fromList])
435 \\ last_x_assum match_mp_tac \\ rw []
436 \\ last_x_assum (qspec_then `h::path` mp_tac)
437 \\ fs [ltree_el_def]
438QED
439
440Definition ltree_rel_def:
441 ltree_rel R x y <=>
442 !path.
443 OPTREL (\x y. R (FST x) (FST y) /\ SND x = SND y)
444 (ltree_el x path) (ltree_el y path)
445End
446
447Theorem ltree_rel:
448 ltree_rel R (Branch a ts) (Branch b us) <=>
449 R a b /\ llist_rel (ltree_rel R) ts us
450Proof
451 fs [ltree_rel_def,llist_rel_def] \\ rw [] \\ eq_tac \\ rw []
452 THEN1 (first_x_assum (qspec_then `[]` mp_tac) \\ fs [ltree_el_def])
453 THEN1 (first_x_assum (qspec_then `[]` mp_tac) \\ fs [ltree_el_def])
454 THEN1 (first_x_assum (qspec_then `i::path` mp_tac) \\ fs [ltree_el_def])
455 \\ Cases_on `path` \\ fs [ltree_el_def]
456 \\ Cases_on `LNTH h ts` \\ fs []
457 \\ Cases_on `LNTH h us` \\ fs []
458 \\ qspec_then `ts` strip_assume_tac fromList_fromSeq
459 \\ qspec_then `us` strip_assume_tac fromList_fromSeq
460 \\ rw [] \\ fs [LNTH_fromList] \\ metis_tac []
461QED
462
463Theorem ltree_rel_eq:
464 ltree_rel (=) x y <=> x = y
465Proof
466 fs [ltree_rel_def,ltree_el_eqv] \\ eq_tac \\ rw []
467 \\ first_x_assum (qspec_then `path` mp_tac)
468 \\ Cases_on `ltree_el x path` \\ Cases_on `ltree_el y path` \\ fs []
469 \\ fs [UNCURRY]
470 \\ rename [`FST y = FST z`]
471 \\ Cases_on `y` \\ Cases_on `z` \\ fs []
472QED
473
474Theorem ltree_bisimulation:
475 !t1 t2.
476 t1 = t2 <=>
477 ?R. R t1 t2 /\
478 !a ts a' ts'.
479 R (Branch a ts) (Branch a' ts') ==>
480 a = a' /\ llist_rel R ts ts'
481Proof
482 rw [] \\ eq_tac \\ rw []
483 THEN1 (qexists_tac `(=)` \\ fs [Branch_11,llist_rel_def] \\ rw [] \\ fs [])
484 \\ simp [ltree_el_eqv]
485 \\ strip_tac
486 \\ last_x_assum mp_tac \\ qid_spec_tac `t1` \\ qid_spec_tac `t2`
487 \\ Induct_on `path` \\ rw []
488 \\ qspec_then `t1` strip_assume_tac ltree_cases
489 \\ qspec_then `t2` strip_assume_tac ltree_cases
490 \\ fs []
491 THEN1 (fs [ltree_el_def] \\ res_tac \\ fs [llist_rel_def])
492 \\ rw [] \\ fs [ltree_el_def]
493 \\ res_tac \\ rw []
494 \\ fs [llist_rel_def]
495 \\ pop_assum (qspec_then `h` mp_tac)
496 \\ Cases_on `LNTH h ts` \\ fs []
497 \\ Cases_on `LNTH h ts'` \\ fs []
498 \\ qspec_then `ts` strip_assume_tac fromList_fromSeq
499 \\ qspec_then `ts'` strip_assume_tac fromList_fromSeq
500 \\ rw [] \\ fs [LNTH_fromList]
501QED
502
503(* ltree_lookup returns the subtree after passing the given path, cf. ltree_el *)
504Definition ltree_lookup_def:
505 ltree_lookup t [] = SOME t /\
506 ltree_lookup t (n::ns) =
507 ltree_CASE t (\a ts.
508 case LNTH n ts of
509 | NONE => NONE
510 | SOME t => ltree_lookup t ns)
511End
512
513Theorem ltree_lookup_def[allow_rebind]:
514 ltree_lookup t [] = SOME t /\
515 ltree_lookup (Branch a ts) (n::ns) =
516 case LNTH n ts of
517 | NONE => NONE
518 | SOME t => ltree_lookup t ns
519Proof
520 qspec_then `t` strip_assume_tac ltree_cases
521 \\ fs [ltree_lookup_def,ltree_CASE]
522QED
523
524Definition subtrees_def:
525 subtrees t = { u | ?path. ltree_lookup t path = SOME u }
526End
527
528Theorem subtrees:
529 subtrees (Branch a ts) =
530 Branch a ts INSERT BIGUNION (IMAGE subtrees (LSET ts))
531Proof
532 fs [subtrees_def,Once EXTENSION,PULL_EXISTS] \\ rw []
533 \\ qspec_then `x` strip_assume_tac ltree_cases
534 \\ fs [Branch_11] \\ rw [] \\ reverse eq_tac \\ rw []
535 THEN1 (qexists_tac `[]` \\ fs [ltree_lookup_def])
536 THEN1 (fs [LSET_def,IN_DEF] \\ qexists_tac `n::path` \\ fs [ltree_lookup_def])
537 \\ Cases_on `path` \\ fs []
538 \\ fs [ltree_lookup_def,Branch_11]
539 \\ Cases_on `LNTH h ts` \\ fs [] \\ disj2_tac
540 \\ fs [LSET_def,IN_DEF,PULL_EXISTS]
541 \\ rpt (goal_assum (first_assum o mp_then Any mp_tac))
542QED
543
544Definition ltree_set_def:
545 ltree_set t = { a | ?ts. Branch a ts IN subtrees t }
546End
547
548Theorem ltree_set:
549 ltree_set (Branch a ts) =
550 a INSERT BIGUNION (IMAGE ltree_set (LSET ts))
551Proof
552 fs [ltree_set_def,subtrees,Once EXTENSION,Branch_11]
553 \\ rw [] \\ Cases_on `a = x` \\ fs [] \\ fs [PULL_EXISTS] \\ metis_tac []
554QED
555
556Definition ltree_map_def:
557 ltree_map f = ltree_unfold (\t. ltree_CASE t (\a ts. (f a,ts)))
558End
559
560Theorem ltree_map:
561 ltree_map f (Branch a xs) = Branch (f a) (LMAP (ltree_map f) xs)
562Proof
563 fs [ltree_map_def,ltree_unfold,ltree_CASE]
564QED
565
566Theorem ltree_map_id:
567 ltree_map I t = t
568Proof
569 fs [ltree_el_eqv] \\ qid_spec_tac `t`
570 \\ Induct_on `path` \\ rw [] \\ fs [ltree_el_def]
571 \\ qspec_then `t` strip_assume_tac ltree_cases
572 \\ fs [ltree_map,ltree_el_def,LLENGTH_MAP]
573 \\ rw [] \\ Cases_on `LNTH h ts` \\ fs []
574QED
575
576Theorem ltree_map_map:
577 ltree_map f (ltree_map g t) = ltree_map (f o g) t
578Proof
579 fs [ltree_el_eqv] \\ qid_spec_tac `t`
580 \\ Induct_on `path` \\ rw [] \\ fs [ltree_el_def]
581 \\ qspec_then `t` strip_assume_tac ltree_cases
582 \\ fs [ltree_map,ltree_el_def,LLENGTH_MAP]
583 \\ rw [] \\ Cases_on `LNTH h ts` \\ fs []
584QED
585
586Theorem ltree_lookup_map[local]:
587 ltree_lookup (ltree_map f t) path =
588 case ltree_lookup t path of
589 | NONE => NONE
590 | SOME t => ltree_CASE t (\a ts. SOME (Branch (f a) (LMAP (ltree_map f) ts)))
591Proof
592 qid_spec_tac `t` \\ Induct_on `path` \\ fs [ltree_lookup_def] \\ rw []
593 \\ qspec_then `t` strip_assume_tac ltree_cases
594 \\ fs [ltree_map,ltree_el_def,LLENGTH_MAP,ltree_CASE]
595 \\ fs [ltree_lookup_def]
596 \\ Cases_on `LNTH h ts` \\ fs []
597QED
598
599Theorem ltree_set_map:
600 ltree_set (ltree_map f t) = IMAGE f (ltree_set t)
601Proof
602 fs [EXTENSION,ltree_set_def,subtrees_def]
603 \\ fs [ltree_lookup_map,AllCaseEqs(),ltree_CASE_eq,PULL_EXISTS,Branch_11]
604 \\ metis_tac []
605QED
606
607Theorem ltree_rel_O:
608 ltree_rel R1 O ltree_rel R2 RSUBSET ltree_rel (R1 O R2)
609Proof
610 fs [ltree_rel_def,RSUBSET,O_DEF,PULL_EXISTS]
611 \\ rw [] \\ rpt (first_x_assum (qspec_then `path` mp_tac)) \\ rw []
612 \\ Cases_on `ltree_el x path` \\ Cases_on `ltree_el y path` \\ fs [OPTREL_def]
613 \\ fs [UNCURRY] \\ metis_tac []
614QED
615
616(* update TypeBase *)
617Theorem ltree_CASE_cong:
618 !M M' f f'.
619 M = M' /\
620 (!a ts. M' = Branch a ts ==> f a ts = f' a ts) ==>
621 ltree_CASE M f = ltree_CASE M' f'
622Proof
623 rw [] \\ qspec_then `M` strip_assume_tac ltree_cases
624 \\ rw [] \\ fs [ltree_CASE]
625QED
626
627Overload "case" = “ltree_CASE”
628
629val _ = TypeBase.export
630 [TypeBasePure.mk_datatype_info
631 { ax = TypeBasePure.ORIG TRUTH,
632 induction = TypeBasePure.ORIG ltree_bisimulation,
633 case_def = ltree_CASE,
634 case_cong = ltree_CASE_cong,
635 case_eq = ltree_CASE_eq,
636 case_elim = ltree_CASE_elim,
637 nchotomy = ltree_cases,
638 size = NONE,
639 encode = NONE,
640 lift = NONE,
641 one_one = SOME Branch_11,
642 distinct = NONE,
643 fields = [],
644 accessors = [],
645 updates = [],
646 destructors = [],
647 recognizers = [] } ]
648
649Theorem datatype_ltree:
650 DATATYPE ((ltree Branch):bool)
651Proof
652 rw [boolTheory.DATATYPE_TAG_THM]
653QED
654
655(* prove that every finite ltree is an inductively defined rose tree *)
656Inductive ltree_finite:
657 EVERY ltree_finite ts ==> ltree_finite (Branch a (fromList ts))
658End
659
660fun tidy_up ind = ind
661 |> Q.SPEC `P` |> UNDISCH |> Q.SPEC `t` |> Q.GEN `t` |> DISCH_ALL |> Q.GEN `P`;
662
663Theorem ltree_finite_ind[allow_rebind] = tidy_up ltree_finite_ind;
664Theorem ltree_finite_strongind[allow_rebind] = tidy_up ltree_finite_strongind;
665
666Theorem ltree_finite:
667 ltree_finite (Branch a ts) <=>
668 LFINITE ts /\ !t. t IN LSET ts ==> ltree_finite t
669Proof
670 simp [Once ltree_finite_cases]
671 \\ qspec_then `ts` strip_assume_tac fromList_fromSeq
672 \\ fs [IN_LSET,LNTH_fromList,PULL_EXISTS,LFINITE_fromList,EVERY_EL]
673QED
674
675(* ltree created by finite steps of unfolding is finite
676
677 If the ltree is generated from a seed, whose resulting seeds after one-step
678 unfolding is finite with smaller "measure", then there must be only finite
679 steps of the unfolding process and the resulting ltree is finite.
680 *)
681Theorem ltree_finite_by_unfolding :
682 !P f. (?(m :'a -> num).
683 !seed. P seed ==>
684 let (a,seeds) = f seed in
685 LFINITE seeds /\
686 every (\e. P e /\ m e < m seed) seeds) ==>
687 !seed. P seed ==> ltree_finite (ltree_unfold f seed)
688Proof
689 NTAC 3 STRIP_TAC
690 >> measureInduct_on ‘m seed’
691 >> DISCH_TAC
692 >> LAST_X_ASSUM (drule o Q.SPEC ‘seed’)
693 >> rw [Once ltree_unfold]
694 >> qabbrev_tac ‘t = f seed’
695 >> Cases_on ‘t’ >> fs []
696 >> rw [Once ltree_finite, IN_LSET]
697 >> FIRST_X_ASSUM irule
698 >> fs [every_LNTH]
699 >> FIRST_X_ASSUM MATCH_MP_TAC
700 >> Q.EXISTS_TAC ‘n’ >> art []
701QED
702
703(* |- !f. (?m. !seed.
704 (let
705 (a,seeds) = f seed
706 in
707 LFINITE seeds /\ every (\e. m e < m seed) seeds)) ==>
708 !seed. ltree_finite (ltree_unfold f seed)
709 *)
710Theorem ltree_finite_by_unfolding' =
711 ltree_finite_by_unfolding |> Q.SPEC ‘\x. T’ |> SRULE []
712
713CoInductive ltree_every :
714 P a ts /\ every (ltree_every P) ts ==> (ltree_every P (Branch a ts))
715End
716
717Theorem ltree_every_rewrite[simp] :
718 ltree_every P (Branch a ts) <=> P a ts /\ every (ltree_every P) ts
719Proof
720 SIMP_TAC std_ss [Once ltree_every_cases]
721 >> EQ_TAC >> rw []
722QED
723
724Definition finite_branching_def :
725 finite_branching = ltree_every (\a ts. LFINITE ts)
726End
727
728Theorem finite_branching_rules :
729 !a ts. EVERY finite_branching ts ==>
730 finite_branching (Branch a (fromList ts))
731Proof
732 rw [finite_branching_def, EVERY_MEM]
733 >> qabbrev_tac ‘P = \(a :'a) (ts :'a ltree llist). LFINITE ts’
734 >> rw [Once ltree_every_cases]
735 >> rw [every_fromList_EVERY, EVERY_MEM]
736QED
737
738(* The "primed" version uses ‘every’ (and ‘LFINITE’) instead of ‘EVERY’ *)
739Theorem finite_branching_rules' :
740 !a ts. LFINITE ts /\ every finite_branching ts ==>
741 finite_branching (Branch a ts)
742Proof
743 rw [finite_branching_def]
744QED
745
746Theorem ltree_finite_imp_finite_branching :
747 !t. ltree_finite t ==> finite_branching t
748Proof
749 HO_MATCH_MP_TAC ltree_finite_ind
750 >> rw [finite_branching_rules]
751QED
752
753(* cf. ltree_cases *)
754Theorem finite_branching_cases :
755 !t. finite_branching t <=>
756 ?a ts. t = Branch a (fromList ts) /\ EVERY finite_branching ts
757Proof
758 rw [finite_branching_def, Once ltree_every_cases]
759 >> EQ_TAC >> rw [LFINITE_fromList, every_fromList_EVERY]
760 >> ‘?l. ts = fromList l’ by METIS_TAC [LFINITE_IMP_fromList]
761 >> fs [every_fromList_EVERY]
762QED
763
764Theorem finite_branching_cases' :
765 !t. finite_branching t <=>
766 ?a ts. t = Branch a ts /\ LFINITE ts /\ every finite_branching ts
767Proof
768 rw [finite_branching_def, Once ltree_every_cases]
769QED
770
771(* |- (!a0. P a0 ==> ?a ts. a0 = Branch a ts /\ LFINITE ts /\ every P ts) ==>
772 !a0. P a0 ==> finite_branching a0
773 *)
774val lemma = ltree_every_coind
775 |> (Q.SPEC ‘\(a :'a) (ts :'a ltree llist). LFINITE ts’)
776 |> (Q.SPEC ‘P’) |> BETA_RULE
777 |> REWRITE_RULE [GSYM finite_branching_def];
778
779Theorem finite_branching_coind :
780 !P. (!t. P t ==> ?a ts. t = Branch a (fromList ts) /\ EVERY P ts) ==>
781 !t. P t ==> finite_branching t
782Proof
783 NTAC 2 STRIP_TAC
784 >> MATCH_MP_TAC lemma
785 >> Q.X_GEN_TAC ‘t’
786 >> DISCH_TAC
787 >> Q.PAT_X_ASSUM ‘!t. P t ==> _’ (drule_then STRIP_ASSUME_TAC)
788 >> qexistsl_tac [‘a’, ‘fromList ts’]
789 >> rw [LFINITE_fromList, every_fromList_EVERY]
790QED
791
792Theorem finite_branching_coind' :
793 !P. (!t. P t ==> ?a ts. t = Branch a ts /\ LFINITE ts /\ every P ts) ==>
794 !t. P t ==> finite_branching t
795Proof
796 NTAC 2 STRIP_TAC
797 >> MATCH_MP_TAC lemma >> rw []
798QED
799
800Theorem finite_branching_rewrite[simp] :
801 finite_branching (Branch a ts) <=> LFINITE ts /\ every finite_branching ts
802Proof
803 SIMP_TAC std_ss [finite_branching_cases]
804 >> EQ_TAC >> rw []
805 >- rw [LFINITE_fromList]
806 >- rw [every_fromList_EVERY]
807 >> ‘?l. ts = fromList l’ by METIS_TAC [LFINITE_IMP_fromList]
808 >> fs [every_fromList_EVERY]
809QED
810
811(*---------------------------------------------------------------------------*
812 * More ltree operators
813 *---------------------------------------------------------------------------*)
814
815Definition ltree_node_def[simp] :
816 ltree_node (Branch a ts) = a
817End
818
819Definition ltree_children_def[simp] :
820 ltree_children (Branch a ts) = ts
821End
822
823Theorem ltree_node_children_reduce[simp] :
824 Branch (ltree_node t) (ltree_children t) = t
825Proof
826 ‘?a ts. t = Branch a ts’ by METIS_TAC [ltree_cases]
827 >> rw []
828QED
829
830Definition ltree_paths_def :
831 ltree_paths t = {p | ltree_lookup t p <> NONE}
832End
833
834Theorem IN_ltree_paths :
835 !p t. p IN ltree_paths t <=> ltree_lookup t p <> NONE
836Proof
837 rw [ltree_paths_def]
838QED
839
840Theorem NIL_IN_ltree_paths[simp] :
841 [] IN ltree_paths t
842Proof
843 rw [ltree_paths_def, ltree_lookup_def]
844QED
845
846Theorem ltree_paths_inclusive :
847 !l1 l2 t. l1 <<= l2 /\ l2 IN ltree_paths t ==> l1 IN ltree_paths t
848Proof
849 Induct_on ‘l1’
850 >> rw [] (* only one goal left *)
851 >> Cases_on ‘l2’ >> fs []
852 >> rename1 ‘l1 <<= l2’
853 >> Q.PAT_X_ASSUM ‘h = h'’ K_TAC
854 >> rename1 ‘h::l1 IN ltree_paths t’
855 >> POP_ASSUM MP_TAC
856 >> ‘?a ts. t = Branch a ts’ by METIS_TAC [ltree_cases]
857 >> POP_ORW
858 >> simp [ltree_paths_def, ltree_lookup_def]
859 >> Cases_on ‘LNTH h ts’ >> rw []
860 >> fs [GSYM IN_ltree_paths]
861 >> FIRST_X_ASSUM MATCH_MP_TAC
862 >> Q.EXISTS_TAC ‘l2’ >> rw []
863QED
864
865Theorem ltree_el :
866 ltree_el t [] = SOME (ltree_node t,LLENGTH (ltree_children t)) /\
867 ltree_el t (n::ns) =
868 case LNTH n (ltree_children t) of
869 NONE => NONE
870 | SOME a => ltree_el a ns
871Proof
872 ‘?a ts. t = Branch a ts’ by METIS_TAC [ltree_cases]
873 >> simp [ltree_el_def]
874QED
875
876Theorem ltree_lookup :
877 ltree_lookup t [] = SOME t /\
878 ltree_lookup t (n::ns) =
879 case LNTH n (ltree_children t) of
880 NONE => NONE
881 | SOME a => ltree_lookup a ns
882Proof
883 ‘?a ts. t = Branch a ts’ by METIS_TAC [ltree_cases]
884 >> simp [ltree_lookup_def]
885QED
886
887Theorem ltree_lookup_iff_ltree_el[local] :
888 !p t. ltree_lookup t p <> NONE <=> ltree_el t p <> NONE
889Proof
890 Induct_on ‘p’
891 >- rw [ltree_lookup, ltree_el]
892 >> rw [Once ltree_lookup, Once ltree_el]
893 >> Cases_on ‘LNTH h (ltree_children t)’ >> fs []
894QED
895
896Theorem ltree_paths_alt_ltree_el :
897 !t. ltree_paths t = {p | ltree_el t p <> NONE}
898Proof
899 rw [ltree_paths_def, Once EXTENSION, ltree_lookup_iff_ltree_el]
900QED
901
902Theorem ltree_el_valid :
903 !p t. p IN ltree_paths t <=> ltree_el t p <> NONE
904Proof
905 rw [ltree_paths_alt_ltree_el]
906QED
907
908Theorem ltree_el_valid_inclusive :
909 !p t. p IN ltree_paths t <=> !p'. p' <<= p ==> ltree_el t p' <> NONE
910Proof
911 rpt GEN_TAC
912 >> reverse EQ_TAC >> STRIP_TAC
913 >- (POP_ASSUM (MP_TAC o (Q.SPEC ‘p’)) \\
914 rw [ltree_el_valid])
915 >> rw [GSYM ltree_el_valid]
916 >> MATCH_MP_TAC ltree_paths_inclusive
917 >> Q.EXISTS_TAC ‘p’ >> art []
918QED
919
920Theorem ltree_lookup_valid :
921 !p t. p IN ltree_paths t <=> ltree_lookup t p <> NONE
922Proof
923 rw [ltree_lookup_iff_ltree_el, ltree_el_valid]
924QED
925
926Theorem ltree_lookup_valid_inclusive :
927 !p t. p IN ltree_paths t <=> !p'. p' <<= p ==> ltree_lookup t p' <> NONE
928Proof
929 rw [ltree_lookup_iff_ltree_el, ltree_el_valid_inclusive]
930QED
931
932(* ltree_lookup returns more information (the entire subtree), thus can be
933 used to construct the return value of ltree_el.
934 *)
935Theorem ltree_el_alt_ltree_lookup :
936 !p t. p IN ltree_paths t ==>
937 ltree_el t p =
938 do
939 t' <- ltree_lookup t p;
940 return (ltree_node t',LLENGTH (ltree_children t'))
941 od
942Proof
943 Induct_on ‘p’
944 >- (Q.X_GEN_TAC ‘t’ \\
945 STRIP_ASSUME_TAC (Q.SPEC ‘t’ ltree_cases) >> POP_ORW \\
946 rw [ltree_el_def, ltree_lookup_def])
947 >> qx_genl_tac [‘h’, ‘t’]
948 >> STRIP_ASSUME_TAC (Q.SPEC ‘t’ ltree_cases) >> POP_ORW
949 >> fs [ltree_paths_def]
950 >> rw [ltree_el_def, ltree_lookup_def]
951 >> qabbrev_tac ‘t' = LNTH h ts’
952 >> Cases_on ‘t' = NONE’ >- rw []
953 >> gs [GSYM IS_SOME_EQ_NOT_NONE, IS_SOME_EXISTS]
954QED
955
956Theorem ltree_paths_map_cong[simp] :
957 !f t. ltree_paths (ltree_map f t) = ltree_paths t
958Proof
959 rw [ltree_paths_def, Once EXTENSION]
960 >> Q.ID_SPEC_TAC ‘t’
961 >> Q.SPEC_TAC (‘x’, ‘p’)
962 >> Induct_on ‘p’
963 >- rw [ltree_lookup_def]
964 >> rpt GEN_TAC
965 >> Cases_on ‘t’
966 >> rw [ltree_lookup_def, ltree_map]
967 >> Cases_on ‘LNTH h ts’ >> rw []
968QED
969
970Theorem ltree_lookup_append :
971 !l1 l2 t. ltree_lookup t l1 <> NONE ==>
972 ltree_lookup t (l1 ++ l2) =
973 ltree_lookup (THE (ltree_lookup t l1)) l2
974Proof
975 Induct_on ‘l1’
976 >- rw [ltree_lookup_def]
977 >> rpt GEN_TAC
978 >> ‘h::l1 ++ l2 = h::(l1 ++ l2)’ by rw [] >> POP_ORW
979 >> Cases_on ‘t’ >> simp [ltree_lookup_def]
980 >> Cases_on ‘LNTH h ts’ >> simp []
981QED
982
983Theorem ltree_lookup_SNOC :
984 !t x xs. ltree_lookup t xs <> NONE ==>
985 ltree_lookup t (SNOC x xs) =
986 ltree_lookup (THE (ltree_lookup t xs)) [x]
987Proof
988 rw [SNOC_APPEND]
989 >> MATCH_MP_TAC ltree_lookup_append >> art []
990QED
991
992Theorem gen_ltree_unchanged :
993 !t. gen_ltree (\p. THE (ltree_el t p)) = t
994Proof
995 Q.X_GEN_TAC ‘t’
996 >> rw [ltree_bisimulation]
997 >> Q.EXISTS_TAC ‘\x y. x = gen_ltree (\p. THE (ltree_el y p))’
998 >> simp []
999 >> rpt STRIP_TAC
1000 >- fs [Once gen_ltree, ltree_el_def]
1001 >> rw [llist_rel_def]
1002 >- fs [Once gen_ltree, ltree_el_def]
1003 >> fs [Once gen_ltree, ltree_el_def, LNTH_EQ, LNTH_LGENLIST]
1004 >> Q.PAT_X_ASSUM ‘!n. P’ (MP_TAC o Q.SPEC ‘i’)
1005 >> simp []
1006 >> Cases_on ‘y’ >> simp [ltree_el_def]
1007 >> Cases_on ‘LLENGTH ts'’ >> simp []
1008 >- (DISCH_THEN (fs o wrap) \\
1009 simp [Once gen_ltree, ltree_el_def])
1010 >> rw []
1011 >> simp [Once gen_ltree, ltree_el_def]
1012QED
1013
1014Theorem gen_ltree_unchanged_extra :
1015 !t f. gen_ltree (\p. if ltree_el t p <> NONE then THE (ltree_el t p)
1016 else f p) = t
1017Proof
1018 rw [ltree_bisimulation]
1019 >> Q.EXISTS_TAC ‘\x y. ?f. x = gen_ltree (\p. if ltree_el y p <> NONE then
1020 THE (ltree_el y p)
1021 else f p)’
1022 >> CONJ_TAC
1023 >- (simp [] >> Q.EXISTS_TAC ‘f’ >> simp [])
1024 >> rpt STRIP_TAC
1025 >- fs [Once gen_ltree, ltree_el_def]
1026 >> rw [llist_rel_def]
1027 >- fs [Once gen_ltree, ltree_el_def]
1028 >> fs [Once gen_ltree, ltree_el_def, LNTH_EQ, LNTH_LGENLIST]
1029 >> Q.PAT_X_ASSUM ‘!n. P’ (MP_TAC o Q.SPEC ‘i’)
1030 >> simp []
1031 >> Cases_on ‘y’ >> simp [ltree_el_def]
1032 >> Cases_on ‘LLENGTH ts'’ >> simp []
1033 >- (DISCH_THEN (fs o wrap) \\
1034 simp [Once gen_ltree, ltree_el_def] \\
1035 Q.EXISTS_TAC ‘\p. f (i::p)’ >> simp [])
1036 >> rw []
1037 >> simp [Once gen_ltree, ltree_el_def]
1038 >> Q.EXISTS_TAC ‘\p. f (i::p)’ >> simp []
1039QED
1040
1041Theorem ltree_el_lemma[local] :
1042 !path. (\(d,len). (d,len)) (THE (ltree_el x path)) = THE (ltree_el x path)
1043Proof
1044 rw [FUN_EQ_THM]
1045 >> qabbrev_tac ‘t0 = THE (ltree_el x path)’
1046 >> Cases_on ‘t0’ >> simp []
1047QED
1048
1049(* This is the number of children at certain ltree node (NONE means infinite).
1050 NOTE: It makes the statements of the [ltree_insert_delete], slightly nicer.
1051 *)
1052Definition ltree_branching_def :
1053 ltree_branching t p = SND (THE (ltree_el t p))
1054End
1055
1056Theorem ltree_branching_alt_ltree_lookup :
1057 !p t. p IN ltree_paths t ==>
1058 ltree_branching t p = LLENGTH (ltree_children (THE (ltree_lookup t p)))
1059Proof
1060 Induct_on ‘p’
1061 >- rw [ltree_branching_def, ltree_el, ltree_lookup]
1062 >> rpt STRIP_TAC
1063 >> ‘ltree_lookup t (h::p) <> NONE’ by fs [ltree_paths_def]
1064 >> ‘ltree_el t (h::p) <> NONE’ by fs [ltree_paths_alt_ltree_el]
1065 >> Cases_on ‘t’
1066 >> fs [ltree_branching_def, ltree_el, ltree_lookup]
1067 >> qabbrev_tac ‘t0 = LNTH h ts’
1068 >> Cases_on ‘t0’ >> fs []
1069 >> FIRST_X_ASSUM MATCH_MP_TAC
1070 >> rw [ltree_paths_def]
1071QED
1072
1073Theorem ltree_branching_NIL :
1074 !a ts. ltree_branching (Branch a ts) [] = LLENGTH ts
1075Proof
1076 rw [ltree_branching_def, ltree_el_def]
1077QED
1078
1079Theorem ltree_branching_CONS :
1080 !h p a ts. h::p IN ltree_paths (Branch a ts) ==>
1081 ltree_branching (Branch a ts) (h::p) =
1082 ltree_branching (THE (LNTH h ts)) p
1083Proof
1084 rpt GEN_TAC
1085 >> rw [ltree_paths_alt_ltree_el, ltree_el_def, ltree_branching_def]
1086 >> Cases_on ‘LNTH h ts’ >> fs []
1087QED
1088
1089Theorem ltree_branching_ltree_paths :
1090 !p t m. p IN ltree_paths t /\ ltree_branching t p = SOME m ==>
1091 !h. h < m <=> SNOC h p IN ltree_paths t
1092Proof
1093 Induct_on ‘p’
1094 >- (rpt GEN_TAC \\
1095 Cases_on ‘t’ \\
1096 rw [ltree_el_def, ltree_branching_NIL, ltree_paths_alt_ltree_el] \\
1097 Cases_on ‘LNTH h ts’ >> simp [ltree_el] >| (* 2 subgoals *)
1098 [ (* goal 1 (of 2) *)
1099 ‘LFINITE ts’ by rw [LFINITE_LLENGTH] \\
1100 Know ‘~IS_SOME (LNTH h ts)’ >- rw [IS_SOME_EQ_NOT_NONE] \\
1101 ASM_SIMP_TAC bool_ss [LFINITE_LNTH_IS_SOME] \\
1102 simp [],
1103 (* goal 2 (of 2) *)
1104 ‘LFINITE ts’ by rw [LFINITE_LLENGTH] \\
1105 Know ‘IS_SOME (LNTH h ts)’ >- rw [IS_SOME_EXISTS] \\
1106 ASM_SIMP_TAC bool_ss [LFINITE_LNTH_IS_SOME] \\
1107 simp [] ])
1108 >> rpt STRIP_TAC
1109 >> Cases_on ‘t’
1110 >> POP_ASSUM MP_TAC
1111 >> simp [ltree_branching_CONS]
1112 >> POP_ASSUM MP_TAC
1113 >> simp [ltree_paths_alt_ltree_el, ltree_el_def]
1114 >> Cases_on ‘LNTH h ts’ >> simp []
1115 >> rpt STRIP_TAC
1116 >> fs [ltree_paths_alt_ltree_el]
1117QED
1118
1119(*---------------------------------------------------------------------------*
1120 * ltree_delete: delete the rightmost children at a subtree
1121 *---------------------------------------------------------------------------*)
1122
1123(* NOTE: Here p is the path of the parent node whose rightmost children node
1124 is going to be deleted. f can be used to update the parent node for the
1125 removal of rightmost child (subtree), otherwise use I.
1126 *)
1127Definition ltree_delete_def :
1128 ltree_delete f t p =
1129 gen_ltree (\ns. let (d,len) = THE (ltree_el t ns); m = THE len in
1130 if ns = p /\ len <> NONE /\ 0 < m then
1131 (f d,SOME (m - 1))
1132 else
1133 (d,len))
1134End
1135Overload ltree_delete' = “ltree_delete I”
1136
1137Theorem ltree_delete_NIL :
1138 !f a ts.
1139 ltree_delete f (Branch a ts) [] =
1140 if LFINITE ts /\ 0 < THE (LLENGTH ts) then
1141 Branch (f a)
1142 (LGENLIST (\i. THE (LNTH i ts)) (SOME (THE (LLENGTH ts) - 1)))
1143 else
1144 Branch a ts
1145Proof
1146 rw [ltree_delete_def]
1147 >- (rw [Once gen_ltree, ltree_el_def] >| (* 3 subgoals *)
1148 [ (* goal 1 (of 3) *)
1149 rw [LNTH_EQ, LNTH_LGENLIST] \\
1150 gs [LFINITE_LLENGTH] \\
1151 rename1 ‘0 < N’ \\
1152 Cases_on ‘n < N - 1’ >> simp [] \\
1153 ‘LFINITE ts’ by rw [LFINITE_LLENGTH] \\
1154 Know ‘IS_SOME (LNTH n ts)’ >- rw [LFINITE_LNTH_IS_SOME] \\
1155 rw [IS_SOME_EXISTS] >> simp [] \\
1156 rw [ltree_el_lemma, gen_ltree_unchanged],
1157 (* goal 2 (of 3) *)
1158 gs [LFINITE_LLENGTH],
1159 (* goal 3 (of 3) *)
1160 gs [LFINITE_LLENGTH] ])
1161 >> fs [] (* 2 subgoals *)
1162 >| [ (* goal 1 (of 2) *)
1163 rw [Once gen_ltree, ltree_el_def]
1164 >- (Cases_on ‘LLENGTH ts’ >> fs [LFINITE_LLENGTH])
1165 >- (Cases_on ‘LLENGTH ts’ >> fs [LFINITE_LLENGTH]) \\
1166 POP_ASSUM K_TAC \\
1167 rw [LNTH_EQ, LNTH_LGENLIST] \\
1168 ‘!n. ?x. LNTH n ts = SOME x’ by METIS_TAC [infinite_lnth_some] \\
1169 POP_ASSUM (MP_TAC o Q.SPEC ‘n’) >> rw [] \\
1170 simp [] \\
1171 fs [LFINITE_LLENGTH] \\
1172 Cases_on ‘LLENGTH ts’ >> fs [] \\
1173 Know ‘!path. (\(d,len). (d,len)) (THE (ltree_el x path)) =
1174 THE (ltree_el x path)’
1175 >- (rw [FUN_EQ_THM] \\
1176 qabbrev_tac ‘t0 = THE (ltree_el x path)’ \\
1177 Cases_on ‘t0’ >> simp []) >> Rewr' \\
1178 rw [gen_ltree_unchanged],
1179 (* goal 2 (of 2) *)
1180 rw [Once gen_ltree, ltree_el_def] \\
1181 rw [LNTH_EQ, LNTH_LGENLIST] \\
1182 Cases_on ‘LLENGTH ts’ >> simp []
1183 >- (‘~LFINITE ts’ by rw [LFINITE_LLENGTH] \\
1184 ‘!n. ?x. LNTH n ts = SOME x’ by METIS_TAC [infinite_lnth_some] \\
1185 POP_ASSUM (MP_TAC o Q.SPEC ‘n’) >> rw [] \\
1186 simp [] \\
1187 rw [ltree_el_lemma, gen_ltree_unchanged]) \\
1188 ‘LFINITE ts’ by rw [LFINITE_LLENGTH] \\
1189 rename1 ‘LLENGTH ts = SOME N’ \\
1190 rfs [] ]
1191QED
1192
1193Theorem ltree_delete_CONS :
1194 !f a ts h p t.
1195 LNTH h ts = SOME t /\ ltree_el t p <> NONE ==>
1196 ltree_delete f (Branch a ts) (h::p) =
1197 Branch a (LGENLIST (\i. if i = h then
1198 ltree_delete f (THE (LNTH h ts)) p
1199 else
1200 THE (LNTH i ts))
1201 (LLENGTH ts))
1202Proof
1203 rpt STRIP_TAC
1204 >> rw [Once ltree_delete_def]
1205 >> rw [Once gen_ltree, ltree_el_def]
1206 >> rw [LNTH_EQ, LNTH_LGENLIST]
1207 >> Cases_on ‘LLENGTH ts’ >> simp []
1208 >- (Cases_on ‘n = h’ >> simp []
1209 >- rw [ltree_delete_def] \\
1210 Know ‘~LFINITE ts’ >- rw [LFINITE_LLENGTH] \\
1211 rw [infinite_lnth_some] \\
1212 POP_ASSUM (MP_TAC o Q.SPEC ‘n’) >> rw [] \\
1213 simp [] \\
1214 Know ‘!path. (\(d,len). (d,len)) (THE (ltree_el x path)) =
1215 THE (ltree_el x path)’
1216 >- (rw [FUN_EQ_THM] \\
1217 qabbrev_tac ‘t0 = THE (ltree_el x path)’ \\
1218 Cases_on ‘t0’ >> simp []) >> Rewr' \\
1219 rw [gen_ltree_unchanged])
1220 >> Cases_on ‘n < x’ >> simp []
1221 >> Cases_on ‘n = h’ >> simp []
1222 >- rw [ltree_delete_def]
1223 >> Know ‘IS_SOME (LNTH n ts)’ >- rw [LNTH_IS_SOME]
1224 >> rw [IS_SOME_EXISTS]
1225 >> simp []
1226 >> Know ‘!path. (\(d,len). (d,len)) (THE (ltree_el x' path)) =
1227 THE (ltree_el x' path)’
1228 >- (rw [FUN_EQ_THM] \\
1229 qabbrev_tac ‘t0 = THE (ltree_el x' path)’ \\
1230 Cases_on ‘t0’ >> simp [])
1231 >> Rewr'
1232 >> rw [gen_ltree_unchanged]
1233QED
1234
1235(* NOTE: “ltree_delete” does not remove the parent branch no matter what *)
1236Theorem ltree_delete_path_stable :
1237 !f p t. p IN ltree_paths t ==> p IN ltree_paths (ltree_delete f t p)
1238Proof
1239 Q.X_GEN_TAC ‘f’
1240 >> Induct_on ‘p’ >- rw []
1241 >> rpt STRIP_TAC
1242 >> fs [ltree_paths_alt_ltree_el]
1243 >> POP_ASSUM MP_TAC
1244 >> Cases_on ‘t’ >> simp [ltree_el_def]
1245 >> Cases_on ‘LNTH h ts’ >> simp []
1246 >> STRIP_TAC
1247 (* applying ltree_delete_CONS *)
1248 >> MP_TAC (Q.SPECL [‘f’, ‘a’, ‘ts’, ‘h’, ‘p’, ‘x’] ltree_delete_CONS)
1249 >> simp []
1250 >> DISCH_THEN K_TAC
1251 >> rw [ltree_el_def, LNTH_LGENLIST]
1252 >> Cases_on ‘LLENGTH ts’ >> simp []
1253 >> rename1 ‘LLENGTH ts = SOME n’
1254 >> Know ‘IS_SOME (LNTH h ts)’ >- rw [IS_SOME_EXISTS]
1255 >> rw [LNTH_IS_SOME, LFINITE_LLENGTH]
1256QED
1257
1258Theorem ltree_el_ltree_delete :
1259 !f p t. ltree_el t p = SOME (a,SOME (SUC n)) ==>
1260 ltree_el (ltree_delete f t p) p = SOME (f a,SOME n)
1261Proof
1262 Q.X_GEN_TAC ‘f’
1263 >> Induct_on ‘p’
1264 >- (rpt STRIP_TAC \\
1265 Cases_on ‘t’ >> fs [ltree_el_def, ltree_delete_NIL] \\
1266 ‘LFINITE ts’ by rw [LFINITE_LLENGTH] \\
1267 simp [ltree_el_def])
1268 >> rpt STRIP_TAC
1269 >> Cases_on ‘t’ >> fs [ltree_el_def]
1270 >> Cases_on ‘LNTH h ts’ >> fs []
1271 >> MP_TAC (Q.SPECL [‘f’, ‘a'’, ‘ts’, ‘h’, ‘p’, ‘x’] ltree_delete_CONS)
1272 >> simp []
1273 >> DISCH_THEN K_TAC
1274 >> rw [ltree_el_def, LNTH_LGENLIST]
1275 >> Cases_on ‘LLENGTH ts’ >> simp []
1276 >> rename1 ‘LLENGTH ts = SOME N’
1277 >> Know ‘IS_SOME (LNTH h ts)’ >- rw [IS_SOME_EXISTS]
1278 >> rw [LNTH_IS_SOME, LFINITE_LLENGTH]
1279QED
1280
1281(* |- !p t.
1282 ltree_el t p = SOME (a,SOME (SUC n)) ==>
1283 ltree_el (ltree_delete' t p) p = SOME (a,SOME n)
1284 *)
1285Theorem ltree_el_ltree_delete' =
1286 ltree_el_ltree_delete |> Q.SPEC ‘I’ |> SRULE []
1287
1288(* NOTE: “ltree_el t p = SOME (a,SOME (SUC n)” indicates that “SNOC n p” is the
1289 subtree to be deleted.
1290 *)
1291Theorem ltree_delete_paths_lemma[local] :
1292 !f p t a n.
1293 ltree_el t p = SOME (a,SOME (SUC n)) ==>
1294 ltree_paths (ltree_delete f t p) =
1295 ltree_paths t DIFF
1296 (IMAGE (\q. SNOC n p ++ q) (ltree_paths (THE (ltree_lookup t (SNOC n p)))))
1297Proof
1298 Q.X_GEN_TAC ‘f’
1299 >> Induct_on ‘p’
1300 >- (rw [ltree_paths_alt_ltree_el] \\
1301 Cases_on ‘t’ \\
1302 fs [ltree_el_def, ltree_lookup_def] \\
1303 Q.PAT_X_ASSUM ‘a' = a’ K_TAC \\
1304 ‘LFINITE ts’ by rw [LFINITE_LLENGTH] \\
1305 MP_TAC (Q.SPECL [‘f’, ‘a’, ‘ts’] ltree_delete_NIL) >> simp [] \\
1306 DISCH_THEN K_TAC \\
1307 rw [Once EXTENSION] \\
1308 EQ_TAC >> rw [] >| (* 3 subgoals *)
1309 [ (* goal 1 (of 3) *)
1310 Cases_on ‘x’ >> fs [ltree_el_def, LNTH_LGENLIST] \\
1311 Cases_on ‘LNTH h ts’ >> simp []
1312 >- (Know ‘~IS_SOME (LNTH h ts)’ >- rw [] \\
1313 rw [LFINITE_LNTH_IS_SOME] \\
1314 CCONTR_TAC \\
1315 ‘~(h < n)’ by rw [] \\
1316 fs []) \\
1317 Cases_on ‘h < n’ >> fs [],
1318 (* goal 2 (of 3) *)
1319 fs [ltree_el_def, LNTH_LGENLIST],
1320 (* goal 3 (of 3) *)
1321 Cases_on ‘x’ >> fs [ltree_el_def, LNTH_LGENLIST] \\
1322 Cases_on ‘h < n’ >> simp []
1323 >- (Know ‘IS_SOME (LNTH h ts)’ >- rw [LFINITE_LNTH_IS_SOME] \\
1324 rw [IS_SOME_EXISTS] \\
1325 POP_ASSUM (fs o wrap)) \\
1326 ‘n <= h’ by rw [] \\
1327 ‘SUC n <= h \/ h = n’ by rw []
1328 >- (Know ‘~IS_SOME (LNTH h ts)’
1329 >- (ASM_SIMP_TAC bool_ss [LFINITE_LNTH_IS_SOME] \\
1330 simp []) >> DISCH_TAC \\
1331 fs []) \\
1332 POP_ASSUM (fs o wrap) \\
1333 Cases_on ‘LNTH n ts’ >> fs [] ])
1334 (* stage work *)
1335 >> rw []
1336 >> Cases_on ‘t’
1337 >> POP_ASSUM MP_TAC
1338 >> simp [ltree_el_def, ltree_lookup_def]
1339 >> Cases_on ‘LNTH h ts’ >> simp []
1340 >> DISCH_TAC
1341 >> MP_TAC (Q.SPECL [‘f’, ‘a'’, ‘ts’, ‘h’, ‘p’, ‘x’] ltree_delete_CONS)
1342 >> simp []
1343 >> DISCH_THEN K_TAC
1344 >> simp [Once ltree_paths_alt_ltree_el]
1345 >> simp [Once EXTENSION]
1346 >> Q.X_GEN_TAC ‘ns’
1347 >> EQ_TAC >> rw []
1348 >| [ (* goal 1 (of 3) *)
1349 Cases_on ‘ns’ >> fs [ltree_el_def, LNTH_LGENLIST] \\
1350 POP_ASSUM MP_TAC \\
1351 Cases_on ‘LLENGTH ts’ >> simp []
1352 >- (Cases_on ‘h' = h’ >> simp []
1353 >- (POP_ASSUM K_TAC \\
1354 DISCH_TAC \\
1355 Know ‘t IN ltree_paths (ltree_delete f x p)’
1356 >- rw [ltree_paths_alt_ltree_el] \\
1357 Q.PAT_X_ASSUM ‘!t a n. P’ (MP_TAC o Q.SPECL [‘x’, ‘a’, ‘n’]) \\
1358 simp [] >> DISCH_THEN K_TAC \\
1359 rw [ltree_paths_alt_ltree_el, ltree_el_def]) \\
1360 rw [ltree_paths_alt_ltree_el, ltree_el_def] \\
1361 Cases_on ‘LNTH h' ts’ >> simp []
1362 >- (Know ‘~LFINITE ts’ >- rw [LFINITE_LLENGTH] \\
1363 DISCH_TAC \\
1364 fs [infinite_lnth_some] \\
1365 POP_ASSUM (MP_TAC o Q.SPEC ‘h'’) >> rw []) \\
1366 fs []) \\
1367 rename1 ‘LLENGTH ts = SOME N’ \\
1368 Cases_on ‘h' < N’ >> simp [] \\
1369 Cases_on ‘h' = h’ >> simp []
1370 >- (POP_ASSUM (fs o wrap) \\
1371 DISCH_TAC \\
1372 Know ‘t IN ltree_paths (ltree_delete f x p)’
1373 >- rw [ltree_paths_alt_ltree_el] \\
1374 Q.PAT_X_ASSUM ‘!t a n. P’ (MP_TAC o Q.SPECL [‘x’, ‘a’, ‘n’]) \\
1375 simp [] >> DISCH_THEN K_TAC \\
1376 rw [ltree_paths_alt_ltree_el, ltree_el_def]) \\
1377 rw [ltree_paths_alt_ltree_el, ltree_el_def] \\
1378 Cases_on ‘LNTH h' ts’ >> simp []
1379 >- (‘LFINITE ts’ by rw [LFINITE_LLENGTH] \\
1380 Know ‘IS_SOME (LNTH h' ts)’ >- rw [LFINITE_LNTH_IS_SOME] \\
1381 rw [IS_SOME_EXISTS]) \\
1382 fs [],
1383 (* goal 2 (of 3) *)
1384 POP_ASSUM MP_TAC \\
1385 simp [ltree_el_def, LNTH_LGENLIST] \\
1386 Cases_on ‘LLENGTH ts’ >> simp []
1387 >- (DISCH_TAC \\
1388 Know ‘SNOC n p ++ q IN ltree_paths (ltree_delete f x p)’
1389 >- rw [ltree_paths_alt_ltree_el] \\
1390 Q.PAT_X_ASSUM ‘!t a n. P’ (MP_TAC o Q.SPECL [‘x’, ‘a’, ‘n’]) \\
1391 simp []) \\
1392 rename1 ‘LLENGTH ts = SOME N’ \\
1393 Cases_on ‘h < N’ >> simp [] \\
1394 DISCH_TAC \\
1395 Know ‘SNOC n p ++ q IN ltree_paths (ltree_delete f x p)’
1396 >- rw [ltree_paths_alt_ltree_el] \\
1397 Q.PAT_X_ASSUM ‘!t a n. P’ (MP_TAC o Q.SPECL [‘x’, ‘a’, ‘n’]) \\
1398 simp [],
1399 (* goal 3 (of 3) *)
1400 Cases_on ‘ns’ >> fs []
1401 >- (simp [ltree_el_def, LNTH_LGENLIST]) \\
1402 simp [ltree_el_def, LNTH_LGENLIST] \\
1403 Cases_on ‘LLENGTH ts’ >> simp []
1404 >- (Cases_on ‘h' = h’ >> simp []
1405 >- (POP_ASSUM (fs o wrap) \\
1406 Know ‘ltree_el (ltree_delete f x p) t <> NONE <=>
1407 t IN ltree_paths (ltree_delete f x p)’
1408 >- rw [ltree_paths_alt_ltree_el] >> Rewr' \\
1409 Q.PAT_X_ASSUM ‘!t a n. P’ (MP_TAC o Q.SPECL [‘x’, ‘a’, ‘n’]) \\
1410 simp [] >> DISCH_THEN K_TAC \\
1411 Q.PAT_X_ASSUM ‘h::t IN ltree_paths (Branch a' ts)’ MP_TAC \\
1412 simp [ltree_paths_alt_ltree_el, ltree_el_def]) \\
1413 fs [] \\
1414 Q.PAT_X_ASSUM ‘h'::t IN ltree_paths (Branch a' ts)’ MP_TAC \\
1415 simp [ltree_paths_alt_ltree_el, ltree_el_def] \\
1416 Cases_on ‘LNTH h' ts’ >> simp []) \\
1417 rename1 ‘LLENGTH ts = SOME N’ \\
1418 Cases_on ‘h' < N’ >> simp []
1419 >- (Cases_on ‘h' = h’ >> simp []
1420 >- (POP_ASSUM (fs o wrap) \\
1421 Know ‘ltree_el (ltree_delete f x p) t <> NONE <=>
1422 t IN ltree_paths (ltree_delete f x p)’
1423 >- rw [ltree_paths_alt_ltree_el] >> Rewr' \\
1424 Q.PAT_X_ASSUM ‘!t a n. P’ (MP_TAC o Q.SPECL [‘x’, ‘a’, ‘n’]) \\
1425 simp [] >> DISCH_THEN K_TAC \\
1426 Q.PAT_X_ASSUM ‘h::t IN ltree_paths (Branch a' ts)’ MP_TAC \\
1427 rw [ltree_paths_alt_ltree_el, ltree_el_def]) \\
1428 fs [] \\
1429 Q.PAT_X_ASSUM ‘h'::t IN ltree_paths (Branch a' ts)’ MP_TAC \\
1430 simp [ltree_paths_alt_ltree_el, ltree_el_def] \\
1431 Cases_on ‘LNTH h' ts’ >> simp []) \\
1432 ‘N <= h'’ by rw [] \\
1433 Q.PAT_X_ASSUM ‘h'::t IN ltree_paths (Branch a' ts)’ MP_TAC \\
1434 simp [ltree_paths_alt_ltree_el, ltree_el_def] \\
1435 Cases_on ‘LNTH h' ts’ >> simp [] \\
1436 ‘LFINITE ts’ by rw [LFINITE_LLENGTH] \\
1437 Know ‘IS_SOME (LNTH h' ts)’ >- rw [IS_SOME_EXISTS] \\
1438 simp [LFINITE_LNTH_IS_SOME] ]
1439QED
1440
1441Theorem ltree_delete_paths :
1442 !f p t n.
1443 p IN ltree_paths t /\ ltree_branching t p = SOME (SUC n) ==>
1444 ltree_paths (ltree_delete f t p) =
1445 ltree_paths t DIFF
1446 IMAGE (\q. SNOC n p ++ q) (ltree_paths (THE (ltree_lookup t (SNOC n p))))
1447Proof
1448 rpt STRIP_TAC
1449 >> MATCH_MP_TAC ltree_delete_paths_lemma
1450 >> Cases_on ‘t’
1451 >> fs [ltree_paths_alt_ltree_el, ltree_branching_def]
1452 >> Cases_on ‘p’ >> fs [ltree_el_def]
1453 >> Cases_on ‘LNTH h ts’ >> fs []
1454 >> Cases_on ‘ltree_el x t’ >> fs []
1455 >> rename1 ‘SND y = SOME (SUC n)’
1456 >> Cases_on ‘y’ >> fs []
1457QED
1458
1459(* NOTE: “ltree_insert f t p t0” inserts t0 as the right-most children of the
1460 ltree node “ltree_lookup t p”.
1461 *)
1462Definition ltree_insert_def :
1463 ltree_insert f t p t0 =
1464 gen_ltree (\ns. if ltree_el t ns <> NONE then
1465 let (d,len) = THE (ltree_el t ns); m = THE len in
1466 if ns = p /\ len <> NONE then
1467 (f d,SOME (m + 1))
1468 else
1469 (d,len)
1470 else
1471 THE (ltree_el t0 (DROP (LENGTH p + 1) ns)))
1472End
1473Overload ltree_insert' = “ltree_insert I”
1474
1475Theorem ltree_insert_NIL :
1476 !f a ts t0.
1477 ltree_insert f (Branch a ts) [] t0 =
1478 if LFINITE ts then
1479 Branch (f a)
1480 (LGENLIST (\i. if i < THE (LLENGTH ts) then THE (LNTH i ts)
1481 else t0)
1482 (SOME (THE (LLENGTH ts) + 1)))
1483 else
1484 Branch a ts
1485Proof
1486 rw [ltree_insert_def]
1487 >- (rw [Once gen_ltree, ltree_el_def] >| (* 3 subgoals *)
1488 [ (* goal 1 (of 3) *)
1489 rw [LNTH_EQ, LNTH_LGENLIST] \\
1490 gs [LFINITE_LLENGTH] \\
1491 rename1 ‘LLENGTH ts = SOME N’ \\
1492 Cases_on ‘n < N + 1’ >> simp [] \\
1493 ‘LFINITE ts’ by rw [LFINITE_LLENGTH] \\
1494 Cases_on ‘LNTH n ts’ >> simp []
1495 >- (Know ‘~IS_SOME (LNTH n ts)’ >- rw [] \\
1496 POP_ASSUM K_TAC \\
1497 ASM_SIMP_TAC bool_ss [LFINITE_LNTH_IS_SOME] \\
1498 simp [] \\
1499 rw [gen_ltree_unchanged]) \\
1500 Know ‘IS_SOME (LNTH n ts)’ >- rw [] \\
1501 rw [LFINITE_LNTH_IS_SOME] \\
1502 simp [ltree_el_lemma] \\
1503 rw [gen_ltree_unchanged_extra],
1504 (* goal 2 (of 3) *)
1505 gs [LFINITE_LLENGTH],
1506 (* goal 3 (of 3) *)
1507 gs [LFINITE_LLENGTH] ])
1508 >> rw [Once gen_ltree, ltree_el_def]
1509 >- (Cases_on ‘LLENGTH ts’ >> fs [LFINITE_LLENGTH])
1510 >- (Cases_on ‘LLENGTH ts’ >> fs [LFINITE_LLENGTH])
1511 >> rw [LNTH_EQ, LNTH_LGENLIST]
1512 >> ‘!n. ?x. LNTH n ts = SOME x’ by METIS_TAC [infinite_lnth_some]
1513 >> POP_ASSUM (MP_TAC o Q.SPEC ‘n’) >> rw []
1514 >> simp []
1515 >> simp [ltree_el_lemma]
1516 >> rw [gen_ltree_unchanged_extra]
1517QED
1518
1519Theorem ltree_insert_CONS :
1520 !f a ts h p t t0.
1521 LNTH h ts = SOME t /\ ltree_el t p <> NONE ==>
1522 ltree_insert f (Branch a ts) (h::p) t0 =
1523 Branch a (LGENLIST (\i. if i = h then
1524 ltree_insert f (THE (LNTH h ts)) p t0
1525 else
1526 THE (LNTH i ts))
1527 (LLENGTH ts))
1528Proof
1529 rpt STRIP_TAC
1530 >> rw [Once ltree_insert_def]
1531 >> rw [Once gen_ltree, ltree_el_def]
1532 >> rw [LNTH_EQ, LNTH_LGENLIST]
1533 >> Cases_on ‘LLENGTH ts’ >> simp []
1534 >- (Cases_on ‘n = h’ >> simp []
1535 >- rw [ltree_insert_def, ADD1] \\
1536 Know ‘~LFINITE ts’ >- rw [LFINITE_LLENGTH] \\
1537 rw [infinite_lnth_some] \\
1538 POP_ASSUM (MP_TAC o Q.SPEC ‘n’) >> rw [] \\
1539 simp [] \\
1540 Know ‘!path. (\(d,len). (d,len)) (THE (ltree_el x path)) =
1541 THE (ltree_el x path)’
1542 >- (rw [FUN_EQ_THM] \\
1543 qabbrev_tac ‘t0 = THE (ltree_el x path)’ \\
1544 Cases_on ‘t0’ >> simp []) >> Rewr' \\
1545 rw [gen_ltree_unchanged_extra])
1546 >> Cases_on ‘n < x’ >> simp []
1547 >> Cases_on ‘n = h’ >> simp []
1548 >- rw [ltree_insert_def, ADD1]
1549 >> Know ‘IS_SOME (LNTH n ts)’ >- rw [LNTH_IS_SOME]
1550 >> rw [IS_SOME_EXISTS]
1551 >> simp []
1552 >> Know ‘!path. (\(d,len). (d,len)) (THE (ltree_el x' path)) =
1553 THE (ltree_el x' path)’
1554 >- (rw [FUN_EQ_THM] \\
1555 qabbrev_tac ‘t0 = THE (ltree_el x' path)’ \\
1556 Cases_on ‘t0’ >> simp [])
1557 >> Rewr'
1558 >> rw [gen_ltree_unchanged_extra]
1559QED
1560
1561Theorem ltree_finite_ltree_insert_lemma[local] :
1562 !f p t t0 d len.
1563 ltree_finite t /\ ltree_el t p = SOME (d,len) /\
1564 ltree_finite t0 ==> ltree_finite (ltree_insert f t p t0)
1565Proof
1566 Q.X_GEN_TAC ‘f’
1567 >> Induct_on ‘p’
1568 >- (rw [ltree_el] \\
1569 Cases_on ‘t’ >> rw [ltree_insert_NIL] \\
1570 rw [ltree_finite, IN_LSET, LNTH_LGENLIST] \\
1571 gs [LFINITE_LLENGTH] \\
1572 rename1 ‘n < N + 1’ \\
1573 Cases_on ‘n < N’ >> simp [] \\
1574 ‘LFINITE ts’ by rw [LFINITE_LLENGTH] \\
1575 Know ‘IS_SOME (LNTH n ts)’ >- rw [LFINITE_LNTH_IS_SOME] \\
1576 rw [IS_SOME_EXISTS] \\
1577 simp [] \\
1578 Q.PAT_X_ASSUM ‘ltree_finite (Branch a ts)’
1579 (MP_TAC o REWRITE_RULE [ltree_finite]) \\
1580 rw [IN_LSET] \\
1581 POP_ASSUM MATCH_MP_TAC \\
1582 Q.EXISTS_TAC ‘n’ >> art [])
1583 >> rpt STRIP_TAC
1584 >> Cases_on ‘t’ >> fs [ltree_el_def]
1585 >> Cases_on ‘LNTH h ts’ >> fs []
1586 >> MP_TAC (Q.SPECL [‘f’, ‘a’, ‘ts’, ‘h’, ‘p’, ‘x’, ‘t0’] ltree_insert_CONS)
1587 >> simp []
1588 >> DISCH_THEN K_TAC
1589 >> rw [ltree_finite, IN_LSET, LNTH_LGENLIST]
1590 >- (Q.PAT_X_ASSUM ‘ltree_finite (Branch a ts)’
1591 (MP_TAC o REWRITE_RULE [ltree_finite]) \\
1592 rw [LFINITE_LLENGTH, IN_LSET, GSYM IS_SOME_EQ_NOT_NONE, IS_SOME_EXISTS])
1593 >> Q.PAT_X_ASSUM ‘ltree_finite (Branch a ts)’
1594 (MP_TAC o REWRITE_RULE [ltree_finite])
1595 >> rw [LFINITE_LLENGTH, IN_LSET, GSYM IS_SOME_EQ_NOT_NONE, IS_SOME_EXISTS]
1596 >> rename1 ‘LLENGTH ts = SOME N’
1597 >> fs []
1598 >> Cases_on ‘n = h’ >> fs []
1599 >- (Q.PAT_X_ASSUM ‘ltree_insert f x p t0 = t’ (REWRITE_TAC o wrap o SYM) \\
1600 LAST_X_ASSUM MATCH_MP_TAC >> art [] \\
1601 qexistsl_tac [‘d’, ‘len’] >> art [] \\
1602 FIRST_X_ASSUM MATCH_MP_TAC \\
1603 Q.EXISTS_TAC ‘h’ >> art [])
1604 >> FIRST_X_ASSUM MATCH_MP_TAC
1605 >> Q.EXISTS_TAC ‘n’ >> simp []
1606 >> ‘LFINITE ts’ by rw [LFINITE_LLENGTH]
1607 >> Know ‘IS_SOME (LNTH n ts)’ >- rw [LFINITE_LNTH_IS_SOME]
1608 >> rw [IS_SOME_EXISTS]
1609 >> simp []
1610QED
1611
1612Theorem ltree_finite_ltree_insert :
1613 !f p t t0.
1614 ltree_finite t /\ p IN ltree_paths t /\ ltree_finite t0 ==>
1615 ltree_finite (ltree_insert f t p t0)
1616Proof
1617 rw [ltree_paths_alt_ltree_el, GSYM IS_SOME_EQ_NOT_NONE, IS_SOME_EXISTS]
1618 >> rename1 ‘ltree_el t p = SOME y’
1619 >> Cases_on ‘y’
1620 >> MATCH_MP_TAC ltree_finite_ltree_insert_lemma
1621 >> qexistsl_tac [‘q’, ‘r’] >> art []
1622QED
1623
1624Theorem ltree_insert_path_stable :
1625 !f p t t0. p IN ltree_paths t ==> p IN ltree_paths (ltree_insert f t p t0)
1626Proof
1627 Q.X_GEN_TAC ‘f’
1628 >> Induct_on ‘p’ >- rw []
1629 >> rpt STRIP_TAC
1630 >> fs [ltree_paths_alt_ltree_el]
1631 >> POP_ASSUM MP_TAC
1632 >> Cases_on ‘t’ >> simp [ltree_el_def]
1633 >> Cases_on ‘LNTH h ts’ >> simp []
1634 >> STRIP_TAC
1635 (* applying ltree_delete_CONS *)
1636 >> MP_TAC (Q.SPECL [‘f’, ‘a’, ‘ts’, ‘h’, ‘p’, ‘x’, ‘t0’] ltree_insert_CONS)
1637 >> simp []
1638 >> DISCH_THEN K_TAC
1639 >> rw [ltree_el_def, LNTH_LGENLIST]
1640 >> Cases_on ‘LLENGTH ts’ >> simp []
1641 >> rename1 ‘LLENGTH ts = SOME n’
1642 >> Know ‘IS_SOME (LNTH h ts)’ >- rw [IS_SOME_EXISTS]
1643 >> rw [LNTH_IS_SOME, LFINITE_LLENGTH]
1644QED
1645
1646Theorem ltree_el_ltree_insert :
1647 !f p t t0. ltree_el t p = SOME (a,SOME n) ==>
1648 ltree_el (ltree_insert f t p t0) p = SOME (f a,SOME (SUC n))
1649Proof
1650 Q.X_GEN_TAC ‘f’
1651 >> Induct_on ‘p’
1652 >- (rpt STRIP_TAC \\
1653 Cases_on ‘t’ >> fs [ltree_el_def, ltree_insert_NIL] \\
1654 ‘LFINITE ts’ by rw [LFINITE_LLENGTH] \\
1655 simp [ltree_el_def])
1656 >> rpt STRIP_TAC
1657 >> Cases_on ‘t’ >> fs [ltree_el_def]
1658 >> Cases_on ‘LNTH h ts’ >> fs []
1659 >> MP_TAC (Q.SPECL [‘f’, ‘a'’, ‘ts’, ‘h’, ‘p’, ‘x’, ‘t0’] ltree_insert_CONS)
1660 >> simp []
1661 >> DISCH_THEN K_TAC
1662 >> rw [ltree_el_def, LNTH_LGENLIST]
1663 >> Cases_on ‘LLENGTH ts’ >> simp []
1664 >> rename1 ‘LLENGTH ts = SOME N’
1665 >> Know ‘IS_SOME (LNTH h ts)’ >- rw [IS_SOME_EXISTS]
1666 >> rw [LNTH_IS_SOME, LFINITE_LLENGTH]
1667QED
1668
1669(* |- !p t t0.
1670 ltree_el t p = SOME (a,SOME n) ==>
1671 ltree_el (ltree_insert I t p t0) p = SOME (a,SOME (SUC n))
1672 *)
1673Theorem ltree_el_ltree_insert' =
1674 ltree_el_ltree_insert |> Q.SPEC ‘I’ |> SRULE []
1675
1676Theorem ltree_insert_paths_lemma[local] :
1677 !f p t a n.
1678 ltree_el t p = SOME (a,SOME n) ==>
1679 ltree_paths (ltree_insert f t p t0) =
1680 ltree_paths t UNION (IMAGE (\q. SNOC n p ++ q) (ltree_paths t0))
1681Proof
1682 Q.X_GEN_TAC ‘f’
1683 >> Induct_on ‘p’
1684 >- (rw [ltree_paths_alt_ltree_el] \\
1685 Cases_on ‘t’ >> fs [ltree_el_def, ltree_lookup_def] \\
1686 Q.PAT_X_ASSUM ‘a' = a’ K_TAC \\
1687 ‘LFINITE ts’ by rw [LFINITE_LLENGTH] \\
1688 MP_TAC (Q.SPECL [‘f’, ‘a’, ‘ts’, ‘t0’] ltree_insert_NIL) >> simp [] \\
1689 DISCH_THEN K_TAC \\
1690 rw [Once EXTENSION] \\
1691 EQ_TAC >> rw [] >| (* 2 subgoals *)
1692 [ (* goal 1 (of 2) *)
1693 Cases_on ‘x’ >> fs [ltree_el_def, LNTH_LGENLIST] \\
1694 Cases_on ‘h < n + 1’ >> fs [] \\
1695 ‘h = n \/ h < n’ by rw [] >- fs [] \\
1696 fs [] \\
1697 Know ‘IS_SOME (LNTH h ts)’ >- rw [LFINITE_LNTH_IS_SOME] \\
1698 REWRITE_TAC [IS_SOME_EXISTS] \\
1699 rw [] \\
1700 CCONTR_TAC >> fs [],
1701 (* goal 2 (of 2) *)
1702 Cases_on ‘x’ >> fs [ltree_el_def, LNTH_LGENLIST] \\
1703 Cases_on ‘LNTH h ts’ >> fs [] \\
1704 Know ‘IS_SOME (LNTH h ts)’ >- rw [] \\
1705 rw [LFINITE_LNTH_IS_SOME] \\
1706 CCONTR_TAC >> fs [] ])
1707 (* stage work *)
1708 >> rw []
1709 >> Cases_on ‘t’
1710 >> POP_ASSUM MP_TAC
1711 >> simp [ltree_el_def, ltree_lookup_def]
1712 >> Cases_on ‘LNTH h ts’ >> simp []
1713 >> DISCH_TAC
1714 >> MP_TAC (Q.SPECL [‘f’, ‘a'’, ‘ts’, ‘h’, ‘p’, ‘x’, ‘t0’] ltree_insert_CONS)
1715 >> simp []
1716 >> DISCH_THEN K_TAC
1717 >> simp [Once ltree_paths_alt_ltree_el]
1718 >> simp [Once EXTENSION]
1719 >> Q.X_GEN_TAC ‘ns’
1720 >> EQ_TAC >> rw []
1721 >| [ (* goal 1 (of 3) *)
1722 Cases_on ‘ns’ >> fs [ltree_el_def, LNTH_LGENLIST] \\
1723 POP_ASSUM MP_TAC \\
1724 Cases_on ‘LLENGTH ts’ >> simp []
1725 >- (Cases_on ‘h' = h’ >> simp []
1726 >- (POP_ASSUM K_TAC \\
1727 DISCH_TAC \\
1728 Know ‘t IN ltree_paths (ltree_insert f x p t0)’
1729 >- rw [ltree_paths_alt_ltree_el] \\
1730 Q.PAT_X_ASSUM ‘!t a n. P’ (MP_TAC o Q.SPECL [‘x’, ‘a’, ‘n’]) \\
1731 simp [] >> DISCH_THEN K_TAC \\
1732 rw [ltree_paths_alt_ltree_el, ltree_el_def]) \\
1733 rw [ltree_paths_alt_ltree_el, ltree_el_def] \\
1734 Cases_on ‘LNTH h' ts’ >> simp []
1735 >- (Know ‘~LFINITE ts’ >- rw [LFINITE_LLENGTH] \\
1736 DISCH_TAC \\
1737 fs [infinite_lnth_some] \\
1738 POP_ASSUM (MP_TAC o Q.SPEC ‘h'’) >> rw []) \\
1739 fs []) \\
1740 rename1 ‘LLENGTH ts = SOME N’ \\
1741 Cases_on ‘h' < N’ >> simp [] \\
1742 Cases_on ‘h' = h’ >> simp []
1743 >- (POP_ASSUM (fs o wrap) \\
1744 DISCH_TAC \\
1745 Know ‘t IN ltree_paths (ltree_insert f x p t0)’
1746 >- rw [ltree_paths_alt_ltree_el] \\
1747 Q.PAT_X_ASSUM ‘!t a n. P’ (MP_TAC o Q.SPECL [‘x’, ‘a’, ‘n’]) \\
1748 simp [] >> DISCH_THEN K_TAC \\
1749 rw [ltree_paths_alt_ltree_el, ltree_el_def]) \\
1750 rw [ltree_paths_alt_ltree_el, ltree_el_def] \\
1751 Cases_on ‘LNTH h' ts’ >> simp []
1752 >- (‘LFINITE ts’ by rw [LFINITE_LLENGTH] \\
1753 Know ‘IS_SOME (LNTH h' ts)’ >- rw [LFINITE_LNTH_IS_SOME] \\
1754 rw [IS_SOME_EXISTS]) \\
1755 fs [],
1756 (* goal 2 (of 3) *)
1757 Cases_on ‘ns’ >> fs []
1758 >- (simp [ltree_el_def, LNTH_LGENLIST]) \\
1759 simp [ltree_el_def, LNTH_LGENLIST] \\
1760 Cases_on ‘LLENGTH ts’ >> simp []
1761 >- (Cases_on ‘h' = h’ >> simp []
1762 >- (POP_ASSUM (fs o wrap) \\
1763 Know ‘ltree_el (ltree_insert f x p t0) t <> NONE <=>
1764 t IN ltree_paths (ltree_insert f x p t0)’
1765 >- rw [ltree_paths_alt_ltree_el] >> Rewr' \\
1766 Q.PAT_X_ASSUM ‘!t a n. P’ (MP_TAC o Q.SPECL [‘x’, ‘a’, ‘n’]) \\
1767 simp [] >> DISCH_THEN K_TAC \\
1768 Q.PAT_X_ASSUM ‘h::t IN ltree_paths (Branch a' ts)’ MP_TAC \\
1769 simp [ltree_paths_alt_ltree_el, ltree_el_def]) \\
1770 fs [] \\
1771 Q.PAT_X_ASSUM ‘h'::t IN ltree_paths (Branch a' ts)’ MP_TAC \\
1772 simp [ltree_paths_alt_ltree_el, ltree_el_def] \\
1773 Cases_on ‘LNTH h' ts’ >> simp []) \\
1774 rename1 ‘LLENGTH ts = SOME N’ \\
1775 Cases_on ‘h' < N’ >> simp []
1776 >- (Cases_on ‘h' = h’ >> simp []
1777 >- (POP_ASSUM (fs o wrap) \\
1778 Know ‘ltree_el (ltree_insert f x p t0) t <> NONE <=>
1779 t IN ltree_paths (ltree_insert f x p t0)’
1780 >- rw [ltree_paths_alt_ltree_el] >> Rewr' \\
1781 Q.PAT_X_ASSUM ‘!t a n. P’ (MP_TAC o Q.SPECL [‘x’, ‘a’, ‘n’]) \\
1782 simp [] >> DISCH_THEN K_TAC \\
1783 Q.PAT_X_ASSUM ‘h::t IN ltree_paths (Branch a' ts)’ MP_TAC \\
1784 rw [ltree_paths_alt_ltree_el, ltree_el_def]) \\
1785 fs [] \\
1786 Q.PAT_X_ASSUM ‘h'::t IN ltree_paths (Branch a' ts)’ MP_TAC \\
1787 simp [ltree_paths_alt_ltree_el, ltree_el_def] \\
1788 Cases_on ‘LNTH h' ts’ >> simp []) \\
1789 ‘N <= h'’ by rw [] \\
1790 Q.PAT_X_ASSUM ‘h'::t IN ltree_paths (Branch a' ts)’ MP_TAC \\
1791 simp [ltree_paths_alt_ltree_el, ltree_el_def] \\
1792 Cases_on ‘LNTH h' ts’ >> simp [] \\
1793 ‘LFINITE ts’ by rw [LFINITE_LLENGTH] \\
1794 Know ‘IS_SOME (LNTH h' ts)’ >- rw [IS_SOME_EXISTS] \\
1795 simp [LFINITE_LNTH_IS_SOME],
1796 (* goal 3 (of 3) *)
1797 simp [ltree_el_def, LNTH_LGENLIST] \\
1798 Cases_on ‘LLENGTH ts’ >> simp []
1799 >- (Know ‘ltree_el (ltree_insert f x p t0) (SNOC n p ++ q) <> NONE <=>
1800 SNOC n p ++ q IN ltree_paths (ltree_insert f x p t0)’
1801 >- rw [ltree_paths_alt_ltree_el] >> Rewr' \\
1802 Q.PAT_X_ASSUM ‘!t a n. P’ (MP_TAC o Q.SPECL [‘x’, ‘a’, ‘n’]) \\
1803 simp []) \\
1804 rename1 ‘LLENGTH ts = SOME N’ \\
1805 Cases_on ‘h < N’ >> simp []
1806 >- (Know ‘ltree_el (ltree_insert f x p t0) (SNOC n p ++ q) <> NONE <=>
1807 SNOC n p ++ q IN ltree_paths (ltree_insert f x p t0)’
1808 >- rw [ltree_paths_alt_ltree_el] >> Rewr' \\
1809 Q.PAT_X_ASSUM ‘!t a n. P’ (MP_TAC o Q.SPECL [‘x’, ‘a’, ‘n’]) \\
1810 simp []) \\
1811 ‘LFINITE ts’ by rw [LFINITE_LLENGTH] \\
1812 Know ‘IS_SOME (LNTH h ts)’ >- rw [IS_SOME_EXISTS] \\
1813 ASM_SIMP_TAC bool_ss [LFINITE_LNTH_IS_SOME] \\
1814 simp [] ]
1815QED
1816
1817Theorem ltree_insert_paths :
1818 !f p t n t0.
1819 p IN ltree_paths t /\ ltree_branching t p = SOME n ==>
1820 ltree_paths (ltree_insert f t p t0) =
1821 ltree_paths t UNION (IMAGE (\q. SNOC n p ++ q) (ltree_paths t0))
1822Proof
1823 rpt STRIP_TAC
1824 >> MATCH_MP_TAC ltree_insert_paths_lemma
1825 >> Cases_on ‘t’
1826 >> fs [ltree_paths_alt_ltree_el, ltree_branching_def]
1827 >> Cases_on ‘p’ >> fs [ltree_el_def]
1828 >> Cases_on ‘LNTH h ts’ >> fs []
1829 >> Cases_on ‘ltree_el x t’ >> fs []
1830 >> rename1 ‘SND y = SOME n’
1831 >> Cases_on ‘y’ >> fs []
1832QED
1833
1834Theorem ltree_insert_delete :
1835 !n p t t0 f g d len.
1836 ltree_branching t p = SOME (SUC n) /\
1837 ltree_lookup t (SNOC n p) = SOME t0 /\
1838 ltree_el t p = SOME (d,len) /\ f (g d) = d ==>
1839 ltree_insert f (ltree_delete g t p) p t0 = t
1840Proof
1841 rpt STRIP_TAC
1842 (* initial preparation (for induction) *)
1843 >> Know ‘p IN ltree_paths t’
1844 >- (MATCH_MP_TAC ltree_paths_inclusive \\
1845 Q.EXISTS_TAC ‘SNOC n p’ \\
1846 rw [isPREFIX_SNOC, ltree_paths_def])
1847 >> DISCH_TAC
1848 >> Q.PAT_X_ASSUM ‘ltree_lookup t (SNOC n p) = SOME t0’ MP_TAC
1849 >> Know ‘ltree_lookup t (SNOC n p) =
1850 ltree_lookup (THE (ltree_lookup t p)) [n]’
1851 >- (MATCH_MP_TAC ltree_lookup_SNOC \\
1852 fs [ltree_paths_def])
1853 >> Rewr'
1854 >> POP_ASSUM MP_TAC
1855 >> simp [ltree_paths_def]
1856 >> simp [GSYM IS_SOME_EQ_NOT_NONE, IS_SOME_EXISTS]
1857 >> STRIP_TAC
1858 >> Cases_on ‘x’
1859 >> simp [ltree_lookup_def]
1860 >> Cases_on ‘LNTH n ts’ >> simp []
1861 >> DISCH_THEN (fs o wrap)
1862 >> fs [ltree_branching_def]
1863 >> MP_TAC (Q.SPECL [‘p’, ‘t’] ltree_el_alt_ltree_lookup)
1864 >> rw [ltree_paths_def]
1865 >> POP_ASSUM (ASSUME_TAC o SYM) (* LLENGTH ts = SOME (SUC n) *)
1866 >> Q.PAT_X_ASSUM ‘ltree_el t p = _’ K_TAC
1867 (* stage work *)
1868 >> rpt (POP_ASSUM MP_TAC)
1869 >> qid_spec_tac ‘t0’
1870 >> qid_spec_tac ‘t’
1871 >> qid_spec_tac ‘a’
1872 >> qid_spec_tac ‘ts’
1873 >> qid_spec_tac ‘n’
1874 >> qid_spec_tac ‘p’
1875 >> Induct_on ‘p’
1876 >- (rw [ltree_lookup] \\
1877 (* 1. eliminating ltree_delete *)
1878 simp [ltree_delete_def] \\
1879 simp [Once gen_ltree, ltree_el_def] \\
1880 qmatch_abbrev_tac ‘ltree_insert f t' [] t0 = _’ \\
1881 Know ‘t' = Branch (g a) (LGENLIST (\i. THE (LNTH i ts)) (SOME n))’
1882 >- (simp [Abbr ‘t'’, LNTH_EQ, LNTH_LGENLIST] \\
1883 Q.X_GEN_TAC ‘i’ \\
1884 Cases_on ‘i < n’ >> simp [] \\
1885 Cases_on ‘LNTH i ts’ >> simp []
1886 >- (Know ‘IS_SOME (LNTH i ts)’
1887 >- (MATCH_MP_TAC LNTH_IS_SOME_MONO \\
1888 Q.EXISTS_TAC ‘n’ >> simp [IS_SOME_EXISTS]) \\
1889 rw [IS_SOME_EXISTS]) \\
1890 simp [ltree_el_lemma, gen_ltree_unchanged]) >> Rewr' \\
1891 qunabbrev_tac ‘t'’ \\
1892 (* 2. eliminating ltree_insert *)
1893 simp [ltree_insert_def] \\
1894 simp [Once gen_ltree, ltree_el_def, LNTH_LGENLIST] \\
1895 (* applying LNTH_EQ again *)
1896 simp [LNTH_EQ, LNTH_LGENLIST, GSYM ADD1] \\
1897 Q.X_GEN_TAC ‘i’ \\
1898 ‘LFINITE ts’ by rw [LFINITE_LLENGTH] \\
1899 reverse (Cases_on ‘i < SUC n’ >> simp [])
1900 >- (MATCH_MP_TAC LNTH_LLENGTH_NONE \\
1901 Q.EXISTS_TAC ‘SUC n’ >> rw []) \\
1902 ‘i = n \/ i < n’ by rw [] >> simp [] >- rw [gen_ltree_unchanged] \\
1903 (* so far so good ... *)
1904 qabbrev_tac ‘t1 = THE (LNTH i ts)’ \\
1905 simp [ltree_el_lemma] \\
1906 (* so far so good ... *)
1907 ‘IS_SOME (LNTH i ts)’ by rw [LFINITE_LNTH_IS_SOME] \\
1908 fs [IS_SOME_EXISTS, Abbr ‘t1’] \\
1909 rw [gen_ltree_unchanged_extra])
1910 (* stage work *)
1911 >> rpt GEN_TAC
1912 >> Cases_on ‘t’ >> simp [ltree_lookup_def]
1913 >> Cases_on ‘LNTH h ts'’ >> rw []
1914 (* applying ltree_delete_CONS *)
1915 >> Know ‘ltree_delete g (Branch a' ts') (h::p) =
1916 Branch a' (LGENLIST (\i. if i = h then
1917 ltree_delete g (THE (LNTH h ts')) p
1918 else
1919 THE (LNTH i ts'))
1920 (LLENGTH ts'))’
1921 >- (MATCH_MP_TAC ltree_delete_CONS \\
1922 Q.EXISTS_TAC ‘x’ >> art [] \\
1923 Know ‘p IN ltree_paths x’ >- rw [ltree_paths_def] \\
1924 rw [ltree_paths_alt_ltree_el])
1925 >> Rewr'
1926 >> simp []
1927 >> qmatch_abbrev_tac ‘ltree_insert f (Branch a' ts1) (h::p) t0 = _’
1928 (* applying ltree_insert_CONS *)
1929 >> Know ‘ltree_insert f (Branch a' ts1) (h::p) t0 =
1930 Branch a' (LGENLIST (\i. if i = h then
1931 ltree_insert f (THE (LNTH h ts1)) p t0
1932 else
1933 THE (LNTH i ts1)) (LLENGTH ts1))’
1934 >- (MATCH_MP_TAC ltree_insert_CONS \\
1935 simp [Abbr ‘ts1’, LNTH_LGENLIST] \\
1936 Cases_on ‘LLENGTH ts'’ >> simp []
1937 >- (MP_TAC (Q.SPECL [‘g’, ‘p’, ‘x’] ltree_delete_path_stable) \\
1938 simp [ltree_paths_alt_ltree_el, GSYM ltree_lookup_iff_ltree_el]) \\
1939 STRONG_CONJ_TAC
1940 >- (Know ‘IS_SOME (LNTH h ts')’ >- rw [IS_SOME_EXISTS] \\
1941 simp [LNTH_IS_SOME] \\
1942 impl_tac >- rw [LFINITE_LLENGTH] >> simp []) >> DISCH_TAC \\
1943 rename1 ‘h < N’ \\
1944 MP_TAC (Q.SPECL [‘g’, ‘p’, ‘x’] ltree_delete_path_stable) \\
1945 simp [ltree_paths_alt_ltree_el, GSYM ltree_lookup_iff_ltree_el])
1946 >> Rewr'
1947 >> simp [LNTH_EQ, LNTH_LGENLIST, Abbr ‘ts1’]
1948 >> Q.X_GEN_TAC ‘i’
1949 >> Cases_on ‘LLENGTH ts'’ >> simp []
1950 >- (Cases_on ‘i = h’ >> simp [] \\
1951 Know ‘~LFINITE ts'’ >- rw [LFINITE_LLENGTH] \\
1952 rw [infinite_lnth_some] \\
1953 POP_ASSUM (MP_TAC o Q.SPEC ‘i’) >> rw [] \\
1954 simp [])
1955 >> reverse (Cases_on ‘i < x'’) >> simp []
1956 >- (‘x' <= i’ by rw [] \\
1957 MATCH_MP_TAC LNTH_LLENGTH_NONE \\
1958 Q.EXISTS_TAC ‘x'’ >> art [])
1959 >> Cases_on ‘i = h’ >> simp []
1960 >> Suff ‘IS_SOME (LNTH i ts')’ >- (rw [IS_SOME_EXISTS] >> simp [])
1961 >> rw [LNTH_IS_SOME]
1962QED
1963
1964Theorem ltree_insert_delete' :
1965 !n p t t0.
1966 ltree_branching t p = SOME (SUC n) /\
1967 ltree_lookup t (SNOC n p) = SOME t0 ==>
1968 ltree_insert' (ltree_delete' t p) p t0 = t
1969Proof
1970 rpt STRIP_TAC
1971 >> MATCH_MP_TAC ltree_insert_delete >> simp []
1972 >> Know ‘p IN ltree_paths t’
1973 >- (MATCH_MP_TAC ltree_paths_inclusive \\
1974 Q.EXISTS_TAC ‘SNOC n p’ \\
1975 simp [isPREFIX_SNOC, ltree_paths_def])
1976 >> rw [ltree_paths_alt_ltree_el, GSYM IS_SOME_EQ_NOT_NONE, IS_SOME_EXISTS]
1977 >> rename1 ‘ltree_el t p = SOME y’
1978 >> Cases_on ‘y’
1979 >> qexistsl_tac [‘q’, ‘r’] >> rw []
1980QED
1981
1982(*---------------------------------------------------------------------------*
1983 * ltree_finite and (finite) ltree_paths
1984 *---------------------------------------------------------------------------*)
1985
1986Theorem ltree_finite_imp_finite_ltree_paths :
1987 !t. ltree_finite t ==> FINITE (ltree_paths t)
1988Proof
1989 HO_MATCH_MP_TAC ltree_finite_ind
1990 >> rw [ltree_paths_alt_ltree_el, EVERY_EL]
1991 >> qabbrev_tac ‘k = LENGTH ts’
1992 >> Know ‘{p | ltree_el (Branch a (fromList ts)) p <> NONE} =
1993 [] INSERT
1994 BIGUNION (IMAGE (\i. {i::q | q | ltree_el (EL i ts) q <> NONE})
1995 (count k))’
1996 >- (rw [Once EXTENSION, IN_BIGUNION_IMAGE] \\
1997 Cases_on ‘x’ >> simp [ltree_el_def, LNTH_fromList] \\
1998 Cases_on ‘h < k’ >> rw [])
1999 >> Rewr'
2000 >> REWRITE_TAC [FINITE_INSERT]
2001 >> MATCH_MP_TAC FINITE_BIGUNION
2002 >> CONJ_TAC >- (MATCH_MP_TAC IMAGE_FINITE >> rw [FINITE_COUNT])
2003 >> rw []
2004 >> Know ‘{i::q | q | ltree_el (EL i ts) q <> NONE} =
2005 IMAGE (\q. i::q) {q | q | ltree_el (EL i ts) q <> NONE}’
2006 >- rw [Once EXTENSION]
2007 >> Rewr'
2008 >> MATCH_MP_TAC IMAGE_FINITE
2009 >> FIRST_X_ASSUM MATCH_MP_TAC >> art []
2010QED
2011
2012Theorem finite_ltree_paths_imp_ltree_finite_lemma[local] :
2013 !n s t. s HAS_SIZE n /\ ltree_paths t = s ==> ltree_finite t
2014Proof
2015 Induct_on ‘n’ >> rw [HAS_SIZE]
2016 >- (‘ltree_paths t = {}’ by PROVE_TAC [CARD_EQ_0] \\
2017 ‘[] IN ltree_paths t’ by PROVE_TAC [NIL_IN_ltree_paths] \\
2018 ASM_SET_TAC [])
2019 >> qabbrev_tac ‘s = ltree_paths t’
2020 >> Know ‘s <> {}’
2021 >- (rw [Abbr ‘s’, GSYM MEMBER_NOT_EMPTY] \\
2022 Q.EXISTS_TAC ‘[]’ >> rw [NIL_IN_ltree_paths])
2023 >> DISCH_TAC
2024 >> qabbrev_tac ‘R = SHORTLEX ($< :num -> num -> bool)’
2025 (* applying finite_acyclic_has_maximal *)
2026 >> qabbrev_tac ‘r = rel_to_reln R’
2027 >> Know ‘?x. x IN maximal_elements s r’
2028 >- (irule finite_acyclic_has_maximal >> art [] \\
2029 MATCH_MP_TAC WF_acyclic >> rw [Abbr ‘r’] \\
2030 rw [Abbr ‘R’, WF_SHORTLEX])
2031 >> rw [maximal_elements_def, Abbr ‘r’, in_rel_to_reln]
2032 >> Cases_on ‘x = []’
2033 >- (fs [Abbr ‘R’] \\
2034 Know ‘!x. x IN s ==> x = []’
2035 >- (Q.X_GEN_TAC ‘z’ >> Cases_on ‘z’ >> rw [] \\
2036 rename1 ‘h::tl NOTIN s’ \\
2037 Q.PAT_X_ASSUM ‘!x. x IN s /\ _ ==> x = []’ (MP_TAC o Q.SPEC ‘h::tl’) \\
2038 simp []) >> DISCH_TAC \\
2039 Know ‘s = {[]}’
2040 >- (rw [Once EXTENSION] >> EQ_TAC >> rw []) >> DISCH_TAC \\
2041 fs [Abbr ‘s’] \\
2042 Q.PAT_X_ASSUM ‘!t. P’ K_TAC \\
2043 Cases_on ‘t’ >> gs [ltree_paths_alt_ltree_el, Once EXTENSION] \\
2044 Suff ‘ts = LNIL’ >- simp [ltree_finite] \\
2045 CCONTR_TAC >> Cases_on ‘ts’ >> gs [] \\
2046 POP_ASSUM (MP_TAC o Q.SPEC ‘[0]’) >> rw [ltree_el])
2047 >> qabbrev_tac ‘s' = s DELETE x’
2048 >> ‘s' HAS_SIZE n’ by rw [Abbr ‘s'’, HAS_SIZE]
2049 >> qabbrev_tac ‘p = FRONT x’
2050 >> qabbrev_tac ‘i = LAST x’
2051 >> qabbrev_tac ‘t' = ltree_delete' t p’
2052 >> Know ‘ltree_lookup t x <> NONE’
2053 >- (Q.PAT_X_ASSUM ‘x IN s’ MP_TAC \\
2054 simp [Abbr ‘s’, ltree_paths_def])
2055 >> DISCH_TAC
2056 >> qabbrev_tac ‘t0 = THE (ltree_lookup t x)’
2057 (* stage work *)
2058 >> Know ‘ltree_children t0 = LNIL’
2059 >- (CCONTR_TAC \\
2060 Cases_on ‘t0’ >> fs [] \\
2061 Cases_on ‘ts’ >> gs [] \\
2062 Know ‘SNOC 0 x IN s’
2063 >- (simp [Abbr ‘s’, ltree_paths_def] \\
2064 simp [ltree_lookup_SNOC, ltree_lookup_def]) >> DISCH_TAC \\
2065 Q.PAT_X_ASSUM ‘!y. y IN s /\ R x y ==> x = y’ (MP_TAC o Q.SPEC ‘SNOC 0 x’) \\
2066 simp [Abbr ‘R’] \\
2067 MATCH_MP_TAC LENGTH_LT_SHORTLEX >> simp [])
2068 >> DISCH_TAC
2069 >> Cases_on ‘t0’ >> gs []
2070 >> POP_ASSUM K_TAC
2071 >> qabbrev_tac ‘t0 = Branch a LNIL’
2072 >> Know ‘ltree_paths t0 = {[]}’
2073 >- (rw [Abbr ‘t0’, ltree_paths_def] \\
2074 simp [Once EXTENSION] \\
2075 Q.X_GEN_TAC ‘y’ \\
2076 reverse EQ_TAC >- rw [ltree_lookup_def] \\
2077 Cases_on ‘y’ >> simp [] \\
2078 rw [ltree_lookup_def])
2079 >> DISCH_TAC
2080 >> ‘SNOC i p = x’ by ASM_SIMP_TAC std_ss [Abbr ‘p’, Abbr ‘i’, SNOC_LAST_FRONT]
2081 (* calculate “ltree_el t p” *)
2082 >> MP_TAC (Q.SPECL [‘t’, ‘i’, ‘p’] ltree_lookup_SNOC) >> simp []
2083 >> Know ‘p IN ltree_paths t’
2084 >- (MATCH_MP_TAC ltree_paths_inclusive \\
2085 Q.EXISTS_TAC ‘x’ \\
2086 reverse CONJ_TAC >- rw [ltree_paths_def] \\
2087 Q.PAT_X_ASSUM ‘SNOC i p = x’ (REWRITE_TAC o wrap o SYM) \\
2088 rw [isPREFIX_SNOC])
2089 >> REWRITE_TAC [ltree_paths_def] >> simp [] >> DISCH_TAC
2090 >> Cases_on ‘ltree_lookup t p’ >> FULL_SIMP_TAC std_ss []
2091 >> rename1 ‘ltree_lookup t p = SOME t1’
2092 >> Cases_on ‘t1’
2093 >> simp [ltree_lookup_def]
2094 >> Cases_on ‘LNTH i ts’ >> simp []
2095 >> DISCH_THEN (FULL_SIMP_TAC std_ss o wrap o SYM)
2096 >> MP_TAC (Q.SPECL [‘p’, ‘t’] ltree_el_alt_ltree_lookup)
2097 >> REWRITE_TAC [ltree_paths_def] >> simp [] >> DISCH_TAC
2098 >> Cases_on ‘LLENGTH ts’ >> simp []
2099 >- (MP_TAC (Q.SPECL [‘t’, ‘SUC i’, ‘p’] ltree_lookup_SNOC) \\
2100 simp [ltree_lookup_def] \\
2101 Know ‘~LFINITE ts’ >- rw [LFINITE_LLENGTH] \\
2102 simp [infinite_lnth_some] >> STRIP_TAC \\
2103 POP_ASSUM (MP_TAC o Q.SPEC ‘SUC i’) >> STRIP_TAC \\
2104 POP_ORW >> simp [] >> DISCH_TAC \\
2105 Q.PAT_X_ASSUM ‘!y. y IN s /\ R x y ==> P’
2106 (MP_TAC o Q.SPEC ‘SNOC (SUC i) p’) \\
2107 simp [Abbr ‘s’, ltree_paths_def] \\
2108 rw [Abbr ‘R’] \\
2109 Suff ‘SHORTLEX $< (SNOC i p) (SNOC (SUC i) p)’ >- rw [] \\
2110 MATCH_MP_TAC SHORTLEX_SNOC >> simp [])
2111 >> rename1 ‘LLENGTH ts = SOME N’
2112 >> Know ‘N = SUC i’
2113 >- (MATCH_MP_TAC LESS_EQUAL_ANTISYM \\
2114 reverse CONJ_TAC
2115 >- (‘LFINITE ts’ by rw [LFINITE_LLENGTH] \\
2116 Know ‘IS_SOME (LNTH i ts)’ >- rw [IS_SOME_EQ_NOT_NONE] \\
2117 rw [LFINITE_LNTH_IS_SOME]) \\
2118 CCONTR_TAC \\
2119 ‘SUC i < N’ by rw [] \\
2120 MP_TAC (Q.SPECL [‘t’, ‘SUC i’, ‘p’] ltree_lookup_SNOC) \\
2121 simp [ltree_lookup_def] \\
2122 ‘LFINITE ts’ by rw [LFINITE_LLENGTH] \\
2123 Know ‘IS_SOME (LNTH (SUC i) ts)’ >- rw [LFINITE_LNTH_IS_SOME] \\
2124 rw [IS_SOME_EXISTS] \\
2125 POP_ORW >> simp [] \\
2126 CCONTR_TAC >> fs [] \\
2127 Q.PAT_X_ASSUM ‘!y. y IN s /\ R (SNOC i p) y ==> P’
2128 (MP_TAC o Q.SPEC ‘SNOC (SUC i) p’) \\
2129 simp [Abbr ‘s’, ltree_paths_def] \\
2130 qunabbrev_tac ‘R’ \\
2131 MATCH_MP_TAC SHORTLEX_SNOC >> simp [])
2132 >> DISCH_THEN (FULL_SIMP_TAC std_ss o wrap)
2133 >> Cases_on ‘ltree_lookup t x’ >> FULL_SIMP_TAC std_ss []
2134 >> rename1 ‘ltree_lookup t x = SOME t1’
2135 >> rpt (Q.PAT_X_ASSUM ‘T’ K_TAC)
2136 (* applying ltree_delete_paths *)
2137 >> MP_TAC (Q.SPECL [‘I’, ‘p’, ‘t’, ‘a'’, ‘i’] ltree_delete_paths_lemma)
2138 >> simp []
2139 >> DISCH_TAC
2140 >> Q.PAT_X_ASSUM ‘!t. ltree_paths t HAS_SIZE n ==> ltree_finite t’
2141 (MP_TAC o Q.SPEC ‘t'’)
2142 >> impl_tac
2143 >- (simp [HAS_SIZE, CARD_DIFF] \\
2144 ‘s INTER {x} = {x}’ by ASM_SET_TAC [] >> POP_ORW \\
2145 simp [])
2146 >> DISCH_TAC (* ltree_finite t' *)
2147 (* applying ltree_insert_delete' *)
2148 >> Know ‘t = ltree_insert' t' p t0’
2149 >- (simp [Abbr ‘t'’, Once EQ_SYM_EQ] \\
2150 MATCH_MP_TAC ltree_insert_delete' \\
2151 Q.EXISTS_TAC ‘i’ >> simp [] \\
2152 simp [ltree_branching_def])
2153 >> Rewr'
2154 (* final goal: ltree_finite t' ==> ltree_finite (ltree_insert' t' p t0) *)
2155 >> ‘ltree_finite t0’ by simp [ltree_finite, Abbr ‘t0’]
2156 >> irule ltree_finite_ltree_insert_lemma >> art []
2157 >> qexistsl_tac [‘a'’, ‘SOME i’]
2158 >> qunabbrev_tac ‘t'’
2159 >> MATCH_MP_TAC ltree_el_ltree_delete' >> art []
2160QED
2161
2162Theorem finite_ltree_paths_imp_ltree_finite[local] :
2163 !t. FINITE (ltree_paths t) ==> ltree_finite t
2164Proof
2165 rpt STRIP_TAC
2166 >> irule finite_ltree_paths_imp_ltree_finite_lemma
2167 >> qabbrev_tac ‘s = ltree_paths t’
2168 >> qexistsl_tac [‘CARD s’, ‘s’]
2169 >> rw [HAS_SIZE]
2170QED
2171
2172Theorem ltree_finite_alt_ltree_paths :
2173 !t. ltree_finite t <=> FINITE (ltree_paths t)
2174Proof
2175 METIS_TAC [ltree_finite_imp_finite_ltree_paths,
2176 finite_ltree_paths_imp_ltree_finite]
2177QED
2178
2179(*---------------------------------------------------------------------------*
2180 * Rose tree is a finite variant of ltree, defined inductively.
2181 *---------------------------------------------------------------------------*)
2182
2183Datatype:
2184 rose_tree = Rose 'a (rose_tree list)
2185End
2186
2187Definition rose_node_def[simp] :
2188 rose_node (Rose a ts) = a
2189End
2190
2191Definition rose_children_def[simp] :
2192 rose_children (Rose a ts) = ts
2193End
2194
2195Definition from_rose_def:
2196 from_rose (Rose a ts) = Branch a (fromList (MAP from_rose ts))
2197End
2198
2199Theorem from_rose_def[allow_rebind] :
2200 !ts a. from_rose (Rose a ts) = Branch a (fromList (MAP from_rose ts))
2201Proof
2202 rw [from_rose_def, LIST_EQ_REWRITE, EL_MAP]
2203QED
2204
2205Theorem from_rose :
2206 !t. from_rose t =
2207 Branch (rose_node t) (fromList (MAP from_rose (rose_children t)))
2208Proof
2209 rpt GEN_TAC
2210 >> Cases_on ‘t’
2211 >> simp [Once from_rose_def]
2212QED
2213
2214Theorem rose_tree_induction[allow_rebind] = from_rose_ind;
2215
2216Theorem from_rose_11 :
2217 !r1 r2. from_rose r1 = from_rose r2 <=> r1 = r2
2218Proof
2219 rpt GEN_TAC
2220 >> reverse EQ_TAC >- simp []
2221 >> qid_spec_tac ‘r2’
2222 >> qid_spec_tac ‘r1’
2223 >> HO_MATCH_MP_TAC rose_tree_induction
2224 >> rpt STRIP_TAC
2225 >> Cases_on ‘r2’
2226 >> fs [from_rose_def]
2227 >> POP_ASSUM MP_TAC
2228 >> rw [LIST_EQ_REWRITE, EL_MAP]
2229 >> rename1 ‘n < LENGTH l’
2230 >> Q.PAT_X_ASSUM ‘!r1. MEM r1 ts ==> P’ (MP_TAC o Q.SPEC ‘EL n ts’)
2231 >> rw [EL_MEM, EL_MAP]
2232QED
2233
2234Theorem ltree_finite_from_rose:
2235 ltree_finite t <=> ?r. from_rose r = t
2236Proof
2237 eq_tac \\ qid_spec_tac `t` THEN1
2238 (ho_match_mp_tac ltree_finite_ind \\ fs [EVERY_MEM] \\ rw []
2239 \\ qsuff_tac `?rs. ts = MAP from_rose rs` THEN1
2240 (strip_tac \\ qexists_tac `Rose a rs` \\ fs [from_rose_def]
2241 \\ CONV_TAC (DEPTH_CONV ETA_CONV) \\ fs [])
2242 \\ Induct_on `ts` \\ fs [] \\ rw []
2243 \\ first_assum (qspec_then `h` assume_tac) \\ fs []
2244 \\ qexists_tac `r::rs` \\ fs [])
2245 \\ fs [PULL_EXISTS]
2246 \\ ho_match_mp_tac from_rose_ind \\ rw []
2247 \\ once_rewrite_tac [ltree_finite_cases]
2248 \\ fs [from_rose_def,Branch_11]
2249 \\ CONV_TAC (DEPTH_CONV ETA_CONV)
2250 \\ fs [EVERY_MEM,MEM_MAP,PULL_EXISTS]
2251QED
2252
2253(* The previous theorem induces a new constant “to_rose” for finite ltrees *)
2254local
2255 val thm = Q.prove (‘!t. ltree_finite t ==> ?r. from_rose r = t’,
2256 METIS_TAC [ltree_finite_from_rose]);
2257in
2258 (* |- !t. ltree_finite t ==> from_rose (to_rose t) = t *)
2259 val to_rose_def = new_specification
2260 ("to_rose_def", ["to_rose"],
2261 SIMP_RULE bool_ss [GSYM RIGHT_EXISTS_IMP_THM, SKOLEM_THM] thm);
2262end;
2263
2264Theorem to_rose_thm :
2265 !r. to_rose (from_rose r) = r
2266Proof
2267 Q.X_GEN_TAC ‘r’
2268 >> qabbrev_tac ‘t = from_rose r’
2269 >> ‘ltree_finite t’ by METIS_TAC [ltree_finite_from_rose]
2270 >> rw [GSYM from_rose_11, to_rose_def]
2271QED
2272
2273Theorem rose_node_to_rose :
2274 !t. ltree_finite t ==> rose_node (to_rose t) = ltree_node t
2275Proof
2276 rw [ltree_finite_from_rose]
2277 >> rw [to_rose_thm]
2278 >> Cases_on ‘r’
2279 >> rw [rose_node_def, from_rose_def, ltree_node_def]
2280QED
2281
2282Theorem rose_children_to_rose :
2283 !t. ltree_finite t ==>
2284 rose_children (to_rose t) = MAP to_rose (THE (toList (ltree_children t)))
2285Proof
2286 rw [ltree_finite_from_rose]
2287 >> rw [to_rose_thm]
2288 >> Cases_on ‘r’
2289 >> rw [rose_node_def, from_rose_def, ltree_node_def]
2290 >> simp [from_toList, MAP_MAP_o]
2291 >> simp [o_DEF, to_rose_thm]
2292QED
2293
2294Theorem rose_children_to_rose' :
2295 !t. ltree_finite t ==>
2296 rose_children (to_rose t) = THE (toList (LMAP to_rose (ltree_children t)))
2297Proof
2298 rpt STRIP_TAC
2299 >> ‘finite_branching t’ by PROVE_TAC [ltree_finite_imp_finite_branching]
2300 >> Suff ‘LFINITE (ltree_children t)’
2301 >- (DISCH_TAC >> simp [GSYM MAP_toList] \\
2302 MATCH_MP_TAC rose_children_to_rose >> art [])
2303 >> Suff ‘finite_branching (Branch (ltree_node t) (ltree_children t))’ >- rw []
2304 >> ASM_REWRITE_TAC [ltree_node_children_reduce]
2305QED
2306
2307(* This is a general recursive reduction function for rose trees. The type of
2308 f is “:'a -> 'b list -> 'b”, where 'b is the type of reductions of trees.
2309
2310 See examples/lambda/barendregt/lameta_complateTheory.rose_to_term_def for
2311 an application.
2312 *)
2313Definition rose_reduce_def :
2314 rose_reduce f ((Rose a ts) :'a rose_tree) = f a (MAP (rose_reduce f) ts)
2315End
2316
2317Theorem rose_reduce_def[allow_rebind] :
2318 !f a ts. rose_reduce f (Rose a ts) = f a (MAP (rose_reduce f) ts)
2319Proof
2320 rw [rose_reduce_def]
2321 >> AP_TERM_TAC
2322 >> rw [LIST_EQ_REWRITE, EL_MAP]
2323QED
2324
2325Theorem rose_reduce :
2326 !f t. rose_reduce f t = f (rose_node t) (MAP (rose_reduce f) (rose_children t))
2327Proof
2328 rpt GEN_TAC
2329 >> Cases_on ‘t’
2330 >> simp [Once rose_reduce_def]
2331QED
2332
2333(*---------------------------------------------------------------------------*
2334 * index function of ltree paths
2335 *---------------------------------------------------------------------------*)
2336
2337Overload ltree_path_lt = “SHORTLEX ($< :num -> num -> bool)”
2338
2339Theorem ltree_path_lt =
2340 SHORTLEX_THM |> Q.GEN ‘R’ |> ISPEC “($< :num -> num -> bool)”
2341
2342(* The first two properties are required by TOPOLOGICAL_SORT' *)
2343Theorem ltree_path_lt_transitive :
2344 transitive ltree_path_lt
2345Proof
2346 rw [SHORTLEX_transitive]
2347QED
2348
2349Theorem ltree_path_lt_antisymmetric :
2350 antisymmetric ltree_path_lt
2351Proof
2352 MATCH_MP_TAC SHORTLEX_antisymmetric
2353 >> rw [relationTheory.irreflexive_def,
2354 relationTheory.antisymmetric_def]
2355QED
2356
2357Theorem ltree_path_lt_irreflexive :
2358 irreflexive ltree_path_lt
2359Proof
2360 MATCH_MP_TAC SHORTLEX_irreflexive
2361 >> rw [relationTheory.irreflexive_def]
2362QED
2363
2364(* “path_index” sorts the ltree paths set and index it from smaller elements *)
2365Theorem path_index_exists[local] :
2366 !s. FINITE s ==>
2367 ?f. s = IMAGE f (count (CARD s)) /\
2368 !j k. j < CARD s /\ k < CARD s /\ j < k ==> ~ltree_path_lt (f k) (f j)
2369Proof
2370 rpt STRIP_TAC
2371 >> MATCH_MP_TAC TOPOLOGICAL_SORT'
2372 >> rw [HAS_SIZE, ltree_path_lt_transitive, ltree_path_lt_antisymmetric]
2373QED
2374
2375(* |- !s. FINITE s ==>
2376 s = IMAGE (path_index s) (count (CARD s)) /\
2377 !j k.
2378 j < CARD s /\ k < CARD s /\ j < k ==>
2379 ~ltree_path_lt (path_index s k) (path_index s j)
2380 *)
2381val path_index_def = new_specification
2382 ("path_index_def", ["path_index"],
2383 SIMP_RULE std_ss [GSYM RIGHT_EXISTS_IMP_THM, SKOLEM_THM] path_index_exists);
2384
2385Theorem path_index_in_paths :
2386 !s i. FINITE s /\ i < CARD s ==> path_index s i IN s
2387Proof
2388 rpt STRIP_TAC
2389 >> drule path_index_def >> rw []
2390 >> Suff ‘path_index s i IN IMAGE (path_index s) (count (CARD s))’
2391 >- (Q.PAT_X_ASSUM ‘s = _’ (REWRITE_TAC o wrap o SYM))
2392 >> rw []
2393 >> Q.EXISTS_TAC ‘i’ >> simp []
2394QED
2395
2396Overload ltree_path_le = “RC ltree_path_lt”
2397
2398Theorem ltree_path_le_total :
2399 total ltree_path_le
2400Proof
2401 MATCH_MP_TAC SHORTLEX_total
2402 >> rw [total_def, RC_DEF]
2403QED
2404
2405(* NOTE: A more complete picture of ‘path_index’. Now SHORTLEX_total is involved
2406 in addition to transitive and antisymmetric.
2407 *)
2408Theorem path_index_thm :
2409 !s n. s HAS_SIZE n ==>
2410 BIJ (path_index s) (count n) s /\
2411 !j k. j < n /\ k < n ==>
2412 (ltree_path_lt (path_index s j) (path_index s k) <=> j < k)
2413Proof
2414 rpt GEN_TAC >> simp [HAS_SIZE]
2415 >> STRIP_TAC
2416 >> MP_TAC (Q.SPEC ‘s’ path_index_def) >> simp []
2417 >> STRIP_TAC
2418 >> STRONG_CONJ_TAC (* BIJ *)
2419 >- (rw [BIJ_ALT, IN_FUNSET, path_index_in_paths] \\
2420 rw [EXISTS_UNIQUE_ALT] \\
2421 qabbrev_tac ‘n = CARD s’ \\
2422 Know ‘y IN IMAGE (path_index s) (count n)’ >- METIS_TAC [] \\
2423 rw [IN_IMAGE] \\
2424 Q.PAT_X_ASSUM ‘s = IMAGE _ _’ (ASSUME_TAC o SYM) \\
2425 Q.EXISTS_TAC ‘x’ >> art [] \\
2426 Q.X_GEN_TAC ‘y’ \\
2427 reverse EQ_TAC >- rw [] \\
2428 rpt STRIP_TAC \\
2429 CCONTR_TAC \\
2430 (* In this case, we found at least one duplicated index (x or y), thus
2431 it should be CARD s < n, conflicting with CARD = n.
2432 *)
2433 Know ‘s = IMAGE (path_index s) (count n DELETE y)’
2434 >- (Q.PAT_X_ASSUM ‘_ = s’ (fn th => REWRITE_TAC [Once (SYM th)]) \\
2435 rw [Once EXTENSION] \\
2436 EQ_TAC >> rw [] >| (* 2 subgoals *)
2437 [ (* goal 1 (of 2) *)
2438 rename1 ‘i < n’ \\
2439 Cases_on ‘i = y’ >- (Q.EXISTS_TAC ‘x’ >> art []) \\
2440 Q.EXISTS_TAC ‘i’ >> art [],
2441 (* goal 2 (of 2) *)
2442 rename1 ‘i <> y’ \\
2443 Q.EXISTS_TAC ‘i’ >> art [] ]) \\
2444 DISCH_THEN (MP_TAC o AP_TERM “CARD :num list set -> num”) \\
2445 simp [] \\
2446 Suff ‘CARD (IMAGE (path_index s) (count n DELETE y)) < n’ >- rw [] \\
2447 MATCH_MP_TAC LESS_EQ_LESS_TRANS \\
2448 Q.EXISTS_TAC ‘CARD (count n DELETE y)’ >> simp [CARD_IMAGE])
2449 >> rw [BIJ_DEF, INJ_DEF]
2450 >> qabbrev_tac ‘n = CARD s’
2451 (* applying ltree_path_le_total *)
2452 >> MP_TAC ltree_path_le_total
2453 >> simp [total_def, RC_DEF]
2454 >> simp [Once EQ_SYM_EQ, GSYM DISJ_ASSOC]
2455 >> simp [TAUT ‘P \/ Q \/ P \/ R <=> Q \/ R \/ P’]
2456 >> STRIP_TAC
2457 >> reverse EQ_TAC
2458 >- (Q.PAT_X_ASSUM ‘!j k. j < n /\ k < n /\ j < k ==> _’
2459 (MP_TAC o Q.SPECL [‘j’, ‘k’]) >> rw [] \\
2460 ‘j <> k’ by rw [] \\
2461 METIS_TAC [])
2462 >> STRIP_TAC
2463 >> CCONTR_TAC
2464 >> fs [NOT_LESS]
2465 >> ‘k = j \/ k < j’ by rw []
2466 >- (ASSUME_TAC ltree_path_lt_irreflexive \\
2467 gs [relationTheory.irreflexive_def])
2468 >> Q.PAT_X_ASSUM ‘!j k. j < n /\ k < n /\ j < k ==> _’ (MP_TAC o Q.SPECL [‘k’, ‘j’])
2469 >> rw []
2470QED
2471
2472Definition parent_inclusive_def :
2473 parent_inclusive (s :num list set) <=>
2474 !p q. p IN s /\ q <<= p ==> q IN s
2475End
2476
2477Definition sibling_inclusive_def :
2478 sibling_inclusive (s :num list set) <=>
2479 !p q. p IN s /\ p <> [] /\ q <> [] /\
2480 FRONT q = FRONT p /\ LAST q < LAST p ==> q IN s
2481End
2482
2483Theorem parent_inclusive_ltree_paths :
2484 !t. parent_inclusive (ltree_paths t)
2485Proof
2486 rw [parent_inclusive_def]
2487 >> MATCH_MP_TAC ltree_paths_inclusive
2488 >> Q.EXISTS_TAC ‘p’ >> art []
2489QED
2490
2491Theorem parent_inclusive_union :
2492 !s1 s2. parent_inclusive s1 /\ parent_inclusive s2 ==>
2493 parent_inclusive (s1 UNION s2)
2494Proof
2495 rw [parent_inclusive_def, IN_UNION]
2496 >| [ (* goal 1 (of 2) *)
2497 DISJ1_TAC \\
2498 FIRST_X_ASSUM MATCH_MP_TAC \\
2499 Q.EXISTS_TAC ‘p’ >> art [],
2500 (* goal 2 (of 2) *)
2501 DISJ2_TAC \\
2502 FIRST_X_ASSUM MATCH_MP_TAC \\
2503 Q.EXISTS_TAC ‘p’ >> art [] ]
2504QED
2505
2506Theorem sibling_inclusive_ltree_paths_lemma[local] :
2507 !p t. p IN ltree_paths t /\ p <> [] ==>
2508 !q. q <> [] /\ FRONT q = FRONT p /\ LAST q < LAST p ==>
2509 q IN ltree_paths t
2510Proof
2511 rpt STRIP_TAC
2512 >> qabbrev_tac ‘xs = FRONT p’
2513 >> qabbrev_tac ‘x = LAST p’
2514 >> ‘p = SNOC x xs’ by METIS_TAC [SNOC_LAST_FRONT]
2515 >> ‘xs <<= p’ by METIS_TAC [isPREFIX_SNOC]
2516 >> Know ‘xs IN ltree_paths t’
2517 >- (MATCH_MP_TAC ltree_paths_inclusive \\
2518 Q.EXISTS_TAC ‘p’ >> art [])
2519 >> DISCH_TAC
2520 >> Q.PAT_X_ASSUM ‘p IN ltree_paths t’ MP_TAC
2521 >> Q.PAT_X_ASSUM ‘p = SNOC x xs’ (REWRITE_TAC o wrap)
2522 >> qabbrev_tac ‘y = LAST q’
2523 >> ‘q = SNOC y xs’ by METIS_TAC [SNOC_LAST_FRONT]
2524 >> POP_ORW
2525 >> fs [ltree_paths_def]
2526 >> simp [ltree_lookup_SNOC]
2527 >> Q.PAT_X_ASSUM ‘ltree_lookup t xs <> NONE’
2528 (MP_TAC o REWRITE_RULE [GSYM IS_SOME_EQ_NOT_NONE])
2529 >> simp [IS_SOME_EXISTS]
2530 >> DISCH_THEN (Q.X_CHOOSE_THEN ‘t0’ STRIP_ASSUME_TAC)
2531 >> simp []
2532 >> Cases_on ‘t0’
2533 >> simp [ltree_lookup_def]
2534 >> Cases_on ‘LNTH x ts’ >> simp []
2535 >> Know ‘IS_SOME (LNTH y ts)’
2536 >- (MATCH_MP_TAC LNTH_IS_SOME_MONO \\
2537 Q.EXISTS_TAC ‘x’ >> rw [IS_SOME_EXISTS])
2538 >> rw [IS_SOME_EXISTS]
2539 >> simp []
2540QED
2541
2542Theorem sibling_inclusive_ltree_paths :
2543 !t. sibling_inclusive (ltree_paths t)
2544Proof
2545 rw [sibling_inclusive_def]
2546 >> irule sibling_inclusive_ltree_paths_lemma >> art []
2547 >> Q.EXISTS_TAC ‘p’ >> art []
2548QED
2549
2550Theorem sibling_inclusive_union :
2551 !s1 s2. sibling_inclusive s1 /\ sibling_inclusive s2 ==>
2552 sibling_inclusive (s1 UNION s2)
2553Proof
2554 rw [sibling_inclusive_def, IN_UNION]
2555 >| [ (* goal 1 (of 2) *)
2556 DISJ1_TAC \\
2557 FIRST_X_ASSUM MATCH_MP_TAC \\
2558 Q.EXISTS_TAC ‘p’ >> art [],
2559 (* goal 2 (of 2) *)
2560 DISJ2_TAC \\
2561 FIRST_X_ASSUM MATCH_MP_TAC \\
2562 Q.EXISTS_TAC ‘p’ >> art [] ]
2563QED
2564
2565Theorem ltree_path_lt_sibling :
2566 !p q. p <> [] /\ q <> [] /\ FRONT p = FRONT q /\ LAST p < LAST q ==>
2567 ltree_path_lt p q
2568Proof
2569 Induct_on ‘p’ >> rw []
2570 >> Cases_on ‘q’ >> gs []
2571 >> Know ‘LENGTH p = LENGTH t’
2572 >- (Q.PAT_X_ASSUM ‘FRONT (h::p) = FRONT (h'::t)’
2573 (MP_TAC o AP_TERM “LENGTH :num list -> num”) \\
2574 simp [])
2575 >> rw []
2576 >> Know ‘h <= h'’
2577 >- (Cases_on ‘p’ >> gs [] \\
2578 Cases_on ‘t’ >> gs [])
2579 >> DISCH_TAC
2580 >> ‘h < h' \/ h = h'’ by rw []
2581 >> simp []
2582 >> Cases_on ‘p = []’ >> gs []
2583 >> Cases_on ‘t = []’ >> gs []
2584 >> FIRST_X_ASSUM MATCH_MP_TAC
2585 >> Cases_on ‘p’ >> gs []
2586 >> Cases_on ‘t’ >> gs []
2587QED
2588
2589Theorem ltree_path_lt_sibling' :
2590 !x y xs. x < y ==> ltree_path_lt (SNOC x xs) (SNOC y xs)
2591Proof
2592 rpt STRIP_TAC
2593 >> MATCH_MP_TAC ltree_path_lt_sibling
2594 >> rw [FRONT_SNOC, LAST_SNOC]
2595QED
2596
2597Theorem finite_branching_ltree_el_cases :
2598 !p t. finite_branching t /\ p IN ltree_paths t ==>
2599 ?d m. ltree_el t p = SOME (d,SOME m)
2600Proof
2601 Induct_on ‘p’
2602 >- (Q.X_GEN_TAC ‘t’ >> Cases_on ‘t’ \\
2603 rw [ltree_el_def, ltree_paths_alt_ltree_el] \\
2604 fs [LFINITE_LLENGTH])
2605 >> rw [ltree_paths_alt_ltree_el]
2606 >> Cases_on ‘t’ >> fs [ltree_el_def]
2607 >> Cases_on ‘LNTH h ts’ >> fs []
2608 >> FIRST_X_ASSUM MATCH_MP_TAC
2609 >> simp [ltree_paths_alt_ltree_el]
2610 >> fs [every_LNTH]
2611 >> FIRST_X_ASSUM MATCH_MP_TAC
2612 >> Q.EXISTS_TAC ‘h’ >> art []
2613QED
2614
2615(* tidy up theory exports *)
2616
2617val _ = List.app Theory.delete_binding
2618 ["Branch_rep_def", "dest_Branch_rep_def", "make_ltree_rep_def",
2619 "make_unfold_def", "path_ok_def", "ltree_absrep", "ltree_absrep",
2620 "gen_ltree_def", "ltree_rep_ok_def", "Branch",
2621 "from_rose_def_primitive", "ltree_finite_def"];
2622