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.6      Author:     Jeremy Avigad
     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.31 -  apply (auto simp add: mod_pos_pos_trivial mod_add_right_eq [symmetric]
    1.32 -    add_ac)
    1.33 +  apply (auto simp add: mod_add_right_eq [symmetric] add_ac)
    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.56    apply (simp add: field_simps)
    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.140    apply (subst add_cong)
   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.172    apply (subst mod_add_self2 [symmetric])
   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>".