# HG changeset patch
# User nipkow
# Date 1284732933 -7200
# Node ID 8bb7f32a3a085961fcf066f2753b38e110d22c2b
# Parent  1c37d19e3d58f0d2856a75168b094d15d72c0c04
added lemmas

diff -r 1c37d19e3d58 -r 8bb7f32a3a08 src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Fri Sep 17 08:41:07 2010 +0200
+++ b/src/HOL/Divides.thy	Fri Sep 17 16:15:33 2010 +0200
@@ -2183,6 +2183,18 @@
 done
 
 
+lemma zdiv_eq_0_iff:
+ "(i::int) div k = 0 \<longleftrightarrow> k=0 \<or> 0\<le>i \<and> i<k \<or> i\<le>0 \<and> k<i" (is "?L = ?R")
+proof
+  assume ?L
+  have "?L \<longrightarrow> ?R" by (rule split_zdiv[THEN iffD2]) simp
+  with `?L` show ?R by blast
+next
+  assume ?R thus ?L
+    by(auto simp: div_pos_pos_trivial div_neg_neg_trivial)
+qed
+
+
 subsubsection{*Quotients of Signs*}
 
 lemma div_neg_pos_less0: "[| a < (0::int);  0 < b |] ==> a div b < 0"
@@ -2220,6 +2232,11 @@
 lemma pos_imp_zdiv_neg_iff: "(0::int) < b ==> (a div b < 0) = (a < 0)"
 by (simp add: linorder_not_le [symmetric] pos_imp_zdiv_nonneg_iff)
 
+lemma pos_imp_zdiv_pos_iff:
+  "0<k \<Longrightarrow> 0 < (i::int) div k \<longleftrightarrow> k \<le> i"
+using pos_imp_zdiv_nonneg_iff[of k i] zdiv_eq_0_iff[of i k]
+by arith
+
 (*Again the law fails for \<le>: consider a = -1, b = -2 when a div b = 0*)
 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)
@@ -2235,6 +2252,12 @@
 done
 
 
+lemma zmod_le_nonneg_dividend: "(m::int) \<ge> 0 ==> m mod k \<le> m"
+apply (rule split_zmod[THEN iffD2])
+apply(fastsimp dest: q_pos_lemma intro: split_mult_pos_le)
+done
+
+
 subsubsection {* The Divides Relation *}
 
 lemmas zdvd_iff_zmod_eq_0_number_of [simp] =