1(*  Title:      Sequents/ILL.thy
2    Author:     Sara Kalvala and Valeria de Paiva
3    Copyright   1995  University of Cambridge
4*)
5
6theory ILL
7imports Sequents
8begin
9
10consts
11  Trueprop       :: "two_seqi"
12
13  tens :: "[o, o] \<Rightarrow> o"        (infixr "><" 35)
14  limp :: "[o, o] \<Rightarrow> o"        (infixr "-o" 45)
15  FShriek :: "o \<Rightarrow> o"          ("! _" [100] 1000)
16  lconj :: "[o, o] \<Rightarrow> o"       (infixr "&&" 35)
17  ldisj :: "[o, o] \<Rightarrow> o"       (infixr "++" 35)
18  zero :: "o"                  ("0")
19  top :: "o"                   ("1")
20  eye :: "o"                   ("I")
21
22
23  (* context manipulation *)
24
25 Context      :: "two_seqi"
26
27  (* promotion rule *)
28
29  PromAux :: "three_seqi"
30
31syntax
32  "_Trueprop" :: "single_seqe" ("((_)/ \<turnstile> (_))" [6,6] 5)
33  "_Context"  :: "two_seqe"   ("((_)/ :=: (_))" [6,6] 5)
34  "_PromAux"  :: "three_seqe" ("promaux {_||_||_}")
35
36parse_translation \<open>
37  [(\<^syntax_const>\<open>_Trueprop\<close>, K (single_tr \<^const_syntax>\<open>Trueprop\<close>)),
38   (\<^syntax_const>\<open>_Context\<close>, K (two_seq_tr \<^const_syntax>\<open>Context\<close>)),
39   (\<^syntax_const>\<open>_PromAux\<close>, K (three_seq_tr \<^const_syntax>\<open>PromAux\<close>))]
40\<close>
41
42print_translation \<open>
43  [(\<^const_syntax>\<open>Trueprop\<close>, K (single_tr' \<^syntax_const>\<open>_Trueprop\<close>)),
44   (\<^const_syntax>\<open>Context\<close>, K (two_seq_tr' \<^syntax_const>\<open>_Context\<close>)),
45   (\<^const_syntax>\<open>PromAux\<close>, K (three_seq_tr' \<^syntax_const>\<open>_PromAux\<close>))]
46\<close>
47
48definition liff :: "[o, o] \<Rightarrow> o"  (infixr "o-o" 45)
49  where "P o-o Q == (P -o Q) >< (Q -o P)"
50
51definition aneg :: "o\<Rightarrow>o"  ("~_")
52  where "~A == A -o 0"
53
54
55axiomatization where
56
57identity:        "P \<turnstile> P" and
58
59zerol:           "$G, 0, $H \<turnstile> A" and
60
61  (* RULES THAT DO NOT DIVIDE CONTEXT *)
62
63derelict:   "$F, A, $G \<turnstile> C \<Longrightarrow> $F, !A, $G \<turnstile> C" and
64  (* unfortunately, this one removes !A  *)
65
66contract:  "$F, !A, !A, $G \<turnstile> C \<Longrightarrow> $F, !A, $G \<turnstile> C" and
67
68weaken:     "$F, $G \<turnstile> C \<Longrightarrow> $G, !A, $F \<turnstile> C" and
69  (* weak form of weakening, in practice just to clean context *)
70  (* weaken and contract not needed (CHECK)  *)
71
72promote2:        "promaux{ || $H || B} \<Longrightarrow> $H \<turnstile> !B" and
73promote1:        "promaux{!A, $G || $H || B}
74                  \<Longrightarrow> promaux {$G || $H, !A || B}" and
75promote0:        "$G \<turnstile> A \<Longrightarrow> promaux {$G || || A}" and
76
77
78
79tensl:     "$H, A, B, $G \<turnstile> C \<Longrightarrow> $H, A >< B, $G \<turnstile> C" and
80
81impr:      "A, $F \<turnstile> B \<Longrightarrow> $F \<turnstile> A -o B" and
82
83conjr:           "\<lbrakk>$F \<turnstile> A ;
84                 $F \<turnstile> B\<rbrakk>
85                \<Longrightarrow> $F \<turnstile> (A && B)" and
86
87conjll:          "$G, A, $H \<turnstile> C \<Longrightarrow> $G, A && B, $H \<turnstile> C" and
88
89conjlr:          "$G, B, $H \<turnstile> C \<Longrightarrow> $G, A && B, $H \<turnstile> C" and
90
91disjrl:          "$G \<turnstile> A \<Longrightarrow> $G \<turnstile> A ++ B" and
92disjrr:          "$G \<turnstile> B \<Longrightarrow> $G \<turnstile> A ++ B" and
93disjl:           "\<lbrakk>$G, A, $H \<turnstile> C ;
94                   $G, B, $H \<turnstile> C\<rbrakk>
95                 \<Longrightarrow> $G, A ++ B, $H \<turnstile> C" and
96
97
98      (* RULES THAT DIVIDE CONTEXT *)
99
100tensr:           "\<lbrakk>$F, $J :=: $G;
101                   $F \<turnstile> A ;
102                   $J \<turnstile> B\<rbrakk>
103                     \<Longrightarrow> $G \<turnstile> A >< B" and
104
105impl:            "\<lbrakk>$G, $F :=: $J, $H ;
106                   B, $F \<turnstile> C ;
107                   $G \<turnstile> A\<rbrakk>
108                     \<Longrightarrow> $J, A -o B, $H \<turnstile> C" and
109
110
111cut: "\<lbrakk> $J1, $H1, $J2, $H3, $J3, $H2, $J4, $H4 :=: $F ;
112        $H1, $H2, $H3, $H4 \<turnstile> A ;
113        $J1, $J2, A, $J3, $J4 \<turnstile> B\<rbrakk> \<Longrightarrow> $F \<turnstile> B" and
114
115
116  (* CONTEXT RULES *)
117
118context1:     "$G :=: $G" and
119context2:     "$F, $G :=: $H, !A, $G \<Longrightarrow> $F, A, $G :=: $H, !A, $G" and
120context3:     "$F, $G :=: $H, $J \<Longrightarrow> $F, A, $G :=: $H, A, $J" and
121context4a:    "$F :=: $H, $G \<Longrightarrow> $F :=: $H, !A, $G" and
122context4b:    "$F, $H :=: $G \<Longrightarrow> $F, !A, $H :=: $G" and
123context5:     "$F, $G :=: $H \<Longrightarrow> $G, $F :=: $H"
124
125text "declarations for lazy classical reasoning:"
126lemmas [safe] =
127  context3
128  context2
129  promote0
130  disjl
131  conjr
132  tensl
133lemmas [unsafe] =
134  context4b
135  context4a
136  context1
137  promote2
138  promote1
139  weaken
140  derelict
141  impl
142  tensr
143  impr
144  disjrr
145  disjrl
146  conjlr
147  conjll
148  zerol
149  identity
150
151lemma aux_impl: "$F, $G \<turnstile> A \<Longrightarrow> $F, !(A -o B), $G \<turnstile> B"
152  apply (rule derelict)
153  apply (rule impl)
154  apply (rule_tac [2] identity)
155  apply (rule context1)
156  apply assumption
157  done
158
159lemma conj_lemma: " $F, !A, !B, $G \<turnstile> C \<Longrightarrow> $F, !(A && B), $G \<turnstile> C"
160  apply (rule contract)
161  apply (rule_tac A = " (!A) >< (!B) " in cut)
162  apply (rule_tac [2] tensr)
163  prefer 3
164  apply (subgoal_tac "! (A && B) \<turnstile> !A")
165  apply assumption
166  apply best
167  prefer 3
168  apply (subgoal_tac "! (A && B) \<turnstile> !B")
169  apply assumption
170  apply best
171  apply (rule_tac [2] context1)
172  apply (rule_tac [2] tensl)
173  prefer 2 apply assumption
174  apply (rule context3)
175  apply (rule context3)
176  apply (rule context1)
177  done
178
179lemma impr_contract: "!A, !A, $G \<turnstile> B \<Longrightarrow> $G \<turnstile> (!A) -o B"
180  apply (rule impr)
181  apply (rule contract)
182  apply assumption
183  done
184
185lemma impr_contr_der: "A, !A, $G \<turnstile> B \<Longrightarrow> $G \<turnstile> (!A) -o B"
186  apply (rule impr)
187  apply (rule contract)
188  apply (rule derelict)
189  apply assumption
190  done
191
192lemma contrad1: "$F, (!B) -o 0, $G, !B, $H \<turnstile> A"
193  apply (rule impl)
194  apply (rule_tac [3] identity)
195  apply (rule context3)
196  apply (rule context1)
197  apply (rule zerol)
198  done
199
200
201lemma contrad2: "$F, !B, $G, (!B) -o 0, $H \<turnstile> A"
202  apply (rule impl)
203  apply (rule_tac [3] identity)
204  apply (rule context3)
205  apply (rule context1)
206  apply (rule zerol)
207  done
208
209lemma ll_mp: "A -o B, A \<turnstile> B"
210  apply (rule impl)
211  apply (rule_tac [2] identity)
212  apply (rule_tac [2] identity)
213  apply (rule context1)
214  done
215
216lemma mp_rule1: "$F, B, $G, $H \<turnstile> C \<Longrightarrow> $F, A, $G, A -o B, $H \<turnstile> C"
217  apply (rule_tac A = "B" in cut)
218  apply (rule_tac [2] ll_mp)
219  prefer 2 apply (assumption)
220  apply (rule context3)
221  apply (rule context3)
222  apply (rule context1)
223  done
224
225lemma mp_rule2: "$F, B, $G, $H \<turnstile> C \<Longrightarrow> $F, A -o B, $G, A, $H \<turnstile> C"
226  apply (rule_tac A = "B" in cut)
227  apply (rule_tac [2] ll_mp)
228  prefer 2 apply (assumption)
229  apply (rule context3)
230  apply (rule context3)
231  apply (rule context1)
232  done
233
234lemma or_to_and: "!((!(A ++ B)) -o 0) \<turnstile> !( ((!A) -o 0) && ((!B) -o 0))"
235  by best
236
237lemma o_a_rule: "$F, !( ((!A) -o 0) && ((!B) -o 0)), $G \<turnstile> C \<Longrightarrow>
238          $F, !((!(A ++ B)) -o 0), $G \<turnstile> C"
239  apply (rule cut)
240  apply (rule_tac [2] or_to_and)
241  prefer 2 apply (assumption)
242  apply (rule context3)
243  apply (rule context1)
244  done
245
246lemma conj_imp: "((!A) -o C) ++ ((!B) -o C) \<turnstile> (!(A && B)) -o C"
247  apply (rule impr)
248  apply (rule conj_lemma)
249  apply (rule disjl)
250  apply (rule mp_rule1, best)+
251  done
252
253lemma not_imp: "!A, !((!B) -o 0) \<turnstile> (!((!A) -o B)) -o 0"
254  by best
255
256lemma a_not_a: "!A -o (!A -o 0) \<turnstile> !A -o 0"
257  apply (rule impr)
258  apply (rule contract)
259  apply (rule impl)
260  apply (rule_tac [3] identity)
261  apply (rule context1)
262  apply best
263  done
264
265lemma a_not_a_rule: "$J1, !A -o 0, $J2 \<turnstile> B \<Longrightarrow> $J1, !A -o (!A -o 0), $J2 \<turnstile> B"
266  apply (rule_tac A = "!A -o 0" in cut)
267  apply (rule_tac [2] a_not_a)
268  prefer 2 apply assumption
269  apply best
270  done
271
272ML \<open>
273  val safe_pack =
274    \<^context>
275    |> fold_rev Cla.add_safe @{thms conj_lemma ll_mp contrad1
276        contrad2 mp_rule1 mp_rule2 o_a_rule a_not_a_rule}
277    |> Cla.add_unsafe @{thm aux_impl}
278    |> Cla.get_pack;
279
280  val power_pack =
281    Cla.put_pack safe_pack \<^context>
282    |> Cla.add_unsafe @{thm impr_contr_der}
283    |> Cla.get_pack;
284\<close>
285
286method_setup best_safe =
287  \<open>Scan.succeed (fn ctxt => SIMPLE_METHOD' (Cla.best_tac (Cla.put_pack safe_pack ctxt)))\<close>
288
289method_setup best_power =
290  \<open>Scan.succeed (fn ctxt => SIMPLE_METHOD' (Cla.best_tac (Cla.put_pack power_pack ctxt)))\<close>
291
292
293(* Some examples from Troelstra and van Dalen *)
294
295lemma "!((!A) -o ((!B) -o 0)) \<turnstile> (!(A && B)) -o 0"
296  by best_safe
297
298lemma "!((!(A && B)) -o 0) \<turnstile> !((!A) -o ((!B) -o 0))"
299  by best_safe
300
301lemma "!( (!((! ((!A) -o B) ) -o 0)) -o 0) \<turnstile>
302        (!A) -o ( (!  ((!B) -o 0)) -o 0)"
303  by best_safe
304
305lemma "!(  (!A) -o ( (!  ((!B) -o 0)) -o 0) ) \<turnstile>
306          (!((! ((!A) -o B) ) -o 0)) -o 0"
307  by best_power
308
309end
310