diff -r 1e29e2666a15 -r e7e54a0b9197 src/HOL/Computational_Algebra/Primes.thy --- a/src/HOL/Computational_Algebra/Primes.thy Sat Nov 11 18:33:35 2017 +0000 +++ b/src/HOL/Computational_Algebra/Primes.thy Sat Nov 11 18:41:08 2017 +0000 @@ -245,9 +245,9 @@ using prime_power_cancel [OF assms] assms by auto lemma prime_power_canonical: - fixes m::nat + fixes m :: nat assumes "prime p" "m > 0" - shows "\k n. \ p dvd n \ m = n * p^k" + shows "\k n. \ p dvd n \ m = n * p ^ k" using \m > 0\ proof (induction m rule: less_induct) case (less m) @@ -381,9 +381,9 @@ (* TODO: Generalise? *) lemma prime_power_mult_nat: - fixes p::nat + fixes p :: nat assumes p: "prime p" and xy: "x * y = p ^ k" - shows "\i j. x = p ^i \ y = p^ j" + shows "\i j. x = p ^ i \ y = p^ j" using xy proof(induct k arbitrary: x y) case 0 thus ?case apply simp by (rule exI[where x="0"], simp) @@ -429,25 +429,10 @@ qed lemma divides_primepow_nat: - fixes p::nat + fixes p :: nat assumes p: "prime p" - shows "d dvd p^k \ (\ i. i \ k \ d = p ^i)" -proof - assume H: "d dvd p^k" then obtain e where e: "d*e = p^k" - unfolding dvd_def apply (auto simp add: mult.commute) by blast - from prime_power_mult_nat[OF p e] obtain i j where ij: "d = p^i" "e=p^j" by blast - from e ij have "p^(i + j) = p^k" by (simp add: power_add) - hence "i + j = k" using p prime_gt_1_nat power_inject_exp[of p "i+j" k] by simp - hence "i \ k" by arith - with ij(1) show "\i\k. d = p ^ i" by blast -next - {fix i assume H: "i \ k" "d = p^i" - then obtain j where j: "k = i + j" - by (metis le_add_diff_inverse) - hence "p^k = p^j*d" using H(2) by (simp add: power_add) - hence "d dvd p^k" unfolding dvd_def by auto} - thus "\i\k. d = p ^ i \ d dvd p ^ k" by blast -qed + shows "d dvd p ^ k \ (\i\k. d = p ^ i)" + using assms divides_primepow [of p d k] by (auto intro: le_imp_power_dvd) subsection \Chinese Remainder Theorem Variants\ @@ -481,8 +466,8 @@ from bezout_add_strong_nat[OF a, of b] bezout_add_strong_nat[OF b, of a] obtain d1 x1 y1 d2 x2 y2 where dxy1: "d1 dvd a" "d1 dvd b" "a * x1 = b * y1 + d1" and dxy2: "d2 dvd b" "d2 dvd a" "b * x2 = a * y2 + d2" by blast - then have d12: "d1 = 1" "d2 =1" - by (metis ab coprime_nat)+ + then have d12: "d1 = 1" "d2 = 1" + using ab coprime_common_divisor_nat [of a b] by blast+ let ?x = "v * a * x1 + u * b * x2" let ?q1 = "v * x1 + u * y2" let ?q2 = "v * y1 + u * x2" @@ -497,14 +482,14 @@ lemma coprime_bezout_strong: fixes a::nat assumes "coprime a b" "b \ 1" shows "\x y. a * x = b * y + 1" -by (metis assms bezout_nat gcd_nat.left_neutral) + 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) lemma bezout_prime: assumes p: "prime p" and pa: "\ p dvd a" shows "\x y. a*x = Suc (p*y)" proof - have ap: "coprime a p" - by (metis gcd.commute p pa prime_imp_coprime) + using coprime_commute p pa prime_imp_coprime by auto moreover from p have "p \ 1" by auto ultimately have "\x y. a * x = p * y + 1" by (rule coprime_bezout_strong)