1.1 --- a/src/HOL/Divides.thy	Thu Mar 12 00:02:30 2009 +0100
     1.2 +++ b/src/HOL/Divides.thy	Thu Mar 12 15:31:26 2009 +0100
     1.3 @@ -295,6 +295,27 @@
     1.4  
     1.5  end
     1.6  
     1.7 +lemma div_mult_div_if_dvd: "(y::'a::{semiring_div,no_zero_divisors}) dvd x \<Longrightarrow> 
     1.8 +  z dvd w \<Longrightarrow> (x div y) * (w div z) = (x * w) div (y * z)"
     1.9 +unfolding dvd_def
    1.10 +  apply clarify
    1.11 +  apply (case_tac "y = 0")
    1.12 +  apply simp
    1.13 +  apply (case_tac "z = 0")
    1.14 +  apply simp
    1.15 +  apply (simp add: algebra_simps)
    1.16 +  apply (subst mult_assoc [symmetric])
    1.17 +  apply (simp add: no_zero_divisors)
    1.18 +done
    1.19 +
    1.20 +
    1.21 +lemma div_power: "(y::'a::{semiring_div,no_zero_divisors,recpower}) dvd x \<Longrightarrow>
    1.22 +    (x div y)^n = x^n div y^n"
    1.23 +apply (induct n)
    1.24 + apply simp
    1.25 +apply(simp add: div_mult_div_if_dvd dvd_power_same)
    1.26 +done
    1.27 +
    1.28  class ring_div = semiring_div + comm_ring_1
    1.29  begin
    1.30