Tutorial/HOLs_number_systems.ml

   1 REAL_ARITH `!x y:real. (abs(x) - abs(y)) <= abs(x - y)`;;
   2
   3 INT_ARITH
   4  `!a b a' b' D:int.
   5      (a pow 2 - D * b pow 2) * (a' pow 2 - D * b' pow 2) =
   6      (a * a' + D * b * b') pow 2 - D * (a * b' + a' * b) pow 2`;;
   7
   8 REAL_ARITH
   9  `!x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11:real.
  10         x3 = abs(x2) - x1 /\
  11         x4 = abs(x3) - x2 /\
  12         x5 = abs(x4) - x3 /\
  13         x6 = abs(x5) - x4 /\
  14         x7 = abs(x6) - x5 /\
  15         x8 = abs(x7) - x6 /\
  16         x9 = abs(x8) - x7 /\
  17         x10 = abs(x9) - x8 /\
  18         x11 = abs(x10) - x9
  19         ==> x1 = x10 /\ x2 = x11`;;
  20
  21 REAL_ARITH `!x y:real. x < y ==> x < (x + y) / &2 /\ (x + y) / &2 < y`;;
  22
  23 REAL_ARITH
  24  `((x1 pow 2 + x2 pow 2 + x3 pow 2 + x4 pow 2) pow 2) =
  25   ((&1 / &6) * ((x1 + x2) pow 4 + (x1 + x3) pow 4 + (x1 + x4) pow 4 +
  26                 (x2 + x3) pow 4 + (x2 + x4) pow 4 + (x3 + x4) pow 4) +
  27    (&1 / &6) * ((x1 - x2) pow 4 + (x1 - x3) pow 4 + (x1 - x4) pow 4 +
  28                 (x2 - x3) pow 4 + (x2 - x4) pow 4 + (x3 - x4) pow 4))`;;
  29
  30 ARITH_RULE `x < 2 ==> 2 * x + 1 < 4`;;
  31
  32 (**** Fails
  33 ARITH_RULE `~(2 * m + 1 = 2 * n)`;;
  34  ****)
  35
  36 ARITH_RULE `x < 2 EXP 30 ==> (429496730 * x) DIV (2 EXP 32) = x DIV 10`;;
  37
  38 (**** Fails
  39 ARITH_RULE `x <= 2 EXP 30 ==> (429496730 * x) DIV (2 EXP 32) = x DIV 10`;;
  40  ****)
  41
  42 (**** Fails
  43 ARITH_RULE `1 <= x /\ 1 <= y ==> 1 <= x * y`;;
  44  ****)
  45
  46 (**** Fails
  47 REAL_ARITH `!x y:real. x = y ==> x * y = y pow 2`;;
  48  ****)
  49
  50 prioritize_real();;
  51
  52 REAL_RING
  53   `s = (a + b + c) / &2
  54    ==> s * (s - b) * (s - c) + s * (s - c) * (s - a) +
  55        s * (s - a) * (s - b) - (s - a) * (s - b) * (s - c) =
  56        a * b * c`;;
  57
  58 REAL_RING `a pow 2 = &2 /\ x pow 2 + a * x + &1 = &0 ==> x pow 4 + &1 = &0`;;
  59
  60 REAL_RING
  61  `(a * x pow 2 + b * x + c = &0) /\
  62   (a * y pow 2 + b * y + c = &0) /\
  63   ~(x = y)
  64   ==> (a * x * y = c) /\ (a * (x + y) + b = &0)`;;
  65
  66 REAL_RING
  67  `p = (&3 * a1 - a2 pow 2) / &3 /\
  68   q = (&9 * a1 * a2 - &27 * a0 - &2 * a2 pow 3) / &27 /\
  69   x = z + a2 / &3 /\
  70   x * w = w pow 2 - p / &3
  71   ==> (z pow 3 + a2 * z pow 2 + a1 * z + a0 = &0 <=>
  72        if p = &0 then x pow 3 = q
  73        else (w pow 3) pow 2 - q * (w pow 3) - p pow 3 / &27 = &0)`;;
  74
  75 REAL_FIELD `&0 < x ==> &1 / x - &1 / (&1 + x) = &1 / (x * (&1 + x))`;;
  76
  77 REAL_FIELD
  78 `s pow 2 = b pow 2 - &4 * a * c
  79  ==> (a * x pow 2 + b * x + c = &0 <=>
  80       if a = &0 then
  81          if b = &0 then
  82             if c = &0 then T else F
  83          else x = --c / b
  84       else x = (--b + s) / (&2 * a) \/ x = (--b + --s) / (&2 * a))`;;
  85
  86 (**** This needs an external SDP solver to assist with proof
  87
  88 needs "Examples/sos.ml";;
  89
  90 SOS_RULE `1 <= x /\ 1 <= y ==> 1 <= x * y`;;
  91
  92 REAL_SOS
  93  `!a1 a2 a3 a4:real.
  94       &0 <= a1 /\ &0 <= a2 /\ &0 <= a3 /\ &0 <= a4
  95       ==> a1 pow 2 +
  96           ((a1 + a2) / &2) pow 2 +
  97           ((a1 + a2 + a3) / &3) pow 2 +
  98           ((a1 + a2 + a3 + a4) / &4) pow 2
  99          <= &4 * (a1 pow 2 + a2 pow 2 + a3 pow 2 + a4 pow 2)`;;
 100
 101 REAL_SOS
 102  `!a b c:real.
 103       a >= &0 /\ b >= &0 /\ c >= &0
 104       ==> &3 / &2 * (b + c) * (a + c) * (a + b) <=
 105           a * (a + c) * (a + b) +
 106           b * (b + c) * (a + b) +
 107           c * (b + c) * (a + c)`;;
 108
 109 SOS_CONV `&2 * x pow 4 + &2 * x pow 3 * y - x pow 2 * y pow 2 + &5 * y pow 4`;;
 110
 111 PURE_SOS
 112 `x pow 4 + &2 * x pow 2 * z + x pow 2 - &2 * x * y * z +
 113           &2 * y pow 2 * z pow 2 + &2 * y * z pow 2 + &2 * z pow 2 - &2 * x +
 114           &2 *  y * z + &1 >= &0`;;
 115
 116 ****)
 117
 118 needs "Examples/cooper.ml";;
 119
 120 COOPER_RULE `ODD n ==> 2 * n DIV 2 < n`;;
 121
 122 COOPER_RULE `!n. n >= 8 ==> ?a b. n = 3 * a + 5 * b`;;
 123
 124 needs "Rqe/make.ml";;
 125
 126 REAL_QELIM_CONV `!x. &0 <= x ==> ?y. y pow 2 = x`;;