71036
|
1 |
section \<open>Approximate Operations on Intervals of Floating Point Numbers\<close>
|
|
2 |
theory Interval_Float
|
|
3 |
imports
|
|
4 |
Interval
|
|
5 |
Float
|
|
6 |
begin
|
|
7 |
|
|
8 |
definition "split_float_interval x = split_interval x ((lower x + upper x) * Float 1 (-1))"
|
|
9 |
|
|
10 |
lemma split_float_intervalD: "split_float_interval X = (A, B) \<Longrightarrow> set_of X \<subseteq> set_of A \<union> set_of B"
|
|
11 |
by (auto dest!: split_intervalD simp: split_float_interval_def)
|
|
12 |
|
|
13 |
lemmas float_round_down_le[intro] = order_trans[OF float_round_down]
|
|
14 |
and float_round_up_ge[intro] = order_trans[OF _ float_round_up]
|
|
15 |
|
|
16 |
definition mid :: "float interval \<Rightarrow> float"
|
|
17 |
where "mid i = (lower i + upper i) * Float 1 (-1)"
|
|
18 |
|
|
19 |
lemma mid_in_interval: "mid i \<in>\<^sub>i i"
|
|
20 |
using lower_le_upper[of i]
|
|
21 |
by (auto simp: mid_def set_of_eq powr_minus)
|
|
22 |
|
|
23 |
definition centered :: "float interval \<Rightarrow> float interval"
|
|
24 |
where "centered i = i - interval_of (mid i)"
|
|
25 |
|
|
26 |
text \<open>TODO: many of the lemmas should move to theories Float or Approximation
|
|
27 |
(the latter should be based on type @{type interval}.\<close>
|
|
28 |
|
|
29 |
subsection "Intervals with Floating Point Bounds"
|
|
30 |
|
|
31 |
context includes interval.lifting begin
|
|
32 |
|
|
33 |
lift_definition round_interval :: "nat \<Rightarrow> float interval \<Rightarrow> float interval"
|
|
34 |
is "\<lambda>p. \<lambda>(l, u). (float_round_down p l, float_round_up p u)"
|
|
35 |
by (auto simp: intro!: float_round_down_le float_round_up_le)
|
|
36 |
|
|
37 |
lemma lower_round_ivl[simp]: "lower (round_interval p x) = float_round_down p (lower x)"
|
|
38 |
by transfer auto
|
|
39 |
lemma upper_round_ivl[simp]: "upper (round_interval p x) = float_round_up p (upper x)"
|
|
40 |
by transfer auto
|
|
41 |
|
|
42 |
lemma round_ivl_correct: "set_of A \<subseteq> set_of (round_interval prec A)"
|
|
43 |
by (auto simp: set_of_eq float_round_down_le float_round_up_le)
|
|
44 |
|
|
45 |
lift_definition truncate_ivl :: "nat \<Rightarrow> real interval \<Rightarrow> real interval"
|
|
46 |
is "\<lambda>p. \<lambda>(l, u). (truncate_down p l, truncate_up p u)"
|
|
47 |
by (auto intro!: truncate_down_le truncate_up_le)
|
|
48 |
|
|
49 |
lemma lower_truncate_ivl[simp]: "lower (truncate_ivl p x) = truncate_down p (lower x)"
|
|
50 |
by transfer auto
|
|
51 |
lemma upper_truncate_ivl[simp]: "upper (truncate_ivl p x) = truncate_up p (upper x)"
|
|
52 |
by transfer auto
|
|
53 |
|
|
54 |
lemma truncate_ivl_correct: "set_of A \<subseteq> set_of (truncate_ivl prec A)"
|
|
55 |
by (auto simp: set_of_eq intro!: truncate_down_le truncate_up_le)
|
|
56 |
|
|
57 |
lift_definition real_interval::"float interval \<Rightarrow> real interval"
|
|
58 |
is "\<lambda>(l, u). (real_of_float l, real_of_float u)"
|
|
59 |
by auto
|
|
60 |
|
|
61 |
lemma lower_real_interval[simp]: "lower (real_interval x) = lower x"
|
|
62 |
by transfer auto
|
|
63 |
lemma upper_real_interval[simp]: "upper (real_interval x) = upper x"
|
|
64 |
by transfer auto
|
|
65 |
|
|
66 |
definition "set_of' x = (case x of None \<Rightarrow> UNIV | Some i \<Rightarrow> set_of (real_interval i))"
|
|
67 |
|
|
68 |
lemma real_interval_min_interval[simp]:
|
|
69 |
"real_interval (min_interval a b) = min_interval (real_interval a) (real_interval b)"
|
|
70 |
by (auto simp: interval_eq_set_of_iff set_of_eq real_of_float_min)
|
|
71 |
|
|
72 |
lemma real_interval_max_interval[simp]:
|
|
73 |
"real_interval (max_interval a b) = max_interval (real_interval a) (real_interval b)"
|
|
74 |
by (auto simp: interval_eq_set_of_iff set_of_eq real_of_float_max)
|
|
75 |
|
|
76 |
lemma in_intervalI:
|
|
77 |
"x \<in>\<^sub>i X" if "lower X \<le> x" "x \<le> upper X"
|
|
78 |
using that by (auto simp: set_of_eq)
|
|
79 |
|
|
80 |
abbreviation in_real_interval ("(_/ \<in>\<^sub>r _)" [51, 51] 50) where
|
|
81 |
"x \<in>\<^sub>r X \<equiv> x \<in>\<^sub>i real_interval X"
|
|
82 |
|
|
83 |
lemma in_real_intervalI:
|
|
84 |
"x \<in>\<^sub>r X" if "lower X \<le> x" "x \<le> upper X" for x::real and X::"float interval"
|
|
85 |
using that
|
|
86 |
by (intro in_intervalI) auto
|
|
87 |
|
|
88 |
lemma lower_Interval: "lower (Interval x) = fst x"
|
|
89 |
and upper_Interval: "upper (Interval x) = snd x"
|
|
90 |
if "fst x \<le> snd x"
|
|
91 |
using that
|
|
92 |
by (auto simp: lower_def upper_def Interval_inverse split_beta')
|
|
93 |
|
|
94 |
definition all_in_i :: "'a::preorder list \<Rightarrow> 'a interval list \<Rightarrow> bool"
|
|
95 |
(infix "(all'_in\<^sub>i)" 50)
|
|
96 |
where "x all_in\<^sub>i I = (length x = length I \<and> (\<forall>i < length I. x ! i \<in>\<^sub>i I ! i))"
|
|
97 |
|
|
98 |
definition all_in :: "real list \<Rightarrow> float interval list \<Rightarrow> bool"
|
|
99 |
(infix "(all'_in)" 50)
|
|
100 |
where "x all_in I = (length x = length I \<and> (\<forall>i < length I. x ! i \<in>\<^sub>r I ! i))"
|
|
101 |
|
|
102 |
definition all_subset :: "'a::order interval list \<Rightarrow> 'a interval list \<Rightarrow> bool"
|
|
103 |
(infix "(all'_subset)" 50)
|
|
104 |
where "I all_subset J = (length I = length J \<and> (\<forall>i < length I. set_of (I!i) \<subseteq> set_of (J!i)))"
|
|
105 |
|
|
106 |
lemmas [simp] = all_in_def all_subset_def
|
|
107 |
|
|
108 |
lemma all_subsetD:
|
|
109 |
assumes "I all_subset J"
|
|
110 |
assumes "x all_in I"
|
|
111 |
shows "x all_in J"
|
|
112 |
using assms
|
|
113 |
by (auto simp: set_of_eq; fastforce)
|
|
114 |
|
|
115 |
lemma round_interval_mono: "set_of (round_interval prec X) \<subseteq> set_of (round_interval prec Y)"
|
|
116 |
if "set_of X \<subseteq> set_of Y"
|
|
117 |
using that
|
|
118 |
by transfer
|
|
119 |
(auto simp: float_round_down.rep_eq float_round_up.rep_eq truncate_down_mono truncate_up_mono)
|
|
120 |
|
|
121 |
lemma Ivl_simps[simp]: "lower (Ivl a b) = min a b" "upper (Ivl a b) = b"
|
|
122 |
subgoal by transfer simp
|
|
123 |
subgoal by transfer simp
|
|
124 |
done
|
|
125 |
|
|
126 |
lemma set_of_subset_iff: "set_of X \<subseteq> set_of Y \<longleftrightarrow> lower Y \<le> lower X \<and> upper X \<le> upper Y"
|
|
127 |
for X Y::"'a::linorder interval"
|
|
128 |
by (auto simp: set_of_eq subset_iff)
|
|
129 |
|
|
130 |
lemma bounds_of_interval_eq_lower_upper:
|
|
131 |
"bounds_of_interval ivl = (lower ivl, upper ivl)" if "lower ivl \<le> upper ivl"
|
|
132 |
using that
|
|
133 |
by (auto simp: lower.rep_eq upper.rep_eq)
|
|
134 |
|
|
135 |
lemma real_interval_Ivl: "real_interval (Ivl a b) = Ivl a b"
|
|
136 |
by transfer (auto simp: min_def)
|
|
137 |
|
|
138 |
lemma set_of_mul_contains_real_zero:
|
|
139 |
"0 \<in>\<^sub>r (A * B)" if "0 \<in>\<^sub>r A \<or> 0 \<in>\<^sub>r B"
|
|
140 |
using that set_of_mul_contains_zero[of A B]
|
|
141 |
by (auto simp: set_of_eq)
|
|
142 |
|
|
143 |
fun subdivide_interval :: "nat \<Rightarrow> float interval \<Rightarrow> float interval list"
|
|
144 |
where "subdivide_interval 0 I = [I]"
|
|
145 |
| "subdivide_interval (Suc n) I = (
|
|
146 |
let m = mid I
|
|
147 |
in (subdivide_interval n (Ivl (lower I) m)) @ (subdivide_interval n (Ivl m (upper I)))
|
|
148 |
)"
|
|
149 |
|
|
150 |
lemma subdivide_interval_length:
|
|
151 |
shows "length (subdivide_interval n I) = 2^n"
|
|
152 |
by(induction n arbitrary: I, simp_all add: Let_def)
|
|
153 |
|
|
154 |
lemma lower_le_mid: "lower x \<le> mid x" "real_of_float (lower x) \<le> mid x"
|
|
155 |
and mid_le_upper: "mid x \<le> upper x" "real_of_float (mid x) \<le> upper x"
|
|
156 |
unfolding mid_def
|
|
157 |
subgoal by transfer (auto simp: powr_neg_one)
|
|
158 |
subgoal by transfer (auto simp: powr_neg_one)
|
|
159 |
subgoal by transfer (auto simp: powr_neg_one)
|
|
160 |
subgoal by transfer (auto simp: powr_neg_one)
|
|
161 |
done
|
|
162 |
|
|
163 |
lemma subdivide_interval_correct:
|
|
164 |
"list_ex (\<lambda>i. x \<in>\<^sub>r i) (subdivide_interval n I)" if "x \<in>\<^sub>r I" for x::real
|
|
165 |
using that
|
|
166 |
proof(induction n arbitrary: x I)
|
|
167 |
case 0
|
|
168 |
then show ?case by simp
|
|
169 |
next
|
|
170 |
case (Suc n)
|
|
171 |
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)"
|
|
172 |
by (cases "x \<le> real_of_float (mid I)")
|
|
173 |
(auto simp: set_of_eq min_def lower_le_mid mid_le_upper)
|
|
174 |
from this[case_names lower upper] show ?case
|
|
175 |
by cases (use Suc.IH in \<open>auto simp: Let_def\<close>)
|
|
176 |
qed
|
|
177 |
|
|
178 |
fun interval_list_union :: "'a::lattice interval list \<Rightarrow> 'a interval"
|
|
179 |
where "interval_list_union [] = undefined"
|
|
180 |
| "interval_list_union [I] = I"
|
|
181 |
| "interval_list_union (I#Is) = sup I (interval_list_union Is)"
|
|
182 |
|
|
183 |
lemma interval_list_union_correct:
|
|
184 |
assumes "S \<noteq> []"
|
|
185 |
assumes "i < length S"
|
|
186 |
shows "set_of (S!i) \<subseteq> set_of (interval_list_union S)"
|
|
187 |
using assms
|
|
188 |
proof(induction S arbitrary: i)
|
|
189 |
case (Cons a S i)
|
|
190 |
thus ?case
|
|
191 |
proof(cases S)
|
|
192 |
fix b S'
|
|
193 |
assume "S = b # S'"
|
|
194 |
hence "S \<noteq> []"
|
|
195 |
by simp
|
|
196 |
show ?thesis
|
|
197 |
proof(cases i)
|
|
198 |
case 0
|
|
199 |
show ?thesis
|
|
200 |
apply(cases S)
|
|
201 |
using interval_union_mono1
|
|
202 |
by (auto simp add: 0)
|
|
203 |
next
|
|
204 |
case (Suc i_prev)
|
|
205 |
hence "i_prev < length S"
|
|
206 |
using Cons(3) by simp
|
|
207 |
|
|
208 |
from Cons(1)[OF \<open>S \<noteq> []\<close> this] Cons(1)
|
|
209 |
have "set_of ((a # S) ! i) \<subseteq> set_of (interval_list_union S)"
|
|
210 |
by (simp add: \<open>i = Suc i_prev\<close>)
|
|
211 |
also have "... \<subseteq> set_of (interval_list_union (a # S))"
|
|
212 |
using \<open>S \<noteq> []\<close>
|
|
213 |
apply(cases S)
|
|
214 |
using interval_union_mono2
|
|
215 |
by auto
|
|
216 |
finally show ?thesis .
|
|
217 |
qed
|
|
218 |
qed simp
|
|
219 |
qed simp
|
|
220 |
|
|
221 |
lemma split_domain_correct:
|
|
222 |
fixes x :: "real list"
|
|
223 |
assumes "x all_in I"
|
|
224 |
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)"
|
|
225 |
shows "list_ex (\<lambda>s. x all_in s) (split_domain split I)"
|
|
226 |
using assms(1)
|
|
227 |
proof(induction I arbitrary: x)
|
|
228 |
case (Cons I Is x)
|
|
229 |
have "x \<noteq> []"
|
|
230 |
using Cons(2) by auto
|
|
231 |
obtain x' xs where x_decomp: "x = x' # xs"
|
|
232 |
using \<open>x \<noteq> []\<close> list.exhaust by auto
|
|
233 |
hence "x' \<in>\<^sub>r I" "xs all_in Is"
|
|
234 |
using Cons(2)
|
|
235 |
by auto
|
|
236 |
show ?case
|
|
237 |
using Cons(1)[OF \<open>xs all_in Is\<close>]
|
|
238 |
split_correct[OF \<open>x' \<in>\<^sub>r I\<close>]
|
|
239 |
apply (auto simp add: list_ex_iff set_of_eq)
|
|
240 |
by (smt length_Cons less_Suc_eq_0_disj nth_Cons_0 nth_Cons_Suc x_decomp)
|
|
241 |
qed simp
|
|
242 |
|
|
243 |
|
|
244 |
lift_definition(code_dt) inverse_float_interval::"nat \<Rightarrow> float interval \<Rightarrow> float interval option" is
|
|
245 |
"\<lambda>prec (l, u). if (0 < l \<or> u < 0) then Some (float_divl prec 1 u, float_divr prec 1 l) else None"
|
|
246 |
by (auto intro!: order_trans[OF float_divl] order_trans[OF _ float_divr]
|
|
247 |
simp: divide_simps)
|
|
248 |
|
|
249 |
lemma inverse_float_interval_eq_Some_conv:
|
|
250 |
defines "one \<equiv> (1::float)"
|
|
251 |
shows
|
|
252 |
"inverse_float_interval p X = Some R \<longleftrightarrow>
|
|
253 |
(lower X > 0 \<or> upper X < 0) \<and>
|
|
254 |
lower R = float_divl p one (upper X) \<and>
|
|
255 |
upper R = float_divr p one (lower X)"
|
|
256 |
by clarsimp (transfer fixing: one, force simp: one_def split: if_splits)
|
|
257 |
|
|
258 |
lemma inverse_float_interval:
|
|
259 |
"inverse ` set_of (real_interval X) \<subseteq> set_of (real_interval Y)"
|
|
260 |
if "inverse_float_interval p X = Some Y"
|
|
261 |
using that
|
|
262 |
apply (clarsimp simp: set_of_eq inverse_float_interval_eq_Some_conv)
|
|
263 |
by (intro order_trans[OF float_divl] order_trans[OF _ float_divr] conjI)
|
|
264 |
(auto simp: divide_simps)
|
|
265 |
|
|
266 |
lemma inverse_float_intervalI:
|
|
267 |
"x \<in>\<^sub>r X \<Longrightarrow> inverse x \<in> set_of' (inverse_float_interval p X)"
|
|
268 |
using inverse_float_interval[of p X]
|
|
269 |
by (auto simp: set_of'_def split: option.splits)
|
|
270 |
|
|
271 |
lemma real_interval_abs_interval[simp]:
|
|
272 |
"real_interval (abs_interval x) = abs_interval (real_interval x)"
|
|
273 |
by (auto simp: interval_eq_set_of_iff set_of_eq real_of_float_max real_of_float_min)
|
|
274 |
|
|
275 |
lift_definition floor_float_interval::"float interval \<Rightarrow> float interval" is
|
|
276 |
"\<lambda>(l, u). (floor_fl l, floor_fl u)"
|
|
277 |
by (auto intro!: floor_mono simp: floor_fl.rep_eq)
|
|
278 |
|
|
279 |
lemma lower_floor_float_interval[simp]: "lower (floor_float_interval x) = floor_fl (lower x)"
|
|
280 |
by transfer auto
|
|
281 |
lemma upper_floor_float_interval[simp]: "upper (floor_float_interval x) = floor_fl (upper x)"
|
|
282 |
by transfer auto
|
|
283 |
|
|
284 |
lemma floor_float_intervalI: "\<lfloor>x\<rfloor> \<in>\<^sub>r floor_float_interval X" if "x \<in>\<^sub>r X"
|
|
285 |
using that by (auto simp: set_of_eq floor_fl_def floor_mono)
|
|
286 |
|
|
287 |
end
|
|
288 |
|
|
289 |
end |