src/HOL/Old_Number_Theory/EulerFermat.thy
changeset 32479 521cc9bf2958
parent 30042 31039ee583fa
child 32960 69916a850301
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Old_Number_Theory/EulerFermat.thy	Tue Sep 01 15:39:33 2009 +0200
     1.3 @@ -0,0 +1,346 @@
     1.4 +(*  Author:     Thomas M. Rasmussen
     1.5 +    Copyright   2000  University of Cambridge
     1.6 +*)
     1.7 +
     1.8 +header {* Fermat's Little Theorem extended to Euler's Totient function *}
     1.9 +
    1.10 +theory EulerFermat
    1.11 +imports BijectionRel IntFact
    1.12 +begin
    1.13 +
    1.14 +text {*
    1.15 +  Fermat's Little Theorem extended to Euler's Totient function. More
    1.16 +  abstract approach than Boyer-Moore (which seems necessary to achieve
    1.17 +  the extended version).
    1.18 +*}
    1.19 +
    1.20 +
    1.21 +subsection {* Definitions and lemmas *}
    1.22 +
    1.23 +inductive_set
    1.24 +  RsetR :: "int => int set set"
    1.25 +  for m :: int
    1.26 +  where
    1.27 +    empty [simp]: "{} \<in> RsetR m"
    1.28 +  | insert: "A \<in> RsetR m ==> zgcd a m = 1 ==>
    1.29 +      \<forall>a'. a' \<in> A --> \<not> zcong a a' m ==> insert a A \<in> RsetR m"
    1.30 +
    1.31 +consts
    1.32 +  BnorRset :: "int * int => int set"
    1.33 +
    1.34 +recdef BnorRset
    1.35 +  "measure ((\<lambda>(a, m). nat a) :: int * int => nat)"
    1.36 +  "BnorRset (a, m) =
    1.37 +   (if 0 < a then
    1.38 +    let na = BnorRset (a - 1, m)
    1.39 +    in (if zgcd a m = 1 then insert a na else na)
    1.40 +    else {})"
    1.41 +
    1.42 +definition
    1.43 +  norRRset :: "int => int set" where
    1.44 +  "norRRset m = BnorRset (m - 1, m)"
    1.45 +
    1.46 +definition
    1.47 +  noXRRset :: "int => int => int set" where
    1.48 +  "noXRRset m x = (\<lambda>a. a * x) ` norRRset m"
    1.49 +
    1.50 +definition
    1.51 +  phi :: "int => nat" where
    1.52 +  "phi m = card (norRRset m)"
    1.53 +
    1.54 +definition
    1.55 +  is_RRset :: "int set => int => bool" where
    1.56 +  "is_RRset A m = (A \<in> RsetR m \<and> card A = phi m)"
    1.57 +
    1.58 +definition
    1.59 +  RRset2norRR :: "int set => int => int => int" where
    1.60 +  "RRset2norRR A m a =
    1.61 +     (if 1 < m \<and> is_RRset A m \<and> a \<in> A then
    1.62 +        SOME b. zcong a b m \<and> b \<in> norRRset m
    1.63 +      else 0)"
    1.64 +
    1.65 +definition
    1.66 +  zcongm :: "int => int => int => bool" where
    1.67 +  "zcongm m = (\<lambda>a b. zcong a b m)"
    1.68 +
    1.69 +lemma abs_eq_1_iff [iff]: "(abs z = (1::int)) = (z = 1 \<or> z = -1)"
    1.70 +  -- {* LCP: not sure why this lemma is needed now *}
    1.71 +  by (auto simp add: abs_if)
    1.72 +
    1.73 +
    1.74 +text {* \medskip @{text norRRset} *}
    1.75 +
    1.76 +declare BnorRset.simps [simp del]
    1.77 +
    1.78 +lemma BnorRset_induct:
    1.79 +  assumes "!!a m. P {} a m"
    1.80 +    and "!!a m. 0 < (a::int) ==> P (BnorRset (a - 1, m::int)) (a - 1) m
    1.81 +      ==> P (BnorRset(a,m)) a m"
    1.82 +  shows "P (BnorRset(u,v)) u v"
    1.83 +  apply (rule BnorRset.induct)
    1.84 +  apply safe
    1.85 +   apply (case_tac [2] "0 < a")
    1.86 +    apply (rule_tac [2] prems)
    1.87 +     apply simp_all
    1.88 +   apply (simp_all add: BnorRset.simps prems)
    1.89 +  done
    1.90 +
    1.91 +lemma Bnor_mem_zle [rule_format]: "b \<in> BnorRset (a, m) \<longrightarrow> b \<le> a"
    1.92 +  apply (induct a m rule: BnorRset_induct)
    1.93 +   apply simp
    1.94 +  apply (subst BnorRset.simps)
    1.95 +   apply (unfold Let_def, auto)
    1.96 +  done
    1.97 +
    1.98 +lemma Bnor_mem_zle_swap: "a < b ==> b \<notin> BnorRset (a, m)"
    1.99 +  by (auto dest: Bnor_mem_zle)
   1.100 +
   1.101 +lemma Bnor_mem_zg [rule_format]: "b \<in> BnorRset (a, m) --> 0 < b"
   1.102 +  apply (induct a m rule: BnorRset_induct)
   1.103 +   prefer 2
   1.104 +   apply (subst BnorRset.simps)
   1.105 +   apply (unfold Let_def, auto)
   1.106 +  done
   1.107 +
   1.108 +lemma Bnor_mem_if [rule_format]:
   1.109 +    "zgcd b m = 1 --> 0 < b --> b \<le> a --> b \<in> BnorRset (a, m)"
   1.110 +  apply (induct a m rule: BnorRset.induct, auto)
   1.111 +   apply (subst BnorRset.simps)
   1.112 +   defer
   1.113 +   apply (subst BnorRset.simps)
   1.114 +   apply (unfold Let_def, auto)
   1.115 +  done
   1.116 +
   1.117 +lemma Bnor_in_RsetR [rule_format]: "a < m --> BnorRset (a, m) \<in> RsetR m"
   1.118 +  apply (induct a m rule: BnorRset_induct, simp)
   1.119 +  apply (subst BnorRset.simps)
   1.120 +  apply (unfold Let_def, auto)
   1.121 +  apply (rule RsetR.insert)
   1.122 +    apply (rule_tac [3] allI)
   1.123 +    apply (rule_tac [3] impI)
   1.124 +    apply (rule_tac [3] zcong_not)
   1.125 +       apply (subgoal_tac [6] "a' \<le> a - 1")
   1.126 +        apply (rule_tac [7] Bnor_mem_zle)
   1.127 +        apply (rule_tac [5] Bnor_mem_zg, auto)
   1.128 +  done
   1.129 +
   1.130 +lemma Bnor_fin: "finite (BnorRset (a, m))"
   1.131 +  apply (induct a m rule: BnorRset_induct)
   1.132 +   prefer 2
   1.133 +   apply (subst BnorRset.simps)
   1.134 +   apply (unfold Let_def, auto)
   1.135 +  done
   1.136 +
   1.137 +lemma norR_mem_unique_aux: "a \<le> b - 1 ==> a < (b::int)"
   1.138 +  apply auto
   1.139 +  done
   1.140 +
   1.141 +lemma norR_mem_unique:
   1.142 +  "1 < m ==>
   1.143 +    zgcd a m = 1 ==> \<exists>!b. [a = b] (mod m) \<and> b \<in> norRRset m"
   1.144 +  apply (unfold norRRset_def)
   1.145 +  apply (cut_tac a = a and m = m in zcong_zless_unique, auto)
   1.146 +   apply (rule_tac [2] m = m in zcong_zless_imp_eq)
   1.147 +       apply (auto intro: Bnor_mem_zle Bnor_mem_zg zcong_trans
   1.148 +	 order_less_imp_le norR_mem_unique_aux simp add: zcong_sym)
   1.149 +  apply (rule_tac x = b in exI, safe)
   1.150 +  apply (rule Bnor_mem_if)
   1.151 +    apply (case_tac [2] "b = 0")
   1.152 +     apply (auto intro: order_less_le [THEN iffD2])
   1.153 +   prefer 2
   1.154 +   apply (simp only: zcong_def)
   1.155 +   apply (subgoal_tac "zgcd a m = m")
   1.156 +    prefer 2
   1.157 +    apply (subst zdvd_iff_zgcd [symmetric])
   1.158 +     apply (rule_tac [4] zgcd_zcong_zgcd)
   1.159 +       apply (simp_all add: zcong_sym)
   1.160 +  done
   1.161 +
   1.162 +
   1.163 +text {* \medskip @{term noXRRset} *}
   1.164 +
   1.165 +lemma RRset_gcd [rule_format]:
   1.166 +    "is_RRset A m ==> a \<in> A --> zgcd a m = 1"
   1.167 +  apply (unfold is_RRset_def)
   1.168 +  apply (rule RsetR.induct [where P="%A. a \<in> A --> zgcd a m = 1"], auto)
   1.169 +  done
   1.170 +
   1.171 +lemma RsetR_zmult_mono:
   1.172 +  "A \<in> RsetR m ==>
   1.173 +    0 < m ==> zgcd x m = 1 ==> (\<lambda>a. a * x) ` A \<in> RsetR m"
   1.174 +  apply (erule RsetR.induct, simp_all)
   1.175 +  apply (rule RsetR.insert, auto)
   1.176 +   apply (blast intro: zgcd_zgcd_zmult)
   1.177 +  apply (simp add: zcong_cancel)
   1.178 +  done
   1.179 +
   1.180 +lemma card_nor_eq_noX:
   1.181 +  "0 < m ==>
   1.182 +    zgcd x m = 1 ==> card (noXRRset m x) = card (norRRset m)"
   1.183 +  apply (unfold norRRset_def noXRRset_def)
   1.184 +  apply (rule card_image)
   1.185 +   apply (auto simp add: inj_on_def Bnor_fin)
   1.186 +  apply (simp add: BnorRset.simps)
   1.187 +  done
   1.188 +
   1.189 +lemma noX_is_RRset:
   1.190 +    "0 < m ==> zgcd x m = 1 ==> is_RRset (noXRRset m x) m"
   1.191 +  apply (unfold is_RRset_def phi_def)
   1.192 +  apply (auto simp add: card_nor_eq_noX)
   1.193 +  apply (unfold noXRRset_def norRRset_def)
   1.194 +  apply (rule RsetR_zmult_mono)
   1.195 +    apply (rule Bnor_in_RsetR, simp_all)
   1.196 +  done
   1.197 +
   1.198 +lemma aux_some:
   1.199 +  "1 < m ==> is_RRset A m ==> a \<in> A
   1.200 +    ==> zcong a (SOME b. [a = b] (mod m) \<and> b \<in> norRRset m) m \<and>
   1.201 +      (SOME b. [a = b] (mod m) \<and> b \<in> norRRset m) \<in> norRRset m"
   1.202 +  apply (rule norR_mem_unique [THEN ex1_implies_ex, THEN someI_ex])
   1.203 +   apply (rule_tac [2] RRset_gcd, simp_all)
   1.204 +  done
   1.205 +
   1.206 +lemma RRset2norRR_correct:
   1.207 +  "1 < m ==> is_RRset A m ==> a \<in> A ==>
   1.208 +    [a = RRset2norRR A m a] (mod m) \<and> RRset2norRR A m a \<in> norRRset m"
   1.209 +  apply (unfold RRset2norRR_def, simp)
   1.210 +  apply (rule aux_some, simp_all)
   1.211 +  done
   1.212 +
   1.213 +lemmas RRset2norRR_correct1 =
   1.214 +  RRset2norRR_correct [THEN conjunct1, standard]
   1.215 +lemmas RRset2norRR_correct2 =
   1.216 +  RRset2norRR_correct [THEN conjunct2, standard]
   1.217 +
   1.218 +lemma RsetR_fin: "A \<in> RsetR m ==> finite A"
   1.219 +  by (induct set: RsetR) auto
   1.220 +
   1.221 +lemma RRset_zcong_eq [rule_format]:
   1.222 +  "1 < m ==>
   1.223 +    is_RRset A m ==> [a = b] (mod m) ==> a \<in> A --> b \<in> A --> a = b"
   1.224 +  apply (unfold is_RRset_def)
   1.225 +  apply (rule RsetR.induct [where P="%A. a \<in> A --> b \<in> A --> a = b"])
   1.226 +    apply (auto simp add: zcong_sym)
   1.227 +  done
   1.228 +
   1.229 +lemma aux:
   1.230 +  "P (SOME a. P a) ==> Q (SOME a. Q a) ==>
   1.231 +    (SOME a. P a) = (SOME a. Q a) ==> \<exists>a. P a \<and> Q a"
   1.232 +  apply auto
   1.233 +  done
   1.234 +
   1.235 +lemma RRset2norRR_inj:
   1.236 +    "1 < m ==> is_RRset A m ==> inj_on (RRset2norRR A m) A"
   1.237 +  apply (unfold RRset2norRR_def inj_on_def, auto)
   1.238 +  apply (subgoal_tac "\<exists>b. ([x = b] (mod m) \<and> b \<in> norRRset m) \<and>
   1.239 +      ([y = b] (mod m) \<and> b \<in> norRRset m)")
   1.240 +   apply (rule_tac [2] aux)
   1.241 +     apply (rule_tac [3] aux_some)
   1.242 +       apply (rule_tac [2] aux_some)
   1.243 +         apply (rule RRset_zcong_eq, auto)
   1.244 +  apply (rule_tac b = b in zcong_trans)
   1.245 +   apply (simp_all add: zcong_sym)
   1.246 +  done
   1.247 +
   1.248 +lemma RRset2norRR_eq_norR:
   1.249 +    "1 < m ==> is_RRset A m ==> RRset2norRR A m ` A = norRRset m"
   1.250 +  apply (rule card_seteq)
   1.251 +    prefer 3
   1.252 +    apply (subst card_image)
   1.253 +      apply (rule_tac RRset2norRR_inj, auto)
   1.254 +     apply (rule_tac [3] RRset2norRR_correct2, auto)
   1.255 +    apply (unfold is_RRset_def phi_def norRRset_def)
   1.256 +    apply (auto simp add: Bnor_fin)
   1.257 +  done
   1.258 +
   1.259 +
   1.260 +lemma Bnor_prod_power_aux: "a \<notin> A ==> inj f ==> f a \<notin> f ` A"
   1.261 +by (unfold inj_on_def, auto)
   1.262 +
   1.263 +lemma Bnor_prod_power [rule_format]:
   1.264 +  "x \<noteq> 0 ==> a < m --> \<Prod>((\<lambda>a. a * x) ` BnorRset (a, m)) =
   1.265 +      \<Prod>(BnorRset(a, m)) * x^card (BnorRset (a, m))"
   1.266 +  apply (induct a m rule: BnorRset_induct)
   1.267 +   prefer 2
   1.268 +   apply (simplesubst BnorRset.simps)  --{*multiple redexes*}
   1.269 +   apply (unfold Let_def, auto)
   1.270 +  apply (simp add: Bnor_fin Bnor_mem_zle_swap)
   1.271 +  apply (subst setprod_insert)
   1.272 +    apply (rule_tac [2] Bnor_prod_power_aux)
   1.273 +     apply (unfold inj_on_def)
   1.274 +     apply (simp_all add: zmult_ac Bnor_fin finite_imageI
   1.275 +       Bnor_mem_zle_swap)
   1.276 +  done
   1.277 +
   1.278 +
   1.279 +subsection {* Fermat *}
   1.280 +
   1.281 +lemma bijzcong_zcong_prod:
   1.282 +    "(A, B) \<in> bijR (zcongm m) ==> [\<Prod>A = \<Prod>B] (mod m)"
   1.283 +  apply (unfold zcongm_def)
   1.284 +  apply (erule bijR.induct)
   1.285 +   apply (subgoal_tac [2] "a \<notin> A \<and> b \<notin> B \<and> finite A \<and> finite B")
   1.286 +    apply (auto intro: fin_bijRl fin_bijRr zcong_zmult)
   1.287 +  done
   1.288 +
   1.289 +lemma Bnor_prod_zgcd [rule_format]:
   1.290 +    "a < m --> zgcd (\<Prod>(BnorRset(a, m))) m = 1"
   1.291 +  apply (induct a m rule: BnorRset_induct)
   1.292 +   prefer 2
   1.293 +   apply (subst BnorRset.simps)
   1.294 +   apply (unfold Let_def, auto)
   1.295 +  apply (simp add: Bnor_fin Bnor_mem_zle_swap)
   1.296 +  apply (blast intro: zgcd_zgcd_zmult)
   1.297 +  done
   1.298 +
   1.299 +theorem Euler_Fermat:
   1.300 +    "0 < m ==> zgcd x m = 1 ==> [x^(phi m) = 1] (mod m)"
   1.301 +  apply (unfold norRRset_def phi_def)
   1.302 +  apply (case_tac "x = 0")
   1.303 +   apply (case_tac [2] "m = 1")
   1.304 +    apply (rule_tac [3] iffD1)
   1.305 +     apply (rule_tac [3] k = "\<Prod>(BnorRset(m - 1, m))"
   1.306 +       in zcong_cancel2)
   1.307 +      prefer 5
   1.308 +      apply (subst Bnor_prod_power [symmetric])
   1.309 +        apply (rule_tac [7] Bnor_prod_zgcd, simp_all)
   1.310 +  apply (rule bijzcong_zcong_prod)
   1.311 +  apply (fold norRRset_def noXRRset_def)
   1.312 +  apply (subst RRset2norRR_eq_norR [symmetric])
   1.313 +    apply (rule_tac [3] inj_func_bijR, auto)
   1.314 +     apply (unfold zcongm_def)
   1.315 +     apply (rule_tac [2] RRset2norRR_correct1)
   1.316 +       apply (rule_tac [5] RRset2norRR_inj)
   1.317 +        apply (auto intro: order_less_le [THEN iffD2]
   1.318 +	   simp add: noX_is_RRset)
   1.319 +  apply (unfold noXRRset_def norRRset_def)
   1.320 +  apply (rule finite_imageI)
   1.321 +  apply (rule Bnor_fin)
   1.322 +  done
   1.323 +
   1.324 +lemma Bnor_prime:
   1.325 +  "\<lbrakk> zprime p; a < p \<rbrakk> \<Longrightarrow> card (BnorRset (a, p)) = nat a"
   1.326 +  apply (induct a p rule: BnorRset.induct)
   1.327 +  apply (subst BnorRset.simps)
   1.328 +  apply (unfold Let_def, auto simp add:zless_zprime_imp_zrelprime)
   1.329 +  apply (subgoal_tac "finite (BnorRset (a - 1,m))")
   1.330 +   apply (subgoal_tac "a ~: BnorRset (a - 1,m)")
   1.331 +    apply (auto simp add: card_insert_disjoint Suc_nat_eq_nat_zadd1)
   1.332 +   apply (frule Bnor_mem_zle, arith)
   1.333 +  apply (frule Bnor_fin)
   1.334 +  done
   1.335 +
   1.336 +lemma phi_prime: "zprime p ==> phi p = nat (p - 1)"
   1.337 +  apply (unfold phi_def norRRset_def)
   1.338 +  apply (rule Bnor_prime, auto)
   1.339 +  done
   1.340 +
   1.341 +theorem Little_Fermat:
   1.342 +    "zprime p ==> \<not> p dvd x ==> [x^(nat (p - 1)) = 1] (mod p)"
   1.343 +  apply (subst phi_prime [symmetric])
   1.344 +   apply (rule_tac [2] Euler_Fermat)
   1.345 +    apply (erule_tac [3] zprime_imp_zrelprime)
   1.346 +    apply (unfold zprime_def, auto)
   1.347 +  done
   1.348 +
   1.349 +end