src/HOL/Divides.thy
changeset 25112 98824cc791c0
parent 25062 af5ef0d4d655
child 25134 3d4953e88449
     1.1 --- a/src/HOL/Divides.thy	Sat Oct 20 12:09:30 2007 +0200
     1.2 +++ b/src/HOL/Divides.thy	Sat Oct 20 12:09:33 2007 +0200
     1.3 @@ -275,12 +275,14 @@
     1.4    by (auto simp add: split_ifs mult_ac quorem_def add_mult_distrib2)
     1.5  
     1.6  lemma div_mult1_eq: "(a*b) div c = a*(b div c) + a*(b mod c) div (c::nat)"
     1.7 -  apply (cases "c = 0", simp)
     1.8 +  apply (cases "c = 0", simp  add: neq0_conv)
     1.9 +  using neq0_conv
    1.10    apply (blast intro: quorem_div_mod [THEN quorem_mult1_eq, THEN quorem_div])
    1.11    done
    1.12  
    1.13  lemma mod_mult1_eq: "(a*b) mod c = a*(b mod c) mod (c::nat)"
    1.14 -  apply (cases "c = 0", simp)
    1.15 +  apply (cases "c = 0", simp add: neq0_conv)
    1.16 +  using neq0_conv
    1.17    apply (blast intro: quorem_div_mod [THEN quorem_mult1_eq, THEN quorem_mod])
    1.18    done
    1.19  
    1.20 @@ -307,11 +309,13 @@
    1.21  lemma div_add1_eq:
    1.22       "(a+b) div (c::nat) = a div c + b div c + ((a mod c + b mod c) div c)"
    1.23    apply (cases "c = 0", simp)
    1.24 +  using neq0_conv
    1.25    apply (blast intro: quorem_add1_eq [THEN quorem_div] quorem_div_mod quorem_div_mod)
    1.26    done
    1.27  
    1.28  lemma mod_add1_eq: "(a+b) mod (c::nat) = (a mod c + b mod c) mod c"
    1.29    apply (cases "c = 0", simp)
    1.30 +  using neq0_conv
    1.31    apply (blast intro: quorem_div_mod quorem_div_mod quorem_add1_eq [THEN quorem_mod])
    1.32    done
    1.33