# HG changeset patch
# User haftmann
# Date 1507494500 -7200
# Node ID dd8922885a6831ce96bab8c9a9f04802b13b74fd
# Parent  627511c13164eea39b69c2dddb5d9ce46bc21c7e
avoid trivial definition

diff -r 627511c13164 -r dd8922885a68 NEWS
--- 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 ***
 
diff -r 627511c13164 -r dd8922885a68 src/HOL/GCD.thy
--- 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
 
 
diff -r 627511c13164 -r dd8922885a68 src/HOL/Number_Theory/Totient.thy
--- 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)"