# HG changeset patch
# User nipkow
# Date 1236868304 -3600
# Node ID 5e9248e8e2f8c67ffe1e2a5ec83808b34bf5d210
# Parent  03765a88f652ef297562bbe2f29a6b8e510f4647# Parent  0a41b0662264f5f8990385348f3a3039b4a2f75c
merged

diff -r 03765a88f652 -r 5e9248e8e2f8 src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Thu Mar 12 14:27:35 2009 +0100
+++ b/src/HOL/Divides.thy	Thu Mar 12 15:31:44 2009 +0100
@@ -295,6 +295,27 @@
 
 end
 
+lemma div_mult_div_if_dvd: "(y::'a::{semiring_div,no_zero_divisors}) dvd x \<Longrightarrow> 
+  z dvd w \<Longrightarrow> (x div y) * (w div z) = (x * w) div (y * z)"
+unfolding dvd_def
+  apply clarify
+  apply (case_tac "y = 0")
+  apply simp
+  apply (case_tac "z = 0")
+  apply simp
+  apply (simp add: algebra_simps)
+  apply (subst mult_assoc [symmetric])
+  apply (simp add: no_zero_divisors)
+done
+
+
+lemma div_power: "(y::'a::{semiring_div,no_zero_divisors,recpower}) dvd x \<Longrightarrow>
+    (x div y)^n = x^n div y^n"
+apply (induct n)
+ apply simp
+apply(simp add: div_mult_div_if_dvd dvd_power_same)
+done
+
 class ring_div = semiring_div + comm_ring_1
 begin