src/Sequents/LK.thy
changeset 7094 6f18ae72a90e
parent 6456 23602e214ebf
child 7117 37eccadf6b8a
equal deleted inserted replaced
7093:b2ee0e5d1a7f 7094:6f18ae72a90e
     1 (*  Title:      LK/lk.thy
     1 (*  Title:      LK/LK
     2     ID:         $Id$
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1993  University of Cambridge
     4     Copyright   1993  University of Cambridge
     5 
     5 
     6 Classical First-Order Sequent Calculus
     6 Axiom to express monotonicity (a variant of the deduction theorem).  Makes the
       
     7 link between |- and ==>, needed for instance to prove imp_cong.
     7 
     8 
     8 There may be printing problems if a seqent is in expanded normal form
     9 CANNOT be added to LK0.thy because modal logic is built upon it, and
     9 	(eta-expanded, beta-contracted)
    10 various modal rules would become inconsistent.
    10 *)
    11 *)
    11 
    12 
    12 LK = Sequents +
    13 LK = LK0 +
    13 
       
    14 classes
       
    15   term < logic
       
    16 
       
    17 default
       
    18   term
       
    19 
       
    20 consts
       
    21 
       
    22  Trueprop	:: "two_seqi"
       
    23  "@Trueprop"	:: "two_seqe" ("((_)/ |- (_))" [6,6] 5)
       
    24 
       
    25 
       
    26   True,False   :: o
       
    27   "="          :: ['a,'a] => o       (infixl 50)
       
    28   Not          :: o => o             ("~ _" [40] 40)
       
    29   "&"          :: [o,o] => o         (infixr 35)
       
    30   "|"          :: [o,o] => o         (infixr 30)
       
    31   "-->","<->"  :: [o,o] => o         (infixr 25)
       
    32   The          :: ('a => o) => 'a    (binder "THE " 10)
       
    33   All          :: ('a => o) => o     (binder "ALL " 10)
       
    34   Ex           :: ('a => o) => o     (binder "EX " 10)
       
    35 
    14 
    36 rules
    15 rules
    37   (*Structural rules*)
       
    38 
    16 
    39   basic "$H, P, $G |- $E, P, $F"
    17   monotonic  "($H |- P ==> $H |- Q) ==> $H, P |- Q"
    40 
    18 
    41   thinR "$H |- $E, $F ==> $H |- $E, P, $F"
       
    42   thinL "$H, $G |- $E ==> $H, P, $G |- $E"
       
    43 
       
    44   cut   "[| $H |- $E, P;  $H, P |- $E |] ==> $H |- $E"
       
    45 
       
    46   (*Propositional rules*)
       
    47 
       
    48   conjR "[| $H|- $E, P, $F;  $H|- $E, Q, $F |] ==> $H|- $E, P&Q, $F"
       
    49   conjL "$H, P, Q, $G |- $E ==> $H, P & Q, $G |- $E"
       
    50 
       
    51   disjR "$H |- $E, P, Q, $F ==> $H |- $E, P|Q, $F"
       
    52   disjL "[| $H, P, $G |- $E;  $H, Q, $G |- $E |] ==> $H, P|Q, $G |- $E"
       
    53 
       
    54   impR  "$H, P |- $E, Q, $F ==> $H |- $E, P-->Q, $F"
       
    55   impL  "[| $H,$G |- $E,P;  $H, Q, $G |- $E |] ==> $H, P-->Q, $G |- $E"
       
    56 
       
    57   notR  "$H, P |- $E, $F ==> $H |- $E, ~P, $F"
       
    58   notL  "$H, $G |- $E, P ==> $H, ~P, $G |- $E"
       
    59 
       
    60   FalseL "$H, False, $G |- $E"
       
    61 
       
    62   True_def "True == False-->False"
       
    63   iff_def  "P<->Q == (P-->Q) & (Q-->P)"
       
    64 
       
    65   (*Quantifiers*)
       
    66 
       
    67   allR  "(!!x.$H |- $E, P(x), $F) ==> $H |- $E, ALL x. P(x), $F"
       
    68   allL  "$H, P(x), $G, ALL x. P(x) |- $E ==> $H, ALL x. P(x), $G |- $E"
       
    69 
       
    70   exR   "$H |- $E, P(x), $F, EX x. P(x) ==> $H |- $E, EX x. P(x), $F"
       
    71   exL   "(!!x.$H, P(x), $G |- $E) ==> $H, EX x. P(x), $G |- $E"
       
    72 
       
    73   (*Equality*)
       
    74 
       
    75   refl  "$H |- $E, a=a, $F"
       
    76   sym   "$H |- $E, a=b, $F ==> $H |- $E, b=a, $F"
       
    77   trans "[| $H|- $E, a=b, $F;  $H|- $E, b=c, $F |] ==> $H|- $E, a=c, $F"
       
    78 
       
    79 
       
    80   (*Descriptions*)
       
    81 
       
    82   The "[| $H |- $E, P(a), $F;  !!x.$H, P(x) |- $E, x=a, $F |] ==> 
       
    83           $H |- $E, P(THE x. P(x)), $F"
       
    84 end
    19 end
    85 
       
    86   ML
       
    87 
       
    88 val parse_translation = [("@Trueprop",Sequents.two_seq_tr "Trueprop")];
       
    89 val print_translation = [("Trueprop",Sequents.two_seq_tr' "@Trueprop")];