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