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 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 x t1 t2 = if t1 = Nothing then t2 else Branch x t1 t2
86End
87
88Definition st_del_cons_def:
89  st_del_cons Nothing x xs = Nothing ∧
90  st_del_cons (Just z) x xs = Just z ∧
91  st_del_cons (Branch c subtrie rest) x xs =
92    if c > x then
93      Branch c subtrie rest
94    else if c < x then
95      Branch c subtrie (st_del_cons rest x xs)
96    else
97      mk_Branch c (case xs of
98                   | [] => st_del_nil subtrie
99                   | (x::xs) => st_del_cons subtrie x xs) rest
100End
101
102Definition st_del_def[simp]:
103  st_del t [] = st_del_nil t ∧
104  st_del t (x::xs) = st_del_cons t x xs
105End
106
107(* verification *)
108
109Definition st_flat_def:
110  st_flat Nothing = [] ∧
111  st_flat (Just a) = [("",a)] ∧
112  st_flat (Branch c t1 t2) = MAP (λ(k,v). (c::k,v)) (st_flat t1) ++ st_flat t2
113End
114
115Definition st_sorted_def:
116  st_sorted Nothing = T ∧
117  st_sorted (Just x) = T ∧
118  st_sorted (Branch c t1 t2) = (t1 ≠ Nothing ∧ st_sorted t1 ∧
119                                st_sorted t2 ∧
120                                ∀c' t1' t2'. t2 = Branch c' t1' t2' ⇒ c < c')
121End
122
123Theorem st_sorted_base[simp]:
124  st_sorted Nothing ∧ st_sorted (Just x)
125Proof
126  rw[st_sorted_def]
127QED
128
129Theorem st_make_not_nothing[simp]:
130  st_make xs y ≠ Nothing
131Proof
132  Cases_on`xs` \\ rw[]
133QED
134
135Theorem st_sorted_st_make[simp]:
136  ∀xs y. st_sorted (st_make xs y)
137Proof
138  Induct \\ rw[st_make_def, st_sorted_def]
139QED
140
141Theorem st_get_st_make:
142  ∀xs y n. st_get (st_make xs y) n = if n = xs then SOME y else NONE
143Proof
144  Induct \\ rw[st_get_def, st_make_def, st_get_nil_def,
145               stringTheory.char_lt_def, stringTheory.char_gt_def] >>
146  qmatch_goalsub_rename_tac`st_get _ ls` >>
147  Cases_on`ls` >> gvs[st_get_def, st_get_nil_def] >> rw[] >>
148  gvs[stringTheory.char_lt_def, stringTheory.char_gt_def] >>
149  qpat_x_assum`_ <> _`mp_tac \\ rw[] >>
150  irule $ iffLR stringTheory.ORD_11 >> simp[]
151QED
152
153Theorem st_get_Nothing[simp]:
154  ∀xs. st_get Nothing xs = NONE
155Proof
156  Cases \\ fs [st_get_def, st_get_nil_def]
157QED
158
159Theorem st_del_Nothing[simp]:
160  ∀xs. st_del Nothing xs = Nothing
161Proof
162  Cases \\ fs [st_del_def, st_del_nil_def, st_del_cons_def]
163QED
164
165Theorem st_sorted_st_set_nil[simp]:
166  ∀t y. st_sorted t ⇒ st_sorted (st_set_nil t y)
167Proof
168  Induct \\ rw [st_set_nil_def, st_sorted_def] >>
169  qmatch_asmsub_rename_tac`st_set_nil tt _ = _` >>
170  Cases_on`tt` \\ gvs[st_set_nil_def]
171QED
172
173Theorem st_set_nil_not_nothing[simp]:
174  st_set_nil t y ≠ Nothing
175Proof
176  Cases_on`t` \\ rw[]
177QED
178
179Theorem st_set_cons_not_nothing[simp]:
180  st_set_cons t x xs y ≠ Nothing
181Proof
182  Cases_on`t` \\ rw[st_set_cons_def]
183QED
184
185Theorem st_sorted_st_set_cons[simp]:
186  ∀t x xs y. st_sorted t ⇒ st_sorted (st_set_cons t x xs y)
187Proof
188  Induct \\ rw[st_set_cons_def, st_sorted_def]
189  >> gvs[stringTheory.char_lt_def, stringTheory.char_gt_def]
190  >- (
191    qmatch_asmsub_rename_tac`st_set_cons tt _ _ _ = _` >>
192    Cases_on`tt` \\ gvs[st_set_cons_def] >>
193    gvs[stringTheory.char_lt_def, stringTheory.char_gt_def] >>
194    qmatch_asmsub_rename_tac`ORD c2 > _` >>
195    qmatch_goalsub_rename_tac`_ < ORD c1` >>
196    Cases_on`c1 = c2` >> gvs[] >>
197    gvs[CaseEq"bool"]) >>
198  CASE_TAC \\ gvs[]
199QED
200
201Theorem st_sorted_st_sets[simp]:
202  st_sorted t ⇒ st_sorted (st_sets t xs)
203Proof
204  Induct_on`xs` \\ simp[st_sets_def] >>
205  Cases >> simp[st_sets_def] >> rw[] >>
206  qmatch_goalsub_rename_tac`st_set _ s _` >>
207  Cases_on`s` >> gvs[st_set_def]
208QED
209
210(* When st_sorted t and t = Branch c t1 t2, looking up (h::rest) where
211   h < c should give NONE, because all branches in the chain have chars ≥ c *)
212Theorem st_get_cons_sorted_lt:
213  ∀t h rest. st_sorted t ⇒
214    (∀c' t1' t2'. t = Branch c' t1' t2' ⇒ h < c') ⇒
215    st_get_cons t h rest = NONE
216Proof
217  Induct \\ rw [st_get_def, st_sorted_def]
218  \\ gvs [stringTheory.char_lt_def, stringTheory.char_gt_def]
219  \\ first_x_assum irule \\ rw [st_sorted_def]
220  \\ res_tac \\ fs []
221QED
222
223Theorem ALOOKUP_MAP_CONS_CONS[local]:
224  ALOOKUP (MAP (λ(k,v). (c::k,v)) ls) (d::rest) =
225  if c = d then ALOOKUP ls rest else NONE
226Proof
227  Induct_on`ls` \\ rw[] \\ pairarg_tac \\ gvs[]
228QED
229
230Theorem ALOOKUP_st_flat:
231  st_sorted t ⇒ ALOOKUP (st_flat t) n = st_get t n
232Proof
233  qid_spec_tac `n` \\ Induct_on `t`
234  \\ rw [st_flat_def, st_sorted_def]
235  >- rw[st_get_def, st_get_nil_def]
236  >- (Cases_on `n` \\ fs [st_get_def, st_get_nil_def])
237  \\ Cases_on `n`
238  >- (
239    simp [ALOOKUP_APPEND, st_get_def, st_get_nil_def] >>
240    CASE_TAC >> imp_res_tac ALOOKUP_MEM >>
241    gvs[MEM_MAP, EXISTS_PROD] ) >>
242  simp [ALOOKUP_APPEND, st_get_def, ALOOKUP_MAP_CONS_CONS] >>
243  rw []
244  \\ gvs [stringTheory.char_lt_def, stringTheory.char_gt_def]
245  >- (
246    CASE_TAC >>
247    irule st_get_cons_sorted_lt >>
248    rw[stringTheory.char_lt_def] )
249  >- (
250    irule st_get_cons_sorted_lt >>
251    rw[stringTheory.char_lt_def] >>
252    CCONTR_TAC >> gvs[NOT_LESS] ) >>
253  `ORD c <> ORD h` by simp[stringTheory.ORD_11] >>
254  gvs[]
255QED
256
257Theorem st_get_nil_st_set_nil[simp]:
258  ∀t y. st_get_nil (st_set_nil t y) = SOME y
259Proof
260  Induct \\ rw [st_set_nil_def, st_get_nil_def]
261QED
262
263Theorem st_get_cons_st_set_nil[simp]:
264  ∀t y x xs. st_get_cons (st_set_nil t y) x xs = st_get_cons t x xs
265Proof
266  Induct \\ rw [st_set_nil_def, st_get_def]
267QED
268
269Theorem st_get_nil_st_set_cons[simp]:
270  ∀t x xs y. st_get_nil (st_set_cons t x xs y) = st_get_nil t
271Proof
272  Induct \\ rw [st_set_cons_def, st_get_nil_def]
273  \\ gvs [st_get_nil_def]
274QED
275
276Theorem st_get_nil_st_make:
277  ∀xs y. st_get_nil (st_make xs y) = if xs = [] then SOME y else NONE
278Proof
279  Cases \\ rw [st_make_def, st_get_nil_def]
280QED
281
282Theorem st_get_cons_st_set_cons:
283  ∀t x xs y h rest.
284    st_sorted t ⇒
285    st_get_cons (st_set_cons t x xs y) h rest =
286      if h = x ∧ rest = xs then SOME y
287      else st_get_cons t h rest
288Proof
289  Induct \\ rw[st_set_cons_def, st_get_def]
290  \\ gvs [stringTheory.char_lt_def, stringTheory.char_gt_def, st_sorted_def]
291  \\ gvs[st_get_st_make]
292  \\ TRY (
293    rw[] >> first_x_assum irule
294    \\ irule $ iffLR stringTheory.ORD_11
295    \\ gvs[] ) >>
296  CASE_TAC \\ gvs[st_get_def] >>
297  `ORD c = ORD x ∧ ORD c = ORD h` by gvs[] >>
298  gvs[stringTheory.ORD_11]
299  >- (Cases_on`rest` \\ gvs[st_get_def]) >>
300  Cases_on`rest=[]` \\ gvs[st_get_def] >>
301  Cases_on`rest` >- gvs[] >>
302  simp[st_get_def] >> IF_CASES_TAC >> simp[] >> gvs[]
303QED
304
305Theorem st_get_st_set:
306  ∀t k v n. st_sorted t ⇒
307    st_get (st_set t k v) n = if n = k then SOME v else st_get t n
308Proof
309  rpt strip_tac
310  \\ Cases_on `k` \\ Cases_on `n`
311  \\ fs [st_set_def, st_get_def,
312         st_get_nil_st_set_nil, st_get_cons_st_set_nil,
313         st_get_nil_st_set_cons, st_get_cons_st_set_cons]
314  \\ rw [] \\ gvs []
315QED
316
317Theorem st_get_st_sets:
318  st_sorted t ⇒
319  st_get (st_sets t xs) n = case ALOOKUP xs n of NONE => st_get t n | res => res
320Proof
321  strip_tac
322  \\ Induct_on `xs` \\ fs [st_sets_def, FORALL_PROD]
323  \\ rw []
324  \\ DEP_REWRITE_TAC [st_get_st_set]
325  \\ rw [] \\ fs []
326QED
327
328Theorem st_sorted_not_Nothing_get:
329  ∀t. st_sorted t ∧ t ≠ Nothing ⇒ ∃k v. st_get t k = SOME v
330Proof
331  Induct \\ rw [st_sorted_def]
332  >- (qexists_tac `[]` \\ simp [st_get_def, st_get_nil_def])
333  >- (rename [`st_get (Branch c t1 t2)`]
334      \\ first_x_assum (drule_all_then strip_assume_tac)
335      \\ qexists_tac `c::k` \\ simp [st_get_def]
336      \\ gvs [stringTheory.char_lt_def, stringTheory.char_gt_def])
337QED
338
339Theorem st_sorted_st_get_eq:
340  ∀t1 t2. st_sorted t1 ∧ st_sorted t2 ∧
341  (∀n. st_get t1 n = st_get t2 n) ⇒ t1 = t2
342Proof
343  Induct
344  >- (Cases \\ rw [st_sorted_def]
345      >- (qexists_tac`[]` \\ rw[st_get_def]) >>
346      CCONTR_TAC \\ gvs[] >>
347      drule_all st_sorted_not_Nothing_get >>
348      simp[] >> rpt strip_tac >>
349      first_x_assum(qspec_then`c::k`mp_tac) >>
350      simp[st_get_def, stringTheory.char_gt_def, stringTheory.char_lt_def])
351  >- (Cases_on`t2` \\ rw [st_sorted_def]
352      >- (qexists_tac`[]` \\ rw[st_get_def])
353      >- (first_x_assum (qspec_then `[]` mp_tac)
354          \\ rw [st_get_def, st_get_nil_def]) >>
355      CCONTR_TAC \\ gvs[] >>
356      drule_all st_sorted_not_Nothing_get \\ rw[] >>
357      first_x_assum (qspec_then `c::k` mp_tac)
358      \\ simp [st_get_def, st_get_nil_def]
359      \\ gvs [stringTheory.char_lt_def, stringTheory.char_gt_def]) >>
360  Cases_on`t2` >> simp[st_sorted_def]
361  >- (
362    CCONTR_TAC \\ gvs[] >>
363    drule_all st_sorted_not_Nothing_get >> rw[] >>
364    first_x_assum (qspec_then `c::k` mp_tac)
365    \\ simp [st_get_def, st_get_nil_def]
366    \\ gvs [stringTheory.char_lt_def, stringTheory.char_gt_def])
367  >- (
368    CCONTR_TAC \\ gvs[] >>
369    drule_all st_sorted_not_Nothing_get >> rw[] >>
370    first_x_assum (qspec_then `c::k` mp_tac)
371    \\ simp [st_get_def, st_get_nil_def]
372    \\ gvs [stringTheory.char_lt_def, stringTheory.char_gt_def]) >>
373  gen_tac >> strip_tac >>
374  Cases_on`char_lt c c'`
375  >- (
376    qspec_then`s`mp_tac st_sorted_not_Nothing_get >>
377    impl_tac >- rw[] >> strip_tac >>
378    first_assum(qspec_then`c::k`mp_tac) >>
379    simp_tac(srw_ss())[st_get_def] >>
380    gvs[stringTheory.char_lt_def, stringTheory.char_gt_def] ) >>
381  Cases_on`char_lt c' c`
382  >- (
383    qspec_then`t1`mp_tac st_sorted_not_Nothing_get >>
384    impl_tac >- rw[] >> strip_tac >>
385    first_assum(qspec_then`c'::k`mp_tac) >>
386    simp_tac(srw_ss())[st_get_def] >>
387    gvs[stringTheory.char_lt_def, stringTheory.char_gt_def] ) >>
388  `ORD c = ORD c'` by gvs[stringTheory.char_lt_def] >>
389  gvs[stringTheory.ORD_11] >>
390  conj_tac
391  >- (
392    first_x_assum irule \\ simp[] >>
393    gen_tac >>
394    first_x_assum(qspec_then`c::n`mp_tac) >>
395    simp[st_get_def, stringTheory.char_gt_def] ) >>
396  first_x_assum irule \\ simp[] >> gen_tac >>
397  first_x_assum(qspec_then`n`mp_tac) >>
398  Cases_on`n` \\ simp[st_get_def] >>
399  Cases_on`char_lt c h` >> gvs[]
400  >- gvs[stringTheory.char_lt_def, stringTheory.char_gt_def] >>
401  strip_tac >>
402  gvs[stringTheory.char_lt_def, stringTheory.char_gt_def] >>
403  qmatch_goalsub_abbrev_tac `sg1 = sg2` >>
404  `sg1 = NONE ∧ sg2 = NONE` suffices_by rw[] >>
405  unabbrev_all_tac >>
406  conj_tac >> irule st_get_cons_sorted_lt >> gvs[] >>
407  rpt strip_tac >> first_x_assum drule >>
408  gvs[stringTheory.char_lt_def, stringTheory.char_gt_def]
409QED
410
411Theorem st_sets_eq:
412  st_sorted t ⇒ ALOOKUP xs = ALOOKUP ys ⇒ st_sets t xs = st_sets t ys
413Proof
414  rw []
415  \\ irule st_sorted_st_get_eq
416  \\ rw []
417  \\ DEP_REWRITE_TAC [st_get_st_sets] \\ fs []
418QED
419
420Theorem st_sorted_st_del_nil[simp]:
421  ∀t. st_sorted t ⇒ st_sorted (st_del_nil t)
422Proof
423  Induct \\ rw [st_del_nil_def, st_sorted_def] >>
424  Cases_on`t'` \\ gvs[]
425QED
426
427Theorem st_sorted_mk_Branch:
428  st_sorted (mk_Branch c t1 t2) ⇔
429    st_sorted t1 ∧ st_sorted t2 ∧
430    (t1 ≠ Nothing ⇒ ∀c' t1' t2'. t2 = Branch c' t1' t2' ⇒ c < c')
431Proof
432  rw [mk_Branch_def, st_sorted_def] \\ rw [] \\ eq_tac \\ rw []
433QED
434
435Theorem st_del_cons_not_Branch_Nothing:
436  ∀t x xs c rest. st_sorted t ⇒
437    st_del_cons t x xs ≠ Branch c Nothing rest
438Proof
439  Induct \\ rw [st_del_cons_def, st_sorted_def]
440  \\ gvs [mk_Branch_def, AllCaseEqs()]
441  \\ gvs[stringTheory.char_gt_def, stringTheory.char_lt_def]
442  \\ `ORD c = ORD x` by gvs[]
443  \\ gvs[stringTheory.ORD_11]
444  \\ CCONTR_TAC \\ gvs[]
445  \\ gvs[Once(oneline st_del_nil_def),AllCaseEqs(),st_sorted_def]
446QED
447
448Theorem st_sorted_st_del_cons[simp]:
449  ∀t x xs. st_sorted t ⇒ st_sorted (st_del_cons t x xs)
450Proof
451  Induct \\ rw [st_del_cons_def, st_sorted_def]
452  \\ gvs [st_sorted_def, st_sorted_mk_Branch]
453  \\ TRY (CASE_TAC \\ gvs [])
454  \\ pop_assum mp_tac
455  \\ simp[Once(oneline st_del_cons_def)]
456  \\ BasicProvers.TOP_CASE_TAC \\ gvs[]
457  \\ gvs[stringTheory.char_lt_def, stringTheory.char_gt_def]
458  \\ rw[] \\ gvs[]
459  \\ gvs[mk_Branch_def, AllCaseEqs(), st_sorted_def]
460  \\ Cases_on`s` \\ gvs[stringTheory.char_lt_def]
461QED
462
463Theorem st_sorted_st_del[simp]:
464  ∀t k. st_sorted t ⇒ st_sorted (st_del t k)
465Proof
466  rpt strip_tac \\ Cases_on `k`
467  \\ fs [st_del_def]
468QED
469
470Theorem st_get_nil_st_del_nil[simp]:
471  ∀t. st_get_nil (st_del_nil t) = NONE
472Proof
473  Induct \\ rw [st_del_nil_def, st_get_nil_def]
474QED
475
476Theorem st_get_cons_st_del_nil[simp]:
477  ∀t x xs. st_get_cons (st_del_nil t) x xs = st_get_cons t x xs
478Proof
479  Induct \\ rw [st_del_nil_def, st_get_def]
480QED
481
482Theorem st_get_nil_mk_Branch[simp]:
483  ∀c t1 t2. st_get_nil (mk_Branch c t1 t2) = st_get_nil t2
484Proof
485  rw [mk_Branch_def, st_get_nil_def]
486QED
487
488Theorem st_get_cons_mk_Branch:
489  ∀c t1 t2 x xs.
490    st_get_cons (mk_Branch c t1 t2) x xs =
491    if t1 = Nothing then st_get_cons t2 x xs
492    else st_get_cons (Branch c t1 t2) x xs
493Proof
494  rw [mk_Branch_def]
495QED
496
497Theorem st_get_nil_st_del_cons[simp]:
498  ∀t x xs. st_get_nil (st_del_cons t x xs) = st_get_nil t
499Proof
500  Induct \\ rw [st_del_cons_def, st_get_nil_def]
501  \\ gvs [st_get_nil_def, mk_Branch_def]
502QED
503
504Theorem st_get_cons_st_del_cons:
505  ∀t x xs h rest.
506    st_sorted t ⇒
507    st_get_cons (st_del_cons t x xs) h rest =
508      if h = x ∧ rest = xs then NONE
509      else st_get_cons t h rest
510Proof
511  Induct
512  \\ simp[st_del_cons_def, st_get_def]
513  \\ rpt gen_tac \\ strip_tac
514  \\ gvs [stringTheory.char_lt_def, stringTheory.char_gt_def, st_sorted_def]
515  \\ rw [st_get_cons_mk_Branch, st_get_def]
516  \\ gvs [stringTheory.char_lt_def, stringTheory.char_gt_def]
517  \\ CASE_TAC \\ rw[]
518  \\ gvs [st_get_def, st_get_nil_st_del_nil,
519          st_get_cons_st_del_nil, st_get_nil_def]
520  \\ TRY (
521    simp[Once(oneline st_get_def)]
522    \\ CASE_TAC
523    \\ simp[stringTheory.char_lt_def, stringTheory.char_gt_def]
524    \\ gvs[] \\ NO_TAC) >>
525  gvs[NOT_LESS, NOT_GREATER] >>
526  imp_res_tac LE_ANTISYM >>
527  imp_res_tac stringTheory.ORD_11 >>
528  rpt BasicProvers.VAR_EQ_TAC >> gvs[]
529  >- (
530    Cases_on`t` \\ gvs[st_get_def] >>
531    drule st_get_cons_sorted_lt >>
532    simp[stringTheory.char_lt_def] >>
533    Cases_on`rest` \\ rw[st_get_def] )
534  >- ( Cases_on`rest` \\ rw[st_get_def] )
535  >- (
536    qmatch_goalsub_abbrev_tac`sg1 = sg2` \\
537    `sg1 = NONE ∧ sg2 = NONE` suffices_by rw[] \\
538    unabbrev_all_tac \\
539    conj_tac >- ( irule st_get_cons_sorted_lt \\ rw[stringTheory.char_lt_def] )
540    >> Cases_on`rest` \\ gvs[st_get_def]
541    >- (
542      irule EQ_TRANS
543      \\ `st_get_nil Nothing = NONE` by simp[]
544      \\ goal_assum $ drule_at Any
545      \\ qpat_assum`_ = Nothing`(SUBST1_TAC o SYM)
546      \\ simp[] )
547    \\ qmatch_asmsub_rename_tac`st_del_cons t h1 t2`
548    \\ last_x_assum(qspecl_then[`h1`,`t2`]mp_tac)
549    \\ simp[]
550    \\ qmatch_goalsub_rename_tac`st_get_cons t h t3`
551    \\ disch_then(qspecl_then[`h`,`t3`]mp_tac)
552    \\ rw[st_get_def] ) >>
553  Cases_on`rest` \\ gvs[st_get_def] >> rw[]
554QED
555
556Theorem st_get_st_del:
557  ∀t k n. st_sorted t ⇒
558    st_get (st_del t k) n = if n = k then NONE else st_get t n
559Proof
560  rpt strip_tac
561  \\ Cases_on `k` \\ Cases_on `n`
562  \\ fs [st_del_def, st_get_def,
563         st_get_nil_st_del_nil, st_get_cons_st_del_nil,
564         st_get_nil_st_del_cons, st_get_cons_st_del_cons]
565  \\ rw [] \\ gvs []
566QED
567
568Theorem st_sorted_st_set[simp]:
569  st_sorted t ⇒
570  st_sorted (st_set t m x)
571Proof
572  Cases_on`m` \\ rw[]
573QED
574
575Theorem st_del_st_set:
576  st_sorted t ⇒
577  st_del (st_set t n x) m = if m = n then st_del t m
578    else st_set (st_del t m) n x
579Proof
580  rw []
581  \\ irule st_sorted_st_get_eq \\ rw []
582  \\ DEP_REWRITE_TAC [st_get_st_del, st_get_st_set]
583  \\ rw [] \\ gvs []
584QED
585
586Theorem st_del_st_sets:
587  st_sorted t ⇒
588  st_del (st_sets t xs) n = st_sets (st_del t n) (FILTER (λ(k,v). k ≠ n) xs)
589Proof
590  strip_tac
591  \\ Induct_on `xs`
592  \\ fs [st_sets_def, FORALL_PROD]
593  \\ rw []
594  \\ DEP_REWRITE_TAC [st_del_st_set]
595  \\ rw []
596  \\ simp [st_sets_def]
597QED
598
599val _ = cv_trans st_get_nil_def;
600val _ = cv_trans st_get_def;
601val _ = cv_trans st_make_def;
602val _ = cv_trans st_set_nil_def;
603val _ = cv_trans st_set_cons_def;
604val _ = cv_trans st_set_def;
605val _ = cv_trans st_del_nil_def;
606val _ = cv_trans mk_Branch_def;
607val _ = cv_trans st_del_cons_def;
608val _ = cv_trans st_del_def;
609
610(*----------------------------------------------------------*
611   string |-> 'a
612 *----------------------------------------------------------*)
613
614Definition from_string_fmap_def:
615  from_string_fmap (f:'a -> cv) (m: string |-> 'a) =
616    from_cv_string_fmap_str_trie f (st_sets Nothing (fmap_to_alist m))
617End
618
619Definition to_string_fmap_def:
620  to_string_fmap (t:cv -> 'a) m =
621    alist_to_fmap (st_flat (to_str_trie t m))
622End
623
624Theorem from_to_string_fmap[cv_from_to]:
625  from_to (f0:'a -> cv) t0 ==>
626  from_to (from_string_fmap f0) (to_string_fmap t0)
627Proof
628  strip_tac
629  \\ drule (DISCH_ALL from_to_str_trie)
630  \\ gvs [from_string_fmap_def,to_string_fmap_def,from_to_def] \\ rw []
631  \\ gvs [finite_mapTheory.TO_FLOOKUP]
632  \\ simp [FUN_EQ_THM] \\ gen_tac
633  \\ DEP_REWRITE_TAC [ALOOKUP_st_flat]
634  \\ irule_at Any st_sorted_st_sets \\ simp [st_sorted_def]
635  \\ gvs [st_get_st_sets,st_get_def,st_get_Nothing]
636  \\ rename [‘FLOOKUP x y’] \\ Cases_on ‘FLOOKUP x y’ \\ fs []
637QED
638
639Theorem cv_rep_string_FEMPTY[cv_rep]:
640  from_string_fmap f FEMPTY = Num 0
641Proof
642  EVAL_TAC \\ gvs [] \\ EVAL_TAC
643QED
644
645Theorem cv_rep_string_FLOOKUP[cv_rep]:
646  from_option f (FLOOKUP m n) =
647  cv_st_get (from_string_fmap f m) (from_list from_char n)
648Proof
649  gvs [from_string_fmap_def, GSYM $ fetch "-" "cv_st_get_thm"]
650  \\ simp [st_get_st_sets, st_get_Nothing]
651  \\ rename [‘FLOOKUP x y’] \\ Cases_on ‘FLOOKUP x y’ \\ fs []
652QED
653
654Theorem cv_rep_string_FUPDATE[cv_rep]:
655  from_string_fmap f (m |+ (k,v)) =
656  cv_st_set (from_string_fmap f m) (from_list from_char k) (f v)
657Proof
658  gvs [from_string_fmap_def,GSYM $ fetch "-" "cv_st_set_thm"] \\ AP_TERM_TAC
659  \\ simp_tac std_ss [GSYM st_sets_def]
660  \\ irule st_sets_eq \\ fs [finite_mapTheory.FLOOKUP_SIMP, FUN_EQ_THM]
661QED
662
663val FUPDATE_LIST_pre_def = finite_mapTheory.FUPDATE_LIST_THM
664 |> SRULE [FORALL_PROD]
665 |> INST_TYPE [alpha |-> “:string”]
666 |> cv_trans_pre "FUPDATE_LIST_pre";
667
668Theorem FUPDATE_LIST_pre[cv_pre]:
669  ∀f ls. FUPDATE_LIST_pre f ls
670Proof
671  Induct_on`ls`
672  \\ rw[Once FUPDATE_LIST_pre_def]
673QED
674
675Theorem cv_rep_string_DOMSUB[cv_rep]:
676  from_to f t ⇒
677  from_string_fmap f (m \\ k) =
678  cv_st_del (from_string_fmap f m) (from_list from_char k)
679Proof
680  rw[from_string_fmap_def]
681  \\ drule (GSYM (theorem "cv_st_del_thm" |> DISCH_ALL))
682  \\ simp [] \\ disch_then kall_tac
683  \\ AP_TERM_TAC
684  \\ simp [st_del_st_sets, st_del_Nothing]
685  \\ irule st_sets_eq \\ fs [finite_mapTheory.FLOOKUP_SIMP, FUN_EQ_THM]
686  \\ gvs [ALOOKUP_FILTER,finite_mapTheory.DOMSUB_FLOOKUP_THM]
687  \\ rw []
688QED