--- a/src/HOL/Divides.thy Sun Feb 15 16:25:39 2009 +0100
+++ b/src/HOL/Divides.thy Sun Feb 15 22:58:02 2009 +0100
@@ -172,6 +172,22 @@
finally show ?thesis .
qed
+lemma dvd_imp_mod_0: "a dvd b \<Longrightarrow> b mod a = 0"
+by (unfold dvd_def, auto)
+
+lemma dvd_div_mult_self: "a dvd b \<Longrightarrow> (b div a) * a = b"
+by (subst (2) mod_div_equality [of b a, symmetric]) (simp add:dvd_imp_mod_0)
+
+lemma div_dvd_div[simp]:
+ "a dvd b \<Longrightarrow> a dvd c \<Longrightarrow> (b div a dvd c div a) = (b dvd c)"
+apply (cases "a = 0")
+ apply simp
+apply (unfold dvd_def)
+apply auto
+ apply(blast intro:mult_assoc[symmetric])
+apply(fastsimp simp add: mult_assoc)
+done
+
text {* Addition respects modular equivalence. *}
lemma mod_add_left_eq: "(a + b) mod c = (a mod c + b) mod c"
--- a/src/HOL/Finite_Set.thy Sun Feb 15 16:25:39 2009 +0100
+++ b/src/HOL/Finite_Set.thy Sun Feb 15 22:58:02 2009 +0100
@@ -1709,6 +1709,42 @@
apply (subst divide_inverse, auto)
done
+lemma setprod_dvd_setprod [rule_format]:
+ "(ALL x : A. f x dvd g x) \<longrightarrow> setprod f A dvd setprod g A"
+ apply (cases "finite A")
+ apply (induct set: finite)
+ apply (auto simp add: dvd_def)
+ apply (rule_tac x = "k * ka" in exI)
+ apply (simp add: algebra_simps)
+done
+
+lemma setprod_dvd_setprod_subset:
+ "finite B \<Longrightarrow> A <= B \<Longrightarrow> setprod f A dvd setprod f B"
+ apply (subgoal_tac "setprod f B = setprod f A * setprod f (B - A)")
+ apply (unfold dvd_def, blast)
+ apply (subst setprod_Un_disjoint [symmetric])
+ apply (auto elim: finite_subset intro: setprod_cong)
+done
+
+lemma setprod_dvd_setprod_subset2:
+ "finite B \<Longrightarrow> A <= B \<Longrightarrow> ALL x : A. (f x::'a::comm_semiring_1) dvd g x \<Longrightarrow>
+ setprod f A dvd setprod g B"
+ apply (rule dvd_trans)
+ apply (rule setprod_dvd_setprod, erule (1) bspec)
+ apply (erule (1) setprod_dvd_setprod_subset)
+done
+
+lemma dvd_setprod: "finite A \<Longrightarrow> i:A \<Longrightarrow>
+ (f i ::'a::comm_semiring_1) dvd setprod f A"
+by (induct set: finite) (auto intro: dvd_mult)
+
+lemma dvd_setsum [rule_format]: "(ALL i : A. d dvd f i) \<longrightarrow>
+ (d::'a::comm_semiring_1) dvd (SUM x : A. f x)"
+ apply (cases "finite A")
+ apply (induct set: finite)
+ apply auto
+done
+
subsection {* Finite cardinality *}
--- a/src/HOL/NumberTheory/IntPrimes.thy Sun Feb 15 16:25:39 2009 +0100
+++ b/src/HOL/NumberTheory/IntPrimes.thy Sun Feb 15 22:58:02 2009 +0100
@@ -144,12 +144,8 @@
done
lemma zcong_trans:
- "[a = b] (mod m) ==> [b = c] (mod m) ==> [a = c] (mod m)"
- unfolding zcong_def
- apply (auto elim!: dvdE simp add: algebra_simps)
- unfolding left_distrib [symmetric]
- apply (rule dvd_mult dvd_refl)+
- done
+ "[a = b] (mod m) ==> [b = c] (mod m) ==> [a = c] (mod m)"
+unfolding zcong_def by (auto elim!: dvdE simp add: algebra_simps)
lemma zcong_zmult:
"[a = b] (mod m) ==> [c = d] (mod m) ==> [a * c = b * d] (mod m)"
--- a/src/HOL/Rational.thy Sun Feb 15 16:25:39 2009 +0100
+++ b/src/HOL/Rational.thy Sun Feb 15 22:58:02 2009 +0100
@@ -801,7 +801,7 @@
then have "?c \<noteq> 0" by simp
then have "Fract ?c ?c = Fract 1 1" by (simp add: eq_rat)
moreover have "Fract (a div ?c * ?c + a mod ?c) (b div ?c * ?c + b mod ?c) = Fract a b"
- by (simp add: semiring_div_class.mod_div_equality)
+ by (simp add: semiring_div_class.mod_div_equality)
moreover have "a mod ?c = 0" by (simp add: dvd_eq_mod_eq_0 [symmetric])
moreover have "b mod ?c = 0" by (simp add: dvd_eq_mod_eq_0 [symmetric])
ultimately show ?thesis
--- a/src/HOL/Ring_and_Field.thy Sun Feb 15 16:25:39 2009 +0100
+++ b/src/HOL/Ring_and_Field.thy Sun Feb 15 22:58:02 2009 +0100
@@ -122,7 +122,7 @@
subclass semiring_1 ..
-lemma dvd_refl: "a dvd a"
+lemma dvd_refl[simp]: "a dvd a"
proof
show "a = a * 1" by simp
qed
@@ -182,19 +182,18 @@
lemma dvd_0_left: "0 dvd a \<Longrightarrow> a = 0"
by simp
-lemma dvd_add:
- assumes ab: "a dvd b"
- and ac: "a dvd c"
- shows "a dvd (b + c)"
+lemma dvd_add[simp]:
+ assumes "a dvd b" and "a dvd c" shows "a dvd (b + c)"
proof -
- from ab obtain b' where "b = a * b'" ..
- moreover from ac obtain c' where "c = a * c'" ..
+ from `a dvd b` obtain b' where "b = a * b'" ..
+ moreover from `a dvd c` obtain c' where "c = a * c'" ..
ultimately have "b + c = a * (b' + c')" by (simp add: right_distrib)
then show ?thesis ..
qed
end
+
class no_zero_divisors = zero + times +
assumes no_zero_divisors: "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> a * b \<noteq> 0"