1(* ------------------------------------------------------------------------- *) 2(* Computational Complexity *) 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 "complexity"; 12 13(* ------------------------------------------------------------------------- *) 14 15 16 17(* val _ = load "jcLib"; *) 18open jcLib; 19 20(* val _ = load "bitsizeTheory"; *) 21open bitsizeTheory; 22open logrootTheory; (* for LOG_1 *) 23 24(* Get dependent theories in lib *) 25(* val _ = load "logPowerTheory"; (* has helperNum, helperSet, helperFunction *) *) 26(* (* val _ = load "helperListTheory"; -- in bitsizeTheory *) *) 27open helperNumTheory helperSetTheory helperListTheory helperFunctionTheory; 28open logPowerTheory; (* for ulog_pos *) 29 30(* open dependent theories *) 31open pred_setTheory arithmeticTheory dividesTheory gcdTheory; 32open listTheory rich_listTheory;; 33 34 35(* ------------------------------------------------------------------------- *) 36(* Computational Complexity Documentation *) 37(* ------------------------------------------------------------------------- *) 38(* Type and Overload: 39 f1 .+. f2 = fun_sum f1 f2 40 f1 .*. f2 = fun_prod f1 f2 41 s1 |+| s2 = set_sum s1 s2 42 s1 |*| s2 = set_prod s1 s2 43 poly_O m = big_O (POLY m) 44 O_poly n = big_O ((POLY n) o size) 45*) 46(* Definitions and Theorems (# are exported): 47 48 Helper Theorems: 49 50 Big O Notation: 51 big_O_def |- !g. big_O g = {f | ?k c. !n. k < n ==> f n <= c * g n} 52 big_O_element |- !f g. f IN big_O g <=> ?k c. !n. k < n ==> f n <= c * g n 53 big_O_self |- !g. g IN big_O g 54 big_O_cong |- !f1 f2 g. f1 IN big_O g /\ (!n. f1 n = f2 n) ==> f2 IN big_O g 55 big_O_has_zero |- !g. K 0 IN big_O g 56 big_O_1 |- !m. K m IN big_O (K 1) 57 big_O_nonempty |- !g. big_O g <> {} 58 59 Sum and Product of Functions and Sets: 60 fun_sum_def |- !f1 f2. (f1 .+. f2) = (\n. f1 n + f2 n) 61 fun_prod_def |- !f1 f2. (f1 .*. f2) = (\n. f1 n * f2 n) 62 set_sum_def |- !s1 s2. s1 |+| s2 = {f1 .+. f2 | f1 IN s1 /\ f2 IN s2} 63 set_sum_element |- !f1 f2 s1 s2. f1 IN s1 /\ f2 IN s2 ==> f1 .+. f2 IN s1 |+| s2 64 set_sum_eqn |- !f1 f2 s1 s2 x. x IN s1 |+| s2 <=> ?f1 f2. f1 IN s1 /\ f2 IN s2 /\ x = f1 .+. f2 65 set_prod_def |- !s1 s2. s1 |*| s2 = {f1 .*. f2 | f1 IN s1 /\ f2 IN s2} 66 set_prod_element |- !f1 f2 s1 s2. f1 IN s1 /\ f2 IN s2 ==> f1 .*. f2 IN s1 |*| s2 67 set_prod_eqn |- !f1 f2 s1 s2 x. x IN s1 |*| s2 <=> ?f1 f2. f1 IN s1 /\ f2 IN s2 /\ x = f1 .*. f2 68 fun_sum_comm |- !f1 f2. f1 .+. f2 = f2 .+. f1 69 fun_sum_assoc |- !f1 f2 f3. f1 .+. f2 .+. f3 = f1 .+. (f2 .+. f3) 70 fun_prod_comm |- !f1 f2. f1 .*. f2 = f2 .*. f1 71 fun_prod_assoc |- !f1 f2 f3. f1 .*. f2 .*. f3 = f1 .*. (f2 .*. f3) 72 fun_sum_zero |- !f. f .+. K 0 = f /\ K 0 .+. f = f 73 fun_prod_one |- !f. f .*. K 1 = f /\ K 1 .*. f = f 74 fun_sum_mono |- !f1 f2. MONO f1 /\ MONO f2 ==> MONO (f1 .+. f2) 75 fun_prod_mono |- !f1 f2. MONO f1 /\ MONO f2 ==> MONO (f1 .*. f2) 76 77 Theorems for Complexity Class: 78 big_O_sum |- !f1 f2 g1 g2. f1 IN big_O g1 /\ f2 IN big_O g2 ==> f1 .+. f2 IN big_O (g1 .+. g2) 79 big_O_sum_subset |- !g1 g2. big_O g1 |+| big_O g2 SUBSET big_O (g1 .+. g2) 80 big_O_prod |- !f1 f2 g1 g2. f1 IN big_O g1 /\ f2 IN big_O g2 ==> f1 .*. f2 IN big_O (g1 .*. g2) 81 82 Big O Classes: 83 big_O_linear |- !f1 f2 g. f1 IN big_O g /\ f2 IN big_O g ==> 84 !a b. (\n. a * f1 n + b * f2 n) IN big_O g 85 big_O_add |- !f1 f2 g. f1 IN big_O g /\ f2 IN big_O g ==> f1 .+. f2 IN big_O g 86 big_O_sum_self |- !g. big_O g |+| big_O g = big_O g 87 88 Poly O Classes: 89 POLY_def |- !m. POLY m = (\n. n ** m) 90 POLY_0 |- POLY 0 = K 1 91 POLY_1 |- POLY 1 = I 92 POLY_ascending |- !m. MONO (POLY m) 93 poly_O_has_poly |- !m. POLY m IN poly_O m 94 poly_O_add_constant |- !f m. f IN poly_O m ==> !c. (\n. f n + c) IN poly_O m 95 poly_O_mult_constant|- !f m. f IN poly_O m ==> !c. (\n. c * f n) IN poly_O m 96 poly_O_nonempty |- !n. poly_O n <> {} 97 poly_O_constant |- !c0. K c0 IN poly_O 0 98 big_O_poly_sum |- !a b. big_O (POLY a .+. POLY b) SUBSET poly_O (MAX a b) 99 big_O_poly_sum_3 |- !a b c. big_O ((POLY a .+. POLY b) .+. POLY c) SUBSET poly_O (MAX (MAX a b) c) 100 big_O_sum_poly |- !f g a b. f IN poly_O a /\ g IN poly_O b ==> f .+. g IN poly_O (MAX a b) 101 big_O_poly_prod |- !a b. big_O (POLY a .*. POLY b) SUBSET poly_O (a + b) 102 big_O_poly_prod_3 |- !a b c. big_O ((POLY a .*. POLY b) .*. POLY c) SUBSET poly_O (a + b + c) 103 big_O_prod_poly |- !f g a b. f IN poly_O a /\ g IN poly_O b ==> f .*. g IN poly_O (a + b) 104 big_O_poly |- !a b. (\n. a * n ** b) IN poly_O b 105 big_O_example |- !n. (\n. n ** 3 + TWICE n + 10) IN poly_O 3 106 poly_O_linear |- !c0 c1. (\n. c1 * n + c0) IN poly_O 1 107 poly_O_quadratic |- !c0 c1 c2. (\n. c2 * n ** 2 + c1 * n + c0) IN poly_O 2 108 poly_O_constant_exists |- !s t c. ?g. g IN poly_O 0 /\ t + c <= g s + t 109 poly_O_linear_exists |- !n s t b c. n <= s ==> ?g. g IN poly_O 1 /\ t + (b * n + c) <= g s + t 110 poly_O_quadratic_exists |- !n s t a b c. n <= s ==> 111 ?g. g IN poly_O 2 /\ t + (a * n ** 2 + b * n + c) <= g s + t 112 113 poly_O_has_constant |- !m. big_O (K 1) SUBSET poly_O m 114 poly_O_multiple |- !f m. f IN poly_O m ==> !a. (\n. f (a * n)) IN poly_O m 115 poly_O_add_linear |- !f1 f2 m. f1 IN poly_O m /\ f2 IN poly_O m ==> 116 !a b. (\n. f1 (a * n) + f2 (b * n)) IN poly_O m 117 poly_O_subset |- !m n. m <= n ==> poly_O m SUBSET poly_O n 118 poly_O_sum |- !n. poly_O n |+| poly_O n = poly_O n 119 poly_O_sum_subset |- !m n. poly_O n |+| poly_O m SUBSET poly_O (MAX n m) 120 121 Big O theorem with size: 122 big_O_K_subset |- !f. FUN_POS f ==> !c. big_O (K c) SUBSET big_O f 123 big_O_compose_K |- !f1 f2 c. MONO f1 /\ f2 IN big_O (K c) ==> 124 ?d. f1 o f2 IN big_O (K d) 125 big_O_constant |- !g c. FUN_POS g ==> K c IN big_O g 126 POLY_size_pos |- !k x. 0 < (POLY k o size) x 127 big_O_size_linear |- !a b. (\n. a * size n + b) IN big_O size 128 big_O_size_linear_0 |- !a. (\n. a * size n) IN big_O size 129 big_O_size_quadratic |- !a b c. (\n. a * size n ** 2 + b * size n + c) IN O_poly 2 130 big_O_size_quadratic_0 |- !a. (\n. a * size n ** 2) IN O_poly 2 131 big_O_size_quadratic_1 |- !a b. (\n. a * size n ** 2 + b * size n) IN O_poly 2 132 big_O_size_quadratic_2 |- !a b. (\n. a * size n ** 2 + b) IN O_poly 2 133 big_O_dominance |- !f1 f2 g k. 134 (!n. k < n ==> f1 n <= f2 n) /\ f2 IN big_O g ==> f1 IN big_O g 135 136 Polynomial Complexity Class: 137 O_poly_thm |- !f m. f IN O_poly m <=> ?h k. !n. h < n ==> f n <= k * size n ** m 138 O_poly_good |- !f m. f IN O_poly m <=> ?h k. 0 < k /\ !n. h < n ==> f n <= k * size n ** m 139 O_poly_eq_O_poly_ulog 140 |- !n. O_poly n = big_O (POLY n o ulog) 141 big_O_poly_eq_O_poly 142 |- !c n. 0 < c ==> big_O (POLY 1 o (\x. c * size x ** n)) = O_poly n 143 big_O_size_subset_big_O_ulog 144 |- !k. big_O (\n. size n ** k) SUBSET big_O (\n. ulog n ** k) 145 big_O_ulog_subset_big_O_size 146 |- !k. big_O (\n. ulog n ** k) SUBSET big_O (\n. size n ** k) 147 big_O_ulog_eq_big_O_size 148 |- !k. big_O (\n. size n ** k) = big_O (\n. ulog n ** k) 149*) 150 151(* Eliminate parenthesis around equality *) 152val _ = ParseExtras.tight_equality(); 153 154(* ------------------------------------------------------------------------- *) 155(* Helper Theorems *) 156(* ------------------------------------------------------------------------- *) 157 158(* ------------------------------------------------------------------------- *) 159(* Big O Notation *) 160(* ------------------------------------------------------------------------- *) 161 162(* Define big_O as a set *) 163val big_O_def = Define` 164 big_O (g:num -> num) = 165 { f:num -> num | ?k c. !n. k < n ==> f n <= c * (g n) } 166`; 167(* As n exceeds k, f(n) is bounded from above by some multiple of g(n) *) 168 169(* Theorem: f IN big_O g <=> ?k c. !n. k < n ==> f n <= c * (g n) *) 170(* Proof: by big_O_def *) 171val big_O_element = store_thm( 172 "big_O_element", 173 ``!f g. f IN big_O g <=> ?k c. !n. k < n ==> f n <= c * (g n)``, 174 rw[big_O_def]); 175 176(* Theorem: g IN big_O g *) 177(* Proof: 178 By big_O_def, this is to show: 179 ?k c. !n. k < n ==> g n <= c * g n 180 Take any k, say k = 0, but take c = 1. 181 Then g n = 1 * g n by MULT_LEFT_1 182 The result follows. 183*) 184val big_O_self = store_thm( 185 "big_O_self", 186 ``!g. g IN big_O g``, 187 rw[big_O_def] >> 188 qexists_tac `0` >> 189 qexists_tac `1` >> 190 rw[]); 191 192(* Theorem: f1 IN big_O g /\ (!n. f1 n = f2 n) ==> f2 IN big_O g *) 193(* Proof: by big_O_def, take same k and c. *) 194val big_O_cong = store_thm( 195 "big_O_cong", 196 ``!f1 f2 g. f1 IN big_O g /\ (!n. f1 n = f2 n) ==> f2 IN big_O g``, 197 rw[big_O_def] >> 198 metis_tac[]); 199 200(* Theorem: (K 0) IN big_O g *) 201(* Proof: by big_O_def *) 202val big_O_has_zero = store_thm( 203 "big_O_has_zero", 204 ``!g. (K 0) IN big_O g``, 205 rw[big_O_def]); 206 207(* Theorem: (K m) IN big_O (K 1) *) 208(* Proof: by big_O_def, take k = 0 and c = m. *) 209val big_O_1 = store_thm( 210 "big_O_1", 211 ``!m. (K m) IN big_O (K 1)``, 212 rw[big_O_def] >> 213 map_every qexists_tac [`0`, `m`] >> 214 decide_tac); 215 216(* Theorem: big_O g <> {} *) 217(* Proof: 218 Note (K 0) IN big_O g by big_O_has_zero 219 Thus big_O g <> {} by MEMBER_NOT_EMPTY 220*) 221val big_O_nonempty = store_thm( 222 "big_O_nonempty", 223 ``!g. big_O g <> {}``, 224 metis_tac[big_O_has_zero, MEMBER_NOT_EMPTY]); 225 226(* ------------------------------------------------------------------------- *) 227(* Sum and Product of Functions and Sets *) 228(* ------------------------------------------------------------------------- *) 229 230(* Define the sum of functions *) 231val fun_sum_def = Define` 232 fun_sum (f1:num -> num) (f2:num -> num) = (\n. f1 n + f2 n) 233`; 234 235(* Overload the sum of two functions *) 236val _ = overload_on(".+.", ``\f1:num -> num f2:num -> num. fun_sum f1 f2``); 237val _ = set_fixity ".+." (Infixl 500); (* same as addition *) 238 239(* Define the product of functions *) 240val fun_prod_def = Define` 241 fun_prod (f1:num -> num) (f2:num -> num) = (\n. f1 n * f2 n) 242`; 243 244(* Overload the product of two functions *) 245val _ = overload_on(".*.", ``\f1:num -> num f2:num -> num. fun_prod f1 f2``); 246val _ = set_fixity ".*." (Infixl 600); (* same as multiplication *) 247 248(* NOT export these simple definitions to avoid functional form. *) 249(* val _ = export_rewrites ["fun_sum_def", "fun_prod_def"]; *) 250 251(* Define sum of two numeric function sets *) 252val set_sum_def = Define` 253 set_sum (s1:(num -> num) -> bool) (s2:(num -> num) -> bool) = 254 {(f1 .+. f2) | f1 IN s1 /\ f2 IN s2} 255`; 256(* Overload on set_sum *) 257val _ = overload_on("|+|", ``set_sum``); 258val _ = set_fixity "|+|" (Infixl 500); (* same as numeric addition *) 259 260(* 261> set_sum_def; 262val it = |- !s1 s2. (s1 |+| s2) = {f1 .+. f2 | f1 IN s1 /\ f2 IN s2}: thm 263*) 264 265(* Theorem: f1 IN s1 /\ f2 IN s2 ==> (f1 .+. f2) IN (s1 |+| s2) *) 266(* Proof: by set_sum_def *) 267val set_sum_element = store_thm( 268 "set_sum_element", 269 ``!f1 f2 s1 s2. f1 IN s1 /\ f2 IN s2 ==> (f1 .+. f2) IN (s1 |+| s2)``, 270 rw[set_sum_def] >> 271 metis_tac[]); 272 273(* Theorem: x IN s1 |+| s2 <=> ?f1 f2. f1 IN s1 /\ f2 IN s2 /\ (x = f1 .+. f2) *) 274(* Proof: by set_sum_def *) 275val set_sum_eqn = store_thm( 276 "set_sum_eqn", 277 ``!f1 f2 s1 s2 x. x IN s1 |+| s2 <=> ?f1 f2. f1 IN s1 /\ f2 IN s2 /\ (x = f1 .+. f2)``, 278 rw[set_sum_def] >> 279 metis_tac[]); 280 281(* Define product of two numeric function sets *) 282val set_prod_def = Define` 283 set_prod (s1:(num -> num) -> bool) (s2:(num -> num) -> bool) = 284 {(f1 .*. f2) | f1 IN s1 /\ f2 IN s2} 285`; 286(* Overload on set_prod *) 287val _ = overload_on("|*|", ``set_prod``); 288val _ = set_fixity "|*|" (Infixl 600); (* same as numeric multiplication *) 289 290(* 291> set_prod_def; 292val it = |- !s1 s2. (s1 |*| s2) = {f1 .*. f2 | f1 IN s1 /\ f2 IN s2}: thm 293*) 294 295(* Theorem: f1 IN s1 /\ f2 IN s2 ==> (f1 .*. f2) IN (s1 |*| s2) *) 296(* Proof: by set_prod_def *) 297val set_prod_element = store_thm( 298 "set_prod_element", 299 ``!f1 f2 s1 s2. f1 IN s1 /\ f2 IN s2 ==> (f1 .*. f2) IN (s1 |*| s2)``, 300 rw[set_prod_def] >> 301 metis_tac[]); 302 303(* Theorem: x IN s1 |*| s2 <=> ?f1 f2. f1 IN s1 /\ f2 IN s2 /\ (x = f1 .*. f2) *) 304(* Proof: by set_prod_def *) 305val set_prod_eqn = store_thm( 306 "set_prod_eqn", 307 ``!f1 f2 s1 s2 x. x IN s1 |*| s2 <=> ?f1 f2. f1 IN s1 /\ f2 IN s2 /\ (x = f1 .*. f2)``, 308 rw[set_prod_def] >> 309 metis_tac[]); 310 311(* Theorem: f1 .+. f2 = f2 .+. f1 *) 312(* Proof: by fun_sum_def, FUN_EQ_THM, ADD_COMM *) 313val fun_sum_comm = store_thm( 314 "fun_sum_comm", 315 ``!f1 f2. f1 .+. f2 = f2 .+. f1``, 316 rw[fun_sum_def]); 317 318(* Theorem: (f1 .+. f2) .+. f3 = f1 .+. (f2 .+. f3) *) 319(* Proof: by fun_sum_def, FUN_EQ_THM, ADD_ASSOC *) 320val fun_sum_assoc = store_thm( 321 "fun_sum_assoc", 322 ``!f1 f2 f3. (f1 .+. f2) .+. f3 = f1 .+. (f2 .+. f3)``, 323 rw[fun_sum_def]); 324 325(* Theorem: f1 .*. f2 = f2 .*. f1 *) 326(* Proof: by fun_prod_def, FUN_EQ_THM, MULT_COMM *) 327val fun_prod_comm = store_thm( 328 "fun_prod_comm", 329 ``!f1 f2. f1 .*. f2 = f2 .*. f1``, 330 rw[fun_prod_def]); 331 332(* Theorem: (f1 .*. f2) .*. f3 = f1 .*. (f2 .*. f3) *) 333(* Proof: by fun_prod_def, FUN_EQ_THM, MULT_ASSOC *) 334val fun_prod_assoc = store_thm( 335 "fun_prod_assoc", 336 ``!f1 f2 f3. (f1 .*. f2) .*. f3 = f1 .*. (f2 .*. f3)``, 337 rw[fun_prod_def]); 338 339(* Theorem: f .+. (K 0) = f /\ (K 0) .+. f = f *) 340(* Proof: by fun_sum_def *) 341val fun_sum_zero = store_thm( 342 "fun_sum_zero", 343 ``!f. f .+. (K 0) = f /\ (K 0) .+. f = f``, 344 rw[fun_sum_def, FUN_EQ_THM]); 345 346(* Theorem: f .*. (K 1) = f /\ (K 1) .*. f = f *) 347(* Proof: by fun_prod_def *) 348val fun_prod_one = store_thm( 349 "fun_prod_one", 350 ``!f. f .*. (K 1) = f /\ (K 1) .*. f = f``, 351 rw[fun_prod_def, FUN_EQ_THM]); 352 353(* Theorem: MONO f1 /\ MONO f2 ==> MONO (f1 .+. f2) *) 354(* Proof: 355 Let x <= y, 356 Note f1 x <= f1 y by MONO f1 357 and f2 x <= f2 y by MONO f2 358 Thus f1 x + f2 x <= f1 y + f2 y by LE_MONO_ADD2 359 or (f1 .+. f2) x <= (f1 .+. f2) y by fun_sum_def 360 ==> MONO (f1 .+. f2) 361*) 362val fun_sum_mono = store_thm( 363 "fun_sum_mono", 364 ``!f1 f2. MONO f1 /\ MONO f2 ==> MONO (f1 .+. f2)``, 365 rw[fun_sum_def, LE_MONO_ADD2]); 366 367(* Theorem: MONO f1 /\ MONO f2 ==> MONO (f1 .*. f2) *) 368(* Proof: 369 Let x <= y, 370 Note f1 x <= f1 y by MONO f1 371 and f2 x <= f2 y by MONO f2 372 Thus f1 x * f2 x <= f1 y * f2 y by LESS_MONO_MULT2 373 or (f1 .*. f2) x <= (f1 .*. f2) y by fun_prod_def 374 ==> MONO (f1 .*. f2) 375*) 376val fun_prod_mono = store_thm( 377 "fun_prod_mono", 378 ``!f1 f2. MONO f1 /\ MONO f2 ==> MONO (f1 .*. f2)``, 379 rw[fun_prod_def, LESS_MONO_MULT2]); 380 381(* ------------------------------------------------------------------------- *) 382(* Theorems for Complexity Class *) 383(* ------------------------------------------------------------------------- *) 384 385(* Theorem: f1 IN big_O g1 /\ f2 IN big_O g2 ==> (f1 .+. f2) IN big_O (g1 .+. g2) *) 386(* Proof: 387 By big_O_def, fun_sum_def, this is to show: 388 !n. k1 < n ==> f1 n <= c1 * g1 n /\ 389 !n. k2 < n ==> f1 n <= c2 * g1 n ==> 390 ?k c. !n. k < n ==> f1 n + f2 n <= c * (g1 n + g2 n) 391 Let k = MAX k1 k2, c = MAX c1 c2. Take this k and c. 392 Then k1 <= k /\ k2 <= k by MAX_IS_MAX 393 and c1 <= c /\ c2 <= c by MAX_IS_MAX 394 Thus f1 n <= c * g1 n by LESS_MONO_MULT, LESS_EQ_TRANS, k1 < n 395 and f2 n <= c * g2 n by LESS_MONO_MULT, LESS_EQ_TRANS, k2 < n 396 ==> f1 n + f2 n <= c * (g1 n + g2 n) by LEFT_ADD_DISTRIB 397*) 398val big_O_sum = store_thm( 399 "big_O_sum", 400 ``!f1 f2 g1 g2. f1 IN big_O g1 /\ f2 IN big_O g2 ==> (f1 .+. f2) IN big_O (g1 .+. g2)``, 401 rw[big_O_def, fun_sum_def] >> 402 qexists_tac `MAX k k'` >> 403 qexists_tac `MAX c c'` >> 404 rpt strip_tac >> 405 qabbrev_tac `d = MAX c c'` >> 406 `f1 n <= c * g1 n /\ f2 n <= c' * g2 n` by fs[] >> 407 `c * g1 n <= d * g1 n /\ c' * g2 n <= d * g2 n` by rw[Abbr`d`] >> 408 `f1 n + f2 n <= d * g1 n + d * g2 n` by rw[] >> 409 `d * g1 n + d * g2 n = d * (g1 n + g2 n)` by rw[] >> 410 decide_tac); 411 412(* Theorem: (big_O g1) |+| (big_O g2) SUBSET big_O (g1 .+. g2) *) 413(* Proof: 414 By set_sum_def, SUBSET_DEF, this is to show: 415 f1 IN big_O g1 /\ f2 IN big_O g2 ==> f1 .+. f2 IN big_O (g1 .+. g2) 416 This is true by big_O_sum 417*) 418val big_O_sum_subset = store_thm( 419 "big_O_sum_subset", 420 ``!g1 g2. (big_O g1) |+| (big_O g2) SUBSET big_O (g1 .+. g2)``, 421 rw[set_sum_def, SUBSET_DEF] >> 422 rw[big_O_sum]); 423 424(* Theorem: f1 IN big_O g1 /\ f2 IN big_O g2 ==> (f1 .*. f2) IN big_O (g1 .*. g2) *) 425(* Proof: 426 By big_O_def, fun_prod_def, this is to show: 427 !n. k1 < n ==> f1 n <= c1 * g1 n /\ 428 !n. k2 < n ==> f1 n <= c2 * g1 n ==> 429 ?k c. !n. k < n ==> f1 n + f2 n <= c * (g1 n + g2 n) 430 Let k = MAX k1 k2, c = MAX c1 c2. Take this k and (SQ c). 431 Then k1 <= k /\ k2 <= k by MAX_IS_MAX 432 and c1 <= c /\ c2 <= c by MAX_IS_MAX 433 Thus f1 n <= (MAX c1 c2) * g1 n by LESS_MONO_MULT, LESS_EQ_TRANS, k1 < n 434 and f2 n <= (MAX c1 c2) * g2 n by LESS_MONO_MULT, LESS_EQ_TRANS, k2 < n 435 ==> f1 n * f2 n <= (SQ c) * (g1 n * g2 n) by LESS_MONO_MULT2 436*) 437val big_O_prod = store_thm( 438 "big_O_prod", 439 ``!f1 f2 g1 g2. f1 IN big_O g1 /\ f2 IN big_O g2 ==> (f1 .*. f2) IN big_O (g1 .*. g2)``, 440 rw[big_O_def, fun_prod_def] >> 441 qexists_tac `MAX k k'` >> 442 qexists_tac `(MAX c c') * (MAX c c')` >> 443 rpt strip_tac >> 444 qabbrev_tac `d = MAX c c'` >> 445 `f1 n <= c * g1 n /\ f2 n <= c' * g2 n` by fs[] >> 446 `c * g1 n <= d * g1 n /\ c' * g2 n <= d * g2 n` by rw[Abbr`d`] >> 447 `f1 n <= d * g1 n /\ f2 n <= d * g2 n` by decide_tac >> 448 `(d * g1 n) * (d * g2 n) = (SQ d) * g1 n * g2 n` by rw[] >> 449 metis_tac[LESS_MONO_MULT2]); 450 451(* ------------------------------------------------------------------------- *) 452(* Big O Classes *) 453(* ------------------------------------------------------------------------- *) 454 455(* Theorem: f1 IN big_O g /\ f2 IN big_O g ==> !a b. (\n. a * f1 n + b * f2 n) IN big_O g *) 456(* Proof: 457 Note f1 IN big_O g 458 ==> ?k1 c1. !n. k1 < n ==> f1 n <= c1 * g n by big_O_def 459 Note f2 IN big_O g 460 ==> ?k2 c2. !n. k2 < n ==> f2 n <= c2 * g n by big_O_def 461 Let k = MAX k1 k2, and c = a * c1 + b * c2. 462 Then k1 <= k /\ k2 <= k by MAX_IS_MAX 463 Thus for n > k, n > k1 and n > k2. 464 ==> a * f1 n + b * f2 n 465 <= a * (c1 * g n) + b * (c2 * g n) by above 466 = (a * c1 + b * c2) * g n by RIGHT_ADD_DISTRIB 467 = c * g n by above 468*) 469val big_O_linear = store_thm( 470 "big_O_linear", 471 ``!f1 f2 g. f1 IN big_O g /\ f2 IN big_O g ==> !a b. (\n. a * f1 n + b * f2 n) IN big_O g``, 472 rw[big_O_def] >> 473 qabbrev_tac `m = MAX k k'` >> 474 `k <= m /\ k' <= m` by rw[Abbr`m`] >> 475 qexists_tac `m` >> 476 qexists_tac `a * c + b * c'` >> 477 rpt strip_tac >> 478 `k < n /\ k' < n` by decide_tac >> 479 `a * f1 n <= a * (c * g n)` by rw[] >> 480 `b * f2 n <= b * (c' * g n)` by rw[] >> 481 `a * f1 n + b * f2 n <= a * (c * g n) + b * (c' * g n)` by decide_tac >> 482 `a * (c * g n) + b * (c' * g n) = (a * c + b * c') * g n` by rw[] >> 483 decide_tac); 484 485(* Theorem: f1 IN big_O g /\ f2 IN big_O g ==> (\n. f1 n + f2 n) IN big_O g *) 486(* Proof: by fun_sum_def, big_O_linear *) 487val big_O_add = store_thm( 488 "big_O_add", 489 ``!f1 f2 g. f1 IN big_O g /\ f2 IN big_O g ==> (f1 .+. f2) IN big_O g``, 490 rpt strip_tac >> 491 `(f1 .+. f2) = (\n. 1 * f1 n + 1 * f2 n)` by rw[fun_sum_def, FUN_EQ_THM] >> 492 `(\n. 1 * f1 n + 1 * f2 n) IN big_O g` by rw[big_O_linear] >> 493 fs[]); 494 495(* Theorem: (big_O g) |+| (big_O g) = (big_O g) *) 496(* Proof: 497 By SUBSET_ANTISYM, to show: 498 (1) (big_O g) |+| (big_O g) SUBSET (big_O g) 499 By SUBSET_DEF, 500 x IN (big_O g) |+| (big_O g) 501 ==> ?f1 f2. f1 IN big_O g /\ f2 IN big_O g /\ x = f1 .+. f2 by set_sum_def 502 ==> ?f1 f2. f1 .+. f2 = x IN (big_O g) by big_O_add 503 ==> x IN big_O g, hence true. 504 (2) (big_O g) ==> (big_O g) |+| (big_O g) 505 This is to show: 506 x IN big_O g ==> ?f1 f2. f1 IN big_O g /\ f2 IN big_O g /\ x = f1 .+. f2 507 Take f1 = x, f2 = K 0. 508 Then f1 = x IN big_O g by given 509 and f2 = (K 0) IN big_O g by big_O_has_zero 510 and f1 .+. f2 = x .+. (K 0) 511 = x by fun_sum_zero 512*) 513val big_O_sum_self = store_thm( 514 "big_O_sum_self", 515 ``!g. (big_O g) |+| (big_O g) = (big_O g)``, 516 rw[set_sum_def, EXTENSION] >> 517 rw[EQ_IMP_THM] >- 518 rw[big_O_add] >> 519 qexists_tac `x` >> 520 qexists_tac `K 0` >> 521 rw[fun_sum_zero, big_O_has_zero]); 522 523(* ------------------------------------------------------------------------- *) 524(* Poly O Classes *) 525(* ------------------------------------------------------------------------- *) 526 527(* Define the standard polynomial functions *) 528val POLY_def = Define` 529 POLY m = (\n:num. n ** m) 530`; 531(* Overload the polynomial class *) 532val _ = overload_on("poly_O", ``\m. big_O (POLY m)``); 533 534(* NOT export POLY_def to avoid expansion of poly_O in rw[], fs[], simp[]. *) 535 536(* Theorem: POLY 0 = K 1 *) 537(* Proof: 538 POLY 0 539 = (\n. n ** 0) by POLY_def 540 = (\n. 1) by EXP_0 541 = K 1 by FUN_EQ_THM 542*) 543val POLY_0 = store_thm( 544 "POLY_0", 545 ``POLY 0 = K 1``, 546 rw[POLY_def, FUN_EQ_THM]); 547 548(* Theorem: POLY 1 = I *) 549(* Proof: 550 POLY 1 551 = (\n. n ** 1) by POLY_def 552 = (\n. n) by EXP_1 553 = I by I_THM 554*) 555val POLY_1 = store_thm( 556 "POLY_1", 557 ``POLY 1 = I``, 558 rw[POLY_def, FUN_EQ_THM]); 559 560(* Theorem: MONO (POLY m) *) 561(* Proof: 562 By notation of MONO, this is to show: 563 x <= y ==> POLY m x <= POLY m y 564 or x <= y ==> x ** m <= y ** m by POLY_def 565 which is true by EXP_EXP_LE_MONO 566*) 567val POLY_ascending = store_thm( 568 "POLY_ascending", 569 ``!m. MONO (POLY m)``, 570 rw[POLY_def]); 571 572(* Theorem: POLY m IN poly_O m *) 573(* Proof: 574 By big_O_def, POLY_def, this is to show: 575 ?k c. !n. k < n ==> 0 < c 576 Take any k, put c = 1. 577*) 578val poly_O_has_poly = store_thm( 579 "poly_O_has_poly", 580 ``!m. POLY m IN poly_O m``, 581 rw[big_O_def, POLY_def] >> 582 metis_tac[DECIDE``0 < 1``]); 583 584(* Theorem: f IN poly_O m ==> !c. (\n. f n + c) IN poly_O m *) 585(* Proof: 586 By big_O_def, POLY_def, this is to show: 587 !n. k < n ==> f n <= c * n ** m 588 ==> ?k c''. !n. k < n ==> c' + f n <= c'' * n ** m 589 Take the same k, but use (c' + c) for c''. 590 Then c'' * n ** m 591 = (c' + c) * n ** m 592 = c' * n ** m + c * n ** m by RIGHT_ADD_DISTRIB 593 >= c' * n ** m + f n by given 594 >= c' + f n by ZERO_LT_EXP, or ONE_LE_EXP, 0 < n 595*) 596val poly_O_add_constant = store_thm( 597 "poly_O_add_constant", 598 ``!f m. f IN poly_O m ==> !c. (\n. f n + c) IN poly_O m``, 599 rw[big_O_def, POLY_def] >> 600 qexists_tac `k` >> 601 qexists_tac `c' + c` >> 602 rw[RIGHT_ADD_DISTRIB] >> 603 `c' <= c' * n ** m` by rw[] >> 604 metis_tac[LE_MONO_ADD2, ADD_COMM]); 605 606(* Theorem: f IN poly_O m ==> !c. (\n. c * f n) IN poly_O m *) 607(* Proof: 608 By big_O_def, POLY_def, this is to show: 609 !n. k < n ==> f n <= c * n ** m 610 ==> ?k c''. !n. k < n ==> c' * f n <= c'' * n ** m 611 Take the same k, but use (c' * c) for c''. 612 Then c'' * n ** m 613 = (c' * c) * n ** m 614 = c' * (c * n ** m) by MULT_ASSOC 615 >= c' * f n by LE_MULT_LCANCEL, given 616*) 617val poly_O_mult_constant = store_thm( 618 "poly_O_mult_constant", 619 ``!f m. f IN poly_O m ==> !c. (\n. c * f n) IN poly_O m``, 620 rw[big_O_def, POLY_def] >> 621 qexists_tac `k` >> 622 qexists_tac `c' * c` >> 623 metis_tac[LE_MULT_LCANCEL, MULT_ASSOC]); 624 625(* Theorem: poly_O n <> {} *) 626(* Proof: by big_O_nonempty *) 627val poly_O_nonempty = store_thm( 628 "poly_O_nonempty", 629 ``!n. poly_O n <> {}``, 630 rw[big_O_nonempty]); 631 632(* Theorem: (K c0) IN poly_O 0 *) 633(* Proof: by big_O_def, POLY_def, arithmetic. *) 634val poly_O_constant = store_thm( 635 "poly_O_constant", 636 ``!c0. (K c0) IN poly_O 0``, 637 rw[big_O_def, POLY_def] >> 638 qexists_tac `0` >> 639 qexists_tac `c0` >> 640 fs[]); 641 642(* Theorem: big_O (POLY a .+. POLY b) SUBSET poly_O (MAX a b) *) 643(* Proof: 644 By big_O_def, fun_sum_def, POLY_def, SUBSET_DEF, this is to show: 645 !n. k < n ==> x n <= c * (n ** a + n ** b) ==> 646 ?k c. !n. k < n ==> x n <= c * n ** MAX a b 647 Take the same k and (2 * c). 648 Let m = MAX a b. 649 Note 0 < n by k < n 650 Then n ** a <= n ** m by EXP_BASE_LEQ_MONO_IMP, MAX_IS_MAX, 0 < n 651 and n ** b <= n ** m by EXP_BASE_LEQ_MONO_IMP, MAX_IS_MAX, 0 < n 652 x n 653 <= c * (n ** a + n ** b) by given 654 <= c * (n ** m + n ** m) by above 655 = 2 * c * n ** m by arithmetic 656*) 657val big_O_poly_sum = store_thm( 658 "big_O_poly_sum", 659 ``!a b. big_O (POLY a .+. POLY b) SUBSET poly_O (MAX a b)``, 660 rw[big_O_def, fun_sum_def, POLY_def, SUBSET_DEF] >> 661 qexists_tac `k` >> 662 qexists_tac `2 * c` >> 663 rpt strip_tac >> 664 qabbrev_tac `m = MAX a b` >> 665 `0 < n` by decide_tac >> 666 `n ** a <= n ** m /\ n ** b <= n ** m` by metis_tac[EXP_BASE_LEQ_MONO_IMP, MAX_IS_MAX] >> 667 `x n <= c * (n ** a + n ** b)` by rw[] >> 668 `c * (n ** a + n ** b) <= c * (n ** m + n ** m)` by rw[] >> 669 `c * (n ** m + n ** m) = 2 * c * n ** m` by rw[] >> 670 decide_tac); 671 672(* Theorem: big_O (POLY a .+. POLY b .+. POLY c) SUBSET poly_O (MAX (MAX a b) c) *) 673(* Proof: 674 By big_O_def, fun_sum_def, POLY_def, SUBSET_DEF, this is to show: 675 !n. k < n ==> x n <= c' * (n ** a + (n ** b + n ** c)) ==> 676 ?k c'. !n. k < n ==> x n <= c' * n ** MAX (MAX a b) c 677 Take the same k and (3 * c'). 678 Let m = MAX (MAX a b) c. 679 Note 0 < n by k < n 680 and a <= m /\ b <= m /\ c <= m by MAX_DEF 681 Then n ** a <= n ** m by EXP_BASE_LEQ_MONO_IMP, 0 < n 682 and n ** b <= n ** m by EXP_BASE_LEQ_MONO_IMP, 0 < n 683 and n ** c <= n ** m by EXP_BASE_LEQ_MONO_IMP, 0 < n 684 x n 685 <= c' * (n ** a + (n ** b + n ** c)) by given 686 <= c' * (n ** m + (n ** m + n ** m)) by above 687 = 3 * c' * n ** m by arithmetic 688*) 689val big_O_poly_sum_3 = store_thm( 690 "big_O_poly_sum_3", 691 ``!a b c. big_O (POLY a .+. POLY b .+. POLY c) SUBSET poly_O (MAX (MAX a b) c)``, 692 rw[big_O_def, fun_sum_def, POLY_def, SUBSET_DEF] >> 693 qexists_tac `k` >> 694 qexists_tac `3 * c'` >> 695 rpt strip_tac >> 696 qabbrev_tac `m = MAX (MAX a b) c` >> 697 `0 < n` by decide_tac >> 698 `a <= m /\ b <= m /\ c <= m` by rw[MAX_DEF, Abbr`m`] >> 699 `n ** a <= n ** m /\ n ** b <= n ** m /\ n ** c <= n ** m` by metis_tac[EXP_BASE_LEQ_MONO_IMP] >> 700 `x n <= c' * (n ** a + (n ** b + n ** c))` by rw[] >> 701 `c' * (n ** a + (n ** b + n ** c)) <= c' * (n ** m + (n ** m + n ** m))` by rw[] >> 702 `c' * (n ** m + (n ** m + n ** m)) = 3 * c' * n ** m` by rw[] >> 703 decide_tac); 704 705(* Theorem: f IN poly_O a /\ g IN poly_O b ==> f .+. g IN poly_O (MAX a b) *) 706(* Proof: 707 f IN poly_O a /\ g IN poly_O b 708 ==> (f .+. g) IN big_O (POLY a .+. POLY b)) by big_O_sum 709 ==> (f .+. g) IN poly_O (MAX a b) by big_O_poly_sum, SUBSET_DEF 710*) 711val big_O_sum_poly = store_thm( 712 "big_O_sum_poly", 713 ``!f g a b. f IN poly_O a /\ g IN poly_O b ==> f .+. g IN poly_O (MAX a b)``, 714 metis_tac[big_O_sum, big_O_poly_sum, SUBSET_DEF]); 715 716(* Theorem: big_O (POLY a .*. POLY b) SUBSET poly_O (a + b) *) 717(* Proof: 718 By big_O_def, fun_prod_def, POLY_def, SUBSET_DEF, this is to show: 719 !n. k < n ==> x n <= c * (n ** a * n ** b) ==> 720 ?k c. !n. k < n ==> x n <= c * n ** (a + b) 721 Take the same k and c. 722 x n 723 <= c * (n ** a * n ** b) by given 724 <= c * n ** (a + b) by EXP_ADD 725*) 726val big_O_poly_prod = store_thm( 727 "big_O_poly_prod", 728 ``!a b. big_O (POLY a .*. POLY b) SUBSET poly_O (a + b)``, 729 rw[big_O_def, fun_prod_def, POLY_def, SUBSET_DEF] >> 730 qexists_tac `k` >> 731 qexists_tac `c` >> 732 rpt strip_tac >> 733 `x n <= c * (n ** a * n ** b)` by rw[] >> 734 `c * (n ** a * n ** b) = c * n ** (a + b)` by rw[EXP_ADD] >> 735 decide_tac); 736 737(* Theorem: big_O (POLY a .*. POLY b .*. POLY c) SUBSET poly_O (a + b + c) *) 738(* Proof: 739 By big_O_def, fun_prod_def, POLY_def, SUBSET_DEF, this is to show: 740 !n. k < n ==> x n <= c' * n ** a * n ** b * n ** c ==> 741 ?k c'. !n. k < n ==> x n <= c' * n ** (a + (b + c)) 742 Take the same k and c'. 743 x n 744 <= c' * (n ** a * n ** b * n ** c) by given 745 <= c' * n ** (a + b + c) by EXP_ADD 746*) 747val big_O_poly_prod_3 = store_thm( 748 "big_O_poly_prod_3", 749 ``!a b c. big_O (POLY a .*. POLY b .*. POLY c) SUBSET poly_O (a + b + c)``, 750 rw[big_O_def, fun_prod_def, POLY_def, SUBSET_DEF] >> 751 qexists_tac `k` >> 752 qexists_tac `c'` >> 753 rpt strip_tac >> 754 `x n <= c' * (n ** a * n ** b * n ** c)` by rw[] >> 755 `c' * (n ** a * n ** b * n ** c) = c' * n ** (a + (b + c))` by rw[EXP_ADD] >> 756 decide_tac); 757 758(* Theorem: f IN poly_O a /\ g IN poly_O b ==> f .*. g IN poly_O (a + b) *) 759(* Proof: 760 f IN poly_O a /\ g IN poly_O b 761 ==> (f .*. g) IN big_O (POLY a .*. POLY b) by big_O_prod 762 ==> (f .*. g) IN poly_O (a + b) by big_O_poly_prod, SUBSET_DEF 763*) 764val big_O_prod_poly = store_thm( 765 "big_O_prod_poly", 766 ``!f g a b. f IN poly_O a /\ g IN poly_O b ==> f .*. g IN poly_O (a + b)``, 767 metis_tac[big_O_prod, big_O_poly_prod, SUBSET_DEF]); 768 769(* Theorem: (\n. a * n ** b) IN poly_O b *) 770(* Proof: by big_O_def, POLY_def, take k = 0 and c = a. *) 771val big_O_poly = store_thm( 772 "big_O_poly", 773 ``!a b. (\n. a * n ** b) IN poly_O b``, 774 rw[big_O_def, POLY_def] >> 775 map_every qexists_tac [`0`, `a`] >> 776 fs[]); 777 778(* Theorem: (\n. n ** 3 + TWICE n + 10) IN poly_O 3 *) 779(* Proof: 780 Let f = \n. n ** 3 + 2 * n + 10. 781 f1 = \n. 1 * n ** 3, 782 f2 = \n. 2 * n ** 1, 783 f3 = \n. 10 * n ** 0. 784 Then f1 IN poly_O 3 by big_O_poly 785 and f2 IN poly_O 1 by big_O_poly 786 and f3 IN poly_O 0 by big_O_poly 787 ==> f1 .+. f2 IN poly_O (MAX 3 1) by big_O_sum_poly 788 Let f4 = (f1 .+. f2). 789 Then f4 IN poly_O 3 by MAX_DEF 790 Note f = f4 .+. f3 by FUN_EQ_THM 791 and f IN poly_O (MAX 3 0) by big_O_sum_poly 792 or f IN poly_O 3 by MAX_DEF 793*) 794val big_O_example = store_thm( 795 "big_O_example", 796 ``!n. (\n. n ** 3 + TWICE n + 10) IN poly_O 3``, 797 rpt strip_tac >> 798 qabbrev_tac `f = \n. n ** 3 + 2 * n + 10` >> 799 qabbrev_tac `f1 = \n. 1 * n ** 3` >> 800 qabbrev_tac `f2 = \n. 2 * n ** 1` >> 801 qabbrev_tac `f3 = \n. 10 * n ** 0` >> 802 `f1 IN poly_O 3` by rw[big_O_poly, Abbr`f1`] >> 803 `f2 IN poly_O 1` by rw[big_O_poly, Abbr`f2`] >> 804 `f3 IN poly_O 0` by rw[big_O_poly, Abbr`f3`] >> 805 `(MAX 3 1 = 3) /\ (MAX 3 0 = 3)` by rw[] >> 806 `f1 .+. f2 IN poly_O (MAX 3 1)` by rw[big_O_sum_poly] >> 807 `f1 .+. f2 IN poly_O 3` by metis_tac[] >> 808 qabbrev_tac `f4 = (f1 .+. f2)` >> 809 `f = (f4 .+. f3)` by rw[fun_sum_def, FUN_EQ_THM, Abbr`f`, Abbr`f1`, Abbr`f2`, Abbr`f3`, Abbr`f4`] >> 810 `f IN poly_O (MAX 3 0)` by rw[big_O_sum_poly] >> 811 metis_tac[]); 812 813(* Theorem: (\n. c1 * n + c0) IN poly_O 1 *) 814(* Proof: by big_O_def, POLY_def, arithmetic. *) 815val poly_O_linear = store_thm( 816 "poly_O_linear", 817 ``!c0 c1. (\n. c1 * n + c0) IN poly_O 1``, 818 rw[big_O_def, POLY_def] >> 819 qexists_tac `c0` >> 820 qexists_tac `1 + c1` >> 821 rpt strip_tac >> 822 `c0 + c1 * n <= n + c1 * n` by rw[] >> 823 `n + c1 * n = (1 + c1) * n` by rw[] >> 824 decide_tac); 825 826(* Theorem: (\n. c2 * n ** 2 + c1 * n + c0) IN poly_O 2 *) 827(* Proof: by big_O_def, POLY_def, arithmetic. *) 828val poly_O_quadratic = store_thm( 829 "poly_O_quadratic", 830 ``!c0 c1 c2. (\n. c2 * n ** 2 + c1 * n + c0) IN poly_O 2``, 831 rw[big_O_def, POLY_def] >> 832 qexists_tac `c0 + c1` >> 833 qexists_tac `1 + c2` >> 834 rpt strip_tac >> 835 `1 <= n` by decide_tac >> 836 `n = n - 1 + 1` by decide_tac >> 837 `c0 + (c1 * n + c2 * n ** 2) = (c0 + c1 * n) + c2 * n ** 2` by decide_tac >> 838 `_ = c0 + (c1 * (n - 1) + c1) + c2 * n ** 2` by metis_tac[LEFT_ADD_DISTRIB, MULT_RIGHT_1] >> 839 `_ = c1 * (n - 1) + (c0 + c1) + c2 * n ** 2` by decide_tac >> 840 `c1 * (n - 1) + (c0 + c1) + c2 * n ** 2 <= c1 * (n - 1) + n + c2 * n ** 2` by rw[] >> 841 `c1 * (n - 1) + n + c2 * n ** 2 <= n * (n - 1) + n + c2 * n ** 2` by rw[] >> 842 `n * (n - 1) + n + c2 * n ** 2 = n * n + c2 * n ** 2` by metis_tac[LEFT_ADD_DISTRIB, MULT_RIGHT_1] >> 843 `_ = (1 + c2) * n ** 2` by rw[GSYM EXP_2] >> 844 decide_tac); 845 846(* Theorem: ?g. g IN poly_O 0 /\ t + c <= g s + t *) 847(* Proof: 848 Take g = K c, 849 Then g IN poly_O 0 by poly_O_constant 850 and c = g s by function application 851 or t + c <= g s + t by arithmetic 852*) 853val poly_O_constant_exists = store_thm( 854 "poly_O_constant_exists", 855 ``!s t c. ?g. g IN poly_O 0 /\ t + c <= g s + t``, 856 rpt strip_tac >> 857 qexists_tac `K c` >> 858 fs[] >> 859 metis_tac[poly_O_constant]); 860 861(* Theorem: n <= s ==> ?g. g IN poly_O 1 /\ t + (b * n + c) <= g s + t *) 862(* Proof: 863 Take g = (\n. b * n + c), 864 Then g IN poly_O 1 by poly_O_linear 865 and b * n + c 866 <= b * s + c by n <= s 867 = g s by function application 868 or t + (b * n + c) <= g s + t by arithmetic 869*) 870val poly_O_linear_exists = store_thm( 871 "poly_O_linear_exists", 872 ``!n s t b c. n <= s ==> ?g. g IN poly_O 1 /\ t + (b * n + c) <= g s + t``, 873 rpt strip_tac >> 874 qexists_tac `\n. b * n + c` >> 875 fs[] >> 876 `(\n. b * n + c) IN poly_O 1` by metis_tac[poly_O_linear] >> 877 fs[]); 878 879(* Theorem: n <= s ==> ?g. g IN poly_O 2 /\ t + (a * n ** 2 + b * n + c) <= g s + t *) 880(* Proof: 881 Take g = (\n. a * n ** 2 + b * n + c), 882 Then g IN poly_O 1 by poly_O_linear 883 and a * n ** 2 + b * n + c 884 <= a * s ** 2 + b * s + c by EXP_EXP_LE_MONO, n <= s 885 = g s by function application 886 or t + (a * n ** 2 + b * n + c) 887 <= g s + t by arithmetic 888*) 889val poly_O_quadratic_exists = store_thm( 890 "poly_O_quadratic_exists", 891 ``!n s t a b c. n <= s ==> ?g. g IN poly_O 2 /\ t + (a * n ** 2 + b * n + c) <= g s + t``, 892 rpt strip_tac >> 893 qexists_tac `\n. a * n ** 2 + b * n + c` >> 894 fs[] >> 895 `(\n'. a * n' ** 2 + b * n' + c) IN poly_O 2` by metis_tac[poly_O_quadratic] >> 896 fs[] >> 897 `a * n ** 2 <= a * s ** 2` by rw[] >> 898 `b * n <= b * s` by rw[] >> 899 decide_tac); 900 901(* Theorem: big_O (K 1) SUBSET poly_O m *) 902(* Proof: 903 By big_O_def, POLY_def and SUBSET_DEF, this is to show: 904 !n. k < n ==> x n <= c ==> ?k c. !n. k < n ==> x n <= c * n ** m 905 Take the same k, the same c. 906 Then if k < n 907 ==> x n <= c by implication 908 and 0 < n ** m by EXP_POS, 0 < n, from k < n 909 so c <= c * n ** m by arithmetic 910 Thus x n <= c * n ** m 911*) 912val poly_O_has_constant = store_thm( 913 "poly_O_has_constant", 914 ``!m. big_O (K 1) SUBSET poly_O m``, 915 rw[big_O_def, POLY_def, SUBSET_DEF] >> 916 qexists_tac `k` >> 917 qexists_tac `c` >> 918 rpt strip_tac >> 919 `x n <= c` by rw[] >> 920 `c <= c * n ** m` by rw[EXP_POS] >> 921 decide_tac); 922 923(* Theorem: f IN poly_O m ==> !a. (\n. f (a * n)) IN poly_O m *) 924(* Proof: 925 By big_O_def, POLY_def, this is to show: 926 !n. k < n ==> f n <= c * n ** m ==> ?k c. !n. k < n ==> f (a * n) <= c * n ** m 927 Take the same k. 928 If a = 0, 929 Take c = f 0. 930 Then if k < n, then 0 < n by arithmetic 931 so 0 < n ** m by EXP_POS 932 ==> f 0 <= f 0 * n ** m by LE_MULT_CANCEL_LBARE 933 or f (a * n) <= c * n ** m by a * n = 0, c = f 0. 934 If a <> 0, 935 Take c as c * a ** m. 936 Then if k < n, then 0 < n by arithmetic 937 ==> n <= a * n by LE_MULT_CANCEL_LBARE 938 Thus k < a * n 939 ==> f (a * n) 940 <= c * (a * n) ** m by implication 941 = c * a ** m * n ** m by EXP_BASE_MULT 942*) 943val poly_O_multiple = store_thm( 944 "poly_O_multiple", 945 ``!f m. f IN poly_O m ==> !a. (\n. f (a * n)) IN poly_O m``, 946 rw[big_O_def, POLY_def] >> 947 qexists_tac `k` >> 948 Cases_on `a = 0` >| [ 949 qexists_tac `f 0` >> 950 simp[], 951 qexists_tac `c * a ** m` >> 952 rpt strip_tac >> 953 `n <= a * n` by rw[] >> 954 `k < a * n` by decide_tac >> 955 `f (a * n) <= c * (a * n) ** m` by rw[] >> 956 `c * (a * n) ** m = c * a ** m * n ** m` by rw[EXP_BASE_MULT] >> 957 decide_tac 958 ]); 959 960(* Theorem: f1 IN poly_O m /\ f2 IN poly_O m ==> !a b. (\n. f1 (a * n) + f2 (b * n)) IN poly_O m *) 961(* Proof: 962 Let g1 = \n. f1 (a * n), g2 = \n. f2 (b * n). 963 Then g1 IN poly_O m by poly_O_multiple 964 and g2 IN poly_O m by poly_O_multiple 965 Note g1 .+. g2 966 = (\n. f1 (a * n) + f2 (b * n)) by fun_sum_def, FUN_EQ_THM 967 and (g1 .+. g2) IN poly_O m by big_O_add 968*) 969val poly_O_add_linear = store_thm( 970 "poly_O_add_linear", 971 ``!f1 f2 m. f1 IN poly_O m /\ f2 IN poly_O m ==> !a b. (\n. f1 (a * n) + f2 (b * n)) IN poly_O m``, 972 rpt strip_tac >> 973 qabbrev_tac `g1 = \n. f1 (a * n)` >> 974 qabbrev_tac `g2 = \n. f2 (b * n)` >> 975 `g1 IN poly_O m` by rw[poly_O_multiple, Abbr`g1`] >> 976 `g2 IN poly_O m` by rw[poly_O_multiple, Abbr`g2`] >> 977 `(g1 .+. g2) = (\n. f1 (a * n) + f2 (b * n))` by rw[fun_sum_def, FUN_EQ_THM, Abbr`g1`, Abbr`g2`] >> 978 `(g1 .+. g2) IN poly_O m` by rw[big_O_add] >> 979 rfs[]); 980 981(* Theorem: m <= n ==> poly_O m SUBSET poly_O n *) 982(* Proof: 983 By big_O_def, POLY_def, SUBSET_DEF, this is to show: 984 m <= n /\ !n'. k < n' ==> x n' <= c * n' ** m ==> ?c. !n'. k < n' ==> x n' <= c * n' ** n 985 Take the same k, and the same c. 986 Then if k < n', 987 ==> x n' <= c * n' ** m by implication 988 Note n' ** m <= n' ** n by EXP_BASE_LEQ_MONO_IMP, 0 < n' 989 ==> c * n' ** m <= c * n' ** n by LE_MULT_LCANCEL 990 Thus x n' <= c * n' ** n by arithmetic 991*) 992val poly_O_subset = store_thm( 993 "poly_O_subset", 994 ``!m n. m <= n ==> poly_O m SUBSET poly_O n``, 995 rw[big_O_def, POLY_def, SUBSET_DEF] >> 996 qexists_tac `k` >> 997 qexists_tac `c` >> 998 rpt strip_tac >> 999 `x n' <= c * n' ** m` by rw[] >> 1000 `c * n' ** m <= c * n' ** n` by rw[EXP_BASE_LEQ_MONO_IMP] >> 1001 decide_tac); 1002 1003(* Theorem: (poly_O n) |+| (poly_O n) = poly_O n *) 1004(* Proof: by big_O_sum_self, with g = POLY n. *) 1005val poly_O_sum = store_thm( 1006 "poly_O_sum", 1007 ``!n. (poly_O n) |+| (poly_O n) = poly_O n``, 1008 rw[big_O_sum_self]); 1009 1010(* Derive this theorem *) 1011val poly_O_sum = save_thm("poly_O_sum", 1012 big_O_sum_self |> SPEC ``POLY n`` |> GEN_ALL); 1013(* val poly_O_sum = |- !n. poly_O n |+| poly_O n = poly_O n: thm *) 1014 1015(* Theorem: poly_O n |+| poly_O m SUBSET poly_O (MAX n m) *) 1016(* Proof: 1017 Note poly_O n |+| poly_O m SUBSET big_O (POLY n .+. POLY m) by big_O_sum_subset 1018 and big_O (POLY n .+. POLY m) SUBSET poly_O (MAX n m) by big_O_poly_sum 1019 The result follows by SUBSET_TRANS 1020*) 1021val poly_O_sum_subset = store_thm( 1022 "poly_O_sum_subset", 1023 ``!m n. poly_O n |+| poly_O m SUBSET poly_O (MAX n m)``, 1024 metis_tac[big_O_sum_subset, big_O_poly_sum, SUBSET_TRANS]); 1025 1026 1027(* ------------------------------------------------------------------------- *) 1028(* Big O theorem with size *) 1029(* ------------------------------------------------------------------------- *) 1030 1031(* Overload positive function *) 1032val _ = overload_on ("FUN_POS", ``\f. (!x. 0 < f x)``); 1033 1034(* Theorem: FUN_POS f ==> !c. big_O (K c) SUBSET big_O f *) 1035(* Proof: 1036 By big_O_def, this is to show: 1037 !n. k < n ==> x n <= c * c' 1038 ==> ?k c. !n. k < n ==> x n <= c * f n 1039 Take the same k, take (c * c') as c. 1040 Since 0 < f n, so 1 <= f n, hence true. 1041*) 1042val big_O_K_subset = store_thm( 1043 "big_O_K_subset", 1044 ``!f. FUN_POS f ==> !c. big_O (K c) SUBSET big_O f``, 1045 rw[big_O_def, SUBSET_DEF] >> 1046 qexists_tac `k` >> 1047 qexists_tac `c * c'` >> 1048 rw[] >> 1049 `0 < f n /\ x n <= c * c'` by fs[] >> 1050 `1 <= f n` by decide_tac >> 1051 `c * c' <= c * c' * f n` by rw[] >> 1052 decide_tac); 1053 1054(* 1055size_pos |- FUN_POS size 1056*) 1057 1058(* Theorem: MONO f1 /\ f2 IN big_O (K c) ==> ?d. f1 o f2 IN big_O (K d) *) 1059(* Proof: 1060 Note ?k c2. !n. k < n ==> f2 n <= c2 * c by big_O_def, f2 IN big_O (K c) 1061 Take same k, 1062 Then for all n > k, f1 (f2 n) <= f1 (c2 * c) by MONO f1 1063*) 1064val big_O_compose_K = store_thm( 1065 "big_O_compose_K", 1066 ``!f1 f2 c. MONO f1 /\ f2 IN big_O (K c) ==> ?d. f1 o f2 IN big_O (K d)``, 1067 rw[big_O_def] >> 1068 qexists_tac `f1 (c * c')` >> 1069 qexists_tac `k` >> 1070 qexists_tac `1` >> 1071 rw[]); 1072 1073(* Theorem: FUN_POS g ==> (K c) IN big_O g *) 1074(* Proof: 1075 By big_O_def, this is to show: 1076 ?k d. !n. k < n ==> c <= d * g n 1077 Note 0 < g n by FUN_POS g 1078 so 1 <= g n by arithmetic 1079 or c <= c * g n 1080 Take k = 0, same c. 1081*) 1082val big_O_constant = store_thm( 1083 "big_O_constant", 1084 ``!g c. FUN_POS g ==> (K c) IN big_O g``, 1085 rw[big_O_def] >> 1086 map_every qexists_tac [`0`, `c`] >> 1087 rpt strip_tac >> 1088 `0 < g n` by rw[] >> 1089 `1 <= g n` by decide_tac >> 1090 rw[]); 1091 1092(* Theorem: FUN_POS (POLY k o size) *) 1093(* Proof: 1094 This is to show: !n. 0 < (POLY k o size) n 1095 (POLY k o size) n 1096 = (size n) ** k 1097 > 0 by size_pos, EXP_POS 1098*) 1099val POLY_size_pos = store_thm( 1100 "POLY_size_pos", 1101 ``!k. FUN_POS (POLY k o size)``, 1102 rw[POLY_def] >> 1103 rw[size_pos]); 1104 1105(* Theorem: (\n. a * size n + b) IN big_O size *) 1106(* Proof: 1107 By big_O_def, this is to show: 1108 ?k c. !n. k < n ==> b + a * size n <= c * size n 1109 Note 1 <= size n by one_le_size 1110 so b <= b * size n by arithmetic 1111 Then b + a * size n 1112 <= b * size n + a * size n by above 1113 = (b + a) * size n by RIGHT_ADD_DISTRIB 1114 Take k = 0, c = a + b, the result follows. 1115*) 1116val big_O_size_linear = store_thm( 1117 "big_O_size_linear", 1118 ``!a b. (\n. a * size n + b) IN big_O size``, 1119 rw[big_O_def] >> 1120 map_every qexists_tac [`0`, `a + b`] >> 1121 rpt strip_tac >> 1122 simp[RIGHT_ADD_DISTRIB] >> 1123 `1 <= size n` by rw[one_le_size] >> 1124 `b <= b * size n` by rw[] >> 1125 decide_tac); 1126 1127(* Theorem: (\n. a * size n) IN big_O size *) 1128(* Proof: by big_O_size_linear *) 1129val big_O_size_linear_0 = store_thm( 1130 "big_O_size_linear_0", 1131 ``!a. (\n. a * size n) IN big_O size``, 1132 rpt strip_tac >> 1133 `(\n. a * size n) = (\n. a * size n + 0)` by rw[FUN_EQ_THM] >> 1134 `(\n. a * size n + 0) IN big_O size` by rw[big_O_size_linear] >> 1135 fs[]); 1136 1137(* Theorem: (\n. a * size n ** 2 + b * size n + c) IN big_O (POLY 2 o size) *) 1138(* Proof: 1139 By big_O_def and POLY_def, this is to show: 1140 ?k c'. !n. k < n ==> c + (a * size n ** 2 + b * size n) <= c' * size n ** 2 1141 Note 1 <= size n by one_le_size 1142 so b <= b * size n by arithmetic 1143 and b * size <= b * (size n) ** 2 by EXP_2 1144 also c <= c * (size n) **2 by EXP_2 1145 Then c + b * size n + a * (size n) ** 2 1146 <= c * (size n) ** 2 + b * (size n) ** 2 + a * (size n) ** 2 by above 1147 = (c + b + a) * (size n) ** by RIGHT_ADD_DISTRIB 1148 Take k = 0, c' = a + b + c, the result follows. 1149*) 1150val big_O_size_quadratic = store_thm( 1151 "big_O_size_quadratic", 1152 ``!a b c. (\n. a * size n ** 2 + b * size n + c) IN big_O (POLY 2 o size)``, 1153 rw[big_O_def, POLY_def] >> 1154 map_every qexists_tac [`0`, `a + b + c`] >> 1155 rpt strip_tac >> 1156 simp[RIGHT_ADD_DISTRIB] >> 1157 `1 <= size n` by rw[one_le_size] >> 1158 `b * size n <= b * (size n * size n)` by rw[] >> 1159 `b * size n <= b * (size n) ** 2` by metis_tac[EXP_2] >> 1160 `c <= c * (size n * size n)` by rw[] >> 1161 `c <= c * (size n) ** 2` by metis_tac[EXP_2] >> 1162 decide_tac); 1163 1164(* Theorem: (\n. a * size n ** 2 ) IN big_O (POLY 2 o size) *) 1165(* Proof: by big_O_size_quadratic *) 1166val big_O_size_quadratic_0 = store_thm( 1167 "big_O_size_quadratic_0", 1168 ``!a. (\n. a * size n ** 2) IN big_O (POLY 2 o size)``, 1169 rpt strip_tac >> 1170 `(\n. a * (size n) ** 2) = (\n. a * (size n) ** 2 + 0 * size n + 0)` by rw[FUN_EQ_THM] >> 1171 `(\n. a * (size n) ** 2 + 0 * size n + 0) IN big_O (POLY 2 o size)` by rw[big_O_size_quadratic] >> 1172 fs[]); 1173 1174(* Theorem: (\n. a * size n ** 2 + b * size n) IN big_O (POLY 2 o size) *) 1175(* Proof: by big_O_size_quadratic *) 1176val big_O_size_quadratic_1 = store_thm( 1177 "big_O_size_quadratic_1", 1178 ``!a b. (\n. a * size n ** 2 + b * size n) IN big_O (POLY 2 o size)``, 1179 rpt strip_tac >> 1180 `(\n. a * (size n) ** 2 + b * size n) = (\n. a * (size n) ** 2 + b * size n + 0)` by rw[FUN_EQ_THM] >> 1181 `(\n. a * (size n) ** 2 + b * size n + 0) IN big_O (POLY 2 o size)` by rw[big_O_size_quadratic] >> 1182 fs[]); 1183 1184(* Theorem: (\n. a * size n ** 2 + b) IN big_O (POLY 2 o size) *) 1185(* Proof: by big_O_size_quadratic *) 1186val big_O_size_quadratic_2 = store_thm( 1187 "big_O_size_quadratic_2", 1188 ``!a b. (\n. a * size n ** 2 + b) IN big_O (POLY 2 o size)``, 1189 rpt strip_tac >> 1190 `(\n. a * (size n) ** 2 + b) = (\n. a * (size n) ** 2 + 0 * size n + b)` by rw[FUN_EQ_THM] >> 1191 `(\n. a * (size n) ** 2 + 0 * size n + b) IN big_O (POLY 2 o size)` by rw[big_O_size_quadratic] >> 1192 fs[]); 1193 1194(* Theorem: (!n. k < n ==> f1 n <= f2 n) /\ f2 IN big_O g ==> f1 IN big_O g *) 1195(* Proof: 1196 By big_O_def, this is to show: 1197 ?t c. !n. t < n ==> f1 n <= c * g n 1198 Note ?h c. !n. h < n ==> f2 n <= c * g n by big_O_def, f2 IN big_O g 1199 Take t = MAX k h, and the same c. 1200 Note k <= t /\ h <= t by MAX_IS_MAX 1201 so t < n 1202 ==> f1 n <= f2 n /\ f2 n <= c * g n 1203 ==> f1 n <= c * g n by LESS_EQ_TRANS 1204*) 1205val big_O_dominance = store_thm( 1206 "big_O_dominance", 1207 ``!f1 f2 g k. (!n. k < n ==> f1 n <= f2 n) /\ f2 IN big_O g ==> f1 IN big_O g``, 1208 rw[big_O_def] >> 1209 qexists_tac `MAX k k'` >> 1210 qexists_tac `c` >> 1211 rpt strip_tac >> 1212 `k <= MAX k k' /\ k' <= MAX k k'` by rw[] >> 1213 `k < n /\ k' < n` by decide_tac >> 1214 metis_tac[LESS_EQ_TRANS]); 1215 1216(* ------------------------------------------------------------------------- *) 1217(* Polynomial Complexity Class *) 1218(* ------------------------------------------------------------------------- *) 1219 1220(* Define polynomial complexity class based on (size ** n) *) 1221val _ = overload_on("O_poly", ``\n. big_O ((POLY n) o size)``); 1222 1223 1224(* Theorem: f IN O_poly m <=> ?h k. (!n. h < n ==> f n <= k * (size n) ** m) *) 1225(* Proof: by big_O_def, POLY_def *) 1226val O_poly_thm = store_thm( 1227 "O_poly_thm", 1228 ``!f m. f IN O_poly m <=> ?h k. (!n. h < n ==> f n <= k * (size n) ** m)``, 1229 rw[big_O_def, POLY_def]); 1230 1231(* Theorem: f IN O_poly m <=> ?h k. 0 < k /\ (!n. h < n ==> f n <= k * (size n) ** m) *) 1232(* Proof: 1233 If part: f IN O_poly m ==> ?h k. 0 < k /\ !n. h < n ==> f n <= k * size n ** m 1234 Note ?h k. (!n. h < n ==> f n <= k * (size n) ** m) by O_poly_thm 1235 Take same h, but use (SUC k). 1236 Then k * (size n) ** m <= SUC k * (size n) ** m by k < SUC k 1237 The result follows. 1238 Only-if part: 0 < k /\ !n. h < n ==> f n <= k * size n ** m ==> f IN O_poly m 1239 True by O_poly_thm. 1240*) 1241val O_poly_good = store_thm( 1242 "O_poly_good", 1243 ``!f m. f IN O_poly m <=> ?h k. 0 < k /\ (!n. h < n ==> f n <= k * (size n) ** m)``, 1244 rw[EQ_IMP_THM] >| [ 1245 `?h k. (!n. h < n ==> f n <= k * (size n) ** m)` by rw[GSYM O_poly_thm] >> 1246 qexists_tac `h` >> 1247 qexists_tac `SUC k` >> 1248 rw_tac std_ss[] >> 1249 `f n <= k * size n ** m` by fs[] >> 1250 `k * size n ** m <= SUC k * size n ** m` by fs[] >> 1251 decide_tac, 1252 metis_tac[O_poly_thm] 1253 ]); 1254 1255(* O_poly n is the same as big_O ((POLY n) o ulog) *) 1256 1257(* Theorem: O_poly n = big_O ((POLY n) o ulog) *) 1258(* Proof: 1259 If part: x IN O_poly n ==> x IN big_O ((POLY n) o ulog) 1260 Expand by definitions, 1261 x n' <= k * size n' ** n 1262 <= k * (1 + ulog n') ** n by size_ulog 1263 <= k * (ulog n' + ulog n') ** n by ulog_pos, 1 < n' 1264 = k * (2 * ulog n') ** n by arithmetic 1265 = (k * 2 ** n) * (ulog n') ** n by EXP_BASE_MULT 1266 Take k = MAX 1 h, and c = k * 2 ** n. 1267 Only-if part: x IN big_O ((POLY n) o ulog) ==> x IN O_poly n 1268 Expand by definitions, 1269 x n' <= c * ulog n' ** n 1270 <= c * size n' ** n by size_ulog 1271*) 1272val O_poly_eq_O_poly_ulog = store_thm( 1273 "O_poly_eq_O_poly_ulog", 1274 ``!n. O_poly n = big_O ((POLY n) o ulog)``, 1275 rw[EXTENSION, O_poly_thm, big_O_def, POLY_def] >> 1276 rw[EQ_IMP_THM] >| [ 1277 qexists_tac `MAX 1 h` >> 1278 qexists_tac `k * 2 ** n` >> 1279 rpt strip_tac >> 1280 `1 < n'` by metis_tac[MAX_LT] >> 1281 `0 < ulog n'` by rw[] >> 1282 `1 + ulog n' <= 2 * ulog n'` by decide_tac >> 1283 `size n' <= 1 + ulog n'` by rw[size_ulog] >> 1284 `x n' <= k * size n' ** n` by fs[] >> 1285 `k * size n' ** n <= k * (2 * ulog n') ** n` by rw[] >> 1286 `k * (2 * ulog n') ** n = k * 2 ** n * ulog n' ** n` by rw[EXP_BASE_MULT] >> 1287 decide_tac, 1288 qexists_tac `k` >> 1289 qexists_tac `c` >> 1290 rpt strip_tac >> 1291 `x n' <= c * ulog n' ** n` by fs[] >> 1292 `c * ulog n' ** n <= c * size n' ** n` by rw[size_ulog] >> 1293 decide_tac 1294 ]); 1295 1296(* Theorem: 0 < c ==> (big_O (POLY 1 o (\x. c * (size x) ** n)) = O_poly n) *) 1297(* Proof: by big_O_def, POLY_def, O_poly_thm *) 1298val big_O_poly_eq_O_poly = store_thm( 1299 "big_O_poly_eq_O_poly", 1300 ``!c n. 0 < c ==> (big_O (POLY 1 o (\x. c * (size x) ** n)) = O_poly n)``, 1301 rw[big_O_def, POLY_def, O_poly_thm, EXTENSION] >> 1302 rw[EQ_IMP_THM] >- 1303 metis_tac[] >> 1304 qexists_tac `h` >> 1305 qexists_tac `k` >> 1306 rw[] >> 1307 `1 <= c` by decide_tac >> 1308 `x n' <= k * size n' ** n` by rw[] >> 1309 `k * size n' ** n <= c * (k * size n' ** n)` by rw[] >> 1310 decide_tac); 1311 1312(* Theorem: big_O (\n. (size n) ** k) SUBSET big_O (\n. (ulog n) ** k) *) 1313(* Proof: 1314 Expand by big_O_def, ulog_by_size, SUBSET_DEF, this is to show: 1315 !n. k' < n ==> f n <= c * size n ** k 1316 ==> ?k' c. 1317 !n. k' < n ==> f n <= c * (if perfect_power n 2 then size n - 1 else size n) ** k 1318 1319 Take (MAX 1 k') as k', (c * 2 ** k) as c. 1320 This is to show: 1321 (1) perfect_power n 2 ==> f n <= c * 2 ** k * (size n - 1) ** k 1322 Note ?e. n = 2 ** e by perfect_power_def 1323 and size n = 1 + e by size_2_exp 1324 so size n - 1 = e by arithmetic 1325 Note 1 < n /\ k' < n by MAX_DEF 1326 so 0 < e by EXP_0, n = 2 ** e, 1 < n 1327 or 1 + e <= 2 * e by arithmetic 1328 By implication, 1329 f n <= c * (1 + e) ** k by k' < n 1330 <= c * (2 * e) ** k by EXP_EXP_LE_MONO 1331 = c * 2 ** k * e ** k by EXP_BASE_MULT 1332 = c * 2 ** k * (size n - 1) ** k 1333 1334 (2) ~perfect_power n 2 ==> f n <= c * 2 ** k * (size n) ** k 1335 Note 1 < n /\ k' < n by MAX_DEF 1336 By implication, 1337 f n <= c * size n ** k by k' < n 1338 <= c * 2 ** k * size n ** k by EXP_POS, 0 < 2 ** k 1339*) 1340val big_O_size_subset_big_O_ulog = store_thm( 1341 "big_O_size_subset_big_O_ulog", 1342 ``!k. big_O (\n. (size n) ** k) SUBSET big_O (\n. (ulog n) ** k)``, 1343 rw[big_O_def, ulog_by_size, SUBSET_DEF] >> 1344 qexists_tac `MAX 1 k'` >> 1345 qexists_tac `c * 2 ** k` >> 1346 rw[] >| [ 1347 `?e. n = 2 ** e` by rw[GSYM perfect_power_def] >> 1348 `size n = 1 + e` by rw[size_2_exp] >> 1349 `0 < e` by metis_tac[EXP_0, LESS_NOT_EQ, NOT_ZERO] >> 1350 `1 + e <= 2 * e` by decide_tac >> 1351 `x n <= c * (1 + e) ** k` by metis_tac[] >> 1352 `c * (1 + e) ** k <= c * (2 * e) ** k` by rw[] >> 1353 `c * (2 * e) ** k = c * 2 ** k * e ** k` by rw[EXP_BASE_MULT] >> 1354 rw[], 1355 `x n <= c * size n ** k` by metis_tac[] >> 1356 `c * size n ** k <= c * 2 ** k * size n ** k` by rw[] >> 1357 decide_tac 1358 ]); 1359 1360(* Theorem: big_O (\n. ulog n ** k) SUBSET big_O (\n. size n ** k) *) 1361(* Proof: 1362 Expand by big_O_def, size_by_ulog, SUBSET_DEF, this is to show: 1363 !n. k' < n ==> f n <= c * ulog n ** k 1364 ==> ?k' c. 1365 !n. k' < n ==> f n <= c * (if n = 0 \/ perfect_power n 2 then 1 + ulog n else ulog n) ** k 1366 Take same k' and c. 1367 If perfect_power n 2, 1368 By implication, 1369 f n <= c * ulog n ** k by k' < n 1370 <= c * (ulog n + 1) ** k by EXP_EXP_LE_MONO 1371 If ~perfect_power n 2, 1372 By implication, 1373 f n <= c * ulog n ** k by k' < n 1374*) 1375val big_O_ulog_subset_big_O_size = store_thm( 1376 "big_O_ulog_subset_big_O_size", 1377 ``!k. big_O (\n. ulog n ** k) SUBSET big_O (\n. size n ** k)``, 1378 rw[big_O_def, size_by_ulog, SUBSET_DEF] >> 1379 qexists_tac `k'` >> 1380 qexists_tac `c` >> 1381 rw[] >> 1382 `x n <= c * ulog n ** k` by metis_tac[] >> 1383 `c * (ulog n) ** k <= c * (ulog n + 1) ** k` by rw[] >> 1384 decide_tac); 1385 1386(* Theorem: big_O (\n. size n ** k) = big_O (\n. ulog n ** k) *) 1387(* Proof: 1388 By SUBSET_ANTISYM, this is to show: 1389 (1) big_O (\n. size n ** k) SUBSET big_O (\n. ulog n ** k) 1390 This is true by big_O_size_subset_big_O_ulog. 1391 (2) big_O (\n. ulog n ** k) SUBSET big_O (\n. size n ** k) 1392 This is true by big_O_ulog_subset_big_O_size. 1393*) 1394val big_O_size_eq_big_O_ulog = store_thm( 1395 "big_O_size_eq_big_O_ulog", 1396 ``!k. big_O (\n. size n ** k) = big_O (\n. ulog n ** k)``, 1397 rw[big_O_size_subset_big_O_ulog, big_O_ulog_subset_big_O_size, SUBSET_ANTISYM]); 1398 1399 1400(* ------------------------------------------------------------------------- *) 1401 1402(* export theory at end *) 1403val _ = export_theory(); 1404 1405(*===========================================================================*) 1406