# HG changeset patch
# User nipkow
# Date 1234735082 -3600
# Node ID 17d1e32ef867ebe794bc504875f3de5595271283
# Parent  f270fe271a656bf995dd307ca8679356d53c63d8
dvd and setprod lemmas

diff -r f270fe271a65 -r 17d1e32ef867 src/HOL/Divides.thy
--- 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"
diff -r f270fe271a65 -r 17d1e32ef867 src/HOL/Finite_Set.thy
--- 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 *}
 
diff -r f270fe271a65 -r 17d1e32ef867 src/HOL/NumberTheory/IntPrimes.thy
--- 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)"
diff -r f270fe271a65 -r 17d1e32ef867 src/HOL/Rational.thy
--- 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
diff -r f270fe271a65 -r 17d1e32ef867 src/HOL/Ring_and_Field.thy
--- 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"