1(* ------------------------------------------------------------------------- *)
2(* Fermat's Little Theorem - Necklace proof of Julius Petersen.              *)
3(* ------------------------------------------------------------------------- *)
4
5(*
6
7Fermat's Little Theorem (Combinatorial proof)
8=============================================
9Solomon W. Golomb (1956)
10http://www.cimat.mx/~mmoreno/teaching/spring08/Fermats_Little_Thm.pdf
11
12Original proof by J. Petersen in 1872:
13
14Take p elements from q with repetitions in all ways, that is, in q^p ways.
15The q sets with elements all alike are not changed by a cyclic permutation of the elements,
16while the remaining q^p - q sets are permuted in sets of p. Hence p divides q^p - q.
17
18This is a combinatorial using Group action, via Orbit-Stabilizer Theorem.
19
20*)
21
22(*===========================================================================*)
23
24(*===========================================================================*)
25
26(* add all dependent libraries for script *)
27open HolKernel boolLib bossLib Parse;
28
29(* declare new theory at start *)
30val _ = new_theory "FLTpetersen";
31
32(* ------------------------------------------------------------------------- *)
33
34
35(* open dependent theories *)
36(* val _ = load "FLTactionTheory"; *)
37open helperNumTheory helperSetTheory;
38open arithmeticTheory pred_setTheory;
39open dividesTheory; (* for PRIME_POS *)
40
41open necklaceTheory; (* for multicoloured_finite *)
42
43open groupTheory;
44open groupActionTheory;
45
46
47(* ------------------------------------------------------------------------- *)
48(* Fermat's Little Theorem by Action Documentation                           *)
49(* ------------------------------------------------------------------------- *)
50(* Overloading:
51*)
52(*
53
54   From groupInstances:
55   Zadd_group          |- !n. 0 < n ==> Group (Zadd n)
56
57   From FLTnecklace:
58   necklace_cycle      |- !n a ls k. ls IN necklace n a ==> cycle k ls IN necklace n a
59   multicoloured_cycle |- !n a ls k. ls IN multicoloured n a ==> cycle k ls IN multicoloured n a
60   multicoloured_not_cycle_1
61                       |- !n a ls. ls IN multicoloured n a ==> cycle 1 ls <> ls
62
63   From FLTaction:
64   cycle_action_on_multicoloured
65                       |- !n a. 0 < n ==> (Zadd n act multicoloured n a) cycle
66   multicoloured_orbit_not_sing
67                       |- !n a ls. ls IN multicoloured n a ==>
68                                   ~SING (orbit cycle (Zadd n) (multicoloured n a) ls)
69   multicoloured_orbit_card_not_1
70                       |- !n a ls. ls IN multicoloured n a ==>
71                                   CARD (orbit cycle (Zadd n) (multicoloured n a) ls) <> 1
72   multicoloured_orbit_card_prime
73                       |- !p a ls. prime p /\ ls IN multicoloured p a ==>
74                                   CARD (orbit cycle (Zadd p) (multicoloured p a) ls) = p
75
76   Application:
77   Fermat_Little_Theorem   |- !p a. prime p ==> a ** p MOD p = a MOD p
78
79*)
80
81(* ------------------------------------------------------------------------- *)
82(* Note: This is a self-contained proof following Petersen's style.          *)
83(* ------------------------------------------------------------------------- *)
84
85(* ------------------------------------------------------------------------- *)
86(* Combinatorial Proof via Group action.                                     *)
87(* ------------------------------------------------------------------------- *)
88
89(* Part 1: Basic ----------------------------------------------------------- *)
90
91val Zadd_group = groupInstancesTheory.Zadd_group;
92(* |- !n. 0 < n ==> Group (Zadd n) *)
93
94val necklace_cycle = FLTnecklaceTheory.necklace_cycle;
95(* |- !n a ls k. ls IN necklace n a ==> cycle k ls IN necklace n a *)
96
97val multicoloured_cycle = FLTnecklaceTheory.multicoloured_cycle;
98(* |- !n a ls k. ls IN multicoloured n a ==> cycle k ls IN multicoloured n a *)
99
100val multicoloured_not_cycle_1 = FLTnecklaceTheory.multicoloured_not_cycle_1;
101(* |- !n a ls. ls IN multicoloured n a ==> cycle 1 ls <> ls *)
102
103(* Part 2: Action ---------------------------------------------------------- *)
104
105val cycle_action_on_multicoloured = FLTactionTheory.cycle_action_on_multicoloured;
106(* |- !n a. 0 < n ==> (Zadd n act multicoloured n a) cycle *)
107
108val multicoloured_orbit_not_sing = FLTactionTheory.multicoloured_orbit_not_sing;
109(* |- !n a ls. ls IN multicoloured n a ==>
110               ~SING (orbit cycle (Zadd n) (multicoloured n a) ls) *)
111
112val multicoloured_orbit_card_not_1 = FLTactionTheory.multicoloured_orbit_card_not_1;
113(* |- !n a ls. ls IN multicoloured n a ==>
114               CARD (orbit cycle (Zadd n) (multicoloured n a) ls) <> 1 *)
115
116val multicoloured_orbit_card_prime = FLTactionTheory.multicoloured_orbit_card_prime;
117(* |- !p a ls. prime p /\ ls IN multicoloured p a ==>
118              CARD (orbit cycle (Zadd p) (multicoloured p a) ls) = p *)
119
120(* Part 3: Application ----------------------------------------------------- *)
121
122(* Idea: [Fermat's Little Theorem] -- line by line
123         !p a. prime p ==> p divides (a ** p - a)   *)
124(* Proof (J. Petersen in 1872):
125   Take p elements from a with repetitions in all ways, that is, in a^p ways.
126                   by necklace_card
127   The a sets with elements all alike are not changed by a cyclic permutation of the elements,
128                   by monocoloured_card
129   while the remaining (a^p - a) sets are
130                   by multicoloured_card
131   permuted in sets of p.
132                   by cycle_action_on_multicoloured, multicoloured_orbit_card_prime
133   Hence p divides a^p - a.
134                   by orbits_equal_size_property
135*)
136
137(* Theorem: prime p ==> p divides (a ** p - a) *)
138(* Proof:
139   Let X = multicoloured p a,
140       b = (\ls. orbit cycle (Zadd p) ls).
141   Note 0 < p                      by PRIME_POS
142    and FINITE X                   by multicoloured_finite
143   with CARD X = a ** p - a        by multicoloured_card, 0 < p
144   Also Group (Zadd p)             by Zadd_group, 0 < p
145   with (Zadd p act A) cycle       by cycle_action_on_multicoloured, 0 < p
146   then !ls. ls IN X ==>
147             (CARD (b ls) = p)     by rw[multicoloured_orbit_card_prime
148   thus p divides CARD X           by orbits_equal_size_property
149     or p divides (a ** p - a)     by above
150     so (a ** p - a) MOD p = 0     by DIVIDES_MOD_0, 0 < p
151    Now a <= a ** p                by EXP_LE, 0 < p
152    ==> a ** p MOD p = a MOD p     by MOD_EQ, 0 < p
153
154orbits_equal_size_property |> ISPEC ``cycle`` |> ISPEC ``Zadd p``;
155|- !X n. Group (Zadd p) /\ (Zadd p act X) cycle /\ FINITE X /\
156         (!x. x IN X ==> CARD (orbit cycle (Zadd p) x) = n) ==> n divides CARD X
157*)
158Theorem Fermat_Little_Theorem:
159  !p a. prime p ==> a ** p MOD p = a MOD p
160Proof
161  rpt strip_tac >>
162  (* prime p is positive *)
163  `0 < p` by rw[PRIME_POS] >>
164  (* let X = the set of multicoloured necklaces *)
165  qabbrev_tac `X = multicoloured p a` >>
166  (* set X is finite *)
167  `FINITE X` by rw[multicoloured_finite, Abbr`X`] >>
168  (* and cardinality of X is known *)
169  `CARD X = a ** p - a` by rw[multicoloured_card, Abbr`X`] >>
170  (* Modulo p is an additive group, by 0 < p *)
171  `Group (Zadd p)` by rw[Zadd_group] >>
172  (* and acts on X by cycle *)
173  `(Zadd p act X) cycle` by rw[cycle_action_on_multicoloured, Abbr`X`] >>
174  (* then all orbits of multicoloured necklaces has size equal to p *)
175  imp_res_tac multicoloured_orbit_card_prime >>
176  (* therefore prime p divides the cardinality of X *)
177  `p divides (a ** p - a)` by metis_tac[orbits_equal_size_property] >>
178  (* or a ** p and a have the same remainder in modulo p *)
179  metis_tac[DIVIDES_MOD_0, EXP_LE, MOD_EQ]
180QED
181
182
183(* Part 4: End ------------------------------------------------------------- *)
184
185(* ------------------------------------------------------------------------- *)
186
187(* export theory at end *)
188val _ = export_theory();
189
190(*===========================================================================*)
191