src/HOL/Divides.thy
changeset 39489 8bb7f32a3a08
parent 38715 6513ea67d95d
child 41550 efa734d9b221
     1.1 --- a/src/HOL/Divides.thy	Fri Sep 17 08:41:07 2010 +0200
     1.2 +++ b/src/HOL/Divides.thy	Fri Sep 17 16:15:33 2010 +0200
     1.3 @@ -2183,6 +2183,18 @@
     1.4  done
     1.5  
     1.6  
     1.7 +lemma zdiv_eq_0_iff:
     1.8 + "(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")
     1.9 +proof
    1.10 +  assume ?L
    1.11 +  have "?L \<longrightarrow> ?R" by (rule split_zdiv[THEN iffD2]) simp
    1.12 +  with `?L` show ?R by blast
    1.13 +next
    1.14 +  assume ?R thus ?L
    1.15 +    by(auto simp: div_pos_pos_trivial div_neg_neg_trivial)
    1.16 +qed
    1.17 +
    1.18 +
    1.19  subsubsection{*Quotients of Signs*}
    1.20  
    1.21  lemma div_neg_pos_less0: "[| a < (0::int);  0 < b |] ==> a div b < 0"
    1.22 @@ -2220,6 +2232,11 @@
    1.23  lemma pos_imp_zdiv_neg_iff: "(0::int) < b ==> (a div b < 0) = (a < 0)"
    1.24  by (simp add: linorder_not_le [symmetric] pos_imp_zdiv_nonneg_iff)
    1.25  
    1.26 +lemma pos_imp_zdiv_pos_iff:
    1.27 +  "0<k \<Longrightarrow> 0 < (i::int) div k \<longleftrightarrow> k \<le> i"
    1.28 +using pos_imp_zdiv_nonneg_iff[of k i] zdiv_eq_0_iff[of i k]
    1.29 +by arith
    1.30 +
    1.31  (*Again the law fails for \<le>: consider a = -1, b = -2 when a div b = 0*)
    1.32  lemma neg_imp_zdiv_neg_iff: "b < (0::int) ==> (a div b < 0) = (0 < a)"
    1.33  by (simp add: linorder_not_le [symmetric] neg_imp_zdiv_nonneg_iff)
    1.34 @@ -2235,6 +2252,12 @@
    1.35  done
    1.36  
    1.37  
    1.38 +lemma zmod_le_nonneg_dividend: "(m::int) \<ge> 0 ==> m mod k \<le> m"
    1.39 +apply (rule split_zmod[THEN iffD2])
    1.40 +apply(fastsimp dest: q_pos_lemma intro: split_mult_pos_le)
    1.41 +done
    1.42 +
    1.43 +
    1.44  subsubsection {* The Divides Relation *}
    1.45  
    1.46  lemmas zdvd_iff_zmod_eq_0_number_of [simp] =