--- a/src/HOL/Decision_Procs/Approximation.thy Wed Jun 08 19:36:45 2016 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy Thu Jun 09 16:04:20 2016 +0200
@@ -1847,7 +1847,7 @@
thus ?thesis unfolding True power_0_left by auto
next
case False hence "real_of_float x < 0" using \<open>real_of_float x \<le> 0\<close> by auto
- show ?thesis by (rule less_imp_le, auto simp add: power_less_zero_eq \<open>real_of_float x < 0\<close>)
+ show ?thesis by (rule less_imp_le, auto simp add: \<open>real_of_float x < 0\<close>)
qed
obtain t where "\<bar>t\<bar> \<le> \<bar>real_of_float x\<bar>"
and "exp x = (\<Sum>m = 0..<get_odd n. (real_of_float x) ^ m / (fact m)) + exp t / (fact (get_odd n)) * (real_of_float x) ^ (get_odd n)"
@@ -2100,7 +2100,7 @@
have "exp x \<le> (1 :: float) / lb_exp prec (-x)"
using lb_exp lb_exp_pos[OF \<open>\<not> 0 < -x\<close>, of prec]
- by (simp del: lb_exp.simps add: exp_minus inverse_eq_divide field_simps)
+ by (simp del: lb_exp.simps add: exp_minus field_simps)
also have "\<dots> \<le> float_divr prec 1 (lb_exp prec (-x))"
using float_divr .
finally show ?thesis
@@ -2550,8 +2550,8 @@
from bitlen_div[OF \<open>0 < m\<close>] float_gt1_scale[OF \<open>1 \<le> Float m e\<close>] \<open>bl \<ge> 0\<close>
have x_bnds: "0 \<le> real_of_float (?x - 1)" "real_of_float (?x - 1) < 1"
unfolding bl_def[symmetric]
- by (auto simp: powr_realpow[symmetric] field_simps inverse_eq_divide)
- (auto simp : powr_minus field_simps inverse_eq_divide)
+ by (auto simp: powr_realpow[symmetric] field_simps)
+ (auto simp : powr_minus field_simps)
{
have "float_round_down prec (lb_ln2 prec * ?s) \<le> ln 2 * (e + (bitlen m - 1))"
@@ -2822,6 +2822,7 @@
| Powr floatarith floatarith
| Ln floatarith
| Power floatarith nat
+ | Floor floatarith
| Var nat
| Num float
@@ -2841,6 +2842,7 @@
"interpret_floatarith (Powr a b) vs = interpret_floatarith a vs powr interpret_floatarith b vs" |
"interpret_floatarith (Ln a) vs = ln (interpret_floatarith a vs)" |
"interpret_floatarith (Power a n) vs = (interpret_floatarith a vs)^n" |
+"interpret_floatarith (Floor a) vs = floor (interpret_floatarith a vs)" |
"interpret_floatarith (Num f) vs = f" |
"interpret_floatarith (Var n) vs = vs ! n"
@@ -2880,6 +2882,10 @@
and "interpret_floatarith (Num (Float (- numeral a) 0)) vs = - numeral a"
by auto
+lemma interpret_floatarith_ceiling:
+ "interpret_floatarith (Minus (Floor (Minus a))) vs = ceiling (interpret_floatarith a vs)"
+ unfolding ceiling_def interpret_floatarith.simps of_int_minus ..
+
subsection "Implement approximation function"
@@ -2960,6 +2966,7 @@
"approx prec (Powr a b) bs = lift_bin (approx' prec a bs) (approx' prec b bs) (bnds_powr prec)" |
"approx prec (Ln a) bs = lift_un (approx' prec a bs) (\<lambda> l u. (lb_ln prec l, ub_ln prec u))" |
"approx prec (Power a n) bs = lift_un' (approx' prec a bs) (float_power_bnds prec n)" |
+"approx prec (Floor a) bs = lift_un' (approx' prec a bs) (\<lambda> l u. (floor_fl l, floor_fl u))" |
"approx prec (Num f) bs = Some (f, f)" |
"approx prec (Var i) bs = (if i < length bs then bs ! i else None)"
@@ -3419,6 +3426,10 @@
case (Power a n)
with lift_un'_bnds[OF bnds_power] show ?case by auto
next
+ case (Floor a)
+ from lift_un'[OF Floor.prems[unfolded approx.simps] Floor.hyps]
+ show ?case by (auto simp: floor_fl.rep_eq floor_mono)
+next
case (Num f)
thus ?case by auto
next
@@ -3621,9 +3632,10 @@
"isDERIV x Pi vs = True" |
"isDERIV x (Sqrt a) vs = (isDERIV x a vs \<and> interpret_floatarith a vs > 0)" |
"isDERIV x (Exp a) vs = isDERIV x a vs" |
-"isDERIV x (Powr a b) vs =
+"isDERIV x (Powr a b) vs =
(isDERIV x a vs \<and> isDERIV x b vs \<and> interpret_floatarith a vs > 0)" |
"isDERIV x (Ln a) vs = (isDERIV x a vs \<and> interpret_floatarith a vs > 0)" |
+"isDERIV x (Floor a) vs = (isDERIV x a vs \<and> interpret_floatarith a vs \<notin> \<int>)" |
"isDERIV x (Power a 0) vs = True" |
"isDERIV x (Power a (Suc n)) vs = isDERIV x a vs" |
"isDERIV x (Num f) vs = True" |
@@ -3647,6 +3659,7 @@
"DERIV_floatarith x (Ln a) = Mult (Inverse a) (DERIV_floatarith x a)" |
"DERIV_floatarith x (Power a 0) = Num 0" |
"DERIV_floatarith x (Power a (Suc n)) = Mult (Num (Float (int (Suc n)) 0)) (Mult (Power a n) (DERIV_floatarith x a))" |
+"DERIV_floatarith x (Floor a) = Num 0" |
"DERIV_floatarith x (Num f) = Num 0" |
"DERIV_floatarith x (Var n) = (if x = n then Num 1 else Num 0)"
@@ -3692,6 +3705,10 @@
thus ?case
by (cases n) (auto intro!: derivative_eq_intros simp del: power_Suc)
next
+ case (Floor a)
+ thus ?case
+ by (auto intro!: derivative_eq_intros DERIV_isCont floor_has_real_derivative)
+next
case (Ln a)
thus ?case by (auto intro!: derivative_eq_intros simp add: divide_inverse)
next
@@ -3726,6 +3743,8 @@
"isDERIV_approx prec x (Ln a) vs =
(isDERIV_approx prec x a vs \<and> (case approx prec a vs of Some (l, u) \<Rightarrow> 0 < l | None \<Rightarrow> False))" |
"isDERIV_approx prec x (Power a 0) vs = True" |
+"isDERIV_approx prec x (Floor a) vs =
+ (isDERIV_approx prec x a vs \<and> (case approx prec a vs of Some (l, u) \<Rightarrow> l > floor u \<and> u < ceiling l | None \<Rightarrow> False))" |
"isDERIV_approx prec x (Power a (Suc n)) vs = isDERIV_approx prec x a vs" |
"isDERIV_approx prec x (Num f) vs = True" |
"isDERIV_approx prec x (Var n) vs = True"
@@ -3769,6 +3788,15 @@
with approx[OF \<open>bounded_by xs vs\<close> a]
have "0 < interpret_floatarith a xs" by auto
with Powr show ?case by auto
+next
+ case (Floor a)
+ then obtain l u where approx_Some: "Some (l, u) = approx prec a vs"
+ and "real_of_int \<lfloor>real_of_float u\<rfloor> < real_of_float l" "real_of_float u < real_of_int \<lceil>real_of_float l\<rceil>"
+ and "isDERIV x a xs"
+ by (cases "approx prec a vs") auto
+ with approx[OF \<open>bounded_by xs vs\<close> approx_Some] le_floor_iff
+ show ?case
+ by (force elim!: Ints_cases)
qed auto
lemma bounded_by_update_var:
@@ -4263,7 +4291,7 @@
lemmas interpret_form_equations = interpret_form.simps interpret_floatarith.simps interpret_floatarith_num
interpret_floatarith_divide interpret_floatarith_diff interpret_floatarith_tan interpret_floatarith_log
- interpret_floatarith_sin
+ interpret_floatarith_sin interpret_floatarith_ceiling
oracle approximation_oracle = \<open>fn (thy, t) =>
let
@@ -4309,6 +4337,7 @@
| floatarith_of_term (@{term Ln} $ a) = @{code Ln} (floatarith_of_term a)
| floatarith_of_term (@{term Power} $ a $ n) =
@{code Power} (floatarith_of_term a, nat_of_term n)
+ | floatarith_of_term (@{term Floor} $ a) = @{code Floor} (floatarith_of_term a)
| floatarith_of_term (@{term Var} $ n) = @{code Var} (nat_of_term n)
| floatarith_of_term (@{term Num} $ m) = @{code Num} (float_of_term m)
| floatarith_of_term t = bad t;
--- a/src/HOL/Decision_Procs/ex/Approximation_Ex.thy Wed Jun 08 19:36:45 2016 +0200
+++ b/src/HOL/Decision_Procs/ex/Approximation_Ex.thy Thu Jun 09 16:04:20 2016 +0200
@@ -67,6 +67,9 @@
lemma "3.2 \<le> (x::real) \<and> x \<le> 6.2 \<Longrightarrow> sin x \<le> 0"
by (approximation 10)
+lemma "3.2 \<le> (x::real) \<and> x \<le> 3.9 \<Longrightarrow> real_of_int (ceiling x) \<in> {4 .. 4}"
+ by (approximation 10)
+
lemma
defines "g \<equiv> 9.80665" and "v \<equiv> 128.61" and "d \<equiv> pi / 180"
shows "g / v * tan (35 * d) \<in> { 3 * d .. 3.1 * d }"
--- a/src/HOL/Deriv.thy Wed Jun 08 19:36:45 2016 +0200
+++ b/src/HOL/Deriv.thy Thu Jun 09 16:04:20 2016 +0200
@@ -931,6 +931,21 @@
by (simp add: DERIV_def filterlim_at_split filterlim_at_left_to_right
tendsto_minus_cancel_left field_simps conj_commute)
+lemma floor_has_real_derivative:
+ fixes f::"real \<Rightarrow> 'a::{floor_ceiling,order_topology}"
+ assumes "isCont f x"
+ assumes "f x \<notin> \<int>"
+ shows "((\<lambda>x. floor (f x)) has_real_derivative 0) (at x)"
+proof (subst DERIV_cong_ev[OF refl _ refl])
+ show "((\<lambda>_. floor (f x)) has_real_derivative 0) (at x)" by simp
+ have "\<forall>\<^sub>F y in at x. \<lfloor>f y\<rfloor> = \<lfloor>f x\<rfloor>"
+ by (rule eventually_floor_eq[OF assms[unfolded continuous_at]])
+ then show "\<forall>\<^sub>F y in nhds x. real_of_int \<lfloor>f y\<rfloor> = real_of_int \<lfloor>f x\<rfloor>"
+ unfolding eventually_at_filter
+ by eventually_elim auto
+qed
+
+
text \<open>Caratheodory formulation of derivative at a point\<close>
lemma CARAT_DERIV: (*FIXME: SUPERSEDED BY THE ONE IN Deriv.thy. But still used by NSA/HDeriv.thy*)
--- a/src/HOL/Limits.thy Wed Jun 08 19:36:45 2016 +0200
+++ b/src/HOL/Limits.thy Thu Jun 09 16:04:20 2016 +0200
@@ -1509,6 +1509,67 @@
qed simp
+subsection \<open>Floor and Ceiling\<close>
+
+lemma eventually_floor_less:
+ fixes f::"'a \<Rightarrow> 'b::{order_topology, floor_ceiling}"
+ assumes f: "(f \<longlongrightarrow> l) F"
+ assumes l: "l \<notin> \<int>"
+ shows "\<forall>\<^sub>F x in F. of_int (floor l) < f x"
+ by (intro order_tendstoD[OF f]) (metis Ints_of_int antisym_conv2 floor_correct l)
+
+lemma eventually_less_ceiling:
+ fixes f::"'a \<Rightarrow> 'b::{order_topology, floor_ceiling}"
+ assumes f: "(f \<longlongrightarrow> l) F"
+ assumes l: "l \<notin> \<int>"
+ shows "\<forall>\<^sub>F x in F. f x < of_int (ceiling l)"
+ by (intro order_tendstoD[OF f]) (metis Ints_of_int l le_of_int_ceiling less_le)
+
+lemma eventually_floor_eq:
+ fixes f::"'a \<Rightarrow> 'b::{order_topology, floor_ceiling}"
+ assumes f: "(f \<longlongrightarrow> l) F"
+ assumes l: "l \<notin> \<int>"
+ shows "\<forall>\<^sub>F x in F. floor (f x) = floor l"
+ using eventually_floor_less[OF assms] eventually_less_ceiling[OF assms]
+ by eventually_elim (meson floor_less_iff less_ceiling_iff not_less_iff_gr_or_eq)
+
+lemma eventually_ceiling_eq:
+ fixes f::"'a \<Rightarrow> 'b::{order_topology, floor_ceiling}"
+ assumes f: "(f \<longlongrightarrow> l) F"
+ assumes l: "l \<notin> \<int>"
+ shows "\<forall>\<^sub>F x in F. ceiling (f x) = ceiling l"
+ using eventually_floor_less[OF assms] eventually_less_ceiling[OF assms]
+ by eventually_elim (meson floor_less_iff less_ceiling_iff not_less_iff_gr_or_eq)
+
+lemma tendsto_of_int_floor:
+ fixes f::"'a \<Rightarrow> 'b::{order_topology, floor_ceiling}"
+ assumes "(f \<longlongrightarrow> l) F"
+ assumes "l \<notin> \<int>"
+ shows "((\<lambda>x. of_int (floor (f x))::'c::{ring_1, topological_space}) \<longlongrightarrow> of_int (floor l)) F"
+ using eventually_floor_eq[OF assms]
+ by (simp add: eventually_mono topological_tendstoI)
+
+lemma tendsto_of_int_ceiling:
+ fixes f::"'a \<Rightarrow> 'b::{order_topology, floor_ceiling}"
+ assumes "(f \<longlongrightarrow> l) F"
+ assumes "l \<notin> \<int>"
+ shows "((\<lambda>x. of_int (ceiling (f x))::'c::{ring_1, topological_space}) \<longlongrightarrow> of_int (ceiling l)) F"
+ using eventually_ceiling_eq[OF assms]
+ by (simp add: eventually_mono topological_tendstoI)
+
+lemma continuous_on_of_int_floor:
+ "continuous_on (UNIV - \<int>::'a::{order_topology, floor_ceiling} set)
+ (\<lambda>x. of_int (floor x)::'b::{ring_1, topological_space})"
+ unfolding continuous_on_def
+ by (auto intro!: tendsto_of_int_floor)
+
+lemma continuous_on_of_int_ceiling:
+ "continuous_on (UNIV - \<int>::'a::{order_topology, floor_ceiling} set)
+ (\<lambda>x. of_int (ceiling x)::'b::{ring_1, topological_space})"
+ unfolding continuous_on_def
+ by (auto intro!: tendsto_of_int_ceiling)
+
+
subsection \<open>Limits of Sequences\<close>
lemma [trans]: "X = Y \<Longrightarrow> Y \<longlonglongrightarrow> z \<Longrightarrow> X \<longlonglongrightarrow> z"