| author | wenzelm |
| Fri, 21 May 2004 21:14:18 +0200 | |
| changeset 14765 | bafb24c150c1 |
| parent 7098 | 86583034aacf |
| child 17481 | 75166ebb619b |
| permissions | -rw-r--r-- |
|
7098
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
2073
diff
changeset
|
1 |
(* Title: Sequents/Modal0 |
|
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 |
|
|
7098
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
2073
diff
changeset
|
7 |
Modal0 = LK0 + |
|
2073
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset
|
8 |
|
|
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset
|
9 |
consts |
|
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset
|
10 |
box :: "o=>o" ("[]_" [50] 50)
|
|
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset
|
11 |
dia :: "o=>o" ("<>_" [50] 50)
|
|
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset
|
12 |
"--<",">-<" :: "[o,o]=>o" (infixr 25) |
| 14765 | 13 |
Lstar,Rstar :: "two_seqi" |
14 |
||
15 |
syntax |
|
|
2073
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset
|
16 |
"@Lstar" :: "two_seqe" ("(_)|L>(_)" [6,6] 5)
|
|
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset
|
17 |
"@Rstar" :: "two_seqe" ("(_)|R>(_)" [6,6] 5)
|
|
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset
|
18 |
|
|
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset
|
19 |
rules |
|
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset
|
20 |
(* Definitions *) |
|
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 |
strimp_def "P --< Q == [](P --> Q)" |
|
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset
|
23 |
streqv_def "P >-< Q == (P --< Q) & (Q --< P)" |
|
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset
|
24 |
end |
|
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset
|
25 |
|
|
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset
|
26 |
ML |
|
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset
|
27 |
|
|
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset
|
28 |
local |
|
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset
|
29 |
|
|
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset
|
30 |
val Lstar = "Lstar"; |
|
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset
|
31 |
val Rstar = "Rstar"; |
|
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset
|
32 |
val SLstar = "@Lstar"; |
|
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset
|
33 |
val SRstar = "@Rstar"; |
|
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset
|
34 |
|
|
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset
|
35 |
fun star_tr c [s1,s2] = |
|
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset
|
36 |
Const(c,dummyT)$Sequents.seq_tr s1$Sequents.seq_tr s2; |
|
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset
|
37 |
fun star_tr' c [s1,s2] = |
|
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset
|
38 |
Const(c,dummyT) $ Sequents.seq_tr' s1 $ Sequents.seq_tr' s2; |
|
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset
|
39 |
in |
|
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset
|
40 |
val parse_translation = [(SLstar,star_tr Lstar), (SRstar,star_tr Rstar)]; |
|
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset
|
41 |
val print_translation = [(Lstar,star_tr' SLstar), (Rstar,star_tr' SRstar)] |
|
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset
|
42 |
end; |