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