author haftmann Fri, 30 Oct 2009 13:59:51 +0100 changeset 33358 3495dbba0da2 parent 33357 2ca60fc13c5a child 33359 8b673ae1bf39
moved some div/mod lemmas to theory Divides
 src/HOL/Parity.thy file | annotate | diff | comparison | revisions
```--- 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")
-done
-
-declare Suc_times_mod_eq [of "number_of w", standard, simp]
-
-lemma [simp]: "n div k \<le> (Suc n) div k"
-
-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)"
-
-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 *}
```