src/FOLP/FOLP.ML
author wenzelm
Sun, 15 Oct 2000 19:50:35 +0200
changeset 10220 2a726de6e124
parent 9263 53e09e592278
permissions -rw-r--r--
proper symbol markup with \isamath, \isatext; support sub/super scripts:
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1459
d12da312eff4 expanded tabs
clasohm
parents: 1142
diff changeset
     1
(*  Title:      FOLP/FOLP.ML
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
1459
d12da312eff4 expanded tabs
clasohm
parents: 1142
diff changeset
     3
    Author:     Martin D Coen, Cambridge University Computer Laboratory
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
    Copyright   1991  University of Cambridge
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
1142
eb0e2ff8f032 Corrected comments in headers
lcp
parents: 0
diff changeset
     6
Tactics and lemmas for FOLP (Classical First-Order Logic with Proofs)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     8
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     9
(*** Classical introduction rules for | and EX ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
9263
53e09e592278 removal of batch style, and tidying
paulson
parents: 3836
diff changeset
    11
val prems= goal FOLP.thy 
53e09e592278 removal of batch style, and tidying
paulson
parents: 3836
diff changeset
    12
   "(!!x. x:~Q ==> f(x):P) ==> ?p : P|Q";
53e09e592278 removal of batch style, and tidying
paulson
parents: 3836
diff changeset
    13
by (rtac classical 1);
53e09e592278 removal of batch style, and tidying
paulson
parents: 3836
diff changeset
    14
by (REPEAT (ares_tac (prems@[disjI1,notI]) 1));
53e09e592278 removal of batch style, and tidying
paulson
parents: 3836
diff changeset
    15
by (REPEAT (ares_tac (prems@[disjI2,notE]) 1)) ;
53e09e592278 removal of batch style, and tidying
paulson
parents: 3836
diff changeset
    16
qed "disjCI";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    17
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    18
(*introduction rule involving only EX*)
9263
53e09e592278 removal of batch style, and tidying
paulson
parents: 3836
diff changeset
    19
val prems= goal FOLP.thy 
53e09e592278 removal of batch style, and tidying
paulson
parents: 3836
diff changeset
    20
   "( !!u. u:~(EX x. P(x)) ==> f(u):P(a)) ==> ?p : EX x. P(x)";
53e09e592278 removal of batch style, and tidying
paulson
parents: 3836
diff changeset
    21
by (rtac classical 1);
53e09e592278 removal of batch style, and tidying
paulson
parents: 3836
diff changeset
    22
by (eresolve_tac (prems RL [exI]) 1) ;
53e09e592278 removal of batch style, and tidying
paulson
parents: 3836
diff changeset
    23
qed "ex_classical";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    24
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    25
(*version of above, simplifying ~EX to ALL~ *)
9263
53e09e592278 removal of batch style, and tidying
paulson
parents: 3836
diff changeset
    26
val [prem]= goal FOLP.thy 
53e09e592278 removal of batch style, and tidying
paulson
parents: 3836
diff changeset
    27
   "(!!u. u:ALL x. ~P(x) ==> f(u):P(a)) ==> ?p : EX x. P(x)";
53e09e592278 removal of batch style, and tidying
paulson
parents: 3836
diff changeset
    28
by (rtac ex_classical 1);
53e09e592278 removal of batch style, and tidying
paulson
parents: 3836
diff changeset
    29
by (resolve_tac [notI RS allI RS prem] 1);
53e09e592278 removal of batch style, and tidying
paulson
parents: 3836
diff changeset
    30
by (etac notE 1);
53e09e592278 removal of batch style, and tidying
paulson
parents: 3836
diff changeset
    31
by (etac exI 1) ;
53e09e592278 removal of batch style, and tidying
paulson
parents: 3836
diff changeset
    32
qed "exCI";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    33
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    34
val excluded_middle = prove_goal FOLP.thy "?p : ~P | P"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    35
 (fn _=> [ rtac disjCI 1, assume_tac 1 ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    36
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    37
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    38
(*** Special elimination rules *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    39
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    40
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    41
(*Classical implies (-->) elimination. *)
9263
53e09e592278 removal of batch style, and tidying
paulson
parents: 3836
diff changeset
    42
val major::prems= goal FOLP.thy 
53e09e592278 removal of batch style, and tidying
paulson
parents: 3836
diff changeset
    43
    "[| p:P-->Q;  !!x. x:~P ==> f(x):R;  !!y. y:Q ==> g(y):R |] ==> ?p : R";
53e09e592278 removal of batch style, and tidying
paulson
parents: 3836
diff changeset
    44
by (resolve_tac [excluded_middle RS disjE] 1);
53e09e592278 removal of batch style, and tidying
paulson
parents: 3836
diff changeset
    45
by (DEPTH_SOLVE (ares_tac (prems@[major RS mp]) 1)) ;
53e09e592278 removal of batch style, and tidying
paulson
parents: 3836
diff changeset
    46
qed "impCE";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    47
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    48
(*Double negation law*)
9263
53e09e592278 removal of batch style, and tidying
paulson
parents: 3836
diff changeset
    49
Goal "p:~~P ==> ?p : P";
53e09e592278 removal of batch style, and tidying
paulson
parents: 3836
diff changeset
    50
by (rtac classical 1);
53e09e592278 removal of batch style, and tidying
paulson
parents: 3836
diff changeset
    51
by (etac notE 1);
53e09e592278 removal of batch style, and tidying
paulson
parents: 3836
diff changeset
    52
by (assume_tac 1);
53e09e592278 removal of batch style, and tidying
paulson
parents: 3836
diff changeset
    53
qed "notnotD";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    54
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    55
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    56
(*** Tactics for implication and contradiction ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    57
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    58
(*Classical <-> elimination.  Proof substitutes P=Q in 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    59
    ~P ==> ~Q    and    P ==> Q  *)
9263
53e09e592278 removal of batch style, and tidying
paulson
parents: 3836
diff changeset
    60
val prems = goalw FOLP.thy [iff_def]
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    61
    "[| p:P<->Q; !!x y.[| x:P; y:Q |] ==> f(x,y):R;  \
9263
53e09e592278 removal of batch style, and tidying
paulson
parents: 3836
diff changeset
    62
\                !!x y.[| x:~P; y:~Q |] ==> g(x,y):R |] ==> ?p : R";
53e09e592278 removal of batch style, and tidying
paulson
parents: 3836
diff changeset
    63
by (rtac conjE 1);
53e09e592278 removal of batch style, and tidying
paulson
parents: 3836
diff changeset
    64
by (REPEAT (DEPTH_SOLVE_1 (etac impCE 1
53e09e592278 removal of batch style, and tidying
paulson
parents: 3836
diff changeset
    65
               ORELSE  mp_tac 1  ORELSE  ares_tac prems 1))) ;
53e09e592278 removal of batch style, and tidying
paulson
parents: 3836
diff changeset
    66
qed "iffCE";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    67
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    68
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    69
(*Should be used as swap since ~P becomes redundant*)
9263
53e09e592278 removal of batch style, and tidying
paulson
parents: 3836
diff changeset
    70
val major::prems= goal FOLP.thy 
53e09e592278 removal of batch style, and tidying
paulson
parents: 3836
diff changeset
    71
   "p:~P ==> (!!x. x:~Q ==> f(x):P) ==> ?p : Q";
53e09e592278 removal of batch style, and tidying
paulson
parents: 3836
diff changeset
    72
by (rtac classical 1);
53e09e592278 removal of batch style, and tidying
paulson
parents: 3836
diff changeset
    73
by (rtac (major RS notE) 1);
53e09e592278 removal of batch style, and tidying
paulson
parents: 3836
diff changeset
    74
by (REPEAT (ares_tac prems 1)) ;
53e09e592278 removal of batch style, and tidying
paulson
parents: 3836
diff changeset
    75
qed "swap";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    76