diff -r 87ac12bed1ab -r 7c8f4a331f9b src/Sequents/ILL.thy
--- 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