isabelle: src/Sequents/S4.thy@0531e5abf680 (annotated)

17481 75166ebb619b converted to Isar theory format; wenzelm parents: 2073 diff changeset	1	(* Title: Modal/S4.thy
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: Martin Coen
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala paulson parents: diff changeset	4	Copyright 1991 University of Cambridge
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala paulson parents: diff changeset	5	*)
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala paulson parents: diff changeset	6
17481 75166ebb619b converted to Isar theory format; wenzelm parents: 2073 diff changeset	7	theory S4
75166ebb619b converted to Isar theory format; wenzelm parents: 2073 diff changeset	8	imports Modal0
75166ebb619b converted to Isar theory format; wenzelm parents: 2073 diff changeset	9	begin
75166ebb619b converted to Isar theory format; wenzelm parents: 2073 diff changeset	10
75166ebb619b converted to Isar theory format; wenzelm parents: 2073 diff changeset	11	axioms
2073 fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala paulson parents: diff changeset	12	(* Definition of the star operation using a set of Horn clauses *)
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala paulson parents: diff changeset	13	(* For system S4: gamma * == {[]P \| []P : gamma} *)
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala paulson parents: diff changeset	14	(* delta * == {<>P \| <>P : delta} *)
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala paulson parents: diff changeset	15
17481 75166ebb619b converted to Isar theory format; wenzelm parents: 2073 diff changeset	16	lstar0: "\|L>"
75166ebb619b converted to Isar theory format; wenzelm parents: 2073 diff changeset	17	lstar1: "$G \|L> $H ==> []P, $G \|L> []P, $H"
75166ebb619b converted to Isar theory format; wenzelm parents: 2073 diff changeset	18	lstar2: "$G \|L> $H ==> P, $G \|L> $H"
75166ebb619b converted to Isar theory format; wenzelm parents: 2073 diff changeset	19	rstar0: "\|R>"
75166ebb619b converted to Isar theory format; wenzelm parents: 2073 diff changeset	20	rstar1: "$G \|R> $H ==> <>P, $G \|R> <>P, $H"
75166ebb619b converted to Isar theory format; wenzelm parents: 2073 diff changeset	21	rstar2: "$G \|R> $H ==> P, $G \|R> $H"
2073 fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala paulson parents: diff changeset	22
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala paulson parents: diff changeset	23	(* Rules for [] and <> *)
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala paulson parents: diff changeset	24
17481 75166ebb619b converted to Isar theory format; wenzelm parents: 2073 diff changeset	25	boxR:
75166ebb619b converted to Isar theory format; wenzelm parents: 2073 diff changeset	26	"[\| $E \|L> $E'; $F \|R> $F'; $G \|R> $G';
2073 fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala paulson parents: diff changeset	27	$E' \|- $F', P, $G'\|] ==> $E \|- $F, []P, $G"
17481 75166ebb619b converted to Isar theory format; wenzelm parents: 2073 diff changeset	28	boxL: "$E,P,$F,[]P \|- $G ==> $E, []P, $F \|- $G"
2073 fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala paulson parents: diff changeset	29
17481 75166ebb619b converted to Isar theory format; wenzelm parents: 2073 diff changeset	30	diaR: "$E \|- $F,P,$G,<>P ==> $E \|- $F, <>P, $G"
75166ebb619b converted to Isar theory format; wenzelm parents: 2073 diff changeset	31	diaL:
75166ebb619b converted to Isar theory format; wenzelm parents: 2073 diff changeset	32	"[\| $E \|L> $E'; $F \|L> $F'; $G \|R> $G';
2073 fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala paulson parents: diff changeset	33	$E', P, $F' \|- $G'\|] ==> $E, <>P, $F \|- $G"
17481 75166ebb619b converted to Isar theory format; wenzelm parents: 2073 diff changeset	34
75166ebb619b converted to Isar theory format; wenzelm parents: 2073 diff changeset	35	ML {* use_legacy_bindings (the_context ()) *}
75166ebb619b converted to Isar theory format; wenzelm parents: 2073 diff changeset	36
2073 fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala paulson parents: diff changeset	37	end

author	wenzelm
	Mon, 01 May 2006 17:05:11 +0200
changeset 19523	0531e5abf680
parent 17481	75166ebb619b
child 21426	87ac12bed1ab
permissions	-rw-r--r--