1open HolKernel Parse boolLib simpLib BasicProvers 2 prim_recTheory arithmeticTheory boolSimps 3 metisLib numLib; 4 5val CALC = EQT_ELIM o reduceLib.REDUCE_CONV; 6val ARITH_TAC = CONV_TAC Arith.ARITH_CONV; 7val DECIDE = EQT_ELIM o Arith.ARITH_CONV; 8 9val arith_ss = numLib.arith_ss; 10 11val ARW = RW_TAC arith_ss; 12 13local open numeralTheory in end; 14 (* concession to Holmake's flawed dependency analysis, which doesn't 15 spot this problem *) 16 17val _ = new_theory "divides"; 18 19val divides_def = Q.new_definition 20 ("divides_def", 21 `divides a b = ?q. b = q*a`); 22 23val ALL_DIVIDES_0 = store_thm 24("ALL_DIVIDES_0", 25 ``!a. divides a 0``, 26 METIS_TAC[divides_def,MULT_CLAUSES]) 27 before 28 export_rewrites ["ALL_DIVIDES_0"]; 29 30val ZERO_DIVIDES = store_thm( 31 "ZERO_DIVIDES", 32 ``divides 0 m = (m = 0)``, 33 SRW_TAC [][divides_def]) 34 before 35 export_rewrites ["ZERO_DIVIDES"]; 36 37val DIVIDES_REFL = store_thm 38("DIVIDES_REFL", 39 ``!a. divides a a``, 40 METIS_TAC[divides_def,MULT_CLAUSES]) 41 before 42 export_rewrites ["DIVIDES_REFL"]; 43 44val DIVIDES_TRANS = store_thm 45 ("DIVIDES_TRANS", 46 ``!a b c. divides a b /\ divides b c ==> divides a c``, 47 METIS_TAC [divides_def,MULT_ASSOC]); 48 49val ONE_DIVIDES_ALL = store_thm 50("ONE_DIVIDES_ALL", 51 ``!a. divides 1 a``, 52 METIS_TAC[divides_def,MULT_CLAUSES]) 53 before 54 export_rewrites ["ONE_DIVIDES_ALL"]; 55 56val DIVIDES_ONE = store_thm 57 ("DIVIDES_ONE", 58 ``!x. divides x 1 = (x = 1)``, 59 METIS_TAC [divides_def,MULT_CLAUSES,MULT_EQ_1]) 60 before 61 export_rewrites ["DIVIDES_ONE"]; 62 63val DIVIDES_ADD_1 = store_thm 64("DIVIDES_ADD_1", 65 ``!a b c. divides a b /\ divides a c ==> divides a (b+c)``, 66 METIS_TAC[divides_def,RIGHT_ADD_DISTRIB]); 67 68val DIVIDES_ADD_2 = store_thm 69("DIVIDES_ADD_2", 70 ``!a b c. divides a b /\ divides a (b+c) ==> divides a c``, 71 ARW[divides_def] THEN EXISTS_TAC ``q' - q`` THEN ARW[RIGHT_SUB_DISTRIB]); 72 73val DIVIDES_SUB = store_thm 74("DIVIDES_SUB", 75 ``!a b c. divides a b /\ divides a c ==> divides a (b-c)``, 76 METIS_TAC[divides_def,RIGHT_SUB_DISTRIB]); 77 78val DIVIDES_LE = store_thm 79("DIVIDES_LE", 80 ``!a b. 0<b /\ divides a b ==> a <= b``, 81 Cases_on `a` THEN ARW[divides_def] THEN Cases_on `q` THENL 82 [METIS_TAC [MULT_CLAUSES,LESS_REFL], 83 ARW[MULT_CLAUSES]]); 84 85val DIVIDES_LEQ_OR_ZERO = store_thm 86 ("DIVIDES_LEQ_OR_ZERO", 87 ``!m n. divides m n ==> m <= n \/ (n = 0)``, 88 ARW [divides_def] 89 THEN Cases_on `q` 90 THEN ARW [MULT_CLAUSES]); 91 92val NOT_LT_DIVIDES = store_thm 93("NOT_LT_DIVIDES", 94 ``!a b. 0<b /\ b<a ==> ~(divides a b)``, 95 METIS_TAC[DIVIDES_LE,LESS_EQ_ANTISYM]); 96 97val DIVIDES_ANTISYM = store_thm 98("DIVIDES_ANTISYM", 99 ``!a b. divides a b /\ divides b a ==> (a = b)``, 100 REPEAT Cases 101 THEN TRY (ARW[divides_def] THEN NO_TAC) 102 THEN METIS_TAC [LESS_EQUAL_ANTISYM,DIVIDES_LE,prim_recTheory.LESS_0]); 103 104val DIVIDES_MULT = store_thm 105("DIVIDES_MULT", 106 ``!a b c. divides a b ==> divides a (b*c)``, 107 METIS_TAC[divides_def,MULT_SYM,MULT_ASSOC]); 108 109val DIVIDES_MULT_LEFT = store_thm( 110 "DIVIDES_MULT_LEFT", 111 ``!n m. divides (n * m) m = (m = 0) \/ (n = 1)``, 112 SIMP_TAC arith_ss [FORALL_AND_THM, EQ_IMP_THM, DISJ_IMP_THM, 113 ALL_DIVIDES_0, DIVIDES_REFL] THEN 114 SIMP_TAC bool_ss [divides_def] THEN REPEAT STRIP_TAC THEN 115 `m * 1 = m * (n * q)` by 116 (POP_ASSUM (CONV_TAC o LAND_CONV o 117 ONCE_REWRITE_CONV o C cons []) THEN 118 ASM_SIMP_TAC bool_ss [MULT_CLAUSES] THEN 119 CONV_TAC (AC_CONV(MULT_ASSOC, MULT_COMM))) THEN 120 `(m = 0) \/ (n * q = 1)` by METIS_TAC [EQ_MULT_LCANCEL] THEN 121 ASM_SIMP_TAC bool_ss [] THEN 122 METIS_TAC [MULT_EQ_1]); 123 124val DIVIDES_EXP = Q.prove 125(`!a b x. 0 < x /\ divides a b ==> divides a (b ** x)`, 126 Cases_on `x` THEN RW_TAC arith_ss [EXP] THEN METIS_TAC [DIVIDES_MULT]); 127 128val DIVIDES_FACT = store_thm 129("DIVIDES_FACT", 130 ``!b. 0<b ==> divides b (FACT b)``, 131 Cases_on `b` THEN ARW[FACT, divides_def] THEN METIS_TAC [MULT_COMM]); 132 133val LEQ_DIVIDES_FACT = store_thm 134 ("LEQ_DIVIDES_FACT", 135 ``!m n. 0 < m /\ m <= n ==> divides m (FACT n)``, 136 RW_TAC arith_ss [LESS_EQ_EXISTS] 137 THEN Induct_on `p` 138 THEN METIS_TAC [FACT, LESS_REFL, num_CASES, DIVIDES_MULT, 139 MULT_COMM, DIVIDES_REFL, ADD_CLAUSES]); 140 141(*---------------------------------------------------------------------------*) 142(* Definition and trivial facts about primality. *) 143(*---------------------------------------------------------------------------*) 144 145val prime_def = Q.new_definition 146("prime_def", 147 `prime a = ~(a=1) /\ !b. divides b a ==> (b=a) \/ (b=1)`); 148 149 150val NOT_PRIME_0 = Q.store_thm 151 ("NOT_PRIME_0", 152 `~prime 0`, 153 ARW [prime_def, ALL_DIVIDES_0]) 154 before 155 export_rewrites ["NOT_PRIME_0"]; 156 157val NOT_PRIME_1 = Q.store_thm 158 ("NOT_PRIME_1", 159 `~prime 1`, 160 ARW [prime_def, DIVIDES_LE]) 161 before 162 export_rewrites ["NOT_PRIME_1"]; 163 164val PRIME_2 = store_thm 165 ("PRIME_2", 166 ``prime 2``, 167 RW_TAC arith_ss [prime_def] THEN 168 `0 < b /\ b <= 2` by METIS_TAC [DIVIDES_LE, ZERO_DIVIDES, 169 CALC ``0<2``,NOT_ZERO_LT_ZERO] THEN 170 NTAC 2 (POP_ASSUM MP_TAC) THEN ARITH_TAC) 171 before 172 export_rewrites ["PRIME_2"]; 173 174val PRIME_3 = Q.store_thm 175("PRIME_3", 176 `prime 3`, 177 RW_TAC arith_ss [prime_def] THEN 178 `b <= 3` by RW_TAC arith_ss [DIVIDES_LE] THEN 179 `(b=0) \/ (b=1) \/ (b=2) \/ (b=3)` by (POP_ASSUM MP_TAC THEN ARITH_TAC) THEN 180 RW_TAC arith_ss [] THENL 181 [FULL_SIMP_TAC arith_ss [ZERO_DIVIDES], 182 FULL_SIMP_TAC arith_ss [divides_def]]) 183 before 184 export_rewrites ["PRIME_3"]; 185 186val PRIME_POS = store_thm 187 ("PRIME_POS", 188 ``!p. prime p ==> 0<p``, 189 Cases THEN RW_TAC arith_ss [NOT_PRIME_0]); 190 191val ONE_LT_PRIME = Q.store_thm 192("ONE_LT_PRIME", 193 `!p. prime p ==> 1 < p`, 194 METIS_TAC [NOT_PRIME_0, NOT_PRIME_1, 195 DECIDE ``(p=0) \/ (p=1) \/ 1 < p``]); 196 197val prime_divides_only_self = Q.store_thm 198("prime_divides_only_self", 199 `!m n. prime m /\ prime n /\ divides m n ==> (m=n)`, 200 RW_TAC arith_ss [divides_def] THEN 201 `m<>1` by METIS_TAC [NOT_PRIME_0,NOT_PRIME_1] THEN 202 Q.PAT_X_ASSUM `prime (m*q)` MP_TAC THEN RW_TAC arith_ss [prime_def] THEN 203 METIS_TAC [divides_def,MULT_SYM]); 204 205 206(*---------------------------------------------------------------------------*) 207(* Every number has a prime factor, except for 1. The proof proceeds by a *) 208(* complete induction on n, and then considers cases on whether n is prime *) 209(* or not. The first case (n is prime) is trivial. In the second case, there *) 210(* must be an x that divides n, and x is not 1 or n. By DIVIDES_LEQ_OR_ZERO, *) 211(* n=0 or x <= n. If n=0, then 2 is a prime that divides 0. On the other *) 212(* hand, if x <= n, there are two cases: if x<n then we can use the i.h. and *) 213(* by transitivity of divides we are done; otherwise, if x=n, then we have *) 214(* a contradiction with the fact that x is not 1 or n. *) 215(* *) 216(* In the following proof, METIS_TAC automatically considers cases on *) 217(* whether n is prime or not. *) 218(*---------------------------------------------------------------------------*) 219 220val PRIME_FACTOR = store_thm 221 ("PRIME_FACTOR", 222 ``!n. ~(n = 1) ==> ?p. prime p /\ divides p n``, 223 completeInduct_on `n` THEN 224 METIS_TAC [DIVIDES_REFL, prime_def, LESS_OR_EQ, PRIME_2, 225 DIVIDES_LEQ_OR_ZERO, DIVIDES_TRANS, ALL_DIVIDES_0]); 226 227(*---------------------------------------------------------------------------*) 228(* For every number there is a larger prime. *) 229(*---------------------------------------------------------------------------*) 230 231val EUCLID = store_thm 232("EUCLID", 233 ``!n. ?p. n < p /\ prime p``, 234CCONTR_TAC 235THEN 236 `?n. !p. n < p ==> ~prime p` by METIS_TAC[] THEN 237 `~(FACT n + 1 = 1)` by RW_TAC arith_ss 238 [FACT_LESS,NOT_ZERO_LT_ZERO] THEN 239 `?p. prime p /\ 240 divides p (FACT n + 1)` by METIS_TAC [PRIME_FACTOR] THEN 241 `0 < p` by METIS_TAC [PRIME_POS] THEN 242 `p <= n` by METIS_TAC [NOT_LESS] THEN 243 `divides p (FACT n)` by METIS_TAC [LEQ_DIVIDES_FACT] THEN 244 `divides p 1` by METIS_TAC [DIVIDES_ADD_2] THEN 245 `p = 1` by METIS_TAC [DIVIDES_ONE] THEN 246 `~prime p` by METIS_TAC [NOT_PRIME_1] 247); 248 249(*---------------------------------------------------------------------------*) 250(* The sequence of primes. *) 251(*---------------------------------------------------------------------------*) 252 253val PRIMES_def = new_recursive_definition 254 {name = "PRIMES_def", 255 rec_axiom = prim_recTheory.num_Axiom, 256 def = ``(PRIMES 0 = 2) /\ 257 (PRIMES (SUC n) = LEAST p. prime p /\ PRIMES n < p)``}; 258 259val primePRIMES = Q.store_thm 260("primePRIMES", 261 `!n. prime (PRIMES n)`, 262 Cases THEN RW_TAC arith_ss [PRIMES_def,PRIME_2] THEN 263 LEAST_ELIM_TAC THEN 264 RW_TAC bool_ss [] THEN 265 METIS_TAC [EUCLID]); 266 267val INFINITE_PRIMES = Q.store_thm 268("INFINITE_PRIMES", 269 `!n. PRIMES n < PRIMES (SUC n)`, 270 RW_TAC arith_ss [PRIMES_def] THEN 271 LEAST_ELIM_TAC THEN 272 RW_TAC bool_ss [] THEN 273 METIS_TAC [EUCLID]); 274 275val LT_PRIMES = Q.store_thm 276("LT_PRIMES", 277 `!m n. m < n ==> PRIMES m < PRIMES n`, 278 Induct_on `n` THEN RW_TAC arith_ss [] THEN 279 METIS_TAC [INFINITE_PRIMES,LESS_TRANS,LESS_THM]); 280 281val PRIMES_11 = Q.store_thm 282("PRIMES_11", 283 `!m n. (PRIMES m = PRIMES n) ==> (m=n)`, 284 METIS_TAC [DECIDE ``a < b ==> a<>b``,LT_PRIMES, 285 DECIDE `` !m n. m < n \/ (m=n) \/ n < m``]); 286 287val INDEX_LESS_PRIMES = Q.store_thm 288("INDEX_LESS_PRIMES", 289 `!n. n < PRIMES n`, 290 Induct THEN RW_TAC arith_ss [PRIMES_def] THEN 291 LEAST_ELIM_TAC THEN CONJ_TAC THENL 292 [METIS_TAC [INFINITE_PRIMES,primePRIMES], RW_TAC arith_ss []]); 293 294val EUCLID_PRIMES = Q.store_thm 295("EUCLID_PRIMES", 296 `!n. ?i. n < PRIMES i`, 297 SPOSE_NOT_THEN (MP_TAC o REWRITE_RULE [NOT_LESS]) THEN STRIP_TAC THEN 298 METIS_TAC [INDEX_LESS_PRIMES,DECIDE ``a <= b /\ b < a ==> F``]); 299 300val NEXT_LARGER_PRIME = Q.store_thm 301("NEXT_LARGER_PRIME", 302 `!n. ?i. n < PRIMES i /\ !j. j < i ==> PRIMES j <= n`, 303 GEN_TAC THEN METIS_TAC [HO_MATCH_MP WOP (SPEC_ALL EUCLID_PRIMES),NOT_LESS]); 304 305val PRIMES_NO_GAP = Q.store_thm 306("PRIMES_NO_GAP", 307 `!n p. PRIMES n < p /\ p < PRIMES (SUC n) /\ prime p ==> F`, 308 RW_TAC bool_ss [PRIMES_def,GSYM IMP_DISJ_THM] THEN POP_ASSUM MP_TAC THEN 309 LEAST_ELIM_TAC THEN METIS_TAC[INFINITE_PRIMES,primePRIMES]); 310 311val PRIMES_ONTO = Q.store_thm 312("PRIMES_ONTO", 313 `!p. prime p ==> ?i. PRIMES i = p`, 314 SPOSE_NOT_THEN STRIP_ASSUME_TAC THEN 315 STRIP_ASSUME_TAC (Q.SPEC `p` NEXT_LARGER_PRIME) THEN 316 Cases_on `i` THENL 317 [METIS_TAC [DECIDE``p < 2 = (p=0) \/ (p=1)``, 318 NOT_PRIME_0,NOT_PRIME_1,PRIME_2,PRIMES_def], 319 `PRIMES n < p` by METIS_TAC [DECIDE ``n < SUC n``,LESS_OR_EQ] THEN 320 METIS_TAC [PRIMES_NO_GAP]]); 321 322val PRIME_INDEX = Q.store_thm 323("PRIME_INDEX", 324 `!p. prime p = ?i. p = PRIMES i`, 325 METIS_TAC [PRIMES_ONTO,primePRIMES]); 326 327val ONE_LT_PRIMES = Q.store_thm 328("ONE_LT_PRIMES", 329 `!n. 1 < PRIMES n`, 330 METIS_TAC [primePRIMES, NOT_PRIME_0, NOT_PRIME_1, 331 DECIDE ``(x=0) \/ (x=1) \/ 1<x``]); 332 333val ZERO_LT_PRIMES = Q.store_thm 334("ZERO_LT_PRIMES", 335 `!n. 0 < PRIMES n`, 336 METIS_TAC [LESS_TRANS, ONE_LT_PRIMES, DECIDE ``0 < 1``]); 337 338(*---------------------------------------------------------------------------*) 339(* Directly computable version of divides *) 340(*---------------------------------------------------------------------------*) 341 342val compute_divides = Q.store_thm 343("compute_divides", 344 `!a b. divides a b = 345 if a=0 then (b=0) else 346 if a=1 then T else 347 if b=0 then T else 348 (b MOD a = 0)`, 349 RW_TAC arith_ss [divides_def] 350 THEN EQ_TAC 351 THEN RW_TAC arith_ss [] THENL 352 [Cases_on `q` THENL 353 [RW_TAC arith_ss [], 354 `0<a` by RW_TAC arith_ss [] THEN 355 METIS_TAC [MOD_MULT, MULT_SYM, ADD_CLAUSES]], 356 Q.EXISTS_TAC `b` THEN RW_TAC arith_ss [], 357 Q.EXISTS_TAC `0` THEN RW_TAC arith_ss [], 358 `0<a` by RW_TAC arith_ss [] THEN 359 let val MOD_P_inst = BETA_RULE (Q.SPECL[`\x. (x = 0)`,`b`,`a`] MOD_P) 360 in METIS_TAC [MOD_P_inst,MULT_SYM, ADD_CLAUSES] 361 end]); 362 363val _ = 364 computeLib.add_persistent_funs 365 ["compute_divides"]; 366 367val _ = export_theory(); 368