src/Sequents/LK.thy
 changeset 7117 37eccadf6b8a parent 7094 6f18ae72a90e child 17481 75166ebb619b
equal inserted replaced
7116:8c1caac3e54e 7117:37eccadf6b8a
`     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 Axiom to express monotonicity (a variant of the deduction theorem).  Makes the`
`     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 link between |- and ==>, needed for instance to prove imp_cong.`
`       `
`     8 `
`       `
`     9 Axiom left_cong allows the simplifier to use left-side formulas.  Ideally it`
`       `
`    10 should be derived from lower-level axioms.`
`     8 `
`    11 `
`     9 CANNOT be added to LK0.thy because modal logic is built upon it, and`
`    12 CANNOT be added to LK0.thy because modal logic is built upon it, and`
`    10 various modal rules would become inconsistent.`
`    13 various modal rules would become inconsistent.`
`    11 *)`
`    14 *)`
`    12 `
`    15 `
`    14 `
`    17 `
`    15 rules`
`    18 rules`
`    16 `
`    19 `
`    17   monotonic  "(\$H |- P ==> \$H |- Q) ==> \$H, P |- Q"`
`    20   monotonic  "(\$H |- P ==> \$H |- Q) ==> \$H, P |- Q"`
`    18 `
`    21 `
`       `
`    22   left_cong  "[| P == P';  |- P' ==> (\$H |- \$F) == (\$H' |- \$F') |] `
`       `
`    23               ==> (P, \$H |- \$F) == (P', \$H' |- \$F')"`
`    19 end`
`    24 end`