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.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.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)
```