# HG changeset patch
# User wenzelm
# Date 1164063639 -3600
# Node ID 7c8f4a331f9b3a434b07c1300f507e678f0db267
# Parent  87ac12bed1ab43e936e7be7f13738468b37b8af4
converted legacy ML scripts;

diff -r 87ac12bed1ab -r 7c8f4a331f9b src/Sequents/ILL.ML
--- a/src/Sequents/ILL.ML	Mon Nov 20 23:47:10 2006 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,168 +0,0 @@
-(*  Title:      Sequents/ILL.ML
-    ID:         $Id$
-    Author:     Sara Kalvala and Valeria de Paiva
-    Copyright   1992  University of Cambridge
-*)
-
-val lazy_cs = empty_pack
- add_safes [tensl, conjr, disjl, promote0,
-            context2,context3]
- add_unsafes [identity, zerol, conjll, conjlr, disjrl, disjrr,
-               impr, tensr, impl, derelict, weaken,
-                 promote1, promote2,context1,context4a,context4b];
-
-fun prom_tac n = REPEAT (resolve_tac [promote0,promote1,promote2] n);
-
-fun auto x = prove_goal (the_context ()) x (fn prems => [best_tac lazy_cs 1]);
-
-Goal "$F, $G |- A ==> $F, !(A -o B), $G |- B";
-by (rtac derelict 1);
-by (rtac impl 1);
-by (rtac identity 2);
-by (rtac context1 1);
-by (assume_tac 1);
-qed "aux_impl";
-
-Goal " $F, !A, !B, $G |- C ==> $F, !(A && B), $G |- C";
-by (rtac contract 1);
-by (res_inst_tac [("A","(!A) >< (!B)")] cut 1);
-by (rtac tensr 2);
-by (rtac (auto "! (A && B) |- !A") 3);
-by (rtac (auto "! (A && B) |- !B") 3);
-by (rtac context1 2);
-by (rtac tensl 2);
-by (assume_tac 2);
-by (rtac context3 1);
-by (rtac context3 1);
-by (rtac context1 1);
-qed "conj_lemma";
-
-Goal "!A, !A, $G |- B ==> $G |- (!A) -o B";
-by (rtac impr 1);
-by (rtac contract 1);
-by (assume_tac 1);
-qed "impr_contract";
-
-
-Goal "A, !A, $G |- B ==> $G |- (!A) -o B";
-by (rtac impr 1);
-by (rtac contract 1);
-by (rtac derelict 1);
-by (assume_tac 1);
-qed "impr_contr_der";
-
-val _ = goal (the_context ()) "$F, (!B) -o 0, $G, !B, $H |- A";
-by (rtac impl 1);
-by (rtac identity 3);
-by (rtac context3 1);
-by (rtac context1 1);
-by (rtac zerol 1);
-qed "contrad1";
-
-
-val _ = goal (the_context ()) "$F, !B, $G, (!B) -o 0, $H |- A";
-by (rtac impl 1);
-by (rtac identity 3);
-by (rtac context3 1);
-by (rtac context1 1);
-by (rtac zerol 1);
-qed "contrad2";
-
-val _ = goal (the_context ()) "A -o B, A |- B";
-by (rtac impl 1);
-by (rtac identity 2);
-by (rtac identity 2);
-by (rtac context1 1);
-qed "ll_mp";
-
-Goal "$F, B, $G, $H |- C ==> $F, A, $G, A -o B, $H |- C";
-by (res_inst_tac [("A","B")] cut 1);
-by (rtac ll_mp 2);
-by (assume_tac 2);
-by (rtac context3 1);
-by (rtac context3 1);
-by (rtac context1 1);
-qed "mp_rule1";
-
-Goal "$F, B, $G, $H |- C ==> $F, A -o B, $G, A, $H |- C";
-by (res_inst_tac [("A","B")] cut 1);
-by (rtac ll_mp 2);
-by (assume_tac 2);
-by (rtac context3 1);
-by (rtac context3 1);
-by (rtac context1 1);
-qed "mp_rule2";
-
-val _ = goal (the_context ()) "!((!(A ++ B)) -o 0) |- !( ((!A) -o 0) && ((!B) -o 0))";
-by (best_tac lazy_cs 1);
-qed "or_to_and";
-
-Goal "$F, !( ((!A) -o 0) && ((!B) -o 0)), $G |- C ==> \
-\         $F, !((!(A ++ B)) -o 0), $G |- C";
-by (rtac cut 1);
-by (rtac or_to_and 2);
-by (assume_tac 2);
-by (rtac context3 1);
-by (rtac context1 1);
-qed "o_a_rule";
-
-
-
-val _ = goal (the_context ()) "((!A) -o C) ++ ((!B) -o C) |- (!(A && B)) -o C";
-by (rtac impr 1);
-by (rtac conj_lemma 1);
-by (rtac disjl 1);
-by (ALLGOALS (rtac mp_rule1 THEN' best_tac lazy_cs));
-qed "conj_imp";
-
-
-val not_imp = auto "!A, !((!B) -o 0) |- (!((!A) -o B)) -o 0";
-
-Goal "!A -o (!A -o 0) |- !A -o 0";
-by (rtac impr 1);
-by (rtac contract 1);
-by (rtac impl 1);
-by (rtac identity 3);
-by (rtac context1 1);
-by (best_tac lazy_cs 1);
-qed "a_not_a";
-
-Goal "$J1, !A -o 0, $J2 |- B ==> $J1, !A -o (!A -o 0), $J2 |- B";
-by (res_inst_tac [("A","!A -o 0")] cut 1);
-by (rtac a_not_a 2);
-by (assume_tac 2);
-by (best_tac lazy_cs 1);
-qed "a_not_a_rule";
-
-fun thm_to_rule x y =
-    prove_goal (the_context ()) x
-      (fn [prem] => [(rtac cut 1), (rtac y 2), (rtac prem 2),
-                     (best_tac lazy_cs 1)]);
-
-val safe_cs = lazy_cs add_safes [conj_lemma, ll_mp,contrad1,
-                                 contrad2, mp_rule1, mp_rule2, o_a_rule,
-                                 a_not_a_rule]
-                      add_unsafes [aux_impl];
-
-val power_cs = safe_cs add_unsafes [impr_contr_der];
-
-fun auto1 x = prove_goal (the_context ()) x (fn prems => [best_tac safe_cs 1]) ;
-
-fun auto2 x = prove_goal (the_context ()) x (fn prems => [best_tac power_cs 1]) ;
-
-
-(* some examples from Troelstra and van Dalen
-
-auto1  "!((!A) -o ((!B) -o 0)) |- (!(A && B)) -o 0";
-
-auto1  "!((!(A && B)) -o 0) |- !((!A) -o ((!B) -o 0))";
-
-auto1  "!( (!((! ((!A) -o B) ) -o 0)) -o 0) |- \
-\        (!A) -o ( (!  ((!B) -o 0)) -o 0)";
-
-
-auto2  "!(  (!A) -o ( (!  ((!B) -o 0)) -o 0) ) |- \
-\         (!((! ((!A) -o B) ) -o 0)) -o 0";
-
-
-                                                         *)
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
diff -r 87ac12bed1ab -r 7c8f4a331f9b src/Sequents/ILL_predlog.thy
--- a/src/Sequents/ILL_predlog.thy	Mon Nov 20 23:47:10 2006 +0100
+++ b/src/Sequents/ILL_predlog.thy	Tue Nov 21 00:00:39 2006 +0100
@@ -29,107 +29,102 @@
 (* another translations for linear implication:
   "[* A > B *]" == "!([*A*] -o [*B*])" *)
 
-method_setup auto1 =
-  {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (best_tac safe_cs)) *} ""
-method_setup auto2 =
-  {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (best_tac power_cs)) *} ""
-
 (* from [kleene 52] pp 118,119 *)
 
 lemma k49a: "|- [* A > ( - ( - A)) *]"
-  by auto1
+  by best_safe
 
 lemma k49b: "|- [*( - ( - ( - A))) = ( - A)*]"
-  by auto1
+  by best_safe
 
 lemma k49c: "|- [* (A | - A) > ( - - A = A) *]"
-  by auto1
+  by best_safe
 
 lemma k50a: "|- [* - (A = - A) *]"
-  by auto2
+  by best_power
 
 lemma k51a: "|- [* - - (A | - A) *]"
-  by auto1
+  by best_safe
 
 lemma k51b: "|- [* - - (- - A > A) *]"
-  by auto2
+  by best_power
 
 lemma k56a: "|- [* (A | B) > - (- A & - B) *]"
-  by auto1
+  by best_safe
 
 lemma k56b: "|- [* (-A | B) > - (A & -B) *]"
-  by auto1
+  by best_safe
 
 lemma k57a: "|- [* (A & B) > - (-A | -B) *]"
-  by auto1
+  by best_safe
 
 lemma k57b: "|- [* (A & -B) > -(-A | B) *]"
-  by auto2
+  by best_power
 
 lemma k58a: "|- [* (A > B) > - (A & -B) *]"
-  by auto1
+  by best_safe
 
 lemma k58b: "|- [* (A > -B) = -(A & B) *]"
-  by auto1
+  by best_safe
 
 lemma k58c: "|- [* - (A & B) = (- - A > - B) *]"
-  by auto1
+  by best_safe
 
 lemma k58d: "|- [* (- - A > - B) = - - (-A | -B) *]"
-  by auto1
+  by best_safe
 
 lemma k58e: "! [* - -B > B *] |- [* (- -A > B) = (A > B) *]"
-  by auto1
+  by best_safe
 
 lemma k58f: "! [* - -B > B *] |- [* (A > B) = - (A & -B) *]"
-  by auto1
+  by best_safe
 
 lemma k58g: "|- [* (- -A > B) > - (A & -B) *]"
-  by auto1
+  by best_safe
 
 lemma k59a: "|- [* (-A | B) > (A > B) *]"
-  by auto1
+  by best_safe
 
 lemma k59b: "|- [* (A > B) > - - (-A | B) *]"
-  by auto2
+  by best_power
 
 lemma k59c: "|- [* (-A > B) > - -(A | B) *]"
-  by auto2
+  by best_power
 
 lemma k60a: "|- [* (A & B) > - (A > -B) *]"
-  by auto1
+  by best_safe
 
 lemma k60b: "|- [* (A & -B) > - (A > B) *]"
-  by auto1
+  by best_safe
 
 lemma k60c: "|- [* ( - - A & B) > - (A > -B) *]"
-  by auto1
+  by best_safe
 
 lemma k60d: "|- [* (- - A & - B) = - (A > B) *]"
-  by auto1
+  by best_safe
 
 lemma k60e: "|- [* - (A > B) = - (-A | B) *]"
-  by auto1
+  by best_safe
 
 lemma k60f: "|- [* - (-A | B) = - - (A & -B) *]"
-  by auto1
+  by best_safe
 
 lemma k60g: "|- [* - - (A > B) = - (A & -B) *]"
-  by auto2
+  by best_power
 
 lemma k60h: "|- [* - (A & -B) = (A > - -B) *]"
-  by auto1
+  by best_safe
 
 lemma k60i: "|- [* (A > - -B) = (- -A > - -B) *]"
-  by auto1
+  by best_safe
 
 lemma k61a: "|- [* (A | B) > (-A > B) *]"
-  by auto1
+  by best_safe
 
 lemma k61b: "|- [* - (A | B) = - (-A > B) *]"
-  by auto2
+  by best_power
 
 lemma k62a: "|- [* (-A | -B) > - (A & B) *]"
-  by auto1
+  by best_safe
 
 end
diff -r 87ac12bed1ab -r 7c8f4a331f9b src/Sequents/IsaMakefile
--- a/src/Sequents/IsaMakefile	Mon Nov 20 23:47:10 2006 +0100
+++ b/src/Sequents/IsaMakefile	Tue Nov 21 00:00:39 2006 +0100
@@ -26,7 +26,7 @@
 Pure:
 	@cd $(SRC)/Pure; $(ISATOOL) make Pure
 
-$(OUT)/Sequents: $(OUT)/Pure ILL.ML ILL.thy LK0.thy LK.thy \
+$(OUT)/Sequents: $(OUT)/Pure ILL.thy LK0.thy LK.thy \
   modal.ML ROOT.ML simpdata.ML S4.thy S43.thy Sequents.thy T.thy prover.ML \
   ILL_predlog.thy Washing.thy
 	@$(ISATOOL) usedir -b $(OUT)/Pure Sequents