removed redundant lemma
authornipkow
Fri Dec 04 08:52:09 2009 +0100 (2009-12-04)
changeset 33946fcc20072df9a
parent 33945 8493ed132fed
child 33948 dbc1a5b94449
removed redundant lemma
src/HOL/GCD.thy
src/HOL/Number_Theory/Primes.thy
     1.1 --- a/src/HOL/GCD.thy	Fri Dec 04 08:26:25 2009 +0100
     1.2 +++ b/src/HOL/GCD.thy	Fri Dec 04 08:52:09 2009 +0100
     1.3 @@ -779,14 +779,6 @@
     1.4    apply auto
     1.5  done
     1.6  
     1.7 -lemma coprime_divprod_nat: "(d::nat) dvd a * b  \<Longrightarrow> coprime d a \<Longrightarrow> d dvd b"
     1.8 -  using coprime_dvd_mult_iff_nat[of d a b]
     1.9 -  by (auto simp add: mult_commute)
    1.10 -
    1.11 -lemma coprime_divprod_int: "(d::int) dvd a * b  \<Longrightarrow> coprime d a \<Longrightarrow> d dvd b"
    1.12 -  using coprime_dvd_mult_iff_int[of d a b]
    1.13 -  by (auto simp add: mult_commute)
    1.14 -
    1.15  lemma division_decomp_nat: assumes dc: "(a::nat) dvd b * c"
    1.16    shows "\<exists>b' c'. a = b' * c' \<and> b' dvd b \<and> c' dvd c"
    1.17  proof-
     2.1 --- a/src/HOL/Number_Theory/Primes.thy	Fri Dec 04 08:26:25 2009 +0100
     2.2 +++ b/src/HOL/Number_Theory/Primes.thy	Fri Dec 04 08:52:09 2009 +0100
     2.3 @@ -360,16 +360,15 @@
     2.4      from prime_dvd_mult_nat[OF p pab']
     2.5      have "p dvd a \<or> p dvd b" .
     2.6      moreover
     2.7 -    {assume pa: "p dvd a"
     2.8 -      have pnba: "p^n dvd b*a" using pab by (simp add: mult_commute)
     2.9 +    { assume pa: "p dvd a"
    2.10        from coprime_common_divisor_nat [OF ab, OF pa] p have "\<not> p dvd b" by auto
    2.11        with p have "coprime b p"
    2.12          by (subst gcd_commute_nat, intro prime_imp_coprime_nat)
    2.13        hence pnb: "coprime (p^n) b"
    2.14          by (subst gcd_commute_nat, rule coprime_exp_nat)
    2.15 -      from coprime_divprod_nat[OF pnba pnb] have ?thesis by blast }
    2.16 +      from coprime_dvd_mult_nat[OF pnb pab] have ?thesis by blast }
    2.17      moreover
    2.18 -    {assume pb: "p dvd b"
    2.19 +    { assume pb: "p dvd b"
    2.20        have pnba: "p^n dvd b*a" using pab by (simp add: mult_commute)
    2.21        from coprime_common_divisor_nat [OF ab, of p] pb p have "\<not> p dvd a"
    2.22          by auto
    2.23 @@ -377,7 +376,7 @@
    2.24          by (subst gcd_commute_nat, intro prime_imp_coprime_nat)
    2.25        hence pna: "coprime (p^n) a"
    2.26          by (subst gcd_commute_nat, rule coprime_exp_nat)
    2.27 -      from coprime_divprod_nat[OF pab pna] have ?thesis by blast }
    2.28 +      from coprime_dvd_mult_nat[OF pna pnba] have ?thesis by blast }
    2.29      ultimately have ?thesis by blast}
    2.30    ultimately show ?thesis by blast
    2.31  qed