author immler Thu, 09 Jun 2016 16:04:20 +0200 changeset 63263 c6c95d64607a parent 63261 90a44d271683 child 63264 6b6f0eb9825b
approximation, derivative, and continuity of floor and ceiling
 src/HOL/Decision_Procs/Approximation.thy file | annotate | diff | comparison | revisions src/HOL/Decision_Procs/ex/Approximation_Ex.thy file | annotate | diff | comparison | revisions src/HOL/Deriv.thy file | annotate | diff | comparison | revisions src/HOL/Limits.thy file | annotate | diff | comparison | revisions
```--- 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"```