forked from jrh13/hol-light
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathint.ml
1507 lines (1336 loc) · 64.2 KB
/
int.ml
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
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
(* ========================================================================= *)
(* Theory of integers. *)
(* *)
(* The integers are carved out of the real numbers; hence all the *)
(* universal theorems can be derived trivially from the real analog. *)
(* *)
(* John Harrison, University of Cambridge Computer Laboratory *)
(* *)
(* (c) Copyright, University of Cambridge 1998 *)
(* (c) Copyright, John Harrison 1998-2007 *)
(* ========================================================================= *)
needs "calc_rat.ml";;
(* ------------------------------------------------------------------------- *)
(* Representing predicate. The "is_int" variant is useful for backwards *)
(* compatibility with former definition of "is_int" constant, now removed. *)
(* ------------------------------------------------------------------------- *)
let integer = new_definition
`integer(x) <=> ?n. abs(x) = &n`;;
let is_int = prove
(`integer(x) <=> ?n. x = &n \/ x = -- &n`,
REWRITE_TAC[integer] THEN AP_TERM_TAC THEN ABS_TAC THEN REAL_ARITH_TAC);;
(* ------------------------------------------------------------------------- *)
(* Type of integers. *)
(* ------------------------------------------------------------------------- *)
let int_tybij = new_type_definition "int" ("int_of_real","real_of_int")
(prove(`?x. integer x`,
EXISTS_TAC `&0` THEN
REWRITE_TAC[is_int; REAL_OF_NUM_EQ; EXISTS_OR_THM; GSYM EXISTS_REFL]));;
let int_abstr,int_rep =
SPEC_ALL(CONJUNCT1 int_tybij),SPEC_ALL(CONJUNCT2 int_tybij);;
let dest_int_rep = prove
(`!i. ?n. (real_of_int i = &n) \/ (real_of_int i = --(&n))`,
REWRITE_TAC[GSYM is_int; int_rep; int_abstr]);;
let INTEGER_REAL_OF_INT = prove
(`!x. integer(real_of_int x)`,
MESON_TAC[int_tybij]);;
(* ------------------------------------------------------------------------- *)
(* We want the following too. *)
(* ------------------------------------------------------------------------- *)
let int_eq = prove
(`!x y. (x = y) <=> (real_of_int x = real_of_int y)`,
REPEAT GEN_TAC THEN EQ_TAC THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN
POP_ASSUM(MP_TAC o AP_TERM `int_of_real`) THEN
REWRITE_TAC[int_abstr]);;
(* ------------------------------------------------------------------------- *)
(* Set up interface map. *)
(* ------------------------------------------------------------------------- *)
do_list overload_interface
["+",`int_add:int->int->int`; "-",`int_sub:int->int->int`;
"*",`int_mul:int->int->int`; "<",`int_lt:int->int->bool`;
"<=",`int_le:int->int->bool`; ">",`int_gt:int->int->bool`;
">=",`int_ge:int->int->bool`; "--",`int_neg:int->int`;
"pow",`int_pow:int->num->int`; "abs",`int_abs:int->int`;
"max",`int_max:int->int->int`; "min",`int_min:int->int->int`;
"&",`int_of_num:num->int`];;
let prioritize_int() = prioritize_overload(mk_type("int",[]));;
(* ------------------------------------------------------------------------- *)
(* Definitions and closure derivations of all operations but "inv" and "/". *)
(* ------------------------------------------------------------------------- *)
let int_le = new_definition
`x <= y <=> (real_of_int x) <= (real_of_int y)`;;
let int_lt = new_definition
`x < y <=> (real_of_int x) < (real_of_int y)`;;
let int_ge = new_definition
`x >= y <=> (real_of_int x) >= (real_of_int y)`;;
let int_gt = new_definition
`x > y <=> (real_of_int x) > (real_of_int y)`;;
let int_of_num = new_definition
`&n = int_of_real(real_of_num n)`;;
let int_of_num_th = prove
(`!n. real_of_int(int_of_num n) = real_of_num n`,
REWRITE_TAC[int_of_num; GSYM int_rep; is_int] THEN
REWRITE_TAC[REAL_OF_NUM_EQ; EXISTS_OR_THM; GSYM EXISTS_REFL]);;
let int_neg = new_definition
`--i = int_of_real(--(real_of_int i))`;;
let int_neg_th = prove
(`!x. real_of_int(int_neg x) = --(real_of_int x)`,
REWRITE_TAC[int_neg; GSYM int_rep; is_int] THEN
GEN_TAC THEN STRIP_ASSUME_TAC(SPEC `x:int` dest_int_rep) THEN
ASM_REWRITE_TAC[REAL_NEG_NEG; EXISTS_OR_THM; REAL_EQ_NEG2;
REAL_OF_NUM_EQ; GSYM EXISTS_REFL]);;
let int_add = new_definition
`x + y = int_of_real((real_of_int x) + (real_of_int y))`;;
let int_add_th = prove
(`!x y. real_of_int(x + y) = (real_of_int x) + (real_of_int y)`,
REWRITE_TAC[int_add; GSYM int_rep; is_int] THEN REPEAT GEN_TAC THEN
X_CHOOSE_THEN `m:num` DISJ_CASES_TAC (SPEC `x:int` dest_int_rep) THEN
X_CHOOSE_THEN `n:num` DISJ_CASES_TAC (SPEC `y:int` dest_int_rep) THEN
ASM_REWRITE_TAC[REAL_OF_NUM_ADD; REAL_OF_NUM_EQ; EXISTS_OR_THM] THEN
REWRITE_TAC[GSYM EXISTS_REFL] THEN
DISJ_CASES_THEN MP_TAC (SPECL [`m:num`; `n:num`] LE_CASES) THEN
REWRITE_TAC[LE_EXISTS] THEN DISCH_THEN(X_CHOOSE_THEN `d:num` SUBST1_TAC) THEN
REWRITE_TAC[GSYM REAL_OF_NUM_ADD; OR_EXISTS_THM; REAL_NEG_ADD] THEN
TRY(EXISTS_TAC `d:num` THEN REAL_ARITH_TAC) THEN
REWRITE_TAC[EXISTS_OR_THM; GSYM REAL_NEG_ADD; REAL_EQ_NEG2;
REAL_OF_NUM_ADD; REAL_OF_NUM_EQ; GSYM EXISTS_REFL]);;
let int_sub = new_definition
`x - y = int_of_real(real_of_int x - real_of_int y)`;;
let int_sub_th = prove
(`!x y. real_of_int(x - y) = (real_of_int x) - (real_of_int y)`,
REWRITE_TAC[int_sub; real_sub; GSYM int_neg_th; GSYM int_add_th] THEN
REWRITE_TAC[int_abstr]);;
let int_mul = new_definition
`x * y = int_of_real ((real_of_int x) * (real_of_int y))`;;
let int_mul_th = prove
(`!x y. real_of_int(x * y) = (real_of_int x) * (real_of_int y)`,
REPEAT GEN_TAC THEN REWRITE_TAC[int_mul; GSYM int_rep; is_int] THEN
X_CHOOSE_THEN `m:num` DISJ_CASES_TAC (SPEC `x:int` dest_int_rep) THEN
X_CHOOSE_THEN `n:num` DISJ_CASES_TAC (SPEC `y:int` dest_int_rep) THEN
ASM_REWRITE_TAC[REAL_OF_NUM_ADD; REAL_OF_NUM_EQ; EXISTS_OR_THM] THEN
REWRITE_TAC[REAL_MUL_LNEG; REAL_MUL_RNEG; REAL_NEG_NEG; REAL_OF_NUM_MUL] THEN
REWRITE_TAC[REAL_EQ_NEG2; REAL_OF_NUM_EQ; GSYM EXISTS_REFL]);;
let int_abs = new_definition
`abs x = int_of_real(abs(real_of_int x))`;;
let int_abs_th = prove
(`!x. real_of_int(abs x) = abs(real_of_int x)`,
GEN_TAC THEN REWRITE_TAC[int_abs; real_abs] THEN COND_CASES_TAC THEN
REWRITE_TAC[GSYM int_neg; int_neg_th; int_abstr]);;
let int_sgn = new_definition
`int_sgn x = int_of_real(real_sgn(real_of_int x))`;;
let int_sgn_th = prove
(`!x. real_of_int(int_sgn x) = real_sgn(real_of_int x)`,
GEN_TAC THEN REWRITE_TAC[int_sgn; real_sgn; GSYM int_rep] THEN
REPEAT(COND_CASES_TAC THEN ASM_REWRITE_TAC[]) THEN
MESON_TAC[is_int]);;
let int_max = new_definition
`int_max x y = int_of_real(max (real_of_int x) (real_of_int y))`;;
let int_max_th = prove
(`!x y. real_of_int(max x y) = max (real_of_int x) (real_of_int y)`,
REPEAT GEN_TAC THEN REWRITE_TAC[int_max; real_max] THEN
COND_CASES_TAC THEN REWRITE_TAC[int_abstr]);;
let int_min = new_definition
`int_min x y = int_of_real(min (real_of_int x) (real_of_int y))`;;
let int_min_th = prove
(`!x y. real_of_int(min x y) = min (real_of_int x) (real_of_int y)`,
REPEAT GEN_TAC THEN REWRITE_TAC[int_min; real_min] THEN
COND_CASES_TAC THEN REWRITE_TAC[int_abstr]);;
let int_pow = new_definition
`x pow n = int_of_real((real_of_int x) pow n)`;;
let int_pow_th = prove
(`!x n. real_of_int(x pow n) = (real_of_int x) pow n`,
GEN_TAC THEN REWRITE_TAC[int_pow] THEN INDUCT_TAC THEN
REWRITE_TAC[real_pow] THENL
[REWRITE_TAC[GSYM int_of_num; int_of_num_th];
POP_ASSUM(SUBST1_TAC o SYM) THEN
ASM_REWRITE_TAC[GSYM int_mul; int_mul_th]]);;
(* ------------------------------------------------------------------------- *)
(* A few convenient theorems about the integer type. *)
(* ------------------------------------------------------------------------- *)
let INT_IMAGE = prove
(`!x. (?n. x = &n) \/ (?n. x = --(&n))`,
GEN_TAC THEN
X_CHOOSE_THEN `n:num` DISJ_CASES_TAC (SPEC `x:int` dest_int_rep) THEN
POP_ASSUM(MP_TAC o AP_TERM `int_of_real`) THEN REWRITE_TAC[int_abstr] THEN
DISCH_THEN SUBST1_TAC THEN REWRITE_TAC[int_of_num; int_neg] THENL
[DISJ1_TAC; DISJ2_TAC] THEN
EXISTS_TAC `n:num` THEN REWRITE_TAC[int_abstr] THEN
REWRITE_TAC[GSYM int_of_num; int_of_num_th]);;
let FORALL_INT_CASES = prove
(`!P:int->bool. (!x. P x) <=> (!n. P(&n)) /\ (!n. P(-- &n))`,
MESON_TAC[INT_IMAGE]);;
let INT_LT_DISCRETE = prove
(`!x y. x < y <=> (x + &1) <= y`,
REPEAT GEN_TAC THEN
REWRITE_TAC[int_le; int_lt; int_add_th] THEN
DISJ_CASES_THEN(X_CHOOSE_THEN `m:num` SUBST1_TAC )
(SPEC `x:int` INT_IMAGE) THEN
DISJ_CASES_THEN(X_CHOOSE_THEN `n:num` SUBST1_TAC )
(SPEC `y:int` INT_IMAGE) THEN
REWRITE_TAC[int_neg_th; int_of_num_th] THEN
REWRITE_TAC[REAL_LE_NEG2; REAL_LT_NEG2] THEN
REWRITE_TAC[REAL_LE_LNEG; REAL_LT_LNEG; REAL_LE_RNEG; REAL_LT_RNEG] THEN
REWRITE_TAC[GSYM REAL_ADD_ASSOC] THEN
ONCE_REWRITE_TAC[REAL_ADD_SYM] THEN
REWRITE_TAC[GSYM real_sub; REAL_LE_SUB_RADD] THEN
REWRITE_TAC[REAL_OF_NUM_LE; REAL_OF_NUM_LT; REAL_OF_NUM_ADD] THEN
REWRITE_TAC[GSYM ADD1; ONCE_REWRITE_RULE[ADD_SYM] (GSYM ADD1)] THEN
REWRITE_TAC[SYM(REWRITE_CONV[ARITH_SUC] `SUC 0`)] THEN
REWRITE_TAC[ADD_CLAUSES; LE_SUC_LT; LT_SUC_LE]);;
let INT_GT_DISCRETE = prove
(`!x y. x > y <=> x >= (y + &1)`,
REWRITE_TAC[int_gt; int_ge; real_ge; real_gt; GSYM int_le; GSYM int_lt] THEN
MATCH_ACCEPT_TAC INT_LT_DISCRETE);;
(* ------------------------------------------------------------------------- *)
(* Conversions of integer constants to and from OCaml numbers. *)
(* ------------------------------------------------------------------------- *)
let is_intconst tm =
match tm with
Comb(Const("int_of_num",_),n) -> is_numeral n
| Comb(Const("int_neg",_),Comb(Const("int_of_num",_),n)) ->
is_numeral n && not(dest_numeral n = num_0)
| _ -> false;;
let dest_intconst tm =
match tm with
Comb(Const("int_of_num",_),n) -> dest_numeral n
| Comb(Const("int_neg",_),Comb(Const("int_of_num",_),n)) ->
let nn = dest_numeral n in
if nn <>/ num_0 then minus_num(dest_numeral n)
else failwith "dest_intconst"
| _ -> failwith "dest_intconst";;
let mk_intconst =
let cast_tm = `int_of_num` and neg_tm = `int_neg` in
let mk_numconst n = mk_comb(cast_tm,mk_numeral n) in
fun x -> if x </ num_0 then mk_comb(neg_tm,mk_numconst(minus_num x))
else mk_numconst x;;
(* ------------------------------------------------------------------------- *)
(* A simple procedure to lift most universal real theorems to integers. *)
(* For a more complete procedure, give required term to INT_ARITH (below). *)
(* ------------------------------------------------------------------------- *)
let INT_OF_REAL_THM =
let dest = `real_of_int`
and real_ty = `:real`
and int_ty = `:int`
and cond_th = prove
(`real_of_int(if b then x else y) =
if b then real_of_int x else real_of_int y`,
COND_CASES_TAC THEN REWRITE_TAC[]) in
let thlist = map GSYM
[int_eq; int_le; int_lt; int_ge; int_gt;
int_of_num_th; int_neg_th; int_add_th; int_mul_th; int_sgn_th;
int_sub_th; int_abs_th; int_max_th; int_min_th; int_pow_th; cond_th] in
let REW_RULE = GEN_REWRITE_RULE DEPTH_CONV thlist in
let int_tm_of_real_var v =
let s,ty = dest_var v in
if ty = real_ty then mk_comb(dest,mk_var(s,int_ty)) else v in
let int_of_real_var v =
let s,ty = dest_var v in
if ty = real_ty then mk_var(s,int_ty) else v in
let INT_OF_REAL_THM1 th =
let newavs = subtract (frees (concl th)) (freesl (hyp th)) in
let avs,bod = strip_forall(concl th) in
let allavs = newavs@avs in
let avs' = map int_tm_of_real_var allavs in
let avs'' = map int_of_real_var avs in
GENL avs'' (REW_RULE(SPECL avs' (GENL newavs th))) in
let rec INT_OF_REAL_THM th =
if is_conj(concl th) then CONJ (INT_OF_REAL_THM (CONJUNCT1 th))
(INT_OF_REAL_THM (CONJUNCT2 th))
else INT_OF_REAL_THM1 th in
INT_OF_REAL_THM;;
(* ------------------------------------------------------------------------- *)
(* Collect together all the theorems derived automatically. *)
(* ------------------------------------------------------------------------- *)
let INT_ABS_0 = INT_OF_REAL_THM REAL_ABS_0;;
let INT_ABS_1 = INT_OF_REAL_THM REAL_ABS_1;;
let INT_ABS_ABS = INT_OF_REAL_THM REAL_ABS_ABS;;
let INT_ABS_BETWEEN = INT_OF_REAL_THM REAL_ABS_BETWEEN;;
let INT_ABS_BETWEEN1 = INT_OF_REAL_THM REAL_ABS_BETWEEN1;;
let INT_ABS_BETWEEN2 = INT_OF_REAL_THM REAL_ABS_BETWEEN2;;
let INT_ABS_BOUND = INT_OF_REAL_THM REAL_ABS_BOUND;;
let INT_ABS_CASES = INT_OF_REAL_THM REAL_ABS_CASES;;
let INT_ABS_CIRCLE = INT_OF_REAL_THM REAL_ABS_CIRCLE;;
let INT_ABS_LE = INT_OF_REAL_THM REAL_ABS_LE;;
let INT_ABS_MUL = INT_OF_REAL_THM REAL_ABS_MUL;;
let INT_ABS_NEG = INT_OF_REAL_THM REAL_ABS_NEG;;
let INT_ABS_NUM = INT_OF_REAL_THM REAL_ABS_NUM;;
let INT_ABS_NZ = INT_OF_REAL_THM REAL_ABS_NZ;;
let INT_ABS_POS = INT_OF_REAL_THM REAL_ABS_POS;;
let INT_ABS_POW = INT_OF_REAL_THM REAL_ABS_POW;;
let INT_ABS_REFL = INT_OF_REAL_THM REAL_ABS_REFL;;
let INT_ABS_SGN = INT_OF_REAL_THM REAL_ABS_SGN;;
let INT_ABS_SIGN = INT_OF_REAL_THM REAL_ABS_SIGN;;
let INT_ABS_SIGN2 = INT_OF_REAL_THM REAL_ABS_SIGN2;;
let INT_ABS_STILLNZ = INT_OF_REAL_THM REAL_ABS_STILLNZ;;
let INT_ABS_SUB = INT_OF_REAL_THM REAL_ABS_SUB;;
let INT_ABS_SUB_ABS = INT_OF_REAL_THM REAL_ABS_SUB_ABS;;
let INT_ABS_TRIANGLE = INT_OF_REAL_THM REAL_ABS_TRIANGLE;;
let INT_ABS_ZERO = INT_OF_REAL_THM REAL_ABS_ZERO;;
let INT_ADD2_SUB2 = INT_OF_REAL_THM REAL_ADD2_SUB2;;
let INT_ADD_AC = INT_OF_REAL_THM REAL_ADD_AC;;
let INT_ADD_ASSOC = INT_OF_REAL_THM REAL_ADD_ASSOC;;
let INT_ADD_LDISTRIB = INT_OF_REAL_THM REAL_ADD_LDISTRIB;;
let INT_ADD_LID = INT_OF_REAL_THM REAL_ADD_LID;;
let INT_ADD_LINV = INT_OF_REAL_THM REAL_ADD_LINV;;
let INT_ADD_RDISTRIB = INT_OF_REAL_THM REAL_ADD_RDISTRIB;;
let INT_ADD_RID = INT_OF_REAL_THM REAL_ADD_RID;;
let INT_ADD_RINV = INT_OF_REAL_THM REAL_ADD_RINV;;
let INT_ADD_SUB = INT_OF_REAL_THM REAL_ADD_SUB;;
let INT_ADD_SUB2 = INT_OF_REAL_THM REAL_ADD_SUB2;;
let INT_ADD_SYM = INT_OF_REAL_THM REAL_ADD_SYM;;
let INT_BOUNDS_LE = INT_OF_REAL_THM REAL_BOUNDS_LE;;
let INT_BOUNDS_LT = INT_OF_REAL_THM REAL_BOUNDS_LT;;
let INT_DIFFSQ = INT_OF_REAL_THM REAL_DIFFSQ;;
let INT_ENTIRE = INT_OF_REAL_THM REAL_ENTIRE;;
let INT_EQ_ADD_LCANCEL = INT_OF_REAL_THM REAL_EQ_ADD_LCANCEL;;
let INT_EQ_ADD_LCANCEL_0 = INT_OF_REAL_THM REAL_EQ_ADD_LCANCEL_0;;
let INT_EQ_ADD_RCANCEL = INT_OF_REAL_THM REAL_EQ_ADD_RCANCEL;;
let INT_EQ_ADD_RCANCEL_0 = INT_OF_REAL_THM REAL_EQ_ADD_RCANCEL_0;;
let INT_EQ_IMP_LE = INT_OF_REAL_THM REAL_EQ_IMP_LE;;
let INT_EQ_MUL_LCANCEL = INT_OF_REAL_THM REAL_EQ_MUL_LCANCEL;;
let INT_EQ_MUL_RCANCEL = INT_OF_REAL_THM REAL_EQ_MUL_RCANCEL;;
let INT_EQ_NEG2 = INT_OF_REAL_THM REAL_EQ_NEG2;;
let INT_EQ_SGN_ABS = INT_OF_REAL_THM REAL_EQ_SGN_ABS;;
let INT_EQ_SQUARE_ABS = INT_OF_REAL_THM REAL_EQ_SQUARE_ABS;;
let INT_EQ_SUB_LADD = INT_OF_REAL_THM REAL_EQ_SUB_LADD;;
let INT_EQ_SUB_RADD = INT_OF_REAL_THM REAL_EQ_SUB_RADD;;
let INT_LET_ADD = INT_OF_REAL_THM REAL_LET_ADD;;
let INT_LET_ADD2 = INT_OF_REAL_THM REAL_LET_ADD2;;
let INT_LET_ANTISYM = INT_OF_REAL_THM REAL_LET_ANTISYM;;
let INT_LET_TOTAL = INT_OF_REAL_THM REAL_LET_TOTAL;;
let INT_LET_TRANS = INT_OF_REAL_THM REAL_LET_TRANS;;
let INT_LE_01 = INT_OF_REAL_THM REAL_LE_01;;
let INT_LE_ADD = INT_OF_REAL_THM REAL_LE_ADD;;
let INT_LE_ADD2 = INT_OF_REAL_THM REAL_LE_ADD2;;
let INT_LE_ADDL = INT_OF_REAL_THM REAL_LE_ADDL;;
let INT_LE_ADDR = INT_OF_REAL_THM REAL_LE_ADDR;;
let INT_LE_ANTISYM = INT_OF_REAL_THM REAL_LE_ANTISYM;;
let INT_LE_DOUBLE = INT_OF_REAL_THM REAL_LE_DOUBLE;;
let INT_LE_LADD = INT_OF_REAL_THM REAL_LE_LADD;;
let INT_LE_LADD_IMP = INT_OF_REAL_THM REAL_LE_LADD_IMP;;
let INT_LE_LMUL = INT_OF_REAL_THM REAL_LE_LMUL;;
let INT_LE_LNEG = INT_OF_REAL_THM REAL_LE_LNEG;;
let INT_LE_LT = INT_OF_REAL_THM REAL_LE_LT;;
let INT_LE_MAX = INT_OF_REAL_THM REAL_LE_MAX;;
let INT_LE_MIN = INT_OF_REAL_THM REAL_LE_MIN;;
let INT_LE_MUL = INT_OF_REAL_THM REAL_LE_MUL;;
let INT_LE_MUL_EQ = INT_OF_REAL_THM REAL_LE_MUL_EQ;;
let INT_LE_NEG2 = INT_OF_REAL_THM REAL_LE_NEG2;;
let INT_LE_NEGL = INT_OF_REAL_THM REAL_LE_NEGL;;
let INT_LE_NEGR = INT_OF_REAL_THM REAL_LE_NEGR;;
let INT_LE_NEGTOTAL = INT_OF_REAL_THM REAL_LE_NEGTOTAL;;
let INT_LE_POW2 = INT_OF_REAL_THM REAL_LE_POW2;;
let INT_LE_RADD = INT_OF_REAL_THM REAL_LE_RADD;;
let INT_LE_REFL = INT_OF_REAL_THM REAL_LE_REFL;;
let INT_LE_RMUL = INT_OF_REAL_THM REAL_LE_RMUL;;
let INT_LE_RNEG = INT_OF_REAL_THM REAL_LE_RNEG;;
let INT_LE_SQUARE = INT_OF_REAL_THM REAL_LE_SQUARE;;
let INT_LE_SQUARE_ABS = INT_OF_REAL_THM REAL_LE_SQUARE_ABS;;
let INT_LE_SUB_LADD = INT_OF_REAL_THM REAL_LE_SUB_LADD;;
let INT_LE_SUB_RADD = INT_OF_REAL_THM REAL_LE_SUB_RADD;;
let INT_LE_TOTAL = INT_OF_REAL_THM REAL_LE_TOTAL;;
let INT_LE_TRANS = INT_OF_REAL_THM REAL_LE_TRANS;;
let INT_LNEG_UNIQ = INT_OF_REAL_THM REAL_LNEG_UNIQ;;
let INT_LTE_ADD = INT_OF_REAL_THM REAL_LTE_ADD;;
let INT_LTE_ADD2 = INT_OF_REAL_THM REAL_LTE_ADD2;;
let INT_LTE_ANTISYM = INT_OF_REAL_THM REAL_LTE_ANTISYM;;
let INT_LTE_TOTAL = INT_OF_REAL_THM REAL_LTE_TOTAL;;
let INT_LTE_TRANS = INT_OF_REAL_THM REAL_LTE_TRANS;;
let INT_LT_01 = INT_OF_REAL_THM REAL_LT_01;;
let INT_LT_ADD = INT_OF_REAL_THM REAL_LT_ADD;;
let INT_LT_ADD1 = INT_OF_REAL_THM REAL_LT_ADD1;;
let INT_LT_ADD2 = INT_OF_REAL_THM REAL_LT_ADD2;;
let INT_LT_ADDL = INT_OF_REAL_THM REAL_LT_ADDL;;
let INT_LT_ADDNEG = INT_OF_REAL_THM REAL_LT_ADDNEG;;
let INT_LT_ADDNEG2 = INT_OF_REAL_THM REAL_LT_ADDNEG2;;
let INT_LT_ADDR = INT_OF_REAL_THM REAL_LT_ADDR;;
let INT_LT_ADD_SUB = INT_OF_REAL_THM REAL_LT_ADD_SUB;;
let INT_LT_ANTISYM = INT_OF_REAL_THM REAL_LT_ANTISYM;;
let INT_LT_GT = INT_OF_REAL_THM REAL_LT_GT;;
let INT_LT_IMP_LE = INT_OF_REAL_THM REAL_LT_IMP_LE;;
let INT_LT_IMP_NE = INT_OF_REAL_THM REAL_LT_IMP_NE;;
let INT_LT_LADD = INT_OF_REAL_THM REAL_LT_LADD;;
let INT_LT_LE = INT_OF_REAL_THM REAL_LT_LE;;
let INT_LT_LMUL_EQ = INT_OF_REAL_THM REAL_LT_LMUL_EQ;;
let INT_LT_MAX = INT_OF_REAL_THM REAL_LT_MAX;;
let INT_LT_MIN = INT_OF_REAL_THM REAL_LT_MIN;;
let INT_LT_MUL = INT_OF_REAL_THM REAL_LT_MUL;;
let INT_LT_MUL_EQ = INT_OF_REAL_THM REAL_LT_MUL_EQ;;
let INT_LT_NEG2 = INT_OF_REAL_THM REAL_LT_NEG2;;
let INT_LT_NEGTOTAL = INT_OF_REAL_THM REAL_LT_NEGTOTAL;;
let INT_LT_POW2 = INT_OF_REAL_THM REAL_LT_POW2;;
let INT_LT_RADD = INT_OF_REAL_THM REAL_LT_RADD;;
let INT_LT_REFL = INT_OF_REAL_THM REAL_LT_REFL;;
let INT_LT_RMUL_EQ = INT_OF_REAL_THM REAL_LT_RMUL_EQ;;
let INT_LT_SQUARE_ABS = INT_OF_REAL_THM REAL_LT_SQUARE_ABS;;
let INT_LT_SUB_LADD = INT_OF_REAL_THM REAL_LT_SUB_LADD;;
let INT_LT_SUB_RADD = INT_OF_REAL_THM REAL_LT_SUB_RADD;;
let INT_LT_TOTAL = INT_OF_REAL_THM REAL_LT_TOTAL;;
let INT_LT_TRANS = INT_OF_REAL_THM REAL_LT_TRANS;;
let INT_MAX_ACI = INT_OF_REAL_THM REAL_MAX_ACI;;
let INT_MAX_ASSOC = INT_OF_REAL_THM REAL_MAX_ASSOC;;
let INT_MAX_LE = INT_OF_REAL_THM REAL_MAX_LE;;
let INT_MAX_LT = INT_OF_REAL_THM REAL_MAX_LT;;
let INT_MAX_MAX = INT_OF_REAL_THM REAL_MAX_MAX;;
let INT_MAX_MIN = INT_OF_REAL_THM REAL_MAX_MIN;;
let INT_MAX_SYM = INT_OF_REAL_THM REAL_MAX_SYM;;
let INT_MIN_ACI = INT_OF_REAL_THM REAL_MIN_ACI;;
let INT_MIN_ASSOC = INT_OF_REAL_THM REAL_MIN_ASSOC;;
let INT_MIN_LE = INT_OF_REAL_THM REAL_MIN_LE;;
let INT_MIN_LT = INT_OF_REAL_THM REAL_MIN_LT;;
let INT_MIN_MAX = INT_OF_REAL_THM REAL_MIN_MAX;;
let INT_MIN_MIN = INT_OF_REAL_THM REAL_MIN_MIN;;
let INT_MIN_SYM = INT_OF_REAL_THM REAL_MIN_SYM;;
let INT_MUL_AC = INT_OF_REAL_THM REAL_MUL_AC;;
let INT_MUL_ASSOC = INT_OF_REAL_THM REAL_MUL_ASSOC;;
let INT_MUL_LID = INT_OF_REAL_THM REAL_MUL_LID;;
let INT_MUL_LNEG = INT_OF_REAL_THM REAL_MUL_LNEG;;
let INT_MUL_LZERO = INT_OF_REAL_THM REAL_MUL_LZERO;;
let INT_MUL_POS_LE = INT_OF_REAL_THM REAL_MUL_POS_LE;;
let INT_MUL_POS_LT = INT_OF_REAL_THM REAL_MUL_POS_LT;;
let INT_MUL_RID = INT_OF_REAL_THM REAL_MUL_RID;;
let INT_MUL_RNEG = INT_OF_REAL_THM REAL_MUL_RNEG;;
let INT_MUL_RZERO = INT_OF_REAL_THM REAL_MUL_RZERO;;
let INT_MUL_SYM = INT_OF_REAL_THM REAL_MUL_SYM;;
let INT_NEG_0 = INT_OF_REAL_THM REAL_NEG_0;;
let INT_NEG_ADD = INT_OF_REAL_THM REAL_NEG_ADD;;
let INT_NEG_EQ = INT_OF_REAL_THM REAL_NEG_EQ;;
let INT_NEG_EQ_0 = INT_OF_REAL_THM REAL_NEG_EQ_0;;
let INT_NEG_GE0 = INT_OF_REAL_THM REAL_NEG_GE0;;
let INT_NEG_GT0 = INT_OF_REAL_THM REAL_NEG_GT0;;
let INT_NEG_LE0 = INT_OF_REAL_THM REAL_NEG_LE0;;
let INT_NEG_LMUL = INT_OF_REAL_THM REAL_NEG_LMUL;;
let INT_NEG_LT0 = INT_OF_REAL_THM REAL_NEG_LT0;;
let INT_NEG_MINUS1 = INT_OF_REAL_THM REAL_NEG_MINUS1;;
let INT_NEG_MUL2 = INT_OF_REAL_THM REAL_NEG_MUL2;;
let INT_NEG_NEG = INT_OF_REAL_THM REAL_NEG_NEG;;
let INT_NEG_RMUL = INT_OF_REAL_THM REAL_NEG_RMUL;;
let INT_NEG_SUB = INT_OF_REAL_THM REAL_NEG_SUB;;
let INT_NOT_EQ = INT_OF_REAL_THM REAL_NOT_EQ;;
let INT_NOT_LE = INT_OF_REAL_THM REAL_NOT_LE;;
let INT_NOT_LT = INT_OF_REAL_THM REAL_NOT_LT;;
let INT_OF_NUM_ADD = INT_OF_REAL_THM REAL_OF_NUM_ADD;;
let INT_OF_NUM_EQ = INT_OF_REAL_THM REAL_OF_NUM_EQ;;
let INT_OF_NUM_GE = INT_OF_REAL_THM REAL_OF_NUM_GE;;
let INT_OF_NUM_GT = INT_OF_REAL_THM REAL_OF_NUM_GT;;
let INT_OF_NUM_LE = INT_OF_REAL_THM REAL_OF_NUM_LE;;
let INT_OF_NUM_LT = INT_OF_REAL_THM REAL_OF_NUM_LT;;
let INT_OF_NUM_MAX = INT_OF_REAL_THM REAL_OF_NUM_MAX;;
let INT_OF_NUM_MIN = INT_OF_REAL_THM REAL_OF_NUM_MIN;;
let INT_OF_NUM_MUL = INT_OF_REAL_THM REAL_OF_NUM_MUL;;
let INT_OF_NUM_POW = INT_OF_REAL_THM REAL_OF_NUM_POW;;
let INT_OF_NUM_SUB = INT_OF_REAL_THM REAL_OF_NUM_SUB;;
let INT_OF_NUM_SUC = INT_OF_REAL_THM REAL_OF_NUM_SUC;;
let INT_POS = INT_OF_REAL_THM REAL_POS;;
let INT_POS_NZ = INT_OF_REAL_THM REAL_LT_IMP_NZ;;
let INT_POW2_ABS = INT_OF_REAL_THM REAL_POW2_ABS;;
let INT_POW_1 = INT_OF_REAL_THM REAL_POW_1;;
let INT_POW_1_LE = INT_OF_REAL_THM REAL_POW_1_LE;;
let INT_POW_1_LT = INT_OF_REAL_THM REAL_POW_1_LT;;
let INT_POW_2 = INT_OF_REAL_THM REAL_POW_2;;
let INT_POW_ADD = INT_OF_REAL_THM REAL_POW_ADD;;
let INT_POW_EQ = INT_OF_REAL_THM REAL_POW_EQ;;
let INT_POW_EQ_0 = INT_OF_REAL_THM REAL_POW_EQ_0;;
let INT_POW_EQ_ABS = INT_OF_REAL_THM REAL_POW_EQ_ABS;;
let INT_POW_LE = INT_OF_REAL_THM REAL_POW_LE;;
let INT_POW_LE2 = INT_OF_REAL_THM REAL_POW_LE2;;
let INT_POW_LE2_ODD = INT_OF_REAL_THM REAL_POW_LE2_ODD;;
let INT_POW_LE2_REV = INT_OF_REAL_THM REAL_POW_LE2_REV;;
let INT_POW_LE_1 = INT_OF_REAL_THM REAL_POW_LE_1;;
let INT_POW_LT = INT_OF_REAL_THM REAL_POW_LT;;
let INT_POW_LT2 = INT_OF_REAL_THM REAL_POW_LT2;;
let INT_POW_LT2_REV = INT_OF_REAL_THM REAL_POW_LT2_REV;;
let INT_POW_LT_1 = INT_OF_REAL_THM REAL_POW_LT_1;;
let INT_POW_MONO = INT_OF_REAL_THM REAL_POW_MONO;;
let INT_POW_MONO_LT = INT_OF_REAL_THM REAL_POW_MONO_LT;;
let INT_POW_MUL = INT_OF_REAL_THM REAL_POW_MUL;;
let INT_POW_NEG = INT_OF_REAL_THM REAL_POW_NEG;;
let INT_POW_NZ = INT_OF_REAL_THM REAL_POW_NZ;;
let INT_POW_ONE = INT_OF_REAL_THM REAL_POW_ONE;;
let INT_POW_POW = INT_OF_REAL_THM REAL_POW_POW;;
let INT_POW_ZERO = INT_OF_REAL_THM REAL_POW_ZERO;;
let INT_RNEG_UNIQ = INT_OF_REAL_THM REAL_RNEG_UNIQ;;
let INT_SGN = INT_OF_REAL_THM real_sgn;;
let INT_SGN_0 = INT_OF_REAL_THM REAL_SGN_0;;
let INT_SGN_ABS = INT_OF_REAL_THM REAL_SGN_ABS;;
let INT_SGN_ABS_ALT = INT_OF_REAL_THM REAL_SGN_ABS_ALT;;
let INT_SGN_CASES = INT_OF_REAL_THM REAL_SGN_CASES;;
let INT_SGN_EQ = INT_OF_REAL_THM REAL_SGN_EQ;;
let INT_SGN_EQ_INEQ = INT_OF_REAL_THM REAL_SGN_EQ_INEQ;;
let INT_SGN_INEQS = INT_OF_REAL_THM REAL_SGN_INEQS;;
let INT_SGN_MUL = INT_OF_REAL_THM REAL_SGN_MUL;;
let INT_SGN_NEG = INT_OF_REAL_THM REAL_SGN_NEG;;
let INT_SGN_POW = INT_OF_REAL_THM REAL_SGN_POW;;
let INT_SGN_POW_2 = INT_OF_REAL_THM REAL_SGN_POW_2;;
let INT_SGN_INT_SGN = INT_OF_REAL_THM REAL_SGN_REAL_SGN;;
let INT_SGNS_EQ = INT_OF_REAL_THM REAL_SGNS_EQ;;
let INT_SGNS_EQ_ALT = INT_OF_REAL_THM REAL_SGNS_EQ_ALT;;
let INT_SOS_EQ_0 = INT_OF_REAL_THM REAL_SOS_EQ_0;;
let INT_SUB_0 = INT_OF_REAL_THM REAL_SUB_0;;
let INT_SUB_ABS = INT_OF_REAL_THM REAL_SUB_ABS;;
let INT_SUB_ADD = INT_OF_REAL_THM REAL_SUB_ADD;;
let INT_SUB_ADD2 = INT_OF_REAL_THM REAL_SUB_ADD2;;
let INT_SUB_LDISTRIB = INT_OF_REAL_THM REAL_SUB_LDISTRIB;;
let INT_SUB_LE = INT_OF_REAL_THM REAL_SUB_LE;;
let INT_SUB_LNEG = INT_OF_REAL_THM REAL_SUB_LNEG;;
let INT_SUB_LT = INT_OF_REAL_THM REAL_SUB_LT;;
let INT_SUB_LZERO = INT_OF_REAL_THM REAL_SUB_LZERO;;
let INT_SUB_NEG2 = INT_OF_REAL_THM REAL_SUB_NEG2;;
let INT_SUB_RDISTRIB = INT_OF_REAL_THM REAL_SUB_RDISTRIB;;
let INT_SUB_REFL = INT_OF_REAL_THM REAL_SUB_REFL;;
let INT_SUB_RNEG = INT_OF_REAL_THM REAL_SUB_RNEG;;
let INT_SUB_RZERO = INT_OF_REAL_THM REAL_SUB_RZERO;;
let INT_SUB_SUB = INT_OF_REAL_THM REAL_SUB_SUB;;
let INT_SUB_SUB2 = INT_OF_REAL_THM REAL_SUB_SUB2;;
let INT_SUB_TRIANGLE = INT_OF_REAL_THM REAL_SUB_TRIANGLE;;
let INT_WLOG_LE = prove
(`(!x y:int. P x y <=> P y x) /\ (!x y. x <= y ==> P x y) ==> !x y. P x y`,
MESON_TAC[INT_LE_TOTAL]);;
let INT_WLOG_LT = prove
(`(!x:int. P x x) /\ (!x y. P x y <=> P y x) /\ (!x y. x < y ==> P x y)
==> !x y. P x y`,
MESON_TAC[INT_LT_TOTAL]);;
let INT_WLOG_LE_3 = prove
(`!P. (!x y z. P x y z ==> P y x z /\ P x z y) /\
(!x y z:int. x <= y /\ y <= z ==> P x y z)
==> !x y z. P x y z`,
MESON_TAC[INT_LE_TOTAL]);;
(* ------------------------------------------------------------------------- *)
(* More useful "image" theorems. *)
(* ------------------------------------------------------------------------- *)
let INT_FORALL_POS = prove
(`!P. (!n. P(&n)) <=> (!i:int. &0 <= i ==> P(i))`,
GEN_TAC THEN EQ_TAC THEN DISCH_TAC THEN GEN_TAC THENL
[DISJ_CASES_THEN (CHOOSE_THEN SUBST1_TAC) (SPEC `i:int` INT_IMAGE) THEN
ASM_REWRITE_TAC[INT_LE_RNEG; INT_ADD_LID; INT_OF_NUM_LE; LE] THEN
DISCH_THEN SUBST1_TAC THEN ASM_REWRITE_TAC[INT_NEG_0];
FIRST_ASSUM MATCH_MP_TAC THEN REWRITE_TAC[INT_OF_NUM_LE; LE_0]]);;
let INT_EXISTS_POS = prove
(`!P. (?n. P(&n)) <=> (?i:int. &0 <= i /\ P(i))`,
GEN_TAC THEN GEN_REWRITE_TAC I [TAUT `(p <=> q) <=> (~p <=> ~q)`] THEN
REWRITE_TAC[NOT_EXISTS_THM; INT_FORALL_POS] THEN MESON_TAC[]);;
let INT_FORALL_ABS = prove
(`!P. (!n. P(&n)) <=> (!x:int. P(abs x))`,
REWRITE_TAC[INT_FORALL_POS] THEN MESON_TAC[INT_ABS_POS; INT_ABS_REFL]);;
let INT_EXISTS_ABS = prove
(`!P. (?n. P(&n)) <=> (?x:int. P(abs x))`,
GEN_TAC THEN GEN_REWRITE_TAC I [TAUT `(p <=> q) <=> (~p <=> ~q)`] THEN
REWRITE_TAC[NOT_EXISTS_THM; INT_FORALL_ABS] THEN MESON_TAC[]);;
(* ------------------------------------------------------------------------- *)
(* Sometimes handy in number-theoretic applications. *)
(* ------------------------------------------------------------------------- *)
let INT_ABS_MUL_1 = prove
(`!x y. (abs(x * y) = &1) <=> (abs(x) = &1) /\ (abs(y) = &1)`,
REPEAT GEN_TAC THEN REWRITE_TAC[INT_ABS_MUL] THEN
MP_TAC(SPEC `y:int` INT_ABS_POS) THEN SPEC_TAC(`abs(y)`,`b:int`) THEN
MP_TAC(SPEC `x:int` INT_ABS_POS) THEN SPEC_TAC(`abs(x)`,`a:int`) THEN
REWRITE_TAC[GSYM INT_FORALL_POS; INT_OF_NUM_MUL; INT_OF_NUM_EQ; MULT_EQ_1]);;
let INT_WOP = prove
(`(?x. &0 <= x /\ P x) <=>
(?x. &0 <= x /\ P x /\ !y. &0 <= y /\ P y ==> x <= y)`,
ONCE_REWRITE_TAC[MESON[] `(?x. P x /\ Q x) <=> ~(!x. P x ==> ~Q x)`] THEN
REWRITE_TAC[IMP_CONJ; GSYM INT_FORALL_POS; INT_OF_NUM_LE] THEN
REWRITE_TAC[NOT_FORALL_THM] THEN GEN_REWRITE_TAC LAND_CONV [num_WOP] THEN
REWRITE_TAC[GSYM NOT_LE; CONTRAPOS_THM]);;
(* ------------------------------------------------------------------------- *)
(* A few "pseudo definitions". *)
(* ------------------------------------------------------------------------- *)
let INT_POW = prove
(`(x pow 0 = &1) /\
(!n. x pow (SUC n) = x * x pow n)`,
REWRITE_TAC(map INT_OF_REAL_THM (CONJUNCTS real_pow)));;
let INT_ABS = prove
(`!x. abs(x) = if &0 <= x then x else --x`,
GEN_TAC THEN MP_TAC(INT_OF_REAL_THM(SPEC `x:real` real_abs)) THEN
COND_CASES_TAC THEN REWRITE_TAC[int_eq]);;
let INT_GE = prove
(`!x y. x >= y <=> y <= x`,
REWRITE_TAC[int_ge; int_le; real_ge]);;
let INT_GT = prove
(`!x y. x > y <=> y < x`,
REWRITE_TAC[int_gt; int_lt; real_gt]);;
let INT_LT = prove
(`!x y. x < y <=> ~(y <= x)`,
REWRITE_TAC[int_lt; int_le; real_lt]);;
(* ------------------------------------------------------------------------- *)
(* Now a decision procedure for the integers. *)
(* ------------------------------------------------------------------------- *)
let INT_ARITH =
let atom_CONV =
let pth = prove
(`(~(x <= y) <=> y + &1 <= x) /\
(~(x < y) <=> y <= x) /\
(~(x = y) <=> x + &1 <= y \/ y + &1 <= x) /\
(x < y <=> x + &1 <= y)`,
REWRITE_TAC[INT_NOT_LE; INT_NOT_LT; INT_NOT_EQ; INT_LT_DISCRETE]) in
GEN_REWRITE_CONV I [pth]
and bub_CONV = GEN_REWRITE_CONV TOP_SWEEP_CONV
[int_eq; int_le; int_lt; int_ge; int_gt;
int_of_num_th; int_neg_th; int_add_th; int_mul_th;
int_sub_th; int_pow_th; int_abs_th; int_max_th; int_min_th] in
let base_CONV = TRY_CONV atom_CONV THENC bub_CONV in
let NNF_NORM_CONV = GEN_NNF_CONV false
(base_CONV,fun t -> base_CONV t,base_CONV(mk_neg t)) in
let init_CONV =
TOP_DEPTH_CONV BETA_CONV THENC
PRESIMP_CONV THENC
GEN_REWRITE_CONV DEPTH_CONV [INT_GT; INT_GE] THENC
NNF_CONV THENC DEPTH_BINOP_CONV `(\/)` CONDS_ELIM_CONV THENC
NNF_NORM_CONV in
let p_tm = `p:bool`
and not_tm = `(~)` in
let pth = TAUT(mk_eq(mk_neg(mk_neg p_tm),p_tm)) in
fun tm ->
let th0 = INST [tm,p_tm] pth
and th1 = init_CONV (mk_neg tm) in
let th2 = REAL_ARITH(mk_neg(rand(concl th1))) in
EQ_MP th0 (EQ_MP (AP_TERM not_tm (SYM th1)) th2);;
let INT_ARITH_TAC = CONV_TAC(EQT_INTRO o INT_ARITH);;
let ASM_INT_ARITH_TAC =
REPEAT(FIRST_X_ASSUM(MP_TAC o check (not o is_forall o concl))) THEN
INT_ARITH_TAC;;
(* ------------------------------------------------------------------------- *)
(* Some pseudo-definitions. *)
(* ------------------------------------------------------------------------- *)
let INT_SUB = INT_ARITH `!x y. x - y = x + --y`;;
let INT_MAX = INT_ARITH `!x y. max x y = if x <= y then y else x`;;
let INT_MIN = INT_ARITH `!x y. min x y = if x <= y then x else y`;;
(* ------------------------------------------------------------------------- *)
(* Additional useful lemmas. *)
(* ------------------------------------------------------------------------- *)
let INT_OF_NUM_EXISTS = prove
(`!x:int. (?n. x = &n) <=> &0 <= x`,
GEN_TAC THEN EQ_TAC THEN STRIP_TAC THEN ASM_SIMP_TAC[INT_POS] THEN
MP_TAC(ISPEC `x:int` INT_IMAGE) THEN
REWRITE_TAC[OR_EXISTS_THM] THEN MATCH_MP_TAC MONO_EXISTS THEN
ASM_INT_ARITH_TAC);;
let INT_LE_DISCRETE = INT_ARITH `!x y:int. x <= y <=> x < y + &1`;;
let INT_LE_TRANS_LE = prove
(`!x y:int. x <= y <=> (!z. y <= z ==> x <= z)`,
MESON_TAC[INT_LE_TRANS; INT_LE_REFL]);;
let INT_LE_TRANS_LT = prove
(`!x y:int. x <= y <=> (!z. y < z ==> x < z)`,
REPEAT GEN_TAC THEN EQ_TAC THENL [INT_ARITH_TAC; ALL_TAC] THEN
DISCH_THEN(MP_TAC o SPEC `y + &1:int`) THEN INT_ARITH_TAC);;
(* ------------------------------------------------------------------------- *)
(* Archimedian property for the integers. *)
(* ------------------------------------------------------------------------- *)
let INT_ARCH = prove
(`!x d. ~(d = &0) ==> ?c. x < c * d`,
SUBGOAL_THEN `!x. &0 <= x ==> ?n. x <= &n` ASSUME_TAC THENL
[REWRITE_TAC[GSYM INT_FORALL_POS; INT_OF_NUM_LE] THEN MESON_TAC[LE_REFL];
ALL_TAC] THEN
SUBGOAL_THEN `!x. ?n. x <= &n` ASSUME_TAC THENL
[ASM_MESON_TAC[INT_LE_TOTAL]; ALL_TAC] THEN
SUBGOAL_THEN `!x d. &0 < d ==> ?c. x < c * d` ASSUME_TAC THENL
[REPEAT GEN_TAC THEN REWRITE_TAC[INT_LT_DISCRETE; INT_ADD_LID] THEN
ASM_MESON_TAC[INT_POS; INT_LE_LMUL; INT_ARITH
`x + &1 <= &n /\ &n * &1 <= &n * d ==> x + &1 <= &n * d`];
ALL_TAC] THEN
SUBGOAL_THEN `!x d. ~(d = &0) ==> ?c. x < c * d` ASSUME_TAC THENL
[ASM_MESON_TAC[INT_ARITH `--x * y = x * --y`;
INT_ARITH `~(d = &0) ==> &0 < d \/ &0 < --d`];
ALL_TAC] THEN
ASM_MESON_TAC[INT_ARITH `--x * y = x * --y`;
INT_ARITH `~(d = &0) ==> &0 < d \/ &0 < --d`]);;
(* ------------------------------------------------------------------------- *)
(* Definitions of ("Euclidean") integer division and remainder. *)
(* ------------------------------------------------------------------------- *)
let INT_DIVMOD_EXIST_0 = prove
(`!m n:int. ?q r. if n = &0 then q = &0 /\ r = m
else &0 <= r /\ r < abs(n) /\ m = q * n + r`,
REPEAT GEN_TAC THEN ASM_CASES_TAC `n = &0` THEN
ASM_REWRITE_TAC[RIGHT_EXISTS_AND_THM; EXISTS_REFL] THEN
GEN_REWRITE_TAC I [SWAP_EXISTS_THM] THEN
SUBGOAL_THEN `?r. &0 <= r /\ ?q:int. m = n * q + r` MP_TAC THENL
[FIRST_ASSUM(MP_TAC o SPEC `--m:int` o MATCH_MP INT_ARCH) THEN
DISCH_THEN(X_CHOOSE_TAC `s:int`) THEN
EXISTS_TAC `m + s * n:int` THEN CONJ_TAC THENL
[ASM_INT_ARITH_TAC; EXISTS_TAC `--s:int` THEN INT_ARITH_TAC];
GEN_REWRITE_TAC LAND_CONV [INT_WOP] THEN
MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `r:int` THEN
REWRITE_TAC[LEFT_AND_EXISTS_THM; RIGHT_AND_EXISTS_THM] THEN
MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `q:int` THEN STRIP_TAC THEN
ASM_REWRITE_TAC[] THEN FIRST_X_ASSUM(MP_TAC o SPEC `r - abs n`) THEN
REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
DISCH_THEN(MP_TAC o SPEC `if &0 <= n then q + &1 else q - &1`) THEN
ASM_INT_ARITH_TAC]);;
parse_as_infix("div",(22,"left"));;
parse_as_infix("rem",(22,"left"));;
let INT_DIVISION_0 = new_specification ["div"; "rem"]
(REWRITE_RULE[SKOLEM_THM] INT_DIVMOD_EXIST_0);;
let INT_DIVISION = prove
(`!m n. ~(n = &0)
==> m = m div n * n + m rem n /\ &0 <= m rem n /\ m rem n < abs n`,
MESON_TAC[INT_DIVISION_0]);;
(* ------------------------------------------------------------------------- *)
(* Arithmetic operations on integers. Essentially a clone of stuff for reals *)
(* in the file "calc_int.ml", except for div and rem, which are more like N. *)
(* ------------------------------------------------------------------------- *)
let INT_LE_CONV,INT_LT_CONV,INT_GE_CONV,INT_GT_CONV,INT_EQ_CONV =
let tth =
TAUT `(F /\ F <=> F) /\ (F /\ T <=> F) /\
(T /\ F <=> F) /\ (T /\ T <=> T)` in
let nth = TAUT `(~T <=> F) /\ (~F <=> T)` in
let NUM2_EQ_CONV = BINOP_CONV NUM_EQ_CONV THENC GEN_REWRITE_CONV I [tth] in
let NUM2_NE_CONV =
RAND_CONV NUM2_EQ_CONV THENC
GEN_REWRITE_CONV I [nth] in
let [pth_le1; pth_le2a; pth_le2b; pth_le3] = (CONJUNCTS o prove)
(`(--(&m) <= &n <=> T) /\
(&m <= &n <=> m <= n) /\
(--(&m) <= --(&n) <=> n <= m) /\
(&m <= --(&n) <=> (m = 0) /\ (n = 0))`,
REWRITE_TAC[INT_LE_NEG2] THEN
REWRITE_TAC[INT_LE_LNEG; INT_LE_RNEG] THEN
REWRITE_TAC[INT_OF_NUM_ADD; INT_OF_NUM_LE; LE_0] THEN
REWRITE_TAC[LE; ADD_EQ_0]) in
let INT_LE_CONV = FIRST_CONV
[GEN_REWRITE_CONV I [pth_le1];
GEN_REWRITE_CONV I [pth_le2a; pth_le2b] THENC NUM_LE_CONV;
GEN_REWRITE_CONV I [pth_le3] THENC NUM2_EQ_CONV] in
let [pth_lt1; pth_lt2a; pth_lt2b; pth_lt3] = (CONJUNCTS o prove)
(`(&m < --(&n) <=> F) /\
(&m < &n <=> m < n) /\
(--(&m) < --(&n) <=> n < m) /\
(--(&m) < &n <=> ~((m = 0) /\ (n = 0)))`,
REWRITE_TAC[pth_le1; pth_le2a; pth_le2b; pth_le3;
GSYM NOT_LE; INT_LT] THEN
CONV_TAC TAUT) in
let INT_LT_CONV = FIRST_CONV
[GEN_REWRITE_CONV I [pth_lt1];
GEN_REWRITE_CONV I [pth_lt2a; pth_lt2b] THENC NUM_LT_CONV;
GEN_REWRITE_CONV I [pth_lt3] THENC NUM2_NE_CONV] in
let [pth_ge1; pth_ge2a; pth_ge2b; pth_ge3] = (CONJUNCTS o prove)
(`(&m >= --(&n) <=> T) /\
(&m >= &n <=> n <= m) /\
(--(&m) >= --(&n) <=> m <= n) /\
(--(&m) >= &n <=> (m = 0) /\ (n = 0))`,
REWRITE_TAC[pth_le1; pth_le2a; pth_le2b; pth_le3; INT_GE] THEN
CONV_TAC TAUT) in
let INT_GE_CONV = FIRST_CONV
[GEN_REWRITE_CONV I [pth_ge1];
GEN_REWRITE_CONV I [pth_ge2a; pth_ge2b] THENC NUM_LE_CONV;
GEN_REWRITE_CONV I [pth_ge3] THENC NUM2_EQ_CONV] in
let [pth_gt1; pth_gt2a; pth_gt2b; pth_gt3] = (CONJUNCTS o prove)
(`(--(&m) > &n <=> F) /\
(&m > &n <=> n < m) /\
(--(&m) > --(&n) <=> m < n) /\
(&m > --(&n) <=> ~((m = 0) /\ (n = 0)))`,
REWRITE_TAC[pth_lt1; pth_lt2a; pth_lt2b; pth_lt3; INT_GT] THEN
CONV_TAC TAUT) in
let INT_GT_CONV = FIRST_CONV
[GEN_REWRITE_CONV I [pth_gt1];
GEN_REWRITE_CONV I [pth_gt2a; pth_gt2b] THENC NUM_LT_CONV;
GEN_REWRITE_CONV I [pth_gt3] THENC NUM2_NE_CONV] in
let [pth_eq1a; pth_eq1b; pth_eq2a; pth_eq2b] = (CONJUNCTS o prove)
(`((&m = &n) <=> (m = n)) /\
((--(&m) = --(&n)) <=> (m = n)) /\
((--(&m) = &n) <=> (m = 0) /\ (n = 0)) /\
((&m = --(&n)) <=> (m = 0) /\ (n = 0))`,
REWRITE_TAC[GSYM INT_LE_ANTISYM; GSYM LE_ANTISYM] THEN
REWRITE_TAC[pth_le1; pth_le2a; pth_le2b; pth_le3; LE; LE_0] THEN
CONV_TAC TAUT) in
let INT_EQ_CONV = FIRST_CONV
[GEN_REWRITE_CONV I [pth_eq1a; pth_eq1b] THENC NUM_EQ_CONV;
GEN_REWRITE_CONV I [pth_eq2a; pth_eq2b] THENC NUM2_EQ_CONV] in
INT_LE_CONV,INT_LT_CONV,
INT_GE_CONV,INT_GT_CONV,INT_EQ_CONV;;
let INT_NEG_CONV =
let pth = prove
(`(--(&0) = &0) /\
(--(--(&x)) = &x)`,
REWRITE_TAC[INT_NEG_NEG; INT_NEG_0]) in
GEN_REWRITE_CONV I [pth];;
let INT_MUL_CONV =
let pth0 = prove
(`(&0 * &x = &0) /\
(&0 * --(&x) = &0) /\
(&x * &0 = &0) /\
(--(&x) * &0 = &0)`,
REWRITE_TAC[INT_MUL_LZERO; INT_MUL_RZERO])
and pth1,pth2 = (CONJ_PAIR o prove)
(`((&m * &n = &(m * n)) /\
(--(&m) * --(&n) = &(m * n))) /\
((--(&m) * &n = --(&(m * n))) /\
(&m * --(&n) = --(&(m * n))))`,
REWRITE_TAC[INT_MUL_LNEG; INT_MUL_RNEG; INT_NEG_NEG] THEN
REWRITE_TAC[INT_OF_NUM_MUL]) in
FIRST_CONV
[GEN_REWRITE_CONV I [pth0];
GEN_REWRITE_CONV I [pth1] THENC RAND_CONV NUM_MULT_CONV;
GEN_REWRITE_CONV I [pth2] THENC RAND_CONV(RAND_CONV NUM_MULT_CONV)];;
let INT_ADD_CONV =
let neg_tm = `(--)` in
let amp_tm = `&` in
let add_tm = `(+)` in
let dest = dest_binop `(+)` in
let m_tm = `m:num` and n_tm = `n:num` in
let pth0 = prove
(`(--(&m) + &m = &0) /\
(&m + --(&m) = &0)`,
REWRITE_TAC[INT_ADD_LINV; INT_ADD_RINV]) in
let [pth1; pth2; pth3; pth4; pth5; pth6] = (CONJUNCTS o prove)
(`(--(&m) + --(&n) = --(&(m + n))) /\
(--(&m) + &(m + n) = &n) /\
(--(&(m + n)) + &m = --(&n)) /\
(&(m + n) + --(&m) = &n) /\
(&m + --(&(m + n)) = --(&n)) /\
(&m + &n = &(m + n))`,
REWRITE_TAC[GSYM INT_OF_NUM_ADD; INT_NEG_ADD] THEN
REWRITE_TAC[INT_ADD_ASSOC; INT_ADD_LINV; INT_ADD_LID] THEN
REWRITE_TAC[INT_ADD_RINV; INT_ADD_LID] THEN
ONCE_REWRITE_TAC[INT_ADD_SYM] THEN
REWRITE_TAC[INT_ADD_ASSOC; INT_ADD_LINV; INT_ADD_LID] THEN
REWRITE_TAC[INT_ADD_RINV; INT_ADD_LID]) in
GEN_REWRITE_CONV I [pth0] ORELSEC
(fun tm ->
try let l,r = dest tm in
if rator l = neg_tm then
if rator r = neg_tm then
let th1 = INST [rand(rand l),m_tm; rand(rand r),n_tm] pth1 in
let tm1 = rand(rand(rand(concl th1))) in
let th2 = AP_TERM neg_tm (AP_TERM amp_tm (NUM_ADD_CONV tm1)) in
TRANS th1 th2
else
let m = rand(rand l) and n = rand r in
let m' = dest_numeral m and n' = dest_numeral n in
if m' <=/ n' then
let p = mk_numeral (n' -/ m') in
let th1 = INST [m,m_tm; p,n_tm] pth2 in
let th2 = NUM_ADD_CONV (rand(rand(lhand(concl th1)))) in
let th3 = AP_TERM (rator tm) (AP_TERM amp_tm (SYM th2)) in
TRANS th3 th1
else
let p = mk_numeral (m' -/ n') in
let th1 = INST [n,m_tm; p,n_tm] pth3 in
let th2 = NUM_ADD_CONV (rand(rand(lhand(lhand(concl th1))))) in
let th3 = AP_TERM neg_tm (AP_TERM amp_tm (SYM th2)) in
let th4 = AP_THM (AP_TERM add_tm th3) (rand tm) in
TRANS th4 th1
else
if rator r = neg_tm then
let m = rand l and n = rand(rand r) in
let m' = dest_numeral m and n' = dest_numeral n in
if n' <=/ m' then
let p = mk_numeral (m' -/ n') in
let th1 = INST [n,m_tm; p,n_tm] pth4 in
let th2 = NUM_ADD_CONV (rand(lhand(lhand(concl th1)))) in
let th3 = AP_TERM add_tm (AP_TERM amp_tm (SYM th2)) in
let th4 = AP_THM th3 (rand tm) in
TRANS th4 th1
else
let p = mk_numeral (n' -/ m') in
let th1 = INST [m,m_tm; p,n_tm] pth5 in
let th2 = NUM_ADD_CONV (rand(rand(rand(lhand(concl th1))))) in
let th3 = AP_TERM neg_tm (AP_TERM amp_tm (SYM th2)) in
let th4 = AP_TERM (rator tm) th3 in
TRANS th4 th1
else
let th1 = INST [rand l,m_tm; rand r,n_tm] pth6 in
let tm1 = rand(rand(concl th1)) in
let th2 = AP_TERM amp_tm (NUM_ADD_CONV tm1) in
TRANS th1 th2
with Failure _ -> failwith "INT_ADD_CONV");;
let INT_SUB_CONV =
GEN_REWRITE_CONV I [INT_SUB] THENC
TRY_CONV(RAND_CONV INT_NEG_CONV) THENC
INT_ADD_CONV;;
let INT_POW_CONV =
let pth1,pth2 = (CONJ_PAIR o prove)
(`(&x pow n = &(x EXP n)) /\
((--(&x)) pow n = if EVEN n then &(x EXP n) else --(&(x EXP n)))`,
REWRITE_TAC[INT_OF_NUM_POW; INT_POW_NEG]) in
let tth = prove
(`((if T then x:int else y) = x) /\ ((if F then x:int else y) = y)`,
REWRITE_TAC[]) in
let neg_tm = `(--)` in
(GEN_REWRITE_CONV I [pth1] THENC RAND_CONV NUM_EXP_CONV) ORELSEC
(GEN_REWRITE_CONV I [pth2] THENC
RATOR_CONV(RATOR_CONV(RAND_CONV NUM_EVEN_CONV)) THENC
GEN_REWRITE_CONV I [tth] THENC
(fun tm -> if rator tm = neg_tm then RAND_CONV(RAND_CONV NUM_EXP_CONV) tm
else RAND_CONV NUM_EXP_CONV tm));;
let INT_ABS_CONV =
let pth = prove
(`(abs(--(&x)) = &x) /\
(abs(&x) = &x)`,
REWRITE_TAC[INT_ABS_NEG; INT_ABS_NUM]) in
GEN_REWRITE_CONV I [pth];;
let INT_MAX_CONV =
REWR_CONV INT_MAX THENC
RATOR_CONV(RATOR_CONV(RAND_CONV INT_LE_CONV)) THENC
GEN_REWRITE_CONV I [COND_CLAUSES];;
let INT_MIN_CONV =
REWR_CONV INT_MIN THENC
RATOR_CONV(RATOR_CONV(RAND_CONV INT_LE_CONV)) THENC
GEN_REWRITE_CONV I [COND_CLAUSES];;
(* ------------------------------------------------------------------------- *)
(* Instantiate the normalizer. *)
(* ------------------------------------------------------------------------- *)
let INT_POLY_CONV =
let sth = prove
(`(!x y z. x + (y + z) = (x + y) + z) /\
(!x y. x + y = y + x) /\
(!x. &0 + x = x) /\
(!x y z. x * (y * z) = (x * y) * z) /\
(!x y. x * y = y * x) /\
(!x. &1 * x = x) /\
(!x. &0 * x = &0) /\
(!x y z. x * (y + z) = x * y + x * z) /\
(!x. x pow 0 = &1) /\
(!x n. x pow (SUC n) = x * x pow n)`,
REWRITE_TAC[INT_POW] THEN INT_ARITH_TAC)
and rth = prove
(`(!x. --x = --(&1) * x) /\
(!x y. x - y = x + --(&1) * y)`,
INT_ARITH_TAC)
and is_semiring_constant = is_intconst
and SEMIRING_ADD_CONV = INT_ADD_CONV
and SEMIRING_MUL_CONV = INT_MUL_CONV
and SEMIRING_POW_CONV = INT_POW_CONV in
let _,_,_,_,_,INT_POLY_CONV =
SEMIRING_NORMALIZERS_CONV sth rth
(is_semiring_constant,
SEMIRING_ADD_CONV,SEMIRING_MUL_CONV,SEMIRING_POW_CONV)
(<) in
INT_POLY_CONV;;
(* ------------------------------------------------------------------------- *)