src/HOL/NumberTheory/EvenOdd.thy
changeset 14434 5f14c1207499
parent 14348 744c868ee0b7
child 14981 e73f8140af78
     1.1 --- a/src/HOL/NumberTheory/EvenOdd.thy	Fri Mar 05 07:46:07 2004 +0100
     1.2 +++ b/src/HOL/NumberTheory/EvenOdd.thy	Fri Mar 05 11:43:55 2004 +0100
     1.3 @@ -43,17 +43,7 @@
     1.4    qed;
     1.5  
     1.6  lemma even_odd_disj: "(x \<in> zOdd | x \<in> zEven)";
     1.7 -  apply (auto simp add: zOdd_def zEven_def)
     1.8 -  proof -;
     1.9 -    assume "\<forall>k. x \<noteq> 2 * k";
    1.10 -    have "0 \<le> (x mod 2) & (x mod 2) < 2";
    1.11 -      by (auto intro: pos_mod_sign pos_mod_bound)
    1.12 -    then have "x mod 2 = 0 | x mod 2 = 1" by arith
    1.13 -    moreover from prems have "x mod 2 \<noteq> 0" by auto
    1.14 -    ultimately have "x mod 2 = 1" by auto
    1.15 -    thus "\<exists>k. x = 2 * k + 1";
    1.16 -      by (insert zmod_zdiv_equality [of "x" "2"], auto)
    1.17 -  qed;
    1.18 +  by (simp add: zOdd_def zEven_def, presburger)
    1.19  
    1.20  lemma not_odd_impl_even: "~(x \<in> zOdd) ==> x \<in> zEven";
    1.21    by (insert even_odd_disj, auto)