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