--- a/src/HOL/Algebra/Exponent.thy Wed Jul 20 14:52:09 2016 +0200
+++ b/src/HOL/Algebra/Exponent.thy Thu Jul 21 10:06:04 2016 +0200
@@ -22,17 +22,17 @@
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_eq_nat by blast
+ 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
+ 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)
- then have "\<exists>y. k dvd m*y \<and> n = p*y"
- using p pk by auto
+ 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
@@ -50,11 +50,16 @@
then show ?case
proof cases
case (1 x)
- with Suc.hyps [of x n] show "\<exists>a b. a + b = Suc c \<and> p ^ a dvd m \<and> p ^ b dvd n"
- by force
+ 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] show "\<exists>a b. a + b = Suc c \<and> p ^ a dvd m \<and> p ^ b dvd n"
+ 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
@@ -73,20 +78,27 @@
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 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"
@@ -96,7 +108,9 @@
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
@@ -107,27 +121,35 @@
apply (auto dest: prime_gt_Suc_0_nat power_dvd_bound)
done
qed
+*)
-lemma power_Suc_exponent_Not_dvd:
+(*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: exponent_def)
+ 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)"
@@ -149,15 +171,22 @@
then show "exponent p (a * b) \<le> exponent p a + exponent p b" by (blast intro: leI)
qed
qed
+*)
-lemma not_divides_exponent_0: "~ (p dvd n) \<Longrightarrow> exponent p n = 0"
- apply (case_tac "exponent p n", simp)
- by (metis dvd_mult_left power_Suc power_exponent_dvd)
+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])
@@ -188,60 +217,56 @@
qed
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))"
- and "k < K"
+ and "k < K" and p: "prime p"
shows "exponent p (j + k choose k) = 0"
-proof (cases "prime p")
- case False then show ?thesis by simp
+ using \<open>k < K\<close>
+proof (induction k)
+ case 0 then show ?case by simp
next
- case True show ?thesis 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)"
- by (metis Suc.IH Suc.prems Suc_lessD Suc_times_binomial_eq add.comm_neutral eeq exponent_mult_add
- mult_pos_pos zero_less_Suc zero_less_mult_pos)
- then show ?case
- by (metis * add.commute add_Suc_right add_eq_self_zero exponent_mult_add zero_less_Suc)
- qed
+ 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)"
+ 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
+ by (subst (asm) prime_multiplicity_mult_distrib) simp_all
qed
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)"
+ 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"
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)
+apply (rule TrueI)+
done
proposition const_p_fac:
- assumes "m>0"
- shows "exponent p (p^a * m choose p^a) = exponent p m"
-proof (cases "prime p")
- case False then show ?thesis by auto
-next
- case True
- with assms have p: "0 < p ^ a" "0 < p^a * m" "p^a \<le> p^a * m"
+ assumes "m>0" and prime: "is_prime p"
+ shows "exponent p (p^a * m choose p^a) = exponent 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"
apply (rule p_not_div_choose [where K = "p^a"])
- using p exponent_p_a_m_k_equation by (auto simp: diff_le_mono)
+ 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"
proof -
- have "p ^ a * m * (p ^ a * m - 1 choose (p ^ a - 1)) = p ^ a * (p ^ a * m choose p ^ a)"
- using p One_nat_def times_binomial_minus1_eq by presburger
- moreover have "exponent p (p ^ a) = a"
- by (meson True exponent_power_eq)
- ultimately show ?thesis
- using * p
- 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)
+ have "(p ^ a * m choose p ^ a) * p ^ a = p ^ a * m * (p ^ a * m - 1 choose (p ^ a - 1))"
+ (is "_ = ?rhs") using prime
+ by (subst times_binomial_minus1_eq [symmetric]) (auto simp: prime_gt_0_nat)
+ also from p have "p ^ a - Suc 0 \<le> p ^ a * m - Suc 0" by linarith
+ with prime * p have "multiplicity p ?rhs = multiplicity p (p ^ a * m)"
+ by (subst prime_multiplicity_mult_distrib) auto
+ also have "\<dots> = a + multiplicity p m"
+ using prime p by (subst prime_multiplicity_mult_distrib) simp_all
+ finally show ?thesis .
qed
then show ?thesis
- using True p exponent_mult_add by auto
+ using prime p by (subst (asm) prime_multiplicity_mult_distrib) simp_all
qed
end
--- a/src/HOL/Algebra/IntRing.thy Wed Jul 20 14:52:09 2016 +0200
+++ b/src/HOL/Algebra/IntRing.thy Thu Jul 21 10:06:04 2016 +0200
@@ -4,7 +4,7 @@
*)
theory IntRing
-imports QuotRing Lattice Int "~~/src/HOL/Number_Theory/Primes"
+imports "~~/src/HOL/Number_Theory/Primes" QuotRing Lattice Int
begin
section \<open>The Ring of Integers\<close>
@@ -240,18 +240,18 @@
apply (elim exE)
proof -
fix a b x
- assume "a * b = x * int p"
+ assume "a * b = x * p"
then have "p dvd a * b" by simp
then have "p dvd a \<or> p dvd b"
by (metis prime prime_dvd_mult_eq_int)
- then show "(\<exists>x. a = x * int p) \<or> (\<exists>x. b = x * int p)"
+ then show "(\<exists>x. a = x * p) \<or> (\<exists>x. b = x * p)"
by (metis dvd_def mult.commute)
next
- assume "UNIV = {uu. EX x. uu = x * int p}"
- then obtain x where "1 = x * int p" by best
- then have "\<bar>int p * x\<bar> = 1" by (simp add: mult.commute)
- then show False
- by (metis abs_of_nat of_nat_1 of_nat_eq_iff abs_zmult_eq_1 one_not_prime_nat prime)
+ assume "UNIV = {uu. EX x. uu = x * p}"
+ then obtain x where "1 = x * p" by best
+ then have "\<bar>p * x\<bar> = 1" by (simp add: mult.commute)
+ then show False using prime
+ by (auto dest!: abs_zmult_eq_1 simp: is_prime_def)
qed
--- a/src/HOL/Algebra/Sylow.thy Wed Jul 20 14:52:09 2016 +0200
+++ b/src/HOL/Algebra/Sylow.thy Thu Jul 21 10:06:04 2016 +0200
@@ -129,11 +129,15 @@
lemma max_p_div_calM:
"~ (p ^ Suc(exponent p m) dvd card(calM))"
-proof -
- have "exponent p m = exponent p (card calM)"
- by (simp add: card_calM const_p_fac zero_less_m)
- then show ?thesis
- by (metis Suc_n_not_le_n exponent_ge prime_p zero_less_card_calM)
+proof
+ assume "p ^ Suc (multiplicity p m) dvd card calM"
+ with zero_less_card_calM prime_p
+ have "Suc (multiplicity p m) \<le> multiplicity p (card calM)"
+ by (intro multiplicity_geI) auto
+ hence "multiplicity p m < multiplicity p (card calM)" by simp
+ also have "multiplicity p m = multiplicity p (card calM)"
+ by (simp add: const_p_fac prime_p zero_less_m card_calM)
+ finally show False by simp
qed
lemma finite_calM: "finite calM"
@@ -305,7 +309,7 @@
apply (rule dvd_imp_le)
apply (rule div_combine [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 power_exponent_dvd
+apply (simp add: index_lem order_G power_add mult_dvd_mono multiplicity_dvd
zero_less_m)
done
--- a/src/HOL/Library/Multiset.thy Wed Jul 20 14:52:09 2016 +0200
+++ b/src/HOL/Library/Multiset.thy Thu Jul 21 10:06:04 2016 +0200
@@ -1005,7 +1005,14 @@
have "subset_mset.bdd_above A"
by (rule ccontr) (insert assms, simp_all add: Sup_multiset_unbounded)
with assms show ?thesis by (simp add: in_Sup_multiset_iff)
-qed
+qed
+
+interpretation subset_mset: distrib_lattice "op #\<inter>" "op \<subseteq>#" "op \<subset>#" "op #\<union>"
+proof
+ fix A B C :: "'a multiset"
+ show "A #\<union> (B #\<inter> C) = A #\<union> B #\<inter> (A #\<union> C)"
+ by (intro multiset_eqI) simp_all
+qed
subsubsection \<open>Filter (with comprehension syntax)\<close>
@@ -1835,6 +1842,12 @@
"setsum f A = msetsum (image_mset f (mset_set A))"
by (cases "finite A") (induct A rule: finite_induct, simp_all)
+lemma msetsum_delta: "msetsum (image_mset (\<lambda>x. if x = y then c else 0) A) = c * count A y"
+ by (induction A) simp_all
+
+lemma msetsum_delta': "msetsum (image_mset (\<lambda>x. if y = x then c else 0) A) = c * count A y"
+ by (induction A) simp_all
+
end
lemma msetsum_diff:
@@ -1910,6 +1923,12 @@
"msetprod M = setprod (\<lambda>x. x ^ count M x) (set_mset M)"
by (simp add: fold_mset_def setprod.eq_fold msetprod.eq_fold funpow_times_power comp_def)
+lemma msetprod_delta: "msetprod (image_mset (\<lambda>x. if x = y then c else 1) A) = c ^ count A y"
+ by (induction A) (simp_all add: mult_ac)
+
+lemma msetprod_delta': "msetprod (image_mset (\<lambda>x. if y = x then c else 1) A) = c ^ count A y"
+ by (induction A) (simp_all add: mult_ac)
+
end
syntax (ASCII)
--- a/src/HOL/Nonstandard_Analysis/Examples/NSPrimes.thy Wed Jul 20 14:52:09 2016 +0200
+++ b/src/HOL/Nonstandard_Analysis/Examples/NSPrimes.thy Thu Jul 21 10:06:04 2016 +0200
@@ -67,7 +67,7 @@
(* Goldblatt: Exercise 5.11(3a) - p 57 *)
lemma starprime:
"starprime = {p. 1 < p & (\<forall>m. m dvd p --> m = 1 | m = p)}"
-by (transfer, auto simp add: prime_def)
+by (transfer, auto simp add: is_prime_nat_iff)
(* Goldblatt Exercise 5.11(3b) - p 57 *)
lemma hyperprime_factor_exists [rule_format]:
@@ -276,7 +276,8 @@
apply clarify
apply (subgoal_tac "k \<notin> hypnat_of_nat ` {p. prime p}")
apply (force simp add: starprime_def)
-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)
+ 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 not_is_prime_0)
done
end
--- a/src/HOL/Number_Theory/Eratosthenes.thy Wed Jul 20 14:52:09 2016 +0200
+++ b/src/HOL/Number_Theory/Eratosthenes.thy Thu Jul 21 10:06:04 2016 +0200
@@ -295,8 +295,8 @@
from 2 show ?thesis
apply (auto simp add: numbers_of_marks_sieve numeral_2_eq_2 set_primes_upto
dest: prime_gt_Suc_0_nat)
- apply (metis One_nat_def Suc_le_eq less_not_refl prime_def)
- apply (metis One_nat_def Suc_le_eq aux prime_def)
+ apply (metis One_nat_def Suc_le_eq less_not_refl is_prime_nat_iff)
+ apply (metis One_nat_def Suc_le_eq aux is_prime_nat_iff)
done
qed
qed
--- a/src/HOL/Number_Theory/Factorial_Ring.thy Wed Jul 20 14:52:09 2016 +0200
+++ b/src/HOL/Number_Theory/Factorial_Ring.thy Thu Jul 21 10:06:04 2016 +0200
@@ -7,8 +7,8 @@
theory Factorial_Ring
imports
- Main
- "~~/src/HOL/Number_Theory/Primes"
+ Main
+ "../GCD"
"~~/src/HOL/Library/Multiset"
begin
@@ -84,6 +84,15 @@
shows "p \<noteq> 0"
using assms by (auto intro: ccontr)
+
+lemma is_prime_elem_dvd_power:
+ "is_prime_elem p \<Longrightarrow> p dvd x ^ n \<Longrightarrow> p dvd x"
+ by (induction n) (auto dest: prime_divides_productD intro: dvd_trans[of _ 1])
+
+lemma is_prime_elem_dvd_power_iff:
+ "is_prime_elem p \<Longrightarrow> n > 0 \<Longrightarrow> p dvd x ^ n \<longleftrightarrow> p dvd x"
+ by (auto dest: is_prime_elem_dvd_power intro: dvd_trans)
+
lemma is_prime_elem_imp_nonzero [simp]:
"ASSUMPTION (is_prime_elem x) \<Longrightarrow> x \<noteq> 0"
unfolding ASSUMPTION_def by (rule is_prime_elem_not_zeroI)
@@ -94,12 +103,13 @@
end
-lemma (in algebraic_semidom) mult_unit_dvd_iff': "is_unit a \<Longrightarrow> (a * b) dvd c \<longleftrightarrow> b dvd c"
- by (subst mult.commute) (rule mult_unit_dvd_iff)
-
context algebraic_semidom
begin
+(* TODO Move *)
+lemma mult_unit_dvd_iff': "is_unit a \<Longrightarrow> (a * b) dvd c \<longleftrightarrow> b dvd c"
+ by (subst mult.commute) (rule mult_unit_dvd_iff)
+
lemma prime_imp_irreducible:
assumes "is_prime_elem p"
shows "irreducible p"
@@ -191,6 +201,29 @@
by (auto simp add: mult_unit_dvd_iff)
qed
+context
+begin
+
+private lemma is_prime_elem_powerD:
+ assumes "is_prime_elem (p ^ n)"
+ shows "is_prime_elem p \<and> n = 1"
+proof (cases n)
+ case (Suc m)
+ note assms
+ also from Suc have "p ^ n = p * p^m" by simp
+ finally have "is_unit p \<or> is_unit (p^m)" by (rule is_prime_elem_multD)
+ moreover from assms have "\<not>is_unit p" by (simp add: is_prime_elem_def is_unit_power_iff)
+ ultimately have "is_unit (p ^ m)" by simp
+ with \<open>\<not>is_unit p\<close> have "m = 0" by (simp add: is_unit_power_iff)
+ with Suc assms show ?thesis by simp
+qed (insert assms, simp_all)
+
+lemma is_prime_elem_power_iff:
+ "is_prime_elem (p ^ n) \<longleftrightarrow> is_prime_elem p \<and> n = 1"
+ by (auto dest: is_prime_elem_powerD)
+
+end
+
lemma irreducible_mult_unit_left:
"is_unit a \<Longrightarrow> irreducible (a * p) \<longleftrightarrow> irreducible p"
by (auto simp: irreducible_altdef mult.commute[of a] is_unit_mult_iff
@@ -235,6 +268,10 @@
lemma is_prime_normalize_iff [simp]: "is_prime (normalize p) \<longleftrightarrow> is_prime_elem p"
by (auto simp add: is_prime_def)
+lemma is_prime_power_iff:
+ "is_prime (p ^ n) \<longleftrightarrow> is_prime p \<and> n = 1"
+ by (auto simp: is_prime_def is_prime_elem_power_iff)
+
lemma is_prime_elem_not_unit' [simp]:
"ASSUMPTION (is_prime_elem x) \<Longrightarrow> \<not>is_unit x"
unfolding ASSUMPTION_def by (rule is_prime_elem_not_unit)
@@ -273,6 +310,20 @@
by (blast intro: is_prime_elemD2)
qed
+lemma is_prime_dvd_multD: "is_prime p \<Longrightarrow> p dvd a * b \<Longrightarrow> p dvd a \<or> p dvd b"
+ by (intro prime_divides_productD) simp_all
+
+lemma is_prime_dvd_mult_iff [simp]: "is_prime p \<Longrightarrow> p dvd a * b \<longleftrightarrow> p dvd a \<or> p dvd b"
+ by (auto dest: is_prime_dvd_multD)
+
+lemma is_prime_dvd_power:
+ "is_prime p \<Longrightarrow> p dvd x ^ n \<Longrightarrow> p dvd x"
+ by (auto dest!: is_prime_elem_dvd_power simp: is_prime_def)
+
+lemma is_prime_dvd_power_iff:
+ "is_prime p \<Longrightarrow> n > 0 \<Longrightarrow> p dvd x ^ n \<longleftrightarrow> p dvd x"
+ by (intro is_prime_elem_dvd_power_iff) simp_all
+
lemma prime_dvd_msetprodE:
assumes "is_prime_elem p"
assumes dvd: "p dvd msetprod A"
@@ -499,6 +550,50 @@
by (auto simp: mult_unit_dvd_iff mult_unit_dvd_iff')
qed (insert assms, auto simp: irreducible_not_unit)
+lemma is_prime_elem_imp_coprime:
+ assumes "is_prime_elem p" "\<not>p dvd n"
+ shows "coprime p n"
+proof (rule coprimeI)
+ fix d assume "d dvd p" "d dvd n"
+ show "is_unit d"
+ proof (rule ccontr)
+ assume "\<not>is_unit d"
+ from \<open>is_prime_elem p\<close> and \<open>d dvd p\<close> and this have "p dvd d"
+ by (rule is_prime_elemD2)
+ from this and \<open>d dvd n\<close> have "p dvd n" by (rule dvd_trans)
+ with \<open>\<not>p dvd n\<close> show False by contradiction
+ qed
+qed
+
+lemma is_prime_imp_coprime:
+ assumes "is_prime p" "\<not>p dvd n"
+ shows "coprime p n"
+ using assms by (simp add: is_prime_elem_imp_coprime)
+
+lemma is_prime_elem_imp_power_coprime:
+ "is_prime_elem p \<Longrightarrow> \<not>p dvd a \<Longrightarrow> coprime a (p ^ m)"
+ by (auto intro!: coprime_exp dest: is_prime_elem_imp_coprime simp: gcd.commute)
+
+lemma is_prime_imp_power_coprime:
+ "is_prime p \<Longrightarrow> \<not>p dvd a \<Longrightarrow> coprime a (p ^ m)"
+ by (simp add: is_prime_elem_imp_power_coprime)
+
+lemma prime_divprod_pow:
+ assumes p: "is_prime_elem p" and ab: "coprime a b" and pab: "p^n dvd a * b"
+ shows "p^n dvd a \<or> p^n dvd b"
+ using assms
+proof -
+ from ab p have "\<not>p dvd a \<or> \<not>p dvd b"
+ by (auto simp: coprime is_prime_elem_def)
+ with p have "coprime (p^n) a \<or> coprime (p^n) b"
+ by (auto intro: is_prime_elem_imp_coprime coprime_exp_left)
+ with pab show ?thesis by (auto intro: coprime_dvd_mult simp: mult_ac)
+qed
+
+lemma primes_coprime:
+ "is_prime p \<Longrightarrow> is_prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> coprime p q"
+ using is_prime_imp_coprime primes_dvd_imp_eq by blast
+
end
@@ -683,12 +778,10 @@
using multiplicity_geI[of n] multiplicity_lessI[of n] by (cases "p ^ n dvd x") auto
lemma multiplicity_eq_zero_iff:
- assumes "x \<noteq> 0" "\<not>is_unit p"
shows "multiplicity p x = 0 \<longleftrightarrow> \<not>p dvd x"
using power_dvd_iff_le_multiplicity[of 1] by auto
lemma multiplicity_gt_zero_iff:
- assumes "x \<noteq> 0" "\<not>is_unit p"
shows "multiplicity p x > 0 \<longleftrightarrow> p dvd x"
using power_dvd_iff_le_multiplicity[of 1] by auto
@@ -716,6 +809,19 @@
lemma multiplicity_zero [simp]: "multiplicity p 0 = 0"
by (simp add: multiplicity_def)
+lemma prime_multiplicity_eq_zero_iff:
+ "is_prime_elem p \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> multiplicity p x = 0 \<longleftrightarrow> \<not>p dvd x"
+ by (rule multiplicity_eq_zero_iff) simp_all
+
+lemma prime_multiplicity_other:
+ assumes "is_prime p" "is_prime q" "p \<noteq> q"
+ shows "multiplicity p q = 0"
+ using assms by (subst prime_multiplicity_eq_zero_iff) (auto dest: primes_dvd_imp_eq)
+
+lemma prime_multiplicity_gt_zero_iff:
+ "is_prime_elem p \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> multiplicity p x > 0 \<longleftrightarrow> p dvd x"
+ by (rule multiplicity_gt_zero_iff) simp_all
+
lemma multiplicity_unit_left: "is_unit p \<Longrightarrow> multiplicity p x = 0"
by (simp add: multiplicity_def is_unit_power_iff unit_imp_dvd)
@@ -1008,7 +1114,7 @@
also have "multiplicity p \<dots> = multiplicity p x"
by (rule multiplicity_times_unit_right) (simp add: is_unit_unit_factor)
finally show ?thesis .
-qed simp_all
+qed simp_all
lemma prime_factorization_cong:
"normalize x = normalize y \<Longrightarrow> prime_factorization x = prime_factorization y"
@@ -1062,6 +1168,10 @@
finally show ?thesis ..
qed
+lemma prime_factorization_subset_imp_dvd:
+ "x \<noteq> 0 \<Longrightarrow> (prime_factorization x \<subseteq># prime_factorization y) \<Longrightarrow> x dvd y"
+ by (cases "y = 0") (simp_all add: prime_factorization_subset_iff_dvd)
+
lemma prime_factorization_divide:
assumes "b dvd a"
shows "prime_factorization (a div b) = prime_factorization a - prime_factorization b"
@@ -1077,6 +1187,204 @@
by (auto dest: in_prime_factorization_imp_prime)
+lemma prime_multiplicity_mult_distrib:
+ assumes "is_prime_elem p" "x \<noteq> 0" "y \<noteq> 0"
+ shows "multiplicity p (x * y) = multiplicity p x + multiplicity p y"
+proof -
+ have "multiplicity p (x * y) = count (prime_factorization (x * y)) (normalize p)"
+ by (subst count_prime_factorization_prime) (simp_all add: assms)
+ also from assms
+ have "prime_factorization (x * y) = prime_factorization x + prime_factorization y"
+ by (intro prime_factorization_mult)
+ also have "count \<dots> (normalize p) =
+ count (prime_factorization x) (normalize p) + count (prime_factorization y) (normalize p)"
+ by simp
+ also have "\<dots> = multiplicity p x + multiplicity p y"
+ by (subst (1 2) count_prime_factorization_prime) (simp_all add: assms)
+ finally show ?thesis .
+qed
+
+lemma prime_multiplicity_power_distrib:
+ assumes "is_prime_elem p" "x \<noteq> 0"
+ shows "multiplicity p (x ^ n) = n * multiplicity p x"
+ by (induction n) (simp_all add: assms prime_multiplicity_mult_distrib)
+
+lemma prime_multiplicity_msetprod_distrib:
+ assumes "is_prime_elem p" "0 \<notin># A"
+ shows "multiplicity p (msetprod A) = msetsum (image_mset (multiplicity p) A)"
+ using assms by (induction A) (auto simp: prime_multiplicity_mult_distrib)
+
+lemma prime_multiplicity_setprod_distrib:
+ assumes "is_prime_elem p" "0 \<notin> f ` A" "finite A"
+ shows "multiplicity p (setprod f A) = (\<Sum>x\<in>A. multiplicity p (f x))"
+proof -
+ have "multiplicity p (setprod f A) = (\<Sum>x\<in>#mset_set A. multiplicity p (f x))"
+ using assms by (subst setprod_unfold_msetprod)
+ (simp_all add: prime_multiplicity_msetprod_distrib setsum_unfold_msetsum
+ multiset.map_comp o_def)
+ also from \<open>finite A\<close> have "\<dots> = (\<Sum>x\<in>A. multiplicity p (f x))"
+ by (induction A rule: finite_induct) simp_all
+ finally show ?thesis .
+qed
+
+
+
+definition prime_factors where
+ "prime_factors x = set_mset (prime_factorization x)"
+
+lemma set_mset_prime_factorization:
+ "set_mset (prime_factorization x) = prime_factors x"
+ by (simp add: prime_factors_def)
+
+lemma prime_factorsI:
+ "x \<noteq> 0 \<Longrightarrow> is_prime p \<Longrightarrow> p dvd x \<Longrightarrow> p \<in> prime_factors x"
+ by (auto simp: prime_factors_def in_prime_factorization_iff)
+
+lemma prime_factors_prime [intro]: "p \<in> prime_factors x \<Longrightarrow> is_prime p"
+ by (auto simp: prime_factors_def dest: in_prime_factorization_imp_prime)
+
+lemma prime_factors_dvd [dest]: "p \<in> prime_factors x \<Longrightarrow> p dvd x"
+ by (auto simp: prime_factors_def dest: in_prime_factorization_imp_dvd)
+
+lemma prime_factors_finite [iff]:
+ "finite (prime_factors n)"
+ unfolding prime_factors_def by simp
+
+lemma prime_factors_altdef_multiplicity:
+ "prime_factors n = {p. is_prime p \<and> multiplicity p n > 0}"
+ by (cases "n = 0")
+ (auto simp: prime_factors_def prime_multiplicity_gt_zero_iff
+ prime_imp_prime_elem in_prime_factorization_iff)
+
+lemma setprod_prime_factors:
+ assumes "x \<noteq> 0"
+ shows "(\<Prod>p \<in> prime_factors x. p ^ multiplicity p x) = normalize x"
+proof -
+ have "normalize x = msetprod (prime_factorization x)"
+ by (simp add: msetprod_prime_factorization assms)
+ also have "\<dots> = (\<Prod>p \<in> prime_factors x. p ^ count (prime_factorization x) p)"
+ by (subst msetprod_multiplicity) (simp_all add: prime_factors_def)
+ also have "\<dots> = (\<Prod>p \<in> prime_factors x. p ^ multiplicity p x)"
+ by (intro setprod.cong)
+ (simp_all add: assms count_prime_factorization_prime prime_factors_prime)
+ finally show ?thesis ..
+qed
+
+(* TODO Move *)
+lemma (in semidom) setprod_zero_iff [simp]:
+ assumes "finite A"
+ shows "setprod f A = 0 \<longleftrightarrow> (\<exists>a\<in>A. f a = 0)"
+ using assms by (induct A) (auto simp: no_zero_divisors)
+(* END TODO *)
+
+lemma prime_factorization_unique'':
+ assumes S_eq: "S = {p. 0 < f p}"
+ and "finite S"
+ and S: "\<forall>p\<in>S. is_prime p" "normalize n = (\<Prod>p\<in>S. p ^ f p)"
+ shows "S = prime_factors n \<and> (\<forall>p. is_prime p \<longrightarrow> f p = multiplicity p n)"
+proof
+ define A where "A = Abs_multiset f"
+ from \<open>finite S\<close> S(1) have "(\<Prod>p\<in>S. p ^ f p) \<noteq> 0" by auto
+ with S(2) have nz: "n \<noteq> 0" by auto
+ from S_eq \<open>finite S\<close> have count_A: "count A x = f x" for x
+ unfolding A_def by (subst multiset.Abs_multiset_inverse) (simp_all add: multiset_def)
+ from S_eq count_A have set_mset_A: "set_mset A = S"
+ by (simp only: set_mset_def)
+ from S(2) have "normalize n = (\<Prod>p\<in>S. p ^ f p)" .
+ also have "\<dots> = msetprod A" by (simp add: msetprod_multiplicity S_eq set_mset_A count_A)
+ also from nz have "normalize n = msetprod (prime_factorization n)"
+ by (simp add: msetprod_prime_factorization)
+ finally have "prime_factorization (msetprod A) =
+ prime_factorization (msetprod (prime_factorization n))" by simp
+ also from S(1) have "prime_factorization (msetprod A) = A"
+ by (intro prime_factorization_msetprod_primes) (auto simp: set_mset_A)
+ also have "prime_factorization (msetprod (prime_factorization n)) = prime_factorization n"
+ by (intro prime_factorization_msetprod_primes) (auto dest: in_prime_factorization_imp_prime)
+ finally show "S = prime_factors n" by (simp add: prime_factors_def set_mset_A [symmetric])
+
+ show "(\<forall>p. is_prime p \<longrightarrow> f p = multiplicity p n)"
+ proof safe
+ fix p :: 'a assume p: "is_prime p"
+ have "multiplicity p n = multiplicity p (normalize n)" by simp
+ also have "normalize n = msetprod A"
+ by (simp add: msetprod_multiplicity S_eq set_mset_A count_A S)
+ also from p set_mset_A S(1)
+ have "multiplicity p \<dots> = msetsum (image_mset (multiplicity p) A)"
+ by (intro prime_multiplicity_msetprod_distrib) auto
+ also from S(1) p
+ have "image_mset (multiplicity p) A = image_mset (\<lambda>q. if p = q then 1 else 0) A"
+ by (intro image_mset_cong) (auto simp: set_mset_A multiplicity_self prime_multiplicity_other)
+ also have "msetsum \<dots> = f p" by (simp add: msetsum_delta' count_A)
+ finally show "f p = multiplicity p n" ..
+ qed
+qed
+
+lemma multiplicity_prime [simp]: "is_prime_elem p \<Longrightarrow> multiplicity p p = 1"
+ by (rule multiplicity_self) auto
+
+lemma multiplicity_prime_power [simp]: "is_prime_elem p \<Longrightarrow> multiplicity p (p ^ n) = n"
+ by (subst multiplicity_same_power') auto
+
+lemma prime_factors_product:
+ "x \<noteq> 0 \<Longrightarrow> y \<noteq> 0 \<Longrightarrow> prime_factors (x * y) = prime_factors x \<union> prime_factors y"
+ by (simp add: prime_factors_def prime_factorization_mult)
+
+lemma multiplicity_distinct_prime_power:
+ "is_prime p \<Longrightarrow> is_prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> multiplicity p (q ^ n) = 0"
+ by (subst prime_multiplicity_power_distrib) (auto simp: prime_multiplicity_other)
+
+lemma dvd_imp_multiplicity_le:
+ assumes "a dvd b" "b \<noteq> 0"
+ shows "multiplicity p a \<le> multiplicity p b"
+proof (cases "is_unit p")
+ case False
+ with assms show ?thesis
+ by (intro multiplicity_geI ) (auto intro: dvd_trans[OF multiplicity_dvd' assms(1)])
+qed (insert assms, auto simp: multiplicity_unit_left)
+
+lemma dvd_prime_factors [intro]:
+ "y \<noteq> 0 \<Longrightarrow> x dvd y \<Longrightarrow> prime_factors x \<subseteq> prime_factors y"
+ unfolding prime_factors_def
+ by (intro set_mset_mono, subst prime_factorization_subset_iff_dvd) auto
+
+(* RENAMED multiplicity_dvd *)
+lemma multiplicity_le_imp_dvd:
+ assumes "x \<noteq> 0" "\<And>p. is_prime p \<Longrightarrow> multiplicity p x \<le> multiplicity p y"
+ shows "x dvd y"
+proof (cases "y = 0")
+ case False
+ from assms this have "prime_factorization x \<subseteq># prime_factorization y"
+ by (intro mset_subset_eqI) (auto simp: count_prime_factorization)
+ with assms False show ?thesis by (subst (asm) prime_factorization_subset_iff_dvd)
+qed auto
+
+lemma dvd_multiplicity_eq:
+ "x \<noteq> 0 \<Longrightarrow> y \<noteq> 0 \<Longrightarrow> x dvd y \<longleftrightarrow> (\<forall>p. multiplicity p x \<le> multiplicity p y)"
+ by (auto intro: dvd_imp_multiplicity_le multiplicity_le_imp_dvd)
+
+lemma prime_factors_altdef: "x \<noteq> 0 \<Longrightarrow> prime_factors x = {p. is_prime p \<and> p dvd x}"
+ by (auto intro: prime_factorsI)
+
+lemma multiplicity_eq_imp_eq:
+ assumes "x \<noteq> 0" "y \<noteq> 0"
+ assumes "\<And>p. is_prime p \<Longrightarrow> multiplicity p x = multiplicity p y"
+ shows "normalize x = normalize y"
+ using assms by (intro associatedI multiplicity_le_imp_dvd) simp_all
+
+lemma prime_factorization_unique':
+ 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)"
+ shows "M = N"
+proof -
+ have "prime_factorization (\<Prod>i \<in># M. i) = prime_factorization (\<Prod>i \<in># N. i)"
+ by (simp only: assms)
+ also from assms have "prime_factorization (\<Prod>i \<in># M. i) = M"
+ by (subst prime_factorization_msetprod_primes) simp_all
+ also from assms have "prime_factorization (\<Prod>i \<in># N. i) = N"
+ by (subst prime_factorization_msetprod_primes) simp_all
+ finally show ?thesis .
+qed
+
+
definition "gcd_factorial a b = (if a = 0 then normalize b
else if b = 0 then normalize a
else msetprod (prime_factorization a #\<inter> prime_factorization b))"
@@ -1418,6 +1726,72 @@
by (standard, unfold Gcd_eq_Gcd_factorial Lcm_eq_Lcm_factorial)
(rule gcd_lcm_factorial; assumption)+
+lemma
+ assumes "x \<noteq> 0" "y \<noteq> 0"
+ shows gcd_eq_factorial':
+ "gcd x y = (\<Prod>p \<in> prime_factors x \<inter> prime_factors y.
+ p ^ min (multiplicity p x) (multiplicity p y))" (is "_ = ?rhs1")
+ and lcm_eq_factorial':
+ "lcm x y = (\<Prod>p \<in> prime_factors x \<union> prime_factors y.
+ p ^ max (multiplicity p x) (multiplicity p y))" (is "_ = ?rhs2")
+proof -
+ have "gcd x y = gcd_factorial x y" by (rule gcd_eq_gcd_factorial)
+ also have "\<dots> = ?rhs1"
+ by (auto simp: gcd_factorial_def assms msetprod_multiplicity set_mset_prime_factorization
+ count_prime_factorization_prime dest: prime_factors_prime intro!: setprod.cong)
+ finally show "gcd x y = ?rhs1" .
+ have "lcm x y = lcm_factorial x y" by (rule lcm_eq_lcm_factorial)
+ also have "\<dots> = ?rhs2"
+ by (auto simp: lcm_factorial_def assms msetprod_multiplicity set_mset_prime_factorization
+ count_prime_factorization_prime dest: prime_factors_prime intro!: setprod.cong)
+ finally show "lcm x y = ?rhs2" .
+qed
+
+lemma
+ assumes "x \<noteq> 0" "y \<noteq> 0" "is_prime p"
+ shows multiplicity_gcd: "multiplicity p (gcd x y) = min (multiplicity p x) (multiplicity p y)"
+ and multiplicity_lcm: "multiplicity p (lcm x y) = max (multiplicity p x) (multiplicity p y)"
+proof -
+ have "gcd x y = gcd_factorial x y" by (rule gcd_eq_gcd_factorial)
+ also from assms have "multiplicity p \<dots> = min (multiplicity p x) (multiplicity p y)"
+ by (simp add: count_prime_factorization_prime [symmetric] prime_factorization_gcd_factorial)
+ finally show "multiplicity p (gcd x y) = min (multiplicity p x) (multiplicity p y)" .
+ have "lcm x y = lcm_factorial x y" by (rule lcm_eq_lcm_factorial)
+ also from assms have "multiplicity p \<dots> = max (multiplicity p x) (multiplicity p y)"
+ by (simp add: count_prime_factorization_prime [symmetric] prime_factorization_lcm_factorial)
+ finally show "multiplicity p (lcm x y) = max (multiplicity p x) (multiplicity p y)" .
+qed
+
+lemma gcd_lcm_distrib:
+ "gcd x (lcm y z) = lcm (gcd x y) (gcd x z)"
+proof (cases "x = 0 \<or> y = 0 \<or> z = 0")
+ case True
+ thus ?thesis
+ by (auto simp: lcm_proj1_if_dvd lcm_proj2_if_dvd)
+next
+ case False
+ hence "normalize (gcd x (lcm y z)) = normalize (lcm (gcd x y) (gcd x z))"
+ by (intro associatedI prime_factorization_subset_imp_dvd)
+ (auto simp: lcm_eq_0_iff prime_factorization_gcd prime_factorization_lcm
+ subset_mset.inf_sup_distrib1)
+ thus ?thesis by simp
+qed
+
+lemma lcm_gcd_distrib:
+ "lcm x (gcd y z) = gcd (lcm x y) (lcm x z)"
+proof (cases "x = 0 \<or> y = 0 \<or> z = 0")
+ case True
+ thus ?thesis
+ by (auto simp: lcm_proj1_if_dvd lcm_proj2_if_dvd)
+next
+ case False
+ hence "normalize (lcm x (gcd y z)) = normalize (gcd (lcm x y) (lcm x z))"
+ by (intro associatedI prime_factorization_subset_imp_dvd)
+ (auto simp: lcm_eq_0_iff prime_factorization_gcd prime_factorization_lcm
+ subset_mset.sup_inf_distrib1)
+ thus ?thesis by simp
+qed
+
end
@@ -1430,37 +1804,5 @@
end
-
-lemma is_prime_elem_nat: "is_prime_elem (n::nat) \<longleftrightarrow> prime n"
-proof
- assume *: "is_prime_elem n"
- show "prime n" unfolding prime_def
- proof safe
- from * have "n \<noteq> 0" "n \<noteq> 1" by (intro notI, simp del: One_nat_def)+
- thus "n > 1" by (cases n) simp_all
- next
- fix m assume m: "m dvd n" "m \<noteq> n"
- from * \<open>m dvd n\<close> have "n dvd m \<or> is_unit m"
- by (intro irreducibleD' prime_imp_irreducible)
- with m show "m = 1" by (auto dest: dvd_antisym)
- qed
-qed (auto simp: is_prime_elem_def prime_gt_0_nat)
-
-lemma is_prime_nat: "is_prime (n::nat) \<longleftrightarrow> prime n"
- by (simp add: is_prime_def is_prime_elem_nat)
-
-lemma is_prime_elem_int: "is_prime_elem (n::int) \<longleftrightarrow> prime (nat (abs n))"
-proof (subst is_prime_elem_nat [symmetric], rule iffI)
- assume "is_prime_elem n"
- thus "is_prime_elem (nat (abs n))" by (auto simp: is_prime_elem_def nat_dvd_iff)
-next
- assume "is_prime_elem (nat (abs n))"
- thus "is_prime_elem n"
- by (auto simp: dvd_int_unfold_dvd_nat is_prime_elem_def abs_mult nat_mult_distrib)
-qed
-
-lemma is_prime_int: "is_prime (n::int) \<longleftrightarrow> prime n \<and> n \<ge> 0"
- by (simp add: is_prime_def is_prime_elem_int)
-
end
--- a/src/HOL/Number_Theory/Gauss.thy Wed Jul 20 14:52:09 2016 +0200
+++ b/src/HOL/Number_Theory/Gauss.thy Thu Jul 21 10:06:04 2016 +0200
@@ -109,10 +109,12 @@
assume c: "x \<le> (int p - 1) div 2"
assume d: "0 < y"
assume e: "y \<le> (int p - 1) div 2"
- from a p_a_relprime p_prime a_nonzero cong_mult_rcancel_int [of _ a x y]
- have "[x = y](mod p)"
- by (metis monoid_mult_class.mult.left_neutral cong_dvd_modulus_int cong_mult_rcancel_int
- cong_mult_self_int gcd.commute prime_imp_coprime_int)
+ from p_a_relprime have "\<not>p dvd a"
+ by (simp add: cong_altdef_int)
+ with p_prime have "coprime a (int p)"
+ by (subst gcd.commute, intro is_prime_imp_coprime) auto
+ with a cong_mult_rcancel_int [of a "int p" x y]
+ have "[x = y] (mod p)" by simp
with cong_less_imp_eq_int [of x y p] p_minus_one_l
order_le_less_trans [of x "(int p - 1) div 2" p]
order_le_less_trans [of y "(int p - 1) div 2" p]
@@ -137,11 +139,14 @@
assume d: "0 < y"
assume e: "y \<le> (int p - 1) div 2"
assume f: "x \<noteq> y"
- from a have "[x * a = y * a](mod p)"
+ from a have a': "[x * a = y * a](mod p)"
by (metis cong_int_def)
- with p_a_relprime p_prime cong_mult_rcancel_int [of a p x y]
- have "[x = y](mod p)"
- by (metis cong_mult_self_int dvd_div_mult_self gcd.commute prime_imp_coprime_int)
+ from p_a_relprime have "\<not>p dvd a"
+ by (simp add: cong_altdef_int)
+ with p_prime have "coprime a (int p)"
+ by (subst gcd.commute, intro is_prime_imp_coprime) auto
+ with a' cong_mult_rcancel_int [of a "int p" x y]
+ have "[x = y] (mod p)" by simp
with cong_less_imp_eq_int [of x y p] p_minus_one_l
order_le_less_trans [of x "(int p - 1) div 2" p]
order_le_less_trans [of y "(int p - 1) div 2" p]
@@ -170,7 +175,7 @@
by (auto simp add: A_def)
lemma B_ncong_p: "x \<in> B \<Longrightarrow> [x \<noteq> 0](mod p)"
- by (auto simp add: B_def) (metis cong_prime_prod_zero_int A_ncong_p p_a_relprime p_prime)
+ by (auto simp: B_def p_prime p_a_relprime A_ncong_p dest: cong_prime_prod_zero_int)
lemma B_greater_zero: "x \<in> B \<Longrightarrow> 0 < x"
using a_nonzero by (auto simp add: B_def A_greater_zero)
@@ -202,7 +207,7 @@
lemma all_A_relprime: assumes "x \<in> A" shows "gcd x p = 1"
using p_prime A_ncong_p [OF assms]
- by (simp add: cong_altdef_int) (metis gcd.commute prime_imp_coprime_int)
+ by (auto simp: cong_altdef_int gcd.commute[of _ "int p"] intro!: is_prime_imp_coprime)
lemma A_prod_relprime: "gcd (setprod id A) p = 1"
by (metis id_def all_A_relprime setprod_coprime)
@@ -266,7 +271,7 @@
by (metis cong_int_def mod_add_left_eq mod_add_right_eq mult.commute ring_class.ring_distribs(1))
with p_prime a_nonzero p_a_relprime
have a: "[y + z = 0] (mod p)"
- by (metis cong_prime_prod_zero_int)
+ by (auto dest!: cong_prime_prod_zero_int)
assume b: "y \<in> A" and c: "z \<in> A"
with A_def have "0 < y + z"
by auto
--- a/src/HOL/Number_Theory/Pocklington.thy Wed Jul 20 14:52:09 2016 +0200
+++ b/src/HOL/Number_Theory/Pocklington.thy Thu Jul 21 10:06:04 2016 +0200
@@ -11,39 +11,17 @@
subsection\<open>Lemmas about previously defined terms\<close>
lemma prime:
- "prime p \<longleftrightarrow> p \<noteq> 0 \<and> p \<noteq> 1 \<and> (\<forall>m. 0 < m \<and> m < p \<longrightarrow> coprime p m)"
- (is "?lhs \<longleftrightarrow> ?rhs")
-proof-
- {assume "p=0 \<or> p=1" hence ?thesis
- by (metis one_not_prime_nat zero_not_prime_nat)}
- moreover
- {assume p0: "p\<noteq>0" "p\<noteq>1"
- {assume H: "?lhs"
- {fix m assume m: "m > 0" "m < p"
- {assume "m=1" hence "coprime p m" by simp}
- moreover
- {assume "p dvd m" hence "p \<le> m" using dvd_imp_le m by blast with m(2)
- have "coprime p m" by simp}
- ultimately have "coprime p m"
- by (metis H prime_imp_coprime_nat)}
- hence ?rhs using p0 by auto}
- moreover
- { assume H: "\<forall>m. 0 < m \<and> m < p \<longrightarrow> coprime p m"
- obtain q where q: "prime q" "q dvd p"
- by (metis p0(2) prime_factor_nat)
- have q0: "q > 0"
- by (metis prime_gt_0_nat q(1))
- from dvd_imp_le[OF q(2)] p0 have qp: "q \<le> p" by arith
- {assume "q = p" hence ?lhs using q(1) by blast}
- moreover
- {assume "q\<noteq>p" with qp have qplt: "q < p" by arith
- from H qplt q0 have "coprime p q" by arith
- hence ?lhs using q
- by (auto dest: gcd_nat.absorb2)}
- ultimately have ?lhs by blast}
- ultimately have ?thesis by blast}
- ultimately show ?thesis by (cases"p=0 \<or> p=1", auto)
-qed
+ "prime (p::nat) \<longleftrightarrow> p \<noteq> 0 \<and> p \<noteq> 1 \<and> (\<forall>m. 0 < m \<and> m < p \<longrightarrow> coprime p m)"
+ unfolding is_prime_nat_iff
+proof safe
+ fix m assume p: "p > 0" "p \<noteq> 1" and m: "m dvd p" "m \<noteq> p"
+ and *: "\<forall>m. m > 0 \<and> m < p \<longrightarrow> coprime p m"
+ from p m have "m \<noteq> 0" by (intro notI) auto
+ moreover from p m have "m < p" by (auto dest: dvd_imp_le)
+ ultimately have "coprime p m" using * by blast
+ with m show "m = 1" by simp
+qed (auto simp: is_prime_nat_iff simp del: One_nat_def
+ intro!: is_prime_imp_coprime dest: dvd_imp_le)
lemma finite_number_segment: "card { m. 0 < m \<and> m < n } = n - 1"
proof-
@@ -94,7 +72,7 @@
qed
lemma cong_solve_unique_nontrivial:
- assumes p: "prime p" and pa: "coprime p a" and x0: "0 < x" and xp: "x < p"
+ assumes p: "prime (p::nat)" and pa: "coprime p a" and x0: "0 < x" and xp: "x < p"
shows "\<exists>!y. 0 < y \<and> y < p \<and> [x * y = a] (mod p)"
proof-
from pa have ap: "coprime a p"
@@ -107,12 +85,12 @@
with y(2) have th: "p dvd a"
by (auto dest: cong_dvd_eq_nat)
have False
- by (metis gcd_nat.absorb1 one_not_prime_nat p pa th)}
+ by (metis gcd_nat.absorb1 not_is_prime_1 p pa th)}
with y show ?thesis unfolding Ex1_def using neq0_conv by blast
qed
lemma cong_unique_inverse_prime:
- assumes "prime p" and "0 < x" and "x < p"
+ assumes "prime (p::nat)" and "0 < x" and "x < p"
shows "\<exists>!y. 0 < y \<and> y < p \<and> [x * y = 1] (mod p)"
by (rule cong_solve_unique_nontrivial) (insert assms, simp_all)
@@ -445,28 +423,28 @@
subsection\<open>Another trivial primality characterization\<close>
lemma prime_prime_factor:
- "prime n \<longleftrightarrow> n \<noteq> 1 \<and> (\<forall>p. prime p \<and> p dvd n \<longrightarrow> p = n)"
+ "prime (n::nat) \<longleftrightarrow> n \<noteq> 1 \<and> (\<forall>p. prime p \<and> p dvd n \<longrightarrow> p = n)"
(is "?lhs \<longleftrightarrow> ?rhs")
proof (cases "n=0 \<or> n=1")
case True
then show ?thesis
- by (metis bigger_prime dvd_0_right one_not_prime_nat zero_not_prime_nat)
+ by (metis bigger_prime dvd_0_right not_is_prime_1 not_is_prime_0)
next
case False
show ?thesis
proof
assume "prime n"
then show ?rhs
- by (metis one_not_prime_nat prime_def)
+ by (metis not_is_prime_1 is_prime_nat_iff)
next
assume ?rhs
with False show "prime n"
- by (auto simp: prime_def) (metis One_nat_def prime_factor_nat prime_def)
+ by (auto simp: is_prime_nat_iff) (metis One_nat_def prime_factor_nat is_prime_nat_iff)
qed
qed
lemma prime_divisor_sqrt:
- "prime n \<longleftrightarrow> n \<noteq> 1 \<and> (\<forall>d. d dvd n \<and> d\<^sup>2 \<le> n \<longrightarrow> d = 1)"
+ "prime (n::nat) \<longleftrightarrow> n \<noteq> 1 \<and> (\<forall>d. d dvd n \<and> d\<^sup>2 \<le> n \<longrightarrow> d = 1)"
proof -
{assume "n=0 \<or> n=1" hence ?thesis
by auto}
@@ -497,17 +475,17 @@
with H[rule_format, of e] h have "e=1" by simp
with e have "d = n" by simp}
ultimately have "d=1 \<or> d=n" by blast}
- ultimately have ?thesis unfolding prime_def using np n(2) by blast}
+ ultimately have ?thesis unfolding is_prime_nat_iff using np n(2) by blast}
ultimately show ?thesis by auto
qed
lemma prime_prime_factor_sqrt:
- "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)"
+ "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)"
(is "?lhs \<longleftrightarrow>?rhs")
proof-
{assume "n=0 \<or> n=1"
hence ?thesis
- by (metis one_not_prime_nat zero_not_prime_nat)}
+ by (metis not_is_prime_0 not_is_prime_1)}
moreover
{assume n: "n\<noteq>0" "n\<noteq>1"
{assume H: ?lhs
@@ -535,10 +513,10 @@
lemma pocklington_lemma:
assumes n: "n \<ge> 2" and nqr: "n - 1 = q*r" and an: "[a^ (n - 1) = 1] (mod n)"
and aq:"\<forall>p. prime p \<and> p dvd q \<longrightarrow> coprime (a^ ((n - 1) div p) - 1) n"
- and pp: "prime p" and pn: "p dvd n"
+ and pp: "prime (p::nat)" and pn: "p dvd n"
shows "[p = 1] (mod q)"
proof -
- 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)
+ have p01: "p \<noteq> 0" "p \<noteq> 1" using pp by (auto intro: prime_gt_0_nat)
obtain k where k: "a ^ (q * r) - 1 = n*k"
by (metis an cong_to_1_nat dvd_def nqr)
from pn[unfolded dvd_def] obtain l where l: "n = p*l" by blast
@@ -561,7 +539,7 @@
from aq P(1) Pq have caP:"coprime (a^ ((n - 1) div P) - 1) n" by blast
from Pq obtain s where s: "q = P*s" unfolding dvd_def by blast
have P0: "P \<noteq> 0" using P(1)
- by (metis zero_not_prime_nat)
+ by (metis not_is_prime_0)
from P(2) obtain t where t: "d = P*t" unfolding dvd_def by blast
from d s t P0 have s': "ord p (a^r) * t = s"
by (metis mult.commute mult_cancel1 mult.assoc)
@@ -581,7 +559,7 @@
hence o: "ord p (a^r) = q" using d by simp
from pp phi_prime[of p] have phip: "phi p = p - 1" by simp
{fix d assume d: "d dvd p" "d dvd a" "d \<noteq> 1"
- from pp[unfolded prime_def] d have dp: "d = p" by blast
+ from pp[unfolded is_prime_nat_iff] d have dp: "d = p" by blast
from n have "n \<noteq> 0" by simp
then have False using d dp pn
by auto (metis One_nat_def Suc_pred an dvd_1_iff_1 gcd_greatest_iff lucas_coprime_lemma)}
@@ -667,36 +645,28 @@
(* FIXME some overlap with material in UniqueFactorization, class unique_factorization *)
-definition "primefact ps n = (foldr op * ps 1 = n \<and> (\<forall>p\<in> set ps. prime p))"
+definition "primefact ps n = (foldr op * ps 1 = n \<and> (\<forall>p\<in> set ps. prime p))"
-lemma primefact: assumes n: "n \<noteq> 0"
+lemma primefact:
+ assumes n: "n \<noteq> (0::nat)"
shows "\<exists>ps. primefact ps n"
-using n
-proof(induct n rule: nat_less_induct)
- fix n assume H: "\<forall>m<n. m \<noteq> 0 \<longrightarrow> (\<exists>ps. primefact ps m)" and n: "n\<noteq>0"
- let ?ths = "\<exists>ps. primefact ps n"
- {assume "n = 1"
- hence "primefact [] n" by (simp add: primefact_def)
- hence ?ths by blast }
- moreover
- {assume n1: "n \<noteq> 1"
- with n have n2: "n \<ge> 2" by arith
- obtain p where p: "prime p" "p dvd n"
- by (metis n1 prime_factor_nat)
- from p(2) obtain m where m: "n = p*m" unfolding dvd_def by blast
- from n m have m0: "m > 0" "m\<noteq>0" by auto
- have "1 < p"
- by (metis p(1) prime_def)
- with m0 m have mn: "m < n" by auto
- from H[rule_format, OF mn m0(2)] obtain ps where ps: "primefact ps m" ..
- from ps m p(1) have "primefact (p#ps) n" by (simp add: primefact_def)
- hence ?ths by blast}
- ultimately show ?ths by blast
+proof -
+ have "\<exists>xs. mset xs = prime_factorization n" by (rule ex_mset)
+ then guess xs .. note xs = this
+ from assms have "n = msetprod (prime_factorization n)"
+ by (simp add: msetprod_prime_factorization)
+ also have "\<dots> = msetprod (mset xs)" by (simp add: xs)
+ also have "\<dots> = foldr op * xs 1" by (induction xs) simp_all
+ finally have "foldr op * xs 1 = n" ..
+ moreover have "\<forall>p\<in>#mset xs. prime p"
+ by (subst xs) (auto dest: in_prime_factorization_imp_prime)
+ ultimately have "primefact xs n" by (auto simp: primefact_def)
+ thus ?thesis ..
qed
lemma primefact_contains:
assumes pf: "primefact ps n" and p: "prime p" and pn: "p dvd n"
- shows "p \<in> set ps"
+ shows "(p::nat) \<in> set ps"
using pf p pn
proof(induct ps arbitrary: p n)
case Nil thus ?case by (auto simp add: primefact_def)
@@ -705,7 +675,7 @@
from Cons.prems[unfolded primefact_def]
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
{assume "p dvd q"
- with p(1) q(1) have "p = q" unfolding prime_def by auto
+ with p(1) q(1) have "p = q" unfolding is_prime_nat_iff by auto
hence ?case by simp}
moreover
{ assume h: "p dvd foldr op * qs 1"
@@ -760,7 +730,7 @@
from psp primefact_contains[OF pfpsq p]
have p': "coprime (a ^ (r * (q div p)) mod n - 1) n"
by (simp add: list_all_iff)
- from p prime_def have p01: "p \<noteq> 0" "p \<noteq> 1" "p =Suc(p - 1)"
+ from p is_prime_nat_iff have p01: "p \<noteq> 0" "p \<noteq> 1" "p =Suc(p - 1)"
by auto
from div_mult1_eq[of r q p] p(2)
have eq1: "r* (q div p) = (n - 1) div p"
--- a/src/HOL/Number_Theory/Primes.thy Wed Jul 20 14:52:09 2016 +0200
+++ b/src/HOL/Number_Theory/Primes.thy Thu Jul 21 10:06:04 2016 +0200
@@ -1,5 +1,6 @@
(* Authors: Christophe Tabacznyj, Lawrence C. Paulson, Amine Chaieb,
- Thomas M. Rasmussen, Jeremy Avigad, Tobias Nipkow
+ Thomas M. Rasmussen, Jeremy Avigad, Tobias Nipkow,
+ Manuel Eberl
This file deals with properties of primes. Definitions and lemmas are
@@ -22,211 +23,246 @@
natural numbers and the integers, and added a number of new theorems.
Tobias Nipkow cleaned up a lot.
+
+Florian Haftmann and Manuel Eberl put primality and prime factorisation
+onto an algebraic foundation and thus generalised these concepts to
+other rings, such as polynomials. (see also the Factorial_Ring theory).
+
+There were also previous formalisations of unique factorisation by
+Thomas Marthedal Rasmussen, Jeremy Avigad, and David Gray.
*)
section \<open>Primes\<close>
theory Primes
-imports "~~/src/HOL/GCD" "~~/src/HOL/Binomial"
+imports "~~/src/HOL/Binomial" Euclidean_Algorithm
begin
+(* As a simp or intro rule,
+
+ prime p \<Longrightarrow> p > 0
+
+ wreaks havoc here. When the premise includes \<forall>x \<in># M. prime x, it
+ leads to the backchaining
+
+ x > 0
+ prime x
+ x \<in># M which is, unfortunately,
+ count M x > 0
+*)
+
declare [[coercion int]]
declare [[coercion_enabled]]
-definition prime :: "nat \<Rightarrow> bool"
- where "prime p = (1 < p \<and> (\<forall>m. m dvd p \<longrightarrow> m = 1 \<or> m = p))"
+abbreviation (input) "prime \<equiv> is_prime"
+
+lemma is_prime_elem_nat_iff:
+ "is_prime_elem (n :: nat) \<longleftrightarrow> (1 < n \<and> (\<forall>m. m dvd n \<longrightarrow> m = 1 \<or> m = n))"
+proof safe
+ assume *: "is_prime_elem n"
+ from * have "n \<noteq> 0" "n \<noteq> 1" by (intro notI, simp del: One_nat_def)+
+ thus "n > 1" by (cases n) simp_all
+ fix m assume m: "m dvd n" "m \<noteq> n"
+ from * \<open>m dvd n\<close> have "n dvd m \<or> is_unit m"
+ by (intro irreducibleD' prime_imp_irreducible)
+ with m show "m = 1" by (auto dest: dvd_antisym)
+next
+ assume "n > 1" "\<forall>m. m dvd n \<longrightarrow> m = 1 \<or> m = n"
+ thus "is_prime_elem n"
+ by (auto simp: prime_iff_irreducible irreducible_altdef)
+qed
+
+lemma is_prime_nat_iff_is_prime_elem: "is_prime (n :: nat) \<longleftrightarrow> is_prime_elem n"
+ by (simp add: is_prime_def)
-subsection \<open>Primes\<close>
+lemma is_prime_nat_iff:
+ "is_prime (n :: nat) \<longleftrightarrow> (1 < n \<and> (\<forall>m. m dvd n \<longrightarrow> m = 1 \<or> m = n))"
+ by (simp add: is_prime_nat_iff_is_prime_elem is_prime_elem_nat_iff)
-lemma prime_odd_nat: "prime p \<Longrightarrow> p > 2 \<Longrightarrow> odd p"
- using nat_dvd_1_iff_1 odd_one prime_def by blast
+lemma is_prime_elem_int_nat_transfer: "is_prime_elem (n::int) \<longleftrightarrow> is_prime_elem (nat (abs n))"
+proof
+ assume "is_prime_elem n"
+ thus "is_prime_elem (nat (abs n))" by (auto simp: is_prime_elem_def nat_dvd_iff)
+next
+ assume "is_prime_elem (nat (abs n))"
+ thus "is_prime_elem n"
+ by (auto simp: dvd_int_unfold_dvd_nat is_prime_elem_def abs_mult nat_mult_distrib)
+qed
+
+lemma is_prime_elem_nat_int_transfer [simp]: "is_prime_elem (int n) \<longleftrightarrow> is_prime_elem n"
+ by (auto simp: is_prime_elem_int_nat_transfer)
+
+lemma is_prime_nat_int_transfer [simp]: "is_prime (int n) \<longleftrightarrow> is_prime n"
+ by (auto simp: is_prime_elem_int_nat_transfer is_prime_def)
+
+lemma is_prime_int_nat_transfer: "is_prime (n::int) \<longleftrightarrow> n \<ge> 0 \<and> is_prime (nat n)"
+ by (auto simp: is_prime_elem_int_nat_transfer is_prime_def)
-lemma prime_gt_0_nat: "prime p \<Longrightarrow> p > 0"
- unfolding prime_def by auto
+lemma is_prime_int_iff:
+ "is_prime (n::int) \<longleftrightarrow> (1 < n \<and> (\<forall>m. m \<ge> 0 \<and> m dvd n \<longrightarrow> m = 1 \<or> m = n))"
+proof (intro iffI conjI allI impI; (elim conjE)?)
+ assume *: "is_prime n"
+ hence irred: "irreducible n" by (simp add: prime_imp_irreducible)
+ from * have "n \<ge> 0" "n \<noteq> 0" "n \<noteq> 1"
+ by (auto simp: is_prime_def zabs_def not_less split: if_splits)
+ thus "n > 1" by presburger
+ fix m assume "m dvd n" \<open>m \<ge> 0\<close>
+ with irred have "m dvd 1 \<or> n dvd m" by (auto simp: irreducible_altdef)
+ with \<open>m dvd n\<close> \<open>m \<ge> 0\<close> \<open>n > 1\<close> show "m = 1 \<or> m = n"
+ using associated_iff_dvd[of m n] by auto
+next
+ assume n: "1 < n" "\<forall>m. m \<ge> 0 \<and> m dvd n \<longrightarrow> m = 1 \<or> m = n"
+ hence "nat n > 1" by simp
+ moreover have "\<forall>m. m dvd nat n \<longrightarrow> m = 1 \<or> m = nat n"
+ proof (intro allI impI)
+ fix m assume "m dvd nat n"
+ with \<open>n > 1\<close> have "int m dvd n" by (auto simp: int_dvd_iff)
+ with n(2) have "int m = 1 \<or> int m = n" by auto
+ thus "m = 1 \<or> m = nat n" by auto
+ qed
+ ultimately show "is_prime n"
+ unfolding is_prime_int_nat_transfer is_prime_nat_iff by auto
+qed
-lemma prime_ge_1_nat: "prime p \<Longrightarrow> p >= 1"
- unfolding prime_def by auto
+
+lemma prime_nat_not_dvd:
+ assumes "prime p" "p > n" "n \<noteq> (1::nat)"
+ shows "\<not>n dvd p"
+proof
+ assume "n dvd p"
+ from assms(1) have "irreducible p" by (simp add: prime_imp_irreducible)
+ from irreducibleD'[OF this \<open>n dvd p\<close>] \<open>n dvd p\<close> \<open>p > n\<close> assms show False
+ by (cases "n = 0") (auto dest!: dvd_imp_le)
+qed
-lemma prime_gt_1_nat: "prime p \<Longrightarrow> p > 1"
- unfolding prime_def by auto
+lemma prime_int_not_dvd:
+ assumes "prime p" "p > n" "n > (1::int)"
+ shows "\<not>n dvd p"
+proof
+ assume "n dvd p"
+ from assms(1) have "irreducible p" by (simp add: prime_imp_irreducible)
+ from irreducibleD'[OF this \<open>n dvd p\<close>] \<open>n dvd p\<close> \<open>p > n\<close> assms show False
+ by (auto dest!: zdvd_imp_le)
+qed
+
+lemma prime_odd_nat: "prime p \<Longrightarrow> p > (2::nat) \<Longrightarrow> odd p"
+ by (intro prime_nat_not_dvd) auto
+
+lemma prime_odd_int: "prime p \<Longrightarrow> p > (2::int) \<Longrightarrow> odd p"
+ by (intro prime_int_not_dvd) auto
-lemma prime_ge_Suc_0_nat: "prime p \<Longrightarrow> p >= Suc 0"
- unfolding prime_def by auto
+lemma prime_ge_0_int: "prime p \<Longrightarrow> p \<ge> (0::int)"
+ unfolding is_prime_int_iff by auto
+
+lemma prime_gt_0_nat: "prime p \<Longrightarrow> p > (0::nat)"
+ unfolding is_prime_nat_iff by auto
+
+lemma prime_gt_0_int: "prime p \<Longrightarrow> p > (0::int)"
+ unfolding is_prime_int_iff by auto
+
+lemma prime_ge_1_nat: "prime p \<Longrightarrow> p \<ge> (1::nat)"
+ unfolding is_prime_nat_iff by auto
+
+lemma prime_ge_Suc_0_nat: "prime p \<Longrightarrow> p \<ge> Suc 0"
+ unfolding is_prime_nat_iff by auto
+
+lemma prime_ge_1_int: "prime p \<Longrightarrow> p \<ge> (1::int)"
+ unfolding is_prime_int_iff by auto
+
+lemma prime_gt_1_nat: "prime p \<Longrightarrow> p > (1::nat)"
+ unfolding is_prime_nat_iff by auto
lemma prime_gt_Suc_0_nat: "prime p \<Longrightarrow> p > Suc 0"
- unfolding prime_def by auto
+ unfolding is_prime_nat_iff by auto
-lemma prime_ge_2_nat: "prime p \<Longrightarrow> p >= 2"
- unfolding prime_def by auto
+lemma prime_gt_1_int: "prime p \<Longrightarrow> p > (1::int)"
+ unfolding is_prime_int_iff by auto
-lemma prime_imp_coprime_nat: "prime p \<Longrightarrow> \<not> p dvd n \<Longrightarrow> coprime p n"
- apply (unfold prime_def)
- apply (metis gcd_dvd1 gcd_dvd2)
- done
+lemma prime_ge_2_nat: "prime p \<Longrightarrow> p \<ge> (2::nat)"
+ unfolding is_prime_nat_iff by auto
+
+lemma prime_ge_2_int: "prime p \<Longrightarrow> p \<ge> (2::int)"
+ unfolding is_prime_int_iff by auto
lemma prime_int_altdef:
"prime p = (1 < p \<and> (\<forall>m::int. m \<ge> 0 \<longrightarrow> m dvd p \<longrightarrow>
m = 1 \<or> m = p))"
- apply (simp add: prime_def)
- apply (auto simp add: )
- apply (metis One_nat_def of_nat_1 nat_0_le nat_dvd_iff)
- apply (metis zdvd_int One_nat_def le0 of_nat_0 of_nat_1 of_nat_eq_iff of_nat_le_iff)
- done
-
-lemma prime_imp_coprime_int:
- fixes n::int shows "prime p \<Longrightarrow> \<not> p dvd n \<Longrightarrow> coprime p n"
- apply (unfold prime_int_altdef)
- apply (metis gcd_dvd1 gcd_dvd2 gcd_ge_0_int)
- done
-
-lemma prime_dvd_mult_nat: "prime p \<Longrightarrow> p dvd m * n \<Longrightarrow> p dvd m \<or> p dvd n"
- by (blast intro: coprime_dvd_mult prime_imp_coprime_nat)
-
-lemma prime_dvd_mult_int:
- fixes n::int shows "prime p \<Longrightarrow> p dvd m * n \<Longrightarrow> p dvd m \<or> p dvd n"
- by (blast intro: coprime_dvd_mult prime_imp_coprime_int)
-
-lemma prime_dvd_mult_eq_nat [simp]: "prime p \<Longrightarrow>
- p dvd m * n = (p dvd m \<or> p dvd n)"
- by (rule iffI, rule prime_dvd_mult_nat, auto)
-
-lemma prime_dvd_mult_eq_int [simp]:
- fixes n::int
- shows "prime p \<Longrightarrow> p dvd m * n = (p dvd m \<or> p dvd n)"
- by (rule iffI, rule prime_dvd_mult_int, auto)
+ unfolding is_prime_int_iff by blast
lemma not_prime_eq_prod_nat:
- "1 < n \<Longrightarrow> \<not> prime n \<Longrightarrow>
- \<exists>m k. n = m * k \<and> 1 < m \<and> m < n \<and> 1 < k \<and> k < n"
- unfolding prime_def dvd_def apply (auto simp add: ac_simps)
- by (metis Suc_lessD Suc_lessI n_less_m_mult_n n_less_n_mult_m nat_0_less_mult_iff)
-
-lemma prime_dvd_power_nat: "prime p \<Longrightarrow> p dvd x^n \<Longrightarrow> p dvd x"
- by (induct n) auto
-
-lemma prime_dvd_power_int:
- fixes x::int shows "prime p \<Longrightarrow> p dvd x^n \<Longrightarrow> p dvd x"
- by (induct n) auto
-
-lemma prime_dvd_power_nat_iff: "prime p \<Longrightarrow> n > 0 \<Longrightarrow>
- p dvd x^n \<longleftrightarrow> p dvd x"
- by (cases n) (auto elim: prime_dvd_power_nat)
-
-lemma prime_dvd_power_int_iff:
- fixes x::int
- shows "prime p \<Longrightarrow> n > 0 \<Longrightarrow> p dvd x^n \<longleftrightarrow> p dvd x"
- by (cases n) (auto elim: prime_dvd_power_int)
+ assumes "m > 1" "\<not>prime (m::nat)"
+ shows "\<exists>n k. n = m * k \<and> 1 < m \<and> m < n \<and> 1 < k \<and> k < n"
+ using assms irreducible_altdef[of m]
+ by (auto simp: prime_iff_irreducible is_prime_def irreducible_altdef)
subsubsection \<open>Make prime naively executable\<close>
-lemma zero_not_prime_nat [simp]: "~prime (0::nat)"
- by (simp add: prime_def)
-
-lemma one_not_prime_nat [simp]: "~prime (1::nat)"
- by (simp add: prime_def)
+lemma Suc_0_not_prime_nat [simp]: "~prime (Suc 0)"
+ unfolding One_nat_def [symmetric] by (rule not_is_prime_1)
-lemma Suc_0_not_prime_nat [simp]: "~prime (Suc 0)"
- by (simp add: prime_def)
+lemma prime_nat_code [code_unfold]:
+ "prime (p::nat) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {1<..<p}. ~ n dvd p)"
+proof safe
+ assume "p > 1" and *: "\<forall>n\<in>{1<..<p}. \<not>n dvd p"
+ show "is_prime p" unfolding is_prime_nat_iff
+ proof (intro conjI allI impI)
+ fix m assume "m dvd p"
+ with \<open>p > 1\<close> have "m \<noteq> 0" by (intro notI) auto
+ hence "m \<ge> 1" by simp
+ moreover from \<open>m dvd p\<close> and * have "m \<notin> {1<..<p}" by blast
+ with \<open>m dvd p\<close> and \<open>p > 1\<close> have "m \<le> 1 \<or> m = p" by (auto dest: dvd_imp_le)
+ ultimately show "m = 1 \<or> m = p" by simp
+ qed fact+
+qed (auto simp: is_prime_nat_iff)
-lemma prime_nat_code [code]:
- "prime p \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {1<..<p}. ~ n dvd p)"
- apply (simp add: Ball_def)
- apply (metis One_nat_def less_not_refl prime_def dvd_triv_right not_prime_eq_prod_nat)
- done
+lemma prime_int_code [code_unfold]:
+ "prime (p::int) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {1<..<p}. ~ n dvd p)" (is "?lhs \<longleftrightarrow> ?rhs")
+proof
+ assume "?lhs"
+ thus "?rhs" by (auto simp: is_prime_int_nat_transfer dvd_int_unfold_dvd_nat prime_nat_code)
+next
+ assume "?rhs"
+ thus "?lhs" by (auto simp: is_prime_int_nat_transfer zdvd_int prime_nat_code)
+qed
lemma prime_nat_simp:
"prime p \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> set [2..<p]. \<not> n dvd p)"
by (auto simp add: prime_nat_code)
+lemma prime_int_simp:
+ "prime (p::int) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {2..<p}. \<not> n dvd p)"
+ by (auto simp add: prime_int_code)
+
lemmas prime_nat_simp_numeral [simp] = prime_nat_simp [of "numeral m"] for m
lemma two_is_prime_nat [simp]: "prime (2::nat)"
by simp
+declare is_prime_int_nat_transfer[of "numeral m" for m, simp]
+
+
text\<open>A bit of regression testing:\<close>
lemma "prime(97::nat)" by simp
lemma "prime(997::nat)" by eval
-
-
-lemma prime_imp_power_coprime_nat: "prime p \<Longrightarrow> ~ p dvd a \<Longrightarrow> coprime a (p^m)"
- by (metis coprime_exp gcd.commute prime_imp_coprime_nat)
-
-lemma prime_imp_power_coprime_int:
- fixes a::int shows "prime p \<Longrightarrow> ~ p dvd a \<Longrightarrow> coprime a (p^m)"
- by (metis coprime_exp gcd.commute prime_imp_coprime_int)
-
-lemma primes_coprime_nat: "prime p \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> coprime p q"
- by (metis gcd_nat.absorb1 gcd_nat.absorb2 prime_imp_coprime_nat)
-
-lemma primes_imp_powers_coprime_nat:
- "prime p \<Longrightarrow> prime q \<Longrightarrow> p ~= q \<Longrightarrow> coprime (p^m) (q^n)"
- by (rule coprime_exp2_nat, rule primes_coprime_nat)
-
-lemma prime_factor_nat:
- "n \<noteq> (1::nat) \<Longrightarrow> \<exists>p. prime p \<and> p dvd n"
-proof (induct n rule: nat_less_induct)
- case (1 n) show ?case
- proof (cases "n = 0")
- case True then show ?thesis
- by (auto intro: two_is_prime_nat)
- next
- case False with "1.prems" have "n > 1" by simp
- with "1.hyps" show ?thesis
- by (metis One_nat_def dvd_mult dvd_refl not_prime_eq_prod_nat order_less_irrefl)
- qed
-qed
-
-text \<open>One property of coprimality is easier to prove via prime factors.\<close>
+lemma "prime(97::int)" by simp
+lemma "prime(997::int)" by eval
-lemma prime_divprod_pow_nat:
- assumes p: "prime p" and ab: "coprime a b" and pab: "p^n dvd a * b"
- shows "p^n dvd a \<or> p^n dvd b"
-proof-
- { assume "n = 0 \<or> a = 1 \<or> b = 1" with pab have ?thesis
- apply (cases "n=0", simp_all)
- apply (cases "a=1", simp_all)
- done }
- moreover
- { assume n: "n \<noteq> 0" and a: "a\<noteq>1" and b: "b\<noteq>1"
- then obtain m where m: "n = Suc m" by (cases n) auto
- from n have "p dvd p^n" apply (intro dvd_power) apply auto done
- also note pab
- finally have pab': "p dvd a * b".
- from prime_dvd_mult_nat[OF p pab']
- have "p dvd a \<or> p dvd b" .
- moreover
- { assume pa: "p dvd a"
- from coprime_common_divisor_nat [OF ab, OF pa] p have "\<not> p dvd b" by auto
- with p have "coprime b p"
- by (subst gcd.commute, intro prime_imp_coprime_nat)
- then have pnb: "coprime (p^n) b"
- by (subst gcd.commute, rule coprime_exp)
- from coprime_dvd_mult[OF pnb pab] have ?thesis by blast }
- moreover
- { assume pb: "p dvd b"
- have pnba: "p^n dvd b*a" using pab by (simp add: mult.commute)
- from coprime_common_divisor_nat [OF ab, of p] pb p have "\<not> p dvd a"
- by auto
- with p have "coprime a p"
- by (subst gcd.commute, intro prime_imp_coprime_nat)
- then have pna: "coprime (p^n) a"
- by (subst gcd.commute, rule coprime_exp)
- from coprime_dvd_mult[OF pna pnba] have ?thesis by blast }
- ultimately have ?thesis by blast }
- ultimately show ?thesis by blast
-qed
+lemma prime_factor_nat:
+ "n \<noteq> (1::nat) \<Longrightarrow> \<exists>p. prime p \<and> p dvd n"
+ using prime_divisor_exists[of n]
+ by (cases "n = 0") (auto intro: exI[of _ "2::nat"])
subsection \<open>Infinitely many primes\<close>
-lemma next_prime_bound: "\<exists>p. prime p \<and> n < p \<and> p <= fact n + 1"
+lemma next_prime_bound: "\<exists>p::nat. prime p \<and> n < p \<and> p \<le> fact n + 1"
proof-
have f1: "fact n + 1 \<noteq> (1::nat)" using fact_ge_1 [of n, where 'a=nat] by arith
from prime_factor_nat [OF f1]
- obtain p where "prime p" and "p dvd fact n + 1" by auto
+ obtain p :: nat where "prime p" and "p dvd fact n + 1" by auto
then have "p \<le> fact n + 1" apply (intro dvd_imp_le) apply auto done
{ assume "p \<le> n"
from \<open>prime p\<close> have "p \<ge> 1"
@@ -238,7 +274,7 @@
then have "p dvd 1" by simp
then have "p <= 1" by auto
moreover from \<open>prime p\<close> have "p > 1"
- using prime_def by blast
+ using is_prime_nat_iff by blast
ultimately have False by auto}
then have "n < p" by presburger
with \<open>prime p\<close> and \<open>p <= fact n + 1\<close> show ?thesis by auto
@@ -269,7 +305,7 @@
proof -
from assms have
"1 < p * q" and P: "\<And>m. m dvd p * q \<Longrightarrow> m = 1 \<or> m = p * q"
- unfolding prime_def by auto
+ unfolding is_prime_nat_iff by auto
from \<open>1 < p * q\<close> have "p \<noteq> 0" by (cases p) auto
then have Q: "p = p * q \<longleftrightarrow> q = 1" by auto
have "p dvd p * q" by simp
@@ -277,30 +313,8 @@
then show ?thesis by (simp add: Q)
qed
-lemma prime_exp:
- fixes p::nat
- shows "prime (p^n) \<longleftrightarrow> prime p \<and> n = 1"
-proof(induct n)
- case 0 thus ?case by simp
-next
- case (Suc n)
- {assume "p = 0" hence ?case by simp}
- moreover
- {assume "p=1" hence ?case by simp}
- moreover
- {assume p: "p \<noteq> 0" "p\<noteq>1"
- {assume pp: "prime (p^Suc n)"
- hence "p = 1 \<or> p^n = 1" using prime_product[of p "p^n"] by simp
- with p have n: "n = 0"
- by (metis One_nat_def nat_power_eq_Suc_0_iff)
- with pp have "prime p \<and> Suc n = 1" by simp}
- moreover
- {assume n: "prime p \<and> Suc n = 1" hence "prime (p^Suc n)" by simp}
- ultimately have ?case by blast}
- ultimately show ?case by blast
-qed
-
-lemma prime_power_mult:
+(* TODO: Generalise? *)
+lemma prime_power_mult_nat:
fixes p::nat
assumes p: "prime p" and xy: "x * y = p ^ k"
shows "\<exists>i j. x = p ^i \<and> y = p^ j"
@@ -310,7 +324,7 @@
next
case (Suc k x y)
from Suc.prems have pxy: "p dvd x*y" by auto
- from Primes.prime_dvd_mult_nat [OF p pxy] have pxyc: "p dvd x \<or> p dvd y" .
+ from is_prime_dvd_multD [OF p pxy] have pxyc: "p dvd x \<or> p dvd y" .
from p have p0: "p \<noteq> 0" by - (rule ccontr, simp)
{assume px: "p dvd x"
then obtain d where d: "x = p*d" unfolding dvd_def by blast
@@ -330,7 +344,7 @@
ultimately show ?case using pxyc by blast
qed
-lemma prime_power_exp:
+lemma prime_power_exp_nat:
fixes p::nat
assumes p: "prime p" and n: "n \<noteq> 0"
and xn: "x^n = p^k" shows "\<exists>i. x = p^i"
@@ -342,20 +356,20 @@
{assume "n = 0" with Suc have ?case by simp (rule exI[where x="k"], simp)}
moreover
{assume n: "n \<noteq> 0"
- from prime_power_mult[OF p th]
+ from prime_power_mult_nat[OF p th]
obtain i j where ij: "x = p^i" "x^n = p^j"by blast
from Suc.hyps[OF n ij(2)] have ?case .}
ultimately show ?case by blast
qed
-lemma divides_primepow:
+lemma divides_primepow_nat:
fixes p::nat
assumes p: "prime p"
shows "d dvd p^k \<longleftrightarrow> (\<exists> i. i \<le> k \<and> d = p ^i)"
proof
assume H: "d dvd p^k" then obtain e where e: "d*e = p^k"
unfolding dvd_def apply (auto simp add: mult.commute) by blast
- from prime_power_mult[OF p e] obtain i j where ij: "d = p^i" "e=p^j" by blast
+ from prime_power_mult_nat[OF p e] obtain i j where ij: "d = p^i" "e=p^j" by blast
from e ij have "p^(i + j) = p^k" by (simp add: power_add)
hence "i + j = k" using p prime_gt_1_nat power_inject_exp[of p "i+j" k] by simp
hence "i \<le> k" by arith
@@ -369,6 +383,7 @@
thus "\<exists>i\<le>k. d = p ^ i \<Longrightarrow> d dvd p ^ k" by blast
qed
+
subsection \<open>Chinese Remainder Theorem Variants\<close>
lemma bezout_gcd_nat:
@@ -392,6 +407,7 @@
text \<open>A binary form of the Chinese Remainder Theorem.\<close>
+(* TODO: Generalise? *)
lemma chinese_remainder:
fixes a::nat assumes ab: "coprime a b" and a: "a \<noteq> 0" and b: "b \<noteq> 0"
shows "\<exists>x q1 q2. x = u + q1 * a \<and> x = v + q2 * b"
@@ -422,11 +438,175 @@
shows "\<exists>x y. a*x = Suc (p*y)"
proof -
have ap: "coprime a p"
- by (metis gcd.commute p pa prime_imp_coprime_nat)
+ by (metis gcd.commute p pa is_prime_imp_coprime)
moreover from p have "p \<noteq> 1" by auto
ultimately have "\<exists>x y. a * x = p * y + 1"
by (rule coprime_bezout_strong)
then show ?thesis by simp
qed
+(* END TODO *)
-end
+
+
+subsection \<open>Multiplicity and primality for natural numbers and integers\<close>
+
+lemma prime_factors_gt_0_nat:
+ "p \<in> prime_factors x \<Longrightarrow> p > (0::nat)"
+ by (simp add: prime_factors_prime prime_gt_0_nat)
+
+lemma prime_factors_gt_0_int:
+ "p \<in> prime_factors x \<Longrightarrow> p > (0::int)"
+ by (simp add: prime_factors_prime prime_gt_0_int)
+
+lemma prime_factors_ge_0_int [elim]:
+ fixes n :: int
+ shows "p \<in> prime_factors n \<Longrightarrow> p \<ge> 0"
+ unfolding prime_factors_def
+ by (auto split: if_splits simp: is_prime_def dest!: in_prime_factorization_imp_prime)
+
+lemma msetprod_prime_factorization_int:
+ fixes n :: int
+ assumes "n > 0"
+ shows "msetprod (prime_factorization n) = n"
+ using assms by (simp add: msetprod_prime_factorization)
+
+lemma prime_factorization_exists_nat:
+ "n > 0 \<Longrightarrow> (\<exists>M. (\<forall>p::nat \<in> set_mset M. prime p) \<and> n = (\<Prod>i \<in># M. i))"
+ using prime_factorization_exists[of n] by (auto simp: is_prime_def)
+
+lemma msetprod_prime_factorization_nat [simp]:
+ "(n::nat) > 0 \<Longrightarrow> msetprod (prime_factorization n) = n"
+ by (subst msetprod_prime_factorization) simp_all
+
+lemma prime_factorization_nat:
+ "n > (0::nat) \<Longrightarrow> n = (\<Prod>p \<in> prime_factors n. p ^ multiplicity p n)"
+ by (simp add: setprod_prime_factors)
+
+lemma prime_factorization_int:
+ "n > (0::int) \<Longrightarrow> n = (\<Prod>p \<in> prime_factors n. p ^ multiplicity p n)"
+ by (simp add: setprod_prime_factors)
+
+lemma prime_factorization_unique_nat:
+ fixes f :: "nat \<Rightarrow> _"
+ assumes S_eq: "S = {p. 0 < f p}"
+ and "finite S"
+ and S: "\<forall>p\<in>S. prime p" "n = (\<Prod>p\<in>S. p ^ f p)"
+ shows "S = prime_factors n \<and> (\<forall>p. is_prime p \<longrightarrow> f p = multiplicity p n)"
+ using assms by (intro prime_factorization_unique'') auto
+
+lemma prime_factorization_unique_int:
+ fixes f :: "int \<Rightarrow> _"
+ assumes S_eq: "S = {p. 0 < f p}"
+ and "finite S"
+ and S: "\<forall>p\<in>S. prime p" "abs n = (\<Prod>p\<in>S. p ^ f p)"
+ shows "S = prime_factors n \<and> (\<forall>p. is_prime p \<longrightarrow> f p = multiplicity p n)"
+ using assms by (intro prime_factorization_unique'') auto
+
+lemma prime_factors_characterization_nat:
+ "S = {p. 0 < f (p::nat)} \<Longrightarrow>
+ finite S \<Longrightarrow> \<forall>p\<in>S. prime p \<Longrightarrow> n = (\<Prod>p\<in>S. p ^ f p) \<Longrightarrow> prime_factors n = S"
+ by (rule prime_factorization_unique_nat [THEN conjunct1, symmetric])
+
+lemma prime_factors_characterization'_nat:
+ "finite {p. 0 < f (p::nat)} \<Longrightarrow>
+ (\<forall>p. 0 < f p \<longrightarrow> prime p) \<Longrightarrow>
+ prime_factors (\<Prod>p | 0 < f p. p ^ f p) = {p. 0 < f p}"
+ by (rule prime_factors_characterization_nat) auto
+
+lemma prime_factors_characterization_int:
+ "S = {p. 0 < f (p::int)} \<Longrightarrow> finite S \<Longrightarrow>
+ \<forall>p\<in>S. prime p \<Longrightarrow> abs n = (\<Prod>p\<in>S. p ^ f p) \<Longrightarrow> prime_factors n = S"
+ by (rule prime_factorization_unique_int [THEN conjunct1, symmetric])
+
+(* TODO Move *)
+lemma abs_setprod: "abs (setprod f A :: 'a :: linordered_idom) = setprod (\<lambda>x. abs (f x)) A"
+ by (cases "finite A", induction A rule: finite_induct) (simp_all add: abs_mult)
+
+lemma primes_characterization'_int [rule_format]:
+ "finite {p. p \<ge> 0 \<and> 0 < f (p::int)} \<Longrightarrow> \<forall>p. 0 < f p \<longrightarrow> prime p \<Longrightarrow>
+ prime_factors (\<Prod>p | p \<ge> 0 \<and> 0 < f p. p ^ f p) = {p. p \<ge> 0 \<and> 0 < f p}"
+ by (rule prime_factors_characterization_int) (auto simp: abs_setprod prime_ge_0_int)
+
+lemma multiplicity_characterization_nat:
+ "S = {p. 0 < f (p::nat)} \<Longrightarrow> 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"
+ by (frule prime_factorization_unique_nat [of S f n, THEN conjunct2, rule_format, symmetric]) auto
+
+lemma multiplicity_characterization'_nat: "finite {p. 0 < f (p::nat)} \<longrightarrow>
+ (\<forall>p. 0 < f p \<longrightarrow> prime p) \<longrightarrow> is_prime p \<longrightarrow>
+ multiplicity p (\<Prod>p | 0 < f p. p ^ f p) = f p"
+ by (intro impI, rule multiplicity_characterization_nat) auto
+
+lemma multiplicity_characterization_int: "S = {p. 0 < f (p::int)} \<Longrightarrow>
+ 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"
+ by (frule prime_factorization_unique_int [of S f n, THEN conjunct2, rule_format, symmetric])
+ (auto simp: abs_setprod power_abs prime_ge_0_int intro!: setprod.cong)
+
+lemma multiplicity_characterization'_int [rule_format]:
+ "finite {p. p \<ge> 0 \<and> 0 < f (p::int)} \<Longrightarrow>
+ (\<forall>p. 0 < f p \<longrightarrow> prime p) \<Longrightarrow> is_prime p \<Longrightarrow>
+ multiplicity p (\<Prod>p | p \<ge> 0 \<and> 0 < f p. p ^ f p) = f p"
+ by (rule multiplicity_characterization_int) (auto simp: prime_ge_0_int)
+
+lemma multiplicity_one_nat [simp]: "multiplicity p (Suc 0) = 0"
+ unfolding One_nat_def [symmetric] by (rule multiplicity_one)
+
+lemma multiplicity_eq_nat:
+ fixes x and y::nat
+ assumes "x > 0" "y > 0" "\<And>p. is_prime p \<Longrightarrow> multiplicity p x = multiplicity p y"
+ shows "x = y"
+ using multiplicity_eq_imp_eq[of x y] assms by simp
+
+lemma multiplicity_eq_int:
+ fixes x y :: int
+ assumes "x > 0" "y > 0" "\<And>p. is_prime p \<Longrightarrow> multiplicity p x = multiplicity p y"
+ shows "x = y"
+ using multiplicity_eq_imp_eq[of x y] assms by simp
+
+lemma multiplicity_prod_prime_powers:
+ assumes "finite S" "\<And>x. x \<in> S \<Longrightarrow> is_prime x" "is_prime p"
+ shows "multiplicity p (\<Prod>p \<in> S. p ^ f p) = (if p \<in> S then f p else 0)"
+proof -
+ define g where "g = (\<lambda>x. if x \<in> S then f x else 0)"
+ define A where "A = Abs_multiset g"
+ have "{x. g x > 0} \<subseteq> S" by (auto simp: g_def)
+ from finite_subset[OF this assms(1)] have [simp]: "g : multiset"
+ by (simp add: multiset_def)
+ from assms have count_A: "count A x = g x" for x unfolding A_def
+ by simp
+ have set_mset_A: "set_mset A = {x\<in>S. f x > 0}"
+ unfolding set_mset_def count_A by (auto simp: g_def)
+ with assms have prime: "prime x" if "x \<in># A" for x using that by auto
+ from set_mset_A assms have "(\<Prod>p \<in> S. p ^ f p) = (\<Prod>p \<in> S. p ^ g p) "
+ by (intro setprod.cong) (auto simp: g_def)
+ also from set_mset_A assms have "\<dots> = (\<Prod>p \<in> set_mset A. p ^ g p)"
+ by (intro setprod.mono_neutral_right) (auto simp: g_def set_mset_A)
+ also have "\<dots> = msetprod A"
+ by (auto simp: msetprod_multiplicity count_A set_mset_A intro!: setprod.cong)
+ also from assms have "multiplicity p \<dots> = msetsum (image_mset (multiplicity p) A)"
+ by (subst prime_multiplicity_msetprod_distrib) (auto dest: prime)
+ also from assms have "image_mset (multiplicity p) A = image_mset (\<lambda>x. if x = p then 1 else 0) A"
+ by (intro image_mset_cong) (auto simp: prime_multiplicity_other dest: prime)
+ also have "msetsum \<dots> = (if p \<in> S then f p else 0)" by (simp add: msetsum_delta count_A g_def)
+ finally show ?thesis .
+qed
+
+(* TODO Legacy names *)
+lemmas prime_imp_coprime_nat = is_prime_imp_coprime[where ?'a = nat]
+lemmas prime_imp_coprime_int = is_prime_imp_coprime[where ?'a = int]
+lemmas prime_dvd_mult_nat = is_prime_dvd_mult_iff[where ?'a = nat]
+lemmas prime_dvd_mult_int = is_prime_dvd_mult_iff[where ?'a = int]
+lemmas prime_dvd_mult_eq_nat = is_prime_dvd_mult_iff[where ?'a = nat]
+lemmas prime_dvd_mult_eq_int = is_prime_dvd_mult_iff[where ?'a = int]
+lemmas prime_dvd_power_nat = is_prime_dvd_power[where ?'a = nat]
+lemmas prime_dvd_power_int = is_prime_dvd_power[where ?'a = int]
+lemmas prime_dvd_power_nat_iff = is_prime_dvd_power_iff[where ?'a = nat]
+lemmas prime_dvd_power_int_iff = is_prime_dvd_power_iff[where ?'a = int]
+lemmas prime_imp_power_coprime_nat = is_prime_imp_power_coprime[where ?'a = nat]
+lemmas prime_imp_power_coprime_int = is_prime_imp_power_coprime[where ?'a = int]
+lemmas primes_coprime_nat = primes_coprime[where ?'a = nat]
+lemmas primes_coprime_int = primes_coprime[where ?'a = nat]
+lemmas prime_divprod_pow_nat = prime_divprod_pow[where ?'a = nat]
+lemmas prime_exp = is_prime_elem_power_iff[where ?'a = nat]
+
+end
\ No newline at end of file
--- a/src/HOL/Number_Theory/Residues.thy Wed Jul 20 14:52:09 2016 +0200
+++ b/src/HOL/Number_Theory/Residues.thy Thu Jul 21 10:06:04 2016 +0200
@@ -202,9 +202,9 @@
subsection \<open>Prime residues\<close>
locale residues_prime =
- fixes p and R (structure)
+ fixes p :: nat and R (structure)
assumes p_prime [intro]: "prime p"
- defines "R \<equiv> residue_ring p"
+ defines "R \<equiv> residue_ring (int p)"
sublocale residues_prime < residues p
apply (unfold R_def residues_def)
@@ -223,7 +223,7 @@
apply (erule notE)
apply (subst gcd.commute)
apply (rule prime_imp_coprime_int)
- apply (rule p_prime)
+ apply (simp add: p_prime)
apply (rule notI)
apply (frule zdvd_imp_le)
apply auto
@@ -280,7 +280,7 @@
qed
then show ?thesis
using \<open>2 \<le> p\<close>
- by (simp add: prime_def)
+ by (simp add: is_prime_nat_iff)
(metis One_nat_def dvd_pos_nat nat_dvd_not_less nat_neq_iff not_gr0
not_numeral_le_zero one_dvd)
qed
@@ -347,19 +347,21 @@
apply auto
done
-lemma phi_prime: "prime p \<Longrightarrow> phi p = nat p - 1"
+lemma phi_prime: "prime (int p) \<Longrightarrow> phi p = nat p - 1"
apply (rule residues_prime.phi_prime)
+ apply simp
apply (erule residues_prime.intro)
done
lemma fermat_theorem:
fixes a :: int
- assumes "prime p"
+ assumes "prime (int p)"
and "\<not> p dvd a"
shows "[a^(p - 1) = 1] (mod p)"
proof -
from assms have "[a ^ phi p = 1] (mod p)"
- by (auto intro!: euler_theorem dest!: prime_imp_coprime_int simp add: ac_simps)
+ by (auto intro!: euler_theorem intro!: prime_imp_coprime_int[of p]
+ simp: gcd.commute[of _ "int p"])
also have "phi p = nat p - 1"
by (rule phi_prime) (rule assms)
finally show ?thesis
@@ -367,7 +369,7 @@
qed
lemma fermat_theorem_nat:
- assumes "prime p" and "\<not> p dvd a"
+ assumes "prime (int p)" and "\<not> p dvd a"
shows "[a ^ (p - 1) = 1] (mod p)"
using fermat_theorem [of p a] assms
by (metis of_nat_1 of_nat_power transfer_int_nat_cong zdvd_int)
--- a/src/HOL/Number_Theory/UniqueFactorization.thy Wed Jul 20 14:52:09 2016 +0200
+++ b/src/HOL/Number_Theory/UniqueFactorization.thy Thu Jul 21 10:06:04 2016 +0200
@@ -12,817 +12,4 @@
imports Cong "~~/src/HOL/Library/Multiset"
begin
-(* As a simp or intro rule,
-
- prime p \<Longrightarrow> p > 0
-
- wreaks havoc here. When the premise includes \<forall>x \<in># M. prime x, it
- leads to the backchaining
-
- x > 0
- prime x
- x \<in># M which is, unfortunately,
- count M x > 0
-*)
-
-(* Here is a version of set product for multisets. Is it worth moving
- to multiset.thy? If so, one should similarly define msetsum for abelian
- semirings, using of_nat. Also, is it worth developing bounded quantifiers
- "\<forall>i \<in># M. P i"?
-*)
-
-
-subsection \<open>Unique factorization: multiset version\<close>
-
-lemma multiset_prime_factorization_exists:
- "n > 0 \<Longrightarrow> (\<exists>M. (\<forall>p::nat \<in> set_mset M. prime p) \<and> n = (\<Prod>i \<in># M. i))"
-proof (induct n rule: nat_less_induct)
- fix n :: nat
- 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))"
- assume "n > 0"
- then consider "n = 1" | "n > 1" "prime n" | "n > 1" "\<not> prime n"
- by arith
- then show "\<exists>M. (\<forall>p \<in> set_mset M. prime p) \<and> n = (\<Prod>i\<in>#M. i)"
- proof cases
- case 1
- then have "(\<forall>p\<in>set_mset {#}. prime p) \<and> n = (\<Prod>i \<in># {#}. i)"
- by auto
- then show ?thesis ..
- next
- case 2
- then have "(\<forall>p\<in>set_mset {#n#}. prime p) \<and> n = (\<Prod>i \<in># {#n#}. i)"
- by auto
- then show ?thesis ..
- next
- case 3
- with not_prime_eq_prod_nat
- obtain m k where n: "n = m * k" "1 < m" "m < n" "1 < k" "k < n"
- by blast
- with ih obtain Q R where "(\<forall>p \<in> set_mset Q. prime p) \<and> m = (\<Prod>i\<in>#Q. i)"
- and "(\<forall>p\<in>set_mset R. prime p) \<and> k = (\<Prod>i\<in>#R. i)"
- by blast
- then have "(\<forall>p\<in>set_mset (Q + R). prime p) \<and> n = (\<Prod>i \<in># Q + R. i)"
- by (auto simp add: n msetprod_Un)
- then show ?thesis ..
- qed
-qed
-
-lemma multiset_prime_factorization_unique_aux:
- fixes a :: nat
- assumes "\<forall>p\<in>set_mset M. prime p"
- and "\<forall>p\<in>set_mset N. prime p"
- and "(\<Prod>i \<in># M. i) dvd (\<Prod>i \<in># N. i)"
- shows "count M a \<le> count N a"
-proof (cases "a \<in> set_mset M")
- case True
- with assms have a: "prime a"
- by auto
- with True have "a ^ count M a dvd (\<Prod>i \<in># M. i)"
- by (auto simp add: msetprod_multiplicity)
- also have "\<dots> dvd (\<Prod>i \<in># N. i)"
- by (rule assms)
- also have "\<dots> = (\<Prod>i \<in> set_mset N. i ^ count N i)"
- by (simp add: msetprod_multiplicity)
- also have "\<dots> = a ^ count N a * (\<Prod>i \<in> (set_mset N - {a}). i ^ count N i)"
- proof (cases "a \<in> set_mset N")
- case True
- then have b: "set_mset N = {a} \<union> (set_mset N - {a})"
- by auto
- then show ?thesis
- by (subst (1) b, subst setprod.union_disjoint, auto)
- next
- case False
- then show ?thesis
- by (auto simp add: not_in_iff)
- qed
- finally have "a ^ count M a dvd a ^ count N a * (\<Prod>i \<in> (set_mset N - {a}). i ^ count N i)" .
- moreover
- have "coprime (a ^ count M a) (\<Prod>i \<in> (set_mset N - {a}). i ^ count N i)"
- apply (subst gcd.commute)
- apply (rule setprod_coprime)
- apply (rule primes_imp_powers_coprime_nat)
- using assms True
- apply auto
- done
- ultimately have "a ^ count M a dvd a ^ count N a"
- by (elim coprime_dvd_mult)
- with a show ?thesis
- using power_dvd_imp_le prime_def by blast
-next
- case False
- then show ?thesis
- by (auto simp add: not_in_iff)
-qed
-
-lemma multiset_prime_factorization_unique:
- assumes "\<forall>p::nat \<in> set_mset M. prime p"
- and "\<forall>p \<in> set_mset N. prime p"
- and "(\<Prod>i \<in># M. i) = (\<Prod>i \<in># N. i)"
- shows "M = N"
-proof -
- have "count M a = count N a" for a
- proof -
- from assms have "count M a \<le> count N a"
- by (intro multiset_prime_factorization_unique_aux, auto)
- moreover from assms have "count N a \<le> count M a"
- by (intro multiset_prime_factorization_unique_aux, auto)
- ultimately show ?thesis
- by auto
- qed
- then show ?thesis
- by (simp add: multiset_eq_iff)
-qed
-
-definition multiset_prime_factorization :: "nat \<Rightarrow> nat multiset"
-where
- "multiset_prime_factorization n =
- (if n > 0
- then THE M. (\<forall>p \<in> set_mset M. prime p) \<and> n = (\<Prod>i \<in># M. i)
- else {#})"
-
-lemma multiset_prime_factorization: "n > 0 \<Longrightarrow>
- (\<forall>p \<in> set_mset (multiset_prime_factorization n). prime p) \<and>
- n = (\<Prod>i \<in># (multiset_prime_factorization n). i)"
- apply (unfold multiset_prime_factorization_def)
- apply clarsimp
- apply (frule multiset_prime_factorization_exists)
- apply clarify
- apply (rule theI)
- apply (insert multiset_prime_factorization_unique)
- apply auto
- done
-
-
-subsection \<open>Prime factors and multiplicity for nat and int\<close>
-
-class unique_factorization =
- fixes multiplicity :: "'a \<Rightarrow> 'a \<Rightarrow> nat"
- and prime_factors :: "'a \<Rightarrow> 'a set"
-
-text \<open>Definitions for the natural numbers.\<close>
-instantiation nat :: unique_factorization
-begin
-
-definition multiplicity_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
- where "multiplicity_nat p n = count (multiset_prime_factorization n) p"
-
-definition prime_factors_nat :: "nat \<Rightarrow> nat set"
- where "prime_factors_nat n = set_mset (multiset_prime_factorization n)"
-
-instance ..
-
end
-
-text \<open>Definitions for the integers.\<close>
-instantiation int :: unique_factorization
-begin
-
-definition multiplicity_int :: "int \<Rightarrow> int \<Rightarrow> nat"
- where "multiplicity_int p n = multiplicity (nat p) (nat n)"
-
-definition prime_factors_int :: "int \<Rightarrow> int set"
- where "prime_factors_int n = int ` (prime_factors (nat n))"
-
-instance ..
-
-end
-
-
-subsection \<open>Set up transfer\<close>
-
-lemma transfer_nat_int_prime_factors: "prime_factors (nat n) = nat ` prime_factors n"
- unfolding prime_factors_int_def
- apply auto
- apply (subst transfer_int_nat_set_return_embed)
- apply assumption
- done
-
-lemma transfer_nat_int_prime_factors_closure: "n \<ge> 0 \<Longrightarrow> nat_set (prime_factors n)"
- by (auto simp add: nat_set_def prime_factors_int_def)
-
-lemma transfer_nat_int_multiplicity:
- "p \<ge> 0 \<Longrightarrow> n \<ge> 0 \<Longrightarrow> multiplicity (nat p) (nat n) = multiplicity p n"
- by (auto simp add: multiplicity_int_def)
-
-declare transfer_morphism_nat_int[transfer add return:
- transfer_nat_int_prime_factors transfer_nat_int_prime_factors_closure
- transfer_nat_int_multiplicity]
-
-lemma transfer_int_nat_prime_factors: "prime_factors (int n) = int ` prime_factors n"
- unfolding prime_factors_int_def by auto
-
-lemma transfer_int_nat_prime_factors_closure: "is_nat n \<Longrightarrow> nat_set (prime_factors n)"
- by (simp only: transfer_nat_int_prime_factors_closure is_nat_def)
-
-lemma transfer_int_nat_multiplicity: "multiplicity (int p) (int n) = multiplicity p n"
- by (auto simp add: multiplicity_int_def)
-
-declare transfer_morphism_int_nat[transfer add return:
- transfer_int_nat_prime_factors transfer_int_nat_prime_factors_closure
- transfer_int_nat_multiplicity]
-
-
-subsection \<open>Properties of prime factors and multiplicity for nat and int\<close>
-
-lemma prime_factors_ge_0_int [elim]:
- fixes n :: int
- shows "p \<in> prime_factors n \<Longrightarrow> p \<ge> 0"
- unfolding prime_factors_int_def by auto
-
-lemma prime_factors_prime_nat [intro]:
- fixes n :: nat
- shows "p \<in> prime_factors n \<Longrightarrow> prime p"
- apply (cases "n = 0")
- apply (simp add: prime_factors_nat_def multiset_prime_factorization_def)
- apply (auto simp add: prime_factors_nat_def multiset_prime_factorization)
- done
-
-lemma prime_factors_prime_int [intro]:
- fixes n :: int
- assumes "n \<ge> 0" and "p \<in> prime_factors n"
- shows "prime p"
- apply (rule prime_factors_prime_nat [transferred, of n p, simplified])
- using assms apply auto
- done
-
-lemma prime_factors_gt_0_nat:
- fixes p :: nat
- shows "p \<in> prime_factors x \<Longrightarrow> p > 0"
- using prime_factors_prime_nat by force
-
-lemma prime_factors_gt_0_int:
- shows "x \<ge> 0 \<Longrightarrow> p \<in> prime_factors x \<Longrightarrow> int p > (0::int)"
- by (simp add: prime_factors_gt_0_nat)
-
-lemma prime_factors_finite_nat [iff]:
- fixes n :: nat
- shows "finite (prime_factors n)"
- unfolding prime_factors_nat_def by auto
-
-lemma prime_factors_finite_int [iff]:
- fixes n :: int
- shows "finite (prime_factors n)"
- unfolding prime_factors_int_def by auto
-
-lemma prime_factors_altdef_nat:
- fixes n :: nat
- shows "prime_factors n = {p. multiplicity p n > 0}"
- by (force simp add: prime_factors_nat_def multiplicity_nat_def)
-
-lemma prime_factors_altdef_int:
- fixes n :: int
- shows "prime_factors n = {p. p \<ge> 0 \<and> multiplicity p n > 0}"
- apply (unfold prime_factors_int_def multiplicity_int_def)
- apply (subst prime_factors_altdef_nat)
- apply (auto simp add: image_def)
- done
-
-lemma prime_factorization_nat:
- fixes n :: nat
- shows "n > 0 \<Longrightarrow> n = (\<Prod>p \<in> prime_factors n. p ^ multiplicity p n)"
- apply (frule multiset_prime_factorization)
- apply (simp add: prime_factors_nat_def multiplicity_nat_def msetprod_multiplicity)
- done
-
-lemma prime_factorization_int:
- fixes n :: int
- assumes "n > 0"
- shows "n = (\<Prod>p \<in> prime_factors n. p ^ multiplicity p n)"
- apply (rule prime_factorization_nat [transferred, of n])
- using assms apply auto
- done
-
-lemma prime_factorization_unique_nat:
- fixes f :: "nat \<Rightarrow> _"
- assumes S_eq: "S = {p. 0 < f p}"
- and "finite S"
- and S: "\<forall>p\<in>S. prime p" "n = (\<Prod>p\<in>S. p ^ f p)"
- shows "S = prime_factors n \<and> (\<forall>p. f p = multiplicity p n)"
-proof -
- from assms have "f \<in> multiset"
- by (auto simp add: multiset_def)
- moreover from assms have "n > 0"
- by (auto intro: prime_gt_0_nat)
- ultimately have "multiset_prime_factorization n = Abs_multiset f"
- apply (unfold multiset_prime_factorization_def)
- apply (subst if_P, assumption)
- apply (rule the1_equality)
- apply (rule ex_ex1I)
- apply (rule multiset_prime_factorization_exists, assumption)
- apply (rule multiset_prime_factorization_unique)
- apply force
- apply force
- apply force
- using S S_eq apply (simp add: set_mset_def msetprod_multiplicity)
- done
- with \<open>f \<in> multiset\<close> have "count (multiset_prime_factorization n) = f"
- by simp
- with S_eq show ?thesis
- by (simp add: set_mset_def multiset_def prime_factors_nat_def multiplicity_nat_def)
-qed
-
-lemma prime_factors_characterization_nat:
- "S = {p. 0 < f (p::nat)} \<Longrightarrow>
- finite S \<Longrightarrow> \<forall>p\<in>S. prime p \<Longrightarrow> n = (\<Prod>p\<in>S. p ^ f p) \<Longrightarrow> prime_factors n = S"
- by (rule prime_factorization_unique_nat [THEN conjunct1, symmetric])
-
-lemma prime_factors_characterization'_nat:
- "finite {p. 0 < f (p::nat)} \<Longrightarrow>
- (\<forall>p. 0 < f p \<longrightarrow> prime p) \<Longrightarrow>
- prime_factors (\<Prod>p | 0 < f p. p ^ f p) = {p. 0 < f p}"
- by (rule prime_factors_characterization_nat) auto
-
-(* A minor glitch:*)
-thm prime_factors_characterization'_nat
- [where f = "\<lambda>x. f (int (x::nat))",
- transferred direction: nat "op \<le> (0::int)", rule_format]
-
-(*
- Transfer isn't smart enough to know that the "0 < f p" should
- remain a comparison between nats. But the transfer still works.
-*)
-
-lemma primes_characterization'_int [rule_format]:
- "finite {p. p \<ge> 0 \<and> 0 < f (p::int)} \<Longrightarrow> \<forall>p. 0 < f p \<longrightarrow> prime p \<Longrightarrow>
- prime_factors (\<Prod>p | p \<ge> 0 \<and> 0 < f p. p ^ f p) = {p. p \<ge> 0 \<and> 0 < f p}"
- using prime_factors_characterization'_nat
- [where f = "\<lambda>x. f (int (x::nat))",
- transferred direction: nat "op \<le> (0::int)"]
- by auto
-
-lemma prime_factors_characterization_int:
- "S = {p. 0 < f (p::int)} \<Longrightarrow> finite S \<Longrightarrow>
- \<forall>p\<in>S. prime (nat p) \<Longrightarrow> n = (\<Prod>p\<in>S. p ^ f p) \<Longrightarrow> prime_factors n = S"
- apply simp
- apply (subgoal_tac "{p. 0 < f p} = {p. 0 \<le> p \<and> 0 < f p}")
- apply (simp only:)
- apply (subst primes_characterization'_int)
- apply simp_all
- apply (metis nat_int)
- apply (metis le_cases nat_le_0 zero_not_prime_nat)
- done
-
-lemma multiplicity_characterization_nat:
- "S = {p. 0 < f (p::nat)} \<Longrightarrow> finite S \<Longrightarrow> \<forall>p\<in>S. prime p \<Longrightarrow>
- n = (\<Prod>p\<in>S. p ^ f p) \<Longrightarrow> multiplicity p n = f p"
- apply (frule prime_factorization_unique_nat [THEN conjunct2, rule_format, symmetric])
- apply auto
- done
-
-lemma multiplicity_characterization'_nat: "finite {p. 0 < f (p::nat)} \<longrightarrow>
- (\<forall>p. 0 < f p \<longrightarrow> prime p) \<longrightarrow>
- multiplicity p (\<Prod>p | 0 < f p. p ^ f p) = f p"
- apply (intro impI)
- apply (rule multiplicity_characterization_nat)
- apply auto
- done
-
-lemma multiplicity_characterization'_int [rule_format]:
- "finite {p. p \<ge> 0 \<and> 0 < f (p::int)} \<Longrightarrow>
- (\<forall>p. 0 < f p \<longrightarrow> prime p) \<Longrightarrow> p \<ge> 0 \<Longrightarrow>
- multiplicity p (\<Prod>p | p \<ge> 0 \<and> 0 < f p. p ^ f p) = f p"
- apply (insert multiplicity_characterization'_nat
- [where f = "\<lambda>x. f (int (x::nat))",
- transferred direction: nat "op \<le> (0::int)", rule_format])
- apply auto
- done
-
-lemma multiplicity_characterization_int: "S = {p. 0 < f (p::int)} \<Longrightarrow>
- finite S \<Longrightarrow> \<forall>p\<in>S. prime (nat p) \<Longrightarrow> n = (\<Prod>p\<in>S. p ^ f p) \<Longrightarrow>
- p \<ge> 0 \<Longrightarrow> multiplicity p n = f p"
- apply simp
- apply (subgoal_tac "{p. 0 < f p} = {p. 0 \<le> p \<and> 0 < f p}")
- apply (simp only:)
- apply (subst multiplicity_characterization'_int)
- apply simp_all
- apply (metis nat_int)
- apply (metis le_cases nat_le_0 zero_not_prime_nat)
- done
-
-lemma multiplicity_zero_nat [simp]: "multiplicity (p::nat) 0 = 0"
- by (simp add: multiplicity_nat_def multiset_prime_factorization_def)
-
-lemma multiplicity_zero_int [simp]: "multiplicity (p::int) 0 = 0"
- by (simp add: multiplicity_int_def)
-
-lemma multiplicity_one_nat': "multiplicity p (1::nat) = 0"
- by (subst multiplicity_characterization_nat [where f = "\<lambda>x. 0"], auto)
-
-lemma multiplicity_one_nat [simp]: "multiplicity p (Suc 0) = 0"
- by (metis One_nat_def multiplicity_one_nat')
-
-lemma multiplicity_one_int [simp]: "multiplicity p (1::int) = 0"
- by (metis multiplicity_int_def multiplicity_one_nat' transfer_nat_int_numerals(2))
-
-lemma multiplicity_prime_nat [simp]: "prime p \<Longrightarrow> multiplicity p p = 1"
- apply (subst multiplicity_characterization_nat [where f = "\<lambda>q. if q = p then 1 else 0"])
- apply auto
- apply (metis (full_types) less_not_refl)
- done
-
-lemma multiplicity_prime_power_nat [simp]: "prime p \<Longrightarrow> multiplicity p (p ^ n) = n"
- apply (cases "n = 0")
- apply auto
- apply (subst multiplicity_characterization_nat [where f = "\<lambda>q. if q = p then n else 0"])
- apply auto
- apply (metis (full_types) less_not_refl)
- done
-
-lemma multiplicity_prime_power_int [simp]: "prime p \<Longrightarrow> multiplicity p (int p ^ n) = n"
- by (metis multiplicity_prime_power_nat of_nat_power transfer_int_nat_multiplicity)
-
-lemma multiplicity_nonprime_nat [simp]:
- fixes p n :: nat
- shows "\<not> prime p \<Longrightarrow> multiplicity p n = 0"
- apply (cases "n = 0")
- apply auto
- apply (frule multiset_prime_factorization)
- apply (auto simp add: multiplicity_nat_def count_eq_zero_iff)
- done
-
-lemma multiplicity_not_factor_nat [simp]:
- fixes p n :: nat
- shows "p \<notin> prime_factors n \<Longrightarrow> multiplicity p n = 0"
- apply (subst (asm) prime_factors_altdef_nat)
- apply auto
- done
-
-lemma multiplicity_not_factor_int [simp]:
- fixes n :: int
- shows "p \<ge> 0 \<Longrightarrow> p \<notin> prime_factors n \<Longrightarrow> multiplicity p n = 0"
- apply (subst (asm) prime_factors_altdef_int)
- apply auto
- done
-
-(*FIXME: messy*)
-lemma multiplicity_product_aux_nat: "(k::nat) > 0 \<Longrightarrow> l > 0 \<Longrightarrow>
- (prime_factors k) \<union> (prime_factors l) = prime_factors (k * l) \<and>
- (\<forall>p. multiplicity p k + multiplicity p l = multiplicity p (k * l))"
- apply (rule prime_factorization_unique_nat)
- apply (simp only: prime_factors_altdef_nat)
- apply auto
- apply (subst power_add)
- apply (subst setprod.distrib)
- apply (rule arg_cong2 [where f = "\<lambda>x y. x*y"])
- apply (subgoal_tac "prime_factors k \<union> prime_factors l = prime_factors k \<union>
- (prime_factors l - prime_factors k)")
- apply (erule ssubst)
- apply (subst setprod.union_disjoint)
- apply auto
- apply (metis One_nat_def nat_mult_1_right prime_factorization_nat setprod.neutral_const)
- apply (subgoal_tac "prime_factors k \<union> prime_factors l = prime_factors l \<union>
- (prime_factors k - prime_factors l)")
- apply (erule ssubst)
- apply (subst setprod.union_disjoint)
- apply auto
- apply (subgoal_tac "(\<Prod>p\<in>prime_factors k - prime_factors l. p ^ multiplicity p l) =
- (\<Prod>p\<in>prime_factors k - prime_factors l. 1)")
- apply auto
- apply (metis One_nat_def nat_mult_1_right prime_factorization_nat setprod.neutral_const)
- done
-
-(* transfer doesn't have the same problem here with the right
- choice of rules. *)
-
-lemma multiplicity_product_aux_int:
- assumes "(k::int) > 0" and "l > 0"
- shows "prime_factors k \<union> prime_factors l = prime_factors (k * l) \<and>
- (\<forall>p \<ge> 0. multiplicity p k + multiplicity p l = multiplicity p (k * l))"
- apply (rule multiplicity_product_aux_nat [transferred, of l k])
- using assms apply auto
- done
-
-lemma prime_factors_product_nat: "(k::nat) > 0 \<Longrightarrow> l > 0 \<Longrightarrow> prime_factors (k * l) =
- prime_factors k \<union> prime_factors l"
- by (rule multiplicity_product_aux_nat [THEN conjunct1, symmetric])
-
-lemma prime_factors_product_int: "(k::int) > 0 \<Longrightarrow> l > 0 \<Longrightarrow> prime_factors (k * l) =
- prime_factors k \<union> prime_factors l"
- by (rule multiplicity_product_aux_int [THEN conjunct1, symmetric])
-
-lemma multiplicity_product_nat: "(k::nat) > 0 \<Longrightarrow> l > 0 \<Longrightarrow> multiplicity p (k * l) =
- multiplicity p k + multiplicity p l"
- by (rule multiplicity_product_aux_nat [THEN conjunct2, rule_format, symmetric])
-
-lemma multiplicity_product_int: "(k::int) > 0 \<Longrightarrow> l > 0 \<Longrightarrow> p \<ge> 0 \<Longrightarrow>
- multiplicity p (k * l) = multiplicity p k + multiplicity p l"
- by (rule multiplicity_product_aux_int [THEN conjunct2, rule_format, symmetric])
-
-lemma multiplicity_setprod_nat: "finite S \<Longrightarrow> \<forall>x\<in>S. f x > 0 \<Longrightarrow>
- multiplicity (p::nat) (\<Prod>x \<in> S. f x) = (\<Sum>x \<in> S. multiplicity p (f x))"
- apply (induct set: finite)
- apply auto
- apply (subst multiplicity_product_nat)
- apply auto
- done
-
-(* Transfer is delicate here for two reasons: first, because there is
- an implicit quantifier over functions (f), and, second, because the
- product over the multiplicity should not be translated to an integer
- product.
-
- The way to handle the first is to use quantifier rules for functions.
- The way to handle the second is to turn off the offending rule.
-*)
-
-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"
- apply (rule setsum_nonneg; auto)
- apply (rule setprod_nonneg; auto)
- done
-
-declare transfer_morphism_nat_int[transfer
- add return: transfer_nat_int_sum_prod_closure3
- del: transfer_nat_int_sum_prod2 (1)]
-
-lemma multiplicity_setprod_int: "p \<ge> 0 \<Longrightarrow> finite S \<Longrightarrow> \<forall>x\<in>S. f x > 0 \<Longrightarrow>
- multiplicity (p::int) (\<Prod>x \<in> S. f x) = (\<Sum>x \<in> S. multiplicity p (f x))"
- apply (frule multiplicity_setprod_nat
- [where f = "\<lambda>x. nat(int(nat(f x)))",
- transferred direction: nat "op \<le> (0::int)"])
- apply auto
- apply (subst (asm) setprod.cong)
- apply (rule refl)
- apply (rule if_P)
- apply auto
- apply (rule setsum.cong)
- apply auto
- done
-
-declare transfer_morphism_nat_int[transfer
- add return: transfer_nat_int_sum_prod2 (1)]
-
-lemma multiplicity_prod_prime_powers_nat:
- "finite S \<Longrightarrow> \<forall>p\<in>S. prime (p::nat) \<Longrightarrow>
- multiplicity p (\<Prod>p \<in> S. p ^ f p) = (if p \<in> S then f p else 0)"
- 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)")
- apply (erule ssubst)
- apply (subst multiplicity_characterization_nat)
- prefer 5 apply (rule refl)
- apply (rule refl)
- apply auto
- apply (subst setprod.mono_neutral_right)
- apply assumption
- prefer 3
- apply (rule setprod.cong)
- apply (rule refl)
- apply auto
- done
-
-(* Here the issue with transfer is the implicit quantifier over S *)
-
-lemma multiplicity_prod_prime_powers_int:
- "(p::int) \<ge> 0 \<Longrightarrow> finite S \<Longrightarrow> \<forall>p\<in>S. prime (nat p) \<Longrightarrow>
- multiplicity p (\<Prod>p \<in> S. p ^ f p) = (if p \<in> S then f p else 0)"
- apply (subgoal_tac "int ` nat ` S = S")
- apply (frule multiplicity_prod_prime_powers_nat
- [where f = "\<lambda>x. f(int x)" and S = "nat ` S", transferred])
- apply auto
- apply (metis linear nat_0_iff zero_not_prime_nat)
- apply (metis (full_types) image_iff int_nat_eq less_le less_linear nat_0_iff zero_not_prime_nat)
- done
-
-lemma multiplicity_distinct_prime_power_nat:
- "prime p \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> multiplicity p (q ^ n) = 0"
- apply (subgoal_tac "q ^ n = setprod (\<lambda>x. x ^ n) {q}")
- apply (erule ssubst)
- apply (subst multiplicity_prod_prime_powers_nat)
- apply auto
- done
-
-lemma multiplicity_distinct_prime_power_int:
- "prime p \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> multiplicity p (int q ^ n) = 0"
- by (metis multiplicity_distinct_prime_power_nat of_nat_power transfer_int_nat_multiplicity)
-
-lemma dvd_multiplicity_nat:
- fixes x y :: nat
- shows "0 < y \<Longrightarrow> x dvd y \<Longrightarrow> multiplicity p x \<le> multiplicity p y"
- apply (cases "x = 0")
- apply (auto simp add: dvd_def multiplicity_product_nat)
- done
-
-lemma dvd_multiplicity_int:
- fixes p x y :: int
- shows "0 < y \<Longrightarrow> 0 \<le> x \<Longrightarrow> x dvd y \<Longrightarrow> p \<ge> 0 \<Longrightarrow> multiplicity p x \<le> multiplicity p y"
- apply (cases "x = 0")
- apply (auto simp add: dvd_def)
- apply (subgoal_tac "0 < k")
- apply (auto simp add: multiplicity_product_int)
- apply (erule zero_less_mult_pos)
- apply arith
- done
-
-lemma dvd_prime_factors_nat [intro]:
- fixes x y :: nat
- shows "0 < y \<Longrightarrow> x dvd y \<Longrightarrow> prime_factors x \<le> prime_factors y"
- apply (simp only: prime_factors_altdef_nat)
- apply auto
- apply (metis dvd_multiplicity_nat le_0_eq neq0_conv)
- done
-
-lemma dvd_prime_factors_int [intro]:
- fixes x y :: int
- shows "0 < y \<Longrightarrow> 0 \<le> x \<Longrightarrow> x dvd y \<Longrightarrow> prime_factors x \<le> prime_factors y"
- apply (auto simp add: prime_factors_altdef_int)
- apply (metis dvd_multiplicity_int le_0_eq neq0_conv)
- done
-
-lemma multiplicity_dvd_nat:
- fixes x y :: nat
- shows "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> \<forall>p. multiplicity p x \<le> multiplicity p y \<Longrightarrow> x dvd y"
- apply (subst prime_factorization_nat [of x], assumption)
- apply (subst prime_factorization_nat [of y], assumption)
- apply (rule setprod_dvd_setprod_subset2)
- apply force
- apply (subst prime_factors_altdef_nat)+
- apply auto
- apply (metis gr0I le_0_eq less_not_refl)
- apply (metis le_imp_power_dvd)
- done
-
-lemma multiplicity_dvd_int:
- fixes x y :: int
- shows "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> \<forall>p\<ge>0. multiplicity p x \<le> multiplicity p y \<Longrightarrow> x dvd y"
- apply (subst prime_factorization_int [of x], assumption)
- apply (subst prime_factorization_int [of y], assumption)
- apply (rule setprod_dvd_setprod_subset2)
- apply force
- apply (subst prime_factors_altdef_int)+
- apply auto
- apply (metis le_imp_power_dvd prime_factors_ge_0_int)
- done
-
-lemma multiplicity_dvd'_nat:
- fixes x y :: nat
- assumes "0 < x"
- assumes "\<forall>p. prime p \<longrightarrow> multiplicity p x \<le> multiplicity p y"
- shows "x dvd y"
- using dvd_0_right assms by (metis (no_types) le0 multiplicity_dvd_nat multiplicity_nonprime_nat not_gr0)
-
-lemma multiplicity_dvd'_int:
- fixes x y :: int
- shows "0 < x \<Longrightarrow> 0 \<le> y \<Longrightarrow>
- \<forall>p. prime p \<longrightarrow> multiplicity p x \<le> multiplicity p y \<Longrightarrow> x dvd y"
- by (metis dvd_int_iff abs_of_nat multiplicity_dvd'_nat multiplicity_int_def nat_int
- zero_le_imp_eq_int zero_less_imp_eq_int)
-
-lemma dvd_multiplicity_eq_nat:
- fixes x y :: nat
- shows "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> x dvd y \<longleftrightarrow> (\<forall>p. multiplicity p x \<le> multiplicity p y)"
- by (auto intro: dvd_multiplicity_nat multiplicity_dvd_nat)
-
-lemma dvd_multiplicity_eq_int: "0 < (x::int) \<Longrightarrow> 0 < y \<Longrightarrow>
- (x dvd y) = (\<forall>p\<ge>0. multiplicity p x \<le> multiplicity p y)"
- by (auto intro: dvd_multiplicity_int multiplicity_dvd_int)
-
-lemma prime_factors_altdef2_nat:
- fixes n :: nat
- shows "n > 0 \<Longrightarrow> p \<in> prime_factors n \<longleftrightarrow> prime p \<and> p dvd n"
- apply (cases "prime p")
- apply auto
- apply (subst prime_factorization_nat [where n = n], assumption)
- apply (rule dvd_trans)
- apply (rule dvd_power [where x = p and n = "multiplicity p n"])
- apply (subst (asm) prime_factors_altdef_nat, force)
- apply rule
- apply auto
- apply (metis One_nat_def Zero_not_Suc dvd_multiplicity_nat le0
- le_antisym multiplicity_not_factor_nat multiplicity_prime_nat)
- done
-
-lemma prime_factors_altdef2_int:
- fixes n :: int
- assumes "n > 0"
- shows "p \<in> prime_factors n \<longleftrightarrow> prime p \<and> p dvd n"
- using assms by (simp add: prime_factors_altdef2_nat [transferred])
-
-lemma multiplicity_eq_nat:
- fixes x and y::nat
- assumes [arith]: "x > 0" "y > 0"
- and mult_eq [simp]: "\<And>p. prime p \<Longrightarrow> multiplicity p x = multiplicity p y"
- shows "x = y"
- apply (rule dvd_antisym)
- apply (auto intro: multiplicity_dvd'_nat)
- done
-
-lemma multiplicity_eq_int:
- fixes x y :: int
- assumes [arith]: "x > 0" "y > 0"
- and mult_eq [simp]: "\<And>p. prime p \<Longrightarrow> multiplicity p x = multiplicity p y"
- shows "x = y"
- apply (rule dvd_antisym [transferred])
- apply (auto intro: multiplicity_dvd'_int)
- done
-
-
-subsection \<open>An application\<close>
-
-lemma gcd_eq_nat:
- fixes x y :: nat
- assumes pos [arith]: "x > 0" "y > 0"
- shows "gcd x y =
- (\<Prod>p \<in> prime_factors x \<union> prime_factors y. p ^ min (multiplicity p x) (multiplicity p y))"
- (is "_ = ?z")
-proof -
- have [arith]: "?z > 0"
- using prime_factors_gt_0_nat by auto
- have aux: "\<And>p. prime p \<Longrightarrow> multiplicity p ?z = min (multiplicity p x) (multiplicity p y)"
- apply (subst multiplicity_prod_prime_powers_nat)
- apply auto
- done
- have "?z dvd x"
- by (intro multiplicity_dvd'_nat) (auto simp add: aux intro: prime_gt_0_nat)
- moreover have "?z dvd y"
- by (intro multiplicity_dvd'_nat) (auto simp add: aux intro: prime_gt_0_nat)
- moreover have "w dvd x \<and> w dvd y \<longrightarrow> w dvd ?z" for w
- proof (cases "w = 0")
- case True
- then show ?thesis by simp
- next
- case False
- then show ?thesis
- apply auto
- apply (erule multiplicity_dvd'_nat)
- apply (auto intro: dvd_multiplicity_nat simp add: aux)
- done
- qed
- ultimately have "?z = gcd x y"
- by (subst gcd_unique_nat [symmetric], blast)
- then show ?thesis
- by auto
-qed
-
-lemma lcm_eq_nat:
- assumes pos [arith]: "x > 0" "y > 0"
- shows "lcm (x::nat) y =
- (\<Prod>p \<in> prime_factors x \<union> prime_factors y. p ^ max (multiplicity p x) (multiplicity p y))"
- (is "_ = ?z")
-proof -
- have [arith]: "?z > 0"
- by (auto intro: prime_gt_0_nat)
- have aux: "\<And>p. prime p \<Longrightarrow> multiplicity p ?z = max (multiplicity p x) (multiplicity p y)"
- apply (subst multiplicity_prod_prime_powers_nat)
- apply auto
- done
- have "x dvd ?z"
- by (intro multiplicity_dvd'_nat) (auto simp add: aux)
- moreover have "y dvd ?z"
- by (intro multiplicity_dvd'_nat) (auto simp add: aux)
- moreover have "x dvd w \<and> y dvd w \<longrightarrow> ?z dvd w" for w
- proof (cases "w = 0")
- case True
- then show ?thesis by auto
- next
- case False
- then show ?thesis
- apply auto
- apply (rule multiplicity_dvd'_nat)
- apply (auto intro: prime_gt_0_nat dvd_multiplicity_nat simp add: aux)
- done
- qed
- ultimately have "?z = lcm x y"
- by (subst lcm_unique_nat [symmetric], blast)
- then show ?thesis
- by auto
-qed
-
-lemma multiplicity_gcd_nat:
- fixes p x y :: nat
- assumes [arith]: "x > 0" "y > 0"
- shows "multiplicity p (gcd x y) = min (multiplicity p x) (multiplicity p y)"
- apply (subst gcd_eq_nat)
- apply auto
- apply (subst multiplicity_prod_prime_powers_nat)
- apply auto
- done
-
-lemma multiplicity_lcm_nat:
- fixes p x y :: nat
- assumes [arith]: "x > 0" "y > 0"
- shows "multiplicity p (lcm x y) = max (multiplicity p x) (multiplicity p y)"
- apply (subst lcm_eq_nat)
- apply auto
- apply (subst multiplicity_prod_prime_powers_nat)
- apply auto
- done
-
-lemma gcd_lcm_distrib_nat:
- fixes x y z :: nat
- shows "gcd x (lcm y z) = lcm (gcd x y) (gcd x z)"
- apply (cases "x = 0 | y = 0 | z = 0")
- apply auto
- apply (rule multiplicity_eq_nat)
- apply (auto simp add: multiplicity_gcd_nat multiplicity_lcm_nat lcm_pos_nat)
- done
-
-lemma gcd_lcm_distrib_int:
- fixes x y z :: int
- shows "gcd x (lcm y z) = lcm (gcd x y) (gcd x z)"
- apply (subst (1 2 3) gcd_abs_int)
- apply (subst lcm_abs_int)
- apply (subst (2) abs_of_nonneg)
- apply force
- apply (rule gcd_lcm_distrib_nat [transferred])
- apply auto
- done
-
-end
--- a/src/HOL/Proofs/Extraction/Euclid.thy Wed Jul 20 14:52:09 2016 +0200
+++ b/src/HOL/Proofs/Extraction/Euclid.thy Thu Jul 21 10:06:04 2016 +0200
@@ -27,8 +27,8 @@
lemma prod_mn_less_k: "0 < n \<Longrightarrow> 0 < k \<Longrightarrow> Suc 0 < m \<Longrightarrow> m * n = k \<Longrightarrow> n < k"
by (induct m) auto
-lemma prime_eq: "prime p \<longleftrightarrow> 1 < p \<and> (\<forall>m. m dvd p \<longrightarrow> 1 < m \<longrightarrow> m = p)"
- apply (simp add: prime_def)
+lemma prime_eq: "prime (p::nat) \<longleftrightarrow> 1 < p \<and> (\<forall>m. m dvd p \<longrightarrow> 1 < m \<longrightarrow> m = p)"
+ apply (simp add: is_prime_nat_iff)
apply (rule iffI)
apply blast
apply (erule conjE)
@@ -45,7 +45,7 @@
apply simp
done
-lemma prime_eq': "prime p \<longleftrightarrow> 1 < p \<and> (\<forall>m k. p = m * k \<longrightarrow> 1 < m \<longrightarrow> m = p)"
+lemma prime_eq': "prime (p::nat) \<longleftrightarrow> 1 < p \<and> (\<forall>m k. p = m * k \<longrightarrow> 1 < m \<longrightarrow> m = p)"
by (simp add: prime_eq dvd_def HOL.all_simps [symmetric] del: HOL.all_simps)
lemma not_prime_ex_mk:
@@ -207,7 +207,7 @@
text \<open>Euclid's theorem: there are infinitely many primes.\<close>
-lemma Euclid: "\<exists>p. prime p \<and> n < p"
+lemma Euclid: "\<exists>p::nat. prime p \<and> n < p"
proof -
let ?k = "fact n + (1::nat)"
have "1 < ?k" by simp
--- a/src/HOL/ex/Sqrt.thy Wed Jul 20 14:52:09 2016 +0200
+++ b/src/HOL/ex/Sqrt.thy Thu Jul 21 10:06:04 2016 +0200
@@ -14,7 +14,7 @@
assumes "prime (p::nat)"
shows "sqrt p \<notin> \<rat>"
proof
- from \<open>prime p\<close> have p: "1 < p" by (simp add: prime_def)
+ from \<open>prime p\<close> have p: "1 < p" by (simp add: is_prime_nat_iff)
assume "sqrt p \<in> \<rat>"
then obtain m n :: nat where
n: "n \<noteq> 0" and sqrt_rat: "\<bar>sqrt p\<bar> = m / n"
@@ -59,7 +59,7 @@
assumes "prime (p::nat)"
shows "sqrt p \<notin> \<rat>"
proof
- from \<open>prime p\<close> have p: "1 < p" by (simp add: prime_def)
+ from \<open>prime p\<close> have p: "1 < p" by (simp add: is_prime_nat_iff)
assume "sqrt p \<in> \<rat>"
then obtain m n :: nat where
n: "n \<noteq> 0" and sqrt_rat: "\<bar>sqrt p\<bar> = m / n"
--- a/src/HOL/ex/Sqrt_Script.thy Wed Jul 20 14:52:09 2016 +0200
+++ b/src/HOL/ex/Sqrt_Script.thy Thu Jul 21 10:06:04 2016 +0200
@@ -17,7 +17,7 @@
subsection \<open>Preliminaries\<close>
lemma prime_nonzero: "prime (p::nat) \<Longrightarrow> p \<noteq> 0"
- by (force simp add: prime_def)
+ by (force simp add: is_prime_nat_iff)
lemma prime_dvd_other_side:
"(n::nat) * n = p * (k * k) \<Longrightarrow> prime p \<Longrightarrow> p dvd n"
@@ -32,7 +32,7 @@
apply (erule disjE)
apply (frule mult_le_mono, assumption)
apply auto
- apply (force simp add: prime_def)
+ apply (force simp add: is_prime_nat_iff)
done
lemma rearrange: "(j::nat) * (p * j) = k * k \<Longrightarrow> k * k = p * (j * j)"