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