src/HOL/Number_Theory/Residues.thy
changeset 60688 01488b559910
parent 60528 190b4a7d8b87
child 62348 9a5f43dac883
     1.1 --- a/src/HOL/Number_Theory/Residues.thy	Wed Jul 08 14:01:40 2015 +0200
     1.2 +++ b/src/HOL/Number_Theory/Residues.thy	Wed Jul 08 14:01:41 2015 +0200
     1.3 @@ -166,15 +166,20 @@
     1.4  lemma (in residues) sum_cong: "finite A \<Longrightarrow> (\<Oplus>i\<in>A. (f i) mod m) = (\<Sum>i\<in>A. f i) mod m"
     1.5    by (induct set: finite) (auto simp: zero_cong add_cong)
     1.6  
     1.7 -lemma mod_in_res_units [simp]: "1 < m \<Longrightarrow> coprime a m \<Longrightarrow> a mod m \<in> Units R"
     1.8 -  apply (subst res_units_eq)
     1.9 -  apply auto
    1.10 -  apply (insert pos_mod_sign [of m a])
    1.11 -  apply (subgoal_tac "a mod m \<noteq> 0")
    1.12 -  apply arith
    1.13 -  apply auto
    1.14 -  apply (metis gcd_int.commute gcd_red_int)
    1.15 -  done
    1.16 +lemma mod_in_res_units [simp]:
    1.17 +  assumes "1 < m" and "coprime a m"
    1.18 +  shows "a mod m \<in> Units R"
    1.19 +proof (cases "a mod m = 0")
    1.20 +  case True with assms show ?thesis
    1.21 +    by (auto simp add: res_units_eq gcd_red_int [symmetric])
    1.22 +next
    1.23 +  case False
    1.24 +  from assms have "0 < m" by simp
    1.25 +  with pos_mod_sign [of m a] have "0 \<le> a mod m" .
    1.26 +  with False have "0 < a mod m" by simp
    1.27 +  with assms show ?thesis
    1.28 +    by (auto simp add: res_units_eq gcd_red_int [symmetric] ac_simps)
    1.29 +qed
    1.30  
    1.31  lemma res_eq_to_cong: "(a mod m) = (b mod m) \<longleftrightarrow> [a = b] (mod m)"
    1.32    unfolding cong_int_def by auto
    1.33 @@ -354,10 +359,7 @@
    1.34    shows "[a^(p - 1) = 1] (mod p)"
    1.35  proof -
    1.36    from assms have "[a ^ phi p = 1] (mod p)"
    1.37 -    apply (intro euler_theorem)
    1.38 -    apply (metis of_nat_0_le_iff)
    1.39 -    apply (metis gcd_int.commute prime_imp_coprime_int)
    1.40 -    done
    1.41 +    by (auto intro!: euler_theorem dest!: prime_imp_coprime_int simp add: ac_simps)
    1.42    also have "phi p = nat p - 1"
    1.43      by (rule phi_prime) (rule assms)
    1.44    finally show ?thesis