summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Old_Number_Theory/EvenOdd.thy

changeset 61382 | efac889fccbc |

parent 58889 | 5b7a9633cfa8 |

child 61649 | 268d88ec9087 |

1.1 --- a/src/HOL/Old_Number_Theory/EvenOdd.thy Sat Oct 10 16:21:34 2015 +0200 1.2 +++ b/src/HOL/Old_Number_Theory/EvenOdd.thy Sat Oct 10 16:26:23 2015 +0200 1.3 @@ -2,7 +2,7 @@ 1.4 Authors: Jeremy Avigad, David Gray, and Adam Kramer 1.5 *) 1.6 1.7 -section {*Parity: Even and Odd Integers*} 1.8 +section \<open>Parity: Even and Odd Integers\<close> 1.9 1.10 theory EvenOdd 1.11 imports Int2 1.12 @@ -14,7 +14,7 @@ 1.13 definition zEven :: "int set" 1.14 where "zEven = {x. \<exists>k. x = 2 * k}" 1.15 1.16 -subsection {* Some useful properties about even and odd *} 1.17 +subsection \<open>Some useful properties about even and odd\<close> 1.18 1.19 lemma zOddI [intro?]: "x = 2 * k + 1 \<Longrightarrow> x \<in> zOdd" 1.20 and zOddE [elim?]: "x \<in> zOdd \<Longrightarrow> (!!k. x = 2 * k + 1 \<Longrightarrow> C) \<Longrightarrow> C" 1.21 @@ -167,11 +167,11 @@ 1.22 lemma neg_one_even_power: "[| x \<in> zEven; 0 \<le> x |] ==> (-1::int)^(nat x) = 1" 1.23 proof - 1.24 assume "x \<in> zEven" and "0 \<le> x" 1.25 - from `x \<in> zEven` obtain a where "x = 2 * a" .. 1.26 - with `0 \<le> x` have "0 \<le> a" by simp 1.27 - from `0 \<le> x` and `x = 2 * a` have "nat x = nat (2 * a)" 1.28 + from \<open>x \<in> zEven\<close> obtain a where "x = 2 * a" .. 1.29 + with \<open>0 \<le> x\<close> have "0 \<le> a" by simp 1.30 + from \<open>0 \<le> x\<close> and \<open>x = 2 * a\<close> have "nat x = nat (2 * a)" 1.31 by simp 1.32 - also from `x = 2 * a` have "nat (2 * a) = 2 * nat a" 1.33 + also from \<open>x = 2 * a\<close> have "nat (2 * a) = 2 * nat a" 1.34 by (simp add: nat_mult_distrib) 1.35 finally have "(-1::int)^nat x = (-1)^(2 * nat a)" 1.36 by simp 1.37 @@ -186,9 +186,9 @@ 1.38 lemma neg_one_odd_power: "[| x \<in> zOdd; 0 \<le> x |] ==> (-1::int)^(nat x) = -1" 1.39 proof - 1.40 assume "x \<in> zOdd" and "0 \<le> x" 1.41 - from `x \<in> zOdd` obtain a where "x = 2 * a + 1" .. 1.42 - with `0 \<le> x` have a: "0 \<le> a" by simp 1.43 - with `0 \<le> x` and `x = 2 * a + 1` have "nat x = nat (2 * a + 1)" 1.44 + from \<open>x \<in> zOdd\<close> obtain a where "x = 2 * a + 1" .. 1.45 + with \<open>0 \<le> x\<close> have a: "0 \<le> a" by simp 1.46 + with \<open>0 \<le> x\<close> and \<open>x = 2 * a + 1\<close> have "nat x = nat (2 * a + 1)" 1.47 by simp 1.48 also from a have "nat (2 * a + 1) = 2 * nat a + 1" 1.49 by (auto simp add: nat_mult_distrib nat_add_distrib) 1.50 @@ -214,8 +214,8 @@ 1.51 lemma even_div_2_l: "[| y \<in> zEven; x < y |] ==> x div 2 < y div 2" 1.52 proof - 1.53 assume "y \<in> zEven" and "x < y" 1.54 - from `y \<in> zEven` obtain k where k: "y = 2 * k" .. 1.55 - with `x < y` have "x < 2 * k" by simp 1.56 + from \<open>y \<in> zEven\<close> obtain k where k: "y = 2 * k" .. 1.57 + with \<open>x < y\<close> have "x < 2 * k" by simp 1.58 then have "x div 2 < k" by (auto simp add: div_prop1) 1.59 also have "k = (2 * k) div 2" by simp 1.60 finally have "x div 2 < 2 * k div 2" by simp