--- a/src/HOL/Decision_Procs/Approximation_Bounds.thy Sun Oct 27 21:51:14 2019 -0400
+++ b/src/HOL/Decision_Procs/Approximation_Bounds.thy Sun Nov 03 19:58:02 2019 -0500
@@ -11,13 +11,15 @@
theory Approximation_Bounds
imports
Complex_Main
- "HOL-Library.Float"
+ "HOL-Library.Interval_Float"
Dense_Linear_Order
begin
declare powr_neg_one [simp]
declare powr_neg_numeral [simp]
+context includes interval.lifting begin
+
section "Horner Scheme"
subsection \<open>Define auxiliary helper \<open>horner\<close> function\<close>
@@ -193,6 +195,44 @@
l1 \<le> x ^ n \<and> x ^ n \<le> u1"
using float_power_bnds by auto
+lift_definition power_float_interval :: "nat \<Rightarrow> nat \<Rightarrow> float interval \<Rightarrow> float interval"
+ is "\<lambda>p n (l, u). float_power_bnds p n l u"
+ using float_power_bnds
+ by (auto simp: bnds_power dest!: float_power_bnds[OF sym])
+
+lemma lower_power_float_interval:
+ "lower (power_float_interval p n x) = fst (float_power_bnds p n (lower x) (upper x))"
+ by transfer auto
+lemma upper_power_float_interval:
+ "upper (power_float_interval p n x) = snd (float_power_bnds p n (lower x) (upper x))"
+ by transfer auto
+
+lemma power_float_intervalI: "x \<in>\<^sub>r X \<Longrightarrow> x ^ n \<in>\<^sub>r power_float_interval p n X"
+ using float_power_bnds[OF prod.collapse]
+ by (auto simp: set_of_eq lower_power_float_interval upper_power_float_interval)
+
+lemma power_float_interval_mono:
+ "set_of (power_float_interval prec n A)
+ \<subseteq> set_of (power_float_interval prec n B)"
+ if "set_of A \<subseteq> set_of B"
+proof -
+ define la where "la = real_of_float (lower A)"
+ define ua where "ua = real_of_float (upper A)"
+ define lb where "lb = real_of_float (lower B)"
+ define ub where "ub = real_of_float (upper B)"
+ have ineqs: "lb \<le> la" "la \<le> ua" "ua \<le> ub" "lb \<le> ub"
+ using that lower_le_upper[of A] lower_le_upper[of B]
+ by (auto simp: la_def ua_def lb_def ub_def set_of_eq)
+ show ?thesis
+ using ineqs
+ by (simp add: set_of_subset_iff float_power_bnds_def max_def
+ power_down_fl.rep_eq power_up_fl.rep_eq
+ lower_power_float_interval upper_power_float_interval
+ la_def[symmetric] ua_def[symmetric] lb_def[symmetric] ub_def[symmetric])
+ (auto intro!: power_down_mono power_up_mono intro: order_trans[where y=0])
+qed
+
+
section \<open>Approximation utility functions\<close>
definition bnds_mult :: "nat \<Rightarrow> float \<Rightarrow> float \<Rightarrow> float \<Rightarrow> float \<Rightarrow> float \<times> float" where
@@ -220,6 +260,42 @@
ultimately show ?thesis by simp
qed
+lift_definition mult_float_interval::"nat \<Rightarrow> float interval \<Rightarrow> float interval \<Rightarrow> float interval"
+ is "\<lambda>prec. \<lambda>(a1, a2). \<lambda>(b1, b2). bnds_mult prec a1 a2 b1 b2"
+ by (auto dest!: bnds_mult[OF sym])
+
+lemma lower_mult_float_interval:
+ "lower (mult_float_interval p x y) = fst (bnds_mult p (lower x) (upper x) (lower y) (upper y))"
+ by transfer auto
+lemma upper_mult_float_interval:
+ "upper (mult_float_interval p x y) = snd (bnds_mult p (lower x) (upper x) (lower y) (upper y))"
+ by transfer auto
+
+lemma mult_float_interval:
+ "set_of (real_interval A) * set_of (real_interval B) \<subseteq>
+ set_of (real_interval (mult_float_interval prec A B))"
+proof -
+ let ?bm = "bnds_mult prec (lower A) (upper A) (lower B) (upper B)"
+ show ?thesis
+ using bnds_mult[of "fst ?bm" "snd ?bm", simplified, OF refl]
+ by (auto simp: set_of_eq set_times_def upper_mult_float_interval lower_mult_float_interval)
+qed
+
+lemma mult_float_intervalI:
+ "x * y \<in>\<^sub>r mult_float_interval prec A B"
+ if "x \<in>\<^sub>i real_interval A" "y \<in>\<^sub>i real_interval B"
+ using mult_float_interval[of A B] that
+ by (auto simp: )
+
+lemma mult_float_interval_mono:
+ "set_of (mult_float_interval prec A B) \<subseteq> set_of (mult_float_interval prec X Y)"
+ if "set_of A \<subseteq> set_of X" "set_of B \<subseteq> set_of Y"
+ using that
+ apply transfer
+ unfolding bnds_mult_def atLeastatMost_subset_iff float_plus_down.rep_eq float_plus_up.rep_eq
+ by (auto simp: float_plus_down.rep_eq float_plus_up.rep_eq mult_float_mono1 mult_float_mono2)
+
+
definition map_bnds :: "(nat \<Rightarrow> float \<Rightarrow> float) \<Rightarrow> (nat \<Rightarrow> float \<Rightarrow> float) \<Rightarrow>
nat \<Rightarrow> (float \<times> float) \<Rightarrow> (float \<times> float)" where
"map_bnds lb ub prec = (\<lambda>(l,u). (lb prec l, ub prec u))"
@@ -456,6 +532,25 @@
show "sqrt x \<le> u" unfolding u using bnds_sqrt'[of ux prec] by auto
qed
+lift_definition sqrt_float_interval::"nat \<Rightarrow> float interval \<Rightarrow> float interval"
+ is "\<lambda>prec. \<lambda>(lx, ux). (lb_sqrt prec lx, ub_sqrt prec ux)"
+ using bnds_sqrt'
+ by auto (meson order_trans real_sqrt_le_iff)
+
+lemma lower_float_interval: "lower (sqrt_float_interval prec X) = lb_sqrt prec (lower X)"
+ by transfer auto
+
+lemma upper_float_interval: "upper (sqrt_float_interval prec X) = ub_sqrt prec (upper X)"
+ by transfer auto
+
+lemma sqrt_float_interval:
+ "sqrt ` set_of (real_interval X) \<subseteq> set_of (real_interval (sqrt_float_interval prec X))"
+ using bnds_sqrt
+ by (auto simp: set_of_eq lower_float_interval upper_float_interval)
+
+lemma sqrt_float_intervalI: "sqrt x \<in>\<^sub>r sqrt_float_interval p X" if "x \<in>\<^sub>r X"
+ using sqrt_float_interval[of X p] that
+ by auto
section "Arcus tangens and \<pi>"
@@ -711,6 +806,18 @@
ultimately show ?thesis by auto
qed
+lift_definition pi_float_interval::"nat \<Rightarrow> float interval" is "\<lambda>prec. (lb_pi prec, ub_pi prec)"
+ using pi_boundaries
+ by (auto intro: order_trans)
+
+lemma lower_pi_float_interval: "lower (pi_float_interval prec) = lb_pi prec"
+ by transfer auto
+lemma upper_pi_float_interval: "upper (pi_float_interval prec) = ub_pi prec"
+ by transfer auto
+lemma pi_float_interval: "pi \<in> set_of (real_interval (pi_float_interval prec))"
+ using pi_boundaries
+ by (auto simp: set_of_eq lower_pi_float_interval upper_pi_float_interval)
+
subsection "Compute arcus tangens in the entire domain"
@@ -1056,6 +1163,32 @@
qed
qed
+lemmas [simp del] = lb_arctan.simps ub_arctan.simps
+
+lemma lb_arctan: "arctan (real_of_float x) \<le> y \<Longrightarrow> real_of_float (lb_arctan prec x) \<le> y"
+ and ub_arctan: "y \<le> arctan x \<Longrightarrow> y \<le> ub_arctan prec x"
+ for x::float and y::real
+ using arctan_boundaries[of x prec] by auto
+
+lift_definition arctan_float_interval :: "nat \<Rightarrow> float interval \<Rightarrow> float interval"
+ is "\<lambda>prec. \<lambda>(lx, ux). (lb_arctan prec lx, ub_arctan prec ux)"
+ by (auto intro!: lb_arctan ub_arctan arctan_monotone')
+
+lemma lower_arctan_float_interval: "lower (arctan_float_interval p x) = lb_arctan p (lower x)"
+ by transfer auto
+lemma upper_arctan_float_interval: "upper (arctan_float_interval p x) = ub_arctan p (upper x)"
+ by transfer auto
+
+lemma arctan_float_interval:
+ "arctan ` set_of (real_interval x) \<subseteq> set_of (real_interval (arctan_float_interval p x))"
+ by (auto simp: set_of_eq lower_arctan_float_interval upper_arctan_float_interval
+ intro!: lb_arctan ub_arctan arctan_monotone')
+
+lemma arctan_float_intervalI:
+ "arctan x \<in>\<^sub>r arctan_float_interval p X" if "x \<in>\<^sub>r X"
+ using arctan_float_interval[of X p] that
+ by auto
+
section "Sinus and Cosinus"
@@ -1794,6 +1927,31 @@
qed
qed
+lemma bnds_cos_lower: "\<And>x. real_of_float xl \<le> x \<Longrightarrow> x \<le> real_of_float xu \<Longrightarrow> cos x \<le> y \<Longrightarrow> real_of_float (fst (bnds_cos prec xl xu)) \<le> y"
+ and bnds_cos_upper: "\<And>x. real_of_float xl \<le> x \<Longrightarrow> x \<le> real_of_float xu \<Longrightarrow> y \<le> cos x \<Longrightarrow> y \<le> real_of_float (snd (bnds_cos prec xl xu))"
+ for xl xu::float and y::real
+ using bnds_cos[of "fst (bnds_cos prec xl xu)" "snd (bnds_cos prec xl xu)" prec]
+ by force+
+
+lift_definition cos_float_interval :: "nat \<Rightarrow> float interval \<Rightarrow> float interval"
+ is "\<lambda>prec. \<lambda>(lx, ux). bnds_cos prec lx ux"
+ using bnds_cos
+ by auto (metis (full_types) order_refl order_trans)
+
+lemma lower_cos_float_interval: "lower (cos_float_interval p x) = fst (bnds_cos p (lower x) (upper x))"
+ by transfer auto
+lemma upper_cos_float_interval: "upper (cos_float_interval p x) = snd (bnds_cos p (lower x) (upper x))"
+ by transfer auto
+
+lemma cos_float_interval:
+ "cos ` set_of (real_interval x) \<subseteq> set_of (real_interval (cos_float_interval p x))"
+ by (auto simp: set_of_eq bnds_cos_lower bnds_cos_upper lower_cos_float_interval
+ upper_cos_float_interval)
+
+lemma cos_float_intervalI: "cos x \<in>\<^sub>r cos_float_interval p X" if "x \<in>\<^sub>r X"
+ using cos_float_interval[of X p] that
+ by auto
+
section "Exponential function"
@@ -2137,6 +2295,31 @@
qed
qed
+lemmas [simp del] = lb_exp.simps ub_exp.simps
+
+lemma lb_exp: "exp x \<le> y \<Longrightarrow> lb_exp prec x \<le> y"
+ and ub_exp: "y \<le> exp x \<Longrightarrow> y \<le> ub_exp prec x"
+ for x::float and y::real using exp_boundaries[of x prec] by auto
+
+lift_definition exp_float_interval :: "nat \<Rightarrow> float interval \<Rightarrow> float interval"
+ is "\<lambda>prec. \<lambda>(lx, ux). (lb_exp prec lx, ub_exp prec ux)"
+ by (auto simp: lb_exp ub_exp)
+
+lemma lower_exp_float_interval: "lower (exp_float_interval p x) = lb_exp p (lower x)"
+ by transfer auto
+lemma upper_exp_float_interval: "upper (exp_float_interval p x) = ub_exp p (upper x)"
+ by transfer auto
+
+lemma exp_float_interval:
+ "exp ` set_of (real_interval x) \<subseteq> set_of (real_interval (exp_float_interval p x))"
+ using exp_boundaries
+ by (auto simp: set_of_eq lower_exp_float_interval upper_exp_float_interval lb_exp ub_exp)
+
+lemma exp_float_intervalI:
+ "exp x \<in>\<^sub>r exp_float_interval p X" if "x \<in>\<^sub>r X"
+ using exp_float_interval[of X p] that
+ by auto
+
section "Logarithm"
@@ -2211,7 +2394,7 @@
also have "\<dots> \<le> ?ub"
unfolding power_Suc2 mult.assoc[symmetric] times_float.rep_eq sum_distrib_right[symmetric]
unfolding mult.commute[of "real_of_float x"] od
- using horner_bounds(2)[where G="\<lambda> i k. Suc k" and F="\<lambda>x. x" and f="\<lambda>x. x" and lb="\<lambda>n i k x. lb_ln_horner prec n k x" and ub="\<lambda>n i k x. ub_ln_horner prec n k x" and j'=1 and n="2*od+1",
+ using horner_bounds(2)[where G="\<lambda> i k. Suc k" and F="\<lambda>x. x" and f="\<lambda>x. x" and lb="\<lambda>n i k x. lb_ln_horner prec n k x" and ub="\<lambda>n i k x. ub_ln_horner prec n k x" and j'=1 and n="2 * od + 1",
OF \<open>0 \<le> real_of_float x\<close> refl lb_ln_horner.simps ub_ln_horner.simps] \<open>0 \<le> real_of_float x\<close>
unfolding real_of_float_power
by (rule mult_right_mono)
@@ -2703,6 +2886,41 @@
ultimately show "l \<le> ln x \<and> ln x \<le> u" ..
qed
+lemmas [simp del] = lb_ln.simps ub_ln.simps
+
+lemma lb_lnD:
+ "y \<le> ln x \<and> 0 < real_of_float x" if "lb_ln prec x = Some y"
+ using lb_ln[OF that[symmetric]] by auto
+
+lemma ub_lnD:
+ "ln x \<le> y\<and> 0 < real_of_float x" if "ub_ln prec x = Some y"
+ using ub_ln[OF that[symmetric]] by auto
+
+lift_definition(code_dt) ln_float_interval :: "nat \<Rightarrow> float interval \<Rightarrow> float interval option"
+ is "\<lambda>prec. \<lambda>(lx, ux).
+ Option.bind (lb_ln prec lx) (\<lambda>l.
+ Option.bind (ub_ln prec ux) (\<lambda>u. Some (l, u)))"
+ by (auto simp: pred_option_def bind_eq_Some_conv ln_le_cancel_iff[symmetric]
+ simp del: ln_le_cancel_iff dest!: lb_lnD ub_lnD)
+
+lemma ln_float_interval_eq_Some_conv:
+ "ln_float_interval p x = Some y \<longleftrightarrow>
+ lb_ln p (lower x) = Some (lower y) \<and> ub_ln p (upper x) = Some (upper y)"
+ by transfer (auto simp: bind_eq_Some_conv)
+
+lemma ln_float_interval: "ln ` set_of (real_interval x) \<subseteq> set_of (real_interval y)"
+ if "ln_float_interval p x = Some y"
+ using that lb_ln[of "lower y" p "lower x"]
+ ub_ln[of "lower y" p "lower x"]
+ apply (auto simp add: set_of_eq ln_float_interval_eq_Some_conv ln_le_cancel_iff)
+ apply (meson less_le_trans ln_less_cancel_iff not_le)
+ by (meson less_le_trans ln_less_cancel_iff not_le ub_lnD)
+
+lemma ln_float_intervalI:
+ "ln x \<in> set_of' (ln_float_interval p X)" if "x \<in>\<^sub>r X"
+ using ln_float_interval[of p X] that
+ by (auto simp: set_of'_def split: option.splits)
+
section \<open>Real power function\<close>
@@ -2719,8 +2937,6 @@
Some (map_bnds lb_exp ub_exp prec
(bnds_mult prec (the (lb_ln prec l1)) (the (ub_ln prec u1)) l2 u2)))"
-lemmas [simp del] = lb_exp.simps ub_exp.simps
-
lemma mono_exp_real: "mono (exp :: real \<Rightarrow> real)"
by (auto simp: mono_def)
@@ -2798,4 +3014,23 @@
qed
qed
+lift_definition(code_dt) powr_float_interval :: "nat \<Rightarrow> float interval \<Rightarrow> float interval \<Rightarrow> float interval option"
+ is "\<lambda>prec. \<lambda>(l1, u1). \<lambda>(l2, u2). bnds_powr prec l1 u1 l2 u2"
+ by (auto simp: pred_option_def dest!: bnds_powr[OF sym])
+
+lemma powr_float_interval:
+ "{x powr y | x y. x \<in> set_of (real_interval X) \<and> y \<in> set_of (real_interval Y)}
+ \<subseteq> set_of (real_interval R)"
+ if "powr_float_interval prec X Y = Some R"
+ using that
+ by transfer (auto dest!: bnds_powr[OF sym])
+
+lemma powr_float_intervalI:
+ "x powr y \<in> set_of' (powr_float_interval p X Y)"
+ if "x \<in>\<^sub>r X" "y \<in>\<^sub>r Y"
+ using powr_float_interval[of p X Y] that
+ by (auto simp: set_of'_def split: option.splits)
+
end
+
+end
\ No newline at end of file
--- a/src/HOL/Library/Float.thy Sun Oct 27 21:51:14 2019 -0400
+++ b/src/HOL/Library/Float.thy Sun Nov 03 19:58:02 2019 -0500
@@ -1104,6 +1104,201 @@
end
+lemma truncate_up_nonneg_mono:
+ assumes "0 \<le> x" "x \<le> y"
+ shows "truncate_up prec x \<le> truncate_up prec y"
+proof -
+ consider "\<lfloor>log 2 x\<rfloor> = \<lfloor>log 2 y\<rfloor>" | "\<lfloor>log 2 x\<rfloor> \<noteq> \<lfloor>log 2 y\<rfloor>" "0 < x" | "x \<le> 0"
+ by arith
+ then show ?thesis
+ proof cases
+ case 1
+ then show ?thesis
+ using assms
+ by (auto simp: truncate_up_def round_up_def intro!: ceiling_mono)
+ next
+ case 2
+ from assms \<open>0 < x\<close> have "log 2 x \<le> log 2 y"
+ by auto
+ with \<open>\<lfloor>log 2 x\<rfloor> \<noteq> \<lfloor>log 2 y\<rfloor>\<close>
+ have logless: "log 2 x < log 2 y"
+ by linarith
+ have flogless: "\<lfloor>log 2 x\<rfloor> < \<lfloor>log 2 y\<rfloor>"
+ using \<open>\<lfloor>log 2 x\<rfloor> \<noteq> \<lfloor>log 2 y\<rfloor>\<close> \<open>log 2 x \<le> log 2 y\<close> by linarith
+ have "truncate_up prec x =
+ real_of_int \<lceil>x * 2 powr real_of_int (int prec - \<lfloor>log 2 x\<rfloor> )\<rceil> * 2 powr - real_of_int (int prec - \<lfloor>log 2 x\<rfloor>)"
+ using assms by (simp add: truncate_up_def round_up_def)
+ also have "\<lceil>x * 2 powr real_of_int (int prec - \<lfloor>log 2 x\<rfloor>)\<rceil> \<le> (2 ^ (Suc prec))"
+ proof (simp only: ceiling_le_iff)
+ have "x * 2 powr real_of_int (int prec - \<lfloor>log 2 x\<rfloor>) \<le>
+ x * (2 powr real (Suc prec) / (2 powr log 2 x))"
+ using real_of_int_floor_add_one_ge[of "log 2 x"] assms
+ by (auto simp: algebra_simps simp flip: powr_diff intro!: mult_left_mono)
+ then show "x * 2 powr real_of_int (int prec - \<lfloor>log 2 x\<rfloor>) \<le> real_of_int ((2::int) ^ (Suc prec))"
+ using \<open>0 < x\<close> by (simp add: powr_realpow powr_add)
+ qed
+ then have "real_of_int \<lceil>x * 2 powr real_of_int (int prec - \<lfloor>log 2 x\<rfloor>)\<rceil> \<le> 2 powr int (Suc prec)"
+ by (auto simp: powr_realpow powr_add)
+ (metis power_Suc of_int_le_numeral_power_cancel_iff)
+ also
+ have "2 powr - real_of_int (int prec - \<lfloor>log 2 x\<rfloor>) \<le> 2 powr - real_of_int (int prec - \<lfloor>log 2 y\<rfloor> + 1)"
+ using logless flogless by (auto intro!: floor_mono)
+ also have "2 powr real_of_int (int (Suc prec)) \<le>
+ 2 powr (log 2 y + real_of_int (int prec - \<lfloor>log 2 y\<rfloor> + 1))"
+ using assms \<open>0 < x\<close>
+ by (auto simp: algebra_simps)
+ finally have "truncate_up prec x \<le>
+ 2 powr (log 2 y + real_of_int (int prec - \<lfloor>log 2 y\<rfloor> + 1)) * 2 powr - real_of_int (int prec - \<lfloor>log 2 y\<rfloor> + 1)"
+ by simp
+ also have "\<dots> = 2 powr (log 2 y + real_of_int (int prec - \<lfloor>log 2 y\<rfloor>) - real_of_int (int prec - \<lfloor>log 2 y\<rfloor>))"
+ by (subst powr_add[symmetric]) simp
+ also have "\<dots> = y"
+ using \<open>0 < x\<close> assms
+ by (simp add: powr_add)
+ also have "\<dots> \<le> truncate_up prec y"
+ by (rule truncate_up)
+ finally show ?thesis .
+ next
+ case 3
+ then show ?thesis
+ using assms
+ by (auto intro!: truncate_up_le)
+ qed
+qed
+
+lemma truncate_up_switch_sign_mono:
+ assumes "x \<le> 0" "0 \<le> y"
+ shows "truncate_up prec x \<le> truncate_up prec y"
+proof -
+ note truncate_up_nonpos[OF \<open>x \<le> 0\<close>]
+ also note truncate_up_le[OF \<open>0 \<le> y\<close>]
+ finally show ?thesis .
+qed
+
+lemma truncate_down_switch_sign_mono:
+ assumes "x \<le> 0"
+ and "0 \<le> y"
+ and "x \<le> y"
+ shows "truncate_down prec x \<le> truncate_down prec y"
+proof -
+ note truncate_down_le[OF \<open>x \<le> 0\<close>]
+ also note truncate_down_nonneg[OF \<open>0 \<le> y\<close>]
+ finally show ?thesis .
+qed
+
+lemma truncate_down_nonneg_mono:
+ assumes "0 \<le> x" "x \<le> y"
+ shows "truncate_down prec x \<le> truncate_down prec y"
+proof -
+ consider "x \<le> 0" | "\<lfloor>log 2 \<bar>x\<bar>\<rfloor> = \<lfloor>log 2 \<bar>y\<bar>\<rfloor>" |
+ "0 < x" "\<lfloor>log 2 \<bar>x\<bar>\<rfloor> \<noteq> \<lfloor>log 2 \<bar>y\<bar>\<rfloor>"
+ by arith
+ then show ?thesis
+ proof cases
+ case 1
+ with assms have "x = 0" "0 \<le> y" by simp_all
+ then show ?thesis
+ by (auto intro!: truncate_down_nonneg)
+ next
+ case 2
+ then show ?thesis
+ using assms
+ by (auto simp: truncate_down_def round_down_def intro!: floor_mono)
+ next
+ case 3
+ from \<open>0 < x\<close> have "log 2 x \<le> log 2 y" "0 < y" "0 \<le> y"
+ using assms by auto
+ with \<open>\<lfloor>log 2 \<bar>x\<bar>\<rfloor> \<noteq> \<lfloor>log 2 \<bar>y\<bar>\<rfloor>\<close>
+ have logless: "log 2 x < log 2 y" and flogless: "\<lfloor>log 2 x\<rfloor> < \<lfloor>log 2 y\<rfloor>"
+ unfolding atomize_conj abs_of_pos[OF \<open>0 < x\<close>] abs_of_pos[OF \<open>0 < y\<close>]
+ by (metis floor_less_cancel linorder_cases not_le)
+ have "2 powr prec \<le> y * 2 powr real prec / (2 powr log 2 y)"
+ using \<open>0 < y\<close> by simp
+ also have "\<dots> \<le> y * 2 powr real (Suc prec) / (2 powr (real_of_int \<lfloor>log 2 y\<rfloor> + 1))"
+ using \<open>0 \<le> y\<close> \<open>0 \<le> x\<close> assms(2)
+ by (auto intro!: powr_mono divide_left_mono
+ simp: of_nat_diff powr_add powr_diff)
+ also have "\<dots> = y * 2 powr real (Suc prec) / (2 powr real_of_int \<lfloor>log 2 y\<rfloor> * 2)"
+ by (auto simp: powr_add)
+ finally have "(2 ^ prec) \<le> \<lfloor>y * 2 powr real_of_int (int (Suc prec) - \<lfloor>log 2 \<bar>y\<bar>\<rfloor> - 1)\<rfloor>"
+ using \<open>0 \<le> y\<close>
+ by (auto simp: powr_diff le_floor_iff powr_realpow powr_add)
+ then have "(2 ^ (prec)) * 2 powr - real_of_int (int prec - \<lfloor>log 2 \<bar>y\<bar>\<rfloor>) \<le> truncate_down prec y"
+ by (auto simp: truncate_down_def round_down_def)
+ moreover have "x \<le> (2 ^ prec) * 2 powr - real_of_int (int prec - \<lfloor>log 2 \<bar>y\<bar>\<rfloor>)"
+ proof -
+ have "x = 2 powr (log 2 \<bar>x\<bar>)" using \<open>0 < x\<close> by simp
+ also have "\<dots> \<le> (2 ^ (Suc prec )) * 2 powr - real_of_int (int prec - \<lfloor>log 2 \<bar>x\<bar>\<rfloor>)"
+ using real_of_int_floor_add_one_ge[of "log 2 \<bar>x\<bar>"] \<open>0 < x\<close>
+ by (auto simp flip: powr_realpow powr_add simp: algebra_simps powr_mult_base le_powr_iff)
+ also
+ have "2 powr - real_of_int (int prec - \<lfloor>log 2 \<bar>x\<bar>\<rfloor>) \<le> 2 powr - real_of_int (int prec - \<lfloor>log 2 \<bar>y\<bar>\<rfloor> + 1)"
+ using logless flogless \<open>x > 0\<close> \<open>y > 0\<close>
+ by (auto intro!: floor_mono)
+ finally show ?thesis
+ by (auto simp flip: powr_realpow simp: powr_diff assms of_nat_diff)
+ qed
+ ultimately show ?thesis
+ by (metis dual_order.trans truncate_down)
+ qed
+qed
+
+lemma truncate_down_eq_truncate_up: "truncate_down p x = - truncate_up p (-x)"
+ and truncate_up_eq_truncate_down: "truncate_up p x = - truncate_down p (-x)"
+ by (auto simp: truncate_up_uminus_eq truncate_down_uminus_eq)
+
+lemma truncate_down_mono: "x \<le> y \<Longrightarrow> truncate_down p x \<le> truncate_down p y"
+ apply (cases "0 \<le> x")
+ apply (rule truncate_down_nonneg_mono, assumption+)
+ apply (simp add: truncate_down_eq_truncate_up)
+ apply (cases "0 \<le> y")
+ apply (auto intro: truncate_up_nonneg_mono truncate_up_switch_sign_mono)
+ done
+
+lemma truncate_up_mono: "x \<le> y \<Longrightarrow> truncate_up p x \<le> truncate_up p y"
+ by (simp add: truncate_up_eq_truncate_down truncate_down_mono)
+
+lemma truncate_up_nonneg: "0 \<le> truncate_up p x" if "0 \<le> x"
+ by (simp add: that truncate_up_le)
+
+lemma truncate_up_pos: "0 < truncate_up p x" if "0 < x"
+ by (meson less_le_trans that truncate_up)
+
+lemma truncate_up_less_zero_iff[simp]: "truncate_up p x < 0 \<longleftrightarrow> x < 0"
+proof -
+ have f1: "\<forall>n r. truncate_up n r + truncate_down n (- 1 * r) = 0"
+ by (simp add: truncate_down_uminus_eq)
+ have f2: "(\<forall>v0 v1. truncate_up v0 v1 + truncate_down v0 (- 1 * v1) = 0) = (\<forall>v0 v1. truncate_up v0 v1 = - 1 * truncate_down v0 (- 1 * v1))"
+ by (auto simp: truncate_up_eq_truncate_down)
+ have f3: "\<forall>x1. ((0::real) < x1) = (\<not> x1 \<le> 0)"
+ by fastforce
+ have "(- 1 * x \<le> 0) = (0 \<le> x)"
+ by force
+ then have "0 \<le> x \<or> \<not> truncate_down p (- 1 * x) \<le> 0"
+ using f3 by (meson truncate_down_pos)
+ then have "(0 \<le> truncate_up p x) \<noteq> (\<not> 0 \<le> x)"
+ using f2 f1 truncate_up_nonneg by force
+ then show ?thesis
+ by linarith
+qed
+
+lemma truncate_up_nonneg_iff[simp]: "truncate_up p x \<ge> 0 \<longleftrightarrow> x \<ge> 0"
+ using truncate_up_less_zero_iff[of p x] truncate_up_nonneg[of x]
+ by linarith
+
+lemma truncate_down_less_zero_iff[simp]: "truncate_down p x < 0 \<longleftrightarrow> x < 0"
+ by (metis le_less_trans not_less_iff_gr_or_eq truncate_down truncate_down_pos truncate_down_zero)
+
+lemma truncate_down_nonneg_iff[simp]: "truncate_down p x \<ge> 0 \<longleftrightarrow> x \<ge> 0"
+ using truncate_down_less_zero_iff[of p x] truncate_down_nonneg[of x p]
+ by linarith
+
+lemma truncate_down_eq_zero_iff[simp]: "truncate_down prec x = 0 \<longleftrightarrow> x = 0"
+ by (metis not_less_iff_gr_or_eq truncate_down_less_zero_iff truncate_down_pos truncate_down_zero)
+
+lemma truncate_up_eq_zero_iff[simp]: "truncate_up prec x = 0 \<longleftrightarrow> x = 0"
+ by (metis not_less_iff_gr_or_eq truncate_up_less_zero_iff truncate_up_pos truncate_up_zero)
+
subsection \<open>Approximation of positive rationals\<close>
@@ -1324,109 +1519,6 @@
end
-subsection \<open>Approximate Power\<close>
-
-lemma div2_less_self[termination_simp]: "odd n \<Longrightarrow> n div 2 < n" for n :: nat
- by (simp add: odd_pos)
-
-fun power_down :: "nat \<Rightarrow> real \<Rightarrow> nat \<Rightarrow> real"
-where
- "power_down p x 0 = 1"
-| "power_down p x (Suc n) =
- (if odd n then truncate_down (Suc p) ((power_down p x (Suc n div 2))\<^sup>2)
- else truncate_down (Suc p) (x * power_down p x n))"
-
-fun power_up :: "nat \<Rightarrow> real \<Rightarrow> nat \<Rightarrow> real"
-where
- "power_up p x 0 = 1"
-| "power_up p x (Suc n) =
- (if odd n then truncate_up p ((power_up p x (Suc n div 2))\<^sup>2)
- else truncate_up p (x * power_up p x n))"
-
-lift_definition power_up_fl :: "nat \<Rightarrow> float \<Rightarrow> nat \<Rightarrow> float" is power_up
- by (induct_tac rule: power_up.induct) simp_all
-
-lift_definition power_down_fl :: "nat \<Rightarrow> float \<Rightarrow> nat \<Rightarrow> float" is power_down
- by (induct_tac rule: power_down.induct) simp_all
-
-lemma power_float_transfer[transfer_rule]:
- "(rel_fun pcr_float (rel_fun (=) pcr_float)) (^) (^)"
- unfolding power_def
- by transfer_prover
-
-lemma compute_power_up_fl[code]:
- "power_up_fl p x 0 = 1"
- "power_up_fl p x (Suc n) =
- (if odd n then float_round_up p ((power_up_fl p x (Suc n div 2))\<^sup>2)
- else float_round_up p (x * power_up_fl p x n))"
- and compute_power_down_fl[code]:
- "power_down_fl p x 0 = 1"
- "power_down_fl p x (Suc n) =
- (if odd n then float_round_down (Suc p) ((power_down_fl p x (Suc n div 2))\<^sup>2)
- else float_round_down (Suc p) (x * power_down_fl p x n))"
- unfolding atomize_conj by transfer simp
-
-lemma power_down_pos: "0 < x \<Longrightarrow> 0 < power_down p x n"
- by (induct p x n rule: power_down.induct)
- (auto simp del: odd_Suc_div_two intro!: truncate_down_pos)
-
-lemma power_down_nonneg: "0 \<le> x \<Longrightarrow> 0 \<le> power_down p x n"
- by (induct p x n rule: power_down.induct)
- (auto simp del: odd_Suc_div_two intro!: truncate_down_nonneg mult_nonneg_nonneg)
-
-lemma power_down: "0 \<le> x \<Longrightarrow> power_down p x n \<le> x ^ n"
-proof (induct p x n rule: power_down.induct)
- case (2 p x n)
- have ?case if "odd n"
- proof -
- from that 2 have "(power_down p x (Suc n div 2)) ^ 2 \<le> (x ^ (Suc n div 2)) ^ 2"
- by (auto intro: power_mono power_down_nonneg simp del: odd_Suc_div_two)
- also have "\<dots> = x ^ (Suc n div 2 * 2)"
- by (simp flip: power_mult)
- also have "Suc n div 2 * 2 = Suc n"
- using \<open>odd n\<close> by presburger
- finally show ?thesis
- using that by (auto intro!: truncate_down_le simp del: odd_Suc_div_two)
- qed
- then show ?case
- by (auto intro!: truncate_down_le mult_left_mono 2 mult_nonneg_nonneg power_down_nonneg)
-qed simp
-
-lemma power_up: "0 \<le> x \<Longrightarrow> x ^ n \<le> power_up p x n"
-proof (induct p x n rule: power_up.induct)
- case (2 p x n)
- have ?case if "odd n"
- proof -
- from that even_Suc have "Suc n = Suc n div 2 * 2"
- by presburger
- then have "x ^ Suc n \<le> (x ^ (Suc n div 2))\<^sup>2"
- by (simp flip: power_mult)
- also from that 2 have "\<dots> \<le> (power_up p x (Suc n div 2))\<^sup>2"
- by (auto intro: power_mono simp del: odd_Suc_div_two)
- finally show ?thesis
- using that by (auto intro!: truncate_up_le simp del: odd_Suc_div_two)
- qed
- then show ?case
- by (auto intro!: truncate_up_le mult_left_mono 2)
-qed simp
-
-lemmas power_up_le = order_trans[OF _ power_up]
- and power_up_less = less_le_trans[OF _ power_up]
- and power_down_le = order_trans[OF power_down]
-
-lemma power_down_fl: "0 \<le> x \<Longrightarrow> power_down_fl p x n \<le> x ^ n"
- by transfer (rule power_down)
-
-lemma power_up_fl: "0 \<le> x \<Longrightarrow> x ^ n \<le> power_up_fl p x n"
- by transfer (rule power_up)
-
-lemma real_power_up_fl: "real_of_float (power_up_fl p x n) = power_up p x n"
- by transfer simp
-
-lemma real_power_down_fl: "real_of_float (power_down_fl p x n) = power_down p x n"
- by transfer simp
-
-
subsection \<open>Approximate Addition\<close>
definition "plus_down prec x y = truncate_down prec (x + y)"
@@ -1794,6 +1886,332 @@
end
+lemma plus_down_mono: "plus_down p a b \<le> plus_down p c d" if "a + b \<le> c + d"
+ by (auto simp: plus_down_def intro!: truncate_down_mono that)
+
+lemma plus_up_mono: "plus_up p a b \<le> plus_up p c d" if "a + b \<le> c + d"
+ by (auto simp: plus_up_def intro!: truncate_up_mono that)
+
+subsection \<open>Approximate Multiplication\<close>
+
+lemma mult_mono_nonpos_nonneg: "a * b \<le> c * d"
+ if "a \<le> c" "a \<le> 0" "0 \<le> d" "d \<le> b" for a b c d::"'a::ordered_ring"
+ by (meson dual_order.trans mult_left_mono_neg mult_right_mono that)
+
+lemma mult_mono_nonneg_nonpos: "b * a \<le> d * c"
+ if "a \<le> c" "c \<le> 0" "0 \<le> d" "d \<le> b" for a b c d::"'a::ordered_ring"
+ by (meson dual_order.trans mult_right_mono_neg mult_left_mono that)
+
+lemma mult_mono_nonpos_nonpos: "a * b \<le> c * d"
+ if "a \<ge> c" "a \<le> 0" "b \<ge> d" "d \<le> 0" for a b c d::real
+ by (meson dual_order.trans mult_left_mono_neg mult_right_mono_neg that)
+
+lemma mult_float_mono1:
+ notes mono_rules = plus_down_mono add_mono nprt_mono nprt_le_zero zero_le_pprt pprt_mono
+ shows "a \<le> b \<Longrightarrow> ab \<le> bb \<Longrightarrow>
+ aa \<le> a \<Longrightarrow>
+ b \<le> ba \<Longrightarrow>
+ ac \<le> ab \<Longrightarrow>
+ bb \<le> bc \<Longrightarrow>
+ plus_down prec (nprt aa * pprt bc)
+ (plus_down prec (nprt ba * nprt bc)
+ (plus_down prec (pprt aa * pprt ac)
+ (pprt ba * nprt ac)))
+ \<le> plus_down prec (nprt a * pprt bb)
+ (plus_down prec (nprt b * nprt bb)
+ (plus_down prec (pprt a * pprt ab)
+ (pprt b * nprt ab)))"
+ apply (rule order_trans)
+ apply (rule mono_rules | assumption)+
+ apply (rule mult_mono_nonpos_nonneg)
+ apply (rule mono_rules | assumption)+
+ apply (rule mult_mono_nonpos_nonpos)
+ apply (rule mono_rules | assumption)+
+ apply (rule mult_mono)
+ apply (rule mono_rules | assumption)+
+ apply (rule mult_mono_nonneg_nonpos)
+ apply (rule mono_rules | assumption)+
+ by (rule order_refl)+
+
+lemma mult_float_mono2:
+ notes mono_rules = plus_up_mono add_mono nprt_mono nprt_le_zero zero_le_pprt pprt_mono
+ shows "a \<le> b \<Longrightarrow>
+ ab \<le> bb \<Longrightarrow>
+ aa \<le> a \<Longrightarrow>
+ b \<le> ba \<Longrightarrow>
+ ac \<le> ab \<Longrightarrow>
+ bb \<le> bc \<Longrightarrow>
+ plus_up prec (pprt b * pprt bb)
+ (plus_up prec (pprt a * nprt bb)
+ (plus_up prec (nprt b * pprt ab)
+ (nprt a * nprt ab)))
+ \<le> plus_up prec (pprt ba * pprt bc)
+ (plus_up prec (pprt aa * nprt bc)
+ (plus_up prec (nprt ba * pprt ac)
+ (nprt aa * nprt ac)))"
+ apply (rule order_trans)
+ apply (rule mono_rules | assumption)+
+ apply (rule mult_mono)
+ apply (rule mono_rules | assumption)+
+ apply (rule mult_mono_nonneg_nonpos)
+ apply (rule mono_rules | assumption)+
+ apply (rule mult_mono_nonpos_nonneg)
+ apply (rule mono_rules | assumption)+
+ apply (rule mult_mono_nonpos_nonpos)
+ apply (rule mono_rules | assumption)+
+ by (rule order_refl)+
+
+
+subsection \<open>Approximate Power\<close>
+
+lemma div2_less_self[termination_simp]: "odd n \<Longrightarrow> n div 2 < n" for n :: nat
+ by (simp add: odd_pos)
+
+fun power_down :: "nat \<Rightarrow> real \<Rightarrow> nat \<Rightarrow> real"
+where
+ "power_down p x 0 = 1"
+| "power_down p x (Suc n) =
+ (if odd n then truncate_down (Suc p) ((power_down p x (Suc n div 2))\<^sup>2)
+ else truncate_down (Suc p) (x * power_down p x n))"
+
+fun power_up :: "nat \<Rightarrow> real \<Rightarrow> nat \<Rightarrow> real"
+where
+ "power_up p x 0 = 1"
+| "power_up p x (Suc n) =
+ (if odd n then truncate_up p ((power_up p x (Suc n div 2))\<^sup>2)
+ else truncate_up p (x * power_up p x n))"
+
+lift_definition power_up_fl :: "nat \<Rightarrow> float \<Rightarrow> nat \<Rightarrow> float" is power_up
+ by (induct_tac rule: power_up.induct) simp_all
+
+lift_definition power_down_fl :: "nat \<Rightarrow> float \<Rightarrow> nat \<Rightarrow> float" is power_down
+ by (induct_tac rule: power_down.induct) simp_all
+
+lemma power_float_transfer[transfer_rule]:
+ "(rel_fun pcr_float (rel_fun (=) pcr_float)) (^) (^)"
+ unfolding power_def
+ by transfer_prover
+
+lemma compute_power_up_fl[code]:
+ "power_up_fl p x 0 = 1"
+ "power_up_fl p x (Suc n) =
+ (if odd n then float_round_up p ((power_up_fl p x (Suc n div 2))\<^sup>2)
+ else float_round_up p (x * power_up_fl p x n))"
+ and compute_power_down_fl[code]:
+ "power_down_fl p x 0 = 1"
+ "power_down_fl p x (Suc n) =
+ (if odd n then float_round_down (Suc p) ((power_down_fl p x (Suc n div 2))\<^sup>2)
+ else float_round_down (Suc p) (x * power_down_fl p x n))"
+ unfolding atomize_conj by transfer simp
+
+lemma power_down_pos: "0 < x \<Longrightarrow> 0 < power_down p x n"
+ by (induct p x n rule: power_down.induct)
+ (auto simp del: odd_Suc_div_two intro!: truncate_down_pos)
+
+lemma power_down_nonneg: "0 \<le> x \<Longrightarrow> 0 \<le> power_down p x n"
+ by (induct p x n rule: power_down.induct)
+ (auto simp del: odd_Suc_div_two intro!: truncate_down_nonneg mult_nonneg_nonneg)
+
+lemma power_down: "0 \<le> x \<Longrightarrow> power_down p x n \<le> x ^ n"
+proof (induct p x n rule: power_down.induct)
+ case (2 p x n)
+ have ?case if "odd n"
+ proof -
+ from that 2 have "(power_down p x (Suc n div 2)) ^ 2 \<le> (x ^ (Suc n div 2)) ^ 2"
+ by (auto intro: power_mono power_down_nonneg simp del: odd_Suc_div_two)
+ also have "\<dots> = x ^ (Suc n div 2 * 2)"
+ by (simp flip: power_mult)
+ also have "Suc n div 2 * 2 = Suc n"
+ using \<open>odd n\<close> by presburger
+ finally show ?thesis
+ using that by (auto intro!: truncate_down_le simp del: odd_Suc_div_two)
+ qed
+ then show ?case
+ by (auto intro!: truncate_down_le mult_left_mono 2 mult_nonneg_nonneg power_down_nonneg)
+qed simp
+
+lemma power_up: "0 \<le> x \<Longrightarrow> x ^ n \<le> power_up p x n"
+proof (induct p x n rule: power_up.induct)
+ case (2 p x n)
+ have ?case if "odd n"
+ proof -
+ from that even_Suc have "Suc n = Suc n div 2 * 2"
+ by presburger
+ then have "x ^ Suc n \<le> (x ^ (Suc n div 2))\<^sup>2"
+ by (simp flip: power_mult)
+ also from that 2 have "\<dots> \<le> (power_up p x (Suc n div 2))\<^sup>2"
+ by (auto intro: power_mono simp del: odd_Suc_div_two)
+ finally show ?thesis
+ using that by (auto intro!: truncate_up_le simp del: odd_Suc_div_two)
+ qed
+ then show ?case
+ by (auto intro!: truncate_up_le mult_left_mono 2)
+qed simp
+
+lemmas power_up_le = order_trans[OF _ power_up]
+ and power_up_less = less_le_trans[OF _ power_up]
+ and power_down_le = order_trans[OF power_down]
+
+lemma power_down_fl: "0 \<le> x \<Longrightarrow> power_down_fl p x n \<le> x ^ n"
+ by transfer (rule power_down)
+
+lemma power_up_fl: "0 \<le> x \<Longrightarrow> x ^ n \<le> power_up_fl p x n"
+ by transfer (rule power_up)
+
+lemma real_power_up_fl: "real_of_float (power_up_fl p x n) = power_up p x n"
+ by transfer simp
+
+lemma real_power_down_fl: "real_of_float (power_down_fl p x n) = power_down p x n"
+ by transfer simp
+
+lemmas [simp del] = power_down.simps(2) power_up.simps(2)
+
+lemmas power_down_simp = power_down.simps(2)
+lemmas power_up_simp = power_up.simps(2)
+
+lemma power_down_even_nonneg: "even n \<Longrightarrow> 0 \<le> power_down p x n"
+ by (induct p x n rule: power_down.induct)
+ (auto simp: power_down_simp simp del: odd_Suc_div_two intro!: truncate_down_nonneg )
+
+lemma power_down_eq_zero_iff[simp]: "power_down prec b n = 0 \<longleftrightarrow> b = 0 \<and> n \<noteq> 0"
+proof (induction n arbitrary: b rule: less_induct)
+ case (less x)
+ then show ?case
+ using power_down_simp[of _ _ "x - 1"]
+ by (cases x) (auto simp add: div2_less_self)
+qed
+
+lemma power_down_nonneg_iff[simp]:
+ "power_down prec b n \<ge> 0 \<longleftrightarrow> even n \<or> b \<ge> 0"
+proof (induction n arbitrary: b rule: less_induct)
+ case (less x)
+ show ?case
+ using less(1)[of "x - 1" b] power_down_simp[of _ _ "x - 1"]
+ by (cases x) (auto simp: algebra_split_simps zero_le_mult_iff)
+qed
+
+lemma power_down_neg_iff[simp]:
+ "power_down prec b n < 0 \<longleftrightarrow>
+ b < 0 \<and> odd n"
+ using power_down_nonneg_iff[of prec b n] by (auto simp del: power_down_nonneg_iff)
+
+lemma power_down_nonpos_iff[simp]:
+ notes [simp del] = power_down_neg_iff power_down_eq_zero_iff
+ shows "power_down prec b n \<le> 0 \<longleftrightarrow> b < 0 \<and> odd n \<or> b = 0 \<and> n \<noteq> 0"
+ using power_down_neg_iff[of prec b n] power_down_eq_zero_iff[of prec b n]
+ by auto
+
+lemma power_down_mono:
+ "power_down prec a n \<le> power_down prec b n"
+ if "((0 \<le> a \<and> a \<le> b)\<or>(odd n \<and> a \<le> b) \<or> (even n \<and> a \<le> 0 \<and> b \<le> a))"
+ using that
+proof (induction n arbitrary: a b rule: less_induct)
+ case (less i)
+ show ?case
+ proof (cases i)
+ case j: (Suc j)
+ note IH = less[unfolded j even_Suc not_not]
+ note [simp del] = power_down.simps
+ show ?thesis
+ proof cases
+ assume [simp]: "even j"
+ have "a * power_down prec a j \<le> b * power_down prec b j"
+ by (smt IH(1) IH(2) \<open>even j\<close> lessI mult_mono' mult_mono_nonpos_nonneg power_down_even_nonneg)
+ then have "truncate_down (Suc prec) (a * power_down prec a j) \<le> truncate_down (Suc prec) (b * power_down prec b j)"
+ by (auto intro!: truncate_down_mono simp: abs_le_square_iff[symmetric] abs_real_def)
+ then show ?thesis
+ unfolding j
+ by (simp add: power_down_simp)
+ next
+ assume [simp]: "odd j"
+ have "power_down prec 0 (Suc (j div 2)) \<le> - power_down prec b (Suc (j div 2))"
+ if "b < 0" "even (j div 2)"
+ apply (rule order_trans[where y=0])
+ using IH that by (auto simp: div2_less_self)
+ then have "truncate_down (Suc prec) ((power_down prec a (Suc (j div 2)))\<^sup>2)
+ \<le> truncate_down (Suc prec) ((power_down prec b (Suc (j div 2)))\<^sup>2)"
+ using IH
+ by (auto intro!: truncate_down_mono intro: order_trans[where y=0]
+ simp: abs_le_square_iff[symmetric] abs_real_def
+ div2_less_self)
+ then show ?thesis
+ unfolding j
+ by (simp add: power_down_simp)
+ qed
+ qed simp
+qed
+
+lemma power_up_even_nonneg: "even n \<Longrightarrow> 0 \<le> power_up p x n"
+ by (induct p x n rule: power_up.induct)
+ (auto simp: power_up.simps simp del: odd_Suc_div_two intro!: )
+
+lemma power_up_eq_zero_iff[simp]: "power_up prec b n = 0 \<longleftrightarrow> b = 0 \<and> n \<noteq> 0"
+proof (induction n arbitrary: b rule: less_induct)
+ case (less x)
+ then show ?case
+ using power_up_simp[of _ _ "x - 1"]
+ by (cases x) (auto simp: algebra_split_simps zero_le_mult_iff div2_less_self)
+qed
+
+lemma power_up_nonneg_iff[simp]:
+ "power_up prec b n \<ge> 0 \<longleftrightarrow> even n \<or> b \<ge> 0"
+proof (induction n arbitrary: b rule: less_induct)
+ case (less x)
+ show ?case
+ using less(1)[of "x - 1" b] power_up_simp[of _ _ "x - 1"]
+ by (cases x) (auto simp: algebra_split_simps zero_le_mult_iff)
+qed
+
+lemma power_up_neg_iff[simp]:
+ "power_up prec b n < 0 \<longleftrightarrow> b < 0 \<and> odd n"
+ using power_up_nonneg_iff[of prec b n] by (auto simp del: power_up_nonneg_iff)
+
+lemma power_up_nonpos_iff[simp]:
+ notes [simp del] = power_up_neg_iff power_up_eq_zero_iff
+ shows "power_up prec b n \<le> 0 \<longleftrightarrow> b < 0 \<and> odd n \<or> b = 0 \<and> n \<noteq> 0"
+ using power_up_neg_iff[of prec b n] power_up_eq_zero_iff[of prec b n]
+ by auto
+
+lemma power_up_mono:
+ "power_up prec a n \<le> power_up prec b n"
+ if "((0 \<le> a \<and> a \<le> b)\<or>(odd n \<and> a \<le> b) \<or> (even n \<and> a \<le> 0 \<and> b \<le> a))"
+ using that
+proof (induction n arbitrary: a b rule: less_induct)
+ case (less i)
+ show ?case
+ proof (cases i)
+ case j: (Suc j)
+ note IH = less[unfolded j even_Suc not_not]
+ note [simp del] = power_up.simps
+ show ?thesis
+ proof cases
+ assume [simp]: "even j"
+ have "a * power_up prec a j \<le> b * power_up prec b j"
+ by (smt IH(1) IH(2) \<open>even j\<close> lessI mult_mono' mult_mono_nonpos_nonneg power_up_even_nonneg)
+ then have "truncate_up prec (a * power_up prec a j) \<le> truncate_up prec (b * power_up prec b j)"
+ by (auto intro!: truncate_up_mono simp: abs_le_square_iff[symmetric] abs_real_def)
+ then show ?thesis
+ unfolding j
+ by (simp add: power_up_simp)
+ next
+ assume [simp]: "odd j"
+ have "power_up prec 0 (Suc (j div 2)) \<le> - power_up prec b (Suc (j div 2))"
+ if "b < 0" "even (j div 2)"
+ apply (rule order_trans[where y=0])
+ using IH that by (auto simp: div2_less_self)
+ then have "truncate_up prec ((power_up prec a (Suc (j div 2)))\<^sup>2)
+ \<le> truncate_up prec ((power_up prec b (Suc (j div 2)))\<^sup>2)"
+ using IH
+ by (auto intro!: truncate_up_mono intro: order_trans[where y=0]
+ simp: abs_le_square_iff[symmetric] abs_real_def
+ div2_less_self)
+ then show ?thesis
+ unfolding j
+ by (simp add: power_up_simp)
+ qed
+ qed simp
+qed
+
subsection \<open>Lemmas needed by Approximate\<close>
@@ -1948,160 +2366,6 @@
"0 \<le> real_of_float x \<Longrightarrow> real_of_float y \<le> 0 \<Longrightarrow> real_of_float (float_divr prec x y) \<le> 0"
by transfer (rule real_divr_nonneg_neg_upper_bound)
-lemma truncate_up_nonneg_mono:
- assumes "0 \<le> x" "x \<le> y"
- shows "truncate_up prec x \<le> truncate_up prec y"
-proof -
- consider "\<lfloor>log 2 x\<rfloor> = \<lfloor>log 2 y\<rfloor>" | "\<lfloor>log 2 x\<rfloor> \<noteq> \<lfloor>log 2 y\<rfloor>" "0 < x" | "x \<le> 0"
- by arith
- then show ?thesis
- proof cases
- case 1
- then show ?thesis
- using assms
- by (auto simp: truncate_up_def round_up_def intro!: ceiling_mono)
- next
- case 2
- from assms \<open>0 < x\<close> have "log 2 x \<le> log 2 y"
- by auto
- with \<open>\<lfloor>log 2 x\<rfloor> \<noteq> \<lfloor>log 2 y\<rfloor>\<close>
- have logless: "log 2 x < log 2 y"
- by linarith
- have flogless: "\<lfloor>log 2 x\<rfloor> < \<lfloor>log 2 y\<rfloor>"
- using \<open>\<lfloor>log 2 x\<rfloor> \<noteq> \<lfloor>log 2 y\<rfloor>\<close> \<open>log 2 x \<le> log 2 y\<close> by linarith
- have "truncate_up prec x =
- real_of_int \<lceil>x * 2 powr real_of_int (int prec - \<lfloor>log 2 x\<rfloor> )\<rceil> * 2 powr - real_of_int (int prec - \<lfloor>log 2 x\<rfloor>)"
- using assms by (simp add: truncate_up_def round_up_def)
- also have "\<lceil>x * 2 powr real_of_int (int prec - \<lfloor>log 2 x\<rfloor>)\<rceil> \<le> (2 ^ (Suc prec))"
- proof (simp only: ceiling_le_iff)
- have "x * 2 powr real_of_int (int prec - \<lfloor>log 2 x\<rfloor>) \<le>
- x * (2 powr real (Suc prec) / (2 powr log 2 x))"
- using real_of_int_floor_add_one_ge[of "log 2 x"] assms
- by (auto simp: algebra_simps simp flip: powr_diff intro!: mult_left_mono)
- then show "x * 2 powr real_of_int (int prec - \<lfloor>log 2 x\<rfloor>) \<le> real_of_int ((2::int) ^ (Suc prec))"
- using \<open>0 < x\<close> by (simp add: powr_realpow powr_add)
- qed
- then have "real_of_int \<lceil>x * 2 powr real_of_int (int prec - \<lfloor>log 2 x\<rfloor>)\<rceil> \<le> 2 powr int (Suc prec)"
- by (auto simp: powr_realpow powr_add)
- (metis power_Suc of_int_le_numeral_power_cancel_iff)
- also
- have "2 powr - real_of_int (int prec - \<lfloor>log 2 x\<rfloor>) \<le> 2 powr - real_of_int (int prec - \<lfloor>log 2 y\<rfloor> + 1)"
- using logless flogless by (auto intro!: floor_mono)
- also have "2 powr real_of_int (int (Suc prec)) \<le>
- 2 powr (log 2 y + real_of_int (int prec - \<lfloor>log 2 y\<rfloor> + 1))"
- using assms \<open>0 < x\<close>
- by (auto simp: algebra_simps)
- finally have "truncate_up prec x \<le>
- 2 powr (log 2 y + real_of_int (int prec - \<lfloor>log 2 y\<rfloor> + 1)) * 2 powr - real_of_int (int prec - \<lfloor>log 2 y\<rfloor> + 1)"
- by simp
- also have "\<dots> = 2 powr (log 2 y + real_of_int (int prec - \<lfloor>log 2 y\<rfloor>) - real_of_int (int prec - \<lfloor>log 2 y\<rfloor>))"
- by (subst powr_add[symmetric]) simp
- also have "\<dots> = y"
- using \<open>0 < x\<close> assms
- by (simp add: powr_add)
- also have "\<dots> \<le> truncate_up prec y"
- by (rule truncate_up)
- finally show ?thesis .
- next
- case 3
- then show ?thesis
- using assms
- by (auto intro!: truncate_up_le)
- qed
-qed
-
-lemma truncate_up_switch_sign_mono:
- assumes "x \<le> 0" "0 \<le> y"
- shows "truncate_up prec x \<le> truncate_up prec y"
-proof -
- note truncate_up_nonpos[OF \<open>x \<le> 0\<close>]
- also note truncate_up_le[OF \<open>0 \<le> y\<close>]
- finally show ?thesis .
-qed
-
-lemma truncate_down_switch_sign_mono:
- assumes "x \<le> 0"
- and "0 \<le> y"
- and "x \<le> y"
- shows "truncate_down prec x \<le> truncate_down prec y"
-proof -
- note truncate_down_le[OF \<open>x \<le> 0\<close>]
- also note truncate_down_nonneg[OF \<open>0 \<le> y\<close>]
- finally show ?thesis .
-qed
-
-lemma truncate_down_nonneg_mono:
- assumes "0 \<le> x" "x \<le> y"
- shows "truncate_down prec x \<le> truncate_down prec y"
-proof -
- consider "x \<le> 0" | "\<lfloor>log 2 \<bar>x\<bar>\<rfloor> = \<lfloor>log 2 \<bar>y\<bar>\<rfloor>" |
- "0 < x" "\<lfloor>log 2 \<bar>x\<bar>\<rfloor> \<noteq> \<lfloor>log 2 \<bar>y\<bar>\<rfloor>"
- by arith
- then show ?thesis
- proof cases
- case 1
- with assms have "x = 0" "0 \<le> y" by simp_all
- then show ?thesis
- by (auto intro!: truncate_down_nonneg)
- next
- case 2
- then show ?thesis
- using assms
- by (auto simp: truncate_down_def round_down_def intro!: floor_mono)
- next
- case 3
- from \<open>0 < x\<close> have "log 2 x \<le> log 2 y" "0 < y" "0 \<le> y"
- using assms by auto
- with \<open>\<lfloor>log 2 \<bar>x\<bar>\<rfloor> \<noteq> \<lfloor>log 2 \<bar>y\<bar>\<rfloor>\<close>
- have logless: "log 2 x < log 2 y" and flogless: "\<lfloor>log 2 x\<rfloor> < \<lfloor>log 2 y\<rfloor>"
- unfolding atomize_conj abs_of_pos[OF \<open>0 < x\<close>] abs_of_pos[OF \<open>0 < y\<close>]
- by (metis floor_less_cancel linorder_cases not_le)
- have "2 powr prec \<le> y * 2 powr real prec / (2 powr log 2 y)"
- using \<open>0 < y\<close> by simp
- also have "\<dots> \<le> y * 2 powr real (Suc prec) / (2 powr (real_of_int \<lfloor>log 2 y\<rfloor> + 1))"
- using \<open>0 \<le> y\<close> \<open>0 \<le> x\<close> assms(2)
- by (auto intro!: powr_mono divide_left_mono
- simp: of_nat_diff powr_add powr_diff)
- also have "\<dots> = y * 2 powr real (Suc prec) / (2 powr real_of_int \<lfloor>log 2 y\<rfloor> * 2)"
- by (auto simp: powr_add)
- finally have "(2 ^ prec) \<le> \<lfloor>y * 2 powr real_of_int (int (Suc prec) - \<lfloor>log 2 \<bar>y\<bar>\<rfloor> - 1)\<rfloor>"
- using \<open>0 \<le> y\<close>
- by (auto simp: powr_diff le_floor_iff powr_realpow powr_add)
- then have "(2 ^ (prec)) * 2 powr - real_of_int (int prec - \<lfloor>log 2 \<bar>y\<bar>\<rfloor>) \<le> truncate_down prec y"
- by (auto simp: truncate_down_def round_down_def)
- moreover have "x \<le> (2 ^ prec) * 2 powr - real_of_int (int prec - \<lfloor>log 2 \<bar>y\<bar>\<rfloor>)"
- proof -
- have "x = 2 powr (log 2 \<bar>x\<bar>)" using \<open>0 < x\<close> by simp
- also have "\<dots> \<le> (2 ^ (Suc prec )) * 2 powr - real_of_int (int prec - \<lfloor>log 2 \<bar>x\<bar>\<rfloor>)"
- using real_of_int_floor_add_one_ge[of "log 2 \<bar>x\<bar>"] \<open>0 < x\<close>
- by (auto simp flip: powr_realpow powr_add simp: algebra_simps powr_mult_base le_powr_iff)
- also
- have "2 powr - real_of_int (int prec - \<lfloor>log 2 \<bar>x\<bar>\<rfloor>) \<le> 2 powr - real_of_int (int prec - \<lfloor>log 2 \<bar>y\<bar>\<rfloor> + 1)"
- using logless flogless \<open>x > 0\<close> \<open>y > 0\<close>
- by (auto intro!: floor_mono)
- finally show ?thesis
- by (auto simp flip: powr_realpow simp: powr_diff assms of_nat_diff)
- qed
- ultimately show ?thesis
- by (metis dual_order.trans truncate_down)
- qed
-qed
-
-lemma truncate_down_eq_truncate_up: "truncate_down p x = - truncate_up p (-x)"
- and truncate_up_eq_truncate_down: "truncate_up p x = - truncate_down p (-x)"
- by (auto simp: truncate_up_uminus_eq truncate_down_uminus_eq)
-
-lemma truncate_down_mono: "x \<le> y \<Longrightarrow> truncate_down p x \<le> truncate_down p y"
- apply (cases "0 \<le> x")
- apply (rule truncate_down_nonneg_mono, assumption+)
- apply (simp add: truncate_down_eq_truncate_up)
- apply (cases "0 \<le> y")
- apply (auto intro: truncate_up_nonneg_mono truncate_up_switch_sign_mono)
- done
-
-lemma truncate_up_mono: "x \<le> y \<Longrightarrow> truncate_up p x \<le> truncate_up p y"
- by (simp add: truncate_up_eq_truncate_down truncate_down_mono)
-
lemma Float_le_zero_iff: "Float a b \<le> 0 \<longleftrightarrow> a \<le> 0"
by (auto simp: zero_float_def mult_le_0_iff)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Interval_Float.thy Sun Nov 03 19:58:02 2019 -0500
@@ -0,0 +1,289 @@
+section \<open>Approximate Operations on Intervals of Floating Point Numbers\<close>
+theory Interval_Float
+ imports
+ Interval
+ Float
+begin
+
+definition "split_float_interval x = split_interval x ((lower x + upper x) * Float 1 (-1))"
+
+lemma split_float_intervalD: "split_float_interval X = (A, B) \<Longrightarrow> set_of X \<subseteq> set_of A \<union> set_of B"
+ by (auto dest!: split_intervalD simp: split_float_interval_def)
+
+lemmas float_round_down_le[intro] = order_trans[OF float_round_down]
+ and float_round_up_ge[intro] = order_trans[OF _ float_round_up]
+
+definition mid :: "float interval \<Rightarrow> float"
+ where "mid i = (lower i + upper i) * Float 1 (-1)"
+
+lemma mid_in_interval: "mid i \<in>\<^sub>i i"
+ using lower_le_upper[of i]
+ by (auto simp: mid_def set_of_eq powr_minus)
+
+definition centered :: "float interval \<Rightarrow> float interval"
+ where "centered i = i - interval_of (mid i)"
+
+text \<open>TODO: many of the lemmas should move to theories Float or Approximation
+ (the latter should be based on type @{type interval}.\<close>
+
+subsection "Intervals with Floating Point Bounds"
+
+context includes interval.lifting begin
+
+lift_definition round_interval :: "nat \<Rightarrow> float interval \<Rightarrow> float interval"
+ is "\<lambda>p. \<lambda>(l, u). (float_round_down p l, float_round_up p u)"
+ by (auto simp: intro!: float_round_down_le float_round_up_le)
+
+lemma lower_round_ivl[simp]: "lower (round_interval p x) = float_round_down p (lower x)"
+ by transfer auto
+lemma upper_round_ivl[simp]: "upper (round_interval p x) = float_round_up p (upper x)"
+ by transfer auto
+
+lemma round_ivl_correct: "set_of A \<subseteq> set_of (round_interval prec A)"
+ by (auto simp: set_of_eq float_round_down_le float_round_up_le)
+
+lift_definition truncate_ivl :: "nat \<Rightarrow> real interval \<Rightarrow> real interval"
+ is "\<lambda>p. \<lambda>(l, u). (truncate_down p l, truncate_up p u)"
+ by (auto intro!: truncate_down_le truncate_up_le)
+
+lemma lower_truncate_ivl[simp]: "lower (truncate_ivl p x) = truncate_down p (lower x)"
+ by transfer auto
+lemma upper_truncate_ivl[simp]: "upper (truncate_ivl p x) = truncate_up p (upper x)"
+ by transfer auto
+
+lemma truncate_ivl_correct: "set_of A \<subseteq> set_of (truncate_ivl prec A)"
+ by (auto simp: set_of_eq intro!: truncate_down_le truncate_up_le)
+
+lift_definition real_interval::"float interval \<Rightarrow> real interval"
+ is "\<lambda>(l, u). (real_of_float l, real_of_float u)"
+ by auto
+
+lemma lower_real_interval[simp]: "lower (real_interval x) = lower x"
+ by transfer auto
+lemma upper_real_interval[simp]: "upper (real_interval x) = upper x"
+ by transfer auto
+
+definition "set_of' x = (case x of None \<Rightarrow> UNIV | Some i \<Rightarrow> set_of (real_interval i))"
+
+lemma real_interval_min_interval[simp]:
+ "real_interval (min_interval a b) = min_interval (real_interval a) (real_interval b)"
+ by (auto simp: interval_eq_set_of_iff set_of_eq real_of_float_min)
+
+lemma real_interval_max_interval[simp]:
+ "real_interval (max_interval a b) = max_interval (real_interval a) (real_interval b)"
+ by (auto simp: interval_eq_set_of_iff set_of_eq real_of_float_max)
+
+lemma in_intervalI:
+ "x \<in>\<^sub>i X" if "lower X \<le> x" "x \<le> upper X"
+ using that by (auto simp: set_of_eq)
+
+abbreviation in_real_interval ("(_/ \<in>\<^sub>r _)" [51, 51] 50) where
+ "x \<in>\<^sub>r X \<equiv> x \<in>\<^sub>i real_interval X"
+
+lemma in_real_intervalI:
+ "x \<in>\<^sub>r X" if "lower X \<le> x" "x \<le> upper X" for x::real and X::"float interval"
+ using that
+ by (intro in_intervalI) auto
+
+lemma lower_Interval: "lower (Interval x) = fst x"
+ and upper_Interval: "upper (Interval x) = snd x"
+ if "fst x \<le> snd x"
+ using that
+ by (auto simp: lower_def upper_def Interval_inverse split_beta')
+
+definition all_in_i :: "'a::preorder list \<Rightarrow> 'a interval list \<Rightarrow> bool"
+ (infix "(all'_in\<^sub>i)" 50)
+ where "x all_in\<^sub>i I = (length x = length I \<and> (\<forall>i < length I. x ! i \<in>\<^sub>i I ! i))"
+
+definition all_in :: "real list \<Rightarrow> float interval list \<Rightarrow> bool"
+ (infix "(all'_in)" 50)
+ where "x all_in I = (length x = length I \<and> (\<forall>i < length I. x ! i \<in>\<^sub>r I ! i))"
+
+definition all_subset :: "'a::order interval list \<Rightarrow> 'a interval list \<Rightarrow> bool"
+ (infix "(all'_subset)" 50)
+ where "I all_subset J = (length I = length J \<and> (\<forall>i < length I. set_of (I!i) \<subseteq> set_of (J!i)))"
+
+lemmas [simp] = all_in_def all_subset_def
+
+lemma all_subsetD:
+ assumes "I all_subset J"
+ assumes "x all_in I"
+ shows "x all_in J"
+ using assms
+ by (auto simp: set_of_eq; fastforce)
+
+lemma round_interval_mono: "set_of (round_interval prec X) \<subseteq> set_of (round_interval prec Y)"
+ if "set_of X \<subseteq> set_of Y"
+ using that
+ by transfer
+ (auto simp: float_round_down.rep_eq float_round_up.rep_eq truncate_down_mono truncate_up_mono)
+
+lemma Ivl_simps[simp]: "lower (Ivl a b) = min a b" "upper (Ivl a b) = b"
+ subgoal by transfer simp
+ subgoal by transfer simp
+ done
+
+lemma set_of_subset_iff: "set_of X \<subseteq> set_of Y \<longleftrightarrow> lower Y \<le> lower X \<and> upper X \<le> upper Y"
+ for X Y::"'a::linorder interval"
+ by (auto simp: set_of_eq subset_iff)
+
+lemma bounds_of_interval_eq_lower_upper:
+ "bounds_of_interval ivl = (lower ivl, upper ivl)" if "lower ivl \<le> upper ivl"
+ using that
+ by (auto simp: lower.rep_eq upper.rep_eq)
+
+lemma real_interval_Ivl: "real_interval (Ivl a b) = Ivl a b"
+ by transfer (auto simp: min_def)
+
+lemma set_of_mul_contains_real_zero:
+ "0 \<in>\<^sub>r (A * B)" if "0 \<in>\<^sub>r A \<or> 0 \<in>\<^sub>r B"
+ using that set_of_mul_contains_zero[of A B]
+ by (auto simp: set_of_eq)
+
+fun subdivide_interval :: "nat \<Rightarrow> float interval \<Rightarrow> float interval list"
+ where "subdivide_interval 0 I = [I]"
+ | "subdivide_interval (Suc n) I = (
+ let m = mid I
+ in (subdivide_interval n (Ivl (lower I) m)) @ (subdivide_interval n (Ivl m (upper I)))
+ )"
+
+lemma subdivide_interval_length:
+ shows "length (subdivide_interval n I) = 2^n"
+ by(induction n arbitrary: I, simp_all add: Let_def)
+
+lemma lower_le_mid: "lower x \<le> mid x" "real_of_float (lower x) \<le> mid x"
+ and mid_le_upper: "mid x \<le> upper x" "real_of_float (mid x) \<le> upper x"
+ unfolding mid_def
+ subgoal by transfer (auto simp: powr_neg_one)
+ subgoal by transfer (auto simp: powr_neg_one)
+ subgoal by transfer (auto simp: powr_neg_one)
+ subgoal by transfer (auto simp: powr_neg_one)
+ done
+
+lemma subdivide_interval_correct:
+ "list_ex (\<lambda>i. x \<in>\<^sub>r i) (subdivide_interval n I)" if "x \<in>\<^sub>r I" for x::real
+ using that
+proof(induction n arbitrary: x I)
+ case 0
+ then show ?case by simp
+next
+ case (Suc n)
+ from \<open>x \<in>\<^sub>r I\<close> consider "x \<in>\<^sub>r Ivl (lower I) (mid I)" | "x \<in>\<^sub>r Ivl (mid I) (upper I)"
+ by (cases "x \<le> real_of_float (mid I)")
+ (auto simp: set_of_eq min_def lower_le_mid mid_le_upper)
+ from this[case_names lower upper] show ?case
+ by cases (use Suc.IH in \<open>auto simp: Let_def\<close>)
+qed
+
+fun interval_list_union :: "'a::lattice interval list \<Rightarrow> 'a interval"
+ where "interval_list_union [] = undefined"
+ | "interval_list_union [I] = I"
+ | "interval_list_union (I#Is) = sup I (interval_list_union Is)"
+
+lemma interval_list_union_correct:
+ assumes "S \<noteq> []"
+ assumes "i < length S"
+ shows "set_of (S!i) \<subseteq> set_of (interval_list_union S)"
+ using assms
+proof(induction S arbitrary: i)
+ case (Cons a S i)
+ thus ?case
+ proof(cases S)
+ fix b S'
+ assume "S = b # S'"
+ hence "S \<noteq> []"
+ by simp
+ show ?thesis
+ proof(cases i)
+ case 0
+ show ?thesis
+ apply(cases S)
+ using interval_union_mono1
+ by (auto simp add: 0)
+ next
+ case (Suc i_prev)
+ hence "i_prev < length S"
+ using Cons(3) by simp
+
+ from Cons(1)[OF \<open>S \<noteq> []\<close> this] Cons(1)
+ have "set_of ((a # S) ! i) \<subseteq> set_of (interval_list_union S)"
+ by (simp add: \<open>i = Suc i_prev\<close>)
+ also have "... \<subseteq> set_of (interval_list_union (a # S))"
+ using \<open>S \<noteq> []\<close>
+ apply(cases S)
+ using interval_union_mono2
+ by auto
+ finally show ?thesis .
+ qed
+ qed simp
+qed simp
+
+lemma split_domain_correct:
+ fixes x :: "real list"
+ assumes "x all_in I"
+ assumes split_correct: "\<And>x a I. x \<in>\<^sub>r I \<Longrightarrow> list_ex (\<lambda>i::float interval. x \<in>\<^sub>r i) (split I)"
+ shows "list_ex (\<lambda>s. x all_in s) (split_domain split I)"
+ using assms(1)
+proof(induction I arbitrary: x)
+ case (Cons I Is x)
+ have "x \<noteq> []"
+ using Cons(2) by auto
+ obtain x' xs where x_decomp: "x = x' # xs"
+ using \<open>x \<noteq> []\<close> list.exhaust by auto
+ hence "x' \<in>\<^sub>r I" "xs all_in Is"
+ using Cons(2)
+ by auto
+ show ?case
+ using Cons(1)[OF \<open>xs all_in Is\<close>]
+ split_correct[OF \<open>x' \<in>\<^sub>r I\<close>]
+ apply (auto simp add: list_ex_iff set_of_eq)
+ by (smt length_Cons less_Suc_eq_0_disj nth_Cons_0 nth_Cons_Suc x_decomp)
+qed simp
+
+
+lift_definition(code_dt) inverse_float_interval::"nat \<Rightarrow> float interval \<Rightarrow> float interval option" is
+ "\<lambda>prec (l, u). if (0 < l \<or> u < 0) then Some (float_divl prec 1 u, float_divr prec 1 l) else None"
+ by (auto intro!: order_trans[OF float_divl] order_trans[OF _ float_divr]
+ simp: divide_simps)
+
+lemma inverse_float_interval_eq_Some_conv:
+ defines "one \<equiv> (1::float)"
+ shows
+ "inverse_float_interval p X = Some R \<longleftrightarrow>
+ (lower X > 0 \<or> upper X < 0) \<and>
+ lower R = float_divl p one (upper X) \<and>
+ upper R = float_divr p one (lower X)"
+ by clarsimp (transfer fixing: one, force simp: one_def split: if_splits)
+
+lemma inverse_float_interval:
+ "inverse ` set_of (real_interval X) \<subseteq> set_of (real_interval Y)"
+ if "inverse_float_interval p X = Some Y"
+ using that
+ apply (clarsimp simp: set_of_eq inverse_float_interval_eq_Some_conv)
+ by (intro order_trans[OF float_divl] order_trans[OF _ float_divr] conjI)
+ (auto simp: divide_simps)
+
+lemma inverse_float_intervalI:
+ "x \<in>\<^sub>r X \<Longrightarrow> inverse x \<in> set_of' (inverse_float_interval p X)"
+ using inverse_float_interval[of p X]
+ by (auto simp: set_of'_def split: option.splits)
+
+lemma real_interval_abs_interval[simp]:
+ "real_interval (abs_interval x) = abs_interval (real_interval x)"
+ by (auto simp: interval_eq_set_of_iff set_of_eq real_of_float_max real_of_float_min)
+
+lift_definition floor_float_interval::"float interval \<Rightarrow> float interval" is
+ "\<lambda>(l, u). (floor_fl l, floor_fl u)"
+ by (auto intro!: floor_mono simp: floor_fl.rep_eq)
+
+lemma lower_floor_float_interval[simp]: "lower (floor_float_interval x) = floor_fl (lower x)"
+ by transfer auto
+lemma upper_floor_float_interval[simp]: "upper (floor_float_interval x) = floor_fl (upper x)"
+ by transfer auto
+
+lemma floor_float_intervalI: "\<lfloor>x\<rfloor> \<in>\<^sub>r floor_float_interval X" if "x \<in>\<^sub>r X"
+ using that by (auto simp: set_of_eq floor_fl_def floor_mono)
+
+end
+
+end
\ No newline at end of file
--- a/src/HOL/Library/Library.thy Sun Oct 27 21:51:14 2019 -0400
+++ b/src/HOL/Library/Library.thy Sun Nov 03 19:58:02 2019 -0500
@@ -39,6 +39,7 @@
Indicator_Function
Infinite_Set
Interval
+ Interval_Float
IArray
Landau_Symbols
Lattice_Algebras