src/HOL/Number_Theory/Gauss.thy
 changeset 67051 e7e54a0b9197 parent 66888 930abfdf8727 child 67091 1393c2340eec
```     1.1 --- a/src/HOL/Number_Theory/Gauss.thy	Sat Nov 11 18:33:35 2017 +0000
1.2 +++ b/src/HOL/Number_Theory/Gauss.thy	Sat Nov 11 18:41:08 2017 +0000
1.3 @@ -115,8 +115,9 @@
1.4    proof -
1.5      from p_a_relprime have "\<not> p dvd a"
1.7 -    with p_prime have "coprime a (int p)"
1.8 -      by (subst gcd.commute, intro prime_imp_coprime) auto
1.9 +    with p_prime prime_imp_coprime [of _ "nat \<bar>a\<bar>"]
1.10 +    have "coprime a (int p)"
1.11 +      by (simp_all add: zdvd_int ac_simps)
1.12      with a cong_mult_rcancel_int [of a "int p" x y] have "[x = y] (mod p)"
1.13        by simp
1.14      with cong_less_imp_eq_int [of x y p] p_minus_one_l
1.15 @@ -149,8 +150,9 @@
1.16        using cong_def by blast
1.17      from p_a_relprime have "\<not>p dvd a"
1.19 -    with p_prime have "coprime a (int p)"
1.20 -      by (subst gcd.commute, intro prime_imp_coprime) auto
1.21 +    with p_prime prime_imp_coprime [of _ "nat \<bar>a\<bar>"]
1.22 +    have "coprime a (int p)"
1.23 +      by (simp_all add: zdvd_int ac_simps)
1.24      with a' cong_mult_rcancel_int [of a "int p" x y]
1.25      have "[x = y] (mod p)" by simp
1.26      with cong_less_imp_eq_int [of x y p] p_minus_one_l
1.27 @@ -219,13 +221,16 @@
1.28    by (auto simp add: D_def C_def B_def A_def)
1.29
1.30  lemma all_A_relprime:
1.31 -  assumes "x \<in> A"
1.32 -  shows "gcd x p = 1"
1.33 -  using p_prime A_ncong_p [OF assms]
1.34 -  by (auto simp: cong_altdef_int gcd.commute[of _ "int p"] intro!: prime_imp_coprime)
1.35 -
1.36 -lemma A_prod_relprime: "gcd (prod id A) p = 1"
1.37 -  by (metis id_def all_A_relprime prod_coprime)
1.38 +  "coprime x p" if "x \<in> A"
1.39 +proof -
1.40 +  from A_ncong_p [OF that] have "\<not> int p dvd x"
1.41 +    by (simp add: cong_altdef_int)
1.42 +  with p_prime show ?thesis
1.43 +    by (metis (no_types) coprime_commute prime_imp_coprime prime_nat_int_transfer)
1.44 +qed
1.45 +
1.46 +lemma A_prod_relprime: "coprime (prod id A) p"
1.47 +  by (auto intro: prod_coprime_left all_A_relprime)
1.48
1.49
1.50  subsection \<open>Relationships Between Gauss Sets\<close>
```