formal_lp/old/arith/interval_arith.hl

   1 (********************************)\r
   2 (* Interval arithmetic (theory) *)\r
   3 (********************************)\r
   4 \r
   5 module Interval_arith = struct\r
   6 \r
   7 (* The main definition *)\r
   8 let interval_arith = \r
   9         new_definition `interval_arith (x:real) (lo, hi) <=> lo <= x /\ x <= hi`;;\r
  10 \r
  11 \r
  12 let CONST_INTERVAL = prove(`!x. interval_arith x (x,x)`,\r
  13                            REWRITE_TAC[interval_arith; REAL_LE_REFL]);;\r
  14 \r
  15 \r
  16 let APPROX_INTERVAL = prove(`(a <= lo /\ hi <= b) /\ interval_arith x (lo, hi)\r
  17                               ==> interval_arith x (a,b)`,\r
  18    REWRITE_TAC[interval_arith] THEN REAL_ARITH_TAC);;\r
  19 \r
  20 let INTERVAL_NEG = prove(`interval_arith x (a, b) ==>\r
  21                            interval_arith (--x) (--b, --a)`,\r
  22                          REWRITE_TAC[interval_arith] THEN REAL_ARITH_TAC);;\r
  23 \r
  24 \r
  25 \r
  26 end;;\r