src/HOL/NumberTheory/EulerFermat.thy
author wenzelm
Tue Aug 27 11:03:05 2002 +0200 (2002-08-27)
changeset 13524 604d0f3622d6
parent 13187 e5434b822a96
child 13833 f8dcb1d9ea68
permissions -rw-r--r--
*** empty log message ***
     1 (*  Title:      HOL/NumberTheory/EulerFermat.thy
     2     ID:         $Id$
     3     Author:     Thomas M. Rasmussen
     4     Copyright   2000  University of Cambridge
     5 *)
     6 
     7 header {* Fermat's Little Theorem extended to Euler's Totient function *}
     8 
     9 theory EulerFermat = BijectionRel + IntFact:
    10 
    11 text {*
    12   Fermat's Little Theorem extended to Euler's Totient function. More
    13   abstract approach than Boyer-Moore (which seems necessary to achieve
    14   the extended version).
    15 *}
    16 
    17 
    18 subsection {* Definitions and lemmas *}
    19 
    20 consts
    21   RsetR :: "int => int set set"
    22   BnorRset :: "int * int => int set"
    23   norRRset :: "int => int set"
    24   noXRRset :: "int => int => int set"
    25   phi :: "int => nat"
    26   is_RRset :: "int set => int => bool"
    27   RRset2norRR :: "int set => int => int => int"
    28 
    29 inductive "RsetR m"
    30   intros
    31     empty [simp]: "{} \<in> RsetR m"
    32     insert: "A \<in> RsetR m ==> zgcd (a, m) = 1 ==>
    33       \<forall>a'. a' \<in> A --> \<not> zcong a a' m ==> insert a A \<in> RsetR m"
    34 
    35 recdef BnorRset
    36   "measure ((\<lambda>(a, m). nat a) :: int * int => nat)"
    37   "BnorRset (a, m) =
    38    (if 0 < a then
    39     let na = BnorRset (a - 1, m)
    40     in (if zgcd (a, m) = 1 then insert a na else na)
    41     else {})"
    42 
    43 defs
    44   norRRset_def: "norRRset m == BnorRset (m - 1, m)"
    45   noXRRset_def: "noXRRset m x == (\<lambda>a. a * x) ` norRRset m"
    46   phi_def: "phi m == card (norRRset m)"
    47   is_RRset_def: "is_RRset A m == A \<in> RsetR m \<and> card A = phi m"
    48   RRset2norRR_def:
    49     "RRset2norRR A m a ==
    50      (if 1 < m \<and> is_RRset A m \<and> a \<in> A then
    51         SOME b. zcong a b m \<and> b \<in> norRRset m
    52       else 0)"
    53 
    54 constdefs
    55   zcongm :: "int => int => int => bool"
    56   "zcongm m == \<lambda>a b. zcong a b m"
    57 
    58 lemma abs_eq_1_iff [iff]: "(abs z = (1::int)) = (z = 1 \<or> z = -1)"
    59   -- {* LCP: not sure why this lemma is needed now *}
    60   apply (auto simp add: zabs_def)
    61   done
    62 
    63 
    64 text {* \medskip @{text norRRset} *}
    65 
    66 declare BnorRset.simps [simp del]
    67 
    68 lemma BnorRset_induct:
    69   "(!!a m. P {} a m) ==>
    70     (!!a m. 0 < (a::int) ==> P (BnorRset (a - 1, m::int)) (a - 1) m
    71       ==> P (BnorRset(a,m)) a m)
    72     ==> P (BnorRset(u,v)) u v"
    73 proof -
    74   case rule_context
    75   show ?thesis
    76     apply (rule BnorRset.induct)
    77     apply safe
    78      apply (case_tac [2] "0 < a")
    79       apply (rule_tac [2] rule_context)
    80        apply simp_all
    81      apply (simp_all add: BnorRset.simps rule_context)
    82   done
    83 qed
    84 
    85 lemma Bnor_mem_zle [rule_format]: "b \<in> BnorRset (a, m) --> b \<le> a"
    86   apply (induct a m rule: BnorRset_induct)
    87    prefer 2
    88    apply (subst BnorRset.simps)
    89    apply (unfold Let_def)
    90    apply auto
    91   done
    92 
    93 lemma Bnor_mem_zle_swap: "a < b ==> b \<notin> BnorRset (a, m)"
    94   apply (auto dest: Bnor_mem_zle)
    95   done
    96 
    97 lemma Bnor_mem_zg [rule_format]: "b \<in> BnorRset (a, m) --> 0 < b"
    98   apply (induct a m rule: BnorRset_induct)
    99    prefer 2
   100    apply (subst BnorRset.simps)
   101    apply (unfold Let_def)
   102    apply auto
   103   done
   104 
   105 lemma Bnor_mem_if [rule_format]:
   106     "zgcd (b, m) = 1 --> 0 < b --> b \<le> a --> b \<in> BnorRset (a, m)"
   107   apply (induct a m rule: BnorRset.induct)
   108   apply auto
   109    apply (case_tac "a = b")
   110     prefer 2
   111     apply (simp add: order_less_le)
   112    apply (simp (no_asm_simp))
   113    prefer 2
   114    apply (subst BnorRset.simps)
   115    defer
   116    apply (subst BnorRset.simps)
   117    apply (unfold Let_def)
   118    apply auto
   119   done
   120 
   121 lemma Bnor_in_RsetR [rule_format]: "a < m --> BnorRset (a, m) \<in> RsetR m"
   122   apply (induct a m rule: BnorRset_induct)
   123    apply simp
   124   apply (subst BnorRset.simps)
   125   apply (unfold Let_def)
   126   apply auto
   127   apply (rule RsetR.insert)
   128     apply (rule_tac [3] allI)
   129     apply (rule_tac [3] impI)
   130     apply (rule_tac [3] zcong_not)
   131        apply (subgoal_tac [6] "a' \<le> a - 1")
   132         apply (rule_tac [7] Bnor_mem_zle)
   133         apply (rule_tac [5] Bnor_mem_zg)
   134         apply auto
   135   done
   136 
   137 lemma Bnor_fin: "finite (BnorRset (a, m))"
   138   apply (induct a m rule: BnorRset_induct)
   139    prefer 2
   140    apply (subst BnorRset.simps)
   141    apply (unfold Let_def)
   142    apply auto
   143   done
   144 
   145 lemma norR_mem_unique_aux: "a \<le> b - 1 ==> a < (b::int)"
   146   apply auto
   147   done
   148 
   149 lemma norR_mem_unique:
   150   "1 < m ==>
   151     zgcd (a, m) = 1 ==> \<exists>!b. [a = b] (mod m) \<and> b \<in> norRRset m"
   152   apply (unfold norRRset_def)
   153   apply (cut_tac a = a and m = m in zcong_zless_unique)
   154    apply auto
   155    apply (rule_tac [2] m = m in zcong_zless_imp_eq)
   156        apply (auto intro: Bnor_mem_zle Bnor_mem_zg zcong_trans
   157 	 order_less_imp_le norR_mem_unique_aux simp add: zcong_sym)
   158   apply (rule_tac "x" = "b" in exI)
   159   apply safe
   160   apply (rule Bnor_mem_if)
   161     apply (case_tac [2] "b = 0")
   162      apply (auto intro: order_less_le [THEN iffD2])
   163    prefer 2
   164    apply (simp only: zcong_def)
   165    apply (subgoal_tac "zgcd (a, m) = m")
   166     prefer 2
   167     apply (subst zdvd_iff_zgcd [symmetric])
   168      apply (rule_tac [4] zgcd_zcong_zgcd)
   169        apply (simp_all add: zdvd_zminus_iff zcong_sym)
   170   done
   171 
   172 
   173 text {* \medskip @{term noXRRset} *}
   174 
   175 lemma RRset_gcd [rule_format]:
   176     "is_RRset A m ==> a \<in> A --> zgcd (a, m) = 1"
   177   apply (unfold is_RRset_def)
   178   apply (rule RsetR.induct)
   179     apply auto
   180   done
   181 
   182 lemma RsetR_zmult_mono:
   183   "A \<in> RsetR m ==>
   184     0 < m ==> zgcd (x, m) = 1 ==> (\<lambda>a. a * x) ` A \<in> RsetR m"
   185   apply (erule RsetR.induct)
   186    apply simp_all
   187   apply (rule RsetR.insert)
   188     apply auto
   189    apply (blast intro: zgcd_zgcd_zmult)
   190   apply (simp add: zcong_cancel)
   191   done
   192 
   193 lemma card_nor_eq_noX:
   194   "0 < m ==>
   195     zgcd (x, m) = 1 ==> card (noXRRset m x) = card (norRRset m)"
   196   apply (unfold norRRset_def noXRRset_def)
   197   apply (rule card_image)
   198    apply (auto simp add: inj_on_def Bnor_fin)
   199   apply (simp add: BnorRset.simps)
   200   done
   201 
   202 lemma noX_is_RRset:
   203     "0 < m ==> zgcd (x, m) = 1 ==> is_RRset (noXRRset m x) m"
   204   apply (unfold is_RRset_def phi_def)
   205   apply (auto simp add: card_nor_eq_noX)
   206   apply (unfold noXRRset_def norRRset_def)
   207   apply (rule RsetR_zmult_mono)
   208     apply (rule Bnor_in_RsetR)
   209     apply simp_all
   210   done
   211 
   212 lemma aux_some:
   213   "1 < m ==> is_RRset A m ==> a \<in> A
   214     ==> zcong a (SOME b. [a = b] (mod m) \<and> b \<in> norRRset m) m \<and>
   215       (SOME b. [a = b] (mod m) \<and> b \<in> norRRset m) \<in> norRRset m"
   216   apply (rule norR_mem_unique [THEN ex1_implies_ex, THEN someI_ex])
   217    apply (rule_tac [2] RRset_gcd)
   218     apply simp_all
   219   done
   220 
   221 lemma RRset2norRR_correct:
   222   "1 < m ==> is_RRset A m ==> a \<in> A ==>
   223     [a = RRset2norRR A m a] (mod m) \<and> RRset2norRR A m a \<in> norRRset m"
   224   apply (unfold RRset2norRR_def)
   225   apply simp
   226   apply (rule aux_some)
   227     apply simp_all
   228   done
   229 
   230 lemmas RRset2norRR_correct1 =
   231   RRset2norRR_correct [THEN conjunct1, standard]
   232 lemmas RRset2norRR_correct2 =
   233   RRset2norRR_correct [THEN conjunct2, standard]
   234 
   235 lemma RsetR_fin: "A \<in> RsetR m ==> finite A"
   236   apply (erule RsetR.induct)
   237    apply auto
   238   done
   239 
   240 lemma RRset_zcong_eq [rule_format]:
   241   "1 < m ==>
   242     is_RRset A m ==> [a = b] (mod m) ==> a \<in> A --> b \<in> A --> a = b"
   243   apply (unfold is_RRset_def)
   244   apply (rule RsetR.induct)
   245     apply (auto simp add: zcong_sym)
   246   done
   247 
   248 lemma aux:
   249   "P (SOME a. P a) ==> Q (SOME a. Q a) ==>
   250     (SOME a. P a) = (SOME a. Q a) ==> \<exists>a. P a \<and> Q a"
   251   apply auto
   252   done
   253 
   254 lemma RRset2norRR_inj:
   255     "1 < m ==> is_RRset A m ==> inj_on (RRset2norRR A m) A"
   256   apply (unfold RRset2norRR_def inj_on_def)
   257   apply auto
   258   apply (subgoal_tac "\<exists>b. ([x = b] (mod m) \<and> b \<in> norRRset m) \<and>
   259       ([y = b] (mod m) \<and> b \<in> norRRset m)")
   260    apply (rule_tac [2] aux)
   261      apply (rule_tac [3] aux_some)
   262        apply (rule_tac [2] aux_some)
   263          apply (rule RRset_zcong_eq)
   264              apply auto
   265   apply (rule_tac b = b in zcong_trans)
   266    apply (simp_all add: zcong_sym)
   267   done
   268 
   269 lemma RRset2norRR_eq_norR:
   270     "1 < m ==> is_RRset A m ==> RRset2norRR A m ` A = norRRset m"
   271   apply (rule card_seteq)
   272     prefer 3
   273     apply (subst card_image)
   274       apply (rule_tac [2] RRset2norRR_inj)
   275        apply auto
   276      apply (rule_tac [4] RRset2norRR_correct2)
   277        apply auto
   278     apply (unfold is_RRset_def phi_def norRRset_def)
   279     apply (auto simp add: RsetR_fin Bnor_fin)
   280   done
   281 
   282 
   283 lemma Bnor_prod_power_aux: "a \<notin> A ==> inj f ==> f a \<notin> f ` A"
   284   apply (unfold inj_on_def)
   285   apply auto
   286   done
   287 
   288 lemma Bnor_prod_power [rule_format]:
   289   "x \<noteq> 0 ==> a < m --> setprod ((\<lambda>a. a * x) ` BnorRset (a, m)) =
   290       setprod (BnorRset(a, m)) * x^card (BnorRset (a, m))"
   291   apply (induct a m rule: BnorRset_induct)
   292    prefer 2
   293    apply (subst BnorRset.simps)
   294    apply (unfold Let_def)
   295    apply auto
   296   apply (simp add: Bnor_fin Bnor_mem_zle_swap)
   297   apply (subst setprod_insert)
   298     apply (rule_tac [2] Bnor_prod_power_aux)
   299      apply (unfold inj_on_def)
   300      apply (simp_all add: zmult_ac Bnor_fin finite_imageI
   301        Bnor_mem_zle_swap)
   302   done
   303 
   304 
   305 subsection {* Fermat *}
   306 
   307 lemma bijzcong_zcong_prod:
   308     "(A, B) \<in> bijR (zcongm m) ==> [setprod A = setprod B] (mod m)"
   309   apply (unfold zcongm_def)
   310   apply (erule bijR.induct)
   311    apply (subgoal_tac [2] "a \<notin> A \<and> b \<notin> B \<and> finite A \<and> finite B")
   312     apply (auto intro: fin_bijRl fin_bijRr zcong_zmult)
   313   done
   314 
   315 lemma Bnor_prod_zgcd [rule_format]:
   316     "a < m --> zgcd (setprod (BnorRset (a, m)), m) = 1"
   317   apply (induct a m rule: BnorRset_induct)
   318    prefer 2
   319    apply (subst BnorRset.simps)
   320    apply (unfold Let_def)
   321    apply auto
   322   apply (simp add: Bnor_fin Bnor_mem_zle_swap)
   323   apply (blast intro: zgcd_zgcd_zmult)
   324   done
   325 
   326 theorem Euler_Fermat:
   327     "0 < m ==> zgcd (x, m) = 1 ==> [x^(phi m) = 1] (mod m)"
   328   apply (unfold norRRset_def phi_def)
   329   apply (case_tac "x = 0")
   330    apply (case_tac [2] "m = 1")
   331     apply (rule_tac [3] iffD1)
   332      apply (rule_tac [3] k = "setprod (BnorRset (m - 1, m))"
   333        in zcong_cancel2)
   334       prefer 5
   335       apply (subst Bnor_prod_power [symmetric])
   336         apply (rule_tac [7] Bnor_prod_zgcd)
   337         apply simp_all
   338   apply (rule bijzcong_zcong_prod)
   339   apply (fold norRRset_def noXRRset_def)
   340   apply (subst RRset2norRR_eq_norR [symmetric])
   341     apply (rule_tac [3] inj_func_bijR)
   342       apply auto
   343      apply (unfold zcongm_def)
   344      apply (rule_tac [2] RRset2norRR_correct1)
   345        apply (rule_tac [5] RRset2norRR_inj)
   346         apply (auto intro: order_less_le [THEN iffD2]
   347 	   simp add: noX_is_RRset)
   348   apply (unfold noXRRset_def norRRset_def)
   349   apply (rule finite_imageI)
   350   apply (rule Bnor_fin)
   351   done
   352 
   353 lemma Bnor_prime [rule_format (no_asm)]:
   354   "p \<in> zprime ==>
   355     a < p --> (\<forall>b. 0 < b \<and> b \<le> a --> zgcd (b, p) = 1)
   356     --> card (BnorRset (a, p)) = nat a"
   357   apply (unfold zprime_def)
   358   apply (induct a p rule: BnorRset.induct)
   359   apply (subst BnorRset.simps)
   360   apply (unfold Let_def)
   361   apply auto
   362   done
   363 
   364 lemma phi_prime: "p \<in> zprime ==> phi p = nat (p - 1)"
   365   apply (unfold phi_def norRRset_def)
   366   apply (rule Bnor_prime)
   367     apply auto
   368   apply (erule zless_zprime_imp_zrelprime)
   369    apply simp_all
   370   done
   371 
   372 theorem Little_Fermat:
   373     "p \<in> zprime ==> \<not> p dvd x ==> [x^(nat (p - 1)) = 1] (mod p)"
   374   apply (subst phi_prime [symmetric])
   375    apply (rule_tac [2] Euler_Fermat)
   376     apply (erule_tac [3] zprime_imp_zrelprime)
   377     apply (unfold zprime_def)
   378     apply auto
   379   done
   380 
   381 end