1(* ------------------------------------------------------------------------- *) 2(* AKS parameter from Count Monad *) 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 "countParam"; 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(* val _ = load "countPowerTheory"; *) 24open countMonadTheory countMacroTheory; 25open countBasicTheory countPowerTheory; 26 27(* val _ = load "countOrderTheory"; *) 28open countOrderTheory; 29 30open bitsizeTheory complexityTheory; 31open loopIncreaseTheory loopDecreaseTheory; 32 33(* Get dependent theories in lib *) 34(* (* val _ = load "helperNumTheory"; -- in monoidTheory *) *) 35(* (* val _ = load "helperSetTheory"; -- in monoidTheory *) *) 36open helperNumTheory helperSetTheory helperListTheory; 37open helperFunctionTheory; 38 39(* (* val _ = load "dividesTheory"; -- in helperNumTheory *) *) 40(* (* val _ = load "gcdTheory"; -- in helperNumTheory *) *) 41open pred_setTheory listTheory arithmeticTheory; 42open dividesTheory gcdTheory; 43 44(* (* val _ = load "logPowerTheory"; *) *) 45open logrootTheory logPowerTheory; 46 47(* val _ = load "computeParamTheory"; *) 48open computeParamTheory; (* for param_search_result *) 49 50(* (* val _ = load "monadsyntax"; *) *) 51open monadsyntax; 52open pairTheory optionTheory; 53open listRangeTheory; 54 55(* val _ = load "ringInstancesTheory"; *) 56open ringInstancesTheory; (* for ZN order *) 57 58val _ = monadsyntax.enable_monadsyntax(); 59val _ = monadsyntax.enable_monad "Count"; 60 61 62(* ------------------------------------------------------------------------- *) 63(* AKS parameter with Count Monad Documentation *) 64(* ------------------------------------------------------------------------- *) 65(* Data type: 66*) 67(* Overloading: 68*) 69(* Definitions and Theorems (# are exported): 70 71 Helper: 72 73 AKS parameter search in Monadic style: 74 param_seekM_def |- !n m k c. param_seekM m c n k = 75 do 76 k0 <- zeroM k; 77 if k0 then unit bad 78 else 79 do 80 b0 <- leqM c k; 81 if b0 then unit bad 82 else 83 do 84 r <- modM n k; 85 r0 <- zeroM r; 86 if r0 then unit (nice k) 87 else 88 do 89 z <- ordzM k n; 90 b1 <- leqM m z; 91 if b1 then unit (good k) 92 else do j <- incM k; param_seekM m c n j od 93 od 94 od 95 od 96 od 97 paramM_def |- !n. paramM n = 98 do 99 m0 <- ulogM n; 100 b0 <- zeroM m0; 101 b1 <- oneM m0; 102 if b0 \/ b1 then unit (nice n) 103 else 104 do 105 m <- sqM m0; 106 v0 <- expM m0 5; 107 d <- halfM v0; 108 c <- addM d 2; 109 param_seekM m c n 2 110 od 111 od 112# param_seekM_value |- !m c n k. valueOf (param_seekM m c n k) = 113 if k = 0 then bad else param_seek m c n k 114# paramM_value |- !n. valueOf (paramM n) = param n 115 paramM_value_alt |- !n. valueOf (paramM n) = aks_param n 116 117 param_seekM_steps_thm 118 |- !m c n k. stepsOf (param_seekM m c n k) = size k + 119 if k = 0 then 0 120 else size (MAX c k) + size (c - k) + if c <= k then 0 121 else size n * size k + size (n MOD k) + if n MOD k = 0 then 0 122 else stepsOf (ordzM k n) + size (MAX m (ordz k n)) + 123 size (m - ordz k n) + if m <= ordz k n then 0 124 else size k + stepsOf (param_seekM m c n (k + 1)) 125 paramM_steps_thm |- !n. stepsOf (paramM n) = 126 stepsOf (ulogM n) + TWICE (size (ulog n)) + 127 if n <= 2 then 0 128 else size (ulog n) ** 2 + TWICE (size (ulog n ** 5)) + 129 size (MAX (HALF (ulog n ** 5)) 2) + stepsOf (expM (ulog n) 5) + 130 stepsOf (param_seekM (SQ (ulog n)) (2 + HALF (ulog n ** 5)) n 2) 131 param_seekM_steps_by_inc_loop 132 |- !m c n. (let quit k = if k = 0 then 1 else 1 + TWICE (size k) ; 133 body k = size k + 134 if k = 0 then 0 135 else size c + size (c - k) + size n * size k + 136 size (n MOD k) + if n MOD k = 0 then 0 137 else stepsOf (ordzM k n) + size (MAX m (ordz k n)) + 138 size (m - ordz k n) + if m <= ordz k n then 0 else size k ; 139 exit k = ((k = 0) \/ (n MOD k = 0) \/ m <= ordz k n) 140 in !k. stepsOf (param_seekM m c n k) = 141 if c <= k then quit k else body k + 142 if exit k then 0 else stepsOf (param_seekM m c n (k + 1))) 143 param_seekM_body_upper 144 |- !m c n. (let body k = size k + 145 if k = 0 then 0 146 else size c + size (c - k) + size n * size k + 147 size (n MOD k) + if n MOD k = 0 then 0 148 else stepsOf (ordzM k n) + size (MAX m (ordz k n)) + 149 size (m - ordz k n) + if m <= ordz k n then 0 else size k 150 in !k. body k <= 151 TWICE (size m) + TWICE (size c) + 4 * size k + 152 size n * size k + 27 * k * size n * size k ** 7) 153 param_seekM_body_bound 154 |- !m c n. (let body k = size k + 155 if k = 0 then 0 156 else size c + size (c - k) + size n * size k + 157 size (n MOD k) + if n MOD k = 0 then 0 158 else stepsOf (ordzM k n) + size (MAX m (ordz k n)) + 159 size (m - ordz k n) + if m <= ordz k n then 0 else size k 160 in !k. body k <= 161 36 * MAX 1 k * size m * size c * size n * size k ** 7) 162 param_seekM_steps_upper 163 |- !m c n k. stepsOf (param_seekM m c n k) <= 164 1 + TWICE (size (MAX c k)) + 165 36 * (c - k) * c * size m * size n * size c ** 8 166 param_seekM_steps_bound 167 |- !m c n k. stepsOf (param_seekM m c n k) <= 168 39 * MAX 1 (c - k) * MAX 1 c * size (MAX c k) * size m * size n * 169 size c ** 7 170 paramM_steps_upper |- !n. stepsOf (paramM n) <= 171 19 * size n + 16904 * size n ** 2 + 1348963434 * size n ** 20 172 paramM_steps_bound |- !n. stepsOf (paramM n) <= 1348980357 * size n ** 20 173 paramM_steps_O_poly |- stepsOf o paramM IN O_poly 20 174 paramM_steps_big_O |- stepsOf o paramM IN big_O (\n. ulog n ** 20) 175 paramM_thm |- !n. (valueOf (paramM n) = param n) /\ 176 stepsOf o paramM IN big_O (\n. ulog n ** 20) 177*) 178 179(* Eliminate parenthesis around equality *) 180val _ = ParseExtras.tight_equality(); 181 182(* ------------------------------------------------------------------------- *) 183(* Helper Theorems *) 184(* ------------------------------------------------------------------------- *) 185 186(* for EVAL IFm *) 187val _ = computeLib.set_skip computeLib.the_compset ``ifM`` (SOME 1); 188(* EVAL IFm must be in current script, e.g. EVAL ``expn 1 2 3``; *) 189 190(* ------------------------------------------------------------------------- *) 191(* AKS parameter search in Monadic style *) 192(* ------------------------------------------------------------------------- *) 193(* Pseudocode: 194 Given n, and a maximum m, and a count k to cutoff c, 195 find a modulus k such that (ordz k n >= m), which is good, 196 or a value k that divides n, which is nice, 197 or k exceeds cutoff c and still no nice or good, then bad. 198 199 if m = 0 or m = 1, nice n // nice n 200 if k = 0, bad // exclude k = 0 201 loop: 202 if c <= k, return bad // unreachable 203 r <- n MOD k // compute remainder of n divided by k 204 if r = 0, return nice k // found a factor k of n 205 z <- ordz k n // compute order of n in modulus k 206 if m <= z, return good k // found a good modulus k 207 k <- k + 1 208 goto loop 209 210 Note: k is at least 2 in order for n MOD k and ordz k n to be reasonable. 211 Note: k needs to be increasing to guarantee the coprime feature when not dividing. 212*) 213 214(* 215> param_seek_def; 216val it = |- !n m k c. 217 param_seek m c n k = 218 if c <= k then bad 219 else if n MOD k = 0 then nice k 220 else if m <= ordz k n then good k 221 else param_seek m c n (k + 1): thm 222*) 223(* Although param_seek_def does not check k = 0, as the caller ensures k = 2, 224param_seekM_def has to check k = 0, in order that complexity analysis can be 225carried out independently on (param_seek m c n k), for all values of k. 226This is particular true when going deeper into !k. body k <= cover k, and MONO cover. 227If (param_seek m c n 0) is undefined, it is difficult to bound (body k), 228unless we develop a theory of partial cover and partial MONO, to derive partial bounds. 229*) 230 231(* Define the parameter seek loop *) 232val param_seekM_def = tDefine "param_seekM" ` 233 param_seekM m c n k = 234 do 235 k0 <- zeroM k; 236 if k0 then return bad 237 else do 238 b0 <- leqM c k; 239 if b0 then return bad 240 else do (* check if k is a factor of n *) 241 r <- modM n k; 242 r0 <- zeroM r; 243 if r0 then return (nice k) 244 else do (* check if ordz k n is big enough *) 245 z <- ordzM k n; 246 b1 <- leqM m z; 247 if b1 then return (good k) 248 else do 249 j <- incM k; 250 param_seekM m c n j; 251 od 252 od 253 od 254 od 255 od 256`(WF_REL_TAC `measure (\(m,c,n,k). c - k)` >> simp[]); 257 258(* 259> EVAL ``param_seekM 25 31 31 2``; 260val it = |- param_seekM 31 25 31 31 = (good 29,Count 38712): thm 261 262Step 2: Use 31 to find a suitable k to make the modulus x^k - 1 263AKS parameter search: n=31, m=25 264AKS parameter search: max=1562 265AKS parameter k=29 266*) 267 268(* 269> param_def; 270val it = |- !n. param n = 271 (let m = SQ (ulog n) ; 272 c = 2 + HALF (ulog n ** 5) 273 in if n <= 2 then nice n else param_seek m c n 2): thm 274*) 275 276(* To compute the AKS parameter k *) 277val paramM_def = Define` 278 paramM n = 279 do 280 m0 <- ulogM n; 281 b0 <- zeroM m0; 282 b1 <- oneM m0; 283 if b0 \/ b1 then unit (nice n) (* m0 <= 1 means n <= 2 *) 284 else do 285 m <- sqM m0; (* make SQ (ulog n) *) 286 v0 <- expM m0 5; 287 d <- halfM v0; (* make HALF (ulog n ** 5) *) 288 c <- addM d 2; (* make 2 + HALF (ulog n ** 5) *) 289 param_seekM m c n 2; 290 od 291 od 292`; 293 294(* 295> EVAL ``paramM 31``; 296val it = |- paramM 31 = (good 29,Count 39428): thm 297*) 298 299 300(* Theorem: valueOf (param_seekM m c n k) = param_seek m c n k *) 301(* Proof: by param_seekM_def, param_seek_def *) 302val param_seekM_value = store_thm( 303 "param_seekM_value[simp]", 304 ``!m c n k. valueOf (param_seekM m c n k) = 305 if k = 0 then bad else param_seek m c n k``, 306 ho_match_mp_tac (theorem "param_seekM_ind") >> 307 rpt strip_tac >> 308 (rw[Once param_seekM_def, Once param_seek_def] >> fs[])); 309 310(* Theorem: valueOf (paramM n) = param n *) 311(* Proof: by paramM_def, param_alt *) 312val paramM_value = store_thm( 313 "paramM_value[simp]", 314 ``!n. valueOf (paramM n) = param n``, 315 (rw[paramM_def, param_alt] >> fs[])); 316 317(* Theorem: valueOf (paramM n) = aks_param n *) 318(* Proof: by paramM_value, param_eqn. *) 319val paramM_value_alt = store_thm( 320 "paramM_value_alt", 321 ``!n. valueOf (paramM n) = aks_param n``, 322 rw[param_eqn]); 323 324(* This is the most important result for correctness! *) 325 326 327(* Theorem: stepsOf (param_seekM m c n k) = size k + 328 if k = 0 then 0 329 else size (MAX c k) + size (c - k) + if c <= k then 0 330 else size n * size k + size (n MOD k) + if n MOD k = 0 then 0 331 else stepsOf (ordzM k n) + size (MAX m (ordz k n)) + size (m - ordz k n) + if (m <= ordz k n) then 0 332 else size k + stepsOf (param_seekM m c n (k + 1)) *) 333(* Proof: 334 stepsOf (param_seekM m c n k) 335 = stepsOf (zeroM k) + if k = 0 then 0 336 else stepsOf (leqM c k) + if c <= k then 0 337 else stepsOf (modM n k) + stepsOf (zeroM (n MOD k)) + if (n MOD k = 0) then 0 338 else stepsOf (ordzM k n) + stepsOf (leqM m (ordz k n)) + if (m <= ordz k n) then 0 339 else stepsOf (incM k) + stepsOf (param_seekM m c n (k + 1)) by param_seekM_def 340 = size k + if k = 0 then 0 341 else size (MAX c k) + size (c - k) + if c <= k then 0 by size_max 342 else size n * size k + size (n MOD k) + if n MOD k = 0 then 0 by modM_steps, 0 < k 343 else stepsOf (ordzM k n) + size (MAX m (ordz k n)) + size (m - ordz k n) + if (m <= ordz k n) then 0 344 else size k + stepsOf (param_seekM m c n (k + 1)) 345 = size k + if k = 0 then 0 346 else size (MAX c k) + size (c - k)) + if c <= k then 0 347 else size n * size k + size (n MOD k) + if n MOD k = 0 then 0 348 else stepsOf (ordzM k n) + size (MAX m (ordz k n)) + size (m - ordz k n) + if (m <= ordz k n) then 0 349 else size k + stepsOf (param_seekM m c n (k + 1)) 350*) 351val param_seekM_steps_thm = store_thm( 352 "param_seekM_steps_thm", 353 ``!m c n k. stepsOf (param_seekM m c n k) = size k + 354 if k = 0 then 0 355 else size (MAX c k) + size (c - k) + if c <= k then 0 356 else size n * size k + size (n MOD k) + if n MOD k = 0 then 0 357 else stepsOf (ordzM k n) + size (MAX m (ordz k n)) + size (m - ordz k n) + if (m <= ordz k n) then 0 358 else size k + stepsOf (param_seekM m c n (k + 1))``, 359 ho_match_mp_tac (theorem "param_seekM_ind") >> 360 rpt strip_tac >> 361 Cases_on `k = 0` >- 362 simp[Once param_seekM_def] >> 363 Cases_on `c <= k` >- 364 simp[Once param_seekM_def, size_max] >> 365 Cases_on `n MOD k = 0` >- 366 simp[Once param_seekM_def, size_max] >> 367 Cases_on `m <= ordz k n` >- 368 simp[Once param_seekM_def, size_max] >> 369 fs[Once param_seekM_def, size_max]); 370 371(* Theorem: stepsOf (paramM n) = 372 stepsOf (ulogM n) + 2 * size (ulog n) + 373 if (n <= 2) then 0 374 else (size (ulog n)) ** 2 + 2 * size ((ulog n) ** 5) + size (MAX (HALF ((ulog n) ** 5)) 2) + 375 stepsOf (expM (ulog n) 5) + 376 stepsOf (param_seekM (SQ (ulog n)) (2 + HALF ((ulog n) ** 5)) n 2) *) 377(* Proof: 378 stepsOf (paramM n) 379 = stepsOf (ulogM n) + 380 stepsOf (zeroM (ulog n)) + 381 stepsOf (oneM (ulog n)) + if (ulog n = 0 \/ ulog n = 1) then 0 382 else stepsOf (sqM (ulog n)) + 383 stepsOf (expM (ulog n) 5) + 384 stepsOf (halfM ((ulog n) ** 5)) + 385 stepsOf (addM (HALF ((ulog n) ** 5)) 2) + 386 stepsOf (param_seekM (SQ (ulog n)) (2 + HALF ((ulog n) ** 5)) n 2)) by paramM_def 387 = stepsOf (ulogM n) + 388 2 * size (ulog n) + 389 if (n <= 2) then 0 by ulog_eq_0, ulog_eq_1 390 else (size (ulog n)) ** 2 + 391 stepsOf (expM (ulog n) 5) + 2 * size ((ulog n) ** 5) + 392 size (MAX (HALF ((ulog n) ** 5)) 2) + 393 stepsOf (param_seekM (SQ (ulog n)) (2 + HALF ((ulog n) ** 5)) n 2) by size_max 394 = stepsOf (ulogM n) + 2 * size (ulog n) + 395 if (n <= 2) then 0 396 else (size (ulog n)) ** 2 + 2 * size ((ulog n) ** 5) + size (MAX (HALF ((ulog n) ** 5)) 2) + 397 stepsOf (expM (ulog n) 5) + 398 stepsOf (param_seekM (SQ (ulog n)) (2 + HALF ((ulog n) ** 5)) n 2) 399*) 400val paramM_steps_thm = store_thm( 401 "paramM_steps_thm", 402 ``!n. stepsOf (paramM n) = 403 stepsOf (ulogM n) + 2 * size (ulog n) + 404 if (n <= 2) then 0 405 else (size (ulog n)) ** 2 + 406 2 * size ((ulog n) ** 5) + size (MAX (HALF ((ulog n) ** 5)) 2) + 407 stepsOf (expM (ulog n) 5) + 408 stepsOf (param_seekM (SQ (ulog n)) (2 + HALF ((ulog n) ** 5)) n 2)``, 409 rw[paramM_def, ulog_eq_0, ulog_eq_1, size_max]); 410 411(* Theorem: let quit k = 2 * size m + if m <= 1 then 0 else if k = 0 then 1 else 1 + 2 * size k; 412 body k = 2 * size m + if m <= 1 then 0 413 else size k + if k = 0 then 0 414 else size c + size (c - k) + size n * size k + size (n MOD k) + if n MOD k = 0 then 0 415 else stepsOf (ordzM k n) + size (MAX m (ordz k n)) + size (m - ordz k n) + if m <= ordz k n then 0 416 else size k; 417 exit k = ((k = 0) \/ (n MOD k = 0) \/ m <= ordz k n) 418 in !k. stepsOf (param_seekM m c n k) = 419 if c <= k then quit k 420 else body k + if exit k then 0 else stepsOf (param_seekM m c n (k + 1)) *) 421(* Proof: 422 stepsOf (param_seekM m c n k) 423 = size k + if k = 0 then 0 424 else size (MAX c k) + size (c - k) + if c <= k then 0 <-- guard is here 425 else size n * size k + size (n MOD k) + if n MOD k = 0 then 0 426 else stepsOf (ordzM k n) + size (MAX m (ordz k n)) + size (m - ordz k n) + if m <= ordz k n then 0 427 else size k + stepsOf (param_seekM m c n (k + 1)) by param_seekM_steps_thm 428 = if c <= k then -- all these before it 429 (size k + if k = 0 then 0 else size (MAX c k) + size (c - k)) 430 else -- repeat all those before it 431 size k + if k = 0 then 0 432 else size (MAX c k) + size (c - k) + 433 size n * size k + size (n MOD k) + if n MOD k = 0 then 0 434 else stepsOf (ordzM k n) + size (MAX m (ordz k n)) + size (m - ordz k n) + if m <= ordz k n then 0 435 else size k + stepsOf (param_seekM m c n (k + 1)) 436 = if c <= k then quit k 437 else body k + if exit k then 0 else stepsOf (param_seekM m c n (k + 1)) 438 where 439 quit k 440 = size k + if k = 0 then 0 else size k + size 0 441 = if k = 0 then size 0 else size k + size k + size 0 442 = if k = 0 then 1 else 1 + 2 * size k 443 body k, with k < c 444 = size k + if k = 0 then 0 445 else size c + size (c - k) + size n * size k + size (n MOD k) + if n MOD k = 0 then 0 446 else stepsOf (ordzM k n) + size (MAX m (ordz k n)) + size (m - ordz k n) + if m <= ordz k n then 0 447 else size k 448 exit k 449 = (k = 0) \/ n MOD k = 0 \/ m <= ordz k n 450*) 451val param_seekM_steps_by_inc_loop = store_thm( 452 "param_seekM_steps_by_inc_loop", 453 ``!m c n. let quit k = if k = 0 then 1 else 1 + 2 * size k; 454 body k = size k + 455 if k = 0 then 0 456 else size c + size (c - k) + size n * size k + size (n MOD k) + if n MOD k = 0 then 0 457 else stepsOf (ordzM k n) + size (MAX m (ordz k n)) + size (m - ordz k n) + if m <= ordz k n then 0 458 else size k; 459 exit k = ((k = 0) \/ (n MOD k = 0) \/ m <= ordz k n) 460 in !k. stepsOf (param_seekM m c n k) = if c <= k then quit k 461 else body k + if exit k then 0 else stepsOf (param_seekM m c n (k + 1))``, 462 rw_tac std_ss[Once param_seekM_steps_thm] >> 463 Cases_on `k = 0` >> simp[Abbr`body`, Abbr`exit`, Abbr`quit`] >> 464 (Cases_on `c <= k` >> simp[MAX_DEF]) >> 465 `c - k = 0` by decide_tac >> 466 rw[] >> 467 `c = k` by decide_tac >> 468 simp[]); 469 470(* 471This puts param_seekM_steps in the category: increasing loop with body cover and exit. 472 param_seekM_steps_by_inc_loop: 473 !k. loop k = if c <= k then quit k else body k + if exit k then 0 else loop (k + 1) 474suitable for: loop_inc_count_cover_exit_le 475*) 476 477(* First, work out a cover for the body. *) 478 479(* Theorem: let body k = size k + 480 if k = 0 then 0 481 else size c + size (c - k) + size n * size k + size (n MOD k) + if n MOD k = 0 then 0 482 else stepsOf (ordzM k n) + size (MAX m (ordz k n)) + size (m - ordz k n) + if m <= ordz k n then 0 483 else size k 484 in !k. body k <= 485 2 * size m + 2 * size c + 4 * size k + size n * size k + 29 * k * size n * size k ** 7 *) 486(* Proof: 487 body k 488 = size k + if k = 0 then 0 489 else size c + size (c - k) + size n * size k + size (n MOD k) + if n MOD k = 0 then 0 490 else stepsOf (ordzM k n) + size (MAX m (ordz k n)) + size (m - ordz k n) + if m <= ordz k n then 0 491 else size k by given 492 <= size k + size c + size (c - k) + size n * size k + size (n MOD k) + 493 stepsOf (ordzM k n) + size (MAX m (ordz k n)) + size (m - ordz k n) + 494 if m <= ordz k n then 0 else size k 495 by ignoring n MOD k = 0 496 Note c - k <= c, so size (c - k) <= size c by size_monotone_le 497 and size (m - ordz k n) <= size m by size_monotone_le 498 and n MOD k < k by MOD_LESS, k <> 0 499 so size (n MOD k) <= size k by size_monotone_lt 500 If m <= ordz k n, 501 size (MAX m (ordz k n)) = size (ordz k n) by MAX_DEF 502 now ordz k n <= k by ZN_order_le, 0 < k 503 so size (MAX m (ordz k n)) <= size k by size_monotone_le 504 but m <= ordz k n gives the last term 0. 505 If ~(m <= ordz k n), or ordz k n < m 506 so size (MAX m (ordz k n)) = size m by MAX_DEF 507 Thus body k 508 <= size k + size c + size c + size n * size k + size k + 509 size m + size m + size k + stepsOf (ordzM k n) 510 = 2 * size m + 2 * size c + 4 * size k + size n * size k + stepsOf (ordzM k n) 511 512 stepsOf (ordzM k n) 513 <= 27 * MAX 1 k * size n * size k ** 7 by ordzM_steps_bound 514 = 27 * k * size n * size k ** 7 by MAX_DEF, k <> 0 515 Thus body k 516 <= 2 * size m + 2 * size c + 4 * size k + size n * size k + 27 * k * size n * size k ** 7 517*) 518val param_seekM_body_upper = store_thm( 519 "param_seekM_body_upper", 520 ``!m c n. let body k = size k + 521 if k = 0 then 0 522 else size c + size (c - k) + size n * size k + size (n MOD k) + if n MOD k = 0 then 0 523 else stepsOf (ordzM k n) + size (MAX m (ordz k n)) + size (m - ordz k n) + if m <= ordz k n then 0 524 else size k 525 in !k. body k <= 526 2 * size m + 2 * size c + 4 * size k + size n * size k + 27 * k * size n * size k ** 7``, 527 rw_tac std_ss[] >> 528 Cases_on `k = 0` >> simp[Abbr`body`] >> 529 `size (c - k) <= size c` by rw[size_monotone_le] >> 530 `0 < size k` by rw[] >> 531 (Cases_on `n MOD k = 0` >> simp[]) >> 532 `size (m - ordz k n) <= size m` by rw[size_monotone_le] >> 533 `size (n MOD k) <= size k` by rw[MOD_LESS, size_monotone_lt] >> 534 `MAX 1 k = k` by rw[MAX_DEF] >> 535 `stepsOf (ordzM k n) <= 27 * k * size n * size k ** 7` by metis_tac[ordzM_steps_bound] >> 536 (Cases_on `m <= ordz k n` >> simp[]) >| [ 537 `MAX m (ordz k n) = ordz k n` by rw[MAX_DEF] >> 538 `ordz k n <= k` by rw[ZN_order_le] >> 539 `MAX m (ordz k n) <= k` by decide_tac >> 540 `size (MAX m (ordz k n)) <= size k` by rw[size_monotone_le] >> 541 decide_tac, 542 `size (MAX m (ordz k n)) = size m` by rw[MAX_DEF] >> 543 decide_tac 544 ]); 545 546(* Theorem: let body k = size k + 547 if k = 0 then 0 548 else size c + size (c - k) + size n * size k + size (n MOD k) + if n MOD k = 0 then 0 549 else stepsOf (ordzM k n) + size (MAX m (ordz k n)) + size (m - ordz k n) + if m <= ordz k n then 0 550 else size k 551 in body k <= 36 * (MAX 1 k) * size m * size c * size n * size k ** 7 *) 552(* Proof: 553 body k 554 <= 2 * size m + 2 * size c + 4 * size k + size n * size k + 27 * k * size n * size k ** 7 555 by param_seekM_body_upper 556 <= (2 + 2 + 4 + 1 + 27) * k * size m * size c * size n * size k ** 7 557 by dominant term 558 = 36 * k * size m * size c * size n * size k ** 7 559 Use (MAX 1 k) to cater for k = 0. 560*) 561val param_seekM_body_bound = store_thm( 562 "param_seekM_body_bound", 563 ``!m c n. let body k = size k + 564 if k = 0 then 0 565 else size c + size (c - k) + size n * size k + size (n MOD k) + if n MOD k = 0 then 0 566 else stepsOf (ordzM k n) + size (MAX m (ordz k n)) + size (m - ordz k n) + if m <= ordz k n then 0 567 else size k 568 in !k. body k <= 36 * (MAX 1 k) * size m * size c * size n * size k ** 7``, 569 rpt strip_tac >> 570 assume_tac param_seekM_body_upper >> 571 last_x_assum (qspecl_then [`m`, `c`, `n`] strip_assume_tac) >> 572 qabbrev_tac `body = \k. size k + 573 if k = 0 then 0 574 else size c + size (c - k) + size n * size k + size (n MOD k) + if n MOD k = 0 then 0 575 else stepsOf (ordzM k n) + size (MAX m (ordz k n)) + size (m - ordz k n) + if m <= ordz k n then 0 576 else size k` >> 577 fs[] >> 578 strip_tac >> 579 last_x_assum (qspec_then `k` strip_assume_tac) >> 580 qabbrev_tac `h = MAX 1 k` >> 581 qabbrev_tac `t = size c * size k ** 7 * size m * size n * h` >> 582 `1 <= h /\ k <= h` by rw[Abbr`h`] >> 583 `0 < t` by rw[MULT_POS, Abbr`t`] >> 584 `1 <= t` by decide_tac >> 585 `size c <= t` by 586 (`size c <= size c * (size k ** 7 * size m * size n * h)` by rw[MULT_POS] >> 587 `size c * (size k ** 7 * size m * size n * h) = t` by rw[Abbr`t`] >> 588 decide_tac) >> 589 `size k <= t` by 590 (`size k <= size k * (size c * size k ** 6 * size m * size n * h)` by rw[MULT_POS] >> 591 `size k * (size c * size k ** 6 * size m * size n * h) = t` by rw[Abbr`t`] >> 592 decide_tac) >> 593 `size m <= t` by 594 (`size m <= size m * (size c * size k ** 7 * size n * h)` by rw[MULT_POS] >> 595 `size m * (size c * size k ** 7 * size n * h) = t` by rw[Abbr`t`] >> 596 decide_tac) >> 597 `size k * size n <= t` by 598 (`size k * size n <= size k * size n * (size c * size k ** 6 * size m * h)` by rw[MULT_POS] >> 599 `size k * size n * (size c * size k ** 6 * size m * h) = t` by rw[Abbr`t`] >> 600 decide_tac) >> 601 `k * size k ** 7 * size n <= t` by 602 (`k * size k ** 7 * size n <= h * size k ** 7 * size n` by rw[] >> 603 `h * size k ** 7 * size n <= h * size k ** 7 * size n * (size c * size m)` by rw[MULT_POS] >> 604 `h * size k ** 7 * size n * (size c * size m) = t` by rw[Abbr`t`] >> 605 decide_tac) >> 606 decide_tac); 607 608(* Theorem: stepsOf (param_seekM m c n k) <= 609 1 + 2 * size (MAX c k) + (c - k) * 36 * c * size m * size n * size c ** 8 *) 610(* Proof: 611 Let quit = (\k. if k = 0 then 1 else 1 + 2 * size k), 612 body = (\k. size k + 613 if k = 0 then 0 614 else size c + size (c - k) + size n * size k + size (n MOD k) + if n MOD k = 0 then 0 615 else stepsOf (ordzM k n) + size (MAX m (ordz k n)) + size (m - ordz k n) + if m <= ordz k n then 0 616 else size k), 617 cover = (\k. 36 * (MAX 1 k) * size m * size c * size n * size k ** 7), 618 exit = (\k. k = 0 \/ n MOD k = 0 \/ m <= ordz k n) 619 loop = (\k. stepsOf (param_seekM m c n k)). 620 621 Then !k. loop k = if c <= k then quit k else body k + if exit k then 0 else loop (k + 1) 622 by param_seekM_steps_by_inc_loop 623 Now !x. body x <= cover x by param_seekM_body_bound 624 and MONO cover by size_monotone_le 625 Let z = k + bop 1 c k * 1 626 = k + (c - k) by bop_1_m_c 627 628 Thus loop k 629 <= quit z + bop 1 c k * cover z by loop_inc_count_cover_exit_le 630 If c <= k, 631 loop k = quit k 632 <= 1 + 2 * size k 633 Otherwise, k < c 634 Then z = k + (c - k) = c. 635 loop k <= quit c + (c - k) * cover c keep (c - k). 636 Note 0 < c by k < c 637 so quit c = 1 + 2 * size c 638 and cover c = 36 * (MAX 1 c) * size m * size c * size n * size c ** 7 639 = 36 * c * size m * size n * size c ** 8 640 Putting all together, 641 loop k <= 1 + 2 * size (MAX c k) + (c - k) * 36 * c * size m * size n * size c ** 8. 642*) 643val param_seekM_steps_upper = store_thm( 644 "param_seekM_steps_upper", 645 ``!m c n k. stepsOf (param_seekM m c n k) <= 646 1 + 2 * size (MAX c k) + 36 * (c - k) * c * size m * size n * size c ** 8``, 647 rpt strip_tac >> 648 assume_tac param_seekM_steps_by_inc_loop >> 649 last_x_assum (qspecl_then [`m`, `c`, `n`] strip_assume_tac) >> 650 assume_tac param_seekM_body_bound >> 651 last_x_assum (qspecl_then [`m`, `c`, `n`] strip_assume_tac) >> 652 qabbrev_tac `quit = \k. if k = 0 then 1 else 1 + 2 * size k` >> 653 qabbrev_tac `body = \k. size k + 654 if k = 0 then 0 655 else size c + size (c - k) + size n * size k + size (n MOD k) + if n MOD k = 0 then 0 656 else stepsOf (ordzM k n) + size (MAX m (ordz k n)) + size (m - ordz k n) + if m <= ordz k n then 0 657 else size k` >> 658 qabbrev_tac `cover = \k. 36 * (MAX 1 k) * size m * size c * size n * size k ** 7` >> 659 qabbrev_tac `exit = \k. (k = 0) \/ (n MOD k = 0) \/ m <= ordz k n` >> 660 qabbrev_tac `loop = \k. stepsOf (param_seekM m c n k)` >> 661 `loop k <= 1 + 2 * size (MAX c k) + 36 * (c - k) * c * size m * size n * size c ** 8` suffices_by rw[] >> 662 `!k. loop k = if c <= k then quit k else body k + if exit k then 0 else loop (k + 1)` by metis_tac[] >> 663 `0 < 1` by decide_tac >> 664 `!x. body x <= cover x` by metis_tac[] >> 665 `MONO cover` by 666 (rw[Abbr`cover`] >> 667 `size x ** 7 <= size y ** 7` by rw[size_monotone_le] >> 668 `MAX 1 x <= MAX 1 y` by rw[MAX_LE] >> 669 `size x ** 7 * MAX 1 x <= size y ** 7 * MAX 1 y` by rw[LE_MONO_MULT2] >> 670 qabbrev_tac `p = size c * size m * size n` >> 671 metis_tac[LE_MULT_LCANCEL, MULT_ASSOC]) >> 672 imp_res_tac loop_inc_count_cover_exit_le >> 673 first_x_assum (qspec_then `k` strip_assume_tac) >> 674 qabbrev_tac `z = k + bop 1 c k * 1` >> 675 Cases_on `c <= k` >| [ 676 `loop k = quit k` by metis_tac[] >> 677 `quit k <= 1 + 2 * size k` by rw[Abbr`quit`] >> 678 `size k <= size (MAX c k)` by rw[size_monotone_le] >> 679 decide_tac, 680 `bop 1 c k = c - k` by rw[bop_1_m_c] >> 681 `z = c` by rw[Abbr`z`] >> 682 `size (MAX c k) = size c` by rw[size_monotone_le, MAX_DEF] >> 683 `cover z = 36 * MAX 1 c * size m * size c * size n * size c ** 7` by rw[Abbr`cover`] >> 684 `MAX 1 c = c` by rw[MAX_DEF] >> 685 `size c * size c ** 7 = size c ** 8` by rw[] >> 686 `36 * MAX 1 c * size m * size c * size n * size c ** 7 = 687 36 * MAX 1 c * size m * size n * (size c * size c ** 7)` by decide_tac >> 688 `_ = 36 * c * size m * size n * size c ** 8` by rw[] >> 689 `quit z <= 1 + 2 * size c` by rw[Abbr`quit`] >> 690 `bop 1 c k * cover z = (c - k) * (36 * c * size m * size n * size c ** 8)` by metis_tac[] >> 691 `size c <= size (MAX c k)` by rw[size_monotone_le] >> 692 decide_tac 693 ]); 694 695(* Theorem: stepsOf (param_seekM m c n k) <= 696 39 * (MAX 1 ((c - k) * c)) * size (MAX c k) * size m * size n * size c ** 7 *) 697(* Proof: 698 stepsOf (param_seekM m c n k) 699 <= 1 + 2 * size (MAX c k) + 36 * (c - k) * c * size m * size n * size c ** 8 700 by param_seekM_steps_upper 701 <= (1 + 2 + 36) * (c - k) * c * size (MAX c k) * size m * size n * size c ** 7 702 by dominant term 703 = 39 * (c - k) * c * size (MAX c k) * size m * size n * size c ** 7 704 Use (MAX 1 (c - k)) to cater for c = k, 705 and (MAX 1 c) to cater for c = 0. 706*) 707val param_seekM_steps_bound = store_thm( 708 "param_seekM_steps_bound", 709 ``!m c n k. stepsOf (param_seekM m c n k) <= 710 39 * (MAX 1 (c - k)) * (MAX 1 c) * size (MAX c k) * size m * size n * size c ** 7``, 711 rpt strip_tac >> 712 assume_tac param_seekM_steps_upper >> 713 last_x_assum (qspecl_then [`m`, `c`, `n`, `k`] strip_assume_tac) >> 714 qabbrev_tac `x = MAX 1 (c - k)` >> 715 qabbrev_tac `y = MAX 1 c` >> 716 qabbrev_tac `z = MAX c k` >> 717 qabbrev_tac `t = x * y * size z * size m * size n * size c ** 7` >> 718 `stepsOf (param_seekM m c n k) <= 39 * t` suffices_by rw[Abbr`t`] >> 719 `1 <= x /\ (c - k) <= x` by rw[MAX_DEF, Abbr`x`] >> 720 `1 <= y /\ c <= y` by rw[Abbr`y`] >> 721 `c <= z /\ k <= z` by rw[Abbr`z`] >> 722 `0 < x * y` by rw[MULT_POS] >> 723 `0 < t` by rw[MULT_POS, Abbr`t`] >> 724 `1 <= t` by decide_tac >> 725 `size z <= t` by 726 (`size z <= size z * (x * y * size m * size n * size c ** 7)` by rw[MULT_POS] >> 727 `size z * (x * y * size m * size n * size c ** 7) = t` by rw[Abbr`t`] >> 728 decide_tac) >> 729 `(c - k) * c * size m * size n * size c ** 8 <= t` by 730 (`size c <= size z` by rw[size_monotone_le] >> 731 `(c - k) * c * size c <= x * y * size z` by rw[LE_MONO_MULT2] >> 732 `(c - k) * c * size m * size n * size c ** 8 = (c - k) * c * size c * (size m * size n * size c ** 7)` by rw[] >> 733 `(c - k) * c * size c * (size m * size n * size c ** 7) <= x * y * size z * (size m * size n * size c ** 7)` by rw[] >> 734 `x * y * size z * (size m * size n * size c ** 7) = t` by rw[Abbr`t`] >> 735 decide_tac) >> 736 decide_tac); 737 738(* Theorem: stepsOf (paramM n) <= 19 * size n + 16904 * size n ** 2 + 1418141046 * size n ** 20 *) 739(* Proof: 740 stepsOf (paramM n) 741 = stepsOf (ulogM n) + 2 * size (ulog n) + 742 if n <= 2 then 0 743 else size (ulog n) ** 2 + 2 * size (ulog n ** 5) + size (MAX (HALF (ulog n ** 5)) 2) + 744 stepsOf (expM (ulog n) 5) + 745 stepsOf (param_seekM (SQ (ulog n)) (2 + HALF (ulog n ** 5)) n 2) by paramM_steps_thm 746 <= 2 * size (ulog n) + size (ulog n) ** 2 + 2 * size (ulog n ** 5) + size (MAX (HALF (ulog n ** 5)) 2) + 747 stepsOf (ulogM n) + stepsOf (expM (ulog n) 5) + 748 stepsOf (param_seekM (SQ (ulog n)) (2 + HALF (ulog n ** 5)) n 2) assume false condition 749 750 The aim is to express each term as some power of (size n). 751 752 Note ulog n <= size n by size_ulog -- this is good 753 and ulog n <= n by ulog_le_self -- not so good 754 Thus size (ulog n) <= size n by size_monotone_le 755 756 Thus b = 2 * size (ulog n) 757 <= 2 * size n for #1 term 758 Thus u = size (ulog n) ** 2 759 <= size n ** 2 for #2 term 760 761 Also size (ulog n ** 5) <= 5 * size (ulog n) by size_exp_upper_alt 762 <= 5 * size n by above 763 Thus v = 2 * size (ulog n ** 5) 764 <= 10 * size n for #3 term 765 766 Note MAX (HALF (ulog n ** 5) 2) 767 <= 2 + HALF (ulog n ** 5) by MAX_LE_SUM 768 Let h = HALF (ulog n ** 5), 769 c = ulog n ** 5, k = size n ** 5. 770 Then h <= c by HALF_LE 771 and c <= k by EXP_EXP_LE_MONO, ulog n <= size n 772 and 0 < k by EXP_POS, size_pos 773 so 2 + h <= 2 + k <= 3 * k by h <= c, c <= k, 0 < k 774 and size (2 + h) <= size (3 * k) by size_monotone_le 775 <= size 3 + size k by size_mult_upper 776 <= 2 + 5 * size n by size_exp_upper_alt, above 777 <= 7 * size n by 0 < size n 778 779 Thus w = size (MAX (HALF (ulog n ** 5)) 2) 780 <= 7 * size n for #4 term 781 782 Now x = stepsOf (ulogM n) for #5 term 783 <= 28 * size n ** 2 by ulogM_steps_bound 784 785 Now y = stepsOf (expM (ulog n) 5) for #6 term 786 <= 15 * MAX 1 5 ** 3 * size (ulog n) ** 2 * (size 5) ** 2 by expM_steps_bound 787 = 15 * 5 ** 3 * 3 ** 2 * size (ulog n) ** 2 by size 5 = 3 788 <= 15 * (5 ** 3) * (3 ** 2) * size n ** 2 789 = 16875 * size n ** 2 790 Now z = stepsOf (param_seekM (SQ (ulog n)) (2 + HALF (ulog n ** 5)) n 2) for #6 term 791 <= 39 * MAX 1 h * MAX 1 (2 + h) * size (MAX (2 + h) 2) * size m * size n * size (2 + h) ** 7 792 by param_seekM_steps_bound, m = SQ (ulog n) 793 = 39 * MAX 1 h * (2 + h) * size (2 + h) * size (SQ (ulog n)) * size n * size (2 + h) ** 7 794 = 39 * MAX 1 h * (2 + h) * size (SQ (ulog n)) * size n * size (2 + h) ** 8 795 796 Note MAX 1 h <= MAX 1 k = k by MAX_LE, 1 <= k, h <= k, 0 < k 797 and 2 + h <= 3 * k by above 798 and size (SQ (ulog n)) 799 <= size (SQ (size n)) by size_monotone_le 800 <= 2 * size (size n) by size_mult_upper 801 <= 2 * size n by size_size_le 802 and size (2 + h) <= 7 * size n by above 803 804 Thus z <= 39 * size n ** 5 * 3 * size n ** 5 * (2 * size n) * size n * (7 * size n) ** 8 805 = 39 * 3 * 2 * 7 ** 8 * size n ** (5 + 5 + 1 + 1 + 8) by EXP_ADD 806 = 1348963434 * size n ** 20 807 808 Finally, 809 stepsOf (paramM n) 810 <= 2 * size n + size n ** 2 + 2 * (5 * size n) + 7 * size n + 811 28 * size n ** 2 + 16875 * size n ** 2 + 1348963434 * size n ** 20 812 = 19 * size n + (1 + 28 + 16875) * size n ** 2 + 1348963434 * size n ** 20 813 = 19 * size n + 16904 * size n ** 2 + 1348963434 * size n ** 20 814*) 815Theorem paramM_steps_upper: 816 !n. stepsOf (paramM n) <= 817 19 * size n + 16904 * size n ** 2 + 1348963434 * size n ** 20 818Proof 819 rpt strip_tac >> 820 assume_tac paramM_steps_thm >> 821 last_x_assum (qspec_then ���n��� strip_assume_tac) >> 822 qabbrev_tac ���h = HALF (ulog n ** 5)��� >> 823 qabbrev_tac ���x = stepsOf (ulogM n)��� >> 824 qabbrev_tac ���y = stepsOf (expM (ulog n) 5)��� >> 825 qabbrev_tac ���z = stepsOf (param_seekM (SQ (ulog n)) (2 + h) n 2)��� >> 826 qabbrev_tac ���b = size (ulog n)��� >> 827 qabbrev_tac ���u = b ** 2��� >> 828 qabbrev_tac ���v = size (ulog n ** 5)��� >> 829 qabbrev_tac ���w = size (MAX h 2)��� >> 830 ���stepsOf (paramM n) <= x + 2 * b + u + 2 * v + w + y + z��� by fs[] >> 831 qabbrev_tac ���c = ulog n ** 5��� >> 832 qabbrev_tac ���k = size n ** 5��� >> 833 ���ulog n <= size n��� by rw[size_ulog] >> 834 ���ulog n <= n��� by rw[ulog_le_self] >> 835 ���b <= size n��� by rw[size_monotone_le, Abbr���b���] >> 836 ���size c <= 5 * b��� by rw[size_exp_upper_alt, Abbr���b���, Abbr���c���] >> 837 ���size c <= 5 * size n��� by decide_tac >> 838 ���h <= c��� by rw[HALF_LE, Abbr���h���] >> 839 ���c <= k��� by rw[Abbr���c���, Abbr���k���] >> 840 ���h <= k��� by decide_tac >> 841 ���0 < k��� by rw[Abbr���k���] >> 842 ���2 + h <= 3 * k��� by decide_tac >> 843 ���size (2 + h) <= 7 * size n��� 844 by (���size (2 + h) <= size (3 * k)��� by rw[size_monotone_le] >> 845 ���size (3 * k) <= size 3 + size k��� by rw[size_mult_upper] >> 846 ���size 3 = 2��� by EVAL_TAC >> 847 ���size k <= 5 * size (size n)��� by rw[size_exp_upper_alt, Abbr���k���] >> 848 ���size (size n) <= size n��� by rw[size_size_le] >> 849 ���0 < size n��� by rw[] >> 850 decide_tac) >> 851 ���u <= size n ** 2��� by rw[Abbr���u���] >> 852 ���v <= 5 * size n��� by rw[Abbr���v���] >> 853 ���w <= 7 * size n��� by 854 (���MAX h 2 <= 2 + h��� by rw[MAX_LE_SUM] >> 855 ���w <= size (2 + h)��� by rw[size_monotone_le, Abbr���w���] >> 856 decide_tac) >> 857 ���x <= 28 * size n ** 2��� by rw[ulogM_steps_bound, Abbr���x���] >> 858 ���y <= 16875 * size n ** 2��� 859 by (���y <= 15 * MAX 1 5 ** 3 * size (ulog n) ** 2 * (size 5) ** 2��� 860 by rw[expM_steps_bound, Abbr���y���] >> 861 ���MAX 1 5 = 5��� by rw[] >> 862 ���size 5 = 3��� by EVAL_TAC >> 863 ���15 * MAX 1 5 ** 3 * size (ulog n) ** 2 * (size 5) ** 2 = 864 15 * 125 * 9 * size (ulog n) ** 2��� by rw[] >> 865 ���size (ulog n) ** 2 <= size n ** 2��� by rw[] >> 866 decide_tac) >> 867 ���z <= 1348963434 * size n ** 20��� 868 by (���z <= 39 * MAX 1 (2 + h - 2) * (MAX 1 (2 + h)) * size (MAX (2 + h) 2) * 869 size (SQ (ulog n)) * size n * size (2 + h) ** 7��� 870 by rw[param_seekM_steps_bound, Abbr���z���, Abbr���h���] >> 871 ���2 + h - 2 = h��� by decide_tac >> 872 ���MAX 1 h <= MAX 1 k��� by rw[] >> 873 ���MAX 1 k = k��� 874 by (rw[MAX_DEF, Abbr���k���] >> ���size n ��� 1��� by simp[] >> 875 ���size n ��� 0��� by (strip_tac >> fs[]) >> simp[]) >> 876 ���MAX 1 (2 + h - 2) <= size n ** 5��� by metis_tac[] >> 877 ���MAX 1 (2 + h) = 2 + h��� by rw[MAX_DEF] >> 878 ���MAX 1 (2 + h) <= 3 * size n ** 5��� by metis_tac[] >> 879 ���size (MAX (2 + h) 2) = size (2 + h)��� by rw[MAX_DEF] >> 880 ���size (MAX (2 + h) 2) <= 7 * size n��� by decide_tac >> 881 ���size (SQ (ulog n)) <= size (size n ** 2)��� by rw[size_monotone_le] >> 882 ���size (size n ** 2) <= 2 * size (size n)��� by rw[size_exp_upper_alt] >> 883 ���size (size n) <= size n��� by rw[size_size_le] >> 884 ���size (SQ (ulog n)) <= 2 * size n��� by decide_tac >> 885 ���size (2 + h) ** 7 <= (7 * size n) ** 7��� by rw[] >> 886 ���(7 * size n) ** 7 = 7 ** 7 * size n ** 7��� by rw[EXP_BASE_MULT] >> 887 ���size (2 + h) ** 7 <= 7 ** 7 * size n ** 7��� by decide_tac >> 888 ���39 * MAX 1 (2 + h - 2) * MAX 1 (2 + h) * size (MAX (2 + h) 2) * size (SQ (ulog n)) * size n * size (2 + h) ** 7 <= 889 39 * size n ** 5 * (3 * size n ** 5) * (7 * size n) * (2 * size n) * size n * (7 ** 7 * size n ** 7)��� by rw[LE_MONO_MULT2] >> 890 ���z <= 39 * 3 * 7 * 2 * 7 ** 7 * (size n ** 5 * size n ** 5 * size n * size n * size n * size n ** 7)��� by decide_tac >> 891 ���SQ (size n ** 5) * size n * size n * size n * size n ** 7 = 892 SQ (size n ** 5) * size n ** 1 * size n ** 1 * size n ** 1 * size n ** 7��� by rw[] >> 893 ���_ = size n ** 20��� by rw[] >> 894 ���39 * 3 * 7 * 2 * 7 ** 7 = 1348963434��� by EVAL_TAC >> 895 metis_tac[]) >> 896 decide_tac 897QED 898 899(* Theorem: stepsOf (paramM n) <= 1348980357 * size n ** 20 *) 900(* Proof: 901 stepsOf (paramM n) 902 <= 19 * size n + 16904 * size n ** 2 + 1348963434 * size n ** 20 by paramM_steps_upper 903 <= (19 + 16904 + 1348963434) * size n ** 20 by dominant term 904 = 1348980357 * size n ** 20 905*) 906val paramM_steps_bound = store_thm( 907 "paramM_steps_bound", 908 ``!n. stepsOf (paramM n) <= 1348980357 * size n ** 20``, 909 rpt strip_tac >> 910 assume_tac paramM_steps_upper >> 911 last_x_assum (qspec_then `n` strip_assume_tac) >> 912 `size n ** 1 <= size n ** 20` by rw[EXP_BASE_LEQ_MONO_IMP] >> 913 `size n ** 2 <= size n ** 20` by rw[EXP_BASE_LEQ_MONO_IMP] >> 914 `size n = size n ** 1` by rw[] >> 915 decide_tac); 916 917(* Theorem: (stepsOf o paramM) IN O_poly 20 *) 918(* Proof: 919 By O_poly_thm, this is to show: 920 ?h k. !n. h < n ==> stepsOf (paramM n) <= k * size n ** 20 921 Note stepsOf (paramM n) <= 1348980357 * size n ** 17 by paramM_steps_bound 922 Take any h, but use k = 1348980357, the result follows. 923*) 924val paramM_steps_O_poly = store_thm( 925 "paramM_steps_O_poly", 926 ``(stepsOf o paramM) IN O_poly 20``, 927 rw[O_poly_thm] >> 928 metis_tac[paramM_steps_bound]); 929 930(* This is a milestone result! *) 931 932(* Theorem: (stepsOf o paramM) IN big_O (\n. (ulog n) ** 20) *) 933(* Proof: 934 Note (stepsOf o paramM) IN O_poly 20 by paramM_steps_O_poly 935 and O_poly 20 936 = big_O (POLY 20 o ulog) by O_poly_eq_O_poly_ulog 937 = (\n. ulog n ** 20) by POLY_def, FUN_EQ_THM 938 The result follows. 939*) 940val paramM_steps_big_O = store_thm( 941 "paramM_steps_big_O", 942 ``(stepsOf o paramM) IN big_O (\n. (ulog n) ** 20)``, 943 assume_tac paramM_steps_O_poly >> 944 `O_poly 20 = big_O (POLY 20 o ulog)` by rw[O_poly_eq_O_poly_ulog] >> 945 `POLY 20 o ulog = \n. (ulog n) ** 20` by rw[FUN_EQ_THM, POLY_def] >> 946 fs[]); 947 948(* Theorem: (valueOf (paramM n) = param n) /\ 949 (stepsOf o paramM) IN big_O (\n. (ulog n) ** 20) *) 950(* Proof: by paramM_value, paramM_steps_big_ *) 951val paramM_thm = store_thm( 952 "paramM_thm", 953 ``!n. (valueOf (paramM n) = param n) /\ 954 (stepsOf o paramM) IN big_O (\n. (ulog n) ** 20)``, 955 metis_tac[paramM_value, paramM_steps_big_O]); 956 957 958(* ------------------------------------------------------------------------- *) 959 960(* export theory at end *) 961val _ = export_theory(); 962 963(*===========================================================================*) 964