lazy_pack is default context for ILL;
authorwenzelm
Sat Feb 01 18:17:13 2014 +0100 (2014-02-01)
changeset 552327a46672934a3
parent 55231 264d34c19bf2
child 55233 3229614ca9c5
lazy_pack is default context for ILL;
src/Sequents/ILL.thy
src/Sequents/Washing.thy
     1.1 --- a/src/Sequents/ILL.thy	Sat Feb 01 18:07:10 2014 +0100
     1.2 +++ b/src/Sequents/ILL.thy	Sat Feb 01 18:17:13 2014 +0100
     1.3 @@ -124,22 +124,31 @@
     1.4  context4b:    "$F, $H :=: $G ==> $F, !A, $H :=: $G" and
     1.5  context5:     "$F, $G :=: $H ==> $G, $F :=: $H"
     1.6  
     1.7 -
     1.8 -ML {*
     1.9 -  val lazy_pack =
    1.10 -    Cla.put_pack Cla.empty_pack @{context}
    1.11 -    |> fold_rev Cla.add_safe @{thms tensl conjr disjl promote0 context2 context3}
    1.12 -    |> fold_rev Cla.add_unsafe @{thms
    1.13 -      identity zerol conjll conjlr
    1.14 -      disjrl disjrr impr tensr impl
    1.15 -      derelict weaken promote1 promote2
    1.16 -      context1 context4a context4b}
    1.17 -    |> Cla.get_pack;
    1.18 -*}
    1.19 -
    1.20 -method_setup best_lazy = {*
    1.21 -  Scan.succeed (fn ctxt => SIMPLE_METHOD' (Cla.best_tac (Cla.put_pack lazy_pack ctxt)))
    1.22 -*} "lazy classical reasoning"
    1.23 +text "declarations for lazy classical reasoning:"
    1.24 +lemmas [safe] =
    1.25 +  context3
    1.26 +  context2
    1.27 +  promote0
    1.28 +  disjl
    1.29 +  conjr
    1.30 +  tensl
    1.31 +lemmas [unsafe] =
    1.32 +  context4b
    1.33 +  context4a
    1.34 +  context1
    1.35 +  promote2
    1.36 +  promote1
    1.37 +  weaken
    1.38 +  derelict
    1.39 +  impl
    1.40 +  tensr
    1.41 +  impr
    1.42 +  disjrr
    1.43 +  disjrl
    1.44 +  conjlr
    1.45 +  conjll
    1.46 +  zerol
    1.47 +  identity
    1.48  
    1.49  lemma aux_impl: "$F, $G |- A \<Longrightarrow> $F, !(A -o B), $G |- B"
    1.50    apply (rule derelict)
    1.51 @@ -156,14 +165,14 @@
    1.52    prefer 3
    1.53    apply (subgoal_tac "! (A && B) |- !A")
    1.54    apply assumption
    1.55 -  apply best_lazy
    1.56 +  apply best
    1.57    prefer 3
    1.58    apply (subgoal_tac "! (A && B) |- !B")
    1.59    apply assumption
    1.60 -  apply best_lazy
    1.61 +  apply best
    1.62    apply (rule_tac [2] context1)
    1.63    apply (rule_tac [2] tensl)
    1.64 -  prefer 2 apply (assumption)
    1.65 +  prefer 2 apply assumption
    1.66    apply (rule context3)
    1.67    apply (rule context3)
    1.68    apply (rule context1)
    1.69 @@ -225,7 +234,7 @@
    1.70    done
    1.71  
    1.72  lemma or_to_and: "!((!(A ++ B)) -o 0) |- !( ((!A) -o 0) && ((!B) -o 0))"
    1.73 -  by best_lazy
    1.74 +  by best
    1.75  
    1.76  lemma o_a_rule: "$F, !( ((!A) -o 0) && ((!B) -o 0)), $G |- C \<Longrightarrow>
    1.77            $F, !((!(A ++ B)) -o 0), $G |- C"
    1.78 @@ -240,11 +249,11 @@
    1.79    apply (rule impr)
    1.80    apply (rule conj_lemma)
    1.81    apply (rule disjl)
    1.82 -  apply (rule mp_rule1, best_lazy)+
    1.83 +  apply (rule mp_rule1, best)+
    1.84    done
    1.85  
    1.86  lemma not_imp: "!A, !((!B) -o 0) |- (!((!A) -o B)) -o 0"
    1.87 -  by best_lazy
    1.88 +  by best
    1.89  
    1.90  lemma a_not_a: "!A -o (!A -o 0) |- !A -o 0"
    1.91    apply (rule impr)
    1.92 @@ -252,19 +261,19 @@
    1.93    apply (rule impl)
    1.94    apply (rule_tac [3] identity)
    1.95    apply (rule context1)
    1.96 -  apply best_lazy
    1.97 +  apply best
    1.98    done
    1.99  
   1.100  lemma a_not_a_rule: "$J1, !A -o 0, $J2 |- B \<Longrightarrow> $J1, !A -o (!A -o 0), $J2 |- B"
   1.101    apply (rule_tac A = "!A -o 0" in cut)
   1.102    apply (rule_tac [2] a_not_a)
   1.103 -  prefer 2 apply (assumption)
   1.104 -  apply best_lazy
   1.105 +  prefer 2 apply assumption
   1.106 +  apply best
   1.107    done
   1.108  
   1.109  ML {*
   1.110    val safe_pack =
   1.111 -    Cla.put_pack lazy_pack @{context}
   1.112 +    @{context}
   1.113      |> fold_rev Cla.add_safe @{thms conj_lemma ll_mp contrad1
   1.114          contrad2 mp_rule1 mp_rule2 o_a_rule a_not_a_rule}
   1.115      |> Cla.add_unsafe @{thm aux_impl}
   1.116 @@ -276,7 +285,6 @@
   1.117      |> Cla.get_pack;
   1.118  *}
   1.119  
   1.120 -
   1.121  method_setup best_safe =
   1.122    {* Scan.succeed (fn ctxt => SIMPLE_METHOD' (Cla.best_tac (Cla.put_pack safe_pack ctxt))) *}
   1.123  
     2.1 --- a/src/Sequents/Washing.thy	Sat Feb 01 18:07:10 2014 +0100
     2.2 +++ b/src/Sequents/Washing.thy	Sat Feb 01 18:17:13 2014 +0100
     2.3 @@ -40,16 +40,16 @@
     2.4  (* a load of dirty clothes and two dollars gives you clean clothes *)
     2.5  
     2.6  lemma "dollar , dollar , dirty |- clean"
     2.7 -  by (tactic {* Cla.best_tac (Cla.put_pack lazy_pack @{context} |> fold Cla.add_safe @{thms changeI load1I washI dryI}) 1 *})
     2.8 +  by (best add!: changeI load1I washI dryI)
     2.9  
    2.10  (* order of premises doesn't matter *)
    2.11  
    2.12  lemma "dollar , dirty , dollar |- clean"
    2.13 -  by (tactic {* Cla.best_tac (Cla.put_pack lazy_pack @{context} |> fold Cla.add_safe @{thms changeI load1I washI dryI}) 1 *})
    2.14 +  by (best add!: changeI load1I washI dryI)
    2.15  
    2.16  (* alternative formulation *)
    2.17  
    2.18  lemma "dollar , dollar |- dirty -o clean"
    2.19 -  by (tactic {* Cla.best_tac (Cla.put_pack lazy_pack @{context} |> fold Cla.add_safe @{thms changeI load1I washI dryI}) 1 *})
    2.20 +  by (best add!: changeI load1I washI dryI)
    2.21  
    2.22  end