src/Sequents/LK.thy
 changeset 7094 6f18ae72a90e parent 6456 23602e214ebf child 7117 37eccadf6b8a
equal 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`
`    38 `
`    16 `
`    39   basic "\$H, P, \$G |- \$E, P, \$F"`
`    17   monotonic  "(\$H |- P ==> \$H |- Q) ==> \$H, P |- Q"`
`    40 `
`    18 `
`    84 end`
`    19 end`