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.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.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.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.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.42  (* An Isar version: