(* ------------------------------------------------------------------------- *) (* Evaluate a quantifier-free formula given a sign matrix row for its polys. *) (* ------------------------------------------------------------------------- *) (* let rec testform pmat fm = match fm with Atom(R(a,[p;Fn("0",[])])) -> let s = assoc p pmat in if a = "=" then s = Zero else if a = "<=" then s = Zero or s = Negative else if a = ">=" then s = Zero or s = Positive else if a = "<" then s = Negative else if a = ">" then s = Positive else failwith "testform: unknown literal" | False -> false | True -> true | Not(p) -> not(testform pmat p) | And(p,q) -> testform pmat p & testform pmat q | Or(p,q) -> testform pmat p or testform pmat q | Imp(p,q) -> not(testform pmat p) or testform pmat q | Iff(p,q) -> (testform pmat p = testform pmat q) | _ -> failwith "testform: non-propositional formula";; The model version of testform takes a row of the sign matrix in the form (p_1,s_1),(p_2,s_2),...,(p_n,s_n) The corresponding argument of TESTFORM is a theorem representing an `interpsigns` proposition. This is natural. The next argument, the formula to be tested, is the same. *) (* ====================================================================== *) (* Theorems *) (* ====================================================================== *) (* -------------------------------- T -------------------------------- *) let t_thm = prove(`!set:real->bool. (!x. set x ==> T)`,MESON_TAC[]);; (* -------------------------------- F --------------------------------- *) let f_thm = prove(`!set:real->bool. ~(?x. set x /\ F)`,MESON_TAC[]);; (* -------------------------------- ~ --------------------------------- *) let neg_thm_p = prove( `!P set. (!x. set x ==> P x) ==> (~ ?x. set x /\ ~ P x)`,MESON_TAC[]);; let neg_thm_n = prove( `!P set. (~ ?x. set x /\ P x) ==> (!x. set x ==> ~ P x)`,MESON_TAC[]);; (* -------------------------------- /\ -------------------------------- *) let and_thm_pp = prove( `!P Q set. (?x. set x) ==> (!x. set x ==> P x) ==> (!x. set x ==> Q x) ==> (!x. set x ==> (P x /\ Q x))`,MESON_TAC[]);; let and_thm_pn = prove( `!P Q set. (?x. set x) ==> (!x. set x ==> P x) ==> (~ ?x. set x /\ Q x) ==> (~ ?x. set x /\ P x /\ Q x)`,MESON_TAC[]);; let and_thm_np = prove( `!P Q set. (?x. set x) ==> (~ ?x. set x /\ P x) ==> (!x. set x ==> Q x) ==> (~ ?x. set x /\ P x /\ Q x)`,MESON_TAC[]);; let and_thm_nn = prove( `!P Q set. (?x. set x) ==> (~ ?x. set x /\ P x) ==> (~ ?x. set x /\ Q x) ==> (~ ?x. set x /\ P x /\ Q x)`,MESON_TAC[]);; (* -------------------------------- \/ -------------------------------- *) let or_thm_p = prove( `!P Q set. (?x. set x) ==> (!x. set x ==> P x) ==> (!x. set x ==> (P x \/ Q x))`, MESON_TAC[]);; let or_thm_q = prove( `!P Q set. (?x. set x) ==> (!x. set x ==> Q x) ==> (!x. set x ==> (P x \/ Q x))`, MESON_TAC[]);; let or_thm_nn = prove(`!P Q set. (?x. set x) ==> (~ ?x. set x /\ P x) ==> (~ ?x. set x /\ Q x) ==> (~ ?x. set x /\ (P x \/ Q x))`,MESON_TAC[]);; (* ------------------------------- ==> -------------------------------- *) let imp_thm_pp = prove(`!P Q set. (?x. set x) ==> (!x. set x ==> Q x) ==> (!x. set x ==> (P x ==> Q x))`,MESON_TAC[]);; let imp_thm_pn = prove(`!P Q set. (?x. set x) ==> (!x. set x ==> P x) ==> (~ ?x. set x /\ Q x) ==> (~ ?x. set x /\ (P x ==> Q x))`,MESON_TAC[]);; let imp_thm_n = prove(`!P Q set. (?x. set x) ==> (~ ?x. set x /\ P x) ==> (!x. set x ==> (P x ==> Q x))`,MESON_TAC[]);; (* -------------------------------- = --------------------------------- *) let iff_thm_pp = prove( `!P Q set. (?x. set x) ==> (!x. set x ==> P x) ==> (!x. set x ==> Q x) ==> (!x. set x ==> (P x <=> Q x))`,MESON_TAC[]);; let iff_thm_pn = prove( `!P Q set. (?x. set x) ==> (!x. set x ==> P x) ==> (~ ?x. set x /\ Q x) ==> (~ ?x. set x /\ (P x <=> Q x))`,MESON_TAC[]);; let iff_thm_np = prove( `!P Q set. (?x. set x) ==> (~ ?x. set x /\ P x) ==> (!x. set x ==> Q x) ==> (~ ?x. set x /\ (P x <=> Q x))`,MESON_TAC[]);; let iff_thm_nn = prove( `!P Q set. (?x. set x) ==> (~ ?x. set x /\ P x) ==> (~ ?x. set x /\ Q x) ==> (!x. set x ==> (P x <=> Q x))`,MESON_TAC[]);; (* ---------------------------------------------------------------------- *) (* Atoms *) (* ---------------------------------------------------------------------- *) (* --------------------------- ?x. p x < &0 --------------------------- *) let eq_lt_thm = prove( `!P set. (!x. set x ==> (P x = &0)) ==> ~ ?x. set x /\ P x < &0`, MESON_TAC[REAL_LT_LE]);; let gt_lt_thm = prove( `!P set. (!x. set x ==> (P x > &0)) ==> ~ ?x. set x /\ P x < &0`, MESON_TAC[real_gt;REAL_LT_REFL;REAL_LT_TRANS]);; (* --------------------------- ?x. p x = &0 --------------------------- *) let lt_eq_thm = prove( `!P set. (!x. set x ==> (P x < &0)) ==> ~ ?x. set x /\ (P x = &0)`, MESON_TAC[REAL_LT_LE]);; let gt_eq_thm = prove( `!P set. (!x. set x ==> (P x > &0)) ==> ~ ?x. set x /\ (P x = &0)`, MESON_TAC[real_gt;REAL_LT_LE]);; (* --------------------------- ?x. p x > &0 --------------------------- *) let eq_gt_thm = prove( `!P set. (!x. set x ==> (P x = &0)) ==> ~ ?x. set x /\ (P x > &0)`, MESON_TAC[real_gt;REAL_LT_LE]);; let lt_gt_thm = prove( `!P set. (!x. set x ==> (P x < &0)) ==> ~ ?x. set x /\ (P x > &0)`, MESON_TAC[real_gt;REAL_LT_LE;REAL_LT_TRANS]);; (* -------------------------- ?x. p x <= &0 --------------------------- *) let lt_le_thm = prove( `!P set. (!x. set x ==> (P x < &0)) ==> !x. set x ==> (P x <= &0)`, MESON_TAC[real_gt;REAL_LT_LE;REAL_LT_TRANS]);; let eq_le_thm = prove( `!P set. (!x. set x ==> (P x = &0)) ==> (!x. set x ==> (P x <= &0))`, MESON_TAC[real_gt;REAL_LT_LE;REAL_LT_TRANS;real_le]);; let gt_le_thm = prove( `!P set. (!x. set x ==> (P x > &0)) ==> ~ ?x. set x /\ (P x <= &0)`, MESON_TAC[real_gt;REAL_LT_LE;REAL_LT_TRANS;real_le]);; (* -------------------------- ?x. p x >= &0 --------------------------- *) let lt_ge_thm = prove( `!P set. (!x. set x ==> (P x < &0)) ==> ~ ?x. set x /\ (P x >= &0)`, MESON_TAC[real_gt;REAL_LT_LE;REAL_LT_TRANS;real_ge]);; let eq_ge_thm = prove( `!P set. (!x. set x ==> (P x = &0)) ==> (!x. set x ==> (P x >= &0))`, MESON_TAC[real_gt;REAL_LT_LE;REAL_LT_TRANS;real_ge;real_le]);; let gt_ge_thm = prove( `!P set. (!x. set x ==> (P x > &0)) ==> (!x. set x ==> (P x >= &0))`, MESON_TAC[real_gt;REAL_LT_LE;REAL_LT_TRANS;real_ge;real_le]);; (* let lookup_sign isigns_thm fm = *) (* let asms,_ = dest_thm isigns_thm in *) (* let *) let NOT_EXISTS_CONJ_THM = prove_by_refinement( `~(?x. P x /\ Q x) ==> (!x. P x ==> ~Q x)`, (* {{{ Proof *) [ MESON_TAC[]; ]);; (* }}} *) let testform_itlem = prove_by_refinement( `(!x. P x ==> ~Q x) ==> (!x. P2 x ==> ~Q x) ==> (!x. P x \/ P2 x ==> ~ Q x)`, (* {{{ Proof *) [MESON_TAC[]]);; (* }}} *)