integerScript.sml
1(*==========================================================================*)
2(* Theory of integers. (John Harrison) *)
3(* *)
4(* The integers are constructed as equivalence classes of pairs of integers *)
5(* using the quotient type procedure. *)
6(* *)
7(* This theory was constructed for use in the HOL-ELLA system, using many of*)
8(* the principles, and some of the code, used in the reals library. It is my*)
9(* eventual intention to produce a more unified library of number systems. *)
10(* *)
11(* October/November 1999. *)
12(* Extensions by Michael Norrish to define exponentiation, division and *)
13(* modulus. *)
14(* *)
15(*==========================================================================*)
16Theory integer
17Ancestors
18 arithmetic pred_set prim_rec num divides normalizer
19Libs
20 jrhUtils quotient liteLib simpLib numLib liteLib metisLib
21 BasicProvers hurdUtils boolSimps
22
23
24
25val _ = temp_delsimps ["NORMEQ_CONV"]
26
27val int_ss = boolSimps.bool_ss ++ numSimps.old_ARITH_ss ++ pairSimps.PAIR_ss;
28
29(*---------------------------------------------------------------------------*)
30(* Following incantation needed since pairLib is now loaded, and that adds *)
31(* pairTheory.pair_rws to the implicit set of rewrites for REWRITE_TAC. *)
32(* Usually that is good, but for some of the proofs below, that makes things *)
33(* worse. *)
34(*---------------------------------------------------------------------------*)
35
36val _ = Rewrite.set_implicit_rewrites Rewrite.bool_rewrites;
37
38(*--------------------------------------------------------------------------*)
39(* Required lemmas about the natural numbers - mostly to drive CANCEL_TAC *)
40(*--------------------------------------------------------------------------*)
41
42Theorem EQ_LADD:
43 !x y z. (x + y = x + z) = (y = z)
44Proof
45 ARITH_TAC
46QED
47
48
49Theorem EQ_ADDL:
50 !x y. (x = x + y) = (y = 0)
51Proof
52 ARITH_TAC
53QED
54
55Theorem LT_LADD:
56 !x y z. (x + y) < (x + z) <=> y < z
57Proof
58 ARITH_TAC
59QED
60
61Theorem LT_ADDL:
62 !x y. x < (x + y) <=> 0 < y
63Proof
64 ARITH_TAC
65QED
66
67Theorem LT_ADDR:
68 !x y. ~((x + y) < x)
69Proof
70 ARITH_TAC
71QED
72
73Theorem LT_ADD2:
74 !x1 x2 y1 y2. x1 < y1 /\ x2 < y2 ==> (x1 + x2) < (y1 + y2)
75Proof
76 ARITH_TAC
77QED
78
79(*--------------------------------------------------------------------------*)
80(* CANCEL_CONV - Try to cancel, rearranging using AC laws as needed *)
81(* *)
82(* The first two arguments are the associative and commutative laws, as *)
83(* given to AC_CONV. The remaining list of theorems should be of the form: *)
84(* *)
85(* |- (a & b ~ a & c) = w (e.g. b ~ c) *)
86(* |- (a & b ~ a) = x (e.g. F) *)
87(* |- (a ~ a & c) = y (e.g. T) *)
88(* |- (a ~ a) = z (e.g. F) *)
89(* *)
90(* For some operator (written as infix &) and relation (~). *)
91(* *)
92(* Theorems may be of the form |- ~ P or |- P, rather than equations, they *)
93(* will be transformed to |- P = F and |- P = T automatically if needed. *)
94(* *)
95(* Note that terms not cancelled will remain in their original order, but *)
96(* will be flattened to right-associated form. *)
97(*--------------------------------------------------------------------------*)
98
99fun CANCEL_CONV (assoc,sym,lcancelthms) tm =
100 let fun pair_from_list [x, y] = (x, y)
101 | pair_from_list _ = raise Match
102 val lcthms =
103 map ((fn th => (assert (is_eq o concl)) th
104 handle _ => EQF_INTRO th
105 handle _ => EQT_INTRO th) o SPEC_ALL) lcancelthms
106 val (eqop, binop) = pair_from_list (map
107 (rator o rator o lhs o snd o strip_forall o concl) [hd lcthms, sym])
108 fun strip_binop tm =
109 if (rator(rator tm) ~~ binop handle _ => false) then
110 (strip_binop (rand(rator tm))) @ (strip_binop(rand tm))
111 else [tm]
112 val mk_binop = ((curry mk_comb) o (curry mk_comb binop))
113 val list_mk_binop = end_itlist mk_binop
114
115 fun rmel i list = op_set_diff aconv list [i]
116
117 val (_, (l1, r1)) =
118 (assert (aconv eqop) ## pair_from_list) (strip_comb tm)
119 val (l, r) = pair_from_list (map strip_binop [l1, r1])
120 val i = op_intersect aconv l r
121 in
122 if null i then raise Fail ""
123 else
124 let val itm = list_mk_binop i
125 val (l', r') = pair_from_list
126 (map (end_itlist (C (curry op o)) (map rmel i)) [l, r])
127 val (l2, r2) = pair_from_list
128 (map (fn ts => mk_binop itm (list_mk_binop ts)
129 handle _ => itm) [l',r'])
130 val (le, re) = pair_from_list
131 (map (EQT_ELIM o AC_CONV(assoc,sym) o mk_eq)[(l1,l2),(r1,r2)])
132 val eqv = MK_COMB(AP_TERM eqop le,re)
133 in
134 CONV_RULE(RAND_CONV(end_itlist (curry(op ORELSEC))
135 (map REWR_CONV lcthms))) eqv
136 end
137 end handle _ => failwith "CANCEL_CONV";
138
139
140
141(*--------------------------------------------------------------------------*)
142(* Tactic to do all the obvious simplifications via cancellation etc. *)
143(*--------------------------------------------------------------------------*)
144
145val CANCEL_TAC =
146 (C (curry (op THEN)) (REWRITE_TAC []) o
147 CONV_TAC o ONCE_DEPTH_CONV o end_itlist (curry (op ORELSEC)))
148 (map CANCEL_CONV [(ADD_ASSOC,ADD_SYM,
149 [EQ_LADD, EQ_ADDL, ADD_INV_0_EQ, EQ_SYM_EQ]),
150 (ADD_ASSOC,ADD_SYM,
151 [LT_LADD, LT_ADDL, LT_ADDR, LESS_REFL])]);
152
153(*--------------------------------------------------------------------------*)
154(* Define operations on representatives. *)
155(*--------------------------------------------------------------------------*)
156
157val _ = print "Defining operations on pairs of naturals\n"
158
159Definition tint_0[nocompute]:
160 tint_0 = (1,1)
161End
162
163Definition tint_1[nocompute]:
164 tint_1 = (1 + 1,1)
165End
166
167Definition tint_neg[nocompute]:
168 tint_neg (x:num,(y:num)) = (y,x)
169End
170
171val tint_add =
172 new_infixl_definition
173 ("tint_add",
174 Term`$tint_add (x1,y1) (x2,y2) = (x1 + x2, y1 + y2)`,
175 500);
176
177val tint_mul =
178 new_infixl_definition
179 ("tint_mul",
180 Term `$tint_mul (x1,y1) (x2,y2) = ((x1 * x2) + (y1 * y2),
181 (x1 * y2) + (y1 * x2))`,
182 600);
183
184Definition tint_lt[nocompute]:
185 $tint_lt (x1,y1) (x2,y2) <=> (x1 + y2) < (x2 + y1)
186End
187val _ = temp_set_fixity "tint_lt" (Infix(NONASSOC, 450))
188
189(*--------------------------------------------------------------------------*)
190(* Define the equivalence relation and prove it *is* one *)
191(*--------------------------------------------------------------------------*)
192
193val _ = print "Define equivalence relation over pairs of naturals\n"
194
195Definition tint_eq[nocompute]:
196 $tint_eq (x1,y1) (x2,y2) = (x1 + y2 = x2 + y1)
197End
198val _ = temp_set_fixity "tint_eq" (Infix(NONASSOC, 450));
199
200Theorem TINT_EQ_REFL:
201 !x. x tint_eq x
202Proof
203 GEN_PAIR_TAC THEN REWRITE_TAC[tint_eq]
204QED
205
206Theorem TINT_EQ_SYM:
207 !x y. x tint_eq y <=> y tint_eq x
208Proof
209 REPEAT GEN_PAIR_TAC THEN REWRITE_TAC[tint_eq]
210 THEN ARITH_TAC
211QED
212
213Theorem TINT_EQ_TRANS:
214 !x y z. x tint_eq y /\ y tint_eq z ==> x tint_eq z
215Proof
216 REPEAT GEN_PAIR_TAC THEN REWRITE_TAC[tint_eq]
217 THEN ARITH_TAC
218QED
219
220Theorem TINT_EQ_EQUIV:
221 !p q. p tint_eq q <=> ($tint_eq p = $tint_eq q)
222Proof
223 REPEAT GEN_TAC THEN CONV_TAC SYM_CONV THEN
224 CONV_TAC (ONCE_DEPTH_CONV (X_FUN_EQ_CONV (Term `r:num#num`))) THEN EQ_TAC
225 THENL
226 [DISCH_THEN(MP_TAC o SPEC (Term `q:num#num`)) THEN REWRITE_TAC[TINT_EQ_REFL],
227 DISCH_TAC THEN GEN_TAC THEN EQ_TAC THENL
228 [RULE_ASSUM_TAC(ONCE_REWRITE_RULE[TINT_EQ_SYM]), ALL_TAC] THEN
229 POP_ASSUM(fn th => DISCH_THEN(MP_TAC o CONJ th)) THEN
230 MATCH_ACCEPT_TAC TINT_EQ_TRANS]
231QED
232
233Theorem TINT_EQ_AP:
234 !p q. (p = q) ==> p tint_eq q
235Proof
236 REPEAT GEN_PAIR_TAC
237 THEN REWRITE_TAC[tint_eq,pairTheory.PAIR_EQ]
238 THEN ARITH_TAC
239QED
240
241(*--------------------------------------------------------------------------*)
242(* Prove the properties of representatives *)
243(*--------------------------------------------------------------------------*)
244
245val _ = print "Proving various properties of pairs of naturals\n"
246
247Theorem TINT_10:
248 ~(tint_1 tint_eq tint_0)
249Proof
250 REWRITE_TAC[tint_1, tint_0, tint_eq]
251 THEN ARITH_TAC
252QED
253
254Theorem TINT_ADD_SYM:
255 !y x. x tint_add y = y tint_add x
256Proof
257 REPEAT GEN_PAIR_TAC
258 THEN REWRITE_TAC[tint_eq,tint_add,pairTheory.PAIR_EQ]
259 THEN ARITH_TAC
260QED
261
262Theorem TINT_MUL_SYM:
263 !y x. x tint_mul y = y tint_mul x
264Proof
265 REPEAT GEN_PAIR_TAC
266 THEN REWRITE_TAC[tint_eq,tint_mul,pairTheory.PAIR_EQ]
267 THEN SIMP_TAC int_ss [MULT_SYM]
268QED
269
270Theorem TINT_ADD_ASSOC:
271 !z y x. x tint_add (y tint_add z) = (x tint_add y) tint_add z
272Proof
273 REPEAT GEN_PAIR_TAC
274 THEN REWRITE_TAC[tint_add,pairTheory.PAIR_EQ,ADD_ASSOC]
275QED
276
277Theorem TINT_MUL_ASSOC:
278 !z y x. x tint_mul (y tint_mul z) = (x tint_mul y) tint_mul z
279Proof
280 REPEAT GEN_PAIR_TAC
281 THEN
282 REWRITE_TAC[tint_mul, pairTheory.PAIR_EQ, LEFT_ADD_DISTRIB,
283 RIGHT_ADD_DISTRIB]
284 THEN
285 SIMP_TAC int_ss [MULT_ASSOC]
286QED
287
288Theorem TINT_LDISTRIB:
289 !z y x. x tint_mul (y tint_add z) =
290 (x tint_mul y) tint_add (x tint_mul z)
291Proof
292 REPEAT GEN_PAIR_TAC THEN
293 REWRITE_TAC[tint_mul, tint_add,pairTheory.PAIR_EQ, LEFT_ADD_DISTRIB]
294 THEN CANCEL_TAC
295QED
296
297Theorem TINT_ADD_LID:
298 !x. (tint_0 tint_add x) tint_eq x
299Proof
300 REPEAT GEN_PAIR_TAC
301 THEN REWRITE_TAC[tint_add,tint_0,tint_eq]
302 THEN ARITH_TAC
303QED
304
305Theorem TINT_MUL_LID:
306 !x. (tint_1 tint_mul x) tint_eq x
307Proof
308 REPEAT GEN_PAIR_TAC
309 THEN REWRITE_TAC[tint_mul,tint_1,tint_eq]
310 THEN ARITH_TAC
311QED
312
313Theorem TINT_ADD_LINV:
314 !x. ((tint_neg x) tint_add x) tint_eq tint_0
315Proof
316 REPEAT GEN_PAIR_TAC
317 THEN REWRITE_TAC[tint_add,tint_0,tint_eq,tint_neg]
318 THEN ARITH_TAC
319QED
320
321Theorem TINT_LT_TOTAL:
322 !x y. x tint_eq y \/ x tint_lt y \/ y tint_lt x
323Proof
324 REPEAT GEN_PAIR_TAC
325 THEN REWRITE_TAC[tint_lt,tint_eq]
326 THEN ARITH_TAC
327QED
328
329Theorem TINT_LT_REFL:
330 !x. ~(x tint_lt x)
331Proof
332 REPEAT GEN_PAIR_TAC
333 THEN REWRITE_TAC[tint_lt]
334 THEN ARITH_TAC
335QED
336
337fun unfold_dec l = REPEAT GEN_PAIR_TAC THEN REWRITE_TAC l THEN ARITH_TAC;
338
339Theorem TINT_LT_TRANS:
340 !x y z. x tint_lt y /\ y tint_lt z ==> x tint_lt z
341Proof
342 unfold_dec[tint_lt]
343QED
344
345
346Theorem TINT_LT_ADD:
347 !x y z. (y tint_lt z) ==> (x tint_add y) tint_lt (x tint_add z)
348Proof
349 unfold_dec[tint_lt,tint_add]
350QED
351
352Theorem TINT_LT_MUL:
353 !x y. tint_0 tint_lt x /\ tint_0 tint_lt y ==>
354 tint_0 tint_lt (x tint_mul y)
355Proof
356 REPEAT GEN_PAIR_TAC THEN PURE_REWRITE_TAC[tint_0, tint_lt, tint_mul] THEN
357 CANCEL_TAC THEN DISCH_THEN(CONJUNCTS_THEN
358 (CHOOSE_THEN SUBST1_TAC o MATCH_MP LESS_ADD_1))
359 THEN SIMP_TAC int_ss [LEFT_ADD_DISTRIB, RIGHT_ADD_DISTRIB]
360QED
361
362(*--------------------------------------------------------------------------*)
363(* Prove that the operations on representatives are well-defined *)
364(*--------------------------------------------------------------------------*)
365
366Theorem TINT_NEG_WELLDEF:
367 !x1 x2. x1 tint_eq x2 ==> (tint_neg x1) tint_eq (tint_neg x2)
368Proof
369 unfold_dec[tint_eq,tint_neg]
370QED
371
372Theorem TINT_ADD_WELLDEFR:
373 !x1 x2 y. x1 tint_eq x2 ==> (x1 tint_add y) tint_eq (x2 tint_add y)
374Proof
375 unfold_dec[tint_eq,tint_add]
376QED
377
378Theorem TINT_ADD_WELLDEF:
379 !x1 x2 y1 y2. x1 tint_eq x2 /\ y1 tint_eq y2 ==>
380 (x1 tint_add y1) tint_eq (x2 tint_add y2)
381Proof
382 unfold_dec[tint_eq,tint_add]
383QED
384
385Theorem TINT_MUL_WELLDEFR:
386 !x1 x2 y. x1 tint_eq x2 ==> (x1 tint_mul y) tint_eq (x2 tint_mul y)
387Proof
388 REPEAT GEN_PAIR_TAC THEN PURE_REWRITE_TAC[tint_mul, tint_eq] THEN
389 ONCE_REWRITE_TAC[jrhUtils.AC(ADD_ASSOC,ADD_SYM)
390 (Term `(a + b) + (c + d) =
391 (a + d) + (b + c)`)] THEN
392 REWRITE_TAC[GSYM RIGHT_ADD_DISTRIB] THEN DISCH_TAC THEN
393 ASM_REWRITE_TAC[] THEN AP_TERM_TAC THEN
394 ONCE_REWRITE_TAC[ADD_SYM] THEN POP_ASSUM SUBST1_TAC THEN REFL_TAC
395QED
396
397Theorem TINT_MUL_WELLDEF:
398 !x1 x2 y1 y2. x1 tint_eq x2 /\ y1 tint_eq y2 ==>
399 (x1 tint_mul y1) tint_eq (x2 tint_mul y2)
400Proof
401 REPEAT GEN_TAC THEN DISCH_TAC THEN
402 MATCH_MP_TAC TINT_EQ_TRANS THEN EXISTS_TAC (Term `x1 tint_mul y2`) THEN
403 CONJ_TAC THENL [ONCE_REWRITE_TAC[TINT_MUL_SYM], ALL_TAC] THEN
404 MATCH_MP_TAC TINT_MUL_WELLDEFR THEN ASM_REWRITE_TAC[]
405QED
406
407Theorem TINT_LT_WELLDEFR:
408 !x1 x2 y. x1 tint_eq x2 ==> (x1 tint_lt y <=> x2 tint_lt y)
409Proof
410 unfold_dec[tint_eq,tint_lt]
411QED
412
413Theorem TINT_LT_WELLDEFL:
414 !x y1 y2. y1 tint_eq y2 ==> (x tint_lt y1 <=> x tint_lt y2)
415Proof
416 unfold_dec[tint_eq,tint_lt]
417QED
418
419Theorem TINT_LT_WELLDEF:
420 !x1 x2 y1 y2. x1 tint_eq x2 /\ y1 tint_eq y2 ==>
421 (x1 tint_lt y1 <=> x2 tint_lt y2)
422Proof
423 unfold_dec[tint_eq,tint_lt]
424QED
425
426(*--------------------------------------------------------------------------*)
427(* Now define the inclusion homomorphism tint_of_num:num->tint. *)
428(*--------------------------------------------------------------------------*)
429
430Definition tint_of_num[nocompute]:
431 (tint_of_num 0 = tint_0) /\
432 (tint_of_num (SUC n) = (tint_of_num n) tint_add tint_1)
433End
434
435(* Could do the following if wished:
436val _ = add_numeral_form(#"t", SOME "tint_of_num");
437*)
438
439val tint_of_num_PAIR =
440 GEN_ALL (SYM (ISPEC(Term `tint_of_num n`) (pairTheory.PAIR)));
441
442Theorem tint_of_num_eq:
443 !n. FST (tint_of_num n) = SND (tint_of_num n) + n
444Proof
445 INDUCT_TAC
446 THENL
447 [ SIMP_TAC int_ss [tint_of_num,tint_0],
448
449 REWRITE_TAC [tint_of_num]
450 THEN ONCE_REWRITE_TAC [tint_of_num_PAIR]
451 THEN ASM_REWRITE_TAC [tint_1,tint_add]
452 THEN SIMP_TAC int_ss []
453 ]
454QED
455
456Theorem TINT_INJ:
457 !m n. (tint_of_num m tint_eq tint_of_num n) = (m = n)
458Proof
459 INDUCT_TAC THEN INDUCT_TAC
460 THEN REPEAT (POP_ASSUM MP_TAC)
461 THEN REWRITE_TAC [tint_of_num]
462 THEN ONCE_REWRITE_TAC [tint_of_num_PAIR]
463 THEN REWRITE_TAC [tint_0,tint_1,tint_add,tint_eq,tint_of_num_eq]
464 THEN SIMP_TAC int_ss []
465QED
466
467Theorem NUM_POSTINT_EX:
468 !t. ~(t tint_lt tint_0) ==> ?n. t tint_eq tint_of_num n
469Proof
470 GEN_TAC THEN DISCH_TAC THEN
471 Q.EXISTS_TAC `FST t - SND t`
472 THEN POP_ASSUM MP_TAC
473 THEN ONCE_REWRITE_TAC [GSYM pairTheory.PAIR]
474 THEN REWRITE_TAC [tint_0,tint_lt,tint_eq,tint_of_num_eq]
475 THEN SIMP_TAC int_ss []
476QED
477
478(*--------------------------------------------------------------------------*)
479(* Now define the functions over the equivalence classes *)
480(*--------------------------------------------------------------------------*)
481
482val _ = print "Establish type of integers\n";
483
484local
485 fun mk_def (d,t,n) = {def_name=d, fixity=NONE, fname=n, func=t}
486in
487 val [INT_10, INT_ADD_SYM, INT_MUL_SYM,
488 INT_ADD_ASSOC, INT_MUL_ASSOC, INT_LDISTRIB,
489 INT_ADD_LID, INT_MUL_LID, INT_ADD_LINV,
490 INT_LT_TOTAL, INT_LT_REFL, INT_LT_TRANS,
491 INT_LT_LADD_IMP, INT_LT_MUL,
492 int_of_num, INT_INJ, NUM_POSINT_EX] =
493 define_equivalence_type
494 {name = "int", equiv = TINT_EQ_EQUIV,
495 defs = [mk_def ("int_0" , “tint_0”, "int_0"),
496 mk_def ("int_1" , “tint_1”, "int_1"),
497 mk_def ("int_neg" , “tint_neg”, "int_neg"),
498 mk_def ("int_add" , “$tint_add”, "int_add"),
499 mk_def ("int_mul" , “$tint_mul”, "int_mul"),
500 mk_def ("int_lt" , “$tint_lt”, "int_lt"),
501 mk_def ("int_of_num" , “tint_of_num”, "int_of_num")],
502
503 welldefs = [TINT_NEG_WELLDEF, TINT_LT_WELLDEF,
504 TINT_ADD_WELLDEF, TINT_MUL_WELLDEF],
505 old_thms = ([TINT_10, TINT_ADD_SYM, TINT_MUL_SYM, TINT_ADD_ASSOC,
506 TINT_MUL_ASSOC, TINT_LDISTRIB,
507 TINT_ADD_LID, TINT_MUL_LID, TINT_ADD_LINV,
508 TINT_LT_TOTAL, TINT_LT_REFL, TINT_LT_TRANS,
509 TINT_LT_ADD, TINT_LT_MUL, tint_of_num,
510 TINT_INJ, NUM_POSTINT_EX])}
511end;
512
513Theorem INT_10 = INT_10
514Theorem INT_ADD_SYM = INT_ADD_SYM
515Theorem INT_ADD_COMM = INT_ADD_SYM;
516Theorem INT_MUL_SYM = INT_MUL_SYM
517Theorem INT_MUL_COMM = INT_MUL_SYM;
518Theorem INT_ADD_ASSOC = INT_ADD_ASSOC
519Theorem INT_MUL_ASSOC = INT_MUL_ASSOC
520Theorem INT_LDISTRIB = INT_LDISTRIB
521Theorem INT_LT_TOTAL = INT_LT_TOTAL
522Theorem INT_LT_REFL = INT_LT_REFL
523Theorem INT_LT_TRANS = INT_LT_TRANS
524Theorem INT_LT_LADD_IMP = INT_LT_LADD_IMP
525Theorem INT_LT_MUL = INT_LT_MUL
526Theorem NUM_POSINT_EX = NUM_POSINT_EX
527;
528
529Overload "+" = Term`int_add`
530Overload "<" = Term`int_lt`
531Overload "*" = Term`int_mul`
532
533
534(* this is a slightly tricky case; we don't have to call overload_on
535 on the boolean negation, but we're doing so to put it back at the
536 top of the list of possible resolutions.
537
538 Also need to overload from the Unicode negation in order to make that
539 preferred over the tilde.
540
541*)
542
543val bool_not = “$~ : bool -> bool”
544Overload "~" = “int_neg”
545Overload "~" = bool_not
546Overload numeric_negate = “int_neg”
547Overload "¬" = bool_not
548
549(*--------------------------------------------------------------------------*)
550(* Define subtraction and the other orderings *)
551(*--------------------------------------------------------------------------*)
552
553val int_sub =
554 new_infixl_definition("int_sub",
555 Term `$int_sub x y = x + ~y`,
556 500);
557Overload "-" = Term`$int_sub`
558
559Definition int_le[nocompute]: int_le x y = ~(y<x:int)
560End
561Overload "<=" = “$int_le”
562
563Definition int_gt[nocompute]: int_gt (x:int) y <=> y < x
564End
565Overload ">" = “$int_gt”
566
567Definition int_ge[nocompute]: int_ge x y <=> y <= x:int
568End
569Overload ">=" = “$int_ge”
570
571Theorem INT_GT = int_gt (* HOL-Light compatible name *)
572Theorem INT_GE = int_ge (* HOL-Light compatible name *)
573
574(*--------------------------------------------------------------------------*)
575(* Now use the lifted inclusion homomorphism int_of_num:num->int. *)
576(*--------------------------------------------------------------------------*)
577
578val _ = add_numeral_form(#"i", SOME "int_of_num");
579
580Theorem INT_0:
581 int_0 = 0i
582Proof
583 REWRITE_TAC[int_of_num]
584QED
585
586Theorem INT_1:
587 int_1 = 1i
588Proof
589 REWRITE_TAC[ONE, int_of_num, INT_ADD_LID]
590QED
591
592(*--------------------------------------------------------------------------*)
593(* Prove lots of boring ring theorems *)
594(*--------------------------------------------------------------------------*)
595
596val _ = print "Prove \"lots of boring ring theorems\"\n";
597
598(* already defined, but using the wrong term for 0 *)
599Theorem INT_ADD_LID[simp]:
600 !x:int. 0 + x = x
601Proof
602 SIMP_TAC int_ss [GSYM INT_0, INT_ADD_LID]
603QED
604
605
606Theorem INT_ADD_RID[simp]:
607 !x:int. x + 0 = x
608Proof
609 PROVE_TAC [INT_ADD_COMM,INT_ADD_LID]
610QED
611
612
613(* already defined, but using the wrong term for 0 *)
614Theorem INT_ADD_LINV[simp]: !x. ~x + x = 0
615Proof SIMP_TAC int_ss [GSYM INT_0, INT_ADD_LINV]
616QED
617Theorem INT_ADD_RINV[simp]:
618 !x. x + ~x = 0
619Proof
620 ONCE_REWRITE_TAC [INT_ADD_SYM] THEN REWRITE_TAC [INT_ADD_LINV]
621QED
622
623(* already defined, but using the wrong term for 1 *)
624Theorem INT_MUL_LID[simp]: !x:int. 1 * x = x
625Proof
626 SIMP_TAC int_ss [GSYM INT_1, INT_MUL_LID]
627QED
628
629Theorem INT_MUL_RID[simp]: !x:int. x * 1 = x
630Proof PROVE_TAC [INT_MUL_SYM,GSYM INT_1,INT_MUL_LID]
631QED
632
633Theorem INT_RDISTRIB:
634 !(x:int) y z. (x + y) * z = (x * z) + (y * z)
635Proof
636 ONCE_REWRITE_TAC [INT_MUL_COMM] THEN
637 REWRITE_TAC [INT_LDISTRIB]
638QED
639
640Theorem INT_EQ_LADD:
641 !(x:int) y z. (x + y = x + z) = (y = z)
642Proof
643 REPEAT GEN_TAC THEN EQ_TAC THENL
644 [DISCH_THEN(MP_TAC o AP_TERM (Term `$+ ~x`)), ALL_TAC] THEN
645 SIMP_TAC int_ss [INT_ADD_ASSOC, INT_ADD_LINV, INT_ADD_LID]
646QED
647
648
649Theorem INT_EQ_RADD:
650 !x:int y z. (x + z = y + z) = (x = y)
651Proof
652 REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[INT_ADD_SYM] THEN
653 SIMP_TAC int_ss [INT_EQ_LADD]
654QED
655
656Theorem INT_ADD_LID_UNIQ:
657 !x:int y. (x + y = y) = (x = 0)
658Proof
659 REPEAT GEN_TAC THEN
660 GEN_REWRITE_TAC (LAND_CONV o RAND_CONV)
661 empty_rewrites [GSYM INT_ADD_LID]
662 THEN SIMP_TAC int_ss [INT_EQ_RADD]
663QED
664
665Theorem INT_ADD_RID_UNIQ:
666 !x:int y. (x + y = x) = (y = 0)
667Proof
668 REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[INT_ADD_SYM] THEN
669 SIMP_TAC int_ss [INT_ADD_LID_UNIQ]
670QED
671
672Theorem INT_LNEG_UNIQ:
673 !x y. (x + y = 0) = (x = ~y)
674Proof
675 REPEAT GEN_TAC
676 THEN SUBST1_TAC (SYM(SPEC (Term `y:int`) INT_ADD_LINV))
677 THEN SIMP_TAC int_ss [INT_EQ_RADD]
678QED
679
680Theorem INT_RNEG_UNIQ:
681 !x y. (x + y = 0) = (y = ~x)
682Proof
683 REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[INT_ADD_SYM] THEN
684 SIMP_TAC int_ss [INT_LNEG_UNIQ]
685QED
686
687Theorem INT_NEG_ADD:
688 !x y. ~(x + y) = ~x + ~y
689Proof
690 REPEAT GEN_TAC THEN CONV_TAC SYM_CONV THEN
691 REWRITE_TAC[GSYM INT_LNEG_UNIQ] THEN
692 ONCE_REWRITE_TAC
693 [jrhUtils.AC(INT_ADD_ASSOC,INT_ADD_SYM)
694 (Term `(a + b) + (c + d) = (a + c) + (b + d:int)`)] THEN
695 REWRITE_TAC[INT_ADD_LINV, INT_ADD_RID,INT_0]
696QED
697
698Theorem INT_MUL_LZERO[simp]:
699 !x:int. 0 * x = 0
700Proof
701 GEN_TAC THEN SUBST1_TAC
702 (SYM(Q.SPECL [`0 * x`, `0 * x`] INT_ADD_LID_UNIQ))
703 THEN REWRITE_TAC[GSYM INT_RDISTRIB, INT_ADD_RID]
704QED
705
706Theorem INT_MUL_RZERO[simp]:
707 !x. x * 0i = 0
708Proof
709 GEN_TAC THEN ONCE_REWRITE_TAC[INT_MUL_SYM] THEN
710 SIMP_TAC int_ss [INT_MUL_LZERO]
711QED
712
713Theorem INT_NEG_LMUL:
714 !x y. ~(x * y) = ~x * y
715Proof
716 REPEAT GEN_TAC THEN CONV_TAC SYM_CONV THEN
717 REWRITE_TAC[GSYM INT_LNEG_UNIQ, GSYM INT_RDISTRIB,
718 INT_ADD_LINV, INT_MUL_LZERO,INT_0]
719QED
720
721(* |- !x y. -x * y = -(x * y) *)
722Theorem INT_MUL_LNEG = GSYM INT_NEG_LMUL (* HOL-Light compatible *)
723
724Theorem INT_NEG_RMUL:
725 !x y. ~(x * y) = x * ~y
726Proof
727 REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[INT_MUL_SYM] THEN
728 SIMP_TAC int_ss [INT_NEG_LMUL]
729QED
730
731(* |- !x y. x * -y = -(x * y) *)
732Theorem INT_MUL_RNEG = GSYM INT_NEG_RMUL (* HOL-Light compatible *)
733
734Theorem INT_NEGNEG[simp]:
735 !x:int. ~~x = x
736Proof
737 GEN_TAC THEN CONV_TAC SYM_CONV THEN
738 REWRITE_TAC[GSYM INT_LNEG_UNIQ, INT_ADD_RINV]
739QED
740
741Theorem INT_NEG_NEG = INT_NEGNEG (* HOL-Light compatible name *)
742
743Theorem INT_NEG_MUL2:
744 !x y. ~x * ~y = x * y
745Proof
746 REWRITE_TAC[GSYM INT_NEG_LMUL, GSYM INT_NEG_RMUL, INT_NEGNEG]
747QED
748
749Theorem INT_LT_LADD:
750 !x:int y z. x + y < x + z <=> y < z
751Proof
752 REPEAT GEN_TAC THEN EQ_TAC THENL
753 [DISCH_THEN(MP_TAC o (SPEC (Term `~x:int`)) o
754 MATCH_MP INT_LT_LADD_IMP)
755 THEN
756 REWRITE_TAC[INT_ADD_ASSOC, INT_ADD_LINV, INT_ADD_LID],
757 SIMP_TAC int_ss [INT_LT_LADD_IMP]]
758QED
759
760Theorem INT_LT_RADD:
761 !x:int y z. (x + z) < (y + z) <=> x < y
762Proof
763 REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[INT_ADD_SYM] THEN
764 SIMP_TAC int_ss [INT_LT_LADD]
765QED
766
767Theorem INT_NOT_LT:
768 !x:int y. ~(x < y) <=> y <= x
769Proof
770 REPEAT GEN_TAC THEN REWRITE_TAC[int_le]
771QED
772
773(* NOTE: This is INT_LT of HOL-Light *)
774Theorem INT_LT2 :
775 !x (y :int). x < y <=> ~(y <= x)
776Proof
777 REWRITE_TAC [GSYM INT_NOT_LT]
778QED
779
780Theorem INT_LT_ANTISYM:
781 !x:int y. ~(x < y /\ y < x)
782Proof
783 REPEAT GEN_TAC THEN DISCH_THEN(MP_TAC o MATCH_MP INT_LT_TRANS)
784 THEN REWRITE_TAC[INT_LT_REFL]
785QED
786
787Theorem INT_LT_GT:
788 !x:int y. x < y ==> ~(y < x)
789Proof
790 REPEAT GEN_TAC THEN
791 DISCH_THEN(fn th => DISCH_THEN(MP_TAC o CONJ th)) THEN
792 REWRITE_TAC[INT_LT_ANTISYM]
793QED
794
795Theorem INT_NOT_LE:
796 !x y:int. ~(x <= y) <=> y < x
797Proof
798 REPEAT GEN_TAC THEN REWRITE_TAC[int_le]
799QED
800
801Theorem INT_LE_TOTAL:
802 !x y:int. x <= y \/ y <= x
803Proof
804 REPEAT GEN_TAC THEN
805 REWRITE_TAC[int_le, GSYM DE_MORGAN_THM, INT_LT_ANTISYM]
806QED
807
808Theorem INT_LET_TOTAL:
809 !x y:int. x <= y \/ y < x
810Proof
811 REPEAT GEN_TAC THEN REWRITE_TAC[int_le] THEN
812 SIMP_TAC int_ss []
813QED
814
815Theorem INT_LTE_TOTAL:
816 !x y:int. x < y \/ y <= x
817Proof
818 REPEAT GEN_TAC THEN REWRITE_TAC[int_le] THEN
819 SIMP_TAC int_ss []
820QED
821
822
823Theorem INT_LE_REFL[simp]: !x:int. x <= x
824Proof GEN_TAC THEN REWRITE_TAC[int_le, INT_LT_REFL]
825QED
826
827Theorem INT_LE_LT:
828 !x y:int. x <= y <=> x < y \/ (x = y)
829Proof
830 REPEAT GEN_TAC THEN REWRITE_TAC[int_le] THEN EQ_TAC THENL
831 [REPEAT_TCL DISJ_CASES_THEN ASSUME_TAC
832 (SPECL [Term `x:int`, Term `y:int`] INT_LT_TOTAL) THEN ASM_REWRITE_TAC[],
833 DISCH_THEN(DISJ_CASES_THEN2
834 (curry(op THEN) (MATCH_MP_TAC INT_LT_GT) o ACCEPT_TAC) SUBST1_TAC) THEN
835 MATCH_ACCEPT_TAC INT_LT_REFL]
836QED
837
838Theorem INT_LT_LE:
839 !x y:int. x < y <=> x <= y /\ ~(x = y)
840Proof
841 let val lemma = TAUT_CONV (Term `~(a /\ ~a)`)
842 in
843 REPEAT GEN_TAC THEN REWRITE_TAC[INT_LE_LT, RIGHT_AND_OVER_OR, lemma]
844 THEN EQ_TAC THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN
845 POP_ASSUM MP_TAC THEN CONV_TAC CONTRAPOS_CONV THEN REWRITE_TAC[] THEN
846 DISCH_THEN SUBST1_TAC THEN REWRITE_TAC[INT_LT_REFL]
847 end
848QED
849
850Theorem INT_LT_IMP_LE:
851 !x y:int. x < y ==> x <= y
852Proof
853 REPEAT GEN_TAC THEN DISCH_TAC THEN
854 ASM_REWRITE_TAC[INT_LE_LT]
855QED
856
857Theorem INT_LTE_TRANS:
858 !x y z:int. x < y /\ y <= z ==> x < z
859Proof
860 REPEAT GEN_TAC THEN REWRITE_TAC[INT_LE_LT, LEFT_AND_OVER_OR] THEN
861 DISCH_THEN(DISJ_CASES_THEN2 (ACCEPT_TAC o MATCH_MP INT_LT_TRANS)
862 (CONJUNCTS_THEN2 MP_TAC SUBST1_TAC))
863 THEN REWRITE_TAC[]
864QED
865
866Theorem INT_LET_TRANS:
867 !x y z:int. x <= y /\ y < z ==> x < z
868Proof
869 REPEAT GEN_TAC THEN REWRITE_TAC[INT_LE_LT, RIGHT_AND_OVER_OR]
870 THEN
871 DISCH_THEN(DISJ_CASES_THEN2 (ACCEPT_TAC o MATCH_MP INT_LT_TRANS)
872 (CONJUNCTS_THEN2 SUBST1_TAC ACCEPT_TAC))
873QED
874
875Theorem INT_LE_TRANS:
876 !x y z:int. x <= y /\ y <= z ==> x <= z
877Proof
878 REPEAT GEN_TAC THEN
879 GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) empty_rewrites
880 [INT_LE_LT] THEN
881 DISCH_THEN(CONJUNCTS_THEN2 MP_TAC
882 (DISJ_CASES_THEN2 ASSUME_TAC SUBST1_TAC))
883 THEN REWRITE_TAC[]
884 THEN DISCH_THEN(MP_TAC o C CONJ (ASSUME (Term `y < z:int`))) THEN
885 DISCH_THEN(ACCEPT_TAC o MATCH_MP
886 INT_LT_IMP_LE o MATCH_MP INT_LET_TRANS)
887QED
888
889Theorem INT_LE_ANTISYM:
890 !x y:int. x <= y /\ y <= x <=> (x = y)
891Proof
892 REPEAT GEN_TAC THEN EQ_TAC THENL
893 [REWRITE_TAC[int_le] THEN REPEAT_TCL DISJ_CASES_THEN ASSUME_TAC
894 (SPECL [Term `x:int`, Term `y:int`] INT_LT_TOTAL) THEN
895 ASM_REWRITE_TAC[],
896 DISCH_THEN SUBST1_TAC THEN REWRITE_TAC[INT_LE_REFL]]
897QED
898
899Theorem INT_LET_ANTISYM:
900 !x y:int. ~(x < y /\ y <= x)
901Proof
902 REPEAT GEN_TAC THEN REWRITE_TAC[int_le] THEN
903 BOOL_CASES_TAC (Term `x < y:int`) THEN REWRITE_TAC[]
904QED
905
906Theorem INT_LTE_ANTSYM:
907 !x y:int. ~(x <= y /\ y < x)
908Proof
909 REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[CONJ_SYM] THEN
910 MATCH_ACCEPT_TAC INT_LET_ANTISYM
911QED
912
913Theorem INT_NEG_LT0:
914 !x. ~x < 0 <=> 0 < x
915Proof
916 GEN_TAC THEN
917 SUBST1_TAC(SYM(Q.SPECL [`~x`, `0`,`x`] INT_LT_RADD)) THEN
918 REWRITE_TAC[INT_ADD_LINV, INT_ADD_LID]
919QED
920
921Theorem INT_NEG_GT0:
922 !x. 0 < ~x <=> x < 0
923Proof GEN_TAC THEN REWRITE_TAC[GSYM INT_NEG_LT0, INT_NEGNEG]
924QED
925
926Theorem INT_NEG_LE0:
927 !x. ~x <= 0 <=> 0 <= x
928Proof GEN_TAC THEN REWRITE_TAC[int_le] THEN
929 REWRITE_TAC[INT_NEG_GT0]
930QED
931
932Theorem INT_NEG_GE0:
933 !x. 0 <= ~x <=> x <= 0
934Proof
935 GEN_TAC THEN REWRITE_TAC[int_le] THEN
936 REWRITE_TAC[INT_NEG_LT0]
937QED
938
939Theorem INT_LT_NEGTOTAL:
940 !x. (x = 0) \/ 0<x \/ 0 < ~x
941Proof
942 GEN_TAC THEN REPEAT_TCL DISJ_CASES_THEN ASSUME_TAC
943 (Q.SPECL [`x`, `0`] INT_LT_TOTAL) THEN
944 ASM_REWRITE_TAC
945 [SYM(REWRITE_RULE[INT_NEGNEG] (Q.SPEC `~x` INT_NEG_LT0))]
946QED
947
948Theorem INT_LE_NEGTOTAL:
949 !x. 0 <= x \/ 0 <= ~x
950Proof
951 GEN_TAC THEN REWRITE_TAC[INT_LE_LT] THEN
952 REPEAT_TCL DISJ_CASES_THEN ASSUME_TAC (SPEC (Term `x:int`)
953 INT_LT_NEGTOTAL)
954 THEN ASM_REWRITE_TAC[]
955QED
956
957Theorem INT_LE_MUL:
958 !x y:int. 0 <= x /\ 0 <= y ==> 0 <= x*y
959Proof
960 REPEAT GEN_TAC THEN REWRITE_TAC[INT_LE_LT] THEN
961 MAP_EVERY ASM_CASES_TAC [Term `0i = x`, Term `0i = y`] THEN
962 ASM_REWRITE_TAC[] THEN TRY(FIRST_ASSUM(SUBST1_TAC o SYM)) THEN
963 REWRITE_TAC[INT_MUL_LZERO, INT_MUL_RZERO] THEN
964 DISCH_TAC THEN DISJ1_TAC
965 THEN MATCH_MP_TAC (REWRITE_RULE [INT_0] INT_LT_MUL) THEN
966 ASM_REWRITE_TAC[]
967QED
968
969Theorem INT_LE_SQUARE:
970 !x:int. 0 <= x * x
971Proof
972 GEN_TAC THEN DISJ_CASES_TAC (SPEC (Term `x:int`) INT_LE_NEGTOTAL)
973 THEN
974 POP_ASSUM(MP_TAC o MATCH_MP INT_LE_MUL o W CONJ) THEN
975 REWRITE_TAC[GSYM INT_NEG_RMUL, GSYM INT_NEG_LMUL, INT_NEGNEG]
976QED
977
978Theorem INT_LE_01:
979 0i <= 1
980Proof
981 SUBST1_TAC(SYM(Q.SPEC `1` INT_MUL_LID)) THEN
982 SIMP_TAC int_ss [INT_LE_SQUARE,INT_1]
983QED
984
985Theorem INT_LT_01:
986 0i < 1i
987Proof
988 SIMP_TAC int_ss [INT_LT_LE, INT_LE_01,
989 GSYM INT_0,GSYM INT_1,INT_10]
990QED
991
992Theorem INT_LE_LADD:
993 !x:int y z. x + y <= x + z <=> y <= z
994Proof
995 REPEAT GEN_TAC THEN REWRITE_TAC[int_le] THEN
996 AP_TERM_TAC THEN MATCH_ACCEPT_TAC INT_LT_LADD
997QED
998
999Theorem INT_LE_RADD:
1000 !x y z:int. (x + z) <= (y + z) <=> x <= y
1001Proof
1002 REPEAT GEN_TAC THEN REWRITE_TAC[int_le] THEN
1003 AP_TERM_TAC THEN MATCH_ACCEPT_TAC INT_LT_RADD
1004QED
1005
1006Theorem INT_LT_ADD2:
1007 !w x y z:int. w < x /\ y < z ==> w + y < x + z
1008Proof
1009 REPEAT GEN_TAC THEN DISCH_TAC THEN
1010 MATCH_MP_TAC INT_LT_TRANS THEN EXISTS_TAC (Term `w + z:int`) THEN
1011 ASM_REWRITE_TAC[INT_LT_LADD, INT_LT_RADD]
1012QED
1013
1014Theorem INT_LE_ADD2:
1015 !w x y z:int. w <= x /\ y <= z ==> w + y <= x + z
1016Proof
1017 REPEAT GEN_TAC THEN DISCH_TAC THEN
1018 MATCH_MP_TAC INT_LE_TRANS THEN EXISTS_TAC (Term `w + z:int`) THEN
1019 ASM_REWRITE_TAC[INT_LE_LADD, INT_LE_RADD]
1020QED
1021
1022Theorem INT_LE_ADD:
1023 !x y:int. 0 <= x /\ 0 <= y ==> 0 <= (x + y)
1024Proof
1025 REPEAT GEN_TAC
1026 THEN DISCH_THEN(MP_TAC o MATCH_MP INT_LE_ADD2) THEN
1027 REWRITE_TAC[INT_ADD_LID]
1028QED
1029
1030Theorem INT_LT_ADD:
1031 !x y:int. 0 < x /\ 0 < y ==> 0 < (x + y)
1032Proof
1033 REPEAT GEN_TAC THEN DISCH_THEN(MP_TAC o MATCH_MP INT_LT_ADD2)
1034 THEN
1035 REWRITE_TAC[INT_ADD_LID]
1036QED
1037
1038Theorem INT_LT_ADDNEG:
1039 !x y z. y < x + ~z <=> y+z < x
1040Proof
1041 REPEAT GEN_TAC THEN
1042 SUBST1_TAC(SYM(SPECL [Term `y:int`,
1043 Term `x + ~z`,
1044 Term `z:int`] INT_LT_RADD)) THEN
1045 REWRITE_TAC[GSYM INT_ADD_ASSOC, INT_ADD_LINV,
1046 INT_ADD_RID, INT_0]
1047QED
1048
1049(* REWRITE TO *)
1050Theorem INT_LT_ADDNEG2:
1051 !x y z. x + ~y < z <=> x < z+y
1052Proof
1053 REPEAT GEN_TAC THEN
1054 SUBST1_TAC
1055 (SYM(SPECL [Term `x + ~y`, Term `z:int`,Term `y:int`] INT_LT_RADD)) THEN
1056 REWRITE_TAC[GSYM INT_ADD_ASSOC, INT_ADD_LINV, INT_ADD_RID,INT_0]
1057QED
1058
1059Theorem INT_LT_ADD1:
1060 !x y:int. x <= y ==> x < (y + 1)
1061Proof
1062 REPEAT GEN_TAC THEN REWRITE_TAC[INT_LE_LT] THEN
1063 DISCH_THEN DISJ_CASES_TAC THENL
1064 [POP_ASSUM(MP_TAC o MATCH_MP INT_LT_ADD2 o C CONJ INT_LT_01)
1065 THEN
1066 REWRITE_TAC[INT_ADD_RID],
1067 POP_ASSUM SUBST1_TAC THEN
1068 GEN_REWRITE_TAC LAND_CONV empty_rewrites [GSYM INT_ADD_RID] THEN
1069 REWRITE_TAC[INT_LT_LADD, INT_LT_01]]
1070QED
1071
1072Theorem INT_SUB_ADD:
1073 !x y:int. (x - y) + y = x
1074Proof
1075 REPEAT GEN_TAC THEN
1076 REWRITE_TAC[int_sub, GSYM INT_ADD_ASSOC,
1077 INT_ADD_LINV, INT_ADD_RID,INT_0]
1078QED
1079
1080Theorem INT_SUB_ADD2:
1081 !x y:int. y + (x - y) = x
1082Proof
1083 REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[INT_ADD_SYM] THEN
1084 MATCH_ACCEPT_TAC INT_SUB_ADD
1085QED
1086
1087Theorem INT_SUB_REFL:
1088 !x:int. x - x = 0
1089Proof
1090 GEN_TAC THEN REWRITE_TAC[int_sub, INT_ADD_RINV]
1091QED
1092
1093Theorem INT_SUB_0:
1094 !x y:int. (x - y = 0) = (x = y)
1095Proof
1096 REPEAT GEN_TAC THEN EQ_TAC THENL
1097 [DISCH_THEN(MP_TAC o C AP_THM (Term `y:int`) o
1098 AP_TERM (Term `$+ :int->int->int`)) THEN
1099 REWRITE_TAC[INT_SUB_ADD, INT_ADD_LID],
1100 DISCH_THEN SUBST1_TAC THEN MATCH_ACCEPT_TAC INT_SUB_REFL]
1101QED
1102
1103Theorem INT_LE_DOUBLE:
1104 !x:int. 0 <= x + x <=> 0 <= x
1105Proof
1106 GEN_TAC THEN EQ_TAC THENL
1107 [CONV_TAC CONTRAPOS_CONV THEN REWRITE_TAC[INT_NOT_LE] THEN
1108 DISCH_THEN(MP_TAC o MATCH_MP INT_LT_ADD2 o W CONJ)
1109 THEN REWRITE_TAC [INT_ADD_RID],
1110 DISCH_THEN(MP_TAC o MATCH_MP INT_LE_ADD2 o W CONJ)] THEN
1111 REWRITE_TAC[INT_ADD_RID]
1112QED
1113
1114Theorem INT_LE_NEGL:
1115 !x. ~x <= x <=> 0 <= x
1116Proof
1117 GEN_TAC THEN SUBST1_TAC (SYM
1118 (SPECL [Term `x:int`,Term `~x:int`, Term `x:int`]INT_LE_LADD))
1119 THEN REWRITE_TAC[INT_ADD_RINV, INT_LE_DOUBLE]
1120QED
1121
1122Theorem INT_LE_NEGR:
1123 !x. x <= ~x <=> x <= 0
1124Proof
1125 GEN_TAC THEN SUBST1_TAC(SYM(SPEC (Term `x:int`) INT_NEGNEG)) THEN
1126 GEN_REWRITE_TAC (LAND_CONV o RAND_CONV)
1127 empty_rewrites [INT_NEGNEG] THEN
1128 REWRITE_TAC[INT_LE_NEGL] THEN REWRITE_TAC[INT_NEG_GE0] THEN
1129 REWRITE_TAC[INT_NEGNEG]
1130QED
1131
1132Theorem INT_NEG_EQ0:
1133 !x. (~x = 0) = (x = 0)
1134Proof
1135GEN_TAC THEN EQ_TAC THENL
1136[DISCH_THEN(MP_TAC o AP_TERM (Term `$+ x:int->int`))
1137 THEN REWRITE_TAC[INT_ADD_RINV, INT_ADD_LINV, INT_ADD_RID, INT_0]
1138 THEN DISCH_THEN SUBST1_TAC THEN REFL_TAC,
1139 DISCH_THEN(MP_TAC o AP_TERM (Term `$+ (~x)`))
1140 THEN REWRITE_TAC[INT_ADD_RINV, INT_ADD_LINV, INT_ADD_RID, INT_0]
1141 THEN DISCH_THEN SUBST1_TAC THEN REFL_TAC]
1142QED
1143
1144Theorem INT_NEG_0[simp]: ~0 = 0
1145Proof REWRITE_TAC[INT_NEG_EQ0]
1146QED
1147
1148Theorem INT_NEG_SUB:
1149 !x y. ~(x - y) = y - x
1150Proof
1151 REPEAT GEN_TAC THEN REWRITE_TAC[int_sub,
1152 INT_NEG_ADD, INT_NEGNEG] THEN
1153 MATCH_ACCEPT_TAC INT_ADD_SYM
1154QED
1155
1156Theorem INT_SUB_LT:
1157 !x:int y. 0 < x - y <=> y < x
1158Proof
1159 REPEAT GEN_TAC THEN
1160 SUBST1_TAC(SYM(Q.SPECL [`0`, `x - y`, `y`] INT_LT_RADD)) THEN
1161 REWRITE_TAC[INT_SUB_ADD, INT_ADD_LID]
1162QED
1163
1164Theorem INT_SUB_LE:
1165 !x:int y. 0 <= (x - y) <=> y <= x
1166Proof
1167 REPEAT GEN_TAC THEN
1168 SUBST1_TAC(SYM(Q.SPECL [`0`, `x - y`, `y`] INT_LE_RADD)) THEN
1169 REWRITE_TAC[INT_SUB_ADD, INT_ADD_LID]
1170QED
1171
1172Theorem INT_ADD_SUB:
1173 !x y:int. (x + y) - x = y
1174Proof
1175 REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[INT_ADD_SYM] THEN
1176 REWRITE_TAC[int_sub, GSYM INT_ADD_ASSOC,
1177 INT_ADD_RINV, INT_ADD_RID, INT_0]
1178QED
1179
1180Theorem INT_SUB_LDISTRIB:
1181 !x y z:int. x * (y - z) = (x * y) - (x * z)
1182Proof
1183 REPEAT GEN_TAC THEN REWRITE_TAC[int_sub,
1184 INT_LDISTRIB, INT_NEG_RMUL]
1185QED
1186
1187Theorem INT_SUB_RDISTRIB:
1188 !x y z:int. (x - y) * z = (x * z) - (y * z)
1189Proof
1190 REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[INT_MUL_SYM] THEN
1191 MATCH_ACCEPT_TAC INT_SUB_LDISTRIB
1192QED
1193
1194Theorem INT_NEG_EQ:
1195 !x y:int. (~x = y) = (x = ~y)
1196Proof
1197 REPEAT GEN_TAC THEN EQ_TAC THENL
1198 [DISCH_THEN(SUBST1_TAC o SYM), DISCH_THEN SUBST1_TAC] THEN
1199 REWRITE_TAC[INT_NEGNEG]
1200QED
1201
1202Theorem INT_NEG_MINUS1:
1203 !x. ~x = ~1 * x
1204Proof
1205 GEN_TAC THEN REWRITE_TAC[GSYM INT_NEG_LMUL] THEN
1206 REWRITE_TAC[INT_MUL_LID,GSYM INT_1]
1207QED
1208
1209
1210Theorem INT_LT_IMP_NE:
1211 !x y:int. x < y ==> ~(x = y)
1212Proof
1213 REPEAT GEN_TAC THEN CONV_TAC CONTRAPOS_CONV THEN
1214 REWRITE_TAC[] THEN DISCH_THEN SUBST1_TAC THEN
1215 REWRITE_TAC[INT_LT_REFL]
1216QED
1217
1218Theorem INT_NOT_EQ :
1219 !x y. ~(x = y) <=> x < y \/ y < x
1220Proof
1221 rpt GEN_TAC
1222 >> EQ_TAC
1223 >- PROVE_TAC [INT_LT_TOTAL]
1224 >> PROVE_TAC [INT_LT_IMP_NE]
1225QED
1226
1227Theorem INT_LE_ADDR:
1228 !x y:int. x <= x + y <=> 0 <= y
1229Proof
1230 REPEAT GEN_TAC THEN
1231 SUBST1_TAC(SYM(Q.SPECL [`x`, `0`, `y`] INT_LE_LADD)) THEN
1232 REWRITE_TAC[INT_ADD_RID,INT_0]
1233QED
1234
1235Theorem INT_LE_ADDL:
1236 !x y:int. y <= x + y <=> 0 <= x
1237Proof
1238 REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[INT_ADD_SYM] THEN
1239 MATCH_ACCEPT_TAC INT_LE_ADDR
1240QED
1241
1242Theorem INT_LT_ADDR:
1243 !x y:int. x < x + y <=> 0 < y
1244Proof
1245 REPEAT GEN_TAC THEN
1246 SUBST1_TAC(SYM(Q.SPECL [`x`, `0`,`y`] INT_LT_LADD)) THEN
1247 REWRITE_TAC[INT_ADD_RID,INT_0]
1248QED
1249
1250Theorem INT_LT_ADDL:
1251 !x y:int. y < x + y <=> 0 < x
1252Proof
1253 REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[INT_ADD_SYM] THEN
1254 MATCH_ACCEPT_TAC INT_LT_ADDR
1255QED
1256
1257Theorem INT_ENTIRE:
1258 !x y:int. (x * y = 0) <=> (x = 0) \/ (y = 0)
1259Proof
1260 REPEAT GEN_TAC THEN EQ_TAC THENL
1261 [CONV_TAC CONTRAPOS_CONV THEN REWRITE_TAC[DE_MORGAN_THM] THEN
1262 STRIP_TAC THEN
1263 REPEAT_TCL DISJ_CASES_THEN MP_TAC
1264 (SPEC (Term `x:int`) INT_LT_NEGTOTAL) THEN
1265 ASM_REWRITE_TAC[] THEN
1266 REPEAT_TCL DISJ_CASES_THEN MP_TAC
1267 (SPEC (Term `y:int`) INT_LT_NEGTOTAL) THEN
1268 ASM_REWRITE_TAC[] THEN
1269 REWRITE_TAC[TAUT_CONV (Term `a ==> b ==> c <=> b /\ a ==> c`)]
1270 THEN
1271 DISCH_THEN(MP_TAC o MATCH_MP (REWRITE_RULE [INT_0] INT_LT_MUL))
1272 THEN
1273 REWRITE_TAC[GSYM INT_NEG_LMUL, GSYM INT_NEG_RMUL] THEN
1274 CONV_TAC CONTRAPOS_CONV THEN REWRITE_TAC[INT_NEGNEG] THEN
1275 DISCH_THEN SUBST1_TAC THEN REWRITE_TAC[INT_LT_REFL,INT_NEG_GT0],
1276 DISCH_THEN(DISJ_CASES_THEN SUBST1_TAC) THEN
1277 REWRITE_TAC[INT_MUL_LZERO, INT_MUL_RZERO]]
1278QED
1279
1280Theorem INT_EQ_LMUL:
1281 !x y z:int. (x * y = x * z) <=> (x = 0) \/ (y = z)
1282Proof
1283 REPEAT GEN_TAC THEN
1284 GEN_REWRITE_TAC LAND_CONV empty_rewrites [GSYM INT_SUB_0] THEN
1285 REWRITE_TAC[GSYM INT_SUB_LDISTRIB] THEN
1286 REWRITE_TAC[INT_ENTIRE, INT_SUB_0]
1287QED
1288
1289Theorem INT_EQ_RMUL:
1290 !x y z:int. (x * z = y * z) <=> (z = 0) \/ (x = y)
1291Proof
1292 REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[INT_MUL_SYM] THEN
1293 MATCH_ACCEPT_TAC INT_EQ_LMUL
1294QED
1295
1296
1297(*--------------------------------------------------------------------------*)
1298(* Prove homomorphisms for the inclusion map *)
1299(*--------------------------------------------------------------------------*)
1300
1301val _ = print "Prove homomorphisms for the inclusion map\n"
1302
1303Theorem INT:
1304 !n. &(SUC n) = &n + 1i
1305Proof
1306 GEN_TAC THEN REWRITE_TAC[int_of_num] THEN
1307 REWRITE_TAC[INT_1]
1308QED
1309
1310Theorem INT_POS:
1311 !n. 0i <= &n
1312Proof
1313 INDUCT_TAC THEN REWRITE_TAC[INT_LE_REFL] THEN
1314 MATCH_MP_TAC INT_LE_TRANS THEN
1315 EXISTS_TAC (Term `&n:int`) THEN ASM_REWRITE_TAC[INT] THEN
1316 REWRITE_TAC[INT_LE_ADDR, INT_LE_01]
1317QED
1318
1319Theorem INT_LE:
1320 !m n. &m:int <= &n <=> m <= n
1321Proof
1322 REPEAT INDUCT_TAC THEN ASM_REWRITE_TAC
1323 [INT, INT_LE_RADD, ZERO_LESS_EQ, LESS_EQ_MONO, INT_LE_REFL] THEN
1324 REWRITE_TAC[GSYM NOT_LESS, LESS_0] THENL
1325 [MATCH_MP_TAC INT_LE_TRANS THEN EXISTS_TAC (Term `&n:int`) THEN
1326 ASM_REWRITE_TAC[ZERO_LESS_EQ, INT_LE_ADDR, INT_LE_01],
1327 DISCH_THEN(MP_TAC o C CONJ (SPEC (Term `m:num`) INT_POS)) THEN
1328 DISCH_THEN(MP_TAC o MATCH_MP INT_LE_TRANS) THEN
1329 REWRITE_TAC[INT_NOT_LE, INT_LT_ADDR, INT_LT_01]]
1330QED
1331
1332Theorem INT_LT[simp]:
1333 !m n. &m:int < &n <=> m < n
1334Proof
1335 REPEAT GEN_TAC THEN
1336 MATCH_ACCEPT_TAC ((REWRITE_RULE[] o
1337 AP_TERM (Term `$~:bool->bool`) o
1338 REWRITE_RULE[GSYM NOT_LESS, GSYM INT_NOT_LT])
1339 (SPEC_ALL INT_LE))
1340QED
1341
1342Theorem INT_OF_NUM_LE = INT_LE (* HOL-Light compatible name *)
1343Theorem INT_OF_NUM_LT = INT_LT (* HOL-Light compatible name *)
1344
1345Theorem INT_INJ[simp]: !m n. (&m:int = &n) = (m = n)
1346Proof
1347 let val th = prove(“(m:num = n) <=> m <= n /\ n <= m”,
1348 EQ_TAC
1349 THENL [DISCH_THEN SUBST1_TAC
1350 THEN REWRITE_TAC[LESS_EQ_REFL],
1351 MATCH_ACCEPT_TAC LESS_EQUAL_ANTISYM])
1352 in
1353 REPEAT GEN_TAC THEN REWRITE_TAC[th, GSYM INT_LE_ANTISYM, INT_LE]
1354 end
1355QED
1356
1357(* |- !m n. &m = &n <=> m = n *)
1358Theorem INT_OF_NUM_EQ = INT_INJ (* HOL-Light compatible name *)
1359
1360Theorem INT_ADD:
1361 !m n. &m + &n = &(m + n)
1362Proof
1363 INDUCT_TAC THEN REWRITE_TAC[INT, ADD, INT_ADD_LID]
1364 THEN
1365 RULE_ASSUM_TAC GSYM THEN GEN_TAC THEN ASM_REWRITE_TAC[] THEN
1366 CONV_TAC(AC_CONV(INT_ADD_ASSOC,INT_ADD_SYM))
1367QED
1368
1369Theorem INT_MUL:
1370 !m n. &m * &n = &(m * n)
1371Proof
1372 INDUCT_TAC THEN REWRITE_TAC[INT_MUL_LZERO, MULT_CLAUSES, INT,
1373 GSYM INT_ADD, INT_RDISTRIB] THEN
1374 FIRST_ASSUM(fn th => REWRITE_TAC[GSYM th]) THEN
1375 REWRITE_TAC[INT_MUL_LID,GSYM INT_1]
1376QED
1377
1378Theorem INT_OF_NUM_ADD = INT_ADD (* HOL-Light compatible name *)
1379Theorem INT_OF_NUM_MUL = INT_MUL (* HOL-Light compatible name *)
1380
1381(*--------------------------------------------------------------------------*)
1382(* Now more theorems *)
1383(*--------------------------------------------------------------------------*)
1384
1385
1386Theorem INT_LT_NZ:
1387 !n. ~(&n = 0) = (0 < &n)
1388Proof
1389 GEN_TAC THEN REWRITE_TAC[INT_LT_LE] THEN
1390 CONV_TAC(RAND_CONV(ONCE_DEPTH_CONV SYM_CONV)) THEN
1391 ASM_CASES_TAC (Term `&n = 0`)
1392 THEN ASM_REWRITE_TAC[INT_LE_REFL, INT_POS]
1393QED
1394
1395Theorem INT_NZ_IMP_LT:
1396 !n. ~(n = 0) ==> 0 < &n
1397Proof
1398 GEN_TAC THEN REWRITE_TAC[GSYM INT_INJ, INT_LT_NZ]
1399QED
1400
1401Theorem INT_DOUBLE:
1402 !x:int. x + x = 2 * x
1403Proof
1404 GEN_TAC THEN REWRITE_TAC[num_CONV (Term `2n`), INT] THEN
1405 REWRITE_TAC[INT_RDISTRIB, INT_MUL_LID,GSYM INT_1]
1406QED
1407
1408Theorem INT_SUB_SUB:
1409 !x y. (x - y) - x = ~y
1410Proof
1411 REPEAT GEN_TAC THEN REWRITE_TAC[int_sub] THEN
1412 ONCE_REWRITE_TAC[jrhUtils.AC(INT_ADD_ASSOC,INT_ADD_SYM)
1413 (Term `(a + b) + c = (c + a) + b:int`)] THEN
1414 REWRITE_TAC[INT_ADD_LINV, INT_ADD_LID]
1415QED
1416
1417Theorem INT_LT_ADD_SUB:
1418 !x y z:int. x + y < z <=> x < z - y
1419Proof
1420 REPEAT GEN_TAC THEN
1421 SUBST1_TAC(SYM(SPECL [Term `x:int`, Term `z - y:int`,
1422 Term `y:int`] INT_LT_RADD)) THEN
1423 REWRITE_TAC[INT_SUB_ADD]
1424QED
1425
1426Theorem INT_LT_SUB_RADD:
1427 !x y z:int. x - y < z <=> x < z + y
1428Proof
1429 REPEAT GEN_TAC THEN
1430 SUBST1_TAC(SYM(Q.SPECL [`x - y`, `z`, `y`] INT_LT_RADD)) THEN
1431 REWRITE_TAC[INT_SUB_ADD]
1432QED
1433
1434Theorem INT_LT_SUB_LADD:
1435 !x y z:int. x < y - z <=> x + z < y
1436Proof
1437 REPEAT GEN_TAC THEN
1438 SUBST1_TAC(SYM(Q.SPECL [`x + z`, `y`, `~z`] INT_LT_RADD)) THEN
1439 REWRITE_TAC[int_sub, GSYM INT_ADD_ASSOC,
1440 INT_ADD_RINV, INT_ADD_RID, INT_0]
1441QED
1442
1443Theorem INT_LE_SUB_LADD:
1444 !x y z:int. x <= y - z <=> x + z <= y
1445Proof
1446 REPEAT GEN_TAC THEN REWRITE_TAC[GSYM INT_NOT_LT, INT_LT_SUB_RADD]
1447QED
1448
1449Theorem INT_LE_SUB_RADD:
1450 !x y z:int. x - y <= z <=> x <= z + y
1451Proof
1452 REPEAT GEN_TAC THEN REWRITE_TAC[GSYM INT_NOT_LT,INT_LT_SUB_LADD]
1453QED
1454
1455Theorem INT_LT_NEG:
1456 !x y. ~x < ~y <=> y < x
1457Proof
1458 REPEAT GEN_TAC THEN
1459 SUBST1_TAC(SYM(Q.SPECL[`~x`, `~y`, `x + y`] INT_LT_RADD)) THEN
1460 REWRITE_TAC[INT_ADD_ASSOC, INT_ADD_LINV, INT_ADD_LID]
1461 THEN ONCE_REWRITE_TAC[INT_ADD_SYM] THEN
1462 REWRITE_TAC[INT_ADD_ASSOC, INT_ADD_RINV, INT_ADD_LID]
1463QED
1464
1465Theorem INT_LE_NEG:
1466 !x y. ~x <= ~y <=> y <= x
1467Proof
1468 REPEAT GEN_TAC THEN REWRITE_TAC[GSYM INT_NOT_LT] THEN
1469 REWRITE_TAC[INT_LT_NEG]
1470QED
1471
1472Theorem INT_ADD2_SUB2:
1473 !a b c d:int. (a + b) - (c + d) = (a - c) + (b - d)
1474Proof
1475 REPEAT GEN_TAC THEN REWRITE_TAC[int_sub, INT_NEG_ADD] THEN
1476 CONV_TAC(AC_CONV(INT_ADD_ASSOC,INT_ADD_SYM))
1477QED
1478
1479Theorem INT_SUB_LZERO[simp]: !x. 0 - x = ~x
1480Proof GEN_TAC THEN REWRITE_TAC[int_sub, INT_ADD_LID]
1481QED
1482
1483Theorem INT_SUB_RZERO[simp]: !x:int. x - 0 = x
1484Proof GEN_TAC THEN REWRITE_TAC[int_sub, INT_NEG_0,INT_ADD_RID, INT_0]
1485QED
1486
1487Theorem INT_LET_ADD2:
1488 !w x y z:int. w <= x /\ y < z ==> w + y < x + z
1489Proof
1490 REPEAT GEN_TAC THEN DISCH_THEN STRIP_ASSUME_TAC THEN
1491 MATCH_MP_TAC INT_LTE_TRANS THEN
1492 Q.EXISTS_TAC `w + z` THEN
1493 ASM_REWRITE_TAC[INT_LE_RADD, INT_LT_LADD]
1494QED
1495
1496Theorem INT_LTE_ADD2:
1497 !w x y z:int. w < x /\ y <= z ==> w + y < x + z
1498Proof
1499 REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[CONJ_SYM] THEN
1500 ONCE_REWRITE_TAC[INT_ADD_SYM] THEN
1501 MATCH_ACCEPT_TAC INT_LET_ADD2
1502QED
1503
1504Theorem INT_LET_ADD:
1505 !x y:int. 0 <= x /\ 0 < y ==> 0 < x + y
1506Proof
1507 REPEAT GEN_TAC THEN DISCH_TAC THEN
1508 SUBST1_TAC(SYM(Q.SPEC `0` INT_ADD_LID)) THEN
1509 MATCH_MP_TAC INT_LET_ADD2 THEN ASM_REWRITE_TAC[]
1510QED
1511
1512Theorem INT_LTE_ADD:
1513 !x y:int. 0 < x /\ 0 <= y ==> 0 < x + y
1514Proof
1515 REPEAT GEN_TAC THEN DISCH_TAC THEN
1516 SUBST1_TAC(SYM(Q.SPEC `0` INT_ADD_LID)) THEN
1517 MATCH_MP_TAC INT_LTE_ADD2 THEN ASM_REWRITE_TAC[]
1518QED
1519
1520Theorem INT_LT_MUL2:
1521 !x1 x2 y1 y2:int.
1522 0 <= x1 /\ 0 <= y1 /\ x1 < x2 /\ y1 < y2
1523 ==>
1524 x1 * y1 < x2 * y2
1525Proof
1526 REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[GSYM INT_SUB_LT] THEN
1527 REWRITE_TAC[INT_SUB_RZERO] THEN SUBGOAL_THEN
1528 (Term `!a b c d:int. (a * b) - (c * d)
1529 =
1530 ((a * b) - (a * d)) + ((a * d) - (c * d))`) MP_TAC
1531 THENL
1532 [REPEAT GEN_TAC THEN REWRITE_TAC[int_sub] THEN
1533 ONCE_REWRITE_TAC[jrhUtils.AC(INT_ADD_ASSOC,INT_ADD_SYM)
1534 (Term `(a + b) + (c + d) = (b + c) + (a + d):int`)]
1535 THEN
1536 REWRITE_TAC[INT_ADD_LINV, INT_ADD_LID],
1537 DISCH_THEN(fn th => ONCE_REWRITE_TAC[th]) THEN
1538 REWRITE_TAC[GSYM INT_SUB_LDISTRIB, GSYM INT_SUB_RDISTRIB] THEN
1539 DISCH_THEN STRIP_ASSUME_TAC THEN
1540 MATCH_MP_TAC INT_LTE_ADD THEN CONJ_TAC THENL
1541 [MATCH_MP_TAC (REWRITE_RULE [INT_0] INT_LT_MUL)
1542 THEN ASM_REWRITE_TAC[] THEN
1543 MATCH_MP_TAC INT_LET_TRANS THEN EXISTS_TAC (Term `x1:int`) THEN
1544 ASM_REWRITE_TAC[] THEN ONCE_REWRITE_TAC[GSYM INT_SUB_LT] THEN
1545 ASM_REWRITE_TAC[],
1546 MATCH_MP_TAC (REWRITE_RULE [INT_0] INT_LE_MUL)
1547 THEN ASM_REWRITE_TAC[] THEN
1548 MATCH_MP_TAC INT_LT_IMP_LE THEN ASM_REWRITE_TAC[]]]
1549QED
1550
1551Theorem INT_SUB_LNEG:
1552 !x y. (~x) - y = ~(x + y)
1553Proof
1554 REPEAT GEN_TAC THEN REWRITE_TAC[int_sub, INT_NEG_ADD]
1555QED
1556
1557Theorem INT_SUB_RNEG:
1558 !x y. x - ~y = x + y
1559Proof
1560 REPEAT GEN_TAC THEN REWRITE_TAC[int_sub, INT_NEGNEG]
1561QED
1562
1563Theorem INT_LE_LNEG :
1564 !x y. -x <= y <=> &0 <= x + y
1565Proof
1566 rpt STRIP_TAC
1567 >> REWRITE_TAC [Q.SPECL [‘y’, ‘-x’] (GSYM INT_SUB_LE)]
1568 >> REWRITE_TAC [INT_SUB_RNEG, Once INT_ADD_SYM]
1569QED
1570
1571Theorem INT_LE_RNEG :
1572 !x y. x <= -y <=> x + y <= &0
1573Proof
1574 rpt STRIP_TAC
1575 >> REWRITE_TAC [Q.SPECL [‘-y’, ‘x’] (GSYM INT_SUB_LE)]
1576 >> REWRITE_TAC [INT_SUB_LNEG, INT_NEG_GE0, Once INT_ADD_SYM]
1577QED
1578
1579Theorem INT_SUB_NEG2:
1580 !x y. (~x) - (~y) = y - x
1581Proof
1582 REPEAT GEN_TAC THEN REWRITE_TAC[INT_SUB_LNEG] THEN
1583 REWRITE_TAC[int_sub, INT_NEG_ADD, INT_NEGNEG] THEN
1584 MATCH_ACCEPT_TAC INT_ADD_SYM
1585QED
1586
1587Theorem INT_SUB_TRIANGLE:
1588 !a b c:int. (a - b) + (b - c) = a - c
1589Proof
1590 REPEAT GEN_TAC THEN REWRITE_TAC[int_sub] THEN
1591 ONCE_REWRITE_TAC[jrhUtils.AC(INT_ADD_ASSOC,INT_ADD_SYM)
1592 (Term `(a + b) + (c + d)
1593 = (b + c) + (a + d):int`)] THEN
1594 REWRITE_TAC[INT_ADD_LINV, INT_ADD_LID]
1595QED
1596
1597Theorem INT_EQ_SUB_LADD:
1598 !x y z:int. (x = y - z) = (x + z = y)
1599Proof
1600 REPEAT GEN_TAC THEN (SUBST1_TAC o SYM o C SPECL INT_EQ_RADD)
1601 [Term `x:int`, Term `y - z:int`, Term `z:int`]
1602 THEN REWRITE_TAC[INT_SUB_ADD]
1603QED
1604
1605Theorem INT_EQ_SUB_RADD:
1606 !x y z:int. (x - y = z) = (x = z + y)
1607Proof
1608 REPEAT GEN_TAC THEN CONV_TAC(SUB_CONV(ONCE_DEPTH_CONV SYM_CONV))
1609 THEN
1610 MATCH_ACCEPT_TAC INT_EQ_SUB_LADD
1611QED
1612
1613Theorem INT_SUB:
1614 !n m. m <= n ==> (&n - &m = &(n - m))
1615Proof
1616 SIMP_TAC int_ss [INT_EQ_SUB_RADD, INT_ADD, INT_INJ]
1617QED
1618
1619Theorem INT_SUB_SUB2:
1620 !x y:int. x - (x - y) = y
1621Proof
1622 REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[GSYM INT_NEGNEG] THEN
1623 AP_TERM_TAC THEN REWRITE_TAC[INT_NEG_SUB, INT_SUB_SUB]
1624QED
1625
1626Theorem INT_ADD_SUB2:
1627 !x y:int. x - (x + y) = ~y
1628Proof
1629 REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[GSYM INT_NEG_SUB] THEN
1630 AP_TERM_TAC THEN REWRITE_TAC[INT_ADD_SUB]
1631QED
1632
1633Theorem INT_EQ_LMUL2:
1634 !x y z:int. ~(x = 0) ==> ((y = z) = (x * y = x * z))
1635Proof
1636 REPEAT GEN_TAC THEN DISCH_TAC THEN
1637 MP_TAC(SPECL [Term `x:int`, Term `y:int`,
1638 Term `z:int`] INT_EQ_LMUL) THEN
1639 ASM_REWRITE_TAC[] THEN DISCH_THEN SUBST_ALL_TAC
1640 THEN REFL_TAC
1641QED
1642
1643Theorem INT_EQ_IMP_LE:
1644 !x y:int. (x = y) ==> x <= y
1645Proof
1646 REPEAT GEN_TAC THEN DISCH_THEN SUBST1_TAC THEN
1647 MATCH_ACCEPT_TAC INT_LE_REFL
1648QED
1649
1650Theorem INT_POS_NZ:
1651 !x:int. 0 < x ==> ~(x = 0)
1652Proof
1653 GEN_TAC THEN DISCH_THEN(ASSUME_TAC o MATCH_MP INT_LT_IMP_NE)
1654 THEN
1655 CONV_TAC(RAND_CONV SYM_CONV) THEN POP_ASSUM ACCEPT_TAC
1656QED
1657
1658Theorem INT_EQ_RMUL_IMP:
1659 !x y z:int. ~(z = 0) /\ (x * z = y * z) ==> (x = y)
1660Proof
1661 REPEAT GEN_TAC
1662 THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
1663 ASM_REWRITE_TAC[INT_EQ_RMUL]
1664QED
1665
1666Theorem INT_EQ_LMUL_IMP:
1667 !x y z:int. ~(x = 0) /\ (x * y = x * z) ==> (y = z)
1668Proof
1669 ONCE_REWRITE_TAC[INT_MUL_SYM]
1670 THEN MATCH_ACCEPT_TAC INT_EQ_RMUL_IMP
1671QED
1672
1673Theorem INT_DIFFSQ:
1674 !x y:int. (x + y) * (x - y) = (x * x) - (y * y)
1675Proof
1676 REPEAT GEN_TAC THEN
1677 REWRITE_TAC[INT_LDISTRIB, INT_RDISTRIB, int_sub,
1678 GSYM INT_ADD_ASSOC] THEN
1679 ONCE_REWRITE_TAC[jrhUtils.AC(INT_ADD_ASSOC,INT_ADD_SYM)
1680 (Term`a + (b + (c + d)) = (b + c) + (a + d):int`)] THEN
1681 REWRITE_TAC[INT_ADD_LID_UNIQ, GSYM INT_NEG_RMUL] THEN
1682 REWRITE_TAC[INT_LNEG_UNIQ] THEN AP_TERM_TAC THEN
1683 MATCH_ACCEPT_TAC INT_MUL_SYM
1684QED
1685
1686Theorem INT_POSSQ:
1687 !x:int. 0 < x*x <=> ~(x = 0)
1688Proof
1689 GEN_TAC THEN REWRITE_TAC[GSYM INT_NOT_LE]
1690 THEN AP_TERM_TAC THEN EQ_TAC THENL
1691 [DISCH_THEN(MP_TAC o C CONJ (SPEC (Term `x:int`) INT_LE_SQUARE))
1692 THEN
1693 REWRITE_TAC[INT_LE_ANTISYM, INT_ENTIRE],
1694 DISCH_THEN SUBST1_TAC
1695 THEN REWRITE_TAC[INT_MUL_LZERO, INT_LE_REFL]]
1696QED
1697
1698Theorem INT_SUMSQ:
1699 !x y:int. ((x * x) + (y * y) = 0) <=> (x = 0) /\ (y = 0)
1700Proof
1701 REPEAT GEN_TAC THEN EQ_TAC THENL
1702 [CONV_TAC CONTRAPOS_CONV THEN REWRITE_TAC[DE_MORGAN_THM] THEN
1703 DISCH_THEN DISJ_CASES_TAC THEN MATCH_MP_TAC INT_POS_NZ THENL
1704 [MATCH_MP_TAC INT_LTE_ADD, MATCH_MP_TAC INT_LET_ADD] THEN
1705 ASM_REWRITE_TAC[INT_POSSQ, INT_LE_SQUARE],
1706 DISCH_TAC THEN ASM_REWRITE_TAC[INT_MUL_LZERO, INT_ADD_RID]]
1707QED
1708
1709Theorem INT_EQ_NEG[simp]: !x y:int. (~x = ~y) = (x = y)
1710Proof
1711 REPEAT GEN_TAC THEN
1712 REWRITE_TAC[GSYM INT_LE_ANTISYM, INT_LE_NEG] THEN
1713 MATCH_ACCEPT_TAC CONJ_SYM
1714QED
1715
1716Theorem int_eq_calculate[simp]:
1717 !n m. ((&n = ~&m) <=> (n = 0) /\ (m = 0)) /\
1718 ((~&n = &m) <=> (n = 0) /\ (m = 0))
1719Proof
1720 Induct THENL [
1721 SIMP_TAC int_ss [INT_NEG_0, INT_INJ, GSYM INT_NEG_EQ],
1722 SIMP_TAC int_ss [INT] THEN GEN_TAC THEN CONJ_TAC THENL [
1723 SIMP_TAC int_ss [GSYM INT_EQ_SUB_LADD, int_sub, GSYM INT_NEG_ADD] THEN
1724 ASM_SIMP_TAC int_ss [INT_ADD],
1725 SIMP_TAC int_ss [INT_NEG_ADD, GSYM INT_EQ_SUB_LADD] THEN
1726 SIMP_TAC int_ss [int_sub] THEN
1727 ASM_SIMP_TAC int_ss [INT_NEGNEG, INT_ADD]
1728 ]
1729 ]
1730QED
1731
1732Theorem INT_LT_CALCULATE:
1733 !n m. (&n:int < &m <=> n < m) /\ (~&n < ~&m <=> m < n) /\
1734 (~&n < &m <=> ~(n = 0) \/ ~(m = 0)) /\ (&n < ~&m <=> F)
1735Proof
1736 SIMP_TAC int_ss [INT_LT, INT_LT_NEG] THEN
1737 Induct THENL [
1738 SIMP_TAC int_ss [INT_NEG_0, INT_LT, INT_NEG_GT0],
1739 GEN_TAC THEN CONJ_TAC THENL [
1740 SIMP_TAC int_ss [INT, INT_NEG_ADD, INT_LT_ADDNEG2] THEN
1741 ASM_SIMP_TAC int_ss [INT_ADD],
1742 SIMP_TAC int_ss [INT, INT_LT_ADD_SUB, int_sub, GSYM INT_NEG_ADD] THEN
1743 ASM_SIMP_TAC int_ss [INT_ADD]
1744 ]
1745 ]
1746QED
1747
1748
1749
1750(*--------------------------------------------------------------------------*)
1751(* A nice proof that the positive integers are a copy of the natural *)
1752(* numbers (replacing a nasty hack which poked under the quotient). *)
1753(*--------------------------------------------------------------------------*)
1754
1755val _ = print "Proving +ve integers are a copy of natural numbers\n"
1756
1757Theorem NUM_POSINT:
1758 !i. 0 <= i ==> ?!n. i = &n
1759Proof
1760 GEN_TAC THEN DISCH_TAC THEN
1761 CONV_TAC EXISTS_UNIQUE_CONV THEN
1762 CONJ_TAC THEN POP_ASSUM MP_TAC THENL
1763 [ REWRITE_TAC[int_le, GSYM INT_0, NUM_POSINT_EX],
1764 REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC THEN
1765 ASM_REWRITE_TAC[INT_INJ]
1766 ]
1767QED
1768
1769Theorem NUM_POSINT_EXISTS:
1770 !i. 0 <= i ==> ?n. i = &n
1771Proof
1772 PROVE_TAC [SIMP_RULE bool_ss [EXISTS_UNIQUE_DEF] NUM_POSINT]
1773QED
1774
1775Theorem NUM_NEGINT_EXISTS:
1776 !i. i <= 0 ==> ?n. i = ~&n
1777Proof
1778 PROVE_TAC [NUM_POSINT_EXISTS, INT_NEG_LE0, INT_NEG_EQ]
1779QED
1780
1781Theorem INT_NUM_CASES:
1782 !p. (?n. (p = &n) /\ ~(n = 0)) \/ (?n. (p = ~&n) /\ ~(n = 0)) \/
1783 (p = 0)
1784Proof
1785 GEN_TAC THEN Cases_on `0 <= p` THENL [
1786 Cases_on `p = 0` THENL [
1787 ASM_SIMP_TAC int_ss [],
1788 PROVE_TAC [NUM_POSINT_EXISTS]
1789 ],
1790 `?n. p = ~&n` by PROVE_TAC [NUM_NEGINT_EXISTS, INT_NOT_LE, INT_LE_LT] THEN
1791 POP_ASSUM SUBST_ALL_TAC THEN
1792 FULL_SIMP_TAC int_ss [INT_EQ_NEG, INT_INJ, INT_NEG_GE0, NOT_LESS_EQUAL,
1793 INT_LE]
1794 ]
1795QED
1796val _ = TypeBase.export [
1797 TypeBasePure.mk_nondatatype_info (
1798 “:int”,
1799 {nchotomy = SOME INT_NUM_CASES,
1800 induction = NONE, encode = NONE, size = NONE}
1801 )
1802 ];
1803
1804
1805(* ----------------------------------------------------------------------
1806 Discreteness of <
1807 ---------------------------------------------------------------------- *)
1808
1809Theorem int_cases :
1810 !x:int. (?n. x = &n) \/ (?n. ~(n = 0) /\ (x = ~&n))
1811Proof
1812 PROVE_TAC [INT_NUM_CASES]
1813QED
1814
1815Theorem INT_DISCRETE:
1816 !x:int y. ~(x < y /\ y < x + 1)
1817Proof
1818 REPEAT GEN_TAC THEN
1819 `((?n. x = &n) \/ (?n. n <> 0 /\ (x = ~&n))) /\
1820 ((?m. y = &m) \/ (?m. m <> 0 /\ (y = ~&m)))`
1821 by PROVE_TAC [int_cases] THEN
1822 REPEAT VAR_EQ_TAC THENL [
1823 REWRITE_TAC [INT_ADD, INT_LT, LESS_LESS_SUC, GSYM ADD1],
1824
1825 REWRITE_TAC [INT_LT_CALCULATE],
1826
1827 ASM_REWRITE_TAC [INT_LT_CALCULATE] THEN
1828 `&m < ~&n + 1 <=> ~(~&n + 1) < ~&m` by REWRITE_TAC [INT_LT_NEG] THEN
1829 POP_ASSUM SUBST1_TAC THEN
1830 REWRITE_TAC [INT_NEG_ADD, INT_NEGNEG, GSYM int_sub] THEN
1831 SRW_TAC [numSimps.ARITH_ss][INT_SUB, INT_LT_CALCULATE],
1832
1833 REWRITE_TAC [INT_LT_CALCULATE] THEN
1834 `~&m < ~&n + 1 <=> ~(~&n + 1) < &m`
1835 by PROVE_TAC [INT_LT_NEG, INT_NEGNEG] THEN
1836 POP_ASSUM SUBST1_TAC THEN
1837 REWRITE_TAC [INT_NEG_ADD, INT_NEGNEG, GSYM int_sub] THEN
1838 SRW_TAC [numSimps.ARITH_ss][INT_SUB, INT_LT_CALCULATE]
1839 ]
1840QED
1841
1842Theorem INT_LE_LT1:
1843 x <= y <=> x < y + 1
1844Proof
1845 SRW_TAC [][EQ_IMP_THM] THENL [
1846 FULL_SIMP_TAC (srw_ss()) [INT_LE_LT, INT_LT_ADDR, INT_LT] THEN
1847 MATCH_MP_TAC INT_LT_TRANS THEN Q.EXISTS_TAC `y` THEN
1848 SRW_TAC [][INT_LT_ADDR, INT_LT],
1849
1850 SRW_TAC [][int_le] THEN PROVE_TAC [INT_DISCRETE]
1851 ]
1852QED
1853
1854Theorem INT_LT_LE1:
1855 x < y <=> x + 1 <= y
1856Proof
1857 SRW_TAC [][INT_LE_LT1, INT_LT_RADD]
1858QED
1859
1860(* |- !x y. x < y <=> x + 1 <= y *)
1861Theorem INT_LT_DISCRETE = Q.GENL [‘x’, ‘y’] INT_LT_LE1
1862
1863(* ------------------------------------------------------------------------ *)
1864(* More random theorems about "stuff" *)
1865(* ------------------------------------------------------------------------ *)
1866
1867Theorem INT_MUL_EQ_1:
1868 !x y. (x * y = 1) <=> (x = 1) /\ (y = 1) \/ (x = ~1) /\ (y = ~1)
1869Proof
1870 REPEAT GEN_TAC THEN
1871 Q.SPEC_THEN `x` STRIP_ASSUME_TAC INT_NUM_CASES THEN
1872 FIRST_X_ASSUM SUBST_ALL_TAC THEN
1873 SIMP_TAC (bool_ss ++ numSimps.ARITH_ss) [INT_MUL_LZERO, INT_INJ,
1874 int_eq_calculate] THEN
1875 Q.SPEC_THEN `y` STRIP_ASSUME_TAC INT_NUM_CASES THEN
1876 FIRST_X_ASSUM SUBST_ALL_TAC THEN
1877 SIMP_TAC (bool_ss ++ numSimps.ARITH_ss) [
1878 INT_MUL_LZERO, INT_INJ, INT_MUL_RZERO, int_eq_calculate,
1879 GSYM INT_NEG_RMUL, INT_MUL, GSYM INT_NEG_LMUL,
1880 INT_NEGNEG, INT_EQ_NEG]
1881QED
1882
1883(*--------------------------------------------------------------------------*)
1884(* Theorems about mapping both ways between :num and :int *)
1885(*--------------------------------------------------------------------------*)
1886
1887Definition Num[nocompute]:
1888 Num (i:int) = @n. if 0 <= i then i = &n else i = - &n
1889End
1890
1891Overload num_of_int[inferior] = “Num” (* from HOL Light *)
1892
1893(* NOTE: In HOL-Light, num_of_int is unspecified for negative integers:
1894 |- !x. num_of_int x = (@n. &n = x) (int.ml, line 2056)
1895 *)
1896Theorem num_of_int = Num
1897
1898Theorem NUM_OF_INT[simp,compute]:
1899 !n. Num(&n) = n
1900Proof
1901 GEN_TAC THEN REWRITE_TAC[Num, INT_INJ, INT_POS] THEN
1902 CONV_TAC(LAND_CONV(ONCE_DEPTH_CONV SYM_CONV)) THEN
1903 REWRITE_TAC[SELECT_REFL]
1904QED
1905
1906Theorem NUM_OF_NEG_INT[simp,compute]:
1907 !n. Num(-&n) = n
1908Proof
1909 GEN_TAC THEN
1910 REWRITE_TAC[Num, INT_INJ, INT_POS, INT_EQ_NEG] THEN
1911 Cases_on ‘0 <= -&n’ THEN ASM_REWRITE_TAC [] THEN
1912 CONV_TAC (RATOR_CONV (ONCE_REWRITE_CONV [EQ_SYM_EQ])) THEN
1913 REWRITE_TAC [SELECT_REFL] THEN
1914 POP_ASSUM MP_TAC THEN
1915 REWRITE_TAC [INT_NEG_GE0,INT_LE,LE] THEN
1916 STRIP_TAC THEN ASM_REWRITE_TAC [INT_NEG_0,INT_INJ] THEN
1917 REWRITE_TAC [SELECT_REFL]
1918QED
1919
1920Theorem INT_OF_NUM[simp]:
1921 !i. (&(Num i) = i) <=> 0 <= i
1922Proof
1923 GEN_TAC THEN EQ_TAC THEN1
1924 (DISCH_THEN(SUBST1_TAC o SYM) THEN MATCH_ACCEPT_TAC INT_POS) THEN
1925 DISCH_THEN(ASSUME_TAC o EXISTENCE o MATCH_MP NUM_POSINT) THEN
1926 REWRITE_TAC[Num] THEN CONV_TAC SYM_CONV THEN
1927 POP_ASSUM STRIP_ASSUME_TAC THEN
1928 ASM_REWRITE_TAC [INT_POS,INT_INJ] THEN
1929 CONV_TAC (RAND_CONV (ONCE_REWRITE_CONV [EQ_SYM_EQ])) THEN
1930 REWRITE_TAC [SELECT_REFL]
1931QED
1932
1933Theorem NUM_EQ0[simp]:
1934 Num i = 0 <=> i = 0
1935Proof
1936 Cases_on ‘i’ >> simp[]
1937QED
1938
1939Theorem Num_EQ:
1940 Num a = Num b <=> a=b \/ a=-b
1941Proof
1942 Cases_on ‘a’ >> Cases_on ‘b’ >> simp[]
1943QED
1944
1945Theorem Num_neg:
1946 Num (-a) = Num a
1947Proof
1948 Cases_on `a` >> gvs[]
1949QED
1950
1951Theorem LE_NUM_OF_INT:
1952 !n i. & n <= i ==> n <= Num i
1953Proof
1954 METIS_TAC [NUM_OF_INT, INT_OF_NUM, INT_LE_TRANS, INT_POS, INT_LE]
1955QED
1956
1957Theorem NUM_LT:
1958 0 <= x /\ 0 <= y ==> (Num x < Num y <=> x < y)
1959Proof
1960 map_every (fn q => Q.SPEC_THEN q strip_assume_tac INT_NUM_CASES) [‘x’, ‘y’] >>
1961 simp[INT_LE, INT_LT, INT_NEG_GE0]
1962QED
1963
1964(*----------------------------------------------------------------------*)
1965(* Define division *)
1966(*----------------------------------------------------------------------*)
1967
1968val _ = print "Integer division\n"
1969
1970Theorem int_div_exists0[local]:
1971 !i j. ?q. ~(j = 0) ==>
1972 (q = if 0 < j then
1973 if 0 <= i then &(Num i DIV Num j)
1974 else ~&(Num ~i DIV Num j) +
1975 (if Num ~i MOD Num j = 0 then 0 else ~1)
1976 else
1977 if 0 <= i then ~&(Num i DIV Num ~j) +
1978 (if Num i MOD Num ~j = 0 then 0 else ~1)
1979 else &(Num ~i DIV Num ~j))
1980Proof
1981 REPEAT GEN_TAC THEN REWRITE_TAC [IMP_DISJ_THM] THEN
1982 CONV_TAC EXISTS_OR_CONV THEN DISJ2_TAC THEN
1983 REWRITE_TAC [EXISTS_REFL]
1984QED
1985
1986val int_div_exists =
1987 CONV_RULE (BINDER_CONV SKOLEM_CONV THENC SKOLEM_CONV) int_div_exists0
1988
1989val int_div = new_specification ("int_div", ["int_div"], int_div_exists);
1990
1991val _ = set_fixity "/" (Infixl 600)
1992Overload "/" = Term`int_div`
1993
1994Theorem INT_DIV:
1995 !n m. ~(m = 0) ==> (&n / &m = &(n DIV m))
1996Proof
1997 SIMP_TAC int_ss [int_div, INT_LE, INT_LT, NUM_OF_INT, INT_INJ]
1998QED
1999
2000Theorem INT_DIV_NEG:
2001 !p q. ~(q = 0) ==> (p / ~q = ~p / q)
2002Proof
2003 REPEAT GEN_TAC THEN
2004 STRUCT_CASES_TAC (Q.SPEC `q` INT_NUM_CASES) THEN
2005 FULL_SIMP_TAC int_ss [INT_INJ, INT_NEG_EQ, INT_NEG_0, INT_NEGNEG] THEN
2006 ASM_SIMP_TAC int_ss [int_div, INT_INJ, INT_NEG_EQ, INT_NEG_0,
2007 INT_NEG_GT0, INT_LT, INT_NEG_GE0, INT_NEGNEG,
2008 NUM_OF_INT] THEN
2009 STRUCT_CASES_TAC (Q.SPEC `p` INT_NUM_CASES) THEN
2010 FULL_SIMP_TAC int_ss [int_div, INT_NEG_EQ0, INT_INJ, INT_NEG_EQ, INT_NEG_0,
2011 INT_NEG_GT0, INT_LT, INT_NEG_GE0, INT_NEGNEG,
2012 NUM_OF_INT, INT_LE, INT_NEG_LE0, ZERO_DIV,
2013 ZERO_MOD, INT_ADD_RID]
2014QED
2015
2016Theorem INT_DIV_1:
2017 !p:int. p / 1 = p
2018Proof
2019 GEN_TAC THEN Cases_on `0 <= p` THENL [
2020 (* p positive *)
2021 `?n. p = &n` by PROVE_TAC [NUM_POSINT_EXISTS] THEN
2022 POP_ASSUM SUBST_ALL_TAC THEN
2023 SIMP_TAC int_ss [DIV_ONE, ONE, INT_DIV],
2024 (* p negative *)
2025 `?n. p = ~&n` by PROVE_TAC [NUM_NEGINT_EXISTS, INT_NOT_LE, INT_LE_LT] THEN
2026 POP_ASSUM SUBST_ALL_TAC THEN
2027 SIMP_TAC (int_ss ++ COND_elim_ss) [INT_INJ, INT_EQ_NEG, int_div, ONE,
2028 DIV_ONE, INT_LT, INT_NEG_GE0, INT_LE,
2029 INT_NEGNEG, NUM_OF_INT, INT_NEG_0, MOD_ONE,
2030 INT_ADD_RID, GSYM INT_NEG_EQ]
2031 ]
2032QED
2033
2034Theorem INT_DIV_0:
2035 !q. ~(q = 0) ==> (0 / q = 0)
2036Proof
2037 GEN_TAC THEN STRUCT_CASES_TAC (Q.SPEC `q` INT_NUM_CASES) THEN
2038 ASM_SIMP_TAC int_ss [INT_NEG_EQ0, INT_INJ, INT_DIV_NEG, INT_DIV,
2039 INT_NEG_0, ZERO_DIV, GSYM NOT_ZERO_LT_ZERO]
2040QED
2041
2042Theorem INT_DIV_ID:
2043 !p:int. ~(p = 0) ==> (p / p = 1)
2044Proof
2045 GEN_TAC THEN Cases_on `0 <= p` THENL [
2046 (* p positive *)
2047 `?n. p = &n` by PROVE_TAC [NUM_POSINT_EXISTS] THEN
2048 ASM_SIMP_TAC int_ss [INT_INJ, INT_DIV, DIVMOD_ID, NOT_ZERO_LT_ZERO],
2049 (* p negative *)
2050 `?n. p = ~&n` by PROVE_TAC [INT_NOT_LE, NUM_NEGINT_EXISTS, INT_LE_LT] THEN
2051 ASM_SIMP_TAC int_ss [INT_NEG_EQ0, INT_NEGNEG, int_div,
2052 NUM_OF_INT, INT_NEG_GT0, INT_INJ, INT_LT,
2053 DIVMOD_ID, NOT_ZERO_LT_ZERO]
2054 ]
2055QED
2056
2057(*----------------------------------------------------------------------*)
2058(* Define the appropriate modulus function for int_div *)
2059(*----------------------------------------------------------------------*)
2060
2061val _ = print "Integer modulus\n"
2062
2063Theorem int_mod_exists0[local]:
2064 !i j. ?r. ~(j = 0) ==> (r = i - i / j * j)
2065Proof
2066 REPEAT GEN_TAC THEN REWRITE_TAC [IMP_DISJ_THM] THEN
2067 CONV_TAC EXISTS_OR_CONV THEN DISJ2_TAC THEN
2068 REWRITE_TAC [EXISTS_REFL]
2069QED
2070val int_mod_exists =
2071 CONV_RULE (BINDER_CONV SKOLEM_CONV THENC SKOLEM_CONV) int_mod_exists0
2072
2073
2074val int_mod = new_specification ("int_mod",["int_mod"],int_mod_exists);
2075
2076val _ = set_fixity "%" (Infixl 650)
2077Overload "%" = “int_mod”
2078
2079Theorem little_lemma[local]:
2080 !x y z. ~x < y + ~z <=> z < y + x
2081Proof
2082 REWRITE_TAC [GSYM int_sub, INT_LT_SUB_LADD] THEN
2083 REPEAT GEN_TAC THEN
2084 CONV_TAC (LHS_CONV (LAND_CONV (REWR_CONV INT_ADD_COMM))) THEN
2085 REWRITE_TAC [GSYM int_sub, INT_LT_SUB_RADD]
2086QED
2087
2088Theorem ll2[local]:
2089 !x y. (x + ~y <= 0) = (x <= y)
2090Proof
2091 REWRITE_TAC [GSYM int_sub, INT_LE_SUB_RADD, INT_ADD_LID]
2092QED
2093
2094
2095Theorem INT_MOD_BOUNDS:
2096 !p q. ~(q = 0) ==> if q < 0 then q < p % q /\ p % q <= 0
2097 else 0 <= p % q /\ p % q < q
2098Proof
2099 REPEAT STRIP_TAC THEN ASM_SIMP_TAC int_ss [int_mod] THEN
2100 STRIP_ALL_THEN ASSUME_TAC (Q.SPEC `q` INT_NUM_CASES) THEN
2101 FIRST_X_ASSUM SUBST_ALL_TAC THENL [
2102 ASM_SIMP_TAC int_ss [INT_LT, INT_SUB_LE, INT_LT_SUB_RADD],
2103 ASM_SIMP_TAC int_ss [INT_NEG_LT0, INT_LT],
2104 FULL_SIMP_TAC bool_ss []
2105 ] THEN FULL_SIMP_TAC bool_ss [INT_INJ, INT_NEG_EQ0] THEN
2106 STRUCT_CASES_TAC (Q.SPEC `p` INT_NUM_CASES) THEN
2107 ASM_SIMP_TAC int_ss [INT_ADD, INT_DIV, INT_MUL, INT_LE, INT_LT,
2108 INT_DIV_NEG, INT_SUB_LZERO, INT_LT_NEG,
2109 INT_DIV_0, INT_INJ, ZERO_DIV, GSYM NOT_ZERO_LT_ZERO,
2110 INT_NEG_0, INT_MUL_LZERO, INT_LE, INT_NEG_LT0,
2111 INT_NEGNEG] THEN
2112 Q.ABBREV_TAC `p = n'` THEN POP_ASSUM (K ALL_TAC)
2113 THENL [
2114 ALL_TAC,
2115 ASM_SIMP_TAC int_ss [int_div, INT_INJ, INT_LT, INT_NEG_GE0, INT_LE,
2116 NUM_OF_INT, INT_NEGNEG] THEN
2117 COND_CASES_TAC THEN
2118 ASM_SIMP_TAC int_ss [INT_RDISTRIB, INT_MUL_LZERO, INT_ADD_RID,
2119 GSYM INT_NEG_LMUL, INT_LE_NEG, INT_LE, INT_MUL,
2120 little_lemma, INT_ADD, INT_LT, GSYM INT_NEG_ADD,
2121 GSYM INT_NEG_RMUL, INT_NEGNEG, int_sub],
2122 ASM_SIMP_TAC int_ss [int_div, INT_INJ, INT_LT, INT_NEG_GE0, INT_LE,
2123 NUM_OF_INT, INT_NEGNEG] THEN
2124 COND_CASES_TAC THEN
2125 ASM_SIMP_TAC int_ss [INT_RDISTRIB, INT_MUL_LZERO, INT_ADD_RID,
2126 GSYM INT_NEG_LMUL, INT_LE_NEG, INT_LE, INT_MUL,
2127 little_lemma, INT_ADD, INT_LT, GSYM INT_NEG_ADD,
2128 GSYM INT_NEG_RMUL, INT_NEGNEG, int_sub, ll2],
2129 SIMP_TAC int_ss [GSYM INT_NEG_RMUL, INT_SUB_NEG2, INT_MUL,
2130 INT_LE_SUB_RADD, INT_ADD_LID, INT_LE_NEG, INT_LE] THEN
2131 SIMP_TAC int_ss [int_sub, little_lemma, INT_ADD, INT_LT]
2132 ] THEN
2133 `(p = p DIV n * n + p MOD n) /\ p MOD n < n` by
2134 PROVE_TAC [DIVISION, NOT_ZERO_LT_ZERO] THEN
2135 Q.ABBREV_TAC `q = p DIV n` THEN POP_ASSUM (K ALL_TAC) THEN
2136 Q.ABBREV_TAC `r = p MOD n` THEN POP_ASSUM (K ALL_TAC) THEN
2137 ASM_SIMP_TAC int_ss []
2138QED
2139
2140Theorem INT_DIVISION:
2141 !q. ~(q = 0) ==> !p. (p = p / q * q + p % q) /\
2142 if q < 0 then q < p % q /\ p % q <= 0
2143 else 0 <= p % q /\ p % q < q
2144Proof
2145 REPEAT STRIP_TAC THENL [
2146 ASM_SIMP_TAC int_ss [int_mod, int_sub] THEN
2147 PROVE_TAC [INT_EQ_SUB_LADD, INT_ADD_COMM, INT_ADD_ASSOC, int_sub],
2148 PROVE_TAC [INT_MOD_BOUNDS]
2149 ]
2150QED
2151
2152Theorem INT_MOD:
2153 !n m. ~(m = 0) ==> (&n % &m = &(n MOD m))
2154Proof
2155 SIMP_TAC int_ss [int_mod, INT_INJ, INT_DIV, INT_MUL, INT_EQ_SUB_RADD,
2156 INT_ADD, INT_INJ] THEN
2157 PROVE_TAC [ADD_COMM, DIVISION, NOT_ZERO_LT_ZERO, MULT_COMM]
2158QED
2159
2160Theorem INT_MOD_NEG:
2161 !p q. ~(q = 0) ==> (p % ~q = ~(~p % q))
2162Proof
2163 REPEAT GEN_TAC THEN
2164 STRUCT_CASES_TAC (Q.SPEC `q` INT_NUM_CASES) THEN
2165 FULL_SIMP_TAC int_ss [INT_INJ, INT_NEGNEG, int_mod, INT_NEG_EQ,
2166 INT_NEG_0, INT_DIV_NEG, INT_NEG_ADD,
2167 GSYM INT_NEG_LMUL, GSYM INT_NEG_RMUL, int_sub,
2168 INT_NEG_EQ0]
2169QED
2170
2171Theorem INT_MOD0:
2172 !p. ~(p = 0) ==> (0 % p = 0)
2173Proof
2174 GEN_TAC THEN
2175 Cases_on `0 <= p` THENL [
2176 `?n. p = &n` by PROVE_TAC [NUM_POSINT_EXISTS] THEN
2177 POP_ASSUM SUBST_ALL_TAC THEN
2178 SIMP_TAC int_ss [INT_MOD, INT_INJ, ZERO_MOD],
2179 `?n. p = ~&n` by PROVE_TAC [NUM_NEGINT_EXISTS, INT_NOT_LE, INT_LE_LT] THEN
2180 POP_ASSUM SUBST_ALL_TAC THEN
2181 SIMP_TAC int_ss [INT_MOD_NEG, INT_NEG_EQ0, INT_MOD, INT_INJ, ZERO_MOD,
2182 INT_NEG_0]
2183 ]
2184QED
2185
2186Theorem INT_DIV_MUL_ID:
2187 !p q. ~(q = 0) /\ (p % q = 0) ==> (p / q * q = p)
2188Proof
2189 REPEAT STRIP_TAC THEN
2190 `p = p/q * q + p % q` by PROVE_TAC [INT_DIVISION] THEN
2191 `p = p / q * q` by PROVE_TAC [INT_ADD_RID] THEN
2192 PROVE_TAC []
2193QED
2194
2195Theorem lessmult_lemma[local]:
2196 !x y:num. x * y < y ==> (x = 0)
2197Proof
2198 Induct THEN ASM_SIMP_TAC int_ss [MULT_CLAUSES]
2199QED
2200
2201Theorem negcase[local]:
2202 !q n m.
2203 m < n /\ ~(q = 0) ==> ((~&q * &n + &m) / &n = ~ &q)
2204Proof
2205 REPEAT STRIP_TAC THEN
2206 `m < q * n` by
2207 PROVE_TAC [NOT_LESS_EQUAL, lessmult_lemma, LESS_LESS_EQ_TRANS] THEN
2208 Q_TAC SUFF_TAC `(&m + ~&q * &n) / &n = ~&q`
2209 THEN1 SRW_TAC [][INT_ADD_COMM] THEN
2210 REWRITE_TAC [GSYM int_sub, GSYM INT_NEG_LMUL] THEN
2211 ONCE_REWRITE_TAC [GSYM INT_NEG_SUB] THEN
2212 ASM_SIMP_TAC int_ss [INT_SUB, INT_MUL, INT_LE,
2213 ARITH_PROVE ``x:num < y ==> x <= y``] THEN
2214 ASM_SIMP_TAC int_ss [int_div, INT_INJ, INT_LT, INT_NEG_GE0, INT_LE,
2215 INT_NEGNEG, NUM_OF_INT, INT_EQ_NEG] THEN
2216 COND_CASES_TAC THEN
2217 ASM_SIMP_TAC int_ss [INT_INJ, INT_LT, INT_NEG_GE0, INT_LE,
2218 INT_NEGNEG, NUM_OF_INT, INT_EQ_NEG,
2219 INT_ADD_RID, GSYM INT_NEG_ADD, INT_ADD]
2220 THENL [
2221 Q.MATCH_ABBREV_TAC `tot DIV n = q` THEN
2222 Q.ABBREV_TAC `q' = tot DIV n` THEN
2223 Q.ABBREV_TAC `r = tot MOD n` THEN
2224 `0 < n` by ASM_SIMP_TAC int_ss [] THEN
2225 `(tot = q' * n + r) /\ r < n` by METIS_TAC [DIVISION] THEN
2226 `q * n = q' * n + m` by ASM_SIMP_TAC int_ss [Abbr`tot`] THEN
2227 `(q * n) DIV n = (q' * n + m) DIV n` by SRW_TAC [][] THEN
2228 rpt VAR_EQ_TAC THEN
2229 FULL_SIMP_TAC (srw_ss()) [ASSUME ``0n < n``, MULT_DIV,
2230 ASSUME ``(m:num) < n``, DIV_MULT],
2231 Q_TAC SUFF_TAC `(q * n - m) DIV n = q - 1` THEN1
2232 ASM_SIMP_TAC int_ss [] THEN
2233 MATCH_MP_TAC DIV_UNIQUE THEN Q.EXISTS_TAC `n - m` THEN
2234 `n <= q * n` by PROVE_TAC [lessmult_lemma, NOT_LESS_EQUAL] THEN
2235 ASM_SIMP_TAC int_ss [RIGHT_SUB_DISTRIB, MULT_CLAUSES,
2236 ARITH_PROVE ``x:num < y ==> x <= y``,
2237 GSYM LESS_EQ_ADD_SUB, SUB_ADD] THEN
2238 Q_TAC SUFF_TAC `~(m = 0)` THEN1 ASM_SIMP_TAC int_ss [] THEN
2239 DISCH_THEN SUBST_ALL_TAC THEN
2240 FULL_SIMP_TAC bool_ss [SUB_0] THEN PROVE_TAC [MOD_EQ_0, MULT_COMM]
2241 ]
2242QED
2243
2244Theorem INT_DIV_UNIQUE:
2245 !i j q. (?r. (i = q * j + r) /\
2246 if j < 0 then j < r /\ r <= 0 else 0 <= r /\ r < j) ==>
2247 (i / j = q)
2248Proof
2249 REPEAT GEN_TAC THEN DISCH_THEN (STRIP_THM_THEN MP_TAC) THEN
2250 STRUCT_CASES_TAC (Q.SPEC `j` INT_NUM_CASES) THEN
2251 FULL_SIMP_TAC int_ss [INT_INJ, INT_MUL_RZERO, INT_LT, INT_ADD_LID,
2252 INT_NEG_LT0]
2253 THENL [
2254 REPEAT STRIP_TAC THEN `?m. r = &m` by PROVE_TAC [NUM_POSINT_EXISTS] THEN
2255 REPEAT (FIRST_X_ASSUM SUBST_ALL_TAC) THEN
2256 FULL_SIMP_TAC int_ss [INT_LT, INT_LE] THEN
2257 STRUCT_CASES_TAC (Q.SPEC `q` INT_NUM_CASES) THENL [
2258 FULL_SIMP_TAC int_ss [INT_MUL, INT_ADD, INT_DIV, INT_INJ] THEN
2259 PROVE_TAC [ADD_COMM, DIV_UNIQUE, MULT_COMM],
2260 PROVE_TAC [negcase],
2261 ASM_SIMP_TAC int_ss [INT_MUL_LZERO, INT_ADD_LID, INT_DIV, INT_INJ,
2262 LESS_DIV_EQ_ZERO]
2263 ],
2264 REPEAT STRIP_TAC THEN
2265 `?m. r = ~&m` by PROVE_TAC [NUM_NEGINT_EXISTS] THEN
2266 REPEAT (FIRST_X_ASSUM SUBST_ALL_TAC) THEN
2267 FULL_SIMP_TAC int_ss [INT_DIV_NEG, INT_INJ, INT_NEG_EQ0,
2268 INT_NEG_LE0, INT_LT_NEG, INT_LE, INT_LT] THEN
2269 STRUCT_CASES_TAC (Q.SPEC `q` INT_NUM_CASES) THENL [
2270 ASM_SIMP_TAC int_ss [INT_NEG_RMUL, INT_NEGNEG, INT_NEG_ADD, INT_DIV,
2271 INT_INJ, INT_ADD, INT_MUL] THEN
2272 PROVE_TAC [DIV_UNIQUE, ADD_COMM, MULT_COMM],
2273 ASM_SIMP_TAC bool_ss [INT_NEG_MUL2, negcase, INT_NEG_ADD, INT_NEGNEG,
2274 INT_NEG_LMUL],
2275 ASM_SIMP_TAC int_ss [INT_MUL_LZERO, INT_ADD_LID, INT_DIV, INT_INJ,
2276 LESS_DIV_EQ_ZERO, INT_NEGNEG]
2277 ],
2278 PROVE_TAC [INT_LET_TRANS, INT_LT_REFL]
2279 ]
2280QED
2281
2282Theorem INT_MOD_UNIQUE:
2283 !i j m.
2284 (?q. (i = q * j + m) /\ if j < 0 then j < m /\ m <= 0
2285 else 0 <= m /\ m < j) ==>
2286 (i % j = m)
2287Proof
2288 REPEAT STRIP_TAC THEN FIRST_X_ASSUM SUBST_ALL_TAC THEN
2289 `~(j = 0)` by (DISCH_THEN SUBST_ALL_TAC THEN
2290 FULL_SIMP_TAC int_ss [INT_LT_REFL] THEN
2291 PROVE_TAC [INT_LET_TRANS, INT_LT_REFL]) THEN
2292 ASM_SIMP_TAC int_ss [int_mod] THEN
2293 `(q * j + m) / j = q` by PROVE_TAC [INT_DIV_UNIQUE] THEN
2294 ASM_SIMP_TAC bool_ss [INT_ADD_SUB]
2295QED
2296
2297Theorem INT_MOD_ID:
2298 !i. ~(i = 0) ==> (i % i = 0)
2299Proof
2300 REPEAT STRIP_TAC THEN MATCH_MP_TAC INT_MOD_UNIQUE THEN
2301 Q.EXISTS_TAC `1` THEN
2302 SIMP_TAC bool_ss [INT_MUL_LID, INT_ADD_RID, INT_LE_REFL] THEN
2303 PROVE_TAC [INT_LT_NEGTOTAL, INT_NEG_GT0]
2304QED
2305
2306Theorem INT_MOD_COMMON_FACTOR:
2307 !p. ~(p = 0) ==> !q. (q * p) % p = 0
2308Proof
2309 REPEAT STRIP_TAC THEN
2310 MATCH_MP_TAC INT_MOD_UNIQUE THEN
2311 SIMP_TAC int_ss [INT_ADD_RID, INT_LE_REFL] THEN
2312 PROVE_TAC [INT_LT_NEGTOTAL, INT_NEG_GT0]
2313QED
2314
2315Theorem INT_DIV_LMUL:
2316 !i j. ~(i = 0) ==> ((i * j) / i = j)
2317Proof
2318 REPEAT STRIP_TAC THEN MATCH_MP_TAC INT_DIV_UNIQUE THEN
2319 Q.EXISTS_TAC `0` THEN
2320 ASM_SIMP_TAC int_ss [INT_MUL_COMM, INT_LE_REFL, INT_ADD_RID] THEN
2321 PROVE_TAC [INT_LT_NEGTOTAL, INT_NEG_GT0]
2322QED
2323
2324Theorem INT_DIV_RMUL:
2325 !i j. ~(i = 0) ==> (j * i / i = j)
2326Proof
2327 PROVE_TAC [INT_DIV_LMUL, INT_MUL_COMM]
2328QED
2329
2330Theorem INT_MOD_EQ0:
2331 !q. ~(q = 0) ==> !p. (p % q = 0) = (?k. p = k * q)
2332Proof
2333 REPEAT STRIP_TAC THEN EQ_TAC THEN STRIP_TAC THENL [
2334 Q.PAT_ASSUM `~(q = 0)` (ASSUME_TAC o Q.SPEC `p` o
2335 MATCH_MP INT_DIVISION) THEN
2336 PROVE_TAC [INT_ADD_RID],
2337 MATCH_MP_TAC INT_MOD_UNIQUE THEN
2338 ASM_SIMP_TAC int_ss [INT_LE_REFL, INT_EQ_RMUL, INT_ADD_RID] THEN
2339 PROVE_TAC [INT_LT_NEGTOTAL, INT_NEG_GT0]
2340 ]
2341QED
2342
2343Theorem INT_MUL_DIV:
2344 !p:int q k. ~(q = 0) /\ (p % q = 0) ==>
2345 ((k * p) / q = k * (p / q))
2346Proof
2347 REPEAT STRIP_TAC THEN MATCH_MP_TAC INT_DIV_UNIQUE THEN
2348 `?m. p = m * q` by PROVE_TAC [INT_MOD_EQ0] THEN
2349 `p / q = m` by PROVE_TAC [INT_DIV_RMUL] THEN
2350 POP_ASSUM SUBST_ALL_TAC THEN POP_ASSUM SUBST_ALL_TAC THEN
2351 Q.EXISTS_TAC `0` THEN
2352 SIMP_TAC int_ss [INT_MUL_ASSOC, INT_ADD_RID, INT_LE_REFL] THEN
2353 PROVE_TAC [INT_LT_NEGTOTAL, INT_NEG_GT0]
2354QED
2355
2356Theorem INT_ADD_DIV:
2357 !i j k. ~(k = 0) /\ ((i % k = 0) \/ (j % k = 0)) ==>
2358 ((i + j) / k = i / k + j / k)
2359Proof
2360 REPEAT STRIP_TAC THENL [
2361 `?m. i = m * k` by PROVE_TAC [INT_MOD_EQ0] THEN
2362 ASM_SIMP_TAC int_ss [INT_DIV_RMUL] THEN
2363 MATCH_MP_TAC INT_DIV_UNIQUE THEN
2364 SIMP_TAC int_ss [INT_RDISTRIB, GSYM INT_ADD_ASSOC, INT_EQ_LADD] THEN
2365 Q.EXISTS_TAC `j % k` THEN PROVE_TAC [INT_DIVISION],
2366 `?m. j = m * k` by PROVE_TAC [INT_MOD_EQ0] THEN
2367 ASM_SIMP_TAC int_ss [INT_DIV_RMUL] THEN
2368 MATCH_MP_TAC INT_DIV_UNIQUE THEN Q.EXISTS_TAC `i % k` THEN
2369 CONV_TAC (LAND_CONV (RAND_CONV (REWR_CONV INT_ADD_COMM))) THEN
2370 ASM_SIMP_TAC int_ss [INT_RDISTRIB, INT_ADD_ASSOC, INT_EQ_RADD,
2371 INT_DIVISION] THEN
2372 PROVE_TAC [INT_DIVISION, INT_ADD_COMM]
2373 ]
2374QED
2375
2376Theorem INT_MOD_ADD0[local]:
2377 0 <= r /\ r < k ==> ((q * k + r) % k = r)
2378Proof
2379 STRIP_TAC THEN
2380 MATCH_MP_TAC INT_MOD_UNIQUE THEN
2381 Q.EXISTS_TAC `q` THEN
2382 METIS_TAC [INT_LET_TRANS, INT_LT_TRANS, INT_LT_REFL]
2383QED
2384
2385Theorem INT_MOD_ADD1[local]:
2386 k < r /\ r <= 0 ==> ((q * k + r) % k = r)
2387Proof
2388 STRIP_TAC THEN
2389 MATCH_MP_TAC INT_MOD_UNIQUE THEN
2390 Q.EXISTS_TAC `q` THEN
2391 METIS_TAC [INT_LTE_TRANS]
2392QED
2393
2394Theorem INT_MOD_ADD_MULTIPLES:
2395 ~(k = 0) ==> ((q * k + r) % k = r % k)
2396Proof
2397 STRIP_TAC THEN
2398 `0 < k \/ k < 0` by METIS_TAC [INT_LT_TRANS, INT_LT_TOTAL] THENL [
2399 `(r = r / k * k + r % k) /\ 0 <= r % k /\ r % k < k`
2400 by METIS_TAC [INT_DIVISION, INT_LT_TRANS, INT_LT_REFL] THEN
2401 Q.ABBREV_TAC `R = r % k` THEN
2402 Q.ABBREV_TAC `Q = r / k` THEN
2403 Q_TAC SUFF_TAC `q * k + r = (q + Q) * k + R` THEN1
2404 SRW_TAC [][INT_MOD_ADD0] THEN
2405 SRW_TAC [][INT_RDISTRIB, INT_ADD_ASSOC],
2406
2407 `(r = r / k * k + r % k) /\ k < r % k /\ r % k <= 0`
2408 by METIS_TAC [INT_DIVISION] THEN
2409 Q.ABBREV_TAC `R = r % k` THEN
2410 Q.ABBREV_TAC `Q = r / k` THEN
2411 Q_TAC SUFF_TAC `q * k + r = (q + Q) * k + R` THEN1
2412 SRW_TAC [][INT_MOD_ADD1] THEN
2413 SRW_TAC [][INT_RDISTRIB, INT_ADD_ASSOC]
2414 ]
2415QED
2416
2417Theorem INT_MOD_NEG_NUMERATOR:
2418 ~(k = 0) ==> (~x % k = (k - x) % k)
2419Proof
2420 METIS_TAC [int_sub, INT_MUL_LID, INT_MOD_ADD_MULTIPLES]
2421QED
2422
2423Theorem INT_MOD_PLUS:
2424 ~(k = 0) ==> ((i % k + j % k) % k = (i + j) % k)
2425Proof
2426 STRIP_TAC THEN
2427 `(i = i / k * k + i % k) /\ (j = j/k * k + j%k)`
2428 by METIS_TAC [INT_DIVISION] THEN
2429 Q.ABBREV_TAC `Qi = i / k` THEN
2430 Q.ABBREV_TAC `Ri = i % k` THEN
2431 Q.ABBREV_TAC `Qj = j / k` THEN
2432 Q.ABBREV_TAC `Rj = j % k` THEN
2433 markerLib.RM_ALL_ABBREVS_TAC THEN
2434 SRW_TAC [][] THEN
2435 `Qi * k + Ri + (Qj * k + Rj) = Qi * k + (Qj * k + (Ri + Rj))`
2436 by SRW_TAC [][AC INT_ADD_ASSOC INT_ADD_COMM] THEN
2437 SRW_TAC [][INT_MOD_ADD_MULTIPLES]
2438QED
2439
2440(* surprisingly, this is not an easy consequence of INT_MOD_PLUS and
2441 INT_MOD_NEG_NUMERATOR
2442*)
2443Theorem INT_MOD_SUB:
2444 ~(k = 0) ==> ((i % k - j % k) % k = (i - j) % k)
2445Proof
2446 STRIP_TAC THEN
2447 `(i = i / k * k + i % k) /\ (j = j / k * k + j % k)`
2448 by METIS_TAC [INT_DIVISION] THEN
2449 Q.ABBREV_TAC `Qi = i / k` THEN
2450 Q.ABBREV_TAC `Ri = i % k` THEN
2451 Q.ABBREV_TAC `Qj = j / k` THEN
2452 Q.ABBREV_TAC `Rj = j % k` THEN
2453 markerLib.RM_ALL_ABBREVS_TAC THEN
2454 SRW_TAC [][int_sub, INT_NEG_ADD, INT_NEG_LMUL] THEN
2455 `Qi * k + Ri + (~Qj * k + ~Rj) = Qi * k + (~Qj * k + (Ri + ~Rj))`
2456 by SRW_TAC [][AC INT_ADD_ASSOC INT_ADD_COMM] THEN
2457 SRW_TAC [][INT_MOD_ADD_MULTIPLES]
2458QED
2459
2460Theorem INT_MOD_MOD[simp]:
2461 ~(k = 0) ==> (j % k % k = j % k)
2462Proof
2463 STRIP_TAC THEN MATCH_MP_TAC INT_MOD_UNIQUE THEN Q.EXISTS_TAC `0` THEN
2464 SRW_TAC [][] THEN METIS_TAC [INT_DIVISION]
2465QED
2466
2467Theorem INT_DIV_P:
2468 !P x c. ~(c = 0) ==>
2469 (P (x / c) = ?k r. (x = k * c + r) /\
2470 (c < 0 /\ c < r /\ r <= 0 \/
2471 ~(c < 0) /\ 0 <= r /\ r < c) /\ P k)
2472Proof
2473 METIS_TAC [INT_DIVISION, INT_DIV_UNIQUE]
2474QED
2475
2476Theorem INT_MOD_P:
2477 !P x c. ~(c = 0) ==>
2478 (P (x % c) = ?k r. (x = k * c + r) /\
2479 (c < 0 /\ c < r /\ r <= 0 \/
2480 ~(c < 0) /\ 0 <= r /\ r < c) /\ P r)
2481Proof
2482 METIS_TAC [INT_DIVISION, INT_MOD_UNIQUE]
2483QED
2484
2485Theorem INT_DIV_FORALL_P:
2486 !P x c. ~(c = 0) ==>
2487 (P (x / c) = !k r. (x = k * c + r) /\
2488 (c < 0 /\ c < r /\ r <= 0 \/
2489 ~(c < 0) /\ 0 <= r /\ r < c) ==>
2490 P k)
2491Proof
2492 METIS_TAC [INT_DIV_UNIQUE, INT_DIVISION]
2493QED
2494
2495Theorem INT_MOD_FORALL_P:
2496 !P x c. ~(c = 0) ==>
2497 (P (x % c) = !q r. (x = q * c + r) /\
2498 (c < 0 /\ c < r /\ r <= 0 \/
2499 ~(c < 0) /\ 0 <= r /\ r < c) ==>
2500 P r)
2501Proof
2502 METIS_TAC [INT_MOD_UNIQUE, INT_DIVISION]
2503QED
2504
2505Theorem INT_MOD_1:
2506 !i. i % 1 = 0
2507Proof
2508 GEN_TAC THEN MATCH_MP_TAC INT_MOD_UNIQUE THEN
2509 Q.EXISTS_TAC `i` THEN SRW_TAC [][INT_LT, INT_LE]
2510QED
2511
2512Theorem INT_LESS_MOD:
2513 !i j. 0 <= i /\ i < j ==> (i % j = i)
2514Proof
2515 REPEAT STRIP_TAC THEN MATCH_MP_TAC INT_MOD_UNIQUE THEN
2516 Q.EXISTS_TAC `0` THEN SRW_TAC [][] THEN
2517 PROVE_TAC [INT_LET_TRANS, INT_LT_ANTISYM]
2518QED
2519
2520Theorem INT_MOD_MINUS1:
2521 !n. 0 < n ==> (~1 % n = n - 1)
2522Proof
2523 REPEAT STRIP_TAC THEN MATCH_MP_TAC INT_MOD_UNIQUE THEN
2524 Q.EXISTS_TAC `~1` THEN SRW_TAC [][] THENL [
2525 SRW_TAC [][GSYM INT_NEG_MINUS1, INT_NEG_EQ, INT_NEG_ADD, INT_NEGNEG,
2526 INT_NEG_SUB, INT_SUB_ADD2],
2527 PROVE_TAC [INT_LT_ANTISYM],
2528 PROVE_TAC [INT_LT_ANTISYM],
2529 SRW_TAC [][INT_SUB_LE] THEN
2530 FULL_SIMP_TAC (srw_ss()) [INT_LT_LE1, INT_ADD],
2531 SRW_TAC [][INT_LT_SUB_RADD, INT_LT_ADDR, INT_LT]
2532 ]
2533QED
2534
2535
2536(*----------------------------------------------------------------------*)
2537(* Define absolute value *)
2538(*----------------------------------------------------------------------*)
2539
2540val _ = print "Absolute value\n"
2541
2542Definition INT_ABS[nocompute]:
2543 ABS n = if n < 0 then ~n else n
2544End
2545
2546Theorem INT_ABS_POS[simp]:
2547 !p. 0 <= ABS p
2548Proof
2549 GEN_TAC THEN STRIP_ASSUME_TAC (Q.SPEC `p` INT_LT_NEGTOTAL) THEN
2550 ASM_SIMP_TAC bool_ss [INT_ABS, INT_LE_REFL, INT_LT_REFL, INT_LT_GT,
2551 INT_NEG_GT0, INT_NEG_0]
2552 THENL [
2553 ASM_SIMP_TAC bool_ss [INT_LE_LT],
2554 SIMP_TAC bool_ss [GSYM INT_NEG_GT0] THEN
2555 ASM_SIMP_TAC bool_ss [INT_LE_LT]
2556 ]
2557QED
2558
2559Theorem INT_ABS_NUM[simp]:
2560 !n. ABS (&n) = &n
2561Proof
2562 SIMP_TAC bool_ss [INT_ABS, REWRITE_RULE [GSYM INT_NOT_LT] INT_POS]
2563QED
2564
2565Theorem INT_NEG_SAME_EQ:
2566 !p. (p = ~p) = (p = 0)
2567Proof
2568 GEN_TAC THEN EQ_TAC THENL [
2569 PROVE_TAC [INT_NEG_GT0, INT_LT_TRANS, INT_LT_REFL, INT_LT_NEGTOTAL],
2570 SIMP_TAC bool_ss [INT_NEG_0]
2571 ]
2572QED
2573
2574Theorem INT_ABS_NEG[simp]:
2575 !p. ABS ~p = ABS p
2576Proof
2577 GEN_TAC THEN
2578 SIMP_TAC (bool_ss ++ boolSimps.COND_elim_ss)
2579 [INT_ABS, INT_NEG_LT0, INT_NEGNEG, INT_NEG_EQ, INT_NEG_SAME_EQ] THEN
2580 PROVE_TAC [INT_LT_NEGTOTAL, INT_NOT_LT, INT_LE_LT]
2581QED
2582
2583Theorem INT_ABS_ABS[simp]:
2584 !p. ABS (ABS p) = ABS p
2585Proof
2586 GEN_TAC THEN Cases_on `0 <= p` THENL [
2587 `?n. p = &n` by PROVE_TAC [NUM_POSINT_EXISTS] THEN
2588 ASM_SIMP_TAC bool_ss [INT_ABS_NUM],
2589 FULL_SIMP_TAC bool_ss [INT_NOT_LE, INT_ABS, INT_NEGNEG, INT_NEG_LT0,
2590 INT_LT_GT]
2591 ]
2592QED
2593
2594Theorem INT_ABS_EQ_ID[simp]:
2595 !p. (ABS p = p) = (0 <= p)
2596Proof
2597 GEN_TAC THEN STRUCT_CASES_TAC (Q.SPEC `p` INT_NUM_CASES) THEN
2598 SIMP_TAC int_ss [INT_ABS_NUM, INT_ABS_NEG, INT_LE, INT_NEG_SAME_EQ,
2599 INT_NEG_GE0, INT_INJ]
2600QED
2601
2602Theorem INT_ABS_MUL:
2603 !p q. ABS p * ABS q = ABS (p * q)
2604Proof
2605 REPEAT GEN_TAC THEN
2606 STRUCT_CASES_TAC (Q.SPEC `p` INT_NUM_CASES) THEN
2607 STRUCT_CASES_TAC (Q.SPEC `q` INT_NUM_CASES) THEN
2608 SIMP_TAC int_ss [INT_ABS_NUM, INT_ABS_NEG, INT_MUL,
2609 GSYM INT_NEG_LMUL, GSYM INT_NEG_RMUL, INT_NEG_MUL2]
2610QED
2611
2612Theorem INT_ABS_EQ0[simp]:
2613 !p. (ABS p = 0) = (p = 0)
2614Proof
2615 GEN_TAC THEN STRUCT_CASES_TAC (Q.SPEC `p` INT_NUM_CASES) THEN
2616 ASM_SIMP_TAC int_ss [INT_ABS_NEG, INT_ABS_NUM, INT_NEG_EQ0]
2617QED
2618
2619Theorem INT_ABS_LT0:
2620 !p. ~(ABS p < 0)
2621Proof
2622 GEN_TAC THEN STRUCT_CASES_TAC (Q.SPEC `p` INT_NUM_CASES) THEN
2623 ASM_SIMP_TAC int_ss [INT_ABS_NEG, INT_ABS_NUM, INT_LT, INT_LT_NEG]
2624QED
2625
2626Theorem INT_ABS_0LT[simp]:
2627 0 < ABS p <=> p <> 0
2628Proof
2629 ‘0 < ABS p <=> 0 <= ABS p /\ ABS p <> 0’ by metis_tac[INT_LE_LT, INT_LT_REFL] >>
2630 pop_assum SUBST1_TAC >> simp[]
2631QED
2632
2633Theorem INT_ABS_LE0[simp]:
2634 !p. (ABS p <= 0) = (p = 0)
2635Proof
2636 GEN_TAC THEN STRUCT_CASES_TAC (Q.SPEC `p` INT_NUM_CASES) THEN
2637 ASM_SIMP_TAC int_ss [INT_ABS_NEG, INT_ABS_NUM, INT_LE, INT_LE_NEG,
2638 INT_INJ, INT_NEG_EQ0]
2639QED
2640
2641Theorem Num_EQ_ABS:
2642 !i. & (Num i) = ABS i
2643Proof
2644 GEN_TAC THEN
2645 STRUCT_CASES_TAC (Q.SPEC `i` INT_NUM_CASES) THEN
2646 REWRITE_TAC [INT_ABS_NUM,INT_ABS_NEG,NUM_OF_INT,NUM_OF_NEG_INT]
2647QED
2648
2649Theorem INT_ABS_LT:
2650 !p q. (ABS p < q <=> p < q /\ ~q < p) /\
2651 (q < ABS p <=> q < p \/ p < ~q) /\
2652 (~ABS p < q <=> ~q < p \/ p < q) /\
2653 (q < ~ABS p <=> p < ~q /\ q < p)
2654Proof
2655 REPEAT GEN_TAC THEN
2656 STRUCT_CASES_TAC (Q.SPEC `p` INT_NUM_CASES) THEN
2657 STRUCT_CASES_TAC (Q.SPEC `q` INT_NUM_CASES) THEN
2658 ASM_SIMP_TAC int_ss [INT_ABS_NUM, INT_ABS_NEG, INT_NEG_LT0,
2659 INT_NEG_0, INT_NEGNEG, INT_NEG_GT0,
2660 INT_LT_CALCULATE]
2661QED
2662
2663Theorem INT_ABS_LE:
2664 !p q. (ABS p <= q <=> p <= q /\ ~q <= p) /\
2665 (q <= ABS p <=> q <= p \/ p <= ~q) /\
2666 (~ABS p <= q <=> ~q <= p \/ p <= q) /\
2667 (q <= ~ABS p <=> p <= ~q /\ q <= p)
2668Proof
2669 REPEAT GEN_TAC THEN
2670 STRUCT_CASES_TAC (Q.SPEC `p` INT_NUM_CASES) THEN
2671 STRUCT_CASES_TAC (Q.SPEC `q` INT_NUM_CASES) THEN
2672 ASM_SIMP_TAC int_ss [INT_ABS_NUM, INT_ABS_NEG, INT_NEG_LT0,
2673 INT_NEG_0, INT_NEGNEG, INT_NEG_GT0, int_le,
2674 INT_LT_CALCULATE]
2675QED
2676
2677Theorem INT_ABS_EQ:
2678 !p q. ((ABS p = q) <=> (p = q) /\ (0 < q) \/ (p = ~q) /\ (0 <= q)) /\
2679 ((q = ABS p) <=> (p = q) /\ (0 < q) \/ (p = ~q) /\ (0 <= q))
2680Proof
2681 REPEAT GEN_TAC THEN
2682 CONV_TAC (RAND_CONV (LAND_CONV (ONCE_REWRITE_CONV [EQ_SYM_EQ]))) THEN
2683 REWRITE_TAC [] THEN
2684 STRUCT_CASES_TAC (Q.SPEC `p` INT_NUM_CASES) THEN
2685 STRUCT_CASES_TAC (Q.SPEC `q` INT_NUM_CASES) THEN
2686 ASM_SIMP_TAC int_ss [INT_ABS_NUM, INT_ABS_NEG, INT_NEG_0, INT_NEGNEG,
2687 int_eq_calculate, INT_EQ_NEG, INT_INJ,
2688 INT_LT_CALCULATE, INT_LE_REFL, INT_LE, INT_NOT_LE]
2689QED
2690
2691Theorem INT_ABS_EQ_ABS:
2692 (ABS x = ABS y) <=> (x = y) \/ (x = -y)
2693Proof
2694 rw[INT_ABS, EQ_IMP_THM] >>
2695 fs[INT_NEG_LT0, INT_NOT_LT, INT_EQ_NEG, INT_NEGNEG, INT_NEG_GE0] >>
2696 metis_tac[INT_LET_TRANS, INT_LT_TRANS, INT_LT_REFL, INT_LE_ANTISYM, INT_NEG_0]
2697QED
2698
2699
2700
2701
2702(* ----------------------------------------------------------------------
2703 Define integer rem(ainder) and quot(ient) functions.
2704 These two are analogous to int_mod and int_div respectively, but
2705 int_quot rounds towards zero, while int_div rounds towards negative
2706 infinity. Once int_quot is fixed, the behaviour of int_rem is
2707 fixed. The choice of names follows the example of the SML Basis
2708 Library.
2709 ---------------------------------------------------------------------- *)
2710
2711val _ = print "Define integer rem(ainder) and quot(ient) functions\n"
2712
2713Theorem int_quot_exists0[local]:
2714 !i j. ?q. ~(j = 0) ==>
2715 (q = if 0 < j then
2716 if 0 <= i then &(Num i DIV Num j)
2717 else ~&(Num ~i DIV Num j)
2718 else
2719 if 0 <= i then ~&(Num i DIV Num ~j)
2720 else &(Num ~i DIV Num ~j))
2721Proof
2722 REPEAT GEN_TAC THEN REWRITE_TAC [IMP_DISJ_THM] THEN
2723 CONV_TAC EXISTS_OR_CONV THEN REWRITE_TAC [EXISTS_REFL]
2724QED
2725
2726val int_quot_exists =
2727 CONV_RULE (BINDER_CONV SKOLEM_CONV THENC SKOLEM_CONV) int_quot_exists0
2728
2729
2730val int_quot = new_specification ("int_quot",["int_quot"],int_quot_exists);
2731
2732val _ = set_fixity "quot" (Infixl 600)
2733Overload quot = ``int_quot``
2734
2735Theorem INT_QUOT:
2736 !p q. ~(q = 0) ==> (&p quot &q = &(p DIV q))
2737Proof
2738 SIMP_TAC int_ss [int_quot, INT_INJ, INT_LT, INT_LE, NUM_OF_INT]
2739QED
2740
2741Theorem INT_QUOT_0:
2742 !q. ~(q = 0) ==> (0 quot q = 0)
2743Proof
2744 GEN_TAC THEN
2745 STRUCT_CASES_TAC (Q.SPEC `q` INT_NUM_CASES) THEN
2746 SIMP_TAC int_ss [INT_INJ, INT_QUOT, INT_NEG_EQ0, ZERO_DIV,
2747 GSYM NOT_ZERO_LT_ZERO, int_quot, INT_NEG_GT0, INT_LE,
2748 INT_LT, INT_NEGNEG, NUM_OF_INT]
2749QED
2750
2751Theorem INT_QUOT_1:
2752 !p. p quot 1 = p
2753Proof
2754 GEN_TAC THEN
2755 STRUCT_CASES_TAC (Q.SPEC `p` INT_NUM_CASES) THEN
2756 ASM_SIMP_TAC int_ss [INT_INJ, INT_QUOT, INT_NEG_EQ0, INT_NEG_GE0,
2757 ONE, DIV_ONE, int_quot, INT_NEG_GT0, INT_LE,
2758 INT_LT, INT_NEGNEG, NUM_OF_INT]
2759QED
2760
2761Theorem INT_QUOT_NEG:
2762 !p q. ~(q = 0) ==> (~p quot q = ~(p quot q)) /\
2763 (p quot ~q = ~(p quot q))
2764Proof
2765 REPEAT GEN_TAC THEN
2766 STRUCT_CASES_TAC (Q.SPEC `p` INT_NUM_CASES) THEN
2767 STRUCT_CASES_TAC (Q.SPEC `q` INT_NUM_CASES) THEN
2768 ASM_SIMP_TAC int_ss [INT_NEGNEG, INT_NEG_0, INT_NEG_EQ0, INT_INJ,
2769 INT_NEGNEG, int_quot, INT_LT, INT_LE, NUM_OF_INT,
2770 INT_NEG_GE0, INT_NEG_GT0, INT_NEG_LT0, INT_NEG_LE0,
2771 ZERO_DIV, GSYM NOT_ZERO_LT_ZERO]
2772QED
2773
2774Theorem INT_ABS_QUOT:
2775 !p q. ~(q = 0) ==> ABS ((p quot q) * q) <= ABS p
2776Proof
2777 REPEAT GEN_TAC THEN
2778 STRUCT_CASES_TAC (Q.SPEC `p` INT_NUM_CASES) THEN
2779 STRUCT_CASES_TAC (Q.SPEC `q` INT_NUM_CASES) THEN
2780 ASM_SIMP_TAC int_ss [INT_INJ, INT_NEG_EQ0, GSYM INT_NEG_LMUL,
2781 GSYM INT_NEG_RMUL, INT_NEG_MUL2, INT_MUL, INT_LE,
2782 INT_QUOT, INT_QUOT_NEG, INT_ABS_NEG, INT_ABS_NUM] THEN
2783 PROVE_TAC [DIVISION, LESS_EQ_EXISTS, NOT_ZERO_LT_ZERO, ZERO_DIV,
2784 MULT_COMM]
2785QED
2786
2787(* can now prove uniqueness of / and % *)
2788fun case_tac s =
2789 STRIP_ALL_THEN ASSUME_TAC (Q.SPEC [QUOTE s] INT_NUM_CASES) THEN
2790 FIRST_X_ASSUM SUBST_ALL_TAC THEN Q.ABBREV_TAC [QUOTE s, QUOTE " = n"] THEN
2791 POP_ASSUM (K ALL_TAC)
2792
2793Theorem lem1[local]:
2794 !x y z. (x = y + ~z) = (x + z = y)
2795Proof
2796 REWRITE_TAC [GSYM int_sub, INT_EQ_SUB_LADD]
2797QED
2798Theorem lem2[local]:
2799 !x y z. (x = ~y + z) = (x + y = z)
2800Proof
2801 PROVE_TAC [INT_ADD_COMM, lem1]
2802QED
2803Theorem lem3[local]:
2804 !x y z. (~x + y = z) = (y = x + z)
2805Proof
2806 PROVE_TAC [INT_ADD_COMM, lem2]
2807QED
2808Theorem lem3a[local]:
2809 !x y z. (x + ~y = z) = (x = y + z)
2810Proof
2811 PROVE_TAC [INT_ADD_COMM, lem2]
2812QED
2813Theorem lem4[local]:
2814 !x y:num. x * y < y <=> (x = 0) /\ ~(y = 0)
2815Proof
2816 Induct THEN ASM_SIMP_TAC int_ss [MULT_CLAUSES]
2817QED
2818
2819Theorem INT_QUOT_UNIQUE:
2820 !p q k.
2821 (?r. (p = k * q + r) /\
2822 (if 0 < p then 0 <= r else r <= 0) /\ ABS r < ABS q) ==>
2823 (p quot q = k)
2824Proof
2825 REPEAT GEN_TAC THEN CONV_TAC LEFT_IMP_EXISTS_CONV THEN GEN_TAC THEN
2826 case_tac "p" THEN
2827 ASM_SIMP_TAC int_ss [INT_LT, INT_NEG_GT0] THEN REPEAT STRIP_TAC THENL [
2828 `?r0. r = &r0` by PROVE_TAC [NUM_POSINT_EXISTS],
2829 `?r0. r = ~&r0` by PROVE_TAC [NUM_NEGINT_EXISTS],
2830 `?r0. r = ~&r0` by PROVE_TAC [NUM_NEGINT_EXISTS]
2831 ] THEN POP_ASSUM SUBST_ALL_TAC THEN Q.ABBREV_TAC `r = r0` THEN
2832 POP_ASSUM (K ALL_TAC) THEN REPEAT (POP_ASSUM MP_TAC) THEN
2833 case_tac "q" THEN case_tac "k" THEN
2834 ASM_SIMP_TAC int_ss
2835 [INT_LT, GSYM AND_IMP_INTRO, INT_MUL_RZERO, INT_ABS_NUM, INT_ADD_LID,
2836 INT_ABS_NEG, INT_LE_REFL, INT_LT_REFL, INT_NEGNEG, GSYM INT_NEG_RMUL,
2837 GSYM INT_NEG_LMUL, INT_MUL, INT_NEG_0, INT_ADD_LID, INT_ABS_LT0,
2838 INT_ADD, INT_NEG_GT0, INT_LE, INT_QUOT, INT_INJ, INT_LT_CALCULATE,
2839 INT_EQ_NEG, INT_QUOT_NEG, LESS_DIV_EQ_ZERO, INT_NEG_LE0, lem1,
2840 lem2, INT_ADD_RINV, INT_ADD_LINV, lem3, int_eq_calculate, lem4] THEN
2841 REPEAT STRIP_TAC THENL [
2842 PROVE_TAC [ADD_COMM, DIV_UNIQUE],
2843 PROVE_TAC [lem4, LESS_EQ_ADD, ADD_COMM, LESS_EQ_LESS_TRANS],
2844 PROVE_TAC [lem4, LESS_EQ_ADD, ADD_COMM, LESS_EQ_LESS_TRANS],
2845 PROVE_TAC [ADD_COMM, DIV_UNIQUE],
2846 PROVE_TAC [lem4, LESS_EQ_ADD, ADD_COMM, LESS_EQ_LESS_TRANS],
2847 ASM_SIMP_TAC int_ss [GSYM INT_NEG_ADD, INT_ADD, INT_QUOT_NEG, INT_QUOT,
2848 INT_INJ, INT_EQ_NEG, INT_NEGNEG] THEN
2849 PROVE_TAC [ADD_COMM, DIV_UNIQUE],
2850 ASM_SIMP_TAC int_ss [GSYM INT_NEG_ADD, INT_ADD, INT_QUOT_NEG, INT_QUOT,
2851 INT_INJ, INT_EQ_NEG, INT_NEGNEG] THEN
2852 PROVE_TAC [ADD_COMM, DIV_UNIQUE],
2853 PROVE_TAC [lem4, LESS_EQ_ADD, ADD_COMM, LESS_EQ_LESS_TRANS]
2854 ]
2855QED
2856
2857Theorem INT_QUOT_ID:
2858 !p. ~(p = 0) ==> (p quot p = 1)
2859Proof
2860 REPEAT STRIP_TAC THEN MATCH_MP_TAC INT_QUOT_UNIQUE THEN
2861 Q.EXISTS_TAC `0` THEN
2862 SIMP_TAC int_ss [INT_ADD_RID, INT_MUL_LID, INT_LE_REFL, INT_ABS_NUM] THEN
2863 PROVE_TAC [INT_ABS_EQ0, INT_ABS_POS, INT_LE_LT]
2864QED
2865
2866(* define rem *)
2867Theorem int_rem_exists0[local]:
2868 !i j. ?r. ~(j = 0) ==> (r = i - i quot j * j)
2869Proof
2870 REPEAT GEN_TAC THEN REWRITE_TAC [IMP_DISJ_THM] THEN
2871 CONV_TAC EXISTS_OR_CONV THEN REWRITE_TAC [EXISTS_REFL]
2872QED
2873val int_rem_exists =
2874 CONV_RULE (BINDER_CONV SKOLEM_CONV THENC SKOLEM_CONV) int_rem_exists0
2875
2876val int_rem = new_specification ("int_rem",["int_rem"],int_rem_exists);
2877
2878val _ = set_fixity "rem" (Infixl 650);
2879Overload rem = ``int_rem``
2880
2881Theorem INT_REM:
2882 !p q. ~(q = 0) ==> (&p rem &q = &(p MOD q))
2883Proof
2884 SIMP_TAC int_ss [int_rem, INT_INJ, int_sub, lem1, lem2, lem3, lem3a,
2885 INT_QUOT, INT_MUL, INT_ADD] THEN
2886 PROVE_TAC [DIVISION, NOT_ZERO_LT_ZERO, MULT_COMM]
2887QED
2888
2889Theorem newlemma[local]:
2890 !x y. (~x + y <= 0 <=> y <= x) /\ (0 <= x + ~y <=> y <= x)
2891Proof
2892 REPEAT STRIP_TAC THENL [
2893 CONV_TAC (LHS_CONV (LAND_CONV (REWR_CONV INT_ADD_COMM))),
2894 ALL_TAC
2895 ] THEN REWRITE_TAC [GSYM int_sub, INT_LE_SUB_RADD, INT_LE_SUB_LADD,
2896 INT_ADD_RID, INT_ADD_LID]
2897QED
2898Theorem nl2[local]:
2899 !p q. ~(q = 0n) ==> p DIV q * q <= p
2900Proof
2901 PROVE_TAC [DIVISION, LESS_EQ_ADD, NOT_ZERO_LT_ZERO]
2902QED
2903Theorem nl2a[local]:
2904 !p q. ~(q = 0n) ==> p < q + p DIV q * q /\ p DIV q * q < p + q
2905Proof
2906 REPEAT STRIP_TAC THENL [
2907 `(p = p DIV q * q + p MOD q) /\ p MOD q < q` by
2908 PROVE_TAC [DIVISION, NOT_ZERO_LT_ZERO] THEN
2909 FIRST_X_ASSUM (CONV_TAC o LAND_CONV o REWR_CONV o
2910 ONCE_REWRITE_RULE [ADD_COMM]) THEN
2911 ASM_REWRITE_TAC [LESS_MONO_ADD_EQ],
2912 MATCH_MP_TAC LESS_EQ_LESS_TRANS THEN Q.EXISTS_TAC `p` THEN
2913 ASM_SIMP_TAC int_ss [nl2]
2914 ]
2915QED
2916
2917Theorem nl3[local]:
2918 !x y z.
2919 (x + ~y < z <=> x < y + z) /\ (~x < y + ~z <=> z < y + x)
2920Proof
2921 REPEAT GEN_TAC THEN
2922 REWRITE_TAC [GSYM int_sub, INT_LT_SUB_RADD, INT_LT_SUB_LADD] THEN
2923 CONV_TAC (RAND_CONV (LHS_CONV (LAND_CONV (REWR_CONV INT_ADD_COMM)))) THEN
2924 REWRITE_TAC [GSYM int_sub, INT_LT_SUB_RADD, INT_LT_SUB_LADD] THEN
2925 PROVE_TAC [INT_ADD_COMM]
2926QED
2927Theorem nl4[local]:
2928 !x y z.
2929 (~x + y < z <=> y < x + z) /\ (~x < ~y + z <=> y < x + z)
2930Proof
2931 PROVE_TAC [nl3, INT_ADD_COMM]
2932QED
2933
2934Theorem INT_REMQUOT:
2935 !q. ~(q = 0) ==> !p. (p = p quot q * q + p rem q) /\
2936 (if 0 < p then 0 <= p rem q else p rem q <= 0) /\
2937 ABS (p rem q) < ABS q
2938Proof
2939 GEN_TAC THEN STRIP_TAC THEN GEN_TAC THEN CONJ_TAC THEN
2940 ASM_SIMP_TAC int_ss [int_rem, INT_INJ, int_sub, INT_ADD_ASSOC, lem1, lem2,
2941 lem3, lem3a]
2942 THENL [
2943 MATCH_ACCEPT_TAC INT_ADD_COMM,
2944 case_tac "p" THEN case_tac "q" THEN FULL_SIMP_TAC int_ss [INT_INJ] THEN
2945 ASM_SIMP_TAC int_ss [INT_INJ, INT_QUOT, INT_LE, INT_LT, INT_QUOT_NEG,
2946 INT_ADD_RID, INT_MUL, INT_NEG_GT0, INT_ADD_LID,
2947 INT_ABS_NUM, INT_ABS_NEG, INT_NEGNEG,
2948 GSYM INT_NEG_RMUL, GSYM INT_NEG_LMUL, ZERO_DIV,
2949 GSYM NOT_ZERO_LT_ZERO, INT_NEG_0, newlemma, nl2
2950 ] THEN
2951 ASM_SIMP_TAC int_ss [INT_ABS_LT, nl3, INT_LT, INT_ADD, nl4, nl2a]
2952 ]
2953QED
2954
2955Theorem INT_REM_UNIQUE:
2956 !p q r.
2957 ABS r < ABS q /\ (if 0 < p then 0 <= r else r <= 0) /\
2958 (?k. p = k * q + r) ==>
2959 (p rem q = r)
2960Proof
2961 REPEAT STRIP_TAC THEN
2962 `~(q = 0)` by (DISCH_THEN SUBST_ALL_TAC THEN
2963 FULL_SIMP_TAC int_ss [INT_ABS_NUM, INT_ABS_LT0]) THEN
2964 ASM_SIMP_TAC int_ss [int_rem, INT_EQ_SUB_RADD] THEN
2965 `(k * q + r) quot q = k` by PROVE_TAC [INT_QUOT_UNIQUE] THEN
2966 ASM_SIMP_TAC int_ss [INT_ADD_COMM]
2967QED
2968
2969Theorem INT_REM_NEG:
2970 !p q. ~(q = 0) ==> (~p rem q = ~(p rem q)) /\ (p rem ~q = p rem q)
2971Proof
2972 REPEAT GEN_TAC THEN
2973 case_tac "p" THEN case_tac "q" THEN
2974 ASM_SIMP_TAC int_ss [INT_INJ, int_rem, INT_NEGNEG, lem1, lem2, lem3,
2975 int_sub, INT_NEG_EQ0, GSYM INT_NEG_LMUL,
2976 GSYM INT_NEG_RMUL, INT_ADD_LID, INT_ADD_RID,
2977 INT_NEG_0, INT_NEG_ADD, INT_QUOT_0, INT_QUOT_NEG,
2978 INT_MUL_LZERO] THEN
2979 METIS_TAC [INT_ADD_ASSOC, INT_ADD_COMM, INT_ADD_LINV, INT_ADD_RID,
2980 INT_ADD_LID, INT_ADD_RINV]
2981QED
2982
2983Theorem INT_REM_ID:
2984 !p. ~(p = 0) ==> (p rem p = 0)
2985Proof
2986 REPEAT STRIP_TAC THEN MATCH_MP_TAC INT_REM_UNIQUE THEN
2987 SIMP_TAC int_ss [INT_LE_REFL] THEN CONJ_TAC THENL [
2988 PROVE_TAC [INT_LE_LT, INT_ABS_POS, INT_ABS_EQ0, INT_ABS_NUM],
2989 Q.EXISTS_TAC `1` THEN REWRITE_TAC [INT_MUL_LID, INT_ADD_RID, INT_LE_REFL]
2990 ]
2991QED
2992
2993Theorem INT_REM0:
2994 !q. ~(q = 0) ==> (0 rem q = 0)
2995Proof
2996 REPEAT STRIP_TAC THEN MATCH_MP_TAC INT_REM_UNIQUE THEN
2997 ASM_SIMP_TAC int_ss [INT_LE_REFL, INT_ABS_NUM, INT_ADD_RID] THEN
2998 PROVE_TAC [INT_LE_LT, INT_ABS_POS, INT_MUL_LZERO, INT_ABS_EQ0]
2999QED
3000
3001Theorem INT_REM_COMMON_FACTOR:
3002 !p. ~(p = 0) ==> !q. (q * p) rem p = 0
3003Proof
3004 REPEAT STRIP_TAC THEN
3005 MATCH_MP_TAC INT_REM_UNIQUE THEN
3006 SIMP_TAC int_ss [INT_ABS_NUM, INT_ADD_RID] THEN
3007 PROVE_TAC [INT_ABS_NUM, INT_LE_LT, INT_ABS_EQ0, INT_ABS_POS]
3008QED
3009
3010Theorem INT_REM_EQ0:
3011 !q. ~(q = 0) ==> !p. (p rem q = 0) = (?k. p = k * q)
3012Proof
3013 REPEAT STRIP_TAC THEN EQ_TAC THEN STRIP_TAC THENL [
3014 Q.PAT_ASSUM `~(q = 0)` (ASSUME_TAC o Q.SPEC `p` o
3015 MATCH_MP INT_REMQUOT) THEN
3016 PROVE_TAC [INT_ADD_RID],
3017 MATCH_MP_TAC INT_REM_UNIQUE THEN CONJ_TAC THENL [
3018 PROVE_TAC [INT_ABS_NUM, INT_ABS_EQ0, INT_LE_LT, INT_ABS_POS],
3019 PROVE_TAC [INT_ADD_RID, INT_LE_REFL]
3020 ]
3021 ]
3022QED
3023
3024Theorem INT_MUL_QUOT:
3025 !p:int q k. ~(q = 0) /\ (p rem q = 0) ==>
3026 ((k * p) quot q = k * (p quot q))
3027Proof
3028 REPEAT STRIP_TAC THEN MATCH_MP_TAC INT_QUOT_UNIQUE THEN
3029 `?m. p = m * q` by PROVE_TAC [INT_REM_EQ0] THEN
3030 Q.SUBGOAL_THEN `p quot q = m` ASSUME_TAC THENL [
3031 MATCH_MP_TAC INT_QUOT_UNIQUE THEN
3032 Q.EXISTS_TAC `0` THEN ASM_SIMP_TAC int_ss [INT_ADD_RID, INT_LE_REFL] THEN
3033 PROVE_TAC [INT_ABS_NUM, INT_ABS_EQ0, INT_LE_LT, INT_ABS_POS],
3034 POP_ASSUM SUBST_ALL_TAC THEN POP_ASSUM SUBST_ALL_TAC THEN
3035 Q.EXISTS_TAC `0` THEN
3036 SIMP_TAC int_ss [INT_MUL_ASSOC, INT_ADD_RID, INT_LE_REFL] THEN
3037 PROVE_TAC [INT_ABS_NUM, INT_ABS_EQ0, INT_LE_LT, INT_ABS_POS]
3038 ]
3039QED
3040
3041Theorem INT_REM_EQ_MOD:
3042 !i n.
3043 0 < n ==>
3044 (i rem n = if i < 0 then (i - 1) % n - n + 1 else i % n)
3045Proof
3046 REPEAT STRIP_TAC THEN
3047 `n <> 0` by METIS_TAC [INT_LT_REFL] THEN
3048 MATCH_MP_TAC INT_REM_UNIQUE THEN
3049 Cases_on `i < 0` THENL [
3050 ASM_SIMP_TAC (srw_ss()) [] THEN
3051 Q.ABBREV_TAC `j = (i - 1) % n` THEN
3052 `0 <= j /\ j < n`
3053 by PROVE_TAC [INT_LT_ANTISYM, INT_DIVISION] THEN
3054 `~(0 < i)` by PROVE_TAC [INT_LT_ANTISYM] THEN
3055 SRW_TAC [][] THENL [
3056 `0 <= n` by IMP_RES_TAC INT_LT_IMP_LE THEN
3057 `ABS n = n` by PROVE_TAC [INT_ABS_EQ_ID] THEN
3058 `~(j - n + 1) = n - (j + 1)`
3059 by SRW_TAC [][int_sub, INT_NEG_ADD, INT_NEGNEG,
3060 AC INT_ADD_ASSOC INT_ADD_COMM] THEN
3061 `0 <= n - (j + 1)` by PROVE_TAC [INT_SUB_LE, INT_LT_LE1] THEN
3062 `ABS (j - n + 1) = n - (j + 1)`
3063 by PROVE_TAC [INT_ABS_EQ_ID, INT_ABS_NEG] THEN
3064 SRW_TAC [][INT_LT_SUB_RADD, INT_LT_ADDR, GSYM INT_LE_LT1],
3065
3066 SRW_TAC [][INT_LT_SUB_RADD, GSYM INT_LT_LE1],
3067
3068 Q.EXISTS_TAC `(i - 1) / n + 1` THEN
3069 SRW_TAC [][INT_RDISTRIB, Abbr`j`, INT_MUL_LID] THEN
3070 SRW_TAC [][INT_ADD_ASSOC] THEN
3071 SRW_TAC [][Once (GSYM INT_EQ_SUB_RADD)] THEN
3072 `(i - 1) / n * n + (i - 1) % n = i - 1`
3073 by METIS_TAC [INT_DIVISION, INT_LT_ANTISYM] THEN
3074 Q_TAC SUFF_TAC `!x y z. x + y + (z - y) = x + z`
3075 THEN1 SRW_TAC [][] THEN
3076 SRW_TAC [][INT_SUB_ADD2, GSYM INT_ADD_ASSOC]
3077 ],
3078
3079 ASM_SIMP_TAC (srw_ss()) [] THEN
3080 `0 <= n` by METIS_TAC [INT_LE_LT] THEN
3081 `0 <= i % n /\ i % n < n` by METIS_TAC [INT_DIVISION, INT_LT_ANTISYM] THEN
3082 `(ABS (i % n) = i % n) /\ (ABS n = n)` by METIS_TAC [INT_ABS_EQ_ID] THEN
3083 SRW_TAC [][] THENL [
3084 `0 < i \/ (i = 0)` by METIS_TAC [INT_NOT_LT, INT_LE_LT] THEN
3085 SRW_TAC [][INT_MOD0, INT_LE_REFL],
3086
3087 Q.EXISTS_TAC `i / n` THEN METIS_TAC [INT_DIVISION]
3088 ]
3089 ]
3090QED
3091
3092
3093(*----------------------------------------------------------------------*)
3094(* Define divisibility *)
3095(*----------------------------------------------------------------------*)
3096
3097val _ = print "Facts about integer divisibility\n";
3098Definition INT_DIVIDES[nocompute]:
3099 int_divides p q = ?m:int. m * p = q
3100End
3101val _ = set_fixity "int_divides" (Infix(NONASSOC, 450))
3102
3103(* HOL-Light compatible definition of ‘int_divides’ (divides) *)
3104Theorem int_divides :
3105 !b a. a int_divides b <=> (?x. b = a * x)
3106Proof
3107 RW_TAC std_ss [INT_DIVIDES, Once INT_MUL_SYM]
3108 >> EQ_TAC >> STRIP_TAC
3109 >| [ Q.EXISTS_TAC ‘m’ >> ASM_REWRITE_TAC [],
3110 Q.EXISTS_TAC ‘x’ >> ASM_REWRITE_TAC [] ]
3111QED
3112
3113Theorem INT_DIVIDES_MOD0:
3114 !p q. p int_divides q <=>
3115 ((q % p = 0) /\ ~(p = 0)) \/ ((p = 0) /\ (q = 0))
3116Proof
3117 REWRITE_TAC [INT_DIVIDES] THEN REPEAT GEN_TAC THEN EQ_TAC THEN
3118 STRIP_TAC THENL [
3119 Cases_on `p = 0` THENL [
3120 POP_ASSUM SUBST_ALL_TAC THEN POP_ASSUM (SUBST_ALL_TAC o SYM) THEN
3121 REWRITE_TAC [INT_MUL_RZERO],
3122 FIRST_X_ASSUM (SUBST_ALL_TAC o SYM) THEN
3123 PROVE_TAC [INT_MOD_COMMON_FACTOR]
3124 ],
3125 PROVE_TAC [INT_MOD_EQ0],
3126 ASM_REWRITE_TAC [INT_MUL_RZERO]
3127 ]
3128QED
3129
3130Theorem INT_DIVIDES_0:
3131 (!x. x int_divides 0) /\ (!x. 0 int_divides x <=> (x = 0))
3132Proof
3133 PROVE_TAC [INT_DIVIDES, INT_MUL_RZERO, INT_MUL_LZERO]
3134QED
3135
3136Theorem INT_DIVIDES_1:
3137 !x. 1 int_divides x /\ (x int_divides 1 <=> (x = 1) \/ (x = ~1))
3138Proof
3139 REPEAT STRIP_TAC THEN
3140 PROVE_TAC [INT_DIVIDES, INT_MUL_RID, INT_MUL_EQ_1]
3141QED
3142
3143Theorem INT_DIVIDES_REFL:
3144 !x. x int_divides x
3145Proof
3146 PROVE_TAC [INT_DIVIDES, INT_MUL_LID]
3147QED
3148
3149Theorem INT_DIVIDES_TRANS:
3150 !x y z. x int_divides y /\ y int_divides z ==> x int_divides z
3151Proof
3152 PROVE_TAC [INT_DIVIDES, INT_MUL_ASSOC]
3153QED
3154
3155Theorem INT_DIVIDES_MUL:
3156 !p q. p int_divides p * q /\ p int_divides q * p
3157Proof
3158 PROVE_TAC [INT_DIVIDES, INT_MUL_COMM]
3159QED
3160
3161Theorem INT_DIVIDES_LMUL:
3162 !p q r. p int_divides q ==> (p int_divides (q * r))
3163Proof
3164 PROVE_TAC [INT_MUL_ASSOC, INT_MUL_SYM, INT_DIVIDES]
3165QED
3166
3167Theorem INT_DIVIDES_RMUL:
3168 !p q r. p int_divides q ==> (p int_divides (r * q))
3169Proof
3170 PROVE_TAC [INT_MUL_ASSOC, INT_MUL_SYM, INT_DIVIDES]
3171QED
3172
3173Theorem INT_DIVIDES_MUL_BOTH:
3174 !p q r. ~(p = 0) ==> (p * q int_divides p * r <=> q int_divides r)
3175Proof
3176 SIMP_TAC bool_ss [INT_DIVIDES] THEN
3177 REPEAT GEN_TAC THEN
3178 `!m p q. m * (p * q) = p * (m * q)` by
3179 PROVE_TAC [INT_MUL_ASSOC, INT_MUL_COMM] THEN
3180 POP_ASSUM (fn th => ONCE_REWRITE_TAC [th]) THEN
3181 PROVE_TAC [INT_EQ_LMUL]
3182QED
3183
3184Theorem INT_DIVIDES_LADD:
3185 !p q r. p int_divides q ==>
3186 (p int_divides (q + r) <=> p int_divides r)
3187Proof
3188 REWRITE_TAC [INT_DIVIDES] THEN REPEAT STRIP_TAC THEN EQ_TAC THEN
3189 DISCH_THEN (Q.X_CHOOSE_THEN `n` ASSUME_TAC) THENL [
3190 Q.EXISTS_TAC `n - m` THEN
3191 ASM_REWRITE_TAC [INT_SUB_RDISTRIB, INT_ADD_SUB],
3192 Q.EXISTS_TAC `m + n` THEN
3193 ASM_REWRITE_TAC [INT_RDISTRIB]
3194 ]
3195QED
3196
3197Theorem INT_DIVIDES_RADD =
3198 ONCE_REWRITE_RULE [INT_ADD_COMM] INT_DIVIDES_LADD;
3199
3200Theorem INT_DIVIDES_NEG:
3201 !p q. (p int_divides ~q <=> p int_divides q) /\
3202 (~p int_divides q <=> p int_divides q)
3203Proof
3204 REWRITE_TAC [INT_DIVIDES] THEN ONCE_REWRITE_TAC [INT_NEG_MINUS1] THEN
3205 REPEAT STRIP_TAC THEN EQ_TAC THEN
3206 DISCH_THEN (Q.X_CHOOSE_THEN `n` ASSUME_TAC) THENL [
3207 Q.EXISTS_TAC `~1 * n` THEN
3208 ASM_REWRITE_TAC [GSYM INT_MUL_ASSOC, GSYM INT_NEG_MINUS1,
3209 INT_NEGNEG],
3210 PROVE_TAC [INT_MUL_ASSOC],
3211 PROVE_TAC [INT_MUL_ASSOC, INT_MUL_SYM],
3212 PROVE_TAC [INT_NEG_MINUS1, INT_NEG_MUL2]
3213 ]
3214QED
3215
3216Theorem INT_DIVIDES_LSUB:
3217 !p q r. p int_divides q ==>
3218 (p int_divides (q - r) <=> p int_divides r)
3219Proof
3220 REWRITE_TAC [int_sub] THEN
3221 PROVE_TAC [INT_DIVIDES_NEG, INT_DIVIDES_LADD]
3222QED
3223
3224Theorem INT_DIVIDES_RSUB:
3225 !p q r. p int_divides q ==>
3226 (p int_divides (r - q) <=> p int_divides r)
3227Proof
3228 REWRITE_TAC [int_sub] THEN
3229 PROVE_TAC [INT_DIVIDES_NEG, INT_DIVIDES_RADD]
3230QED
3231
3232(* temporarily make divides an infix *)
3233val _ = temp_set_fixity "divides" (Infixl 480);
3234
3235(* NOTE: This theorem is the definition of ‘divides’ of natural numbers in
3236 HOL-Light. This name is HOL-Light compatible.
3237 *)
3238Theorem num_divides :
3239 a divides b <=> &a int_divides &b
3240Proof
3241 rw [INT_DIVIDES, divides_def]
3242 >> EQ_TAC >> rw []
3243 >- (Q.EXISTS_TAC ‘&q’ \\
3244 rw [INT_OF_NUM_MUL])
3245 (* INT_POS *)
3246 >> MP_TAC (Q.SPEC ‘m’ INT_NUM_CASES)
3247 >> rw [] (* 3 subgoals *)
3248 >| [ (* goal 1 (of 3) *)
3249 Q.EXISTS_TAC ‘n’ >> fs [INT_OF_NUM_MUL],
3250 (* goal 2 (of 3): impossible *)
3251 fs [INT_MUL_LNEG, INT_OF_NUM_MUL],
3252 (* goal 3 (of 3) *)
3253 fs [] >> POP_ASSUM (fn th => rw [GSYM th]) \\
3254 Q.EXISTS_TAC ‘0’ >> rw [] ]
3255QED
3256
3257(*----------------------------------------------------------------------*)
3258(* Define exponentiation *)
3259(*----------------------------------------------------------------------*)
3260
3261val _ = print "Exponentiation\n"
3262
3263Definition int_exp[nocompute]:
3264 (int_exp (p:int) 0 = 1) /\
3265 (int_exp p (SUC n) = p * int_exp p n)
3266End
3267
3268val _ = set_fixity "int_exp" (Infixr 700);
3269Overload "**" = Term`$int_exp`
3270
3271Theorem INT_POW :
3272 (x :int) ** 0 = &1 /\ (!n. x ** SUC n = x * x ** n)
3273Proof
3274 rw [int_exp]
3275QED
3276
3277Theorem INT_EXP:
3278 !n m. &n ** m = &(n EXP m)
3279Proof
3280 REPEAT GEN_TAC THEN Induct_on `m` THENL [
3281 REWRITE_TAC [int_exp, EXP],
3282 ASM_REWRITE_TAC [int_exp, EXP, INT_MUL]
3283 ]
3284QED
3285
3286Theorem INT_OF_NUM_POW = INT_EXP (* HOL-Light compatible name *)
3287
3288Theorem INT_EXP_EQ0:
3289 !(p:int) n. (p ** n = 0) <=> (p = 0) /\ ~(n = 0)
3290Proof
3291 REPEAT GEN_TAC THEN EQ_TAC THEN STRIP_TAC THENL [
3292 Induct_on `n` THENL [
3293 SIMP_TAC int_ss [int_exp, INT_INJ],
3294 SIMP_TAC int_ss [int_exp, INT_ENTIRE] THEN PROVE_TAC []
3295 ],
3296 `?m. n = SUC m` by PROVE_TAC [num_CASES] THEN
3297 REPEAT (FIRST_X_ASSUM SUBST_ALL_TAC) THEN
3298 SIMP_TAC int_ss [int_exp, INT_MUL_LZERO]
3299 ]
3300QED
3301
3302Theorem INT_MUL_SIGN_CASES:
3303 !p:int q. ((0 < p * q) = (0 < p /\ 0 < q \/ p < 0 /\ q < 0)) /\
3304 ((p * q < 0) = (0 < p /\ q < 0 \/ p < 0 /\ 0 < q))
3305Proof
3306 REPEAT GEN_TAC THEN
3307 Cases_on `0 <= p` THEN Cases_on `0 <= q` THENL [
3308 (* both non-negative *)
3309 `?n. p = &n` by PROVE_TAC [NUM_POSINT_EXISTS] THEN
3310 POP_ASSUM SUBST_ALL_TAC THEN
3311 `?m. q = &m` by PROVE_TAC [NUM_POSINT_EXISTS] THEN
3312 POP_ASSUM SUBST_ALL_TAC THEN
3313 FULL_SIMP_TAC int_ss [INT_LE, INT_LT, INT_MUL] THEN
3314 REWRITE_TAC [GSYM NOT_ZERO_LT_ZERO, MULT_EQ_0, DE_MORGAN_THM],
3315 (* p positive, q negative *)
3316 `?n. p = &n` by PROVE_TAC [NUM_POSINT_EXISTS] THEN
3317 POP_ASSUM SUBST_ALL_TAC THEN
3318 `?m. q = ~&m` by PROVE_TAC [INT_NOT_LE, NUM_NEGINT_EXISTS, INT_LE_LT] THEN
3319 POP_ASSUM SUBST_ALL_TAC THEN
3320 FULL_SIMP_TAC bool_ss [INT_NEG_GE0, GSYM INT_NEG_RMUL,
3321 INT_NEG_GT0, INT_NEG_LT0, INT_MUL, INT_LT,
3322 INT_LE, NOT_LESS_EQUAL, NOT_LESS_0] THEN
3323 ASM_SIMP_TAC int_ss [GSYM NOT_ZERO_LT_ZERO, MULT_EQ_0],
3324 (* q positive, p negative *)
3325 `?n. q = &n` by PROVE_TAC [NUM_POSINT_EXISTS] THEN
3326 POP_ASSUM SUBST_ALL_TAC THEN
3327 `?m. p = ~&m` by PROVE_TAC [INT_NOT_LE, NUM_NEGINT_EXISTS, INT_LE_LT] THEN
3328 POP_ASSUM SUBST_ALL_TAC THEN
3329 FULL_SIMP_TAC bool_ss [INT_NEG_GE0, GSYM INT_NEG_LMUL,
3330 INT_NEG_GT0, INT_NEG_LT0, INT_MUL, INT_LT,
3331 INT_LE, NOT_LESS_EQUAL, NOT_LESS_0] THEN
3332 ASM_SIMP_TAC int_ss [GSYM NOT_ZERO_LT_ZERO, MULT_EQ_0],
3333 (* both negative *)
3334 `?n. p = ~&n` by PROVE_TAC [INT_NOT_LE, NUM_NEGINT_EXISTS, INT_LE_LT] THEN
3335 POP_ASSUM SUBST_ALL_TAC THEN
3336 `?m. q = ~&m` by PROVE_TAC [INT_NOT_LE, NUM_NEGINT_EXISTS, INT_LE_LT] THEN
3337 POP_ASSUM SUBST_ALL_TAC THEN
3338 FULL_SIMP_TAC bool_ss [INT_NEG_GE0, INT_NEG_MUL2, INT_MUL, INT_LT,
3339 INT_LE, NOT_LESS_0, INT_NEG_GT0, INT_NEG_LT0] THEN
3340 SIMP_TAC int_ss [MULT_EQ_0, GSYM NOT_ZERO_LT_ZERO]
3341 ]
3342QED
3343
3344Theorem INT_EXP_NEG:
3345 !n m.
3346 (EVEN n ==> (~&m ** n = &(m EXP n))) /\
3347 (ODD n ==> (~&m ** n = ~&(m EXP n)))
3348Proof
3349 Induct THENL [
3350 SIMP_TAC int_ss [EVEN, ODD, int_exp, INT_LE, EXP],
3351 ASM_SIMP_TAC int_ss [EVEN, ODD, GSYM EVEN_ODD, GSYM ODD_EVEN, int_exp,
3352 EXP, GSYM INT_NEG_LMUL, GSYM INT_NEG_RMUL, INT_MUL,
3353 INT_NEGNEG]
3354 ]
3355QED
3356
3357Theorem INT_POW_NEG :
3358 !(x :int) n. -x ** n = (if EVEN n then x ** n else -(x ** n))
3359Proof
3360 qx_genl_tac [‘p’, ‘m’]
3361 >> MP_TAC (Q.SPEC ‘p’ INT_NUM_CASES)
3362 >> RW_TAC std_ss []
3363 >> FULL_SIMP_TAC std_ss [GSYM ODD_EVEN]
3364 >| [ (* goal 1 (of 6) *)
3365 RW_TAC std_ss[INT_EXP_NEG, INT_EXP],
3366 (* goal 2 (of 6) *)
3367 RW_TAC std_ss[INT_NEG_NEG, INT_EXP_NEG, INT_EXP],
3368 (* goal 3 (of 6) *)
3369 RW_TAC std_ss[INT_NEG_0],
3370 (* goal 4 (of 6) *)
3371 RW_TAC std_ss [INT_EXP_NEG, INT_EXP],
3372 (* goal 5 (of 6) *)
3373 RW_TAC std_ss [INT_NEG_NEG, INT_EXP_NEG, INT_EXP],
3374 (* goal 6 (of 6) *)
3375 RW_TAC std_ss [INT_NEG_0, INT_EXP] \\
3376 rw [ZERO_EXP] \\
3377 CCONTR_TAC >> fs [] ]
3378QED
3379
3380Theorem INT_EXP_ADD_EXPONENTS:
3381 !n m p:int. p ** n * p ** m = p ** (n + m)
3382Proof
3383 Induct THENL [
3384 SIMP_TAC int_ss [int_exp, INT_MUL_LID],
3385 SIMP_TAC bool_ss [int_exp, ADD_CLAUSES] THEN
3386 PROVE_TAC [INT_MUL_ASSOC, INT_EQ_LMUL]
3387 ]
3388QED
3389
3390Theorem INT_EXP_MULTIPLY_EXPONENTS:
3391 !m n p:int. (p ** n) ** m = p ** (n * m)
3392Proof
3393 Induct THENL [
3394 SIMP_TAC int_ss [MULT_CLAUSES, int_exp],
3395 ASM_SIMP_TAC bool_ss [int_exp, MULT_CLAUSES, GSYM INT_EXP_ADD_EXPONENTS]
3396 ]
3397QED
3398
3399Theorem INT_EXP_MOD:
3400 !m n p:int. n <= m /\ ~(p = 0) ==> (p ** m % p ** n = 0)
3401Proof
3402 SIMP_TAC int_ss [INT_MOD_EQ0, INT_EXP_EQ0] THEN
3403 PROVE_TAC [LESS_EQ_EXISTS, INT_EXP_ADD_EXPONENTS, ADD_COMM]
3404QED
3405
3406Theorem INT_EXP_SUBTRACT_EXPONENTS:
3407 !m n p:int. n <= m /\ ~(p = 0) ==>
3408 ((p ** m) / (p ** n) = p ** (m - n))
3409Proof
3410 Induct THENL [
3411 REPEAT STRIP_TAC THEN
3412 `n = 0` by ASM_SIMP_TAC int_ss [] THEN
3413 RW_TAC int_ss [int_exp, ONE, INT_EXP, DIV_ONE, INT_DIV],
3414 REPEAT GEN_TAC THEN Cases_on `n = SUC m` THENL
3415 [ASM_SIMP_TAC int_ss [int_exp, INT_DIV_ID, INT_ENTIRE, INT_EXP_EQ0],
3416 STRIP_TAC THEN `n <= m` by ASM_SIMP_TAC int_ss []
3417 THEN ASM_SIMP_TAC int_ss [SUB, int_exp] THEN
3418 `p ** m % p ** n = 0` by PROVE_TAC [INT_EXP_MOD] THEN
3419 `p * p ** m / p ** n = p * (p ** m / p ** n)`
3420 by (MATCH_MP_TAC INT_MUL_DIV THEN ASM_SIMP_TAC int_ss [INT_EXP_EQ0])
3421 THEN RW_TAC int_ss []]]
3422QED
3423
3424(*----------------------------------------------------------------------*)
3425(* Define integer minimum and maximum *)
3426(*----------------------------------------------------------------------*)
3427
3428Definition INT_MIN[nocompute]:
3429 int_min (x:int) y = if x < y then x else y
3430End
3431
3432Definition INT_MAX[nocompute]:
3433 int_max (x:int) y = if x < y then y else x
3434End
3435
3436Theorem INT_MIN_LT:
3437 !x y z. x < int_min y z ==> x < y /\ x < z
3438Proof
3439 SIMP_TAC bool_ss [INT_MIN] THEN REPEAT GEN_TAC THEN COND_CASES_TAC THEN
3440 PROVE_TAC [INT_LT_TRANS, INT_LT_TOTAL]
3441QED
3442
3443Theorem INT_MAX_LT:
3444 !x y z. int_max x y < z ==> x < z /\ y < z
3445Proof
3446 SIMP_TAC bool_ss [INT_MAX] THEN REPEAT GEN_TAC THEN COND_CASES_TAC THEN
3447 PROVE_TAC [INT_LT_TRANS, INT_LT_TOTAL]
3448QED
3449
3450Theorem INT_MIN_NUM:
3451 !m n. int_min (&m) (&n) = &(MIN m n)
3452Proof
3453 SIMP_TAC (bool_ss ++ LIFT_COND_ss) [INT_MIN, MIN_DEF, INT_LT]
3454QED
3455
3456Theorem INT_MAX_NUM:
3457 !m n. int_max (&m) (&n) = &(MAX m n)
3458Proof
3459 SIMP_TAC (bool_ss ++ LIFT_COND_ss) [INT_MAX, MAX_DEF, INT_LT]
3460QED
3461
3462
3463(* ----------------------------------------------------------------------
3464 Some monotonicity results
3465 ---------------------------------------------------------------------- *)
3466
3467Theorem INT_LT_MONO:
3468 !x y z. 0 < x ==> (x * y < x * z <=> y < z)
3469Proof
3470 REPEAT STRIP_TAC THEN
3471 CONV_TAC (Conv.BINOP_CONV (LAND_CONV (REWR_CONV (GSYM INT_ADD_LID)))) THEN
3472 REWRITE_TAC [GSYM INT_LT_SUB_LADD, GSYM INT_SUB_LDISTRIB] THEN
3473 PROVE_TAC [INT_LT_ANTISYM, INT_MUL_SIGN_CASES]
3474QED
3475
3476Theorem INT_LE_MONO:
3477 !x y z. 0 < x ==> (x * y <= x * z <=> y <= z)
3478Proof
3479 REPEAT STRIP_TAC THEN
3480 CONV_TAC (Conv.BINOP_CONV (LAND_CONV (REWR_CONV (GSYM INT_ADD_LID)))) THEN
3481 REWRITE_TAC [GSYM INT_LE_SUB_LADD, GSYM INT_SUB_LDISTRIB] THEN
3482 ASM_SIMP_TAC bool_ss [INT_LE_LT, INT_MUL_SIGN_CASES, INT_LT_GT] THEN
3483 PROVE_TAC [INT_ENTIRE, INT_LT_REFL]
3484QED
3485
3486Theorem INFINITE_INT_UNIV[simp]:
3487 INFINITE univ(:int)
3488Proof
3489 REWRITE_TAC [] THEN STRIP_TAC THEN
3490 `FINITE (IMAGE Num univ(:int))` by SRW_TAC [][] THEN
3491 Q_TAC SUFF_TAC `IMAGE Num univ(:int) = univ(:num)`
3492 THEN1 (STRIP_TAC THEN FULL_SIMP_TAC (srw_ss()) []) THEN
3493 SRW_TAC [][EXTENSION] THEN Q.EXISTS_TAC `&x` THEN SRW_TAC [][NUM_OF_INT]
3494QED
3495
3496Theorem INT_ABS_SUB:
3497 ABS (i - j) = ABS (j - i)
3498Proof
3499 Cases_on ‘i’ >> Cases_on‘j’ >> simp[INT_ABS, INT_LT_SUB_RADD, INT_LT] >>
3500 rw[] >> gs[INT_NEG_SUB, INT_SUB, INT_LT, INT_LT_CALCULATE] >>
3501 rename [‘~(m < n)’, ‘~(n < m)’] >> ‘m = n’ by DECIDE_TAC >> gvs[]
3502QED
3503
3504Theorem INT_ABS_TRIANGLE:
3505 ABS (i + j) <= ABS i + ABS j
3506Proof
3507 Cases_on ‘i’ >> Cases_on ‘j’ >> simp[INT_ADD, GSYM INT_NEG_ADD] >~
3508 [‘ABS (&m + -&n)’]
3509 >- (Cases_on ‘n <= m’ >> simp[GSYM int_sub, INT_SUB, INT_LE] >>
3510 simp[Once INT_ABS_SUB, INT_SUB, INT_LE]) >~
3511 [‘ABS (-&m + &n)’]
3512 >- (ONCE_REWRITE_TAC[INT_ADD_COMM] >>
3513 Cases_on ‘m <= n’ >> simp[GSYM int_sub, INT_SUB, INT_LE] >>
3514 simp[Once INT_ABS_SUB, INT_SUB, INT_LE])
3515QED
3516
3517Theorem INT_SUB_ABS_TRIANGLE:
3518 ABS i - ABS j <= ABS (i - j)
3519Proof
3520 Cases_on ‘i’ >> Cases_on ‘j’ >> simp[] >>~-
3521 ([‘-&m <= &m’], irule INT_LE_TRANS >> qexists ‘0’ >>
3522 simp[INT_NEG_LE0, INT_LE]) >>
3523 simp[INT_SUB, INT_SUB_RNEG, INT_ADD] >>
3524 rename [‘&m - &n <= _’] >>
3525 Cases_on ‘m <= n’ >> simp[INT_SUB, INT_SUB_RNEG, INT_LE] >>~-
3526 ([‘&m:int - &n’, ‘m <= n’],
3527 irule INT_LE_TRANS >> qexists ‘0’ >> simp[INT_LE_SUB_RADD, INT_LE]) >~
3528 [‘-&m - &n:int’] >- simp[INT_SUB_LNEG, INT_ADD, INT_LE] >~
3529 [‘-&m + &n’]
3530 >- (‘-&m + &n = &n - &m’ by simp[int_sub, AC INT_ADD_COMM INT_ADD_ASSOC] >>
3531 simp[Once INT_ABS_SUB, INT_SUB])
3532QED
3533
3534(*----------------------------------------------------------------------*)
3535(* Prove rewrites for calculation with integers *)
3536(*----------------------------------------------------------------------*)
3537
3538val _ = print "Proving rewrites for calculation with integers\n"
3539
3540Theorem INT_ADD_CALCULATE:
3541 !p:int n m.
3542 (0 + p = p) /\ (p + 0 = p) /\
3543 (&n + &m:int = &(n + m)) /\
3544 (&n + ~&m = if m <= n then &(n - m) else ~&(m - n)) /\
3545 (~&n + &m = if n <= m then &(m - n) else ~&(n - m)) /\
3546 (~&n + ~&m = ~&(n + m))
3547Proof
3548 SIMP_TAC (int_ss ++ boolSimps.COND_elim_ss) [
3549 INT_ADD_LID, INT_ADD_RID, INT_ADD, GSYM INT_NEG_ADD, INT_ADD_COMM,
3550 GSYM int_sub, INT_EQ_SUB_RADD, INT_INJ, INT_SUB
3551 ]
3552QED
3553
3554Theorem INT_ADD_REDUCE:
3555 !p:int n m.
3556 (0 + p = p) /\ (p + 0 = p) /\ (~0 = 0) /\ (~~p = p) /\
3557 (&(NUMERAL n) + &(NUMERAL m):int =
3558 &(NUMERAL (numeral$iZ (n + m)))) /\
3559 (&(NUMERAL n) + ~&(NUMERAL m):int =
3560 if m <= n then &(NUMERAL (n - m)) else ~&(NUMERAL (m - n))) /\
3561 (~&(NUMERAL n) + &(NUMERAL m):int =
3562 if n <= m then &(NUMERAL (m - n)) else ~&(NUMERAL (n - m))) /\
3563 (~&(NUMERAL n) + ~&(NUMERAL m):int =
3564 ~&(NUMERAL (numeral$iZ (n + m))))
3565Proof
3566 SIMP_TAC (int_ss ++ boolSimps.COND_elim_ss) [
3567 INT_ADD_LID, INT_ADD_RID, INT_ADD, GSYM INT_NEG_ADD, INT_ADD_COMM,
3568 GSYM int_sub, INT_EQ_SUB_RADD, INT_INJ, INT_SUB, numeralTheory.iZ,
3569 NUMERAL_DEF, INT_NEG_0, INT_NEGNEG
3570 ]
3571QED
3572
3573Theorem INT_SUB_CALCULATE = int_sub;
3574
3575Theorem INT_SUB_REDUCE:
3576 !m n p:int.
3577 (p - 0 = p) /\ (0 - p = ~p) /\
3578 (&(NUMERAL m) - &(NUMERAL n):int = &(NUMERAL m) + ~&(NUMERAL n)) /\
3579 (~&(NUMERAL m) - &(NUMERAL n):int = ~&(NUMERAL m) + ~&(NUMERAL n)) /\
3580 (&(NUMERAL m) - ~&(NUMERAL n):int = &(NUMERAL m) + &(NUMERAL n)) /\
3581 (~&(NUMERAL m) - ~&(NUMERAL n):int = ~&(NUMERAL m) + &(NUMERAL n))
3582Proof
3583 REWRITE_TAC [int_sub, INT_NEG_0, INT_ADD_LID, INT_ADD_RID, INT_NEGNEG]
3584QED
3585
3586Theorem INT_MUL_CALCULATE =
3587 LIST_CONJ [INT_MUL, GSYM INT_NEG_LMUL, GSYM INT_NEG_RMUL, INT_NEGNEG];
3588
3589Theorem INT_MUL_REDUCE:
3590 !m n p.
3591 (p * 0i = 0) /\ (0 * p = 0) /\
3592 (&(NUMERAL m) * &(NUMERAL n):int = &(NUMERAL (m * n))) /\
3593 (~&(NUMERAL m) * &(NUMERAL n) = ~&(NUMERAL (m * n))) /\
3594 (&(NUMERAL m) * ~&(NUMERAL n) = ~&(NUMERAL (m * n))) /\
3595 (~&(NUMERAL m) * ~&(NUMERAL n) = &(NUMERAL (m * n)))
3596Proof
3597 REWRITE_TAC [INT_MUL, GSYM INT_NEG_LMUL, GSYM INT_NEG_RMUL, INT_NEGNEG,
3598 NUMERAL_DEF, INT_MUL_LZERO, INT_MUL_RZERO]
3599QED
3600
3601Theorem INT_DIV_CALCULATE =
3602 LIST_CONJ [INT_DIV, INT_DIV_NEG, INT_INJ, INT_NEG_EQ0, INT_NEGNEG];
3603
3604Theorem NB_NOT_0[local]:
3605 !n. ~(BIT1 n = 0) /\ ~(BIT2 n = 0)
3606Proof
3607 SIMP_TAC bool_ss [BIT1, BIT2, ADD_CLAUSES, SUC_NOT]
3608QED
3609Theorem INT_DIV_REDUCE:
3610 !m n.
3611 (0i / &(NUMERAL (BIT1 n)) = 0i) /\
3612 (0i / &(NUMERAL (BIT2 n)) = 0i) /\
3613 (&(NUMERAL m) / &(NUMERAL (BIT1 n)) =
3614 &(NUMERAL m DIV NUMERAL (BIT1 n))) /\
3615 (&(NUMERAL m) / &(NUMERAL (BIT2 n)) =
3616 &(NUMERAL m DIV NUMERAL (BIT2 n))) /\
3617 (~&(NUMERAL m) / &(NUMERAL (BIT1 n)) =
3618 ~&(NUMERAL m DIV NUMERAL (BIT1 n)) +
3619 if NUMERAL m MOD NUMERAL (BIT1 n) = 0 then 0 else ~1) /\
3620 (~&(NUMERAL m) / &(NUMERAL (BIT2 n)) =
3621 ~&(NUMERAL m DIV NUMERAL (BIT2 n)) +
3622 if NUMERAL m MOD NUMERAL (BIT2 n) = 0 then 0 else ~1) /\
3623 (&(NUMERAL m) / ~&(NUMERAL (BIT1 n)) =
3624 ~&(NUMERAL m DIV NUMERAL (BIT1 n)) +
3625 if NUMERAL m MOD NUMERAL (BIT1 n) = 0 then 0 else ~1) /\
3626 (&(NUMERAL m) / ~&(NUMERAL (BIT2 n)) =
3627 ~&(NUMERAL m DIV NUMERAL (BIT2 n)) +
3628 if NUMERAL m MOD NUMERAL (BIT2 n) = 0 then 0 else ~1) /\
3629 (~&(NUMERAL m) / ~&(NUMERAL (BIT1 n)) =
3630 &(NUMERAL m DIV NUMERAL (BIT1 n))) /\
3631 (~&(NUMERAL m) / ~&(NUMERAL (BIT2 n)) =
3632 &(NUMERAL m DIV NUMERAL (BIT2 n)))
3633Proof
3634 SIMP_TAC int_ss [INT_DIV, INT_DIV_NEG, INT_INJ, INT_NEG_EQ0, INT_NEGNEG,
3635 NUMERAL_DEF, NB_NOT_0, ZERO_DIV,
3636 GSYM NOT_ZERO_LT_ZERO] THEN
3637 SIMP_TAC int_ss [INT_INJ, INT_NEG_EQ0, int_div, INT_NEGNEG, INT_NEG_GE0,
3638 NUMERAL_DEF, NB_NOT_0, ZERO_DIV,
3639 GSYM NOT_ZERO_LT_ZERO, INT_LT, INT_LE, NUM_OF_INT,
3640 INT_NEG_EQ0, INT_NEG_0] THEN
3641 REPEAT GEN_TAC THEN Q.ASM_CASES_TAC `m = 0` THEN
3642 ASM_SIMP_TAC int_ss [ZERO_DIV, NB_NOT_0, GSYM NOT_ZERO_LT_ZERO,
3643 ZERO_MOD, INT_NEG_0, INT_ADD, INT_INJ]
3644QED
3645
3646Theorem INT_QUOT_CALCULATE =
3647 LIST_CONJ [INT_QUOT, INT_QUOT_NEG, INT_INJ, INT_NEG_EQ0, INT_NEGNEG];
3648
3649Theorem INT_QUOT_REDUCE:
3650 !m n.
3651 (0i quot &(NUMERAL (BIT1 n)) = 0i) /\
3652 (0i quot &(NUMERAL (BIT2 n)) = 0i) /\
3653 (&(NUMERAL m) quot &(NUMERAL (BIT1 n)) =
3654 &(NUMERAL m DIV NUMERAL (BIT1 n))) /\
3655 (&(NUMERAL m) quot &(NUMERAL (BIT2 n)) =
3656 &(NUMERAL m DIV NUMERAL (BIT2 n))) /\
3657 (~&(NUMERAL m) quot &(NUMERAL (BIT1 n)) =
3658 ~&(NUMERAL m DIV NUMERAL (BIT1 n))) /\
3659 (~&(NUMERAL m) quot &(NUMERAL (BIT2 n)) =
3660 ~&(NUMERAL m DIV NUMERAL (BIT2 n))) /\
3661 (&(NUMERAL m) quot ~&(NUMERAL (BIT1 n)) =
3662 ~&(NUMERAL m DIV NUMERAL (BIT1 n))) /\
3663 (&(NUMERAL m) quot ~&(NUMERAL (BIT2 n)) =
3664 ~&(NUMERAL m DIV NUMERAL (BIT2 n))) /\
3665 (~&(NUMERAL m) quot ~&(NUMERAL (BIT1 n)) =
3666 &(NUMERAL m DIV NUMERAL (BIT1 n))) /\
3667 (~&(NUMERAL m) quot ~&(NUMERAL (BIT2 n)) =
3668 &(NUMERAL m DIV NUMERAL (BIT2 n)))
3669Proof
3670 SIMP_TAC bool_ss [INT_QUOT, INT_QUOT_NEG, INT_INJ, INT_NEG_EQ0, INT_NEGNEG,
3671 NUMERAL_DEF, BIT1, BIT2, ZERO_DIV, ADD_CLAUSES, NOT_SUC,
3672 prim_recTheory.LESS_0]
3673QED
3674
3675Theorem INT_MOD_CALCULATE =
3676 LIST_CONJ [INT_MOD, INT_MOD_NEG, INT_NEGNEG, INT_INJ, INT_NEG_EQ0];
3677
3678Theorem INT_MOD_REDUCE:
3679 !m n.
3680 (0i % &(NUMERAL (BIT1 n)) = 0i) /\
3681 (0i % &(NUMERAL (BIT2 n)) = 0i) /\
3682 (0i % -&(NUMERAL (BIT1 n)) = 0i) /\
3683 (0i % -&(NUMERAL (BIT2 n)) = 0i) /\
3684 (&(NUMERAL m) % &(NUMERAL (BIT1 n)) = &(NUMERAL m MOD NUMERAL (BIT1 n))) /\
3685 (&(NUMERAL m) % &(NUMERAL (BIT2 n)) = &(NUMERAL m MOD NUMERAL (BIT2 n))) /\
3686 (&(NUMERAL m) % -&(NUMERAL (BIT1 n)) =
3687 -(-&(NUMERAL m) % &(NUMERAL (BIT1 n)))) /\
3688 (&(NUMERAL m) % -&(NUMERAL (BIT2 n)) =
3689 -(-&(NUMERAL m) % &(NUMERAL (BIT2 n)))) /\
3690 (x % &(NUMERAL (BIT1 n)) =
3691 x - x / &(NUMERAL(BIT1 n)) * &(NUMERAL(BIT1 n))) /\
3692 (x % &(NUMERAL (BIT2 n)) =
3693 x - x / &(NUMERAL(BIT2 n)) * &(NUMERAL(BIT2 n))) /\
3694 (x % -&(NUMERAL (BIT1 n)) =
3695 (-x / &(NUMERAL(BIT1 n)) * &(NUMERAL(BIT1 n)) + x)) /\
3696 (x % -&(NUMERAL (BIT2 n)) =
3697 (-x / &(NUMERAL(BIT2 n)) * &(NUMERAL(BIT2 n)) + x))
3698Proof
3699 SIMP_TAC int_ss
3700 [INT_MOD_CALCULATE, BIT1, BIT2, NUMERAL_DEF, ALT_ZERO, ZERO_MOD, int_mod,
3701 INT_NEG_0, INT_DIV_0, INT_MUL_LZERO, INT_SUB_RZERO, INT_NEG_SUB,
3702 INT_SUB_RNEG]
3703QED
3704
3705
3706Theorem INT_REM_CALCULATE =
3707 LIST_CONJ [INT_REM, INT_REM_NEG, INT_NEGNEG, INT_INJ, INT_NEG_EQ0];
3708
3709Theorem INT_REM_REDUCE:
3710 !m n. (0i rem &(NUMERAL (BIT1 n)) = 0i) /\
3711 (0i rem &(NUMERAL (BIT2 n)) = 0i) /\
3712 (&(NUMERAL m) rem &(NUMERAL (BIT1 n)) =
3713 &(NUMERAL m MOD NUMERAL (BIT1 n))) /\
3714 (&(NUMERAL m) rem &(NUMERAL (BIT2 n)) =
3715 &(NUMERAL m MOD NUMERAL (BIT2 n))) /\
3716 (~&(NUMERAL m) rem &(NUMERAL (BIT1 n)) =
3717 ~&(NUMERAL m MOD NUMERAL (BIT1 n))) /\
3718 (~&(NUMERAL m) rem &(NUMERAL (BIT2 n)) =
3719 ~&(NUMERAL m MOD NUMERAL (BIT2 n))) /\
3720 (&(NUMERAL m) rem ~&(NUMERAL (BIT1 n)) =
3721 &(NUMERAL m MOD NUMERAL (BIT1 n))) /\
3722 (&(NUMERAL m) rem ~&(NUMERAL (BIT2 n)) =
3723 &(NUMERAL m MOD NUMERAL (BIT2 n))) /\
3724 (~&(NUMERAL m) rem ~&(NUMERAL (BIT1 n)) =
3725 ~&(NUMERAL m MOD NUMERAL (BIT1 n))) /\
3726 (~&(NUMERAL m) rem ~&(NUMERAL (BIT2 n)) =
3727 ~&(NUMERAL m MOD NUMERAL (BIT2 n)))
3728Proof
3729 SIMP_TAC int_ss [INT_REM_CALCULATE, BIT1, BIT2,
3730 NUMERAL_DEF, ALT_ZERO, ZERO_MOD]
3731QED
3732
3733Theorem ODD_NB1[local]:
3734 !n. ODD(BIT1 n)
3735Proof
3736 SIMP_TAC bool_ss [BIT1, ODD, ADD_CLAUSES, ODD_ADD]
3737QED
3738Theorem EVEN_NB2[local]:
3739 !n. EVEN(BIT2 n)
3740Proof
3741 SIMP_TAC bool_ss [BIT2, ADD_CLAUSES, EVEN, EVEN_ADD]
3742QED
3743
3744Theorem INT_EXP_CALCULATE:
3745 !p:int n m.
3746 (p ** 0 = 1) /\ (&n ** m = &(n EXP m)) /\
3747 (~&n ** NUMERAL (BIT1 m) =
3748 ~&(NUMERAL (n EXP NUMERAL (BIT1 m)))) /\
3749 (~&n ** NUMERAL (BIT2 m) =
3750 &(NUMERAL (n EXP NUMERAL (BIT2 m))))
3751Proof
3752 SIMP_TAC int_ss [INT_EXP, int_exp] THEN
3753 SIMP_TAC int_ss [NUMERAL_DEF, ODD_NB1, EVEN_NB2, INT_EXP_NEG]
3754QED
3755
3756Theorem INT_EXP_REDUCE:
3757 !n m p:int.
3758 (p ** 0 = 1) /\
3759 (&(NUMERAL n):int ** (NUMERAL m) = &(NUMERAL (n EXP m))) /\
3760 (~&(NUMERAL n) ** NUMERAL (BIT1 m) =
3761 ~&(NUMERAL (n EXP BIT1 m))) /\
3762 (~&(NUMERAL n) ** NUMERAL (BIT2 m) =
3763 &(NUMERAL (n EXP BIT2 m)))
3764Proof
3765 SIMP_TAC int_ss [INT_EXP_CALCULATE, NUMERAL_DEF]
3766QED
3767
3768Theorem INT_LT_REDUCE:
3769 !n m. (0i < &(NUMERAL (BIT1 n)) <=> T) /\
3770 (0i < &(NUMERAL (BIT2 n)) <=> T) /\
3771 (0i < 0i <=> F) /\
3772 (0i < ~&(NUMERAL n) <=> F) /\
3773 (&(NUMERAL n) < 0i <=> F) /\
3774 (~&(NUMERAL (BIT1 n)) < 0i <=> T) /\
3775 (~&(NUMERAL (BIT2 n)) < 0i <=> T) /\
3776 (&(NUMERAL n) :int < &(NUMERAL m) <=> n < m) /\
3777 (~&(NUMERAL (BIT1 n)) < &(NUMERAL m) <=> T) /\
3778 (~&(NUMERAL (BIT2 n)) < &(NUMERAL m) <=> T) /\
3779 (&(NUMERAL n) < ~&(NUMERAL m) <=> F) /\
3780 (~&(NUMERAL n) < ~&(NUMERAL m) <=> m < n)
3781Proof
3782 SIMP_TAC bool_ss [INT_LT_CALCULATE, NUMERAL_DEF, BIT1,
3783 BIT2] THEN
3784 CONV_TAC ARITH_CONV
3785QED
3786
3787Theorem INT_LE_CALCULATE = INT_LE_LT;
3788
3789Theorem INT_LE_REDUCE:
3790 !n m. (0i <= 0i <=> T) /\ (0i <= &(NUMERAL n) <=> T) /\
3791 (0i <= ~&(NUMERAL (BIT1 n)) <=> F) /\
3792 (0i <= ~&(NUMERAL (BIT2 n)) <=> F) /\
3793 (&(NUMERAL(BIT1 n)) <= 0i <=> F) /\
3794 (&(NUMERAL(BIT2 n)) <= 0i <=> F) /\
3795 (~&(NUMERAL(BIT1 n)) <= 0i <=> T) /\
3796 (~&(NUMERAL(BIT2 n)) <= 0i <=> T) /\
3797 (&(NUMERAL n):int <= &(NUMERAL m) <=> n <= m) /\
3798 (&(NUMERAL n) <= ~&(NUMERAL (BIT1 m)) <=> F) /\
3799 (&(NUMERAL n) <= ~&(NUMERAL (BIT2 m)) <=> F) /\
3800 (~&(NUMERAL n) <= &(NUMERAL m) <=> T) /\
3801 (~&(NUMERAL n) <= ~&(NUMERAL m) <=> m <= n)
3802Proof
3803 SIMP_TAC bool_ss [NUMERAL_DEF, INT_LE_CALCULATE, INT_LT_CALCULATE,
3804 int_eq_calculate, INT_INJ, INT_EQ_NEG, BIT1,
3805 BIT2] THEN
3806 CONV_TAC ARITH_CONV
3807QED
3808
3809Theorem INT_GT_CALCULATE = int_gt;
3810Theorem INT_GT_REDUCE =
3811 PURE_REWRITE_RULE [GSYM int_gt] INT_LT_REDUCE;
3812Theorem INT_GE_CALCULATE = int_ge;
3813Theorem INT_GE_REDUCE =
3814 PURE_REWRITE_RULE [GSYM int_ge] INT_LE_REDUCE;
3815
3816Theorem INT_EQ_CALCULATE =
3817 LIST_CONJ [INT_INJ, INT_EQ_NEG, int_eq_calculate];
3818Theorem INT_EQ_REDUCE:
3819 !n m. ((0i = 0i) <=> T) /\
3820 ((0i = &(NUMERAL (BIT1 n))) <=> F) /\
3821 ((0i = &(NUMERAL (BIT2 n))) <=> F) /\
3822 ((0i = ~&(NUMERAL (BIT1 n))) <=> F) /\
3823 ((0i = ~&(NUMERAL (BIT2 n))) <=> F) /\
3824 ((&(NUMERAL (BIT1 n)) = 0i) <=> F) /\
3825 ((&(NUMERAL (BIT2 n)) = 0i) <=> F) /\
3826 ((~&(NUMERAL (BIT1 n)) = 0i) <=> F) /\
3827 ((~&(NUMERAL (BIT2 n)) = 0i) <=> F) /\
3828 ((&(NUMERAL n) :int = &(NUMERAL m)) <=> (n = m)) /\
3829 ((&(NUMERAL (BIT1 n)) = ~&(NUMERAL m)) <=> F) /\
3830 ((&(NUMERAL (BIT2 n)) = ~&(NUMERAL m)) <=> F) /\
3831 ((~&(NUMERAL (BIT1 n)) = &(NUMERAL m)) <=> F) /\
3832 ((~&(NUMERAL (BIT2 n)) = &(NUMERAL m)) <=> F) /\
3833 ((~&(NUMERAL n) :int = ~&(NUMERAL m)) <=> (n = m))
3834Proof
3835 SIMP_TAC bool_ss [INT_EQ_CALCULATE, NUMERAL_DEF, BIT1,
3836 BIT2] THEN
3837 CONV_TAC ARITH_CONV
3838QED
3839
3840Theorem INT_DIVIDES_REDUCE:
3841 !n m p:int.
3842 (0 int_divides 0 <=> T) /\
3843 (0 int_divides &(NUMERAL (BIT1 n)) <=> F) /\
3844 (0 int_divides &(NUMERAL (BIT2 n)) <=> F) /\
3845 (p int_divides 0 <=> T) /\
3846 (&(NUMERAL (BIT1 n)) int_divides &(NUMERAL m) <=>
3847 (NUMERAL m MOD NUMERAL (BIT1 n) = 0)) /\
3848 (&(NUMERAL (BIT2 n)) int_divides &(NUMERAL m) <=>
3849 (NUMERAL m MOD NUMERAL (BIT2 n) = 0)) /\
3850 (&(NUMERAL (BIT1 n)) int_divides ~&(NUMERAL m) <=>
3851 (NUMERAL m MOD NUMERAL (BIT1 n) = 0)) /\
3852 (&(NUMERAL (BIT2 n)) int_divides ~&(NUMERAL m) <=>
3853 (NUMERAL m MOD NUMERAL (BIT2 n) = 0)) /\
3854 (~&(NUMERAL (BIT1 n)) int_divides &(NUMERAL m) <=>
3855 (NUMERAL m MOD NUMERAL (BIT1 n) = 0)) /\
3856 (~&(NUMERAL (BIT2 n)) int_divides &(NUMERAL m) <=>
3857 (NUMERAL m MOD NUMERAL (BIT2 n) = 0)) /\
3858 (~&(NUMERAL (BIT1 n)) int_divides ~&(NUMERAL m) <=>
3859 (NUMERAL m MOD NUMERAL (BIT1 n) = 0)) /\
3860 (~&(NUMERAL (BIT2 n)) int_divides ~&(NUMERAL m) <=>
3861 (NUMERAL m MOD NUMERAL (BIT2 n) = 0))
3862Proof
3863 SIMP_TAC bool_ss [INT_DIVIDES_NEG] THEN
3864 SIMP_TAC bool_ss [INT_DIVIDES_MOD0, INT_EQ_CALCULATE,
3865 INT_MOD_REDUCE] THEN
3866 SIMP_TAC bool_ss [NUMERAL_DEF, BIT1, BIT2, ADD_CLAUSES, SUC_NOT] THEN
3867 PROVE_TAC [INT_MOD0]
3868QED
3869
3870(* equations to put any expression build on + * ~ & int_0 int_1
3871 under the (unique) following forms: &n or ~&n
3872
3873 NOTE: was in integerRingScript.sml
3874 *)
3875Theorem int_calculate :
3876 ( &n + &m = &(n+m))
3877 /\ (~&n + &m = if n<=m then &(m-n) else ~&(n-m))
3878 /\ ( &n + ~&m = if m<=n then &(n-m) else ~&(m-n))
3879 /\ (~&n + ~&m = ~&(n+m))
3880
3881 /\ ( &n * &m = &(n*m))
3882 /\ (~&n * &m = ~&(n*m))
3883 /\ ( &n * ~&m = ~&(n*m))
3884 /\ (~&n * ~&m = &(n*m))
3885
3886 /\ (( &n = &m) <=> (n=m))
3887 /\ (( &n = ~&m) <=> (n=0)/\(m=0))
3888 /\ ((~&n = &m) <=> (n=0)/\(m=0))
3889 /\ ((~&n = ~&m) <=> (n=m))
3890
3891 /\ (~~x = x : int)
3892 /\ (~0 = 0 : int)
3893Proof
3894 REWRITE_TAC [INT_ADD_CALCULATE,INT_MUL_CALCULATE,INT_EQ_CALCULATE]
3895QED
3896
3897(*---------------------------------------------------------------------------*)
3898(* Lemmas for intLib. *)
3899(*---------------------------------------------------------------------------*)
3900
3901Theorem INT_POLY_CONV_sth[local]:
3902 (!x y z. x + (y + z) = (x + y) + z :int) /\
3903 (!x y. x + y = y + x :int) /\
3904 (!x. &0 + x = x :int) /\
3905 (!x y z. x * (y * z) = (x * y) * z :int) /\
3906 (!x y. x * y = y * x :int) /\
3907 (!x. &1 * x = x :int) /\
3908 (!(x :int). &0 * x = &0) /\
3909 (!x y z. x * (y + z) = x * y + x * z :int) /\
3910 (!(x :int). x ** 0 = &1) /\
3911 (!(x :int) n. x ** (SUC n) = x * (x ** n))
3912Proof
3913 REWRITE_TAC [INT_POW, INT_ADD_ASSOC, INT_MUL_ASSOC, INT_ADD_LID,
3914 INT_MUL_LZERO, INT_MUL_LID, INT_LDISTRIB] THEN
3915 REWRITE_TAC [Once INT_ADD_SYM, Once INT_MUL_SYM]
3916QED
3917
3918Theorem INT_POLY_CONV_sth = MATCH_MP SEMIRING_PTHS INT_POLY_CONV_sth;
3919
3920Theorem INT_POLY_CONV_rth:
3921 (!x. -x = -(&1) * x :int) /\
3922 (!x y. x - y = x + -(&1) * y :int)
3923Proof
3924 REWRITE_TAC [INT_MUL_LNEG, INT_MUL_LID, int_sub]
3925QED
3926
3927Theorem INT_INTEGRAL:
3928 (!(x :int). &0 * x = &0) /\
3929 (!x y (z :int). (x + y = x + z) <=> (y = z)) /\
3930 (!w x y (z :int). (w * y + x * z = w * z + x * y) <=> (w = x) \/ (y = z))
3931Proof
3932 REWRITE_TAC[INT_MUL_LZERO, INT_EQ_LADD] THEN
3933 ONCE_REWRITE_TAC[GSYM INT_SUB_0] THEN
3934 REWRITE_TAC[GSYM INT_ENTIRE] THEN
3935 rpt GEN_TAC \\
3936 Suff ‘w * y + x * z - (w * z + x * y) = (w - x) * (y - z :int)’
3937 >- (Rewr' >> REWRITE_TAC []) \\
3938 REWRITE_TAC [INT_ADD2_SUB2] \\
3939 REWRITE_TAC [GSYM INT_SUB_LDISTRIB] \\
3940 ‘x * (z - y) = -x * (y - z :int)’
3941 by (REWRITE_TAC [INT_MUL_LNEG, INT_SUB_LDISTRIB, INT_NEG_SUB]) \\
3942 POP_ORW \\
3943 REWRITE_TAC [GSYM INT_RDISTRIB, GSYM int_sub]
3944QED
3945
3946(*---------------------------------------------------------------------------*)
3947(* LEAST integer satisfying a predicate (may be undefined). *)
3948(*---------------------------------------------------------------------------*)
3949
3950Definition LEAST_INT_DEF[nocompute]:
3951 LEAST_INT P = @i. P i /\ !j. j < i ==> ~P j
3952End
3953
3954val _ = set_fixity "LEAST_INT" Binder
3955
3956(* NOTE: Ported from HOL-Light *)
3957Theorem FORALL_INT_CASES :
3958 !(P :int -> bool). (!x. P x) <=> (!n. P (&n)) /\ (!n. P (-&n))
3959Proof
3960 rpt STRIP_TAC
3961 >> EQ_TAC >> rw []
3962 >> MP_TAC (Q.SPEC ‘x’ INT_NUM_CASES) >> rw [] (* 3 subgoals *)
3963 >> rw []
3964QED
3965
3966(*---------------------------------------------------------------------------*)
3967(* Euclidean div and mod *)
3968(*---------------------------------------------------------------------------*)
3969
3970Definition EDIV_DEF[nocompute]:
3971 ediv i j = if 0 < j then i / j else -(i / -j)
3972End
3973
3974Definition EMOD_DEF[nocompute]:
3975 emod i j = i % ABS j
3976End
3977
3978(*---------------------------------------------------------------------------*)
3979(* Theorems used for converting div/mod operations into ediv and emod *)
3980(*---------------------------------------------------------------------------*)
3981
3982Theorem INT_DIV_EDIV:
3983 !i j. j <> 0 ==> i / j = if 0 < j then ediv i j else -ediv (-i) j
3984Proof
3985 simp[EDIV_DEF, INT_DIV_NEG, INT_NEGNEG]
3986QED
3987
3988Theorem INT_MOD_EMOD:
3989 !i j. j <> 0 ==> i % j = if 0 < j then emod i j else -emod (-i) j
3990Proof
3991 METIS_TAC[INT_MOD_NEG, INT_NEGNEG, INT_NOT_LT, INT_LT_LE, EMOD_DEF, INT_ABS]
3992QED
3993
3994Theorem INT_QUOT_EDIV:
3995 !i j. j <> 0 ==> i quot j = if 0 <= i then ediv i j else ediv (-i) (-j)
3996Proof
3997 simp[EDIV_DEF, int_quot, int_div, INT_DIV_NEG, INT_NEGNEG] THEN
3998 METIS_TAC[INT_NEG_0, NUM_OF_INT, INT_ADD_LID, INT_LT_LE, INT_NOT_LE,
3999 INT_LE_NEG, ZERO_DIV, ZERO_MOD, NUM_LT]
4000QED
4001
4002Theorem INT_REM_EMOD:
4003 !i j. j <> 0 ==> i rem j = if 0 <= i then emod i j else -emod (-i) j
4004Proof
4005 REPEAT GEN_TAC THEN
4006 STRIP_TAC THEN
4007 simp[EMOD_DEF, int_rem, int_mod, int_quot, int_div, INT_ABS_EQ0] THEN
4008 simp[INT_ABS] THEN
4009 Cases_on `j < 0` THEN
4010 simp[INT_NEGNEG] THEN
4011 METIS_TAC[INT_MUL_CALCULATE, INT_LE_NEG, INT_LT_LE, INT_NOT_LE, INT_SUB_NEG2,
4012 INT_NEG_SUB, INT_NEG_EQ0]
4013QED
4014
4015(*---------------------------------------------------------------------------*)
4016(* Theorems used for converting num operators into int operators *)
4017(*---------------------------------------------------------------------------*)
4018
4019Theorem NUM_INT_ADD:
4020 !m n. m + n = Num (&m + &n)
4021Proof
4022 REWRITE_TAC [INT_ADD, NUM_OF_INT]
4023QED
4024
4025Theorem NUM_INT_SUB:
4026 !m n. m - n = if &m <= &n then 0n else Num (&m - &n)
4027Proof
4028 METIS_TAC[INT_LE, INT_SUB, NUM_OF_INT, NOT_LESS_EQUAL, LESS_IMP_LESS_OR_EQ,
4029 SUB_EQ_0, INT_LE]
4030QED
4031
4032Theorem NUM_INT_MUL:
4033 !m n. m * n = Num (&m * &n)
4034Proof
4035 REWRITE_TAC [INT_MUL, NUM_OF_INT]
4036QED
4037
4038Theorem NUM_INT_EDIV:
4039 !n m. n DIV m = if m = 0 then 0 else Num (ediv (&n) (&m))
4040Proof
4041 METIS_TAC[EDIV_DEF, INT_POS, INT_LT_LE, INT_DIV, NUM_OF_INT, DIV_def]
4042QED
4043
4044Theorem NUM_INT_EMOD:
4045 !n m. n MOD m = if m = 0 then n else Num (emod (&n) (&m))
4046Proof
4047 METIS_TAC[EMOD_DEF, INT_ABS_NUM, INT_MOD, NUM_OF_INT, MOD_def]
4048QED
4049
4050(*---------------------------------------------------------------------------*)
4051
4052val _ = BasicProvers.export_rewrites
4053 ["INT_ADD_LID_UNIQ",
4054 "INT_ADD_RID_UNIQ",
4055 "INT_ADD_SUB", "INT_ADD_SUB2", "INT_DIVIDES_0",
4056 "INT_DIVIDES_1", "INT_DIVIDES_LADD", "INT_DIVIDES_LMUL",
4057 "INT_DIVIDES_LSUB", "INT_DIVIDES_MUL", "INT_DIVIDES_NEG",
4058 "INT_DIVIDES_RADD", "INT_DIVIDES_REFL", "INT_DIVIDES_RMUL",
4059 "INT_DIVIDES_RSUB", "INT_DIV", "INT_QUOT", "INT_DIV_1",
4060 "INT_QUOT_1", "INT_DIV_ID", "INT_QUOT_ID", "INT_DIV_NEG",
4061 "INT_QUOT_NEG", "INT_ENTIRE",
4062 "INT_EQ_LADD", "INT_EQ_LMUL", "INT_EQ_RADD", "INT_EQ_LMUL",
4063 "INT_EXP", "INT_EXP_EQ0", "INT_LE", "INT_LE_ADD",
4064 "INT_LE_ADDL", "INT_LE_ADDR", "INT_LE_DOUBLE", "INT_LE_LADD",
4065 "INT_LE_MUL", "INT_LE_NEG", "INT_LE_NEGL", "INT_LE_NEGR",
4066 "INT_LE_RADD", "INT_LE_SQUARE", "INT_LT_ADD",
4067 "INT_LT_ADDL", "INT_LT_ADDR", "INT_LT_CALCULATE",
4068 "INT_LT_IMP_LE", "INT_LT_LADD",
4069 "INT_LT_RADD", "INT_LT_REFL", "INT_MAX_NUM", "INT_MIN_NUM",
4070 "INT_MOD", "INT_REM", "INT_MOD0", "INT_REM0",
4071 "INT_MOD_COMMON_FACTOR", "INT_REM_COMMON_FACTOR",
4072 "INT_MOD_ID", "INT_REM_ID", "INT_MOD_NEG", "INT_REM_NEG",
4073 "INT_MUL", "INT_MUL_EQ_1", "INT_MUL_LZERO",
4074 "INT_MUL_RZERO",
4075 "INT_NEG_EQ0", "INT_NEG_GE0", "INT_NEG_GT0", "INT_NEG_LE0",
4076 "INT_NEG_LT0", "INT_NEG_MUL2", "INT_NEG_SAME_EQ",
4077 "INT_NEG_SUB", "INT_SUB_0", "INT_SUB_ADD", "INT_SUB_ADD2",
4078 "INT_SUB_NEG2", "INT_SUB_REFL",
4079 "INT_SUB_RNEG", "INT_SUB_SUB",
4080 "INT_SUB_SUB2", "NUM_OF_INT"]