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