# HG changeset patch
# User eberlm <eberlm@in.tum.de>
# Date 1469201754 -7200
# Node ID 831816778409a26b256aaab2abdd947efda85049
# Parent  8cecf0100996dfa70fcef931ced55a702b633a93
Removed redundant material related to primes

diff -r 8cecf0100996 -r 831816778409 src/HOL/Algebra/Exponent.thy
--- a/src/HOL/Algebra/Exponent.thy	Fri Jul 22 15:39:32 2016 +0200
+++ b/src/HOL/Algebra/Exponent.thy	Fri Jul 22 17:35:54 2016 +0200
@@ -13,183 +13,16 @@
 
 text \<open>The Combinatorial Argument Underlying the First Sylow Theorem\<close>
 
-
-subsection\<open>Prime Theorems\<close>
-
-lemma prime_dvd_cases:
-  assumes pk: "p*k dvd m*n" and p: "prime p"
-  shows "(\<exists>x. k dvd x*n \<and> m = p*x) \<or> (\<exists>y. k dvd m*y \<and> n = p*y)"
-proof -
-  have "p dvd m*n" using dvd_mult_left pk by blast
-  then consider "p dvd m" | "p dvd n"
-    using p is_prime_dvd_mult_iff by blast
-  then show ?thesis
-  proof cases
-    case 1 then obtain a where "m = p * a" by (metis dvd_mult_div_cancel) 
-      then have "\<exists>x. k dvd x * n \<and> m = p * x"
-        using p pk by (auto simp: mult.assoc)
-    then show ?thesis ..
-  next
-    case 2 then obtain b where "n = p * b" by (metis dvd_mult_div_cancel) 
-    with p pk have "\<exists>y. k dvd m*y \<and> n = p*y" 
-      by (metis dvd_mult_right dvd_times_left_cancel_iff mult.left_commute mult_zero_left)
-    then show ?thesis ..
-  qed
-qed
-
-lemma prime_power_dvd_prod:
-  assumes pc: "p^c dvd m*n" and p: "prime p"
-  shows "\<exists>a b. a+b = c \<and> p^a dvd m \<and> p^b dvd n"
-using pc
-proof (induct c arbitrary: m n)
-  case 0 show ?case by simp
-next
-  case (Suc c)
-  consider x where "p^c dvd x*n" "m = p*x" | y where "p^c dvd m*y" "n = p*y"
-    using prime_dvd_cases [of _ "p^c", OF _ p] Suc.prems by force
-  then show ?case
-  proof cases
-    case (1 x) 
-    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
-    with 1 have "Suc a + b = Suc c \<and> p ^ Suc a dvd m \<and> p ^ b dvd n"
-      by (auto intro: mult_dvd_mono)
-    thus ?thesis by blast
-  next
-    case (2 y) 
-    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
-    with 2 have "a + Suc b = Suc c \<and> p ^ a dvd m \<and> p ^ Suc b dvd n"
-      by (auto intro: mult_dvd_mono)
-    with Suc.hyps [of m y] show "\<exists>a b. a + b = Suc c \<and> p ^ a dvd m \<and> p ^ b dvd n"
-      by force
-  qed
-qed
-
-lemma add_eq_Suc_lem: "a+b = Suc (x+y) \<Longrightarrow> a \<le> x \<or> b \<le> y"
-  by arith
-
-lemma prime_power_dvd_cases:
-     "\<lbrakk>p^c dvd m * n; a + b = Suc c; prime p\<rbrakk> \<Longrightarrow> p ^ a dvd m \<or> p ^ b dvd n"
-  using power_le_dvd prime_power_dvd_prod by (blast dest: prime_power_dvd_prod add_eq_Suc_lem)
-
 text\<open>needed in this form to prove Sylow's theorem\<close>
-corollary div_combine: "\<lbrakk>prime p; \<not> p ^ Suc r dvd n; p ^ (a + r) dvd n * k\<rbrakk> \<Longrightarrow> p ^ a dvd k"
+corollary (in algebraic_semidom) div_combine: 
+  "\<lbrakk>is_prime_elem p; \<not> p ^ Suc r dvd n; p ^ (a + r) dvd n * k\<rbrakk> \<Longrightarrow> p ^ a dvd k"
   by (metis add_Suc_right mult.commute prime_power_dvd_cases)
 
-
-subsection\<open>The Exponent Function\<close>
-
-abbreviation (input) "exponent \<equiv> multiplicity"
-
-(*
-definition
-  exponent :: "nat => nat => nat"
-  where "exponent p s = (if prime p then (GREATEST r. p^r dvd s) else 0)"
-*)
-
-(*lemma exponent_eq_0 [simp]: "\<not> prime p \<Longrightarrow> exponent p s = 0"
-  by (simp add: exponent_def)*)
-
-lemma Suc_le_power: "Suc 0 < p \<Longrightarrow> Suc n \<le> p ^ n"
-  by (induct n) (auto simp: Suc_le_eq le_less_trans)
-
-(*
-text\<open>An upper bound for the @{term n} such that @{term"p^n dvd a"}: needed for GREATEST to exist\<close>
-lemma power_dvd_bound: "\<lbrakk>p ^ n dvd a; Suc 0 < p; 0 < a\<rbrakk> \<Longrightarrow> n < a"
-  by (meson Suc_le_lessD Suc_le_power dvd_imp_le le_trans)
-*)
-
-(*
-lemma exponent_ge:
-  assumes "p ^ k dvd n" "prime p" "0 < n"
-    shows "k \<le> exponent p n"
-proof -
-  have "Suc 0 < p"
-    using \<open>prime p\<close> by (simp add: prime_def)
-  with assms show ?thesis
-    by (simp add: \<open>prime p\<close> exponent_def) (meson Greatest_le power_dvd_bound)
-qed
-*)
-
-(*
-lemma power_exponent_dvd: "p ^ exponent p s dvd s"
-proof (cases "s = 0")
-  case True then show ?thesis by simp
-next
-  case False then show ?thesis 
-    apply (simp add: exponent_def, clarify)
-    apply (rule GreatestI [where k = 0])
-    apply (auto dest: prime_gt_Suc_0_nat power_dvd_bound)
-    done
-qed
-*)
-
-(*lemma power_Suc_exponent_Not_dvd:
-    "\<lbrakk>p * p ^ exponent p s dvd s; prime p\<rbrakk> \<Longrightarrow> s = 0"
-  by (metis exponent_ge neq0_conv not_less_eq_eq order_refl power_Suc)
-*)
-
-
-(*
-lemma exponent_power_eq [simp]: "prime p \<Longrightarrow> exponent p (p ^ a) = a"
-  apply (simp add: exponent_def)
-  apply (rule Greatest_equality, simp)
-  apply (simp add: prime_gt_Suc_0_nat power_dvd_imp_le)
-  done
-*)
-
-(*
-lemma exponent_1_eq_0 [simp]: "exponent p (Suc 0) = 0"
-  apply (case_tac "prime p")
-  apply (metis exponent_power_eq nat_power_eq_Suc_0_iff)
-  apply simp
-  done
-*)
-
-lemma exponent_equalityI:
-  "(\<And>r. p ^ r dvd a \<longleftrightarrow> p ^ r dvd b) \<Longrightarrow> exponent p a = exponent p b"
-  by (simp add: multiplicity_def)
-
-(*
-lemma exponent_mult_add: 
-  assumes "a > 0" "b > 0"
-    shows "exponent p (a * b) = (exponent p a) + (exponent p b)"
-proof (cases "prime p")
-  case False then show ?thesis by simp
-next
-  case True show ?thesis
-  proof (rule order_antisym)
-    show "exponent p a + exponent p b \<le> exponent p (a * b)"
-      by (rule exponent_ge) (auto simp: mult_dvd_mono power_add power_exponent_dvd \<open>prime p\<close> assms)
-  next
-    { assume "exponent p a + exponent p b < exponent p (a * b)"
-      then have "p ^ (Suc (exponent p a + exponent p b)) dvd a * b"
-        by (meson Suc_le_eq power_exponent_dvd power_le_dvd)
-      with prime_power_dvd_cases [where  a = "Suc (exponent p a)" and b = "Suc (exponent p b)"] 
-      have False 
-        by (metis Suc_n_not_le_n True add_Suc add_Suc_right assms exponent_ge)
-    } 
-  then show "exponent p (a * b) \<le> exponent p a + exponent p b" by (blast intro: leI)
-  qed
-qed
-*)
-
-lemma not_dvd_imp_multiplicity_0: 
-  assumes "\<not>p dvd x"
-  shows   "multiplicity p x = 0"
-proof -
-  from assms have "multiplicity p x < 1"
-    by (intro multiplicity_lessI) auto
-  thus ?thesis by simp
-qed
-
-
-subsection\<open>The Main Combinatorial Argument\<close>
-
 lemma exponent_p_a_m_k_equation: 
   fixes p :: nat
   assumes "0 < m" "0 < k" "p \<noteq> 0" "k < p^a" 
-    shows "exponent p (p^a * m - k) = exponent p (p^a - k)"
-proof (rule exponent_equalityI [OF iffI])
+    shows "multiplicity p (p^a * m - k) = multiplicity p (p^a - k)"
+proof (rule multiplicity_cong [OF iffI])
   fix r
   assume *: "p ^ r dvd p ^ a * m - k" 
   show "p ^ r dvd p ^ a - k"
@@ -218,16 +51,16 @@
 
 lemma p_not_div_choose_lemma: 
   fixes p :: nat
-  assumes eeq: "\<And>i. Suc i < K \<Longrightarrow> exponent p (Suc i) = exponent p (Suc (j + i))"
+  assumes eeq: "\<And>i. Suc i < K \<Longrightarrow> multiplicity p (Suc i) = multiplicity p (Suc (j + i))"
       and "k < K" and p: "prime p"
-    shows "exponent p (j + k choose k) = 0"
+    shows "multiplicity p (j + k choose k) = 0"
   using \<open>k < K\<close>
 proof (induction k)
   case 0 then show ?case by simp
 next
   case (Suc k)
   then have *: "(Suc (j+k) choose Suc k) > 0" by simp
-  then have "exponent p ((Suc (j+k) choose Suc k) * Suc k) = exponent p (Suc k)"
+  then have "multiplicity p ((Suc (j+k) choose Suc k) * Suc k) = multiplicity p (Suc k)"
     by (subst Suc_times_binomial_eq [symmetric], subst prime_multiplicity_mult_distrib)
        (insert p Suc.prems, simp_all add: eeq [symmetric] Suc.IH)
   with p * show ?case
@@ -237,8 +70,8 @@
 text\<open>The lemma above, with two changes of variables\<close>
 lemma p_not_div_choose:
   assumes "k < K" and "k \<le> n" 
-      and eeq: "\<And>j. \<lbrakk>0<j; j<K\<rbrakk> \<Longrightarrow> exponent p (n - k + (K - j)) = exponent p (K - j)" "is_prime p"
-    shows "exponent p (n choose k) = 0"
+      and eeq: "\<And>j. \<lbrakk>0<j; j<K\<rbrakk> \<Longrightarrow> multiplicity p (n - k + (K - j)) = multiplicity p (K - j)" "is_prime p"
+    shows "multiplicity p (n choose k) = 0"
 apply (rule p_not_div_choose_lemma [of K p "n-k" k, simplified assms nat_minus_add_max max_absorb1])
 apply (metis add_Suc_right eeq diff_diff_cancel order_less_imp_le zero_less_Suc zero_less_diff)
 apply (rule TrueI)+
@@ -246,14 +79,14 @@
 
 proposition const_p_fac:
   assumes "m>0" and prime: "is_prime p"
-  shows "exponent p (p^a * m choose p^a) = exponent p m"
+  shows "multiplicity p (p^a * m choose p^a) = multiplicity p m"
 proof-
   from assms have p: "0 < p ^ a" "0 < p^a * m" "p^a \<le> p^a * m"
     by (auto simp: prime_gt_0_nat) 
-  have *: "exponent p ((p^a * m - 1) choose (p^a - 1)) = 0"
+  have *: "multiplicity p ((p^a * m - 1) choose (p^a - 1)) = 0"
     apply (rule p_not_div_choose [where K = "p^a"])
     using p exponent_p_a_m_k_equation by (auto simp: diff_le_mono prime)
-  have "exponent p ((p ^ a * m choose p ^ a) * p ^ a) = a + exponent p m"
+  have "multiplicity p ((p ^ a * m choose p ^ a) * p ^ a) = a + multiplicity p m"
   proof -
     have "(p ^ a * m choose p ^ a) * p ^ a = p ^ a * m * (p ^ a * m - 1 choose (p ^ a - 1))" 
       (is "_ = ?rhs") using prime 
diff -r 8cecf0100996 -r 831816778409 src/HOL/Algebra/Sylow.thy
--- a/src/HOL/Algebra/Sylow.thy	Fri Jul 22 15:39:32 2016 +0200
+++ b/src/HOL/Algebra/Sylow.thy	Fri Jul 22 17:35:54 2016 +0200
@@ -60,7 +60,7 @@
 locale sylow_central = sylow +
   fixes H and M1 and M
   assumes M_in_quot:  "M \<in> calM // RelM"
-      and not_dvd_M:  "~(p ^ Suc(exponent p m) dvd card(M))"
+      and not_dvd_M:  "~(p ^ Suc(multiplicity p m) dvd card(M))"
       and M1_in_M:    "M1 \<in> M"
   defines "H == {g. g\<in>carrier G & M1 #> g = M1}"
 
@@ -128,7 +128,7 @@
 by (simp add: card_calM zero_less_binomial le_extend_mult zero_less_m)
 
 lemma max_p_div_calM:
-     "~ (p ^ Suc(exponent p m) dvd card(calM))"
+     "~ (p ^ Suc(multiplicity p m) dvd card(calM))"
 proof
   assume "p ^ Suc (multiplicity p m) dvd card calM"
   with zero_less_card_calM prime_p 
@@ -145,7 +145,7 @@
   by (rule_tac B = "Pow (carrier G) " in finite_subset) auto
 
 lemma lemma_A1:
-     "\<exists>M \<in> calM // RelM. ~ (p ^ Suc(exponent p m) dvd card(M))"
+     "\<exists>M \<in> calM // RelM. ~ (p ^ Suc(multiplicity p m) dvd card(M))"
   using RelM_equiv equiv_imp_dvd_card finite_calM max_p_div_calM by blast
 
 end
@@ -307,7 +307,7 @@
 
 lemma (in sylow_central) lemma_leq1: "p^a \<le> card(H)"
 apply (rule dvd_imp_le)
- apply (rule div_combine [OF prime_p not_dvd_M])
+ apply (rule div_combine [OF prime_imp_prime_elem[OF prime_p] not_dvd_M])
  prefer 2 apply (blast intro: subgroup.finite_imp_card_positive H_is_subgroup)
 apply (simp add: index_lem order_G power_add mult_dvd_mono multiplicity_dvd
                  zero_less_m)
diff -r 8cecf0100996 -r 831816778409 src/HOL/Nonstandard_Analysis/Examples/NSPrimes.thy
--- a/src/HOL/Nonstandard_Analysis/Examples/NSPrimes.thy	Fri Jul 22 15:39:32 2016 +0200
+++ b/src/HOL/Nonstandard_Analysis/Examples/NSPrimes.thy	Fri Jul 22 17:35:54 2016 +0200
@@ -7,7 +7,7 @@
 section\<open>The Nonstandard Primes as an Extension of the Prime Numbers\<close>
 
 theory NSPrimes
-imports "~~/src/HOL/Number_Theory/UniqueFactorization" "../Hyperreal"
+imports "~~/src/HOL/Number_Theory/Primes" "../Hyperreal"
 begin
 
 text\<open>These can be used to derive an alternative proof of the infinitude of
diff -r 8cecf0100996 -r 831816778409 src/HOL/Number_Theory/Factorial_Ring.thy
--- a/src/HOL/Number_Theory/Factorial_Ring.thy	Fri Jul 22 15:39:32 2016 +0200
+++ b/src/HOL/Number_Theory/Factorial_Ring.thy	Fri Jul 22 17:35:54 2016 +0200
@@ -233,6 +233,61 @@
   "is_unit a \<Longrightarrow> is_prime_elem (a * p) \<longleftrightarrow> is_prime_elem p"
   by (auto simp: is_prime_elem_def mult.commute[of a] is_unit_mult_iff mult_unit_dvd_iff)
 
+lemma prime_dvd_cases:
+  assumes pk: "p*k dvd m*n" and p: "is_prime_elem p"
+  shows "(\<exists>x. k dvd x*n \<and> m = p*x) \<or> (\<exists>y. k dvd m*y \<and> n = p*y)"
+proof -
+  have "p dvd m*n" using dvd_mult_left pk by blast
+  then consider "p dvd m" | "p dvd n"
+    using p prime_dvd_mult_iff by blast
+  then show ?thesis
+  proof cases
+    case 1 then obtain a where "m = p * a" by (metis dvd_mult_div_cancel) 
+      then have "\<exists>x. k dvd x * n \<and> m = p * x"
+        using p pk by (auto simp: mult.assoc)
+    then show ?thesis ..
+  next
+    case 2 then obtain b where "n = p * b" by (metis dvd_mult_div_cancel) 
+    with p pk have "\<exists>y. k dvd m*y \<and> n = p*y" 
+      by (metis dvd_mult_right dvd_times_left_cancel_iff mult.left_commute mult_zero_left)
+    then show ?thesis ..
+  qed
+qed
+
+lemma prime_power_dvd_prod:
+  assumes pc: "p^c dvd m*n" and p: "is_prime_elem p"
+  shows "\<exists>a b. a+b = c \<and> p^a dvd m \<and> p^b dvd n"
+using pc
+proof (induct c arbitrary: m n)
+  case 0 show ?case by simp
+next
+  case (Suc c)
+  consider x where "p^c dvd x*n" "m = p*x" | y where "p^c dvd m*y" "n = p*y"
+    using prime_dvd_cases [of _ "p^c", OF _ p] Suc.prems by force
+  then show ?case
+  proof cases
+    case (1 x) 
+    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
+    with 1 have "Suc a + b = Suc c \<and> p ^ Suc a dvd m \<and> p ^ b dvd n"
+      by (auto intro: mult_dvd_mono)
+    thus ?thesis by blast
+  next
+    case (2 y) 
+    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
+    with 2 have "a + Suc b = Suc c \<and> p ^ a dvd m \<and> p ^ Suc b dvd n"
+      by (auto intro: mult_dvd_mono)
+    with Suc.hyps [of m y] show "\<exists>a b. a + b = Suc c \<and> p ^ a dvd m \<and> p ^ b dvd n"
+      by force
+  qed
+qed
+
+lemma add_eq_Suc_lem: "a+b = Suc (x+y) \<Longrightarrow> a \<le> x \<or> b \<le> y"
+  by arith
+
+lemma prime_power_dvd_cases:
+     "\<lbrakk>p^c dvd m * n; a + b = Suc c; is_prime_elem p\<rbrakk> \<Longrightarrow> p ^ a dvd m \<or> p ^ b dvd n"
+  using power_le_dvd prime_power_dvd_prod by (blast dest: prime_power_dvd_prod add_eq_Suc_lem)
+
 end
 
 context normalization_semidom
@@ -1384,6 +1439,19 @@
   finally show ?thesis .
 qed
 
+lemma multiplicity_cong:
+  "(\<And>r. p ^ r dvd a \<longleftrightarrow> p ^ r dvd b) \<Longrightarrow> multiplicity p a = multiplicity p b"
+  by (simp add: multiplicity_def)
+
+lemma not_dvd_imp_multiplicity_0: 
+  assumes "\<not>p dvd x"
+  shows   "multiplicity p x = 0"
+proof -
+  from assms have "multiplicity p x < 1"
+    by (intro multiplicity_lessI) auto
+  thus ?thesis by simp
+qed
+
 
 definition "gcd_factorial a b = (if a = 0 then normalize b
      else if b = 0 then normalize a
diff -r 8cecf0100996 -r 831816778409 src/HOL/Number_Theory/Residues.thy
--- a/src/HOL/Number_Theory/Residues.thy	Fri Jul 22 15:39:32 2016 +0200
+++ b/src/HOL/Number_Theory/Residues.thy	Fri Jul 22 17:35:54 2016 +0200
@@ -8,7 +8,7 @@
 section \<open>Residue rings\<close>
 
 theory Residues
-imports UniqueFactorization MiscAlgebra
+imports Cong MiscAlgebra
 begin
 
 subsection \<open>A locale for residue rings\<close>
diff -r 8cecf0100996 -r 831816778409 src/HOL/Number_Theory/UniqueFactorization.thy
--- a/src/HOL/Number_Theory/UniqueFactorization.thy	Fri Jul 22 15:39:32 2016 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,15 +0,0 @@
-(*  Title:      HOL/Number_Theory/UniqueFactorization.thy
-    Author:     Jeremy Avigad
-
-Note: there were previous Isabelle formalizations of unique
-factorization due to Thomas Marthedal Rasmussen, and, building on
-that, by Jeremy Avigad and David Gray.
-*)
-
-section \<open>Unique factorization for the natural numbers and the integers\<close>
-
-theory UniqueFactorization
-imports Cong "~~/src/HOL/Library/Multiset"
-begin
-
-end
diff -r 8cecf0100996 -r 831816778409 src/HOL/Proofs/Extraction/Euclid.thy
--- a/src/HOL/Proofs/Extraction/Euclid.thy	Fri Jul 22 15:39:32 2016 +0200
+++ b/src/HOL/Proofs/Extraction/Euclid.thy	Fri Jul 22 17:35:54 2016 +0200
@@ -8,7 +8,7 @@
 
 theory Euclid
 imports
-  "~~/src/HOL/Number_Theory/UniqueFactorization"
+  "~~/src/HOL/Number_Theory/Primes"
   Util
   "~~/src/HOL/Library/Code_Target_Numeral"
 begin
diff -r 8cecf0100996 -r 831816778409 src/HOL/ROOT
--- a/src/HOL/ROOT	Fri Jul 22 15:39:32 2016 +0200
+++ b/src/HOL/ROOT	Fri Jul 22 17:35:54 2016 +0200
@@ -416,7 +416,6 @@
     "~~/src/HOL/Library/Code_Target_Numeral"
     "~~/src/HOL/Library/Monad_Syntax"
     "~~/src/HOL/Number_Theory/Primes"
-    "~~/src/HOL/Number_Theory/UniqueFactorization"
     "~~/src/HOL/Library/State_Monad"
   theories
     Greatest_Common_Divisor