|
1 (* Title: ILL.thy |
|
2 ID: $Id$ |
|
3 Author: Sara Kalvala and Valeria de Paiva |
|
4 Copyright 1995 University of Cambridge |
|
5 *) |
|
6 |
|
7 |
|
8 ILL = Sequents + |
|
9 |
|
10 consts |
|
11 |
|
12 |
|
13 Trueprop :: "two_seqi" |
|
14 "@Trueprop" :: "single_seqe" ("((_)/ |- (_))" [6,6] 5) |
|
15 |
|
16 |
|
17 |
|
18 "><" ::"[o, o] => o" (infixr 35) |
|
19 "-o" ::"[o, o] => o" (infixr 45) |
|
20 "o-o" ::"[o, o] => o" (infixr 45) |
|
21 FShriek ::"o => o" ("! _" [100] 1000) |
|
22 "&&" ::"[o, o] => o" (infixr 35) |
|
23 "++" ::"[o, o] => o" (infixr 35) |
|
24 zero ::"o" ("0") |
|
25 top ::"o" ("1") |
|
26 eye ::"o" ("I") |
|
27 aneg ::"o=>o" ("~_") |
|
28 |
|
29 |
|
30 (* syntax for context manipulation *) |
|
31 |
|
32 Context :: "two_seqi" |
|
33 "@Context" :: "two_seqe" ("((_)/ :=: (_))" [6,6] 5) |
|
34 |
|
35 (* syntax for promotion rule *) |
|
36 |
|
37 PromAux :: "three_seqi" |
|
38 "@PromAux":: "three_seqe" ("promaux {_||_||_}") |
|
39 |
|
40 defs |
|
41 |
|
42 liff_def "P o-o Q == (P -o Q) >< (Q -o P)" |
|
43 |
|
44 aneg_def "~A == A -o 0" |
|
45 |
|
46 |
|
47 |
|
48 |
|
49 rules |
|
50 |
|
51 identity "P |- P" |
|
52 |
|
53 zerol "$G, 0, $H |- A" |
|
54 |
|
55 (* RULES THAT DO NOT DIVIDE CONTEXT *) |
|
56 |
|
57 derelict "$F, A, $G |- C ==> $F, !A, $G |- C" |
|
58 (* unfortunately, this one removes !A *) |
|
59 |
|
60 contract "$F, !A, !A, $G |- C ==> $F, !A, $G |- C" |
|
61 |
|
62 weaken "$F, $G |- C ==> $G, !A, $F |- C" |
|
63 (* weak form of weakening, in practice just to clean context *) |
|
64 (* weaken and contract not needed (CHECK) *) |
|
65 |
|
66 promote2 "promaux{ || $H || B} ==> $H |- !B" |
|
67 promote1 "promaux{!A, $G || $H || B} |
|
68 ==> promaux {$G || $H, !A || B}" |
|
69 promote0 "$G |- A ==> promaux {$G || || A}" |
|
70 |
|
71 |
|
72 |
|
73 tensl "$H, A, B, $G |- C ==> $H, A >< B, $G |- C" |
|
74 |
|
75 impr "A, $F |- B ==> $F |- A -o B" |
|
76 |
|
77 conjr "[| $F |- A ; |
|
78 $F |- B |] |
|
79 ==> $F |- (A && B)" |
|
80 |
|
81 conjll "$G, A, $H |- C ==> $G, A && B, $H |- C" |
|
82 |
|
83 conjlr "$G, B, $H |- C ==> $G, A && B, $H |- C" |
|
84 |
|
85 disjrl "$G |- A ==> $G |- A ++ B" |
|
86 disjrr "$G |- B ==> $G |- A ++ B" |
|
87 disjl "[| $G, A, $H |- C ; |
|
88 $G, B, $H |- C |] |
|
89 ==> $G, A ++ B, $H |- C" |
|
90 |
|
91 |
|
92 (* RULES THAT DIVIDE CONTEXT *) |
|
93 |
|
94 tensr "[| $F, $J :=: $G; |
|
95 $F |- A ; |
|
96 $J |- B |] |
|
97 ==> $G |- A >< B" |
|
98 |
|
99 impl "[| $G, $F :=: $J, $H ; |
|
100 B, $F |- C ; |
|
101 $G |- A |] |
|
102 ==> $J, A -o B, $H |- C" |
|
103 |
|
104 |
|
105 cut " [| $J1, $H1, $J2, $H3, $J3, $H2, $J4, $H4 :=: $F ; |
|
106 $H1, $H2, $H3, $H4 |- A ; |
|
107 $J1, $J2, A, $J3, $J4 |- B |] ==> $F |- B" |
|
108 |
|
109 |
|
110 (* CONTEXT RULES *) |
|
111 |
|
112 context1 "$G :=: $G" |
|
113 context2 "$F, $G :=: $H, !A, $G ==> $F, A, $G :=: $H, !A, $G" |
|
114 context3 "$F, $G :=: $H, $J ==> $F, A, $G :=: $H, A, $J" |
|
115 context4a "$F :=: $H, $G ==> $F :=: $H, !A, $G" |
|
116 context4b "$F, $H :=: $G ==> $F, !A, $H :=: $G" |
|
117 context5 "$F, $G :=: $H ==> $G, $F :=: $H" |
|
118 |
|
119 |
|
120 |
|
121 |
|
122 end |
|
123 |
|
124 ML |
|
125 |
|
126 val parse_translation = [("@Trueprop",Sequents.single_tr "Trueprop"), |
|
127 ("@Context",Sequents.two_seq_tr "Context"), |
|
128 ("@PromAux", Sequents.three_seq_tr "PromAux")]; |
|
129 |
|
130 val print_translation = [("Trueprop",Sequents.single_tr' "@Trueprop"), |
|
131 ("Context",Sequents.two_seq_tr'"@Context"), |
|
132 ("PromAux", Sequents.three_seq_tr'"@PromAux")]; |
|
133 |
|
134 |