cv_string_fmapScript.sml
1(*
2 Set up cv translator for string |-> 'a
3*)
4Theory cv_string_fmap
5Ancestors
6 cv cv_type arithmetic words cv_rep cv_prim pair list option sum
7 alist indexedLists rich_list sptree finite_set sorting cv_std
8Libs
9 dep_rewrite cv_typeLib cv_repLib cv_transLib
10
11Overload Num[local] = “cv$Num”
12Overload Pair[local] = “cv$Pair”
13
14(*----------------------------------------------------------*
15 string trie
16 *----------------------------------------------------------*)
17
18Datatype:
19 str_trie = Nothing
20 | Just 'a
21 | Branch char str_trie str_trie
22End
23
24val _ = (cv_memLib.use_long_names := false);
25val from_to_str_trie = cv_typeLib.from_to_thm_for “:'a str_trie”;
26val _ = (cv_memLib.use_long_names := true);
27
28Definition st_get_nil_def[simp]:
29 st_get_nil (Branch _ _ rest) = st_get_nil rest ∧
30 st_get_nil (Just x) = SOME x ∧
31 st_get_nil Nothing = NONE
32End
33
34Definition st_get_def:
35 st_get t [] = st_get_nil t ∧
36 st_get t (x::xs) = st_get_cons t x xs ∧
37 st_get_cons Nothing x xs = NONE ∧
38 st_get_cons (Just _) x xs = NONE ∧
39 st_get_cons (Branch c subtrie rest) x xs =
40 if c > x then NONE else
41 if c < x then st_get_cons rest x xs else
42 st_get subtrie xs
43End
44
45Definition st_make_def[simp]:
46 st_make [] y = Just y ∧
47 st_make (x::xs) y = Branch x (st_make xs y) Nothing
48End
49
50Definition st_set_nil_def[simp]:
51 st_set_nil (Branch c t rest) y = Branch c t (st_set_nil rest y) ∧
52 st_set_nil _ y = Just y
53End
54
55Definition st_set_cons_def:
56 st_set_cons Nothing x xs y = Branch x (st_make xs y) Nothing ∧
57 st_set_cons (Just z) x xs y = Branch x (st_make xs y) (Just z) ∧
58 st_set_cons (Branch c subtrie rest) x xs y =
59 if c > x then
60 Branch x (st_make xs y) (Branch c subtrie rest)
61 else if c < x then
62 Branch c subtrie (st_set_cons rest x xs y)
63 else
64 Branch c (case xs of
65 | [] => st_set_nil subtrie y
66 | (x::xs) => st_set_cons subtrie x xs y) rest
67End
68
69Definition st_set_def[simp]:
70 st_set t [] y = st_set_nil t y ∧
71 st_set t (x::xs) y = st_set_cons t x xs y
72End
73
74Definition st_sets_def[simp]:
75 st_sets t [] = t ∧
76 st_sets t ((s,a)::rest) = st_set (st_sets t rest) s a
77End
78
79Definition st_del_nil_def[simp]:
80 st_del_nil (Branch x y rest) = Branch x y (st_del_nil rest) ∧
81 st_del_nil _ = Nothing
82End
83
84Definition mk_Branch_def:
85 mk_Branch c Nothing t2 = t2 ∧
86 mk_Branch c (Just x) t2 = Branch c (Just x) t2 ∧
87 mk_Branch c (Branch a b d) t2 = Branch c (Branch a b d) t2
88End
89
90Definition st_del_cons_def:
91 st_del_cons Nothing x xs = Nothing ∧
92 st_del_cons (Just z) x xs = Just z ∧
93 st_del_cons (Branch c subtrie rest) x xs =
94 if c > x then
95 Branch c subtrie rest
96 else if c < x then
97 Branch c subtrie (st_del_cons rest x xs)
98 else
99 mk_Branch c (case xs of
100 | [] => st_del_nil subtrie
101 | (x::xs) => st_del_cons subtrie x xs) rest
102End
103
104Definition st_del_def[simp]:
105 st_del t [] = st_del_nil t ∧
106 st_del t (x::xs) = st_del_cons t x xs
107End
108
109Definition st_union_def:
110 st_union Nothing t = t ∧
111 st_union t Nothing = t ∧
112 st_union (Just x) (Just y) = Just x ∧
113 st_union (Just x) (Branch c t1 t2) = Branch c t1 (st_union (Just x) t2) ∧
114 st_union (Branch c t1 t2) (Just x) = Branch c t1 (st_union t2 (Just x)) ∧
115 st_union (Branch c1 t1 t2) (Branch c2 u1 u2) =
116 if ORD c1 < ORD c2 then
117 Branch c1 t1 (st_union t2 (Branch c2 u1 u2))
118 else if ORD c2 < ORD c1 then
119 Branch c2 u1 (st_union (Branch c1 t1 t2) u2)
120 else
121 Branch c1 (st_union t1 u1) (st_union t2 u2)
122End
123
124Definition st_inter_def:
125 st_inter Nothing t = Nothing ∧
126 st_inter t Nothing = Nothing ∧
127 st_inter (Just x) (Just y) = Just x ∧
128 st_inter (Just x) (Branch c t1 t2) = st_inter (Just x) t2 ∧
129 st_inter (Branch c t1 t2) (Just x) = st_inter t2 (Just x) ∧
130 st_inter (Branch c1 t1 t2) (Branch c2 u1 u2) =
131 if ORD c1 < ORD c2 then
132 st_inter t2 (Branch c2 u1 u2)
133 else if ORD c2 < ORD c1 then
134 st_inter (Branch c1 t1 t2) u2
135 else
136 mk_Branch c1 (st_inter t1 u1) (st_inter t2 u2)
137End
138
139Definition st_minus_def:
140 st_minus Nothing t = Nothing ∧
141 st_minus t Nothing = t ∧
142 st_minus (Just x) (Just y) = Nothing ∧
143 st_minus (Just x) (Branch c t1 t2) = st_minus (Just x) t2 ∧
144 st_minus (Branch c t1 t2) (Just x) = Branch c t1 (st_minus t2 (Just x)) ∧
145 st_minus (Branch c1 t1 t2) (Branch c2 u1 u2) =
146 if ORD c1 < ORD c2 then
147 Branch c1 t1 (st_minus t2 (Branch c2 u1 u2))
148 else if ORD c2 < ORD c1 then
149 st_minus (Branch c1 t1 t2) u2
150 else
151 mk_Branch c1 (st_minus t1 u1) (st_minus t2 u2)
152End
153
154Definition st_card_def:
155 st_card Nothing = 0:num ∧
156 st_card (Just x) = 1 ∧
157 st_card (Branch c t1 t2) = st_card t1 + st_card t2
158End
159
160Definition st_submap_def:
161 st_submap Nothing u = T ∧
162 st_submap (Just x) Nothing = F ∧
163 st_submap (Branch c t1 t2) Nothing = F ∧
164 st_submap (Just x) (Just y) = (x = y) ∧
165 st_submap (Just x) (Branch c u1 u2) = st_submap (Just x) u2 ∧
166 st_submap (Branch c t1 t2) (Just y) = F ∧
167 st_submap (Branch c1 t1 t2) (Branch c2 u1 u2) =
168 if ORD c1 < ORD c2 then F
169 else if ORD c2 < ORD c1 then st_submap (Branch c1 t1 t2) u2
170 else st_submap t1 u1 ∧ st_submap t2 u2
171End
172
173Definition st_lex_def:
174 st_lex t = (case st_get_nil t of
175 | NONE => st_branches t
176 | SOME v => ("",v) :: st_branches t) ∧
177 st_branches Nothing = [] ∧
178 st_branches (Just x) = [] ∧
179 st_branches (Branch c t1 t2) =
180 MAP (λ(k,v). (STRING c k, v)) (st_lex t1) ++ st_branches t2
181Termination
182 WF_REL_TAC ‘measure (λx. case x of
183 | INL t => str_trie_size (K 0) t * 2 + 1
184 | INR t => str_trie_size (K 0) t * 2)’
185End
186
187Definition st_lex_acc_def:
188 st_lex_acc t rp acc =
189 (case st_get_nil t of
190 | NONE => st_branches_acc t rp acc
191 | SOME v => (REVERSE rp, v) :: st_branches_acc t rp acc) ∧
192 st_branches_acc Nothing rp acc = acc ∧
193 st_branches_acc (Just x) rp acc = acc ∧
194 st_branches_acc (Branch c t1 t2) rp acc =
195 st_lex_acc t1 (c::rp) (st_branches_acc t2 rp acc)
196Termination
197 WF_REL_TAC ‘measure (λx. case x of
198 | INL (t,rp,acc) => str_trie_size (K 0) t * 2 + 1
199 | INR (t,rp,acc) => str_trie_size (K 0) t * 2)’
200End
201
202Definition st_to_list_def:
203 st_to_list t = st_lex_acc t [] []
204End
205
206(* verification *)
207
208Definition st_flat_def:
209 st_flat Nothing = [] ∧
210 st_flat (Just a) = [("",a)] ∧
211 st_flat (Branch c t1 t2) = MAP (λ(k,v). (c::k,v)) (st_flat t1) ++ st_flat t2
212End
213
214Definition st_sorted_def:
215 st_sorted Nothing = T ∧
216 st_sorted (Just x) = T ∧
217 st_sorted (Branch c t1 t2) = (t1 ≠ Nothing ∧ st_sorted t1 ∧
218 st_sorted t2 ∧
219 ∀c' t1' t2'. t2 = Branch c' t1' t2' ⇒ c < c')
220End
221
222Theorem st_sorted_base[simp]:
223 st_sorted Nothing ∧ st_sorted (Just x)
224Proof
225 rw[st_sorted_def]
226QED
227
228Theorem st_make_not_nothing[simp]:
229 st_make xs y ≠ Nothing
230Proof
231 Cases_on`xs` \\ rw[]
232QED
233
234Theorem st_sorted_st_make[simp]:
235 ∀xs y. st_sorted (st_make xs y)
236Proof
237 Induct \\ rw[st_make_def, st_sorted_def]
238QED
239
240Theorem st_get_st_make:
241 ∀xs y n. st_get (st_make xs y) n = if n = xs then SOME y else NONE
242Proof
243 Induct \\ rw[st_get_def, st_make_def, st_get_nil_def,
244 stringTheory.char_lt_def, stringTheory.char_gt_def] >>
245 qmatch_goalsub_rename_tac`st_get _ ls` >>
246 Cases_on`ls` >> gvs[st_get_def, st_get_nil_def] >> rw[] >>
247 gvs[stringTheory.char_lt_def, stringTheory.char_gt_def] >>
248 qpat_x_assum`_ <> _`mp_tac \\ rw[] >>
249 irule $ iffLR stringTheory.ORD_11 >> simp[]
250QED
251
252Theorem st_get_Nothing[simp]:
253 ∀xs. st_get Nothing xs = NONE
254Proof
255 Cases \\ fs [st_get_def, st_get_nil_def]
256QED
257
258Theorem st_del_Nothing[simp]:
259 ∀xs. st_del Nothing xs = Nothing
260Proof
261 Cases \\ fs [st_del_def, st_del_nil_def, st_del_cons_def]
262QED
263
264Theorem st_sorted_st_set_nil[simp]:
265 ∀t y. st_sorted t ⇒ st_sorted (st_set_nil t y)
266Proof
267 Induct \\ rw [st_set_nil_def, st_sorted_def] >>
268 qmatch_asmsub_rename_tac`st_set_nil tt _ = _` >>
269 Cases_on`tt` \\ gvs[st_set_nil_def]
270QED
271
272Theorem st_set_nil_not_nothing[simp]:
273 st_set_nil t y ≠ Nothing
274Proof
275 Cases_on`t` \\ rw[]
276QED
277
278Theorem st_set_cons_not_nothing[simp]:
279 st_set_cons t x xs y ≠ Nothing
280Proof
281 Cases_on`t` \\ rw[st_set_cons_def]
282QED
283
284Theorem st_sorted_st_set_cons[simp]:
285 ∀t x xs y. st_sorted t ⇒ st_sorted (st_set_cons t x xs y)
286Proof
287 Induct \\ rw[st_set_cons_def, st_sorted_def]
288 >> gvs[stringTheory.char_lt_def, stringTheory.char_gt_def]
289 >- (
290 qmatch_asmsub_rename_tac`st_set_cons tt _ _ _ = _` >>
291 Cases_on`tt` \\ gvs[st_set_cons_def] >>
292 gvs[stringTheory.char_lt_def, stringTheory.char_gt_def] >>
293 qmatch_asmsub_rename_tac`ORD c2 > _` >>
294 qmatch_goalsub_rename_tac`_ < ORD c1` >>
295 Cases_on`c1 = c2` >> gvs[] >>
296 gvs[CaseEq"bool"]) >>
297 CASE_TAC \\ gvs[]
298QED
299
300Theorem st_sorted_st_sets[simp]:
301 st_sorted t ⇒ st_sorted (st_sets t xs)
302Proof
303 Induct_on`xs` \\ simp[st_sets_def] >>
304 Cases >> simp[st_sets_def] >> rw[] >>
305 qmatch_goalsub_rename_tac`st_set _ s _` >>
306 Cases_on`s` >> gvs[st_set_def]
307QED
308
309(* When st_sorted t and t = Branch c t1 t2, looking up (h::rest) where
310 h < c should give NONE, because all branches in the chain have chars ≥ c *)
311Theorem st_get_cons_sorted_lt:
312 ∀t h rest. st_sorted t ⇒
313 (∀c' t1' t2'. t = Branch c' t1' t2' ⇒ h < c') ⇒
314 st_get_cons t h rest = NONE
315Proof
316 Induct \\ rw [st_get_def, st_sorted_def]
317 \\ gvs [stringTheory.char_lt_def, stringTheory.char_gt_def]
318 \\ first_x_assum irule \\ rw [st_sorted_def]
319 \\ res_tac \\ fs []
320QED
321
322Theorem ALOOKUP_MAP_CONS_CONS[local]:
323 ALOOKUP (MAP (λ(k,v). (c::k,v)) ls) (d::rest) =
324 if c = d then ALOOKUP ls rest else NONE
325Proof
326 Induct_on`ls` \\ rw[] \\ pairarg_tac \\ gvs[]
327QED
328
329Theorem ALOOKUP_st_flat:
330 st_sorted t ⇒ ALOOKUP (st_flat t) n = st_get t n
331Proof
332 qid_spec_tac `n` \\ Induct_on `t`
333 \\ rw [st_flat_def, st_sorted_def]
334 >- rw[st_get_def, st_get_nil_def]
335 >- (Cases_on `n` \\ fs [st_get_def, st_get_nil_def])
336 \\ Cases_on `n`
337 >- (
338 simp [ALOOKUP_APPEND, st_get_def, st_get_nil_def] >>
339 CASE_TAC >> imp_res_tac ALOOKUP_MEM >>
340 gvs[MEM_MAP, EXISTS_PROD] ) >>
341 simp [ALOOKUP_APPEND, st_get_def, ALOOKUP_MAP_CONS_CONS] >>
342 rw []
343 \\ gvs [stringTheory.char_lt_def, stringTheory.char_gt_def]
344 >- (
345 CASE_TAC >>
346 irule st_get_cons_sorted_lt >>
347 rw[stringTheory.char_lt_def] )
348 >- (
349 irule st_get_cons_sorted_lt >>
350 rw[stringTheory.char_lt_def] >>
351 CCONTR_TAC >> gvs[NOT_LESS] ) >>
352 `ORD c <> ORD h` by simp[stringTheory.ORD_11] >>
353 gvs[]
354QED
355
356Theorem st_get_nil_st_set_nil[simp]:
357 ∀t y. st_get_nil (st_set_nil t y) = SOME y
358Proof
359 Induct \\ rw [st_set_nil_def, st_get_nil_def]
360QED
361
362Theorem st_get_cons_st_set_nil[simp]:
363 ∀t y x xs. st_get_cons (st_set_nil t y) x xs = st_get_cons t x xs
364Proof
365 Induct \\ rw [st_set_nil_def, st_get_def]
366QED
367
368Theorem st_get_nil_st_set_cons[simp]:
369 ∀t x xs y. st_get_nil (st_set_cons t x xs y) = st_get_nil t
370Proof
371 Induct \\ rw [st_set_cons_def, st_get_nil_def]
372 \\ gvs [st_get_nil_def]
373QED
374
375Theorem st_get_nil_st_make:
376 ∀xs y. st_get_nil (st_make xs y) = if xs = [] then SOME y else NONE
377Proof
378 Cases \\ rw [st_make_def, st_get_nil_def]
379QED
380
381Theorem st_get_cons_st_set_cons:
382 ∀t x xs y h rest.
383 st_sorted t ⇒
384 st_get_cons (st_set_cons t x xs y) h rest =
385 if h = x ∧ rest = xs then SOME y
386 else st_get_cons t h rest
387Proof
388 Induct \\ rw[st_set_cons_def, st_get_def]
389 \\ gvs [stringTheory.char_lt_def, stringTheory.char_gt_def, st_sorted_def]
390 \\ gvs[st_get_st_make]
391 \\ TRY (
392 rw[] >> first_x_assum irule
393 \\ irule $ iffLR stringTheory.ORD_11
394 \\ gvs[] ) >>
395 CASE_TAC \\ gvs[st_get_def] >>
396 `ORD c = ORD x ∧ ORD c = ORD h` by gvs[] >>
397 gvs[stringTheory.ORD_11]
398 >- (Cases_on`rest` \\ gvs[st_get_def]) >>
399 Cases_on`rest=[]` \\ gvs[st_get_def] >>
400 Cases_on`rest` >- gvs[] >>
401 simp[st_get_def] >> IF_CASES_TAC >> simp[] >> gvs[]
402QED
403
404Theorem st_get_st_set:
405 ∀t k v n. st_sorted t ⇒
406 st_get (st_set t k v) n = if n = k then SOME v else st_get t n
407Proof
408 rpt strip_tac
409 \\ Cases_on `k` \\ Cases_on `n`
410 \\ fs [st_set_def, st_get_def,
411 st_get_nil_st_set_nil, st_get_cons_st_set_nil,
412 st_get_nil_st_set_cons, st_get_cons_st_set_cons]
413 \\ rw [] \\ gvs []
414QED
415
416Theorem st_get_st_sets:
417 st_sorted t ⇒
418 st_get (st_sets t xs) n = case ALOOKUP xs n of NONE => st_get t n | res => res
419Proof
420 strip_tac
421 \\ Induct_on `xs` \\ fs [st_sets_def, FORALL_PROD]
422 \\ rw []
423 \\ DEP_REWRITE_TAC [st_get_st_set]
424 \\ rw [] \\ fs []
425QED
426
427Theorem st_sorted_not_Nothing_get:
428 ∀t. st_sorted t ∧ t ≠ Nothing ⇒ ∃k v. st_get t k = SOME v
429Proof
430 Induct \\ rw [st_sorted_def]
431 >- (qexists_tac `[]` \\ simp [st_get_def, st_get_nil_def])
432 >- (rename [`st_get (Branch c t1 t2)`]
433 \\ first_x_assum (drule_all_then strip_assume_tac)
434 \\ qexists_tac `c::k` \\ simp [st_get_def]
435 \\ gvs [stringTheory.char_lt_def, stringTheory.char_gt_def])
436QED
437
438Theorem st_sorted_st_get_eq:
439 ∀t1 t2. st_sorted t1 ∧ st_sorted t2 ∧
440 (∀n. st_get t1 n = st_get t2 n) ⇒ t1 = t2
441Proof
442 Induct
443 >- (Cases \\ rw [st_sorted_def]
444 >- (qexists_tac`[]` \\ rw[st_get_def]) >>
445 CCONTR_TAC \\ gvs[] >>
446 drule_all st_sorted_not_Nothing_get >>
447 simp[] >> rpt strip_tac >>
448 first_x_assum(qspec_then`c::k`mp_tac) >>
449 simp[st_get_def, stringTheory.char_gt_def, stringTheory.char_lt_def])
450 >- (Cases_on`t2` \\ rw [st_sorted_def]
451 >- (qexists_tac`[]` \\ rw[st_get_def])
452 >- (first_x_assum (qspec_then `[]` mp_tac)
453 \\ rw [st_get_def, st_get_nil_def]) >>
454 CCONTR_TAC \\ gvs[] >>
455 drule_all st_sorted_not_Nothing_get \\ rw[] >>
456 first_x_assum (qspec_then `c::k` mp_tac)
457 \\ simp [st_get_def, st_get_nil_def]
458 \\ gvs [stringTheory.char_lt_def, stringTheory.char_gt_def]) >>
459 Cases_on`t2` >> simp[st_sorted_def]
460 >- (
461 CCONTR_TAC \\ gvs[] >>
462 drule_all st_sorted_not_Nothing_get >> rw[] >>
463 first_x_assum (qspec_then `c::k` mp_tac)
464 \\ simp [st_get_def, st_get_nil_def]
465 \\ gvs [stringTheory.char_lt_def, stringTheory.char_gt_def])
466 >- (
467 CCONTR_TAC \\ gvs[] >>
468 drule_all st_sorted_not_Nothing_get >> rw[] >>
469 first_x_assum (qspec_then `c::k` mp_tac)
470 \\ simp [st_get_def, st_get_nil_def]
471 \\ gvs [stringTheory.char_lt_def, stringTheory.char_gt_def]) >>
472 gen_tac >> strip_tac >>
473 Cases_on`char_lt c c'`
474 >- (
475 qspec_then`s`mp_tac st_sorted_not_Nothing_get >>
476 impl_tac >- rw[] >> strip_tac >>
477 first_assum(qspec_then`c::k`mp_tac) >>
478 simp_tac(srw_ss())[st_get_def] >>
479 gvs[stringTheory.char_lt_def, stringTheory.char_gt_def] ) >>
480 Cases_on`char_lt c' c`
481 >- (
482 qspec_then`t1`mp_tac st_sorted_not_Nothing_get >>
483 impl_tac >- rw[] >> strip_tac >>
484 first_assum(qspec_then`c'::k`mp_tac) >>
485 simp_tac(srw_ss())[st_get_def] >>
486 gvs[stringTheory.char_lt_def, stringTheory.char_gt_def] ) >>
487 `ORD c = ORD c'` by gvs[stringTheory.char_lt_def] >>
488 gvs[stringTheory.ORD_11] >>
489 conj_tac
490 >- (
491 first_x_assum irule \\ simp[] >>
492 gen_tac >>
493 first_x_assum(qspec_then`c::n`mp_tac) >>
494 simp[st_get_def, stringTheory.char_gt_def] ) >>
495 first_x_assum irule \\ simp[] >> gen_tac >>
496 first_x_assum(qspec_then`n`mp_tac) >>
497 Cases_on`n` \\ simp[st_get_def] >>
498 Cases_on`char_lt c h` >> gvs[]
499 >- gvs[stringTheory.char_lt_def, stringTheory.char_gt_def] >>
500 strip_tac >>
501 gvs[stringTheory.char_lt_def, stringTheory.char_gt_def] >>
502 qmatch_goalsub_abbrev_tac `sg1 = sg2` >>
503 `sg1 = NONE ∧ sg2 = NONE` suffices_by rw[] >>
504 unabbrev_all_tac >>
505 conj_tac >> irule st_get_cons_sorted_lt >> gvs[] >>
506 rpt strip_tac >> first_x_assum drule >>
507 gvs[stringTheory.char_lt_def, stringTheory.char_gt_def]
508QED
509
510Theorem st_sets_eq:
511 st_sorted t ⇒ ALOOKUP xs = ALOOKUP ys ⇒ st_sets t xs = st_sets t ys
512Proof
513 rw []
514 \\ irule st_sorted_st_get_eq
515 \\ rw []
516 \\ DEP_REWRITE_TAC [st_get_st_sets] \\ fs []
517QED
518
519Theorem st_sorted_st_del_nil[simp]:
520 ∀t. st_sorted t ⇒ st_sorted (st_del_nil t)
521Proof
522 Induct \\ rw [st_del_nil_def, st_sorted_def] >>
523 Cases_on`t'` \\ gvs[]
524QED
525
526Theorem mk_Branch_thm:
527 mk_Branch c t1 t2 = if t1 = Nothing then t2 else Branch c t1 t2
528Proof
529 Cases_on ‘t1’ \\ gvs [mk_Branch_def]
530QED
531
532Theorem st_sorted_mk_Branch:
533 st_sorted (mk_Branch c t1 t2) ⇔
534 st_sorted t1 ∧ st_sorted t2 ∧
535 (t1 ≠ Nothing ⇒ ∀c' t1' t2'. t2 = Branch c' t1' t2' ⇒ c < c')
536Proof
537 rw [mk_Branch_thm, st_sorted_def] \\ rw [] \\ eq_tac \\ rw []
538QED
539
540Theorem st_del_cons_not_Branch_Nothing:
541 ∀t x xs c rest. st_sorted t ⇒
542 st_del_cons t x xs ≠ Branch c Nothing rest
543Proof
544 Induct \\ rw [st_del_cons_def, st_sorted_def]
545 \\ gvs [mk_Branch_thm, AllCaseEqs()]
546 \\ gvs[stringTheory.char_gt_def, stringTheory.char_lt_def]
547 \\ `ORD c = ORD x` by gvs[]
548 \\ gvs[stringTheory.ORD_11]
549 \\ CCONTR_TAC \\ gvs[]
550 \\ gvs[Once(oneline st_del_nil_def),AllCaseEqs(),st_sorted_def]
551QED
552
553Theorem st_sorted_st_del_cons[simp]:
554 ∀t x xs. st_sorted t ⇒ st_sorted (st_del_cons t x xs)
555Proof
556 Induct \\ rw [st_del_cons_def, st_sorted_def]
557 \\ gvs [st_sorted_def, st_sorted_mk_Branch]
558 \\ TRY (CASE_TAC \\ gvs [])
559 \\ pop_assum mp_tac
560 \\ simp[Once(oneline st_del_cons_def)]
561 \\ BasicProvers.TOP_CASE_TAC \\ gvs[]
562 \\ gvs[stringTheory.char_lt_def, stringTheory.char_gt_def]
563 \\ rw[] \\ gvs[]
564 \\ gvs[mk_Branch_thm, AllCaseEqs(), st_sorted_def]
565 \\ Cases_on`s` \\ gvs[stringTheory.char_lt_def]
566QED
567
568Theorem st_sorted_st_del[simp]:
569 ∀t k. st_sorted t ⇒ st_sorted (st_del t k)
570Proof
571 rpt strip_tac \\ Cases_on `k`
572 \\ fs [st_del_def]
573QED
574
575Theorem st_get_nil_st_del_nil[simp]:
576 ∀t. st_get_nil (st_del_nil t) = NONE
577Proof
578 Induct \\ rw [st_del_nil_def, st_get_nil_def]
579QED
580
581Theorem st_get_cons_st_del_nil[simp]:
582 ∀t x xs. st_get_cons (st_del_nil t) x xs = st_get_cons t x xs
583Proof
584 Induct \\ rw [st_del_nil_def, st_get_def]
585QED
586
587Theorem st_get_nil_mk_Branch[simp]:
588 ∀c t1 t2. st_get_nil (mk_Branch c t1 t2) = st_get_nil t2
589Proof
590 rw [mk_Branch_thm, st_get_nil_def]
591QED
592
593Theorem st_get_cons_mk_Branch:
594 ∀c t1 t2 x xs.
595 st_get_cons (mk_Branch c t1 t2) x xs =
596 if t1 = Nothing then st_get_cons t2 x xs
597 else st_get_cons (Branch c t1 t2) x xs
598Proof
599 rw [mk_Branch_thm]
600QED
601
602Theorem st_get_nil_st_del_cons[simp]:
603 ∀t x xs. st_get_nil (st_del_cons t x xs) = st_get_nil t
604Proof
605 Induct \\ rw [st_del_cons_def, st_get_nil_def]
606 \\ gvs [st_get_nil_def, mk_Branch_thm]
607QED
608
609Theorem st_get_cons_st_del_cons:
610 ∀t x xs h rest.
611 st_sorted t ⇒
612 st_get_cons (st_del_cons t x xs) h rest =
613 if h = x ∧ rest = xs then NONE
614 else st_get_cons t h rest
615Proof
616 Induct
617 \\ simp[st_del_cons_def, st_get_def]
618 \\ rpt gen_tac \\ strip_tac
619 \\ gvs [stringTheory.char_lt_def, stringTheory.char_gt_def, st_sorted_def]
620 \\ rw [st_get_cons_mk_Branch, st_get_def]
621 \\ gvs [stringTheory.char_lt_def, stringTheory.char_gt_def]
622 \\ CASE_TAC \\ rw[]
623 \\ gvs [st_get_def, st_get_nil_st_del_nil,
624 st_get_cons_st_del_nil, st_get_nil_def]
625 \\ TRY (
626 simp[Once(oneline st_get_def)]
627 \\ CASE_TAC
628 \\ simp[stringTheory.char_lt_def, stringTheory.char_gt_def]
629 \\ gvs[] \\ NO_TAC) >>
630 gvs[NOT_LESS, NOT_GREATER] >>
631 imp_res_tac LE_ANTISYM >>
632 imp_res_tac stringTheory.ORD_11 >>
633 rpt BasicProvers.VAR_EQ_TAC >> gvs[]
634 >- (
635 Cases_on`t` \\ gvs[st_get_def] >>
636 drule st_get_cons_sorted_lt >>
637 simp[stringTheory.char_lt_def] >>
638 Cases_on`rest` \\ rw[st_get_def] )
639 >- ( Cases_on`rest` \\ rw[st_get_def] )
640 >- (
641 qmatch_goalsub_abbrev_tac`sg1 = sg2` \\
642 `sg1 = NONE ∧ sg2 = NONE` suffices_by rw[] \\
643 unabbrev_all_tac \\
644 conj_tac >- ( irule st_get_cons_sorted_lt \\ rw[stringTheory.char_lt_def] )
645 >> Cases_on`rest` \\ gvs[st_get_def]
646 >- (
647 irule EQ_TRANS
648 \\ `st_get_nil Nothing = NONE` by simp[]
649 \\ goal_assum $ drule_at Any
650 \\ qpat_assum`_ = Nothing`(SUBST1_TAC o SYM)
651 \\ simp[] )
652 \\ qmatch_asmsub_rename_tac`st_del_cons t h1 t2`
653 \\ last_x_assum(qspecl_then[`h1`,`t2`]mp_tac)
654 \\ simp[]
655 \\ qmatch_goalsub_rename_tac`st_get_cons t h t3`
656 \\ disch_then(qspecl_then[`h`,`t3`]mp_tac)
657 \\ rw[st_get_def] ) >>
658 Cases_on`rest` \\ gvs[st_get_def] >> rw[]
659QED
660
661Theorem st_get_st_del:
662 ∀t k n. st_sorted t ⇒
663 st_get (st_del t k) n = if n = k then NONE else st_get t n
664Proof
665 rpt strip_tac
666 \\ Cases_on `k` \\ Cases_on `n`
667 \\ fs [st_del_def, st_get_def,
668 st_get_nil_st_del_nil, st_get_cons_st_del_nil,
669 st_get_nil_st_del_cons, st_get_cons_st_del_cons]
670 \\ rw [] \\ gvs []
671QED
672
673Theorem st_sorted_st_set[simp]:
674 st_sorted t ⇒
675 st_sorted (st_set t m x)
676Proof
677 Cases_on`m` \\ rw[]
678QED
679
680Theorem st_del_st_set:
681 st_sorted t ⇒
682 st_del (st_set t n x) m = if m = n then st_del t m
683 else st_set (st_del t m) n x
684Proof
685 rw []
686 \\ irule st_sorted_st_get_eq \\ rw []
687 \\ DEP_REWRITE_TAC [st_get_st_del, st_get_st_set]
688 \\ rw [] \\ gvs []
689QED
690
691Theorem st_del_st_sets:
692 st_sorted t ⇒
693 st_del (st_sets t xs) n = st_sets (st_del t n) (FILTER (λ(k,v). k ≠ n) xs)
694Proof
695 strip_tac
696 \\ Induct_on `xs`
697 \\ fs [st_sets_def, FORALL_PROD]
698 \\ rw []
699 \\ DEP_REWRITE_TAC [st_del_st_set]
700 \\ rw []
701 \\ simp [st_sets_def]
702QED
703
704Theorem st_union_eq_Nothing[simp]:
705 st_union t u = Nothing ⇔ t = Nothing ∧ u = Nothing
706Proof
707 Cases_on ‘t’ \\ Cases_on ‘u’ \\ gvs [st_union_def] \\ rw []
708QED
709
710Theorem st_union_Branch:
711 ∀t u c t1 t2.
712 st_union t u = Branch c t1 t2 ⇒
713 (∃x y. t = Branch c x y) ∨ (∃x y. u = Branch c x y)
714Proof
715 Cases \\ Cases \\ gvs [st_union_def] \\ rw [] \\ gvs []
716QED
717
718Theorem st_sorted_st_union[simp]:
719 ∀t1 t2.
720 st_sorted t1 ∧ st_sorted t2 ⇒
721 st_sorted (st_union t1 t2)
722Proof
723 ho_match_mp_tac st_union_ind \\ rw [st_union_def, st_sorted_def]
724 \\ gvs [st_sorted_def]
725 \\ drule st_union_Branch \\ strip_tac \\ gvs []
726 \\ res_tac \\ gvs [stringTheory.char_lt_def]
727QED
728
729Theorem st_get_nil_st_union:
730 ∀t u.
731 st_get_nil (st_union t u) =
732 case st_get_nil t of
733 | SOME r => SOME r
734 | NONE => st_get_nil u
735Proof
736 ho_match_mp_tac st_union_ind \\ rw [st_union_def]
737 \\ CASE_TAC \\ gvs []
738QED
739
740Theorem option_case_id[local]:
741 (case x of NONE => NONE | SOME r => SOME r) = x
742Proof
743 Cases_on ‘x’ \\ gvs []
744QED
745
746Theorem st_get_st_union:
747 ∀t1 t2 n.
748 st_sorted t1 ∧ st_sorted t2 ⇒
749 st_get (st_union t1 t2) n =
750 case st_get t1 n of
751 | SOME r => SOME r
752 | NONE => st_get t2 n
753Proof
754 ho_match_mp_tac st_union_ind \\ rpt strip_tac
755 \\ Cases_on ‘n’
756 \\ gvs [st_union_def, st_get_def, st_get_nil_st_union, option_case_id]
757 \\ gvs [st_sorted_def]
758 >- (rename [‘st_get_cons (st_union (Just x) u) h s’]
759 \\ first_x_assum (qspec_then ‘STRING h s’ mp_tac)
760 \\ gvs [st_get_def])
761 >- (rename [‘st_get_cons (st_union u (Just x)) h s’]
762 \\ first_x_assum (qspec_then ‘STRING h s’ mp_tac)
763 \\ gvs [st_get_def, option_case_id])
764 \\ rename [‘st_get_cons (if ORD c1 < ORD c2 then _ else _) h s’]
765 \\ Cases_on ‘ORD c1 < ORD c2’ \\ gvs []
766 >- (first_x_assum (qspec_then ‘STRING h s’ mp_tac)
767 \\ gvs [st_get_def, stringTheory.char_lt_def, stringTheory.char_gt_def]
768 \\ rw [] \\ gvs [option_case_id])
769 \\ Cases_on ‘ORD c2 < ORD c1’ \\ gvs []
770 >- (first_x_assum (qspec_then ‘STRING h s’ mp_tac)
771 \\ gvs [st_get_def, stringTheory.char_lt_def, stringTheory.char_gt_def]
772 \\ rw [] \\ gvs [option_case_id])
773 \\ ‘c1 = c2’ by gvs [GSYM stringTheory.ORD_11] \\ gvs []
774 \\ rename [‘st_get_cons (Branch c (st_union l1 r1) (st_union l2 r2)) h s’]
775 \\ qpat_x_assum ‘∀n. st_get (st_union l2 r2) n = _’
776 (qspec_then ‘STRING h s’ mp_tac)
777 \\ qpat_x_assum ‘∀n. st_get (st_union l1 r1) n = _’
778 (qspec_then ‘s’ mp_tac)
779 \\ gvs [st_get_def, stringTheory.char_lt_def, stringTheory.char_gt_def]
780 \\ rw [] \\ gvs [option_case_id]
781QED
782
783Theorem st_inter_Just_left[local]:
784 ∀u x. st_inter (Just x) u =
785 case st_get_nil u of
786 | NONE => Nothing
787 | SOME _ => Just x
788Proof
789 Induct \\ gvs [st_inter_def]
790QED
791
792Theorem st_inter_Just_right[local]:
793 ∀t x. st_inter t (Just x) =
794 case st_get_nil t of
795 | NONE => Nothing
796 | SOME y => Just y
797Proof
798 Induct \\ gvs [st_inter_def]
799QED
800
801Theorem st_inter_Branch_le[local]:
802 ∀t u c' t1 t2.
803 st_sorted t ∧ st_inter t u = Branch c' t1 t2 ⇒
804 ∃d s1 s2. t = Branch d s1 s2 ∧ ORD d ≤ ORD c'
805Proof
806 ho_match_mp_tac st_inter_ind \\ rpt strip_tac
807 \\ gvs [st_inter_def, st_inter_Just_left, st_inter_Just_right, AllCaseEqs()]
808 \\ gvs [st_sorted_def, mk_Branch_thm, AllCaseEqs()]
809 \\ gvs [stringTheory.char_lt_def]
810QED
811
812Theorem st_sorted_st_inter[simp]:
813 ∀t u.
814 st_sorted t ∧ st_sorted u ⇒
815 st_sorted (st_inter t u)
816Proof
817 ho_match_mp_tac st_inter_ind \\ rpt strip_tac
818 \\ gvs [st_inter_def, st_inter_Just_left, st_inter_Just_right, AllCaseEqs()]
819 \\ gvs [st_sorted_def]
820 \\ rw [st_sorted_mk_Branch]
821 \\ drule_all st_inter_Branch_le
822 \\ rw [] \\ gvs [stringTheory.char_lt_def]
823QED
824
825Theorem st_get_nil_st_inter:
826 ∀t u.
827 st_get_nil (st_inter t u) =
828 case st_get_nil u of
829 | NONE => NONE
830 | SOME _ => st_get_nil t
831Proof
832 ho_match_mp_tac st_inter_ind \\ rw [st_inter_def]
833 \\ CASE_TAC \\ gvs []
834QED
835
836Theorem st_get_st_inter:
837 ∀t1 t2 n.
838 st_sorted t1 ∧ st_sorted t2 ⇒
839 st_get (st_inter t1 t2) n =
840 case st_get t2 n of
841 | NONE => NONE
842 | SOME _ => st_get t1 n
843Proof
844 ho_match_mp_tac st_inter_ind \\ rpt strip_tac
845 \\ Cases_on ‘n’
846 \\ gvs [st_inter_def, st_get_def, st_get_nil_st_inter, option_case_id,
847 st_inter_Just_left, st_inter_Just_right]
848 \\ gvs [st_sorted_def]
849 >- (rpt CASE_TAC \\ gvs [st_get_def])
850 >- (rpt CASE_TAC \\ gvs [st_get_def])
851 >- (rpt CASE_TAC \\ gvs [st_get_def])
852 \\ rename [‘st_get_cons (if ORD c1 < ORD c2 then _ else _) h s’]
853 \\ Cases_on ‘ORD c1 < ORD c2’ \\ gvs []
854 >- (first_x_assum (qspec_then ‘STRING h s’ mp_tac)
855 \\ gvs [st_get_def, stringTheory.char_lt_def, stringTheory.char_gt_def]
856 \\ rw [] \\ gvs [] \\ rpt CASE_TAC \\ gvs [])
857 \\ Cases_on ‘ORD c2 < ORD c1’ \\ gvs []
858 >- (first_x_assum (qspec_then ‘STRING h s’ mp_tac)
859 \\ gvs [st_get_def, stringTheory.char_lt_def, stringTheory.char_gt_def]
860 \\ rw [] \\ gvs [] \\ rpt CASE_TAC \\ gvs [])
861 \\ ‘c1 = c2’ by gvs [GSYM stringTheory.ORD_11] \\ gvs []
862 \\ rename [‘st_get_cons (mk_Branch c (st_inter l1 r1) (st_inter l2 r2)) h s’]
863 \\ qpat_x_assum ‘∀n. st_get (st_inter l2 r2) n = _’
864 (qspec_then ‘STRING h s’ mp_tac)
865 \\ qpat_x_assum ‘∀n. st_get (st_inter l1 r1) n = _’
866 (qspec_then ‘s’ mp_tac)
867 \\ gvs [st_get_cons_mk_Branch, st_get_def,
868 stringTheory.char_lt_def, stringTheory.char_gt_def]
869 \\ rw [] \\ gvs []
870 \\ ‘st_get_cons l2 h s = NONE’ by
871 (irule st_get_cons_sorted_lt
872 \\ gvs [stringTheory.char_lt_def] \\ rw [] \\ res_tac \\ gvs [])
873 \\ gvs [] \\ rpt CASE_TAC \\ gvs []
874QED
875
876Theorem st_minus_Just_left[local]:
877 ∀u x. st_minus (Just x) u =
878 case st_get_nil u of
879 | NONE => Just x
880 | SOME _ => Nothing
881Proof
882 Induct \\ gvs [st_minus_def]
883QED
884
885Theorem st_minus_Branch_le[local]:
886 ∀t u c' t1 t2.
887 st_sorted t ∧ st_minus t u = Branch c' t1 t2 ⇒
888 ∃d s1 s2. t = Branch d s1 s2 ∧ ORD d ≤ ORD c'
889Proof
890 ho_match_mp_tac st_minus_ind \\ rpt strip_tac
891 \\ gvs [st_minus_def, st_minus_Just_left, AllCaseEqs()]
892 \\ gvs [st_sorted_def, mk_Branch_thm, AllCaseEqs()]
893 \\ gvs [stringTheory.char_lt_def]
894QED
895
896Theorem st_sorted_st_minus[simp]:
897 ∀t u.
898 st_sorted t ∧ st_sorted u ⇒
899 st_sorted (st_minus t u)
900Proof
901 ho_match_mp_tac st_minus_ind \\ rpt strip_tac
902 \\ gvs [st_minus_def, st_minus_Just_left, AllCaseEqs()]
903 \\ gvs [st_sorted_def]
904 \\ rw [st_sorted_mk_Branch, st_sorted_def]
905 \\ drule_all st_minus_Branch_le
906 \\ rw [] \\ gvs [stringTheory.char_lt_def]
907QED
908
909Theorem st_get_nil_st_minus:
910 ∀t u.
911 st_get_nil (st_minus t u) =
912 case st_get_nil u of
913 | NONE => st_get_nil t
914 | SOME _ => NONE
915Proof
916 ho_match_mp_tac st_minus_ind \\ rw [st_minus_def]
917 \\ CASE_TAC \\ gvs []
918QED
919
920Theorem st_get_st_minus:
921 ∀t1 t2 n.
922 st_sorted t1 ∧ st_sorted t2 ⇒
923 st_get (st_minus t1 t2) n =
924 case st_get t2 n of
925 | NONE => st_get t1 n
926 | SOME _ => NONE
927Proof
928 ho_match_mp_tac st_minus_ind \\ rpt strip_tac
929 \\ Cases_on ‘n’
930 \\ gvs [st_minus_def, st_get_def, st_get_nil_st_minus, option_case_id,
931 st_minus_Just_left]
932 \\ gvs [st_sorted_def]
933 >- (rpt CASE_TAC \\ gvs [st_get_def])
934 >- (rpt CASE_TAC \\ gvs [st_get_def])
935 >- (rename [‘st_get_cons (st_minus u (Just x)) h s’]
936 \\ first_x_assum (qspec_then ‘STRING h s’ mp_tac)
937 \\ gvs [st_get_def])
938 \\ rename [‘st_get_cons (if ORD c1 < ORD c2 then _ else _) h s’]
939 \\ Cases_on ‘ORD c1 < ORD c2’ \\ gvs []
940 >- (first_x_assum (qspec_then ‘STRING h s’ mp_tac)
941 \\ gvs [st_get_def, stringTheory.char_lt_def, stringTheory.char_gt_def]
942 \\ rw [] \\ gvs [] \\ rpt CASE_TAC \\ gvs [])
943 \\ Cases_on ‘ORD c2 < ORD c1’ \\ gvs []
944 >- (first_x_assum (qspec_then ‘STRING h s’ mp_tac)
945 \\ gvs [st_get_def, stringTheory.char_lt_def, stringTheory.char_gt_def]
946 \\ rw [] \\ gvs [] \\ rpt CASE_TAC \\ gvs [])
947 \\ ‘c1 = c2’ by gvs [GSYM stringTheory.ORD_11] \\ gvs []
948 \\ rename [‘st_get_cons (mk_Branch c (st_minus l1 r1) (st_minus l2 r2)) h s’]
949 \\ qpat_x_assum ‘∀n. st_get (st_minus l2 r2) n = _’
950 (qspec_then ‘STRING h s’ mp_tac)
951 \\ qpat_x_assum ‘∀n. st_get (st_minus l1 r1) n = _’
952 (qspec_then ‘s’ mp_tac)
953 \\ gvs [st_get_cons_mk_Branch, st_get_def,
954 stringTheory.char_lt_def, stringTheory.char_gt_def]
955 \\ rw [] \\ gvs []
956 \\ ‘st_get_cons l2 h s = NONE’ by
957 (irule st_get_cons_sorted_lt
958 \\ gvs [stringTheory.char_lt_def] \\ rw [] \\ res_tac \\ gvs [])
959 \\ gvs [] \\ rpt CASE_TAC \\ gvs []
960QED
961
962Theorem st_card_st_flat[local]:
963 ∀t. st_card t = LENGTH (st_flat t)
964Proof
965 Induct \\ gvs [st_card_def, st_flat_def]
966QED
967
968Theorem MEM_st_flat_lt[local]:
969 ∀t c k v.
970 st_sorted t ∧ (∀d t1 t2. t = Branch d t1 t2 ⇒ c < d) ∧
971 MEM (k,v) (st_flat t) ⇒
972 k = [] ∨ ∃d k'. k = STRING d k' ∧ c < d
973Proof
974 Induct \\ gvs [st_flat_def, st_sorted_def, MEM_MAP, EXISTS_PROD]
975 \\ rw [] \\ gvs []
976 \\ last_x_assum drule_all \\ rw [] \\ gvs [stringTheory.char_lt_def]
977QED
978
979Theorem MAP_FST_MAP_CONS[local]:
980 MAP FST (MAP (λ(k,v). (STRING c k,v)) l) = MAP (STRING c) (MAP FST l)
981Proof
982 gvs [MAP_MAP_o, combinTheory.o_DEF, LAMBDA_PROD]
983QED
984
985Theorem ALL_DISTINCT_st_flat[local]:
986 ∀t. st_sorted t ⇒ ALL_DISTINCT (MAP FST (st_flat t))
987Proof
988 Induct \\ gvs [st_flat_def, st_sorted_def]
989 \\ rw [MAP_FST_MAP_CONS, ALL_DISTINCT_APPEND]
990 >- (irule ALL_DISTINCT_MAP_INJ \\ gvs [])
991 \\ gvs [MEM_MAP] \\ rw []
992 \\ CCONTR_TAC \\ gvs [MEM_MAP, EXISTS_PROD]
993 \\ drule MEM_st_flat_lt \\ disch_then drule \\ gvs []
994 \\ Cases_on ‘y’ \\ gvs []
995 \\ first_assum $ irule_at Any \\ gvs [stringTheory.char_lt_def]
996QED
997
998Theorem st_submap_thm:
999 ∀t u.
1000 st_sorted t ∧ st_sorted u ⇒
1001 (st_submap t u ⇔ ∀k v. st_get t k = SOME v ⇒ st_get u k = SOME v)
1002Proof
1003 ho_match_mp_tac st_submap_ind \\ rpt strip_tac
1004 \\ gvs [st_submap_def, st_get_def, st_sorted_def]
1005 >- (qexists_tac ‘[]’ \\ gvs [st_get_def])
1006 >- (irule st_sorted_not_Nothing_get \\ gvs [st_sorted_def])
1007 >- (eq_tac \\ rw [] \\ gvs [st_get_def]
1008 \\ first_x_assum (qspecl_then [‘[]’,‘x’] mp_tac) \\ gvs [st_get_def])
1009 >- (eq_tac \\ rw [] \\ Cases_on ‘k’ \\ gvs [st_get_def]
1010 \\ first_x_assum (qspecl_then [‘[]’,‘v’] mp_tac) \\ gvs [st_get_def])
1011 >- (rename [‘Branch c l1 l2’]
1012 \\ qspec_then ‘l1’ mp_tac st_sorted_not_Nothing_get \\ gvs [] \\ rw []
1013 \\ qexists_tac ‘STRING c k’ \\ qexists_tac ‘v’
1014 \\ gvs [st_get_def, stringTheory.char_lt_def, stringTheory.char_gt_def])
1015 \\ rename [‘st_get (Branch c1 l1 l2) _ = SOME _ ⇒
1016 st_get (Branch c2 r1 r2) _ = SOME _’]
1017 \\ Cases_on ‘ORD c1 < ORD c2’ \\ gvs []
1018 >- (qspec_then ‘l1’ mp_tac st_sorted_not_Nothing_get \\ gvs [] \\ rw []
1019 \\ qexists_tac ‘STRING c1 k’ \\ qexists_tac ‘v’
1020 \\ gvs [st_get_def, stringTheory.char_lt_def, stringTheory.char_gt_def])
1021 \\ Cases_on ‘ORD c2 < ORD c1’ \\ gvs []
1022 >- (‘∀k v. st_get (Branch c1 l1 l2) k = SOME v ⇒
1023 st_get (Branch c2 r1 r2) k = st_get r2 k’ by
1024 (Cases \\ gvs [st_get_def, stringTheory.char_lt_def,
1025 stringTheory.char_gt_def]
1026 \\ rw [] \\ gvs [])
1027 \\ eq_tac \\ rw [] \\ res_tac \\ gvs [])
1028 \\ ‘c1 = c2’ by gvs [GSYM stringTheory.ORD_11] \\ gvs []
1029 \\ ‘∀h rest. st_get_cons l2 h rest ≠ NONE ⇒ ORD c1 < ORD h’ by
1030 (rpt strip_tac \\ CCONTR_TAC
1031 \\ qspecl_then [‘l2’,‘h’,‘rest’] mp_tac st_get_cons_sorted_lt
1032 \\ gvs [] \\ rw [] \\ gvs [stringTheory.char_lt_def])
1033 \\ eq_tac \\ rw []
1034 >- (Cases_on ‘k’
1035 \\ gvs [st_get_def, stringTheory.char_lt_def, stringTheory.char_gt_def]
1036 >- (qpat_x_assum ‘∀k v. st_get l2 k = _ ⇒ _’
1037 (qspecl_then [‘[]’,‘v’] mp_tac) \\ gvs [st_get_def])
1038 \\ rw []
1039 >- (qpat_x_assum ‘∀k v. st_get l2 k = _ ⇒ _’
1040 (qspecl_then [‘STRING h t’,‘v’] mp_tac) \\ gvs [st_get_def])
1041 \\ qpat_x_assum ‘∀k v. st_get l1 k = _ ⇒ _’
1042 (qspecl_then [‘t’,‘v’] mp_tac) \\ gvs [st_get_def])
1043 >- (first_x_assum (qspecl_then [‘STRING c1 k’,‘v’] mp_tac)
1044 \\ gvs [st_get_def, stringTheory.char_lt_def, stringTheory.char_gt_def])
1045 \\ Cases_on ‘k’
1046 >- (first_x_assum (qspecl_then [‘[]’,‘v’] mp_tac) \\ gvs [st_get_def])
1047 \\ ‘ORD c1 < ORD h’ by
1048 (qpat_x_assum ‘∀h rest. st_get_cons l2 h rest ≠ NONE ⇒ _’
1049 (qspecl_then [‘h’,‘t’] mp_tac) \\ gvs [st_get_def])
1050 \\ first_x_assum (qspecl_then [‘STRING h t’,‘v’] mp_tac)
1051 \\ gvs [st_get_def, stringTheory.char_lt_def, stringTheory.char_gt_def]
1052QED
1053
1054Theorem MEM_alookup[local]:
1055 ∀l x. MEM x (MAP FST l) ⇔ ALOOKUP l x ≠ NONE
1056Proof
1057 gvs [ALOOKUP_NONE]
1058QED
1059
1060Theorem ALOOKUP_MAP_STRING[local]:
1061 ALOOKUP (MAP (λ(k,v). (STRING c k,v)) l) (STRING d rest) =
1062 (if c = d then ALOOKUP l rest else NONE) ∧
1063 ALOOKUP (MAP (λ(k,v). (STRING c k,v)) l) "" = NONE
1064Proof
1065 Induct_on ‘l’ \\ gvs [] \\ Cases \\ gvs [] \\ rw []
1066QED
1067
1068Theorem ALOOKUP_st_lex:
1069 (∀t:'a str_trie. st_sorted t ⇒ ∀k. ALOOKUP (st_lex t) k = st_get t k) ∧
1070 (∀t:'a str_trie. st_sorted t ⇒
1071 ∀k. ALOOKUP (st_branches t) k = if k = "" then NONE else st_get t k)
1072Proof
1073 ho_match_mp_tac st_lex_ind \\ rw [st_lex_def, st_get_def, st_sorted_def]
1074 \\ Cases_on ‘k’
1075 \\ gvs [ALOOKUP_APPEND, ALOOKUP_MAP_STRING, st_get_def]
1076 \\ TRY (CASE_TAC \\ gvs [st_get_def] \\ NO_TAC)
1077 \\ ‘∀d rest. ORD d ≤ ORD c ⇒ st_get_cons t' d rest = NONE’ by
1078 (rw [] \\ irule st_get_cons_sorted_lt \\ gvs [] \\ rw []
1079 \\ res_tac \\ gvs [stringTheory.char_lt_def])
1080 \\ Cases_on ‘c = h’
1081 \\ gvs [stringTheory.char_lt_def, stringTheory.char_gt_def]
1082 >- (CASE_TAC \\ gvs [])
1083 \\ rw [] \\ gvs []
1084 \\ ‘ORD h = ORD c’ by DECIDE_TAC \\ gvs [stringTheory.ORD_11]
1085QED
1086
1087Theorem st_lex_acc_thm[local]:
1088 (∀t:'a str_trie rp acc. st_lex_acc t rp acc =
1089 MAP (λ(k,v). (REVERSE rp ++ k, v)) (st_lex t) ++ acc) ∧
1090 (∀t:'a str_trie rp acc. st_branches_acc t rp acc =
1091 MAP (λ(k,v). (REVERSE rp ++ k, v)) (st_branches t) ++ acc)
1092Proof
1093 ho_match_mp_tac st_lex_acc_ind
1094 \\ rw [st_lex_acc_def, st_lex_def]
1095 \\ gvs [MAP_MAP_o, combinTheory.o_DEF, LAMBDA_PROD]
1096 \\ CASE_TAC \\ gvs []
1097QED
1098
1099Theorem st_to_list_thm:
1100 st_to_list t = st_lex t
1101Proof
1102 gvs [st_to_list_def, st_lex_acc_thm, pairTheory.ELIM_UNCURRY]
1103QED
1104
1105Theorem MEM_st_lex[local]:
1106 ∀t k. st_sorted t ⇒
1107 (MEM k (MAP FST (st_lex t)) ⇔ st_get t k ≠ NONE) ∧
1108 (MEM k (MAP FST (st_branches t)) ⇔ k ≠ "" ∧ st_get t k ≠ NONE)
1109Proof
1110 rw [MEM_alookup] \\ gvs [ALOOKUP_st_lex] \\ rw [] \\ gvs []
1111QED
1112
1113Theorem transitive_string_lt[local]:
1114 transitive string_lt
1115Proof
1116 gvs [relationTheory.transitive_def]
1117 \\ metis_tac [stringTheory.string_lt_trans]
1118QED
1119
1120Theorem SORTED_MAP_STRING[local]:
1121 ∀l. SORTED string_lt (MAP (STRING c) l) ⇔ SORTED string_lt l
1122Proof
1123 Induct \\ gvs [] \\ Cases_on ‘l’
1124 \\ gvs [SORTED_DEF, stringTheory.string_lt_def, stringTheory.char_lt_def]
1125QED
1126
1127Theorem SORTED_st_lex:
1128 (∀t:'a str_trie. st_sorted t ⇒ SORTED string_lt (MAP FST (st_lex t))) ∧
1129 (∀t:'a str_trie. st_sorted t ⇒ SORTED string_lt (MAP FST (st_branches t)))
1130Proof
1131 ho_match_mp_tac st_lex_ind \\ rw [st_lex_def, st_sorted_def]
1132 \\ gvs [SORTED_APPEND, transitive_string_lt, MAP_FST_MAP_CONS,
1133 SORTED_MAP_STRING]
1134 >- (CASE_TAC \\ gvs [SORTED_EQ, transitive_string_lt] \\ rw []
1135 \\ ‘y ≠ ""’ by (qspecl_then [‘t’,‘y’] mp_tac MEM_st_lex \\ gvs [])
1136 \\ Cases_on ‘y’ \\ gvs [stringTheory.string_lt_def])
1137 \\ ‘∀d rest. ORD d ≤ ORD c ⇒ st_get_cons t' d rest = NONE’ by
1138 (rw [] \\ irule st_get_cons_sorted_lt \\ gvs [] \\ rw []
1139 \\ res_tac \\ gvs [stringTheory.char_lt_def])
1140 \\ ‘∀y. MEM y (MAP FST (st_branches t')) ⇒
1141 ∃d k2. y = STRING d k2 ∧ char_lt c d’ by
1142 (rw [] \\ qspecl_then [‘t'’,‘y’] mp_tac MEM_st_lex \\ gvs [] \\ rw []
1143 \\ Cases_on ‘y’ \\ gvs []
1144 \\ CCONTR_TAC \\ gvs [st_get_def, stringTheory.char_lt_def]
1145 \\ ‘ORD h ≤ ORD c’ by DECIDE_TAC \\ res_tac \\ gvs [])
1146 \\ rw [] \\ gvs [MEM_MAP] \\ res_tac
1147 \\ gvs [stringTheory.string_lt_def]
1148QED
1149
1150Theorem ALOOKUP_eq_NONE[local]:
1151 ∀l k v k'. SORTED string_lt (MAP FST ((k,v)::l)) ∧ ¬string_lt k k' ⇒
1152 ALOOKUP l k' = NONE
1153Proof
1154 rw [] \\ gvs [SORTED_EQ, transitive_string_lt]
1155 \\ CCONTR_TAC \\ gvs [GSYM MEM_alookup]
1156 \\ first_x_assum drule \\ gvs []
1157QED
1158
1159Theorem sorted_alist_unique[local]:
1160 ∀l1 l2. SORTED string_lt (MAP FST l1) ∧ SORTED string_lt (MAP FST l2) ∧
1161 ALOOKUP l1 = ALOOKUP l2 ⇒ l1 = l2
1162Proof
1163 Induct \\ Cases_on ‘l2’ \\ gvs [] \\ strip_tac
1164 >- (Cases_on ‘h’ \\ gvs [FUN_EQ_THM]
1165 \\ first_x_assum (qspec_then ‘q’ mp_tac) \\ gvs [])
1166 >- (rw [] \\ Cases_on ‘h’ \\ gvs [FUN_EQ_THM]
1167 \\ first_x_assum (qspec_then ‘q’ mp_tac) \\ gvs [])
1168 \\ Cases_on ‘h’ \\ Cases_on ‘h'’ \\ strip_tac \\ gvs []
1169 \\ ‘q' = q’ by
1170 (CCONTR_TAC
1171 \\ ‘string_lt q' q ∨ string_lt q q'’ by
1172 metis_tac [stringTheory.string_lt_cases]
1173 \\ gvs [FUN_EQ_THM]
1174 >- (first_x_assum (qspec_then ‘q'’ mp_tac) \\ gvs []
1175 \\ qspecl_then [‘t’,‘q’,‘r’,‘q'’] mp_tac ALOOKUP_eq_NONE
1176 \\ impl_tac
1177 >- (gvs [] \\ metis_tac [stringTheory.string_lt_antisym])
1178 \\ gvs [])
1179 \\ first_x_assum (qspec_then ‘q’ mp_tac) \\ gvs []
1180 \\ qspecl_then [‘l1’,‘q'’,‘r'’,‘q’] mp_tac ALOOKUP_eq_NONE
1181 \\ impl_tac >- (gvs [] \\ metis_tac [stringTheory.string_lt_antisym])
1182 \\ gvs [])
1183 \\ gvs [FUN_EQ_THM]
1184 \\ ‘r' = r’ by (first_x_assum (qspec_then ‘q’ mp_tac) \\ gvs [])
1185 \\ gvs []
1186 \\ first_x_assum irule
1187 \\ gvs [SORTED_EQ, transitive_string_lt] \\ rw []
1188 \\ Cases_on ‘q = x’ \\ gvs []
1189 >- (Cases_on ‘ALOOKUP l1 q’ \\ Cases_on ‘ALOOKUP t q’ \\ gvs [MEM_alookup]
1190 \\ metis_tac [stringTheory.string_lt_nonrefl, optionTheory.NOT_SOME_NONE])
1191 \\ first_x_assum (qspec_then ‘x’ mp_tac) \\ gvs []
1192QED
1193
1194val _ = cv_trans st_get_nil_def;
1195val _ = cv_trans st_get_def;
1196val _ = cv_trans st_make_def;
1197val _ = cv_trans st_set_nil_def;
1198val _ = cv_trans st_set_cons_def;
1199val _ = cv_trans st_set_def;
1200val _ = cv_trans st_del_nil_def;
1201val _ = cv_trans mk_Branch_def;
1202val _ = cv_trans st_del_cons_def;
1203val _ = cv_trans st_del_def;
1204
1205Theorem cv_size_cv_fst_cv_snd[local]:
1206 ∀x. cv_size (cv_fst x) + cv_size (cv_snd x) ≤ cv_size x
1207Proof
1208 Cases \\ gvs [cvTheory.cv_size_def, cvTheory.cv_fst_def, cvTheory.cv_snd_def]
1209QED
1210
1211val _ = cv_trans_rec st_union_def
1212 (WF_REL_TAC ‘measure $ λ(x,y). cv_size x + cv_size y’
1213 \\ cv_termination_tac
1214 \\ rename [‘cv_size (cv_snd (cv_snd x)) + (cv_size (cv_snd (cv_snd y)) + 5)’]
1215 \\ qspec_then ‘x’ assume_tac cv_size_cv_fst_cv_snd
1216 \\ qspec_then ‘y’ assume_tac cv_size_cv_fst_cv_snd
1217 \\ qspec_then ‘cv_snd x’ assume_tac cv_size_cv_fst_cv_snd
1218 \\ qspec_then ‘cv_snd y’ assume_tac cv_size_cv_fst_cv_snd
1219 \\ gvs []);
1220
1221val _ = cv_trans_rec st_inter_def
1222 (WF_REL_TAC ‘measure $ λ(x,y). cv_size x + cv_size y’
1223 \\ cv_termination_tac
1224 \\ rename [‘cv_size (cv_snd (cv_snd x)) + (cv_size (cv_snd (cv_snd y)) + 5)’]
1225 \\ qspec_then ‘x’ assume_tac cv_size_cv_fst_cv_snd
1226 \\ qspec_then ‘y’ assume_tac cv_size_cv_fst_cv_snd
1227 \\ qspec_then ‘cv_snd x’ assume_tac cv_size_cv_fst_cv_snd
1228 \\ qspec_then ‘cv_snd y’ assume_tac cv_size_cv_fst_cv_snd
1229 \\ gvs []);
1230
1231val _ = cv_trans st_card_def;
1232val _ = cv_trans st_submap_def;
1233
1234val st_lex_acc_pre_def = cv_trans_pre_rec "" st_lex_acc_def
1235 (WF_REL_TAC ‘measure (λx. case x of
1236 | INL (cv,rp,acc) => cv_size cv * 2 + 1
1237 | INR (cv,rp,acc) => cv_size cv * 2)’
1238 \\ cv_termination_tac);
1239
1240Theorem st_lex_acc_pre[cv_pre]:
1241 (∀t:'a str_trie rp acc. st_lex_acc_pre t rp acc) ∧
1242 (∀t:'a str_trie rp acc. st_branches_acc_pre t rp acc)
1243Proof
1244 ho_match_mp_tac st_lex_acc_ind \\ rw [] \\ simp [Once st_lex_acc_pre_def]
1245QED
1246
1247val _ = cv_trans st_to_list_def;
1248
1249val _ = cv_trans_rec st_minus_def
1250 (WF_REL_TAC ‘measure $ λ(x,y). cv_size x + cv_size y’
1251 \\ cv_termination_tac
1252 \\ rename [‘cv_size (cv_snd (cv_snd x)) + (cv_size (cv_snd (cv_snd y)) + 5)’]
1253 \\ qspec_then ‘x’ assume_tac cv_size_cv_fst_cv_snd
1254 \\ qspec_then ‘y’ assume_tac cv_size_cv_fst_cv_snd
1255 \\ qspec_then ‘cv_snd x’ assume_tac cv_size_cv_fst_cv_snd
1256 \\ qspec_then ‘cv_snd y’ assume_tac cv_size_cv_fst_cv_snd
1257 \\ gvs []);
1258
1259(*----------------------------------------------------------*
1260 string |-> 'a
1261 *----------------------------------------------------------*)
1262
1263Definition from_string_fmap_def:
1264 from_string_fmap (f:'a -> cv) (m: string |-> 'a) =
1265 from_cv_string_fmap_str_trie f (st_sets Nothing (fmap_to_alist m))
1266End
1267
1268Definition to_string_fmap_def:
1269 to_string_fmap (t:cv -> 'a) m =
1270 alist_to_fmap (st_flat (to_str_trie t m))
1271End
1272
1273Theorem from_to_string_fmap[cv_from_to]:
1274 from_to (f0:'a -> cv) t0 ==>
1275 from_to (from_string_fmap f0) (to_string_fmap t0)
1276Proof
1277 strip_tac
1278 \\ drule (DISCH_ALL from_to_str_trie)
1279 \\ gvs [from_string_fmap_def,to_string_fmap_def,from_to_def] \\ rw []
1280 \\ gvs [finite_mapTheory.TO_FLOOKUP]
1281 \\ simp [FUN_EQ_THM] \\ gen_tac
1282 \\ DEP_REWRITE_TAC [ALOOKUP_st_flat]
1283 \\ irule_at Any st_sorted_st_sets \\ simp [st_sorted_def]
1284 \\ gvs [st_get_st_sets,st_get_def,st_get_Nothing]
1285 \\ rename [‘FLOOKUP x y’] \\ Cases_on ‘FLOOKUP x y’ \\ fs []
1286QED
1287
1288Theorem cv_rep_string_FEMPTY[cv_rep]:
1289 from_string_fmap f FEMPTY = Num 0
1290Proof
1291 EVAL_TAC \\ gvs [] \\ EVAL_TAC
1292QED
1293
1294Theorem cv_rep_string_FLOOKUP[cv_rep]:
1295 from_option f (FLOOKUP m n) =
1296 cv_st_get (from_string_fmap f m) (from_list from_char n)
1297Proof
1298 gvs [from_string_fmap_def, GSYM $ fetch "-" "cv_st_get_thm"]
1299 \\ simp [st_get_st_sets, st_get_Nothing]
1300 \\ rename [‘FLOOKUP x y’] \\ Cases_on ‘FLOOKUP x y’ \\ fs []
1301QED
1302
1303Theorem cv_rep_string_FUPDATE[cv_rep]:
1304 from_string_fmap f (m |+ (k,v)) =
1305 cv_st_set (from_string_fmap f m) (from_list from_char k) (f v)
1306Proof
1307 gvs [from_string_fmap_def,GSYM $ fetch "-" "cv_st_set_thm"] \\ AP_TERM_TAC
1308 \\ simp_tac std_ss [GSYM st_sets_def]
1309 \\ irule st_sets_eq \\ fs [finite_mapTheory.FLOOKUP_SIMP, FUN_EQ_THM]
1310QED
1311
1312val FUPDATE_LIST_pre_def = finite_mapTheory.FUPDATE_LIST_THM
1313 |> SRULE [FORALL_PROD]
1314 |> INST_TYPE [alpha |-> “:string”]
1315 |> cv_trans_pre "FUPDATE_LIST_pre";
1316
1317Theorem FUPDATE_LIST_pre[cv_pre]:
1318 ∀f ls. FUPDATE_LIST_pre f ls
1319Proof
1320 Induct_on`ls`
1321 \\ rw[Once FUPDATE_LIST_pre_def]
1322QED
1323
1324Theorem cv_rep_string_DOMSUB[cv_rep]:
1325 from_string_fmap f (m \\ k) =
1326 cv_st_del (from_string_fmap f m) (from_list from_char k)
1327Proof
1328 gvs [from_string_fmap_def, GSYM $ fetch "-" "cv_st_del_thm"]
1329 \\ AP_TERM_TAC
1330 \\ simp [st_del_st_sets, st_del_Nothing]
1331 \\ irule st_sets_eq \\ fs [finite_mapTheory.FLOOKUP_SIMP, FUN_EQ_THM]
1332 \\ gvs [ALOOKUP_FILTER,finite_mapTheory.DOMSUB_FLOOKUP_THM]
1333 \\ rw []
1334QED
1335
1336Theorem cv_rep_string_FUNION[cv_rep]:
1337 from_string_fmap f (m1 ⊌ m2) =
1338 cv_st_union (from_string_fmap f m1) (from_string_fmap f m2)
1339Proof
1340 gvs [from_string_fmap_def, GSYM $ fetch "-" "cv_st_union_thm"]
1341 \\ AP_TERM_TAC
1342 \\ irule st_sorted_st_get_eq
1343 \\ irule_at Any st_sorted_st_union
1344 \\ rw [st_sorted_st_sets, st_sorted_def]
1345 \\ DEP_REWRITE_TAC [st_get_st_union]
1346 \\ gvs [st_get_st_sets, st_get_Nothing, st_sorted_def, option_case_id,
1347 finite_mapTheory.FLOOKUP_FUNION]
1348QED
1349
1350Theorem cv_rep_string_FINTER[cv_rep]:
1351 from_string_fmap f (FINTER m1 m2) =
1352 cv_st_inter (from_string_fmap f m1) (from_string_fmap g m2)
1353Proof
1354 gvs [from_string_fmap_def, GSYM $ fetch "-" "cv_st_inter_thm"]
1355 \\ AP_TERM_TAC
1356 \\ irule st_sorted_st_get_eq
1357 \\ irule_at Any st_sorted_st_inter
1358 \\ rw [st_sorted_st_sets, st_sorted_def]
1359 \\ DEP_REWRITE_TAC [st_get_st_inter]
1360 \\ gvs [st_get_st_sets, st_get_Nothing, st_sorted_def, option_case_id,
1361 finite_mapTheory.FLOOKUP_FINTER]
1362QED
1363
1364Theorem cv_rep_string_FMINUS[cv_rep]:
1365 from_string_fmap f (FMINUS m1 m2) =
1366 cv_st_minus (from_string_fmap f m1) (from_string_fmap g m2)
1367Proof
1368 gvs [from_string_fmap_def, GSYM $ fetch "-" "cv_st_minus_thm"]
1369 \\ AP_TERM_TAC
1370 \\ irule st_sorted_st_get_eq
1371 \\ irule_at Any st_sorted_st_minus
1372 \\ rw [st_sorted_st_sets, st_sorted_def]
1373 \\ DEP_REWRITE_TAC [st_get_st_minus]
1374 \\ gvs [st_get_st_sets, st_get_Nothing, st_sorted_def, option_case_id,
1375 finite_mapTheory.FLOOKUP_FMINUS]
1376QED
1377
1378Theorem cv_rep_string_FCARD[cv_rep]:
1379 Num (FCARD m) = cv_st_card (from_string_fmap f m)
1380Proof
1381 gvs [from_string_fmap_def, GSYM $ fetch "-" "cv_st_card_thm"]
1382 \\ qmatch_goalsub_abbrev_tac ‘st_card t’
1383 \\ ‘st_sorted t’ by gvs [Abbr‘t’]
1384 \\ ‘ALOOKUP (st_flat t) = FLOOKUP m’ by
1385 (gvs [FUN_EQ_THM] \\ rw []
1386 \\ DEP_REWRITE_TAC [ALOOKUP_st_flat]
1387 \\ gvs [Abbr‘t’, st_get_st_sets]
1388 \\ CASE_TAC \\ gvs [])
1389 \\ ‘∀x. MEM x (MAP FST (st_flat t)) ⇔ ALOOKUP (st_flat t) x ≠ NONE’ by
1390 gvs [ALOOKUP_NONE]
1391 \\ ‘FDOM m = set (MAP FST (st_flat t))’ by
1392 (gvs [pred_setTheory.EXTENSION]
1393 \\ gvs [finite_mapTheory.FLOOKUP_DEF] \\ rw [])
1394 \\ gvs [st_card_st_flat, finite_mapTheory.FCARD_DEF]
1395 \\ DEP_REWRITE_TAC [ALL_DISTINCT_CARD_LIST_TO_SET]
1396 \\ gvs [ALL_DISTINCT_st_flat]
1397QED
1398
1399val submap_lemma = cv_rep_for [] “st_submap t u” |> DISCH_ALL;
1400
1401Theorem cv_rep_string_SUBMAP[cv_rep]:
1402 from_to f_a t_a ⇒
1403 cv_rep T (cv_st_submap (from_string_fmap f_a m1) (from_string_fmap f_a m2))
1404 b2c (m1 ⊑ m2)
1405Proof
1406 qsuff_tac ‘m1 ⊑ m2 ⇔ st_submap (st_sets Nothing (fmap_to_alist m1))
1407 (st_sets Nothing (fmap_to_alist m2))’
1408 >- (simp [from_string_fmap_def]
1409 \\ mp_tac (submap_lemma |> Q.GENL [‘t’,‘u’]
1410 |> Q.SPECL [‘st_sets Nothing (fmap_to_alist m1)’,
1411 ‘st_sets Nothing (fmap_to_alist m2)’])
1412 \\ fs [])
1413 \\ DEP_REWRITE_TAC [st_submap_thm]
1414 \\ gvs [st_get_st_sets, option_case_id, finite_mapTheory.SUBMAP_FLOOKUP_EQN]
1415QED
1416
1417(* the entries of a finite map, listed in increasing order of the keys *)
1418Definition fmap_to_sorted_list_def:
1419 fmap_to_sorted_list m =
1420 @l. ALOOKUP l = FLOOKUP m ∧ SORTED string_lt (MAP FST l)
1421End
1422
1423Theorem fmap_to_sorted_list_eq:
1424 ALOOKUP l = FLOOKUP m ∧ SORTED string_lt (MAP FST l) ⇒
1425 fmap_to_sorted_list m = l
1426Proof
1427 rw [fmap_to_sorted_list_def] \\ SELECT_ELIM_TAC \\ rw []
1428 >- (qexists_tac ‘l’ \\ gvs [])
1429 \\ irule sorted_alist_unique \\ gvs []
1430QED
1431
1432Theorem fmap_to_sorted_list_thm:
1433 ALOOKUP (fmap_to_sorted_list m) = FLOOKUP m ∧
1434 SORTED string_lt (MAP FST (fmap_to_sorted_list m))
1435Proof
1436 ‘∃l. ALOOKUP l = FLOOKUP m ∧ SORTED string_lt (MAP FST l)’ by
1437 (qexists_tac ‘st_lex (st_sets Nothing (fmap_to_alist m))’
1438 \\ qmatch_goalsub_abbrev_tac ‘st_lex t’
1439 \\ ‘st_sorted t’ by gvs [Abbr‘t’]
1440 \\ conj_tac
1441 >- (gvs [FUN_EQ_THM] \\ rw []
1442 \\ DEP_REWRITE_TAC [ALOOKUP_st_lex] \\ gvs [Abbr‘t’, st_get_st_sets]
1443 \\ CASE_TAC \\ gvs [])
1444 \\ irule (CONJUNCT1 SORTED_st_lex) \\ gvs [])
1445 \\ gvs [fmap_to_sorted_list_def] \\ SELECT_ELIM_TAC \\ rw []
1446 \\ metis_tac []
1447QED
1448
1449Theorem LENGTH_fmap_to_sorted_list:
1450 LENGTH (fmap_to_sorted_list m) = FCARD m
1451Proof
1452 strip_assume_tac fmap_to_sorted_list_thm
1453 \\ ‘ALL_DISTINCT (MAP FST (fmap_to_sorted_list m))’ by
1454 (qspec_then ‘string_lt’ mp_tac (GEN_ALL SORTED_ALL_DISTINCT)
1455 \\ impl_tac
1456 >- gvs [transitive_string_lt, relationTheory.irreflexive_def,
1457 stringTheory.string_lt_nonrefl]
1458 \\ disch_then irule \\ gvs [])
1459 \\ ‘FDOM m = set (MAP FST (fmap_to_sorted_list m))’ by
1460 (‘∀x. MEM x (MAP FST (fmap_to_sorted_list m)) ⇔
1461 ALOOKUP (fmap_to_sorted_list m) x ≠ NONE’ by gvs [ALOOKUP_NONE]
1462 \\ gvs [pred_setTheory.EXTENSION]
1463 \\ gvs [finite_mapTheory.FLOOKUP_DEF] \\ rw [])
1464 \\ gvs [finite_mapTheory.FCARD_DEF]
1465 \\ DEP_REWRITE_TAC [ALL_DISTINCT_CARD_LIST_TO_SET] \\ gvs []
1466QED
1467
1468Theorem cv_rep_string_fmap_to_sorted_list[cv_rep]:
1469 from_list (from_pair (from_list from_char) f) (fmap_to_sorted_list m) =
1470 cv_st_to_list (from_string_fmap f m)
1471Proof
1472 gvs [from_string_fmap_def, GSYM $ fetch "-" "cv_st_to_list_thm"]
1473 \\ AP_TERM_TAC
1474 \\ gvs [st_to_list_thm]
1475 \\ irule fmap_to_sorted_list_eq
1476 \\ qmatch_goalsub_abbrev_tac ‘st_lex t’
1477 \\ ‘st_sorted t’ by gvs [Abbr‘t’]
1478 \\ conj_tac
1479 >- (gvs [FUN_EQ_THM] \\ rw []
1480 \\ DEP_REWRITE_TAC [ALOOKUP_st_lex] \\ gvs [Abbr‘t’, st_get_st_sets]
1481 \\ CASE_TAC \\ gvs [])
1482 \\ irule (CONJUNCT1 SORTED_st_lex) \\ gvs []
1483QED