Rqe/condense_thms.ml

   1 (* ------------------------------------------------------------------------- *)
   2 (* Condense subdivision by removing points with no relevant zeros.           *)
   3 (* ------------------------------------------------------------------------- *)
   4
   5 let real_cases = prove(`!x y. x < y \/ (x = y) \/ y < x`,REAL_ARITH_TAC);;
   6
   7 let gt_aux = prove(
   8   `!x. (x1 < x2 /\ x2 < x3) /\ ((x1 < x /\ x < x2) \/ (x = x2) \/ (x2 < x /\ x < x3)) ==> x1 < x /\ x < x3`,
   9    REAL_ARITH_TAC);;
  10
  11 let gen_thm = prove_by_refinement(
  12  `!P x1 x2 x3.
  13       (x1 < x3) ==>
  14       (!x. x1 < x /\ x < x2 ==> P x) ==>
  15       (!x. (x = x2) ==> P x) ==>
  16       (!x. x2 < x /\ x < x3 ==> P x) ==>
  17         (!x. x1 < x /\ x < x3 ==> P x)`,
  18 (* {{{ Proof *)
  19
  20 [
  21   MESON_TAC[real_cases;gt_aux;DE_MORGAN_THM;REAL_NOT_LT;REAL_LE_LT];
  22 ]);;
  23
  24 (* }}} *)
  25
  26 let gen_thm_noleft = prove(
  27  `!P x2 x3.
  28       (x2 < x3) ==>
  29       (!x. x < x2 ==> P x) ==>
  30       (!x. (x = x2) ==> P x) ==>
  31       (!x. x2 < x /\ x < x3 ==> P x) ==>
  32         (!x. x < x3 ==> P x)`,
  33   MESON_TAC[real_cases;gt_aux]);;
  34
  35 let gen_thm_noright = prove(
  36  `!P x1 x2.
  37       (x1 < x2) ==>
  38       (!x. x1 < x /\ x < x2 ==> P x) ==>
  39       (!x. (x = x2) ==> P x) ==>
  40       (!x. x2 < x ==> P x) ==>
  41         (!x. x1 < x ==> P x)`,
  42   MESON_TAC[real_cases;gt_aux]);;
  43
  44 let gen_thm_noboth = prove(
  45  `!P Q x2.
  46        Q ==>
  47       (!x. x < x2 ==> P x) ==>
  48       (!x. (x = x2) ==> P x) ==>
  49       (!x. x2 < x ==> P x) ==>
  50         (!x. T ==> P x)`,
  51   MESON_TAC[real_cases;gt_aux]);;