src/HOL/Parity.thy
 changeset 33358 3495dbba0da2 parent 33318 ddd97d9dfbfb child 35028 108662d50512
```     1.1 --- a/src/HOL/Parity.thy	Fri Oct 30 13:59:50 2009 +0100
1.2 +++ b/src/HOL/Parity.thy	Fri Oct 30 13:59:51 2009 +0100
1.3 @@ -315,42 +315,6 @@
1.4    qed
1.5  qed
1.6
1.7 -subsection {* General Lemmas About Division *}
1.8 -
1.9 -(*FIXME move to Divides.thy*)
1.10 -
1.11 -lemma Suc_times_mod_eq: "1<k ==> Suc (k * m) mod k = 1"
1.12 -apply (induct "m")
1.14 -done
1.15 -
1.16 -declare Suc_times_mod_eq [of "number_of w", standard, simp]
1.17 -
1.18 -lemma [simp]: "n div k \<le> (Suc n) div k"
1.20 -
1.21 -lemma Suc_n_div_2_gt_zero [simp]: "(0::nat) < n ==> 0 < (n + 1) div 2"
1.22 -by arith
1.23 -
1.24 -lemma div_2_gt_zero [simp]: "(1::nat) < n ==> 0 < n div 2"
1.25 -by arith
1.26 -
1.27 -  (* Potential use of algebra : Equality modulo n*)
1.28 -lemma mod_mult_self3 [simp]: "(k*n + m) mod n = m mod (n::nat)"
1.30 -
1.31 -lemma mod_mult_self4 [simp]: "Suc (k*n + m) mod n = Suc m mod n"
1.32 -proof -
1.33 -  have "Suc (k * n + m) mod n = (k * n + Suc m) mod n" by simp
1.34 -  also have "... = Suc m mod n" by (rule mod_mult_self3)
1.35 -  finally show ?thesis .
1.36 -qed
1.37 -
1.38 -lemma mod_Suc_eq_Suc_mod: "Suc m mod n = Suc (m mod n) mod n"
1.39 -apply (subst mod_Suc [of m])
1.40 -apply (subst mod_Suc [of "m mod n"], simp)
1.41 -done
1.42 -
1.43
1.44  subsection {* More Even/Odd Results *}
1.45
```