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