(* ========================================================================= *) (* Basic divisibility notions over the integers. *) (* *) (* This is similar to stuff in Library/prime.ml etc. for natural numbers. *) (* ========================================================================= *) prioritize_int();; (* ------------------------------------------------------------------------- *) (* Basic properties of divisibility. *) (* ------------------------------------------------------------------------- *) let INT_DIVIDES_REFL = INTEGER_RULE `!d. d divides d`;; let INT_DIVIDES_TRANS = INTEGER_RULE `!x y z. x divides y /\ y divides z ==> x divides z`;; let INT_DIVIDES_ADD = INTEGER_RULE `!d a b. d divides a /\ d divides b ==> d divides (a + b)`;; let INT_DIVIDES_SUB = INTEGER_RULE `!d a b. d divides a /\ d divides b ==> d divides (a - b)`;; let INT_DIVIDES_0 = INTEGER_RULE `!d. d divides &0`;; let INT_DIVIDES_ZERO = INTEGER_RULE `!x. &0 divides x <=> x = &0`;; let INT_DIVIDES_LNEG = INTEGER_RULE `!d x. (--d) divides x <=> d divides x`;; let INT_DIVIDES_RNEG = INTEGER_RULE `!d x. d divides (--x) <=> d divides x`;; let INT_DIVIDES_RMUL = INTEGER_RULE `!d x y. d divides x ==> d divides (x * y)`;; let INT_DIVIDES_LMUL = INTEGER_RULE `!d x y. d divides y ==> d divides (x * y)`;; let INT_DIVIDES_1 = INTEGER_RULE `!x. &1 divides x`;; let INT_DIVIDES_ADD_REVR = INTEGER_RULE `!d a b. d divides a /\ d divides (a + b) ==> d divides b`;; let INT_DIVIDES_ADD_REVL = INTEGER_RULE `!d a b. d divides b /\ d divides (a + b) ==> d divides a`;; let INT_DIVIDES_MUL_L = INTEGER_RULE `!a b c. a divides b ==> (c * a) divides (c * b)`;; let INT_DIVIDES_MUL_R = INTEGER_RULE `!a b c. a divides b ==> (a * c) divides (b * c)`;; let INT_DIVIDES_LMUL2 = INTEGER_RULE `!d a x. (x * d) divides a ==> d divides a`;; let INT_DIVIDES_RMUL2 = INTEGER_RULE `!d a x. (d * x) divides a ==> d divides a`;; let INT_DIVIDES_CMUL2 = INTEGER_RULE `!a b c. (c * a) divides (c * b) /\ ~(c = &0) ==> a divides b`;; let INT_DIVIDES_LMUL2_EQ = INTEGER_RULE `!a b c. ~(c = &0) ==> ((c * a) divides (c * b) <=> a divides b)`;; let INT_DIVIDES_RMUL2_EQ = INTEGER_RULE `!a b c. ~(c = &0) ==> ((a * c) divides (b * c) <=> a divides b)`;; let INT_DIVIDES_MUL2 = INTEGER_RULE `!a b c d. a divides b /\ c divides d ==> (a * c) divides (b * d)`;; let INT_DIVIDES_LABS = prove (`!d n. abs(d) divides n <=> d divides n`, REPEAT GEN_TAC THEN SIMP_TAC[INT_ABS] THEN COND_CASES_TAC THEN INTEGER_TAC);; let INT_DIVIDES_RABS = prove (`!d n. d divides (abs n) <=> d divides n`, REPEAT GEN_TAC THEN SIMP_TAC[INT_ABS] THEN COND_CASES_TAC THEN INTEGER_TAC);; let INT_DIVIDES_ABS = prove (`(!d n. abs(d) divides n <=> d divides n) /\ (!d n. d divides (abs n) <=> d divides n)`, REWRITE_TAC[INT_DIVIDES_LABS; INT_DIVIDES_RABS]);; let INT_DIVIDES_POW = prove (`!x y n. x divides y ==> (x pow n) divides (y pow n)`, REWRITE_TAC[int_divides] THEN MESON_TAC[INT_POW_MUL]);; let INT_DIVIDES_POW2 = prove (`!n x y. ~(n = 0) /\ (x pow n) divides y ==> x divides y`, INDUCT_TAC THEN REWRITE_TAC[NOT_SUC; INT_POW] THEN INTEGER_TAC);; let INT_DIVIDES_RPOW = prove (`!x y n. x divides y /\ ~(n = 0) ==> x divides (y pow n)`, GEN_TAC THEN GEN_TAC THEN INDUCT_TAC THEN SIMP_TAC[INT_DIVIDES_RMUL; INT_POW]);; let INT_DIVIDES_RPOW_SUC = prove (`!x y n. x divides y ==> x divides (y pow (SUC n))`, SIMP_TAC[INT_DIVIDES_RPOW; NOT_SUC]);; let INT_DIVIDES_ANTISYM_DIVISORS = prove (`!a b:int. a divides b /\ b divides a <=> !d. d divides a <=> d divides b`, MESON_TAC[INT_DIVIDES_REFL; INT_DIVIDES_TRANS]);; (* ------------------------------------------------------------------------- *) (* Now carefully distinguish signs. *) (* ------------------------------------------------------------------------- *) let INT_DIVIDES_ONE_POS = prove (`!x. &0 <= x ==> (x divides &1 <=> x = &1)`, REPEAT STRIP_TAC THEN EQ_TAC THENL [REWRITE_TAC[int_divides]; INTEGER_TAC] THEN DISCH_THEN(CHOOSE_THEN(MP_TAC o AP_TERM `abs` o SYM)) THEN SIMP_TAC[INT_ABS_NUM; INT_ABS_MUL_1] THEN ASM_SIMP_TAC[INT_ABS]);; let INT_DIVIDES_ONE_ABS = prove (`!d. d divides &1 <=> abs(d) = &1`, MESON_TAC[INT_DIVIDES_LABS; INT_DIVIDES_ONE_POS; INT_ABS_POS]);; let INT_DIVIDES_ONE = prove (`!d. d divides &1 <=> d = &1 \/ d = -- &1`, REWRITE_TAC[INT_DIVIDES_ONE_ABS] THEN INT_ARITH_TAC);; let INT_DIVIDES_ANTISYM_ASSOCIATED = prove (`!x y. x divides y /\ y divides x <=> ?u. u divides &1 /\ x = y * u`, REPEAT GEN_TAC THEN EQ_TAC THENL [ALL_TAC; INTEGER_TAC] THEN ASM_CASES_TAC `x = &0` THEN ASM_SIMP_TAC[INT_DIVIDES_ZERO; INT_MUL_LZERO] THEN ASM_MESON_TAC[int_divides; INT_DIVIDES_REFL; INTEGER_RULE `y = x * d /\ x = y * e /\ ~(y = &0) ==> d divides &1`]);; let INT_DIVIDES_ANTISYM = prove (`!x y. x divides y /\ y divides x <=> x = y \/ x = --y`, REWRITE_TAC[INT_DIVIDES_ANTISYM_ASSOCIATED; INT_DIVIDES_ONE] THEN REWRITE_TAC[RIGHT_OR_DISTRIB; EXISTS_OR_THM; UNWIND_THM2] THEN INT_ARITH_TAC);; let INT_DIVIDES_ANTISYM_ABS = prove (`!x y. x divides y /\ y divides x <=> abs(x) = abs(y)`, REWRITE_TAC[INT_DIVIDES_ANTISYM] THEN INT_ARITH_TAC);; let INT_DIVIDES_ANTISYM_POS = prove (`!x y. &0 <= x /\ &0 <= y ==> (x divides y /\ y divides x <=> x = y)`, REWRITE_TAC[INT_DIVIDES_ANTISYM_ABS] THEN INT_ARITH_TAC);; (* ------------------------------------------------------------------------- *) (* Lemmas about GCDs. *) (* ------------------------------------------------------------------------- *) let INT_GCD_POS = prove (`!a b. &0 <= gcd(a,b)`, REWRITE_TAC[int_gcd]);; let INT_GCD_DIVIDES = prove (`!a b. gcd(a,b) divides a /\ gcd(a,b) divides b`, INTEGER_TAC);; let INT_GCD_BEZOUT = prove (`!a b. ?x y. gcd(a,b) = a * x + b * y`, INTEGER_TAC);; let INT_DIVIDES_GCD = prove (`!a b d. d divides gcd(a,b) <=> d divides a /\ d divides b`, INTEGER_TAC);; let INT_DIVIDES_GCD = prove (`!a b d. d divides gcd(a,b) <=> d divides a /\ d divides b`, INTEGER_TAC);; let INT_GCD = INTEGER_RULE `!a b. (gcd(a,b) divides a /\ gcd(a,b) divides b) /\ (!e. e divides a /\ e divides b ==> e divides gcd(a,b))`;; let INT_GCD_UNIQUE = prove (`!a b d. gcd(a,b) = d <=> &0 <= d /\ d divides a /\ d divides b /\ !e. e divides a /\ e divides b ==> e divides d`, REPEAT GEN_TAC THEN EQ_TAC THENL [MESON_TAC[INT_GCD; INT_GCD_POS]; ALL_TAC] THEN ASM_SIMP_TAC[INT_GCD_POS; GSYM INT_DIVIDES_ANTISYM_POS; INT_DIVIDES_GCD] THEN REPEAT STRIP_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN INTEGER_TAC);; let INT_GCD_UNIQUE_ABS = prove (`!a b d. gcd(a,b) = abs(d) <=> d divides a /\ d divides b /\ !e. e divides a /\ e divides b ==> e divides d`, REWRITE_TAC[INT_GCD_UNIQUE; INT_ABS_POS; INT_DIVIDES_ABS]);; let INT_GCD_REFL = prove (`!a. gcd(a,a) = abs(a)`, REWRITE_TAC[INT_GCD_UNIQUE_ABS] THEN INTEGER_TAC);; let INT_GCD_SYM = prove (`!a b. gcd(a,b) = gcd(b,a)`, SIMP_TAC[INT_GCD_POS; GSYM INT_DIVIDES_ANTISYM_POS] THEN INTEGER_TAC);; let INT_GCD_ASSOC = prove (`!a b c. gcd(a,gcd(b,c)) = gcd(gcd(a,b),c)`, SIMP_TAC[INT_GCD_POS; GSYM INT_DIVIDES_ANTISYM_POS] THEN INTEGER_TAC);; let INT_GCD_1 = prove (`!a. gcd(a,&1) = &1 /\ gcd(&1,a) = &1`, SIMP_TAC[INT_GCD_UNIQUE; INT_POS; INT_DIVIDES_1]);; let INT_GCD_0 = prove (`!a. gcd(a,&0) = abs(a) /\ gcd(&0,a) = abs(a)`, SIMP_TAC[INT_GCD_UNIQUE_ABS] THEN INTEGER_TAC);; let INT_GCD_ABS = prove (`!a b. gcd(abs(a),b) = gcd(a,b) /\ gcd(a,abs(b)) = gcd(a,b)`, REWRITE_TAC[INT_GCD_UNIQUE; INT_DIVIDES_ABS; INT_GCD_POS; INT_GCD]);; let INT_GCD_MULTIPLE = (`!a b. gcd(a,a * b) = abs(a) /\ gcd(b,a * b) = abs(b)`, REWRITE_TAC[INT_GCD_UNIQUE_ABS] THEN INTEGER_TAC);; let INT_GCD_ADD = prove (`(!a b. gcd(a + b,b) = gcd(a,b)) /\ (!a b. gcd(b + a,b) = gcd(a,b)) /\ (!a b. gcd(a,a + b) = gcd(a,b)) /\ (!a b. gcd(a,b + a) = gcd(a,b))`, SIMP_TAC[INT_GCD_UNIQUE; INT_GCD_POS] THEN INTEGER_TAC);; let INT_GCD_SUB = prove (`(!a b. gcd(a - b,b) = gcd(a,b)) /\ (!a b. gcd(b - a,b) = gcd(a,b)) /\ (!a b. gcd(a,a - b) = gcd(a,b)) /\ (!a b. gcd(a,b - a) = gcd(a,b))`, SIMP_TAC[INT_GCD_UNIQUE; INT_GCD_POS] THEN INTEGER_TAC);; let INT_DIVIDES_GCD_LEFT = prove (`!m n:int. m divides n <=> gcd(m,n) = abs m`, SIMP_TAC[INT_GCD_UNIQUE; INT_ABS_POS; INT_DIVIDES_ABS; INT_DIVIDES_REFL] THEN MESON_TAC[INT_DIVIDES_REFL; INT_DIVIDES_TRANS]);; let INT_DIVIDES_GCD_RIGHT = prove (`!m n:int. n divides m <=> gcd(m,n) = abs n`, SIMP_TAC[INT_GCD_UNIQUE; INT_ABS_POS; INT_DIVIDES_ABS; INT_DIVIDES_REFL] THEN MESON_TAC[INT_DIVIDES_REFL; INT_DIVIDES_TRANS]);; (* ------------------------------------------------------------------------- *) (* More lemmas about coprimality. *) (* ------------------------------------------------------------------------- *) let INT_COPRIME_GCD = prove (`!a b. coprime(a,b) <=> gcd(a,b) = &1`, SIMP_TAC[GSYM INT_DIVIDES_ONE_POS; INT_GCD_POS] THEN INTEGER_TAC);; let int_coprime = prove (`!a b. coprime(a,b) <=> !d. d divides a /\ d divides b ==> d divides &1`, REWRITE_TAC[INT_COPRIME_GCD; INT_GCD_UNIQUE; INT_POS; INT_DIVIDES_1]);; let COPRIME = prove (`!a b. coprime(a,b) <=> !d. d divides a /\ d divides b <=> d divides &1`, MESON_TAC[INT_DIVIDES_1; INT_DIVIDES_TRANS; int_coprime]);; let INT_COPRIME_SYM = prove (`!a b. coprime(a,b) <=> coprime(b,a)`, INTEGER_TAC);; let INT_COPRIME_DIVPROD = prove (`!d a b. d divides (a * b) /\ coprime(d,a) ==> d divides b`, INTEGER_TAC);; let INT_COPRIME_1 = prove (`!a. coprime(a,&1) /\ coprime(&1,a)`, INTEGER_TAC);; let INT_GCD_COPRIME = prove (`!a b a' b'. ~(gcd(a,b) = &0) /\ a = a' * gcd(a,b) /\ b = b' * gcd(a,b) ==> coprime(a',b')`, INTEGER_TAC);; let INT_GCD_COPRIME_EXISTS = prove (`!a b. ~(gcd(a,b) = &0) ==> ?a' b'. (a = a' * gcd(a,b)) /\ (b = b' * gcd(a,b)) /\ coprime(a',b')`, INTEGER_TAC);; let INT_COPRIME_0 = prove (`(!a. coprime(a,&0) <=> a divides &1) /\ (!a. coprime(&0,a) <=> a divides &1)`, INTEGER_TAC);; let INT_COPRIME_MUL = prove (`!d a b. coprime(d,a) /\ coprime(d,b) ==> coprime(d,a * b)`, INTEGER_TAC);; let INT_COPRIME_LMUL2 = prove (`!d a b. coprime(d,a * b) ==> coprime(d,b)`, INTEGER_TAC);; let INT_COPRIME_RMUL2 = prove (`!d a b. coprime(d,a * b) ==> coprime(d,a)`, INTEGER_TAC);; let INT_COPRIME_LMUL = prove (`!d a b. coprime(a * b,d) <=> coprime(a,d) /\ coprime(b,d)`, INTEGER_TAC);; let INT_COPRIME_RMUL = prove (`!d a b. coprime(d,a * b) <=> coprime(d,a) /\ coprime(d,b)`, INTEGER_TAC);; let INT_COPRIME_REFL = prove (`!n. coprime(n,n) <=> n divides &1`, INTEGER_TAC);; let INT_COPRIME_PLUS1 = prove (`!n. coprime(n + &1,n) /\ coprime(n,n + &1)`, INTEGER_TAC);; let INT_COPRIME_MINUS1 = prove (`!n. coprime(n - &1,n) /\ coprime(n,n - &1)`, INTEGER_TAC);; let INT_COPRIME_RPOW = prove (`!m n k. coprime(m,n pow k) <=> coprime(m,n) \/ k = 0`, GEN_TAC THEN GEN_TAC THEN INDUCT_TAC THEN ASM_SIMP_TAC[INT_POW; INT_COPRIME_1; INT_COPRIME_RMUL; NOT_SUC] THEN CONV_TAC TAUT);; let INT_COPRIME_LPOW = prove (`!m n k. coprime(m pow k,n) <=> coprime(m,n) \/ k = 0`, ONCE_REWRITE_TAC[INT_COPRIME_SYM] THEN REWRITE_TAC[INT_COPRIME_RPOW]);; let INT_COPRIME_POW2 = prove (`!m n k. coprime(m pow k,n pow k) <=> coprime(m,n) \/ k = 0`, REWRITE_TAC[INT_COPRIME_RPOW; INT_COPRIME_LPOW; DISJ_ACI]);; let INT_COPRIME_POW = prove (`!n a d. coprime(d,a) ==> coprime(d,a pow n)`, SIMP_TAC[INT_COPRIME_RPOW]);; let INT_COPRIME_POW_IMP = prove (`!n a b. coprime(a,b) ==> coprime(a pow n,b pow n)`, MESON_TAC[INT_COPRIME_POW; INT_COPRIME_SYM]);; let INT_GCD_EQ_0 = prove (`!a b. gcd(a,b) = &0 <=> a = &0 /\ b = &0`, INTEGER_TAC);; let INT_DIVISION_DECOMP = prove (`!a b c. a divides (b * c) ==> ?b' c'. (a = b' * c') /\ b' divides b /\ c' divides c`, REPEAT STRIP_TAC THEN EXISTS_TAC `gcd(a,b)` THEN ASM_CASES_TAC `gcd(a,b) = &0` THEN REPEAT(POP_ASSUM MP_TAC) THENL [SIMP_TAC[INT_GCD_EQ_0; INT_GCD_0; INT_ABS_NUM]; INTEGER_TAC] THEN REWRITE_TAC[INT_MUL_LZERO] THEN MESON_TAC[INT_DIVIDES_REFL]);; let INT_DIVIDES_MUL = prove (`!m n r. m divides r /\ n divides r /\ coprime(m,n) ==> (m * n) divides r`, INTEGER_TAC);; let INT_CHINESE_REMAINDER = prove (`!a b u v. coprime(a,b) /\ ~(a = &0) /\ ~(b = &0) ==> ?x q1 q2. (x = u + q1 * a) /\ (x = v + q2 * b)`, INTEGER_TAC);; let INT_CHINESE_REMAINDER_USUAL = prove (`!a b u v. coprime(a,b) ==> ?x. (x == u) (mod a) /\ (x == v) (mod b)`, INTEGER_TAC);; let INT_COPRIME_DIVISORS = prove (`!a b d e. d divides a /\ e divides b /\ coprime(a,b) ==> coprime(d,e)`, INTEGER_TAC);; let INT_COPRIME_LNEG = prove (`!a b. coprime(--a,b) <=> coprime(a,b)`, INTEGER_TAC);; let INT_COPRIME_RNEG = prove (`!a b. coprime(a,--b) <=> coprime(a,b)`, INTEGER_TAC);; let INT_COPRIME_NEG = prove (`(!a b. coprime(--a,b) <=> coprime(a,b)) /\ (!a b. coprime(a,--b) <=> coprime(a,b))`, INTEGER_TAC);; let INT_COPRIME_LABS = prove (`!a b. coprime(abs a,b) <=> coprime(a,b)`, REWRITE_TAC[INT_ABS] THEN MESON_TAC[INT_COPRIME_LNEG]);; let INT_COPRIME_RABS = prove (`!a b. coprime(a,abs b) <=> coprime(a,b)`, REWRITE_TAC[INT_ABS] THEN MESON_TAC[INT_COPRIME_RNEG]);; let INT_COPRIME_ABS = prove (`(!a b. coprime(abs a,b) <=> coprime(a,b)) /\ (!a b. coprime(a,abs b) <=> coprime(a,b))`, REWRITE_TAC[INT_COPRIME_LABS; INT_COPRIME_RABS]);; (* ------------------------------------------------------------------------- *) (* More lemmas about congruences. *) (* ------------------------------------------------------------------------- *) let INT_CONG_MOD_0 = prove (`!x y. (x == y) (mod &0) <=> (x = y)`, INTEGER_TAC);; let INT_CONG_MOD_1 = prove (`!x y. (x == y) (mod &1)`, INTEGER_TAC);; let INT_CONG_0 = prove (`!x n. ((x == &0) (mod n) <=> n divides x)`, INTEGER_TAC);; let INT_CONG = prove (`!x y n. (x == y) (mod n) <=> n divides (x - y)`, INTEGER_TAC);; let INT_CONG_MUL_LCANCEL = prove (`!a n x y. coprime(a,n) /\ (a * x == a * y) (mod n) ==> (x == y) (mod n)`, INTEGER_TAC);; let INT_CONG_MUL_RCANCEL = prove (`!a n x y. coprime(a,n) /\ (x * a == y * a) (mod n) ==> (x == y) (mod n)`, INTEGER_TAC);; let INT_CONG_REFL = prove (`!x n. (x == x) (mod n)`, INTEGER_TAC);; let INT_EQ_IMP_CONG = prove (`!a b n. a = b ==> (a == b) (mod n)`, INTEGER_TAC);; let INT_CONG_SYM = prove (`!x y n. (x == y) (mod n) <=> (y == x) (mod n)`, INTEGER_TAC);; let INT_CONG_TRANS = prove (`!x y z n. (x == y) (mod n) /\ (y == z) (mod n) ==> (x == z) (mod n)`, INTEGER_TAC);; let INT_CONG_ADD = prove (`!x x' y y'. (x == x') (mod n) /\ (y == y') (mod n) ==> (x + y == x' + y') (mod n)`, INTEGER_TAC);; let INT_CONG_SUB = prove (`!x x' y y'. (x == x') (mod n) /\ (y == y') (mod n) ==> (x - y == x' - y') (mod n)`, INTEGER_TAC);; let INT_CONG_MUL = prove (`!x x' y y'. (x == x') (mod n) /\ (y == y') (mod n) ==> (x * y == x' * y') (mod n)`, INTEGER_TAC);; let INT_CONG_POW = prove (`!n k x y. (x == y) (mod n) ==> (x pow k == y pow k) (mod n)`, GEN_TAC THEN INDUCT_TAC THEN ASM_SIMP_TAC[INT_CONG_MUL; INT_POW; INT_CONG_REFL]);; let INT_CONG_MUL_LCANCEL_EQ = prove (`!a n x y. coprime(a,n) ==> ((a * x == a * y) (mod n) <=> (x == y) (mod n))`, INTEGER_TAC);; let INT_CONG_MUL_RCANCEL_EQ = prove (`!a n x y. coprime(a,n) ==> ((x * a == y * a) (mod n) <=> (x == y) (mod n))`, INTEGER_TAC);; let INT_CONG_ADD_LCANCEL_EQ = prove (`!a n x y. (a + x == a + y) (mod n) <=> (x == y) (mod n)`, INTEGER_TAC);; let INT_CONG_ADD_RCANCEL_EQ = prove (`!a n x y. (x + a == y + a) (mod n) <=> (x == y) (mod n)`, INTEGER_TAC);; let INT_CONG_ADD_RCANCEL = prove (`!a n x y. (x + a == y + a) (mod n) ==> (x == y) (mod n)`, INTEGER_TAC);; let INT_CONG_ADD_LCANCEL = prove (`!a n x y. (a + x == a + y) (mod n) ==> (x == y) (mod n)`, INTEGER_TAC);; let INT_CONG_ADD_LCANCEL_EQ_0 = prove (`!a n x y. (a + x == a) (mod n) <=> (x == &0) (mod n)`, INTEGER_TAC);; let INT_CONG_ADD_RCANCEL_EQ_0 = prove (`!a n x y. (x + a == a) (mod n) <=> (x == &0) (mod n)`, INTEGER_TAC);; let INT_CONG_INT_DIVIDES_MODULUS = prove (`!x y m n. (x == y) (mod m) /\ n divides m ==> (x == y) (mod n)`, INTEGER_TAC);; let INT_CONG_0_DIVIDES = prove (`!n x. (x == &0) (mod n) <=> n divides x`, INTEGER_TAC);; let INT_CONG_1_DIVIDES = prove (`!n x. (x == &1) (mod n) ==> n divides (x - &1)`, INTEGER_TAC);; let INT_CONG_DIVIDES = prove (`!x y n. (x == y) (mod n) ==> (n divides x <=> n divides y)`, INTEGER_TAC);; let INT_CONG_COPRIME = prove (`!x y n. (x == y) (mod n) ==> (coprime(n,x) <=> coprime(n,y))`, INTEGER_TAC);; let INT_CONG_MOD_MULT = prove (`!x y m n. (x == y) (mod n) /\ m divides n ==> (x == y) (mod m)`, INTEGER_TAC);; let INT_CONG_TO_1 = prove (`!a n. (a == &1) (mod n) <=> ?m. a = &1 + m * n`, INTEGER_TAC);; let INT_CONG_SOLVE = prove (`!a b n. coprime(a,n) ==> ?x. (a * x == b) (mod n)`, INTEGER_TAC);; let INT_CONG_SOLVE_UNIQUE = prove (`!a b n. coprime(a,n) ==> !x y. (a * x == b) (mod n) /\ (a * y == b) (mod n) ==> (x == y) (mod n)`, INTEGER_TAC);; let INT_CONG_CHINESE = prove (`coprime(a,b) /\ (x == y) (mod a) /\ (x == y) (mod b) ==> (x == y) (mod (a * b))`, INTEGER_TAC);; let INT_CHINESE_REMAINDER_COPRIME = prove (`!a b m n. coprime(a,b) /\ ~(a = &0) /\ ~(b = &0) /\ coprime(m,a) /\ coprime(n,b) ==> ?x. coprime(x,a * b) /\ (x == m) (mod a) /\ (x == n) (mod b)`, INTEGER_TAC);; let INT_CHINESE_REMAINDER_COPRIME_UNIQUE = prove (`!a b m n x y. coprime(a,b) /\ (x == m) (mod a) /\ (x == n) (mod b) /\ (y == m) (mod a) /\ (y == n) (mod b) ==> (x == y) (mod (a * b))`, INTEGER_TAC);; let SOLVABLE_GCD = prove (`!a b n. gcd(a,n) divides b ==> ?x. (a * x == b) (mod n)`, INTEGER_TAC);; let INT_LINEAR_CONG_POS = prove (`!n a x:int. ~(n = &0) ==> ?y. &0 <= y /\ (a * x == a * y) (mod n)`, REPEAT STRIP_TAC THEN EXISTS_TAC `x + abs(x * n):int` THEN CONJ_TAC THENL [MATCH_MP_TAC(INT_ARITH `abs(x:int) * &1 <= y ==> &0 <= x + y`) THEN REWRITE_TAC[INT_ABS_MUL] THEN MATCH_MP_TAC INT_LE_LMUL THEN ASM_INT_ARITH_TAC; MATCH_MP_TAC(INTEGER_RULE `n divides y ==> (a * x:int == a * (x + y)) (mod n)`) THEN REWRITE_TAC[INT_DIVIDES_RABS] THEN INTEGER_TAC]);; let INT_CONG_SOLVE_POS = prove (`!a b n:int. coprime(a,n) /\ ~(n = &0 /\ abs a = &1) ==> ?x. &0 <= x /\ (a * x == b) (mod n)`, REPEAT GEN_TAC THEN ASM_CASES_TAC `n:int = &0` THEN ASM_REWRITE_TAC[INT_COPRIME_0; INT_DIVIDES_ONE] THENL [INT_ARITH_TAC; ASM_MESON_TAC[INT_LINEAR_CONG_POS; INT_CONG_SOLVE; INT_CONG_TRANS; INT_CONG_SYM]]);; let INT_CONG_IMP_EQ = prove (`!x y n:int. abs(x - y) < n /\ (x == y) (mod n) ==> x = y`, REPEAT GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN ONCE_REWRITE_TAC[int_congruent; GSYM INT_SUB_0] THEN DISCH_THEN(X_CHOOSE_THEN `q:int` SUBST_ALL_TAC) THEN FIRST_X_ASSUM(MP_TAC o MATCH_MP (ARITH_RULE `abs(n * q) < n ==> abs(n * q) < abs n * &1`)) THEN REWRITE_TAC[INT_ABS_MUL; INT_ENTIRE] THEN REWRITE_TAC[INT_ARITH `abs n * (q:int) < abs n * &1 <=> ~(&0 <= abs n * (q - &1))`] THEN ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN REWRITE_TAC[DE_MORGAN_THM] THEN STRIP_TAC THEN MATCH_MP_TAC INT_LE_MUL THEN ASM_INT_ARITH_TAC);; (* ------------------------------------------------------------------------- *) (* A stronger form of the CRT. *) (* ------------------------------------------------------------------------- *) let INT_CRT_STRONG = prove (`!a1 a2 n1 n2:int. (a1 == a2) (mod (gcd(n1,n2))) ==> ?x. (x == a1) (mod n1) /\ (x == a2) (mod n2)`, INTEGER_TAC);; let INT_CRT_STRONG_IFF = prove (`!a1 a2 n1 n2:int. (?x. (x == a1) (mod n1) /\ (x == a2) (mod n2)) <=> (a1 == a2) (mod (gcd(n1,n2)))`, INTEGER_TAC);; (* ------------------------------------------------------------------------- *) (* Other miscellaneous lemmas. *) (* ------------------------------------------------------------------------- *) let EVEN_SQUARE_MOD4 = prove (`((&2 * n) pow 2 == &0) (mod &4)`, INTEGER_TAC);; let ODD_SQUARE_MOD4 = prove (`((&2 * n + &1) pow 2 == &1) (mod &4)`, INTEGER_TAC);; let INT_DIVIDES_LE = prove (`!x y. x divides y ==> abs(x) <= abs(y) \/ y = &0`, REWRITE_TAC[int_divides; LEFT_IMP_EXISTS_THM] THEN MAP_EVERY X_GEN_TAC [`x:int`; `y:int`; `z:int`] THEN DISCH_THEN SUBST1_TAC THEN REWRITE_TAC[INT_ABS_MUL; INT_ENTIRE] THEN REWRITE_TAC[INT_ARITH `x <= x * z <=> &0 <= x * (z - &1)`] THEN ASM_CASES_TAC `x = &0` THEN ASM_REWRITE_TAC[] THEN ASM_CASES_TAC `z = &0` THEN ASM_REWRITE_TAC[] THEN MATCH_MP_TAC INT_LE_MUL THEN ASM_INT_ARITH_TAC);; let INT_DIVIDES_POW_LE = prove (`!p m n. &2 <= abs p ==> ((p pow m) divides (p pow n) <=> m <= n)`, REPEAT STRIP_TAC THEN EQ_TAC THENL [DISCH_THEN(MP_TAC o MATCH_MP INT_DIVIDES_LE) THEN ASM_SIMP_TAC[INT_POW_EQ_0; INT_ARITH `&2 <= abs p ==> ~(p = &0)`] THEN ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN REWRITE_TAC[INT_NOT_LE; NOT_LE; INT_ABS_POW] THEN ASM_MESON_TAC[INT_POW_MONO_LT; ARITH_RULE `&2 <= x ==> &1 < x`]; SIMP_TAC[LE_EXISTS; LEFT_IMP_EXISTS_THM; INT_POW_ADD] THEN INTEGER_TAC]);; (* ------------------------------------------------------------------------- *) (* Integer primality / irreducibility. *) (* ------------------------------------------------------------------------- *) let int_prime = new_definition `int_prime p <=> abs(p) > &1 /\ !x. x divides p ==> abs(x) = &1 \/ abs(x) = abs(p)`;; let INT_PRIME_NEG = prove (`!p. int_prime(--p) <=> int_prime p`, REWRITE_TAC[int_prime; INT_DIVIDES_RNEG; INT_ABS_NEG]);; let INT_PRIME_ABS = prove (`!p. int_prime(abs p) <=> int_prime p`, GEN_TAC THEN REWRITE_TAC[INT_ABS] THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[INT_PRIME_NEG]);; let INT_PRIME_GE_2 = prove (`!p. int_prime p ==> &2 <= abs(p)`, REWRITE_TAC[int_prime] THEN INT_ARITH_TAC);; let INT_PRIME_0 = prove (`~(int_prime(&0))`, REWRITE_TAC[int_prime] THEN INT_ARITH_TAC);; let INT_PRIME_1 = prove (`~(int_prime(&1))`, REWRITE_TAC[int_prime] THEN INT_ARITH_TAC);; let INT_PRIME_2 = prove (`int_prime(&2)`, REWRITE_TAC[int_prime] THEN CONV_TAC INT_REDUCE_CONV THEN X_GEN_TAC `x:int` THEN ASM_CASES_TAC `x = &0` THEN ASM_REWRITE_TAC[INT_DIVIDES_ZERO] THEN CONV_TAC INT_REDUCE_CONV THEN DISCH_THEN(MP_TAC o MATCH_MP INT_DIVIDES_LE) THEN ASM_INT_ARITH_TAC);; let INT_PRIME_FACTOR = prove (`!x. ~(abs x = &1) ==> ?p. int_prime p /\ p divides x`, MATCH_MP_TAC WF_INT_MEASURE THEN EXISTS_TAC `abs` THEN REWRITE_TAC[INT_ABS_POS] THEN X_GEN_TAC `x:int` THEN REPEAT STRIP_TAC THEN ASM_CASES_TAC `int_prime x` THENL [EXISTS_TAC `x:int` THEN ASM_REWRITE_TAC[] THEN REPEAT(POP_ASSUM MP_TAC) THEN INTEGER_TAC; ALL_TAC] THEN ASM_CASES_TAC `x = &0` THEN ASM_REWRITE_TAC[] THENL [EXISTS_TAC `&2` THEN ASM_REWRITE_TAC[INT_PRIME_2; INT_DIVIDES_0]; ALL_TAC] THEN FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE RAND_CONV [int_prime]) THEN ASM_SIMP_TAC[INT_ARITH `~(x = &0) /\ ~(abs x = &1) ==> abs x > &1`] THEN REWRITE_TAC[NOT_FORALL_THM; NOT_IMP; DE_MORGAN_THM] THEN DISCH_THEN(X_CHOOSE_THEN `y:int` STRIP_ASSUME_TAC) THEN FIRST_X_ASSUM(MP_TAC o SPEC `y:int`) THEN ASM_REWRITE_TAC[] THEN ANTS_TAC THENL [FIRST_X_ASSUM(MP_TAC o MATCH_MP INT_DIVIDES_LE) THEN ASM_INT_ARITH_TAC; MATCH_MP_TAC MONO_EXISTS THEN GEN_TAC THEN SIMP_TAC[] THEN UNDISCH_TAC `y divides x` THEN INTEGER_TAC]);; let INT_PRIME_FACTOR_LT = prove (`!n m p. int_prime(p) /\ ~(n = &0) /\ n = p * m ==> abs m < abs n`, REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[INT_ABS_MUL] THEN MATCH_MP_TAC(INT_ARITH `&0 < m * (p - &1) ==> m < p * m`) THEN MATCH_MP_TAC INT_LT_MUL THEN UNDISCH_TAC `~(n = &0)` THEN ASM_CASES_TAC `m = &0` THEN ASM_REWRITE_TAC[INT_MUL_RZERO] THEN DISCH_THEN(K ALL_TAC) THEN CONJ_TAC THENL [ASM_INT_ARITH_TAC; ALL_TAC] THEN FIRST_ASSUM(MP_TAC o MATCH_MP INT_PRIME_GE_2) THEN INT_ARITH_TAC);; let INT_PRIME_FACTOR_INDUCT = prove (`!P. P(&0) /\ P(&1) /\ P(-- &1) /\ (!p n. int_prime p /\ ~(n = &0) /\ P n ==> P(p * n)) ==> !n. P n`, GEN_TAC THEN STRIP_TAC THEN MATCH_MP_TAC WF_INT_MEASURE THEN EXISTS_TAC `abs` THEN REWRITE_TAC[INT_ABS_POS] THEN X_GEN_TAC `n:int` THEN DISCH_TAC THEN ASM_CASES_TAC `n = &0` THEN ASM_REWRITE_TAC[] THEN ASM_CASES_TAC `abs n = &1` THENL [ASM_MESON_TAC[INT_ARITH `abs x = &a <=> x = &a \/ x = -- &a`]; ALL_TAC] THEN FIRST_ASSUM(X_CHOOSE_THEN `p:int` STRIP_ASSUME_TAC o MATCH_MP INT_PRIME_FACTOR) THEN FIRST_X_ASSUM(X_CHOOSE_THEN `d:int` SUBST_ALL_TAC o GEN_REWRITE_RULE I [int_divides]) THEN FIRST_X_ASSUM(MP_TAC o SPECL [`p:int`; `d:int`]) THEN RULE_ASSUM_TAC(REWRITE_RULE[INT_ENTIRE; DE_MORGAN_THM]) THEN DISCH_THEN MATCH_MP_TAC THEN ASM_REWRITE_TAC[] THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_MESON_TAC[INT_PRIME_FACTOR_LT; INT_ENTIRE]);; (* ------------------------------------------------------------------------- *) (* Infinitude. *) (* ------------------------------------------------------------------------- *) let INT_DIVIDES_FACT = prove (`!n x. &1 <= abs(x) /\ abs(x) <= &n ==> x divides &(FACT n)`, INDUCT_TAC THENL [INT_ARITH_TAC; ALL_TAC] THEN REWRITE_TAC[FACT; INT_ARITH `x <= &n <=> x = &n \/ x < &n`] THEN REWRITE_TAC[GSYM INT_OF_NUM_SUC; INT_ARITH `x < &m + &1 <=> x <= &m`] THEN REWRITE_TAC[INT_OF_NUM_SUC; GSYM INT_OF_NUM_MUL] THEN REPEAT STRIP_TAC THEN ASM_SIMP_TAC[INT_DIVIDES_LMUL] THEN MATCH_MP_TAC INT_DIVIDES_RMUL THEN ASM_MESON_TAC[INT_DIVIDES_LABS; INT_DIVIDES_REFL]);; let INT_EUCLID_BOUND = prove (`!n. ?p. int_prime(p) /\ &n < p /\ p <= &(FACT n) + &1`, GEN_TAC THEN MP_TAC(SPEC `&(FACT n) + &1` INT_PRIME_FACTOR) THEN REWRITE_TAC[INT_OF_NUM_ADD; INT_ABS_NUM; INT_OF_NUM_EQ] THEN REWRITE_TAC[EQ_ADD_RCANCEL_0; FACT_NZ; GSYM INT_OF_NUM_ADD] THEN DISCH_THEN(X_CHOOSE_THEN `p:int` STRIP_ASSUME_TAC) THEN EXISTS_TAC `abs p` THEN ASM_REWRITE_TAC[INT_PRIME_ABS] THEN CONJ_TAC THENL [ALL_TAC; FIRST_ASSUM(MP_TAC o MATCH_MP INT_DIVIDES_LE) THEN REWRITE_TAC[GSYM INT_OF_NUM_ADD; GSYM INT_OF_NUM_SUC] THEN INT_ARITH_TAC] THEN REWRITE_TAC[GSYM INT_NOT_LE] THEN DISCH_TAC THEN MP_TAC(SPECL [`n:num`; `p:int`] INT_DIVIDES_FACT) THEN ASM_SIMP_TAC[INT_PRIME_GE_2; INT_ARITH `&2 <= p ==> &1 <= p`] THEN DISCH_TAC THEN SUBGOAL_THEN `p divides &1` MP_TAC THENL [REPEAT(POP_ASSUM MP_TAC) THEN INTEGER_TAC; REWRITE_TAC[INT_DIVIDES_ONE] THEN ASM_MESON_TAC[INT_PRIME_NEG; INT_PRIME_1]]);; let INT_EUCLID = prove (`!n. ?p. int_prime(p) /\ p > n`, MP_TAC INT_IMAGE THEN MATCH_MP_TAC MONO_FORALL THEN X_GEN_TAC `n:int` THEN REWRITE_TAC[INT_GT] THEN ASM_REWRITE_TAC[OR_EXISTS_THM; LEFT_IMP_EXISTS_THM] THEN MP_TAC INT_EUCLID_BOUND THEN MATCH_MP_TAC MONO_FORALL THEN X_GEN_TAC `m:num` THEN DISCH_THEN(fun th -> DISCH_TAC THEN MP_TAC th) THEN MATCH_MP_TAC MONO_EXISTS THEN SIMP_TAC[] THEN FIRST_X_ASSUM(DISJ_CASES_THEN SUBST1_TAC) THEN INT_ARITH_TAC);; let INT_PRIMES_INFINITE = prove (`INFINITE {p | int_prime p}`, SUBGOAL_THEN `INFINITE {n | int_prime(&n)}` MP_TAC THEN REWRITE_TAC[INFINITE; CONTRAPOS_THM] THENL [REWRITE_TAC[num_FINITE; IN_ELIM_THM] THEN REWRITE_TAC[NOT_EXISTS_THM; NOT_FORALL_THM; NOT_IMP; NOT_LE] THEN REWRITE_TAC[GSYM INT_OF_NUM_LT; INT_EXISTS_POS] THEN MP_TAC INT_EUCLID_BOUND THEN MATCH_MP_TAC MONO_FORALL THEN GEN_TAC THEN MATCH_MP_TAC MONO_EXISTS THEN GEN_TAC THEN SIMP_TAC[] THEN INT_ARITH_TAC; MP_TAC(ISPECL [`&`; `{p | int_prime p}`] FINITE_IMAGE_INJ) THEN REWRITE_TAC[INT_OF_NUM_EQ; IN_ELIM_THM]]);; let INT_COPRIME_PRIME = prove (`!p a b. coprime(a,b) ==> ~(int_prime(p) /\ p divides a /\ p divides b)`, REWRITE_TAC[int_coprime] THEN MESON_TAC[INT_DIVIDES_ONE; INT_PRIME_NEG; INT_PRIME_1]);; let INT_COPRIME_PRIME_EQ = prove (`!a b. coprime(a,b) <=> !p. ~(int_prime(p) /\ p divides a /\ p divides b)`, REPEAT GEN_TAC THEN EQ_TAC THENL [MESON_TAC[INT_COPRIME_PRIME]; ALL_TAC] THEN ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN REWRITE_TAC[int_coprime; INT_DIVIDES_ONE_ABS] THEN ONCE_REWRITE_TAC[NOT_FORALL_THM] THEN REWRITE_TAC[NOT_IMP] THEN DISCH_THEN(X_CHOOSE_THEN `d:int` STRIP_ASSUME_TAC) THEN FIRST_ASSUM(X_CHOOSE_TAC `p:int` o MATCH_MP INT_PRIME_FACTOR) THEN EXISTS_TAC `p:int` THEN ASM_MESON_TAC[INT_DIVIDES_TRANS]);; let INT_PRIME_COPRIME = prove (`!x p. int_prime(p) ==> p divides x \/ coprime(p,x)`, REPEAT STRIP_TAC THEN REWRITE_TAC[int_coprime] THEN MATCH_MP_TAC(TAUT `(~b ==> a) ==> a \/ b`) THEN REWRITE_TAC[NOT_FORALL_THM; NOT_IMP; INT_DIVIDES_ONE_ABS] THEN DISCH_THEN(X_CHOOSE_THEN `d:int` STRIP_ASSUME_TAC) THEN FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [int_prime]) THEN DISCH_THEN(MP_TAC o SPEC `d:int` o CONJUNCT2) THEN ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[INT_DIVIDES_TRANS; INT_DIVIDES_LABS; INT_DIVIDES_RABS]);; let INT_PRIME_COPRIME_EQ = prove (`!p n. int_prime p ==> (coprime(p,n) <=> ~(p divides n))`, REPEAT STRIP_TAC THEN MATCH_MP_TAC(TAUT `(b \/ a) /\ ~(a /\ b) ==> (a <=> ~b)`) THEN ASM_SIMP_TAC[INT_PRIME_COPRIME; int_coprime; INT_DIVIDES_ONE_ABS] THEN ASM_MESON_TAC[INT_DIVIDES_REFL; INT_PRIME_1; INT_PRIME_ABS]);; let INT_COPRIME_PRIMEPOW = prove (`!p k m. int_prime p /\ ~(k = 0) ==> (coprime(m,p pow k) <=> ~(p divides m))`, SIMP_TAC[INT_COPRIME_RPOW] THEN ONCE_REWRITE_TAC[INT_COPRIME_SYM] THEN SIMP_TAC[INT_PRIME_COPRIME_EQ]);; let INT_COPRIME_BEZOUT = prove (`!a b. coprime(a,b) <=> ?x y. a * x + b * y = &1`, INTEGER_TAC);; let INT_COPRIME_BEZOUT_ALT = prove (`!a b. coprime(a,b) ==> ?x y. a * x = b * y + &1`, INTEGER_TAC);; let INT_BEZOUT_PRIME = prove (`!a p. int_prime p /\ ~(p divides a) ==> ?x y. a * x = p * y + &1`, MESON_TAC[INT_COPRIME_BEZOUT_ALT; INT_COPRIME_SYM; INT_PRIME_COPRIME_EQ]);; let INT_PRIME_DIVPROD = prove (`!p a b. int_prime(p) /\ p divides (a * b) ==> p divides a \/ p divides b`, ONCE_REWRITE_TAC[TAUT `a /\ b ==> c \/ d <=> a ==> (~c /\ ~d ==> ~b)`] THEN SIMP_TAC[GSYM INT_PRIME_COPRIME_EQ] THEN INTEGER_TAC);; let INT_PRIME_DIVPROD_EQ = prove (`!p a b. int_prime(p) ==> (p divides (a * b) <=> p divides a \/ p divides b)`, MESON_TAC[INT_PRIME_DIVPROD; INT_DIVIDES_LMUL; INT_DIVIDES_RMUL]);; let INT_PRIME_DIVPOW = prove (`!n p x. int_prime(p) /\ p divides (x pow n) ==> p divides x`, REPEAT GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN ASM_SIMP_TAC[GSYM INT_PRIME_COPRIME_EQ; INT_COPRIME_POW]);; let INT_PRIME_DIVPOW_N = prove (`!n p x. int_prime p /\ p divides (x pow n) ==> (p pow n) divides (x pow n)`, MESON_TAC[INT_PRIME_DIVPOW; INT_DIVIDES_POW]);; let INT_COPRIME_SOS = prove (`!x y. coprime(x,y) ==> coprime(x * y,x pow 2 + y pow 2)`, INTEGER_TAC);; let INT_PRIME_IMP_NZ = prove (`!p. int_prime p ==> ~(p = &0)`, GEN_TAC THEN DISCH_THEN(MP_TAC o MATCH_MP INT_PRIME_GE_2) THEN INT_ARITH_TAC);; let INT_DISTINCT_PRIME_COPRIME = prove (`!p q. int_prime p /\ int_prime q /\ ~(abs p = abs q) ==> coprime(p,q)`, REWRITE_TAC[GSYM INT_DIVIDES_ANTISYM_ABS] THEN MESON_TAC[INT_COPRIME_SYM; INT_PRIME_COPRIME_EQ]);; let INT_PRIME_COPRIME_LT = prove (`!x p. int_prime p /\ &0 < abs x /\ abs x < abs p ==> coprime(x,p)`, ONCE_REWRITE_TAC[INT_COPRIME_SYM] THEN SIMP_TAC[INT_PRIME_COPRIME_EQ] THEN REPEAT GEN_TAC THEN STRIP_TAC THEN DISCH_THEN(MP_TAC o MATCH_MP INT_DIVIDES_LE) THEN ASM_INT_ARITH_TAC);; let INT_DIVIDES_PRIME_PRIME = prove (`!p q. int_prime p /\ int_prime q ==> (p divides q <=> abs p = abs q)`, REPEAT STRIP_TAC THEN EQ_TAC THENL [ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN ASM_SIMP_TAC[GSYM INT_PRIME_COPRIME_EQ; INT_DISTINCT_PRIME_COPRIME]; SIMP_TAC[GSYM INT_DIVIDES_ANTISYM_ABS]]);; let INT_COPRIME_POW_DIVPROD = prove (`!d a b. (d pow n) divides (a * b) /\ coprime(d,a) ==> (d pow n) divides b`, MESON_TAC[INT_COPRIME_DIVPROD; INT_COPRIME_POW; INT_COPRIME_SYM]);; let INT_PRIME_COPRIME_CASES = prove (`!p a b. int_prime p /\ coprime(a,b) ==> coprime(p,a) \/ coprime(p,b)`, MESON_TAC[INT_COPRIME_PRIME; INT_PRIME_COPRIME_EQ]);; let INT_PRIME_DIVPROD_POW = prove (`!n p a b. int_prime(p) /\ coprime(a,b) /\ (p pow n) divides (a * b) ==> (p pow n) divides a \/ (p pow n) divides b`, MESON_TAC[INT_COPRIME_POW_DIVPROD; INT_PRIME_COPRIME_CASES; INT_MUL_SYM]);; let INT_DIVIDES_POW2_REV = prove (`!n a b. (a pow n) divides (b pow n) /\ ~(n = 0) ==> a divides b`, REPEAT GEN_TAC THEN ASM_CASES_TAC `gcd(a,b) = &0` THENL [ASM_MESON_TAC[INT_GCD_EQ_0; INT_DIVIDES_REFL]; ALL_TAC] THEN FIRST_ASSUM(MP_TAC o MATCH_MP INT_GCD_COPRIME_EXISTS) THEN STRIP_TAC THEN DISCH_THEN(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN ONCE_ASM_REWRITE_TAC[] THEN REWRITE_TAC[INT_POW_MUL] THEN ASM_SIMP_TAC[INT_POW_EQ_0; INT_DIVIDES_RMUL2_EQ] THEN DISCH_THEN(MP_TAC o MATCH_MP (INTEGER_RULE `a divides b ==> coprime(a,b) ==> a divides &1`)) THEN ASM_SIMP_TAC[INT_COPRIME_POW2] THEN ASM_MESON_TAC[INT_DIVIDES_POW2; INT_DIVIDES_TRANS; INT_DIVIDES_1]);; let INT_DIVIDES_POW2_EQ = prove (`!n a b. ~(n = 0) ==> ((a pow n) divides (b pow n) <=> a divides b)`, MESON_TAC[INT_DIVIDES_POW2_REV; INT_DIVIDES_POW]);; let INT_POW_MUL_EXISTS = prove (`!m n p k. ~(m = &0) /\ m pow k * n = p pow k ==> ?q. n = q pow k`, REPEAT GEN_TAC THEN ASM_CASES_TAC `k = 0` THEN ASM_SIMP_TAC[INT_POW; INT_MUL_LID] THEN STRIP_TAC THEN MP_TAC(SPECL [`k:num`; `m:int`; `p:int`] INT_DIVIDES_POW2_REV) THEN ASM_REWRITE_TAC[] THEN ANTS_TAC THENL [ASM_MESON_TAC[int_divides; INT_MUL_SYM]; ALL_TAC] THEN REWRITE_TAC[int_divides] THEN DISCH_THEN(CHOOSE_THEN SUBST_ALL_TAC) THEN FIRST_X_ASSUM(MP_TAC o SYM) THEN ASM_SIMP_TAC[INT_POW_MUL; INT_EQ_MUL_LCANCEL; INT_POW_EQ_0] THEN MESON_TAC[]);; let INT_COPRIME_POW_ABS = prove (`!n a b c. coprime(a,b) /\ a * b = c pow n ==> ?r s. abs a = r pow n /\ abs b = s pow n`, GEN_TAC THEN GEN_REWRITE_TAC BINDER_CONV [SWAP_FORALL_THM] THEN GEN_REWRITE_TAC I [SWAP_FORALL_THM] THEN ASM_CASES_TAC `n = 0` THENL [ASM_REWRITE_TAC[INT_POW] THEN MESON_TAC[INT_ABS_MUL_1; INT_ABS_NUM]; ALL_TAC] THEN MATCH_MP_TAC INT_PRIME_FACTOR_INDUCT THEN REPEAT CONJ_TAC THENL [REPEAT GEN_TAC THEN ASM_REWRITE_TAC[INT_POW_ZERO; INT_ENTIRE] THEN DISCH_THEN(CONJUNCTS_THEN2 MP_TAC DISJ_CASES_TAC) THEN ASM_SIMP_TAC[INT_COPRIME_0; INT_DIVIDES_ONE_ABS; INT_ABS_NUM] THEN ASM_MESON_TAC[INT_POW_ONE; INT_POW_ZERO]; REPEAT STRIP_TAC THEN FIRST_X_ASSUM(MP_TAC o AP_TERM `abs:int->int`) THEN SIMP_TAC[INT_POW_ONE; INT_ABS_NUM; INT_ABS_MUL_1] THEN MESON_TAC[INT_POW_ONE]; REPEAT STRIP_TAC THEN FIRST_X_ASSUM(MP_TAC o AP_TERM `abs:int->int`) THEN SIMP_TAC[INT_POW_ONE; INT_ABS_POW; INT_ABS_NEG; INT_ABS_NUM; INT_ABS_MUL_1] THEN MESON_TAC[INT_POW_ONE]; REWRITE_TAC[INT_POW_MUL] THEN REPEAT STRIP_TAC THEN SUBGOAL_THEN `p pow n divides a \/ p pow n divides b` MP_TAC THENL [ASM_MESON_TAC[INT_PRIME_DIVPROD_POW; int_divides]; ALL_TAC] THEN REWRITE_TAC[int_divides] THEN DISCH_THEN(DISJ_CASES_THEN(X_CHOOSE_THEN `d:int` SUBST_ALL_TAC)) THEN FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [INT_COPRIME_SYM]) THEN ASM_SIMP_TAC[INT_COPRIME_RMUL; INT_COPRIME_LMUL; INT_COPRIME_LPOW; INT_COPRIME_RPOW] THEN STRIP_TAC THENL [FIRST_X_ASSUM(MP_TAC o SPECL [`b:int`; `d:int`]); FIRST_X_ASSUM(MP_TAC o SPECL [`d:int`; `a:int`])] THEN ASM_REWRITE_TAC[] THEN (ANTS_TAC THENL [MATCH_MP_TAC(INT_RING `!p. ~(p = &0) /\ a * p = b * p ==> a = b`) THEN EXISTS_TAC `p pow n` THEN ASM_SIMP_TAC[INT_POW_EQ_0; INT_PRIME_IMP_NZ] THEN FIRST_X_ASSUM(MP_TAC o SYM) THEN CONV_TAC INT_RING; STRIP_TAC THEN ASM_REWRITE_TAC[INT_ABS_POW; GSYM INT_POW_MUL; INT_ABS_MUL] THEN MESON_TAC[]])]);; let INT_COPRIME_POW_ODD = prove (`!n a b c. ODD n /\ coprime(a,b) /\ a * b = c pow n ==> ?r s. a = r pow n /\ b = s pow n`, REPEAT STRIP_TAC THEN MP_TAC(SPECL [`n:num`; `a:int`; `b:int`; `c:int`] INT_COPRIME_POW_ABS) THEN ASM_REWRITE_TAC[INT_ABS] THEN REWRITE_TAC[RIGHT_EXISTS_AND_THM; LEFT_EXISTS_AND_THM] THEN MATCH_MP_TAC MONO_AND THEN REWRITE_TAC[INT_ABS] THEN ASM_MESON_TAC[INT_POW_NEG; INT_NEG_NEG; NOT_ODD]);; let INT_DIVIDES_PRIME_POW_LE = prove (`!p q m n. int_prime p /\ int_prime q ==> ((p pow m) divides (q pow n) <=> m = 0 \/ abs p = abs q /\ m <= n)`, REPEAT STRIP_TAC THEN ASM_CASES_TAC `m = 0` THEN ASM_REWRITE_TAC[INT_POW; INT_DIVIDES_1] THEN GEN_REWRITE_TAC LAND_CONV [GSYM INT_DIVIDES_LABS] THEN GEN_REWRITE_TAC LAND_CONV [GSYM INT_DIVIDES_RABS] THEN REWRITE_TAC[INT_ABS_POW] THEN EQ_TAC THENL [DISCH_TAC THEN MATCH_MP_TAC(TAUT `a /\ (a ==> b) ==> a /\ b`); ALL_TAC] THEN ASM_MESON_TAC[INT_DIVIDES_POW_LE; INT_PRIME_GE_2; INT_PRIME_DIVPOW; INT_ABS_ABS; INT_PRIME_ABS; INT_DIVIDES_POW2; INT_DIVIDES_PRIME_PRIME]);; let INT_EQ_PRIME_POW_ABS = prove (`!p q m n. int_prime p /\ int_prime q ==> (abs p pow m = abs q pow n <=> m = 0 /\ n = 0 \/ abs p = abs q /\ m = n)`, REPEAT STRIP_TAC THEN REWRITE_TAC[GSYM INT_ABS_POW] THEN GEN_REWRITE_TAC LAND_CONV [GSYM INT_DIVIDES_ANTISYM_ABS] THEN ASM_SIMP_TAC[INT_DIVIDES_PRIME_POW_LE; INT_PRIME_ABS] THEN ASM_CASES_TAC `abs p = abs q` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);; let INT_EQ_PRIME_POW_POS = prove (`!p q m n. int_prime p /\ int_prime q /\ &0 <= p /\ &0 <= q ==> (p pow m = q pow n <=> m = 0 /\ n = 0 \/ p = q /\ m = n)`, REPEAT STRIP_TAC THEN MP_TAC(SPECL [`p:int`; `q:int`; `m:num`; `n:num`] INT_EQ_PRIME_POW_ABS) THEN ASM_SIMP_TAC[INT_ABS]);; let INT_DIVIDES_FACT_PRIME = prove (`!p. int_prime p ==> !n. p divides &(FACT n) <=> abs p <= &n`, GEN_TAC THEN DISCH_TAC THEN INDUCT_TAC THEN REWRITE_TAC[FACT] THENL [REWRITE_TAC[INT_ARITH `abs x <= &0 <=> x = &0`] THEN ASM_MESON_TAC[INT_DIVIDES_ONE; INT_PRIME_NEG; INT_PRIME_0; INT_PRIME_1]; ASM_SIMP_TAC[INT_PRIME_DIVPROD_EQ; GSYM INT_OF_NUM_MUL] THEN REWRITE_TAC[GSYM INT_OF_NUM_SUC] THEN ASM_MESON_TAC[INT_DIVIDES_LE; INT_ARITH `x <= n ==> x <= n + &1`; INT_DIVIDES_REFL; INT_DIVIDES_LABS; INT_ARITH `p <= n + &1 ==> p <= n \/ p = n + &1`; INT_ARITH `~(&n + &1 = &0)`; INT_ARITH `abs(&n + &1) = &n + &1`]]);;