--- a/src/Sequents/ILL.thy Mon Nov 20 23:47:10 2006 +0100
+++ b/src/Sequents/ILL.thy Tue Nov 21 00:00:39 2006 +0100
@@ -123,6 +123,185 @@
context4b: "$F, $H :=: $G ==> $F, !A, $H :=: $G"
context5: "$F, $G :=: $H ==> $G, $F :=: $H"
-ML {* use_legacy_bindings (the_context ()) *}
+
+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"];
+
+local
+ val promote0 = thm "promote0"
+ val promote1 = thm "promote1"
+ val promote2 = thm "promote2"
+in
+
+fun prom_tac n = REPEAT (resolve_tac [promote0,promote1,promote2] n)
end
+*}
+
+method_setup best_lazy =
+{* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (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 =
+ {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (best_tac safe_cs)) *} ""
+
+method_setup best_power =
+ {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (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