IntervalArithScript.sml 17.4 KB
Newer Older
1
2
3
4
5
(**
  Formalization of real valued interval arithmetic
  Used in soundness proofs for error bound validator.
**)
open preamble
Heiko Becker's avatar
Heiko Becker committed
6
open realTheory realLib RealArith
7
open AbbrevsTheory ExpressionsTheory RealSimpsTheory;
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75

val _ = new_theory "IntervalArith";

(**
  Define validity of an interval, requiring that the lower bound is less than or equal to the upper bound.
  Containement is defined such that if x is contained in the interval, it must lie between the lower and upper bound.
**)
val valid_def = Define `
valid (iv:interval) = (IVlo iv <= IVhi iv)`;

val contained_def = Define `
contained (a:real) (iv:interval) = (IVlo iv <= a /\ a <= IVhi iv)`;

(**
Subset definition; when an interval is a subinterval of another
**)
val isSupersetInterval_def = Define `
isSupersetInterval (iv1:interval) (iv2:interval) =
((IVlo iv2 <= IVlo iv1) /\ (IVhi iv1 <= IVhi iv2))`;

val pointInterval_def = Define `pointInterval (x:real) = (x,x)`;

(**
Definitions of validity conditions for interval operations: Addition,
Subtraction, Multiplication and Division
**)
val validIntervalAdd_def = Define `
validIntervalAdd (iv1:interval) (iv2:interval) (iv3:interval) =
(! a b. contained a iv1 /\ contained b iv2 ==> contained (a + b) iv3)`;

val validIntervalSub_def = Define `
validIntervalSub (iv1:interval) (iv2:interval) (iv3:interval) =
(! a b. contained a iv1 /\ contained b iv2 ==> contained (a - b) iv3)`;

val validIntervalMult_def = Define`
validIntervalMult (iv1:interval) (iv2:interval) (iv3:interval) =
(! a b. contained a iv1 /\ contained b iv2 ==> contained (a * b) iv3)`;

val validIntervalDiv_def = Define `
validIntervalDiv (iv1:interval) (iv2:interval) (iv3:interval) =
(! a b. contained a iv1 /\ contained b iv2 ==> contained (a / b) iv3)`;

val min4_def = Define `
min4 a b c d = min a (min b (min c d))`;

val max4_def = Define `
max4 a b c d = max a (max b (max c d))`;

val absIntvUpd_def = Define `
absIntvUpd (op:real->real->real) (iv1:interval) (iv2:interval) =
(
  min4 (op (IVlo iv1) (IVlo iv2))
       (op (IVlo iv1) (IVhi iv2))
       (op (IVhi iv1) (IVlo iv2))
       (op (IVhi iv1) (IVhi iv2)),
  max4 (op (IVlo iv1) (IVlo iv2))
       (op (IVlo iv1) (IVhi iv2))
       (op (IVhi iv1) (IVlo iv2))
       (op (IVhi iv1) (IVhi iv2))
)`;

val widenInterval_def = Define `
widenInterval (iv:interval) (v:real) = ((IVlo iv - v), (IVhi iv + v))`;

val negateInterval_def = Define `
negateInterval (iv:interval) = ((- IVhi iv), (- IVlo iv))`;

val invertInterval_def = Define `
76
invertInterval (iv:interval)  = (1 /(IVhi iv), 1 /(IVlo iv))`;
77
78
79
80
81
82
83
84
85
86
87
88
89

val addInterval_def = Define `
addInterval (iv1:interval) (iv2:interval) = absIntvUpd (+) iv1 iv2`;

val subtractInterval_def = Define `
subtractInterval (iv1:interval) (iv2:interval) = addInterval iv1 (negateInterval iv2)`;

val multInterval_def = Define `
multInterval (iv1:interval) (iv2:interval) = absIntvUpd ( * ) iv1 iv2`;

val divideInterval_def = Define `
divideInterval iv1 iv2 = multInterval iv1 (invertInterval iv2)`;

90
91
val maxAbs_def = Define `
maxAbs iv = max (abs (FST iv)) (abs (SND iv))`;
92

93
94
val minAbsFun_def = Define `
minAbsFun iv = min (abs (FST iv)) (abs (SND iv))`;
95
96
97
98
99
100
101
102
103
104
105

val iv_ss = [IVlo_def, IVhi_def, valid_def, contained_def, isSupersetInterval_def,
                     pointInterval_def, validIntervalAdd_def,
                     validIntervalSub_def, validIntervalMult_def,
                     validIntervalDiv_def,
                     min4_def, max4_def,
                     absIntvUpd_def, widenInterval_def,
                     negateInterval_def,
                     invertInterval_def,
                     addInterval_def, subtractInterval_def,
                     multInterval_def, divideInterval_def,
106
                     maxAbs_def, minAbsFun_def
107
108
                    ];

109
val contained_implies_valid = store_thm ("contained_implies_valid",
110
111
112
``!(a:real) (iv:interval).
  contained a iv ==> valid iv``,
metis_tac (iv_ss @ [REAL_LE_TRANS]));
113

114
val contained_implies_subset = store_thm ("contained_implies_subset",
115
116
``!(a:real) (iv:interval).
  contained a iv ==> isSupersetInterval (pointInterval a) iv``,
117
118
fs iv_ss);

119
120
121
122
val validPointInterval = store_thm("validPointInterval",
``!(a:real).
  contained a (pointInterval a)``,
fs iv_ss);
123

124
val min4_correct = store_thm ("min4_correct",
125
126
127
128
129
130
131
``!a b c d.
  let m = min4 a b c d in
    m <= a /\ m <= b /\ m <= c /\ m <= d``,
rpt strip_tac \\fs [min4_def] \\ conj_tac \\
try (fs [REAL_MIN_LE1]) \\ conj_tac
>- (`min b (min c d) <= b` by fs[REAL_MIN_LE1] \\
   match_mp_tac REAL_LE_TRANS \\
132
133
134
135
   HINT_EXISTS_TAC \\
   fs [REAL_MIN_LE2])
>- (conj_tac
    >- (`min c d <= c` by fs [REAL_MIN_LE1] \\
136
       match_mp_tac REAL_LE_TRANS \\
137
138
       HINT_EXISTS_TAC \\
       fs [REAL_MIN_LE2] \\
139
       match_mp_tac REAL_LE_TRANS \\
140
141
       `min b (min c d) <= min c d` by fs[REAL_MIN_LE2] \\
       HINT_EXISTS_TAC \\
142
       fs [REAL_MIN_LE2] )
143
    >- (`min c d <= d` by fs [REAL_MIN_LE2] \\
144
       match_mp_tac REAL_LE_TRANS \\
145
146
       HINT_EXISTS_TAC \\
       fs [REAL_MIN_LE2] \\
147
       match_mp_tac REAL_LE_TRANS \\
148
149
150
151
       `min b (min c d) <= min c d` by fs[REAL_MIN_LE2] \\
       HINT_EXISTS_TAC \\
       fs [REAL_MIN_LE2])));

152
val max4_correct = store_thm ("max4_correct",
153
154
155
156
157
``!a b c d.
  let m = max4 a b c d in
    a <= m /\ b <= m /\ c <= m /\ d <= m``,
rpt strip_tac \\fs [max4_def] \\ conj_tac \\
try (fs [REAL_LE_MAX1]) \\ conj_tac
158
>-(`b <= max b (max c d)` by fs[REAL_LE_MAX1] \\
159
match_mp_tac REAL_LE_TRANS \\
160
161
162
163
HINT_EXISTS_TAC \\
fs [REAL_LE_MAX2])
>- (conj_tac
    >- (`c <= max c d` by fs [REAL_LE_MAX1] \\
164
       match_mp_tac REAL_LE_TRANS \\
165
166
       HINT_EXISTS_TAC \\
       fs [REAL_LE_MAX2] \\
167
       match_mp_tac REAL_LE_TRANS \\
168
169
170
171
       `max c d <= max b (max c d)` by fs[REAL_LE_MAX2] \\
       HINT_EXISTS_TAC \\
       fs [REAL_LE_MAX2] )
    >- (`d <= max c d` by fs [REAL_LE_MAX2] \\
172
       match_mp_tac REAL_LE_TRANS \\
173
174
       HINT_EXISTS_TAC \\
       fs [REAL_LE_MAX2] \\
175
       match_mp_tac REAL_LE_TRANS \\
176
       `max c d <= max b (max c d)` by fs[REAL_LE_MAX2] \\
177
178
       HINT_EXISTS_TAC \\
       fs [REAL_LE_MAX2] )));
179

180
181

val interval_negation_valid = store_thm ("interval_negation_valid",
182
183
``!iv a.
  contained a iv ==> contained (- a) (negateInterval iv)``,
184
185
fs iv_ss);

186
val interval_inversion_valid = store_thm ("interval_inversion_valid",
187
188
189
``!iv a.
  (IVhi iv < 0 \/ 0 < IVlo iv) /\ contained a iv ==>
    contained (inv a) (invertInterval iv)``,
190
fs iv_ss \\ rpt strip_tac \\ once_rewrite_tac [GSYM REAL_INV_1OVER]
191
(* First subgoal *)
192
>- (once_rewrite_tac [GSYM REAL_LE_NEG] \\
193
194
195
196
   `0 < - a` by REAL_ASM_ARITH_TAC \\
   `a <> 0` by REAL_ASM_ARITH_TAC \\
   `0 < - SND iv` by REAL_ASM_ARITH_TAC \\
   `SND iv <> 0` by REAL_ASM_ARITH_TAC \\
197
198
199
200
   `-a⁻¹ = (-a)⁻¹` by (match_mp_tac REAL_NEG_INV \\ simp[]) \\
   `-(SND iv)⁻¹ = (-(SND iv))⁻¹` by (match_mp_tac REAL_NEG_INV \\ simp []) \\
   asm_rewrite_tac [] \\
   `inv(-a)  inv (-SND iv) <=> (- SND iv) <= - a` by match_mp_tac REAL_INV_LE_ANTIMONO \\ fs [])
201
(* Second subgoal *)
202
203
204
205
206
207
208
209
210
211
212
>- (once_rewrite_tac [GSYM REAL_LE_NEG] \\
   `a < 0` by REAL_ASM_ARITH_TAC \\
   `0 < -a` by REAL_ASM_ARITH_TAC \\
   `- a <> 0` by REAL_ASM_ARITH_TAC \\
   `a <> 0` by REAL_ASM_ARITH_TAC \\
   `-a⁻¹ = (-a)⁻¹` by (match_mp_tac REAL_NEG_INV \\ simp []) \\
   `-(FST iv)⁻¹ = (-(FST iv))⁻¹` by (match_mp_tac REAL_NEG_INV \\ simp [] \\
   try REAL_ASM_ARITH_TAC \\ asm_rewrite_tac []) \\
   `inv (- (FST iv)) <= inv (- a) <=> - a <= - (FST iv)`
     by (match_mp_tac REAL_INV_LE_ANTIMONO \\ fs []) \\
   REAL_ASM_ARITH_TAC)
213
(* Third subgoal *)
214
215
216
217
>- (rewrite_tac [GSYM REAL_INV_1OVER] \\
   `inv (SND iv) <= inv a <=> a <= SND iv`
     by (match_mp_tac REAL_INV_LE_ANTIMONO \\ fs []) \\
   REAL_ASM_ARITH_TAC)
218
(* Fourth subgoal *)
219
220
221
222
>- (rewrite_tac [GSYM REAL_INV_1OVER] \\
   `inv a <= inv (FST iv) <=> FST iv <= a`
     by (match_mp_tac REAL_INV_LE_ANTIMONO \\ fs []) \\
   REAL_ASM_ARITH_TAC));
223
224
225

val interval_addition_valid = store_thm ("interval_addition_valid",
``!iv1 iv2. validIntervalAdd iv1 iv2 (addInterval iv1 iv2)``,
226
fs iv_ss \\ rpt strip_tac
227
(* First subgoal, lower bound *)
228
229
230
231
>- (`FST iv1 + FST iv2 <= a + b`
     by (match_mp_tac REAL_LE_ADD2 \\ fs []) \\
   match_mp_tac REAL_LE_TRANS \\
   HINT_EXISTS_TAC \\ strip_tac \\ fs[REAL_MIN_LE1])
232
(* Second subgoal, upper bound *)
233
234
235
236
>- (`a + b <= SND iv1 + SND iv2`
     by (match_mp_tac REAL_LE_ADD2 \\ fs []) \\
   match_mp_tac REAL_LE_TRANS \\
   HINT_EXISTS_TAC \\ strip_tac \\ fs [REAL_LE_MAX]));
237
238

val interval_subtraction_valid = store_thm ("interval_subtraction_valid",
239
240
241
242
243
244
``!iv1 iv2.
  validIntervalSub iv1 iv2 (subtractInterval iv1 iv2)``,
rpt gen_tac \\ Cases_on `iv2` \\ rewrite_tac (iv_ss @ [real_sub]) \\
rpt gen_tac \\ strip_tac \\
(** TODO: FIXME, use qspecl_then or sth else **)
match_mp_tac (REWRITE_RULE (iv_ss @ [FST,SND]) (SPECL [``iv1:interval``,``(-r,-q):interval``] interval_addition_valid)) \\
245
fs []);
246

247
val interval_multiplication_valid = store_thm ("interval_multiplication_valid",
248
249
250
``!iv1 iv2 a b.
  contained a iv1 /\ contained b iv2 ==> contained (a * b) (multInterval iv1 iv2)``,
fs iv_ss \\ rpt strip_tac
251
252
(* Lower Bound *)
(* Case distinction for a *)
253
>- (qspecl_then [`a`,`0`] DISJ_CASES_TAC REAL_LTE_TOTAL
254
255
256
  (* First case: a < 0 *)
  >- (`a <= 0 /\ a <> 0` by fs[REAL_LT_LE] \\
     (* Case distinction for SND iv2 *)
257
     qspecl_then [`SND iv2`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL
258
     (* First case: SND iv2 < 0 *)
259
260
261
262
263
264
265
266
267
268
269
270
271
     >- (match_mp_tac REAL_LE_TRANS \\
        exists_tac ``SND (iv1:interval) * SND (iv2:interval)`` \\
        conj_tac
        >- (qspecl_then
                [`FST iv1 * FST iv2`, `FST iv1 * SND iv2`,`SND iv1 * FST iv2`, `SND iv1 * SND iv2`]
                (fn thm =>
                    rewrite_tac [SIMP_RULE bool_ss [min4_def] (CONV_RULE let_CONV thm)])
                min4_correct)
        >- (once_rewrite_tac[REAL_MUL_SYM] \\
           match_mp_tac REAL_LE_TRANS \\
           exists_tac ``SND (iv2:interval) * (a:real)`` \\
           conj_tac
           >- (match_mp_tac REAL_MUL_LE_COMPAT_NEG_L \\
272
              fs [REAL_LT_LE])
273
274
           >- (once_rewrite_tac [REAL_MUL_SYM] \\
              match_mp_tac REAL_MUL_LE_COMPAT_NEG_L \\
275
276
              fs [])))
     (* Second case: 0 <= SND iv2 *)
277
278
279
280
281
282
283
284
285
286
287
     >- (match_mp_tac REAL_LE_TRANS\\
        exists_tac ``FST (iv1:interval) * SND (iv2:interval)`` \\
        conj_tac
        >- (qspecl_then
                [`FST iv1 * FST iv2`, `FST iv1 * SND iv2`,`SND iv1 * FST iv2`, `SND iv1 * SND iv2`]
                (fn thm =>
                    rewrite_tac [SIMP_RULE bool_ss [min4_def] (CONV_RULE let_CONV thm)])
                min4_correct)
        >- (match_mp_tac REAL_LE_TRANS \\
           exists_tac ``(a:real) * SND (iv2:interval)`` \\
           conj_tac \\ fs[REAL_LE_RMUL_IMP, REAL_MUL_LE_COMPAT_NEG_L])))
288
289
  (* Second case: 0 <= a*)
  (* Case distinction for FST iv2 *)
290
  >- (qspecl_then [`FST iv2`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL
291
     (* First case: FST iv2 < 0 *)
292
293
294
295
296
297
298
299
300
301
302
303
304
     >- (match_mp_tac REAL_LE_TRANS \\
        exists_tac ``SND (iv1:interval) * FST (iv2:interval)`` \\
        conj_tac
        >- (qspecl_then
                 [`FST iv1 * FST iv2`, `FST iv1 * SND iv2`,`SND iv1 * FST iv2`, `SND iv1 * SND iv2`]
                 (fn thm =>
                     rewrite_tac [SIMP_RULE bool_ss [min4_def] (CONV_RULE let_CONV thm)])
                 min4_correct)
        >- (once_rewrite_tac [REAL_MUL_SYM] \\
           match_mp_tac REAL_LE_TRANS \\
           exists_tac ``FST (iv2:interval) * (a:real)`` \\
           conj_tac
           >- (match_mp_tac REAL_MUL_LE_COMPAT_NEG_L \\ fs[REAL_LT_LE])
305
306
           >- (fs [REAL_LE_RMUL_IMP])))
     (* Second case: 0 <= FST iv2 *)
307
308
309
310
311
312
313
314
315
316
317
     >- (match_mp_tac REAL_LE_TRANS \\
        exists_tac ``FST (iv1:interval) * FST (iv2:interval)`` \\
        conj_tac
        >- (qspecl_then
                [`FST iv1 * FST iv2`, `FST iv1 * SND iv2`,`SND iv1 * FST iv2`, `SND iv1 * SND iv2`]
                (fn thm =>
                    rewrite_tac [SIMP_RULE bool_ss [min4_def] (CONV_RULE let_CONV thm)])
                min4_correct)
        >- (match_mp_tac REAL_LE_TRANS \\
           exists_tac ``a:real * FST (iv2:interval)`` \\
           conj_tac \\ fs [REAL_LE_RMUL_IMP, REAL_LE_LMUL_IMP]))))
318
319
(* Upper Bound *)
(* Case distinction for a *)
320
>- (qspecl_then [`a`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL
321
322
323
   (* First case: a < 0 *)
   >- (`a <= 0 /\ a <> 0` by fs[REAL_LT_LE] \\
      (* Case distinction for SND iv2 *)
324
      qspecl_then [`FST iv2`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL
325
      (* First case: FST iv2 < 0 *)
326
327
328
329
330
331
332
333
334
      >- (match_mp_tac REAL_LE_TRANS \\
         exists_tac ``FST (iv1:interval) * FST (iv2:interval)`` \\
         conj_tac
         >- (once_rewrite_tac[REAL_MUL_SYM] \\
            match_mp_tac REAL_LE_TRANS \\
            exists_tac ``FST (iv2:interval) * (a:real)`` \\
            conj_tac
            >- (once_rewrite_tac [REAL_MUL_SYM] \\
               match_mp_tac REAL_MUL_LE_COMPAT_NEG_L \\
335
               fs [])
336
            >- (match_mp_tac REAL_MUL_LE_COMPAT_NEG_L \\
337
               fs [REAL_LT_LE]))
338
339
340
341
342
         >- (qspecl_then
              [`FST iv1 * FST iv2`, `FST iv1 * SND iv2`,`SND iv1 * FST iv2`, `SND iv1 * SND iv2`]
              (fn thm =>
                  rewrite_tac [SIMP_RULE bool_ss [max4_def] (CONV_RULE let_CONV thm)])
              max4_correct))
343
      (* Second case: 0 <= FST iv2 *)
344
345
346
347
348
349
350
351
352
353
354
355
      >- (match_mp_tac REAL_LE_TRANS\\
         exists_tac ``SND (iv1:interval) * FST (iv2:interval)`` \\
         conj_tac
         >- (match_mp_tac REAL_LE_TRANS \\
            exists_tac ``(a:real) * FST (iv2:interval)`` \\
            conj_tac \\ fs[REAL_LE_RMUL_IMP, REAL_MUL_LE_COMPAT_NEG_L])
         >- (qspecl_then
                 [`FST iv1 * FST iv2`, `FST iv1 * SND iv2`,`SND iv1 * FST iv2`, `SND iv1 * SND iv2`]
                 (fn thm =>
                     rewrite_tac [SIMP_RULE bool_ss [max4_def] (CONV_RULE let_CONV thm)])
                 max4_correct)))
  (* Second case  0 <= a *)
356
  (* Case distinction for FST iv2 *)
357
  >- (qspecl_then [`SND iv2`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL
358
     (* First case: FST iv2 < 0 *)
359
360
361
362
363
364
365
     >- (match_mp_tac REAL_LE_TRANS \\
        exists_tac ``FST (iv1:interval) * SND (iv2:interval)`` \\
        conj_tac
        >- (once_rewrite_tac [REAL_MUL_SYM] \\
           match_mp_tac REAL_LE_TRANS \\
           exists_tac ``SND (iv2:interval) * (a:real)`` \\
           conj_tac
366
           >- (fs [REAL_LE_RMUL_IMP])
367
368
369
370
371
372
           >- (match_mp_tac REAL_MUL_LE_COMPAT_NEG_L \\ fs[REAL_LT_LE]))
        >- (qspecl_then
                [`FST iv1 * FST iv2`, `FST iv1 * SND iv2`,`SND iv1 * FST iv2`, `SND iv1 * SND iv2`]
                (fn thm =>
                    rewrite_tac [SIMP_RULE bool_ss [max4_def] (CONV_RULE let_CONV thm)])
                max4_correct))
373
     (* Second case: 0 <= FST iv2 *)
374
375
376
377
378
379
380
381
382
383
384
     >- (match_mp_tac REAL_LE_TRANS \\
        exists_tac ``SND (iv1:interval) * SND (iv2:interval)`` \\
        conj_tac
        >- (match_mp_tac REAL_LE_TRANS \\
           exists_tac ``a:real * SND (iv2:interval)`` \\
           conj_tac \\ fs [REAL_LE_RMUL_IMP, REAL_LE_LMUL_IMP])
        >- (qspecl_then
                [`FST iv1 * FST iv2`, `FST iv1 * SND iv2`,`SND iv1 * FST iv2`, `SND iv1 * SND iv2`]
                (fn thm =>
                    rewrite_tac [SIMP_RULE bool_ss [max4_def] (CONV_RULE let_CONV thm)])
                max4_correct)))));
385
386

val interval_division_valid = store_thm ( "interval_division_valid",
387
``!(iv1:interval) (iv2:interval) (a:real) (b:real).
388
389
390
391
    (IVhi iv2 < 0 \/ 0 < IVlo iv2) /\
    contained a iv1 /\
    contained b iv2 ==>
    contained (a / b) (divideInterval iv1 iv2)``,
392
393
394
395
396
397
rpt gen_tac \\ Cases_on `iv2` \\ rewrite_tac (iv_ss @ [real_div, REAL_MUL_LID]) \\
rpt gen_tac \\ strip_tac \\
(** TODO: FIXME use qspecl_then **)
match_mp_tac
  (REWRITE_RULE (iv_ss @ [FST,SND])
    (SPECL [``iv1:interval``, ``(inv r, inv q):interval``] interval_multiplication_valid)) \\
398
fs [] \\
399
400
401
match_mp_tac
  (REWRITE_RULE
    (iv_ss @ [FST, SND, real_div, REAL_MUL_LID]) (SPECL [``(q,r):interval``, ``b:real``] interval_inversion_valid)) \\
402
403
fs[]);

Heiko Becker's avatar
Heiko Becker committed
404
405
(** Properties of the maxAbs function **)
val contained_leq_maxAbs = store_thm ("contained_leq_maxAbs",
406
  ``!a iv. contained a iv ==> abs a <= maxAbs iv``,
407
  rpt strip_tac\\ fs iv_ss \\ match_mp_tac maxAbs \\ fs []);
Heiko Becker's avatar
Heiko Becker committed
408

409
val contained_leq_maxAbs_val = store_thm ("contained_leq_maxAbs_val",
410
  ``!a iv. contained a iv ==> a <= maxAbs iv``,
411
412
413
414
  rpt strip_tac \\ fs iv_ss \\
  `abs a <= max (abs (FST iv)) (abs (SND iv))`
    by (match_mp_tac (REWRITE_RULE iv_ss contained_leq_maxAbs) \\ fs []) \\
  REAL_ASM_ARITH_TAC);
415

Heiko Becker's avatar
Heiko Becker committed
416
val contained_leq_maxAbs_neg_val = store_thm ("contained_leq_maxAbs_neg_val",
417
  ``!a iv. contained a iv ==> - a <= maxAbs iv``,
418
419
420
  rpt strip_tac\\ fs iv_ss \\
  `abs a <= max (abs (FST iv)) (abs (SND iv))` by (match_mp_tac (REWRITE_RULE iv_ss contained_leq_maxAbs) \\ fs []) \\
  REAL_ASM_ARITH_TAC);
Heiko Becker's avatar
Heiko Becker committed
421
422

val distance_gives_iv = store_thm ("distance_gives_iv",
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
  ``!a b e iv. contained a iv /\ abs (a - b) <= e ==> contained b (widenInterval iv e)``,
  fs iv_ss \\ rpt strip_tac \\
  `(b:real) - e <= a /\ a <= b + e` by REAL_ASM_ARITH_TAC \\
  REAL_ASM_ARITH_TAC);

val minAbs_positive_iv_is_lo = store_thm ("minAbs_positive_iv_is_lo",
  ``!(a b:real).
    (0 < a) /\
	(a <= b) ==>
	(minAbsFun (a,b) = a)``,
  rpt (strip_tac) \\
  fs[minAbsFun_def] \\
  `abs a = a` by (fs[ABS_REFL] \\ REAL_ASM_ARITH_TAC) \\
  `abs b = b` by (fs[ABS_REFL] \\ REAL_ASM_ARITH_TAC) \\
  fs[REAL_MIN_ALT]);

val minAbs_negative_iv_is_hi = store_thm ("minAbs_negative_iv_is_hi",
  ``!(a b:real).
    (b < 0) /\
	(a <= b) ==>
	(minAbsFun (a,b) = - b)``,
  rpt (strip_tac) \\
  fs[minAbsFun_def] \\
  `abs a = - a` by REAL_ASM_ARITH_TAC \\
  `abs b = - b` by REAL_ASM_ARITH_TAC \\
448
  fs[REAL_MIN_ALT]);
Heiko Becker's avatar
Heiko Becker committed
449

450
val _ = export_theory();