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.21      by (simp_all add: m'_def)
    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