formal_ineqs/arith/interval_arith.hl

   1 (* =========================================================== *)\r
   2 (* Theoretical results for interval arithmetic                 *)\r
   3 (* Author: Alexey Solovyev                                     *)\r
   4 (* Date: 2012-10-27                                            *)\r
   5 (* =========================================================== *)\r
   6 \r
   7 needs "misc/vars.hl";;\r
   8 \r
   9 module Interval_arith = struct\r
  10 \r
  11 (*******************************)\r
  12 (* The main definition *)\r
  13 let interval_arith = \r
  14         new_definition `interval_arith (x:real) (lo, hi) <=> lo <= x /\ x <= hi`;;\r
  15 \r
  16 (* Additional definitions *)\r
  17 let bounded_on = new_definition `bounded_on f s f_bounds <=>\r
  18         !x. x IN s ==> interval_arith (f x) f_bounds`;;\r
  19 \r
  20 let bounded_on_int = new_definition `bounded_on_int f int f_bounds <=>\r
  21         !x. interval_arith x int ==> interval_arith (f x) f_bounds`;;\r
  22         \r
  23 let iabs = new_definition `iabs (x_lo, x_hi) = max x_hi (-- x_lo)`;;\r
  24 let interval_not_zero = new_definition `interval_not_zero (lo, hi) <=> &0 < lo \/ hi < &0`;;\r
  25 let interval_pos = new_definition `interval_pos (lo, hi) <=> &0 < lo`;;\r
  26 \r
  27 \r
  28 (********************************)\r
  29 (* Lemmas *)\r
  30 let CONST_INTERVAL = prove(`!x. interval_arith x (x,x)`,\r
  31                            REWRITE_TAC[interval_arith; REAL_LE_REFL]);;\r
  32 \r
  33 let APPROX_INTERVAL = (GEN_ALL o prove)(`(a <= lo /\ hi <= b) /\ interval_arith x (lo, hi)\r
  34                               ==> interval_arith x (a,b)`,\r
  35    REWRITE_TAC[interval_arith] THEN REAL_ARITH_TAC);;\r
  36 \r
  37 let INTERVAL_NEG = (GEN_ALL o prove)(`interval_arith x (a, b) ==>\r
  38                            interval_arith (--x) (--b, --a)`,\r
  39                          REWRITE_TAC[interval_arith] THEN REAL_ARITH_TAC);;\r
  40                                                  \r
  41 \r
  42 (**************************************)\r
  43 (* Conversions *)               \r
  44 open Misc_vars;;\r
  45                                  \r
  46 let interval_tm = `interval_arith`;;\r
  47 \r
  48 let dest_interval_arith tm =\r
  49   let lhs, int_tm = dest_comb tm in\r
  50     rand lhs, int_tm;;\r
  51 \r
  52 let mk_interval tm bounds =\r
  53         mk_comb (mk_comb (interval_tm, tm), bounds);;\r
  54         \r
  55 let mk_const_interval =\r
  56         let lemma = SPEC_ALL CONST_INTERVAL in\r
  57                 fun tm -> INST[tm, x_var_real] lemma;;\r
  58 \r
  59 end;;\r