author | paulson |
Wed, 20 Mar 1996 18:42:31 +0100 | |
changeset 1593 | 69ed69a9c32a |
parent 1459 | d12da312eff4 |
child 1954 | 4b5b2d04782c |
permissions | -rw-r--r-- |
1459 | 1 |
(* Title: FOL/ex/mini |
663 | 2 |
ID: $Id$ |
1459 | 3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
663 | 4 |
Copyright 1994 University of Cambridge |
5 |
||
6 |
Classical First-Order Logic |
|
7 |
||
8 |
Conversion to nnf/miniscope format: pushing quantifiers in |
|
9 |
||
10 |
Demonstration of formula rewriting by proof |
|
11 |
*) |
|
12 |
||
13 |
val ccontr = FalseE RS classical; |
|
14 |
||
15 |
(**** Negation Normal Form ****) |
|
16 |
||
17 |
(*** de Morgan laws ***) |
|
18 |
||
743
9dcce140bdfc
prove_fun: new; no longer depends upon the version in simpdata.ML
lcp
parents:
663
diff
changeset
|
19 |
fun prove_fun s = |
9dcce140bdfc
prove_fun: new; no longer depends upon the version in simpdata.ML
lcp
parents:
663
diff
changeset
|
20 |
(writeln s; |
9dcce140bdfc
prove_fun: new; no longer depends upon the version in simpdata.ML
lcp
parents:
663
diff
changeset
|
21 |
prove_goal FOL.thy s |
9dcce140bdfc
prove_fun: new; no longer depends upon the version in simpdata.ML
lcp
parents:
663
diff
changeset
|
22 |
(fn prems => [ (cut_facts_tac prems 1), |
1459 | 23 |
(Cla.fast_tac FOL_cs 1) ])); |
663 | 24 |
|
743
9dcce140bdfc
prove_fun: new; no longer depends upon the version in simpdata.ML
lcp
parents:
663
diff
changeset
|
25 |
val demorgans = map prove_fun |
1459 | 26 |
["~(P&Q) <-> ~P | ~Q", |
27 |
"~(P|Q) <-> ~P & ~Q", |
|
28 |
"~~P <-> P", |
|
29 |
"~(ALL x.P(x)) <-> (EX x. ~P(x))", |
|
30 |
"~(EX x.P(x)) <-> (ALL x. ~P(x))"]; |
|
663 | 31 |
|
32 |
(*** Removal of --> and <-> (positive and negative occurrences) ***) |
|
743
9dcce140bdfc
prove_fun: new; no longer depends upon the version in simpdata.ML
lcp
parents:
663
diff
changeset
|
33 |
(*Last one is important for computing a compact CNF*) |
9dcce140bdfc
prove_fun: new; no longer depends upon the version in simpdata.ML
lcp
parents:
663
diff
changeset
|
34 |
val nnf_rews = map prove_fun |
1459 | 35 |
["(P-->Q) <-> (~P | Q)", |
36 |
"~(P-->Q) <-> (P & ~Q)", |
|
37 |
"(P<->Q) <-> (~P | Q) & (~Q | P)", |
|
38 |
"~(P<->Q) <-> (P | Q) & (~P | ~Q)"]; |
|
663 | 39 |
|
743
9dcce140bdfc
prove_fun: new; no longer depends upon the version in simpdata.ML
lcp
parents:
663
diff
changeset
|
40 |
(* BEWARE: rewrite rules for <-> can confuse the simplifier!! *) |
663 | 41 |
|
42 |
(*** Pushing in the existential quantifiers ***) |
|
43 |
||
743
9dcce140bdfc
prove_fun: new; no longer depends upon the version in simpdata.ML
lcp
parents:
663
diff
changeset
|
44 |
val ex_rews = map prove_fun |
1459 | 45 |
["(EX x. P) <-> P", |
46 |
"(EX x. P(x) & Q) <-> (EX x.P(x)) & Q", |
|
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))", |
|
49 |
"(EX x. P(x) | Q) <-> (EX x.P(x)) | Q", |
|
50 |
"(EX x. P | Q(x)) <-> P | (EX x.Q(x))"]; |
|
663 | 51 |
|
52 |
(*** Pushing in the universal quantifiers ***) |
|
53 |
||
743
9dcce140bdfc
prove_fun: new; no longer depends upon the version in simpdata.ML
lcp
parents:
663
diff
changeset
|
54 |
val all_rews = map prove_fun |
1459 | 55 |
["(ALL x. P) <-> P", |
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", |
|
58 |
"(ALL x. P & Q(x)) <-> P & (ALL x.Q(x))", |
|
59 |
"(ALL x. P(x) | Q) <-> (ALL x.P(x)) | Q", |
|
60 |
"(ALL x. P | Q(x)) <-> P | (ALL x.Q(x))"]; |
|
663 | 61 |
|
62 |
||
743
9dcce140bdfc
prove_fun: new; no longer depends upon the version in simpdata.ML
lcp
parents:
663
diff
changeset
|
63 |
val mini_ss = |
9dcce140bdfc
prove_fun: new; no longer depends upon the version in simpdata.ML
lcp
parents:
663
diff
changeset
|
64 |
empty_ss |
9dcce140bdfc
prove_fun: new; no longer depends upon the version in simpdata.ML
lcp
parents:
663
diff
changeset
|
65 |
setmksimps (map mk_meta_eq o atomize o gen_all) |
9dcce140bdfc
prove_fun: new; no longer depends upon the version in simpdata.ML
lcp
parents:
663
diff
changeset
|
66 |
setsolver (fn prems => resolve_tac (triv_rls@prems) |
1459 | 67 |
ORELSE' assume_tac |
68 |
ORELSE' etac FalseE) |
|
743
9dcce140bdfc
prove_fun: new; no longer depends upon the version in simpdata.ML
lcp
parents:
663
diff
changeset
|
69 |
setsubgoaler asm_simp_tac |
9dcce140bdfc
prove_fun: new; no longer depends upon the version in simpdata.ML
lcp
parents:
663
diff
changeset
|
70 |
addsimps (demorgans @ nnf_rews @ ex_rews @ all_rews); |
663 | 71 |
|
743
9dcce140bdfc
prove_fun: new; no longer depends upon the version in simpdata.ML
lcp
parents:
663
diff
changeset
|
72 |
val mini_tac = rtac ccontr THEN' asm_full_simp_tac mini_ss; |
663 | 73 |