# HG changeset patch
# User immler
# Date 1465481060 -7200
# Node ID c6c95d64607a757263108734ba3435d3edcc00b8
# Parent  90a44d2716837bef7fb1579ca17ea8d8c138cc34
approximation, derivative, and continuity of floor and ceiling

diff -r 90a44d271683 -r c6c95d64607a src/HOL/Decision_Procs/Approximation.thy
--- 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;
diff -r 90a44d271683 -r c6c95d64607a src/HOL/Decision_Procs/ex/Approximation_Ex.thy
--- 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 }"
diff -r 90a44d271683 -r c6c95d64607a src/HOL/Deriv.thy
--- 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*)
diff -r 90a44d271683 -r c6c95d64607a src/HOL/Limits.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"