author paulson Tue Nov 09 13:59:37 2010 +0000 (2010-11-09) changeset 40461 e876e95588ce parent 40445 65bd37d7d501 child 40462 89ee82ee0e0f
tidied using metis
```     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:
```
```     2.1 --- a/src/HOL/Number_Theory/UniqueFactorization.thy	Mon Nov 08 23:02:20 2010 +0100
2.2 +++ b/src/HOL/Number_Theory/UniqueFactorization.thy	Tue Nov 09 13:59:37 2010 +0000
2.3 @@ -691,14 +691,9 @@
2.4    apply (frule multiplicity_prod_prime_powers_nat [where f = "%x. f(int x)"
2.5      and S = "nat ` S", transferred])
2.6    apply auto
2.7 -  apply (subst prime_int_def [symmetric])
2.8 -  apply auto
2.9 -  apply (subgoal_tac "xb >= 0")
2.10 -  apply force
2.11 -  apply (rule prime_ge_0_int)
2.12 -  apply force
2.13 -  apply (subst transfer_nat_int_set_return_embed)
2.14 -  apply (unfold nat_set_def, auto)
2.15 +  apply (metis prime_int_def)
2.16 +  apply (metis prime_ge_0_int)
2.17 +  apply (metis nat_set_def prime_ge_0_int transfer_nat_int_set_return_embed)
2.18  done
2.19
2.20  lemma multiplicity_distinct_prime_power_nat: "prime (p::nat) \<Longrightarrow> prime q \<Longrightarrow>
2.21 @@ -739,19 +734,13 @@
2.22      "0 < (y::nat) \<Longrightarrow> x dvd y \<Longrightarrow> prime_factors x <= prime_factors y"
2.23    apply (simp only: prime_factors_altdef_nat)
2.24    apply auto
2.25 -  apply (frule dvd_multiplicity_nat)
2.26 -  apply auto
2.27 -(* It is a shame that auto and arith don't get this. *)
2.28 -  apply (erule order_less_le_trans)back
2.29 -  apply assumption
2.30 +  apply (metis dvd_multiplicity_nat le_0_eq neq_zero_eq_gt_zero_nat)
2.31  done
2.32
2.33  lemma dvd_prime_factors_int [intro]:
2.34      "0 < (y::int) \<Longrightarrow> 0 <= x \<Longrightarrow> x dvd y \<Longrightarrow> prime_factors x <= prime_factors y"
2.35    apply (auto simp add: prime_factors_altdef_int)
2.36 -  apply (erule order_less_le_trans)
2.37 -  apply (rule dvd_multiplicity_int)
2.38 -  apply auto
2.39 +  apply (metis dvd_multiplicity_int le_0_eq neq_zero_eq_gt_zero_nat)
2.40  done
2.41
2.42  lemma multiplicity_dvd_nat: "0 < (x::nat) \<Longrightarrow> 0 < y \<Longrightarrow>
2.43 @@ -763,10 +752,8 @@
2.44    apply force
2.45    apply (subst prime_factors_altdef_nat)+
2.46    apply auto
2.47 -(* Again, a shame that auto and arith don't get this. *)
2.48 -  apply (drule_tac x = xa in spec, auto)
2.49 -  apply (rule le_imp_power_dvd)
2.50 -  apply blast
2.51 +  apply (metis gr0I le_0_eq less_not_refl)
2.52 +  apply (metis le_imp_power_dvd)
2.53  done
2.54
2.55  lemma multiplicity_dvd_int: "0 < (x::int) \<Longrightarrow> 0 < y \<Longrightarrow>
2.56 @@ -778,30 +765,18 @@
2.57    apply force
2.58    apply (subst prime_factors_altdef_int)+
2.59    apply auto
2.60 -  apply (rule dvd_power_le)
2.61 -  apply auto
2.62 -  apply (drule_tac x = xa in spec)
2.63 -  apply (erule impE)
2.64 -  apply auto
2.65 +  apply (metis le_imp_power_dvd prime_factors_ge_0_int)
2.66  done
2.67
2.68  lemma multiplicity_dvd'_nat: "(0::nat) < x \<Longrightarrow>
2.69      \<forall>p. prime p \<longrightarrow> multiplicity p x \<le> multiplicity p y \<Longrightarrow> x dvd y"
2.70 -  apply (cases "y = 0")
2.71 -  apply auto
2.72 -  apply (rule multiplicity_dvd_nat, auto)
2.73 -  apply (case_tac "prime p")
2.74 -  apply auto
2.75 -done
2.76 +by (metis gcd_lcm_complete_lattice_nat.top_greatest le_refl multiplicity_dvd_nat
2.77 +          multiplicity_nonprime_nat neq0_conv)
2.78
2.79  lemma multiplicity_dvd'_int: "(0::int) < x \<Longrightarrow> 0 <= y \<Longrightarrow>
2.80      \<forall>p. prime p \<longrightarrow> multiplicity p x \<le> multiplicity p y \<Longrightarrow> x dvd y"
2.81 -  apply (cases "y = 0")
2.82 -  apply auto
2.83 -  apply (rule multiplicity_dvd_int, auto)
2.84 -  apply (case_tac "prime p")
2.85 -  apply auto
2.86 -done
2.87 +by (metis eq_imp_le gcd_lcm_complete_lattice_nat.top_greatest int_eq_0_conv multiplicity_dvd_int
2.88 +          multiplicity_nonprime_int nat_int transfer_nat_int_relations(4) zless_le)
2.89
2.90  lemma dvd_multiplicity_eq_nat: "0 < (x::nat) \<Longrightarrow> 0 < y \<Longrightarrow>
2.91      (x dvd y) = (ALL p. multiplicity p x <= multiplicity p y)"
2.92 @@ -820,12 +795,8 @@
2.93    apply (rule dvd_power [where x = p and n = "multiplicity p n"])
2.94    apply (subst (asm) prime_factors_altdef_nat, force)
2.95    apply (rule dvd_setprod)
2.96 -  apply auto
2.97 -  apply (subst prime_factors_altdef_nat)
2.98 -  apply (subst (asm) dvd_multiplicity_eq_nat)
2.99    apply auto
2.100 -  apply (drule spec [where x = p])
2.101 -  apply auto
2.102 +  apply (metis One_nat_def Zero_not_Suc dvd_multiplicity_nat le0 le_antisym multiplicity_not_factor_nat multiplicity_prime_nat)
2.103  done
2.104
2.105  lemma prime_factors_altdef2_int:
```