src/Sequents/LK.thy
author paulson
Mon Dec 07 18:26:25 1998 +0100 (1998-12-07)
changeset 6019 0e55c2fb2ebb
parent 3839 56544d061e1d
child 6456 23602e214ebf
permissions -rw-r--r--
tidying
     1 (*  Title:      LK/lk.thy
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1993  University of Cambridge
     5 
     6 Classical First-Order Sequent Calculus
     7 
     8 There may be printing problems if a seqent is in expanded normal form
     9 	(eta-expanded, beta-contracted)
    10 *)
    11 
    12 LK = Sequents +
    13 
    14 
    15 consts
    16 
    17  Trueprop	:: "two_seqi"
    18  "@Trueprop"	:: "two_seqe" ("((_)/ |- (_))" [6,6] 5)
    19 
    20 
    21   True,False   :: o
    22   "="          :: ['a,'a] => o       (infixl 50)
    23   Not          :: o => o             ("~ _" [40] 40)
    24   "&"          :: [o,o] => o         (infixr 35)
    25   "|"          :: [o,o] => o         (infixr 30)
    26   "-->","<->"  :: [o,o] => o         (infixr 25)
    27   The          :: ('a => o) => 'a    (binder "THE " 10)
    28   All          :: ('a => o) => o     (binder "ALL " 10)
    29   Ex           :: ('a => o) => o     (binder "EX " 10)
    30 
    31 rules
    32   (*Structural rules*)
    33 
    34   basic "$H, P, $G |- $E, P, $F"
    35 
    36   thinR "$H |- $E, $F ==> $H |- $E, P, $F"
    37   thinL "$H, $G |- $E ==> $H, P, $G |- $E"
    38 
    39   cut   "[| $H |- $E, P;  $H, P |- $E |] ==> $H |- $E"
    40 
    41   (*Propositional rules*)
    42 
    43   conjR "[| $H|- $E, P, $F;  $H|- $E, Q, $F |] ==> $H|- $E, P&Q, $F"
    44   conjL "$H, P, Q, $G |- $E ==> $H, P & Q, $G |- $E"
    45 
    46   disjR "$H |- $E, P, Q, $F ==> $H |- $E, P|Q, $F"
    47   disjL "[| $H, P, $G |- $E;  $H, Q, $G |- $E |] ==> $H, P|Q, $G |- $E"
    48 
    49   impR  "$H, P |- $E, Q, $F ==> $H |- $E, P-->Q, $F"
    50   impL  "[| $H,$G |- $E,P;  $H, Q, $G |- $E |] ==> $H, P-->Q, $G |- $E"
    51 
    52   notR  "$H, P |- $E, $F ==> $H |- $E, ~P, $F"
    53   notL  "$H, $G |- $E, P ==> $H, ~P, $G |- $E"
    54 
    55   FalseL "$H, False, $G |- $E"
    56 
    57   True_def "True == False-->False"
    58   iff_def  "P<->Q == (P-->Q) & (Q-->P)"
    59 
    60   (*Quantifiers*)
    61 
    62   allR  "(!!x.$H |- $E, P(x), $F) ==> $H |- $E, ALL x. P(x), $F"
    63   allL  "$H, P(x), $G, ALL x. P(x) |- $E ==> $H, ALL x. P(x), $G |- $E"
    64 
    65   exR   "$H |- $E, P(x), $F, EX x. P(x) ==> $H |- $E, EX x. P(x), $F"
    66   exL   "(!!x.$H, P(x), $G |- $E) ==> $H, EX x. P(x), $G |- $E"
    67 
    68   (*Equality*)
    69 
    70   refl  "$H |- $E, a=a, $F"
    71   sym   "$H |- $E, a=b, $F ==> $H |- $E, b=a, $F"
    72   trans "[| $H|- $E, a=b, $F;  $H|- $E, b=c, $F |] ==> $H|- $E, a=c, $F"
    73 
    74 
    75   (*Descriptions*)
    76 
    77   The "[| $H |- $E, P(a), $F;  !!x.$H, P(x) |- $E, x=a, $F |] ==> 
    78           $H |- $E, P(THE x. P(x)), $F"
    79 end
    80 
    81   ML
    82 
    83 val parse_translation = [("@Trueprop",Sequents.two_seq_tr "Trueprop")];
    84 val print_translation = [("Trueprop",Sequents.two_seq_tr' "@Trueprop")];