(* Title: Sequents/ILL.thy Author: Sara Kalvala and Valeria de Paiva Copyright 1995 University of Cambridge *) theory ILL imports Sequents begin consts Trueprop :: "two_seqi" tens :: "[o, o] => o" (infixr "><" 35) limp :: "[o, o] => o" (infixr "-o" 45) liff :: "[o, o] => o" (infixr "o-o" 45) FShriek :: "o => o" ("! _" [100] 1000) lconj :: "[o, o] => o" (infixr "&&" 35) ldisj :: "[o, o] => o" (infixr "++" 35) zero :: "o" ("0") top :: "o" ("1") eye :: "o" ("I") aneg :: "o=>o" ("~_") (* context manipulation *) Context :: "two_seqi" (* promotion rule *) PromAux :: "three_seqi" syntax "_Trueprop" :: "single_seqe" ("((_)/ |- (_))" [6,6] 5) "_Context" :: "two_seqe" ("((_)/ :=: (_))" [6,6] 5) "_PromAux" :: "three_seqe" ("promaux {_||_||_}") parse_translation {* [(@{syntax_const "_Trueprop"}, single_tr @{const_syntax Trueprop}), (@{syntax_const "_Context"}, two_seq_tr @{const_syntax Context}), (@{syntax_const "_PromAux"}, three_seq_tr @{const_syntax PromAux})] *} print_translation {* [(@{const_syntax Trueprop}, single_tr' @{syntax_const "_Trueprop"}), (@{const_syntax Context}, two_seq_tr' @{syntax_const "_Context"}), (@{const_syntax PromAux}, three_seq_tr' @{syntax_const "_PromAux"})] *} defs liff_def: "P o-o Q == (P -o Q) >< (Q -o P)" aneg_def: "~A == A -o 0" axioms identity: "P |- P" zerol: "$G, 0, $H |- A" (* RULES THAT DO NOT DIVIDE CONTEXT *) derelict: "$F, A, $G |- C ==> $F, !A, $G |- C" (* unfortunately, this one removes !A *) contract: "$F, !A, !A, $G |- C ==> $F, !A, $G |- C" weaken: "$F, $G |- C ==> $G, !A, $F |- C" (* weak form of weakening, in practice just to clean context *) (* weaken and contract not needed (CHECK) *) promote2: "promaux{ || $H || B} ==> $H |- !B" promote1: "promaux{!A, $G || $H || B} ==> promaux {$G || $H, !A || B}" promote0: "$G |- A ==> promaux {$G || || A}" tensl: "$H, A, B, $G |- C ==> $H, A >< B, $G |- C" impr: "A, $F |- B ==> $F |- A -o B" conjr: "[| $F |- A ; $F |- B |] ==> $F |- (A && B)" conjll: "$G, A, $H |- C ==> $G, A && B, $H |- C" conjlr: "$G, B, $H |- C ==> $G, A && B, $H |- C" disjrl: "$G |- A ==> $G |- A ++ B" disjrr: "$G |- B ==> $G |- A ++ B" disjl: "[| $G, A, $H |- C ; $G, B, $H |- C |] ==> $G, A ++ B, $H |- C" (* RULES THAT DIVIDE CONTEXT *) tensr: "[| $F, $J :=: $G; $F |- A ; $J |- B |] ==> $G |- A >< B" impl: "[| $G, $F :=: $J, $H ; B, $F |- C ; $G |- A |] ==> $J, A -o B, $H |- C" cut: " [| $J1, $H1, $J2, $H3, $J3, $H2, $J4, $H4 :=: $F ; $H1, $H2, $H3, $H4 |- A ; $J1, $J2, A, $J3, $J4 |- B |] ==> $F |- B" (* CONTEXT RULES *) context1: "$G :=: $G" context2: "$F, $G :=: $H, !A, $G ==> $F, A, $G :=: $H, !A, $G" context3: "$F, $G :=: $H, $J ==> $F, A, $G :=: $H, A, $J" context4a: "$F :=: $H, $G ==> $F :=: $H, !A, $G" context4b: "$F, $H :=: $G ==> $F, !A, $H :=: $G" context5: "$F, $G :=: $H ==> $G, $F :=: $H" ML {* val lazy_cs = empty_pack add_safes [@{thm tensl}, @{thm conjr}, @{thm disjl}, @{thm promote0}, @{thm context2}, @{thm context3}] add_unsafes [@{thm identity}, @{thm zerol}, @{thm conjll}, @{thm conjlr}, @{thm disjrl}, @{thm disjrr}, @{thm impr}, @{thm tensr}, @{thm impl}, @{thm derelict}, @{thm weaken}, @{thm promote1}, @{thm promote2}, @{thm context1}, @{thm context4a}, @{thm context4b}]; fun prom_tac n = REPEAT (resolve_tac [@{thm promote0}, @{thm promote1}, @{thm promote2}] n) *} method_setup best_lazy = {* Scan.succeed (K (SIMPLE_METHOD' (best_tac lazy_cs))) *} "lazy classical reasoning" lemma aux_impl: "$F, $G |- A ==> $F, !(A -o B), $G |- B" apply (rule derelict) apply (rule impl) apply (rule_tac [2] identity) apply (rule context1) apply assumption done lemma conj_lemma: " $F, !A, !B, $G |- C ==> $F, !(A && B), $G |- C" apply (rule contract) apply (rule_tac A = " (!A) >< (!B) " in cut) apply (rule_tac [2] tensr) prefer 3 apply (subgoal_tac "! (A && B) |- !A") apply assumption apply best_lazy prefer 3 apply (subgoal_tac "! (A && B) |- !B") apply assumption apply best_lazy apply (rule_tac [2] context1) apply (rule_tac [2] tensl) prefer 2 apply (assumption) apply (rule context3) apply (rule context3) apply (rule context1) done lemma impr_contract: "!A, !A, $G |- B ==> $G |- (!A) -o B" apply (rule impr) apply (rule contract) apply assumption done lemma impr_contr_der: "A, !A, $G |- B ==> $G |- (!A) -o B" apply (rule impr) apply (rule contract) apply (rule derelict) apply assumption done lemma contrad1: "$F, (!B) -o 0, $G, !B, $H |- A" apply (rule impl) apply (rule_tac [3] identity) apply (rule context3) apply (rule context1) apply (rule zerol) done lemma contrad2: "$F, !B, $G, (!B) -o 0, $H |- A" apply (rule impl) apply (rule_tac [3] identity) apply (rule context3) apply (rule context1) apply (rule zerol) done lemma ll_mp: "A -o B, A |- B" apply (rule impl) apply (rule_tac [2] identity) apply (rule_tac [2] identity) apply (rule context1) done lemma mp_rule1: "$F, B, $G, $H |- C ==> $F, A, $G, A -o B, $H |- C" apply (rule_tac A = "B" in cut) apply (rule_tac [2] ll_mp) prefer 2 apply (assumption) apply (rule context3) apply (rule context3) apply (rule context1) done lemma mp_rule2: "$F, B, $G, $H |- C ==> $F, A -o B, $G, A, $H |- C" apply (rule_tac A = "B" in cut) apply (rule_tac [2] ll_mp) prefer 2 apply (assumption) apply (rule context3) apply (rule context3) apply (rule context1) done lemma or_to_and: "!((!(A ++ B)) -o 0) |- !( ((!A) -o 0) && ((!B) -o 0))" by best_lazy lemma o_a_rule: "$F, !( ((!A) -o 0) && ((!B) -o 0)), $G |- C ==> $F, !((!(A ++ B)) -o 0), $G |- C" apply (rule cut) apply (rule_tac [2] or_to_and) prefer 2 apply (assumption) apply (rule context3) apply (rule context1) done lemma conj_imp: "((!A) -o C) ++ ((!B) -o C) |- (!(A && B)) -o C" apply (rule impr) apply (rule conj_lemma) apply (rule disjl) apply (rule mp_rule1, best_lazy)+ done lemma not_imp: "!A, !((!B) -o 0) |- (!((!A) -o B)) -o 0" by best_lazy lemma a_not_a: "!A -o (!A -o 0) |- !A -o 0" apply (rule impr) apply (rule contract) apply (rule impl) apply (rule_tac [3] identity) apply (rule context1) apply best_lazy done lemma a_not_a_rule: "$J1, !A -o 0, $J2 |- B ==> $J1, !A -o (!A -o 0), $J2 |- B" apply (rule_tac A = "!A -o 0" in cut) apply (rule_tac [2] a_not_a) prefer 2 apply (assumption) apply best_lazy done ML {* val safe_cs = lazy_cs add_safes [@{thm conj_lemma}, @{thm ll_mp}, @{thm contrad1}, @{thm contrad2}, @{thm mp_rule1}, @{thm mp_rule2}, @{thm o_a_rule}, @{thm a_not_a_rule}] add_unsafes [@{thm aux_impl}]; val power_cs = safe_cs add_unsafes [@{thm impr_contr_der}]; *} method_setup best_safe = {* Scan.succeed (K (SIMPLE_METHOD' (best_tac safe_cs))) *} "" method_setup best_power = {* Scan.succeed (K (SIMPLE_METHOD' (best_tac power_cs))) *} "" (* Some examples from Troelstra and van Dalen *) lemma "!((!A) -o ((!B) -o 0)) |- (!(A && B)) -o 0" by best_safe lemma "!((!(A && B)) -o 0) |- !((!A) -o ((!B) -o 0))" by best_safe lemma "!( (!((! ((!A) -o B) ) -o 0)) -o 0) |- (!A) -o ( (! ((!B) -o 0)) -o 0)" by best_safe lemma "!( (!A) -o ( (! ((!B) -o 0)) -o 0) ) |- (!((! ((!A) -o B) ) -o 0)) -o 0" by best_power end