src/HOL/Number_Theory/Primes.thy
changeset 57512 cc97b347b301
parent 55337 5d45fb978d5a
child 58623 2db1df2c8467
     1.1 --- a/src/HOL/Number_Theory/Primes.thy	Fri Jul 04 20:07:08 2014 +0200
     1.2 +++ b/src/HOL/Number_Theory/Primes.thy	Fri Jul 04 20:18:47 2014 +0200
     1.3 @@ -106,7 +106,7 @@
     1.4  lemma not_prime_eq_prod_nat: "(n::nat) > 1 \<Longrightarrow> ~ prime n \<Longrightarrow>
     1.5      EX m k. n = m * k & 1 < m & m < n & 1 < k & k < n"
     1.6    unfolding prime_nat_def dvd_def apply auto
     1.7 -  by (metis mult_commute linorder_neq_iff linorder_not_le mult_1
     1.8 +  by (metis mult.commute linorder_neq_iff linorder_not_le mult_1
     1.9        n_less_n_mult_m one_le_mult_iff less_imp_le_nat)
    1.10  
    1.11  lemma prime_dvd_power_nat: "prime p \<Longrightarrow> p dvd x^n \<Longrightarrow> p dvd x"
    1.12 @@ -209,7 +209,7 @@
    1.13        from coprime_dvd_mult_nat[OF pnb pab] have ?thesis by blast }
    1.14      moreover
    1.15      { assume pb: "p dvd b"
    1.16 -      have pnba: "p^n dvd b*a" using pab by (simp add: mult_commute)
    1.17 +      have pnba: "p^n dvd b*a" using pab by (simp add: mult.commute)
    1.18        from coprime_common_divisor_nat [OF ab, of p] pb p have "\<not> p dvd a"
    1.19          by auto
    1.20        with p have "coprime a p"
    1.21 @@ -323,7 +323,7 @@
    1.22    moreover 
    1.23    {assume px: "p dvd y"
    1.24      then obtain d where d: "y = p*d" unfolding dvd_def by blast
    1.25 -    from Suc.prems d  have "p*d*x = p^Suc k" by (simp add: mult_commute)
    1.26 +    from Suc.prems d  have "p*d*x = p^Suc k" by (simp add: mult.commute)
    1.27      hence th: "d*x = p^k" using p0 by simp
    1.28      from Suc.hyps[OF th] obtain i j where ij: "d = p^i" "x = p^j" by blast
    1.29      with d have "y = p^Suc i" by simp 
    1.30 @@ -355,7 +355,7 @@
    1.31    shows "d dvd p^k \<longleftrightarrow> (\<exists> i. i \<le> k \<and> d = p ^i)"
    1.32  proof
    1.33    assume H: "d dvd p^k" then obtain e where e: "d*e = p^k" 
    1.34 -    unfolding dvd_def  apply (auto simp add: mult_commute) by blast
    1.35 +    unfolding dvd_def  apply (auto simp add: mult.commute) by blast
    1.36    from prime_power_mult[OF p e] obtain i j where ij: "d = p^i" "e=p^j" by blast
    1.37    from e ij have "p^(i + j) = p^k" by (simp add: power_add)
    1.38    hence "i + j = k" using p prime_gt_1_nat power_inject_exp[of p "i+j" k] by simp