1(* ------------------------------------------------------------------------- *) 2(* Binomial coefficients and expansion, for Field *) 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 "fieldBinomial"; 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 "ringTheory"; *) *) 31(* val _ = load "fieldMapTheory"; *) 32open fieldTheory; 33open ringTheory; 34open groupTheory; 35open monoidTheory; 36 37open monoidMapTheory groupMapTheory ringMapTheory fieldMapTheory; 38 39(* val _ = load "ringBinomialTheory"; *) 40open ringBinomialTheory; 41 42(* Get dependent theories in lib *) 43(* (* val _ = load "helperNumTheory"; -- in monoidTheory *) *) 44(* (* val _ = load "helperSetTheory"; -- in monoidTheory *) *) 45open helperNumTheory helperSetTheory; 46 47 48(* ------------------------------------------------------------------------- *) 49(* Field Binomial Documentation *) 50(* ------------------------------------------------------------------------- *) 51(* 52 Overloading: 53*) 54(* Definitions and Theorems (# are exported): 55 56 Field Binomial Theorems: 57 field_binomial_property |- !r. Field r ==> !k. 0 < k /\ k < char r ==> (##(binomial (char r) k) = #0) 58 finite_field_freshman_thm |- !r. FiniteField r ==> !x y. x IN R /\ y IN R ==> 59 ((x + y) ** char r = x ** char r + y ** char r) 60 finite_field_freshman_all |- !r. FiniteField r ==> !x y. x IN R /\ y IN R ==> 61 !k. (x + y) ** char r ** k = x ** char r ** k + y ** char r ** k 62 finite_field_freshman_all_sub |- !r. FiniteField r ==> !x y. x IN R /\ y IN R ==> 63 !k. (x - y) ** char r ** k = x ** char r ** k - y ** char r ** k 64 finite_field_num_fermat_thm |- !r. FiniteField r ==> !n. ##n ** char r = ##n 65 finite_field_num_fermat_all |- !r. FiniteField r ==> !n k. ##n ** char r ** k = ##n 66 finite_field_map_endo |- !r. FiniteField r ==> FieldEndo (\x. x ** char r) r 67 finite_field_map_auto |- !r. FiniteField r /\ (CARD R = char r) ==> FieldAuto (\x. x ** char r) r 68*) 69 70(* ------------------------------------------------------------------------- *) 71(* Field Binomial Theorems *) 72(* ------------------------------------------------------------------------- *) 73 74(* Theorem: Field r ==> 1 < char r /\ ##(binomial (char r) k) = #0 for 0 < k < (char r) *) 75(* Proof: 76 Field r ==> prime (char r) or char r = 0 by field_char 77 If char r = 0, no k in range 0 ... char. 78 Otherwise, true by ring_char_prime 79*) 80val field_binomial_property = store_thm( 81 "field_binomial_property", 82 ``!r:'a field. Field r ==> !k. 0 < k /\ k < char r ==> (##(binomial (char r) k) = #0)``, 83 rpt strip_tac >> 84 `(char r = 0) \/ prime (char r)` by rw[field_char] >- 85 metis_tac[DECIDE ``!k. 0 < k /\ k < 0 <=> F``] >> 86 metis_tac[ring_char_prime, field_is_ring]); 87 88(* Theorem: [Freshman's Theorem] FiniteField r ==> (x + y)^(char r) = x^(char r) + y^(char r) *) 89(* Proof: 90 FiniteField r ==> prime (char r) by finite_field_char 91 FiniteField r ==> Ring r by FiniteField_def, field_is_ring 92 Hence true by ring_freshman_thm 93*) 94val finite_field_freshman_thm = store_thm( 95 "finite_field_freshman_thm", 96 ``!r:'a field. FiniteField r ==> !x y. x IN R /\ y IN R ==> ((x + y) ** (char r) = x ** (char r) + y ** (char r))``, 97 rw[ring_freshman_thm, finite_field_char, FiniteField_def]); 98 99(* Theorem: [Freshman's Theorem Generalized] 100 FiniteField r ==> 1 < char r /\ !k. (x + y)^(char r)^k = x^(char r)^k + y^(char r)^k 101 Note: a^b^c = a^(b^c) *) 102(* Proof: 103 FiniteField r ==> prime (char r) by finite_field_char 104 FiniteField r ==> Ring r by FiniteField_def, field_is_ring 105 Hence true by ring_freshman_all 106*) 107val finite_field_freshman_all = store_thm( 108 "finite_field_freshman_all", 109 ``!r:'a field. FiniteField r ==> 110 !x y. x IN R /\ y IN R ==> !k. (x + y) ** (char r) ** k = x ** (char r) ** k + y ** (char r) ** k``, 111 rw[ring_freshman_all, finite_field_char, FiniteField_def]); 112 113(* Theorem: FiniteField r ==> !x y. x IN R /\ y IN R ==> 114 !k. (x - y) ** char r ** k = x ** char r ** k - y ** char r ** k *) 115(* Proof: 116 Note prime (char r) by finite_field_char 117 Hence the result follows by ring_freshman_all_sub 118*) 119val finite_field_freshman_all_sub = store_thm( 120 "finite_field_freshman_all_sub", 121 ``!r:'a field. FiniteField r ==> !x y. x IN R /\ y IN R ==> 122 !k. (x - y) ** char r ** k = x ** char r ** k - y ** char r ** k``, 123 metis_tac[finite_field_char, ring_freshman_all_sub, finite_field_is_field, field_is_ring]); 124 125(* Theorem: [Fermat's Little Theorem] FiniteField r ==> (##n) ** (char r) = (##n) *) 126(* Proof: 127 FiniteField r ==> prime (char r) by finite_field_char 128 FiniteField r ==> Ring r by FiniteField_def, field_is_ring 129 Hence true by ring_fermat_thm 130*) 131val finite_field_num_fermat_thm = store_thm( 132 "finite_field_num_fermat_thm", 133 ``!r:'a field. FiniteField r ==> !n. (##n) ** (char r) = (##n)``, 134 rw[ring_fermat_thm, finite_field_char, FiniteField_def]); 135 136(* Theorem: [Fermat's Little Theorem Generalized] FiniteField r ==> !k. (##n) ** (char r) ** k = (##n) *) 137(* Proof: 138 FiniteField r ==> prime (char r) by finite_field_char 139 FiniteField r ==> Ring r by FiniteField_def, field_is_ring 140 Hence true by ring_fermat_all 141*) 142val finite_field_num_fermat_all = store_thm( 143 "finite_field_num_fermat_all", 144 ``!r:'a field. FiniteField r ==> !n k. (##n) ** (char r) ** k = (##n)``, 145 rw[ring_fermat_all, finite_field_char, FiniteField_def]); 146 147(* Theorem: [Frobenius Theorem] 148 For a FiniteField r, x IN R, 149 the map x --> x^p is a ring homomorphism to itself (endomorphism) 150 or FiniteField r ==> RingEndo (\x. x ** (char r)) r *) 151(* Proof: 152 Let p = char r. 153 First, x IN R ==> x ** p IN R by field_exp_element. 154 So we need to verify F(x) = x ** p is a ring homomorphism, meaning: 155 (1) FiniteField r ==> GroupHomo (\x. x ** p) (ring_sum r) (ring_sum r) 156 Expanding by GroupHomo_def, this is to show: 157 FiniteField r /\ x IN R /\ x' IN R ==> (x + x') ** p = x ** p + x' ** p 158 which is true by finite_field_freshman_thm. 159 (2) FiniteField r ==> MonoidHomo (\x. x ** p) r.prod r.prod 160 Expanding by MonoidHomo_def, this is to show: 161 FiniteField r /\ x IN R /\ x' IN r ==> (x * x') ** p = x ** p * x' ** p 162 which is true by field_mult_exp. 163*) 164val finite_field_map_endo = store_thm( 165 "finite_field_map_endo", 166 ``!r:'a ring. FiniteField r ==> FieldEndo (\x. x ** (char r)) r``, 167 rpt strip_tac >> 168 `Field r /\ FINITE R` by metis_tac[FiniteField_def] >> 169 qabbrev_tac `p = char r` >> 170 rw[FieldEndo_def, FieldHomo_def, RingHomo_def] >| [ 171 rw[GroupHomo_def] >> 172 rw[finite_field_freshman_thm, Abbr`p`], 173 rw[MonoidHomo_def] 174 ]); 175 176(* Theorem: FiniteField r /\ (CARD R = char r) ==> FieldAuto (\x. x ** char r) r *) 177(* Proof: 178 By FieldAuto_def, FieldIso_def, this is to show: 179 (1) FieldHomo (\x. x ** char r) r r 180 Since FieldEndo (\x. x ** char r) r by finite_field_map_endo 181 so FieldHomo (\x. x ** char r) r r by FieldEndo_def 182 (2) (\x. x ** char r) PERMUTES R 183 Note !x. x IN R ==> (x ** char r = x) by finite_field_fermat_thm, CARD R = char r 184 Expand by BIJ_DEF, INJ_DEF, SURJ_DEF, this is to show: 185 (1) x IN R ==> x ** char r IN R, true by field_exp_element 186 (2) x IN R /\ x' IN R /\ x ** char r = x' ** char r ==> x = x' 187 Since x ** char r = x by above, finite_field_fermat_thm 188 and x' ** char r = x' by above, finite_field_fermat_thm 189 This is trivially true. 190 (3) same as (1) 191 (4) x IN R ==> ?x'. x' IN R /\ (x' ** char r = x), true by taking x' = x. 192*) 193val finite_field_map_auto = store_thm( 194 "finite_field_map_auto", 195 ``!r:'a field. FiniteField r /\ (CARD R = char r) ==> FieldAuto (\x. x ** char r) r``, 196 rpt (stripDup[FiniteField_def]) >> 197 rw_tac std_ss[FieldAuto_def, FieldIso_def] >- 198 metis_tac[finite_field_map_endo, FieldEndo_def] >> 199 `!x. x IN R ==> (x ** char r = x)` by metis_tac[finite_field_fermat_thm] >> 200 rw[BIJ_DEF, INJ_DEF, SURJ_DEF] >> 201 metis_tac[]); 202 203(* ------------------------------------------------------------------------- *) 204 205(* export theory at end *) 206val _ = export_theory(); 207 208(*===========================================================================*) 209