# HG changeset patch # User huffman # Date 1245113976 25200 # Node ID 1e252b8b2334014df45840734fee63b1aa19e78e # Parent 84912dff2d746d64a57c15e0bde315cefc30927a move lemma div_power into semiring_div context; class ring_div inherits from idom diff -r 84912dff2d74 -r 1e252b8b2334 src/HOL/Divides.thy --- a/src/HOL/Divides.thy Sat Jun 13 17:31:56 2009 -0700 +++ b/src/HOL/Divides.thy Mon Jun 15 17:59:36 2009 -0700 @@ -331,17 +331,16 @@ "(a * c) mod (b * c) = (a mod b) * c" using mod_mult_mult1 [of c a b] by (simp add: mult_commute) -end - lemma div_power: - "(y::'a::{semiring_div,no_zero_divisors,power}) dvd x \ - (x div y) ^ n = x ^ n div y ^ n" + "y dvd x \ (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 +end + +class ring_div = semiring_div + idom begin text {* Negation respects modular equivalence. *}