src/HOL/Old_Number_Theory/EulerFermat.thy
author huffman
Sun Nov 13 19:26:53 2011 +0100 (2011-11-13)
changeset 45480 a39bb6d42ace
parent 44766 d4d33a4d7548
child 45605 a89b4bc311a5
permissions -rw-r--r--
remove unnecessary number-representation-specific rules from metis calls;
speed up another proof
     1 (*  Title:      HOL/Old_Number_Theory/EulerFermat.thy
     2     Author:     Thomas M. Rasmussen
     3     Copyright   2000  University of Cambridge
     4 *)
     5 
     6 header {* 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 [where P="%A. a \<in> A --> zgcd a m = 1"], 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 =
   200   RRset2norRR_correct [THEN conjunct1, standard]
   201 lemmas RRset2norRR_correct2 =
   202   RRset2norRR_correct [THEN conjunct2, standard]
   203 
   204 lemma RsetR_fin: "A \<in> RsetR m ==> finite A"
   205   by (induct set: RsetR) auto
   206 
   207 lemma RRset_zcong_eq [rule_format]:
   208   "1 < m ==>
   209     is_RRset A m ==> [a = b] (mod m) ==> a \<in> A --> b \<in> A --> a = b"
   210   apply (unfold is_RRset_def)
   211   apply (rule RsetR.induct [where P="%A. a \<in> A --> b \<in> A --> a = b"])
   212     apply (auto simp add: zcong_sym)
   213   done
   214 
   215 lemma aux:
   216   "P (SOME a. P a) ==> Q (SOME a. Q a) ==>
   217     (SOME a. P a) = (SOME a. Q a) ==> \<exists>a. P a \<and> Q a"
   218   apply auto
   219   done
   220 
   221 lemma RRset2norRR_inj:
   222     "1 < m ==> is_RRset A m ==> inj_on (RRset2norRR A m) A"
   223   apply (unfold RRset2norRR_def inj_on_def, auto)
   224   apply (subgoal_tac "\<exists>b. ([x = b] (mod m) \<and> b \<in> norRRset m) \<and>
   225       ([y = b] (mod m) \<and> b \<in> norRRset m)")
   226    apply (rule_tac [2] aux)
   227      apply (rule_tac [3] aux_some)
   228        apply (rule_tac [2] aux_some)
   229          apply (rule RRset_zcong_eq, auto)
   230   apply (rule_tac b = b in zcong_trans)
   231    apply (simp_all add: zcong_sym)
   232   done
   233 
   234 lemma RRset2norRR_eq_norR:
   235     "1 < m ==> is_RRset A m ==> RRset2norRR A m ` A = norRRset m"
   236   apply (rule card_seteq)
   237     prefer 3
   238     apply (subst card_image)
   239       apply (rule_tac RRset2norRR_inj, auto)
   240      apply (rule_tac [3] RRset2norRR_correct2, auto)
   241     apply (unfold is_RRset_def phi_def norRRset_def)
   242     apply (auto simp add: Bnor_fin)
   243   done
   244 
   245 
   246 lemma Bnor_prod_power_aux: "a \<notin> A ==> inj f ==> f a \<notin> f ` A"
   247 by (unfold inj_on_def, auto)
   248 
   249 lemma Bnor_prod_power [rule_format]:
   250   "x \<noteq> 0 ==> a < m --> \<Prod>((\<lambda>a. a * x) ` BnorRset a m) =
   251       \<Prod>(BnorRset a m) * x^card (BnorRset a m)"
   252   apply (induct a m rule: BnorRset_induct)
   253    prefer 2
   254    apply (simplesubst BnorRset.simps)  --{*multiple redexes*}
   255    apply (unfold Let_def, auto)
   256   apply (simp add: Bnor_fin Bnor_mem_zle_swap)
   257   apply (subst setprod_insert)
   258     apply (rule_tac [2] Bnor_prod_power_aux)
   259      apply (unfold inj_on_def)
   260      apply (simp_all add: mult_ac Bnor_fin Bnor_mem_zle_swap)
   261   done
   262 
   263 
   264 subsection {* Fermat *}
   265 
   266 lemma bijzcong_zcong_prod:
   267     "(A, B) \<in> bijR (zcongm m) ==> [\<Prod>A = \<Prod>B] (mod m)"
   268   apply (unfold zcongm_def)
   269   apply (erule bijR.induct)
   270    apply (subgoal_tac [2] "a \<notin> A \<and> b \<notin> B \<and> finite A \<and> finite B")
   271     apply (auto intro: fin_bijRl fin_bijRr zcong_zmult)
   272   done
   273 
   274 lemma Bnor_prod_zgcd [rule_format]:
   275     "a < m --> zgcd (\<Prod>(BnorRset a m)) m = 1"
   276   apply (induct a m rule: BnorRset_induct)
   277    prefer 2
   278    apply (subst BnorRset.simps)
   279    apply (unfold Let_def, auto)
   280   apply (simp add: Bnor_fin Bnor_mem_zle_swap)
   281   apply (blast intro: zgcd_zgcd_zmult)
   282   done
   283 
   284 theorem Euler_Fermat:
   285     "0 < m ==> zgcd x m = 1 ==> [x^(phi m) = 1] (mod m)"
   286   apply (unfold norRRset_def phi_def)
   287   apply (case_tac "x = 0")
   288    apply (case_tac [2] "m = 1")
   289     apply (rule_tac [3] iffD1)
   290      apply (rule_tac [3] k = "\<Prod>(BnorRset (m - 1) m)"
   291        in zcong_cancel2)
   292       prefer 5
   293       apply (subst Bnor_prod_power [symmetric])
   294         apply (rule_tac [7] Bnor_prod_zgcd, simp_all)
   295   apply (rule bijzcong_zcong_prod)
   296   apply (fold norRRset_def, fold noXRRset_def)
   297   apply (subst RRset2norRR_eq_norR [symmetric])
   298     apply (rule_tac [3] inj_func_bijR, auto)
   299      apply (unfold zcongm_def)
   300      apply (rule_tac [2] RRset2norRR_correct1)
   301        apply (rule_tac [5] RRset2norRR_inj)
   302         apply (auto intro: order_less_le [THEN iffD2]
   303            simp add: noX_is_RRset)
   304   apply (unfold noXRRset_def norRRset_def)
   305   apply (rule finite_imageI)
   306   apply (rule Bnor_fin)
   307   done
   308 
   309 lemma Bnor_prime:
   310   "\<lbrakk> zprime p; a < p \<rbrakk> \<Longrightarrow> card (BnorRset a p) = nat a"
   311   apply (induct a p rule: BnorRset.induct)
   312   apply (subst BnorRset.simps)
   313   apply (unfold Let_def, auto simp add:zless_zprime_imp_zrelprime)
   314   apply (subgoal_tac "finite (BnorRset (a - 1) m)")
   315    apply (subgoal_tac "a ~: BnorRset (a - 1) m")
   316     apply (auto simp add: card_insert_disjoint Suc_nat_eq_nat_zadd1)
   317    apply (frule Bnor_mem_zle, arith)
   318   apply (frule Bnor_fin)
   319   done
   320 
   321 lemma phi_prime: "zprime p ==> phi p = nat (p - 1)"
   322   apply (unfold phi_def norRRset_def)
   323   apply (rule Bnor_prime, auto)
   324   done
   325 
   326 theorem Little_Fermat:
   327     "zprime p ==> \<not> p dvd x ==> [x^(nat (p - 1)) = 1] (mod p)"
   328   apply (subst phi_prime [symmetric])
   329    apply (rule_tac [2] Euler_Fermat)
   330     apply (erule_tac [3] zprime_imp_zrelprime)
   331     apply (unfold zprime_def, auto)
   332   done
   333 
   334 end