# HG changeset patch
# User wenzelm
# Date 1391275033 -3600
# Node ID 7a46672934a3a0d65fce200a0f69918506dd778f
# Parent  264d34c19bf29d2a47b5131c26e5f91665af6b0a
lazy_pack is default context for ILL;

diff -r 264d34c19bf2 -r 7a46672934a3 src/Sequents/ILL.thy
--- a/src/Sequents/ILL.thy	Sat Feb 01 18:07:10 2014 +0100
+++ b/src/Sequents/ILL.thy	Sat Feb 01 18:17:13 2014 +0100
@@ -124,22 +124,31 @@
 context4b:    "$F, $H :=: $G ==> $F, !A, $H :=: $G" and
 context5:     "$F, $G :=: $H ==> $G, $F :=: $H"
 
-
-ML {*
-  val lazy_pack =
-    Cla.put_pack Cla.empty_pack @{context}
-    |> fold_rev Cla.add_safe @{thms tensl conjr disjl promote0 context2 context3}
-    |> fold_rev Cla.add_unsafe @{thms
-      identity zerol conjll conjlr
-      disjrl disjrr impr tensr impl
-      derelict weaken promote1 promote2
-      context1 context4a context4b}
-    |> Cla.get_pack;
-*}
-
-method_setup best_lazy = {*
-  Scan.succeed (fn ctxt => SIMPLE_METHOD' (Cla.best_tac (Cla.put_pack lazy_pack ctxt)))
-*} "lazy classical reasoning"
+text "declarations for lazy classical reasoning:"
+lemmas [safe] =
+  context3
+  context2
+  promote0
+  disjl
+  conjr
+  tensl
+lemmas [unsafe] =
+  context4b
+  context4a
+  context1
+  promote2
+  promote1
+  weaken
+  derelict
+  impl
+  tensr
+  impr
+  disjrr
+  disjrl
+  conjlr
+  conjll
+  zerol
+  identity
 
 lemma aux_impl: "$F, $G |- A \<Longrightarrow> $F, !(A -o B), $G |- B"
   apply (rule derelict)
@@ -156,14 +165,14 @@
   prefer 3
   apply (subgoal_tac "! (A && B) |- !A")
   apply assumption
-  apply best_lazy
+  apply best
   prefer 3
   apply (subgoal_tac "! (A && B) |- !B")
   apply assumption
-  apply best_lazy
+  apply best
   apply (rule_tac [2] context1)
   apply (rule_tac [2] tensl)
-  prefer 2 apply (assumption)
+  prefer 2 apply assumption
   apply (rule context3)
   apply (rule context3)
   apply (rule context1)
@@ -225,7 +234,7 @@
   done
 
 lemma or_to_and: "!((!(A ++ B)) -o 0) |- !( ((!A) -o 0) && ((!B) -o 0))"
-  by best_lazy
+  by best
 
 lemma o_a_rule: "$F, !( ((!A) -o 0) && ((!B) -o 0)), $G |- C \<Longrightarrow>
           $F, !((!(A ++ B)) -o 0), $G |- C"
@@ -240,11 +249,11 @@
   apply (rule impr)
   apply (rule conj_lemma)
   apply (rule disjl)
-  apply (rule mp_rule1, best_lazy)+
+  apply (rule mp_rule1, best)+
   done
 
 lemma not_imp: "!A, !((!B) -o 0) |- (!((!A) -o B)) -o 0"
-  by best_lazy
+  by best
 
 lemma a_not_a: "!A -o (!A -o 0) |- !A -o 0"
   apply (rule impr)
@@ -252,19 +261,19 @@
   apply (rule impl)
   apply (rule_tac [3] identity)
   apply (rule context1)
-  apply best_lazy
+  apply best
   done
 
 lemma a_not_a_rule: "$J1, !A -o 0, $J2 |- B \<Longrightarrow> $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
+  prefer 2 apply assumption
+  apply best
   done
 
 ML {*
   val safe_pack =
-    Cla.put_pack lazy_pack @{context}
+    @{context}
     |> fold_rev Cla.add_safe @{thms conj_lemma ll_mp contrad1
         contrad2 mp_rule1 mp_rule2 o_a_rule a_not_a_rule}
     |> Cla.add_unsafe @{thm aux_impl}
@@ -276,7 +285,6 @@
     |> Cla.get_pack;
 *}
 
-
 method_setup best_safe =
   {* Scan.succeed (fn ctxt => SIMPLE_METHOD' (Cla.best_tac (Cla.put_pack safe_pack ctxt))) *}
 
diff -r 264d34c19bf2 -r 7a46672934a3 src/Sequents/Washing.thy
--- a/src/Sequents/Washing.thy	Sat Feb 01 18:07:10 2014 +0100
+++ b/src/Sequents/Washing.thy	Sat Feb 01 18:17:13 2014 +0100
@@ -40,16 +40,16 @@
 (* a load of dirty clothes and two dollars gives you clean clothes *)
 
 lemma "dollar , dollar , dirty |- clean"
-  by (tactic {* Cla.best_tac (Cla.put_pack lazy_pack @{context} |> fold Cla.add_safe @{thms changeI load1I washI dryI}) 1 *})
+  by (best add!: changeI load1I washI dryI)
 
 (* order of premises doesn't matter *)
 
 lemma "dollar , dirty , dollar |- clean"
-  by (tactic {* Cla.best_tac (Cla.put_pack lazy_pack @{context} |> fold Cla.add_safe @{thms changeI load1I washI dryI}) 1 *})
+  by (best add!: changeI load1I washI dryI)
 
 (* alternative formulation *)
 
 lemma "dollar , dollar |- dirty -o clean"
-  by (tactic {* Cla.best_tac (Cla.put_pack lazy_pack @{context} |> fold Cla.add_safe @{thms changeI load1I washI dryI}) 1 *})
+  by (best add!: changeI load1I washI dryI)
 
 end