# HG changeset patch
# User nipkow
# Date 1258698216 -3600
# Node ID 39b494e8c055643136836cd69be533983943bfb1
# Parent  0a0d6d79d984fe99052b8642d51e51b07abaf7a5
added lemma

diff -r 0a0d6d79d984 -r 39b494e8c055 src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Thu Nov 19 08:19:57 2009 +0100
+++ b/src/HOL/Divides.thy	Fri Nov 20 07:23:36 2009 +0100
@@ -2157,6 +2157,10 @@
 lemma div_nonpos_pos_le0: "[| (a::int) \<le> 0; b > 0 |] ==> a div b \<le> 0"
 by (drule zdiv_mono1, auto)
 
+text{* Now for some equivalences of the form @{text"a div b >=< 0 \<longleftrightarrow> \<dots>"}
+conditional upon the sign of @{text a} or @{text b}. There are many more.
+They should all be simp rules unless that causes too much search. *}
+
 lemma pos_imp_zdiv_nonneg_iff: "(0::int) < b ==> (0 \<le> a div b) = (0 \<le> a)"
 apply auto
 apply (drule_tac [2] zdiv_mono1)
@@ -2166,7 +2170,7 @@
 done
 
 lemma neg_imp_zdiv_nonneg_iff:
-     "b < (0::int) ==> (0 \<le> a div b) = (a \<le> (0::int))"
+  "b < (0::int) ==> (0 \<le> a div b) = (a \<le> (0::int))"
 apply (subst zdiv_zminus_zminus [symmetric])
 apply (subst pos_imp_zdiv_nonneg_iff, auto)
 done
@@ -2179,6 +2183,16 @@
 lemma neg_imp_zdiv_neg_iff: "b < (0::int) ==> (a div b < 0) = (0 < a)"
 by (simp add: linorder_not_le [symmetric] neg_imp_zdiv_nonneg_iff)
 
+lemma nonneg1_imp_zdiv_pos_iff:
+  "(0::int) <= a \<Longrightarrow> (a div b > 0) = (a >= b & b>0)"
+apply rule
+ apply rule
+  using div_pos_pos_trivial[of a b]apply arith
+ apply(cases "b=0")apply simp
+ using div_nonneg_neg_le0[of a b]apply arith
+using int_one_le_iff_zero_less[of "a div b"] zdiv_mono1[of b a b]apply simp
+done
+
 
 subsubsection {* The Divides Relation *}