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
```