relaxed preconditions
authorhaftmann
Sun Aug 18 15:29:50 2013 +0200 (2013-08-18)
changeset 5306841fc65da66f1
parent 53067 ee0b7c2315d2
child 53069 d165213e3924
relaxed preconditions
src/HOL/Divides.thy
     1.1 --- a/src/HOL/Divides.thy	Sun Aug 18 15:29:50 2013 +0200
     1.2 +++ b/src/HOL/Divides.thy	Sun Aug 18 15:29:50 2013 +0200
     1.3 @@ -2122,15 +2122,18 @@
     1.4                     zero_less_mult_iff distrib_left [symmetric] 
     1.5                     zmult2_lemma_aux1 zmult2_lemma_aux2 zmult2_lemma_aux3 zmult2_lemma_aux4 mult_less_0_iff split: split_if_asm)
     1.6  
     1.7 -lemma zdiv_zmult2_eq: "(0::int) < c ==> a div (b*c) = (a div b) div c"
     1.8 +lemma zdiv_zmult2_eq:
     1.9 +  fixes a b c :: int
    1.10 +  shows "0 \<le> c \<Longrightarrow> a div (b * c) = (a div b) div c"
    1.11  apply (case_tac "b = 0", simp)
    1.12 -apply (force simp add: divmod_int_rel_div_mod [THEN zmult2_lemma, THEN div_int_unique])
    1.13 +apply (force simp add: le_less divmod_int_rel_div_mod [THEN zmult2_lemma, THEN div_int_unique])
    1.14  done
    1.15  
    1.16  lemma zmod_zmult2_eq:
    1.17 -     "(0::int) < c ==> a mod (b*c) = b*(a div b mod c) + a mod b"
    1.18 +  fixes a b c :: int
    1.19 +  shows "0 \<le> c \<Longrightarrow> a mod (b * c) = b * (a div b mod c) + a mod b"
    1.20  apply (case_tac "b = 0", simp)
    1.21 -apply (force simp add: divmod_int_rel_div_mod [THEN zmult2_lemma, THEN mod_int_unique])
    1.22 +apply (force simp add: le_less divmod_int_rel_div_mod [THEN zmult2_lemma, THEN mod_int_unique])
    1.23  done
    1.24  
    1.25  lemma div_pos_geq:
    1.26 @@ -2555,9 +2558,10 @@
    1.27    by auto
    1.28  
    1.29  instance int :: semiring_numeral_div
    1.30 -  by intro_classes (auto intro: zmod_le_nonneg_dividend simp add: zmult_div_cancel
    1.31 -    pos_imp_zdiv_pos_iff div_pos_pos_trivial mod_pos_pos_trivial,
    1.32 -    auto intro: zmod_zmult2_eq zdiv_zmult2_eq simp add: le_less)
    1.33 +  by intro_classes (auto intro: zmod_le_nonneg_dividend
    1.34 +    simp add: zmult_div_cancel
    1.35 +    pos_imp_zdiv_pos_iff div_pos_pos_trivial mod_pos_pos_trivial
    1.36 +    zmod_zmult2_eq zdiv_zmult2_eq)
    1.37  
    1.38  
    1.39  subsubsection {* Tools setup *}