author | haftmann |
Mon, 08 Jun 2009 08:38:51 +0200 | |
changeset 31483 | 88210717bfc8 |
parent 30549 | d2d7874648bd |
child 35762 | af3ff2ba4c54 |
permissions | -rw-r--r-- |
17481 | 1 |
(* Title: Modal/T.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 | 7 |
theory T |
8 |
imports Modal0 |
|
9 |
begin |
|
10 |
||
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 T: 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 | 16 |
lstar0: "|L>" |
17 |
lstar1: "$G |L> $H ==> []P, $G |L> P, $H" |
|
18 |
lstar2: "$G |L> $H ==> P, $G |L> $H" |
|
19 |
rstar0: "|R>" |
|
20 |
rstar1: "$G |R> $H ==> <>P, $G |R> P, $H" |
|
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 | 25 |
boxR: |
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 | 28 |
boxL: "$E, P, $F |- $G ==> $E, []P, $F |- $G" |
29 |
diaR: "$E |- $F, P, $G ==> $E |- $F, <>P, $G" |
|
30 |
diaL: |
|
31 |
"[| $E |L> $E'; $F |L> $F'; $G |R> $G'; |
|
2073
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset
|
32 |
$E', P, $F'|- $G'|] ==> $E, <>P, $F |- $G" |
17481 | 33 |
|
21426 | 34 |
ML {* |
35 |
structure T_Prover = Modal_ProverFun |
|
36 |
( |
|
37 |
val rewrite_rls = thms "rewrite_rls" |
|
38 |
val safe_rls = thms "safe_rls" |
|
39 |
val unsafe_rls = thms "unsafe_rls" @ [thm "boxR", thm "diaL"] |
|
40 |
val bound_rls = thms "bound_rls" @ [thm "boxL", thm "diaR"] |
|
41 |
val aside_rls = [thm "lstar0", thm "lstar1", thm "lstar2", thm "rstar0", |
|
42 |
thm "rstar1", thm "rstar2"] |
|
43 |
) |
|
44 |
*} |
|
45 |
||
46 |
method_setup T_solve = |
|
30549 | 47 |
{* Scan.succeed (K (SIMPLE_METHOD (T_Prover.solve_tac 2))) *} "T solver" |
21426 | 48 |
|
49 |
||
50 |
(* Theorems of system T from Hughes and Cresswell and Hailpern, LNCS 129 *) |
|
51 |
||
52 |
lemma "|- []P --> P" by T_solve |
|
53 |
lemma "|- [](P-->Q) --> ([]P-->[]Q)" by T_solve (* normality*) |
|
54 |
lemma "|- (P--<Q) --> []P --> []Q" by T_solve |
|
55 |
lemma "|- P --> <>P" by T_solve |
|
56 |
||
57 |
lemma "|- [](P & Q) <-> []P & []Q" by T_solve |
|
58 |
lemma "|- <>(P | Q) <-> <>P | <>Q" by T_solve |
|
59 |
lemma "|- [](P<->Q) <-> (P>-<Q)" by T_solve |
|
60 |
lemma "|- <>(P-->Q) <-> ([]P--><>Q)" by T_solve |
|
61 |
lemma "|- []P <-> ~<>(~P)" by T_solve |
|
62 |
lemma "|- [](~P) <-> ~<>P" by T_solve |
|
63 |
lemma "|- ~[]P <-> <>(~P)" by T_solve |
|
64 |
lemma "|- [][]P <-> ~<><>(~P)" by T_solve |
|
65 |
lemma "|- ~<>(P | Q) <-> ~<>P & ~<>Q" by T_solve |
|
66 |
||
67 |
lemma "|- []P | []Q --> [](P | Q)" by T_solve |
|
68 |
lemma "|- <>(P & Q) --> <>P & <>Q" by T_solve |
|
69 |
lemma "|- [](P | Q) --> []P | <>Q" by T_solve |
|
70 |
lemma "|- <>P & []Q --> <>(P & Q)" by T_solve |
|
71 |
lemma "|- [](P | Q) --> <>P | []Q" by T_solve |
|
72 |
lemma "|- <>(P-->(Q & R)) --> ([]P --> <>Q) & ([]P--><>R)" by T_solve |
|
73 |
lemma "|- (P--<Q) & (Q--<R) --> (P--<R)" by T_solve |
|
74 |
lemma "|- []P --> <>Q --> <>(P & Q)" by T_solve |
|
17481 | 75 |
|
2073
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset
|
76 |
end |