src/HOL/Number_Theory/Residues.thy
 changeset 60527 eb431a5651fe parent 60526 fad653acf58f child 60528 190b4a7d8b87
```     1.1 --- a/src/HOL/Number_Theory/Residues.thy	Fri Jun 19 21:41:33 2015 +0200
1.2 +++ b/src/HOL/Number_Theory/Residues.thy	Fri Jun 19 23:40:46 2015 +0200
1.3 @@ -11,26 +11,21 @@
1.4  imports UniqueFactorization MiscAlgebra
1.5  begin
1.6
1.7 -(*
1.8 -
1.9 -  A locale for residue rings
1.10 -
1.11 -*)
1.12 +subsection \<open>A locale for residue rings\<close>
1.13
1.14 -definition residue_ring :: "int => int ring" where
1.15 -  "residue_ring m == (|
1.16 -    carrier =       {0..m - 1},
1.17 -    mult =          (%x y. (x * y) mod m),
1.18 -    one =           1,
1.19 -    zero =          0,
1.20 -    add =           (%x y. (x + y) mod m) |)"
1.21 +definition residue_ring :: "int \<Rightarrow> int ring"
1.22 +  where
1.23 +  "residue_ring m =
1.24 +    \<lparr>carrier = {0..m - 1},
1.25 +     mult = \<lambda>x y. (x * y) mod m,
1.26 +     one = 1,
1.27 +     zero = 0,
1.28 +     add = \<lambda>x y. (x + y) mod m\<rparr>"
1.29
1.30  locale residues =
1.31    fixes m :: int and R (structure)
1.32    assumes m_gt_one: "m > 1"
1.33 -  defines "R == residue_ring m"
1.34 -
1.35 -context residues
1.36 +  defines "R \<equiv> residue_ring m"
1.37  begin
1.38
1.39  lemma abelian_group: "abelian_group R"
1.40 @@ -76,8 +71,10 @@
1.41  context residues
1.42  begin
1.43
1.44 -(* These lemmas translate back and forth between internal and
1.45 -   external concepts *)
1.46 +text \<open>
1.47 +  These lemmas translate back and forth between internal and
1.48 +  external concepts.
1.49 +\<close>
1.50
1.51  lemma res_carrier_eq: "carrier R = {0..m - 1}"
1.52    unfolding R_def residue_ring_def by auto
1.53 @@ -94,11 +91,11 @@
1.54  lemma res_one_eq: "\<one> = 1"
1.55    unfolding R_def residue_ring_def units_of_def by auto
1.56
1.57 -lemma res_units_eq: "Units R = { x. 0 < x & x < m & coprime x m}"
1.58 +lemma res_units_eq: "Units R = {x. 0 < x \<and> x < m \<and> coprime x m}"
1.59    apply (insert m_gt_one)
1.60    apply (unfold Units_def R_def residue_ring_def)
1.61    apply auto
1.62 -  apply (subgoal_tac "x ~= 0")
1.63 +  apply (subgoal_tac "x \<noteq> 0")
1.64    apply auto
1.65    apply (metis invertible_coprime_int)
1.66    apply (subst (asm) coprime_iff_invertible'_int)
1.67 @@ -121,19 +118,20 @@
1.68    done
1.69
1.70  lemma finite [iff]: "finite (carrier R)"
1.71 -  by (subst res_carrier_eq, auto)
1.72 +  by (subst res_carrier_eq) auto
1.73
1.74  lemma finite_Units [iff]: "finite (Units R)"
1.75    by (subst res_units_eq) auto
1.76
1.77 -(* The function a -> a mod m maps the integers to the
1.78 -   residue classes. The following lemmas show that this mapping
1.79 -   respects addition and multiplication on the integers. *)
1.80 +text \<open>
1.81 +  The function @{text "a \<mapsto> a mod m"} maps the integers to the
1.82 +  residue classes. The following lemmas show that this mapping
1.83 +  respects addition and multiplication on the integers.
1.84 +\<close>
1.85
1.86 -lemma mod_in_carrier [iff]: "a mod m : carrier R"
1.87 -  apply (unfold res_carrier_eq)
1.88 -  apply (insert m_gt_one, auto)
1.89 -  done
1.90 +lemma mod_in_carrier [iff]: "a mod m \<in> carrier R"
1.91 +  unfolding res_carrier_eq
1.92 +  using insert m_gt_one by auto
1.93
1.94  lemma add_cong: "(x mod m) \<oplus> (y mod m) = (x + y) mod m"
1.95    unfolding R_def residue_ring_def
1.96 @@ -151,7 +149,7 @@
1.97  lemma one_cong: "\<one> = 1 mod m"
1.98    using m_gt_one unfolding R_def residue_ring_def by auto
1.99
1.100 -(* revise algebra library to use 1? *)
1.101 +(* FIXME revise algebra library to use 1? *)
1.102  lemma pow_cong: "(x mod m) (^) n = x^n mod m"
1.103    apply (insert m_gt_one)
1.104    apply (induct n)
1.105 @@ -162,19 +160,17 @@
1.106  lemma neg_cong: "\<ominus> (x mod m) = (- x) mod m"
1.107    by (metis mod_minus_eq res_neg_eq)
1.108
1.109 -lemma (in residues) prod_cong:
1.110 -    "finite A \<Longrightarrow> (\<Otimes> i:A. (f i) mod m) = (PROD i:A. f i) mod m"
1.111 +lemma (in residues) prod_cong: "finite A \<Longrightarrow> (\<Otimes> i:A. (f i) mod m) = (\<Prod>i\<in>A. f i) mod m"
1.112    by (induct set: finite) (auto simp: one_cong mult_cong)
1.113
1.114 -lemma (in residues) sum_cong:
1.115 -    "finite A \<Longrightarrow> (\<Oplus> i:A. (f i) mod m) = (SUM i: A. f i) mod m"
1.116 +lemma (in residues) sum_cong: "finite A \<Longrightarrow> (\<Oplus> i:A. (f i) mod m) = (\<Sum>i\<in>A. f i) mod m"
1.117    by (induct set: finite) (auto simp: zero_cong add_cong)
1.118
1.119 -lemma mod_in_res_units [simp]: "1 < m \<Longrightarrow> coprime a m \<Longrightarrow>
1.120 -    a mod m : Units R"
1.121 -  apply (subst res_units_eq, auto)
1.122 +lemma mod_in_res_units [simp]: "1 < m \<Longrightarrow> coprime a m \<Longrightarrow> a mod m \<in> Units R"
1.123 +  apply (subst res_units_eq)
1.124 +  apply auto
1.125    apply (insert pos_mod_sign [of m a])
1.126 -  apply (subgoal_tac "a mod m ~= 0")
1.127 +  apply (subgoal_tac "a mod m \<noteq> 0")
1.128    apply arith
1.129    apply auto
1.130    apply (metis gcd_int.commute gcd_red_int)
1.131 @@ -183,13 +179,13 @@
1.132  lemma res_eq_to_cong: "((a mod m) = (b mod m)) = [a = b] (mod (m::int))"
1.133    unfolding cong_int_def by auto
1.134
1.135 -(* Simplifying with these will translate a ring equation in R to a
1.136 -   congruence. *)
1.137
1.138 +text \<open>Simplifying with these will translate a ring equation in R to a
1.139 +   congruence.\<close>
1.140  lemmas res_to_cong_simps = add_cong mult_cong pow_cong one_cong
1.141      prod_cong sum_cong neg_cong res_eq_to_cong
1.142
1.143 -(* Other useful facts about the residue ring *)
1.144 +text \<open>Other useful facts about the residue ring.\<close>
1.145
1.146  lemma one_eq_neg_one: "\<one> = \<ominus> \<one> \<Longrightarrow> m = 2"
1.147    apply (simp add: res_one_eq res_neg_eq)
1.148 @@ -200,12 +196,12 @@
1.149  end
1.150
1.151
1.152 -(* prime residues *)
1.153 +subsection \<open>Prime residues\<close>
1.154
1.155  locale residues_prime =
1.156    fixes p and R (structure)
1.157    assumes p_prime [intro]: "prime p"
1.158 -  defines "R == residue_ring p"
1.159 +  defines "R \<equiv> residue_ring p"
1.160
1.161  sublocale residues_prime < residues p
1.162    apply (unfold R_def residues_def)
1.163 @@ -243,40 +239,42 @@
1.164    by (rule is_field)
1.165
1.166
1.167 -(*
1.168 -  Test cases: Euler's theorem and Wilson's theorem.
1.169 -*)
1.170 +section \<open>Test cases: Euler's theorem and Wilson's theorem\<close>
1.171
1.172 -
1.173 -subsection\<open>Euler's theorem\<close>
1.174 +subsection \<open>Euler's theorem\<close>
1.175
1.176 -(* the definition of the phi function *)
1.177 +text \<open>The definition of the phi function.\<close>
1.178
1.179 -definition phi :: "int => nat"
1.180 -  where "phi m = card({ x. 0 < x & x < m & gcd x m = 1})"
1.181 +definition phi :: "int \<Rightarrow> nat"
1.182 +  where "phi m = card {x. 0 < x \<and> x < m \<and> gcd x m = 1}"
1.183
1.184 -lemma phi_def_nat: "phi m = card({ x. 0 < x & x < nat m & gcd x (nat m) = 1})"
1.185 +lemma phi_def_nat: "phi m = card {x. 0 < x \<and> x < nat m \<and> gcd x (nat m) = 1}"
1.186    apply (simp add: phi_def)
1.187    apply (rule bij_betw_same_card [of nat])
1.188    apply (auto simp add: inj_on_def bij_betw_def image_def)
1.189    apply (metis dual_order.irrefl dual_order.strict_trans leI nat_1 transfer_nat_int_gcd(1))
1.190 -  apply (metis One_nat_def int_0 int_1 int_less_0_conv int_nat_eq nat_int transfer_int_nat_gcd(1) zless_int)
1.191 +  apply (metis One_nat_def int_0 int_1 int_less_0_conv int_nat_eq nat_int
1.192 +    transfer_int_nat_gcd(1) zless_int)
1.193    done
1.194
1.195  lemma prime_phi:
1.196 -  assumes  "2 \<le> p" "phi p = p - 1" shows "prime p"
1.197 +  assumes "2 \<le> p" "phi p = p - 1"
1.198 +  shows "prime p"
1.199  proof -
1.200    have "{x. 0 < x \<and> x < p \<and> coprime x p} = {1..p - 1}"
1.201      using assms unfolding phi_def_nat
1.202      by (intro card_seteq) fastforce+
1.203 -  then have cop: "\<And>x. x \<in> {1::nat..p - 1} \<Longrightarrow> coprime x p"
1.204 +  then have cop: "\<And>x::nat. x \<in> {1..p - 1} \<Longrightarrow> coprime x p"
1.205      by blast
1.206 -  { fix x::nat assume *: "1 < x" "x < p" and "x dvd p"
1.207 +  have False if *: "1 < x" "x < p" and "x dvd p" for x :: nat
1.208 +  proof -
1.209      have "coprime x p"
1.210        apply (rule cop)
1.211        using * apply auto
1.212        done
1.213 -    with \<open>x dvd p\<close> \<open>1 < x\<close> have "False" by auto }
1.214 +    with \<open>x dvd p\<close> \<open>1 < x\<close> show ?thesis
1.215 +      by auto
1.216 +  qed
1.217    then show ?thesis
1.218      using \<open>2 \<le> p\<close>
1.219      by (simp add: prime_def)
1.220 @@ -285,9 +283,9 @@
1.221  qed
1.222
1.223  lemma phi_zero [simp]: "phi 0 = 0"
1.224 -  apply (subst phi_def)
1.225 +  unfolding phi_def
1.226  (* Auto hangs here. Once again, where is the simplification rule
1.227 -   1 == Suc 0 coming from? *)
1.228 +   1 \<equiv> Suc 0 coming from? *)
1.229    apply (auto simp add: card_eq_0_iff)
1.230  (* Add card_eq_0_iff as a simp rule? delete card_empty_imp? *)
1.231    done
1.232 @@ -295,19 +293,19 @@
1.233  lemma phi_one [simp]: "phi 1 = 0"
1.234    by (auto simp add: phi_def card_eq_0_iff)
1.235
1.236 -lemma (in residues) phi_eq: "phi m = card(Units R)"
1.237 +lemma (in residues) phi_eq: "phi m = card (Units R)"
1.238    by (simp add: phi_def res_units_eq)
1.239
1.240  lemma (in residues) euler_theorem1:
1.241    assumes a: "gcd a m = 1"
1.242    shows "[a^phi m = 1] (mod m)"
1.243  proof -
1.244 -  from a m_gt_one have [simp]: "a mod m : Units R"
1.245 +  from a m_gt_one have [simp]: "a mod m \<in> Units R"
1.246      by (intro mod_in_res_units)
1.247    from phi_eq have "(a mod m) (^) (phi m) = (a mod m) (^) (card (Units R))"
1.248      by simp
1.249    also have "\<dots> = \<one>"
1.250 -    by (intro units_power_order_eq_one, auto)
1.251 +    by (intro units_power_order_eq_one) auto
1.252    finally show ?thesis
1.253      by (simp add: res_to_cong_simps)
1.254  qed
1.255 @@ -329,55 +327,57 @@
1.256  (* outside the locale, we can relax the restriction m > 1 *)
1.257
1.258  lemma euler_theorem:
1.259 -  assumes "m >= 0" and "gcd a m = 1"
1.260 +  assumes "m \<ge> 0"
1.261 +    and "gcd a m = 1"
1.262    shows "[a^phi m = 1] (mod m)"
1.263 -proof (cases)
1.264 -  assume "m = 0 | m = 1"
1.265 +proof (cases "m = 0 | m = 1")
1.266 +  case True
1.267    then show ?thesis by auto
1.268  next
1.269 -  assume "~(m = 0 | m = 1)"
1.270 +  case False
1.271    with assms show ?thesis
1.272      by (intro residues.euler_theorem1, unfold residues_def, auto)
1.273  qed
1.274
1.275 -lemma (in residues_prime) phi_prime: "phi p = (nat p - 1)"
1.276 +lemma (in residues_prime) phi_prime: "phi p = nat p - 1"
1.277    apply (subst phi_eq)
1.278    apply (subst res_prime_units_eq)
1.279    apply auto
1.280    done
1.281
1.282 -lemma phi_prime: "prime p \<Longrightarrow> phi p = (nat p - 1)"
1.283 +lemma phi_prime: "prime p \<Longrightarrow> phi p = nat p - 1"
1.284    apply (rule residues_prime.phi_prime)
1.285    apply (erule residues_prime.intro)
1.286    done
1.287
1.288  lemma fermat_theorem:
1.289 -  fixes a::int
1.290 -  assumes "prime p" and "~ (p dvd a)"
1.291 +  fixes a :: int
1.292 +  assumes "prime p"
1.293 +    and "\<not> p dvd a"
1.294    shows "[a^(p - 1) = 1] (mod p)"
1.295  proof -
1.296 -  from assms have "[a^phi p = 1] (mod p)"
1.297 +  from assms have "[a ^ phi p = 1] (mod p)"
1.298      apply (intro euler_theorem)
1.299      apply (metis of_nat_0_le_iff)
1.300      apply (metis gcd_int.commute prime_imp_coprime_int)
1.301      done
1.302    also have "phi p = nat p - 1"
1.303 -    by (rule phi_prime, rule assms)
1.304 +    by (rule phi_prime) (rule assms)
1.305    finally show ?thesis
1.306      by (metis nat_int)
1.307  qed
1.308
1.309  lemma fermat_theorem_nat:
1.310 -  assumes "prime p" and "~ (p dvd a)"
1.311 -  shows "[a^(p - 1) = 1] (mod p)"
1.312 -using fermat_theorem [of p a] assms
1.313 -by (metis int_1 of_nat_power transfer_int_nat_cong zdvd_int)
1.314 +  assumes "prime p" and "\<not> p dvd a"
1.315 +  shows "[a ^ (p - 1) = 1] (mod p)"
1.316 +  using fermat_theorem [of p a] assms
1.317 +  by (metis int_1 of_nat_power transfer_int_nat_cong zdvd_int)
1.318
1.319
1.320  subsection \<open>Wilson's theorem\<close>
1.321
1.322 -lemma (in field) inv_pair_lemma: "x : Units R \<Longrightarrow> y : Units R \<Longrightarrow>
1.323 -    {x, inv x} ~= {y, inv y} \<Longrightarrow> {x, inv x} Int {y, inv y} = {}"
1.324 +lemma (in field) inv_pair_lemma: "x \<in> Units R \<Longrightarrow> y \<in> Units R \<Longrightarrow>
1.325 +    {x, inv x} \<noteq> {y, inv y} \<Longrightarrow> {x, inv x} \<inter> {y, inv y} = {}"
1.326    apply auto
1.327    apply (metis Units_inv_inv)+
1.328    done
1.329 @@ -386,41 +386,43 @@
1.330    assumes a: "p > 2"
1.331    shows "[fact (p - 1) = (-1::int)] (mod p)"
1.332  proof -
1.333 -  let ?InversePairs = "{ {x, inv x} | x. x : Units R - {\<one>, \<ominus> \<one>}}"
1.334 -  have UR: "Units R = {\<one>, \<ominus> \<one>} Un (Union ?InversePairs)"
1.335 +  let ?Inverse_Pairs = "{{x, inv x}| x. x \<in> Units R - {\<one>, \<ominus> \<one>}}"
1.336 +  have UR: "Units R = {\<one>, \<ominus> \<one>} \<union> \<Union>?Inverse_Pairs"
1.337      by auto
1.338 -  have "(\<Otimes>i: Units R. i) =
1.339 -    (\<Otimes>i: {\<one>, \<ominus> \<one>}. i) \<otimes> (\<Otimes>i: Union ?InversePairs. i)"
1.340 +  have "(\<Otimes>i\<in>Units R. i) = (\<Otimes>i\<in>{\<one>, \<ominus> \<one>}. i) \<otimes> (\<Otimes>i\<in>\<Union>?Inverse_Pairs. i)"
1.341      apply (subst UR)
1.342      apply (subst finprod_Un_disjoint)
1.343      apply (auto intro: funcsetI)
1.344 -    apply (metis Units_inv_inv inv_one inv_neg_one)+
1.345 +    using inv_one apply auto[1]
1.346 +    using inv_eq_neg_one_eq apply auto
1.347      done
1.348 -  also have "(\<Otimes>i: {\<one>, \<ominus> \<one>}. i) = \<ominus> \<one>"
1.349 +  also have "(\<Otimes>i\<in>{\<one>, \<ominus> \<one>}. i) = \<ominus> \<one>"
1.350      apply (subst finprod_insert)
1.351      apply auto
1.352      apply (frule one_eq_neg_one)
1.353 -    apply (insert a, force)
1.354 +    using a apply force
1.355      done
1.356 -  also have "(\<Otimes>i:(Union ?InversePairs). i) =
1.357 -      (\<Otimes>A: ?InversePairs. (\<Otimes>y:A. y))"
1.358 -    apply (subst finprod_Union_disjoint, auto)
1.359 +  also have "(\<Otimes>i\<in>(\<Union>?Inverse_Pairs). i) = (\<Otimes>A\<in>?Inverse_Pairs. (\<Otimes>y\<in>A. y))"
1.360 +    apply (subst finprod_Union_disjoint)
1.361 +    apply auto
1.362      apply (metis Units_inv_inv)+
1.363      done
1.364    also have "\<dots> = \<one>"
1.365 -    apply (rule finprod_one, auto)
1.366 -    apply (subst finprod_insert, auto)
1.367 +    apply (rule finprod_one)
1.368 +    apply auto
1.369 +    apply (subst finprod_insert)
1.370 +    apply auto
1.371      apply (metis inv_eq_self)
1.372      done
1.373 -  finally have "(\<Otimes>i: Units R. i) = \<ominus> \<one>"
1.374 +  finally have "(\<Otimes>i\<in>Units R. i) = \<ominus> \<one>"
1.375      by simp
1.376 -  also have "(\<Otimes>i: Units R. i) = (\<Otimes>i: Units R. i mod p)"
1.377 +  also have "(\<Otimes>i\<in>Units R. i) = (\<Otimes>i\<in>Units R. i mod p)"
1.378      apply (rule finprod_cong')
1.379 -    apply (auto)
1.380 +    apply auto
1.381      apply (subst (asm) res_prime_units_eq)
1.382      apply auto
1.383      done
1.384 -  also have "\<dots> = (PROD i: Units R. i) mod p"
1.385 +  also have "\<dots> = (\<Prod>i\<in>Units R. i) mod p"
1.386      apply (rule prod_cong)
1.387      apply auto
1.388      done
1.389 @@ -430,13 +432,14 @@
1.390      apply (subst res_prime_units_eq)
1.391      apply (simp add: int_setprod zmod_int setprod_int_eq)
1.392      done
1.393 -  finally have "fact (p - 1) mod p = (\<ominus> \<one> :: int)".
1.394 -  then show ?thesis
1.395 +  finally have "fact (p - 1) mod p = \<ominus> \<one>" .
1.396 +  then show ?thesis
1.397      by (metis of_nat_fact Divides.transfer_int_nat_functions(2) cong_int_def res_neg_eq res_one_eq)
1.398  qed
1.399
1.400  lemma wilson_theorem:
1.401 -  assumes "prime p" shows "[fact (p - 1) = - 1] (mod p)"
1.402 +  assumes "prime p"
1.403 +  shows "[fact (p - 1) = - 1] (mod p)"
1.404  proof (cases "p = 2")
1.405    case True
1.406    then show ?thesis
```