src/HOL/Old_Number_Theory/WilsonBij.thy
 author haftmann Mon Feb 08 17:12:30 2010 +0100 (2010-02-08) changeset 35048 82ab78fff970 parent 32960 69916a850301 child 38159 e9b4835a54ee permissions -rw-r--r--
tuned proofs
 haftmann@32479 ` 1` ```(* Author: Thomas M. Rasmussen ``` wenzelm@11049 ` 2` ``` Copyright 2000 University of Cambridge ``` paulson@9508 ` 3` ```*) ``` paulson@9508 ` 4` wenzelm@11049 ` 5` ```header {* Wilson's Theorem using a more abstract approach *} ``` wenzelm@11049 ` 6` haftmann@16417 ` 7` ```theory WilsonBij imports BijectionRel IntFact begin ``` wenzelm@11049 ` 8` wenzelm@11049 ` 9` ```text {* ``` wenzelm@11049 ` 10` ``` Wilson's Theorem using a more ``abstract'' approach based on ``` wenzelm@11049 ` 11` ``` bijections between sets. Does not use Fermat's Little Theorem ``` wenzelm@11049 ` 12` ``` (unlike Russinoff). ``` wenzelm@11049 ` 13` ```*} ``` wenzelm@11049 ` 14` wenzelm@11049 ` 15` wenzelm@11049 ` 16` ```subsection {* Definitions and lemmas *} ``` wenzelm@11049 ` 17` wenzelm@19670 ` 18` ```definition ``` wenzelm@21404 ` 19` ``` reciR :: "int => int => int => bool" where ``` wenzelm@19670 ` 20` ``` "reciR p = (\a b. zcong (a * b) 1 p \ 1 < a \ a < p - 1 \ 1 < b \ b < p - 1)" ``` wenzelm@21404 ` 21` wenzelm@21404 ` 22` ```definition ``` wenzelm@21404 ` 23` ``` inv :: "int => int => int" where ``` wenzelm@19670 ` 24` ``` "inv p a = ``` wenzelm@19670 ` 25` ``` (if zprime p \ 0 < a \ a < p then ``` paulson@11868 ` 26` ``` (SOME x. 0 \ x \ x < p \ zcong (a * x) 1 p) ``` wenzelm@19670 ` 27` ``` else 0)" ``` wenzelm@11049 ` 28` wenzelm@11049 ` 29` wenzelm@11049 ` 30` ```text {* \medskip Inverse *} ``` wenzelm@11049 ` 31` wenzelm@11049 ` 32` ```lemma inv_correct: ``` nipkow@16663 ` 33` ``` "zprime p ==> 0 < a ==> a < p ``` paulson@11868 ` 34` ``` ==> 0 \ inv p a \ inv p a < p \ [a * inv p a = 1] (mod p)" ``` wenzelm@11049 ` 35` ``` apply (unfold inv_def) ``` wenzelm@11049 ` 36` ``` apply (simp (no_asm_simp)) ``` wenzelm@11049 ` 37` ``` apply (rule zcong_lineq_unique [THEN ex1_implies_ex, THEN someI_ex]) ``` wenzelm@11049 ` 38` ``` apply (erule_tac [2] zless_zprime_imp_zrelprime) ``` wenzelm@11049 ` 39` ``` apply (unfold zprime_def) ``` wenzelm@11049 ` 40` ``` apply auto ``` wenzelm@11049 ` 41` ``` done ``` wenzelm@11049 ` 42` wenzelm@11049 ` 43` ```lemmas inv_ge = inv_correct [THEN conjunct1, standard] ``` wenzelm@11049 ` 44` ```lemmas inv_less = inv_correct [THEN conjunct2, THEN conjunct1, standard] ``` wenzelm@11049 ` 45` ```lemmas inv_is_inv = inv_correct [THEN conjunct2, THEN conjunct2, standard] ``` wenzelm@11049 ` 46` wenzelm@11049 ` 47` ```lemma inv_not_0: ``` nipkow@16663 ` 48` ``` "zprime p ==> 1 < a ==> a < p - 1 ==> inv p a \ 0" ``` wenzelm@11049 ` 49` ``` -- {* same as @{text WilsonRuss} *} ``` wenzelm@11049 ` 50` ``` apply safe ``` wenzelm@11049 ` 51` ``` apply (cut_tac a = a and p = p in inv_is_inv) ``` wenzelm@11049 ` 52` ``` apply (unfold zcong_def) ``` wenzelm@11049 ` 53` ``` apply auto ``` paulson@11868 ` 54` ``` apply (subgoal_tac "\ p dvd 1") ``` wenzelm@11049 ` 55` ``` apply (rule_tac [2] zdvd_not_zless) ``` paulson@11868 ` 56` ``` apply (subgoal_tac "p dvd 1") ``` wenzelm@11049 ` 57` ``` prefer 2 ``` nipkow@30042 ` 58` ``` apply (subst dvd_minus_iff [symmetric]) ``` wenzelm@11049 ` 59` ``` apply auto ``` wenzelm@11049 ` 60` ``` done ``` paulson@9508 ` 61` wenzelm@11049 ` 62` ```lemma inv_not_1: ``` nipkow@16663 ` 63` ``` "zprime p ==> 1 < a ==> a < p - 1 ==> inv p a \ 1" ``` wenzelm@11049 ` 64` ``` -- {* same as @{text WilsonRuss} *} ``` wenzelm@11049 ` 65` ``` apply safe ``` wenzelm@11049 ` 66` ``` apply (cut_tac a = a and p = p in inv_is_inv) ``` wenzelm@11049 ` 67` ``` prefer 4 ``` wenzelm@11049 ` 68` ``` apply simp ``` paulson@11868 ` 69` ``` apply (subgoal_tac "a = 1") ``` wenzelm@11049 ` 70` ``` apply (rule_tac [2] zcong_zless_imp_eq) ``` wenzelm@11049 ` 71` ``` apply auto ``` wenzelm@11049 ` 72` ``` done ``` wenzelm@11049 ` 73` paulson@11868 ` 74` ```lemma aux: "[a * (p - 1) = 1] (mod p) = [a = p - 1] (mod p)" ``` wenzelm@11049 ` 75` ``` -- {* same as @{text WilsonRuss} *} ``` wenzelm@11049 ` 76` ``` apply (unfold zcong_def) ``` haftmann@35048 ` 77` ``` apply (simp add: diff_diff_eq diff_diff_eq2 zdiff_zmult_distrib2) ``` paulson@11868 ` 78` ``` apply (rule_tac s = "p dvd -((a + 1) + (p * -a))" in trans) ``` haftmann@35048 ` 79` ``` apply (simp add: algebra_simps) ``` nipkow@30042 ` 80` ``` apply (subst dvd_minus_iff) ``` wenzelm@11049 ` 81` ``` apply (subst zdvd_reduce) ``` paulson@11868 ` 82` ``` apply (rule_tac s = "p dvd (a + 1) + (p * -1)" in trans) ``` wenzelm@11049 ` 83` ``` apply (subst zdvd_reduce) ``` wenzelm@11049 ` 84` ``` apply auto ``` wenzelm@11049 ` 85` ``` done ``` wenzelm@11049 ` 86` wenzelm@11049 ` 87` ```lemma inv_not_p_minus_1: ``` nipkow@16663 ` 88` ``` "zprime p ==> 1 < a ==> a < p - 1 ==> inv p a \ p - 1" ``` wenzelm@11049 ` 89` ``` -- {* same as @{text WilsonRuss} *} ``` wenzelm@11049 ` 90` ``` apply safe ``` wenzelm@11049 ` 91` ``` apply (cut_tac a = a and p = p in inv_is_inv) ``` wenzelm@11049 ` 92` ``` apply auto ``` wenzelm@11049 ` 93` ``` apply (simp add: aux) ``` paulson@11868 ` 94` ``` apply (subgoal_tac "a = p - 1") ``` wenzelm@11049 ` 95` ``` apply (rule_tac [2] zcong_zless_imp_eq) ``` wenzelm@11049 ` 96` ``` apply auto ``` wenzelm@11049 ` 97` ``` done ``` wenzelm@11049 ` 98` wenzelm@11049 ` 99` ```text {* ``` wenzelm@11049 ` 100` ``` Below is slightly different as we don't expand @{term [source] inv} ``` wenzelm@11049 ` 101` ``` but use ``@{text correct}'' theorems. ``` wenzelm@11049 ` 102` ```*} ``` wenzelm@11049 ` 103` nipkow@16663 ` 104` ```lemma inv_g_1: "zprime p ==> 1 < a ==> a < p - 1 ==> 1 < inv p a" ``` paulson@11868 ` 105` ``` apply (subgoal_tac "inv p a \ 1") ``` paulson@11868 ` 106` ``` apply (subgoal_tac "inv p a \ 0") ``` wenzelm@11049 ` 107` ``` apply (subst order_less_le) ``` wenzelm@11049 ` 108` ``` apply (subst zle_add1_eq_le [symmetric]) ``` wenzelm@11049 ` 109` ``` apply (subst order_less_le) ``` wenzelm@11049 ` 110` ``` apply (rule_tac [2] inv_not_0) ``` wenzelm@11049 ` 111` ``` apply (rule_tac [5] inv_not_1) ``` wenzelm@11049 ` 112` ``` apply auto ``` wenzelm@11049 ` 113` ``` apply (rule inv_ge) ``` wenzelm@11049 ` 114` ``` apply auto ``` wenzelm@11049 ` 115` ``` done ``` wenzelm@11049 ` 116` wenzelm@11049 ` 117` ```lemma inv_less_p_minus_1: ``` nipkow@16663 ` 118` ``` "zprime p ==> 1 < a ==> a < p - 1 ==> inv p a < p - 1" ``` wenzelm@11049 ` 119` ``` -- {* ditto *} ``` wenzelm@11049 ` 120` ``` apply (subst order_less_le) ``` wenzelm@11049 ` 121` ``` apply (simp add: inv_not_p_minus_1 inv_less) ``` wenzelm@11049 ` 122` ``` done ``` wenzelm@11049 ` 123` wenzelm@11049 ` 124` wenzelm@11049 ` 125` ```text {* \medskip Bijection *} ``` wenzelm@11049 ` 126` paulson@11868 ` 127` ```lemma aux1: "1 < x ==> 0 \ (x::int)" ``` wenzelm@11049 ` 128` ``` apply auto ``` wenzelm@11049 ` 129` ``` done ``` paulson@9508 ` 130` paulson@11868 ` 131` ```lemma aux2: "1 < x ==> 0 < (x::int)" ``` wenzelm@11049 ` 132` ``` apply auto ``` wenzelm@11049 ` 133` ``` done ``` wenzelm@11049 ` 134` wenzelm@11704 ` 135` ```lemma aux3: "x \ p - 2 ==> x < (p::int)" ``` wenzelm@11049 ` 136` ``` apply auto ``` wenzelm@11049 ` 137` ``` done ``` wenzelm@11049 ` 138` paulson@11868 ` 139` ```lemma aux4: "x \ p - 2 ==> x < (p::int) - 1" ``` wenzelm@11049 ` 140` ``` apply auto ``` wenzelm@11049 ` 141` ``` done ``` wenzelm@11049 ` 142` nipkow@16663 ` 143` ```lemma inv_inj: "zprime p ==> inj_on (inv p) (d22set (p - 2))" ``` wenzelm@11049 ` 144` ``` apply (unfold inj_on_def) ``` wenzelm@11049 ` 145` ``` apply auto ``` wenzelm@11049 ` 146` ``` apply (rule zcong_zless_imp_eq) ``` wenzelm@11049 ` 147` ``` apply (tactic {* stac (thm "zcong_cancel" RS sym) 5 *}) ``` wenzelm@11049 ` 148` ``` apply (rule_tac [7] zcong_trans) ``` wenzelm@11049 ` 149` ``` apply (tactic {* stac (thm "zcong_sym") 8 *}) ``` wenzelm@11049 ` 150` ``` apply (erule_tac [7] inv_is_inv) ``` wenzelm@23894 ` 151` ``` apply (tactic "asm_simp_tac @{simpset} 9") ``` wenzelm@11049 ` 152` ``` apply (erule_tac [9] inv_is_inv) ``` wenzelm@11049 ` 153` ``` apply (rule_tac [6] zless_zprime_imp_zrelprime) ``` wenzelm@11049 ` 154` ``` apply (rule_tac [8] inv_less) ``` wenzelm@11049 ` 155` ``` apply (rule_tac [7] inv_g_1 [THEN aux2]) ``` wenzelm@11049 ` 156` ``` apply (unfold zprime_def) ``` wenzelm@11049 ` 157` ``` apply (auto intro: d22set_g_1 d22set_le ``` wenzelm@32960 ` 158` ``` aux1 aux2 aux3 aux4) ``` wenzelm@11049 ` 159` ``` done ``` wenzelm@11049 ` 160` wenzelm@11049 ` 161` ```lemma inv_d22set_d22set: ``` nipkow@16663 ` 162` ``` "zprime p ==> inv p ` d22set (p - 2) = d22set (p - 2)" ``` wenzelm@11049 ` 163` ``` apply (rule endo_inj_surj) ``` wenzelm@11049 ` 164` ``` apply (rule d22set_fin) ``` wenzelm@11049 ` 165` ``` apply (erule_tac [2] inv_inj) ``` wenzelm@11049 ` 166` ``` apply auto ``` wenzelm@11049 ` 167` ``` apply (rule d22set_mem) ``` wenzelm@11049 ` 168` ``` apply (erule inv_g_1) ``` paulson@11868 ` 169` ``` apply (subgoal_tac [3] "inv p xa < p - 1") ``` wenzelm@11049 ` 170` ``` apply (erule_tac [4] inv_less_p_minus_1) ``` wenzelm@11049 ` 171` ``` apply (auto intro: d22set_g_1 d22set_le aux4) ``` wenzelm@11049 ` 172` ``` done ``` wenzelm@11049 ` 173` wenzelm@11049 ` 174` ```lemma d22set_d22set_bij: ``` nipkow@16663 ` 175` ``` "zprime p ==> (d22set (p - 2), d22set (p - 2)) \ bijR (reciR p)" ``` wenzelm@11049 ` 176` ``` apply (unfold reciR_def) ``` wenzelm@11704 ` 177` ``` apply (rule_tac s = "(d22set (p - 2), inv p ` d22set (p - 2))" in subst) ``` wenzelm@11049 ` 178` ``` apply (simp add: inv_d22set_d22set) ``` wenzelm@11049 ` 179` ``` apply (rule inj_func_bijR) ``` wenzelm@11049 ` 180` ``` apply (rule_tac [3] d22set_fin) ``` wenzelm@11049 ` 181` ``` apply (erule_tac [2] inv_inj) ``` wenzelm@11049 ` 182` ``` apply auto ``` wenzelm@11049 ` 183` ``` apply (erule inv_is_inv) ``` wenzelm@11049 ` 184` ``` apply (erule_tac [5] inv_g_1) ``` wenzelm@11049 ` 185` ``` apply (erule_tac [7] inv_less_p_minus_1) ``` wenzelm@11049 ` 186` ``` apply (auto intro: d22set_g_1 d22set_le aux2 aux3 aux4) ``` wenzelm@11049 ` 187` ``` done ``` wenzelm@11049 ` 188` nipkow@16663 ` 189` ```lemma reciP_bijP: "zprime p ==> bijP (reciR p) (d22set (p - 2))" ``` wenzelm@11049 ` 190` ``` apply (unfold reciR_def bijP_def) ``` wenzelm@11049 ` 191` ``` apply auto ``` wenzelm@11049 ` 192` ``` apply (rule d22set_mem) ``` wenzelm@11049 ` 193` ``` apply auto ``` wenzelm@11049 ` 194` ``` done ``` wenzelm@11049 ` 195` nipkow@16663 ` 196` ```lemma reciP_uniq: "zprime p ==> uniqP (reciR p)" ``` wenzelm@11049 ` 197` ``` apply (unfold reciR_def uniqP_def) ``` wenzelm@11049 ` 198` ``` apply auto ``` wenzelm@11049 ` 199` ``` apply (rule zcong_zless_imp_eq) ``` wenzelm@11049 ` 200` ``` apply (tactic {* stac (thm "zcong_cancel2" RS sym) 5 *}) ``` wenzelm@11049 ` 201` ``` apply (rule_tac [7] zcong_trans) ``` wenzelm@11049 ` 202` ``` apply (tactic {* stac (thm "zcong_sym") 8 *}) ``` wenzelm@11049 ` 203` ``` apply (rule_tac [6] zless_zprime_imp_zrelprime) ``` wenzelm@11049 ` 204` ``` apply auto ``` wenzelm@11049 ` 205` ``` apply (rule zcong_zless_imp_eq) ``` wenzelm@11049 ` 206` ``` apply (tactic {* stac (thm "zcong_cancel" RS sym) 5 *}) ``` wenzelm@11049 ` 207` ``` apply (rule_tac [7] zcong_trans) ``` wenzelm@11049 ` 208` ``` apply (tactic {* stac (thm "zcong_sym") 8 *}) ``` wenzelm@11049 ` 209` ``` apply (rule_tac [6] zless_zprime_imp_zrelprime) ``` wenzelm@11049 ` 210` ``` apply auto ``` wenzelm@11049 ` 211` ``` done ``` wenzelm@11049 ` 212` nipkow@16663 ` 213` ```lemma reciP_sym: "zprime p ==> symP (reciR p)" ``` wenzelm@11049 ` 214` ``` apply (unfold reciR_def symP_def) ``` wenzelm@11049 ` 215` ``` apply (simp add: zmult_commute) ``` wenzelm@11049 ` 216` ``` apply auto ``` wenzelm@11049 ` 217` ``` done ``` wenzelm@11049 ` 218` nipkow@16663 ` 219` ```lemma bijER_d22set: "zprime p ==> d22set (p - 2) \ bijER (reciR p)" ``` wenzelm@11049 ` 220` ``` apply (rule bijR_bijER) ``` wenzelm@11049 ` 221` ``` apply (erule d22set_d22set_bij) ``` wenzelm@11049 ` 222` ``` apply (erule reciP_bijP) ``` wenzelm@11049 ` 223` ``` apply (erule reciP_uniq) ``` wenzelm@11049 ` 224` ``` apply (erule reciP_sym) ``` wenzelm@11049 ` 225` ``` done ``` wenzelm@11049 ` 226` wenzelm@11049 ` 227` wenzelm@11049 ` 228` ```subsection {* Wilson *} ``` wenzelm@11049 ` 229` wenzelm@11049 ` 230` ```lemma bijER_zcong_prod_1: ``` nipkow@16663 ` 231` ``` "zprime p ==> A \ bijER (reciR p) ==> [\A = 1] (mod p)" ``` wenzelm@11049 ` 232` ``` apply (unfold reciR_def) ``` wenzelm@11049 ` 233` ``` apply (erule bijER.induct) ``` paulson@11868 ` 234` ``` apply (subgoal_tac [2] "a = 1 \ a = p - 1") ``` wenzelm@11049 ` 235` ``` apply (rule_tac [3] zcong_square_zless) ``` wenzelm@11049 ` 236` ``` apply auto ``` wenzelm@11049 ` 237` ``` apply (subst setprod_insert) ``` wenzelm@11049 ` 238` ``` prefer 3 ``` wenzelm@11049 ` 239` ``` apply (subst setprod_insert) ``` wenzelm@11049 ` 240` ``` apply (auto simp add: fin_bijER) ``` nipkow@15392 ` 241` ``` apply (subgoal_tac "zcong ((a * b) * \A) (1 * 1) p") ``` wenzelm@11049 ` 242` ``` apply (simp add: zmult_assoc) ``` wenzelm@11049 ` 243` ``` apply (rule zcong_zmult) ``` wenzelm@11049 ` 244` ``` apply auto ``` wenzelm@11049 ` 245` ``` done ``` wenzelm@11049 ` 246` nipkow@16663 ` 247` ```theorem Wilson_Bij: "zprime p ==> [zfact (p - 1) = -1] (mod p)" ``` paulson@11868 ` 248` ``` apply (subgoal_tac "zcong ((p - 1) * zfact (p - 2)) (-1 * 1) p") ``` wenzelm@11049 ` 249` ``` apply (rule_tac [2] zcong_zmult) ``` wenzelm@11049 ` 250` ``` apply (simp add: zprime_def) ``` wenzelm@11049 ` 251` ``` apply (subst zfact.simps) ``` paulson@11868 ` 252` ``` apply (rule_tac t = "p - 1 - 1" and s = "p - 2" in subst) ``` wenzelm@11049 ` 253` ``` apply auto ``` wenzelm@11049 ` 254` ``` apply (simp add: zcong_def) ``` wenzelm@11049 ` 255` ``` apply (subst d22set_prod_zfact [symmetric]) ``` wenzelm@11049 ` 256` ``` apply (rule bijER_zcong_prod_1) ``` wenzelm@11049 ` 257` ``` apply (rule_tac [2] bijER_d22set) ``` wenzelm@11049 ` 258` ``` apply auto ``` wenzelm@11049 ` 259` ``` done ``` paulson@9508 ` 260` paulson@9508 ` 261` ```end ```