src/HOL/Number_Theory/Residues.thy
 changeset 66837 6ba663ff2b1c parent 66817 0b12755ccbb2 child 66888 930abfdf8727
```     1.1 --- a/src/HOL/Number_Theory/Residues.thy	Mon Oct 09 19:10:47 2017 +0200
1.2 +++ b/src/HOL/Number_Theory/Residues.thy	Mon Oct 09 19:10:48 2017 +0200
1.3 @@ -222,12 +222,11 @@
1.4
1.5  lemma is_field: "field R"
1.6  proof -
1.7 -  have "gcd x (int p) \<noteq> 1 \<Longrightarrow> 0 \<le> x \<Longrightarrow> x < int p \<Longrightarrow> x = 0" for x
1.8 -    by (metis dual_order.order_iff_strict gcd.commute less_le_not_le p_prime prime_imp_coprime prime_nat_int_transfer zdvd_imp_le)
1.9 +  have "0 < x \<Longrightarrow> x < int p \<Longrightarrow> coprime (int p) x" for x
1.10 +    by (rule prime_imp_coprime) (auto simp add: zdvd_not_zless)
1.11    then show ?thesis
1.12 -    apply (intro cring.field_intro2 cring)
1.13 -     apply (auto simp add: res_carrier_eq res_one_eq res_zero_eq res_units_eq)
1.14 -    done
1.15 +    by (intro cring.field_intro2 cring)
1.16 +      (auto simp add: res_carrier_eq res_one_eq res_zero_eq res_units_eq ac_simps)
1.17  qed
1.18
1.19  lemma res_prime_units_eq: "Units R = {1..p - 1}"
1.20 @@ -256,7 +255,7 @@
1.22    then have "x \<in> Units R \<longleftrightarrow> x \<in> int ` totatives m'" for x
1.23      unfolding res_units_eq
1.24 -    by (cases x; cases "x = m") (auto simp: totatives_def transfer_int_nat_gcd)
1.25 +    by (cases x; cases "x = m") (auto simp: totatives_def gcd_int_def)
1.26    then have "Units R = int ` totatives m'"
1.27      by blast
1.28    then have "totatives m' = nat ` Units R"
1.29 @@ -293,7 +292,7 @@
1.30    case False
1.31    with assms show ?thesis
1.32      using residues.euler_theorem [of "int m" "int a"] transfer_int_nat_cong
1.33 -    by (auto simp add: residues_def transfer_int_nat_gcd(1)) force
1.34 +    by (auto simp add: residues_def gcd_int_def) force
1.35  qed
1.36
1.37  lemma fermat_theorem:
1.38 @@ -418,7 +417,7 @@
1.39        using that \<open>p\<ge>2\<close> by force
1.40      then show "?L \<subseteq> ?R" by blast
1.41      have "n \<in> ?L" if "n \<in> ?R" for n
1.42 -      using that \<open>p\<ge>2\<close> Set_Interval.transfer_nat_int_set_functions(2) by fastforce
1.43 +      using that \<open>p\<ge>2\<close> by (auto intro: rev_image_eqI [of "int n"])
1.44      then show "?R \<subseteq> ?L" by blast
1.45    qed
1.46    moreover
```