avoid trivial definition
authorhaftmann
Sun Oct 08 22:28:20 2017 +0200 (19 months ago)
changeset 66803dd8922885a68
parent 66802 627511c13164
child 66804 3f9bb52082c4
avoid trivial definition
NEWS
src/HOL/GCD.thy
src/HOL/Number_Theory/Totient.thy
     1.1 --- a/NEWS	Sun Oct 08 22:28:20 2017 +0200
     1.2 +++ b/NEWS	Sun Oct 08 22:28:20 2017 +0200
     1.3 @@ -47,6 +47,9 @@
     1.4  * Fact mod_mult_self4 (on nat) renamed to mod_mult_self3', to avoid clash
     1.5  with fact mod_mult_self4 (on more generic semirings). INCOMPATIBILITY.
     1.6  
     1.7 +* Predicate pairwise_coprime abolished, use "pairwise coprime" instead.
     1.8 +INCOMPATIBILITY.
     1.9 +
    1.10  
    1.11  *** System ***
    1.12  
     2.1 --- a/src/HOL/GCD.thy	Sun Oct 08 22:28:20 2017 +0200
     2.2 +++ b/src/HOL/GCD.thy	Sun Oct 08 22:28:20 2017 +0200
     2.3 @@ -1510,21 +1510,6 @@
     2.4  lemma Gcd_2 [simp]: "Gcd {a, b} = gcd a b"
     2.5    by simp
     2.6  
     2.7 -
     2.8 -definition pairwise_coprime
     2.9 -  where "pairwise_coprime A = (\<forall>x y. x \<in> A \<and> y \<in> A \<and> x \<noteq> y \<longrightarrow> coprime x y)"
    2.10 -
    2.11 -lemma pairwise_coprimeI [intro?]:
    2.12 -  "(\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> x \<noteq> y \<Longrightarrow> coprime x y) \<Longrightarrow> pairwise_coprime A"
    2.13 -  by (simp add: pairwise_coprime_def)
    2.14 -
    2.15 -lemma pairwise_coprimeD:
    2.16 -  "pairwise_coprime A \<Longrightarrow> x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> x \<noteq> y \<Longrightarrow> coprime x y"
    2.17 -  by (simp add: pairwise_coprime_def)
    2.18 -
    2.19 -lemma pairwise_coprime_subset: "pairwise_coprime A \<Longrightarrow> B \<subseteq> A \<Longrightarrow> pairwise_coprime B"
    2.20 -  by (force simp: pairwise_coprime_def)
    2.21 -
    2.22  end
    2.23  
    2.24  
     3.1 --- a/src/HOL/Number_Theory/Totient.thy	Sun Oct 08 22:28:20 2017 +0200
     3.2 +++ b/src/HOL/Number_Theory/Totient.thy	Sun Oct 08 22:28:20 2017 +0200
     3.3 @@ -335,19 +335,30 @@
     3.4  qed
     3.5  
     3.6  lemma totient_prod_coprime:
     3.7 -  assumes "pairwise_coprime (f ` A)" "inj_on f A"
     3.8 -  shows   "totient (prod f A) = prod (\<lambda>x. totient (f x)) A"
     3.9 +  assumes "pairwise coprime (f ` A)" "inj_on f A"
    3.10 +  shows   "totient (prod f A) = (\<Prod>a\<in>A. totient (f a))"
    3.11    using assms
    3.12  proof (induction A rule: infinite_finite_induct)
    3.13    case (insert x A)
    3.14 -  from insert.prems and insert.hyps have *: "coprime (prod f A) (f x)"
    3.15 -    by (intro prod_coprime[OF pairwise_coprimeD[OF insert.prems(1)]]) (auto simp: inj_on_def)
    3.16 +  have *: "coprime (prod f A) (f x)"
    3.17 +  proof (rule prod_coprime)
    3.18 +    fix y
    3.19 +    assume "y \<in> A"
    3.20 +    with \<open>x \<notin> A\<close> have "y \<noteq> x"
    3.21 +      by auto
    3.22 +    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"
    3.23 +      using inj_onD [of f "insert x A" y x]
    3.24 +      by auto
    3.25 +    with \<open>y \<in> A\<close> show "coprime (f y) (f x)"
    3.26 +      using pairwiseD [OF \<open>pairwise coprime (f ` insert x A)\<close>]
    3.27 +      by auto
    3.28 +  qed
    3.29    from insert.hyps have "prod f (insert x A) = prod f A * f x" by simp
    3.30    also have "totient \<dots> = totient (prod f A) * totient (f x)"
    3.31      using insert.hyps insert.prems by (intro totient_mult_coprime *)
    3.32 -  also have "totient (prod f A) = (\<Prod>x\<in>A. totient (f x))" 
    3.33 -    using insert.prems by (intro insert.IH) (auto dest: pairwise_coprime_subset)
    3.34 -  also from insert.hyps have "\<dots> * totient (f x) = (\<Prod>x\<in>insert x A. totient (f x))" by simp
    3.35 +  also have "totient (prod f A) = (\<Prod>a\<in>A. totient (f a))" 
    3.36 +    using insert.prems by (intro insert.IH) (auto dest: pairwise_subset)
    3.37 +  also from insert.hyps have "\<dots> * totient (f x) = (\<Prod>a\<in>insert x A. totient (f a))" by simp
    3.38    finally show ?case .
    3.39  qed simp_all
    3.40  
    3.41 @@ -375,8 +386,8 @@
    3.42      by (rule prime_factorization_nat)
    3.43    also have "totient \<dots> = (\<Prod>x\<in>prime_factors n. totient (x ^ multiplicity x n))"
    3.44    proof (rule totient_prod_coprime)
    3.45 -    show "pairwise_coprime ((\<lambda>p. p ^ multiplicity p n) ` prime_factors n)"
    3.46 -    proof (standard, clarify, goal_cases)
    3.47 +    show "pairwise coprime ((\<lambda>p. p ^ multiplicity p n) ` prime_factors n)"
    3.48 +    proof (rule pairwiseI, clarify)
    3.49        fix p q assume "p \<in># prime_factorization n" "q \<in># prime_factorization n" 
    3.50                       "p ^ multiplicity p n \<noteq> q ^ multiplicity q n"
    3.51        thus "coprime (p ^ multiplicity p n) (q ^ multiplicity q n)"