11 FUNCTION nodups -- if done to goal clauses too! |
11 FUNCTION nodups -- if done to goal clauses too! |
12 *) |
12 *) |
13 |
13 |
14 local |
14 local |
15 |
15 |
16 (*Prove theorems using fast_tac*) |
16 val not_conjD = thm "meson_not_conjD"; |
17 fun prove_fun s = |
17 val not_disjD = thm "meson_not_disjD"; |
18 prove_goal (the_context ()) s |
18 val not_notD = thm "meson_not_notD"; |
19 (fn prems => [ cut_facts_tac prems 1, Fast_tac 1 ]); |
19 val not_allD = thm "meson_not_allD"; |
20 |
20 val not_exD = thm "meson_not_exD"; |
21 (**** Negation Normal Form ****) |
21 val imp_to_disjD = thm "meson_imp_to_disjD"; |
22 |
22 val not_impD = thm "meson_not_impD"; |
23 (*** de Morgan laws ***) |
23 val iff_to_disjD = thm "meson_iff_to_disjD"; |
24 |
24 val not_iffD = thm "meson_not_iffD"; |
25 val not_conjD = prove_fun "~(P&Q) ==> ~P | ~Q"; |
25 val conj_exD1 = thm "meson_conj_exD1"; |
26 val not_disjD = prove_fun "~(P|Q) ==> ~P & ~Q"; |
26 val conj_exD2 = thm "meson_conj_exD2"; |
27 val not_notD = prove_fun "~~P ==> P"; |
27 val disj_exD = thm "meson_disj_exD"; |
28 val not_allD = prove_fun "~(ALL x. P(x)) ==> EX x. ~P(x)"; |
28 val disj_exD1 = thm "meson_disj_exD1"; |
29 val not_exD = prove_fun "~(EX x. P(x)) ==> ALL x. ~P(x)"; |
29 val disj_exD2 = thm "meson_disj_exD2"; |
30 |
30 val disj_assoc = thm "meson_disj_assoc"; |
31 |
31 val disj_comm = thm "meson_disj_comm"; |
32 (*** Removal of --> and <-> (positive and negative occurrences) ***) |
32 val disj_FalseD1 = thm "meson_disj_FalseD1"; |
33 |
33 val disj_FalseD2 = thm "meson_disj_FalseD2"; |
34 val imp_to_disjD = prove_fun "P-->Q ==> ~P | Q"; |
|
35 val not_impD = prove_fun "~(P-->Q) ==> P & ~Q"; |
|
36 |
|
37 val iff_to_disjD = prove_fun "P=Q ==> (~P | Q) & (~Q | P)"; |
|
38 |
|
39 (*Much more efficient than (P & ~Q) | (Q & ~P) for computing CNF*) |
|
40 val not_iffD = prove_fun "~(P=Q) ==> (P | Q) & (~P | ~Q)"; |
|
41 |
|
42 |
|
43 (**** Pulling out the existential quantifiers ****) |
|
44 |
|
45 (*** Conjunction ***) |
|
46 |
|
47 val conj_exD1 = prove_fun "(EX x. P(x)) & Q ==> EX x. P(x) & Q"; |
|
48 val conj_exD2 = prove_fun "P & (EX x. Q(x)) ==> EX x. P & Q(x)"; |
|
49 |
|
50 (*** Disjunction ***) |
|
51 |
|
52 (*DO NOT USE with forall-Skolemization: makes fewer schematic variables!! |
|
53 With ex-Skolemization, makes fewer Skolem constants*) |
|
54 val disj_exD = prove_fun "(EX x. P(x)) | (EX x. Q(x)) ==> EX x. P(x) | Q(x)"; |
|
55 |
|
56 val disj_exD1 = prove_fun "(EX x. P(x)) | Q ==> EX x. P(x) | Q"; |
|
57 val disj_exD2 = prove_fun "P | (EX x. Q(x)) ==> EX x. P | Q(x)"; |
|
58 |
|
59 |
|
60 |
|
61 (***** Generating clauses for the Meson Proof Procedure *****) |
|
62 |
|
63 (*** Disjunctions ***) |
|
64 |
|
65 val disj_assoc = prove_fun "(P|Q)|R ==> P|(Q|R)"; |
|
66 |
|
67 val disj_comm = prove_fun "P|Q ==> Q|P"; |
|
68 |
|
69 val disj_FalseD1 = prove_fun "False|P ==> P"; |
|
70 val disj_FalseD2 = prove_fun "P|False ==> P"; |
|
71 |
34 |
72 |
35 |
73 (**** Operators for forward proof ****) |
36 (**** Operators for forward proof ****) |
74 |
37 |
75 (*raises exception if no rules apply -- unlike RL*) |
38 (*raises exception if no rules apply -- unlike RL*) |