satScript.sml

1
2(* random theorems used here, there, everywhere by HolSatLib *)
3Theory sat[bare]
4Ancestors
5  bool
6Libs
7  Globals HolKernel Parse Drule Thm Tactical Tactic Rewrite
8
9
10(* gross truth table method for proving propositional tautologies *)
11(* used to bootstrap HolSatLib *)
12fun TT_TAUT_PROVE tm =
13    let val (qv,tm) = boolSyntax.strip_forall tm
14        val fv = free_vars tm
15    in GENL qv (prove(tm,(MAP_EVERY BOOL_CASES_TAC fv) THEN REWRITE_TAC [])) end
16
17Theorem AND_IMP =
18  TT_TAUT_PROVE ``!A B C. A /\ B ==> C <=> A ==> B ==> C``
19Theorem NOT_NOT =
20  GEN_ALL (hd (CONJUNCTS (SPEC_ALL NOT_CLAUSES)))
21Theorem AND_INV = TT_TAUT_PROVE ``!A. ~A /\ A <=> F``
22Theorem AND_INV_IMP = TT_TAUT_PROVE ``!A. A ==> ~A ==> F``
23Theorem OR_DUAL =
24  TT_TAUT_PROVE ``(~(A \/ B) ==> F) = (~A ==> ~B ==> F)``
25Theorem OR_DUAL2 =
26  TT_TAUT_PROVE ``(~(A \/ B) ==> F) = ((A==>F) ==> ~B ==> F)``
27Theorem OR_DUAL3 =
28  TT_TAUT_PROVE ``(~(~A \/ B) ==> F) = (A ==> ~B ==> F)``
29Theorem AND_INV2 =
30  TT_TAUT_PROVE ``(~A ==> F) ==> (A==>F) ==> F``
31Theorem NOT_ELIM2 = TT_TAUT_PROVE ``(~A ==> F) = A``
32
33(* for satTools.sml *)
34Theorem EQT_Imp1 = TT_TAUT_PROVE ``!b. b ==> (b=T)``
35Theorem EQF_Imp1 = TT_TAUT_PROVE ``!b. (~b) ==> (b=F)``
36
37(* for def_cnf.sml *)
38Theorem dc_eq =
39   TT_TAUT_PROVE “(p = (q = r)) <=>
40                    (p \/ q \/ r) /\ (p \/ ~r \/ ~q) /\ (q \/ ~r \/ ~p) /\
41                    (r \/ ~q \/ ~p)”
42
43Theorem dc_conj =
44  TT_TAUT_PROVE “(p = (q /\ r)) <=> (p \/ ~q \/ ~r) /\ (q \/ ~p) /\ (r \/ ~p)”
45
46Theorem dc_disj =
47  TT_TAUT_PROVE “(p = (q \/ r)) <=> (p \/ ~q) /\ (p \/ ~r) /\ (q \/ r \/ ~p)”
48
49Theorem dc_imp =
50  TT_TAUT_PROVE “(p = (q ==> r)) <=> (p \/ q) /\ (p \/ ~r) /\ (~q \/ r \/ ~p)”
51
52Theorem dc_neg = TT_TAUT_PROVE “(p = ~q) <=> (p \/ q) /\ (~q \/ ~p)”
53
54Theorem dc_cond =
55  TT_TAUT_PROVE “(p = (if q then r else s)) <=>
56                   (p \/ q \/ ~s) /\ (p \/ ~r \/ ~q) /\ (p \/ ~r \/ ~s) /\
57                   (~q \/ r \/ ~p) /\ (q \/ s \/ ~p)”
58
59val [pth_ni1, pth_ni2, pth_no1, pth_no2, pth_an1, pth_an2, pth_nn] =
60            (CONJUNCTS o TT_TAUT_PROVE)
61             ``(~(p ==> q) ==> p)  /\ (~(p ==> q) ==> ~q)
62            /\ (~(p \/ q)  ==> ~p) /\ (~(p \/ q)  ==> ~q)
63            /\ ((p /\ q)   ==> p)  /\ ((p /\ q)   ==> q)
64            /\ ((~ ~p)     ==> p)``
65Theorem pth_ni1 = pth_ni1
66Theorem pth_ni2 = pth_ni2
67Theorem pth_no1 = pth_no1
68Theorem pth_no2 = pth_no2
69Theorem pth_an1 = pth_an1
70Theorem pth_an2 = pth_an2
71Theorem pth_nn = pth_nn