24 |
24 |
25 val demorgans = map prove_fun |
25 val demorgans = map prove_fun |
26 ["~(P&Q) <-> ~P | ~Q", |
26 ["~(P&Q) <-> ~P | ~Q", |
27 "~(P|Q) <-> ~P & ~Q", |
27 "~(P|Q) <-> ~P & ~Q", |
28 "~~P <-> P", |
28 "~~P <-> P", |
29 "~(ALL x.P(x)) <-> (EX x. ~P(x))", |
29 "~(ALL x. P(x)) <-> (EX x. ~P(x))", |
30 "~(EX x.P(x)) <-> (ALL x. ~P(x))"]; |
30 "~(EX x. P(x)) <-> (ALL x. ~P(x))"]; |
31 |
31 |
32 (*** Removal of --> and <-> (positive and negative occurrences) ***) |
32 (*** Removal of --> and <-> (positive and negative occurrences) ***) |
33 (*Last one is important for computing a compact CNF*) |
33 (*Last one is important for computing a compact CNF*) |
34 val nnf_simps = map prove_fun |
34 val nnf_simps = map prove_fun |
35 ["(P-->Q) <-> (~P | Q)", |
35 ["(P-->Q) <-> (~P | Q)", |
41 |
41 |
42 (*** Pushing in the existential quantifiers ***) |
42 (*** Pushing in the existential quantifiers ***) |
43 |
43 |
44 val ex_simps = map prove_fun |
44 val ex_simps = map prove_fun |
45 ["(EX x. P) <-> P", |
45 ["(EX x. P) <-> P", |
46 "(EX x. P(x) & Q) <-> (EX x.P(x)) & Q", |
46 "(EX x. P(x) & Q) <-> (EX x. P(x)) & Q", |
47 "(EX x. P & Q(x)) <-> P & (EX x.Q(x))", |
47 "(EX x. P & Q(x)) <-> P & (EX x. Q(x))", |
48 "(EX x. P(x) | Q(x)) <-> (EX x.P(x)) | (EX x.Q(x))", |
48 "(EX x. P(x) | Q(x)) <-> (EX x. P(x)) | (EX x. Q(x))", |
49 "(EX x. P(x) | Q) <-> (EX x.P(x)) | Q", |
49 "(EX x. P(x) | Q) <-> (EX x. P(x)) | Q", |
50 "(EX x. P | Q(x)) <-> P | (EX x.Q(x))"]; |
50 "(EX x. P | Q(x)) <-> P | (EX x. Q(x))"]; |
51 |
51 |
52 (*** Pushing in the universal quantifiers ***) |
52 (*** Pushing in the universal quantifiers ***) |
53 |
53 |
54 val all_simps = map prove_fun |
54 val all_simps = map prove_fun |
55 ["(ALL x. P) <-> P", |
55 ["(ALL x. P) <-> P", |
56 "(ALL x. P(x) & Q(x)) <-> (ALL x.P(x)) & (ALL x.Q(x))", |
56 "(ALL x. P(x) & Q(x)) <-> (ALL x. P(x)) & (ALL x. Q(x))", |
57 "(ALL x. P(x) & Q) <-> (ALL x.P(x)) & Q", |
57 "(ALL x. P(x) & Q) <-> (ALL x. P(x)) & Q", |
58 "(ALL x. P & Q(x)) <-> P & (ALL x.Q(x))", |
58 "(ALL x. P & Q(x)) <-> P & (ALL x. Q(x))", |
59 "(ALL x. P(x) | Q) <-> (ALL x.P(x)) | Q", |
59 "(ALL x. P(x) | Q) <-> (ALL x. P(x)) | Q", |
60 "(ALL x. P | Q(x)) <-> P | (ALL x.Q(x))"]; |
60 "(ALL x. P | Q(x)) <-> P | (ALL x. Q(x))"]; |
61 |
61 |
62 |
62 |
63 val mini_ss=FOL_basic_ss addsimps (demorgans @ nnf_simps @ ex_simps @ all_simps); |
63 val mini_ss=FOL_basic_ss addsimps (demorgans @ nnf_simps @ ex_simps @ all_simps); |
64 |
64 |
65 val mini_tac = rtac ccontr THEN' asm_full_simp_tac mini_ss; |
65 val mini_tac = rtac ccontr THEN' asm_full_simp_tac mini_ss; |