--- a/src/HOL/Decision_Procs/Approximation.thy Thu Apr 23 12:17:51 2009 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy Thu Apr 23 12:17:51 2009 +0200
@@ -97,7 +97,7 @@
"(\<Sum>j=0..<n. (1 / real (f (j' + j))) * (Ifloat x ^ j)) \<le> Ifloat (ub n ((F o^ 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.simps uminus_float.simps times_float.simps algebra_simps)
+ by (cases x, cases y, cases z, simp add: plus_float.simps minus_float_def uminus_float.simps 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
@@ -1462,7 +1462,8 @@
finally have "0 < Ifloat ((?horner x) ^ num)" .
}
ultimately show ?thesis
- unfolding lb_exp.simps if_not_P[OF `\<not> 0 < x`] Let_def by (cases "floor_fl x", cases "x < - 1", auto simp add: le_float_def less_float_def normfloat)
+ unfolding lb_exp.simps if_not_P[OF `\<not> 0 < x`] Let_def
+ by (cases "floor_fl x", cases "x < - 1", auto simp add: float_power le_float_def less_float_def)
qed
lemma exp_boundaries': assumes "x \<le> 0"