src/Sequents/LK.ML
author paulson
Mon Dec 07 18:26:25 1998 +0100 (1998-12-07)
changeset 6019 0e55c2fb2ebb
parent 3839 56544d061e1d
permissions -rw-r--r--
tidying
     1 (*  Title:      LK/LK.ML
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1992  University of Cambridge
     5 
     6 Tactics and lemmas for lk.thy (thanks also to Philippe de Groote)  
     7 *)
     8 
     9 open LK;
    10 
    11 (*Higher precedence than := facilitates use of references*)
    12 infix 4 add_safes add_unsafes;
    13 
    14 (*Cut and thin, replacing the right-side formula*)
    15 fun cutR_tac (sP: string) i = 
    16     res_inst_tac [ ("P",sP) ] cut i  THEN  rtac thinR i;
    17 
    18 (*Cut and thin, replacing the left-side formula*)
    19 fun cutL_tac (sP: string) i = 
    20     res_inst_tac [ ("P",sP) ] cut i  THEN  rtac thinL (i+1);
    21 
    22 
    23 (** If-and-only-if rules **)
    24 qed_goalw "iffR" LK.thy [iff_def]
    25     "[| $H,P |- $E,Q,$F;  $H,Q |- $E,P,$F |] ==> $H |- $E, P <-> Q, $F"
    26  (fn prems=> [ (REPEAT (resolve_tac (prems@[conjR,impR]) 1)) ]);
    27 
    28 qed_goalw "iffL" LK.thy [iff_def]
    29    "[| $H,$G |- $E,P,Q;  $H,Q,P,$G |- $E |] ==> $H, P <-> Q, $G |- $E"
    30  (fn prems=> [ (REPEAT (resolve_tac (prems@[conjL,impL,basic]) 1)) ]);
    31 
    32 qed_goalw "TrueR" LK.thy [True_def]
    33     "$H |- $E, True, $F"
    34  (fn _=> [ rtac impR 1, rtac basic 1 ]);
    35 
    36 
    37 (** Weakened quantifier rules.  Incomplete, they let the search terminate.**)
    38 
    39 qed_goal "allL_thin" LK.thy 
    40     "$H, P(x), $G |- $E ==> $H, ALL x. P(x), $G |- $E"
    41  (fn prems=> [ (rtac allL 1), (rtac thinL 1), (resolve_tac prems 1) ]);
    42 
    43 qed_goal "exR_thin" LK.thy 
    44     "$H |- $E, P(x), $F ==> $H |- $E, EX x. P(x), $F"
    45  (fn prems=> [ (rtac exR 1), (rtac thinR 1), (resolve_tac prems 1) ]);
    46 
    47 (* Symmetry of equality in hypotheses *)
    48 qed_goal "symL" LK.thy 
    49     "$H, $G, B = A |- $E ==> $H, A = B, $G |- $E" 
    50  (fn prems=>
    51   [ (rtac cut 1),
    52     (rtac thinL 2),
    53     (resolve_tac prems 2),
    54     (resolve_tac [basic RS sym] 1) ]);
    55 
    56 
    57 
    58 
    59 (*The rules of LK*)
    60 val prop_pack = empty_pack add_safes 
    61                 [basic, refl, conjL, conjR, disjL, disjR, impL, impR, 
    62                  notL, notR, iffL, iffR];
    63 
    64 val LK_pack = prop_pack add_safes   [allR, exL] 
    65                         add_unsafes [allL_thin, exR_thin];
    66 
    67 val LK_dup_pack = prop_pack add_safes   [allR, exL] 
    68                             add_unsafes [allL, exR];
    69 
    70 
    71 
    72 (** Contraction.  Useful since some rules are not complete. **)
    73 
    74 qed_goal "conR" LK.thy 
    75     "$H |- $E, P, $F, P ==> $H |- $E, P, $F"
    76  (fn prems=>
    77   [ (rtac cut 1), (REPEAT (resolve_tac (prems@[basic]) 1)) ]);
    78 
    79 qed_goal "conL" LK.thy 
    80     "$H, P, $G, P |- $E ==> $H, P, $G |- $E"
    81  (fn prems=>
    82   [ (rtac cut 1), (REPEAT (resolve_tac (prems@[basic]) 1)) ]);