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