src/Sequents/LK.thy
changeset 7117 37eccadf6b8a
parent 7094 6f18ae72a90e
child 17481 75166ebb619b
equal deleted 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