1(* ------------------------------------------------------------------------- *) 2(* Integer Functions Computation. *) 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 "logPower"; 12 13(* ------------------------------------------------------------------------- *) 14 15 16 17(* val _ = load "jcLib"; *) 18open jcLib; 19 20(* val _ = load "SatisfySimps"; (* for SatisfySimps.SATISFY_ss *) *) 21 22(* Get dependent theories local *) 23 24(* Get dependent theories in lib *) 25(* val _ = load "helperNumTheory"; *) 26open helperNumTheory; 27 28(* val _ = load "helperFunctionTheory"; *) 29open helperFunctionTheory; 30open pred_setTheory; 31open helperSetTheory; 32 33(* open dependent theories *) 34open arithmeticTheory; 35open dividesTheory gcdTheory; 36 37(* val _ = load "logrootTheory"; *) 38open logrootTheory; (* for ROOT *) 39 40 41(* ------------------------------------------------------------------------- *) 42(* Integer Functions Computation Documentation *) 43(* ------------------------------------------------------------------------- *) 44(* Overloading: 45 SQRT n = ROOT 2 n 46 LOG2 n = LOG 2 n 47 n power_of b = perfect_power n b 48*) 49 50(* Definitions and Theorems (# are exported): 51 52 ROOT computation: 53 ROOT_POWER |- !a n. 1 < a /\ 0 < n ==> (ROOT n (a ** n) = a) 54 ROOT_FROM_POWER |- !m n b. 0 < m /\ (b ** m = n) ==> (b = ROOT m n) 55# ROOT_OF_0 |- !m. 0 < m ==> (ROOT m 0 = 0) 56# ROOT_OF_1 |- !m. 0 < m ==> (ROOT m 1 = 1) 57 ROOT_EQ_0 |- !m. 0 < m ==> !n. (ROOT m n = 0) <=> (n = 0) 58# ROOT_1 |- !n. ROOT 1 n = n 59 ROOT_THM |- !r. 0 < r ==> !n p. (ROOT r n = p) <=> p ** r <= n /\ n < SUC p ** r 60 ROOT_compute |- !r n. 0 < r ==> (ROOT r 0 = 0) /\ 61 (ROOT r n = (let x = 2 * ROOT r (n DIV 2 ** r) 62 in if n < SUC x ** r then x else SUC x)) 63 ROOT_EQN |- !r n. 0 < r ==> (ROOT r n = 64 (let m = TWICE (ROOT r (n DIV 2 ** r)) 65 in m + if (m + 1) ** r <= n then 1 else 0)) 66 ROOT_EVAL |- !r n. ROOT r n = 67 if r = 0 then ROOT 0 n 68 else if n = 0 then 0 69 else (let m = TWICE (ROOT r (n DIV 2 ** r)) 70 in m + if SUC m ** r <= n then 1 else 0) 71 ROOT_SUC |- !r n. 0 < r ==> 72 ROOT r (SUC n) = ROOT r n + 73 if SUC n = SUC (ROOT r n) ** r then 1 else 0 74 ROOT_EQ_1 |- !m. 0 < m ==> !n. (ROOT m n = 1) <=> 0 < n /\ n < 2 ** m 75 ROOT_LE_SELF |- !m n. 0 < m ==> ROOT m n <= n 76 ROOT_EQ_SELF |- !m n. 0 < m ==> (ROOT m n = n) <=> (m = 1) \/ (n = 0) \/ (n = 1)) 77 ROOT_GE_SELF |- !m n. 0 < m ==> (n <= ROOT m n) <=> (m = 1) \/ (n = 0) \/ (n = 1)) 78 ROOT_LE_REVERSE |- !a b n. 0 < a /\ a <= b ==> ROOT b n <= ROOT a n 79 80 Square Root: 81 SQRT_PROPERTY |- !n. 0 < n ==> SQRT n ** 2 <= n /\ n < SUC (SQRT n) ** 2 82 SQRT_THM |- !n p. (SQRT n = p) <=> p ** 2 <= n /\ n < SUC p ** 2 83 SQ_SQRT_LE |- !n. SQ (SQRT n) <= n 84 SQRT_LE |- !n m. n <= m ==> SQRT n <= SQRT m 85 SQRT_LT |- !n m. n < m ==> SQRT n <= SQRT m 86# SQRT_0 |- SQRT 0 = 0 87# SQRT_1 |- SQRT 1 = 1 88 SQRT_EQ_0 |- !n. (SQRT n = 0) <=> (n = 0) 89 SQRT_EQ_1 |- !n. (SQRT n = 1) <=> (n = 1) \/ (n = 2) \/ (n = 3) 90 SQRT_EXP_2 |- !n. SQRT (n ** 2) = n 91 SQRT_OF_SQ |- !n. SQRT (n ** 2) = n 92 SQRT_SQ |- !n. SQRT (SQ n) = n 93 SQRT_LE_SELF |- !n. SQRT n <= n 94 SQRT_GE_SELF |- !n. n <= SQRT n <=> (n = 0) \/ (n = 1) 95 SQRT_EQ_SELF |- !n. (SQRT n = n) <=> (n = 0) \/ (n = 1) 96 SQRT_LE_IMP |- !n m. SQRT n <= m ==> n <= 3 * m ** 2 97 98 Logarithm: 99 LOG_EXACT_EXP |- !a. 1 < a ==> !n. LOG a (a ** n) = n 100 EXP_TO_LOG |- !a b n. 1 < a /\ 0 < b /\ b <= a ** n ==> LOG a b <= n 101 LOG_THM |- !a n. 1 < a /\ 0 < n ==> 102 !p. (LOG a n = p) <=> a ** p <= n /\ n < a ** SUC p 103 LOG_EVAL |- !m n. LOG m n = if m <= 1 \/ n = 0 then LOG m n 104 else if n < m then 0 else SUC (LOG m (n DIV m)) 105 LOG_TEST |- !a n. 1 < a /\ 0 < n ==> 106 !p. (LOG a n = p) <=> SUC n <= a ** SUC p /\ a ** SUC p <= a * n 107 LOG_POWER |- !b x n. 1 < b /\ 0 < x /\ 0 < n ==> 108 n * LOG b x <= LOG b (x ** n) /\ 109 LOG b (x ** n) < n * SUC (LOG b x) 110 LOG_LE_REVERSE |- !a b n. 1 < a /\ 0 < n /\ a <= b ==> LOG b n <= LOG a n 111 112# LOG2_1 |- LOG2 1 = 0 113# LOG2_2 |- LOG2 2 = 1 114 LOG2_THM |- !n. 0 < n ==> !p. (LOG2 n = p) <=> 2 ** p <= n /\ n < 2 ** SUC p 115 LOG2_PROPERTY |- !n. 0 < n ==> 2 ** LOG2 n <= n /\ n < 2 ** SUC (LOG2 n) 116 TWO_EXP_LOG2_LE |- !n. 0 < n ==> 2 ** LOG2 n <= n 117 LOG2_UNIQUE |- !n m. 2 ** m <= n /\ n < 2 ** SUC m ==> (LOG2 n = m) 118 LOG2_EQ_0 |- !n. 0 < n ==> (LOG2 n = 0 <=> n = 1) 119 LOG2_EQ_1 |- !n. 0 < n ==> ((LOG2 n = 1) <=> (n = 2) \/ (n = 3)) 120 LOG2_LE_MONO |- !n m. 0 < n ==> n <= m ==> LOG2 n <= LOG2 m 121 LOG2_LE |- !n m. 0 < n /\ n <= m ==> LOG2 n <= LOG2 m 122 LOG2_LT |- !n m. 0 < n /\ n < m ==> LOG2 n <= LOG2 m 123 LOG2_LT_SELF |- !n. 0 < n ==> LOG2 n < n 124 LOG2_NEQ_SELF |- !n. 0 < n ==> LOG2 n <> n 125 LOG2_EQ_SELF |- !n. (LOG2 n = n) ==> (n = 0) 126# LOG2_POS |- !n. 1 < n ==> 0 < LOG2 n 127 LOG2_TWICE_LT |- !n. 1 < n ==> 1 < 2 * LOG2 n 128 LOG2_TWICE_SQ |- !n. 1 < n ==> 4 <= (2 * LOG2 n) ** 2 129 LOG2_SUC_TWICE_SQ |- !n. 0 < n ==> 4 <= (2 * SUC (LOG2 n)) ** 2 130 LOG2_SUC_SQ |- !n. 1 < n ==> 1 < SUC (LOG2 n) ** 2 131 LOG2_SUC_TIMES_SQ_DIV_2_POS |- !n m. 1 < m ==> 0 < SUC (LOG2 n) * (m ** 2 DIV 2) 132 LOG2_2_EXP |- !n. LOG2 (2 ** n) = n 133 LOG2_EXACT_EXP |- !n. (2 ** LOG2 n = n) <=> ?k. n = 2 ** k 134 LOG2_MULT_EXP |- !n m. 0 < n ==> (LOG2 (n * 2 ** m) = LOG2 n + m) 135 LOG2_TWICE |- !n. 0 < n ==> (LOG2 (TWICE n) = 1 + LOG2 n) 136 LOG2_HALF |- !n. 1 < n ==> (LOG2 (HALF n) = LOG2 n - 1) 137 LOG2_BY_HALF |- !n. 1 < n ==> (LOG2 n = 1 + LOG2 (HALF n)) 138 LOG2_DIV_EXP |- !n m. 2 ** m < n ==> (LOG2 (n DIV 2 ** m) = LOG2 n - m) 139 140 LOG2 Computation: 141 halves_def |- !n. halves n = if n = 0 then 0 else SUC (halves (HALF n)) 142 halves_alt |- !n. halves n = if n = 0 then 0 else 1 + halves (HALF n) 143# halves_0 |- halves 0 = 0 144# halves_1 |- halves 1 = 1 145# halves_2 |- halves 2 = 2 146# halves_pos |- !n. 0 < n ==> 0 < halves n 147 halves_by_LOG2 |- !n. 0 < n ==> (halves n = 1 + LOG2 n) 148 LOG2_compute |- !n. LOG2 n = if n = 0 then LOG2 0 else halves n - 1 149 halves_le |- !m n. m <= n ==> halves m <= halves n 150 halves_eq_0 |- !n. (halves n = 0) <=> (n = 0) 151 halves_eq_1 |- !n. (halves n = 1) <=> (n = 1) 152 153 Perfect Power and Power Free: 154 perfect_power_def |- !n m. perfect_power n m <=> ?e. n = m ** e 155 perfect_power_self |- !n. perfect_power n n 156 perfect_power_0_m |- !m. perfect_power 0 m <=> (m = 0) 157 perfect_power_1_m |- !m. perfect_power 1 m 158 perfect_power_n_0 |- !n. perfect_power n 0 <=> (n = 0) \/ (n = 1) 159 perfect_power_n_1 |- !n. perfect_power n 1 <=> (n = 1) 160 perfect_power_mod_eq_0 |- !n m. 0 < m /\ 1 < n /\ n MOD m = 0 ==> 161 (perfect_power n m <=> perfect_power (n DIV m) m) 162 perfect_power_mod_ne_0 |- !n m. 0 < m /\ 1 < n /\ n MOD m <> 0 ==> ~perfect_power n m 163 perfect_power_test |- !n m. perfect_power n m <=> 164 if n = 0 then m = 0 165 else if n = 1 then T 166 else if m = 0 then n <= 1 167 else if m = 1 then n = 1 168 else if n MOD m = 0 then perfect_power (n DIV m) m 169 else F 170 perfect_power_suc |- !m n. 1 < m /\ perfect_power n m /\ perfect_power (SUC n) m ==> 171 (m = 2) /\ (n = 1) 172 perfect_power_not_suc |- !m n. 1 < m /\ 1 < n /\ perfect_power n m ==> ~perfect_power (SUC n) m 173 LOG_SUC |- !b n. 1 < b /\ 0 < n ==> 174 LOG b (SUC n) = LOG b n + 175 if perfect_power (SUC n) b then 1 else 0 176 perfect_power_bound_LOG2 |- !n. 0 < n ==> !m. perfect_power n m <=> ?k. k <= LOG2 n /\ (n = m ** k) 177 perfect_power_condition |- !p q. prime p /\ (?x y. 0 < x /\ (p ** x = q ** y)) ==> perfect_power q p 178 perfect_power_cofactor |- !n p. 0 < p /\ p divides n ==> (perfect_power n p <=> perfect_power (n DIV p) p) 179 perfect_power_cofactor_alt 180 |- !n p. 0 < n /\ p divides n ==> (perfect_power n p <=> perfect_power (n DIV p) p) 181 perfect_power_2_odd |- !n. perfect_power n 2 ==> (ODD n <=> (n = 1)) 182 183 Power Free: 184 power_free_def |- !n. power_free n <=> !m e. (n = m ** e) ==> (m = n) /\ (e = 1) 185 power_free_0 |- power_free 0 <=> F 186 power_free_1 |- power_free 1 <=> F 187 power_free_gt_1 |- !n. power_free n ==> 1 < n 188 power_free_alt |- !n. power_free n <=> 1 < n /\ !m. perfect_power n m ==> (n = m) 189 prime_is_power_free |- !n. prime n ==> power_free n 190 power_free_perfect_power |- !m n. power_free n /\ perfect_power n m ==> (n = m) 191 power_free_property |- !n. power_free n ==> !j. 1 < j ==> ROOT j n ** j <> n 192 power_free_check_all |- !n. power_free n <=> 1 < n /\ !j. 1 < j ==> ROOT j n ** j <> n 193 194 Upper Logarithm: 195 count_up_def |- !n m k. count_up n m k = if m = 0 then 0 196 else if n <= m then k 197 else count_up n (2 * m) (SUC k) 198 ulog_def |- !n. ulog n = count_up n 1 0 199# ulog_0 |- ulog 0 = 0 200# ulog_1 |- ulog 1 = 0 201# ulog_2 |- ulog 2 = 1 202 203 count_up_exit |- !m n. m <> 0 /\ n <= m ==> !k. count_up n m k = k 204 count_up_suc |- !m n. m <> 0 /\ m < n ==> !k. count_up n m k = count_up n (2 * m) (SUC k) 205 count_up_suc_eqn |- !m. m <> 0 ==> !n t. 2 ** t * m < n ==> 206 !k. count_up n m k = count_up n (2 ** SUC t * m) (SUC k + t) 207 count_up_exit_eqn |- !m. m <> 0 ==> !n t. 2 ** t * m < 2 * n /\ n <= 2 ** t * m ==> 208 !k. count_up n m k = k + t 209 ulog_unique |- !m n. 2 ** m < 2 * n /\ n <= 2 ** m ==> (ulog n = m) 210 ulog_eqn |- !n. ulog n = if 1 < n then SUC (LOG2 (n - 1)) else 0 211 ulog_suc |- !n. 0 < n ==> (ulog (SUC n) = SUC (LOG2 n)) 212 ulog_property |- !n. 0 < n ==> 2 ** ulog n < 2 * n /\ n <= 2 ** ulog n 213 ulog_thm |- !n. 0 < n ==> !m. (ulog n = m) <=> 2 ** m < 2 * n /\ n <= 2 ** m 214 ulog_def_alt |- (ulog 0 = 0) /\ 215 !n. 0 < n ==> !m. (ulog n = m) <=> n <= 2 ** m /\ 2 ** m < TWICE n 216 ulog_eq_0 |- !n. (ulog n = 0) <=> (n = 0) \/ (n = 1) 217 ulog_eq_1 |- !n. (ulog n = 1) <=> (n = 2) 218 ulog_le_1 |- !n. ulog n <= 1 <=> n <= 2 219 ulog_le |- !m n. n <= m ==> ulog n <= ulog m 220 ulog_lt |- !m n. n < m ==> ulog n <= ulog m 221 ulog_2_exp |- !n. ulog (2 ** n) = n 222 ulog_le_self |- !n. ulog n <= n 223 ulog_eq_self |- !n. (ulog n = n) <=> (n = 0) 224 ulog_lt_self |- !n. 0 < n ==> ulog n < n 225 ulog_exp_exact |- !n. (2 ** ulog n = n) <=> perfect_power n 2 226 ulog_exp_not_exact |- !n. ~perfect_power n 2 ==> 2 ** ulog n <> n 227 ulog_property_not_exact |- !n. 0 < n /\ ~perfect_power n 2 ==> n < 2 ** ulog n 228 ulog_property_odd |- !n. 1 < n /\ ODD n ==> n < 2 ** ulog n 229 exp_to_ulog |- !m n. n <= 2 ** m ==> ulog n <= m 230# ulog_pos |- !n. 1 < n ==> 0 < ulog n 231 ulog_ge_1 |- !n. 1 < n ==> 1 <= ulog n 232 ulog_sq_gt_1 |- !n. 2 < n ==> 1 < ulog n ** 2 233 ulog_twice_sq |- !n. 1 < n ==> 4 <= TWICE (ulog n) ** 2 234 ulog_alt |- !n. ulog n = if n = 0 then 0 235 else if perfect_power n 2 then LOG2 n else SUC (LOG2 n) 236 ulog_LOG2 |- !n. 0 < n ==> LOG2 n <= ulog n /\ ulog n <= 1 + LOG2 n 237 perfect_power_bound_ulog 238 |- !n. 0 < n ==> !m. perfect_power n m <=> ?k. k <= ulog n /\ (n = m ** k) 239 240 Upper Log Theorems: 241 ulog_mult |- !m n. ulog (m * n) <= ulog m + ulog n 242 ulog_exp |- !m n. ulog (m ** n) <= n * ulog m 243 ulog_even |- !n. 0 < n /\ EVEN n ==> (ulog n = 1 + ulog (HALF n)) 244 ulog_odd |- !n. 1 < n /\ ODD n ==> ulog (HALF n) + 1 <= ulog n 245 ulog_half |- !n. 1 < n ==> ulog (HALF n) + 1 <= ulog n 246 sqrt_upper |- !n. SQRT n <= 2 ** ulog n 247 248 Power Free up to a limit: 249 power_free_upto_def |- !n k. n power_free_upto k <=> !j. 1 < j /\ j <= k ==> ROOT j n ** j <> n 250 power_free_upto_0 |- !n. n power_free_upto 0 <=> T 251 power_free_upto_1 |- !n. n power_free_upto 1 <=> T 252 power_free_upto_suc |- !n k. 0 < k /\ n power_free_upto k ==> 253 (n power_free_upto k + 1 <=> ROOT (k + 1) n ** (k + 1) <> n) 254 power_free_check_upto_LOG2 |- !n. power_free n <=> 1 < n /\ n power_free_upto LOG2 n 255 power_free_check_upto_ulog |- !n. power_free n <=> 1 < n /\ n power_free_upto ulog n 256 power_free_check_upto |- !n b. LOG2 n <= b ==> (power_free n <=> 1 < n /\ n power_free_upto b) 257 power_free_2 |- power_free 2 258 power_free_3 |- power_free 3 259 power_free_test_def |- !n. power_free_test n <=> 1 < n /\ n power_free_upto ulog n 260 power_free_test_eqn |- !n. power_free_test n <=> power_free n 261 power_free_test_upto_LOG2 |- !n. power_free n <=> 262 1 < n /\ !j. 1 < j /\ j <= LOG2 n ==> ROOT j n ** j <> n 263 power_free_test_upto_ulog |- !n. power_free n <=> 264 1 < n /\ !j. 1 < j /\ j <= ulog n ==> ROOT j n ** j <> n 265 266 Another Characterisation of Power Free: 267 power_index_def |- !n k. power_index n k = 268 if k <= 1 then 1 269 else if ROOT k n ** k = n then k 270 else power_index n (k - 1) 271 power_index_0 |- !n. power_index n 0 = 1 272 power_index_1 |- !n. power_index n 1 = 1 273 power_index_eqn |- !n k. ROOT (power_index n k) n ** power_index n k = n 274 power_index_root |- !n k. perfect_power n (ROOT (power_index n k) n) 275 power_index_of_1 |- !k. power_index 1 k = if k = 0 then 1 else k 276 power_index_exact_root |- !n k. 0 < k /\ (ROOT k n ** k = n) ==> (power_index n k = k) 277 power_index_not_exact_root |- !n k. ROOT k n ** k <> n ==> (power_index n k = power_index n (k - 1)) 278 power_index_no_exact_roots |- !m n k. k <= m /\ (!j. k < j /\ j <= m ==> ROOT j n ** j <> n) ==> 279 (power_index n m = power_index n k) 280 power_index_lower |- !m n k. k <= m /\ (ROOT k n ** k = n) ==> k <= power_index n m 281 power_index_pos |- !n k. 0 < power_index n k 282 power_index_upper |- !n k. 0 < k ==> power_index n k <= k 283 power_index_equal |- !m n k. 0 < k /\ k <= m ==> 284 ((power_index n m = power_index n k) <=> !j. k < j /\ j <= m ==> ROOT j n ** j <> n) 285 power_index_property |- !m n k. (power_index n m = k) ==> !j. k < j /\ j <= m ==> ROOT j n ** j <> n 286 287 power_free_by_power_index_LOG2 288 |- !n. power_free n <=> 1 < n /\ (power_index n (LOG2 n) = 1) 289 power_free_by_power_index_ulog 290 |- !n. power_free n <=> 1 < n /\ (power_index n (ulog n) = 1) 291 292*) 293 294(* ------------------------------------------------------------------------- *) 295(* ROOT Computation *) 296(* ------------------------------------------------------------------------- *) 297 298(* Theorem: ROOT n (a ** n) = a *) 299(* Proof: 300 Since a < SUC a by LESS_SUC 301 a ** n < (SUC a) ** n by EXP_BASE_LT_MONO 302 Let b = a ** n, 303 Then a ** n <= b by LESS_EQ_REFL 304 and b < (SUC a) ** n by above 305 Hence a = ROOT n b by ROOT_UNIQUE 306*) 307val ROOT_POWER = store_thm( 308 "ROOT_POWER", 309 ``!a n. 1 < a /\ 0 < n ==> (ROOT n (a ** n) = a)``, 310 rw[EXP_BASE_LT_MONO, ROOT_UNIQUE]); 311 312(* Theorem: 0 < m /\ (b ** m = n) ==> (b = ROOT m n) *) 313(* Proof: 314 Note n <= n by LESS_EQ_REFL 315 so b ** m <= n by b ** m = n 316 Also b < SUC b by LESS_SUC 317 so b ** m < (SUC b) ** m by EXP_EXP_LT_MONO, 0 < m 318 so n < (SUC b) ** m by b ** m = n 319 Thus b = ROOT m n by ROOT_UNIQUE 320*) 321val ROOT_FROM_POWER = store_thm( 322 "ROOT_FROM_POWER", 323 ``!m n b. 0 < m /\ (b ** m = n) ==> (b = ROOT m n)``, 324 rpt strip_tac >> 325 rw[ROOT_UNIQUE]); 326 327(* Theorem: 0 < m ==> (ROOT m 0 = 0) *) 328(* Proof: 329 Note 0 ** m = 0 by EXP_0 330 Thus 0 = ROOT m 0 by ROOT_FROM_POWER 331*) 332val ROOT_OF_0 = store_thm( 333 "ROOT_OF_0[simp]", 334 ``!m. 0 < m ==> (ROOT m 0 = 0)``, 335 rw[ROOT_FROM_POWER]); 336 337(* Theorem: 0 < m ==> (ROOT m 1 = 1) *) 338(* Proof: 339 Note 1 ** m = 1 by EXP_1 340 Thus 1 = ROOT m 1 by ROOT_FROM_POWER 341*) 342val ROOT_OF_1 = store_thm( 343 "ROOT_OF_1[simp]", 344 ``!m. 0 < m ==> (ROOT m 1 = 1)``, 345 rw[ROOT_FROM_POWER]); 346 347(* Theorem: 0 < r ==> !n p. (ROOT r n = p) <=> (p ** r <= n /\ n < SUC p ** r) *) 348(* Proof: 349 If part: 0 < r ==> ROOT r n ** r <= n /\ n < SUC (ROOT r n) ** r 350 This is true by ROOT, 0 < r 351 Only-if part: p ** r <= n /\ n < SUC p ** r ==> ROOT r n = p 352 This is true by ROOT_UNIQUE 353*) 354val ROOT_THM = store_thm( 355 "ROOT_THM", 356 ``!r. 0 < r ==> !n p. (ROOT r n = p) <=> (p ** r <= n /\ n < SUC p ** r)``, 357 metis_tac[ROOT, ROOT_UNIQUE]); 358 359(* Rework proof of ROOT_COMPUTE in logroot theory. *) 360(* ./num/extra_theories/logrootScript.sml *) 361 362(* ROOT r n = r-th root of n. 363 364Make use of indentity: 365n ^ (1/r) = 2 (n/ 2^r) ^(1/r) 366 367if n = 0 then 0 368else (* precompute *) let x = 2 * r-th root of (n DIV (2 ** r)) 369 (* apply *) in if n < (SUC x) ** r then x else (SUC x) 370*) 371 372(* 373 374val lem = prove(``0 < r ==> (0 ** r = 0)``, RW_TAC arith_ss [EXP_EQ_0]); 375 376val ROOT_COMPUTE = Q.store_thm("ROOT_COMPUTE", 377 `!r n. 378 0 < r ==> 379 (ROOT r 0 = 0) /\ 380 (ROOT r n = let x = 2 * ROOT r (n DIV 2 ** r) in 381 if n < SUC x ** r then x else SUC x)`, 382 RW_TAC (arith_ss ++ boolSimps.LET_ss) [] 383 THEN MATCH_MP_TAC ROOT_UNIQUE 384 THEN CONJ_TAC 385 THEN FULL_SIMP_TAC arith_ss [NOT_LESS, EXP_1, lem] 386 THEN MAP_FIRST MATCH_MP_TAC 387 [LESS_EQ_TRANS, DECIDE ``!a b c. a < b /\ b <= c ==> a < c``] 388 THENL [ 389 Q.EXISTS_TAC `ROOT r n ** r`, 390 Q.EXISTS_TAC `SUC (ROOT r n) ** r`] 391 THEN RW_TAC arith_ss 392 [ROOT, GSYM EXP_LE_ISO, GSYM ROOT_DIV, DECIDE ``0 < 2n``] 393 THEN METIS_TAC 394 [DIVISION, MULT_COMM, DECIDE ``0 < 2n``, 395 DECIDE ``(a = b + c) ==> b <= a:num``, ADD1, LE_ADD_LCANCEL, 396 DECIDE ``a <= 1 = a < 2n``]); 397 398> ROOT_COMPUTE; 399val it = 400 |- !r n. 401 0 < r ==> 402 (ROOT r 0 = 0) /\ 403 (ROOT r n = 404 (let x = 2 * ROOT r (n DIV 2 ** r) 405 in 406 if n < SUC x ** r then x else SUC x)): 407 thm 408*) 409 410(* Theorem: 0 < m ==> !n. (ROOT m n = 0) <=> (n = 0) *) 411(* Proof: 412 If part: ROOT m n = 0 ==> n = 0 413 Note n < SUC (ROOT m n) ** r by ROOT 414 or n < SUC 0 ** m by ROOT m n = 0 415 so n < 1 by ONE, EXP_1 416 or n = 0 by arithmetic 417 Only-if part: ROOT m 0 = 0, true by ROOT_OF_0 418*) 419val ROOT_EQ_0 = store_thm( 420 "ROOT_EQ_0", 421 ``!m. 0 < m ==> !n. (ROOT m n = 0) <=> (n = 0)``, 422 rw[EQ_IMP_THM] >> 423 `n < 1` by metis_tac[ROOT, EXP_1, ONE] >> 424 decide_tac); 425 426(* Theorem: ROOT 1 n = n *) 427(* Proof: 428 Note n ** 1 = n by EXP_1 429 so n ** 1 <= n 430 Also n < SUC n by LESS_SUC 431 so n < SUC n ** 1 by EXP_1 432 Thus ROOT 1 n = n by ROOT_UNIQUE 433*) 434val ROOT_1 = store_thm( 435 "ROOT_1[simp]", 436 ``!n. ROOT 1 n = n``, 437 rw[ROOT_UNIQUE]); 438 439(* This is a rework of logrootTheory.ROOT_COMPUTE *) 440 441(* Theorem: 0 < r ==> (ROOT r 0 = 0) /\ 442 (ROOT r n = let x = 2 * ROOT r (n DIV 2 ** r) in if n < SUC x ** r then x else SUC x) *) 443(* Proof: 444 This is to show: 445 (1) ROOT r 0 = 0, true by ROOT_EQ_0 446 (2) ROOT r n = (let x = 2 * ROOT r (n DIV 2 ** r) in if n < SUC x ** r then x else SUC x) 447 Let x = 2 * ROOT r (n DIV 2 ** r). 448 To show: ROOT r n = if n < SUC x ** r then x else SUC x 449 By ROOT_UNIQUE, this is to show: 450 (1) n < SUC (if n < SUC x ** r then x else SUC x) ** r 451 If n < SUC x ** r, to show: n < SUC x ** r, true trivially 452 If ~(n < SUC x ** r), to show: n < SUC (SUC x) ** r 453 Let y = SUC (ROOT r n) ** r. 454 Then n < y by ROOT 455 and ROOT r n <= SUC (2 * HALF (ROOT r n)) by TWO_HALF_LESS_EQ 456 But x = 2 * HALF (ROOT r n) by ROOT_DIV 457 so ROOT r n <= SUC x by above 458 or y <= SUC (SUC x) ** r by EXP_LE_ISO 459 Thus n < SUC (SUC x) ** r by LESS_LESS_EQ_TRANS 460 461 (2) (if n < SUC x ** r then x else SUC x) ** r <= n 462 If n < SUC x ** r, to show: x ** r <= n 463 Let y = ROOT r n ** r. 464 Then y <= n by ROOT 465 and 2 * HALF (ROOT r n) <= ROOT r n by TWO_HALF_LESS_EQ 466 But x = 2 * HALF (ROOT r n) by ROOT_DIV 467 so x <= ROOT r n by above 468 or x ** r <= y by EXP_LE_ISO 469 Thus x ** r <= n by LESS_EQ_TRANS 470 471*) 472val ROOT_compute = store_thm( 473 "ROOT_compute", 474 ``!r n. 0 < r ==> (ROOT r 0 = 0) /\ 475 (ROOT r n = let x = 2 * ROOT r (n DIV 2 ** r) in 476 if n < SUC x ** r then x else SUC x)``, 477 rpt strip_tac >- 478 rw[ROOT_EQ_0] >> 479 rw_tac std_ss[] >> 480 (irule ROOT_UNIQUE >> rpt conj_tac >> simp[]) >| [ 481 rw[] >> 482 `x = 2 * HALF (ROOT r n)` by rw[ROOT_DIV, Abbr`x`] >> 483 qabbrev_tac `y = SUC (ROOT r n) ** r` >> 484 `n < y` by rw[ROOT, Abbr`y`] >> 485 `ROOT r n <= SUC x` by rw[TWO_HALF_LESS_EQ] >> 486 `y <= SUC (SUC x) ** r` by rw[EXP_LE_ISO, Abbr`y`] >> 487 decide_tac, 488 rw[] >> 489 `x = 2 * HALF (ROOT r n)` by rw[ROOT_DIV, Abbr`x`] >> 490 qabbrev_tac `y = ROOT r n ** r` >> 491 `y <= n` by rw[ROOT, Abbr`y`] >> 492 `x <= ROOT r n` by rw[TWO_HALF_LESS_EQ] >> 493 `x ** r <= y` by rw[EXP_LE_ISO, Abbr`y`] >> 494 decide_tac 495 ]); 496 497(* Theorem: 0 < r ==> (ROOT r n = 498 let m = 2 * ROOT r (n DIV 2 ** r) in m + if (m + 1) ** r <= n then 1 else 0) *) 499(* Proof: 500 ROOT k n 501 = if n < SUC m ** k then m else SUC m by ROOT_COMPUTE 502 = if SUC m ** k <= n then SUC m else m by logic 503 = if (m + 1) ** k <= n then (m + 1) else m by ADD1 504 = m + if (m + 1) ** k <= n then 1 else 0 by arithmetic 505*) 506val ROOT_EQN = store_thm( 507 "ROOT_EQN", 508 ``!r n. 0 < r ==> (ROOT r n = 509 let m = 2 * ROOT r (n DIV 2 ** r) in m + if (m + 1) ** r <= n then 1 else 0)``, 510 rw_tac std_ss[] >> 511 Cases_on `(m + 1) ** r <= n` >- 512 rw[ROOT_COMPUTE, ADD1] >> 513 rw[ROOT_COMPUTE, ADD1]); 514 515(* Theorem: ROOT r n = 516 if r = 0 then ROOT 0 n else 517 if n = 0 then 0 else 518 let m = TWICE (ROOT r (n DIV 2 ** r)) in 519 m + if (SUC m) ** r <= n then 1 else 0 *) 520(* Proof: by ROOT_OF_0, ROOT_EQN *) 521val ROOT_EVAL = store_thm( 522 "ROOT_EVAL[compute]", (* put in computeLib *) 523 ``!r n. ROOT r n = 524 if r = 0 then ROOT 0 n else 525 if n = 0 then 0 else 526 let m = TWICE (ROOT r (n DIV 2 ** r)) in 527 m + if (SUC m) ** r <= n then 1 else 0``, 528 metis_tac[ROOT_OF_0, ROOT_EQN, ADD1, NOT_ZERO_LT_ZERO]); 529(* Put ROOT_EVAL into computeLib *) 530 531(* 532> EVAL ``ROOT 3 125``; 533val it = |- ROOT 3 125 = 5: thm 534> EVAL ``ROOT 3 100``; 535val it = |- ROOT 3 100 = 4: thm 536> EVAL ``MAP (ROOT 3) [1 .. 20]``; = 537 [1; 1; 1; 1; 1; 1; 1; 2; 2; 2; 2; 2; 2; 2; 2; 2; 2; 2; 2; 2]: thm 538> EVAL ``MAP (ROOT 3) [1 .. 30]``; = 539 [1; 1; 1; 1; 1; 1; 1; 2; 2; 2; 2; 2; 2; 2; 2; 2; 2; 2; 2; 2; 2; 2; 2; 2; 2; 2; 3; 3; 3; 3]: thm 540*) 541 542(* Theorem: 0 < r ==> 543 (ROOT r (SUC n) = ROOT r n + if SUC n = (SUC (ROOT r n)) ** r then 1 else 0) *) 544(* Proof: 545 Let x = ROOT r n, y = ROOT r (SUC n). x <= y. 546 Note n < (SUC x) ** r /\ x ** r <= n by ROOT_THM 547 and SUC n < (SUC y) ** r /\ y ** r <= SUC n by ROOT_THM 548 Since n < (SUC x) ** r, 549 SUC n <= (SUC x) ** r. 550 If SUC n = (SUC x) ** r, 551 Then y = ROOT r (SUC n) 552 = ROOT r ((SUC x) ** r) 553 = SUC x by ROOT_POWER 554 If SUC n < (SUC x) ** r, 555 Then x ** r <= n < SUC n by LESS_SUC 556 Thus x = y by ROOT_THM 557*) 558val ROOT_SUC = store_thm( 559 "ROOT_SUC", 560 ``!r n. 0 < r ==> 561 (ROOT r (SUC n) = ROOT r n + if SUC n = (SUC (ROOT r n)) ** r then 1 else 0)``, 562 rpt strip_tac >> 563 qabbrev_tac `x = ROOT r n` >> 564 qabbrev_tac `y = ROOT r (SUC n)` >> 565 Cases_on `n = 0` >| [ 566 `x = 0` by rw[ROOT_OF_0, Abbr`x`] >> 567 `y = 1` by rw[ROOT_OF_1, Abbr`y`] >> 568 simp[], 569 `x <> 0` by rw[ROOT_EQ_0, Abbr`x`] >> 570 `n < (SUC x) ** r /\ x ** r <= n` by metis_tac[ROOT_THM] >> 571 `SUC n < (SUC y) ** r /\ y ** r <= SUC n` by metis_tac[ROOT_THM] >> 572 `(SUC n = (SUC x) ** r) \/ SUC n < (SUC x) ** r` by decide_tac >| [ 573 `1 < SUC x` by decide_tac >> 574 `y = SUC x` by metis_tac[ROOT_POWER] >> 575 simp[], 576 `x ** r <= SUC n` by decide_tac >> 577 `x = y` by metis_tac[ROOT_THM] >> 578 simp[] 579 ] 580 ]); 581 582(* 583ROOT_SUC; 584|- !r n. 0 < r ==> ROOT r (SUC n) = ROOT r n + if SUC n = SUC (ROOT r n) ** r then 1 else 0 585Let z = ROOT r n. 586 587 z(n) 588 ------------------------------------------------- 589 n (n+1=(z+1)**r) 590 591> EVAL ``MAP (ROOT 2) [1 .. 20]``; 592val it = |- MAP (ROOT 2) [1 .. 20] = 593 [1; 1; 1; 2; 2; 2; 2; 2; 3; 3; 3; 3; 3; 3; 3; 4; 4; 4; 4; 4]: thm 594 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 595*) 596 597(* Theorem: 0 < m ==> !n. (ROOT m n = 1) <=> (0 < n /\ n < 2 ** m) *) 598(* Proof: 599 ROOT m n = 1 600 <=> 1 ** m <= n /\ n < (SUC 1) ** m by ROOT_THM, 0 < m 601 <=> 1 <= n /\ n < 2 ** m by TWO, EXP_1 602 <=> 0 < n /\ n < 2 ** m by arithmetic 603*) 604val ROOT_EQ_1 = store_thm( 605 "ROOT_EQ_1", 606 ``!m. 0 < m ==> !n. (ROOT m n = 1) <=> (0 < n /\ n < 2 ** m)``, 607 rpt strip_tac >> 608 `!n. 0 < n <=> 1 <= n` by decide_tac >> 609 metis_tac[ROOT_THM, TWO, EXP_1]); 610 611(* Theorem: 0 < m ==> ROOT m n <= n *) 612(* Proof: 613 Let r = ROOT m n. 614 Note r <= r ** m by X_LE_X_EXP, 0 < m 615 <= n by ROOT 616*) 617val ROOT_LE_SELF = store_thm( 618 "ROOT_LE_SELF", 619 ``!m n. 0 < m ==> ROOT m n <= n``, 620 metis_tac[X_LE_X_EXP, ROOT, LESS_EQ_TRANS]); 621 622(* Theorem: 0 < m ==> ((ROOT m n = n) <=> ((m = 1) \/ (n = 0) \/ (n = 1))) *) 623(* Proof: 624 If part: ROOT m n = n ==> m = 1 \/ n = 0 \/ n = 1 625 Note n ** m <= n by ROOT, 0 < r 626 But n <= n ** m by X_LE_X_EXP, 0 < m 627 so n ** m = n by EQ_LESS_EQ 628 ==> m = 1 or n = 0 or n = 1 by EXP_EQ_SELF 629 Only-if part: ROOT 1 n = n /\ ROOT m 0 = 0 /\ ROOT m 1 = 1 630 True by ROOT_1, ROOT_OF_0, ROOT_OF_1. 631*) 632val ROOT_EQ_SELF = store_thm( 633 "ROOT_EQ_SELF", 634 ``!m n. 0 < m ==> ((ROOT m n = n) <=> ((m = 1) \/ (n = 0) \/ (n = 1)))``, 635 (rw_tac std_ss[EQ_IMP_THM] >> rw[]) >> 636 `n ** m <= n` by metis_tac[ROOT] >> 637 `n <= n ** m` by rw[X_LE_X_EXP] >> 638 `n ** m = n` by decide_tac >> 639 rw[GSYM EXP_EQ_SELF]); 640 641(* Theorem: 0 < m ==> (n <= ROOT m n <=> ((m = 1) \/ (n = 0) \/ (n = 1))) *) 642(* Proof: 643 Note ROOT m n <= n by ROOT_LE_SELF 644 Thus n <= ROOT m n <=> ROOT m n = n by EQ_LESS_EQ 645 The result follows by ROOT_EQ_SELF 646*) 647val ROOT_GE_SELF = store_thm( 648 "ROOT_GE_SELF", 649 ``!m n. 0 < m ==> (n <= ROOT m n <=> ((m = 1) \/ (n = 0) \/ (n = 1)))``, 650 metis_tac[ROOT_LE_SELF, ROOT_EQ_SELF, EQ_LESS_EQ]); 651 652(* 653EVAL ``MAP (\k. ROOT k 100) [1 .. 10]``; = [100; 10; 4; 3; 2; 2; 1; 1; 1; 1]: thm 654 655This shows (ROOT k) is a decreasing function of k, 656but this is very hard to prove without some real number theory. 657Even this is hard to prove: ROOT 3 n <= ROOT 2 n 658 659No! -- this can be proved, see below. 660*) 661 662(* Theorem: 0 < a /\ a <= b ==> ROOT b n <= ROOT a n *) 663(* Proof: 664 Let x = ROOT a n, y = ROOT b n. To show: y <= x. 665 By contradiction, suppose x < y. 666 Then SUC x <= y. 667 Note x ** a <= n /\ n < (SUC x) ** a by ROOT 668 and y ** b <= n /\ n < (SUC y) ** b by ROOT 669 But a <= b 670 (SUC x) ** a 671 <= (SUC x) ** b by EXP_BASE_LEQ_MONO_IMP, 0 < SUC x, a <= b 672 <= y ** b by EXP_EXP_LE_MONO, 0 < b 673 This leads to n < (SUC x) ** a <= y ** b <= n, a contradiction. 674*) 675val ROOT_LE_REVERSE = store_thm( 676 "ROOT_LE_REVERSE", 677 ``!a b n. 0 < a /\ a <= b ==> ROOT b n <= ROOT a n``, 678 rpt strip_tac >> 679 qabbrev_tac `x = ROOT a n` >> 680 qabbrev_tac `y = ROOT b n` >> 681 spose_not_then strip_assume_tac >> 682 `0 < b /\ SUC x <= y` by decide_tac >> 683 `x ** a <= n /\ n < (SUC x) ** a` by rw[ROOT, Abbr`x`] >> 684 `y ** b <= n /\ n < (SUC y) ** b` by rw[ROOT, Abbr`y`] >> 685 `(SUC x) ** a <= (SUC x) ** b` by rw[EXP_BASE_LEQ_MONO_IMP] >> 686 `(SUC x) ** b <= y ** b` by rw[EXP_EXP_LE_MONO] >> 687 decide_tac); 688 689 690(* ------------------------------------------------------------------------- *) 691(* Square Root *) 692(* ------------------------------------------------------------------------- *) 693(* Use overload for SQRT *) 694val _ = overload_on ("SQRT", ``\n. ROOT 2 n``); 695 696(* 697> EVAL ``SQRT 4``; 698val it = |- SQRT 4 = 2: thm 699> EVAL ``(SQRT 4) ** 2``; 700val it = |- SQRT 4 ** 2 = 4: thm 701> EVAL ``(SQRT 5) ** 2``; 702val it = |- SQRT 5 ** 2 = 4: thm 703> EVAL ``(SQRT 8) ** 2``; 704val it = |- SQRT 8 ** 2 = 4: thm 705> EVAL ``(SQRT 9) ** 2``; 706val it = |- SQRT 9 ** 2 = 9: thm 707 708> EVAL ``LOG2 4``; 709val it = |- LOG2 4 = 2: thm 710> EVAL ``2 ** (LOG2 4)``; 711val it = |- 2 ** LOG2 4 = 4: thm 712> EVAL ``2 ** (LOG2 5)``; 713val it = |- 2 ** LOG2 5 = 4: thm 714> EVAL ``2 ** (LOG2 6)``; 715val it = |- 2 ** LOG2 6 = 4: thm 716> EVAL ``2 ** (LOG2 7)``; 717val it = |- 2 ** LOG2 7 = 4: thm 718> EVAL ``2 ** (LOG2 8)``; 719val it = |- 2 ** LOG2 8 = 8: thm 720 721> EVAL ``SQRT 9``; 722val it = |- SQRT 9 = 3: thm 723> EVAL ``SQRT 8``; 724val it = |- SQRT 8 = 2: thm 725> EVAL ``SQRT 7``; 726val it = |- SQRT 7 = 2: thm 727> EVAL ``SQRT 6``; 728val it = |- SQRT 6 = 2: thm 729> EVAL ``SQRT 5``; 730val it = |- SQRT 5 = 2: thm 731> EVAL ``SQRT 4``; 732val it = |- SQRT 4 = 2: thm 733> EVAL ``SQRT 3``; 734val it = |- SQRT 3 = 1: thm 735*) 736 737(* 738EXP_BASE_LT_MONO |- !b. 1 < b ==> !n m. b ** m < b ** n <=> m < n 739LT_EXP_ISO |- !e a b. 1 < e ==> (a < b <=> e ** a < e ** b) 740 741ROOT_exists |- !r n. 0 < r ==> ?rt. rt ** r <= n /\ n < SUC rt ** r 742ROOT_UNIQUE |- !r n p. p ** r <= n /\ n < SUC p ** r ==> (ROOT r n = p) 743ROOT_LE_MONO |- !r x y. 0 < r ==> x <= y ==> ROOT r x <= ROOT r y 744 745LOG_exists |- ?f. !a n. 1 < a /\ 0 < n ==> a ** f a n <= n /\ n < a ** SUC (f a n) 746LOG_UNIQUE |- !a n p. a ** p <= n /\ n < a ** SUC p ==> (LOG a n = p) 747LOG_LE_MONO |- !a x y. 1 < a /\ 0 < x ==> x <= y ==> LOG a x <= LOG a y 748 749LOG_EXP |- !n a b. 1 < a /\ 0 < b ==> (LOG a (a ** n * b) = n + LOG a b) 750LOG |- !a n. 1 < a /\ 0 < n ==> a ** LOG a n <= n /\ n < a ** SUC (LOG a n) 751*) 752 753(* Theorem: 0 < n ==> (SQRT n) ** 2 <= n /\ n < SUC (SQRT n) ** 2 *) 754(* Proof: by ROOT: 755 |- !r n. 0 < r ==> ROOT r n ** r <= n /\ n < SUC (ROOT r n) ** r 756*) 757val SQRT_PROPERTY = store_thm( 758 "SQRT_PROPERTY", 759 ``!n. (SQRT n) ** 2 <= n /\ n < SUC (SQRT n) ** 2``, 760 rw[ROOT]); 761 762(* Obtain a theorem *) 763val SQRT_THM = save_thm("SQRT_THM", 764 ROOT_THM |> SPEC ``2`` |> SIMP_RULE (srw_ss())[]); 765(* val SQRT_THM = |- !n p. (SQRT n = p) <=> p ** 2 <= n /\ n < SUC p ** 2: thm *) 766 767(* Theorem: SQ (SQRT n) <= n *) 768(* Proof: by SQRT_PROPERTY, EXP_2 *) 769val SQ_SQRT_LE = store_thm( 770 "SQ_SQRT_LE", 771 ``!n. SQ (SQRT n) <= n``, 772 metis_tac[SQRT_PROPERTY, EXP_2]); 773 774(* Theorem: n <= m ==> SQRT n <= SQRT m *) 775(* Proof: by ROOT_LE_MONO *) 776val SQRT_LE = store_thm( 777 "SQRT_LE", 778 ``!n m. n <= m ==> SQRT n <= SQRT m``, 779 rw[ROOT_LE_MONO]); 780 781(* Theorem: n < m ==> SQRT n <= SQRT m *) 782(* Proof: 783 Since n < m ==> n <= m by LESS_IMP_LESS_OR_EQ 784 This is true by ROOT_LE_MONO 785*) 786val SQRT_LT = store_thm( 787 "SQRT_LT", 788 ``!n m. n < m ==> SQRT n <= SQRT m``, 789 rw[ROOT_LE_MONO, LESS_IMP_LESS_OR_EQ]); 790 791(* Theorem: SQRT 0 = 0 *) 792(* Proof: by ROOT_OF_0 *) 793val SQRT_0 = store_thm( 794 "SQRT_0[simp]", 795 ``SQRT 0 = 0``, 796 rw[]); 797 798(* Theorem: SQRT 1 = 1 *) 799(* Proof: by ROOT_OF_1 *) 800val SQRT_1 = store_thm( 801 "SQRT_1[simp]", 802 ``SQRT 1 = 1``, 803 rw[]); 804 805(* Theorem: SQRT n = 0 <=> n = 0 *) 806(* Proof: 807 If part: SQRT n = 0 ==> n = 0. 808 By contradiction, suppose n <> 0. 809 This means 1 <= n 810 Hence SQRT 1 <= SQRT n by SQRT_LE 811 so 1 <= SQRT n by SQRT_1 812 This contradicts SQRT n = 0. 813 Only-if part: n = 0 ==> SQRT n = 0 814 True since SQRT 0 = 0 by SQRT_0 815*) 816val SQRT_EQ_0 = store_thm( 817 "SQRT_EQ_0", 818 ``!n. (SQRT n = 0) <=> (n = 0)``, 819 rw[EQ_IMP_THM] >> 820 spose_not_then strip_assume_tac >> 821 `1 <= n` by decide_tac >> 822 `SQRT 1 <= SQRT n` by rw[SQRT_LE] >> 823 `SQRT 1 = 1` by rw[] >> 824 decide_tac); 825 826(* Theorem: SQRT n = 1 <=> n = 1 \/ n = 2 \/ n = 3 *) 827(* Proof: 828 If part: SQRT n = 1 ==> (n = 1) \/ (n = 2) \/ (n = 3). 829 By contradiction, suppose n <> 1 /\ n <> 2 /\ n <> 3. 830 Note n <> 0 by SQRT_EQ_0 831 This means 4 <= n 832 Hence SQRT 4 <= SQRT n by SQRT_LE 833 so 2 <= SQRT n by EVAL_TAC, SQRT 4 = 2 834 This contradicts SQRT n = 1. 835 Only-if part: n = 1 \/ n = 2 \/ n = 3 ==> SQRT n = 1 836 All these are true by EVAL_TAC 837*) 838val SQRT_EQ_1 = store_thm( 839 "SQRT_EQ_1", 840 ``!n. (SQRT n = 1) <=> ((n = 1) \/ (n = 2) \/ (n = 3))``, 841 rw[EQ_IMP_THM] >| [ 842 spose_not_then strip_assume_tac >> 843 `n <> 0` by metis_tac[SQRT_EQ_0] >> 844 `4 <= n` by decide_tac >> 845 `SQRT 4 <= SQRT n` by rw[SQRT_LE] >> 846 `SQRT 4 = 2` by EVAL_TAC >> 847 decide_tac, 848 EVAL_TAC, 849 EVAL_TAC, 850 EVAL_TAC 851 ]); 852 853(* Theorem: SQRT (n ** 2) = n *) 854(* Proof: 855 If 1 < n, true by ROOT_POWER, 0 < 2 856 Otherwise, n = 0 or n = 1. 857 When n = 0, 858 SQRT (0 ** 2) = SQRT 0 = 0 by SQRT_0 859 When n = 1, 860 SQRT (1 ** 2) = SQRT 1 = 1 by SQRT_1 861*) 862val SQRT_EXP_2 = store_thm( 863 "SQRT_EXP_2", 864 ``!n. SQRT (n ** 2) = n``, 865 rpt strip_tac >> 866 Cases_on `1 < n` >- 867 fs[ROOT_POWER] >> 868 `(n = 0) \/ (n = 1)` by decide_tac >> 869 rw[]); 870 871(* Theorem alias *) 872val SQRT_OF_SQ = save_thm("SQRT_OF_SQ", SQRT_EXP_2); 873(* val SQRT_OF_SQ = |- !n. SQRT (n ** 2) = n: thm *) 874 875(* Theorem: SQRT (SQ n) = n *) 876(* Proof: 877 SQRT (SQ n) 878 = SQRT (n ** 2) by EXP_2 879 = n by SQRT_EXP_2 880*) 881val SQRT_SQ = store_thm( 882 "SQRT_SQ", 883 ``!n. SQRT (SQ n) = n``, 884 metis_tac[SQRT_EXP_2, EXP_2]); 885 886(* Theorem: SQRT n <= n *) 887(* Proof: 888 Note n <= n ** 2 by SELF_LE_SQ 889 Thus SQRT n <= SQRT (n ** 2) by SQRT_LE 890 or SQRT n <= n by SQRT_EXP_2 891*) 892val SQRT_LE_SELF = store_thm( 893 "SQRT_LE_SELF", 894 ``!n. SQRT n <= n``, 895 metis_tac[SELF_LE_SQ, SQRT_LE, SQRT_EXP_2]); 896 897(* Theorem: (n <= SQRT n) <=> ((n = 0) \/ (n = 1)) *) 898(* Proof: 899 If part: (n <= SQRT n) ==> ((n = 0) \/ (n = 1)) 900 By contradiction, suppose n <> 0 /\ n <> 1. 901 Then 1 < n, implying n ** 2 <= SQRT n ** 2 by EXP_BASE_LE_MONO 902 but SQRT n ** 2 <= n by SQRT_PROPERTY 903 so n ** 2 <= n by LESS_EQ_TRANS 904 or n * n <= n * 1 by EXP_2 905 or n <= 1 by LE_MULT_LCANCEL, n <> 0. 906 This contradicts 1 < n. 907 Only-if part: ((n = 0) \/ (n = 1)) ==> (n <= SQRT n) 908 This is to show: 909 (1) 0 <= SQRT 0, true by SQRT 0 = 0 by SQRT_0 910 (2) 1 <= SQRT 1, true by SQRT 1 = 1 by SQRT_1 911*) 912val SQRT_GE_SELF = store_thm( 913 "SQRT_GE_SELF", 914 ``!n. (n <= SQRT n) <=> ((n = 0) \/ (n = 1))``, 915 rw[EQ_IMP_THM] >| [ 916 spose_not_then strip_assume_tac >> 917 `1 < n` by decide_tac >> 918 `n ** 2 <= SQRT n ** 2` by rw[EXP_BASE_LE_MONO] >> 919 `SQRT n ** 2 <= n` by rw[SQRT_PROPERTY] >> 920 `n ** 2 <= n` by metis_tac[LESS_EQ_TRANS] >> 921 `n * n <= n * 1` by metis_tac[EXP_2, MULT_RIGHT_1] >> 922 `n <= 1` by metis_tac[LE_MULT_LCANCEL] >> 923 decide_tac, 924 rw[], 925 rw[] 926 ]); 927 928(* Theorem: (SQRT n = n) <=> ((n = 0) \/ (n = 1)) *) 929(* Proof: by ROOT_EQ_SELF, 0 < 2 *) 930val SQRT_EQ_SELF = store_thm( 931 "SQRT_EQ_SELF", 932 ``!n. (SQRT n = n) <=> ((n = 0) \/ (n = 1))``, 933 rw[ROOT_EQ_SELF]); 934 935(* Theorem: SQRT n <= m ==> n <= 3 * (m ** 2) *) 936(* Proof: 937 Note n < (SUC (SQRT n)) ** 2 by SQRT_PROPERTY 938 = SUC ((SQRT n) ** 2) + 2 * SQRT n by SUC_SQ 939 Thus n <= m ** 2 + 2 * m by SQRT n <= m 940 <= m ** 2 + 2 * m ** 2 by arithmetic 941 = 3 * m ** 2 942*) 943val SQRT_LE_IMP = store_thm( 944 "SQRT_LE_IMP", 945 ``!n m. SQRT n <= m ==> n <= 3 * (m ** 2)``, 946 rpt strip_tac >> 947 `n < (SUC (SQRT n)) ** 2` by rw[SQRT_PROPERTY] >> 948 `SUC (SQRT n) ** 2 = SUC ((SQRT n) ** 2) + 2 * SQRT n` by rw[SUC_SQ] >> 949 `SQRT n ** 2 <= m ** 2` by rw[] >> 950 `2 * SQRT n <= 2 * m` by rw[] >> 951 `2 * m <= 2 * m * m` by rw[] >> 952 `2 * m * m = 2 * m ** 2` by rw[] >> 953 decide_tac); 954 955(* ------------------------------------------------------------------------- *) 956(* Logarithm *) 957(* ------------------------------------------------------------------------- *) 958 959(* Theorem: 1 < a ==> LOG a (a ** n) = n *) 960(* Proof: 961 LOG a (a ** n) 962 = LOG a ((a ** n) * 1) by MULT_RIGHT_1 963 = n + LOG a 1 by LOG_EXP 964 = n + 0 by LOG_1 965 = n by ADD_0 966*) 967val LOG_EXACT_EXP = store_thm( 968 "LOG_EXACT_EXP", 969 ``!a. 1 < a ==> !n. LOG a (a ** n) = n``, 970 metis_tac[MULT_RIGHT_1, LOG_EXP, LOG_1, ADD_0, DECIDE``0 < 1``]); 971 972(* Theorem: 1 < a /\ 0 < b /\ b <= a ** n ==> LOG a b <= n *) 973(* Proof: 974 Given b <= a ** n 975 LOG a b <= LOG a (a ** n) by LOG_LE_MONO 976 = n by LOG_EXACT_EXP 977*) 978val EXP_TO_LOG = store_thm( 979 "EXP_TO_LOG", 980 ``!a b n. 1 < a /\ 0 < b /\ b <= a ** n ==> LOG a b <= n``, 981 metis_tac[LOG_LE_MONO, LOG_EXACT_EXP]); 982 983(* Theorem: 1 < a /\ 0 < n ==> !p. (LOG a n = p) <=> (a ** p <= n /\ n < a ** SUC p) *) 984(* Proof: 985 If part: 1 < a /\ 0 < n ==> a ** LOG a n <= n /\ n < a ** SUC (LOG a n) 986 This is true by LOG. 987 Only-if part: a ** p <= n /\ n < a ** SUC p ==> LOG a n = p 988 This is true by LOG_UNIQUE 989*) 990val LOG_THM = store_thm( 991 "LOG_THM", 992 ``!a n. 1 < a /\ 0 < n ==> !p. (LOG a n = p) <=> (a ** p <= n /\ n < a ** SUC p)``, 993 metis_tac[LOG, LOG_UNIQUE]); 994 995(* Theorem: LOG m n = if m <= 1 \/ (n = 0) then LOG m n 996 else if n < m then 0 else SUC (LOG m (n DIV m)) *) 997(* Proof: by LOG_RWT *) 998val LOG_EVAL = store_thm( 999 "LOG_EVAL[compute]", 1000 ``!m n. LOG m n = if m <= 1 \/ (n = 0) then LOG m n 1001 else if n < m then 0 else SUC (LOG m (n DIV m))``, 1002 rw[LOG_RWT]); 1003(* Put to computeLib for LOG evaluation of any base *) 1004 1005(* 1006> EVAL ``MAP (LOG 3) [1 .. 20]``; = 1007 [0; 0; 1; 1; 1; 1; 1; 1; 2; 2; 2; 2; 2; 2; 2; 2; 2; 2; 2; 2]: thm 1008> EVAL ``MAP (LOG 3) [1 .. 30]``; = 1009 [0; 0; 1; 1; 1; 1; 1; 1; 2; 2; 2; 2; 2; 2; 2; 2; 2; 2; 2; 2; 2; 2; 2; 2; 2; 2; 3; 3; 3; 3]: thm 1010*) 1011 1012(* Theorem: 1 < a /\ 0 < n ==> 1013 !p. (LOG a n = p) <=> SUC n <= a ** SUC p /\ a ** SUC p <= a * n *) 1014(* Proof: 1015 Note !p. LOG a n = p 1016 <=> n < a ** SUC p /\ a ** p <= n by LOG_THM 1017 <=> n < a ** SUC p /\ a * a ** p <= a * n by LE_MULT_LCANCEL 1018 <=> n < a ** SUC p /\ a ** SUC p <= a * n by EXP 1019 <=> SUC n <= a ** SUC p /\ a ** SUC p <= a * n by arithmetic 1020*) 1021val LOG_TEST = store_thm( 1022 "LOG_TEST", 1023 ``!a n. 1 < a /\ 0 < n ==> 1024 !p. (LOG a n = p) <=> SUC n <= a ** SUC p /\ a ** SUC p <= a * n``, 1025 rw[EQ_IMP_THM] >| [ 1026 `n < a ** SUC (LOG a n)` by metis_tac[LOG_THM] >> 1027 decide_tac, 1028 `a ** (LOG a n) <= n` by metis_tac[LOG_THM] >> 1029 rw[EXP], 1030 `a * a ** p <= a * n` by fs[EXP] >> 1031 `a ** p <= n` by fs[] >> 1032 `n < a ** SUC p` by decide_tac >> 1033 metis_tac[LOG_THM] 1034 ]); 1035 1036(* For continuous functions, log_b (x ** y) = y * log_b x. *) 1037 1038(* Theorem: 1 < b /\ 0 < x /\ 0 < n ==> 1039 n * LOG b x <= LOG b (x ** n) /\ LOG b (x ** n) < n * SUC (LOG b x) *) 1040(* Proof: 1041 Note: 1042> LOG_THM |> SPEC ``b:num`` |> SPEC ``x:num``; 1043val it = |- 1 < b /\ 0 < x ==> !p. LOG b x = p <=> b ** p <= x /\ x < b ** SUC p: thm 1044> LOG_THM |> SPEC ``b:num`` |> SPEC ``(x:num) ** n``; 1045val it = |- 1 < b /\ 0 < x ** n ==> 1046 !p. LOG b (x ** n) = p <=> b ** p <= x ** n /\ x ** n < b ** SUC p: thm 1047 1048 Let y = LOG b x, z = LOG b (x ** n). 1049 Then b ** y <= x /\ x < b ** SUC y by LOG_THM, (1) 1050 and b ** z <= x ** n /\ x ** n < b ** SUC z by LOG_THM, (2) 1051 From (1), 1052 b ** (n * y) <= x ** n /\ by EXP_EXP_LE_MONO, EXP_EXP_MULT 1053 x ** n < b ** (n * SUC y) by EXP_EXP_LT_MONO, EXP_EXP_MULT, 0 < n 1054 Cross combine with (2), 1055 b ** (n * y) <= x ** n < b ** SUC z 1056 and b ** z <= x ** n < b ** (n * y) 1057 ==> n * y < SUC z /\ z < n * SUC y by EXP_BASE_LT_MONO 1058 or n * y <= z /\ z < n * SUC y 1059*) 1060val LOG_POWER = store_thm( 1061 "LOG_POWER", 1062 ``!b x n. 1 < b /\ 0 < x /\ 0 < n ==> 1063 n * LOG b x <= LOG b (x ** n) /\ LOG b (x ** n) < n * SUC (LOG b x)``, 1064 ntac 4 strip_tac >> 1065 `0 < x ** n` by rw[] >> 1066 qabbrev_tac `y = LOG b x` >> 1067 qabbrev_tac `z = LOG b (x ** n)` >> 1068 `b ** y <= x /\ x < b ** SUC y` by metis_tac[LOG_THM] >> 1069 `b ** z <= x ** n /\ x ** n < b ** SUC z` by metis_tac[LOG_THM] >> 1070 `b ** (y * n) <= x ** n` by rw[EXP_EXP_MULT] >> 1071 `x ** n < b ** ((SUC y) * n)` by rw[EXP_EXP_MULT] >> 1072 `b ** (y * n) < b ** SUC z` by decide_tac >> 1073 `b ** z < b ** (SUC y * n)` by decide_tac >> 1074 `y * n < SUC z` by metis_tac[EXP_BASE_LT_MONO] >> 1075 `z < SUC y * n` by metis_tac[EXP_BASE_LT_MONO] >> 1076 decide_tac); 1077 1078(* Theorem: 1 < a /\ 0 < n /\ a <= b ==> LOG b n <= LOG a n *) 1079(* Proof: 1080 Let x = LOG a n, y = LOG b n. To show: y <= x. 1081 By contradiction, suppose x < y. 1082 Then SUC x <= y. 1083 Note a ** x <= n /\ n < a ** SUC x by LOG_THM 1084 and b ** y <= n /\ n < b ** SUC y by LOG_THM 1085 But a <= b 1086 a ** SUC x 1087 <= b ** SUC x by EXP_EXP_LE_MONO, 0 < SUC x 1088 <= b ** y by EXP_BASE_LEQ_MONO_IMP, SUC x <= y 1089 This leads to n < a ** SUC x <= b ** y <= n, a contradiction. 1090*) 1091val LOG_LE_REVERSE = store_thm( 1092 "LOG_LE_REVERSE", 1093 ``!a b n. 1 < a /\ 0 < n /\ a <= b ==> LOG b n <= LOG a n``, 1094 rpt strip_tac >> 1095 qabbrev_tac `x = LOG a n` >> 1096 qabbrev_tac `y = LOG b n` >> 1097 spose_not_then strip_assume_tac >> 1098 `1 < b /\ SUC x <= y` by decide_tac >> 1099 `a ** x <= n /\ n < a ** SUC x` by metis_tac[LOG_THM] >> 1100 `b ** y <= n /\ n < b ** SUC y` by metis_tac[LOG_THM] >> 1101 `a ** SUC x <= b ** SUC x` by rw[EXP_EXP_LE_MONO] >> 1102 `b ** SUC x <= b ** y` by rw[EXP_BASE_LEQ_MONO_IMP] >> 1103 decide_tac); 1104 1105(* Overload LOG base 2 *) 1106val _ = overload_on ("LOG2", ``\n. LOG 2 n``); 1107 1108(* Theorem: LOG2 1 = 0 *) 1109(* Proof: 1110 LOG_1 |> SPEC ``2``; 1111 val it = |- 1 < 2 ==> LOG2 1 = 0: thm 1112*) 1113val LOG2_1 = store_thm( 1114 "LOG2_1[simp]", 1115 ``LOG2 1 = 0``, 1116 rw[LOG_1]); 1117 1118(* Theorem: LOG2 2 = 1 *) 1119(* Proof: 1120 LOG_BASE |> SPEC ``2``; 1121 val it = |- 1 < 2 ==> LOG2 2 = 1: thm 1122*) 1123val LOG2_2 = store_thm( 1124 "LOG2_2[simp]", 1125 ``LOG2 2 = 1``, 1126 rw[LOG_BASE]); 1127 1128(* Obtain a theorem *) 1129val LOG2_THM = save_thm("LOG2_THM", 1130 LOG_THM |> SPEC ``2`` |> SIMP_RULE (srw_ss())[]); 1131(* val LOG2_THM = |- !n. 0 < n ==> !p. (LOG2 n = p) <=> 2 ** p <= n /\ n < 2 ** SUC p: thm *) 1132 1133(* Theorem: 0 < n ==> 2 ** LOG2 n <= n /\ n < 2 ** SUC (LOG2 n) *) 1134(* Proof: 1135 LOG |> SPEC ``2``; 1136 val it = |- !n. 1 < 2 /\ 0 < n ==> 2 ** LOG2 n <= n /\ n < 2 ** SUC (LOG2 n): thm 1137*) 1138val LOG2_PROPERTY = store_thm( 1139 "LOG2_PROPERTY", 1140 ``!n. 0 < n ==> 2 ** LOG2 n <= n /\ n < 2 ** SUC (LOG2 n)``, 1141 rw[LOG]); 1142 1143(* Obtain the same theorem *) 1144val LOG2_PROPERTY = save_thm("LOG2_PROPERTY", 1145 LOG |> SPEC ``2`` |> SIMP_RULE (srw_ss())[]); 1146(* val LOG2_PROPERTY = |- !n. 0 < n ==> 2 ** LOG2 n <= n /\ n < 2 ** SUC (LOG2 n): thm *) 1147 1148(* Theorem: 0 < n ==> 2 ** LOG2 n <= n) *) 1149(* Proof: by LOG2_PROPERTY *) 1150val TWO_EXP_LOG2_LE = store_thm( 1151 "TWO_EXP_LOG2_LE", 1152 ``!n. 0 < n ==> 2 ** LOG2 n <= n``, 1153 rw[LOG2_PROPERTY]); 1154 1155(* Obtain a theorem *) 1156val LOG2_UNIQUE = save_thm("LOG2_UNIQUE", 1157 LOG_UNIQUE |> SPEC ``2`` |> SPEC ``n:num`` |> SPEC ``m:num`` |> GEN_ALL); 1158(* val LOG2_UNIQUE = |- !n m. 2 ** m <= n /\ n < 2 ** SUC m ==> LOG2 n = m: thm *) 1159 1160(* Theorem: 0 < n ==> ((LOG2 n = 0) <=> (n = 1)) *) 1161(* Proof: 1162 LOG_EQ_0 |> SPEC ``2``; 1163 |- !b. 1 < 2 /\ 0 < b ==> (LOG2 b = 0 <=> b < 2) 1164*) 1165val LOG2_EQ_0 = store_thm( 1166 "LOG2_EQ_0", 1167 ``!n. 0 < n ==> ((LOG2 n = 0) <=> (n = 1))``, 1168 rw[LOG_EQ_0]); 1169 1170(* Theorem: 0 < n ==> LOG2 n = 1 <=> (n = 2) \/ (n = 3) *) 1171(* Proof: 1172 If part: LOG2 n = 1 ==> n = 2 \/ n = 3 1173 Note 2 ** 1 <= n /\ n < 2 ** SUC 1 by LOG2_PROPERTY 1174 or 2 <= n /\ n < 4 by arithmetic 1175 Thus n = 2 or n = 3. 1176 Only-if part: LOG2 2 = 1 /\ LOG2 3 = 1 1177 Note LOG2 2 = 1 by LOG2_2 1178 and LOG2 3 = 1 by LOG2_UNIQUE 1179 since 2 ** 1 <= 3 /\ 3 < 2 ** SUC 1 ==> (LOG2 3 = 1) 1180*) 1181val LOG2_EQ_1 = store_thm( 1182 "LOG2_EQ_1", 1183 ``!n. 0 < n ==> ((LOG2 n = 1) <=> ((n = 2) \/ (n = 3)))``, 1184 rw_tac std_ss[EQ_IMP_THM] >| [ 1185 imp_res_tac LOG2_PROPERTY >> 1186 rfs[], 1187 rw[], 1188 irule LOG2_UNIQUE >> 1189 simp[] 1190 ]); 1191 1192(* Obtain theorem *) 1193val LOG2_LE_MONO = save_thm("LOG2_LE_MONO", 1194 LOG_LE_MONO |> SPEC ``2`` |> SPEC ``n:num`` |> SPEC ``m:num`` 1195 |> SIMP_RULE (srw_ss())[] |> GEN_ALL); 1196(* val LOG2_LE_MONO = |- !n m. 0 < n ==> n <= m ==> LOG2 n <= LOG2 m: thm *) 1197 1198(* Theorem: 0 < n /\ n <= m ==> LOG2 n <= LOG2 m *) 1199(* Proof: by LOG_LE_MONO *) 1200val LOG2_LE = store_thm( 1201 "LOG2_LE", 1202 ``!n m. 0 < n /\ n <= m ==> LOG2 n <= LOG2 m``, 1203 rw[LOG_LE_MONO, DECIDE``1 < 2``]); 1204 1205(* Note: next is not LOG2_LT_MONO! *) 1206 1207(* Theorem: 0 < n /\ n < m ==> LOG2 n <= LOG2 m *) 1208(* Proof: 1209 Since n < m ==> n <= m by LESS_IMP_LESS_OR_EQ 1210 This is true by LOG_LE_MONO 1211*) 1212val LOG2_LT = store_thm( 1213 "LOG2_LT", 1214 ``!n m. 0 < n /\ n < m ==> LOG2 n <= LOG2 m``, 1215 rw[LOG_LE_MONO, LESS_IMP_LESS_OR_EQ, DECIDE``1 < 2``]); 1216 1217(* Theorem: 0 < n ==> LOG2 n < n *) 1218(* Proof: 1219 LOG2 n 1220 < 2 ** (LOG2 n) by X_LT_EXP_X, 1 < 2 1221 <= n by LOG2_PROPERTY, 0 < n 1222*) 1223val LOG2_LT_SELF = store_thm( 1224 "LOG2_LT_SELF", 1225 ``!n. 0 < n ==> LOG2 n < n``, 1226 rpt strip_tac >> 1227 `LOG2 n < 2 ** (LOG2 n)` by rw[X_LT_EXP_X] >> 1228 `2 ** LOG2 n <= n` by rw[LOG2_PROPERTY] >> 1229 decide_tac); 1230 1231(* Theorem: 0 < n ==> LOG2 n <> n *) 1232(* Proof: 1233 Note n < LOG2 n by LOG2_LT_SELF 1234 Thus n <> LOG2 n by arithmetic 1235*) 1236val LOG2_NEQ_SELF = store_thm( 1237 "LOG2_NEQ_SELF", 1238 ``!n. 0 < n ==> LOG2 n <> n``, 1239 rpt strip_tac >> 1240 `LOG2 n < n` by rw[LOG2_LT_SELF] >> 1241 decide_tac); 1242 1243(* Theorem: LOG2 n = n ==> n = 0 *) 1244(* Proof: by LOG2_NEQ_SELF *) 1245val LOG2_EQ_SELF = store_thm( 1246 "LOG2_EQ_SELF", 1247 ``!n. (LOG2 n = n) ==> (n = 0)``, 1248 metis_tac[LOG2_NEQ_SELF, DECIDE``~(0 < n) <=> (n = 0)``]); 1249 1250(* Theorem: 1 < n ==> 0 < LOG2 n *) 1251(* Proof: 1252 1 < n 1253 ==> 2 <= n 1254 ==> LOG2 2 <= LOG2 n by LOG2_LE 1255 ==> 1 <= LOG2 n by LOG_BASE, LOG2 2 = 1 1256 or 0 < LOG2 n 1257*) 1258val LOG2_POS = store_thm( 1259 "LOG2_POS[simp]", 1260 ``!n. 1 < n ==> 0 < LOG2 n``, 1261 rpt strip_tac >> 1262 `LOG2 2 = 1` by rw[LOG_BASE, DECIDE``1 < 2``] >> 1263 `2 <= n` by decide_tac >> 1264 `LOG2 2 <= LOG2 n` by rw[LOG2_LE] >> 1265 decide_tac); 1266 1267(* Theorem: 1 < n ==> 1 < 2 * LOG2 n *) 1268(* Proof: 1269 1 < n 1270 ==> 2 <= n 1271 ==> LOG2 2 <= LOG2 n by LOG2_LE 1272 ==> 1 <= LOG2 n by LOG_BASE, LOG2 2 = 1 1273 ==> 2 * 1 <= 2 * LOG2 n by LE_MULT_LCANCEL 1274 or 1 < 2 * LOG2 n 1275*) 1276val LOG2_TWICE_LT = store_thm( 1277 "LOG2_TWICE_LT", 1278 ``!n. 1 < n ==> 1 < 2 * (LOG2 n)``, 1279 rpt strip_tac >> 1280 `LOG2 2 = 1` by rw[LOG_BASE, DECIDE``1 < 2``] >> 1281 `2 <= n` by decide_tac >> 1282 `LOG2 2 <= LOG2 n` by rw[LOG2_LE] >> 1283 `1 <= LOG2 n` by decide_tac >> 1284 `2 <= 2 * LOG2 n` by rw_tac arith_ss[LE_MULT_LCANCEL, DECIDE``0 < 2``] >> 1285 decide_tac); 1286 1287(* Theorem: 1 < n ==> 4 <= (2 * (LOG2 n)) ** 2 *) 1288(* Proof: 1289 1 < n 1290 ==> 2 <= n 1291 ==> LOG2 2 <= LOG2 n by LOG2_LE 1292 ==> 1 <= LOG2 n by LOG2_2, or LOG_BASE, LOG2 2 = 1 1293 ==> 2 * 1 <= 2 * LOG2 n by LE_MULT_LCANCEL 1294 ==> 2 ** 2 <= (2 * LOG2 n) ** 2 by EXP_EXP_LE_MONO 1295 ==> 4 <= (2 * LOG2 n) ** 2 1296*) 1297val LOG2_TWICE_SQ = store_thm( 1298 "LOG2_TWICE_SQ", 1299 ``!n. 1 < n ==> 4 <= (2 * (LOG2 n)) ** 2``, 1300 rpt strip_tac >> 1301 `LOG2 2 = 1` by rw[] >> 1302 `2 <= n` by decide_tac >> 1303 `LOG2 2 <= LOG2 n` by rw[LOG2_LE] >> 1304 `1 <= LOG2 n` by decide_tac >> 1305 `2 <= 2 * LOG2 n` by rw_tac arith_ss[LE_MULT_LCANCEL, DECIDE``0 < 2``] >> 1306 `2 ** 2 <= (2 * LOG2 n) ** 2` by rw[EXP_EXP_LE_MONO, DECIDE``0 < 2``] >> 1307 `2 ** 2 = 4` by rw_tac arith_ss[] >> 1308 decide_tac); 1309 1310(* Theorem: 0 < n ==> 4 <= (2 * SUC (LOG2 n)) ** 2 *) 1311(* Proof: 1312 0 < n 1313 ==> 1 <= n 1314 ==> LOG2 1 <= LOG2 n by LOG2_LE 1315 ==> 0 <= LOG2 n by LOG2_1, or LOG_BASE, LOG2 1 = 0 1316 ==> 1 <= SUC (LOG2 n) by LESS_EQ_MONO 1317 ==> 2 * 1 <= 2 * SUC (LOG2 n) by LE_MULT_LCANCEL 1318 ==> 2 ** 2 <= (2 * SUC (LOG2 n)) ** 2 by EXP_EXP_LE_MONO 1319 ==> 4 <= (2 * SUC (LOG2 n)) ** 2 1320*) 1321val LOG2_SUC_TWICE_SQ = store_thm( 1322 "LOG2_SUC_TWICE_SQ", 1323 ``!n. 0 < n ==> 4 <= (2 * SUC (LOG2 n)) ** 2``, 1324 rpt strip_tac >> 1325 `LOG2 1 = 0` by rw[] >> 1326 `1 <= n` by decide_tac >> 1327 `LOG2 1 <= LOG2 n` by rw[LOG2_LE] >> 1328 `1 <= SUC (LOG2 n)` by decide_tac >> 1329 `2 <= 2 * SUC (LOG2 n)` by rw_tac arith_ss[LE_MULT_LCANCEL, DECIDE``0 < 2``] >> 1330 `2 ** 2 <= (2 * SUC (LOG2 n)) ** 2` by rw[EXP_EXP_LE_MONO, DECIDE``0 < 2``] >> 1331 `2 ** 2 = 4` by rw_tac arith_ss[] >> 1332 decide_tac); 1333 1334(* Theorem: 1 < n ==> 1 < (SUC (LOG2 n)) ** 2 *) 1335(* Proof: 1336 Note 0 < LOG2 n by LOG2_POS, 1 < n 1337 so 1 < SUC (LOG2 n) by arithmetic 1338 ==> 1 < (SUC (LOG2 n)) ** 2 by ONE_LT_EXP, 0 < 2 1339*) 1340val LOG2_SUC_SQ = store_thm( 1341 "LOG2_SUC_SQ", 1342 ``!n. 1 < n ==> 1 < (SUC (LOG2 n)) ** 2``, 1343 rpt strip_tac >> 1344 `0 < LOG2 n` by rw[] >> 1345 `1 < SUC (LOG2 n)` by decide_tac >> 1346 rw[ONE_LT_EXP]); 1347 1348(* Theorem: 1 < m ==> 0 < SUC (LOG2 n) * (m ** 2 DIV 2) *) 1349(* Proof: 1350 Since 1 < m ==> 1 < m ** 2 DIV 2 by ONE_LT_HALF_SQ 1351 Hence 0 < m ** 2 DIV 2 1352 and 0 < 0 < SUC (LOG2 n) by prim_recTheory.LESS_0 1353 Therefore 0 < SUC (LOG2 n) * (m ** 2 DIV 2) by ZERO_LESS_MULT 1354*) 1355val LOG2_SUC_TIMES_SQ_DIV_2_POS = store_thm( 1356 "LOG2_SUC_TIMES_SQ_DIV_2_POS", 1357 ``!n m. 1 < m ==> 0 < SUC (LOG2 n) * (m ** 2 DIV 2)``, 1358 rpt strip_tac >> 1359 `1 < m ** 2 DIV 2` by rw[ONE_LT_HALF_SQ] >> 1360 `0 < m ** 2 DIV 2 /\ 0 < SUC (LOG2 n)` by decide_tac >> 1361 rw[ZERO_LESS_MULT]); 1362 1363(* Theorem: LOG2 (2 ** n) = n *) 1364(* Proof: by LOG_EXACT_EXP *) 1365val LOG2_2_EXP = store_thm( 1366 "LOG2_2_EXP", 1367 ``!n. LOG2 (2 ** n) = n``, 1368 rw[LOG_EXACT_EXP]); 1369 1370(* Theorem: (2 ** (LOG2 n) = n) <=> ?k. n = 2 ** k *) 1371(* Proof: 1372 If part: 2 ** LOG2 n = n ==> ?k. n = 2 ** k 1373 True by taking k = LOG2 n. 1374 Only-if part: 2 ** LOG2 (2 ** k) = 2 ** k 1375 Note LOG2 n = k by LOG_EXACT_EXP, 1 < 2 1376 or n = 2 ** k = 2 ** LOG2 n. 1377*) 1378val LOG2_EXACT_EXP = store_thm( 1379 "LOG2_EXACT_EXP", 1380 ``!n. (2 ** (LOG2 n) = n) <=> ?k. n = 2 ** k``, 1381 metis_tac[LOG2_2_EXP]); 1382 1383(* Theorem: 0 < n ==> LOG2 (n * 2 ** m) = (LOG2 n) + m *) 1384(* Proof: 1385 LOG_EXP |> SPEC ``m:num`` |> SPEC ``2`` |> SPEC ``n:num``; 1386 val it = |- 1 < 2 /\ 0 < n ==> LOG2 (2 ** m * n) = m + LOG2 n: thm 1387*) 1388val LOG2_MULT_EXP = store_thm( 1389 "LOG2_MULT_EXP", 1390 ``!n m. 0 < n ==> (LOG2 (n * 2 ** m) = (LOG2 n) + m)``, 1391 rw[GSYM LOG_EXP]); 1392 1393(* Theorem: 0 < n ==> (LOG2 (2 * n) = 1 + LOG2 n) *) 1394(* Proof: 1395 LOG_MULT |> SPEC ``2`` |> SPEC ``n:num``; 1396 val it = |- 1 < 2 /\ 0 < n ==> LOG2 (TWICE n) = SUC (LOG2 n): thm 1397*) 1398val LOG2_TWICE = store_thm( 1399 "LOG2_TWICE", 1400 ``!n. 0 < n ==> (LOG2 (2 * n) = 1 + LOG2 n)``, 1401 rw[LOG_MULT]); 1402 1403(* Theorem: 1 < n ==> LOG2 (HALF n) = (LOG2 n) - 1 *) 1404(* Proof: 1405 Note: > LOG_DIV |> SPEC ``2`` |> SPEC ``n:num``; 1406 val it = |- 1 < 2 /\ 2 <= n ==> LOG2 n = 1 + LOG2 (HALF n): thm 1407 Hence the result. 1408*) 1409val LOG2_HALF = store_thm( 1410 "LOG2_HALF", 1411 ``!n. 1 < n ==> (LOG2 (HALF n) = (LOG2 n) - 1)``, 1412 rpt strip_tac >> 1413 `LOG2 n = 1 + LOG2 (HALF n)` by rw[LOG_DIV] >> 1414 decide_tac); 1415 1416(* Theorem: 1 < n ==> (LOG2 n = 1 + LOG2 (HALF n)) *) 1417(* Proof: by LOG_DIV: 1418> LOG_DIV |> SPEC ``2``; 1419val it = |- !x. 1 < 2 /\ 2 <= x ==> (LOG2 x = 1 + LOG2 (HALF x)): thm 1420*) 1421val LOG2_BY_HALF = store_thm( 1422 "LOG2_BY_HALF", 1423 ``!n. 1 < n ==> (LOG2 n = 1 + LOG2 (HALF n))``, 1424 rw[LOG_DIV]); 1425 1426(* Theorem: 2 ** m < n ==> LOG2 (n DIV 2 ** m) = (LOG2 n) - m *) 1427(* Proof: 1428 By induction on m. 1429 Base: !n. 2 ** 0 < n ==> LOG2 (n DIV 2 ** 0) = LOG2 n - 0 1430 LOG2 (n DIV 2 ** 0) 1431 = LOG2 (n DIV 1) by EXP_0 1432 = LOG2 n by DIV_1 1433 = LOG2 n - 0 by SUB_0 1434 Step: !n. 2 ** m < n ==> LOG2 (n DIV 2 ** m) = LOG2 n - m ==> 1435 !n. 2 ** SUC m < n ==> LOG2 (n DIV 2 ** SUC m) = LOG2 n - SUC m 1436 Note 2 ** SUC m = 2 * 2 ** m by EXP, [1] 1437 Thus HALF (2 * 2 ** m) <= HALF n by DIV_LE_MONOTONE 1438 or 2 ** m <= HALF n by HALF_TWICE 1439 If 2 ** m < HALF n, 1440 LOG2 (n DIV 2 ** SUC m) 1441 = LOG2 (n DIV (2 * 2 ** m)) by [1] 1442 = LOG2 ((HALF n) DIV 2 ** m) by DIV_DIV_DIV_MULT 1443 = LOG2 (HALF n) - m by induction hypothesis, 2 ** m < HALF n 1444 = (LOG2 n - 1) - m by LOG2_HALF, 1 < n 1445 = LOG2 n - (1 + m) by arithmetic 1446 = LOG2 n - SUC m by ADD1 1447 Otherwise 2 ** m = HALF n, 1448 LOG2 (n DIV 2 ** SUC m) 1449 = LOG2 (n DIV (2 * 2 ** m)) by [1] 1450 = LOG2 ((HALF n) DIV 2 ** m) by DIV_DIV_DIV_MULT 1451 = LOG2 ((HALF n) DIV (HALF n)) by 2 ** m = HALF n 1452 = LOG2 1 by DIVMOD_ID, 0 < HALF n 1453 = 0 by LOG2_1 1454 LOG2 n 1455 = 1 + LOG2 (HALF n) by LOG_DIV 1456 = 1 + LOG2 (2 ** m) by 2 ** m = HALF n 1457 = 1 + m by LOG2_2_EXP 1458 = SUC m by SUC_ONE_ADD 1459 Thus RHS = LOG2 n - SUC m = 0 = LHS. 1460*) 1461 1462Theorem LOG2_DIV_EXP: 1463 !n m. 2 ** m < n ==> LOG2 (n DIV 2 ** m) = LOG2 n - m 1464Proof 1465 Induct_on ���m��� >- rw[] >> 1466 rpt strip_tac >> 1467 ���1 < 2 ** SUC m��� by rw[ONE_LT_EXP] >> 1468 ���1 < n��� by decide_tac >> 1469 fs[EXP] >> 1470 ���2 ** m <= HALF n��� 1471 by metis_tac[DIV_LE_MONOTONE, HALF_TWICE, LESS_IMP_LESS_OR_EQ, 1472 DECIDE ���0 < 2���] >> 1473 ���LOG2 (n DIV (TWICE (2 ** m))) = LOG2 ((HALF n) DIV 2 ** m)��� 1474 by rw[DIV_DIV_DIV_MULT] >> 1475 fs[LESS_OR_EQ] >- rw[LOG2_HALF] >> 1476 ���LOG2 n = 1 + LOG2 (HALF n)��� by rw[LOG_DIV] >> 1477 ���_ = 1 + m��� by metis_tac[LOG2_2_EXP] >> 1478 ���_ = SUC m��� by rw[] >> 1479 ���0 < HALF n��� suffices_by rw[] >> 1480 metis_tac[DECIDE ���0 < 2���, ZERO_LT_EXP] 1481QED 1482 1483(* ------------------------------------------------------------------------- *) 1484(* LOG2 Computation *) 1485(* ------------------------------------------------------------------------- *) 1486 1487(* Define halves n = count of HALFs of n to 0, recursively. *) 1488val halves_def = Define` 1489 halves n = if n = 0 then 0 else SUC (halves (HALF n)) 1490`; 1491 1492(* Theorem: halves n = if n = 0 then 0 else 1 + (halves (HALF n)) *) 1493(* Proof: by halves_def, ADD1 *) 1494val halves_alt = store_thm( 1495 "halves_alt", 1496 ``!n. halves n = if n = 0 then 0 else 1 + (halves (HALF n))``, 1497 rw[Once halves_def, ADD1]); 1498 1499(* Extract theorems from definition *) 1500val halves_0 = save_thm("halves_0[simp]", halves_def |> SPEC ``0`` |> SIMP_RULE arith_ss[]); 1501(* val halves_0 = |- halves 0 = 0: thm *) 1502val halves_1 = save_thm("halves_1[simp]", halves_def |> SPEC ``1`` |> SIMP_RULE arith_ss[]); 1503(* val halves_1 = |- halves 1 = 1: thm *) 1504val halves_2 = save_thm("halves_2[simp]", halves_def |> SPEC ``2`` |> SIMP_RULE arith_ss[halves_1]); 1505(* val halves_2 = |- halves 2 = 2: thm *) 1506 1507(* Theorem: 0 < n ==> 0 < halves n *) 1508(* Proof: by halves_def *) 1509val halves_pos = store_thm( 1510 "halves_pos[simp]", 1511 ``!n. 0 < n ==> 0 < halves n``, 1512 rw[Once halves_def]); 1513 1514(* Theorem: 0 < n ==> (halves n = 1 + LOG2 n) *) 1515(* Proof: 1516 By complete induction on n. 1517 Assume: !m. m < n ==> 0 < m ==> (halves m = 1 + LOG2 m) 1518 To show: 0 < n ==> (halves n = 1 + LOG2 n) 1519 Note HALF n < n by HALF_LESS, 0 < n 1520 Need 0 < HALF n to apply induction hypothesis. 1521 If HALF n = 0, 1522 Then n = 1 by HALF_EQ_0 1523 halves 1 1524 = SUC (halves 0) by halves_def 1525 = 1 by halves_def 1526 = 1 + LOG2 1 by LOG2_1 1527 If HALF n <> 0, 1528 Then n <> 1 by HALF_EQ_0 1529 so 1 < n by n <> 0, n <> 1. 1530 halves n 1531 = SUC (halves (HALF n)) by halves_def 1532 = SUC (1 + LOG2 (HALF n)) by induction hypothesis 1533 = SUC (LOG2 n) by LOG2_BY_HALF 1534 = 1 + LOG2 n by ADD1 1535*) 1536val halves_by_LOG2 = store_thm( 1537 "halves_by_LOG2", 1538 ``!n. 0 < n ==> (halves n = 1 + LOG2 n)``, 1539 completeInduct_on `n` >> 1540 strip_tac >> 1541 rw[Once halves_def] >> 1542 Cases_on `n = 1` >- 1543 simp[Once halves_def] >> 1544 `HALF n < n` by rw[HALF_LESS] >> 1545 `HALF n <> 0` by fs[HALF_EQ_0] >> 1546 simp[LOG2_BY_HALF]); 1547 1548(* Theorem: LOG2 n = if n = 0 then LOG2 0 else (halves n - 1) *) 1549(* Proof: 1550 If 0 < n, 1551 Note 0 < halves n by halves_pos 1552 and halves n = 1 + LOG2 n by halves_by_LOG2 1553 or LOG2 n = halves - 1. 1554 If n = 0, make it an infinite loop. 1555*) 1556val LOG2_compute = store_thm( 1557 "LOG2_compute[compute]", 1558 ``!n. LOG2 n = if n = 0 then LOG2 0 else (halves n - 1)``, 1559 rpt strip_tac >> 1560 (Cases_on `n = 0` >> simp[]) >> 1561 `0 < halves n` by rw[] >> 1562 `halves n = 1 + LOG2 n` by rw[halves_by_LOG2] >> 1563 decide_tac); 1564 1565(* Put this to computeLib *) 1566(* val _ = computeLib.add_persistent_funs ["LOG2_compute"]; *) 1567 1568(* 1569EVAL ``LOG2 16``; --> 4 1570EVAL ``LOG2 17``; --> 4 1571EVAL ``LOG2 32``; --> 5 1572EVAL ``LOG2 1024``; --> 10 1573EVAL ``LOG2 1023``; --> 9 1574*) 1575 1576(* Michael's method *) 1577(* 1578Define `count_divs n = if 2 <= n then 1 + count_divs (n DIV 2) else 0`; 1579 1580g `0 < n ==> (LOG2 n = count_divs n)`; 1581e (completeInduct_on `n`); 1582e strip_tac; 1583e (ONCE_REWRITE_TAC [theorm "count_divs_def"]); 1584e (Cases_on `2 <= n`); 1585e (mp_tac (Q.SPECL [`2`, `n`] LOG_DIV)); 1586e (simp[]); 1587(* prove on-the-fly *) 1588e (`0 < n DIV 2` suffices_by simp[]); 1589(* DB.match [] ``x < k DIV n``; *) 1590e (simp[arithmeticTheory.X_LT_DIV]); 1591e (`n = 1` by simp[]); 1592LOG_1; 1593e (simp[it]); 1594val foo = top_thm(); 1595 1596g `!n. LOG2 n = if 0 < n then count_divs n else LOG2 n`; 1597 1598e (rw[]); 1599e (simp[foo]); 1600e (lfs[]); ??? 1601 1602val bar = top_thm(); 1603var bar = save_thm("bar", bar); 1604computeLib.add_persistent_funs ["bar"]; 1605EVAL ``LOG2 16``; 1606EVAL ``LOG2 17``; 1607EVAL ``LOG2 32``; 1608EVAL ``LOG2 1024``; 1609EVAL ``LOG2 1023``; 1610EVAL ``LOG2 0``; -- loops! 1611 1612So for n = 97, 1613EVAL ``LOG2 97``; --> 6 1614EVAL ``4 * LOG2 97 * LOG2 97``; --> 4 * 6 * 6 = 4 * 36 = 144 1615 1616Need ord_r (97) > 144, r < 97, not possible ??? 1617 1618val count_divs_def = Define `count_divs n = if 1 < n then 1 + count_divs (n DIV 2) else 0`; 1619 1620val LOG2_by_count_divs = store_thm( 1621 "LOG2_by_count_divs", 1622 ``!n. 0 < n ==> (LOG2 n = count_divs n)``, 1623 completeInduct_on `n` >> 1624 strip_tac >> 1625 ONCE_REWRITE_TAC[count_divs_def] >> 1626 rw[] >| [ 1627 mp_tac (Q.SPECL [`2`, `n`] LOG_DIV) >> 1628 `2 <= n` by decide_tac >> 1629 `0 < n DIV 2` by rw[X_LT_DIV] >> 1630 simp[], 1631 `n = 1` by decide_tac >> 1632 simp[LOG_1] 1633 ]); 1634 1635val LOG2_compute = store_thm( 1636 "LOG2_compute[compute]", 1637 ``!n. LOG2 n = if 0 < n then count_divs n else LOG2 n``, 1638 rw_tac std_ss[LOG2_by_count_divs]); 1639 1640*) 1641 1642(* Theorem: m <= n ==> halves m <= halves n *) 1643(* Proof: 1644 If m = 0, 1645 Then halves m = 0 by halves_0 1646 Thus halves m <= halves n by 0 <= halves n 1647 If m <> 0, 1648 Then 0 < m and 0 < n by m <= n 1649 so halves m = 1 + LOG2 m by halves_by_LOG2 1650 and halves n = 1 + LOG2 n by halves_by_LOG2 1651 and LOG2 m <= LOG2 n by LOG2_LE 1652 ==> halves m <= halves n by arithmetic 1653*) 1654val halves_le = store_thm( 1655 "halves_le", 1656 ``!m n. m <= n ==> halves m <= halves n``, 1657 rpt strip_tac >> 1658 Cases_on `m = 0` >- 1659 rw[] >> 1660 `0 < m /\ 0 < n` by decide_tac >> 1661 `LOG2 m <= LOG2 n` by rw[LOG2_LE] >> 1662 rw[halves_by_LOG2]); 1663 1664(* Theorem: (halves n = 0) <=> (n = 0) *) 1665(* Proof: by halves_pos, halves_0 *) 1666val halves_eq_0 = store_thm( 1667 "halves_eq_0", 1668 ``!n. (halves n = 0) <=> (n = 0)``, 1669 metis_tac[halves_pos, halves_0, NOT_ZERO_LT_ZERO]); 1670 1671(* Theorem: (halves n = 1) <=> (n = 1) *) 1672(* Proof: 1673 If part: halves n = 1 ==> n = 1 1674 By contradiction, assume n <> 1. 1675 Note n <> 0 by halves_eq_0 1676 so 2 <= n by n <> 0, n <> 1 1677 or halves 2 <= halves n by halves_le 1678 But halves 2 = 2 by halves_2 1679 This gives 2 <= 1, a contradiction. 1680 Only-if part: halves 1 = 1, true by halves_1 1681*) 1682val halves_eq_1 = store_thm( 1683 "halves_eq_1", 1684 ``!n. (halves n = 1) <=> (n = 1)``, 1685 rw[EQ_IMP_THM] >> 1686 spose_not_then strip_assume_tac >> 1687 `n <> 0` by metis_tac[halves_eq_0, DECIDE``1 <> 0``] >> 1688 `2 <= n` by decide_tac >> 1689 `halves 2 <= halves n` by rw[halves_le] >> 1690 fs[]); 1691 1692(* ------------------------------------------------------------------------- *) 1693(* Perfect Power *) 1694(* ------------------------------------------------------------------------- *) 1695 1696(* Define a PerfectPower number *) 1697val perfect_power_def = Define` 1698 perfect_power (n:num) (m:num) <=> ?e. (n = m ** e) 1699`; 1700 1701(* Overload perfect_power *) 1702val _ = overload_on("power_of", ``perfect_power``); 1703val _ = set_fixity "power_of" (Infix(NONASSOC, 450)); (* same as relation *) 1704(* from pretty-printing, a good idea. *) 1705 1706(* Theorem: perfect_power n n *) 1707(* Proof: 1708 True since n = n ** 1 by EXP_1 1709*) 1710val perfect_power_self = store_thm( 1711 "perfect_power_self", 1712 ``!n. perfect_power n n``, 1713 metis_tac[perfect_power_def, EXP_1]); 1714 1715(* Theorem: perfect_power 0 m <=> (m = 0) *) 1716(* Proof: by perfect_power_def, EXP_EQ_0 *) 1717val perfect_power_0_m = store_thm( 1718 "perfect_power_0_m", 1719 ``!m. perfect_power 0 m <=> (m = 0)``, 1720 rw[perfect_power_def, EQ_IMP_THM]); 1721 1722(* Theorem: perfect_power 1 m *) 1723(* Proof: by perfect_power_def, take e = 0 *) 1724val perfect_power_1_m = store_thm( 1725 "perfect_power_1_m", 1726 ``!m. perfect_power 1 m``, 1727 rw[perfect_power_def] >> 1728 metis_tac[]); 1729 1730(* Theorem: perfect_power n 0 <=> ((n = 0) \/ (n = 1)) *) 1731(* Proof: by perfect_power_def, ZERO_EXP. *) 1732val perfect_power_n_0 = store_thm( 1733 "perfect_power_n_0", 1734 ``!n. perfect_power n 0 <=> ((n = 0) \/ (n = 1))``, 1735 rw[perfect_power_def] >> 1736 metis_tac[ZERO_EXP]); 1737 1738(* Theorem: perfect_power n 1 <=> (n = 1) *) 1739(* Proof: by perfect_power_def, EXP_1 *) 1740val perfect_power_n_1 = store_thm( 1741 "perfect_power_n_1", 1742 ``!n. perfect_power n 1 <=> (n = 1)``, 1743 rw[perfect_power_def]); 1744 1745(* Theorem: 0 < m /\ 1 < n /\ (n MOD m = 0) ==> 1746 (perfect_power n m) <=> (perfect_power (n DIV m) m) *) 1747(* Proof: 1748 If part: perfect_power n m ==> perfect_power (n DIV m) m 1749 Note ?e. n = m ** e by perfect_power_def 1750 and e <> 0 by EXP_0, n <> 1 1751 so ?k. e = SUC k by num_CASES 1752 or n = m ** SUC k 1753 ==> n DIV m = m ** k by EXP_SUC_DIV 1754 Thus perfect_power (n DIV m) m by perfect_power_def 1755 Only-if part: perfect_power (n DIV m) m ==> perfect_power n m 1756 Note ?e. n DIV m = m ** e by perfect_power_def 1757 Now m divides n by DIVIDES_MOD_0, n MOD m = 0, 0 < m 1758 ==> n = m * (n DIV m) by DIVIDES_EQN_COMM, 0 < m 1759 = m * m ** e by above 1760 = m ** (SUC e) by EXP 1761 Thus perfect_power n m by perfect_power_def 1762*) 1763val perfect_power_mod_eq_0 = store_thm( 1764 "perfect_power_mod_eq_0", 1765 ``!n m. 0 < m /\ 1 < n /\ (n MOD m = 0) ==> 1766 ((perfect_power n m) <=> (perfect_power (n DIV m) m))``, 1767 rw[perfect_power_def] >> 1768 rw[EQ_IMP_THM] >| [ 1769 `m ** e <> 1` by decide_tac >> 1770 `e <> 0` by metis_tac[EXP_0] >> 1771 `?k. e = SUC k` by metis_tac[num_CASES] >> 1772 qexists_tac `k` >> 1773 rw[EXP_SUC_DIV], 1774 `m divides n` by rw[DIVIDES_MOD_0] >> 1775 `n = m * (n DIV m)` by rw[GSYM DIVIDES_EQN_COMM] >> 1776 metis_tac[EXP] 1777 ]); 1778 1779(* Theorem: 0 < m /\ 1 < n /\ (n MOD m <> 0) ==> ~(perfect_power n m) *) 1780(* Proof: 1781 By contradiction, assume perfect_power n m. 1782 Then ?e. n = m ** e by perfect_power_def 1783 Now e <> 0 by EXP_0, n <> 1 1784 so ?k. e = SUC k by num_CASES 1785 n = m ** SUC k 1786 = m * (m ** k) by EXP 1787 = (m ** k) * m by MULT_COMM 1788 Thus m divides n by divides_def 1789 ==> n MOD m = 0 by DIVIDES_MOD_0 1790 This contradicts n MOD m <> 0. 1791*) 1792val perfect_power_mod_ne_0 = store_thm( 1793 "perfect_power_mod_ne_0", 1794 ``!n m. 0 < m /\ 1 < n /\ (n MOD m <> 0) ==> ~(perfect_power n m)``, 1795 rpt strip_tac >> 1796 fs[perfect_power_def] >> 1797 `n <> 1` by decide_tac >> 1798 `e <> 0` by metis_tac[EXP_0] >> 1799 `?k. e = SUC k` by metis_tac[num_CASES] >> 1800 `n = m * m ** k` by fs[EXP] >> 1801 `m divides n` by metis_tac[divides_def, MULT_COMM] >> 1802 metis_tac[DIVIDES_MOD_0]); 1803 1804(* Theorem: perfect_power n m = 1805 if n = 0 then (m = 0) 1806 else if n = 1 then T 1807 else if m = 0 then (n <= 1) 1808 else if m = 1 then (n = 1) 1809 else if n MOD m = 0 then perfect_power (n DIV m) m else F *) 1810(* Proof: 1811 If n = 0, to show: 1812 perfect_power 0 m <=> (m = 0), true by perfect_power_0_m 1813 If n = 1, to show: 1814 perfect_power 1 m = T, true by perfect_power_1_m 1815 If m = 0, to show: 1816 perfect_power n 0 <=> (n <= 1), true by perfect_power_n_0 1817 If m = 1, to show: 1818 perfect_power n 1 <=> (n = 1), true by perfect_power_n_1 1819 Otherwise, 1820 If n MOD m = 0, to show: 1821 perfect_power (n DIV m) m <=> perfect_power n m, true 1822 by perfect_power_mod_eq_0 1823 If n MOD m <> 0, to show: 1824 ~perfect_power n m, true by perfect_power_mod_ne_0 1825*) 1826val perfect_power_test = store_thm( 1827 "perfect_power_test", 1828 ``!n m. perfect_power n m = 1829 if n = 0 then (m = 0) 1830 else if n = 1 then T 1831 else if m = 0 then (n <= 1) 1832 else if m = 1 then (n = 1) 1833 else if n MOD m = 0 then perfect_power (n DIV m) m else F``, 1834 rpt strip_tac >> 1835 (Cases_on `n = 0` >> simp[perfect_power_0_m]) >> 1836 (Cases_on `n = 1` >> simp[perfect_power_1_m]) >> 1837 `1 < n` by decide_tac >> 1838 (Cases_on `m = 0` >> simp[perfect_power_n_0]) >> 1839 `0 < m` by decide_tac >> 1840 (Cases_on `m = 1` >> simp[perfect_power_n_1]) >> 1841 (Cases_on `n MOD m = 0` >> simp[]) >- 1842 rw[perfect_power_mod_eq_0] >> 1843 rw[perfect_power_mod_ne_0]); 1844 1845(* Theorem: 1 < m /\ perfect_power n m /\ perfect_power (SUC n) m ==> (m = 2) /\ (n = 1) *) 1846(* Proof: 1847 Note ?x. n = m ** x by perfect_power_def 1848 and ?y. SUC n = m ** y by perfect_power_def 1849 Since n < SUC n by LESS_SUC 1850 ==> x < y by EXP_BASE_LT_MONO 1851 Let d = y - x. 1852 Then 0 < d /\ (y = x + d). 1853 Let v = m ** d 1854 Note 1 < v by ONE_LT_EXP, 1 < m 1855 and m ** y = n * v by EXP_ADD 1856 Let z = v - 1. 1857 Then 0 < z /\ (v = z + 1). 1858 and SUC n = n * v 1859 = n * (z + 1) 1860 = n * z + n * 1 by LEFT_ADD_DISTRIB 1861 = n * z + n 1862 ==> n * z = 1 by ADD1 1863 ==> n = 1 /\ z = 1 by MULT_EQ_1 1864 so v = 2 by v = z + 1 1865 1866 To show: m = 2. 1867 By contradiction, suppose m <> 2. 1868 Then 2 < m by 1 < m, m <> 2 1869 ==> 2 ** y < m ** y by EXP_EXP_LT_MONO 1870 = n * v = 2 = 2 ** 1 by EXP_1 1871 ==> y < 1 by EXP_BASE_LT_MONO 1872 Thus y = 0, but y <> 0 by x < y, 1873 leading to a contradiction. 1874*) 1875 1876Theorem perfect_power_suc: 1877 !m n. 1 < m /\ perfect_power n m /\ perfect_power (SUC n) m ==> 1878 m = 2 /\ n = 1 1879Proof 1880 ntac 3 strip_tac >> 1881 `?x. n = m ** x` by fs[perfect_power_def] >> 1882 `?y. SUC n = m ** y` by fs[GSYM perfect_power_def] >> 1883 `n < SUC n` by decide_tac >> 1884 `x < y` by metis_tac[EXP_BASE_LT_MONO] >> 1885 qabbrev_tac `d = y - x` >> 1886 `0 < d /\ (y = x + d)` by fs[Abbr`d`] >> 1887 qabbrev_tac `v = m ** d` >> 1888 `m ** y = n * v` by fs[EXP_ADD, Abbr`v`] >> 1889 `1 < v` by rw[ONE_LT_EXP, Abbr`v`] >> 1890 qabbrev_tac `z = v - 1` >> 1891 `0 < z /\ (v = z + 1)` by fs[Abbr`z`] >> 1892 `n * v = n * z + n * 1` by rw[] >> 1893 `n * z = 1` by decide_tac >> 1894 `n = 1 /\ z = 1` by metis_tac[MULT_EQ_1] >> 1895 `v = 2` by decide_tac >> 1896 simp[] >> 1897 spose_not_then strip_assume_tac >> 1898 `2 < m` by decide_tac >> 1899 `2 ** y < m ** y` by simp[EXP_EXP_LT_MONO] >> 1900 `m ** y = 2` by decide_tac >> 1901 `2 ** y < 2 ** 1` by metis_tac[EXP_1] >> 1902 `y < 1` by fs[EXP_BASE_LT_MONO] >> 1903 decide_tac 1904QED 1905 1906(* Theorem: 1 < m /\ 1 < n /\ perfect_power n m ==> ~perfect_power (SUC n) m *) 1907(* Proof: 1908 By contradiction, suppose perfect_power (SUC n) m. 1909 Then n = 1 by perfect_power_suc 1910 This contradicts 1 < n. 1911*) 1912val perfect_power_not_suc = store_thm( 1913 "perfect_power_not_suc", 1914 ``!m n. 1 < m /\ 1 < n /\ perfect_power n m ==> ~perfect_power (SUC n) m``, 1915 spose_not_then strip_assume_tac >> 1916 `n = 1` by metis_tac[perfect_power_suc] >> 1917 decide_tac); 1918 1919(* Theorem: 1 < b /\ 0 < n ==> 1920 (LOG b (SUC n) = LOG b n + if perfect_power (SUC n) b then 1 else 0) *) 1921(* Proof: 1922 Let x = LOG b n, y = LOG b (SUC n). x <= y 1923 Note SUC n <= b ** SUC x /\ b ** SUC x <= b * n by LOG_TEST 1924 and SUC (SUC n) <= b ** SUC y /\ b ** SUC y <= b * SUC n by LOG_TEST, 0 < SUC n 1925 1926 If SUC n = b ** SUC x, 1927 Then perfect_power (SUC n) b by perfect_power_def 1928 and y = LOG b (SUC n) 1929 = LOG b (b ** SUC x) 1930 = SUC x by LOG_EXACT_EXP 1931 = x + 1 by ADD1 1932 hence true. 1933 Otherwise, SUC n < b ** SUC x, 1934 Then SUC (SUC n) <= b ** SUC x by SUC n < b ** SUC x 1935 and b * n < b * SUC n by LT_MULT_LCANCEL, n < SUC n 1936 Thus b ** SUC x <= b * n < b * SUC n 1937 or y = x by LOG_TEST 1938 Claim: ~perfect_power (SUC n) b 1939 Proof: By contradiction, suppose perfect_power (SUC n) b. 1940 Then ?e. SUC n = b ** e. 1941 Thus y = LOG b (SUC n) 1942 = LOG b (b ** e) by LOG_EXACT_EXP 1943 = e 1944 ==> b * n < b * SUC n 1945 = b * b ** e by SUC n = b ** e 1946 = b ** SUC e by EXP 1947 = b ** SUC x by e = y = x 1948 This contradicts b ** SUC x <= b * n 1949 With ~perfect_power (SUC n) b, hence true. 1950*) 1951 1952Theorem LOG_SUC: 1953 !b n. 1 < b /\ 0 < n ==> 1954 (LOG b (SUC n) = LOG b n + if perfect_power (SUC n) b then 1 else 0) 1955Proof 1956 rpt strip_tac >> 1957 qabbrev_tac ���x = LOG b n��� >> 1958 qabbrev_tac ���y = LOG b (SUC n)��� >> 1959 ���0 < SUC n��� by decide_tac >> 1960 ���SUC n <= b ** SUC x /\ b ** SUC x <= b * n��� by metis_tac[LOG_TEST] >> 1961 ���SUC (SUC n) <= b ** SUC y /\ b ** SUC y <= b * SUC n��� 1962 by metis_tac[LOG_TEST] >> 1963 ���(SUC n = b ** SUC x) \/ (SUC n < b ** SUC x)��� by decide_tac >| [ 1964 ���perfect_power (SUC n) b��� by metis_tac[perfect_power_def] >> 1965 ���y = SUC x��� by rw[LOG_EXACT_EXP, Abbr���y���] >> 1966 simp[], 1967 ���SUC (SUC n) <= b ** SUC x��� by decide_tac >> 1968 ���b * n < b * SUC n��� by rw[] >> 1969 ���b ** SUC x <= b * SUC n��� by decide_tac >> 1970 ���y = x��� by metis_tac[LOG_TEST] >> 1971 ���~perfect_power (SUC n) b��� 1972 by (spose_not_then strip_assume_tac >> 1973 `?e. SUC n = b ** e` by fs[perfect_power_def] >> 1974 `y = e` by (simp[Abbr`y`] >> fs[] >> rfs[LOG_EXACT_EXP]) >> 1975 `b * n < b ** SUC x` by metis_tac[EXP] >> 1976 decide_tac) >> 1977 simp[] 1978 ] 1979QED 1980 1981(* 1982LOG_SUC; 1983|- !b n. 1 < b /\ 0 < n ==> LOG b (SUC n) = LOG b n + if perfect_power (SUC n) b then 1 else 0 1984Let v = LOG b n. 1985 1986 v v+1. v+2. v+3. 1987 ----------------------------------------------- 1988 b b ** 2 b ** 3 b ** 4 1989 1990> EVAL ``MAP (LOG 2) [1 .. 20]``; 1991val it = |- MAP (LOG 2) [1 .. 20] = 1992 [0; 1; 1; 2; 2; 2; 2; 3; 3; 3; 3; 3; 3; 3; 3; 4; 4; 4; 4; 4]: thm 1993 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 1994*) 1995 1996(* Theorem: 0 < n ==> !m. perfect_power n m <=> ?k. k <= LOG2 n /\ (n = m ** k) *) 1997(* Proof: 1998 If part: perfect_power n m ==> ?k. k <= LOG2 n /\ (n = m ** k) 1999 Given perfect_power n m, ?e. (n = m ** e) by perfect_power_def 2000 If n = 1, 2001 Then LOG2 1 = 0 by LOG2_1 2002 Take k = 0, then 1 = m ** 0 by EXP_0 2003 If n <> 1, so e <> 0 by EXP 2004 and m <> 1 by EXP_1 2005 also n <> 0, so m <> 0 by ZERO_EXP 2006 Therefore 2 <= m 2007 ==> 2 ** e <= m ** e by EXP_BASE_LE_MONO, 1 < 2 2008 But n < 2 ** (SUC (LOG2 n)) by LOG2_PROPERTY, 0 < n 2009 or 2 ** e < 2 ** (SUC (LOG2 n)) 2010 hence e < SUC (LOG2 n) by EXP_BASE_LT_MONO, 1 < 2 2011 i.e. e <= LOG2 n 2012 Only-if part: ?k. k <= LOG2 n /\ (n = m ** k) ==> perfect_power n m 2013 True by perfect_power_def. 2014*) 2015val perfect_power_bound_LOG2 = store_thm( 2016 "perfect_power_bound_LOG2", 2017 ``!n. 0 < n ==> !m. perfect_power n m <=> ?k. k <= LOG2 n /\ (n = m ** k)``, 2018 rw[EQ_IMP_THM] >| [ 2019 Cases_on `n = 1` >- 2020 simp[] >> 2021 `?e. (n = m ** e)` by rw[GSYM perfect_power_def] >> 2022 `n <> 0 /\ 1 < n /\ 1 < 2` by decide_tac >> 2023 `e <> 0` by metis_tac[EXP] >> 2024 `m <> 1` by metis_tac[EXP_1] >> 2025 `m <> 0` by metis_tac[ZERO_EXP] >> 2026 `2 <= m` by decide_tac >> 2027 `2 ** e <= n` by rw[EXP_BASE_LE_MONO] >> 2028 `n < 2 ** (SUC (LOG2 n))` by rw[LOG2_PROPERTY] >> 2029 `e < SUC (LOG2 n)` by metis_tac[EXP_BASE_LT_MONO, LESS_EQ_LESS_TRANS] >> 2030 `e <= LOG2 n` by decide_tac >> 2031 metis_tac[], 2032 metis_tac[perfect_power_def] 2033 ]); 2034 2035(* Theorem: prime p /\ (?x y. 0 < x /\ (p ** x = q ** y)) ==> perfect_power q p *) 2036(* Proof: 2037 Note ?k. (q = p ** k) by power_eq_prime_power, prime p, 0 < x 2038 Thus perfect_power q p by perfect_power_def 2039*) 2040val perfect_power_condition = store_thm( 2041 "perfect_power_condition", 2042 ``!p q. prime p /\ (?x y. 0 < x /\ (p ** x = q ** y)) ==> perfect_power q p``, 2043 metis_tac[power_eq_prime_power, perfect_power_def]); 2044 2045(* Theorem: 0 < p /\ p divides n ==> (perfect_power n p <=> perfect_power (n DIV p) p) *) 2046(* Proof: 2047 Let q = n DIV p. 2048 Then n = p * q by DIVIDES_EQN_COMM, 0 < p 2049 If part: perfect_power n p ==> perfect_power q p 2050 Note ?k. n = p ** k by perfect_power_def 2051 If k = 0, 2052 Then p * q = p ** 0 = 1 by EXP 2053 ==> p = 1 and q = 1 by MULT_EQ_1 2054 so perfect_power q p by perfect_power_self 2055 If k <> 0, k = SUC h for some h. 2056 Then p * q = p ** SUC h 2057 = p * p ** h by EXP 2058 or q = p ** h by MULT_LEFT_CANCEL, p <> 0 2059 so perfect_power q p by perfect_power_self 2060 2061 Only-if part: perfect_power q p ==> perfect_power n p 2062 Note ?k. q = p ** k by perfect_power_def 2063 so n = p * q = p ** SUC k by EXP 2064 thus perfect_power n p by perfect_power_def 2065*) 2066val perfect_power_cofactor = store_thm( 2067 "perfect_power_cofactor", 2068 ``!n p. 0 < p /\ p divides n ==> (perfect_power n p <=> perfect_power (n DIV p) p)``, 2069 rpt strip_tac >> 2070 qabbrev_tac `q = n DIV p` >> 2071 `n = p * q` by rw[GSYM DIVIDES_EQN_COMM, Abbr`q`] >> 2072 simp[EQ_IMP_THM] >> 2073 rpt strip_tac >| [ 2074 `?k. p * q = p ** k` by rw[GSYM perfect_power_def] >> 2075 Cases_on `k` >| [ 2076 `(p = 1) /\ (q = 1)` by metis_tac[MULT_EQ_1, EXP] >> 2077 metis_tac[perfect_power_self], 2078 `q = p ** n'` by metis_tac[EXP, MULT_LEFT_CANCEL, NOT_ZERO_LT_ZERO] >> 2079 metis_tac[perfect_power_def] 2080 ], 2081 `?k. q = p ** k` by rw[GSYM perfect_power_def] >> 2082 `p * q = p ** SUC k` by rw[EXP] >> 2083 metis_tac[perfect_power_def] 2084 ]); 2085 2086(* Theorem: 0 < n /\ p divides n ==> (perfect_power n p <=> perfect_power (n DIV p) p) *) 2087(* Proof: 2088 Note 0 < p by ZERO_DIVIDES, 0 < n 2089 The result follows by perfect_power_cofactor 2090*) 2091val perfect_power_cofactor_alt = store_thm( 2092 "perfect_power_cofactor_alt", 2093 ``!n p. 0 < n /\ p divides n ==> (perfect_power n p <=> perfect_power (n DIV p) p)``, 2094 rpt strip_tac >> 2095 `0 < p` by metis_tac[ZERO_DIVIDES, NOT_ZERO] >> 2096 qabbrev_tac `q = n DIV p` >> 2097 rw[perfect_power_cofactor]); 2098 2099(* Theorem: perfect_power n 2 ==> (ODD n <=> (n = 1)) *) 2100(* Proof: 2101 If part: perfect_power n 2 /\ ODD n ==> n = 1 2102 By contradiction, suppose n <> 1. 2103 Note ?k. n = 2 ** k by perfect_power_def 2104 Thus k <> 0 by EXP 2105 so ?h. k = SUC h by num_CASES 2106 n = 2 ** (SUC h) by above 2107 = 2 * 2 ** h by EXP 2108 ==> EVEN n by EVEN_DOUBLE 2109 This contradicts ODD n by EVEN_ODD 2110 Only-if part: perfect_power n 2 /\ n = 1 ==> ODD n 2111 This is true by ODD_1 2112*) 2113val perfect_power_2_odd = store_thm( 2114 "perfect_power_2_odd", 2115 ``!n. perfect_power n 2 ==> (ODD n <=> (n = 1))``, 2116 rw[EQ_IMP_THM] >> 2117 spose_not_then strip_assume_tac >> 2118 `?k. n = 2 ** k` by rw[GSYM perfect_power_def] >> 2119 `k <> 0` by metis_tac[EXP] >> 2120 `?h. k = SUC h` by metis_tac[num_CASES] >> 2121 `n = 2 * 2 ** h` by rw[EXP] >> 2122 metis_tac[EVEN_DOUBLE, EVEN_ODD]); 2123 2124(* ------------------------------------------------------------------------- *) 2125(* Power Free *) 2126(* ------------------------------------------------------------------------- *) 2127 2128(* Define a PowerFree number: a trivial perfect power *) 2129val power_free_def = zDefine` 2130 power_free (n:num) <=> !m e. (n = m ** e) ==> (m = n) /\ (e = 1) 2131`; 2132(* Use zDefine as this is not computationally effective. *) 2133 2134(* Theorem: power_free 0 = F *) 2135(* Proof: 2136 Note 0 ** 2 = 0 by ZERO_EXP 2137 Thus power_free 0 = F by power_free_def 2138*) 2139val power_free_0 = store_thm( 2140 "power_free_0", 2141 ``power_free 0 = F``, 2142 rw[power_free_def]); 2143 2144(* Theorem: power_free 1 = F *) 2145(* Proof: 2146 Note 0 ** 0 = 1 by ZERO_EXP 2147 Thus power_free 1 = F by power_free_def 2148*) 2149val power_free_1 = store_thm( 2150 "power_free_1", 2151 ``power_free 1 = F``, 2152 rw[power_free_def]); 2153 2154(* Theorem: power_free n ==> 1 < n *) 2155(* Proof: 2156 By contradiction, suppose n = 0 or n = 1. 2157 Then power_free 0 = F by power_free_0 2158 and power_free 1 = F by power_free_1 2159*) 2160val power_free_gt_1 = store_thm( 2161 "power_free_gt_1", 2162 ``!n. power_free n ==> 1 < n``, 2163 metis_tac[power_free_0, power_free_1, DECIDE``1 < n <=> (n <> 0 /\ n <> 1)``]); 2164 2165(* Theorem: power_free n <=> 1 < n /\ (!m. perfect_power n m ==> (n = m)) *) 2166(* Proof: 2167 If part: power_free n ==> 1 < n /\ (!m. perfect_power n m ==> (n = m)) 2168 Note power_free n 2169 ==> 1 < n by power_free_gt_1 2170 Now ?e. n = m ** e by perfect_power_def 2171 ==> n = m by power_free_def 2172 2173 Only-if part: 1 < n /\ (!m. perfect_power n m ==> (n = m)) ==> power_free n 2174 By power_free_def, this is to show: 2175 (n = m ** e) ==> (m = n) /\ (e = 1) 2176 Note perfect_power n m by perfect_power_def, ?e. 2177 ==> m = n by implication 2178 so n = n ** e by given, m = n 2179 ==> e = 1 by POWER_EQ_SELF 2180*) 2181val power_free_alt = store_thm( 2182 "power_free_alt", 2183 ``!n. power_free n <=> 1 < n /\ (!m. perfect_power n m ==> (n = m))``, 2184 rw[EQ_IMP_THM] >- 2185 rw[power_free_gt_1] >- 2186 fs[power_free_def, perfect_power_def] >> 2187 fs[power_free_def, perfect_power_def] >> 2188 rpt strip_tac >- 2189 metis_tac[] >> 2190 `n = m` by metis_tac[] >> 2191 metis_tac[POWER_EQ_SELF]); 2192 2193(* Theorem: prime n ==> power_free n *) 2194(* Proof: 2195 Let n = m ** e. To show that n is power_free, 2196 (1) show m = n, by squeezing m as a factor of prime n. 2197 (2) show e = 1, by applying prime_powers_eq 2198 This is a typical detective-style proof. 2199 2200 Note prime n ==> n <> 1 by NOT_PRIME_1 2201 2202 Claim: !m e. n = m ** e ==> m = n 2203 Proof: Note m <> 1 by EXP_1, n <> 1 2204 and e <> 0 by EXP, n <> 1 2205 Thus e = SUC k for some k by num_CASES 2206 n = m ** SUC k 2207 = m * (m ** k) by EXP 2208 = (m ** k) * m by MULT_COMM 2209 Thus m divides n, by divides_def 2210 But m <> 1, so m = n by prime_def 2211 2212 The claim satisfies half of the power_free_def. 2213 With m = n, prime m, 2214 and e <> 0 by EXP, n <> 1 2215 Thus n = n ** 1 = m ** e by EXP_1 2216 ==> e = 1 by prime_powers_eq, 0 < e. 2217*) 2218val prime_is_power_free = store_thm( 2219 "prime_is_power_free", 2220 ``!n. prime n ==> power_free n``, 2221 rpt strip_tac >> 2222 `n <> 1` by metis_tac[NOT_PRIME_1] >> 2223 `!m e. (n = m ** e) ==> (m = n)` by 2224 (rpt strip_tac >> 2225 `m <> 1` by metis_tac[EXP_1] >> 2226 metis_tac[EXP, num_CASES, MULT_COMM, divides_def, prime_def]) >> 2227 `!m e. (n = m ** e) ==> (e = 1)` by metis_tac[EXP, EXP_1, prime_powers_eq, NOT_ZERO_LT_ZERO] >> 2228 metis_tac[power_free_def]); 2229 2230(* Theorem: power_free n /\ perfect_power n m ==> (n = m) *) 2231(* Proof: 2232 Note ?e. n = m ** e by perfect_power_def 2233 ==> n = m by power_free_def 2234*) 2235val power_free_perfect_power = store_thm( 2236 "power_free_perfect_power", 2237 ``!m n. power_free n /\ perfect_power n m ==> (n = m)``, 2238 metis_tac[perfect_power_def, power_free_def]); 2239 2240(* Theorem: power_free n ==> (!j. 1 < j ==> (ROOT j n) ** j <> n) *) 2241(* Proof: 2242 By contradiction, suppose (ROOT j n) ** j = n. 2243 Then j = 1 by power_free_def 2244 This contradicts 1 < j. 2245*) 2246val power_free_property = store_thm( 2247 "power_free_property", 2248 ``!n. power_free n ==> (!j. 1 < j ==> (ROOT j n) ** j <> n)``, 2249 spose_not_then strip_assume_tac >> 2250 `j = 1` by metis_tac[power_free_def] >> 2251 decide_tac); 2252 2253(* We have: 2254power_free_0 |- power_free 0 <=> F 2255power_free_1 |- power_free 1 <=> F 2256So, given 1 < n, how to check power_free n ? 2257*) 2258 2259(* Theorem: power_free n <=> 1 < n /\ (!j. 1 < j ==> (ROOT j n) ** j <> n) *) 2260(* Proof: 2261 If part: power_free n ==> 1 < n /\ (!j. 1 < j ==> (ROOT j n) ** j <> n) 2262 Note 1 < n by power_free_gt_1 2263 The rest is true by power_free_property. 2264 Only-if part: 1 < n /\ (!j. 1 < j ==> (ROOT j n) ** j <> n) ==> power_free n 2265 By contradiction, assume ~(power_free n). 2266 That is, ?m e. n = m ** e /\ (m = m ** e ==> e <> 1) by power_free_def 2267 Note 1 < m /\ 0 < e by ONE_LT_EXP, 1 < n 2268 Thus ROOT e n = m by ROOT_POWER, 1 < m, 0 < e 2269 By the implication, ~(1 < e), or e <= 1. 2270 Since 0 < e, this shows e = 1. 2271 Then m = m ** e by EXP_1 2272 This gives e <> 1, a contradiction. 2273*) 2274val power_free_check_all = store_thm( 2275 "power_free_check_all", 2276 ``!n. power_free n <=> 1 < n /\ (!j. 1 < j ==> (ROOT j n) ** j <> n)``, 2277 rw[EQ_IMP_THM] >- 2278 rw[power_free_gt_1] >- 2279 rw[power_free_property] >> 2280 simp[power_free_def] >> 2281 spose_not_then strip_assume_tac >> 2282 `1 < m /\ 0 < e` by metis_tac[ONE_LT_EXP] >> 2283 `ROOT e n = m` by rw[ROOT_POWER] >> 2284 `~(1 < e)` by metis_tac[] >> 2285 `e = 1` by decide_tac >> 2286 rw[]); 2287 2288(* However, there is no need to check all the exponents: 2289 just up to (LOG2 n) or (ulog n) is sufficient. 2290 See earlier part with power_free_upto_def. *) 2291 2292(* ------------------------------------------------------------------------- *) 2293(* Upper Logarithm *) 2294(* ------------------------------------------------------------------------- *) 2295 2296(* Find the power of 2 more or equal to n *) 2297val count_up_def = tDefine "count_up" ` 2298 count_up n m k = 2299 if m = 0 then 0 (* just to provide m <> 0 for the next one *) 2300 else if n <= m then k else count_up n (2 * m) (SUC k) 2301` (WF_REL_TAC `measure (\(n, m, k). n - m)`); 2302 2303(* Define upper LOG2 n by count_up *) 2304val ulog_def = Define` 2305 ulog n = count_up n 1 0 2306`; 2307 2308(* 2309> EVAL ``ulog 1``; --> 0 2310> EVAL ``ulog 2``; --> 1 2311> EVAL ``ulog 3``; --> 2 2312> EVAL ``ulog 4``; --> 2 2313> EVAL ``ulog 5``; --> 3 2314> EVAL ``ulog 6``; --> 3 2315> EVAL ``ulog 7``; --> 3 2316> EVAL ``ulog 8``; --> 3 2317> EVAL ``ulog 9``; --> 4 2318*) 2319 2320(* Theorem: ulog 0 = 0 *) 2321(* Proof: 2322 ulog 0 2323 = count_up 0 1 0 by ulog_def 2324 = 0 by count_up_def, 0 <= 1 2325*) 2326val ulog_0 = store_thm( 2327 "ulog_0[simp]", 2328 ``ulog 0 = 0``, 2329 rw[ulog_def, Once count_up_def]); 2330 2331(* Theorem: ulog 1 = 0 *) 2332(* Proof: 2333 ulog 1 2334 = count_up 1 1 0 by ulog_def 2335 = 0 by count_up_def, 1 <= 1 2336*) 2337val ulog_1 = store_thm( 2338 "ulog_1[simp]", 2339 ``ulog 1 = 0``, 2340 rw[ulog_def, Once count_up_def]); 2341 2342(* Theorem: ulog 2 = 1 *) 2343(* Proof: 2344 ulog 2 2345 = count_up 2 1 0 by ulog_def 2346 = count_up 2 2 1 by count_up_def, ~(1 < 2) 2347 = 1 by count_up_def, 2 <= 2 2348*) 2349val ulog_2 = store_thm( 2350 "ulog_2[simp]", 2351 ``ulog 2 = 1``, 2352 rw[ulog_def, Once count_up_def] >> 2353 rw[Once count_up_def]); 2354 2355(* Theorem: m <> 0 /\ n <= m ==> !k. count_up n m k = k *) 2356(* Proof: by count_up_def *) 2357val count_up_exit = store_thm( 2358 "count_up_exit", 2359 ``!m n. m <> 0 /\ n <= m ==> !k. count_up n m k = k``, 2360 rw[Once count_up_def]); 2361 2362(* Theorem: m <> 0 /\ m < n ==> !k. count_up n m k = count_up n (2 * m) (SUC k) *) 2363(* Proof: by count_up_def *) 2364val count_up_suc = store_thm( 2365 "count_up_suc", 2366 ``!m n. m <> 0 /\ m < n ==> !k. count_up n m k = count_up n (2 * m) (SUC k)``, 2367 rw[Once count_up_def]); 2368 2369(* Theorem: m <> 0 ==> 2370 !t. 2 ** t * m < n ==> !k. count_up n m k = count_up n (2 ** (SUC t) * m) ((SUC k) + t) *) 2371(* Proof: 2372 By induction on t. 2373 Base: 2 ** 0 * m < n ==> !k. count_up n m k = count_up n (2 ** SUC 0 * m) (SUC k + 0) 2374 Simplifying, this is to show: 2375 m < n ==> !k. count_up n m k = count_up n (2 * m) (SUC k) 2376 which is true by count_up_suc. 2377 Step: 2 ** t * m < n ==> !k. count_up n m k = count_up n (2 ** SUC t * m) (SUC k + t) ==> 2378 2 ** SUC t * m < n ==> !k. count_up n m k = count_up n (2 ** SUC (SUC t) * m) (SUC k + SUC t) 2379 Note 2 ** SUC t <> 0 by EXP_EQ_0, 2 <> 0 2380 so 2 ** SUC t * m <> 0 by MULT_EQ_0, m <> 0 2381 and 2 ** SUC t * m 2382 = 2 * 2 ** t * m by EXP 2383 = 2 * (2 ** t * m) by MULT_ASSOC 2384 Thus (2 ** t * m) < n by MULT_LESS_IMP_LESS, 0 < 2 2385 count_up n m k 2386 = count_up n (2 ** SUC t * m) (SUC k + t) by induction hypothesis 2387 = count_up n (2 * (2 ** SUC t * m)) (SUC (SUC k + t)) by count_up_suc 2388 = count_up n (2 ** SUC (SUC t) * m) (SUC k + SUC t) by EXP, ADD1 2389*) 2390val count_up_suc_eqn = store_thm( 2391 "count_up_suc_eqn", 2392 ``!m. m <> 0 ==> 2393 !n t. 2 ** t * m < n ==> !k. count_up n m k = count_up n (2 ** (SUC t) * m) ((SUC k) + t)``, 2394 ntac 3 strip_tac >> 2395 Induct >- 2396 rw[count_up_suc] >> 2397 rpt strip_tac >> 2398 qabbrev_tac `q = 2 ** t * m` >> 2399 `2 ** SUC t <> 0` by metis_tac[EXP_EQ_0, DECIDE``2 <> 0``] >> 2400 `2 ** SUC t * m <> 0` by metis_tac[MULT_EQ_0] >> 2401 `2 ** SUC t * m = 2 * q` by rw_tac std_ss[EXP, MULT_ASSOC, Abbr`q`] >> 2402 `q < n` by rw[MULT_LESS_IMP_LESS] >> 2403 rw[count_up_suc, EXP, ADD1]); 2404 2405(* Theorem: m <> 0 ==> !n t. 2 ** t * m < 2 * n /\ n <= 2 ** t * m ==> !k. count_up n m k = k + t *) 2406(* Proof: 2407 If t = 0, 2408 Then n <= m by EXP 2409 so count_up n m k 2410 = k by count_up_exit 2411 = k + 0 by ADD_0 2412 If t <> 0, 2413 Then ?s. t = SUC s by num_CASES 2414 Note 2 ** t * m 2415 = 2 ** SUC s * m by above 2416 = 2 * 2 ** s * m by EXP 2417 = 2 * (2 ** s * m) by MULT_ASSOC 2418 Note 2 ** SUC s * m < 2 * n by given 2419 so (2 ** s * m) < n by LT_MULT_RCANCEL, 2 <> 0 2420 2421 count_up n m k 2422 = count_up n (2 ** t * m) ((SUC k) + t) by count_up_suc_eqn 2423 = (SUC k) + t by count_up_exit 2424*) 2425val count_up_exit_eqn = store_thm( 2426 "count_up_exit_eqn", 2427 ``!m. m <> 0 ==> !n t. 2 ** t * m < 2 * n /\ n <= 2 ** t * m ==> !k. count_up n m k = k + t``, 2428 rpt strip_tac >> 2429 Cases_on `t` >- 2430 fs[count_up_exit] >> 2431 qabbrev_tac `q = 2 ** n' * m` >> 2432 `2 ** SUC n' * m = 2 * q` by rw_tac std_ss[EXP, MULT_ASSOC, Abbr`q`] >> 2433 `q < n` by decide_tac >> 2434 `count_up n m k = count_up n (2 ** (SUC n') * m) ((SUC k) + n')` by rw[count_up_suc_eqn, Abbr`q`] >> 2435 `_ = (SUC k) + n'` by rw[count_up_exit] >> 2436 rw[]); 2437 2438(* Theorem: 2 ** m < 2 * n /\ n <= 2 ** m ==> (ulog n = m) *) 2439(* Proof: 2440 Put m = 1 in count_up_exit_eqn: 2441 2 ** t * 1 < 2 * n /\ n <= 2 ** t * 1 ==> !k. count_up n 1 k = k + t 2442 Put k = 0, and apply MULT_RIGHT_1, ADD: 2443 2 ** t * 1 < 2 * n /\ n <= 2 ** t * 1 ==> count_up n 1 0 = t 2444 Then apply ulog_def to get the result, and rename t by m. 2445*) 2446val ulog_unique = store_thm( 2447 "ulog_unique", 2448 ``!m n. 2 ** m < 2 * n /\ n <= 2 ** m ==> (ulog n = m)``, 2449 metis_tac[ulog_def, count_up_exit_eqn, MULT_RIGHT_1, ADD, DECIDE``1 <> 0``]); 2450 2451(* Theorem: ulog n = if 1 < n then SUC (LOG2 (n - 1)) else 0 *) 2452(* Proof: 2453 If 1 < n, 2454 Then 0 < n - 1 by 1 < n 2455 ==> 2 ** LOG2 (n - 1) <= (n - 1) /\ 2456 (n - 1) < 2 ** SUC (LOG2 (n - 1)) by LOG2_PROPERTY 2457 or 2 ** LOG2 (n - 1) < n /\ 2458 n <= 2 ** SUC (LOG2 (n - 1)) by shifting inequalities 2459 Let t = SUC (LOG2 (n - 1)). 2460 Then 2 ** t = 2 * 2 ** (LOG2 (n - 1)) by EXP 2461 < 2 * n by LT_MULT_LCANCEL, 2 ** LOG2 (n - 1) < n 2462 Thus ulog n = t by ulog_unique. 2463 If ~(1 < n), 2464 Then n <= 1, or n = 0 or n = 1. 2465 If n = 0, ulog n = 0 by ulog_0 2466 If n = 1, ulog n = 0 by ulog_1 2467*) 2468val ulog_eqn = store_thm( 2469 "ulog_eqn", 2470 ``!n. ulog n = if 1 < n then SUC (LOG2 (n - 1)) else 0``, 2471 rw[] >| [ 2472 `0 < n - 1` by decide_tac >> 2473 `2 ** LOG2 (n - 1) <= (n - 1) /\ (n - 1) < 2 ** SUC (LOG2 (n - 1))` by metis_tac[LOG2_PROPERTY] >> 2474 `2 * 2 ** LOG2 (n - 1) < 2 * n /\ n <= 2 ** SUC (LOG2 (n - 1))` by decide_tac >> 2475 rw[EXP, ulog_unique], 2476 metis_tac[ulog_0, ulog_1, DECIDE``~(1 < n) <=> (n = 0) \/ (n = 1)``] 2477 ]); 2478 2479(* Theorem: 0 < n ==> (ulog (SUC n) = SUC (LOG2 n)) *) 2480(* Proof: 2481 Note 0 < n ==> 1 < SUC n by LT_ADD_RCANCEL, ADD1 2482 Thus ulog (SUC n) 2483 = SUC (LOG2 (SUC n - 1)) by ulog_eqn 2484 = SUC (LOG2 n) by SUC_SUB1 2485*) 2486val ulog_suc = store_thm( 2487 "ulog_suc", 2488 ``!n. 0 < n ==> (ulog (SUC n) = SUC (LOG2 n))``, 2489 rpt strip_tac >> 2490 `1 < SUC n` by decide_tac >> 2491 rw[ulog_eqn]); 2492 2493(* Theorem: 0 < n ==> 2 ** (ulog n) < 2 * n /\ n <= 2 ** (ulog n) *) 2494(* Proof: 2495 Apply ulog_eqn, this is to show: 2496 (1) 1 < n ==> 2 ** SUC (LOG2 (n - 1)) < 2 * n 2497 Let m = n - 1. 2498 Note 0 < m by 1 < n 2499 ==> 2 ** LOG2 m <= m by TWO_EXP_LOG2_LE, 0 < m 2500 or <= n - 1 by notation 2501 Thus 2 ** LOG2 m < n by inequality [1] 2502 and 2 ** SUC (LOG2 m) 2503 = 2 * 2 ** (LOG2 m) by EXP 2504 < 2 * n by LT_MULT_LCANCEL, [1] 2505 (2) 1 < n ==> n <= 2 ** SUC (LOG2 (n - 1)) 2506 Let m = n - 1. 2507 Note 0 < m by 1 < n 2508 ==> m < 2 ** SUC (LOG2 m) by LOG2_PROPERTY, 0 < m 2509 n - 1 < 2 ** SUC (LOG2 m) by notation 2510 n <= 2 ** SUC (LOG2 m) by inequality [2] 2511 or n <= 2 ** SUC (LOG2 (n - 1)) by notation 2512*) 2513val ulog_property = store_thm( 2514 "ulog_property", 2515 ``!n. 0 < n ==> 2 ** (ulog n) < 2 * n /\ n <= 2 ** (ulog n)``, 2516 rw[ulog_eqn] >| [ 2517 `0 < n - 1` by decide_tac >> 2518 qabbrev_tac `m = n - 1` >> 2519 `2 ** SUC (LOG2 m) = 2 * 2 ** (LOG2 m)` by rw[EXP] >> 2520 `2 ** LOG2 m <= n - 1` by rw[TWO_EXP_LOG2_LE, Abbr`m`] >> 2521 decide_tac, 2522 `0 < n - 1` by decide_tac >> 2523 qabbrev_tac `m = n - 1` >> 2524 `2 ** SUC (LOG2 m) = 2 * 2 ** (LOG2 m)` by rw[EXP] >> 2525 `n - 1 < 2 ** SUC (LOG2 m)` by metis_tac[LOG2_PROPERTY] >> 2526 decide_tac 2527 ]); 2528 2529(* Theorem: 0 < n ==> !m. (ulog n = m) <=> 2 ** m < 2 * n /\ n <= 2 ** m *) 2530(* Proof: 2531 If part: 0 < n ==> 2 ** (ulog n) < 2 * n /\ n <= 2 ** (ulog n) 2532 True by ulog_property, 0 < n 2533 Only-if part: 2 ** m < 2 * n /\ n <= 2 ** m ==> ulog n = m 2534 True by ulog_unique 2535*) 2536val ulog_thm = store_thm( 2537 "ulog_thm", 2538 ``!n. 0 < n ==> !m. (ulog n = m) <=> (2 ** m < 2 * n /\ n <= 2 ** m)``, 2539 metis_tac[ulog_property, ulog_unique]); 2540 2541(* Have an equation to present the definition *) 2542val ulog_def_alt = save_thm("ulog_def_alt", CONJ ulog_0 ulog_thm); 2543(* val ulog_def_alt = 2544|- (ulog 0 = 0) /\ !n. 0 < n ==> !m. ulog n = m <=> 2 ** m < TWICE n /\ n <= 2 ** m: thm *) 2545 2546(* This is OK, but the followig is better *) 2547 2548(* Theorem: (ulog 0 = 0) /\ !n. 0 < n ==> !m. (ulog n = m) <=> (n <= 2 ** m /\ 2 ** m < 2 * n) *) 2549(* Proof: by ulog_0 ulog_thm *) 2550val ulog_def_alt = store_thm( 2551 "ulog_def_alt", 2552 ``(ulog 0 = 0) /\ !n. 0 < n ==> !m. (ulog n = m) <=> (n <= 2 ** m /\ 2 ** m < 2 * n)``, 2553 rw[ulog_0, ulog_thm]); 2554 2555(* Theorem: (ulog n = 0) <=> ((n = 0) \/ (n = 1)) *) 2556(* Proof: 2557 Note !n. SUC n <> 0 by NOT_SUC 2558 so if 1 < n, ulog n <> 0 by ulog_eqn 2559 Thus ulog n = 0 <=> ~(1 < n) by above 2560 or <=> n <= 1 by negation 2561 or <=> n = 0 or n = 1 by range 2562*) 2563val ulog_eq_0 = store_thm( 2564 "ulog_eq_0", 2565 ``!n. (ulog n = 0) <=> ((n = 0) \/ (n = 1))``, 2566 rw[ulog_eqn]); 2567 2568(* Theorem: (ulog n = 1) <=> (n = 2) *) 2569(* Proof: 2570 If part: ulog n = 1 ==> n = 2 2571 Note n <> 0 and n <> 1 by ulog_eq_0 2572 Thus 1 < n, or 0 < n - 1 by arithmetic 2573 ==> SUC (LOG2 (n - 1)) = 1 by ulog_eqn, 1 < n 2574 or LOG2 (n - 1) = 0 by SUC_EQ, ONE 2575 ==> n - 1 < 2 by LOG_EQ_0, 0 < n - 1 2576 or n <= 2 by inequality 2577 Combine with 1 < n, n = 2. 2578 Only-if part: ulog 2 = 1 2579 ulog 2 2580 = ulog (SUC 1) by TWO 2581 = SUC (LOG2 1) by ulog_suc 2582 = SUC 0 by LOG_1, 0 < 2 2583 = 1 by ONE 2584*) 2585val ulog_eq_1 = store_thm( 2586 "ulog_eq_1", 2587 ``!n. (ulog n = 1) <=> (n = 2)``, 2588 rw[EQ_IMP_THM] >> 2589 `n <> 0 /\ n <> 1` by metis_tac[ulog_eq_0, DECIDE``1 <> 0``] >> 2590 `1 < n /\ 0 < n - 1` by decide_tac >> 2591 `SUC (LOG2 (n - 1)) = 1` by metis_tac[ulog_eqn] >> 2592 `LOG2 (n - 1) = 0` by decide_tac >> 2593 `n - 1 < 2` by metis_tac[LOG_EQ_0, DECIDE``1 < 2``] >> 2594 decide_tac); 2595 2596(* Theorem: ulog n <= 1 <=> n <= 2 *) 2597(* Proof: 2598 ulog n <= 1 2599 <=> ulog n = 0 \/ ulog n = 1 by arithmetic 2600 <=> n = 0 \/ n = 1 \/ n = 2 by ulog_eq_0, ulog_eq_1 2601 <=> n <= 2 by arithmetic 2602 2603*) 2604val ulog_le_1 = store_thm( 2605 "ulog_le_1", 2606 ``!n. ulog n <= 1 <=> n <= 2``, 2607 rpt strip_tac >> 2608 `ulog n <= 1 <=> ((ulog n = 0) \/ (ulog n = 1))` by decide_tac >> 2609 rw[ulog_eq_0, ulog_eq_1]); 2610 2611(* Theorem: n <= m ==> ulog n <= ulog m *) 2612(* Proof: 2613 If n = 0, 2614 Note ulog 0 = 0 by ulog_0 2615 and 0 <= ulog m for anything 2616 If n = 1, 2617 Note ulog 1 = 0 by ulog_1 2618 Thus 0 <= ulog m by arithmetic 2619 If n <> 1, then 1 < n 2620 Note n <= m, so 1 < m 2621 Thus 0 < n - 1 by arithmetic 2622 and n - 1 <= m - 1 by arithmetic 2623 ==> LOG2 (n - 1) <= LOG2 (m - 1) by LOG2_LE 2624 ==> SUC (LOG2 (n - 1)) <= SUC (LOG2 (m - 1)) by LESS_EQ_MONO 2625 or ulog n <= ulog m by ulog_eqn, 1 < n, 1 < m 2626*) 2627val ulog_le = store_thm( 2628 "ulog_le", 2629 ``!m n. n <= m ==> ulog n <= ulog m``, 2630 rpt strip_tac >> 2631 Cases_on `n = 0` >- 2632 rw[] >> 2633 Cases_on `n = 1` >- 2634 rw[] >> 2635 rw[ulog_eqn, LOG2_LE]); 2636 2637(* Theorem: n < m ==> ulog n <= ulog m *) 2638(* Proof: by ulog_le *) 2639val ulog_lt = store_thm( 2640 "ulog_lt", 2641 ``!m n. n < m ==> ulog n <= ulog m``, 2642 rw[ulog_le]); 2643 2644(* Theorem: ulog (2 ** n) = n *) 2645(* Proof: 2646 Note 0 < 2 ** n by EXP_POS, 0 < 2 2647 From 1 < 2 by arithmetic 2648 ==> 2 ** n < 2 * 2 ** n by LT_MULT_RCANCEL, 0 < 2 ** n 2649 Now 2 ** n <= 2 ** n by LESS_EQ_REFL 2650 Thus ulog (2 ** n) = n by ulog_unique 2651*) 2652val ulog_2_exp = store_thm( 2653 "ulog_2_exp", 2654 ``!n. ulog (2 ** n) = n``, 2655 rpt strip_tac >> 2656 `0 < 2 ** n` by rw[EXP_POS] >> 2657 `2 ** n < 2 * 2 ** n` by decide_tac >> 2658 `2 ** n <= 2 ** n` by decide_tac >> 2659 rw[ulog_unique]); 2660 2661(* Theorem: ulog n <= n *) 2662(* Proof: 2663 Note n < 2 ** n by X_LT_EXP_X 2664 Thus ulog n <= ulog (2 ** n) by ulog_lt 2665 or ulog n <= n by ulog_2_exp 2666*) 2667val ulog_le_self = store_thm( 2668 "ulog_le_self", 2669 ``!n. ulog n <= n``, 2670 metis_tac[X_LT_EXP_X, ulog_lt, ulog_2_exp, DECIDE``1 < 2n``]); 2671 2672(* Theorem: ulog n = n <=> n = 0 *) 2673(* Proof: 2674 If part: ulog n = n ==> n = 0 2675 By contradiction, assume n <> 0 2676 Then ?k. n = SUC k by num_CASES, n < 0 2677 so 2 ** SUC k < 2 * SUC k by ulog_property 2678 or 2 * 2 ** k < 2 * SUC k by EXP 2679 ==> 2 ** k < SUC k by arithmetic 2680 or 2 ** k <= k by arithmetic 2681 This contradicts k < 2 ** k by X_LT_EXP_X, 0 < 2 2682 Only-if part: ulog 0 = 0 2683 This is true by ulog_0 2684*) 2685val ulog_eq_self = store_thm( 2686 "ulog_eq_self", 2687 ``!n. (ulog n = n) <=> (n = 0)``, 2688 rw[EQ_IMP_THM] >> 2689 spose_not_then strip_assume_tac >> 2690 `?k. n = SUC k` by metis_tac[num_CASES] >> 2691 `2 * (2 ** k) = 2 ** SUC k` by rw[EXP] >> 2692 `0 < n` by decide_tac >> 2693 `2 ** SUC k < 2 * SUC k` by metis_tac[ulog_property] >> 2694 `2 ** k <= k` by decide_tac >> 2695 `k < 2 ** k` by rw[X_LT_EXP_X] >> 2696 decide_tac); 2697 2698(* Theorem: 0 < n ==> ulog n < n *) 2699(* Proof: 2700 By contradiction, assume ~(ulog n < n). 2701 Then n <= ulog n by ~(ulog n < n) 2702 But ulog n <= n by ulog_le_self 2703 ==> ulog n = n by arithmetic 2704 so n = 0 by ulog_eq_self 2705 This contradicts 0 < n. 2706*) 2707val ulog_lt_self = store_thm( 2708 "ulog_lt_self", 2709 ``!n. 0 < n ==> ulog n < n``, 2710 rpt strip_tac >> 2711 spose_not_then strip_assume_tac >> 2712 `ulog n <= n` by rw[ulog_le_self] >> 2713 `ulog n = n` by decide_tac >> 2714 `n = 0` by rw[GSYM ulog_eq_self] >> 2715 decide_tac); 2716 2717(* Theorem: (2 ** (ulog n) = n) <=> perfect_power n 2 *) 2718(* Proof: 2719 Using perfect_power_def, 2720 If part: 2 ** (ulog n) = n ==> ?e. n = 2 ** e 2721 True by taking e = ulog n. 2722 Only-if part: 2 ** ulog (2 ** e) = 2 ** e 2723 This is true by ulog_2_exp 2724*) 2725val ulog_exp_exact = store_thm( 2726 "ulog_exp_exact", 2727 ``!n. (2 ** (ulog n) = n) <=> perfect_power n 2``, 2728 rw[perfect_power_def, EQ_IMP_THM] >- 2729 metis_tac[] >> 2730 rw[ulog_2_exp]); 2731 2732(* Theorem: ~(perfect_power n 2) ==> 2 ** ulog n <> n *) 2733(* Proof: by ulog_exp_exact. *) 2734val ulog_exp_not_exact = store_thm( 2735 "ulog_exp_not_exact", 2736 ``!n. ~(perfect_power n 2) ==> 2 ** ulog n <> n``, 2737 rw[ulog_exp_exact]); 2738 2739(* Theorem: 0 < n /\ ~(perfect_power n 2) ==> n < 2 ** ulog n *) 2740(* Proof: 2741 Note n <= 2 ** ulog n by ulog_property, 0 < n 2742 But n <> 2 ** ulog n by ulog_exp_not_exact, ~(perfect_power n 2) 2743 Thus n < 2 ** ulog n by LESS_OR_EQ 2744*) 2745val ulog_property_not_exact = store_thm( 2746 "ulog_property_not_exact", 2747 ``!n. 0 < n /\ ~(perfect_power n 2) ==> n < 2 ** ulog n``, 2748 metis_tac[ulog_property, ulog_exp_not_exact, LESS_OR_EQ]); 2749 2750(* Theorem: 1 < n /\ ODD n ==> n < 2 ** ulog n *) 2751(* Proof: 2752 Note 0 < n /\ n <> 1 by 1 < n 2753 Thus n <= 2 ** ulog n by ulog_property, 0 < n 2754 But ~(perfect_power n 2) by perfect_power_2_odd, n <> 1 2755 ==> n <> 2 ** ulog n by ulog_exp_not_exact, ~(perfect_power n 2) 2756 Thus n < 2 ** ulog n by LESS_OR_EQ 2757*) 2758val ulog_property_odd = store_thm( 2759 "ulog_property_odd", 2760 ``!n. 1 < n /\ ODD n ==> n < 2 ** ulog n``, 2761 rpt strip_tac >> 2762 `0 < n /\ n <> 1` by decide_tac >> 2763 `n <= 2 ** ulog n` by metis_tac[ulog_property] >> 2764 `~(perfect_power n 2)` by metis_tac[perfect_power_2_odd] >> 2765 `2 ** ulog n <> n` by rw[ulog_exp_not_exact] >> 2766 decide_tac); 2767 2768(* Theorem: n <= 2 ** m ==> ulog n <= m *) 2769(* Proof: 2770 n <= 2 ** m 2771 ==> ulog n <= ulog (2 ** m) by ulog_le 2772 ==> ulog n <= m by ulog_2_exp 2773*) 2774val exp_to_ulog = store_thm( 2775 "exp_to_ulog", 2776 ``!m n. n <= 2 ** m ==> ulog n <= m``, 2777 metis_tac[ulog_le, ulog_2_exp]); 2778 2779(* Theorem: 1 < n ==> 0 < ulog n *) 2780(* Proof: 2781 Note 1 < n ==> n <> 0 /\ n <> 1 by arithmetic 2782 so ulog n <> 0 by ulog_eq_0 2783 or 0 < ulog n by NOT_ZERO_LT_ZERO 2784*) 2785val ulog_pos = store_thm( 2786 "ulog_pos[simp]", 2787 ``!n. 1 < n ==> 0 < ulog n``, 2788 metis_tac[ulog_eq_0, NOT_ZERO, DECIDE``1 < n <=> n <> 0 /\ n <> 1``]); 2789 2790(* Theorem: 1 < n ==> 1 <= ulog n *) 2791(* Proof: 2792 Note 0 < ulog n by ulog_pos 2793 Thus 1 <= ulog n by arithmetic 2794*) 2795val ulog_ge_1 = store_thm( 2796 "ulog_ge_1", 2797 ``!n. 1 < n ==> 1 <= ulog n``, 2798 metis_tac[ulog_pos, DECIDE``0 < n ==> 1 <= n``]); 2799 2800(* Theorem: 2 < n ==> 1 < (ulog n) ** 2 *) 2801(* Proof: 2802 Note 1 < n /\ n <> 2 by 2 < n 2803 so 0 < ulog n by ulog_pos, 1 < n 2804 and ulog n <> 1 by ulog_eq_1, n <> 2 2805 Thus 1 < ulog n by ulog n <> 0, ulog n <> 1 2806 so 1 < (ulog n) ** 2 by ONE_LT_EXP, 0 < 2 2807*) 2808val ulog_sq_gt_1 = store_thm( 2809 "ulog_sq_gt_1", 2810 ``!n. 2 < n ==> 1 < (ulog n) ** 2``, 2811 rpt strip_tac >> 2812 `1 < n /\ n <> 2` by decide_tac >> 2813 `0 < ulog n` by rw[] >> 2814 `ulog n <> 1` by rw[ulog_eq_1] >> 2815 `1 < ulog n` by decide_tac >> 2816 rw[ONE_LT_EXP]); 2817 2818(* Theorem: 1 < n ==> 4 <= (2 * ulog n) ** 2 *) 2819(* Proof: 2820 Note 0 < ulog n by ulog_pos, 1 < n 2821 Thus 2 <= 2 * ulog n by arithmetic 2822 or 4 <= (2 * ulog n) ** 2 by EXP_BASE_LE_MONO 2823*) 2824val ulog_twice_sq = store_thm( 2825 "ulog_twice_sq", 2826 ``!n. 1 < n ==> 4 <= (2 * ulog n) ** 2``, 2827 rpt strip_tac >> 2828 `0 < ulog n` by rw[ulog_pos] >> 2829 `2 <= 2 * ulog n` by decide_tac >> 2830 `2 ** 2 <= (2 * ulog n) ** 2` by rw[EXP_BASE_LE_MONO] >> 2831 `2 ** 2 = 4` by rw[] >> 2832 decide_tac); 2833 2834(* Theorem: ulog n = if n = 0 then 0 2835 else if (perfect_power n 2) then (LOG2 n) else SUC (LOG2 n) *) 2836(* Proof: 2837 This is to show: 2838 (1) ulog 0 = 0, true by ulog_0 2839 (2) perfect_power n 2 ==> ulog n = LOG2 n 2840 Note ?k. n = 2 ** k by perfect_power_def 2841 Thus ulog n = k by ulog_exp_exact 2842 and LOG2 n = k by LOG_EXACT_EXP, 1 < 2 2843 (3) ~(perfect_power n 2) ==> ulog n = SUC (LOG2 n) 2844 Let m = SUC (LOG2 n). 2845 Then 2 ** m 2846 = 2 * 2 ** (LOG2 n) by EXP 2847 <= 2 * n by TWO_EXP_LOG2_LE 2848 But n <> LOG2 n by LOG2_EXACT_EXP, ~(perfect_power n 2) 2849 Thus 2 ** m < 2 * n [1] 2850 2851 Also n < 2 ** m by LOG2_PROPERTY 2852 Thus n <= 2 ** m, [2] 2853 giving ulog n = m by ulog_unique, [1] [2] 2854*) 2855val ulog_alt = store_thm( 2856 "ulog_alt", 2857 ``!n. ulog n = if n = 0 then 0 2858 else if (perfect_power n 2) then (LOG2 n) else SUC (LOG2 n)``, 2859 rw[] >- 2860 metis_tac[perfect_power_def, ulog_exp_exact, LOG_EXACT_EXP, DECIDE``1 < 2``] >> 2861 qabbrev_tac `m = SUC (LOG2 n)` >> 2862 (irule ulog_unique >> rpt conj_tac) >| [ 2863 `2 ** m = 2 * 2 ** (LOG2 n)` by rw[EXP, Abbr`m`] >> 2864 `2 ** (LOG2 n) <= n` by rw[TWO_EXP_LOG2_LE] >> 2865 `2 ** (LOG2 n) <> n` by rw[LOG2_EXACT_EXP, GSYM perfect_power_def] >> 2866 decide_tac, 2867 `n < 2 ** m` by rw[LOG2_PROPERTY, Abbr`m`] >> 2868 decide_tac 2869 ]); 2870 2871(* 2872Thus, for 0 < n, (ulog n) and SUC (LOG2 n) differ only for (perfect_power n 2). 2873This means that replacing AKS bounds of SUC (LOG2 n) by (ulog n) 2874only affect calculations involving (perfect_power n 2), 2875which are irrelevant for primality testing ! 2876However, in display, (ulog n) is better, while SUC (LOG2 n) is a bit ugly. 2877*) 2878 2879(* Theorem: 0 < n ==> (LOG2 n <= ulog n /\ ulog n <= 1 + LOG2 n) *) 2880(* Proof: by ulog_alt *) 2881val ulog_LOG2 = store_thm( 2882 "ulog_LOG2", 2883 ``!n. 0 < n ==> (LOG2 n <= ulog n /\ ulog n <= 1 + LOG2 n)``, 2884 rw[ulog_alt]); 2885 2886(* Theorem: 0 < n ==> !m. perfect_power n m <=> ?k. k <= ulog n /\ (n = m ** k) *) 2887(* Proof: by perfect_power_bound_LOG2, ulog_LOG2 *) 2888val perfect_power_bound_ulog = store_thm( 2889 "perfect_power_bound_ulog", 2890 ``!n. 0 < n ==> !m. perfect_power n m <=> ?k. k <= ulog n /\ (n = m ** k)``, 2891 rw[EQ_IMP_THM] >| [ 2892 `LOG2 n <= ulog n` by rw[ulog_LOG2] >> 2893 metis_tac[perfect_power_bound_LOG2, LESS_EQ_TRANS], 2894 metis_tac[perfect_power_def] 2895 ]); 2896 2897(* ------------------------------------------------------------------------- *) 2898(* Upper Log Theorems *) 2899(* ------------------------------------------------------------------------- *) 2900 2901(* Theorem: ulog (m * n) <= ulog m + ulog n *) 2902(* Proof: 2903 Let x = ulog (m * n), y = ulog m + ulog n. 2904 Note m * n <= 2 ** x < 2 * m * n by ulog_thm 2905 and m <= 2 ** ulog m < 2 * m by ulog_thm 2906 and n <= 2 ** ulog n < 2 * n by ulog_thm 2907 Note that 2 ** ulog m * 2 ** ulog n = 2 ** y by EXP_ADD 2908 Multiplying inequalities, 2909 m * n <= 2 ** y by LE_MONO_MULT2 2910 2 ** y < 4 * m * n by LT_MONO_MULT2 2911 The picture is: 2912 m * n ....... 2 * m * n ....... 4 * m * n 2913 2 ** x somewhere 2914 2 ** y somewhere 2915 If 2 ** y < 2 * m * n, 2916 Then x = y by ulog_unique 2917 Otherwise, 2918 2 ** y is in the second range. 2919 Then 2 ** x < 2 ** y since 2 ** x in the first 2920 or x < y by EXP_BASE_LT_MONO 2921 Combining these two cases: x <= y. 2922*) 2923val ulog_mult = store_thm( 2924 "ulog_mult", 2925 ``!m n. ulog (m * n) <= ulog m + ulog n``, 2926 rpt strip_tac >> 2927 Cases_on `(m = 0) \/ (n = 0)` >- 2928 fs[] >> 2929 `m * n <> 0` by rw[] >> 2930 `0 < m /\ 0 < n /\ 0 < m * n` by decide_tac >> 2931 qabbrev_tac `x = ulog (m * n)` >> 2932 qabbrev_tac `y = ulog m + ulog n` >> 2933 `m * n <= 2 ** x /\ 2 ** x < TWICE (m * n)` by metis_tac[ulog_thm] >> 2934 `m * n <= 2 ** y /\ 2 ** y < (TWICE m) * (TWICE n)` by metis_tac[ulog_thm, LE_MONO_MULT2, LT_MONO_MULT2, EXP_ADD] >> 2935 Cases_on `2 ** y < TWICE (m * n)` >| [ 2936 `y = x` by metis_tac[ulog_unique] >> 2937 decide_tac, 2938 `2 ** x < 2 ** y /\ 1 < 2` by decide_tac >> 2939 `x < y` by metis_tac[EXP_BASE_LT_MONO] >> 2940 decide_tac 2941 ]); 2942 2943(* Theorem: ulog (m ** n) <= n * ulog m *) 2944(* Proof: 2945 By induction on n. 2946 Base: ulog (m ** 0) <= 0 * ulog m 2947 LHS = ulog (m ** 0) 2948 = ulog 1 by EXP_0 2949 = 0 by ulog_1 2950 <= 0 * ulog m by MULT 2951 = RHS 2952 Step: ulog (m ** n) <= n * ulog m ==> ulog (m ** SUC n) <= SUC n * ulog m 2953 LHS = ulog (m ** SUC n) 2954 = ulog (m * m ** n) by EXP 2955 <= ulog m + ulog (m ** n) by ulog_mult 2956 <= ulog m + n * ulog m by induction hypothesis 2957 = (1 + n) * ulog m by RIGHT_ADD_DISTRIB 2958 = SUC n * ulog m by ADD1, ADD_COMM 2959 = RHS 2960*) 2961val ulog_exp = store_thm( 2962 "ulog_exp", 2963 ``!m n. ulog (m ** n) <= n * ulog m``, 2964 rpt strip_tac >> 2965 Induct_on `n` >> 2966 rw[EXP_0] >> 2967 `ulog (m ** SUC n) <= ulog m + ulog (m ** n)` by rw[EXP, ulog_mult] >> 2968 `ulog m + ulog (m ** n) <= ulog m + n * ulog m` by rw[] >> 2969 `ulog m + n * ulog m = SUC n * ulog m` by rw[ADD1] >> 2970 decide_tac); 2971 2972(* Theorem: 0 < n /\ EVEN n ==> (ulog n = 1 + ulog (HALF n)) *) 2973(* Proof: 2974 Let k = HALF n. 2975 Then 0 < k by HALF_EQ_0, EVEN n 2976 and EVEN n ==> n = TWICE k by EVEN_HALF 2977 Note n <= 2 ** ulog n < 2 * n by ulog_thm, by 0 < n 2978 and k <= 2 ** ulog k < 2 * k by ulog_thm, by 0 < k 2979 so 2 * k <= 2 * 2 ** ulog k < 2 * 2 * k by multiplying 2 2980 or n <= 2 ** (1 + ulog k) < 2 * n by EXP 2981 Thus ulog n = 1 + ulog k by ulog_unique 2982*) 2983val ulog_even = store_thm( 2984 "ulog_even", 2985 ``!n. 0 < n /\ EVEN n ==> (ulog n = 1 + ulog (HALF n))``, 2986 rpt strip_tac >> 2987 qabbrev_tac `k = HALF n` >> 2988 `n = TWICE k` by rw[EVEN_HALF, Abbr`k`] >> 2989 `0 < k` by rw[Abbr`k`] >> 2990 `n <= 2 ** ulog n /\ 2 ** ulog n < 2 * n` by metis_tac[ulog_thm] >> 2991 `k <= 2 ** ulog k /\ 2 ** ulog k < 2 * k` by metis_tac[ulog_thm] >> 2992 `2 <> 0` by decide_tac >> 2993 `n <= 2 * 2 ** ulog k` by rw[LE_MULT_LCANCEL] >> 2994 `2 * 2 ** ulog k < 2 * n` by rw[LT_MULT_LCANCEL] >> 2995 `2 * 2 ** ulog k = 2 ** (1 + ulog k)` by metis_tac[EXP, ADD1, ADD_COMM] >> 2996 metis_tac[ulog_unique]); 2997 2998(* Theorem: 1 < n /\ ODD n ==> ulog (HALF n) + 1 <= ulog n *) 2999(* Proof: 3000 Let k = HALF n. 3001 Then 0 < k by HALF_EQ_0, 1 < n 3002 and ODD n ==> n = TWICE k + 1 by ODD_HALF 3003 Note n <= 2 ** ulog n < 2 * n by ulog_thm, by 0 < n 3004 and k <= 2 ** ulog k < 2 * k by ulog_thm, by 0 < k 3005 so 2 * k <= 2 * 2 ** ulog k < 2 * 2 * k by multiplying 2 3006 or (2 * k) <= 2 ** (1 + ulog k) < 2 * (2 * k) by EXP 3007 Since 2 * k < n, so 2 * (2 * k) < 2 * n, 3008 the picture is: 3009 2 * k ... n ...... 2 * (2 * k) ... 2 * n 3010 <--- 2 ** ulog n ----> 3011 <--- 2 ** (1 + ulog k) --> 3012 If n <= 2 ** (1 + ulog k), then ulog n = 1 + ulog k by ulog_unique 3013 Otherwise, 2 ** (1 + ulog k) < 2 ** ulog n 3014 so 1 + ulog k < ulog n by EXP_BASE_LT_MONO, 1 < 2 3015 Combining, 1 + ulog k <= ulog n. 3016*) 3017val ulog_odd = store_thm( 3018 "ulog_odd", 3019 ``!n. 1 < n /\ ODD n ==> ulog (HALF n) + 1 <= ulog n``, 3020 rpt strip_tac >> 3021 qabbrev_tac `k = HALF n` >> 3022 `(n <> 0) /\ (n <> 1)` by decide_tac >> 3023 `0 < n /\ 0 < k` by metis_tac[HALF_EQ_0, NOT_ZERO_LT_ZERO] >> 3024 `n = TWICE k + 1` by rw[ODD_HALF, Abbr`k`] >> 3025 `n <= 2 ** ulog n /\ 2 ** ulog n < 2 * n` by metis_tac[ulog_thm] >> 3026 `k <= 2 ** ulog k /\ 2 ** ulog k < 2 * k` by metis_tac[ulog_thm] >> 3027 `2 <> 0 /\ 1 < 2` by decide_tac >> 3028 `2 * k <= 2 * 2 ** ulog k` by rw[LE_MULT_LCANCEL] >> 3029 `2 * 2 ** ulog k < 2 * (2 * k)` by rw[LT_MULT_LCANCEL] >> 3030 `2 * 2 ** ulog k = 2 ** (1 + ulog k)` by metis_tac[EXP, ADD1, ADD_COMM] >> 3031 Cases_on `n <= 2 ** (1 + ulog k)` >| [ 3032 `2 * k < n` by decide_tac >> 3033 `2 * (2 * k) < 2 * n` by rw[LT_MULT_LCANCEL] >> 3034 `2 ** (1 + ulog k) < TWICE n` by decide_tac >> 3035 `1 + ulog k = ulog n` by metis_tac[ulog_unique] >> 3036 decide_tac, 3037 `2 ** (1 + ulog k) < 2 ** ulog n` by decide_tac >> 3038 `1 + ulog k < ulog n` by metis_tac[EXP_BASE_LT_MONO] >> 3039 decide_tac 3040 ]); 3041 3042(* 3043EVAL ``let n = 13 in [ulog (HALF n) + 1; ulog n]``; 3044|- (let n = 13 in [ulog (HALF n) + 1; ulog n]) = [4; 4]: 3045|- (let n = 17 in [ulog (HALF n) + 1; ulog n]) = [4; 5]: 3046*) 3047 3048(* Theorem: 1 < n ==> ulog (HALF n) + 1 <= ulog n *) 3049(* Proof: 3050 Note 1 < n ==> 0 < n by arithmetic 3051 If EVEN n, true by ulog_even, 0 < n 3052 If ODD n, true by ulog_odd, 1 < n, ODD_EVEN. 3053*) 3054val ulog_half = store_thm( 3055 "ulog_half", 3056 ``!n. 1 < n ==> ulog (HALF n) + 1 <= ulog n``, 3057 rpt strip_tac >> 3058 Cases_on `EVEN n` >- 3059 rw[ulog_even] >> 3060 rw[ODD_EVEN, ulog_odd]); 3061 3062(* Theorem: SQRT n <= 2 ** (ulog n) *) 3063(* Proof: 3064 Note n <= 2 ** ulog n by ulog_property 3065 and SQRT n <= n by SQRT_LE_SELF 3066 Thus SQRT n <= 2 ** ulog n by LESS_EQ_TRANS 3067 or SQRT n <= 3068*) 3069val sqrt_upper = store_thm( 3070 "sqrt_upper", 3071 ``!n. SQRT n <= 2 ** (ulog n)``, 3072 rpt strip_tac >> 3073 Cases_on `n = 0` >- 3074 rw[] >> 3075 `n <= 2 ** ulog n` by rw[ulog_property] >> 3076 `SQRT n <= n` by rw[SQRT_LE_SELF] >> 3077 decide_tac); 3078 3079(* ------------------------------------------------------------------------- *) 3080(* Power Free up to a limit *) 3081(* ------------------------------------------------------------------------- *) 3082 3083(* Define a power free property of a number *) 3084val power_free_upto_def = Define` 3085 power_free_upto n k <=> !j. 1 < j /\ j <= k ==> (ROOT j n) ** j <> n 3086`; 3087(* make this an infix relation. *) 3088val _ = set_fixity "power_free_upto" (Infix(NONASSOC, 450)); (* same as relation *) 3089 3090(* Theorem: (n power_free_upto 0) = T *) 3091(* Proof: by power_free_upto_def, no counter-example. *) 3092val power_free_upto_0 = store_thm( 3093 "power_free_upto_0", 3094 ``!n. (n power_free_upto 0) = T``, 3095 rw[power_free_upto_def]); 3096 3097(* Theorem: (n power_free_upto 1) = T *) 3098(* Proof: by power_free_upto_def, no counter-example. *) 3099val power_free_upto_1 = store_thm( 3100 "power_free_upto_1", 3101 ``!n. (n power_free_upto 1) = T``, 3102 rw[power_free_upto_def]); 3103 3104(* Theorem: 0 < k /\ (n power_free_upto k) ==> 3105 ((n power_free_upto (k + 1)) <=> ROOT (k + 1) n ** (k + 1) <> n) *) 3106(* Proof: by power_free_upto_def *) 3107val power_free_upto_suc = store_thm( 3108 "power_free_upto_suc", 3109 ``!n k. 0 < k /\ (n power_free_upto k) ==> 3110 ((n power_free_upto (k + 1)) <=> ROOT (k + 1) n ** (k + 1) <> n)``, 3111 rw[power_free_upto_def] >> 3112 rw[EQ_IMP_THM] >> 3113 metis_tac[LESS_OR_EQ, DECIDE``k < n + 1 ==> k <= n``]); 3114 3115(* Theorem: ower_free n <=> 1 < n /\ n power_free_upto (LOG2 n) *) 3116(* Proof: 3117 By power_free_check_all and power_free_upto_def, 3118 this result is true if we can show that: 3119 1 < n /\ (!j. 1 < j ==> (ROOT j n) ** j <> n) <=> 3120 1 < n /\ (!j. 1 < j /\ j <= LOG2 n ==> (ROOT j n) ** j <> n) 3121 That is, to show that: 3122 1 < n /\ 1 < j /\ (!j. 1 < j /\ j <= LOG2 n ==> ROOT j n ** j <> n) ==> (ROOT j n) ** j <> n 3123 By contradiction, suppose (ROOT j n) ** j = n. 3124 Let m = ROOT j n. 3125 Then m ** j = n by above 3126 Thus perfect_power n m by perfect_power_def 3127 ==> ?k. k <= LOG2 n /\ n = m ** k by perfect_power_bound_LOG2 3128 But 1 < m by ONE_LT_EXP, 1 < n 3129 Thus j = k by EXP_BASE_INJECTIVE, 1 < m 3130 The implication gives m ** j <> n, a contradiction. 3131*) 3132val power_free_check_upto_LOG2 = store_thm( 3133 "power_free_check_upto_LOG2", 3134 ``!n. power_free n <=> 1 < n /\ n power_free_upto (LOG2 n)``, 3135 rw[power_free_check_all, power_free_upto_def] >> 3136 rw[EQ_IMP_THM] >> 3137 spose_not_then strip_assume_tac >> 3138 qabbrev_tac `m = ROOT j n` >> 3139 `perfect_power n m` by metis_tac[perfect_power_def] >> 3140 `?k. k <= LOG2 n /\ (n = m ** k)` by fs[GSYM perfect_power_bound_LOG2] >> 3141 `1 < m` by metis_tac[ONE_LT_EXP] >> 3142 `j = k` by fs[ ] >> 3143 metis_tac[]); 3144 3145(* Theorem: power_free n <=> 1 < n /\ (!j. 1 < j /\ j <= ulog n ==> (ROOT j n) ** j <> n) *) 3146(* Proof: 3147 By power_free_check_all and power_free_upto_def, 3148 this result is true if we can show that: 3149 1 < n /\ (!j. 1 < j ==> (ROOT j n) ** j <> n) <=> 3150 1 < n /\ (!j. 1 < j /\ j <= ulog n ==> (ROOT j n) ** j <> n) 3151 That is, to show that: 3152 1 < n /\ 1 < j /\ (!j. 1 < j /\ j <= ulog n ==> ROOT j n ** j <> n) ==> (ROOT j n) ** j <> n 3153 By contradiction, suppose (ROOT j n) ** j = n. 3154 Let m = ROOT j n. 3155 Then m ** j = n by above 3156 Thus perfect_power n m by perfect_power_def 3157 ==> ?k. k <= LOG2 n /\ n = m ** k by perfect_power_bound_LOG2 3158 But 1 < m by ONE_LT_EXP, 1 < n 3159 Thus j = k by EXP_BASE_INJECTIVE, 1 < m 3160 Note LOG2 n <= ulog n by ulog_LOG2, 0 < n 3161 Thus j <= ulog n by j = k, k <= LOG2 n, LOG2 n <= ulog n 3162 The implication gives m ** j <> n, a contradiction. 3163*) 3164val power_free_check_upto_ulog = store_thm( 3165 "power_free_check_upto_ulog", 3166 ``!n. power_free n <=> 1 < n /\ n power_free_upto (ulog n)``, 3167 rw[power_free_check_all, power_free_upto_def] >> 3168 rw[EQ_IMP_THM] >> 3169 spose_not_then strip_assume_tac >> 3170 qabbrev_tac `m = ROOT j n` >> 3171 `perfect_power n m` by metis_tac[perfect_power_def] >> 3172 `?k. k <= LOG2 n /\ (n = m ** k)` by fs[GSYM perfect_power_bound_LOG2] >> 3173 `1 < m` by metis_tac[ONE_LT_EXP] >> 3174 `j = k` by fs[EXP_BASE_INJECTIVE] >> 3175 `LOG2 n <= ulog n` by rw[ulog_LOG2] >> 3176 `j <= ulog n` by decide_tac >> 3177 metis_tac[]); 3178 3179(* More general proof of the above assertions *) 3180 3181(* Theorem: LOG2 n <= b ==> (power_free n <=> (1 < n /\ n power_free_upto b)) *) 3182(* Proof: 3183 If part: LOG2 n <= b /\ power_free n ==> 1 < n /\ n power_free_upto b 3184 (1) 1 < n, 3185 By contradiction, suppose n <= 1. 3186 Then n = 0, but power_free 0 = F by power_free_0 3187 or n = 1, but power_free 1 = F by power_free_1 3188 (2) n power_free_upto b, 3189 By power_free_upto_def, this is to show: 3190 1 < j /\ j <= b ==> ROOT j n ** j <> n 3191 By contradiction, suppose ROOT j n ** j = n. 3192 Then n = m ** j where m = ROOT j n, with j <> 1. 3193 This contradicts power_free n by power_free_def 3194 3195 Only-if part: 1 < n /\ LOG2 n <= b /\ n power_free_upto b ==> power_free n 3196 By contradiction, suppose ~(power_free n). 3197 Then ?e. n = m ** e with n = m ==> e <> 1 by power_free_def 3198 ==> perfect_power n m by perfect_power_def 3199 Thus ?k. k <= LOG2 n /\ (n = m ** k) by perfect_power_bound_LOG2, 0 < n 3200 Now k <> 0 by EXP_0, n <> 1 3201 so m = ROOT k n by ROOT_FROM_POWER, k <> 0 3202 3203 Claim: k <> 1 3204 Proof: Note m <> 0 by ROOT_EQ_0, n <> 0 3205 and m <> 1 by EXP_1, k <> 0, n <> 1 3206 ==> 1 < m by m <> 0, m <> 1 3207 Thus n = m ** e = m ** k ==> k = e by EXP_BASE_INJECTIVE 3208 But e <> 1 3209 since e = 1 ==> n <> m, by n = m ==> e <> 1 3210 yet n = m ** 1 ==> n = m by EXP_1 3211 Since k = e, k <> 1. 3212 3213 Therefore 1 < k by k <> 0, k <> 1 3214 and k <= LOG2 n /\ LOG2 n <= b ==> k <= b by arithmetic 3215 With 1 < k /\ k <= b /\ m = ROOT k n /\ m ** k = n, 3216 These will give a contradiction by power_free_upto_def 3217*) 3218val power_free_check_upto = store_thm( 3219 "power_free_check_upto", 3220 ``!n b. LOG2 n <= b ==> (power_free n <=> (1 < n /\ n power_free_upto b))``, 3221 rw[EQ_IMP_THM] >| [ 3222 spose_not_then strip_assume_tac >> 3223 `(n = 0) \/ (n = 1)` by decide_tac >- 3224 fs[power_free_0] >> 3225 fs[power_free_1], 3226 rw[power_free_upto_def] >> 3227 spose_not_then strip_assume_tac >> 3228 `j <> 1` by decide_tac >> 3229 metis_tac[power_free_def], 3230 simp[power_free_def] >> 3231 spose_not_then strip_assume_tac >> 3232 `perfect_power n m` by metis_tac[perfect_power_def] >> 3233 `0 < n /\ n <> 1` by decide_tac >> 3234 `?k. k <= LOG2 n /\ (n = m ** k)` by rw[GSYM perfect_power_bound_LOG2] >> 3235 `k <> 0` by metis_tac[EXP_0] >> 3236 `m = ROOT k n` by rw[ROOT_FROM_POWER] >> 3237 `k <> 1` by 3238 (`m <> 0` by rw[ROOT_EQ_0] >> 3239 `m <> 1 /\ e <> 1` by metis_tac[EXP_1] >> 3240 `1 < m` by decide_tac >> 3241 metis_tac[EXP_BASE_INJECTIVE]) >> 3242 `1 < k` by decide_tac >> 3243 `k <= b` by decide_tac >> 3244 metis_tac[power_free_upto_def] 3245 ]); 3246 3247(* Theorem: power_free n <=> (1 < n /\ n power_free_upto LOG2 n) *) 3248(* Proof: by power_free_check_upto, LOG2 n <= LOG2 n *) 3249val power_free_check_upto_LOG2 = store_thm( 3250 "power_free_check_upto_LOG2", 3251 ``!n. power_free n <=> (1 < n /\ n power_free_upto LOG2 n)``, 3252 rw[power_free_check_upto]); 3253 3254(* Theorem: power_free n <=> (1 < n /\ n power_free_upto ulog n) *) 3255(* Proof: 3256 If n = 0, 3257 LHS = power_free 0 = F by power_free_0 3258 = RHS, as 1 < 0 = F 3259 If n <> 0, 3260 Then LOG2 n <= ulog n by ulog_LOG2, 0 < n 3261 The result follows by power_free_check_upto 3262*) 3263val power_free_check_upto_ulog = store_thm( 3264 "power_free_check_upto_ulog", 3265 ``!n. power_free n <=> (1 < n /\ n power_free_upto ulog n)``, 3266 rpt strip_tac >> 3267 Cases_on `n = 0` >- 3268 rw[power_free_0] >> 3269 rw[power_free_check_upto, ulog_LOG2]); 3270 3271(* Theorem: power_free 2 *) 3272(* Proof: 3273 power_free 2 3274 <=> 2 power_free_upto (LOG2 2) by power_free_check_upto_LOG2 3275 <=> 2 power_free_upto 1 by LOG2_2 3276 <=> T by power_free_upto_1 3277*) 3278val power_free_2 = store_thm( 3279 "power_free_2", 3280 ``power_free 2``, 3281 rw[power_free_check_upto_LOG2, power_free_upto_1]); 3282 3283(* Theorem: power_free 3 *) 3284(* Proof: 3285 Note 3 power_free_upto 1 by power_free_upto_1 3286 power_free 3 3287 <=> 3 power_free_upto (ulog 3) by power_free_check_upto_ulog 3288 <=> 3 power_free_upto 2 by evaluation 3289 <=> ROOT 2 3 ** 2 <> 3 by power_free_upto_suc, 0 < 1 3290 <=> T by evaluation 3291*) 3292val power_free_3 = store_thm( 3293 "power_free_3", 3294 ``power_free 3``, 3295 `3 power_free_upto 1` by rw[power_free_upto_1] >> 3296 `ulog 3 = 2` by EVAL_TAC >> 3297 `ROOT 2 3 ** 2 <> 3` by EVAL_TAC >> 3298 `power_free 3 <=> 3 power_free_upto 2` by rw[power_free_check_upto_ulog] >> 3299 metis_tac[power_free_upto_suc, DECIDE``0 < 1 /\ (1 + 1 = 2)``]); 3300 3301(* Define a power free test, based on (ulog n), for computation. *) 3302val power_free_test_def = Define` 3303 power_free_test n <=>(1 < n /\ n power_free_upto (ulog n)) 3304`; 3305 3306(* Theorem: power_free_test n = power_free n *) 3307(* Proof: by power_free_test_def, power_free_check_upto_ulog *) 3308val power_free_test_eqn = store_thm( 3309 "power_free_test_eqn", 3310 ``!n. power_free_test n = power_free n``, 3311 rw[power_free_test_def, power_free_check_upto_ulog]); 3312 3313(* Theorem: power_free n <=> 3314 (1 < n /\ !j. 1 < j /\ j <= (LOG2 n) ==> ROOT j n ** j <> n) *) 3315(* Proof: by power_free_check_upto_ulog, power_free_upto_def *) 3316val power_free_test_upto_LOG2 = store_thm( 3317 "power_free_test_upto_LOG2", 3318 ``!n. power_free n <=> 3319 (1 < n /\ !j. 1 < j /\ j <= (LOG2 n) ==> ROOT j n ** j <> n)``, 3320 rw[power_free_check_upto_LOG2, power_free_upto_def]); 3321 3322(* Theorem: power_free n <=> 3323 (1 < n /\ !j. 1 < j /\ j <= (ulog n) ==> ROOT j n ** j <> n) *) 3324(* Proof: by power_free_check_upto_ulog, power_free_upto_def *) 3325val power_free_test_upto_ulog = store_thm( 3326 "power_free_test_upto_ulog", 3327 ``!n. power_free n <=> 3328 (1 < n /\ !j. 1 < j /\ j <= (ulog n) ==> ROOT j n ** j <> n)``, 3329 rw[power_free_check_upto_ulog, power_free_upto_def]); 3330 3331(* ------------------------------------------------------------------------- *) 3332(* Another Characterisation of Power Free *) 3333(* ------------------------------------------------------------------------- *) 3334 3335(* Define power index of n, the highest index of n in power form by descending from k *) 3336val power_index_def = Define ` 3337 power_index n k <=> 3338 if k <= 1 then 1 3339 else if (ROOT k n) ** k = n then k 3340 else power_index n (k - 1) 3341`; 3342 3343(* Theorem: power_index n 0 = 1 *) 3344(* Proof: by power_index_def *) 3345val power_index_0 = store_thm( 3346 "power_index_0", 3347 ``!n. power_index n 0 = 1``, 3348 rw[Once power_index_def]); 3349 3350(* Theorem: power_index n 1 = 1 *) 3351(* Proof: by power_index_def *) 3352val power_index_1 = store_thm( 3353 "power_index_1", 3354 ``!n. power_index n 1 = 1``, 3355 rw[Once power_index_def]); 3356 3357(* Theorem: (ROOT (power_index n k) n) ** (power_index n k) = n *) 3358(* Proof: 3359 By induction on k. 3360 Base: ROOT (power_index n 0) n ** power_index n 0 = n 3361 ROOT (power_index n 0) n ** power_index n 0 3362 = (ROOT 1 n) ** 1 by power_index_0 3363 = n ** 1 by ROOT_1 3364 = n by EXP_1 3365 Step: ROOT (power_index n k) n ** power_index n k = n ==> 3366 ROOT (power_index n (SUC k)) n ** power_index n (SUC k) = n 3367 If k = 0, 3368 ROOT (power_index n (SUC 0)) n ** power_index n (SUC 0) 3369 = ROOT (power_index n 1) n ** power_index n 1 by ONE 3370 = (ROOT 1 n) ** 1 by power_index_1 3371 = n ** 1 by ROOT_1 3372 = n by EXP_1 3373 If k <> 0, 3374 Then ~(SUC k <= 1) by 0 < k 3375 If ROOT (SUC k) n ** SUC k = n, 3376 Then power_index n (SUC k) = SUC k by power_index_def 3377 so ROOT (power_index n (SUC k)) n ** power_index n (SUC k) 3378 = ROOT (SUC k) n ** SUC k by above 3379 = n by condition 3380 If ROOT (SUC k) n ** SUC k <> n, 3381 Then power_index n (SUC k) = power_index n k by power_index_def 3382 so ROOT (power_index n (SUC k)) n ** power_index n (SUC k) 3383 = ROOT (power_index n k) n ** power_index n k by above 3384 = n by induction hypothesis 3385*) 3386val power_index_eqn = store_thm( 3387 "power_index_eqn", 3388 ``!n k. (ROOT (power_index n k) n) ** (power_index n k) = n``, 3389 rpt strip_tac >> 3390 Induct_on `k` >- 3391 rw[power_index_0] >> 3392 Cases_on `k = 0` >- 3393 rw[power_index_1] >> 3394 `~(SUC k <= 1)` by decide_tac >> 3395 rw_tac std_ss[Once power_index_def] >- 3396 rw[Once power_index_def] >> 3397 `power_index n (SUC k) = power_index n k` by rw[Once power_index_def] >> 3398 rw[]); 3399 3400(* Theorem: perfect_power n (ROOT (power_index n k) n) *) 3401(* Proof: 3402 Let m = ROOT (power_index n k) n. 3403 By perfect_power_def, this is to show: 3404 ?e. n = m ** e 3405 Take e = power_index n k. 3406 m ** e 3407 = (ROOT (power_index n k) n) ** (power_index n k) by root_compute_eqn 3408 = n by power_index_eqn 3409*) 3410val power_index_root = store_thm( 3411 "power_index_root", 3412 ``!n k. perfect_power n (ROOT (power_index n k) n)``, 3413 metis_tac[perfect_power_def, power_index_eqn]); 3414 3415(* Theorem: power_index 1 k = if k = 0 then 1 else k *) 3416(* Proof: 3417 If k = 0, 3418 power_index 1 0 = 1 by power_index_0 3419 If k <> 0, then 0 < k. 3420 If k = 1, 3421 Then power_index 1 1 = 1 = k by power_index_1 3422 If k <> 1, 1 < k. 3423 Note ROOT k 1 = 1 by ROOT_OF_1, 0 < k. 3424 so power_index 1 k = k by power_index_def 3425*) 3426val power_index_of_1 = store_thm( 3427 "power_index_of_1", 3428 ``!k. power_index 1 k = if k = 0 then 1 else k``, 3429 rw[Once power_index_def]); 3430 3431(* Theorem: 0 < k /\ ((ROOT k n) ** k = n) ==> (power_index n k = k) *) 3432(* Proof: 3433 If k = 1, 3434 True since power_index n 1 = 1 by power_index_1 3435 If k <> 1, then 1 < k by 0 < k 3436 True by power_index_def 3437*) 3438val power_index_exact_root = store_thm( 3439 "power_index_exact_root", 3440 ``!n k. 0 < k /\ ((ROOT k n) ** k = n) ==> (power_index n k = k)``, 3441 rpt strip_tac >> 3442 Cases_on `k = 1` >- 3443 rw[power_index_1] >> 3444 `1 < k` by decide_tac >> 3445 rw[Once power_index_def]); 3446 3447(* Theorem: (ROOT k n) ** k <> n ==> (power_index n k = power_index n (k - 1)) *) 3448(* Proof: 3449 If k = 0, 3450 Then k = k - 1 by k = 0 3451 Thus true trivially. 3452 If k = 1, 3453 Note power_index n 1 = 1 by power_index_1 3454 and power_index n 0 = 1 by power_index_0 3455 Thus true. 3456 If k <> 0 /\ k <> 1, then 1 < k by arithmetic 3457 True by power_index_def 3458*) 3459val power_index_not_exact_root = store_thm( 3460 "power_index_not_exact_root", 3461 ``!n k. (ROOT k n) ** k <> n ==> (power_index n k = power_index n (k - 1))``, 3462 rpt strip_tac >> 3463 Cases_on `k = 0` >| [ 3464 `k = k - 1` by decide_tac >> 3465 rw[], 3466 Cases_on `k = 1` >- 3467 rw[power_index_0, power_index_1] >> 3468 `1 < k` by decide_tac >> 3469 rw[Once power_index_def] 3470 ]); 3471 3472(* Theorem: k <= m /\ (!j. k < j /\ j <= m ==> (ROOT j n) ** j <> n) ==> (power_index n m = power_index n k) *) 3473(* Proof: 3474 By induction on (m - k). 3475 Base: k <= m /\ 0 = m - k ==> power_index n m = power_index n k 3476 Note m <= k by 0 = m - k 3477 so m = k by k <= m 3478 Thus true trivially. 3479 Step: !m'. v = m' - k /\ k <= m' /\ ... ==> power_index n m' = power_index n k ==> 3480 SUC v = m - k ==> power_index n m = power_index n k 3481 If m = k, true trivially. 3482 If m <> k, then k < m. 3483 Thus k <= (m - 1), and v = (m - 1) - k. 3484 Note ROOT m n ** m <> n by j = m in implication 3485 Thus power_index n m 3486 = power_index n (m - 1) by power_index_not_exact_root 3487 = power_index n k by induction hypothesis, m' = m - 1. 3488*) 3489val power_index_no_exact_roots = store_thm( 3490 "power_index_no_exact_roots", 3491 ``!m n k. k <= m /\ (!j. k < j /\ j <= m ==> (ROOT j n) ** j <> n) ==> (power_index n m = power_index n k)``, 3492 rpt strip_tac >> 3493 Induct_on `m - k` >| [ 3494 rpt strip_tac >> 3495 `m = k` by decide_tac >> 3496 rw[], 3497 rpt strip_tac >> 3498 Cases_on `m = k` >- 3499 rw[] >> 3500 `ROOT m n ** m <> n` by rw[] >> 3501 `k <= m - 1` by decide_tac >> 3502 `power_index n (m - 1) = power_index n k` by rw[] >> 3503 rw[power_index_not_exact_root] 3504 ]); 3505 3506(* The theorem power_index_equal requires a detective-style proof, based on these lemma. *) 3507 3508(* Theorem: k <= m /\ ((ROOT k n) ** k = n) ==> k <= power_index n m *) 3509(* Proof: 3510 If k = 0, 3511 Then n = 1 by EXP 3512 If m = 0, 3513 Then power_index 1 0 = 1 by power_index_of_1 3514 But k <= 0, so k = 0 by arithmetic 3515 Hence k <= power_index n m 3516 If m <> 0, 3517 Then power_index 1 m = m by power_index_of_1 3518 Hence k <= power_index 1 m = m by given 3519 3520 If k <> 0, then 0 < k. 3521 Let s = {j | j <= m /\ ((ROOT j n) ** j = n)} 3522 Then s SUBSET (count (SUC m)) by SUBSET_DEF 3523 ==> FINITE s by SUBSET_FINITE, FINITE_COUNT 3524 Note k IN s by given 3525 ==> s <> {} by MEMBER_NOT_EMPTY 3526 Let t = MAX_SET s. 3527 3528 Claim: !x. t < x /\ x <= m ==> (ROOT x n) ** x <> n 3529 Proof: By contradiction, suppose (ROOT x n) ** x = n 3530 Then x IN s, so x <= t by MAX_SET_PROPERTY 3531 This contradicts t < x. 3532 3533 Note t IN s by MAX_SET_IN_SET 3534 so t <= m /\ (ROOT t n) ** t = n by above 3535 Thus power_index n m = power_index n t by power_index_no_exact_roots, t <= m 3536 and power_index n t = t by power_index_exact_root, (ROOT t n) ** t = n 3537 But k <= t by MAX_SET_PROPERTY 3538 Thus k <= t = power_index n m 3539*) 3540val power_index_lower = store_thm( 3541 "power_index_lower", 3542 ``!m n k. k <= m /\ ((ROOT k n) ** k = n) ==> k <= power_index n m``, 3543 rpt strip_tac >> 3544 Cases_on `k = 0` >| [ 3545 `n = 1` by fs[EXP] >> 3546 rw[power_index_of_1], 3547 `0 < k` by decide_tac >> 3548 qabbrev_tac `s = {j | j <= m /\ ((ROOT j n) ** j = n)}` >> 3549 `!j. j IN s <=> j <= m /\ ((ROOT j n) ** j = n)` by rw[Abbr`s`] >> 3550 `s SUBSET (count (SUC m))` by rw[SUBSET_DEF] >> 3551 `FINITE s` by metis_tac[SUBSET_FINITE, FINITE_COUNT] >> 3552 `k IN s` by rw[] >> 3553 `s <> {}` by metis_tac[MEMBER_NOT_EMPTY] >> 3554 qabbrev_tac `t = MAX_SET s` >> 3555 `!x. t < x /\ x <= m ==> (ROOT x n) ** x <> n` by 3556 (spose_not_then strip_assume_tac >> 3557 `x IN s` by rw[] >> 3558 `x <= t` by rw[MAX_SET_PROPERTY, Abbr`t`] >> 3559 decide_tac) >> 3560 `t IN s` by rw[MAX_SET_IN_SET, Abbr`t`] >> 3561 `power_index n m = power_index n t` by metis_tac[power_index_no_exact_roots] >> 3562 `k <= t` by rw[MAX_SET_PROPERTY, Abbr`t`] >> 3563 `(ROOT t n) ** t = n` by metis_tac[] >> 3564 `power_index n t = t` by rw[power_index_exact_root] >> 3565 decide_tac 3566 ]); 3567 3568(* Theorem: 0 < power_index n k *) 3569(* Proof: 3570 If k = 0, 3571 True since power_index n 0 = 1 by power_index_0 3572 If k <> 0, 3573 Then 1 <= k. 3574 Note (ROOT 1 n) ** 1 = n ** 1 = n by ROOT_1, EXP_1 3575 Thus 1 <= power_index n k by power_index_lower 3576 or 0 < power_index n k 3577*) 3578val power_index_pos = store_thm( 3579 "power_index_pos", 3580 ``!n k. 0 < power_index n k``, 3581 rpt strip_tac >> 3582 Cases_on `k = 0` >- 3583 rw[power_index_0] >> 3584 `1 <= power_index n k` by rw[power_index_lower, EXP_1] >> 3585 decide_tac); 3586 3587(* Theorem: 0 < k ==> power_index n k <= k *) 3588(* Proof: 3589 By induction on k. 3590 Base: 0 < 0 ==> power_index n 0 <= 0 3591 True by 0 < 0 = F. 3592 Step: 0 < k ==> power_index n k <= k ==> 3593 0 < SUC k ==> power_index n (SUC k) <= SUC k 3594 If k = 0, 3595 Then SUC k = 1 by ONE 3596 True since power_index n 1 = 1 by power_index_1 3597 If k <> 0, 3598 Let m = SUC k, or k = m - 1. 3599 Then 1 < m by arithmetic 3600 If (ROOT m n) ** m = n, 3601 Then power_index n m 3602 = m <= m by power_index_exact_root 3603 If (ROOT m n) ** m <> n, 3604 Then power_index n m 3605 = power_index n (m - 1) by power_index_not_exact_root 3606 = power_index n k by m - 1 = k 3607 <= k by induction hypothesis 3608 But k < SUC k = m by LESS_SUC 3609 Thus power_index n m < m by LESS_EQ_LESS_TRANS 3610 or power_index n m <= m by LESS_IMP_LESS_OR_EQ 3611*) 3612val power_index_upper = store_thm( 3613 "power_index_upper", 3614 ``!n k. 0 < k ==> power_index n k <= k``, 3615 strip_tac >> 3616 Induct >- 3617 rw[] >> 3618 rpt strip_tac >> 3619 Cases_on `k = 0` >- 3620 rw[power_index_1] >> 3621 `1 < SUC k` by decide_tac >> 3622 qabbrev_tac `m = SUC k` >> 3623 Cases_on `(ROOT m n) ** m = n` >- 3624 rw[power_index_exact_root] >> 3625 rw[power_index_not_exact_root, Abbr`m`]); 3626 3627(* Theorem: 0 < k /\ k <= m ==> 3628 ((power_index n m = power_index n k) <=> (!j. k < j /\ j <= m ==> (ROOT j n) ** j <> n)) *) 3629(* Proof: 3630 If part: 0 < k /\ k <= m /\ power_index n m = power_index n k /\ k < j /\ j <= m ==> ROOT j n ** j <> n 3631 By contradiction, suppose ROOT j n ** j = n. 3632 Then j <= power_index n m by power_index_lower 3633 But power_index n k <= k by power_index_upper, 0 < k 3634 Thus j <= k by LESS_EQ_TRANS 3635 This contradicts k < j. 3636 Only-if part: 0 < k /\ k <= m /\ !j. k < j /\ j <= m ==> ROOT j n ** j <> n ==> 3637 power_index n m = power_index n k 3638 True by power_index_no_exact_roots 3639*) 3640val power_index_equal = store_thm( 3641 "power_index_equal", 3642 ``!m n k. 0 < k /\ k <= m ==> 3643 ((power_index n m = power_index n k) <=> (!j. k < j /\ j <= m ==> (ROOT j n) ** j <> n))``, 3644 rpt strip_tac >> 3645 rw[EQ_IMP_THM] >| [ 3646 spose_not_then strip_assume_tac >> 3647 `j <= power_index n m` by rw[power_index_lower] >> 3648 `power_index n k <= k` by rw[power_index_upper] >> 3649 decide_tac, 3650 rw[power_index_no_exact_roots] 3651 ]); 3652 3653(* Theorem: (power_index n m = k) ==> !j. k < j /\ j <= m ==> (ROOT j n) ** j <> n *) 3654(* Proof: 3655 By contradiction, suppose k < j /\ j <= m /\ (ROOT j n) ** j = n. 3656 Then j <= power_index n m by power_index_lower 3657 This contradicts power_index n m = k < j by given 3658*) 3659val power_index_property = store_thm( 3660 "power_index_property", 3661 ``!m n k. (power_index n m = k) ==> !j. k < j /\ j <= m ==> (ROOT j n) ** j <> n``, 3662 spose_not_then strip_assume_tac >> 3663 `j <= power_index n m` by rw[power_index_lower] >> 3664 decide_tac); 3665 3666(* Theorem: power_free n <=> (1 < n) /\ (power_index n (LOG2 n) = 1) *) 3667(* Proof: 3668 By power_free_check_upto_LOG2, power_free_upto_def, this is to show: 3669 1 < n /\ (!j. 1 < j /\ j <= LOG2 n ==> ROOT j n ** j <> n) <=> 3670 1 < n /\ (power_index n (LOG2 n) = 1) 3671 If part: 3672 Note 0 < LOG2 n by LOG2_POS, 1 < n 3673 power_index n (LOG2 n) 3674 = power_index n 1 by power_index_no_exact_roots, 1 <= LOG2 n 3675 = 1 by power_index_1 3676 Only-if part, true by power_index_property 3677*) 3678val power_free_by_power_index_LOG2 = store_thm( 3679 "power_free_by_power_index_LOG2", 3680 ``!n. power_free n <=> (1 < n) /\ (power_index n (LOG2 n) = 1)``, 3681 rw[power_free_check_upto_LOG2, power_free_upto_def] >> 3682 rw[EQ_IMP_THM] >| [ 3683 `0 < LOG2 n` by rw[] >> 3684 `1 <= LOG2 n` by decide_tac >> 3685 `power_index n (LOG2 n) = power_index n 1` by rw[power_index_no_exact_roots] >> 3686 rw[power_index_1], 3687 metis_tac[power_index_property] 3688 ]); 3689 3690(* Theorem: power_free n <=> (1 < n) /\ (power_index n (ulog n) = 1) *) 3691(* Proof: 3692 By power_free_check_upto_ulog, power_free_upto_def, this is to show: 3693 1 < n /\ (!j. 1 < j /\ j <= ulog n ==> ROOT j n ** j <> n) <=> 3694 1 < n /\ (power_index n (ulog n) = 1) 3695 If part: 3696 Note 0 < ulog n by ulog_POS, 1 < n 3697 power_index n (ulog n) 3698 = power_index n 1 by power_index_no_exact_roots, 1 <= ulog n 3699 = 1 by power_index_1 3700 Only-if part, true by power_index_property 3701*) 3702val power_free_by_power_index_ulog = store_thm( 3703 "power_free_by_power_index_ulog", 3704 ``!n. power_free n <=> (1 < n) /\ (power_index n (ulog n) = 1)``, 3705 rw[power_free_check_upto_ulog, power_free_upto_def] >> 3706 rw[EQ_IMP_THM] >| [ 3707 `0 < ulog n` by rw[] >> 3708 `1 <= ulog n` by decide_tac >> 3709 `power_index n (ulog n) = power_index n 1` by rw[power_index_no_exact_roots] >> 3710 rw[power_index_1], 3711 metis_tac[power_index_property] 3712 ]); 3713 3714(* ------------------------------------------------------------------------- *) 3715 3716(* export theory at end *) 3717val _ = export_theory(); 3718 3719(*===========================================================================*) 3720