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