# HG changeset patch
# User haftmann
# Date 1256907591 -3600
# Node ID 3495dbba0da2061fac8ec16a19d2d4ea7708c612
# Parent  2ca60fc13c5a550cb62638b6e558662b53cf284a
moved some div/mod lemmas to theory Divides

diff -r 2ca60fc13c5a -r 3495dbba0da2 src/HOL/Parity.thy
--- a/src/HOL/Parity.thy	Fri Oct 30 13:59:50 2009 +0100
+++ b/src/HOL/Parity.thy	Fri Oct 30 13:59:51 2009 +0100
@@ -315,42 +315,6 @@
   qed
 qed
 
-subsection {* General Lemmas About Division *}
-
-(*FIXME move to Divides.thy*)
-
-lemma Suc_times_mod_eq: "1<k ==> Suc (k * m) mod k = 1" 
-apply (induct "m")
-apply (simp_all add: mod_Suc)
-done
-
-declare Suc_times_mod_eq [of "number_of w", standard, simp]
-
-lemma [simp]: "n div k \<le> (Suc n) div k"
-by (simp add: div_le_mono) 
-
-lemma Suc_n_div_2_gt_zero [simp]: "(0::nat) < n ==> 0 < (n + 1) div 2"
-by arith
-
-lemma div_2_gt_zero [simp]: "(1::nat) < n ==> 0 < n div 2" 
-by arith
-
-  (* Potential use of algebra : Equality modulo n*)
-lemma mod_mult_self3 [simp]: "(k*n + m) mod n = m mod (n::nat)"
-by (simp add: mult_ac add_ac)
-
-lemma mod_mult_self4 [simp]: "Suc (k*n + m) mod n = Suc m mod n"
-proof -
-  have "Suc (k * n + m) mod n = (k * n + Suc m) mod n" by simp
-  also have "... = Suc m mod n" by (rule mod_mult_self3) 
-  finally show ?thesis .
-qed
-
-lemma mod_Suc_eq_Suc_mod: "Suc m mod n = Suc (m mod n) mod n"
-apply (subst mod_Suc [of m]) 
-apply (subst mod_Suc [of "m mod n"], simp) 
-done
-
 
 subsection {* More Even/Odd Results *}