src/Sequents/LK.thy
 author wenzelm Sun Sep 18 15:20:08 2005 +0200 (2005-09-18) changeset 17481 75166ebb619b parent 7117 37eccadf6b8a child 21428 f84cf8e9cad8 permissions -rw-r--r--
converted to Isar theory format;
```     1 (*  Title:      LK/LK.ML
```
```     2     ID:         \$Id\$
```
```     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
```
```     4     Copyright   1993  University of Cambridge
```
```     5
```
```     6 Axiom to express monotonicity (a variant of the deduction theorem).  Makes the
```
```     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.
```
```    11
```
```    12 CANNOT be added to LK0.thy because modal logic is built upon it, and
```
```    13 various modal rules would become inconsistent.
```
```    14 *)
```
```    15
```
```    16 theory LK
```
```    17 imports LK0
```
```    18 uses ("simpdata.ML")
```
```    19 begin
```
```    20
```
```    21 axioms
```
```    22
```
```    23   monotonic:  "(\$H |- P ==> \$H |- Q) ==> \$H, P |- Q"
```
```    24
```
```    25   left_cong:  "[| P == P';  |- P' ==> (\$H |- \$F) == (\$H' |- \$F') |]
```
```    26                ==> (P, \$H |- \$F) == (P', \$H' |- \$F')"
```
```    27
```
```    28 ML {* use_legacy_bindings (the_context ()) *}
```
```    29
```
```    30 use "simpdata.ML"
```
```    31
```
```    32 end
```