src/HOL/NumberTheory/EulerFermat.thy
author obua
Mon Apr 10 16:00:34 2006 +0200 (2006-04-10)
changeset 19404 9bf2cdc9e8e8
parent 18369 694ea14ab4f2
child 19670 2e4a143c73c5
permissions -rw-r--r--
Moved stuff from Ring_and_Field to Matrix
     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 imports BijectionRel IntFact begin
    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   by (auto simp add: abs_if)
    61 
    62 
    63 text {* \medskip @{text norRRset} *}
    64 
    65 declare BnorRset.simps [simp del]
    66 
    67 lemma BnorRset_induct:
    68   assumes "!!a m. P {} a m"
    69     and "!!a m. 0 < (a::int) ==> P (BnorRset (a - 1, m::int)) (a - 1) m
    70       ==> P (BnorRset(a,m)) a m"
    71   shows "P (BnorRset(u,v)) u v"
    72   apply (rule BnorRset.induct)
    73   apply safe
    74    apply (case_tac [2] "0 < a")
    75     apply (rule_tac [2] prems)
    76      apply simp_all
    77    apply (simp_all add: BnorRset.simps prems)
    78   done
    79 
    80 lemma Bnor_mem_zle [rule_format]: "b \<in> BnorRset (a, m) \<longrightarrow> b \<le> a"
    81   apply (induct a m rule: BnorRset_induct)
    82    apply simp
    83   apply (subst BnorRset.simps)
    84    apply (unfold Let_def, auto)
    85   done
    86 
    87 lemma Bnor_mem_zle_swap: "a < b ==> b \<notin> BnorRset (a, m)"
    88   by (auto dest: Bnor_mem_zle)
    89 
    90 lemma Bnor_mem_zg [rule_format]: "b \<in> BnorRset (a, m) --> 0 < b"
    91   apply (induct a m rule: BnorRset_induct)
    92    prefer 2
    93    apply (subst BnorRset.simps)
    94    apply (unfold Let_def, auto)
    95   done
    96 
    97 lemma Bnor_mem_if [rule_format]:
    98     "zgcd (b, m) = 1 --> 0 < b --> b \<le> a --> b \<in> BnorRset (a, m)"
    99   apply (induct a m rule: BnorRset.induct, auto)
   100    apply (subst BnorRset.simps)
   101    defer
   102    apply (subst BnorRset.simps)
   103    apply (unfold Let_def, auto)
   104   done
   105 
   106 lemma Bnor_in_RsetR [rule_format]: "a < m --> BnorRset (a, m) \<in> RsetR m"
   107   apply (induct a m rule: BnorRset_induct, simp)
   108   apply (subst BnorRset.simps)
   109   apply (unfold Let_def, auto)
   110   apply (rule RsetR.insert)
   111     apply (rule_tac [3] allI)
   112     apply (rule_tac [3] impI)
   113     apply (rule_tac [3] zcong_not)
   114        apply (subgoal_tac [6] "a' \<le> a - 1")
   115         apply (rule_tac [7] Bnor_mem_zle)
   116         apply (rule_tac [5] Bnor_mem_zg, auto)
   117   done
   118 
   119 lemma Bnor_fin: "finite (BnorRset (a, m))"
   120   apply (induct a m rule: BnorRset_induct)
   121    prefer 2
   122    apply (subst BnorRset.simps)
   123    apply (unfold Let_def, auto)
   124   done
   125 
   126 lemma norR_mem_unique_aux: "a \<le> b - 1 ==> a < (b::int)"
   127   apply auto
   128   done
   129 
   130 lemma norR_mem_unique:
   131   "1 < m ==>
   132     zgcd (a, m) = 1 ==> \<exists>!b. [a = b] (mod m) \<and> b \<in> norRRset m"
   133   apply (unfold norRRset_def)
   134   apply (cut_tac a = a and m = m in zcong_zless_unique, auto)
   135    apply (rule_tac [2] m = m in zcong_zless_imp_eq)
   136        apply (auto intro: Bnor_mem_zle Bnor_mem_zg zcong_trans
   137 	 order_less_imp_le norR_mem_unique_aux simp add: zcong_sym)
   138   apply (rule_tac x = b in exI, safe)
   139   apply (rule Bnor_mem_if)
   140     apply (case_tac [2] "b = 0")
   141      apply (auto intro: order_less_le [THEN iffD2])
   142    prefer 2
   143    apply (simp only: zcong_def)
   144    apply (subgoal_tac "zgcd (a, m) = m")
   145     prefer 2
   146     apply (subst zdvd_iff_zgcd [symmetric])
   147      apply (rule_tac [4] zgcd_zcong_zgcd)
   148        apply (simp_all add: zdvd_zminus_iff zcong_sym)
   149   done
   150 
   151 
   152 text {* \medskip @{term noXRRset} *}
   153 
   154 lemma RRset_gcd [rule_format]:
   155     "is_RRset A m ==> a \<in> A --> zgcd (a, m) = 1"
   156   apply (unfold is_RRset_def)
   157   apply (rule RsetR.induct, auto)
   158   done
   159 
   160 lemma RsetR_zmult_mono:
   161   "A \<in> RsetR m ==>
   162     0 < m ==> zgcd (x, m) = 1 ==> (\<lambda>a. a * x) ` A \<in> RsetR m"
   163   apply (erule RsetR.induct, simp_all)
   164   apply (rule RsetR.insert, auto)
   165    apply (blast intro: zgcd_zgcd_zmult)
   166   apply (simp add: zcong_cancel)
   167   done
   168 
   169 lemma card_nor_eq_noX:
   170   "0 < m ==>
   171     zgcd (x, m) = 1 ==> card (noXRRset m x) = card (norRRset m)"
   172   apply (unfold norRRset_def noXRRset_def)
   173   apply (rule card_image)
   174    apply (auto simp add: inj_on_def Bnor_fin)
   175   apply (simp add: BnorRset.simps)
   176   done
   177 
   178 lemma noX_is_RRset:
   179     "0 < m ==> zgcd (x, m) = 1 ==> is_RRset (noXRRset m x) m"
   180   apply (unfold is_RRset_def phi_def)
   181   apply (auto simp add: card_nor_eq_noX)
   182   apply (unfold noXRRset_def norRRset_def)
   183   apply (rule RsetR_zmult_mono)
   184     apply (rule Bnor_in_RsetR, simp_all)
   185   done
   186 
   187 lemma aux_some:
   188   "1 < m ==> is_RRset A m ==> a \<in> A
   189     ==> zcong a (SOME b. [a = b] (mod m) \<and> b \<in> norRRset m) m \<and>
   190       (SOME b. [a = b] (mod m) \<and> b \<in> norRRset m) \<in> norRRset m"
   191   apply (rule norR_mem_unique [THEN ex1_implies_ex, THEN someI_ex])
   192    apply (rule_tac [2] RRset_gcd, simp_all)
   193   done
   194 
   195 lemma RRset2norRR_correct:
   196   "1 < m ==> is_RRset A m ==> a \<in> A ==>
   197     [a = RRset2norRR A m a] (mod m) \<and> RRset2norRR A m a \<in> norRRset m"
   198   apply (unfold RRset2norRR_def, simp)
   199   apply (rule aux_some, simp_all)
   200   done
   201 
   202 lemmas RRset2norRR_correct1 =
   203   RRset2norRR_correct [THEN conjunct1, standard]
   204 lemmas RRset2norRR_correct2 =
   205   RRset2norRR_correct [THEN conjunct2, standard]
   206 
   207 lemma RsetR_fin: "A \<in> RsetR m ==> finite A"
   208   by (induct set: RsetR) auto
   209 
   210 lemma RRset_zcong_eq [rule_format]:
   211   "1 < m ==>
   212     is_RRset A m ==> [a = b] (mod m) ==> a \<in> A --> b \<in> A --> a = b"
   213   apply (unfold is_RRset_def)
   214   apply (rule RsetR.induct)
   215     apply (auto simp add: zcong_sym)
   216   done
   217 
   218 lemma aux:
   219   "P (SOME a. P a) ==> Q (SOME a. Q a) ==>
   220     (SOME a. P a) = (SOME a. Q a) ==> \<exists>a. P a \<and> Q a"
   221   apply auto
   222   done
   223 
   224 lemma RRset2norRR_inj:
   225     "1 < m ==> is_RRset A m ==> inj_on (RRset2norRR A m) A"
   226   apply (unfold RRset2norRR_def inj_on_def, auto)
   227   apply (subgoal_tac "\<exists>b. ([x = b] (mod m) \<and> b \<in> norRRset m) \<and>
   228       ([y = b] (mod m) \<and> b \<in> norRRset m)")
   229    apply (rule_tac [2] aux)
   230      apply (rule_tac [3] aux_some)
   231        apply (rule_tac [2] aux_some)
   232          apply (rule RRset_zcong_eq, auto)
   233   apply (rule_tac b = b in zcong_trans)
   234    apply (simp_all add: zcong_sym)
   235   done
   236 
   237 lemma RRset2norRR_eq_norR:
   238     "1 < m ==> is_RRset A m ==> RRset2norRR A m ` A = norRRset m"
   239   apply (rule card_seteq)
   240     prefer 3
   241     apply (subst card_image)
   242       apply (rule_tac RRset2norRR_inj, auto)
   243      apply (rule_tac [3] RRset2norRR_correct2, auto)
   244     apply (unfold is_RRset_def phi_def norRRset_def)
   245     apply (auto simp add: Bnor_fin)
   246   done
   247 
   248 
   249 lemma Bnor_prod_power_aux: "a \<notin> A ==> inj f ==> f a \<notin> f ` A"
   250 by (unfold inj_on_def, auto)
   251 
   252 lemma Bnor_prod_power [rule_format]:
   253   "x \<noteq> 0 ==> a < m --> \<Prod>((\<lambda>a. a * x) ` BnorRset (a, m)) =
   254       \<Prod>(BnorRset(a, m)) * x^card (BnorRset (a, m))"
   255   apply (induct a m rule: BnorRset_induct)
   256    prefer 2
   257    apply (simplesubst BnorRset.simps)  --{*multiple redexes*}
   258    apply (unfold Let_def, auto)
   259   apply (simp add: Bnor_fin Bnor_mem_zle_swap)
   260   apply (subst setprod_insert)
   261     apply (rule_tac [2] Bnor_prod_power_aux)
   262      apply (unfold inj_on_def)
   263      apply (simp_all add: zmult_ac Bnor_fin finite_imageI
   264        Bnor_mem_zle_swap)
   265   done
   266 
   267 
   268 subsection {* Fermat *}
   269 
   270 lemma bijzcong_zcong_prod:
   271     "(A, B) \<in> bijR (zcongm m) ==> [\<Prod>A = \<Prod>B] (mod m)"
   272   apply (unfold zcongm_def)
   273   apply (erule bijR.induct)
   274    apply (subgoal_tac [2] "a \<notin> A \<and> b \<notin> B \<and> finite A \<and> finite B")
   275     apply (auto intro: fin_bijRl fin_bijRr zcong_zmult)
   276   done
   277 
   278 lemma Bnor_prod_zgcd [rule_format]:
   279     "a < m --> zgcd (\<Prod>(BnorRset(a, m)), m) = 1"
   280   apply (induct a m rule: BnorRset_induct)
   281    prefer 2
   282    apply (subst BnorRset.simps)
   283    apply (unfold Let_def, auto)
   284   apply (simp add: Bnor_fin Bnor_mem_zle_swap)
   285   apply (blast intro: zgcd_zgcd_zmult)
   286   done
   287 
   288 theorem Euler_Fermat:
   289     "0 < m ==> zgcd (x, m) = 1 ==> [x^(phi m) = 1] (mod m)"
   290   apply (unfold norRRset_def phi_def)
   291   apply (case_tac "x = 0")
   292    apply (case_tac [2] "m = 1")
   293     apply (rule_tac [3] iffD1)
   294      apply (rule_tac [3] k = "\<Prod>(BnorRset(m - 1, m))"
   295        in zcong_cancel2)
   296       prefer 5
   297       apply (subst Bnor_prod_power [symmetric])
   298         apply (rule_tac [7] Bnor_prod_zgcd, simp_all)
   299   apply (rule bijzcong_zcong_prod)
   300   apply (fold norRRset_def noXRRset_def)
   301   apply (subst RRset2norRR_eq_norR [symmetric])
   302     apply (rule_tac [3] inj_func_bijR, auto)
   303      apply (unfold zcongm_def)
   304      apply (rule_tac [2] RRset2norRR_correct1)
   305        apply (rule_tac [5] RRset2norRR_inj)
   306         apply (auto intro: order_less_le [THEN iffD2]
   307 	   simp add: noX_is_RRset)
   308   apply (unfold noXRRset_def norRRset_def)
   309   apply (rule finite_imageI)
   310   apply (rule Bnor_fin)
   311   done
   312 
   313 lemma Bnor_prime:
   314   "\<lbrakk> zprime p; a < p \<rbrakk> \<Longrightarrow> card (BnorRset (a, p)) = nat a"
   315   apply (induct a p rule: BnorRset.induct)
   316   apply (subst BnorRset.simps)
   317   apply (unfold Let_def, auto simp add:zless_zprime_imp_zrelprime)
   318   apply (subgoal_tac "finite (BnorRset (a - 1,m))")
   319    apply (subgoal_tac "a ~: BnorRset (a - 1,m)")
   320     apply (auto simp add: card_insert_disjoint Suc_nat_eq_nat_zadd1)
   321    apply (frule Bnor_mem_zle, arith)
   322   apply (frule Bnor_fin)
   323   done
   324 
   325 lemma phi_prime: "zprime p ==> phi p = nat (p - 1)"
   326   apply (unfold phi_def norRRset_def)
   327   apply (rule Bnor_prime, auto)
   328   done
   329 
   330 theorem Little_Fermat:
   331     "zprime p ==> \<not> p dvd x ==> [x^(nat (p - 1)) = 1] (mod p)"
   332   apply (subst phi_prime [symmetric])
   333    apply (rule_tac [2] Euler_Fermat)
   334     apply (erule_tac [3] zprime_imp_zrelprime)
   335     apply (unfold zprime_def, auto)
   336   done
   337 
   338 end