1(* interactive mode 2loadPath := ["../ho_prover","../subtypes","../rsa"] @ !loadPath; 3app load ["bossLib","subtypeTheory","HurdUseful","extra_boolTheory"]; 4quietdec := true; 5*) 6 7open HolKernel Parse boolLib bossLib arithmeticTheory HurdUseful 8 pred_setTheory subtypeTheory extra_boolTheory combinTheory; 9 10(* 11quietdec := false; 12*) 13 14val _ = new_theory "extra_num"; 15 16infixr 0 ++ << || THENC ORELSEC ORELSER ##; 17infix 1 >>; 18 19val op!! = op REPEAT; 20val op++ = op THEN; 21val op<< = op THENL; 22val op|| = op ORELSE; 23val op>> = op THEN1; 24 25(* ------------------------------------------------------------------------- *) 26(* Tools. *) 27(* ------------------------------------------------------------------------- *) 28 29val Strip = !! STRIP_TAC; 30val Simplify = RW_TAC arith_ss; 31val bool_ss = boolSimps.bool_ss; 32 33(* ------------------------------------------------------------------------- *) 34(* Needed for definitions. *) 35(* ------------------------------------------------------------------------- *) 36 37val DIV_THEN_MULT = store_thm 38 ("DIV_THEN_MULT", 39 ``!p q. SUC q * (p DIV SUC q) <= p``, 40 NTAC 2 STRIP_TAC 41 ++ Know `?r. p = (p DIV SUC q) * SUC q + r` 42 >> (Know `0 < SUC q` >> DECIDE_TAC 43 ++ PROVE_TAC [DIVISION]) 44 ++ STRIP_TAC 45 ++ Suff `p = SUC q * (p DIV SUC q) + r` 46 >> (KILL_TAC ++ DECIDE_TAC) 47 ++ PROVE_TAC [MULT_COMM]); 48 49(* ------------------------------------------------------------------------- *) 50(* Definitions. *) 51(* ------------------------------------------------------------------------- *) 52 53val min_def = Define `min (m:num) n = if m <= n then m else n`; 54 55val gtnum_def = Define `gtnum (n : num) x = n < x`; 56 57val (log2_def, log2_ind) = Defn.tprove 58 let val d = Hol_defn "log2" 59 `(log2 0 = 0) 60 /\ (log2 n = SUC (log2 (n DIV 2)))` 61 val g = `measure (\x. x)` 62 in (d, 63 WF_REL_TAC g 64 ++ STRIP_TAC 65 ++ Know `2 * (SUC v DIV 2) <= SUC v` 66 >> PROVE_TAC [TWO, DIV_THEN_MULT] 67 ++ DECIDE_TAC) 68 end; 69 70val _ = save_thm ("log2_def", log2_def); 71val _ = save_thm ("log2_ind", log2_ind); 72 73(* ------------------------------------------------------------------------- *) 74(* Theorems. *) 75(* ------------------------------------------------------------------------- *) 76 77val SUC_0 = store_thm 78 ("SUC_0", 79 ``SUC 0 = 1``, 80 DECIDE_TAC); 81 82val LESS_0_MULT2 = store_thm 83 ("LESS_0_MULT2", 84 ``!m n : num. 0 < m * n = 0 < m /\ 0 < n``, 85 !! STRIP_TAC 86 ++ Cases_on `m` >> RW_TAC arith_ss [] 87 ++ Cases_on `n` >> RW_TAC arith_ss [] 88 ++ RW_TAC arith_ss [MULT]); 89 90val LESS_1_MULT2 = store_thm 91 ("LESS_1_MULT2", 92 ``!m n : num. 1 < m /\ 1 < n ==> 1 < m * n``, 93 !! STRIP_TAC 94 ++ Suff `~(m * n = 0) /\ ~(m * n = 1)` >> DECIDE_TAC 95 ++ CONJ_TAC 96 ++ ONCE_REWRITE_TAC [MULT_EQ_0, MULT_EQ_1] 97 ++ DECIDE_TAC); 98 99val FUNPOW_SUC = store_thm 100 ("FUNPOW_SUC", 101 ``!f n x. FUNPOW f (SUC n) x = f (FUNPOW f n x)``, 102 Induct_on `n` >> RW_TAC std_ss [FUNPOW] 103 ++ ONCE_REWRITE_TAC [FUNPOW] 104 ++ RW_TAC std_ss []); 105 106val EVEN_ODD_BASIC = store_thm 107 ("EVEN_ODD_BASIC", 108 ``EVEN 0 /\ ~EVEN 1 /\ EVEN 2 /\ ~ODD 0 /\ ODD 1 /\ ~ODD 2``, 109 CONV_TAC (TOP_DEPTH_CONV Num_conv.num_CONV) 110 ++ RW_TAC arith_ss [EVEN, ODD]); 111 112val EVEN_ODD_EXISTS_EQ = store_thm 113 ("EVEN_ODD_EXISTS_EQ", 114 ``!n. (EVEN n = ?m. n = 2 * m) /\ (ODD n = ?m. n = SUC (2 * m))``, 115 PROVE_TAC [EVEN_ODD_EXISTS, EVEN_DOUBLE, ODD_DOUBLE]); 116 117val MOD_1 = store_thm 118 ("MOD_1", 119 ``!n : num. n MOD 1 = 0``, 120 PROVE_TAC [SUC_0, MOD_ONE]); 121 122val DIV_1 = store_thm 123 ("DIV_1", 124 ``!n : num. n DIV 1 = n``, 125 PROVE_TAC [SUC_0, DIV_ONE]); 126 127val MOD_LESS = store_thm 128 ("MOD_LESS", 129 ``!n k : num. 0 < n ==> k MOD n < n``, 130 PROVE_TAC [DIVISION]); 131 132val X_MOD_X = store_thm 133 ("X_MOD_X", 134 ``!n. 0 < n ==> (n MOD n = 0)``, PROVE_TAC [DIVMOD_ID]); 135 136val LESS_MOD_EQ = store_thm 137 ("LESS_MOD_EQ", 138 ``!x n. x < n ==> (x MOD n = x)``, 139 REPEAT STRIP_TAC 140 ++ MP_TAC (Q.SPECL [`x`, `n`] LESS_DIV_EQ_ZERO) 141 ++ ASM_REWRITE_TAC [] 142 ++ STRIP_TAC 143 ++ MP_TAC (Q.SPEC `n` DIVISION) 144 ++ Know `0 < n` >> DECIDE_TAC 145 ++ STRIP_TAC 146 ++ ASM_REWRITE_TAC [] 147 ++ DISCH_THEN (MP_TAC o Q.SPEC `x`) 148 ++ RW_TAC arith_ss []); 149 150val MOD_PLUS1 = store_thm 151 ("MOD_PLUS1", 152 ``!n a b. 0 < n ==> ((a MOD n + b) MOD n = (a + b) MOD n)``, 153 RW_TAC arith_ss [] 154 ++ MP_TAC (Q.SPEC `n` MOD_PLUS) 155 ++ ASM_REWRITE_TAC [] 156 ++ DISCH_THEN (fn th => ONCE_REWRITE_TAC [GSYM th]) 157 ++ RW_TAC arith_ss [MOD_MOD]); 158 159val MOD_PLUS2 = store_thm 160 ("MOD_PLUS2", 161 ``!n a b. 0 < n ==> ((a + b MOD n) MOD n = (a + b) MOD n)``, 162 PROVE_TAC [MOD_PLUS1, ADD_COMM]); 163 164val MOD_MULT1 = store_thm 165 ("MOD_MULT1", 166 ``!n a b. 0 < n ==> ((a MOD n * b) MOD n = (a * b) MOD n)``, 167 RW_TAC std_ss [] 168 ++ Induct_on `b` >> RW_TAC arith_ss [MULT_CLAUSES] 169 ++ RW_TAC std_ss [MULT_CLAUSES] 170 ++ MP_TAC (Q.SPEC `n` (GSYM MOD_PLUS2)) 171 ++ ASM_REWRITE_TAC [] 172 ++ DISCH_THEN (fn th => ONCE_REWRITE_TAC [th]) 173 ++ RW_TAC std_ss [] 174 ++ MP_TAC (Q.SPEC `n` MOD_PLUS1) 175 ++ ASM_REWRITE_TAC [] 176 ++ DISCH_THEN (fn th => ONCE_REWRITE_TAC [th]) 177 ++ RW_TAC std_ss []); 178 179val MOD_MULT2 = store_thm 180 ("MOD_MULT2", 181 ``!n a b. 0 < n ==> ((a * b MOD n) MOD n = (a * b) MOD n)``, 182 PROVE_TAC [MOD_MULT1, MULT_COMM]); 183 184val DIVISION_ALT = store_thm 185 ("DIVISION_ALT", 186 ``!n k. 0 < n ==> (k DIV n * n + k MOD n = k)``, 187 PROVE_TAC [DIVISION]); 188 189val MOD_EQ_X = store_thm 190 ("MOD_EQ_X", 191 ``!n r. 0 < n ==> ((r MOD n = r) = r < n)``, 192 !! STRIP_TAC 193 ++ REVERSE EQ_TAC >> PROVE_TAC [LESS_MOD] 194 ++ DISCH_THEN (fn th => ONCE_REWRITE_TAC [SYM th]) 195 ++ RW_TAC std_ss [MOD_LESS]); 196 197val DIV_EQ_0 = store_thm 198 ("DIV_EQ_0", 199 ``!n r. 0 < n ==> ((r DIV n = 0) = r < n)``, 200 !! STRIP_TAC 201 ++ REVERSE EQ_TAC >> PROVE_TAC [LESS_DIV_EQ_ZERO] 202 ++ STRIP_TAC 203 ++ Know `r DIV n * n + r MOD n = r` 204 >> RW_TAC std_ss [DIVISION_ALT] 205 ++ RW_TAC arith_ss [MOD_EQ_X]); 206 207val MOD_EXP = store_thm 208 ("MOD_EXP", 209 ``!n a b. 0 < n ==> ((a MOD n) EXP b MOD n = a EXP b MOD n)``, 210 NTAC 2 STRIP_TAC 211 ++ Induct >> RW_TAC std_ss [EXP] 212 ++ STRIP_TAC 213 ++ RES_TAC 214 ++ RW_TAC std_ss 215 [EXP, GSYM (Q.SPECL [`n`, `a MOD n`, `(a MOD n) EXP b`] MOD_MULT2)] 216 ++ RW_TAC std_ss [MOD_MULT1, MOD_MULT2]); 217 218val DIV_TWO_UNIQUE = store_thm 219 ("DIV_TWO_UNIQUE", 220 ``!n q r. (n = 2 * q + r) /\ ((r = 0) \/ (r = 1)) 221 ==> (q = n DIV 2) /\ (r = n MOD 2)``, 222 NTAC 3 STRIP_TAC 223 ++ MP_TAC (Q.SPECL [`2`, `n`, `q`] DIV_UNIQUE) 224 ++ MP_TAC (Q.SPECL [`2`, `n`, `r`] MOD_UNIQUE) 225 ++ Know `((r = 0) \/ (r = 1)) = r < 2` >> DECIDE_TAC 226 ++ DISCH_THEN (fn th => REWRITE_TAC [th]) 227 ++ RW_TAC std_ss [] 228 ++ PROVE_TAC [MULT_COMM]); 229 230val DIVISION_TWO = store_thm 231 ("DIVISION_TWO", 232 ``!n. (n = 2 * (n DIV 2) + (n MOD 2)) /\ ((n MOD 2 = 0) \/ (n MOD 2 = 1))``, 233 STRIP_TAC 234 ++ MP_TAC (Q.SPEC `2` DIVISION) 235 ++ Know `0:num < 2` >> DECIDE_TAC 236 ++ DISCH_THEN (fn th => REWRITE_TAC [th]) 237 ++ DISCH_THEN (MP_TAC o Q.SPEC `n`) 238 ++ RW_TAC bool_ss [] << 239 [PROVE_TAC [MULT_COMM], 240 DECIDE_TAC]); 241 242val DIV_TWO = store_thm 243 ("DIV_TWO", 244 ``!n. n = 2 * (n DIV 2) + (n MOD 2)``, 245 PROVE_TAC [DIVISION_TWO]); 246 247val MOD_TWO = store_thm 248 ("MOD_TWO", 249 ``!n. n MOD 2 = if EVEN n then 0 else 1``, 250 STRIP_TAC 251 ++ MP_TAC (Q.SPEC `n` DIVISION_TWO) 252 ++ STRIP_TAC << 253 [Q.PAT_ASSUM `n = X` MP_TAC 254 ++ RW_TAC std_ss [] 255 ++ PROVE_TAC [EVEN_DOUBLE, ODD_EVEN, ADD_CLAUSES], 256 Q.PAT_ASSUM `n = X` MP_TAC 257 ++ RW_TAC std_ss [] 258 ++ PROVE_TAC [ODD_DOUBLE, ODD_EVEN, ADD1]]); 259 260val DIV_TWO_BASIC = store_thm 261 ("DIV_TWO_BASIC", 262 ``(0 DIV 2 = 0) /\ (1 DIV 2 = 0) /\ (2 DIV 2 = 1)``, 263 Know `(0:num = 2 * 0 + 0) /\ (1:num = 2 * 0 + 1) /\ (2:num = 2 * 1 + 0)` 264 >> RW_TAC arith_ss [] 265 ++ PROVE_TAC [DIV_TWO_UNIQUE]); 266 267val DIV_TWO_MONO = store_thm 268 ("DIV_TWO_MONO", 269 ``!m n. m DIV 2 < n DIV 2 ==> m < n``, 270 NTAC 2 STRIP_TAC 271 ++ (CONV_TAC o RAND_CONV o ONCE_REWRITE_CONV) [DIV_TWO] 272 ++ Q.SPEC_TAC (`m DIV 2`, `p`) 273 ++ Q.SPEC_TAC (`n DIV 2`, `q`) 274 ++ REPEAT STRIP_TAC 275 ++ Know `(m MOD 2 = 0) \/ (m MOD 2 = 1)` >> PROVE_TAC [MOD_TWO] 276 ++ Know `(n MOD 2 = 0) \/ (n MOD 2 = 1)` >> PROVE_TAC [MOD_TWO] 277 ++ DECIDE_TAC); 278 279val DIV_TWO_MONO_EVEN = store_thm 280 ("DIV_TWO_MONO_EVEN", 281 ``!m n. EVEN n ==> (m DIV 2 < n DIV 2 = m < n)``, 282 RW_TAC std_ss [] 283 ++ EQ_TAC >> PROVE_TAC [DIV_TWO_MONO] 284 ++ (CONV_TAC o RATOR_CONV o ONCE_REWRITE_CONV) [DIV_TWO] 285 ++ Q.SPEC_TAC (`m DIV 2`, `p`) 286 ++ Q.SPEC_TAC (`n DIV 2`, `q`) 287 ++ REPEAT STRIP_TAC 288 ++ Know `n MOD 2 = 0` >> PROVE_TAC [MOD_TWO] 289 ++ Know `(m MOD 2 = 0) \/ (m MOD 2 = 1)` >> PROVE_TAC [MOD_TWO] 290 ++ DECIDE_TAC); 291 292val DIV_TWO_CANCEL = store_thm 293 ("DIV_TWO_CANCEL", 294 ``!n. (2 * n DIV 2 = n) /\ (SUC (2 * n) DIV 2 = n)``, 295 RW_TAC std_ss [] << 296 [MP_TAC (Q.SPEC `2 * n` DIV_TWO) 297 ++ RW_TAC arith_ss [MOD_TWO, EVEN_DOUBLE], 298 MP_TAC (Q.SPEC `SUC (2 * n)` DIV_TWO) 299 ++ RW_TAC arith_ss [MOD_TWO, ODD_DOUBLE]]); 300 301val EXP_DIV_TWO = store_thm 302 ("EXP_DIV_TWO", 303 ``!n. 2 EXP SUC n DIV 2 = 2 EXP n``, 304 RW_TAC std_ss [EXP, DIV_TWO_CANCEL]); 305 306val EVEN_EXP_TWO = store_thm 307 ("EVEN_EXP_TWO", 308 ``!n. EVEN (2 EXP n) = ~(n = 0)``, 309 Cases >> RW_TAC arith_ss [EXP, EVEN_ODD_BASIC] 310 ++ RW_TAC arith_ss [EXP, EVEN_DOUBLE]); 311 312val DIV_TWO_EXP = store_thm 313 ("DIV_TWO_EXP", 314 ``!n k. k DIV 2 < 2 EXP n = k < 2 EXP SUC n``, 315 RW_TAC std_ss [] 316 ++ (CONV_TAC o RATOR_CONV o ONCE_REWRITE_CONV) [GSYM EXP_DIV_TWO] 317 ++ MATCH_MP_TAC DIV_TWO_MONO_EVEN 318 ++ RW_TAC std_ss [EVEN_EXP_TWO]); 319 320val MIN_0L = store_thm 321 ("MIN_0L", 322 ``!n : num. min 0 n = 0``, 323 RW_TAC arith_ss [min_def]); 324 325val MIN_0R = store_thm 326 ("MIN_0R", 327 ``!n : num. min n 0 = 0``, 328 RW_TAC arith_ss [min_def]); 329 330val MIN_REFL = store_thm 331 ("MIN_REFL", 332 ``!a : num. min a a = a``, 333 RW_TAC arith_ss [min_def]); 334 335val MIN_SYM = store_thm 336 ("MIN_SYM", 337 ``!a b : num. min a b = min b a``, 338 RW_TAC arith_ss [min_def]); 339 340val LEQ_MINL = store_thm 341 ("LEQ_MINL", 342 ``!a b : num. a <= b ==> (min a b = a)``, 343 RW_TAC arith_ss [min_def]); 344 345val LEQ_MINR = store_thm 346 ("LEQ_MINR", 347 ``!a b : num. a <= b ==> (min b a = a)``, 348 RW_TAC arith_ss [min_def]); 349 350val LESS_MINL = store_thm 351 ("LESS_MINL", 352 ``!a b : num. a < b ==> (min a b = a)``, 353 RW_TAC arith_ss [min_def]); 354 355val LESS_MINR = store_thm 356 ("LESS_MINR", 357 ``!a b : num. a < b ==> (min b a = a)``, 358 RW_TAC arith_ss [min_def]); 359 360val IN_GTNUM = store_thm 361 ("IN_GTNUM", 362 ``!x n : num. x IN gtnum n = n < x``, 363 RW_TAC std_ss [gtnum_def, SPECIFICATION]); 364 365val GTNUM0_SUBTYPE_JUDGEMENT = store_thm 366 ("GTNUM0_SUBTYPE_JUDGEMENT", 367 ``!m n. 368 SUC m <= n \/ m < n \/ ~(0 = n) \/ ~(n = 0) \/ 369 (n = SUC m) \/ (SUC m = n) ==> n IN gtnum 0``, 370 RW_TAC std_ss [IN_GTNUM] 371 ++ DECIDE_TAC); 372 373val GTNUM1_SUBTYPE_JUDGEMENT = store_thm 374 ("GTNUM1_SUBTYPE_JUDGEMENT", 375 ``!m n. SUC (SUC m) <= n \/ SUC m < n \/ 1 < n \/ 376 (n = SUC (SUC m)) \/ (SUC (SUC m) = n) ==> n IN gtnum 1``, 377 RW_TAC std_ss [IN_GTNUM] 378 ++ DECIDE_TAC); 379 380val GTNUM1_SUBSET_GTNUM0 = store_thm 381 ("GTNUM1_SUBSET_GTNUM0", 382 ``gtnum 1 SUBSET gtnum 0``, 383 RW_TAC std_ss [SUBSET_DEF, IN_GTNUM] 384 ++ DECIDE_TAC); 385 386val SUC_SUBTYPE = store_thm 387 ("SUC_SUBTYPE", 388 ``SUC IN ((UNIV -> gtnum 0) INTER (gtnum 0 -> gtnum 1))``, 389 RW_TAC std_ss [IN_FUNSET, IN_INTER, IN_UNIV, IN_GTNUM] 390 ++ DECIDE_TAC); 391 392val ADD_SUBTYPE = store_thm 393 ("ADD_SUBTYPE", 394 ``!n. $+ IN ((UNIV -> gtnum n -> gtnum n) INTER (gtnum n -> UNIV -> gtnum n) 395 INTER (gtnum 0 -> gtnum 0 -> gtnum 1))``, 396 RW_TAC std_ss [IN_FUNSET, IN_INTER, IN_UNIV, IN_GTNUM] 397 ++ DECIDE_TAC); 398 399val MULT_SUBTYPE = store_thm 400 ("MULT_SUBTYPE", 401 ``$* IN ((gtnum 0 -> gtnum 0 -> gtnum 0) INTER 402 (gtnum 1 -> gtnum 0 -> gtnum 1) INTER 403 (gtnum 0 -> gtnum 1 -> gtnum 1))``, 404 RW_TAC std_ss [IN_FUNSET, IN_INTER, IN_UNIV, IN_GTNUM, LESS_MULT2] << 405 [Cases_on `x' = 1` >> RW_TAC arith_ss [] 406 ++ Know `1 < x'` >> DECIDE_TAC 407 ++ RW_TAC std_ss [LESS_1_MULT2], 408 Cases_on `x = 1` >> RW_TAC arith_ss [] 409 ++ Know `1 < x` >> DECIDE_TAC 410 ++ RW_TAC std_ss [LESS_1_MULT2]]); 411 412val MIN_SUBTYPE = store_thm 413 ("MIN_SUBTYPE", 414 ``!x. min IN (x -> x -> x)``, 415 RW_TAC arith_ss [IN_FUNSET, min_def] 416 ++ PROVE_TAC []); 417 418val EXP_SUBTYPE = store_thm 419 ("EXP_SUBTYPE", 420 ``$EXP IN ((gtnum 0 -> UNIV -> gtnum 0) INTER 421 (gtnum 1 -> gtnum 0 -> gtnum 1))``, 422 RW_TAC std_ss [IN_FUNSET, IN_INTER, IN_UNIV, IN_GTNUM] 423 ++ Cases_on `x` >> DECIDE_TAC 424 ++ Cases_on `n` >> DECIDE_TAC 425 ++ Cases_on `x'` >> DECIDE_TAC 426 ++ KILL_TAC 427 ++ Induct_on `n` >> RW_TAC arith_ss [EXP] 428 ++ ONCE_REWRITE_TAC [EXP] 429 ++ MATCH_MP_TAC LESS_1_MULT2 430 ++ RW_TAC arith_ss []); 431 432val FUNPOW_SUBTYPE = store_thm 433 ("FUNPOW_SUBTYPE", 434 ``!(x:'a->bool). FUNPOW IN ((x -> x) -> UNIV -> x -> x)``, 435 RW_TAC std_ss [IN_FUNSET, IN_UNIV] 436 ++ POP_ASSUM MP_TAC 437 ++ Q.SPEC_TAC (`x'''`, `y`) 438 ++ Induct_on `x''` >> RW_TAC std_ss [FUNPOW] 439 ++ RW_TAC std_ss [FUNPOW]); 440 441val NUMERAL_BIT1_SUBTYPE = store_thm 442 ("NUMERAL_BIT1_SUBTYPE", 443 ``BIT1 IN ((UNIV -> gtnum 0) INTER (gtnum 0 -> gtnum 1))``, 444 RW_TAC bool_ss [IN_FUNSET, IN_GTNUM, BIT1, IN_INTER, IN_UNIV, 445 NUMERAL_DEF, ALT_ZERO, BIT2] 446 ++ DECIDE_TAC); 447 448val NUMERAL_BIT2_SUBTYPE = store_thm 449 ("NUMERAL_BIT2_SUBTYPE", 450 ``BIT2 IN (UNIV -> gtnum 1)``, 451 RW_TAC bool_ss [IN_FUNSET, IN_GTNUM, BIT1, IN_INTER, IN_UNIV, 452 NUMERAL_DEF, ALT_ZERO, BIT2] 453 ++ DECIDE_TAC); 454 455val NUMERAL_SUBTYPE = store_thm 456 ("NUMERAL_SUBTYPE", 457 ``!x. NUMERAL IN (x -> x)``, 458 RW_TAC std_ss [IN_FUNSET, NUMERAL_DEF]); 459 460val GTNUM0_SUBTYPE_REWRITE = store_thm 461 ("GTNUM0_SUBTYPE_REWRITE", 462 ``!n. n IN gtnum 0 ==> 0 < n /\ ~(n = 0) /\ ~(0 = n)``, 463 RW_TAC arith_ss [IN_GTNUM]); 464 465val GTNUM1_SUBTYPE_REWRITE = store_thm 466 ("GTNUM1_SUBTYPE_REWRITE", 467 ``!n. n IN gtnum 1 ==> 1 < n /\ ~(n = 1) /\ ~(1 = n)``, 468 RW_TAC arith_ss [IN_GTNUM]); 469 470val SQUARED_GT_1 = store_thm 471 ("SQUARED_GT_1", 472 ``!n : num. (n * n = n) = ~(1 < n)``, 473 Cases >> RW_TAC arith_ss [] 474 ++ Cases_on `n'` >> RW_TAC arith_ss [] 475 ++ RW_TAC std_ss [MULT] 476 ++ DECIDE_TAC); 477 478val MOD_LESS_1 = store_thm 479 ("MOD_LESS_1", 480 ``!a n. 0 < n ==> (a MOD n <= a)``, 481 !! STRIP_TAC 482 ++ MP_TAC (Q.SPECL [`n`, `a`] DIVISION_ALT) 483 ++ DECIDE_TAC); 484 485val MULT_EXP = store_thm 486 ("MULT_EXP", 487 ``!a b n. (a * b) EXP n = a EXP n * b EXP n``, 488 Induct_on `n` >> RW_TAC arith_ss [EXP] 489 ++ RW_TAC arith_ss [EXP] 490 ++ KILL_TAC 491 ++ PROVE_TAC [MULT_COMM, MULT_ASSOC]); 492 493val EXP_MULT = store_thm 494 ("EXP_MULT", 495 ``!n a b. (n EXP a) EXP b = n EXP (a * b)``, 496 !! STRIP_TAC 497 ++ Induct_on `b` >> RW_TAC arith_ss [EXP] 498 ++ RW_TAC arith_ss [EXP, MULT_CLAUSES, EXP_ADD]); 499 500val LT_LE_1_MULT = store_thm 501 ("LT_LE_1_MULT", 502 ``!m n : num. 1 < m /\ 0 < n ==> 1 < m * n``, 503 !! STRIP_TAC 504 ++ Suff `~(m * n = 0) /\ ~(m * n = 1)` >> DECIDE_TAC 505 ++ RW_TAC arith_ss []); 506 507val EXP_MONO = store_thm 508 ("EXP_MONO", 509 ``!p a b. 1 < p ==> (p EXP a < p EXP b = a < b)``, 510 Induct_on `b` 511 >> (RW_TAC arith_ss [EXP] 512 ++ STRIP_TAC 513 ++ Suff `~(p EXP a = 0)` >> DECIDE_TAC 514 ++ RW_TAC arith_ss [EXP_EQ_0]) 515 ++ !! STRIP_TAC 516 ++ Cases_on `a` 517 >> (RW_TAC arith_ss [EXP] 518 ++ MATCH_MP_TAC LT_LE_1_MULT 519 ++ RW_TAC arith_ss [] 520 ++ Cases_on `p` 521 >> (Suff `~(1:num < 0)` >> PROVE_TAC [] ++ KILL_TAC ++ DECIDE_TAC) 522 ++ RW_TAC arith_ss [ZERO_LESS_EXP]) 523 ++ RW_TAC arith_ss [EXP] 524 ++ Cases_on `p` 525 >> (Suff `~(1:num < 0)` >> PROVE_TAC [] ++ KILL_TAC ++ DECIDE_TAC) 526 ++ RW_TAC arith_ss []); 527 528val MINUS_1_SQUARED_MOD = store_thm 529 ("MINUS_1_SQUARED_MOD", 530 ``!n. 1 < n ==> (((n - 1) * (n - 1)) MOD n = 1)``, 531 !! STRIP_TAC 532 ++ Know `0 < n` >> DECIDE_TAC 533 ++ STRIP_TAC 534 ++ RW_TAC std_ss [LEFT_SUB_DISTRIB] 535 ++ Suff `(n + ((n - 1) * n - (n - 1) * 1)) MOD n = 1` 536 >> (Suff `!a. (n + a) MOD n = a MOD n` 537 >> DISCH_THEN (fn th => REWRITE_TAC [th] ++ RW_TAC std_ss []) 538 ++ Suff `!a. (n MOD n + a) MOD n = a MOD n` 539 >> RW_TAC std_ss [MOD_PLUS1] 540 ++ RW_TAC arith_ss [X_MOD_X]) 541 ++ Know `!a. n - 1 <= a ==> (n + (a - (n - 1)) = a + (n - (n - 1)))` 542 >> DECIDE_TAC 543 ++ DISCH_THEN (MP_TAC o Q.SPEC `(n - 1) * n`) 544 ++ Know `n - 1 <= (n - 1) * n` 545 >> (Cases_on `n` >> DECIDE_TAC 546 ++ RW_TAC arith_ss [MULT_CLAUSES]) 547 ++ STRIP_TAC 548 ++ ASM_REWRITE_TAC [] 549 ++ STRIP_TAC 550 ++ ASM_REWRITE_TAC [MULT_RIGHT_1] 551 ++ Suff `(((n - 1) * (n MOD n)) MOD n + (n - (n - 1))) MOD n = 1` 552 >> (EVERY (map (MP_TAC o Q.SPEC `n`) [MOD_PLUS1, MOD_MULT2]) 553 ++ ASM_REWRITE_TAC [] 554 ++ DISCH_THEN (REWRITE_TAC o wrap) 555 ++ DISCH_THEN (REWRITE_TAC o wrap)) 556 ++ NTAC 2 (POP_ASSUM K_TAC) 557 ++ Know `n - (n - 1) = 1` >> DECIDE_TAC 558 ++ DISCH_THEN (fn th => RW_TAC arith_ss [th, X_MOD_X, LESS_MOD])); 559 560val NUM_DOUBLE = store_thm 561 ("NUM_DOUBLE", 562 ``!n : num. n + n = 2 * n``, 563 DECIDE_TAC); 564 565val MOD_POWER_EQ_1 = store_thm 566 ("MOD_POWER_EQ_1", 567 ``!n x a b. 568 1 < n /\ (x EXP a MOD n = 1) ==> (x EXP (a * b) MOD n = 1)``, 569 Strip 570 ++ Simplify [GSYM EXP_MULT] 571 ++ Suff `((x EXP a) MOD n) EXP b MOD n = 1` 572 >> RW_TAC arith_ss [MOD_EXP] 573 ++ ASM_REWRITE_TAC [] 574 ++ RW_TAC arith_ss [EXP_1, LESS_MOD]); 575 576val ODD_EXP = store_thm 577 ("ODD_EXP", 578 ``!n a. 0 < a ==> (ODD (n EXP a) = ODD n)``, 579 STRIP_TAC 580 ++ Induct >> RW_TAC arith_ss [] 581 ++ RW_TAC arith_ss [EXP, ODD_MULT] 582 ++ Cases_on `a` >> RW_TAC arith_ss [EVEN_ODD_BASIC, EXP] 583 ++ RW_TAC arith_ss []); 584 585val ODD_GT_1 = store_thm 586 ("ODD_GT_1", 587 ``!n. 1 < n /\ ODD n ==> 2 < n``, 588 Cases >> Simplify [] 589 ++ Cases_on `n'` >> Simplify [] 590 ++ Cases_on `n` >> Simplify [GSYM ONE, GSYM TWO, EVEN_ODD_BASIC] 591 ++ DISCH_THEN K_TAC 592 ++ DECIDE_TAC); 593 594val MINUS_1_MULT_MOD = store_thm 595 ("MINUS_1_MULT_MOD", 596 ``!a b. 0 < a /\ 0 < b ==> ((a * b - 1) MOD b = b - 1)``, 597 Strip 598 ++ Cases_on `a` >> DECIDE_TAC 599 ++ RW_TAC std_ss [MULT] 600 ++ Know `!c. c + b - 1 = c + (b - 1)` >> DECIDE_TAC 601 ++ RW_TAC std_ss [] 602 ++ POP_ASSUM K_TAC 603 ++ Suff `((n * b) MOD b + (b - 1)) MOD b = b - 1` 604 >> RW_TAC std_ss [MOD_PLUS1] 605 ++ RW_TAC std_ss [MOD_EQ_0] 606 ++ RW_TAC arith_ss [MOD_EQ_X]); 607 608val EXP2_MONO_LE = store_thm 609 ("EXP2_MONO_LE", 610 ``!a b n. 0 < n /\ a <= b ==> a EXP n <= b EXP n``, 611 Strip 612 ++ Induct_on `n` >> DECIDE_TAC 613 ++ RW_TAC arith_ss [EXP] 614 ++ Cases_on `n` >> RW_TAC arith_ss [EXP] 615 ++ POP_ASSUM MP_TAC 616 ++ Simplify [] 617 ++ Know `a * a EXP SUC n' <= a * b EXP SUC n'` 618 >> (Cases_on `a` >> RW_TAC arith_ss [] 619 ++ Simplify [GSYM MULT_LESS_EQ_SUC]) 620 ++ Suff `a * b EXP SUC n' <= b * b EXP SUC n'` >> DECIDE_TAC 621 ++ Cases_on `b EXP SUC n'` 622 ++ Simplify [ONCE_REWRITE_RULE [MULT_COMM] (GSYM MULT_LESS_EQ_SUC)]); 623 624val EXP1_MONO_LE = store_thm 625 ("EXP1_MONO_LE", 626 ``!n a b. 0 < n /\ a <= b ==> n EXP a <= n EXP b``, 627 Strip 628 ++ Cases_on `a = b` >> Simplify [] 629 ++ Cases_on `n = 1` >> Simplify [EXP_1] 630 ++ Suff `n EXP a < n EXP b` >> DECIDE_TAC 631 ++ Know `1 < n /\ a < b` >> DECIDE_TAC 632 ++ RW_TAC std_ss [EXP_MONO]); 633 634val LT_SUC = store_thm 635 ("LT_SUC", 636 ``!a b. a < SUC b = a < b \/ (a = b)``, 637 DECIDE_TAC); 638 639val LE_SUC = store_thm 640 ("LE_SUC", 641 ``!a b. a <= SUC b = a <= b \/ (a = SUC b)``, 642 DECIDE_TAC); 643 644val TRANSFORM_2D_NUM = store_thm 645 ("TRANSFORM_2D_NUM", 646 ``!P. 647 (!m n : num. P m n ==> P n m) /\ (!m n. P m (m + n)) ==> (!m n. P m n)``, 648 Strip 649 ++ Know `m <= n \/ n <= m` >> DECIDE_TAC 650 ++ RW_TAC std_ss [LESS_EQ_EXISTS] 651 ++ PROVE_TAC []); 652 653val TRIANGLE_2D_NUM = store_thm 654 ("TRIANGLE_2D_NUM", 655 ``!P. (!d n. P n (d + n)) ==> (!m n : num. m <= n ==> P m n)``, 656 RW_TAC std_ss [LESS_EQ_EXISTS] 657 ++ PROVE_TAC [ADD_COMM]); 658 659val MAX_LE_X = store_thm 660 ("MAX_LE_X", 661 ``!m n k. MAX m n <= k = m <= k /\ n <= k``, 662 RW_TAC arith_ss [MAX_DEF]); 663 664val X_LE_MAX = store_thm 665 ("X_LE_MAX", 666 ``!m n k. k <= MAX m n = k <= m \/ k <= n``, 667 RW_TAC arith_ss [MAX_DEF]); 668 669val SUC_DIV_TWO_ZERO = store_thm 670 ("SUC_DIV_TWO_ZERO", 671 ``!n. (SUC n DIV 2 = 0) = (n = 0)``, 672 RW_TAC std_ss [] 673 ++ REVERSE EQ_TAC 674 >> (MP_TAC DIV_TWO_BASIC 675 ++ Know `SUC 0 = 1` >> DECIDE_TAC 676 ++ RW_TAC arith_ss []) 677 ++ RW_TAC std_ss [] 678 ++ MP_TAC (Q.SPEC `SUC n` DIV_TWO) 679 ++ RW_TAC arith_ss [MULT_CLAUSES, MOD_TWO]); 680 681val LOG2_LOWER = store_thm 682 ("LOG2_LOWER", 683 ``!n. n < 2 EXP log2 n``, 684 recInduct log2_ind 685 ++ RW_TAC arith_ss [log2_def, EXP] 686 ++ POP_ASSUM MP_TAC 687 ++ RW_TAC std_ss [DIV_TWO_EXP, EXP]); 688 689val LOG2_LOWER_SUC = store_thm 690 ("LOG2_LOWER_SUC", 691 ``!n. SUC n <= 2 EXP log2 n``, 692 RW_TAC std_ss [] 693 ++ MP_TAC (Q.SPEC `n` LOG2_LOWER) 694 ++ DECIDE_TAC); 695 696val LOG2_UPPER = store_thm 697 ("LOG2_UPPER", 698 ``!n. ~(n = 0) ==> 2 EXP log2 n <= 2 * n``, 699 recInduct log2_ind 700 ++ RW_TAC arith_ss [log2_def, EXP] 701 ++ Cases_on `SUC v DIV 2 = 0` 702 >> (POP_ASSUM MP_TAC 703 ++ RW_TAC std_ss [SUC_DIV_TWO_ZERO] 704 ++ RW_TAC arith_ss [DECIDE ``SUC 0 = 1``, DIV_TWO_BASIC, 705 log2_def, EXP]) 706 ++ RES_TAC 707 ++ POP_ASSUM MP_TAC 708 ++ KILL_TAC 709 ++ Q.SPEC_TAC (`SUC v`, `n`) 710 ++ GEN_TAC 711 ++ Q.SPEC_TAC (`2 EXP log2 (n DIV 2)`, `m`) 712 ++ GEN_TAC 713 ++ Suff `2 * (n DIV 2) <= n` >> DECIDE_TAC 714 ++ MP_TAC (Q.SPEC `n` DIV_TWO) 715 ++ DECIDE_TAC); 716 717val LOG2_UPPER_SUC = store_thm 718 ("LOG2_UPPER_SUC", 719 ``!n. 2 EXP log2 n <= SUC (2 * n)``, 720 STRIP_TAC 721 ++ MP_TAC (Q.SPEC `n` LOG2_UPPER) 722 ++ REVERSE (Cases_on `n = 0`) >> RW_TAC arith_ss [] 723 ++ RW_TAC arith_ss [log2_def, EXP]); 724 725(* non-interactive mode 726*) 727val _ = export_theory (); 728