src/Sequents/LK.thy
author haftmann
Tue, 10 Jul 2007 17:30:50 +0200
changeset 23709 fd31da8f752a
parent 21428 f84cf8e9cad8
child 27149 123377499a8e
permissions -rw-r--r--
moved lfp_induct2 here
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
17481
75166ebb619b converted to Isar theory format;
wenzelm
parents: 7117
diff changeset
     1
(*  Title:      LK/LK.ML
2073
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
     2
    ID:         $Id$
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
     4
    Copyright   1993  University of Cambridge
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
     5
7094
6f18ae72a90e a new theory containing just an axiom needed to derive imp_cong
paulson
parents: 6456
diff changeset
     6
Axiom to express monotonicity (a variant of the deduction theorem).  Makes the
6f18ae72a90e a new theory containing just an axiom needed to derive imp_cong
paulson
parents: 6456
diff changeset
     7
link between |- and ==>, needed for instance to prove imp_cong.
2073
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
     8
7117
37eccadf6b8a congruence rule for |-
paulson
parents: 7094
diff changeset
     9
Axiom left_cong allows the simplifier to use left-side formulas.  Ideally it
37eccadf6b8a congruence rule for |-
paulson
parents: 7094
diff changeset
    10
should be derived from lower-level axioms.
37eccadf6b8a congruence rule for |-
paulson
parents: 7094
diff changeset
    11
7094
6f18ae72a90e a new theory containing just an axiom needed to derive imp_cong
paulson
parents: 6456
diff changeset
    12
CANNOT be added to LK0.thy because modal logic is built upon it, and
6f18ae72a90e a new theory containing just an axiom needed to derive imp_cong
paulson
parents: 6456
diff changeset
    13
various modal rules would become inconsistent.
2073
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    14
*)
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    15
17481
75166ebb619b converted to Isar theory format;
wenzelm
parents: 7117
diff changeset
    16
theory LK
75166ebb619b converted to Isar theory format;
wenzelm
parents: 7117
diff changeset
    17
imports LK0
75166ebb619b converted to Isar theory format;
wenzelm
parents: 7117
diff changeset
    18
uses ("simpdata.ML")
75166ebb619b converted to Isar theory format;
wenzelm
parents: 7117
diff changeset
    19
begin
2073
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    20
17481
75166ebb619b converted to Isar theory format;
wenzelm
parents: 7117
diff changeset
    21
axioms
75166ebb619b converted to Isar theory format;
wenzelm
parents: 7117
diff changeset
    22
75166ebb619b converted to Isar theory format;
wenzelm
parents: 7117
diff changeset
    23
  monotonic:  "($H |- P ==> $H |- Q) ==> $H, P |- Q"
2073
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    24
17481
75166ebb619b converted to Isar theory format;
wenzelm
parents: 7117
diff changeset
    25
  left_cong:  "[| P == P';  |- P' ==> ($H |- $F) == ($H' |- $F') |]
75166ebb619b converted to Isar theory format;
wenzelm
parents: 7117
diff changeset
    26
               ==> (P, $H |- $F) == (P', $H' |- $F')"
2073
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    27
17481
75166ebb619b converted to Isar theory format;
wenzelm
parents: 7117
diff changeset
    28
use "simpdata.ML"
75166ebb619b converted to Isar theory format;
wenzelm
parents: 7117
diff changeset
    29
2073
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    30
end