File: theorems.tex

package info (click to toggle)
hol88 2.02.19940316-35
  • links: PTS
  • area: main
  • in suites: bullseye, buster, sid
  • size: 65,988 kB
  • ctags: 21,623
  • sloc: ml: 199,939; ansic: 9,666; sh: 7,118; makefile: 6,095; lisp: 2,747; yacc: 894; sed: 201; cpp: 87; awk: 5
file content (761 lines) | stat: -rw-r--r-- 21,946 bytes parent folder | download | duplicates (5)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
\chapter{Pre-proved Theorems}\input{theorems-intro}\section{The theory {\tt word\_base}}\THEOREM BIT0 word\_base
|- !b. BIT 0(WORD[b]) = b
\ENDTHEOREM
\THEOREM BIT\_DEF word\_base
|- !k l. BIT k(WORD l) = ELL k l
\ENDTHEOREM
\THEOREM BIT\_EQ\_IMP\_WORD\_EQ word\_base
|- !n.
    !w1 w2 :: PWORDLEN n.
     (!k. k < n ==> (BIT k w1 = BIT k w2)) ==> (w1 = w2)
\ENDTHEOREM
\THEOREM BIT\_WCAT1 word\_base
|- !n. !w :: PWORDLEN n. !b. BIT n(WCAT(WORD[b],w)) = b
\ENDTHEOREM
\THEOREM BIT\_WCAT\_FST word\_base
|- !n1 n2.
    !w1 :: PWORDLEN n1.
     !w2 :: PWORDLEN n2.
      !k.
       n2 <= k /\ k < (n1 + n2) ==> (BIT k(WCAT(w1,w2)) = BIT(k - n2)w1)
\ENDTHEOREM
\THEOREM BIT\_WCAT\_SND word\_base
|- !n1 n2.
    !w1 :: PWORDLEN n1.
     !w2 :: PWORDLEN n2. !k. k < n2 ==> (BIT k(WCAT(w1,w2)) = BIT k w2)
\ENDTHEOREM
\THEOREM BIT\_WSEG word\_base
|- !n.
    !w :: PWORDLEN n.
     !m k j.
      (m + k) <= n ==> j < m ==> (BIT j(WSEG m k w) = BIT(j + k)w)
\ENDTHEOREM
\THEOREM LSB\_DEF word\_base
|- !l. LSB(WORD l) = LAST l
\ENDTHEOREM
\THEOREM LSB word\_base
|- !n. !w :: PWORDLEN n. 0 < n ==> (LSB w = BIT 0 w)
\ENDTHEOREM
\THEOREM MSB\_DEF word\_base
|- !l. MSB(WORD l) = HD l
\ENDTHEOREM
\THEOREM MSB word\_base
|- !n. !w :: PWORDLEN n. 0 < n ==> (MSB w = BIT(PRE n)w)
\ENDTHEOREM
\THEOREM PWORDLEN0 word\_base
|- !w. PWORDLEN 0 w ==> (w = WORD[])
\ENDTHEOREM
\THEOREM PWORDLEN1 word\_base
|- !x. PWORDLEN 1(WORD[x])
\ENDTHEOREM
\THEOREM PWORDLEN\_DEF word\_base
|- !n l. PWORDLEN n(WORD l) = (n = LENGTH l)
\ENDTHEOREM
\THEOREM PWORDLEN word\_base
|- !n w. PWORDLEN n w = (WORDLEN w = n)
\ENDTHEOREM
\THEOREM WCAT0 word\_base
|- !w. (WCAT(WORD[],w) = w) /\ (WCAT(w,WORD[]) = w)
\ENDTHEOREM
\THEOREM WCAT\_11 word\_base
|- !m n.
    !wm1 wm2 :: PWORDLEN m.
     !wn1 wn2 :: PWORDLEN n.
      (WCAT(wm1,wn1) = WCAT(wm2,wn2)) = (wm1 = wm2) /\ (wn1 = wn2)
\ENDTHEOREM
\THEOREM WCAT\_ASSOC word\_base
|- !w1 w2 w3. WCAT(w1,WCAT(w2,w3)) = WCAT(WCAT(w1,w2),w3)
\ENDTHEOREM
\THEOREM WCAT\_DEF word\_base
|- !l1 l2. WCAT(WORD l1,WORD l2) = WORD(APPEND l1 l2)
\ENDTHEOREM
\THEOREM WCAT\_PWORDLEN word\_base
|- !n1.
    !w1 :: PWORDLEN n1.
     !n2. !w2 :: PWORDLEN n2. PWORDLEN(n1 + n2)(WCAT(w1,w2))
\ENDTHEOREM
\THEOREM WCAT\_WSEG\_WSEG word\_base
|- !n.
    !w :: PWORDLEN n.
     !m1 m2 k.
      (m1 + (m2 + k)) <= n ==>
      (WCAT(WSEG m2(m1 + k)w,WSEG m1 k w) = WSEG(m1 + m2)k w)
\ENDTHEOREM
\THEOREM WORD\_11 word\_base
|- !l l'. (WORD l = WORD l') = (l = l')
\ENDTHEOREM
\THEOREM word\_Ax word\_base
|- !f. ?! fn. !l. fn(WORD l) = f l
\ENDTHEOREM
\THEOREM word\_cases word\_base
|- !w. ?l. w = WORD l
\ENDTHEOREM
\THEOREM WORD\_CONS\_WCAT word\_base
|- !x l. WORD(CONS x l) = WCAT(WORD[x],WORD l)
\ENDTHEOREM
\THEOREM WORD\_DEF word\_base
|- !l. WORD l = ABS_word(Node l[])
\ENDTHEOREM
\THEOREM word\_induct word\_base
|- !P. (!l. P(WORD l)) ==> (!w. P w)
\ENDTHEOREM
\THEOREM word\_ISO\_DEF word\_base
|- (!a. ABS_word(REP_word a) = a) /\
   (!r.
     TRP(\v tl. (?l. v = l) /\ (LENGTH tl = 0))r =
     (REP_word(ABS_word r) = r))
\ENDTHEOREM
\THEOREM WORDLEN\_DEF word\_base
|- !l. WORDLEN(WORD l) = LENGTH l
\ENDTHEOREM
\THEOREM WORDLEN\_SUC\_WCAT\_BIT\_WSEG word\_base
|- !n. !w :: PWORDLEN(SUC n). w = WCAT(WORD[BIT n w],WSEG n 0 w)
\ENDTHEOREM
\THEOREM WORDLEN\_SUC\_WCAT\_BIT\_WSEG\_RIGHT word\_base
|- !n. !w :: PWORDLEN(SUC n). w = WCAT(WSEG n 1 w,WORD[BIT 0 w])
\ENDTHEOREM
\THEOREM WORDLEN\_SUC\_WCAT word\_base
|- !n w.
    PWORDLEN(SUC n)w ==>
    (?b :: PWORDLEN 1. ?w' :: PWORDLEN n. w = WCAT(b,w'))
\ENDTHEOREM
\THEOREM WORDLEN\_SUC\_WCAT\_WSEG\_WSEG word\_base
|- !w :: PWORDLEN(SUC n). w = WCAT(WSEG 1 n w,WSEG n 0 w)
\ENDTHEOREM
\THEOREM WORDLEN\_SUC\_WCAT\_WSEG\_WSEG\_RIGHT word\_base
|- !w :: PWORDLEN(SUC n). w = WCAT(WSEG n 1 w,WSEG 1 0 w)
\ENDTHEOREM
\THEOREM WORD\_PARTITION word\_base
|- (!n. !w :: PWORDLEN n. !m. m <= n ==> (WCAT(WSPLIT m w) = w)) /\
   (!n m.
     !w1 :: PWORDLEN n. !w2 :: PWORDLEN m. WSPLIT m(WCAT(w1,w2)) = w1,w2)
\ENDTHEOREM
\THEOREM WORD\_SNOC\_WCAT word\_base
|- !x l. WORD(SNOC x l) = WCAT(WORD l,WORD[x])
\ENDTHEOREM
\THEOREM WORD\_SPLIT word\_base
|- !n1 n2. !w :: PWORDLEN(n1 + n2). w = WCAT(WSEG n1 n2 w,WSEG n2 0 w)
\ENDTHEOREM
\THEOREM word\_TY\_DEF word\_base
|- ?rep. TYPE_DEFINITION(TRP(\v tl. (?l. v = l) /\ (LENGTH tl = 0)))rep
\ENDTHEOREM
\THEOREM WSEG0 word\_base
|- !k w. WSEG 0 k w = WORD[]
\ENDTHEOREM
\THEOREM WSEG\_BIT word\_base
|- !n. !w :: PWORDLEN n. !k. k < n ==> (WSEG 1 k w = WORD[BIT k w])
\ENDTHEOREM
\THEOREM WSEG\_DEF word\_base
|- !m k l. WSEG m k(WORD l) = WORD(LASTN m(BUTLASTN k l))
\ENDTHEOREM
\THEOREM WSEG\_PWORDLEN word\_base
|- !n. !w :: PWORDLEN n. !m k. (m + k) <= n ==> PWORDLEN m(WSEG m k w)
\ENDTHEOREM
\THEOREM WSEG\_WCAT1 word\_base
|- !n1 n2.
    !w1 :: PWORDLEN n1. !w2 :: PWORDLEN n2. WSEG n1 n2(WCAT(w1,w2)) = w1
\ENDTHEOREM
\THEOREM WSEG\_WCAT2 word\_base
|- !n1 n2.
    !w1 :: PWORDLEN n1. !w2 :: PWORDLEN n2. WSEG n2 0(WCAT(w1,w2)) = w2
\ENDTHEOREM
\THEOREM WSEG\_WCAT\_WSEG1 word\_base
|- !n1 n2.
    !w1 :: PWORDLEN n1.
     !w2 :: PWORDLEN n2.
      !m k.
       m <= n1 /\ n2 <= k ==> (WSEG m k(WCAT(w1,w2)) = WSEG m(k - n2)w1)
\ENDTHEOREM
\THEOREM WSEG\_WCAT\_WSEG2 word\_base
|- !n1 n2.
    !w1 :: PWORDLEN n1.
     !w2 :: PWORDLEN n2.
      !m k. (m + k) <= n2 ==> (WSEG m k(WCAT(w1,w2)) = WSEG m k w2)
\ENDTHEOREM
\THEOREM WSEG\_WCAT\_WSEG word\_base
|- !n1 n2.
    !w1 :: PWORDLEN n1.
     !w2 :: PWORDLEN n2.
      !m k.
       (m + k) <= (n1 + n2) /\ k < n2 /\ n2 <= (m + k) ==>
       (WSEG m k(WCAT(w1,w2)) =
        WCAT(WSEG((m + k) - n2)0 w1,WSEG(n2 - k)k w2))
\ENDTHEOREM
\THEOREM WSEG\_WORDLEN word\_base
|- !n.
    !w :: PWORDLEN n. !m k. (m + k) <= n ==> (WORDLEN(WSEG m k w) = m)
\ENDTHEOREM
\THEOREM WSEG\_WORD\_LENGTH word\_base
|- !n. !w :: PWORDLEN n. WSEG n 0 w = w
\ENDTHEOREM
\THEOREM WSEG\_WSEG word\_base
|- !n.
    !w :: PWORDLEN n.
     !m1 k1 m2 k2.
      (m1 + k1) <= n /\ (m2 + k2) <= m1 ==>
      (WSEG m2 k2(WSEG m1 k1 w) = WSEG m2(k1 + k2)w)
\ENDTHEOREM
\THEOREM WSPLIT\_DEF word\_base
|- !m l. WSPLIT m(WORD l) = WORD(BUTLASTN m l),WORD(LASTN m l)
\ENDTHEOREM
\THEOREM WSPLIT\_PWORDLEN word\_base
|- !n.
    !w :: PWORDLEN n.
     !m.
      m <= n ==>
      PWORDLEN(n - m)(FST(WSPLIT m w)) /\ PWORDLEN m(SND(WSPLIT m w))
\ENDTHEOREM
\THEOREM WSPLIT\_WSEG1 word\_base
|- !n.
    !w :: PWORDLEN n. !k. k <= n ==> (FST(WSPLIT k w) = WSEG(n - k)k w)
\ENDTHEOREM
\THEOREM WSPLIT\_WSEG2 word\_base
|- !n. !w :: PWORDLEN n. !k. k <= n ==> (SND(WSPLIT k w) = WSEG k 0 w)
\ENDTHEOREM
\THEOREM WSPLIT\_WSEG word\_base
|- !n.
    !w :: PWORDLEN n.
     !k. k <= n ==> (WSPLIT k w = WSEG(n - k)k w,WSEG k 0 w)
\ENDTHEOREM
\section{The theory {\tt word\_bitop}}\THEOREM EXISTSABIT\_DEF word\_bitop
|- !P l. EXISTSABIT P(WORD l) = SOME_EL P l
\ENDTHEOREM
\THEOREM EXISTSABIT word\_bitop
|- !n. !w :: PWORDLEN n. !P. EXISTSABIT P w = (?k. k < n /\ P(BIT k w))
\ENDTHEOREM
\THEOREM EXISTSABIT\_WCAT word\_bitop
|- !w1 w2 P.
    EXISTSABIT P(WCAT(w1,w2)) = EXISTSABIT P w1 \/ EXISTSABIT P w2
\ENDTHEOREM
\THEOREM EXISTSABIT\_WSEG word\_bitop
|- !n.
    !w :: PWORDLEN n.
     !m k.
      (m + k) <= n ==> (!P. EXISTSABIT P(WSEG m k w) ==> EXISTSABIT P w)
\ENDTHEOREM
\THEOREM FORALLBITS\_DEF word\_bitop
|- !P l. FORALLBITS P(WORD l) = ALL_EL P l
\ENDTHEOREM
\THEOREM FORALLBITS word\_bitop
|- !n. !w :: PWORDLEN n. !P. FORALLBITS P w = (!k. k < n ==> P(BIT k w))
\ENDTHEOREM
\THEOREM FORALLBITS\_WCAT word\_bitop
|- !w1 w2 P.
    FORALLBITS P(WCAT(w1,w2)) = FORALLBITS P w1 /\ FORALLBITS P w2
\ENDTHEOREM
\THEOREM FORALLBITS\_WSEG word\_bitop
|- !n.
    !w :: PWORDLEN n.
     !P.
      FORALLBITS P w ==>
      (!m k. (m + k) <= n ==> FORALLBITS P(WSEG m k w))
\ENDTHEOREM
\THEOREM NOT\_EXISTSABIT word\_bitop
|- !P w. ~EXISTSABIT P w = FORALLBITS($~ o P)w
\ENDTHEOREM
\THEOREM NOT\_FORALLBITS word\_bitop
|- !P w. ~FORALLBITS P w = EXISTSABIT($~ o P)w
\ENDTHEOREM
\THEOREM PBITBOP\_DEF word\_bitop
|- !op.
    PBITBOP op =
    (!n.
      !w1 :: PWORDLEN n.
       !w2 :: PWORDLEN n.
        PWORDLEN n(op w1 w2) /\
        (!m k.
          (m + k) <= n ==>
          (op(WSEG m k w1)(WSEG m k w2) = WSEG m k(op w1 w2))))
\ENDTHEOREM
\THEOREM PBITBOP\_EXISTS word\_bitop
|- !f. ?fn. !l1 l2. fn(WORD l1)(WORD l2) = WORD(MAP2 f l1 l2)
\ENDTHEOREM
\THEOREM PBITBOP\_PWORDLEN word\_bitop
|- !op :: PBITBOP.
    !n. !w1 :: PWORDLEN n. !w2 :: PWORDLEN n. PWORDLEN n(op w1 w2)
\ENDTHEOREM
\THEOREM PBITBOP\_WSEG word\_bitop
|- !op :: PBITBOP.
    !n.
     !w1 :: PWORDLEN n.
      !w2 :: PWORDLEN n.
       !m k.
        (m + k) <= n ==>
        (op(WSEG m k w1)(WSEG m k w2) = WSEG m k(op w1 w2))
\ENDTHEOREM
\THEOREM PBITOP\_BIT word\_bitop
|- !op :: PBITOP.
    !n.
     !w :: PWORDLEN n.
      !k. k < n ==> (op(WORD[BIT k w]) = WORD[BIT k(op w)])
\ENDTHEOREM
\THEOREM PBITOP\_DEF word\_bitop
|- !op.
    PBITOP op =
    (!n.
      !w :: PWORDLEN n.
       PWORDLEN n(op w) /\
       (!m k. (m + k) <= n ==> (op(WSEG m k w) = WSEG m k(op w))))
\ENDTHEOREM
\THEOREM PBITOP\_PWORDLEN word\_bitop
|- !op :: PBITOP. !n. !w :: PWORDLEN n. PWORDLEN n(op w)
\ENDTHEOREM
\THEOREM PBITOP\_WSEG word\_bitop
|- !op :: PBITOP.
    !n.
     !w :: PWORDLEN n.
      !m k. (m + k) <= n ==> (op(WSEG m k w) = WSEG m k(op w))
\ENDTHEOREM
\THEOREM SHL\_DEF word\_bitop
|- !f w b.
    SHL f w b =
    BIT(PRE(WORDLEN w))w,
    WCAT(WSEG(PRE(WORDLEN w))0 w,(f => WSEG 1 0 w | WORD[b]))
\ENDTHEOREM
\THEOREM SHL\_WSEG\_1F word\_bitop
|- !n.
    !w :: PWORDLEN n.
     !m k.
      (m + k) <= n ==>
      0 < m ==>
      (!b.
        SHL F(WSEG m k w)b =
        BIT(k + (m - 1))w,WCAT(WSEG(m - 1)k w,WORD[b]))
\ENDTHEOREM
\THEOREM SHL\_WSEG word\_bitop
|- !n.
    !w :: PWORDLEN n.
     !m k.
      (m + k) <= n ==>
      0 < m ==>
      (!f b.
        SHL f(WSEG m k w)b =
        BIT(k + (m - 1))w,
        (f => 
         WCAT(WSEG(m - 1)k w,WSEG 1 k w) | 
         WCAT(WSEG(m - 1)k w,WORD[b])))
\ENDTHEOREM
\THEOREM SHL\_WSEG\_NF word\_bitop
|- !n.
    !w :: PWORDLEN n.
     !m k.
      (m + k) <= n ==>
      0 < m ==>
      0 < k ==>
      (SHL F(WSEG m k w)(BIT(k - 1)w) =
       BIT(k + (m - 1))w,WSEG m(k - 1)w)
\ENDTHEOREM
\THEOREM SHR\_DEF word\_bitop
|- !f b w.
    SHR f b w =
    WCAT
    ((f => WSEG 1(PRE(WORDLEN w))w | WORD[b]),WSEG(PRE(WORDLEN w))1 w),
    BIT 0 w
\ENDTHEOREM
\THEOREM SHR\_WSEG\_1F word\_bitop
|- !n.
    !w :: PWORDLEN n.
     !m k.
      (m + k) <= n ==>
      0 < m ==>
      (!b.
        SHR F b(WSEG m k w) = WCAT(WORD[b],WSEG(m - 1)(k + 1)w),BIT k w)
\ENDTHEOREM
\THEOREM SHR\_WSEG word\_bitop
|- !n.
    !w :: PWORDLEN n.
     !m k.
      (m + k) <= n ==>
      0 < m ==>
      (!f b.
        SHR f b(WSEG m k w) =
        (f => 
         WCAT(WSEG 1(k + (m - 1))w,WSEG(m - 1)(k + 1)w) | 
         WCAT(WORD[b],WSEG(m - 1)(k + 1)w)),BIT k w)
\ENDTHEOREM
\THEOREM SHR\_WSEG\_NF word\_bitop
|- !n.
    !w :: PWORDLEN n.
     !m k.
      (m + k) < n ==>
      0 < m ==>
      (SHR F(BIT(m + k)w)(WSEG m k w) = WSEG m(k + 1)w,BIT k w)
\ENDTHEOREM
\THEOREM WMAP\_0 word\_bitop
|- !f. WMAP f(WORD[]) = WORD[]
\ENDTHEOREM
\THEOREM WMAP\_BIT word\_bitop
|- !n.
    !w :: PWORDLEN n. !k. k < n ==> (!f. BIT k(WMAP f w) = f(BIT k w))
\ENDTHEOREM
\THEOREM WMAP\_DEF word\_bitop
|- !f l. WMAP f(WORD l) = WORD(MAP f l)
\ENDTHEOREM
\THEOREM WMAP\_o word\_bitop
|- !w f g. WMAP g(WMAP f w) = WMAP(g o f)w
\ENDTHEOREM
\THEOREM WMAP\_PBITOP word\_bitop
|- !f. PBITOP(WMAP f)
\ENDTHEOREM
\THEOREM WMAP\_PWORDLEN word\_bitop
|- !w :: PWORDLEN n. !f. PWORDLEN n(WMAP f w)
\ENDTHEOREM
\THEOREM WMAP\_WCAT word\_bitop
|- !w1 w2 f. WMAP f(WCAT(w1,w2)) = WCAT(WMAP f w1,WMAP f w2)
\ENDTHEOREM
\THEOREM WMAP\_WSEG word\_bitop
|- !n.
    !w :: PWORDLEN n.
     !m k.
      (m + k) <= n ==> (!f. WMAP f(WSEG m k w) = WSEG m k(WMAP f w))
\ENDTHEOREM
\THEOREM WSEG\_SHL\_0 word\_bitop
|- !n.
    !w :: PWORDLEN(SUC n).
     !m b.
      0 < m /\ m <= (SUC n) ==>
      (WSEG m 0(SND(SHL f w b)) =
       WCAT(WSEG(m - 1)0 w,(f => WSEG 1 0 w | WORD[b])))
\ENDTHEOREM
\THEOREM WSEG\_SHL word\_bitop
|- !n.
    !w :: PWORDLEN(SUC n).
     !m k.
      0 < k /\ (m + k) <= (SUC n) ==>
      (!b. WSEG m k(SND(SHL f w b)) = WSEG m(k - 1)w)
\ENDTHEOREM
\section{The theory {\tt word\_num}}\THEOREM LVAL\_DEF word\_num
|- !f b l. LVAL f b l = FOLDL(\e x. (b * e) + (f x))0 l
\ENDTHEOREM
\THEOREM LVAL word\_num
|- (!f b. LVAL f b[] = 0) /\
   (!l f b x.
     LVAL f b(CONS x l) = ((f x) * (b EXP (LENGTH l))) + (LVAL f b l))
\ENDTHEOREM
\THEOREM LVAL\_MAX word\_num
|- !l f b. (!x. (f x) < b) ==> (LVAL f b l) < (b EXP (LENGTH l))
\ENDTHEOREM
\THEOREM LVAL\_SNOC word\_num
|- !l h f b. LVAL f b(SNOC h l) = ((LVAL f b l) * b) + (f h)
\ENDTHEOREM
\THEOREM NLIST\_DEF word\_num
|- (!frep b m. NLIST 0 frep b m = []) /\
   (!n frep b m.
     NLIST(SUC n)frep b m = SNOC(frep(m MOD b))(NLIST n frep b(m DIV b)))
\ENDTHEOREM
\THEOREM NVAL0 word\_num
|- !f b. NVAL f b(WORD[]) = 0
\ENDTHEOREM
\THEOREM NVAL1 word\_num
|- !f b x. NVAL f b(WORD[x]) = f x
\ENDTHEOREM
\THEOREM NVAL\_DEF word\_num
|- !f b l. NVAL f b(WORD l) = LVAL f b l
\ENDTHEOREM
\THEOREM NVAL\_MAX word\_num
|- !f b.
    (!x. (f x) < b) ==> (!n. !w :: PWORDLEN n. (NVAL f b w) < (b EXP n))
\ENDTHEOREM
\THEOREM NVAL\_WCAT1 word\_num
|- !w f b x. NVAL f b(WCAT(w,WORD[x])) = ((NVAL f b w) * b) + (f x)
\ENDTHEOREM
\THEOREM NVAL\_WCAT2 word\_num
|- !n.
    !w :: PWORDLEN n.
     !f b x.
      NVAL f b(WCAT(WORD[x],w)) = ((f x) * (b EXP n)) + (NVAL f b w)
\ENDTHEOREM
\THEOREM NVAL\_WCAT word\_num
|- !n m.
    !w1 :: PWORDLEN n.
     !w2 :: PWORDLEN m.
      !f b.
       NVAL f b(WCAT(w1,w2)) =
       ((NVAL f b w1) * (b EXP m)) + (NVAL f b w2)
\ENDTHEOREM
\THEOREM NVAL\_WORDLEN\_0 word\_num
|- !w :: PWORDLEN 0. !fv r. NVAL fv r w = 0
\ENDTHEOREM
\THEOREM NWORD\_DEF word\_num
|- !n frep b m. NWORD n frep b m = WORD(NLIST n frep b m)
\ENDTHEOREM
\THEOREM NWORD\_LENGTH word\_num
|- !n f b m. WORDLEN(NWORD n f b m) = n
\ENDTHEOREM
\THEOREM NWORD\_PWORDLEN word\_num
|- !n f b m. PWORDLEN n(NWORD n f b m)
\ENDTHEOREM
\section{The theory {\tt bword\_bitop}}\THEOREM PBITBOP\_WAND bword\_bitop
|- PBITBOP $WAND
\ENDTHEOREM
\THEOREM PBITBOP\_WOR bword\_bitop
|- PBITBOP $WOR
\ENDTHEOREM
\THEOREM PBITBOP\_WXOR bword\_bitop
|- PBITBOP $WXOR
\ENDTHEOREM
\THEOREM PBITOP\_WNOT bword\_bitop
|- PBITOP WNOT
\ENDTHEOREM
\THEOREM WAND\_DEF bword\_bitop
|- !l1 l2. (WORD l1) WAND (WORD l2) = WORD(MAP2 $/\ l1 l2)
\ENDTHEOREM
\THEOREM WCAT\_WNOT bword\_bitop
|- !n1 n2.
    !w1 :: PWORDLEN n1.
     !w2 :: PWORDLEN n2. WCAT(WNOT w1,WNOT w2) = WNOT(WCAT(w1,w2))
\ENDTHEOREM
\THEOREM WNOT\_DEF bword\_bitop
|- !l. WNOT(WORD l) = WORD(MAP $~ l)
\ENDTHEOREM
\THEOREM WNOT\_WNOT bword\_bitop
|- !w. WNOT(WNOT w) = w
\ENDTHEOREM
\THEOREM WOR\_DEF bword\_bitop
|- !l1 l2. (WORD l1) WOR (WORD l2) = WORD(MAP2 $\/ l1 l2)
\ENDTHEOREM
\THEOREM WXOR\_DEF bword\_bitop
|- !l1 l2. (WORD l1) WXOR (WORD l2) = WORD(MAP2(\x y. ~(x = y))l1 l2)
\ENDTHEOREM
\section{The theory {\tt bword\_num}}\THEOREM ADD\_BNVAL\_LEFT bword\_num
|- !n.
    !w1 w2 :: PWORDLEN(SUC n).
     (BNVAL w1) + (BNVAL w2) =
     (((BV(BIT n w1)) + (BV(BIT n w2))) * (2 EXP n)) +
     ((BNVAL(WSEG n 0 w1)) + (BNVAL(WSEG n 0 w2)))
\ENDTHEOREM
\THEOREM ADD\_BNVAL\_RIGHT bword\_num
|- !n.
    !w1 w2 :: PWORDLEN(SUC n).
     (BNVAL w1) + (BNVAL w2) =
     (((BNVAL(WSEG n 1 w1)) + (BNVAL(WSEG n 1 w2))) * 2) +
     ((BV(BIT 0 w1)) + (BV(BIT 0 w2)))
\ENDTHEOREM
\THEOREM ADD\_BNVAL\_SPLIT bword\_num
|- !n1 n2.
    !w1 w2 :: PWORDLEN(n1 + n2).
     (BNVAL w1) + (BNVAL w2) =
     (((BNVAL(WSEG n1 n2 w1)) + (BNVAL(WSEG n1 n2 w2))) * (2 EXP n2)) +
     ((BNVAL(WSEG n2 0 w1)) + (BNVAL(WSEG n2 0 w2)))
\ENDTHEOREM
\THEOREM BIT\_NBWORD0 bword\_num
|- !k n. k < n ==> (BIT k(NBWORD n 0) = F)
\ENDTHEOREM
\THEOREM BNVAL0 bword\_num
|- BNVAL(WORD[]) = 0
\ENDTHEOREM
\THEOREM BNVAL\_11 bword\_num
|- !w1 w2.
    (WORDLEN w1 = WORDLEN w2) ==> (BNVAL w1 = BNVAL w2) ==> (w1 = w2)
\ENDTHEOREM
\THEOREM BNVAL\_DEF bword\_num
|- !l. BNVAL(WORD l) = LVAL BV 2 l
\ENDTHEOREM
\THEOREM BNVAL\_MAX bword\_num
|- !n. !w :: PWORDLEN n. (BNVAL w) < (2 EXP n)
\ENDTHEOREM
\THEOREM BNVAL\_NBWORD bword\_num
|- !n m. m < (2 EXP n) ==> (BNVAL(NBWORD n m) = m)
\ENDTHEOREM
\THEOREM BNVAL\_NVAL bword\_num
|- !w. BNVAL w = NVAL BV 2 w
\ENDTHEOREM
\THEOREM BNVAL\_ONTO bword\_num
|- !w. ?n. BNVAL w = n
\ENDTHEOREM
\THEOREM BNVAL\_WCAT1 bword\_num
|- !n.
    !w :: PWORDLEN n.
     !x. BNVAL(WCAT(w,WORD[x])) = ((BNVAL w) * 2) + (BV x)
\ENDTHEOREM
\THEOREM BNVAL\_WCAT2 bword\_num
|- !n.
    !w :: PWORDLEN n.
     !x. BNVAL(WCAT(WORD[x],w)) = ((BV x) * (2 EXP n)) + (BNVAL w)
\ENDTHEOREM
\THEOREM BNVAL\_WCAT bword\_num
|- !n m.
    !w1 :: PWORDLEN n.
     !w2 :: PWORDLEN m.
      BNVAL(WCAT(w1,w2)) = ((BNVAL w1) * (2 EXP m)) + (BNVAL w2)
\ENDTHEOREM
\THEOREM BV\_DEF bword\_num
|- !b. BV b = (b => SUC 0 | 0)
\ENDTHEOREM
\THEOREM BV\_LESS\_2 bword\_num
|- !x. (BV x) < 2
\ENDTHEOREM
\THEOREM BV\_VB bword\_num
|- !x. x < 2 ==> (BV(VB x) = x)
\ENDTHEOREM
\THEOREM DOUBL\_EQ\_SHL bword\_num
|- !n.
    0 < n ==>
    (!w :: PWORDLEN n.
      !b. NBWORD n((BNVAL w) + ((BNVAL w) + (BV b))) = SND(SHL F w b))
\ENDTHEOREM
\THEOREM EQ\_NBWORD0\_SPLIT bword\_num
|- !n.
    !w :: PWORDLEN n.
     !m.
      m <= n ==>
      ((w = NBWORD n 0) =
       (WSEG(n - m)m w = NBWORD(n - m)0) /\ (WSEG m 0 w = NBWORD m 0))
\ENDTHEOREM
\THEOREM MSB\_NBWORD bword\_num
|- !n m. BIT n(NBWORD(SUC n)m) = VB((m DIV (2 EXP n)) MOD 2)
\ENDTHEOREM
\THEOREM NBWORD0 bword\_num
|- !m. NBWORD 0 m = WORD[]
\ENDTHEOREM
\THEOREM NBWORD\_BNVAL bword\_num
|- !n. !w :: PWORDLEN n. NBWORD n(BNVAL w) = w
\ENDTHEOREM
\THEOREM NBWORD\_DEF bword\_num
|- !n m. NBWORD n m = WORD(NLIST n VB 2 m)
\ENDTHEOREM
\THEOREM NBWORD\_MOD bword\_num
|- !n m. NBWORD n(m MOD (2 EXP n)) = NBWORD n m
\ENDTHEOREM
\THEOREM NBWORD\_SPLIT bword\_num
|- !n1 n2 m.
    NBWORD(n1 + n2)m = WCAT(NBWORD n1(m DIV (2 EXP n2)),NBWORD n2 m)
\ENDTHEOREM
\THEOREM NBWORD\_SUC bword\_num
|- !n m. NBWORD(SUC n)m = WCAT(NBWORD n(m DIV 2),WORD[VB(m MOD 2)])
\ENDTHEOREM
\THEOREM NBWORD\_SUC\_FST bword\_num
|- !n m.
    NBWORD(SUC n)m = WCAT(WORD[VB((m DIV (2 EXP n)) MOD 2)],NBWORD n m)
\ENDTHEOREM
\THEOREM NBWORD\_SUC\_WSEG bword\_num
|- !n. !w :: PWORDLEN(SUC n). NBWORD n(BNVAL w) = WSEG n 0 w
\ENDTHEOREM
\THEOREM PWORDLEN\_NBWORD bword\_num
|- !n m. PWORDLEN n(NBWORD n m)
\ENDTHEOREM
\THEOREM VB\_BV bword\_num
|- !x. VB(BV x) = x
\ENDTHEOREM
\THEOREM VB\_DEF bword\_num
|- !n. VB n = ~(n MOD 2 = 0)
\ENDTHEOREM
\THEOREM WCAT\_NBWORD\_0 bword\_num
|- !n1 n2. WCAT(NBWORD n1 0,NBWORD n2 0) = NBWORD(n1 + n2)0
\ENDTHEOREM
\THEOREM WORDLEN\_NBWORD bword\_num
|- !n m. WORDLEN(NBWORD n m) = n
\ENDTHEOREM
\THEOREM WSEG\_NBWORD bword\_num
|- !m k n.
    (m + k) <= n ==>
    (!l. WSEG m k(NBWORD n l) = NBWORD m(l DIV (2 EXP k)))
\ENDTHEOREM
\THEOREM WSEG\_NBWORD\_SUC bword\_num
|- !n m. WSEG n 0(NBWORD(SUC n)m) = NBWORD n m
\ENDTHEOREM
\THEOREM WSPLIT\_NBWORD\_0 bword\_num
|- !m n. m <= n ==> (WSPLIT m(NBWORD n 0) = NBWORD(n - m)0,NBWORD m 0)
\ENDTHEOREM
\THEOREM ZERO\_WORD\_VAL bword\_num
|- !n. !w :: PWORDLEN n. (w = NBWORD n 0) = (BNVAL w = 0)
\ENDTHEOREM
\section{The theory {\tt bword\_arith}}\THEOREM ACARRY\_ACARRY\_WSEG bword\_arith
|- !n.
    !w1 w2 :: PWORDLEN n.
     !cin m k1 k2.
      k1 < m /\ k2 < n /\ (m + k2) <= n ==>
      (ACARRY k1(WSEG m k2 w1)(WSEG m k2 w2)(ACARRY k2 w1 w2 cin) =
       ACARRY(k1 + k2)w1 w2 cin)
\ENDTHEOREM
\THEOREM ACARRY\_DEF bword\_arith
|- (!w1 w2 cin. ACARRY 0 w1 w2 cin = cin) /\
   (!n w1 w2 cin.
     ACARRY(SUC n)w1 w2 cin =
     VB
     (((BV(BIT n w1)) + ((BV(BIT n w2)) + (BV(ACARRY n w1 w2 cin)))) DIV
      2))
\ENDTHEOREM
\THEOREM ACARRY\_EQ\_ADD\_DIV bword\_arith
|- !n.
    !w1 w2 :: PWORDLEN n.
     !k.
      k < n ==>
      (BV(ACARRY k w1 w2 cin) =
       ((BNVAL(WSEG k 0 w1)) + ((BNVAL(WSEG k 0 w2)) + (BV cin))) DIV
       (2 EXP k))
\ENDTHEOREM
\THEOREM ACARRY\_EQ\_ICARRY bword\_arith
|- !n.
    !w1 w2 :: PWORDLEN n.
     !cin k. k <= n ==> (ACARRY k w1 w2 cin = ICARRY k w1 w2 cin)
\ENDTHEOREM
\THEOREM ACARRY\_MSB bword\_arith
|- !n.
    !w1 w2 :: PWORDLEN n.
     !cin.
      ACARRY n w1 w2 cin =
      BIT n(NBWORD(SUC n)((BNVAL w1) + ((BNVAL w2) + (BV cin))))
\ENDTHEOREM
\THEOREM ACARRY\_WSEG bword\_arith
|- !n.
    !w1 w2 :: PWORDLEN n.
     !cin k m.
      k < m /\ m <= n ==>
      (ACARRY k(WSEG m 0 w1)(WSEG m 0 w2)cin = ACARRY k w1 w2 cin)
\ENDTHEOREM
\THEOREM ADD\_NBWORD\_EQ0\_SPLIT bword\_arith
|- !n1 n2.
    !w1 w2 :: PWORDLEN(n1 + n2).
     !cin.
      (NBWORD(n1 + n2)((BNVAL w1) + ((BNVAL w2) + (BV cin))) =
       NBWORD(n1 + n2)0) =
      (NBWORD 
       n1
       ((BNVAL(WSEG n1 n2 w1)) +
        ((BNVAL(WSEG n1 n2 w2)) + (BV(ACARRY n2 w1 w2 cin)))) =
       NBWORD n1 0) /\
      (NBWORD 
       n2
       ((BNVAL(WSEG n2 0 w1)) + ((BNVAL(WSEG n2 0 w2)) + (BV cin))) =
       NBWORD n2 0)
\ENDTHEOREM
\THEOREM ADD\_WORD\_SPLIT bword\_arith
|- !n1 n2.
    !w1 w2 :: PWORDLEN(n1 + n2).
     !cin.
      NBWORD(n1 + n2)((BNVAL w1) + ((BNVAL w2) + (BV cin))) =
      WCAT
      (NBWORD 
       n1
       ((BNVAL(WSEG n1 n2 w1)) +
        ((BNVAL(WSEG n1 n2 w2)) + (BV(ACARRY n2 w1 w2 cin)))),
       NBWORD 
       n2
       ((BNVAL(WSEG n2 0 w1)) + ((BNVAL(WSEG n2 0 w2)) + (BV cin))))
\ENDTHEOREM
\THEOREM ICARRY\_DEF bword\_arith
|- (!w1 w2 cin. ICARRY 0 w1 w2 cin = cin) /\
   (!n w1 w2 cin.
     ICARRY(SUC n)w1 w2 cin =
     BIT n w1 /\ BIT n w2 \/
     (BIT n w1 \/ BIT n w2) /\ ICARRY n w1 w2 cin)
\ENDTHEOREM
\THEOREM ICARRY\_WSEG bword\_arith
|- !n.
    !w1 w2 :: PWORDLEN n.
     !cin k m.
      k < m /\ m <= n ==>
      (ICARRY k(WSEG m 0 w1)(WSEG m 0 w2)cin = ICARRY k w1 w2 cin)
\ENDTHEOREM
\THEOREM WSEG\_NBWORD\_ADD bword\_arith
|- !n.
    !w1 w2 :: PWORDLEN n.
     !m k cin.
      (m + k) <= n ==>
      (WSEG m k(NBWORD n((BNVAL w1) + ((BNVAL w2) + (BV cin)))) =
       NBWORD 
       m
       ((BNVAL(WSEG m k w1)) +
        ((BNVAL(WSEG m k w2)) + (BV(ACARRY k w1 w2 cin)))))
\ENDTHEOREM