src/HOL/Parity.thy
changeset 62597 b3f2b8c906a6
parent 62083 7582b39f51ed
child 63654 f90e3926e627
     1.1 --- a/src/HOL/Parity.thy	Fri Mar 11 17:20:14 2016 +0100
     1.2 +++ b/src/HOL/Parity.thy	Sat Mar 12 22:04:52 2016 +0100
     1.3 @@ -180,6 +180,21 @@
     1.4    "odd (n :: nat) \<Longrightarrow> 0 < n"
     1.5    by (auto elim: oddE)
     1.6  
     1.7 +lemma Suc_double_not_eq_double:
     1.8 +  fixes m n :: nat
     1.9 +  shows "Suc (2 * m) \<noteq> 2 * n"
    1.10 +proof
    1.11 +  assume "Suc (2 * m) = 2 * n"
    1.12 +  moreover have "odd (Suc (2 * m))" and "even (2 * n)"
    1.13 +    by simp_all
    1.14 +  ultimately show False by simp
    1.15 +qed
    1.16 +
    1.17 +lemma double_not_eq_Suc_double:
    1.18 +  fixes m n :: nat
    1.19 +  shows "2 * m \<noteq> Suc (2 * n)"
    1.20 +  using Suc_double_not_eq_double [of n m] by simp
    1.21 +
    1.22  lemma even_diff_iff [simp]:
    1.23    fixes k l :: int
    1.24    shows "2 dvd (k - l) \<longleftrightarrow> 2 dvd (k + l)"