--- a/NEWS Sun Oct 08 22:28:20 2017 +0200
+++ b/NEWS Sun Oct 08 22:28:20 2017 +0200
@@ -47,6 +47,9 @@
* Fact mod_mult_self4 (on nat) renamed to mod_mult_self3', to avoid clash
with fact mod_mult_self4 (on more generic semirings). INCOMPATIBILITY.
+* Predicate pairwise_coprime abolished, use "pairwise coprime" instead.
+INCOMPATIBILITY.
+
*** System ***
--- a/src/HOL/GCD.thy Sun Oct 08 22:28:20 2017 +0200
+++ b/src/HOL/GCD.thy Sun Oct 08 22:28:20 2017 +0200
@@ -1510,21 +1510,6 @@
lemma Gcd_2 [simp]: "Gcd {a, b} = gcd a b"
by simp
-
-definition pairwise_coprime
- where "pairwise_coprime A = (\<forall>x y. x \<in> A \<and> y \<in> A \<and> x \<noteq> y \<longrightarrow> coprime x y)"
-
-lemma pairwise_coprimeI [intro?]:
- "(\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> x \<noteq> y \<Longrightarrow> coprime x y) \<Longrightarrow> pairwise_coprime A"
- by (simp add: pairwise_coprime_def)
-
-lemma pairwise_coprimeD:
- "pairwise_coprime A \<Longrightarrow> x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> x \<noteq> y \<Longrightarrow> coprime x y"
- by (simp add: pairwise_coprime_def)
-
-lemma pairwise_coprime_subset: "pairwise_coprime A \<Longrightarrow> B \<subseteq> A \<Longrightarrow> pairwise_coprime B"
- by (force simp: pairwise_coprime_def)
-
end
--- a/src/HOL/Number_Theory/Totient.thy Sun Oct 08 22:28:20 2017 +0200
+++ b/src/HOL/Number_Theory/Totient.thy Sun Oct 08 22:28:20 2017 +0200
@@ -335,19 +335,30 @@
qed
lemma totient_prod_coprime:
- assumes "pairwise_coprime (f ` A)" "inj_on f A"
- shows "totient (prod f A) = prod (\<lambda>x. totient (f x)) A"
+ assumes "pairwise coprime (f ` A)" "inj_on f A"
+ shows "totient (prod f A) = (\<Prod>a\<in>A. totient (f a))"
using assms
proof (induction A rule: infinite_finite_induct)
case (insert x A)
- from insert.prems and insert.hyps have *: "coprime (prod f A) (f x)"
- by (intro prod_coprime[OF pairwise_coprimeD[OF insert.prems(1)]]) (auto simp: inj_on_def)
+ have *: "coprime (prod f A) (f x)"
+ proof (rule prod_coprime)
+ fix y
+ assume "y \<in> A"
+ with \<open>x \<notin> A\<close> have "y \<noteq> x"
+ by auto
+ with \<open>x \<notin> A\<close> \<open>y \<in> A\<close> \<open>inj_on f (insert x A)\<close> have "f y \<noteq> f x"
+ using inj_onD [of f "insert x A" y x]
+ by auto
+ with \<open>y \<in> A\<close> show "coprime (f y) (f x)"
+ using pairwiseD [OF \<open>pairwise coprime (f ` insert x A)\<close>]
+ by auto
+ qed
from insert.hyps have "prod f (insert x A) = prod f A * f x" by simp
also have "totient \<dots> = totient (prod f A) * totient (f x)"
using insert.hyps insert.prems by (intro totient_mult_coprime *)
- also have "totient (prod f A) = (\<Prod>x\<in>A. totient (f x))"
- using insert.prems by (intro insert.IH) (auto dest: pairwise_coprime_subset)
- also from insert.hyps have "\<dots> * totient (f x) = (\<Prod>x\<in>insert x A. totient (f x))" by simp
+ also have "totient (prod f A) = (\<Prod>a\<in>A. totient (f a))"
+ using insert.prems by (intro insert.IH) (auto dest: pairwise_subset)
+ also from insert.hyps have "\<dots> * totient (f x) = (\<Prod>a\<in>insert x A. totient (f a))" by simp
finally show ?case .
qed simp_all
@@ -375,8 +386,8 @@
by (rule prime_factorization_nat)
also have "totient \<dots> = (\<Prod>x\<in>prime_factors n. totient (x ^ multiplicity x n))"
proof (rule totient_prod_coprime)
- show "pairwise_coprime ((\<lambda>p. p ^ multiplicity p n) ` prime_factors n)"
- proof (standard, clarify, goal_cases)
+ show "pairwise coprime ((\<lambda>p. p ^ multiplicity p n) ` prime_factors n)"
+ proof (rule pairwiseI, clarify)
fix p q assume "p \<in># prime_factorization n" "q \<in># prime_factorization n"
"p ^ multiplicity p n \<noteq> q ^ multiplicity q n"
thus "coprime (p ^ multiplicity p n) (q ^ multiplicity q n)"