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
```