Overhaul of prime/multiplicity/prime_factors
authoreberlm <eberlm@in.tum.de>
Thu Jul 21 10:06:04 2016 +0200 (2016-07-21)
changeset 63534523b488b15c9
parent 63525 f01d1e393f3f
child 63535 6887fda4541a
Overhaul of prime/multiplicity/prime_factors
src/HOL/Algebra/Exponent.thy
src/HOL/Algebra/IntRing.thy
src/HOL/Algebra/Sylow.thy
src/HOL/Library/Multiset.thy
src/HOL/Nonstandard_Analysis/Examples/NSPrimes.thy
src/HOL/Number_Theory/Eratosthenes.thy
src/HOL/Number_Theory/Factorial_Ring.thy
src/HOL/Number_Theory/Gauss.thy
src/HOL/Number_Theory/Pocklington.thy
src/HOL/Number_Theory/Primes.thy
src/HOL/Number_Theory/Residues.thy
src/HOL/Number_Theory/UniqueFactorization.thy
src/HOL/Proofs/Extraction/Euclid.thy
src/HOL/ex/Sqrt.thy
src/HOL/ex/Sqrt_Script.thy
     1.1 --- a/src/HOL/Algebra/Exponent.thy	Wed Jul 20 14:52:09 2016 +0200
     1.2 +++ b/src/HOL/Algebra/Exponent.thy	Thu Jul 21 10:06:04 2016 +0200
     1.3 @@ -22,17 +22,17 @@
     1.4  proof -
     1.5    have "p dvd m*n" using dvd_mult_left pk by blast
     1.6    then consider "p dvd m" | "p dvd n"
     1.7 -    using p prime_dvd_mult_eq_nat by blast
     1.8 +    using p is_prime_dvd_mult_iff by blast
     1.9    then show ?thesis
    1.10    proof cases
    1.11      case 1 then obtain a where "m = p * a" by (metis dvd_mult_div_cancel) 
    1.12        then have "\<exists>x. k dvd x * n \<and> m = p * x"
    1.13 -        using p pk by auto
    1.14 +        using p pk by (auto simp: mult.assoc)
    1.15      then show ?thesis ..
    1.16    next
    1.17      case 2 then obtain b where "n = p * b" by (metis dvd_mult_div_cancel) 
    1.18 -      then have "\<exists>y. k dvd m*y \<and> n = p*y"
    1.19 -        using p pk by auto
    1.20 +    with p pk have "\<exists>y. k dvd m*y \<and> n = p*y" 
    1.21 +      by (metis dvd_mult_right dvd_times_left_cancel_iff mult.left_commute mult_zero_left)
    1.22      then show ?thesis ..
    1.23    qed
    1.24  qed
    1.25 @@ -50,11 +50,16 @@
    1.26    then show ?case
    1.27    proof cases
    1.28      case (1 x) 
    1.29 -      with Suc.hyps [of x n] show "\<exists>a b. a + b = Suc c \<and> p ^ a dvd m \<and> p ^ b dvd n"
    1.30 -      by force
    1.31 +    with Suc.hyps[of x n] obtain a b where "a + b = c \<and> p ^ a dvd x \<and> p ^ b dvd n" by blast
    1.32 +    with 1 have "Suc a + b = Suc c \<and> p ^ Suc a dvd m \<and> p ^ b dvd n"
    1.33 +      by (auto intro: mult_dvd_mono)
    1.34 +    thus ?thesis by blast
    1.35    next
    1.36      case (2 y) 
    1.37 -      with Suc.hyps [of m y] show "\<exists>a b. a + b = Suc c \<and> p ^ a dvd m \<and> p ^ b dvd n"
    1.38 +    with Suc.hyps[of m y] obtain a b where "a + b = c \<and> p ^ a dvd m \<and> p ^ b dvd y" by blast
    1.39 +    with 2 have "a + Suc b = Suc c \<and> p ^ a dvd m \<and> p ^ Suc b dvd n"
    1.40 +      by (auto intro: mult_dvd_mono)
    1.41 +    with Suc.hyps [of m y] show "\<exists>a b. a + b = Suc c \<and> p ^ a dvd m \<and> p ^ b dvd n"
    1.42        by force
    1.43    qed
    1.44  qed
    1.45 @@ -73,20 +78,27 @@
    1.46  
    1.47  subsection\<open>The Exponent Function\<close>
    1.48  
    1.49 +abbreviation (input) "exponent \<equiv> multiplicity"
    1.50 +
    1.51 +(*
    1.52  definition
    1.53    exponent :: "nat => nat => nat"
    1.54    where "exponent p s = (if prime p then (GREATEST r. p^r dvd s) else 0)"
    1.55 +*)
    1.56  
    1.57 -lemma exponent_eq_0 [simp]: "\<not> prime p \<Longrightarrow> exponent p s = 0"
    1.58 -  by (simp add: exponent_def)
    1.59 +(*lemma exponent_eq_0 [simp]: "\<not> prime p \<Longrightarrow> exponent p s = 0"
    1.60 +  by (simp add: exponent_def)*)
    1.61  
    1.62  lemma Suc_le_power: "Suc 0 < p \<Longrightarrow> Suc n \<le> p ^ n"
    1.63    by (induct n) (auto simp: Suc_le_eq le_less_trans)
    1.64  
    1.65 +(*
    1.66  text\<open>An upper bound for the @{term n} such that @{term"p^n dvd a"}: needed for GREATEST to exist\<close>
    1.67  lemma power_dvd_bound: "\<lbrakk>p ^ n dvd a; Suc 0 < p; 0 < a\<rbrakk> \<Longrightarrow> n < a"
    1.68    by (meson Suc_le_lessD Suc_le_power dvd_imp_le le_trans)
    1.69 +*)
    1.70  
    1.71 +(*
    1.72  lemma exponent_ge:
    1.73    assumes "p ^ k dvd n" "prime p" "0 < n"
    1.74      shows "k \<le> exponent p n"
    1.75 @@ -96,7 +108,9 @@
    1.76    with assms show ?thesis
    1.77      by (simp add: \<open>prime p\<close> exponent_def) (meson Greatest_le power_dvd_bound)
    1.78  qed
    1.79 +*)
    1.80  
    1.81 +(*
    1.82  lemma power_exponent_dvd: "p ^ exponent p s dvd s"
    1.83  proof (cases "s = 0")
    1.84    case True then show ?thesis by simp
    1.85 @@ -107,27 +121,35 @@
    1.86      apply (auto dest: prime_gt_Suc_0_nat power_dvd_bound)
    1.87      done
    1.88  qed
    1.89 +*)
    1.90  
    1.91 -lemma power_Suc_exponent_Not_dvd:
    1.92 +(*lemma power_Suc_exponent_Not_dvd:
    1.93      "\<lbrakk>p * p ^ exponent p s dvd s; prime p\<rbrakk> \<Longrightarrow> s = 0"
    1.94    by (metis exponent_ge neq0_conv not_less_eq_eq order_refl power_Suc)
    1.95 +*)
    1.96  
    1.97 +
    1.98 +(*
    1.99  lemma exponent_power_eq [simp]: "prime p \<Longrightarrow> exponent p (p ^ a) = a"
   1.100    apply (simp add: exponent_def)
   1.101    apply (rule Greatest_equality, simp)
   1.102    apply (simp add: prime_gt_Suc_0_nat power_dvd_imp_le)
   1.103    done
   1.104 +*)
   1.105  
   1.106 +(*
   1.107  lemma exponent_1_eq_0 [simp]: "exponent p (Suc 0) = 0"
   1.108    apply (case_tac "prime p")
   1.109    apply (metis exponent_power_eq nat_power_eq_Suc_0_iff)
   1.110    apply simp
   1.111    done
   1.112 +*)
   1.113  
   1.114  lemma exponent_equalityI:
   1.115    "(\<And>r. p ^ r dvd a \<longleftrightarrow> p ^ r dvd b) \<Longrightarrow> exponent p a = exponent p b"
   1.116 -  by (simp add: exponent_def)
   1.117 +  by (simp add: multiplicity_def)
   1.118  
   1.119 +(*
   1.120  lemma exponent_mult_add: 
   1.121    assumes "a > 0" "b > 0"
   1.122      shows "exponent p (a * b) = (exponent p a) + (exponent p b)"
   1.123 @@ -149,15 +171,22 @@
   1.124    then show "exponent p (a * b) \<le> exponent p a + exponent p b" by (blast intro: leI)
   1.125    qed
   1.126  qed
   1.127 +*)
   1.128  
   1.129 -lemma not_divides_exponent_0: "~ (p dvd n) \<Longrightarrow> exponent p n = 0"
   1.130 -  apply (case_tac "exponent p n", simp)
   1.131 -  by (metis dvd_mult_left power_Suc power_exponent_dvd)
   1.132 +lemma not_dvd_imp_multiplicity_0: 
   1.133 +  assumes "\<not>p dvd x"
   1.134 +  shows   "multiplicity p x = 0"
   1.135 +proof -
   1.136 +  from assms have "multiplicity p x < 1"
   1.137 +    by (intro multiplicity_lessI) auto
   1.138 +  thus ?thesis by simp
   1.139 +qed
   1.140  
   1.141  
   1.142  subsection\<open>The Main Combinatorial Argument\<close>
   1.143  
   1.144  lemma exponent_p_a_m_k_equation: 
   1.145 +  fixes p :: nat
   1.146    assumes "0 < m" "0 < k" "p \<noteq> 0" "k < p^a" 
   1.147      shows "exponent p (p^a * m - k) = exponent p (p^a - k)"
   1.148  proof (rule exponent_equalityI [OF iffI])
   1.149 @@ -188,60 +217,56 @@
   1.150  qed
   1.151  
   1.152  lemma p_not_div_choose_lemma: 
   1.153 +  fixes p :: nat
   1.154    assumes eeq: "\<And>i. Suc i < K \<Longrightarrow> exponent p (Suc i) = exponent p (Suc (j + i))"
   1.155 -      and "k < K"
   1.156 +      and "k < K" and p: "prime p"
   1.157      shows "exponent p (j + k choose k) = 0"
   1.158 -proof (cases "prime p")
   1.159 -  case False then show ?thesis by simp
   1.160 +  using \<open>k < K\<close>
   1.161 +proof (induction k)
   1.162 +  case 0 then show ?case by simp
   1.163  next
   1.164 -  case True show ?thesis using \<open>k < K\<close> 
   1.165 -  proof (induction k)
   1.166 -    case 0 then show ?case by simp
   1.167 -  next
   1.168 -    case (Suc k)
   1.169 -    then have *: "(Suc (j+k) choose Suc k) > 0" by simp
   1.170 -    then have "exponent p ((Suc (j+k) choose Suc k) * Suc k) = exponent p (Suc k)"
   1.171 -      by (metis Suc.IH Suc.prems Suc_lessD Suc_times_binomial_eq add.comm_neutral eeq exponent_mult_add 
   1.172 -                mult_pos_pos zero_less_Suc zero_less_mult_pos)
   1.173 -    then show ?case
   1.174 -      by (metis * add.commute add_Suc_right add_eq_self_zero exponent_mult_add zero_less_Suc)
   1.175 -  qed
   1.176 +  case (Suc k)
   1.177 +  then have *: "(Suc (j+k) choose Suc k) > 0" by simp
   1.178 +  then have "exponent p ((Suc (j+k) choose Suc k) * Suc k) = exponent p (Suc k)"
   1.179 +    by (subst Suc_times_binomial_eq [symmetric], subst prime_multiplicity_mult_distrib)
   1.180 +       (insert p Suc.prems, simp_all add: eeq [symmetric] Suc.IH)
   1.181 +  with p * show ?case
   1.182 +    by (subst (asm) prime_multiplicity_mult_distrib) simp_all
   1.183  qed
   1.184  
   1.185  text\<open>The lemma above, with two changes of variables\<close>
   1.186  lemma p_not_div_choose:
   1.187    assumes "k < K" and "k \<le> n" 
   1.188 -      and eeq: "\<And>j. \<lbrakk>0<j; j<K\<rbrakk> \<Longrightarrow> exponent p (n - k + (K - j)) = exponent p (K - j)"
   1.189 +      and eeq: "\<And>j. \<lbrakk>0<j; j<K\<rbrakk> \<Longrightarrow> exponent p (n - k + (K - j)) = exponent p (K - j)" "is_prime p"
   1.190      shows "exponent p (n choose k) = 0"
   1.191  apply (rule p_not_div_choose_lemma [of K p "n-k" k, simplified assms nat_minus_add_max max_absorb1])
   1.192  apply (metis add_Suc_right eeq diff_diff_cancel order_less_imp_le zero_less_Suc zero_less_diff)
   1.193 -apply (rule TrueI)
   1.194 +apply (rule TrueI)+
   1.195  done
   1.196  
   1.197  proposition const_p_fac:
   1.198 -  assumes "m>0"
   1.199 -    shows "exponent p (p^a * m choose p^a) = exponent p m"
   1.200 -proof (cases "prime p")
   1.201 -  case False then show ?thesis by auto
   1.202 -next
   1.203 -  case True 
   1.204 -  with assms have p: "0 < p ^ a" "0 < p^a * m" "p^a \<le> p^a * m"
   1.205 +  assumes "m>0" and prime: "is_prime p"
   1.206 +  shows "exponent p (p^a * m choose p^a) = exponent p m"
   1.207 +proof-
   1.208 +  from assms have p: "0 < p ^ a" "0 < p^a * m" "p^a \<le> p^a * m"
   1.209      by (auto simp: prime_gt_0_nat) 
   1.210    have *: "exponent p ((p^a * m - 1) choose (p^a - 1)) = 0"
   1.211      apply (rule p_not_div_choose [where K = "p^a"])
   1.212 -    using p exponent_p_a_m_k_equation by (auto simp: diff_le_mono)
   1.213 +    using p exponent_p_a_m_k_equation by (auto simp: diff_le_mono prime)
   1.214    have "exponent p ((p ^ a * m choose p ^ a) * p ^ a) = a + exponent p m"
   1.215    proof -
   1.216 -    have "p ^ a * m * (p ^ a * m - 1 choose (p ^ a - 1)) = p ^ a * (p ^ a * m choose p ^ a)"
   1.217 -      using p One_nat_def times_binomial_minus1_eq by presburger
   1.218 -    moreover have "exponent p (p ^ a) = a"
   1.219 -      by (meson True exponent_power_eq)
   1.220 -    ultimately show ?thesis
   1.221 -      using * p 
   1.222 -      by (metis (no_types, lifting) One_nat_def exponent_1_eq_0 exponent_mult_add mult.commute mult.right_neutral nat_0_less_mult_iff zero_less_binomial)
   1.223 +    have "(p ^ a * m choose p ^ a) * p ^ a = p ^ a * m * (p ^ a * m - 1 choose (p ^ a - 1))" 
   1.224 +      (is "_ = ?rhs") using prime 
   1.225 +      by (subst times_binomial_minus1_eq [symmetric]) (auto simp: prime_gt_0_nat)
   1.226 +    also from p have "p ^ a - Suc 0 \<le> p ^ a * m - Suc 0" by linarith
   1.227 +    with prime * p have "multiplicity p ?rhs = multiplicity p (p ^ a * m)"
   1.228 +      by (subst prime_multiplicity_mult_distrib) auto
   1.229 +    also have "\<dots> = a + multiplicity p m" 
   1.230 +      using prime p by (subst prime_multiplicity_mult_distrib) simp_all
   1.231 +    finally show ?thesis .
   1.232    qed
   1.233    then show ?thesis
   1.234 -    using True p exponent_mult_add by auto
   1.235 +    using prime p by (subst (asm) prime_multiplicity_mult_distrib) simp_all
   1.236  qed
   1.237  
   1.238  end
     2.1 --- a/src/HOL/Algebra/IntRing.thy	Wed Jul 20 14:52:09 2016 +0200
     2.2 +++ b/src/HOL/Algebra/IntRing.thy	Thu Jul 21 10:06:04 2016 +0200
     2.3 @@ -4,7 +4,7 @@
     2.4  *)
     2.5  
     2.6  theory IntRing
     2.7 -imports QuotRing Lattice Int "~~/src/HOL/Number_Theory/Primes"
     2.8 +imports "~~/src/HOL/Number_Theory/Primes" QuotRing Lattice Int
     2.9  begin
    2.10  
    2.11  section \<open>The Ring of Integers\<close>
    2.12 @@ -240,18 +240,18 @@
    2.13   apply (elim exE)
    2.14  proof -
    2.15    fix a b x
    2.16 -  assume "a * b = x * int p"
    2.17 +  assume "a * b = x * p"
    2.18    then have "p dvd a * b" by simp
    2.19    then have "p dvd a \<or> p dvd b"
    2.20      by (metis prime prime_dvd_mult_eq_int)
    2.21 -  then show "(\<exists>x. a = x * int p) \<or> (\<exists>x. b = x * int p)"
    2.22 +  then show "(\<exists>x. a = x * p) \<or> (\<exists>x. b = x * p)"
    2.23      by (metis dvd_def mult.commute)
    2.24  next
    2.25 -  assume "UNIV = {uu. EX x. uu = x * int p}"
    2.26 -  then obtain x where "1 = x * int p" by best
    2.27 -  then have "\<bar>int p * x\<bar> = 1" by (simp add: mult.commute)
    2.28 -  then show False
    2.29 -    by (metis abs_of_nat of_nat_1 of_nat_eq_iff abs_zmult_eq_1 one_not_prime_nat prime)
    2.30 +  assume "UNIV = {uu. EX x. uu = x * p}"
    2.31 +  then obtain x where "1 = x * p" by best
    2.32 +  then have "\<bar>p * x\<bar> = 1" by (simp add: mult.commute)
    2.33 +  then show False using prime
    2.34 +    by (auto dest!: abs_zmult_eq_1 simp: is_prime_def)
    2.35  qed
    2.36  
    2.37  
     3.1 --- a/src/HOL/Algebra/Sylow.thy	Wed Jul 20 14:52:09 2016 +0200
     3.2 +++ b/src/HOL/Algebra/Sylow.thy	Thu Jul 21 10:06:04 2016 +0200
     3.3 @@ -129,11 +129,15 @@
     3.4  
     3.5  lemma max_p_div_calM:
     3.6       "~ (p ^ Suc(exponent p m) dvd card(calM))"
     3.7 -proof -
     3.8 -  have "exponent p m = exponent p (card calM)"
     3.9 -    by (simp add: card_calM const_p_fac zero_less_m)
    3.10 -  then show ?thesis
    3.11 -    by (metis Suc_n_not_le_n exponent_ge prime_p zero_less_card_calM)
    3.12 +proof
    3.13 +  assume "p ^ Suc (multiplicity p m) dvd card calM"
    3.14 +  with zero_less_card_calM prime_p 
    3.15 +  have "Suc (multiplicity p m) \<le> multiplicity p (card calM)"
    3.16 +    by (intro multiplicity_geI) auto
    3.17 +  hence "multiplicity p m < multiplicity p (card calM)" by simp
    3.18 +  also have "multiplicity p m = multiplicity p (card calM)"
    3.19 +    by (simp add: const_p_fac prime_p zero_less_m card_calM)
    3.20 +  finally show False by simp
    3.21  qed
    3.22  
    3.23  lemma finite_calM: "finite calM"
    3.24 @@ -305,7 +309,7 @@
    3.25  apply (rule dvd_imp_le)
    3.26   apply (rule div_combine [OF prime_p not_dvd_M])
    3.27   prefer 2 apply (blast intro: subgroup.finite_imp_card_positive H_is_subgroup)
    3.28 -apply (simp add: index_lem order_G power_add mult_dvd_mono power_exponent_dvd
    3.29 +apply (simp add: index_lem order_G power_add mult_dvd_mono multiplicity_dvd
    3.30                   zero_less_m)
    3.31  done
    3.32  
     4.1 --- a/src/HOL/Library/Multiset.thy	Wed Jul 20 14:52:09 2016 +0200
     4.2 +++ b/src/HOL/Library/Multiset.thy	Thu Jul 21 10:06:04 2016 +0200
     4.3 @@ -1005,7 +1005,14 @@
     4.4    have "subset_mset.bdd_above A"
     4.5      by (rule ccontr) (insert assms, simp_all add: Sup_multiset_unbounded)
     4.6    with assms show ?thesis by (simp add: in_Sup_multiset_iff)
     4.7 -qed    
     4.8 +qed
     4.9 +
    4.10 +interpretation subset_mset: distrib_lattice "op #\<inter>" "op \<subseteq>#" "op \<subset>#" "op #\<union>"
    4.11 +proof
    4.12 +  fix A B C :: "'a multiset"
    4.13 +  show "A #\<union> (B #\<inter> C) = A #\<union> B #\<inter> (A #\<union> C)"
    4.14 +    by (intro multiset_eqI) simp_all
    4.15 +qed
    4.16  
    4.17  
    4.18  subsubsection \<open>Filter (with comprehension syntax)\<close>
    4.19 @@ -1835,6 +1842,12 @@
    4.20    "setsum f A = msetsum (image_mset f (mset_set A))"
    4.21    by (cases "finite A") (induct A rule: finite_induct, simp_all)
    4.22  
    4.23 +lemma msetsum_delta: "msetsum (image_mset (\<lambda>x. if x = y then c else 0) A) = c * count A y"
    4.24 +  by (induction A) simp_all
    4.25 +
    4.26 +lemma msetsum_delta': "msetsum (image_mset (\<lambda>x. if y = x then c else 0) A) = c * count A y"
    4.27 +  by (induction A) simp_all
    4.28 +
    4.29  end
    4.30  
    4.31  lemma msetsum_diff:
    4.32 @@ -1910,6 +1923,12 @@
    4.33    "msetprod M = setprod (\<lambda>x. x ^ count M x) (set_mset M)"
    4.34    by (simp add: fold_mset_def setprod.eq_fold msetprod.eq_fold funpow_times_power comp_def)
    4.35  
    4.36 +lemma msetprod_delta: "msetprod (image_mset (\<lambda>x. if x = y then c else 1) A) = c ^ count A y"
    4.37 +  by (induction A) (simp_all add: mult_ac)
    4.38 +
    4.39 +lemma msetprod_delta': "msetprod (image_mset (\<lambda>x. if y = x then c else 1) A) = c ^ count A y"
    4.40 +  by (induction A) (simp_all add: mult_ac)
    4.41 +
    4.42  end
    4.43  
    4.44  syntax (ASCII)
     5.1 --- a/src/HOL/Nonstandard_Analysis/Examples/NSPrimes.thy	Wed Jul 20 14:52:09 2016 +0200
     5.2 +++ b/src/HOL/Nonstandard_Analysis/Examples/NSPrimes.thy	Thu Jul 21 10:06:04 2016 +0200
     5.3 @@ -67,7 +67,7 @@
     5.4  (* Goldblatt: Exercise 5.11(3a) - p 57  *)
     5.5  lemma starprime:
     5.6    "starprime = {p. 1 < p & (\<forall>m. m dvd p --> m = 1 | m = p)}"
     5.7 -by (transfer, auto simp add: prime_def)
     5.8 +by (transfer, auto simp add: is_prime_nat_iff)
     5.9  
    5.10  (* Goldblatt Exercise 5.11(3b) - p 57  *)
    5.11  lemma hyperprime_factor_exists [rule_format]:
    5.12 @@ -276,7 +276,8 @@
    5.13  apply clarify
    5.14  apply (subgoal_tac "k \<notin> hypnat_of_nat ` {p. prime p}")
    5.15  apply (force simp add: starprime_def)
    5.16 -apply (metis Compl_iff add.commute dvd_add_left_iff empty_iff hdvd_one_eq_one hypnat_one_not_prime imageE insert_iff mem_Collect_eq zero_not_prime_nat)
    5.17 +  apply (metis Compl_iff add.commute dvd_add_left_iff empty_iff hdvd_one_eq_one hypnat_one_not_prime 
    5.18 +           imageE insert_iff mem_Collect_eq not_is_prime_0)
    5.19  done
    5.20  
    5.21  end
     6.1 --- a/src/HOL/Number_Theory/Eratosthenes.thy	Wed Jul 20 14:52:09 2016 +0200
     6.2 +++ b/src/HOL/Number_Theory/Eratosthenes.thy	Thu Jul 21 10:06:04 2016 +0200
     6.3 @@ -295,8 +295,8 @@
     6.4      from 2 show ?thesis
     6.5        apply (auto simp add: numbers_of_marks_sieve numeral_2_eq_2 set_primes_upto
     6.6          dest: prime_gt_Suc_0_nat)
     6.7 -      apply (metis One_nat_def Suc_le_eq less_not_refl prime_def)
     6.8 -      apply (metis One_nat_def Suc_le_eq aux prime_def)
     6.9 +      apply (metis One_nat_def Suc_le_eq less_not_refl is_prime_nat_iff)
    6.10 +      apply (metis One_nat_def Suc_le_eq aux is_prime_nat_iff)
    6.11        done
    6.12    qed
    6.13  qed
     7.1 --- a/src/HOL/Number_Theory/Factorial_Ring.thy	Wed Jul 20 14:52:09 2016 +0200
     7.2 +++ b/src/HOL/Number_Theory/Factorial_Ring.thy	Thu Jul 21 10:06:04 2016 +0200
     7.3 @@ -7,8 +7,8 @@
     7.4  
     7.5  theory Factorial_Ring
     7.6  imports 
     7.7 -  Main 
     7.8 -  "~~/src/HOL/Number_Theory/Primes"
     7.9 +  Main
    7.10 +  "../GCD"
    7.11    "~~/src/HOL/Library/Multiset"
    7.12  begin
    7.13  
    7.14 @@ -84,6 +84,15 @@
    7.15    shows "p \<noteq> 0"
    7.16    using assms by (auto intro: ccontr)
    7.17  
    7.18 +
    7.19 +lemma is_prime_elem_dvd_power: 
    7.20 +  "is_prime_elem p \<Longrightarrow> p dvd x ^ n \<Longrightarrow> p dvd x"
    7.21 +  by (induction n) (auto dest: prime_divides_productD intro: dvd_trans[of _ 1])
    7.22 +
    7.23 +lemma is_prime_elem_dvd_power_iff:
    7.24 +  "is_prime_elem p \<Longrightarrow> n > 0 \<Longrightarrow> p dvd x ^ n \<longleftrightarrow> p dvd x"
    7.25 +  by (auto dest: is_prime_elem_dvd_power intro: dvd_trans)
    7.26 +
    7.27  lemma is_prime_elem_imp_nonzero [simp]:
    7.28    "ASSUMPTION (is_prime_elem x) \<Longrightarrow> x \<noteq> 0"
    7.29    unfolding ASSUMPTION_def by (rule is_prime_elem_not_zeroI)
    7.30 @@ -94,12 +103,13 @@
    7.31  
    7.32  end
    7.33  
    7.34 -lemma (in algebraic_semidom) mult_unit_dvd_iff': "is_unit a \<Longrightarrow> (a * b) dvd c \<longleftrightarrow> b dvd c"
    7.35 -  by (subst mult.commute) (rule mult_unit_dvd_iff)
    7.36 -
    7.37  context algebraic_semidom
    7.38  begin
    7.39  
    7.40 +(* TODO Move *)
    7.41 +lemma mult_unit_dvd_iff': "is_unit a \<Longrightarrow> (a * b) dvd c \<longleftrightarrow> b dvd c"
    7.42 +  by (subst mult.commute) (rule mult_unit_dvd_iff)
    7.43 +
    7.44  lemma prime_imp_irreducible:
    7.45    assumes "is_prime_elem p"
    7.46    shows   "irreducible p"
    7.47 @@ -191,6 +201,29 @@
    7.48      by (auto simp add: mult_unit_dvd_iff)
    7.49  qed
    7.50  
    7.51 +context
    7.52 +begin
    7.53 +
    7.54 +private lemma is_prime_elem_powerD:
    7.55 +  assumes "is_prime_elem (p ^ n)"
    7.56 +  shows   "is_prime_elem p \<and> n = 1"
    7.57 +proof (cases n)
    7.58 +  case (Suc m)
    7.59 +  note assms
    7.60 +  also from Suc have "p ^ n = p * p^m" by simp
    7.61 +  finally have "is_unit p \<or> is_unit (p^m)" by (rule is_prime_elem_multD)
    7.62 +  moreover from assms have "\<not>is_unit p" by (simp add: is_prime_elem_def is_unit_power_iff)
    7.63 +  ultimately have "is_unit (p ^ m)" by simp
    7.64 +  with \<open>\<not>is_unit p\<close> have "m = 0" by (simp add: is_unit_power_iff)
    7.65 +  with Suc assms show ?thesis by simp
    7.66 +qed (insert assms, simp_all)
    7.67 +
    7.68 +lemma is_prime_elem_power_iff:
    7.69 +  "is_prime_elem (p ^ n) \<longleftrightarrow> is_prime_elem p \<and> n = 1"
    7.70 +  by (auto dest: is_prime_elem_powerD)
    7.71 +
    7.72 +end
    7.73 +
    7.74  lemma irreducible_mult_unit_left:
    7.75    "is_unit a \<Longrightarrow> irreducible (a * p) \<longleftrightarrow> irreducible p"
    7.76    by (auto simp: irreducible_altdef mult.commute[of a] is_unit_mult_iff
    7.77 @@ -235,6 +268,10 @@
    7.78  lemma is_prime_normalize_iff [simp]: "is_prime (normalize p) \<longleftrightarrow> is_prime_elem p"
    7.79    by (auto simp add: is_prime_def)
    7.80  
    7.81 +lemma is_prime_power_iff:
    7.82 +  "is_prime (p ^ n) \<longleftrightarrow> is_prime p \<and> n = 1"
    7.83 +  by (auto simp: is_prime_def is_prime_elem_power_iff)
    7.84 +
    7.85  lemma is_prime_elem_not_unit' [simp]:
    7.86    "ASSUMPTION (is_prime_elem x) \<Longrightarrow> \<not>is_unit x"
    7.87    unfolding ASSUMPTION_def by (rule is_prime_elem_not_unit)
    7.88 @@ -273,6 +310,20 @@
    7.89      by (blast intro: is_prime_elemD2)
    7.90  qed
    7.91  
    7.92 +lemma is_prime_dvd_multD: "is_prime p \<Longrightarrow> p dvd a * b \<Longrightarrow> p dvd a \<or> p dvd b"
    7.93 +  by (intro prime_divides_productD) simp_all
    7.94 +
    7.95 +lemma is_prime_dvd_mult_iff [simp]: "is_prime p \<Longrightarrow> p dvd a * b \<longleftrightarrow> p dvd a \<or> p dvd b"
    7.96 +  by (auto dest: is_prime_dvd_multD)
    7.97 +
    7.98 +lemma is_prime_dvd_power: 
    7.99 +  "is_prime p \<Longrightarrow> p dvd x ^ n \<Longrightarrow> p dvd x"
   7.100 +  by (auto dest!: is_prime_elem_dvd_power simp: is_prime_def)
   7.101 +
   7.102 +lemma is_prime_dvd_power_iff:
   7.103 +  "is_prime p \<Longrightarrow> n > 0 \<Longrightarrow> p dvd x ^ n \<longleftrightarrow> p dvd x"
   7.104 +  by (intro is_prime_elem_dvd_power_iff) simp_all
   7.105 +
   7.106  lemma prime_dvd_msetprodE:
   7.107    assumes "is_prime_elem p"
   7.108    assumes dvd: "p dvd msetprod A"
   7.109 @@ -499,6 +550,50 @@
   7.110      by (auto simp: mult_unit_dvd_iff mult_unit_dvd_iff')
   7.111  qed (insert assms, auto simp: irreducible_not_unit)
   7.112  
   7.113 +lemma is_prime_elem_imp_coprime:
   7.114 +  assumes "is_prime_elem p" "\<not>p dvd n"
   7.115 +  shows   "coprime p n"
   7.116 +proof (rule coprimeI)
   7.117 +  fix d assume "d dvd p" "d dvd n"
   7.118 +  show "is_unit d"
   7.119 +  proof (rule ccontr)
   7.120 +    assume "\<not>is_unit d"
   7.121 +    from \<open>is_prime_elem p\<close> and \<open>d dvd p\<close> and this have "p dvd d"
   7.122 +      by (rule is_prime_elemD2)
   7.123 +    from this and \<open>d dvd n\<close> have "p dvd n" by (rule dvd_trans)
   7.124 +    with \<open>\<not>p dvd n\<close> show False by contradiction
   7.125 +  qed
   7.126 +qed
   7.127 +
   7.128 +lemma is_prime_imp_coprime:
   7.129 +  assumes "is_prime p" "\<not>p dvd n"
   7.130 +  shows   "coprime p n"
   7.131 +  using assms by (simp add: is_prime_elem_imp_coprime)
   7.132 +
   7.133 +lemma is_prime_elem_imp_power_coprime: 
   7.134 +  "is_prime_elem p \<Longrightarrow> \<not>p dvd a \<Longrightarrow> coprime a (p ^ m)"
   7.135 +  by (auto intro!: coprime_exp dest: is_prime_elem_imp_coprime simp: gcd.commute)
   7.136 +
   7.137 +lemma is_prime_imp_power_coprime: 
   7.138 +  "is_prime p \<Longrightarrow> \<not>p dvd a \<Longrightarrow> coprime a (p ^ m)"
   7.139 +  by (simp add: is_prime_elem_imp_power_coprime)
   7.140 +
   7.141 +lemma prime_divprod_pow:
   7.142 +  assumes p: "is_prime_elem p" and ab: "coprime a b" and pab: "p^n dvd a * b"
   7.143 +  shows   "p^n dvd a \<or> p^n dvd b"
   7.144 +  using assms
   7.145 +proof -
   7.146 +  from ab p have "\<not>p dvd a \<or> \<not>p dvd b"
   7.147 +    by (auto simp: coprime is_prime_elem_def)
   7.148 +  with p have "coprime (p^n) a \<or> coprime (p^n) b" 
   7.149 +    by (auto intro: is_prime_elem_imp_coprime coprime_exp_left)
   7.150 +  with pab show ?thesis by (auto intro: coprime_dvd_mult simp: mult_ac)
   7.151 +qed
   7.152 +
   7.153 +lemma primes_coprime: 
   7.154 +  "is_prime p \<Longrightarrow> is_prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> coprime p q"
   7.155 +  using is_prime_imp_coprime primes_dvd_imp_eq by blast
   7.156 +
   7.157  end
   7.158  
   7.159  
   7.160 @@ -683,12 +778,10 @@
   7.161    using multiplicity_geI[of n] multiplicity_lessI[of n] by (cases "p ^ n dvd x") auto
   7.162  
   7.163  lemma multiplicity_eq_zero_iff:
   7.164 -  assumes "x \<noteq> 0" "\<not>is_unit p"
   7.165    shows   "multiplicity p x = 0 \<longleftrightarrow> \<not>p dvd x"
   7.166    using power_dvd_iff_le_multiplicity[of 1] by auto
   7.167  
   7.168  lemma multiplicity_gt_zero_iff:
   7.169 -  assumes "x \<noteq> 0" "\<not>is_unit p"
   7.170    shows   "multiplicity p x > 0 \<longleftrightarrow> p dvd x"
   7.171    using power_dvd_iff_le_multiplicity[of 1] by auto
   7.172  
   7.173 @@ -716,6 +809,19 @@
   7.174  lemma multiplicity_zero [simp]: "multiplicity p 0 = 0"
   7.175    by (simp add: multiplicity_def)
   7.176  
   7.177 +lemma prime_multiplicity_eq_zero_iff:
   7.178 +  "is_prime_elem p \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> multiplicity p x = 0 \<longleftrightarrow> \<not>p dvd x"
   7.179 +  by (rule multiplicity_eq_zero_iff) simp_all
   7.180 +
   7.181 +lemma prime_multiplicity_other:
   7.182 +  assumes "is_prime p" "is_prime q" "p \<noteq> q"
   7.183 +  shows   "multiplicity p q = 0"
   7.184 +  using assms by (subst prime_multiplicity_eq_zero_iff) (auto dest: primes_dvd_imp_eq)  
   7.185 +
   7.186 +lemma prime_multiplicity_gt_zero_iff:
   7.187 +  "is_prime_elem p \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> multiplicity p x > 0 \<longleftrightarrow> p dvd x"
   7.188 +  by (rule multiplicity_gt_zero_iff) simp_all
   7.189 +
   7.190  lemma multiplicity_unit_left: "is_unit p \<Longrightarrow> multiplicity p x = 0"
   7.191    by (simp add: multiplicity_def is_unit_power_iff unit_imp_dvd)
   7.192  
   7.193 @@ -1008,7 +1114,7 @@
   7.194    also have "multiplicity p \<dots> = multiplicity p x"
   7.195      by (rule multiplicity_times_unit_right) (simp add: is_unit_unit_factor)
   7.196    finally show ?thesis .
   7.197 -qed simp_all
   7.198 +qed simp_all   
   7.199  
   7.200  lemma prime_factorization_cong:
   7.201    "normalize x = normalize y \<Longrightarrow> prime_factorization x = prime_factorization y"
   7.202 @@ -1062,6 +1168,10 @@
   7.203    finally show ?thesis ..
   7.204  qed
   7.205  
   7.206 +lemma prime_factorization_subset_imp_dvd: 
   7.207 +  "x \<noteq> 0 \<Longrightarrow> (prime_factorization x \<subseteq># prime_factorization y) \<Longrightarrow> x dvd y"
   7.208 +  by (cases "y = 0") (simp_all add: prime_factorization_subset_iff_dvd)
   7.209 +
   7.210  lemma prime_factorization_divide:
   7.211    assumes "b dvd a"
   7.212    shows   "prime_factorization (a div b) = prime_factorization a - prime_factorization b"
   7.213 @@ -1077,6 +1187,204 @@
   7.214    by (auto dest: in_prime_factorization_imp_prime)
   7.215  
   7.216  
   7.217 +lemma prime_multiplicity_mult_distrib:
   7.218 +  assumes "is_prime_elem p" "x \<noteq> 0" "y \<noteq> 0"
   7.219 +  shows   "multiplicity p (x * y) = multiplicity p x + multiplicity p y"
   7.220 +proof -
   7.221 +  have "multiplicity p (x * y) = count (prime_factorization (x * y)) (normalize p)"
   7.222 +    by (subst count_prime_factorization_prime) (simp_all add: assms)
   7.223 +  also from assms 
   7.224 +    have "prime_factorization (x * y) = prime_factorization x + prime_factorization y"
   7.225 +      by (intro prime_factorization_mult)
   7.226 +  also have "count \<dots> (normalize p) = 
   7.227 +    count (prime_factorization x) (normalize p) + count (prime_factorization y) (normalize p)"
   7.228 +    by simp
   7.229 +  also have "\<dots> = multiplicity p x + multiplicity p y" 
   7.230 +    by (subst (1 2) count_prime_factorization_prime) (simp_all add: assms)
   7.231 +  finally show ?thesis .
   7.232 +qed
   7.233 +
   7.234 +lemma prime_multiplicity_power_distrib:
   7.235 +  assumes "is_prime_elem p" "x \<noteq> 0"
   7.236 +  shows   "multiplicity p (x ^ n) = n * multiplicity p x"
   7.237 +  by (induction n) (simp_all add: assms prime_multiplicity_mult_distrib)
   7.238 +
   7.239 +lemma prime_multiplicity_msetprod_distrib:
   7.240 +  assumes "is_prime_elem p" "0 \<notin># A"
   7.241 +  shows   "multiplicity p (msetprod A) = msetsum (image_mset (multiplicity p) A)"
   7.242 +  using assms by (induction A) (auto simp: prime_multiplicity_mult_distrib)
   7.243 +
   7.244 +lemma prime_multiplicity_setprod_distrib:
   7.245 +  assumes "is_prime_elem p" "0 \<notin> f ` A" "finite A"
   7.246 +  shows   "multiplicity p (setprod f A) = (\<Sum>x\<in>A. multiplicity p (f x))"
   7.247 +proof -
   7.248 +  have "multiplicity p (setprod f A) = (\<Sum>x\<in>#mset_set A. multiplicity p (f x))"
   7.249 +    using assms by (subst setprod_unfold_msetprod)
   7.250 +                   (simp_all add: prime_multiplicity_msetprod_distrib setsum_unfold_msetsum 
   7.251 +                      multiset.map_comp o_def)
   7.252 +  also from \<open>finite A\<close> have "\<dots> = (\<Sum>x\<in>A. multiplicity p (f x))"
   7.253 +    by (induction A rule: finite_induct) simp_all
   7.254 +  finally show ?thesis .
   7.255 +qed
   7.256 +
   7.257 +
   7.258 +
   7.259 +definition prime_factors where
   7.260 +  "prime_factors x = set_mset (prime_factorization x)"
   7.261 +
   7.262 +lemma set_mset_prime_factorization:
   7.263 +  "set_mset (prime_factorization x) = prime_factors x"
   7.264 +  by (simp add: prime_factors_def)
   7.265 +
   7.266 +lemma prime_factorsI:
   7.267 +  "x \<noteq> 0 \<Longrightarrow> is_prime p \<Longrightarrow> p dvd x \<Longrightarrow> p \<in> prime_factors x"
   7.268 +  by (auto simp: prime_factors_def in_prime_factorization_iff)
   7.269 +
   7.270 +lemma prime_factors_prime [intro]: "p \<in> prime_factors x \<Longrightarrow> is_prime p"
   7.271 +  by (auto simp: prime_factors_def dest: in_prime_factorization_imp_prime)
   7.272 +
   7.273 +lemma prime_factors_dvd [dest]: "p \<in> prime_factors x \<Longrightarrow> p dvd x"
   7.274 +  by (auto simp: prime_factors_def dest: in_prime_factorization_imp_dvd)
   7.275 +
   7.276 +lemma prime_factors_finite [iff]:
   7.277 +  "finite (prime_factors n)"
   7.278 +  unfolding prime_factors_def by simp
   7.279 +
   7.280 +lemma prime_factors_altdef_multiplicity:
   7.281 +  "prime_factors n = {p. is_prime p \<and> multiplicity p n > 0}"
   7.282 +  by (cases "n = 0")
   7.283 +     (auto simp: prime_factors_def prime_multiplicity_gt_zero_iff 
   7.284 +        prime_imp_prime_elem in_prime_factorization_iff)
   7.285 +
   7.286 +lemma setprod_prime_factors:
   7.287 +  assumes "x \<noteq> 0"
   7.288 +  shows   "(\<Prod>p \<in> prime_factors x. p ^ multiplicity p x) = normalize x"
   7.289 +proof -
   7.290 +  have "normalize x = msetprod (prime_factorization x)"
   7.291 +    by (simp add: msetprod_prime_factorization assms)
   7.292 +  also have "\<dots> = (\<Prod>p \<in> prime_factors x. p ^ count (prime_factorization x) p)"
   7.293 +    by (subst msetprod_multiplicity) (simp_all add: prime_factors_def)
   7.294 +  also have "\<dots> = (\<Prod>p \<in> prime_factors x. p ^ multiplicity p x)"
   7.295 +    by (intro setprod.cong) 
   7.296 +      (simp_all add: assms count_prime_factorization_prime prime_factors_prime)
   7.297 +  finally show ?thesis ..
   7.298 +qed
   7.299 +
   7.300 +(* TODO Move *)
   7.301 +lemma (in semidom) setprod_zero_iff [simp]:
   7.302 +  assumes "finite A"
   7.303 +  shows "setprod f A = 0 \<longleftrightarrow> (\<exists>a\<in>A. f a = 0)"
   7.304 +  using assms by (induct A) (auto simp: no_zero_divisors)
   7.305 +(* END TODO *)
   7.306 +
   7.307 +lemma prime_factorization_unique'':
   7.308 +  assumes S_eq: "S = {p. 0 < f p}"
   7.309 +    and "finite S"
   7.310 +    and S: "\<forall>p\<in>S. is_prime p" "normalize n = (\<Prod>p\<in>S. p ^ f p)"
   7.311 +  shows "S = prime_factors n \<and> (\<forall>p. is_prime p \<longrightarrow> f p = multiplicity p n)"
   7.312 +proof
   7.313 +  define A where "A = Abs_multiset f"
   7.314 +  from \<open>finite S\<close> S(1) have "(\<Prod>p\<in>S. p ^ f p) \<noteq> 0" by auto
   7.315 +  with S(2) have nz: "n \<noteq> 0" by auto
   7.316 +  from S_eq \<open>finite S\<close> have count_A: "count A x = f x" for x
   7.317 +    unfolding A_def by (subst multiset.Abs_multiset_inverse) (simp_all add: multiset_def)
   7.318 +  from S_eq count_A have set_mset_A: "set_mset A = S"
   7.319 +    by (simp only: set_mset_def)
   7.320 +  from S(2) have "normalize n = (\<Prod>p\<in>S. p ^ f p)" .
   7.321 +  also have "\<dots> = msetprod A" by (simp add: msetprod_multiplicity S_eq set_mset_A count_A)
   7.322 +  also from nz have "normalize n = msetprod (prime_factorization n)" 
   7.323 +    by (simp add: msetprod_prime_factorization)
   7.324 +  finally have "prime_factorization (msetprod A) = 
   7.325 +                  prime_factorization (msetprod (prime_factorization n))" by simp
   7.326 +  also from S(1) have "prime_factorization (msetprod A) = A"
   7.327 +    by (intro prime_factorization_msetprod_primes) (auto simp: set_mset_A)
   7.328 +  also have "prime_factorization (msetprod (prime_factorization n)) = prime_factorization n"
   7.329 +    by (intro prime_factorization_msetprod_primes) (auto dest: in_prime_factorization_imp_prime)
   7.330 +  finally show "S = prime_factors n" by (simp add: prime_factors_def set_mset_A [symmetric])
   7.331 +  
   7.332 +  show "(\<forall>p. is_prime p \<longrightarrow> f p = multiplicity p n)"
   7.333 +  proof safe
   7.334 +    fix p :: 'a assume p: "is_prime p"
   7.335 +    have "multiplicity p n = multiplicity p (normalize n)" by simp
   7.336 +    also have "normalize n = msetprod A" 
   7.337 +      by (simp add: msetprod_multiplicity S_eq set_mset_A count_A S)
   7.338 +    also from p set_mset_A S(1) 
   7.339 +    have "multiplicity p \<dots> = msetsum (image_mset (multiplicity p) A)"
   7.340 +      by (intro prime_multiplicity_msetprod_distrib) auto
   7.341 +    also from S(1) p
   7.342 +    have "image_mset (multiplicity p) A = image_mset (\<lambda>q. if p = q then 1 else 0) A"
   7.343 +      by (intro image_mset_cong) (auto simp: set_mset_A multiplicity_self prime_multiplicity_other)
   7.344 +    also have "msetsum \<dots> = f p" by (simp add: msetsum_delta' count_A)
   7.345 +    finally show "f p = multiplicity p n" ..
   7.346 +  qed
   7.347 +qed
   7.348 +
   7.349 +lemma multiplicity_prime [simp]: "is_prime_elem p \<Longrightarrow> multiplicity p p = 1"
   7.350 +  by (rule multiplicity_self) auto
   7.351 +
   7.352 +lemma multiplicity_prime_power [simp]: "is_prime_elem p \<Longrightarrow> multiplicity p (p ^ n) = n"
   7.353 +  by (subst multiplicity_same_power') auto
   7.354 +
   7.355 +lemma prime_factors_product: 
   7.356 +  "x \<noteq> 0 \<Longrightarrow> y \<noteq> 0 \<Longrightarrow> prime_factors (x * y) = prime_factors x \<union> prime_factors y"
   7.357 +  by (simp add: prime_factors_def prime_factorization_mult)
   7.358 +
   7.359 +lemma multiplicity_distinct_prime_power:
   7.360 +  "is_prime p \<Longrightarrow> is_prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> multiplicity p (q ^ n) = 0"
   7.361 +  by (subst prime_multiplicity_power_distrib) (auto simp: prime_multiplicity_other)
   7.362 +
   7.363 +lemma dvd_imp_multiplicity_le:
   7.364 +  assumes "a dvd b" "b \<noteq> 0"
   7.365 +  shows   "multiplicity p a \<le> multiplicity p b"
   7.366 +proof (cases "is_unit p")
   7.367 +  case False
   7.368 +  with assms show ?thesis
   7.369 +    by (intro multiplicity_geI ) (auto intro: dvd_trans[OF multiplicity_dvd' assms(1)])
   7.370 +qed (insert assms, auto simp: multiplicity_unit_left)
   7.371 +
   7.372 +lemma dvd_prime_factors [intro]:
   7.373 +  "y \<noteq> 0 \<Longrightarrow> x dvd y \<Longrightarrow> prime_factors x \<subseteq> prime_factors y"
   7.374 +  unfolding prime_factors_def
   7.375 +  by (intro set_mset_mono, subst prime_factorization_subset_iff_dvd) auto
   7.376 +
   7.377 +(* RENAMED multiplicity_dvd *)
   7.378 +lemma multiplicity_le_imp_dvd:
   7.379 +  assumes "x \<noteq> 0" "\<And>p. is_prime p \<Longrightarrow> multiplicity p x \<le> multiplicity p y"
   7.380 +  shows   "x dvd y"
   7.381 +proof (cases "y = 0")
   7.382 +  case False
   7.383 +  from assms this have "prime_factorization x \<subseteq># prime_factorization y"
   7.384 +    by (intro mset_subset_eqI) (auto simp: count_prime_factorization)
   7.385 +  with assms False show ?thesis by (subst (asm) prime_factorization_subset_iff_dvd)
   7.386 +qed auto
   7.387 +
   7.388 +lemma dvd_multiplicity_eq:
   7.389 +  "x \<noteq> 0 \<Longrightarrow> y \<noteq> 0 \<Longrightarrow> x dvd y \<longleftrightarrow> (\<forall>p. multiplicity p x \<le> multiplicity p y)"
   7.390 +  by (auto intro: dvd_imp_multiplicity_le multiplicity_le_imp_dvd)
   7.391 +
   7.392 +lemma prime_factors_altdef: "x \<noteq> 0 \<Longrightarrow> prime_factors x = {p. is_prime p \<and> p dvd x}"
   7.393 +  by (auto intro: prime_factorsI)
   7.394 +
   7.395 +lemma multiplicity_eq_imp_eq:
   7.396 +  assumes "x \<noteq> 0" "y \<noteq> 0"
   7.397 +  assumes "\<And>p. is_prime p \<Longrightarrow> multiplicity p x = multiplicity p y"
   7.398 +  shows   "normalize x = normalize y"
   7.399 +  using assms by (intro associatedI multiplicity_le_imp_dvd) simp_all
   7.400 +
   7.401 +lemma prime_factorization_unique':
   7.402 +  assumes "\<forall>p \<in># M. is_prime p" "\<forall>p \<in># N. is_prime p" "(\<Prod>i \<in># M. i) = (\<Prod>i \<in># N. i)"
   7.403 +  shows   "M = N"
   7.404 +proof -
   7.405 +  have "prime_factorization (\<Prod>i \<in># M. i) = prime_factorization (\<Prod>i \<in># N. i)"
   7.406 +    by (simp only: assms)
   7.407 +  also from assms have "prime_factorization (\<Prod>i \<in># M. i) = M"
   7.408 +    by (subst prime_factorization_msetprod_primes) simp_all
   7.409 +  also from assms have "prime_factorization (\<Prod>i \<in># N. i) = N"
   7.410 +    by (subst prime_factorization_msetprod_primes) simp_all
   7.411 +  finally show ?thesis .
   7.412 +qed
   7.413 +
   7.414 +
   7.415  definition "gcd_factorial a b = (if a = 0 then normalize b
   7.416       else if b = 0 then normalize a
   7.417       else msetprod (prime_factorization a #\<inter> prime_factorization b))"
   7.418 @@ -1418,6 +1726,72 @@
   7.419    by (standard, unfold Gcd_eq_Gcd_factorial Lcm_eq_Lcm_factorial)
   7.420       (rule gcd_lcm_factorial; assumption)+
   7.421  
   7.422 +lemma
   7.423 +  assumes "x \<noteq> 0" "y \<noteq> 0"
   7.424 +  shows gcd_eq_factorial': 
   7.425 +          "gcd x y = (\<Prod>p \<in> prime_factors x \<inter> prime_factors y. 
   7.426 +                          p ^ min (multiplicity p x) (multiplicity p y))" (is "_ = ?rhs1")
   7.427 +    and lcm_eq_factorial':
   7.428 +          "lcm x y = (\<Prod>p \<in> prime_factors x \<union> prime_factors y. 
   7.429 +                          p ^ max (multiplicity p x) (multiplicity p y))" (is "_ = ?rhs2")
   7.430 +proof -
   7.431 +  have "gcd x y = gcd_factorial x y" by (rule gcd_eq_gcd_factorial)
   7.432 +  also have "\<dots> = ?rhs1"
   7.433 +    by (auto simp: gcd_factorial_def assms msetprod_multiplicity set_mset_prime_factorization
   7.434 +          count_prime_factorization_prime dest: prime_factors_prime intro!: setprod.cong)
   7.435 +  finally show "gcd x y = ?rhs1" .
   7.436 +  have "lcm x y = lcm_factorial x y" by (rule lcm_eq_lcm_factorial)
   7.437 +  also have "\<dots> = ?rhs2"
   7.438 +    by (auto simp: lcm_factorial_def assms msetprod_multiplicity set_mset_prime_factorization
   7.439 +          count_prime_factorization_prime dest: prime_factors_prime intro!: setprod.cong)
   7.440 +  finally show "lcm x y = ?rhs2" .
   7.441 +qed
   7.442 +
   7.443 +lemma
   7.444 +  assumes "x \<noteq> 0" "y \<noteq> 0" "is_prime p"
   7.445 +  shows   multiplicity_gcd: "multiplicity p (gcd x y) = min (multiplicity p x) (multiplicity p y)"
   7.446 +    and   multiplicity_lcm: "multiplicity p (lcm x y) = max (multiplicity p x) (multiplicity p y)"
   7.447 +proof -
   7.448 +  have "gcd x y = gcd_factorial x y" by (rule gcd_eq_gcd_factorial)
   7.449 +  also from assms have "multiplicity p \<dots> = min (multiplicity p x) (multiplicity p y)"
   7.450 +    by (simp add: count_prime_factorization_prime [symmetric] prime_factorization_gcd_factorial)
   7.451 +  finally show "multiplicity p (gcd x y) = min (multiplicity p x) (multiplicity p y)" .
   7.452 +  have "lcm x y = lcm_factorial x y" by (rule lcm_eq_lcm_factorial)
   7.453 +  also from assms have "multiplicity p \<dots> = max (multiplicity p x) (multiplicity p y)"
   7.454 +    by (simp add: count_prime_factorization_prime [symmetric] prime_factorization_lcm_factorial)
   7.455 +  finally show "multiplicity p (lcm x y) = max (multiplicity p x) (multiplicity p y)" .
   7.456 +qed
   7.457 +
   7.458 +lemma gcd_lcm_distrib:
   7.459 +  "gcd x (lcm y z) = lcm (gcd x y) (gcd x z)"
   7.460 +proof (cases "x = 0 \<or> y = 0 \<or> z = 0")
   7.461 +  case True
   7.462 +  thus ?thesis
   7.463 +    by (auto simp: lcm_proj1_if_dvd lcm_proj2_if_dvd)
   7.464 +next
   7.465 +  case False
   7.466 +  hence "normalize (gcd x (lcm y z)) = normalize (lcm (gcd x y) (gcd x z))"
   7.467 +    by (intro associatedI prime_factorization_subset_imp_dvd)
   7.468 +       (auto simp: lcm_eq_0_iff prime_factorization_gcd prime_factorization_lcm 
   7.469 +          subset_mset.inf_sup_distrib1)
   7.470 +  thus ?thesis by simp
   7.471 +qed
   7.472 +
   7.473 +lemma lcm_gcd_distrib:
   7.474 +  "lcm x (gcd y z) = gcd (lcm x y) (lcm x z)"
   7.475 +proof (cases "x = 0 \<or> y = 0 \<or> z = 0")
   7.476 +  case True
   7.477 +  thus ?thesis
   7.478 +    by (auto simp: lcm_proj1_if_dvd lcm_proj2_if_dvd)
   7.479 +next
   7.480 +  case False
   7.481 +  hence "normalize (lcm x (gcd y z)) = normalize (gcd (lcm x y) (lcm x z))"
   7.482 +    by (intro associatedI prime_factorization_subset_imp_dvd)
   7.483 +       (auto simp: lcm_eq_0_iff prime_factorization_gcd prime_factorization_lcm 
   7.484 +          subset_mset.sup_inf_distrib1)
   7.485 +  thus ?thesis by simp
   7.486 +qed
   7.487 +
   7.488  end
   7.489  
   7.490  
   7.491 @@ -1430,37 +1804,5 @@
   7.492  
   7.493  end
   7.494  
   7.495 -
   7.496 -lemma is_prime_elem_nat: "is_prime_elem (n::nat) \<longleftrightarrow> prime n"
   7.497 -proof
   7.498 -  assume *: "is_prime_elem n"
   7.499 -  show "prime n" unfolding prime_def
   7.500 -  proof safe
   7.501 -    from * have "n \<noteq> 0" "n \<noteq> 1" by (intro notI, simp del: One_nat_def)+
   7.502 -    thus "n > 1" by (cases n) simp_all
   7.503 -  next
   7.504 -    fix m assume m: "m dvd n" "m \<noteq> n"
   7.505 -    from * \<open>m dvd n\<close> have "n dvd m \<or> is_unit m"
   7.506 -      by (intro irreducibleD' prime_imp_irreducible)
   7.507 -    with m show "m = 1" by (auto dest: dvd_antisym)
   7.508 -  qed
   7.509 -qed (auto simp: is_prime_elem_def prime_gt_0_nat)
   7.510 -
   7.511 -lemma is_prime_nat: "is_prime (n::nat) \<longleftrightarrow> prime n"
   7.512 -  by (simp add: is_prime_def is_prime_elem_nat)
   7.513 -
   7.514 -lemma is_prime_elem_int: "is_prime_elem (n::int) \<longleftrightarrow> prime (nat (abs n))"
   7.515 -proof (subst is_prime_elem_nat [symmetric], rule iffI)
   7.516 -  assume "is_prime_elem n"
   7.517 -  thus "is_prime_elem (nat (abs n))" by (auto simp: is_prime_elem_def nat_dvd_iff)
   7.518 -next
   7.519 -  assume "is_prime_elem (nat (abs n))"
   7.520 -  thus "is_prime_elem n"
   7.521 -    by (auto simp: dvd_int_unfold_dvd_nat is_prime_elem_def abs_mult nat_mult_distrib)
   7.522 -qed
   7.523 -
   7.524 -lemma is_prime_int: "is_prime (n::int) \<longleftrightarrow> prime n \<and> n \<ge> 0"
   7.525 -  by (simp add: is_prime_def is_prime_elem_int)
   7.526 -
   7.527  end
   7.528  
     8.1 --- a/src/HOL/Number_Theory/Gauss.thy	Wed Jul 20 14:52:09 2016 +0200
     8.2 +++ b/src/HOL/Number_Theory/Gauss.thy	Thu Jul 21 10:06:04 2016 +0200
     8.3 @@ -109,10 +109,12 @@
     8.4      assume c: "x \<le> (int p - 1) div 2"
     8.5      assume d: "0 < y"
     8.6      assume e: "y \<le> (int p - 1) div 2"
     8.7 -    from a p_a_relprime p_prime a_nonzero cong_mult_rcancel_int [of _ a x y]
     8.8 -    have "[x = y](mod p)"
     8.9 -      by (metis monoid_mult_class.mult.left_neutral cong_dvd_modulus_int cong_mult_rcancel_int 
    8.10 -                cong_mult_self_int gcd.commute prime_imp_coprime_int)
    8.11 +    from p_a_relprime have "\<not>p dvd a"
    8.12 +      by (simp add: cong_altdef_int)
    8.13 +    with p_prime have "coprime a (int p)" 
    8.14 +       by (subst gcd.commute, intro is_prime_imp_coprime) auto
    8.15 +    with a cong_mult_rcancel_int [of a "int p" x y]
    8.16 +      have "[x = y] (mod p)" by simp
    8.17      with cong_less_imp_eq_int [of x y p] p_minus_one_l
    8.18          order_le_less_trans [of x "(int p - 1) div 2" p]
    8.19          order_le_less_trans [of y "(int p - 1) div 2" p] 
    8.20 @@ -137,11 +139,14 @@
    8.21    assume d: "0 < y"
    8.22    assume e: "y \<le> (int p - 1) div 2"
    8.23    assume f: "x \<noteq> y"
    8.24 -  from a have "[x * a = y * a](mod p)" 
    8.25 +  from a have a': "[x * a = y * a](mod p)" 
    8.26      by (metis cong_int_def)
    8.27 -  with p_a_relprime p_prime cong_mult_rcancel_int [of a p x y]
    8.28 -  have "[x = y](mod p)" 
    8.29 -    by (metis cong_mult_self_int dvd_div_mult_self gcd.commute prime_imp_coprime_int)
    8.30 +  from p_a_relprime have "\<not>p dvd a"
    8.31 +    by (simp add: cong_altdef_int)
    8.32 +  with p_prime have "coprime a (int p)" 
    8.33 +     by (subst gcd.commute, intro is_prime_imp_coprime) auto
    8.34 +  with a' cong_mult_rcancel_int [of a "int p" x y]
    8.35 +    have "[x = y] (mod p)" by simp
    8.36    with cong_less_imp_eq_int [of x y p] p_minus_one_l
    8.37      order_le_less_trans [of x "(int p - 1) div 2" p]
    8.38      order_le_less_trans [of y "(int p - 1) div 2" p] 
    8.39 @@ -170,7 +175,7 @@
    8.40    by (auto simp add: A_def)
    8.41  
    8.42  lemma B_ncong_p: "x \<in> B \<Longrightarrow> [x \<noteq> 0](mod p)"
    8.43 -  by (auto simp add: B_def) (metis cong_prime_prod_zero_int A_ncong_p p_a_relprime p_prime)
    8.44 +  by (auto simp: B_def p_prime p_a_relprime A_ncong_p dest: cong_prime_prod_zero_int) 
    8.45  
    8.46  lemma B_greater_zero: "x \<in> B \<Longrightarrow> 0 < x"
    8.47    using a_nonzero by (auto simp add: B_def A_greater_zero)
    8.48 @@ -202,7 +207,7 @@
    8.49  
    8.50  lemma all_A_relprime: assumes "x \<in> A" shows "gcd x p = 1"
    8.51    using p_prime A_ncong_p [OF assms]
    8.52 -  by (simp add: cong_altdef_int) (metis gcd.commute prime_imp_coprime_int)
    8.53 +  by (auto simp: cong_altdef_int gcd.commute[of _ "int p"] intro!: is_prime_imp_coprime)
    8.54  
    8.55  lemma A_prod_relprime: "gcd (setprod id A) p = 1"
    8.56    by (metis id_def all_A_relprime setprod_coprime)
    8.57 @@ -266,7 +271,7 @@
    8.58      by (metis cong_int_def mod_add_left_eq mod_add_right_eq mult.commute ring_class.ring_distribs(1))
    8.59    with p_prime a_nonzero p_a_relprime
    8.60    have a: "[y + z = 0] (mod p)"
    8.61 -    by (metis cong_prime_prod_zero_int)
    8.62 +    by (auto dest!: cong_prime_prod_zero_int)
    8.63    assume b: "y \<in> A" and c: "z \<in> A"
    8.64    with A_def have "0 < y + z"
    8.65      by auto
     9.1 --- a/src/HOL/Number_Theory/Pocklington.thy	Wed Jul 20 14:52:09 2016 +0200
     9.2 +++ b/src/HOL/Number_Theory/Pocklington.thy	Thu Jul 21 10:06:04 2016 +0200
     9.3 @@ -11,39 +11,17 @@
     9.4  subsection\<open>Lemmas about previously defined terms\<close>
     9.5  
     9.6  lemma prime: 
     9.7 -  "prime p \<longleftrightarrow> p \<noteq> 0 \<and> p \<noteq> 1 \<and> (\<forall>m. 0 < m \<and> m < p \<longrightarrow> coprime p m)"
     9.8 -  (is "?lhs \<longleftrightarrow> ?rhs")
     9.9 -proof-
    9.10 -  {assume "p=0 \<or> p=1" hence ?thesis
    9.11 -    by (metis one_not_prime_nat zero_not_prime_nat)}
    9.12 -  moreover
    9.13 -  {assume p0: "p\<noteq>0" "p\<noteq>1"
    9.14 -    {assume H: "?lhs"
    9.15 -      {fix m assume m: "m > 0" "m < p"
    9.16 -        {assume "m=1" hence "coprime p m" by simp}
    9.17 -        moreover
    9.18 -        {assume "p dvd m" hence "p \<le> m" using dvd_imp_le m by blast with m(2)
    9.19 -          have "coprime p m" by simp}
    9.20 -        ultimately have "coprime p m" 
    9.21 -          by (metis H prime_imp_coprime_nat)}
    9.22 -      hence ?rhs using p0 by auto}
    9.23 -    moreover
    9.24 -    { assume H: "\<forall>m. 0 < m \<and> m < p \<longrightarrow> coprime p m"
    9.25 -      obtain q where q: "prime q" "q dvd p"
    9.26 -        by (metis p0(2) prime_factor_nat) 
    9.27 -      have q0: "q > 0"
    9.28 -        by (metis prime_gt_0_nat q(1))
    9.29 -      from dvd_imp_le[OF q(2)] p0 have qp: "q \<le> p" by arith
    9.30 -      {assume "q = p" hence ?lhs using q(1) by blast}
    9.31 -      moreover
    9.32 -      {assume "q\<noteq>p" with qp have qplt: "q < p" by arith
    9.33 -        from H qplt q0 have "coprime p q" by arith
    9.34 -       hence ?lhs using q
    9.35 -         by (auto dest: gcd_nat.absorb2)}
    9.36 -      ultimately have ?lhs by blast}
    9.37 -    ultimately have ?thesis by blast}
    9.38 -  ultimately show ?thesis  by (cases"p=0 \<or> p=1", auto)
    9.39 -qed
    9.40 +  "prime (p::nat) \<longleftrightarrow> p \<noteq> 0 \<and> p \<noteq> 1 \<and> (\<forall>m. 0 < m \<and> m < p \<longrightarrow> coprime p m)"
    9.41 +  unfolding is_prime_nat_iff
    9.42 +proof safe
    9.43 +  fix m assume p: "p > 0" "p \<noteq> 1" and m: "m dvd p" "m \<noteq> p" 
    9.44 +           and *: "\<forall>m. m > 0 \<and> m < p \<longrightarrow> coprime p m"
    9.45 +  from p m have "m \<noteq> 0" by (intro notI) auto
    9.46 +  moreover from p m have "m < p" by (auto dest: dvd_imp_le)
    9.47 +  ultimately have "coprime p m" using * by blast
    9.48 +  with m show "m = 1" by simp
    9.49 +qed (auto simp: is_prime_nat_iff simp del: One_nat_def 
    9.50 +          intro!: is_prime_imp_coprime dest: dvd_imp_le)
    9.51  
    9.52  lemma finite_number_segment: "card { m. 0 < m \<and> m < n } = n - 1"
    9.53  proof-
    9.54 @@ -94,7 +72,7 @@
    9.55  qed
    9.56  
    9.57  lemma cong_solve_unique_nontrivial:
    9.58 -  assumes p: "prime p" and pa: "coprime p a" and x0: "0 < x" and xp: "x < p"
    9.59 +  assumes p: "prime (p::nat)" and pa: "coprime p a" and x0: "0 < x" and xp: "x < p"
    9.60    shows "\<exists>!y. 0 < y \<and> y < p \<and> [x * y = a] (mod p)"
    9.61  proof-
    9.62    from pa have ap: "coprime a p"
    9.63 @@ -107,12 +85,12 @@
    9.64      with y(2) have th: "p dvd a"
    9.65        by (auto dest: cong_dvd_eq_nat)
    9.66      have False
    9.67 -      by (metis gcd_nat.absorb1 one_not_prime_nat p pa th)}
    9.68 +      by (metis gcd_nat.absorb1 not_is_prime_1 p pa th)}
    9.69    with y show ?thesis unfolding Ex1_def using neq0_conv by blast
    9.70  qed
    9.71  
    9.72  lemma cong_unique_inverse_prime:
    9.73 -  assumes "prime p" and "0 < x" and "x < p"
    9.74 +  assumes "prime (p::nat)" and "0 < x" and "x < p"
    9.75    shows "\<exists>!y. 0 < y \<and> y < p \<and> [x * y = 1] (mod p)"
    9.76    by (rule cong_solve_unique_nontrivial) (insert assms, simp_all)
    9.77  
    9.78 @@ -445,28 +423,28 @@
    9.79  subsection\<open>Another trivial primality characterization\<close>
    9.80  
    9.81  lemma prime_prime_factor:
    9.82 -  "prime n \<longleftrightarrow> n \<noteq> 1 \<and> (\<forall>p. prime p \<and> p dvd n \<longrightarrow> p = n)" 
    9.83 +  "prime (n::nat) \<longleftrightarrow> n \<noteq> 1 \<and> (\<forall>p. prime p \<and> p dvd n \<longrightarrow> p = n)" 
    9.84    (is "?lhs \<longleftrightarrow> ?rhs")
    9.85  proof (cases "n=0 \<or> n=1")
    9.86    case True
    9.87    then show ?thesis
    9.88 -     by (metis bigger_prime dvd_0_right one_not_prime_nat zero_not_prime_nat)
    9.89 +     by (metis bigger_prime dvd_0_right not_is_prime_1 not_is_prime_0)
    9.90  next
    9.91    case False
    9.92    show ?thesis
    9.93    proof
    9.94      assume "prime n"
    9.95      then show ?rhs
    9.96 -      by (metis one_not_prime_nat prime_def)
    9.97 +      by (metis  not_is_prime_1 is_prime_nat_iff)
    9.98    next
    9.99      assume ?rhs
   9.100      with False show "prime n"
   9.101 -      by (auto simp: prime_def) (metis One_nat_def prime_factor_nat prime_def)
   9.102 +      by (auto simp: is_prime_nat_iff) (metis One_nat_def prime_factor_nat is_prime_nat_iff)
   9.103    qed
   9.104  qed
   9.105  
   9.106  lemma prime_divisor_sqrt:
   9.107 -  "prime n \<longleftrightarrow> n \<noteq> 1 \<and> (\<forall>d. d dvd n \<and> d\<^sup>2 \<le> n \<longrightarrow> d = 1)"
   9.108 +  "prime (n::nat) \<longleftrightarrow> n \<noteq> 1 \<and> (\<forall>d. d dvd n \<and> d\<^sup>2 \<le> n \<longrightarrow> d = 1)"
   9.109  proof -
   9.110    {assume "n=0 \<or> n=1" hence ?thesis
   9.111      by auto}
   9.112 @@ -497,17 +475,17 @@
   9.113          with H[rule_format, of e] h have "e=1" by simp
   9.114          with e have "d = n" by simp}
   9.115        ultimately have "d=1 \<or> d=n"  by blast}
   9.116 -    ultimately have ?thesis unfolding prime_def using np n(2) by blast}
   9.117 +    ultimately have ?thesis unfolding is_prime_nat_iff using np n(2) by blast}
   9.118    ultimately show ?thesis by auto
   9.119  qed
   9.120  
   9.121  lemma prime_prime_factor_sqrt:
   9.122 -  "prime n \<longleftrightarrow> n \<noteq> 0 \<and> n \<noteq> 1 \<and> \<not> (\<exists>p. prime p \<and> p dvd n \<and> p\<^sup>2 \<le> n)"
   9.123 +  "prime (n::nat) \<longleftrightarrow> n \<noteq> 0 \<and> n \<noteq> 1 \<and> \<not> (\<exists>p. prime p \<and> p dvd n \<and> p\<^sup>2 \<le> n)"
   9.124    (is "?lhs \<longleftrightarrow>?rhs")
   9.125  proof-
   9.126    {assume "n=0 \<or> n=1" 
   9.127     hence ?thesis
   9.128 -     by (metis one_not_prime_nat zero_not_prime_nat)}
   9.129 +     by (metis not_is_prime_0 not_is_prime_1)}
   9.130    moreover
   9.131    {assume n: "n\<noteq>0" "n\<noteq>1"
   9.132      {assume H: ?lhs
   9.133 @@ -535,10 +513,10 @@
   9.134  lemma pocklington_lemma:
   9.135    assumes n: "n \<ge> 2" and nqr: "n - 1 = q*r" and an: "[a^ (n - 1) = 1] (mod n)"
   9.136    and aq:"\<forall>p. prime p \<and> p dvd q \<longrightarrow> coprime (a^ ((n - 1) div p) - 1) n"
   9.137 -  and pp: "prime p" and pn: "p dvd n"
   9.138 +  and pp: "prime (p::nat)" and pn: "p dvd n"
   9.139    shows "[p = 1] (mod q)"
   9.140  proof -
   9.141 -  have p01: "p \<noteq> 0" "p \<noteq> 1" using pp one_not_prime_nat zero_not_prime_nat by (auto intro: prime_gt_0_nat)
   9.142 +  have p01: "p \<noteq> 0" "p \<noteq> 1" using pp by (auto intro: prime_gt_0_nat)
   9.143    obtain k where k: "a ^ (q * r) - 1 = n*k"
   9.144      by (metis an cong_to_1_nat dvd_def nqr)
   9.145    from pn[unfolded dvd_def] obtain l where l: "n = p*l" by blast
   9.146 @@ -561,7 +539,7 @@
   9.147      from aq P(1) Pq have caP:"coprime (a^ ((n - 1) div P) - 1) n" by blast
   9.148      from Pq obtain s where s: "q = P*s" unfolding dvd_def by blast
   9.149      have P0: "P \<noteq> 0" using P(1)
   9.150 -      by (metis zero_not_prime_nat) 
   9.151 +      by (metis not_is_prime_0) 
   9.152      from P(2) obtain t where t: "d = P*t" unfolding dvd_def by blast
   9.153      from d s t P0  have s': "ord p (a^r) * t = s"
   9.154        by (metis mult.commute mult_cancel1 mult.assoc) 
   9.155 @@ -581,7 +559,7 @@
   9.156    hence o: "ord p (a^r) = q" using d by simp
   9.157    from pp phi_prime[of p] have phip: "phi p = p - 1" by simp
   9.158    {fix d assume d: "d dvd p" "d dvd a" "d \<noteq> 1"
   9.159 -    from pp[unfolded prime_def] d have dp: "d = p" by blast
   9.160 +    from pp[unfolded is_prime_nat_iff] d have dp: "d = p" by blast
   9.161      from n have "n \<noteq> 0" by simp
   9.162      then have False using d dp pn
   9.163        by auto (metis One_nat_def Suc_pred an dvd_1_iff_1 gcd_greatest_iff lucas_coprime_lemma)} 
   9.164 @@ -667,36 +645,28 @@
   9.165  
   9.166  (* FIXME some overlap with material in UniqueFactorization, class unique_factorization *)
   9.167  
   9.168 -definition "primefact ps n = (foldr op * ps  1 = n \<and> (\<forall>p\<in> set ps. prime p))"
   9.169 +definition "primefact ps n = (foldr op * ps 1 = n \<and> (\<forall>p\<in> set ps. prime p))"
   9.170  
   9.171 -lemma primefact: assumes n: "n \<noteq> 0"
   9.172 +lemma primefact: 
   9.173 +  assumes n: "n \<noteq> (0::nat)"
   9.174    shows "\<exists>ps. primefact ps n"
   9.175 -using n
   9.176 -proof(induct n rule: nat_less_induct)
   9.177 -  fix n assume H: "\<forall>m<n. m \<noteq> 0 \<longrightarrow> (\<exists>ps. primefact ps m)" and n: "n\<noteq>0"
   9.178 -  let ?ths = "\<exists>ps. primefact ps n"
   9.179 -  {assume "n = 1"
   9.180 -    hence "primefact [] n" by (simp add: primefact_def)
   9.181 -    hence ?ths by blast }
   9.182 -  moreover
   9.183 -  {assume n1: "n \<noteq> 1"
   9.184 -    with n have n2: "n \<ge> 2" by arith
   9.185 -    obtain p where p: "prime p" "p dvd n"
   9.186 -      by (metis n1 prime_factor_nat) 
   9.187 -    from p(2) obtain m where m: "n = p*m" unfolding dvd_def by blast
   9.188 -    from n m have m0: "m > 0" "m\<noteq>0" by auto
   9.189 -    have "1 < p"
   9.190 -      by (metis p(1) prime_def)
   9.191 -    with m0 m have mn: "m < n" by auto
   9.192 -    from H[rule_format, OF mn m0(2)] obtain ps where ps: "primefact ps m" ..
   9.193 -    from ps m p(1) have "primefact (p#ps) n" by (simp add: primefact_def)
   9.194 -    hence ?ths by blast}
   9.195 -  ultimately show ?ths by blast
   9.196 +proof -
   9.197 +  have "\<exists>xs. mset xs = prime_factorization n" by (rule ex_mset)
   9.198 +  then guess xs .. note xs = this
   9.199 +  from assms have "n = msetprod (prime_factorization n)" 
   9.200 +    by (simp add: msetprod_prime_factorization)
   9.201 +  also have "\<dots> = msetprod (mset xs)" by (simp add: xs)
   9.202 +  also have "\<dots> = foldr op * xs 1" by (induction xs) simp_all
   9.203 +  finally have "foldr op * xs 1 = n" ..
   9.204 +  moreover have "\<forall>p\<in>#mset xs. prime p"
   9.205 +    by (subst xs) (auto dest: in_prime_factorization_imp_prime)
   9.206 +  ultimately have "primefact xs n" by (auto simp: primefact_def)
   9.207 +  thus ?thesis ..
   9.208  qed
   9.209  
   9.210  lemma primefact_contains:
   9.211    assumes pf: "primefact ps n" and p: "prime p" and pn: "p dvd n"
   9.212 -  shows "p \<in> set ps"
   9.213 +  shows "(p::nat) \<in> set ps"
   9.214    using pf p pn
   9.215  proof(induct ps arbitrary: p n)
   9.216    case Nil thus ?case by (auto simp add: primefact_def)
   9.217 @@ -705,7 +675,7 @@
   9.218    from Cons.prems[unfolded primefact_def]
   9.219    have q: "prime q" "q * foldr op * qs 1 = n" "\<forall>p \<in>set qs. prime p"  and p: "prime p" "p dvd q * foldr op * qs 1" by simp_all
   9.220    {assume "p dvd q"
   9.221 -    with p(1) q(1) have "p = q" unfolding prime_def by auto
   9.222 +    with p(1) q(1) have "p = q" unfolding is_prime_nat_iff by auto
   9.223      hence ?case by simp}
   9.224    moreover
   9.225    { assume h: "p dvd foldr op * qs 1"
   9.226 @@ -760,7 +730,7 @@
   9.227      from psp primefact_contains[OF pfpsq p]
   9.228      have p': "coprime (a ^ (r * (q div p)) mod n - 1) n"
   9.229        by (simp add: list_all_iff)
   9.230 -    from p prime_def have p01: "p \<noteq> 0" "p \<noteq> 1" "p =Suc(p - 1)" 
   9.231 +    from p is_prime_nat_iff have p01: "p \<noteq> 0" "p \<noteq> 1" "p =Suc(p - 1)" 
   9.232        by auto
   9.233      from div_mult1_eq[of r q p] p(2)
   9.234      have eq1: "r* (q div p) = (n - 1) div p"
    10.1 --- a/src/HOL/Number_Theory/Primes.thy	Wed Jul 20 14:52:09 2016 +0200
    10.2 +++ b/src/HOL/Number_Theory/Primes.thy	Thu Jul 21 10:06:04 2016 +0200
    10.3 @@ -1,5 +1,6 @@
    10.4  (*  Authors:    Christophe Tabacznyj, Lawrence C. Paulson, Amine Chaieb,
    10.5 -                Thomas M. Rasmussen, Jeremy Avigad, Tobias Nipkow
    10.6 +                Thomas M. Rasmussen, Jeremy Avigad, Tobias Nipkow, 
    10.7 +                Manuel Eberl
    10.8  
    10.9  
   10.10  This file deals with properties of primes. Definitions and lemmas are
   10.11 @@ -22,211 +23,246 @@
   10.12  natural numbers and the integers, and added a number of new theorems.
   10.13  
   10.14  Tobias Nipkow cleaned up a lot.
   10.15 +
   10.16 +Florian Haftmann and Manuel Eberl put primality and prime factorisation
   10.17 +onto an algebraic foundation and thus generalised these concepts to 
   10.18 +other rings, such as polynomials. (see also the Factorial_Ring theory).
   10.19 +
   10.20 +There were also previous formalisations of unique factorisation by 
   10.21 +Thomas Marthedal Rasmussen, Jeremy Avigad, and David Gray.
   10.22  *)
   10.23  
   10.24  
   10.25  section \<open>Primes\<close>
   10.26  
   10.27  theory Primes
   10.28 -imports "~~/src/HOL/GCD" "~~/src/HOL/Binomial"
   10.29 +imports "~~/src/HOL/Binomial" Euclidean_Algorithm
   10.30  begin
   10.31  
   10.32 +(* As a simp or intro rule,
   10.33 +
   10.34 +     prime p \<Longrightarrow> p > 0
   10.35 +
   10.36 +   wreaks havoc here. When the premise includes \<forall>x \<in># M. prime x, it
   10.37 +   leads to the backchaining
   10.38 +
   10.39 +     x > 0
   10.40 +     prime x
   10.41 +     x \<in># M   which is, unfortunately,
   10.42 +     count M x > 0
   10.43 +*)
   10.44 +
   10.45  declare [[coercion int]]
   10.46  declare [[coercion_enabled]]
   10.47  
   10.48 -definition prime :: "nat \<Rightarrow> bool"
   10.49 -  where "prime p = (1 < p \<and> (\<forall>m. m dvd p \<longrightarrow> m = 1 \<or> m = p))"
   10.50 +abbreviation (input) "prime \<equiv> is_prime"
   10.51 +
   10.52 +lemma is_prime_elem_nat_iff:
   10.53 +  "is_prime_elem (n :: nat) \<longleftrightarrow> (1 < n \<and> (\<forall>m. m dvd n \<longrightarrow> m = 1 \<or> m = n))"
   10.54 +proof safe
   10.55 +  assume *: "is_prime_elem n"
   10.56 +  from * have "n \<noteq> 0" "n \<noteq> 1" by (intro notI, simp del: One_nat_def)+
   10.57 +  thus "n > 1" by (cases n) simp_all
   10.58 +  fix m assume m: "m dvd n" "m \<noteq> n"
   10.59 +  from * \<open>m dvd n\<close> have "n dvd m \<or> is_unit m"
   10.60 +    by (intro irreducibleD' prime_imp_irreducible)
   10.61 +  with m show "m = 1" by (auto dest: dvd_antisym)
   10.62 +next
   10.63 +  assume "n > 1" "\<forall>m. m dvd n \<longrightarrow> m = 1 \<or> m = n"
   10.64 +  thus "is_prime_elem n"
   10.65 +    by (auto simp: prime_iff_irreducible irreducible_altdef)
   10.66 +qed
   10.67 +
   10.68 +lemma is_prime_nat_iff_is_prime_elem: "is_prime (n :: nat) \<longleftrightarrow> is_prime_elem n"
   10.69 +  by (simp add: is_prime_def)
   10.70  
   10.71 -subsection \<open>Primes\<close>
   10.72 +lemma is_prime_nat_iff:
   10.73 +  "is_prime (n :: nat) \<longleftrightarrow> (1 < n \<and> (\<forall>m. m dvd n \<longrightarrow> m = 1 \<or> m = n))"
   10.74 +  by (simp add: is_prime_nat_iff_is_prime_elem is_prime_elem_nat_iff)
   10.75  
   10.76 -lemma prime_odd_nat: "prime p \<Longrightarrow> p > 2 \<Longrightarrow> odd p"
   10.77 -  using nat_dvd_1_iff_1 odd_one prime_def by blast
   10.78 +lemma is_prime_elem_int_nat_transfer: "is_prime_elem (n::int) \<longleftrightarrow> is_prime_elem (nat (abs n))"
   10.79 +proof
   10.80 +  assume "is_prime_elem n"
   10.81 +  thus "is_prime_elem (nat (abs n))" by (auto simp: is_prime_elem_def nat_dvd_iff)
   10.82 +next
   10.83 +  assume "is_prime_elem (nat (abs n))"
   10.84 +  thus "is_prime_elem n"
   10.85 +    by (auto simp: dvd_int_unfold_dvd_nat is_prime_elem_def abs_mult nat_mult_distrib)
   10.86 +qed
   10.87 +
   10.88 +lemma is_prime_elem_nat_int_transfer [simp]: "is_prime_elem (int n) \<longleftrightarrow> is_prime_elem n"
   10.89 +  by (auto simp: is_prime_elem_int_nat_transfer)
   10.90 +
   10.91 +lemma is_prime_nat_int_transfer [simp]: "is_prime (int n) \<longleftrightarrow> is_prime n"
   10.92 +  by (auto simp: is_prime_elem_int_nat_transfer is_prime_def)
   10.93 +
   10.94 +lemma is_prime_int_nat_transfer: "is_prime (n::int) \<longleftrightarrow> n \<ge> 0 \<and> is_prime (nat n)"
   10.95 +  by (auto simp: is_prime_elem_int_nat_transfer is_prime_def)
   10.96  
   10.97 -lemma prime_gt_0_nat: "prime p \<Longrightarrow> p > 0"
   10.98 -  unfolding prime_def by auto
   10.99 +lemma is_prime_int_iff:
  10.100 +  "is_prime (n::int) \<longleftrightarrow> (1 < n \<and> (\<forall>m. m \<ge> 0 \<and> m dvd n \<longrightarrow> m = 1 \<or> m = n))"
  10.101 +proof (intro iffI conjI allI impI; (elim conjE)?)
  10.102 +  assume *: "is_prime n"
  10.103 +  hence irred: "irreducible n" by (simp add: prime_imp_irreducible)
  10.104 +  from * have "n \<ge> 0" "n \<noteq> 0" "n \<noteq> 1" 
  10.105 +    by (auto simp: is_prime_def zabs_def not_less split: if_splits)
  10.106 +  thus "n > 1" by presburger
  10.107 +  fix m assume "m dvd n" \<open>m \<ge> 0\<close>
  10.108 +  with irred have "m dvd 1 \<or> n dvd m" by (auto simp: irreducible_altdef)
  10.109 +  with \<open>m dvd n\<close> \<open>m \<ge> 0\<close> \<open>n > 1\<close> show "m = 1 \<or> m = n"
  10.110 +    using associated_iff_dvd[of m n] by auto
  10.111 +next
  10.112 +  assume n: "1 < n" "\<forall>m. m \<ge> 0 \<and> m dvd n \<longrightarrow> m = 1 \<or> m = n"
  10.113 +  hence "nat n > 1" by simp
  10.114 +  moreover have "\<forall>m. m dvd nat n \<longrightarrow> m = 1 \<or> m = nat n"
  10.115 +  proof (intro allI impI)
  10.116 +    fix m assume "m dvd nat n"
  10.117 +    with \<open>n > 1\<close> have "int m dvd n" by (auto simp: int_dvd_iff)
  10.118 +    with n(2) have "int m = 1 \<or> int m = n" by auto
  10.119 +    thus "m = 1 \<or> m = nat n" by auto
  10.120 +  qed
  10.121 +  ultimately show "is_prime n" 
  10.122 +    unfolding is_prime_int_nat_transfer is_prime_nat_iff by auto
  10.123 +qed
  10.124  
  10.125 -lemma prime_ge_1_nat: "prime p \<Longrightarrow> p >= 1"
  10.126 -  unfolding prime_def by auto
  10.127 +
  10.128 +lemma prime_nat_not_dvd:
  10.129 +  assumes "prime p" "p > n" "n \<noteq> (1::nat)"
  10.130 +  shows   "\<not>n dvd p"
  10.131 +proof
  10.132 +  assume "n dvd p"
  10.133 +  from assms(1) have "irreducible p" by (simp add: prime_imp_irreducible)
  10.134 +  from irreducibleD'[OF this \<open>n dvd p\<close>] \<open>n dvd p\<close> \<open>p > n\<close> assms show False
  10.135 +    by (cases "n = 0") (auto dest!: dvd_imp_le)
  10.136 +qed
  10.137  
  10.138 -lemma prime_gt_1_nat: "prime p \<Longrightarrow> p > 1"
  10.139 -  unfolding prime_def by auto
  10.140 +lemma prime_int_not_dvd:
  10.141 +  assumes "prime p" "p > n" "n > (1::int)"
  10.142 +  shows   "\<not>n dvd p"
  10.143 +proof
  10.144 +  assume "n dvd p"
  10.145 +  from assms(1) have "irreducible p" by (simp add: prime_imp_irreducible)
  10.146 +  from irreducibleD'[OF this \<open>n dvd p\<close>] \<open>n dvd p\<close> \<open>p > n\<close> assms show False
  10.147 +    by (auto dest!: zdvd_imp_le)
  10.148 +qed
  10.149 +
  10.150 +lemma prime_odd_nat: "prime p \<Longrightarrow> p > (2::nat) \<Longrightarrow> odd p"
  10.151 +  by (intro prime_nat_not_dvd) auto
  10.152 +
  10.153 +lemma prime_odd_int: "prime p \<Longrightarrow> p > (2::int) \<Longrightarrow> odd p"
  10.154 +  by (intro prime_int_not_dvd) auto
  10.155  
  10.156 -lemma prime_ge_Suc_0_nat: "prime p \<Longrightarrow> p >= Suc 0"
  10.157 -  unfolding prime_def by auto
  10.158 +lemma prime_ge_0_int: "prime p \<Longrightarrow> p \<ge> (0::int)"
  10.159 +  unfolding is_prime_int_iff by auto
  10.160 +
  10.161 +lemma prime_gt_0_nat: "prime p \<Longrightarrow> p > (0::nat)"
  10.162 +  unfolding is_prime_nat_iff by auto
  10.163 +
  10.164 +lemma prime_gt_0_int: "prime p \<Longrightarrow> p > (0::int)"
  10.165 +  unfolding is_prime_int_iff by auto
  10.166 +
  10.167 +lemma prime_ge_1_nat: "prime p \<Longrightarrow> p \<ge> (1::nat)"
  10.168 +  unfolding is_prime_nat_iff by auto
  10.169 +
  10.170 +lemma prime_ge_Suc_0_nat: "prime p \<Longrightarrow> p \<ge> Suc 0"
  10.171 +  unfolding is_prime_nat_iff by auto
  10.172 +
  10.173 +lemma prime_ge_1_int: "prime p \<Longrightarrow> p \<ge> (1::int)"
  10.174 +  unfolding is_prime_int_iff by auto
  10.175 +
  10.176 +lemma prime_gt_1_nat: "prime p \<Longrightarrow> p > (1::nat)"
  10.177 +  unfolding is_prime_nat_iff by auto
  10.178  
  10.179  lemma prime_gt_Suc_0_nat: "prime p \<Longrightarrow> p > Suc 0"
  10.180 -  unfolding prime_def by auto
  10.181 +  unfolding is_prime_nat_iff by auto
  10.182  
  10.183 -lemma prime_ge_2_nat: "prime p \<Longrightarrow> p >= 2"
  10.184 -  unfolding prime_def by auto
  10.185 +lemma prime_gt_1_int: "prime p \<Longrightarrow> p > (1::int)"
  10.186 +  unfolding is_prime_int_iff by auto
  10.187  
  10.188 -lemma prime_imp_coprime_nat: "prime p \<Longrightarrow> \<not> p dvd n \<Longrightarrow> coprime p n"
  10.189 -  apply (unfold prime_def)
  10.190 -  apply (metis gcd_dvd1 gcd_dvd2)
  10.191 -  done
  10.192 +lemma prime_ge_2_nat: "prime p \<Longrightarrow> p \<ge> (2::nat)"
  10.193 +  unfolding is_prime_nat_iff by auto
  10.194 +
  10.195 +lemma prime_ge_2_int: "prime p \<Longrightarrow> p \<ge> (2::int)"
  10.196 +  unfolding is_prime_int_iff by auto
  10.197  
  10.198  lemma prime_int_altdef:
  10.199    "prime p = (1 < p \<and> (\<forall>m::int. m \<ge> 0 \<longrightarrow> m dvd p \<longrightarrow>
  10.200      m = 1 \<or> m = p))"
  10.201 -  apply (simp add: prime_def)
  10.202 -  apply (auto simp add: )
  10.203 -  apply (metis One_nat_def of_nat_1 nat_0_le nat_dvd_iff)
  10.204 -  apply (metis zdvd_int One_nat_def le0 of_nat_0 of_nat_1 of_nat_eq_iff of_nat_le_iff)
  10.205 -  done
  10.206 -
  10.207 -lemma prime_imp_coprime_int:
  10.208 -  fixes n::int shows "prime p \<Longrightarrow> \<not> p dvd n \<Longrightarrow> coprime p n"
  10.209 -  apply (unfold prime_int_altdef)
  10.210 -  apply (metis gcd_dvd1 gcd_dvd2 gcd_ge_0_int)
  10.211 -  done
  10.212 -
  10.213 -lemma prime_dvd_mult_nat: "prime p \<Longrightarrow> p dvd m * n \<Longrightarrow> p dvd m \<or> p dvd n"
  10.214 -  by (blast intro: coprime_dvd_mult prime_imp_coprime_nat)
  10.215 -
  10.216 -lemma prime_dvd_mult_int:
  10.217 -  fixes n::int shows "prime p \<Longrightarrow> p dvd m * n \<Longrightarrow> p dvd m \<or> p dvd n"
  10.218 -  by (blast intro: coprime_dvd_mult prime_imp_coprime_int)
  10.219 -
  10.220 -lemma prime_dvd_mult_eq_nat [simp]: "prime p \<Longrightarrow>
  10.221 -    p dvd m * n = (p dvd m \<or> p dvd n)"
  10.222 -  by (rule iffI, rule prime_dvd_mult_nat, auto)
  10.223 -
  10.224 -lemma prime_dvd_mult_eq_int [simp]:
  10.225 -  fixes n::int
  10.226 -  shows "prime p \<Longrightarrow> p dvd m * n = (p dvd m \<or> p dvd n)"
  10.227 -  by (rule iffI, rule prime_dvd_mult_int, auto)
  10.228 +  unfolding is_prime_int_iff by blast
  10.229  
  10.230  lemma not_prime_eq_prod_nat:
  10.231 -  "1 < n \<Longrightarrow> \<not> prime n \<Longrightarrow>
  10.232 -    \<exists>m k. n = m * k \<and> 1 < m \<and> m < n \<and> 1 < k \<and> k < n"
  10.233 -  unfolding prime_def dvd_def apply (auto simp add: ac_simps)
  10.234 -  by (metis Suc_lessD Suc_lessI n_less_m_mult_n n_less_n_mult_m nat_0_less_mult_iff)
  10.235 -
  10.236 -lemma prime_dvd_power_nat: "prime p \<Longrightarrow> p dvd x^n \<Longrightarrow> p dvd x"
  10.237 -  by (induct n) auto
  10.238 -
  10.239 -lemma prime_dvd_power_int:
  10.240 -  fixes x::int shows "prime p \<Longrightarrow> p dvd x^n \<Longrightarrow> p dvd x"
  10.241 -  by (induct n) auto
  10.242 -
  10.243 -lemma prime_dvd_power_nat_iff: "prime p \<Longrightarrow> n > 0 \<Longrightarrow>
  10.244 -    p dvd x^n \<longleftrightarrow> p dvd x"
  10.245 -  by (cases n) (auto elim: prime_dvd_power_nat)
  10.246 -
  10.247 -lemma prime_dvd_power_int_iff:
  10.248 -  fixes x::int
  10.249 -  shows "prime p \<Longrightarrow> n > 0 \<Longrightarrow> p dvd x^n \<longleftrightarrow> p dvd x"
  10.250 -  by (cases n) (auto elim: prime_dvd_power_int)
  10.251 +  assumes "m > 1" "\<not>prime (m::nat)"
  10.252 +  shows   "\<exists>n k. n = m * k \<and> 1 < m \<and> m < n \<and> 1 < k \<and> k < n"
  10.253 +  using assms irreducible_altdef[of m]
  10.254 +  by (auto simp: prime_iff_irreducible is_prime_def irreducible_altdef)
  10.255  
  10.256  
  10.257  subsubsection \<open>Make prime naively executable\<close>
  10.258  
  10.259 -lemma zero_not_prime_nat [simp]: "~prime (0::nat)"
  10.260 -  by (simp add: prime_def)
  10.261 -
  10.262 -lemma one_not_prime_nat [simp]: "~prime (1::nat)"
  10.263 -  by (simp add: prime_def)
  10.264 +lemma Suc_0_not_prime_nat [simp]: "~prime (Suc 0)"
  10.265 +  unfolding One_nat_def [symmetric] by (rule not_is_prime_1)
  10.266  
  10.267 -lemma Suc_0_not_prime_nat [simp]: "~prime (Suc 0)"
  10.268 -  by (simp add: prime_def)
  10.269 +lemma prime_nat_code [code_unfold]:
  10.270 +  "prime (p::nat) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {1<..<p}. ~ n dvd p)"
  10.271 +proof safe
  10.272 +  assume "p > 1" and *: "\<forall>n\<in>{1<..<p}. \<not>n dvd p"
  10.273 +  show "is_prime p" unfolding is_prime_nat_iff
  10.274 +  proof (intro conjI allI impI)
  10.275 +    fix m assume "m dvd p"
  10.276 +    with \<open>p > 1\<close> have "m \<noteq> 0" by (intro notI) auto
  10.277 +    hence "m \<ge> 1" by simp
  10.278 +    moreover from \<open>m dvd p\<close> and * have "m \<notin> {1<..<p}" by blast
  10.279 +    with \<open>m dvd p\<close> and \<open>p > 1\<close> have "m \<le> 1 \<or> m = p" by (auto dest: dvd_imp_le)
  10.280 +    ultimately show "m = 1 \<or> m = p" by simp
  10.281 +  qed fact+
  10.282 +qed (auto simp: is_prime_nat_iff)
  10.283  
  10.284 -lemma prime_nat_code [code]:
  10.285 -    "prime p \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {1<..<p}. ~ n dvd p)"
  10.286 -  apply (simp add: Ball_def)
  10.287 -  apply (metis One_nat_def less_not_refl prime_def dvd_triv_right not_prime_eq_prod_nat)
  10.288 -  done
  10.289 +lemma prime_int_code [code_unfold]:
  10.290 +  "prime (p::int) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {1<..<p}. ~ n dvd p)" (is "?lhs \<longleftrightarrow> ?rhs")
  10.291 +proof
  10.292 +  assume "?lhs"
  10.293 +  thus "?rhs" by (auto simp: is_prime_int_nat_transfer dvd_int_unfold_dvd_nat prime_nat_code)
  10.294 +next
  10.295 +  assume "?rhs"
  10.296 +  thus "?lhs" by (auto simp: is_prime_int_nat_transfer zdvd_int prime_nat_code)
  10.297 +qed
  10.298  
  10.299  lemma prime_nat_simp:
  10.300      "prime p \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> set [2..<p]. \<not> n dvd p)"
  10.301    by (auto simp add: prime_nat_code)
  10.302  
  10.303 +lemma prime_int_simp:
  10.304 +    "prime (p::int) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {2..<p}. \<not> n dvd p)"
  10.305 +  by (auto simp add: prime_int_code)
  10.306 +
  10.307  lemmas prime_nat_simp_numeral [simp] = prime_nat_simp [of "numeral m"] for m
  10.308  
  10.309  lemma two_is_prime_nat [simp]: "prime (2::nat)"
  10.310    by simp
  10.311  
  10.312 +declare is_prime_int_nat_transfer[of "numeral m" for m, simp]
  10.313 +
  10.314 +
  10.315  text\<open>A bit of regression testing:\<close>
  10.316  
  10.317  lemma "prime(97::nat)" by simp
  10.318  lemma "prime(997::nat)" by eval
  10.319 -
  10.320 -
  10.321 -lemma prime_imp_power_coprime_nat: "prime p \<Longrightarrow> ~ p dvd a \<Longrightarrow> coprime a (p^m)"
  10.322 -  by (metis coprime_exp gcd.commute prime_imp_coprime_nat)
  10.323 -
  10.324 -lemma prime_imp_power_coprime_int:
  10.325 -  fixes a::int shows "prime p \<Longrightarrow> ~ p dvd a \<Longrightarrow> coprime a (p^m)"
  10.326 -  by (metis coprime_exp gcd.commute prime_imp_coprime_int)
  10.327 -
  10.328 -lemma primes_coprime_nat: "prime p \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> coprime p q"
  10.329 -  by (metis gcd_nat.absorb1 gcd_nat.absorb2 prime_imp_coprime_nat)
  10.330 -
  10.331 -lemma primes_imp_powers_coprime_nat:
  10.332 -    "prime p \<Longrightarrow> prime q \<Longrightarrow> p ~= q \<Longrightarrow> coprime (p^m) (q^n)"
  10.333 -  by (rule coprime_exp2_nat, rule primes_coprime_nat)
  10.334 -
  10.335 -lemma prime_factor_nat:
  10.336 -  "n \<noteq> (1::nat) \<Longrightarrow> \<exists>p. prime p \<and> p dvd n"
  10.337 -proof (induct n rule: nat_less_induct)
  10.338 -  case (1 n) show ?case
  10.339 -  proof (cases "n = 0")
  10.340 -    case True then show ?thesis
  10.341 -    by (auto intro: two_is_prime_nat)
  10.342 -  next
  10.343 -    case False with "1.prems" have "n > 1" by simp
  10.344 -    with "1.hyps" show ?thesis
  10.345 -    by (metis One_nat_def dvd_mult dvd_refl not_prime_eq_prod_nat order_less_irrefl)
  10.346 -  qed
  10.347 -qed
  10.348 -
  10.349 -text \<open>One property of coprimality is easier to prove via prime factors.\<close>
  10.350 +lemma "prime(97::int)" by simp
  10.351 +lemma "prime(997::int)" by eval
  10.352  
  10.353 -lemma prime_divprod_pow_nat:
  10.354 -  assumes p: "prime p" and ab: "coprime a b" and pab: "p^n dvd a * b"
  10.355 -  shows "p^n dvd a \<or> p^n dvd b"
  10.356 -proof-
  10.357 -  { assume "n = 0 \<or> a = 1 \<or> b = 1" with pab have ?thesis
  10.358 -      apply (cases "n=0", simp_all)
  10.359 -      apply (cases "a=1", simp_all)
  10.360 -      done }
  10.361 -  moreover
  10.362 -  { assume n: "n \<noteq> 0" and a: "a\<noteq>1" and b: "b\<noteq>1"
  10.363 -    then obtain m where m: "n = Suc m" by (cases n) auto
  10.364 -    from n have "p dvd p^n" apply (intro dvd_power) apply auto done
  10.365 -    also note pab
  10.366 -    finally have pab': "p dvd a * b".
  10.367 -    from prime_dvd_mult_nat[OF p pab']
  10.368 -    have "p dvd a \<or> p dvd b" .
  10.369 -    moreover
  10.370 -    { assume pa: "p dvd a"
  10.371 -      from coprime_common_divisor_nat [OF ab, OF pa] p have "\<not> p dvd b" by auto
  10.372 -      with p have "coprime b p"
  10.373 -        by (subst gcd.commute, intro prime_imp_coprime_nat)
  10.374 -      then have pnb: "coprime (p^n) b"
  10.375 -        by (subst gcd.commute, rule coprime_exp)
  10.376 -      from coprime_dvd_mult[OF pnb pab] have ?thesis by blast }
  10.377 -    moreover
  10.378 -    { assume pb: "p dvd b"
  10.379 -      have pnba: "p^n dvd b*a" using pab by (simp add: mult.commute)
  10.380 -      from coprime_common_divisor_nat [OF ab, of p] pb p have "\<not> p dvd a"
  10.381 -        by auto
  10.382 -      with p have "coprime a p"
  10.383 -        by (subst gcd.commute, intro prime_imp_coprime_nat)
  10.384 -      then have pna: "coprime (p^n) a"
  10.385 -        by (subst gcd.commute, rule coprime_exp)
  10.386 -      from coprime_dvd_mult[OF pna pnba] have ?thesis by blast }
  10.387 -    ultimately have ?thesis by blast }
  10.388 -  ultimately show ?thesis by blast
  10.389 -qed
  10.390 +lemma prime_factor_nat: 
  10.391 +  "n \<noteq> (1::nat) \<Longrightarrow> \<exists>p. prime p \<and> p dvd n"
  10.392 +  using prime_divisor_exists[of n]
  10.393 +  by (cases "n = 0") (auto intro: exI[of _ "2::nat"])
  10.394  
  10.395  
  10.396  subsection \<open>Infinitely many primes\<close>
  10.397  
  10.398 -lemma next_prime_bound: "\<exists>p. prime p \<and> n < p \<and> p <= fact n + 1"
  10.399 +lemma next_prime_bound: "\<exists>p::nat. prime p \<and> n < p \<and> p \<le> fact n + 1"
  10.400  proof-
  10.401    have f1: "fact n + 1 \<noteq> (1::nat)" using fact_ge_1 [of n, where 'a=nat] by arith
  10.402    from prime_factor_nat [OF f1]
  10.403 -  obtain p where "prime p" and "p dvd fact n + 1" by auto
  10.404 +  obtain p :: nat where "prime p" and "p dvd fact n + 1" by auto
  10.405    then have "p \<le> fact n + 1" apply (intro dvd_imp_le) apply auto done
  10.406    { assume "p \<le> n"
  10.407      from \<open>prime p\<close> have "p \<ge> 1"
  10.408 @@ -238,7 +274,7 @@
  10.409      then have "p dvd 1" by simp
  10.410      then have "p <= 1" by auto
  10.411      moreover from \<open>prime p\<close> have "p > 1"
  10.412 -      using prime_def by blast
  10.413 +      using is_prime_nat_iff by blast
  10.414      ultimately have False by auto}
  10.415    then have "n < p" by presburger
  10.416    with \<open>prime p\<close> and \<open>p <= fact n + 1\<close> show ?thesis by auto
  10.417 @@ -269,7 +305,7 @@
  10.418  proof -
  10.419    from assms have
  10.420      "1 < p * q" and P: "\<And>m. m dvd p * q \<Longrightarrow> m = 1 \<or> m = p * q"
  10.421 -    unfolding prime_def by auto
  10.422 +    unfolding is_prime_nat_iff by auto
  10.423    from \<open>1 < p * q\<close> have "p \<noteq> 0" by (cases p) auto
  10.424    then have Q: "p = p * q \<longleftrightarrow> q = 1" by auto
  10.425    have "p dvd p * q" by simp
  10.426 @@ -277,30 +313,8 @@
  10.427    then show ?thesis by (simp add: Q)
  10.428  qed
  10.429  
  10.430 -lemma prime_exp:
  10.431 -  fixes p::nat
  10.432 -  shows "prime (p^n) \<longleftrightarrow> prime p \<and> n = 1"
  10.433 -proof(induct n)
  10.434 -  case 0 thus ?case by simp
  10.435 -next
  10.436 -  case (Suc n)
  10.437 -  {assume "p = 0" hence ?case by simp}
  10.438 -  moreover
  10.439 -  {assume "p=1" hence ?case by simp}
  10.440 -  moreover
  10.441 -  {assume p: "p \<noteq> 0" "p\<noteq>1"
  10.442 -    {assume pp: "prime (p^Suc n)"
  10.443 -      hence "p = 1 \<or> p^n = 1" using prime_product[of p "p^n"] by simp
  10.444 -      with p have n: "n = 0"
  10.445 -        by (metis One_nat_def nat_power_eq_Suc_0_iff)
  10.446 -      with pp have "prime p \<and> Suc n = 1" by simp}
  10.447 -    moreover
  10.448 -    {assume n: "prime p \<and> Suc n = 1" hence "prime (p^Suc n)" by simp}
  10.449 -    ultimately have ?case by blast}
  10.450 -  ultimately show ?case by blast
  10.451 -qed
  10.452 -
  10.453 -lemma prime_power_mult:
  10.454 +(* TODO: Generalise? *)
  10.455 +lemma prime_power_mult_nat:
  10.456    fixes p::nat
  10.457    assumes p: "prime p" and xy: "x * y = p ^ k"
  10.458    shows "\<exists>i j. x = p ^i \<and> y = p^ j"
  10.459 @@ -310,7 +324,7 @@
  10.460  next
  10.461    case (Suc k x y)
  10.462    from Suc.prems have pxy: "p dvd x*y" by auto
  10.463 -  from Primes.prime_dvd_mult_nat [OF p pxy] have pxyc: "p dvd x \<or> p dvd y" .
  10.464 +  from is_prime_dvd_multD [OF p pxy] have pxyc: "p dvd x \<or> p dvd y" .
  10.465    from p have p0: "p \<noteq> 0" by - (rule ccontr, simp)
  10.466    {assume px: "p dvd x"
  10.467      then obtain d where d: "x = p*d" unfolding dvd_def by blast
  10.468 @@ -330,7 +344,7 @@
  10.469    ultimately show ?case  using pxyc by blast
  10.470  qed
  10.471  
  10.472 -lemma prime_power_exp:
  10.473 +lemma prime_power_exp_nat:
  10.474    fixes p::nat
  10.475    assumes p: "prime p" and n: "n \<noteq> 0"
  10.476      and xn: "x^n = p^k" shows "\<exists>i. x = p^i"
  10.477 @@ -342,20 +356,20 @@
  10.478    {assume "n = 0" with Suc have ?case by simp (rule exI[where x="k"], simp)}
  10.479    moreover
  10.480    {assume n: "n \<noteq> 0"
  10.481 -    from prime_power_mult[OF p th]
  10.482 +    from prime_power_mult_nat[OF p th]
  10.483      obtain i j where ij: "x = p^i" "x^n = p^j"by blast
  10.484      from Suc.hyps[OF n ij(2)] have ?case .}
  10.485    ultimately show ?case by blast
  10.486  qed
  10.487  
  10.488 -lemma divides_primepow:
  10.489 +lemma divides_primepow_nat:
  10.490    fixes p::nat
  10.491    assumes p: "prime p"
  10.492    shows "d dvd p^k \<longleftrightarrow> (\<exists> i. i \<le> k \<and> d = p ^i)"
  10.493  proof
  10.494    assume H: "d dvd p^k" then obtain e where e: "d*e = p^k"
  10.495      unfolding dvd_def  apply (auto simp add: mult.commute) by blast
  10.496 -  from prime_power_mult[OF p e] obtain i j where ij: "d = p^i" "e=p^j" by blast
  10.497 +  from prime_power_mult_nat[OF p e] obtain i j where ij: "d = p^i" "e=p^j" by blast
  10.498    from e ij have "p^(i + j) = p^k" by (simp add: power_add)
  10.499    hence "i + j = k" using p prime_gt_1_nat power_inject_exp[of p "i+j" k] by simp
  10.500    hence "i \<le> k" by arith
  10.501 @@ -369,6 +383,7 @@
  10.502    thus "\<exists>i\<le>k. d = p ^ i \<Longrightarrow> d dvd p ^ k" by blast
  10.503  qed
  10.504  
  10.505 +
  10.506  subsection \<open>Chinese Remainder Theorem Variants\<close>
  10.507  
  10.508  lemma bezout_gcd_nat:
  10.509 @@ -392,6 +407,7 @@
  10.510  
  10.511  text \<open>A binary form of the Chinese Remainder Theorem.\<close>
  10.512  
  10.513 +(* TODO: Generalise? *)
  10.514  lemma chinese_remainder:
  10.515    fixes a::nat  assumes ab: "coprime a b" and a: "a \<noteq> 0" and b: "b \<noteq> 0"
  10.516    shows "\<exists>x q1 q2. x = u + q1 * a \<and> x = v + q2 * b"
  10.517 @@ -422,11 +438,175 @@
  10.518    shows "\<exists>x y. a*x = Suc (p*y)"
  10.519  proof -
  10.520    have ap: "coprime a p"
  10.521 -    by (metis gcd.commute p pa prime_imp_coprime_nat)
  10.522 +    by (metis gcd.commute p pa is_prime_imp_coprime)
  10.523    moreover from p have "p \<noteq> 1" by auto
  10.524    ultimately have "\<exists>x y. a * x = p * y + 1"
  10.525      by (rule coprime_bezout_strong)
  10.526    then show ?thesis by simp    
  10.527  qed
  10.528 +(* END TODO *)
  10.529  
  10.530 -end
  10.531 +
  10.532 +
  10.533 +subsection \<open>Multiplicity and primality for natural numbers and integers\<close>
  10.534 +
  10.535 +lemma prime_factors_gt_0_nat:
  10.536 +  "p \<in> prime_factors x \<Longrightarrow> p > (0::nat)"
  10.537 +  by (simp add: prime_factors_prime prime_gt_0_nat)
  10.538 +
  10.539 +lemma prime_factors_gt_0_int:
  10.540 +  "p \<in> prime_factors x \<Longrightarrow> p > (0::int)"
  10.541 +  by (simp add: prime_factors_prime prime_gt_0_int)
  10.542 +
  10.543 +lemma prime_factors_ge_0_int [elim]:
  10.544 +  fixes n :: int
  10.545 +  shows "p \<in> prime_factors n \<Longrightarrow> p \<ge> 0"
  10.546 +  unfolding prime_factors_def 
  10.547 +  by (auto split: if_splits simp: is_prime_def dest!: in_prime_factorization_imp_prime)
  10.548 +
  10.549 +lemma msetprod_prime_factorization_int:
  10.550 +  fixes n :: int
  10.551 +  assumes "n > 0"
  10.552 +  shows   "msetprod (prime_factorization n) = n"
  10.553 +  using assms by (simp add: msetprod_prime_factorization)
  10.554 +
  10.555 +lemma prime_factorization_exists_nat:
  10.556 +  "n > 0 \<Longrightarrow> (\<exists>M. (\<forall>p::nat \<in> set_mset M. prime p) \<and> n = (\<Prod>i \<in># M. i))"
  10.557 +  using prime_factorization_exists[of n] by (auto simp: is_prime_def)
  10.558 +
  10.559 +lemma msetprod_prime_factorization_nat [simp]: 
  10.560 +  "(n::nat) > 0 \<Longrightarrow> msetprod (prime_factorization n) = n"
  10.561 +  by (subst msetprod_prime_factorization) simp_all
  10.562 +
  10.563 +lemma prime_factorization_nat:
  10.564 +    "n > (0::nat) \<Longrightarrow> n = (\<Prod>p \<in> prime_factors n. p ^ multiplicity p n)"
  10.565 +  by (simp add: setprod_prime_factors)
  10.566 +
  10.567 +lemma prime_factorization_int:
  10.568 +    "n > (0::int) \<Longrightarrow> n = (\<Prod>p \<in> prime_factors n. p ^ multiplicity p n)"
  10.569 +  by (simp add: setprod_prime_factors)
  10.570 +
  10.571 +lemma prime_factorization_unique_nat:
  10.572 +  fixes f :: "nat \<Rightarrow> _"
  10.573 +  assumes S_eq: "S = {p. 0 < f p}"
  10.574 +    and "finite S"
  10.575 +    and S: "\<forall>p\<in>S. prime p" "n = (\<Prod>p\<in>S. p ^ f p)"
  10.576 +  shows "S = prime_factors n \<and> (\<forall>p. is_prime p \<longrightarrow> f p = multiplicity p n)"
  10.577 +  using assms by (intro prime_factorization_unique'') auto
  10.578 +
  10.579 +lemma prime_factorization_unique_int:
  10.580 +  fixes f :: "int \<Rightarrow> _"
  10.581 +  assumes S_eq: "S = {p. 0 < f p}"
  10.582 +    and "finite S"
  10.583 +    and S: "\<forall>p\<in>S. prime p" "abs n = (\<Prod>p\<in>S. p ^ f p)"
  10.584 +  shows "S = prime_factors n \<and> (\<forall>p. is_prime p \<longrightarrow> f p = multiplicity p n)"
  10.585 +  using assms by (intro prime_factorization_unique'') auto
  10.586 +
  10.587 +lemma prime_factors_characterization_nat:
  10.588 +  "S = {p. 0 < f (p::nat)} \<Longrightarrow>
  10.589 +    finite S \<Longrightarrow> \<forall>p\<in>S. prime p \<Longrightarrow> n = (\<Prod>p\<in>S. p ^ f p) \<Longrightarrow> prime_factors n = S"
  10.590 +  by (rule prime_factorization_unique_nat [THEN conjunct1, symmetric])
  10.591 +
  10.592 +lemma prime_factors_characterization'_nat:
  10.593 +  "finite {p. 0 < f (p::nat)} \<Longrightarrow>
  10.594 +    (\<forall>p. 0 < f p \<longrightarrow> prime p) \<Longrightarrow>
  10.595 +      prime_factors (\<Prod>p | 0 < f p. p ^ f p) = {p. 0 < f p}"
  10.596 +  by (rule prime_factors_characterization_nat) auto
  10.597 +
  10.598 +lemma prime_factors_characterization_int:
  10.599 +  "S = {p. 0 < f (p::int)} \<Longrightarrow> finite S \<Longrightarrow>
  10.600 +    \<forall>p\<in>S. prime p \<Longrightarrow> abs n = (\<Prod>p\<in>S. p ^ f p) \<Longrightarrow> prime_factors n = S"
  10.601 +  by (rule prime_factorization_unique_int [THEN conjunct1, symmetric])
  10.602 +
  10.603 +(* TODO Move *)
  10.604 +lemma abs_setprod: "abs (setprod f A :: 'a :: linordered_idom) = setprod (\<lambda>x. abs (f x)) A"
  10.605 +  by (cases "finite A", induction A rule: finite_induct) (simp_all add: abs_mult)
  10.606 +
  10.607 +lemma primes_characterization'_int [rule_format]:
  10.608 +  "finite {p. p \<ge> 0 \<and> 0 < f (p::int)} \<Longrightarrow> \<forall>p. 0 < f p \<longrightarrow> prime p \<Longrightarrow>
  10.609 +      prime_factors (\<Prod>p | p \<ge> 0 \<and> 0 < f p. p ^ f p) = {p. p \<ge> 0 \<and> 0 < f p}"
  10.610 +  by (rule prime_factors_characterization_int) (auto simp: abs_setprod prime_ge_0_int)
  10.611 +
  10.612 +lemma multiplicity_characterization_nat:
  10.613 +  "S = {p. 0 < f (p::nat)} \<Longrightarrow> finite S \<Longrightarrow> \<forall>p\<in>S. prime p \<Longrightarrow> is_prime p \<Longrightarrow>
  10.614 +    n = (\<Prod>p\<in>S. p ^ f p) \<Longrightarrow> multiplicity p n = f p"
  10.615 +  by (frule prime_factorization_unique_nat [of S f n, THEN conjunct2, rule_format, symmetric]) auto
  10.616 +
  10.617 +lemma multiplicity_characterization'_nat: "finite {p. 0 < f (p::nat)} \<longrightarrow>
  10.618 +    (\<forall>p. 0 < f p \<longrightarrow> prime p) \<longrightarrow> is_prime p \<longrightarrow>
  10.619 +      multiplicity p (\<Prod>p | 0 < f p. p ^ f p) = f p"
  10.620 +  by (intro impI, rule multiplicity_characterization_nat) auto
  10.621 +
  10.622 +lemma multiplicity_characterization_int: "S = {p. 0 < f (p::int)} \<Longrightarrow>
  10.623 +    finite S \<Longrightarrow> \<forall>p\<in>S. prime p \<Longrightarrow> is_prime p \<Longrightarrow> n = (\<Prod>p\<in>S. p ^ f p) \<Longrightarrow> multiplicity p n = f p"
  10.624 +  by (frule prime_factorization_unique_int [of S f n, THEN conjunct2, rule_format, symmetric]) 
  10.625 +     (auto simp: abs_setprod power_abs prime_ge_0_int intro!: setprod.cong)
  10.626 +
  10.627 +lemma multiplicity_characterization'_int [rule_format]:
  10.628 +  "finite {p. p \<ge> 0 \<and> 0 < f (p::int)} \<Longrightarrow>
  10.629 +    (\<forall>p. 0 < f p \<longrightarrow> prime p) \<Longrightarrow> is_prime p \<Longrightarrow>
  10.630 +      multiplicity p (\<Prod>p | p \<ge> 0 \<and> 0 < f p. p ^ f p) = f p"
  10.631 +  by (rule multiplicity_characterization_int) (auto simp: prime_ge_0_int)
  10.632 +
  10.633 +lemma multiplicity_one_nat [simp]: "multiplicity p (Suc 0) = 0"
  10.634 +  unfolding One_nat_def [symmetric] by (rule multiplicity_one)
  10.635 +
  10.636 +lemma multiplicity_eq_nat:
  10.637 +  fixes x and y::nat
  10.638 +  assumes "x > 0" "y > 0" "\<And>p. is_prime p \<Longrightarrow> multiplicity p x = multiplicity p y"
  10.639 +  shows "x = y"
  10.640 +  using multiplicity_eq_imp_eq[of x y] assms by simp
  10.641 +
  10.642 +lemma multiplicity_eq_int:
  10.643 +  fixes x y :: int
  10.644 +  assumes "x > 0" "y > 0" "\<And>p. is_prime p \<Longrightarrow> multiplicity p x = multiplicity p y"
  10.645 +  shows "x = y"
  10.646 +  using multiplicity_eq_imp_eq[of x y] assms by simp
  10.647 +
  10.648 +lemma multiplicity_prod_prime_powers:
  10.649 +  assumes "finite S" "\<And>x. x \<in> S \<Longrightarrow> is_prime x" "is_prime p"
  10.650 +  shows   "multiplicity p (\<Prod>p \<in> S. p ^ f p) = (if p \<in> S then f p else 0)"
  10.651 +proof -
  10.652 +  define g where "g = (\<lambda>x. if x \<in> S then f x else 0)"
  10.653 +  define A where "A = Abs_multiset g"
  10.654 +  have "{x. g x > 0} \<subseteq> S" by (auto simp: g_def)
  10.655 +  from finite_subset[OF this assms(1)] have [simp]: "g :  multiset"
  10.656 +    by (simp add: multiset_def)
  10.657 +  from assms have count_A: "count A x = g x" for x unfolding A_def
  10.658 +    by simp
  10.659 +  have set_mset_A: "set_mset A = {x\<in>S. f x > 0}"
  10.660 +    unfolding set_mset_def count_A by (auto simp: g_def)
  10.661 +  with assms have prime: "prime x" if "x \<in># A" for x using that by auto
  10.662 +  from set_mset_A assms have "(\<Prod>p \<in> S. p ^ f p) = (\<Prod>p \<in> S. p ^ g p) "
  10.663 +    by (intro setprod.cong) (auto simp: g_def)
  10.664 +  also from set_mset_A assms have "\<dots> = (\<Prod>p \<in> set_mset A. p ^ g p)"
  10.665 +    by (intro setprod.mono_neutral_right) (auto simp: g_def set_mset_A)
  10.666 +  also have "\<dots> = msetprod A"
  10.667 +    by (auto simp: msetprod_multiplicity count_A set_mset_A intro!: setprod.cong)
  10.668 +  also from assms have "multiplicity p \<dots> = msetsum (image_mset (multiplicity p) A)"
  10.669 +    by (subst prime_multiplicity_msetprod_distrib) (auto dest: prime)
  10.670 +  also from assms have "image_mset (multiplicity p) A = image_mset (\<lambda>x. if x = p then 1 else 0) A"
  10.671 +    by (intro image_mset_cong) (auto simp: prime_multiplicity_other dest: prime)
  10.672 +  also have "msetsum \<dots> = (if p \<in> S then f p else 0)" by (simp add: msetsum_delta count_A g_def)
  10.673 +  finally show ?thesis .
  10.674 +qed
  10.675 +
  10.676 +(* TODO Legacy names *)
  10.677 +lemmas prime_imp_coprime_nat = is_prime_imp_coprime[where ?'a = nat]
  10.678 +lemmas prime_imp_coprime_int = is_prime_imp_coprime[where ?'a = int]
  10.679 +lemmas prime_dvd_mult_nat = is_prime_dvd_mult_iff[where ?'a = nat]
  10.680 +lemmas prime_dvd_mult_int = is_prime_dvd_mult_iff[where ?'a = int]
  10.681 +lemmas prime_dvd_mult_eq_nat = is_prime_dvd_mult_iff[where ?'a = nat]
  10.682 +lemmas prime_dvd_mult_eq_int = is_prime_dvd_mult_iff[where ?'a = int]
  10.683 +lemmas prime_dvd_power_nat = is_prime_dvd_power[where ?'a = nat]
  10.684 +lemmas prime_dvd_power_int = is_prime_dvd_power[where ?'a = int]
  10.685 +lemmas prime_dvd_power_nat_iff = is_prime_dvd_power_iff[where ?'a = nat]
  10.686 +lemmas prime_dvd_power_int_iff = is_prime_dvd_power_iff[where ?'a = int]
  10.687 +lemmas prime_imp_power_coprime_nat = is_prime_imp_power_coprime[where ?'a = nat]
  10.688 +lemmas prime_imp_power_coprime_int = is_prime_imp_power_coprime[where ?'a = int]
  10.689 +lemmas primes_coprime_nat = primes_coprime[where ?'a = nat]
  10.690 +lemmas primes_coprime_int = primes_coprime[where ?'a = nat]
  10.691 +lemmas prime_divprod_pow_nat = prime_divprod_pow[where ?'a = nat]
  10.692 +lemmas prime_exp = is_prime_elem_power_iff[where ?'a = nat]
  10.693 +
  10.694 +end
  10.695 \ No newline at end of file
    11.1 --- a/src/HOL/Number_Theory/Residues.thy	Wed Jul 20 14:52:09 2016 +0200
    11.2 +++ b/src/HOL/Number_Theory/Residues.thy	Thu Jul 21 10:06:04 2016 +0200
    11.3 @@ -202,9 +202,9 @@
    11.4  subsection \<open>Prime residues\<close>
    11.5  
    11.6  locale residues_prime =
    11.7 -  fixes p and R (structure)
    11.8 +  fixes p :: nat and R (structure)
    11.9    assumes p_prime [intro]: "prime p"
   11.10 -  defines "R \<equiv> residue_ring p"
   11.11 +  defines "R \<equiv> residue_ring (int p)"
   11.12  
   11.13  sublocale residues_prime < residues p
   11.14    apply (unfold R_def residues_def)
   11.15 @@ -223,7 +223,7 @@
   11.16    apply (erule notE)
   11.17    apply (subst gcd.commute)
   11.18    apply (rule prime_imp_coprime_int)
   11.19 -  apply (rule p_prime)
   11.20 +  apply (simp add: p_prime)
   11.21    apply (rule notI)
   11.22    apply (frule zdvd_imp_le)
   11.23    apply auto
   11.24 @@ -280,7 +280,7 @@
   11.25    qed
   11.26    then show ?thesis
   11.27      using \<open>2 \<le> p\<close>
   11.28 -    by (simp add: prime_def)
   11.29 +    by (simp add: is_prime_nat_iff)
   11.30         (metis One_nat_def dvd_pos_nat nat_dvd_not_less nat_neq_iff not_gr0
   11.31                not_numeral_le_zero one_dvd)
   11.32  qed
   11.33 @@ -347,19 +347,21 @@
   11.34    apply auto
   11.35    done
   11.36  
   11.37 -lemma phi_prime: "prime p \<Longrightarrow> phi p = nat p - 1"
   11.38 +lemma phi_prime: "prime (int p) \<Longrightarrow> phi p = nat p - 1"
   11.39    apply (rule residues_prime.phi_prime)
   11.40 +  apply simp
   11.41    apply (erule residues_prime.intro)
   11.42    done
   11.43  
   11.44  lemma fermat_theorem:
   11.45    fixes a :: int
   11.46 -  assumes "prime p"
   11.47 +  assumes "prime (int p)"
   11.48      and "\<not> p dvd a"
   11.49    shows "[a^(p - 1) = 1] (mod p)"
   11.50  proof -
   11.51    from assms have "[a ^ phi p = 1] (mod p)"
   11.52 -    by (auto intro!: euler_theorem dest!: prime_imp_coprime_int simp add: ac_simps)
   11.53 +    by (auto intro!: euler_theorem intro!: prime_imp_coprime_int[of p]
   11.54 +             simp: gcd.commute[of _ "int p"])
   11.55    also have "phi p = nat p - 1"
   11.56      by (rule phi_prime) (rule assms)
   11.57    finally show ?thesis
   11.58 @@ -367,7 +369,7 @@
   11.59  qed
   11.60  
   11.61  lemma fermat_theorem_nat:
   11.62 -  assumes "prime p" and "\<not> p dvd a"
   11.63 +  assumes "prime (int p)" and "\<not> p dvd a"
   11.64    shows "[a ^ (p - 1) = 1] (mod p)"
   11.65    using fermat_theorem [of p a] assms
   11.66    by (metis of_nat_1 of_nat_power transfer_int_nat_cong zdvd_int)
    12.1 --- a/src/HOL/Number_Theory/UniqueFactorization.thy	Wed Jul 20 14:52:09 2016 +0200
    12.2 +++ b/src/HOL/Number_Theory/UniqueFactorization.thy	Thu Jul 21 10:06:04 2016 +0200
    12.3 @@ -12,817 +12,4 @@
    12.4  imports Cong "~~/src/HOL/Library/Multiset"
    12.5  begin
    12.6  
    12.7 -(* As a simp or intro rule,
    12.8 -
    12.9 -     prime p \<Longrightarrow> p > 0
   12.10 -
   12.11 -   wreaks havoc here. When the premise includes \<forall>x \<in># M. prime x, it
   12.12 -   leads to the backchaining
   12.13 -
   12.14 -     x > 0
   12.15 -     prime x
   12.16 -     x \<in># M   which is, unfortunately,
   12.17 -     count M x > 0
   12.18 -*)
   12.19 -
   12.20 -(* Here is a version of set product for multisets. Is it worth moving
   12.21 -   to multiset.thy? If so, one should similarly define msetsum for abelian
   12.22 -   semirings, using of_nat. Also, is it worth developing bounded quantifiers
   12.23 -   "\<forall>i \<in># M. P i"?
   12.24 -*)
   12.25 -
   12.26 -
   12.27 -subsection \<open>Unique factorization: multiset version\<close>
   12.28 -
   12.29 -lemma multiset_prime_factorization_exists:
   12.30 -  "n > 0 \<Longrightarrow> (\<exists>M. (\<forall>p::nat \<in> set_mset M. prime p) \<and> n = (\<Prod>i \<in># M. i))"
   12.31 -proof (induct n rule: nat_less_induct)
   12.32 -  fix n :: nat
   12.33 -  assume ih: "\<forall>m < n. 0 < m \<longrightarrow> (\<exists>M. (\<forall>p\<in>set_mset M. prime p) \<and> m = (\<Prod>i \<in># M. i))"
   12.34 -  assume "n > 0"
   12.35 -  then consider "n = 1" | "n > 1" "prime n" | "n > 1" "\<not> prime n"
   12.36 -    by arith
   12.37 -  then show "\<exists>M. (\<forall>p \<in> set_mset M. prime p) \<and> n = (\<Prod>i\<in>#M. i)"
   12.38 -  proof cases
   12.39 -    case 1
   12.40 -    then have "(\<forall>p\<in>set_mset {#}. prime p) \<and> n = (\<Prod>i \<in># {#}. i)"
   12.41 -      by auto
   12.42 -    then show ?thesis ..
   12.43 -  next
   12.44 -    case 2
   12.45 -    then have "(\<forall>p\<in>set_mset {#n#}. prime p) \<and> n = (\<Prod>i \<in># {#n#}. i)"
   12.46 -      by auto
   12.47 -    then show ?thesis ..
   12.48 -  next
   12.49 -    case 3
   12.50 -    with not_prime_eq_prod_nat
   12.51 -    obtain m k where n: "n = m * k" "1 < m" "m < n" "1 < k" "k < n"
   12.52 -      by blast
   12.53 -    with ih obtain Q R where "(\<forall>p \<in> set_mset Q. prime p) \<and> m = (\<Prod>i\<in>#Q. i)"
   12.54 -        and "(\<forall>p\<in>set_mset R. prime p) \<and> k = (\<Prod>i\<in>#R. i)"
   12.55 -      by blast
   12.56 -    then have "(\<forall>p\<in>set_mset (Q + R). prime p) \<and> n = (\<Prod>i \<in># Q + R. i)"
   12.57 -      by (auto simp add: n msetprod_Un)
   12.58 -    then show ?thesis ..
   12.59 -  qed
   12.60 -qed
   12.61 -
   12.62 -lemma multiset_prime_factorization_unique_aux:
   12.63 -  fixes a :: nat
   12.64 -  assumes "\<forall>p\<in>set_mset M. prime p"
   12.65 -    and "\<forall>p\<in>set_mset N. prime p"
   12.66 -    and "(\<Prod>i \<in># M. i) dvd (\<Prod>i \<in># N. i)"
   12.67 -  shows "count M a \<le> count N a"
   12.68 -proof (cases "a \<in> set_mset M")
   12.69 -  case True
   12.70 -  with assms have a: "prime a"
   12.71 -    by auto
   12.72 -  with True have "a ^ count M a dvd (\<Prod>i \<in># M. i)"
   12.73 -    by (auto simp add: msetprod_multiplicity)
   12.74 -  also have "\<dots> dvd (\<Prod>i \<in># N. i)"
   12.75 -    by (rule assms)
   12.76 -  also have "\<dots> = (\<Prod>i \<in> set_mset N. i ^ count N i)"
   12.77 -    by (simp add: msetprod_multiplicity)
   12.78 -  also have "\<dots> = a ^ count N a * (\<Prod>i \<in> (set_mset N - {a}). i ^ count N i)"
   12.79 -  proof (cases "a \<in> set_mset N")
   12.80 -    case True
   12.81 -    then have b: "set_mset N = {a} \<union> (set_mset N - {a})"
   12.82 -      by auto
   12.83 -    then show ?thesis
   12.84 -      by (subst (1) b, subst setprod.union_disjoint, auto)
   12.85 -  next
   12.86 -    case False
   12.87 -    then show ?thesis
   12.88 -      by (auto simp add: not_in_iff)
   12.89 -  qed
   12.90 -  finally have "a ^ count M a dvd a ^ count N a * (\<Prod>i \<in> (set_mset N - {a}). i ^ count N i)" .
   12.91 -  moreover
   12.92 -  have "coprime (a ^ count M a) (\<Prod>i \<in> (set_mset N - {a}). i ^ count N i)"
   12.93 -    apply (subst gcd.commute)
   12.94 -    apply (rule setprod_coprime)
   12.95 -    apply (rule primes_imp_powers_coprime_nat)
   12.96 -    using assms True
   12.97 -    apply auto
   12.98 -    done
   12.99 -  ultimately have "a ^ count M a dvd a ^ count N a"
  12.100 -    by (elim coprime_dvd_mult)
  12.101 -  with a show ?thesis
  12.102 -    using power_dvd_imp_le prime_def by blast
  12.103 -next
  12.104 -  case False
  12.105 -  then show ?thesis
  12.106 -    by (auto simp add: not_in_iff)
  12.107 -qed
  12.108 -
  12.109 -lemma multiset_prime_factorization_unique:
  12.110 -  assumes "\<forall>p::nat \<in> set_mset M. prime p"
  12.111 -    and "\<forall>p \<in> set_mset N. prime p"
  12.112 -    and "(\<Prod>i \<in># M. i) = (\<Prod>i \<in># N. i)"
  12.113 -  shows "M = N"
  12.114 -proof -
  12.115 -  have "count M a = count N a" for a
  12.116 -  proof -
  12.117 -    from assms have "count M a \<le> count N a"
  12.118 -      by (intro multiset_prime_factorization_unique_aux, auto)
  12.119 -    moreover from assms have "count N a \<le> count M a"
  12.120 -      by (intro multiset_prime_factorization_unique_aux, auto)
  12.121 -    ultimately show ?thesis
  12.122 -      by auto
  12.123 -  qed
  12.124 -  then show ?thesis
  12.125 -    by (simp add: multiset_eq_iff)
  12.126 -qed
  12.127 -
  12.128 -definition multiset_prime_factorization :: "nat \<Rightarrow> nat multiset"
  12.129 -where
  12.130 -  "multiset_prime_factorization n =
  12.131 -    (if n > 0
  12.132 -     then THE M. (\<forall>p \<in> set_mset M. prime p) \<and> n = (\<Prod>i \<in># M. i)
  12.133 -     else {#})"
  12.134 -
  12.135 -lemma multiset_prime_factorization: "n > 0 \<Longrightarrow>
  12.136 -    (\<forall>p \<in> set_mset (multiset_prime_factorization n). prime p) \<and>
  12.137 -       n = (\<Prod>i \<in># (multiset_prime_factorization n). i)"
  12.138 -  apply (unfold multiset_prime_factorization_def)
  12.139 -  apply clarsimp
  12.140 -  apply (frule multiset_prime_factorization_exists)
  12.141 -  apply clarify
  12.142 -  apply (rule theI)
  12.143 -  apply (insert multiset_prime_factorization_unique)
  12.144 -  apply auto
  12.145 -  done
  12.146 -
  12.147 -
  12.148 -subsection \<open>Prime factors and multiplicity for nat and int\<close>
  12.149 -
  12.150 -class unique_factorization =
  12.151 -  fixes multiplicity :: "'a \<Rightarrow> 'a \<Rightarrow> nat"
  12.152 -    and prime_factors :: "'a \<Rightarrow> 'a set"
  12.153 -
  12.154 -text \<open>Definitions for the natural numbers.\<close>
  12.155 -instantiation nat :: unique_factorization
  12.156 -begin
  12.157 -
  12.158 -definition multiplicity_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
  12.159 -  where "multiplicity_nat p n = count (multiset_prime_factorization n) p"
  12.160 -
  12.161 -definition prime_factors_nat :: "nat \<Rightarrow> nat set"
  12.162 -  where "prime_factors_nat n = set_mset (multiset_prime_factorization n)"
  12.163 -
  12.164 -instance ..
  12.165 -
  12.166  end
  12.167 -
  12.168 -text \<open>Definitions for the integers.\<close>
  12.169 -instantiation int :: unique_factorization
  12.170 -begin
  12.171 -
  12.172 -definition multiplicity_int :: "int \<Rightarrow> int \<Rightarrow> nat"
  12.173 -  where "multiplicity_int p n = multiplicity (nat p) (nat n)"
  12.174 -
  12.175 -definition prime_factors_int :: "int \<Rightarrow> int set"
  12.176 -  where "prime_factors_int n = int ` (prime_factors (nat n))"
  12.177 -
  12.178 -instance ..
  12.179 -
  12.180 -end
  12.181 -
  12.182 -
  12.183 -subsection \<open>Set up transfer\<close>
  12.184 -
  12.185 -lemma transfer_nat_int_prime_factors: "prime_factors (nat n) = nat ` prime_factors n"
  12.186 -  unfolding prime_factors_int_def
  12.187 -  apply auto
  12.188 -  apply (subst transfer_int_nat_set_return_embed)
  12.189 -  apply assumption
  12.190 -  done
  12.191 -
  12.192 -lemma transfer_nat_int_prime_factors_closure: "n \<ge> 0 \<Longrightarrow> nat_set (prime_factors n)"
  12.193 -  by (auto simp add: nat_set_def prime_factors_int_def)
  12.194 -
  12.195 -lemma transfer_nat_int_multiplicity:
  12.196 -  "p \<ge> 0 \<Longrightarrow> n \<ge> 0 \<Longrightarrow> multiplicity (nat p) (nat n) = multiplicity p n"
  12.197 -  by (auto simp add: multiplicity_int_def)
  12.198 -
  12.199 -declare transfer_morphism_nat_int[transfer add return:
  12.200 -  transfer_nat_int_prime_factors transfer_nat_int_prime_factors_closure
  12.201 -  transfer_nat_int_multiplicity]
  12.202 -
  12.203 -lemma transfer_int_nat_prime_factors: "prime_factors (int n) = int ` prime_factors n"
  12.204 -  unfolding prime_factors_int_def by auto
  12.205 -
  12.206 -lemma transfer_int_nat_prime_factors_closure: "is_nat n \<Longrightarrow> nat_set (prime_factors n)"
  12.207 -  by (simp only: transfer_nat_int_prime_factors_closure is_nat_def)
  12.208 -
  12.209 -lemma transfer_int_nat_multiplicity: "multiplicity (int p) (int n) = multiplicity p n"
  12.210 -  by (auto simp add: multiplicity_int_def)
  12.211 -
  12.212 -declare transfer_morphism_int_nat[transfer add return:
  12.213 -  transfer_int_nat_prime_factors transfer_int_nat_prime_factors_closure
  12.214 -  transfer_int_nat_multiplicity]
  12.215 -
  12.216 -
  12.217 -subsection \<open>Properties of prime factors and multiplicity for nat and int\<close>
  12.218 -
  12.219 -lemma prime_factors_ge_0_int [elim]:
  12.220 -  fixes n :: int
  12.221 -  shows "p \<in> prime_factors n \<Longrightarrow> p \<ge> 0"
  12.222 -  unfolding prime_factors_int_def by auto
  12.223 -
  12.224 -lemma prime_factors_prime_nat [intro]:
  12.225 -  fixes n :: nat
  12.226 -  shows "p \<in> prime_factors n \<Longrightarrow> prime p"
  12.227 -  apply (cases "n = 0")
  12.228 -  apply (simp add: prime_factors_nat_def multiset_prime_factorization_def)
  12.229 -  apply (auto simp add: prime_factors_nat_def multiset_prime_factorization)
  12.230 -  done
  12.231 -
  12.232 -lemma prime_factors_prime_int [intro]:
  12.233 -  fixes n :: int
  12.234 -  assumes "n \<ge> 0" and "p \<in> prime_factors n"
  12.235 -  shows "prime p"
  12.236 -  apply (rule prime_factors_prime_nat [transferred, of n p, simplified])
  12.237 -  using assms apply auto
  12.238 -  done
  12.239 -
  12.240 -lemma prime_factors_gt_0_nat:
  12.241 -  fixes p :: nat
  12.242 -  shows "p \<in> prime_factors x \<Longrightarrow> p > 0"
  12.243 -    using prime_factors_prime_nat by force
  12.244 -
  12.245 -lemma prime_factors_gt_0_int:
  12.246 -  shows "x \<ge> 0 \<Longrightarrow> p \<in> prime_factors x \<Longrightarrow> int p > (0::int)"
  12.247 -    by (simp add: prime_factors_gt_0_nat)
  12.248 -
  12.249 -lemma prime_factors_finite_nat [iff]:
  12.250 -  fixes n :: nat
  12.251 -  shows "finite (prime_factors n)"
  12.252 -  unfolding prime_factors_nat_def by auto
  12.253 -
  12.254 -lemma prime_factors_finite_int [iff]:
  12.255 -  fixes n :: int
  12.256 -  shows "finite (prime_factors n)"
  12.257 -  unfolding prime_factors_int_def by auto
  12.258 -
  12.259 -lemma prime_factors_altdef_nat:
  12.260 -  fixes n :: nat
  12.261 -  shows "prime_factors n = {p. multiplicity p n > 0}"
  12.262 -  by (force simp add: prime_factors_nat_def multiplicity_nat_def)
  12.263 -
  12.264 -lemma prime_factors_altdef_int:
  12.265 -  fixes n :: int
  12.266 -  shows "prime_factors n = {p. p \<ge> 0 \<and> multiplicity p n > 0}"
  12.267 -  apply (unfold prime_factors_int_def multiplicity_int_def)
  12.268 -  apply (subst prime_factors_altdef_nat)
  12.269 -  apply (auto simp add: image_def)
  12.270 -  done
  12.271 -
  12.272 -lemma prime_factorization_nat:
  12.273 -  fixes n :: nat
  12.274 -  shows "n > 0 \<Longrightarrow> n = (\<Prod>p \<in> prime_factors n. p ^ multiplicity p n)"
  12.275 -  apply (frule multiset_prime_factorization)
  12.276 -  apply (simp add: prime_factors_nat_def multiplicity_nat_def msetprod_multiplicity)
  12.277 -  done
  12.278 -
  12.279 -lemma prime_factorization_int:
  12.280 -  fixes n :: int
  12.281 -  assumes "n > 0"
  12.282 -  shows "n = (\<Prod>p \<in> prime_factors n. p ^ multiplicity p n)"
  12.283 -  apply (rule prime_factorization_nat [transferred, of n])
  12.284 -  using assms apply auto
  12.285 -  done
  12.286 -
  12.287 -lemma prime_factorization_unique_nat:
  12.288 -  fixes f :: "nat \<Rightarrow> _"
  12.289 -  assumes S_eq: "S = {p. 0 < f p}"
  12.290 -    and "finite S"
  12.291 -    and S: "\<forall>p\<in>S. prime p" "n = (\<Prod>p\<in>S. p ^ f p)"
  12.292 -  shows "S = prime_factors n \<and> (\<forall>p. f p = multiplicity p n)"
  12.293 -proof -
  12.294 -  from assms have "f \<in> multiset"
  12.295 -    by (auto simp add: multiset_def)
  12.296 -  moreover from assms have "n > 0" 
  12.297 -    by (auto intro: prime_gt_0_nat)
  12.298 -  ultimately have "multiset_prime_factorization n = Abs_multiset f"
  12.299 -    apply (unfold multiset_prime_factorization_def)
  12.300 -    apply (subst if_P, assumption)
  12.301 -    apply (rule the1_equality)
  12.302 -    apply (rule ex_ex1I)
  12.303 -    apply (rule multiset_prime_factorization_exists, assumption)
  12.304 -    apply (rule multiset_prime_factorization_unique)
  12.305 -    apply force
  12.306 -    apply force
  12.307 -    apply force
  12.308 -    using S S_eq  apply (simp add: set_mset_def msetprod_multiplicity)
  12.309 -    done
  12.310 -  with \<open>f \<in> multiset\<close> have "count (multiset_prime_factorization n) = f"
  12.311 -    by simp
  12.312 -  with S_eq show ?thesis
  12.313 -    by (simp add: set_mset_def multiset_def prime_factors_nat_def multiplicity_nat_def)
  12.314 -qed
  12.315 -
  12.316 -lemma prime_factors_characterization_nat:
  12.317 -  "S = {p. 0 < f (p::nat)} \<Longrightarrow>
  12.318 -    finite S \<Longrightarrow> \<forall>p\<in>S. prime p \<Longrightarrow> n = (\<Prod>p\<in>S. p ^ f p) \<Longrightarrow> prime_factors n = S"
  12.319 -  by (rule prime_factorization_unique_nat [THEN conjunct1, symmetric])
  12.320 -
  12.321 -lemma prime_factors_characterization'_nat:
  12.322 -  "finite {p. 0 < f (p::nat)} \<Longrightarrow>
  12.323 -    (\<forall>p. 0 < f p \<longrightarrow> prime p) \<Longrightarrow>
  12.324 -      prime_factors (\<Prod>p | 0 < f p. p ^ f p) = {p. 0 < f p}"
  12.325 -  by (rule prime_factors_characterization_nat) auto
  12.326 -
  12.327 -(* A minor glitch:*)
  12.328 -thm prime_factors_characterization'_nat
  12.329 -    [where f = "\<lambda>x. f (int (x::nat))",
  12.330 -      transferred direction: nat "op \<le> (0::int)", rule_format]
  12.331 -
  12.332 -(*
  12.333 -  Transfer isn't smart enough to know that the "0 < f p" should
  12.334 -  remain a comparison between nats. But the transfer still works.
  12.335 -*)
  12.336 -
  12.337 -lemma primes_characterization'_int [rule_format]:
  12.338 -  "finite {p. p \<ge> 0 \<and> 0 < f (p::int)} \<Longrightarrow> \<forall>p. 0 < f p \<longrightarrow> prime p \<Longrightarrow>
  12.339 -      prime_factors (\<Prod>p | p \<ge> 0 \<and> 0 < f p. p ^ f p) = {p. p \<ge> 0 \<and> 0 < f p}"
  12.340 -  using prime_factors_characterization'_nat
  12.341 -    [where f = "\<lambda>x. f (int (x::nat))",
  12.342 -    transferred direction: nat "op \<le> (0::int)"]
  12.343 -  by auto
  12.344 -
  12.345 -lemma prime_factors_characterization_int:
  12.346 -  "S = {p. 0 < f (p::int)} \<Longrightarrow> finite S \<Longrightarrow>
  12.347 -    \<forall>p\<in>S. prime (nat p) \<Longrightarrow> n = (\<Prod>p\<in>S. p ^ f p) \<Longrightarrow> prime_factors n = S"
  12.348 -  apply simp
  12.349 -  apply (subgoal_tac "{p. 0 < f p} = {p. 0 \<le> p \<and> 0 < f p}")
  12.350 -  apply (simp only:)
  12.351 -  apply (subst primes_characterization'_int)
  12.352 -  apply simp_all
  12.353 -  apply (metis nat_int)
  12.354 -  apply (metis le_cases nat_le_0 zero_not_prime_nat)
  12.355 -  done
  12.356 -
  12.357 -lemma multiplicity_characterization_nat:
  12.358 -  "S = {p. 0 < f (p::nat)} \<Longrightarrow> finite S \<Longrightarrow> \<forall>p\<in>S. prime p \<Longrightarrow>
  12.359 -    n = (\<Prod>p\<in>S. p ^ f p) \<Longrightarrow> multiplicity p n = f p"
  12.360 -  apply (frule prime_factorization_unique_nat [THEN conjunct2, rule_format, symmetric])
  12.361 -  apply auto
  12.362 -  done
  12.363 -
  12.364 -lemma multiplicity_characterization'_nat: "finite {p. 0 < f (p::nat)} \<longrightarrow>
  12.365 -    (\<forall>p. 0 < f p \<longrightarrow> prime p) \<longrightarrow>
  12.366 -      multiplicity p (\<Prod>p | 0 < f p. p ^ f p) = f p"
  12.367 -  apply (intro impI)
  12.368 -  apply (rule multiplicity_characterization_nat)
  12.369 -  apply auto
  12.370 -  done
  12.371 -
  12.372 -lemma multiplicity_characterization'_int [rule_format]:
  12.373 -  "finite {p. p \<ge> 0 \<and> 0 < f (p::int)} \<Longrightarrow>
  12.374 -    (\<forall>p. 0 < f p \<longrightarrow> prime p) \<Longrightarrow> p \<ge> 0 \<Longrightarrow>
  12.375 -      multiplicity p (\<Prod>p | p \<ge> 0 \<and> 0 < f p. p ^ f p) = f p"
  12.376 -  apply (insert multiplicity_characterization'_nat
  12.377 -    [where f = "\<lambda>x. f (int (x::nat))",
  12.378 -      transferred direction: nat "op \<le> (0::int)", rule_format])
  12.379 -  apply auto
  12.380 -  done
  12.381 -
  12.382 -lemma multiplicity_characterization_int: "S = {p. 0 < f (p::int)} \<Longrightarrow>
  12.383 -    finite S \<Longrightarrow> \<forall>p\<in>S. prime (nat p) \<Longrightarrow> n = (\<Prod>p\<in>S. p ^ f p) \<Longrightarrow>
  12.384 -      p \<ge> 0 \<Longrightarrow> multiplicity p n = f p"
  12.385 -  apply simp
  12.386 -  apply (subgoal_tac "{p. 0 < f p} = {p. 0 \<le> p \<and> 0 < f p}")
  12.387 -  apply (simp only:)
  12.388 -  apply (subst multiplicity_characterization'_int)
  12.389 -  apply simp_all
  12.390 -  apply (metis nat_int)
  12.391 -  apply (metis le_cases nat_le_0 zero_not_prime_nat)
  12.392 -  done
  12.393 -
  12.394 -lemma multiplicity_zero_nat [simp]: "multiplicity (p::nat) 0 = 0"
  12.395 -  by (simp add: multiplicity_nat_def multiset_prime_factorization_def)
  12.396 -
  12.397 -lemma multiplicity_zero_int [simp]: "multiplicity (p::int) 0 = 0"
  12.398 -  by (simp add: multiplicity_int_def)
  12.399 -
  12.400 -lemma multiplicity_one_nat': "multiplicity p (1::nat) = 0"
  12.401 -  by (subst multiplicity_characterization_nat [where f = "\<lambda>x. 0"], auto)
  12.402 -
  12.403 -lemma multiplicity_one_nat [simp]: "multiplicity p (Suc 0) = 0"
  12.404 -  by (metis One_nat_def multiplicity_one_nat')
  12.405 -
  12.406 -lemma multiplicity_one_int [simp]: "multiplicity p (1::int) = 0"
  12.407 -  by (metis multiplicity_int_def multiplicity_one_nat' transfer_nat_int_numerals(2))
  12.408 -
  12.409 -lemma multiplicity_prime_nat [simp]: "prime p \<Longrightarrow> multiplicity p p = 1"
  12.410 -  apply (subst multiplicity_characterization_nat [where f = "\<lambda>q. if q = p then 1 else 0"])
  12.411 -  apply auto
  12.412 -  apply (metis (full_types) less_not_refl)
  12.413 -  done
  12.414 -
  12.415 -lemma multiplicity_prime_power_nat [simp]: "prime p \<Longrightarrow> multiplicity p (p ^ n) = n"
  12.416 -  apply (cases "n = 0")
  12.417 -  apply auto
  12.418 -  apply (subst multiplicity_characterization_nat [where f = "\<lambda>q. if q = p then n else 0"])
  12.419 -  apply auto
  12.420 -  apply (metis (full_types) less_not_refl)
  12.421 -  done
  12.422 -
  12.423 -lemma multiplicity_prime_power_int [simp]: "prime p \<Longrightarrow> multiplicity p (int p ^ n) = n"
  12.424 -  by (metis multiplicity_prime_power_nat of_nat_power transfer_int_nat_multiplicity)
  12.425 -
  12.426 -lemma multiplicity_nonprime_nat [simp]:
  12.427 -  fixes p n :: nat
  12.428 -  shows "\<not> prime p \<Longrightarrow> multiplicity p n = 0"
  12.429 -  apply (cases "n = 0")
  12.430 -  apply auto
  12.431 -  apply (frule multiset_prime_factorization)
  12.432 -  apply (auto simp add: multiplicity_nat_def count_eq_zero_iff)
  12.433 -  done
  12.434 -
  12.435 -lemma multiplicity_not_factor_nat [simp]:
  12.436 -  fixes p n :: nat
  12.437 -  shows "p \<notin> prime_factors n \<Longrightarrow> multiplicity p n = 0"
  12.438 -  apply (subst (asm) prime_factors_altdef_nat)
  12.439 -  apply auto
  12.440 -  done
  12.441 -
  12.442 -lemma multiplicity_not_factor_int [simp]:
  12.443 -  fixes n :: int
  12.444 -  shows "p \<ge> 0 \<Longrightarrow> p \<notin> prime_factors n \<Longrightarrow> multiplicity p n = 0"
  12.445 -  apply (subst (asm) prime_factors_altdef_int)
  12.446 -  apply auto
  12.447 -  done
  12.448 -
  12.449 -(*FIXME: messy*)
  12.450 -lemma multiplicity_product_aux_nat: "(k::nat) > 0 \<Longrightarrow> l > 0 \<Longrightarrow>
  12.451 -    (prime_factors k) \<union> (prime_factors l) = prime_factors (k * l) \<and>
  12.452 -    (\<forall>p. multiplicity p k + multiplicity p l = multiplicity p (k * l))"
  12.453 -  apply (rule prime_factorization_unique_nat)
  12.454 -  apply (simp only: prime_factors_altdef_nat)
  12.455 -  apply auto
  12.456 -  apply (subst power_add)
  12.457 -  apply (subst setprod.distrib)
  12.458 -  apply (rule arg_cong2 [where f = "\<lambda>x y. x*y"])
  12.459 -  apply (subgoal_tac "prime_factors k \<union> prime_factors l = prime_factors k \<union>
  12.460 -      (prime_factors l - prime_factors k)")
  12.461 -  apply (erule ssubst)
  12.462 -  apply (subst setprod.union_disjoint)
  12.463 -  apply auto
  12.464 -  apply (metis One_nat_def nat_mult_1_right prime_factorization_nat setprod.neutral_const)
  12.465 -  apply (subgoal_tac "prime_factors k \<union> prime_factors l = prime_factors l \<union>
  12.466 -      (prime_factors k - prime_factors l)")
  12.467 -  apply (erule ssubst)
  12.468 -  apply (subst setprod.union_disjoint)
  12.469 -  apply auto
  12.470 -  apply (subgoal_tac "(\<Prod>p\<in>prime_factors k - prime_factors l. p ^ multiplicity p l) =
  12.471 -      (\<Prod>p\<in>prime_factors k - prime_factors l. 1)")
  12.472 -  apply auto
  12.473 -  apply (metis One_nat_def nat_mult_1_right prime_factorization_nat setprod.neutral_const)
  12.474 -  done
  12.475 -
  12.476 -(* transfer doesn't have the same problem here with the right
  12.477 -   choice of rules. *)
  12.478 -
  12.479 -lemma multiplicity_product_aux_int:
  12.480 -  assumes "(k::int) > 0" and "l > 0"
  12.481 -  shows "prime_factors k \<union> prime_factors l = prime_factors (k * l) \<and>
  12.482 -    (\<forall>p \<ge> 0. multiplicity p k + multiplicity p l = multiplicity p (k * l))"
  12.483 -  apply (rule multiplicity_product_aux_nat [transferred, of l k])
  12.484 -  using assms apply auto
  12.485 -  done
  12.486 -
  12.487 -lemma prime_factors_product_nat: "(k::nat) > 0 \<Longrightarrow> l > 0 \<Longrightarrow> prime_factors (k * l) =
  12.488 -    prime_factors k \<union> prime_factors l"
  12.489 -  by (rule multiplicity_product_aux_nat [THEN conjunct1, symmetric])
  12.490 -
  12.491 -lemma prime_factors_product_int: "(k::int) > 0 \<Longrightarrow> l > 0 \<Longrightarrow> prime_factors (k * l) =
  12.492 -    prime_factors k \<union> prime_factors l"
  12.493 -  by (rule multiplicity_product_aux_int [THEN conjunct1, symmetric])
  12.494 -
  12.495 -lemma multiplicity_product_nat: "(k::nat) > 0 \<Longrightarrow> l > 0 \<Longrightarrow> multiplicity p (k * l) =
  12.496 -    multiplicity p k + multiplicity p l"
  12.497 -  by (rule multiplicity_product_aux_nat [THEN conjunct2, rule_format, symmetric])
  12.498 -
  12.499 -lemma multiplicity_product_int: "(k::int) > 0 \<Longrightarrow> l > 0 \<Longrightarrow> p \<ge> 0 \<Longrightarrow>
  12.500 -    multiplicity p (k * l) = multiplicity p k + multiplicity p l"
  12.501 -  by (rule multiplicity_product_aux_int [THEN conjunct2, rule_format, symmetric])
  12.502 -
  12.503 -lemma multiplicity_setprod_nat: "finite S \<Longrightarrow> \<forall>x\<in>S. f x > 0 \<Longrightarrow>
  12.504 -    multiplicity (p::nat) (\<Prod>x \<in> S. f x) = (\<Sum>x \<in> S. multiplicity p (f x))"
  12.505 -  apply (induct set: finite)
  12.506 -  apply auto
  12.507 -  apply (subst multiplicity_product_nat)
  12.508 -  apply auto
  12.509 -  done
  12.510 -
  12.511 -(* Transfer is delicate here for two reasons: first, because there is
  12.512 -   an implicit quantifier over functions (f), and, second, because the
  12.513 -   product over the multiplicity should not be translated to an integer
  12.514 -   product.
  12.515 -
  12.516 -   The way to handle the first is to use quantifier rules for functions.
  12.517 -   The way to handle the second is to turn off the offending rule.
  12.518 -*)
  12.519 -
  12.520 -lemma transfer_nat_int_sum_prod_closure3: "(\<Sum>x \<in> A. int (f x)) \<ge> 0" "(\<Prod>x \<in> A. int (f x)) \<ge> 0"
  12.521 -  apply (rule setsum_nonneg; auto)
  12.522 -  apply (rule setprod_nonneg; auto)
  12.523 -  done
  12.524 -
  12.525 -declare transfer_morphism_nat_int[transfer
  12.526 -  add return: transfer_nat_int_sum_prod_closure3
  12.527 -  del: transfer_nat_int_sum_prod2 (1)]
  12.528 -
  12.529 -lemma multiplicity_setprod_int: "p \<ge> 0 \<Longrightarrow> finite S \<Longrightarrow> \<forall>x\<in>S. f x > 0 \<Longrightarrow>
  12.530 -    multiplicity (p::int) (\<Prod>x \<in> S. f x) = (\<Sum>x \<in> S. multiplicity p (f x))"
  12.531 -  apply (frule multiplicity_setprod_nat
  12.532 -    [where f = "\<lambda>x. nat(int(nat(f x)))",
  12.533 -      transferred direction: nat "op \<le> (0::int)"])
  12.534 -  apply auto
  12.535 -  apply (subst (asm) setprod.cong)
  12.536 -  apply (rule refl)
  12.537 -  apply (rule if_P)
  12.538 -  apply auto
  12.539 -  apply (rule setsum.cong)
  12.540 -  apply auto
  12.541 -  done
  12.542 -
  12.543 -declare transfer_morphism_nat_int[transfer
  12.544 -  add return: transfer_nat_int_sum_prod2 (1)]
  12.545 -
  12.546 -lemma multiplicity_prod_prime_powers_nat:
  12.547 -    "finite S \<Longrightarrow> \<forall>p\<in>S. prime (p::nat) \<Longrightarrow>
  12.548 -       multiplicity p (\<Prod>p \<in> S. p ^ f p) = (if p \<in> S then f p else 0)"
  12.549 -  apply (subgoal_tac "(\<Prod>p \<in> S. p ^ f p) = (\<Prod>p \<in> S. p ^ (\<lambda>x. if x \<in> S then f x else 0) p)")
  12.550 -  apply (erule ssubst)
  12.551 -  apply (subst multiplicity_characterization_nat)
  12.552 -  prefer 5 apply (rule refl)
  12.553 -  apply (rule refl)
  12.554 -  apply auto
  12.555 -  apply (subst setprod.mono_neutral_right)
  12.556 -  apply assumption
  12.557 -  prefer 3
  12.558 -  apply (rule setprod.cong)
  12.559 -  apply (rule refl)
  12.560 -  apply auto
  12.561 -  done
  12.562 -
  12.563 -(* Here the issue with transfer is the implicit quantifier over S *)
  12.564 -
  12.565 -lemma multiplicity_prod_prime_powers_int:
  12.566 -    "(p::int) \<ge> 0 \<Longrightarrow> finite S \<Longrightarrow> \<forall>p\<in>S. prime (nat p) \<Longrightarrow>
  12.567 -       multiplicity p (\<Prod>p \<in> S. p ^ f p) = (if p \<in> S then f p else 0)"
  12.568 -  apply (subgoal_tac "int ` nat ` S = S")
  12.569 -  apply (frule multiplicity_prod_prime_powers_nat
  12.570 -    [where f = "\<lambda>x. f(int x)" and S = "nat ` S", transferred])
  12.571 -  apply auto
  12.572 -  apply (metis linear nat_0_iff zero_not_prime_nat)
  12.573 -  apply (metis (full_types) image_iff int_nat_eq less_le less_linear nat_0_iff zero_not_prime_nat)
  12.574 -  done
  12.575 -
  12.576 -lemma multiplicity_distinct_prime_power_nat:
  12.577 -    "prime p \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> multiplicity p (q ^ n) = 0"
  12.578 -  apply (subgoal_tac "q ^ n = setprod (\<lambda>x. x ^ n) {q}")
  12.579 -  apply (erule ssubst)
  12.580 -  apply (subst multiplicity_prod_prime_powers_nat)
  12.581 -  apply auto
  12.582 -  done
  12.583 -
  12.584 -lemma multiplicity_distinct_prime_power_int:
  12.585 -    "prime p \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> multiplicity p (int q ^ n) = 0"
  12.586 -  by (metis multiplicity_distinct_prime_power_nat of_nat_power transfer_int_nat_multiplicity)
  12.587 -
  12.588 -lemma dvd_multiplicity_nat:
  12.589 -  fixes x y :: nat
  12.590 -  shows "0 < y \<Longrightarrow> x dvd y \<Longrightarrow> multiplicity p x \<le> multiplicity p y"
  12.591 -  apply (cases "x = 0")
  12.592 -  apply (auto simp add: dvd_def multiplicity_product_nat)
  12.593 -  done
  12.594 -
  12.595 -lemma dvd_multiplicity_int:
  12.596 -  fixes p x y :: int
  12.597 -  shows "0 < y \<Longrightarrow> 0 \<le> x \<Longrightarrow> x dvd y \<Longrightarrow> p \<ge> 0 \<Longrightarrow> multiplicity p x \<le> multiplicity p y"
  12.598 -  apply (cases "x = 0")
  12.599 -  apply (auto simp add: dvd_def)
  12.600 -  apply (subgoal_tac "0 < k")
  12.601 -  apply (auto simp add: multiplicity_product_int)
  12.602 -  apply (erule zero_less_mult_pos)
  12.603 -  apply arith
  12.604 -  done
  12.605 -
  12.606 -lemma dvd_prime_factors_nat [intro]:
  12.607 -  fixes x y :: nat
  12.608 -  shows "0 < y \<Longrightarrow> x dvd y \<Longrightarrow> prime_factors x \<le> prime_factors y"
  12.609 -  apply (simp only: prime_factors_altdef_nat)
  12.610 -  apply auto
  12.611 -  apply (metis dvd_multiplicity_nat le_0_eq neq0_conv)
  12.612 -  done
  12.613 -
  12.614 -lemma dvd_prime_factors_int [intro]:
  12.615 -  fixes x y :: int
  12.616 -  shows "0 < y \<Longrightarrow> 0 \<le> x \<Longrightarrow> x dvd y \<Longrightarrow> prime_factors x \<le> prime_factors y"
  12.617 -  apply (auto simp add: prime_factors_altdef_int)
  12.618 -  apply (metis dvd_multiplicity_int le_0_eq neq0_conv)
  12.619 -  done
  12.620 -
  12.621 -lemma multiplicity_dvd_nat:
  12.622 -  fixes x y :: nat
  12.623 -  shows "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> \<forall>p. multiplicity p x \<le> multiplicity p y \<Longrightarrow> x dvd y"
  12.624 -  apply (subst prime_factorization_nat [of x], assumption)
  12.625 -  apply (subst prime_factorization_nat [of y], assumption)
  12.626 -  apply (rule setprod_dvd_setprod_subset2)
  12.627 -  apply force
  12.628 -  apply (subst prime_factors_altdef_nat)+
  12.629 -  apply auto
  12.630 -  apply (metis gr0I le_0_eq less_not_refl)
  12.631 -  apply (metis le_imp_power_dvd)
  12.632 -  done
  12.633 -
  12.634 -lemma multiplicity_dvd_int:
  12.635 -  fixes x y :: int
  12.636 -  shows "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> \<forall>p\<ge>0. multiplicity p x \<le> multiplicity p y \<Longrightarrow> x dvd y"
  12.637 -  apply (subst prime_factorization_int [of x], assumption)
  12.638 -  apply (subst prime_factorization_int [of y], assumption)
  12.639 -  apply (rule setprod_dvd_setprod_subset2)
  12.640 -  apply force
  12.641 -  apply (subst prime_factors_altdef_int)+
  12.642 -  apply auto
  12.643 -  apply (metis le_imp_power_dvd prime_factors_ge_0_int)
  12.644 -  done
  12.645 -
  12.646 -lemma multiplicity_dvd'_nat:
  12.647 -  fixes x y :: nat
  12.648 -  assumes "0 < x"
  12.649 -  assumes "\<forall>p. prime p \<longrightarrow> multiplicity p x \<le> multiplicity p y"
  12.650 -  shows "x dvd y"
  12.651 -  using dvd_0_right assms by (metis (no_types) le0 multiplicity_dvd_nat multiplicity_nonprime_nat not_gr0)
  12.652 -
  12.653 -lemma multiplicity_dvd'_int:
  12.654 -  fixes x y :: int
  12.655 -  shows "0 < x \<Longrightarrow> 0 \<le> y \<Longrightarrow>
  12.656 -    \<forall>p. prime p \<longrightarrow> multiplicity p x \<le> multiplicity p y \<Longrightarrow> x dvd y"
  12.657 -  by (metis dvd_int_iff abs_of_nat multiplicity_dvd'_nat multiplicity_int_def nat_int
  12.658 -    zero_le_imp_eq_int zero_less_imp_eq_int)
  12.659 -
  12.660 -lemma dvd_multiplicity_eq_nat:
  12.661 -  fixes x y :: nat
  12.662 -  shows "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> x dvd y \<longleftrightarrow> (\<forall>p. multiplicity p x \<le> multiplicity p y)"
  12.663 -  by (auto intro: dvd_multiplicity_nat multiplicity_dvd_nat)
  12.664 -
  12.665 -lemma dvd_multiplicity_eq_int: "0 < (x::int) \<Longrightarrow> 0 < y \<Longrightarrow>
  12.666 -    (x dvd y) = (\<forall>p\<ge>0. multiplicity p x \<le> multiplicity p y)"
  12.667 -  by (auto intro: dvd_multiplicity_int multiplicity_dvd_int)
  12.668 -
  12.669 -lemma prime_factors_altdef2_nat:
  12.670 -  fixes n :: nat
  12.671 -  shows "n > 0 \<Longrightarrow> p \<in> prime_factors n \<longleftrightarrow> prime p \<and> p dvd n"
  12.672 -  apply (cases "prime p")
  12.673 -  apply auto
  12.674 -  apply (subst prime_factorization_nat [where n = n], assumption)
  12.675 -  apply (rule dvd_trans)
  12.676 -  apply (rule dvd_power [where x = p and n = "multiplicity p n"])
  12.677 -  apply (subst (asm) prime_factors_altdef_nat, force)
  12.678 -  apply rule
  12.679 -  apply auto
  12.680 -  apply (metis One_nat_def Zero_not_Suc dvd_multiplicity_nat le0
  12.681 -    le_antisym multiplicity_not_factor_nat multiplicity_prime_nat)
  12.682 -  done
  12.683 -
  12.684 -lemma prime_factors_altdef2_int:
  12.685 -  fixes n :: int
  12.686 -  assumes "n > 0"
  12.687 -  shows "p \<in> prime_factors n \<longleftrightarrow> prime p \<and> p dvd n"
  12.688 -  using assms by (simp add:  prime_factors_altdef2_nat [transferred])
  12.689 -
  12.690 -lemma multiplicity_eq_nat:
  12.691 -  fixes x and y::nat
  12.692 -  assumes [arith]: "x > 0" "y > 0"
  12.693 -    and mult_eq [simp]: "\<And>p. prime p \<Longrightarrow> multiplicity p x = multiplicity p y"
  12.694 -  shows "x = y"
  12.695 -  apply (rule dvd_antisym)
  12.696 -  apply (auto intro: multiplicity_dvd'_nat)
  12.697 -  done
  12.698 -
  12.699 -lemma multiplicity_eq_int:
  12.700 -  fixes x y :: int
  12.701 -  assumes [arith]: "x > 0" "y > 0"
  12.702 -    and mult_eq [simp]: "\<And>p. prime p \<Longrightarrow> multiplicity p x = multiplicity p y"
  12.703 -  shows "x = y"
  12.704 -  apply (rule dvd_antisym [transferred])
  12.705 -  apply (auto intro: multiplicity_dvd'_int)
  12.706 -  done
  12.707 -
  12.708 -
  12.709 -subsection \<open>An application\<close>
  12.710 -
  12.711 -lemma gcd_eq_nat:
  12.712 -  fixes x y :: nat
  12.713 -  assumes pos [arith]: "x > 0" "y > 0"
  12.714 -  shows "gcd x y =
  12.715 -    (\<Prod>p \<in> prime_factors x \<union> prime_factors y. p ^ min (multiplicity p x) (multiplicity p y))"
  12.716 -  (is "_ = ?z")
  12.717 -proof -
  12.718 -  have [arith]: "?z > 0" 
  12.719 -    using prime_factors_gt_0_nat by auto
  12.720 -  have aux: "\<And>p. prime p \<Longrightarrow> multiplicity p ?z = min (multiplicity p x) (multiplicity p y)"
  12.721 -    apply (subst multiplicity_prod_prime_powers_nat)
  12.722 -    apply auto
  12.723 -    done
  12.724 -  have "?z dvd x"
  12.725 -    by (intro multiplicity_dvd'_nat) (auto simp add: aux intro: prime_gt_0_nat)
  12.726 -  moreover have "?z dvd y"
  12.727 -    by (intro multiplicity_dvd'_nat) (auto simp add: aux intro: prime_gt_0_nat)
  12.728 -  moreover have "w dvd x \<and> w dvd y \<longrightarrow> w dvd ?z" for w
  12.729 -  proof (cases "w = 0")
  12.730 -    case True
  12.731 -    then show ?thesis by simp
  12.732 -  next
  12.733 -    case False
  12.734 -    then show ?thesis
  12.735 -      apply auto
  12.736 -      apply (erule multiplicity_dvd'_nat)
  12.737 -      apply (auto intro: dvd_multiplicity_nat simp add: aux)
  12.738 -      done
  12.739 -  qed
  12.740 -  ultimately have "?z = gcd x y"
  12.741 -    by (subst gcd_unique_nat [symmetric], blast)
  12.742 -  then show ?thesis
  12.743 -    by auto
  12.744 -qed
  12.745 -
  12.746 -lemma lcm_eq_nat:
  12.747 -  assumes pos [arith]: "x > 0" "y > 0"
  12.748 -  shows "lcm (x::nat) y =
  12.749 -    (\<Prod>p \<in> prime_factors x \<union> prime_factors y. p ^ max (multiplicity p x) (multiplicity p y))"
  12.750 -  (is "_ = ?z")
  12.751 -proof -
  12.752 -  have [arith]: "?z > 0"
  12.753 -    by (auto intro: prime_gt_0_nat)
  12.754 -  have aux: "\<And>p. prime p \<Longrightarrow> multiplicity p ?z = max (multiplicity p x) (multiplicity p y)"
  12.755 -    apply (subst multiplicity_prod_prime_powers_nat)
  12.756 -    apply auto
  12.757 -    done
  12.758 -  have "x dvd ?z"
  12.759 -    by (intro multiplicity_dvd'_nat) (auto simp add: aux)
  12.760 -  moreover have "y dvd ?z"
  12.761 -    by (intro multiplicity_dvd'_nat) (auto simp add: aux)
  12.762 -  moreover have "x dvd w \<and> y dvd w \<longrightarrow> ?z dvd w" for w
  12.763 -  proof (cases "w = 0")
  12.764 -    case True
  12.765 -    then show ?thesis by auto
  12.766 -  next
  12.767 -    case False
  12.768 -    then show ?thesis
  12.769 -      apply auto
  12.770 -      apply (rule multiplicity_dvd'_nat)
  12.771 -      apply (auto intro: prime_gt_0_nat dvd_multiplicity_nat simp add: aux)
  12.772 -      done
  12.773 -  qed
  12.774 -  ultimately have "?z = lcm x y"
  12.775 -    by (subst lcm_unique_nat [symmetric], blast)
  12.776 -  then show ?thesis
  12.777 -    by auto
  12.778 -qed
  12.779 -
  12.780 -lemma multiplicity_gcd_nat:
  12.781 -  fixes p x y :: nat
  12.782 -  assumes [arith]: "x > 0" "y > 0"
  12.783 -  shows "multiplicity p (gcd x y) = min (multiplicity p x) (multiplicity p y)"
  12.784 -  apply (subst gcd_eq_nat)
  12.785 -  apply auto
  12.786 -  apply (subst multiplicity_prod_prime_powers_nat)
  12.787 -  apply auto
  12.788 -  done
  12.789 -
  12.790 -lemma multiplicity_lcm_nat:
  12.791 -  fixes p x y :: nat
  12.792 -  assumes [arith]: "x > 0" "y > 0"
  12.793 -  shows "multiplicity p (lcm x y) = max (multiplicity p x) (multiplicity p y)"
  12.794 -  apply (subst lcm_eq_nat)
  12.795 -  apply auto
  12.796 -  apply (subst multiplicity_prod_prime_powers_nat)
  12.797 -  apply auto
  12.798 -  done
  12.799 -
  12.800 -lemma gcd_lcm_distrib_nat:
  12.801 -  fixes x y z :: nat
  12.802 -  shows "gcd x (lcm y z) = lcm (gcd x y) (gcd x z)"
  12.803 -  apply (cases "x = 0 | y = 0 | z = 0")
  12.804 -  apply auto
  12.805 -  apply (rule multiplicity_eq_nat)
  12.806 -  apply (auto simp add: multiplicity_gcd_nat multiplicity_lcm_nat lcm_pos_nat)
  12.807 -  done
  12.808 -
  12.809 -lemma gcd_lcm_distrib_int:
  12.810 -  fixes x y z :: int
  12.811 -  shows "gcd x (lcm y z) = lcm (gcd x y) (gcd x z)"
  12.812 -  apply (subst (1 2 3) gcd_abs_int)
  12.813 -  apply (subst lcm_abs_int)
  12.814 -  apply (subst (2) abs_of_nonneg)
  12.815 -  apply force
  12.816 -  apply (rule gcd_lcm_distrib_nat [transferred])
  12.817 -  apply auto
  12.818 -  done
  12.819 -
  12.820 -end
    13.1 --- a/src/HOL/Proofs/Extraction/Euclid.thy	Wed Jul 20 14:52:09 2016 +0200
    13.2 +++ b/src/HOL/Proofs/Extraction/Euclid.thy	Thu Jul 21 10:06:04 2016 +0200
    13.3 @@ -27,8 +27,8 @@
    13.4  lemma prod_mn_less_k: "0 < n \<Longrightarrow> 0 < k \<Longrightarrow> Suc 0 < m \<Longrightarrow> m * n = k \<Longrightarrow> n < k"
    13.5    by (induct m) auto
    13.6  
    13.7 -lemma prime_eq: "prime p \<longleftrightarrow> 1 < p \<and> (\<forall>m. m dvd p \<longrightarrow> 1 < m \<longrightarrow> m = p)"
    13.8 -  apply (simp add: prime_def)
    13.9 +lemma prime_eq: "prime (p::nat) \<longleftrightarrow> 1 < p \<and> (\<forall>m. m dvd p \<longrightarrow> 1 < m \<longrightarrow> m = p)"
   13.10 +  apply (simp add: is_prime_nat_iff)
   13.11    apply (rule iffI)
   13.12    apply blast
   13.13    apply (erule conjE)
   13.14 @@ -45,7 +45,7 @@
   13.15    apply simp
   13.16    done
   13.17  
   13.18 -lemma prime_eq': "prime p \<longleftrightarrow> 1 < p \<and> (\<forall>m k. p = m * k \<longrightarrow> 1 < m \<longrightarrow> m = p)"
   13.19 +lemma prime_eq': "prime (p::nat) \<longleftrightarrow> 1 < p \<and> (\<forall>m k. p = m * k \<longrightarrow> 1 < m \<longrightarrow> m = p)"
   13.20    by (simp add: prime_eq dvd_def HOL.all_simps [symmetric] del: HOL.all_simps)
   13.21  
   13.22  lemma not_prime_ex_mk:
   13.23 @@ -207,7 +207,7 @@
   13.24  
   13.25  text \<open>Euclid's theorem: there are infinitely many primes.\<close>
   13.26  
   13.27 -lemma Euclid: "\<exists>p. prime p \<and> n < p"
   13.28 +lemma Euclid: "\<exists>p::nat. prime p \<and> n < p"
   13.29  proof -
   13.30    let ?k = "fact n + (1::nat)"
   13.31    have "1 < ?k" by simp
    14.1 --- a/src/HOL/ex/Sqrt.thy	Wed Jul 20 14:52:09 2016 +0200
    14.2 +++ b/src/HOL/ex/Sqrt.thy	Thu Jul 21 10:06:04 2016 +0200
    14.3 @@ -14,7 +14,7 @@
    14.4    assumes "prime (p::nat)"
    14.5    shows "sqrt p \<notin> \<rat>"
    14.6  proof
    14.7 -  from \<open>prime p\<close> have p: "1 < p" by (simp add: prime_def)
    14.8 +  from \<open>prime p\<close> have p: "1 < p" by (simp add: is_prime_nat_iff)
    14.9    assume "sqrt p \<in> \<rat>"
   14.10    then obtain m n :: nat where
   14.11        n: "n \<noteq> 0" and sqrt_rat: "\<bar>sqrt p\<bar> = m / n"
   14.12 @@ -59,7 +59,7 @@
   14.13    assumes "prime (p::nat)"
   14.14    shows "sqrt p \<notin> \<rat>"
   14.15  proof
   14.16 -  from \<open>prime p\<close> have p: "1 < p" by (simp add: prime_def)
   14.17 +  from \<open>prime p\<close> have p: "1 < p" by (simp add: is_prime_nat_iff)
   14.18    assume "sqrt p \<in> \<rat>"
   14.19    then obtain m n :: nat where
   14.20        n: "n \<noteq> 0" and sqrt_rat: "\<bar>sqrt p\<bar> = m / n"
    15.1 --- a/src/HOL/ex/Sqrt_Script.thy	Wed Jul 20 14:52:09 2016 +0200
    15.2 +++ b/src/HOL/ex/Sqrt_Script.thy	Thu Jul 21 10:06:04 2016 +0200
    15.3 @@ -17,7 +17,7 @@
    15.4  subsection \<open>Preliminaries\<close>
    15.5  
    15.6  lemma prime_nonzero:  "prime (p::nat) \<Longrightarrow> p \<noteq> 0"
    15.7 -  by (force simp add: prime_def)
    15.8 +  by (force simp add: is_prime_nat_iff)
    15.9  
   15.10  lemma prime_dvd_other_side:
   15.11      "(n::nat) * n = p * (k * k) \<Longrightarrow> prime p \<Longrightarrow> p dvd n"
   15.12 @@ -32,7 +32,7 @@
   15.13    apply (erule disjE)
   15.14     apply (frule mult_le_mono, assumption)
   15.15     apply auto
   15.16 -  apply (force simp add: prime_def)
   15.17 +  apply (force simp add: is_prime_nat_iff)
   15.18    done
   15.19  
   15.20  lemma rearrange: "(j::nat) * (p * j) = k * k \<Longrightarrow> k * k = p * (j * j)"