cv_stdScript.sml

1(*
2  Apply cv translator to standard theories list, pair, sptree, etc.
3*)
4Theory cv_std
5Ancestors
6  cv cv_type arithmetic words byte cv_rep cv_prim pair list option sum
7  alist indexedLists rich_list sptree finite_set
8Libs
9  dep_rewrite wordsLib cv_typeLib cv_repLib cv_transLib
10
11Overload Num[local] = “cv$Num”
12Overload Pair[local] = “cv$Pair”
13
14(*----------------------------------------------------------*
15   pair
16 *----------------------------------------------------------*)
17
18val _ = cv_rep_for [] “(x:'a, y:'b)”
19
20Theorem cv_FST[cv_rep]:
21  f_a (FST v) = cv_fst ((from_pair f_a f_b) (v: 'a # 'b))
22Proof
23  Cases_on ‘v’ \\ gvs [from_pair_def]
24QED
25
26Theorem cv_SND[cv_rep]:
27  f_b (SND v) = cv_snd ((from_pair f_a f_b) (v: 'a # 'b))
28Proof
29  Cases_on ‘v’ \\ gvs [from_pair_def]
30QED
31
32(*----------------------------------------------------------*
33   option
34 *----------------------------------------------------------*)
35
36val _ = cv_rep_for [] “SOME (x:'a)”
37
38Theorem cv_THE[cv_rep]:
39  v <> NONE ==> f_a (THE v) = cv_snd ((from_option f_a) (v:'a option))
40Proof
41  Cases_on ‘v’ \\ gvs [from_option_def]
42QED
43
44Theorem cv_IS_SOME[cv_rep]:
45  b2c (IS_SOME v) = cv_ispair ((from_option f_a) (v:'a option))
46Proof
47  Cases_on ‘v’ \\ gvs [from_option_def]
48QED
49
50Theorem cv_IS_NONE[cv_rep]:
51  b2c (IS_NONE v) = cv_sub (Num 1) (cv_ispair ((from_option f_a) (v:'a option)))
52Proof
53  Cases_on ‘v’ \\ gvs [from_option_def]
54QED
55
56(*----------------------------------------------------------*
57   sum
58 *----------------------------------------------------------*)
59
60val res = cv_trans ISL;
61val res = cv_trans ISR;
62
63val res = cv_trans_pre "OUTL_pre" OUTL;
64
65Theorem OUTL_pre[cv_pre]:
66  OUTL_pre x <=> ISL x
67Proof
68  Cases_on ‘x’ \\ fs [res]
69QED
70
71val res = cv_trans_pre "OUTR_pre" OUTR;
72
73Theorem OUTR_pre[cv_pre]:
74  OUTR_pre x <=> ISR x
75Proof
76  Cases_on ‘x’ \\ fs [res]
77QED
78
79(*----------------------------------------------------------*
80   list
81 *----------------------------------------------------------*)
82
83Theorem cv_HD[cv_rep]:
84  v <> [] ==> f_a (HD v) = cv_fst ((from_list f_a) (v:'a list))
85Proof
86  Cases_on ‘v’ \\ fs [from_list_def]
87QED
88
89Theorem cv_TL[cv_rep]:
90  (from_list f_a) (TL v) = cv_snd ((from_list f_a) (v:'a list))
91Proof
92  Cases_on ‘v’ \\ fs [from_list_def]
93QED
94
95val res = cv_trans oHD_def;
96val res = cv_trans NULL_DEF;
97val res = cv_trans oEL_def;
98
99val res = cv_trans SNOC;
100val res = cv_trans APPEND;
101
102val res = cv_trans FLAT;
103
104val res = cv_trans TAKE_def;
105
106val res = cv_trans DROP_def;
107
108val res = cv_trans_pre "EL_pre" EL_def;
109
110Theorem EL_pre[cv_pre]:
111  !n xs. EL_pre n xs <=> n < LENGTH xs
112Proof
113  Induct \\ rw [] \\ simp [Once res] \\ Cases_on ‘xs’ \\ gvs []
114QED
115
116val res = cv_trans LEN_DEF;
117val res = cv_trans LENGTH_LEN;
118
119val res = cv_trans REV_DEF;
120val res = cv_trans REVERSE_REV;
121
122val res = cv_trans SUM_ACC_DEF;
123val res = cv_trans SUM_SUM_ACC;
124
125Theorem FRONT[local]:
126  FRONT (x::xs) = case xs of [] => [] | _ => x :: FRONT xs
127Proof
128  Cases_on ‘xs’ \\ gvs [FRONT_DEF]
129QED
130
131val res = cv_trans_pre "FRONT_pre" FRONT;
132
133Theorem FRONT_pre[cv_pre]:
134  !xs. FRONT_pre xs <=> xs <> []
135Proof
136  Induct_on ‘xs’
137  \\ once_rewrite_tac [res] \\ gvs []
138  \\ Cases_on ‘xs’ \\ gvs []
139QED
140
141Theorem LAST[local]:
142  LAST (x::xs) = case xs of [] => x | _ => LAST xs
143Proof
144  Cases_on ‘xs’ \\ gvs [LAST_DEF]
145QED
146
147val res = cv_trans_pre "LAST_pre" LAST;
148
149Theorem LAST_pre[cv_pre]:
150  !xs. LAST_pre xs <=> xs <> []
151Proof
152  Induct_on ‘xs’
153  \\ once_rewrite_tac [res] \\ gvs []
154  \\ Cases_on ‘xs’ \\ gvs []
155QED
156
157Definition list_mem_def:
158  list_mem y [] = F /\
159  list_mem y (x::xs) = if x = y then T else list_mem y xs
160End
161
162val res = cv_trans list_mem_def;
163
164val lemma = cv_rep_for [] “list_mem x xs” |> DISCH_ALL
165
166Theorem cv_rep_MEM[cv_rep]:
167  cv_rep p1 c1 (f_a:'a->cv) x /\
168  cv_rep p2 c2 (from_list f_a) xs /\
169  from_to f_a t_a ==>
170  cv_rep (p1 /\ p2) (cv_list_mem c1 c2) b2c (MEM x xs)
171Proof
172  have ‘MEM x xs = list_mem x xs’
173  >- (Induct_on ‘xs’ \\ gvs [list_mem_def] \\ metis_tac [])
174  \\ rw [] \\ mp_tac lemma  \\ gvs [cv_rep_def]
175QED
176
177Theorem conj_eq_if[local]:
178  x /\ y <=> if x then y else F
179Proof
180  Cases_on ‘x’ \\ gvs []
181QED
182
183Theorem if_not[local]:
184  (if ~b then x else y) = if b then y else x
185Proof
186  Cases_on ‘b’ \\ gvs []
187QED
188
189val all_distinct =
190  ALL_DISTINCT |> DefnBase.one_line_ify NONE
191               |> PURE_REWRITE_RULE [conj_eq_if,if_not]
192
193val res = cv_trans all_distinct;
194
195val is_prefix =
196  isPREFIX |> DefnBase.one_line_ify NONE
197           |> PURE_REWRITE_RULE [conj_eq_if,if_not]
198
199val res = cv_trans is_prefix;
200
201val res = cv_trans LUPDATE_DEF;
202
203Theorem index_of[local]:
204  INDEX_OF x [] = NONE /\
205  INDEX_OF x (y::ys) =
206    if x = y then SOME 0 else
207      case INDEX_OF x ys of
208      | NONE => NONE
209      | SOME n => SOME (n+1)
210Proof
211  gvs [INDEX_OF_def,INDEX_FIND_def]
212  \\ rw [] \\ gvs []
213  \\ simp [Once listTheory.INDEX_FIND_add]
214  \\ Cases_on ‘INDEX_FIND 0 ($= x) ys’ \\ gvs []
215  \\ rename [‘_ = SOME y’] \\ PairCases_on ‘y’ \\ gvs []
216QED
217
218val res = cv_trans_pre "INDEX_OF_pre" index_of;
219
220Theorem INDEX_OF_pre[cv_pre]:
221  ∀x y. INDEX_OF_pre x y
222Proof
223  Induct_on`y` \\ rw[Once res]
224QED
225
226Definition replicate_acc_def:
227  replicate_acc n x acc =
228    if n = 0:num then acc else replicate_acc (n-1) x (x::acc)
229End
230
231val res = cv_trans replicate_acc_def;
232
233Theorem REPLICATE:
234  REPLICATE n c = replicate_acc n c []
235Proof
236  qsuff_tac ‘!n c acc. replicate_acc n c acc = REPLICATE n c ++ acc’ >- gvs []
237  \\ Induct \\ gvs [] \\ simp [Once replicate_acc_def]
238  \\ rewrite_tac [GSYM SNOC_APPEND,SNOC_REPLICATE] \\ gvs []
239QED
240
241val res = cv_trans REPLICATE;
242val res = cv_trans (PAD_LEFT |> REWRITE_RULE [GSYM REPLICATE_GENLIST]);
243val res = cv_trans (PAD_RIGHT |> REWRITE_RULE [GSYM REPLICATE_GENLIST]);
244
245val res = cv_trans nub_def;
246
247val res = cv_trans ALOOKUP_def
248
249val res = cv_trans findi_def (* TODO: improve *)
250
251val res = cv_trans ZIP_def;
252
253Theorem UNZIP_eq:
254  UNZIP ts =
255    case ts of
256    | [] => ([],[])
257    | (x::xs) => let (t1,t2) = UNZIP xs in (FST x :: t1, SND x :: t2)
258Proof
259  Cases_on ‘ts’ \\ gvs []
260  \\ gvs [UNZIP] \\ Cases_on ‘UNZIP t’ \\ gvs []
261QED
262
263val res = cv_trans UNZIP_eq
264
265val lcp2_pre_def = cv_trans_pre "lcp2_pre" rich_listTheory.lcp2_thm;
266
267Theorem lcp2_pre[cv_pre]:
268  !xs ys. lcp2_pre xs ys
269Proof
270  Induct \\ rw[] \\ simp[Once lcp2_pre_def] \\
271  Cases_on `ys` \\ simp[Once lcp2_pre_def]
272QED
273
274val lcp_pre_def = cv_trans_pre "lcp_pre" rich_listTheory.lcp_oneline;
275
276Theorem lcp_pre[cv_pre]:
277  lcp_pre ls
278Proof
279  completeInduct_on `LENGTH ls` \\ rw[Once lcp_pre_def]
280QED
281
282Definition genlist_def:
283  genlist i f 0 = [] /\
284  genlist i f (SUC n) = f i :: genlist (i+1:num) f n
285End
286
287Theorem genlist_eq_GENLIST[cv_inline]:
288  GENLIST = genlist 0
289Proof
290  qsuff_tac ‘!i f n. genlist i f n = GENLIST (f o (λk. k + i)) n’
291  >- (gvs [FUN_EQ_THM] \\ rw [] \\ AP_THM_TAC \\ AP_TERM_TAC \\ gvs[FUN_EQ_THM])
292  \\ Induct_on ‘n’ \\ gvs [genlist_def]
293  \\ rewrite_tac [listTheory.GENLIST_CONS] \\ gvs []
294  \\ rw [] \\ AP_THM_TAC \\ AP_TERM_TAC \\ gvs[FUN_EQ_THM,arithmeticTheory.ADD1]
295QED
296
297Definition count_loop_def:
298  count_loop n k = if n = 0:num then [] else k::count_loop (n-1) (k+1:num)
299End
300
301val res = cv_trans count_loop_def;
302
303Theorem cv_COUNT_LIST[cv_inline]:
304  COUNT_LIST n = count_loop n 0
305Proof
306  qsuff_tac `!n k. count_loop n k = MAP (\i. i + k) (COUNT_LIST n)` >>
307  simp[] >>
308  Induct \\ rw[] \\ simp [rich_listTheory.COUNT_LIST_def,Once count_loop_def]
309  \\ gvs [MAP_MAP_o,combinTheory.o_DEF,ADD1] \\ AP_THM_TAC \\ AP_TERM_TAC
310  \\ gvs [FUN_EQ_THM]
311QED
312
313Theorem K_THM[cv_inline] = combinTheory.K_THM;
314Theorem I_THM[cv_inline] = combinTheory.I_THM;
315Theorem o_THM[cv_inline] = combinTheory.o_THM;
316
317Definition list_mapi_def:
318  list_mapi i f [] = [] /\
319  list_mapi i f (x::xs) = f i x :: list_mapi (i + 1n) f xs
320End
321
322Theorem MAPi_eq_list_mapi[cv_inline]:
323  MAPi = list_mapi 0
324Proof
325  qsuff_tac `!l i f. list_mapi i f l = MAPi (f o (λn. n + i)) l`
326  >- gvs[FUN_EQ_THM, combinTheory.o_DEF, SF ETA_ss] >>
327  Induct >> rw[list_mapi_def] >> gvs[combinTheory.o_DEF, ADD1]
328QED
329
330Definition cv_map_fst_def:
331  cv_map_fst cv =
332    cv_if (cv_ispair cv)
333      (Pair (cv_fst (cv_fst cv)) (cv_map_fst (cv_snd cv)))
334      (Num 0)
335Termination
336  WF_REL_TAC ‘measure cv_size’ >> cv_termination_tac
337End
338
339Theorem cv_MAP_FST[cv_rep]:
340  from_list a (MAP FST l) = cv_map_fst (from_list (from_pair a b) l)
341Proof
342  Induct_on `l` >> rw[from_list_def] >>
343  simp[Once cv_map_fst_def, SimpRHS] >>
344  Cases_on `h` >> gvs[from_pair_def]
345QED
346
347Definition cv_map_snd_def:
348  cv_map_snd cv =
349    cv_if (cv_ispair cv)
350      (Pair (cv_snd (cv_fst cv)) (cv_map_snd (cv_snd cv)))
351      (Num 0)
352Termination
353  WF_REL_TAC ‘measure cv_size’ >> cv_termination_tac
354End
355
356Theorem cv_MAP_SND[cv_rep]:
357  from_list b (MAP SND l) = cv_map_snd (from_list (from_pair a b) l)
358Proof
359  Induct_on `l` >> rw[from_list_def] >>
360  simp[Once cv_map_snd_def, SimpRHS] >>
361  Cases_on `h` >> gvs[from_pair_def]
362QED
363
364(*----------------------------------------------------------*
365   sptree / num_map / num_set
366 *----------------------------------------------------------*)
367
368val res = cv_trans sptreeTheory.insert_def;
369val res = cv_trans sptreeTheory.lookup_def;
370
371val def = sptreeTheory.fromList_def;
372val res = cv_auto_trans sptreeTheory.fromList_def;
373
374val res = cv_trans sptreeTheory.mk_BN_def;
375val res = cv_trans sptreeTheory.mk_BS_def;
376val res = cv_trans sptreeTheory.delete_def;
377
378val res = cv_trans sptreeTheory.union_def;
379val res = cv_trans sptreeTheory.inter_def;
380val res = cv_trans sptreeTheory.difference_def;
381
382val res = cv_auto_trans sptreeTheory.toList_def;
383val res = cv_auto_trans sptreeTheory.mk_wf_def;
384val res = cv_auto_trans sptreeTheory.size_def;
385
386val res = cv_trans sptreeTheory.list_to_num_set_def;
387val res = cv_trans sptreeTheory.list_insert_def;
388val res = cv_trans sptreeTheory.alist_insert_def;
389
390val res = cv_trans sptreeTheory.lrnext_def;
391
392val res = cv_trans sptreeTheory.spt_center_def
393
394val res = cv_trans sptreeTheory.spt_left_def
395val res = cv_trans sptreeTheory.spt_right_def
396
397val res = cv_trans sptreeTheory.subspt_eq;
398
399val lam = sptreeTheory.toAList_def |> SPEC_ALL |> concl |> find_term is_abs;
400
401Definition toAList_foldi_def:
402  toAList_foldi = foldi ^lam
403End
404
405val toAList_foldi_eq = sptreeTheory.foldi_def
406                  |> CONJUNCTS |> map (ISPEC lam)
407                  |> LIST_CONJ |> REWRITE_RULE [GSYM toAList_foldi_def]
408                  |> SIMP_RULE std_ss [];
409
410val res = cv_trans_pre "toAList_foldi_pre" toAList_foldi_eq;
411
412Theorem toAList_foldi_pre[cv_pre]:
413  !a0 a1 a2. toAList_foldi_pre a0 a1 a2
414Proof
415  Induct_on ‘a2’ \\ gvs [] \\ simp [Once res] \\ gvs []
416QED
417
418val res = cv_trans
419  (sptreeTheory.toAList_def
420     |> REWRITE_RULE [GSYM toAList_foldi_def,FUN_EQ_THM]);
421
422Definition cv_right_depth_def:
423  cv_right_depth (Num _) = 0:num /\
424  cv_right_depth (Pair x y) = cv_right_depth y + 1
425End
426
427val res = cv_trans spts_to_alist_add_pause_def;
428val res = cv_trans spts_to_alist_aux_def;
429val res = cv_trans spts_to_alist_def;
430
431val res = cv_trans toSortedAList_def;
432
433(*----------------------------------------------------------*
434   num |-> 'a
435 *----------------------------------------------------------*)
436
437Definition from_fmap_def:
438  from_fmap (f:'a -> cv) (m: num |-> 'a) =
439    from_sptree_sptree_spt f (fromAList (fmap_to_alist m))
440End
441
442Definition to_fmap_def:
443  to_fmap (t:cv -> 'a) m =
444    alist_to_fmap (toAList (to_sptree_spt t m))
445End
446
447Theorem from_to_fmap[cv_from_to]:
448  from_to (f0:'a -> cv) t0 ==>
449  from_to (from_fmap f0) (to_fmap t0)
450Proof
451  strip_tac
452  \\ drule (fetch "-" "from_sptree_to_sptree_spt_thm")
453  \\ gvs [from_fmap_def,to_fmap_def,from_to_def] \\ rw []
454  \\ gvs [finite_mapTheory.TO_FLOOKUP]
455  \\ gvs [FUN_EQ_THM,sptreeTheory.ALOOKUP_toAList,sptreeTheory.lookup_fromAList]
456QED
457
458Theorem cv_rep_FEMPTY[cv_rep]:
459  from_fmap f FEMPTY = Num 0
460Proof
461  EVAL_TAC \\ gvs [] \\ EVAL_TAC
462QED
463
464Theorem cv_rep_FLOOKUP[cv_rep]:
465  from_option f (FLOOKUP m n) = cv_lookup (Num n) (from_fmap f m)
466Proof
467  gvs [from_fmap_def,GSYM $ fetch "-" "cv_lookup_thm",
468       sptreeTheory.lookup_fromAList]
469QED
470
471Theorem cv_rep_FUPDATE[cv_rep]:
472  from_fmap f (m |+ (k,v)) = cv_insert (Num k) (f v) (from_fmap f m)
473Proof
474  gvs [from_fmap_def,GSYM $ fetch "-" "cv_insert_thm"] \\ AP_TERM_TAC
475  \\ dep_rewrite.DEP_REWRITE_TAC[sptreeTheory.spt_eq_thm,sptreeTheory.wf_insert]
476  \\ gvs [wf_fromAList,lookup_insert,lookup_fromAList,
477          finite_mapTheory.FLOOKUP_SIMP]
478  \\ rw []
479QED
480
481val FUPDATE_LIST_pre_def = finite_mapTheory.FUPDATE_LIST_THM
482 |> SRULE [FORALL_PROD]
483 |> INST_TYPE [alpha |-> “:num”]
484 |> cv_auto_trans_pre "FUPDATE_LIST_pre";
485
486Theorem FUPDATE_LIST_pre[cv_pre]:
487  ∀f ls. FUPDATE_LIST_pre f ls
488Proof
489  Induct_on`ls`
490  \\ rw[Once FUPDATE_LIST_pre_def]
491QED
492
493Theorem cv_rep_DOMSUB[cv_rep]:
494  from_fmap f (m \\ k) = cv_delete (Num k) (from_fmap f m)
495Proof
496  rw[from_fmap_def, GSYM (theorem "cv_delete_thm")]
497  \\ AP_TERM_TAC
498  \\ DEP_REWRITE_TAC[sptreeTheory.spt_eq_thm]
499  \\ rw[sptreeTheory.wf_fromAList, sptreeTheory.wf_delete]
500  \\ rw[sptreeTheory.lookup_delete, sptreeTheory.lookup_fromAList]
501  \\ rw[finite_mapTheory.DOMSUB_FLOOKUP_THM]
502QED
503
504Theorem cv_rep_FUNION[cv_rep]:
505  from_fmap f (FUNION m1 m2) = cv_union (from_fmap f m1) (from_fmap f m2)
506Proof
507  rw[from_fmap_def, GSYM (theorem "cv_union_thm")]
508  \\ AP_TERM_TAC
509  \\ DEP_REWRITE_TAC[sptreeTheory.spt_eq_thm]
510  \\ simp[sptreeTheory.wf_union, sptreeTheory.wf_fromAList]
511  \\ simp[sptreeTheory.lookup_union, sptreeTheory.lookup_fromAList]
512  \\ simp[finite_mapTheory.FLOOKUP_FUNION]
513QED
514
515(*----------------------------------------------------------*
516   num fset
517 *----------------------------------------------------------*)
518
519val from_to_num_set = from_to_thm_for “:num_set”;
520val to_num_set = from_to_num_set |> concl |> rand;
521val from_num_set = from_to_num_set |> concl |> rator |> rand;
522
523Definition to_num_fset_def:
524  to_num_fset cv = fromSet (domain (^to_num_set cv))
525End
526
527Definition from_num_fset_def:
528  from_num_fset fs = ^from_num_set $ list_to_num_set $ fset_REP fs
529End
530
531Theorem from_to_num_fset[cv_from_to]:
532  from_to from_num_fset to_num_fset
533Proof
534  rw[from_to_def, from_num_fset_def, to_num_fset_def]
535  \\ rw[GSYM toSet_11, toSet_fromSet]
536  \\ mp_tac from_to_num_set
537  \\ gs[from_to_def, pred_setTheory.EXTENSION,
538        GSYM fIN_IN, domain_list_to_num_set, fIN_def]
539QED
540
541val from_sptree_sptree_spt_def = definition "from_sptree_sptree_spt_def";
542val cv_insert_thm = theorem "cv_insert_thm";
543val cv_lookup_thm = theorem "cv_lookup_thm";
544val cv_union_thm = theorem "cv_union_thm";
545val cv_list_to_num_set_thm = theorem "cv_list_to_num_set_thm";
546
547Theorem fEMPTY_num_cv_rep[cv_rep]:
548  from_num_fset fEMPTY = Num 0
549Proof
550  rw[from_num_fset_def,
551     Q.ISPEC`from_unit`(CONJUNCT1(GSYM from_sptree_sptree_spt_def))]
552  \\ AP_TERM_TAC
553  \\ DEP_REWRITE_TAC[spt_eq_thm]
554  \\ rw[lookup_list_to_num_set, wf_list_to_num_set, MEM_fset_REP]
555QED
556
557Theorem fINSERT_num_cv_rep[cv_rep]:
558  from_num_fset (fINSERT e s) =
559  cv_insert (Num e) (Num 0) (from_num_fset s)
560Proof
561  rw[from_num_fset_def, GSYM cv_insert_thm, GSYM from_unit_def]
562  \\ AP_TERM_TAC
563  \\ DEP_REWRITE_TAC[spt_eq_thm]
564  \\ rw[wf_insert, wf_list_to_num_set,
565        lookup_list_to_num_set, lookup_insert,
566        MEM_fset_REP]
567  \\ gs[]
568QED
569
570Theorem fIN_num_cv_rep[cv_rep]:
571  b2c (fIN e s) =
572  cv_ispair $ (cv_lookup (Num e) (from_num_fset s))
573Proof
574  rw[from_num_fset_def, GSYM cv_lookup_thm, from_option_def,
575     lookup_list_to_num_set, MEM_fset_REP]
576QED
577
578Theorem fUNION_num_cv_rep[cv_rep]:
579  from_num_fset (fUNION s1 s2) =
580  cv_union (from_num_fset s1) (from_num_fset s2)
581Proof
582  rw[from_num_fset_def, GSYM cv_union_thm]
583  \\ AP_TERM_TAC
584  \\ DEP_REWRITE_TAC[spt_eq_thm]
585  \\ simp[wf_list_to_num_set, wf_union,
586          lookup_list_to_num_set, lookup_union]
587  \\ rw[fUNION_def, MEM_fset_REP] \\ gs[]
588QED
589
590Theorem fset_ABS_num_cv_rep[cv_rep]:
591  from_num_fset (fset_ABS l) =
592  cv_list_to_num_set (from_list Num l)
593Proof
594  rw[from_num_fset_def, GSYM cv_list_to_num_set_thm]
595  \\ AP_TERM_TAC
596  \\ DEP_REWRITE_TAC[spt_eq_thm]
597  \\ simp[wf_list_to_num_set, lookup_list_to_num_set, MEM_fset_REP]
598  \\ simp[GSYM fromSet_set, IN_fromSet]
599QED
600
601(*----------------------------------------------------------*
602   Misc.
603 *----------------------------------------------------------*)
604
605val _ = cv_trans v2n_custom_def;
606
607(*----------------------------------------------------------*
608   Help for manual termination proofs
609 *----------------------------------------------------------*)
610
611val cv_size'_def = theorem "cv_size'_def";
612val cv_mk_BN_def = definition "cv_mk_BN_def";
613val cv_mk_BS_def = definition "cv_mk_BS_def";
614
615Theorem cv_size'_Num[simp]:
616  cv_size' (Num m) = Num 0
617Proof
618  rw[Once cv_size'_def]
619QED
620
621Theorem cv_size'_cv_mk_BN[simp]:
622  cv_size' (cv_mk_BN x y) =
623  cv_add (cv_size' x) (cv_size' y)
624Proof
625  rw[cv_mk_BN_def]
626  \\ TRY (
627    rw[Once cv_size'_def]
628    \\ rw[Once cv_size'_def]
629    \\ Cases_on`x` \\ gs[]
630    \\ rw[Once cv_size'_def, SimpRHS]
631    \\ NO_TAC)
632  \\ rw[Once cv_size'_def]
633  \\ rw[Once cv_size'_def]
634  \\ Cases_on`y` \\ gs[]
635  \\ rw[Once cv_size'_def]
636  \\ rw[Once cv_size'_def]
637QED
638
639Theorem cv_size'_cv_mk_BS[simp]:
640  cv_size' (cv_mk_BS x y z) =
641  cv_add (cv_add (cv_size' x) (cv_size' z)) (Num 1)
642Proof
643  rw[cv_mk_BS_def]
644  \\ rw[Q.SPEC`Pair x y`cv_size'_def]
645  \\ Cases_on`x` \\ Cases_on`z` \\ gvs[]
646  \\ gvs[Q.SPEC`Pair x y`cv_size'_def]
647QED
648
649(*----------------------------------------------------------*
650   byte: word_of_bytes / word_to_bytes
651 *----------------------------------------------------------*)
652
653val _ = cv_trans num_of_bytes_def;
654val _ = cv_trans bytes_of_num_def;
655val _ = cv_trans be_bytes_def;
656
657(* Theorem connecting word_of_bytes (little-endian, starting at 0w) to
658   num_of_bytes.
659   This can be instantiated at any word type and then cv_trans'd. *)
660Theorem word_of_bytes_le_eq_num_of_bytes:
661  8 ≤ dimindex(:'a) ∧ divides 8 (dimindex(:'a)) ⇒
662  word_of_bytes_le bs = n2w (num_of_bytes bs) : 'a word
663Proof
664  rewrite_tac[word_of_bytes_le_def] \\ strip_tac
665  \\ drule_then (drule_then irule) word_eq_of_get_byte
666  \\ qexists_tac `F`
667  \\ qx_gen_tac `j` \\ strip_tac
668  \\ drule_then drule get_byte_word_of_bytes_le
669  \\ simp[] \\ disch_then kall_tac
670  \\ DEP_REWRITE_TAC[first_byte_at_0w]
671  \\ conj_tac >- gvs[DIV_LE_X,dimindex_lt_dimword]
672  \\ DEP_REWRITE_TAC[get_byte_n2w_le]
673  \\ simp[]
674  \\ qmatch_assum_abbrev_tac`j < k`
675  \\ `dimword(:'a) = 256 ** k`
676  by (simp[dimword_def] \\ gvs[dividesTheory.DIV_MULT_EQ]
677      \\ qpat_x_assum`_ * _ = _`(SUBST_ALL_TAC o SYM)
678      \\ simp[EXP_EXP_MULT] )
679  \\ simp[]
680  \\ qmatch_goalsub_abbrev_tac`x MOD _ DIV _`
681  \\ qspecl_then[`x`,`256 ** j`,`256 ** (k - j)`]mp_tac DIV_MOD_MOD_DIV
682  \\ impl_tac >- rw[]
683  \\ simp[GSYM EXP_ADD]
684  \\ disch_then $ SUBST_ALL_TAC o SYM
685  \\ qmatch_goalsub_abbrev_tac`l = _`
686  \\ Cases_on`l` \\ simp[dimword_8]
687  \\ qspecl_then[`256 ** (k - j - 1)`,`256`]mp_tac MOD_MULT_MOD
688  \\ impl_tac >- gvs[]
689  \\ simp[GSYM EXP, ADD1]
690  \\ disch_then kall_tac
691  \\ simp[Abbr`x`, num_of_bytes_DIV_EXP_MOD]
692  \\ rw[] \\ gvs[]
693QED
694
695(* Theorem connecting word_of_bytes (big-endian, starting at 0w) to num_of_bytes
696   via be_bytes *)
697Theorem word_of_bytes_be_eq_num_of_bytes:
698  8 ≤ dimindex(:'a) ∧ divides 8 (dimindex (:'a)) ⇒
699  word_of_bytes_be bs =
700    n2w (num_of_bytes (be_bytes (dimindex(:'a) DIV 8) [] bs)) : 'a word
701Proof
702  rewrite_tac[word_of_bytes_be_def] \\ strip_tac
703  \\ drule_then (drule_then irule) word_eq_of_get_byte
704  \\ qexists_tac `T`
705  \\ qx_gen_tac `j` \\ strip_tac
706  \\ drule_then drule get_byte_word_of_bytes_be
707  \\ simp[] \\ disch_then kall_tac
708  \\ DEP_REWRITE_TAC[first_byte_at_0w]
709  \\ qmatch_assum_abbrev_tac `j < k`
710  \\ conj_tac >- gvs[DIV_LE_X, dimindex_lt_dimword, Abbr`k`]
711  \\ DEP_REWRITE_TAC[get_byte_n2w_be]
712  \\ simp[LENGTH_be_bytes]
713  \\ `dimword(:'a) = 256 ** k`
714  by (simp[dimword_def] \\ gvs[dividesTheory.DIV_MULT_EQ]
715      \\ qpat_x_assum`_ * _ = _`(SUBST_ALL_TAC o SYM)
716      \\ simp[EXP_EXP_MULT] )
717  \\ simp[]
718  \\ qmatch_goalsub_abbrev_tac `x MOD _ DIV _`
719  \\ qspecl_then[`x`,`256 ** (k - 1 - j)`,`256 ** (j + 1)`] mp_tac
720                DIV_MOD_MOD_DIV
721  \\ impl_tac >- rw[]
722  \\ simp[GSYM EXP_ADD]
723  \\ disch_then $ SUBST_ALL_TAC o SYM
724  \\ qmatch_goalsub_abbrev_tac `l = _`
725  \\ Cases_on `l` \\ simp[dimword_8]
726  \\ qspecl_then[`256 ** j`,`256`]mp_tac MOD_MULT_MOD
727  \\ impl_tac >- gvs[]
728  \\ simp[GSYM EXP, ADD1]
729  \\ disch_then kall_tac
730  \\ simp[Abbr`x`, num_of_bytes_DIV_EXP_MOD, LENGTH_be_bytes]
731  \\ simp[be_bytes_thm, EL_REVERSE, LENGTH_TAKE_EQ, EL_TAKE, EL_APPEND_EQN,
732          EL_REPLICATE]
733  \\ rw[] \\ gvs[PRE_SUB1]
734QED
735
736(* Theorem connecting word_to_bytes (little-endian) to bytes_of_num.
737   No precondition needed since output length is fixed by dimindex. *)
738Theorem word_to_bytes_le_eq_bytes_of_num:
739  word_to_bytes_le (w:'a word) = bytes_of_num (dimindex(:'a) DIV 8) (w2n w)
740Proof
741  rewrite_tac[word_to_bytes_le_def] \\
742  reverse $ Cases_on`8 ≤ dimindex(:'a)` >- (
743    gvs[GSYM DIV_EQ_0, NOT_LESS_EQUAL]
744    \\ rw[bytes_of_num_def, word_to_bytes_def, word_to_bytes_aux_def])
745  \\ rw[word_to_bytes_def, LIST_EQ_REWRITE]
746  \\ rw[EL_bytes_of_num, EL_word_to_bytes_aux]
747  \\ rw[get_byte_n2w_le]
748QED
749
750(* Theorem connecting word_to_bytes (big-endian) to bytes_of_num.
751   No precondition needed since output length is fixed by dimindex. *)
752Theorem word_to_bytes_be_eq_bytes_of_num:
753  word_to_bytes_be (w:'a word) =
754    REVERSE (bytes_of_num (dimindex(:'a) DIV 8) (w2n w))
755Proof
756  rewrite_tac[word_to_bytes_be_def] \\
757  reverse $ Cases_on`8 ≤ dimindex(:'a)` >- (
758    gvs[GSYM DIV_EQ_0, NOT_LESS_EQUAL]
759    \\ rw[bytes_of_num_def, word_to_bytes_def, word_to_bytes_aux_def])
760  \\ rw[word_to_bytes_def, LIST_EQ_REWRITE, EL_REVERSE, PRE_SUB1]
761  \\ rw[EL_bytes_of_num, EL_word_to_bytes_aux]
762  \\ rw[get_byte_n2w_be]
763QED
764
765(* Translate at common word sizes: 32 and 64 bits *)
766val () = cv_trans (word_of_bytes_le_eq_num_of_bytes
767                   |> INST_TYPE [alpha |-> “:32”]
768                   |> SRULE[dividesTheory.compute_divides]);
769val () = cv_trans (word_of_bytes_le_eq_num_of_bytes
770                   |> INST_TYPE [alpha |-> “:64”]
771                   |> SRULE[dividesTheory.compute_divides]);
772val () = cv_trans (word_of_bytes_be_eq_num_of_bytes
773                   |> INST_TYPE [alpha |-> “:32”]
774                   |> SRULE[dividesTheory.compute_divides]);
775val () = cv_trans (word_of_bytes_be_eq_num_of_bytes
776                   |> INST_TYPE [alpha |-> “:64”]
777                   |> SRULE[dividesTheory.compute_divides]);
778val () = cv_trans (word_to_bytes_le_eq_bytes_of_num
779                   |> INST_TYPE [alpha |-> “:32”]);
780val () = cv_trans (word_to_bytes_le_eq_bytes_of_num
781                   |> INST_TYPE [alpha |-> “:64”]);
782val () = cv_trans (word_to_bytes_be_eq_bytes_of_num
783                   |> INST_TYPE [alpha |-> “:32”]);
784val () = cv_trans (word_to_bytes_be_eq_bytes_of_num
785                   |> INST_TYPE [alpha |-> “:64”])