src/HOL/Real.thy
 changeset 63040 eb4ddd18d635 parent 62626 de25474ce728 child 63331 247eac9758dd
```     1.1 --- a/src/HOL/Real.thy	Sun Apr 24 21:31:14 2016 +0200
1.2 +++ b/src/HOL/Real.thy	Mon Apr 25 16:09:26 2016 +0200
1.3 @@ -775,7 +775,7 @@
1.4    obtain x where x: "x \<in> S" using assms(1) ..
1.5    obtain z where z: "\<forall>x\<in>S. x \<le> z" using assms(2) ..
1.6
1.7 -  def P \<equiv> "\<lambda>x. \<forall>y\<in>S. y \<le> of_rat x"
1.8 +  define P where "P x \<longleftrightarrow> (\<forall>y\<in>S. y \<le> of_rat x)" for x
1.9    obtain a where a: "\<not> P a"
1.10    proof
1.11      have "of_int \<lfloor>x - 1\<rfloor> \<le> x - 1" by (rule of_int_floor_le)
1.12 @@ -797,11 +797,11 @@
1.13      qed
1.14    qed
1.15
1.16 -  def avg \<equiv> "\<lambda>x y :: rat. x/2 + y/2"
1.17 -  def bisect \<equiv> "\<lambda>(x, y). if P (avg x y) then (x, avg x y) else (avg x y, y)"
1.18 -  def A \<equiv> "\<lambda>n. fst ((bisect ^^ n) (a, b))"
1.19 -  def B \<equiv> "\<lambda>n. snd ((bisect ^^ n) (a, b))"
1.20 -  def C \<equiv> "\<lambda>n. avg (A n) (B n)"
1.21 +  define avg where "avg x y = x/2 + y/2" for x y :: rat
1.22 +  define bisect where "bisect = (\<lambda>(x, y). if P (avg x y) then (x, avg x y) else (avg x y, y))"
1.23 +  define A where "A n = fst ((bisect ^^ n) (a, b))" for n
1.24 +  define B where "B n = snd ((bisect ^^ n) (a, b))" for n
1.25 +  define C where "C n = avg (A n) (B n)" for n
1.26    have A_0 [simp]: "A 0 = a" unfolding A_def by simp
1.27    have B_0 [simp]: "B 0 = b" unfolding B_def by simp
1.28    have A_Suc [simp]: "\<And>n. A (Suc n) = (if P (C n) then A n else C n)"
1.29 @@ -1251,8 +1251,8 @@
1.30    from \<open>x<y\<close> have "0 < y-x" by simp
1.31    with reals_Archimedean obtain q::nat
1.32      where q: "inverse (real q) < y-x" and "0 < q" by blast
1.33 -  def p \<equiv> "\<lceil>y * real q\<rceil> - 1"
1.34 -  def r \<equiv> "of_int p / real q"
1.35 +  define p where "p = \<lceil>y * real q\<rceil> - 1"
1.36 +  define r where "r = of_int p / real q"
1.37    from q have "x < y - inverse (real q)" by simp
1.38    also have "y - inverse (real q) \<le> r"
1.39      unfolding r_def p_def
```