--- 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
--- 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)
--- 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
--- 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
--- 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>
--- 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
--- 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
--- 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