isabelle: src/Sequents/LK.thy@f84cf8e9cad8 (annotated)

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

author	wenzelm
	Tue, 21 Nov 2006 00:07:05 +0100
changeset 21428	f84cf8e9cad8
parent 17481	75166ebb619b
child 27149	123377499a8e
permissions	-rw-r--r--