src/LK/LK.thy
changeset 1474 3f7d67927fe2
parent 1304 976f9e19a828
child 1863 9402e633fe53
     1.1 --- a/src/LK/LK.thy	Mon Feb 05 13:44:28 1996 +0100
     1.2 +++ b/src/LK/LK.thy	Mon Feb 05 14:44:09 1996 +0100
     1.3 @@ -1,6 +1,6 @@
     1.4 -(*  Title: 	LK/lk.thy
     1.5 +(*  Title:      LK/lk.thy
     1.6      ID:         $Id$
     1.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     1.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.9      Copyright   1993  University of Cambridge
    1.10  
    1.11  Classical First-Order Sequent Calculus
    1.12 @@ -19,51 +19,51 @@
    1.13   o :: logic
    1.14  
    1.15  consts
    1.16 - True,False	:: "o"
    1.17 - "="		:: "['a,'a] => o"	(infixl 50)
    1.18 - "Not"		:: "o => o"		("~ _" [40] 40)
    1.19 - "&"		:: "[o,o] => o"		(infixr 35)
    1.20 - "|"		:: "[o,o] => o"		(infixr 30)
    1.21 - "-->","<->"	:: "[o,o] => o"		(infixr 25)
    1.22 - The		:: "('a => o) => 'a"	(binder "THE " 10)
    1.23 - All		:: "('a => o) => o"	(binder "ALL " 10)
    1.24 - Ex		:: "('a => o) => o"	(binder "EX " 10)
    1.25 + True,False     :: "o"
    1.26 + "="            :: "['a,'a] => o"       (infixl 50)
    1.27 + "Not"          :: "o => o"             ("~ _" [40] 40)
    1.28 + "&"            :: "[o,o] => o"         (infixr 35)
    1.29 + "|"            :: "[o,o] => o"         (infixr 30)
    1.30 + "-->","<->"    :: "[o,o] => o"         (infixr 25)
    1.31 + The            :: "('a => o) => 'a"    (binder "THE " 10)
    1.32 + All            :: "('a => o) => o"     (binder "ALL " 10)
    1.33 + Ex             :: "('a => o) => o"     (binder "EX " 10)
    1.34  
    1.35   (*Representation of sequents*)
    1.36 - Trueprop	:: "[sobj=>sobj,sobj=>sobj] => prop"
    1.37 - Seqof		:: "o => sobj=>sobj"
    1.38 - "@Trueprop"	:: "[sequence,sequence] => prop" ("((_)/ |- (_))" [6,6] 5)
    1.39 - "@MtSeq"	:: "sequence"				("" [] 1000)
    1.40 - "@NmtSeq"	:: "[seqobj,seqcont] => sequence"	("__" [] 1000)
    1.41 - "@MtSeqCont"	:: "seqcont"				("" [] 1000)
    1.42 - "@SeqCont"	:: "[seqobj,seqcont] => seqcont"	(",/ __" [] 1000)
    1.43 - ""		:: "o => seqobj"			("_" [] 1000)
    1.44 - "@SeqId"	:: "id => seqobj"			("$_" [] 1000)
    1.45 - "@SeqVar"	:: "var => seqobj"			("$_")
    1.46 + Trueprop       :: "[sobj=>sobj,sobj=>sobj] => prop"
    1.47 + Seqof          :: "o => sobj=>sobj"
    1.48 + "@Trueprop"    :: "[sequence,sequence] => prop" ("((_)/ |- (_))" [6,6] 5)
    1.49 + "@MtSeq"       :: "sequence"                           ("" [] 1000)
    1.50 + "@NmtSeq"      :: "[seqobj,seqcont] => sequence"       ("__" [] 1000)
    1.51 + "@MtSeqCont"   :: "seqcont"                            ("" [] 1000)
    1.52 + "@SeqCont"     :: "[seqobj,seqcont] => seqcont"        (",/ __" [] 1000)
    1.53 + ""             :: "o => seqobj"                        ("_" [] 1000)
    1.54 + "@SeqId"       :: "id => seqobj"                       ("$_" [] 1000)
    1.55 + "@SeqVar"      :: "var => seqobj"                      ("$_")
    1.56  
    1.57  rules
    1.58    (*Structural rules*)
    1.59  
    1.60 -  basic	"$H, P, $G |- $E, P, $F"
    1.61 +  basic "$H, P, $G |- $E, P, $F"
    1.62  
    1.63 -  thinR	"$H |- $E, $F ==> $H |- $E, P, $F"
    1.64 -  thinL	"$H, $G |- $E ==> $H, P, $G |- $E"
    1.65 +  thinR "$H |- $E, $F ==> $H |- $E, P, $F"
    1.66 +  thinL "$H, $G |- $E ==> $H, P, $G |- $E"
    1.67  
    1.68 -  cut	"[| $H |- $E, P;  $H, P |- $E |] ==> $H |- $E"
    1.69 +  cut   "[| $H |- $E, P;  $H, P |- $E |] ==> $H |- $E"
    1.70  
    1.71    (*Propositional rules*)
    1.72  
    1.73 -  conjR	"[| $H|- $E, P, $F;  $H|- $E, Q, $F |] ==> $H|- $E, P&Q, $F"
    1.74 -  conjL	"$H, P, Q, $G |- $E ==> $H, P & Q, $G |- $E"
    1.75 +  conjR "[| $H|- $E, P, $F;  $H|- $E, Q, $F |] ==> $H|- $E, P&Q, $F"
    1.76 +  conjL "$H, P, Q, $G |- $E ==> $H, P & Q, $G |- $E"
    1.77  
    1.78 -  disjR	"$H |- $E, P, Q, $F ==> $H |- $E, P|Q, $F"
    1.79 -  disjL	"[| $H, P, $G |- $E;  $H, Q, $G |- $E |] ==> $H, P|Q, $G |- $E"
    1.80 +  disjR "$H |- $E, P, Q, $F ==> $H |- $E, P|Q, $F"
    1.81 +  disjL "[| $H, P, $G |- $E;  $H, Q, $G |- $E |] ==> $H, P|Q, $G |- $E"
    1.82  
    1.83 -  impR	"$H, P |- $E, Q, $F ==> $H |- $E, P-->Q, $F"
    1.84 -  impL	"[| $H,$G |- $E,P;  $H, Q, $G |- $E |] ==> $H, P-->Q, $G |- $E"
    1.85 +  impR  "$H, P |- $E, Q, $F ==> $H |- $E, P-->Q, $F"
    1.86 +  impL  "[| $H,$G |- $E,P;  $H, Q, $G |- $E |] ==> $H, P-->Q, $G |- $E"
    1.87  
    1.88 -  notR	"$H, P |- $E, $F ==> $H |- $E, ~P, $F"
    1.89 -  notL	"$H, $G |- $E, P ==> $H, ~P, $G |- $E"
    1.90 +  notR  "$H, P |- $E, $F ==> $H |- $E, ~P, $F"
    1.91 +  notL  "$H, $G |- $E, P ==> $H, ~P, $G |- $E"
    1.92  
    1.93    FalseL "$H, False, $G |- $E"
    1.94  
    1.95 @@ -72,15 +72,15 @@
    1.96  
    1.97    (*Quantifiers*)
    1.98  
    1.99 -  allR	"(!!x.$H |- $E, P(x), $F) ==> $H |- $E, ALL x.P(x), $F"
   1.100 -  allL	"$H, P(x), $G, ALL x.P(x) |- $E ==> $H, ALL x.P(x), $G |- $E"
   1.101 +  allR  "(!!x.$H |- $E, P(x), $F) ==> $H |- $E, ALL x.P(x), $F"
   1.102 +  allL  "$H, P(x), $G, ALL x.P(x) |- $E ==> $H, ALL x.P(x), $G |- $E"
   1.103  
   1.104 -  exR	"$H |- $E, P(x), $F, EX x.P(x) ==> $H |- $E, EX x.P(x), $F"
   1.105 -  exL	"(!!x.$H, P(x), $G |- $E) ==> $H, EX x.P(x), $G |- $E"
   1.106 +  exR   "$H |- $E, P(x), $F, EX x.P(x) ==> $H |- $E, EX x.P(x), $F"
   1.107 +  exL   "(!!x.$H, P(x), $G |- $E) ==> $H, EX x.P(x), $G |- $E"
   1.108  
   1.109    (*Equality*)
   1.110  
   1.111 -  refl	"$H |- $E, a=a, $F"
   1.112 +  refl  "$H |- $E, a=a, $F"
   1.113    sym   "$H |- $E, a=b, $F ==> $H |- $E, b=a, $F"
   1.114    trans "[| $H|- $E, a=b, $F;  $H|- $E, b=c, $F |] ==> $H|- $E, a=c, $F"
   1.115