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