src/HOL/Number_Theory/UniqueFactorization.thy
changeset 40461 e876e95588ce
parent 39302 d7728f65b353
child 41413 64cd30d6b0b8
     1.1 --- a/src/HOL/Number_Theory/UniqueFactorization.thy	Mon Nov 08 23:02:20 2010 +0100
     1.2 +++ b/src/HOL/Number_Theory/UniqueFactorization.thy	Tue Nov 09 13:59:37 2010 +0000
     1.3 @@ -691,14 +691,9 @@
     1.4    apply (frule multiplicity_prod_prime_powers_nat [where f = "%x. f(int x)" 
     1.5      and S = "nat ` S", transferred])
     1.6    apply auto
     1.7 -  apply (subst prime_int_def [symmetric])
     1.8 -  apply auto
     1.9 -  apply (subgoal_tac "xb >= 0")
    1.10 -  apply force
    1.11 -  apply (rule prime_ge_0_int)
    1.12 -  apply force
    1.13 -  apply (subst transfer_nat_int_set_return_embed)
    1.14 -  apply (unfold nat_set_def, auto)
    1.15 +  apply (metis prime_int_def)
    1.16 +  apply (metis prime_ge_0_int)
    1.17 +  apply (metis nat_set_def prime_ge_0_int transfer_nat_int_set_return_embed)
    1.18  done
    1.19  
    1.20  lemma multiplicity_distinct_prime_power_nat: "prime (p::nat) \<Longrightarrow> prime q \<Longrightarrow>
    1.21 @@ -739,19 +734,13 @@
    1.22      "0 < (y::nat) \<Longrightarrow> x dvd y \<Longrightarrow> prime_factors x <= prime_factors y"
    1.23    apply (simp only: prime_factors_altdef_nat)
    1.24    apply auto
    1.25 -  apply (frule dvd_multiplicity_nat)
    1.26 -  apply auto
    1.27 -(* It is a shame that auto and arith don't get this. *)
    1.28 -  apply (erule order_less_le_trans)back
    1.29 -  apply assumption
    1.30 +  apply (metis dvd_multiplicity_nat le_0_eq neq_zero_eq_gt_zero_nat)
    1.31  done
    1.32  
    1.33  lemma dvd_prime_factors_int [intro]:
    1.34      "0 < (y::int) \<Longrightarrow> 0 <= x \<Longrightarrow> x dvd y \<Longrightarrow> prime_factors x <= prime_factors y"
    1.35    apply (auto simp add: prime_factors_altdef_int)
    1.36 -  apply (erule order_less_le_trans)
    1.37 -  apply (rule dvd_multiplicity_int)
    1.38 -  apply auto
    1.39 +  apply (metis dvd_multiplicity_int le_0_eq neq_zero_eq_gt_zero_nat)
    1.40  done
    1.41  
    1.42  lemma multiplicity_dvd_nat: "0 < (x::nat) \<Longrightarrow> 0 < y \<Longrightarrow> 
    1.43 @@ -763,10 +752,8 @@
    1.44    apply force
    1.45    apply (subst prime_factors_altdef_nat)+
    1.46    apply auto
    1.47 -(* Again, a shame that auto and arith don't get this. *)
    1.48 -  apply (drule_tac x = xa in spec, auto)
    1.49 -  apply (rule le_imp_power_dvd)
    1.50 -  apply blast
    1.51 +  apply (metis gr0I le_0_eq less_not_refl)
    1.52 +  apply (metis le_imp_power_dvd)
    1.53  done
    1.54  
    1.55  lemma multiplicity_dvd_int: "0 < (x::int) \<Longrightarrow> 0 < y \<Longrightarrow> 
    1.56 @@ -778,30 +765,18 @@
    1.57    apply force
    1.58    apply (subst prime_factors_altdef_int)+
    1.59    apply auto
    1.60 -  apply (rule dvd_power_le)
    1.61 -  apply auto
    1.62 -  apply (drule_tac x = xa in spec)
    1.63 -  apply (erule impE)
    1.64 -  apply auto
    1.65 +  apply (metis le_imp_power_dvd prime_factors_ge_0_int)
    1.66  done
    1.67  
    1.68  lemma multiplicity_dvd'_nat: "(0::nat) < x \<Longrightarrow> 
    1.69      \<forall>p. prime p \<longrightarrow> multiplicity p x \<le> multiplicity p y \<Longrightarrow> x dvd y"
    1.70 -  apply (cases "y = 0")
    1.71 -  apply auto
    1.72 -  apply (rule multiplicity_dvd_nat, auto)
    1.73 -  apply (case_tac "prime p")
    1.74 -  apply auto
    1.75 -done
    1.76 +by (metis gcd_lcm_complete_lattice_nat.top_greatest le_refl multiplicity_dvd_nat
    1.77 +          multiplicity_nonprime_nat neq0_conv)
    1.78  
    1.79  lemma multiplicity_dvd'_int: "(0::int) < x \<Longrightarrow> 0 <= y \<Longrightarrow>
    1.80      \<forall>p. prime p \<longrightarrow> multiplicity p x \<le> multiplicity p y \<Longrightarrow> x dvd y"
    1.81 -  apply (cases "y = 0")
    1.82 -  apply auto
    1.83 -  apply (rule multiplicity_dvd_int, auto)
    1.84 -  apply (case_tac "prime p")
    1.85 -  apply auto
    1.86 -done
    1.87 +by (metis eq_imp_le gcd_lcm_complete_lattice_nat.top_greatest int_eq_0_conv multiplicity_dvd_int
    1.88 +          multiplicity_nonprime_int nat_int transfer_nat_int_relations(4) zless_le)
    1.89  
    1.90  lemma dvd_multiplicity_eq_nat: "0 < (x::nat) \<Longrightarrow> 0 < y \<Longrightarrow>
    1.91      (x dvd y) = (ALL p. multiplicity p x <= multiplicity p y)"
    1.92 @@ -820,12 +795,8 @@
    1.93    apply (rule dvd_power [where x = p and n = "multiplicity p n"])
    1.94    apply (subst (asm) prime_factors_altdef_nat, force)
    1.95    apply (rule dvd_setprod)
    1.96 -  apply auto  
    1.97 -  apply (subst prime_factors_altdef_nat)
    1.98 -  apply (subst (asm) dvd_multiplicity_eq_nat)
    1.99    apply auto
   1.100 -  apply (drule spec [where x = p])
   1.101 -  apply auto
   1.102 +  apply (metis One_nat_def Zero_not_Suc dvd_multiplicity_nat le0 le_antisym multiplicity_not_factor_nat multiplicity_prime_nat)  
   1.103  done
   1.104  
   1.105  lemma prime_factors_altdef2_int: