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)