author | haftmann |
Tue, 28 Sep 2010 15:21:45 +0200 | |
changeset 39774 | 30cf9d80939e |
parent 35113 | 1a0c129bb2e0 |
child 48891 | c0eafbd55de3 |
permissions | -rw-r--r-- |
17481 | 1 |
(* Title: Sequents/Modal0.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 | 6 |
theory Modal0 |
7 |
imports LK0 |
|
8 |
uses "modal.ML" |
|
9 |
begin |
|
2073
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset
|
10 |
|
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset
|
11 |
consts |
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset
|
12 |
box :: "o=>o" ("[]_" [50] 50) |
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset
|
13 |
dia :: "o=>o" ("<>_" [50] 50) |
21426 | 14 |
strimp :: "[o,o]=>o" (infixr "--<" 25) |
15 |
streqv :: "[o,o]=>o" (infixr ">-<" 25) |
|
17481 | 16 |
Lstar :: "two_seqi" |
17 |
Rstar :: "two_seqi" |
|
14765 | 18 |
|
19 |
syntax |
|
35113 | 20 |
"_Lstar" :: "two_seqe" ("(_)|L>(_)" [6,6] 5) |
21 |
"_Rstar" :: "two_seqe" ("(_)|R>(_)" [6,6] 5) |
|
2073
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset
|
22 |
|
17481 | 23 |
ML {* |
35113 | 24 |
fun star_tr c [s1, s2] = Const(c, dummyT) $ seq_tr s1 $ seq_tr s2; |
25 |
fun star_tr' c [s1, s2] = Const(c, dummyT) $ seq_tr' s1 $ seq_tr' s2; |
|
17481 | 26 |
*} |
27 |
||
35113 | 28 |
parse_translation {* |
29 |
[(@{syntax_const "_Lstar"}, star_tr @{const_syntax Lstar}), |
|
30 |
(@{syntax_const "_Rstar"}, star_tr @{const_syntax Rstar})] |
|
31 |
*} |
|
32 |
||
33 |
print_translation {* |
|
34 |
[(@{const_syntax Lstar}, star_tr' @{syntax_const "_Lstar"}), |
|
35 |
(@{const_syntax Rstar}, star_tr' @{syntax_const "_Rstar"})] |
|
36 |
*} |
|
17481 | 37 |
|
38 |
defs |
|
39 |
strimp_def: "P --< Q == [](P --> Q)" |
|
40 |
streqv_def: "P >-< Q == (P --< Q) & (Q --< P)" |
|
41 |
||
21426 | 42 |
|
43 |
lemmas rewrite_rls = strimp_def streqv_def |
|
44 |
||
45 |
lemma iffR: |
|
46 |
"[| $H,P |- $E,Q,$F; $H,Q |- $E,P,$F |] ==> $H |- $E, P <-> Q, $F" |
|
47 |
apply (unfold iff_def) |
|
48 |
apply (assumption | rule conjR impR)+ |
|
49 |
done |
|
50 |
||
51 |
lemma iffL: |
|
52 |
"[| $H,$G |- $E,P,Q; $H,Q,P,$G |- $E |] ==> $H, P <-> Q, $G |- $E" |
|
53 |
apply (unfold iff_def) |
|
54 |
apply (assumption | rule conjL impL basic)+ |
|
55 |
done |
|
56 |
||
57 |
lemmas safe_rls = basic conjL conjR disjL disjR impL impR notL notR iffL iffR |
|
58 |
and unsafe_rls = allR exL |
|
59 |
and bound_rls = allL exR |
|
17481 | 60 |
|
61 |
end |