author immler Wed, 21 Sep 2016 17:56:25 +0200 changeset 63931 f17a1c60ac39 parent 63930 867ca0d92ea2 child 63937 45ed7d0aeb6f
approximation: preprocessing for nat/int expressions
```--- a/src/HOL/Decision_Procs/Approximation.thy	Wed Sep 21 17:56:25 2016 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy	Wed Sep 21 17:56:25 2016 +0200
@@ -4388,8 +4388,45 @@
"log x y = ln y * inverse (ln x)"
"sin x = cos (pi / 2 - x)"
"tan x = sin x / cos x"
+  by (simp_all add: inverse_eq_divide ceiling_def log_def sin_cos_eq tan_def real_of_float_eq)
+
+lemma approximation_preproc_int[approximation_preproc]:
+  "real_of_int 0 = real_of_float 0"
+  "real_of_int 1 = real_of_float 1"
+  "real_of_int (i + j) = real_of_int i + real_of_int j"
"real_of_int (- i) = - real_of_int i"
-  by (simp_all add: inverse_eq_divide ceiling_def log_def sin_cos_eq tan_def real_of_float_eq)
+  "real_of_int (i - j) = real_of_int i - real_of_int j"
+  "real_of_int (i * j) = real_of_int i * real_of_int j"
+  "real_of_int (i div j) = real_of_int (floor (real_of_int i / real_of_int j))"
+  "real_of_int (min i j) = min (real_of_int i) (real_of_int j)"
+  "real_of_int (max i j) = max (real_of_int i) (real_of_int j)"
+  "real_of_int (abs i) = abs (real_of_int i)"
+  "real_of_int (i ^ n) = (real_of_int i) ^ n"
+  "real_of_int (numeral a) = real_of_float (numeral a)"
+  "i mod j = i - i div j * j"
+  "i = j \<longleftrightarrow> real_of_int i = real_of_int j"
+  "i \<le> j \<longleftrightarrow> real_of_int i \<le> real_of_int j"
+  "i < j \<longleftrightarrow> real_of_int i < real_of_int j"
+  "i \<in> {j .. k} \<longleftrightarrow> real_of_int i \<in> {real_of_int j .. real_of_int k}"
+  by (simp_all add: floor_divide_of_int_eq zmod_zdiv_equality')
+
+lemma approximation_preproc_nat[approximation_preproc]:
+  "real 0 = real_of_float 0"
+  "real 1 = real_of_float 1"
+  "real (i + j) = real i + real j"
+  "real (i - j) = max (real i - real j) 0"
+  "real (i * j) = real i * real j"
+  "real (i div j) = real_of_int (floor (real i / real j))"
+  "real (min i j) = min (real i) (real j)"
+  "real (max i j) = max (real i) (real j)"
+  "real (i ^ n) = (real i) ^ n"
+  "real (numeral a) = real_of_float (numeral a)"
+  "i mod j = i - i div j * j"
+  "n = m \<longleftrightarrow> real n = real m"
+  "n \<le> m \<longleftrightarrow> real n \<le> real m"
+  "n < m \<longleftrightarrow> real n < real m"
+  "n \<in> {m .. l} \<longleftrightarrow> real n \<in> {real m .. real l}"
+  by (simp_all add: real_div_nat_eq_floor_of_divide mod_div_equality')

ML_file "approximation.ML"
```
```--- a/src/HOL/Decision_Procs/approximation_generator.ML	Wed Sep 21 17:56:25 2016 +0200
+++ b/src/HOL/Decision_Procs/approximation_generator.ML	Wed Sep 21 17:56:25 2016 +0200
@@ -55,6 +55,7 @@
| mapprox_floatarith (@{term Ln} \$ a) xs = Math.ln (mapprox_floatarith a xs)
| mapprox_floatarith (@{term Power} \$ a \$ n) xs =
Math.pow (mapprox_floatarith a xs, Real.fromInt (nat_of_term n))
+  | mapprox_floatarith (@{term Floor} \$ a) xs = Real.fromInt (floor (mapprox_floatarith a xs))
| mapprox_floatarith (@{term Var} \$ n) xs = nth xs (nat_of_term n)
| mapprox_floatarith (@{term Num} \$ m) _ = mapprox_float m
| mapprox_floatarith t _ = raise TERM ("mapprox_floatarith", [t])
@@ -130,7 +131,13 @@
(map (fn t => mk_Some @{typ "float * float"} \$ HOLogic.mk_prod (t, t)) ts)) \$
@{term "[] :: nat list"}
in
-    (if mapprox_form eps e (map (real_of_Float o fst) rs)
+    (if
+      mapprox_form eps e (map (real_of_Float o fst) rs)
+      handle
+        General.Overflow => false
+      | General.Domain => false
+      | General.Div => false
+      | IEEEReal.Unordered => false
then
let
val ts = map (fn x => snd x ()) rs```
```--- a/src/HOL/Decision_Procs/ex/Approximation_Ex.thy	Wed Sep 21 17:56:25 2016 +0200
+++ b/src/HOL/Decision_Procs/ex/Approximation_Ex.thy	Wed Sep 21 17:56:25 2016 +0200
@@ -78,6 +78,10 @@
lemma "x \<in> { 0 .. 1 :: real } \<longrightarrow> x\<^sup>2 \<le> x"
by (approximation 30 splitting: x=1 taylor: x = 3)

-approximate "10"
+lemma "(n::real) \<in> {32 .. 62} \<Longrightarrow> \<lceil>log 2 (2 * (\<lfloor>n\<rfloor> div 2) + 1)\<rceil> = \<lceil>log 2 (\<lfloor>n\<rfloor> + 1)\<rceil>"
+  unfolding eq_iff
+  by (approximation 20)
+
+approximate 10

end```