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