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
```