4386 "x / y = x * inverse y" |
4386 "x / y = x * inverse y" |
4387 "ceiling x = - floor (- x)" |
4387 "ceiling x = - floor (- x)" |
4388 "log x y = ln y * inverse (ln x)" |
4388 "log x y = ln y * inverse (ln x)" |
4389 "sin x = cos (pi / 2 - x)" |
4389 "sin x = cos (pi / 2 - x)" |
4390 "tan x = sin x / cos x" |
4390 "tan x = sin x / cos x" |
|
4391 by (simp_all add: inverse_eq_divide ceiling_def log_def sin_cos_eq tan_def real_of_float_eq) |
|
4392 |
|
4393 lemma approximation_preproc_int[approximation_preproc]: |
|
4394 "real_of_int 0 = real_of_float 0" |
|
4395 "real_of_int 1 = real_of_float 1" |
|
4396 "real_of_int (i + j) = real_of_int i + real_of_int j" |
4391 "real_of_int (- i) = - real_of_int i" |
4397 "real_of_int (- i) = - real_of_int i" |
4392 by (simp_all add: inverse_eq_divide ceiling_def log_def sin_cos_eq tan_def real_of_float_eq) |
4398 "real_of_int (i - j) = real_of_int i - real_of_int j" |
|
4399 "real_of_int (i * j) = real_of_int i * real_of_int j" |
|
4400 "real_of_int (i div j) = real_of_int (floor (real_of_int i / real_of_int j))" |
|
4401 "real_of_int (min i j) = min (real_of_int i) (real_of_int j)" |
|
4402 "real_of_int (max i j) = max (real_of_int i) (real_of_int j)" |
|
4403 "real_of_int (abs i) = abs (real_of_int i)" |
|
4404 "real_of_int (i ^ n) = (real_of_int i) ^ n" |
|
4405 "real_of_int (numeral a) = real_of_float (numeral a)" |
|
4406 "i mod j = i - i div j * j" |
|
4407 "i = j \<longleftrightarrow> real_of_int i = real_of_int j" |
|
4408 "i \<le> j \<longleftrightarrow> real_of_int i \<le> real_of_int j" |
|
4409 "i < j \<longleftrightarrow> real_of_int i < real_of_int j" |
|
4410 "i \<in> {j .. k} \<longleftrightarrow> real_of_int i \<in> {real_of_int j .. real_of_int k}" |
|
4411 by (simp_all add: floor_divide_of_int_eq zmod_zdiv_equality') |
|
4412 |
|
4413 lemma approximation_preproc_nat[approximation_preproc]: |
|
4414 "real 0 = real_of_float 0" |
|
4415 "real 1 = real_of_float 1" |
|
4416 "real (i + j) = real i + real j" |
|
4417 "real (i - j) = max (real i - real j) 0" |
|
4418 "real (i * j) = real i * real j" |
|
4419 "real (i div j) = real_of_int (floor (real i / real j))" |
|
4420 "real (min i j) = min (real i) (real j)" |
|
4421 "real (max i j) = max (real i) (real j)" |
|
4422 "real (i ^ n) = (real i) ^ n" |
|
4423 "real (numeral a) = real_of_float (numeral a)" |
|
4424 "i mod j = i - i div j * j" |
|
4425 "n = m \<longleftrightarrow> real n = real m" |
|
4426 "n \<le> m \<longleftrightarrow> real n \<le> real m" |
|
4427 "n < m \<longleftrightarrow> real n < real m" |
|
4428 "n \<in> {m .. l} \<longleftrightarrow> real n \<in> {real m .. real l}" |
|
4429 by (simp_all add: real_div_nat_eq_floor_of_divide mod_div_equality') |
4393 |
4430 |
4394 ML_file "approximation.ML" |
4431 ML_file "approximation.ML" |
4395 |
4432 |
4396 method_setup approximation = \<open> |
4433 method_setup approximation = \<open> |
4397 let |
4434 let |