src/HOL/Number_Theory/UniqueFactorization.thy
 changeset 41541 1fa4725c4656 parent 41413 64cd30d6b0b8 child 41959 b460124855b8
```     1.1 --- a/src/HOL/Number_Theory/UniqueFactorization.thy	Thu Jan 13 21:50:13 2011 +0100
1.2 +++ b/src/HOL/Number_Theory/UniqueFactorization.thy	Thu Jan 13 23:50:16 2011 +0100
1.3 @@ -1,12 +1,11 @@
1.4  (*  Title:      UniqueFactorization.thy
1.5      Author:     Jeremy Avigad
1.6
1.7 -
1.8 -    Unique factorization for the natural numbers and the integers.
1.9 +Unique factorization for the natural numbers and the integers.
1.10
1.11 -    Note: there were previous Isabelle formalizations of unique
1.12 -    factorization due to Thomas Marthedal Rasmussen, and, building on
1.13 -    that, by Jeremy Avigad and David Gray.
1.14 +Note: there were previous Isabelle formalizations of unique
1.15 +factorization due to Thomas Marthedal Rasmussen, and, building on
1.16 +that, by Jeremy Avigad and David Gray.
1.17  *)
1.18
1.19  header {* UniqueFactorization *}
1.20 @@ -135,14 +134,13 @@
1.21    moreover
1.22    {
1.23      assume "n > 1" and "~ prime n"
1.24 -    from prems not_prime_eq_prod_nat
1.25 -      obtain m k where "n = m * k & 1 < m & m < n & 1 < k & k < n"
1.26 +    with not_prime_eq_prod_nat obtain m k where n: "n = m * k & 1 < m & m < n & 1 < k & k < n"
1.27          by blast
1.28      with ih obtain Q R where "(ALL p : set_of Q. prime p) & m = (PROD i:#Q. i)"
1.29          and "(ALL p: set_of R. prime p) & k = (PROD i:#R. i)"
1.30        by blast
1.31      hence "(ALL p: set_of (Q + R). prime p) & n = (PROD i :# Q + R. i)"
1.32 -      by (auto simp add: prems msetprod_Un set_of_union)
1.33 +      by (auto simp add: n msetprod_Un)
1.34      then have "EX M. (ALL p : set_of M. prime p) & n = (PROD i :# M. i)"..
1.35    }
1.36    ultimately show "EX M. (ALL p : set_of M. prime p) & n = (PROD i::nat:#M. i)"
1.37 @@ -157,13 +155,11 @@
1.38    shows
1.39      "count M a <= count N a"
1.40  proof cases
1.41 -  assume "a : set_of M"
1.42 -  with prems have a: "prime a"
1.43 -    by auto
1.44 -  with prems have "a ^ count M a dvd (PROD i :# M. i)"
1.45 +  assume M: "a : set_of M"
1.46 +  with assms have a: "prime a" by auto
1.47 +  with M have "a ^ count M a dvd (PROD i :# M. i)"
1.48      by (auto intro: dvd_setprod simp add: msetprod_def)
1.49 -  also have "... dvd (PROD i :# N. i)"
1.50 -    by (rule prems)
1.51 +  also have "... dvd (PROD i :# N. i)" by (rule assms)
1.52    also have "... = (PROD i : (set_of N). i ^ (count N i))"
1.53      by (simp add: msetprod_def)
1.54    also have "... =
1.55 @@ -186,7 +182,8 @@
1.56      apply (subst gcd_commute_nat)
1.57      apply (rule setprod_coprime_nat)
1.58      apply (rule primes_imp_powers_coprime_nat)
1.59 -    apply (insert prems, auto)
1.60 +    using assms M
1.61 +    apply auto
1.62      done
1.63    ultimately have "a ^ count M a dvd a^(count N a)"
1.64      by (elim coprime_dvd_mult_nat)
1.65 @@ -206,9 +203,9 @@
1.66  proof -
1.67    {
1.68      fix a
1.69 -    from prems have "count M a <= count N a"
1.70 +    from assms have "count M a <= count N a"
1.71        by (intro multiset_prime_factorization_unique_aux, auto)
1.72 -    moreover from prems have "count N a <= count M a"
1.73 +    moreover from assms have "count N a <= count M a"
1.74        by (intro multiset_prime_factorization_unique_aux, auto)
1.75      ultimately have "count M a = count N a"
1.76        by auto
1.77 @@ -245,7 +242,6 @@
1.78  (* definitions for the natural numbers *)
1.79
1.80  instantiation nat :: unique_factorization
1.81 -
1.82  begin
1.83
1.84  definition
1.85 @@ -265,7 +261,6 @@
1.86  (* definitions for the integers *)
1.87
1.88  instantiation int :: unique_factorization
1.89 -
1.90  begin
1.91
1.92  definition
1.93 @@ -329,15 +324,14 @@
1.94    apply (case_tac "n = 0")
1.95    apply (simp add: prime_factors_nat_def multiset_prime_factorization_def)
1.96    apply (auto simp add: prime_factors_nat_def multiset_prime_factorization)
1.97 -done
1.98 +  done
1.99
1.100  lemma prime_factors_prime_int [intro]:
1.101    assumes "n >= 0" and "p : prime_factors (n::int)"
1.102    shows "prime p"
1.103 -
1.104    apply (rule prime_factors_prime_nat [transferred, of n p])
1.105 -  using prems apply auto
1.106 -done
1.107 +  using assms apply auto
1.108 +  done
1.109
1.110  lemma prime_factors_gt_0_nat [elim]: "p : prime_factors x \<Longrightarrow> p > (0::nat)"
1.111    by (frule prime_factors_prime_nat, auto)
1.112 @@ -361,22 +355,19 @@
1.113    apply (unfold prime_factors_int_def multiplicity_int_def)
1.114    apply (subst prime_factors_altdef_nat)
1.115    apply (auto simp add: image_def)
1.116 -done
1.117 +  done
1.118
1.119  lemma prime_factorization_nat: "(n::nat) > 0 \<Longrightarrow>
1.120      n = (PROD p : prime_factors n. p^(multiplicity p n))"
1.121    by (frule multiset_prime_factorization,
1.122      simp add: prime_factors_nat_def multiplicity_nat_def msetprod_def)
1.123
1.124 -thm prime_factorization_nat [transferred]
1.125 -
1.126  lemma prime_factorization_int:
1.127    assumes "(n::int) > 0"
1.128    shows "n = (PROD p : prime_factors n. p^(multiplicity p n))"
1.129 -
1.130    apply (rule prime_factorization_nat [transferred, of n])
1.131 -  using prems apply auto
1.132 -done
1.133 +  using assms apply auto
1.134 +  done
1.135
1.136  lemma neq_zero_eq_gt_zero_nat: "((x::nat) ~= 0) = (x > 0)"
1.137    by auto
1.138 @@ -591,10 +582,9 @@
1.139    shows
1.140      "(prime_factors k) Un (prime_factors l) = prime_factors (k * l) &
1.141      (ALL p >= 0. multiplicity p k + multiplicity p l = multiplicity p (k * l))"
1.142 -
1.143    apply (rule multiplicity_product_aux_nat [transferred, of l k])
1.144 -  using prems apply auto
1.145 -done
1.146 +  using assms apply auto
1.147 +  done
1.148
1.149  lemma prime_factors_product_nat: "(k::nat) > 0 \<Longrightarrow> l > 0 \<Longrightarrow> prime_factors (k * l) =
1.150      prime_factors k Un prime_factors l"
1.151 @@ -805,9 +795,9 @@
1.152
1.153    apply (case_tac "p >= 0")
1.154    apply (rule prime_factors_altdef2_nat [transferred])
1.155 -  using prems apply auto
1.156 +  using assms apply auto
1.157    apply (auto simp add: prime_ge_0_int prime_factors_ge_0_int)
1.158 -done
1.159 +  done
1.160
1.161  lemma multiplicity_eq_nat:
1.162    fixes x and y::nat
1.163 @@ -846,7 +836,7 @@
1.164        min (multiplicity p x) (multiplicity p y)"
1.165      unfolding z_def
1.166      apply (subst multiplicity_prod_prime_powers_nat)
1.167 -    apply (auto simp add: multiplicity_not_factor_nat)
1.168 +    apply auto
1.169      done
1.170    have "z dvd x"
1.171      by (intro multiplicity_dvd'_nat, auto simp add: aux)
1.172 @@ -878,7 +868,7 @@
1.173        max (multiplicity p x) (multiplicity p y)"
1.174      unfolding z_def
1.175      apply (subst multiplicity_prod_prime_powers_nat)
1.176 -    apply (auto simp add: multiplicity_not_factor_nat)
1.177 +    apply auto
1.178      done
1.179    have "x dvd z"
1.180      by (intro multiplicity_dvd'_nat, auto simp add: aux)
```