src/HOL/Divides.thy
changeset 30224 79136ce06bdb
parent 30180 6d29a873141f
child 30242 aea5d7fa7ef5
     1.1 --- a/src/HOL/Divides.thy	Tue Mar 03 12:14:52 2009 +1100
     1.2 +++ b/src/HOL/Divides.thy	Tue Mar 03 17:05:18 2009 +0100
     1.3 @@ -684,16 +684,6 @@
     1.4  apply (blast intro: divmod_rel [THEN divmod_rel_mult1_eq, THEN div_eq])
     1.5  done
     1.6  
     1.7 -lemma mod_mult1_eq: "(a*b) mod c = a*(b mod c) mod (c::nat)"
     1.8 -by (rule mod_mult_right_eq)
     1.9 -
    1.10 -lemma mod_mult1_eq': "(a*b) mod (c::nat) = ((a mod c) * b) mod c"
    1.11 -by (rule mod_mult_left_eq)
    1.12 -
    1.13 -lemma mod_mult_distrib_mod:
    1.14 -  "(a*b) mod (c::nat) = ((a mod c) * (b mod c)) mod c"
    1.15 -by (rule mod_mult_eq)
    1.16 -
    1.17  lemma divmod_rel_add1_eq:
    1.18    "[| divmod_rel a c aq ar; divmod_rel b c bq br;  c > 0 |]
    1.19     ==> divmod_rel (a + b) c (aq + bq + (ar+br) div c) ((ar + br) mod c)"
    1.20 @@ -706,9 +696,6 @@
    1.21  apply (blast intro: divmod_rel_add1_eq [THEN div_eq] divmod_rel)
    1.22  done
    1.23  
    1.24 -lemma mod_add1_eq: "(a+b) mod (c::nat) = (a mod c + b mod c) mod c"
    1.25 -by (rule mod_add_eq)
    1.26 -
    1.27  lemma mod_lemma: "[| (0::nat) < c; r < b |] ==> b * (q mod c) + r < b * c"
    1.28    apply (cut_tac m = q and n = c in mod_less_divisor)
    1.29    apply (drule_tac [2] m = "q mod c" in less_imp_Suc_add, auto)