equal
deleted
inserted
replaced
6 header {*Parity: Even and Odd Integers*} |
6 header {*Parity: Even and Odd Integers*} |
7 |
7 |
8 theory EvenOdd imports Int2 begin |
8 theory EvenOdd imports Int2 begin |
9 |
9 |
10 definition |
10 definition |
11 zOdd :: "int set" |
11 zOdd :: "int set" where |
12 "zOdd = {x. \<exists>k. x = 2 * k + 1}" |
12 "zOdd = {x. \<exists>k. x = 2 * k + 1}" |
13 zEven :: "int set" |
13 |
|
14 definition |
|
15 zEven :: "int set" where |
14 "zEven = {x. \<exists>k. x = 2 * k}" |
16 "zEven = {x. \<exists>k. x = 2 * k}" |
15 |
17 |
16 subsection {* Some useful properties about even and odd *} |
18 subsection {* Some useful properties about even and odd *} |
17 |
19 |
18 lemma zOddI [intro?]: "x = 2 * k + 1 \<Longrightarrow> x \<in> zOdd" |
20 lemma zOddI [intro?]: "x = 2 * k + 1 \<Longrightarrow> x \<in> zOdd" |