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