src/Provers/genelim.ML
author nipkow
Fri, 09 Oct 1998 14:19:13 +0200
changeset 5633 fb7fa1b154c4
parent 927 305e7cfda869
permissions -rw-r--r--
Added a few breaks in error text.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     1
(** Generalized elimination rules **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     3
(*Generalized elimination for two conclusions*)
927
305e7cfda869 replaced Pure by ProtoPure
clasohm
parents: 0
diff changeset
     4
val prems = goal proto_pure_thy 
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
     "[| PROP U ==> PROP VA;  \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     6
\        PROP U ==> PROP VB;  \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
\        PROP U;              \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     8
\        [| PROP VA; PROP VB |] ==> PROP W    \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     9
\     |] ==> PROP W";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
by (REPEAT (resolve_tac prems 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    11
val general_elim2_rl = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    12
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    13
fun make_elim2 (rl1,rl2) = standard (rl2 COMP rl1 COMP general_elim2_rl);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    14
fun elim2_tac (rl1,rl2) = eresolve_tac [rl2 COMP rl1 COMP general_elim2_rl];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    15
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    16
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    17
(*For example,  make_elim2(conjunct1,conjunct2)  
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    18
  yields conjunction elimination *)