Rqe/signs_thms.ml

   1 let [pth_0g;pth_0l;pth_gg;pth_gl;pth_lg;pth_ll] =
   2    (CONJUNCTS o prove)
   3    (`((p = &0) ==> c > &0 ==> (c * p = &0)) /\
   4      ((p = &0) ==> c < &0 ==> (c * p = &0)) /\
   5      (p > &0 ==> c > &0 ==> c * p > &0) /\
   6      (p > &0 ==> c < &0 ==> c * p < &0) /\
   7      (p < &0 ==> c > &0 ==> c * p < &0) /\
   8      (p < &0 ==> c < &0 ==> c * p > &0)`,
   9     SIMP_TAC[REAL_MUL_RZERO] THEN
  10     REWRITE_TAC[REAL_ARITH `(x > &0 <=> &0 < x) /\ (x < &0 <=> &0 < --x)`;
  11                 REAL_ARITH `~(p = &0) <=> p < &0 \/ p > &0`] THEN
  12     REWRITE_TAC[IMP_IMP] THEN
  13     REPEAT CONJ_TAC THEN DISCH_THEN(MP_TAC o MATCH_MP REAL_LT_MUL) THEN
  14     REAL_ARITH_TAC);;
  15
  16 let pth_nzg = prove_by_refinement(
  17   `p <> &0 ==> c > &0 ==> c * p <> &0`,
  18 (* {{{ Proof *)
  19 [
  20   REWRITE_TAC[NEQ;REAL_ENTIRE] THEN REAL_ARITH_TAC;
  21 ]);;
  22 (* }}} *)
  23
  24 let pth_nzl = prove_by_refinement(
  25   `p <> &0 ==> c < &0 ==> c * p <> &0`,
  26 (* {{{ Proof *)
  27 [
  28   REWRITE_TAC[NEQ;REAL_ENTIRE] THEN REAL_ARITH_TAC;
  29 ]);;
  30 (* }}} *)
  31
  32 let signs_lem01 = prove_by_refinement(
  33   `c < &0 ==> p < &0 ==> (c * p = p') ==> p' > &0`,
  34 (* {{{ Proof *)
  35 [
  36   ASM_MESON_TAC[REAL_MUL_LT;REAL_MUL_GT;real_gt];
  37 ]);;
  38 (* }}} *)
  39
  40 let signs_lem02 = prove_by_refinement(
  41   `c > &0 ==> p < &0 ==> (c * p = p') ==> p' < &0`,
  42 (* {{{ Proof *)
  43 [
  44   ASM_MESON_TAC[REAL_MUL_LT;REAL_MUL_GT;real_gt];
  45 ]);;
  46 (* }}} *)
  47
  48 let signs_lem03 = prove_by_refinement(
  49   `c < &0 ==> p > &0 ==> (c * p = p') ==> p' < &0`,
  50 (* {{{ Proof *)
  51 [
  52   ASM_MESON_TAC[REAL_MUL_LT;REAL_MUL_GT;real_gt];
  53 ]);;
  54 (* }}} *)
  55
  56 let signs_lem04 = prove_by_refinement(
  57   `c > &0 ==> p > &0 ==> (c * p = p') ==> p' > &0`,
  58 (* {{{ Proof *)
  59 [
  60   ASM_MESON_TAC[REAL_MUL_LT;REAL_MUL_GT;real_gt];
  61 ]);;
  62 (* }}} *)
  63
  64 let signs_lem05 = prove_by_refinement(
  65   `c < &0 ==> (p = &0) ==> (c * p = p') ==> (p' = &0)`,
  66 (* {{{ Proof *)
  67 [
  68   ASM_MESON_TAC[REAL_MUL_LT;REAL_MUL_GT;real_gt;REAL_MUL_RZERO];
  69 ]);;
  70 (* }}} *)
  71
  72 let signs_lem06 = prove_by_refinement(
  73   `c > &0 ==> (p = &0) ==> (c * p = p') ==> (p' = &0)`,
  74 (* {{{ Proof *)
  75 [
  76   ASM_MESON_TAC[REAL_MUL_LT;REAL_MUL_GT;real_gt;REAL_MUL_RZERO];
  77 ]);;
  78 (* }}} *)
  79
  80 let signs_lem07 = prove_by_refinement(
  81   `c < &0 ==> p <> &0 ==> (c * p = p') ==> p' <> &0`,
  82 (* {{{ Proof *)
  83
  84 [
  85   ASM_MESON_TAC[NEQ;REAL_MUL_LT;REAL_MUL_GT;real_gt;REAL_MUL_RZERO;REAL_ENTIRE;REAL_GT_IMP_NZ];
  86 ]);;
  87
  88 (* }}} *)
  89
  90 let signs_lem08 = prove_by_refinement(
  91   `c > &0 ==> p <> &0 ==> (c * p = p') ==> p' <> &0`,
  92 (* {{{ Proof *)
  93
  94 [
  95   ASM_MESON_TAC[NEQ;REAL_MUL_LT;REAL_MUL_GT;real_gt;REAL_MUL_RZERO;REAL_ENTIRE;REAL_LT_IMP_NZ];
  96 ]);;
  97
  98 (* }}} *)
  99
 100 let signs_lem002 = prove_by_refinement(
 101   `!p. (p = &0) \/ (p <> &0)`,
 102 (* {{{ Proof *)
 103 [
 104   MESON_TAC[NEQ];
 105 ]);;
 106 (* }}} *)
 107
 108 let signs_lem003 = TAUT `a \/ b ==> (a ==> x) ==> (b ==> y) ==> (a /\ x \/ b /\ y)`;;
 109
 110 let sz_z_thm = ref TRUTH;;
 111 let sz_nz_thm = ref TRUTH;;
 112
 113 let PULL_CASES_THM = prove
 114  (`!a p p0 p1.
 115 ((a = &0) /\ (p <=> p0) \/ (a <> &0) /\ (p <=> p1)) <=> ((p <=> (a = &0) /\ p0 \/ a <> &0 /\ p1 ))`,
 116 (* {{{ Proof *)
 117    REPEAT STRIP_TAC THEN  REWRITE_TAC[NEQ] THEN MAP_EVERY BOOL_CASES_TAC [`p:bool`; `p0:bool`; `p1:bool`; `p2:bool`] THEN
 118   ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC);;
 119 (* }}} *)
 120
 121 let signs_lem0002 = prove(
 122   `!p. p <> &0 ==> (p > &0) \/ (p < &0)`,REWRITE_TAC [NEQ] THEN REAL_ARITH_TAC);;
 123 let signs_lem0003 = TAUT `a \/ b ==> (a ==> x) ==> (b ==> y) ==> (a /\ x \/ b /\ y)`;;
 124
 125 let PULL_CASES_THM_NZ = prove
 126  (`!a p p1 p2.
 127   (a <> &0) ==> ((a > &0 /\ (p <=> p1) \/ a < &0 /\ (p <=> p2)) <=>
 128    ((p <=> a > &0 /\ p1 \/ a < &0 /\ p2)))`,
 129 (* {{{ Proof *)
 130    REWRITE_TAC[NEQ] THEN
 131    REPEAT STRIP_TAC THEN
 132    REWRITE_TAC[NEQ] THEN
 133    MAP_EVERY BOOL_CASES_TAC [`p:bool`; `p0:bool`; `p1:bool`; `p2:bool`] THEN
 134    ASM_REWRITE_TAC[] THEN TRY (POP_ASSUM MP_TAC THEN REAL_ARITH_TAC)
 135 );;
 136 (* }}} *)