1.1 --- a/src/HOL/Decision_Procs/Approximation.thy Wed Mar 11 12:51:00 2009 +0100
1.2 +++ b/src/HOL/Decision_Procs/Approximation.thy Wed Mar 11 13:53:51 2009 +0100
1.3 @@ -1,6 +1,4 @@
1.4 -(* Title: HOL/Decision_Procs/Approximation.thy
1.5 - Author: Johannes Hoelzl <hoelzl@in.tum.de> 2008 / 2009
1.6 -*)
1.7 +(* Author: Johannes Hoelzl <hoelzl@in.tum.de> 2008 / 2009 *)
1.8
1.9 header {* Prove unequations about real numbers by computation *}
1.10
1.11 @@ -2408,20 +2406,15 @@
1.12 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)
1.13 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)"
1.14 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)"
1.15 - by (auto simp add: Ifloat.simps pow2_def)
1.16 + and "Ifloat (Float (number_of A) (int B)) = (number_of A) * 2^B"
1.17 + and "Ifloat (Float 1 (int B)) = 2^B"
1.18 + and "Ifloat (Float (number_of A) (- int B)) = (number_of A) / 2^B"
1.19 + and "Ifloat (Float 1 (- int B)) = 1 / 2^B"
1.20 + by (auto simp add: Ifloat.simps pow2_def real_divide_def)
1.21
1.22 lemmas bounded_by_equations = bounded_by_Cons bounded_by_Nil float_power bounded_divl bounded_divr bounded_num HOL.simp_thms
1.23 lemmas uneq_equations = uneq.simps Ifloatarith.simps Ifloatarith_num Ifloatarith_divide Ifloatarith_diff Ifloatarith_tan Ifloatarith_powr Ifloatarith_log
1.24
1.25 -lemma "x div (0::int) = 0" by auto -- "What happens in the zero case for div"
1.26 -lemma "x mod (0::int) = x" by auto -- "What happens in the zero case for mod"
1.27 -
1.28 -text {* The following equations must hold for div & mod
1.29 - -- see "The Definition of Standard ML" by R. Milner, M. Tofte and R. Harper (pg. 79) *}
1.30 -lemma "d * (i div d) + i mod d = (i::int)" by auto
1.31 -lemma "0 < (d :: int) \<Longrightarrow> 0 \<le> i mod d \<and> i mod d < d" by auto
1.32 -lemma "(d :: int) < 0 \<Longrightarrow> d < i mod d \<and> i mod d \<le> 0" by auto
1.33 -
1.34 ML {*
1.35 val uneq_equations = PureThy.get_thms @{theory} "uneq_equations";
1.36 val bounded_by_equations = PureThy.get_thms @{theory} "bounded_by_equations";
1.37 @@ -2438,24 +2431,37 @@
1.38 val to_natc = conv_num @{typ "nat"} #> Thm.cterm_of (ProofContext.theory_of ctxt)
1.39 val to_nat = conv_num @{typ "nat"}
1.40 val to_int = conv_num @{typ "int"}
1.41 + fun int_to_float A = @{term "Float"} $ to_int A $ @{term "0 :: int"}
1.42
1.43 val prec' = to_nat prec
1.44
1.45 fun bot_float (Const (@{const_name "times"}, _) $ mantisse $ (Const (@{const_name "pow2"}, _) $ exp))
1.46 = @{term "Float"} $ to_int mantisse $ to_int exp
1.47 - | bot_float (Const (@{const_name "divide"}, _) $ mantisse $ (Const (@{const_name "power"}, _) $ ten $ exp))
1.48 - = @{term "float_divl"} $ prec' $ (@{term "Float"} $ to_int mantisse $ @{term "0 :: int"}) $ (@{term "power (Float 5 1)"} $ to_nat exp)
1.49 - | bot_float (Const (@{const_name "divide"}, _) $ mantisse $ ten)
1.50 - = @{term "float_divl"} $ prec' $ (@{term "Float"} $ to_int mantisse $ @{term "0 :: int"}) $ @{term "Float 5 1"}
1.51 - | bot_float mantisse = @{term "Float"} $ to_int mantisse $ @{term "0 :: int"}
1.52 + | bot_float (Const (@{const_name "divide"}, _) $ mantisse $ (@{term "power 2 :: nat \<Rightarrow> real"} $ exp))
1.53 + = @{term "Float"} $ to_int mantisse $ (@{term "uminus :: int \<Rightarrow> int"} $ (@{term "int :: nat \<Rightarrow> int"} $ to_nat exp))
1.54 + | bot_float (Const (@{const_name "times"}, _) $ mantisse $ (@{term "power 2 :: nat \<Rightarrow> real"} $ exp))
1.55 + = @{term "Float"} $ to_int mantisse $ (@{term "int :: nat \<Rightarrow> int"} $ to_nat exp)
1.56 + | bot_float (Const (@{const_name "divide"}, _) $ A $ (@{term "power 10 :: nat \<Rightarrow> real"} $ exp))
1.57 + = @{term "float_divl"} $ prec' $ (int_to_float A) $ (@{term "power (Float 5 1)"} $ to_nat exp)
1.58 + | bot_float (Const (@{const_name "divide"}, _) $ A $ B)
1.59 + = @{term "float_divl"} $ prec' $ int_to_float A $ int_to_float B
1.60 + | bot_float (@{term "power 2 :: nat \<Rightarrow> real"} $ exp)
1.61 + = @{term "Float 1"} $ (@{term "int :: nat \<Rightarrow> int"} $ to_nat exp)
1.62 + | bot_float A = int_to_float A
1.63
1.64 fun top_float (Const (@{const_name "times"}, _) $ mantisse $ (Const (@{const_name "pow2"}, _) $ exp))
1.65 = @{term "Float"} $ to_int mantisse $ to_int exp
1.66 - | top_float (Const (@{const_name "divide"}, _) $ mantisse $ (Const (@{const_name "power"}, _) $ ten $ exp))
1.67 - = @{term "float_divr"} $ prec' $ (@{term "Float"} $ to_int mantisse $ @{term "0 :: int"}) $ (@{term "power (Float 5 1)"} $ to_nat exp)
1.68 - | top_float (Const (@{const_name "divide"}, _) $ mantisse $ ten)
1.69 - = @{term "float_divr"} $ prec' $ (@{term "Float"} $ to_int mantisse $ @{term "0 :: int"}) $ @{term "Float 5 1"}
1.70 - | top_float mantisse = @{term "Float"} $ to_int mantisse $ @{term "0 :: int"}
1.71 + | top_float (Const (@{const_name "divide"}, _) $ mantisse $ (@{term "power 2 :: nat \<Rightarrow> real"} $ exp))
1.72 + = @{term "Float"} $ to_int mantisse $ (@{term "uminus :: int \<Rightarrow> int"} $ (@{term "int :: nat \<Rightarrow> int"} $ to_nat exp))
1.73 + | top_float (Const (@{const_name "times"}, _) $ mantisse $ (@{term "power 2 :: nat \<Rightarrow> real"} $ exp))
1.74 + = @{term "Float"} $ to_int mantisse $ (@{term "int :: nat \<Rightarrow> int"} $ to_nat exp)
1.75 + | top_float (Const (@{const_name "divide"}, _) $ A $ (@{term "power 10 :: nat \<Rightarrow> real"} $ exp))
1.76 + = @{term "float_divr"} $ prec' $ (int_to_float A) $ (@{term "power (Float 5 1)"} $ to_nat exp)
1.77 + | top_float (Const (@{const_name "divide"}, _) $ A $ B)
1.78 + = @{term "float_divr"} $ prec' $ int_to_float A $ int_to_float B
1.79 + | top_float (@{term "power 2 :: nat \<Rightarrow> real"} $ exp)
1.80 + = @{term "Float 1"} $ (@{term "int :: nat \<Rightarrow> int"} $ to_nat exp)
1.81 + | top_float A = int_to_float A
1.82
1.83 val goal' : term = List.nth (prems_of thm, i - 1)
1.84
1.85 @@ -2464,7 +2470,7 @@
1.86 bottom $ (Free (name, _))) $
1.87 (Const (@{const_name "less_eq"}, _) $ _ $ top)))
1.88 = ((name, HOLogic.mk_prod (bot_float bottom, top_float top))
1.89 - handle TERM (txt, ts) => raise TERM ("Premisse needs format '<num> <= <var> & <var> <= <num>', but found " ^
1.90 + handle TERM (txt, ts) => raise TERM ("Invalid bound number format: " ^
1.91 (Syntax.string_of_term ctxt t), [t]))
1.92 | lift_bnd t = raise TERM ("Premisse needs format '<num> <= <var> & <var> <= <num>', but found " ^
1.93 (Syntax.string_of_term ctxt t), [t])
1.94 @@ -2501,5 +2507,5 @@
1.95 THEN (gen_eval_tac eval_oracle ctxt) i))
1.96 end)
1.97 *} "real number approximation"
1.98 -
1.99 +
1.100 end