equal
deleted
inserted
replaced
11 definition zOdd :: "int set" |
11 definition zOdd :: "int set" |
12 where "zOdd = {x. \<exists>k. x = 2 * k + 1}" |
12 where "zOdd = {x. \<exists>k. x = 2 * k + 1}" |
13 |
13 |
14 definition zEven :: "int set" |
14 definition zEven :: "int set" |
15 where "zEven = {x. \<exists>k. x = 2 * k}" |
15 where "zEven = {x. \<exists>k. x = 2 * k}" |
|
16 |
|
17 lemma in_zEven_zOdd_iff: |
|
18 fixes k :: int |
|
19 shows "k \<in> zEven \<longleftrightarrow> even k" |
|
20 and "k \<in> zOdd \<longleftrightarrow> odd k" |
|
21 by (auto simp add: zEven_def zOdd_def elim: evenE oddE) |
|
22 |
16 |
23 |
17 subsection \<open>Some useful properties about even and odd\<close> |
24 subsection \<open>Some useful properties about even and odd\<close> |
18 |
25 |
19 lemma zOddI [intro?]: "x = 2 * k + 1 \<Longrightarrow> x \<in> zOdd" |
26 lemma zOddI [intro?]: "x = 2 * k + 1 \<Longrightarrow> x \<in> zOdd" |
20 and zOddE [elim?]: "x \<in> zOdd \<Longrightarrow> (!!k. x = 2 * k + 1 \<Longrightarrow> C) \<Longrightarrow> C" |
27 and zOddE [elim?]: "x \<in> zOdd \<Longrightarrow> (!!k. x = 2 * k + 1 \<Longrightarrow> C) \<Longrightarrow> C" |