54 aneg_def: "~A == A -o 0" |
54 aneg_def: "~A == A -o 0" |
55 |
55 |
56 |
56 |
57 axiomatization where |
57 axiomatization where |
58 |
58 |
59 identity: "P |- P" and |
59 identity: "P \<turnstile> P" and |
60 |
60 |
61 zerol: "$G, 0, $H |- A" and |
61 zerol: "$G, 0, $H \<turnstile> A" and |
62 |
62 |
63 (* RULES THAT DO NOT DIVIDE CONTEXT *) |
63 (* RULES THAT DO NOT DIVIDE CONTEXT *) |
64 |
64 |
65 derelict: "$F, A, $G |- C \<Longrightarrow> $F, !A, $G |- C" and |
65 derelict: "$F, A, $G \<turnstile> C \<Longrightarrow> $F, !A, $G \<turnstile> C" and |
66 (* unfortunately, this one removes !A *) |
66 (* unfortunately, this one removes !A *) |
67 |
67 |
68 contract: "$F, !A, !A, $G |- C \<Longrightarrow> $F, !A, $G |- C" and |
68 contract: "$F, !A, !A, $G \<turnstile> C \<Longrightarrow> $F, !A, $G \<turnstile> C" and |
69 |
69 |
70 weaken: "$F, $G |- C \<Longrightarrow> $G, !A, $F |- C" and |
70 weaken: "$F, $G \<turnstile> C \<Longrightarrow> $G, !A, $F \<turnstile> C" and |
71 (* weak form of weakening, in practice just to clean context *) |
71 (* weak form of weakening, in practice just to clean context *) |
72 (* weaken and contract not needed (CHECK) *) |
72 (* weaken and contract not needed (CHECK) *) |
73 |
73 |
74 promote2: "promaux{ || $H || B} \<Longrightarrow> $H |- !B" and |
74 promote2: "promaux{ || $H || B} \<Longrightarrow> $H \<turnstile> !B" and |
75 promote1: "promaux{!A, $G || $H || B} |
75 promote1: "promaux{!A, $G || $H || B} |
76 \<Longrightarrow> promaux {$G || $H, !A || B}" and |
76 \<Longrightarrow> promaux {$G || $H, !A || B}" and |
77 promote0: "$G |- A \<Longrightarrow> promaux {$G || || A}" and |
77 promote0: "$G \<turnstile> A \<Longrightarrow> promaux {$G || || A}" and |
78 |
78 |
79 |
79 |
80 |
80 |
81 tensl: "$H, A, B, $G |- C \<Longrightarrow> $H, A >< B, $G |- C" and |
81 tensl: "$H, A, B, $G \<turnstile> C \<Longrightarrow> $H, A >< B, $G \<turnstile> C" and |
82 |
82 |
83 impr: "A, $F |- B \<Longrightarrow> $F |- A -o B" and |
83 impr: "A, $F \<turnstile> B \<Longrightarrow> $F \<turnstile> A -o B" and |
84 |
84 |
85 conjr: "\<lbrakk>$F |- A ; |
85 conjr: "\<lbrakk>$F \<turnstile> A ; |
86 $F |- B\<rbrakk> |
86 $F \<turnstile> B\<rbrakk> |
87 \<Longrightarrow> $F |- (A && B)" and |
87 \<Longrightarrow> $F \<turnstile> (A && B)" and |
88 |
88 |
89 conjll: "$G, A, $H |- C \<Longrightarrow> $G, A && B, $H |- C" and |
89 conjll: "$G, A, $H \<turnstile> C \<Longrightarrow> $G, A && B, $H \<turnstile> C" and |
90 |
90 |
91 conjlr: "$G, B, $H |- C \<Longrightarrow> $G, A && B, $H |- C" and |
91 conjlr: "$G, B, $H \<turnstile> C \<Longrightarrow> $G, A && B, $H \<turnstile> C" and |
92 |
92 |
93 disjrl: "$G |- A \<Longrightarrow> $G |- A ++ B" and |
93 disjrl: "$G \<turnstile> A \<Longrightarrow> $G \<turnstile> A ++ B" and |
94 disjrr: "$G |- B \<Longrightarrow> $G |- A ++ B" and |
94 disjrr: "$G \<turnstile> B \<Longrightarrow> $G \<turnstile> A ++ B" and |
95 disjl: "\<lbrakk>$G, A, $H |- C ; |
95 disjl: "\<lbrakk>$G, A, $H \<turnstile> C ; |
96 $G, B, $H |- C\<rbrakk> |
96 $G, B, $H \<turnstile> C\<rbrakk> |
97 \<Longrightarrow> $G, A ++ B, $H |- C" and |
97 \<Longrightarrow> $G, A ++ B, $H \<turnstile> C" and |
98 |
98 |
99 |
99 |
100 (* RULES THAT DIVIDE CONTEXT *) |
100 (* RULES THAT DIVIDE CONTEXT *) |
101 |
101 |
102 tensr: "\<lbrakk>$F, $J :=: $G; |
102 tensr: "\<lbrakk>$F, $J :=: $G; |
103 $F |- A ; |
103 $F \<turnstile> A ; |
104 $J |- B\<rbrakk> |
104 $J \<turnstile> B\<rbrakk> |
105 \<Longrightarrow> $G |- A >< B" and |
105 \<Longrightarrow> $G \<turnstile> A >< B" and |
106 |
106 |
107 impl: "\<lbrakk>$G, $F :=: $J, $H ; |
107 impl: "\<lbrakk>$G, $F :=: $J, $H ; |
108 B, $F |- C ; |
108 B, $F \<turnstile> C ; |
109 $G |- A\<rbrakk> |
109 $G \<turnstile> A\<rbrakk> |
110 \<Longrightarrow> $J, A -o B, $H |- C" and |
110 \<Longrightarrow> $J, A -o B, $H \<turnstile> C" and |
111 |
111 |
112 |
112 |
113 cut: "\<lbrakk> $J1, $H1, $J2, $H3, $J3, $H2, $J4, $H4 :=: $F ; |
113 cut: "\<lbrakk> $J1, $H1, $J2, $H3, $J3, $H2, $J4, $H4 :=: $F ; |
114 $H1, $H2, $H3, $H4 |- A ; |
114 $H1, $H2, $H3, $H4 \<turnstile> A ; |
115 $J1, $J2, A, $J3, $J4 |- B\<rbrakk> \<Longrightarrow> $F |- B" and |
115 $J1, $J2, A, $J3, $J4 \<turnstile> B\<rbrakk> \<Longrightarrow> $F \<turnstile> B" and |
116 |
116 |
117 |
117 |
118 (* CONTEXT RULES *) |
118 (* CONTEXT RULES *) |
119 |
119 |
120 context1: "$G :=: $G" and |
120 context1: "$G :=: $G" and |
148 conjlr |
148 conjlr |
149 conjll |
149 conjll |
150 zerol |
150 zerol |
151 identity |
151 identity |
152 |
152 |
153 lemma aux_impl: "$F, $G |- A \<Longrightarrow> $F, !(A -o B), $G |- B" |
153 lemma aux_impl: "$F, $G \<turnstile> A \<Longrightarrow> $F, !(A -o B), $G \<turnstile> B" |
154 apply (rule derelict) |
154 apply (rule derelict) |
155 apply (rule impl) |
155 apply (rule impl) |
156 apply (rule_tac [2] identity) |
156 apply (rule_tac [2] identity) |
157 apply (rule context1) |
157 apply (rule context1) |
158 apply assumption |
158 apply assumption |
159 done |
159 done |
160 |
160 |
161 lemma conj_lemma: " $F, !A, !B, $G |- C \<Longrightarrow> $F, !(A && B), $G |- C" |
161 lemma conj_lemma: " $F, !A, !B, $G \<turnstile> C \<Longrightarrow> $F, !(A && B), $G \<turnstile> C" |
162 apply (rule contract) |
162 apply (rule contract) |
163 apply (rule_tac A = " (!A) >< (!B) " in cut) |
163 apply (rule_tac A = " (!A) >< (!B) " in cut) |
164 apply (rule_tac [2] tensr) |
164 apply (rule_tac [2] tensr) |
165 prefer 3 |
165 prefer 3 |
166 apply (subgoal_tac "! (A && B) |- !A") |
166 apply (subgoal_tac "! (A && B) \<turnstile> !A") |
167 apply assumption |
167 apply assumption |
168 apply best |
168 apply best |
169 prefer 3 |
169 prefer 3 |
170 apply (subgoal_tac "! (A && B) |- !B") |
170 apply (subgoal_tac "! (A && B) \<turnstile> !B") |
171 apply assumption |
171 apply assumption |
172 apply best |
172 apply best |
173 apply (rule_tac [2] context1) |
173 apply (rule_tac [2] context1) |
174 apply (rule_tac [2] tensl) |
174 apply (rule_tac [2] tensl) |
175 prefer 2 apply assumption |
175 prefer 2 apply assumption |
176 apply (rule context3) |
176 apply (rule context3) |
177 apply (rule context3) |
177 apply (rule context3) |
178 apply (rule context1) |
178 apply (rule context1) |
179 done |
179 done |
180 |
180 |
181 lemma impr_contract: "!A, !A, $G |- B \<Longrightarrow> $G |- (!A) -o B" |
181 lemma impr_contract: "!A, !A, $G \<turnstile> B \<Longrightarrow> $G \<turnstile> (!A) -o B" |
182 apply (rule impr) |
182 apply (rule impr) |
183 apply (rule contract) |
183 apply (rule contract) |
184 apply assumption |
184 apply assumption |
185 done |
185 done |
186 |
186 |
187 lemma impr_contr_der: "A, !A, $G |- B \<Longrightarrow> $G |- (!A) -o B" |
187 lemma impr_contr_der: "A, !A, $G \<turnstile> B \<Longrightarrow> $G \<turnstile> (!A) -o B" |
188 apply (rule impr) |
188 apply (rule impr) |
189 apply (rule contract) |
189 apply (rule contract) |
190 apply (rule derelict) |
190 apply (rule derelict) |
191 apply assumption |
191 apply assumption |
192 done |
192 done |
193 |
193 |
194 lemma contrad1: "$F, (!B) -o 0, $G, !B, $H |- A" |
194 lemma contrad1: "$F, (!B) -o 0, $G, !B, $H \<turnstile> A" |
195 apply (rule impl) |
195 apply (rule impl) |
196 apply (rule_tac [3] identity) |
196 apply (rule_tac [3] identity) |
197 apply (rule context3) |
197 apply (rule context3) |
198 apply (rule context1) |
198 apply (rule context1) |
199 apply (rule zerol) |
199 apply (rule zerol) |
200 done |
200 done |
201 |
201 |
202 |
202 |
203 lemma contrad2: "$F, !B, $G, (!B) -o 0, $H |- A" |
203 lemma contrad2: "$F, !B, $G, (!B) -o 0, $H \<turnstile> A" |
204 apply (rule impl) |
204 apply (rule impl) |
205 apply (rule_tac [3] identity) |
205 apply (rule_tac [3] identity) |
206 apply (rule context3) |
206 apply (rule context3) |
207 apply (rule context1) |
207 apply (rule context1) |
208 apply (rule zerol) |
208 apply (rule zerol) |
209 done |
209 done |
210 |
210 |
211 lemma ll_mp: "A -o B, A |- B" |
211 lemma ll_mp: "A -o B, A \<turnstile> B" |
212 apply (rule impl) |
212 apply (rule impl) |
213 apply (rule_tac [2] identity) |
213 apply (rule_tac [2] identity) |
214 apply (rule_tac [2] identity) |
214 apply (rule_tac [2] identity) |
215 apply (rule context1) |
215 apply (rule context1) |
216 done |
216 done |
217 |
217 |
218 lemma mp_rule1: "$F, B, $G, $H |- C \<Longrightarrow> $F, A, $G, A -o B, $H |- C" |
218 lemma mp_rule1: "$F, B, $G, $H \<turnstile> C \<Longrightarrow> $F, A, $G, A -o B, $H \<turnstile> C" |
219 apply (rule_tac A = "B" in cut) |
219 apply (rule_tac A = "B" in cut) |
220 apply (rule_tac [2] ll_mp) |
220 apply (rule_tac [2] ll_mp) |
221 prefer 2 apply (assumption) |
221 prefer 2 apply (assumption) |
222 apply (rule context3) |
222 apply (rule context3) |
223 apply (rule context3) |
223 apply (rule context3) |
224 apply (rule context1) |
224 apply (rule context1) |
225 done |
225 done |
226 |
226 |
227 lemma mp_rule2: "$F, B, $G, $H |- C \<Longrightarrow> $F, A -o B, $G, A, $H |- C" |
227 lemma mp_rule2: "$F, B, $G, $H \<turnstile> C \<Longrightarrow> $F, A -o B, $G, A, $H \<turnstile> C" |
228 apply (rule_tac A = "B" in cut) |
228 apply (rule_tac A = "B" in cut) |
229 apply (rule_tac [2] ll_mp) |
229 apply (rule_tac [2] ll_mp) |
230 prefer 2 apply (assumption) |
230 prefer 2 apply (assumption) |
231 apply (rule context3) |
231 apply (rule context3) |
232 apply (rule context3) |
232 apply (rule context3) |
233 apply (rule context1) |
233 apply (rule context1) |
234 done |
234 done |
235 |
235 |
236 lemma or_to_and: "!((!(A ++ B)) -o 0) |- !( ((!A) -o 0) && ((!B) -o 0))" |
236 lemma or_to_and: "!((!(A ++ B)) -o 0) \<turnstile> !( ((!A) -o 0) && ((!B) -o 0))" |
237 by best |
237 by best |
238 |
238 |
239 lemma o_a_rule: "$F, !( ((!A) -o 0) && ((!B) -o 0)), $G |- C \<Longrightarrow> |
239 lemma o_a_rule: "$F, !( ((!A) -o 0) && ((!B) -o 0)), $G \<turnstile> C \<Longrightarrow> |
240 $F, !((!(A ++ B)) -o 0), $G |- C" |
240 $F, !((!(A ++ B)) -o 0), $G \<turnstile> C" |
241 apply (rule cut) |
241 apply (rule cut) |
242 apply (rule_tac [2] or_to_and) |
242 apply (rule_tac [2] or_to_and) |
243 prefer 2 apply (assumption) |
243 prefer 2 apply (assumption) |
244 apply (rule context3) |
244 apply (rule context3) |
245 apply (rule context1) |
245 apply (rule context1) |
246 done |
246 done |
247 |
247 |
248 lemma conj_imp: "((!A) -o C) ++ ((!B) -o C) |- (!(A && B)) -o C" |
248 lemma conj_imp: "((!A) -o C) ++ ((!B) -o C) \<turnstile> (!(A && B)) -o C" |
249 apply (rule impr) |
249 apply (rule impr) |
250 apply (rule conj_lemma) |
250 apply (rule conj_lemma) |
251 apply (rule disjl) |
251 apply (rule disjl) |
252 apply (rule mp_rule1, best)+ |
252 apply (rule mp_rule1, best)+ |
253 done |
253 done |
254 |
254 |
255 lemma not_imp: "!A, !((!B) -o 0) |- (!((!A) -o B)) -o 0" |
255 lemma not_imp: "!A, !((!B) -o 0) \<turnstile> (!((!A) -o B)) -o 0" |
256 by best |
256 by best |
257 |
257 |
258 lemma a_not_a: "!A -o (!A -o 0) |- !A -o 0" |
258 lemma a_not_a: "!A -o (!A -o 0) \<turnstile> !A -o 0" |
259 apply (rule impr) |
259 apply (rule impr) |
260 apply (rule contract) |
260 apply (rule contract) |
261 apply (rule impl) |
261 apply (rule impl) |
262 apply (rule_tac [3] identity) |
262 apply (rule_tac [3] identity) |
263 apply (rule context1) |
263 apply (rule context1) |
264 apply best |
264 apply best |
265 done |
265 done |
266 |
266 |
267 lemma a_not_a_rule: "$J1, !A -o 0, $J2 |- B \<Longrightarrow> $J1, !A -o (!A -o 0), $J2 |- B" |
267 lemma a_not_a_rule: "$J1, !A -o 0, $J2 \<turnstile> B \<Longrightarrow> $J1, !A -o (!A -o 0), $J2 \<turnstile> B" |
268 apply (rule_tac A = "!A -o 0" in cut) |
268 apply (rule_tac A = "!A -o 0" in cut) |
269 apply (rule_tac [2] a_not_a) |
269 apply (rule_tac [2] a_not_a) |
270 prefer 2 apply assumption |
270 prefer 2 apply assumption |
271 apply best |
271 apply best |
272 done |
272 done |