misc tuning and modernization;
authorwenzelm
Thu Jun 23 23:08:37 2016 +0200 (2016-06-23)
changeset 63353176d1f408696
parent 63352 4eaf35781b23
child 63354 6038ba2687cf
misc tuning and modernization;
src/HOL/Real.thy
     1.1 --- a/src/HOL/Real.thy	Thu Jun 23 11:01:14 2016 +0200
     1.2 +++ b/src/HOL/Real.thy	Thu Jun 23 23:08:37 2016 +0200
     1.3 @@ -20,28 +20,22 @@
     1.4    construction using Dedekind cuts.
     1.5  \<close>
     1.6  
     1.7 +
     1.8  subsection \<open>Preliminary lemmas\<close>
     1.9  
    1.10 -lemma inj_add_left [simp]:
    1.11 -  fixes x :: "'a::cancel_semigroup_add" shows "inj (op+ x)"
    1.12 -by (meson add_left_imp_eq injI)
    1.13 +lemma inj_add_left [simp]: "inj (op + x)" for x :: "'a::cancel_semigroup_add"
    1.14 +  by (meson add_left_imp_eq injI)
    1.15  
    1.16 -lemma inj_mult_left [simp]: "inj (op* x) \<longleftrightarrow> x \<noteq> (0::'a::idom)"
    1.17 +lemma inj_mult_left [simp]: "inj (op * x) \<longleftrightarrow> x \<noteq> 0" for x :: "'a::idom"
    1.18    by (metis injI mult_cancel_left the_inv_f_f zero_neq_one)
    1.19  
    1.20 -lemma add_diff_add:
    1.21 -  fixes a b c d :: "'a::ab_group_add"
    1.22 -  shows "(a + c) - (b + d) = (a - b) + (c - d)"
    1.23 +lemma add_diff_add: "(a + c) - (b + d) = (a - b) + (c - d)" for a b c d :: "'a::ab_group_add"
    1.24    by simp
    1.25  
    1.26 -lemma minus_diff_minus:
    1.27 -  fixes a b :: "'a::ab_group_add"
    1.28 -  shows "- a - - b = - (a - b)"
    1.29 +lemma minus_diff_minus: "- a - - b = - (a - b)" for a b :: "'a::ab_group_add"
    1.30    by simp
    1.31  
    1.32 -lemma mult_diff_mult:
    1.33 -  fixes x y a b :: "'a::ring"
    1.34 -  shows "(x * y - a * b) = x * (y - b) + (x - a) * b"
    1.35 +lemma mult_diff_mult: "(x * y - a * b) = x * (y - b) + (x - a) * b" for x y a b :: "'a::ring"
    1.36    by (simp add: algebra_simps)
    1.37  
    1.38  lemma inverse_diff_inverse:
    1.39 @@ -54,38 +48,41 @@
    1.40    fixes r :: rat assumes r: "0 < r"
    1.41    obtains s t where "0 < s" and "0 < t" and "r = s + t"
    1.42  proof
    1.43 -    from r show "0 < r/2" by simp
    1.44 -    from r show "0 < r/2" by simp
    1.45 -    show "r = r/2 + r/2" by simp
    1.46 +  from r show "0 < r/2" by simp
    1.47 +  from r show "0 < r/2" by simp
    1.48 +  show "r = r/2 + r/2" by simp
    1.49  qed
    1.50  
    1.51 +
    1.52  subsection \<open>Sequences that converge to zero\<close>
    1.53  
    1.54 -definition
    1.55 -  vanishes :: "(nat \<Rightarrow> rat) \<Rightarrow> bool"
    1.56 -where
    1.57 -  "vanishes X = (\<forall>r>0. \<exists>k. \<forall>n\<ge>k. \<bar>X n\<bar> < r)"
    1.58 +definition vanishes :: "(nat \<Rightarrow> rat) \<Rightarrow> bool"
    1.59 +  where "vanishes X \<longleftrightarrow> (\<forall>r>0. \<exists>k. \<forall>n\<ge>k. \<bar>X n\<bar> < r)"
    1.60  
    1.61  lemma vanishesI: "(\<And>r. 0 < r \<Longrightarrow> \<exists>k. \<forall>n\<ge>k. \<bar>X n\<bar> < r) \<Longrightarrow> vanishes X"
    1.62    unfolding vanishes_def by simp
    1.63  
    1.64 -lemma vanishesD: "\<lbrakk>vanishes X; 0 < r\<rbrakk> \<Longrightarrow> \<exists>k. \<forall>n\<ge>k. \<bar>X n\<bar> < r"
    1.65 +lemma vanishesD: "vanishes X \<Longrightarrow> 0 < r \<Longrightarrow> \<exists>k. \<forall>n\<ge>k. \<bar>X n\<bar> < r"
    1.66    unfolding vanishes_def by simp
    1.67  
    1.68  lemma vanishes_const [simp]: "vanishes (\<lambda>n. c) \<longleftrightarrow> c = 0"
    1.69    unfolding vanishes_def
    1.70 -  apply (cases "c = 0", auto)
    1.71 -  apply (rule exI [where x="\<bar>c\<bar>"], auto)
    1.72 +  apply (cases "c = 0")
    1.73 +  apply auto
    1.74 +  apply (rule exI [where x = "\<bar>c\<bar>"])
    1.75 +  apply auto
    1.76    done
    1.77  
    1.78  lemma vanishes_minus: "vanishes X \<Longrightarrow> vanishes (\<lambda>n. - X n)"
    1.79    unfolding vanishes_def by simp
    1.80  
    1.81  lemma vanishes_add:
    1.82 -  assumes X: "vanishes X" and Y: "vanishes Y"
    1.83 +  assumes X: "vanishes X"
    1.84 +    and Y: "vanishes Y"
    1.85    shows "vanishes (\<lambda>n. X n + Y n)"
    1.86  proof (rule vanishesI)
    1.87 -  fix r :: rat assume "0 < r"
    1.88 +  fix r :: rat
    1.89 +  assume "0 < r"
    1.90    then obtain s t where s: "0 < s" and t: "0 < t" and r: "r = s + t"
    1.91      by (rule obtain_pos_sum)
    1.92    obtain i where i: "\<forall>n\<ge>i. \<bar>X n\<bar> < s"
    1.93 @@ -93,26 +90,28 @@
    1.94    obtain j where j: "\<forall>n\<ge>j. \<bar>Y n\<bar> < t"
    1.95      using vanishesD [OF Y t] ..
    1.96    have "\<forall>n\<ge>max i j. \<bar>X n + Y n\<bar> < r"
    1.97 -  proof (clarsimp)
    1.98 -    fix n assume n: "i \<le> n" "j \<le> n"
    1.99 +  proof clarsimp
   1.100 +    fix n
   1.101 +    assume n: "i \<le> n" "j \<le> n"
   1.102      have "\<bar>X n + Y n\<bar> \<le> \<bar>X n\<bar> + \<bar>Y n\<bar>" by (rule abs_triangle_ineq)
   1.103      also have "\<dots> < s + t" by (simp add: add_strict_mono i j n)
   1.104      finally show "\<bar>X n + Y n\<bar> < r" unfolding r .
   1.105    qed
   1.106 -  thus "\<exists>k. \<forall>n\<ge>k. \<bar>X n + Y n\<bar> < r" ..
   1.107 +  then show "\<exists>k. \<forall>n\<ge>k. \<bar>X n + Y n\<bar> < r" ..
   1.108  qed
   1.109  
   1.110  lemma vanishes_diff:
   1.111 -  assumes X: "vanishes X" and Y: "vanishes Y"
   1.112 +  assumes "vanishes X" "vanishes Y"
   1.113    shows "vanishes (\<lambda>n. X n - Y n)"
   1.114 -  unfolding diff_conv_add_uminus by (intro vanishes_add vanishes_minus X Y)
   1.115 +  unfolding diff_conv_add_uminus by (intro vanishes_add vanishes_minus assms)
   1.116  
   1.117  lemma vanishes_mult_bounded:
   1.118    assumes X: "\<exists>a>0. \<forall>n. \<bar>X n\<bar> < a"
   1.119    assumes Y: "vanishes (\<lambda>n. Y n)"
   1.120    shows "vanishes (\<lambda>n. X n * Y n)"
   1.121  proof (rule vanishesI)
   1.122 -  fix r :: rat assume r: "0 < r"
   1.123 +  fix r :: rat
   1.124 +  assume r: "0 < r"
   1.125    obtain a where a: "0 < a" "\<forall>n. \<bar>X n\<bar> < a"
   1.126      using X by blast
   1.127    obtain b where b: "0 < b" "r = a * b"
   1.128 @@ -124,22 +123,19 @@
   1.129      using vanishesD [OF Y b(1)] ..
   1.130    have "\<forall>n\<ge>k. \<bar>X n * Y n\<bar> < r"
   1.131      by (simp add: b(2) abs_mult mult_strict_mono' a k)
   1.132 -  thus "\<exists>k. \<forall>n\<ge>k. \<bar>X n * Y n\<bar> < r" ..
   1.133 +  then show "\<exists>k. \<forall>n\<ge>k. \<bar>X n * Y n\<bar> < r" ..
   1.134  qed
   1.135  
   1.136 +
   1.137  subsection \<open>Cauchy sequences\<close>
   1.138  
   1.139 -definition
   1.140 -  cauchy :: "(nat \<Rightarrow> rat) \<Rightarrow> bool"
   1.141 -where
   1.142 -  "cauchy X \<longleftrightarrow> (\<forall>r>0. \<exists>k. \<forall>m\<ge>k. \<forall>n\<ge>k. \<bar>X m - X n\<bar> < r)"
   1.143 +definition cauchy :: "(nat \<Rightarrow> rat) \<Rightarrow> bool"
   1.144 +  where "cauchy X \<longleftrightarrow> (\<forall>r>0. \<exists>k. \<forall>m\<ge>k. \<forall>n\<ge>k. \<bar>X m - X n\<bar> < r)"
   1.145  
   1.146 -lemma cauchyI:
   1.147 -  "(\<And>r. 0 < r \<Longrightarrow> \<exists>k. \<forall>m\<ge>k. \<forall>n\<ge>k. \<bar>X m - X n\<bar> < r) \<Longrightarrow> cauchy X"
   1.148 +lemma cauchyI: "(\<And>r. 0 < r \<Longrightarrow> \<exists>k. \<forall>m\<ge>k. \<forall>n\<ge>k. \<bar>X m - X n\<bar> < r) \<Longrightarrow> cauchy X"
   1.149    unfolding cauchy_def by simp
   1.150  
   1.151 -lemma cauchyD:
   1.152 -  "\<lbrakk>cauchy X; 0 < r\<rbrakk> \<Longrightarrow> \<exists>k. \<forall>m\<ge>k. \<forall>n\<ge>k. \<bar>X m - X n\<bar> < r"
   1.153 +lemma cauchyD: "cauchy X \<Longrightarrow> 0 < r \<Longrightarrow> \<exists>k. \<forall>m\<ge>k. \<forall>n\<ge>k. \<bar>X m - X n\<bar> < r"
   1.154    unfolding cauchy_def by simp
   1.155  
   1.156  lemma cauchy_const [simp]: "cauchy (\<lambda>n. x)"
   1.157 @@ -149,7 +145,8 @@
   1.158    assumes X: "cauchy X" and Y: "cauchy Y"
   1.159    shows "cauchy (\<lambda>n. X n + Y n)"
   1.160  proof (rule cauchyI)
   1.161 -  fix r :: rat assume "0 < r"
   1.162 +  fix r :: rat
   1.163 +  assume "0 < r"
   1.164    then obtain s t where s: "0 < s" and t: "0 < t" and r: "r = s + t"
   1.165      by (rule obtain_pos_sum)
   1.166    obtain i where i: "\<forall>m\<ge>i. \<forall>n\<ge>i. \<bar>X m - X n\<bar> < s"
   1.167 @@ -157,30 +154,32 @@
   1.168    obtain j where j: "\<forall>m\<ge>j. \<forall>n\<ge>j. \<bar>Y m - Y n\<bar> < t"
   1.169      using cauchyD [OF Y t] ..
   1.170    have "\<forall>m\<ge>max i j. \<forall>n\<ge>max i j. \<bar>(X m + Y m) - (X n + Y n)\<bar> < r"
   1.171 -  proof (clarsimp)
   1.172 -    fix m n assume *: "i \<le> m" "j \<le> m" "i \<le> n" "j \<le> n"
   1.173 +  proof clarsimp
   1.174 +    fix m n
   1.175 +    assume *: "i \<le> m" "j \<le> m" "i \<le> n" "j \<le> n"
   1.176      have "\<bar>(X m + Y m) - (X n + Y n)\<bar> \<le> \<bar>X m - X n\<bar> + \<bar>Y m - Y n\<bar>"
   1.177        unfolding add_diff_add by (rule abs_triangle_ineq)
   1.178      also have "\<dots> < s + t"
   1.179 -      by (rule add_strict_mono, simp_all add: i j *)
   1.180 -    finally show "\<bar>(X m + Y m) - (X n + Y n)\<bar> < r" unfolding r .
   1.181 +      by (rule add_strict_mono) (simp_all add: i j *)
   1.182 +    finally show "\<bar>(X m + Y m) - (X n + Y n)\<bar> < r" by (simp only: r)
   1.183    qed
   1.184 -  thus "\<exists>k. \<forall>m\<ge>k. \<forall>n\<ge>k. \<bar>(X m + Y m) - (X n + Y n)\<bar> < r" ..
   1.185 +  then show "\<exists>k. \<forall>m\<ge>k. \<forall>n\<ge>k. \<bar>(X m + Y m) - (X n + Y n)\<bar> < r" ..
   1.186  qed
   1.187  
   1.188  lemma cauchy_minus [simp]:
   1.189    assumes X: "cauchy X"
   1.190    shows "cauchy (\<lambda>n. - X n)"
   1.191 -using assms unfolding cauchy_def
   1.192 -unfolding minus_diff_minus abs_minus_cancel .
   1.193 +  using assms unfolding cauchy_def
   1.194 +  unfolding minus_diff_minus abs_minus_cancel .
   1.195  
   1.196  lemma cauchy_diff [simp]:
   1.197 -  assumes X: "cauchy X" and Y: "cauchy Y"
   1.198 +  assumes "cauchy X" "cauchy Y"
   1.199    shows "cauchy (\<lambda>n. X n - Y n)"
   1.200    using assms unfolding diff_conv_add_uminus by (simp del: add_uminus_conv_diff)
   1.201  
   1.202  lemma cauchy_imp_bounded:
   1.203 -  assumes "cauchy X" shows "\<exists>b>0. \<forall>n. \<bar>X n\<bar> < b"
   1.204 +  assumes "cauchy X"
   1.205 +  shows "\<exists>b>0. \<forall>n. \<bar>X n\<bar> < b"
   1.206  proof -
   1.207    obtain k where k: "\<forall>m\<ge>k. \<forall>n\<ge>k. \<bar>X m - X n\<bar> < 1"
   1.208      using cauchyD [OF assms zero_less_one] ..
   1.209 @@ -189,21 +188,21 @@
   1.210      have "0 \<le> \<bar>X 0\<bar>" by simp
   1.211      also have "\<bar>X 0\<bar> \<le> Max (abs ` X ` {..k})" by simp
   1.212      finally have "0 \<le> Max (abs ` X ` {..k})" .
   1.213 -    thus "0 < Max (abs ` X ` {..k}) + 1" by simp
   1.214 +    then show "0 < Max (abs ` X ` {..k}) + 1" by simp
   1.215    next
   1.216      fix n :: nat
   1.217      show "\<bar>X n\<bar> < Max (abs ` X ` {..k}) + 1"
   1.218      proof (rule linorder_le_cases)
   1.219        assume "n \<le> k"
   1.220 -      hence "\<bar>X n\<bar> \<le> Max (abs ` X ` {..k})" by simp
   1.221 -      thus "\<bar>X n\<bar> < Max (abs ` X ` {..k}) + 1" by simp
   1.222 +      then have "\<bar>X n\<bar> \<le> Max (abs ` X ` {..k})" by simp
   1.223 +      then show "\<bar>X n\<bar> < Max (abs ` X ` {..k}) + 1" by simp
   1.224      next
   1.225        assume "k \<le> n"
   1.226        have "\<bar>X n\<bar> = \<bar>X k + (X n - X k)\<bar>" by simp
   1.227        also have "\<bar>X k + (X n - X k)\<bar> \<le> \<bar>X k\<bar> + \<bar>X n - X k\<bar>"
   1.228          by (rule abs_triangle_ineq)
   1.229        also have "\<dots> < Max (abs ` X ` {..k}) + 1"
   1.230 -        by (rule add_le_less_mono, simp, simp add: k \<open>k \<le> n\<close>)
   1.231 +        by (rule add_le_less_mono) (simp_all add: k \<open>k \<le> n\<close>)
   1.232        finally show "\<bar>X n\<bar> < Max (abs ` X ` {..k}) + 1" .
   1.233      qed
   1.234    qed
   1.235 @@ -232,8 +231,9 @@
   1.236    obtain j where j: "\<forall>m\<ge>j. \<forall>n\<ge>j. \<bar>Y m - Y n\<bar> < t"
   1.237      using cauchyD [OF Y t] ..
   1.238    have "\<forall>m\<ge>max i j. \<forall>n\<ge>max i j. \<bar>X m * Y m - X n * Y n\<bar> < r"
   1.239 -  proof (clarsimp)
   1.240 -    fix m n assume *: "i \<le> m" "j \<le> m" "i \<le> n" "j \<le> n"
   1.241 +  proof clarsimp
   1.242 +    fix m n
   1.243 +    assume *: "i \<le> m" "j \<le> m" "i \<le> n" "j \<le> n"
   1.244      have "\<bar>X m * Y m - X n * Y n\<bar> = \<bar>X m * (Y m - Y n) + (X m - X n) * Y n\<bar>"
   1.245        unfolding mult_diff_mult ..
   1.246      also have "\<dots> \<le> \<bar>X m * (Y m - Y n)\<bar> + \<bar>(X m - X n) * Y n\<bar>"
   1.247 @@ -242,9 +242,9 @@
   1.248        unfolding abs_mult ..
   1.249      also have "\<dots> < a * t + s * b"
   1.250        by (simp_all add: add_strict_mono mult_strict_mono' a b i j *)
   1.251 -    finally show "\<bar>X m * Y m - X n * Y n\<bar> < r" unfolding r .
   1.252 +    finally show "\<bar>X m * Y m - X n * Y n\<bar> < r" by (simp only: r)
   1.253    qed
   1.254 -  thus "\<exists>k. \<forall>m\<ge>k. \<forall>n\<ge>k. \<bar>X m * Y m - X n * Y n\<bar> < r" ..
   1.255 +  then show "\<exists>k. \<forall>m\<ge>k. \<forall>n\<ge>k. \<bar>X m * Y m - X n * Y n\<bar> < r" ..
   1.256  qed
   1.257  
   1.258  lemma cauchy_not_vanishes_cases:
   1.259 @@ -264,10 +264,10 @@
   1.260      using i \<open>i \<le> k\<close> by auto
   1.261    have "X k \<le> - r \<or> r \<le> X k"
   1.262      using \<open>r \<le> \<bar>X k\<bar>\<close> by auto
   1.263 -  hence "(\<forall>n\<ge>k. t < - X n) \<or> (\<forall>n\<ge>k. t < X n)"
   1.264 +  then have "(\<forall>n\<ge>k. t < - X n) \<or> (\<forall>n\<ge>k. t < X n)"
   1.265      unfolding \<open>r = s + t\<close> using k by auto
   1.266 -  hence "\<exists>k. (\<forall>n\<ge>k. t < - X n) \<or> (\<forall>n\<ge>k. t < X n)" ..
   1.267 -  thus "\<exists>t>0. \<exists>k. (\<forall>n\<ge>k. t < - X n) \<or> (\<forall>n\<ge>k. t < X n)"
   1.268 +  then have "\<exists>k. (\<forall>n\<ge>k. t < - X n) \<or> (\<forall>n\<ge>k. t < X n)" ..
   1.269 +  then show "\<exists>t>0. \<exists>k. (\<forall>n\<ge>k. t < - X n) \<or> (\<forall>n\<ge>k. t < X n)"
   1.270      using t by auto
   1.271  qed
   1.272  
   1.273 @@ -275,15 +275,21 @@
   1.274    assumes X: "cauchy X"
   1.275    assumes nz: "\<not> vanishes X"
   1.276    shows "\<exists>b>0. \<exists>k. \<forall>n\<ge>k. b < \<bar>X n\<bar>"
   1.277 -using cauchy_not_vanishes_cases [OF assms]
   1.278 -by clarify (rule exI, erule conjI, rule_tac x=k in exI, auto)
   1.279 +  using cauchy_not_vanishes_cases [OF assms]
   1.280 +  apply clarify
   1.281 +  apply (rule exI)
   1.282 +  apply (erule conjI)
   1.283 +  apply (rule_tac x = k in exI)
   1.284 +  apply auto
   1.285 +  done
   1.286  
   1.287  lemma cauchy_inverse [simp]:
   1.288    assumes X: "cauchy X"
   1.289    assumes nz: "\<not> vanishes X"
   1.290    shows "cauchy (\<lambda>n. inverse (X n))"
   1.291  proof (rule cauchyI)
   1.292 -  fix r :: rat assume "0 < r"
   1.293 +  fix r :: rat
   1.294 +  assume "0 < r"
   1.295    obtain b i where b: "0 < b" and i: "\<forall>n\<ge>i. b < \<bar>X n\<bar>"
   1.296      using cauchy_not_vanishes [OF X nz] by blast
   1.297    from b i have nz: "\<forall>n\<ge>i. X n \<noteq> 0" by auto
   1.298 @@ -296,84 +302,84 @@
   1.299    obtain j where j: "\<forall>m\<ge>j. \<forall>n\<ge>j. \<bar>X m - X n\<bar> < s"
   1.300      using cauchyD [OF X s] ..
   1.301    have "\<forall>m\<ge>max i j. \<forall>n\<ge>max i j. \<bar>inverse (X m) - inverse (X n)\<bar> < r"
   1.302 -  proof (clarsimp)
   1.303 -    fix m n assume *: "i \<le> m" "j \<le> m" "i \<le> n" "j \<le> n"
   1.304 -    have "\<bar>inverse (X m) - inverse (X n)\<bar> =
   1.305 -          inverse \<bar>X m\<bar> * \<bar>X m - X n\<bar> * inverse \<bar>X n\<bar>"
   1.306 +  proof clarsimp
   1.307 +    fix m n
   1.308 +    assume *: "i \<le> m" "j \<le> m" "i \<le> n" "j \<le> n"
   1.309 +    have "\<bar>inverse (X m) - inverse (X n)\<bar> = inverse \<bar>X m\<bar> * \<bar>X m - X n\<bar> * inverse \<bar>X n\<bar>"
   1.310        by (simp add: inverse_diff_inverse nz * abs_mult)
   1.311      also have "\<dots> < inverse b * s * inverse b"
   1.312 -      by (simp add: mult_strict_mono less_imp_inverse_less
   1.313 -                    i j b * s)
   1.314 -    finally show "\<bar>inverse (X m) - inverse (X n)\<bar> < r" unfolding r .
   1.315 +      by (simp add: mult_strict_mono less_imp_inverse_less i j b * s)
   1.316 +    finally show "\<bar>inverse (X m) - inverse (X n)\<bar> < r" by (simp only: r)
   1.317    qed
   1.318 -  thus "\<exists>k. \<forall>m\<ge>k. \<forall>n\<ge>k. \<bar>inverse (X m) - inverse (X n)\<bar> < r" ..
   1.319 +  then show "\<exists>k. \<forall>m\<ge>k. \<forall>n\<ge>k. \<bar>inverse (X m) - inverse (X n)\<bar> < r" ..
   1.320  qed
   1.321  
   1.322  lemma vanishes_diff_inverse:
   1.323    assumes X: "cauchy X" "\<not> vanishes X"
   1.324 -  assumes Y: "cauchy Y" "\<not> vanishes Y"
   1.325 -  assumes XY: "vanishes (\<lambda>n. X n - Y n)"
   1.326 +    and Y: "cauchy Y" "\<not> vanishes Y"
   1.327 +    and XY: "vanishes (\<lambda>n. X n - Y n)"
   1.328    shows "vanishes (\<lambda>n. inverse (X n) - inverse (Y n))"
   1.329  proof (rule vanishesI)
   1.330 -  fix r :: rat assume r: "0 < r"
   1.331 +  fix r :: rat
   1.332 +  assume r: "0 < r"
   1.333    obtain a i where a: "0 < a" and i: "\<forall>n\<ge>i. a < \<bar>X n\<bar>"
   1.334      using cauchy_not_vanishes [OF X] by blast
   1.335    obtain b j where b: "0 < b" and j: "\<forall>n\<ge>j. b < \<bar>Y n\<bar>"
   1.336      using cauchy_not_vanishes [OF Y] by blast
   1.337    obtain s where s: "0 < s" and "inverse a * s * inverse b = r"
   1.338    proof
   1.339 -    show "0 < a * r * b"
   1.340 -      using a r b by simp
   1.341 -    show "inverse a * (a * r * b) * inverse b = r"
   1.342 -      using a r b by simp
   1.343 +    show "0 < a * r * b" using a r b by simp
   1.344 +    show "inverse a * (a * r * b) * inverse b = r" using a r b by simp
   1.345    qed
   1.346    obtain k where k: "\<forall>n\<ge>k. \<bar>X n - Y n\<bar> < s"
   1.347      using vanishesD [OF XY s] ..
   1.348    have "\<forall>n\<ge>max (max i j) k. \<bar>inverse (X n) - inverse (Y n)\<bar> < r"
   1.349 -  proof (clarsimp)
   1.350 -    fix n assume n: "i \<le> n" "j \<le> n" "k \<le> n"
   1.351 -    have "X n \<noteq> 0" and "Y n \<noteq> 0"
   1.352 -      using i j a b n by auto
   1.353 -    hence "\<bar>inverse (X n) - inverse (Y n)\<bar> =
   1.354 -        inverse \<bar>X n\<bar> * \<bar>X n - Y n\<bar> * inverse \<bar>Y n\<bar>"
   1.355 +  proof clarsimp
   1.356 +    fix n
   1.357 +    assume n: "i \<le> n" "j \<le> n" "k \<le> n"
   1.358 +    with i j a b have "X n \<noteq> 0" and "Y n \<noteq> 0"
   1.359 +      by auto
   1.360 +    then have "\<bar>inverse (X n) - inverse (Y n)\<bar> = inverse \<bar>X n\<bar> * \<bar>X n - Y n\<bar> * inverse \<bar>Y n\<bar>"
   1.361        by (simp add: inverse_diff_inverse abs_mult)
   1.362      also have "\<dots> < inverse a * s * inverse b"
   1.363 -      apply (intro mult_strict_mono' less_imp_inverse_less)
   1.364 -      apply (simp_all add: a b i j k n)
   1.365 -      done
   1.366 +      by (intro mult_strict_mono' less_imp_inverse_less) (simp_all add: a b i j k n)
   1.367      also note \<open>inverse a * s * inverse b = r\<close>
   1.368      finally show "\<bar>inverse (X n) - inverse (Y n)\<bar> < r" .
   1.369    qed
   1.370 -  thus "\<exists>k. \<forall>n\<ge>k. \<bar>inverse (X n) - inverse (Y n)\<bar> < r" ..
   1.371 +  then show "\<exists>k. \<forall>n\<ge>k. \<bar>inverse (X n) - inverse (Y n)\<bar> < r" ..
   1.372  qed
   1.373  
   1.374 +
   1.375  subsection \<open>Equivalence relation on Cauchy sequences\<close>
   1.376  
   1.377  definition realrel :: "(nat \<Rightarrow> rat) \<Rightarrow> (nat \<Rightarrow> rat) \<Rightarrow> bool"
   1.378    where "realrel = (\<lambda>X Y. cauchy X \<and> cauchy Y \<and> vanishes (\<lambda>n. X n - Y n))"
   1.379  
   1.380 -lemma realrelI [intro?]:
   1.381 -  assumes "cauchy X" and "cauchy Y" and "vanishes (\<lambda>n. X n - Y n)"
   1.382 -  shows "realrel X Y"
   1.383 -  using assms unfolding realrel_def by simp
   1.384 +lemma realrelI [intro?]: "cauchy X \<Longrightarrow> cauchy Y \<Longrightarrow> vanishes (\<lambda>n. X n - Y n) \<Longrightarrow> realrel X Y"
   1.385 +  by (simp add: realrel_def)
   1.386  
   1.387  lemma realrel_refl: "cauchy X \<Longrightarrow> realrel X X"
   1.388 -  unfolding realrel_def by simp
   1.389 +  by (simp add: realrel_def)
   1.390  
   1.391  lemma symp_realrel: "symp realrel"
   1.392    unfolding realrel_def
   1.393 -  by (rule sympI, clarify, drule vanishes_minus, simp)
   1.394 +  apply (rule sympI)
   1.395 +  apply clarify
   1.396 +  apply (drule vanishes_minus)
   1.397 +  apply simp
   1.398 +  done
   1.399  
   1.400  lemma transp_realrel: "transp realrel"
   1.401    unfolding realrel_def
   1.402 -  apply (rule transpI, clarify)
   1.403 +  apply (rule transpI)
   1.404 +  apply clarify
   1.405    apply (drule (1) vanishes_add)
   1.406    apply (simp add: algebra_simps)
   1.407    done
   1.408  
   1.409  lemma part_equivp_realrel: "part_equivp realrel"
   1.410 -  by (blast intro: part_equivpI symp_realrel transp_realrel
   1.411 -    realrel_refl cauchy_const)
   1.412 +  by (blast intro: part_equivpI symp_realrel transp_realrel realrel_refl cauchy_const)
   1.413 +
   1.414  
   1.415  subsection \<open>The field of real numbers\<close>
   1.416  
   1.417 @@ -385,20 +391,20 @@
   1.418    unfolding real.pcr_cr_eq cr_real_def realrel_def by auto
   1.419  
   1.420  lemma Real_induct [induct type: real]: (* TODO: generate automatically *)
   1.421 -  assumes "\<And>X. cauchy X \<Longrightarrow> P (Real X)" shows "P x"
   1.422 +  assumes "\<And>X. cauchy X \<Longrightarrow> P (Real X)"
   1.423 +  shows "P x"
   1.424  proof (induct x)
   1.425    case (1 X)
   1.426 -  hence "cauchy X" by (simp add: realrel_def)
   1.427 -  thus "P (Real X)" by (rule assms)
   1.428 +  then have "cauchy X" by (simp add: realrel_def)
   1.429 +  then show "P (Real X)" by (rule assms)
   1.430  qed
   1.431  
   1.432 -lemma eq_Real:
   1.433 -  "cauchy X \<Longrightarrow> cauchy Y \<Longrightarrow> Real X = Real Y \<longleftrightarrow> vanishes (\<lambda>n. X n - Y n)"
   1.434 +lemma eq_Real: "cauchy X \<Longrightarrow> cauchy Y \<Longrightarrow> Real X = Real Y \<longleftrightarrow> vanishes (\<lambda>n. X n - Y n)"
   1.435    using real.rel_eq_transfer
   1.436    unfolding real.pcr_cr_eq cr_real_def rel_fun_def realrel_def by simp
   1.437  
   1.438  lemma Domainp_pcr_real [transfer_domain_rule]: "Domainp pcr_real = cauchy"
   1.439 -by (simp add: real.domain_eq realrel_def)
   1.440 +  by (simp add: real.domain_eq realrel_def)
   1.441  
   1.442  instantiation real :: field
   1.443  begin
   1.444 @@ -419,14 +425,16 @@
   1.445  
   1.446  lift_definition times_real :: "real \<Rightarrow> real \<Rightarrow> real" is "\<lambda>X Y n. X n * Y n"
   1.447    unfolding realrel_def mult_diff_mult
   1.448 -  by (subst (4) mult.commute, simp only: cauchy_mult vanishes_add
   1.449 -    vanishes_mult_bounded cauchy_imp_bounded simp_thms)
   1.450 +  apply (subst (4) mult.commute)
   1.451 +  apply (simp only: cauchy_mult vanishes_add vanishes_mult_bounded cauchy_imp_bounded simp_thms)
   1.452 +  done
   1.453  
   1.454  lift_definition inverse_real :: "real \<Rightarrow> real"
   1.455    is "\<lambda>X. if vanishes X then (\<lambda>n. 0) else (\<lambda>n. inverse (X n))"
   1.456  proof -
   1.457 -  fix X Y assume "realrel X Y"
   1.458 -  hence X: "cauchy X" and Y: "cauchy Y" and XY: "vanishes (\<lambda>n. X n - Y n)"
   1.459 +  fix X Y
   1.460 +  assume "realrel X Y"
   1.461 +  then have X: "cauchy X" and Y: "cauchy Y" and XY: "vanishes (\<lambda>n. X n - Y n)"
   1.462      unfolding realrel_def by simp_all
   1.463    have "vanishes X \<longleftrightarrow> vanishes Y"
   1.464    proof
   1.465 @@ -436,49 +444,32 @@
   1.466      assume "vanishes Y"
   1.467      from vanishes_add [OF this XY] show "vanishes X" by simp
   1.468    qed
   1.469 -  thus "?thesis X Y"
   1.470 -    unfolding realrel_def
   1.471 -    by (simp add: vanishes_diff_inverse X Y XY)
   1.472 +  then show "?thesis X Y" by (simp add: vanishes_diff_inverse X Y XY realrel_def)
   1.473  qed
   1.474  
   1.475 -definition
   1.476 -  "x - y = (x::real) + - y"
   1.477 -
   1.478 -definition
   1.479 -  "x div y = (x::real) * inverse y"
   1.480 +definition "x - y = x + - y" for x y :: real
   1.481  
   1.482 -lemma add_Real:
   1.483 -  assumes X: "cauchy X" and Y: "cauchy Y"
   1.484 -  shows "Real X + Real Y = Real (\<lambda>n. X n + Y n)"
   1.485 -  using assms plus_real.transfer
   1.486 -  unfolding cr_real_eq rel_fun_def by simp
   1.487 +definition "x div y = x * inverse y" for x y :: real
   1.488 +
   1.489 +lemma add_Real: "cauchy X \<Longrightarrow> cauchy Y \<Longrightarrow> Real X + Real Y = Real (\<lambda>n. X n + Y n)"
   1.490 +  using plus_real.transfer by (simp add: cr_real_eq rel_fun_def)
   1.491  
   1.492 -lemma minus_Real:
   1.493 -  assumes X: "cauchy X"
   1.494 -  shows "- Real X = Real (\<lambda>n. - X n)"
   1.495 -  using assms uminus_real.transfer
   1.496 -  unfolding cr_real_eq rel_fun_def by simp
   1.497 +lemma minus_Real: "cauchy X \<Longrightarrow> - Real X = Real (\<lambda>n. - X n)"
   1.498 +  using uminus_real.transfer by (simp add: cr_real_eq rel_fun_def)
   1.499  
   1.500 -lemma diff_Real:
   1.501 -  assumes X: "cauchy X" and Y: "cauchy Y"
   1.502 -  shows "Real X - Real Y = Real (\<lambda>n. X n - Y n)"
   1.503 -  unfolding minus_real_def
   1.504 -  by (simp add: minus_Real add_Real X Y)
   1.505 +lemma diff_Real: "cauchy X \<Longrightarrow> cauchy Y \<Longrightarrow> Real X - Real Y = Real (\<lambda>n. X n - Y n)"
   1.506 +  by (simp add: minus_Real add_Real minus_real_def)
   1.507  
   1.508 -lemma mult_Real:
   1.509 -  assumes X: "cauchy X" and Y: "cauchy Y"
   1.510 -  shows "Real X * Real Y = Real (\<lambda>n. X n * Y n)"
   1.511 -  using assms times_real.transfer
   1.512 -  unfolding cr_real_eq rel_fun_def by simp
   1.513 +lemma mult_Real: "cauchy X \<Longrightarrow> cauchy Y \<Longrightarrow> Real X * Real Y = Real (\<lambda>n. X n * Y n)"
   1.514 +  using times_real.transfer by (simp add: cr_real_eq rel_fun_def)
   1.515  
   1.516  lemma inverse_Real:
   1.517 -  assumes X: "cauchy X"
   1.518 -  shows "inverse (Real X) =
   1.519 -    (if vanishes X then 0 else Real (\<lambda>n. inverse (X n)))"
   1.520 -  using assms inverse_real.transfer zero_real.transfer
   1.521 +  "cauchy X \<Longrightarrow> inverse (Real X) = (if vanishes X then 0 else Real (\<lambda>n. inverse (X n)))"
   1.522 +  using inverse_real.transfer zero_real.transfer
   1.523    unfolding cr_real_eq rel_fun_def by (simp split: if_split_asm, metis)
   1.524  
   1.525 -instance proof
   1.526 +instance
   1.527 +proof
   1.528    fix a b c :: real
   1.529    show "a + b = b + a"
   1.530      by transfer (simp add: ac_simps realrel_def)
   1.531 @@ -516,115 +507,125 @@
   1.532  
   1.533  end
   1.534  
   1.535 +
   1.536  subsection \<open>Positive reals\<close>
   1.537  
   1.538  lift_definition positive :: "real \<Rightarrow> bool"
   1.539    is "\<lambda>X. \<exists>r>0. \<exists>k. \<forall>n\<ge>k. r < X n"
   1.540  proof -
   1.541 -  { fix X Y
   1.542 -    assume "realrel X Y"
   1.543 -    hence XY: "vanishes (\<lambda>n. X n - Y n)"
   1.544 -      unfolding realrel_def by simp_all
   1.545 -    assume "\<exists>r>0. \<exists>k. \<forall>n\<ge>k. r < X n"
   1.546 -    then obtain r i where "0 < r" and i: "\<forall>n\<ge>i. r < X n"
   1.547 +  have 1: "\<exists>r>0. \<exists>k. \<forall>n\<ge>k. r < Y n"
   1.548 +    if *: "realrel X Y" and **: "\<exists>r>0. \<exists>k. \<forall>n\<ge>k. r < X n" for X Y
   1.549 +  proof -
   1.550 +    from * have XY: "vanishes (\<lambda>n. X n - Y n)"
   1.551 +      by (simp_all add: realrel_def)
   1.552 +    from ** obtain r i where "0 < r" and i: "\<forall>n\<ge>i. r < X n"
   1.553        by blast
   1.554      obtain s t where s: "0 < s" and t: "0 < t" and r: "r = s + t"
   1.555        using \<open>0 < r\<close> by (rule obtain_pos_sum)
   1.556      obtain j where j: "\<forall>n\<ge>j. \<bar>X n - Y n\<bar> < s"
   1.557        using vanishesD [OF XY s] ..
   1.558      have "\<forall>n\<ge>max i j. t < Y n"
   1.559 -    proof (clarsimp)
   1.560 -      fix n assume n: "i \<le> n" "j \<le> n"
   1.561 +    proof clarsimp
   1.562 +      fix n
   1.563 +      assume n: "i \<le> n" "j \<le> n"
   1.564        have "\<bar>X n - Y n\<bar> < s" and "r < X n"
   1.565          using i j n by simp_all
   1.566 -      thus "t < Y n" unfolding r by simp
   1.567 +      then show "t < Y n" by (simp add: r)
   1.568      qed
   1.569 -    hence "\<exists>r>0. \<exists>k. \<forall>n\<ge>k. r < Y n" using t by blast
   1.570 -  } note 1 = this
   1.571 +    then show ?thesis using t by blast
   1.572 +  qed
   1.573    fix X Y assume "realrel X Y"
   1.574 -  hence "realrel X Y" and "realrel Y X"
   1.575 -    using symp_realrel unfolding symp_def by auto
   1.576 -  thus "?thesis X Y"
   1.577 +  then have "realrel X Y" and "realrel Y X"
   1.578 +    using symp_realrel by (auto simp: symp_def)
   1.579 +  then show "?thesis X Y"
   1.580      by (safe elim!: 1)
   1.581  qed
   1.582  
   1.583 -lemma positive_Real:
   1.584 -  assumes X: "cauchy X"
   1.585 -  shows "positive (Real X) \<longleftrightarrow> (\<exists>r>0. \<exists>k. \<forall>n\<ge>k. r < X n)"
   1.586 -  using assms positive.transfer
   1.587 -  unfolding cr_real_eq rel_fun_def by simp
   1.588 +lemma positive_Real: "cauchy X \<Longrightarrow> positive (Real X) \<longleftrightarrow> (\<exists>r>0. \<exists>k. \<forall>n\<ge>k. r < X n)"
   1.589 +  using positive.transfer by (simp add: cr_real_eq rel_fun_def)
   1.590  
   1.591  lemma positive_zero: "\<not> positive 0"
   1.592    by transfer auto
   1.593  
   1.594 -lemma positive_add:
   1.595 -  "positive x \<Longrightarrow> positive y \<Longrightarrow> positive (x + y)"
   1.596 -apply transfer
   1.597 -apply (clarify, rename_tac a b i j)
   1.598 -apply (rule_tac x="a + b" in exI, simp)
   1.599 -apply (rule_tac x="max i j" in exI, clarsimp)
   1.600 -apply (simp add: add_strict_mono)
   1.601 -done
   1.602 +lemma positive_add: "positive x \<Longrightarrow> positive y \<Longrightarrow> positive (x + y)"
   1.603 +  apply transfer
   1.604 +  apply clarify
   1.605 +  apply (rename_tac a b i j)
   1.606 +  apply (rule_tac x = "a + b" in exI)
   1.607 +  apply simp
   1.608 +  apply (rule_tac x = "max i j" in exI)
   1.609 +  apply clarsimp
   1.610 +  apply (simp add: add_strict_mono)
   1.611 +  done
   1.612  
   1.613 -lemma positive_mult:
   1.614 -  "positive x \<Longrightarrow> positive y \<Longrightarrow> positive (x * y)"
   1.615 -apply transfer
   1.616 -apply (clarify, rename_tac a b i j)
   1.617 -apply (rule_tac x="a * b" in exI, simp)
   1.618 -apply (rule_tac x="max i j" in exI, clarsimp)
   1.619 -apply (rule mult_strict_mono, auto)
   1.620 -done
   1.621 +lemma positive_mult: "positive x \<Longrightarrow> positive y \<Longrightarrow> positive (x * y)"
   1.622 +  apply transfer
   1.623 +  apply clarify
   1.624 +  apply (rename_tac a b i j)
   1.625 +  apply (rule_tac x = "a * b" in exI)
   1.626 +  apply simp
   1.627 +  apply (rule_tac x = "max i j" in exI)
   1.628 +  apply clarsimp
   1.629 +  apply (rule mult_strict_mono)
   1.630 +  apply auto
   1.631 +  done
   1.632  
   1.633 -lemma positive_minus:
   1.634 -  "\<not> positive x \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> positive (- x)"
   1.635 -apply transfer
   1.636 -apply (simp add: realrel_def)
   1.637 -apply (drule (1) cauchy_not_vanishes_cases, safe)
   1.638 -apply blast+
   1.639 -done
   1.640 +lemma positive_minus: "\<not> positive x \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> positive (- x)"
   1.641 +  apply transfer
   1.642 +  apply (simp add: realrel_def)
   1.643 +  apply (drule (1) cauchy_not_vanishes_cases, safe)
   1.644 +  apply blast+
   1.645 +  done
   1.646  
   1.647  instantiation real :: linordered_field
   1.648  begin
   1.649  
   1.650 -definition
   1.651 -  "x < y \<longleftrightarrow> positive (y - x)"
   1.652 +definition "x < y \<longleftrightarrow> positive (y - x)"
   1.653  
   1.654 -definition
   1.655 -  "x \<le> (y::real) \<longleftrightarrow> x < y \<or> x = y"
   1.656 +definition "x \<le> y \<longleftrightarrow> x < y \<or> x = y" for x y :: real
   1.657  
   1.658 -definition
   1.659 -  "\<bar>a::real\<bar> = (if a < 0 then - a else a)"
   1.660 +definition "\<bar>a\<bar> = (if a < 0 then - a else a)" for a :: real
   1.661  
   1.662 -definition
   1.663 -  "sgn (a::real) = (if a = 0 then 0 else if 0 < a then 1 else - 1)"
   1.664 +definition "sgn a = (if a = 0 then 0 else if 0 < a then 1 else - 1)" for a :: real
   1.665  
   1.666 -instance proof
   1.667 +instance
   1.668 +proof
   1.669    fix a b c :: real
   1.670    show "\<bar>a\<bar> = (if a < 0 then - a else a)"
   1.671      by (rule abs_real_def)
   1.672    show "a < b \<longleftrightarrow> a \<le> b \<and> \<not> b \<le> a"
   1.673      unfolding less_eq_real_def less_real_def
   1.674 -    by (auto, drule (1) positive_add, simp_all add: positive_zero)
   1.675 +    apply auto
   1.676 +    apply (drule (1) positive_add)
   1.677 +    apply (simp_all add: positive_zero)
   1.678 +    done
   1.679    show "a \<le> a"
   1.680      unfolding less_eq_real_def by simp
   1.681    show "a \<le> b \<Longrightarrow> b \<le> c \<Longrightarrow> a \<le> c"
   1.682      unfolding less_eq_real_def less_real_def
   1.683 -    by (auto, drule (1) positive_add, simp add: algebra_simps)
   1.684 +    apply auto
   1.685 +    apply (drule (1) positive_add)
   1.686 +    apply (simp add: algebra_simps)
   1.687 +    done
   1.688    show "a \<le> b \<Longrightarrow> b \<le> a \<Longrightarrow> a = b"
   1.689      unfolding less_eq_real_def less_real_def
   1.690 -    by (auto, drule (1) positive_add, simp add: positive_zero)
   1.691 +    apply auto
   1.692 +    apply (drule (1) positive_add)
   1.693 +    apply (simp add: positive_zero)
   1.694 +    done
   1.695    show "a \<le> b \<Longrightarrow> c + a \<le> c + b"
   1.696 -    unfolding less_eq_real_def less_real_def by auto
   1.697 +    by (auto simp: less_eq_real_def less_real_def)
   1.698      (* FIXME: Procedure int_combine_numerals: c + b - (c + a) \<equiv> b + - a *)
   1.699      (* Should produce c + b - (c + a) \<equiv> b - a *)
   1.700    show "sgn a = (if a = 0 then 0 else if 0 < a then 1 else - 1)"
   1.701      by (rule sgn_real_def)
   1.702    show "a \<le> b \<or> b \<le> a"
   1.703 -    unfolding less_eq_real_def less_real_def
   1.704 -    by (auto dest!: positive_minus)
   1.705 +    by (auto dest!: positive_minus simp: less_eq_real_def less_real_def)
   1.706    show "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b"
   1.707      unfolding less_real_def
   1.708 -    by (drule (1) positive_mult, simp add: algebra_simps)
   1.709 +    apply (drule (1) positive_mult)
   1.710 +    apply (simp add: algebra_simps)
   1.711 +    done
   1.712  qed
   1.713  
   1.714  end
   1.715 @@ -632,34 +633,26 @@
   1.716  instantiation real :: distrib_lattice
   1.717  begin
   1.718  
   1.719 -definition
   1.720 -  "(inf :: real \<Rightarrow> real \<Rightarrow> real) = min"
   1.721 +definition "(inf :: real \<Rightarrow> real \<Rightarrow> real) = min"
   1.722  
   1.723 -definition
   1.724 -  "(sup :: real \<Rightarrow> real \<Rightarrow> real) = max"
   1.725 +definition "(sup :: real \<Rightarrow> real \<Rightarrow> real) = max"
   1.726  
   1.727 -instance proof
   1.728 -qed (auto simp add: inf_real_def sup_real_def max_min_distrib2)
   1.729 +instance by standard (auto simp add: inf_real_def sup_real_def max_min_distrib2)
   1.730  
   1.731  end
   1.732  
   1.733  lemma of_nat_Real: "of_nat x = Real (\<lambda>n. of_nat x)"
   1.734 -apply (induct x)
   1.735 -apply (simp add: zero_real_def)
   1.736 -apply (simp add: one_real_def add_Real)
   1.737 -done
   1.738 +  by (induct x) (simp_all add: zero_real_def one_real_def add_Real)
   1.739  
   1.740  lemma of_int_Real: "of_int x = Real (\<lambda>n. of_int x)"
   1.741 -apply (cases x rule: int_diff_cases)
   1.742 -apply (simp add: of_nat_Real diff_Real)
   1.743 -done
   1.744 +  by (cases x rule: int_diff_cases) (simp add: of_nat_Real diff_Real)
   1.745  
   1.746  lemma of_rat_Real: "of_rat x = Real (\<lambda>n. x)"
   1.747 -apply (induct x)
   1.748 -apply (simp add: Fract_of_int_quotient of_rat_divide)
   1.749 -apply (simp add: of_int_Real divide_inverse)
   1.750 -apply (simp add: inverse_Real mult_Real)
   1.751 -done
   1.752 +  apply (induct x)
   1.753 +  apply (simp add: Fract_of_int_quotient of_rat_divide)
   1.754 +  apply (simp add: of_int_Real divide_inverse)
   1.755 +  apply (simp add: inverse_Real mult_Real)
   1.756 +  done
   1.757  
   1.758  instance real :: archimedean_field
   1.759  proof
   1.760 @@ -681,69 +674,82 @@
   1.761  instantiation real :: floor_ceiling
   1.762  begin
   1.763  
   1.764 -definition [code del]:
   1.765 -  "\<lfloor>x::real\<rfloor> = (THE z. of_int z \<le> x \<and> x < of_int (z + 1))"
   1.766 +definition [code del]: "\<lfloor>x::real\<rfloor> = (THE z. of_int z \<le> x \<and> x < of_int (z + 1))"
   1.767  
   1.768  instance
   1.769  proof
   1.770 -  fix x :: real
   1.771 -  show "of_int \<lfloor>x\<rfloor> \<le> x \<and> x < of_int (\<lfloor>x\<rfloor> + 1)"
   1.772 +  show "of_int \<lfloor>x\<rfloor> \<le> x \<and> x < of_int (\<lfloor>x\<rfloor> + 1)" for x :: real
   1.773      unfolding floor_real_def using floor_exists1 by (rule theI')
   1.774  qed
   1.775  
   1.776  end
   1.777  
   1.778 +
   1.779  subsection \<open>Completeness\<close>
   1.780  
   1.781  lemma not_positive_Real:
   1.782    assumes X: "cauchy X"
   1.783    shows "\<not> positive (Real X) \<longleftrightarrow> (\<forall>r>0. \<exists>k. \<forall>n\<ge>k. X n \<le> r)"
   1.784 -unfolding positive_Real [OF X]
   1.785 -apply (auto, unfold not_less)
   1.786 -apply (erule obtain_pos_sum)
   1.787 -apply (drule_tac x=s in spec, simp)
   1.788 -apply (drule_tac r=t in cauchyD [OF X], clarify)
   1.789 -apply (drule_tac x=k in spec, clarsimp)
   1.790 -apply (rule_tac x=n in exI, clarify, rename_tac m)
   1.791 -apply (drule_tac x=m in spec, simp)
   1.792 -apply (drule_tac x=n in spec, simp)
   1.793 -apply (drule spec, drule (1) mp, clarify, rename_tac i)
   1.794 -apply (rule_tac x="max i k" in exI, simp)
   1.795 -done
   1.796 +  unfolding positive_Real [OF X]
   1.797 +  apply auto
   1.798 +  apply (unfold not_less)
   1.799 +  apply (erule obtain_pos_sum)
   1.800 +  apply (drule_tac x=s in spec)
   1.801 +  apply simp
   1.802 +  apply (drule_tac r=t in cauchyD [OF X])
   1.803 +  apply clarify
   1.804 +  apply (drule_tac x=k in spec)
   1.805 +  apply clarsimp
   1.806 +  apply (rule_tac x=n in exI)
   1.807 +  apply clarify
   1.808 +  apply (rename_tac m)
   1.809 +  apply (drule_tac x=m in spec)
   1.810 +  apply simp
   1.811 +  apply (drule_tac x=n in spec)
   1.812 +  apply simp
   1.813 +  apply (drule spec)
   1.814 +  apply (drule (1) mp)
   1.815 +  apply clarify
   1.816 +  apply (rename_tac i)
   1.817 +  apply (rule_tac x = "max i k" in exI)
   1.818 +  apply simp
   1.819 +  done
   1.820  
   1.821  lemma le_Real:
   1.822 -  assumes X: "cauchy X" and Y: "cauchy Y"
   1.823 +  assumes "cauchy X" "cauchy Y"
   1.824    shows "Real X \<le> Real Y = (\<forall>r>0. \<exists>k. \<forall>n\<ge>k. X n \<le> Y n + r)"
   1.825 -unfolding not_less [symmetric, where 'a=real] less_real_def
   1.826 -apply (simp add: diff_Real not_positive_Real X Y)
   1.827 -apply (simp add: diff_le_eq ac_simps)
   1.828 -done
   1.829 +  unfolding not_less [symmetric, where 'a=real] less_real_def
   1.830 +  apply (simp add: diff_Real not_positive_Real assms)
   1.831 +  apply (simp add: diff_le_eq ac_simps)
   1.832 +  done
   1.833  
   1.834  lemma le_RealI:
   1.835    assumes Y: "cauchy Y"
   1.836    shows "\<forall>n. x \<le> of_rat (Y n) \<Longrightarrow> x \<le> Real Y"
   1.837  proof (induct x)
   1.838 -  fix X assume X: "cauchy X" and "\<forall>n. Real X \<le> of_rat (Y n)"
   1.839 -  hence le: "\<And>m r. 0 < r \<Longrightarrow> \<exists>k. \<forall>n\<ge>k. X n \<le> Y m + r"
   1.840 +  fix X
   1.841 +  assume X: "cauchy X" and "\<forall>n. Real X \<le> of_rat (Y n)"
   1.842 +  then have le: "\<And>m r. 0 < r \<Longrightarrow> \<exists>k. \<forall>n\<ge>k. X n \<le> Y m + r"
   1.843      by (simp add: of_rat_Real le_Real)
   1.844 -  {
   1.845 -    fix r :: rat assume "0 < r"
   1.846 -    then obtain s t where s: "0 < s" and t: "0 < t" and r: "r = s + t"
   1.847 +  then have "\<exists>k. \<forall>n\<ge>k. X n \<le> Y n + r" if "0 < r" for r :: rat
   1.848 +  proof -
   1.849 +    from that obtain s t where s: "0 < s" and t: "0 < t" and r: "r = s + t"
   1.850        by (rule obtain_pos_sum)
   1.851      obtain i where i: "\<forall>m\<ge>i. \<forall>n\<ge>i. \<bar>Y m - Y n\<bar> < s"
   1.852        using cauchyD [OF Y s] ..
   1.853      obtain j where j: "\<forall>n\<ge>j. X n \<le> Y i + t"
   1.854        using le [OF t] ..
   1.855      have "\<forall>n\<ge>max i j. X n \<le> Y n + r"
   1.856 -    proof (clarsimp)
   1.857 -      fix n assume n: "i \<le> n" "j \<le> n"
   1.858 +    proof clarsimp
   1.859 +      fix n
   1.860 +      assume n: "i \<le> n" "j \<le> n"
   1.861        have "X n \<le> Y i + t" using n j by simp
   1.862        moreover have "\<bar>Y i - Y n\<bar> < s" using n i by simp
   1.863        ultimately show "X n \<le> Y n + r" unfolding r by simp
   1.864      qed
   1.865 -    hence "\<exists>k. \<forall>n\<ge>k. X n \<le> Y n + r" ..
   1.866 -  }
   1.867 -  thus "Real X \<le> Real Y"
   1.868 +    then show ?thesis ..
   1.869 +  qed
   1.870 +  then show "Real X \<le> Real Y"
   1.871      by (simp add: of_rat_Real le_Real X Y)
   1.872  qed
   1.873  
   1.874 @@ -754,18 +760,22 @@
   1.875  proof -
   1.876    have "- y \<le> - Real X"
   1.877      by (simp add: minus_Real X le_RealI of_rat_minus le)
   1.878 -  thus ?thesis by simp
   1.879 +  then show ?thesis by simp
   1.880  qed
   1.881  
   1.882  lemma less_RealD:
   1.883 -  assumes Y: "cauchy Y"
   1.884 +  assumes "cauchy Y"
   1.885    shows "x < Real Y \<Longrightarrow> \<exists>n. x < of_rat (Y n)"
   1.886 -by (erule contrapos_pp, simp add: not_less, erule Real_leI [OF Y])
   1.887 +  apply (erule contrapos_pp)
   1.888 +  apply (simp add: not_less)
   1.889 +  apply (erule Real_leI [OF assms])
   1.890 +  done
   1.891  
   1.892 -lemma of_nat_less_two_power [simp]:
   1.893 -  "of_nat n < (2::'a::linordered_idom) ^ n"
   1.894 -apply (induct n, simp)
   1.895 -by (metis add_le_less_mono mult_2 of_nat_Suc one_le_numeral one_le_power power_Suc)
   1.896 +lemma of_nat_less_two_power [simp]: "of_nat n < (2::'a::linordered_idom) ^ n"
   1.897 +  apply (induct n)
   1.898 +  apply simp
   1.899 +  apply (metis add_le_less_mono mult_2 of_nat_Suc one_le_numeral one_le_power power_Suc)
   1.900 +  done
   1.901  
   1.902  lemma complete_real:
   1.903    fixes S :: "real set"
   1.904 @@ -781,7 +791,7 @@
   1.905      have "of_int \<lfloor>x - 1\<rfloor> \<le> x - 1" by (rule of_int_floor_le)
   1.906      also have "x - 1 < x" by simp
   1.907      finally have "of_int \<lfloor>x - 1\<rfloor> < x" .
   1.908 -    hence "\<not> x \<le> of_int \<lfloor>x - 1\<rfloor>" by (simp only: not_le)
   1.909 +    then have "\<not> x \<le> of_int \<lfloor>x - 1\<rfloor>" by (simp only: not_le)
   1.910      then show "\<not> P (of_int \<lfloor>x - 1\<rfloor>)"
   1.911        unfolding P_def of_rat_of_int_eq using x by blast
   1.912    qed
   1.913 @@ -791,7 +801,7 @@
   1.914      unfolding P_def of_rat_of_int_eq
   1.915      proof
   1.916        fix y assume "y \<in> S"
   1.917 -      hence "y \<le> z" using z by simp
   1.918 +      then have "y \<le> z" using z by simp
   1.919        also have "z \<le> of_int \<lceil>z\<rceil>" by (rule le_of_int_ceiling)
   1.920        finally show "y \<le> of_int \<lceil>z\<rceil>" .
   1.921      qed
   1.922 @@ -809,13 +819,13 @@
   1.923    have B_Suc [simp]: "\<And>n. B (Suc n) = (if P (C n) then C n else B n)"
   1.924      unfolding A_def B_def C_def bisect_def split_def by simp
   1.925  
   1.926 -  have width: "\<And>n. B n - A n = (b - a) / 2^n"
   1.927 -    apply (simp add: eq_divide_eq)
   1.928 -    apply (induct_tac n, simp)
   1.929 -    apply (simp add: C_def avg_def algebra_simps)
   1.930 +  have width: "B n - A n = (b - a) / 2^n" for n
   1.931 +    apply (induct n)
   1.932 +    apply (simp_all add: eq_divide_eq)
   1.933 +    apply (simp_all add: C_def avg_def algebra_simps)
   1.934      done
   1.935  
   1.936 -  have twos: "\<And>y r :: rat. 0 < r \<Longrightarrow> \<exists>n. y / 2 ^ n < r"
   1.937 +  have twos: "0 < r \<Longrightarrow> \<exists>n. y / 2 ^ n < r" for y r :: rat
   1.938      apply (simp add: divide_less_eq)
   1.939      apply (subst mult.commute)
   1.940      apply (frule_tac y=y in ex_less_of_nat_mult)
   1.941 @@ -828,10 +838,8 @@
   1.942      apply assumption
   1.943      done
   1.944  
   1.945 -  have PA: "\<And>n. \<not> P (A n)"
   1.946 -    by (induct_tac n, simp_all add: a)
   1.947 -  have PB: "\<And>n. P (B n)"
   1.948 -    by (induct_tac n, simp_all add: b)
   1.949 +  have PA: "\<not> P (A n)" for n by (induct n) (simp_all add: a)
   1.950 +  have PB: "P (B n)" for n by (induct n) (simp_all add: b)
   1.951    have ab: "a < b"
   1.952      using a b unfolding P_def
   1.953      apply (clarsimp simp add: not_le)
   1.954 @@ -839,8 +847,7 @@
   1.955      apply (drule (1) less_le_trans)
   1.956      apply (simp add: of_rat_less)
   1.957      done
   1.958 -  have AB: "\<And>n. A n < B n"
   1.959 -    by (induct_tac n, simp add: ab, simp add: C_def avg_def)
   1.960 +  have AB: "A n < B n" for n by (induct n) (simp_all add: ab C_def avg_def)
   1.961    have A_mono: "\<And>i j. i \<le> j \<Longrightarrow> A i \<le> A j"
   1.962      apply (auto simp add: le_less [where 'a=nat])
   1.963      apply (erule less_Suc_induct)
   1.964 @@ -857,8 +864,7 @@
   1.965      apply (rule AB [THEN less_imp_le])
   1.966      apply simp
   1.967      done
   1.968 -  have cauchy_lemma:
   1.969 -    "\<And>X. \<forall>n. \<forall>i\<ge>n. A n \<le> X i \<and> X i \<le> B n \<Longrightarrow> cauchy X"
   1.970 +  have cauchy_lemma: "\<And>X. \<forall>n. \<forall>i\<ge>n. A n \<le> X i \<and> X i \<le> B n \<Longrightarrow> cauchy X"
   1.971      apply (rule cauchyI)
   1.972      apply (drule twos [where y="b - a"])
   1.973      apply (erule exE)
   1.974 @@ -884,7 +890,8 @@
   1.975      done
   1.976    have 1: "\<forall>x\<in>S. x \<le> Real B"
   1.977    proof
   1.978 -    fix x assume "x \<in> S"
   1.979 +    fix x
   1.980 +    assume "x \<in> S"
   1.981      then show "x \<le> Real B"
   1.982        using PB [unfolded P_def] \<open>cauchy B\<close>
   1.983        by (simp add: le_RealI)
   1.984 @@ -902,12 +909,14 @@
   1.985      done
   1.986    have "vanishes (\<lambda>n. (b - a) / 2 ^ n)"
   1.987    proof (rule vanishesI)
   1.988 -    fix r :: rat assume "0 < r"
   1.989 +    fix r :: rat
   1.990 +    assume "0 < r"
   1.991      then obtain k where k: "\<bar>b - a\<bar> / 2 ^ k < r"
   1.992        using twos by blast
   1.993      have "\<forall>n\<ge>k. \<bar>(b - a) / 2 ^ n\<bar> < r"
   1.994 -    proof (clarify)
   1.995 -      fix n assume n: "k \<le> n"
   1.996 +    proof clarify
   1.997 +      fix n
   1.998 +      assume n: "k \<le> n"
   1.999        have "\<bar>(b - a) / 2 ^ n\<bar> = \<bar>b - a\<bar> / 2 ^ n"
  1.1000          by simp
  1.1001        also have "\<dots> \<le> \<bar>b - a\<bar> / 2 ^ k"
  1.1002 @@ -915,52 +924,55 @@
  1.1003        also note k
  1.1004        finally show "\<bar>(b - a) / 2 ^ n\<bar> < r" .
  1.1005      qed
  1.1006 -    thus "\<exists>k. \<forall>n\<ge>k. \<bar>(b - a) / 2 ^ n\<bar> < r" ..
  1.1007 +    then show "\<exists>k. \<forall>n\<ge>k. \<bar>(b - a) / 2 ^ n\<bar> < r" ..
  1.1008    qed
  1.1009 -  hence 3: "Real B = Real A"
  1.1010 +  then have 3: "Real B = Real A"
  1.1011      by (simp add: eq_Real \<open>cauchy A\<close> \<open>cauchy B\<close> width)
  1.1012    show "\<exists>y. (\<forall>x\<in>S. x \<le> y) \<and> (\<forall>z. (\<forall>x\<in>S. x \<le> z) \<longrightarrow> y \<le> z)"
  1.1013 -    using 1 2 3 by (rule_tac x="Real B" in exI, simp)
  1.1014 +    apply (rule exI [where x = "Real B"])
  1.1015 +    using 1 2 3
  1.1016 +    apply simp
  1.1017 +    done
  1.1018  qed
  1.1019  
  1.1020  instantiation real :: linear_continuum
  1.1021  begin
  1.1022  
  1.1023 -subsection\<open>Supremum of a set of reals\<close>
  1.1024 +subsection \<open>Supremum of a set of reals\<close>
  1.1025  
  1.1026  definition "Sup X = (LEAST z::real. \<forall>x\<in>X. x \<le> z)"
  1.1027 -definition "Inf (X::real set) = - Sup (uminus ` X)"
  1.1028 +definition "Inf X = - Sup (uminus ` X)" for X :: "real set"
  1.1029  
  1.1030  instance
  1.1031  proof
  1.1032 -  { fix x :: real and X :: "real set"
  1.1033 -    assume x: "x \<in> X" "bdd_above X"
  1.1034 -    then obtain s where s: "\<forall>y\<in>X. y \<le> s" "\<And>z. \<forall>y\<in>X. y \<le> z \<Longrightarrow> s \<le> z"
  1.1035 +  show Sup_upper: "x \<le> Sup X" if "x \<in> X" "bdd_above X" for x :: real and X :: "real set"
  1.1036 +  proof -
  1.1037 +    from that obtain s where s: "\<forall>y\<in>X. y \<le> s" "\<And>z. \<forall>y\<in>X. y \<le> z \<Longrightarrow> s \<le> z"
  1.1038        using complete_real[of X] unfolding bdd_above_def by blast
  1.1039 -    then show "x \<le> Sup X"
  1.1040 -      unfolding Sup_real_def by (rule LeastI2_order) (auto simp: x) }
  1.1041 -  note Sup_upper = this
  1.1042 -
  1.1043 -  { fix z :: real and X :: "real set"
  1.1044 -    assume x: "X \<noteq> {}" and z: "\<And>x. x \<in> X \<Longrightarrow> x \<le> z"
  1.1045 -    then obtain s where s: "\<forall>y\<in>X. y \<le> s" "\<And>z. \<forall>y\<in>X. y \<le> z \<Longrightarrow> s \<le> z"
  1.1046 -      using complete_real[of X] by blast
  1.1047 +    then show ?thesis unfolding Sup_real_def by (rule LeastI2_order) (auto simp: that)
  1.1048 +  qed
  1.1049 +  show Sup_least: "Sup X \<le> z" if "X \<noteq> {}" and z: "\<And>x. x \<in> X \<Longrightarrow> x \<le> z"
  1.1050 +    for z :: real and X :: "real set"
  1.1051 +  proof -
  1.1052 +    from that obtain s where s: "\<forall>y\<in>X. y \<le> s" "\<And>z. \<forall>y\<in>X. y \<le> z \<Longrightarrow> s \<le> z"
  1.1053 +      using complete_real [of X] by blast
  1.1054      then have "Sup X = s"
  1.1055        unfolding Sup_real_def by (best intro: Least_equality)
  1.1056 -    also from s z have "... \<le> z"
  1.1057 +    also from s z have "\<dots> \<le> z"
  1.1058        by blast
  1.1059 -    finally show "Sup X \<le> z" . }
  1.1060 -  note Sup_least = this
  1.1061 -
  1.1062 -  { fix x :: real and X :: "real set" assume x: "x \<in> X" "bdd_below X" then show "Inf X \<le> x"
  1.1063 -      using Sup_upper[of "-x" "uminus ` X"] by (auto simp: Inf_real_def) }
  1.1064 -  { fix z :: real and X :: "real set" assume "X \<noteq> {}" "\<And>x. x \<in> X \<Longrightarrow> z \<le> x" then show "z \<le> Inf X"
  1.1065 -      using Sup_least[of "uminus ` X" "- z"] by (force simp: Inf_real_def) }
  1.1066 +    finally show ?thesis .
  1.1067 +  qed
  1.1068 +  show "Inf X \<le> x" if "x \<in> X" "bdd_below X" for x :: real and X :: "real set"
  1.1069 +    using Sup_upper [of "-x" "uminus ` X"] by (auto simp: Inf_real_def that)
  1.1070 +  show "z \<le> Inf X" if "X \<noteq> {}" "\<And>x. x \<in> X \<Longrightarrow> z \<le> x" for z :: real and X :: "real set"
  1.1071 +    using Sup_least [of "uminus ` X" "- z"] by (force simp: Inf_real_def that)
  1.1072    show "\<exists>a b::real. a \<noteq> b"
  1.1073      using zero_neq_one by blast
  1.1074  qed
  1.1075 +
  1.1076  end
  1.1077  
  1.1078 +
  1.1079  subsection \<open>Hiding implementation details\<close>
  1.1080  
  1.1081  hide_const (open) vanishes cauchy positive Real
  1.1082 @@ -972,42 +984,35 @@
  1.1083  lifting_update real.lifting
  1.1084  lifting_forget real.lifting
  1.1085  
  1.1086 -subsection\<open>More Lemmas\<close>
  1.1087 +
  1.1088 +subsection \<open>More Lemmas\<close>
  1.1089  
  1.1090  text \<open>BH: These lemmas should not be necessary; they should be
  1.1091 -covered by existing simp rules and simplification procedures.\<close>
  1.1092 +  covered by existing simp rules and simplification procedures.\<close>
  1.1093  
  1.1094 -lemma real_mult_less_iff1 [simp]: "(0::real) < z ==> (x*z < y*z) = (x < y)"
  1.1095 -by simp (* solved by linordered_ring_less_cancel_factor simproc *)
  1.1096 +lemma real_mult_less_iff1 [simp]: "0 < z \<Longrightarrow> x * z < y * z \<longleftrightarrow> x < y" for x y z :: real
  1.1097 +  by simp (* solved by linordered_ring_less_cancel_factor simproc *)
  1.1098  
  1.1099 -lemma real_mult_le_cancel_iff1 [simp]: "(0::real) < z ==> (x*z \<le> y*z) = (x\<le>y)"
  1.1100 -by simp (* solved by linordered_ring_le_cancel_factor simproc *)
  1.1101 +lemma real_mult_le_cancel_iff1 [simp]: "0 < z \<Longrightarrow> x * z \<le> y * z \<longleftrightarrow> x \<le> y" for x y z :: real
  1.1102 +  by simp (* solved by linordered_ring_le_cancel_factor simproc *)
  1.1103  
  1.1104 -lemma real_mult_le_cancel_iff2 [simp]: "(0::real) < z ==> (z*x \<le> z*y) = (x\<le>y)"
  1.1105 -by simp (* solved by linordered_ring_le_cancel_factor simproc *)
  1.1106 +lemma real_mult_le_cancel_iff2 [simp]: "0 < z \<Longrightarrow> z * x \<le> z * y \<longleftrightarrow> x \<le> y" for x y z :: real
  1.1107 +  by simp (* solved by linordered_ring_le_cancel_factor simproc *)
  1.1108  
  1.1109  
  1.1110  subsection \<open>Embedding numbers into the Reals\<close>
  1.1111  
  1.1112 -abbreviation
  1.1113 -  real_of_nat :: "nat \<Rightarrow> real"
  1.1114 -where
  1.1115 -  "real_of_nat \<equiv> of_nat"
  1.1116 +abbreviation real_of_nat :: "nat \<Rightarrow> real"
  1.1117 +  where "real_of_nat \<equiv> of_nat"
  1.1118  
  1.1119 -abbreviation
  1.1120 -  real :: "nat \<Rightarrow> real"
  1.1121 -where
  1.1122 -  "real \<equiv> of_nat"
  1.1123 +abbreviation real :: "nat \<Rightarrow> real"
  1.1124 +  where "real \<equiv> of_nat"
  1.1125  
  1.1126 -abbreviation
  1.1127 -  real_of_int :: "int \<Rightarrow> real"
  1.1128 -where
  1.1129 -  "real_of_int \<equiv> of_int"
  1.1130 +abbreviation real_of_int :: "int \<Rightarrow> real"
  1.1131 +  where "real_of_int \<equiv> of_int"
  1.1132  
  1.1133 -abbreviation
  1.1134 -  real_of_rat :: "rat \<Rightarrow> real"
  1.1135 -where
  1.1136 -  "real_of_rat \<equiv> of_rat"
  1.1137 +abbreviation real_of_rat :: "rat \<Rightarrow> real"
  1.1138 +  where "real_of_rat \<equiv> of_rat"
  1.1139  
  1.1140  declare [[coercion_enabled]]
  1.1141  
  1.1142 @@ -1036,68 +1041,65 @@
  1.1143  declare of_int_1_less_iff [algebra, presburger]
  1.1144  declare of_int_1_le_iff [algebra, presburger]
  1.1145  
  1.1146 -lemma int_less_real_le: "(n < m) = (real_of_int n + 1 <= real_of_int m)"
  1.1147 +lemma int_less_real_le: "n < m \<longleftrightarrow> real_of_int n + 1 \<le> real_of_int m"
  1.1148  proof -
  1.1149    have "(0::real) \<le> 1"
  1.1150      by (metis less_eq_real_def zero_less_one)
  1.1151 -  thus ?thesis
  1.1152 +  then show ?thesis
  1.1153      by (metis floor_of_int less_floor_iff)
  1.1154  qed
  1.1155  
  1.1156 -lemma int_le_real_less: "(n \<le> m) = (real_of_int n < real_of_int m + 1)"
  1.1157 +lemma int_le_real_less: "n \<le> m \<longleftrightarrow> real_of_int n < real_of_int m + 1"
  1.1158    by (meson int_less_real_le not_le)
  1.1159  
  1.1160 -
  1.1161 -lemma real_of_int_div_aux: "(real_of_int x) / (real_of_int d) =
  1.1162 +lemma real_of_int_div_aux:
  1.1163 +  "(real_of_int x) / (real_of_int d) =
  1.1164      real_of_int (x div d) + (real_of_int (x mod d)) / (real_of_int d)"
  1.1165  proof -
  1.1166    have "x = (x div d) * d + x mod d"
  1.1167      by auto
  1.1168    then have "real_of_int x = real_of_int (x div d) * real_of_int d + real_of_int(x mod d)"
  1.1169      by (metis of_int_add of_int_mult)
  1.1170 -  then have "real_of_int x / real_of_int d = ... / real_of_int d"
  1.1171 +  then have "real_of_int x / real_of_int d = \<dots> / real_of_int d"
  1.1172      by simp
  1.1173    then show ?thesis
  1.1174      by (auto simp add: add_divide_distrib algebra_simps)
  1.1175  qed
  1.1176  
  1.1177  lemma real_of_int_div:
  1.1178 -  fixes d n :: int
  1.1179 -  shows "d dvd n \<Longrightarrow> real_of_int (n div d) = real_of_int n / real_of_int d"
  1.1180 +  "d dvd n \<Longrightarrow> real_of_int (n div d) = real_of_int n / real_of_int d" for d n :: int
  1.1181    by (simp add: real_of_int_div_aux)
  1.1182  
  1.1183 -lemma real_of_int_div2:
  1.1184 -  "0 <= real_of_int n / real_of_int x - real_of_int (n div x)"
  1.1185 -  apply (case_tac "x = 0", simp)
  1.1186 -  apply (case_tac "0 < x")
  1.1187 +lemma real_of_int_div2: "0 \<le> real_of_int n / real_of_int x - real_of_int (n div x)"
  1.1188 +  apply (cases "x = 0")
  1.1189 +  apply simp
  1.1190 +  apply (cases "0 < x")
  1.1191     apply (metis add.left_neutral floor_correct floor_divide_of_int_eq le_diff_eq)
  1.1192    apply (metis add.left_neutral floor_correct floor_divide_of_int_eq le_diff_eq)
  1.1193    done
  1.1194  
  1.1195 -lemma real_of_int_div3:
  1.1196 -  "real_of_int (n::int) / real_of_int (x) - real_of_int (n div x) <= 1"
  1.1197 +lemma real_of_int_div3: "real_of_int n / real_of_int x - real_of_int (n div x) \<le> 1"
  1.1198    apply (simp add: algebra_simps)
  1.1199    apply (subst real_of_int_div_aux)
  1.1200    apply (auto simp add: divide_le_eq intro: order_less_imp_le)
  1.1201 -done
  1.1202 +  done
  1.1203  
  1.1204 -lemma real_of_int_div4: "real_of_int (n div x) <= real_of_int (n::int) / real_of_int x"
  1.1205 -by (insert real_of_int_div2 [of n x], simp)
  1.1206 +lemma real_of_int_div4: "real_of_int (n div x) \<le> real_of_int n / real_of_int x"
  1.1207 +  using real_of_int_div2 [of n x] by simp
  1.1208  
  1.1209  
  1.1210 -subsection\<open>Embedding the Naturals into the Reals\<close>
  1.1211 +subsection \<open>Embedding the Naturals into the Reals\<close>
  1.1212  
  1.1213 -lemma real_of_card: "real (card A) = setsum (\<lambda>x.1) A"
  1.1214 +lemma real_of_card: "real (card A) = setsum (\<lambda>x. 1) A"
  1.1215    by simp
  1.1216  
  1.1217 -lemma nat_less_real_le: "(n < m) = (real n + 1 \<le> real m)"
  1.1218 +lemma nat_less_real_le: "n < m \<longleftrightarrow> real n + 1 \<le> real m"
  1.1219    by (metis discrete of_nat_1 of_nat_add of_nat_le_iff)
  1.1220  
  1.1221 -lemma nat_le_real_less: "((n::nat) <= m) = (real n < real m + 1)"
  1.1222 +lemma nat_le_real_less: "n \<le> m \<longleftrightarrow> real n < real m + 1" for m n :: nat
  1.1223    by (meson nat_less_real_le not_le)
  1.1224  
  1.1225 -lemma real_of_nat_div_aux: "(real x) / (real d) =
  1.1226 -    real (x div d) + (real (x mod d)) / (real d)"
  1.1227 +lemma real_of_nat_div_aux: "real x / real d = real (x div d) + real (x mod d) / real d"
  1.1228  proof -
  1.1229    have "x = (x div d) * d + x mod d"
  1.1230      by auto
  1.1231 @@ -1110,27 +1112,25 @@
  1.1232  qed
  1.1233  
  1.1234  lemma real_of_nat_div: "d dvd n \<Longrightarrow> real(n div d) = real n / real d"
  1.1235 -  by (subst real_of_nat_div_aux)
  1.1236 -    (auto simp add: dvd_eq_mod_eq_0 [symmetric])
  1.1237 +  by (subst real_of_nat_div_aux) (auto simp add: dvd_eq_mod_eq_0 [symmetric])
  1.1238  
  1.1239 -lemma real_of_nat_div2:
  1.1240 -  "0 <= real (n::nat) / real (x) - real (n div x)"
  1.1241 -apply (simp add: algebra_simps)
  1.1242 -apply (subst real_of_nat_div_aux)
  1.1243 -apply simp
  1.1244 -done
  1.1245 +lemma real_of_nat_div2: "0 \<le> real n / real x - real (n div x)" for n x :: nat
  1.1246 +  apply (simp add: algebra_simps)
  1.1247 +  apply (subst real_of_nat_div_aux)
  1.1248 +  apply simp
  1.1249 +  done
  1.1250  
  1.1251 -lemma real_of_nat_div3:
  1.1252 -  "real (n::nat) / real (x) - real (n div x) <= 1"
  1.1253 -apply(case_tac "x = 0")
  1.1254 -apply (simp)
  1.1255 -apply (simp add: algebra_simps)
  1.1256 -apply (subst real_of_nat_div_aux)
  1.1257 -apply simp
  1.1258 -done
  1.1259 +lemma real_of_nat_div3: "real n / real x - real (n div x) \<le> 1" for n x :: nat
  1.1260 +  apply (cases "x = 0")
  1.1261 +  apply simp
  1.1262 +  apply (simp add: algebra_simps)
  1.1263 +  apply (subst real_of_nat_div_aux)
  1.1264 +  apply simp
  1.1265 +  done
  1.1266  
  1.1267 -lemma real_of_nat_div4: "real (n div x) <= real (n::nat) / real x"
  1.1268 -by (insert real_of_nat_div2 [of n x], simp)
  1.1269 +lemma real_of_nat_div4: "real (n div x) \<le> real n / real x" for n x :: nat
  1.1270 +  using real_of_nat_div2 [of n x] by simp
  1.1271 +
  1.1272  
  1.1273  subsection \<open>The Archimedean Property of the Reals\<close>
  1.1274  
  1.1275 @@ -1145,77 +1145,85 @@
  1.1276  
  1.1277  lemma real_archimedian_rdiv_eq_0:
  1.1278    assumes x0: "x \<ge> 0"
  1.1279 -      and c: "c \<ge> 0"
  1.1280 -      and xc: "\<And>m::nat. m > 0 \<Longrightarrow> real m * x \<le> c"
  1.1281 -    shows "x = 0"
  1.1282 -by (metis reals_Archimedean3 dual_order.order_iff_strict le0 le_less_trans not_le x0 xc)
  1.1283 +    and c: "c \<ge> 0"
  1.1284 +    and xc: "\<And>m::nat. m > 0 \<Longrightarrow> real m * x \<le> c"
  1.1285 +  shows "x = 0"
  1.1286 +  by (metis reals_Archimedean3 dual_order.order_iff_strict le0 le_less_trans not_le x0 xc)
  1.1287  
  1.1288  
  1.1289 -subsection\<open>Rationals\<close>
  1.1290 +subsection \<open>Rationals\<close>
  1.1291  
  1.1292 -lemma Rats_eq_int_div_int:
  1.1293 -  "\<rat> = { real_of_int i / real_of_int j |i j. j \<noteq> 0}" (is "_ = ?S")
  1.1294 +lemma Rats_eq_int_div_int: "\<rat> = {real_of_int i / real_of_int j | i j. j \<noteq> 0}"  (is "_ = ?S")
  1.1295  proof
  1.1296    show "\<rat> \<subseteq> ?S"
  1.1297    proof
  1.1298 -    fix x::real assume "x : \<rat>"
  1.1299 -    then obtain r where "x = of_rat r" unfolding Rats_def ..
  1.1300 -    have "of_rat r : ?S"
  1.1301 -      by (cases r) (auto simp add:of_rat_rat)
  1.1302 -    thus "x : ?S" using \<open>x = of_rat r\<close> by simp
  1.1303 +    fix x :: real
  1.1304 +    assume "x \<in> \<rat>"
  1.1305 +    then obtain r where "x = of_rat r"
  1.1306 +      unfolding Rats_def ..
  1.1307 +    have "of_rat r \<in> ?S"
  1.1308 +      by (cases r) (auto simp add: of_rat_rat)
  1.1309 +    then show "x \<in> ?S"
  1.1310 +      using \<open>x = of_rat r\<close> by simp
  1.1311    qed
  1.1312  next
  1.1313    show "?S \<subseteq> \<rat>"
  1.1314 -  proof(auto simp:Rats_def)
  1.1315 -    fix i j :: int assume "j \<noteq> 0"
  1.1316 -    hence "real_of_int i / real_of_int j = of_rat(Fract i j)"
  1.1317 +  proof (auto simp: Rats_def)
  1.1318 +    fix i j :: int
  1.1319 +    assume "j \<noteq> 0"
  1.1320 +    then have "real_of_int i / real_of_int j = of_rat (Fract i j)"
  1.1321        by (simp add: of_rat_rat)
  1.1322 -    thus "real_of_int i / real_of_int j \<in> range of_rat" by blast
  1.1323 +    then show "real_of_int i / real_of_int j \<in> range of_rat"
  1.1324 +      by blast
  1.1325    qed
  1.1326  qed
  1.1327  
  1.1328 -lemma Rats_eq_int_div_nat:
  1.1329 -  "\<rat> = { real_of_int i / real n |i n. n \<noteq> 0}"
  1.1330 -proof(auto simp:Rats_eq_int_div_int)
  1.1331 -  fix i j::int assume "j \<noteq> 0"
  1.1332 -  show "EX (i'::int) (n::nat). real_of_int i / real_of_int j = real_of_int i'/real n \<and> 0<n"
  1.1333 -  proof cases
  1.1334 -    assume "j>0"
  1.1335 -    hence "real_of_int i / real_of_int j = real_of_int i/real(nat j) \<and> 0<nat j"
  1.1336 -      by (simp add: of_nat_nat)
  1.1337 -    thus ?thesis by blast
  1.1338 +lemma Rats_eq_int_div_nat: "\<rat> = { real_of_int i / real n | i n. n \<noteq> 0}"
  1.1339 +proof (auto simp: Rats_eq_int_div_int)
  1.1340 +  fix i j :: int
  1.1341 +  assume "j \<noteq> 0"
  1.1342 +  show "\<exists>(i'::int) (n::nat). real_of_int i / real_of_int j = real_of_int i' / real n \<and> 0 < n"
  1.1343 +  proof (cases "j > 0")
  1.1344 +    case True
  1.1345 +    then have "real_of_int i / real_of_int j = real_of_int i / real (nat j) \<and> 0 < nat j"
  1.1346 +      by simp
  1.1347 +    then show ?thesis by blast
  1.1348    next
  1.1349 -    assume "~ j>0"
  1.1350 -    hence "real_of_int i / real_of_int j = real_of_int(-i) / real(nat(-j)) \<and> 0<nat(-j)" using \<open>j\<noteq>0\<close>
  1.1351 -      by (simp add: of_nat_nat)
  1.1352 -    thus ?thesis by blast
  1.1353 +    case False
  1.1354 +    with \<open>j \<noteq> 0\<close>
  1.1355 +    have "real_of_int i / real_of_int j = real_of_int (- i) / real (nat (- j)) \<and> 0 < nat (- j)"
  1.1356 +      by simp
  1.1357 +    then show ?thesis by blast
  1.1358    qed
  1.1359  next
  1.1360 -  fix i::int and n::nat assume "0 < n"
  1.1361 -  hence "real_of_int i / real n = real_of_int i / real_of_int(int n) \<and> int n \<noteq> 0" by simp
  1.1362 -  thus "\<exists>i' j. real_of_int i / real n = real_of_int i' / real_of_int j \<and> j \<noteq> 0" by blast
  1.1363 +  fix i :: int and n :: nat
  1.1364 +  assume "0 < n"
  1.1365 +  then have "real_of_int i / real n = real_of_int i / real_of_int(int n) \<and> int n \<noteq> 0"
  1.1366 +    by simp
  1.1367 +  then show "\<exists>i' j. real_of_int i / real n = real_of_int i' / real_of_int j \<and> j \<noteq> 0"
  1.1368 +    by blast
  1.1369  qed
  1.1370  
  1.1371  lemma Rats_abs_nat_div_natE:
  1.1372    assumes "x \<in> \<rat>"
  1.1373 -  obtains m n :: nat
  1.1374 -  where "n \<noteq> 0" and "\<bar>x\<bar> = real m / real n" and "gcd m n = 1"
  1.1375 +  obtains m n :: nat where "n \<noteq> 0" and "\<bar>x\<bar> = real m / real n" and "gcd m n = 1"
  1.1376  proof -
  1.1377 -  from \<open>x \<in> \<rat>\<close> obtain i::int and n::nat where "n \<noteq> 0" and "x = real_of_int i / real n"
  1.1378 -    by(auto simp add: Rats_eq_int_div_nat)
  1.1379 -  hence "\<bar>x\<bar> = real (nat \<bar>i\<bar>) / real n" by (simp add: of_nat_nat)
  1.1380 +  from \<open>x \<in> \<rat>\<close> obtain i :: int and n :: nat where "n \<noteq> 0" and "x = real_of_int i / real n"
  1.1381 +    by (auto simp add: Rats_eq_int_div_nat)
  1.1382 +  then have "\<bar>x\<bar> = real (nat \<bar>i\<bar>) / real n" by simp
  1.1383    then obtain m :: nat where x_rat: "\<bar>x\<bar> = real m / real n" by blast
  1.1384    let ?gcd = "gcd m n"
  1.1385 -  from \<open>n\<noteq>0\<close> have gcd: "?gcd \<noteq> 0" by simp
  1.1386 +  from \<open>n \<noteq> 0\<close> have gcd: "?gcd \<noteq> 0" by simp
  1.1387    let ?k = "m div ?gcd"
  1.1388    let ?l = "n div ?gcd"
  1.1389    let ?gcd' = "gcd ?k ?l"
  1.1390 -  have "?gcd dvd m" .. then have gcd_k: "?gcd * ?k = m"
  1.1391 +  have "?gcd dvd m" ..
  1.1392 +  then have gcd_k: "?gcd * ?k = m"
  1.1393      by (rule dvd_mult_div_cancel)
  1.1394 -  have "?gcd dvd n" .. then have gcd_l: "?gcd * ?l = n"
  1.1395 +  have "?gcd dvd n" ..
  1.1396 +  then have gcd_l: "?gcd * ?l = n"
  1.1397      by (rule dvd_mult_div_cancel)
  1.1398 -  from \<open>n \<noteq> 0\<close> and gcd_l
  1.1399 -  have "?gcd * ?l \<noteq> 0" by simp
  1.1400 +  from \<open>n \<noteq> 0\<close> and gcd_l have "?gcd * ?l \<noteq> 0" by simp
  1.1401    then have "?l \<noteq> 0" by (blast dest!: mult_not_zero)
  1.1402    moreover
  1.1403    have "\<bar>x\<bar> = real ?k / real ?l"
  1.1404 @@ -1237,19 +1245,22 @@
  1.1405    ultimately show ?thesis ..
  1.1406  qed
  1.1407  
  1.1408 -subsection\<open>Density of the Rational Reals in the Reals\<close>
  1.1409 +
  1.1410 +subsection \<open>Density of the Rational Reals in the Reals\<close>
  1.1411  
  1.1412 -text\<open>This density proof is due to Stefan Richter and was ported by TN.  The
  1.1413 -original source is \emph{Real Analysis} by H.L. Royden.
  1.1414 -It employs the Archimedean property of the reals.\<close>
  1.1415 +text \<open>
  1.1416 +  This density proof is due to Stefan Richter and was ported by TN.  The
  1.1417 +  original source is \emph{Real Analysis} by H.L. Royden.
  1.1418 +  It employs the Archimedean property of the reals.\<close>
  1.1419  
  1.1420  lemma Rats_dense_in_real:
  1.1421    fixes x :: real
  1.1422 -  assumes "x < y" shows "\<exists>r\<in>\<rat>. x < r \<and> r < y"
  1.1423 +  assumes "x < y"
  1.1424 +  shows "\<exists>r\<in>\<rat>. x < r \<and> r < y"
  1.1425  proof -
  1.1426 -  from \<open>x<y\<close> have "0 < y-x" by simp
  1.1427 -  with reals_Archimedean obtain q::nat
  1.1428 -    where q: "inverse (real q) < y-x" and "0 < q" by blast
  1.1429 +  from \<open>x < y\<close> have "0 < y - x" by simp
  1.1430 +  with reals_Archimedean obtain q :: nat where q: "inverse (real q) < y - x" and "0 < q"
  1.1431 +    by blast
  1.1432    define p where "p = \<lceil>y * real q\<rceil> - 1"
  1.1433    define r where "r = of_int p / real q"
  1.1434    from q have "x < y - inverse (real q)" by simp
  1.1435 @@ -1259,8 +1270,7 @@
  1.1436    finally have "x < r" .
  1.1437    moreover have "r < y"
  1.1438      unfolding r_def p_def
  1.1439 -    by (simp add: divide_less_eq diff_less_eq \<open>0 < q\<close>
  1.1440 -      less_ceiling_iff [symmetric])
  1.1441 +    by (simp add: divide_less_eq diff_less_eq \<open>0 < q\<close> less_ceiling_iff [symmetric])
  1.1442    moreover from r_def have "r \<in> \<rat>" by simp
  1.1443    ultimately show ?thesis by blast
  1.1444  qed
  1.1445 @@ -1269,11 +1279,11 @@
  1.1446    fixes x y :: real
  1.1447    assumes "x < y"
  1.1448    shows "\<exists>q :: rat. x < of_rat q \<and> of_rat q < y"
  1.1449 -using Rats_dense_in_real [OF \<open>x < y\<close>]
  1.1450 -by (auto elim: Rats_cases)
  1.1451 +  using Rats_dense_in_real [OF \<open>x < y\<close>]
  1.1452 +  by (auto elim: Rats_cases)
  1.1453  
  1.1454  
  1.1455 -subsection\<open>Numerals and Arithmetic\<close>
  1.1456 +subsection \<open>Numerals and Arithmetic\<close>
  1.1457  
  1.1458  lemma [code_abbrev]:   (*FIXME*)
  1.1459    "real_of_int (numeral k) = numeral k"
  1.1460 @@ -1294,147 +1304,140 @@
  1.1461    #> Lin_Arith.add_inj_const (@{const_name of_int}, @{typ "int \<Rightarrow> real"}))
  1.1462  \<close>
  1.1463  
  1.1464 -subsection\<open>Simprules combining x+y and 0: ARE THEY NEEDED?\<close>
  1.1465 +
  1.1466 +subsection \<open>Simprules combining \<open>x + y\<close> and \<open>0\<close>\<close> (* FIXME ARE THEY NEEDED? *)
  1.1467  
  1.1468 -lemma real_add_minus_iff [simp]: "(x + - a = (0::real)) = (x=a)"
  1.1469 -by arith
  1.1470 +lemma real_add_minus_iff [simp]: "x + - a = 0 \<longleftrightarrow> x = a" for x a :: real
  1.1471 +  by arith
  1.1472  
  1.1473 -lemma real_add_less_0_iff: "(x+y < (0::real)) = (y < -x)"
  1.1474 -by auto
  1.1475 +lemma real_add_less_0_iff: "x + y < 0 \<longleftrightarrow> y < - x" for x y :: real
  1.1476 +  by auto
  1.1477  
  1.1478 -lemma real_0_less_add_iff: "((0::real) < x+y) = (-x < y)"
  1.1479 -by auto
  1.1480 +lemma real_0_less_add_iff: "0 < x + y \<longleftrightarrow> - x < y" for x y :: real
  1.1481 +  by auto
  1.1482  
  1.1483 -lemma real_add_le_0_iff: "(x+y \<le> (0::real)) = (y \<le> -x)"
  1.1484 -by auto
  1.1485 +lemma real_add_le_0_iff: "x + y \<le> 0 \<longleftrightarrow> y \<le> - x" for x y :: real
  1.1486 +  by auto
  1.1487  
  1.1488 -lemma real_0_le_add_iff: "((0::real) \<le> x+y) = (-x \<le> y)"
  1.1489 -by auto
  1.1490 +lemma real_0_le_add_iff: "0 \<le> x + y \<longleftrightarrow> - x \<le> y" for x y :: real
  1.1491 +  by auto
  1.1492 +
  1.1493  
  1.1494  subsection \<open>Lemmas about powers\<close>
  1.1495  
  1.1496  lemma two_realpow_ge_one: "(1::real) \<le> 2 ^ n"
  1.1497    by simp
  1.1498  
  1.1499 -text \<open>FIXME: declare this [simp] for all types, or not at all\<close>
  1.1500 +(* FIXME: declare this [simp] for all types, or not at all *)
  1.1501  declare sum_squares_eq_zero_iff [simp] sum_power2_eq_zero_iff [simp]
  1.1502  
  1.1503 -lemma real_minus_mult_self_le [simp]: "-(u * u) \<le> (x * (x::real))"
  1.1504 -by (rule_tac y = 0 in order_trans, auto)
  1.1505 +lemma real_minus_mult_self_le [simp]: "- (u * u) \<le> x * x" for u x :: real
  1.1506 +  by (rule order_trans [where y = 0]) auto
  1.1507  
  1.1508 -lemma realpow_square_minus_le [simp]: "- u\<^sup>2 \<le> (x::real)\<^sup>2"
  1.1509 +lemma realpow_square_minus_le [simp]: "- u\<^sup>2 \<le> x\<^sup>2" for u x :: real
  1.1510    by (auto simp add: power2_eq_square)
  1.1511  
  1.1512 -lemma numeral_power_eq_real_of_int_cancel_iff[simp]:
  1.1513 -     "numeral x ^ n = real_of_int (y::int) \<longleftrightarrow> numeral x ^ n = y"
  1.1514 +lemma numeral_power_eq_real_of_int_cancel_iff [simp]:
  1.1515 +  "numeral x ^ n = real_of_int y \<longleftrightarrow> numeral x ^ n = y"
  1.1516    by (metis of_int_eq_iff of_int_numeral of_int_power)
  1.1517  
  1.1518 -lemma real_of_int_eq_numeral_power_cancel_iff[simp]:
  1.1519 -     "real_of_int (y::int) = numeral x ^ n \<longleftrightarrow> y = numeral x ^ n"
  1.1520 -  using numeral_power_eq_real_of_int_cancel_iff[of x n y]
  1.1521 -  by metis
  1.1522 +lemma real_of_int_eq_numeral_power_cancel_iff [simp]:
  1.1523 +  "real_of_int y = numeral x ^ n \<longleftrightarrow> y = numeral x ^ n"
  1.1524 +  using numeral_power_eq_real_of_int_cancel_iff [of x n y] by metis
  1.1525  
  1.1526 -lemma numeral_power_eq_real_of_nat_cancel_iff[simp]:
  1.1527 -     "numeral x ^ n = real (y::nat) \<longleftrightarrow> numeral x ^ n = y"
  1.1528 +lemma numeral_power_eq_real_of_nat_cancel_iff [simp]:
  1.1529 +  "numeral x ^ n = real y \<longleftrightarrow> numeral x ^ n = y"
  1.1530    using of_nat_eq_iff by fastforce
  1.1531  
  1.1532 -lemma real_of_nat_eq_numeral_power_cancel_iff[simp]:
  1.1533 -  "real (y::nat) = numeral x ^ n \<longleftrightarrow> y = numeral x ^ n"
  1.1534 -  using numeral_power_eq_real_of_nat_cancel_iff[of x n y]
  1.1535 -  by metis
  1.1536 +lemma real_of_nat_eq_numeral_power_cancel_iff [simp]:
  1.1537 +  "real y = numeral x ^ n \<longleftrightarrow> y = numeral x ^ n"
  1.1538 +  using numeral_power_eq_real_of_nat_cancel_iff [of x n y] by metis
  1.1539  
  1.1540 -lemma numeral_power_le_real_of_nat_cancel_iff[simp]:
  1.1541 -  "(numeral x::real) ^ n \<le> real a \<longleftrightarrow> (numeral x::nat) ^ n \<le> a"
  1.1542 -by (metis of_nat_le_iff of_nat_numeral of_nat_power)
  1.1543 +lemma numeral_power_le_real_of_nat_cancel_iff [simp]:
  1.1544 +  "(numeral x :: real) ^ n \<le> real a \<longleftrightarrow> (numeral x::nat) ^ n \<le> a"
  1.1545 +  by (metis of_nat_le_iff of_nat_numeral of_nat_power)
  1.1546  
  1.1547 -lemma real_of_nat_le_numeral_power_cancel_iff[simp]:
  1.1548 +lemma real_of_nat_le_numeral_power_cancel_iff [simp]:
  1.1549    "real a \<le> (numeral x::real) ^ n \<longleftrightarrow> a \<le> (numeral x::nat) ^ n"
  1.1550 -by (metis of_nat_le_iff of_nat_numeral of_nat_power)
  1.1551 +  by (metis of_nat_le_iff of_nat_numeral of_nat_power)
  1.1552  
  1.1553 -lemma numeral_power_le_real_of_int_cancel_iff[simp]:
  1.1554 -    "(numeral x::real) ^ n \<le> real_of_int a \<longleftrightarrow> (numeral x::int) ^ n \<le> a"
  1.1555 +lemma numeral_power_le_real_of_int_cancel_iff [simp]:
  1.1556 +  "(numeral x::real) ^ n \<le> real_of_int a \<longleftrightarrow> (numeral x::int) ^ n \<le> a"
  1.1557    by (metis ceiling_le_iff ceiling_of_int of_int_numeral of_int_power)
  1.1558  
  1.1559 -lemma real_of_int_le_numeral_power_cancel_iff[simp]:
  1.1560 -    "real_of_int a \<le> (numeral x::real) ^ n \<longleftrightarrow> a \<le> (numeral x::int) ^ n"
  1.1561 +lemma real_of_int_le_numeral_power_cancel_iff [simp]:
  1.1562 +  "real_of_int a \<le> (numeral x::real) ^ n \<longleftrightarrow> a \<le> (numeral x::int) ^ n"
  1.1563    by (metis floor_of_int le_floor_iff of_int_numeral of_int_power)
  1.1564  
  1.1565 -lemma numeral_power_less_real_of_nat_cancel_iff[simp]:
  1.1566 -    "(numeral x::real) ^ n < real a \<longleftrightarrow> (numeral x::nat) ^ n < a"
  1.1567 +lemma numeral_power_less_real_of_nat_cancel_iff [simp]:
  1.1568 +  "(numeral x::real) ^ n < real a \<longleftrightarrow> (numeral x::nat) ^ n < a"
  1.1569 +  by (metis of_nat_less_iff of_nat_numeral of_nat_power)
  1.1570 +
  1.1571 +lemma real_of_nat_less_numeral_power_cancel_iff [simp]:
  1.1572 +  "real a < (numeral x::real) ^ n \<longleftrightarrow> a < (numeral x::nat) ^ n"
  1.1573    by (metis of_nat_less_iff of_nat_numeral of_nat_power)
  1.1574  
  1.1575 -lemma real_of_nat_less_numeral_power_cancel_iff[simp]:
  1.1576 -  "real a < (numeral x::real) ^ n \<longleftrightarrow> a < (numeral x::nat) ^ n"
  1.1577 -by (metis of_nat_less_iff of_nat_numeral of_nat_power)
  1.1578 -
  1.1579 -lemma numeral_power_less_real_of_int_cancel_iff[simp]:
  1.1580 -    "(numeral x::real) ^ n < real_of_int a \<longleftrightarrow> (numeral x::int) ^ n < a"
  1.1581 +lemma numeral_power_less_real_of_int_cancel_iff [simp]:
  1.1582 +  "(numeral x::real) ^ n < real_of_int a \<longleftrightarrow> (numeral x::int) ^ n < a"
  1.1583    by (meson not_less real_of_int_le_numeral_power_cancel_iff)
  1.1584  
  1.1585 -lemma real_of_int_less_numeral_power_cancel_iff[simp]:
  1.1586 -     "real_of_int a < (numeral x::real) ^ n \<longleftrightarrow> a < (numeral x::int) ^ n"
  1.1587 +lemma real_of_int_less_numeral_power_cancel_iff [simp]:
  1.1588 +  "real_of_int a < (numeral x::real) ^ n \<longleftrightarrow> a < (numeral x::int) ^ n"
  1.1589    by (meson not_less numeral_power_le_real_of_int_cancel_iff)
  1.1590  
  1.1591 -lemma neg_numeral_power_le_real_of_int_cancel_iff[simp]:
  1.1592 -    "(- numeral x::real) ^ n \<le> real_of_int a \<longleftrightarrow> (- numeral x::int) ^ n \<le> a"
  1.1593 +lemma neg_numeral_power_le_real_of_int_cancel_iff [simp]:
  1.1594 +  "(- numeral x::real) ^ n \<le> real_of_int a \<longleftrightarrow> (- numeral x::int) ^ n \<le> a"
  1.1595    by (metis of_int_le_iff of_int_neg_numeral of_int_power)
  1.1596  
  1.1597 -lemma real_of_int_le_neg_numeral_power_cancel_iff[simp]:
  1.1598 -     "real_of_int a \<le> (- numeral x::real) ^ n \<longleftrightarrow> a \<le> (- numeral x::int) ^ n"
  1.1599 +lemma real_of_int_le_neg_numeral_power_cancel_iff [simp]:
  1.1600 +  "real_of_int a \<le> (- numeral x::real) ^ n \<longleftrightarrow> a \<le> (- numeral x::int) ^ n"
  1.1601    by (metis of_int_le_iff of_int_neg_numeral of_int_power)
  1.1602  
  1.1603  
  1.1604 -subsection\<open>Density of the Reals\<close>
  1.1605 +subsection \<open>Density of the Reals\<close>
  1.1606 +
  1.1607 +lemma real_lbound_gt_zero: "0 < d1 \<Longrightarrow> 0 < d2 \<Longrightarrow> \<exists>e. 0 < e \<and> e < d1 \<and> e < d2" for d1 d2 :: real
  1.1608 +  by (rule exI [where x = "min d1 d2 / 2"]) (simp add: min_def)
  1.1609  
  1.1610 -lemma real_lbound_gt_zero:
  1.1611 -     "[| (0::real) < d1; 0 < d2 |] ==> \<exists>e. 0 < e & e < d1 & e < d2"
  1.1612 -apply (rule_tac x = " (min d1 d2) /2" in exI)
  1.1613 -apply (simp add: min_def)
  1.1614 -done
  1.1615 +text \<open>Similar results are proved in @{theory Fields}\<close>
  1.1616 +lemma real_less_half_sum: "x < y \<Longrightarrow> x < (x + y) / 2" for x y :: real
  1.1617 +  by auto
  1.1618 +
  1.1619 +lemma real_gt_half_sum: "x < y \<Longrightarrow> (x + y) / 2 < y" for x y :: real
  1.1620 +  by auto
  1.1621 +
  1.1622 +lemma real_sum_of_halves: "x / 2 + x / 2 = x" for x :: real
  1.1623 +  by simp
  1.1624  
  1.1625  
  1.1626 -text\<open>Similar results are proved in \<open>Fields\<close>\<close>
  1.1627 -lemma real_less_half_sum: "x < y ==> x < (x+y) / (2::real)"
  1.1628 -  by auto
  1.1629 -
  1.1630 -lemma real_gt_half_sum: "x < y ==> (x+y)/(2::real) < y"
  1.1631 -  by auto
  1.1632 -
  1.1633 -lemma real_sum_of_halves: "x/2 + x/2 = (x::real)"
  1.1634 -  by simp
  1.1635 -
  1.1636 -subsection\<open>Floor and Ceiling Functions from the Reals to the Integers\<close>
  1.1637 +subsection \<open>Floor and Ceiling Functions from the Reals to the Integers\<close>
  1.1638  
  1.1639  (* FIXME: theorems for negative numerals. Many duplicates, e.g. from Archimedean_Field.thy. *)
  1.1640  
  1.1641 -lemma real_of_nat_less_numeral_iff [simp]:
  1.1642 -     "real (n::nat) < numeral w \<longleftrightarrow> n < numeral w"
  1.1643 +lemma real_of_nat_less_numeral_iff [simp]: "real n < numeral w \<longleftrightarrow> n < numeral w" for n :: nat
  1.1644    by (metis of_nat_less_iff of_nat_numeral)
  1.1645  
  1.1646 -lemma numeral_less_real_of_nat_iff [simp]:
  1.1647 -     "numeral w < real (n::nat) \<longleftrightarrow> numeral w < n"
  1.1648 +lemma numeral_less_real_of_nat_iff [simp]: "numeral w < real n \<longleftrightarrow> numeral w < n" for n :: nat
  1.1649    by (metis of_nat_less_iff of_nat_numeral)
  1.1650  
  1.1651 -lemma numeral_le_real_of_nat_iff[simp]:
  1.1652 -  "(numeral n \<le> real(m::nat)) = (numeral n \<le> m)"
  1.1653 -by (metis not_le real_of_nat_less_numeral_iff)
  1.1654 +lemma numeral_le_real_of_nat_iff [simp]: "numeral n \<le> real m \<longleftrightarrow> numeral n \<le> m" for m :: nat
  1.1655 +  by (metis not_le real_of_nat_less_numeral_iff)
  1.1656  
  1.1657 -declare of_int_floor_le [simp] (* FIXME*)
  1.1658 +declare of_int_floor_le [simp]  (* FIXME duplicate!? *)
  1.1659  
  1.1660 -lemma of_int_floor_cancel [simp]:
  1.1661 -    "(of_int \<lfloor>x\<rfloor> = x) = (\<exists>n::int. x = of_int n)"
  1.1662 +lemma of_int_floor_cancel [simp]: "of_int \<lfloor>x\<rfloor> = x \<longleftrightarrow> (\<exists>n::int. x = of_int n)"
  1.1663    by (metis floor_of_int)
  1.1664  
  1.1665 -lemma floor_eq: "[| real_of_int n < x; x < real_of_int n + 1 |] ==> \<lfloor>x\<rfloor> = n"
  1.1666 +lemma floor_eq: "real_of_int n < x \<Longrightarrow> x < real_of_int n + 1 \<Longrightarrow> \<lfloor>x\<rfloor> = n"
  1.1667    by linarith
  1.1668  
  1.1669 -lemma floor_eq2: "[| real_of_int n \<le> x; x < real_of_int n + 1 |] ==> \<lfloor>x\<rfloor> = n"
  1.1670 +lemma floor_eq2: "real_of_int n \<le> x \<Longrightarrow> x < real_of_int n + 1 \<Longrightarrow> \<lfloor>x\<rfloor> = n"
  1.1671    by linarith
  1.1672  
  1.1673 -lemma floor_eq3: "[| real n < x; x < real (Suc n) |] ==> nat \<lfloor>x\<rfloor> = n"
  1.1674 +lemma floor_eq3: "real n < x \<Longrightarrow> x < real (Suc n) \<Longrightarrow> nat \<lfloor>x\<rfloor> = n"
  1.1675    by linarith
  1.1676  
  1.1677 -lemma floor_eq4: "[| real n \<le> x; x < real (Suc n) |] ==> nat \<lfloor>x\<rfloor> = n"
  1.1678 +lemma floor_eq4: "real n \<le> x \<Longrightarrow> x < real (Suc n) \<Longrightarrow> nat \<lfloor>x\<rfloor> = n"
  1.1679    by linarith
  1.1680  
  1.1681  lemma real_of_int_floor_ge_diff_one [simp]: "r - 1 \<le> real_of_int \<lfloor>r\<rfloor>"
  1.1682 @@ -1455,41 +1458,52 @@
  1.1683  lemma floor_add2[simp]: "\<lfloor>of_int a + x\<rfloor> = a + \<lfloor>x\<rfloor>"
  1.1684    by (simp add: add.commute)
  1.1685  
  1.1686 -lemma floor_divide_real_eq_div: "0 \<le> b \<Longrightarrow> \<lfloor>a / real_of_int b\<rfloor> = \<lfloor>a\<rfloor> div b"
  1.1687 -proof cases
  1.1688 -  assume "0 < b"
  1.1689 -  { fix i j :: int assume "real_of_int i \<le> a" "a < 1 + real_of_int i"
  1.1690 +lemma floor_divide_real_eq_div:
  1.1691 +  assumes "0 \<le> b"
  1.1692 +  shows "\<lfloor>a / real_of_int b\<rfloor> = \<lfloor>a\<rfloor> div b"
  1.1693 +proof (cases "b = 0")
  1.1694 +  case True
  1.1695 +  then show ?thesis by simp
  1.1696 +next
  1.1697 +  case False
  1.1698 +  with assms have b: "b > 0" by simp
  1.1699 +  have "j = i div b"
  1.1700 +    if "real_of_int i \<le> a" "a < 1 + real_of_int i"
  1.1701        "real_of_int j * real_of_int b \<le> a" "a < real_of_int b + real_of_int j * real_of_int b"
  1.1702 -    then have "i < b + j * b"
  1.1703 -      by (metis linorder_not_less of_int_add of_int_le_iff of_int_mult order_trans_rules(21))
  1.1704 +    for i j :: int
  1.1705 +  proof -
  1.1706 +    from that have "i < b + j * b"
  1.1707 +      by (metis le_less_trans of_int_add of_int_less_iff of_int_mult)
  1.1708      moreover have "j * b < 1 + i"
  1.1709      proof -
  1.1710        have "real_of_int (j * b) < real_of_int i + 1"
  1.1711          using \<open>a < 1 + real_of_int i\<close> \<open>real_of_int j * real_of_int b \<le> a\<close> by force
  1.1712 -      thus "j * b < 1 + i"
  1.1713 +      then show "j * b < 1 + i"
  1.1714          by linarith
  1.1715      qed
  1.1716      ultimately have "(j - i div b) * b \<le> i mod b" "i mod b < ((j - i div b) + 1) * b"
  1.1717        by (auto simp: field_simps)
  1.1718      then have "(j - i div b) * b < 1 * b" "0 * b < ((j - i div b) + 1) * b"
  1.1719 -      using pos_mod_bound[OF \<open>0<b\<close>, of i] pos_mod_sign[OF \<open>0<b\<close>, of i] by linarith+
  1.1720 -    then have "j = i div b"
  1.1721 -      using \<open>0 < b\<close> unfolding mult_less_cancel_right by auto
  1.1722 -  }
  1.1723 -  with \<open>0 < b\<close> show ?thesis
  1.1724 +      using pos_mod_bound [OF b, of i] pos_mod_sign [OF b, of i]
  1.1725 +      by linarith+
  1.1726 +    then show ?thesis
  1.1727 +      using b unfolding mult_less_cancel_right by auto
  1.1728 +  qed
  1.1729 +  with b show ?thesis
  1.1730      by (auto split: floor_split simp: field_simps)
  1.1731 -qed auto
  1.1732 +qed
  1.1733  
  1.1734 -lemma floor_divide_eq_div_numeral[simp]: "\<lfloor>numeral a / numeral b::real\<rfloor> = numeral a div numeral b"
  1.1735 +lemma floor_divide_eq_div_numeral [simp]: "\<lfloor>numeral a / numeral b::real\<rfloor> = numeral a div numeral b"
  1.1736    by (metis floor_divide_of_int_eq of_int_numeral)
  1.1737  
  1.1738 -lemma floor_minus_divide_eq_div_numeral[simp]: "\<lfloor>- (numeral a / numeral b)::real\<rfloor> = - numeral a div numeral b"
  1.1739 +lemma floor_minus_divide_eq_div_numeral [simp]:
  1.1740 +  "\<lfloor>- (numeral a / numeral b)::real\<rfloor> = - numeral a div numeral b"
  1.1741    by (metis divide_minus_left floor_divide_of_int_eq of_int_neg_numeral of_int_numeral)
  1.1742  
  1.1743 -lemma of_int_ceiling_cancel [simp]: "(of_int \<lceil>x\<rceil> = x) = (\<exists>n::int. x = of_int n)"
  1.1744 +lemma of_int_ceiling_cancel [simp]: "of_int \<lceil>x\<rceil> = x \<longleftrightarrow> (\<exists>n::int. x = of_int n)"
  1.1745    using ceiling_of_int by metis
  1.1746  
  1.1747 -lemma ceiling_eq: "[| of_int n < x; x \<le> of_int n + 1 |] ==> \<lceil>x\<rceil> = n + 1"
  1.1748 +lemma ceiling_eq: "of_int n < x \<Longrightarrow> x \<le> of_int n + 1 \<Longrightarrow> \<lceil>x\<rceil> = n + 1"
  1.1749    by (simp add: ceiling_unique)
  1.1750  
  1.1751  lemma of_int_ceiling_diff_one_le [simp]: "of_int \<lceil>r\<rceil> - 1 \<le> r"
  1.1752 @@ -1498,7 +1512,7 @@
  1.1753  lemma of_int_ceiling_le_add_one [simp]: "of_int \<lceil>r\<rceil> \<le> r + 1"
  1.1754    by linarith
  1.1755  
  1.1756 -lemma ceiling_le: "x <= of_int a ==> \<lceil>x\<rceil> <= a"
  1.1757 +lemma ceiling_le: "x \<le> of_int a \<Longrightarrow> \<lceil>x\<rceil> \<le> a"
  1.1758    by (simp add: ceiling_le_iff)
  1.1759  
  1.1760  lemma ceiling_divide_eq_div: "\<lceil>of_int a / of_int b\<rceil> = - (- a div b)"
  1.1761 @@ -1512,34 +1526,37 @@
  1.1762    "\<lceil>- (numeral a / numeral b :: real)\<rceil> = - (numeral a div numeral b)"
  1.1763    using ceiling_divide_eq_div[of "- numeral a" "numeral b"] by simp
  1.1764  
  1.1765 -text\<open>The following lemmas are remnants of the erstwhile functions natfloor
  1.1766 -and natceiling.\<close>
  1.1767 +text \<open>
  1.1768 +  The following lemmas are remnants of the erstwhile functions natfloor
  1.1769 +  and natceiling.
  1.1770 +\<close>
  1.1771  
  1.1772 -lemma nat_floor_neg: "(x::real) <= 0 ==> nat \<lfloor>x\<rfloor> = 0"
  1.1773 +lemma nat_floor_neg: "x \<le> 0 \<Longrightarrow> nat \<lfloor>x\<rfloor> = 0" for x :: real
  1.1774    by linarith
  1.1775  
  1.1776 -lemma le_nat_floor: "real x <= a ==> x <= nat \<lfloor>a\<rfloor>"
  1.1777 +lemma le_nat_floor: "real x \<le> a \<Longrightarrow> x \<le> nat \<lfloor>a\<rfloor>"
  1.1778    by linarith
  1.1779  
  1.1780  lemma le_mult_nat_floor: "nat \<lfloor>a\<rfloor> * nat \<lfloor>b\<rfloor> \<le> nat \<lfloor>a * b\<rfloor>"
  1.1781 -  by (cases "0 <= a & 0 <= b")
  1.1782 +  by (cases "0 \<le> a \<and> 0 \<le> b")
  1.1783       (auto simp add: nat_mult_distrib[symmetric] nat_mono le_mult_floor)
  1.1784  
  1.1785 -lemma nat_ceiling_le_eq [simp]: "(nat \<lceil>x\<rceil> <= a) = (x <= real a)"
  1.1786 +lemma nat_ceiling_le_eq [simp]: "nat \<lceil>x\<rceil> \<le> a \<longleftrightarrow> x \<le> real a"
  1.1787    by linarith
  1.1788  
  1.1789 -lemma real_nat_ceiling_ge: "x <= real (nat \<lceil>x\<rceil>)"
  1.1790 +lemma real_nat_ceiling_ge: "x \<le> real (nat \<lceil>x\<rceil>)"
  1.1791    by linarith
  1.1792  
  1.1793 -lemma Rats_no_top_le: "\<exists> q \<in> \<rat>. (x :: real) \<le> q"
  1.1794 +lemma Rats_no_top_le: "\<exists>q \<in> \<rat>. x \<le> q" for x :: real
  1.1795    by (auto intro!: bexI[of _ "of_nat (nat \<lceil>x\<rceil>)"]) linarith
  1.1796  
  1.1797 -lemma Rats_no_bot_less: "\<exists> q \<in> \<rat>. q < (x :: real)"
  1.1798 +lemma Rats_no_bot_less: "\<exists>q \<in> \<rat>. q < x" for x :: real
  1.1799    apply (auto intro!: bexI[of _ "of_int (\<lfloor>x\<rfloor> - 1)"])
  1.1800    apply (rule less_le_trans[OF _ of_int_floor_le])
  1.1801    apply simp
  1.1802    done
  1.1803  
  1.1804 +
  1.1805  subsection \<open>Exponentiation with floor\<close>
  1.1806  
  1.1807  lemma floor_power:
  1.1808 @@ -1551,48 +1568,41 @@
  1.1809    then show ?thesis by (metis floor_of_int)
  1.1810  qed
  1.1811  
  1.1812 -lemma floor_numeral_power[simp]:
  1.1813 -  "\<lfloor>numeral x ^ n\<rfloor> = numeral x ^ n"
  1.1814 +lemma floor_numeral_power [simp]: "\<lfloor>numeral x ^ n\<rfloor> = numeral x ^ n"
  1.1815    by (metis floor_of_int of_int_numeral of_int_power)
  1.1816  
  1.1817 -lemma ceiling_numeral_power[simp]:
  1.1818 -  "\<lceil>numeral x ^ n\<rceil> = numeral x ^ n"
  1.1819 +lemma ceiling_numeral_power [simp]: "\<lceil>numeral x ^ n\<rceil> = numeral x ^ n"
  1.1820    by (metis ceiling_of_int of_int_numeral of_int_power)
  1.1821  
  1.1822 +
  1.1823  subsection \<open>Implementation of rational real numbers\<close>
  1.1824  
  1.1825  text \<open>Formal constructor\<close>
  1.1826  
  1.1827 -definition Ratreal :: "rat \<Rightarrow> real" where
  1.1828 -  [code_abbrev, simp]: "Ratreal = of_rat"
  1.1829 +definition Ratreal :: "rat \<Rightarrow> real"
  1.1830 +  where [code_abbrev, simp]: "Ratreal = of_rat"
  1.1831  
  1.1832  code_datatype Ratreal
  1.1833  
  1.1834  
  1.1835  text \<open>Numerals\<close>
  1.1836  
  1.1837 -lemma [code_abbrev]:
  1.1838 -  "(of_rat (of_int a) :: real) = of_int a"
  1.1839 +lemma [code_abbrev]: "(of_rat (of_int a) :: real) = of_int a"
  1.1840    by simp
  1.1841  
  1.1842 -lemma [code_abbrev]:
  1.1843 -  "(of_rat 0 :: real) = 0"
  1.1844 +lemma [code_abbrev]: "(of_rat 0 :: real) = 0"
  1.1845    by simp
  1.1846  
  1.1847 -lemma [code_abbrev]:
  1.1848 -  "(of_rat 1 :: real) = 1"
  1.1849 +lemma [code_abbrev]: "(of_rat 1 :: real) = 1"
  1.1850    by simp
  1.1851  
  1.1852 -lemma [code_abbrev]:
  1.1853 -  "(of_rat (- 1) :: real) = - 1"
  1.1854 +lemma [code_abbrev]: "(of_rat (- 1) :: real) = - 1"
  1.1855    by simp
  1.1856  
  1.1857 -lemma [code_abbrev]:
  1.1858 -  "(of_rat (numeral k) :: real) = numeral k"
  1.1859 +lemma [code_abbrev]: "(of_rat (numeral k) :: real) = numeral k"
  1.1860    by simp
  1.1861  
  1.1862 -lemma [code_abbrev]:
  1.1863 -  "(of_rat (- numeral k) :: real) = - numeral k"
  1.1864 +lemma [code_abbrev]: "(of_rat (- numeral k) :: real) = - numeral k"
  1.1865    by simp
  1.1866  
  1.1867  lemma [code_post]:
  1.1868 @@ -1605,28 +1615,23 @@
  1.1869  
  1.1870  text \<open>Operations\<close>
  1.1871  
  1.1872 -lemma zero_real_code [code]:
  1.1873 -  "0 = Ratreal 0"
  1.1874 +lemma zero_real_code [code]: "0 = Ratreal 0"
  1.1875  by simp
  1.1876  
  1.1877 -lemma one_real_code [code]:
  1.1878 -  "1 = Ratreal 1"
  1.1879 +lemma one_real_code [code]: "1 = Ratreal 1"
  1.1880  by simp
  1.1881  
  1.1882  instantiation real :: equal
  1.1883  begin
  1.1884  
  1.1885 -definition "HOL.equal (x::real) y \<longleftrightarrow> x - y = 0"
  1.1886 +definition "HOL.equal x y \<longleftrightarrow> x - y = 0" for x :: real
  1.1887  
  1.1888 -instance proof
  1.1889 -qed (simp add: equal_real_def)
  1.1890 +instance by standard (simp add: equal_real_def)
  1.1891  
  1.1892 -lemma real_equal_code [code]:
  1.1893 -  "HOL.equal (Ratreal x) (Ratreal y) \<longleftrightarrow> HOL.equal x y"
  1.1894 +lemma real_equal_code [code]: "HOL.equal (Ratreal x) (Ratreal y) \<longleftrightarrow> HOL.equal x y"
  1.1895    by (simp add: equal_real_def equal)
  1.1896  
  1.1897 -lemma [code nbe]:
  1.1898 -  "HOL.equal (x::real) x \<longleftrightarrow> True"
  1.1899 +lemma [code nbe]: "HOL.equal x x \<longleftrightarrow> True" for x :: real
  1.1900    by (rule equal_refl)
  1.1901  
  1.1902  end
  1.1903 @@ -1656,14 +1661,15 @@
  1.1904    by (simp add: of_rat_divide)
  1.1905  
  1.1906  lemma real_floor_code [code]: "\<lfloor>Ratreal x\<rfloor> = \<lfloor>x\<rfloor>"
  1.1907 -  by (metis Ratreal_def floor_le_iff floor_unique le_floor_iff of_int_floor_le of_rat_of_int_eq real_less_eq_code)
  1.1908 +  by (metis Ratreal_def floor_le_iff floor_unique le_floor_iff
  1.1909 +      of_int_floor_le of_rat_of_int_eq real_less_eq_code)
  1.1910  
  1.1911  
  1.1912  text \<open>Quickcheck\<close>
  1.1913  
  1.1914  definition (in term_syntax)
  1.1915 -  valterm_ratreal :: "rat \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow> real \<times> (unit \<Rightarrow> Code_Evaluation.term)" where
  1.1916 -  [code_unfold]: "valterm_ratreal k = Code_Evaluation.valtermify Ratreal {\<cdot>} k"
  1.1917 +  valterm_ratreal :: "rat \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow> real \<times> (unit \<Rightarrow> Code_Evaluation.term)"
  1.1918 +  where [code_unfold]: "valterm_ratreal k = Code_Evaluation.valtermify Ratreal {\<cdot>} k"
  1.1919  
  1.1920  notation fcomp (infixl "\<circ>>" 60)
  1.1921  notation scomp (infixl "\<circ>\<rightarrow>" 60)
  1.1922 @@ -1685,7 +1691,7 @@
  1.1923  begin
  1.1924  
  1.1925  definition
  1.1926 -  "exhaustive_real f d = Quickcheck_Exhaustive.exhaustive (%r. f (Ratreal r)) d"
  1.1927 +  "exhaustive_real f d = Quickcheck_Exhaustive.exhaustive (\<lambda>r. f (Ratreal r)) d"
  1.1928  
  1.1929  instance ..
  1.1930  
  1.1931 @@ -1695,7 +1701,7 @@
  1.1932  begin
  1.1933  
  1.1934  definition
  1.1935 -  "full_exhaustive_real f d = Quickcheck_Exhaustive.full_exhaustive (%r. f (valterm_ratreal r)) d"
  1.1936 +  "full_exhaustive_real f d = Quickcheck_Exhaustive.full_exhaustive (\<lambda>r. f (valterm_ratreal r)) d"
  1.1937  
  1.1938  instance ..
  1.1939  
  1.1940 @@ -1705,7 +1711,7 @@
  1.1941  begin
  1.1942  
  1.1943  definition
  1.1944 -  "narrowing = Quickcheck_Narrowing.apply (Quickcheck_Narrowing.cons Ratreal) narrowing"
  1.1945 +  "narrowing_real = Quickcheck_Narrowing.apply (Quickcheck_Narrowing.cons Ratreal) narrowing"
  1.1946  
  1.1947  instance ..
  1.1948  
  1.1949 @@ -1727,9 +1733,9 @@
  1.1950  \<close>
  1.1951  
  1.1952  lemmas [nitpick_unfold] = inverse_real_inst.inverse_real one_real_inst.one_real
  1.1953 -    ord_real_inst.less_real ord_real_inst.less_eq_real plus_real_inst.plus_real
  1.1954 -    times_real_inst.times_real uminus_real_inst.uminus_real
  1.1955 -    zero_real_inst.zero_real
  1.1956 +  ord_real_inst.less_real ord_real_inst.less_eq_real plus_real_inst.plus_real
  1.1957 +  times_real_inst.times_real uminus_real_inst.uminus_real
  1.1958 +  zero_real_inst.zero_real
  1.1959  
  1.1960  
  1.1961  subsection \<open>Setup for SMT\<close>
  1.1962 @@ -1738,11 +1744,12 @@
  1.1963  ML_file "Tools/SMT/z3_real.ML"
  1.1964  
  1.1965  lemma [z3_rule]:
  1.1966 -  "0 + (x::real) = x"
  1.1967 +  "0 + x = x"
  1.1968    "x + 0 = x"
  1.1969    "0 * x = 0"
  1.1970    "1 * x = x"
  1.1971    "x + y = y + x"
  1.1972 +  for x y :: real
  1.1973    by auto
  1.1974  
  1.1975  end