src/HOL/Computational_Algebra/Primes.thy
changeset 67051 e7e54a0b9197
parent 66837 6ba663ff2b1c
child 67091 1393c2340eec
     1.1 --- a/src/HOL/Computational_Algebra/Primes.thy	Sat Nov 11 18:33:35 2017 +0000
     1.2 +++ b/src/HOL/Computational_Algebra/Primes.thy	Sat Nov 11 18:41:08 2017 +0000
     1.3 @@ -245,9 +245,9 @@
     1.4    using prime_power_cancel [OF assms] assms by auto
     1.5  
     1.6  lemma prime_power_canonical:
     1.7 -  fixes m::nat
     1.8 +  fixes m :: nat
     1.9    assumes "prime p" "m > 0"
    1.10 -  shows "\<exists>k n. \<not> p dvd n \<and> m = n * p^k"
    1.11 +  shows "\<exists>k n. \<not> p dvd n \<and> m = n * p ^ k"
    1.12  using \<open>m > 0\<close>
    1.13  proof (induction m rule: less_induct)
    1.14    case (less m)
    1.15 @@ -381,9 +381,9 @@
    1.16  
    1.17  (* TODO: Generalise? *)
    1.18  lemma prime_power_mult_nat:
    1.19 -  fixes p::nat
    1.20 +  fixes p :: nat
    1.21    assumes p: "prime p" and xy: "x * y = p ^ k"
    1.22 -  shows "\<exists>i j. x = p ^i \<and> y = p^ j"
    1.23 +  shows "\<exists>i j. x = p ^ i \<and> y = p^ j"
    1.24  using xy
    1.25  proof(induct k arbitrary: x y)
    1.26    case 0 thus ?case apply simp by (rule exI[where x="0"], simp)
    1.27 @@ -429,25 +429,10 @@
    1.28  qed
    1.29  
    1.30  lemma divides_primepow_nat:
    1.31 -  fixes p::nat
    1.32 +  fixes p :: nat
    1.33    assumes p: "prime p"
    1.34 -  shows "d dvd p^k \<longleftrightarrow> (\<exists> i. i \<le> k \<and> d = p ^i)"
    1.35 -proof
    1.36 -  assume H: "d dvd p^k" then obtain e where e: "d*e = p^k"
    1.37 -    unfolding dvd_def  apply (auto simp add: mult.commute) by blast
    1.38 -  from prime_power_mult_nat[OF p e] obtain i j where ij: "d = p^i" "e=p^j" by blast
    1.39 -  from e ij have "p^(i + j) = p^k" by (simp add: power_add)
    1.40 -  hence "i + j = k" using p prime_gt_1_nat power_inject_exp[of p "i+j" k] by simp
    1.41 -  hence "i \<le> k" by arith
    1.42 -  with ij(1) show "\<exists>i\<le>k. d = p ^ i" by blast
    1.43 -next
    1.44 -  {fix i assume H: "i \<le> k" "d = p^i"
    1.45 -    then obtain j where j: "k = i + j"
    1.46 -      by (metis le_add_diff_inverse)
    1.47 -    hence "p^k = p^j*d" using H(2) by (simp add: power_add)
    1.48 -    hence "d dvd p^k" unfolding dvd_def by auto}
    1.49 -  thus "\<exists>i\<le>k. d = p ^ i \<Longrightarrow> d dvd p ^ k" by blast
    1.50 -qed
    1.51 +  shows "d dvd p ^ k \<longleftrightarrow> (\<exists>i\<le>k. d = p ^ i)"
    1.52 +  using assms divides_primepow [of p d k] by (auto intro: le_imp_power_dvd)
    1.53  
    1.54  
    1.55  subsection \<open>Chinese Remainder Theorem Variants\<close>
    1.56 @@ -481,8 +466,8 @@
    1.57    from bezout_add_strong_nat[OF a, of b] bezout_add_strong_nat[OF b, of a]
    1.58    obtain d1 x1 y1 d2 x2 y2 where dxy1: "d1 dvd a" "d1 dvd b" "a * x1 = b * y1 + d1"
    1.59      and dxy2: "d2 dvd b" "d2 dvd a" "b * x2 = a * y2 + d2" by blast
    1.60 -  then have d12: "d1 = 1" "d2 =1"
    1.61 -    by (metis ab coprime_nat)+
    1.62 +  then have d12: "d1 = 1" "d2 = 1"
    1.63 +    using ab coprime_common_divisor_nat [of a b] by blast+
    1.64    let ?x = "v * a * x1 + u * b * x2"
    1.65    let ?q1 = "v * x1 + u * y2"
    1.66    let ?q2 = "v * y1 + u * x2"
    1.67 @@ -497,14 +482,14 @@
    1.68  lemma coprime_bezout_strong:
    1.69    fixes a::nat assumes "coprime a b"  "b \<noteq> 1"
    1.70    shows "\<exists>x y. a * x = b * y + 1"
    1.71 -by (metis assms bezout_nat gcd_nat.left_neutral)
    1.72 +  by (metis add.commute add.right_neutral assms(1) assms(2) chinese_remainder coprime_1_left coprime_1_right coprime_crossproduct_nat mult.commute mult.right_neutral mult_cancel_left)
    1.73  
    1.74  lemma bezout_prime:
    1.75    assumes p: "prime p" and pa: "\<not> p dvd a"
    1.76    shows "\<exists>x y. a*x = Suc (p*y)"
    1.77  proof -
    1.78    have ap: "coprime a p"
    1.79 -    by (metis gcd.commute p pa prime_imp_coprime)
    1.80 +    using coprime_commute p pa prime_imp_coprime by auto
    1.81    moreover from p have "p \<noteq> 1" by auto
    1.82    ultimately have "\<exists>x y. a * x = p * y + 1"
    1.83      by (rule coprime_bezout_strong)