1open HolKernel boolLib Parse
2
3open integerTheory intSyntax dividesTheory
4open simpLib boolSimps BasicProvers
5
6val arith_ss = bool_ss ++ numSimps.old_ARITH_ss
7
8val _ = new_theory "int_arith";
9
10
11val not_less = store_thm(
12  "not_less",
13  Term`~(x:int < y) = y < x + 1`,
14  EQ_TAC THEN REWRITE_TAC [INT_NOT_LT] THEN STRIP_TAC THENL [
15    IMP_RES_TAC INT_LT_ADD1,
16    REWRITE_TAC [INT_LE_LT] THEN Q.ASM_CASES_TAC `y = x` THEN
17    ASM_REWRITE_TAC [] THEN Q.ASM_CASES_TAC `x < y` THENL [
18      IMP_RES_TAC INT_DISCRETE,
19      MP_TAC (Q.SPEC `x` (Q.SPEC `y` INT_LT_TOTAL)) THEN
20      ASM_REWRITE_TAC []
21    ]
22  ]);
23
24val elim_eq = store_thm(
25  "elim_eq",
26  Term`(x:int = y) = (x < y + 1 /\ y < x + 1)`,
27  REWRITE_TAC [GSYM not_less] THEN EQ_TAC THEN STRIP_TAC THENL [
28    ASM_REWRITE_TAC [INT_LT_REFL],
29    MP_TAC (Q.SPECL [`x`,`y`] INT_LT_TOTAL) THEN
30    ASM_REWRITE_TAC []
31  ]);
32
33val less_to_leq_samel = store_thm(
34  "less_to_leq_samel",
35  Term`!x y. x < y = x <= y + ~1`,
36  REWRITE_TAC [int_le, not_less, GSYM INT_ADD_ASSOC, INT_ADD_LINV,
37               INT_ADD_RID]);
38val less_to_leq_samer = store_thm(
39  "less_to_leq_samer",
40  Term`!x y:int. x < y = x + 1 <= y`,
41  REWRITE_TAC [int_le, not_less, INT_LT_RADD]);
42
43val lt_move_all_right = store_thm(
44  "lt_move_all_right",
45  ``!x y. x < y = 0 < y + ~x``,
46  REWRITE_TAC [INT_LT_ADDNEG, INT_ADD_LID]);
47val lt_move_all_left = store_thm(
48  "lt_move_all_left",
49  ``!x y. x < y = x + ~y < 0``,
50  REWRITE_TAC [INT_LT_ADDNEG2, INT_ADD_LID]);
51val lt_move_left_left = store_thm(
52  "lt_move_left_left",
53  ``!x y z. x < y + z = x + ~y < z``,
54  REPEAT GEN_TAC THEN REWRITE_TAC [INT_LT_ADDNEG2] THEN
55  CONV_TAC (LHS_CONV (RAND_CONV (REWR_CONV INT_ADD_COMM))) THEN REFL_TAC);
56val lt_move_left_right = store_thm(
57  "lt_move_left_right",
58  ``!x y z. x + y < z = y < z + ~x``,
59  REPEAT GEN_TAC THEN REWRITE_TAC [INT_LT_ADDNEG] THEN
60  CONV_TAC (LHS_CONV (RATOR_CONV (RAND_CONV (REWR_CONV INT_ADD_COMM)))) THEN
61  REFL_TAC);
62
63val le_move_right_left = store_thm(
64  "le_move_right_left",
65  ``!x y z. x <= y + z = x + ~z <= y``,
66  REWRITE_TAC [INT_LE_SUB_RADD, GSYM int_sub]);
67
68val le_move_all_right = store_thm(
69  "le_move_all_right",
70  ``!x y. x <= y = 0 <= y + ~x``,
71  REWRITE_TAC [GSYM int_sub, INT_LE_SUB_LADD, INT_ADD_LID]);
72
73
74val eq_move_all_right = store_thm(
75  "eq_move_all_right",
76  ``!x y. (x = y) = (0 = y + ~x)``,
77  REPEAT GEN_TAC THEN EQ_TAC THENL [
78    SIMP_TAC bool_ss [INT_ADD_RINV],
79    SIMP_TAC bool_ss [GSYM int_sub, INT_EQ_SUB_LADD, INT_ADD_LID]
80  ]);
81val eq_move_all_left = store_thm(
82  "eq_move_all_left",
83  ``!x y. (x = y) = (x + ~y = 0)``,
84  PROVE_TAC [INT_ADD_COMM, eq_move_all_right]);
85val eq_move_left_left = store_thm(
86  "eq_move_left_left",
87  ``!x y z. (x = y + z) = (x + ~y = z)``,
88  REPEAT GEN_TAC THEN EQ_TAC THENL [
89    DISCH_THEN SUBST1_TAC THEN
90    ONCE_REWRITE_TAC [INT_ADD_COMM] THEN
91    REWRITE_TAC [INT_ADD_ASSOC, INT_ADD_LINV, INT_ADD_LID],
92    DISCH_THEN (SUBST1_TAC o SYM) THEN
93    ONCE_REWRITE_TAC [INT_ADD_COMM] THEN
94    REWRITE_TAC [GSYM INT_ADD_ASSOC, INT_ADD_LINV, INT_ADD_RID]
95  ]);
96val eq_move_left_right = store_thm(
97  "eq_move_left_right",
98  ``!x y z. (x + y = z) = (y = z + ~x)``,
99  PROVE_TAC [INT_ADD_COMM, eq_move_left_left]);
100
101val eq_move_right_left = store_thm(
102  "eq_move_right_left",
103  ``!x y z. (x = y + z) = (x + ~z = y)``,
104  PROVE_TAC [INT_ADD_COMM, eq_move_left_left]);
105
106val lcm_eliminate = store_thm(
107  "lcm_eliminate",
108  ``!P c. (?x. P (c * x)) = (?x. P x /\ c int_divides x)``,
109  REPEAT GEN_TAC THEN SIMP_TAC bool_ss [INT_DIVIDES] THEN
110  PROVE_TAC [INT_MUL_SYM]);
111
112
113val lt_justify_multiplication = store_thm(
114  "lt_justify_multiplication",
115  ���!n x y:int. 0 < n ==> (x < y = n * x < n * y)���,
116  REPEAT STRIP_TAC THEN
117  `n * x < n * y = 0 < n * y - n * x`
118     by PROVE_TAC [INT_LT_ADD_SUB, INT_ADD_LID] THEN
119  POP_ASSUM SUBST_ALL_TAC THEN
120  ASM_REWRITE_TAC [GSYM INT_SUB_LDISTRIB, INT_MUL_SIGN_CASES] THEN
121  `~(n < 0)` by PROVE_TAC [INT_LT_TRANS, INT_LT_REFL] THEN
122  ASM_REWRITE_TAC [INT_ADD_LID, GSYM INT_LT_ADD_SUB]);
123
124val eq_justify_multiplication = store_thm(
125  "eq_justify_multiplication",
126  ���!n x y:int. 0 < n ==> ((x = y) = (n * x = n * y))���,
127  PROVE_TAC [INT_EQ_RMUL, INT_LT_REFL, INT_MUL_COMM]);
128
129val justify_divides = store_thm(
130  "justify_divides",
131  ���!n x y:int. 0 < n ==> (x int_divides y = n * x int_divides n * y)���,
132  PROVE_TAC [INT_DIVIDES_MUL_BOTH, INT_LT_REFL]);
133
134val justify_divides2 = store_thm(
135  "justify_divides2",
136  ���!n c x y:int.
137        n * x int_divides n * y + c =
138        n * x int_divides n * y + c /\ n int_divides c���,
139  REPEAT STRIP_TAC THEN EQ_TAC THEN STRIP_TAC THEN
140  ASM_REWRITE_TAC [] THEN POP_ASSUM MP_TAC THEN
141  REWRITE_TAC [INT_DIVIDES] THEN
142  DISCH_THEN (STRIP_THM_THEN
143              (SUBST_ALL_TAC o SYM o
144               REWRITE_RULE [eq_move_left_left,
145                             INT_NEG_RMUL])) THEN
146  `m * (n * x) = n * (m * x)` by PROVE_TAC [INT_MUL_COMM, INT_MUL_ASSOC] THEN
147  POP_ASSUM SUBST_ALL_TAC THEN
148  REWRITE_TAC [GSYM INT_LDISTRIB] THEN
149  PROVE_TAC [INT_MUL_COMM]);
150
151val justify_divides3 = store_thm(
152  "justify_divides3",
153  ``!n x c. n int_divides n * x + c = n int_divides c``,
154  REPEAT STRIP_TAC THEN MATCH_MP_TAC INT_DIVIDES_LADD THEN
155  MATCH_MP_TAC INT_DIVIDES_LMUL THEN MATCH_ACCEPT_TAC INT_DIVIDES_REFL);
156
157
158val INT_SUB_SUB3 = store_thm(
159  "INT_SUB_SUB3",
160  Term`!x y z:int. x - (y - z) = x + z - y`,
161  REWRITE_TAC [int_sub, INT_NEG_ADD, INT_NEGNEG] THEN
162  PROVE_TAC [INT_ADD_COMM, INT_ADD_ASSOC]);
163
164(* |- !a b c:int. a - b + c = a + c - b *)
165val move_sub = let
166  val thm0 = SYM (SPEC_ALL INT_ADD2_SUB2)
167  val thm1 = Thm.INST [(mk_var("d", int_ty) |-> zero_tm)] thm0
168  val thm2 = REWRITE_RULE [INT_ADD_RID, INT_SUB_RZERO] thm1
169in
170  save_thm("move_sub", GEN_ALL thm2)
171end
172
173val can_get_small = store_thm(
174  "can_get_small",
175  Term`!x:int y d. 0 < d ==> ?c. 0 < c /\ y - c * d < x`,
176  REPEAT STRIP_TAC THEN
177  Q.EXISTS_TAC `if y < x then 1
178                else if y = x then 1
179                else 2 * (y - x)` THEN
180  SRW_TAC [][] THENL [
181    SRW_TAC [][INT_MUL_SIGN_CASES, INT_SUB_LT] THEN PROVE_TAC [INT_LT_TOTAL],
182    MATCH_MP_TAC INT_LT_TRANS THEN Q.EXISTS_TAC `y` THEN
183    ASM_REWRITE_TAC [INT_LT_SUB_RADD, INT_LT_ADDR],
184    ASM_REWRITE_TAC [INT_LT_SUB_RADD, INT_LT_ADDR],
185    ASM_SIMP_TAC (srw_ss()) [INT_MUL_SIGN_CASES, INT_SUB_LDISTRIB,
186                             INT_SUB_RDISTRIB, INT_SUB_LT, INT_SUB_SUB3] THEN
187    `x < y` by PROVE_TAC [INT_LT_TOTAL] THEN
188    ASM_REWRITE_TAC [GSYM move_sub, INT_LT_ADD_SUB] THEN
189    `2 * y * d = y * (2 * d)` by PROVE_TAC [INT_MUL_SYM, INT_MUL_ASSOC] THEN
190    POP_ASSUM SUBST_ALL_TAC THEN
191    `2 * x * d = x * (2 * d)` by PROVE_TAC [INT_MUL_SYM, INT_MUL_ASSOC] THEN
192    POP_ASSUM SUBST_ALL_TAC THEN
193    CONV_TAC
194     (BINOP_CONV (LAND_CONV (REWR_CONV (GSYM INT_MUL_RID)))) THEN
195    REWRITE_TAC [GSYM INT_SUB_LDISTRIB] THEN
196    ONCE_REWRITE_TAC [GSYM INT_LT_NEG] THEN
197    REWRITE_TAC [INT_NEG_RMUL, INT_NEG_SUB] THEN
198    Q.SUBGOAL_THEN `0 < 2 * d - 1`
199      (fn th => PROVE_TAC [th, lt_justify_multiplication, INT_MUL_SYM]) THEN
200    `?n. d = &n` by PROVE_TAC [NUM_POSINT_EXISTS, INT_LE_LT] THEN
201    SRW_TAC [][INT_SUB_LT, INT_LT, INT_MUL] THEN
202    FULL_SIMP_TAC (srw_ss() ++ numSimps.ARITH_ss) []
203  ]);
204
205val can_get_big = store_thm(
206  "can_get_big",
207  ``!x:int y d. 0 < d ==> ?c. 0 < c /\ x < y + c * d``,
208  REPEAT STRIP_TAC THEN REWRITE_TAC [GSYM INT_LT_SUB_RADD] THEN
209  PROVE_TAC [can_get_small]);
210
211val positive_product_implication = store_thm(
212  "positive_product_implication",
213  Term`!c d:int. 0 < c /\ 0 < d ==> 0 < c * d`,
214  SRW_TAC [] [INT_MUL_SIGN_CASES]);
215
216val restricted_quantification_simp = store_thm(
217  "restricted_quantification_simp",
218  Term`!low high x:int.
219           (low < x /\ x <= high) =
220           (low < high /\ ((x = high) \/ (low < x /\ x <= high - 1)))`,
221  REPEAT GEN_TAC THEN EQ_TAC THEN STRIP_TAC THENL [
222    `low < high` by PROVE_TAC [INT_LTE_TRANS] THEN
223    FULL_SIMP_TAC (srw_ss()) [INT_LE_LT] THEN
224    `~(x = high)` by PROVE_TAC [INT_LT_REFL] THEN
225    POP_ASSUM (fn th => REWRITE_TAC [th]) THEN
226    SPOSE_NOT_THEN STRIP_ASSUME_TAC THEN
227    `high - 1 < x` by PROVE_TAC [INT_LT_TOTAL] THEN
228    `high < x + 1` by PROVE_TAC [INT_LT_SUB_RADD] THEN
229    PROVE_TAC [INT_DISCRETE],
230    SRW_TAC [][],
231    FULL_SIMP_TAC (srw_ss()) [INT_LE_LT] THEN DISJ1_TAC THENL [
232      MATCH_MP_TAC INT_LT_TRANS THEN
233      Q.EXISTS_TAC `high - 1`,
234      ALL_TAC
235    ] THEN
236    SRW_TAC [] [INT_LT_SUB_RADD, INT_LT_ADDR]
237  ]);
238
239val top_and_lessers = store_thm(
240  "top_and_lessers",
241  Term`!P d:int x0. (!x. P x ==> P(x - d)) /\ P x0 ==>
242              !c. 0 < c ==> P(x0 - c * d)`,
243  REPEAT STRIP_TAC THEN
244  STRIP_ASSUME_TAC (Q.SPEC `c` INT_NUM_CASES) THENL [
245    (* c strictly positive *)
246    FIRST_ASSUM SUBST_ALL_TAC THEN
247    Induct_on `n` THEN REWRITE_TAC [INT_LT,
248                                    prim_recTheory.LESS_0,
249                                    numTheory.NOT_SUC, INT,
250                                    INT_RDISTRIB, INT_MUL_LID] THEN
251    Cases_on `n` THENL [
252      PROVE_TAC [INT_MUL_LZERO, INT_ADD_LID],
253      FULL_SIMP_TAC bool_ss [INT_INJ, prim_recTheory.INV_SUC_EQ,
254                             prim_recTheory.LESS_0, INT_LT,
255                             numTheory.NOT_SUC] THEN
256      Q.ABBREV_TAC `q = &(SUC n')*d` THEN
257      Q.SUBGOAL_THEN `x0 - (q + d) = x0 - q - d` (fn th => PROVE_TAC [th]) THEN
258      REWRITE_TAC [INT_SUB_CALCULATE, INT_NEG_ADD] THEN
259      CONV_TAC (AC_CONV(INT_ADD_ASSOC, INT_ADD_COMM))
260    ],
261    (* c strictly negative *)
262    FULL_SIMP_TAC bool_ss [INT_NEG_GT0, INT_LT,
263                                   prim_recTheory.NOT_LESS_0],
264    (* c zero *)
265    PROVE_TAC [INT_LT_REFL]
266  ]);
267
268val bot_and_greaters = store_thm(
269  "bot_and_greaters",
270  Term`!P d:int x0. (!x. P x ==> P (x + d)) /\ P x0 ==>
271                    !c. 0 < c ==> P(x0 + c * d)`,
272  REPEAT STRIP_TAC THEN
273  Q.SPECL_THEN [`P`, `~d`, `x0`] MP_TAC top_and_lessers THEN
274  ASM_SIMP_TAC bool_ss [int_sub, INT_NEGNEG, GSYM INT_NEG_RMUL]);
275
276val in_additive_range = store_thm(
277  "in_additive_range",
278  Term`!low d x:int.
279          low < x /\ x <= low + d =
280          ?j. (x = low + j) /\ 0 < j /\ j <= d`,
281  REPEAT GEN_TAC THEN EQ_TAC THEN STRIP_TAC THENL [
282    Q.EXISTS_TAC `x - low` THEN
283    FULL_SIMP_TAC bool_ss [INT_LE_SUB_RADD, INT_LT_SUB_LADD,
284                           INT_ADD_COMM, INT_ADD_LID, INT_SUB_ADD2],
285    FIRST_X_ASSUM SUBST_ALL_TAC THEN
286    ASM_SIMP_TAC bool_ss [INT_LT_SUB_RADD, INT_LT_ADDR, INT_LE_LADD]
287  ]);
288
289val in_subtractive_range = store_thm(
290  "in_subtractive_range",
291  Term`!high d x:int.
292          high - d <= x /\ x < high =
293          ?j. (x = high - j) /\ 0 < j /\ j <= d`,
294  REPEAT GEN_TAC THEN EQ_TAC THEN STRIP_TAC THENL [
295    Q.EXISTS_TAC `high - x` THEN
296    FULL_SIMP_TAC bool_ss [INT_SUB_SUB2, INT_LT_SUB_LADD,
297                           INT_ADD_LID, INT_LE_SUB_RADD,
298                           INT_ADD_COMM],
299    FIRST_X_ASSUM SUBST_ALL_TAC THEN
300    ASM_SIMP_TAC bool_ss [INT_LT_SUB_RADD, INT_LT_ADDR] THEN
301    ASM_SIMP_TAC bool_ss [int_sub, INT_LE_LADD, INT_LE_NEG]
302  ]);
303
304val subtract_to_small = store_thm(
305  "subtract_to_small",
306  Term`!x d:int. 0 < d ==> ?k. 0 < x - k * d /\ x - k * d <= d`,
307  REPEAT STRIP_TAC THEN
308  `~(d = 0)` by PROVE_TAC [INT_LT_REFL] THEN
309  `~(d < 0)` by PROVE_TAC [INT_NOT_LT, INT_LE_LT] THEN
310  `(x = x / d * d + x % d) /\ 0 <= x % d /\ x % d < d`
311     by PROVE_TAC [INT_DIVISION] THEN
312  Q.ABBREV_TAC `q = x / d` THEN POP_ASSUM (K ALL_TAC) THEN
313  Q.ABBREV_TAC `r = x % d` THEN POP_ASSUM (K ALL_TAC) THEN
314  FIRST_X_ASSUM SUBST_ALL_TAC THEN
315  FULL_SIMP_TAC (srw_ss()) [INT_LE_LT] THENL [
316    Q.EXISTS_TAC `q`,
317    Q.EXISTS_TAC `q - 1`
318  ] THEN
319  SRW_TAC [] [INT_LT_SUB_LADD, INT_LE_SUB_RADD, INT_SUB_RDISTRIB,
320              INT_LT_SUB_RADD] THEN
321  PROVE_TAC [INT_ADD_COMM, INT_LT_LADD]);
322
323val add_to_great = store_thm(
324  "add_to_great",
325  Term`!x d:int. 0 < d ==> ?k. 0 < x + k * d /\ x + k * d <= d`,
326  REPEAT STRIP_TAC THEN
327  Q.SPECL_THEN [`x`, `d`] MP_TAC subtract_to_small THEN
328  ASM_REWRITE_TAC [] THEN STRIP_TAC THEN
329  Q.EXISTS_TAC `~k` THEN
330  ASM_REWRITE_TAC [GSYM INT_NEG_LMUL, GSYM int_sub]);
331
332
333open arithmeticTheory
334val INT_LT_ADD_NUMERAL = store_thm(
335  "INT_LT_ADD_NUMERAL",
336  Term`!x:int y. x < x + &(NUMERAL (BIT1 y)) /\
337                 x < x + &(NUMERAL (BIT2 y)) /\
338                 ~(x < x + ~(&(NUMERAL y)))`,
339  SIMP_TAC bool_ss [INT_LT_ADDR, INT_LT, NUMERAL_DEF, BIT1,BIT2,
340                    ADD_CLAUSES, prim_recTheory.LESS_0,
341                    INT_NEG_GT0, prim_recTheory.NOT_LESS_0]);
342
343
344val INT_NUM_FORALL = store_thm(
345  "INT_NUM_FORALL",
346  Term`(!n:num. P (&n)) = (!x:int. 0 <= x ==> P x)`,
347  EQ_TAC THEN REPEAT STRIP_TAC THENL [
348    PROVE_TAC [NUM_POSINT_EXISTS],
349    POP_ASSUM MATCH_MP_TAC THEN SIMP_TAC bool_ss [INT_LE, ZERO_LESS_EQ]
350  ]);
351
352val INT_NUM_EXISTS = store_thm(
353  "INT_NUM_EXISTS",
354  Term`(?n:num. P(&n)) = (?x:int. 0 <= x /\ P x)`,
355  EQ_TAC THEN REPEAT STRIP_TAC THENL [
356    PROVE_TAC [INT_LE, ZERO_LESS_EQ],
357    PROVE_TAC [NUM_POSINT_EXISTS]
358  ]);
359
360val INT_NUM_UEXISTS = store_thm(
361  "INT_NUM_UEXISTS",
362  Term`(?!n:num. P (&n)) = (?!x:int. 0 <= x /\ P x)`,
363  EQ_TAC THEN SIMP_TAC bool_ss [EXISTS_UNIQUE_THM] THEN
364  REPEAT STRIP_TAC THENL [
365    PROVE_TAC [INT_LE, ZERO_LESS_EQ],
366    PROVE_TAC [INT_INJ, NUM_POSINT_EXISTS],
367    PROVE_TAC [NUM_POSINT_EXISTS],
368    PROVE_TAC [INT_INJ, ZERO_LESS_EQ, INT_LE]
369  ]);
370
371val INT_NUM_SUB = store_thm(
372  "INT_NUM_SUB",
373  Term`!n m:num. &(n - m) = if int_of_num n < &m then 0i else &n - &m`,
374  SIMP_TAC (bool_ss ++ COND_elim_ss) [INT_LT, INT_INJ] THEN
375  REPEAT GEN_TAC THEN Q.ASM_CASES_TAC `n < m` THEN
376  ASM_SIMP_TAC bool_ss [SUB_EQ_0, LESS_OR_EQ] THEN
377  PROVE_TAC [INT_SUB, NOT_LESS]);
378
379val INT_NUM_COND = store_thm(
380  "INT_NUM_COND",
381  Term`!b n m. int_of_num (if b then n else m) =
382               if b then &n else &m`,
383  SIMP_TAC (bool_ss ++ COND_elim_ss) [] THEN PROVE_TAC []);
384
385val INT_NUM_ODD = store_thm(
386  "INT_NUM_ODD",
387  Term`!n:num. ODD n = ~(2 int_divides &n)`,
388  SIMP_TAC bool_ss [ODD_EVEN, EVEN_EXISTS, INT_DIVIDES, GSYM INT_INJ,
389                    GSYM INT_MUL] THEN GEN_TAC THEN EQ_TAC THEN
390  REPEAT STRIP_TAC THENL [
391    Cases_on `&n = 0` THENL [
392      POP_ASSUM SUBST_ALL_TAC THEN POP_ASSUM MP_TAC THEN
393      FULL_SIMP_TAC (srw_ss()) [INT_MUL],
394      `0 < &n` by PROVE_TAC [INT_LE_LT, INT_POS] THEN
395      `0 < 2i` by SRW_TAC [][] THEN
396      `0 < m` by PROVE_TAC [INT_MUL_SIGN_CASES, INT_LT_ANTISYM] THEN
397      `?k. m = &k` by PROVE_TAC [NUM_POSINT_EXISTS, INT_LE_LT] THEN
398      POP_ASSUM SUBST_ALL_TAC THEN
399      FIRST_X_ASSUM (MP_TAC o ONCE_REWRITE_RULE [INT_MUL_COMM] o
400                     Q.SPEC `k`) THEN
401      ASM_REWRITE_TAC []
402    ],
403    FIRST_X_ASSUM (MP_TAC o Q.SPEC `int_of_num m`) THEN
404    ASM_REWRITE_TAC [] THEN MATCH_ACCEPT_TAC INT_MUL_COMM
405  ]);
406
407val INT_NUM_EVEN = store_thm(
408  "INT_NUM_EVEN",
409  Term`!n:num. EVEN n = 2 int_divides &n`,
410  SIMP_TAC bool_ss [EVEN_ODD, INT_NUM_ODD]);
411
412val HO_SUB_ELIM = store_thm(
413  "HO_SUB_ELIM",
414  Term`!(P:int -> bool) a b.
415           P(&(a - b)) =
416            (int_of_num b <= &a /\ P(&a + ~&b)) \/
417            (int_of_num a < &b /\ P 0i)`,
418  REPEAT GEN_TAC THEN EQ_TAC THEN STRIP_TAC THEN
419  FULL_SIMP_TAC (bool_ss ++ COND_elim_ss) [INT_NUM_SUB, LEFT_AND_OVER_OR,
420                                           RIGHT_AND_OVER_OR, INT_NOT_LT,
421                                           int_sub] THEN
422  PROVE_TAC [INT_LE_LT, INT_LT_TOTAL, INT_LET_TRANS, INT_LT_REFL])
423
424val CONJ_EQ_ELIM = store_thm(
425  "CONJ_EQ_ELIM",
426  Term`!P v e. (v = e) /\ P v = (v = e) /\ P e`,
427  REPEAT GEN_TAC THEN EQ_TAC THEN STRIP_TAC THENL [
428    FIRST_X_ASSUM (SUBST1_TAC o SYM) THEN ASM_REWRITE_TAC [],
429    ASM_REWRITE_TAC []
430  ]);
431
432val elim_neg_ones = store_thm(
433  "elim_neg_ones",
434  Term`!x. x + ~1 + 1 = x`,
435  REWRITE_TAC [GSYM INT_ADD_ASSOC, INT_ADD_LINV, INT_ADD_RID]);
436
437val elim_minus_ones = store_thm(
438  "elim_minus_ones",
439  Term`!x:int. (x + 1) - 1 = x`,
440  REWRITE_TAC [int_sub, GSYM INT_ADD_ASSOC, INT_ADD_RINV, INT_ADD_RID]);
441
442open gcdTheory
443
444val INT_NUM_DIVIDES = store_thm(
445  "INT_NUM_DIVIDES",
446  ``!n m. &n int_divides &m = divides n m``,
447  SIMP_TAC bool_ss [INT_DIVIDES, dividesTheory.divides_def, EQ_IMP_THM,
448                    FORALL_AND_THM, GSYM LEFT_FORALL_IMP_THM] THEN
449  REPEAT STRIP_TAC THENL [
450    STRIP_ASSUME_TAC (Q.SPEC `m'` INT_NUM_CASES) THEN
451    FULL_SIMP_TAC bool_ss [INT_MUL_CALCULATE, INT_INJ, INT_EQ_CALCULATE,
452                           MULT_CLAUSES] THENL [
453      PROVE_TAC [],
454      PROVE_TAC [MULT_CLAUSES],
455      PROVE_TAC [MULT_CLAUSES]
456    ],
457    Q.EXISTS_TAC `&q` THEN SIMP_TAC bool_ss [INT_MUL]
458  ]);
459
460val INT_LINEAR_GCD = store_thm(
461  "INT_LINEAR_GCD",
462  ``!n m. ?p:int q. p * &n + q * &m = &(gcd n m)``,
463  REPEAT GEN_TAC THEN
464  Cases_on `n = 0` THENL [
465    POP_ASSUM SUBST1_TAC THEN
466    SIMP_TAC bool_ss [INT_MUL_RZERO, GCD_0L, INT_ADD_LID] THEN
467    PROVE_TAC [INT_MUL_LID],
468    ALL_TAC
469  ] THEN Cases_on `m = 0` THENL [
470    POP_ASSUM SUBST1_TAC THEN
471    SIMP_TAC bool_ss [INT_MUL_RZERO, GCD_0R, INT_ADD_RID] THEN
472    PROVE_TAC [INT_MUL_LID],
473    ALL_TAC
474  ] THEN
475  `?i j. i * n = j * m + gcd m n` by PROVE_TAC [LINEAR_GCD] THEN
476  MAP_EVERY Q.EXISTS_TAC [`&i`, `~&j`] THEN
477  ASM_SIMP_TAC bool_ss [INT_MUL_CALCULATE, GSYM eq_move_left_left,
478                        GCD_SYM, INT_ADD]);
479
480val INT_DIVIDES_LRMUL = store_thm(
481  "INT_DIVIDES_LRMUL",
482  ``!p q r. ~(q = 0) ==> ((p * q) int_divides (r * q) = p int_divides r)``,
483  REPEAT GEN_TAC THEN SIMP_TAC bool_ss [INT_DIVIDES] THEN
484  STRIP_TAC THEN EQ_TAC THEN STRIP_TAC THENL [
485    `(m * p) * q = r * q` by PROVE_TAC [INT_MUL_ASSOC] THEN
486    PROVE_TAC [INT_EQ_RMUL],
487    PROVE_TAC [INT_MUL_ASSOC]
488  ]);
489
490
491val INT_DIVIDES_RELPRIME_MUL = store_thm(
492  "INT_DIVIDES_RELPRIME_MUL",
493  ``!p q r.
494      (gcd p q = 1) ==>
495      (&p int_divides &q * r = &p int_divides r)``,
496  REPEAT STRIP_TAC THEN EQ_TAC THEN STRIP_TAC THENL [
497    STRIP_ASSUME_TAC (Q.SPEC `r` INT_NUM_CASES) THEN
498    FIRST_X_ASSUM SUBST_ALL_TAC THEN
499    FULL_SIMP_TAC bool_ss [INT_NUM_DIVIDES, INT_MUL_CALCULATE,
500                           INT_DIVIDES_NEG] THEN
501    PROVE_TAC [L_EUCLIDES, GCD_SYM],
502    PROVE_TAC [INT_DIVIDES_RMUL]
503  ]);
504
505val INT_MUL_DIV' = prove(
506  ``!p q k.
507       ~(q = 0) /\ q int_divides p ==> (k * (p / q) = k * p / q)``,
508  REPEAT STRIP_TAC THEN
509  FULL_SIMP_TAC bool_ss [INT_DIVIDES_MOD0] THEN FULL_SIMP_TAC bool_ss [] THEN
510  PROVE_TAC [INT_MUL_DIV]);
511
512val fractions = prove(
513  ``!p q r.
514       ~(r = 0) /\ r int_divides p /\ r int_divides q ==>
515       (p / r + q / r = (p + q) / r)``,
516  REPEAT STRIP_TAC THEN
517  `?i. p = i * r` by PROVE_TAC [INT_DIVIDES] THEN POP_ASSUM SUBST1_TAC THEN
518  `?j. q = j * r` by PROVE_TAC [INT_DIVIDES] THEN POP_ASSUM SUBST1_TAC THEN
519  `i * r + j * r = (i + j) * r` by REWRITE_TAC [INT_RDISTRIB] THEN
520  POP_ASSUM SUBST1_TAC THEN
521  ASM_SIMP_TAC bool_ss [INT_MUL_DIV, INT_MOD_ID, INT_DIV_ID, INT_MUL_RID]);
522
523val gcdthm2 = store_thm(
524  "gcdthm2",
525  ``!m:num a:num x b d p q.
526       (d = gcd a m) /\ (&d = p * &a + q * &m) /\ ~(d = 0) /\
527       ~(m = 0) /\ ~(a = 0) ==>
528       (&m int_divides (&a * x) + b =
529        &d int_divides b /\
530        ?t. x = ~p * (b / &d) + t * (&m / &d))``,
531  REPEAT STRIP_TAC THEN EQ_TAC THENL [
532    STRIP_TAC THEN
533    `&d int_divides &a /\ &d int_divides &m` by
534       PROVE_TAC [INT_NUM_DIVIDES, GCD_IS_GCD, is_gcd_def] THEN
535    `&d int_divides &a * x + b` by PROVE_TAC [INT_DIVIDES_TRANS] THEN
536    `&d int_divides &a * x` by PROVE_TAC [INT_DIVIDES_LMUL] THEN
537    `&d int_divides b` by PROVE_TAC [INT_DIVIDES_LADD] THEN CONJ_TAC THENL [
538      ASM_REWRITE_TAC [],
539      ALL_TAC
540    ] THEN  (* existential goal remains *)
541    Cases_on `d = 1` THENL [
542      POP_ASSUM SUBST_ALL_TAC THEN SIMP_TAC bool_ss [INT_DIV_1],
543      `?b'. b = b' * &d` by PROVE_TAC [INT_DIVIDES] THEN
544      POP_ASSUM SUBST_ALL_TAC THEN
545      REPEAT (FIRST_X_ASSUM (MP_TAC o assert (is_eq o concl))) THEN
546      REPEAT (DISCH_THEN (ASSUME_TAC o SYM)) THEN
547      ASM_SIMP_TAC bool_ss [INT_MUL_DIV, INT_MOD_ID, INT_INJ, INT_DIV_ID,
548                            INT_MUL_RID] THEN
549      MP_TAC (Q.SPECL [`m`, `a`] FACTOR_OUT_GCD) THEN
550      ASM_REWRITE_TAC [] THEN
551      DISCH_THEN (Q.X_CHOOSE_THEN `m'`
552                  (Q.X_CHOOSE_THEN `a'` STRIP_ASSUME_TAC)) THEN
553      `gcd m a = d` by PROVE_TAC [GCD_SYM] THEN
554      POP_ASSUM SUBST_ALL_TAC THEN
555      POP_ASSUM MP_TAC THEN
556      NTAC 2 (POP_ASSUM SUBST_ALL_TAC) THEN
557      FULL_SIMP_TAC bool_ss [MULT_EQ_0] THEN
558      ASM_SIMP_TAC bool_ss [INT_MUL_DIV, GSYM INT_MUL, INT_MOD_ID, INT_INJ,
559                            INT_DIV_ID, INT_MUL_RID] THEN
560      FULL_SIMP_TAC bool_ss [GSYM INT_MUL] THEN
561      `&m' int_divides &a' * x + b'` by
562          (`&a' * &d * x = &a' * x * &d` by
563              CONV_TAC(AC_CONV(INT_MUL_ASSOC, INT_MUL_COMM)) THEN
564           POP_ASSUM SUBST_ALL_TAC THEN
565           `&m' * &d int_divides (&a' * x + b') * &d` by
566              ASM_SIMP_TAC bool_ss [INT_RDISTRIB] THEN
567           POP_ASSUM MP_TAC THEN
568           ASM_SIMP_TAC bool_ss [INT_DIVIDES_LRMUL, INT_INJ]) THEN
569      NTAC 2 (POP_ASSUM MP_TAC) THEN POP_ASSUM (K ALL_TAC) THEN
570      REPEAT (Q.PAT_X_ASSUM `y int_divides z` (K ALL_TAC)) THEN
571      Q.PAT_X_ASSUM `T` (K ALL_TAC) THEN
572      REWRITE_TAC [INT_MUL_ASSOC, GSYM INT_RDISTRIB] THEN
573      CONV_TAC (LAND_CONV (RHS_CONV (REWR_CONV (GSYM INT_MUL_LID)))) THEN
574      ASM_SIMP_TAC bool_ss [INT_INJ, INT_EQ_RMUL] THEN
575      REPEAT (DISCH_THEN (ASSUME_TAC o GSYM)) THEN
576      Q.ABBREV_TAC `b = b'` THEN POP_ASSUM (K ALL_TAC) THEN
577      Q.ABBREV_TAC `m = m'` THEN POP_ASSUM (K ALL_TAC) THEN
578      Q.ABBREV_TAC `a = a'` THEN POP_ASSUM (K ALL_TAC) THEN
579      POP_ASSUM (ASSUME_TAC o ONCE_REWRITE_RULE [GCD_SYM])
580    ] THEN
581
582    `b * 1 = b * (p * &a + q * &m)` by (AP_TERM_TAC THEN
583                                        ASM_REWRITE_TAC []) THEN
584    POP_ASSUM (fn th =>
585      `b = b * (p * &a) + b * (q * &m)` by
586          PROVE_TAC [th, INT_LDISTRIB, INT_MUL_RID]) THEN
587    POP_ASSUM (fn th =>
588      `b + ~(b * (q * &m)) = b * (p * &a)` by
589          (MP_TAC th THEN
590           SIMP_TAC bool_ss [GSYM eq_move_left_left] THEN
591           SIMP_TAC bool_ss [INT_ADD_COMM])) THEN
592    POP_ASSUM (fn th =>
593      `&a * (b * p) = b + ~(b * (q * &m))` by
594         (REWRITE_TAC [th] THEN
595          CONV_TAC (AC_CONV(INT_MUL_ASSOC, INT_MUL_COMM)))) THEN
596    POP_ASSUM (fn th =>
597      `&m int_divides &a * (x + b * p)` by
598         (SIMP_TAC bool_ss [INT_LDISTRIB, th] THEN
599          REWRITE_TAC [INT_ADD_ASSOC] THEN
600          ASM_SIMP_TAC bool_ss [INT_DIVIDES_LADD] THEN
601          SIMP_TAC bool_ss [INT_NEG_LMUL, INT_DIVIDES_RMUL,
602                            INT_DIVIDES_REFL])) THEN
603    `&m int_divides x + b*p`
604       by PROVE_TAC [GCD_SYM, INT_DIVIDES_RELPRIME_MUL] THEN
605    `?j. j * &m = x + p * b` by PROVE_TAC [INT_DIVIDES, INT_MUL_COMM] THEN
606    `x = j * &m + ~(p * b)` by PROVE_TAC [eq_move_left_left, INT_ADD_COMM] THEN
607    PROVE_TAC [INT_MUL_CALCULATE, INT_ADD_COMM],
608
609    STRIP_TAC THEN POP_ASSUM SUBST_ALL_TAC THEN
610    REPEAT (FIRST_X_ASSUM (MP_TAC o assert (is_eq o concl))) THEN
611    REPEAT (DISCH_THEN (ASSUME_TAC o SYM)) THEN
612    `&d int_divides &m /\ &d int_divides &a` by
613       PROVE_TAC [INT_NUM_DIVIDES, GCD_IS_GCD, is_gcd_def] THEN
614    REWRITE_TAC [INT_LDISTRIB] THEN
615    `&a * (~p * (b / &d)) = b * (~p * &a / &d)` by
616       (ASM_SIMP_TAC bool_ss [INT_MUL_DIV', INT_DIVIDES_LMUL,
617                              INT_DIVIDES_RMUL, INT_INJ] THEN
618        REPEAT (AP_THM_TAC ORELSE AP_TERM_TAC) THEN
619        CONV_TAC (AC_CONV(INT_MUL_ASSOC, INT_MUL_COMM))) THEN
620    POP_ASSUM SUBST1_TAC THEN
621    `&a * (t * (&m / &d)) = &m * (t * &a / &d)` by
622       (ASM_SIMP_TAC bool_ss [INT_MUL_DIV', INT_DIVIDES_LMUL,
623                              INT_DIVIDES_RMUL, INT_INJ] THEN
624        REPEAT (AP_THM_TAC ORELSE AP_TERM_TAC) THEN
625        CONV_TAC (AC_CONV(INT_MUL_ASSOC, INT_MUL_COMM))) THEN
626    POP_ASSUM SUBST1_TAC THEN
627    `b * (~p * &a / &d) + &m * (t * &a / &d) + b =
628     &m * (t * &a / &d) + b * (1 + ~p * &a / &d)` by
629        (REWRITE_TAC [INT_LDISTRIB, INT_MUL_RID] THEN
630         CONV_TAC (AC_CONV(INT_ADD_ASSOC, INT_ADD_COMM))) THEN
631    POP_ASSUM SUBST1_TAC THEN
632    SIMP_TAC bool_ss [INT_DIVIDES_LADD, INT_DIVIDES_LMUL,
633                      INT_DIVIDES_REFL] THEN
634    Q.SUBGOAL_THEN `1 = &d / &d` SUBST1_TAC THENL [
635      ASM_SIMP_TAC bool_ss [INT_INJ, INT_DIV_ID],
636      ALL_TAC
637    ] THEN
638    ASM_SIMP_TAC bool_ss [fractions, INT_DIVIDES_RMUL, INT_DIVIDES_REFL,
639                          INT_INJ] THEN
640    Q.SUBGOAL_THEN `&d + ~p * &a = q * &m` SUBST1_TAC THENL [
641      REWRITE_TAC [INT_MUL_CALCULATE] THEN
642      PROVE_TAC [eq_move_left_left],
643      ALL_TAC
644    ] THEN
645    Q.SUBGOAL_THEN `b * (q * &m / &d) = &m * (q * b / &d)`
646    (fn th => SUBST1_TAC th THEN
647              SIMP_TAC bool_ss [INT_DIVIDES_LMUL, INT_DIVIDES_REFL]) THEN
648    ASM_SIMP_TAC bool_ss [INT_MUL_DIV', INT_DIVIDES_LMUL, INT_DIVIDES_RMUL,
649                          INT_INJ] THEN
650    REPEAT (AP_TERM_TAC ORELSE AP_THM_TAC) THEN
651    CONV_TAC (AC_CONV(INT_MUL_ASSOC, INT_MUL_COMM))
652  ]);
653
654val gcd1_thm = store_thm(
655  "gcd1thm",
656  ``!m n p q. (p * &m + q * &n = 1i) ==> (gcd m n = 1n)``,
657  REPEAT STRIP_TAC THEN
658  Q.SUBGOAL_THEN `&(gcd m n) int_divides (p * &m + q * &n)` ASSUME_TAC
659  THENL [
660    Q.SUBGOAL_THEN `&(gcd m n) int_divides (p * &m)`
661    (REWRITE_TAC o C cons [] o MATCH_MP INT_DIVIDES_LADD) THENL [
662       Q.SPEC_THEN `p` STRIP_ASSUME_TAC INT_NUM_CASES THEN
663       FIRST_X_ASSUM SUBST_ALL_TAC THEN
664       SIMP_TAC bool_ss [INT_NUM_DIVIDES, INT_MUL_CALCULATE,
665                         INT_DIVIDES_NEG, INT_MUL_LZERO,
666                         ALL_DIVIDES_0] THEN
667       `divides (gcd m n) m` by PROVE_TAC [GCD_IS_GCD, is_gcd_def] THEN
668       PROVE_TAC [DIVIDES_TRANS, DIVIDES_MULT, MULT_COMM],
669
670       Q.SPEC_THEN `q` STRIP_ASSUME_TAC INT_NUM_CASES THEN
671       FIRST_X_ASSUM SUBST_ALL_TAC THEN
672       SIMP_TAC bool_ss [INT_NUM_DIVIDES, INT_MUL_CALCULATE,
673                         INT_DIVIDES_NEG, INT_MUL_LZERO,
674                         ALL_DIVIDES_0] THEN
675       `divides (gcd m n) n` by PROVE_TAC [GCD_IS_GCD, is_gcd_def] THEN
676       PROVE_TAC [DIVIDES_TRANS, DIVIDES_MULT, MULT_COMM]
677    ],
678
679    FIRST_X_ASSUM SUBST_ALL_TAC THEN
680    FULL_SIMP_TAC bool_ss [INT_DIVIDES_1, INT_EQ_CALCULATE]
681  ]);
682
683val gcd21_thm = store_thm(
684  "gcd21_thm",
685  ``!m a x b p q.
686      (p * &a + q * &m = 1i) /\ ~(m = 0) /\ ~(a = 0) ==>
687      (&m int_divides &a * x + b = ?t. x = ~p * b + t * &m)``,
688  REPEAT STRIP_TAC THEN
689  `1 = gcd a m` by PROVE_TAC [gcd1_thm] THEN
690  `~(1n = 0)` by ASM_SIMP_TAC arith_ss []  THEN
691  Q.PAT_X_ASSUM `_ = 1i` (ASSUME_TAC o SYM) THEN
692  Q.SPECL_THEN [`m`, `a`, `x`, `b`, `1`, `p`, `q`] MP_TAC gcdthm2 THEN
693  REPEAT (FIRST_X_ASSUM (MP_TAC o SYM)) THEN
694  ASM_SIMP_TAC bool_ss [INT_DIV_1, INT_DIVIDES_1]);
695
696
697val elim_lt_coeffs1 = store_thm(
698  "elim_lt_coeffs1",
699  ``!n m x:int.  ~(m = 0) ==> (&n < &m * x = &n / &m < x)``,
700  REPEAT STRIP_TAC THEN
701  ASM_SIMP_TAC bool_ss [INT_DIV] THEN
702  `0 < m` by ASM_SIMP_TAC arith_ss [] THEN
703  POP_ASSUM (STRIP_ASSUME_TAC o Q.SPEC `n` o MATCH_MP DIVISION) THEN
704  Q.ABBREV_TAC `r = n MOD m` THEN
705  Q.ABBREV_TAC `i = n DIV m` THEN
706  EQ_TAC THEN STRIP_TAC THENL [
707    SPOSE_NOT_THEN (ASSUME_TAC o REWRITE_RULE [INT_NOT_LT]) THEN
708    Q.SUBGOAL_THEN `&m * x <= &m * &i` ASSUME_TAC THENL [
709      ASM_SIMP_TAC arith_ss [INT_LE_CALCULATE, INT_EQ_LMUL, INT_INJ,
710                             GSYM lt_justify_multiplication, INT_LT] THEN
711      ASM_SIMP_TAC bool_ss [GSYM INT_LE_CALCULATE],
712      ALL_TAC
713    ] THEN
714    `&n < &i * &m` by PROVE_TAC [INT_LTE_TRANS, INT_MUL_COMM] THEN
715    POP_ASSUM MP_TAC THEN ASM_SIMP_TAC arith_ss [INT_LT, INT_MUL],
716
717    Q.SPEC_THEN `x` STRIP_ASSUME_TAC INT_NUM_CASES THEN
718    FIRST_X_ASSUM SUBST_ALL_TAC THEN
719    FULL_SIMP_TAC arith_ss [INT_LT, INT_INJ, INT_LT_CALCULATE, INT_MUL] THEN
720    `i + 1 <= n'` by ASM_SIMP_TAC arith_ss [] THEN
721    POP_ASSUM (MP_TAC o EQ_MP (Q.SPECL [`i + 1`, `n'`, `PRE m`]
722                               MULT_LESS_EQ_SUC)) THEN
723    `~(m = 0)` by ASM_SIMP_TAC arith_ss [] THEN POP_ASSUM MP_TAC THEN
724    SIMP_TAC bool_ss [
725      numLib.ARITH_PROVE ``~(x = 0) ==> (SUC (PRE x) = x)``] THEN
726    Q.SUBGOAL_THEN `i * m = m * i` SUBST1_TAC THENL [
727      CONV_TAC (AC_CONV(MULT_ASSOC, MULT_COMM)),
728      ALL_TAC
729    ] THEN
730    MP_TAC (Q.ASSUME `r:num < m`) THEN
731    SIMP_TAC bool_ss [LEFT_ADD_DISTRIB, MULT_CLAUSES] THEN
732    numLib.ARITH_TAC
733  ]);
734
735val elim_lt_coeffs2 = store_thm(
736  "elim_lt_coeffs2",
737  ``!n m x:int. ~(m = 0) ==>
738                 (&m * x < &n = x < if &m int_divides &n then &n / &m
739                                    else &n / &m + 1)``,
740  REPEAT STRIP_TAC THEN
741  ASM_SIMP_TAC bool_ss [INT_DIV, INT_DIVIDES_MOD0, INT_INJ,
742                        INT_MOD] THEN
743  `0 < m` by ASM_SIMP_TAC arith_ss [] THEN
744  POP_ASSUM (STRIP_ASSUME_TAC o Q.SPEC `n` o MATCH_MP DIVISION) THEN
745  Q.ABBREV_TAC `r = n MOD m` THEN
746  Q.ABBREV_TAC `i = n DIV m` THEN
747  `i * m = m * i` by CONV_TAC (AC_CONV(MULT_ASSOC, MULT_COMM)) THEN
748  POP_ASSUM SUBST_ALL_TAC THEN
749  EQ_TAC THEN COND_CASES_TAC THEN STRIP_TAC THEN
750  REPEAT (FIRST_X_ASSUM SUBST_ALL_TAC) THENL [
751    FULL_SIMP_TAC arith_ss [GSYM INT_MUL] THEN
752    PROVE_TAC [lt_justify_multiplication, INT_LT],
753    FULL_SIMP_TAC arith_ss [GSYM INT_MUL, GSYM INT_ADD] THEN
754    `&m * &i + &r < &m * (&i + 1)` by
755       ASM_SIMP_TAC bool_ss [INT_LDISTRIB, INT_LT_LADD, INT_LT,
756                             INT_MUL_RID] THEN
757    `&m * x < &m * (&i + 1)` by PROVE_TAC [INT_LT_TRANS] THEN
758    `0i < &m` by ASM_SIMP_TAC arith_ss [INT_LT] THEN
759    PROVE_TAC [lt_justify_multiplication],
760    REWRITE_TAC [GSYM INT_MUL, GSYM INT_ADD, INT_ADD_RID] THEN
761    PROVE_TAC [lt_justify_multiplication, INT_LT],
762    `x <= &i` by ASM_SIMP_TAC bool_ss [GSYM INT_NOT_LT, not_less] THEN
763    `&m * x <= &m * &i` by
764       (FULL_SIMP_TAC bool_ss [INT_LE_CALCULATE, INT_EQ_LMUL, INT_INJ] THEN
765        ASM_SIMP_TAC arith_ss [INT_LT, GSYM lt_justify_multiplication]) THEN
766    `&m * &i < &(m * i + r)` by
767       ASM_SIMP_TAC arith_ss [INT_LT, INT_MUL] THEN
768    PROVE_TAC [INT_LET_TRANS]
769  ]);
770
771val elim_le_coeffs = store_thm(
772  "elim_le_coeffs",
773  ``!m n x.  0 < m ==> (0 <= m * x + n = 0 <= x + n/m)``,
774  REPEAT STRIP_TAC THEN
775  `~(m = 0) /\ ~(m < 0)` by PROVE_TAC [INT_LT_REFL, INT_LT_ANTISYM] THEN
776  Q.SPEC_THEN `m` MP_TAC INT_DIVISION THEN
777  ASM_SIMP_TAC arith_ss [] THEN
778  DISCH_THEN (Q.SPEC_THEN `n` STRIP_ASSUME_TAC) THEN
779  Q.ABBREV_TAC `q = n / m` THEN POP_ASSUM (K ALL_TAC) THEN
780  Q.ABBREV_TAC `r = n % m` THEN POP_ASSUM (K ALL_TAC) THEN
781  FIRST_X_ASSUM SUBST_ALL_TAC THEN
782  SIMP_TAC arith_ss [INT_ADD_ASSOC, INT_MUL_COMM, GSYM INT_LDISTRIB] THEN
783  EQ_TAC THEN STRIP_TAC THENL [
784    `0 < m * (x + q) + m * 1` by
785        (MATCH_MP_TAC INT_LET_TRANS THEN
786         Q.EXISTS_TAC `m * (x + q) + r` THEN
787         ASM_SIMP_TAC arith_ss [INT_LT_LADD, INT_MUL_RID]) THEN
788    `0 < m * (x + q + 1)` by PROVE_TAC [INT_LDISTRIB] THEN
789    `0 < x + q + 1` by PROVE_TAC [INT_LT_MONO, INT_MUL_RZERO] THEN
790    PROVE_TAC [elim_minus_ones, int_sub, less_to_leq_samel],
791    MATCH_MP_TAC INT_LE_TRANS THEN Q.EXISTS_TAC `m * (x + q)` THEN
792    PROVE_TAC [INT_LE_MONO, INT_MUL_RZERO, INT_LE_ADDR]
793  ]);
794
795val elim_eq_coeffs = store_thm(
796  "elim_eq_coeffs",
797  ``!m x y.  ~(m = 0) ==>
798             ((&m * x = y) = &m int_divides y /\ (x = y / &m))``,
799  REPEAT STRIP_TAC THEN
800  ASM_SIMP_TAC bool_ss [INT_DIVIDES] THEN EQ_TAC THEN STRIP_TAC THENL [
801    POP_ASSUM (SUBST_ALL_TAC o SYM) THEN CONJ_TAC THENL [
802      PROVE_TAC [INT_MUL_COMM],
803      ALL_TAC
804    ] THEN ONCE_REWRITE_TAC [INT_MUL_COMM] THEN
805    ASM_SIMP_TAC bool_ss [INT_MUL_DIV, INT_INJ, INT_MOD_ID, INT_DIV_ID,
806                          INT_MUL_RID],
807    POP_ASSUM SUBST_ALL_TAC THEN POP_ASSUM (SUBST_ALL_TAC o SYM) THEN
808    ASM_SIMP_TAC bool_ss [INT_MUL_DIV, INT_INJ, INT_MOD_ID, INT_DIV_ID,
809                          INT_MUL_RID] THEN
810    PROVE_TAC [INT_MUL_COMM]
811  ]);
812
813
814val int_acnorm_ss = SSFRAG{
815  name = SOME "int_acnorm",
816  ac = [(SPEC_ALL INT_ADD_ASSOC, SPEC_ALL INT_ADD_COMM),
817        (SPEC_ALL INT_MUL_ASSOC, SPEC_ALL INT_MUL_COMM)],
818  convs = [], congs = [], dprocs = [], filter = NONE,
819  rewrs = []};
820
821(* lemma 1 from Cooper's paper
822
823     (d = gcd(um, an) = pum + qan) ==>
824     ( m | ax + b /\ n | ux + v =
825        mn | dx + bqn + vpm /\ d | av - ub )
826*)
827val adhoc_lemma = prove(
828  ``!a b c.  a + (b - c) = (a - c) + b:int``,
829  SIMP_TAC (bool_ss ++ int_acnorm_ss) [INT_SUB_CALCULATE]);
830val adhoc_lemma2 = prove(
831  ``!a b c.  a - b + c = a + (c - b:int)``,
832  SIMP_TAC (bool_ss ++ int_acnorm_ss) [INT_SUB_CALCULATE]);
833
834
835val cooper_lemma_1 = store_thm(
836  "cooper_lemma_1",
837  ``!m n a b u v p q x d.
838       (d = gcd (u * m) (a * n)) /\
839       (&d = p * &u * &m + q * &a * &n) /\
840       ~(m = 0) /\ ~(n = 0) /\ ~(a = 0) /\ ~(u = 0) ==>
841       (&m int_divides &a * x + b /\ &n int_divides &u * x + v =
842        &m * &n int_divides &d * x + v * &m * p + b * &n * q /\
843        &d int_divides &a * v - &u * b)``,
844  REPEAT STRIP_TAC THEN
845  EQ_TAC THEN REPEAT STRIP_TAC THENL [
846    (* m | ax + b /\ n | ux + v ==> mn | dx + vmp + bnq *)
847    `&m * &n int_divides (&a * x + b) * &n` by
848        PROVE_TAC [INT_INJ, INT_DIVIDES_LRMUL] THEN
849    `&m * &n int_divides (&u * x + v) * &m` by
850        PROVE_TAC [INT_INJ, INT_MUL_COMM, INT_DIVIDES_LRMUL] THEN
851    `&m * &n int_divides (&a * x + b) * &n * q` by
852        PROVE_TAC [INT_DIVIDES_LMUL] THEN
853    `&m * &n int_divides (&u * x + v) * &m * p` by
854        PROVE_TAC [INT_DIVIDES_LMUL] THEN
855    `&m * &n int_divides (&a * x + b) * &n * q + (&u * x + v) * &m * p` by
856        PROVE_TAC [INT_DIVIDES_LADD] THEN
857    `&m * &n int_divides &a * x * &n * q + b * &n * q +
858                         &u * x * &m * p + v * &m * p` by
859        (POP_ASSUM MP_TAC THEN
860         SIMP_TAC bool_ss [INT_RDISTRIB, INT_ADD_ASSOC]) THEN
861    `&m * &n int_divides (p * &u * &m + q * &a * &n) * x +
862                         v * &m * p + b * &n * q` by
863        (POP_ASSUM MP_TAC THEN
864         SIMP_TAC (bool_ss ++ int_acnorm_ss)[INT_LDISTRIB, INT_RDISTRIB]) THEN
865    POP_ASSUM MP_TAC THEN ASM_SIMP_TAC bool_ss [],
866    (* m | ax + b /\ n | ux + v ==> d | av - ub *)
867    `?j. &m * j = &a * x + b` by PROVE_TAC [INT_DIVIDES, INT_MUL_COMM] THEN
868    `?k. &n * k = &u * x + v` by PROVE_TAC [INT_DIVIDES, INT_MUL_COMM] THEN
869    `b = &m * j - &a * x` by
870        PROVE_TAC [INT_EQ_SUB_LADD, INT_ADD_COMM] THEN
871    `v = &n * k - &u * x` by
872        PROVE_TAC [INT_EQ_SUB_LADD, INT_ADD_COMM] THEN
873    `&u * b = &u * &m * j - &u * &a * x` by
874        PROVE_TAC [INT_SUB_LDISTRIB, INT_MUL_ASSOC] THEN
875    `&a * v = &a * &n * k - &a * &u * x` by
876        PROVE_TAC [INT_SUB_LDISTRIB, INT_MUL_ASSOC] THEN
877    `&a * v = &a * &n * k - &u * &a * x` by
878        (POP_ASSUM MP_TAC THEN SIMP_TAC (bool_ss ++ int_acnorm_ss)[]) THEN
879    `&a * v - &u * b = &a * &n * k - &u * &m * j` by
880        ASM_SIMP_TAC bool_ss [INT_SUB_SUB3, INT_SUB_ADD] THEN
881    `&d int_divides &u * &m /\ &d int_divides &a * &n` by
882        PROVE_TAC [is_gcd_def, GCD_IS_GCD, INT_NUM_DIVIDES, INT_MUL] THEN
883    `&d int_divides &u * &m * j /\ &d int_divides &a * &n * k` by
884        PROVE_TAC [INT_DIVIDES_LMUL, INT_MUL_ASSOC] THEN
885    `&d int_divides &a * &n * k - &u * &m * j` by
886        PROVE_TAC [INT_DIVIDES_LSUB] THEN
887    PROVE_TAC [],
888    (* mn | dx + vmp + bnq /\ d | av - ub ==> m | ax + b *)
889    Q.PAT_X_ASSUM `&m * &n int_divides &d * x + v * &m * p + b * &n * q`
890       ASSUME_TAC THEN
891    `&m * &n int_divides &m * p * (&u * x + v) + &n * q * (&a * x + b)` by
892       (POP_ASSUM MP_TAC THEN
893        ASM_SIMP_TAC (bool_ss ++ int_acnorm_ss)
894                     [INT_LDISTRIB, INT_RDISTRIB]) THEN
895    `&a * &u * &m * &n int_divides
896         &u * &m * p * (&u * &a * x + &a * v) +
897         &a * &n * q * (&u * &a * x + &u * b)` by
898       (`~(&a * &u = 0)` by PROVE_TAC [INT_ENTIRE, INT_INJ, INT_MUL] THEN
899        `(&a * &u) * (&m * &n) int_divides
900             (&a * &u) * (&m * p * (&u * x + v) + &n * q * (&a * x + b))` by
901           PROVE_TAC [INT_DIVIDES_LRMUL, INT_MUL_COMM] THEN
902        POP_ASSUM MP_TAC THEN
903        SIMP_TAC (bool_ss ++ int_acnorm_ss)[INT_LDISTRIB]) THEN
904    `&a * &n * q = &d - &u * &m * p` by
905       (FULL_SIMP_TAC (bool_ss ++ int_acnorm_ss) [] THEN
906        PROVE_TAC [INT_EQ_SUB_RADD, INT_ADD_COMM]) THEN
907    POP_ASSUM SUBST_ALL_TAC THEN
908    POP_ASSUM (ASSUME_TAC o REWRITE_RULE [INT_SUB_RDISTRIB, adhoc_lemma]) THEN
909    POP_ASSUM (ASSUME_TAC o REWRITE_RULE [GSYM INT_SUB_LDISTRIB,
910                                          INT_ADD2_SUB2, INT_ADD_LID,
911                                          INT_SUB_REFL,
912                                          INT_MUL_RZERO]) THEN
913    `&u * (&a * &m * &n) int_divides
914        &u * (&m * p * (&a * v - &u * b) + &d * (&a * x + b))` by
915      (POP_ASSUM MP_TAC THEN
916       SIMP_TAC (bool_ss ++ int_acnorm_ss) [INT_LDISTRIB]) THEN
917    `&a * &m * &n int_divides
918         &m * p * (&a * v - &u * b) + &d * (&a * x + b)` by
919       PROVE_TAC [INT_DIVIDES_LRMUL, INT_INJ, INT_MUL_COMM] THEN
920    `?k. &d * k = &a * v - &u * b` by
921       PROVE_TAC [INT_DIVIDES, INT_MUL_COMM] THEN
922    `&d int_divides &a * &n` by
923       PROVE_TAC [GCD_IS_GCD, is_gcd_def, INT_MUL, INT_NUM_DIVIDES] THEN
924    `?l. &d * l = &a * &n` by
925       PROVE_TAC [INT_DIVIDES, INT_MUL_COMM] THEN
926    `&a * &m * &n int_divides
927         &d * k * &m * p + &d * (&a * x + b)` by
928       (Q.PAT_X_ASSUM `&a * &m * &n int_divides Y` MP_TAC THEN
929        Q.PAT_X_ASSUM `&d * k = X` SUBST1_TAC THEN
930        SIMP_TAC (bool_ss ++ int_acnorm_ss)[]) THEN
931    `&d * l * &m int_divides
932         &d * k * &m * p + &d * (&a * x + b)` by
933       (POP_ASSUM MP_TAC THEN POP_ASSUM SUBST1_TAC THEN
934        SIMP_TAC (bool_ss ++ int_acnorm_ss)[]) THEN
935    `&m * l int_divides k * &m * p + (&a * x + b)` by
936       (POP_ASSUM MP_TAC THEN
937        `~(&d = 0)` by PROVE_TAC [INT_INJ, GCD_EQ_0, MULT_EQ_0] THEN
938        REWRITE_TAC [GSYM INT_MUL_ASSOC, GSYM INT_LDISTRIB] THEN
939        DISCH_THEN (MP_TAC o
940                    CONV_RULE (BINOP_CONV (REWR_CONV INT_MUL_COMM))) THEN
941        POP_ASSUM MP_TAC THEN
942        SIMP_TAC (bool_ss ++ int_acnorm_ss) [INT_DIVIDES_LRMUL]) THEN
943    `&m int_divides k * &m * p + (&a * x + b)` by
944        PROVE_TAC [INT_DIVIDES_MUL, INT_DIVIDES_TRANS] THEN
945    `&m int_divides k * &m * p` by
946        PROVE_TAC [INT_DIVIDES_MUL, INT_MUL_COMM, INT_MUL_ASSOC] THEN
947    PROVE_TAC [INT_DIVIDES_LADD],
948    (* mn | dx + vmp + bnq /\ d | av - ub ==> n | ux + v *)
949    Q.PAT_X_ASSUM `&m * &n int_divides &d * x + v * &m * p + b * &n * q`
950       ASSUME_TAC THEN
951    `&m * &n int_divides &m * p * (&u * x + v) + &n * q * (&a * x + b)` by
952       (POP_ASSUM MP_TAC THEN
953        ASM_SIMP_TAC (bool_ss ++ int_acnorm_ss)
954                     [INT_LDISTRIB, INT_RDISTRIB]) THEN
955    `&a * &u * &m * &n int_divides
956         &u * &m * p * (&u * &a * x + &a * v) +
957         &a * &n * q * (&u * &a * x + &u * b)` by
958       (`~(&a * &u = 0)` by PROVE_TAC [INT_ENTIRE, INT_INJ, INT_MUL] THEN
959        `(&a * &u) * (&m * &n) int_divides
960             (&a * &u) * (&m * p * (&u * x + v) + &n * q * (&a * x + b))` by
961           PROVE_TAC [INT_DIVIDES_LRMUL, INT_MUL_COMM] THEN
962        POP_ASSUM MP_TAC THEN
963        SIMP_TAC (bool_ss ++ int_acnorm_ss)[INT_LDISTRIB]) THEN
964    `&u * &m * p = &d - &a * &n * q` by
965       (FULL_SIMP_TAC (bool_ss ++ int_acnorm_ss) [] THEN
966        PROVE_TAC [INT_EQ_SUB_RADD, INT_ADD_COMM]) THEN
967    POP_ASSUM SUBST_ALL_TAC THEN
968    POP_ASSUM (ASSUME_TAC o REWRITE_RULE [INT_SUB_RDISTRIB, adhoc_lemma2]) THEN
969    POP_ASSUM (ASSUME_TAC o REWRITE_RULE [GSYM INT_SUB_LDISTRIB,
970                                          INT_ADD2_SUB2, INT_ADD_LID,
971                                          INT_SUB_REFL,
972                                          INT_MUL_RZERO]) THEN
973    `&a * (&u * &m * &n) int_divides
974        &a * (&n * q * (&u * b - &a * v) + &d * (&u * x + v))` by
975      (POP_ASSUM MP_TAC THEN
976       SIMP_TAC (bool_ss ++ int_acnorm_ss) [INT_LDISTRIB]) THEN
977    `&u * &m * &n int_divides
978         &n * q * (&u * b - &a * v) + &d * (&u * x + v)` by
979       PROVE_TAC [INT_DIVIDES_LRMUL, INT_INJ, INT_MUL_COMM] THEN
980    `?k. &d * k = &u * b - &a * v` by
981       PROVE_TAC [INT_DIVIDES, INT_MUL_COMM, INT_DIVIDES_NEG,
982                  INT_NEG_SUB] THEN
983    `&d int_divides &u * &m` by
984       PROVE_TAC [GCD_IS_GCD, is_gcd_def, INT_MUL, INT_NUM_DIVIDES] THEN
985    `?l. &d * l = &u * &m` by
986       PROVE_TAC [INT_DIVIDES, INT_MUL_COMM] THEN
987    `&u * &m * &n int_divides
988         &d * k * &n * q + &d * (&u * x + v)` by
989       (Q.PAT_X_ASSUM `&u * &m * &n int_divides Y` MP_TAC THEN
990        Q.PAT_X_ASSUM `&d * k = X` SUBST1_TAC THEN
991        SIMP_TAC (bool_ss ++ int_acnorm_ss)[]) THEN
992    `&d * l * &n int_divides
993         &d * k * &n * q + &d * (&u * x + v)` by
994       (POP_ASSUM MP_TAC THEN POP_ASSUM SUBST1_TAC THEN
995        SIMP_TAC (bool_ss ++ int_acnorm_ss)[]) THEN
996    `&n * l int_divides k * &n * q + (&u * x + v)` by
997       (POP_ASSUM MP_TAC THEN
998        `~(&d = 0)` by PROVE_TAC [INT_INJ, GCD_EQ_0, MULT_EQ_0] THEN
999        REWRITE_TAC [GSYM INT_MUL_ASSOC, GSYM INT_LDISTRIB] THEN
1000        DISCH_THEN (MP_TAC o
1001                    CONV_RULE (BINOP_CONV (REWR_CONV INT_MUL_COMM))) THEN
1002        POP_ASSUM MP_TAC THEN
1003        SIMP_TAC (bool_ss ++ int_acnorm_ss) [INT_DIVIDES_LRMUL]) THEN
1004    `&n int_divides k * &n * q + (&u * x + v)` by
1005        PROVE_TAC [INT_DIVIDES_MUL, INT_DIVIDES_TRANS] THEN
1006    `&n int_divides k * &n * q` by
1007        PROVE_TAC [INT_DIVIDES_MUL, INT_MUL_COMM, INT_MUL_ASSOC] THEN
1008    PROVE_TAC [INT_DIVIDES_LADD]
1009  ]);
1010
1011val bmarker_def = new_definition(
1012  "bmarker_def",
1013  ``bmarker (b:bool) = b``);
1014
1015val bmarker_rewrites = store_thm(
1016  "bmarker_rewrites",
1017  ``!p q r. (q /\ bmarker p = bmarker p /\ q) /\
1018            (q /\ (bmarker p /\ r) = bmarker p /\ (q /\ r)) /\
1019            ((bmarker p /\ q) /\ r = bmarker p /\ (q /\ r))``,
1020  REWRITE_TAC [bmarker_def] THEN tautLib.TAUT_TAC);
1021
1022val positive_mod_part = prove(
1023  ``!p q r. 0 < q /\ 0 <= r /\ r < q ==>
1024            ((p * q + r) % q = r)``,
1025  REPEAT STRIP_TAC THEN MATCH_MP_TAC INT_MOD_UNIQUE THEN
1026  ASM_SIMP_TAC bool_ss [INT_LT_GT] THEN PROVE_TAC []);
1027
1028infix 8 on
1029val int_ss = srw_ss() ++ numSimps.ARITH_ss
1030val tac1 =
1031    Q.EXISTS_TAC `&n - r` THEN
1032    ASM_SIMP_TAC bool_ss [INT_LE_SUB_LADD, INT_LE_SUB_RADD, move_sub,
1033                          INT_LE_LADD] THEN
1034    `0 < r` by FULL_SIMP_TAC bool_ss [INT_LE_LT] THEN
1035    FULL_SIMP_TAC int_ss [GSYM INT_ADD_ASSOC, INT_SUB_ADD2,
1036                           less_to_leq_samer, INT_ADD_COMM] THEN
1037    SUBST_ALL_TAC on
1038      (`&n + q * &n = (q + 1) * &n`,
1039       SIMP_TAC bool_ss [INT_ADD_COMM, INT_RDISTRIB, INT_MUL_LID]) THEN
1040    ASM_SIMP_TAC int_ss [INT_MOD_COMMON_FACTOR]
1041val tac2 =
1042    STRIP_TAC THEN REPEAT VAR_EQ_TAC THEN
1043    FULL_SIMP_TAC bool_ss [INT_ADD_RID] THEN
1044    POP_ASSUM MP_TAC THEN
1045    `0 <= i` by PROVE_TAC [INT_LE_TRANS, INT_LE_01] THEN
1046    `i < &n` by ASM_SIMP_TAC bool_ss [less_to_leq_samel, GSYM int_sub] THEN
1047    ASM_SIMP_TAC bool_ss [positive_mod_part] THEN
1048    STRIP_TAC THEN VAR_EQ_TAC THEN FULL_SIMP_TAC int_ss []
1049val NOT_INT_DIVIDES = store_thm(
1050  "NOT_INT_DIVIDES",
1051  ``!c d. ~(c = 0) ==>
1052          (~(c int_divides d) =
1053           ?i. 1 <= i /\ i <= ABS c - 1 /\ c int_divides d + i)``,
1054  REPEAT GEN_TAC THEN
1055  Q.SPEC_THEN `c` STRIP_ASSUME_TAC INT_NUM_CASES THEN
1056  ASM_SIMP_TAC bool_ss [INT_DIVIDES_NEG, INT_ABS_NUM, INT_ABS_NEG,
1057                        INT_NEG_EQ0] THEN
1058  REPEAT STRIP_TAC THEN
1059  ASM_SIMP_TAC bool_ss [INT_DIVIDES_MOD0] THEN
1060  FIRST_ASSUM (MP_TAC o Q.SPEC `d` o MATCH_MP INT_DIVISION) THEN
1061  ASM_SIMP_TAC int_ss [INT_LT] THEN STRIP_TAC THEN
1062  Q.ABBREV_TAC `q = d / &n` THEN POP_ASSUM (K ALL_TAC) THEN
1063  Q.ABBREV_TAC `r = d % &n` THEN POP_ASSUM (K ALL_TAC) THEN
1064  EQ_TAC THEN STRIP_TAC THENL [tac1,tac2,tac1,tac2]);
1065
1066val NOT_INT_DIVIDES_POS = store_thm(
1067  "NOT_INT_DIVIDES_POS",
1068  ``!n d. ~(n = 0) ==>
1069          (~(&n int_divides d) =
1070           ?i. (1 <= i /\ i <= &n - 1) /\ &n int_divides d + i)``,
1071  REPEAT STRIP_TAC THEN
1072  `~(&n = 0)` by ASM_SIMP_TAC bool_ss [INT_INJ] THEN
1073  ASM_SIMP_TAC bool_ss [NOT_INT_DIVIDES, INT_ABS_NUM, CONJ_ASSOC]);
1074
1075val le_context_rwt1 = store_thm(
1076  "le_context_rwt1",
1077  ``0 <= c + x ==> x <= y ==> (0 <= c + y = T)``,
1078  PROVE_TAC [INT_LE_LADD, INT_ADD_COMM, INT_ADD_ASSOC, INT_LE_ADD2,
1079             INT_ADD_LID]);
1080
1081val le_context_rwt2 = store_thm(
1082  "le_context_rwt2",
1083  ``0 <= c + x ==> y < ~x ==> (0 <= ~c + y = F)``,
1084  REWRITE_TAC [] THEN REPEAT STRIP_TAC THEN
1085  `c <= y` by PROVE_TAC [le_move_all_right, INT_ADD_COMM] THEN
1086  `~x <= c` by PROVE_TAC [INT_NEGNEG, le_move_all_right, INT_ADD_COMM] THEN
1087  PROVE_TAC [INT_LE_TRANS, INT_NOT_LE]);
1088
1089val le_context_rwt3 = store_thm(
1090  "le_context_rwt3",
1091  ``0 <= c + x ==> x < y ==> ((0 = c + y) = F)``,
1092  REWRITE_TAC [] THEN REPEAT STRIP_TAC THEN
1093  PROVE_TAC [INT_LE_LADD, INT_LET_TRANS, INT_LT_REFL]);
1094
1095val le_context_rwt4 = store_thm(
1096  "le_context_rwt4",
1097  ``0 <= c + x ==> x < ~y  ==> ((0 = ~c + y) = F)``,
1098  REWRITE_TAC [] THEN REPEAT STRIP_TAC THEN
1099  POP_ASSUM (SUBST_ALL_TAC o
1100             REWRITE_RULE [INT_NEG_0, INT_NEG_ADD, INT_NEGNEG] o
1101             AP_TERM ``$~ : int -> int``) THEN
1102  PROVE_TAC [INT_LE_LADD, INT_LET_TRANS, INT_LT_REFL]);
1103
1104val le_context_rwt5 = store_thm(
1105  "le_context_rwt5",
1106  ``0 <= c + x ==> (0 <= ~c + ~x = (0 = c + x))``,
1107  STRIP_TAC THEN EQ_TAC THEN STRIP_TAC THENL [
1108    POP_ASSUM (ASSUME_TAC o REWRITE_RULE [INT_NEG_0, INT_NEG_ADD, INT_NEGNEG] o
1109               CONV_RULE (REWR_CONV (GSYM INT_LE_NEG))) THEN
1110    IMP_RES_TAC INT_LE_ANTISYM,
1111    POP_ASSUM (SUBST_ALL_TAC o
1112               REWRITE_RULE [INT_NEG_0, INT_NEG_ADD, INT_NEGNEG] o
1113               AP_TERM ``$~ : int -> int``) THEN
1114    REWRITE_TAC [INT_LE_REFL]
1115  ]);
1116
1117
1118val eq_context_rwt1 = store_thm(
1119  "eq_context_rwt1",
1120  ``(0i = c + x) ==> (0 <= c + y = x <= y)``,
1121  STRIP_TAC THEN ASM_REWRITE_TAC [INT_LE_LADD]);
1122
1123val eq_context_rwt2 = store_thm(
1124  "eq_context_rwt2",
1125  ``(0 = c + x) ==> (0 <= ~c + y = ~x <= y)``,
1126  STRIP_TAC THEN
1127  POP_ASSUM (ASSUME_TAC o REWRITE_RULE [INT_NEG_0, INT_NEG_ADD] o
1128             AP_TERM ``$~ : int -> int``) THEN
1129  ASM_REWRITE_TAC [INT_LE_LADD]);
1130
1131val _ = hide "bmarker";
1132
1133val _ = export_theory();
1134