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