1.1 --- a/src/HOL/Metric_Spaces.thy Tue Mar 26 12:20:56 2013 +0100
1.2 +++ b/src/HOL/Metric_Spaces.thy Tue Mar 26 12:20:56 2013 +0100
1.3 @@ -6,7 +6,7 @@
1.4 header {* Metric Spaces *}
1.5
1.6 theory Metric_Spaces
1.7 -imports RealDef Topological_Spaces
1.8 +imports Real Topological_Spaces
1.9 begin
1.10
1.11
2.1 --- a/src/HOL/Nitpick_Examples/Manual_Nits.thy Tue Mar 26 12:20:56 2013 +0100
2.2 +++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy Tue Mar 26 12:20:56 2013 +0100
2.3 @@ -12,7 +12,7 @@
2.4 suite. *)
2.5
2.6 theory Manual_Nits
2.7 -imports Main "~~/src/HOL/Library/Quotient_Product" RealDef
2.8 +imports Main "~~/src/HOL/Library/Quotient_Product" Real
2.9 begin
2.10
2.11 chapter {* 2. First Steps *}
3.1 --- a/src/HOL/Quickcheck_Benchmark/Find_Unused_Assms_Examples.thy Tue Mar 26 12:20:56 2013 +0100
3.2 +++ b/src/HOL/Quickcheck_Benchmark/Find_Unused_Assms_Examples.thy Tue Mar 26 12:20:56 2013 +0100
3.3 @@ -8,7 +8,7 @@
3.4
3.5 find_unused_assms Divides
3.6 find_unused_assms GCD
3.7 -find_unused_assms RealDef
3.8 +find_unused_assms Real
3.9
3.10 section {* Set Theory *}
3.11
4.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
4.2 +++ b/src/HOL/Real.thy Tue Mar 26 12:20:56 2013 +0100
4.3 @@ -0,0 +1,2229 @@
4.4 +(* Title: HOL/Real.thy
4.5 + Author: Jacques D. Fleuriot, University of Edinburgh, 1998
4.6 + Author: Larry Paulson, University of Cambridge
4.7 + Author: Jeremy Avigad, Carnegie Mellon University
4.8 + Author: Florian Zuleger, Johannes Hoelzl, and Simon Funke, TU Muenchen
4.9 + Conversion to Isar and new proofs by Lawrence C Paulson, 2003/4
4.10 + Construction of Cauchy Reals by Brian Huffman, 2010
4.11 +*)
4.12 +
4.13 +header {* Development of the Reals using Cauchy Sequences *}
4.14 +
4.15 +theory Real
4.16 +imports Rat Conditional_Complete_Lattices
4.17 +begin
4.18 +
4.19 +text {*
4.20 + This theory contains a formalization of the real numbers as
4.21 + equivalence classes of Cauchy sequences of rationals. See
4.22 + @{file "~~/src/HOL/ex/Dedekind_Real.thy"} for an alternative
4.23 + construction using Dedekind cuts.
4.24 +*}
4.25 +
4.26 +subsection {* Preliminary lemmas *}
4.27 +
4.28 +lemma add_diff_add:
4.29 + fixes a b c d :: "'a::ab_group_add"
4.30 + shows "(a + c) - (b + d) = (a - b) + (c - d)"
4.31 + by simp
4.32 +
4.33 +lemma minus_diff_minus:
4.34 + fixes a b :: "'a::ab_group_add"
4.35 + shows "- a - - b = - (a - b)"
4.36 + by simp
4.37 +
4.38 +lemma mult_diff_mult:
4.39 + fixes x y a b :: "'a::ring"
4.40 + shows "(x * y - a * b) = x * (y - b) + (x - a) * b"
4.41 + by (simp add: algebra_simps)
4.42 +
4.43 +lemma inverse_diff_inverse:
4.44 + fixes a b :: "'a::division_ring"
4.45 + assumes "a \<noteq> 0" and "b \<noteq> 0"
4.46 + shows "inverse a - inverse b = - (inverse a * (a - b) * inverse b)"
4.47 + using assms by (simp add: algebra_simps)
4.48 +
4.49 +lemma obtain_pos_sum:
4.50 + fixes r :: rat assumes r: "0 < r"
4.51 + obtains s t where "0 < s" and "0 < t" and "r = s + t"
4.52 +proof
4.53 + from r show "0 < r/2" by simp
4.54 + from r show "0 < r/2" by simp
4.55 + show "r = r/2 + r/2" by simp
4.56 +qed
4.57 +
4.58 +subsection {* Sequences that converge to zero *}
4.59 +
4.60 +definition
4.61 + vanishes :: "(nat \<Rightarrow> rat) \<Rightarrow> bool"
4.62 +where
4.63 + "vanishes X = (\<forall>r>0. \<exists>k. \<forall>n\<ge>k. \<bar>X n\<bar> < r)"
4.64 +
4.65 +lemma vanishesI: "(\<And>r. 0 < r \<Longrightarrow> \<exists>k. \<forall>n\<ge>k. \<bar>X n\<bar> < r) \<Longrightarrow> vanishes X"
4.66 + unfolding vanishes_def by simp
4.67 +
4.68 +lemma vanishesD: "\<lbrakk>vanishes X; 0 < r\<rbrakk> \<Longrightarrow> \<exists>k. \<forall>n\<ge>k. \<bar>X n\<bar> < r"
4.69 + unfolding vanishes_def by simp
4.70 +
4.71 +lemma vanishes_const [simp]: "vanishes (\<lambda>n. c) \<longleftrightarrow> c = 0"
4.72 + unfolding vanishes_def
4.73 + apply (cases "c = 0", auto)
4.74 + apply (rule exI [where x="\<bar>c\<bar>"], auto)
4.75 + done
4.76 +
4.77 +lemma vanishes_minus: "vanishes X \<Longrightarrow> vanishes (\<lambda>n. - X n)"
4.78 + unfolding vanishes_def by simp
4.79 +
4.80 +lemma vanishes_add:
4.81 + assumes X: "vanishes X" and Y: "vanishes Y"
4.82 + shows "vanishes (\<lambda>n. X n + Y n)"
4.83 +proof (rule vanishesI)
4.84 + fix r :: rat assume "0 < r"
4.85 + then obtain s t where s: "0 < s" and t: "0 < t" and r: "r = s + t"
4.86 + by (rule obtain_pos_sum)
4.87 + obtain i where i: "\<forall>n\<ge>i. \<bar>X n\<bar> < s"
4.88 + using vanishesD [OF X s] ..
4.89 + obtain j where j: "\<forall>n\<ge>j. \<bar>Y n\<bar> < t"
4.90 + using vanishesD [OF Y t] ..
4.91 + have "\<forall>n\<ge>max i j. \<bar>X n + Y n\<bar> < r"
4.92 + proof (clarsimp)
4.93 + fix n assume n: "i \<le> n" "j \<le> n"
4.94 + have "\<bar>X n + Y n\<bar> \<le> \<bar>X n\<bar> + \<bar>Y n\<bar>" by (rule abs_triangle_ineq)
4.95 + also have "\<dots> < s + t" by (simp add: add_strict_mono i j n)
4.96 + finally show "\<bar>X n + Y n\<bar> < r" unfolding r .
4.97 + qed
4.98 + thus "\<exists>k. \<forall>n\<ge>k. \<bar>X n + Y n\<bar> < r" ..
4.99 +qed
4.100 +
4.101 +lemma vanishes_diff:
4.102 + assumes X: "vanishes X" and Y: "vanishes Y"
4.103 + shows "vanishes (\<lambda>n. X n - Y n)"
4.104 +unfolding diff_minus by (intro vanishes_add vanishes_minus X Y)
4.105 +
4.106 +lemma vanishes_mult_bounded:
4.107 + assumes X: "\<exists>a>0. \<forall>n. \<bar>X n\<bar> < a"
4.108 + assumes Y: "vanishes (\<lambda>n. Y n)"
4.109 + shows "vanishes (\<lambda>n. X n * Y n)"
4.110 +proof (rule vanishesI)
4.111 + fix r :: rat assume r: "0 < r"
4.112 + obtain a where a: "0 < a" "\<forall>n. \<bar>X n\<bar> < a"
4.113 + using X by fast
4.114 + obtain b where b: "0 < b" "r = a * b"
4.115 + proof
4.116 + show "0 < r / a" using r a by (simp add: divide_pos_pos)
4.117 + show "r = a * (r / a)" using a by simp
4.118 + qed
4.119 + obtain k where k: "\<forall>n\<ge>k. \<bar>Y n\<bar> < b"
4.120 + using vanishesD [OF Y b(1)] ..
4.121 + have "\<forall>n\<ge>k. \<bar>X n * Y n\<bar> < r"
4.122 + by (simp add: b(2) abs_mult mult_strict_mono' a k)
4.123 + thus "\<exists>k. \<forall>n\<ge>k. \<bar>X n * Y n\<bar> < r" ..
4.124 +qed
4.125 +
4.126 +subsection {* Cauchy sequences *}
4.127 +
4.128 +definition
4.129 + cauchy :: "(nat \<Rightarrow> rat) \<Rightarrow> bool"
4.130 +where
4.131 + "cauchy X \<longleftrightarrow> (\<forall>r>0. \<exists>k. \<forall>m\<ge>k. \<forall>n\<ge>k. \<bar>X m - X n\<bar> < r)"
4.132 +
4.133 +lemma cauchyI:
4.134 + "(\<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"
4.135 + unfolding cauchy_def by simp
4.136 +
4.137 +lemma cauchyD:
4.138 + "\<lbrakk>cauchy X; 0 < r\<rbrakk> \<Longrightarrow> \<exists>k. \<forall>m\<ge>k. \<forall>n\<ge>k. \<bar>X m - X n\<bar> < r"
4.139 + unfolding cauchy_def by simp
4.140 +
4.141 +lemma cauchy_const [simp]: "cauchy (\<lambda>n. x)"
4.142 + unfolding cauchy_def by simp
4.143 +
4.144 +lemma cauchy_add [simp]:
4.145 + assumes X: "cauchy X" and Y: "cauchy Y"
4.146 + shows "cauchy (\<lambda>n. X n + Y n)"
4.147 +proof (rule cauchyI)
4.148 + fix r :: rat assume "0 < r"
4.149 + then obtain s t where s: "0 < s" and t: "0 < t" and r: "r = s + t"
4.150 + by (rule obtain_pos_sum)
4.151 + obtain i where i: "\<forall>m\<ge>i. \<forall>n\<ge>i. \<bar>X m - X n\<bar> < s"
4.152 + using cauchyD [OF X s] ..
4.153 + obtain j where j: "\<forall>m\<ge>j. \<forall>n\<ge>j. \<bar>Y m - Y n\<bar> < t"
4.154 + using cauchyD [OF Y t] ..
4.155 + have "\<forall>m\<ge>max i j. \<forall>n\<ge>max i j. \<bar>(X m + Y m) - (X n + Y n)\<bar> < r"
4.156 + proof (clarsimp)
4.157 + fix m n assume *: "i \<le> m" "j \<le> m" "i \<le> n" "j \<le> n"
4.158 + have "\<bar>(X m + Y m) - (X n + Y n)\<bar> \<le> \<bar>X m - X n\<bar> + \<bar>Y m - Y n\<bar>"
4.159 + unfolding add_diff_add by (rule abs_triangle_ineq)
4.160 + also have "\<dots> < s + t"
4.161 + by (rule add_strict_mono, simp_all add: i j *)
4.162 + finally show "\<bar>(X m + Y m) - (X n + Y n)\<bar> < r" unfolding r .
4.163 + qed
4.164 + thus "\<exists>k. \<forall>m\<ge>k. \<forall>n\<ge>k. \<bar>(X m + Y m) - (X n + Y n)\<bar> < r" ..
4.165 +qed
4.166 +
4.167 +lemma cauchy_minus [simp]:
4.168 + assumes X: "cauchy X"
4.169 + shows "cauchy (\<lambda>n. - X n)"
4.170 +using assms unfolding cauchy_def
4.171 +unfolding minus_diff_minus abs_minus_cancel .
4.172 +
4.173 +lemma cauchy_diff [simp]:
4.174 + assumes X: "cauchy X" and Y: "cauchy Y"
4.175 + shows "cauchy (\<lambda>n. X n - Y n)"
4.176 +using assms unfolding diff_minus by simp
4.177 +
4.178 +lemma cauchy_imp_bounded:
4.179 + assumes "cauchy X" shows "\<exists>b>0. \<forall>n. \<bar>X n\<bar> < b"
4.180 +proof -
4.181 + obtain k where k: "\<forall>m\<ge>k. \<forall>n\<ge>k. \<bar>X m - X n\<bar> < 1"
4.182 + using cauchyD [OF assms zero_less_one] ..
4.183 + show "\<exists>b>0. \<forall>n. \<bar>X n\<bar> < b"
4.184 + proof (intro exI conjI allI)
4.185 + have "0 \<le> \<bar>X 0\<bar>" by simp
4.186 + also have "\<bar>X 0\<bar> \<le> Max (abs ` X ` {..k})" by simp
4.187 + finally have "0 \<le> Max (abs ` X ` {..k})" .
4.188 + thus "0 < Max (abs ` X ` {..k}) + 1" by simp
4.189 + next
4.190 + fix n :: nat
4.191 + show "\<bar>X n\<bar> < Max (abs ` X ` {..k}) + 1"
4.192 + proof (rule linorder_le_cases)
4.193 + assume "n \<le> k"
4.194 + hence "\<bar>X n\<bar> \<le> Max (abs ` X ` {..k})" by simp
4.195 + thus "\<bar>X n\<bar> < Max (abs ` X ` {..k}) + 1" by simp
4.196 + next
4.197 + assume "k \<le> n"
4.198 + have "\<bar>X n\<bar> = \<bar>X k + (X n - X k)\<bar>" by simp
4.199 + also have "\<bar>X k + (X n - X k)\<bar> \<le> \<bar>X k\<bar> + \<bar>X n - X k\<bar>"
4.200 + by (rule abs_triangle_ineq)
4.201 + also have "\<dots> < Max (abs ` X ` {..k}) + 1"
4.202 + by (rule add_le_less_mono, simp, simp add: k `k \<le> n`)
4.203 + finally show "\<bar>X n\<bar> < Max (abs ` X ` {..k}) + 1" .
4.204 + qed
4.205 + qed
4.206 +qed
4.207 +
4.208 +lemma cauchy_mult [simp]:
4.209 + assumes X: "cauchy X" and Y: "cauchy Y"
4.210 + shows "cauchy (\<lambda>n. X n * Y n)"
4.211 +proof (rule cauchyI)
4.212 + fix r :: rat assume "0 < r"
4.213 + then obtain u v where u: "0 < u" and v: "0 < v" and "r = u + v"
4.214 + by (rule obtain_pos_sum)
4.215 + obtain a where a: "0 < a" "\<forall>n. \<bar>X n\<bar> < a"
4.216 + using cauchy_imp_bounded [OF X] by fast
4.217 + obtain b where b: "0 < b" "\<forall>n. \<bar>Y n\<bar> < b"
4.218 + using cauchy_imp_bounded [OF Y] by fast
4.219 + obtain s t where s: "0 < s" and t: "0 < t" and r: "r = a * t + s * b"
4.220 + proof
4.221 + show "0 < v/b" using v b(1) by (rule divide_pos_pos)
4.222 + show "0 < u/a" using u a(1) by (rule divide_pos_pos)
4.223 + show "r = a * (u/a) + (v/b) * b"
4.224 + using a(1) b(1) `r = u + v` by simp
4.225 + qed
4.226 + obtain i where i: "\<forall>m\<ge>i. \<forall>n\<ge>i. \<bar>X m - X n\<bar> < s"
4.227 + using cauchyD [OF X s] ..
4.228 + obtain j where j: "\<forall>m\<ge>j. \<forall>n\<ge>j. \<bar>Y m - Y n\<bar> < t"
4.229 + using cauchyD [OF Y t] ..
4.230 + have "\<forall>m\<ge>max i j. \<forall>n\<ge>max i j. \<bar>X m * Y m - X n * Y n\<bar> < r"
4.231 + proof (clarsimp)
4.232 + fix m n assume *: "i \<le> m" "j \<le> m" "i \<le> n" "j \<le> n"
4.233 + 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>"
4.234 + unfolding mult_diff_mult ..
4.235 + also have "\<dots> \<le> \<bar>X m * (Y m - Y n)\<bar> + \<bar>(X m - X n) * Y n\<bar>"
4.236 + by (rule abs_triangle_ineq)
4.237 + also have "\<dots> = \<bar>X m\<bar> * \<bar>Y m - Y n\<bar> + \<bar>X m - X n\<bar> * \<bar>Y n\<bar>"
4.238 + unfolding abs_mult ..
4.239 + also have "\<dots> < a * t + s * b"
4.240 + by (simp_all add: add_strict_mono mult_strict_mono' a b i j *)
4.241 + finally show "\<bar>X m * Y m - X n * Y n\<bar> < r" unfolding r .
4.242 + qed
4.243 + thus "\<exists>k. \<forall>m\<ge>k. \<forall>n\<ge>k. \<bar>X m * Y m - X n * Y n\<bar> < r" ..
4.244 +qed
4.245 +
4.246 +lemma cauchy_not_vanishes_cases:
4.247 + assumes X: "cauchy X"
4.248 + assumes nz: "\<not> vanishes X"
4.249 + shows "\<exists>b>0. \<exists>k. (\<forall>n\<ge>k. b < - X n) \<or> (\<forall>n\<ge>k. b < X n)"
4.250 +proof -
4.251 + obtain r where "0 < r" and r: "\<forall>k. \<exists>n\<ge>k. r \<le> \<bar>X n\<bar>"
4.252 + using nz unfolding vanishes_def by (auto simp add: not_less)
4.253 + obtain s t where s: "0 < s" and t: "0 < t" and "r = s + t"
4.254 + using `0 < r` by (rule obtain_pos_sum)
4.255 + obtain i where i: "\<forall>m\<ge>i. \<forall>n\<ge>i. \<bar>X m - X n\<bar> < s"
4.256 + using cauchyD [OF X s] ..
4.257 + obtain k where "i \<le> k" and "r \<le> \<bar>X k\<bar>"
4.258 + using r by fast
4.259 + have k: "\<forall>n\<ge>k. \<bar>X n - X k\<bar> < s"
4.260 + using i `i \<le> k` by auto
4.261 + have "X k \<le> - r \<or> r \<le> X k"
4.262 + using `r \<le> \<bar>X k\<bar>` by auto
4.263 + hence "(\<forall>n\<ge>k. t < - X n) \<or> (\<forall>n\<ge>k. t < X n)"
4.264 + unfolding `r = s + t` using k by auto
4.265 + hence "\<exists>k. (\<forall>n\<ge>k. t < - X n) \<or> (\<forall>n\<ge>k. t < X n)" ..
4.266 + thus "\<exists>t>0. \<exists>k. (\<forall>n\<ge>k. t < - X n) \<or> (\<forall>n\<ge>k. t < X n)"
4.267 + using t by auto
4.268 +qed
4.269 +
4.270 +lemma cauchy_not_vanishes:
4.271 + assumes X: "cauchy X"
4.272 + assumes nz: "\<not> vanishes X"
4.273 + shows "\<exists>b>0. \<exists>k. \<forall>n\<ge>k. b < \<bar>X n\<bar>"
4.274 +using cauchy_not_vanishes_cases [OF assms]
4.275 +by clarify (rule exI, erule conjI, rule_tac x=k in exI, auto)
4.276 +
4.277 +lemma cauchy_inverse [simp]:
4.278 + assumes X: "cauchy X"
4.279 + assumes nz: "\<not> vanishes X"
4.280 + shows "cauchy (\<lambda>n. inverse (X n))"
4.281 +proof (rule cauchyI)
4.282 + fix r :: rat assume "0 < r"
4.283 + obtain b i where b: "0 < b" and i: "\<forall>n\<ge>i. b < \<bar>X n\<bar>"
4.284 + using cauchy_not_vanishes [OF X nz] by fast
4.285 + from b i have nz: "\<forall>n\<ge>i. X n \<noteq> 0" by auto
4.286 + obtain s where s: "0 < s" and r: "r = inverse b * s * inverse b"
4.287 + proof
4.288 + show "0 < b * r * b"
4.289 + by (simp add: `0 < r` b mult_pos_pos)
4.290 + show "r = inverse b * (b * r * b) * inverse b"
4.291 + using b by simp
4.292 + qed
4.293 + obtain j where j: "\<forall>m\<ge>j. \<forall>n\<ge>j. \<bar>X m - X n\<bar> < s"
4.294 + using cauchyD [OF X s] ..
4.295 + have "\<forall>m\<ge>max i j. \<forall>n\<ge>max i j. \<bar>inverse (X m) - inverse (X n)\<bar> < r"
4.296 + proof (clarsimp)
4.297 + fix m n assume *: "i \<le> m" "j \<le> m" "i \<le> n" "j \<le> n"
4.298 + have "\<bar>inverse (X m) - inverse (X n)\<bar> =
4.299 + inverse \<bar>X m\<bar> * \<bar>X m - X n\<bar> * inverse \<bar>X n\<bar>"
4.300 + by (simp add: inverse_diff_inverse nz * abs_mult)
4.301 + also have "\<dots> < inverse b * s * inverse b"
4.302 + by (simp add: mult_strict_mono less_imp_inverse_less
4.303 + mult_pos_pos i j b * s)
4.304 + finally show "\<bar>inverse (X m) - inverse (X n)\<bar> < r" unfolding r .
4.305 + qed
4.306 + thus "\<exists>k. \<forall>m\<ge>k. \<forall>n\<ge>k. \<bar>inverse (X m) - inverse (X n)\<bar> < r" ..
4.307 +qed
4.308 +
4.309 +lemma vanishes_diff_inverse:
4.310 + assumes X: "cauchy X" "\<not> vanishes X"
4.311 + assumes Y: "cauchy Y" "\<not> vanishes Y"
4.312 + assumes XY: "vanishes (\<lambda>n. X n - Y n)"
4.313 + shows "vanishes (\<lambda>n. inverse (X n) - inverse (Y n))"
4.314 +proof (rule vanishesI)
4.315 + fix r :: rat assume r: "0 < r"
4.316 + obtain a i where a: "0 < a" and i: "\<forall>n\<ge>i. a < \<bar>X n\<bar>"
4.317 + using cauchy_not_vanishes [OF X] by fast
4.318 + obtain b j where b: "0 < b" and j: "\<forall>n\<ge>j. b < \<bar>Y n\<bar>"
4.319 + using cauchy_not_vanishes [OF Y] by fast
4.320 + obtain s where s: "0 < s" and "inverse a * s * inverse b = r"
4.321 + proof
4.322 + show "0 < a * r * b"
4.323 + using a r b by (simp add: mult_pos_pos)
4.324 + show "inverse a * (a * r * b) * inverse b = r"
4.325 + using a r b by simp
4.326 + qed
4.327 + obtain k where k: "\<forall>n\<ge>k. \<bar>X n - Y n\<bar> < s"
4.328 + using vanishesD [OF XY s] ..
4.329 + have "\<forall>n\<ge>max (max i j) k. \<bar>inverse (X n) - inverse (Y n)\<bar> < r"
4.330 + proof (clarsimp)
4.331 + fix n assume n: "i \<le> n" "j \<le> n" "k \<le> n"
4.332 + have "X n \<noteq> 0" and "Y n \<noteq> 0"
4.333 + using i j a b n by auto
4.334 + hence "\<bar>inverse (X n) - inverse (Y n)\<bar> =
4.335 + inverse \<bar>X n\<bar> * \<bar>X n - Y n\<bar> * inverse \<bar>Y n\<bar>"
4.336 + by (simp add: inverse_diff_inverse abs_mult)
4.337 + also have "\<dots> < inverse a * s * inverse b"
4.338 + apply (intro mult_strict_mono' less_imp_inverse_less)
4.339 + apply (simp_all add: a b i j k n mult_nonneg_nonneg)
4.340 + done
4.341 + also note `inverse a * s * inverse b = r`
4.342 + finally show "\<bar>inverse (X n) - inverse (Y n)\<bar> < r" .
4.343 + qed
4.344 + thus "\<exists>k. \<forall>n\<ge>k. \<bar>inverse (X n) - inverse (Y n)\<bar> < r" ..
4.345 +qed
4.346 +
4.347 +subsection {* Equivalence relation on Cauchy sequences *}
4.348 +
4.349 +definition realrel :: "(nat \<Rightarrow> rat) \<Rightarrow> (nat \<Rightarrow> rat) \<Rightarrow> bool"
4.350 + where "realrel = (\<lambda>X Y. cauchy X \<and> cauchy Y \<and> vanishes (\<lambda>n. X n - Y n))"
4.351 +
4.352 +lemma realrelI [intro?]:
4.353 + assumes "cauchy X" and "cauchy Y" and "vanishes (\<lambda>n. X n - Y n)"
4.354 + shows "realrel X Y"
4.355 + using assms unfolding realrel_def by simp
4.356 +
4.357 +lemma realrel_refl: "cauchy X \<Longrightarrow> realrel X X"
4.358 + unfolding realrel_def by simp
4.359 +
4.360 +lemma symp_realrel: "symp realrel"
4.361 + unfolding realrel_def
4.362 + by (rule sympI, clarify, drule vanishes_minus, simp)
4.363 +
4.364 +lemma transp_realrel: "transp realrel"
4.365 + unfolding realrel_def
4.366 + apply (rule transpI, clarify)
4.367 + apply (drule (1) vanishes_add)
4.368 + apply (simp add: algebra_simps)
4.369 + done
4.370 +
4.371 +lemma part_equivp_realrel: "part_equivp realrel"
4.372 + by (fast intro: part_equivpI symp_realrel transp_realrel
4.373 + realrel_refl cauchy_const)
4.374 +
4.375 +subsection {* The field of real numbers *}
4.376 +
4.377 +quotient_type real = "nat \<Rightarrow> rat" / partial: realrel
4.378 + morphisms rep_real Real
4.379 + by (rule part_equivp_realrel)
4.380 +
4.381 +lemma cr_real_eq: "pcr_real = (\<lambda>x y. cauchy x \<and> Real x = y)"
4.382 + unfolding real.pcr_cr_eq cr_real_def realrel_def by auto
4.383 +
4.384 +lemma Real_induct [induct type: real]: (* TODO: generate automatically *)
4.385 + assumes "\<And>X. cauchy X \<Longrightarrow> P (Real X)" shows "P x"
4.386 +proof (induct x)
4.387 + case (1 X)
4.388 + hence "cauchy X" by (simp add: realrel_def)
4.389 + thus "P (Real X)" by (rule assms)
4.390 +qed
4.391 +
4.392 +lemma eq_Real:
4.393 + "cauchy X \<Longrightarrow> cauchy Y \<Longrightarrow> Real X = Real Y \<longleftrightarrow> vanishes (\<lambda>n. X n - Y n)"
4.394 + using real.rel_eq_transfer
4.395 + unfolding real.pcr_cr_eq cr_real_def fun_rel_def realrel_def by simp
4.396 +
4.397 +declare real.forall_transfer [transfer_rule del]
4.398 +
4.399 +lemma forall_real_transfer [transfer_rule]: (* TODO: generate automatically *)
4.400 + "(fun_rel (fun_rel pcr_real op =) op =)
4.401 + (transfer_bforall cauchy) transfer_forall"
4.402 + using real.forall_transfer
4.403 + by (simp add: realrel_def)
4.404 +
4.405 +instantiation real :: field_inverse_zero
4.406 +begin
4.407 +
4.408 +lift_definition zero_real :: "real" is "\<lambda>n. 0"
4.409 + by (simp add: realrel_refl)
4.410 +
4.411 +lift_definition one_real :: "real" is "\<lambda>n. 1"
4.412 + by (simp add: realrel_refl)
4.413 +
4.414 +lift_definition plus_real :: "real \<Rightarrow> real \<Rightarrow> real" is "\<lambda>X Y n. X n + Y n"
4.415 + unfolding realrel_def add_diff_add
4.416 + by (simp only: cauchy_add vanishes_add simp_thms)
4.417 +
4.418 +lift_definition uminus_real :: "real \<Rightarrow> real" is "\<lambda>X n. - X n"
4.419 + unfolding realrel_def minus_diff_minus
4.420 + by (simp only: cauchy_minus vanishes_minus simp_thms)
4.421 +
4.422 +lift_definition times_real :: "real \<Rightarrow> real \<Rightarrow> real" is "\<lambda>X Y n. X n * Y n"
4.423 + unfolding realrel_def mult_diff_mult
4.424 + by (subst (4) mult_commute, simp only: cauchy_mult vanishes_add
4.425 + vanishes_mult_bounded cauchy_imp_bounded simp_thms)
4.426 +
4.427 +lift_definition inverse_real :: "real \<Rightarrow> real"
4.428 + is "\<lambda>X. if vanishes X then (\<lambda>n. 0) else (\<lambda>n. inverse (X n))"
4.429 +proof -
4.430 + fix X Y assume "realrel X Y"
4.431 + hence X: "cauchy X" and Y: "cauchy Y" and XY: "vanishes (\<lambda>n. X n - Y n)"
4.432 + unfolding realrel_def by simp_all
4.433 + have "vanishes X \<longleftrightarrow> vanishes Y"
4.434 + proof
4.435 + assume "vanishes X"
4.436 + from vanishes_diff [OF this XY] show "vanishes Y" by simp
4.437 + next
4.438 + assume "vanishes Y"
4.439 + from vanishes_add [OF this XY] show "vanishes X" by simp
4.440 + qed
4.441 + thus "?thesis X Y"
4.442 + unfolding realrel_def
4.443 + by (simp add: vanishes_diff_inverse X Y XY)
4.444 +qed
4.445 +
4.446 +definition
4.447 + "x - y = (x::real) + - y"
4.448 +
4.449 +definition
4.450 + "x / y = (x::real) * inverse y"
4.451 +
4.452 +lemma add_Real:
4.453 + assumes X: "cauchy X" and Y: "cauchy Y"
4.454 + shows "Real X + Real Y = Real (\<lambda>n. X n + Y n)"
4.455 + using assms plus_real.transfer
4.456 + unfolding cr_real_eq fun_rel_def by simp
4.457 +
4.458 +lemma minus_Real:
4.459 + assumes X: "cauchy X"
4.460 + shows "- Real X = Real (\<lambda>n. - X n)"
4.461 + using assms uminus_real.transfer
4.462 + unfolding cr_real_eq fun_rel_def by simp
4.463 +
4.464 +lemma diff_Real:
4.465 + assumes X: "cauchy X" and Y: "cauchy Y"
4.466 + shows "Real X - Real Y = Real (\<lambda>n. X n - Y n)"
4.467 + unfolding minus_real_def diff_minus
4.468 + by (simp add: minus_Real add_Real X Y)
4.469 +
4.470 +lemma mult_Real:
4.471 + assumes X: "cauchy X" and Y: "cauchy Y"
4.472 + shows "Real X * Real Y = Real (\<lambda>n. X n * Y n)"
4.473 + using assms times_real.transfer
4.474 + unfolding cr_real_eq fun_rel_def by simp
4.475 +
4.476 +lemma inverse_Real:
4.477 + assumes X: "cauchy X"
4.478 + shows "inverse (Real X) =
4.479 + (if vanishes X then 0 else Real (\<lambda>n. inverse (X n)))"
4.480 + using assms inverse_real.transfer zero_real.transfer
4.481 + unfolding cr_real_eq fun_rel_def by (simp split: split_if_asm, metis)
4.482 +
4.483 +instance proof
4.484 + fix a b c :: real
4.485 + show "a + b = b + a"
4.486 + by transfer (simp add: add_ac realrel_def)
4.487 + show "(a + b) + c = a + (b + c)"
4.488 + by transfer (simp add: add_ac realrel_def)
4.489 + show "0 + a = a"
4.490 + by transfer (simp add: realrel_def)
4.491 + show "- a + a = 0"
4.492 + by transfer (simp add: realrel_def)
4.493 + show "a - b = a + - b"
4.494 + by (rule minus_real_def)
4.495 + show "(a * b) * c = a * (b * c)"
4.496 + by transfer (simp add: mult_ac realrel_def)
4.497 + show "a * b = b * a"
4.498 + by transfer (simp add: mult_ac realrel_def)
4.499 + show "1 * a = a"
4.500 + by transfer (simp add: mult_ac realrel_def)
4.501 + show "(a + b) * c = a * c + b * c"
4.502 + by transfer (simp add: distrib_right realrel_def)
4.503 + show "(0\<Colon>real) \<noteq> (1\<Colon>real)"
4.504 + by transfer (simp add: realrel_def)
4.505 + show "a \<noteq> 0 \<Longrightarrow> inverse a * a = 1"
4.506 + apply transfer
4.507 + apply (simp add: realrel_def)
4.508 + apply (rule vanishesI)
4.509 + apply (frule (1) cauchy_not_vanishes, clarify)
4.510 + apply (rule_tac x=k in exI, clarify)
4.511 + apply (drule_tac x=n in spec, simp)
4.512 + done
4.513 + show "a / b = a * inverse b"
4.514 + by (rule divide_real_def)
4.515 + show "inverse (0::real) = 0"
4.516 + by transfer (simp add: realrel_def)
4.517 +qed
4.518 +
4.519 +end
4.520 +
4.521 +subsection {* Positive reals *}
4.522 +
4.523 +lift_definition positive :: "real \<Rightarrow> bool"
4.524 + is "\<lambda>X. \<exists>r>0. \<exists>k. \<forall>n\<ge>k. r < X n"
4.525 +proof -
4.526 + { fix X Y
4.527 + assume "realrel X Y"
4.528 + hence XY: "vanishes (\<lambda>n. X n - Y n)"
4.529 + unfolding realrel_def by simp_all
4.530 + assume "\<exists>r>0. \<exists>k. \<forall>n\<ge>k. r < X n"
4.531 + then obtain r i where "0 < r" and i: "\<forall>n\<ge>i. r < X n"
4.532 + by fast
4.533 + obtain s t where s: "0 < s" and t: "0 < t" and r: "r = s + t"
4.534 + using `0 < r` by (rule obtain_pos_sum)
4.535 + obtain j where j: "\<forall>n\<ge>j. \<bar>X n - Y n\<bar> < s"
4.536 + using vanishesD [OF XY s] ..
4.537 + have "\<forall>n\<ge>max i j. t < Y n"
4.538 + proof (clarsimp)
4.539 + fix n assume n: "i \<le> n" "j \<le> n"
4.540 + have "\<bar>X n - Y n\<bar> < s" and "r < X n"
4.541 + using i j n by simp_all
4.542 + thus "t < Y n" unfolding r by simp
4.543 + qed
4.544 + hence "\<exists>r>0. \<exists>k. \<forall>n\<ge>k. r < Y n" using t by fast
4.545 + } note 1 = this
4.546 + fix X Y assume "realrel X Y"
4.547 + hence "realrel X Y" and "realrel Y X"
4.548 + using symp_realrel unfolding symp_def by auto
4.549 + thus "?thesis X Y"
4.550 + by (safe elim!: 1)
4.551 +qed
4.552 +
4.553 +lemma positive_Real:
4.554 + assumes X: "cauchy X"
4.555 + shows "positive (Real X) \<longleftrightarrow> (\<exists>r>0. \<exists>k. \<forall>n\<ge>k. r < X n)"
4.556 + using assms positive.transfer
4.557 + unfolding cr_real_eq fun_rel_def by simp
4.558 +
4.559 +lemma positive_zero: "\<not> positive 0"
4.560 + by transfer auto
4.561 +
4.562 +lemma positive_add:
4.563 + "positive x \<Longrightarrow> positive y \<Longrightarrow> positive (x + y)"
4.564 +apply transfer
4.565 +apply (clarify, rename_tac a b i j)
4.566 +apply (rule_tac x="a + b" in exI, simp)
4.567 +apply (rule_tac x="max i j" in exI, clarsimp)
4.568 +apply (simp add: add_strict_mono)
4.569 +done
4.570 +
4.571 +lemma positive_mult:
4.572 + "positive x \<Longrightarrow> positive y \<Longrightarrow> positive (x * y)"
4.573 +apply transfer
4.574 +apply (clarify, rename_tac a b i j)
4.575 +apply (rule_tac x="a * b" in exI, simp add: mult_pos_pos)
4.576 +apply (rule_tac x="max i j" in exI, clarsimp)
4.577 +apply (rule mult_strict_mono, auto)
4.578 +done
4.579 +
4.580 +lemma positive_minus:
4.581 + "\<not> positive x \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> positive (- x)"
4.582 +apply transfer
4.583 +apply (simp add: realrel_def)
4.584 +apply (drule (1) cauchy_not_vanishes_cases, safe, fast, fast)
4.585 +done
4.586 +
4.587 +instantiation real :: linordered_field_inverse_zero
4.588 +begin
4.589 +
4.590 +definition
4.591 + "x < y \<longleftrightarrow> positive (y - x)"
4.592 +
4.593 +definition
4.594 + "x \<le> (y::real) \<longleftrightarrow> x < y \<or> x = y"
4.595 +
4.596 +definition
4.597 + "abs (a::real) = (if a < 0 then - a else a)"
4.598 +
4.599 +definition
4.600 + "sgn (a::real) = (if a = 0 then 0 else if 0 < a then 1 else - 1)"
4.601 +
4.602 +instance proof
4.603 + fix a b c :: real
4.604 + show "\<bar>a\<bar> = (if a < 0 then - a else a)"
4.605 + by (rule abs_real_def)
4.606 + show "a < b \<longleftrightarrow> a \<le> b \<and> \<not> b \<le> a"
4.607 + unfolding less_eq_real_def less_real_def
4.608 + by (auto, drule (1) positive_add, simp_all add: positive_zero)
4.609 + show "a \<le> a"
4.610 + unfolding less_eq_real_def by simp
4.611 + show "a \<le> b \<Longrightarrow> b \<le> c \<Longrightarrow> a \<le> c"
4.612 + unfolding less_eq_real_def less_real_def
4.613 + by (auto, drule (1) positive_add, simp add: algebra_simps)
4.614 + show "a \<le> b \<Longrightarrow> b \<le> a \<Longrightarrow> a = b"
4.615 + unfolding less_eq_real_def less_real_def
4.616 + by (auto, drule (1) positive_add, simp add: positive_zero)
4.617 + show "a \<le> b \<Longrightarrow> c + a \<le> c + b"
4.618 + unfolding less_eq_real_def less_real_def by (auto simp: diff_minus) (* by auto *)
4.619 + (* FIXME: Procedure int_combine_numerals: c + b - (c + a) \<equiv> b + - a *)
4.620 + (* Should produce c + b - (c + a) \<equiv> b - a *)
4.621 + show "sgn a = (if a = 0 then 0 else if 0 < a then 1 else - 1)"
4.622 + by (rule sgn_real_def)
4.623 + show "a \<le> b \<or> b \<le> a"
4.624 + unfolding less_eq_real_def less_real_def
4.625 + by (auto dest!: positive_minus)
4.626 + show "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b"
4.627 + unfolding less_real_def
4.628 + by (drule (1) positive_mult, simp add: algebra_simps)
4.629 +qed
4.630 +
4.631 +end
4.632 +
4.633 +instantiation real :: distrib_lattice
4.634 +begin
4.635 +
4.636 +definition
4.637 + "(inf :: real \<Rightarrow> real \<Rightarrow> real) = min"
4.638 +
4.639 +definition
4.640 + "(sup :: real \<Rightarrow> real \<Rightarrow> real) = max"
4.641 +
4.642 +instance proof
4.643 +qed (auto simp add: inf_real_def sup_real_def min_max.sup_inf_distrib1)
4.644 +
4.645 +end
4.646 +
4.647 +lemma of_nat_Real: "of_nat x = Real (\<lambda>n. of_nat x)"
4.648 +apply (induct x)
4.649 +apply (simp add: zero_real_def)
4.650 +apply (simp add: one_real_def add_Real)
4.651 +done
4.652 +
4.653 +lemma of_int_Real: "of_int x = Real (\<lambda>n. of_int x)"
4.654 +apply (cases x rule: int_diff_cases)
4.655 +apply (simp add: of_nat_Real diff_Real)
4.656 +done
4.657 +
4.658 +lemma of_rat_Real: "of_rat x = Real (\<lambda>n. x)"
4.659 +apply (induct x)
4.660 +apply (simp add: Fract_of_int_quotient of_rat_divide)
4.661 +apply (simp add: of_int_Real divide_inverse)
4.662 +apply (simp add: inverse_Real mult_Real)
4.663 +done
4.664 +
4.665 +instance real :: archimedean_field
4.666 +proof
4.667 + fix x :: real
4.668 + show "\<exists>z. x \<le> of_int z"
4.669 + apply (induct x)
4.670 + apply (frule cauchy_imp_bounded, clarify)
4.671 + apply (rule_tac x="ceiling b + 1" in exI)
4.672 + apply (rule less_imp_le)
4.673 + apply (simp add: of_int_Real less_real_def diff_Real positive_Real)
4.674 + apply (rule_tac x=1 in exI, simp add: algebra_simps)
4.675 + apply (rule_tac x=0 in exI, clarsimp)
4.676 + apply (rule le_less_trans [OF abs_ge_self])
4.677 + apply (rule less_le_trans [OF _ le_of_int_ceiling])
4.678 + apply simp
4.679 + done
4.680 +qed
4.681 +
4.682 +instantiation real :: floor_ceiling
4.683 +begin
4.684 +
4.685 +definition [code del]:
4.686 + "floor (x::real) = (THE z. of_int z \<le> x \<and> x < of_int (z + 1))"
4.687 +
4.688 +instance proof
4.689 + fix x :: real
4.690 + show "of_int (floor x) \<le> x \<and> x < of_int (floor x + 1)"
4.691 + unfolding floor_real_def using floor_exists1 by (rule theI')
4.692 +qed
4.693 +
4.694 +end
4.695 +
4.696 +subsection {* Completeness *}
4.697 +
4.698 +lemma not_positive_Real:
4.699 + assumes X: "cauchy X"
4.700 + shows "\<not> positive (Real X) \<longleftrightarrow> (\<forall>r>0. \<exists>k. \<forall>n\<ge>k. X n \<le> r)"
4.701 +unfolding positive_Real [OF X]
4.702 +apply (auto, unfold not_less)
4.703 +apply (erule obtain_pos_sum)
4.704 +apply (drule_tac x=s in spec, simp)
4.705 +apply (drule_tac r=t in cauchyD [OF X], clarify)
4.706 +apply (drule_tac x=k in spec, clarsimp)
4.707 +apply (rule_tac x=n in exI, clarify, rename_tac m)
4.708 +apply (drule_tac x=m in spec, simp)
4.709 +apply (drule_tac x=n in spec, simp)
4.710 +apply (drule spec, drule (1) mp, clarify, rename_tac i)
4.711 +apply (rule_tac x="max i k" in exI, simp)
4.712 +done
4.713 +
4.714 +lemma le_Real:
4.715 + assumes X: "cauchy X" and Y: "cauchy Y"
4.716 + shows "Real X \<le> Real Y = (\<forall>r>0. \<exists>k. \<forall>n\<ge>k. X n \<le> Y n + r)"
4.717 +unfolding not_less [symmetric, where 'a=real] less_real_def
4.718 +apply (simp add: diff_Real not_positive_Real X Y)
4.719 +apply (simp add: diff_le_eq add_ac)
4.720 +done
4.721 +
4.722 +lemma le_RealI:
4.723 + assumes Y: "cauchy Y"
4.724 + shows "\<forall>n. x \<le> of_rat (Y n) \<Longrightarrow> x \<le> Real Y"
4.725 +proof (induct x)
4.726 + fix X assume X: "cauchy X" and "\<forall>n. Real X \<le> of_rat (Y n)"
4.727 + hence le: "\<And>m r. 0 < r \<Longrightarrow> \<exists>k. \<forall>n\<ge>k. X n \<le> Y m + r"
4.728 + by (simp add: of_rat_Real le_Real)
4.729 + {
4.730 + fix r :: rat assume "0 < r"
4.731 + then obtain s t where s: "0 < s" and t: "0 < t" and r: "r = s + t"
4.732 + by (rule obtain_pos_sum)
4.733 + obtain i where i: "\<forall>m\<ge>i. \<forall>n\<ge>i. \<bar>Y m - Y n\<bar> < s"
4.734 + using cauchyD [OF Y s] ..
4.735 + obtain j where j: "\<forall>n\<ge>j. X n \<le> Y i + t"
4.736 + using le [OF t] ..
4.737 + have "\<forall>n\<ge>max i j. X n \<le> Y n + r"
4.738 + proof (clarsimp)
4.739 + fix n assume n: "i \<le> n" "j \<le> n"
4.740 + have "X n \<le> Y i + t" using n j by simp
4.741 + moreover have "\<bar>Y i - Y n\<bar> < s" using n i by simp
4.742 + ultimately show "X n \<le> Y n + r" unfolding r by simp
4.743 + qed
4.744 + hence "\<exists>k. \<forall>n\<ge>k. X n \<le> Y n + r" ..
4.745 + }
4.746 + thus "Real X \<le> Real Y"
4.747 + by (simp add: of_rat_Real le_Real X Y)
4.748 +qed
4.749 +
4.750 +lemma Real_leI:
4.751 + assumes X: "cauchy X"
4.752 + assumes le: "\<forall>n. of_rat (X n) \<le> y"
4.753 + shows "Real X \<le> y"
4.754 +proof -
4.755 + have "- y \<le> - Real X"
4.756 + by (simp add: minus_Real X le_RealI of_rat_minus le)
4.757 + thus ?thesis by simp
4.758 +qed
4.759 +
4.760 +lemma less_RealD:
4.761 + assumes Y: "cauchy Y"
4.762 + shows "x < Real Y \<Longrightarrow> \<exists>n. x < of_rat (Y n)"
4.763 +by (erule contrapos_pp, simp add: not_less, erule Real_leI [OF Y])
4.764 +
4.765 +lemma of_nat_less_two_power:
4.766 + "of_nat n < (2::'a::linordered_idom) ^ n"
4.767 +apply (induct n)
4.768 +apply simp
4.769 +apply (subgoal_tac "(1::'a) \<le> 2 ^ n")
4.770 +apply (drule (1) add_le_less_mono, simp)
4.771 +apply simp
4.772 +done
4.773 +
4.774 +lemma complete_real:
4.775 + fixes S :: "real set"
4.776 + assumes "\<exists>x. x \<in> S" and "\<exists>z. \<forall>x\<in>S. x \<le> z"
4.777 + shows "\<exists>y. (\<forall>x\<in>S. x \<le> y) \<and> (\<forall>z. (\<forall>x\<in>S. x \<le> z) \<longrightarrow> y \<le> z)"
4.778 +proof -
4.779 + obtain x where x: "x \<in> S" using assms(1) ..
4.780 + obtain z where z: "\<forall>x\<in>S. x \<le> z" using assms(2) ..
4.781 +
4.782 + def P \<equiv> "\<lambda>x. \<forall>y\<in>S. y \<le> of_rat x"
4.783 + obtain a where a: "\<not> P a"
4.784 + proof
4.785 + have "of_int (floor (x - 1)) \<le> x - 1" by (rule of_int_floor_le)
4.786 + also have "x - 1 < x" by simp
4.787 + finally have "of_int (floor (x - 1)) < x" .
4.788 + hence "\<not> x \<le> of_int (floor (x - 1))" by (simp only: not_le)
4.789 + then show "\<not> P (of_int (floor (x - 1)))"
4.790 + unfolding P_def of_rat_of_int_eq using x by fast
4.791 + qed
4.792 + obtain b where b: "P b"
4.793 + proof
4.794 + show "P (of_int (ceiling z))"
4.795 + unfolding P_def of_rat_of_int_eq
4.796 + proof
4.797 + fix y assume "y \<in> S"
4.798 + hence "y \<le> z" using z by simp
4.799 + also have "z \<le> of_int (ceiling z)" by (rule le_of_int_ceiling)
4.800 + finally show "y \<le> of_int (ceiling z)" .
4.801 + qed
4.802 + qed
4.803 +
4.804 + def avg \<equiv> "\<lambda>x y :: rat. x/2 + y/2"
4.805 + def bisect \<equiv> "\<lambda>(x, y). if P (avg x y) then (x, avg x y) else (avg x y, y)"
4.806 + def A \<equiv> "\<lambda>n. fst ((bisect ^^ n) (a, b))"
4.807 + def B \<equiv> "\<lambda>n. snd ((bisect ^^ n) (a, b))"
4.808 + def C \<equiv> "\<lambda>n. avg (A n) (B n)"
4.809 + have A_0 [simp]: "A 0 = a" unfolding A_def by simp
4.810 + have B_0 [simp]: "B 0 = b" unfolding B_def by simp
4.811 + have A_Suc [simp]: "\<And>n. A (Suc n) = (if P (C n) then A n else C n)"
4.812 + unfolding A_def B_def C_def bisect_def split_def by simp
4.813 + have B_Suc [simp]: "\<And>n. B (Suc n) = (if P (C n) then C n else B n)"
4.814 + unfolding A_def B_def C_def bisect_def split_def by simp
4.815 +
4.816 + have width: "\<And>n. B n - A n = (b - a) / 2^n"
4.817 + apply (simp add: eq_divide_eq)
4.818 + apply (induct_tac n, simp)
4.819 + apply (simp add: C_def avg_def algebra_simps)
4.820 + done
4.821 +
4.822 + have twos: "\<And>y r :: rat. 0 < r \<Longrightarrow> \<exists>n. y / 2 ^ n < r"
4.823 + apply (simp add: divide_less_eq)
4.824 + apply (subst mult_commute)
4.825 + apply (frule_tac y=y in ex_less_of_nat_mult)
4.826 + apply clarify
4.827 + apply (rule_tac x=n in exI)
4.828 + apply (erule less_trans)
4.829 + apply (rule mult_strict_right_mono)
4.830 + apply (rule le_less_trans [OF _ of_nat_less_two_power])
4.831 + apply simp
4.832 + apply assumption
4.833 + done
4.834 +
4.835 + have PA: "\<And>n. \<not> P (A n)"
4.836 + by (induct_tac n, simp_all add: a)
4.837 + have PB: "\<And>n. P (B n)"
4.838 + by (induct_tac n, simp_all add: b)
4.839 + have ab: "a < b"
4.840 + using a b unfolding P_def
4.841 + apply (clarsimp simp add: not_le)
4.842 + apply (drule (1) bspec)
4.843 + apply (drule (1) less_le_trans)
4.844 + apply (simp add: of_rat_less)
4.845 + done
4.846 + have AB: "\<And>n. A n < B n"
4.847 + by (induct_tac n, simp add: ab, simp add: C_def avg_def)
4.848 + have A_mono: "\<And>i j. i \<le> j \<Longrightarrow> A i \<le> A j"
4.849 + apply (auto simp add: le_less [where 'a=nat])
4.850 + apply (erule less_Suc_induct)
4.851 + apply (clarsimp simp add: C_def avg_def)
4.852 + apply (simp add: add_divide_distrib [symmetric])
4.853 + apply (rule AB [THEN less_imp_le])
4.854 + apply simp
4.855 + done
4.856 + have B_mono: "\<And>i j. i \<le> j \<Longrightarrow> B j \<le> B i"
4.857 + apply (auto simp add: le_less [where 'a=nat])
4.858 + apply (erule less_Suc_induct)
4.859 + apply (clarsimp simp add: C_def avg_def)
4.860 + apply (simp add: add_divide_distrib [symmetric])
4.861 + apply (rule AB [THEN less_imp_le])
4.862 + apply simp
4.863 + done
4.864 + have cauchy_lemma:
4.865 + "\<And>X. \<forall>n. \<forall>i\<ge>n. A n \<le> X i \<and> X i \<le> B n \<Longrightarrow> cauchy X"
4.866 + apply (rule cauchyI)
4.867 + apply (drule twos [where y="b - a"])
4.868 + apply (erule exE)
4.869 + apply (rule_tac x=n in exI, clarify, rename_tac i j)
4.870 + apply (rule_tac y="B n - A n" in le_less_trans) defer
4.871 + apply (simp add: width)
4.872 + apply (drule_tac x=n in spec)
4.873 + apply (frule_tac x=i in spec, drule (1) mp)
4.874 + apply (frule_tac x=j in spec, drule (1) mp)
4.875 + apply (frule A_mono, drule B_mono)
4.876 + apply (frule A_mono, drule B_mono)
4.877 + apply arith
4.878 + done
4.879 + have "cauchy A"
4.880 + apply (rule cauchy_lemma [rule_format])
4.881 + apply (simp add: A_mono)
4.882 + apply (erule order_trans [OF less_imp_le [OF AB] B_mono])
4.883 + done
4.884 + have "cauchy B"
4.885 + apply (rule cauchy_lemma [rule_format])
4.886 + apply (simp add: B_mono)
4.887 + apply (erule order_trans [OF A_mono less_imp_le [OF AB]])
4.888 + done
4.889 + have 1: "\<forall>x\<in>S. x \<le> Real B"
4.890 + proof
4.891 + fix x assume "x \<in> S"
4.892 + then show "x \<le> Real B"
4.893 + using PB [unfolded P_def] `cauchy B`
4.894 + by (simp add: le_RealI)
4.895 + qed
4.896 + have 2: "\<forall>z. (\<forall>x\<in>S. x \<le> z) \<longrightarrow> Real A \<le> z"
4.897 + apply clarify
4.898 + apply (erule contrapos_pp)
4.899 + apply (simp add: not_le)
4.900 + apply (drule less_RealD [OF `cauchy A`], clarify)
4.901 + apply (subgoal_tac "\<not> P (A n)")
4.902 + apply (simp add: P_def not_le, clarify)
4.903 + apply (erule rev_bexI)
4.904 + apply (erule (1) less_trans)
4.905 + apply (simp add: PA)
4.906 + done
4.907 + have "vanishes (\<lambda>n. (b - a) / 2 ^ n)"
4.908 + proof (rule vanishesI)
4.909 + fix r :: rat assume "0 < r"
4.910 + then obtain k where k: "\<bar>b - a\<bar> / 2 ^ k < r"
4.911 + using twos by fast
4.912 + have "\<forall>n\<ge>k. \<bar>(b - a) / 2 ^ n\<bar> < r"
4.913 + proof (clarify)
4.914 + fix n assume n: "k \<le> n"
4.915 + have "\<bar>(b - a) / 2 ^ n\<bar> = \<bar>b - a\<bar> / 2 ^ n"
4.916 + by simp
4.917 + also have "\<dots> \<le> \<bar>b - a\<bar> / 2 ^ k"
4.918 + using n by (simp add: divide_left_mono mult_pos_pos)
4.919 + also note k
4.920 + finally show "\<bar>(b - a) / 2 ^ n\<bar> < r" .
4.921 + qed
4.922 + thus "\<exists>k. \<forall>n\<ge>k. \<bar>(b - a) / 2 ^ n\<bar> < r" ..
4.923 + qed
4.924 + hence 3: "Real B = Real A"
4.925 + by (simp add: eq_Real `cauchy A` `cauchy B` width)
4.926 + show "\<exists>y. (\<forall>x\<in>S. x \<le> y) \<and> (\<forall>z. (\<forall>x\<in>S. x \<le> z) \<longrightarrow> y \<le> z)"
4.927 + using 1 2 3 by (rule_tac x="Real B" in exI, simp)
4.928 +qed
4.929 +
4.930 +
4.931 +instantiation real :: conditional_complete_linorder
4.932 +begin
4.933 +
4.934 +subsection{*Supremum of a set of reals*}
4.935 +
4.936 +definition
4.937 + Sup_real_def: "Sup X \<equiv> LEAST z::real. \<forall>x\<in>X. x\<le>z"
4.938 +
4.939 +definition
4.940 + Inf_real_def: "Inf (X::real set) \<equiv> - Sup (uminus ` X)"
4.941 +
4.942 +instance
4.943 +proof
4.944 + { fix z x :: real and X :: "real set"
4.945 + assume x: "x \<in> X" and z: "\<And>x. x \<in> X \<Longrightarrow> x \<le> z"
4.946 + 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"
4.947 + using complete_real[of X] by blast
4.948 + then show "x \<le> Sup X"
4.949 + unfolding Sup_real_def by (rule LeastI2_order) (auto simp: x) }
4.950 + note Sup_upper = this
4.951 +
4.952 + { fix z :: real and X :: "real set"
4.953 + assume x: "X \<noteq> {}" and z: "\<And>x. x \<in> X \<Longrightarrow> x \<le> z"
4.954 + 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"
4.955 + using complete_real[of X] by blast
4.956 + then have "Sup X = s"
4.957 + unfolding Sup_real_def by (best intro: Least_equality)
4.958 + also with s z have "... \<le> z"
4.959 + by blast
4.960 + finally show "Sup X \<le> z" . }
4.961 + note Sup_least = this
4.962 +
4.963 + { fix x z :: real and X :: "real set"
4.964 + assume x: "x \<in> X" and z: "\<And>x. x \<in> X \<Longrightarrow> z \<le> x"
4.965 + have "-x \<le> Sup (uminus ` X)"
4.966 + by (rule Sup_upper[of _ _ "- z"]) (auto simp add: image_iff x z)
4.967 + then show "Inf X \<le> x"
4.968 + by (auto simp add: Inf_real_def) }
4.969 +
4.970 + { fix z :: real and X :: "real set"
4.971 + assume x: "X \<noteq> {}" and z: "\<And>x. x \<in> X \<Longrightarrow> z \<le> x"
4.972 + have "Sup (uminus ` X) \<le> -z"
4.973 + using x z by (force intro: Sup_least)
4.974 + then show "z \<le> Inf X"
4.975 + by (auto simp add: Inf_real_def) }
4.976 +qed
4.977 +end
4.978 +
4.979 +text {*
4.980 + \medskip Completeness properties using @{text "isUb"}, @{text "isLub"}:
4.981 +*}
4.982 +
4.983 +lemma reals_complete: "\<exists>X. X \<in> S \<Longrightarrow> \<exists>Y. isUb (UNIV::real set) S Y \<Longrightarrow> \<exists>t. isLub (UNIV :: real set) S t"
4.984 + by (intro exI[of _ "Sup S"] isLub_cSup) (auto simp: setle_def isUb_def intro: cSup_upper)
4.985 +
4.986 +
4.987 +subsection {* Hiding implementation details *}
4.988 +
4.989 +hide_const (open) vanishes cauchy positive Real
4.990 +
4.991 +declare Real_induct [induct del]
4.992 +declare Abs_real_induct [induct del]
4.993 +declare Abs_real_cases [cases del]
4.994 +
4.995 +lemmas [transfer_rule del] =
4.996 + real.All_transfer real.Ex_transfer real.rel_eq_transfer forall_real_transfer
4.997 + zero_real.transfer one_real.transfer plus_real.transfer uminus_real.transfer
4.998 + times_real.transfer inverse_real.transfer positive.transfer real.right_unique
4.999 + real.right_total
4.1000 +
4.1001 +subsection{*More Lemmas*}
4.1002 +
4.1003 +text {* BH: These lemmas should not be necessary; they should be
4.1004 +covered by existing simp rules and simplification procedures. *}
4.1005 +
4.1006 +lemma real_mult_left_cancel: "(c::real) \<noteq> 0 ==> (c*a=c*b) = (a=b)"
4.1007 +by simp (* redundant with mult_cancel_left *)
4.1008 +
4.1009 +lemma real_mult_right_cancel: "(c::real) \<noteq> 0 ==> (a*c=b*c) = (a=b)"
4.1010 +by simp (* redundant with mult_cancel_right *)
4.1011 +
4.1012 +lemma real_mult_less_iff1 [simp]: "(0::real) < z ==> (x*z < y*z) = (x < y)"
4.1013 +by simp (* solved by linordered_ring_less_cancel_factor simproc *)
4.1014 +
4.1015 +lemma real_mult_le_cancel_iff1 [simp]: "(0::real) < z ==> (x*z \<le> y*z) = (x\<le>y)"
4.1016 +by simp (* solved by linordered_ring_le_cancel_factor simproc *)
4.1017 +
4.1018 +lemma real_mult_le_cancel_iff2 [simp]: "(0::real) < z ==> (z*x \<le> z*y) = (x\<le>y)"
4.1019 +by simp (* solved by linordered_ring_le_cancel_factor simproc *)
4.1020 +
4.1021 +
4.1022 +subsection {* Embedding numbers into the Reals *}
4.1023 +
4.1024 +abbreviation
4.1025 + real_of_nat :: "nat \<Rightarrow> real"
4.1026 +where
4.1027 + "real_of_nat \<equiv> of_nat"
4.1028 +
4.1029 +abbreviation
4.1030 + real_of_int :: "int \<Rightarrow> real"
4.1031 +where
4.1032 + "real_of_int \<equiv> of_int"
4.1033 +
4.1034 +abbreviation
4.1035 + real_of_rat :: "rat \<Rightarrow> real"
4.1036 +where
4.1037 + "real_of_rat \<equiv> of_rat"
4.1038 +
4.1039 +consts
4.1040 + (*overloaded constant for injecting other types into "real"*)
4.1041 + real :: "'a => real"
4.1042 +
4.1043 +defs (overloaded)
4.1044 + real_of_nat_def [code_unfold]: "real == real_of_nat"
4.1045 + real_of_int_def [code_unfold]: "real == real_of_int"
4.1046 +
4.1047 +declare [[coercion_enabled]]
4.1048 +declare [[coercion "real::nat\<Rightarrow>real"]]
4.1049 +declare [[coercion "real::int\<Rightarrow>real"]]
4.1050 +declare [[coercion "int"]]
4.1051 +
4.1052 +declare [[coercion_map map]]
4.1053 +declare [[coercion_map "% f g h x. g (h (f x))"]]
4.1054 +declare [[coercion_map "% f g (x,y) . (f x, g y)"]]
4.1055 +
4.1056 +lemma real_eq_of_nat: "real = of_nat"
4.1057 + unfolding real_of_nat_def ..
4.1058 +
4.1059 +lemma real_eq_of_int: "real = of_int"
4.1060 + unfolding real_of_int_def ..
4.1061 +
4.1062 +lemma real_of_int_zero [simp]: "real (0::int) = 0"
4.1063 +by (simp add: real_of_int_def)
4.1064 +
4.1065 +lemma real_of_one [simp]: "real (1::int) = (1::real)"
4.1066 +by (simp add: real_of_int_def)
4.1067 +
4.1068 +lemma real_of_int_add [simp]: "real(x + y) = real (x::int) + real y"
4.1069 +by (simp add: real_of_int_def)
4.1070 +
4.1071 +lemma real_of_int_minus [simp]: "real(-x) = -real (x::int)"
4.1072 +by (simp add: real_of_int_def)
4.1073 +
4.1074 +lemma real_of_int_diff [simp]: "real(x - y) = real (x::int) - real y"
4.1075 +by (simp add: real_of_int_def)
4.1076 +
4.1077 +lemma real_of_int_mult [simp]: "real(x * y) = real (x::int) * real y"
4.1078 +by (simp add: real_of_int_def)
4.1079 +
4.1080 +lemma real_of_int_power [simp]: "real (x ^ n) = real (x::int) ^ n"
4.1081 +by (simp add: real_of_int_def of_int_power)
4.1082 +
4.1083 +lemmas power_real_of_int = real_of_int_power [symmetric]
4.1084 +
4.1085 +lemma real_of_int_setsum [simp]: "real ((SUM x:A. f x)::int) = (SUM x:A. real(f x))"
4.1086 + apply (subst real_eq_of_int)+
4.1087 + apply (rule of_int_setsum)
4.1088 +done
4.1089 +
4.1090 +lemma real_of_int_setprod [simp]: "real ((PROD x:A. f x)::int) =
4.1091 + (PROD x:A. real(f x))"
4.1092 + apply (subst real_eq_of_int)+
4.1093 + apply (rule of_int_setprod)
4.1094 +done
4.1095 +
4.1096 +lemma real_of_int_zero_cancel [simp, algebra, presburger]: "(real x = 0) = (x = (0::int))"
4.1097 +by (simp add: real_of_int_def)
4.1098 +
4.1099 +lemma real_of_int_inject [iff, algebra, presburger]: "(real (x::int) = real y) = (x = y)"
4.1100 +by (simp add: real_of_int_def)
4.1101 +
4.1102 +lemma real_of_int_less_iff [iff, presburger]: "(real (x::int) < real y) = (x < y)"
4.1103 +by (simp add: real_of_int_def)
4.1104 +
4.1105 +lemma real_of_int_le_iff [simp, presburger]: "(real (x::int) \<le> real y) = (x \<le> y)"
4.1106 +by (simp add: real_of_int_def)
4.1107 +
4.1108 +lemma real_of_int_gt_zero_cancel_iff [simp, presburger]: "(0 < real (n::int)) = (0 < n)"
4.1109 +by (simp add: real_of_int_def)
4.1110 +
4.1111 +lemma real_of_int_ge_zero_cancel_iff [simp, presburger]: "(0 <= real (n::int)) = (0 <= n)"
4.1112 +by (simp add: real_of_int_def)
4.1113 +
4.1114 +lemma real_of_int_lt_zero_cancel_iff [simp, presburger]: "(real (n::int) < 0) = (n < 0)"
4.1115 +by (simp add: real_of_int_def)
4.1116 +
4.1117 +lemma real_of_int_le_zero_cancel_iff [simp, presburger]: "(real (n::int) <= 0) = (n <= 0)"
4.1118 +by (simp add: real_of_int_def)
4.1119 +
4.1120 +lemma one_less_real_of_int_cancel_iff: "1 < real (i :: int) \<longleftrightarrow> 1 < i"
4.1121 + unfolding real_of_one[symmetric] real_of_int_less_iff ..
4.1122 +
4.1123 +lemma one_le_real_of_int_cancel_iff: "1 \<le> real (i :: int) \<longleftrightarrow> 1 \<le> i"
4.1124 + unfolding real_of_one[symmetric] real_of_int_le_iff ..
4.1125 +
4.1126 +lemma real_of_int_less_one_cancel_iff: "real (i :: int) < 1 \<longleftrightarrow> i < 1"
4.1127 + unfolding real_of_one[symmetric] real_of_int_less_iff ..
4.1128 +
4.1129 +lemma real_of_int_le_one_cancel_iff: "real (i :: int) \<le> 1 \<longleftrightarrow> i \<le> 1"
4.1130 + unfolding real_of_one[symmetric] real_of_int_le_iff ..
4.1131 +
4.1132 +lemma real_of_int_abs [simp]: "real (abs x) = abs(real (x::int))"
4.1133 +by (auto simp add: abs_if)
4.1134 +
4.1135 +lemma int_less_real_le: "((n::int) < m) = (real n + 1 <= real m)"
4.1136 + apply (subgoal_tac "real n + 1 = real (n + 1)")
4.1137 + apply (simp del: real_of_int_add)
4.1138 + apply auto
4.1139 +done
4.1140 +
4.1141 +lemma int_le_real_less: "((n::int) <= m) = (real n < real m + 1)"
4.1142 + apply (subgoal_tac "real m + 1 = real (m + 1)")
4.1143 + apply (simp del: real_of_int_add)
4.1144 + apply simp
4.1145 +done
4.1146 +
4.1147 +lemma real_of_int_div_aux: "(real (x::int)) / (real d) =
4.1148 + real (x div d) + (real (x mod d)) / (real d)"
4.1149 +proof -
4.1150 + have "x = (x div d) * d + x mod d"
4.1151 + by auto
4.1152 + then have "real x = real (x div d) * real d + real(x mod d)"
4.1153 + by (simp only: real_of_int_mult [THEN sym] real_of_int_add [THEN sym])
4.1154 + then have "real x / real d = ... / real d"
4.1155 + by simp
4.1156 + then show ?thesis
4.1157 + by (auto simp add: add_divide_distrib algebra_simps)
4.1158 +qed
4.1159 +
4.1160 +lemma real_of_int_div: "(d :: int) dvd n ==>
4.1161 + real(n div d) = real n / real d"
4.1162 + apply (subst real_of_int_div_aux)
4.1163 + apply simp
4.1164 + apply (simp add: dvd_eq_mod_eq_0)
4.1165 +done
4.1166 +
4.1167 +lemma real_of_int_div2:
4.1168 + "0 <= real (n::int) / real (x) - real (n div x)"
4.1169 + apply (case_tac "x = 0")
4.1170 + apply simp
4.1171 + apply (case_tac "0 < x")
4.1172 + apply (simp add: algebra_simps)
4.1173 + apply (subst real_of_int_div_aux)
4.1174 + apply simp
4.1175 + apply (subst zero_le_divide_iff)
4.1176 + apply auto
4.1177 + apply (simp add: algebra_simps)
4.1178 + apply (subst real_of_int_div_aux)
4.1179 + apply simp
4.1180 + apply (subst zero_le_divide_iff)
4.1181 + apply auto
4.1182 +done
4.1183 +
4.1184 +lemma real_of_int_div3:
4.1185 + "real (n::int) / real (x) - real (n div x) <= 1"
4.1186 + apply (simp add: algebra_simps)
4.1187 + apply (subst real_of_int_div_aux)
4.1188 + apply (auto simp add: divide_le_eq intro: order_less_imp_le)
4.1189 +done
4.1190 +
4.1191 +lemma real_of_int_div4: "real (n div x) <= real (n::int) / real x"
4.1192 +by (insert real_of_int_div2 [of n x], simp)
4.1193 +
4.1194 +lemma Ints_real_of_int [simp]: "real (x::int) \<in> Ints"
4.1195 +unfolding real_of_int_def by (rule Ints_of_int)
4.1196 +
4.1197 +
4.1198 +subsection{*Embedding the Naturals into the Reals*}
4.1199 +
4.1200 +lemma real_of_nat_zero [simp]: "real (0::nat) = 0"
4.1201 +by (simp add: real_of_nat_def)
4.1202 +
4.1203 +lemma real_of_nat_1 [simp]: "real (1::nat) = 1"
4.1204 +by (simp add: real_of_nat_def)
4.1205 +
4.1206 +lemma real_of_nat_one [simp]: "real (Suc 0) = (1::real)"
4.1207 +by (simp add: real_of_nat_def)
4.1208 +
4.1209 +lemma real_of_nat_add [simp]: "real (m + n) = real (m::nat) + real n"
4.1210 +by (simp add: real_of_nat_def)
4.1211 +
4.1212 +(*Not for addsimps: often the LHS is used to represent a positive natural*)
4.1213 +lemma real_of_nat_Suc: "real (Suc n) = real n + (1::real)"
4.1214 +by (simp add: real_of_nat_def)
4.1215 +
4.1216 +lemma real_of_nat_less_iff [iff]:
4.1217 + "(real (n::nat) < real m) = (n < m)"
4.1218 +by (simp add: real_of_nat_def)
4.1219 +
4.1220 +lemma real_of_nat_le_iff [iff]: "(real (n::nat) \<le> real m) = (n \<le> m)"
4.1221 +by (simp add: real_of_nat_def)
4.1222 +
4.1223 +lemma real_of_nat_ge_zero [iff]: "0 \<le> real (n::nat)"
4.1224 +by (simp add: real_of_nat_def)
4.1225 +
4.1226 +lemma real_of_nat_Suc_gt_zero: "0 < real (Suc n)"
4.1227 +by (simp add: real_of_nat_def del: of_nat_Suc)
4.1228 +
4.1229 +lemma real_of_nat_mult [simp]: "real (m * n) = real (m::nat) * real n"
4.1230 +by (simp add: real_of_nat_def of_nat_mult)
4.1231 +
4.1232 +lemma real_of_nat_power [simp]: "real (m ^ n) = real (m::nat) ^ n"
4.1233 +by (simp add: real_of_nat_def of_nat_power)
4.1234 +
4.1235 +lemmas power_real_of_nat = real_of_nat_power [symmetric]
4.1236 +
4.1237 +lemma real_of_nat_setsum [simp]: "real ((SUM x:A. f x)::nat) =
4.1238 + (SUM x:A. real(f x))"
4.1239 + apply (subst real_eq_of_nat)+
4.1240 + apply (rule of_nat_setsum)
4.1241 +done
4.1242 +
4.1243 +lemma real_of_nat_setprod [simp]: "real ((PROD x:A. f x)::nat) =
4.1244 + (PROD x:A. real(f x))"
4.1245 + apply (subst real_eq_of_nat)+
4.1246 + apply (rule of_nat_setprod)
4.1247 +done
4.1248 +
4.1249 +lemma real_of_card: "real (card A) = setsum (%x.1) A"
4.1250 + apply (subst card_eq_setsum)
4.1251 + apply (subst real_of_nat_setsum)
4.1252 + apply simp
4.1253 +done
4.1254 +
4.1255 +lemma real_of_nat_inject [iff]: "(real (n::nat) = real m) = (n = m)"
4.1256 +by (simp add: real_of_nat_def)
4.1257 +
4.1258 +lemma real_of_nat_zero_iff [iff]: "(real (n::nat) = 0) = (n = 0)"
4.1259 +by (simp add: real_of_nat_def)
4.1260 +
4.1261 +lemma real_of_nat_diff: "n \<le> m ==> real (m - n) = real (m::nat) - real n"
4.1262 +by (simp add: add: real_of_nat_def of_nat_diff)
4.1263 +
4.1264 +lemma real_of_nat_gt_zero_cancel_iff [simp]: "(0 < real (n::nat)) = (0 < n)"
4.1265 +by (auto simp: real_of_nat_def)
4.1266 +
4.1267 +lemma real_of_nat_le_zero_cancel_iff [simp]: "(real (n::nat) \<le> 0) = (n = 0)"
4.1268 +by (simp add: add: real_of_nat_def)
4.1269 +
4.1270 +lemma not_real_of_nat_less_zero [simp]: "~ real (n::nat) < 0"
4.1271 +by (simp add: add: real_of_nat_def)
4.1272 +
4.1273 +lemma nat_less_real_le: "((n::nat) < m) = (real n + 1 <= real m)"
4.1274 + apply (subgoal_tac "real n + 1 = real (Suc n)")
4.1275 + apply simp
4.1276 + apply (auto simp add: real_of_nat_Suc)
4.1277 +done
4.1278 +
4.1279 +lemma nat_le_real_less: "((n::nat) <= m) = (real n < real m + 1)"
4.1280 + apply (subgoal_tac "real m + 1 = real (Suc m)")
4.1281 + apply (simp add: less_Suc_eq_le)
4.1282 + apply (simp add: real_of_nat_Suc)
4.1283 +done
4.1284 +
4.1285 +lemma real_of_nat_div_aux: "(real (x::nat)) / (real d) =
4.1286 + real (x div d) + (real (x mod d)) / (real d)"
4.1287 +proof -
4.1288 + have "x = (x div d) * d + x mod d"
4.1289 + by auto
4.1290 + then have "real x = real (x div d) * real d + real(x mod d)"
4.1291 + by (simp only: real_of_nat_mult [THEN sym] real_of_nat_add [THEN sym])
4.1292 + then have "real x / real d = \<dots> / real d"
4.1293 + by simp
4.1294 + then show ?thesis
4.1295 + by (auto simp add: add_divide_distrib algebra_simps)
4.1296 +qed
4.1297 +
4.1298 +lemma real_of_nat_div: "(d :: nat) dvd n ==>
4.1299 + real(n div d) = real n / real d"
4.1300 + by (subst real_of_nat_div_aux)
4.1301 + (auto simp add: dvd_eq_mod_eq_0 [symmetric])
4.1302 +
4.1303 +lemma real_of_nat_div2:
4.1304 + "0 <= real (n::nat) / real (x) - real (n div x)"
4.1305 +apply (simp add: algebra_simps)
4.1306 +apply (subst real_of_nat_div_aux)
4.1307 +apply simp
4.1308 +apply (subst zero_le_divide_iff)
4.1309 +apply simp
4.1310 +done
4.1311 +
4.1312 +lemma real_of_nat_div3:
4.1313 + "real (n::nat) / real (x) - real (n div x) <= 1"
4.1314 +apply(case_tac "x = 0")
4.1315 +apply (simp)
4.1316 +apply (simp add: algebra_simps)
4.1317 +apply (subst real_of_nat_div_aux)
4.1318 +apply simp
4.1319 +done
4.1320 +
4.1321 +lemma real_of_nat_div4: "real (n div x) <= real (n::nat) / real x"
4.1322 +by (insert real_of_nat_div2 [of n x], simp)
4.1323 +
4.1324 +lemma real_of_int_of_nat_eq [simp]: "real (of_nat n :: int) = real n"
4.1325 +by (simp add: real_of_int_def real_of_nat_def)
4.1326 +
4.1327 +lemma real_nat_eq_real [simp]: "0 <= x ==> real(nat x) = real x"
4.1328 + apply (subgoal_tac "real(int(nat x)) = real(nat x)")
4.1329 + apply force
4.1330 + apply (simp only: real_of_int_of_nat_eq)
4.1331 +done
4.1332 +
4.1333 +lemma Nats_real_of_nat [simp]: "real (n::nat) \<in> Nats"
4.1334 +unfolding real_of_nat_def by (rule of_nat_in_Nats)
4.1335 +
4.1336 +lemma Ints_real_of_nat [simp]: "real (n::nat) \<in> Ints"
4.1337 +unfolding real_of_nat_def by (rule Ints_of_nat)
4.1338 +
4.1339 +subsection {* The Archimedean Property of the Reals *}
4.1340 +
4.1341 +theorem reals_Archimedean:
4.1342 + assumes x_pos: "0 < x"
4.1343 + shows "\<exists>n. inverse (real (Suc n)) < x"
4.1344 + unfolding real_of_nat_def using x_pos
4.1345 + by (rule ex_inverse_of_nat_Suc_less)
4.1346 +
4.1347 +lemma reals_Archimedean2: "\<exists>n. (x::real) < real (n::nat)"
4.1348 + unfolding real_of_nat_def by (rule ex_less_of_nat)
4.1349 +
4.1350 +lemma reals_Archimedean3:
4.1351 + assumes x_greater_zero: "0 < x"
4.1352 + shows "\<forall>(y::real). \<exists>(n::nat). y < real n * x"
4.1353 + unfolding real_of_nat_def using `0 < x`
4.1354 + by (auto intro: ex_less_of_nat_mult)
4.1355 +
4.1356 +
4.1357 +subsection{* Rationals *}
4.1358 +
4.1359 +lemma Rats_real_nat[simp]: "real(n::nat) \<in> \<rat>"
4.1360 +by (simp add: real_eq_of_nat)
4.1361 +
4.1362 +
4.1363 +lemma Rats_eq_int_div_int:
4.1364 + "\<rat> = { real(i::int)/real(j::int) |i j. j \<noteq> 0}" (is "_ = ?S")
4.1365 +proof
4.1366 + show "\<rat> \<subseteq> ?S"
4.1367 + proof
4.1368 + fix x::real assume "x : \<rat>"
4.1369 + then obtain r where "x = of_rat r" unfolding Rats_def ..
4.1370 + have "of_rat r : ?S"
4.1371 + by (cases r)(auto simp add:of_rat_rat real_eq_of_int)
4.1372 + thus "x : ?S" using `x = of_rat r` by simp
4.1373 + qed
4.1374 +next
4.1375 + show "?S \<subseteq> \<rat>"
4.1376 + proof(auto simp:Rats_def)
4.1377 + fix i j :: int assume "j \<noteq> 0"
4.1378 + hence "real i / real j = of_rat(Fract i j)"
4.1379 + by (simp add:of_rat_rat real_eq_of_int)
4.1380 + thus "real i / real j \<in> range of_rat" by blast
4.1381 + qed
4.1382 +qed
4.1383 +
4.1384 +lemma Rats_eq_int_div_nat:
4.1385 + "\<rat> = { real(i::int)/real(n::nat) |i n. n \<noteq> 0}"
4.1386 +proof(auto simp:Rats_eq_int_div_int)
4.1387 + fix i j::int assume "j \<noteq> 0"
4.1388 + show "EX (i'::int) (n::nat). real i/real j = real i'/real n \<and> 0<n"
4.1389 + proof cases
4.1390 + assume "j>0"
4.1391 + hence "real i/real j = real i/real(nat j) \<and> 0<nat j"
4.1392 + by (simp add: real_eq_of_int real_eq_of_nat of_nat_nat)
4.1393 + thus ?thesis by blast
4.1394 + next
4.1395 + assume "~ j>0"
4.1396 + hence "real i/real j = real(-i)/real(nat(-j)) \<and> 0<nat(-j)" using `j\<noteq>0`
4.1397 + by (simp add: real_eq_of_int real_eq_of_nat of_nat_nat)
4.1398 + thus ?thesis by blast
4.1399 + qed
4.1400 +next
4.1401 + fix i::int and n::nat assume "0 < n"
4.1402 + hence "real i/real n = real i/real(int n) \<and> int n \<noteq> 0" by simp
4.1403 + thus "\<exists>(i'::int) j::int. real i/real n = real i'/real j \<and> j \<noteq> 0" by blast
4.1404 +qed
4.1405 +
4.1406 +lemma Rats_abs_nat_div_natE:
4.1407 + assumes "x \<in> \<rat>"
4.1408 + obtains m n :: nat
4.1409 + where "n \<noteq> 0" and "\<bar>x\<bar> = real m / real n" and "gcd m n = 1"
4.1410 +proof -
4.1411 + from `x \<in> \<rat>` obtain i::int and n::nat where "n \<noteq> 0" and "x = real i / real n"
4.1412 + by(auto simp add: Rats_eq_int_div_nat)
4.1413 + hence "\<bar>x\<bar> = real(nat(abs i)) / real n" by simp
4.1414 + then obtain m :: nat where x_rat: "\<bar>x\<bar> = real m / real n" by blast
4.1415 + let ?gcd = "gcd m n"
4.1416 + from `n\<noteq>0` have gcd: "?gcd \<noteq> 0" by simp
4.1417 + let ?k = "m div ?gcd"
4.1418 + let ?l = "n div ?gcd"
4.1419 + let ?gcd' = "gcd ?k ?l"
4.1420 + have "?gcd dvd m" .. then have gcd_k: "?gcd * ?k = m"
4.1421 + by (rule dvd_mult_div_cancel)
4.1422 + have "?gcd dvd n" .. then have gcd_l: "?gcd * ?l = n"
4.1423 + by (rule dvd_mult_div_cancel)
4.1424 + from `n\<noteq>0` and gcd_l have "?l \<noteq> 0" by (auto iff del: neq0_conv)
4.1425 + moreover
4.1426 + have "\<bar>x\<bar> = real ?k / real ?l"
4.1427 + proof -
4.1428 + from gcd have "real ?k / real ?l =
4.1429 + real (?gcd * ?k) / real (?gcd * ?l)" by simp
4.1430 + also from gcd_k and gcd_l have "\<dots> = real m / real n" by simp
4.1431 + also from x_rat have "\<dots> = \<bar>x\<bar>" ..
4.1432 + finally show ?thesis ..
4.1433 + qed
4.1434 + moreover
4.1435 + have "?gcd' = 1"
4.1436 + proof -
4.1437 + have "?gcd * ?gcd' = gcd (?gcd * ?k) (?gcd * ?l)"
4.1438 + by (rule gcd_mult_distrib_nat)
4.1439 + with gcd_k gcd_l have "?gcd * ?gcd' = ?gcd" by simp
4.1440 + with gcd show ?thesis by auto
4.1441 + qed
4.1442 + ultimately show ?thesis ..
4.1443 +qed
4.1444 +
4.1445 +subsection{*Density of the Rational Reals in the Reals*}
4.1446 +
4.1447 +text{* This density proof is due to Stefan Richter and was ported by TN. The
4.1448 +original source is \emph{Real Analysis} by H.L. Royden.
4.1449 +It employs the Archimedean property of the reals. *}
4.1450 +
4.1451 +lemma Rats_dense_in_real:
4.1452 + fixes x :: real
4.1453 + assumes "x < y" shows "\<exists>r\<in>\<rat>. x < r \<and> r < y"
4.1454 +proof -
4.1455 + from `x<y` have "0 < y-x" by simp
4.1456 + with reals_Archimedean obtain q::nat
4.1457 + where q: "inverse (real q) < y-x" and "0 < q" by auto
4.1458 + def p \<equiv> "ceiling (y * real q) - 1"
4.1459 + def r \<equiv> "of_int p / real q"
4.1460 + from q have "x < y - inverse (real q)" by simp
4.1461 + also have "y - inverse (real q) \<le> r"
4.1462 + unfolding r_def p_def
4.1463 + by (simp add: le_divide_eq left_diff_distrib le_of_int_ceiling `0 < q`)
4.1464 + finally have "x < r" .
4.1465 + moreover have "r < y"
4.1466 + unfolding r_def p_def
4.1467 + by (simp add: divide_less_eq diff_less_eq `0 < q`
4.1468 + less_ceiling_iff [symmetric])
4.1469 + moreover from r_def have "r \<in> \<rat>" by simp
4.1470 + ultimately show ?thesis by fast
4.1471 +qed
4.1472 +
4.1473 +
4.1474 +
4.1475 +subsection{*Numerals and Arithmetic*}
4.1476 +
4.1477 +lemma [code_abbrev]:
4.1478 + "real_of_int (numeral k) = numeral k"
4.1479 + "real_of_int (neg_numeral k) = neg_numeral k"
4.1480 + by simp_all
4.1481 +
4.1482 +text{*Collapse applications of @{term real} to @{term number_of}*}
4.1483 +lemma real_numeral [simp]:
4.1484 + "real (numeral v :: int) = numeral v"
4.1485 + "real (neg_numeral v :: int) = neg_numeral v"
4.1486 +by (simp_all add: real_of_int_def)
4.1487 +
4.1488 +lemma real_of_nat_numeral [simp]:
4.1489 + "real (numeral v :: nat) = numeral v"
4.1490 +by (simp add: real_of_nat_def)
4.1491 +
4.1492 +declaration {*
4.1493 + K (Lin_Arith.add_inj_thms [@{thm real_of_nat_le_iff} RS iffD2, @{thm real_of_nat_inject} RS iffD2]
4.1494 + (* not needed because x < (y::nat) can be rewritten as Suc x <= y: real_of_nat_less_iff RS iffD2 *)
4.1495 + #> Lin_Arith.add_inj_thms [@{thm real_of_int_le_iff} RS iffD2, @{thm real_of_int_inject} RS iffD2]
4.1496 + (* not needed because x < (y::int) can be rewritten as x + 1 <= y: real_of_int_less_iff RS iffD2 *)
4.1497 + #> Lin_Arith.add_simps [@{thm real_of_nat_zero}, @{thm real_of_nat_Suc}, @{thm real_of_nat_add},
4.1498 + @{thm real_of_nat_mult}, @{thm real_of_int_zero}, @{thm real_of_one},
4.1499 + @{thm real_of_int_add}, @{thm real_of_int_minus}, @{thm real_of_int_diff},
4.1500 + @{thm real_of_int_mult}, @{thm real_of_int_of_nat_eq},
4.1501 + @{thm real_of_nat_numeral}, @{thm real_numeral(1)}, @{thm real_numeral(2)}]
4.1502 + #> Lin_Arith.add_inj_const (@{const_name real}, @{typ "nat \<Rightarrow> real"})
4.1503 + #> Lin_Arith.add_inj_const (@{const_name real}, @{typ "int \<Rightarrow> real"}))
4.1504 +*}
4.1505 +
4.1506 +
4.1507 +subsection{* Simprules combining x+y and 0: ARE THEY NEEDED?*}
4.1508 +
4.1509 +lemma real_add_minus_iff [simp]: "(x + - a = (0::real)) = (x=a)"
4.1510 +by arith
4.1511 +
4.1512 +text {* FIXME: redundant with @{text add_eq_0_iff} below *}
4.1513 +lemma real_add_eq_0_iff: "(x+y = (0::real)) = (y = -x)"
4.1514 +by auto
4.1515 +
4.1516 +lemma real_add_less_0_iff: "(x+y < (0::real)) = (y < -x)"
4.1517 +by auto
4.1518 +
4.1519 +lemma real_0_less_add_iff: "((0::real) < x+y) = (-x < y)"
4.1520 +by auto
4.1521 +
4.1522 +lemma real_add_le_0_iff: "(x+y \<le> (0::real)) = (y \<le> -x)"
4.1523 +by auto
4.1524 +
4.1525 +lemma real_0_le_add_iff: "((0::real) \<le> x+y) = (-x \<le> y)"
4.1526 +by auto
4.1527 +
4.1528 +subsection {* Lemmas about powers *}
4.1529 +
4.1530 +text {* FIXME: declare this in Rings.thy or not at all *}
4.1531 +declare abs_mult_self [simp]
4.1532 +
4.1533 +(* used by Import/HOL/real.imp *)
4.1534 +lemma two_realpow_ge_one: "(1::real) \<le> 2 ^ n"
4.1535 +by simp
4.1536 +
4.1537 +lemma two_realpow_gt [simp]: "real (n::nat) < 2 ^ n"
4.1538 +apply (induct "n")
4.1539 +apply (auto simp add: real_of_nat_Suc)
4.1540 +apply (subst mult_2)
4.1541 +apply (erule add_less_le_mono)
4.1542 +apply (rule two_realpow_ge_one)
4.1543 +done
4.1544 +
4.1545 +text {* TODO: no longer real-specific; rename and move elsewhere *}
4.1546 +lemma realpow_Suc_le_self:
4.1547 + fixes r :: "'a::linordered_semidom"
4.1548 + shows "[| 0 \<le> r; r \<le> 1 |] ==> r ^ Suc n \<le> r"
4.1549 +by (insert power_decreasing [of 1 "Suc n" r], simp)
4.1550 +
4.1551 +text {* TODO: no longer real-specific; rename and move elsewhere *}
4.1552 +lemma realpow_minus_mult:
4.1553 + fixes x :: "'a::monoid_mult"
4.1554 + shows "0 < n \<Longrightarrow> x ^ (n - 1) * x = x ^ n"
4.1555 +by (simp add: power_commutes split add: nat_diff_split)
4.1556 +
4.1557 +text {* FIXME: declare this [simp] for all types, or not at all *}
4.1558 +lemma real_two_squares_add_zero_iff [simp]:
4.1559 + "(x * x + y * y = 0) = ((x::real) = 0 \<and> y = 0)"
4.1560 +by (rule sum_squares_eq_zero_iff)
4.1561 +
4.1562 +text {* FIXME: declare this [simp] for all types, or not at all *}
4.1563 +lemma realpow_two_sum_zero_iff [simp]:
4.1564 + "(x ^ 2 + y ^ 2 = (0::real)) = (x = 0 & y = 0)"
4.1565 +by (rule sum_power2_eq_zero_iff)
4.1566 +
4.1567 +lemma real_minus_mult_self_le [simp]: "-(u * u) \<le> (x * (x::real))"
4.1568 +by (rule_tac y = 0 in order_trans, auto)
4.1569 +
4.1570 +lemma realpow_square_minus_le [simp]: "-(u ^ 2) \<le> (x::real) ^ 2"
4.1571 +by (auto simp add: power2_eq_square)
4.1572 +
4.1573 +
4.1574 +lemma numeral_power_le_real_of_nat_cancel_iff[simp]:
4.1575 + "(numeral x::real) ^ n \<le> real a \<longleftrightarrow> (numeral x::nat) ^ n \<le> a"
4.1576 + unfolding real_of_nat_le_iff[symmetric] by simp
4.1577 +
4.1578 +lemma real_of_nat_le_numeral_power_cancel_iff[simp]:
4.1579 + "real a \<le> (numeral x::real) ^ n \<longleftrightarrow> a \<le> (numeral x::nat) ^ n"
4.1580 + unfolding real_of_nat_le_iff[symmetric] by simp
4.1581 +
4.1582 +lemma numeral_power_le_real_of_int_cancel_iff[simp]:
4.1583 + "(numeral x::real) ^ n \<le> real a \<longleftrightarrow> (numeral x::int) ^ n \<le> a"
4.1584 + unfolding real_of_int_le_iff[symmetric] by simp
4.1585 +
4.1586 +lemma real_of_int_le_numeral_power_cancel_iff[simp]:
4.1587 + "real a \<le> (numeral x::real) ^ n \<longleftrightarrow> a \<le> (numeral x::int) ^ n"
4.1588 + unfolding real_of_int_le_iff[symmetric] by simp
4.1589 +
4.1590 +lemma neg_numeral_power_le_real_of_int_cancel_iff[simp]:
4.1591 + "(neg_numeral x::real) ^ n \<le> real a \<longleftrightarrow> (neg_numeral x::int) ^ n \<le> a"
4.1592 + unfolding real_of_int_le_iff[symmetric] by simp
4.1593 +
4.1594 +lemma real_of_int_le_neg_numeral_power_cancel_iff[simp]:
4.1595 + "real a \<le> (neg_numeral x::real) ^ n \<longleftrightarrow> a \<le> (neg_numeral x::int) ^ n"
4.1596 + unfolding real_of_int_le_iff[symmetric] by simp
4.1597 +
4.1598 +subsection{*Density of the Reals*}
4.1599 +
4.1600 +lemma real_lbound_gt_zero:
4.1601 + "[| (0::real) < d1; 0 < d2 |] ==> \<exists>e. 0 < e & e < d1 & e < d2"
4.1602 +apply (rule_tac x = " (min d1 d2) /2" in exI)
4.1603 +apply (simp add: min_def)
4.1604 +done
4.1605 +
4.1606 +
4.1607 +text{*Similar results are proved in @{text Fields}*}
4.1608 +lemma real_less_half_sum: "x < y ==> x < (x+y) / (2::real)"
4.1609 + by auto
4.1610 +
4.1611 +lemma real_gt_half_sum: "x < y ==> (x+y)/(2::real) < y"
4.1612 + by auto
4.1613 +
4.1614 +lemma real_sum_of_halves: "x/2 + x/2 = (x::real)"
4.1615 + by simp
4.1616 +
4.1617 +subsection{*Absolute Value Function for the Reals*}
4.1618 +
4.1619 +lemma abs_minus_add_cancel: "abs(x + (-y)) = abs (y + (-(x::real)))"
4.1620 +by (simp add: abs_if)
4.1621 +
4.1622 +(* FIXME: redundant, but used by Integration/RealRandVar.thy in AFP *)
4.1623 +lemma abs_le_interval_iff: "(abs x \<le> r) = (-r\<le>x & x\<le>(r::real))"
4.1624 +by (force simp add: abs_le_iff)
4.1625 +
4.1626 +lemma abs_add_one_gt_zero: "(0::real) < 1 + abs(x)"
4.1627 +by (simp add: abs_if)
4.1628 +
4.1629 +lemma abs_real_of_nat_cancel [simp]: "abs (real x) = real (x::nat)"
4.1630 +by (rule abs_of_nonneg [OF real_of_nat_ge_zero])
4.1631 +
4.1632 +lemma abs_add_one_not_less_self: "~ abs(x) + (1::real) < x"
4.1633 +by simp
4.1634 +
4.1635 +lemma abs_sum_triangle_ineq: "abs ((x::real) + y + (-l + -m)) \<le> abs(x + -l) + abs(y + -m)"
4.1636 +by simp
4.1637 +
4.1638 +
4.1639 +subsection{*Floor and Ceiling Functions from the Reals to the Integers*}
4.1640 +
4.1641 +(* FIXME: theorems for negative numerals *)
4.1642 +lemma numeral_less_real_of_int_iff [simp]:
4.1643 + "((numeral n) < real (m::int)) = (numeral n < m)"
4.1644 +apply auto
4.1645 +apply (rule real_of_int_less_iff [THEN iffD1])
4.1646 +apply (drule_tac [2] real_of_int_less_iff [THEN iffD2], auto)
4.1647 +done
4.1648 +
4.1649 +lemma numeral_less_real_of_int_iff2 [simp]:
4.1650 + "(real (m::int) < (numeral n)) = (m < numeral n)"
4.1651 +apply auto
4.1652 +apply (rule real_of_int_less_iff [THEN iffD1])
4.1653 +apply (drule_tac [2] real_of_int_less_iff [THEN iffD2], auto)
4.1654 +done
4.1655 +
4.1656 +lemma numeral_le_real_of_int_iff [simp]:
4.1657 + "((numeral n) \<le> real (m::int)) = (numeral n \<le> m)"
4.1658 +by (simp add: linorder_not_less [symmetric])
4.1659 +
4.1660 +lemma numeral_le_real_of_int_iff2 [simp]:
4.1661 + "(real (m::int) \<le> (numeral n)) = (m \<le> numeral n)"
4.1662 +by (simp add: linorder_not_less [symmetric])
4.1663 +
4.1664 +lemma floor_real_of_nat [simp]: "floor (real (n::nat)) = int n"
4.1665 +unfolding real_of_nat_def by simp
4.1666 +
4.1667 +lemma floor_minus_real_of_nat [simp]: "floor (- real (n::nat)) = - int n"
4.1668 +unfolding real_of_nat_def by (simp add: floor_minus)
4.1669 +
4.1670 +lemma floor_real_of_int [simp]: "floor (real (n::int)) = n"
4.1671 +unfolding real_of_int_def by simp
4.1672 +
4.1673 +lemma floor_minus_real_of_int [simp]: "floor (- real (n::int)) = - n"
4.1674 +unfolding real_of_int_def by (simp add: floor_minus)
4.1675 +
4.1676 +lemma real_lb_ub_int: " \<exists>n::int. real n \<le> r & r < real (n+1)"
4.1677 +unfolding real_of_int_def by (rule floor_exists)
4.1678 +
4.1679 +lemma lemma_floor:
4.1680 + assumes a1: "real m \<le> r" and a2: "r < real n + 1"
4.1681 + shows "m \<le> (n::int)"
4.1682 +proof -
4.1683 + have "real m < real n + 1" using a1 a2 by (rule order_le_less_trans)
4.1684 + also have "... = real (n + 1)" by simp
4.1685 + finally have "m < n + 1" by (simp only: real_of_int_less_iff)
4.1686 + thus ?thesis by arith
4.1687 +qed
4.1688 +
4.1689 +lemma real_of_int_floor_le [simp]: "real (floor r) \<le> r"
4.1690 +unfolding real_of_int_def by (rule of_int_floor_le)
4.1691 +
4.1692 +lemma lemma_floor2: "real n < real (x::int) + 1 ==> n \<le> x"
4.1693 +by (auto intro: lemma_floor)
4.1694 +
4.1695 +lemma real_of_int_floor_cancel [simp]:
4.1696 + "(real (floor x) = x) = (\<exists>n::int. x = real n)"
4.1697 + using floor_real_of_int by metis
4.1698 +
4.1699 +lemma floor_eq: "[| real n < x; x < real n + 1 |] ==> floor x = n"
4.1700 + unfolding real_of_int_def using floor_unique [of n x] by simp
4.1701 +
4.1702 +lemma floor_eq2: "[| real n \<le> x; x < real n + 1 |] ==> floor x = n"
4.1703 + unfolding real_of_int_def by (rule floor_unique)
4.1704 +
4.1705 +lemma floor_eq3: "[| real n < x; x < real (Suc n) |] ==> nat(floor x) = n"
4.1706 +apply (rule inj_int [THEN injD])
4.1707 +apply (simp add: real_of_nat_Suc)
4.1708 +apply (simp add: real_of_nat_Suc floor_eq floor_eq [where n = "int n"])
4.1709 +done
4.1710 +
4.1711 +lemma floor_eq4: "[| real n \<le> x; x < real (Suc n) |] ==> nat(floor x) = n"
4.1712 +apply (drule order_le_imp_less_or_eq)
4.1713 +apply (auto intro: floor_eq3)
4.1714 +done
4.1715 +
4.1716 +lemma real_of_int_floor_ge_diff_one [simp]: "r - 1 \<le> real(floor r)"
4.1717 + unfolding real_of_int_def using floor_correct [of r] by simp
4.1718 +
4.1719 +lemma real_of_int_floor_gt_diff_one [simp]: "r - 1 < real(floor r)"
4.1720 + unfolding real_of_int_def using floor_correct [of r] by simp
4.1721 +
4.1722 +lemma real_of_int_floor_add_one_ge [simp]: "r \<le> real(floor r) + 1"
4.1723 + unfolding real_of_int_def using floor_correct [of r] by simp
4.1724 +
4.1725 +lemma real_of_int_floor_add_one_gt [simp]: "r < real(floor r) + 1"
4.1726 + unfolding real_of_int_def using floor_correct [of r] by simp
4.1727 +
4.1728 +lemma le_floor: "real a <= x ==> a <= floor x"
4.1729 + unfolding real_of_int_def by (simp add: le_floor_iff)
4.1730 +
4.1731 +lemma real_le_floor: "a <= floor x ==> real a <= x"
4.1732 + unfolding real_of_int_def by (simp add: le_floor_iff)
4.1733 +
4.1734 +lemma le_floor_eq: "(a <= floor x) = (real a <= x)"
4.1735 + unfolding real_of_int_def by (rule le_floor_iff)
4.1736 +
4.1737 +lemma floor_less_eq: "(floor x < a) = (x < real a)"
4.1738 + unfolding real_of_int_def by (rule floor_less_iff)
4.1739 +
4.1740 +lemma less_floor_eq: "(a < floor x) = (real a + 1 <= x)"
4.1741 + unfolding real_of_int_def by (rule less_floor_iff)
4.1742 +
4.1743 +lemma floor_le_eq: "(floor x <= a) = (x < real a + 1)"
4.1744 + unfolding real_of_int_def by (rule floor_le_iff)
4.1745 +
4.1746 +lemma floor_add [simp]: "floor (x + real a) = floor x + a"
4.1747 + unfolding real_of_int_def by (rule floor_add_of_int)
4.1748 +
4.1749 +lemma floor_subtract [simp]: "floor (x - real a) = floor x - a"
4.1750 + unfolding real_of_int_def by (rule floor_diff_of_int)
4.1751 +
4.1752 +lemma le_mult_floor:
4.1753 + assumes "0 \<le> (a :: real)" and "0 \<le> b"
4.1754 + shows "floor a * floor b \<le> floor (a * b)"
4.1755 +proof -
4.1756 + have "real (floor a) \<le> a"
4.1757 + and "real (floor b) \<le> b" by auto
4.1758 + hence "real (floor a * floor b) \<le> a * b"
4.1759 + using assms by (auto intro!: mult_mono)
4.1760 + also have "a * b < real (floor (a * b) + 1)" by auto
4.1761 + finally show ?thesis unfolding real_of_int_less_iff by simp
4.1762 +qed
4.1763 +
4.1764 +lemma floor_divide_eq_div:
4.1765 + "floor (real a / real b) = a div b"
4.1766 +proof cases
4.1767 + assume "b \<noteq> 0 \<or> b dvd a"
4.1768 + with real_of_int_div3[of a b] show ?thesis
4.1769 + by (auto simp: real_of_int_div[symmetric] intro!: floor_eq2 real_of_int_div4 neq_le_trans)
4.1770 + (metis add_left_cancel zero_neq_one real_of_int_div_aux real_of_int_inject
4.1771 + real_of_int_zero_cancel right_inverse_eq div_self mod_div_trivial)
4.1772 +qed (auto simp: real_of_int_div)
4.1773 +
4.1774 +lemma ceiling_real_of_nat [simp]: "ceiling (real (n::nat)) = int n"
4.1775 + unfolding real_of_nat_def by simp
4.1776 +
4.1777 +lemma real_of_int_ceiling_ge [simp]: "r \<le> real (ceiling r)"
4.1778 + unfolding real_of_int_def by (rule le_of_int_ceiling)
4.1779 +
4.1780 +lemma ceiling_real_of_int [simp]: "ceiling (real (n::int)) = n"
4.1781 + unfolding real_of_int_def by simp
4.1782 +
4.1783 +lemma real_of_int_ceiling_cancel [simp]:
4.1784 + "(real (ceiling x) = x) = (\<exists>n::int. x = real n)"
4.1785 + using ceiling_real_of_int by metis
4.1786 +
4.1787 +lemma ceiling_eq: "[| real n < x; x < real n + 1 |] ==> ceiling x = n + 1"
4.1788 + unfolding real_of_int_def using ceiling_unique [of "n + 1" x] by simp
4.1789 +
4.1790 +lemma ceiling_eq2: "[| real n < x; x \<le> real n + 1 |] ==> ceiling x = n + 1"
4.1791 + unfolding real_of_int_def using ceiling_unique [of "n + 1" x] by simp
4.1792 +
4.1793 +lemma ceiling_eq3: "[| real n - 1 < x; x \<le> real n |] ==> ceiling x = n"
4.1794 + unfolding real_of_int_def using ceiling_unique [of n x] by simp
4.1795 +
4.1796 +lemma real_of_int_ceiling_diff_one_le [simp]: "real (ceiling r) - 1 \<le> r"
4.1797 + unfolding real_of_int_def using ceiling_correct [of r] by simp
4.1798 +
4.1799 +lemma real_of_int_ceiling_le_add_one [simp]: "real (ceiling r) \<le> r + 1"
4.1800 + unfolding real_of_int_def using ceiling_correct [of r] by simp
4.1801 +
4.1802 +lemma ceiling_le: "x <= real a ==> ceiling x <= a"
4.1803 + unfolding real_of_int_def by (simp add: ceiling_le_iff)
4.1804 +
4.1805 +lemma ceiling_le_real: "ceiling x <= a ==> x <= real a"
4.1806 + unfolding real_of_int_def by (simp add: ceiling_le_iff)
4.1807 +
4.1808 +lemma ceiling_le_eq: "(ceiling x <= a) = (x <= real a)"
4.1809 + unfolding real_of_int_def by (rule ceiling_le_iff)
4.1810 +
4.1811 +lemma less_ceiling_eq: "(a < ceiling x) = (real a < x)"
4.1812 + unfolding real_of_int_def by (rule less_ceiling_iff)
4.1813 +
4.1814 +lemma ceiling_less_eq: "(ceiling x < a) = (x <= real a - 1)"
4.1815 + unfolding real_of_int_def by (rule ceiling_less_iff)
4.1816 +
4.1817 +lemma le_ceiling_eq: "(a <= ceiling x) = (real a - 1 < x)"
4.1818 + unfolding real_of_int_def by (rule le_ceiling_iff)
4.1819 +
4.1820 +lemma ceiling_add [simp]: "ceiling (x + real a) = ceiling x + a"
4.1821 + unfolding real_of_int_def by (rule ceiling_add_of_int)
4.1822 +
4.1823 +lemma ceiling_subtract [simp]: "ceiling (x - real a) = ceiling x - a"
4.1824 + unfolding real_of_int_def by (rule ceiling_diff_of_int)
4.1825 +
4.1826 +
4.1827 +subsubsection {* Versions for the natural numbers *}
4.1828 +
4.1829 +definition
4.1830 + natfloor :: "real => nat" where
4.1831 + "natfloor x = nat(floor x)"
4.1832 +
4.1833 +definition
4.1834 + natceiling :: "real => nat" where
4.1835 + "natceiling x = nat(ceiling x)"
4.1836 +
4.1837 +lemma natfloor_zero [simp]: "natfloor 0 = 0"
4.1838 + by (unfold natfloor_def, simp)
4.1839 +
4.1840 +lemma natfloor_one [simp]: "natfloor 1 = 1"
4.1841 + by (unfold natfloor_def, simp)
4.1842 +
4.1843 +lemma zero_le_natfloor [simp]: "0 <= natfloor x"
4.1844 + by (unfold natfloor_def, simp)
4.1845 +
4.1846 +lemma natfloor_numeral_eq [simp]: "natfloor (numeral n) = numeral n"
4.1847 + by (unfold natfloor_def, simp)
4.1848 +
4.1849 +lemma natfloor_real_of_nat [simp]: "natfloor(real n) = n"
4.1850 + by (unfold natfloor_def, simp)
4.1851 +
4.1852 +lemma real_natfloor_le: "0 <= x ==> real(natfloor x) <= x"
4.1853 + by (unfold natfloor_def, simp)
4.1854 +
4.1855 +lemma natfloor_neg: "x <= 0 ==> natfloor x = 0"
4.1856 + unfolding natfloor_def by simp
4.1857 +
4.1858 +lemma natfloor_mono: "x <= y ==> natfloor x <= natfloor y"
4.1859 + unfolding natfloor_def by (intro nat_mono floor_mono)
4.1860 +
4.1861 +lemma le_natfloor: "real x <= a ==> x <= natfloor a"
4.1862 + apply (unfold natfloor_def)
4.1863 + apply (subst nat_int [THEN sym])
4.1864 + apply (rule nat_mono)
4.1865 + apply (rule le_floor)
4.1866 + apply simp
4.1867 +done
4.1868 +
4.1869 +lemma natfloor_less_iff: "0 \<le> x \<Longrightarrow> natfloor x < n \<longleftrightarrow> x < real n"
4.1870 + unfolding natfloor_def real_of_nat_def
4.1871 + by (simp add: nat_less_iff floor_less_iff)
4.1872 +
4.1873 +lemma less_natfloor:
4.1874 + assumes "0 \<le> x" and "x < real (n :: nat)"
4.1875 + shows "natfloor x < n"
4.1876 + using assms by (simp add: natfloor_less_iff)
4.1877 +
4.1878 +lemma le_natfloor_eq: "0 <= x ==> (a <= natfloor x) = (real a <= x)"
4.1879 + apply (rule iffI)
4.1880 + apply (rule order_trans)
4.1881 + prefer 2
4.1882 + apply (erule real_natfloor_le)
4.1883 + apply (subst real_of_nat_le_iff)
4.1884 + apply assumption
4.1885 + apply (erule le_natfloor)
4.1886 +done
4.1887 +
4.1888 +lemma le_natfloor_eq_numeral [simp]:
4.1889 + "~ neg((numeral n)::int) ==> 0 <= x ==>
4.1890 + (numeral n <= natfloor x) = (numeral n <= x)"
4.1891 + apply (subst le_natfloor_eq, assumption)
4.1892 + apply simp
4.1893 +done
4.1894 +
4.1895 +lemma le_natfloor_eq_one [simp]: "(1 <= natfloor x) = (1 <= x)"
4.1896 + apply (case_tac "0 <= x")
4.1897 + apply (subst le_natfloor_eq, assumption, simp)
4.1898 + apply (rule iffI)
4.1899 + apply (subgoal_tac "natfloor x <= natfloor 0")
4.1900 + apply simp
4.1901 + apply (rule natfloor_mono)
4.1902 + apply simp
4.1903 + apply simp
4.1904 +done
4.1905 +
4.1906 +lemma natfloor_eq: "real n <= x ==> x < real n + 1 ==> natfloor x = n"
4.1907 + unfolding natfloor_def by (simp add: floor_eq2 [where n="int n"])
4.1908 +
4.1909 +lemma real_natfloor_add_one_gt: "x < real(natfloor x) + 1"
4.1910 + apply (case_tac "0 <= x")
4.1911 + apply (unfold natfloor_def)
4.1912 + apply simp
4.1913 + apply simp_all
4.1914 +done
4.1915 +
4.1916 +lemma real_natfloor_gt_diff_one: "x - 1 < real(natfloor x)"
4.1917 +using real_natfloor_add_one_gt by (simp add: algebra_simps)
4.1918 +
4.1919 +lemma ge_natfloor_plus_one_imp_gt: "natfloor z + 1 <= n ==> z < real n"
4.1920 + apply (subgoal_tac "z < real(natfloor z) + 1")
4.1921 + apply arith
4.1922 + apply (rule real_natfloor_add_one_gt)
4.1923 +done
4.1924 +
4.1925 +lemma natfloor_add [simp]: "0 <= x ==> natfloor (x + real a) = natfloor x + a"
4.1926 + unfolding natfloor_def
4.1927 + unfolding real_of_int_of_nat_eq [symmetric] floor_add
4.1928 + by (simp add: nat_add_distrib)
4.1929 +
4.1930 +lemma natfloor_add_numeral [simp]:
4.1931 + "~neg ((numeral n)::int) ==> 0 <= x ==>
4.1932 + natfloor (x + numeral n) = natfloor x + numeral n"
4.1933 + by (simp add: natfloor_add [symmetric])
4.1934 +
4.1935 +lemma natfloor_add_one: "0 <= x ==> natfloor(x + 1) = natfloor x + 1"
4.1936 + by (simp add: natfloor_add [symmetric] del: One_nat_def)
4.1937 +
4.1938 +lemma natfloor_subtract [simp]:
4.1939 + "natfloor(x - real a) = natfloor x - a"
4.1940 + unfolding natfloor_def real_of_int_of_nat_eq [symmetric] floor_subtract
4.1941 + by simp
4.1942 +
4.1943 +lemma natfloor_div_nat:
4.1944 + assumes "1 <= x" and "y > 0"
4.1945 + shows "natfloor (x / real y) = natfloor x div y"
4.1946 +proof (rule natfloor_eq)
4.1947 + have "(natfloor x) div y * y \<le> natfloor x"
4.1948 + by (rule add_leD1 [where k="natfloor x mod y"], simp)
4.1949 + thus "real (natfloor x div y) \<le> x / real y"
4.1950 + using assms by (simp add: le_divide_eq le_natfloor_eq)
4.1951 + have "natfloor x < (natfloor x) div y * y + y"
4.1952 + apply (subst mod_div_equality [symmetric])
4.1953 + apply (rule add_strict_left_mono)
4.1954 + apply (rule mod_less_divisor)
4.1955 + apply fact
4.1956 + done
4.1957 + thus "x / real y < real (natfloor x div y) + 1"
4.1958 + using assms
4.1959 + by (simp add: divide_less_eq natfloor_less_iff distrib_right)
4.1960 +qed
4.1961 +
4.1962 +lemma le_mult_natfloor:
4.1963 + shows "natfloor a * natfloor b \<le> natfloor (a * b)"
4.1964 + by (cases "0 <= a & 0 <= b")
4.1965 + (auto simp add: le_natfloor_eq mult_nonneg_nonneg mult_mono' real_natfloor_le natfloor_neg)
4.1966 +
4.1967 +lemma natceiling_zero [simp]: "natceiling 0 = 0"
4.1968 + by (unfold natceiling_def, simp)
4.1969 +
4.1970 +lemma natceiling_one [simp]: "natceiling 1 = 1"
4.1971 + by (unfold natceiling_def, simp)
4.1972 +
4.1973 +lemma zero_le_natceiling [simp]: "0 <= natceiling x"
4.1974 + by (unfold natceiling_def, simp)
4.1975 +
4.1976 +lemma natceiling_numeral_eq [simp]: "natceiling (numeral n) = numeral n"
4.1977 + by (unfold natceiling_def, simp)
4.1978 +
4.1979 +lemma natceiling_real_of_nat [simp]: "natceiling(real n) = n"
4.1980 + by (unfold natceiling_def, simp)
4.1981 +
4.1982 +lemma real_natceiling_ge: "x <= real(natceiling x)"
4.1983 + unfolding natceiling_def by (cases "x < 0", simp_all)
4.1984 +
4.1985 +lemma natceiling_neg: "x <= 0 ==> natceiling x = 0"
4.1986 + unfolding natceiling_def by simp
4.1987 +
4.1988 +lemma natceiling_mono: "x <= y ==> natceiling x <= natceiling y"
4.1989 + unfolding natceiling_def by (intro nat_mono ceiling_mono)
4.1990 +
4.1991 +lemma natceiling_le: "x <= real a ==> natceiling x <= a"
4.1992 + unfolding natceiling_def real_of_nat_def
4.1993 + by (simp add: nat_le_iff ceiling_le_iff)
4.1994 +
4.1995 +lemma natceiling_le_eq: "(natceiling x <= a) = (x <= real a)"
4.1996 + unfolding natceiling_def real_of_nat_def
4.1997 + by (simp add: nat_le_iff ceiling_le_iff)
4.1998 +
4.1999 +lemma natceiling_le_eq_numeral [simp]:
4.2000 + "~ neg((numeral n)::int) ==>
4.2001 + (natceiling x <= numeral n) = (x <= numeral n)"
4.2002 + by (simp add: natceiling_le_eq)
4.2003 +
4.2004 +lemma natceiling_le_eq_one: "(natceiling x <= 1) = (x <= 1)"
4.2005 + unfolding natceiling_def
4.2006 + by (simp add: nat_le_iff ceiling_le_iff)
4.2007 +
4.2008 +lemma natceiling_eq: "real n < x ==> x <= real n + 1 ==> natceiling x = n + 1"
4.2009 + unfolding natceiling_def
4.2010 + by (simp add: ceiling_eq2 [where n="int n"])
4.2011 +
4.2012 +lemma natceiling_add [simp]: "0 <= x ==>
4.2013 + natceiling (x + real a) = natceiling x + a"
4.2014 + unfolding natceiling_def
4.2015 + unfolding real_of_int_of_nat_eq [symmetric] ceiling_add
4.2016 + by (simp add: nat_add_distrib)
4.2017 +
4.2018 +lemma natceiling_add_numeral [simp]:
4.2019 + "~ neg ((numeral n)::int) ==> 0 <= x ==>
4.2020 + natceiling (x + numeral n) = natceiling x + numeral n"
4.2021 + by (simp add: natceiling_add [symmetric])
4.2022 +
4.2023 +lemma natceiling_add_one: "0 <= x ==> natceiling(x + 1) = natceiling x + 1"
4.2024 + by (simp add: natceiling_add [symmetric] del: One_nat_def)
4.2025 +
4.2026 +lemma natceiling_subtract [simp]: "natceiling(x - real a) = natceiling x - a"
4.2027 + unfolding natceiling_def real_of_int_of_nat_eq [symmetric] ceiling_subtract
4.2028 + by simp
4.2029 +
4.2030 +subsection {* Exponentiation with floor *}
4.2031 +
4.2032 +lemma floor_power:
4.2033 + assumes "x = real (floor x)"
4.2034 + shows "floor (x ^ n) = floor x ^ n"
4.2035 +proof -
4.2036 + have *: "x ^ n = real (floor x ^ n)"
4.2037 + using assms by (induct n arbitrary: x) simp_all
4.2038 + show ?thesis unfolding real_of_int_inject[symmetric]
4.2039 + unfolding * floor_real_of_int ..
4.2040 +qed
4.2041 +
4.2042 +lemma natfloor_power:
4.2043 + assumes "x = real (natfloor x)"
4.2044 + shows "natfloor (x ^ n) = natfloor x ^ n"
4.2045 +proof -
4.2046 + from assms have "0 \<le> floor x" by auto
4.2047 + note assms[unfolded natfloor_def real_nat_eq_real[OF `0 \<le> floor x`]]
4.2048 + from floor_power[OF this]
4.2049 + show ?thesis unfolding natfloor_def nat_power_eq[OF `0 \<le> floor x`, symmetric]
4.2050 + by simp
4.2051 +qed
4.2052 +
4.2053 +
4.2054 +subsection {* Implementation of rational real numbers *}
4.2055 +
4.2056 +text {* Formal constructor *}
4.2057 +
4.2058 +definition Ratreal :: "rat \<Rightarrow> real" where
4.2059 + [code_abbrev, simp]: "Ratreal = of_rat"
4.2060 +
4.2061 +code_datatype Ratreal
4.2062 +
4.2063 +
4.2064 +text {* Numerals *}
4.2065 +
4.2066 +lemma [code_abbrev]:
4.2067 + "(of_rat (of_int a) :: real) = of_int a"
4.2068 + by simp
4.2069 +
4.2070 +lemma [code_abbrev]:
4.2071 + "(of_rat 0 :: real) = 0"
4.2072 + by simp
4.2073 +
4.2074 +lemma [code_abbrev]:
4.2075 + "(of_rat 1 :: real) = 1"
4.2076 + by simp
4.2077 +
4.2078 +lemma [code_abbrev]:
4.2079 + "(of_rat (numeral k) :: real) = numeral k"
4.2080 + by simp
4.2081 +
4.2082 +lemma [code_abbrev]:
4.2083 + "(of_rat (neg_numeral k) :: real) = neg_numeral k"
4.2084 + by simp
4.2085 +
4.2086 +lemma [code_post]:
4.2087 + "(of_rat (0 / r) :: real) = 0"
4.2088 + "(of_rat (r / 0) :: real) = 0"
4.2089 + "(of_rat (1 / 1) :: real) = 1"
4.2090 + "(of_rat (numeral k / 1) :: real) = numeral k"
4.2091 + "(of_rat (neg_numeral k / 1) :: real) = neg_numeral k"
4.2092 + "(of_rat (1 / numeral k) :: real) = 1 / numeral k"
4.2093 + "(of_rat (1 / neg_numeral k) :: real) = 1 / neg_numeral k"
4.2094 + "(of_rat (numeral k / numeral l) :: real) = numeral k / numeral l"
4.2095 + "(of_rat (numeral k / neg_numeral l) :: real) = numeral k / neg_numeral l"
4.2096 + "(of_rat (neg_numeral k / numeral l) :: real) = neg_numeral k / numeral l"
4.2097 + "(of_rat (neg_numeral k / neg_numeral l) :: real) = neg_numeral k / neg_numeral l"
4.2098 + by (simp_all add: of_rat_divide)
4.2099 +
4.2100 +
4.2101 +text {* Operations *}
4.2102 +
4.2103 +lemma zero_real_code [code]:
4.2104 + "0 = Ratreal 0"
4.2105 +by simp
4.2106 +
4.2107 +lemma one_real_code [code]:
4.2108 + "1 = Ratreal 1"
4.2109 +by simp
4.2110 +
4.2111 +instantiation real :: equal
4.2112 +begin
4.2113 +
4.2114 +definition "HOL.equal (x\<Colon>real) y \<longleftrightarrow> x - y = 0"
4.2115 +
4.2116 +instance proof
4.2117 +qed (simp add: equal_real_def)
4.2118 +
4.2119 +lemma real_equal_code [code]:
4.2120 + "HOL.equal (Ratreal x) (Ratreal y) \<longleftrightarrow> HOL.equal x y"
4.2121 + by (simp add: equal_real_def equal)
4.2122 +
4.2123 +lemma [code nbe]:
4.2124 + "HOL.equal (x::real) x \<longleftrightarrow> True"
4.2125 + by (rule equal_refl)
4.2126 +
4.2127 +end
4.2128 +
4.2129 +lemma real_less_eq_code [code]: "Ratreal x \<le> Ratreal y \<longleftrightarrow> x \<le> y"
4.2130 + by (simp add: of_rat_less_eq)
4.2131 +
4.2132 +lemma real_less_code [code]: "Ratreal x < Ratreal y \<longleftrightarrow> x < y"
4.2133 + by (simp add: of_rat_less)
4.2134 +
4.2135 +lemma real_plus_code [code]: "Ratreal x + Ratreal y = Ratreal (x + y)"
4.2136 + by (simp add: of_rat_add)
4.2137 +
4.2138 +lemma real_times_code [code]: "Ratreal x * Ratreal y = Ratreal (x * y)"
4.2139 + by (simp add: of_rat_mult)
4.2140 +
4.2141 +lemma real_uminus_code [code]: "- Ratreal x = Ratreal (- x)"
4.2142 + by (simp add: of_rat_minus)
4.2143 +
4.2144 +lemma real_minus_code [code]: "Ratreal x - Ratreal y = Ratreal (x - y)"
4.2145 + by (simp add: of_rat_diff)
4.2146 +
4.2147 +lemma real_inverse_code [code]: "inverse (Ratreal x) = Ratreal (inverse x)"
4.2148 + by (simp add: of_rat_inverse)
4.2149 +
4.2150 +lemma real_divide_code [code]: "Ratreal x / Ratreal y = Ratreal (x / y)"
4.2151 + by (simp add: of_rat_divide)
4.2152 +
4.2153 +lemma real_floor_code [code]: "floor (Ratreal x) = floor x"
4.2154 + 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)
4.2155 +
4.2156 +
4.2157 +text {* Quickcheck *}
4.2158 +
4.2159 +definition (in term_syntax)
4.2160 + valterm_ratreal :: "rat \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow> real \<times> (unit \<Rightarrow> Code_Evaluation.term)" where
4.2161 + [code_unfold]: "valterm_ratreal k = Code_Evaluation.valtermify Ratreal {\<cdot>} k"
4.2162 +
4.2163 +notation fcomp (infixl "\<circ>>" 60)
4.2164 +notation scomp (infixl "\<circ>\<rightarrow>" 60)
4.2165 +
4.2166 +instantiation real :: random
4.2167 +begin
4.2168 +
4.2169 +definition
4.2170 + "Quickcheck_Random.random i = Quickcheck_Random.random i \<circ>\<rightarrow> (\<lambda>r. Pair (valterm_ratreal r))"
4.2171 +
4.2172 +instance ..
4.2173 +
4.2174 +end
4.2175 +
4.2176 +no_notation fcomp (infixl "\<circ>>" 60)
4.2177 +no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
4.2178 +
4.2179 +instantiation real :: exhaustive
4.2180 +begin
4.2181 +
4.2182 +definition
4.2183 + "exhaustive_real f d = Quickcheck_Exhaustive.exhaustive (%r. f (Ratreal r)) d"
4.2184 +
4.2185 +instance ..
4.2186 +
4.2187 +end
4.2188 +
4.2189 +instantiation real :: full_exhaustive
4.2190 +begin
4.2191 +
4.2192 +definition
4.2193 + "full_exhaustive_real f d = Quickcheck_Exhaustive.full_exhaustive (%r. f (valterm_ratreal r)) d"
4.2194 +
4.2195 +instance ..
4.2196 +
4.2197 +end
4.2198 +
4.2199 +instantiation real :: narrowing
4.2200 +begin
4.2201 +
4.2202 +definition
4.2203 + "narrowing = Quickcheck_Narrowing.apply (Quickcheck_Narrowing.cons Ratreal) narrowing"
4.2204 +
4.2205 +instance ..
4.2206 +
4.2207 +end
4.2208 +
4.2209 +
4.2210 +subsection {* Setup for Nitpick *}
4.2211 +
4.2212 +declaration {*
4.2213 + Nitpick_HOL.register_frac_type @{type_name real}
4.2214 + [(@{const_name zero_real_inst.zero_real}, @{const_name Nitpick.zero_frac}),
4.2215 + (@{const_name one_real_inst.one_real}, @{const_name Nitpick.one_frac}),
4.2216 + (@{const_name plus_real_inst.plus_real}, @{const_name Nitpick.plus_frac}),
4.2217 + (@{const_name times_real_inst.times_real}, @{const_name Nitpick.times_frac}),
4.2218 + (@{const_name uminus_real_inst.uminus_real}, @{const_name Nitpick.uminus_frac}),
4.2219 + (@{const_name inverse_real_inst.inverse_real}, @{const_name Nitpick.inverse_frac}),
4.2220 + (@{const_name ord_real_inst.less_real}, @{const_name Nitpick.less_frac}),
4.2221 + (@{const_name ord_real_inst.less_eq_real}, @{const_name Nitpick.less_eq_frac})]
4.2222 +*}
4.2223 +
4.2224 +lemmas [nitpick_unfold] = inverse_real_inst.inverse_real one_real_inst.one_real
4.2225 + ord_real_inst.less_real ord_real_inst.less_eq_real plus_real_inst.plus_real
4.2226 + times_real_inst.times_real uminus_real_inst.uminus_real
4.2227 + zero_real_inst.zero_real
4.2228 +
4.2229 +ML_file "Tools/SMT/smt_real.ML"
4.2230 +setup SMT_Real.setup
4.2231 +
4.2232 +end
5.1 --- a/src/HOL/RealDef.thy Tue Mar 26 12:20:56 2013 +0100
5.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
5.3 @@ -1,2229 +0,0 @@
5.4 -(* Title: HOL/RealDef.thy
5.5 - Author: Jacques D. Fleuriot, University of Edinburgh, 1998
5.6 - Author: Larry Paulson, University of Cambridge
5.7 - Author: Jeremy Avigad, Carnegie Mellon University
5.8 - Author: Florian Zuleger, Johannes Hoelzl, and Simon Funke, TU Muenchen
5.9 - Conversion to Isar and new proofs by Lawrence C Paulson, 2003/4
5.10 - Construction of Cauchy Reals by Brian Huffman, 2010
5.11 -*)
5.12 -
5.13 -header {* Development of the Reals using Cauchy Sequences *}
5.14 -
5.15 -theory RealDef
5.16 -imports Rat Conditional_Complete_Lattices
5.17 -begin
5.18 -
5.19 -text {*
5.20 - This theory contains a formalization of the real numbers as
5.21 - equivalence classes of Cauchy sequences of rationals. See
5.22 - @{file "~~/src/HOL/ex/Dedekind_Real.thy"} for an alternative
5.23 - construction using Dedekind cuts.
5.24 -*}
5.25 -
5.26 -subsection {* Preliminary lemmas *}
5.27 -
5.28 -lemma add_diff_add:
5.29 - fixes a b c d :: "'a::ab_group_add"
5.30 - shows "(a + c) - (b + d) = (a - b) + (c - d)"
5.31 - by simp
5.32 -
5.33 -lemma minus_diff_minus:
5.34 - fixes a b :: "'a::ab_group_add"
5.35 - shows "- a - - b = - (a - b)"
5.36 - by simp
5.37 -
5.38 -lemma mult_diff_mult:
5.39 - fixes x y a b :: "'a::ring"
5.40 - shows "(x * y - a * b) = x * (y - b) + (x - a) * b"
5.41 - by (simp add: algebra_simps)
5.42 -
5.43 -lemma inverse_diff_inverse:
5.44 - fixes a b :: "'a::division_ring"
5.45 - assumes "a \<noteq> 0" and "b \<noteq> 0"
5.46 - shows "inverse a - inverse b = - (inverse a * (a - b) * inverse b)"
5.47 - using assms by (simp add: algebra_simps)
5.48 -
5.49 -lemma obtain_pos_sum:
5.50 - fixes r :: rat assumes r: "0 < r"
5.51 - obtains s t where "0 < s" and "0 < t" and "r = s + t"
5.52 -proof
5.53 - from r show "0 < r/2" by simp
5.54 - from r show "0 < r/2" by simp
5.55 - show "r = r/2 + r/2" by simp
5.56 -qed
5.57 -
5.58 -subsection {* Sequences that converge to zero *}
5.59 -
5.60 -definition
5.61 - vanishes :: "(nat \<Rightarrow> rat) \<Rightarrow> bool"
5.62 -where
5.63 - "vanishes X = (\<forall>r>0. \<exists>k. \<forall>n\<ge>k. \<bar>X n\<bar> < r)"
5.64 -
5.65 -lemma vanishesI: "(\<And>r. 0 < r \<Longrightarrow> \<exists>k. \<forall>n\<ge>k. \<bar>X n\<bar> < r) \<Longrightarrow> vanishes X"
5.66 - unfolding vanishes_def by simp
5.67 -
5.68 -lemma vanishesD: "\<lbrakk>vanishes X; 0 < r\<rbrakk> \<Longrightarrow> \<exists>k. \<forall>n\<ge>k. \<bar>X n\<bar> < r"
5.69 - unfolding vanishes_def by simp
5.70 -
5.71 -lemma vanishes_const [simp]: "vanishes (\<lambda>n. c) \<longleftrightarrow> c = 0"
5.72 - unfolding vanishes_def
5.73 - apply (cases "c = 0", auto)
5.74 - apply (rule exI [where x="\<bar>c\<bar>"], auto)
5.75 - done
5.76 -
5.77 -lemma vanishes_minus: "vanishes X \<Longrightarrow> vanishes (\<lambda>n. - X n)"
5.78 - unfolding vanishes_def by simp
5.79 -
5.80 -lemma vanishes_add:
5.81 - assumes X: "vanishes X" and Y: "vanishes Y"
5.82 - shows "vanishes (\<lambda>n. X n + Y n)"
5.83 -proof (rule vanishesI)
5.84 - fix r :: rat assume "0 < r"
5.85 - then obtain s t where s: "0 < s" and t: "0 < t" and r: "r = s + t"
5.86 - by (rule obtain_pos_sum)
5.87 - obtain i where i: "\<forall>n\<ge>i. \<bar>X n\<bar> < s"
5.88 - using vanishesD [OF X s] ..
5.89 - obtain j where j: "\<forall>n\<ge>j. \<bar>Y n\<bar> < t"
5.90 - using vanishesD [OF Y t] ..
5.91 - have "\<forall>n\<ge>max i j. \<bar>X n + Y n\<bar> < r"
5.92 - proof (clarsimp)
5.93 - fix n assume n: "i \<le> n" "j \<le> n"
5.94 - have "\<bar>X n + Y n\<bar> \<le> \<bar>X n\<bar> + \<bar>Y n\<bar>" by (rule abs_triangle_ineq)
5.95 - also have "\<dots> < s + t" by (simp add: add_strict_mono i j n)
5.96 - finally show "\<bar>X n + Y n\<bar> < r" unfolding r .
5.97 - qed
5.98 - thus "\<exists>k. \<forall>n\<ge>k. \<bar>X n + Y n\<bar> < r" ..
5.99 -qed
5.100 -
5.101 -lemma vanishes_diff:
5.102 - assumes X: "vanishes X" and Y: "vanishes Y"
5.103 - shows "vanishes (\<lambda>n. X n - Y n)"
5.104 -unfolding diff_minus by (intro vanishes_add vanishes_minus X Y)
5.105 -
5.106 -lemma vanishes_mult_bounded:
5.107 - assumes X: "\<exists>a>0. \<forall>n. \<bar>X n\<bar> < a"
5.108 - assumes Y: "vanishes (\<lambda>n. Y n)"
5.109 - shows "vanishes (\<lambda>n. X n * Y n)"
5.110 -proof (rule vanishesI)
5.111 - fix r :: rat assume r: "0 < r"
5.112 - obtain a where a: "0 < a" "\<forall>n. \<bar>X n\<bar> < a"
5.113 - using X by fast
5.114 - obtain b where b: "0 < b" "r = a * b"
5.115 - proof
5.116 - show "0 < r / a" using r a by (simp add: divide_pos_pos)
5.117 - show "r = a * (r / a)" using a by simp
5.118 - qed
5.119 - obtain k where k: "\<forall>n\<ge>k. \<bar>Y n\<bar> < b"
5.120 - using vanishesD [OF Y b(1)] ..
5.121 - have "\<forall>n\<ge>k. \<bar>X n * Y n\<bar> < r"
5.122 - by (simp add: b(2) abs_mult mult_strict_mono' a k)
5.123 - thus "\<exists>k. \<forall>n\<ge>k. \<bar>X n * Y n\<bar> < r" ..
5.124 -qed
5.125 -
5.126 -subsection {* Cauchy sequences *}
5.127 -
5.128 -definition
5.129 - cauchy :: "(nat \<Rightarrow> rat) \<Rightarrow> bool"
5.130 -where
5.131 - "cauchy X \<longleftrightarrow> (\<forall>r>0. \<exists>k. \<forall>m\<ge>k. \<forall>n\<ge>k. \<bar>X m - X n\<bar> < r)"
5.132 -
5.133 -lemma cauchyI:
5.134 - "(\<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"
5.135 - unfolding cauchy_def by simp
5.136 -
5.137 -lemma cauchyD:
5.138 - "\<lbrakk>cauchy X; 0 < r\<rbrakk> \<Longrightarrow> \<exists>k. \<forall>m\<ge>k. \<forall>n\<ge>k. \<bar>X m - X n\<bar> < r"
5.139 - unfolding cauchy_def by simp
5.140 -
5.141 -lemma cauchy_const [simp]: "cauchy (\<lambda>n. x)"
5.142 - unfolding cauchy_def by simp
5.143 -
5.144 -lemma cauchy_add [simp]:
5.145 - assumes X: "cauchy X" and Y: "cauchy Y"
5.146 - shows "cauchy (\<lambda>n. X n + Y n)"
5.147 -proof (rule cauchyI)
5.148 - fix r :: rat assume "0 < r"
5.149 - then obtain s t where s: "0 < s" and t: "0 < t" and r: "r = s + t"
5.150 - by (rule obtain_pos_sum)
5.151 - obtain i where i: "\<forall>m\<ge>i. \<forall>n\<ge>i. \<bar>X m - X n\<bar> < s"
5.152 - using cauchyD [OF X s] ..
5.153 - obtain j where j: "\<forall>m\<ge>j. \<forall>n\<ge>j. \<bar>Y m - Y n\<bar> < t"
5.154 - using cauchyD [OF Y t] ..
5.155 - have "\<forall>m\<ge>max i j. \<forall>n\<ge>max i j. \<bar>(X m + Y m) - (X n + Y n)\<bar> < r"
5.156 - proof (clarsimp)
5.157 - fix m n assume *: "i \<le> m" "j \<le> m" "i \<le> n" "j \<le> n"
5.158 - have "\<bar>(X m + Y m) - (X n + Y n)\<bar> \<le> \<bar>X m - X n\<bar> + \<bar>Y m - Y n\<bar>"
5.159 - unfolding add_diff_add by (rule abs_triangle_ineq)
5.160 - also have "\<dots> < s + t"
5.161 - by (rule add_strict_mono, simp_all add: i j *)
5.162 - finally show "\<bar>(X m + Y m) - (X n + Y n)\<bar> < r" unfolding r .
5.163 - qed
5.164 - thus "\<exists>k. \<forall>m\<ge>k. \<forall>n\<ge>k. \<bar>(X m + Y m) - (X n + Y n)\<bar> < r" ..
5.165 -qed
5.166 -
5.167 -lemma cauchy_minus [simp]:
5.168 - assumes X: "cauchy X"
5.169 - shows "cauchy (\<lambda>n. - X n)"
5.170 -using assms unfolding cauchy_def
5.171 -unfolding minus_diff_minus abs_minus_cancel .
5.172 -
5.173 -lemma cauchy_diff [simp]:
5.174 - assumes X: "cauchy X" and Y: "cauchy Y"
5.175 - shows "cauchy (\<lambda>n. X n - Y n)"
5.176 -using assms unfolding diff_minus by simp
5.177 -
5.178 -lemma cauchy_imp_bounded:
5.179 - assumes "cauchy X" shows "\<exists>b>0. \<forall>n. \<bar>X n\<bar> < b"
5.180 -proof -
5.181 - obtain k where k: "\<forall>m\<ge>k. \<forall>n\<ge>k. \<bar>X m - X n\<bar> < 1"
5.182 - using cauchyD [OF assms zero_less_one] ..
5.183 - show "\<exists>b>0. \<forall>n. \<bar>X n\<bar> < b"
5.184 - proof (intro exI conjI allI)
5.185 - have "0 \<le> \<bar>X 0\<bar>" by simp
5.186 - also have "\<bar>X 0\<bar> \<le> Max (abs ` X ` {..k})" by simp
5.187 - finally have "0 \<le> Max (abs ` X ` {..k})" .
5.188 - thus "0 < Max (abs ` X ` {..k}) + 1" by simp
5.189 - next
5.190 - fix n :: nat
5.191 - show "\<bar>X n\<bar> < Max (abs ` X ` {..k}) + 1"
5.192 - proof (rule linorder_le_cases)
5.193 - assume "n \<le> k"
5.194 - hence "\<bar>X n\<bar> \<le> Max (abs ` X ` {..k})" by simp
5.195 - thus "\<bar>X n\<bar> < Max (abs ` X ` {..k}) + 1" by simp
5.196 - next
5.197 - assume "k \<le> n"
5.198 - have "\<bar>X n\<bar> = \<bar>X k + (X n - X k)\<bar>" by simp
5.199 - also have "\<bar>X k + (X n - X k)\<bar> \<le> \<bar>X k\<bar> + \<bar>X n - X k\<bar>"
5.200 - by (rule abs_triangle_ineq)
5.201 - also have "\<dots> < Max (abs ` X ` {..k}) + 1"
5.202 - by (rule add_le_less_mono, simp, simp add: k `k \<le> n`)
5.203 - finally show "\<bar>X n\<bar> < Max (abs ` X ` {..k}) + 1" .
5.204 - qed
5.205 - qed
5.206 -qed
5.207 -
5.208 -lemma cauchy_mult [simp]:
5.209 - assumes X: "cauchy X" and Y: "cauchy Y"
5.210 - shows "cauchy (\<lambda>n. X n * Y n)"
5.211 -proof (rule cauchyI)
5.212 - fix r :: rat assume "0 < r"
5.213 - then obtain u v where u: "0 < u" and v: "0 < v" and "r = u + v"
5.214 - by (rule obtain_pos_sum)
5.215 - obtain a where a: "0 < a" "\<forall>n. \<bar>X n\<bar> < a"
5.216 - using cauchy_imp_bounded [OF X] by fast
5.217 - obtain b where b: "0 < b" "\<forall>n. \<bar>Y n\<bar> < b"
5.218 - using cauchy_imp_bounded [OF Y] by fast
5.219 - obtain s t where s: "0 < s" and t: "0 < t" and r: "r = a * t + s * b"
5.220 - proof
5.221 - show "0 < v/b" using v b(1) by (rule divide_pos_pos)
5.222 - show "0 < u/a" using u a(1) by (rule divide_pos_pos)
5.223 - show "r = a * (u/a) + (v/b) * b"
5.224 - using a(1) b(1) `r = u + v` by simp
5.225 - qed
5.226 - obtain i where i: "\<forall>m\<ge>i. \<forall>n\<ge>i. \<bar>X m - X n\<bar> < s"
5.227 - using cauchyD [OF X s] ..
5.228 - obtain j where j: "\<forall>m\<ge>j. \<forall>n\<ge>j. \<bar>Y m - Y n\<bar> < t"
5.229 - using cauchyD [OF Y t] ..
5.230 - have "\<forall>m\<ge>max i j. \<forall>n\<ge>max i j. \<bar>X m * Y m - X n * Y n\<bar> < r"
5.231 - proof (clarsimp)
5.232 - fix m n assume *: "i \<le> m" "j \<le> m" "i \<le> n" "j \<le> n"
5.233 - 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>"
5.234 - unfolding mult_diff_mult ..
5.235 - also have "\<dots> \<le> \<bar>X m * (Y m - Y n)\<bar> + \<bar>(X m - X n) * Y n\<bar>"
5.236 - by (rule abs_triangle_ineq)
5.237 - also have "\<dots> = \<bar>X m\<bar> * \<bar>Y m - Y n\<bar> + \<bar>X m - X n\<bar> * \<bar>Y n\<bar>"
5.238 - unfolding abs_mult ..
5.239 - also have "\<dots> < a * t + s * b"
5.240 - by (simp_all add: add_strict_mono mult_strict_mono' a b i j *)
5.241 - finally show "\<bar>X m * Y m - X n * Y n\<bar> < r" unfolding r .
5.242 - qed
5.243 - thus "\<exists>k. \<forall>m\<ge>k. \<forall>n\<ge>k. \<bar>X m * Y m - X n * Y n\<bar> < r" ..
5.244 -qed
5.245 -
5.246 -lemma cauchy_not_vanishes_cases:
5.247 - assumes X: "cauchy X"
5.248 - assumes nz: "\<not> vanishes X"
5.249 - shows "\<exists>b>0. \<exists>k. (\<forall>n\<ge>k. b < - X n) \<or> (\<forall>n\<ge>k. b < X n)"
5.250 -proof -
5.251 - obtain r where "0 < r" and r: "\<forall>k. \<exists>n\<ge>k. r \<le> \<bar>X n\<bar>"
5.252 - using nz unfolding vanishes_def by (auto simp add: not_less)
5.253 - obtain s t where s: "0 < s" and t: "0 < t" and "r = s + t"
5.254 - using `0 < r` by (rule obtain_pos_sum)
5.255 - obtain i where i: "\<forall>m\<ge>i. \<forall>n\<ge>i. \<bar>X m - X n\<bar> < s"
5.256 - using cauchyD [OF X s] ..
5.257 - obtain k where "i \<le> k" and "r \<le> \<bar>X k\<bar>"
5.258 - using r by fast
5.259 - have k: "\<forall>n\<ge>k. \<bar>X n - X k\<bar> < s"
5.260 - using i `i \<le> k` by auto
5.261 - have "X k \<le> - r \<or> r \<le> X k"
5.262 - using `r \<le> \<bar>X k\<bar>` by auto
5.263 - hence "(\<forall>n\<ge>k. t < - X n) \<or> (\<forall>n\<ge>k. t < X n)"
5.264 - unfolding `r = s + t` using k by auto
5.265 - hence "\<exists>k. (\<forall>n\<ge>k. t < - X n) \<or> (\<forall>n\<ge>k. t < X n)" ..
5.266 - thus "\<exists>t>0. \<exists>k. (\<forall>n\<ge>k. t < - X n) \<or> (\<forall>n\<ge>k. t < X n)"
5.267 - using t by auto
5.268 -qed
5.269 -
5.270 -lemma cauchy_not_vanishes:
5.271 - assumes X: "cauchy X"
5.272 - assumes nz: "\<not> vanishes X"
5.273 - shows "\<exists>b>0. \<exists>k. \<forall>n\<ge>k. b < \<bar>X n\<bar>"
5.274 -using cauchy_not_vanishes_cases [OF assms]
5.275 -by clarify (rule exI, erule conjI, rule_tac x=k in exI, auto)
5.276 -
5.277 -lemma cauchy_inverse [simp]:
5.278 - assumes X: "cauchy X"
5.279 - assumes nz: "\<not> vanishes X"
5.280 - shows "cauchy (\<lambda>n. inverse (X n))"
5.281 -proof (rule cauchyI)
5.282 - fix r :: rat assume "0 < r"
5.283 - obtain b i where b: "0 < b" and i: "\<forall>n\<ge>i. b < \<bar>X n\<bar>"
5.284 - using cauchy_not_vanishes [OF X nz] by fast
5.285 - from b i have nz: "\<forall>n\<ge>i. X n \<noteq> 0" by auto
5.286 - obtain s where s: "0 < s" and r: "r = inverse b * s * inverse b"
5.287 - proof
5.288 - show "0 < b * r * b"
5.289 - by (simp add: `0 < r` b mult_pos_pos)
5.290 - show "r = inverse b * (b * r * b) * inverse b"
5.291 - using b by simp
5.292 - qed
5.293 - obtain j where j: "\<forall>m\<ge>j. \<forall>n\<ge>j. \<bar>X m - X n\<bar> < s"
5.294 - using cauchyD [OF X s] ..
5.295 - have "\<forall>m\<ge>max i j. \<forall>n\<ge>max i j. \<bar>inverse (X m) - inverse (X n)\<bar> < r"
5.296 - proof (clarsimp)
5.297 - fix m n assume *: "i \<le> m" "j \<le> m" "i \<le> n" "j \<le> n"
5.298 - have "\<bar>inverse (X m) - inverse (X n)\<bar> =
5.299 - inverse \<bar>X m\<bar> * \<bar>X m - X n\<bar> * inverse \<bar>X n\<bar>"
5.300 - by (simp add: inverse_diff_inverse nz * abs_mult)
5.301 - also have "\<dots> < inverse b * s * inverse b"
5.302 - by (simp add: mult_strict_mono less_imp_inverse_less
5.303 - mult_pos_pos i j b * s)
5.304 - finally show "\<bar>inverse (X m) - inverse (X n)\<bar> < r" unfolding r .
5.305 - qed
5.306 - thus "\<exists>k. \<forall>m\<ge>k. \<forall>n\<ge>k. \<bar>inverse (X m) - inverse (X n)\<bar> < r" ..
5.307 -qed
5.308 -
5.309 -lemma vanishes_diff_inverse:
5.310 - assumes X: "cauchy X" "\<not> vanishes X"
5.311 - assumes Y: "cauchy Y" "\<not> vanishes Y"
5.312 - assumes XY: "vanishes (\<lambda>n. X n - Y n)"
5.313 - shows "vanishes (\<lambda>n. inverse (X n) - inverse (Y n))"
5.314 -proof (rule vanishesI)
5.315 - fix r :: rat assume r: "0 < r"
5.316 - obtain a i where a: "0 < a" and i: "\<forall>n\<ge>i. a < \<bar>X n\<bar>"
5.317 - using cauchy_not_vanishes [OF X] by fast
5.318 - obtain b j where b: "0 < b" and j: "\<forall>n\<ge>j. b < \<bar>Y n\<bar>"
5.319 - using cauchy_not_vanishes [OF Y] by fast
5.320 - obtain s where s: "0 < s" and "inverse a * s * inverse b = r"
5.321 - proof
5.322 - show "0 < a * r * b"
5.323 - using a r b by (simp add: mult_pos_pos)
5.324 - show "inverse a * (a * r * b) * inverse b = r"
5.325 - using a r b by simp
5.326 - qed
5.327 - obtain k where k: "\<forall>n\<ge>k. \<bar>X n - Y n\<bar> < s"
5.328 - using vanishesD [OF XY s] ..
5.329 - have "\<forall>n\<ge>max (max i j) k. \<bar>inverse (X n) - inverse (Y n)\<bar> < r"
5.330 - proof (clarsimp)
5.331 - fix n assume n: "i \<le> n" "j \<le> n" "k \<le> n"
5.332 - have "X n \<noteq> 0" and "Y n \<noteq> 0"
5.333 - using i j a b n by auto
5.334 - hence "\<bar>inverse (X n) - inverse (Y n)\<bar> =
5.335 - inverse \<bar>X n\<bar> * \<bar>X n - Y n\<bar> * inverse \<bar>Y n\<bar>"
5.336 - by (simp add: inverse_diff_inverse abs_mult)
5.337 - also have "\<dots> < inverse a * s * inverse b"
5.338 - apply (intro mult_strict_mono' less_imp_inverse_less)
5.339 - apply (simp_all add: a b i j k n mult_nonneg_nonneg)
5.340 - done
5.341 - also note `inverse a * s * inverse b = r`
5.342 - finally show "\<bar>inverse (X n) - inverse (Y n)\<bar> < r" .
5.343 - qed
5.344 - thus "\<exists>k. \<forall>n\<ge>k. \<bar>inverse (X n) - inverse (Y n)\<bar> < r" ..
5.345 -qed
5.346 -
5.347 -subsection {* Equivalence relation on Cauchy sequences *}
5.348 -
5.349 -definition realrel :: "(nat \<Rightarrow> rat) \<Rightarrow> (nat \<Rightarrow> rat) \<Rightarrow> bool"
5.350 - where "realrel = (\<lambda>X Y. cauchy X \<and> cauchy Y \<and> vanishes (\<lambda>n. X n - Y n))"
5.351 -
5.352 -lemma realrelI [intro?]:
5.353 - assumes "cauchy X" and "cauchy Y" and "vanishes (\<lambda>n. X n - Y n)"
5.354 - shows "realrel X Y"
5.355 - using assms unfolding realrel_def by simp
5.356 -
5.357 -lemma realrel_refl: "cauchy X \<Longrightarrow> realrel X X"
5.358 - unfolding realrel_def by simp
5.359 -
5.360 -lemma symp_realrel: "symp realrel"
5.361 - unfolding realrel_def
5.362 - by (rule sympI, clarify, drule vanishes_minus, simp)
5.363 -
5.364 -lemma transp_realrel: "transp realrel"
5.365 - unfolding realrel_def
5.366 - apply (rule transpI, clarify)
5.367 - apply (drule (1) vanishes_add)
5.368 - apply (simp add: algebra_simps)
5.369 - done
5.370 -
5.371 -lemma part_equivp_realrel: "part_equivp realrel"
5.372 - by (fast intro: part_equivpI symp_realrel transp_realrel
5.373 - realrel_refl cauchy_const)
5.374 -
5.375 -subsection {* The field of real numbers *}
5.376 -
5.377 -quotient_type real = "nat \<Rightarrow> rat" / partial: realrel
5.378 - morphisms rep_real Real
5.379 - by (rule part_equivp_realrel)
5.380 -
5.381 -lemma cr_real_eq: "pcr_real = (\<lambda>x y. cauchy x \<and> Real x = y)"
5.382 - unfolding real.pcr_cr_eq cr_real_def realrel_def by auto
5.383 -
5.384 -lemma Real_induct [induct type: real]: (* TODO: generate automatically *)
5.385 - assumes "\<And>X. cauchy X \<Longrightarrow> P (Real X)" shows "P x"
5.386 -proof (induct x)
5.387 - case (1 X)
5.388 - hence "cauchy X" by (simp add: realrel_def)
5.389 - thus "P (Real X)" by (rule assms)
5.390 -qed
5.391 -
5.392 -lemma eq_Real:
5.393 - "cauchy X \<Longrightarrow> cauchy Y \<Longrightarrow> Real X = Real Y \<longleftrightarrow> vanishes (\<lambda>n. X n - Y n)"
5.394 - using real.rel_eq_transfer
5.395 - unfolding real.pcr_cr_eq cr_real_def fun_rel_def realrel_def by simp
5.396 -
5.397 -declare real.forall_transfer [transfer_rule del]
5.398 -
5.399 -lemma forall_real_transfer [transfer_rule]: (* TODO: generate automatically *)
5.400 - "(fun_rel (fun_rel pcr_real op =) op =)
5.401 - (transfer_bforall cauchy) transfer_forall"
5.402 - using real.forall_transfer
5.403 - by (simp add: realrel_def)
5.404 -
5.405 -instantiation real :: field_inverse_zero
5.406 -begin
5.407 -
5.408 -lift_definition zero_real :: "real" is "\<lambda>n. 0"
5.409 - by (simp add: realrel_refl)
5.410 -
5.411 -lift_definition one_real :: "real" is "\<lambda>n. 1"
5.412 - by (simp add: realrel_refl)
5.413 -
5.414 -lift_definition plus_real :: "real \<Rightarrow> real \<Rightarrow> real" is "\<lambda>X Y n. X n + Y n"
5.415 - unfolding realrel_def add_diff_add
5.416 - by (simp only: cauchy_add vanishes_add simp_thms)
5.417 -
5.418 -lift_definition uminus_real :: "real \<Rightarrow> real" is "\<lambda>X n. - X n"
5.419 - unfolding realrel_def minus_diff_minus
5.420 - by (simp only: cauchy_minus vanishes_minus simp_thms)
5.421 -
5.422 -lift_definition times_real :: "real \<Rightarrow> real \<Rightarrow> real" is "\<lambda>X Y n. X n * Y n"
5.423 - unfolding realrel_def mult_diff_mult
5.424 - by (subst (4) mult_commute, simp only: cauchy_mult vanishes_add
5.425 - vanishes_mult_bounded cauchy_imp_bounded simp_thms)
5.426 -
5.427 -lift_definition inverse_real :: "real \<Rightarrow> real"
5.428 - is "\<lambda>X. if vanishes X then (\<lambda>n. 0) else (\<lambda>n. inverse (X n))"
5.429 -proof -
5.430 - fix X Y assume "realrel X Y"
5.431 - hence X: "cauchy X" and Y: "cauchy Y" and XY: "vanishes (\<lambda>n. X n - Y n)"
5.432 - unfolding realrel_def by simp_all
5.433 - have "vanishes X \<longleftrightarrow> vanishes Y"
5.434 - proof
5.435 - assume "vanishes X"
5.436 - from vanishes_diff [OF this XY] show "vanishes Y" by simp
5.437 - next
5.438 - assume "vanishes Y"
5.439 - from vanishes_add [OF this XY] show "vanishes X" by simp
5.440 - qed
5.441 - thus "?thesis X Y"
5.442 - unfolding realrel_def
5.443 - by (simp add: vanishes_diff_inverse X Y XY)
5.444 -qed
5.445 -
5.446 -definition
5.447 - "x - y = (x::real) + - y"
5.448 -
5.449 -definition
5.450 - "x / y = (x::real) * inverse y"
5.451 -
5.452 -lemma add_Real:
5.453 - assumes X: "cauchy X" and Y: "cauchy Y"
5.454 - shows "Real X + Real Y = Real (\<lambda>n. X n + Y n)"
5.455 - using assms plus_real.transfer
5.456 - unfolding cr_real_eq fun_rel_def by simp
5.457 -
5.458 -lemma minus_Real:
5.459 - assumes X: "cauchy X"
5.460 - shows "- Real X = Real (\<lambda>n. - X n)"
5.461 - using assms uminus_real.transfer
5.462 - unfolding cr_real_eq fun_rel_def by simp
5.463 -
5.464 -lemma diff_Real:
5.465 - assumes X: "cauchy X" and Y: "cauchy Y"
5.466 - shows "Real X - Real Y = Real (\<lambda>n. X n - Y n)"
5.467 - unfolding minus_real_def diff_minus
5.468 - by (simp add: minus_Real add_Real X Y)
5.469 -
5.470 -lemma mult_Real:
5.471 - assumes X: "cauchy X" and Y: "cauchy Y"
5.472 - shows "Real X * Real Y = Real (\<lambda>n. X n * Y n)"
5.473 - using assms times_real.transfer
5.474 - unfolding cr_real_eq fun_rel_def by simp
5.475 -
5.476 -lemma inverse_Real:
5.477 - assumes X: "cauchy X"
5.478 - shows "inverse (Real X) =
5.479 - (if vanishes X then 0 else Real (\<lambda>n. inverse (X n)))"
5.480 - using assms inverse_real.transfer zero_real.transfer
5.481 - unfolding cr_real_eq fun_rel_def by (simp split: split_if_asm, metis)
5.482 -
5.483 -instance proof
5.484 - fix a b c :: real
5.485 - show "a + b = b + a"
5.486 - by transfer (simp add: add_ac realrel_def)
5.487 - show "(a + b) + c = a + (b + c)"
5.488 - by transfer (simp add: add_ac realrel_def)
5.489 - show "0 + a = a"
5.490 - by transfer (simp add: realrel_def)
5.491 - show "- a + a = 0"
5.492 - by transfer (simp add: realrel_def)
5.493 - show "a - b = a + - b"
5.494 - by (rule minus_real_def)
5.495 - show "(a * b) * c = a * (b * c)"
5.496 - by transfer (simp add: mult_ac realrel_def)
5.497 - show "a * b = b * a"
5.498 - by transfer (simp add: mult_ac realrel_def)
5.499 - show "1 * a = a"
5.500 - by transfer (simp add: mult_ac realrel_def)
5.501 - show "(a + b) * c = a * c + b * c"
5.502 - by transfer (simp add: distrib_right realrel_def)
5.503 - show "(0\<Colon>real) \<noteq> (1\<Colon>real)"
5.504 - by transfer (simp add: realrel_def)
5.505 - show "a \<noteq> 0 \<Longrightarrow> inverse a * a = 1"
5.506 - apply transfer
5.507 - apply (simp add: realrel_def)
5.508 - apply (rule vanishesI)
5.509 - apply (frule (1) cauchy_not_vanishes, clarify)
5.510 - apply (rule_tac x=k in exI, clarify)
5.511 - apply (drule_tac x=n in spec, simp)
5.512 - done
5.513 - show "a / b = a * inverse b"
5.514 - by (rule divide_real_def)
5.515 - show "inverse (0::real) = 0"
5.516 - by transfer (simp add: realrel_def)
5.517 -qed
5.518 -
5.519 -end
5.520 -
5.521 -subsection {* Positive reals *}
5.522 -
5.523 -lift_definition positive :: "real \<Rightarrow> bool"
5.524 - is "\<lambda>X. \<exists>r>0. \<exists>k. \<forall>n\<ge>k. r < X n"
5.525 -proof -
5.526 - { fix X Y
5.527 - assume "realrel X Y"
5.528 - hence XY: "vanishes (\<lambda>n. X n - Y n)"
5.529 - unfolding realrel_def by simp_all
5.530 - assume "\<exists>r>0. \<exists>k. \<forall>n\<ge>k. r < X n"
5.531 - then obtain r i where "0 < r" and i: "\<forall>n\<ge>i. r < X n"
5.532 - by fast
5.533 - obtain s t where s: "0 < s" and t: "0 < t" and r: "r = s + t"
5.534 - using `0 < r` by (rule obtain_pos_sum)
5.535 - obtain j where j: "\<forall>n\<ge>j. \<bar>X n - Y n\<bar> < s"
5.536 - using vanishesD [OF XY s] ..
5.537 - have "\<forall>n\<ge>max i j. t < Y n"
5.538 - proof (clarsimp)
5.539 - fix n assume n: "i \<le> n" "j \<le> n"
5.540 - have "\<bar>X n - Y n\<bar> < s" and "r < X n"
5.541 - using i j n by simp_all
5.542 - thus "t < Y n" unfolding r by simp
5.543 - qed
5.544 - hence "\<exists>r>0. \<exists>k. \<forall>n\<ge>k. r < Y n" using t by fast
5.545 - } note 1 = this
5.546 - fix X Y assume "realrel X Y"
5.547 - hence "realrel X Y" and "realrel Y X"
5.548 - using symp_realrel unfolding symp_def by auto
5.549 - thus "?thesis X Y"
5.550 - by (safe elim!: 1)
5.551 -qed
5.552 -
5.553 -lemma positive_Real:
5.554 - assumes X: "cauchy X"
5.555 - shows "positive (Real X) \<longleftrightarrow> (\<exists>r>0. \<exists>k. \<forall>n\<ge>k. r < X n)"
5.556 - using assms positive.transfer
5.557 - unfolding cr_real_eq fun_rel_def by simp
5.558 -
5.559 -lemma positive_zero: "\<not> positive 0"
5.560 - by transfer auto
5.561 -
5.562 -lemma positive_add:
5.563 - "positive x \<Longrightarrow> positive y \<Longrightarrow> positive (x + y)"
5.564 -apply transfer
5.565 -apply (clarify, rename_tac a b i j)
5.566 -apply (rule_tac x="a + b" in exI, simp)
5.567 -apply (rule_tac x="max i j" in exI, clarsimp)
5.568 -apply (simp add: add_strict_mono)
5.569 -done
5.570 -
5.571 -lemma positive_mult:
5.572 - "positive x \<Longrightarrow> positive y \<Longrightarrow> positive (x * y)"
5.573 -apply transfer
5.574 -apply (clarify, rename_tac a b i j)
5.575 -apply (rule_tac x="a * b" in exI, simp add: mult_pos_pos)
5.576 -apply (rule_tac x="max i j" in exI, clarsimp)
5.577 -apply (rule mult_strict_mono, auto)
5.578 -done
5.579 -
5.580 -lemma positive_minus:
5.581 - "\<not> positive x \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> positive (- x)"
5.582 -apply transfer
5.583 -apply (simp add: realrel_def)
5.584 -apply (drule (1) cauchy_not_vanishes_cases, safe, fast, fast)
5.585 -done
5.586 -
5.587 -instantiation real :: linordered_field_inverse_zero
5.588 -begin
5.589 -
5.590 -definition
5.591 - "x < y \<longleftrightarrow> positive (y - x)"
5.592 -
5.593 -definition
5.594 - "x \<le> (y::real) \<longleftrightarrow> x < y \<or> x = y"
5.595 -
5.596 -definition
5.597 - "abs (a::real) = (if a < 0 then - a else a)"
5.598 -
5.599 -definition
5.600 - "sgn (a::real) = (if a = 0 then 0 else if 0 < a then 1 else - 1)"
5.601 -
5.602 -instance proof
5.603 - fix a b c :: real
5.604 - show "\<bar>a\<bar> = (if a < 0 then - a else a)"
5.605 - by (rule abs_real_def)
5.606 - show "a < b \<longleftrightarrow> a \<le> b \<and> \<not> b \<le> a"
5.607 - unfolding less_eq_real_def less_real_def
5.608 - by (auto, drule (1) positive_add, simp_all add: positive_zero)
5.609 - show "a \<le> a"
5.610 - unfolding less_eq_real_def by simp
5.611 - show "a \<le> b \<Longrightarrow> b \<le> c \<Longrightarrow> a \<le> c"
5.612 - unfolding less_eq_real_def less_real_def
5.613 - by (auto, drule (1) positive_add, simp add: algebra_simps)
5.614 - show "a \<le> b \<Longrightarrow> b \<le> a \<Longrightarrow> a = b"
5.615 - unfolding less_eq_real_def less_real_def
5.616 - by (auto, drule (1) positive_add, simp add: positive_zero)
5.617 - show "a \<le> b \<Longrightarrow> c + a \<le> c + b"
5.618 - unfolding less_eq_real_def less_real_def by (auto simp: diff_minus) (* by auto *)
5.619 - (* FIXME: Procedure int_combine_numerals: c + b - (c + a) \<equiv> b + - a *)
5.620 - (* Should produce c + b - (c + a) \<equiv> b - a *)
5.621 - show "sgn a = (if a = 0 then 0 else if 0 < a then 1 else - 1)"
5.622 - by (rule sgn_real_def)
5.623 - show "a \<le> b \<or> b \<le> a"
5.624 - unfolding less_eq_real_def less_real_def
5.625 - by (auto dest!: positive_minus)
5.626 - show "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b"
5.627 - unfolding less_real_def
5.628 - by (drule (1) positive_mult, simp add: algebra_simps)
5.629 -qed
5.630 -
5.631 -end
5.632 -
5.633 -instantiation real :: distrib_lattice
5.634 -begin
5.635 -
5.636 -definition
5.637 - "(inf :: real \<Rightarrow> real \<Rightarrow> real) = min"
5.638 -
5.639 -definition
5.640 - "(sup :: real \<Rightarrow> real \<Rightarrow> real) = max"
5.641 -
5.642 -instance proof
5.643 -qed (auto simp add: inf_real_def sup_real_def min_max.sup_inf_distrib1)
5.644 -
5.645 -end
5.646 -
5.647 -lemma of_nat_Real: "of_nat x = Real (\<lambda>n. of_nat x)"
5.648 -apply (induct x)
5.649 -apply (simp add: zero_real_def)
5.650 -apply (simp add: one_real_def add_Real)
5.651 -done
5.652 -
5.653 -lemma of_int_Real: "of_int x = Real (\<lambda>n. of_int x)"
5.654 -apply (cases x rule: int_diff_cases)
5.655 -apply (simp add: of_nat_Real diff_Real)
5.656 -done
5.657 -
5.658 -lemma of_rat_Real: "of_rat x = Real (\<lambda>n. x)"
5.659 -apply (induct x)
5.660 -apply (simp add: Fract_of_int_quotient of_rat_divide)
5.661 -apply (simp add: of_int_Real divide_inverse)
5.662 -apply (simp add: inverse_Real mult_Real)
5.663 -done
5.664 -
5.665 -instance real :: archimedean_field
5.666 -proof
5.667 - fix x :: real
5.668 - show "\<exists>z. x \<le> of_int z"
5.669 - apply (induct x)
5.670 - apply (frule cauchy_imp_bounded, clarify)
5.671 - apply (rule_tac x="ceiling b + 1" in exI)
5.672 - apply (rule less_imp_le)
5.673 - apply (simp add: of_int_Real less_real_def diff_Real positive_Real)
5.674 - apply (rule_tac x=1 in exI, simp add: algebra_simps)
5.675 - apply (rule_tac x=0 in exI, clarsimp)
5.676 - apply (rule le_less_trans [OF abs_ge_self])
5.677 - apply (rule less_le_trans [OF _ le_of_int_ceiling])
5.678 - apply simp
5.679 - done
5.680 -qed
5.681 -
5.682 -instantiation real :: floor_ceiling
5.683 -begin
5.684 -
5.685 -definition [code del]:
5.686 - "floor (x::real) = (THE z. of_int z \<le> x \<and> x < of_int (z + 1))"
5.687 -
5.688 -instance proof
5.689 - fix x :: real
5.690 - show "of_int (floor x) \<le> x \<and> x < of_int (floor x + 1)"
5.691 - unfolding floor_real_def using floor_exists1 by (rule theI')
5.692 -qed
5.693 -
5.694 -end
5.695 -
5.696 -subsection {* Completeness *}
5.697 -
5.698 -lemma not_positive_Real:
5.699 - assumes X: "cauchy X"
5.700 - shows "\<not> positive (Real X) \<longleftrightarrow> (\<forall>r>0. \<exists>k. \<forall>n\<ge>k. X n \<le> r)"
5.701 -unfolding positive_Real [OF X]
5.702 -apply (auto, unfold not_less)
5.703 -apply (erule obtain_pos_sum)
5.704 -apply (drule_tac x=s in spec, simp)
5.705 -apply (drule_tac r=t in cauchyD [OF X], clarify)
5.706 -apply (drule_tac x=k in spec, clarsimp)
5.707 -apply (rule_tac x=n in exI, clarify, rename_tac m)
5.708 -apply (drule_tac x=m in spec, simp)
5.709 -apply (drule_tac x=n in spec, simp)
5.710 -apply (drule spec, drule (1) mp, clarify, rename_tac i)
5.711 -apply (rule_tac x="max i k" in exI, simp)
5.712 -done
5.713 -
5.714 -lemma le_Real:
5.715 - assumes X: "cauchy X" and Y: "cauchy Y"
5.716 - shows "Real X \<le> Real Y = (\<forall>r>0. \<exists>k. \<forall>n\<ge>k. X n \<le> Y n + r)"
5.717 -unfolding not_less [symmetric, where 'a=real] less_real_def
5.718 -apply (simp add: diff_Real not_positive_Real X Y)
5.719 -apply (simp add: diff_le_eq add_ac)
5.720 -done
5.721 -
5.722 -lemma le_RealI:
5.723 - assumes Y: "cauchy Y"
5.724 - shows "\<forall>n. x \<le> of_rat (Y n) \<Longrightarrow> x \<le> Real Y"
5.725 -proof (induct x)
5.726 - fix X assume X: "cauchy X" and "\<forall>n. Real X \<le> of_rat (Y n)"
5.727 - hence le: "\<And>m r. 0 < r \<Longrightarrow> \<exists>k. \<forall>n\<ge>k. X n \<le> Y m + r"
5.728 - by (simp add: of_rat_Real le_Real)
5.729 - {
5.730 - fix r :: rat assume "0 < r"
5.731 - then obtain s t where s: "0 < s" and t: "0 < t" and r: "r = s + t"
5.732 - by (rule obtain_pos_sum)
5.733 - obtain i where i: "\<forall>m\<ge>i. \<forall>n\<ge>i. \<bar>Y m - Y n\<bar> < s"
5.734 - using cauchyD [OF Y s] ..
5.735 - obtain j where j: "\<forall>n\<ge>j. X n \<le> Y i + t"
5.736 - using le [OF t] ..
5.737 - have "\<forall>n\<ge>max i j. X n \<le> Y n + r"
5.738 - proof (clarsimp)
5.739 - fix n assume n: "i \<le> n" "j \<le> n"
5.740 - have "X n \<le> Y i + t" using n j by simp
5.741 - moreover have "\<bar>Y i - Y n\<bar> < s" using n i by simp
5.742 - ultimately show "X n \<le> Y n + r" unfolding r by simp
5.743 - qed
5.744 - hence "\<exists>k. \<forall>n\<ge>k. X n \<le> Y n + r" ..
5.745 - }
5.746 - thus "Real X \<le> Real Y"
5.747 - by (simp add: of_rat_Real le_Real X Y)
5.748 -qed
5.749 -
5.750 -lemma Real_leI:
5.751 - assumes X: "cauchy X"
5.752 - assumes le: "\<forall>n. of_rat (X n) \<le> y"
5.753 - shows "Real X \<le> y"
5.754 -proof -
5.755 - have "- y \<le> - Real X"
5.756 - by (simp add: minus_Real X le_RealI of_rat_minus le)
5.757 - thus ?thesis by simp
5.758 -qed
5.759 -
5.760 -lemma less_RealD:
5.761 - assumes Y: "cauchy Y"
5.762 - shows "x < Real Y \<Longrightarrow> \<exists>n. x < of_rat (Y n)"
5.763 -by (erule contrapos_pp, simp add: not_less, erule Real_leI [OF Y])
5.764 -
5.765 -lemma of_nat_less_two_power:
5.766 - "of_nat n < (2::'a::linordered_idom) ^ n"
5.767 -apply (induct n)
5.768 -apply simp
5.769 -apply (subgoal_tac "(1::'a) \<le> 2 ^ n")
5.770 -apply (drule (1) add_le_less_mono, simp)
5.771 -apply simp
5.772 -done
5.773 -
5.774 -lemma complete_real:
5.775 - fixes S :: "real set"
5.776 - assumes "\<exists>x. x \<in> S" and "\<exists>z. \<forall>x\<in>S. x \<le> z"
5.777 - shows "\<exists>y. (\<forall>x\<in>S. x \<le> y) \<and> (\<forall>z. (\<forall>x\<in>S. x \<le> z) \<longrightarrow> y \<le> z)"
5.778 -proof -
5.779 - obtain x where x: "x \<in> S" using assms(1) ..
5.780 - obtain z where z: "\<forall>x\<in>S. x \<le> z" using assms(2) ..
5.781 -
5.782 - def P \<equiv> "\<lambda>x. \<forall>y\<in>S. y \<le> of_rat x"
5.783 - obtain a where a: "\<not> P a"
5.784 - proof
5.785 - have "of_int (floor (x - 1)) \<le> x - 1" by (rule of_int_floor_le)
5.786 - also have "x - 1 < x" by simp
5.787 - finally have "of_int (floor (x - 1)) < x" .
5.788 - hence "\<not> x \<le> of_int (floor (x - 1))" by (simp only: not_le)
5.789 - then show "\<not> P (of_int (floor (x - 1)))"
5.790 - unfolding P_def of_rat_of_int_eq using x by fast
5.791 - qed
5.792 - obtain b where b: "P b"
5.793 - proof
5.794 - show "P (of_int (ceiling z))"
5.795 - unfolding P_def of_rat_of_int_eq
5.796 - proof
5.797 - fix y assume "y \<in> S"
5.798 - hence "y \<le> z" using z by simp
5.799 - also have "z \<le> of_int (ceiling z)" by (rule le_of_int_ceiling)
5.800 - finally show "y \<le> of_int (ceiling z)" .
5.801 - qed
5.802 - qed
5.803 -
5.804 - def avg \<equiv> "\<lambda>x y :: rat. x/2 + y/2"
5.805 - def bisect \<equiv> "\<lambda>(x, y). if P (avg x y) then (x, avg x y) else (avg x y, y)"
5.806 - def A \<equiv> "\<lambda>n. fst ((bisect ^^ n) (a, b))"
5.807 - def B \<equiv> "\<lambda>n. snd ((bisect ^^ n) (a, b))"
5.808 - def C \<equiv> "\<lambda>n. avg (A n) (B n)"
5.809 - have A_0 [simp]: "A 0 = a" unfolding A_def by simp
5.810 - have B_0 [simp]: "B 0 = b" unfolding B_def by simp
5.811 - have A_Suc [simp]: "\<And>n. A (Suc n) = (if P (C n) then A n else C n)"
5.812 - unfolding A_def B_def C_def bisect_def split_def by simp
5.813 - have B_Suc [simp]: "\<And>n. B (Suc n) = (if P (C n) then C n else B n)"
5.814 - unfolding A_def B_def C_def bisect_def split_def by simp
5.815 -
5.816 - have width: "\<And>n. B n - A n = (b - a) / 2^n"
5.817 - apply (simp add: eq_divide_eq)
5.818 - apply (induct_tac n, simp)
5.819 - apply (simp add: C_def avg_def algebra_simps)
5.820 - done
5.821 -
5.822 - have twos: "\<And>y r :: rat. 0 < r \<Longrightarrow> \<exists>n. y / 2 ^ n < r"
5.823 - apply (simp add: divide_less_eq)
5.824 - apply (subst mult_commute)
5.825 - apply (frule_tac y=y in ex_less_of_nat_mult)
5.826 - apply clarify
5.827 - apply (rule_tac x=n in exI)
5.828 - apply (erule less_trans)
5.829 - apply (rule mult_strict_right_mono)
5.830 - apply (rule le_less_trans [OF _ of_nat_less_two_power])
5.831 - apply simp
5.832 - apply assumption
5.833 - done
5.834 -
5.835 - have PA: "\<And>n. \<not> P (A n)"
5.836 - by (induct_tac n, simp_all add: a)
5.837 - have PB: "\<And>n. P (B n)"
5.838 - by (induct_tac n, simp_all add: b)
5.839 - have ab: "a < b"
5.840 - using a b unfolding P_def
5.841 - apply (clarsimp simp add: not_le)
5.842 - apply (drule (1) bspec)
5.843 - apply (drule (1) less_le_trans)
5.844 - apply (simp add: of_rat_less)
5.845 - done
5.846 - have AB: "\<And>n. A n < B n"
5.847 - by (induct_tac n, simp add: ab, simp add: C_def avg_def)
5.848 - have A_mono: "\<And>i j. i \<le> j \<Longrightarrow> A i \<le> A j"
5.849 - apply (auto simp add: le_less [where 'a=nat])
5.850 - apply (erule less_Suc_induct)
5.851 - apply (clarsimp simp add: C_def avg_def)
5.852 - apply (simp add: add_divide_distrib [symmetric])
5.853 - apply (rule AB [THEN less_imp_le])
5.854 - apply simp
5.855 - done
5.856 - have B_mono: "\<And>i j. i \<le> j \<Longrightarrow> B j \<le> B i"
5.857 - apply (auto simp add: le_less [where 'a=nat])
5.858 - apply (erule less_Suc_induct)
5.859 - apply (clarsimp simp add: C_def avg_def)
5.860 - apply (simp add: add_divide_distrib [symmetric])
5.861 - apply (rule AB [THEN less_imp_le])
5.862 - apply simp
5.863 - done
5.864 - have cauchy_lemma:
5.865 - "\<And>X. \<forall>n. \<forall>i\<ge>n. A n \<le> X i \<and> X i \<le> B n \<Longrightarrow> cauchy X"
5.866 - apply (rule cauchyI)
5.867 - apply (drule twos [where y="b - a"])
5.868 - apply (erule exE)
5.869 - apply (rule_tac x=n in exI, clarify, rename_tac i j)
5.870 - apply (rule_tac y="B n - A n" in le_less_trans) defer
5.871 - apply (simp add: width)
5.872 - apply (drule_tac x=n in spec)
5.873 - apply (frule_tac x=i in spec, drule (1) mp)
5.874 - apply (frule_tac x=j in spec, drule (1) mp)
5.875 - apply (frule A_mono, drule B_mono)
5.876 - apply (frule A_mono, drule B_mono)
5.877 - apply arith
5.878 - done
5.879 - have "cauchy A"
5.880 - apply (rule cauchy_lemma [rule_format])
5.881 - apply (simp add: A_mono)
5.882 - apply (erule order_trans [OF less_imp_le [OF AB] B_mono])
5.883 - done
5.884 - have "cauchy B"
5.885 - apply (rule cauchy_lemma [rule_format])
5.886 - apply (simp add: B_mono)
5.887 - apply (erule order_trans [OF A_mono less_imp_le [OF AB]])
5.888 - done
5.889 - have 1: "\<forall>x\<in>S. x \<le> Real B"
5.890 - proof
5.891 - fix x assume "x \<in> S"
5.892 - then show "x \<le> Real B"
5.893 - using PB [unfolded P_def] `cauchy B`
5.894 - by (simp add: le_RealI)
5.895 - qed
5.896 - have 2: "\<forall>z. (\<forall>x\<in>S. x \<le> z) \<longrightarrow> Real A \<le> z"
5.897 - apply clarify
5.898 - apply (erule contrapos_pp)
5.899 - apply (simp add: not_le)
5.900 - apply (drule less_RealD [OF `cauchy A`], clarify)
5.901 - apply (subgoal_tac "\<not> P (A n)")
5.902 - apply (simp add: P_def not_le, clarify)
5.903 - apply (erule rev_bexI)
5.904 - apply (erule (1) less_trans)
5.905 - apply (simp add: PA)
5.906 - done
5.907 - have "vanishes (\<lambda>n. (b - a) / 2 ^ n)"
5.908 - proof (rule vanishesI)
5.909 - fix r :: rat assume "0 < r"
5.910 - then obtain k where k: "\<bar>b - a\<bar> / 2 ^ k < r"
5.911 - using twos by fast
5.912 - have "\<forall>n\<ge>k. \<bar>(b - a) / 2 ^ n\<bar> < r"
5.913 - proof (clarify)
5.914 - fix n assume n: "k \<le> n"
5.915 - have "\<bar>(b - a) / 2 ^ n\<bar> = \<bar>b - a\<bar> / 2 ^ n"
5.916 - by simp
5.917 - also have "\<dots> \<le> \<bar>b - a\<bar> / 2 ^ k"
5.918 - using n by (simp add: divide_left_mono mult_pos_pos)
5.919 - also note k
5.920 - finally show "\<bar>(b - a) / 2 ^ n\<bar> < r" .
5.921 - qed
5.922 - thus "\<exists>k. \<forall>n\<ge>k. \<bar>(b - a) / 2 ^ n\<bar> < r" ..
5.923 - qed
5.924 - hence 3: "Real B = Real A"
5.925 - by (simp add: eq_Real `cauchy A` `cauchy B` width)
5.926 - show "\<exists>y. (\<forall>x\<in>S. x \<le> y) \<and> (\<forall>z. (\<forall>x\<in>S. x \<le> z) \<longrightarrow> y \<le> z)"
5.927 - using 1 2 3 by (rule_tac x="Real B" in exI, simp)
5.928 -qed
5.929 -
5.930 -
5.931 -instantiation real :: conditional_complete_linorder
5.932 -begin
5.933 -
5.934 -subsection{*Supremum of a set of reals*}
5.935 -
5.936 -definition
5.937 - Sup_real_def: "Sup X \<equiv> LEAST z::real. \<forall>x\<in>X. x\<le>z"
5.938 -
5.939 -definition
5.940 - Inf_real_def: "Inf (X::real set) \<equiv> - Sup (uminus ` X)"
5.941 -
5.942 -instance
5.943 -proof
5.944 - { fix z x :: real and X :: "real set"
5.945 - assume x: "x \<in> X" and z: "\<And>x. x \<in> X \<Longrightarrow> x \<le> z"
5.946 - 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"
5.947 - using complete_real[of X] by blast
5.948 - then show "x \<le> Sup X"
5.949 - unfolding Sup_real_def by (rule LeastI2_order) (auto simp: x) }
5.950 - note Sup_upper = this
5.951 -
5.952 - { fix z :: real and X :: "real set"
5.953 - assume x: "X \<noteq> {}" and z: "\<And>x. x \<in> X \<Longrightarrow> x \<le> z"
5.954 - 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"
5.955 - using complete_real[of X] by blast
5.956 - then have "Sup X = s"
5.957 - unfolding Sup_real_def by (best intro: Least_equality)
5.958 - also with s z have "... \<le> z"
5.959 - by blast
5.960 - finally show "Sup X \<le> z" . }
5.961 - note Sup_least = this
5.962 -
5.963 - { fix x z :: real and X :: "real set"
5.964 - assume x: "x \<in> X" and z: "\<And>x. x \<in> X \<Longrightarrow> z \<le> x"
5.965 - have "-x \<le> Sup (uminus ` X)"
5.966 - by (rule Sup_upper[of _ _ "- z"]) (auto simp add: image_iff x z)
5.967 - then show "Inf X \<le> x"
5.968 - by (auto simp add: Inf_real_def) }
5.969 -
5.970 - { fix z :: real and X :: "real set"
5.971 - assume x: "X \<noteq> {}" and z: "\<And>x. x \<in> X \<Longrightarrow> z \<le> x"
5.972 - have "Sup (uminus ` X) \<le> -z"
5.973 - using x z by (force intro: Sup_least)
5.974 - then show "z \<le> Inf X"
5.975 - by (auto simp add: Inf_real_def) }
5.976 -qed
5.977 -end
5.978 -
5.979 -text {*
5.980 - \medskip Completeness properties using @{text "isUb"}, @{text "isLub"}:
5.981 -*}
5.982 -
5.983 -lemma reals_complete: "\<exists>X. X \<in> S \<Longrightarrow> \<exists>Y. isUb (UNIV::real set) S Y \<Longrightarrow> \<exists>t. isLub (UNIV :: real set) S t"
5.984 - by (intro exI[of _ "Sup S"] isLub_cSup) (auto simp: setle_def isUb_def intro: cSup_upper)
5.985 -
5.986 -
5.987 -subsection {* Hiding implementation details *}
5.988 -
5.989 -hide_const (open) vanishes cauchy positive Real
5.990 -
5.991 -declare Real_induct [induct del]
5.992 -declare Abs_real_induct [induct del]
5.993 -declare Abs_real_cases [cases del]
5.994 -
5.995 -lemmas [transfer_rule del] =
5.996 - real.All_transfer real.Ex_transfer real.rel_eq_transfer forall_real_transfer
5.997 - zero_real.transfer one_real.transfer plus_real.transfer uminus_real.transfer
5.998 - times_real.transfer inverse_real.transfer positive.transfer real.right_unique
5.999 - real.right_total
5.1000 -
5.1001 -subsection{*More Lemmas*}
5.1002 -
5.1003 -text {* BH: These lemmas should not be necessary; they should be
5.1004 -covered by existing simp rules and simplification procedures. *}
5.1005 -
5.1006 -lemma real_mult_left_cancel: "(c::real) \<noteq> 0 ==> (c*a=c*b) = (a=b)"
5.1007 -by simp (* redundant with mult_cancel_left *)
5.1008 -
5.1009 -lemma real_mult_right_cancel: "(c::real) \<noteq> 0 ==> (a*c=b*c) = (a=b)"
5.1010 -by simp (* redundant with mult_cancel_right *)
5.1011 -
5.1012 -lemma real_mult_less_iff1 [simp]: "(0::real) < z ==> (x*z < y*z) = (x < y)"
5.1013 -by simp (* solved by linordered_ring_less_cancel_factor simproc *)
5.1014 -
5.1015 -lemma real_mult_le_cancel_iff1 [simp]: "(0::real) < z ==> (x*z \<le> y*z) = (x\<le>y)"
5.1016 -by simp (* solved by linordered_ring_le_cancel_factor simproc *)
5.1017 -
5.1018 -lemma real_mult_le_cancel_iff2 [simp]: "(0::real) < z ==> (z*x \<le> z*y) = (x\<le>y)"
5.1019 -by simp (* solved by linordered_ring_le_cancel_factor simproc *)
5.1020 -
5.1021 -
5.1022 -subsection {* Embedding numbers into the Reals *}
5.1023 -
5.1024 -abbreviation
5.1025 - real_of_nat :: "nat \<Rightarrow> real"
5.1026 -where
5.1027 - "real_of_nat \<equiv> of_nat"
5.1028 -
5.1029 -abbreviation
5.1030 - real_of_int :: "int \<Rightarrow> real"
5.1031 -where
5.1032 - "real_of_int \<equiv> of_int"
5.1033 -
5.1034 -abbreviation
5.1035 - real_of_rat :: "rat \<Rightarrow> real"
5.1036 -where
5.1037 - "real_of_rat \<equiv> of_rat"
5.1038 -
5.1039 -consts
5.1040 - (*overloaded constant for injecting other types into "real"*)
5.1041 - real :: "'a => real"
5.1042 -
5.1043 -defs (overloaded)
5.1044 - real_of_nat_def [code_unfold]: "real == real_of_nat"
5.1045 - real_of_int_def [code_unfold]: "real == real_of_int"
5.1046 -
5.1047 -declare [[coercion_enabled]]
5.1048 -declare [[coercion "real::nat\<Rightarrow>real"]]
5.1049 -declare [[coercion "real::int\<Rightarrow>real"]]
5.1050 -declare [[coercion "int"]]
5.1051 -
5.1052 -declare [[coercion_map map]]
5.1053 -declare [[coercion_map "% f g h x. g (h (f x))"]]
5.1054 -declare [[coercion_map "% f g (x,y) . (f x, g y)"]]
5.1055 -
5.1056 -lemma real_eq_of_nat: "real = of_nat"
5.1057 - unfolding real_of_nat_def ..
5.1058 -
5.1059 -lemma real_eq_of_int: "real = of_int"
5.1060 - unfolding real_of_int_def ..
5.1061 -
5.1062 -lemma real_of_int_zero [simp]: "real (0::int) = 0"
5.1063 -by (simp add: real_of_int_def)
5.1064 -
5.1065 -lemma real_of_one [simp]: "real (1::int) = (1::real)"
5.1066 -by (simp add: real_of_int_def)
5.1067 -
5.1068 -lemma real_of_int_add [simp]: "real(x + y) = real (x::int) + real y"
5.1069 -by (simp add: real_of_int_def)
5.1070 -
5.1071 -lemma real_of_int_minus [simp]: "real(-x) = -real (x::int)"
5.1072 -by (simp add: real_of_int_def)
5.1073 -
5.1074 -lemma real_of_int_diff [simp]: "real(x - y) = real (x::int) - real y"
5.1075 -by (simp add: real_of_int_def)
5.1076 -
5.1077 -lemma real_of_int_mult [simp]: "real(x * y) = real (x::int) * real y"
5.1078 -by (simp add: real_of_int_def)
5.1079 -
5.1080 -lemma real_of_int_power [simp]: "real (x ^ n) = real (x::int) ^ n"
5.1081 -by (simp add: real_of_int_def of_int_power)
5.1082 -
5.1083 -lemmas power_real_of_int = real_of_int_power [symmetric]
5.1084 -
5.1085 -lemma real_of_int_setsum [simp]: "real ((SUM x:A. f x)::int) = (SUM x:A. real(f x))"
5.1086 - apply (subst real_eq_of_int)+
5.1087 - apply (rule of_int_setsum)
5.1088 -done
5.1089 -
5.1090 -lemma real_of_int_setprod [simp]: "real ((PROD x:A. f x)::int) =
5.1091 - (PROD x:A. real(f x))"
5.1092 - apply (subst real_eq_of_int)+
5.1093 - apply (rule of_int_setprod)
5.1094 -done
5.1095 -
5.1096 -lemma real_of_int_zero_cancel [simp, algebra, presburger]: "(real x = 0) = (x = (0::int))"
5.1097 -by (simp add: real_of_int_def)
5.1098 -
5.1099 -lemma real_of_int_inject [iff, algebra, presburger]: "(real (x::int) = real y) = (x = y)"
5.1100 -by (simp add: real_of_int_def)
5.1101 -
5.1102 -lemma real_of_int_less_iff [iff, presburger]: "(real (x::int) < real y) = (x < y)"
5.1103 -by (simp add: real_of_int_def)
5.1104 -
5.1105 -lemma real_of_int_le_iff [simp, presburger]: "(real (x::int) \<le> real y) = (x \<le> y)"
5.1106 -by (simp add: real_of_int_def)
5.1107 -
5.1108 -lemma real_of_int_gt_zero_cancel_iff [simp, presburger]: "(0 < real (n::int)) = (0 < n)"
5.1109 -by (simp add: real_of_int_def)
5.1110 -
5.1111 -lemma real_of_int_ge_zero_cancel_iff [simp, presburger]: "(0 <= real (n::int)) = (0 <= n)"
5.1112 -by (simp add: real_of_int_def)
5.1113 -
5.1114 -lemma real_of_int_lt_zero_cancel_iff [simp, presburger]: "(real (n::int) < 0) = (n < 0)"
5.1115 -by (simp add: real_of_int_def)
5.1116 -
5.1117 -lemma real_of_int_le_zero_cancel_iff [simp, presburger]: "(real (n::int) <= 0) = (n <= 0)"
5.1118 -by (simp add: real_of_int_def)
5.1119 -
5.1120 -lemma one_less_real_of_int_cancel_iff: "1 < real (i :: int) \<longleftrightarrow> 1 < i"
5.1121 - unfolding real_of_one[symmetric] real_of_int_less_iff ..
5.1122 -
5.1123 -lemma one_le_real_of_int_cancel_iff: "1 \<le> real (i :: int) \<longleftrightarrow> 1 \<le> i"
5.1124 - unfolding real_of_one[symmetric] real_of_int_le_iff ..
5.1125 -
5.1126 -lemma real_of_int_less_one_cancel_iff: "real (i :: int) < 1 \<longleftrightarrow> i < 1"
5.1127 - unfolding real_of_one[symmetric] real_of_int_less_iff ..
5.1128 -
5.1129 -lemma real_of_int_le_one_cancel_iff: "real (i :: int) \<le> 1 \<longleftrightarrow> i \<le> 1"
5.1130 - unfolding real_of_one[symmetric] real_of_int_le_iff ..
5.1131 -
5.1132 -lemma real_of_int_abs [simp]: "real (abs x) = abs(real (x::int))"
5.1133 -by (auto simp add: abs_if)
5.1134 -
5.1135 -lemma int_less_real_le: "((n::int) < m) = (real n + 1 <= real m)"
5.1136 - apply (subgoal_tac "real n + 1 = real (n + 1)")
5.1137 - apply (simp del: real_of_int_add)
5.1138 - apply auto
5.1139 -done
5.1140 -
5.1141 -lemma int_le_real_less: "((n::int) <= m) = (real n < real m + 1)"
5.1142 - apply (subgoal_tac "real m + 1 = real (m + 1)")
5.1143 - apply (simp del: real_of_int_add)
5.1144 - apply simp
5.1145 -done
5.1146 -
5.1147 -lemma real_of_int_div_aux: "(real (x::int)) / (real d) =
5.1148 - real (x div d) + (real (x mod d)) / (real d)"
5.1149 -proof -
5.1150 - have "x = (x div d) * d + x mod d"
5.1151 - by auto
5.1152 - then have "real x = real (x div d) * real d + real(x mod d)"
5.1153 - by (simp only: real_of_int_mult [THEN sym] real_of_int_add [THEN sym])
5.1154 - then have "real x / real d = ... / real d"
5.1155 - by simp
5.1156 - then show ?thesis
5.1157 - by (auto simp add: add_divide_distrib algebra_simps)
5.1158 -qed
5.1159 -
5.1160 -lemma real_of_int_div: "(d :: int) dvd n ==>
5.1161 - real(n div d) = real n / real d"
5.1162 - apply (subst real_of_int_div_aux)
5.1163 - apply simp
5.1164 - apply (simp add: dvd_eq_mod_eq_0)
5.1165 -done
5.1166 -
5.1167 -lemma real_of_int_div2:
5.1168 - "0 <= real (n::int) / real (x) - real (n div x)"
5.1169 - apply (case_tac "x = 0")
5.1170 - apply simp
5.1171 - apply (case_tac "0 < x")
5.1172 - apply (simp add: algebra_simps)
5.1173 - apply (subst real_of_int_div_aux)
5.1174 - apply simp
5.1175 - apply (subst zero_le_divide_iff)
5.1176 - apply auto
5.1177 - apply (simp add: algebra_simps)
5.1178 - apply (subst real_of_int_div_aux)
5.1179 - apply simp
5.1180 - apply (subst zero_le_divide_iff)
5.1181 - apply auto
5.1182 -done
5.1183 -
5.1184 -lemma real_of_int_div3:
5.1185 - "real (n::int) / real (x) - real (n div x) <= 1"
5.1186 - apply (simp add: algebra_simps)
5.1187 - apply (subst real_of_int_div_aux)
5.1188 - apply (auto simp add: divide_le_eq intro: order_less_imp_le)
5.1189 -done
5.1190 -
5.1191 -lemma real_of_int_div4: "real (n div x) <= real (n::int) / real x"
5.1192 -by (insert real_of_int_div2 [of n x], simp)
5.1193 -
5.1194 -lemma Ints_real_of_int [simp]: "real (x::int) \<in> Ints"
5.1195 -unfolding real_of_int_def by (rule Ints_of_int)
5.1196 -
5.1197 -
5.1198 -subsection{*Embedding the Naturals into the Reals*}
5.1199 -
5.1200 -lemma real_of_nat_zero [simp]: "real (0::nat) = 0"
5.1201 -by (simp add: real_of_nat_def)
5.1202 -
5.1203 -lemma real_of_nat_1 [simp]: "real (1::nat) = 1"
5.1204 -by (simp add: real_of_nat_def)
5.1205 -
5.1206 -lemma real_of_nat_one [simp]: "real (Suc 0) = (1::real)"
5.1207 -by (simp add: real_of_nat_def)
5.1208 -
5.1209 -lemma real_of_nat_add [simp]: "real (m + n) = real (m::nat) + real n"
5.1210 -by (simp add: real_of_nat_def)
5.1211 -
5.1212 -(*Not for addsimps: often the LHS is used to represent a positive natural*)
5.1213 -lemma real_of_nat_Suc: "real (Suc n) = real n + (1::real)"
5.1214 -by (simp add: real_of_nat_def)
5.1215 -
5.1216 -lemma real_of_nat_less_iff [iff]:
5.1217 - "(real (n::nat) < real m) = (n < m)"
5.1218 -by (simp add: real_of_nat_def)
5.1219 -
5.1220 -lemma real_of_nat_le_iff [iff]: "(real (n::nat) \<le> real m) = (n \<le> m)"
5.1221 -by (simp add: real_of_nat_def)
5.1222 -
5.1223 -lemma real_of_nat_ge_zero [iff]: "0 \<le> real (n::nat)"
5.1224 -by (simp add: real_of_nat_def)
5.1225 -
5.1226 -lemma real_of_nat_Suc_gt_zero: "0 < real (Suc n)"
5.1227 -by (simp add: real_of_nat_def del: of_nat_Suc)
5.1228 -
5.1229 -lemma real_of_nat_mult [simp]: "real (m * n) = real (m::nat) * real n"
5.1230 -by (simp add: real_of_nat_def of_nat_mult)
5.1231 -
5.1232 -lemma real_of_nat_power [simp]: "real (m ^ n) = real (m::nat) ^ n"
5.1233 -by (simp add: real_of_nat_def of_nat_power)
5.1234 -
5.1235 -lemmas power_real_of_nat = real_of_nat_power [symmetric]
5.1236 -
5.1237 -lemma real_of_nat_setsum [simp]: "real ((SUM x:A. f x)::nat) =
5.1238 - (SUM x:A. real(f x))"
5.1239 - apply (subst real_eq_of_nat)+
5.1240 - apply (rule of_nat_setsum)
5.1241 -done
5.1242 -
5.1243 -lemma real_of_nat_setprod [simp]: "real ((PROD x:A. f x)::nat) =
5.1244 - (PROD x:A. real(f x))"
5.1245 - apply (subst real_eq_of_nat)+
5.1246 - apply (rule of_nat_setprod)
5.1247 -done
5.1248 -
5.1249 -lemma real_of_card: "real (card A) = setsum (%x.1) A"
5.1250 - apply (subst card_eq_setsum)
5.1251 - apply (subst real_of_nat_setsum)
5.1252 - apply simp
5.1253 -done
5.1254 -
5.1255 -lemma real_of_nat_inject [iff]: "(real (n::nat) = real m) = (n = m)"
5.1256 -by (simp add: real_of_nat_def)
5.1257 -
5.1258 -lemma real_of_nat_zero_iff [iff]: "(real (n::nat) = 0) = (n = 0)"
5.1259 -by (simp add: real_of_nat_def)
5.1260 -
5.1261 -lemma real_of_nat_diff: "n \<le> m ==> real (m - n) = real (m::nat) - real n"
5.1262 -by (simp add: add: real_of_nat_def of_nat_diff)
5.1263 -
5.1264 -lemma real_of_nat_gt_zero_cancel_iff [simp]: "(0 < real (n::nat)) = (0 < n)"
5.1265 -by (auto simp: real_of_nat_def)
5.1266 -
5.1267 -lemma real_of_nat_le_zero_cancel_iff [simp]: "(real (n::nat) \<le> 0) = (n = 0)"
5.1268 -by (simp add: add: real_of_nat_def)
5.1269 -
5.1270 -lemma not_real_of_nat_less_zero [simp]: "~ real (n::nat) < 0"
5.1271 -by (simp add: add: real_of_nat_def)
5.1272 -
5.1273 -lemma nat_less_real_le: "((n::nat) < m) = (real n + 1 <= real m)"
5.1274 - apply (subgoal_tac "real n + 1 = real (Suc n)")
5.1275 - apply simp
5.1276 - apply (auto simp add: real_of_nat_Suc)
5.1277 -done
5.1278 -
5.1279 -lemma nat_le_real_less: "((n::nat) <= m) = (real n < real m + 1)"
5.1280 - apply (subgoal_tac "real m + 1 = real (Suc m)")
5.1281 - apply (simp add: less_Suc_eq_le)
5.1282 - apply (simp add: real_of_nat_Suc)
5.1283 -done
5.1284 -
5.1285 -lemma real_of_nat_div_aux: "(real (x::nat)) / (real d) =
5.1286 - real (x div d) + (real (x mod d)) / (real d)"
5.1287 -proof -
5.1288 - have "x = (x div d) * d + x mod d"
5.1289 - by auto
5.1290 - then have "real x = real (x div d) * real d + real(x mod d)"
5.1291 - by (simp only: real_of_nat_mult [THEN sym] real_of_nat_add [THEN sym])
5.1292 - then have "real x / real d = \<dots> / real d"
5.1293 - by simp
5.1294 - then show ?thesis
5.1295 - by (auto simp add: add_divide_distrib algebra_simps)
5.1296 -qed
5.1297 -
5.1298 -lemma real_of_nat_div: "(d :: nat) dvd n ==>
5.1299 - real(n div d) = real n / real d"
5.1300 - by (subst real_of_nat_div_aux)
5.1301 - (auto simp add: dvd_eq_mod_eq_0 [symmetric])
5.1302 -
5.1303 -lemma real_of_nat_div2:
5.1304 - "0 <= real (n::nat) / real (x) - real (n div x)"
5.1305 -apply (simp add: algebra_simps)
5.1306 -apply (subst real_of_nat_div_aux)
5.1307 -apply simp
5.1308 -apply (subst zero_le_divide_iff)
5.1309 -apply simp
5.1310 -done
5.1311 -
5.1312 -lemma real_of_nat_div3:
5.1313 - "real (n::nat) / real (x) - real (n div x) <= 1"
5.1314 -apply(case_tac "x = 0")
5.1315 -apply (simp)
5.1316 -apply (simp add: algebra_simps)
5.1317 -apply (subst real_of_nat_div_aux)
5.1318 -apply simp
5.1319 -done
5.1320 -
5.1321 -lemma real_of_nat_div4: "real (n div x) <= real (n::nat) / real x"
5.1322 -by (insert real_of_nat_div2 [of n x], simp)
5.1323 -
5.1324 -lemma real_of_int_of_nat_eq [simp]: "real (of_nat n :: int) = real n"
5.1325 -by (simp add: real_of_int_def real_of_nat_def)
5.1326 -
5.1327 -lemma real_nat_eq_real [simp]: "0 <= x ==> real(nat x) = real x"
5.1328 - apply (subgoal_tac "real(int(nat x)) = real(nat x)")
5.1329 - apply force
5.1330 - apply (simp only: real_of_int_of_nat_eq)
5.1331 -done
5.1332 -
5.1333 -lemma Nats_real_of_nat [simp]: "real (n::nat) \<in> Nats"
5.1334 -unfolding real_of_nat_def by (rule of_nat_in_Nats)
5.1335 -
5.1336 -lemma Ints_real_of_nat [simp]: "real (n::nat) \<in> Ints"
5.1337 -unfolding real_of_nat_def by (rule Ints_of_nat)
5.1338 -
5.1339 -subsection {* The Archimedean Property of the Reals *}
5.1340 -
5.1341 -theorem reals_Archimedean:
5.1342 - assumes x_pos: "0 < x"
5.1343 - shows "\<exists>n. inverse (real (Suc n)) < x"
5.1344 - unfolding real_of_nat_def using x_pos
5.1345 - by (rule ex_inverse_of_nat_Suc_less)
5.1346 -
5.1347 -lemma reals_Archimedean2: "\<exists>n. (x::real) < real (n::nat)"
5.1348 - unfolding real_of_nat_def by (rule ex_less_of_nat)
5.1349 -
5.1350 -lemma reals_Archimedean3:
5.1351 - assumes x_greater_zero: "0 < x"
5.1352 - shows "\<forall>(y::real). \<exists>(n::nat). y < real n * x"
5.1353 - unfolding real_of_nat_def using `0 < x`
5.1354 - by (auto intro: ex_less_of_nat_mult)
5.1355 -
5.1356 -
5.1357 -subsection{* Rationals *}
5.1358 -
5.1359 -lemma Rats_real_nat[simp]: "real(n::nat) \<in> \<rat>"
5.1360 -by (simp add: real_eq_of_nat)
5.1361 -
5.1362 -
5.1363 -lemma Rats_eq_int_div_int:
5.1364 - "\<rat> = { real(i::int)/real(j::int) |i j. j \<noteq> 0}" (is "_ = ?S")
5.1365 -proof
5.1366 - show "\<rat> \<subseteq> ?S"
5.1367 - proof
5.1368 - fix x::real assume "x : \<rat>"
5.1369 - then obtain r where "x = of_rat r" unfolding Rats_def ..
5.1370 - have "of_rat r : ?S"
5.1371 - by (cases r)(auto simp add:of_rat_rat real_eq_of_int)
5.1372 - thus "x : ?S" using `x = of_rat r` by simp
5.1373 - qed
5.1374 -next
5.1375 - show "?S \<subseteq> \<rat>"
5.1376 - proof(auto simp:Rats_def)
5.1377 - fix i j :: int assume "j \<noteq> 0"
5.1378 - hence "real i / real j = of_rat(Fract i j)"
5.1379 - by (simp add:of_rat_rat real_eq_of_int)
5.1380 - thus "real i / real j \<in> range of_rat" by blast
5.1381 - qed
5.1382 -qed
5.1383 -
5.1384 -lemma Rats_eq_int_div_nat:
5.1385 - "\<rat> = { real(i::int)/real(n::nat) |i n. n \<noteq> 0}"
5.1386 -proof(auto simp:Rats_eq_int_div_int)
5.1387 - fix i j::int assume "j \<noteq> 0"
5.1388 - show "EX (i'::int) (n::nat). real i/real j = real i'/real n \<and> 0<n"
5.1389 - proof cases
5.1390 - assume "j>0"
5.1391 - hence "real i/real j = real i/real(nat j) \<and> 0<nat j"
5.1392 - by (simp add: real_eq_of_int real_eq_of_nat of_nat_nat)
5.1393 - thus ?thesis by blast
5.1394 - next
5.1395 - assume "~ j>0"
5.1396 - hence "real i/real j = real(-i)/real(nat(-j)) \<and> 0<nat(-j)" using `j\<noteq>0`
5.1397 - by (simp add: real_eq_of_int real_eq_of_nat of_nat_nat)
5.1398 - thus ?thesis by blast
5.1399 - qed
5.1400 -next
5.1401 - fix i::int and n::nat assume "0 < n"
5.1402 - hence "real i/real n = real i/real(int n) \<and> int n \<noteq> 0" by simp
5.1403 - thus "\<exists>(i'::int) j::int. real i/real n = real i'/real j \<and> j \<noteq> 0" by blast
5.1404 -qed
5.1405 -
5.1406 -lemma Rats_abs_nat_div_natE:
5.1407 - assumes "x \<in> \<rat>"
5.1408 - obtains m n :: nat
5.1409 - where "n \<noteq> 0" and "\<bar>x\<bar> = real m / real n" and "gcd m n = 1"
5.1410 -proof -
5.1411 - from `x \<in> \<rat>` obtain i::int and n::nat where "n \<noteq> 0" and "x = real i / real n"
5.1412 - by(auto simp add: Rats_eq_int_div_nat)
5.1413 - hence "\<bar>x\<bar> = real(nat(abs i)) / real n" by simp
5.1414 - then obtain m :: nat where x_rat: "\<bar>x\<bar> = real m / real n" by blast
5.1415 - let ?gcd = "gcd m n"
5.1416 - from `n\<noteq>0` have gcd: "?gcd \<noteq> 0" by simp
5.1417 - let ?k = "m div ?gcd"
5.1418 - let ?l = "n div ?gcd"
5.1419 - let ?gcd' = "gcd ?k ?l"
5.1420 - have "?gcd dvd m" .. then have gcd_k: "?gcd * ?k = m"
5.1421 - by (rule dvd_mult_div_cancel)
5.1422 - have "?gcd dvd n" .. then have gcd_l: "?gcd * ?l = n"
5.1423 - by (rule dvd_mult_div_cancel)
5.1424 - from `n\<noteq>0` and gcd_l have "?l \<noteq> 0" by (auto iff del: neq0_conv)
5.1425 - moreover
5.1426 - have "\<bar>x\<bar> = real ?k / real ?l"
5.1427 - proof -
5.1428 - from gcd have "real ?k / real ?l =
5.1429 - real (?gcd * ?k) / real (?gcd * ?l)" by simp
5.1430 - also from gcd_k and gcd_l have "\<dots> = real m / real n" by simp
5.1431 - also from x_rat have "\<dots> = \<bar>x\<bar>" ..
5.1432 - finally show ?thesis ..
5.1433 - qed
5.1434 - moreover
5.1435 - have "?gcd' = 1"
5.1436 - proof -
5.1437 - have "?gcd * ?gcd' = gcd (?gcd * ?k) (?gcd * ?l)"
5.1438 - by (rule gcd_mult_distrib_nat)
5.1439 - with gcd_k gcd_l have "?gcd * ?gcd' = ?gcd" by simp
5.1440 - with gcd show ?thesis by auto
5.1441 - qed
5.1442 - ultimately show ?thesis ..
5.1443 -qed
5.1444 -
5.1445 -subsection{*Density of the Rational Reals in the Reals*}
5.1446 -
5.1447 -text{* This density proof is due to Stefan Richter and was ported by TN. The
5.1448 -original source is \emph{Real Analysis} by H.L. Royden.
5.1449 -It employs the Archimedean property of the reals. *}
5.1450 -
5.1451 -lemma Rats_dense_in_real:
5.1452 - fixes x :: real
5.1453 - assumes "x < y" shows "\<exists>r\<in>\<rat>. x < r \<and> r < y"
5.1454 -proof -
5.1455 - from `x<y` have "0 < y-x" by simp
5.1456 - with reals_Archimedean obtain q::nat
5.1457 - where q: "inverse (real q) < y-x" and "0 < q" by auto
5.1458 - def p \<equiv> "ceiling (y * real q) - 1"
5.1459 - def r \<equiv> "of_int p / real q"
5.1460 - from q have "x < y - inverse (real q)" by simp
5.1461 - also have "y - inverse (real q) \<le> r"
5.1462 - unfolding r_def p_def
5.1463 - by (simp add: le_divide_eq left_diff_distrib le_of_int_ceiling `0 < q`)
5.1464 - finally have "x < r" .
5.1465 - moreover have "r < y"
5.1466 - unfolding r_def p_def
5.1467 - by (simp add: divide_less_eq diff_less_eq `0 < q`
5.1468 - less_ceiling_iff [symmetric])
5.1469 - moreover from r_def have "r \<in> \<rat>" by simp
5.1470 - ultimately show ?thesis by fast
5.1471 -qed
5.1472 -
5.1473 -
5.1474 -
5.1475 -subsection{*Numerals and Arithmetic*}
5.1476 -
5.1477 -lemma [code_abbrev]:
5.1478 - "real_of_int (numeral k) = numeral k"
5.1479 - "real_of_int (neg_numeral k) = neg_numeral k"
5.1480 - by simp_all
5.1481 -
5.1482 -text{*Collapse applications of @{term real} to @{term number_of}*}
5.1483 -lemma real_numeral [simp]:
5.1484 - "real (numeral v :: int) = numeral v"
5.1485 - "real (neg_numeral v :: int) = neg_numeral v"
5.1486 -by (simp_all add: real_of_int_def)
5.1487 -
5.1488 -lemma real_of_nat_numeral [simp]:
5.1489 - "real (numeral v :: nat) = numeral v"
5.1490 -by (simp add: real_of_nat_def)
5.1491 -
5.1492 -declaration {*
5.1493 - K (Lin_Arith.add_inj_thms [@{thm real_of_nat_le_iff} RS iffD2, @{thm real_of_nat_inject} RS iffD2]
5.1494 - (* not needed because x < (y::nat) can be rewritten as Suc x <= y: real_of_nat_less_iff RS iffD2 *)
5.1495 - #> Lin_Arith.add_inj_thms [@{thm real_of_int_le_iff} RS iffD2, @{thm real_of_int_inject} RS iffD2]
5.1496 - (* not needed because x < (y::int) can be rewritten as x + 1 <= y: real_of_int_less_iff RS iffD2 *)
5.1497 - #> Lin_Arith.add_simps [@{thm real_of_nat_zero}, @{thm real_of_nat_Suc}, @{thm real_of_nat_add},
5.1498 - @{thm real_of_nat_mult}, @{thm real_of_int_zero}, @{thm real_of_one},
5.1499 - @{thm real_of_int_add}, @{thm real_of_int_minus}, @{thm real_of_int_diff},
5.1500 - @{thm real_of_int_mult}, @{thm real_of_int_of_nat_eq},
5.1501 - @{thm real_of_nat_numeral}, @{thm real_numeral(1)}, @{thm real_numeral(2)}]
5.1502 - #> Lin_Arith.add_inj_const (@{const_name real}, @{typ "nat \<Rightarrow> real"})
5.1503 - #> Lin_Arith.add_inj_const (@{const_name real}, @{typ "int \<Rightarrow> real"}))
5.1504 -*}
5.1505 -
5.1506 -
5.1507 -subsection{* Simprules combining x+y and 0: ARE THEY NEEDED?*}
5.1508 -
5.1509 -lemma real_add_minus_iff [simp]: "(x + - a = (0::real)) = (x=a)"
5.1510 -by arith
5.1511 -
5.1512 -text {* FIXME: redundant with @{text add_eq_0_iff} below *}
5.1513 -lemma real_add_eq_0_iff: "(x+y = (0::real)) = (y = -x)"
5.1514 -by auto
5.1515 -
5.1516 -lemma real_add_less_0_iff: "(x+y < (0::real)) = (y < -x)"
5.1517 -by auto
5.1518 -
5.1519 -lemma real_0_less_add_iff: "((0::real) < x+y) = (-x < y)"
5.1520 -by auto
5.1521 -
5.1522 -lemma real_add_le_0_iff: "(x+y \<le> (0::real)) = (y \<le> -x)"
5.1523 -by auto
5.1524 -
5.1525 -lemma real_0_le_add_iff: "((0::real) \<le> x+y) = (-x \<le> y)"
5.1526 -by auto
5.1527 -
5.1528 -subsection {* Lemmas about powers *}
5.1529 -
5.1530 -text {* FIXME: declare this in Rings.thy or not at all *}
5.1531 -declare abs_mult_self [simp]
5.1532 -
5.1533 -(* used by Import/HOL/real.imp *)
5.1534 -lemma two_realpow_ge_one: "(1::real) \<le> 2 ^ n"
5.1535 -by simp
5.1536 -
5.1537 -lemma two_realpow_gt [simp]: "real (n::nat) < 2 ^ n"
5.1538 -apply (induct "n")
5.1539 -apply (auto simp add: real_of_nat_Suc)
5.1540 -apply (subst mult_2)
5.1541 -apply (erule add_less_le_mono)
5.1542 -apply (rule two_realpow_ge_one)
5.1543 -done
5.1544 -
5.1545 -text {* TODO: no longer real-specific; rename and move elsewhere *}
5.1546 -lemma realpow_Suc_le_self:
5.1547 - fixes r :: "'a::linordered_semidom"
5.1548 - shows "[| 0 \<le> r; r \<le> 1 |] ==> r ^ Suc n \<le> r"
5.1549 -by (insert power_decreasing [of 1 "Suc n" r], simp)
5.1550 -
5.1551 -text {* TODO: no longer real-specific; rename and move elsewhere *}
5.1552 -lemma realpow_minus_mult:
5.1553 - fixes x :: "'a::monoid_mult"
5.1554 - shows "0 < n \<Longrightarrow> x ^ (n - 1) * x = x ^ n"
5.1555 -by (simp add: power_commutes split add: nat_diff_split)
5.1556 -
5.1557 -text {* FIXME: declare this [simp] for all types, or not at all *}
5.1558 -lemma real_two_squares_add_zero_iff [simp]:
5.1559 - "(x * x + y * y = 0) = ((x::real) = 0 \<and> y = 0)"
5.1560 -by (rule sum_squares_eq_zero_iff)
5.1561 -
5.1562 -text {* FIXME: declare this [simp] for all types, or not at all *}
5.1563 -lemma realpow_two_sum_zero_iff [simp]:
5.1564 - "(x ^ 2 + y ^ 2 = (0::real)) = (x = 0 & y = 0)"
5.1565 -by (rule sum_power2_eq_zero_iff)
5.1566 -
5.1567 -lemma real_minus_mult_self_le [simp]: "-(u * u) \<le> (x * (x::real))"
5.1568 -by (rule_tac y = 0 in order_trans, auto)
5.1569 -
5.1570 -lemma realpow_square_minus_le [simp]: "-(u ^ 2) \<le> (x::real) ^ 2"
5.1571 -by (auto simp add: power2_eq_square)
5.1572 -
5.1573 -
5.1574 -lemma numeral_power_le_real_of_nat_cancel_iff[simp]:
5.1575 - "(numeral x::real) ^ n \<le> real a \<longleftrightarrow> (numeral x::nat) ^ n \<le> a"
5.1576 - unfolding real_of_nat_le_iff[symmetric] by simp
5.1577 -
5.1578 -lemma real_of_nat_le_numeral_power_cancel_iff[simp]:
5.1579 - "real a \<le> (numeral x::real) ^ n \<longleftrightarrow> a \<le> (numeral x::nat) ^ n"
5.1580 - unfolding real_of_nat_le_iff[symmetric] by simp
5.1581 -
5.1582 -lemma numeral_power_le_real_of_int_cancel_iff[simp]:
5.1583 - "(numeral x::real) ^ n \<le> real a \<longleftrightarrow> (numeral x::int) ^ n \<le> a"
5.1584 - unfolding real_of_int_le_iff[symmetric] by simp
5.1585 -
5.1586 -lemma real_of_int_le_numeral_power_cancel_iff[simp]:
5.1587 - "real a \<le> (numeral x::real) ^ n \<longleftrightarrow> a \<le> (numeral x::int) ^ n"
5.1588 - unfolding real_of_int_le_iff[symmetric] by simp
5.1589 -
5.1590 -lemma neg_numeral_power_le_real_of_int_cancel_iff[simp]:
5.1591 - "(neg_numeral x::real) ^ n \<le> real a \<longleftrightarrow> (neg_numeral x::int) ^ n \<le> a"
5.1592 - unfolding real_of_int_le_iff[symmetric] by simp
5.1593 -
5.1594 -lemma real_of_int_le_neg_numeral_power_cancel_iff[simp]:
5.1595 - "real a \<le> (neg_numeral x::real) ^ n \<longleftrightarrow> a \<le> (neg_numeral x::int) ^ n"
5.1596 - unfolding real_of_int_le_iff[symmetric] by simp
5.1597 -
5.1598 -subsection{*Density of the Reals*}
5.1599 -
5.1600 -lemma real_lbound_gt_zero:
5.1601 - "[| (0::real) < d1; 0 < d2 |] ==> \<exists>e. 0 < e & e < d1 & e < d2"
5.1602 -apply (rule_tac x = " (min d1 d2) /2" in exI)
5.1603 -apply (simp add: min_def)
5.1604 -done
5.1605 -
5.1606 -
5.1607 -text{*Similar results are proved in @{text Fields}*}
5.1608 -lemma real_less_half_sum: "x < y ==> x < (x+y) / (2::real)"
5.1609 - by auto
5.1610 -
5.1611 -lemma real_gt_half_sum: "x < y ==> (x+y)/(2::real) < y"
5.1612 - by auto
5.1613 -
5.1614 -lemma real_sum_of_halves: "x/2 + x/2 = (x::real)"
5.1615 - by simp
5.1616 -
5.1617 -subsection{*Absolute Value Function for the Reals*}
5.1618 -
5.1619 -lemma abs_minus_add_cancel: "abs(x + (-y)) = abs (y + (-(x::real)))"
5.1620 -by (simp add: abs_if)
5.1621 -
5.1622 -(* FIXME: redundant, but used by Integration/RealRandVar.thy in AFP *)
5.1623 -lemma abs_le_interval_iff: "(abs x \<le> r) = (-r\<le>x & x\<le>(r::real))"
5.1624 -by (force simp add: abs_le_iff)
5.1625 -
5.1626 -lemma abs_add_one_gt_zero: "(0::real) < 1 + abs(x)"
5.1627 -by (simp add: abs_if)
5.1628 -
5.1629 -lemma abs_real_of_nat_cancel [simp]: "abs (real x) = real (x::nat)"
5.1630 -by (rule abs_of_nonneg [OF real_of_nat_ge_zero])
5.1631 -
5.1632 -lemma abs_add_one_not_less_self: "~ abs(x) + (1::real) < x"
5.1633 -by simp
5.1634 -
5.1635 -lemma abs_sum_triangle_ineq: "abs ((x::real) + y + (-l + -m)) \<le> abs(x + -l) + abs(y + -m)"
5.1636 -by simp
5.1637 -
5.1638 -
5.1639 -subsection{*Floor and Ceiling Functions from the Reals to the Integers*}
5.1640 -
5.1641 -(* FIXME: theorems for negative numerals *)
5.1642 -lemma numeral_less_real_of_int_iff [simp]:
5.1643 - "((numeral n) < real (m::int)) = (numeral n < m)"
5.1644 -apply auto
5.1645 -apply (rule real_of_int_less_iff [THEN iffD1])
5.1646 -apply (drule_tac [2] real_of_int_less_iff [THEN iffD2], auto)
5.1647 -done
5.1648 -
5.1649 -lemma numeral_less_real_of_int_iff2 [simp]:
5.1650 - "(real (m::int) < (numeral n)) = (m < numeral n)"
5.1651 -apply auto
5.1652 -apply (rule real_of_int_less_iff [THEN iffD1])
5.1653 -apply (drule_tac [2] real_of_int_less_iff [THEN iffD2], auto)
5.1654 -done
5.1655 -
5.1656 -lemma numeral_le_real_of_int_iff [simp]:
5.1657 - "((numeral n) \<le> real (m::int)) = (numeral n \<le> m)"
5.1658 -by (simp add: linorder_not_less [symmetric])
5.1659 -
5.1660 -lemma numeral_le_real_of_int_iff2 [simp]:
5.1661 - "(real (m::int) \<le> (numeral n)) = (m \<le> numeral n)"
5.1662 -by (simp add: linorder_not_less [symmetric])
5.1663 -
5.1664 -lemma floor_real_of_nat [simp]: "floor (real (n::nat)) = int n"
5.1665 -unfolding real_of_nat_def by simp
5.1666 -
5.1667 -lemma floor_minus_real_of_nat [simp]: "floor (- real (n::nat)) = - int n"
5.1668 -unfolding real_of_nat_def by (simp add: floor_minus)
5.1669 -
5.1670 -lemma floor_real_of_int [simp]: "floor (real (n::int)) = n"
5.1671 -unfolding real_of_int_def by simp
5.1672 -
5.1673 -lemma floor_minus_real_of_int [simp]: "floor (- real (n::int)) = - n"
5.1674 -unfolding real_of_int_def by (simp add: floor_minus)
5.1675 -
5.1676 -lemma real_lb_ub_int: " \<exists>n::int. real n \<le> r & r < real (n+1)"
5.1677 -unfolding real_of_int_def by (rule floor_exists)
5.1678 -
5.1679 -lemma lemma_floor:
5.1680 - assumes a1: "real m \<le> r" and a2: "r < real n + 1"
5.1681 - shows "m \<le> (n::int)"
5.1682 -proof -
5.1683 - have "real m < real n + 1" using a1 a2 by (rule order_le_less_trans)
5.1684 - also have "... = real (n + 1)" by simp
5.1685 - finally have "m < n + 1" by (simp only: real_of_int_less_iff)
5.1686 - thus ?thesis by arith
5.1687 -qed
5.1688 -
5.1689 -lemma real_of_int_floor_le [simp]: "real (floor r) \<le> r"
5.1690 -unfolding real_of_int_def by (rule of_int_floor_le)
5.1691 -
5.1692 -lemma lemma_floor2: "real n < real (x::int) + 1 ==> n \<le> x"
5.1693 -by (auto intro: lemma_floor)
5.1694 -
5.1695 -lemma real_of_int_floor_cancel [simp]:
5.1696 - "(real (floor x) = x) = (\<exists>n::int. x = real n)"
5.1697 - using floor_real_of_int by metis
5.1698 -
5.1699 -lemma floor_eq: "[| real n < x; x < real n + 1 |] ==> floor x = n"
5.1700 - unfolding real_of_int_def using floor_unique [of n x] by simp
5.1701 -
5.1702 -lemma floor_eq2: "[| real n \<le> x; x < real n + 1 |] ==> floor x = n"
5.1703 - unfolding real_of_int_def by (rule floor_unique)
5.1704 -
5.1705 -lemma floor_eq3: "[| real n < x; x < real (Suc n) |] ==> nat(floor x) = n"
5.1706 -apply (rule inj_int [THEN injD])
5.1707 -apply (simp add: real_of_nat_Suc)
5.1708 -apply (simp add: real_of_nat_Suc floor_eq floor_eq [where n = "int n"])
5.1709 -done
5.1710 -
5.1711 -lemma floor_eq4: "[| real n \<le> x; x < real (Suc n) |] ==> nat(floor x) = n"
5.1712 -apply (drule order_le_imp_less_or_eq)
5.1713 -apply (auto intro: floor_eq3)
5.1714 -done
5.1715 -
5.1716 -lemma real_of_int_floor_ge_diff_one [simp]: "r - 1 \<le> real(floor r)"
5.1717 - unfolding real_of_int_def using floor_correct [of r] by simp
5.1718 -
5.1719 -lemma real_of_int_floor_gt_diff_one [simp]: "r - 1 < real(floor r)"
5.1720 - unfolding real_of_int_def using floor_correct [of r] by simp
5.1721 -
5.1722 -lemma real_of_int_floor_add_one_ge [simp]: "r \<le> real(floor r) + 1"
5.1723 - unfolding real_of_int_def using floor_correct [of r] by simp
5.1724 -
5.1725 -lemma real_of_int_floor_add_one_gt [simp]: "r < real(floor r) + 1"
5.1726 - unfolding real_of_int_def using floor_correct [of r] by simp
5.1727 -
5.1728 -lemma le_floor: "real a <= x ==> a <= floor x"
5.1729 - unfolding real_of_int_def by (simp add: le_floor_iff)
5.1730 -
5.1731 -lemma real_le_floor: "a <= floor x ==> real a <= x"
5.1732 - unfolding real_of_int_def by (simp add: le_floor_iff)
5.1733 -
5.1734 -lemma le_floor_eq: "(a <= floor x) = (real a <= x)"
5.1735 - unfolding real_of_int_def by (rule le_floor_iff)
5.1736 -
5.1737 -lemma floor_less_eq: "(floor x < a) = (x < real a)"
5.1738 - unfolding real_of_int_def by (rule floor_less_iff)
5.1739 -
5.1740 -lemma less_floor_eq: "(a < floor x) = (real a + 1 <= x)"
5.1741 - unfolding real_of_int_def by (rule less_floor_iff)
5.1742 -
5.1743 -lemma floor_le_eq: "(floor x <= a) = (x < real a + 1)"
5.1744 - unfolding real_of_int_def by (rule floor_le_iff)
5.1745 -
5.1746 -lemma floor_add [simp]: "floor (x + real a) = floor x + a"
5.1747 - unfolding real_of_int_def by (rule floor_add_of_int)
5.1748 -
5.1749 -lemma floor_subtract [simp]: "floor (x - real a) = floor x - a"
5.1750 - unfolding real_of_int_def by (rule floor_diff_of_int)
5.1751 -
5.1752 -lemma le_mult_floor:
5.1753 - assumes "0 \<le> (a :: real)" and "0 \<le> b"
5.1754 - shows "floor a * floor b \<le> floor (a * b)"
5.1755 -proof -
5.1756 - have "real (floor a) \<le> a"
5.1757 - and "real (floor b) \<le> b" by auto
5.1758 - hence "real (floor a * floor b) \<le> a * b"
5.1759 - using assms by (auto intro!: mult_mono)
5.1760 - also have "a * b < real (floor (a * b) + 1)" by auto
5.1761 - finally show ?thesis unfolding real_of_int_less_iff by simp
5.1762 -qed
5.1763 -
5.1764 -lemma floor_divide_eq_div:
5.1765 - "floor (real a / real b) = a div b"
5.1766 -proof cases
5.1767 - assume "b \<noteq> 0 \<or> b dvd a"
5.1768 - with real_of_int_div3[of a b] show ?thesis
5.1769 - by (auto simp: real_of_int_div[symmetric] intro!: floor_eq2 real_of_int_div4 neq_le_trans)
5.1770 - (metis add_left_cancel zero_neq_one real_of_int_div_aux real_of_int_inject
5.1771 - real_of_int_zero_cancel right_inverse_eq div_self mod_div_trivial)
5.1772 -qed (auto simp: real_of_int_div)
5.1773 -
5.1774 -lemma ceiling_real_of_nat [simp]: "ceiling (real (n::nat)) = int n"
5.1775 - unfolding real_of_nat_def by simp
5.1776 -
5.1777 -lemma real_of_int_ceiling_ge [simp]: "r \<le> real (ceiling r)"
5.1778 - unfolding real_of_int_def by (rule le_of_int_ceiling)
5.1779 -
5.1780 -lemma ceiling_real_of_int [simp]: "ceiling (real (n::int)) = n"
5.1781 - unfolding real_of_int_def by simp
5.1782 -
5.1783 -lemma real_of_int_ceiling_cancel [simp]:
5.1784 - "(real (ceiling x) = x) = (\<exists>n::int. x = real n)"
5.1785 - using ceiling_real_of_int by metis
5.1786 -
5.1787 -lemma ceiling_eq: "[| real n < x; x < real n + 1 |] ==> ceiling x = n + 1"
5.1788 - unfolding real_of_int_def using ceiling_unique [of "n + 1" x] by simp
5.1789 -
5.1790 -lemma ceiling_eq2: "[| real n < x; x \<le> real n + 1 |] ==> ceiling x = n + 1"
5.1791 - unfolding real_of_int_def using ceiling_unique [of "n + 1" x] by simp
5.1792 -
5.1793 -lemma ceiling_eq3: "[| real n - 1 < x; x \<le> real n |] ==> ceiling x = n"
5.1794 - unfolding real_of_int_def using ceiling_unique [of n x] by simp
5.1795 -
5.1796 -lemma real_of_int_ceiling_diff_one_le [simp]: "real (ceiling r) - 1 \<le> r"
5.1797 - unfolding real_of_int_def using ceiling_correct [of r] by simp
5.1798 -
5.1799 -lemma real_of_int_ceiling_le_add_one [simp]: "real (ceiling r) \<le> r + 1"
5.1800 - unfolding real_of_int_def using ceiling_correct [of r] by simp
5.1801 -
5.1802 -lemma ceiling_le: "x <= real a ==> ceiling x <= a"
5.1803 - unfolding real_of_int_def by (simp add: ceiling_le_iff)
5.1804 -
5.1805 -lemma ceiling_le_real: "ceiling x <= a ==> x <= real a"
5.1806 - unfolding real_of_int_def by (simp add: ceiling_le_iff)
5.1807 -
5.1808 -lemma ceiling_le_eq: "(ceiling x <= a) = (x <= real a)"
5.1809 - unfolding real_of_int_def by (rule ceiling_le_iff)
5.1810 -
5.1811 -lemma less_ceiling_eq: "(a < ceiling x) = (real a < x)"
5.1812 - unfolding real_of_int_def by (rule less_ceiling_iff)
5.1813 -
5.1814 -lemma ceiling_less_eq: "(ceiling x < a) = (x <= real a - 1)"
5.1815 - unfolding real_of_int_def by (rule ceiling_less_iff)
5.1816 -
5.1817 -lemma le_ceiling_eq: "(a <= ceiling x) = (real a - 1 < x)"
5.1818 - unfolding real_of_int_def by (rule le_ceiling_iff)
5.1819 -
5.1820 -lemma ceiling_add [simp]: "ceiling (x + real a) = ceiling x + a"
5.1821 - unfolding real_of_int_def by (rule ceiling_add_of_int)
5.1822 -
5.1823 -lemma ceiling_subtract [simp]: "ceiling (x - real a) = ceiling x - a"
5.1824 - unfolding real_of_int_def by (rule ceiling_diff_of_int)
5.1825 -
5.1826 -
5.1827 -subsubsection {* Versions for the natural numbers *}
5.1828 -
5.1829 -definition
5.1830 - natfloor :: "real => nat" where
5.1831 - "natfloor x = nat(floor x)"
5.1832 -
5.1833 -definition
5.1834 - natceiling :: "real => nat" where
5.1835 - "natceiling x = nat(ceiling x)"
5.1836 -
5.1837 -lemma natfloor_zero [simp]: "natfloor 0 = 0"
5.1838 - by (unfold natfloor_def, simp)
5.1839 -
5.1840 -lemma natfloor_one [simp]: "natfloor 1 = 1"
5.1841 - by (unfold natfloor_def, simp)
5.1842 -
5.1843 -lemma zero_le_natfloor [simp]: "0 <= natfloor x"
5.1844 - by (unfold natfloor_def, simp)
5.1845 -
5.1846 -lemma natfloor_numeral_eq [simp]: "natfloor (numeral n) = numeral n"
5.1847 - by (unfold natfloor_def, simp)
5.1848 -
5.1849 -lemma natfloor_real_of_nat [simp]: "natfloor(real n) = n"
5.1850 - by (unfold natfloor_def, simp)
5.1851 -
5.1852 -lemma real_natfloor_le: "0 <= x ==> real(natfloor x) <= x"
5.1853 - by (unfold natfloor_def, simp)
5.1854 -
5.1855 -lemma natfloor_neg: "x <= 0 ==> natfloor x = 0"
5.1856 - unfolding natfloor_def by simp
5.1857 -
5.1858 -lemma natfloor_mono: "x <= y ==> natfloor x <= natfloor y"
5.1859 - unfolding natfloor_def by (intro nat_mono floor_mono)
5.1860 -
5.1861 -lemma le_natfloor: "real x <= a ==> x <= natfloor a"
5.1862 - apply (unfold natfloor_def)
5.1863 - apply (subst nat_int [THEN sym])
5.1864 - apply (rule nat_mono)
5.1865 - apply (rule le_floor)
5.1866 - apply simp
5.1867 -done
5.1868 -
5.1869 -lemma natfloor_less_iff: "0 \<le> x \<Longrightarrow> natfloor x < n \<longleftrightarrow> x < real n"
5.1870 - unfolding natfloor_def real_of_nat_def
5.1871 - by (simp add: nat_less_iff floor_less_iff)
5.1872 -
5.1873 -lemma less_natfloor:
5.1874 - assumes "0 \<le> x" and "x < real (n :: nat)"
5.1875 - shows "natfloor x < n"
5.1876 - using assms by (simp add: natfloor_less_iff)
5.1877 -
5.1878 -lemma le_natfloor_eq: "0 <= x ==> (a <= natfloor x) = (real a <= x)"
5.1879 - apply (rule iffI)
5.1880 - apply (rule order_trans)
5.1881 - prefer 2
5.1882 - apply (erule real_natfloor_le)
5.1883 - apply (subst real_of_nat_le_iff)
5.1884 - apply assumption
5.1885 - apply (erule le_natfloor)
5.1886 -done
5.1887 -
5.1888 -lemma le_natfloor_eq_numeral [simp]:
5.1889 - "~ neg((numeral n)::int) ==> 0 <= x ==>
5.1890 - (numeral n <= natfloor x) = (numeral n <= x)"
5.1891 - apply (subst le_natfloor_eq, assumption)
5.1892 - apply simp
5.1893 -done
5.1894 -
5.1895 -lemma le_natfloor_eq_one [simp]: "(1 <= natfloor x) = (1 <= x)"
5.1896 - apply (case_tac "0 <= x")
5.1897 - apply (subst le_natfloor_eq, assumption, simp)
5.1898 - apply (rule iffI)
5.1899 - apply (subgoal_tac "natfloor x <= natfloor 0")
5.1900 - apply simp
5.1901 - apply (rule natfloor_mono)
5.1902 - apply simp
5.1903 - apply simp
5.1904 -done
5.1905 -
5.1906 -lemma natfloor_eq: "real n <= x ==> x < real n + 1 ==> natfloor x = n"
5.1907 - unfolding natfloor_def by (simp add: floor_eq2 [where n="int n"])
5.1908 -
5.1909 -lemma real_natfloor_add_one_gt: "x < real(natfloor x) + 1"
5.1910 - apply (case_tac "0 <= x")
5.1911 - apply (unfold natfloor_def)
5.1912 - apply simp
5.1913 - apply simp_all
5.1914 -done
5.1915 -
5.1916 -lemma real_natfloor_gt_diff_one: "x - 1 < real(natfloor x)"
5.1917 -using real_natfloor_add_one_gt by (simp add: algebra_simps)
5.1918 -
5.1919 -lemma ge_natfloor_plus_one_imp_gt: "natfloor z + 1 <= n ==> z < real n"
5.1920 - apply (subgoal_tac "z < real(natfloor z) + 1")
5.1921 - apply arith
5.1922 - apply (rule real_natfloor_add_one_gt)
5.1923 -done
5.1924 -
5.1925 -lemma natfloor_add [simp]: "0 <= x ==> natfloor (x + real a) = natfloor x + a"
5.1926 - unfolding natfloor_def
5.1927 - unfolding real_of_int_of_nat_eq [symmetric] floor_add
5.1928 - by (simp add: nat_add_distrib)
5.1929 -
5.1930 -lemma natfloor_add_numeral [simp]:
5.1931 - "~neg ((numeral n)::int) ==> 0 <= x ==>
5.1932 - natfloor (x + numeral n) = natfloor x + numeral n"
5.1933 - by (simp add: natfloor_add [symmetric])
5.1934 -
5.1935 -lemma natfloor_add_one: "0 <= x ==> natfloor(x + 1) = natfloor x + 1"
5.1936 - by (simp add: natfloor_add [symmetric] del: One_nat_def)
5.1937 -
5.1938 -lemma natfloor_subtract [simp]:
5.1939 - "natfloor(x - real a) = natfloor x - a"
5.1940 - unfolding natfloor_def real_of_int_of_nat_eq [symmetric] floor_subtract
5.1941 - by simp
5.1942 -
5.1943 -lemma natfloor_div_nat:
5.1944 - assumes "1 <= x" and "y > 0"
5.1945 - shows "natfloor (x / real y) = natfloor x div y"
5.1946 -proof (rule natfloor_eq)
5.1947 - have "(natfloor x) div y * y \<le> natfloor x"
5.1948 - by (rule add_leD1 [where k="natfloor x mod y"], simp)
5.1949 - thus "real (natfloor x div y) \<le> x / real y"
5.1950 - using assms by (simp add: le_divide_eq le_natfloor_eq)
5.1951 - have "natfloor x < (natfloor x) div y * y + y"
5.1952 - apply (subst mod_div_equality [symmetric])
5.1953 - apply (rule add_strict_left_mono)
5.1954 - apply (rule mod_less_divisor)
5.1955 - apply fact
5.1956 - done
5.1957 - thus "x / real y < real (natfloor x div y) + 1"
5.1958 - using assms
5.1959 - by (simp add: divide_less_eq natfloor_less_iff distrib_right)
5.1960 -qed
5.1961 -
5.1962 -lemma le_mult_natfloor:
5.1963 - shows "natfloor a * natfloor b \<le> natfloor (a * b)"
5.1964 - by (cases "0 <= a & 0 <= b")
5.1965 - (auto simp add: le_natfloor_eq mult_nonneg_nonneg mult_mono' real_natfloor_le natfloor_neg)
5.1966 -
5.1967 -lemma natceiling_zero [simp]: "natceiling 0 = 0"
5.1968 - by (unfold natceiling_def, simp)
5.1969 -
5.1970 -lemma natceiling_one [simp]: "natceiling 1 = 1"
5.1971 - by (unfold natceiling_def, simp)
5.1972 -
5.1973 -lemma zero_le_natceiling [simp]: "0 <= natceiling x"
5.1974 - by (unfold natceiling_def, simp)
5.1975 -
5.1976 -lemma natceiling_numeral_eq [simp]: "natceiling (numeral n) = numeral n"
5.1977 - by (unfold natceiling_def, simp)
5.1978 -
5.1979 -lemma natceiling_real_of_nat [simp]: "natceiling(real n) = n"
5.1980 - by (unfold natceiling_def, simp)
5.1981 -
5.1982 -lemma real_natceiling_ge: "x <= real(natceiling x)"
5.1983 - unfolding natceiling_def by (cases "x < 0", simp_all)
5.1984 -
5.1985 -lemma natceiling_neg: "x <= 0 ==> natceiling x = 0"
5.1986 - unfolding natceiling_def by simp
5.1987 -
5.1988 -lemma natceiling_mono: "x <= y ==> natceiling x <= natceiling y"
5.1989 - unfolding natceiling_def by (intro nat_mono ceiling_mono)
5.1990 -
5.1991 -lemma natceiling_le: "x <= real a ==> natceiling x <= a"
5.1992 - unfolding natceiling_def real_of_nat_def
5.1993 - by (simp add: nat_le_iff ceiling_le_iff)
5.1994 -
5.1995 -lemma natceiling_le_eq: "(natceiling x <= a) = (x <= real a)"
5.1996 - unfolding natceiling_def real_of_nat_def
5.1997 - by (simp add: nat_le_iff ceiling_le_iff)
5.1998 -
5.1999 -lemma natceiling_le_eq_numeral [simp]:
5.2000 - "~ neg((numeral n)::int) ==>
5.2001 - (natceiling x <= numeral n) = (x <= numeral n)"
5.2002 - by (simp add: natceiling_le_eq)
5.2003 -
5.2004 -lemma natceiling_le_eq_one: "(natceiling x <= 1) = (x <= 1)"
5.2005 - unfolding natceiling_def
5.2006 - by (simp add: nat_le_iff ceiling_le_iff)
5.2007 -
5.2008 -lemma natceiling_eq: "real n < x ==> x <= real n + 1 ==> natceiling x = n + 1"
5.2009 - unfolding natceiling_def
5.2010 - by (simp add: ceiling_eq2 [where n="int n"])
5.2011 -
5.2012 -lemma natceiling_add [simp]: "0 <= x ==>
5.2013 - natceiling (x + real a) = natceiling x + a"
5.2014 - unfolding natceiling_def
5.2015 - unfolding real_of_int_of_nat_eq [symmetric] ceiling_add
5.2016 - by (simp add: nat_add_distrib)
5.2017 -
5.2018 -lemma natceiling_add_numeral [simp]:
5.2019 - "~ neg ((numeral n)::int) ==> 0 <= x ==>
5.2020 - natceiling (x + numeral n) = natceiling x + numeral n"
5.2021 - by (simp add: natceiling_add [symmetric])
5.2022 -
5.2023 -lemma natceiling_add_one: "0 <= x ==> natceiling(x + 1) = natceiling x + 1"
5.2024 - by (simp add: natceiling_add [symmetric] del: One_nat_def)
5.2025 -
5.2026 -lemma natceiling_subtract [simp]: "natceiling(x - real a) = natceiling x - a"
5.2027 - unfolding natceiling_def real_of_int_of_nat_eq [symmetric] ceiling_subtract
5.2028 - by simp
5.2029 -
5.2030 -subsection {* Exponentiation with floor *}
5.2031 -
5.2032 -lemma floor_power:
5.2033 - assumes "x = real (floor x)"
5.2034 - shows "floor (x ^ n) = floor x ^ n"
5.2035 -proof -
5.2036 - have *: "x ^ n = real (floor x ^ n)"
5.2037 - using assms by (induct n arbitrary: x) simp_all
5.2038 - show ?thesis unfolding real_of_int_inject[symmetric]
5.2039 - unfolding * floor_real_of_int ..
5.2040 -qed
5.2041 -
5.2042 -lemma natfloor_power:
5.2043 - assumes "x = real (natfloor x)"
5.2044 - shows "natfloor (x ^ n) = natfloor x ^ n"
5.2045 -proof -
5.2046 - from assms have "0 \<le> floor x" by auto
5.2047 - note assms[unfolded natfloor_def real_nat_eq_real[OF `0 \<le> floor x`]]
5.2048 - from floor_power[OF this]
5.2049 - show ?thesis unfolding natfloor_def nat_power_eq[OF `0 \<le> floor x`, symmetric]
5.2050 - by simp
5.2051 -qed
5.2052 -
5.2053 -
5.2054 -subsection {* Implementation of rational real numbers *}
5.2055 -
5.2056 -text {* Formal constructor *}
5.2057 -
5.2058 -definition Ratreal :: "rat \<Rightarrow> real" where
5.2059 - [code_abbrev, simp]: "Ratreal = of_rat"
5.2060 -
5.2061 -code_datatype Ratreal
5.2062 -
5.2063 -
5.2064 -text {* Numerals *}
5.2065 -
5.2066 -lemma [code_abbrev]:
5.2067 - "(of_rat (of_int a) :: real) = of_int a"
5.2068 - by simp
5.2069 -
5.2070 -lemma [code_abbrev]:
5.2071 - "(of_rat 0 :: real) = 0"
5.2072 - by simp
5.2073 -
5.2074 -lemma [code_abbrev]:
5.2075 - "(of_rat 1 :: real) = 1"
5.2076 - by simp
5.2077 -
5.2078 -lemma [code_abbrev]:
5.2079 - "(of_rat (numeral k) :: real) = numeral k"
5.2080 - by simp
5.2081 -
5.2082 -lemma [code_abbrev]:
5.2083 - "(of_rat (neg_numeral k) :: real) = neg_numeral k"
5.2084 - by simp
5.2085 -
5.2086 -lemma [code_post]:
5.2087 - "(of_rat (0 / r) :: real) = 0"
5.2088 - "(of_rat (r / 0) :: real) = 0"
5.2089 - "(of_rat (1 / 1) :: real) = 1"
5.2090 - "(of_rat (numeral k / 1) :: real) = numeral k"
5.2091 - "(of_rat (neg_numeral k / 1) :: real) = neg_numeral k"
5.2092 - "(of_rat (1 / numeral k) :: real) = 1 / numeral k"
5.2093 - "(of_rat (1 / neg_numeral k) :: real) = 1 / neg_numeral k"
5.2094 - "(of_rat (numeral k / numeral l) :: real) = numeral k / numeral l"
5.2095 - "(of_rat (numeral k / neg_numeral l) :: real) = numeral k / neg_numeral l"
5.2096 - "(of_rat (neg_numeral k / numeral l) :: real) = neg_numeral k / numeral l"
5.2097 - "(of_rat (neg_numeral k / neg_numeral l) :: real) = neg_numeral k / neg_numeral l"
5.2098 - by (simp_all add: of_rat_divide)
5.2099 -
5.2100 -
5.2101 -text {* Operations *}
5.2102 -
5.2103 -lemma zero_real_code [code]:
5.2104 - "0 = Ratreal 0"
5.2105 -by simp
5.2106 -
5.2107 -lemma one_real_code [code]:
5.2108 - "1 = Ratreal 1"
5.2109 -by simp
5.2110 -
5.2111 -instantiation real :: equal
5.2112 -begin
5.2113 -
5.2114 -definition "HOL.equal (x\<Colon>real) y \<longleftrightarrow> x - y = 0"
5.2115 -
5.2116 -instance proof
5.2117 -qed (simp add: equal_real_def)
5.2118 -
5.2119 -lemma real_equal_code [code]:
5.2120 - "HOL.equal (Ratreal x) (Ratreal y) \<longleftrightarrow> HOL.equal x y"
5.2121 - by (simp add: equal_real_def equal)
5.2122 -
5.2123 -lemma [code nbe]:
5.2124 - "HOL.equal (x::real) x \<longleftrightarrow> True"
5.2125 - by (rule equal_refl)
5.2126 -
5.2127 -end
5.2128 -
5.2129 -lemma real_less_eq_code [code]: "Ratreal x \<le> Ratreal y \<longleftrightarrow> x \<le> y"
5.2130 - by (simp add: of_rat_less_eq)
5.2131 -
5.2132 -lemma real_less_code [code]: "Ratreal x < Ratreal y \<longleftrightarrow> x < y"
5.2133 - by (simp add: of_rat_less)
5.2134 -
5.2135 -lemma real_plus_code [code]: "Ratreal x + Ratreal y = Ratreal (x + y)"
5.2136 - by (simp add: of_rat_add)
5.2137 -
5.2138 -lemma real_times_code [code]: "Ratreal x * Ratreal y = Ratreal (x * y)"
5.2139 - by (simp add: of_rat_mult)
5.2140 -
5.2141 -lemma real_uminus_code [code]: "- Ratreal x = Ratreal (- x)"
5.2142 - by (simp add: of_rat_minus)
5.2143 -
5.2144 -lemma real_minus_code [code]: "Ratreal x - Ratreal y = Ratreal (x - y)"
5.2145 - by (simp add: of_rat_diff)
5.2146 -
5.2147 -lemma real_inverse_code [code]: "inverse (Ratreal x) = Ratreal (inverse x)"
5.2148 - by (simp add: of_rat_inverse)
5.2149 -
5.2150 -lemma real_divide_code [code]: "Ratreal x / Ratreal y = Ratreal (x / y)"
5.2151 - by (simp add: of_rat_divide)
5.2152 -
5.2153 -lemma real_floor_code [code]: "floor (Ratreal x) = floor x"
5.2154 - 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)
5.2155 -
5.2156 -
5.2157 -text {* Quickcheck *}
5.2158 -
5.2159 -definition (in term_syntax)
5.2160 - valterm_ratreal :: "rat \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow> real \<times> (unit \<Rightarrow> Code_Evaluation.term)" where
5.2161 - [code_unfold]: "valterm_ratreal k = Code_Evaluation.valtermify Ratreal {\<cdot>} k"
5.2162 -
5.2163 -notation fcomp (infixl "\<circ>>" 60)
5.2164 -notation scomp (infixl "\<circ>\<rightarrow>" 60)
5.2165 -
5.2166 -instantiation real :: random
5.2167 -begin
5.2168 -
5.2169 -definition
5.2170 - "Quickcheck_Random.random i = Quickcheck_Random.random i \<circ>\<rightarrow> (\<lambda>r. Pair (valterm_ratreal r))"
5.2171 -
5.2172 -instance ..
5.2173 -
5.2174 -end
5.2175 -
5.2176 -no_notation fcomp (infixl "\<circ>>" 60)
5.2177 -no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
5.2178 -
5.2179 -instantiation real :: exhaustive
5.2180 -begin
5.2181 -
5.2182 -definition
5.2183 - "exhaustive_real f d = Quickcheck_Exhaustive.exhaustive (%r. f (Ratreal r)) d"
5.2184 -
5.2185 -instance ..
5.2186 -
5.2187 -end
5.2188 -
5.2189 -instantiation real :: full_exhaustive
5.2190 -begin
5.2191 -
5.2192 -definition
5.2193 - "full_exhaustive_real f d = Quickcheck_Exhaustive.full_exhaustive (%r. f (valterm_ratreal r)) d"
5.2194 -
5.2195 -instance ..
5.2196 -
5.2197 -end
5.2198 -
5.2199 -instantiation real :: narrowing
5.2200 -begin
5.2201 -
5.2202 -definition
5.2203 - "narrowing = Quickcheck_Narrowing.apply (Quickcheck_Narrowing.cons Ratreal) narrowing"
5.2204 -
5.2205 -instance ..
5.2206 -
5.2207 -end
5.2208 -
5.2209 -
5.2210 -subsection {* Setup for Nitpick *}
5.2211 -
5.2212 -declaration {*
5.2213 - Nitpick_HOL.register_frac_type @{type_name real}
5.2214 - [(@{const_name zero_real_inst.zero_real}, @{const_name Nitpick.zero_frac}),
5.2215 - (@{const_name one_real_inst.one_real}, @{const_name Nitpick.one_frac}),
5.2216 - (@{const_name plus_real_inst.plus_real}, @{const_name Nitpick.plus_frac}),
5.2217 - (@{const_name times_real_inst.times_real}, @{const_name Nitpick.times_frac}),
5.2218 - (@{const_name uminus_real_inst.uminus_real}, @{const_name Nitpick.uminus_frac}),
5.2219 - (@{const_name inverse_real_inst.inverse_real}, @{const_name Nitpick.inverse_frac}),
5.2220 - (@{const_name ord_real_inst.less_real}, @{const_name Nitpick.less_frac}),
5.2221 - (@{const_name ord_real_inst.less_eq_real}, @{const_name Nitpick.less_eq_frac})]
5.2222 -*}
5.2223 -
5.2224 -lemmas [nitpick_unfold] = inverse_real_inst.inverse_real one_real_inst.one_real
5.2225 - ord_real_inst.less_real ord_real_inst.less_eq_real plus_real_inst.plus_real
5.2226 - times_real_inst.times_real uminus_real_inst.uminus_real
5.2227 - zero_real_inst.zero_real
5.2228 -
5.2229 -ML_file "Tools/SMT/smt_real.ML"
5.2230 -setup SMT_Real.setup
5.2231 -
5.2232 -end
6.1 --- a/src/HOL/Tools/hologic.ML Tue Mar 26 12:20:56 2013 +0100
6.2 +++ b/src/HOL/Tools/hologic.ML Tue Mar 26 12:20:56 2013 +0100
6.3 @@ -572,7 +572,7 @@
6.4
6.5 (* real *)
6.6
6.7 -val realT = Type ("RealDef.real", []);
6.8 +val realT = Type ("Real.real", []);
6.9
6.10
6.11 (* list *)