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