1(* ------------------------------------------------------------------------- *) 2(* Binomial coefficients and expansion, for Ring *) 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 "ringBinomial"; 12 13(* ------------------------------------------------------------------------- *) 14 15 16 17(* val _ = load "jcLib"; *) 18open jcLib; 19 20(* open dependent theories *) 21open pred_setTheory listTheory arithmeticTheory; 22 23(* val _ = load "binomialTheory"; *) 24open binomialTheory; 25open dividesTheory; 26 27(* Get dependent theories local *) 28(* (* val _ = load "groupTheory"; *) *) 29(* (* val _ = load "groupInstancesTheory"; *) *) 30(* val _ = load "ringMapTheory"; *) 31open ringTheory; 32open groupTheory; 33open monoidTheory; 34open monoidMapTheory groupMapTheory ringMapTheory; 35 36(* Get dependent theories in lib *) 37(* (* val _ = load "helperNumTheory"; -- in monoidTheory *) *) 38(* (* val _ = load "helperSetTheory"; -- in monoidTheory *) *) 39open helperNumTheory helperSetTheory; 40 41 42(* ------------------------------------------------------------------------- *) 43(* Ring Binomial Documentation *) 44(* ------------------------------------------------------------------------- *) 45(* 46 Overloading: 47 rlist = ring_list r 48 rsum = ring_sum r 49 rfun = ring_fun r 50*) 51(* Definitions and Theorems (# are exported): 52 53 List from elements in Ring: 54# ring_list_def |- (!r. rlist [] <=> T) /\ !r h t. rlist (h::t) <=> h IN R /\ rlist t 55 ring_list_nil |- !r. rlist [] <=> T 56 ring_list_cons |- !r h t. rlist (h::t) <=> h IN R /\ rlist t 57 ring_list_front_last |- !s. rlist (FRONT s) /\ LAST s IN R ==> rlist s 58 ring_list_SNOC |- !x s. rlist (SNOC x s) <=> x IN R /\ rlist s 59 60 Summation in Ring: 61# ring_sum_def |- (!r. rsum [] = #0) /\ !r h t. rsum (h::t) = h + rsum t 62 ring_sum_nil |- !r. rsum [] = #0 63 ring_sum_cons |- !r h t. rsum (h::t) = h + rsum t 64# ring_sum_element |- !r. Ring r ==> !s. rlist s ==> rsum s IN R 65 ring_sum_sing |- !r. Ring r ==> !x. x IN R ==> (rsum [x] = x) 66 ring_sum_append |- !r. Ring r ==> !s t. rlist s /\ rlist t ==> (rsum (s ++ t) = rsum s + rsum t) 67 ring_sum_mult |- !r. Ring r ==> !k s. k IN R /\ rlist s ==> (k * rsum s = rsum (MAP (\x. k * x) s)) 68 ring_sum_mult_ladd |- !r. Ring r ==> !m n s. m IN R /\ n IN R /\ rlist s ==> 69 ((m + n) * rsum s = rsum (MAP (\x. m * x) s) + rsum (MAP (\x. n * x) s)) 70 ring_sum_SNOC |- !r. Ring r ==> !k s. k IN R /\ rlist s ==> (rsum (SNOC k s) = rsum s + k) 71 72 Function giving elements in Ring: 73# ring_fun_def |- !r f. rfun f <=> !x. f x IN R 74 ring_fun_add |- !r. Ring r ==> !a b. rfun a /\ rfun b ==> rfun (\k. a k + b k) 75 ring_fun_genlist |- !f. rfun f ==> !n. rlist (GENLIST f n) 76 ring_fun_map |- !f l. rfun f ==> rlist (MAP f l) 77 ring_fun_from_ring_fun |- !r. Ring r ==> !f. rfun f ==> !x. x IN R ==> rfun (\j. f j * x ** j) 78 ring_fun_from_ring_fun_exp |- !r. Ring r ==> !f. rfun f ==> !x. x IN R ==> 79 !n. rfun (\j. (f j * x ** j) ** n) 80 ring_list_gen_from_ring_fun |- !r. Ring r ==> !f. rfun f ==> !x. x IN R ==> 81 !n. rlist (GENLIST (\j. f j * x ** j) n) 82 ring_list_from_genlist_ring_fun |- !r f. rfun f ==> !n g. rlist (GENLIST (f o g) n) 83 ring_list_from_genlist |- !r f. rfun f ==> !n. rlist (GENLIST f n) 84 85 Ring Sum Involving GENLIST: 86 ring_sum_fun_zero |- !r. Ring r ==> !f. rfun f ==> !n. (!k. 0 < k /\ k < n ==> 87 (f k = #0)) ==> (rsum (MAP f (GENLIST SUC (PRE n))) = #0) 88 89 ring_sum_decompose_first |- !r f n. rsum (GENLIST f (SUC n)) = f 0 + rsum (GENLIST (f o SUC) n) 90 ring_sum_decompose_last |- !r. Ring r ==> !f n. rfun f ==> (rsum (GENLIST f (SUC n)) = rsum (GENLIST f n) + f n) 91 ring_sum_decompose_first_last |- !r. Ring r ==> !f n. rfun f /\ 0 < n ==> 92 (rsum (GENLIST f (SUC n)) = f 0 + rsum (GENLIST (f o SUC) (PRE n)) + f n) 93 ring_sum_genlist_add |- !r. Ring r ==> !a b. rfun a /\ rfun b ==> 94 !n. rsum (GENLIST a n) + rsum (GENLIST b n) = rsum (GENLIST (\k. a k + b k) n) 95 ring_sum_genlist_append |- !r. Ring r ==> !a b. rfun a /\ rfun b ==> 96 !n. rsum (GENLIST a n ++ GENLIST b n) = rsum (GENLIST (\k. a k + b k) n) 97 ring_sum_genlist_sum |- !r. Ring r ==> !f. rfun f ==> 98 !n m. rsum (GENLIST f (n + m)) = rsum (GENLIST f m) + rsum (GENLIST (\k. f (k + m)) n) 99 ring_sum_genlist_const |- !r. Ring r ==> !x. x IN R ==> !n. rsum (GENLIST (K x) n) = ##n * x 100 101 Ring Binomial Theorem: 102 ring_binomial_genlist_index_shift |- !r. Ring r ==> !x y. x IN R /\ y IN R ==> 103 !n. GENLIST ((\k. ##(binomial n k) * x ** SUC (n - k) * y ** k) o SUC) n = 104 GENLIST (\k. ##(binomial n (SUC k)) * x ** (n - k) * y ** SUC k) n 105 ring_binomial_index_shift |- !r. Ring r ==> !x y. x IN R /\ y IN R ==> 106 !n. (\k. ##(binomial (SUC n) k) * x ** (SUC n - k) * y ** k) o SUC = 107 (\k. ##(binomial (SUC n) (SUC k)) * x ** (n - k) * y ** SUC k) 108 ring_binomial_term_merge_x |- !r. Ring r ==> !x y. x IN R /\ y IN R ==> 109 !n. (\k. x * k) o (\k. ##(binomial n k) * x ** (n - k) * y ** k) = (\k. ##(binomial n k) * x ** SUC (n - k) * y ** k) 110 ring_binomial_term_merge_y |- !r. Ring r ==> !x y. x IN R /\ y IN R ==> 111 !n. (\k. y * k) o (\k. ##(binomial n k) * x ** (n - k) * y ** k) = (\k. ##(binomial n k) * x ** (n - k) * y ** SUC k) 112 ring_binomial_thm |- !r. Ring r ==> !x y. x IN R /\ y IN R ==> 113 !n. (x + y) ** n = rsum (GENLIST (\k. ##(binomial n k) * x ** (n - k) * y ** k) (SUC n)) 114 115 Ring with prime characteristic: 116 ring_char_prime |- !r. Ring r ==> (prime (char r) <=> 117 1 < char r /\ !k. 0 < k /\ k < char r ==> (##(binomial (char r) k) = #0)) 118 ring_freshman_thm |- !r. Ring r /\ prime (char r) ==> !x y. x IN R /\ y IN R ==> 119 ((x + y) ** char r = x ** char r + y ** char r) 120 ring_freshman_all |- !r. Ring r /\ prime (char r) ==> !x y. x IN R /\ y IN R ==> 121 !n. (x + y) ** char r ** n = x ** char r ** n + y ** char r ** n 122 ring_freshman_thm_sub |- !r. Ring r /\ prime (char r) ==> !x y. x IN R /\ y IN R ==> 123 ((x - y) ** char r = x ** char r - y ** char r) 124 ring_freshman_all_sub |- !r. Ring r /\ prime (char r) ==> !x y. x IN R /\ y IN R ==> 125 !n. (x - y) ** char r ** n = x ** char r ** n - y ** char r ** n 126 ring_fermat_thm |- !r. Ring r /\ prime (char r) ==> !n. (##n) ** (char r) = (##n) 127 ring_fermat_all |- !r. Ring r /\ prime (char r) ==> !n k. ##n ** char r ** k = ##n 128 ring_sum_freshman_thm |- !r. Ring r /\ prime (char r) ==> !f. rfun f ==> !x. x IN R ==> 129 !n. rsum (GENLIST (\j. f j * x ** j) n) ** char r = 130 rsum (GENLIST (\j. (f j * x ** j) ** char r) n) 131 ring_sum_freshman_all |- !r. Ring r /\ prime (char r) ==> !f. rfun f ==> !x. x IN R ==> 132 !n k. rsum (GENLIST (\j. f j * x ** j) n) ** char r ** k = 133 rsum (GENLIST (\j. (f j * x ** j) ** char r ** k) n) 134 ring_char_prime_endo |- !r. Ring r /\ prime (char r) ==> RingEndo (\x. x ** char r) r 135*) 136 137(* 138binomial_thm: 139!n x y. (x + y)**n = rsum (GENLIST (\k. (binomial n k)* x**(n-k) * y**k) (SUC n)) 140*) 141 142(* ------------------------------------------------------------------------- *) 143(* List from elements in Ring *) 144(* ------------------------------------------------------------------------- *) 145 146(* Ring element list. *) 147val ring_list_def = Define` 148 (ring_list (r:'a ring) [] <=> T) /\ 149 (ring_list (r:'a ring) ((h:'a)::(t:'a list)) <=> h IN R /\ (ring_list r t)) 150`; 151val _ = overload_on ("rlist", ``ring_list r``); 152 153(* export simple definition. *) 154val _ = export_rewrites ["ring_list_def"]; 155 156(* Theorem: rlist [] <=> T *) 157val ring_list_nil = save_thm("ring_list_nil", ring_list_def |> CONJUNCT1); 158(* > val ring_list_nil = |- !r. rlist [] <=> T : thm *) 159 160(* Theorem: rlist (h::t) <=> h IN R /\ rlist t *) 161val ring_list_cons = save_thm("ring_list_cons", ring_list_def |> CONJUNCT2); 162(* > val ring_list_cons = |- !r h t. rlist (h::t) <=> h IN R /\ rlist t : thm *) 163 164 165(* Theorem: rlist (FRONT l) /\ LAST l IN R ==> rlist l *) 166(* Proof: by induction on s. 167 Base case: rlist (FRONT []) ==> LAST [] IN R ==> rlist [] 168 true since rlist [] by ring_list_nil. 169 Step case: rlist (FRONT s) ==> LAST s IN R ==> rlist s ==> 170 !h. rlist (FRONT (h::s)) ==> LAST (h::s) IN R ==> rlist (h::s) 171 If s = [], 172 FRONT (h::[]) = [], LAST (h::[]) = h, by FRONT_CONS and LAST_CONS, 173 hence rlist [] /\ h IN R, hence rlist (h::[]) by ring_list_cons. 174 If s <> [], s = h'::t 175 FRONT (h::s) = h::FRONT s, LAST (h::s) = LAST s, by FRONT_CONS and LAST_CONS, 176 hence rlist (h::FRONT s) /\ LAST s IN R, 177 or h IN R /\ rlist (FRONT s) /\ LAST s IN R by ring_list_cons 178 or h IN R /\ rlist s by induction hypothesis 179 hence rlist (h::s) by ring_list_cons 180*) 181val ring_list_front_last = store_thm( 182 "ring_list_front_last", 183 ``!s. rlist (FRONT s) /\ LAST s IN R ==> rlist s``, 184 rpt strip_tac >> 185 Induct_on `s` >- 186 rw[] >> 187 metis_tac[FRONT_CONS, LAST_CONS, ring_list_def, list_CASES]); 188 189(* Theorem: !x s. rlist (SNOC x s) <=> x IN R /\ rlist s *) 190(* Proof: 191 By induction on s. 192 Base case: rlist (SNOC x []) <=> x IN R /\ rlist [] 193 rlist (SNOC x []) 194 <=> rlist [x] by SNOC 195 <=> x IN R /\ rlist [] by ring_list_cons 196 Step case: rlist (SNOC x s) <=> x IN R /\ rlist s ==> 197 !h. rlist (SNOC x (h::s)) <=> x IN R /\ rlist (h::s) 198 rlist (SNOC x (h::s)) 199 <=> rlist (h::SONC x s) by SNOC 200 <=> h IN R /\ rlist (SNOC x s) by ring_list_cons 201 <=> h IN R /\ x IN R /\ rlist s by induction hypothesis 202 <=> x IN R /\ rlist (h::s) by ring_list_cons 203*) 204val ring_list_SNOC = store_thm( 205 "ring_list_SNOC", 206 ``!x s. rlist (SNOC x s) <=> x IN R /\ rlist s``, 207 rpt strip_tac >> 208 Induct_on `s` >- 209 rw[] >> 210 rw[] >> 211 metis_tac[]); 212 213(* ------------------------------------------------------------------------- *) 214(* Summation in Ring *) 215(* ------------------------------------------------------------------------- *) 216 217(* Summation in a Ring. *) 218val ring_sum_def = Define` 219 (ring_sum (r:'a ring) [] = #0) /\ 220 (ring_sum (r:'a ring) ((h:'a)::(t:'a list)) = h + (ring_sum r t)) 221`; 222val _ = overload_on ("rsum", ``ring_sum r``); 223 224(* export simple definition. *) 225val _ = export_rewrites ["ring_sum_def"]; 226 227(* Theorem: rsum [] = #0 *) 228val ring_sum_nil = save_thm("ring_sum_nil", ring_sum_def |> CONJUNCT1); 229(* > val ring_sum_nil = |- !r. rsum [] = #0 : thm *) 230 231(* Theorem: rsum (h::t)= h + rsum t *) 232val ring_sum_cons = save_thm("ring_sum_cons", ring_sum_def |> CONJUNCT2); 233(* > val ring_sum_cons = |- !r h t. rsum (h::t) = h + rsum t : thm *) 234 235(* Theorem: rsum s IN R *) 236(* Proof: by induction on s. 237 Base case: rlist [] ==> rsum [] IN R 238 true by ring_sum_nil, ring_zero_element. 239 Step case: rlist s ==> rsum s IN R ==> !h. rlist (h::s) ==> rsum (h::s) IN R 240 rlist (h::s) ==> h IN R /\ rlist s by ring_list_cons 241 since ring_sum(h::s) = h + rsum s by ring_sum_cons 242 with h IN R and rlist s ==> rsum s IN R by induction hypothesis 243 true by ring_add_element 244*) 245val ring_sum_element = store_thm( 246 "ring_sum_element", 247 ``!r:'a ring. Ring r ==> !s. rlist s ==> rsum s IN R``, 248 rpt strip_tac >> 249 Induct_on `s` >> 250 rw[]); 251 252val _ = export_rewrites ["ring_sum_element"]; 253 254(* Theorem: rsum [x] = x *) 255(* Proof: 256 rsum [x] 257 = x + rsum [] by ring_sum_cons 258 = x + #0 by ring_sum_nil 259 = x by ring_add_rzero 260*) 261val ring_sum_sing = store_thm( 262 "ring_sum_sing", 263 ``!r:'a ring. Ring r ==> !x. x IN R ==> (rsum [x] = x)``, 264 rw[]); 265 266(* Theorem: rsum (s ++ t) = rsum s + rsum t *) 267(* Proof: by induction on s 268 Base case: rlist [] ==> (rsum ([] ++ t) = rsum [] + rsum t) 269 rsum ([] ++ t) 270 = rsum t by APPEND 271 = #0 + rsum t by ring_add_lzero 272 = rsum [] + rsum t by ring_sum_nil 273 Step case: rlist s /\ rlist t ==> (rsum (s ++ t) = rsum s + rsum t) ==> 274 rlist (h::s) ==> (rsum (h::s ++ t) = rsum (h::s) + rsum t) 275 rsum (h::s ++ t) 276 = rsum (h::(s ++ t)) by APPEND 277 = h + rsum (s ++ t) by ring_sum_cons, h IN R by ring_list_cons 278 = h + (rsum s + rsum t) by induction hypothesis 279 = (h + rsum s) + rsum t by ring_add_assoc 280 = rsum (h::s) + rsum t by ring_sum_cons 281*) 282val ring_sum_append = store_thm( 283 "ring_sum_append", 284 ``!r:'a ring. Ring r ==> !s t. rlist s /\ rlist t ==> (rsum (s ++ t) = rsum s + rsum t)``, 285 rpt strip_tac >> 286 Induct_on `s` >> 287 rw[ring_add_assoc]); 288 289(* Theorem: constant multiplication: k * rsum s = rsum (MAP (\x. k*x) s)) *) 290(* Proof: by induction on s 291 Base case: k * rsum [] = rsum (MAP (\x. k * x) []) 292 LHS = k * rsum [] 293 = k * #0 by ring_sum_nil 294 = #0 by ring_mult_rzero 295 RHS = rsum (MAP (\x. k * x) []) 296 = rsum [] by MAP 297 = #0 by ring_sum_nil 298 = LHS 299 Step case: rlist s ==> (k * rsum s = rsum (MAP (\x. k * x) s)) ==> 300 !h. rlist (h::s) ==> (k * rsum (h::s) = rsum (MAP (\x. k * x) (h::s))) 301 LHS = k * rsum (h::s) 302 = k * (h + rsum s) by ring_sum_cons 303 = k * h + k * rsum s by ring_mult_radd 304 = k * h + rsum (MAP (\x. k * x) s) by induction hypothesis 305 RHS = rsum (MAP (\x. k * x) (h::s)) 306 = rsum ((\x. k * x) h :: MAP (\x. k * x) s) by MAP 307 = (\x. k * x) h + rsum (MAP (\x. k * x) s) by ring_sum_cons 308 = k * h + rsum (MAP (\x. k * x) s 309 = LHS 310*) 311val ring_sum_mult = store_thm( 312 "ring_sum_mult", 313 ``!r:'a ring. Ring r ==> !k s. k IN R /\ rlist s ==> (k * rsum s = rsum (MAP (\x. k*x) s))``, 314 rpt strip_tac >> 315 Induct_on `s` >> 316 rw[]); 317 318(* Theorem: (m+n) * rsum s = rsum (MAP (\x. m*x) s) + rsum (MAP (\x. n*x) s) *) 319(* Proof: 320 (m + n) * rsum s 321 = m * rsum s + n * rsum s by ring_mult_ladd 322 = rsum (MAP (\x. m*x) s) + rsum (MAP (\x. n*x) s) by ring_sum_mult 323*) 324val ring_sum_mult_ladd = store_thm( 325 "ring_sum_mult_ladd", 326 ``!r:'a ring. Ring r ==> !m n s. m IN R /\ n IN R /\ rlist s ==> 327 ((m + n) * rsum s = rsum (MAP (\x. m*x) s) + rsum (MAP (\x. n*x) s))``, 328 rw[ring_sum_mult, ring_mult_ladd]); 329 330(* 331- EVAL ``GENLIST I 4``; 332> val it = |- GENLIST I 4 = [0; 1; 2; 3] : thm 333- EVAL ``GENLIST SUC 4``; 334> val it = |- GENLIST SUC 4 = [1; 2; 3; 4] : thm 335- EVAL ``GENLIST (\k. binomial 4 k) 5``; 336> val it = |- GENLIST (\k. binomial 4 k) 5 = [1; 4; 6; 4; 1] : thm 337- EVAL ``GENLIST (\k. binomial 5 k) 6``; 338> val it = |- GENLIST (\k. binomial 5 k) 6 = [1; 5; 10; 10; 5; 1] : thm 339- EVAL ``GENLIST (\k. binomial 10 k) 11``; 340> val it = |- GENLIST (\k. binomial 10 k) 11 = [1; 10; 45; 120; 210; 252; 210; 120; 45; 10; 1] : thm 341*) 342 343(* Theorems on GENLIST: 344 345- GENLIST; 346> val it = |- (!f. GENLIST f 0 = []) /\ 347 !f n. GENLIST f (SUC n) = SNOC (f n) (GENLIST f n) : thm 348- NULL_GENLIST; 349> val it = |- !n f. NULL (GENLIST f n) <=> (n = 0) : thm 350- GENLIST_CONS; 351> val it = |- GENLIST f (SUC n) = f 0::GENLIST (f o SUC) n : thm 352- EL_GENLIST; 353> val it = |- !f n x. x < n ==> (EL x (GENLIST f n) = f x) : thm 354- EXISTS_GENLIST; 355> val it = |- !n. EXISTS P (GENLIST f n) <=> ?i. i < n /\ P (f i) : thm 356- EVERY_GENLIST; 357> val it = |- !n. EVERY P (GENLIST f n) <=> !i. i < n ==> P (f i) : thm 358- MAP_GENLIST; 359> val it = |- !f g n. MAP f (GENLIST g n) = GENLIST (f o g) n : thm 360- GENLIST_APPEND; 361> val it = |- !f a b. GENLIST f (a + b) = GENLIST f b ++ GENLIST (\t. f (t + b)) a : thm 362- HD_GENLIST; 363> val it = |- HD (GENLIST f (SUC n)) = f 0 : thm 364- TL_GENLIST; 365> val it = |- !f n. TL (GENLIST f (SUC n)) = GENLIST (f o SUC) n : thm 366- HD_GENLIST_COR; 367> val it = |- !n f. 0 < n ==> (HD (GENLIST f n) = f 0) : thm 368- GENLIST_FUN_EQ; 369> val it = |- !n f g. (GENLIST f n = GENLIST g n) <=> !x. x < n ==> (f x = g x) : thm 370 371*) 372 373(* Theorem: rsum (SNOC h s) = (rsum s) + h *) 374(* Proof: by induction on s. 375 Base case: (rsum (SNOC k []) = rsum [] + k) 376 rsum (SNOC k []) 377 = rsum [k] by SNOC 378 = k + #0 by ring_sum_cons, ring_sum_nil 379 = k by ring_add_rzero 380 = #0 + k by ring_add_lzero 381 = rsum [] + k by ring_sum_nil 382 Step case: rlist s ==> (rsum (SNOC k s) = rsum s + k) ==> 383 !h. rlist (h::s) ==> (rsum (SNOC k (h::s)) = rsum (h::s) + k) 384 rsum (SNOC k (h::s)) 385 = rsum (h::SNOC k s) by SNOC 386 = h + rsum (SNOC k s) by ring_sum_cons 387 = h + (rsum s + k) by induction hypothesis 388 = (h + rsum s) + k by ring_add_assoc, ring_sum_element 389 = rsum(h::s) + k by ring_sum_cons 390*) 391val ring_sum_SNOC = store_thm( 392 "ring_sum_SNOC", 393 ``!r:'a ring. Ring r ==> !k s. k IN R /\ rlist s ==> (rsum (SNOC k s) = (rsum s) + k)``, 394 rpt strip_tac >> 395 Induct_on `s` >> 396 rw[ring_add_assoc]); 397 398(* ------------------------------------------------------------------------- *) 399(* Function giving elements in Ring *) 400(* ------------------------------------------------------------------------- *) 401 402(* Ring element function. *) 403val ring_fun_def = Define` 404 ring_fun (r:'a ring) f <=> !x. f x IN R 405`; 406val _ = overload_on ("rfun", ``ring_fun r``); 407 408(* export simple definition. *) 409val _ = export_rewrites ["ring_fun_def"]; 410 411(* Theorem: rfun a /\ rfun b ==> rfun (\k. a k + b k) *) 412(* Proof: by ring_add_element. *) 413val ring_fun_add = store_thm( 414 "ring_fun_add", 415 ``!r:'a ring. Ring r ==> !a b. rfun a /\ rfun b ==> rfun (\k. a k + b k)``, 416 rw[]); 417 418(* Theorem: rfun f ==> rlist (GENLIST f n) *) 419(* Proof: by induction on n. 420 Base case: rlist (GENLIST f 0) 421 Since GENLIST f 0 = [] by GENLIST 422 hence true by ring_list_nil. 423 Step case: rlist (GENLIST f n) ==> rlist (GENLIST f (SUC n)) 424*) 425val ring_fun_genlist = store_thm( 426 "ring_fun_genlist", 427 ``!f. rfun f ==> !n. rlist (GENLIST f n)``, 428 rw_tac std_ss[ring_fun_def] >> 429 Induct_on `n` >- 430 rw[] >> 431 rw_tac std_ss[ring_list_cons, GENLIST] >> 432 `rlist (FRONT (SNOC (f n) (GENLIST f n)))` by rw_tac std_ss[FRONT_SNOC] >> 433 `LAST (SNOC (f n) (GENLIST f n)) IN R` by rw_tac std_ss[LAST_SNOC] >> 434 metis_tac[ring_list_front_last]); 435 436(* Theorem: rfun f ==> rlist (MAP f l) *) 437(* Proof: by induction. 438 Base case: rlist (MAP f []) 439 True by ring_list_nil, MAP: MAP f [] = [] 440 Step case: rlist l ==> rlist (MAP f l) ==> !h. rlist (h::l) ==> rlist (MAP f (h::l)) 441 True by ring_list_cons, MAP: MAP f (h::t) = f h::MAP f t 442*) 443val ring_fun_map = store_thm( 444 "ring_fun_map", 445 ``!f l. rfun f ==> rlist (MAP f l)``, 446 rw_tac std_ss[ring_fun_def] >> 447 Induct_on `l` >| [ 448 rw_tac std_ss[MAP, ring_list_nil], 449 rw_tac std_ss[MAP, ring_list_cons] 450 ]); 451 452(* Theorem: rfun f ==> !x. x IN R ==> rfun (\j. f j * x ** j *) 453(* Proof: by ring_fun_def, ring_exp_element, ring_mult_element *) 454val ring_fun_from_ring_fun = store_thm( 455 "ring_fun_from_ring_fun", 456 ``!r:'a ring. Ring r ==> !f. rfun f ==> !x. x IN R ==> rfun (\j. f j * x ** j)``, 457 rw[ring_fun_def]); 458 459(* Theorem: rfun f ==> !x. x IN R ==> !n. rfun (\j. (f j * x ** j) ** n) *) 460(* Proof: by ring_fun_def, ring_exp_element, ring_mult_element *) 461val ring_fun_from_ring_fun_exp = store_thm( 462 "ring_fun_from_ring_fun_exp", 463 ``!r:'a ring. Ring r ==> !f. rfun f ==> !x. x IN R ==> !n. rfun (\j. (f j * x ** j) ** n)``, 464 rw[ring_fun_def]); 465 466(* Theorem: rfun f ==> !x. x IN R ==> !n. rlist (GENLIST (\j. f j * x ** j) n) *) 467(* Proof: 468 By induction on n. 469 Base case: rlist (GENLIST (\j. f j * x ** j) 0) 470 Since rlist (GENLIST (\j. f j * x ** j) 0) = rlist [] by GENLIST 471 and rlist [] = T by ring_list_nil 472 Step case: rlist (GENLIST (\j. f j * x ** j) n) ==> rlist (GENLIST (\j. f j * x ** j) (SUC n)) 473 rlist (GENLIST (\j. f j * x ** j) (SUC n)) 474 = rlist (SNOC (f n * x ** n) (GENLIST (\j. f j * x ** j) n)) by GENLIST 475 = (f n ** x ** n) IN R /\ rlist (GENLIST (\j. f j * x ** j) n) by ring_list_SNOC 476 = true /\ rlist (GENLIST (\j. f j * x ** j) n) by ring_fun_def, ring_exp_element 477 = true /\ true by induction hypothesis 478*) 479val ring_list_gen_from_ring_fun = store_thm( 480 "ring_list_gen_from_ring_fun", 481 ``!r:'a ring. Ring r ==> !f. rfun f ==> !x. x IN R ==> !n. rlist (GENLIST (\j. f j * x ** j) n)``, 482 rpt strip_tac >> 483 Induct_on `n` >- 484 rw[] >> 485 `!j. f j IN R` by metis_tac[ring_fun_def] >> 486 rw_tac std_ss[GENLIST, ring_list_SNOC, ring_exp_element, ring_mult_element]); 487 488(* Theorem: !f. rfun f ==> !n g. rlist (GENLIST (f o g) n) *) 489(* Proof: 490 By induction on n. 491 Base: rlist (GENLIST (f o g) 0) 492 rlist (GENLIST (f o g) 0) 493 <=> rlist [] by GENLIST_0 494 <=> T by ring_list_nil 495 Step: rlist (GENLIST (f o g) n) ==> rlist (GENLIST (f o g) (SUC n)) 496 rlist (GENLIST (f o g) (SUC n)) 497 <=> rlist (SNOC ((f o g) n) (GENLIST (f o g) n)) by GENLIST 498 <=> (f o g) n IN R /\ rlist (GENLIST (f o g) n) by ring_list_SNOC 499 <=> (f o g) n IN R /\ T by induction hypothesis 500 <=> f (g n) IN R by o_THM 501 <=> T by ring_fun_def 502*) 503val ring_list_from_genlist_ring_fun = store_thm( 504 "ring_list_from_genlist_ring_fun", 505 ``!r:'a ring. !f. rfun f ==> !n g. rlist (GENLIST (f o g) n)``, 506 rpt strip_tac >> 507 Induct_on `n` >- 508 rw[] >> 509 `rlist (GENLIST (f o g) (SUC n)) <=> f (g n) IN R` by rw_tac std_ss[GENLIST, ring_list_SNOC] >> 510 metis_tac[ring_fun_def]); 511 512(* Theorem: !f. rfun f ==> !n. rlist (GENLIST f n) *) 513(* Proof: 514 Since f = f o I by I_o_ID 515 The result follows from ring_list_from_genlist_ring_fun 516*) 517val ring_list_from_genlist = store_thm( 518 "ring_list_from_genlist", 519 ``!r:'a ring. !f. rfun f ==> !n. rlist (GENLIST f n)``, 520 rpt strip_tac >> 521 `f = f o I` by rw[] >> 522 `rlist (GENLIST (f o I) n)` by rw[ring_list_from_genlist_ring_fun] >> 523 metis_tac[]); 524 525(* ------------------------------------------------------------------------- *) 526(* Ring Sum Involving GENLIST *) 527(* ------------------------------------------------------------------------- *) 528 529(* Theorem: Ring r ==> !f n k. (0 < k /\ k < n ==> (f k = #0)) ==> (rsum (MAP f (GENLIST SUC (PRE p))) = #0) *) 530(* Proof: by induction on n 531 Base case: (!k. 0 < k /\ k < 0 ==> (f k = #0)) ==> (rsum (MAP f (GENLIST SUC (PRE 0))) = #0) 532 rsum (MAP f (GENLIST SUC (PRE 0)) 533 = rsum (MAP f (GENLIST SUC 0)) by PRE 0 = 0 534 = rsum (MAP f []) by GENLIST f 0 = [] in GENLIST 535 = rsum [] by MAP f [] = [] in MAP 536 = #0 by ring_sum_nil 537 Step case: (!k. 0 < k /\ k < n ==> (f k = #0)) ==> (rsum (MAP f (GENLIST SUC (PRE n))) = #0) ==> 538 (!k. 0 < k /\ k < SUC n ==> (f k = #0)) ==> (rsum (MAP f (GENLIST SUC (PRE (SUC n)))) = #0) 539 First, note that n < SUC n by LESS_SUC 540 hence !k. 0 < k /\ k < n ==> f k = #0 by LESS_TRANS 541 If n = 0, true by similar reasoning in base case. 542 If n <> 0, 0 < n, then n = SUC m for some m by num_CASES 543 rsum (MAP f (GENLIST SUC (PRE (SUC n)))) 544 = rsum (MAP f (GENLIST SUC n)) 545 = rsum (MAP f (GENLIST SUC (SUC (PRE n)))) by SUC_PRE 546 = rsum (MAP f ((GENLIST SUC (PRE n)) ++ [SUC (PRE n)])) by GENLIST, SNOC_APPEND 547 = rsum (MAP f ((GENLIST SUC (PRE n)) ++ [n])) by SUC_PRE 548 = rsum (MAP f (GENLIST SUC (PRE n)) ++ MAP f [n]) by MAP_APPEND 549 = rsum (MAP f (GENLIST SUC (PRE n))) + rsum (MAP f [n]) by ring_sum_append, ring_fun_map 550 = #0 + rsum (MAP f [n]) by induction hypothesis 551 = rsum (MAP f [n]) by ring_add_lzero, ring_sum_element, ring_fun_map 552 = rsum ([f n]) by MAP 553 = f n by ring_sum_sing, ring_fun_def 554 = #0 by n < SUC n 555*) 556val ring_sum_fun_zero = store_thm( 557 "ring_sum_fun_zero", 558 ``!r:'a ring. Ring r ==> !f. rfun f ==> 559 !n. (!k. 0 < k /\ k < n ==> (f k = #0)) ==> (rsum (MAP f (GENLIST SUC (PRE n))) = #0)``, 560 ntac 4 strip_tac >> 561 Induct_on `n` >| [ 562 `GENLIST SUC 0 = []` by rw_tac std_ss[GENLIST] >> 563 `MAP f [] = []` by rw_tac std_ss[MAP] >> 564 rw_tac std_ss[ring_sum_nil], 565 rw_tac std_ss[] >> 566 `n < SUC n /\ !k. 0 < k /\ k < n ==> (f k = #0)` by metis_tac[LESS_SUC, LESS_TRANS] >> 567 Cases_on `n = 0` >| [ 568 rw_tac std_ss[] >> 569 `GENLIST SUC 0 = []` by rw_tac std_ss[GENLIST] >> 570 `MAP f [] = []` by rw_tac std_ss[MAP] >> 571 rw_tac std_ss[ring_sum_nil], 572 `0 < n /\ ?m. n = SUC m` by metis_tac[num_CASES, NOT_ZERO_LT_ZERO] >> 573 `rsum (MAP f (GENLIST SUC n)) = rsum (MAP f (GENLIST SUC (SUC (PRE n))))` by rw_tac std_ss[SUC_PRE] >> 574 `_ = rsum (MAP f ((GENLIST SUC (PRE n)) ++ [SUC (PRE n)]))` by rw_tac std_ss[GENLIST, SNOC_APPEND] >> 575 `_ = rsum (MAP f ((GENLIST SUC (PRE n)) ++ [n]))` by rw_tac std_ss[SUC_PRE] >> 576 `_ = rsum (MAP f (GENLIST SUC (PRE n)) ++ MAP f [n])` by rw_tac std_ss[MAP_APPEND] >> 577 `_ = rsum (MAP f (GENLIST SUC (PRE n))) + rsum (MAP f [n])` by rw_tac std_ss[ring_sum_append, ring_fun_map] >> 578 `_ = #0 + rsum (MAP f [n])` by metis_tac[] >> 579 `_ = rsum (MAP f [n])` by rw_tac std_ss[ring_add_lzero, ring_sum_element, ring_fun_map] >> 580 `_ = rsum ([f n])` by rw_tac std_ss[MAP] >> 581 `_ = f n` by metis_tac[ring_sum_sing, ring_fun_def] >> 582 metis_tac[] 583 ] 584 ]); 585 586(* Theorem: rsum (k=0..n) f(k) = f(0) + rsum (k=1..n) f(k) *) 587(* Proof: 588 rsum (GENLIST f (SUC n)) 589 = rsum (f 0 :: GENLIST (f o SUC) n) by GENLIST_CONS 590 = f 0 + rsum (GENLIST (f o SUC) n) by ring_sum_cons 591*) 592val ring_sum_decompose_first = store_thm( 593 "ring_sum_decompose_first", 594 ``!r:'a ring. !f n. rsum (GENLIST f (SUC n)) = f 0 + rsum (GENLIST (f o SUC) n)``, 595 rw[GENLIST_CONS]); 596 597(* Theorem: rsum (k=0..n) f(k) = rsum (k=0..(n-1)) f(k) + f n *) 598(* Proof: 599 rsum (GENLIST f (SUC n)) 600 = rsum (SNOC (f n) (GENLIST f n)) by GENLIST definition 601 = rsum ((GENLIST f n) ++ [f n]) by SNOC_APPEND 602 = rsum (GENLIST f n) + rsum [f n] by ring_sum_append 603 = rsum (GENLIST f n) + f n by ring_sum_sing 604*) 605val ring_sum_decompose_last = store_thm( 606 "ring_sum_decompose_last", 607 ``!r:'a ring. Ring r ==> !f n. rfun f ==> (rsum (GENLIST f (SUC n)) = rsum (GENLIST f n) + f n)``, 608 rpt strip_tac >> 609 `rlist (GENLIST f n)` by rw_tac std_ss[ring_fun_genlist] >> 610 `f n IN R /\ rlist [f n]` by metis_tac[ring_list_def, ring_fun_def] >> 611 rw_tac std_ss[GENLIST, SNOC_APPEND, ring_sum_append, ring_sum_sing]); 612 613(* Theorem: Ring r /\ rfun f /\ 0 < n ==> rsum (k=0..n) f(k) = f(0) + rsum (k=1..n-1) f(k) + f(n) *) 614(* Proof: 615 rsum (GENLIST f (SUC n)) 616 = rsum (GENLIST f n) + f n by ring_sum_decompose_last 617 = rsum (GENLIST f (SUC m)) + f n by n = SUC m, since 0 < n 618 = f 0 + rsum (GENLIST f o SUC m) + f n by ring_sum_decompose_first 619 = f 0 + rsum (GENLIST f o SUC (PRE n)) + f n by PRE_SUC_EQ 620*) 621val ring_sum_decompose_first_last = store_thm( 622 "ring_sum_decompose_first_last", 623 ``!r:'a ring. Ring r ==> !f n. rfun f /\ 0 < n ==> (rsum (GENLIST f (SUC n)) = f 0 + rsum (GENLIST (f o SUC) (PRE n)) + f n)``, 624 rpt strip_tac >> 625 `n <> 0` by decide_tac >> 626 `?m. n = SUC m` by metis_tac[num_CASES] >> 627 `rsum (GENLIST f (SUC n)) = rsum (GENLIST f n) + f n` by rw_tac std_ss[ring_sum_decompose_last] >> 628 `_ = f 0 + rsum (GENLIST (f o SUC) m) + f n` by rw_tac std_ss[ring_sum_decompose_first] >> 629 rw_tac std_ss[PRE_SUC_EQ]); 630 631(* Theorem: rsum (GENLIST a n) + rsum (GENLIST b n) = rsum (GENLIST (\k. a k + b k) n) *) 632(* Proof: by induction on n. 633 Base case: rsum (GENLIST a 0) + rsum (GENLIST b 0) = rsum (GENLIST (\k. a k + b k) 0) 634 true by GENLIST f 0 = [], and rsum [] = #0, and #0 + #0 = #0 by ring_add_zero_zero. 635 Step case: rsum (GENLIST a n) + rsum (GENLIST b n) = rsum (GENLIST (\k. a k + b k) n) ==> 636 rsum (GENLIST a (SUC n)) + rsum (GENLIST b (SUC n)) = rsum (GENLIST (\k. a k + b k) (SUC n)) 637 LHS = rsum (GENLIST a (SUC n)) + rsum (GENLIST b (SUC n)) 638 = (rsum (GENLIST a n) + a n) + (rsum (GENLIST b n) + b n) by ring_sum_decompose_last 639 = rsum (GENLIST a n) + (a n + (rsum (GENLIST b n) + b n)) by ring_add_assoc 640 = rsum (GENLIST a n) + (a n + rsum (GENLIST b n) + b n) by ring_add_assoc 641 = rsum (GENLIST a n) + (rsum (GENLIST b n) + a n + b n) by ring_add_comm 642 = rsum (GENLIST a n) + (rsum (GENLIST b n) + (a n + b n)) by ring_add_assoc 643 = rsum (GENLIST a n) + rsum (GENLIST b n) + (a n + b n) by ring_add_assoc 644 = rsum (GENLIST (\k. a k + b k) n) + (a n + b n) by induction hypothesis 645 = rsum (GENLIST (\k. a k + b k) (SUC n)) by ring_sum_decompose_last 646 = RHS 647*) 648val ring_sum_genlist_add = store_thm( 649 "ring_sum_genlist_add", 650 ``!r:'a ring. Ring r ==> !a b. rfun a /\ rfun b ==> 651 !n. rsum (GENLIST a n) + rsum (GENLIST b n) = rsum (GENLIST (\k. a k + b k) n)``, 652 rpt strip_tac >> 653 Induct_on `n` >- 654 rw[] >> 655 `rfun (\k. a k + b k)` by rw_tac std_ss[ring_fun_add] >> 656 rw_tac std_ss[ring_sum_decompose_last] >> 657 `rsum (GENLIST a n) IN R /\ rsum (GENLIST b n) IN R` by rw_tac std_ss[ring_sum_element, ring_fun_genlist] >> 658 `a n IN R /\ b n IN R` by metis_tac[ring_fun_def] >> 659 `rsum (GENLIST a n) + a n + (rsum (GENLIST b n) + b n) 660 = rsum (GENLIST a n) + (a n + rsum (GENLIST b n) + b n)` by rw[ring_add_assoc] >> 661 `_ = rsum (GENLIST a n) + (rsum (GENLIST b n) + a n + b n)` by rw_tac std_ss[ring_add_comm] >> 662 `_ = rsum (GENLIST a n) + rsum (GENLIST b n) + (a n + b n)` by rw[ring_add_assoc] >> 663 rw_tac std_ss[]); 664 665(* Theorem: rsum (GENLIST a n ++ GENLIST b n) = rsum (GENLIST (\k. a k + b k) n) *) 666(* Proof: 667 rsum (GENLIST a n ++ GENLIST b n) 668 = rsum (GENLIST a n) + rsum (GENLIST b n) by ring_sum_append, due to ring_fun_genlist. 669 = rsum (GENLIST (\k. a k + b k) n) by ring_sum_genlist_add 670*) 671val ring_sum_genlist_append = store_thm( 672 "ring_sum_genlist_append", 673 ``!r:'a ring. Ring r ==> !a b. rfun a /\ rfun b ==> 674 !n. rsum (GENLIST a n ++ GENLIST b n) = rsum (GENLIST (\k. a k + b k) n)``, 675 rw_tac std_ss[ring_sum_append, ring_sum_genlist_add, ring_fun_genlist]); 676 677(* Theorem: Ring r ==> !f. rfun f ==> 678 !n m. rsum (GENLIST f (n + m)) = rsum (GENLIST f m) + rsum (GENLIST (\k. f (k + m)) n) *) 679(* Proof: 680 Note (\k. f (k + m)) = f o (\k. k + m) by FUN_EQ_THM 681 Hence rlist (GENLIST f m) by ring_list_from_genlist 682 and rlist (GENLIST (\k. f (k + m)) n) by ring_list_from_genlist_ring_fun 683 rsum (GENLIST f (n + m)) 684 = rsum (GENLIST f m ++ GENLIST (\k. f (k + m)) n) by GENLIST_APPEND 685 = rsum (GENLIST f m) + rsum (GENLIST (\k. f (k + m)) n) by ring_sum_append 686*) 687val ring_sum_genlist_sum = store_thm( 688 "ring_sum_genlist_sum", 689 ``!r:'a ring. Ring r ==> !f. rfun f ==> 690 !n m. rsum (GENLIST f (n + m)) = rsum (GENLIST f m) + rsum (GENLIST (\k. f (k + m)) n)``, 691 rpt strip_tac >> 692 `(\k. f (k + m)) = f o (\k. k + m)` by rw[FUN_EQ_THM] >> 693 `rlist (GENLIST (\k. f (k + m)) n)` by rw[ring_list_from_genlist_ring_fun] >> 694 `rlist (GENLIST f m)` by rw[ring_list_from_genlist] >> 695 metis_tac[GENLIST_APPEND, ring_sum_append]); 696 697(* Theorem: Ring r ==> !x. x IN R ==> !n. rsum (GENLIST (K x) n) = ##n * x *) 698(* Proof: 699 By induction on n. 700 Base: rsum (GENLIST (K x) 0) = ##0 * x 701 rsum (GENLIST (K x) 0) 702 = rsum [] by GENLIST_0 703 = #0 by ring_sum_nil 704 = ##0 * x by ring_num_0, ring_mult_lzero 705 Step: rsum (GENLIST (K x) n) = ##n * x ==> 706 rsum (GENLIST (K x) (SUC n)) = ##(SUC n) * x 707 Note rfun (K x) by ring_fun_def, K_THM, x IN R 708 so rlist (GENLIST (K x) n) by ring_list_from_genlist 709 rsum (GENLIST (K x) (SUC n)) 710 = rsum (SNOC ((K x) n) (GENLIST (K x) n)) by GENLIST 711 = rsum (SNOC x (GENLIST (K x) n)) by K_THM 712 = rsum (GENLIST (K x) n) + x by ring_sum_SNOC 713 = ##n * x + x by induction hypothesis 714 = ##n * x + #1 * x by ring_mult_lone 715 = (##n + #1) * x by ring_mult_ladd 716 = ##(SUC n) * x by ring_num_suc 717*) 718val ring_sum_genlist_const = store_thm( 719 "ring_sum_genlist_const", 720 ``!r:'a ring. Ring r ==> !x. x IN R ==> !n. rsum (GENLIST (K x) n) = ##n * x``, 721 rpt strip_tac >> 722 Induct_on `n` >- 723 rw[] >> 724 `rfun (K x)` by rw[ring_fun_def] >> 725 `rlist (GENLIST (K x) n)` by rw[ring_list_from_genlist] >> 726 `rsum (GENLIST (K x) (SUC n)) = ##n * x + x` by rw[GENLIST, ring_sum_SNOC] >> 727 rw[ring_mult_ladd, ring_num_suc]); 728 729(* ------------------------------------------------------------------------- *) 730(* Ring Binomial Theorem *) 731(* ------------------------------------------------------------------------- *) 732 733(* Theorem: Binomial Index Shifting, for 734 rsum (k=1..n) ##C(n,k) x^(n+1-k) y^k = rsum (k=0..n-1) ##C(n,k+1) x^(n-k) y^(k+1) *) 735(* Proof: 736 Since 737 rsum (k=1..n) C(n,k)x^(n+1-k)y^k 738 = rsum (MAP (\k. (binomial n k)* x**(n+1-k) * y**k) (GENLIST SUC n)) 739 = rsum (GENLIST (\k. (binomial n k)* x**(n+1-k) * y**k) o SUC n) 740 741 rsum (k=0..n-1) C(n,k+1)x^(n-k)y^(k+1) 742 = rsum (MAP (\k. (binomial n (k+1)) * x**(n-k) * y**(k+1)) (GENLIST I n)) 743 = rsum (GENLIST (\k. (binomial n (k+1)) * x**(n-k) * y**(k+1)) o I n) 744 = rsum (GENLIST (\k. (binomial n (k+1)) * x**(n-k) * y**(k+1)) n) 745 746 This is equivalent to showing: 747 (\k. (binomial n k)* x**(n-k+1) * y**k) o SUC = (\k. (binomial n (k+1)) * x**(n-k) * y**(k+1)) 748*) 749 750(* Theorem: Binomial index shift for GENLIST: 751 (\k. (binomial n k)* x**(n-k+1) * y**k) o SUC = (\k. (binomial n (k+1)) * x**(n-k) * y**(k+1)) *) 752(* Proof: 753 For any k < n, 754 ((\k. (binomial n k)* x**(n-k+1) * y**k) o SUC) k 755 = ##(binomial n (SUC k)) * x ** SUC (n - SUC k) * y ** SUC k 756 = ##(binomial n (SUC k)) * x ** (n-k) * y ** SUC k by SUC (n - SUC k) = n - k for k < n 757 = ##(binomial n (k + 1)) * x ** (n-k) * y ** (k+1) by definition of SUC 758 = (\k. (binomial n (k+1)) * x**(n-k) * y**(k+1)) k 759*) 760val ring_binomial_genlist_index_shift = store_thm( 761 "ring_binomial_genlist_index_shift", 762 ``!r:'a ring. Ring r ==> !x y. x IN R /\ y IN R ==> 763 !n. GENLIST ((\k. ##(binomial n k) * x ** SUC(n - k) * y ** k) o SUC) n = 764 GENLIST (\k. ##(binomial n (SUC k)) * x**(n-k) * y**(SUC k)) n``, 765 rw_tac std_ss[GENLIST_FUN_EQ] >> 766 `SUC (n - SUC k) = n - k` by decide_tac >> 767 rw_tac std_ss[]); 768 769(* This is closely related to above, with (SUC n) replacing (n), 770 but does not require k < n. *) 771(* Proof: by equality of function. *) 772val ring_binomial_index_shift = store_thm( 773 "ring_binomial_index_shift", 774 ``!r:'a ring. Ring r ==> !x y. x IN R /\ y IN R ==> 775 !n. (\k. ##(binomial (SUC n) k) * x**((SUC n) - k) * y**k) o SUC = 776 (\k. ##(binomial (SUC n) (SUC k)) * x**(n-k) * y**(SUC k))``, 777 rw[FUN_EQ_THM]); 778 779(* Pattern for binomial expansion: 780 781 (x+y)(x^3 + 3x^2y + 3xy^2 + y^3) 782 = x(x^3) + 3x(x^2y) + 3x(xy^2) + x(y^3) + 783 y(x^3) + 3y(x^2y) + 3y(xy^2) + y(y^3) 784 = x^4 + (3+1)x^3y + (3+3)(x^2y^2) + (1+3)(xy^3) + y^4 785 = x^4 + 4x^3y + 6x^2y^2 + 4xy^3 + y^4 786 787*) 788 789(* Theorem: multiply x into a binomial term: 790 (\k. x*k) o (\k. ##(binomial n k) * x ** (n - k) * y ** k) = (\k. ##(binomial n k) * x ** (SUC(n - k)) * y ** k) *) 791(* Proof: to prove: 792 x * (##(binomial n k) * x ** (n - k) * y ** k) = ##(binomial n k) * x ** SUC (n - k) * y ** k 793 LHS = x * (##(binomial n k) * x ** (n - k) * y ** k) 794 = x * (##(binomial n k) * (x ** (n - k) * y ** k)) by ring_mult_assoc 795 = (x * ##(binomial n k)) * (x ** (n - k) * y ** k) by ring_mult_assoc 796 = (##(binomial n k) * x) * (x ** (n - k) * y ** k) by ring_mult_comm 797 = ##(binomial n k) * (x * x ** (n - k) * y ** k) by ring_mult_assoc 798 = ##(binomial n k) * (x ** SUC (n - k) * y ** k) by ring_exp_SUC 799 = ##(binomial n k) * x ** SUC (n - k) * y ** k by ring_mult_assoc 800 = RHS 801*) 802val ring_binomial_term_merge_x = store_thm( 803 "ring_binomial_term_merge_x", 804 ``!r:'a ring. Ring r ==> !x y. x IN R /\ y IN R ==> 805 !n. (\k. x*k) o (\k. ##(binomial n k) * x ** (n - k) * y ** k) = (\k. ##(binomial n k) * x ** (SUC(n - k)) * y ** k)``, 806 rw_tac std_ss[FUN_EQ_THM] >> 807 `##(binomial n k) IN R /\ x ** (n - k) IN R /\ y ** k IN R /\ x ** SUC (n - k) IN R` by rw[] >> 808 `x * (##(binomial n k) * x ** (n - k) * y ** k) = (x * ##(binomial n k)) * (x ** (n - k) * y ** k)` by rw[ring_mult_assoc] >> 809 `_ = (##(binomial n k) * x) * (x ** (n - k) * y ** k)` by rw_tac std_ss[ring_mult_comm] >> 810 rw[ring_mult_assoc]); 811 812(* Theorem: multiply y into a binomial term: 813 (\k. y*k) o (\k. ##(binomial n k) * x ** (n - k) * y ** k) = (\k. ##(binomial n k) * x ** (n - k) * y ** (SUC k)) *) 814(* Proof: to prove: 815 y * (##(binomial n k) * x ** (n - k) * y ** k) = ##(binomial n k) * x ** (n - k) * y ** SUC k 816 LHS = y * (##(binomial n k) * x ** (n - k) * y ** k) 817 = y * (##(binomial n k) * (x ** (n - k) * y ** k)) by ring_mult_assoc 818 = (y * ##(binomial n k)) * (x ** (n - k) * y ** k) by ring_mult_assoc 819 = (##(binomial n k) * y) * (x ** (n - k) * y ** k) by ring_mult_comm 820 = (##(binomial n k) * y) * (y ** k * x ** (n - k)) by ring_mult_comm 821 = ##(binomial n k) * (y * y ** k * x ** (n - k)) by ring_mult_assoc 822 = ##(binomial n k) * (y ** SUC k * x ** (n - k)) by ring_exp_SUC 823 = ##(binomial n k) * (x ** (n - k) * y ** SUC k) by ring_mult_comm 824 = ##(binomial n k) * x ** (n - k) * y ** SUC k by ring_mult_assoc 825 = RHS 826*) 827val ring_binomial_term_merge_y = store_thm( 828 "ring_binomial_term_merge_y", 829 ``!r:'a ring. Ring r ==> !x y. x IN R /\ y IN R ==> 830 !n. (\k. y*k) o (\k. ##(binomial n k) * x ** (n - k) * y ** k) = (\k. ##(binomial n k) * x ** (n - k) * y ** (SUC k))``, 831 rw_tac std_ss[FUN_EQ_THM] >> 832 `##(binomial n k) IN R /\ x ** (n - k) IN R /\ y ** k IN R /\ y ** SUC k IN R` by rw[] >> 833 `y * (##(binomial n k) * x ** (n - k) * y ** k) = 834 (y * ##(binomial n k)) * (x ** (n - k) * y ** k)` by rw[ring_mult_assoc] >> 835 `_ = (##(binomial n k) * y) * (y ** k * x ** (n - k))` by rw_tac std_ss[ring_mult_comm] >> 836 `_ = ##(binomial n k) * (y ** SUC k * x ** (n - k))` by rw[ring_mult_assoc] >> 837 `_ = ##(binomial n k) * (x ** (n - k) * y ** SUC k)` by rw_tac std_ss[ring_mult_comm] >> 838 rw[ring_mult_assoc]); 839 840 841(* GOAL: *) 842 843(* Theorem: [Binomial Theorem] (x + y)^n = rsum (k=0..n) C(n,k)x^(n-k)y^k 844 or (x + y)**n = rsum (GENLIST (\k. (binomial n k)* x**(n-k) * y**k) (SUC n)) *) 845(* Proof: by induction on n. 846 Base case: to prove (x + y)^0 = rsum (k=0..0) C(0,k)x^(0-k)y^k 847 or (x + y) ** 0 = rsum (GENLIST (\k. ##(binomial 0 k) * x ** (0 - k) * y ** k) (SUC 0)) 848 LHS = (x + y) ** 0 = #1 by ring_exp_0, ring_add_element 849 RHS = rsum (GENLIST (\k. ##(binomial 0 k) * x ** (0 - k) * y ** k) (SUC 0)) 850 = rsum (GENLIST (\k. ##(binomial 0 k) * x ** (0 - k) * y ** k) 1) by ONE 851 = rsum (SNOC (##(binomial 0 0) * x ** 0 * y ** 0) []) by GENLIST 852 = rsum [##(binomial 0 0) * x ** 0 * y ** 0] by SNOC 853 = rsum [##(binomial 0 0) * #1 * #1] by ring_exp_0 854 = rsum [##1 * #1 * #1] by binomial_n_n 855 = rsum [#1 * #1 * #1] by ring_num_1 856 = rsum [#1] by ring_mult_one_one 857 = #1 by ring_sum_sing, ring_one_element 858 = LHS 859 Step case: assume (x + y)^n = rsum (k=0..n) C(n,k)x^(n-k)y^k 860 to prove: (x + y)^SUC n = rsum (k=0..(SUC n)) C(SUC n,k)x^((SUC n)-k)y^k 861 or (x + y) ** n = rsum (GENLIST (\k. ##(binomial n k) * x ** (n - k) * y ** k) (SUC n)) ==> 862 (x + y) ** SUC n = rsum (GENLIST (\k. ##(binomial (SUC n) k) * x ** (SUC n - k) * y ** k) (SUC (SUC n))) 863 LHS = (x + y) ** SUC n 864 = (x + y) * (x + y) ** n by ring_exp_SUC 865 = (x + y) * rsum (GENLIST (\k. ##(binomial n k) * x ** (n - k) * y ** k) (SUC n)) by induction hypothesis 866 = x * rsum (GENLIST (\k. ##(binomial n k) * x ** (n - k) * y ** k) (SUC n)) + 867 y * rsum (GENLIST (\k. ##(binomial n k) * x ** (n - k) * y ** k) (SUC n)) by ring_mult_ladd 868 = rsum (MAP (\k. x*k) (GENLIST (\k. ##(binomial n k) * x ** (n - k) * y ** k) (SUC n))) + 869 rsum (MAP (\k. y*k) (GENLIST (\k. ##(binomial n k) * x ** (n - k) * y ** k) (SUC n))) by ring_sum_mult 870 = rsum (GENLIST ((\k. x*k) o (\k. ##(binomial n k) * x ** (n - k) * y ** k)) (SUC n)) + 871 rsum (GENLIST ((\k. y*k) o (\k. ##(binomial n k) * x ** (n - k) * y ** k)) (SUC n)) by MAP_GENLIST 872 = rsum (GENLIST (\k. ##(binomial n k) * x ** SUC(n - k) * y ** k) (SUC n)) + 873 rsum (GENLIST (\k. ##(binomial n k) * x ** (n - k) * y ** (SUC k)) (SUC n)) 874 by ring_binomial_term_merge_x, ring_binomial_term_merge_y 875 = (\k. ##(binomial n k) * x ** SUC (n - k) * y ** k) 0 + 876 rsum (GENLIST ((\k. ##(binomial n k) * x ** SUC (n - k) * y ** k) o SUC) n) + 877 rsum (GENLIST (\k. ##(binomial n k) * x ** (n - k) * y ** (SUC k)) (SUC n)) by ring_sum_decompose_first 878 = (\k. ##(binomial n k) * x ** SUC (n - k) * y ** k) 0 + 879 rsum (GENLIST ((\k. ##(binomial n k) * x ** SUC (n - k) * y ** k) o SUC) n) + 880 (rsum (GENLIST (\k. ##(binomial n k) * x ** (n - k) * y ** (SUC k)) n) + 881 (\k. ##(binomial n k) * x ** (n - k) * y ** (SUC k)) n ) by ring_sum_decompose_last 882 = (\k. ##(binomial n k) * x ** SUC(n - k) * y ** k) 0 + 883 rsum (GENLIST (\k. ##(binomial n (SUC k)) * x ** (n - k) * y ** (SUC k)) n) + 884 (rsum (GENLIST (\k. ##(binomial n k) * x ** (n - k) * y ** (SUC k)) n) + 885 (\k. ##(binomial n k) * x ** (n - k) * y ** (SUC k)) n ) by ring_binomial_genlist_index_shift 886 = (\k. ##(binomial n k) * x ** SUC(n - k) * y ** k) 0 + 887 (rsum (GENLIST (\k. ##(binomial n (SUC k)) * x ** (n - k) * y ** (SUC k)) n) + 888 rsum (GENLIST (\k. ##(binomial n k) * x ** (n - k) * y ** (SUC k)) n)) + 889 (\k. ##(binomial n k) * x ** (n - k) * y ** (SUC k)) n by ring_add_assoc, ring_add_element 890 = (\k. ##(binomial n k) * x ** SUC (n - k) * y ** k) 0 + 891 rsum (GENLIST (\k. (##(binomial n (SUC k)) * x ** (n - k) * y ** (SUC k) + 892 ##(binomial n k) * x ** (n - k) * y ** (SUC k))) n) + 893 (\k. ##(binomial n k) * x ** (n - k) * y ** (SUC k)) n by ring_sum_genlist_add 894 = (\k. ##(binomial n k) * x ** SUC (n - k) * y ** k) 0 + 895 rsum (GENLIST (\k. (##(binomial n (SUC k)) + ##(binomial n k)) * x ** (n - k) * y ** (SUC k)) n) + 896 (\k. ##(binomial n k) * x ** (n - k) * y ** (SUC k)) n by ring_mult_ladd, ring_mult_element 897 = (\k. ##(binomial n k) * x ** SUC (n - k) * y ** k) 0 + 898 rsum (GENLIST (\k. (##(binomial n (SUC k)) * (x ** (n - k) * y ** (SUC k)) + 899 ##(binomial n k) * (x ** (n - k) * y ** (SUC k)))) n) + 900 (\k. ##(binomial n k) * x ** (n - k) * y ** (SUC k)) n by ring_mult_assoc 901 = (\k. ##(binomial n k) * x ** SUC (n - k) * y ** k) 0 + 902 rsum (GENLIST (\k. ##(binomial n (SUC k) + binomial n k) * (x ** (n - k) * y ** (SUC k))) n) + 903 (\k. ##(binomial n k) * x ** (n - k) * y ** (SUC k)) n by ring_num_add_mult, ring_mult_element 904 = (\k. ##(binomial n k) * x ** SUC(n - k) * y ** k) 0 + 905 rsum (GENLIST (\k. ##(binomial (SUC n) (SUC k)) * (x ** (n - k) * y ** (SUC k))) n) + 906 (\k. ##(binomial n k) * x ** (n - k) * y ** (SUC k)) n by binomial_recurrence, ADD_COMM 907 = (\k. ##(binomial n k) * x ** SUC(n - k) * y ** k) 0 + 908 rsum (GENLIST (\k. ##(binomial (SUC n) (SUC k)) * x ** (n - k) * y ** (SUC k)) n) + 909 (\k. ##(binomial n k) * x ** (n - k) * y ** (SUC k)) n by ring_mult_assoc 910 = ##(binomial n 0) * x ** (SUC n) * y ** 0 + 911 rsum (GENLIST (\k. ##(binomial (SUC n) (SUC k)) * x ** (n - k) * y ** (SUC k)) n) + 912 ##(binomial n n) * x ** 0 * y ** (SUC n) by function application 913 = ##(binomial (SUC n) 0) * x ** (SUC n) * y ** 0 + 914 rsum (GENLIST (\k. ##(binomial (SUC n) (SUC k)) * x ** (n - k) * y ** (SUC k)) n) + 915 ##(binomial (SUC n) (SUC n)) * x ** 0 * y ** (SUC n) by binomial_n_0, binomial_n_n 916 = ##(binomial (SUC n) 0) * x ** (SUC n) * y ** 0 + 917 rsum (GENLIST ((\k. ##(binomial (SUC n) k) * x ** ((SUC n) - k) * y ** k) o SUC) n) + 918 ##(binomial (SUC n) (SUC n)) * x ** 0 * y ** (SUC n) by ring_binomial_index_shift 919 = (\k. ##(binomial (SUC n) k) * x ** ((SUC n) - k) * y ** k) 0 + 920 rsum (GENLIST ((\k. ##(binomial (SUC n) k) * x ** ((SUC n) - k) * y ** k) o SUC) n) + 921 (\k. ##(binomial (SUC n) k) * x ** ((SUC n) - k) * y ** k) (SUC n) by function application 922 = rsum (GENLIST (\k. ##(binomial (SUC n) k) * x ** (SUC n - k) * y ** k) (SUC n)) + 923 (\k. ##(binomial (SUC n) k) * x ** (SUC n - k) * y ** k) (SUC n) by ring_sum_decompose_first 924 = rsum (GENLIST (\k. ##(binomial (SUC n) k) * x ** (SUC n - k) * y ** k) (SUC (SUC n))) by ring_sum_decompose_last 925 = RHS 926 Conventionally, 927 (x + y)^SUC n 928 = (x + y)(x + y)^n by EXP 929 = (x + y) rsum (k=0..n) C(n,k)x^(n-k)y^k by induction hypothesis 930 = x (rsum (k=0..n) C(n,k)x^(n-k)y^k) + 931 y (rsum (k=0..n) C(n,k)x^(n-k)y^k) by RIGHT_ADD_DISTRIB 932 = rsum (k=0..n) C(n,k)x^(n+1-k)y^k + 933 rsum (k=0..n) C(n,k)x^(n-k)y^(k+1) by moving factor into ring_sum 934 = C(n,0)x^(n+1) + rsum (k=1..n) C(n,k)x^(n+1-k)y^k + 935 rsum (k=0..n-1) C(n,k)x^(n-k)y^(k+1) + C(n,n)y^(n+1) by breaking sum 936 = C(n,0)x^(n+1) + rsum (k=0..n-1) C(n,k+1)x^(n-k)y^(k+1) + 937 rsum (k=0..n-1) C(n,k)x^(n-k)y^(k+1) + C(n,n)y^(n+1) by index shifting 938 = C(n,0)x^(n+1) + rsum (k=0..n-1) [C(n,k+1) + C(n,k)] x^(n-k)y^(k+1) + C(n,n)y^(n+1) by merging sums 939 = C(n,0)x^(n+1) + rsum (k=0..n-1) C(n+1,k+1) x^(n-k)y^(k+1) + C(n,n)y^(n+1) by binomial recurrence 940 = C(n,0)x^(n+1) + rsum (k=1..n) C(n+1,k) x^(n+1-k)y^k + C(n,n)y^(n+1) by index shifting again 941 = C(n+1,0)x^(n+1) + rsum (k=1..n) C(n+1,k) x^(n+1-k)y^k + C(n+1,n+1)y^(n+1) by binomial identities 942 = rsum (k=0..(SUC n))C(SUC n,k) x^((SUC n)-k)y^k by synthesis of sum 943*) 944val ring_binomial_thm = store_thm( 945 "ring_binomial_thm", 946 ``!r:'a ring. Ring r ==> !x y. x IN R /\ y IN R ==> 947 !n. (x + y)**n = rsum (GENLIST (\k. ##(binomial n k) * x**(n-k) * y**k) (SUC n))``, 948 rpt strip_tac >> 949 Induct_on `n` >- 950 rw[ring_sum_sing, binomial_n_n] >> 951 rw_tac std_ss[ring_exp_SUC, ring_add_element] >> 952 `!m n k h. ##(binomial m n) IN R /\ x ** h IN R /\ y ** k IN R` by rw[] >> 953 `!h. (\k. ##(binomial n k) * x ** SUC (n - k) * y ** k) h IN R` by rw_tac std_ss[ring_mult_element] >> 954 `!h. (\k. ##(binomial n k) * x ** (n - k) * y ** (SUC k)) h IN R` by rw_tac std_ss[ring_mult_element] >> 955 `!m. rfun (\k. ##(binomial m k) * x ** (m - k) * y ** k)` by rw_tac std_ss[ring_fun_def, ring_mult_element] >> 956 `!m n. rlist (GENLIST (\k. ##(binomial m k) * x ** (m - k) * y ** k) n)` by rw_tac std_ss[ring_fun_genlist] >> 957 `!m n. rsum (GENLIST (\k. ##(binomial m k) * x ** (m - k) * y ** k) n) IN R` by rw_tac std_ss[ring_sum_element] >> 958 `!m. rfun (\k. ##(binomial m k) * x ** (m - k) * y ** SUC k)` by rw_tac std_ss[ring_fun_def, ring_mult_element] >> 959 `!m n. rlist (GENLIST (\k. ##(binomial m k) * x ** (m - k) * y ** SUC k) n)` by rw_tac std_ss[ring_fun_genlist] >> 960 `!m n. rsum (GENLIST (\k. ##(binomial m k) * x ** (m - k) * y ** SUC k) n) IN R` by rw_tac std_ss[ring_sum_element] >> 961 `!m. rfun (\k. ##(binomial m (SUC k)) * x ** (m - k) * y ** SUC k)` by rw_tac std_ss[ring_fun_def, ring_mult_element] >> 962 `!m n. rlist (GENLIST (\k. ##(binomial m (SUC k)) * x ** (m - k) * y ** SUC k) n)` by rw_tac std_ss[ring_fun_genlist] >> 963 `!m n. rsum (GENLIST (\k. ##(binomial m (SUC k)) * x ** (m - k) * y ** SUC k) n) IN R` by rw_tac std_ss[ring_sum_element] >> 964 `(x + y) * rsum (GENLIST (\k. ##(binomial n k) * x ** (n - k) * y ** k) (SUC n)) = 965 x * rsum (GENLIST (\k. ##(binomial n k) * x ** (n - k) * y ** k) (SUC n)) + 966 y * rsum (GENLIST (\k. ##(binomial n k) * x ** (n - k) * y ** k) (SUC n))` by rw_tac std_ss[ring_mult_ladd] >> 967 `_ = rsum (GENLIST ((\k. x*k) o (\k. ##(binomial n k) * x ** (n - k) * y ** k)) (SUC n)) + 968 rsum (GENLIST ((\k. y*k) o (\k. ##(binomial n k) * x ** (n - k) * y ** k)) (SUC n))` 969 by rw_tac std_ss[ring_sum_mult, MAP_GENLIST] >> 970 `_ = rsum (GENLIST (\k. ##(binomial n k) * x ** SUC(n - k) * y ** k) (SUC n)) + 971 rsum (GENLIST (\k. ##(binomial n k) * x ** (n - k) * y ** (SUC k)) (SUC n))` 972 by rw_tac std_ss[ring_binomial_term_merge_x, ring_binomial_term_merge_y] >> 973 `_ = (\k. ##(binomial n k) * x ** SUC (n - k) * y ** k) 0 + 974 rsum (GENLIST ((\k. ##(binomial n k) * x ** SUC (n - k) * y ** k) o SUC) n) + 975 rsum (GENLIST (\k. ##(binomial n k) * x ** (n - k) * y ** (SUC k)) (SUC n))` 976 by rw_tac std_ss[ring_sum_decompose_first] >> 977 `_ = (\k. ##(binomial n k) * x ** SUC (n - k) * y ** k) 0 + 978 rsum (GENLIST ((\k. ##(binomial n k) * x ** SUC (n - k) * y ** k) o SUC) n) + 979 (rsum (GENLIST (\k. ##(binomial n k) * x ** (n - k) * y ** (SUC k)) n) + 980 (\k. ##(binomial n k) * x ** (n - k) * y ** (SUC k)) n )` 981 by rw_tac std_ss[ring_sum_decompose_last] >> 982 `_ = (\k. ##(binomial n k) * x ** SUC(n - k) * y ** k) 0 + 983 rsum (GENLIST (\k. ##(binomial n (SUC k)) * x ** (n - k) * y ** (SUC k)) n) + 984 (rsum (GENLIST (\k. ##(binomial n k) * x ** (n - k) * y ** (SUC k)) n) + 985 (\k. ##(binomial n k) * x ** (n - k) * y ** (SUC k)) n )` 986 by rw_tac std_ss[ring_binomial_genlist_index_shift] >> 987 `_ = (\k. ##(binomial n k) * x ** SUC(n - k) * y ** k) 0 + 988 (rsum (GENLIST (\k. ##(binomial n (SUC k)) * x ** (n - k) * y ** (SUC k)) n) + 989 rsum (GENLIST (\k. ##(binomial n k) * x ** (n - k) * y ** (SUC k)) n)) + 990 (\k. ##(binomial n k) * x ** (n - k) * y ** (SUC k)) n` 991 by rw_tac std_ss[ring_add_assoc, ring_add_element] >> 992 `_ = (\k. ##(binomial n k) * x ** SUC (n - k) * y ** k) 0 + 993 rsum (GENLIST (\k. (##(binomial n (SUC k)) * x ** (n - k) * y ** (SUC k) + 994 ##(binomial n k) * x ** (n - k) * y ** (SUC k))) n) + 995 (\k. ##(binomial n k) * x ** (n - k) * y ** (SUC k)) n` 996 by rw_tac std_ss[ring_sum_genlist_add] >> 997 `_ = (\k. ##(binomial n k) * x ** SUC (n - k) * y ** k) 0 + 998 rsum (GENLIST (\k. (##(binomial n (SUC k)) * (x ** (n - k) * y ** (SUC k)) + 999 ##(binomial n k) * (x ** (n - k) * y ** (SUC k)))) n) + 1000 (\k. ##(binomial n k) * x ** (n - k) * y ** (SUC k)) n` 1001 by rw_tac std_ss[ring_mult_assoc] >> 1002 `_ = (\k. ##(binomial n k) * x ** SUC (n - k) * y ** k) 0 + 1003 rsum (GENLIST (\k. ##(binomial n (SUC k) + binomial n k) * (x ** (n - k) * y ** (SUC k))) n) + 1004 (\k. ##(binomial n k) * x ** (n - k) * y ** (SUC k)) n` 1005 by rw_tac std_ss[ring_num_add_mult, ring_mult_element] >> 1006 `_ = (\k. ##(binomial n k) * x ** SUC(n - k) * y ** k) 0 + 1007 rsum (GENLIST (\k. ##(binomial (SUC n) (SUC k)) * (x ** (n - k) * y ** (SUC k))) n) + 1008 (\k. ##(binomial n k) * x ** (n - k) * y ** (SUC k)) n` 1009 by rw_tac std_ss[binomial_recurrence, ADD_COMM] >> 1010 `_ = (\k. ##(binomial n k) * x ** SUC(n - k) * y ** k) 0 + 1011 rsum (GENLIST (\k. ##(binomial (SUC n) (SUC k)) * x ** (n - k) * y ** (SUC k)) n) + 1012 (\k. ##(binomial n k) * x ** (n - k) * y ** (SUC k)) n` 1013 by rw_tac std_ss[ring_mult_assoc] >> 1014 `_ = ##(binomial (SUC n) 0) * x ** (SUC n) * y ** 0 + 1015 rsum (GENLIST (\k. ##(binomial (SUC n) (SUC k)) * x ** (n - k) * y ** (SUC k)) n) + 1016 ##(binomial (SUC n) (SUC n)) * x ** 0 * y ** (SUC n)` 1017 by rw_tac std_ss[binomial_n_0, binomial_n_n] >> 1018 `_ = ##(binomial (SUC n) 0) * x ** (SUC n) * y ** 0 + 1019 rsum (GENLIST ((\k. ##(binomial (SUC n) k) * x ** ((SUC n) - k) * y ** k) o SUC) n) + 1020 ##(binomial (SUC n) (SUC n)) * x ** 0 * y ** (SUC n)` 1021 by rw_tac std_ss[ring_binomial_index_shift] >> 1022 `_ = rsum (GENLIST (\k. ##(binomial (SUC n) k) * x ** (SUC n - k) * y ** k) (SUC n)) + 1023 (\k. ##(binomial (SUC n) k) * x ** (SUC n - k) * y ** k) (SUC n)` 1024 by rw_tac std_ss[ring_sum_decompose_first] >> 1025 `_ = rsum (GENLIST (\k. ##(binomial (SUC n) k) * x ** (SUC n - k) * y ** k) (SUC (SUC n)))` 1026 by rw_tac std_ss[ring_sum_decompose_last] >> 1027 rw_tac std_ss[]); 1028 1029(* This is a major milestone theorem. *) 1030 1031(* ------------------------------------------------------------------------- *) 1032(* Ring with prime characteristic *) 1033(* ------------------------------------------------------------------------- *) 1034 1035(* Theorem: Ring r ==> prime (char r) <=> 1 < char r /\ ##(binomial (char r) k) = #0 for 0 < k < (char r) *) 1036(* Proof: 1037 prime (char r) 1038 <=> divides (char r) (binomial (char r) k) for 0 < k < (char r) by prime_iff_divides_binomials 1039 <=> ##(binomial (char r) k) = #0 for 0 < k < (char r) by ring_char_divides 1040*) 1041val ring_char_prime = store_thm( 1042 "ring_char_prime", 1043 ``!r:'a ring. Ring r ==> 1044 (prime (char r) <=> 1 < char r /\ !k. 0 < k /\ k < char r ==> (##(binomial (char r) k) = #0))``, 1045 rw_tac std_ss[prime_iff_divides_binomials, ring_char_divides]); 1046 1047(* Theorem: [Freshman's Theorem] 1048 Ring r /\ prime (char r) ==> !x y. x IN R /\ y IN R ==> 1049 ((x + y) ** (char r) = x ** (char r) + y ** (char r)) *) 1050(* Proof: 1051 Let p = char r. 1052 prime p ==> 0 < p by PRIME_POS 1053 Let f = (\k. ##(binomial p k) * x**(p-k) * y**k), then 1054 then rfun f /\ f 0 IN R /\ f p IN R by ring_fun_def 1055 !k. 0 < k /\ k < p ==> (##(binomial p k) = #0) by ring_char_prime 1056 !k. 0 < k /\ k < p ==> (f k = #0) by ring_mult_lzero, ring_num_element, ring_exp_element 1057 (x + y) ** p 1058 = rsum (GENLIST f) (SUC p)) by ring_binomial_thm 1059 = f 0 + rsum (GENLIST (f o SUC) (PRE p)) + f p by ring_sum_decompose_first_last 1060 = f 0 + rsum (MAP f (GENLIST SUC (PRE p))) + f p by MAP_GENLIST 1061 = f 0 + #0 + f p by ring_sum_fun_zero 1062 = f 0 + f p by ring_add_rzero 1063 1064 f 0 = ##(binomial p 0) * x**(p-0) * y**0 1065 = #1 * x**p * #1 by binomial_n_0, ring_exp_0, ring_num_1 1066 = x ** p by ring_mult_lone, ring_mult_rone 1067 f p = ##(binomial p p) * x**(p-p) * y**p 1068 = #1 * #1 * y**p by binomial_n_n, ring_exp_0, ring_num_1 1069 = y ** p by ring_exp_element, ring_mult_one_one 1070 The result follows. 1071*) 1072val ring_freshman_thm = store_thm( 1073 "ring_freshman_thm", 1074 ``!r:'a ring. Ring r /\ prime (char r) ==> !x y. x IN R /\ y IN R ==> 1075 ((x + y) ** (char r) = x ** (char r) + y ** (char r))``, 1076 rpt strip_tac >> 1077 qabbrev_tac `p = char r` >> 1078 `0 < p` by metis_tac[PRIME_POS] >> 1079 qabbrev_tac `f = (\k. ##(binomial p k) * x**(p-k) * y**k)` >> 1080 `rfun f /\ f 0 IN R /\ f p IN R` by rw[ring_fun_def, Abbr`f`] >> 1081 `!k. 0 < k /\ k < p ==> (##(binomial p k) = #0)` by metis_tac[ring_char_prime] >> 1082 `!k. 0 < k /\ k < p ==> (f k = #0)` by rw[Abbr`f`, Abbr`p`] >> 1083 `(x + y) ** p = rsum (GENLIST f (SUC p))` by rw_tac std_ss[ring_binomial_thm, Abbr(`p`), Abbr(`f`)] >> 1084 `(x + y) ** p = f 0 + rsum (GENLIST (f o SUC) (PRE p)) + f p` by metis_tac[ring_sum_decompose_first_last] >> 1085 `_ = f 0 + rsum (MAP f (GENLIST SUC (PRE p))) + f p` by rw_tac std_ss[MAP_GENLIST] >> 1086 `_ = f 0 + f p` by rw_tac std_ss[ring_sum_fun_zero, ring_add_rzero] >> 1087 `f 0 = #1 * x**p * #1` by rw_tac std_ss[Abbr`f`, binomial_n_0, ring_exp_0, ring_num_1] >> 1088 `f p = #1 * #1 * y**p` by rw_tac std_ss[Abbr`f`, binomial_n_n, ring_exp_0, ring_num_1] >> 1089 rw[]); 1090 1091(* Note: a ** b ** c = a ** (b ** c) *) 1092(* Theorem: [Freshman's Theorem Generalized] 1093 Ring r /\ prime (char r) ==> !x y. x IN R /\ y IN R ==> 1094 !n. (x + y) ** (char r) ** n = x ** (char r) ** n + y ** (char r) ** n *) 1095(* Proof: 1096 Let p = char r. 1097 prime p ==> 0 < p by PRIME_POS 1098 By induction on n. 1099 Base case: (x + y) ** p ** 0 = x ** p ** 0 + y ** p ** 0 1100 LHS = (x + y) ** p ** 0 1101 = (x + y) ** 1 by EXP 1102 = x + y by ring_exp_1 1103 = x ** 1 + y ** 1 by ring_exp_1 1104 = x ** p ** 0 + y ** p ** 0 by EXP 1105 = RHS 1106 Step case: (x + y) ** p ** n = x ** p ** n + y ** p ** n ==> 1107 (x + y) ** p ** SUC n = x ** p ** SUC n + y ** p ** SUC n 1108 LHS = (x + y) ** p ** SUC n 1109 = (x + y) ** (p * p ** n) by EXP 1110 = (x + y) ** (p ** n * p) by MULT_COMM 1111 = ((x + y) ** p ** n) ** p by ring_exp_mult 1112 = (x ** p ** n + y ** p ** n) ** p by induction hypothesis 1113 = (x ** p ** n) ** p + (y ** p ** n) ** p by ring_freshman_thm 1114 = x ** (p ** n * p) + y ** (p ** n * p) by ring_exp_mult 1115 = x ** (p * p ** n) + y ** (p * p ** n) by MULT_COMM 1116 = x ** p ** SUC n + y ** p ** SUC n by EXP 1117 = RHS 1118*) 1119val ring_freshman_all = store_thm( 1120 "ring_freshman_all", 1121 ``!r:'a ring. Ring r /\ prime (char r) ==> !x y. x IN R /\ y IN R ==> 1122 !n. (x + y) ** (char r) ** n = x ** (char r) ** n + y ** (char r) ** n``, 1123 rpt strip_tac >> 1124 qabbrev_tac `p = char r` >> 1125 Induct_on `n` >- 1126 rw[EXP] >> 1127 `(x + y) ** p ** SUC n = (x + y) ** (p * p ** n)` by rw[EXP] >> 1128 `_ = (x + y) ** (p ** n * p)` by rw_tac std_ss[MULT_COMM] >> 1129 `_ = ((x + y) ** p ** n) ** p` by rw[ring_exp_mult] >> 1130 `_ = (x ** p ** n + y ** p ** n) ** p` by rw[] >> 1131 `_ = (x ** p ** n) ** p + (y ** p ** n) ** p` by rw[ring_freshman_thm, Abbr`p`] >> 1132 `_ = x ** (p ** n * p) + y ** (p ** n * p)` by rw[ring_exp_mult] >> 1133 `_ = x ** (p * p ** n) + y ** (p * p ** n)` by rw_tac std_ss[MULT_COMM] >> 1134 `_ = x ** p ** SUC n + y ** p ** SUC n` by rw[EXP] >> 1135 rw[]); 1136 1137(* Theorem: Ring r /\ prime (char r) ==> !x y. x IN R /\ y IN R ==> 1138 ((x - y) ** char r = x ** char r - y ** char r) *) 1139(* Proof: 1140 Let m = char r. 1141 (x - y) ** m 1142 = (x + -y) ** m by ring_sub_def 1143 = x ** m + (-y) ** m by ring_freshman_thm 1144 If EVEN m, 1145 (-y) ** m = y ** m by ring_neg_exp 1146 prime m ==> m = 2 by EVEN_PRIME 1147 y ** m = - (y ** m) by ring_neg_char_2 1148 The result follows by ring_sub_def 1149 If ~EVEN m, 1150 (-y) ** m = - (y ** m) by ring_neg_exp 1151 The result follows by ring_sub_def 1152*) 1153val ring_freshman_thm_sub = store_thm( 1154 "ring_freshman_thm_sub", 1155 ``!r:'a ring. Ring r /\ prime (char r) ==> !x y. x IN R /\ y IN R ==> 1156 ((x - y) ** char r = x ** char r - y ** char r)``, 1157 rpt strip_tac >> 1158 qabbrev_tac `m = char r` >> 1159 rw[] >> 1160 `(x + -y) ** m = x ** m + (-y) ** m` by rw[ring_freshman_thm, Abbr`m`] >> 1161 Cases_on `EVEN m` >- 1162 rw[EVEN_PRIME, ring_neg_exp, ring_neg_char_2, Abbr`m`] >> 1163 rw[ring_neg_exp]); 1164 1165(* Theorem: Ring r /\ prime (char r) ==> !x y. x IN R /\ y IN R ==> 1166 !n. (x - y) ** (char r) ** n = x ** (char r) ** n - y ** (char r) ** n *) 1167(* Proof: 1168 Let m = char r. 1169 prime m ==> 0 < m by PRIME_POS 1170 By induction on n. 1171 Base case: (x - y) ** m ** 0 = x ** m ** 0 - y ** m ** 0 1172 (x - y) ** m ** 0 1173 = (x - y) ** 1 by EXP 1174 = x - y by ring_exp_1 1175 = x ** 1 - y ** 1 by ring_exp_1 1176 = x ** m ** 0 - y ** m ** 0 by EXP 1177 Step case: (x - y) ** m ** n = x ** m ** n - y ** m ** n ==> 1178 (x - y) ** m ** SUC n = x ** m ** SUC n - y ** m ** SUC n 1179 (x - y) ** m ** SUC n 1180 = (x - y) ** (m * m ** n) by EXP 1181 = (x - y) ** (m ** n * m) by MULT_COMM 1182 = ((x - y) ** m ** n) ** m by ring_exp_mult 1183 = (x ** m ** n - y ** m ** n) ** m by induction hypothesis 1184 = (x ** m ** n) ** m - (y ** m ** n) ** m by ring_freshman_thm_sub 1185 = x ** (m ** n * m) - y ** (m ** n * m) by ring_exp_mult 1186 = x ** (m * m ** n) - y ** (m * m ** n) by MULT_COMM 1187 = x ** m ** SUC n - y ** m ** SUC n by EXP 1188*) 1189val ring_freshman_all_sub = store_thm( 1190 "ring_freshman_all_sub", 1191 ``!r:'a ring. Ring r /\ prime (char r) ==> !x y. x IN R /\ y IN R ==> 1192 !n. (x - y) ** (char r) ** n = x ** (char r) ** n - y ** (char r) ** n``, 1193 rpt strip_tac >> 1194 qabbrev_tac `m = char r` >> 1195 Induct_on `n` >- 1196 rw[EXP] >> 1197 `(x - y) ** m ** SUC n = (x - y) ** (m * m ** n)` by rw[EXP] >> 1198 `_ = (x - y) ** (m ** n * m)` by rw_tac std_ss[MULT_COMM] >> 1199 `_ = ((x - y) ** m ** n) ** m` by rw[ring_exp_mult] >> 1200 `_ = (x ** m ** n - y ** m ** n) ** m` by rw[] >> 1201 `_ = (x ** m ** n) ** m - (y ** m ** n) ** m` by rw[ring_freshman_thm_sub, Abbr`m`] >> 1202 `_ = x ** (m ** n * m) - y ** (m ** n * m)` by rw[ring_exp_mult] >> 1203 `_ = x ** (m * m ** n) - y ** (m * m ** n)` by rw_tac std_ss[MULT_COMM] >> 1204 `_ = x ** m ** SUC n - y ** m ** SUC n` by rw[EXP] >> 1205 rw[]); 1206 1207(* Theorem: [Fermat's Little Theorem] 1208 Ring r /\ prime (char r) ==> !n. (##n) ** (char r) = (##n) *) 1209(* Proof: by induction on n. 1210 Let p = char r, prime p ==> 0 < p by PRIME_POS 1211 Base case: ##0 ** p = ##0 1212 ##0 ** p 1213 = #0 ** p by ring_num_0 1214 = #0 by ring_zero_exp, p <> 0 1215 = ##0 by ring_num_0 1216 Step case: ##n ** p = ##n ==> ##(SUC n) ** p = ##(SUC n) 1217 ##(SUC n) ** p 1218 = (#1 + ##n) ** p by ring_num_SUC 1219 = #1 ** p + ##n ** p by ring_freshman_thm 1220 = #1 ** p + ##n by induction hypothesis 1221 = #1 + ##n by ring_one_exp 1222 = ##(SUC n) by ring_num_SUC 1223*) 1224val ring_fermat_thm = store_thm( 1225 "ring_fermat_thm", 1226 ``!r:'a ring. Ring r /\ prime (char r) ==> !n. (##n) ** (char r) = (##n)``, 1227 rpt strip_tac >> 1228 qabbrev_tac `p = char r` >> 1229 `0 < p` by rw_tac std_ss[PRIME_POS] >> 1230 `p <> 0` by decide_tac >> 1231 Induct_on `n` >| [ 1232 rw[ring_zero_exp], 1233 rw_tac std_ss[ring_num_SUC] >> 1234 `#1 IN R /\ ##n IN R` by rw[] >> 1235 metis_tac[ring_freshman_thm, ring_one_exp] 1236 ]); 1237 1238(* Theorem: [Fermat's Little Theorem Generalized] 1239 Ring r /\ prime (char r) ==> !n k. (##n) ** (char r) ** k = (##n) *) 1240(* Proof: 1241 Let p = char r. By induction on k. 1242 Base case: ##n ** p ** 0 = ##n 1243 ##n ** p ** 0 1244 = ##n ** 1 by EXP 1245 = ##n by ring_exp_1 1246 Step case: ##n ** p ** k = ##n ==> ##n ** p ** SUC k = ##n 1247 ##n ** p ** SUC k 1248 = ##n ** (p * p ** k) by EXP 1249 = ##n ** (p ** k * p) by MULT_COMM 1250 = (##n ** p ** k) ** p by ring_exp_mult 1251 = ##n ** p by induction hypothesis 1252 = ##n by ring_fermat_thm 1253*) 1254val ring_fermat_all = store_thm( 1255 "ring_fermat_all", 1256 ``!r:'a ring. Ring r /\ prime (char r) ==> !n k. (##n) ** (char r) ** k = (##n)``, 1257 rpt strip_tac >> 1258 qabbrev_tac `p = char r` >> 1259 Induct_on `k` >- 1260 rw[EXP] >> 1261 `##n ** p ** SUC k = ##n ** (p * p ** k)` by rw[EXP] >> 1262 `_ = ##n ** (p ** k * p)` by rw_tac std_ss[MULT_COMM] >> 1263 rw[ring_exp_mult, ring_fermat_thm, Abbr`p`]); 1264 1265(* Theorem: [Freshman Theorem for Ring Sum] 1266 Ring r /\ prime (char r) ==> !f. rfun f ==> !x. x IN R ==> 1267 !n. rsum (GENLIST (\j. f j * x ** j) n) ** char r = 1268 rsum (GENLIST (\j. (f j * x ** j) ** char r) n) *) 1269(* Proof: 1270 Let m = char r. 1271 By induction on n. 1272 Base case: rsum (GENLIST (\j. f j * x ** j) 0) ** m = 1273 rsum (GENLIST (\j. (f j * x ** j) ** m) 0) 1274 Note 0 < m by PRIME_POS 1275 rsum (GENLIST (\j. f j * x ** j) 0) ** m 1276 = rsum [] ** m by GENLIST 1277 = #0 ** m by ring_sum_nil 1278 = #0 by ring_zero_exp, 0 < m. 1279 = rsum [] by ring_sum_nil 1280 = rsum (GENLIST (\j. (f j * x ** j) ** m) 0) by GENLIST 1281 Step case: rsum (GENLIST (\j. f j * x ** j) (SUC n)) ** m = 1282 rsum (GENLIST (\j. (f j * x ** j) ** m) (SUC n)) 1283 Note rfun (\j. f j * x ** j) by ring_fun_from_ring_fun 1284 and rfun (\j. (f j * x ** j) ** m) by ring_fun_from_ring_fun_exp 1285 and rsum (GENLIST (\j. f j * x ** j) n) IN R by ring_sum_element, ring_list_gen_from_ring_fun 1286 rsum (GENLIST (\j. f j * x ** j) (SUC n)) ** m 1287 = (rsum (GENLIST (\j. f j * x ** j) n) + (f n * x ** n)) ** m by ring_sum_decompose_last 1288 = (rsum (GENLIST (\j. f j * x ** j) n)) ** m + (f n * x ** n) ** m by ring_freshman_thm 1289 = rsum (GENLIST (\j. (f j * x ** j) ** m) n) + (f n * x ** n) ** m by induction hypothesis 1290 = rsum (GENLIST (\j. (f j * x ** j) ** m) (SUC n)) by poly_sum_decompose_last 1291*) 1292val ring_sum_freshman_thm = store_thm( 1293 "ring_sum_freshman_thm", 1294 ``!r:'a ring. Ring r /\ prime (char r) ==> !f. rfun f ==> !x. x IN R ==> 1295 !n. rsum (GENLIST (\j. f j * x ** j) n) ** char r = 1296 rsum (GENLIST (\j. (f j * x ** j) ** char r) n)``, 1297 rpt strip_tac >> 1298 qabbrev_tac `m = char r` >> 1299 Induct_on `n` >| [ 1300 rw_tac std_ss[GENLIST, ring_sum_nil] >> 1301 `0 < m` by rw[PRIME_POS, Abbr`m`] >> 1302 `m <> 0` by decide_tac >> 1303 rw[ring_zero_exp], 1304 `rfun (\j. f j * x ** j)` by rw[ring_fun_from_ring_fun] >> 1305 `rfun (\j. (f j * x ** j) ** m)` by rw[ring_fun_from_ring_fun_exp] >> 1306 `rsum (GENLIST (\j. f j * x ** j) n) IN R` by rw[ring_sum_element, ring_list_gen_from_ring_fun] >> 1307 `!j. f j IN R` by metis_tac[ring_fun_def] >> 1308 `f n * x ** n IN R` by rw[] >> 1309 `rsum (GENLIST (\j. f j * x ** j) (SUC n)) ** m 1310 = (rsum (GENLIST (\j. f j * x ** j) n) + (f n * x ** n)) ** m` by rw[ring_sum_decompose_last] >> 1311 `_ = (rsum (GENLIST (\j. f j * x ** j) n)) ** m + (f n * x ** n) ** m` by rw[ring_freshman_thm, Abbr`m`] >> 1312 `_ = rsum (GENLIST (\j. (f j * x ** j) ** m) n) + (f n * x ** n) ** m` by rw[] >> 1313 `_ = rsum (GENLIST (\j. (f j * x ** j) ** m) (SUC n))` by rw[ring_sum_decompose_last] >> 1314 rw[] 1315 ]); 1316 1317(* Theorem: Ring r /\ prime (char r) ==> !f. rfun f ==> !x. x IN R ==> 1318 !n k. rsum (GENLIST (\j. f j * x ** j) n) ** char r ** k = 1319 rsum (GENLIST (\j. (f j * x ** j) ** char r ** k) n) *) 1320(* Proof: 1321 Let m = char r. 1322 By induction on n. 1323 Base case: rsum (GENLIST (\j. f j * x ** j) 0) ** m ** k = 1324 rsum (GENLIST (\j. (f j * x ** j) ** m ** k) 0) 1325 Note 0 < m by PRIME_POS 1326 so 0 < m ** k by EXP_NONZERO 1327 rsum (GENLIST (\j. f j * x ** j) 0) ** m ** k 1328 = rsum [] ** m ** k by GENLIST 1329 = #0 ** m ** k by ring_sum_nil 1330 = #0 by ring_zero_exp, 0 < m ** k. 1331 = rsum [] by ring_sum_nil 1332 = rsum (GENLIST (\j. (f j * x ** j) ** m ** k) 0) by GENLIST 1333 Step case: rsum (GENLIST (\j. f j * x ** j) (SUC n)) ** m ** k = 1334 rsum (GENLIST (\j. (f j * x ** j) ** m ** k) (SUC n)) 1335 Note rfun (\j. f j * x ** j) by ring_fun_from_ring_fun 1336 and rfun (\j. (f j * x ** j) ** m ** k) by ring_fun_from_ring_fun_exp 1337 and rsum (GENLIST (\j. f j * x ** j) n) IN R by ring_sum_element, ring_list_gen_from_ring_fun 1338 rsum (GENLIST (\j. f j * x ** j) (SUC n)) ** m ** k 1339 = (rsum (GENLIST (\j. f j * x ** j) n) + (f n * x ** n)) ** m ** k by ring_sum_decompose_last 1340 = (rsum (GENLIST (\j. f j * x ** j) n)) ** m ** k + (f n * x ** n) ** m ** k by ring_freshman_all 1341 = rsum (GENLIST (\j. (f j * x ** j) ** m ** k) n) + (f n * x ** n) ** m ** k by induction hypothesis 1342 = rsum (GENLIST (\j. (f j * x ** j) ** m ** k) (SUC n)) by ring_sum_decompose_last 1343*) 1344val ring_sum_freshman_all = store_thm( 1345 "ring_sum_freshman_all", 1346 ``!r:'a ring. Ring r /\ prime (char r) ==> !f. rfun f ==> !x. x IN R ==> 1347 !n k. rsum (GENLIST (\j. f j * x ** j) n) ** char r ** k = 1348 rsum (GENLIST (\j. (f j * x ** j) ** char r ** k) n)``, 1349 rpt strip_tac >> 1350 qabbrev_tac `m = char r` >> 1351 Induct_on `n` >| [ 1352 rw_tac std_ss[GENLIST, ring_sum_nil] >> 1353 `0 < m` by rw[PRIME_POS, Abbr`m`] >> 1354 `m <> 0` by decide_tac >> 1355 `m ** k <> 0` by rw[EXP_NONZERO] >> 1356 rw[ring_zero_exp], 1357 `rfun (\j. f j * x ** j)` by rw[ring_fun_from_ring_fun] >> 1358 `rfun (\j. (f j * x ** j) ** m ** k)` by rw[ring_fun_from_ring_fun_exp] >> 1359 `rsum (GENLIST (\j. f j * x ** j) n) IN R` by rw[ring_sum_element, ring_list_gen_from_ring_fun] >> 1360 `!j. f j IN R` by metis_tac[ring_fun_def] >> 1361 `f n * x ** n IN R` by rw[] >> 1362 `rsum (GENLIST (\j. f j * x ** j) (SUC n)) ** m ** k 1363 = (rsum (GENLIST (\j. f j * x ** j) n) + (f n * x ** n)) ** m ** k` by rw[ring_sum_decompose_last] >> 1364 `_ = (rsum (GENLIST (\j. f j * x ** j) n)) ** m ** k + (f n * x ** n) ** m ** k` by rw[ring_freshman_all, Abbr`m`] >> 1365 `_ = rsum (GENLIST (\j. (f j * x ** j) ** m ** k) n) + (f n * x ** n) ** m ** k` by rw[] >> 1366 `_ = rsum (GENLIST (\j. (f j * x ** j) ** m ** k) (SUC n))` by rw[ring_sum_decompose_last] >> 1367 rw[] 1368 ]); 1369 1370(* Theorem: [Frobenius Theorem] 1371 For a Ring with prime p = char r, x IN R, 1372 the map x --> x^p is a ring homomorphism to itself (endomorphism) 1373 or Ring r /\ prime (char r) ==> RingEndo (\x. x ** (char r)) r *) 1374(* Proof: 1375 Let p = char r, and prime p. 1376 First, x IN R ==> x ** p IN R by ring_exp_element. 1377 So we need to verify F(x) = x ** p is a ring homomorphism, meaning: 1378 (1) Ring r /\ prime p ==> GroupHomo (\x. x ** p) (ring_sum r) (ring_sum r) 1379 Expanding by GroupHomo_def, this is to show: 1380 Ring r /\ prime p /\ x IN R /\ x' IN R ==> (x + x') ** p = x ** p + x' ** p 1381 which is true by ring_freshman_thm. 1382 (2) Ring r ==> MonoidHomo (\x. x ** p) r.prod r.prod 1383 Expanding by MonoidHomo_def, this is to show: 1384 Ring r /\ prime p /\ x IN R /\ x' IN R ==> (x * x') ** p = x ** p * x' ** p 1385 which is true by ring_mult_exp. 1386*) 1387val ring_char_prime_endo = store_thm( 1388 "ring_char_prime_endo", 1389 ``!r:'a ring. Ring r /\ prime (char r) ==> RingEndo (\x. x ** (char r)) r``, 1390 rpt strip_tac >> 1391 rw[RingEndo_def, RingHomo_def] >| [ 1392 rw[GroupHomo_def] >> 1393 metis_tac[ring_freshman_thm], 1394 rw[MonoidHomo_def, ring_mult_monoid] 1395 ]); 1396 1397(* ------------------------------------------------------------------------- *) 1398 1399(* export theory at end *) 1400val _ = export_theory(); 1401 1402(*===========================================================================*) 1403