src/FOL/ex/mini.ML
author oheimb
Sat, 15 Feb 1997 17:44:10 +0100
changeset 2634 b85c77b64c7a
parent 1954 4b5b2d04782c
child 3835 9a5a4e123859
permissions -rw-r--r--
updated mini_ss
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1459
d12da312eff4 expanded tabs
clasohm
parents: 743
diff changeset
     1
(*  Title:      FOL/ex/mini
663
dc3f0582e839 Miniscope conversoin; example of formula rewriting
lcp
parents:
diff changeset
     2
    ID:         $Id$
1459
d12da312eff4 expanded tabs
clasohm
parents: 743
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
663
dc3f0582e839 Miniscope conversoin; example of formula rewriting
lcp
parents:
diff changeset
     4
    Copyright   1994  University of Cambridge
dc3f0582e839 Miniscope conversoin; example of formula rewriting
lcp
parents:
diff changeset
     5
dc3f0582e839 Miniscope conversoin; example of formula rewriting
lcp
parents:
diff changeset
     6
Classical First-Order Logic
dc3f0582e839 Miniscope conversoin; example of formula rewriting
lcp
parents:
diff changeset
     7
dc3f0582e839 Miniscope conversoin; example of formula rewriting
lcp
parents:
diff changeset
     8
Conversion to nnf/miniscope format: pushing quantifiers in
dc3f0582e839 Miniscope conversoin; example of formula rewriting
lcp
parents:
diff changeset
     9
dc3f0582e839 Miniscope conversoin; example of formula rewriting
lcp
parents:
diff changeset
    10
Demonstration of formula rewriting by proof
dc3f0582e839 Miniscope conversoin; example of formula rewriting
lcp
parents:
diff changeset
    11
*)
dc3f0582e839 Miniscope conversoin; example of formula rewriting
lcp
parents:
diff changeset
    12
dc3f0582e839 Miniscope conversoin; example of formula rewriting
lcp
parents:
diff changeset
    13
val ccontr = FalseE RS classical;
dc3f0582e839 Miniscope conversoin; example of formula rewriting
lcp
parents:
diff changeset
    14
dc3f0582e839 Miniscope conversoin; example of formula rewriting
lcp
parents:
diff changeset
    15
(**** Negation Normal Form ****)
dc3f0582e839 Miniscope conversoin; example of formula rewriting
lcp
parents:
diff changeset
    16
dc3f0582e839 Miniscope conversoin; example of formula rewriting
lcp
parents:
diff changeset
    17
(*** de Morgan laws ***)
dc3f0582e839 Miniscope conversoin; example of formula rewriting
lcp
parents:
diff changeset
    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
d12da312eff4 expanded tabs
clasohm
parents: 743
diff changeset
    23
                  (Cla.fast_tac FOL_cs 1) ]));
663
dc3f0582e839 Miniscope conversoin; example of formula rewriting
lcp
parents:
diff changeset
    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
d12da312eff4 expanded tabs
clasohm
parents: 743
diff changeset
    26
                  ["~(P&Q) <-> ~P | ~Q",
d12da312eff4 expanded tabs
clasohm
parents: 743
diff changeset
    27
                   "~(P|Q) <-> ~P & ~Q",
d12da312eff4 expanded tabs
clasohm
parents: 743
diff changeset
    28
                   "~~P <-> P",
d12da312eff4 expanded tabs
clasohm
parents: 743
diff changeset
    29
                   "~(ALL x.P(x)) <-> (EX x. ~P(x))",
d12da312eff4 expanded tabs
clasohm
parents: 743
diff changeset
    30
                   "~(EX x.P(x)) <-> (ALL x. ~P(x))"];
663
dc3f0582e839 Miniscope conversoin; example of formula rewriting
lcp
parents:
diff changeset
    31
dc3f0582e839 Miniscope conversoin; example of formula rewriting
lcp
parents:
diff changeset
    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*)
1954
4b5b2d04782c Some renaming. Note that this miniscoping is more
paulson
parents: 1459
diff changeset
    34
val nnf_simps = map prove_fun
1459
d12da312eff4 expanded tabs
clasohm
parents: 743
diff changeset
    35
                ["(P-->Q) <-> (~P | Q)",
d12da312eff4 expanded tabs
clasohm
parents: 743
diff changeset
    36
                 "~(P-->Q) <-> (P & ~Q)",
d12da312eff4 expanded tabs
clasohm
parents: 743
diff changeset
    37
                 "(P<->Q) <-> (~P | Q) & (~Q | P)",
d12da312eff4 expanded tabs
clasohm
parents: 743
diff changeset
    38
                 "~(P<->Q) <-> (P | Q) & (~P | ~Q)"];
663
dc3f0582e839 Miniscope conversoin; example of formula rewriting
lcp
parents:
diff changeset
    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
dc3f0582e839 Miniscope conversoin; example of formula rewriting
lcp
parents:
diff changeset
    41
dc3f0582e839 Miniscope conversoin; example of formula rewriting
lcp
parents:
diff changeset
    42
(*** Pushing in the existential quantifiers ***)
dc3f0582e839 Miniscope conversoin; example of formula rewriting
lcp
parents:
diff changeset
    43
1954
4b5b2d04782c Some renaming. Note that this miniscoping is more
paulson
parents: 1459
diff changeset
    44
val ex_simps = map prove_fun 
1459
d12da312eff4 expanded tabs
clasohm
parents: 743
diff changeset
    45
                ["(EX x. P) <-> P",
d12da312eff4 expanded tabs
clasohm
parents: 743
diff changeset
    46
                 "(EX x. P(x) & Q) <-> (EX x.P(x)) & Q",
d12da312eff4 expanded tabs
clasohm
parents: 743
diff changeset
    47
                 "(EX x. P & Q(x)) <-> P & (EX x.Q(x))",
d12da312eff4 expanded tabs
clasohm
parents: 743
diff changeset
    48
                 "(EX x. P(x) | Q(x)) <-> (EX x.P(x)) | (EX x.Q(x))",
d12da312eff4 expanded tabs
clasohm
parents: 743
diff changeset
    49
                 "(EX x. P(x) | Q) <-> (EX x.P(x)) | Q",
d12da312eff4 expanded tabs
clasohm
parents: 743
diff changeset
    50
                 "(EX x. P | Q(x)) <-> P | (EX x.Q(x))"];
663
dc3f0582e839 Miniscope conversoin; example of formula rewriting
lcp
parents:
diff changeset
    51
dc3f0582e839 Miniscope conversoin; example of formula rewriting
lcp
parents:
diff changeset
    52
(*** Pushing in the universal quantifiers ***)
dc3f0582e839 Miniscope conversoin; example of formula rewriting
lcp
parents:
diff changeset
    53
1954
4b5b2d04782c Some renaming. Note that this miniscoping is more
paulson
parents: 1459
diff changeset
    54
val all_simps = map prove_fun
1459
d12da312eff4 expanded tabs
clasohm
parents: 743
diff changeset
    55
                ["(ALL x. P) <-> P",
d12da312eff4 expanded tabs
clasohm
parents: 743
diff changeset
    56
                 "(ALL x. P(x) & Q(x)) <-> (ALL x.P(x)) & (ALL x.Q(x))",
d12da312eff4 expanded tabs
clasohm
parents: 743
diff changeset
    57
                 "(ALL x. P(x) & Q) <-> (ALL x.P(x)) & Q",
d12da312eff4 expanded tabs
clasohm
parents: 743
diff changeset
    58
                 "(ALL x. P & Q(x)) <-> P & (ALL x.Q(x))",
d12da312eff4 expanded tabs
clasohm
parents: 743
diff changeset
    59
                 "(ALL x. P(x) | Q) <-> (ALL x.P(x)) | Q",
d12da312eff4 expanded tabs
clasohm
parents: 743
diff changeset
    60
                 "(ALL x. P | Q(x)) <-> P | (ALL x.Q(x))"];
663
dc3f0582e839 Miniscope conversoin; example of formula rewriting
lcp
parents:
diff changeset
    61
dc3f0582e839 Miniscope conversoin; example of formula rewriting
lcp
parents:
diff changeset
    62
2634
b85c77b64c7a updated mini_ss
oheimb
parents: 1954
diff changeset
    63
val mini_ss=FOL_basic_ss addsimps (demorgans @ nnf_simps @ ex_simps @ all_simps);
663
dc3f0582e839 Miniscope conversoin; example of formula rewriting
lcp
parents:
diff changeset
    64
743
9dcce140bdfc prove_fun: new; no longer depends upon the version in simpdata.ML
lcp
parents: 663
diff changeset
    65
val mini_tac = rtac ccontr THEN' asm_full_simp_tac mini_ss;
663
dc3f0582e839 Miniscope conversoin; example of formula rewriting
lcp
parents:
diff changeset
    66