1(* ------------------------------------------------------------------------- *) 2(* Helper Theorems - a collection of useful results -- for Numbers. *) 3(* ------------------------------------------------------------------------- *) 4 5(*===========================================================================*) 6 7(* add all dependent libraries for script *) 8open HolKernel boolLib bossLib Parse; 9 10(* declare new theory at start *) 11val _ = new_theory "helperNum"; 12 13(* ------------------------------------------------------------------------- *) 14 15 16(* val _ = load "jcLib"; *) 17open jcLib; 18 19(* open dependent theories *) 20open pred_setTheory; 21 22(* val _ = load "dividesTheory"; *) 23(* val _ = load "gcdTheory"; *) 24open arithmeticTheory dividesTheory 25open gcdTheory; (* for P_EUCLIDES *) 26 27 28(* ------------------------------------------------------------------------- *) 29(* HelperNum Documentation *) 30(* ------------------------------------------------------------------------- *) 31(* Overloading: 32 SQ n = n * n 33 HALF n = n DIV 2 34 TWICE n = 2 * n 35 n divides m = divides n m 36*) 37(* Definitions and Theorems (# are exported): 38 39 Arithmetic Theorems: 40 THREE |- 3 = SUC 2 41 FOUR |- 4 = SUC 3 42 FIVE |- 5 = SUC 4 43 ZERO_LE_ALL |- !n. 0 <= n 44 NOT_ZERO |- !n. n <> 0 <=> 0 < n 45 ONE_LT_POS |- !n. 1 < n ==> 0 < n 46 ONE_LT_NONZERO |- !n. 1 < n ==> n <> 0 47 NOT_LT_ONE |- !n. ~(1 < n) <=> (n = 0) \/ (n = 1) 48 NOT_ZERO_GE_ONE |- !n. n <> 0 <=> 1 <= n 49 ONE_LE_NONZERO |- !n. 1 <= n <=> n <> 0 50 LE_ONE |- !n. n <= 1 <=> (n = 0) \/ (n = 1) 51 LT_ONE |- !n. n < 1 <=> (n = 0) 52 LT_TWO |- !n. n < 2 <=> (n = 0) \/ (n = 1) 53 LESS_TWICE |- !m n. m < TWICE n ==> m - n < n 54 LESS_NOT_EQ |- !m n. m < n ==> m <> n 55 LESS_SELF |- !n. ~(n < n) 56 LESS_SUC |- !n. n < SUC n 57 PRE_LESS |- !n. 0 < n ==> PRE n < n 58 LESS_EQ_SUC |- !n. 0 < n ==> ?m. n = SUC m 59 SUC_POS |- !n. 0 < SUC n 60 SUC_NOT_ZERO |- !n. SUC n <> 0 61 ONE_NOT_ZERO |- 1 <> 0 62 SUC_ADD_SUC |- !m n. SUC m + SUC n = m + n + 2 63 SUC_MULT_SUC |- !m n. SUC m * SUC n = m * n + m + n + 1 64 SUC_EQ |- !m n. (SUC m = SUC n) <=> (m = n) 65 TWICE_EQ_0 |- !n. (TWICE n = 0) <=> (n = 0) 66 SQ_EQ_0 |- !n. (SQ n = 0) <=> (n = 0) 67 SQ_EQ_1 |- !n. (SQ n = 1) <=> (n = 1) 68 MULT3_EQ_0 |- !x y z. (x * y * z = 0) <=> ((x = 0) \/ (y = 0) \/ (z = 0)) 69 MULT3_EQ_1 |- !x y z. (x * y * z = 1) <=> ((x = 1) /\ (y = 1) /\ (z = 1)) 70 SQ_0 |- 0 ** 2 = 0 71 EXP_2_EQ_0 |- !n. (n ** 2 = 0) <=> (n = 0) 72 73 Maximum and minimum: 74 MAX_ALT |- !m n. MAX m n = if m <= n then n else m 75 MIN_ALT |- !m n. MIN m n = if m <= n then m else n 76 MAX_SWAP |- !f. (!x y. x <= y ==> f x <= f y) ==> !x y. f (MAX x y) = MAX (f x) (f y) 77 MIN_SWAP |- !f. (!x y. x <= y ==> f x <= f y) ==> !x y. f (MIN x y) = MIN (f x) (f y) 78 SUC_MAX |- !m n. SUC (MAX m n) = MAX (SUC m) (SUC n) 79 SUC_MIN |- !m n. SUC (MIN m n) = MIN (SUC m) (SUC n) 80 MAX_SUC |- !m n. MAX (SUC m) (SUC n) = SUC (MAX m n) 81 MIN_SUC |- !m n. MIN (SUC m) (SUC n) = SUC (MIN m n) 82 MAX_LESS |- !x y n. x < n /\ y < n ==> MAX x y < n 83 MAX_CASES |- !m n. (MAX n m = n) \/ (MAX n m = m) 84 MIN_CASES |- !m n. (MIN n m = n) \/ (MIN n m = m) 85 MAX_EQ_0 |- !m n. (MAX n m = 0) <=> (n = 0) /\ (m = 0) 86 MIN_EQ_0 |- !m n. (MIN n m = 0) <=> (n = 0) \/ (m = 0) 87 MAX_IS_MAX |- !m n. m <= MAX m n /\ n <= MAX m n 88 MIN_IS_MIN |- !m n. MIN m n <= m /\ MIN m n <= n 89 MAX_ID |- !m n. MAX (MAX m n) n = MAX m n /\ MAX m (MAX m n) = MAX m n 90 MIN_ID |- !m n. MIN (MIN m n) n = MIN m n /\ MIN m (MIN m n) = MIN m n 91 MAX_LE_PAIR |- !a b c d. a <= b /\ c <= d ==> MAX a c <= MAX b d 92 MIN_LE_PAIR |- !a b c d. a <= b /\ c <= d ==> MIN a c <= MIN b d 93 MAX_ADD |- !a b c. MAX a (b + c) <= MAX a b + MAX a c 94 MIN_ADD |- !a b c. MIN a (b + c) <= MIN a b + MIN a c 95 MAX_1_POS |- !n. 0 < n ==> MAX 1 n = n 96 MIN_1_POS |- !n. 0 < n ==> MIN 1 n = 1 97 MAX_LE_SUM |- !m n. MAX m n <= m + n 98 MIN_LE_SUM |- !m n. MIN m n <= m + n 99 MAX_1_EXP |- !n m. MAX 1 (m ** n) = MAX 1 m ** n 100 MIN_1_EXP |- !n m. MIN 1 (m ** n) = MIN 1 m ** n 101 102 Arithmetic Manipulations: 103 MULT_POS |- !m n. 0 < m /\ 0 < n ==> 0 < m * n 104 MULT_COMM_ASSOC |- !m n p. m * (n * p) = n * (m * p) 105 EQ_MULT_RCANCEL |- !m n p. (n * m = p * m) <=> (m = 0) \/ (n = p) 106 MULT_RIGHT_CANCEL |- !m n p. (n * p = m * p) <=> (p = 0) \/ (n = m) 107 MULT_LEFT_CANCEL |- !m n p. (p * n = p * m) <=> (p = 0) \/ (n = m) 108 MULT_TO_DIV |- !m n. 0 < n ==> (n * m DIV n = m) 109 MULT_ASSOC_COMM |- !m n p. m * (n * p) = m * p * n 110 MULT_LEFT_ID |- !n. 0 < n ==> !m. (m * n = n) <=> (m = 1) 111 MULT_RIGHT_ID |- !n. 0 < n ==> !m. (n * m = n) <=> (m = 1) 112 MULT_EQ_SELF |- !n. 0 < n ==> !m. (n * m = n) <=> (m = 1) 113 SQ_EQ_SELF |- !n. (n * n = n) <=> (n = 0) \/ (n = 1) 114 EXP_EXP_BASE_LE |- !b c m n. m <= n /\ 0 < c ==> b ** c ** m <= b ** c ** n 115 EXP_EXP_LE_MONO_IMP|- !a b n. a <= b ==> a ** n <= b ** n 116 EXP_BY_ADD_SUB_LE |- !m n. m <= n ==> !p. p ** n = p ** m * p ** (n - m) 117 EXP_BY_ADD_SUB_LT |- !m n. m < n ==> !p. p ** n = p ** m * p ** (n - m) 118 EXP_SUC_DIV |- !m n. 0 < m ==> m ** SUC n DIV m = m ** n 119 SELF_LE_SQ |- !n. n <= n ** 2 120 LE_MONO_ADD2 |- !a b c d. a <= b /\ c <= d ==> a + c <= b + d 121 LT_MONO_ADD2 |- !a b c d. a < b /\ c < d ==> a + c < b + d 122 LE_MONO_MULT2 |- !a b c d. a <= b /\ c <= d ==> a * c <= b * d 123 LT_MONO_MULT2 |- !a b c d. a < b /\ c < d ==> a * c < b * d 124 SUM_LE_PRODUCT |- !m n. 1 < m /\ 1 < n ==> m + n <= m * n 125 MULTIPLE_SUC_LE |- !n k. 0 < n ==> k * n + 1 <= (k + 1) * n 126 127 Simple Theorems: 128 ADD_EQ_2 |- !m n. 0 < m /\ 0 < n /\ (m + n = 2) ==> (m = 1) /\ (n = 1) 129 EVEN_0 |- EVEN 0 130 ODD_1 |- ODD 1 131 EVEN_2 |- EVEN 2 132 EVEN_SQ |- !n. EVEN (n ** 2) <=> EVEN n 133 ODD_SQ |- !n. ODD (n ** 2) <=> ODD n 134 EQ_PARITY |- !a b. EVEN (2 * a + b) <=> EVEN b 135 ODD_MOD2 |- !x. ODD x <=> (x MOD 2 = 1) 136 EVEN_ODD_SUC |- !n. (EVEN n <=> ODD (SUC n)) /\ (ODD n <=> EVEN (SUC n)) 137 EVEN_ODD_PRE |- !n. 0 < n ==> (EVEN n <=> ODD (PRE n)) /\ (ODD n <=> EVEN (PRE n)) 138 EVEN_PARTNERS |- !n. EVEN (n * (n + 1)) 139 EVEN_HALF |- !n. EVEN n ==> (n = 2 * HALF n) 140 ODD_HALF |- !n. ODD n ==> (n = 2 * HALF n + 1) 141 EVEN_SUC_HALF |- !n. EVEN n ==> (HALF (SUC n) = HALF n) 142 ODD_SUC_HALF |- !n. ODD n ==> (HALF (SUC n) = SUC (HALF n)) 143 HALF_EQ_0 |- !n. (HALF n = 0) <=> (n = 0) \/ (n = 1) 144 HALF_EQ_SELF |- !n. (HALF n = n) <=> (n = 0) 145 HALF_LESS |- !n. 0 < n ==> HALF n < n 146 HALF_TWICE |- !n. HALF (TWICE n) = n 147 HALF_MULT |- !m n. n * HALF m <= HALF (n * m) 148 TWO_HALF_LESS_EQ |- !n. 2 * HALF n <= n /\ n <= SUC (2 * HALF n) 149 TWO_HALF_TIMES_LE |- !m n. TWICE (HALF n * m) <= n * m 150 SUC_HALF_LE |- !n. 0 < n ==> 1 + HALF n <= n 151 HALF_SQ_LE |- !n. HALF n ** 2 <= n ** 2 DIV 4 152 HALF_LE |- !n. HALF n <= n 153 HALF_LE_MONO |- !x y. x <= y ==> HALF x <= HALF y 154 MULT_EVEN |- !n. EVEN n ==> !m. m * n = TWICE m * HALF n 155 MULT_ODD |- !n. ODD n ==> !m. m * n = m + TWICE m * HALF n 156 EVEN_MOD_EVEN |- !m. EVEN m /\ m <> 0 ==> !n. EVEN n <=> EVEN (n MOD m) 157 EVEN_MOD_ODD |- !m. EVEN m /\ m <> 0 ==> !n. ODD n <=> ODD (n MOD m) 158 159 SUB_SUB_SUB |- !a b c. c <= a ==> (a - b - (a - c) = c - b) 160 ADD_SUB_SUB |- !a b c. c <= a ==> (a + b - (a - c) = c + b) 161 SUB_EQ_ADD |- !p. 0 < p ==> !m n. (m - n = p) <=> (m = n + p) 162 MULT_EQ_LESS_TO_MORE |- !a b c d. 0 < a /\ 0 < b /\ a < c /\ (a * b = c * d) ==> d < b 163 LE_IMP_REVERSE_LT |- !a b c d. 0 < c /\ 0 < d /\ a * b <= c * d /\ d < b ==> a < c 164 165 Exponential Theorems: 166 EXP_0 |- !n. n ** 0 = 1 167 EXP_2 |- !n. n ** 2 = n * n 168 EXP_NONZERO |- !m n. m <> 0 ==> m ** n <> 0 169 EXP_POS |- !m n. 0 < m ==> 0 < m ** n 170 EXP_EQ_SELF |- !n m. 0 < m ==> (n ** m = n) <=> (m = 1) \/ (n = 0) \/ (n = 1) 171 EXP_LE |- !n b. 0 < n ==> b <= b ** n 172 EXP_LT |- !n b. 1 < b /\ 1 < n ==> b < b ** n 173 EXP_LCANCEL |- !a b c n m. 0 < a /\ n < m /\ (a ** n * b = a ** m * c) ==> ?d. 0 < d /\ (b = a ** d * c) 174 EXP_RCANCEL |- !a b c n m. 0 < a /\ n < m /\ (b * a ** n = c * a ** m) ==> ?d. 0 < d /\ (b = c * a ** d) 175 ONE_LE_EXP |- !m n. 0 < m ==> 1 <= m ** n 176 EXP_EVEN |- !n. EVEN n ==> !m. m ** n = SQ m ** HALF n 177 EXP_ODD |- !n. ODD n ==> !m. m ** n = m * SQ m ** HALF n 178 EXP_THM |- !m n. m ** n = 179 if n = 0 then 1 else if n = 1 then m 180 else if EVEN n then SQ m ** HALF n 181 else m * SQ m ** HALF n 182 EXP_EQN |- !m n. m ** n = 183 if n = 0 then 1 184 else if EVEN n then SQ m ** HALF n 185 else m * SQ m ** HALF n 186 EXP_EQN_ALT |- !m n. m ** n = 187 if n = 0 then 1 else (if EVEN n then 1 else m) * SQ m ** HALF n 188 EXP_ALT_EQN |- !m n. m ** n = 189 if n = 0 then 1 else (if EVEN n then 1 else m) * (m ** 2) ** HALF n 190 EXP_MOD_EQN |- !b n m. 1 < m ==> 191 (b ** n MOD m = 192 if n = 0 then 1 193 else (let result = SQ b ** HALF n MOD m 194 in if EVEN n then result else (b * result) MOD m)) 195 EXP_MOD_ALT |- !b n m. 1 < m ==> 196 (b ** n MOD m = 197 if n = 0 then 1 198 else ((if EVEN n then 1 else b) * SQ b ** HALF n MOD m) MOD m) 199 EXP_EXP_SUC |- !x y n. x ** y ** SUC n = (x ** y) ** y ** n 200 EXP_LOWER_LE_LOW |- !n m. 1 + n * m <= (1 + m) ** n 201 EXP_LOWER_LT_LOW |- !n m. 0 < m /\ 1 < n ==> 1 + n * m < (1 + m) ** n 202 EXP_LOWER_LE_HIGH |- !n m. n * m ** (n - 1) + m ** n <= (1 + m) ** n 203 SUC_X_LT_2_EXP_X |- !n. 1 < n ==> SUC n < 2 ** n 204 205 DIVIDES Theorems: 206 DIV_EQ_0 |- !m n. 0 < n ==> ((m DIV n = 0) <=> m < n) 207 DIV_POS |- !m n. 0 < n /\ m divides n ==> 0 < n DIV m 208 DIV_LE |- !x y z. 0 < y /\ x <= y * z ==> x DIV y <= z 209 DIV_SOLVE |- !n. 0 < n ==> !x y. (x * n = y) ==> (x = y DIV n) 210 DIV_SOLVE_COMM |- !n. 0 < n ==> !x y. (n * x = y) ==> (x = y DIV n) 211 ONE_DIV |- !n. 1 < n ==> (1 DIV n = 0) 212 DIVIDES_ODD |- !n. ODD n ==> !m. m divides n ==> ODD m 213 DIVIDES_EVEN |- !m. EVEN m ==> !n. m divides n ==> EVEN n 214 DIVIDES_MOD_0 |- !n. 0 < n ==> !m. n divides m <=> (m MOD n = 0) 215 EVEN_ALT |- !n. EVEN n <=> 2 divides n 216 ODD_ALT |- !n. ODD n <=> ~(2 divides n) 217 218 DIV_MULT_LE |- !n. 0 < n ==> !q. q DIV n * n <= q 219 DIV_MULT_EQ |- !n. 0 < n ==> !q. n divides q <=> (q DIV n * n = q) 220 DIV_MULT_LESS_EQ |- !m n. 0 < m ==> m * (n DIV m) <= n /\ n < m * SUC (n DIV m) 221 DIV_LE_MONOTONE_REVERSE |- !x y. 0 < x /\ 0 < y /\ x <= y ==> !n. n DIV y <= n DIV x 222 DIVIDES_EQN |- !n. 0 < n ==> !m. n divides m <=> (m = m DIV n * n) 223 DIVIDES_EQN_COMM |- !n. 0 < n ==> !m. n divides m <=> (m = n * (m DIV n)) 224 SUB_DIV |- !m n. 0 < n /\ n <= m ==> ((m - n) DIV n = m DIV n - 1) 225 SUB_DIV_EQN |- !m n. 0 < n ==> ((m - n) DIV n = if m < n then 0 else m DIV n - 1) 226 SUB_MOD_EQN |- !m n. 0 < n ==> ((m - n) MOD n = if m < n then 0 else m MOD n) 227 DIV_EQ_MULT |- !n. 0 < n ==> !k m. (m MOD n = 0) ==> ((k * n = m) <=> (k = m DIV n)) 228 MULT_LT_DIV |- !n. 0 < n ==> !k m. (m MOD n = 0) ==> (k * n < m <=> k < m DIV n) 229 LE_MULT_LE_DIV |- !n. 0 < n ==> !k m. (m MOD n = 0) ==> (m <= n * k <=> m DIV n <= k) 230 DIV_MOD_EQ_0 |- !m n. 0 < m ==> (n DIV m = 0 /\ n MOD m = 0 <=> n = 0) 231 DIV_LT_SUC |- !m n. 0 < m /\ 0 < n /\ n MOD m = 0 ==> n DIV SUC m < n DIV m 232 DIV_LT_MONOTONE_REVERSE |- !x y. 0 < x /\ 0 < y /\ x < y ==> 233 !n. 0 < n /\ n MOD x = 0 ==> n DIV y < n DIV x 234 235 EXP_DIVIDES |- !a b n. 0 < n /\ a ** n divides b ==> a divides b 236 DIVIDES_EXP_BASE |- !a b n. prime a /\ 0 < n ==> (a divides b <=> a divides (b ** n)) 237 DIVIDES_MULTIPLE |- !m n. n divides m ==> !k. n divides (k * m) 238 DIVIDES_MULTIPLE_IFF |- !m n k. k <> 0 ==> (m divides n <=> k * m divides k * n) 239 DIVIDES_FACTORS |- !m n. 0 < n /\ n divides m ==> (m = n * (m DIV n)) 240 DIVIDES_COFACTOR |- !m n. 0 < n /\ n divides m ==> (m DIV n) divides m 241 MULTIPLY_DIV |- !n p q. 0 < n /\ n divides q ==> (p * (q DIV n) = p * q DIV n) 242 DIVIDES_MOD_MOD |- !m n. 0 < n /\ m divides n ==> !x. x MOD n MOD m = x MOD m 243 DIVIDES_CANCEL |- !k. 0 < k ==> !m n. m divides n <=> (m * k) divides (n * k) 244 DIVIDES_CANCEL_COMM |- !a b k. a divides b ==> (k * a) divides (k * b) 245 DIV_COMMON_FACTOR |- !m n. 0 < n /\ 0 < m ==> !x. n divides x ==> (m * x DIV (m * n) = x DIV n) 246 DIV_DIV_MULT |- !m n x. 0 < n /\ 0 < m /\ 0 < m DIV n /\ n divides m /\ m divides x /\ 247 (m DIV n) divides x ==> (x DIV (m DIV n) = n * (x DIV m)) 248 249 Basic Divisibility: 250 dividend_divides_divisor_multiple |- !m n. 0 < m /\ n divides m ==> 251 !t. m divides t * n <=> m DIV n divides t 252 divisor_pos |- !m n. 0 < n /\ m divides n ==> 0 < m 253 divides_pos |- !m n. 0 < n /\ m divides n ==> 0 < m /\ m <= n 254 divide_by_cofactor |- !m n. 0 < n /\ m divides n ==> (n DIV (n DIV m) = m) 255 divides_exp |- !n. 0 < n ==> !a b. a divides b ==> a divides b ** n 256 divides_linear |- !a b c. c divides a /\ c divides b ==> !h k. c divides h * a + k * b 257 divides_linear_sub |- !a b c. c divides a /\ c divides b ==> 258 !h k d. (h * a = k * b + d) ==> c divides d 259 power_divides_iff |- !p. 1 < p ==> !m n. p ** m divides p ** n <=> m <= n 260 prime_power_divides_iff |- !p. prime p ==> !m n. p ** m divides p ** n <=> m <= n 261 divides_self_power |- !n p. 0 < n /\ 1 < p ==> p divides p ** n 262 divides_eq_thm |- !a b. a divides b /\ 0 < b /\ b < 2 * a ==> (b = a) 263 factor_eq_cofactor |- !m n. 0 < m /\ m divides n ==> (m = n DIV m <=> n = m ** 2) 264 euclid_prime |- !p a b. prime p /\ p divides a * b ==> p divides a \/ p divides b 265 euclid_coprime |- !a b c. (gcd a b = 1) /\ b divides a * c ==> b divides c 266 267 Modulo Theorems: 268 MOD_EQN |- !n. 0 < n ==> !a b. (a MOD n = b) <=> ?c. (a = c * n + b) /\ b < n 269 MOD_PLUS3 |- !n. 0 < n ==> !x y z. (x + y + z) MOD n = (x MOD n + y MOD n + z MOD n) MOD n 270 MOD_ADD_ASSOC |- !n x y z. 0 < n /\ x < n /\ y < n /\ z < n ==> 271 (((x + y) MOD n + z) MOD n = (x + (y + z) MOD n) MOD n) 272 MOD_MULT_ASSOC |- !n x y z. 0 < n /\ x < n /\ y < n /\ z < n ==> 273 (((x * y) MOD n * z) MOD n = (x * (y * z) MOD n) MOD n) 274 MOD_ADD_INV |- !n x. 0 < n /\ x < n ==> (((n - x) MOD n + x) MOD n = 0) 275 MOD_MULITPLE_ZERO |- !n k. 0 < n /\ (k MOD n = 0) ==> !x. (k * x) MOD n = 0 276 MOD_EQ_DIFF |- !n a b. 0 < n /\ (a MOD n = b MOD n) ==> ((a - b) MOD n = 0) 277 MOD_EQ |- !n a b. 0 < n /\ b <= a ==> (((a - b) MOD n = 0) <=> (a MOD n = b MOD n)) 278 MOD_EQ_0_IFF |- !m n. n < m ==> ((n MOD m = 0) <=> (n = 0)) 279 MOD_EXP |- !n. 0 < n ==> !a m. (a MOD n) ** m MOD n = a ** m MOD n 280 ODD_EXP |- !m n. 0 < n /\ ODD m ==> ODD (m ** n) 281 power_parity |- !n. 0 < n ==> !m. (EVEN m <=> EVEN (m ** n)) /\ (ODD m <=> ODD (m ** n)) 282 EXP_2_EVEN |- !n. 0 < n ==> EVEN (2 ** n) 283 EXP_2_PRE_ODD |- !n. 0 < n ==> ODD (2 ** n - 1) 284 285 Modulo Inverse: 286 GCD_LINEAR |- !j k. 0 < j ==> ?p q. p * j = q * k + gcd j k 287 EUCLID_LEMMA |- !p x y. prime p ==> (((x * y) MOD p = 0) <=> (x MOD p = 0) \/ (y MOD p = 0)) 288 MOD_MULT_LCANCEL |- !p x y z. prime p /\ (x * y) MOD p = (x * z) MOD p /\ x MOD p <> 0 ==> 289 y MOD p = z MOD p 290 MOD_MULT_RCANCEL |- !p x y z. prime p /\ (y * x) MOD p = (z * x) MOD p /\ x MOD p <> 0 ==> 291 y MOD p = z MOD p 292 MOD_MULT_INV_EXISTS |- !p x. prime p /\ 0 < x /\ x < p ==> ?y. 0 < y /\ y < p /\ ((y * x) MOD p = 1) 293 MOD_MULT_INV_DEF |- !p x. prime p /\ 0 < x /\ x < p ==> 294 0 < MOD_MULT_INV p x /\ MOD_MULT_INV p x < p /\ ((MOD_MULT_INV p x * x) MOD p = 1) 295 296 FACTOR Theorems: 297 PRIME_FACTOR_PROPER |- !n. 1 < n /\ ~prime n ==> ?p. prime p /\ p < n /\ (p divides n) 298 FACTOR_OUT_POWER |- !n p. 0 < n /\ 1 < p /\ p divides n ==> 299 ?m. (p ** m) divides n /\ ~(p divides (n DIV p ** m)) 300 301 Useful Theorems: 302 binomial_add |- !a b. (a + b) ** 2 = a ** 2 + b ** 2 + 2 * a * b 303 binomial_sub |- !a b. b <= a ==> ((a - b) ** 2 = a ** 2 + b ** 2 - 2 * a * b) 304 binomial_means |- !a b. 2 * a * b <= a ** 2 + b ** 2 305 binomial_sub_add |- !a b. b <= a ==> ((a - b) ** 2 + 4 * a * b = (a + b) ** 2) 306 difference_of_squares|- !a b. a ** 2 - b ** 2 = (a - b) * (a + b) 307 difference_of_squares_alt 308 |- !a b. a * a - b * b = (a - b) * (a + b) 309 binomial_2 |- !m n. (m + n) ** 2 = m ** 2 + n ** 2 + TWICE m * n 310 SUC_SQ |- !n. SUC n ** 2 = SUC (n ** 2) + TWICE n 311 SQ_LE |- !m n. m <= n ==> SQ m <= SQ n 312 EVEN_PRIME |- !n. EVEN n /\ prime n ==> (n = 2) 313 ODD_PRIME |- !n. prime n /\ n <> 2 ==> ODD n 314 TWO_LE_PRIME |- !p. prime p ==> 2 <= p 315 NOT_PRIME_4 |- ~prime 4 316 prime_divides_prime |- !n m. prime n /\ prime m ==> (n divides m <=> (n = m)) 317 ALL_PRIME_FACTORS_MOD_EQ_1 |- !m n. 0 < m /\ 1 < n /\ 318 (!p. prime p /\ p divides m ==> (p MOD n = 1)) ==> (m MOD n = 1) 319 prime_divides_power |- !p n. prime p /\ 0 < n ==> !b. p divides b ** n <=> p divides b 320 prime_divides_self_power |- !p. prime p ==> !n. 0 < n ==> p divides p ** n 321 power_eq_prime_power |- !p. prime p ==> !b n m. 0 < m /\ (b ** n = p ** m) ==> 322 ?k. (b = p ** k) /\ (k * n = m) 323 POWER_EQ_SELF |- !n. 1 < n ==> !m. (n ** m = n) <=> (m = 1) 324 325 LESS_HALF_IFF |- !n k. k < HALF n <=> k + 1 < n - k 326 MORE_HALF_IMP |- !n k. HALF n < k ==> n - k <= HALF n 327 MONOTONE_MAX |- !f m. (!k. k < m ==> f k < f (k + 1)) ==> !k. k < m ==> f k < f m 328 MULTIPLE_INTERVAL |- !n m. n divides m ==> !x. m - n < x /\ x < m + n /\ n divides x ==> (x = m) 329 MOD_SUC_EQN |- !m n. 0 < m ==> (SUC (n MOD m) = SUC n MOD m + (SUC n DIV m - n DIV m) * m) 330 ONE_LT_HALF_SQ |- !n. 1 < n ==> 1 < HALF (n ** 2) 331 EXP_2_HALF |- !n. 0 < n ==> (HALF (2 ** n) = 2 ** (n - 1)) 332 HALF_MULT_EVEN |- !m n. EVEN n ==> (HALF (m * n) = m * HALF n) 333 MULT_LESS_IMP_LESS |- !m n k. 0 < k /\ k * m < n ==> m < n 334 HALF_EXP_5 |- !n. n * HALF (SQ n ** 2) <= HALF (n ** 5) 335 LE_TWICE_ALT |- !m n. n <= TWICE m <=> n <> 0 ==> HALF (n - 1) < m 336 HALF_DIV_TWO_POWER |- !m n. HALF n DIV 2 ** m = n DIV 2 ** SUC m 337 fit_for_100 |- 1 * 2 + 3 * 4 + 5 * 6 + 7 * 8 = 100 338*) 339 340(* ------------------------------------------------------------------------- *) 341(* Arithmetic Theorems *) 342(* ------------------------------------------------------------------------- *) 343 344(* Theorem: 3 = SUC 2 *) 345(* Proof: by arithmetic *) 346val THREE = store_thm( 347 "THREE", 348 ``3 = SUC 2``, 349 decide_tac); 350 351(* Theorem: 4 = SUC 3 *) 352(* Proof: by arithmetic *) 353val FOUR = store_thm( 354 "FOUR", 355 ``4 = SUC 3``, 356 decide_tac); 357 358(* Theorem: 5 = SUC 4 *) 359(* Proof: by arithmetic *) 360val FIVE = store_thm( 361 "FIVE", 362 ``5 = SUC 4``, 363 decide_tac); 364 365(* Overload squaring *) 366val _ = overload_on("SQ", ``\n. n * n``); (* not n ** 2 *) 367 368(* Overload half of a number *) 369val _ = overload_on("HALF", ``\n. n DIV 2``); 370 371(* Overload twice of a number *) 372val _ = overload_on("TWICE", ``\n. 2 * n``); 373 374(* make divides infix *) 375val _ = set_fixity "divides" (Infixl 480); (* relation is 450, +/- is 500, * is 600. *) 376 377(* Theorem alias *) 378val ZERO_LE_ALL = save_thm("ZERO_LE_ALL", ZERO_LESS_EQ); 379(* val ZERO_LE_ALL = |- !n. 0 <= n: thm *) 380 381(* Theorem alias *) 382val NOT_ZERO = save_thm("NOT_ZERO", NOT_ZERO_LT_ZERO); 383 384(* Theorem: !n. 1 < n ==> 0 < n *) 385(* Proof: by arithmetic. *) 386val ONE_LT_POS = store_thm( 387 "ONE_LT_POS", 388 ``!n. 1 < n ==> 0 < n``, 389 decide_tac); 390 391(* Theorem: !n. 1 < n ==> n <> 0 *) 392(* Proof: by arithmetic. *) 393val ONE_LT_NONZERO = store_thm( 394 "ONE_LT_NONZERO", 395 ``!n. 1 < n ==> n <> 0``, 396 decide_tac); 397 398(* Theorem: ~(1 < n) <=> (n = 0) \/ (n = 1) *) 399(* Proof: by arithmetic. *) 400val NOT_LT_ONE = store_thm( 401 "NOT_LT_ONE", 402 ``!n. ~(1 < n) <=> (n = 0) \/ (n = 1)``, 403 decide_tac); 404 405(* Theorem: n <> 0 <=> 1 <= n *) 406(* Proof: by arithmetic. *) 407val NOT_ZERO_GE_ONE = store_thm( 408 "NOT_ZERO_GE_ONE", 409 ``!n. n <> 0 <=> 1 <= n``, 410 decide_tac); 411 412(* Theorem: 1 <= n <=> n <> 0 *) 413(* Proof: by arithmetic *) 414val ONE_LE_NONZERO = store_thm( 415 "ONE_LE_NONZERO", 416 ``!n. 1 <= n <=> n <> 0``, 417 decide_tac); 418(* This is the reverse of: NOT_ZERO_GE_ONE *) 419 420(* Theorem: n <= 1 <=> (n = 0) \/ (n = 1) *) 421(* Proof: by arithmetic *) 422val LE_ONE = store_thm( 423 "LE_ONE", 424 ``!n. n <= 1 <=> (n = 0) \/ (n = 1)``, 425 decide_tac); 426 427(* Theorem: n < 1 <=> (n = 0) *) 428(* Proof: by arithmetic *) 429val LT_ONE = store_thm( 430 "LT_ONE", 431 ``!n. n < 1 <=> (n = 0)``, 432 decide_tac); 433 434(* Theorem: n < 2 <=> (n = 0) \/ (n = 1) *) 435(* Proof: by arithmetic *) 436val LT_TWO = store_thm( 437 "LT_TWO", 438 ``!n. n < 2 <=> (n = 0) \/ (n = 1)``, 439 decide_tac); 440 441(* Theorem: m < 2 * n ==> m - n < n *) 442(* Proof: by arithmetic *) 443val LESS_TWICE = store_thm( 444 "LESS_TWICE", 445 ``!m n. m < 2 * n ==> m - n < n``, 446 decide_tac); 447 448(* Theorem: m < n ==> m <> n *) 449(* Proof: by arithmetic. *) 450val LESS_NOT_EQ = store_thm( 451 "LESS_NOT_EQ", 452 ``!m n. m < n ==> m <> n``, 453 decide_tac); 454 455(* Theorem alias *) 456val LESS_SELF = save_thm("LESS_SELF", prim_recTheory.LESS_REFL); 457(* val LESS_SELF = |- !n. ~(n < n): thm *) 458 459(* arithmeticTheory.LESS_EQ_SUC_REFL |- !m. m <= SUC m *) 460(* Theorem: n < SUC n *) 461(* Proof: by arithmetic. *) 462val LESS_SUC = store_thm( 463 "LESS_SUC", 464 ``!n. n < SUC n``, 465 decide_tac); 466 467(* Theorem: 0 < n ==> PRE n < n *) 468(* Proof: by arithmetic. *) 469val PRE_LESS = store_thm( 470 "PRE_LESS", 471 ``!n. 0 < n ==> PRE n < n``, 472 decide_tac); 473 474(* Theorem: 0 < n ==> ?m. n = SUC m *) 475(* Proof: by NOT_ZERO_LT_ZERO. *) 476val LESS_EQ_SUC = store_thm( 477 "LESS_EQ_SUC", 478 ``!n. 0 < n ==> ?m. n = SUC m``, 479 metis_tac[NOT_ZERO_LT_ZERO, num_CASES]); 480 481(* prim_recTheory.LESS_0 |- !n. 0 < SUC n *) 482(* Theorem: 0 < SUC n *) 483(* Proof: by arithmetic. *) 484val SUC_POS = store_thm( 485 "SUC_POS", 486 ``!n. 0 < SUC n``, 487 decide_tac); 488 489(* numTheory.NOT_SUC |- !n. SUC n <> 0 *) 490(* Theorem: 0 < SUC n *) 491(* Proof: by arithmetic. *) 492val SUC_NOT_ZERO = store_thm( 493 "SUC_NOT_ZERO", 494 ``!n. SUC n <> 0``, 495 decide_tac); 496 497(* Theorem: 1 <> 0 *) 498(* Proof: by ONE, SUC_ID *) 499val ONE_NOT_ZERO = store_thm( 500 "ONE_NOT_ZERO", 501 ``1 <> 0``, 502 decide_tac); 503 504(* Theorem: (SUC m) + (SUC n) = m + n + 2 *) 505(* Proof: 506 (SUC m) + (SUC n) 507 = (m + 1) + (n + 1) by ADD1 508 = m + n + 2 by arithmetic 509*) 510val SUC_ADD_SUC = store_thm( 511 "SUC_ADD_SUC", 512 ``!m n. (SUC m) + (SUC n) = m + n + 2``, 513 decide_tac); 514 515(* Theorem: (SUC m) * (SUC n) = m * n + m + n + 1 *) 516(* Proof: 517 (SUC m) * (SUC n) 518 = SUC m + (SUC m) * n by MULT_SUC 519 = SUC m + n * (SUC m) by MULT_COMM 520 = SUC m + (n + n * m) by MULT_SUC 521 = m * n + m + n + 1 by arithmetic 522*) 523val SUC_MULT_SUC = store_thm( 524 "SUC_MULT_SUC", 525 ``!m n. (SUC m) * (SUC n) = m * n + m + n + 1``, 526 rw[MULT_SUC]); 527 528(* Theorem: (SUC m = SUC n) <=> (m = n) *) 529(* Proof: by prim_recTheory.INV_SUC_EQ *) 530val SUC_EQ = store_thm( 531 "SUC_EQ", 532 ``!m n. (SUC m = SUC n) <=> (m = n)``, 533 rw[]); 534 535(* Theorem: (TWICE n = 0) <=> (n = 0) *) 536(* Proof: MULT_EQ_0 *) 537val TWICE_EQ_0 = store_thm( 538 "TWICE_EQ_0", 539 ``!n. (TWICE n = 0) <=> (n = 0)``, 540 rw[]); 541 542(* Theorem: (SQ n = 0) <=> (n = 0) *) 543(* Proof: MULT_EQ_0 *) 544val SQ_EQ_0 = store_thm( 545 "SQ_EQ_0", 546 ``!n. (SQ n = 0) <=> (n = 0)``, 547 rw[]); 548 549(* Theorem: (SQ n = 1) <=> (n = 1) *) 550(* Proof: MULT_EQ_1 *) 551val SQ_EQ_1 = store_thm( 552 "SQ_EQ_1", 553 ``!n. (SQ n = 1) <=> (n = 1)``, 554 rw[]); 555 556(* Theorem: (x * y * z = 0) <=> ((x = 0) \/ (y = 0) \/ (z = 0)) *) 557(* Proof: by MULT_EQ_0 *) 558val MULT3_EQ_0 = store_thm( 559 "MULT3_EQ_0", 560 ``!x y z. (x * y * z = 0) <=> ((x = 0) \/ (y = 0) \/ (z = 0))``, 561 metis_tac[MULT_EQ_0]); 562 563(* Theorem: (x * y * z = 1) <=> ((x = 1) /\ (y = 1) /\ (z = 1)) *) 564(* Proof: by MULT_EQ_1 *) 565val MULT3_EQ_1 = store_thm( 566 "MULT3_EQ_1", 567 ``!x y z. (x * y * z = 1) <=> ((x = 1) /\ (y = 1) /\ (z = 1))``, 568 metis_tac[MULT_EQ_1]); 569 570(* Theorem: 0 ** 2 = 0 *) 571(* Proof: by ZERO_EXP *) 572Theorem SQ_0: 573 0 ** 2 = 0 574Proof 575 simp[] 576QED 577 578(* Theorem: (n ** 2 = 0) <=> (n = 0) *) 579(* Proof: by EXP_2, MULT_EQ_0 *) 580Theorem EXP_2_EQ_0: 581 !n. (n ** 2 = 0) <=> (n = 0) 582Proof 583 simp[] 584QED 585 586(* ------------------------------------------------------------------------- *) 587(* Maximum and minimum *) 588(* ------------------------------------------------------------------------- *) 589 590(* Theorem: MAX m n = if m <= n then n else m *) 591(* Proof: by MAX_DEF *) 592val MAX_ALT = store_thm( 593 "MAX_ALT", 594 ``!m n. MAX m n = if m <= n then n else m``, 595 rw[MAX_DEF]); 596 597(* Theorem: MIN m n = if m <= n then m else n *) 598(* Proof: by MIN_DEF *) 599val MIN_ALT = store_thm( 600 "MIN_ALT", 601 ``!m n. MIN m n = if m <= n then m else n``, 602 rw[MIN_DEF]); 603 604(* Theorem: (!x y. x <= y ==> f x <= f y) ==> !x y. f (MAX x y) = MAX (f x) (f y) *) 605(* Proof: by MAX_DEF *) 606val MAX_SWAP = store_thm( 607 "MAX_SWAP", 608 ``!f. (!x y. x <= y ==> f x <= f y) ==> !x y. f (MAX x y) = MAX (f x) (f y)``, 609 rw[MAX_DEF] >> 610 Cases_on `x < y` >| [ 611 `f x <= f y` by rw[] >> 612 Cases_on `f x = f y` >- 613 rw[] >> 614 rw[], 615 `y <= x` by decide_tac >> 616 `f y <= f x` by rw[] >> 617 rw[] 618 ]); 619 620(* Theorem: (!x y. x <= y ==> f x <= f y) ==> !x y. f (MIN x y) = MIN (f x) (f y) *) 621(* Proof: by MIN_DEF *) 622val MIN_SWAP = store_thm( 623 "MIN_SWAP", 624 ``!f. (!x y. x <= y ==> f x <= f y) ==> !x y. f (MIN x y) = MIN (f x) (f y)``, 625 rw[MIN_DEF] >> 626 Cases_on `x < y` >| [ 627 `f x <= f y` by rw[] >> 628 Cases_on `f x = f y` >- 629 rw[] >> 630 rw[], 631 `y <= x` by decide_tac >> 632 `f y <= f x` by rw[] >> 633 rw[] 634 ]); 635 636(* Theorem: SUC (MAX m n) = MAX (SUC m) (SUC n) *) 637(* Proof: 638 If m < n, then SUC m < SUC n by LESS_MONO_EQ 639 hence true by MAX_DEF. 640 If m = n, then true by MAX_IDEM. 641 If n < m, true by MAX_COMM of the case m < n. 642*) 643val SUC_MAX = store_thm( 644 "SUC_MAX", 645 ``!m n. SUC (MAX m n) = MAX (SUC m) (SUC n)``, 646 rw[MAX_DEF]); 647 648(* Theorem: SUC (MIN m n) = MIN (SUC m) (SUC n) *) 649(* Proof: by MIN_DEF *) 650val SUC_MIN = store_thm( 651 "SUC_MIN", 652 ``!m n. SUC (MIN m n) = MIN (SUC m) (SUC n)``, 653 rw[MIN_DEF]); 654 655(* Reverse theorems *) 656val MAX_SUC = save_thm("MAX_SUC", GSYM SUC_MAX); 657(* val MAX_SUC = |- !m n. MAX (SUC m) (SUC n) = SUC (MAX m n): thm *) 658val MIN_SUC = save_thm("MIN_SUC", GSYM SUC_MIN); 659(* val MIN_SUC = |- !m n. MIN (SUC m) (SUC n) = SUC (MIN m n): thm *) 660 661(* Theorem: x < n /\ y < n ==> MAX x y < n *) 662(* Proof: 663 MAX x y 664 = if x < y then y else x by MAX_DEF 665 = either x or y 666 < n for either case 667*) 668val MAX_LESS = store_thm( 669 "MAX_LESS", 670 ``!x y n. x < n /\ y < n ==> MAX x y < n``, 671 rw[]); 672 673(* Theorem: (MAX n m = n) \/ (MAX n m = m) *) 674(* Proof: by MAX_DEF *) 675val MAX_CASES = store_thm( 676 "MAX_CASES", 677 ``!m n. (MAX n m = n) \/ (MAX n m = m)``, 678 rw[MAX_DEF]); 679 680(* Theorem: (MIN n m = n) \/ (MIN n m = m) *) 681(* Proof: by MIN_DEF *) 682val MIN_CASES = store_thm( 683 "MIN_CASES", 684 ``!m n. (MIN n m = n) \/ (MIN n m = m)``, 685 rw[MIN_DEF]); 686 687(* Theorem: (MAX n m = 0) <=> ((n = 0) /\ (m = 0)) *) 688(* Proof: 689 If part: MAX n m = 0 ==> n = 0 /\ m = 0 690 If n < m, 0 = MAX n m = m, hence m = 0 by MAX_DEF 691 but n < 0 is F by NOT_LESS_0 692 If ~(n < m), 0 = MAX n m = n, hence n = 0 by MAX_DEF 693 and ~(0 < m) ==> m = 0 by NOT_LESS 694 Only-if part: n = 0 /\ m = 0 ==> MAX n m = 0 695 True since MAX 0 0 = 0 by MAX_0 696*) 697val MAX_EQ_0 = store_thm( 698 "MAX_EQ_0", 699 ``!m n. (MAX n m = 0) <=> ((n = 0) /\ (m = 0))``, 700 rw[MAX_DEF]); 701 702(* Theorem: (MIN n m = 0) <=> ((n = 0) \/ (m = 0)) *) 703(* Proof: 704 If part: MIN n m = 0 ==> n = 0 \/ m = 0 705 If n < m, 0 = MIN n m = n, hence n = 0 by MIN_DEF 706 If ~(n < m), 0 = MAX n m = m, hence m = 0 by MIN_DEF 707 Only-if part: n = 0 \/ m = 0 ==> MIN n m = 0 708 True since MIN 0 0 = 0 by MIN_0 709*) 710val MIN_EQ_0 = store_thm( 711 "MIN_EQ_0", 712 ``!m n. (MIN n m = 0) <=> ((n = 0) \/ (m = 0))``, 713 rw[MIN_DEF]); 714 715(* Theorem: m <= MAX m n /\ n <= MAX m n *) 716(* Proof: by MAX_DEF *) 717val MAX_IS_MAX = store_thm( 718 "MAX_IS_MAX", 719 ``!m n. m <= MAX m n /\ n <= MAX m n``, 720 rw_tac std_ss[MAX_DEF]); 721 722(* Theorem: MIN m n <= m /\ MIN m n <= n *) 723(* Proof: by MIN_DEF *) 724val MIN_IS_MIN = store_thm( 725 "MIN_IS_MIN", 726 ``!m n. MIN m n <= m /\ MIN m n <= n``, 727 rw_tac std_ss[MIN_DEF]); 728 729(* Theorem: (MAX (MAX m n) n = MAX m n) /\ (MAX m (MAX m n) = MAX m n) *) 730(* Proof: by MAX_DEF *) 731val MAX_ID = store_thm( 732 "MAX_ID", 733 ``!m n. (MAX (MAX m n) n = MAX m n) /\ (MAX m (MAX m n) = MAX m n)``, 734 rw[MAX_DEF]); 735 736(* Theorem: (MIN (MIN m n) n = MIN m n) /\ (MIN m (MIN m n) = MIN m n) *) 737(* Proof: by MIN_DEF *) 738val MIN_ID = store_thm( 739 "MIN_ID", 740 ``!m n. (MIN (MIN m n) n = MIN m n) /\ (MIN m (MIN m n) = MIN m n)``, 741 rw[MIN_DEF]); 742 743(* Theorem: a <= b /\ c <= d ==> MAX a c <= MAX b d *) 744(* Proof: by MAX_DEF *) 745val MAX_LE_PAIR = store_thm( 746 "MAX_LE_PAIR", 747 ``!a b c d. a <= b /\ c <= d ==> MAX a c <= MAX b d``, 748 rw[]); 749 750(* Theorem: a <= b /\ c <= d ==> MIN a c <= MIN b d *) 751(* Proof: by MIN_DEF *) 752val MIN_LE_PAIR = store_thm( 753 "MIN_LE_PAIR", 754 ``!a b c d. a <= b /\ c <= d ==> MIN a c <= MIN b d``, 755 rw[]); 756 757(* Theorem: MAX a (b + c) <= MAX a b + MAX a c *) 758(* Proof: by MAX_DEF *) 759val MAX_ADD = store_thm( 760 "MAX_ADD", 761 ``!a b c. MAX a (b + c) <= MAX a b + MAX a c``, 762 rw[MAX_DEF]); 763 764(* Theorem: MIN a (b + c) <= MIN a b + MIN a c *) 765(* Proof: by MIN_DEF *) 766val MIN_ADD = store_thm( 767 "MIN_ADD", 768 ``!a b c. MIN a (b + c) <= MIN a b + MIN a c``, 769 rw[MIN_DEF]); 770 771(* Theorem: 0 < n ==> (MAX 1 n = n) *) 772(* Proof: by MAX_DEF *) 773val MAX_1_POS = store_thm( 774 "MAX_1_POS", 775 ``!n. 0 < n ==> (MAX 1 n = n)``, 776 rw[MAX_DEF]); 777 778(* Theorem: 0 < n ==> (MIN 1 n = 1) *) 779(* Proof: by MIN_DEF *) 780val MIN_1_POS = store_thm( 781 "MIN_1_POS", 782 ``!n. 0 < n ==> (MIN 1 n = 1)``, 783 rw[MIN_DEF]); 784 785(* Theorem: MAX m n <= m + n *) 786(* Proof: 787 If m < n, MAX m n = n <= m + n by arithmetic 788 Otherwise, MAX m n = m <= m + n by arithmetic 789*) 790val MAX_LE_SUM = store_thm( 791 "MAX_LE_SUM", 792 ``!m n. MAX m n <= m + n``, 793 rw[MAX_DEF]); 794 795(* Theorem: MIN m n <= m + n *) 796(* Proof: 797 If m < n, MIN m n = m <= m + n by arithmetic 798 Otherwise, MIN m n = n <= m + n by arithmetic 799*) 800val MIN_LE_SUM = store_thm( 801 "MIN_LE_SUM", 802 ``!m n. MIN m n <= m + n``, 803 rw[MIN_DEF]); 804 805(* Theorem: MAX 1 (m ** n) = (MAX 1 m) ** n *) 806(* Proof: 807 If m = 0, 808 Then 0 ** n = 0 or 1 by ZERO_EXP 809 Thus MAX 1 (0 ** n) = 1 by MAX_DEF 810 and (MAX 1 0) ** n = 1 by MAX_DEF, EXP_1 811 If m <> 0, 812 Then 0 < m ** n by EXP_POS 813 so MAX 1 (m ** n) = m ** n by MAX_DEF 814 and (MAX 1 m) ** n = m ** n by MAX_DEF, 0 < m 815*) 816val MAX_1_EXP = store_thm( 817 "MAX_1_EXP", 818 ``!n m. MAX 1 (m ** n) = (MAX 1 m) ** n``, 819 rpt strip_tac >> 820 Cases_on `m = 0` >- 821 rw[ZERO_EXP, MAX_DEF] >> 822 `0 < m /\ 0 < m ** n` by rw[] >> 823 `MAX 1 (m ** n) = m ** n` by rw[MAX_DEF] >> 824 `MAX 1 m = m` by rw[MAX_DEF] >> 825 fs[]); 826 827(* Theorem: MIN 1 (m ** n) = (MIN 1 m) ** n *) 828(* Proof: 829 If m = 0, 830 Then 0 ** n = 0 or 1 by ZERO_EXP 831 Thus MIN 1 (0 ** n) = 0 when n <> 0 or 1 when n = 0 by MIN_DEF 832 and (MIN 1 0) ** n = 0 ** n by MIN_DEF 833 If m <> 0, 834 Then 0 < m ** n by EXP_POS 835 so MIN 1 (m ** n) = 1 ** n by MIN_DEF 836 and (MIN 1 m) ** n = 1 ** n by MIN_DEF, 0 < m 837*) 838val MIN_1_EXP = store_thm( 839 "MIN_1_EXP", 840 ``!n m. MIN 1 (m ** n) = (MIN 1 m) ** n``, 841 rpt strip_tac >> 842 Cases_on `m = 0` >- 843 rw[ZERO_EXP, MIN_DEF] >> 844 `0 < m ** n` by rw[] >> 845 `MIN 1 (m ** n) = 1` by rw[MIN_DEF] >> 846 `MIN 1 m = 1` by rw[MIN_DEF] >> 847 fs[]); 848 849(* ------------------------------------------------------------------------- *) 850(* Arithmetic Manipulations *) 851(* ------------------------------------------------------------------------- *) 852 853(* Rename theorem *) 854val MULT_POS = save_thm("MULT_POS", LESS_MULT2); 855(* val MULT_POS = |- !m n. 0 < m /\ 0 < n ==> 0 < m * n: thm *) 856 857(* Theorem: m * (n * p) = n * (m * p) *) 858(* Proof: 859 m * (n * p) 860 = (m * n) * p by MULT_ASSOC 861 = (n * m) * p by MULT_COMM 862 = n * (m * p) by MULT_ASSOC 863*) 864val MULT_COMM_ASSOC = store_thm( 865 "MULT_COMM_ASSOC", 866 ``!m n p. m * (n * p) = n * (m * p)``, 867 metis_tac[MULT_COMM, MULT_ASSOC]); 868 869(* The missing theorem in arithmeticTheory. Only has EQ_MULT_LCANCEL: 870 |- !m n p. (m * n = m * p) <=> (m = 0) \/ (n = p): thm 871*) 872(* Theorem: (n * m = p * m) <=> (m = 0) \/ (n = p) *) 873(* Proof: by EQ_MULT_LCANCEL, MULT_COMM *) 874val EQ_MULT_RCANCEL = store_thm( 875 "EQ_MULT_RCANCEL", 876 ``!m n p. (n * m = p * m) <=> (m = 0) \/ (n = p)``, 877 rw[EQ_MULT_LCANCEL, MULT_COMM]); 878 879(* Theorem: n * p = m * p <=> p = 0 \/ n = m *) 880(* Proof: 881 n * p = m * p 882 <=> n * p - m * p = 0 by SUB_EQUAL_0 883 <=> (n - m) * p = 0 by RIGHT_SUB_DISTRIB 884 <=> n - m = 0 or p = 0 by MULT_EQ_0 885 <=> n = m or p = 0 by SUB_EQUAL_0 886*) 887val MULT_RIGHT_CANCEL = store_thm( 888 "MULT_RIGHT_CANCEL", 889 ``!m n p. (n * p = m * p) <=> (p = 0) \/ (n = m)``, 890 rw[]); 891 892(* Theorem: p * n = p * m <=> p = 0 \/ n = m *) 893(* Proof: by MULT_RIGHT_CANCEL and MULT_COMM. *) 894val MULT_LEFT_CANCEL = store_thm( 895 "MULT_LEFT_CANCEL", 896 ``!m n p. (p * n = p * m) <=> (p = 0) \/ (n = m)``, 897 rw[MULT_RIGHT_CANCEL, MULT_COMM]); 898 899(* Theorem: 0 < n ==> ((n * m) DIV n = m) *) 900(* Proof: 901 Since n * m = m * n by MULT_COMM 902 = m * n + 0 by ADD_0 903 and 0 < n by given 904 Hence (n * m) DIV n = m by DIV_UNIQUE: 905 |- !n k q. (?r. (k = q * n + r) /\ r < n) ==> (k DIV n = q) 906*) 907val MULT_TO_DIV = store_thm( 908 "MULT_TO_DIV", 909 ``!m n. 0 < n ==> ((n * m) DIV n = m)``, 910 metis_tac[MULT_COMM, ADD_0, DIV_UNIQUE]); 911(* This is commutative version of: 912arithmeticTheory.MULT_DIV |- !n q. 0 < n ==> (q * n DIV n = q) 913*) 914 915(* Theorem: m * (n * p) = m * p * n *) 916(* Proof: by MULT_ASSOC, MULT_COMM *) 917val MULT_ASSOC_COMM = store_thm( 918 "MULT_ASSOC_COMM", 919 ``!m n p. m * (n * p) = m * p * n``, 920 metis_tac[MULT_ASSOC, MULT_COMM]); 921 922(* Theorem: 0 < n ==> !m. (m * n = n) <=> (m = 1) *) 923(* Proof: by MULT_EQ_ID *) 924val MULT_LEFT_ID = store_thm( 925 "MULT_LEFT_ID", 926 ``!n. 0 < n ==> !m. (m * n = n) <=> (m = 1)``, 927 metis_tac[MULT_EQ_ID, NOT_ZERO_LT_ZERO]); 928 929(* Theorem: 0 < n ==> !m. (n * m = n) <=> (m = 1) *) 930(* Proof: by MULT_EQ_ID *) 931val MULT_RIGHT_ID = store_thm( 932 "MULT_RIGHT_ID", 933 ``!n. 0 < n ==> !m. (n * m = n) <=> (m = 1)``, 934 metis_tac[MULT_EQ_ID, MULT_COMM, NOT_ZERO_LT_ZERO]); 935 936(* Theorem alias *) 937val MULT_EQ_SELF = save_thm("MULT_EQ_SELF", MULT_RIGHT_ID); 938(* val MULT_EQ_SELF = |- !n. 0 < n ==> !m. (n * m = n) <=> (m = 1): thm *) 939 940(* Theorem: (n * n = n) <=> ((n = 0) \/ (n = 1)) *) 941(* Proof: 942 If part: n * n = n ==> (n = 0) \/ (n = 1) 943 By contradiction, suppose n <> 0 /\ n <> 1. 944 Since n * n = n = n * 1 by MULT_RIGHT_1 945 then n = 1 by MULT_LEFT_CANCEL, n <> 0 946 This contradicts n <> 1. 947 Only-if part: (n = 0) \/ (n = 1) ==> n * n = n 948 That is, 0 * 0 = 0 by MULT 949 and 1 * 1 = 1 by MULT_RIGHT_1 950*) 951val SQ_EQ_SELF = store_thm( 952 "SQ_EQ_SELF", 953 ``!n. (n * n = n) <=> ((n = 0) \/ (n = 1))``, 954 rw_tac bool_ss[EQ_IMP_THM] >- 955 metis_tac[MULT_RIGHT_1, MULT_LEFT_CANCEL] >- 956 rw[] >> 957 rw[]); 958 959(* Theorem: m <= n /\ 0 < c ==> b ** c ** m <= b ** c ** n *) 960(* Proof: 961 If b = 0, 962 Note 0 < c ** m /\ 0 < c ** n by EXP_POS, by 0 < c 963 Thus 0 ** c ** m = 0 by ZERO_EXP 964 and 0 ** c ** n = 0 by ZERO_EXP 965 Hence true. 966 If b <> 0, 967 Then c ** m <= c ** n by EXP_BASE_LEQ_MONO_IMP, 0 < c 968 so b ** c ** m <= b ** c ** n by EXP_BASE_LEQ_MONO_IMP, 0 < b 969*) 970val EXP_EXP_BASE_LE = store_thm( 971 "EXP_EXP_BASE_LE", 972 ``!b c m n. m <= n /\ 0 < c ==> b ** c ** m <= b ** c ** n``, 973 rpt strip_tac >> 974 Cases_on `b = 0` >- 975 rw[ZERO_EXP] >> 976 rw[EXP_BASE_LEQ_MONO_IMP]); 977 978(* Theorem: a <= b ==> a ** n <= b ** n *) 979(* Proof: 980 Note a ** n <= b ** n by EXP_EXP_LE_MONO 981 Thus size (a ** n) <= size (b ** n) by size_monotone_le 982*) 983val EXP_EXP_LE_MONO_IMP = store_thm( 984 "EXP_EXP_LE_MONO_IMP", 985 ``!a b n. a <= b ==> a ** n <= b ** n``, 986 rw[]); 987 988(* Theorem: m <= n ==> !p. p ** n = p ** m * p ** (n - m) *) 989(* Proof: 990 Note n = (n - m) + m by m <= n 991 p ** n 992 = p ** (n - m) * p ** m by EXP_ADD 993 = p ** m * p ** (n - m) by MULT_COMM 994*) 995val EXP_BY_ADD_SUB_LE = store_thm( 996 "EXP_BY_ADD_SUB_LE", 997 ``!m n. m <= n ==> !p. p ** n = p ** m * p ** (n - m)``, 998 rpt strip_tac >> 999 `n = (n - m) + m` by decide_tac >> 1000 metis_tac[EXP_ADD, MULT_COMM]); 1001 1002(* Theorem: m < n ==> (p ** n = p ** m * p ** (n - m)) *) 1003(* Proof: by EXP_BY_ADD_SUB_LE, LESS_IMP_LESS_OR_EQ *) 1004val EXP_BY_ADD_SUB_LT = store_thm( 1005 "EXP_BY_ADD_SUB_LT", 1006 ``!m n. m < n ==> !p. p ** n = p ** m * p ** (n - m)``, 1007 rw[EXP_BY_ADD_SUB_LE]); 1008 1009(* Theorem: 0 < m ==> m ** (SUC n) DIV m = m ** n *) 1010(* Proof: 1011 m ** (SUC n) DIV m 1012 = (m * m ** n) DIV m by EXP 1013 = m ** n by MULT_TO_DIV, 0 < m 1014*) 1015val EXP_SUC_DIV = store_thm( 1016 "EXP_SUC_DIV", 1017 ``!m n. 0 < m ==> (m ** (SUC n) DIV m = m ** n)``, 1018 simp[EXP, MULT_TO_DIV]); 1019 1020(* Theorem: n <= n ** 2 *) 1021(* Proof: 1022 If n = 0, 1023 Then n ** 2 = 0 >= 0 by ZERO_EXP 1024 If n <> 0, then 0 < n by NOT_ZERO_LT_ZERO 1025 Hence n = n ** 1 by EXP_1 1026 <= n ** 2 by EXP_BASE_LEQ_MONO_IMP 1027*) 1028val SELF_LE_SQ = store_thm( 1029 "SELF_LE_SQ", 1030 ``!n. n <= n ** 2``, 1031 rpt strip_tac >> 1032 Cases_on `n = 0` >- 1033 rw[] >> 1034 `0 < n /\ 1 <= 2` by decide_tac >> 1035 metis_tac[EXP_BASE_LEQ_MONO_IMP, EXP_1]); 1036 1037(* Theorem: a <= b /\ c <= d ==> a + c <= b + d *) 1038(* Proof: by LESS_EQ_LESS_EQ_MONO, or 1039 Note a <= b ==> a + c <= b + c by LE_ADD_RCANCEL 1040 and c <= d ==> b + c <= b + d by LE_ADD_LCANCEL 1041 Thus a + c <= b + d by LESS_EQ_TRANS 1042*) 1043val LE_MONO_ADD2 = store_thm( 1044 "LE_MONO_ADD2", 1045 ``!a b c d. a <= b /\ c <= d ==> a + c <= b + d``, 1046 rw[LESS_EQ_LESS_EQ_MONO]); 1047 1048(* Theorem: a < b /\ c < d ==> a + c < b + d *) 1049(* Proof: 1050 Note a < b ==> a + c < b + c by LT_ADD_RCANCEL 1051 and c < d ==> b + c < b + d by LT_ADD_LCANCEL 1052 Thus a + c < b + d by LESS_TRANS 1053*) 1054val LT_MONO_ADD2 = store_thm( 1055 "LT_MONO_ADD2", 1056 ``!a b c d. a < b /\ c < d ==> a + c < b + d``, 1057 rw[LT_ADD_RCANCEL, LT_ADD_LCANCEL]); 1058 1059(* Theorem: a <= b /\ c <= d ==> a * c <= b * d *) 1060(* Proof: by LESS_MONO_MULT2, or 1061 Note a <= b ==> a * c <= b * c by LE_MULT_RCANCEL 1062 and c <= d ==> b * c <= b * d by LE_MULT_LCANCEL 1063 Thus a * c <= b * d by LESS_EQ_TRANS 1064*) 1065val LE_MONO_MULT2 = store_thm( 1066 "LE_MONO_MULT2", 1067 ``!a b c d. a <= b /\ c <= d ==> a * c <= b * d``, 1068 rw[LESS_MONO_MULT2]); 1069 1070(* Theorem: a < b /\ c < d ==> a * c < b * d *) 1071(* Proof: 1072 Note 0 < b, by a < b. 1073 and 0 < d, by c < d. 1074 If c = 0, 1075 Then a * c = 0 < b * d by MULT_EQ_0 1076 If c <> 0, then 0 < c by NOT_ZERO_LT_ZERO 1077 a < b ==> a * c < b * c by LT_MULT_RCANCEL, 0 < c 1078 c < d ==> b * c < b * d by LT_MULT_LCANCEL, 0 < b 1079 Thus a * c < b * d by LESS_TRANS 1080*) 1081val LT_MONO_MULT2 = store_thm( 1082 "LT_MONO_MULT2", 1083 ``!a b c d. a < b /\ c < d ==> a * c < b * d``, 1084 rpt strip_tac >> 1085 `0 < b /\ 0 < d` by decide_tac >> 1086 Cases_on `c = 0` >- 1087 metis_tac[MULT_EQ_0, NOT_ZERO_LT_ZERO] >> 1088 metis_tac[LT_MULT_RCANCEL, LT_MULT_LCANCEL, LESS_TRANS, NOT_ZERO_LT_ZERO]); 1089 1090(* Theorem: 1 < m /\ 1 < n ==> (m + n <= m * n) *) 1091(* Proof: 1092 Let m = m' + 1, n = n' + 1. 1093 Note m' <> 0 /\ n' <> 0. 1094 Thus m' * n' <> 0 by MULT_EQ_0 1095 or 1 <= m' * n' 1096 m * n 1097 = (m' + 1) * (n' + 1) 1098 = m' * n' + m' + n' + 1 by arithmetic 1099 >= 1 + m' + n' + 1 by 1 <= m' * n' 1100 = m + n 1101*) 1102val SUM_LE_PRODUCT = store_thm( 1103 "SUM_LE_PRODUCT", 1104 ``!m n. 1 < m /\ 1 < n ==> (m + n <= m * n)``, 1105 rpt strip_tac >> 1106 `m <> 0 /\ n <> 0` by decide_tac >> 1107 `?m' n'. (m = m' + 1) /\ (n = n' + 1)` by metis_tac[num_CASES, ADD1] >> 1108 `m * n = (m' + 1) * n' + (m' + 1)` by rw[LEFT_ADD_DISTRIB] >> 1109 `_ = m' * n' + n' + (m' + 1)` by rw[RIGHT_ADD_DISTRIB] >> 1110 `_ = m + (n' + m' * n')` by decide_tac >> 1111 `m' * n' <> 0` by fs[] >> 1112 decide_tac); 1113 1114(* Theorem: 0 < n ==> k * n + 1 <= (k + 1) * n *) 1115(* Proof: 1116 k * n + 1 1117 <= k * n + n by 1 <= n 1118 <= (k + 1) * n by RIGHT_ADD_DISTRIB 1119*) 1120val MULTIPLE_SUC_LE = store_thm( 1121 "MULTIPLE_SUC_LE", 1122 ``!n k. 0 < n ==> k * n + 1 <= (k + 1) * n``, 1123 decide_tac); 1124 1125(* ------------------------------------------------------------------------- *) 1126(* Simple Theorems *) 1127(* ------------------------------------------------------------------------- *) 1128 1129(* Theorem: 0 < m /\ 0 < n /\ (m + n = 2) ==> m = 1 /\ n = 1 *) 1130(* Proof: by arithmetic. *) 1131val ADD_EQ_2 = store_thm( 1132 "ADD_EQ_2", 1133 ``!m n. 0 < m /\ 0 < n /\ (m + n = 2) ==> (m = 1) /\ (n = 1)``, 1134 rw_tac arith_ss[]); 1135 1136(* Theorem: EVEN 0 *) 1137(* Proof: by EVEN. *) 1138val EVEN_0 = store_thm( 1139 "EVEN_0", 1140 ``EVEN 0``, 1141 simp[]); 1142 1143(* Theorem: ODD 1 *) 1144(* Proof: by ODD. *) 1145val ODD_1 = store_thm( 1146 "ODD_1", 1147 ``ODD 1``, 1148 simp[]); 1149 1150(* Theorem: EVEN 2 *) 1151(* Proof: by EVEN_MOD2. *) 1152val EVEN_2 = store_thm( 1153 "EVEN_2", 1154 ``EVEN 2``, 1155 EVAL_TAC); 1156 1157(* 1158EVEN_ADD |- !m n. EVEN (m + n) <=> (EVEN m <=> EVEN n) 1159ODD_ADD |- !m n. ODD (m + n) <=> (ODD m <=/=> ODD n) 1160EVEN_MULT |- !m n. EVEN (m * n) <=> EVEN m \/ EVEN n 1161ODD_MULT |- !m n. ODD (m * n) <=> ODD m /\ ODD n 1162*) 1163 1164(* Derive theorems. *) 1165val EVEN_SQ = save_thm("EVEN_SQ", 1166 EVEN_MULT |> SPEC ``n:num`` |> SPEC ``n:num`` |> SIMP_RULE arith_ss[] |> GEN_ALL); 1167(* val EVEN_SQ = |- !n. EVEN (n ** 2) <=> EVEN n: thm *) 1168val ODD_SQ = save_thm("ODD_SQ", 1169 ODD_MULT |> SPEC ``n:num`` |> SPEC ``n:num`` |> SIMP_RULE arith_ss[] |> GEN_ALL); 1170(* val ODD_SQ = |- !n. ODD (n ** 2) <=> ODD n: thm *) 1171 1172(* Theorem: EVEN (2 * a + b) <=> EVEN b *) 1173(* Proof: 1174 EVEN (2 * a + b) 1175 <=> EVEN (2 * a) /\ EVEN b by EVEN_ADD 1176 <=> T /\ EVEN b by EVEN_DOUBLE 1177 <=> EVEN b 1178*) 1179Theorem EQ_PARITY: 1180 !a b. EVEN (2 * a + b) <=> EVEN b 1181Proof 1182 rw[EVEN_ADD, EVEN_DOUBLE] 1183QED 1184 1185(* Theorem: ODD x <=> (x MOD 2 = 1) *) 1186(* Proof: 1187 If part: ODD x ==> x MOD 2 = 1 1188 Since ODD x 1189 <=> ~EVEN x by ODD_EVEN 1190 <=> ~(x MOD 2 = 0) by EVEN_MOD2 1191 But x MOD 2 < 2 by MOD_LESS, 0 < 2 1192 so x MOD 2 = 1 by arithmetic 1193 Only-if part: x MOD 2 = 1 ==> ODD x 1194 By contradiction, suppose ~ODD x. 1195 Then EVEN x by ODD_EVEN 1196 and x MOD 2 = 0 by EVEN_MOD2 1197 This contradicts x MOD 2 = 1. 1198*) 1199val ODD_MOD2 = store_thm( 1200 "ODD_MOD2", 1201 ``!x. ODD x <=> (x MOD 2 = 1)``, 1202 metis_tac[EVEN_MOD2, ODD_EVEN, MOD_LESS, 1203 DECIDE``0 <> 1 /\ 0 < 2 /\ !n. n < 2 /\ n <> 1 ==> (n = 0)``]); 1204 1205(* Theorem: (EVEN n <=> ODD (SUC n)) /\ (ODD n <=> EVEN (SUC n)) *) 1206(* Proof: by EVEN, ODD, EVEN_OR_ODD *) 1207val EVEN_ODD_SUC = store_thm( 1208 "EVEN_ODD_SUC", 1209 ``!n. (EVEN n <=> ODD (SUC n)) /\ (ODD n <=> EVEN (SUC n))``, 1210 metis_tac[EVEN, ODD, EVEN_OR_ODD]); 1211 1212(* Theorem: 0 < n ==> (EVEN n <=> ODD (PRE n)) /\ (ODD n <=> EVEN (PRE n)) *) 1213(* Proof: by EVEN, ODD, EVEN_OR_ODD, PRE_SUC_EQ *) 1214val EVEN_ODD_PRE = store_thm( 1215 "EVEN_ODD_PRE", 1216 ``!n. 0 < n ==> (EVEN n <=> ODD (PRE n)) /\ (ODD n <=> EVEN (PRE n))``, 1217 metis_tac[EVEN, ODD, EVEN_OR_ODD, PRE_SUC_EQ]); 1218 1219(* Theorem: EVEN (n * (n + 1)) *) 1220(* Proof: 1221 If EVEN n, true by EVEN_MULT 1222 If ~(EVEN n), 1223 Then EVEN (SUC n) by EVEN 1224 or EVEN (n + 1) by ADD1 1225 Thus true by EVEN_MULT 1226*) 1227val EVEN_PARTNERS = store_thm( 1228 "EVEN_PARTNERS", 1229 ``!n. EVEN (n * (n + 1))``, 1230 metis_tac[EVEN, EVEN_MULT, ADD1]); 1231 1232(* Theorem: EVEN n ==> (n = 2 * HALF n) *) 1233(* Proof: 1234 Note EVEN n ==> ?m. n = 2 * m by EVEN_EXISTS 1235 and HALF n = HALF (2 * m) by above 1236 = m by MULT_TO_DIV, 0 < 2 1237 Thus n = 2 * m = 2 * HALF n by above 1238*) 1239val EVEN_HALF = store_thm( 1240 "EVEN_HALF", 1241 ``!n. EVEN n ==> (n = 2 * HALF n)``, 1242 metis_tac[EVEN_EXISTS, MULT_TO_DIV, DECIDE``0 < 2``]); 1243 1244(* Theorem: ODD n ==> (n = 2 * HALF n + 1 *) 1245(* Proof: 1246 Since n = HALF n * 2 + n MOD 2 by DIVISION, 0 < 2 1247 = 2 * HALF n + n MOD 2 by MULT_COMM 1248 = 2 * HALF n + 1 by ODD_MOD2 1249*) 1250val ODD_HALF = store_thm( 1251 "ODD_HALF", 1252 ``!n. ODD n ==> (n = 2 * HALF n + 1)``, 1253 metis_tac[DIVISION, MULT_COMM, ODD_MOD2, DECIDE``0 < 2``]); 1254 1255(* Theorem: EVEN n ==> (HALF (SUC n) = HALF n) *) 1256(* Proof: 1257 Note n = (HALF n) * 2 + (n MOD 2) by DIVISION, 0 < 2 1258 = (HALF n) * 2 by EVEN_MOD2 1259 Now SUC n 1260 = n + 1 by ADD1 1261 = (HALF n) * 2 + 1 by above 1262 Thus HALF (SUC n) 1263 = ((HALF n) * 2 + 1) DIV 2 by above 1264 = HALF n by DIV_MULT, 1 < 2 1265*) 1266val EVEN_SUC_HALF = store_thm( 1267 "EVEN_SUC_HALF", 1268 ``!n. EVEN n ==> (HALF (SUC n) = HALF n)``, 1269 rpt strip_tac >> 1270 `n MOD 2 = 0` by rw[GSYM EVEN_MOD2] >> 1271 `n = HALF n * 2 + n MOD 2` by rw[DIVISION] >> 1272 `SUC n = HALF n * 2 + 1` by rw[] >> 1273 metis_tac[DIV_MULT, DECIDE``1 < 2``]); 1274 1275(* Theorem: ODD n ==> (HALF (SUC n) = SUC (HALF n)) *) 1276(* Proof: 1277 SUC n 1278 = SUC (2 * HALF n + 1) by ODD_HALF 1279 = 2 * HALF n + 1 + 1 by ADD1 1280 = 2 * HALF n + 2 by arithmetic 1281 = 2 * (HALF n + 1) by LEFT_ADD_DISTRIB 1282 = 2 * SUC (HALF n) by ADD1 1283 = SUC (HALF n) * 2 + 0 by MULT_COMM, ADD_0 1284 Hence HALF (SUC n) = SUC (HALF n) by DIV_UNIQUE, 0 < 2 1285*) 1286val ODD_SUC_HALF = store_thm( 1287 "ODD_SUC_HALF", 1288 ``!n. ODD n ==> (HALF (SUC n) = SUC (HALF n))``, 1289 rpt strip_tac >> 1290 `SUC n = SUC (2 * HALF n + 1)` by rw[ODD_HALF] >> 1291 `_ = SUC (HALF n) * 2 + 0` by rw[] >> 1292 metis_tac[DIV_UNIQUE, DECIDE``0 < 2``]); 1293 1294(* Theorem: (HALF n = 0) <=> ((n = 0) \/ (n = 1)) *) 1295(* Proof: 1296 If part: (HALF n = 0) ==> ((n = 0) \/ (n = 1)) 1297 Note n = (HALF n) * 2 + (n MOD 2) by DIVISION, 0 < 2 1298 = n MOD 2 by HALF n = 0 1299 and n MOD 2 < 2 by MOD_LESS, 0 < 2 1300 so n < 2, or n = 0 or n = 1 by arithmetic 1301 Only-if part: HALF 0 = 0, HALF 1 = 0. 1302 True since both 0 or 1 < 2 by LESS_DIV_EQ_ZERO, 0 < 2 1303*) 1304val HALF_EQ_0 = store_thm( 1305 "HALF_EQ_0", 1306 ``!n. (HALF n = 0) <=> ((n = 0) \/ (n = 1))``, 1307 rw[LESS_DIV_EQ_ZERO, EQ_IMP_THM] >> 1308 `n = (HALF n) * 2 + (n MOD 2)` by rw[DIVISION] >> 1309 `n MOD 2 < 2` by rw[MOD_LESS] >> 1310 decide_tac); 1311 1312(* Theorem: (HALF n = n) <=> (n = 0) *) 1313(* Proof: 1314 If part: HALF n = n ==> n = 0 1315 Note n = 2 * HALF n + (n MOD 2) by DIVISION, MULT_COMM 1316 so n = 2 * n + (n MOD 2) by HALF n = n 1317 or 0 = n + (n MOD 2) by arithmetic 1318 Thus n = 0 and (n MOD 2 = 0) by ADD_EQ_0 1319 Only-if part: HALF 0 = 0, true by ZERO_DIV, 0 < 2 1320*) 1321val HALF_EQ_SELF = store_thm( 1322 "HALF_EQ_SELF", 1323 ``!n. (HALF n = n) <=> (n = 0)``, 1324 rw[EQ_IMP_THM] >> 1325 `n = 2 * HALF n + (n MOD 2)` by metis_tac[DIVISION, MULT_COMM, DECIDE``0 < 2``] >> 1326 rw[ADD_EQ_0]); 1327 1328(* Theorem: 0 < n ==> HALF n < n *) 1329(* Proof: 1330 Note HALF n <= n by DIV_LESS_EQ, 0 < 2 1331 and HALF n <> n by HALF_EQ_SELF, n <> 0 1332 so HALF n < n by arithmetic 1333*) 1334val HALF_LESS = store_thm( 1335 "HALF_LESS", 1336 ``!n. 0 < n ==> HALF n < n``, 1337 rpt strip_tac >> 1338 `HALF n <= n` by rw[DIV_LESS_EQ] >> 1339 `HALF n <> n` by rw[HALF_EQ_SELF] >> 1340 decide_tac); 1341 1342(* Theorem: HALF (2 * n) = n *) 1343(* Proof: 1344 Let m = 2 * n. 1345 Then EVEN m by EVEN_DOUBLE 1346 so 2 * HALF m = m = 2 * n by EVEN_HALF 1347 or HALF m = n by MULT_LEFT_CANCEL 1348*) 1349val HALF_TWICE = store_thm( 1350 "HALF_TWICE", 1351 ``!n. HALF (2 * n) = n``, 1352 metis_tac[EVEN_DOUBLE, EVEN_HALF, MULT_LEFT_CANCEL, DECIDE``2 <> 0``]); 1353 1354(* Theorem: n * HALF m <= HALF (n * m) *) 1355(* Proof: 1356 Let k = HALF m. 1357 If EVEN m, 1358 Then m = 2 * k by EVEN_HALF 1359 HALF (n * m) 1360 = HALF (n * (2 * k)) by above 1361 = HALF (2 * (n * k)) by arithmetic 1362 = n * k by HALF_TWICE 1363 If ~EVEN m, then ODD m by ODD_EVEN 1364 Then m = 2 * k + 1 by ODD_HALF 1365 so HALF (n * m) 1366 = HALF (n * (2 * k + 1)) by above 1367 = HALF (2 * (n * k) + n) by LEFT_ADD_DISTRIB 1368 = HALF (2 * (n * k)) + HALF n by ADD_DIV_ADD_DIV 1369 = n * k + HALF n by HALF_TWICE 1370 >= n * k by arithmetic 1371*) 1372val HALF_MULT = store_thm( 1373 "HALF_MULT", 1374 ``!m n. n * HALF m <= HALF (n * m)``, 1375 rpt strip_tac >> 1376 qabbrev_tac `k = HALF m` >> 1377 Cases_on `EVEN m` >| [ 1378 `m = 2 * k` by rw[EVEN_HALF, Abbr`k`] >> 1379 `HALF (n * m) = HALF (2 * (n * k))` by rw[] >> 1380 `_ = n * k` by rw[GSYM HALF_TWICE] >> 1381 decide_tac, 1382 `ODD m` by rw[ODD_EVEN] >> 1383 `m = 2 * k + 1` by rw[ODD_HALF, Abbr`k`] >> 1384 `HALF (n * m) = HALF (2 * (n * k) + n)` by rw[LEFT_ADD_DISTRIB] >> 1385 `_ = (n * k) + HALF n` by rw[HALF_TWICE, GSYM ADD_DIV_ADD_DIV] >> 1386 decide_tac 1387 ]); 1388 1389(* Theorem: 2 * HALF n <= n /\ n <= SUC (2 * HALF n) *) 1390(* Proof: 1391 If EVEN n, 1392 Then n = 2 * HALF n by EVEN_HALF 1393 and n = n < SUC n by LESS_SUC 1394 or n <= n <= SUC n, 1395 Giving 2 * HALF n <= n /\ n <= SUC (2 * HALF n) 1396 If ~(EVEN n), then ODD n by EVEN_ODD 1397 Then n = 2 * HALF n + 1 by ODD_HALF 1398 = SUC (2 * HALF n) by ADD1 1399 or n - 1 < n = n 1400 or n - 1 <= n <= n, 1401 Giving 2 * HALF n <= n /\ n <= SUC (2 * HALF n) 1402*) 1403val TWO_HALF_LESS_EQ = store_thm( 1404 "TWO_HALF_LESS_EQ", 1405 ``!n. 2 * HALF n <= n /\ n <= SUC (2 * HALF n)``, 1406 strip_tac >> 1407 Cases_on `EVEN n` >- 1408 rw[GSYM EVEN_HALF] >> 1409 `ODD n` by rw[ODD_EVEN] >> 1410 `n <> 0` by metis_tac[ODD] >> 1411 `n = SUC (2 * HALF n)` by rw[ODD_HALF, ADD1] >> 1412 `2 * HALF n = PRE n` by rw[] >> 1413 rw[]); 1414 1415(* Theorem: 2 * ((HALF n) * m) <= n * m *) 1416(* Proof: 1417 2 * ((HALF n) * m) 1418 = 2 * (m * HALF n) by MULT_COMM 1419 <= 2 * (HALF (m * n)) by HALF_MULT 1420 <= m * n by TWO_HALF_LESS_EQ 1421 = n * m by MULT_COMM 1422*) 1423val TWO_HALF_TIMES_LE = store_thm( 1424 "TWO_HALF_TIMES_LE", 1425 ``!m n. 2 * ((HALF n) * m) <= n * m``, 1426 rpt strip_tac >> 1427 `2 * (m * HALF n) <= 2 * (HALF (m * n))` by rw[HALF_MULT] >> 1428 `2 * (HALF (m * n)) <= m * n` by rw[TWO_HALF_LESS_EQ] >> 1429 fs[]); 1430 1431(* Theorem: 0 < n ==> 1 + HALF n <= n *) 1432(* Proof: 1433 If n = 1, 1434 HALF 1 = 0, hence true. 1435 If n <> 1, 1436 Then HALF n <> 0 by HALF_EQ_0, n <> 0, n <> 1 1437 Thus 1 + HALF n 1438 <= HALF n + HALF n by 1 <= HALF n 1439 = 2 * HALF n 1440 <= n by TWO_HALF_LESS_EQ 1441*) 1442val SUC_HALF_LE = store_thm( 1443 "SUC_HALF_LE", 1444 ``!n. 0 < n ==> 1 + HALF n <= n``, 1445 rpt strip_tac >> 1446 (Cases_on `n = 1` >> simp[]) >> 1447 `HALF n <> 0` by metis_tac[HALF_EQ_0, NOT_ZERO] >> 1448 `1 + HALF n <= 2 * HALF n` by decide_tac >> 1449 `2 * HALF n <= n` by rw[TWO_HALF_LESS_EQ] >> 1450 decide_tac); 1451 1452(* Theorem: (HALF n) ** 2 <= (n ** 2) DIV 4 *) 1453(* Proof: 1454 Let k = HALF n. 1455 Then 2 * k <= n by TWO_HALF_LESS_EQ 1456 so (2 * k) ** 2 <= n ** 2 by EXP_EXP_LE_MONO 1457 and (2 * k) ** 2 DIV 4 <= n ** 2 DIV 4 by DIV_LE_MONOTONE, 0 < 4 1458 But (2 * k) ** 2 DIV 4 1459 = 4 * k ** 2 DIV 4 by EXP_BASE_MULT 1460 = k ** 2 by MULT_TO_DIV, 0 < 4 1461 Thus k ** 2 <= n ** 2 DIV 4. 1462*) 1463val HALF_SQ_LE = store_thm( 1464 "HALF_SQ_LE", 1465 ``!n. (HALF n) ** 2 <= (n ** 2) DIV 4``, 1466 rpt strip_tac >> 1467 qabbrev_tac `k = HALF n` >> 1468 `2 * k <= n` by rw[TWO_HALF_LESS_EQ, Abbr`k`] >> 1469 `(2 * k) ** 2 <= n ** 2` by rw[] >> 1470 `(2 * k) ** 2 DIV 4 <= n ** 2 DIV 4` by rw[DIV_LE_MONOTONE] >> 1471 `(2 * k) ** 2 DIV 4 = 4 * k ** 2 DIV 4` by rw[EXP_BASE_MULT] >> 1472 `_ = k ** 2` by rw[MULT_TO_DIV] >> 1473 decide_tac); 1474 1475(* Obtain theorems *) 1476val HALF_LE = save_thm("HALF_LE", 1477 DIV_LESS_EQ |> SPEC ``2`` |> SIMP_RULE (arith_ss) [] |> SPEC ``n:num`` |> GEN_ALL); 1478(* val HALF_LE = |- !n. HALF n <= n: thm *) 1479val HALF_LE_MONO = save_thm("HALF_LE_MONO", 1480 DIV_LE_MONOTONE |> SPEC ``2`` |> SIMP_RULE (arith_ss) []); 1481(* val HALF_LE_MONO = |- !x y. x <= y ==> HALF x <= HALF y: thm *) 1482 1483(* Theorem: EVEN n ==> !m. m * n = (TWICE m) * (HALF n) *) 1484(* Proof: 1485 (TWICE m) * (HALF n) 1486 = (2 * m) * (HALF n) by notation 1487 = m * TWICE (HALF n) by MULT_COMM, MULT_ASSOC 1488 = m * n by EVEN_HALF 1489*) 1490val MULT_EVEN = store_thm( 1491 "MULT_EVEN", 1492 ``!n. EVEN n ==> !m. m * n = (TWICE m) * (HALF n)``, 1493 metis_tac[MULT_COMM, MULT_ASSOC, EVEN_HALF]); 1494 1495(* Theorem: ODD n ==> !m. m * n = m + (TWICE m) * (HALF n) *) 1496(* Proof: 1497 m + (TWICE m) * (HALF n) 1498 = m + (2 * m) * (HALF n) by notation 1499 = m + m * (TWICE (HALF n)) by MULT_COMM, MULT_ASSOC 1500 = m * (SUC (TWICE (HALF n))) by MULT_SUC 1501 = m * (TWICE (HALF n) + 1) by ADD1 1502 = m * n by ODD_HALF 1503*) 1504val MULT_ODD = store_thm( 1505 "MULT_ODD", 1506 ``!n. ODD n ==> !m. m * n = m + (TWICE m) * (HALF n)``, 1507 metis_tac[MULT_COMM, MULT_ASSOC, ODD_HALF, MULT_SUC, ADD1]); 1508 1509(* Theorem: EVEN m /\ m <> 0 ==> !n. EVEN n <=> EVEN (n MOD m) *) 1510(* Proof: 1511 Note ?k. m = 2 * k by EVEN_EXISTS, EVEN m 1512 and k <> 0 by MULT_EQ_0, m <> 0 1513 ==> (n MOD m) MOD 2 = n MOD 2 by MOD_MULT_MOD 1514 The result follows by EVEN_MOD2 1515*) 1516val EVEN_MOD_EVEN = store_thm( 1517 "EVEN_MOD_EVEN", 1518 ``!m. EVEN m /\ m <> 0 ==> !n. EVEN n <=> EVEN (n MOD m)``, 1519 rpt strip_tac >> 1520 `?k. m = 2 * k` by rw[GSYM EVEN_EXISTS] >> 1521 `(n MOD m) MOD 2 = n MOD 2` by rw[MOD_MULT_MOD] >> 1522 metis_tac[EVEN_MOD2]); 1523 1524(* Theorem: EVEN m /\ m <> 0 ==> !n. ODD n <=> ODD (n MOD m) *) 1525(* Proof: by EVEN_MOD_EVEN, ODD_EVEN *) 1526val EVEN_MOD_ODD = store_thm( 1527 "EVEN_MOD_ODD", 1528 ``!m. EVEN m /\ m <> 0 ==> !n. ODD n <=> ODD (n MOD m)``, 1529 rw_tac std_ss[EVEN_MOD_EVEN, ODD_EVEN]); 1530 1531(* Theorem: c <= a ==> ((a - b) - (a - c) = c - b) *) 1532(* Proof: 1533 a - b - (a - c) 1534 = a - (b + (a - c)) by SUB_RIGHT_SUB, no condition 1535 = a - ((a - c) + b) by ADD_COMM, no condition 1536 = a - (a - c) - b by SUB_RIGHT_SUB, no condition 1537 = a + c - a - b by SUB_SUB, c <= a 1538 = c + a - a - b by ADD_COMM, no condition 1539 = c + (a - a) - b by LESS_EQ_ADD_SUB, a <= a 1540 = c + 0 - b by SUB_EQUAL_0 1541 = c - b 1542*) 1543val SUB_SUB_SUB = store_thm( 1544 "SUB_SUB_SUB", 1545 ``!a b c. c <= a ==> ((a - b) - (a - c) = c - b)``, 1546 decide_tac); 1547 1548(* Theorem: c <= a ==> (a + b - (a - c) = c + b) *) 1549(* Proof: 1550 a + b - (a - c) 1551 = a + b + c - a by SUB_SUB, a <= c 1552 = a + (b + c) - a by ADD_ASSOC 1553 = (b + c) + a - a by ADD_COMM 1554 = b + c - (a - a) by SUB_SUB, a <= a 1555 = b + c - 0 by SUB_EQUAL_0 1556 = b + c by SUB_0 1557*) 1558val ADD_SUB_SUB = store_thm( 1559 "ADD_SUB_SUB", 1560 ``!a b c. c <= a ==> (a + b - (a - c) = c + b)``, 1561 decide_tac); 1562 1563(* Theorem: 0 < p ==> !m n. (m - n = p) <=> (m = n + p) *) 1564(* Proof: 1565 If part: m - n = p ==> m = n + p 1566 Note 0 < m - n by 0 < p 1567 so n < m by LESS_MONO_ADD 1568 or m = m - n + n by SUB_ADD, n <= m 1569 = p + n by m - n = p 1570 = n + p by ADD_COMM 1571 Only-if part: m = n + p ==> m - n = p 1572 m - n 1573 = (n + p) - n by m = n + p 1574 = p + n - n by ADD_COMM 1575 = p by ADD_SUB 1576*) 1577val SUB_EQ_ADD = store_thm( 1578 "SUB_EQ_ADD", 1579 ``!p. 0 < p ==> !m n. (m - n = p) <=> (m = n + p)``, 1580 decide_tac); 1581 1582(* Note: ADD_EQ_SUB |- !m n p. n <= p ==> ((m + n = p) <=> (m = p - n)) *) 1583 1584(* Theorem: 0 < a /\ 0 < b /\ a < c /\ (a * b = c * d) ==> (d < b) *) 1585(* Proof: 1586 By contradiction, suppose b <= d. 1587 Since a * b <> 0 by MULT_EQ_0, 0 < a, 0 < b 1588 so d <> 0, or 0 < d by MULT_EQ_0, a * b <> 0 1589 Now a * b <= a * d by LE_MULT_LCANCEL, b <= d, a <> 0 1590 and a * d < c * d by LT_MULT_LCANCEL, a < c, d <> 0 1591 so a * b < c * d by LESS_EQ_LESS_TRANS 1592 This contradicts a * b = c * d. 1593*) 1594val MULT_EQ_LESS_TO_MORE = store_thm( 1595 "MULT_EQ_LESS_TO_MORE", 1596 ``!a b c d. 0 < a /\ 0 < b /\ a < c /\ (a * b = c * d) ==> (d < b)``, 1597 spose_not_then strip_assume_tac >> 1598 `b <= d` by decide_tac >> 1599 `0 < d` by decide_tac >> 1600 `a * b <= a * d` by rw[LE_MULT_LCANCEL] >> 1601 `a * d < c * d` by rw[LT_MULT_LCANCEL] >> 1602 decide_tac); 1603 1604(* Theorem: 0 < c /\ 0 < d /\ a * b <= c * d /\ d < b ==> a < c *) 1605(* Proof: 1606 By contradiction, suppose c <= a. 1607 With d < b, which gives d <= b by LESS_IMP_LESS_OR_EQ 1608 Thus c * d <= a * b by LE_MONO_MULT2 1609 or a * b = c * d by a * b <= c * d 1610 Note 0 < c /\ 0 < d by given 1611 ==> a < c by MULT_EQ_LESS_TO_MORE 1612 This contradicts c <= a. 1613 1614MULT_EQ_LESS_TO_MORE 1615|- !a b c d. 0 < a /\ 0 < b /\ a < c /\ a * b = c * d ==> d < b 1616 0 < d /\ 0 < c /\ d < b /\ d * c = b * a ==> a < c 1617*) 1618val LE_IMP_REVERSE_LT = store_thm( 1619 "LE_IMP_REVERSE_LT", 1620 ``!a b c d. 0 < c /\ 0 < d /\ a * b <= c * d /\ d < b ==> a < c``, 1621 spose_not_then strip_assume_tac >> 1622 `c <= a` by decide_tac >> 1623 `c * d <= a * b` by rw[LE_MONO_MULT2] >> 1624 `a * b = c * d` by decide_tac >> 1625 `a < c` by metis_tac[MULT_EQ_LESS_TO_MORE, MULT_COMM]); 1626 1627(* ------------------------------------------------------------------------- *) 1628(* Exponential Theorems *) 1629(* ------------------------------------------------------------------------- *) 1630 1631(* Theorem: n ** 0 = 1 *) 1632(* Proof: by EXP *) 1633val EXP_0 = store_thm( 1634 "EXP_0", 1635 ``!n. n ** 0 = 1``, 1636 rw_tac std_ss[EXP]); 1637 1638(* Theorem: n ** 2 = n * n *) 1639(* Proof: 1640 n ** 2 = n * (n ** 1) = n * (n * (n ** 0)) = n * (n * 1) = n * n 1641 or n ** 2 = n * (n ** 1) = n * n by EXP_1: !n. (1 ** n = 1) /\ (n ** 1 = n) 1642*) 1643val EXP_2 = store_thm( 1644 "EXP_2", 1645 ``!n. n ** 2 = n * n``, 1646 metis_tac[EXP, TWO, EXP_1]); 1647 1648(* Theorem: m <> 0 ==> m ** n <> 0 *) 1649(* Proof: by EXP_EQ_0 *) 1650val EXP_NONZERO = store_thm( 1651 "EXP_NONZERO", 1652 ``!m n. m <> 0 ==> m ** n <> 0``, 1653 metis_tac[EXP_EQ_0]); 1654 1655(* Theorem: 0 < m ==> 0 < m ** n *) 1656(* Proof: by EXP_NONZERO *) 1657val EXP_POS = store_thm( 1658 "EXP_POS", 1659 ``!m n. 0 < m ==> 0 < m ** n``, 1660 rw[EXP_NONZERO]); 1661 1662(* Theorem: 0 < m ==> ((n ** m = n) <=> ((m = 1) \/ (n = 0) \/ (n = 1))) *) 1663(* Proof: 1664 If part: n ** m = n ==> n = 0 \/ n = 1 1665 By contradiction, assume n <> 0 /\ n <> 1. 1666 Then ?k. m = SUC k by num_CASES, 0 < m 1667 so n ** SUC k = n by n ** m = n 1668 or n * n ** k = n by EXP 1669 ==> n ** k = 1 by MULT_EQ_SELF, 0 < n 1670 ==> n = 1 or k = 0 by EXP_EQ_1 1671 ==> n = 1 or m = 1, 1672 These contradict n <> 1 and m <> 1. 1673 Only-if part: n ** 1 = n /\ 0 ** m = 0 /\ 1 ** m = 1 1674 These are true by EXP_1, ZERO_EXP. 1675*) 1676val EXP_EQ_SELF = store_thm( 1677 "EXP_EQ_SELF", 1678 ``!n m. 0 < m ==> ((n ** m = n) <=> ((m = 1) \/ (n = 0) \/ (n = 1)))``, 1679 rw_tac std_ss[EQ_IMP_THM] >| [ 1680 spose_not_then strip_assume_tac >> 1681 `m <> 0` by decide_tac >> 1682 `?k. m = SUC k` by metis_tac[num_CASES] >> 1683 `n * n ** k = n` by fs[EXP] >> 1684 `n ** k = 1` by metis_tac[MULT_EQ_SELF, NOT_ZERO_LT_ZERO] >> 1685 fs[EXP_EQ_1], 1686 rw[], 1687 rw[], 1688 rw[] 1689 ]); 1690 1691(* Obtain a theorem *) 1692val EXP_LE = save_thm("EXP_LE", X_LE_X_EXP |> GEN ``x:num`` |> SPEC ``b:num`` |> GEN_ALL); 1693(* val EXP_LE = |- !n b. 0 < n ==> b <= b ** n: thm *) 1694 1695(* Theorem: 1 < b /\ 1 < n ==> b < b ** n *) 1696(* Proof: 1697 By contradiction, assume ~(b < b ** n). 1698 Then b ** n <= b by arithmetic 1699 But b <= b ** n by EXP_LE, 0 < n 1700 ==> b ** n = b by EQ_LESS_EQ 1701 ==> b = 1 or n = 0 or n = 1. 1702 All these contradict 1 < b and 1 < n. 1703*) 1704val EXP_LT = store_thm( 1705 "EXP_LT", 1706 ``!n b. 1 < b /\ 1 < n ==> b < b ** n``, 1707 spose_not_then strip_assume_tac >> 1708 `b <= b ** n` by rw[EXP_LE] >> 1709 `b ** n = b` by decide_tac >> 1710 rfs[EXP_EQ_SELF]); 1711 1712(* Theorem: 0 < a /\ n < m /\ (a ** n * b = a ** m * c) ==> ?d. 0 < d /\ (b = a ** d * c) *) 1713(* Proof: 1714 Let d = m - n. 1715 Then 0 < d, and m = n + d by arithmetic 1716 and 0 < a ==> a ** n <> 0 by EXP_EQ_0 1717 a ** n * b 1718 = a ** (n + d) * c by m = n + d 1719 = (a ** n * a ** d) * c by EXP_ADD 1720 = a ** n * (a ** d * c) by MULT_ASSOC 1721 The result follows by MULT_LEFT_CANCEL 1722*) 1723val EXP_LCANCEL = store_thm( 1724 "EXP_LCANCEL", 1725 ``!a b c n m. 0 < a /\ n < m /\ (a ** n * b = a ** m * c) ==> ?d. 0 < d /\ (b = a ** d * c)``, 1726 rpt strip_tac >> 1727 `0 < m - n /\ (m = n + (m - n))` by decide_tac >> 1728 qabbrev_tac `d = m - n` >> 1729 `a ** n <> 0` by metis_tac[EXP_EQ_0, NOT_ZERO_LT_ZERO] >> 1730 metis_tac[EXP_ADD, MULT_ASSOC, MULT_LEFT_CANCEL]); 1731 1732(* Theorem: 0 < a /\ n < m /\ (a ** n * b = a ** m * c) ==> ?d. 0 < d /\ (b = a ** d * c) *) 1733(* Proof: by EXP_LCANCEL, MULT_COMM. *) 1734val EXP_RCANCEL = store_thm( 1735 "EXP_RCANCEL", 1736 ``!a b c n m. 0 < a /\ n < m /\ (b * a ** n = c * a ** m) ==> ?d. 0 < d /\ (b = c * a ** d)``, 1737 metis_tac[EXP_LCANCEL, MULT_COMM]); 1738 1739(* 1740EXP_POS |- !m n. 0 < m ==> 0 < m ** n 1741ONE_LT_EXP |- !x y. 1 < x ** y <=> 1 < x /\ 0 < y 1742ZERO_LT_EXP |- 0 < x ** y <=> 0 < x \/ (y = 0) 1743*) 1744 1745(* Theorem: 0 < m ==> 1 <= m ** n *) 1746(* Proof: 1747 0 < m ==> 0 < m ** n by EXP_POS 1748 or 1 <= m ** n by arithmetic 1749*) 1750val ONE_LE_EXP = store_thm( 1751 "ONE_LE_EXP", 1752 ``!m n. 0 < m ==> 1 <= m ** n``, 1753 metis_tac[EXP_POS, DECIDE``!x. 0 < x <=> 1 <= x``]); 1754 1755(* Theorem: EVEN n ==> !m. m ** n = (SQ m) ** (HALF n) *) 1756(* Proof: 1757 (SQ m) ** (HALF n) 1758 = (m ** 2) ** (HALF n) by notation 1759 = m ** (2 * HALF n) by EXP_EXP_MULT 1760 = m ** n by EVEN_HALF 1761*) 1762val EXP_EVEN = store_thm( 1763 "EXP_EVEN", 1764 ``!n. EVEN n ==> !m. m ** n = (SQ m) ** (HALF n)``, 1765 rpt strip_tac >> 1766 `(SQ m) ** (HALF n) = m ** (2 * HALF n)` by rw[EXP_EXP_MULT] >> 1767 `_ = m ** n` by rw[GSYM EVEN_HALF] >> 1768 rw[]); 1769 1770(* Theorem: ODD n ==> !m. m ** n = m * (SQ m) ** (HALF n) *) 1771(* Proof: 1772 m * (SQ m) ** (HALF n) 1773 = m * (m ** 2) ** (HALF n) by notation 1774 = m * m ** (2 * HALF n) by EXP_EXP_MULT 1775 = m ** (SUC (2 * HALF n)) by EXP 1776 = m ** (2 * HALF n + 1) by ADD1 1777 = m ** n by ODD_HALF 1778*) 1779val EXP_ODD = store_thm( 1780 "EXP_ODD", 1781 ``!n. ODD n ==> !m. m ** n = m * (SQ m) ** (HALF n)``, 1782 rpt strip_tac >> 1783 `m * (SQ m) ** (HALF n) = m * m ** (2 * HALF n)` by rw[EXP_EXP_MULT] >> 1784 `_ = m ** (2 * HALF n + 1)` by rw[GSYM EXP, ADD1] >> 1785 `_ = m ** n` by rw[GSYM ODD_HALF] >> 1786 rw[]); 1787 1788(* An exponentiation identity *) 1789val EXP_THM = save_thm("EXP_THM", CONJ EXP_EVEN EXP_ODD); 1790(* 1791val EXP_THM = |- (!n. EVEN n ==> !m. m ** n = SQ m ** HALF n) /\ 1792 !n. ODD n ==> !m. m ** n = m * SQ m ** HALF n: thm 1793*) 1794(* Next is better *) 1795 1796(* Theorem: m ** n = if n = 0 then 1 else if n = 1 then m else 1797 if EVEN n then (m * m) ** HALF n else m * ((m * m) ** (HALF n)) *) 1798(* Proof: mainly by EXP_EVEN, EXP_ODD. *) 1799val EXP_THM = store_thm( 1800 "EXP_THM", 1801 ``!m n. m ** n = if n = 0 then 1 else if n = 1 then m else 1802 if EVEN n then (m * m) ** HALF n else m * ((m * m) ** (HALF n))``, 1803 metis_tac[EXP_0, EXP_1, EXP_EVEN, EXP_ODD, EVEN_ODD]); 1804 1805(* Theorem: m ** n = 1806 if n = 0 then 1 1807 else if EVEN n then (m * m) ** (HALF n) else m * (m * m) ** (HALF n) *) 1808(* Proof: 1809 If n = 0, to show: 1810 m ** 0 = 1, true by EXP_0 1811 If EVEN n, to show: 1812 m ** n = (m * m) ** (HALF n), true by EXP_EVEN 1813 If ~EVEN n, ODD n, to show: by EVEN_ODD 1814 m ** n = m * (m * m) ** HALF n, true by EXP_ODD 1815*) 1816val EXP_EQN = store_thm( 1817 "EXP_EQN", 1818 ``!m n. m ** n = 1819 if n = 0 then 1 1820 else if EVEN n then (m * m) ** (HALF n) else m * (m * m) ** (HALF n)``, 1821 rw[] >- 1822 rw[Once EXP_EVEN] >> 1823 `ODD n` by metis_tac[EVEN_ODD] >> 1824 rw[Once EXP_ODD]); 1825 1826(* Theorem: m ** n = if n = 0 then 1 else (if EVEN n then 1 else m) * (m * m) ** (HALF n) *) 1827(* Proof: by EXP_EQN *) 1828val EXP_EQN_ALT = store_thm( 1829 "EXP_EQN_ALT", 1830 ``!m n. m ** n = 1831 if n = 0 then 1 1832 else (if EVEN n then 1 else m) * (m * m) ** (HALF n)``, 1833 rw[Once EXP_EQN]); 1834 1835(* Theorem: m ** n = (if n = 0 then 1 else (if EVEN n then 1 else m) * (m ** 2) ** HALF n) *) 1836(* Proof: by EXP_EQN_ALT, EXP_2 *) 1837val EXP_ALT_EQN = store_thm( 1838 "EXP_ALT_EQN", 1839 ``!m n. m ** n = (if n = 0 then 1 else (if EVEN n then 1 else m) * (m ** 2) ** HALF n)``, 1840 metis_tac[EXP_EQN_ALT, EXP_2]); 1841 1842(* Theorem: 1 < m ==> 1843 (b ** n) MOD m = if (n = 0) then 1 1844 else let result = (b * b) ** (HALF n) MOD m 1845 in if EVEN n then result else (b * result) MOD m *) 1846(* Proof: 1847 This is to show: 1848 (1) 1 < m ==> b ** 0 MOD m = 1 1849 b ** 0 MOD m 1850 = 1 MOD m by EXP_0 1851 = 1 by ONE_MOD, 1 < m 1852 (2) EVEN n ==> b ** n MOD m = (b ** 2) ** HALF n MOD m 1853 b ** n MOD m 1854 = (b * b) ** HALF n MOD m by EXP_EVEN 1855 = (b ** 2) ** HALF n MOD m by EXP_2 1856 (3) ~EVEN n ==> b ** n MOD m = (b * (b ** 2) ** HALF n) MOD m 1857 b ** n MOD m 1858 = (b * (b * b) ** HALF n) MOD m by EXP_ODD, EVEN_ODD 1859 = (b * (b ** 2) ** HALF n) MOD m by EXP_2 1860*) 1861val EXP_MOD_EQN = store_thm( 1862 "EXP_MOD_EQN", 1863 ``!b n m. 1 < m ==> 1864 ((b ** n) MOD m = 1865 if (n = 0) then 1 1866 else let result = (b * b) ** (HALF n) MOD m 1867 in if EVEN n then result else (b * result) MOD m)``, 1868 rw[] >- 1869 rw[EXP_0, ONE_MOD] >- 1870 metis_tac[EXP_EVEN, EXP_2] >> 1871 metis_tac[EXP_ODD, EXP_2, EVEN_ODD]); 1872 1873(* Pretty version of EXP_MOD_EQN, same pattern as EXP_EQN_ALT. *) 1874 1875(* Theorem: 1 < m ==> b ** n MOD m = 1876 if n = 0 then 1 else 1877 ((if EVEN n then 1 else b) * ((SQ b ** HALF n) MOD m)) MOD m *) 1878(* Proof: by EXP_MOD_EQN *) 1879val EXP_MOD_ALT = store_thm( 1880 "EXP_MOD_ALT", 1881 ``!b n m. 1 < m ==> b ** n MOD m = 1882 if n = 0 then 1 else 1883 ((if EVEN n then 1 else b) * ((SQ b ** HALF n) MOD m)) MOD m``, 1884 rpt strip_tac >> 1885 imp_res_tac EXP_MOD_EQN >> 1886 last_x_assum (qspecl_then [`n`, `b`] strip_assume_tac) >> 1887 rw[]); 1888 1889(* Theorem: x ** (y ** SUC n) = (x ** y) ** y ** n *) 1890(* Proof: 1891 x ** (y ** SUC n) 1892 = x ** (y * y ** n) by EXP 1893 = (x ** y) ** (y ** n) by EXP_EXP_MULT 1894*) 1895val EXP_EXP_SUC = store_thm( 1896 "EXP_EXP_SUC", 1897 ``!x y n. x ** (y ** SUC n) = (x ** y) ** y ** n``, 1898 rw[EXP, EXP_EXP_MULT]); 1899 1900(* Theorem: 1 + n * m <= (1 + m) ** n *) 1901(* Proof: 1902 By induction on n. 1903 Base: 1 + 0 * m <= (1 + m) ** 0 1904 LHS = 1 + 0 * m = 1 by arithmetic 1905 RHS = (1 + m) ** 0 = 1 by EXP_0 1906 Hence true. 1907 Step: 1 + n * m <= (1 + m) ** n ==> 1908 1 + SUC n * m <= (1 + m) ** SUC n 1909 1 + SUC n * m 1910 = 1 + n * m + m by MULT 1911 <= (1 + m) ** n + m by induction hypothesis 1912 <= (1 + m) ** n + m * (1 + m) ** n by EXP_POS 1913 <= (1 + m) * (1 + m) ** n by RIGHT_ADD_DISTRIB 1914 = (1 + m) ** SUC n by EXP 1915*) 1916val EXP_LOWER_LE_LOW = store_thm( 1917 "EXP_LOWER_LE_LOW", 1918 ``!n m. 1 + n * m <= (1 + m) ** n``, 1919 rpt strip_tac >> 1920 Induct_on `n` >- 1921 rw[EXP_0] >> 1922 `0 < (1 + m) ** n` by rw[] >> 1923 `1 + SUC n * m = 1 + (n * m + m)` by rw[MULT] >> 1924 `_ = 1 + n * m + m` by decide_tac >> 1925 `m <= m * (1 + m) ** n` by rw[] >> 1926 `1 + SUC n * m <= (1 + m) ** n + m * (1 + m) ** n` by decide_tac >> 1927 `(1 + m) ** n + m * (1 + m) ** n = (1 + m) * (1 + m) ** n` by decide_tac >> 1928 `_ = (1 + m) ** SUC n` by rw[EXP] >> 1929 decide_tac); 1930 1931(* Theorem: 0 < m /\ 1 < n ==> 1 + n * m < (1 + m) ** n *) 1932(* Proof: 1933 By induction on n. 1934 Base: 1 < 0 ==> 1 + 0 * m <= (1 + m) ** 0 1935 True since 1 < 0 = F. 1936 Step: 1 < n ==> 1 + n * m < (1 + m) ** n ==> 1937 1 < SUC n ==> 1 + SUC n * m < (1 + m) ** SUC n 1938 Note n <> 0, since SUC 0 = 1 by ONE 1939 If n = 1, 1940 Note m * m <> 0 by MULT_EQ_0, m <> 0 1941 (1 + m) ** SUC 1 1942 = (1 + m) ** 2 by TWO 1943 = 1 + 2 * m + m * m by expansion 1944 > 1 + 2 * m by 0 < m * m 1945 = 1 + (SUC 1) * m 1946 If n <> 1, then 1 < n. 1947 1 + SUC n * m 1948 = 1 + n * m + m by MULT 1949 < (1 + m) ** n + m by induction hypothesis, 1 < n 1950 <= (1 + m) ** n + m * (1 + m) ** n by EXP_POS 1951 <= (1 + m) * (1 + m) ** n by RIGHT_ADD_DISTRIB 1952 = (1 + m) ** SUC n by EXP 1953*) 1954val EXP_LOWER_LT_LOW = store_thm( 1955 "EXP_LOWER_LT_LOW", 1956 ``!n m. 0 < m /\ 1 < n ==> 1 + n * m < (1 + m) ** n``, 1957 rpt strip_tac >> 1958 Induct_on `n` >- 1959 rw[] >> 1960 rpt strip_tac >> 1961 `n <> 0` by fs[] >> 1962 Cases_on `n = 1` >| [ 1963 simp[] >> 1964 `(m + 1) ** 2 = (m + 1) * (m + 1)` by rw[GSYM EXP_2] >> 1965 `_ = m * m + 2 * m + 1` by decide_tac >> 1966 `0 < SQ m` by metis_tac[SQ_EQ_0, NOT_ZERO_LT_ZERO] >> 1967 decide_tac, 1968 `1 < n` by decide_tac >> 1969 `0 < (1 + m) ** n` by rw[] >> 1970 `1 + SUC n * m = 1 + (n * m + m)` by rw[MULT] >> 1971 `_ = 1 + n * m + m` by decide_tac >> 1972 `m <= m * (1 + m) ** n` by rw[] >> 1973 `1 + SUC n * m < (1 + m) ** n + m * (1 + m) ** n` by decide_tac >> 1974 `(1 + m) ** n + m * (1 + m) ** n = (1 + m) * (1 + m) ** n` by decide_tac >> 1975 `_ = (1 + m) ** SUC n` by rw[EXP] >> 1976 decide_tac 1977 ]); 1978 1979(* 1980Note: EXP_LOWER_LE_LOW collects the first two terms of binomial expansion. 1981 but EXP_LOWER_LE_HIGH collects the last two terms of binomial expansion. 1982*) 1983 1984(* Theorem: n * m ** (n - 1) + m ** n <= (1 + m) ** n *) 1985(* Proof: 1986 By induction on n. 1987 Base: 0 * m ** (0 - 1) + m ** 0 <= (1 + m) ** 0 1988 LHS = 0 * m ** (0 - 1) + m ** 0 1989 = 0 + 1 by EXP_0 1990 = 1 1991 <= 1 = (1 + m) ** 0 = RHS by EXP_0 1992 Step: n * m ** (n - 1) + m ** n <= (1 + m) ** n ==> 1993 SUC n * m ** (SUC n - 1) + m ** SUC n <= (1 + m) ** SUC n 1994 If n = 0, 1995 LHS = 1 * m ** 0 + m ** 1 1996 = 1 + m by EXP_0, EXP_1 1997 = (1 + m) ** 1 = RHS by EXP_1 1998 If n <> 0, 1999 Then SUC (n - 1) = n by n <> 0. 2000 LHS = SUC n * m ** (SUC n - 1) + m ** SUC n 2001 = (n + 1) * m ** n + m * m ** n by EXP, ADD1 2002 = (n + 1 + m) * m ** n by arithmetic 2003 = n * m ** n + (1 + m) * m ** n by arithmetic 2004 = n * m ** SUC (n - 1) + (1 + m) * m ** n by SUC (n - 1) = n 2005 = n * m * m ** (n - 1) + (1 + m) * m ** n by EXP 2006 = m * (n * m ** (n - 1)) + (1 + m) * m ** n by arithmetic 2007 <= (1 + m) * (n * m ** (n - 1)) + (1 + m) * m ** n by m < 1 + m 2008 = (1 + m) * (n * m ** (n - 1) + m ** n) by LEFT_ADD_DISTRIB 2009 <= (1 + m) * (1 + m) ** n by induction hypothesis 2010 = (1 + m) ** SUC n by EXP 2011*) 2012val EXP_LOWER_LE_HIGH = store_thm( 2013 "EXP_LOWER_LE_HIGH", 2014 ``!n m. n * m ** (n - 1) + m ** n <= (1 + m) ** n``, 2015 rpt strip_tac >> 2016 Induct_on `n` >- 2017 simp[] >> 2018 Cases_on `n = 0` >- 2019 simp[EXP_0] >> 2020 `SUC (n - 1) = n` by decide_tac >> 2021 simp[EXP] >> 2022 simp[ADD1] >> 2023 `m * m ** n + (n + 1) * m ** n = (m + (n + 1)) * m ** n` by rw[LEFT_ADD_DISTRIB] >> 2024 `_ = (n + (m + 1)) * m ** n` by decide_tac >> 2025 `_ = n * m ** n + (m + 1) * m ** n` by rw[LEFT_ADD_DISTRIB] >> 2026 `_ = n * m ** SUC (n - 1) + (m + 1) * m ** n` by rw[] >> 2027 `_ = n * (m * m ** (n - 1)) + (m + 1) * m ** n` by rw[EXP] >> 2028 `_ = m * (n * m ** (n - 1)) + (m + 1) * m ** n` by decide_tac >> 2029 `m * (n * m ** (n - 1)) + (m + 1) * m ** n <= (m + 1) * (n * m ** (n - 1)) + (m + 1) * m ** n` by decide_tac >> 2030 qabbrev_tac `t = n * m ** (n - 1) + m ** n` >> 2031 `(m + 1) * (n * m ** (n - 1)) + (m + 1) * m ** n = (m + 1) * t` by rw[LEFT_ADD_DISTRIB, Abbr`t`] >> 2032 `t <= (m + 1) ** n` by metis_tac[ADD_COMM] >> 2033 `(m + 1) * t <= (m + 1) * (m + 1) ** n` by rw[] >> 2034 decide_tac); 2035 2036(* Theorem: 1 < n ==> SUC n < 2 ** n *) 2037(* Proof: 2038 Note 1 + n < (1 + 1) ** n by EXP_LOWER_LT_LOW, m = 1 2039 or SUC n < SUC 1 ** n by ADD1 2040 or SUC n < 2 ** n by TWO 2041*) 2042val SUC_X_LT_2_EXP_X = store_thm( 2043 "SUC_X_LT_2_EXP_X", 2044 ``!n. 1 < n ==> SUC n < 2 ** n``, 2045 rpt strip_tac >> 2046 `1 + n * 1 < (1 + 1) ** n` by rw[EXP_LOWER_LT_LOW] >> 2047 fs[]); 2048 2049(* ------------------------------------------------------------------------- *) 2050(* DIVIDES Theorems *) 2051(* ------------------------------------------------------------------------- *) 2052 2053(* arithmeticTheory.LESS_DIV_EQ_ZERO = |- !r n. r < n ==> (r DIV n = 0) *) 2054 2055(* Theorem: 0 < n ==> ((m DIV n = 0) <=> m < n) *) 2056(* Proof: 2057 If part: 0 < n /\ m DIV n = 0 ==> m < n 2058 Since m = m DIV n * n + m MOD n) /\ (m MOD n < n) by DIVISION, 0 < n 2059 so m = 0 * n + m MOD n by m DIV n = 0 2060 = 0 + m MOD n by MULT 2061 = m MOD n by ADD 2062 Since m MOD n < n, m < n. 2063 Only-if part: 0 < n /\ m < n ==> m DIV n = 0 2064 True by LESS_DIV_EQ_ZERO. 2065*) 2066val DIV_EQ_0 = store_thm( 2067 "DIV_EQ_0", 2068 ``!m n. 0 < n ==> ((m DIV n = 0) <=> m < n)``, 2069 rw[EQ_IMP_THM] >- 2070 metis_tac[DIVISION, MULT, ADD] >> 2071 rw[LESS_DIV_EQ_ZERO]); 2072 2073(* Theorem: 0 < n /\ m divides n ==> 0 < (n DIV m) *) 2074(* Proof: 2075 Given 0 < n /\ m divides n, 2076 ==> 0 < m by ZERO_DIVIDES, n <> 0, so m <> 0 2077 and m <= n by DIVIDES_LE 2078 By contradiction, suppose ~(0 < n DIV m). 2079 That means n DIV m = 0 by arithmetic 2080 Thus n < m by DIV_EQ_0 2081 This contradicts m <= n. 2082*) 2083val DIV_POS = store_thm( 2084 "DIV_POS", 2085 ``!m n. 0 < n /\ m divides n ==> 0 < (n DIV m)``, 2086 rpt strip_tac >> 2087 `0 < m /\ m <= n` by metis_tac[ZERO_DIVIDES, NOT_ZERO_LT_ZERO, DIVIDES_LE] >> 2088 spose_not_then strip_assume_tac >> 2089 `n DIV m = 0` by decide_tac >> 2090 `n < m` by rw[GSYM DIV_EQ_0] >> 2091 decide_tac); 2092 2093(* 2094DIV_LE_MONOTONE |- !n x y. 0 < n /\ x <= y ==> x DIV n <= y DIV n 2095DIV_LE_X |- !x y z. 0 < z ==> (y DIV z <= x <=> y < (x + 1) * z) 2096*) 2097 2098(* Theorem: 0 < y /\ x <= y * z ==> x DIV y <= z *) 2099(* Proof: 2100 x <= y * z 2101 ==> x DIV y <= (y * z) DIV y by DIV_LE_MONOTONE, 0 < y 2102 = z by MULT_TO_DIV 2103*) 2104val DIV_LE = store_thm( 2105 "DIV_LE", 2106 ``!x y z. 0 < y /\ x <= y * z ==> x DIV y <= z``, 2107 metis_tac[DIV_LE_MONOTONE, MULT_TO_DIV]); 2108 2109(* Theorem: 0 < n ==> !x y. (x * n = y) ==> (x = y DIV n) *) 2110(* Proof: 2111 x = (x * n + 0) DIV n by DIV_MULT, 0 < n 2112 = (x * n) DIV n by ADD_0 2113*) 2114val DIV_SOLVE = store_thm( 2115 "DIV_SOLVE", 2116 ``!n. 0 < n ==> !x y. (x * n = y) ==> (x = y DIV n)``, 2117 metis_tac[DIV_MULT, ADD_0]); 2118 2119(* Theorem: 0 < n ==> !x y. (n * x = y) ==> (x = y DIV n) *) 2120(* Proof: by DIV_SOLVE, MULT_COMM *) 2121val DIV_SOLVE_COMM = store_thm( 2122 "DIV_SOLVE_COMM", 2123 ``!n. 0 < n ==> !x y. (n * x = y) ==> (x = y DIV n)``, 2124 rw[DIV_SOLVE]); 2125 2126(* Theorem: 1 < n ==> (1 DIV n = 0) *) 2127(* Proof: 2128 Since 1 = (1 DIV n) * n + (1 MOD n) by DIVISION, 0 < n. 2129 and 1 MOD n = 1 by ONE_MOD, 1 < n. 2130 thus (1 DIV n) * n = 0 by arithmetic 2131 or 1 DIV n = 0 since n <> 0 by MULT_EQ_0 2132*) 2133val ONE_DIV = store_thm( 2134 "ONE_DIV", 2135 ``!n. 1 < n ==> (1 DIV n = 0)``, 2136 rpt strip_tac >> 2137 `0 < n /\ n <> 0` by decide_tac >> 2138 `1 = (1 DIV n) * n + (1 MOD n)` by rw[DIVISION] >> 2139 `_ = (1 DIV n) * n + 1` by rw[ONE_MOD] >> 2140 `(1 DIV n) * n = 0` by decide_tac >> 2141 metis_tac[MULT_EQ_0]); 2142 2143(* Theorem: ODD n ==> !m. m divides n ==> ODD m *) 2144(* Proof: 2145 Since m divides n 2146 ==> ?q. n = q * m by divides_def 2147 By contradiction, suppose ~ODD m. 2148 Then EVEN m by ODD_EVEN 2149 and EVEN (q * m) = EVEN n by EVEN_MULT 2150 or ~ODD n by ODD_EVEN 2151 This contradicts with ODD n. 2152*) 2153val DIVIDES_ODD = store_thm( 2154 "DIVIDES_ODD", 2155 ``!n. ODD n ==> !m. m divides n ==> ODD m``, 2156 metis_tac[divides_def, EVEN_MULT, EVEN_ODD]); 2157 2158(* Note: For EVEN n, m divides n cannot conclude EVEN m. 2159Example: EVEN 2 or ODD 3 both divides EVEN 6. 2160*) 2161 2162(* Theorem: EVEN m ==> !n. m divides n ==> EVEN n*) 2163(* Proof: 2164 Since m divides n 2165 ==> ?q. n = q * m by divides_def 2166 Given EVEN m 2167 Then EVEN (q * m) = n by EVEN_MULT 2168*) 2169val DIVIDES_EVEN = store_thm( 2170 "DIVIDES_EVEN", 2171 ``!m. EVEN m ==> !n. m divides n ==> EVEN n``, 2172 metis_tac[divides_def, EVEN_MULT]); 2173 2174(* Theorem: n divides m <=> m MOD n = 0 *) 2175(* Proof: 2176 if part: n divides m ==> m MOD n = 0 2177 n divides m 2178 ==> ?q. m = q * n by divides_def 2179 ==> m MOD n 2180 = (q * n) MOD n by substitution 2181 = 0 by MOD_EQ_0 2182 only-if part: m MOD n = 0 ==> n divides m 2183 m = (m DIV n) * n + (m MOD n) by DIVISION 2184 = (m DIV n) * n by ADD_0 and given 2185 Hence n divides m by divides_def 2186 Or, 2187 m MOD n = 0 2188 <=> ?d. m = d * n by MOD_EQ_0_DIVISOR, 0 < n 2189 <=> n divides m by divides_def 2190*) 2191val DIVIDES_MOD_0 = store_thm( 2192 "DIVIDES_MOD_0", 2193 ``!n. 0 < n ==> !m. n divides m <=> (m MOD n = 0)``, 2194 metis_tac[MOD_EQ_0_DIVISOR, divides_def]); 2195 2196(* Theorem: EVEN n = 2 divides n *) 2197(* Proof: 2198 EVEN n 2199 <=> n MOD 2 = 0 by EVEN_MOD2 2200 <=> 2 divides n by DIVIDES_MOD_0, 0 < 2 2201*) 2202val EVEN_ALT = store_thm( 2203 "EVEN_ALT", 2204 ``!n. EVEN n = 2 divides n``, 2205 rw[EVEN_MOD2, DIVIDES_MOD_0]); 2206 2207(* Theorem: ODD n = ~(2 divides n) *) 2208(* Proof: 2209 Note n MOD 2 < 2 by MOD_LESS 2210 and !x. x < 2 <=> (x = 0) \/ (x = 1) by arithmetic 2211 ODD n 2212 <=> n MOD 2 = 1 by ODD_MOD2 2213 <=> ~(2 divides n) by DIVIDES_MOD_0, 0 < 2 2214 Or, 2215 ODD n = ~(EVEN n) by ODD_EVEN 2216 = ~(2 divides n) by EVEN_ALT 2217*) 2218val ODD_ALT = store_thm( 2219 "ODD_ALT", 2220 ``!n. ODD n = ~(2 divides n)``, 2221 metis_tac[EVEN_ODD, EVEN_ALT]); 2222 2223(* Theorem: 0 < n ==> !q. (q DIV n) * n <= q *) 2224(* Proof: 2225 Since q = (q DIV n) * n + q MOD n by DIVISION 2226 Thus (q DIV n) * n <= q by discarding remainder 2227*) 2228val DIV_MULT_LE = store_thm( 2229 "DIV_MULT_LE", 2230 ``!n. 0 < n ==> !q. (q DIV n) * n <= q``, 2231 rpt strip_tac >> 2232 `q = (q DIV n) * n + q MOD n` by rw[DIVISION] >> 2233 decide_tac); 2234 2235(* Theorem: 0 < n ==> !q. n divides q <=> ((q DIV n) * n = q) *) 2236(* Proof: 2237 If part: n divides q ==> q DIV n * n = q 2238 q = (q DIV n) * n + q MOD n by DIVISION 2239 = (q DIV n) * n + 0 by MOD_EQ_0_DIVISOR, divides_def 2240 = (q DIV n) * n by ADD_0 2241 Only-if part: q DIV n * n = q ==> n divides q 2242 True by divides_def 2243*) 2244val DIV_MULT_EQ = store_thm( 2245 "DIV_MULT_EQ", 2246 ``!n. 0 < n ==> !q. n divides q <=> ((q DIV n) * n = q)``, 2247 metis_tac[divides_def, DIVISION, MOD_EQ_0_DIVISOR, ADD_0]); 2248(* same as DIVIDES_EQN below *) 2249 2250(* Theorem: 0 < m ==> m * (n DIV m) <= n /\ n < m * SUC (n DIV m) *) 2251(* Proof: 2252 Note n = n DIV m * m + n MOD m /\ 2253 n MOD m < m by DIVISION 2254 Thus m * (n DIV m) <= n by MULT_COMM 2255 and n < m * (n DIV m) + m 2256 = m * (n DIV m + 1) by LEFT_ADD_DISTRIB 2257 = m * SUC (n DIV m) by ADD1 2258*) 2259val DIV_MULT_LESS_EQ = store_thm( 2260 "DIV_MULT_LESS_EQ", 2261 ``!m n. 0 < m ==> m * (n DIV m) <= n /\ n < m * SUC (n DIV m)``, 2262 ntac 3 strip_tac >> 2263 `(n = n DIV m * m + n MOD m) /\ n MOD m < m` by rw[DIVISION] >> 2264 `n < m * (n DIV m) + m` by decide_tac >> 2265 `m * (n DIV m) + m = m * (SUC (n DIV m))` by rw[ADD1] >> 2266 decide_tac); 2267 2268(* Theorem: 0 < x /\ 0 < y /\ x <= y ==> !n. n DIV y <= n DIV x *) 2269(* Proof: 2270 If n DIV y = 0, 2271 Then 0 <= n DIV x is trivially true. 2272 If n DIV y <> 0, 2273 (n DIV y) * x <= (n DIV y) * y by LE_MULT_LCANCEL, x <= y, n DIV y <> 0 2274 <= n by DIV_MULT_LE 2275 Hence (n DIV y) * x <= n by LESS_EQ_TRANS 2276 Then ((n DIV y) * x) DIV x <= n DIV x by DIV_LE_MONOTONE 2277 or n DIV y <= n DIV x by MULT_DIV 2278*) 2279val DIV_LE_MONOTONE_REVERSE = store_thm( 2280 "DIV_LE_MONOTONE_REVERSE", 2281 ``!x y. 0 < x /\ 0 < y /\ x <= y ==> !n. n DIV y <= n DIV x``, 2282 rpt strip_tac >> 2283 Cases_on `n DIV y = 0` >- 2284 decide_tac >> 2285 `(n DIV y) * x <= (n DIV y) * y` by rw[LE_MULT_LCANCEL] >> 2286 `(n DIV y) * y <= n` by rw[DIV_MULT_LE] >> 2287 `(n DIV y) * x <= n` by decide_tac >> 2288 `((n DIV y) * x) DIV x <= n DIV x` by rw[DIV_LE_MONOTONE] >> 2289 metis_tac[MULT_DIV]); 2290 2291(* Theorem: n divides m <=> (m = (m DIV n) * n) *) 2292(* Proof: 2293 Since n divides m <=> m MOD n = 0 by DIVIDES_MOD_0 2294 and m = (m DIV n) * n + (m MOD n) by DIVISION 2295 If part: n divides m ==> m = m DIV n * n 2296 This is true by ADD_0 2297 Only-if part: m = m DIV n * n ==> n divides m 2298 Since !x y. x + y = x <=> y = 0 by ADD_INV_0 2299 The result follows. 2300*) 2301val DIVIDES_EQN = store_thm( 2302 "DIVIDES_EQN", 2303 ``!n. 0 < n ==> !m. n divides m <=> (m = (m DIV n) * n)``, 2304 metis_tac[DIVISION, DIVIDES_MOD_0, ADD_0, ADD_INV_0]); 2305 2306(* Theorem: 0 < n ==> !m. n divides m <=> (m = n * (m DIV n)) *) 2307(* Proof: vy DIVIDES_EQN, MULT_COMM *) 2308val DIVIDES_EQN_COMM = store_thm( 2309 "DIVIDES_EQN_COMM", 2310 ``!n. 0 < n ==> !m. n divides m <=> (m = n * (m DIV n))``, 2311 rw_tac std_ss[DIVIDES_EQN, MULT_COMM]); 2312 2313(* Theorem: 0 < n /\ n <= m ==> ((m - n) DIV n = m DIV n - 1) *) 2314(* Proof: 2315 Apply DIV_SUB |> GEN_ALL |> SPEC ``1`` |> REWRITE_RULE[MULT_RIGHT_1]; 2316 val it = |- !n m. 0 < n /\ n <= m ==> ((m - n) DIV n = m DIV n - 1): thm 2317*) 2318val SUB_DIV = save_thm("SUB_DIV", 2319 DIV_SUB |> GEN ``n:num`` |> GEN ``m:num`` |> GEN ``q:num`` |> SPEC ``1`` |> REWRITE_RULE[MULT_RIGHT_1]); 2320(* val SUB_DIV = |- !m n. 0 < n /\ n <= m ==> ((m - n) DIV n = m DIV n - 1): thm *) 2321 2322 2323(* Note: 2324SUB_DIV |- !m n. 0 < n /\ n <= m ==> (m - n) DIV n = m DIV n - 1 2325SUB_MOD |- !m n. 0 < n /\ n <= m ==> (m - n) MOD n = m MOD n 2326*) 2327 2328(* Theorem: 0 < n ==> (m - n) DIV n = if m < n then 0 else (m DIV n - 1) *) 2329(* Proof: 2330 If m < n, then m - n = 0, so (m - n) DIV n = 0 by ZERO_DIV 2331 Otherwise, n <= m, and (m - n) DIV n = m DIV n - 1 by SUB_DIV 2332*) 2333val SUB_DIV_EQN = store_thm( 2334 "SUB_DIV_EQN", 2335 ``!m n. 0 < n ==> ((m - n) DIV n = if m < n then 0 else (m DIV n - 1))``, 2336 rw[SUB_DIV] >> 2337 `m - n = 0` by decide_tac >> 2338 rw[ZERO_DIV]); 2339 2340(* Theorem: 0 < n ==> (m - n) MOD n = if m < n then 0 else m MOD n *) 2341(* Proof: 2342 If m < n, then m - n = 0, so (m - n) MOD n = 0 by ZERO_MOD 2343 Otherwise, n <= m, and (m - n) MOD n = m MOD n by SUB_MOD 2344*) 2345val SUB_MOD_EQN = store_thm( 2346 "SUB_MOD_EQN", 2347 ``!m n. 0 < n ==> ((m - n) MOD n = if m < n then 0 else m MOD n)``, 2348 rw[SUB_MOD]); 2349 2350(* 2351Note: !n. 0 < n ==> !k m. (m MOD n = 0) ==> ((k * n = m) <=> (k = m DIV n)) is almost MULT_EQ_DIV, 2352 but actually DIVIDES_EQN, DIVIDES_MOD_0, EQ_MULT_RCANCEL. See below. 2353Note: !n. 0 < n ==> !k m. (m MOD n = 0) ==> (k * n <= m <=> k <= m DIV n) is X_LE_DIV, no m MOD n = 0. 2354Note: !n. 0 < n ==> !k m. (m MOD n = 0) ==> ((k + 1) * n <= m <=> k < m DIV n) is X_LT_DIV, no m MOD n = 0. 2355Note: !n. 0 < n ==> !k m. (m MOD n = 0) ==> (k * n < m <=> k < m DIV n) is below next. 2356*) 2357 2358(* Theorem: 0 < n ==> !k m. (m MOD n = 0) ==> ((k * n = m) <=> (k = m DIV n)) *) 2359(* Proof: 2360 Note m MOD n = 0 2361 ==> n divides m by DIVIDES_MOD_0, 0 < n 2362 ==> m = (m DIV n) * n by DIVIDES_EQN, 0 < n 2363 k * n = m 2364 <=> k * n = (m DIV n) * n by above 2365 <=> k = (m DIV n) by EQ_MULT_RCANCEL, n <> 0. 2366*) 2367val DIV_EQ_MULT = store_thm( 2368 "DIV_EQ_MULT", 2369 ``!n. 0 < n ==> !k m. (m MOD n = 0) ==> ((k * n = m) <=> (k = m DIV n))``, 2370 rpt strip_tac >> 2371 `n <> 0` by decide_tac >> 2372 `m = (m DIV n) * n` by rw[GSYM DIVIDES_EQN, DIVIDES_MOD_0] >> 2373 metis_tac[EQ_MULT_RCANCEL]); 2374 2375(* Theorem: 0 < n ==> !k m. (m MOD n = 0) ==> (k * n < m <=> k < m DIV n) *) 2376(* Proof: 2377 k * n < m 2378 <=> k * n < (m DIV n) * n by DIVIDES_EQN, DIVIDES_MOD_0, 0 < n 2379 <=> k < m DIV n by LT_MULT_RCANCEL, n <> 0 2380*) 2381val MULT_LT_DIV = store_thm( 2382 "MULT_LT_DIV", 2383 ``!n. 0 < n ==> !k m. (m MOD n = 0) ==> (k * n < m <=> k < m DIV n)``, 2384 metis_tac[DIVIDES_EQN, DIVIDES_MOD_0, LT_MULT_RCANCEL, NOT_ZERO_LT_ZERO]); 2385 2386(* Theorem: 0 < n ==> !k m. (m MOD n = 0) ==> (m <= n * k <=> m DIV n <= k) *) 2387(* Proof: 2388 m <= n * k 2389 <=> (m DIV n) * n <= n * k by DIVIDES_EQN, DIVIDES_MOD_0, 0 < n 2390 <=> (m DIV n) * n <= k * n by MULT_COMM 2391 <=> m DIV n <= k by LE_MULT_RCANCEL, n <> 0 2392*) 2393val LE_MULT_LE_DIV = store_thm( 2394 "LE_MULT_LE_DIV", 2395 ``!n. 0 < n ==> !k m. (m MOD n = 0) ==> (m <= n * k <=> m DIV n <= k)``, 2396 metis_tac[DIVIDES_EQN, DIVIDES_MOD_0, MULT_COMM, LE_MULT_RCANCEL, NOT_ZERO_LT_ZERO]); 2397 2398(* Theorem: 0 < m ==> ((n DIV m = 0) /\ (n MOD m = 0) <=> (n = 0)) *) 2399(* Proof: 2400 If part: (n DIV m = 0) /\ (n MOD m = 0) ==> (n = 0) 2401 Note n DIV m = 0 ==> n < m by DIV_EQ_0 2402 Thus n MOD m = n by LESS_MOD 2403 or n = 0 2404 Only-if part: 0 DIV m = 0 by ZERO_DIV 2405 0 MOD m = 0 by ZERO_MOD 2406*) 2407val DIV_MOD_EQ_0 = store_thm( 2408 "DIV_MOD_EQ_0", 2409 ``!m n. 0 < m ==> ((n DIV m = 0) /\ (n MOD m = 0) <=> (n = 0))``, 2410 rpt strip_tac >> 2411 rw[EQ_IMP_THM] >- 2412 metis_tac[DIV_EQ_0, LESS_MOD] >> 2413 rw[ZERO_DIV]); 2414 2415(* Theorem: 0 < m /\ 0 < n /\ (n MOD m = 0) ==> n DIV (SUC m) < n DIV m *) 2416(* Proof: 2417 Note n = n DIV (SUC m) * (SUC m) + n MOD (SUC m) by DIVISION 2418 = n DIV m * m + n MOD m by DIVISION 2419 = n DIV m * m by n MOD m = 0 2420 Thus n DIV SUC m * SUC m <= n DIV m * m by arithmetic 2421 Note m < SUC m by LESS_SUC 2422 and n DIV m <> 0, or 0 < n DIV m by DIV_MOD_EQ_0 2423 Thus n DIV (SUC m) < n DIV m by LE_IMP_REVERSE_LT 2424*) 2425val DIV_LT_SUC = store_thm( 2426 "DIV_LT_SUC", 2427 ``!m n. 0 < m /\ 0 < n /\ (n MOD m = 0) ==> n DIV (SUC m) < n DIV m``, 2428 rpt strip_tac >> 2429 `n DIV m * m = n` by metis_tac[DIVISION, ADD_0] >> 2430 `_ = n DIV (SUC m) * (SUC m) + n MOD (SUC m)` by metis_tac[DIVISION, SUC_POS] >> 2431 `n DIV SUC m * SUC m <= n DIV m * m` by decide_tac >> 2432 `m < SUC m` by decide_tac >> 2433 `0 < n DIV m` by metis_tac[DIV_MOD_EQ_0, NOT_ZERO_LT_ZERO] >> 2434 metis_tac[LE_IMP_REVERSE_LT]); 2435 2436(* Theorem: 0 < x /\ 0 < y /\ x < y ==> !n. 0 < n /\ (n MOD x = 0) ==> n DIV y < n DIV x *) 2437(* Proof: 2438 Note x < y ==> SUC x <= y by arithmetic 2439 Thus n DIV y <= n DIV (SUC x) by DIV_LE_MONOTONE_REVERSE 2440 But 0 < x /\ 0 < n /\ (n MOD x = 0) by given 2441 ==> n DIV (SUC x) < n DIV x by DIV_LT_SUC 2442 Hence n DIV y < n DIV x by inequalities 2443*) 2444val DIV_LT_MONOTONE_REVERSE = store_thm( 2445 "DIV_LT_MONOTONE_REVERSE", 2446 ``!x y. 0 < x /\ 0 < y /\ x < y ==> !n. 0 < n /\ (n MOD x = 0) ==> n DIV y < n DIV x``, 2447 rpt strip_tac >> 2448 `SUC x <= y` by decide_tac >> 2449 `n DIV y <= n DIV (SUC x)` by rw[DIV_LE_MONOTONE_REVERSE] >> 2450 `n DIV (SUC x) < n DIV x` by rw[DIV_LT_SUC] >> 2451 decide_tac); 2452 2453(* Theorem: 0 < n /\ a ** n divides b ==> a divides b *) 2454(* Proof: 2455 Note ?k. n = SUC k by num_CASES, n <> 0 2456 and ?q. b = q * (a ** n) by divides_def 2457 = q * (a * a ** k) by EXP 2458 = (q * a ** k) * a by arithmetic 2459 Thus a divides b by divides_def 2460*) 2461val EXP_DIVIDES = store_thm( 2462 "EXP_DIVIDES", 2463 ``!a b n. 0 < n /\ a ** n divides b ==> a divides b``, 2464 rpt strip_tac >> 2465 `?k. n = SUC k` by metis_tac[num_CASES, NOT_ZERO_LT_ZERO] >> 2466 `?q. b = q * a ** n` by rw[GSYM divides_def] >> 2467 `_ = q * (a * a ** k)` by rw[EXP] >> 2468 `_ = (q * a ** k) * a` by decide_tac >> 2469 metis_tac[divides_def]); 2470 2471(* Theorem: prime a ==> a divides b iff a divides b ** n for any n *) 2472(* Proof: 2473 by induction on n. 2474 Base case: 0 < 0 ==> (a divides b <=> a divides (b ** 0)) 2475 True since 0 < 0 is False. 2476 Step case: 0 < n ==> (a divides b <=> a divides (b ** n)) ==> 2477 0 < SUC n ==> (a divides b <=> a divides (b ** SUC n)) 2478 i.e. 0 < n ==> (a divides b <=> a divides (b ** n))==> 2479 a divides b <=> a divides (b * b ** n) by EXP 2480 If n = 0, b ** 0 = 1 by EXP 2481 Hence true. 2482 If n <> 0, 0 < n, 2483 If part: a divides b /\ 0 < n ==> (a divides b <=> a divides (b ** n)) ==> a divides (b ** n) 2484 True by DIVIDES_MULT. 2485 Only-if part: a divides (b * b ** n) /\ 0 < n ==> (a divides b <=> a divides (b ** n)) ==> a divides (b ** n) 2486 Since prime a, a divides b, or a divides (b ** n) by P_EUCLIDES 2487 Either case is true. 2488*) 2489val DIVIDES_EXP_BASE = store_thm( 2490 "DIVIDES_EXP_BASE", 2491 ``!a b n. prime a /\ 0 < n ==> (a divides b <=> a divides (b ** n))``, 2492 rpt strip_tac >> 2493 Induct_on `n` >- 2494 rw[] >> 2495 rw[EXP] >> 2496 Cases_on `n = 0` >- 2497 rw[EXP] >> 2498 `0 < n` by decide_tac >> 2499 rw[EQ_IMP_THM] >- 2500 metis_tac[DIVIDES_MULT] >> 2501 `a divides b \/ a divides (b ** n)` by rw[P_EUCLIDES] >> 2502 metis_tac[]); 2503 2504(* Theorem: n divides m ==> !k. n divides (k * m) *) 2505(* Proof: 2506 n divides m ==> ?q. m = q * n by divides_def 2507 Hence k * m = k * (q * n) 2508 = (k * q) * n by MULT_ASSOC 2509 or n divides (k * m) by divides_def 2510*) 2511val DIVIDES_MULTIPLE = store_thm( 2512 "DIVIDES_MULTIPLE", 2513 ``!m n. n divides m ==> !k. n divides (k * m)``, 2514 metis_tac[divides_def, MULT_ASSOC]); 2515 2516(* Theorem: k <> 0 ==> (m divides n <=> (k * m) divides (k * n)) *) 2517(* Proof: 2518 m divides n 2519 <=> ?q. n = q * m by divides_def 2520 <=> ?q. k * n = k * (q * m) by EQ_MULT_LCANCEL, k <> 0 2521 <=> ?q. k * n = q * (k * m) by MULT_ASSOC, MULT_COMM 2522 <=> (k * m) divides (k * n) by divides_def 2523*) 2524val DIVIDES_MULTIPLE_IFF = store_thm( 2525 "DIVIDES_MULTIPLE_IFF", 2526 ``!m n k. k <> 0 ==> (m divides n <=> (k * m) divides (k * n))``, 2527 rpt strip_tac >> 2528 `m divides n <=> ?q. n = q * m` by rw[GSYM divides_def] >> 2529 `_ = ?q. (k * n = k * (q * m))` by rw[EQ_MULT_LCANCEL] >> 2530 metis_tac[divides_def, MULT_COMM, MULT_ASSOC]); 2531 2532(* Theorem: 0 < n /\ n divides m ==> m = n * (m DIV n) *) 2533(* Proof: 2534 n divides m <=> m MOD n = 0 by DIVIDES_MOD_0 2535 m = (m DIV n) * n + (m MOD n) by DIVISION 2536 = (m DIV n) * n by above 2537 = n * (m DIV n) by MULT_COMM 2538*) 2539val DIVIDES_FACTORS = store_thm( 2540 "DIVIDES_FACTORS", 2541 ``!m n. 0 < n /\ n divides m ==> (m = n * (m DIV n))``, 2542 metis_tac[DIVISION, DIVIDES_MOD_0, ADD_0, MULT_COMM]); 2543 2544(* Theorem: 0 < n /\ n divides m ==> (m DIV n) divides m *) 2545(* Proof: 2546 By DIVIDES_FACTORS: m = (m DIV n) * n 2547 Hence (m DIV n) | m by divides_def 2548*) 2549val DIVIDES_COFACTOR = store_thm( 2550 "DIVIDES_COFACTOR", 2551 ``!m n. 0 < n /\ n divides m ==> (m DIV n) divides m``, 2552 metis_tac[DIVIDES_FACTORS, divides_def]); 2553 2554(* Theorem: n divides q ==> p * (q DIV n) = (p * q) DIV n *) 2555(* Proof: 2556 n divides q ==> q MOD n = 0 by DIVIDES_MOD_0 2557 p * q = p * ((q DIV n) * n + q MOD n) by DIVISION 2558 = p * ((q DIV n) * n) by ADD_0 2559 = p * (q DIV n) * n by MULT_ASSOC 2560 = p * (q DIV n) * n + 0 by ADD_0 2561 Hence (p * q) DIV n = p * (q DIV n) by DIV_UNIQUE, 0 < n: 2562 |- !n k q. (?r. (k = q * n + r) /\ r < n) ==> (k DIV n = q) 2563*) 2564val MULTIPLY_DIV = store_thm( 2565 "MULTIPLY_DIV", 2566 ``!n p q. 0 < n /\ n divides q ==> (p * (q DIV n) = (p * q) DIV n)``, 2567 rpt strip_tac >> 2568 `q MOD n = 0` by rw[GSYM DIVIDES_MOD_0] >> 2569 `p * q = p * ((q DIV n) * n)` by metis_tac[DIVISION, ADD_0] >> 2570 `_ = p * (q DIV n) * n + 0` by rw[MULT_ASSOC] >> 2571 metis_tac[DIV_UNIQUE]); 2572 2573(* Note: The condition: n divides q is important: 2574> EVAL ``5 * (10 DIV 3)``; 2575val it = |- 5 * (10 DIV 3) = 15: thm 2576> EVAL ``(5 * 10) DIV 3``; 2577val it = |- 5 * 10 DIV 3 = 16: thm 2578*) 2579 2580(* Theorem: 0 < n /\ m divides n ==> !x. (x MOD n) MOD m = x MOD m *) 2581(* Proof: 2582 Note 0 < m by ZERO_DIVIDES, 0 < n 2583 Given divides m n ==> ?q. n = q * m by divides_def 2584 Since x = (x DIV n) * n + (x MOD n) by DIVISION 2585 = (x DIV n) * (q * m) + (x MOD n) by above 2586 = ((x DIV n) * q) * m + (x MOD n) by MULT_ASSOC 2587 Hence x MOD m 2588 = ((x DIV n) * q) * m + (x MOD n)) MOD m by above 2589 = (((x DIV n) * q * m) MOD m + (x MOD n) MOD m) MOD m by MOD_PLUS 2590 = (0 + (x MOD n) MOD m) MOD m by MOD_EQ_0 2591 = (x MOD n) MOD m by ADD, MOD_MOD 2592*) 2593val DIVIDES_MOD_MOD = store_thm( 2594 "DIVIDES_MOD_MOD", 2595 ``!m n. 0 < n /\ m divides n ==> !x. (x MOD n) MOD m = x MOD m``, 2596 rpt strip_tac >> 2597 `0 < m` by metis_tac[ZERO_DIVIDES, NOT_ZERO] >> 2598 `?q. n = q * m` by rw[GSYM divides_def] >> 2599 `x MOD m = ((x DIV n) * n + (x MOD n)) MOD m` by rw[GSYM DIVISION] >> 2600 `_ = (((x DIV n) * q) * m + (x MOD n)) MOD m` by rw[MULT_ASSOC] >> 2601 `_ = (((x DIV n) * q * m) MOD m + (x MOD n) MOD m) MOD m` by rw[MOD_PLUS] >> 2602 rw[MOD_EQ_0, MOD_MOD]); 2603 2604(* Theorem: m divides n <=> (m * k) divides (n * k) *) 2605(* Proof: by divides_def and EQ_MULT_LCANCEL. *) 2606val DIVIDES_CANCEL = store_thm( 2607 "DIVIDES_CANCEL", 2608 ``!k. 0 < k ==> !m n. m divides n <=> (m * k) divides (n * k)``, 2609 rw[divides_def] >> 2610 `k <> 0` by decide_tac >> 2611 `!q. (q * m) * k = q * (m * k)` by rw_tac arith_ss[] >> 2612 metis_tac[EQ_MULT_LCANCEL, MULT_COMM]); 2613 2614(* Theorem: m divides n ==> (k * m) divides (k * n) *) 2615(* Proof: 2616 m divides n 2617 ==> ?q. n = q * m by divides_def 2618 So k * n = k * (q * m) 2619 = (k * q) * m by MULT_ASSOC 2620 = (q * k) * m by MULT_COMM 2621 = q * (k * m) by MULT_ASSOC 2622 Hence (k * m) divides (k * n) by divides_def 2623*) 2624val DIVIDES_CANCEL_COMM = store_thm( 2625 "DIVIDES_CANCEL_COMM", 2626 ``!m n k. m divides n ==> (k * m) divides (k * n)``, 2627 metis_tac[MULT_ASSOC, MULT_COMM, divides_def]); 2628 2629(* Theorem: 0 < n /\ 0 < m ==> !x. n divides x ==> ((m * x) DIV (m * n) = x DIV n) *) 2630(* Proof: 2631 n divides x ==> x = n * (x DIV n) by DIVIDES_FACTORS 2632 or m * x = (m * n) * (x DIV n) by MULT_ASSOC 2633 n divides x 2634 ==> divides (m * n) (m * x) by DIVIDES_CANCEL_COMM 2635 ==> m * x = (m * n) * ((m * x) DIV (m * n)) by DIVIDES_FACTORS 2636 Equating expressions for m * x, 2637 (m * n) * (x DIV n) = (m * n) * ((m * x) DIV (m * n)) 2638 or x DIV n = (m * x) DIV (m * n) by MULT_LEFT_CANCEL 2639*) 2640val DIV_COMMON_FACTOR = store_thm( 2641 "DIV_COMMON_FACTOR", 2642 ``!m n. 0 < n /\ 0 < m ==> !x. n divides x ==> ((m * x) DIV (m * n) = x DIV n)``, 2643 rpt strip_tac >> 2644 `!n. n <> 0 <=> 0 < n` by decide_tac >> 2645 `0 < m * n` by metis_tac[MULT_EQ_0] >> 2646 metis_tac[DIVIDES_CANCEL_COMM, DIVIDES_FACTORS, MULT_ASSOC, MULT_LEFT_CANCEL]); 2647 2648(* Theorem: 0 < n /\ 0 < m /\ 0 < m DIV n /\ 2649 n divides m /\ m divides x /\ (m DIV n) divides x ==> 2650 (x DIV (m DIV n) = n * (x DIV m)) *) 2651(* Proof: 2652 x DIV (m DIV n) 2653 = (n * x) DIV (n * (m DIV n)) by DIV_COMMON_FACTOR, (m DIV n) divides x, 0 < m DIV n. 2654 = (n * x) DIV m by DIVIDES_FACTORS, n divides m, 0 < n. 2655 = n * (x DIV m) by MULTIPLY_DIV, m divides x, 0 < m. 2656*) 2657val DIV_DIV_MULT = store_thm( 2658 "DIV_DIV_MULT", 2659 ``!m n x. 0 < n /\ 0 < m /\ 0 < m DIV n /\ 2660 n divides m /\ m divides x /\ (m DIV n) divides x ==> 2661 (x DIV (m DIV n) = n * (x DIV m))``, 2662 metis_tac[DIV_COMMON_FACTOR, DIVIDES_FACTORS, MULTIPLY_DIV]); 2663 2664(* ------------------------------------------------------------------------- *) 2665(* Basic Divisibility *) 2666(* ------------------------------------------------------------------------- *) 2667 2668(* Theorem: 0 < m /\ n divides m ==> !t. m divides (t * n) <=> (m DIV n) divides t *) 2669(* Proof: 2670 Let k = m DIV n. 2671 Since m <> 0, n divides m ==> n <> 0 by ZERO_DIVIDES 2672 Thus m = k * n by DIVIDES_EQN, 0 < n 2673 so 0 < k by MULT, NOT_ZERO_LT_ZERO 2674 Hence k * n divides t * n <=> k divides t by DIVIDES_CANCEL, 0 < k 2675*) 2676val dividend_divides_divisor_multiple = store_thm( 2677 "dividend_divides_divisor_multiple", 2678 ``!m n. 0 < m /\ n divides m ==> !t. m divides (t * n) <=> (m DIV n) divides t``, 2679 rpt strip_tac >> 2680 qabbrev_tac `k = m DIV n` >> 2681 `0 < n` by metis_tac[ZERO_DIVIDES, NOT_ZERO_LT_ZERO] >> 2682 `m = k * n` by rw[GSYM DIVIDES_EQN, Abbr`k`] >> 2683 `0 < k` by metis_tac[MULT, NOT_ZERO_LT_ZERO] >> 2684 metis_tac[DIVIDES_CANCEL]); 2685 2686(* Theorem: 0 < n /\ m divides n ==> 0 < m *) 2687(* Proof: 2688 Since 0 < n means n <> 0, 2689 then m divides n ==> m <> 0 by ZERO_DIVIDES 2690 or 0 < m by NOT_ZERO_LT_ZERO 2691*) 2692val divisor_pos = store_thm( 2693 "divisor_pos", 2694 ``!m n. 0 < n /\ m divides n ==> 0 < m``, 2695 metis_tac[ZERO_DIVIDES, NOT_ZERO_LT_ZERO]); 2696 2697(* Theorem: 0 < n /\ m divides n ==> 0 < m /\ m <= n *) 2698(* Proof: 2699 Since 0 < n /\ m divides n, 2700 then 0 < m by divisor_pos 2701 and m <= n by DIVIDES_LE 2702*) 2703val divides_pos = store_thm( 2704 "divides_pos", 2705 ``!m n. 0 < n /\ m divides n ==> 0 < m /\ m <= n``, 2706 metis_tac[divisor_pos, DIVIDES_LE]); 2707 2708(* Theorem: 0 < n /\ m divides n ==> (n DIV (n DIV m) = m) *) 2709(* Proof: 2710 Since 0 < n /\ m divides n, 0 < m by divisor_pos 2711 Hence n = (n DIV m) * m by DIVIDES_EQN, 0 < m 2712 Note 0 < n DIV m, otherwise contradicts 0 < n by MULT 2713 Now n = m * (n DIV m) by MULT_COMM 2714 = m * (n DIV m) + 0 by ADD_0 2715 Therefore n DIV (n DIV m) = m by DIV_UNIQUE 2716*) 2717val divide_by_cofactor = store_thm( 2718 "divide_by_cofactor", 2719 ``!m n. 0 < n /\ m divides n ==> (n DIV (n DIV m) = m)``, 2720 rpt strip_tac >> 2721 `0 < m` by metis_tac[divisor_pos] >> 2722 `n = (n DIV m) * m` by rw[GSYM DIVIDES_EQN] >> 2723 `0 < n DIV m` by metis_tac[MULT, NOT_ZERO_LT_ZERO] >> 2724 `n = m * (n DIV m) + 0` by metis_tac[MULT_COMM, ADD_0] >> 2725 metis_tac[DIV_UNIQUE]); 2726 2727(* Theorem: 0 < n ==> !a b. a divides b ==> a divides b ** n *) 2728(* Proof: 2729 Since 0 < n, n = SUC m for some m. 2730 thus b ** n = b ** (SUC m) 2731 = b * b ** m by EXP 2732 Now a divides b means 2733 ?k. b = k * a by divides_def 2734 so b ** n 2735 = k * a * b ** m 2736 = (k * b ** m) * a by MULT_COMM, MULT_ASSOC 2737 Hence a divides (b ** n) by divides_def 2738*) 2739val divides_exp = store_thm( 2740 "divides_exp", 2741 ``!n. 0 < n ==> !a b. a divides b ==> a divides b ** n``, 2742 rw_tac std_ss[divides_def] >> 2743 `n <> 0` by decide_tac >> 2744 `?m. n = SUC m` by metis_tac[num_CASES] >> 2745 `(q * a) ** n = q * a * (q * a) ** m` by rw[EXP] >> 2746 `_ = q * (q * a) ** m * a` by rw[MULT_COMM, MULT_ASSOC] >> 2747 metis_tac[]); 2748 2749(* Note; converse need prime divisor: 2750DIVIDES_EXP_BASE |- !a b n. prime a /\ 0 < n ==> (a divides b <=> a divides b ** n) 2751Counter-example for a general base: 12 divides 36 = 6^2, but ~(12 divides 6) 2752*) 2753 2754(* Better than: DIVIDES_ADD_1 |- !a b c. a divides b /\ a divides c ==> a divides b + c *) 2755 2756(* Theorem: c divides a /\ c divides b ==> !h k. c divides (h * a + k * b) *) 2757(* Proof: 2758 Since c divides a, ?u. a = u * c by divides_def 2759 and c divides b, ?v. b = v * c by divides_def 2760 h * a + k * b 2761 = h * (u * c) + k * (v * c) by above 2762 = h * u * c + k * v * c by MULT_ASSOC 2763 = (h * u + k * v) * c by RIGHT_ADD_DISTRIB 2764 Hence c divides (h * a + k * b) by divides_def 2765*) 2766val divides_linear = store_thm( 2767 "divides_linear", 2768 ``!a b c. c divides a /\ c divides b ==> !h k. c divides (h * a + k * b)``, 2769 rw_tac std_ss[divides_def] >> 2770 metis_tac[RIGHT_ADD_DISTRIB, MULT_ASSOC]); 2771 2772(* Theorem: c divides a /\ c divides b ==> !h k d. (h * a = k * b + d) ==> c divides d *) 2773(* Proof: 2774 If c = 0, 2775 0 divides a ==> a = 0 by ZERO_DIVIDES 2776 0 divides b ==> b = 0 by ZERO_DIVIDES 2777 Thus d = 0 by arithmetic 2778 and 0 divides 0 by ZERO_DIVIDES 2779 If c <> 0, 0 < c. 2780 c divides a ==> (a MOD c = 0) by DIVIDES_MOD_0 2781 c divides b ==> (b MOD c = 0) by DIVIDES_MOD_0 2782 Hence 0 = (h * a) MOD c by MOD_TIMES2, ZERO_MOD 2783 = (0 + d MOD c) MOD c by MOD_PLUS, MOD_TIMES2, ZERO_MOD 2784 = d MOD c by MOD_MOD 2785 or c divides d by DIVIDES_MOD_0 2786*) 2787val divides_linear_sub = store_thm( 2788 "divides_linear_sub", 2789 ``!a b c. c divides a /\ c divides b ==> !h k d. (h * a = k * b + d) ==> c divides d``, 2790 rpt strip_tac >> 2791 Cases_on `c = 0` >| [ 2792 `(a = 0) /\ (b = 0)` by metis_tac[ZERO_DIVIDES] >> 2793 `d = 0` by rw_tac arith_ss[] >> 2794 rw[], 2795 `0 < c` by decide_tac >> 2796 `(a MOD c = 0) /\ (b MOD c = 0)` by rw[GSYM DIVIDES_MOD_0] >> 2797 `0 = (h * a) MOD c` by metis_tac[MOD_TIMES2, ZERO_MOD, MULT_0] >> 2798 `_ = (0 + d MOD c) MOD c` by metis_tac[MOD_PLUS, MOD_TIMES2, ZERO_MOD, MULT_0] >> 2799 `_ = d MOD c` by rw[MOD_MOD] >> 2800 rw[DIVIDES_MOD_0] 2801 ]); 2802 2803(* Theorem: 1 < p ==> !m n. p ** m divides p ** n <=> m <= n *) 2804(* Proof: 2805 Note p <> 0 /\ p <> 1 by 1 < p 2806 2807 If-part: p ** m divides p ** n ==> m <= n 2808 By contradiction, suppose n < m. 2809 Let d = m - n, then d <> 0 by n < m 2810 Note p ** m = p ** n * p ** d by EXP_BY_ADD_SUB_LT 2811 and p ** n <> 0 by EXP_EQ_0, p <> 0 2812 Now ?q. p ** n = q * p ** m by divides_def 2813 = q * p ** d * p ** n by MULT_ASSOC_COMM 2814 Thus 1 * p ** n = q * p ** d * p ** n by MULT_LEFT_1 2815 or 1 = q * p ** d by MULT_RIGHT_CANCEL 2816 ==> p ** d = 1 by MULT_EQ_1 2817 or d = 0 by EXP_EQ_1, p <> 1 2818 This contradicts d <> 0. 2819 2820 Only-if part: m <= n ==> p ** m divides p ** n 2821 Note p ** n = p ** m * p ** (n - m) by EXP_BY_ADD_SUB_LE 2822 Thus p ** m divides p ** n by divides_def, MULT_COMM 2823*) 2824val power_divides_iff = store_thm( 2825 "power_divides_iff", 2826 ``!p. 1 < p ==> !m n. p ** m divides p ** n <=> m <= n``, 2827 rpt strip_tac >> 2828 `p <> 0 /\ p <> 1` by decide_tac >> 2829 rw[EQ_IMP_THM] >| [ 2830 spose_not_then strip_assume_tac >> 2831 `n < m /\ m - n <> 0` by decide_tac >> 2832 qabbrev_tac `d = m - n` >> 2833 `p ** m = p ** n * p ** d` by rw[EXP_BY_ADD_SUB_LT, Abbr`d`] >> 2834 `p ** n <> 0` by rw[EXP_EQ_0] >> 2835 `?q. p ** n = q * p ** m` by rw[GSYM divides_def] >> 2836 `_ = q * p ** d * p ** n` by metis_tac[MULT_ASSOC_COMM] >> 2837 `1 = q * p ** d` by metis_tac[MULT_RIGHT_CANCEL, MULT_LEFT_1] >> 2838 `p ** d = 1` by metis_tac[MULT_EQ_1] >> 2839 metis_tac[EXP_EQ_1], 2840 `p ** n = p ** m * p ** (n - m)` by rw[EXP_BY_ADD_SUB_LE] >> 2841 metis_tac[divides_def, MULT_COMM] 2842 ]); 2843 2844(* Theorem: prime p ==> !m n. p ** m divides p ** n <=> m <= n *) 2845(* Proof: by power_divides_iff, ONE_LT_PRIME *) 2846val prime_power_divides_iff = store_thm( 2847 "prime_power_divides_iff", 2848 ``!p. prime p ==> !m n. p ** m divides p ** n <=> m <= n``, 2849 rw[power_divides_iff, ONE_LT_PRIME]); 2850 2851(* Theorem: 0 < n /\ 1 < p ==> p divides p ** n *) 2852(* Proof: 2853 Note 0 < n <=> 1 <= n by arithmetic 2854 so p ** 1 divides p ** n by power_divides_iff 2855 or p divides p ** n by EXP_1 2856*) 2857val divides_self_power = store_thm( 2858 "divides_self_power", 2859 ``!n p. 0 < n /\ 1 < p ==> p divides p ** n``, 2860 metis_tac[power_divides_iff, EXP_1, DECIDE``0 < n <=> 1 <= n``]); 2861 2862(* Theorem: a divides b /\ 0 < b /\ b < 2 * a ==> (b = a) *) 2863(* Proof: 2864 Note ?k. b = k * a by divides_def 2865 and 0 < k by MULT_EQ_0, 0 < b 2866 and k < 2 by LT_MULT_RCANCEL, k * a < 2 * a 2867 Thus k = 1 by 0 < k < 2 2868 or b = k * a = a by arithmetic 2869*) 2870Theorem divides_eq_thm: 2871 !a b. a divides b /\ 0 < b /\ b < 2 * a ==> (b = a) 2872Proof 2873 rpt strip_tac >> 2874 `?k. b = k * a` by rw[GSYM divides_def] >> 2875 `0 < k` by metis_tac[MULT_EQ_0, NOT_ZERO] >> 2876 `k < 2` by metis_tac[LT_MULT_RCANCEL] >> 2877 `k = 1` by decide_tac >> 2878 simp[] 2879QED 2880 2881(* Idea: factor equals cofactor iff the number is a square of the factor. *) 2882 2883(* Theorem: 0 < m /\ m divides n ==> (m = n DIV m <=> n = m ** 2) *) 2884(* Proof: 2885 n 2886 = n DIV m * m + n MOD m by DIVISION, 0 < m 2887 = n DIV m * m + 0 by DIVIDES_MOD_0, m divides n 2888 = n DIV m * m by ADD_0 2889 If m = n DIV m, 2890 then n = m * m = m ** 2 by EXP_2 2891 If n = m ** 2, 2892 then n = m * m by EXP_2 2893 so m = n DIV m by EQ_MULT_RCANCEL 2894*) 2895Theorem factor_eq_cofactor: 2896 !m n. 0 < m /\ m divides n ==> (m = n DIV m <=> n = m ** 2) 2897Proof 2898 rw[EQ_IMP_THM] >> 2899 `n = n DIV m * m + n MOD m` by rw[DIVISION] >> 2900 `_ = m * m + 0` by metis_tac[DIVIDES_MOD_0] >> 2901 simp[] 2902QED 2903 2904(* Theorem alias *) 2905val euclid_prime = save_thm("euclid_prime", P_EUCLIDES); 2906(* |- !p a b. prime p /\ p divides a * b ==> p divides a \/ p divides b *) 2907 2908(* Theorem alias *) 2909val euclid_coprime = save_thm("euclid_coprime", L_EUCLIDES); 2910(* |- !a b c. (gcd a b = 1) /\ b divides a * c ==> b divides c *) 2911 2912(* ------------------------------------------------------------------------- *) 2913(* Modulo Theorems *) 2914(* ------------------------------------------------------------------------- *) 2915 2916(* Theorem: 0 < n ==> !a b. (a MOD n = b) <=> ?c. (a = c * n + b) /\ (b < n) *) 2917(* Proof: 2918 If part: (a MOD n = b) ==> ?c. (a = c * n + b) /\ (b < n) 2919 Or to show: ?c. (a = c * n + a MOD n) /\ a MOD n < n 2920 Taking c = a DIV n, this is true by DIVISION 2921 Only-if part: (a = c * n + b) /\ (b < n) ==> (a MOD n = b) 2922 Or to show: b < n ==> (c * n + b) MOD n = b 2923 (c * n + b) MOD n 2924 = ((c * n) MOD n + b MOD n) MOD n by MOD_PLUS 2925 = (0 + b MOD n) MOD n by MOD_EQ_0 2926 = b MOD n by MOD_MOD 2927 = b by LESS_MOD, b < n 2928*) 2929val MOD_EQN = store_thm( 2930 "MOD_EQN", 2931 ``!n. 0 < n ==> !a b. (a MOD n = b) <=> ?c. (a = c * n + b) /\ (b < n)``, 2932 rw_tac std_ss[EQ_IMP_THM] >- 2933 metis_tac[DIVISION] >> 2934 metis_tac[MOD_PLUS, MOD_EQ_0, ADD, MOD_MOD, LESS_MOD]); 2935 2936(* Theorem: (x + y + z) MOD n = (x MOD n + y MOD n + z MOD n) MOD n *) 2937(* Proof: 2938 (x + y + z) MOD n 2939 = ((x + y) MOD n + z MOD n) MOD n by MOD_PLUS 2940 = ((x MOD n + y MOD n) MOD n + z MOD n) MOD n by MOD_PLUS 2941 = (x MOD n + y MOD n + z MOD n) MOD n by MOD_MOD 2942*) 2943val MOD_PLUS3 = store_thm( 2944 "MOD_PLUS3", 2945 ``!n. 0 < n ==> !x y z. (x + y + z) MOD n = (x MOD n + y MOD n + z MOD n) MOD n``, 2946 metis_tac[MOD_PLUS, MOD_MOD]); 2947 2948(* Theorem: Addition is associative in MOD: if x, y, z all < n, 2949 ((x + y) MOD n + z) MOD n = (x + (y + z) MOD n) MOD n. *) 2950(* Proof: 2951 ((x * y) MOD n * z) MOD n 2952 = (((x * y) MOD n) MOD n * z MOD n) MOD n by MOD_TIMES2 2953 = ((x * y) MOD n * z MOD n) MOD n by MOD_MOD 2954 = (x * y * z) MOD n by MOD_TIMES2 2955 = (x * (y * z)) MOD n by MULT_ASSOC 2956 = (x MOD n * (y * z) MOD n) MOD n by MOD_TIMES2 2957 = (x MOD n * ((y * z) MOD n) MOD n) MOD n by MOD_MOD 2958 = (x * (y * z) MOD n) MOD n by MOD_TIMES2 2959 or 2960 ((x + y) MOD n + z) MOD n 2961 = ((x + y) MOD n + z MOD n) MOD n by LESS_MOD, z < n 2962 = (x + y + z) MOD n by MOD_PLUS 2963 = (x + (y + z)) MOD n by ADD_ASSOC 2964 = (x MOD n + (y + z) MOD n) MOD n by MOD_PLUS 2965 = (x + (y + z) MOD n) MOD n by LESS_MOD, x < n 2966*) 2967val MOD_ADD_ASSOC = store_thm( 2968 "MOD_ADD_ASSOC", 2969 ``!n x y z. 0 < n /\ x < n /\ y < n /\ z < n ==> (((x + y) MOD n + z) MOD n = (x + (y + z) MOD n) MOD n)``, 2970 metis_tac[LESS_MOD, MOD_PLUS, ADD_ASSOC]); 2971 2972(* Theorem: mutliplication is associative in MOD: 2973 (x*y MOD n * z) MOD n = (x * y*Z MOD n) MOD n *) 2974(* Proof: 2975 ((x * y) MOD n * z) MOD n 2976 = (((x * y) MOD n) MOD n * z MOD n) MOD n by MOD_TIMES2 2977 = ((x * y) MOD n * z MOD n) MOD n by MOD_MOD 2978 = (x * y * z) MOD n by MOD_TIMES2 2979 = (x * (y * z)) MOD n by MULT_ASSOC 2980 = (x MOD n * (y * z) MOD n) MOD n by MOD_TIMES2 2981 = (x MOD n * ((y * z) MOD n) MOD n) MOD n by MOD_MOD 2982 = (x * (y * z) MOD n) MOD n by MOD_TIMES2 2983 or 2984 ((x * y) MOD n * z) MOD n 2985 = ((x * y) MOD n * z MOD n) MOD n by LESS_MOD, z < n 2986 = (((x * y) * z) MOD n) MOD n by MOD_TIMES2 2987 = ((x * (y * z)) MOD n) MOD n by MULT_ASSOC 2988 = (x MOD n * (y * z) MOD n) MOD n by MOD_TIMES2 2989 = (x * (y * z) MOD n) MOD n by LESS_MOD, x < n 2990*) 2991val MOD_MULT_ASSOC = store_thm( 2992 "MOD_MULT_ASSOC", 2993 ``!n x y z. 0 < n /\ x < n /\ y < n /\ z < n ==> (((x * y) MOD n * z) MOD n = (x * (y * z) MOD n) MOD n)``, 2994 metis_tac[LESS_MOD, MOD_TIMES2, MULT_ASSOC]); 2995 2996(* Theorem: If n > 0, ((n - x) MOD n + x) MOD n = 0 for x < n. *) 2997(* Proof: 2998 ((n - x) MOD n + x) MOD n 2999 = ((n - x) MOD n + x MOD n) MOD n by LESS_MOD 3000 = (n - x + x) MOD n by MOD_PLUS 3001 = n MOD n by SUB_ADD and 0 <= n 3002 = (1*n) MOD n by MULT_LEFT_1 3003 = 0 by MOD_EQ_0 3004*) 3005val MOD_ADD_INV = store_thm( 3006 "MOD_ADD_INV", 3007 ``!n x. 0 < n /\ x < n ==> (((n - x) MOD n + x) MOD n = 0)``, 3008 metis_tac[LESS_MOD, MOD_PLUS, SUB_ADD, LESS_IMP_LESS_OR_EQ, MOD_EQ_0, MULT_LEFT_1]); 3009 3010(* Theorem: If n > 0, k MOD n = 0 ==> !x. (k*x) MOD n = 0 *) 3011(* Proof: 3012 (k*x) MOD n = (k MOD n * x MOD n) MOD n by MOD_TIMES2 3013 = (0 * x MOD n) MOD n by given 3014 = 0 MOD n by MULT_0 and MULT_COMM 3015 = 0 by ZERO_MOD 3016*) 3017val MOD_MULITPLE_ZERO = store_thm( 3018 "MOD_MULITPLE_ZERO", 3019 ``!n k. 0 < n /\ (k MOD n = 0) ==> !x. ((k*x) MOD n = 0)``, 3020 metis_tac[MOD_TIMES2, MULT_0, MULT_COMM, ZERO_MOD]); 3021 3022(* Theorem: If n > 0, a MOD n = b MOD n ==> (a - b) MOD n = 0 *) 3023(* Proof: 3024 a = (a DIV n)*n + (a MOD n) by DIVISION 3025 b = (b DIV n)*n + (b MOD n) by DIVISION 3026 Hence a - b = ((a DIV n) - (b DIV n))* n 3027 = a multiple of n 3028 Therefore (a - b) MOD n = 0. 3029*) 3030val MOD_EQ_DIFF = store_thm( 3031 "MOD_EQ_DIFF", 3032 ``!n a b. 0 < n /\ (a MOD n = b MOD n) ==> ((a - b) MOD n = 0)``, 3033 rpt strip_tac >> 3034 `a = a DIV n * n + a MOD n` by metis_tac[DIVISION] >> 3035 `b = b DIV n * n + b MOD n` by metis_tac[DIVISION] >> 3036 `a - b = (a DIV n - b DIV n) * n` by rw_tac arith_ss[] >> 3037 metis_tac[MOD_EQ_0]); 3038(* Note: The reverse is true only when a >= b: 3039 (a-b) MOD n = 0 cannot imply a MOD n = b MOD n *) 3040 3041(* Theorem: if n > 0, a >= b, then (a - b) MOD n = 0 <=> a MOD n = b MOD n *) 3042(* Proof: 3043 (a-b) MOD n = 0 3044 ==> n divides (a-b) by MOD_0_DIVIDES 3045 ==> (a-b) = k*n for some k by divides_def 3046 ==> a = b + k*n need b <= a to apply arithmeticTheory.SUB_ADD 3047 ==> a MOD n = b MOD n by arithmeticTheory.MOD_TIMES 3048 3049 The converse is given by MOD_EQ_DIFF. 3050*) 3051val MOD_EQ = store_thm( 3052 "MOD_EQ", 3053 ``!n a b. 0 < n /\ b <= a ==> (((a - b) MOD n = 0) <=> (a MOD n = b MOD n))``, 3054 rw[EQ_IMP_THM] >| [ 3055 `?k. a - b = k * n` by metis_tac[DIVIDES_MOD_0, divides_def] >> 3056 `a = k*n + b` by rw_tac arith_ss[] >> 3057 metis_tac[MOD_TIMES], 3058 metis_tac[MOD_EQ_DIFF] 3059 ]); 3060(* Both MOD_EQ_DIFF and MOD_EQ are required in MOD_MULT_LCANCEL *) 3061 3062(* Theorem: n < m ==> ((n MOD m = 0) <=> (n = 0)) *) 3063(* Proof: 3064 Note n < m ==> (n MOD m = n) by LESS_MOD 3065 Thus (n MOD m = 0) <=> (n = 0) by above 3066*) 3067val MOD_EQ_0_IFF = store_thm( 3068 "MOD_EQ_0_IFF", 3069 ``!m n. n < m ==> ((n MOD m = 0) <=> (n = 0))``, 3070 rw_tac bool_ss[LESS_MOD]); 3071 3072(* Theorem: ((a MOD n) ** m) MOD n = (a ** m) MOD n *) 3073(* Proof: by induction on m. 3074 Base case: (a MOD n) ** 0 MOD n = a ** 0 MOD n 3075 (a MOD n) ** 0 MOD n 3076 = 1 MOD n by EXP 3077 = a ** 0 MOD n by EXP 3078 Step case: (a MOD n) ** m MOD n = a ** m MOD n ==> (a MOD n) ** SUC m MOD n = a ** SUC m MOD n 3079 (a MOD n) ** SUC m MOD n 3080 = ((a MOD n) * (a MOD n) ** m) MOD n by EXP 3081 = ((a MOD n) * (((a MOD n) ** m) MOD n)) MOD n by MOD_TIMES2, MOD_MOD 3082 = ((a MOD n) * (a ** m MOD n)) MOD n by induction hypothesis 3083 = (a * a ** m) MOD n by MOD_TIMES2 3084 = a ** SUC m MOD n by EXP 3085*) 3086val MOD_EXP = store_thm( 3087 "MOD_EXP", 3088 ``!n. 0 < n ==> !a m. ((a MOD n) ** m) MOD n = (a ** m) MOD n``, 3089 rpt strip_tac >> 3090 Induct_on `m` >- 3091 rw[EXP] >> 3092 `(a MOD n) ** SUC m MOD n = ((a MOD n) * (a MOD n) ** m) MOD n` by rw[EXP] >> 3093 `_ = ((a MOD n) * (((a MOD n) ** m) MOD n)) MOD n` by metis_tac[MOD_TIMES2, MOD_MOD] >> 3094 `_ = ((a MOD n) * (a ** m MOD n)) MOD n` by rw[] >> 3095 `_ = (a * a ** m) MOD n` by rw[MOD_TIMES2] >> 3096 rw[EXP]); 3097 3098 3099(* Theorem: 0 < n /\ EVEN m ==> EVEN (m ** n) *) 3100(* Proof: 3101 Since EVEN m, m MOD 2 = 0 by EVEN_MOD2 3102 EVEN (m ** n) 3103 <=> (m ** n) MOD 2 = 0 by EVEN_MOD2 3104 <=> (m MOD 2) ** n MOD 2 = 0 by EXP_MOD, 0 < 2 3105 ==> 0 ** n MOD 2 = 0 by above 3106 <=> 0 MOD 2 = 0 by ZERO_EXP, n <> 0 3107 <=> 0 = 0 by ZERO_MOD 3108 <=> T 3109*) 3110(* Note: arithmeticTheory.EVEN_EXP |- !m n. 0 < n /\ EVEN m ==> EVEN (m ** n) *) 3111 3112(* Theorem: !m n. 0 < n /\ ODD m ==> ODD (m ** n) *) 3113(* Proof: 3114 Since ODD m, m MOD 2 = 1 by ODD_MOD2 3115 ODD (m ** n) 3116 <=> (m ** n) MOD 2 = 1 by ODD_MOD2 3117 <=> (m MOD 2) ** n MOD 2 = 1 by EXP_MOD, 0 < 2 3118 ==> 1 ** n MOD 2 = 1 by above 3119 <=> 1 MOD 2 = 1 by EXP_1, n <> 0 3120 <=> 1 = 1 by ONE_MOD, 1 < 2 3121 <=> T 3122*) 3123val ODD_EXP = store_thm( 3124 "ODD_EXP", 3125 ``!m n. 0 < n /\ ODD m ==> ODD (m ** n)``, 3126 rw[ODD_MOD2] >> 3127 `n <> 0 /\ 0 < 2` by decide_tac >> 3128 metis_tac[EXP_MOD, EXP_1, ONE_MOD]); 3129 3130(* Theorem: 0 < n ==> !m. (EVEN m <=> EVEN (m ** n)) /\ (ODD m <=> ODD (m ** n)) *) 3131(* Proof: 3132 First goal: EVEN m <=> EVEN (m ** n) 3133 If part: EVEN m ==> EVEN (m ** n), true by EVEN_EXP 3134 Only-if part: EVEN (m ** n) ==> EVEN m. 3135 By contradiction, suppose ~EVEN m. 3136 Then ODD m by EVEN_ODD 3137 and ODD (m ** n) by ODD_EXP 3138 or ~EVEN (m ** n) by EVEN_ODD 3139 This contradicts EVEN (m ** n). 3140 Second goal: ODD m <=> ODD (m ** n) 3141 Just mirror the reasoning of first goal. 3142*) 3143val power_parity = store_thm( 3144 "power_parity", 3145 ``!n. 0 < n ==> !m. (EVEN m <=> EVEN (m ** n)) /\ (ODD m <=> ODD (m ** n))``, 3146 metis_tac[EVEN_EXP, ODD_EXP, ODD_EVEN]); 3147 3148(* Theorem: 0 < n ==> EVEN (2 ** n) *) 3149(* Proof: 3150 EVEN (2 ** n) 3151 <=> (2 ** n) MOD 2 = 0 by EVEN_MOD2 3152 <=> (2 MOD 2) ** n MOD 2 = 0 by EXP_MOD 3153 <=> 0 ** n MOD 2 = 0 by DIVMOD_ID, 0 < 2 3154 <=> 0 MOD 2 = 0 by ZERO_EXP, n <> 0 3155 <=> 0 = 0 by ZERO_MOD 3156 <=> T 3157*) 3158val EXP_2_EVEN = store_thm( 3159 "EXP_2_EVEN", 3160 ``!n. 0 < n ==> EVEN (2 ** n)``, 3161 rw[EVEN_MOD2, ZERO_EXP]); 3162(* Michael's proof by induction *) 3163val EXP_2_EVEN = store_thm( 3164 "EXP_2_EVEN", 3165 ``!n. 0 < n ==> EVEN (2 ** n)``, 3166 Induct >> rw[EXP, EVEN_DOUBLE]); 3167 3168(* Theorem: 0 < n ==> ODD (2 ** n - 1) *) 3169(* Proof: 3170 Since 0 < 2 ** n by EXP_POS, 0 < 2 3171 so 1 <= 2 ** n by LESS_EQ 3172 thus SUC (2 ** n - 1) 3173 = 2 ** n - 1 + 1 by ADD1 3174 = 2 ** n by SUB_ADD, 1 <= 2 ** n 3175 and EVEN (2 ** n) by EXP_2_EVEN 3176 Hence ODD (2 ** n - 1) by EVEN_ODD_SUC 3177*) 3178val EXP_2_PRE_ODD = store_thm( 3179 "EXP_2_PRE_ODD", 3180 ``!n. 0 < n ==> ODD (2 ** n - 1)``, 3181 rpt strip_tac >> 3182 `0 < 2 ** n` by rw[EXP_POS] >> 3183 `SUC (2 ** n - 1) = 2 ** n` by decide_tac >> 3184 metis_tac[EXP_2_EVEN, EVEN_ODD_SUC]); 3185 3186(* ------------------------------------------------------------------------- *) 3187(* Modulo Inverse *) 3188(* ------------------------------------------------------------------------- *) 3189 3190(* 3191> LINEAR_GCD |> SPEC ``j:num`` |> SPEC ``k:num``; 3192val it = |- j <> 0 ==> ?p q. p * j = q * k + gcd k j: thm 3193*) 3194 3195(* Theorem: 0 < j ==> ?p q. p * j = q * k + gcd j k *) 3196(* Proof: by LINEAR_GCD, GCD_SYM *) 3197val GCD_LINEAR = store_thm( 3198 "GCD_LINEAR", 3199 ``!j k. 0 < j ==> ?p q. p * j = q * k + gcd j k``, 3200 metis_tac[LINEAR_GCD, GCD_SYM, NOT_ZERO]); 3201 3202(* Theorem: [Euclid's Lemma] A prime a divides product iff the prime a divides factor. 3203 [in MOD notation] For prime p, x*y MOD p = 0 <=> x MOD p = 0 or y MOD p = 0 *) 3204(* Proof: 3205 The if part is already in P_EUCLIDES: 3206 !p a b. prime p /\ divides p (a * b) ==> p divides a \/ p divides b 3207 Convert the divides to MOD by DIVIDES_MOD_0. 3208 The only-if part is: 3209 (1) divides p x ==> divides p (x * y) 3210 (2) divides p y ==> divides p (x * y) 3211 Both are true by DIVIDES_MULT: !a b c. a divides b ==> a divides (b * c). 3212 The symmetry of x and y can be taken care of by MULT_COMM. 3213*) 3214val EUCLID_LEMMA = store_thm( 3215 "EUCLID_LEMMA", 3216 ``!p x y. prime p ==> (((x * y) MOD p = 0) <=> (x MOD p = 0) \/ (y MOD p = 0))``, 3217 rpt strip_tac >> 3218 `0 < p` by rw[PRIME_POS] >> 3219 rw[GSYM DIVIDES_MOD_0, EQ_IMP_THM] >> 3220 metis_tac[P_EUCLIDES, DIVIDES_MULT, MULT_COMM]); 3221 3222(* Theorem: [Cancellation Law for MOD p] 3223 For prime p, if x MOD p <> 0, 3224 (x*y) MOD p = (x*z) MOD p ==> y MOD p = z MOD p *) 3225(* Proof: 3226 (x*y) MOD p = (x*z) MOD p 3227 ==> ((x*y) - (x*z)) MOD p = 0 by MOD_EQ_DIFF 3228 ==> (x*(y-z)) MOD p = 0 by arithmetic LEFT_SUB_DISTRIB 3229 ==> (y-z) MOD p = 0 by EUCLID_LEMMA, x MOD p <> 0 3230 ==> y MOD p = z MOD p if z <= y 3231 3232 Since this theorem is symmetric in y, z, 3233 First prove the theorem assuming z <= y, 3234 then use the same proof for y <= z. 3235*) 3236Theorem MOD_MULT_LCANCEL: 3237 !p x y z. prime p /\ (x * y) MOD p = (x * z) MOD p /\ x MOD p <> 0 ==> y MOD p = z MOD p 3238Proof 3239 rpt strip_tac >> 3240 `!a b c. c <= b /\ (a * b) MOD p = (a * c) MOD p /\ a MOD p <> 0 ==> b MOD p = c MOD p` by 3241 (rpt strip_tac >> 3242 `0 < p` by rw[PRIME_POS] >> 3243 `(a * b - a * c) MOD p = 0` by rw[MOD_EQ_DIFF] >> 3244 `(a * (b - c)) MOD p = 0` by rw[LEFT_SUB_DISTRIB] >> 3245 metis_tac[EUCLID_LEMMA, MOD_EQ]) >> 3246 Cases_on `z <= y` >- 3247 metis_tac[] >> 3248 `y <= z` by decide_tac >> 3249 metis_tac[] 3250QED 3251 3252(* Theorem: prime p /\ (y * x) MOD p = (z * x) MOD p /\ x MOD p <> 0 ==> 3253 y MOD p = z MOD p *) 3254(* Proof: by MOD_MULT_LCANCEL, MULT_COMM *) 3255Theorem MOD_MULT_RCANCEL: 3256 !p x y z. prime p /\ (y * x) MOD p = (z * x) MOD p /\ x MOD p <> 0 ==> 3257 y MOD p = z MOD p 3258Proof 3259 metis_tac[MOD_MULT_LCANCEL, MULT_COMM] 3260QED 3261 3262(* Theorem: For prime p, 0 < x < p ==> ?y. 0 < y /\ y < p /\ (y*x) MOD p = 1 *) 3263(* Proof: 3264 0 < x < p 3265 ==> ~ divides p x by NOT_LT_DIVIDES 3266 ==> gcd p x = 1 by gcdTheory.PRIME_GCD 3267 ==> ?k q. k * x = q * p + 1 by gcdTheory.LINEAR_GCD 3268 ==> k*x MOD p = (q*p + 1) MOD p by arithmetic 3269 ==> k*x MOD p = 1 by MOD_MULT, 1 < p. 3270 ==> (k MOD p)*(x MOD p) MOD p = 1 by MOD_TIMES2 3271 ==> ((k MOD p) * x) MOD p = 1 by LESS_MOD, x < p. 3272 Now k MOD p < p by MOD_LESS 3273 and 0 < k MOD p since (k*x) MOD p <> 0 (by 1 <> 0) 3274 and x MOD p <> 0 (by ~ divides p x) 3275 by EUCLID_LEMMA 3276 Hence take y = k MOD p, then 0 < y < p. 3277*) 3278val MOD_MULT_INV_EXISTS = store_thm( 3279 "MOD_MULT_INV_EXISTS", 3280 ``!p x. prime p /\ 0 < x /\ x < p ==> ?y. 0 < y /\ y < p /\ ((y * x) MOD p = 1)``, 3281 rpt strip_tac >> 3282 `0 < p /\ 1 < p` by metis_tac[PRIME_POS, ONE_LT_PRIME] >> 3283 `gcd p x = 1` by metis_tac[PRIME_GCD, NOT_LT_DIVIDES] >> 3284 `?k q. k * x = q * p + 1` by metis_tac[LINEAR_GCD, NOT_ZERO_LT_ZERO] >> 3285 `1 = (k * x) MOD p` by metis_tac[MOD_MULT] >> 3286 `_ = ((k MOD p) * (x MOD p)) MOD p` by metis_tac[MOD_TIMES2] >> 3287 `0 < k MOD p` by 3288 (`1 <> 0` by decide_tac >> 3289 `x MOD p <> 0` by metis_tac[DIVIDES_MOD_0, NOT_LT_DIVIDES] >> 3290 `k MOD p <> 0` by metis_tac[EUCLID_LEMMA, MOD_MOD] >> 3291 decide_tac) >> 3292 metis_tac[MOD_LESS, LESS_MOD]); 3293 3294(* Convert this theorem into MUL_INV_DEF *) 3295 3296(* Step 1: move ?y forward by collecting quantifiers *) 3297val lemma = prove( 3298 ``!p x. ?y. prime p /\ 0 < x /\ x < p ==> 0 < y /\ y < p /\ ((y * x) MOD p = 1)``, 3299 metis_tac[MOD_MULT_INV_EXISTS]); 3300 3301(* Step 2: apply SKOLEM_THM *) 3302(* 3303- SKOLEM_THM; 3304> val it = |- !P. (!x. ?y. P x y) <=> ?f. !x. P x (f x) : thm 3305*) 3306val MOD_MULT_INV_DEF = new_specification( 3307 "MOD_MULT_INV_DEF", 3308 ["MOD_MULT_INV"], (* avoid MOD_MULT_INV_EXISTS: thm *) 3309 SIMP_RULE (srw_ss()) [SKOLEM_THM] lemma); 3310(* 3311> val MOD_MULT_INV_DEF = 3312 |- !p x. 3313 prime p /\ 0 < x /\ x < p ==> 3314 0 < MOD_MULT_INV p x /\ MOD_MULT_INV p x < p /\ 3315 ((MOD_MULT_INV p x * x) MOD p = 1) : thm 3316*) 3317 3318(* ------------------------------------------------------------------------- *) 3319(* FACTOR Theorems *) 3320(* ------------------------------------------------------------------------- *) 3321 3322(* Theorem: ~ prime n ==> n has a proper prime factor p *) 3323(* Proof: apply PRIME_FACTOR: 3324 !n. n <> 1 ==> ?p. prime p /\ p divides n : thm 3325*) 3326val PRIME_FACTOR_PROPER = store_thm( 3327 "PRIME_FACTOR_PROPER", 3328 ``!n. 1 < n /\ ~prime n ==> ?p. prime p /\ p < n /\ (p divides n)``, 3329 rpt strip_tac >> 3330 `0 < n /\ n <> 1` by decide_tac >> 3331 `?p. prime p /\ p divides n` by metis_tac[PRIME_FACTOR] >> 3332 `~(n < p)` by metis_tac[NOT_LT_DIVIDES] >> 3333 Cases_on `n = p` >- 3334 full_simp_tac std_ss[] >> 3335 `p < n` by decide_tac >> 3336 metis_tac[]); 3337 3338(* Theorem: If p divides n, then there is a (p ** m) that maximally divides n. *) 3339(* Proof: 3340 Consider the set s = {k | p ** k divides n} 3341 Since p IN s, s <> {} by MEMBER_NOT_EMPTY 3342 For k IN s, p ** k n divides ==> p ** k <= n by DIVIDES_LE 3343 Since ?z. n <= p ** z by EXP_ALWAYS_BIG_ENOUGH 3344 p ** k <= p ** z 3345 k <= z by EXP_BASE_LE_MONO 3346 or k < SUC z 3347 Hence s SUBSET count (SUC z) by SUBSET_DEF 3348 and FINITE s by FINITE_COUNT, SUBSET_FINITE 3349 Let m = MAX_SET s 3350 Then p ** m n divides by MAX_SET_DEF 3351 Let q = n DIV (p ** m) 3352 i.e. n = q * (p ** m) 3353 If p divides q, then q = t * p 3354 or n = t * p * (p ** m) 3355 = t * (p * p ** m) by MULT_ASSOC 3356 = t * p ** SUC m by EXP 3357 i.e. p ** SUC m divides n, or SUC m IN s. 3358 Since m < SUC m by LESS_SUC 3359 This contradicts the maximal property of m. 3360*) 3361val FACTOR_OUT_POWER = store_thm( 3362 "FACTOR_OUT_POWER", 3363 ``!n p. 0 < n /\ 1 < p /\ p divides n ==> ?m. (p ** m) divides n /\ ~(p divides (n DIV (p ** m)))``, 3364 rpt strip_tac >> 3365 `p <= n` by rw[DIVIDES_LE] >> 3366 `1 < n` by decide_tac >> 3367 qabbrev_tac `s = {k | (p ** k) divides n }` >> 3368 qexists_tac `MAX_SET s` >> 3369 qabbrev_tac `m = MAX_SET s` >> 3370 `!k. k IN s <=> (p ** k) divides n` by rw[Abbr`s`] >> 3371 `s <> {}` by metis_tac[MEMBER_NOT_EMPTY, EXP_1] >> 3372 `?z. n <= p ** z` by rw[EXP_ALWAYS_BIG_ENOUGH] >> 3373 `!k. k IN s ==> k <= z` by metis_tac[DIVIDES_LE, EXP_BASE_LE_MONO, LESS_EQ_TRANS] >> 3374 `!k. k <= z ==> k < SUC z` by decide_tac >> 3375 `s SUBSET (count (SUC z))` by metis_tac[IN_COUNT, SUBSET_DEF, LESS_EQ_TRANS] >> 3376 `FINITE s` by metis_tac[FINITE_COUNT, SUBSET_FINITE] >> 3377 `m IN s /\ !y. y IN s ==> y <= m` by metis_tac[MAX_SET_DEF] >> 3378 `(p ** m) divides n` by metis_tac[] >> 3379 rw[] >> 3380 spose_not_then strip_assume_tac >> 3381 `0 < p` by decide_tac >> 3382 `0 < p ** m` by rw[EXP_POS] >> 3383 `n = (p ** m) * (n DIV (p ** m))` by rw[DIVIDES_FACTORS] >> 3384 `?q. n DIV (p ** m) = q * p` by rw[GSYM divides_def] >> 3385 `n = q * p ** SUC m` by metis_tac[MULT_COMM, MULT_ASSOC, EXP] >> 3386 `SUC m <= m` by metis_tac[divides_def] >> 3387 decide_tac); 3388 3389(* ------------------------------------------------------------------------- *) 3390(* Useful Theorems. *) 3391(* ------------------------------------------------------------------------- *) 3392 3393(* binomial_add: same as SUM_SQUARED *) 3394 3395(* Theorem: (a + b) ** 2 = a ** 2 + b ** 2 + 2 * a * b *) 3396(* Proof: 3397 (a + b) ** 2 3398 = (a + b) * (a + b) by EXP_2 3399 = a * (a + b) + b * (a + b) by RIGHT_ADD_DISTRIB 3400 = (a * a + a * b) + (b * a + b * b) by LEFT_ADD_DISTRIB 3401 = a * a + b * b + 2 * a * b by arithmetic 3402 = a ** 2 + b ** 2 + 2 * a * b by EXP_2 3403*) 3404Theorem binomial_add: 3405 !a b. (a + b) ** 2 = a ** 2 + b ** 2 + 2 * a * b 3406Proof 3407 rpt strip_tac >> 3408 `(a + b) ** 2 = (a + b) * (a + b)` by simp[] >> 3409 `_ = a * a + b * b + 2 * a * b` by decide_tac >> 3410 simp[] 3411QED 3412 3413(* Theorem: b <= a ==> ((a - b) ** 2 = a ** 2 + b ** 2 - 2 * a * b) *) 3414(* Proof: 3415 If b = 0, 3416 RHS = a ** 2 + 0 ** 2 - 2 * a * 0 3417 = a ** 2 + 0 - 0 3418 = a ** 2 3419 = (a - 0) ** 2 3420 = LHS 3421 If b <> 0, 3422 Then b * b <= a * b by LE_MULT_RCANCEL, b <> 0 3423 and b * b <= 2 * a * b 3424 3425 LHS = (a - b) ** 2 3426 = (a - b) * (a - b) by EXP_2 3427 = a * (a - b) - b * (a - b) by RIGHT_SUB_DISTRIB 3428 = (a * a - a * b) - (b * a - b * b) by LEFT_SUB_DISTRIB 3429 = a * a - (a * b + (a * b - b * b)) by SUB_PLUS 3430 = a * a - (a * b + a * b - b * b) by LESS_EQ_ADD_SUB, b * b <= a * b 3431 = a * a - (2 * a * b - b * b) 3432 = a * a + b * b - 2 * a * b by SUB_SUB, b * b <= 2 * a * b 3433 = a ** 2 + b ** 2 - 2 * a * b by EXP_2 3434 = RHS 3435*) 3436Theorem binomial_sub: 3437 !a b. b <= a ==> ((a - b) ** 2 = a ** 2 + b ** 2 - 2 * a * b) 3438Proof 3439 rpt strip_tac >> 3440 Cases_on `b = 0` >- 3441 simp[] >> 3442 `b * b <= a * b` by rw[] >> 3443 `b * b <= 2 * a * b` by decide_tac >> 3444 `(a - b) ** 2 = (a - b) * (a - b)` by simp[] >> 3445 `_ = a * a + b * b - 2 * a * b` by decide_tac >> 3446 rw[] 3447QED 3448 3449(* Theorem: 2 * a * b <= a ** 2 + b ** 2 *) 3450(* Proof: 3451 If a = b, 3452 LHS = 2 * a * a 3453 = a * a + a * a 3454 = a ** 2 + a ** 2 by EXP_2 3455 = RHS 3456 If a < b, then 0 < b - a. 3457 Thus 0 < (b - a) * (b - a) by MULT_EQ_0 3458 or 0 < (b - a) ** 2 by EXP_2 3459 so 0 < b ** 2 + a ** 2 - 2 * b * a by binomial_sub, a <= b 3460 ==> 2 * a * b < a ** 2 + b ** 2 due to 0 < RHS. 3461 If b < a, then 0 < a - b. 3462 Thus 0 < (a - b) * (a - b) by MULT_EQ_0 3463 or 0 < (a - b) ** 2 by EXP_2 3464 so 0 < a ** 2 + b ** 2 - 2 * a * b by binomial_sub, b <= a 3465 ==> 2 * a * b < a ** 2 + b ** 2 due to 0 < RHS. 3466*) 3467Theorem binomial_means: 3468 !a b. 2 * a * b <= a ** 2 + b ** 2 3469Proof 3470 rpt strip_tac >> 3471 Cases_on `a = b` >- 3472 simp[] >> 3473 Cases_on `a < b` >| [ 3474 `b - a <> 0` by decide_tac >> 3475 `(b - a) * (b - a) <> 0` by metis_tac[MULT_EQ_0] >> 3476 `(b - a) * (b - a) = (b - a) ** 2` by simp[] >> 3477 `_ = b ** 2 + a ** 2 - 2 * b * a` by rw[binomial_sub] >> 3478 decide_tac, 3479 `a - b <> 0` by decide_tac >> 3480 `(a - b) * (a - b) <> 0` by metis_tac[MULT_EQ_0] >> 3481 `(a - b) * (a - b) = (a - b) ** 2` by simp[] >> 3482 `_ = a ** 2 + b ** 2 - 2 * a * b` by rw[binomial_sub] >> 3483 decide_tac 3484 ] 3485QED 3486 3487(* Theorem: b <= a ==> ((a - b) ** 2 + 4 * a * b = (a + b) ** 2) *) 3488(* Proof: 3489 Note: 2 * a * b <= a ** 2 + b ** 2 by binomial_means, as [1] 3490 (a - b) ** 2 + 4 * a * b 3491 = a ** 2 + b ** 2 - 2 * a * b + 4 * a * b by binomial_sub, b <= a 3492 = a ** 2 + b ** 2 + 4 * a * b - 2 * a * b by SUB_ADD, [1] 3493 = a ** 2 + b ** 2 + 2 * a * b 3494 = (a + b) ** 2 by binomial_add 3495*) 3496Theorem binomial_sub_add: 3497 !a b. b <= a ==> ((a - b) ** 2 + 4 * a * b = (a + b) ** 2) 3498Proof 3499 rpt strip_tac >> 3500 `2 * a * b <= a ** 2 + b ** 2` by rw[binomial_means] >> 3501 `(a - b) ** 2 + 4 * a * b = a ** 2 + b ** 2 - 2 * a * b + 4 * a * b` by rw[binomial_sub] >> 3502 `_ = a ** 2 + b ** 2 + 4 * a * b - 2 * a * b` by decide_tac >> 3503 `_ = a ** 2 + b ** 2 + 2 * a * b` by decide_tac >> 3504 `_ = (a + b) ** 2` by rw[binomial_add] >> 3505 decide_tac 3506QED 3507 3508(* Theorem: a ** 2 - b ** 2 = (a - b) * (a + b) *) 3509(* Proof: 3510 a ** 2 - b ** 2 3511 = a * a - b * b by EXP_2 3512 = a * a + a * b - a * b - b * b by ADD_SUB 3513 = a * a + a * b - (b * a + b * b) by SUB_PLUS 3514 = a * (a + b) - b * (a + b) by LEFT_ADD_DISTRIB 3515 = (a - b) * (a + b) by RIGHT_SUB_DISTRIB 3516*) 3517Theorem difference_of_squares: 3518 !a b. a ** 2 - b ** 2 = (a - b) * (a + b) 3519Proof 3520 rpt strip_tac >> 3521 `a ** 2 - b ** 2 = a * a - b * b` by simp[] >> 3522 `_ = a * a + a * b - a * b - b * b` by decide_tac >> 3523 decide_tac 3524QED 3525 3526(* Theorem: a * a - b * b = (a - b) * (a + b) *) 3527(* Proof: 3528 a * a - b * b 3529 = a ** 2 - b ** 2 by EXP_2 3530 = (a + b) * (a - b) by difference_of_squares 3531*) 3532Theorem difference_of_squares_alt: 3533 !a b. a * a - b * b = (a - b) * (a + b) 3534Proof 3535 rw[difference_of_squares] 3536QED 3537 3538(* binomial_2: same as binomial_add, or SUM_SQUARED *) 3539 3540(* Theorem: (m + n) ** 2 = m ** 2 + n ** 2 + 2 * m * n *) 3541(* Proof: 3542 (m + n) ** 2 3543 = (m + n) * (m + n) by EXP_2 3544 = m * m + n * m + m * n + n * n by LEFT_ADD_DISTRIB, RIGHT_ADD_DISTRIB 3545 = m ** 2 + n ** 2 + 2 * m * n by EXP_2 3546*) 3547val binomial_2 = store_thm( 3548 "binomial_2", 3549 ``!m n. (m + n) ** 2 = m ** 2 + n ** 2 + 2 * m * n``, 3550 rpt strip_tac >> 3551 `(m + n) ** 2 = (m + n) * (m + n)` by rw[] >> 3552 `_ = m * m + n * m + m * n + n * n` by decide_tac >> 3553 `_ = m ** 2 + n ** 2 + 2 * m * n` by rw[] >> 3554 decide_tac); 3555 3556(* Obtain a corollary *) 3557val SUC_SQ = save_thm("SUC_SQ", 3558 binomial_2 |> SPEC ``1`` |> SIMP_RULE (srw_ss()) [GSYM SUC_ONE_ADD]); 3559(* val SUC_SQ = |- !n. SUC n ** 2 = SUC (n ** 2) + TWICE n: thm *) 3560 3561(* Theorem: m <= n ==> SQ m <= SQ n *) 3562(* Proof: 3563 Since m * m <= n * n by LE_MONO_MULT2 3564 so SQ m <= SQ n by notation 3565*) 3566val SQ_LE = store_thm( 3567 "SQ_LE", 3568 ``!m n. m <= n ==> SQ m <= SQ n``, 3569 rw[]); 3570 3571(* Theorem: EVEN n /\ prime n ==> (n = 2) *) 3572(* Proof: 3573 EVEN n ==> n MOD 2 = 0 by EVEN_MOD2 3574 ==> 2 divides n by DIVIDES_MOD_0, 0 < 2 3575 ==> n = 2 by prime_def, 2 <> 1 3576*) 3577val EVEN_PRIME = store_thm( 3578 "EVEN_PRIME", 3579 ``!n. EVEN n /\ prime n ==> (n = 2)``, 3580 rpt strip_tac >> 3581 `0 < 2 /\ 2 <> 1` by decide_tac >> 3582 `2 divides n` by rw[DIVIDES_MOD_0, GSYM EVEN_MOD2] >> 3583 metis_tac[prime_def]); 3584 3585(* Theorem: prime n /\ n <> 2 ==> ODD n *) 3586(* Proof: 3587 By contradiction, suppose ~ODD n. 3588 Then EVEN n by EVEN_ODD 3589 but EVEN n /\ prime n ==> n = 2 by EVEN_PRIME 3590 This contradicts n <> 2. 3591*) 3592val ODD_PRIME = store_thm( 3593 "ODD_PRIME", 3594 ``!n. prime n /\ n <> 2 ==> ODD n``, 3595 metis_tac[EVEN_PRIME, EVEN_ODD]); 3596 3597(* Theorem: prime p ==> 2 <= p *) 3598(* Proof: by ONE_LT_PRIME *) 3599val TWO_LE_PRIME = store_thm( 3600 "TWO_LE_PRIME", 3601 ``!p. prime p ==> 2 <= p``, 3602 metis_tac[ONE_LT_PRIME, DECIDE``1 < n <=> 2 <= n``]); 3603 3604(* Theorem: ~prime 4 *) 3605(* Proof: 3606 Note 4 = 2 * 2 by arithmetic 3607 so 2 divides 4 by divides_def 3608 thus ~prime 4 by primes_def 3609*) 3610Theorem NOT_PRIME_4: 3611 ~prime 4 3612Proof 3613 rpt strip_tac >> 3614 `4 = 2 * 2` by decide_tac >> 3615 `4 <> 2 /\ 4 <> 1 /\ 2 <> 1` by decide_tac >> 3616 metis_tac[prime_def, divides_def] 3617QED 3618 3619(* Theorem: prime n /\ prime m ==> (n divides m <=> (n = m)) *) 3620(* Proof: 3621 If part: prime n /\ prime m /\ n divides m ==> (n = m) 3622 Note prime n 3623 ==> n <> 1 by NOT_PRIME_1 3624 With n divides m by given 3625 and prime m by given 3626 Thus n = m by prime_def 3627 Only-if part; prime n /\ prime m /\ (n = m) ==> n divides m 3628 True as m divides m by DIVIDES_REFL 3629*) 3630val prime_divides_prime = store_thm( 3631 "prime_divides_prime", 3632 ``!n m. prime n /\ prime m ==> (n divides m <=> (n = m))``, 3633 rw[EQ_IMP_THM] >> 3634 `n <> 1` by metis_tac[NOT_PRIME_1] >> 3635 metis_tac[prime_def]); 3636(* This is: dividesTheory.prime_divides_only_self; 3637|- !m n. prime m /\ prime n /\ m divides n ==> (m = n) 3638*) 3639 3640(* Theorem: 0 < m /\ 1 < n /\ (!p. prime p /\ p divides m ==> (p MOD n = 1)) ==> (m MOD n = 1) *) 3641(* Proof: 3642 By complete induction on m. 3643 If m = 1, trivially true by ONE_MOD 3644 If m <> 1, 3645 Then ?p. prime p /\ p divides m by PRIME_FACTOR, m <> 1 3646 and ?q. m = q * p by divides_def 3647 and q divides m by divides_def, MULT_COMM 3648 In order to apply induction hypothesis, 3649 Show: q < m 3650 Note q <= m by DIVIDES_LE, 0 < m 3651 But p <> 1 by NOT_PRIME_1 3652 Thus q <> m by MULT_RIGHT_1, EQ_MULT_LCANCEL, m <> 0 3653 ==> q < m 3654 Show: 0 < q 3655 Since m = q * p and m <> 0 by above 3656 Thus q <> 0, or 0 < q by MULT 3657 Show: !p. prime p /\ p divides q ==> (p MOD n = 1) 3658 If p divides q, and q divides m, 3659 Then p divides m by DIVIDES_TRANS 3660 ==> p MOD n = 1 by implication 3661 3662 Hence q MOD n = 1 by induction hypothesis 3663 and p MOD n = 1 by implication 3664 Now 0 < n by 1 < n 3665 m MDO n 3666 = (q * p) MOD n by m = q * p 3667 = (q MOD n * p MOD n) MOD n by MOD_TIMES2, 0 < n 3668 = (1 * 1) MOD n by above 3669 = 1 by MULT_RIGHT_1, ONE_MOD 3670*) 3671val ALL_PRIME_FACTORS_MOD_EQ_1 = store_thm( 3672 "ALL_PRIME_FACTORS_MOD_EQ_1", 3673 ``!m n. 0 < m /\ 1 < n /\ (!p. prime p /\ p divides m ==> (p MOD n = 1)) ==> (m MOD n = 1)``, 3674 completeInduct_on `m` >> 3675 rpt strip_tac >> 3676 Cases_on `m = 1` >- 3677 rw[] >> 3678 `?p. prime p /\ p divides m` by rw[PRIME_FACTOR] >> 3679 `?q. m = q * p` by rw[GSYM divides_def] >> 3680 `q divides m` by metis_tac[divides_def, MULT_COMM] >> 3681 `p <> 1` by metis_tac[NOT_PRIME_1] >> 3682 `m <> 0` by decide_tac >> 3683 `q <> m` by metis_tac[MULT_RIGHT_1, EQ_MULT_LCANCEL] >> 3684 `q <= m` by metis_tac[DIVIDES_LE] >> 3685 `q < m` by decide_tac >> 3686 `q <> 0` by metis_tac[MULT] >> 3687 `0 < q` by decide_tac >> 3688 `!p. prime p /\ p divides q ==> (p MOD n = 1)` by metis_tac[DIVIDES_TRANS] >> 3689 `q MOD n = 1` by rw[] >> 3690 `p MOD n = 1` by rw[] >> 3691 `0 < n` by decide_tac >> 3692 metis_tac[MOD_TIMES2, MULT_RIGHT_1, ONE_MOD]); 3693 3694(* Theorem: prime p /\ 0 < n ==> !b. p divides (b ** n) <=> p divides b *) 3695(* Proof: 3696 If part: p divides b ** n ==> p divides b 3697 By induction on n. 3698 Base: 0 < 0 ==> p divides b ** 0 ==> p divides b 3699 True by 0 < 0 = F. 3700 Step: 0 < n ==> p divides b ** n ==> p divides b ==> 3701 0 < SUC n ==> p divides b ** SUC n ==> p divides b 3702 If n = 0, 3703 b ** SUC 0 3704 = b ** 1 by ONE 3705 = b by EXP_1 3706 so p divides b. 3707 If n <> 0, 0 < n. 3708 b ** SUC n 3709 = b * b ** n by EXP 3710 Thus p divides b, 3711 or p divides (b ** n) by P_EUCLIDES 3712 For the latter case, 3713 p divides b by induction hypothesis, 0 < n 3714 3715 Only-if part: p divides b ==> p divides b ** n 3716 Since n <> 0, ?m. n = SUC m by num_CASES 3717 and b ** n 3718 = b ** SUC m 3719 = b * b ** m by EXP 3720 Thus p divides b ** n by DIVIDES_MULTIPLE, MULT_COMM 3721*) 3722val prime_divides_power = store_thm( 3723 "prime_divides_power", 3724 ``!p n. prime p /\ 0 < n ==> !b. p divides (b ** n) <=> p divides b``, 3725 rw[EQ_IMP_THM] >| [ 3726 Induct_on `n` >- 3727 rw[] >> 3728 rpt strip_tac >> 3729 Cases_on `n = 0` >- 3730 metis_tac[ONE, EXP_1] >> 3731 `0 < n` by decide_tac >> 3732 `b ** SUC n = b * b ** n` by rw[EXP] >> 3733 metis_tac[P_EUCLIDES], 3734 `n <> 0` by decide_tac >> 3735 `?m. n = SUC m` by metis_tac[num_CASES] >> 3736 `b ** SUC m = b * b ** m` by rw[EXP] >> 3737 metis_tac[DIVIDES_MULTIPLE, MULT_COMM] 3738 ]); 3739 3740(* Theorem: prime p ==> !n. 0 < n ==> p divides p ** n *) 3741(* Proof: 3742 Since p divides p by DIVIDES_REFL 3743 so p divides p ** n by prime_divides_power, 0 < n 3744*) 3745val prime_divides_self_power = store_thm( 3746 "prime_divides_self_power", 3747 ``!p. prime p ==> !n. 0 < n ==> p divides p ** n``, 3748 rw[prime_divides_power, DIVIDES_REFL]); 3749 3750(* Theorem: prime p ==> !b n m. 0 < m /\ (b ** n = p ** m) ==> ?k. (b = p ** k) /\ (k * n = m) *) 3751(* Proof: 3752 Note 1 < p by ONE_LT_PRIME 3753 so p <> 0, 0 < p, p <> 1 by arithmetic 3754 also m <> 0 by 0 < m 3755 Thus p ** m <> 0 by EXP_EQ_0, p <> 0 3756 and p ** m <> 1 by EXP_EQ_1, p <> 1, m <> 0 3757 ==> n <> 0, 0 < n by EXP, b ** n = p ** m <> 1 3758 also b <> 0, 0 < b by EXP_EQ_0, b ** n = p ** m <> 0, 0 < n 3759 3760 Step 1: show p divides b. 3761 Note p divides (p ** m) by prime_divides_self_power, 0 < m 3762 so p divides (b ** n) by given, b ** n = p ** m 3763 or p divides b by prime_divides_power, 0 < b 3764 3765 Step 2: express b = q * p ** u where ~(p divides q). 3766 Note 1 < p /\ 0 < b /\ p divides b 3767 ==> ?u. p ** u divides b /\ ~(p divides b DIV p ** u) by FACTOR_OUT_POWER 3768 Let q = b DIV p ** u, v = u * n. 3769 Since p ** u <> 0 by EXP_EQ_0, p <> 0 3770 so b = q * p ** u by DIVIDES_EQN, 0 < p ** u 3771 p ** m 3772 = (q * p ** u) ** n by b = q * p ** u 3773 = q ** n * (p ** u) ** n by EXP_BASE_MULT 3774 = q ** n * p ** (u * n) by EXP_EXP_MULT 3775 = q ** n * p ** v by v = u * n 3776 3777 Step 3: split cases 3778 If v = m, 3779 Then q ** n * p ** m = 1 * p ** m by above 3780 or q ** n = 1 by EQ_MULT_RCANCEL, p ** m <> 0 3781 giving q = 1 by EXP_EQ_1, 0 < n 3782 Thus b = p ** u by b = q * p ** u 3783 Take k = u, the result follows. 3784 3785 If v < m, 3786 Let d = m - v. 3787 Then 0 < d /\ (m = d + v) by arithmetic 3788 and p ** m = p ** d * p ** v by EXP_ADD 3789 Note p ** v <> 0 by EXP_EQ_0, p <> 0 3790 q ** n * p ** v = p ** d * p ** v 3791 ==> q ** n = p ** d by EQ_MULT_RCANCEL, p ** v <> 0 3792 Now p divides p ** d by prime_divides_self_power, 0 < d 3793 so p divides q ** n by above, q ** n = p ** d 3794 ==> p divides q by prime_divides_power, 0 < n 3795 This contradicts ~(p divides q) 3796 3797 If m < v, 3798 Let d = v - m. 3799 Then 0 < d /\ (v = d + m) by arithmetic 3800 and q ** n * p ** v 3801 = q ** n * (p ** d * p ** m) by EXP_ADD 3802 = q ** n * p ** d * p ** m by MULT_ASSOC 3803 = 1 * p ** m by arithmetic, b ** n = p ** m 3804 Hence q ** n * p ** d = 1 by EQ_MULT_RCANCEL, p ** m <> 0 3805 ==> (q ** n = 1) /\ (p ** d = 1) by MULT_EQ_1 3806 But p ** d <> 1 by EXP_EQ_1, 0 < d 3807 This contradicts p ** d = 1. 3808*) 3809Theorem power_eq_prime_power: 3810 !p. prime p ==> 3811 !b n m. 0 < m /\ (b ** n = p ** m) ==> ?k. (b = p ** k) /\ (k * n = m) 3812Proof 3813 rpt strip_tac >> 3814 `1 < p` by rw[ONE_LT_PRIME] >> 3815 `m <> 0 /\ 0 < p /\ p <> 0 /\ p <> 1` by decide_tac >> 3816 `p ** m <> 0` by rw[EXP_EQ_0] >> 3817 `p ** m <> 1` by rw[EXP_EQ_1] >> 3818 `n <> 0` by metis_tac[EXP] >> 3819 `0 < n /\ 0 < p ** m` by decide_tac >> 3820 `b <> 0` by metis_tac[EXP_EQ_0] >> 3821 `0 < b` by decide_tac >> 3822 `p divides (p ** m)` by rw[prime_divides_self_power] >> 3823 `p divides b` by metis_tac[prime_divides_power] >> 3824 `?u. p ** u divides b /\ ~(p divides b DIV p ** u)` by metis_tac[FACTOR_OUT_POWER] >> 3825 qabbrev_tac `q = b DIV p ** u` >> 3826 `p ** u <> 0` by rw[EXP_EQ_0] >> 3827 `0 < p ** u` by decide_tac >> 3828 `b = q * p ** u` by rw[GSYM DIVIDES_EQN, Abbr`q`] >> 3829 `q ** n * p ** (u * n) = p ** m` by metis_tac[EXP_BASE_MULT, EXP_EXP_MULT] >> 3830 qabbrev_tac `v = u * n` >> 3831 Cases_on `v = m` >| [ 3832 `p ** m = 1 * p ** m` by simp[] >> 3833 `q ** n = 1` by metis_tac[EQ_MULT_RCANCEL] >> 3834 `q = 1` by metis_tac[EXP_EQ_1] >> 3835 `b = p ** u` by simp[] >> 3836 metis_tac[], 3837 Cases_on `v < m` >| [ 3838 `?d. d = m - v` by rw[] >> 3839 `0 < d /\ (m = d + v)` by rw[] >> 3840 `p ** m = p ** d * p ** v` by rw[EXP_ADD] >> 3841 `p ** v <> 0` by metis_tac[EXP_EQ_0] >> 3842 `q ** n = p ** d` by metis_tac[EQ_MULT_RCANCEL] >> 3843 `p divides p ** d` by metis_tac[prime_divides_self_power] >> 3844 metis_tac[prime_divides_power], 3845 `m < v` by decide_tac >> 3846 `?d. d = v - m` by rw[] >> 3847 `0 < d /\ (v = d + m)` by rw[] >> 3848 `d <> 0` by decide_tac >> 3849 `q ** n * p ** d * p ** m = p ** m` by metis_tac[EXP_ADD, MULT_ASSOC] >> 3850 `_ = 1 * p ** m` by rw[] >> 3851 `q ** n * p ** d = 1` by metis_tac[EQ_MULT_RCANCEL] >> 3852 `(q ** n = 1) /\ (p ** d = 1)` by metis_tac[MULT_EQ_1] >> 3853 metis_tac[EXP_EQ_1] 3854 ] 3855 ] 3856QED 3857 3858(* Theorem: 1 < n ==> !m. (n ** m = n) <=> (m = 1) *) 3859(* Proof: 3860 If part: n ** m = n ==> m = 1 3861 Note n = n ** 1 by EXP_1 3862 so n ** m = n ** 1 by given 3863 or m = 1 by EXP_BASE_INJECTIVE, 1 < n 3864 Only-if part: m = 1 ==> n ** m = n 3865 This is true by EXP_1 3866*) 3867val POWER_EQ_SELF = store_thm( 3868 "POWER_EQ_SELF", 3869 ``!n. 1 < n ==> !m. (n ** m = n) <=> (m = 1)``, 3870 metis_tac[EXP_BASE_INJECTIVE, EXP_1]); 3871 3872(* Theorem: k < HALF n <=> k + 1 < n - k *) 3873(* Proof: 3874 If part: k < HALF n ==> k + 1 < n - k 3875 Claim: 1 < n - 2 * k. 3876 Proof: If EVEN n, 3877 Claim: n - 2 * k <> 0 3878 Proof: By contradiction, assume n - 2 * k = 0. 3879 Then 2 * k = n = 2 * HALF n by EVEN_HALF 3880 or k = HALF n by MULT_LEFT_CANCEL, 2 <> 0 3881 but this contradicts k < HALF n. 3882 Claim: n - 2 * k <> 1 3883 Proof: By contradiction, assume n - 2 * k = 1. 3884 Then n = 2 * k + 1 by SUB_EQ_ADD, 0 < 1 3885 or ODD n by ODD_EXISTS, ADD1 3886 but this contradicts EVEN n by EVEN_ODD 3887 Thus n - 2 * k <> 1, or 1 < n - 2 * k by above claims. 3888 Since 1 < n - 2 * k by above 3889 so 2 * k + 1 < n by arithmetic 3890 or k + k + 1 < n by TIMES2 3891 or k + 1 < n - k by arithmetic 3892 3893 Only-if part: k + 1 < n - k ==> k < HALF n 3894 Since k + 1 < n - k 3895 so 2 * k + 1 < n by arithmetic 3896 But n = 2 * HALF n + (n MOD 2) by DIVISION, MULT_COMM, 0 < 2 3897 and n MOD 2 < 2 by MOD_LESS, 0 < 2 3898 so n <= 2 * HALF n + 1 by arithmetic 3899 Thus 2 * k + 1 < 2 * HALF n + 1 by LESS_LESS_EQ_TRANS 3900 or k < HALF by LT_MULT_LCANCEL 3901*) 3902val LESS_HALF_IFF = store_thm( 3903 "LESS_HALF_IFF", 3904 ``!n k. k < HALF n <=> k + 1 < n - k``, 3905 rw[EQ_IMP_THM] >| [ 3906 `1 < n - 2 * k` by 3907 (Cases_on `EVEN n` >| [ 3908 `n - 2 * k <> 0` by 3909 (spose_not_then strip_assume_tac >> 3910 `2 * HALF n = n` by metis_tac[EVEN_HALF] >> 3911 decide_tac) >> 3912 `n - 2 * k <> 1` by 3913 (spose_not_then strip_assume_tac >> 3914 `n = 2 * k + 1` by decide_tac >> 3915 `ODD n` by metis_tac[ODD_EXISTS, ADD1] >> 3916 metis_tac[EVEN_ODD]) >> 3917 decide_tac, 3918 `n MOD 2 = 1` by metis_tac[EVEN_ODD, ODD_MOD2] >> 3919 `n = 2 * HALF n + (n MOD 2)` by metis_tac[DIVISION, MULT_COMM, DECIDE``0 < 2``] >> 3920 decide_tac 3921 ]) >> 3922 decide_tac, 3923 `2 * k + 1 < n` by decide_tac >> 3924 `n = 2 * HALF n + (n MOD 2)` by metis_tac[DIVISION, MULT_COMM, DECIDE``0 < 2``] >> 3925 `n MOD 2 < 2` by rw[] >> 3926 decide_tac 3927 ]); 3928 3929(* Theorem: HALF n < k ==> n - k <= HALF n *) 3930(* Proof: 3931 If k < n, 3932 If EVEN n, 3933 Note HALF n + HALF n < k + HALF n by HALF n < k 3934 or 2 * HALF n < k + HALF n by TIMES2 3935 or n < k + HALF n by EVEN_HALF, EVEN n 3936 or n - k < HALF n by LESS_EQ_SUB_LESS, k <= n 3937 Hence true. 3938 If ~EVEN n, then ODD n by EVEN_ODD 3939 Note HALF n + HALF n + 1 < k + HALF n + 1 by HALF n < k 3940 or 2 * HALF n + 1 < k + HALF n + 1 by TIMES2 3941 or n < k + HALF n + 1 by ODD_HALF 3942 or n <= k + HALF n by arithmetic 3943 so n - k <= HALF n by SUB_LESS_EQ_ADD, k <= n 3944 If ~(k < n), then n <= k. 3945 Thus n - k = 0, hence n - k <= HALF n by arithmetic 3946*) 3947val MORE_HALF_IMP = store_thm( 3948 "MORE_HALF_IMP", 3949 ``!n k. HALF n < k ==> n - k <= HALF n``, 3950 rpt strip_tac >> 3951 Cases_on `k < n` >| [ 3952 Cases_on `EVEN n` >| [ 3953 `n = 2 * HALF n` by rw[EVEN_HALF] >> 3954 `n < k + HALF n` by decide_tac >> 3955 `n - k < HALF n` by decide_tac >> 3956 decide_tac, 3957 `ODD n` by rw[ODD_EVEN] >> 3958 `n = 2 * HALF n + 1` by rw[ODD_HALF] >> 3959 decide_tac 3960 ], 3961 decide_tac 3962 ]); 3963 3964(* Theorem: (!k. k < m ==> f k < f (k + 1)) ==> !k. k < m ==> f k < f m *) 3965(* Proof: 3966 By induction on the difference (m - k): 3967 Base: 0 = m - k /\ k < m ==> f k < f m 3968 Note m = k and k < m contradicts, hence true. 3969 Step: !m k. (v = m - k) ==> k < m ==> f k < f m ==> 3970 SUC v = m - k /\ k < m ==> f k < f m 3971 Note v + 1 = m - k by ADD1 3972 so v = m - (k + 1) by arithmetic 3973 If v = 0, 3974 Then m = k + 1 3975 so f k < f (k + 1) by implication 3976 or f k < f m by m = k + 1 3977 If v <> 0, then 0 < v. 3978 Then 0 < m - (k + 1) by v = m - (k + 1) 3979 or k + 1 < m by arithmetic 3980 Now f k < f (k + 1) by implication, k < m 3981 and f (k + 1) < f m by induction hypothesis, put k = k + 1 3982 so f k < f m by LESS_TRANS 3983*) 3984val MONOTONE_MAX = store_thm( 3985 "MONOTONE_MAX", 3986 ``!f m. (!k. k < m ==> f k < f (k + 1)) ==> !k. k < m ==> f k < f m``, 3987 rpt strip_tac >> 3988 Induct_on `m - k` >| [ 3989 rpt strip_tac >> 3990 decide_tac, 3991 rpt strip_tac >> 3992 `v + 1 = m - k` by rw[] >> 3993 `v = m - (k + 1)` by decide_tac >> 3994 Cases_on `v = 0` >| [ 3995 `m = k + 1` by decide_tac >> 3996 rw[], 3997 `k + 1 < m` by decide_tac >> 3998 `f k < f (k + 1)` by rw[] >> 3999 `f (k + 1) < f m` by rw[] >> 4000 decide_tac 4001 ] 4002 ]); 4003 4004(* Theorem: (multiple gap) 4005 If n divides m, n cannot divide any x: m - n < x < m, or m < x < m + n 4006 n divides m ==> !x. m - n < x /\ x < m + n /\ n divides x ==> (x = m) *) 4007(* Proof: 4008 All these x, when divided by n, have non-zero remainders. 4009 Since n divides m and n divides x 4010 ==> ?h. m = h * n, and ?k. x = k * n by divides_def 4011 Hence m - n < x 4012 ==> (h-1) * n < k * n by RIGHT_SUB_DISTRIB, MULT_LEFT_1 4013 and x < m + n 4014 ==> k * n < (h+1) * n by RIGHT_ADD_DISTRIB, MULT_LEFT_1 4015 so 0 < n, and h-1 < k, and k < h+1 by LT_MULT_RCANCEL 4016 that is, h <= k, and k <= h 4017 Therefore h = k, or m = h * n = k * n = x. 4018*) 4019val MULTIPLE_INTERVAL = store_thm( 4020 "MULTIPLE_INTERVAL", 4021 ``!n m. n divides m ==> !x. m - n < x /\ x < m + n /\ n divides x ==> (x = m)``, 4022 rpt strip_tac >> 4023 `(?h. m = h*n) /\ (?k. x = k * n)` by metis_tac[divides_def] >> 4024 `(h-1) * n < k * n` by metis_tac[RIGHT_SUB_DISTRIB, MULT_LEFT_1] >> 4025 `k * n < (h+1) * n` by metis_tac[RIGHT_ADD_DISTRIB, MULT_LEFT_1] >> 4026 `0 < n /\ h-1 < k /\ k < h+1` by metis_tac[LT_MULT_RCANCEL] >> 4027 `h = k` by decide_tac >> 4028 metis_tac[]); 4029 4030(* Theorem: 0 < m ==> (SUC (n MOD m) = SUC n MOD m + (SUC n DIV m - n DIV m) * m) *) 4031(* Proof: 4032 Let x = n DIV m, y = (SUC n) DIV m. 4033 Let a = SUC (n MOD m), b = (SUC n) MOD m. 4034 Note SUC n = y * m + b by DIVISION, 0 < m, for (SUC n), [1] 4035 and n = x * m + (n MOD m) by DIVISION, 0 < m, for n 4036 so SUC n = SUC (x * m + (n MOD m)) by above 4037 = x * m + a by ADD_SUC, [2] 4038 Equating, x * m + a = y * m + b by [1], [2] 4039 Now n < SUC n by SUC_POS 4040 so n DIV m <= (SUC n) DIV m by DIV_LE_MONOTONE, n <= SUC n 4041 or x <= y 4042 so x * m <= y * m by LE_MULT_RCANCEL, m <> 0 4043 4044 Thus a = b + (y * m - x * m) by arithmetic 4045 = b + (y - x) * m by RIGHT_SUB_DISTRIB 4046*) 4047val MOD_SUC_EQN = store_thm( 4048 "MOD_SUC_EQN", 4049 ``!m n. 0 < m ==> (SUC (n MOD m) = SUC n MOD m + (SUC n DIV m - n DIV m) * m)``, 4050 rpt strip_tac >> 4051 qabbrev_tac `x = n DIV m` >> 4052 qabbrev_tac `y = (SUC n) DIV m` >> 4053 qabbrev_tac `a = SUC (n MOD m)` >> 4054 qabbrev_tac `b = (SUC n) MOD m` >> 4055 `SUC n = y * m + b` by rw[DIVISION, Abbr`y`, Abbr`b`] >> 4056 `n = x * m + (n MOD m)` by rw[DIVISION, Abbr`x`] >> 4057 `SUC n = x * m + a` by rw[Abbr`a`] >> 4058 `n < SUC n` by rw[] >> 4059 `x <= y` by rw[DIV_LE_MONOTONE, Abbr`x`, Abbr`y`] >> 4060 `x * m <= y * m` by rw[] >> 4061 `a = b + (y * m - x * m)` by decide_tac >> 4062 `_ = b + (y - x) * m` by rw[] >> 4063 rw[]); 4064 4065(* Note: Compare this result with these in arithmeticTheory: 4066MOD_SUC |- 0 < y /\ SUC x <> SUC (x DIV y) * y ==> (SUC x MOD y = SUC (x MOD y)) 4067MOD_SUC_IFF |- 0 < y ==> ((SUC x MOD y = SUC (x MOD y)) <=> SUC x <> SUC (x DIV y) * y) 4068*) 4069 4070(* Theorem: 1 < n ==> 1 < HALF (n ** 2) *) 4071(* Proof: 4072 1 < n 4073 ==> 2 <= n by arithmetic 4074 ==> 2 ** 2 <= n ** 2 by EXP_EXP_LE_MONO 4075 ==> (2 ** 2) DIV 2 <= (n ** 2) DIV 2 by DIV_LE_MONOTONE 4076 ==> 2 <= (n ** 2) DIV 2 by arithmetic 4077 ==> 1 < (n ** 2) DIV 2 by arithmetic 4078*) 4079val ONE_LT_HALF_SQ = store_thm( 4080 "ONE_LT_HALF_SQ", 4081 ``!n. 1 < n ==> 1 < HALF (n ** 2)``, 4082 rpt strip_tac >> 4083 `2 <= n` by decide_tac >> 4084 `2 ** 2 <= n ** 2` by rw[] >> 4085 `(2 ** 2) DIV 2 <= (n ** 2) DIV 2` by rw[DIV_LE_MONOTONE] >> 4086 `(2 ** 2) DIV 2 = 2` by EVAL_TAC >> 4087 decide_tac); 4088 4089(* Theorem: 0 < n ==> (HALF (2 ** n) = 2 ** (n - 1)) *) 4090(* Proof: 4091 Since 2 ** n = (2 ** n) DIV 2 * 2 + (2 ** n) MOD 2 by DIVISION 4092 But (2 ** n) MOD 2 4093 = ((2 MOD 2) ** n) MOD 2 by EXP_MOD 4094 = (0 ** n) MOD 2 by DIVMOD_ID 4095 = 0 MOD 2 by ZERO_EXP, n <> 0 4096 = 0 by ZERO_MOD, 0 < n 4097 Now 2 ** n 4098 = 2 ** SUC (n - 1) 4099 = 2 * 2 ** (n - 1) by EXP 4100 = 2 * (2 ** n DIV 2) by MULT_COMM, above 4101 Hence 2 ** (n - 1) = (2 ** n) DIV 2 by MULT_LEFT_CANCEL 4102*) 4103val EXP_2_HALF = store_thm( 4104 "EXP_2_HALF", 4105 ``!n. 0 < n ==> (HALF (2 ** n) = 2 ** (n - 1))``, 4106 rpt strip_tac >> 4107 `2 ** n = (2 ** n) DIV 2 * 2 + (2 ** n) MOD 2` by rw[DIVISION] >> 4108 `(2 ** n) MOD 2 = ((2 MOD 2) ** n) MOD 2` by rw[] >> 4109 `2 MOD 2 = 0` by rw[] >> 4110 `n <> 0` by decide_tac >> 4111 `0 ** n = 0` by rw[] >> 4112 `(2 ** n) MOD 2 = 0` by rw[] >> 4113 `2 ** n = 2 ** n DIV 2 * 2` by decide_tac >> 4114 `n = SUC (n - 1)` by decide_tac >> 4115 `2 * 2 ** (n - 1) = 2 * (2 ** n DIV 2)` by metis_tac[EXP, MULT_COMM] >> 4116 decide_tac); 4117(* Michael's proof by induction *) 4118val EXP_2_HALF = store_thm( 4119 "EXP_2_HALF", 4120 ``!n. 0 < n ==> (HALF (2 ** n) = 2 ** (n - 1))``, 4121 Induct >> 4122 simp[EXP, MULT_TO_DIV]); 4123 4124(* 4125There is EVEN_MULT |- !m n. EVEN (m * n) <=> EVEN m \/ EVEN n 4126There is EVEN_DOUBLE |- !n. EVEN (TWICE n) 4127*) 4128 4129(* Theorem: EVEN n ==> (HALF (m * n) = m * HALF n) *) 4130(* Proof: 4131 Note n = TWICE (HALF n) by EVEN_HALF 4132 Let k = HALF n. 4133 HALF (m * n) 4134 = HALF (m * (2 * k)) by above 4135 = HALF (2 * (m * k)) by MULT_COMM_ASSOC 4136 = m * k by HALF_TWICE 4137 = m * HALF n by notation 4138*) 4139val HALF_MULT_EVEN = store_thm( 4140 "HALF_MULT_EVEN", 4141 ``!m n. EVEN n ==> (HALF (m * n) = m * HALF n)``, 4142 metis_tac[EVEN_HALF, MULT_COMM_ASSOC, HALF_TWICE]); 4143 4144(* Theorem: 0 < k /\ k * m < n ==> m < n *) 4145(* Proof: 4146 Note ?h. k = SUC h by num_CASES, k <> 0 4147 k * m 4148 = SUC h * m by above 4149 = (h + 1) * m by ADD1 4150 = h * m + 1 * m by LEFT_ADD_DISTRIB 4151 = h * m + m by MULT_LEFT_1 4152 Since 0 <= h * m, 4153 so k * m < n ==> m < n. 4154*) 4155val MULT_LESS_IMP_LESS = store_thm( 4156 "MULT_LESS_IMP_LESS", 4157 ``!m n k. 0 < k /\ k * m < n ==> m < n``, 4158 rpt strip_tac >> 4159 `k <> 0` by decide_tac >> 4160 `?h. k = SUC h` by metis_tac[num_CASES] >> 4161 `k * m = h * m + m` by rw[ADD1] >> 4162 decide_tac); 4163 4164(* Theorem: n * HALF ((SQ n) ** 2) <= HALF (n ** 5) *) 4165(* Proof: 4166 n * HALF ((SQ n) ** 2) 4167 <= HALF (n * (SQ n) ** 2) by HALF_MULT 4168 = HALF (n * (n ** 2) ** 2) by EXP_2 4169 = HALF (n * n ** 4) by EXP_EXP_MULT 4170 = HALF (n ** 5) by EXP 4171*) 4172val HALF_EXP_5 = store_thm( 4173 "HALF_EXP_5", 4174 ``!n. n * HALF ((SQ n) ** 2) <= HALF (n ** 5)``, 4175 rpt strip_tac >> 4176 `n * ((SQ n) ** 2) = n * n ** 4` by rw[EXP_2, EXP_EXP_MULT] >> 4177 `_ = n ** 5` by rw[EXP] >> 4178 metis_tac[HALF_MULT]); 4179 4180(* Theorem: n <= 2 * m <=> (n <> 0 ==> HALF (n - 1) < m) *) 4181(* Proof: 4182 Let k = n - 1, then n = SUC k. 4183 If part: n <= TWICE m /\ n <> 0 ==> HALF k < m 4184 Note HALF (SUC k) <= m by DIV_LE_MONOTONE, HALF_TWICE 4185 If EVEN n, 4186 Then ODD k by EVEN_ODD_SUC 4187 ==> HALF (SUC k) = SUC (HALF k) by ODD_SUC_HALF 4188 Thus SUC (HALF k) <= m by above 4189 or HALF k < m by LESS_EQ 4190 If ~EVEN n, then ODD n by EVEN_ODD 4191 Thus EVEN k by EVEN_ODD_SUC 4192 ==> HALF (SUC k) = HALF k by EVEN_SUC_HALF 4193 But k <> TWICE m by k = n - 1, n <= TWICE m 4194 ==> HALF k <> m by EVEN_HALF 4195 Thus HALF k < m by HALF k <= m, HALF k <> m 4196 4197 Only-if part: n <> 0 ==> HALF k < m ==> n <= TWICE m 4198 If n = 0, trivially true. 4199 If n <> 0, has HALF k < m. 4200 If EVEN n, 4201 Then ODD k by EVEN_ODD_SUC 4202 ==> HALF (SUC k) = SUC (HALF k) by ODD_SUC_HALF 4203 But SUC (HALF k) <= m by HALF k < m 4204 Thus HALF n <= m by n = SUC k 4205 ==> TWICE (HALF n) <= TWICE m by LE_MULT_LCANCEL 4206 or n <= TWICE m by EVEN_HALF 4207 If ~EVEN n, then ODD n by EVEN_ODD 4208 Then EVEN k by EVEN_ODD_SUC 4209 ==> TWICE (HALF k) < TWICE m by LT_MULT_LCANCEL 4210 or k < TWICE m by EVEN_HALF 4211 or n <= TWICE m by n = k + 1 4212*) 4213val LE_TWICE_ALT = store_thm( 4214 "LE_TWICE_ALT", 4215 ``!m n. n <= 2 * m <=> (n <> 0 ==> HALF (n - 1) < m)``, 4216 rw[EQ_IMP_THM] >| [ 4217 `n = SUC (n - 1)` by decide_tac >> 4218 qabbrev_tac `k = n - 1` >> 4219 `HALF (SUC k) <= m` by metis_tac[DIV_LE_MONOTONE, HALF_TWICE, DECIDE``0 < 2``] >> 4220 Cases_on `EVEN n` >| [ 4221 `ODD k` by rw[EVEN_ODD_SUC] >> 4222 `HALF (SUC k) = SUC (HALF k)` by rw[ODD_SUC_HALF] >> 4223 decide_tac, 4224 `ODD n` by metis_tac[EVEN_ODD] >> 4225 `EVEN k` by rw[EVEN_ODD_SUC] >> 4226 `HALF (SUC k) = HALF k` by rw[EVEN_SUC_HALF] >> 4227 `k <> TWICE m` by rw[Abbr`k`] >> 4228 `HALF k <> m` by metis_tac[EVEN_HALF] >> 4229 decide_tac 4230 ], 4231 Cases_on `n = 0` >- 4232 rw[] >> 4233 `n = SUC (n - 1)` by decide_tac >> 4234 qabbrev_tac `k = n - 1` >> 4235 Cases_on `EVEN n` >| [ 4236 `ODD k` by rw[EVEN_ODD_SUC] >> 4237 `HALF (SUC k) = SUC (HALF k)` by rw[ODD_SUC_HALF] >> 4238 `HALF n <= m` by rw[] >> 4239 metis_tac[LE_MULT_LCANCEL, EVEN_HALF, DECIDE``2 <> 0``], 4240 `ODD n` by metis_tac[EVEN_ODD] >> 4241 `EVEN k` by rw[EVEN_ODD_SUC] >> 4242 `k < TWICE m` by metis_tac[LT_MULT_LCANCEL, EVEN_HALF, DECIDE``0 < 2``] >> 4243 rw[Abbr`k`] 4244 ] 4245 ]); 4246 4247(* Theorem: (HALF n) DIV 2 ** m = n DIV (2 ** SUC m) *) 4248(* Proof: 4249 (HALF n) DIV 2 ** m 4250 = (n DIV 2) DIV (2 ** m) by notation 4251 = n DIV (2 * 2 ** m) by DIV_DIV_DIV_MULT, 0 < 2, 0 < 2 ** m 4252 = n DIV (2 ** (SUC m)) by EXP 4253*) 4254val HALF_DIV_TWO_POWER = store_thm( 4255 "HALF_DIV_TWO_POWER", 4256 ``!m n. (HALF n) DIV 2 ** m = n DIV (2 ** SUC m)``, 4257 rw[DIV_DIV_DIV_MULT, EXP]); 4258 4259(* Theorem: 1 * 2 + 3 * 4 + 5 * 6 + 7 * 8 = 100 *) 4260(* Proof: by calculation. *) 4261val fit_for_100 = store_thm( 4262 "fit_for_100", 4263 ``1 * 2 + 3 * 4 + 5 * 6 + 7 * 8 = 100``, 4264 decide_tac); 4265 4266(* ------------------------------------------------------------------------- *) 4267 4268(* export theory at end *) 4269val _ = export_theory(); 4270 4271(*===========================================================================*) 4272