cv_primScript.sml
1(*
2 Prove theorems cv_transLib uses for its operation
3*)
4Theory cv_prim
5Ancestors
6 cv_type cv arithmetic words cv_rep integer rat list rich_list
7 bitstring integer_word
8Libs
9 dep_rewrite cv_typeLib cv_repLib
10
11Overload c2n[local] = “cv$c2n”
12Overload c2b[local] = “cv$c2b”
13Overload Num[local] = “cv$Num”
14Overload Pair[local] = “cv$Pair”
15
16(*----------------------------------------------------------*
17 bool
18 *----------------------------------------------------------*)
19
20Theorem cv_rep_T[cv_rep]:
21 b2c T = Num 1
22Proof
23 fs []
24QED
25
26Theorem cv_rep_F[cv_rep]:
27 b2c F = Num 0
28Proof
29 fs []
30QED
31
32Theorem cv_rep_not[cv_rep]:
33 b2c (~b1) = cv_sub (Num 1) (b2c b1)
34Proof
35 Cases_on ‘b1’ \\ fs []
36QED
37
38Theorem cv_rep_and[cv_rep]:
39 b2c (b1 /\ b2) = cv_if (b2c b1) (b2c b2) (Num 0)
40Proof
41 Cases_on ‘b1’ \\ Cases_on ‘b2’ \\ fs []
42QED
43
44Theorem cv_rep_or[cv_rep]:
45 b2c (b1 \/ b2) = cv_if (b2c b1) (Num 1) (b2c b2)
46Proof
47 Cases_on ‘b1’ \\ Cases_on ‘b2’ \\ fs [cv_rep_def]
48QED
49
50Theorem cv_inline_imp[cv_rep]:
51 b2c (a ==> b) = cv_if (b2c a) (b2c b) (Num 1)
52Proof
53 Cases_on `a` >> Cases_on `b` >> gvs[cvTheory.b2c_def]
54QED
55
56(*----------------------------------------------------------*
57 num
58 *----------------------------------------------------------*)
59
60Theorem cv_rep_suc[cv_rep]:
61 Num (SUC n) = cv_add (Num n) (Num 1)
62Proof
63 fs []
64QED
65
66Theorem cv_rep_sub1[cv_rep]:
67 Num (PRE n) = cv_sub (Num n) (Num 1)
68Proof
69 fs []
70QED
71
72Theorem cv_rep_add[cv_rep]:
73 Num (n + m) = cv_add (Num n) (Num m)
74Proof
75 fs []
76QED
77
78Theorem cv_rep_sub[cv_rep]:
79 Num (n - m) = cv_sub (Num n) (Num m)
80Proof
81 fs []
82QED
83
84Theorem cv_rep_mul[cv_rep]:
85 Num (n * m) = cv_mul (Num n) (Num m)
86Proof
87 fs [cv_rep_def]
88QED
89
90Theorem cv_rep_div[cv_rep]:
91 Num (n DIV m) = cv_div (Num n) (Num m)
92Proof
93 fs [cv_rep_def]
94QED
95
96Theorem cv_rep_mod[cv_rep]:
97 Num (n MOD m) = cv_mod (Num n) (Num m)
98Proof
99 fs [cv_rep_def]
100QED
101
102Theorem cv_rep_exp[cv_rep]:
103 Num (n ** m) = cv_exp (Num n) (Num m)
104Proof
105 fs [cv_rep_def,cvTheory.cv_exp_def]
106QED
107
108Theorem cv_rep_odd[cv_rep]:
109 b2c (ODD n) = cv_mod (Num n) (Num 2)
110Proof
111 fs [cv_rep_def] \\ rw [] \\ gvs [bitTheory.ODD_MOD2_LEM]
112 \\ ‘n MOD 2 < 2’ by fs []
113 \\ Cases_on ‘n MOD 2’ \\ fs []
114QED
115
116Theorem cv_rep_even[cv_rep]:
117 b2c (EVEN n) = cv_sub (Num 1) (cv_mod (Num n) (Num 2))
118Proof
119 simp [cv_rep_odd,cv_rep_not,arithmeticTheory.EVEN_ODD]
120QED
121
122Theorem cv_rep_lt[cv_rep]:
123 b2c (n < m) = cv_lt (Num n) (Num m)
124Proof
125 fs [cv_rep_def] \\ rw []
126QED
127
128Theorem cv_rep_le[cv_rep]:
129 b2c (n <= m) = cv_sub (Num 1) (cv_lt (Num m) (Num n))
130Proof
131 fs [cv_rep_def] \\ rw []
132QED
133
134Theorem cv_rep_gt[cv_rep]:
135 b2c (n > m) = cv_lt (Num m) (Num n)
136Proof
137 fs [cv_rep_def] \\ rw []
138QED
139
140Theorem cv_rep_ge[cv_rep]:
141 b2c (n >= m) = cv_sub (Num 1) (cv_lt (Num n) (Num m))
142Proof
143 fs [cv_rep_def] \\ rw []
144QED
145
146Theorem cv_rep_num_case[cv_rep]:
147 cv_rep p1 c1 Num x /\
148 cv_rep p2 c2 (a:'a->cv) y /\
149 (!v:num. cv_rep (p3 v) (c3 (Num v)) (a:'a->cv) (z v)) ==>
150 cv_rep (p1 /\ (x = 0 ==> p2) /\ !n. x = SUC n ==> p3 n)
151 (cv_if (cv_lt (Num 0) c1) (let y = cv_sub c1 (Num 1) in c3 y) c2)
152 a (num_CASE x y z)
153Proof
154 rw [] \\ gvs [cv_rep_def] \\ rw [] \\ gvs []
155 \\ Cases_on ‘x’ \\ gvs []
156QED
157
158Definition cv_min_def:
159 cv_min x y = cv_if (cv_lt x y) x y
160End
161
162Definition cv_max_def:
163 cv_max x y = cv_if (cv_lt x y) y x
164End
165
166Theorem cv_min_thm[cv_rep]:
167 Num (MIN m n) = cv_min (Num m) (Num n)
168Proof
169 fs [cv_min_def] \\ rw []
170 \\ BasicProvers.every_case_tac \\ fs []
171 \\ gvs [arithmeticTheory.MIN_DEF]
172QED
173
174Theorem cv_max_thm[cv_rep]:
175 Num (MAX m n) = cv_max (Num m) (Num n)
176Proof
177 fs [cv_max_def] \\ rw []
178 \\ BasicProvers.every_case_tac \\ fs []
179 \\ gvs [arithmeticTheory.MAX_DEF]
180QED
181
182Definition cv_gcd_def:
183 cv_gcd a b = cv_if a (cv_gcd (cv_mod b a) a) b
184Termination
185 WF_REL_TAC `measure $ λ(a,b). c2n a + c2n b + (c2n a - c2n b)` >>
186 rpt gen_tac >> strip_tac >>
187 simp[] >> gvs[c2b_def] >>
188 Cases_on `b` >> gvs[cv_mod_def] >>
189 `m MOD SUC k - SUC k = 0` by (
190 simp[] >> irule LESS_IMP_LESS_OR_EQ >> simp[]) >>
191 `m MOD SUC k < SUC k` by simp[] >>
192 simp[] >> DECIDE_TAC
193End
194
195Theorem cv_gcd_thm[cv_rep]:
196 Num (gcd a b) = cv_gcd (Num a) (Num b)
197Proof
198 qsuff_tac `!c d a b. c = Num a /\ d = Num b ==> Num (gcd a b) = cv_gcd c d`
199 >- rw[] >>
200 ho_match_mp_tac cv_gcd_ind >> rw[] >>
201 rw[Once gcdTheory.GCD_EFFICIENTLY, Once cv_gcd_def] >> gvs[] >>
202 gvs[c2b_def] >> Cases_on `a` >> gvs[]
203QED
204
205Definition cv_log2_def:
206 cv_log2 acc n =
207 cv_if (cv_lt (Num 1) n)
208 (cv_log2 (cv_add acc (Num 1)) (cv_div n (Num 2)))
209 acc
210Termination
211 WF_REL_TAC `measure $ λ(_,n). cv$c2n n` >> Cases >> rw[]
212End
213
214Theorem cv_rep_LOG2[cv_rep]:
215 n <> 0 ==> Num (LOG2 n) = cv_log2 (Num 0) (Num n)
216Proof
217 qsuff_tac `!acc. n <> 0 ==> cv_log2 (Num acc) (Num n) = Num (LOG2 n + acc)`
218 >- rw[] >>
219 simp[bitTheory.LOG2_def] >>
220 completeInduct_on `n` >> rw[] >>
221 once_rewrite_tac[numeral_bitTheory.LOG_compute] >> simp[] >>
222 once_rewrite_tac[cv_log2_def] >>
223 simp[cvTheory.cv_lt_def] >>
224 IF_CASES_TAC >> gvs[cvTheory.c2b_def, AllCaseEqs()] >>
225 first_x_assum $ qspec_then `n DIV 2` mp_tac >>
226 simp[DIV_LT_X, DIV_EQ_X]
227QED
228
229(*----------------------------------------------------------*
230 int
231 *----------------------------------------------------------*)
232
233Theorem cv_int_of_num[cv_rep]:
234 from_int (&n) = Num n
235Proof
236 gvs[from_int_def]
237QED
238
239Definition cv_abs_def:
240 cv_abs i = cv_if (cv_ispair i) (cv_fst i) i
241End
242
243Theorem cv_Num[cv_rep]:
244 Num (integer$Num i) = cv_abs (from_int i)
245Proof
246 gvs[from_int_def, cv_abs_def] >>
247 rw[] >> gvs[cv_ispair_def]
248QED
249
250Definition cv_int_neg_def:
251 cv_int_neg x =
252 cv_if (cv_eq x (Num 0)) x $
253 cv_if (cv_ispair x) (cv_fst x) (Pair x (Num 0))
254End
255
256Theorem cv_neg_int[cv_rep]:
257 from_int (- x) = cv_int_neg (from_int x)
258Proof
259 gvs[from_int_def]
260 \\ Cases_on ‘x = 0’ \\ gvs [cv_int_neg_def]
261 \\ Cases_on ‘x’ \\ gvs []
262QED
263
264Definition cv_int_lt_def:
265 cv_int_lt i j =
266 cv_if (cv_ispair i) (* if i < 0 *)
267 (cv_if (cv_ispair j) (* if j < 0 *)
268 (cv_lt (cv_abs j) (cv_abs i))
269 (Num 1))
270 (cv_if (cv_ispair j) (* if j < 0 *)
271 (Num 0)
272 (cv_lt i j))
273End
274
275Theorem cv_int_lt[cv_rep]:
276 b2c (int_lt i j) = cv_int_lt (from_int i) (from_int j)
277Proof
278 simp[cv_int_lt_def, from_int_def, cv_abs_def] >>
279 IF_CASES_TAC >>
280 gvs[COND_RAND] >> rw[] >> gvs[c2b_def] >>
281 Cases_on `i` >> gvs[] >> Cases_on `j` >> gvs[]
282QED
283
284Theorem cv_int_le[cv_rep]:
285 b2c (int_le i j) = cv_if (cv_int_lt (from_int j) (from_int i))
286 (Num 0) (Num 1)
287Proof
288 simp[int_le, GSYM cv_int_lt] >> Cases_on `j < i` >> simp[]
289QED
290
291Theorem cv_int_gt[cv_rep]:
292 b2c (int_gt i j) = cv_int_lt (from_int j) (from_int i)
293Proof
294 simp[int_gt, GSYM cv_int_lt]
295QED
296
297Theorem cv_int_ge[cv_rep]:
298 b2c (int_ge i j) = cv_if (cv_int_lt (from_int i) (from_int j))
299 (Num 0) (Num 1)
300Proof
301 simp[int_ge, int_le, GSYM cv_int_lt] >> Cases_on `i < j` >> gvs[]
302QED
303
304Definition cv_int_add_def:
305 cv_int_add i j =
306 cv_if (cv_ispair i) (* if i < 0 *)
307 (cv_if (cv_ispair j) (* if j < 0 *)
308 (Pair (cv_add (cv_fst i) (cv_fst j)) (Num 0))
309 (cv_if (cv_int_lt j (cv_fst i)) (* i < 0 /\ ~(j < 0); if j < |i| *)
310 (Pair (cv_sub (cv_fst i) j) (Num 0))
311 (cv_sub j (cv_fst i))))
312 (cv_if (cv_ispair j) (* if j < 0 *)
313 (cv_if (cv_int_lt i (cv_fst j)) (* ~(i < 0) /\ j < 0; if i < |j| *)
314 (Pair (cv_sub (cv_fst j) i) (Num 0))
315 (cv_sub i (cv_fst j)))
316 (cv_add i j))
317End
318
319Theorem cv_int_add[cv_rep]:
320 from_int (i + j) = cv_int_add (from_int i) (from_int j)
321Proof
322 simp[from_int_def, cv_int_add_def, cv_int_lt_def, cv_sub_def] >>
323 Cases_on `i < 0` >> Cases_on `j < 0` >> gvs[] >>
324 namedCases_on `i` ["ni","ni",""] >> namedCases_on `j` ["nj","nj",""] >>
325 gvs[INT_ADD_CALCULATE]
326 >- (Cases_on `ni <= nj` >> gvs[])
327 >- (Cases_on `nj <= ni` >> gvs[])
328QED
329
330Theorem cv_int_sub[cv_rep]:
331 from_int (i - j) = cv_int_add (from_int i) (cv_int_neg (from_int j))
332Proof
333 simp[int_sub, GSYM cv_neg_int, GSYM cv_int_add]
334QED
335
336Theorem int_div[local]:
337 j <> 0 ==>
338 int_div i j =
339 if j < 0 then
340 if i < 0 then &(Num i DIV Num j)
341 else -&(Num i DIV Num j) + if Num i MOD Num j = 0 then 0 else -1
342 else if i < 0 then
343 -&(Num i DIV Num j) + if Num i MOD Num j = 0 then 0 else -1
344 else &(Num i DIV Num j)
345Proof
346 strip_tac >> simp[int_div] >>
347 Cases_on `j < 0` >> Cases_on `i < 0` >> gvs[] >>
348 namedCases_on `i` ["ni","ni",""] >> gvs[] >>
349 namedCases_on `j` ["nj","nj",""] >> gvs[]
350QED
351
352Definition cv_int_div_def:
353 cv_int_div i j =
354 cv_if (cv_ispair j) (* if j < 0 *)
355 (cv_if (cv_ispair i) (* if i < 0 *)
356 (cv_div (cv_fst i) (cv_fst j))
357 (cv_int_add
358 (Pair (cv_div i (cv_fst j)) (Num 0))
359 (cv_if (cv_mod i (cv_fst j))
360 (Pair (Num 1) (Num 0)) (Num 0))))
361 (cv_if (cv_ispair i) (* if i < 0 *)
362 (cv_int_add
363 (Pair (cv_div (cv_fst i) j) (Num 0))
364 (cv_if (cv_mod (cv_fst i) j)
365 (Pair (Num 1) (Num 0)) (Num 0)))
366 (cv_div i j))
367End
368
369Definition total_int_div_def:
370 total_int_div i j = if j = 0 then 0 else int_div i j
371End
372
373Definition cv_total_int_div_def:
374 cv_total_int_div i j =
375 cv_if (cv_eq j (Num 0)) (Num 0) (cv_int_div i j)
376End
377
378Theorem cv_int_div[cv_rep]:
379 j <> 0 ==> from_int (int_div i j) = cv_int_div (from_int i) (from_int j)
380Proof
381 simp[int_div, cv_int_div_def, from_int_def] >>
382 Cases_on `j = 0` >> gvs[] >>
383 Cases_on `j < 0` >> Cases_on `i < 0` >> gvs[] >>
384 Cases_on `i = 0` >> gvs[] >>
385 reverse $ Cases_on `Num i MOD Num j` >> gvs[] >>
386 simp[INT_ADD_CALCULATE, cv_int_add_def, cv_int_lt_def] >>
387 Cases_on `Num i DIV Num j` >> gvs[]
388QED
389
390Theorem cv_total_int_div[cv_rep]:
391 from_int (total_int_div i j) = cv_total_int_div (from_int i) (from_int j)
392Proof
393 simp[total_int_div_def, cv_total_int_div_def] >>
394 Cases_on `j = 0` >> gvs[] >- simp[from_int_def] >>
395 rw[GSYM cv_int_div] >> Cases_on `j` >> gvs[from_int_def]
396QED
397
398Definition cv_int_mul_def:
399 cv_int_mul i j =
400 cv_if (cv_eq i (Num 0)) (Num 0) $
401 cv_if (cv_eq j (Num 0)) (Num 0) $
402 cv_if (cv_ispair i)
403 (cv_if (cv_ispair j)
404 (cv_mul (cv_fst i) (cv_fst j))
405 (Pair (cv_mul (cv_fst i) j) (Num 0)))
406 (cv_if (cv_ispair j)
407 (Pair (cv_mul i (cv_fst j)) (Num 0))
408 (cv_mul i j))
409End
410
411Theorem cv_int_mul[cv_rep]:
412 from_int (i * j) = cv_int_mul (from_int i) (from_int j)
413Proof
414 simp[cv_int_mul_def, from_int_def, cv_eq_def] >>
415 namedCases_on `i` ["ni","ni",""] >> gvs[] >>
416 namedCases_on `j` ["nj","nj",""] >> gvs[] >>
417 gvs[INT_MUL_CALCULATE]
418QED
419
420Definition cv_int_mod_def:
421 cv_int_mod i j = cv_int_add i (cv_int_neg (cv_int_mul (cv_int_div i j) j))
422End
423
424Definition total_int_mod_def:
425 total_int_mod i j = if j = 0 then i else int_mod i j
426End
427
428Definition cv_total_int_mod_def:
429 cv_total_int_mod i j = cv_if (cv_eq j (Num 0)) i (cv_int_mod i j)
430End
431
432Theorem cv_int_mod[cv_rep]:
433 j <> 0 ==>
434 from_int (int_mod i j) = cv_int_mod (from_int i) (from_int j)
435Proof
436 strip_tac >> simp[cv_int_mod_def] >>
437 simp[GSYM cv_int_div, GSYM cv_int_mul, GSYM cv_int_sub] >>
438 simp[Once int_mod]
439QED
440
441Theorem cv_total_int_mod[cv_rep]:
442 from_int (total_int_mod i j) = cv_total_int_mod (from_int i) (from_int j)
443Proof
444 simp[total_int_mod_def, cv_total_int_mod_def] >>
445 Cases_on `j = 0` >> gvs[] >- simp[from_int_def] >>
446 rw[GSYM cv_int_mod] >> Cases_on `j` >> gvs[from_int_def]
447QED
448
449(*----------------------------------------------------------*
450 rat
451 *----------------------------------------------------------*)
452
453Theorem cv_rat_of_int[cv_rep]:
454 from_rat (rat_of_int i) = Pair (from_int i) (Num 1)
455Proof
456 rw[from_rat_def]
457QED
458
459Definition cv_rat_neg_def:
460 cv_rat_neg r = Pair (cv_int_neg (cv_fst r)) (cv_snd r)
461End
462
463Theorem cv_rat_neg[cv_rep]:
464 from_rat (-r) = cv_rat_neg (from_rat r)
465Proof
466 simp[from_rat_def, cv_rat_neg_def, cv_neg_int]
467QED
468
469Definition cv_rat_reciprocal_def:
470 cv_rat_reciprocal r =
471 cv_if (cv_int_lt (cv_fst r) (Num 0))
472 (Pair (Pair (cv_snd r) (Num 0)) (cv_fst (cv_fst r)))
473 (Pair (cv_snd r) (cv_fst r))
474End
475
476Theorem cv_rat_reciprocal[cv_rep]:
477 r <> 0 ==> from_rat (rat_minv r) = cv_rat_reciprocal (from_rat r)
478Proof
479 rw[] >> simp[RAT_MINV_RATND] >> simp[cv_rat_reciprocal_def] >>
480 `Num 0 = from_int 0` by gvs[from_int_def] >> simp[] >> pop_assum kall_tac >>
481 reverse $ rw[] >> gvs[c2b_def] >> pop_assum mp_tac >>
482 simp[Once from_rat_def, GSYM cv_int_lt] >>
483 strip_tac >> gvs[] >> Cases_on `r < 0` >> gvs[]
484 >- (
485 `rat_sgn r = 1` by (CCONTR_TAC >> gvs[RAT_LEQ_LES, RAT_LEQ_ANTISYM]) >>
486 `rat_of_int (ABS (RATN r)) = &Num (RATN r)`
487 by (Cases_on `RATN r` >> gvs[]) >>
488 simp[from_rat_def] >>
489 qspecl_then [`int_of_num $ RATD r`,`Num (RATN r)`]
490 mp_tac $ GEN_ALL RATND_suff_eq >>
491 simp[Once gcdTheory.GCD_SYM] >> strip_tac >> simp[from_int_def]
492 )
493 >- (
494 `rat_sgn r = -1` by gvs[] >> simp[] >>
495 simp[rat_of_int_ainv, from_rat_def, from_int_def] >>
496 DEP_REWRITE_TAC[RAT_LDIV_LES_POS] >> simp[] >> conj_tac
497 >- (
498 `0 = rat_of_int 0` by gvs[] >> pop_assum SUBST1_TAC >>
499 rewrite_tac[rat_of_int_LT] >> simp[]
500 ) >>
501 simp[RAT_MUL_NUM_CALCULATE] >>
502 simp[GSYM RAT_DIV_AINV, Num_neg] >>
503 `rat_of_int (ABS (RATN r)) = &Num (RATN r)`
504 by (Cases_on `RATN r` >> gvs[]) >>
505 qspecl_then [`int_of_num $ RATD r`,`Num (RATN r)`]
506 mp_tac $ GEN_ALL RATND_suff_eq >>
507 simp[Once gcdTheory.GCD_SYM]
508 )
509QED
510
511Definition cv_rat_norm_def:
512 cv_rat_norm r =
513 let d = cv_gcd (cv_abs (cv_fst r)) (cv_snd r) in
514 cv_if (cv_lt d (Num 2))
515 r
516 (Pair (cv_total_int_div (cv_fst r) d) (cv_div (cv_snd r) d))
517End
518
519Theorem cv_rat_norm_div_gcd:
520 (λ(x,y). Pair (from_int x) (Num y)) (div_gcd a b) =
521 cv_rat_norm (Pair (from_int a) (Num b))
522Proof
523 simp[div_gcd_def, cv_rat_norm_def] >>
524 simp[GSYM cv_Num, GSYM cv_gcd_thm, c2b_def] >>
525 ntac 3 $ simp[Once COND_RAND] >> simp[COND_RATOR] >>
526 `Num (gcd (Num a) b) = from_int (&(gcd (Num a) b))` by simp[from_int_def] >>
527 simp[GSYM cv_total_int_div] >>
528 simp[wordsTheory.NUMERAL_LESS_THM] >>
529 Cases_on `a = 0 /\ b = 0 \/ gcd (Num a) b = 1` >> gvs[] >>
530 IF_CASES_TAC >> gvs[] >> simp[total_int_div_def] >> IF_CASES_TAC >> gvs[]
531QED
532
533Theorem from_rat_eq_cv_rat_norm_suff[local]:
534 r = rat_of_int n / &d /\ d <> 0 /\
535 from_int n = x /\
536 Num d = y
537 ==> from_rat r = cv_rat_norm (Pair x y)
538Proof
539 rw[] >> simp[GSYM cv_rat_norm_div_gcd] >>
540 pairarg_tac >> gvs[from_rat_def] >>
541 drule_all div_gcd_correct >> rw[]
542QED
543
544Definition cv_rat_add_def:
545 cv_rat_add r1 r2 =
546 cv_rat_norm $ Pair
547 (cv_int_add (cv_int_mul (cv_fst r1) (cv_snd r2))
548 (cv_int_mul (cv_fst r2) (cv_snd r1)))
549 (cv_mul (cv_snd r1) (cv_snd r2))
550End
551
552Theorem cv_rat_add[cv_rep]:
553 from_rat (r1 + r2) = cv_rat_add (from_rat r1) (from_rat r2)
554Proof
555 simp[cv_rat_add_def] >> irule from_rat_eq_cv_rat_norm_suff >>
556 qexistsl [`RATD r1 * RATD r2`,`(RATN r1 * &RATD r2) + (RATN r2 * &RATD r1)`]>>
557 simp[from_rat_def] >> rw[]
558 >- (
559 simp[cv_int_add] >> rpt MK_COMB_TAC >> simp[] >>
560 simp[cv_int_mul] >> rpt MK_COMB_TAC >> simp[from_int_def]
561 ) >>
562 qspecl_then [`&RATD r1`,`rat_of_int $ RATN r1`,`&RATD r2`,
563 `rat_of_int $ RATN r2`]
564 mp_tac $ GEN_ALL $ GSYM RAT_DIVDIV_ADD >> simp[] >>
565 once_rewrite_tac[GSYM rat_of_int_of_num] >>
566 rewrite_tac[rat_of_int_MUL, rat_of_int_ADD, INT_MUL_CALCULATE] >> simp[]
567QED
568
569Theorem cv_rat_sub[cv_rep]:
570 from_rat (r1 - r2) = cv_rat_add (from_rat r1) (cv_rat_neg (from_rat r2))
571Proof
572 simp[RAT_SUB_ADDAINV, GSYM cv_rat_neg, GSYM cv_rat_add]
573QED
574
575Definition cv_rat_mul_def:
576 cv_rat_mul r1 r2 =
577 cv_rat_norm $ Pair
578 (cv_int_mul (cv_fst r1) (cv_fst r2))
579 (cv_mul (cv_snd r1) (cv_snd r2))
580End
581
582Theorem cv_rat_mul[cv_rep]:
583 from_rat (r1 * r2) = cv_rat_mul (from_rat r1) (from_rat r2)
584Proof
585 simp[cv_rat_mul_def] >> irule from_rat_eq_cv_rat_norm_suff >>
586 qexistsl [`RATD r1 * RATD r2`,`RATN r1 * RATN r2`] >>
587 simp[from_rat_def, cv_int_mul] >>
588 qspecl_then [`&RATD r2`,`rat_of_int $ RATN r2`,`&RATD r1`,
589 `rat_of_int $ RATN r1`]
590 mp_tac $ GEN_ALL $ GSYM RAT_DIVDIV_MUL >>
591 simp[rat_of_int_MUL, RAT_MUL_NUM_CALCULATE]
592QED
593
594Theorem cv_rat_div[cv_rep]:
595 r2 <> 0 ==> from_rat (r1 / r2) =
596 cv_rat_mul (from_rat r1) (cv_rat_reciprocal (from_rat r2))
597Proof
598 simp[RAT_DIV_MULMINV, GSYM cv_rat_reciprocal, GSYM cv_rat_mul]
599QED
600
601Definition cv_rat_lt_def:
602 cv_rat_lt r1 r2 =
603 cv_int_lt (cv_int_mul (cv_fst r1) (cv_snd r2))
604 (cv_int_mul (cv_fst r2) (cv_snd r1))
605End
606
607Theorem cv_rat_lt[cv_rep]:
608 b2c (r1 < r2) = cv_rat_lt (from_rat r1) (from_rat r2)
609Proof
610 rw[cv_rat_lt_def, from_rat_def] >>
611 `!n. Num n = from_int (&n)` by simp[from_int_def] >>
612 simp[] >> pop_assum kall_tac >>
613 simp[GSYM cv_int_mul, GSYM cv_int_lt] >> AP_TERM_TAC >>
614 qspec_then `r1` mp_tac $ GEN_ALL RATN_RATD_EQ_THM >>
615 disch_then $ rewrite_tac o single o Once >>
616 qspec_then `r2` mp_tac $ GEN_ALL RATN_RATD_EQ_THM >>
617 disch_then $ rewrite_tac o single o Once >>
618 `0 < RATD r1` by gvs[] >> `0 < RATD r2` by gvs[] >>
619 rename1 `rat_of_int n1 / &d1 < rat_of_int n2 / &d2` >>
620 simp[RAT_LDIV_LES_POS, RDIV_MUL_OUT, RAT_RDIV_LES_POS] >>
621 once_rewrite_tac[GSYM rat_of_int_of_num] >> rewrite_tac[rat_of_int_MUL] >>
622 simp[AC INT_MUL_ASSOC INT_MUL_COMM]
623QED
624
625Theorem cv_rat_le[cv_rep]:
626 b2c (r1 <= r2) = cv_if (cv_rat_lt (from_rat r2) (from_rat r1))
627 (Num 0) (Num 1)
628Proof
629 simp[GSYM RAT_LEQ_LES, GSYM cv_rat_lt] >> Cases_on `r2 < r1` >> gvs[]
630QED
631
632Theorem cv_rat_gt[cv_rep]:
633 b2c (r1 > r2) = cv_rat_lt (from_rat r2) (from_rat r1)
634Proof
635 simp[rat_gre_def, GSYM cv_rat_lt]
636QED
637
638Theorem cv_rat_ge[cv_rep]:
639 b2c (r1 >= r2) = cv_if (cv_rat_lt (from_rat r1) (from_rat r2))
640 (Num 0) (Num 1)
641Proof
642 simp[rat_geq_def, GSYM RAT_LEQ_LES, GSYM cv_rat_lt] >>
643 Cases_on `r1 < r2` >> gvs[]
644QED
645
646(*----------------------------------------------------------*
647 char
648 *----------------------------------------------------------*)
649
650Theorem cv_chr_thm[cv_rep]:
651 n < 256 ==> from_char (CHR n) = Num n
652Proof
653 gvs [from_char_def]
654QED
655
656Theorem cv_ord_thm[cv_rep]:
657 Num (ORD c) = from_char c
658Proof
659 gvs [from_char_def]
660QED
661
662Theorem cv_rep_char_lt[cv_rep]:
663 b2c (n < m) = cv_lt (from_char n) (from_char m)
664Proof
665 fs [cv_rep_def] \\ rw [from_char_def,stringTheory.char_lt_def]
666QED
667
668Theorem cv_rep_char_le[cv_rep]:
669 b2c (n <= m) = cv_sub (Num 1) (cv_lt (from_char m) (from_char n))
670Proof
671 fs [cv_rep_def] \\ rw [from_char_def,stringTheory.char_le_def]
672QED
673
674Theorem cv_rep_char_gt[cv_rep]:
675 b2c (n > m) = cv_lt (from_char m) (from_char n)
676Proof
677 fs [cv_rep_def] \\ rw [from_char_def,stringTheory.char_gt_def]
678QED
679
680Theorem cv_rep_char_ge[cv_rep]:
681 b2c (n >= m) = cv_sub (Num 1) (cv_lt (from_char n) (from_char m))
682Proof
683 fs [cv_rep_def] \\ rw [from_char_def,stringTheory.char_ge_def]
684QED
685
686(*----------------------------------------------------------*
687 if, let, arb, =
688 *----------------------------------------------------------*)
689
690Theorem cv_rep_if[cv_rep]:
691 cv_rep p1 c1 b2c b /\
692 cv_rep p2 c2 f t /\
693 cv_rep p3 c3 f e ==>
694 cv_rep (p1 /\ (b ==> p2) /\ (~b ==> p3))
695 (cv_if c1 c2 c3) f (if b then t else e)
696Proof
697 fs [cv_rep_def] \\ rw [] \\ gvs []
698QED
699
700Theorem cv_rep_let[cv_rep]:
701 cv_rep p1 c1 (a:'a->cv) x /\
702 (!v. cv_rep (p2 v) (c2 (a v)) (b:'b->cv) (y v)) ==>
703 cv_rep (p1 /\ !v. v = x ==> p2 v) (LET c2 c1) b (LET y x)
704Proof
705 fs [cv_rep_def]
706QED
707
708Theorem cv_rep_arb[cv_rep]:
709 F ==> f ARB = Num 0
710Proof
711 fs []
712QED
713
714Theorem cv_rep_eq[cv_rep]:
715 cv_rep p1 c1 f x /\
716 cv_rep p2 c2 f y /\
717 from_to f t ==>
718 cv_rep (p1 /\ p2) (cv_eq c1 c2) b2c (x = y)
719Proof
720 fs [cv_rep_def,cv_eq_def]
721 \\ Cases_on ‘x = y’ \\ fs []
722 \\ rw [] \\ gvs []
723 \\ fs [from_to_def]
724 \\ metis_tac []
725QED
726
727(*----------------------------------------------------------*
728 word conversions
729 *----------------------------------------------------------*)
730
731Theorem cv_rep_word_w2n[cv_rep]:
732 Num (w2n w) = from_word (w :'a word)
733Proof
734 fs [cv_rep_def] \\ rw [] \\ gvs [from_word_def]
735QED
736
737Theorem cv_rep_word_n2w[cv_rep]:
738 from_word (n2w n : 'a word) = (cv_mod (Num n) (Num (2 ** dimindex (:'a))))
739Proof
740 fs [cv_rep_def] \\ rw [] \\ gvs [from_word_def,dimword_def]
741QED
742
743Theorem cv_rep_word_w2w[cv_rep]:
744 from_word ((w2w (w:'a word)) : 'b word)
745 =
746 if dimindex (:'a) <= dimindex (:'b) then from_word w else
747 cv_mod (from_word w) (Num (2 ** dimindex (:'b)))
748Proof
749 fs [cv_rep_def] \\ rw []
750 \\ gvs [from_word_def,GSYM dimword_def,w2w_def]
751 \\ irule LESS_LESS_EQ_TRANS
752 \\ irule_at Any w2n_lt
753 \\ gvs [dimword_def]
754QED
755
756Theorem cv_inline_word_sw2sw[cv_inline]:
757 sw2sw (w : 'a word) =
758 let v = w
759 in
760 (if word_msb v then -1w << dimindex (:'a) else 0w) + w2w v : 'b word
761Proof
762 rw[sw2sw_w2w_add]
763QED
764
765Theorem cv_rep_dimindex[cv_rep]:
766 Num (dimindex (:'a)) = Num (dimindex (:'a))
767Proof
768 simp[]
769QED
770
771Theorem cv_inline_w2i[cv_inline]:
772 w2i w = let v = w in if word_msb v then -&w2n (-v) else &w2n v
773Proof
774 simp[w2i_def]
775QED
776
777Definition v2n_custom_def:
778 v2n_custom acc [] = acc /\
779 v2n_custom acc (T::rest) = v2n_custom (2 * acc + 1n) rest /\
780 v2n_custom acc (F::rest) = v2n_custom (2 * acc) rest
781End
782
783Theorem v2n_custom_thm:
784 v2n_custom 0 = v2n
785Proof
786 qsuff_tac `!acc l. v2n_custom acc l = v2n l + acc * (2 ** LENGTH l)`
787 >- rw[FUN_EQ_THM] >>
788 recInduct v2n_custom_ind >> rw[v2n_custom_def, v2n] >>
789 simp[RIGHT_ADD_DISTRIB, EXP]
790QED
791
792Theorem cv_inline_v2n[cv_inline] = GSYM v2n_custom_thm;
793
794Theorem cv_inline_v2w[cv_inline] =
795 REWRITE_RULE [GSYM v2n_custom_thm] $ GSYM n2w_v2n;
796
797Theorem cv_inline_w2v[cv_inline]:
798 w2v (w:'a word) = let d = dimindex (:'a) in
799 GENLIST (λi. word_bit (d - 1 - i) w) d
800Proof
801 simp[w2v_def, GENLIST_FUN_EQ, word_bit_def]
802QED
803
804(*----------------------------------------------------------*
805 word arithmetic
806 *----------------------------------------------------------*)
807
808Theorem cv_rep_word_add[cv_rep]:
809 from_word (w1 + w2)
810 =
811 cv_mod (cv_add (from_word (w1 :'a word)) (from_word w2)) (Num (dimword (:'a)))
812Proof
813 fs [cv_rep_def] \\ rw [] \\ gvs [from_word_def]
814 \\ Cases_on ‘w1’ \\ Cases_on ‘w2’ \\ gvs [wordsTheory.word_add_n2w]
815QED
816
817Definition cv_word_sub_def:
818 cv_word_sub x y d =
819 cv_if (cv_lt x y)
820 (cv_sub (cv_add x d) y)
821 (cv_sub x y)
822End
823
824Theorem cv_rep_word_sub[cv_rep]:
825 from_word (w1 - w2 :'a word)
826 =
827 cv_word_sub (from_word w1) (from_word w2) (Num (dimword (:'a)))
828Proof
829 fs [cv_rep_def] \\ rw [] \\ gvs [from_word_def,cv_word_sub_def]
830 \\ Cases_on ‘w1’ \\ Cases_on ‘w2’ \\ gvs []
831 \\ reverse $ Cases_on ‘n < n'’ \\ gvs []
832 >- gvs [arithmeticTheory.NOT_LESS,GSYM wordsTheory.n2w_sub]
833 \\ gvs [wordsTheory.word_sub_def,wordsTheory.word_2comp_n2w]
834 \\ gvs [wordsTheory.word_add_n2w]
835QED
836
837Theorem cv_rep_word_neg[cv_rep]:
838 from_word (- w1 :'a word)
839 =
840 cv_word_sub (Num 0) (from_word w1) (Num (dimword (:'a)))
841Proof
842 rewrite_tac [GSYM wordsTheory.WORD_SUB_LZERO,cv_rep_word_sub]
843 \\ fs [from_word_def]
844QED
845
846Theorem cv_rep_word_mul[cv_rep]:
847 from_word (w1 * w2 :'a word)
848 =
849 cv_mod (cv_mul (from_word w1) (from_word w2)) (Num (dimword (:'a)))
850Proof
851 fs [cv_rep_def] \\ rw [] \\ gvs [from_word_def]
852 \\ Cases_on ‘w1’ \\ Cases_on ‘w2’ \\ gvs [wordsTheory.word_mul_n2w]
853QED
854
855Theorem cv_rep_word_div[cv_rep]:
856 from_word (word_div w1 w2)
857 =
858 cv_div (from_word w1) (from_word w2)
859Proof
860 fs [cv_rep_def] \\ rw [] \\ gvs [from_word_def]
861 \\ Cases_on ‘w1’ \\ Cases_on ‘w2’ \\ gvs [word_div_def]
862 \\ rename [‘n DIV m’] \\ Cases_on ‘m’ \\ fs []
863 \\ gvs [DIV_LT_X] \\ gvs [MULT_CLAUSES]
864QED
865
866Theorem cv_rep_word_mod[cv_rep]:
867 from_word (word_mod w1 w2)
868 =
869 cv_mod (from_word w1) (from_word w2)
870Proof
871 fs [cv_rep_def] \\ rw [] \\ gvs [from_word_def]
872 \\ Cases_on ‘w1’ \\ Cases_on ‘w2’ \\ gvs [word_mod_def]
873 \\ rename [‘n MOD m’] \\ Cases_on ‘m’ \\ fs []
874 \\ irule LESS_EQ_LESS_TRANS
875 \\ last_x_assum $ irule_at Any
876 \\ irule arithmeticTheory.MOD_LESS_EQ \\ fs []
877QED
878
879Theorem cv_inline_word_log2[cv_inline] = word_log2_def;
880
881(*----------------------------------------------------------*
882 word_msb, unit_max, word shifts
883 *----------------------------------------------------------*)
884
885Theorem cv_rep_word_msb[cv_rep]:
886 b2c (word_msb w)
887 =
888 cv_div (from_word (w :'a word)) (Num (2 ** (dimindex (:'a) - 1)))
889Proof
890 rw [Once EQ_SYM_EQ] \\ gvs [from_word_def]
891 \\ Cases_on ‘w’ \\ gvs [wordsTheory.word_msb_def]
892 \\ gvs [wordsTheory.n2w_def,fcpTheory.FCP_BETA,bitTheory.BIT_def,
893 bitTheory.BITS_THM,wordsTheory.dimword_def]
894 \\ ‘0 < dimindex (:'a)’ by fs [fcpTheory.DIMINDEX_GT_0]
895 \\ Cases_on ‘dimindex (:'a)’ \\ gvs []
896 \\ rename [‘SUC l’]
897 \\ ‘0 < 2:num’ by fs []
898 \\ drule arithmeticTheory.DIVISION
899 \\ disch_then $ qspec_then ‘n DIV (2 ** l)’
900 (strip_assume_tac o ONCE_REWRITE_RULE [CONJ_COMM])
901 \\ pop_assum (fn th => simp [Once th])
902 \\ simp [arithmeticTheory.DIV_DIV_DIV_MULT]
903 \\ ‘n DIV (2 * 2 ** l) = 0’ by gvs [DIV_EQ_X,GSYM EXP]
904 \\ asm_rewrite_tac [] \\ simp []
905 \\ drule (DECIDE “n < 2 ==> n = 0 \/ n = 1:num”)
906 \\ strip_tac \\ gvs []
907QED
908
909Theorem cv_rep_word_uint_max[cv_rep]:
910 from_word (UINT_MAXw:'a word)
911 =
912 Num (2 ** dimindex (:'a) - 1)
913Proof
914 rw [cv_rep_def,from_word_def] \\ EVAL_TAC
915 \\ gvs [w2n_n2w,dimword_def]
916QED
917
918Theorem cv_rep_word_lsl[cv_rep]:
919 from_word (word_lsl (w:'a word) n)
920 =
921 cv_mod (cv_mul (from_word w) (cv_exp (Num 2) (Num n)))
922 (Num (2 ** dimindex (:'a)))
923Proof
924 gvs [cv_rep_def] \\ rw [] \\ gvs []
925 \\ gvs [from_word_def,cv_exp_def]
926 \\ Cases_on ‘w’ \\ gvs [word_lsl_n2w]
927 \\ rw [] \\ gvs [dimword_def]
928 \\ ‘0n < 2 ** dimindex (:'a)’ by gvs []
929 \\ once_rewrite_tac [GSYM MOD_TIMES2]
930 \\ qsuff_tac ‘2 ** n MOD 2 ** dimindex (:'a) = 0’ \\ gvs []
931 \\ ‘dimindex (:'a) <= n’ by fs []
932 \\ gvs [LESS_EQ_EXISTS,EXP_ADD]
933QED
934
935Theorem cv_rep_word_lsr[cv_rep]:
936 from_word (word_lsr (w:'a word) n)
937 =
938 let k = Num n in
939 cv_if (cv_lt k (Num (dimindex (:'a))))
940 (cv_div (from_word w) (cv_exp (Num 2) k))
941 (Num 0)
942Proof
943 gvs [cv_rep_def] \\ rw [] \\ gvs []
944 >- gvs [from_word_def,cv_exp_def,w2n_lsr]
945 \\ gvs[from_word_def]
946 \\ irule LSR_LIMIT
947 \\ pop_assum mp_tac \\ rw[]
948QED
949
950Theorem word_asr_add[cv_inline]:
951 w >> n =
952 let x = w in
953 if word_msb (x :'a word) then
954 (dimindex (:'a) - 1 '' dimindex (:'a) - n) UINT_MAXw + (x >>> n)
955 else x >>> n
956Proof
957 simp []
958 \\ dep_rewrite.DEP_REWRITE_TAC [WORD_ADD_OR]
959 \\ conj_tac >-
960 (gvs [fcpTheory.CART_EQ,word_and_def,word_bits_def,
961 wordsTheory.word_0,fcpTheory.FCP_BETA,word_slice_def]
962 \\ rpt strip_tac \\ CCONTR_TAC \\ gvs [word_T,word_lsr_def]
963 \\ gvs [fcpTheory.FCP_BETA])
964 \\ rw [word_asr]
965QED
966
967Theorem cv_inline_word_ror[cv_inline]:
968 !r a. (a : 'a word) #>> r =
969 let a = a;
970 d = dimindex (:'a);
971 r = r MOD d
972 in a << (d - r) || a >>> r
973Proof
974 rw[word_ror_alt]
975QED
976
977(*----------------------------------------------------------*
978 word comparisons (unsigned and signed)
979 *----------------------------------------------------------*)
980
981Theorem cv_word_lo_thm[cv_rep]:
982 b2c (word_lo w1 w2) = cv_lt (from_word w1) (from_word w2)
983Proof
984 fs [from_word_def] \\ rw [WORD_LO]
985QED
986
987Theorem cv_word_hi_thm[cv_rep]:
988 b2c (word_hi w2 w1) = cv_lt (from_word w1) (from_word w2)
989Proof
990 fs [from_word_def] \\ rw [WORD_HI]
991QED
992
993Theorem cv_word_hs_thm[cv_rep]:
994 b2c (word_hs w1 w2) = cv_sub (Num 1) (cv_lt (from_word w1) (from_word w2))
995Proof
996 simp [GSYM cv_word_hi_thm,GSYM cv_rep_not,WORD_HS,WORD_HI,
997 GREATER_EQ,GREATER_DEF,NOT_LESS]
998QED
999
1000Theorem cv_word_ls_thm[cv_rep]:
1001 b2c (word_ls w1 w2) = cv_sub (Num 1) (cv_lt (from_word w2) (from_word w1))
1002Proof
1003 simp [GSYM cv_word_hi_thm,GSYM cv_rep_not]
1004 \\ rw [WORD_HI,WORD_LS,NOT_LESS,arithmeticTheory.GREATER_DEF]
1005QED
1006
1007Definition cv_word_lt_def:
1008 cv_word_lt w1 w2 msb1 msb2 =
1009 cv_if (cv_eq msb1 msb2)
1010 (cv_lt w1 w2)
1011 (cv_if msb1 (Num 1) (cv_sub (Num 1) msb2))
1012End
1013
1014Theorem cv_word_lt_thm[cv_rep]:
1015 b2c (word_lt w1 w2)
1016 =
1017 cv_word_lt (from_word w1) (from_word (w2:'a word))
1018 (cv_div (from_word w1) (Num (2 ** (dimindex (:'a) - 1))))
1019 (cv_div (from_word w2) (Num (2 ** (dimindex (:'a) - 1))))
1020Proof
1021 rewrite_tac [GSYM cv_rep_word_msb] \\ simp [Once EQ_SYM_EQ]
1022 \\ gvs [cv_word_lt_def]
1023 \\ ‘!b1 b2. (c2b (cv_eq (b2c b1) (b2c b2)) ⇔ b1 = b2) ∧ c2b (b2c b1) = b1’ by
1024 (Cases \\ Cases \\ gvs [])
1025 \\ simp [GSYM cv_word_lo_thm,GSYM cv_rep_not,wordsTheory.WORD_LT,WORD_LO]
1026 \\ rw [] \\ gvs []
1027QED
1028
1029Theorem cv_word_gt_thm[cv_rep]:
1030 b2c (word_gt w2 w1)
1031 =
1032 cv_word_lt (from_word w1) (from_word (w2:'a word))
1033 (cv_div (from_word w1) (Num (2 ** (dimindex (:'a) - 1))))
1034 (cv_div (from_word w2) (Num (2 ** (dimindex (:'a) - 1))))
1035Proof
1036 rewrite_tac [wordsTheory.WORD_GREATER,cv_word_lt_thm]
1037QED
1038
1039Theorem cv_word_le_thm[cv_rep]:
1040 b2c (word_le w2 w1)
1041 =
1042 cv_sub (Num 1)
1043 (cv_word_lt (from_word w1) (from_word (w2:'a word))
1044 (cv_div (from_word w1) (Num (2 ** (dimindex (:'a) - 1))))
1045 (cv_div (from_word w2) (Num (2 ** (dimindex (:'a) - 1)))))
1046Proof
1047 rewrite_tac [GSYM cv_word_lt_thm,GSYM cv_rep_not,WORD_NOT_LESS]
1048QED
1049
1050Theorem cv_word_ge_thm[cv_rep]:
1051 b2c (word_ge w1 w2)
1052 =
1053 cv_sub (Num 1)
1054 (cv_word_lt (from_word w1) (from_word (w2:'a word))
1055 (cv_div (from_word w1) (Num (2 ** (dimindex (:'a) - 1))))
1056 (cv_div (from_word w2) (Num (2 ** (dimindex (:'a) - 1)))))
1057Proof
1058 rewrite_tac [cv_word_le_thm,wordsTheory.WORD_GREATER_EQ]
1059QED
1060
1061(*----------------------------------------------------------*
1062 word bits, slice, extract, concat
1063 *----------------------------------------------------------*)
1064
1065Theorem cv_word_bit_thm[cv_rep]:
1066 b2c (word_bit b w) =
1067 cv_mod (cv_div (from_word w) (cv_exp (Num 2) (Num b))) (Num 2)
1068Proof
1069 Cases_on `w` >> simp[word_bit_n2w] >>
1070 simp[GSYM cv_rep_exp, from_word_def] >>
1071 simp[bitTheory.BIT_DEF] >>
1072 simp[LE_LT1] >> `dimindex (:'a) <> 0` by gvs[] >> simp[] >>
1073 Cases_on `b < dimindex (:'a)` >> gvs[]
1074 >- (
1075 simp[oneline b2c_def] >> rw[] >> gvs[] >>
1076 qspecl_then [`n DIV 2 ** b`,`2`] assume_tac MOD_LESS >> simp[]
1077 ) >>
1078 gvs[dimword_def] >>
1079 qsuff_tac `n DIV 2 ** b = 0` >> gvs[] >>
1080 irule LESS_DIV_EQ_ZERO >> gvs[NOT_LESS] >>
1081 irule LESS_LESS_EQ_TRANS >> goal_assum drule >> simp[]
1082QED
1083
1084Theorem MIN_lemma[local]:
1085 l <> 0 ==> MIN k (l - 1) + 1 = MIN (k+1) l
1086Proof
1087 rw [MIN_DEF] \\ gvs []
1088QED
1089
1090Theorem cv_word_bits_thm[cv_rep]:
1091 from_word (word_bits h l (w:'a word))
1092 =
1093 cv_div (cv_mod (from_word w)
1094 (cv_exp (Num 2) (cv_min (cv_add (Num h) (Num 1))
1095 (Num (dimindex (:'a))))))
1096 (cv_exp (Num 2) (Num l))
1097Proof
1098 simp [Once EQ_SYM_EQ]
1099 \\ ‘w = n2w (w2n w)’ by fs []
1100 \\ pop_assum (fn th => once_rewrite_tac [th])
1101 \\ rewrite_tac [word_bits_n2w,bitTheory.BITS_THM2,cv_add_def,GSYM cv_min_thm,
1102 cv_exp_def,c2n_def]
1103 \\ gvs [from_word_def,ADD1,MIN_lemma,w2n_lt]
1104 \\ gvs [DIV_LT_X]
1105 \\ match_mp_tac LESS_EQ_LESS_TRANS
1106 \\ irule_at (Pos hd) arithmeticTheory.MOD_LESS_EQ
1107 \\ gvs []
1108 \\ match_mp_tac LESS_LESS_EQ_TRANS
1109 \\ irule_at (Pos hd) w2n_lt
1110 \\ gvs []
1111QED
1112
1113Theorem cv_word_slice_thm[cv_rep]:
1114 from_word (word_slice h l (w:'a word))
1115 =
1116 cv_mod (cv_mul
1117 (cv_div (cv_mod (from_word w)
1118 (cv_exp (Num 2)
1119 (cv_min (cv_add (Num h) (Num 1))
1120 (Num (dimindex (:'a))))))
1121 (cv_exp (Num 2) (Num l)))
1122 (cv_exp (Num 2) (Num l))) (Num (dimword (:'a)))
1123Proof
1124 rewrite_tac [GSYM cv_word_bits_thm,wordsTheory.WORD_SLICE_THM]
1125 \\ rewrite_tac [cv_rep_word_lsl,cv_exp_def] \\ fs []
1126 \\ simp [from_word_def,dimword_def]
1127QED
1128
1129Theorem cv_word_extract[cv_rep] =
1130 “from_word (word_extract h l (w:'a word) : 'b word)”
1131 |> SIMP_CONV std_ss [word_extract_def,cv_rep_word_w2w,cv_word_bits_thm];
1132
1133Theorem word_join_add[local]:
1134 FINITE univ(:'a) /\ FINITE univ(:'b) ==>
1135 word_join (v:'a word) (w:'b word) =
1136 (w2w v << dimindex (:'b)) + w2w w
1137Proof
1138 simp [word_join_def]
1139 \\ once_rewrite_tac [EQ_SYM_EQ] \\ rw []
1140 \\ irule WORD_ADD_OR
1141 \\ gvs [fcpTheory.CART_EQ,word_and_def,fcpTheory.FCP_BETA,word_lsl_def,w2w]
1142 \\ gvs [fcpTheory.index_sum,wordsTheory.word_0,NOT_LESS]
1143 \\ metis_tac []
1144QED
1145
1146Theorem cv_word_join_thm[cv_rep]:
1147 FINITE univ(:'a) /\ FINITE univ(:'b) ==>
1148 from_word (word_join (w1:'a word) (w2:'b word))
1149 =
1150 cv_add (cv_mul (from_word w1) (cv_exp (Num 2) (Num (dimindex (:'b)))))
1151 (from_word w2)
1152Proof
1153 simp [word_join_add, cv_rep_word_add, cv_rep_word_lsl, cv_rep_word_w2w]
1154 \\ gvs [fcpTheory.index_sum]
1155 \\ gvs [from_word_def,cv_add_def,cv_mod_def,cv_mul_def,cv_exp_def]
1156 \\ gvs [GSYM dimword_def]
1157 \\ ‘(dimword (:'b) * w2n w1) < 2 ** (dimindex (:'a) + dimindex (:'b))’ by
1158 (once_rewrite_tac [ADD_COMM]
1159 \\ rewrite_tac [EXP_ADD,dimword_def,LT_MULT_LCANCEL]
1160 \\ simp [GSYM dimword_def,w2n_lt])
1161 \\ rpt strip_tac \\ gvs []
1162 \\ qsuff_tac ‘(w2n w2 + dimword (:'b) * w2n w1) < dimword (:'a + 'b)’ >- fs []
1163 \\ simp [dimword_def] \\ gvs [fcpTheory.index_sum,EXP_ADD]
1164 \\ irule LESS_LESS_EQ_TRANS
1165 \\ rewrite_tac [GSYM dimword_def]
1166 \\ qexists_tac ‘SUC (w2n w1) * dimword (:'b)’
1167 \\ gvs [LE_MULT_RCANCEL] \\ gvs [DECIDE “SUC n <= k <=> n < k”, w2n_lt]
1168 \\ gvs [MULT_CLAUSES,w2n_lt]
1169QED
1170
1171Theorem cv_word_concat_thm[cv_rep] =
1172 “from_word (((w1:'a word) @@ (w2:'b word)) :'c word)”
1173 |> REWRITE_CONV [word_concat_def,cv_rep_word_w2w,
1174 UNDISCH cv_word_join_thm]
1175 |> DISCH_ALL
1176 |> SIMP_RULE std_ss [fcpTheory.index_sum];
1177
1178(*----------------------------------------------------------*
1179 word or, and, xor
1180 *----------------------------------------------------------*)
1181
1182Definition cv_word_or_loop_def:
1183 cv_word_or_loop x y =
1184 if c2b (cv_lt (Num 0) x) then
1185 cv_add (cv_mul (Num 2)
1186 (cv_word_or_loop (cv_div x (Num 2)) (cv_div y (Num 2))))
1187 (cv_max (cv_mod x (Num 2)) (cv_mod y (Num 2)))
1188 else y
1189Termination
1190 WF_REL_TAC ‘measure (c2n o FST)’ \\ Cases \\ fs [] \\ rw []
1191End
1192
1193Theorem cv_word_or_loop_def[allow_rebind] = cv_word_or_loop_def
1194 |> REWRITE_RULE [GSYM cvTheory.cv_if]
1195
1196Definition cv_word_or_def:
1197 cv_word_or x y =
1198 cv_if (cv_lt x y)
1199 (cv_word_or_loop x y)
1200 (cv_word_or_loop y x)
1201End
1202
1203Definition cv_word_and_loop_def:
1204 cv_word_and_loop x y =
1205 if c2b (cv_lt (Num 0) x) then
1206 cv_add (cv_mul (Num 2)
1207 (cv_word_and_loop (cv_div x (Num 2)) (cv_div y (Num 2))))
1208 (cv_div (cv_add (cv_mod x (Num 2)) (cv_mod y (Num 2))) (Num 2))
1209 else (Num 0)
1210Termination
1211 WF_REL_TAC ‘measure (c2n o FST)’ \\ Cases \\ fs [] \\ rw []
1212End
1213
1214Theorem cv_word_and_loop_def[allow_rebind] = cv_word_and_loop_def
1215 |> REWRITE_RULE [GSYM cvTheory.cv_if]
1216
1217Definition cv_word_and_def:
1218 cv_word_and x y =
1219 cv_if (cv_lt x y)
1220 (cv_word_and_loop x y)
1221 (cv_word_and_loop y x)
1222End
1223
1224Definition cv_word_xor_loop_def:
1225 cv_word_xor_loop x y =
1226 if c2b (cv_lt (Num 0) x) then
1227 cv_add (cv_mul (Num 2)
1228 (cv_word_xor_loop (cv_div x (Num 2)) (cv_div y (Num 2))))
1229 (cv_mod (cv_add (cv_mod x (Num 2)) (cv_mod y (Num 2))) (Num 2))
1230 else y
1231Termination
1232 WF_REL_TAC ‘measure (c2n o FST)’ \\ Cases \\ fs [] \\ rw []
1233End
1234
1235Theorem cv_word_xor_loop_def[allow_rebind] = cv_word_xor_loop_def
1236 |> REWRITE_RULE [GSYM cvTheory.cv_if]
1237
1238Definition cv_word_xor_def:
1239 cv_word_xor x y =
1240 cv_if (cv_lt x y)
1241 (cv_word_xor_loop x y)
1242 (cv_word_xor_loop y x)
1243End
1244
1245Theorem BITWISE_ADD:
1246 !l k m n b.
1247 BITWISE (l + k) b m n =
1248 BITWISE l b m n +
1249 BITWISE k b (m DIV 2 ** l) (n DIV 2 ** l) * 2 ** l
1250Proof
1251 Induct_on ‘k’
1252 \\ fs [bitTheory.BITWISE_def,arithmeticTheory.ADD_CLAUSES]
1253 \\ rw []
1254 \\ rewrite_tac [arithmeticTheory.ADD_ASSOC,arithmeticTheory.EQ_ADD_RCANCEL]
1255 \\ simp_tac std_ss [AC arithmeticTheory.ADD_ASSOC arithmeticTheory.ADD_COMM]
1256 \\ simp_tac std_ss [AC arithmeticTheory.MULT_ASSOC arithmeticTheory.MULT_COMM]
1257 \\ simp_tac std_ss [arithmeticTheory.LEFT_ADD_DISTRIB]
1258 \\ simp_tac std_ss [AC arithmeticTheory.ADD_ASSOC arithmeticTheory.ADD_COMM]
1259 \\ simp_tac std_ss [AC arithmeticTheory.MULT_ASSOC arithmeticTheory.MULT_COMM]
1260 \\ simp [DECIDE “m + n = n + k <=> m = k:num”]
1261 \\ simp_tac std_ss [Once arithmeticTheory.MULT_COMM]
1262 \\ rewrite_tac [GSYM bitTheory.SBIT_MULT]
1263 \\ rewrite_tac [GSYM bitTheory.BIT_SHIFT_THM4]
1264QED
1265
1266Theorem BITWISE:
1267 BITWISE 0 b m n = 0 /\
1268 BITWISE (SUC k) b m n =
1269 (if b (ODD m) (ODD n) then 1 else 0) + 2 * BITWISE k b (m DIV 2) (n DIV 2)
1270Proof
1271 rewrite_tac [DECIDE “SUC n = 1 + n”,BITWISE_ADD] \\ gvs []
1272 \\ rewrite_tac [DECIDE “1 = SUC 0”,bitTheory.BITWISE_def] \\ gvs []
1273 \\ gvs [bitTheory.SBIT_def,bitTheory.BIT0_ODD]
1274QED
1275
1276Theorem cv_word_and_loop_thm:
1277 !m n.
1278 m <= n /\ n < dimword (:'a) ==>
1279 cv_word_and_loop (Num m) (Num n) = Num (w2n (n2w m && n2w n :'a word))
1280Proof
1281 simp [wordsTheory.word_and_n2w,wordsTheory.dimword_def,
1282 bitTheory.BITWISE_LT_2EXP]
1283 \\ Q.SPEC_TAC (‘dimindex (:'a)’,‘l’)
1284 \\ completeInduct_on ‘m’
1285 \\ simp [Once cv_word_and_loop_def]
1286 \\ Cases_on ‘m = 0’ \\ fs [wordsTheory.WORD_AND_CLAUSES]
1287 \\ gvs [PULL_FORALL,AND_IMP_INTRO] \\ rw []
1288 \\ Cases_on ‘l’ \\ gvs []
1289 \\ rename [‘n < 2 ** SUC l’]
1290 \\ gvs [BITWISE]
1291 \\ first_x_assum $ qspecl_then [‘m DIV 2’,‘l’,‘n DIV 2’] mp_tac
1292 \\ impl_tac
1293 >- (gvs [] \\ irule_at Any arithmeticTheory.DIV_LE_MONOTONE \\ gvs [])
1294 \\ strip_tac \\ gvs [bitTheory.BITWISE_LT_2EXP,wordsTheory.dimword_def]
1295 \\ Cases_on ‘ODD m’
1296 \\ Cases_on ‘ODD n’
1297 \\ imp_res_tac bitTheory.ODD_MOD2_LEM
1298 \\ gvs [arithmeticTheory.ODD_EVEN]
1299 \\ imp_res_tac arithmeticTheory.EVEN_MOD2 \\ gvs []
1300QED
1301
1302Theorem cv_word_or_loop_thm:
1303 !m n.
1304 m <= n /\ n < dimword (:'a) ==>
1305 cv_word_or_loop (Num m) (Num n) = Num (w2n (n2w m || n2w n :'a word))
1306Proof
1307 simp [wordsTheory.word_or_n2w,wordsTheory.dimword_def,
1308 bitTheory.BITWISE_LT_2EXP]
1309 \\ Q.SPEC_TAC (‘dimindex (:'a)’,‘l’)
1310 \\ completeInduct_on ‘m’
1311 \\ simp [Once cv_word_or_loop_def]
1312 \\ Cases_on ‘m = 0’ \\ fs [wordsTheory.WORD_OR_CLAUSES]
1313 >-
1314 (Induct \\ fs [BITWISE]
1315 \\ rpt strip_tac
1316 \\ ‘0 < 2:num’ by fs []
1317 \\ drule_then strip_assume_tac arithmeticTheory.DIVISION
1318 \\ pop_assum $ qspec_then ‘n’ mp_tac \\ strip_tac
1319 \\ pop_assum kall_tac
1320 \\ pop_assum (fn th => simp [Once th])
1321 \\ first_x_assum $ qspec_then ‘n DIV 2’ mp_tac
1322 \\ impl_tac >- gvs []
1323 \\ disch_then (fn th => simp [Once th])
1324 \\ Cases_on ‘ODD n’
1325 \\ imp_res_tac bitTheory.ODD_MOD2_LEM \\ gvs []
1326 \\ gvs [arithmeticTheory.ODD_EVEN]
1327 \\ imp_res_tac arithmeticTheory.EVEN_MOD2 \\ gvs [])
1328 \\ gvs [PULL_FORALL,AND_IMP_INTRO,GSYM cv_max_thm] \\ rw []
1329 \\ Cases_on ‘l’ \\ gvs []
1330 \\ rename [‘n < 2 ** SUC l’]
1331 \\ gvs [BITWISE]
1332 \\ first_x_assum $ qspecl_then [‘m DIV 2’,‘l’,‘n DIV 2’] mp_tac
1333 \\ impl_tac
1334 >- (gvs [] \\ irule_at Any arithmeticTheory.DIV_LE_MONOTONE \\ gvs [])
1335 \\ strip_tac \\ gvs [bitTheory.BITWISE_LT_2EXP,wordsTheory.dimword_def]
1336 \\ Cases_on ‘ODD m’
1337 \\ Cases_on ‘ODD n’
1338 \\ imp_res_tac bitTheory.ODD_MOD2_LEM
1339 \\ gvs []
1340 \\ gvs [arithmeticTheory.ODD_EVEN]
1341 \\ imp_res_tac arithmeticTheory.EVEN_MOD2 \\ gvs []
1342QED
1343
1344Theorem cv_word_xor_loop_thm:
1345 !m n.
1346 m <= n /\ n < dimword (:'a) ==>
1347 cv_word_xor_loop (Num m) (Num n) =
1348 Num (w2n (word_xor (n2w m) (n2w n) :'a word))
1349Proof
1350 simp [wordsTheory.word_xor_n2w,wordsTheory.dimword_def,
1351 bitTheory.BITWISE_LT_2EXP]
1352 \\ Q.SPEC_TAC (‘dimindex (:'a)’,‘l’)
1353 \\ completeInduct_on ‘m’
1354 \\ simp [Once cv_word_xor_loop_def]
1355 \\ Cases_on ‘m = 0’ \\ fs [wordsTheory.WORD_XOR_CLAUSES]
1356 >-
1357 (Induct \\ fs [BITWISE]
1358 \\ rpt strip_tac
1359 \\ ‘0 < 2:num’ by fs []
1360 \\ drule_then strip_assume_tac arithmeticTheory.DIVISION
1361 \\ pop_assum $ qspec_then ‘n’ mp_tac \\ strip_tac
1362 \\ pop_assum kall_tac
1363 \\ pop_assum (fn th => simp [Once th])
1364 \\ first_x_assum $ qspec_then ‘n DIV 2’ mp_tac
1365 \\ impl_tac >- gvs []
1366 \\ disch_then (fn th => simp [Once th])
1367 \\ Cases_on ‘ODD n’
1368 \\ imp_res_tac bitTheory.ODD_MOD2_LEM \\ gvs []
1369 \\ gvs [arithmeticTheory.ODD_EVEN]
1370 \\ imp_res_tac arithmeticTheory.EVEN_MOD2 \\ gvs [])
1371 \\ gvs [PULL_FORALL,AND_IMP_INTRO] \\ rw []
1372 \\ Cases_on ‘l’ \\ gvs []
1373 \\ rename [‘n < 2 ** SUC l’]
1374 \\ gvs [BITWISE]
1375 \\ first_x_assum $ qspecl_then [‘m DIV 2’,‘l’,‘n DIV 2’] mp_tac
1376 \\ impl_tac
1377 >- (gvs [] \\ irule_at Any arithmeticTheory.DIV_LE_MONOTONE \\ gvs [])
1378 \\ strip_tac \\ gvs [bitTheory.BITWISE_LT_2EXP,wordsTheory.dimword_def]
1379 \\ ‘0 < 2:num’ by fs []
1380 \\ simp_tac std_ss [Once (GSYM arithmeticTheory.MOD_PLUS)]
1381 \\ Cases_on ‘ODD m’
1382 \\ Cases_on ‘ODD n’
1383 \\ imp_res_tac bitTheory.ODD_MOD2_LEM
1384 \\ full_simp_tac std_ss [arithmeticTheory.ODD_EVEN]
1385 \\ imp_res_tac arithmeticTheory.EVEN_MOD2
1386 \\ full_simp_tac std_ss [arithmeticTheory.ODD_EVEN]
1387QED
1388
1389Theorem cv_rep_word_and[cv_rep]:
1390 from_word (w1 && w2)
1391 =
1392 cv_word_and (from_word w1) (from_word w2)
1393Proof
1394 fs [cv_rep_def] \\ rw [] \\ gvs [from_word_def]
1395 \\ rw [cv_word_and_def]
1396 \\ Cases_on ‘w1’ \\ Cases_on ‘w2’ \\ gvs []
1397 \\ Cases_on ‘n < n'’ \\ gvs []
1398 >-
1399 (‘n <= n'’ by fs [] \\ pop_assum mp_tac \\ pop_assum kall_tac \\ rw []
1400 \\ drule_all cv_word_and_loop_thm
1401 \\ strip_tac \\ gvs [])
1402 \\ gvs [arithmeticTheory.NOT_LESS]
1403 \\ drule_all cv_word_and_loop_thm
1404 \\ strip_tac \\ gvs []
1405 \\ simp [Once wordsTheory.WORD_AND_COMM]
1406QED
1407
1408Theorem cv_rep_word_or[cv_rep]:
1409 from_word (w1 || w2)
1410 =
1411 cv_word_or (from_word w1) (from_word w2)
1412Proof
1413 fs [cv_rep_def] \\ rw [] \\ gvs [from_word_def]
1414 \\ rw [cv_word_or_def]
1415 \\ Cases_on ‘w1’ \\ Cases_on ‘w2’ \\ gvs []
1416 \\ Cases_on ‘n < n'’ \\ gvs []
1417 >-
1418 (‘n <= n'’ by fs [] \\ pop_assum mp_tac \\ pop_assum kall_tac \\ rw []
1419 \\ drule_all cv_word_or_loop_thm
1420 \\ strip_tac \\ gvs [])
1421 \\ gvs [arithmeticTheory.NOT_LESS]
1422 \\ drule_all cv_word_or_loop_thm
1423 \\ strip_tac \\ gvs []
1424 \\ simp [Once wordsTheory.WORD_OR_COMM]
1425QED
1426
1427Theorem cv_rep_word_xor[cv_rep]:
1428 from_word (word_xor w1 w2)
1429 =
1430 cv_word_xor (from_word w1) (from_word w2)
1431Proof
1432 fs [cv_rep_def] \\ rw [] \\ gvs [from_word_def]
1433 \\ rw [cv_word_xor_def]
1434 \\ Cases_on ‘w1’ \\ Cases_on ‘w2’ \\ gvs []
1435 \\ Cases_on ‘n < n'’ \\ gvs []
1436 >-
1437 (‘n <= n'’ by fs [] \\ pop_assum mp_tac \\ pop_assum kall_tac \\ rw []
1438 \\ drule_all cv_word_xor_loop_thm
1439 \\ strip_tac \\ gvs [])
1440 \\ gvs [arithmeticTheory.NOT_LESS]
1441 \\ drule_all cv_word_xor_loop_thm
1442 \\ strip_tac \\ gvs []
1443 \\ simp [Once wordsTheory.WORD_XOR_COMM]
1444QED
1445
1446Theorem cv_rep_word_not[cv_rep]:
1447 from_word (~ w :'a word)
1448 =
1449 cv_word_xor (from_word w) (Num (2 ** dimindex (:'a) - 1))
1450Proof
1451 ‘~w = w ?? UINT_MAXw’ by fs [WORD_XOR_CLAUSES]
1452 \\ asm_rewrite_tac [cv_rep_word_xor, cv_rep_word_uint_max]
1453QED