src/Sequents/LK.thy
author wenzelm
Thu Dec 07 00:42:04 2006 +0100 (2006-12-07)
changeset 21687 f689f729afab
parent 21428 f84cf8e9cad8
child 27149 123377499a8e
permissions -rw-r--r--
reorganized structure Goal vs. Tactic;
     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 use "simpdata.ML"
    29 
    30 end