# HG changeset patch
# User haftmann
# Date 1376832590 -7200
# Node ID 41fc65da66f1b2d7c043282f63b9f95558fa0616
# Parent  ee0b7c2315d24533e056444b9b00177305f0ff97
relaxed preconditions

diff -r ee0b7c2315d2 -r 41fc65da66f1 src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Sun Aug 18 15:29:50 2013 +0200
+++ b/src/HOL/Divides.thy	Sun Aug 18 15:29:50 2013 +0200
@@ -2122,15 +2122,18 @@
                    zero_less_mult_iff distrib_left [symmetric] 
                    zmult2_lemma_aux1 zmult2_lemma_aux2 zmult2_lemma_aux3 zmult2_lemma_aux4 mult_less_0_iff split: split_if_asm)
 
-lemma zdiv_zmult2_eq: "(0::int) < c ==> a div (b*c) = (a div b) div c"
+lemma zdiv_zmult2_eq:
+  fixes a b c :: int
+  shows "0 \<le> c \<Longrightarrow> a div (b * c) = (a div b) div c"
 apply (case_tac "b = 0", simp)
-apply (force simp add: divmod_int_rel_div_mod [THEN zmult2_lemma, THEN div_int_unique])
+apply (force simp add: le_less divmod_int_rel_div_mod [THEN zmult2_lemma, THEN div_int_unique])
 done
 
 lemma zmod_zmult2_eq:
-     "(0::int) < c ==> a mod (b*c) = b*(a div b mod c) + a mod b"
+  fixes a b c :: int
+  shows "0 \<le> c \<Longrightarrow> a mod (b * c) = b * (a div b mod c) + a mod b"
 apply (case_tac "b = 0", simp)
-apply (force simp add: divmod_int_rel_div_mod [THEN zmult2_lemma, THEN mod_int_unique])
+apply (force simp add: le_less divmod_int_rel_div_mod [THEN zmult2_lemma, THEN mod_int_unique])
 done
 
 lemma div_pos_geq:
@@ -2555,9 +2558,10 @@
   by auto
 
 instance int :: semiring_numeral_div
-  by intro_classes (auto intro: zmod_le_nonneg_dividend simp add: zmult_div_cancel
-    pos_imp_zdiv_pos_iff div_pos_pos_trivial mod_pos_pos_trivial,
-    auto intro: zmod_zmult2_eq zdiv_zmult2_eq simp add: le_less)
+  by intro_classes (auto intro: zmod_le_nonneg_dividend
+    simp add: zmult_div_cancel
+    pos_imp_zdiv_pos_iff div_pos_pos_trivial mod_pos_pos_trivial
+    zmod_zmult2_eq zdiv_zmult2_eq)
 
 
 subsubsection {* Tools setup *}