src/HOL/Old_Number_Theory/EulerFermat.thy
author haftmann
Fri Nov 27 08:41:10 2009 +0100 (2009-11-27)
changeset 33963 977b94b64905
parent 32960 69916a850301
child 35440 bdf8ad377877
permissions -rw-r--r--
renamed former datatype.ML to datatype_data.ML; datatype.ML provides uniform view on datatype.ML and datatype_rep_proofs.ML
     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