1(* ------------------------------------------------------------------------- *) 2(* The Helper File *) 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 "helper"; 12 13(* ------------------------------------------------------------------------- *) 14 15 16(* open dependent theories *) 17val _ = load("helperFunctionTheory"); 18open helperFunctionTheory; 19open helperSetTheory; 20open helperNumTheory; 21 22(* arithmeticTheory -- load by default *) 23open arithmeticTheory pred_setTheory; 24open dividesTheory; 25open gcdTheory; (* for GCD_IS_GREATEST_COMMON_DIVISOR *) 26 27val _ = load("logPowerTheory"); 28open logPowerTheory; (* for SQRT *) 29 30open whileTheory; (* for HOARE_SPEC_DEF *) 31 32 33(* ------------------------------------------------------------------------- *) 34(* Helper Theorems Documentation *) 35(* ------------------------------------------------------------------------- *) 36(* Overloading: 37*) 38(* 39 40 Number Theorems: 41 square_def |- !n. square n <=> ?k. n = k * k 42 square_alt |- !n. square n <=> ?k. n = k ** 2 43 square_eqn |- !n. square n <=> SQRT n ** 2 = n 44 square_0 |- square 0 45 square_1 |- square 1 46 prime_non_square |- !p. prime p ==> ~square p 47 prime_non_quad |- !p. prime p ==> ~(4 divides p) 48 prime_mod_eq_0 |- !p q. prime p /\ 1 < q ==> (p MOD q = 0 <=> q = p) 49 even_by_mod_4 |- !n. EVEN n <=> n MOD 4 = 0 \/ n MOD 4 = 2 50 odd_by_mod_4 |- !n. ODD n <=> n MOD 4 = 1 \/ n MOD 4 = 3 51 mod_4_even |- !n. EVEN n <=> n MOD 4 IN {0; 2} 52 mod_4_odd |- !n. ODD n <=> n MOD 4 IN {1; 3} 53 mod_4_square |- !n. n ** 2 MOD 4 IN {0; 1} 54 mod_4_not_squares |- !n. n MOD 4 = 3 ==> !x y. n <> x ** 2 + y ** 2 55 half_add1_lt |- !n. 2 < n ==> 1 + HALF n < n 56 57 Arithmetic Theorems: 58 four_squares_identity |- !a b c d. b * d <= a * c ==> 59 (a ** 2 + b ** 2) * (c ** 2 + d ** 2) = 60 (a * d + b * c) ** 2 + (a * c - b * d) ** 2 61 four_squares_identity_alt |- !a b c d. a * c <= b * d ==> 62 (a ** 2 + b ** 2) * (c ** 2 + d ** 2) = 63 (a * d + b * c) ** 2 + (b * d - a * c) ** 2 64 65 Square Sum Theorems: 66 squares_sum_eq_0 |- !a b. a ** 2 + b ** 2 = 0 <=> a = 0 /\ b = 0 67 squares_sum_identity_1 |- !a b c d. a ** 2 + b ** 2 = c ** 2 + d ** 2 ==> 68 (a * d - b * c) * (a * d + b * c) = 69 (a ** 2 + b ** 2) * (d ** 2 - b ** 2) 70 squares_sum_identity_2 |- !a b c d. a ** 2 + b ** 2 = c ** 2 + d ** 2 ==> 71 (b * c - a * d) * (a * d + b * c) = 72 (a ** 2 + b ** 2) * (b ** 2 - d ** 2) 73 squares_sum_inequality |- !a b c d. a ** 2 + b ** 2 = c ** 2 + d ** 2 /\ 74 0 < b /\ 0 < d ==> a * c < a ** 2 + b ** 2 75 squares_sum_inequality_1 |- !a b c d. a ** 2 + b ** 2 = c ** 2 + d ** 2 /\ 76 0 < b /\ 0 < c ==> a * d < a ** 2 + b ** 2 77 squares_sum_inequality_2 |- !a b c d. a ** 2 + b ** 2 = c ** 2 + d ** 2 /\ 78 0 < a /\ 0 < d ==> b * c < a ** 2 + b ** 2 79 squares_sum_prime_coprime |- !p a b. prime p /\ p = a ** 2 + b ** 2 ==> coprime a b 80 squares_sum_prime_thm |- !p a b c d. prime p /\ 81 p = a ** 2 + b ** 2 /\ p = c ** 2 + d ** 2 /\ 82 a * d = b * c ==> a = c /\ b = d 83 84 Set Theorems: 85 doublet_eq |- !a b c d. {a; b} = {c; d} <=> a = c /\ b = d \/ a = d /\ b = c 86 doublet_finite |- !a b. FINITE {a; b} 87 doublet_card |- !a b. a <> b ==> CARD {a; b} = 2 88 partition_three_special_card 89 |- !s a b c. FINITE s /\ s = a UNION b UNION c /\ 90 a INTER b = {} /\ b INTER c = {} /\ a INTER c = {} /\ 91 CARD a = CARD c ==> CARD s = 2 * CARD a + CARD b 92 set_partition_bij_card 93 |- !f s a b. FINITE s /\ s = a UNION b /\ a INTER b = {} /\ BIJ f a b ==> 94 CARD s = 2 * CARD a 95 set_partition_bij_card_even 96 |- !f s a b. FINITE s /\ s = a UNION b /\ a INTER b = {} /\ BIJ f a b ==> 97 EVEN (CARD s) 98 set_partition_bij_give_bij 99 |- !f s t a b c d. s = a UNION b /\ a INTER b = {} /\ 100 t = c UNION d /\ c INTER d = {} /\ 101 BIJ f a d /\ BIJ f b c ==> BIJ f s t 102 103 WHILE Loop Specification: 104 WHILE_RULE_PRE_POST 105 |- (!x. Invariant x /\ Guard x ==> Measure (Command x) < Measure x) /\ 106 (!x. Precond x ==> Invariant x) /\ 107 (!x. Invariant x /\ ~Guard x ==> Postcond x) /\ 108 HOARE_SPEC (\x. Invariant x /\ Guard x) Command Invariant ==> 109 HOARE_SPEC Precond (WHILE Guard Command) Postcond 110*) 111 112(* ------------------------------------------------------------------------- *) 113(* Arithmetic Theorems *) 114(* ------------------------------------------------------------------------- *) 115 116(* ------------------------------------------------------------------------- *) 117(* Number Theorems *) 118(* ------------------------------------------------------------------------- *) 119 120(* remove overload of TWICE, SQ *) 121val _ = clear_overloads_on "TWICE"; 122val _ = clear_overloads_on "SQ"; 123 124(* Overloading for a square n *) 125(* val _ = overload_on ("square", ``\n:num. ?k. n = k ** 2``); *) 126(* Make square in computeLib, cannot be an overload. *) 127 128(* Define square predicate. *) 129val square_def = zDefine` 130 square (n:num) = ?k. n = k * k 131`; 132(* use zDefine as this is not effective. *) 133 134(* Theorem: square n = ?k. n = k ** 2 *) 135(* Proof: by square_def. *) 136Theorem square_alt: 137 !n. square n = ?k. n = k ** 2 138Proof 139 simp[square_def] 140QED 141 142(* Theorem: square n <=> (SQRT n) ** 2 = n *) 143(* Proof: 144 If part: square n ==> (SQRT n) ** 2 = n 145 This is true by SQRT_SQ, EXP_2 146 Only-if part: (SQRT n) ** 2 = n ==> square n 147 Take k = SQRT n for n = k ** 2. 148*) 149Theorem square_eqn[compute]: 150 !n. square n <=> (SQRT n) ** 2 = n 151Proof 152 metis_tac[square_def, SQRT_SQ, EXP_2] 153QED 154 155(* 156EVAL ``square 10``; F 157EVAL ``square 16``; T 158*) 159 160(* Theorem: square 0 *) 161(* Proof: by 0 = 0 * 0. *) 162Theorem square_0: 163 square 0 164Proof 165 simp[square_def] 166QED 167 168(* Theorem: square 1 *) 169(* Proof: by 1 = 1 * 1. *) 170Theorem square_1: 171 square 1 172Proof 173 simp[square_def] 174QED 175 176(* Theorem: prime p ==> ~square p *) 177(* Proof: 178 By contradiction, suppose (square p). 179 Then p = k * k by square_def 180 thus k divides p by divides_def 181 so k = 1 or k = p by prime_def 182 If k = 1, 183 then p = 1 * 1 = 1 by arithmetic 184 but p <> 1 by NOT_PRIME_1 185 If k = p, 186 then p * 1 = p * p by arithmetic 187 or 1 = p by EQ_MULT_LCANCEL, NOT_PRIME_0 188 but p <> 1 by NOT_PRIME_1 189*) 190Theorem prime_non_square: 191 !p. prime p ==> ~square p 192Proof 193 rpt strip_tac >> 194 `?k. p = k * k` by rw[GSYM square_def] >> 195 `k divides p` by metis_tac[divides_def] >> 196 `(k = 1) \/ (k = p)` by metis_tac[prime_def] >- 197 fs[NOT_PRIME_1] >> 198 `p * 1 = p * p` by metis_tac[MULT_RIGHT_1] >> 199 `1 = p` by metis_tac[EQ_MULT_LCANCEL, NOT_PRIME_0] >> 200 metis_tac[NOT_PRIME_1] 201QED 202 203(* Theorem: prime p ==> ~(4 divides p) *) 204(* Proof: 205 By contradiction, suppose 4 divides p. 206 Then p = 4 by prime_def 207 = 2 * 2 by arithmetic 208 Thus p = 2 by divides_def, prime_def 209 ==> 4 = 2, which is a contradiction. 210*) 211Theorem prime_non_quad: 212 !p. prime p ==> ~(4 divides p) 213Proof 214 rpt strip_tac >> 215 `4 <> 1 /\ 2 <> 1` by fs[] >> 216 `p = 4` by metis_tac[prime_def] >> 217 `_ = 2 * 2` by decide_tac >> 218 `p = 2` by metis_tac[divides_def, prime_def] >> 219 fs[] 220QED 221 222(* Theorem: prime p /\ 1 < q ==> (p MOD q = 0 <=> q = p) *) 223(* Proof: 224 If part: p MOD q = 0 ==> q = p 225 Note q divides p by DIVIDES_MOD_0 226 and q <> 1 by 1 < q 227 so q = p by prime_def 228 Only-if part: q = p ==> p MOD q = 0 229 This is true by DIVMOD_ID, by 0 < q. 230*) 231Theorem prime_mod_eq_0: 232 !p q. prime p /\ 1 < q ==> (p MOD q = 0 <=> q = p) 233Proof 234 rw[EQ_IMP_THM] >> 235 `q divides p` by rw[DIVIDES_MOD_0] >> 236 `q <> 1` by decide_tac >> 237 metis_tac[prime_def] 238QED 239 240(* Theorem: EVEN n <=> n MOD 4 = 0 \/ n MOD 4 = 2 *) 241(* Proof: 242 Since 2 divides 4 by divides_def 243 Hence (n MOD 4) MOD 2 = n MOD 2 by DIVIDES_MOD_MOD 244 If part: EVEN n ==> (n MOD 4 = 0) \/ (n MOD 4 = 2) 245 Note EVEN n ==> n MOD 2 = 0 by EVEN_MOD2 246 By contradiction, suppose (n MOD 4 <> 0) /\ (n MOD 4 <> 2). 247 Since n MOD 4 < 4 by MOD_LESS 248 so n MOD 4 = 1 or n MOD 4 = 3. 249 If n MOD 4 = 1, 250 Then (n MOD 4) MOD 2 = 1 MOD 2 = 1 <> 0, a contradiction. 251 If n MOD 4 = 3, 252 Then (n MOD 4) MOD 2 = 3 MOD 2 = 1 <> 0, a contradiction. 253 Only-if part: (n MOD 4 = 0) \/ (n MOD 4 = 2) ==> EVEN n 254 If n MOD 4 = 0, 255 Then n MOD 2 = 0 MOD 2 = 0 256 so EVEN n by EVEN_DOUBLE 257 If n MOD 4 = 2, 258 Then n MOD 2 = 2 MOD 2 = 0 259 so EVEN n by EVEN_DOUBLE 260*) 261Theorem even_by_mod_4: 262 !n. EVEN n <=> n MOD 4 = 0 \/ n MOD 4 = 2 263Proof 264 rpt strip_tac >> 265 `2 divides 4` by rw[divides_def] >> 266 `n MOD 2 = (n MOD 4) MOD 2` by rw[DIVIDES_MOD_MOD] >> 267 rw[EQ_IMP_THM] >| [ 268 spose_not_then strip_assume_tac >> 269 `n MOD 2 = 0` by rw[GSYM EVEN_MOD2] >> 270 `n <> 0` by metis_tac[ZERO_MOD, DECIDE``0 < 4``] >> 271 `n MOD 4 < 4` by rw[MOD_LESS] >> 272 `(n MOD 4 = 1) \/ (n MOD 4 = 3)` by decide_tac >| [ 273 `1 MOD 2 = 1` by rw[] >> 274 fs[], 275 `3 MOD 2 = 1` by rw[] >> 276 fs[] 277 ], 278 `0 MOD 2 = 0` by rw[] >> 279 fs[EVEN_MOD2], 280 `2 MOD 2 = 0` by rw[] >> 281 fs[EVEN_MOD2] 282 ] 283QED 284 285(* Theorem: ODD n <=> n MOD 4 = 1 \/ n MOD 4 = 3 *) 286(* Proof: 287 Since 2 divides 4 by divides_def 288 Hence (n MOD 4) MOD 2 = n MOD 2 by DIVIDES_MOD_MOD 289 If part: ODD n ==> (n MOD 4 = 1) \/ (n MOD 4 = 3) 290 Note ODD n ==> n MOD 2 = 1 by ODD_MOD2 291 By contradiction, suppose (n MOD 4 <> 1) /\ (n MOD 4 <> 3). 292 Since n MOD 4 < 4 by MOD_LESS 293 so n MOD 4 = 0 or n MOD 4 = 2. 294 If n MOD 4 = 0, 295 Then n MOD 2 = 0 MOD 2 = 0 <> 1, a contradiction. 296 If n MOD 4 = 2, 297 Then n MOD 2 = 2 MOD 2 = 0 <> 1, a contradiction. 298 Only-if part: (n MOD 4 = 1) \/ (n MOD 4 = 3) ==> ODD n 299 If n MOD 4 = 1, 300 Then n MOD 2 = 1 MOD 1 = 1 301 so ODD n by ODD_MOD2 302 If n MOD 4 = 3, 303 Then n MOD 2 = 3 MOD 1 = 1 304 so ODD n by ODD_MOD2 305*) 306Theorem odd_by_mod_4: 307 !n. ODD n <=> n MOD 4 = 1 \/ n MOD 4 = 3 308Proof 309 rpt strip_tac >> 310 `2 divides 4` by rw[divides_def] >> 311 `n MOD 2 = (n MOD 4) MOD 2` by rw[DIVIDES_MOD_MOD] >> 312 rw[EQ_IMP_THM] >| [ 313 spose_not_then strip_assume_tac >> 314 `n MOD 2 = 1` by rw[GSYM ODD_MOD2] >> 315 `n <> 0` by metis_tac[EVEN_0, EVEN_ODD] >> 316 `n MOD 4 < 4` by rw[MOD_LESS] >> 317 `(n MOD 4 = 0) \/ (n MOD 4 = 2)` by decide_tac >| [ 318 `0 MOD 2 = 0` by rw[] >> 319 fs[], 320 `2 MOD 2 = 0` by rw[] >> 321 fs[] 322 ], 323 `1 MOD 2 = 1` by rw[] >> 324 fs[ODD_MOD2], 325 `3 MOD 2 = 1` by rw[] >> 326 fs[ODD_MOD2] 327 ] 328QED 329 330(* Theorem: EVEN n <=> n MOD 4 IN {0; 2} *) 331(* Proof: 332 EVEN n 333 <=> ?k. n = 2 * k by EVEN_EXISTS 334 <=> ?k. n MOD 4 335 = (2 * k) MOD 4 336 = (2 * k MOD 4) MOD 4 by MOD_TIMES 337 = (0 or 2 or 4 or 6) MOD 4 by MOD_LESS 338 = 0 or 2 by arithmetic 339*) 340Theorem mod_4_even: 341 !n. EVEN n <=> n MOD 4 IN {0; 2} 342Proof 343 rw[EVEN_EXISTS, EQ_IMP_THM] >| [ 344 `(2 * m) MOD 4 = (2 * m MOD 4) MOD 4` by rw[MOD_TIMES] >> 345 `m MOD 4 < 4` by rw[] >> 346 qabbrev_tac `x = m MOD 4` >> 347 (`(x = 0) \/ (x = 1) \/ (x = 2) \/ (x = 3)` by decide_tac >> rfs[]), 348 fs[MOD_EQN] >> 349 qexists_tac `2 * c` >> 350 decide_tac, 351 fs[MOD_EQN] >> 352 qexists_tac `2 * c + 1` >> 353 decide_tac 354 ] 355QED 356 357(* Theorem: ODD n <=> n MOD 4 IN {1; 3} *) 358(* Proof: 359 ODD n 360 <=> ~EVEN n by EVEN_ODD 361 <=> n MOD 4 NOTIN {0; 2} by mod_4_even 362 <=> n MOD 4 IN {1; 3} by MOD_LESS 363*) 364Theorem mod_4_odd: 365 !n. ODD n <=> n MOD 4 IN {1; 3} 366Proof 367 rpt strip_tac >> 368 `n MOD 4 < 4` by rw[] >> 369 `n MOD 4 NOTIN {0; 2} <=> n MOD 4 IN {1; 3}` by rw[] >> 370 metis_tac[mod_4_even, EVEN_ODD] 371QED 372 373(* Theorem: (n ** 2) MOD 4 IN {0; 1} *) 374(* Proof: 375 Let m = n MOD 4. 376 Then m < 4 by MOD_LESS 377 (n ** 2) MOD 4 378 = m ** 2 MOD 4 by MOD_EXP 379 = 0 ** 2 MOD 4 or 380 1 ** 2 MOD 4 or 381 2 ** 2 MOD 4 or 382 3 ** 2 MOD 4 by m < 4 383 = 0 or 1 by arithmetic 384*) 385Theorem mod_4_square: 386 !n. (n ** 2) MOD 4 IN {0; 1} 387Proof 388 rpt strip_tac >> 389 qabbrev_tac `m = n MOD 4` >> 390 `m < 4` by rw[MOD_LESS, Abbr`m`] >> 391 `(n ** 2) MOD 4 = m ** 2 MOD 4` by rw[MOD_EXP, Abbr`m`] >> 392 (`(m = 0) \/ (m = 1) \/ (m = 2) \/ (m = 3)` by decide_tac >> fs[]) 393QED 394 395(* Theorem: n MOD 4 = 3 ==> !x y. n <> x ** 2 + y ** 2 *) 396(* Proof: 397 By contradiction, suppose n = x ** 2 + y ** 2. 398 n MOD 4 399 = (x ** 2 + y ** 2) MOD 4 400 = ((x ** 2) MOD 4 + (y ** 2) MOD 4) MOD 4 by MOD_PLUS 401 = (0 or 1 + 0 or 1) MOD 4 by mod_4_square 402 = (0 or 1 or 2) MOD 4 by arithmetic 403 This contradicts n MOD 4 = 3. 404*) 405Theorem mod_4_not_squares: 406 !n. n MOD 4 = 3 ==> !x y. n <> x ** 2 + y ** 2 407Proof 408 rpt strip_tac >> 409 qabbrev_tac `a = x ** 2` >> 410 qabbrev_tac `b = y ** 2` >> 411 `n MOD 4 = ((a MOD 4) + (b MOD 4)) MOD 4` by rw[MOD_PLUS] >> 412 `a MOD 4 IN {0; 1} /\ b MOD 4 IN {0; 1}` by rw[mod_4_square, Abbr`a`, Abbr`b`] >> 413 fs[] 414QED 415 416 417(* Theorem: 2 < n ==> (1 + HALF n < n) *) 418(* Proof: 419 If EVEN n, 420 then 2 * HALF n = n by EVEN_HALF 421 so 2 + 2 * HALF n < n + n by 2 < n 422 or 1 + HALF n < n by arithmetic 423 If ~EVEN n, then ODD n by ODD_EVEN 424 then 1 + 2 * HALF n = 2 by ODD_HALF 425 so 1 + 2 * HALF n < n by 2 < n 426 also 2 + 2 * HALF n < n + n by 1 < n 427 or 1 + HALF n < n by arithmetic 428*) 429Theorem half_add1_lt: 430 !n. 2 < n ==> 1 + HALF n < n 431Proof 432 rpt strip_tac >> 433 Cases_on `EVEN n` >| [ 434 `2 * HALF n = n` by rw[EVEN_HALF] >> 435 decide_tac, 436 `1 + 2 * HALF n = n` by rw[ODD_HALF, ODD_EVEN] >> 437 decide_tac 438 ] 439QED 440 441(* ------------------------------------------------------------------------- *) 442(* Arithmetic Theorems *) 443(* ------------------------------------------------------------------------- *) 444 445(* Theorem: b * d <= a * c ==> 446 (a ** 2 + b ** 2) * (c ** 2 + d ** 2) = 447 (a * d + b * c) ** 2 + (a * c - b * d) ** 2 *) 448(* Proof: 449 (a * d + b * c) ** 2 + (a * c - b * d) ** 2 450 = (a * d) ** 2 + (b * c) ** 2 + 2 * (a * d) * (b * c) + by binomial_add 451 (a * c) ** 2 + (b * d) ** 2 - 2 * (a * c) * (b * d) by binomial_sub 452 = (a * d) ** 2 + (b * c) ** 2 + (a * c) ** 2 + (b * d) ** 2 by arithmetic 453 = a ** 2 * c ** 2 + a ** 2 * d ** 2 + b ** 2 * c ** 2 + b ** 2 * d ** 2 454 = a ** 2 * (c ** 2 + d ** 2) + b ** 2 * (c ** 2 + d ** 2) 455 = (a ** 2 + b ** 2) * (c ** 2 + d ** 2) 456*) 457Theorem four_squares_identity: 458 !a b c d. b * d <= a * c ==> 459 (a ** 2 + b ** 2) * (c ** 2 + d ** 2) = 460 (a * d + b * c) ** 2 + (a * c - b * d) ** 2 461Proof 462 rpt strip_tac >> 463 `(a * d + b * c) ** 2 + (a * c - b * d) ** 2 464 = (a * d) ** 2 + (b * c) ** 2 + 2 * (a * d) * (b * c) + 465 ((a * c) ** 2 + (b * d) ** 2 - 2 * (a * c) * (b * d))` by rw[binomial_add, binomial_sub] >> 466 `_ = (a * d) ** 2 + (b * c) ** 2 + 2 * (a * d) * (b * c) + 467 ((a * c) ** 2 + (b * d) ** 2) - 2 * (a * c) * (b * d)` by rw[binomial_means, LESS_EQ_ADD_SUB] >> 468 `_ = (a * d) ** 2 + (b * c) ** 2 + (a * c) ** 2 + (b * d) ** 2 + 469 2 * a * b * c * d - 2 * a * b * c * d` by decide_tac >> 470 `_ = (a * d) ** 2 + (b * c) ** 2 + (a * c) ** 2 + (b * d) ** 2` by decide_tac >> 471 `_ = a ** 2 * c ** 2 + a ** 2 * d ** 2 + b ** 2 * c ** 2 + b ** 2 * d ** 2` by rw[EXP_BASE_MULT] >> 472 `_ = a ** 2 * (c ** 2 + d ** 2) + b ** 2 * (c ** 2 + d ** 2)` by decide_tac >> 473 `_ = (a ** 2 + b ** 2) * (c ** 2 + d ** 2)` by decide_tac >> 474 decide_tac 475QED 476 477(* Theorem: a * c <= b * d ==> 478 (a ** 2 + b ** 2) * (c ** 2 + d ** 2) = 479 (a * d + b * c) ** 2 + (b * d - a * c) ** 2 *) 480(* Proof: by four_squares_identity, ADD_COMM *) 481Theorem four_squares_identity_alt: 482 !a b c d. a * c <= b * d ==> 483 (a ** 2 + b ** 2) * (c ** 2 + d ** 2) = 484 (a * d + b * c) ** 2 + (b * d - a * c) ** 2 485Proof 486 metis_tac[four_squares_identity, ADD_COMM] 487QED 488 489(* ------------------------------------------------------------------------- *) 490(* Squares Sum Theorems *) 491(* ------------------------------------------------------------------------- *) 492 493(* Theorem: a ** 2 + b ** 2 = 0 <=> a = 0 /\ b = 0 *) 494(* Proof: 495 a ** 2 + b ** 2 = 0 496 <=> a ** 2 = 0 /\ b ** 2 = 0 by ADD_EQ_0 497 <=> a * a = 0 /\ b * b = 0 by EXP_2 498 <=> a = 0 /\ b = 0 by MULT_EQ_0 499*) 500Theorem squares_sum_eq_0: 501 !a b. a ** 2 + b ** 2 = 0 <=> a = 0 /\ b = 0 502Proof 503 rw[EQ_IMP_THM] 504QED 505 506(* Theorem: a ** 2 + b ** 2 = c ** 2 + d ** 2 ==> 507 (a * d - b * c) * (a * d + b * c) = 508 (a ** 2 + b ** 2) * (d ** 2 - b ** 2) *) 509(* Proof: 510 Let p = a ** 2 + b ** 2, 511 then p = c ** 2 + d ** 2. 512 (a * d - b * c) * (a * d + b * c) 513 = (a * d) * (a * d) - (b * c) * (b * c) by difference_of_squares_alt 514 = (a * a) * (d * d) - (c * c) * (b * b) by arithmetic 515 = (p - b * b) * d * d - (p - d * d) * b * b by EXP_2 516 = (p * d * d - b * b * d * d) - (p * b * b - d * d * b * b) 517 = p * d * d - b * b * d * d + d * d * b * b - p * b * b 518 = p * d * d - p * b * b 519 = p * (d * d - b * b) 520 = p * (d ** 2 - b ** 2) by EXP_2 521*) 522Theorem squares_sum_identity_1: 523 !a b c d. a ** 2 + b ** 2 = c ** 2 + d ** 2 ==> 524 (a * d - b * c) * (a * d + b * c) = 525 (a ** 2 + b ** 2) * (d ** 2 - b ** 2) 526Proof 527 rpt strip_tac >> 528 qabbrev_tac `p = a ** 2 + b ** 2` >> 529 `(a * d - b * c) * (a * d + b * c) = (a * d) * (a * d) - (b * c) * (b * c)` by rw[difference_of_squares_alt] >> 530 `_ = (a * a) * (d * d) - (c * c) * (b * b)` by fs[] >> 531 `_ = (a ** 2) * (d ** 2) - (c ** 2) * (b ** 2)` by fs[GSYM EXP_2] >> 532 `_ = (p - b ** 2) * d ** 2 - (p - d ** 2) * b ** 2` by fs[Abbr`p`] >> 533 `_ = (p - b * b) * d * d - (p - d * d) * b * b` by fs[GSYM EXP_2] >> 534 `_ = (p * d * d - b * b * d * d) - (p * b * b - d * d * b * b)` by decide_tac >> 535 `_ = p * d * d - b * b * d * d + d * d * b * b - p * b * b` by simp[] >> 536 `_ = p * d * d - p * b * b` by simp[] >> 537 `_ = p * (d * d - b * b)` by decide_tac >> 538 fs[GSYM EXP_2] 539QED 540 541(* Theorem: a ** 2 + b ** 2 = c ** 2 + d ** 2 ==> 542 (b * c - a * d) * (a * d + b * c) = 543 (a ** 2 + b ** 2) * (b ** 2 - d ** 2) *) 544(* Proof: 545 Let p = a ** 2 + b ** 2, 546 then p = c ** 2 + d ** 2. 547 (b * c - a * d) * (a * d + b * c) 548 = (b * c) * (b * c) - (a * d) * (a * d) by difference_of_squares_alt 549 = (c * c) * (b * b) - (a * a) * (d * d) by arithmetic 550 = (p - d * d) * b * b - (p - b * b) * d * d by EXP_2 551 = (p * b * b - d * d * b * b) - (p * d * d - b * b * d * d) 552 = p * b * b - d * d * b * b + b * b * d * d - p * d * d 553 by SUB_SUB, b * b <= p 554 = p * b * b - p * d * d 555 = p * (b * b - d * d) 556 = p * (b ** 2 - d ** 2) 557*) 558Theorem squares_sum_identity_2: 559 !a b c d. a ** 2 + b ** 2 = c ** 2 + d ** 2 ==> 560 (b * c - a * d) * (a * d + b * c) = 561 (a ** 2 + b ** 2) * (b ** 2 - d ** 2) 562Proof 563 rpt strip_tac >> 564 qabbrev_tac `p = a ** 2 + b ** 2` >> 565 `(b * c - a * d) * (a * d + b * c) = (b * c) * (b * c) - (a * d) * (a * d)` by rw[difference_of_squares_alt] >> 566 `_ = (c * c) * (b * b) - (a * a) * (d * d)` by fs[] >> 567 `_ = (c ** 2) * (b ** 2) - (a ** 2) * (d ** 2)` by fs[GSYM EXP_2] >> 568 `_ = (p - d ** 2) * b * b - (p - b ** 2) * d * d` by fs[Abbr`p`] >> 569 `_ = (p - d * d) * b * b - (p - b * b) * d * d` by fs[GSYM EXP_2] >> 570 `_ = (p * b * b - d * d * b * b) - (p * d * d - b * b * d * d)` by simp[] >> 571 `_ = p * b * b - d * d * b * b + b * b * d * d - p * d * d` by simp[SUB_SUB, GSYM EXP_2, Abbr`p`] >> 572 `_ = p * b * b - p * d * d` by simp[] >> 573 `_ = p * (b * b - d * d)` by decide_tac >> 574 simp[GSYM EXP_2] 575QED 576 577(* Theorem: a ** 2 + b ** 2 = c ** 2 + d ** 2 /\ 0 < b /\ 0 < d ==> 578 a * c < a ** 2 + b ** 2 *) 579(* Proof: 580 Let p = a ** 2 + b ** 2, 581 then p = c ** 2 + d ** 2. 582 Note a * a < p by 0 < b, so 0 < b ** 2 583 and c * c < p by 0 < d, so 0 < d ** 2 584 so a * a * c * c < p * p by LT_MONO_MULT2 585 or (a * c) ** 2 < p ** 2 by EXP_2 586 Hence a * c < p by EXP_EXP_LT_MONO 587*) 588Theorem squares_sum_inequality: 589 !a b c d. a ** 2 + b ** 2 = c ** 2 + d ** 2 /\ 0 < b /\ 0 < d ==> 590 a * c < a ** 2 + b ** 2 591Proof 592 rpt strip_tac >> 593 qabbrev_tac `p = a ** 2 + b ** 2` >> 594 `p = a * a + b * b` by simp[Abbr`p`] >> 595 `p = c * c + d * d` by rfs[] >> 596 `0 < b * b /\ 0 < d * d` by rfs[] >> 597 `a * a < p /\ c * c < p` by decide_tac >> 598 `a * a * (c * c) < p * p` by rw[LT_MONO_MULT2] >> 599 `(a * c) * (a * c) < p * p` by decide_tac >> 600 metis_tac[EXP_EXP_LT_MONO, EXP_2, DECIDE``0 < 2``] 601QED 602 603(* Theorem: a ** 2 + b ** 2 = c ** 2 + d ** 2 /\ 0 < b /\ 0 < c ==> 604 a * d < a ** 2 + b ** 2 *) 605(* Proof: 606 Let p = a ** 2 + b ** 2, 607 then p = c ** 2 + d ** 2. 608 Note a * a < p by 0 < b, so 0 < b ** 2 609 and d * d < p by 0 < c, so 0 < c ** 2 610 so a * a * d * d < p * p by LT_MONO_MULT2 611 or (a * d) ** 2 < p ** 2 by EXP_2 612 Hence a * d < p by EXP_EXP_LT_MONO 613*) 614Theorem squares_sum_inequality_1: 615 !a b c d. a ** 2 + b ** 2 = c ** 2 + d ** 2 /\ 0 < b /\ 0 < c ==> 616 a * d < a ** 2 + b ** 2 617Proof 618 rpt strip_tac >> 619 qabbrev_tac `p = a ** 2 + b ** 2` >> 620 `p = a * a + b * b` by simp[Abbr`p`] >> 621 `p = c * c + d * d` by rfs[] >> 622 `0 < b * b /\ 0 < c * c` by rfs[] >> 623 `a * a < p /\ d * d < p` by decide_tac >> 624 `a * a * (d * d) = (a * d) * (a * d)` by simp[] >> 625 `a * a * (d * d) < p * p` by rw[LT_MONO_MULT2] >> 626 metis_tac[EXP_EXP_LT_MONO, EXP_2, DECIDE``0 < 2``] 627QED 628 629(* Theorem: a ** 2 + b ** 2 = c ** 2 + d ** 2 /\ 0 < a /\ 0 < d ==> 630 b * c < a ** 2 + b ** 2 *) 631(* Proof: by squares_sum_inequality_1, ADD_COMM *) 632Theorem squares_sum_inequality_2: 633 !a b c d. a ** 2 + b ** 2 = c ** 2 + d ** 2 /\ 0 < a /\ 0 < d ==> 634 b * c < a ** 2 + b ** 2 635Proof 636 metis_tac[squares_sum_inequality_1, ADD_COMM] 637QED 638 639(* Theorem: prime p /\ p = a ** 2 + b ** 2 ==> coprime a b *) 640(* Proof: 641 Let g = gcd a b. 642 Then g divides a /\ g divides b by GCD_IS_GREATEST_COMMON_DIVISOR 643 ==> ?h k. (a = h * g) /\ (b = k * g) by divides_def 644 Now p = a * a + b * b by EXP_2 645 = (h * g) * (h * g) + (k * g) * (k * g) 646 = (h * h + k * k) * (g * g) by arithmetic 647 Hence g * g divides p by divides_def 648 or g * g = 1 by prime_def, prime_non_square, square_def 649 ==> g = 1 by SQ_EQ_1 650*) 651Theorem squares_sum_prime_coprime: 652 !p a b. prime p /\ p = a ** 2 + b ** 2 ==> coprime a b 653Proof 654 rpt strip_tac >> 655 qabbrev_tac `g = gcd a b` >> 656 `g divides a /\ g divides b` by rw[GCD_IS_GREATEST_COMMON_DIVISOR, Abbr`g`] >> 657 `?h k. (a = h * g) /\ (b = k * g)` by metis_tac[divides_def] >> 658 `p = a * a + b * b` by simp[] >> 659 `_ = (h * g) * (h * g) + (k * g) * (k * g)` by metis_tac[] >> 660 `_ = (h * h + k * k) * (g * g)` by simp[] >> 661 `g * g divides p` by metis_tac[divides_def] >> 662 `g * g = 1` by metis_tac[prime_def, prime_non_square, square_def] >> 663 fs[SQ_EQ_1] 664QED 665 666(* Theorem: prime p /\ p = a ** 2 + b ** 2 /\ p = c ** 2 + d ** 2 /\ 667 a * d = b * c ==> a = c /\ b = d *) 668(* Proof: 669 Note p <> 0 by NOT_PRIME_0 670 and a <> 0 by prime_non_square, square_def, MULT_EQ_0 671 and gcd a b = 1 by squares_sum_prime_coprime 672 Now a divides (b * c) by divides_def, MULT_COMM, a * d = b * c 673 so a divides c by euclid_coprime, GCD_SYM 674 ==> ?k. c = k * a by divides_def 675 Thus d * a = b * (k * a) 676 = (k * b) * a 677 or d = k * b by EQ_MULT_RCANCEL, a <> 0 678 679 p = c * c + d * d by EXP_2 680 = (k * a) * (k * a) + (k * b) * (k * b) 681 = k * k * (a * a + b * b) 682 = k * k * p 683 Thus k * k = 1 by EQ_MULT_RCANCEL 684 so k = 1 by MULT_EQ_1 685 Hence c = k * a = a, d = k * b = b. 686*) 687Theorem squares_sum_prime_thm: 688 !p a b c d. prime p /\ 689 p = a ** 2 + b ** 2 /\ p = c ** 2 + d ** 2 /\ 690 a * d = b * c ==> a = c /\ b = d 691Proof 692 spose_not_then strip_assume_tac >> 693 qabbrev_tac `p = a ** 2 + b ** 2` >> 694 `p <> 0` by metis_tac[NOT_PRIME_0] >> 695 `a <> 0` by metis_tac[prime_non_square, square_def, EXP_2, MULT_EQ_0, ADD] >> 696 `gcd a b = 1` by metis_tac[squares_sum_prime_coprime] >> 697 `a divides (b * c)` by metis_tac[divides_def, MULT_COMM] >> 698 `a divides c` by metis_tac[euclid_coprime, GCD_SYM] >> 699 `?k. c = k * a` by metis_tac[divides_def] >> 700 `d * a = b * (k * a)` by fs[] >> 701 `_ = (k * b) * a` by fs[] >> 702 `d = k * b` by metis_tac[EQ_MULT_RCANCEL] >> 703 `p = c * c + d * d` by simp[] >> 704 `_ = (k * a) * (k * a) + (k * b) * (k * b)` by metis_tac[] >> 705 `_ = k * k * (a * a + b * b)` by decide_tac >> 706 `_ = k * k * p` by fs[Abbr`p`] >> 707 `k * k = 1` by metis_tac[EQ_MULT_RCANCEL, MULT_LEFT_1] >> 708 metis_tac[MULT_EQ_1, MULT_LEFT_1] 709QED 710 711(* ------------------------------------------------------------------------- *) 712(* Set Theorems *) 713(* ------------------------------------------------------------------------- *) 714 715(* Theorem: {a; b} = {c; d} <=> a = c /\ b = d \/ a = d /\ b = c *) 716(* Proof: by EXTENSION. *) 717Theorem doublet_eq: 718 !a b c d. {a; b} = {c; d} <=> a = c /\ b = d \/ a = d /\ b = c 719Proof 720 simp[EXTENSION] >> 721 metis_tac[] 722QED 723 724(* Theorem: FINITE {a; b} *) 725(* Proof: 726 Since {a; b} = b INSERT (a INSERT {}) by notation 727 and FINITE {} by FINITE_EMPTY 728 hence FINITE {a; b} by FINITE_INSERT 729*) 730Theorem doublet_finite: 731 !a b. FINITE {a; b} 732Proof 733 rw[] 734QED 735 736(* Theorem: a <> b ==> CARD {a; b} = 2 *) 737(* Proof: 738 Since {a; b} = b INSERT (a INSERT {}) by notation 739 and CARD {} = 0 by CARD_EMPTY 740 hence CARD {a; b} = 2 by CARD_DEF 741*) 742Theorem doublet_card: 743 !a b. a <> b ==> CARD {a; b} = 2 744Proof 745 rw[] 746QED 747 748(* Theorem: FINITE s /\ s = a UNION b UNION c /\ 749 a INTER b = {} /\ b INTER c = {} /\ a INTER c = {} /\ 750 CARD a = CARD c ==> CARD s = 2 * CARD a + CARD b *) 751(* Proof: 752 Note FINITE a /\ FINITE b /\ FINITE c by FINITE_UNION 753 and a INTER b INTER c = EMPTY by INTER_EMPTY 754 CARD s 755 = CARD (a UNION b UNION c) by s = a UNION b UNION c 756 = CARD a + CARD b + CARD c + CARD (a INTER b INTER c) 757 - CARD (a INTER b) - CARD (b INTER c) - CARD (a INTER c) 758 by CARD_UNION_3_EQN 759 = CARD a + CARD b + CARD c by CARD_EMPTY 760 = CARD a + CARD b + CARD a by CARD c = CARD a 761 = 2 * CARD a + CARD b by arithmetic 762*) 763Theorem partition_three_special_card: 764 !s a b c. FINITE s /\ s = a UNION b UNION c /\ 765 a INTER b = {} /\ b INTER c = {} /\ a INTER c = {} /\ 766 CARD a = CARD c ==> CARD s = 2 * CARD a + CARD b 767Proof 768 rpt strip_tac >> 769 `FINITE a /\ FINITE b /\ FINITE c` by metis_tac[FINITE_UNION] >> 770 rw[CARD_UNION_3_EQN] 771QED 772 773(* Theorem: FINITE s /\ s = a UNION b /\ a INTER b = {} /\ BIJ f a b ==> 774 CARD s = 2 * CARD a *) 775(* Proof: 776 Note a SUBSET s /\ b SUBSET s by SUBSET_UNION 777 so FINITE a /\ FINITE b by SUBSET_FINITE 778 Now BIJ f a b by given 779 ==> CARD a = CARD b by FINITE_BIJ_CARD 780 CARD s 781 = CARD a + CARD b - CARD (a INTER b) by CARD_UNION_EQN 782 = CARD a + CARD a by CARD_EMPTY 783 = 2 * CARD a by arithmetic 784*) 785Theorem set_partition_bij_card: 786 !f s a b. FINITE s /\ s = a UNION b /\ a INTER b = {} /\ BIJ f a b ==> 787 CARD s = 2 * CARD a 788Proof 789 rpt strip_tac >> 790 `FINITE a /\ FINITE b` by metis_tac[SUBSET_UNION, SUBSET_FINITE] >> 791 `CARD a = CARD b` by metis_tac[FINITE_BIJ_CARD] >> 792 `CARD s = CARD a + CARD a` by rw[CARD_UNION_EQN] >> 793 decide_tac 794QED 795 796(* Theorem: FINITE s /\ (s = a UNION b) /\ (a INTER b = EMPTY) /\ BIJ f a b ==> 797 EVEN (CARD s) *) 798(* Proof: 799 Note CARD s = 2 * CARD a by set_partition_bij_card 800 ==> EVEN (CARD s) by EVEN_DOUBLE 801*) 802Theorem set_partition_bij_card_even: 803 !f s a b. FINITE s /\ s = a UNION b /\ a INTER b = {} /\ BIJ f a b ==> 804 EVEN (CARD s) 805Proof 806 metis_tac[set_partition_bij_card, EVEN_DOUBLE] 807QED 808 809(* Theorem: s = a UNION b /\ a INTER b = {} /\ 810 t = c UNION d /\ c INTER d = {} /\ 811 BIJ f a d /\ BIJ f b c ==> BIJ f s t *) 812(* Proof: by BIJ_DEF, SURJ_DEF, INJ_DEF *) 813Theorem set_partition_bij_give_bij: 814 !f s t a b c d. 815 s = a UNION b /\ a INTER b = {} /\ 816 t = c UNION d /\ c INTER d = {} /\ 817 BIJ f a d /\ BIJ f b c ==> BIJ f s t 818Proof 819 (rw[BIJ_DEF, SURJ_DEF, INJ_DEF] >> simp[]) >> 820 metis_tac[IN_INTER, MEMBER_NOT_EMPTY] 821QED 822 823(* ------------------------------------------------------------------------- *) 824(* WHILE Loop Specification. *) 825(* ------------------------------------------------------------------------- *) 826 827(* Taken from ringInstances, for multiplicative order computation by WHILE. *) 828 829(* HOL4 can evaluate WHILE directly: 830 831> EVAL ``WHILE (\i. i <= 4) SUC 1``; 832val it = |- WHILE (\i. i <= 4) SUC 1 = 5: thm 833*) 834 835(* 836For WHILE Guard Cmd, 837we want to show: 838 {Pre-condition} WHILE Guard Command {Post-condition} 839 840> WHILE_RULE; 841val it = |- !R B C. WF R /\ (!s. B s ==> R (C s) s) ==> 842 HOARE_SPEC (\s. P s /\ B s) C P ==> 843 HOARE_SPEC P (WHILE B C) (\s. P s /\ ~B s): thm 844 845> HOARE_SPEC_DEF; 846val it = |- !P C Q. HOARE_SPEC P C Q <=> !s. P s ==> Q (C s): thm 847*) 848 849(* Idea: For a command Command on x, 850 if x is invariant and allowed by guard before command, 851 and keeps the invariant after the command, 852 then putting command in WHILE loop with guard to continue 853 will transform x from Precond to Postcond, when: 854 (a) invariant and guard implies a shrinking measure, 855 (b) pre-condition implies invariant, 856 (c) invarant and opposite of guard implies post-condition 857*) 858 859(* Theorem: (!x. Invariant x /\ Guard x ==> Measure (Command x) < Measure x) /\ 860 (!x. Precond x ==> Invariant x) /\ 861 (!x. Invariant x /\ ~Guard x ==> Postcond x) /\ 862 HOARE_SPEC (\x. Invariant x /\ Guard x) Command Invariant ==> 863 HOARE_SPEC Precond (WHILE Guard Command) Postcond *) 864(* Proof: 865 By HOARE_SPEC_DEF, change the goal to show: 866 !s. Invariant s ==> Postcond (WHILE Guard Command s) 867 By complete induction on (Measure s). 868 After rewrite by WHILE, this is to show: 869 Postcond (if Guard s then WHILE Guard Command (Command s) else s) 870 If Guard s, 871 With Invariant s, 872 ==> Postcond (WHILE Guard Command (Command s)) 873 by induction hypothesis 874 If ~(Guard s), 875 With Invariant s, 876 ==> Postcond s by given 877*) 878Theorem WHILE_RULE_PRE_POST: 879 (!x. Invariant x /\ Guard x ==> Measure (Command x) < Measure x) /\ 880 (!x. Precond x ==> Invariant x) /\ 881 (!x. Invariant x /\ ~Guard x ==> Postcond x) /\ 882 HOARE_SPEC (\x. Invariant x /\ Guard x) Command Invariant ==> 883 HOARE_SPEC Precond (WHILE Guard Command) Postcond 884Proof 885 simp[HOARE_SPEC_DEF] >> 886 rpt strip_tac >> 887 `!s. Invariant s ==> Postcond (WHILE Guard Command s)` suffices_by metis_tac[] >> 888 Q.UNDISCH_THEN `Precond s` (K ALL_TAC) >> 889 rpt strip_tac >> 890 completeInduct_on `Measure s` >> 891 rpt strip_tac >> 892 fs[PULL_FORALL] >> 893 first_x_assum (qspec_then `Measure` assume_tac) >> 894 rfs[] >> 895 ONCE_REWRITE_TAC[WHILE] >> 896 Cases_on `Guard s` >- 897 simp[] >> 898 simp[] 899QED 900 901(* ------------------------------------------------------------------------- *) 902 903(* export theory at end *) 904val _ = export_theory(); 905 906(*===========================================================================*) 907