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