1.1 --- a/src/HOL/Divides.thy	Sun Feb 15 16:25:39 2009 +0100
     1.2 +++ b/src/HOL/Divides.thy	Sun Feb 15 22:58:02 2009 +0100
     1.3 @@ -172,6 +172,22 @@
     1.4    finally show ?thesis .
     1.5  qed
     1.6  
     1.7 +lemma dvd_imp_mod_0: "a dvd b \<Longrightarrow> b mod a = 0"
     1.8 +by (unfold dvd_def, auto)
     1.9 +
    1.10 +lemma dvd_div_mult_self: "a dvd b \<Longrightarrow> (b div a) * a = b"
    1.11 +by (subst (2) mod_div_equality [of b a, symmetric]) (simp add:dvd_imp_mod_0)
    1.12 +
    1.13 +lemma div_dvd_div[simp]:
    1.14 +  "a dvd b \<Longrightarrow> a dvd c \<Longrightarrow> (b div a dvd c div a) = (b dvd c)"
    1.15 +apply (cases "a = 0")
    1.16 + apply simp
    1.17 +apply (unfold dvd_def)
    1.18 +apply auto
    1.19 + apply(blast intro:mult_assoc[symmetric])
    1.20 +apply(fastsimp simp add: mult_assoc)
    1.21 +done
    1.22 +
    1.23  text {* Addition respects modular equivalence. *}
    1.24  
    1.25  lemma mod_add_left_eq: "(a + b) mod c = (a mod c + b) mod c"

     2.1 --- a/src/HOL/Finite_Set.thy	Sun Feb 15 16:25:39 2009 +0100
     2.2 +++ b/src/HOL/Finite_Set.thy	Sun Feb 15 22:58:02 2009 +0100
     2.3 @@ -1709,6 +1709,42 @@
     2.4  apply (subst divide_inverse, auto)
     2.5  done
     2.6  
     2.7 +lemma setprod_dvd_setprod [rule_format]: 
     2.8 +    "(ALL x : A. f x dvd g x) \<longrightarrow> setprod f A dvd setprod g A"
     2.9 +  apply (cases "finite A")
    2.10 +  apply (induct set: finite)
    2.11 +  apply (auto simp add: dvd_def)
    2.12 +  apply (rule_tac x = "k * ka" in exI)
    2.13 +  apply (simp add: algebra_simps)
    2.14 +done
    2.15 +
    2.16 +lemma setprod_dvd_setprod_subset:
    2.17 +  "finite B \<Longrightarrow> A <= B \<Longrightarrow> setprod f A dvd setprod f B"
    2.18 +  apply (subgoal_tac "setprod f B = setprod f A * setprod f (B - A)")
    2.19 +  apply (unfold dvd_def, blast)
    2.20 +  apply (subst setprod_Un_disjoint [symmetric])
    2.21 +  apply (auto elim: finite_subset intro: setprod_cong)
    2.22 +done
    2.23 +
    2.24 +lemma setprod_dvd_setprod_subset2:
    2.25 +  "finite B \<Longrightarrow> A <= B \<Longrightarrow> ALL x : A. (f x::'a::comm_semiring_1) dvd g x \<Longrightarrow> 
    2.26 +      setprod f A dvd setprod g B"
    2.27 +  apply (rule dvd_trans)
    2.28 +  apply (rule setprod_dvd_setprod, erule (1) bspec)
    2.29 +  apply (erule (1) setprod_dvd_setprod_subset)
    2.30 +done
    2.31 +
    2.32 +lemma dvd_setprod: "finite A \<Longrightarrow> i:A \<Longrightarrow> 
    2.33 +    (f i ::'a::comm_semiring_1) dvd setprod f A"
    2.34 +by (induct set: finite) (auto intro: dvd_mult)
    2.35 +
    2.36 +lemma dvd_setsum [rule_format]: "(ALL i : A. d dvd f i) \<longrightarrow> 
    2.37 +    (d::'a::comm_semiring_1) dvd (SUM x : A. f x)"
    2.38 +  apply (cases "finite A")
    2.39 +  apply (induct set: finite)
    2.40 +  apply auto
    2.41 +done
    2.42 +
    2.43  
    2.44  subsection {* Finite cardinality *}
    2.45  

     3.1 --- a/src/HOL/NumberTheory/IntPrimes.thy	Sun Feb 15 16:25:39 2009 +0100
     3.2 +++ b/src/HOL/NumberTheory/IntPrimes.thy	Sun Feb 15 22:58:02 2009 +0100
     3.3 @@ -144,12 +144,8 @@
     3.4    done
     3.5  
     3.6  lemma zcong_trans:
     3.7 -    "[a = b] (mod m) ==> [b = c] (mod m) ==> [a = c] (mod m)"
     3.8 -  unfolding zcong_def
     3.9 -  apply (auto elim!: dvdE simp add: algebra_simps)
    3.10 -  unfolding left_distrib [symmetric]
    3.11 -  apply (rule dvd_mult dvd_refl)+
    3.12 -  done
    3.13 +  "[a = b] (mod m) ==> [b = c] (mod m) ==> [a = c] (mod m)"
    3.14 +unfolding zcong_def by (auto elim!: dvdE simp add: algebra_simps)
    3.15  
    3.16  lemma zcong_zmult:
    3.17      "[a = b] (mod m) ==> [c = d] (mod m) ==> [a * c = b * d] (mod m)"

     4.1 --- a/src/HOL/Rational.thy	Sun Feb 15 16:25:39 2009 +0100
     4.2 +++ b/src/HOL/Rational.thy	Sun Feb 15 22:58:02 2009 +0100
     4.3 @@ -801,7 +801,7 @@
     4.4    then have "?c \<noteq> 0" by simp
     4.5    then have "Fract ?c ?c = Fract 1 1" by (simp add: eq_rat)
     4.6    moreover have "Fract (a div ?c * ?c + a mod ?c) (b div ?c * ?c + b mod ?c) = Fract a b"
     4.7 -   by (simp add: semiring_div_class.mod_div_equality)
     4.8 +    by (simp add: semiring_div_class.mod_div_equality)
     4.9    moreover have "a mod ?c = 0" by (simp add: dvd_eq_mod_eq_0 [symmetric])
    4.10    moreover have "b mod ?c = 0" by (simp add: dvd_eq_mod_eq_0 [symmetric])
    4.11    ultimately show ?thesis

     5.1 --- a/src/HOL/Ring_and_Field.thy	Sun Feb 15 16:25:39 2009 +0100
     5.2 +++ b/src/HOL/Ring_and_Field.thy	Sun Feb 15 22:58:02 2009 +0100
     5.3 @@ -122,7 +122,7 @@
     5.4  
     5.5  subclass semiring_1 ..
     5.6  
     5.7 -lemma dvd_refl: "a dvd a"
     5.8 +lemma dvd_refl[simp]: "a dvd a"
     5.9  proof
    5.10    show "a = a * 1" by simp
    5.11  qed
    5.12 @@ -182,19 +182,18 @@
    5.13  lemma dvd_0_left: "0 dvd a \<Longrightarrow> a = 0"
    5.14  by simp
    5.15  
    5.16 -lemma dvd_add:
    5.17 -  assumes ab: "a dvd b"
    5.18 -    and ac: "a dvd c"
    5.19 -    shows "a dvd (b + c)"
    5.20 +lemma dvd_add[simp]:
    5.21 +  assumes "a dvd b" and "a dvd c" shows "a dvd (b + c)"
    5.22  proof -
    5.23 -  from ab obtain b' where "b = a * b'" ..
    5.24 -  moreover from ac obtain c' where "c = a * c'" ..
    5.25 +  from `a dvd b` obtain b' where "b = a * b'" ..
    5.26 +  moreover from `a dvd c` obtain c' where "c = a * c'" ..
    5.27    ultimately have "b + c = a * (b' + c')" by (simp add: right_distrib)
    5.28    then show ?thesis ..
    5.29  qed
    5.30  
    5.31  end
    5.32  
    5.33 +
    5.34  class no_zero_divisors = zero + times +
    5.35    assumes no_zero_divisors: "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> a * b \<noteq> 0"
    5.36