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.13 -apply (simp_all add: mod_Suc)
    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.19 -by (simp add: div_le_mono) 
    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.29 -by (simp add: mult_ac add_ac)
    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