isabelle: src/Sequents/T.thy@db7c735e963d (annotated)

35762 af3ff2ba4c54 removed old CVS Ids; wenzelm parents: 30549 diff changeset	1	(* Title: Sequents/T.thy
2073 fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala paulson parents: diff changeset	2	Author: Martin Coen
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala paulson parents: diff changeset	3	Copyright 1991 University of Cambridge
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala paulson parents: diff changeset	4	*)
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala paulson parents: diff changeset	5
17481 75166ebb619b converted to Isar theory format; wenzelm parents: 2073 diff changeset	6	theory T
75166ebb619b converted to Isar theory format; wenzelm parents: 2073 diff changeset	7	imports Modal0
75166ebb619b converted to Isar theory format; wenzelm parents: 2073 diff changeset	8	begin
75166ebb619b converted to Isar theory format; wenzelm parents: 2073 diff changeset	9
51309 473303ef6e34 eliminated legacy 'axioms'; wenzelm parents: 42814 diff changeset	10	axiomatization where
2073 fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala paulson parents: diff changeset	11	(* 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	12	(* For system T: gamma * == {P \| []P : gamma} *)
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala paulson parents: diff changeset	13	(* delta * == {P \| <>P : delta} *)
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala paulson parents: diff changeset	14
51309 473303ef6e34 eliminated legacy 'axioms'; wenzelm parents: 42814 diff changeset	15	lstar0: "\|L>" and
473303ef6e34 eliminated legacy 'axioms'; wenzelm parents: 42814 diff changeset	16	lstar1: "$G \|L> $H ==> []P, $G \|L> P, $H" and
473303ef6e34 eliminated legacy 'axioms'; wenzelm parents: 42814 diff changeset	17	lstar2: "$G \|L> $H ==> P, $G \|L> $H" and
473303ef6e34 eliminated legacy 'axioms'; wenzelm parents: 42814 diff changeset	18	rstar0: "\|R>" and
473303ef6e34 eliminated legacy 'axioms'; wenzelm parents: 42814 diff changeset	19	rstar1: "$G \|R> $H ==> <>P, $G \|R> P, $H" and
473303ef6e34 eliminated legacy 'axioms'; wenzelm parents: 42814 diff changeset	20	rstar2: "$G \|R> $H ==> P, $G \|R> $H" and
2073 fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala paulson parents: diff changeset	21
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala paulson parents: diff changeset	22	(* Rules for [] and <> *)
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala paulson parents: diff changeset	23
17481 75166ebb619b converted to Isar theory format; wenzelm parents: 2073 diff changeset	24	boxR:
75166ebb619b converted to Isar theory format; wenzelm parents: 2073 diff changeset	25	"[\| $E \|L> $E'; $F \|R> $F'; $G \|R> $G';
51309 473303ef6e34 eliminated legacy 'axioms'; wenzelm parents: 42814 diff changeset	26	$E' \|- $F', P, $G'\|] ==> $E \|- $F, []P, $G" and
473303ef6e34 eliminated legacy 'axioms'; wenzelm parents: 42814 diff changeset	27	boxL: "$E, P, $F \|- $G ==> $E, []P, $F \|- $G" and
473303ef6e34 eliminated legacy 'axioms'; wenzelm parents: 42814 diff changeset	28	diaR: "$E \|- $F, P, $G ==> $E \|- $F, <>P, $G" and
17481 75166ebb619b converted to Isar theory format; wenzelm parents: 2073 diff changeset	29	diaL:
75166ebb619b converted to Isar theory format; wenzelm parents: 2073 diff changeset	30	"[\| $E \|L> $E'; $F \|L> $F'; $G \|R> $G';
2073 fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala paulson parents: diff changeset	31	$E', P, $F'\|- $G'\|] ==> $E, <>P, $F \|- $G"
17481 75166ebb619b converted to Isar theory format; wenzelm parents: 2073 diff changeset	32
21426 87ac12bed1ab converted legacy ML scripts; wenzelm parents: 17481 diff changeset	33	ML {*
87ac12bed1ab converted legacy ML scripts; wenzelm parents: 17481 diff changeset	34	structure T_Prover = Modal_ProverFun
87ac12bed1ab converted legacy ML scripts; wenzelm parents: 17481 diff changeset	35	(
39159 0dec18004e75 more antiquotations; wenzelm parents: 35762 diff changeset	36	val rewrite_rls = @{thms rewrite_rls}
0dec18004e75 more antiquotations; wenzelm parents: 35762 diff changeset	37	val safe_rls = @{thms safe_rls}
0dec18004e75 more antiquotations; wenzelm parents: 35762 diff changeset	38	val unsafe_rls = @{thms unsafe_rls} @ [@{thm boxR}, @{thm diaL}]
0dec18004e75 more antiquotations; wenzelm parents: 35762 diff changeset	39	val bound_rls = @{thms bound_rls} @ [@{thm boxL}, @{thm diaR}]
0dec18004e75 more antiquotations; wenzelm parents: 35762 diff changeset	40	val aside_rls = [@{thm lstar0}, @{thm lstar1}, @{thm lstar2}, @{thm rstar0},
0dec18004e75 more antiquotations; wenzelm parents: 35762 diff changeset	41	@{thm rstar1}, @{thm rstar2}]
21426 87ac12bed1ab converted legacy ML scripts; wenzelm parents: 17481 diff changeset	42	)
87ac12bed1ab converted legacy ML scripts; wenzelm parents: 17481 diff changeset	43	*}
87ac12bed1ab converted legacy ML scripts; wenzelm parents: 17481 diff changeset	44
54742 7a86358a3c0b proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.; wenzelm parents: 51309 diff changeset	45	method_setup T_solve = {* Scan.succeed (fn ctxt => SIMPLE_METHOD (T_Prover.solve_tac ctxt 2)) *}
21426 87ac12bed1ab converted legacy ML scripts; wenzelm parents: 17481 diff changeset	46
87ac12bed1ab converted legacy ML scripts; wenzelm parents: 17481 diff changeset	47
87ac12bed1ab converted legacy ML scripts; wenzelm parents: 17481 diff changeset	48	(* Theorems of system T from Hughes and Cresswell and Hailpern, LNCS 129 *)
87ac12bed1ab converted legacy ML scripts; wenzelm parents: 17481 diff changeset	49
87ac12bed1ab converted legacy ML scripts; wenzelm parents: 17481 diff changeset	50	lemma "\|- []P --> P" by T_solve
87ac12bed1ab converted legacy ML scripts; wenzelm parents: 17481 diff changeset	51	lemma "\|- [](P-->Q) --> ([]P-->[]Q)" by T_solve (* normality*)
87ac12bed1ab converted legacy ML scripts; wenzelm parents: 17481 diff changeset	52	lemma "\|- (P--<Q) --> []P --> []Q" by T_solve
87ac12bed1ab converted legacy ML scripts; wenzelm parents: 17481 diff changeset	53	lemma "\|- P --> <>P" by T_solve
87ac12bed1ab converted legacy ML scripts; wenzelm parents: 17481 diff changeset	54
87ac12bed1ab converted legacy ML scripts; wenzelm parents: 17481 diff changeset	55	lemma "\|- [](P & Q) <-> []P & []Q" by T_solve
87ac12bed1ab converted legacy ML scripts; wenzelm parents: 17481 diff changeset	56	lemma "\|- <>(P \| Q) <-> <>P \| <>Q" by T_solve
87ac12bed1ab converted legacy ML scripts; wenzelm parents: 17481 diff changeset	57	lemma "\|- [](P<->Q) <-> (P>-<Q)" by T_solve
87ac12bed1ab converted legacy ML scripts; wenzelm parents: 17481 diff changeset	58	lemma "\|- <>(P-->Q) <-> ([]P--><>Q)" by T_solve
87ac12bed1ab converted legacy ML scripts; wenzelm parents: 17481 diff changeset	59	lemma "\|- []P <-> ~<>(~P)" by T_solve
87ac12bed1ab converted legacy ML scripts; wenzelm parents: 17481 diff changeset	60	lemma "\|- [](~P) <-> ~<>P" by T_solve
87ac12bed1ab converted legacy ML scripts; wenzelm parents: 17481 diff changeset	61	lemma "\|- ~[]P <-> <>(~P)" by T_solve
87ac12bed1ab converted legacy ML scripts; wenzelm parents: 17481 diff changeset	62	lemma "\|- [][]P <-> ~<><>(~P)" by T_solve
87ac12bed1ab converted legacy ML scripts; wenzelm parents: 17481 diff changeset	63	lemma "\|- ~<>(P \| Q) <-> ~<>P & ~<>Q" by T_solve
87ac12bed1ab converted legacy ML scripts; wenzelm parents: 17481 diff changeset	64
87ac12bed1ab converted legacy ML scripts; wenzelm parents: 17481 diff changeset	65	lemma "\|- []P \| []Q --> [](P \| Q)" by T_solve
87ac12bed1ab converted legacy ML scripts; wenzelm parents: 17481 diff changeset	66	lemma "\|- <>(P & Q) --> <>P & <>Q" by T_solve
87ac12bed1ab converted legacy ML scripts; wenzelm parents: 17481 diff changeset	67	lemma "\|- [](P \| Q) --> []P \| <>Q" by T_solve
87ac12bed1ab converted legacy ML scripts; wenzelm parents: 17481 diff changeset	68	lemma "\|- <>P & []Q --> <>(P & Q)" by T_solve
87ac12bed1ab converted legacy ML scripts; wenzelm parents: 17481 diff changeset	69	lemma "\|- [](P \| Q) --> <>P \| []Q" by T_solve
87ac12bed1ab converted legacy ML scripts; wenzelm parents: 17481 diff changeset	70	lemma "\|- <>(P-->(Q & R)) --> ([]P --> <>Q) & ([]P--><>R)" by T_solve
87ac12bed1ab converted legacy ML scripts; wenzelm parents: 17481 diff changeset	71	lemma "\|- (P--<Q) & (Q--<R) --> (P--<R)" by T_solve
87ac12bed1ab converted legacy ML scripts; wenzelm parents: 17481 diff changeset	72	lemma "\|- []P --> <>Q --> <>(P & Q)" by T_solve
17481 75166ebb619b converted to Isar theory format; wenzelm parents: 2073 diff changeset	73
2073 fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala paulson parents: diff changeset	74	end

author	wenzelm
	Sun, 25 May 2014 17:08:46 +0200
changeset 57086	db7c735e963d
parent 54742	7a86358a3c0b
child 60770	240563fbf41d
permissions	-rw-r--r--