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