src/HOL/Number_Theory/Residues.thy
changeset 55352 1d2852dfc4a7
parent 55262 16724746ad89
child 57512 cc97b347b301
     1.1 --- a/src/HOL/Number_Theory/Residues.thy	Thu Feb 06 23:55:00 2014 +0100
     1.2 +++ b/src/HOL/Number_Theory/Residues.thy	Thu Feb 06 23:09:22 2014 +0000
     1.3 @@ -103,11 +103,8 @@
     1.4    apply auto
     1.5    apply (subgoal_tac "x ~= 0")
     1.6    apply auto
     1.7 -  apply (rule invertible_coprime_int)
     1.8 -  apply (subgoal_tac "x ~= 0")
     1.9 -  apply auto
    1.10 +  apply (metis invertible_coprime_int)
    1.11    apply (subst (asm) coprime_iff_invertible'_int)
    1.12 -  apply arith
    1.13    apply (auto simp add: cong_int_def mult_commute)
    1.14    done
    1.15  
    1.16 @@ -123,8 +120,7 @@
    1.17    apply auto
    1.18    apply (subgoal_tac "y mod m = - x mod m")
    1.19    apply simp
    1.20 -  apply (subst zmod_eq_dvd_iff)
    1.21 -  apply auto
    1.22 +  apply (metis minus_add_cancel mod_mult_self1 mult_commute)
    1.23    done
    1.24  
    1.25  lemma finite [iff]: "finite (carrier R)"
    1.26 @@ -149,13 +145,8 @@
    1.27    done
    1.28  
    1.29  lemma mult_cong: "(x mod m) \<otimes> (y mod m) = (x * y) mod m"
    1.30 -  apply (unfold R_def residue_ring_def, auto)
    1.31 -  apply (subst mod_mult_right_eq [symmetric])
    1.32 -  apply (subst mult_commute)
    1.33 -  apply (subst mod_mult_right_eq [symmetric])
    1.34 -  apply (subst mult_commute)
    1.35 -  apply auto
    1.36 -  done
    1.37 +  unfolding R_def residue_ring_def
    1.38 +  by auto (metis mod_mult_eq)
    1.39  
    1.40  lemma zero_cong: "\<zero> = 0"
    1.41    unfolding R_def residue_ring_def by auto
    1.42 @@ -168,30 +159,19 @@
    1.43    apply (insert m_gt_one)
    1.44    apply (induct n)
    1.45    apply (auto simp add: nat_pow_def one_cong)
    1.46 -  apply (subst mult_commute)
    1.47 -  apply (rule mult_cong)
    1.48 +  apply (metis mult_commute mult_cong)
    1.49    done
    1.50  
    1.51  lemma neg_cong: "\<ominus> (x mod m) = (- x) mod m"
    1.52 -  apply (rule sym)
    1.53 -  apply (rule sum_zero_eq_neg)
    1.54 -  apply auto
    1.55 -  apply (subst add_cong)
    1.56 -  apply (subst zero_cong)
    1.57 -  apply auto
    1.58 -  done
    1.59 +  by (metis mod_minus_eq res_neg_eq)
    1.60  
    1.61  lemma (in residues) prod_cong:
    1.62      "finite A \<Longrightarrow> (\<Otimes> i:A. (f i) mod m) = (PROD i:A. f i) mod m"
    1.63 -  apply (induct set: finite)
    1.64 -  apply (auto simp: one_cong mult_cong)
    1.65 -  done
    1.66 +  by (induct set: finite) (auto simp: one_cong mult_cong)
    1.67  
    1.68  lemma (in residues) sum_cong:
    1.69      "finite A \<Longrightarrow> (\<Oplus> i:A. (f i) mod m) = (SUM i: A. f i) mod m"
    1.70 -  apply (induct set: finite)
    1.71 -  apply (auto simp: zero_cong add_cong)
    1.72 -  done
    1.73 +  by (induct set: finite) (auto simp: zero_cong add_cong)
    1.74  
    1.75  lemma mod_in_res_units [simp]: "1 < m \<Longrightarrow> coprime a m \<Longrightarrow>
    1.76      a mod m : Units R"
    1.77 @@ -200,8 +180,7 @@
    1.78    apply (subgoal_tac "a mod m ~= 0")
    1.79    apply arith
    1.80    apply auto
    1.81 -  apply (subst (asm) gcd_red_int)
    1.82 -  apply (subst gcd_commute_int, assumption)
    1.83 +  apply (metis gcd_int.commute gcd_red_int)
    1.84    done
    1.85  
    1.86  lemma res_eq_to_cong: "((a mod m) = (b mod m)) = [a = b] (mod (m::int))"
    1.87 @@ -217,15 +196,8 @@
    1.88  
    1.89  lemma one_eq_neg_one: "\<one> = \<ominus> \<one> \<Longrightarrow> m = 2"
    1.90    apply (simp add: res_one_eq res_neg_eq)
    1.91 -  apply (insert m_gt_one)
    1.92 -  apply (subgoal_tac "~(m > 2)")
    1.93 -  apply arith
    1.94 -  apply (rule notI)
    1.95 -  apply (subgoal_tac "-1 mod m = m - 1")
    1.96 -  apply force
    1.97 -  apply (subst mod_add_self2 [symmetric])
    1.98 -  apply (subst mod_pos_pos_trivial)
    1.99 -  apply auto
   1.100 +  apply (metis add_commute add_diff_cancel mod_mod_trivial one_add_one uminus_add_conv_diff
   1.101 +            zero_neq_one zmod_zminus1_eq_if)
   1.102    done
   1.103  
   1.104  end
   1.105 @@ -265,10 +237,7 @@
   1.106    apply (subst res_units_eq)
   1.107    apply auto
   1.108    apply (subst gcd_commute_int)
   1.109 -  apply (rule prime_imp_coprime_int)
   1.110 -  apply (rule p_prime)
   1.111 -  apply (rule zdvd_not_zless)
   1.112 -  apply auto
   1.113 +  apply (auto simp add: p_prime prime_imp_coprime_int zdvd_not_zless)
   1.114    done
   1.115  
   1.116  end
   1.117 @@ -314,7 +283,8 @@
   1.118    then show ?thesis 
   1.119      using `2 \<le> p` 
   1.120      by (simp add: prime_def)
   1.121 -       (metis One_nat_def dvd_pos_nat nat_dvd_not_less nat_neq_iff not_gr0 not_numeral_le_zero one_dvd)
   1.122 +       (metis One_nat_def dvd_pos_nat nat_dvd_not_less nat_neq_iff not_gr0 
   1.123 +              not_numeral_le_zero one_dvd)
   1.124  qed
   1.125  
   1.126  lemma phi_zero [simp]: "phi 0 = 0"
   1.127 @@ -412,12 +382,7 @@
   1.128  lemma (in field) inv_pair_lemma: "x : Units R \<Longrightarrow> y : Units R \<Longrightarrow>
   1.129      {x, inv x} ~= {y, inv y} \<Longrightarrow> {x, inv x} Int {y, inv y} = {}"
   1.130    apply auto
   1.131 -  apply (erule notE)
   1.132 -  apply (erule inv_eq_imp_eq)
   1.133 -  apply auto
   1.134 -  apply (erule notE)
   1.135 -  apply (erule inv_eq_imp_eq)
   1.136 -  apply auto
   1.137 +  apply (metis Units_inv_inv)+
   1.138    done
   1.139  
   1.140  lemma (in residues_prime) wilson_theorem1:
   1.141 @@ -431,11 +396,8 @@
   1.142      (\<Otimes>i: {\<one>, \<ominus> \<one>}. i) \<otimes> (\<Otimes>i: Union ?InversePairs. i)"
   1.143      apply (subst UR)
   1.144      apply (subst finprod_Un_disjoint)
   1.145 -    apply (auto intro:funcsetI)
   1.146 -    apply (drule sym, subst (asm) inv_eq_one_eq)
   1.147 -    apply auto
   1.148 -    apply (drule sym, subst (asm) inv_eq_neg_one_eq)
   1.149 -    apply auto
   1.150 +    apply (auto intro: funcsetI)
   1.151 +    apply (metis Units_inv_inv inv_one inv_neg_one)+
   1.152      done
   1.153    also have "(\<Otimes>i: {\<one>, \<ominus> \<one>}. i) = \<ominus> \<one>"
   1.154      apply (subst finprod_insert)
   1.155 @@ -445,20 +407,13 @@
   1.156      done
   1.157    also have "(\<Otimes>i:(Union ?InversePairs). i) =
   1.158        (\<Otimes>A: ?InversePairs. (\<Otimes>y:A. y))"
   1.159 -    apply (subst finprod_Union_disjoint)
   1.160 -    apply force
   1.161 -    apply force
   1.162 -    apply clarify
   1.163 -    apply (rule inv_pair_lemma)
   1.164 -    apply auto
   1.165 +    apply (subst finprod_Union_disjoint, auto)
   1.166 +    apply (metis Units_inv_inv)+
   1.167      done
   1.168    also have "\<dots> = \<one>"
   1.169 -    apply (rule finprod_one)
   1.170 -    apply auto
   1.171 -    apply (subst finprod_insert)
   1.172 -    apply auto
   1.173 -    apply (frule inv_eq_self)
   1.174 -    apply (auto)
   1.175 +    apply (rule finprod_one, auto)
   1.176 +    apply (subst finprod_insert, auto)
   1.177 +    apply (metis inv_eq_self)
   1.178      done
   1.179    finally have "(\<Otimes>i: Units R. i) = \<ominus> \<one>"
   1.180      by simp
   1.181 @@ -483,15 +438,17 @@
   1.182      by (metis Divides.transfer_int_nat_functions(2) cong_int_def res_neg_eq res_one_eq)
   1.183  qed
   1.184  
   1.185 -lemma wilson_theorem: "prime p \<Longrightarrow> [fact (p - 1) = - 1] (mod p)"
   1.186 -  apply (frule prime_gt_1_nat)
   1.187 -  apply (case_tac "p = 2")
   1.188 -  apply (subst fact_altdef_nat, simp)
   1.189 -  apply (subst cong_int_def)
   1.190 -  apply simp
   1.191 -  apply (rule residues_prime.wilson_theorem1)
   1.192 -  apply (rule residues_prime.intro)
   1.193 -  apply auto
   1.194 -  done
   1.195 +lemma wilson_theorem:
   1.196 +  assumes "prime p" shows "[fact (p - 1) = - 1] (mod p)"
   1.197 +proof (cases "p = 2")
   1.198 +  case True 
   1.199 +  then show ?thesis
   1.200 +    by (simp add: cong_int_def fact_altdef_nat)
   1.201 +next
   1.202 +  case False
   1.203 +  then show ?thesis
   1.204 +    using assms prime_ge_2_nat
   1.205 +    by (metis residues_prime.wilson_theorem1 residues_prime.intro le_eq_less_or_eq)
   1.206 +qed
   1.207  
   1.208  end