# HG changeset patch # User haftmann # Date 1329081005 -3600 # Node ID 69f45ffd5091a6c84b207dd622a5f56791153832 # Parent 460b0d81d4864590bd946b60ffa5f691c27c1084 tuned diff -r 460b0d81d486 -r 69f45ffd5091 src/HOL/Decision_Procs/Approximation.thy --- a/src/HOL/Decision_Procs/Approximation.thy Sat Feb 11 00:07:28 2012 +0100 +++ b/src/HOL/Decision_Procs/Approximation.thy Sun Feb 12 22:10:05 2012 +0100 @@ -62,7 +62,7 @@ - (x * horner F G n (F ((F ^^ j') s)) (G ((F ^^ j') s) (f j')) x)" unfolding real_of_float_mult neg_le_iff_le by (rule mult_left_mono) qed - moreover have "?horner (Suc n) j' \ ?ub (Suc n) j'" unfolding ub_Suc ub_Suc horner.simps real_of_float_sub diff_minus + moreover have "?horner (Suc n) j' \ ?ub (Suc n) j'" unfolding ub_Suc horner.simps real_of_float_sub diff_minus proof (rule add_mono) show "1 / (f j') \ (rapprox_rat prec 1 (f j'))" using rapprox_rat[of 1 "f j'" prec] by auto from Suc[where j'="Suc j'", unfolded funpow.simps comp_def f_Suc, THEN conjunct1] `0 \ real x` @@ -107,10 +107,10 @@ "(\j=0.. (ub n ((F ^^ j') s) (f j') x)" (is "?ub") proof - { fix x y z :: float have "x - y * z = x + - y * z" - by (cases x, cases y, cases z, simp add: plus_float.simps minus_float_def uminus_float.simps times_float.simps algebra_simps) + by (cases x, cases y, cases z, simp add: plus_float.simps minus_float_def times_float.simps algebra_simps) } note diff_mult_minus = this - { fix x :: float have "- (- x) = x" by (cases x, auto simp add: uminus_float.simps) } note minus_minus = this + { fix x :: float have "- (- x) = x" by (cases x) auto } note minus_minus = this have move_minus: "(-x) = -1 * real x" by auto (* coercion "inside" is necessary *) @@ -245,7 +245,7 @@ proof - from assms have "0 < (b - sqrt x) ^ 2 " by simp also have "\ = b ^ 2 - 2 * b * sqrt x + (sqrt x) ^ 2" by algebra - also have "\ = b ^ 2 - 2 * b * sqrt x + x" using assms by (simp add: real_sqrt_pow2) + also have "\ = b ^ 2 - 2 * b * sqrt x + x" using assms by simp finally have "0 < b ^ 2 - 2 * b * sqrt x + x" by assumption hence "0 < b / 2 - sqrt x + x / (2 * b)" using assms by (simp add: field_simps power2_eq_square) @@ -747,7 +747,7 @@ moreover have "pi / 2 \ ub_pi prec * Float 1 -1" unfolding real_of_float_mult Float_num times_divide_eq_right mult_1_right using pi_boundaries by auto ultimately - show ?thesis unfolding ub_arctan.simps Let_def if_not_P[OF `\ x < 0`] if_not_P[OF `\ x \ Float 1 -1`] if_not_P[OF `\ x \ Float 1 1`] if_not_P[OF False] + show ?thesis unfolding ub_arctan.simps Let_def if_not_P[OF `\ x < 0`]if_not_P[OF `\ x \ Float 1 -1`] if_not_P[OF False] by auto qed qed @@ -1432,7 +1432,7 @@ obtain t where "\t\ \ \real x\" and "exp x = (\m = 0.. exp t / real (fact (get_even n)) * (real x) ^ (get_even n)" - by (auto intro!: mult_nonneg_nonneg divide_nonneg_pos simp add: get_even zero_le_even_power exp_gt_zero) + by (auto intro!: mult_nonneg_nonneg divide_nonneg_pos simp add: zero_le_even_power) ultimately show ?thesis using get_odd exp_gt_zero by (auto intro!: mult_nonneg_nonneg) qed @@ -1446,13 +1446,13 @@ thus ?thesis unfolding True power_0_left by auto next case False hence "real x < 0" using `real x \ 0` by auto - show ?thesis by (rule less_imp_le, auto simp add: power_less_zero_eq get_odd `real x < 0`) + show ?thesis by (rule less_imp_le, auto simp add: power_less_zero_eq `real x < 0`) qed obtain t where "\t\ \ \real x\" and "exp x = (\m = 0.. 0" - by (auto intro!: mult_nonneg_nonpos divide_nonpos_pos simp add: x_less_zero exp_gt_zero) + by (auto intro!: mult_nonneg_nonpos divide_nonpos_pos simp add: x_less_zero) ultimately have "exp x \ (\j = 0.. \ ub_exp_horner prec (get_odd n) 1 1 x" @@ -1591,7 +1591,7 @@ from order_trans[OF exp_m1_ge_quarter this[unfolded exp_le_cancel_iff[where x="- 1", symmetric]]] have "Float 1 -2 \ exp (x / (- floor_fl x))" unfolding Float_num . hence "real (Float 1 -2) ^ ?num \ exp (x / (- floor_fl x)) ^ ?num" - by (auto intro!: power_mono simp add: Float_num) + by (auto intro!: power_mono) also have "\ = exp x" unfolding num_eq exp_real_of_nat_mult[symmetric] using `real (floor_fl x) \ 0` by auto finally show ?thesis unfolding lb_exp.simps if_not_P[OF `\ 0 < x`] if_P[OF `x < - 1`] float.cases Float_floor Let_def if_P[OF True] float_power . @@ -3045,7 +3045,7 @@ then obtain ly uy where *: "approx_tse prec 0 t ((l + u) * Float 1 -1) 1 f [Some (l, u)] = Some (ly, uy)" and **: "cmp ly uy" by (auto elim!: option_caseE) - with 0 show ?case by (auto intro!: exI) + with 0 show ?case by auto next case (Suc s) let ?m = "(l + u) * Float 1 -1" @@ -3350,7 +3350,7 @@ val form_equations = @{thms interpret_form_equations}; fun rewrite_interpret_form_tac ctxt prec splitting taylor i st = let - fun lookup_splitting (Free (name, typ)) + fun lookup_splitting (Free (name, _)) = case AList.lookup (op =) splitting name of SOME s => HOLogic.mk_number @{typ nat} s | NONE => @{term "0 :: nat"} @@ -3395,7 +3395,7 @@ end (* copied from Tools/induct.ML should probably in args.ML *) - val free = Args.context -- Args.term >> (fn (_, Free (n, t)) => n | (ctxt, t) => + val free = Args.context -- Args.term >> (fn (_, Free (n, _)) => n | (ctxt, t) => error ("Bad free variable: " ^ Syntax.string_of_term ctxt t)); *} @@ -3497,11 +3497,11 @@ (@{term "power 10 :: nat \ real"} $ HOLogic.mk_number @{typ nat} (~e)) end) in @{term "atLeastAtMost :: real \ real \ real set"} $ mk_float10 true l $ mk_float10 false u end) - | mk_result prec NONE = @{term "UNIV :: real set"} + | mk_result _ NONE = @{term "UNIV :: real set"} fun realify t = let val t = Logic.varify_global t - val m = map (fn (name, sort) => (name, @{typ real})) (Term.add_tvars t []) + val m = map (fn (name, _) => (name, @{typ real})) (Term.add_tvars t []) val t = Term.subst_TVars m t in t end