-
Notifications
You must be signed in to change notification settings - Fork 131
/
integerScript.sml
3516 lines (3061 loc) · 133 KB
/
integerScript.sml
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. (John Harrison) *)
(* *)
(* The integers are constructed as equivalence classes of pairs of integers *)
(* using the quotient type procedure. *)
(* *)
(* This theory was constructed for use in the HOL-ELLA system, using many of*)
(* the principles, and some of the code, used in the reals library. It is my*)
(* eventual intention to produce a more unified library of number systems. *)
(* *)
(* October/November 1999. *)
(* Extensions by Michael Norrish to define exponentiation, division and *)
(* modulus. *)
(* *)
(*==========================================================================*)
open HolKernel Parse boolLib
val _ = new_theory "integer";
val _ = set_grammar_ancestry ["arithmetic", "pred_set"]
(* interactive mode
app load ["jrhUtils", "quotient", "liteLib", "QLib",
"BasicProvers", "boolSimps", "pairSimps",
"numSimps", "numLib", "metisLib"];
*)
open jrhUtils quotient liteLib
arithmeticTheory prim_recTheory numTheory
simpLib numLib boolTheory liteLib metisLib BasicProvers;
open bossLib
val _ = temp_delsimps ["NORMEQ_CONV"]
val int_ss = boolSimps.bool_ss ++ numSimps.old_ARITH_ss ++ pairSimps.PAIR_ss;
(*---------------------------------------------------------------------------*)
(* Following incantation needed since pairLib is now loaded, and that adds *)
(* pairTheory.pair_rws to the implicit set of rewrites for REWRITE_TAC. *)
(* Usually that is good, but for some of the proofs below, that makes things *)
(* worse. *)
(*---------------------------------------------------------------------------*)
val _ = Rewrite.set_implicit_rewrites Rewrite.bool_rewrites;
(*--------------------------------------------------------------------------*)
(* Required lemmas about the natural numbers - mostly to drive CANCEL_TAC *)
(*--------------------------------------------------------------------------*)
val EQ_LADD = store_thm("EQ_LADD",
Term `!x y z. (x + y = x + z) = (y = z)`,
ARITH_TAC)
val EQ_ADDL = store_thm("EQ_ADDL",
Term `!x y. (x = x + y) = (y = 0)`,
ARITH_TAC)
val LT_LADD = store_thm("LT_LADD",
Term `!x y z. (x + y) < (x + z) <=> y < z`,
ARITH_TAC)
val LT_ADDL = store_thm("LT_ADDL",
Term `!x y. x < (x + y) <=> 0 < y`,
ARITH_TAC)
val LT_ADDR = store_thm("LT_ADDR",
Term `!x y. ~((x + y) < x)`,
ARITH_TAC)
val LT_ADD2 =
store_thm("LT_ADD2",
Term`!x1 x2 y1 y2. x1 < y1 /\ x2 < y2 ==> (x1 + x2) < (y1 + y2)`,
ARITH_TAC);
(*--------------------------------------------------------------------------*)
(* CANCEL_CONV - Try to cancel, rearranging using AC laws as needed *)
(* *)
(* The first two arguments are the associative and commutative laws, as *)
(* given to AC_CONV. The remaining list of theorems should be of the form: *)
(* *)
(* |- (a & b ~ a & c) = w (e.g. b ~ c) *)
(* |- (a & b ~ a) = x (e.g. F) *)
(* |- (a ~ a & c) = y (e.g. T) *)
(* |- (a ~ a) = z (e.g. F) *)
(* *)
(* For some operator (written as infix &) and relation (~). *)
(* *)
(* Theorems may be of the form |- ~ P or |- P, rather than equations, they *)
(* will be transformed to |- P = F and |- P = T automatically if needed. *)
(* *)
(* Note that terms not cancelled will remain in their original order, but *)
(* will be flattened to right-associated form. *)
(*--------------------------------------------------------------------------*)
fun CANCEL_CONV (assoc,sym,lcancelthms) tm =
let fun pair_from_list [x, y] = (x, y)
| pair_from_list _ = raise Match
val lcthms =
map ((fn th => (assert (is_eq o concl)) th
handle _ => EQF_INTRO th
handle _ => EQT_INTRO th) o SPEC_ALL) lcancelthms
val (eqop, binop) = pair_from_list (map
(rator o rator o lhs o snd o strip_forall o concl) [hd lcthms, sym])
fun strip_binop tm =
if (rator(rator tm) ~~ binop handle _ => false) then
(strip_binop (rand(rator tm))) @ (strip_binop(rand tm))
else [tm]
val mk_binop = ((curry mk_comb) o (curry mk_comb binop))
val list_mk_binop = end_itlist mk_binop
fun rmel i list = op_set_diff aconv list [i]
val (_, (l1, r1)) =
(assert (aconv eqop) ## pair_from_list) (strip_comb tm)
val (l, r) = pair_from_list (map strip_binop [l1, r1])
val i = op_intersect aconv l r
in
if null i then raise Fail ""
else
let val itm = list_mk_binop i
val (l', r') = pair_from_list
(map (end_itlist (C (curry op o)) (map rmel i)) [l, r])
val (l2, r2) = pair_from_list
(map (fn ts => mk_binop itm (list_mk_binop ts)
handle _ => itm) [l',r'])
val (le, re) = pair_from_list
(map (EQT_ELIM o AC_CONV(assoc,sym) o mk_eq)[(l1,l2),(r1,r2)])
val eqv = MK_COMB(AP_TERM eqop le,re)
in
CONV_RULE(RAND_CONV(end_itlist (curry(op ORELSEC))
(map REWR_CONV lcthms))) eqv
end
end handle _ => failwith "CANCEL_CONV";
(*--------------------------------------------------------------------------*)
(* Tactic to do all the obvious simplifications via cancellation etc. *)
(*--------------------------------------------------------------------------*)
val CANCEL_TAC =
(C (curry (op THEN)) (REWRITE_TAC []) o
CONV_TAC o ONCE_DEPTH_CONV o end_itlist (curry (op ORELSEC)))
(map CANCEL_CONV [(ADD_ASSOC,ADD_SYM,
[EQ_LADD, EQ_ADDL, ADD_INV_0_EQ, EQ_SYM_EQ]),
(ADD_ASSOC,ADD_SYM,
[LT_LADD, LT_ADDL, LT_ADDR, LESS_REFL])]);
(*--------------------------------------------------------------------------*)
(* Define operations on representatives. *)
(*--------------------------------------------------------------------------*)
val _ = print "Defining operations on pairs of naturals\n"
val tint_0 = new_definition("tint_0",
Term `tint_0 = (1,1)`);
val tint_1 = new_definition("tint_1",
Term `tint_1 = (1 + 1,1)`);
val tint_neg = new_definition("tint_neg",
Term `tint_neg (x:num,(y:num)) = (y,x)`);
val tint_add =
new_infixl_definition
("tint_add",
Term`$tint_add (x1,y1) (x2,y2) = (x1 + x2, y1 + y2)`,
500);
val tint_mul =
new_infixl_definition
("tint_mul",
Term `$tint_mul (x1,y1) (x2,y2) = ((x1 * x2) + (y1 * y2),
(x1 * y2) + (y1 * x2))`,
600);
val tint_lt = new_definition (
"tint_lt",
Term `$tint_lt (x1,y1) (x2,y2) <=> (x1 + y2) < (x2 + y1)`);
val _ = temp_set_fixity "tint_lt" (Infix(NONASSOC, 450))
(*--------------------------------------------------------------------------*)
(* Define the equivalence relation and prove it *is* one *)
(*--------------------------------------------------------------------------*)
val _ = print "Define equivalence relation over pairs of naturals\n"
val tint_eq = new_definition(
"tint_eq",
Term `$tint_eq (x1,y1) (x2,y2) = (x1 + y2 = x2 + y1)`);
val _ = temp_set_fixity "tint_eq" (Infix(NONASSOC, 450));
val TINT_EQ_REFL =
store_thm("TINT_EQ_REFL",
Term `!x. x tint_eq x`,
GEN_PAIR_TAC THEN REWRITE_TAC[tint_eq]);
val TINT_EQ_SYM =
store_thm("TINT_EQ_SYM",
Term `!x y. x tint_eq y <=> y tint_eq x`,
REPEAT GEN_PAIR_TAC THEN REWRITE_TAC[tint_eq]
THEN ARITH_TAC)
val TINT_EQ_TRANS =
store_thm("TINT_EQ_TRANS",
Term `!x y z. x tint_eq y /\ y tint_eq z ==> x tint_eq z`,
REPEAT GEN_PAIR_TAC THEN REWRITE_TAC[tint_eq]
THEN ARITH_TAC)
val TINT_EQ_EQUIV = store_thm("TINT_EQ_EQUIV",
Term `!p q. p tint_eq q <=> ($tint_eq p = $tint_eq q)`,
REPEAT GEN_TAC THEN CONV_TAC SYM_CONV THEN
CONV_TAC (ONCE_DEPTH_CONV (X_FUN_EQ_CONV (Term `r:num#num`))) THEN EQ_TAC
THENL
[DISCH_THEN(MP_TAC o SPEC (Term `q:num#num`)) THEN REWRITE_TAC[TINT_EQ_REFL],
DISCH_TAC THEN GEN_TAC THEN EQ_TAC THENL
[RULE_ASSUM_TAC(ONCE_REWRITE_RULE[TINT_EQ_SYM]), ALL_TAC] THEN
POP_ASSUM(fn th => DISCH_THEN(MP_TAC o CONJ th)) THEN
MATCH_ACCEPT_TAC TINT_EQ_TRANS]);
val TINT_EQ_AP =
store_thm("TINT_EQ_AP",
Term `!p q. (p = q) ==> p tint_eq q`,
REPEAT GEN_PAIR_TAC
THEN REWRITE_TAC[tint_eq,pairTheory.PAIR_EQ]
THEN ARITH_TAC)
(*--------------------------------------------------------------------------*)
(* Prove the properties of representatives *)
(*--------------------------------------------------------------------------*)
val _ = print "Proving various properties of pairs of naturals\n"
val TINT_10 =
store_thm("TINT_10",
Term `~(tint_1 tint_eq tint_0)`,
REWRITE_TAC[tint_1, tint_0, tint_eq]
THEN ARITH_TAC)
val TINT_ADD_SYM =
store_thm("TINT_ADD_SYM",
Term `!y x. x tint_add y = y tint_add x`,
REPEAT GEN_PAIR_TAC
THEN REWRITE_TAC[tint_eq,tint_add,pairTheory.PAIR_EQ]
THEN ARITH_TAC)
val TINT_MUL_SYM =
store_thm("TINT_MUL_SYM",
Term `!y x. x tint_mul y = y tint_mul x`,
REPEAT GEN_PAIR_TAC
THEN REWRITE_TAC[tint_eq,tint_mul,pairTheory.PAIR_EQ]
THEN SIMP_TAC int_ss [MULT_SYM])
val TINT_ADD_ASSOC =
store_thm
("TINT_ADD_ASSOC",
Term `!z y x. x tint_add (y tint_add z) = (x tint_add y) tint_add z`,
REPEAT GEN_PAIR_TAC
THEN REWRITE_TAC[tint_add,pairTheory.PAIR_EQ,ADD_ASSOC])
val TINT_MUL_ASSOC =
store_thm
("TINT_MUL_ASSOC",
Term `!z y x. x tint_mul (y tint_mul z) = (x tint_mul y) tint_mul z`,
REPEAT GEN_PAIR_TAC
THEN
REWRITE_TAC[tint_mul, pairTheory.PAIR_EQ, LEFT_ADD_DISTRIB,
RIGHT_ADD_DISTRIB]
THEN
SIMP_TAC int_ss [MULT_ASSOC]);
val TINT_LDISTRIB =
store_thm
("TINT_LDISTRIB",
Term `!z y x. x tint_mul (y tint_add z) =
(x tint_mul y) tint_add (x tint_mul z)`,
REPEAT GEN_PAIR_TAC THEN
REWRITE_TAC[tint_mul, tint_add,pairTheory.PAIR_EQ, LEFT_ADD_DISTRIB]
THEN CANCEL_TAC);
val TINT_ADD_LID =
store_thm
("TINT_ADD_LID",
Term `!x. (tint_0 tint_add x) tint_eq x`,
REPEAT GEN_PAIR_TAC
THEN REWRITE_TAC[tint_add,tint_0,tint_eq]
THEN ARITH_TAC);
val TINT_MUL_LID =
store_thm
("TINT_MUL_LID",
Term `!x. (tint_1 tint_mul x) tint_eq x`,
REPEAT GEN_PAIR_TAC
THEN REWRITE_TAC[tint_mul,tint_1,tint_eq]
THEN ARITH_TAC)
val TINT_ADD_LINV =
store_thm
("TINT_ADD_LINV",
Term `!x. ((tint_neg x) tint_add x) tint_eq tint_0`,
REPEAT GEN_PAIR_TAC
THEN REWRITE_TAC[tint_add,tint_0,tint_eq,tint_neg]
THEN ARITH_TAC)
val TINT_LT_TOTAL =
store_thm
("TINT_LT_TOTAL",
Term `!x y. x tint_eq y \/ x tint_lt y \/ y tint_lt x`,
REPEAT GEN_PAIR_TAC
THEN REWRITE_TAC[tint_lt,tint_eq]
THEN ARITH_TAC)
val TINT_LT_REFL =
store_thm("TINT_LT_REFL",
Term `!x. ~(x tint_lt x)`,
REPEAT GEN_PAIR_TAC
THEN REWRITE_TAC[tint_lt]
THEN ARITH_TAC)
fun unfold_dec l = REPEAT GEN_PAIR_TAC THEN REWRITE_TAC l THEN ARITH_TAC;
val TINT_LT_TRANS =
store_thm
("TINT_LT_TRANS",
Term `!x y z. x tint_lt y /\ y tint_lt z ==> x tint_lt z`,
unfold_dec[tint_lt])
val TINT_LT_ADD =
store_thm
("TINT_LT_ADD",
Term `!x y z. (y tint_lt z) ==> (x tint_add y) tint_lt (x tint_add z)`,
unfold_dec[tint_lt,tint_add])
val TINT_LT_MUL =
store_thm
("TINT_LT_MUL",
Term `!x y. tint_0 tint_lt x /\ tint_0 tint_lt y ==>
tint_0 tint_lt (x tint_mul y)`,
REPEAT GEN_PAIR_TAC THEN PURE_REWRITE_TAC[tint_0, tint_lt, tint_mul] THEN
CANCEL_TAC THEN DISCH_THEN(CONJUNCTS_THEN
(CHOOSE_THEN SUBST1_TAC o MATCH_MP LESS_ADD_1))
THEN SIMP_TAC int_ss [LEFT_ADD_DISTRIB, RIGHT_ADD_DISTRIB])
(*--------------------------------------------------------------------------*)
(* Prove that the operations on representatives are well-defined *)
(*--------------------------------------------------------------------------*)
val TINT_NEG_WELLDEF =
store_thm
("TINT_NEG_WELLDEF",
Term `!x1 x2. x1 tint_eq x2 ==> (tint_neg x1) tint_eq (tint_neg x2)`,
unfold_dec[tint_eq,tint_neg])
val TINT_ADD_WELLDEFR =
store_thm
("TINT_ADD_WELLDEFR",
Term`!x1 x2 y. x1 tint_eq x2 ==> (x1 tint_add y) tint_eq (x2 tint_add y)`,
unfold_dec[tint_eq,tint_add])
val TINT_ADD_WELLDEF =
store_thm
("TINT_ADD_WELLDEF",
Term `!x1 x2 y1 y2. x1 tint_eq x2 /\ y1 tint_eq y2 ==>
(x1 tint_add y1) tint_eq (x2 tint_add y2)`,
unfold_dec[tint_eq,tint_add])
val TINT_MUL_WELLDEFR =
store_thm
("TINT_MUL_WELLDEFR",
Term`!x1 x2 y. x1 tint_eq x2 ==> (x1 tint_mul y) tint_eq (x2 tint_mul y)`,
REPEAT GEN_PAIR_TAC THEN PURE_REWRITE_TAC[tint_mul, tint_eq] THEN
ONCE_REWRITE_TAC[jrhUtils.AC(ADD_ASSOC,ADD_SYM)
(Term `(a + b) + (c + d) =
(a + d) + (b + c)`)] THEN
REWRITE_TAC[GSYM RIGHT_ADD_DISTRIB] THEN DISCH_TAC THEN
ASM_REWRITE_TAC[] THEN AP_TERM_TAC THEN
ONCE_REWRITE_TAC[ADD_SYM] THEN POP_ASSUM SUBST1_TAC THEN REFL_TAC);
val TINT_MUL_WELLDEF =
store_thm
("TINT_MUL_WELLDEF",
Term `!x1 x2 y1 y2. x1 tint_eq x2 /\ y1 tint_eq y2 ==>
(x1 tint_mul y1) tint_eq (x2 tint_mul y2)`,
REPEAT GEN_TAC THEN DISCH_TAC THEN
MATCH_MP_TAC TINT_EQ_TRANS THEN EXISTS_TAC (Term `x1 tint_mul y2`) THEN
CONJ_TAC THENL [ONCE_REWRITE_TAC[TINT_MUL_SYM], ALL_TAC] THEN
MATCH_MP_TAC TINT_MUL_WELLDEFR THEN ASM_REWRITE_TAC[]);
val TINT_LT_WELLDEFR =
store_thm
("TINT_LT_WELLDEFR",
Term `!x1 x2 y. x1 tint_eq x2 ==> (x1 tint_lt y <=> x2 tint_lt y)`,
unfold_dec[tint_eq,tint_lt])
val TINT_LT_WELLDEFL =
store_thm
("TINT_LT_WELLDEFL",
Term `!x y1 y2. y1 tint_eq y2 ==> (x tint_lt y1 <=> x tint_lt y2)`,
unfold_dec[tint_eq,tint_lt])
val TINT_LT_WELLDEF =
store_thm
("TINT_LT_WELLDEF",
Term `!x1 x2 y1 y2. x1 tint_eq x2 /\ y1 tint_eq y2 ==>
(x1 tint_lt y1 <=> x2 tint_lt y2)`,
unfold_dec[tint_eq,tint_lt]);
(*--------------------------------------------------------------------------*)
(* Now define the inclusion homomorphism tint_of_num:num->tint. *)
(*--------------------------------------------------------------------------*)
val tint_of_num =
new_recursive_definition
{name = "tint_of_num",
rec_axiom = prim_recTheory.num_Axiom,
def = Term `(tint_of_num 0 = tint_0) /\
(tint_of_num (SUC n) = (tint_of_num n) tint_add tint_1)`};
(* Could do the following if wished:
val _ = add_numeral_form(#"t", SOME "tint_of_num");
*)
val tint_of_num_PAIR =
GEN_ALL (SYM (ISPEC(Term `tint_of_num n`) (pairTheory.PAIR)));
val tint_of_num_eq =
store_thm("tint_of_num_eq",
Term `!n. FST (tint_of_num n) = SND (tint_of_num n) + n`,
INDUCT_TAC
THENL
[ SIMP_TAC int_ss [tint_of_num,tint_0],
REWRITE_TAC [tint_of_num]
THEN ONCE_REWRITE_TAC [tint_of_num_PAIR]
THEN ASM_REWRITE_TAC [tint_1,tint_add]
THEN SIMP_TAC int_ss []
])
val TINT_INJ =
store_thm("TINT_INJ",
Term `!m n. (tint_of_num m tint_eq tint_of_num n) = (m = n)`,
INDUCT_TAC THEN INDUCT_TAC
THEN REPEAT (POP_ASSUM MP_TAC)
THEN REWRITE_TAC [tint_of_num]
THEN ONCE_REWRITE_TAC [tint_of_num_PAIR]
THEN REWRITE_TAC [tint_0,tint_1,tint_add,tint_eq,tint_of_num_eq]
THEN SIMP_TAC int_ss [])
val NUM_POSTINT_EX =
store_thm("NUM_POSTINT_EX",
Term `!t. ~(t tint_lt tint_0) ==> ?n. t tint_eq tint_of_num n`,
GEN_TAC THEN DISCH_TAC THEN
Q.EXISTS_TAC `FST t - SND t`
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC [GSYM pairTheory.PAIR]
THEN REWRITE_TAC [tint_0,tint_lt,tint_eq,tint_of_num_eq]
THEN SIMP_TAC int_ss []);
(*--------------------------------------------------------------------------*)
(* Now define the functions over the equivalence classes *)
(*--------------------------------------------------------------------------*)
val _ = print "Establish type of integers\n";
local
fun mk_def (d,t,n) = {def_name=d, fixity=NONE, fname=n, func=t}
in
val [INT_10, INT_ADD_SYM, INT_MUL_SYM,
INT_ADD_ASSOC, INT_MUL_ASSOC, INT_LDISTRIB,
INT_ADD_LID, INT_MUL_LID, INT_ADD_LINV,
INT_LT_TOTAL, INT_LT_REFL, INT_LT_TRANS,
INT_LT_LADD_IMP, INT_LT_MUL,
int_of_num, INT_INJ, NUM_POSINT_EX] =
define_equivalence_type
{name = "int", equiv = TINT_EQ_EQUIV,
defs = [mk_def ("int_0" , “tint_0”, "int_0"),
mk_def ("int_1" , “tint_1”, "int_1"),
mk_def ("int_neg" , “tint_neg”, "int_neg"),
mk_def ("int_add" , “$tint_add”, "int_add"),
mk_def ("int_mul" , “$tint_mul”, "int_mul"),
mk_def ("int_lt" , “$tint_lt”, "int_lt"),
mk_def ("int_of_num" , “tint_of_num”, "int_of_num")],
welldefs = [TINT_NEG_WELLDEF, TINT_LT_WELLDEF,
TINT_ADD_WELLDEF, TINT_MUL_WELLDEF],
old_thms = ([TINT_10, TINT_ADD_SYM, TINT_MUL_SYM, TINT_ADD_ASSOC,
TINT_MUL_ASSOC, TINT_LDISTRIB,
TINT_ADD_LID, TINT_MUL_LID, TINT_ADD_LINV,
TINT_LT_TOTAL, TINT_LT_REFL, TINT_LT_TRANS,
TINT_LT_ADD, TINT_LT_MUL, tint_of_num,
TINT_INJ, NUM_POSTINT_EX])}
end;
val _ = Theory.save_thm ("INT_10",INT_10)
val _ = Theory.save_thm ("INT_ADD_SYM",INT_ADD_SYM)
val INT_ADD_COMM = Theory.save_thm("INT_ADD_COMM", INT_ADD_SYM);
val _ = Theory.save_thm ("INT_MUL_SYM",INT_MUL_SYM)
val INT_MUL_COMM = Theory.save_thm("INT_MUL_COMM", INT_MUL_SYM);
val _ = Theory.save_thm ("INT_ADD_ASSOC",INT_ADD_ASSOC)
val _ = Theory.save_thm ("INT_MUL_ASSOC",INT_MUL_ASSOC)
val _ = Theory.save_thm ("INT_LDISTRIB",INT_LDISTRIB)
val _ = Theory.save_thm ("INT_LT_TOTAL",INT_LT_TOTAL)
val _ = Theory.save_thm ("INT_LT_REFL",INT_LT_REFL)
val _ = Theory.save_thm ("INT_LT_TRANS",INT_LT_TRANS)
val _ = Theory.save_thm ("INT_LT_LADD_IMP",INT_LT_LADD_IMP)
val _ = Theory.save_thm ("INT_LT_MUL",INT_LT_MUL)
val _ = Theory.save_thm ("int_of_num",int_of_num)
val _ = Theory.save_thm ("INT_INJ",INT_INJ)
val _ = Theory.save_thm ("NUM_POSINT_EX",NUM_POSINT_EX)
;
val _ = overload_on ("+", Term`int_add`);
val _ = overload_on ("<", Term`int_lt`);
val _ = overload_on ("*", Term`int_mul`);
(* this is a slightly tricky case; we don't have to call overload_on
on the boolean negation, but we're doing so to put it back at the
top of the list of possible resolutions.
Also need to overload from the Unicode negation in order to make that
preferred over the tilde.
*)
val bool_not = “$~ : bool -> bool”
Overload "~" = “int_neg”
Overload "~" = bool_not
Overload numeric_negate = “int_neg”
Overload "¬" = bool_not (* UOK *)
(*--------------------------------------------------------------------------*)
(* Define subtraction and the other orderings *)
(*--------------------------------------------------------------------------*)
val int_sub =
new_infixl_definition("int_sub",
Term `$int_sub x y = x + ~y`,
500);
val _ = overload_on ("-", Term`$int_sub`);
val int_le = new_definition("int_le", Term `int_le x y = ~(y<x:int)`);
val _ = overload_on ("<=", Term`$int_le`);
val int_gt = new_definition("int_gt", Term `int_gt (x:int) y <=> y < x`);
val _ = overload_on (">", Term`$int_gt`);
val int_ge = new_definition("int_ge", Term `int_ge x y <=> y <= x:int`)
val _ = overload_on (">=", Term`$int_ge`);
(*--------------------------------------------------------------------------*)
(* Now use the lifted inclusion homomorphism int_of_num:num->int. *)
(*--------------------------------------------------------------------------*)
val _ = add_numeral_form(#"i", SOME "int_of_num");
val INT_0 =
store_thm("INT_0",
Term `int_0 = 0i`,
REWRITE_TAC[int_of_num]);
val INT_1 =
store_thm("INT_1",
Term `int_1 = 1i`,
REWRITE_TAC[ONE, int_of_num, INT_ADD_LID]);
(*--------------------------------------------------------------------------*)
(* Prove lots of boring ring theorems *)
(*--------------------------------------------------------------------------*)
val _ = print "Prove \"lots of boring ring theorems\"\n";
(* already defined, but using the wrong term for 0 *)
val INT_ADD_LID =
store_thm("INT_ADD_LID",
Term`!x:int. 0 + x = x`,
SIMP_TAC int_ss [GSYM INT_0, INT_ADD_LID]);
val _ = export_rewrites ["INT_ADD_LID"]
val INT_ADD_RID =
store_thm("INT_ADD_RID",
Term `!x:int. x + 0 = x`,
PROVE_TAC [INT_ADD_COMM,INT_ADD_LID])
val _ = export_rewrites ["INT_ADD_RID"]
(* already defined, but using the wrong term for 0 *)
Theorem INT_ADD_LINV[simp]: !x. ~x + x = 0
Proof SIMP_TAC int_ss [GSYM INT_0, INT_ADD_LINV]
QED
Theorem INT_ADD_RINV[simp]:
!x. x + ~x = 0
Proof
ONCE_REWRITE_TAC [INT_ADD_SYM] THEN REWRITE_TAC [INT_ADD_LINV]
QED
(* already defined, but using the wrong term for 1 *)
Theorem INT_MUL_LID[simp]: !x:int. 1 * x = x
Proof
SIMP_TAC int_ss [GSYM INT_1, INT_MUL_LID]
QED
Theorem INT_MUL_RID[simp]: !x:int. x * 1 = x
Proof PROVE_TAC [INT_MUL_SYM,GSYM INT_1,INT_MUL_LID]
QED
val INT_RDISTRIB =
store_thm("INT_RDISTRIB",
Term `!(x:int) y z. (x + y) * z = (x * z) + (y * z)`,
ONCE_REWRITE_TAC [INT_MUL_COMM] THEN
REWRITE_TAC [INT_LDISTRIB])
val INT_EQ_LADD =
store_thm("INT_EQ_LADD",
Term `!(x:int) y z. (x + y = x + z) = (y = z)`,
REPEAT GEN_TAC THEN EQ_TAC THENL
[DISCH_THEN(MP_TAC o AP_TERM (Term `$+ ~x`)), ALL_TAC] THEN
SIMP_TAC int_ss [INT_ADD_ASSOC, INT_ADD_LINV, INT_ADD_LID])
val INT_EQ_RADD =
store_thm("INT_EQ_RADD",
Term `!x:int y z. (x + z = y + z) = (x = y)`,
REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[INT_ADD_SYM] THEN
SIMP_TAC int_ss [INT_EQ_LADD]);
val INT_ADD_LID_UNIQ =
store_thm("INT_ADD_LID_UNIQ",
Term `!x:int y. (x + y = y) = (x = 0)`,
REPEAT GEN_TAC THEN
GEN_REWRITE_TAC (LAND_CONV o RAND_CONV)
empty_rewrites [GSYM INT_ADD_LID]
THEN SIMP_TAC int_ss [INT_EQ_RADD])
val INT_ADD_RID_UNIQ =
store_thm("INT_ADD_RID_UNIQ",
Term `!x:int y. (x + y = x) = (y = 0)`,
REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[INT_ADD_SYM] THEN
SIMP_TAC int_ss [INT_ADD_LID_UNIQ])
val INT_LNEG_UNIQ =
store_thm
("INT_LNEG_UNIQ",
Term `!x y. (x + y = 0) = (x = ~y)`,
REPEAT GEN_TAC
THEN SUBST1_TAC (SYM(SPEC (Term `y:int`) INT_ADD_LINV))
THEN SIMP_TAC int_ss [INT_EQ_RADD]);
val INT_RNEG_UNIQ =
store_thm("INT_RNEG_UNIQ",
Term `!x y. (x + y = 0) = (y = ~x)`,
REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[INT_ADD_SYM] THEN
SIMP_TAC int_ss [INT_LNEG_UNIQ])
val INT_NEG_ADD =
store_thm("INT_NEG_ADD",
Term `!x y. ~(x + y) = ~x + ~y`,
REPEAT GEN_TAC THEN CONV_TAC SYM_CONV THEN
REWRITE_TAC[GSYM INT_LNEG_UNIQ] THEN
ONCE_REWRITE_TAC
[jrhUtils.AC(INT_ADD_ASSOC,INT_ADD_SYM)
(Term `(a + b) + (c + d) = (a + c) + (b + d:int)`)] THEN
REWRITE_TAC[INT_ADD_LINV, INT_ADD_RID,INT_0]);
val INT_MUL_LZERO =
store_thm("INT_MUL_LZERO",
Term `!x:int. 0 * x = 0`,
GEN_TAC THEN SUBST1_TAC
(SYM(Q.SPECL [`0 * x`, `0 * x`] INT_ADD_LID_UNIQ))
THEN REWRITE_TAC[GSYM INT_RDISTRIB, INT_ADD_RID]);
val _ = export_rewrites ["INT_MUL_LZERO"]
val INT_MUL_RZERO
= store_thm("INT_MUL_RZERO",
Term `!x. x * 0i = 0`,
GEN_TAC THEN ONCE_REWRITE_TAC[INT_MUL_SYM] THEN
SIMP_TAC int_ss [INT_MUL_LZERO]);
val _ = export_rewrites ["INT_MUL_RZERO"]
val INT_NEG_LMUL =
store_thm("INT_NEG_LMUL",
Term `!x y. ~(x * y) = ~x * y`,
REPEAT GEN_TAC THEN CONV_TAC SYM_CONV THEN
REWRITE_TAC[GSYM INT_LNEG_UNIQ, GSYM INT_RDISTRIB,
INT_ADD_LINV, INT_MUL_LZERO,INT_0]);
val INT_NEG_RMUL =
store_thm("INT_NEG_RMUL",
Term `!x y. ~(x * y) = x * ~y`,
REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[INT_MUL_SYM] THEN
SIMP_TAC int_ss [INT_NEG_LMUL]);
Theorem INT_NEGNEG[simp]:
!x:int. ~~x = x
Proof
GEN_TAC THEN CONV_TAC SYM_CONV THEN
REWRITE_TAC[GSYM INT_LNEG_UNIQ, INT_ADD_RINV]
QED
val INT_NEG_MUL2 =
store_thm("INT_NEG_MUL2",
Term `!x y. ~x * ~y = x * y`,
REWRITE_TAC[GSYM INT_NEG_LMUL, GSYM INT_NEG_RMUL, INT_NEGNEG]);
val INT_LT_LADD =
store_thm("INT_LT_LADD",
Term `!x:int y z. x + y < x + z <=> y < z`,
REPEAT GEN_TAC THEN EQ_TAC THENL
[DISCH_THEN(MP_TAC o (SPEC (Term `~x:int`)) o
MATCH_MP INT_LT_LADD_IMP)
THEN
REWRITE_TAC[INT_ADD_ASSOC, INT_ADD_LINV, INT_ADD_LID],
SIMP_TAC int_ss [INT_LT_LADD_IMP]]);
Theorem INT_LT_RADD:
!x:int y z. (x + z) < (y + z) <=> x < y
Proof
REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[INT_ADD_SYM] THEN
SIMP_TAC int_ss [INT_LT_LADD]
QED
Theorem INT_NOT_LT:
!x:int y. ~(x < y) <=> y <= x
Proof
REPEAT GEN_TAC THEN REWRITE_TAC[int_le]
QED
val INT_LT_ANTISYM =
store_thm("INT_LT_ANTISYM",
Term `!x:int y. ~(x < y /\ y < x)`,
REPEAT GEN_TAC THEN DISCH_THEN(MP_TAC o MATCH_MP INT_LT_TRANS)
THEN REWRITE_TAC[INT_LT_REFL]);
val INT_LT_GT =
store_thm("INT_LT_GT",
Term `!x:int y. x < y ==> ~(y < x)`,
REPEAT GEN_TAC THEN
DISCH_THEN(fn th => DISCH_THEN(MP_TAC o CONJ th)) THEN
REWRITE_TAC[INT_LT_ANTISYM]);
Theorem INT_NOT_LE:
!x y:int. ~(x <= y) <=> y < x
Proof
REPEAT GEN_TAC THEN REWRITE_TAC[int_le]
QED
val INT_LE_TOTAL =
store_thm("INT_LE_TOTAL",
Term `!x y:int. x <= y \/ y <= x`,
REPEAT GEN_TAC THEN
REWRITE_TAC[int_le, GSYM DE_MORGAN_THM, INT_LT_ANTISYM]);
val INT_LET_TOTAL =
store_thm("INT_LET_TOTAL",
Term `!x y:int. x <= y \/ y < x`,
REPEAT GEN_TAC THEN REWRITE_TAC[int_le] THEN
SIMP_TAC int_ss []);
val INT_LTE_TOTAL =
store_thm("INT_LTE_TOTAL",
Term `!x y:int. x < y \/ y <= x`,
REPEAT GEN_TAC THEN REWRITE_TAC[int_le] THEN
SIMP_TAC int_ss [])
Theorem INT_LE_REFL[simp]: !x:int. x <= x
Proof GEN_TAC THEN REWRITE_TAC[int_le, INT_LT_REFL]
QED
Theorem INT_LE_LT:
!x y:int. x <= y <=> x < y \/ (x = y)
Proof
REPEAT GEN_TAC THEN REWRITE_TAC[int_le] THEN EQ_TAC THENL
[REPEAT_TCL DISJ_CASES_THEN ASSUME_TAC
(SPECL [Term `x:int`, Term `y:int`] INT_LT_TOTAL) THEN ASM_REWRITE_TAC[],
DISCH_THEN(DISJ_CASES_THEN2
(curry(op THEN) (MATCH_MP_TAC INT_LT_GT) o ACCEPT_TAC) SUBST1_TAC) THEN
MATCH_ACCEPT_TAC INT_LT_REFL]
QED
Theorem INT_LT_LE:
!x y:int. x < y <=> x <= y /\ ~(x = y)
Proof
let val lemma = TAUT_CONV (Term `~(a /\ ~a)`)
in
REPEAT GEN_TAC THEN REWRITE_TAC[INT_LE_LT, RIGHT_AND_OVER_OR, lemma]
THEN EQ_TAC THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN
POP_ASSUM MP_TAC THEN CONV_TAC CONTRAPOS_CONV THEN REWRITE_TAC[] THEN
DISCH_THEN SUBST1_TAC THEN REWRITE_TAC[INT_LT_REFL]
end
QED
val INT_LT_IMP_LE =
store_thm("INT_LT_IMP_LE",
Term `!x y:int. x < y ==> x <= y`,
REPEAT GEN_TAC THEN DISCH_TAC THEN
ASM_REWRITE_TAC[INT_LE_LT]);
val INT_LTE_TRANS =
store_thm("INT_LTE_TRANS",
Term `!x y z:int. x < y /\ y <= z ==> x < z`,
REPEAT GEN_TAC THEN REWRITE_TAC[INT_LE_LT, LEFT_AND_OVER_OR] THEN
DISCH_THEN(DISJ_CASES_THEN2 (ACCEPT_TAC o MATCH_MP INT_LT_TRANS)
(CONJUNCTS_THEN2 MP_TAC SUBST1_TAC))
THEN REWRITE_TAC[]);
val INT_LET_TRANS =
store_thm("INT_LET_TRANS",
Term `!x y z:int. x <= y /\ y < z ==> x < z`,
REPEAT GEN_TAC THEN REWRITE_TAC[INT_LE_LT, RIGHT_AND_OVER_OR]
THEN
DISCH_THEN(DISJ_CASES_THEN2 (ACCEPT_TAC o MATCH_MP INT_LT_TRANS)
(CONJUNCTS_THEN2 SUBST1_TAC ACCEPT_TAC)));
val INT_LE_TRANS =
store_thm("INT_LE_TRANS",
Term `!x y z:int. x <= y /\ y <= z ==> x <= z`,
REPEAT GEN_TAC THEN
GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) empty_rewrites
[INT_LE_LT] THEN
DISCH_THEN(CONJUNCTS_THEN2 MP_TAC
(DISJ_CASES_THEN2 ASSUME_TAC SUBST1_TAC))
THEN REWRITE_TAC[]
THEN DISCH_THEN(MP_TAC o C CONJ (ASSUME (Term `y < z:int`))) THEN
DISCH_THEN(ACCEPT_TAC o MATCH_MP
INT_LT_IMP_LE o MATCH_MP INT_LET_TRANS));
Theorem INT_LE_ANTISYM:
!x y:int. x <= y /\ y <= x <=> (x = y)
Proof
REPEAT GEN_TAC THEN EQ_TAC THENL
[REWRITE_TAC[int_le] THEN REPEAT_TCL DISJ_CASES_THEN ASSUME_TAC
(SPECL [Term `x:int`, Term `y:int`] INT_LT_TOTAL) THEN
ASM_REWRITE_TAC[],
DISCH_THEN SUBST1_TAC THEN REWRITE_TAC[INT_LE_REFL]]
QED
val INT_LET_ANTISYM =
store_thm("INT_LET_ANTISYM",
Term `!x y:int. ~(x < y /\ y <= x)`,
REPEAT GEN_TAC THEN REWRITE_TAC[int_le] THEN
BOOL_CASES_TAC (Term `x < y:int`) THEN REWRITE_TAC[]);
val INT_LTE_ANTSYM =
store_thm("INT_LTE_ANTSYM",
Term `!x y:int. ~(x <= y /\ y < x)`,
REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[CONJ_SYM] THEN
MATCH_ACCEPT_TAC INT_LET_ANTISYM);
Theorem INT_NEG_LT0:
!x. ~x < 0 <=> 0 < x
Proof
GEN_TAC THEN
SUBST1_TAC(SYM(Q.SPECL [`~x`, `0`,`x`] INT_LT_RADD)) THEN
REWRITE_TAC[INT_ADD_LINV, INT_ADD_LID]
QED
Theorem INT_NEG_GT0:
!x. 0 < ~x <=> x < 0
Proof GEN_TAC THEN REWRITE_TAC[GSYM INT_NEG_LT0, INT_NEGNEG]
QED
Theorem INT_NEG_LE0:
!x. ~x <= 0 <=> 0 <= x
Proof GEN_TAC THEN REWRITE_TAC[int_le] THEN
REWRITE_TAC[INT_NEG_GT0]
QED
Theorem INT_NEG_GE0:
!x. 0 <= ~x <=> x <= 0
Proof
GEN_TAC THEN REWRITE_TAC[int_le] THEN
REWRITE_TAC[INT_NEG_LT0]
QED
Theorem INT_LT_NEGTOTAL:
!x. (x = 0) \/ 0<x \/ 0 < ~x
Proof
GEN_TAC THEN REPEAT_TCL DISJ_CASES_THEN ASSUME_TAC
(Q.SPECL [`x`, `0`] INT_LT_TOTAL) THEN
ASM_REWRITE_TAC
[SYM(REWRITE_RULE[INT_NEGNEG] (Q.SPEC `~x` INT_NEG_LT0))]
QED
val INT_LE_NEGTOTAL =
store_thm
("INT_LE_NEGTOTAL",
Term `!x. 0 <= x \/ 0 <= ~x`,
GEN_TAC THEN REWRITE_TAC[INT_LE_LT] THEN
REPEAT_TCL DISJ_CASES_THEN ASSUME_TAC (SPEC (Term `x:int`)
INT_LT_NEGTOTAL)
THEN ASM_REWRITE_TAC[]);
val INT_LE_MUL =
store_thm
("INT_LE_MUL",
Term `!x y:int. 0 <= x /\ 0 <= y ==> 0 <= x*y`,
REPEAT GEN_TAC THEN REWRITE_TAC[INT_LE_LT] THEN
MAP_EVERY ASM_CASES_TAC [Term `0i = x`, Term `0i = y`] THEN
ASM_REWRITE_TAC[] THEN TRY(FIRST_ASSUM(SUBST1_TAC o SYM)) THEN
REWRITE_TAC[INT_MUL_LZERO, INT_MUL_RZERO] THEN
DISCH_TAC THEN DISJ1_TAC
THEN MATCH_MP_TAC (REWRITE_RULE [INT_0] INT_LT_MUL) THEN
ASM_REWRITE_TAC[]);
val INT_LE_SQUARE =
store_thm("INT_LE_SQUARE",
Term `!x:int. 0 <= x * x`,
GEN_TAC THEN DISJ_CASES_TAC (SPEC (Term `x:int`) INT_LE_NEGTOTAL)
THEN
POP_ASSUM(MP_TAC o MATCH_MP INT_LE_MUL o W CONJ) THEN
REWRITE_TAC[GSYM INT_NEG_RMUL, GSYM INT_NEG_LMUL, INT_NEGNEG]);
val INT_LE_01 =
store_thm("INT_LE_01",
Term `0i <= 1`,
SUBST1_TAC(SYM(Q.SPEC `1` INT_MUL_LID)) THEN
SIMP_TAC int_ss [INT_LE_SQUARE,INT_1]);
val INT_LT_01 =
store_thm("INT_LT_01",
Term `0i < 1i`,
SIMP_TAC int_ss [INT_LT_LE, INT_LE_01,
GSYM INT_0,GSYM INT_1,INT_10])
Theorem INT_LE_LADD:
!x:int y z. x + y <= x + z <=> y <= z
Proof
REPEAT GEN_TAC THEN REWRITE_TAC[int_le] THEN
AP_TERM_TAC THEN MATCH_ACCEPT_TAC INT_LT_LADD
QED
Theorem INT_LE_RADD:
!x y z:int. (x + z) <= (y + z) <=> x <= y
Proof
REPEAT GEN_TAC THEN REWRITE_TAC[int_le] THEN
AP_TERM_TAC THEN MATCH_ACCEPT_TAC INT_LT_RADD
QED
val INT_LT_ADD2 =
store_thm("INT_LT_ADD2",
Term `!w x y z:int. w < x /\ y < z ==> w + y < x + z`,
REPEAT GEN_TAC THEN DISCH_TAC THEN
MATCH_MP_TAC INT_LT_TRANS THEN EXISTS_TAC (Term `w + z:int`) THEN
ASM_REWRITE_TAC[INT_LT_LADD, INT_LT_RADD]);
val INT_LE_ADD2 =
store_thm("INT_LE_ADD2",
Term `!w x y z:int. w <= x /\ y <= z ==> w + y <= x + z`,
REPEAT GEN_TAC THEN DISCH_TAC THEN
MATCH_MP_TAC INT_LE_TRANS THEN EXISTS_TAC (Term `w + z:int`) THEN
ASM_REWRITE_TAC[INT_LE_LADD, INT_LE_RADD]);
val INT_LE_ADD =
store_thm("INT_LE_ADD",
Term `!x y:int. 0 <= x /\ 0 <= y ==> 0 <= (x + y)`,
REPEAT GEN_TAC
THEN DISCH_THEN(MP_TAC o MATCH_MP INT_LE_ADD2) THEN
REWRITE_TAC[INT_ADD_LID]);
val INT_LT_ADD =
store_thm("INT_LT_ADD",
Term `!x y:int. 0 < x /\ 0 < y ==> 0 < (x + y)`,
REPEAT GEN_TAC THEN DISCH_THEN(MP_TAC o MATCH_MP INT_LT_ADD2)
THEN
REWRITE_TAC[INT_ADD_LID]);
Theorem INT_LT_ADDNEG:
!x y z. y < x + ~z <=> y+z < x
Proof
REPEAT GEN_TAC THEN
SUBST1_TAC(SYM(SPECL [Term `y:int`,
Term `x + ~z`,
Term `z:int`] INT_LT_RADD)) THEN
REWRITE_TAC[GSYM INT_ADD_ASSOC, INT_ADD_LINV,
INT_ADD_RID, INT_0]
QED
(* REWRITE TO *)
Theorem INT_LT_ADDNEG2:
!x y z. x + ~y < z <=> x < z+y
Proof
REPEAT GEN_TAC THEN
SUBST1_TAC
(SYM(SPECL [Term `x + ~y`, Term `z:int`,Term `y:int`] INT_LT_RADD)) THEN
REWRITE_TAC[GSYM INT_ADD_ASSOC, INT_ADD_LINV, INT_ADD_RID,INT_0]
QED
val INT_LT_ADD1 =
store_thm("INT_LT_ADD1",
Term `!x y:int. x <= y ==> x < (y + 1)`,
REPEAT GEN_TAC THEN REWRITE_TAC[INT_LE_LT] THEN
DISCH_THEN DISJ_CASES_TAC THENL
[POP_ASSUM(MP_TAC o MATCH_MP INT_LT_ADD2 o C CONJ INT_LT_01)