1(* ------------------------------------------------------------------------- *) 2(* Bit Size for Numbers *) 3(* ------------------------------------------------------------------------- *) 4 5(*===========================================================================*) 6 7(* add all dependent libraries for script *) 8open HolKernel boolLib bossLib Parse; 9 10(* declare new theory at start *) 11val _ = new_theory "bitsize"; 12 13(* ------------------------------------------------------------------------- *) 14 15 16 17(* val _ = load "jcLib"; *) 18open jcLib; 19 20(* Get dependent theories in lib *) 21(* val _ = load "helperFunctionTheory"; (* has helperNum, helperSet *) *) 22(* val _ = load "helperListTheory"; *) 23open pred_setTheory arithmeticTheory dividesTheory gcdTheory; 24open helperNumTheory helperSetTheory helperListTheory helperFunctionTheory; (* for DIV_EQ_0 *) 25 26(* open dependent theories *) 27open listTheory rich_listTheory; 28 29(* val _ = load "logPowerTheory"; *) 30open logrootTheory logPowerTheory; (* for LOG_1, ulog *) 31 32 33(* ------------------------------------------------------------------------- *) 34(* Bit Size for Numbers Documentation *) 35(* ------------------------------------------------------------------------- *) 36(* Type and Overload: 37*) 38(* Definitions and Theorems (# are exported): 39 40 Helper Theorems: 41 42 Encoding and Decoding Binary Bits: 43 decode_def |- decode [] = 0 /\ !h t. decode (h::t) = h + TWICE (decode t) 44 encode_def |- encode 0 = [] /\ !n. encode (SUC n) = SUC n MOD 2::encode (HALF (SUC n)) 45 encode_eqn |- !n. 0 < n ==> encode n = n MOD 2::encode (HALF n) 46 encode_0 |- encode 0 = [] 47 encode_1 |- encode 1 = [1] 48 encode_2 |- encode 2 = [0; 1] 49 decode_encode_eq_id |- !n. decode (encode n) = n 50 decode_all_zero |- !l. EVERY (\x. x = 0) l ==> (decode l = 0) 51 decode_genlist_zero |- !m. decode (GENLIST (K 0) m) = 0 52 decode_nil |- decode [] = 0 53 decode_cons |- !h t. decode (h::t) = h + TWICE (decode t) 54 decode_sing |- !x. decode [x] = x 55 decode_snoc |- !x l. decode (SNOC x l) = decode l + x * 2 ** LENGTH l 56 57 Binary Representation: 58 binary_def |- !n. binary n = if n = 0 then [0] else encode n 59 binary_0 |- binary 0 = [0] 60 binary_1 |- binary 1 = [1] 61 binary_length |- !n. LENGTH (binary n) = if n = 0 then 1 else 1 + LOG2 n 62 63 Size of Binary Representation: 64 size_def |- !n. size n = if n = 0 then 1 else if n = 1 then 1 65 else SUC (size (HALF n)) 66 size_alt |- !n. size n = if n <= 1 then 1 else 1 + size (HALF n) 67# size_pos |- !n. 0 < size n 68# size_nonzero |- !n. size n <> 0 69 one_le_size |- !n. 1 <= size n 70# size_0 |- size 0 = 1 71# size_1 |- size 1 = 1 72# size_2 |- size 2 = 2 73 size_by_halves |- !n. size n = if n = 0 then 1 else halves n 74 size_by_LOG2 |- !n. size n = if n = 0 then 1 else 1 + LOG2 n 75 size_ulog |- !n. ulog n <= size n /\ size n <= 1 + ulog n 76 size_le_ulog |- !n. 1 < n ==> size n <= TWICE (ulog n) 77 size_max_1_n |- !n. size (MAX 1 n) = size n 78 max_1_size_n |- !n. size n = MAX 1 (size n) 79 size_monotone_lt |- !m n. m < n ==> size m <= size n 80 size_monotone_le |- !m n. m <= n ==> size m <= size n 81 size_eq_1 |- !n. size n = 1 <=> n = 0 \/ n = 1 82 size_mult_two_power |- !n m. size (n * 2 ** m) = size n + if n = 0 then 0 else m 83 size_twice |- !n. size (TWICE n) = size n + if n = 0 then 0 else 1 84 size_2_exp |- !n. size (2 ** n) = 1 + n 85 size_half_SUC |- !n. 1 < n ==> SUC (size (HALF n)) = size n 86 size_half |- !n. 1 < n ==> size (HALF n) = size n - 1 87 size_div_2_exp |- !n k. size (n DIV 2 ** k) = if n < 2 ** k then 1 else size n - k 88 size_exp |- !n. n < 2 ** size n 89 size_property |- !n. 0 < n ==> n < 2 ** size n /\ 2 ** size n <= TWICE n 90 size_property_alt |- !n. n < 2 ** size n /\ 2 ** size n <= TWICE (MAX 1 n) 91 size_unique |- !n m. 2 ** m <= TWICE n /\ n < 2 ** m ==> size n = m 92 size_thm |- !n. 0 < n ==> !m. size n = m <=> 2 ** m <= TWICE n /\ n < 2 ** m 93 size_eq_self |- !n. (size n = n) <=> (n = 1) \/ (n = 2) 94 size_le |- !n. 0 < n ==> size n <= n 95 size_lt |- !n. 2 < n ==> size n < n 96 size_le_self |- !n. 0 < n ==> size n <= n 97 size_size_le |- !n. size (size n) <= size n 98 size_by_ulog |- !n. size n = if n = 0 \/ perfect_power n 2 then 1 + ulog n else ulog n 99 size_by_ulog_alt |- !n. size n = ulog n + if n = 0 \/ perfect_power n 2 then 1 else 0 100 size_by_ulog_eqn |- !n. size n = if n = 0 then 1 else ulog n + if perfect_power n 2 then 1 else 0 101 ulog_by_size |- !n. ulog n = if n = 0 \/ perfect_power n 2 then size n - 1 else size n 102 ulog_by_size_alt |- !n. ulog n = size n - if n = 0 \/ perfect_power n 2 then 1 else 0 103 ulog_by_size_eqn |- !n. ulog n = if n = 0 then 0 else size n - if perfect_power n 2 then 1 else 0 104 halves_by_size |- !n. halves n = if n = 0 then 0 else size n 105 size_genlist_half |- !k. 1 < k ==> GENLIST (\j. k DIV 2 ** j) (size k) = 106 k::GENLIST (\j. HALF k DIV 2 ** j) (size (HALF k)) 107 size_genlist_twice |- !n k. 1 < k ==> GENLIST (\j. n * 2 ** j) (size k) = 108 n::GENLIST (\j. TWICE n * 2 ** j) (size (HALF k)) 109 size_genlist_square |- !n k. 1 < k ==> GENLIST (\j. n ** 2 ** j) (size k) = 110 n::GENLIST (\j. SQ n ** 2 ** j) (size (HALF k)) 111 size_genlist_select |- !n k. 1 < k ==> 112 GENLIST (\j. if EVEN (k DIV 2 ** j) then 0 else n * 2 ** j) (size k) = 113 (if EVEN k then 0 else n):: 114 GENLIST (\j. if EVEN (HALF k DIV 2 ** j) then 0 else TWICE n * 2 ** j) (size (HALF k)) 115 size_mult_two_power_upper 116 |- !m n. size (n * 2 ** m) <= size n + m 117 size_add_upper |- !m n. size (m + n) <= 1 + size (MAX m n) 118 size_mult_upper |- !m n. size (m * n) <= size m + size n 119 size_sq_upper |- !n. size (SQ n) <= TWICE (size n) 120 size_upper |- !n. size n <= 1 + n 121 size_add1 |- !n. size (n + 1) <= 1 + size n 122 size_gt_1 |- !n. 1 < n ==> 1 < size n 123 size_max |- !m n. size (MAX m n) = MAX (size m) (size n) 124 size_min |- !m n. size (MIN m n) = MIN (size m) (size n) 125 size_exp_upper |- !m n. size (m ** n) <= MAX 1 (n * size m) 126 size_exp_upper_alt |- !m n. 0 < n ==> size (m ** n) <= n * size m 127 size_exp_two_power_upper |- !m n. size (n ** 2 ** size m) <= TWICE (MAX 1 m) * size n 128 size_exp_two_power_le |- !n m j. 0 < n /\ j < size n ==> size (m ** 2 ** j) <= n * size m 129 size_exp_base_le |- !n m b. m <= n ==> size (b ** m) <= size (b ** n) 130 size_exp_exp_le |- !a b n. a <= b ==> size (a ** n) <= size (b ** n) 131 132 Encode to Fixed Binary Bits: 133 to_bits_def |- !n. to_bits n 0 = [] /\ !n m. to_bits n (SUC m) = n MOD 2::to_bits (HALF n) m 134 to_bits_n_0 |- !n. to_bits n 0 = [] 135 to_bits_n_SUC |- !n m. to_bits n (SUC m) = n MOD 2::to_bits (HALF n) m 136 to_bits_snoc |- !n m. to_bits n (SUC m) = SNOC ((n DIV 2 ** m) MOD 2) (to_bits n m) 137 to_bits_0_m |- !m. to_bits 0 m = GENLIST (K 0) m 138 to_bits_n_m |- !m n. to_bits n m = GENLIST (\j. (n DIV 2 ** j) MOD 2) m 139 to_bits_length |- !m n. LENGTH (to_bits n m) = m 140 to_bits_element |- !k m n. k < m ==> EL k (to_bits n m) = (n DIV 2 ** k) MOD 2 141 decode_to_bits_eq_mod |- !m n. decode (to_bits n m) = n MOD 2 ** m 142 143*) 144 145(* Eliminate parenthesis around equality *) 146val _ = ParseExtras.tight_equality(); 147 148(* ------------------------------------------------------------------------- *) 149(* Helper Theorems *) 150(* ------------------------------------------------------------------------- *) 151 152(* ------------------------------------------------------------------------- *) 153(* Encoding and Decoding Binary Bits *) 154(* ------------------------------------------------------------------------- *) 155 156(* Decode a binary list *) 157val decode_def = Define` 158 (decode [] = 0) /\ 159 (decode (h::t) = h + 2 * decode t) 160`; 161 162(* 163> EVAL ``decode [0; 1]``; 164val it = |- decode [0; 1] = 2: thm 165> EVAL ``decode [1; 1]``; 166val it = |- decode [1; 1] = 3: thm 167> EVAL ``decode [1; 1; 0]``; 168val it = |- decode [1; 1; 0] = 3: thm 169> EVAL ``decode [1; 1; 0; 1]``; 170val it = |- decode [1; 1; 0; 1] = 11: thm 171> EVAL ``decode [1; 1; 1; 0]``; 172val it = |- decode [1; 1; 1; 0] = 7: thm 173> EVAL ``decode [0]``; 174val it = |- decode [0] = 0: thm 175> EVAL ``decode [1]``; 176val it = |- decode [1] = 1: thm 177*) 178 179(* Encode a number to a binary list *) 180val encode_def = Define` 181 (encode 0 = []) /\ 182 (encode (SUC n) = (SUC n) MOD 2 :: encode (HALF (SUC n))) 183`; 184 185(* Theorem: 0 < n ==> (encode n = n MOD 2 :: encode (HALF n)) *) 186(* Proof: 187 Note 0 < n means n <> 0 by NOT_ZERO_LT_ZERO 188 Thus ?k. n = SUC k by num_CASES 189 The result follows by encode_def 190*) 191val encode_eqn = store_thm( 192 "encode_eqn", 193 ``!n. 0 < n ==> (encode n = n MOD 2 :: encode (HALF n))``, 194 metis_tac[encode_def, num_CASES, NOT_ZERO_LT_ZERO]); 195 196(* 197> EVAL ``encode 2``; 198val it = |- encode 2 = [0; 1]: thm 199> EVAL ``encode 3``; 200val it = |- encode 3 = [1; 1]: thm 201> EVAL ``encode 11``; 202val it = |- encode 11 = [1; 1; 0; 1]: thm 203> EVAL ``decode (encode 11)``; 204val it = |- decode (encode 11) = 11: thm 205> EVAL ``encode 1``; 206val it = |- encode 1 = [1]: thm 207> EVAL ``encode 0``; 208val it = |- encode 0 = []: thm 209*) 210 211(* Extract theorems *) 212val encode_0 = save_thm("encode_0", encode_def |> CONJUNCT1); 213val encode_1 = save_thm("encode_1", encode_def |> CONJUNCT2 |> SPEC ``0`` |> SIMP_RULE arith_ss[encode_0]); 214val encode_2 = save_thm("encode_2", encode_def |> CONJUNCT2 |> SPEC ``1`` |> SIMP_RULE arith_ss[encode_1]); 215 216(* 217val encode_0 = |- encode 0 = []: thm 218val encode_1 = |- encode 1 = [1]: thm 219val encode_2 = |- encode 2 = [0; 1]: thm 220*) 221 222(* Theorem: decode (encode n) = n *) 223(* Proof: 224 By complete induction on n. 225 Base: n = 0 ==> decode (encode n) = n 226 decode (encode 0) 227 = decode [] by encode_def 228 = 0 by decode_def 229 Step: !m. m < n ==> (decode (encode m) = m) ==> 230 n <> 0 ==> decode (encode n) = n 231 Note ?m. n = SUC m by num_CASES 232 and HALF n < n by HALF_LESS, 0 < n 233 decode (encode n) 234 = decode (n MOD 2::encode (HALF n)) by encode_def 235 = n MOD 2 + 2 * decode (encode (HALF n)) by decode_def 236 = n MOD 2 + 2 * (HALF n) by induction hypothesis 237 = (HALF n) * 2 + (n MOD 2) by arithmetic 238 = n by DIVISION 239*) 240val decode_encode_eq_id = store_thm( 241 "decode_encode_eq_id", 242 ``!n. decode (encode n) = n``, 243 completeInduct_on `n` >> 244 Cases_on `n = 0` >- 245 rw_tac std_ss[encode_def, decode_def] >> 246 `?m. n = SUC m` by metis_tac[num_CASES] >> 247 `HALF n < n` by rw[HALF_LESS] >> 248 `decode (encode n) = decode (n MOD 2::encode (HALF n))` by rw[encode_def] >> 249 `_ = n MOD 2 + 2 * decode (encode (HALF n))` by rw[decode_def] >> 250 `_ = n MOD 2 + 2 * (HALF n)` by rw[] >> 251 `_ = (HALF n) * 2 + (n MOD 2)` by rw[] >> 252 `_ = n` by rw[DIVISION] >> 253 rw[]); 254 255(* Theorem: EVERY (\x. x = 0) l ==> (decode l = 0) *) 256(* Proof: 257 By induction on l. 258 Base: decode [] = 0, true by decode_def 259 Step: EVERY (\x. x = 0) l ==> (decode l = 0) ==> 260 !h. EVERY (\x. x = 0) (h::l) ==> (decode (h::l) = 0) 261 EVERY (\x. x = 0) (h::l) 262 = (h = 0) /\ EVERY (\x. x = 0) l by EVERY_DEF 263 = (h = 0) /\ (decode l = 0) by induction hypothesis 264 = (h + 2 * decode l = 0) by arithmetic 265 = (decode (h::l) = 0) by decode_def 266*) 267val decode_all_zero = store_thm( 268 "decode_all_zero", 269 ``!l. EVERY (\x. x = 0) l ==> (decode l = 0)``, 270 Induct >> 271 rw[decode_def] >> 272 rw[decode_def]); 273 274(* Theorem: decode (GENLIST (K 0) m) = 0 *) 275(* Proof: 276 Note EVERY (\x. x = 0) (GENLIST (K 0) m) by EVERY_GENLIST 277 ==> decode (GENLIST (K 0) m) = 0 by decode_all_zero 278*) 279val decode_genlist_zero = store_thm( 280 "decode_genlist_zero", 281 ``!m. decode (GENLIST (K 0) m) = 0``, 282 rw[decode_all_zero, EVERY_GENLIST]); 283 284(* Extract theorems from definition *) 285val decode_nil = save_thm("decode_nil", decode_def |> CONJUNCT1); 286(* val decode_nil = |- decode [] = 0: thm *) 287 288val decode_cons = save_thm("decode_cons", decode_def |> CONJUNCT2); 289(* val decode_cons = |- !h t. decode (h::t) = h + TWICE (decode t): thm *) 290 291(* Theorem: decode [x] = x *) 292(* Proof: by decode_def *) 293val decode_sing = store_thm( 294 "decode_sing", 295 ``!x. decode [x] = x``, 296 rw_tac std_ss[decode_def]); 297 298(* 299> EVAL ``decode [0;0;1]``; 300val it = |- decode [0; 0; 1] = 4: thm 301> EVAL ``decode [0;0;1;1]``; 302val it = |- decode [0; 0; 1; 1] = 12: thm 303*) 304 305(* Theorem: decode (SNOC x l) = decode l + x * 2 ** (LENGTH l) *) 306(* Proof: 307 By induction on l. 308 Base: decode (SNOC x []) = decode [] + x * 2 ** LENGTH [] 309 decode (SNOC x []) 310 = decode [x] by SNOC_NIL 311 = x by decode_sing 312 = 0 + x * 1 by arithmetic 313 = decode [] + x * 1 by decode_nil 314 = decode [] + x * 2 ** 0 by EXP_0 315 = decode [] + x * 2 ** (LENGTH []) by LENGTH_NIL 316 Step: decode (SNOC x l) = decode l + x * 2 ** LENGTH l ==> 317 !h. decode (SNOC x (h::l)) = decode (h::l) + x * 2 ** LENGTH (h::l) 318 decode (SNOC x (h::l)) 319 = decode (h::SNOC x l) by SNOC_CONS 320 = h + 2 * decode (SNOC x l) by decode_cons 321 = h + 2 * (decode l + x * 2 ** LENGTH l) by induction hypothesis 322 = (h + 2 * decode l) + x * 2 * 2 ** LENGTH l by arithmetic 323 = decode (h::l) + x * 2 ** SUC (LENGTH l) by decode_cons, EXP 324 = decode (h::l) + x * 2 ** LENGTH (h::l) by LENGTH 325*) 326val decode_snoc = store_thm( 327 "decode_snoc", 328 ``!x l. decode (SNOC x l) = decode l + x * 2 ** (LENGTH l)``, 329 strip_tac >> 330 Induct >- 331 rw[decode_def] >> 332 rw[decode_def, SNOC_CONS, EXP]); 333 334(* ------------------------------------------------------------------------- *) 335(* Binary Representation *) 336(* ------------------------------------------------------------------------- *) 337 338(* Correct binary list of a number *) 339val binary_def = Define` 340 binary n = if n = 0 then [0] else encode n 341`; 342(* 343> EVAL ``binary 0``; 344val it = |- binary 0 = [0]: thm 345> EVAL ``binary 1``; 346val it = |- binary 1 = [1]: thm 347> EVAL ``binary 2``; 348val it = |- binary 2 = [0; 1]: thm 349> EVAL ``binary 3``; 350val it = |- binary 3 = [1; 1]: thm 351> EVAL ``binary 4``; 352val it = |- binary 4 = [0; 0; 1]: thm 353> EVAL ``binary 5``; 354val it = |- binary 5 = [1; 0; 1]: thm 355*) 356 357val binary_0 = save_thm("binary_0", EVAL ``binary 0``); 358(* val binary_0 = |- binary 0 = [0]: thm *) 359val binary_1 = save_thm("binary_1", EVAL ``binary 1``); 360(* val binary_1 = |- binary 1 = [1]: thm *) 361 362(* Theorem: LENGTH (binary n) = if n = 0 then 1 else 1 + LOG2 n *) 363(* Proof: 364 If n = 0, 365 LENGTH (binary 0) 366 = LENGTH [0] by binary_0 367 = 1 by LENGTH 368 If n <> 0, 369 By complete induction on n. 370 Note 0 < n by n <> 0 371 Thus HALF n < n by HALF_LESS 372 Let m = HALF n. 373 374 If m = 0, 375 Then n = 1 by HALF_EQ_0 376 LENGTH (binary 1) 377 = LENGTH [1] by binary_1 378 = 1 by LENGTH 379 = 1 + 0 by ADD_0 380 = 1 + LOG2 1 by LOG2_1 381 If m <> 0, 382 LENGTH (binary n) 383 LENGTH (encode n) by binary_def 384 = LENGTH (n MOD 2 :: encode m) by encode_eqn, 0 < n 385 = LENGTH (encode m) + 1 by LENGTH 386 = LOG2 m + 1 + 1 by induction hypothesis, m < n 387 = 1 + (1 + LOG2 m) by arithmetic 388 = 1 + LOG2 n by LOG_DIV 389*) 390val binary_length = store_thm( 391 "binary_length", 392 ``!n. LENGTH (binary n) = if n = 0 then 1 else 1 + LOG2 n``, 393 rw[binary_def] >> 394 completeInduct_on `n` >> 395 rpt strip_tac >> 396 `HALF n < n` by rw[HALF_LESS] >> 397 qabbrev_tac `m = HALF n` >> 398 Cases_on `m = 0` >| [ 399 `n = 1` by metis_tac[HALF_EQ_0] >> 400 simp[] >> 401 rw[encode_1, LOG2_1], 402 fs[encode_eqn, LOG_DIV, Abbr`m`] 403 ]); 404 405(* ------------------------------------------------------------------------- *) 406(* Size of Binary Representation *) 407(* ------------------------------------------------------------------------- *) 408 409(* Define number of bits of a number, recursively. *) 410val size_def = Define` 411 size n = if n = 0 then 1 else if n = 1 then 1 else SUC (size (HALF n)) 412`; 413(* Both 0 and 1 needs no halving to count. *) 414 415(* 416> size_def |> SPEC_ALL |> SIMP_RULE (srw_ss()) [ADD1] |> GEN_ALL; 417val it = |- !n. size n = if n = 0 then 1 else if n = 1 then 1 else size (HALF n) + 1: thm 418*) 419 420(* Theorem: size n = if n <= 1 then 1 else 1 + size (HALF n) *) 421(* Proof: by size_def *) 422val size_alt = store_thm( 423 "size_alt", 424 ``!n. size n = if n <= 1 then 1 else 1 + size (HALF n)``, 425 rw[Once size_def]); 426 427(* Theorem: 0 < size n *) 428(* Proof: by size_def *) 429val size_pos = store_thm( 430 "size_pos[simp]", 431 ``!n. 0 < size n``, 432 rw[Once size_def]); 433 434(* Theorem: size n <> 0 *) 435(* Proof: by size_pos *) 436val size_nonzero = store_thm( 437 "size_nonzero[simp]", 438 ``!n. size n <> 0``, 439 metis_tac[size_pos, NOT_ZERO_LT_ZERO]); 440 441(* Theorem: 1 <= size n *) 442(* Proof: by size_pos *) 443val one_le_size = store_thm( 444 "one_le_size", 445 ``!n. 1 <= size n``, 446 metis_tac[size_nonzero, NOT_ZERO_GE_ONE]); 447 448(* Extract theorems from definition *) 449val size_0 = save_thm("size_0[simp]", size_def |> SPEC ``0`` |> SIMP_RULE arith_ss[]); 450(* val size_0 = |- size 0 = 1: thm *) 451val size_1 = save_thm("size_1[simp]", size_def |> SPEC ``1`` |> SIMP_RULE arith_ss[]); 452(* val size_1 = |- size 1 = 1: thm *) 453val size_2 = save_thm("size_2[simp]", size_def |> SPEC ``2`` |> SIMP_RULE arith_ss[size_1]); 454(* val size_2 = |- size 2 = 2: thm *) 455 456(* Note: 457logPowerTheory.halves_def 458|- !n. halves n = if n = 0 then 0 else SUC (halves (HALF n)) 459*) 460 461(* Theorem: size n = if n = 0 then 1 else halves n *) 462(* Proof: 463 By complete induction on n. 464 Base: size 0 = if 0 = 0 then 1 else halves 0 465 Note size 0 = 1 by size_0 466 Hence true. 467 Step: n <> 0. 468 If n = 1, 469 LHS = size 1 = 1 by size_1 470 RHS = halves 1 = 1 by halves_1 471 If n <> 1, 472 HALF n <> 0 by HALF_EQ_0, 1 < n 473 and HALF n < n by HALF_LESS 474 size n 475 = SUC (size (HALF n)) by size_def, 1 < n 476 = SUC (halves (HALF n)) by induction hypothesis 477 = halves n by halves_def 478*) 479val size_by_halves = store_thm( 480 "size_by_halves", 481 ``!n. size n = if n = 0 then 1 else halves n``, 482 completeInduct_on `n` >> 483 Cases_on `n = 0` >> 484 rw[] >> 485 Cases_on `HALF n = 0` >| [ 486 `n = 1` by fs[HALF_EQ_0] >> 487 simp[halves_1], 488 `HALF n < n` by rw[HALF_LESS] >> 489 `size n = SUC (size (HALF n))` by rw[Once size_def] >> 490 `_ = SUC (halves (HALF n))` by rw[] >> 491 `_ = halves n` by metis_tac[halves_def] >> 492 decide_tac 493 ]); 494 495(* Theorem: size n = if n = 0 then 1 else 1 + LOG2 n *) 496(* Proof: 497 If n = 0, 498 size 0 = 1 by size_1 499 If n <> 0, 500 size n = halves n by size_by_halves 501 = 1 + LOG2 n by halves_by_LOG2 502*) 503val size_by_LOG2 = store_thm( 504 "size_by_LOG2", 505 ``!n. size n = if n = 0 then 1 else 1 + LOG2 n``, 506 rpt strip_tac >> 507 Cases_on `n = 0` >- 508 simp[] >> 509 simp[size_by_halves, halves_by_LOG2]); 510 511(* Theorem: ulog n <= size n /\ size n <= 1 + ulog n *) 512(* Proof: 513 If n = 0, 514 Note size 0 = 1 by size_0 515 and ulog 0 = 0 by ulog_0 516 and 0 <= 1 /\ 1 <= 1 + 0 by arithmetic 517 If n <> 0, then 0 < n. 518 Note size n = 1 + LOG2 n by size_by_LOG2 519 and LOG2 n <= ulog n /\ 520 ulog n <= 1 + LOG2 n by ulog_LOG2, 0 < n 521 Thus size n <= 1 + ulog n /\ ulog n <= size n. 522*) 523val size_ulog = store_thm( 524 "size_ulog", 525 ``!n. ulog n <= size n /\ size n <= 1 + ulog n``, 526 strip_tac >> 527 Cases_on `n = 0` >- 528 rw[ulog_0] >> 529 `size n = 1 + LOG2 n` by rw[size_by_LOG2] >> 530 `0 < n` by decide_tac >> 531 imp_res_tac ulog_LOG2 >> 532 decide_tac); 533 534(* Theorem: 1 < n ==> size n <= 2 * ulog n *) 535(* Proof: 536 size n <= 1 + ulog n by size_ulog 537 <= ulog n + ulog n by ulog_ge_1 538 = 2 * ulog n by arithmetic 539*) 540val size_le_ulog = store_thm( 541 "size_le_ulog", 542 ``!n. 1 < n ==> size n <= 2 * ulog n``, 543 rpt strip_tac >> 544 `size n <= 1 + ulog n` by rw[size_ulog] >> 545 `1 <= ulog n` by rw[ulog_ge_1] >> 546 decide_tac); 547 548(* Theorem: size (MAX 1 n) = size n *) 549(* Proof: 550 If n = 0, 551 LHS = size (MAX 1 0) = size 1 = 1 by size_1 552 RHS = size 0 = 1 = LHS by size_0 553 If n <> 0, then 1 <= n 554 LHS = size (MAX 1 n) = size n by MAX_DEF 555*) 556val size_max_1_n = store_thm( 557 "size_max_1_n", 558 ``!n. size (MAX 1 n) = size n``, 559 rpt strip_tac >> 560 Cases_on `n = 0` >- 561 rw[] >> 562 `1 <= n` by decide_tac >> 563 metis_tac[MAX_ALT]); 564 565(* Theorem: size n = MAX 1 (size n) *) 566(* Proof: by size_pos, MAX_1_POS *) 567val max_1_size_n = store_thm( 568 "max_1_size_n", 569 ``!n. size n = MAX 1 (size n)``, 570 rw[MAX_1_POS]); 571 572(* Note: (size n) is almost (ulog n). 573 In fact, (size n) = (ulog n) except when n is a power of 2, in which case (size n) = 1 + ulog n. 574 This is because, the real-valued (log n) is talking about an exponent: n = 2 ** (log n). 575 The floor of the real-valued (log n) is (LOG2 n). 576 The ceiling of the real-valued (log n) is (ulog n). 577 When n is a power of 2, there is an exact exponent, so in this case: LOG2 n = log n = ulog n. 578 Indeed, when n is a power of 2, ulog n = 1 + LOG2 n. 579 For powers of 2, say, n = 8 = 2 ** 3, 3 bits can represent 8 binaries, from 000 to 111, or 0 to 7. 580 The number 8 itself in binary is 1000, with 4 bits, 1 bit more than what the exponent indicates. 581 The formula is: size n = 1 + LOG2 n, except when n = 0. Since 0 needs only 1 bit, size 0 = 1. 582 583> EVAL ``GENLIST I 10``; 584val it = |- GENLIST I 10 = [0; 1; 2; 3; 4; 5; 6; 7; 8; 9]: thm 585> EVAL ``MAP ulog (GENLIST I 10)``; 586val it = |- MAP ulog (GENLIST I 10) = [0; 0; 1; 2; 2; 3; 3; 3; 3; 4]: thm 587> EVAL ``MAP size (GENLIST I 10)``; 588val it = |- MAP size (GENLIST I 10) = [1; 1; 2; 2; 3; 3; 3; 3; 4; 4]: thm 589 590> EVAL ``GENLIST SUC 10``; 591val it = |- GENLIST SUC 10 = [1; 2; 3; 4; 5; 6; 7; 8; 9; 10]: thm 592> EVAL ``MAP LOG2 (GENLIST SUC 10)``; 593val it = |- MAP (\n. LOG2 n) (GENLIST SUC 10) = [0; 1; 1; 2; 2; 2; 2; 3; 3; 3]: thm 594> EVAL ``MAP ulog (GENLIST SUC 10)``; 595val it = |- MAP ulog (GENLIST SUC 10) = [0; 1; 2; 2; 3; 3; 3; 3; 4; 4]: thm 596> EVAL ``MAP size (GENLIST SUC 10)``; 597val it = |- MAP size (GENLIST SUC 10) = [1; 2; 2; 3; 3; 3; 3; 4; 4; 4]: thm 598 599*) 600 601(* Theorem: m < n ==> size m <= size n *) 602(* Proof: 603 By size_by_LOG2, this is to show: 604 m <> 0 /\ m < n ==> LOG2 m <= LOG2 n 605 or 0 < m /\ m < n ==> LOG2 m <= LOG2 n by NOT_ZERO_LT_ZERO 606 which is true by LOG2_LT 607*) 608val size_monotone_lt = store_thm( 609 "size_monotone_lt", 610 ``!m n. m < n ==> size m <= size n``, 611 rw[size_by_LOG2, LOG2_LT]); 612 613(* Theorem: m <= n ==> size m <= size n *) 614(* Proof: 615 If m < n, this is true by size_monotone_lt 616 If m = n, this is true trivially. 617*) 618val size_monotone_le = store_thm( 619 "size_monotone_le", 620 ``!m n. m <= n ==> size m <= size n``, 621 rpt strip_tac >> 622 `m < n \/ (m = n)` by decide_tac >- 623 rw[size_monotone_lt] >> 624 rw[]); 625 626(* Theorem: size n = 1 <=> n = 0 \/ n = 1 *) 627(* Proof: 628 If part: size n = 1 ==> n = 0 \/ n = 1 629 By contradiction, assume n <> 0 /\ n <> 1. 630 Then 2 <= n by n <> 0, n <> 1. 631 so size 2 <= size n by size_monotone_le 632 or 2 <= size n by size_2 633 This contradicts size n = 1. 634 Only-if part: n = 0 \/ n = 1 ==> size n = 1 635 True since size 0 = 1 by size_0 636 and size 1 = 1 by size_1 637*) 638val size_eq_1 = store_thm( 639 "size_eq_1", 640 ``!n. size n = 1 <=> n = 0 \/ n = 1``, 641 (rw[EQ_IMP_THM] >> simp[]) >> 642 spose_not_then strip_assume_tac >> 643 `2 <= n` by decide_tac >> 644 `size 2 <= size n` by rw[size_monotone_le] >> 645 `size 2 = 2` by rw[size_2] >> 646 decide_tac); 647 648(* Theorem: size (n * 2 ** m) = size n + (if n = 0 then 0 else m) *) 649(* Proof: 650 If n = 0, 651 size (n * 2 ** m) 652 = size 0 by arithmetic 653 = size 0 + 0 by ADD_0 654 If n <> 0, 655 size (n * 2 ** m) 656 = if (n * 2 ** m = 0) then 1 else 1 + LOG2 (n * 2 ** m) by size_by_LOG2 657 = 1 + LOG2 (n * 2 ** m) by EXP_EQ_0, n <> 0 658 = 1 + (m + LOG2 n) by LOG_EXP, 1 < 2, 0 < n 659 = (1 + LOG2 n) + m by arithmetic 660 = size n + m by size_by_LOG2 661*) 662val size_mult_two_power = store_thm( 663 "size_mult_two_power", 664 ``!n m. size (n * 2 ** m) = size n + (if n = 0 then 0 else m)``, 665 rw[size_by_LOG2] >> 666 `LOG2 (n * 2 ** m) = m + LOG2 n` by rw[GSYM LOG_EXP] >> 667 rw[]); 668 669(* Theorem: size (2 * n) = size n + if n = 0 then 0 else 1 *) 670(* Proof: by size_mult_two_power *) 671val size_twice = store_thm( 672 "size_twice", 673 ``!n. size (2 * n) = size n + if n = 0 then 0 else 1``, 674 metis_tac[size_mult_two_power, EXP_1, MULT_RIGHT_1, MULT_COMM]); 675 676(* Theorem: size (2 ** n) = 1 + n *) 677(* Proof: 678 size (2 ** n) 679 = size (1 * 2 ** n) by MULT_LEFT_1 680 = size 1 + n by size_mult_two_power 681 = 1 + n by size_1 682*) 683val size_2_exp = store_thm( 684 "size_2_exp", 685 ``!n. size (2 ** n) = 1 + n``, 686 metis_tac[size_mult_two_power, size_1, MULT_LEFT_1, DECIDE``1 <> 0``]); 687 688(* Theorem: 1 < n ==> SUC (size (HALF n)) = size n *) 689(* Proof: 690 Note 1 < n means n <> 0 /\ n <> 1 by arithmetic 691 Thus size n = SUC (size (HALF n)) by size_def 692*) 693val size_half_SUC = store_thm( 694 "size_half_SUC", 695 ``!n. 1 < n ==> SUC (size (HALF n)) = size n``, 696 rpt strip_tac >> 697 `n <> 0 /\ n <> 1` by decide_tac >> 698 metis_tac[size_def]); 699 700(* Theorem: 1 < n ==> size (HALF n) = (size n) - 1 *) 701(* Proof: 702 Note size n = SUC (size (HALF n)) by size_half_SUC 703 = 1 + size (HALF n) by SUC_ONE_ADD 704 Thus size (HALF n) = (size n) - 1 by arithmetic 705*) 706val size_half = store_thm( 707 "size_half", 708 ``!n. 1 < n ==> size (HALF n) = (size n) - 1``, 709 rpt strip_tac >> 710 `size n = 1 + size (HALF n)` by rw[GSYM size_half_SUC] >> 711 decide_tac); 712 713(* Theorem: size (n DIV (2 ** k)) = if n < 2 ** k then 1 else size n - k *) 714(* Proof: 715 By induction on k. 716 Base: !n. size (n DIV 2 ** 0) = if n < 2 ** 0 then 1 else size n - 0 717 LHS = size (n DIV 2 ** 0) 718 = size (n DIV 1) by EXP_0 719 = size n by DIV_1 720 RHS = if n < 1 then 1 else size n by EXP_0 721 = if n = 0 then 1 else size n by arithmetic 722 If n = 0, LHS = size 0 = 1 = RHS by size_0 723 If n <> 0, LHS = RHS. 724 Step: !n. size (n DIV 2 ** k) = if n < 2 ** k then 1 else size n - k ==> 725 !n. size (n DIV 2 ** SUC k) = if n < 2 ** SUC k then 1 else size n - SUC k 726 If n < 2 ** SUC k, 727 Then n DIV 2 ** SUC k = 0 by DIV_EQ_0 728 LHS = size 0 = 1 = RHS by size_0 729 Otherwise, 2 ** SUC k <= n. 730 Thus 2 * 2 ** k <= n by EXP 731 or 2 ** k <= HALF n by arithmetic 732 Also 1 < 2 ** SUC k by ONE_LT_EXP 733 so 1 < n by 2 ** SUC k <= n 734 size (n DIV 2 ** SUC k) 735 = size ((HALF n) DIV 2 ** k)) by HALF_DIV_TWO_POWER 736 = if (HALF n) < 2 ** k then 1 else size (HALF n) - k by induction hypothesis 737 = size (HALF n) - k by above, 2 ** k <= HALF n 738 = (size n - 1) - k by size_half, 1 < n 739 = size n - SUC k by ADD1 740*) 741val size_div_2_exp = store_thm( 742 "size_div_2_exp", 743 ``!n k. size (n DIV (2 ** k)) = if n < 2 ** k then 1 else size n - k``, 744 Induct_on `k` >| [ 745 rw[] >> 746 `n = 0` by decide_tac >> 747 simp[], 748 rpt strip_tac >> 749 (Cases_on `n < 2 ** SUC k` >> simp[]) >| [ 750 `n DIV 2 ** SUC k = 0` by rw[DIV_EQ_0] >> 751 simp[], 752 `2 ** SUC k <= n` by decide_tac >> 753 `HALF (2 ** SUC k) <= HALF n` by rw[DIV_LE_MONOTONE] >> 754 `HALF (2 ** SUC k) = 2 ** k` by rw[EXP_2_HALF] >> 755 `~(HALF n < 2 ** k)` by decide_tac >> 756 `size (n DIV 2 ** SUC k) = size ((HALF n) DIV 2 ** k)` by rw[GSYM HALF_DIV_TWO_POWER] >> 757 `_ = size (HALF n) - k` by rw[] >> 758 `1 < 2 ** SUC k` by rw[ONE_LT_EXP] >> 759 `1 < n` by decide_tac >> 760 `size (HALF n) - k = (size n - 1) - k` by rw[size_half] >> 761 decide_tac 762 ] 763 ]); 764 765(* Theorem: n < 2 ** (size n) *) 766(* Proof: 767 If n = 0, 768 RHS = 2 ** (size 0) 769 = 2 ** 1 by size_0 770 = 2 > 0 by EXP_1 771 If n <> 0, then 0 < n. 772 RHS = 2 ** (size n) 773 = 2 ** (1 + LOG2 n) by size_by_LOG2, n <> 0 774 = 2 ** SUC (LOG2 n) by SUC_ONE_ADD 775 > n by LOG2_PROPERTY 776*) 777val size_exp = store_thm( 778 "size_exp", 779 ``!n. n < 2 ** (size n)``, 780 rw[size_by_LOG2] >> 781 simp[GSYM ADD1] >> 782 rw[LOG2_PROPERTY]); 783 784(* Theorem: n < 2 ** size n /\ 2 ** size n <= 2 * (MAX 1 n) *) 785(* Proof: 786 This is to show: 787 (1) n < 2 ** size n, true by size_exp 788 (2) 2 ** size n <= TWICE n 789 2 ** size n 790 = 2 ** SUC (LOG2 n) by size_by_LOG2, 0 < n 791 = 2 * 2 ** LOG2 n by EXP 792 <= 2 * n by LOG2_PROPERTY, 0 < n 793*) 794val size_property = store_thm( 795 "size_property", 796 ``!n. 0 < n ==> n < 2 ** size n /\ 2 ** size n <= 2 * n``, 797 rpt strip_tac >- 798 rw[size_exp] >> 799 `2 ** size n = 2 ** SUC (LOG2 n)` by rw[size_by_LOG2] >> 800 `_ = 2 * 2 ** LOG2 n` by rw[EXP] >> 801 `2 * 2 ** LOG2 n <= 2 * n` by rw[LOG2_PROPERTY] >> 802 decide_tac); 803 804(* Theorem: n < 2 ** size n /\ 2 ** size n <= 2 * (MAX 1 n) *) 805(* Proof: 806 This is to show: 807 (1) n < 2 ** size n, true by size_exp 808 (2) 2 ** size n <= 2 * (MAX 1 n) 809 If n = 0, 810 to show: 2 ** size 0 <= 2 * (MAX 1 0) 811 LHS = 2 ** size 0 812 = 2 ** 1 by size_0 813 = 2 by EXP_1 814 = 2 * (MAX 1 0) = RHS by MAX_DEF 815 If n <> 0, 816 to show: 2 ** size n <= 2 * (MAX 1 n) 817 Note MAX 1 n = n by MAX_DEF, 1 <= n 818 Thus true by size_property 819*) 820val size_property_alt = store_thm( 821 "size_property_alt", 822 ``!n. n < 2 ** size n /\ 2 ** size n <= 2 * (MAX 1 n)``, 823 rpt strip_tac >- 824 rw[size_exp] >> 825 Cases_on `n = 0` >- 826 rw[] >> 827 `1 <= n` by decide_tac >> 828 `MAX 1 n = n` by rw[MAX_DEF] >> 829 rw[size_property]); 830 831(* Theorem: 2 ** m <= 2 * n /\ n < 2 ** m ==> (size n = m) *) 832(* Proof: 833 Note n <> 0, since 2 * n = 0 by 2 ** m <= 0 /\ 0 < 2 ** m is a contradiction. 834 Thus m <> 0 since n < 1 means n = 0 by EXP_0 835 so m = SUC k for some k by num_CASES 836 2 ** m = 2 ** SUC k 837 = 2 * 2 ** k by EXP 838 <= 2 * n by given 839 2 ** k <= n /\ n < 2 ** SUC k by above 840 ==> k = LOG2 n by LOG2_UNIQUE 841 Thus m = 1 + k 842 = 1 + LOG2 n 843 = size n by size_by_LOG2, n <> 0 844*) 845val size_unique = store_thm( 846 "size_unique", 847 ``!n m. 2 ** m <= 2 * n /\ n < 2 ** m ==> (size n = m)``, 848 rpt strip_tac >> 849 `n <> 0` by metis_tac[MULT_0, NOT_LESS] >> 850 `m <> 0` by metis_tac[EXP_0, DECIDE``n:num < 1 ==> (n = 0)``] >> 851 `?k. m = SUC k` by metis_tac[num_CASES] >> 852 `2 ** k <= n` by fs[EXP] >> 853 `k = LOG2 n` by metis_tac[LOG2_UNIQUE] >> 854 rw[size_by_LOG2]); 855 856(* Theorem: 0 < n ==> !m. (size n = m) <=> (2 ** m <= TWICE n /\ n < 2 ** m) *) 857(* Proof: 858 If part: 0 < n ==> 2 ** size n <= TWICE n /\ n < 2 ** size n 859 This is true by size_property. 860 Only-if part: !n m. 2 ** m <= TWICE n /\ n < 2 ** m ==> size n = m 861 This is true by size_unique. 862*) 863val size_thm = store_thm( 864 "size_thm", 865 ``!n. 0 < n ==> !m. (size n = m) <=> (2 ** m <= TWICE n /\ n < 2 ** m)``, 866 metis_tac[size_property, size_unique]); 867 868(* Theorem: size n = n <=> n = 1 \/ n = 2 *) 869(* Proof: 870 If part: size n = n ==> n = 1 \/ n = 2 871 By contradiction, assume n <> 1 /\ n <> 2. 872 Note n <> 0 since size 0 = 1 by size_0 873 so ?k. n = SUC k by num_CASES, n <> 0 874 Thus 2 ** SUC k <= 2 * SUC k by size_property 875 or 2 * 2 ** k <= 2 * SUC k by EXP 876 ==> 2 ** k <= SUC k by arithmetic 877 But SUC k < 2 ** k by SUC_X_LT_2_EXP_X, 1 < k 878 This is a contradiction. 879 Only-if part: size 1 = 1 /\ size 2 = 2 880 This is true by size_1, size_2 881*) 882val size_eq_self = store_thm( 883 "size_eq_self", 884 ``!n. (size n = n) <=> ((n = 1) \/ (n = 2))``, 885 rw_tac std_ss[EQ_IMP_THM] >| [ 886 spose_not_then strip_assume_tac >> 887 `n <> 0` by metis_tac[size_0, DECIDE``1 <> 0``] >> 888 `2 < n` by decide_tac >> 889 `?k. n = SUC k` by metis_tac[num_CASES] >> 890 `1 < k /\ 0 < n` by decide_tac >> 891 `2 * 2 ** k = 2 ** SUC k` by rw[EXP] >> 892 `2 ** SUC k <= 2 * SUC k` by metis_tac[size_property] >> 893 `2 ** k <= SUC k` by decide_tac >> 894 `SUC k < 2 ** k` by rw[SUC_X_LT_2_EXP_X] >> 895 decide_tac, 896 rw[], 897 rw[] 898 ]); 899 900(* Theorem: 0 < n ==> size n <= n *) 901(* Proof: 902 Note size n = 1 + LOG2 n by size_by_LOG2, 0 < n 903 and LOG2 n < n by LOG2_LT_SELF 904 so 1 + LOG2 n <= n by arithmetic 905 Thus size n <= n by above 906*) 907val size_le = store_thm( 908 "size_le", 909 ``!n. 0 < n ==> size n <= n``, 910 rpt strip_tac >> 911 `size n = 1 + LOG2 n` by rw[size_by_LOG2] >> 912 `LOG2 n < n` by rw[LOG2_LT_SELF] >> 913 decide_tac); 914 915(* Theorem: 2 < n ==> size n < n *) 916(* Proof: 917 By contradiction, assume ~(size n < n), or n <= size n. 918 Note size n <= n by size_le 919 so size n = n by EQ_LESS_EQ 920 ==> n = 1 or n = 2 by size_eq_self 921 This contradicts 2 < n. 922*) 923val size_lt = store_thm( 924 "size_lt", 925 ``!n. 2 < n ==> size n < n``, 926 spose_not_then strip_assume_tac >> 927 `size n <= n` by rw[size_le] >> 928 `size n = n` by decide_tac >> 929 fs[size_eq_self]); 930 931(* Theorem: 0 < n ==> size n <= n *) 932(* Proof: 933 size n 934 = 1 + LOG2 n by size_by_LOG2, n <> 0 935 < 1 + n by LOG2_LT_SELF 936 Thus size n <= n by arithmetic 937*) 938val size_le_self = store_thm( 939 "size_le_self", 940 ``!n. 0 < n ==> size n <= n``, 941 rpt strip_tac >> 942 `size n = 1 + LOG2 n` by rw[size_by_LOG2] >> 943 `1 + LOG2 n < 1 + n` by rw[LOG2_LT_SELF] >> 944 decide_tac); 945 946(* Theorem: size (size n) <= size n *) 947(* Proof: 948 If n = 0, 949 LHS = size (size 0) 950 = size 1 = 1 by size_0, size_1 951 = size 0 = RHS by size_0 952 If n <> 0, 953 Then size n <= n by size_le_self 954 Thus size (size n) <= size n by size_monotone_le 955*) 956val size_size_le = store_thm( 957 "size_size_le", 958 ``!n. size (size n) <= size n``, 959 rpt strip_tac >> 960 (Cases_on `n = 0` >> simp[]) >> 961 `size n <= n` by rw[size_le_self] >> 962 rw[size_monotone_le]); 963 964(* 965> EVAL ``MAP size [1 .. 10]``; 966val it = |- MAP size [1 .. 10] = [1; 2; 2; 3; 3; 3; 3; 4; 4; 4]: thm 967> EVAL ``MAP ulog [1 .. 10]``; 968val it = |- MAP ulog [1 .. 10] = [0; 1; 2; 2; 3; 3; 3; 3; 4; 4]: thm 969diff: 1 2 4 8 970> EVAL ``MAP LOG2 [1 .. 10]``; 971val it = |- MAP (\n. LOG2 n) [1 .. 10] = [0; 1; 1; 2; 2; 2; 2; 3; 3; 3]: thm 972*) 973 974(* Theorem: size n = if (n = 0 \/ perfect_power n 2) then 1 + ulog n else ulog n *) 975(* Proof: 976 If n = 0, 977 Then size 0 = 1 + 0 by size_0 978 = 1 + ulog 0 by ulog_0 979 If perfect_power n 2, 980 Then size n 981 = size (2 ** k) for some k by perfect_power_def 982 = 1 + k by size_2_exp 983 = 1 + ulog (2 ** k) by ulog_2_exp 984 = 1 + ulog n by n = 2 ** k 985 Otherwise, 986 Note 0 < n by n <> 0, 987 and !e. n <> 2 ** e by perfect_power_def 988 Thus 2 ** ulog n < TWICE n /\ 989 n <= 2 ** ulog n by ulog_property, 0 < n 990 or 2 ** ulog n <= TWICE n /\ 991 n < 2 ** ulog n by 2 ** ulog n <> n, take e = ulog n. 992 ==> size = ulog n by size_unique 993*) 994val size_by_ulog = store_thm( 995 "size_by_ulog", 996 ``!n. size n = if (n = 0 \/ perfect_power n 2) then 1 + ulog n else ulog n``, 997 rw_tac std_ss[perfect_power_def] >- 998 rw[ulog_0] >- 999 rw[size_2_exp, ulog_2_exp] >> 1000 irule size_unique >> 1001 `0 < n` by metis_tac[NOT_ZERO_LT_ZERO] >> 1002 imp_res_tac ulog_property >> 1003 `n <> 2 ** ulog n` by metis_tac[] >> 1004 decide_tac); 1005 1006(* Theorem: size n = ulog n + (if (n = 0) \/ perfect_power n 2 then 1 else 0) *) 1007(* Proof: by size_by_ulog *) 1008val size_by_ulog_alt = store_thm( 1009 "size_by_ulog_alt", 1010 ``!n. size n = ulog n + (if (n = 0) \/ perfect_power n 2 then 1 else 0)``, 1011 rw[size_by_ulog]); 1012 1013(* Theorem: size n = if (n = 0) then 1 else ulog n + (if perfect_power n 2 then 1 else 0) *) 1014(* Proof: by size_by_ulog *) 1015val size_by_ulog_eqn = store_thm( 1016 "size_by_ulog_eqn", 1017 ``!n. size n = if (n = 0) then 1 else ulog n + (if perfect_power n 2 then 1 else 0)``, 1018 rpt strip_tac >> 1019 (Cases_on `n = 0` >> rw[size_by_ulog])); 1020 1021(* Theorem: ulog n = if (n = 0) \/ perfect_power n 2 then size n - 1 else size n *) 1022(* Proof: by size_by_ulog *) 1023val ulog_by_size = store_thm( 1024 "ulog_by_size", 1025 ``!n. ulog n = if (n = 0) \/ perfect_power n 2 then size n - 1 else size n``, 1026 rw[size_by_ulog]); 1027 1028(* Theorem: ulog n = size n - (if (n = 0) \/ perfect_power n 2 then 1 else 0) *) 1029(* Proof: by ulog_by_size *) 1030val ulog_by_size_alt = store_thm( 1031 "ulog_by_size_alt", 1032 ``!n. ulog n = size n - (if (n = 0) \/ perfect_power n 2 then 1 else 0)``, 1033 rw[ulog_by_size]); 1034 1035(* Theorem: ulog n = if (n = 0) then 0 else size n - (if perfect_power n 2 then 1 else 0) *) 1036(* Proof: by ulog_by_size *) 1037val ulog_by_size_eqn = store_thm( 1038 "ulog_by_size_eqn", 1039 ``!n. ulog n = if (n = 0) then 0 else size n - (if perfect_power n 2 then 1 else 0)``, 1040 rpt strip_tac >> 1041 (Cases_on `n = 0` >> rw[ulog_by_size])); 1042 1043(* Theorem: halves n = if n = 0 then 0 else size n *) 1044(* Proof: 1045 If n = 0, 1046 halves 0 = 0 by halves_0 1047 If n <> 0, 1048 halves n 1049 = size n by size_by_halves, n <> 0 1050*) 1051val halves_by_size = store_thm( 1052 "halves_by_size", 1053 ``!n. halves n = if n = 0 then 0 else size n``, 1054 rpt strip_tac >> 1055 rw[halves_0] >> 1056 rw[size_by_halves]); 1057 1058(* Theorem: 1 < k ==> GENLIST (\j. k DIV 2 ** j) (size k) = 1059 k :: GENLIST (\j. (HALF k) DIV 2 ** j) (size (HALF k)) *) 1060(* Proof: 1061 Let f = (\j. k DIV 2 ** j), h = HALF k. 1062 Then f 0 = k DIV 2 ** 0 by notation 1063 = k DIV 1 = k by EXP_0, DIV_1 1064 and f o SUC = (\j. k DIV 2 ** (SUC j)) by notation 1065 = (\j. (HALF k) DIV 2 ** j) by HALF_DIV_TWO_POWER 1066 = (\j. h DIV 2 ** j) by notation 1067 GENLIST (\j. k DIV 2 ** j) (size k) 1068 = GENLIST f (size k) by notation 1069 = GENLIST f (SUC (size h)) by size_half_SUC 1070 = f 0::GENLIST (f o SUC) (size h) by GENLIST_CONS 1071 = k :: GENLIST (\j. h DIV 2 ** j) (size h) by above, notation 1072*) 1073val size_genlist_half = store_thm( 1074 "size_genlist_half", 1075 ``!k. 1 < k ==> GENLIST (\j. k DIV 2 ** j) (size k) = 1076 k :: GENLIST (\j. (HALF k) DIV 2 ** j) (size (HALF k))``, 1077 rpt strip_tac >> 1078 qabbrev_tac `f = \j. k DIV 2 ** j` >> 1079 `f o SUC = \j. (HALF k) DIV 2 ** j` by 1080 (rw[FUN_EQ_THM, Abbr`f`] >> 1081 rw[HALF_DIV_TWO_POWER]) >> 1082 `f 0 = k` by rw[Abbr`f`] >> 1083 `GENLIST f (size k) = GENLIST f (SUC (size (HALF k)))` by rw[size_half_SUC] >> 1084 rw[GENLIST_CONS]); 1085 1086(* Theorem: 1 < k ==> GENLIST (\j. n * 2 ** j) (size k) = 1087 n :: GENLIST (\j. 2 * n * 2 ** j) (size (HALF k)) *) 1088(* Proof: 1089 Let f = (\j. n * 2 ** j), h = HALF k. 1090 Then f 0 = n * 2 ** 0 by notation 1091 = n * 1 = n by EXP_0, MULT_RIGHT_1 1092 and f o SUC = (\j. n * 2 ** (SUC j)) by notation 1093 = (\j. n * 2 * 2 ** j) by EXP 1094 = (\j. 2 * n * 2 ** j) by MULT_ASSOC 1095 GENLIST (\j. n * 2 ** j) (size k) 1096 = GENLIST f (size k) by notation 1097 = GENLIST f (SUC (size h)) by size_half_SUC 1098 = f 0::GENLIST (f o SUC) (size h) by GENLIST_CONS 1099 = n :: GENLIST (\j. 2 * n * 2 ** j) (size h) by above, notation 1100*) 1101val size_genlist_twice = store_thm( 1102 "size_genlist_twice", 1103 ``!n k. 1 < k ==> GENLIST (\j. n * 2 ** j) (size k) = 1104 n :: GENLIST (\j. 2 * n * 2 ** j) (size (HALF k))``, 1105 rpt strip_tac >> 1106 qabbrev_tac `f = \j. n * 2 ** j` >> 1107 `f o SUC = \j. 2 * n * 2 ** j` by 1108 (rw[FUN_EQ_THM, Abbr`f`] >> 1109 rw[EXP]) >> 1110 `f 0 = n` by rw[Abbr`f`] >> 1111 `GENLIST f (size k) = GENLIST f (SUC (size (HALF k)))` by rw[size_half_SUC] >> 1112 rw[GENLIST_CONS]); 1113 1114(* Theorem: 1 < k ==> GENLIST (\j. n ** 2 ** j) (size k) = 1115 n :: GENLIST (\j. (n * n) ** 2 ** j) (size (HALF k)) *) 1116(* Proof: 1117 Let f = (\j. n ** 2 ** j), h = HALF k. 1118 Then f 0 = n ** 2 ** 0 by notation 1119 = n ** 1 = n by EXP_0, EXP_1 1120 and f o SUC = (\j. n ** 2 ** (SUC j)) by notation 1121 = (\j. (n ** 2) ** 2 ** j) by EXP_EXP_SUC 1122 = (\j. (n * n) ** 2 ** j) by EXP_2 1123 GENLIST (\j. n ** 2 ** j) (size k) 1124 = GENLIST f (size k) by notation 1125 = GENLIST f (SUC (size h)) by size_half_SUC 1126 = f 0::GENLIST (f o SUC) (size h) by GENLIST_CONS 1127 = n :: GENLIST (\j. (n * n) * n ** 2 ** j) (size h) by above, notation 1128*) 1129val size_genlist_square = store_thm( 1130 "size_genlist_square", 1131 ``!n:num k. 1 < k ==> GENLIST (\j. n ** 2 ** j) (size k) = 1132 n :: GENLIST (\j. (n * n) ** 2 ** j) (size (HALF k))``, 1133 rpt strip_tac >> 1134 qabbrev_tac `f = \j. n ** 2 ** j` >> 1135 `f o SUC = \j. (n * n) ** 2 ** j` by 1136 (rw[FUN_EQ_THM, Abbr`f`] >> 1137 rw[EXP_EXP_SUC]) >> 1138 `f 0 = n` by rw[Abbr`f`] >> 1139 `GENLIST f (size k) = GENLIST f (SUC (size (HALF k)))` by rw[size_half_SUC] >> 1140 rw[GENLIST_CONS]); 1141 1142(* Theorem: 1 < k ==> GENLIST (\j. if EVEN (k DIV 2 ** j) then 0 else n * 2 ** j) (size k) = 1143 (if EVEN k then 0 else n) :: 1144 GENLIST (\j. if EVEN ((HALF k) DIV 2 ** j) then 0 else 2 * n * 2 ** j) (size (HALF k)) *) 1145(* Proof: 1146 Let f = (\j. if EVEN (k DIV 2 ** j) then 0 else n * 2 ** j), h = HALF k. 1147 Then f 0 = if EVEN (k DIV 2 ** 0) then 0 else n * 2 ** 0 by notation 1148 = if EVEN (k DIV 1) then 0 else n * 1 by EXP_0 1149 = if EVEN k then 0 else n by DIV_1, MULT_RIGHT_1 1150 and f o SUC = (\j. if EVEN (k DIV 2 ** (SUC j)) then 0 else n * 2 ** (SUC j)) by notation 1151 = (\j. if EVEN ((HALF k) DIV 2 ** j) then 0 else n * 2 * 2 ** j) by HALF_DIV_TWO_POWER, EXP 1152 = (\j. if EVEN (h DIV 2 ** j) then 0 else 2 * n * 2 ** j) by MULT_ASSOC 1153 GENLIST (\j. if EVEN (k DIV 2 ** j) then 0 else n * 2 ** j) (size k) 1154 = GENLIST f (size k) by notation 1155 = GENLIST f (SUC (size h)) by size_half_SUC 1156 = f 0::GENLIST (f o SUC) (size h) by GENLIST_CONS 1157 = (if EVEN k then 0 else n) :: 1158 GENLIST (\j. if EVEN (h DIV 2 ** j) then 0 else 2 * n * 2 ** j) (size h) by above, notation 1159*) 1160val size_genlist_select = store_thm( 1161 "size_genlist_select", 1162 ``!n k. 1 < k ==> GENLIST (\j. if EVEN (k DIV 2 ** j) then 0 else n * 2 ** j) (size k) = 1163 (if EVEN k then 0 else n) :: 1164 GENLIST (\j. if EVEN ((HALF k) DIV 2 ** j) then 0 else 2 * n * 2 ** j) (size (HALF k))``, 1165 rpt strip_tac >> 1166 qabbrev_tac `f = \j. if EVEN (k DIV 2 ** j) then 0 else n * 2 ** j` >> 1167 `f o SUC = \j. if EVEN ((HALF k) DIV 2 ** j) then 0 else 2 * n * 2 ** j` by 1168 (rw[FUN_EQ_THM, Abbr`f`] >> 1169 rw[EXP, HALF_DIV_TWO_POWER]) >> 1170 `f 0 = if EVEN k then 0 else n` by rw[Abbr`f`] >> 1171 `GENLIST f (size k) = GENLIST f (SUC (size (HALF k)))` by rw[size_half_SUC] >> 1172 rw[GENLIST_CONS]); 1173 1174(* Theorem: size (n * 2 ** m) <= size n + m *) 1175(* Proof: by size_mult_two_power *) 1176val size_mult_two_power_upper = store_thm( 1177 "size_mult_two_power_upper", 1178 ``!m n. size (n * 2 ** m) <= size n + m``, 1179 rw[size_mult_two_power]); 1180 1181(* Theorem: size (m + n) <= 1 + size (MAX m n) *) 1182(* Proof: 1183 If m < n, 1184 Then MAX m n = n by MAX_DEF 1185 and m + n <= 2 * n by arithmetic 1186 size (m + n) 1187 <= size (2 * n) by size_monotone_le 1188 <= 1 + size n by size_twice 1189 Thus size (m + n) <= 1 + size n. 1190 Otherwise n <= m. 1191 Then MAX m n = m by MAX_DEF 1192 and m + n <= 2 * m by arithmetic 1193 size (m + n) 1194 <= size (2 * m) by size_monotone_le 1195 <= 1 + size m by size_twice 1196 Thus size (m + n) <= 1 + size m. 1197*) 1198val size_add_upper = store_thm( 1199 "size_add_upper", 1200 ``!m n. size (m + n) <= 1 + size (MAX m n)``, 1201 rpt strip_tac >> 1202 Cases_on `m < n` >| [ 1203 `MAX m n = n` by rw[MAX_DEF] >> 1204 `m + n <= 2 * n` by rw[] >> 1205 `size (m + n) <= size (2 * n)` by rw[size_monotone_le] >> 1206 `size (2 * n) <= 1 + size n` by rw[size_twice] >> 1207 fs[], 1208 `MAX m n = m` by rw[MAX_DEF] >> 1209 `m + n <= 2 * m` by rw[] >> 1210 `size (m + n) <= size (2 * m)` by rw[size_monotone_le] >> 1211 `size (2 * m) <= 1 + size m` by rw[size_twice] >> 1212 fs[] 1213 ]); 1214 1215(* Theorem: size (m * n) <= size m + size n *) 1216(* Proof: 1217 Note n < 2 ** size n by size_exp 1218 Thus m * n <= m * 2 ** size n by arithmetic 1219 size (m * n) 1220 <= size (m * 2 ** size n) by size_monotone_le 1221 <= size m + size n by size_mult_two_power_upper 1222*) 1223val size_mult_upper = store_thm( 1224 "size_mult_upper", 1225 ``!m n. size (m * n) <= size m + size n``, 1226 rpt strip_tac >> 1227 `n < 2 ** size n` by rw[size_exp] >> 1228 `m * n <= m * 2 ** size n` by rw[] >> 1229 `size (m * n) <= size (m * 2 ** size n)` by rw[size_monotone_le] >> 1230 `size (m * 2 ** size n) <= size m + size n` by rw[size_mult_two_power_upper] >> 1231 decide_tac); 1232 1233(* Theorem: size (SQ n) <= 2 * size n *) 1234(* Proof: 1235 size (SQ n) 1236 = size (n * n) by EXP_2 1237 <= (size n) + (size n) by size_mult_upper 1238 = 2 * size n by TIMES2 1239*) 1240val size_sq_upper = store_thm( 1241 "size_sq_upper", 1242 ``!n. size (SQ n) <= 2 * size n``, 1243 metis_tac[size_mult_upper, EXP_2, TIMES2]); 1244 1245(* Theorem: size n <= 1 + n *) 1246(* Proof: 1247 Note n < 2 ** n by X_LT_EXP_X, 1 < 2 1248 size n 1249 <= size (2 ** n) by size_monotone_le 1250 = 1 + n by size_2_exp 1251*) 1252val size_upper = store_thm( 1253 "size_upper", 1254 ``!n. size n <= 1 + n``, 1255 rpt strip_tac >> 1256 `n < 2 ** n` by rw[X_LT_EXP_X] >> 1257 `size n <= size (2 ** n)` by rw[size_monotone_le] >> 1258 rw[GSYM size_2_exp]); 1259 1260(* Theorem: size (n + 1) <= 1 + size n *) 1261(* Proof: 1262 size (n + 1) 1263 <= 1 + size (MAX n 1) by size_add_upper 1264 <= 1 + size n by size_max_1_n, MAX_COMM 1265*) 1266val size_add1 = store_thm( 1267 "size_add1", 1268 ``!n. size (n + 1) <= 1 + size n``, 1269 rpt strip_tac >> 1270 `size (n + 1) <= 1 + size (MAX n 1)` by rw[size_add_upper] >> 1271 `size (MAX n 1) = size n` by metis_tac[size_max_1_n, MAX_COMM] >> 1272 decide_tac); 1273 1274(* Theorem: 1 < n ==> 1 < size n *) 1275(* Proof: 1276 Note size n <> 0 by size_nonzero 1277 and size n <> 1 by size_eq_1, n <> 0, n <> 1 1278 Thus 1 < size n by arithmetic 1279*) 1280val size_gt_1 = store_thm( 1281 "size_gt_1", 1282 ``!n. 1 < n ==> 1 < size n``, 1283 rpt strip_tac >> 1284 `size n <> 0` by rw[] >> 1285 `size n <> 1` by rw[size_eq_1] >> 1286 decide_tac); 1287 1288(* Theorem: size (MAX m n) = MAX (size m) (size n) *) 1289(* Proof: by MAX_SWAP, size_monotone_le *) 1290val size_max = store_thm( 1291 "size_max", 1292 ``!m n. size (MAX m n) = MAX (size m) (size n)``, 1293 rw[MAX_SWAP, size_monotone_le]); 1294 1295(* Theorem: size (MIN m n) = MIN (size m) (size n) *) 1296(* Proof: by MIN_SWAP, size_monotone_le *) 1297val size_min = store_thm( 1298 "size_min", 1299 ``!m n. size (MIN m n) = MIN (size m) (size n)``, 1300 rw[MIN_SWAP, size_monotone_le]); 1301 1302(* Theorem: size (m ** n) <= MAX 1 (n * size m) *) 1303(* Proof: 1304 By induction on n. 1305 Base: size (m ** 0) <= MAX 1 (0 * size m) 1306 LHS = size 1 = 1 by EXP_0, size_1 1307 RHS = MAX 1 0 = 1 by MULT, MAX_DEF 1308 Hence true. 1309 Step: size (m ** n) <= MAX 1 (n * size m) ==> 1310 size (m ** SUC n) <= MAX 1 (SUC n * size m) 1311 If n = 0, 1312 size (m ** SUC 0) 1313 = size m by EXP_1 1314 <= MAX 1 (size m) by MAX_IS_MAX 1315 If n <> 0, 1316 Note 0 < n * size m by size_pos, MULT_POS 1317 so 1 <= n * size m by arithmetic 1318 thus MAX 1 (n * size m) = n * size m by MAX_1_POS 1319 also 0 < SUC n * size m by SUC_POS, size_pos, MULT_POS 1320 thus MAX 1 (SUC n * size m) = SUC n * size m 1321 by MAX_1_POS 1322 size (m ** SUC n) 1323 = size (m * m ** n) by EXP 1324 <= size m + size (m ** n) by size_mult_upper 1325 <= size m + MAX 1 (n * size m) by induction hypothesis 1326 = size m + n * size m by above 1327 = SUC n * size m by arithmetic 1328 = MAX 1 (SUC n * size m) by above 1329*) 1330val size_exp_upper = store_thm( 1331 "size_exp_upper", 1332 ``!m n. size (m ** n) <= MAX 1 (n * size m)``, 1333 rpt strip_tac >> 1334 Induct_on `n` >- 1335 rw[EXP_0] >> 1336 Cases_on `n = 0` >- 1337 simp[] >> 1338 `0 < n * size m /\ 0 < SUC n * size m` by rw[MULT_POS] >> 1339 `size (m ** SUC n) = size (m * m ** n)` by rw[EXP] >> 1340 `size (m * m ** n) <= size m + size (m ** n)` by rw[size_mult_upper] >> 1341 `size m + size (m ** n) <= size m + MAX 1 (n * size m)` by rw[] >> 1342 `size m + MAX 1 (n * size m) = size m + n * size m` by rw[MAX_1_POS] >> 1343 `_ = SUC n * size m` by rw[MULT] >> 1344 rw[MAX_1_POS]); 1345 1346(* This upper bound seems not likely to be lowered: 1347val it = |- size 100 = 7: thm 1348val it = |- size (100 ** 2) = 14: thm 1349val it = |- size (100 ** 3) = 20: thm 1350val it = |- size (100 ** 4) = 27: thm 1351val it = |- size (100 ** 5) = 34: thm 1352*) 1353 1354(* Theorem: 0 < n ==> size (m ** n) <= n * size m *) 1355(* Proof: 1356 Note 0 < size m by size_pos 1357 so 0 < n * size m by MULT_POS, 0 < n 1358 or 1 <= n * size m by arithmetic 1359 size (m ** n) 1360 <= MAX 1 (n * size m) by size_exp_upper 1361 = n * size m by above, MAX_DEF 1362*) 1363val size_exp_upper_alt = store_thm( 1364 "size_exp_upper_alt", 1365 ``!m n. 0 < n ==> size (m ** n) <= n * size m``, 1366 rpt strip_tac >> 1367 `0 < n * size m` by rw[MULT_POS] >> 1368 `1 <= n * size m` by decide_tac >> 1369 `MAX 1 (n * size m) = n * size m` by rw[MAX_DEF] >> 1370 metis_tac[size_exp_upper]); 1371 1372(* Theorem: size (n ** 2 ** size m) <= 2 * (MAX 1 m) * size n *) 1373(* Proof: 1374 size (n ** 2 ** size m) 1375 <= MAX 1 (2 ** size m * size n) by size_exp_upper 1376 = 2 ** size m * size n by EXP_POS, size_pos 1377 <= 2 * (MAX 1 m) * size n by size_property_alt 1378*) 1379val size_exp_two_power_upper = store_thm( 1380 "size_exp_two_power_upper", 1381 ``!m n. size (n ** 2 ** size m) <= 2 * (MAX 1 m) * size n``, 1382 rpt strip_tac >> 1383 `size (n ** 2 ** size m) <= MAX 1 (2 ** size m * size n)` by rw[size_exp_upper] >> 1384 `0 < 2 ** size m * size n` by rw[MULT_POS] >> 1385 `MAX 1 (2 ** size m * size n) = 2 ** size m * size n` by rw[MAX_1_POS] >> 1386 `2 ** size m * size n <= 2 * (MAX 1 m) * size n` by rw[size_property_alt] >> 1387 decide_tac); 1388 1389(* Theorem: 0 < n /\ j < size n ==> size (m ** 2 ** j) <= n * size m *) 1390(* Proof: 1391 Note j <= size n - 1 by j < size n 1392 so 2 ** j <= 2 ** (size n - 1) by EXP_BASE_LE_MONO, [1] 1393 But 2 * 2 ** (size n - 1) 1394 = 2 ** SUC (size n - 1) by EXP 1395 = 2 ** size n by size_pos, 0 < size n 1396 <= 2 * n by size_property, 0 < n, [2] 1397 so 2 ** j <= n by arithmetic, [1] [2] 1398 Thus size (m ** (2 ** j)) 1399 <= 2 ** j * size m by size_exp_upper_alt 1400 <= n * size m by above, 2 ** j <= n. 1401*) 1402val size_exp_two_power_le = store_thm( 1403 "size_exp_two_power_le", 1404 ``!n m j. 0 < n /\ j < size n ==> size (m ** 2 ** j) <= n * size m``, 1405 rpt strip_tac >> 1406 `size (m ** 2 ** j) <= 2 ** j * size m` by rw[size_exp_upper_alt] >> 1407 `j <= size n - 1` by decide_tac >> 1408 `2 ** j <= 2 ** (size n - 1)` by rw[EXP_BASE_LE_MONO] >> 1409 `0 < size n` by rw[] >> 1410 `SUC (size n - 1) = size n` by decide_tac >> 1411 `2 * 2 ** (size n - 1) = 2 ** size n` by rw[GSYM EXP] >> 1412 `2 ** size n <= 2 * n` by rw[size_property] >> 1413 `2 ** j * size m <= n * size m` by rw[] >> 1414 decide_tac); 1415 1416(* Theorem: m <= n ==> size (b ** m) <= size (b ** n) *) 1417(* Proof: 1418 If b = 0, 1419 Then b ** m = 0 or 1, so size (b ** m) = 1 by size_0, size_1 1420 and b ** n = 0 or 1, so size (b ** n) = 1 by size_0, size_1 1421 and 1 <= 1. 1422 If b <> 0, 1423 Then b ** m <= b ** n by EXP_BASE_LEQ_MONO_IMP 1424 so size (b ** m) <= size (b ** n) by size_monotone_le 1425*) 1426val size_exp_base_le = store_thm( 1427 "size_exp_base_le", 1428 ``!n m b. m <= n ==> size (b ** m) <= size (b ** n)``, 1429 rpt strip_tac >> 1430 Cases_on `b = 0` >- 1431 rw[ZERO_EXP] >> 1432 `0 < b` by decide_tac >> 1433 `b ** m <= b ** n` by rw[EXP_BASE_LEQ_MONO_IMP] >> 1434 rw[size_monotone_le]); 1435 1436(* Theorem: a <= b ==> size (a ** n) <= size (b ** n) *) 1437(* Proof: 1438 Note a ** n <= b ** n by EXP_EXP_LE_MONO 1439 Thus size (a ** n) <= size (b ** n) by size_monotone_le 1440*) 1441val size_exp_exp_le = store_thm( 1442 "size_exp_exp_le", 1443 ``!a b n. a <= b ==> size (a ** n) <= size (b ** n)``, 1444 rw[EXP_EXP_LE_MONO, size_monotone_le]); 1445 1446(* ------------------------------------------------------------------------- *) 1447(* Encode to Fixed Binary Bits *) 1448(* ------------------------------------------------------------------------- *) 1449 1450(* Encode a number to fix-bit binary *) 1451val to_bits_def = Define` 1452 (to_bits n 0 = []) /\ 1453 (to_bits n (SUC m) = n MOD 2 :: to_bits (HALF n) m) 1454`; 1455 1456(* 1457> EVAL ``to_bits 5 3``; 1458val it = |- to_bits 5 3 = [1; 0; 1]: thm 1459> EVAL ``to_bits 5 4``; 1460val it = |- to_bits 5 4 = [1; 0; 1; 0]: thm 1461> EVAL ``to_bits 5 2``; 1462val it = |- to_bits 5 2 = [1; 0]: thm 1463> EVAL ``to_bits 5 1``; 1464val it = |- to_bits 5 1 = [1]: thm 1465> EVAL ``decode (to_bits 5 4)``; 1466val it = |- decode (to_bits 5 4) = 5: thm 1467> EVAL ``decode (to_bits 5 2)``; 1468val it = |- decode (to_bits 5 2) = 1: thm 1469*) 1470 1471(* Extract theorems from definition *) 1472val to_bits_n_0 = save_thm("to_bits_n_0", to_bits_def |> CONJUNCT1); 1473(* val to_bits_n_0 = |- !n. to_bits n 0 = []: thm *) 1474 1475val to_bits_n_SUC = save_thm("to_bits_n_SUC", to_bits_def |> CONJUNCT2); 1476(* val to_bits_n_SUC = |- !n m. to_bits n (SUC m) = n MOD 2::to_bits (HALF n) m: thm *) 1477 1478(* Theorem: to_bits n (SUC m) = SNOC ((n DIV (2 ** m)) MOD 2) (to_bits n m) *) 1479(* Proof: 1480 By induction on m. 1481 Base: !n. to_bits n (SUC 0) = SNOC ((n DIV 2 ** 0) MOD 2) (to_bits n 0) 1482 to_bits n (SUC 0) 1483 = n MOD 2::to_bits (HALF n) 0 by to_bits_n_SUC 1484 = [n MOD 2] by to_bits_n_0 1485 SNOC ((n DIV 2 ** 0) MOD 2) (to_bits n 0) 1486 = SNOC ((n DIV 2 ** 0) MOD 2) [] by to_bits_n_0 1487 = [(n DIV 1) MOD 2] by SNOC 1488 = [n MOD 2] by DIV_ONE 1489 Step: !n. to_bits n (SUC m) = SNOC ((n DIV 2 ** m) MOD 2) (to_bits n m) ==> 1490 !n. to_bits n (SUC (SUC m)) = SNOC ((n DIV 2 ** SUC m) MOD 2) (to_bits n (SUC m)) 1491 to_bits n (SUC (SUC m)) 1492 = n MOD 2::to_bits (HALF n) (SUC m) by to_bits_n_SUC 1493 = n MOD 2::SNOC (((HALF n) DIV 2 ** m) MOD 2) (to_bits (HALF n) m) by induction hypothesis 1494 = SNOC (((HALF n) DIV 2 ** m) MOD 2) (n MOD 2 :: to_bits (HALF n) m) by SNOC_CONS 1495 = SNOC (((HALF n) DIV 2 ** m) MOD 2) (to_bits n (SUC m)) by to_bits_n_SUC 1496 = SNOC ((n DIV 2 ** SUC m) MOD 2) (to_bits n (SUC m)) by HALF_DIV_TWO_POWER 1497*) 1498val to_bits_snoc = store_thm( 1499 "to_bits_snoc", 1500 ``!n m. to_bits n (SUC m) = SNOC ((n DIV (2 ** m)) MOD 2) (to_bits n m)``, 1501 Induct_on `m` >- 1502 rw[to_bits_def] >> 1503 rpt strip_tac >> 1504 `to_bits n (SUC (SUC m)) = n MOD 2::to_bits (HALF n) (SUC m)` by rw[to_bits_n_SUC] >> 1505 `_ = n MOD 2::SNOC (((HALF n) DIV 2 ** m) MOD 2) (to_bits (HALF n) m)` by rw[] >> 1506 `_ = SNOC (((HALF n) DIV 2 ** m) MOD 2) (n MOD 2 :: to_bits (HALF n) m)` by rw[SNOC_CONS] >> 1507 `_ = SNOC (((HALF n) DIV 2 ** m) MOD 2) (to_bits n (SUC m))` by rw[GSYM to_bits_n_SUC] >> 1508 `_ = SNOC ((n DIV 2 ** SUC m) MOD 2) (to_bits n (SUC m))` by rw[HALF_DIV_TWO_POWER] >> 1509 rw[]); 1510 1511(* Theorem: to_bits 0 m = GENLIST (K 0) m *) 1512(* Proof: 1513 By induction on m. 1514 Base: to_bits 0 0 = GENLIST (K 0) 0 1515 to_bits 0 0 1516 = [] by to_bits_def 1517 = GENLIST (K 0) 0 by GENLIST_0 1518 Step: to_bits 0 m = GENLIST (K 0) m ==> to_bits 0 (SUC m) = GENLIST (K 0) (SUC m) 1519 to_bits 0 (SUC m) 1520 = 0 MOD 2::to_bits (HALF 0) m by to_bits_def 1521 = 0 :: to_bits 0 m by ZERO_MOD, ZERO_DIV, 0 < 2 1522 = 0 :: (GENLIST K 0) m by induction hypothesis 1523 = GENLIST (K 0) (SUC m) by GENLIST_K_CONS 1524*) 1525val to_bits_0_m = store_thm( 1526 "to_bits_0_m", 1527 ``!m. to_bits 0 m = GENLIST (K 0) m``, 1528 Induct >- 1529 rw_tac std_ss[to_bits_def, GENLIST_0] >> 1530 rw_tac std_ss[to_bits_def, GENLIST_K_CONS]); 1531 1532(* 1533> EVAL ``to_bits 7 0``; 1534val it = |- to_bits 7 0 = []: thm 1535> EVAL ``to_bits 7 1``; 1536val it = |- to_bits 7 1 = [1]: thm 1537> EVAL ``to_bits 7 2``; 1538val it = |- to_bits 7 2 = [1; 1]: thm 1539> EVAL ``to_bits 7 3``; 1540val it = |- to_bits 7 3 = [1; 1; 1]: thm 1541> EVAL ``to_bits 7 4``; 1542val it = |- to_bits 7 4 = [1; 1; 1; 0]: thm 1543*) 1544 1545(* Theorem: to_bits n m = GENLIST (\j. (n DIV 2 ** j) MOD 2) m *) 1546(* Proof: 1547 By induction on m. 1548 Base: !n. to_bits n 0 = GENLIST (\j. (n DIV 2 ** j) MOD 2) 0 1549 Let f = \j. (n DIV 2 ** j) MOD 2. 1550 to_bits n 0 1551 = [] by to_bits_def 1552 = GENLIST f 0 by GENLIST_0 1553 Step: !n. to_bits n m = GENLIST (\j. (n DIV 2 ** j) MOD 2) m ==> 1554 !n. to_bits n (SUC m) = GENLIST (\j. (n DIV 2 ** j) MOD 2) (SUC m) 1555 Let f = \j. (n DIV 2 ** j) MOD 2. 1556 and f 0 = (n DIV 2 ** 0) MOD 2 1557 = (n DIV 1) MOD 2 by ONE 1558 = n MOD 2 by DIV_ONE 1559 to_bits n (SUC m) 1560 = n MOD 2::to_bits (HALF n) m by to_bits_def 1561 = n MOD 2::GENLIST (\j. ((HALF n) DIV 2 ** j) MOD 2) m by induction hypothesis 1562 = n MOD 2::GENLIST (\j. (n DIV (2 * 2 ** j)) MOD 2) m by DIV_DIV_DIV_MULT 1563 = n MOD 2::GENLIST (\j. (n DIV (2 ** (SUC j))) MOD 2) m by EXP 1564 = n MOD 2::GENLIST (f o SUC) m by GENLIST_CONG, composition 1565 = f 0:: GENLIST (f o SUC) m by above 1566 = GENLIST f (SUC m) by GENLIST_CONS 1567*) 1568Theorem to_bits_n_m: 1569 !m n. to_bits n m = GENLIST (\j. (n DIV 2 ** j) MOD 2) m 1570Proof 1571 Induct >- 1572 rw[to_bits_def] >> 1573 rpt strip_tac >> 1574 qabbrev_tac `f = \j. (n DIV 2 ** j) MOD 2` >> 1575 `f 0 = n MOD 2` by rw[Abbr`f`] >> 1576 `to_bits n (SUC m) = n MOD 2::to_bits (HALF n) m` by rw[to_bits_def] >> 1577 `_ = n MOD 2::GENLIST (\j. ((HALF n) DIV 2 ** j) MOD 2) m` by rw[] >> 1578 `_ = n MOD 2::GENLIST (\j. (n DIV (2 * 2 ** j)) MOD 2) m` by rw[DIV_DIV_DIV_MULT] >> 1579 `_ = n MOD 2::GENLIST (\j. (n DIV (2 ** (SUC j))) MOD 2) m` by rw[GSYM EXP] >> 1580 `_ = n MOD 2::GENLIST (f o SUC) m` by rw[GENLIST_CONG, Abbr`f`] >> 1581 `_ = GENLIST f (SUC m)` by rw[GENLIST_CONS] >> 1582 rw[] 1583QED 1584 1585(* Theorem: LENGTH (to_bits n m) = m *) 1586(* Proof: 1587 Let f = \j. (n DIV 2 ** j) MOD 2. 1588 LENGTH (to_bits n m) 1589 = LENGTH (GENLIST f m) by to_bits_n_m 1590 = m by LENGTH_GENLIST 1591*) 1592val to_bits_length = store_thm( 1593 "to_bits_length", 1594 ``!m n. LENGTH (to_bits n m) = m``, 1595 rw_tac std_ss[to_bits_n_m, LENGTH_GENLIST]); 1596 1597(* Theorem: k < m ==> (EL k (to_bits n m) = (n DIV (2 ** k)) MOD 2) *) 1598(* Proof: 1599 Let f = \j. (n DIV 2 ** j) MOD 2. 1600 EL k (to_bits n m) 1601 = EL k (GENLIST f m) by to_bits_n_m 1602 = f k by EL_GENLIST, k < m 1603 = (n DIV 2 ** k) MOD 2 by notation 1604*) 1605val to_bits_element = store_thm( 1606 "to_bits_element", 1607 ``!k m n. k < m ==> (EL k (to_bits n m) = (n DIV (2 ** k)) MOD 2)``, 1608 rw_tac std_ss[to_bits_length, to_bits_n_m, EL_GENLIST]); 1609 1610(* Theorem: decode (to_bits n m) = n MOD (2 ** m) *) 1611(* Proof: 1612 By complete induction on n. 1613 Base: n = 0 ==> decode (to_bits n m) = n MOD 2 ** m 1614 decode (to_bits 0 m) 1615 = decode (GENLIST (K 0) m) by to_bits_0_m 1616 = 0 by decode_genlist_zero 1617 = 0 MOD 2 ** m by ZERO_MOD 1618 Step: !m. m < n ==> !m'. decode (to_bits m m') = m MOD 2 ** m' ==> 1619 n <> 0 ==> decode (to_bits n m) = n MOD 2 ** m 1620 If m = 0, 1621 to show: decode (to_bits n 0) = n MOD 2 ** 0 1622 decode (to_bits n 0) 1623 = decode [] by to_bits_def 1624 = 0 by decode_def 1625 = n MOD 1 by MOD_ONE 1626 = n MOD (2 ** 0) by EXP_0 1627 1628 Otherwise, m <> 0, 1629 Note ?k. m = SUC k by num_CASES 1630 Let h = 2 ** k. 1631 Note HALF n < n` by HALF_LESS, 0 < n 1632 and 0 < h by EXP_POS, 0 < 2 1633 decode (to_bits n m) 1634 = decode (to_bits n (SUC k)) by m = SUC k 1635 = decode (n MOD 2 :: to_bits (HALF n) k) by to_bits_def 1636 = n MOD 2 + 2 * (decode (to_bits (HALF n) k)) by decode_def 1637 = n MOD 2 + 2 * ((HALF n) MOD 2 ** k) by induction hypothesis, HALF n < n 1638 = n MOD 2 + 2 * (HALF (n MOD (2 * h))) by DIV_MOD_MOD_DIV 1639 = 2 * (HALF (n MOD (2 * h))) + n MOD 2 by ADD_COMM 1640 = 2 * (HALF (n MOD (2 * h))) + (n MOD (2 * h)) MOD 2 by MOD_MULT_MOD, 0 < h 1641 = HALF (n MOD (2 * h)) * 2 + (n MOD (2 * h)) MOD 2 by MULT_COMM 1642 = n MOD (2 * h) by DIVISION 1643 = n MOD (2 * 2 ** k) by h = 2 ** k 1644 = n MOD (2 ** m) by EXP 1645*) 1646val decode_to_bits_eq_mod = store_thm( 1647 "decode_to_bits_eq_mod", 1648 ``!m n. decode (to_bits n m) = n MOD (2 ** m)``, 1649 completeInduct_on `n` >> 1650 Cases_on `n = 0` >- 1651 rw_tac std_ss[decode_genlist_zero, to_bits_0_m] >> 1652 rpt strip_tac >> 1653 Cases_on `m` >- 1654 rw[decode_def, to_bits_def] >> 1655 qabbrev_tac `m = SUC n'` >> 1656 qabbrev_tac `h = 2 ** n'` >> 1657 `HALF n < n` by rw[HALF_LESS] >> 1658 `0 < h` by rw[EXP_POS, Abbr`h`] >> 1659 `decode (to_bits n m) = decode (n MOD 2 :: to_bits (HALF n) n')` by rw[to_bits_def, Abbr`m`] >> 1660 `_ = n MOD 2 + TWICE (decode (to_bits (HALF n) n'))` by rw[decode_def] >> 1661 `_ = n MOD 2 + TWICE ((HALF n) MOD 2 ** n')` by rw[] >> 1662 `_ = n MOD 2 + TWICE (HALF (n MOD (2 * h)))` by rw[DIV_MOD_MOD_DIV, Abbr`h`] >> 1663 `_ = TWICE (HALF (n MOD (2 * h))) + n MOD 2` by rw[] >> 1664 `_ = TWICE (HALF (n MOD (2 * h))) + (n MOD (2 * h)) MOD 2` by rw[MOD_MULT_MOD] >> 1665 `_ = HALF (n MOD (2 * h)) * 2 + (n MOD (2 * h)) MOD 2` by rw[] >> 1666 `_ = n MOD (2 * h)` by rw[DIVISION] >> 1667 `_ = n MOD 2 ** m` by rw[EXP, Abbr`m`] >> 1668 rw[]); 1669 1670 1671(* ------------------------------------------------------------------------- *) 1672 1673(* export theory at end *) 1674val _ = export_theory(); 1675 1676(*===========================================================================*) 1677