src/HOL/Real.thy
changeset 63494 ac0a3b9c6dae
parent 63353 176d1f408696
child 63597 bef0277ec73b
     1.1 --- a/src/HOL/Real.thy	Thu Jul 14 12:21:12 2016 +0200
     1.2 +++ b/src/HOL/Real.thy	Fri Jul 15 11:07:51 2016 +0200
     1.3 @@ -23,19 +23,24 @@
     1.4  
     1.5  subsection \<open>Preliminary lemmas\<close>
     1.6  
     1.7 -lemma inj_add_left [simp]: "inj (op + x)" for x :: "'a::cancel_semigroup_add"
     1.8 +lemma inj_add_left [simp]: "inj (op + x)"
     1.9 +  for x :: "'a::cancel_semigroup_add"
    1.10    by (meson add_left_imp_eq injI)
    1.11  
    1.12 -lemma inj_mult_left [simp]: "inj (op * x) \<longleftrightarrow> x \<noteq> 0" for x :: "'a::idom"
    1.13 +lemma inj_mult_left [simp]: "inj (op * x) \<longleftrightarrow> x \<noteq> 0"
    1.14 +  for x :: "'a::idom"
    1.15    by (metis injI mult_cancel_left the_inv_f_f zero_neq_one)
    1.16  
    1.17 -lemma add_diff_add: "(a + c) - (b + d) = (a - b) + (c - d)" for a b c d :: "'a::ab_group_add"
    1.18 +lemma add_diff_add: "(a + c) - (b + d) = (a - b) + (c - d)"
    1.19 +  for a b c d :: "'a::ab_group_add"
    1.20    by simp
    1.21  
    1.22 -lemma minus_diff_minus: "- a - - b = - (a - b)" for a b :: "'a::ab_group_add"
    1.23 +lemma minus_diff_minus: "- a - - b = - (a - b)"
    1.24 +  for a b :: "'a::ab_group_add"
    1.25    by simp
    1.26  
    1.27 -lemma mult_diff_mult: "(x * y - a * b) = x * (y - b) + (x - a) * b" for x y a b :: "'a::ring"
    1.28 +lemma mult_diff_mult: "(x * y - a * b) = x * (y - b) + (x - a) * b"
    1.29 +  for x y a b :: "'a::ring"
    1.30    by (simp add: algebra_simps)
    1.31  
    1.32  lemma inverse_diff_inverse:
    1.33 @@ -68,7 +73,7 @@
    1.34  lemma vanishes_const [simp]: "vanishes (\<lambda>n. c) \<longleftrightarrow> c = 0"
    1.35    unfolding vanishes_def
    1.36    apply (cases "c = 0")
    1.37 -  apply auto
    1.38 +   apply auto
    1.39    apply (rule exI [where x = "\<bar>c\<bar>"])
    1.40    apply auto
    1.41    done
    1.42 @@ -93,9 +98,12 @@
    1.43    proof clarsimp
    1.44      fix n
    1.45      assume n: "i \<le> n" "j \<le> n"
    1.46 -    have "\<bar>X n + Y n\<bar> \<le> \<bar>X n\<bar> + \<bar>Y n\<bar>" by (rule abs_triangle_ineq)
    1.47 -    also have "\<dots> < s + t" by (simp add: add_strict_mono i j n)
    1.48 -    finally show "\<bar>X n + Y n\<bar> < r" unfolding r .
    1.49 +    have "\<bar>X n + Y n\<bar> \<le> \<bar>X n\<bar> + \<bar>Y n\<bar>"
    1.50 +      by (rule abs_triangle_ineq)
    1.51 +    also have "\<dots> < s + t"
    1.52 +      by (simp add: add_strict_mono i j n)
    1.53 +    finally show "\<bar>X n + Y n\<bar> < r"
    1.54 +      by (simp only: r)
    1.55    qed
    1.56    then show "\<exists>k. \<forall>n\<ge>k. \<bar>X n + Y n\<bar> < r" ..
    1.57  qed
    1.58 @@ -242,7 +250,8 @@
    1.59        unfolding abs_mult ..
    1.60      also have "\<dots> < a * t + s * b"
    1.61        by (simp_all add: add_strict_mono mult_strict_mono' a b i j *)
    1.62 -    finally show "\<bar>X m * Y m - X n * Y n\<bar> < r" by (simp only: r)
    1.63 +    finally show "\<bar>X m * Y m - X n * Y n\<bar> < r"
    1.64 +      by (simp only: r)
    1.65    qed
    1.66    then show "\<exists>k. \<forall>m\<ge>k. \<forall>n\<ge>k. \<bar>X m * Y m - X n * Y n\<bar> < r" ..
    1.67  qed
    1.68 @@ -273,7 +282,7 @@
    1.69  
    1.70  lemma cauchy_not_vanishes:
    1.71    assumes X: "cauchy X"
    1.72 -  assumes nz: "\<not> vanishes X"
    1.73 +    and nz: "\<not> vanishes X"
    1.74    shows "\<exists>b>0. \<exists>k. \<forall>n\<ge>k. b < \<bar>X n\<bar>"
    1.75    using cauchy_not_vanishes_cases [OF assms]
    1.76    apply clarify
    1.77 @@ -285,7 +294,7 @@
    1.78  
    1.79  lemma cauchy_inverse [simp]:
    1.80    assumes X: "cauchy X"
    1.81 -  assumes nz: "\<not> vanishes X"
    1.82 +    and nz: "\<not> vanishes X"
    1.83    shows "cauchy (\<lambda>n. inverse (X n))"
    1.84  proof (rule cauchyI)
    1.85    fix r :: rat
    1.86 @@ -328,8 +337,10 @@
    1.87      using cauchy_not_vanishes [OF Y] by blast
    1.88    obtain s where s: "0 < s" and "inverse a * s * inverse b = r"
    1.89    proof
    1.90 -    show "0 < a * r * b" using a r b by simp
    1.91 -    show "inverse a * (a * r * b) * inverse b = r" using a r b by simp
    1.92 +    show "0 < a * r * b"
    1.93 +      using a r b by simp
    1.94 +    show "inverse a * (a * r * b) * inverse b = r"
    1.95 +      using a r b by simp
    1.96    qed
    1.97    obtain k where k: "\<forall>n\<ge>k. \<bar>X n - Y n\<bar> < s"
    1.98      using vanishesD [OF XY s] ..
    1.99 @@ -435,16 +446,19 @@
   1.100    fix X Y
   1.101    assume "realrel X Y"
   1.102    then have X: "cauchy X" and Y: "cauchy Y" and XY: "vanishes (\<lambda>n. X n - Y n)"
   1.103 -    unfolding realrel_def by simp_all
   1.104 +    by (simp_all add: realrel_def)
   1.105    have "vanishes X \<longleftrightarrow> vanishes Y"
   1.106    proof
   1.107      assume "vanishes X"
   1.108 -    from vanishes_diff [OF this XY] show "vanishes Y" by simp
   1.109 +    from vanishes_diff [OF this XY] show "vanishes Y"
   1.110 +      by simp
   1.111    next
   1.112      assume "vanishes Y"
   1.113 -    from vanishes_add [OF this XY] show "vanishes X" by simp
   1.114 +    from vanishes_add [OF this XY] show "vanishes X"
   1.115 +      by simp
   1.116    qed
   1.117 -  then show "?thesis X Y" by (simp add: vanishes_diff_inverse X Y XY realrel_def)
   1.118 +  then show "?thesis X Y"
   1.119 +    by (simp add: vanishes_diff_inverse X Y XY realrel_def)
   1.120  qed
   1.121  
   1.122  definition "x - y = x + - y" for x y :: real
   1.123 @@ -495,9 +509,12 @@
   1.124      apply transfer
   1.125      apply (simp add: realrel_def)
   1.126      apply (rule vanishesI)
   1.127 -    apply (frule (1) cauchy_not_vanishes, clarify)
   1.128 -    apply (rule_tac x=k in exI, clarify)
   1.129 -    apply (drule_tac x=n in spec, simp)
   1.130 +    apply (frule (1) cauchy_not_vanishes)
   1.131 +    apply clarify
   1.132 +    apply (rule_tac x=k in exI)
   1.133 +    apply clarify
   1.134 +    apply (drule_tac x=n in spec)
   1.135 +    apply simp
   1.136      done
   1.137    show "a div b = a * inverse b"
   1.138      by (rule divide_real_def)
   1.139 @@ -567,14 +584,15 @@
   1.140    apply (rule_tac x = "max i j" in exI)
   1.141    apply clarsimp
   1.142    apply (rule mult_strict_mono)
   1.143 -  apply auto
   1.144 +     apply auto
   1.145    done
   1.146  
   1.147  lemma positive_minus: "\<not> positive x \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> positive (- x)"
   1.148    apply transfer
   1.149    apply (simp add: realrel_def)
   1.150 -  apply (drule (1) cauchy_not_vanishes_cases, safe)
   1.151 -  apply blast+
   1.152 +  apply (drule (1) cauchy_not_vanishes_cases)
   1.153 +  apply safe
   1.154 +   apply blast+
   1.155    done
   1.156  
   1.157  instantiation real :: linordered_field
   1.158 @@ -596,8 +614,8 @@
   1.159    show "a < b \<longleftrightarrow> a \<le> b \<and> \<not> b \<le> a"
   1.160      unfolding less_eq_real_def less_real_def
   1.161      apply auto
   1.162 -    apply (drule (1) positive_add)
   1.163 -    apply (simp_all add: positive_zero)
   1.164 +     apply (drule (1) positive_add)
   1.165 +     apply (simp_all add: positive_zero)
   1.166      done
   1.167    show "a \<le> a"
   1.168      unfolding less_eq_real_def by simp
   1.169 @@ -637,7 +655,8 @@
   1.170  
   1.171  definition "(sup :: real \<Rightarrow> real \<Rightarrow> real) = max"
   1.172  
   1.173 -instance by standard (auto simp add: inf_real_def sup_real_def max_min_distrib2)
   1.174 +instance
   1.175 +  by standard (auto simp add: inf_real_def sup_real_def max_min_distrib2)
   1.176  
   1.177  end
   1.178  
   1.179 @@ -656,15 +675,16 @@
   1.180  
   1.181  instance real :: archimedean_field
   1.182  proof
   1.183 -  fix x :: real
   1.184 -  show "\<exists>z. x \<le> of_int z"
   1.185 +  show "\<exists>z. x \<le> of_int z" for x :: real
   1.186      apply (induct x)
   1.187      apply (frule cauchy_imp_bounded, clarify)
   1.188      apply (rule_tac x="\<lceil>b\<rceil> + 1" in exI)
   1.189      apply (rule less_imp_le)
   1.190      apply (simp add: of_int_Real less_real_def diff_Real positive_Real)
   1.191 -    apply (rule_tac x=1 in exI, simp add: algebra_simps)
   1.192 -    apply (rule_tac x=0 in exI, clarsimp)
   1.193 +    apply (rule_tac x=1 in exI)
   1.194 +    apply (simp add: algebra_simps)
   1.195 +    apply (rule_tac x=0 in exI)
   1.196 +    apply clarsimp
   1.197      apply (rule le_less_trans [OF abs_ge_self])
   1.198      apply (rule less_le_trans [OF _ le_of_int_ceiling])
   1.199      apply simp
   1.200 @@ -687,26 +707,24 @@
   1.201  
   1.202  subsection \<open>Completeness\<close>
   1.203  
   1.204 -lemma not_positive_Real:
   1.205 -  assumes X: "cauchy X"
   1.206 -  shows "\<not> positive (Real X) \<longleftrightarrow> (\<forall>r>0. \<exists>k. \<forall>n\<ge>k. X n \<le> r)"
   1.207 -  unfolding positive_Real [OF X]
   1.208 +lemma not_positive_Real: "\<not> positive (Real X) \<longleftrightarrow> (\<forall>r>0. \<exists>k. \<forall>n\<ge>k. X n \<le> r)" if "cauchy X"
   1.209 +  apply (simp only: positive_Real [OF that])
   1.210    apply auto
   1.211 -  apply (unfold not_less)
   1.212 -  apply (erule obtain_pos_sum)
   1.213 -  apply (drule_tac x=s in spec)
   1.214 -  apply simp
   1.215 -  apply (drule_tac r=t in cauchyD [OF X])
   1.216 -  apply clarify
   1.217 -  apply (drule_tac x=k in spec)
   1.218 -  apply clarsimp
   1.219 -  apply (rule_tac x=n in exI)
   1.220 -  apply clarify
   1.221 -  apply (rename_tac m)
   1.222 -  apply (drule_tac x=m in spec)
   1.223 -  apply simp
   1.224 -  apply (drule_tac x=n in spec)
   1.225 -  apply simp
   1.226 +   apply (unfold not_less)
   1.227 +   apply (erule obtain_pos_sum)
   1.228 +   apply (drule_tac x=s in spec)
   1.229 +   apply simp
   1.230 +   apply (drule_tac r=t in cauchyD [OF that])
   1.231 +   apply clarify
   1.232 +   apply (drule_tac x=k in spec)
   1.233 +   apply clarsimp
   1.234 +   apply (rule_tac x=n in exI)
   1.235 +   apply clarify
   1.236 +   apply (rename_tac m)
   1.237 +   apply (drule_tac x=m in spec)
   1.238 +   apply simp
   1.239 +   apply (drule_tac x=n in spec)
   1.240 +   apply simp
   1.241    apply (drule spec)
   1.242    apply (drule (1) mp)
   1.243    apply clarify
   1.244 @@ -743,9 +761,12 @@
   1.245      proof clarsimp
   1.246        fix n
   1.247        assume n: "i \<le> n" "j \<le> n"
   1.248 -      have "X n \<le> Y i + t" using n j by simp
   1.249 -      moreover have "\<bar>Y i - Y n\<bar> < s" using n i by simp
   1.250 -      ultimately show "X n \<le> Y n + r" unfolding r by simp
   1.251 +      have "X n \<le> Y i + t"
   1.252 +        using n j by simp
   1.253 +      moreover have "\<bar>Y i - Y n\<bar> < s"
   1.254 +        using n i by simp
   1.255 +      ultimately show "X n \<le> Y n + r"
   1.256 +        unfolding r by simp
   1.257      qed
   1.258      then show ?thesis ..
   1.259    qed
   1.260 @@ -773,7 +794,7 @@
   1.261  
   1.262  lemma of_nat_less_two_power [simp]: "of_nat n < (2::'a::linordered_idom) ^ n"
   1.263    apply (induct n)
   1.264 -  apply simp
   1.265 +   apply simp
   1.266    apply (metis add_le_less_mono mult_2 of_nat_Suc one_le_numeral one_le_power power_Suc)
   1.267    done
   1.268  
   1.269 @@ -821,7 +842,7 @@
   1.270  
   1.271    have width: "B n - A n = (b - a) / 2^n" for n
   1.272      apply (induct n)
   1.273 -    apply (simp_all add: eq_divide_eq)
   1.274 +     apply (simp_all add: eq_divide_eq)
   1.275      apply (simp_all add: C_def avg_def algebra_simps)
   1.276      done
   1.277  
   1.278 @@ -833,13 +854,15 @@
   1.279      apply (rule_tac x=n in exI)
   1.280      apply (erule less_trans)
   1.281      apply (rule mult_strict_right_mono)
   1.282 -    apply (rule le_less_trans [OF _ of_nat_less_two_power])
   1.283 -    apply simp
   1.284 +     apply (rule le_less_trans [OF _ of_nat_less_two_power])
   1.285 +     apply simp
   1.286      apply assumption
   1.287      done
   1.288  
   1.289 -  have PA: "\<not> P (A n)" for n by (induct n) (simp_all add: a)
   1.290 -  have PB: "P (B n)" for n by (induct n) (simp_all add: b)
   1.291 +  have PA: "\<not> P (A n)" for n
   1.292 +    by (induct n) (simp_all add: a)
   1.293 +  have PB: "P (B n)" for n
   1.294 +    by (induct n) (simp_all add: b)
   1.295    have ab: "a < b"
   1.296      using a b unfolding P_def
   1.297      apply (clarsimp simp add: not_le)
   1.298 @@ -847,21 +870,22 @@
   1.299      apply (drule (1) less_le_trans)
   1.300      apply (simp add: of_rat_less)
   1.301      done
   1.302 -  have AB: "A n < B n" for n by (induct n) (simp_all add: ab C_def avg_def)
   1.303 +  have AB: "A n < B n" for n
   1.304 +    by (induct n) (simp_all add: ab C_def avg_def)
   1.305    have A_mono: "\<And>i j. i \<le> j \<Longrightarrow> A i \<le> A j"
   1.306      apply (auto simp add: le_less [where 'a=nat])
   1.307      apply (erule less_Suc_induct)
   1.308 -    apply (clarsimp simp add: C_def avg_def)
   1.309 -    apply (simp add: add_divide_distrib [symmetric])
   1.310 -    apply (rule AB [THEN less_imp_le])
   1.311 +     apply (clarsimp simp add: C_def avg_def)
   1.312 +     apply (simp add: add_divide_distrib [symmetric])
   1.313 +     apply (rule AB [THEN less_imp_le])
   1.314      apply simp
   1.315      done
   1.316    have B_mono: "\<And>i j. i \<le> j \<Longrightarrow> B j \<le> B i"
   1.317      apply (auto simp add: le_less [where 'a=nat])
   1.318      apply (erule less_Suc_induct)
   1.319 -    apply (clarsimp simp add: C_def avg_def)
   1.320 -    apply (simp add: add_divide_distrib [symmetric])
   1.321 -    apply (rule AB [THEN less_imp_le])
   1.322 +     apply (clarsimp simp add: C_def avg_def)
   1.323 +     apply (simp add: add_divide_distrib [symmetric])
   1.324 +     apply (rule AB [THEN less_imp_le])
   1.325      apply simp
   1.326      done
   1.327    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.328 @@ -870,7 +894,7 @@
   1.329      apply (erule exE)
   1.330      apply (rule_tac x=n in exI, clarify, rename_tac i j)
   1.331      apply (rule_tac y="B n - A n" in le_less_trans) defer
   1.332 -    apply (simp add: width)
   1.333 +     apply (simp add: width)
   1.334      apply (drule_tac x=n in spec)
   1.335      apply (frule_tac x=i in spec, drule (1) mp)
   1.336      apply (frule_tac x=j in spec, drule (1) mp)
   1.337 @@ -900,11 +924,13 @@
   1.338      apply clarify
   1.339      apply (erule contrapos_pp)
   1.340      apply (simp add: not_le)
   1.341 -    apply (drule less_RealD [OF \<open>cauchy A\<close>], clarify)
   1.342 +    apply (drule less_RealD [OF \<open>cauchy A\<close>])
   1.343 +    apply clarify
   1.344      apply (subgoal_tac "\<not> P (A n)")
   1.345 -    apply (simp add: P_def not_le, clarify)
   1.346 -    apply (erule rev_bexI)
   1.347 -    apply (erule (1) less_trans)
   1.348 +     apply (simp add: P_def not_le)
   1.349 +     apply clarify
   1.350 +     apply (erule rev_bexI)
   1.351 +     apply (erule (1) less_trans)
   1.352      apply (simp add: PA)
   1.353      done
   1.354    have "vanishes (\<lambda>n. (b - a) / 2 ^ n)"
   1.355 @@ -945,13 +971,17 @@
   1.356  
   1.357  instance
   1.358  proof
   1.359 -  show Sup_upper: "x \<le> Sup X" if "x \<in> X" "bdd_above X" for x :: real and X :: "real set"
   1.360 +  show Sup_upper: "x \<le> Sup X"
   1.361 +    if "x \<in> X" "bdd_above X"
   1.362 +    for x :: real and X :: "real set"
   1.363    proof -
   1.364      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.365        using complete_real[of X] unfolding bdd_above_def by blast
   1.366 -    then show ?thesis unfolding Sup_real_def by (rule LeastI2_order) (auto simp: that)
   1.367 +    then show ?thesis
   1.368 +      unfolding Sup_real_def by (rule LeastI2_order) (auto simp: that)
   1.369    qed
   1.370 -  show Sup_least: "Sup X \<le> z" if "X \<noteq> {}" and z: "\<And>x. x \<in> X \<Longrightarrow> x \<le> z"
   1.371 +  show Sup_least: "Sup X \<le> z"
   1.372 +    if "X \<noteq> {}" and z: "\<And>x. x \<in> X \<Longrightarrow> x \<le> z"
   1.373      for z :: real and X :: "real set"
   1.374    proof -
   1.375      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.376 @@ -962,9 +992,11 @@
   1.377        by blast
   1.378      finally show ?thesis .
   1.379    qed
   1.380 -  show "Inf X \<le> x" if "x \<in> X" "bdd_below X" for x :: real and X :: "real set"
   1.381 +  show "Inf X \<le> x" if "x \<in> X" "bdd_below X"
   1.382 +    for x :: real and X :: "real set"
   1.383      using Sup_upper [of "-x" "uminus ` X"] by (auto simp: Inf_real_def that)
   1.384 -  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.385 +  show "z \<le> Inf X" if "X \<noteq> {}" "\<And>x. x \<in> X \<Longrightarrow> z \<le> x"
   1.386 +    for z :: real and X :: "real set"
   1.387      using Sup_least [of "uminus ` X" "- z"] by (force simp: Inf_real_def that)
   1.388    show "\<exists>a b::real. a \<noteq> b"
   1.389      using zero_neq_one by blast
   1.390 @@ -990,13 +1022,16 @@
   1.391  text \<open>BH: These lemmas should not be necessary; they should be
   1.392    covered by existing simp rules and simplification procedures.\<close>
   1.393  
   1.394 -lemma real_mult_less_iff1 [simp]: "0 < z \<Longrightarrow> x * z < y * z \<longleftrightarrow> x < y" for x y z :: real
   1.395 +lemma real_mult_less_iff1 [simp]: "0 < z \<Longrightarrow> x * z < y * z \<longleftrightarrow> x < y"
   1.396 +  for x y z :: real
   1.397    by simp (* solved by linordered_ring_less_cancel_factor simproc *)
   1.398  
   1.399 -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.400 +lemma real_mult_le_cancel_iff1 [simp]: "0 < z \<Longrightarrow> x * z \<le> y * z \<longleftrightarrow> x \<le> y"
   1.401 +  for x y z :: real
   1.402    by simp (* solved by linordered_ring_le_cancel_factor simproc *)
   1.403  
   1.404 -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.405 +lemma real_mult_le_cancel_iff2 [simp]: "0 < z \<Longrightarrow> z * x \<le> z * y \<longleftrightarrow> x \<le> y"
   1.406 +  for x y z :: real
   1.407    by simp (* solved by linordered_ring_le_cancel_factor simproc *)
   1.408  
   1.409  
   1.410 @@ -1072,7 +1107,7 @@
   1.411  
   1.412  lemma real_of_int_div2: "0 \<le> real_of_int n / real_of_int x - real_of_int (n div x)"
   1.413    apply (cases "x = 0")
   1.414 -  apply simp
   1.415 +   apply simp
   1.416    apply (cases "0 < x")
   1.417     apply (metis add.left_neutral floor_correct floor_divide_of_int_eq le_diff_eq)
   1.418    apply (metis add.left_neutral floor_correct floor_divide_of_int_eq le_diff_eq)
   1.419 @@ -1096,7 +1131,8 @@
   1.420  lemma nat_less_real_le: "n < m \<longleftrightarrow> real n + 1 \<le> real m"
   1.421    by (metis discrete of_nat_1 of_nat_add of_nat_le_iff)
   1.422  
   1.423 -lemma nat_le_real_less: "n \<le> m \<longleftrightarrow> real n < real m + 1" for m n :: nat
   1.424 +lemma nat_le_real_less: "n \<le> m \<longleftrightarrow> real n < real m + 1"
   1.425 +  for m n :: nat
   1.426    by (meson nat_less_real_le not_le)
   1.427  
   1.428  lemma real_of_nat_div_aux: "real x / real d = real (x div d) + real (x mod d) / real d"
   1.429 @@ -1122,7 +1158,7 @@
   1.430  
   1.431  lemma real_of_nat_div3: "real n / real x - real (n div x) \<le> 1" for n x :: nat
   1.432    apply (cases "x = 0")
   1.433 -  apply simp
   1.434 +   apply simp
   1.435    apply (simp add: algebra_simps)
   1.436    apply (subst real_of_nat_div_aux)
   1.437    apply simp
   1.438 @@ -1138,10 +1174,8 @@
   1.439    using reals_Archimedean[of e] less_trans[of 0 "1 / real n" e for n::nat]
   1.440    by (auto simp add: field_simps cong: conj_cong simp del: of_nat_Suc)
   1.441  
   1.442 -lemma reals_Archimedean3:
   1.443 -  assumes x_greater_zero: "0 < x"
   1.444 -  shows "\<forall>y. \<exists>n. y < real n * x"
   1.445 -  using \<open>0 < x\<close> by (auto intro: ex_less_of_nat_mult)
   1.446 +lemma reals_Archimedean3: "0 < x \<Longrightarrow> \<forall>y. \<exists>n. y < real n * x"
   1.447 +  by (auto intro: ex_less_of_nat_mult)
   1.448  
   1.449  lemma real_archimedian_rdiv_eq_0:
   1.450    assumes x0: "x \<ge> 0"
   1.451 @@ -1250,7 +1284,7 @@
   1.452  
   1.453  text \<open>
   1.454    This density proof is due to Stefan Richter and was ported by TN.  The
   1.455 -  original source is \emph{Real Analysis} by H.L. Royden.
   1.456 +  original source is \<^emph>\<open>Real Analysis\<close> by H.L. Royden.
   1.457    It employs the Archimedean property of the reals.\<close>
   1.458  
   1.459  lemma Rats_dense_in_real:
   1.460 @@ -1263,15 +1297,15 @@
   1.461      by blast
   1.462    define p where "p = \<lceil>y * real q\<rceil> - 1"
   1.463    define r where "r = of_int p / real q"
   1.464 -  from q have "x < y - inverse (real q)" by simp
   1.465 -  also have "y - inverse (real q) \<le> r"
   1.466 -    unfolding r_def p_def
   1.467 -    by (simp add: le_divide_eq left_diff_distrib le_of_int_ceiling \<open>0 < q\<close>)
   1.468 +  from q have "x < y - inverse (real q)"
   1.469 +    by simp
   1.470 +  also from \<open>0 < q\<close> have "y - inverse (real q) \<le> r"
   1.471 +    by (simp add: r_def p_def le_divide_eq left_diff_distrib)
   1.472    finally have "x < r" .
   1.473 -  moreover have "r < y"
   1.474 -    unfolding r_def p_def
   1.475 -    by (simp add: divide_less_eq diff_less_eq \<open>0 < q\<close> less_ceiling_iff [symmetric])
   1.476 -  moreover from r_def have "r \<in> \<rat>" by simp
   1.477 +  moreover from \<open>0 < q\<close> have "r < y"
   1.478 +    by (simp add: r_def p_def divide_less_eq diff_less_eq less_ceiling_iff [symmetric])
   1.479 +  moreover have "r \<in> \<rat>"
   1.480 +    by (simp add: r_def)
   1.481    ultimately show ?thesis by blast
   1.482  qed
   1.483  
   1.484 @@ -1307,19 +1341,24 @@
   1.485  
   1.486  subsection \<open>Simprules combining \<open>x + y\<close> and \<open>0\<close>\<close> (* FIXME ARE THEY NEEDED? *)
   1.487  
   1.488 -lemma real_add_minus_iff [simp]: "x + - a = 0 \<longleftrightarrow> x = a" for x a :: real
   1.489 +lemma real_add_minus_iff [simp]: "x + - a = 0 \<longleftrightarrow> x = a"
   1.490 +  for x a :: real
   1.491    by arith
   1.492  
   1.493 -lemma real_add_less_0_iff: "x + y < 0 \<longleftrightarrow> y < - x" for x y :: real
   1.494 +lemma real_add_less_0_iff: "x + y < 0 \<longleftrightarrow> y < - x"
   1.495 +  for x y :: real
   1.496    by auto
   1.497  
   1.498 -lemma real_0_less_add_iff: "0 < x + y \<longleftrightarrow> - x < y" for x y :: real
   1.499 +lemma real_0_less_add_iff: "0 < x + y \<longleftrightarrow> - x < y"
   1.500 +  for x y :: real
   1.501    by auto
   1.502  
   1.503 -lemma real_add_le_0_iff: "x + y \<le> 0 \<longleftrightarrow> y \<le> - x" for x y :: real
   1.504 +lemma real_add_le_0_iff: "x + y \<le> 0 \<longleftrightarrow> y \<le> - x"
   1.505 +  for x y :: real
   1.506    by auto
   1.507  
   1.508 -lemma real_0_le_add_iff: "0 \<le> x + y \<longleftrightarrow> - x \<le> y" for x y :: real
   1.509 +lemma real_0_le_add_iff: "0 \<le> x + y \<longleftrightarrow> - x \<le> y"
   1.510 +  for x y :: real
   1.511    by auto
   1.512  
   1.513  
   1.514 @@ -1331,10 +1370,12 @@
   1.515  (* FIXME: declare this [simp] for all types, or not at all *)
   1.516  declare sum_squares_eq_zero_iff [simp] sum_power2_eq_zero_iff [simp]
   1.517  
   1.518 -lemma real_minus_mult_self_le [simp]: "- (u * u) \<le> x * x" for u x :: real
   1.519 +lemma real_minus_mult_self_le [simp]: "- (u * u) \<le> x * x"
   1.520 +  for u x :: real
   1.521    by (rule order_trans [where y = 0]) auto
   1.522  
   1.523 -lemma realpow_square_minus_le [simp]: "- u\<^sup>2 \<le> x\<^sup>2" for u x :: real
   1.524 +lemma realpow_square_minus_le [simp]: "- u\<^sup>2 \<le> x\<^sup>2"
   1.525 +  for u x :: real
   1.526    by (auto simp add: power2_eq_square)
   1.527  
   1.528  lemma numeral_power_eq_real_of_int_cancel_iff [simp]:
   1.529 @@ -1396,17 +1437,21 @@
   1.530  
   1.531  subsection \<open>Density of the Reals\<close>
   1.532  
   1.533 -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.534 +lemma real_lbound_gt_zero: "0 < d1 \<Longrightarrow> 0 < d2 \<Longrightarrow> \<exists>e. 0 < e \<and> e < d1 \<and> e < d2"
   1.535 +  for d1 d2 :: real
   1.536    by (rule exI [where x = "min d1 d2 / 2"]) (simp add: min_def)
   1.537  
   1.538  text \<open>Similar results are proved in @{theory Fields}\<close>
   1.539 -lemma real_less_half_sum: "x < y \<Longrightarrow> x < (x + y) / 2" for x y :: real
   1.540 +lemma real_less_half_sum: "x < y \<Longrightarrow> x < (x + y) / 2"
   1.541 +  for x y :: real
   1.542    by auto
   1.543  
   1.544 -lemma real_gt_half_sum: "x < y \<Longrightarrow> (x + y) / 2 < y" for x y :: real
   1.545 +lemma real_gt_half_sum: "x < y \<Longrightarrow> (x + y) / 2 < y"
   1.546 +  for x y :: real
   1.547    by auto
   1.548  
   1.549 -lemma real_sum_of_halves: "x / 2 + x / 2 = x" for x :: real
   1.550 +lemma real_sum_of_halves: "x / 2 + x / 2 = x"
   1.551 +  for x :: real
   1.552    by simp
   1.553  
   1.554  
   1.555 @@ -1414,13 +1459,16 @@
   1.556  
   1.557  (* FIXME: theorems for negative numerals. Many duplicates, e.g. from Archimedean_Field.thy. *)
   1.558  
   1.559 -lemma real_of_nat_less_numeral_iff [simp]: "real n < numeral w \<longleftrightarrow> n < numeral w" for n :: nat
   1.560 +lemma real_of_nat_less_numeral_iff [simp]: "real n < numeral w \<longleftrightarrow> n < numeral w"
   1.561 +  for n :: nat
   1.562    by (metis of_nat_less_iff of_nat_numeral)
   1.563  
   1.564 -lemma numeral_less_real_of_nat_iff [simp]: "numeral w < real n \<longleftrightarrow> numeral w < n" for n :: nat
   1.565 +lemma numeral_less_real_of_nat_iff [simp]: "numeral w < real n \<longleftrightarrow> numeral w < n"
   1.566 +  for n :: nat
   1.567    by (metis of_nat_less_iff of_nat_numeral)
   1.568  
   1.569 -lemma numeral_le_real_of_nat_iff [simp]: "numeral n \<le> real m \<longleftrightarrow> numeral n \<le> m" for m :: nat
   1.570 +lemma numeral_le_real_of_nat_iff [simp]: "numeral n \<le> real m \<longleftrightarrow> numeral n \<le> m"
   1.571 +  for m :: nat
   1.572    by (metis not_le real_of_nat_less_numeral_iff)
   1.573  
   1.574  declare of_int_floor_le [simp]  (* FIXME duplicate!? *)
   1.575 @@ -1531,7 +1579,8 @@
   1.576    and natceiling.
   1.577  \<close>
   1.578  
   1.579 -lemma nat_floor_neg: "x \<le> 0 \<Longrightarrow> nat \<lfloor>x\<rfloor> = 0" for x :: real
   1.580 +lemma nat_floor_neg: "x \<le> 0 \<Longrightarrow> nat \<lfloor>x\<rfloor> = 0"
   1.581 +  for x :: real
   1.582    by linarith
   1.583  
   1.584  lemma le_nat_floor: "real x \<le> a \<Longrightarrow> x \<le> nat \<lfloor>a\<rfloor>"
   1.585 @@ -1547,7 +1596,8 @@
   1.586  lemma real_nat_ceiling_ge: "x \<le> real (nat \<lceil>x\<rceil>)"
   1.587    by linarith
   1.588  
   1.589 -lemma Rats_no_top_le: "\<exists>q \<in> \<rat>. x \<le> q" for x :: real
   1.590 +lemma Rats_no_top_le: "\<exists>q \<in> \<rat>. x \<le> q"
   1.591 +  for x :: real
   1.592    by (auto intro!: bexI[of _ "of_nat (nat \<lceil>x\<rceil>)"]) linarith
   1.593  
   1.594  lemma Rats_no_bot_less: "\<exists>q \<in> \<rat>. q < x" for x :: real
   1.595 @@ -1616,10 +1666,10 @@
   1.596  text \<open>Operations\<close>
   1.597  
   1.598  lemma zero_real_code [code]: "0 = Ratreal 0"
   1.599 -by simp
   1.600 +  by simp
   1.601  
   1.602  lemma one_real_code [code]: "1 = Ratreal 1"
   1.603 -by simp
   1.604 +  by simp
   1.605  
   1.606  instantiation real :: equal
   1.607  begin
   1.608 @@ -1631,7 +1681,8 @@
   1.609  lemma real_equal_code [code]: "HOL.equal (Ratreal x) (Ratreal y) \<longleftrightarrow> HOL.equal x y"
   1.610    by (simp add: equal_real_def equal)
   1.611  
   1.612 -lemma [code nbe]: "HOL.equal x x \<longleftrightarrow> True" for x :: real
   1.613 +lemma [code nbe]: "HOL.equal x x \<longleftrightarrow> True"
   1.614 +  for x :: real
   1.615    by (rule equal_refl)
   1.616  
   1.617  end