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;
wenzelm@17481
     1
(*  Title:      LK/LK.ML
paulson@2073
     2
    ID:         $Id$
paulson@2073
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@2073
     4
    Copyright   1993  University of Cambridge
paulson@2073
     5
paulson@7094
     6
Axiom to express monotonicity (a variant of the deduction theorem).  Makes the
paulson@7094
     7
link between |- and ==>, needed for instance to prove imp_cong.
paulson@2073
     8
paulson@7117
     9
Axiom left_cong allows the simplifier to use left-side formulas.  Ideally it
paulson@7117
    10
should be derived from lower-level axioms.
paulson@7117
    11
paulson@7094
    12
CANNOT be added to LK0.thy because modal logic is built upon it, and
paulson@7094
    13
various modal rules would become inconsistent.
paulson@2073
    14
*)
paulson@2073
    15
wenzelm@17481
    16
theory LK
wenzelm@17481
    17
imports LK0
wenzelm@17481
    18
uses ("simpdata.ML")
wenzelm@17481
    19
begin
paulson@2073
    20
wenzelm@17481
    21
axioms
wenzelm@17481
    22
wenzelm@17481
    23
  monotonic:  "($H |- P ==> $H |- Q) ==> $H, P |- Q"
paulson@2073
    24
wenzelm@17481
    25
  left_cong:  "[| P == P';  |- P' ==> ($H |- $F) == ($H' |- $F') |]
wenzelm@17481
    26
               ==> (P, $H |- $F) == (P', $H' |- $F')"
paulson@2073
    27
wenzelm@17481
    28
ML {* use_legacy_bindings (the_context ()) *}
wenzelm@17481
    29
wenzelm@17481
    30
use "simpdata.ML"
wenzelm@17481
    31
paulson@2073
    32
end