# 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' \<le> ?ub (Suc n) j'" unfolding ub_Suc ub_Suc horner.simps real_of_float_sub diff_minus
+  moreover have "?horner (Suc n) j' \<le> ?ub (Suc n) j'" unfolding ub_Suc horner.simps real_of_float_sub diff_minus
   proof (rule add_mono)
     show "1 / (f j') \<le> (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 \<le> real x`
@@ -107,10 +107,10 @@
     "(\<Sum>j=0..<n. (1 / (f (j' + j))) * real x ^ j) \<le> (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 "\<dots> = b ^ 2 - 2 * b * sqrt x + (sqrt x) ^ 2" by algebra
-  also have "\<dots> = b ^ 2 - 2 * b * sqrt x + x" using assms by (simp add: real_sqrt_pow2)
+  also have "\<dots> = 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 \<le> 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 `\<not> x < 0`] if_not_P[OF `\<not> x \<le> Float 1 -1`] if_not_P[OF `\<not> x \<le> Float 1 1`] if_not_P[OF False]
+      show ?thesis unfolding ub_arctan.simps Let_def if_not_P[OF `\<not> x < 0`]if_not_P[OF `\<not> x \<le> Float 1 -1`] if_not_P[OF False]
         by auto
     qed
   qed
@@ -1432,7 +1432,7 @@
       obtain t where "\<bar>t\<bar> \<le> \<bar>real x\<bar>" and "exp x = (\<Sum>m = 0..<get_even n. real x ^ m / real (fact m)) + exp t / real (fact (get_even n)) * (real x) ^ (get_even n)"
         using Maclaurin_exp_le by blast
       moreover have "0 \<le> 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 \<le> 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 "\<bar>t\<bar> \<le> \<bar>real x\<bar>" and "exp x = (\<Sum>m = 0..<get_odd n. (real x) ^ m / real (fact m)) + exp t / real (fact (get_odd n)) * (real x) ^ (get_odd n)"
       using Maclaurin_exp_le by blast
     moreover have "exp t / real (fact (get_odd n)) * (real x) ^ (get_odd n) \<le> 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 \<le> (\<Sum>j = 0..<get_odd n. 1 / real (fact j) * real x ^ j)"
       using get_odd exp_gt_zero by (auto intro!: mult_nonneg_nonneg)
     also have "\<dots> \<le> 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 \<le> exp (x / (- floor_fl x))" unfolding Float_num .
         hence "real (Float 1 -2) ^ ?num \<le> exp (x / (- floor_fl x)) ^ ?num"
-          by (auto intro!: power_mono simp add: Float_num)
+          by (auto intro!: power_mono)
         also have "\<dots> = exp x" unfolding num_eq exp_real_of_nat_mult[symmetric] using `real (floor_fl x) \<noteq> 0` by auto
         finally show ?thesis
           unfolding lb_exp.simps if_not_P[OF `\<not> 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 \<Rightarrow> real"} $
                                            HOLogic.mk_number @{typ nat} (~e)) end)
       in @{term "atLeastAtMost :: real \<Rightarrow> real \<Rightarrow> 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