src/HOL/Number_Theory/Primes.thy
 changeset 62349 7c23469b5118 parent 62348 9a5f43dac883 child 62410 2fc7a8d9c529
```     1.1 --- a/src/HOL/Number_Theory/Primes.thy	Wed Feb 17 21:51:57 2016 +0100
1.2 +++ b/src/HOL/Number_Theory/Primes.thy	Wed Feb 17 21:51:57 2016 +0100
1.3 @@ -167,14 +167,19 @@
1.4      "prime p \<Longrightarrow> prime q \<Longrightarrow> p ~= q \<Longrightarrow> coprime (p^m) (q^n)"
1.5    by (rule coprime_exp2_nat, rule primes_coprime_nat)
1.6
1.7 -lemma prime_factor_nat: "n \<noteq> (1::nat) \<Longrightarrow> \<exists> p. prime p \<and> p dvd n"
1.8 -  apply (induct n rule: nat_less_induct)
1.9 -  apply (case_tac "n = 0")
1.10 -  using two_is_prime_nat
1.11 -  apply blast
1.12 -  apply (metis One_nat_def dvd.order_trans dvd_refl less_Suc0 linorder_neqE_nat
1.13 -    nat_dvd_not_less neq0_conv prime_def)
1.14 -  done
1.15 +lemma prime_factor_nat:
1.16 +  "n \<noteq> (1::nat) \<Longrightarrow> \<exists>p. prime p \<and> p dvd n"
1.17 +proof (induct n rule: nat_less_induct)
1.18 +  case (1 n) show ?case
1.19 +  proof (cases "n = 0")
1.20 +    case True then show ?thesis
1.21 +    by (auto intro: two_is_prime_nat)
1.22 +  next
1.23 +    case False with "1.prems" have "n > 1" by simp
1.24 +    with "1.hyps" show ?thesis
1.25 +    by (metis One_nat_def dvd_mult dvd_refl not_prime_eq_prod_nat order_less_irrefl)
1.26 +  qed
1.27 +qed
1.28
1.29  text \<open>One property of coprimality is easier to prove via prime factors.\<close>
1.30
1.31 @@ -417,11 +422,13 @@
1.32  lemma bezout_prime:
1.33    assumes p: "prime p" and pa: "\<not> p dvd a"
1.34    shows "\<exists>x y. a*x = Suc (p*y)"
1.35 -proof-
1.36 +proof -
1.37    have ap: "coprime a p"
1.38      by (metis gcd.commute p pa prime_imp_coprime_nat)
1.39 -  from coprime_bezout_strong[OF ap] show ?thesis
1.40 -    by (metis Suc_eq_plus1 gcd_lcm_complete_lattice_nat.bot.extremum pa)
1.41 +  moreover from p have "p \<noteq> 1" by auto
1.42 +  ultimately have "\<exists>x y. a * x = p * y + 1"
1.43 +    by (rule coprime_bezout_strong)
1.44 +  then show ?thesis by simp
1.45  qed
1.46
1.47  end
```