src/HOL/Number_Theory/Primes.thy
changeset 40461 e876e95588ce
parent 37765 26bdfb7b680b
child 44821 a92f65e174cf
     1.1 --- a/src/HOL/Number_Theory/Primes.thy	Mon Nov 08 23:02:20 2010 +0100
     1.2 +++ b/src/HOL/Number_Theory/Primes.thy	Tue Nov 09 13:59:37 2010 +0000
     1.3 @@ -88,11 +88,7 @@
     1.4  
     1.5  lemma prime_odd_nat: "prime (p::nat) \<Longrightarrow> p > 2 \<Longrightarrow> odd p"
     1.6    unfolding prime_nat_def
     1.7 -  apply (subst even_mult_two_ex)
     1.8 -  apply clarify
     1.9 -  apply (drule_tac x = 2 in spec)
    1.10 -  apply auto
    1.11 -done
    1.12 +  by (metis gcd_lcm_complete_lattice_nat.bot_least nat_even_iff_2_dvd nat_neq_iff odd_1_nat)
    1.13  
    1.14  lemma prime_odd_int: "prime (p::int) \<Longrightarrow> p > 2 \<Longrightarrow> odd p"
    1.15    unfolding prime_int_def
    1.16 @@ -275,10 +271,8 @@
    1.17  
    1.18  lemma primes_coprime_int: "prime (p::int) \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> coprime p q"
    1.19    apply (rule prime_imp_coprime_int, assumption)
    1.20 -  apply (unfold prime_int_altdef, clarify)
    1.21 -  apply (drule_tac x = q in spec)
    1.22 -  apply (drule_tac x = p in spec)
    1.23 -  apply auto
    1.24 +  apply (unfold prime_int_altdef)
    1.25 +  apply (metis int_one_le_iff_zero_less zless_le)
    1.26  done
    1.27  
    1.28  lemma primes_imp_powers_coprime_nat: "prime (p::nat) \<Longrightarrow> prime q \<Longrightarrow> p ~= q \<Longrightarrow> coprime (p^m) (q^n)"
    1.29 @@ -291,11 +285,8 @@
    1.30    apply (induct n rule: nat_less_induct)
    1.31    apply (case_tac "n = 0")
    1.32    using two_is_prime_nat apply blast
    1.33 -  apply (case_tac "prime n")
    1.34 -  apply blast
    1.35 -  apply (subgoal_tac "n > 1")
    1.36 -  apply (frule (1) not_prime_eq_prod_nat)
    1.37 -  apply (auto intro: dvd_mult dvd_mult2)
    1.38 +  apply (metis One_nat_def dvd.order_trans dvd_refl less_Suc0 linorder_neqE_nat nat_dvd_not_less 
    1.39 +               neq0_conv prime_nat_def)
    1.40  done
    1.41  
    1.42  (* An Isar version: