author hoelzl Wed, 11 Mar 2009 13:53:51 +0100 changeset 30443 873fa77be5f0 parent 30442 1bc0638d554d child 30444 62139eb64bfe child 30454 c816b6dcc8af
Extended approximation boundaries by fractions and base-2 floating point numbers
```--- a/src/HOL/Decision_Procs/Approximation.thy	Wed Mar 11 12:51:00 2009 +0100
+++ b/src/HOL/Decision_Procs/Approximation.thy	Wed Mar 11 13:53:51 2009 +0100
@@ -1,6 +1,4 @@
-(*  Title:      HOL/Decision_Procs/Approximation.thy
-    Author:     Johannes Hoelzl <hoelzl@in.tum.de> 2008 / 2009
-*)
+(* Author:     Johannes Hoelzl <hoelzl@in.tum.de> 2008 / 2009 *)

@@ -2408,20 +2406,15 @@
lemma bounded_divr: assumes "x \<le> Ifloat a / Ifloat b" shows "x \<le> Ifloat (float_divr p a b)" by (rule order_trans[OF assms _], rule float_divr)
lemma bounded_num: shows "Ifloat (Float 5 1) = 10" and "Ifloat (Float 0 0) = 0" and "Ifloat (Float 1 0) = 1" and "Ifloat (Float (number_of n) 0) = (number_of n)"
and "0 * pow2 e = Ifloat (Float 0 e)" and "1 * pow2 e = Ifloat (Float 1 e)" and "number_of m * pow2 e = Ifloat (Float (number_of m) e)"
-  by (auto simp add: Ifloat.simps pow2_def)
+                     and "Ifloat (Float (number_of A) (int B)) = (number_of A) * 2^B"
+                     and "Ifloat (Float 1 (int B)) = 2^B"
+                     and "Ifloat (Float (number_of A) (- int B)) = (number_of A) / 2^B"
+                     and "Ifloat (Float 1 (- int B)) = 1 / 2^B"
+  by (auto simp add: Ifloat.simps pow2_def real_divide_def)

lemmas bounded_by_equations = bounded_by_Cons bounded_by_Nil float_power bounded_divl bounded_divr bounded_num HOL.simp_thms
lemmas uneq_equations = uneq.simps Ifloatarith.simps Ifloatarith_num Ifloatarith_divide Ifloatarith_diff Ifloatarith_tan Ifloatarith_powr Ifloatarith_log

-lemma "x div (0::int) = 0" by auto -- "What happens in the zero case for div"
-lemma "x mod (0::int) = x" by auto -- "What happens in the zero case for mod"
-
-text {* The following equations must hold for div & mod
-        -- see "The Definition of Standard ML" by R. Milner, M. Tofte and R. Harper (pg. 79) *}
-lemma "d * (i div d) + i mod d = (i::int)" by auto
-lemma "0 < (d :: int) \<Longrightarrow> 0 \<le> i mod d \<and> i mod d < d" by auto
-lemma "(d :: int) < 0 \<Longrightarrow> d < i mod d \<and> i mod d \<le> 0" by auto
-
ML {*
val uneq_equations = PureThy.get_thms @{theory} "uneq_equations";
val bounded_by_equations = PureThy.get_thms @{theory} "bounded_by_equations";
@@ -2438,24 +2431,37 @@
val to_natc = conv_num @{typ "nat"} #> Thm.cterm_of (ProofContext.theory_of ctxt)
val to_nat = conv_num @{typ "nat"}
val to_int = conv_num @{typ "int"}
+    fun int_to_float A = @{term "Float"} \$ to_int A \$ @{term "0 :: int"}

val prec' = to_nat prec

fun bot_float (Const (@{const_name "times"}, _) \$ mantisse \$ (Const (@{const_name "pow2"}, _) \$ exp))
= @{term "Float"} \$ to_int mantisse \$ to_int exp
-      | bot_float (Const (@{const_name "divide"}, _) \$ mantisse \$ (Const (@{const_name "power"}, _) \$ ten \$ exp))
-                   = @{term "float_divl"} \$ prec' \$ (@{term "Float"} \$ to_int mantisse \$ @{term "0 :: int"}) \$ (@{term "power (Float 5 1)"} \$ to_nat exp)
-      | bot_float (Const (@{const_name "divide"}, _) \$ mantisse \$ ten)
-                   = @{term "float_divl"} \$ prec' \$ (@{term "Float"} \$ to_int mantisse \$ @{term "0 :: int"}) \$ @{term "Float 5 1"}
-      | bot_float mantisse = @{term "Float"} \$ to_int mantisse \$ @{term "0 :: int"}
+      | bot_float (Const (@{const_name "divide"}, _) \$ mantisse \$ (@{term "power 2 :: nat \<Rightarrow> real"} \$ exp))
+                   = @{term "Float"} \$ to_int mantisse \$ (@{term "uminus :: int \<Rightarrow> int"} \$ (@{term "int :: nat \<Rightarrow> int"} \$ to_nat exp))
+      | bot_float (Const (@{const_name "times"}, _) \$ mantisse \$ (@{term "power 2 :: nat \<Rightarrow> real"} \$ exp))
+                   = @{term "Float"} \$ to_int mantisse \$ (@{term "int :: nat \<Rightarrow> int"} \$ to_nat exp)
+      | bot_float (Const (@{const_name "divide"}, _) \$ A \$ (@{term "power 10 :: nat \<Rightarrow> real"} \$ exp))
+                   = @{term "float_divl"} \$ prec' \$ (int_to_float A) \$ (@{term "power (Float 5 1)"} \$ to_nat exp)
+      | bot_float (Const (@{const_name "divide"}, _) \$ A \$ B)
+                   = @{term "float_divl"} \$ prec' \$ int_to_float A \$ int_to_float B
+      | bot_float (@{term "power 2 :: nat \<Rightarrow> real"} \$ exp)
+                   = @{term "Float 1"} \$ (@{term "int :: nat \<Rightarrow> int"} \$ to_nat exp)
+      | bot_float A = int_to_float A

fun top_float (Const (@{const_name "times"}, _) \$ mantisse \$ (Const (@{const_name "pow2"}, _) \$ exp))
= @{term "Float"} \$ to_int mantisse \$ to_int exp
-      | top_float (Const (@{const_name "divide"}, _) \$ mantisse \$ (Const (@{const_name "power"}, _) \$ ten \$ exp))
-                   = @{term "float_divr"} \$ prec' \$ (@{term "Float"} \$ to_int mantisse \$ @{term "0 :: int"}) \$ (@{term "power (Float 5 1)"} \$ to_nat exp)
-      | top_float (Const (@{const_name "divide"}, _) \$ mantisse \$ ten)
-                   = @{term "float_divr"} \$ prec' \$ (@{term "Float"} \$ to_int mantisse \$ @{term "0 :: int"}) \$ @{term "Float 5 1"}
-      | top_float mantisse = @{term "Float"} \$ to_int mantisse \$ @{term "0 :: int"}
+      | top_float (Const (@{const_name "divide"}, _) \$ mantisse \$ (@{term "power 2 :: nat \<Rightarrow> real"} \$ exp))
+                   = @{term "Float"} \$ to_int mantisse \$ (@{term "uminus :: int \<Rightarrow> int"} \$ (@{term "int :: nat \<Rightarrow> int"} \$ to_nat exp))
+      | top_float (Const (@{const_name "times"}, _) \$ mantisse \$ (@{term "power 2 :: nat \<Rightarrow> real"} \$ exp))
+                   = @{term "Float"} \$ to_int mantisse \$ (@{term "int :: nat \<Rightarrow> int"} \$ to_nat exp)
+      | top_float (Const (@{const_name "divide"}, _) \$ A \$ (@{term "power 10 :: nat \<Rightarrow> real"} \$ exp))
+                   = @{term "float_divr"} \$ prec' \$ (int_to_float A) \$ (@{term "power (Float 5 1)"} \$ to_nat exp)
+      | top_float (Const (@{const_name "divide"}, _) \$ A \$ B)
+                   = @{term "float_divr"} \$ prec' \$ int_to_float A \$ int_to_float B
+      | top_float (@{term "power 2 :: nat \<Rightarrow> real"} \$ exp)
+                   = @{term "Float 1"} \$ (@{term "int :: nat \<Rightarrow> int"} \$ to_nat exp)
+      | top_float A = int_to_float A

val goal' : term = List.nth (prems_of thm, i - 1)

@@ -2464,7 +2470,7 @@
bottom \$ (Free (name, _))) \$
(Const (@{const_name "less_eq"}, _) \$ _ \$ top)))
= ((name, HOLogic.mk_prod (bot_float bottom, top_float top))
-            handle TERM (txt, ts) => raise TERM ("Premisse needs format '<num> <= <var> & <var> <= <num>', but found " ^
+            handle TERM (txt, ts) => raise TERM ("Invalid bound number format: " ^
(Syntax.string_of_term ctxt t), [t]))
| lift_bnd t = raise TERM ("Premisse needs format '<num> <= <var> & <var> <= <num>', but found " ^
(Syntax.string_of_term ctxt t), [t])
@@ -2501,5 +2507,5 @@
THEN (gen_eval_tac eval_oracle ctxt) i))
end)
*} "real number approximation"
-
+
end```
```--- a/src/HOL/Decision_Procs/ex/Approximation_Ex.thy	Wed Mar 11 12:51:00 2009 +0100
+++ b/src/HOL/Decision_Procs/ex/Approximation_Ex.thy	Wed Mar 11 13:53:51 2009 +0100
@@ -1,6 +1,4 @@
-(*  Title:      HOL/ex/ApproximationEx.thy
-    Author:     Johannes Hoelzl <hoelzl@in.tum.de> 2009
-*)
+(* Author:     Johannes Hoelzl <hoelzl@in.tum.de> 2009 *)

theory Approximation_Ex
imports Complex_Main "~~/src/HOL/Decision_Procs/Approximation"
@@ -42,7 +40,7 @@
lemma "0.49 \<le> x \<and> x \<le> 4.49 \<Longrightarrow> \<bar> arctan x - 0.91 \<bar> < 0.455"
by (approximation 20)

-lemma "1 * pow2 -1 \<le> x \<and> x \<le> 9 * pow2 -1 \<Longrightarrow> \<bar> arctan x - 0.91 \<bar> < 0.455"
+lemma "1 / 2^1 \<le> x \<and> x \<le> 9 / 2^1 \<Longrightarrow> \<bar> arctan x - 0.91 \<bar> < 0.455"
by (approximation 10)

lemma "0 \<le> x \<and> x \<le> 1 \<Longrightarrow> 0 \<le> sin x"```