src/HOL/Number_Theory/Residues.thy
 changeset 41541 1fa4725c4656 parent 36350 bc7982c54e37 child 41959 b460124855b8
```     1.1 --- a/src/HOL/Number_Theory/Residues.thy	Thu Jan 13 21:50:13 2011 +0100
1.2 +++ b/src/HOL/Number_Theory/Residues.thy	Thu Jan 13 23:50:16 2011 +0100
1.3 @@ -1,18 +1,17 @@
1.4  (*  Title:      HOL/Library/Residues.thy
1.5 -    ID:
1.7
1.8 -    An algebraic treatment of residue rings, and resulting proofs of
1.9 -    Euler's theorem and Wilson's theorem.
1.10 +An algebraic treatment of residue rings, and resulting proofs of
1.11 +Euler's theorem and Wilson's theorem.
1.12  *)
1.13
1.14  header {* Residue rings *}
1.15
1.16  theory Residues
1.17  imports
1.18 -   UniqueFactorization
1.19 -   Binomial
1.20 -   MiscAlgebra
1.21 +  UniqueFactorization
1.22 +  Binomial
1.23 +  MiscAlgebra
1.24  begin
1.25
1.26
1.27 @@ -41,14 +40,13 @@
1.28    apply (insert m_gt_one)
1.29    apply (rule abelian_groupI)
1.30    apply (unfold R_def residue_ring_def)
1.34    apply (case_tac "x = 0")
1.35    apply force
1.36    apply (subgoal_tac "(x + (m - x)) mod m = 0")
1.37    apply (erule bexI)
1.38    apply auto
1.39 -done
1.40 +  done
1.41
1.42  lemma comm_monoid: "comm_monoid R"
1.43    apply (insert m_gt_one)
1.44 @@ -59,7 +57,7 @@
1.45    apply (erule ssubst)
1.46    apply (subst zmod_zmult1_eq [symmetric])+
1.47    apply (simp_all only: mult_ac)
1.48 -done
1.49 +  done
1.50
1.51  lemma cring: "cring R"
1.52    apply (rule cringI)
1.53 @@ -70,7 +68,7 @@
1.54    apply (subst mult_commute)
1.55    apply (subst zmod_zmult1_eq [symmetric])
1.57 -done
1.58 +  done
1.59
1.60  end
1.61
1.62 @@ -78,7 +76,8 @@
1.63    by (rule cring)
1.64
1.65
1.66 -context residues begin
1.67 +context residues
1.68 +begin
1.69
1.70  (* These lemmas translate back and forth between internal and
1.71     external concepts *)
1.72 @@ -96,7 +95,7 @@
1.73    by (unfold R_def residue_ring_def, auto)
1.74
1.75  lemma res_one_eq: "\<one> = 1"
1.76 -  by (unfold R_def residue_ring_def units_of_def residue_ring_def, auto)
1.77 +  by (unfold R_def residue_ring_def units_of_def, auto)
1.78
1.79  lemma res_units_eq: "Units R = { x. 0 < x & x < m & coprime x m}"
1.80    apply (insert m_gt_one)
1.81 @@ -110,7 +109,7 @@
1.82    apply (subst (asm) coprime_iff_invertible'_int)
1.83    apply (rule m_gt_one)
1.84    apply (auto simp add: cong_int_def mult_commute)
1.85 -done
1.86 +  done
1.87
1.88  lemma res_neg_eq: "\<ominus> x = (- x) mod m"
1.89    apply (insert m_gt_one)
1.90 @@ -126,7 +125,7 @@
1.91    apply simp
1.92    apply (subst zmod_eq_dvd_iff)
1.93    apply auto
1.94 -done
1.95 +  done
1.96
1.97  lemma finite [iff]: "finite(carrier R)"
1.98    by (subst res_carrier_eq, auto)
1.99 @@ -141,7 +140,7 @@
1.100  lemma mod_in_carrier [iff]: "a mod m : carrier R"
1.101    apply (unfold res_carrier_eq)
1.102    apply (insert m_gt_one, auto)
1.103 -done
1.104 +  done
1.105
1.106  lemma add_cong: "(x mod m) \<oplus> (y mod m) = (x + y) mod m"
1.107    by (unfold R_def residue_ring_def, auto, arith)
1.108 @@ -153,25 +152,25 @@
1.109    apply (subst zmod_zmult1_eq [symmetric])
1.110    apply (subst mult_commute)
1.111    apply auto
1.112 -done
1.113 +  done
1.114
1.115  lemma zero_cong: "\<zero> = 0"
1.116    apply (unfold R_def residue_ring_def, auto)
1.117 -done
1.118 +  done
1.119
1.120  lemma one_cong: "\<one> = 1 mod m"
1.121    apply (insert m_gt_one)
1.122    apply (unfold R_def residue_ring_def, auto)
1.123 -done
1.124 +  done
1.125
1.126  (* revise algebra library to use 1? *)
1.127  lemma pow_cong: "(x mod m) (^) n = x^n mod m"
1.128    apply (insert m_gt_one)
1.129    apply (induct n)
1.130 -  apply (auto simp add: nat_pow_def one_cong One_nat_def)
1.131 +  apply (auto simp add: nat_pow_def one_cong)
1.132    apply (subst mult_commute)
1.133    apply (rule mult_cong)
1.134 -done
1.135 +  done
1.136
1.137  lemma neg_cong: "\<ominus> (x mod m) = (- x) mod m"
1.138    apply (rule sym)
1.139 @@ -180,19 +179,19 @@
1.141    apply (subst zero_cong)
1.142    apply auto
1.143 -done
1.144 +  done
1.145
1.146  lemma (in residues) prod_cong:
1.147    "finite A \<Longrightarrow> (\<Otimes> i:A. (f i) mod m) = (PROD i:A. f i) mod m"
1.148    apply (induct set: finite)
1.149    apply (auto simp: one_cong mult_cong)
1.150 -done
1.151 +  done
1.152
1.153  lemma (in residues) sum_cong:
1.154    "finite A \<Longrightarrow> (\<Oplus> i:A. (f i) mod m) = (SUM i: A. f i) mod m"
1.155    apply (induct set: finite)
1.156    apply (auto simp: zero_cong add_cong)
1.157 -done
1.158 +  done
1.159
1.160  lemma mod_in_res_units [simp]: "1 < m \<Longrightarrow> coprime a m \<Longrightarrow>
1.161      a mod m : Units R"
1.162 @@ -203,7 +202,7 @@
1.163    apply auto
1.164    apply (subst (asm) gcd_red_int)
1.165    apply (subst gcd_commute_int, assumption)
1.166 -done
1.167 +  done
1.168
1.169  lemma res_eq_to_cong: "((a mod m) = (b mod m)) = [a = b] (mod (m::int))"
1.170    unfolding cong_int_def by auto
1.171 @@ -227,7 +226,7 @@
1.173    apply (subst mod_pos_pos_trivial)
1.174    apply auto
1.175 -done
1.176 +  done
1.177
1.178  end
1.179
1.180 @@ -242,7 +241,7 @@
1.181  sublocale residues_prime < residues p
1.182    apply (unfold R_def residues_def)
1.183    using p_prime apply auto
1.184 -done
1.185 +  done
1.186
1.187  context residues_prime begin
1.188
1.189 @@ -259,7 +258,7 @@
1.190    apply (rule notI)
1.191    apply (frule zdvd_imp_le)
1.192    apply auto
1.193 -done
1.194 +  done
1.195
1.196  lemma res_prime_units_eq: "Units R = {1..p - 1}"
1.197    apply (subst res_units_eq)
1.198 @@ -269,7 +268,7 @@
1.199    apply (rule p_prime)
1.200    apply (rule zdvd_not_zless)
1.201    apply auto
1.202 -done
1.203 +  done
1.204
1.205  end
1.206
1.207 @@ -295,11 +294,11 @@
1.208     1 == Suc 0 coming from? *)
1.209    apply (auto simp add: card_eq_0_iff)
1.210  (* Add card_eq_0_iff as a simp rule? delete card_empty_imp? *)
1.211 -done
1.212 +  done
1.213
1.214  lemma phi_one [simp]: "phi 1 = 0"
1.215    apply (auto simp add: phi_def card_eq_0_iff)
1.216 -done
1.217 +  done
1.218
1.219  lemma (in residues) phi_eq: "phi m = card(Units R)"
1.220    by (simp add: phi_def res_units_eq)
1.221 @@ -342,7 +341,7 @@
1.222    thus ?thesis by auto
1.223  next
1.224    assume "~(m = 0 | m = 1)"
1.225 -  with prems show ?thesis
1.226 +  with assms show ?thesis
1.227      by (intro residues.euler_theorem1, unfold residues_def, auto)
1.228  qed
1.229
1.230 @@ -350,18 +349,18 @@
1.231    apply (subst phi_eq)
1.232    apply (subst res_prime_units_eq)
1.233    apply auto
1.234 -done
1.235 +  done
1.236
1.237  lemma phi_prime: "prime p \<Longrightarrow> phi p = (nat p - 1)"
1.238    apply (rule residues_prime.phi_prime)
1.239    apply (erule residues_prime.intro)
1.240 -done
1.241 +  done
1.242
1.243  lemma fermat_theorem:
1.244    assumes "prime p" and "~ (p dvd a)"
1.245    shows "[a^(nat p - 1) = 1] (mod p)"
1.246  proof -
1.247 -  from prems have "[a^phi p = 1] (mod p)"
1.248 +  from assms have "[a^phi p = 1] (mod p)"
1.249      apply (intro euler_theorem)
1.250      (* auto should get this next part. matching across
1.251         substitutions is needed. *)
1.252 @@ -369,7 +368,7 @@
1.253      apply (subst gcd_commute_int, erule prime_imp_coprime_int, assumption)
1.254      done
1.255    also have "phi p = nat p - 1"
1.256 -    by (rule phi_prime, rule prems)
1.257 +    by (rule phi_prime, rule assms)
1.258    finally show ?thesis .
1.259  qed
1.260
1.261 @@ -377,7 +376,7 @@
1.262  subsection {* Wilson's theorem *}
1.263
1.264  lemma (in field) inv_pair_lemma: "x : Units R \<Longrightarrow> y : Units R \<Longrightarrow>
1.265 -  {x, inv x} ~= {y, inv y} \<Longrightarrow> {x, inv x} Int {y, inv y} = {}"
1.266 +    {x, inv x} ~= {y, inv y} \<Longrightarrow> {x, inv x} Int {y, inv y} = {}"
1.267    apply auto
1.268    apply (erule notE)
1.269    apply (erule inv_eq_imp_eq)
1.270 @@ -385,7 +384,7 @@
1.271    apply (erule notE)
1.272    apply (erule inv_eq_imp_eq)
1.273    apply auto
1.274 -done
1.275 +  done
1.276
1.277  lemma (in residues_prime) wilson_theorem1:
1.278    assumes a: "p > 2"
1.279 @@ -411,7 +410,7 @@
1.280      apply (insert a, force)
1.281      done
1.282    also have "(\<Otimes>i:(Union ?InversePairs). i) =
1.283 -      (\<Otimes> A: ?InversePairs. (\<Otimes> y:A. y))"
1.284 +      (\<Otimes>A: ?InversePairs. (\<Otimes>y:A. y))"
1.285      apply (subst finprod_Union_disjoint)
1.286      apply force
1.287      apply force
1.288 @@ -441,7 +440,7 @@
1.289      done
1.290    also have "\<dots> = fact (p - 1) mod p"
1.291      apply (subst fact_altdef_int)
1.292 -    apply (insert prems, force)
1.293 +    apply (insert assms, force)
1.294      apply (subst res_prime_units_eq, rule refl)
1.295      done
1.296    finally have "fact (p - 1) mod p = \<ominus> \<one>".
```