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.6        by (simp add: cong_altdef_int)
     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.18        by (simp add: cong_altdef_int)
    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>