Rqe/testform_thms.ml

   1 (* ------------------------------------------------------------------------- *)
   2 (* Evaluate a quantifier-free formula given a sign matrix row for its polys. *)
   3 (* ------------------------------------------------------------------------- *)
   4
   5 (*
   6 let rec testform pmat fm =
   7   match fm with
   8       Atom(R(a,[p;Fn("0",[])])) ->
   9         let s = assoc p pmat in
  10           if a = "=" then s = Zero
  11           else if a = "<=" then s = Zero or s = Negative
  12           else if a = ">=" then s = Zero or s = Positive
  13           else if a = "<" then s = Negative
  14           else if a = ">" then s = Positive
  15           else failwith "testform: unknown literal"
  16     | False -> false
  17     | True -> true
  18     | Not(p) -> not(testform pmat p)
  19     | And(p,q) -> testform pmat p & testform pmat q
  20     | Or(p,q) -> testform pmat p or testform pmat q
  21     | Imp(p,q) -> not(testform pmat p) or testform pmat q
  22     | Iff(p,q) -> (testform pmat p = testform pmat q)
  23     | _ -> failwith "testform: non-propositional formula";;
  24
  25 The model version of testform takes a row of the sign matrix in the form
  26  (p_1,s_1),(p_2,s_2),...,(p_n,s_n)
  27 The corresponding argument of TESTFORM is a theorem representing
  28 an `interpsigns` proposition.  This is natural.  The next argument,
  29 the formula to be tested, is the same.
  30
  31 *)
  32
  33 (* ====================================================================== *)
  34 (*  Theorems                                                              *)
  35 (* ====================================================================== *)
  36
  37 (* --------------------------------  T   -------------------------------- *)
  38
  39 let t_thm = prove(`!set:real->bool. (!x. set x ==> T)`,MESON_TAC[]);;
  40
  41 (* --------------------------------  F  --------------------------------- *)
  42
  43 let f_thm = prove(`!set:real->bool. ~(?x. set x /\ F)`,MESON_TAC[]);;
  44
  45 (* --------------------------------  ~  --------------------------------- *)
  46
  47 let neg_thm_p = prove(
  48   `!P set. (!x. set x ==> P x) ==> (~ ?x. set x /\ ~ P x)`,MESON_TAC[]);;
  49
  50 let neg_thm_n = prove(
  51   `!P set. (~ ?x. set x /\ P x) ==> (!x. set x ==> ~ P x)`,MESON_TAC[]);;
  52
  53 (* --------------------------------  /\  -------------------------------- *)
  54
  55 let and_thm_pp = prove(
  56   `!P Q set. (?x. set x) ==> (!x. set x ==> P x) ==> (!x. set x ==> Q x) ==>
  57         (!x. set x ==> (P x /\ Q x))`,MESON_TAC[]);;
  58
  59 let and_thm_pn = prove(
  60   `!P Q set. (?x. set x) ==> (!x. set x ==> P x) ==>
  61      (~ ?x. set x /\ Q x) ==> (~ ?x. set x /\ P x /\ Q x)`,MESON_TAC[]);;
  62
  63 let and_thm_np = prove(
  64   `!P Q set. (?x. set x) ==> (~ ?x. set x /\ P x) ==>
  65           (!x. set x ==> Q x) ==> (~ ?x. set x /\ P x /\ Q x)`,MESON_TAC[]);;
  66
  67 let and_thm_nn = prove(
  68   `!P Q set. (?x. set x) ==> (~ ?x. set x /\ P x) ==>
  69     (~ ?x. set x /\ Q x) ==> (~ ?x. set x /\ P x /\ Q x)`,MESON_TAC[]);;
  70
  71 (* --------------------------------  \/  -------------------------------- *)
  72
  73 let or_thm_p = prove(
  74 `!P Q set. (?x. set x) ==> (!x. set x ==> P x) ==> (!x. set x ==> (P x \/ Q x))`,
  75   MESON_TAC[]);;
  76
  77 let or_thm_q = prove(
  78   `!P Q set. (?x. set x) ==> (!x. set x ==> Q x) ==> (!x. set x ==> (P x \/ Q x))`,
  79   MESON_TAC[]);;
  80
  81 let or_thm_nn =
  82   prove(`!P Q set. (?x. set x) ==> (~ ?x. set x /\ P x) ==>
  83           (~ ?x. set x /\ Q x) ==> (~ ?x. set x /\ (P x \/ Q x))`,MESON_TAC[]);;
  84
  85 (* -------------------------------  ==>  -------------------------------- *)
  86
  87 let imp_thm_pp =
  88   prove(`!P Q set. (?x. set x) ==> (!x. set x ==> Q x) ==>
  89         (!x. set x ==> (P x ==> Q x))`,MESON_TAC[]);;
  90
  91 let imp_thm_pn =
  92   prove(`!P Q set. (?x. set x) ==> (!x. set x ==> P x) ==>
  93         (~ ?x. set x /\ Q x) ==> (~ ?x. set x /\ (P x ==> Q x))`,MESON_TAC[]);;
  94
  95 let imp_thm_n =
  96   prove(`!P Q set. (?x. set x) ==> (~ ?x. set x /\ P x) ==>
  97      (!x. set x ==> (P x ==> Q x))`,MESON_TAC[]);;
  98
  99 (* --------------------------------  =  --------------------------------- *)
 100
 101 let iff_thm_pp = prove(
 102   `!P Q set. (?x. set x) ==> (!x. set x ==> P x) ==> (!x. set x ==> Q x) ==>
 103         (!x. set x ==> (P x <=> Q x))`,MESON_TAC[]);;
 104
 105 let iff_thm_pn = prove(
 106   `!P Q set. (?x. set x) ==> (!x. set x ==> P x) ==>
 107      (~ ?x. set x /\ Q x) ==> (~ ?x. set x /\ (P x <=> Q x))`,MESON_TAC[]);;
 108
 109 let iff_thm_np = prove(
 110   `!P Q set. (?x. set x) ==> (~ ?x. set x /\ P x) ==>
 111           (!x. set x ==> Q x) ==> (~ ?x. set x /\ (P x <=> Q x))`,MESON_TAC[]);;
 112
 113 let iff_thm_nn = prove(
 114   `!P Q set. (?x. set x) ==> (~ ?x. set x /\ P x) ==>
 115     (~ ?x. set x /\ Q x) ==> (!x. set x ==> (P x <=> Q x))`,MESON_TAC[]);;
 116
 117 (* ---------------------------------------------------------------------- *)
 118 (*  Atoms                                                                 *)
 119 (* ---------------------------------------------------------------------- *)
 120
 121 (* ---------------------------  ?x. p x < &0  --------------------------- *)
 122
 123 let eq_lt_thm = prove(
 124   `!P set. (!x. set x ==> (P x = &0)) ==> ~ ?x. set x /\ P x < &0`,
 125   MESON_TAC[REAL_LT_LE]);;
 126
 127 let gt_lt_thm = prove(
 128   `!P set. (!x. set x ==> (P x > &0)) ==> ~ ?x. set x /\ P x < &0`,
 129   MESON_TAC[real_gt;REAL_LT_REFL;REAL_LT_TRANS]);;
 130
 131 (* ---------------------------  ?x. p x = &0  --------------------------- *)
 132
 133 let lt_eq_thm = prove(
 134   `!P set. (!x. set x ==> (P x < &0)) ==> ~ ?x. set x /\ (P x = &0)`,
 135   MESON_TAC[REAL_LT_LE]);;
 136
 137 let gt_eq_thm = prove(
 138   `!P set. (!x. set x ==> (P x > &0)) ==> ~ ?x. set x /\ (P x = &0)`,
 139   MESON_TAC[real_gt;REAL_LT_LE]);;
 140
 141 (* ---------------------------  ?x. p x > &0  --------------------------- *)
 142
 143 let eq_gt_thm = prove(
 144   `!P set. (!x. set x ==> (P x = &0)) ==> ~ ?x. set x /\ (P x > &0)`,
 145   MESON_TAC[real_gt;REAL_LT_LE]);;
 146
 147 let lt_gt_thm = prove(
 148   `!P set. (!x. set x ==> (P x < &0)) ==> ~ ?x. set x /\ (P x > &0)`,
 149   MESON_TAC[real_gt;REAL_LT_LE;REAL_LT_TRANS]);;
 150
 151 (* --------------------------  ?x. p x <= &0  --------------------------- *)
 152
 153 let lt_le_thm = prove(
 154   `!P set. (!x. set x ==> (P x < &0)) ==> !x. set x ==> (P x <= &0)`,
 155   MESON_TAC[real_gt;REAL_LT_LE;REAL_LT_TRANS]);;
 156
 157 let eq_le_thm = prove(
 158   `!P set. (!x. set x ==> (P x = &0)) ==> (!x. set x ==> (P x <= &0))`,
 159   MESON_TAC[real_gt;REAL_LT_LE;REAL_LT_TRANS;real_le]);;
 160
 161 let gt_le_thm = prove(
 162   `!P set. (!x. set x ==> (P x > &0)) ==> ~ ?x. set x /\ (P x <= &0)`,
 163   MESON_TAC[real_gt;REAL_LT_LE;REAL_LT_TRANS;real_le]);;
 164
 165 (* --------------------------  ?x. p x >= &0  --------------------------- *)
 166
 167 let lt_ge_thm = prove(
 168   `!P set. (!x. set x ==> (P x < &0)) ==> ~ ?x. set x /\ (P x >= &0)`,
 169   MESON_TAC[real_gt;REAL_LT_LE;REAL_LT_TRANS;real_ge]);;
 170
 171 let eq_ge_thm = prove(
 172   `!P set. (!x. set x ==> (P x = &0)) ==> (!x. set x ==> (P x >= &0))`,
 173   MESON_TAC[real_gt;REAL_LT_LE;REAL_LT_TRANS;real_ge;real_le]);;
 174
 175 let gt_ge_thm = prove(
 176   `!P set. (!x. set x ==> (P x > &0)) ==> (!x. set x ==> (P x >= &0))`,
 177   MESON_TAC[real_gt;REAL_LT_LE;REAL_LT_TRANS;real_ge;real_le]);;
 178
 179 (* let lookup_sign isigns_thm fm =  *)
 180 (*   let asms,_ = dest_thm isigns_thm in *)
 181 (*   let    *)
 182
 183
 184 let NOT_EXISTS_CONJ_THM = prove_by_refinement(
 185   `~(?x. P x /\ Q x) ==> (!x. P x ==> ~Q x)`,
 186 (* {{{ Proof *)
 187 [
 188   MESON_TAC[];
 189 ]);;
 190 (* }}} *)
 191
 192 let testform_itlem = prove_by_refinement(
 193   `(!x. P x ==> ~Q x) ==> (!x. P2 x ==> ~Q x) ==> (!x. P x \/ P2 x ==> ~ Q x)`,
 194 (* {{{ Proof *)
 195 [MESON_TAC[]]);;
 196 (* }}} *)