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