approximation, derivative, and continuity of floor and ceiling
authorimmler
Thu Jun 09 16:04:20 2016 +0200 (2016-06-09)
changeset 63263c6c95d64607a
parent 63261 90a44d271683
child 63264 6b6f0eb9825b
approximation, derivative, and continuity of floor and ceiling
src/HOL/Decision_Procs/Approximation.thy
src/HOL/Decision_Procs/ex/Approximation_Ex.thy
src/HOL/Deriv.thy
src/HOL/Limits.thy
     1.1 --- a/src/HOL/Decision_Procs/Approximation.thy	Wed Jun 08 19:36:45 2016 +0200
     1.2 +++ b/src/HOL/Decision_Procs/Approximation.thy	Thu Jun 09 16:04:20 2016 +0200
     1.3 @@ -1847,7 +1847,7 @@
     1.4        thus ?thesis unfolding True power_0_left by auto
     1.5      next
     1.6        case False hence "real_of_float x < 0" using \<open>real_of_float x \<le> 0\<close> by auto
     1.7 -      show ?thesis by (rule less_imp_le, auto simp add: power_less_zero_eq \<open>real_of_float x < 0\<close>)
     1.8 +      show ?thesis by (rule less_imp_le, auto simp add: \<open>real_of_float x < 0\<close>)
     1.9      qed
    1.10      obtain t where "\<bar>t\<bar> \<le> \<bar>real_of_float x\<bar>"
    1.11        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)"
    1.12 @@ -2100,7 +2100,7 @@
    1.13  
    1.14        have "exp x \<le> (1 :: float) / lb_exp prec (-x)"
    1.15          using lb_exp lb_exp_pos[OF \<open>\<not> 0 < -x\<close>, of prec]
    1.16 -        by (simp del: lb_exp.simps add: exp_minus inverse_eq_divide field_simps)
    1.17 +        by (simp del: lb_exp.simps add: exp_minus field_simps)
    1.18        also have "\<dots> \<le> float_divr prec 1 (lb_exp prec (-x))"
    1.19          using float_divr .
    1.20        finally show ?thesis
    1.21 @@ -2550,8 +2550,8 @@
    1.22      from bitlen_div[OF \<open>0 < m\<close>] float_gt1_scale[OF \<open>1 \<le> Float m e\<close>] \<open>bl \<ge> 0\<close>
    1.23      have x_bnds: "0 \<le> real_of_float (?x - 1)" "real_of_float (?x - 1) < 1"
    1.24        unfolding bl_def[symmetric]
    1.25 -      by (auto simp: powr_realpow[symmetric] field_simps inverse_eq_divide)
    1.26 -         (auto simp : powr_minus field_simps inverse_eq_divide)
    1.27 +      by (auto simp: powr_realpow[symmetric] field_simps)
    1.28 +         (auto simp : powr_minus field_simps)
    1.29  
    1.30      {
    1.31        have "float_round_down prec (lb_ln2 prec * ?s) \<le> ln 2 * (e + (bitlen m - 1))"
    1.32 @@ -2822,6 +2822,7 @@
    1.33    | Powr floatarith floatarith
    1.34    | Ln floatarith
    1.35    | Power floatarith nat
    1.36 +  | Floor floatarith
    1.37    | Var nat
    1.38    | Num float
    1.39  
    1.40 @@ -2841,6 +2842,7 @@
    1.41  "interpret_floatarith (Powr a b) vs   = interpret_floatarith a vs powr interpret_floatarith b vs" |
    1.42  "interpret_floatarith (Ln a) vs       = ln (interpret_floatarith a vs)" |
    1.43  "interpret_floatarith (Power a n) vs  = (interpret_floatarith a vs)^n" |
    1.44 +"interpret_floatarith (Floor a) vs      = floor (interpret_floatarith a vs)" |
    1.45  "interpret_floatarith (Num f) vs      = f" |
    1.46  "interpret_floatarith (Var n) vs     = vs ! n"
    1.47  
    1.48 @@ -2880,6 +2882,10 @@
    1.49      and "interpret_floatarith (Num (Float (- numeral a) 0)) vs = - numeral a"
    1.50    by auto
    1.51  
    1.52 +lemma interpret_floatarith_ceiling:
    1.53 +  "interpret_floatarith (Minus (Floor (Minus a))) vs = ceiling (interpret_floatarith a vs)"
    1.54 +  unfolding ceiling_def interpret_floatarith.simps of_int_minus ..
    1.55 +
    1.56  
    1.57  subsection "Implement approximation function"
    1.58  
    1.59 @@ -2960,6 +2966,7 @@
    1.60  "approx prec (Powr a b) bs  = lift_bin (approx' prec a bs) (approx' prec b bs) (bnds_powr prec)" |
    1.61  "approx prec (Ln a) bs      = lift_un (approx' prec a bs) (\<lambda> l u. (lb_ln prec l, ub_ln prec u))" |
    1.62  "approx prec (Power a n) bs = lift_un' (approx' prec a bs) (float_power_bnds prec n)" |
    1.63 +"approx prec (Floor a) bs = lift_un' (approx' prec a bs) (\<lambda> l u. (floor_fl l, floor_fl u))" |
    1.64  "approx prec (Num f) bs     = Some (f, f)" |
    1.65  "approx prec (Var i) bs    = (if i < length bs then bs ! i else None)"
    1.66  
    1.67 @@ -3419,6 +3426,10 @@
    1.68    case (Power a n)
    1.69    with lift_un'_bnds[OF bnds_power] show ?case by auto
    1.70  next
    1.71 +  case (Floor a)
    1.72 +  from lift_un'[OF Floor.prems[unfolded approx.simps] Floor.hyps]
    1.73 +  show ?case by (auto simp: floor_fl.rep_eq floor_mono)
    1.74 +next
    1.75    case (Num f)
    1.76    thus ?case by auto
    1.77  next
    1.78 @@ -3621,9 +3632,10 @@
    1.79  "isDERIV x Pi vs                = True" |
    1.80  "isDERIV x (Sqrt a) vs          = (isDERIV x a vs \<and> interpret_floatarith a vs > 0)" |
    1.81  "isDERIV x (Exp a) vs           = isDERIV x a vs" |
    1.82 -"isDERIV x (Powr a b) vs        = 
    1.83 +"isDERIV x (Powr a b) vs        =
    1.84      (isDERIV x a vs \<and> isDERIV x b vs \<and> interpret_floatarith a vs > 0)" |
    1.85  "isDERIV x (Ln a) vs            = (isDERIV x a vs \<and> interpret_floatarith a vs > 0)" |
    1.86 +"isDERIV x (Floor a) vs         = (isDERIV x a vs \<and> interpret_floatarith a vs \<notin> \<int>)" |
    1.87  "isDERIV x (Power a 0) vs       = True" |
    1.88  "isDERIV x (Power a (Suc n)) vs = isDERIV x a vs" |
    1.89  "isDERIV x (Num f) vs           = True" |
    1.90 @@ -3647,6 +3659,7 @@
    1.91  "DERIV_floatarith x (Ln a)            = Mult (Inverse a) (DERIV_floatarith x a)" |
    1.92  "DERIV_floatarith x (Power a 0)       = Num 0" |
    1.93  "DERIV_floatarith x (Power a (Suc n)) = Mult (Num (Float (int (Suc n)) 0)) (Mult (Power a n) (DERIV_floatarith x a))" |
    1.94 +"DERIV_floatarith x (Floor a)         = Num 0" |
    1.95  "DERIV_floatarith x (Num f)           = Num 0" |
    1.96  "DERIV_floatarith x (Var n)          = (if x = n then Num 1 else Num 0)"
    1.97  
    1.98 @@ -3692,6 +3705,10 @@
    1.99    thus ?case
   1.100      by (cases n) (auto intro!: derivative_eq_intros simp del: power_Suc)
   1.101  next
   1.102 +  case (Floor a)
   1.103 +  thus ?case
   1.104 +    by (auto intro!: derivative_eq_intros DERIV_isCont floor_has_real_derivative)
   1.105 +next
   1.106    case (Ln a)
   1.107    thus ?case by (auto intro!: derivative_eq_intros simp add: divide_inverse)
   1.108  next
   1.109 @@ -3726,6 +3743,8 @@
   1.110  "isDERIV_approx prec x (Ln a) vs            =
   1.111    (isDERIV_approx prec x a vs \<and> (case approx prec a vs of Some (l, u) \<Rightarrow> 0 < l | None \<Rightarrow> False))" |
   1.112  "isDERIV_approx prec x (Power a 0) vs       = True" |
   1.113 +"isDERIV_approx prec x (Floor a) vs         =
   1.114 +  (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))" |
   1.115  "isDERIV_approx prec x (Power a (Suc n)) vs = isDERIV_approx prec x a vs" |
   1.116  "isDERIV_approx prec x (Num f) vs           = True" |
   1.117  "isDERIV_approx prec x (Var n) vs           = True"
   1.118 @@ -3769,6 +3788,15 @@
   1.119    with approx[OF \<open>bounded_by xs vs\<close> a]
   1.120      have "0 < interpret_floatarith a xs" by auto
   1.121    with Powr show ?case by auto
   1.122 +next
   1.123 +  case (Floor a)
   1.124 +  then obtain l u where approx_Some: "Some (l, u) = approx prec a vs"
   1.125 +    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>"
   1.126 +    and "isDERIV x a xs"
   1.127 +    by (cases "approx prec a vs") auto
   1.128 +  with approx[OF \<open>bounded_by xs vs\<close> approx_Some] le_floor_iff
   1.129 +  show ?case
   1.130 +    by (force elim!: Ints_cases)
   1.131  qed auto
   1.132  
   1.133  lemma bounded_by_update_var:
   1.134 @@ -4263,7 +4291,7 @@
   1.135  
   1.136  lemmas interpret_form_equations = interpret_form.simps interpret_floatarith.simps interpret_floatarith_num
   1.137    interpret_floatarith_divide interpret_floatarith_diff interpret_floatarith_tan interpret_floatarith_log
   1.138 -  interpret_floatarith_sin
   1.139 +  interpret_floatarith_sin interpret_floatarith_ceiling
   1.140  
   1.141  oracle approximation_oracle = \<open>fn (thy, t) =>
   1.142  let
   1.143 @@ -4309,6 +4337,7 @@
   1.144      | floatarith_of_term (@{term Ln} $ a) = @{code Ln} (floatarith_of_term a)
   1.145      | floatarith_of_term (@{term Power} $ a $ n) =
   1.146          @{code Power} (floatarith_of_term a, nat_of_term n)
   1.147 +    | floatarith_of_term (@{term Floor} $ a) = @{code Floor} (floatarith_of_term a)
   1.148      | floatarith_of_term (@{term Var} $ n) = @{code Var} (nat_of_term n)
   1.149      | floatarith_of_term (@{term Num} $ m) = @{code Num} (float_of_term m)
   1.150      | floatarith_of_term t = bad t;
     2.1 --- a/src/HOL/Decision_Procs/ex/Approximation_Ex.thy	Wed Jun 08 19:36:45 2016 +0200
     2.2 +++ b/src/HOL/Decision_Procs/ex/Approximation_Ex.thy	Thu Jun 09 16:04:20 2016 +0200
     2.3 @@ -67,6 +67,9 @@
     2.4  lemma "3.2 \<le> (x::real) \<and> x \<le> 6.2 \<Longrightarrow> sin x \<le> 0"
     2.5    by (approximation 10)
     2.6  
     2.7 +lemma "3.2 \<le> (x::real) \<and> x \<le> 3.9 \<Longrightarrow> real_of_int (ceiling x) \<in> {4 .. 4}"
     2.8 +  by (approximation 10)
     2.9 +
    2.10  lemma
    2.11    defines "g \<equiv> 9.80665" and "v \<equiv> 128.61" and "d \<equiv> pi / 180"
    2.12    shows "g / v * tan (35 * d) \<in> { 3 * d .. 3.1 * d }"
     3.1 --- a/src/HOL/Deriv.thy	Wed Jun 08 19:36:45 2016 +0200
     3.2 +++ b/src/HOL/Deriv.thy	Thu Jun 09 16:04:20 2016 +0200
     3.3 @@ -931,6 +931,21 @@
     3.4    by (simp add: DERIV_def filterlim_at_split filterlim_at_left_to_right
     3.5                  tendsto_minus_cancel_left field_simps conj_commute)
     3.6  
     3.7 +lemma floor_has_real_derivative:
     3.8 +  fixes f::"real \<Rightarrow> 'a::{floor_ceiling,order_topology}"
     3.9 +  assumes "isCont f x"
    3.10 +  assumes "f x \<notin> \<int>"
    3.11 +  shows "((\<lambda>x. floor (f x)) has_real_derivative 0) (at x)"
    3.12 +proof (subst DERIV_cong_ev[OF refl _ refl])
    3.13 +  show "((\<lambda>_. floor (f x)) has_real_derivative 0) (at x)" by simp
    3.14 +  have "\<forall>\<^sub>F y in at x. \<lfloor>f y\<rfloor> = \<lfloor>f x\<rfloor>"
    3.15 +    by (rule eventually_floor_eq[OF assms[unfolded continuous_at]])
    3.16 +  then show "\<forall>\<^sub>F y in nhds x. real_of_int \<lfloor>f y\<rfloor> = real_of_int \<lfloor>f x\<rfloor>"
    3.17 +    unfolding eventually_at_filter
    3.18 +    by eventually_elim auto
    3.19 +qed
    3.20 +
    3.21 +
    3.22  text \<open>Caratheodory formulation of derivative at a point\<close>
    3.23  
    3.24  lemma CARAT_DERIV: (*FIXME: SUPERSEDED BY THE ONE IN Deriv.thy. But still used by NSA/HDeriv.thy*)
     4.1 --- a/src/HOL/Limits.thy	Wed Jun 08 19:36:45 2016 +0200
     4.2 +++ b/src/HOL/Limits.thy	Thu Jun 09 16:04:20 2016 +0200
     4.3 @@ -1509,6 +1509,67 @@
     4.4  qed simp
     4.5  
     4.6  
     4.7 +subsection \<open>Floor and Ceiling\<close>
     4.8 +
     4.9 +lemma eventually_floor_less:
    4.10 +  fixes f::"'a \<Rightarrow> 'b::{order_topology, floor_ceiling}"
    4.11 +  assumes f: "(f \<longlongrightarrow> l) F"
    4.12 +  assumes l: "l \<notin> \<int>"
    4.13 +  shows "\<forall>\<^sub>F x in F. of_int (floor l) < f x"
    4.14 +  by (intro order_tendstoD[OF f]) (metis Ints_of_int antisym_conv2 floor_correct l)
    4.15 +
    4.16 +lemma eventually_less_ceiling:
    4.17 +  fixes f::"'a \<Rightarrow> 'b::{order_topology, floor_ceiling}"
    4.18 +  assumes f: "(f \<longlongrightarrow> l) F"
    4.19 +  assumes l: "l \<notin> \<int>"
    4.20 +  shows "\<forall>\<^sub>F x in F. f x < of_int (ceiling l)"
    4.21 +  by (intro order_tendstoD[OF f]) (metis Ints_of_int l le_of_int_ceiling less_le)
    4.22 +
    4.23 +lemma eventually_floor_eq:
    4.24 +  fixes f::"'a \<Rightarrow> 'b::{order_topology, floor_ceiling}"
    4.25 +  assumes f: "(f \<longlongrightarrow> l) F"
    4.26 +  assumes l: "l \<notin> \<int>"
    4.27 +  shows "\<forall>\<^sub>F x in F. floor (f x) = floor l"
    4.28 +  using eventually_floor_less[OF assms] eventually_less_ceiling[OF assms]
    4.29 +  by eventually_elim (meson floor_less_iff less_ceiling_iff not_less_iff_gr_or_eq)
    4.30 +
    4.31 +lemma eventually_ceiling_eq:
    4.32 +  fixes f::"'a \<Rightarrow> 'b::{order_topology, floor_ceiling}"
    4.33 +  assumes f: "(f \<longlongrightarrow> l) F"
    4.34 +  assumes l: "l \<notin> \<int>"
    4.35 +  shows "\<forall>\<^sub>F x in F. ceiling (f x) = ceiling l"
    4.36 +  using eventually_floor_less[OF assms] eventually_less_ceiling[OF assms]
    4.37 +  by eventually_elim (meson floor_less_iff less_ceiling_iff not_less_iff_gr_or_eq)
    4.38 +
    4.39 +lemma tendsto_of_int_floor:
    4.40 +  fixes f::"'a \<Rightarrow> 'b::{order_topology, floor_ceiling}"
    4.41 +  assumes "(f \<longlongrightarrow> l) F"
    4.42 +  assumes "l \<notin> \<int>"
    4.43 +  shows "((\<lambda>x. of_int (floor (f x))::'c::{ring_1, topological_space}) \<longlongrightarrow> of_int (floor l)) F"
    4.44 +  using eventually_floor_eq[OF assms]
    4.45 +  by (simp add: eventually_mono topological_tendstoI)
    4.46 +
    4.47 +lemma tendsto_of_int_ceiling:
    4.48 +  fixes f::"'a \<Rightarrow> 'b::{order_topology, floor_ceiling}"
    4.49 +  assumes "(f \<longlongrightarrow> l) F"
    4.50 +  assumes "l \<notin> \<int>"
    4.51 +  shows "((\<lambda>x. of_int (ceiling (f x))::'c::{ring_1, topological_space}) \<longlongrightarrow> of_int (ceiling l)) F"
    4.52 +  using eventually_ceiling_eq[OF assms]
    4.53 +  by (simp add: eventually_mono topological_tendstoI)
    4.54 +
    4.55 +lemma continuous_on_of_int_floor:
    4.56 +  "continuous_on (UNIV - \<int>::'a::{order_topology, floor_ceiling} set)
    4.57 +    (\<lambda>x. of_int (floor x)::'b::{ring_1, topological_space})"
    4.58 +  unfolding continuous_on_def
    4.59 +  by (auto intro!: tendsto_of_int_floor)
    4.60 +
    4.61 +lemma continuous_on_of_int_ceiling:
    4.62 +  "continuous_on (UNIV - \<int>::'a::{order_topology, floor_ceiling} set)
    4.63 +    (\<lambda>x. of_int (ceiling x)::'b::{ring_1, topological_space})"
    4.64 +  unfolding continuous_on_def
    4.65 +  by (auto intro!: tendsto_of_int_ceiling)
    4.66 +
    4.67 +
    4.68  subsection \<open>Limits of Sequences\<close>
    4.69  
    4.70  lemma [trans]: "X = Y \<Longrightarrow> Y \<longlonglongrightarrow> z \<Longrightarrow> X \<longlonglongrightarrow> z"