New unified treatment of sequent calculi by Sara Kalvala
combines the old LK and Modal with the new ILL (Int. Linear Logic)

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Sequents/ILL.ML	Wed Oct 09 13:32:33 1996 +0200
@@ -0,0 +1,140 @@
+(*  Title:      Sequents/ILL.ML
+    ID:         $Id$
+    Author:     Sara Kalvala and Valeria de Paiva
+    Copyright   1992  University of Cambridge
+
+*)
+
+open ILL;
+
+
+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 thy x (fn prems => [best_tac lazy_cs 1]);
+
+val aux_impl = prove_goal thy "$F, $G |- A ==> $F, !(A -o B), $G |- B"
+(fn prems => [rtac derelict 1 THEN rtac impl 1 THEN rtac identity 2
+	THEN rtac context1 1 THEN rtac (hd(prems)) 1]);
+
+val conj_lemma =
+prove_goal thy " $F, !A, !B, $G |- C ==> $F, !(A && B), $G |- C"
+(fn prems => [rtac contract 1,
+	res_inst_tac [("A","(!A) >< (!B)")] cut 1,
+	rtac tensr 2,
+	rtac (auto "! (A && B) |- !A") 3,
+	rtac (auto "! (A && B) |- !B") 3,
+	rtac context1 2,
+	rtac tensl 2,
+	rtac (hd(prems)) 2,
+	rtac context3 1,
+	rtac context3 1,
+	rtac context1 1]);
+
+val impr_contract =
+prove_goal thy "!A, !A, $G |- B ==> $G |- (!A) -o B"
+(fn prems => [rtac impr 1 THEN rtac contract 1
+		 THEN rtac (hd(prems)) 1]);
+
+
+val impr_contr_der =
+prove_goal thy "A, !A, $G |- B ==> $G |- (!A) -o B"
+(fn prems => [rtac impr 1 THEN rtac contract 1 THEN rtac derelict 1
+		 THEN rtac (hd(prems)) 1]);
+
+val contrad1 =
+prove_goal thy "$F, (!B) -o 0, $G, !B, $H |- A"
+(fn _ => [rtac impl 1,rtac identity 3,rtac context3 1,rtac context1 1,
+	  rtac zerol 1]);
+
+
+val contrad2 =
+prove_goal thy "$F, !B, $G, (!B) -o 0, $H |- A"
+(fn _ => [rtac impl 1,rtac identity 3,rtac context3 1,rtac context1 1,
+	  rtac zerol 1]);
+
+val ll_mp =
+prove_goal thy "A -o B, A |- B"
+(fn _ => [rtac impl 1 THEN rtac identity 2 THEN rtac identity 2
+	 THEN rtac context1 1]);
+
+val mp_rule1 =
+prove_goal thy "$F, B, $G, $H |- C ==> $F, A, $G, A -o B, $H |- C"
+(fn prems => [res_inst_tac [("A","B")] cut 1, rtac ll_mp 2,
+		rtac (hd(prems)) 2, rtac context3 1, rtac context3 1,
+		rtac context1 1]);
+
+val mp_rule2 =
+prove_goal thy "$F, B, $G, $H |- C ==> $F, A -o B, $G, A, $H |- C"
+(fn prems => [res_inst_tac [("A","B")] cut 1, rtac ll_mp 2,
+		rtac (hd(prems)) 2, rtac context3 1, rtac context3 1,
+		rtac context1 1]);
+
+val or_to_and =
+prove_goal thy "!((!(A ++ B)) -o 0) |- !( ((!A) -o 0) && ((!B) -o 0))"
+(fn _ => [best_tac lazy_cs 1]);
+
+val o_a_rule =
+prove_goal thy "$F, !( ((!A) -o 0) && ((!B) -o 0)), $G |- C ==> \
+\         $F, !((!(A ++ B)) -o 0), $G |- C"
+(fn prems => [rtac cut 1, rtac or_to_and 2, rtac (hd(prems)) 2,
+		rtac context3 1, rtac context1 1]);
+
+
+
+val conj_imp =
+ prove_goal thy "((!A) -o C) ++ ((!B) -o C) |- (!(A && B)) -o C"
+(fn _ => [rtac impr 1,rtac conj_lemma 1, rtac disjl 1,
+	  ALLGOALS (rtac mp_rule1 THEN' best_tac lazy_cs)]);
+
+
+val not_imp = auto "!A, !((!B) -o 0) |- (!((!A) -o B)) -o 0";
+
+val a_not_a =
+prove_goal thy "!A -o (!A -o 0) |- !A -o 0"
+     (fn _ => [rtac impr 1, rtac contract 1, rtac impl 1,
+	  rtac context1 1 THEN rtac identity 2, best_tac lazy_cs 1]);
+
+val a_not_a_rule =
+prove_goal thy "$J1, !A -o 0, $J2 |- B ==> $J1, !A -o (!A -o 0), $J2 |- B"
+ (fn prems => [res_inst_tac [("A","!A -o 0")] cut 1,
+               rtac a_not_a 2 THEN rtac (hd(prems)) 2
+		 THEN best_tac lazy_cs 1]);
+
+fun thm_to_rule x y =
+prove_goal thy x (fn prems => [rtac cut 1, rtac y 2, rtac (hd(prems)) 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 thy x (fn prems => [best_tac safe_cs 1]) ;
+
+fun auto2 x = prove_goal thy 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";
+
+
+                                                         *)

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Sequents/ILL.thy	Wed Oct 09 13:32:33 1996 +0200
@@ -0,0 +1,134 @@
+(*  Title:      ILL.thy
+    ID:         $Id$
+    Author:     Sara Kalvala and Valeria de Paiva
+    Copyright   1995  University of Cambridge
+*)
+
+
+ILL = Sequents +
+
+consts
+
+  
+ Trueprop	:: "two_seqi"
+ "@Trueprop"	:: "single_seqe" ("((_)/ |- (_))" [6,6] 5)
+ 
+ 
+
+"><"    ::"[o, o] => o"        (infixr 35)
+"-o"    ::"[o, o] => o"        (infixr 45)
+"o-o"   ::"[o, o] => o"        (infixr 45)
+FShriek ::"o => o"             ("! _" [100] 1000)
+"&&"    ::"[o, o] => o"        (infixr 35)
+"++"    ::"[o, o] => o"        (infixr 35)
+zero    ::"o"                  ("0")
+top     ::"o"                  ("1")
+eye     ::"o"                  ("I")
+aneg    ::"o=>o"               ("~_")
+
+
+  (* syntax for context manipulation *)
+
+ Context      :: "two_seqi"
+"@Context"    :: "two_seqe"   ("((_)/ :=: (_))" [6,6] 5)
+
+  (* syntax for promotion rule *)
+
+  PromAux :: "three_seqi"
+"@PromAux":: "three_seqe" ("promaux {_||_||_}")
+
+defs
+
+liff_def        "P o-o Q == (P -o Q) >< (Q -o P)"
+
+aneg_def        "~A == A -o 0"
+
+
+
+
+rules
+  
+identity        "P |- P"
+
+zerol           "$G, 0, $H |- A"
+
+  (* RULES THAT DO NOT DIVIDE CONTEXT *)
+
+derelict   "$F, A, $G |- C ==> $F, !A, $G |- C"
+  (* unfortunately, this one removes !A  *)
+
+contract  "$F, !A, !A, $G |- C ==> $F, !A, $G |- C"
+  
+weaken     "$F, $G |- C ==> $G, !A, $F |- C"
+  (* weak form of weakening, in practice just to clean context *)
+  (* weaken and contract not needed (CHECK)  *)
+
+promote2        "promaux{ || $H || B} ==> $H |- !B"
+promote1        "promaux{!A, $G || $H || B}
+                 ==> promaux {$G || $H, !A || B}"
+promote0        "$G |- A ==> promaux {$G || || A}"
+
+
+  
+tensl     "$H, A, B, $G |- C ==> $H, A >< B, $G |- C"
+
+impr      "A, $F |- B ==> $F |- A -o B"
+
+conjr           "[| $F |- A ;
+                 $F |- B |]
+                ==> $F |- (A && B)"
+
+conjll          "$G, A, $H |- C ==> $G, A && B, $H |- C"
+
+conjlr          "$G, B, $H |- C ==> $G, A && B, $H |- C"
+
+disjrl          "$G |- A ==> $G |- A ++ B"
+disjrr          "$G |- B ==> $G |- A ++ B"
+disjl           "[| $G, A, $H |- C ;
+                    $G, B, $H |- C |]
+                ==> $G, A ++ B, $H |- C"
+
+
+      (* RULES THAT DIVIDE CONTEXT *)
+
+tensr           "[| $F, $J :=: $G;
+                    $F |- A ;
+                    $J |- B     |]
+                    ==> $G |- A >< B"
+
+impl            "[| $G, $F :=: $J, $H ;
+                    B, $F |- C ;
+                       $G |- A |]
+                    ==> $J, A -o B, $H |- C"
+
+    
+cut " [| $J1, $H1, $J2, $H3, $J3, $H2, $J4, $H4 :=: $F ;
+         $H1, $H2, $H3, $H4 |- A ;
+         $J1, $J2, A, $J3, $J4 |- B |]  ==> $F |- B"
+
+
+  (* CONTEXT RULES *)
+
+context1     "$G :=: $G"
+context2     "$F, $G :=: $H, !A, $G ==> $F, A, $G :=: $H, !A, $G"
+context3     "$F, $G :=: $H, $J ==> $F, A, $G :=: $H, A, $J"
+context4a    "$F :=: $H, $G ==> $F :=: $H, !A, $G"
+context4b    "$F, $H :=: $G ==> $F, !A, $H :=: $G"
+context5     "$F, $G :=: $H ==> $G, $F :=: $H"
+
+
+
+ 
+end
+
+ML
+
+val parse_translation = [("@Trueprop",Sequents.single_tr "Trueprop"),
+                         ("@Context",Sequents.two_seq_tr "Context"),
+                         ("@PromAux", Sequents.three_seq_tr "PromAux")];
+
+val print_translation = [("Trueprop",Sequents.single_tr' "@Trueprop"),
+                         ("Context",Sequents.two_seq_tr'"@Context"),
+                         ("PromAux", Sequents.three_seq_tr'"@PromAux")];
+
+ 

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Sequents/LK.ML	Wed Oct 09 13:32:33 1996 +0200
@@ -0,0 +1,82 @@
+(*  Title:      LK/LK.ML
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1992  University of Cambridge
+
+Tactics and lemmas for lk.thy (thanks also to Philippe de Groote)  
+*)
+
+open LK;
+
+(*Higher precedence than := facilitates use of references*)
+infix 4 add_safes add_unsafes;
+
+(*Cut and thin, replacing the right-side formula*)
+fun cutR_tac (sP: string) i = 
+    res_inst_tac [ ("P",sP) ] cut i  THEN  rtac thinR i;
+
+(*Cut and thin, replacing the left-side formula*)
+fun cutL_tac (sP: string) i = 
+    res_inst_tac [ ("P",sP) ] cut i  THEN  rtac thinL (i+1);
+
+
+(** If-and-only-if rules **)
+qed_goalw "iffR" LK.thy [iff_def]
+    "[| $H,P |- $E,Q,$F;  $H,Q |- $E,P,$F |] ==> $H |- $E, P <-> Q, $F"
+ (fn prems=> [ (REPEAT (resolve_tac (prems@[conjR,impR]) 1)) ]);
+
+qed_goalw "iffL" LK.thy [iff_def]
+   "[| $H,$G |- $E,P,Q;  $H,Q,P,$G |- $E |] ==> $H, P <-> Q, $G |- $E"
+ (fn prems=> [ (REPEAT (resolve_tac (prems@[conjL,impL,basic]) 1)) ]);
+
+qed_goalw "TrueR" LK.thy [True_def]
+    "$H |- $E, True, $F"
+ (fn _=> [ rtac impR 1, rtac basic 1 ]);
+
+
+(** Weakened quantifier rules.  Incomplete, they let the search terminate.**)
+
+qed_goal "allL_thin" LK.thy 
+    "$H, P(x), $G |- $E ==> $H, ALL x.P(x), $G |- $E"
+ (fn prems=> [ (rtac allL 1), (rtac thinL 1), (resolve_tac prems 1) ]);
+
+qed_goal "exR_thin" LK.thy 
+    "$H |- $E, P(x), $F ==> $H |- $E, EX x.P(x), $F"
+ (fn prems=> [ (rtac exR 1), (rtac thinR 1), (resolve_tac prems 1) ]);
+
+(* Symmetry of equality in hypotheses *)
+qed_goal "symL" LK.thy 
+    "$H, $G, B = A |- $E ==> $H, A = B, $G |- $E" 
+ (fn prems=>
+  [ (rtac cut 1),
+    (rtac thinL 2),
+    (resolve_tac prems 2),
+    (resolve_tac [basic RS sym] 1) ]);
+
+
+
+
+(*The rules of LK*)
+val prop_pack = empty_pack add_safes 
+                [basic, refl, conjL, conjR, disjL, disjR, impL, impR, 
+                 notL, notR, iffL, iffR];
+
+val LK_pack = prop_pack add_safes   [allR, exL] 
+                        add_unsafes [allL_thin, exR_thin];
+
+val LK_dup_pack = prop_pack add_safes   [allR, exL] 
+                            add_unsafes [allL, exR];
+
+
+
+(** Contraction.  Useful since some rules are not complete. **)
+
+qed_goal "conR" LK.thy 
+    "$H |- $E, P, $F, P ==> $H |- $E, P, $F"
+ (fn prems=>
+  [ (rtac cut 1), (REPEAT (resolve_tac (prems@[basic]) 1)) ]);
+
+qed_goal "conL" LK.thy 
+    "$H, P, $G, P |- $E ==> $H, P, $G |- $E"
+ (fn prems=>
+  [ (rtac cut 1), (REPEAT (resolve_tac (prems@[basic]) 1)) ]);

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Sequents/LK.thy	Wed Oct 09 13:32:33 1996 +0200
@@ -0,0 +1,84 @@
+(*  Title:      LK/lk.thy
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1993  University of Cambridge
+
+Classical First-Order Sequent Calculus
+
+There may be printing problems if a seqent is in expanded normal form
+	(eta-expanded, beta-contracted)
+*)
+
+LK = Sequents +
+
+
+consts
+
+ Trueprop	:: "two_seqi"
+ "@Trueprop"	:: "two_seqe" ("((_)/ |- (_))" [6,6] 5)
+
+
+  True,False   :: o
+  "="          :: ['a,'a] => o       (infixl 50)
+  Not          :: o => o             ("~ _" [40] 40)
+  "&"          :: [o,o] => o         (infixr 35)
+  "|"          :: [o,o] => o         (infixr 30)
+  "-->","<->"  :: [o,o] => o         (infixr 25)
+  The          :: ('a => o) => 'a    (binder "THE " 10)
+  All          :: ('a => o) => o     (binder "ALL " 10)
+  Ex           :: ('a => o) => o     (binder "EX " 10)
+
+rules
+  (*Structural rules*)
+
+  basic "$H, P, $G |- $E, P, $F"
+
+  thinR "$H |- $E, $F ==> $H |- $E, P, $F"
+  thinL "$H, $G |- $E ==> $H, P, $G |- $E"
+
+  cut   "[| $H |- $E, P;  $H, P |- $E |] ==> $H |- $E"
+
+  (*Propositional rules*)
+
+  conjR "[| $H|- $E, P, $F;  $H|- $E, Q, $F |] ==> $H|- $E, P&Q, $F"
+  conjL "$H, P, Q, $G |- $E ==> $H, P & Q, $G |- $E"
+
+  disjR "$H |- $E, P, Q, $F ==> $H |- $E, P|Q, $F"
+  disjL "[| $H, P, $G |- $E;  $H, Q, $G |- $E |] ==> $H, P|Q, $G |- $E"
+
+  impR  "$H, P |- $E, Q, $F ==> $H |- $E, P-->Q, $F"
+  impL  "[| $H,$G |- $E,P;  $H, Q, $G |- $E |] ==> $H, P-->Q, $G |- $E"
+
+  notR  "$H, P |- $E, $F ==> $H |- $E, ~P, $F"
+  notL  "$H, $G |- $E, P ==> $H, ~P, $G |- $E"
+
+  FalseL "$H, False, $G |- $E"
+
+  True_def "True == False-->False"
+  iff_def  "P<->Q == (P-->Q) & (Q-->P)"
+
+  (*Quantifiers*)
+
+  allR  "(!!x.$H |- $E, P(x), $F) ==> $H |- $E, ALL x.P(x), $F"
+  allL  "$H, P(x), $G, ALL x.P(x) |- $E ==> $H, ALL x.P(x), $G |- $E"
+
+  exR   "$H |- $E, P(x), $F, EX x.P(x) ==> $H |- $E, EX x.P(x), $F"
+  exL   "(!!x.$H, P(x), $G |- $E) ==> $H, EX x.P(x), $G |- $E"
+
+  (*Equality*)
+
+  refl  "$H |- $E, a=a, $F"
+  sym   "$H |- $E, a=b, $F ==> $H |- $E, b=a, $F"
+  trans "[| $H|- $E, a=b, $F;  $H|- $E, b=c, $F |] ==> $H|- $E, a=c, $F"
+
+
+  (*Descriptions*)
+
+  The "[| $H |- $E, P(a), $F;  !!x.$H, P(x) |- $E, x=a, $F |] ==> 
+          $H |- $E, P(THE x.P(x)), $F"
+end
+
+  ML
+
+val parse_translation = [("@Trueprop",Sequents.two_seq_tr "Trueprop")];
+val print_translation = [("Trueprop",Sequents.two_seq_tr' "@Trueprop")];

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Sequents/Makefile	Wed Oct 09 13:32:33 1996 +0200
@@ -0,0 +1,72 @@
+# $Id$
+#########################################################################
+#									#
+# 			Makefile for Isabelle (Sequents)		#
+#									#
+#########################################################################
+
+#To make the system, cd to this directory and type
+#	make
+#To make the system and test it on standard examples, type 
+#	make test
+#To generate HTML files for every theory, set the environment variable
+#MAKE_HTML or add the parameter "MAKE_HTML=".
+
+#Environment variable ISABELLECOMP specifies the compiler.
+#Environment variable ISABELLEBIN specifies the destination directory.
+#For Poly/ML, ISABELLEBIN must begin with a /
+
+#Makes Pure if this file is ABSENT -- but not 
+#if it is out of date, since this Makefile does not know its dependencies!
+
+BIN = $(ISABELLEBIN)
+COMP = $(ISABELLECOMP)
+NAMES = ILL LK S4 S43 T
+FILES = ROOT.ML Sequents.thy prover.ML $(NAMES:%=%.thy) $(NAMES:%=%.ML)
+
+ILL_NAMES = ILL_predlog washing 
+EX_FILES = ex/ROOT.ML \
+    ex/LK/ROOT.ML ex/LK/hardquant.ML ex/LK/prop.ML ex/LK/quant.ML \
+    ex/Modal/ROOT.ML ex/Modal/S43thms.ML ex/Modal/S4thms.ML ex/Modal/Tthms.ML \
+    ex/ILL/ILL_kleene_lemmas.ML \
+    $(ILL_NAMES:%=ex/ILL/%.thy) $(ILL_NAMES:%=ex/ILL/%.ML)
+
+$(BIN)/Sequents:   $(BIN)/Pure  $(FILES) 
+	case "$(COMP)" in \
+	poly*)	echo 'make_database"$(BIN)/Sequents"; quit();'  \
+			| $(COMP) $(BIN)/Pure;\
+                if [ "$${MAKE_HTML}" = "true" ]; \
+                then echo 'open PolyML; make_html := true; exit_use_dir".";' \
+                       | $(COMP) $(BIN)/Sequents;\
+		elif [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
+                then echo 'open PolyML; make_html := true; exit_use_dir".";                               make_html := false;' | $(COMP) $(BIN)/Sequents;\
+                else echo 'open PolyML; exit_use_dir".";' | $(COMP) $(BIN)/Sequents;\
+                fi;\
+		discgarb -c $(BIN)/Sequents;;\
+	sml*)	if [ "$${MAKE_HTML}" = "true" ]; \
+                then echo 'make_html := true; exit_use_dir".";                                            xML"$(BIN)/Sequents" banner;' | $(BIN)/Pure;\
+                elif [ "$${MAKE_HTML-undefined}" != "undefined" ];\
+                then echo 'make_html := true; exit_use_dir".";                                            make_html := false; xML"$(BIN)/Sequents" banner;' \
+                       | $(BIN)/Pure;\
+                else echo 'exit_use_dir"."; xML"$(BIN)/Sequents" banner;' \
+                       | $(BIN)/Pure;\
+                fi;;\
+	*)	echo Bad value for ISABELLECOMP: \
+                	$(COMP) is not poly or sml;;\
+	esac
+
+$(BIN)/Pure:
+	cd ../Pure;  $(MAKE)
+
+test:   $(BIN)/Sequents  $(EX_FILES)
+	case "$(COMP)" in \
+	poly*)	echo 'exit_use"ex/ROOT.ML";quit();' | $(COMP) $(BIN)/Sequents;;\
+	sml*)	echo 'exit_use"ex/ROOT.ML";' | $(BIN)/Sequents;;\
+	*)	echo Bad value for ISABELLECOMP: \
+                	$(COMP) is not poly or sml;;\
+	esac
+
+
+
+
+.PRECIOUS:  $(BIN)/Pure $(BIN)/Sequents 

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Sequents/Modal0.ML	Wed Oct 09 13:32:33 1996 +0200
@@ -0,0 +1,30 @@
+(*  Title:      Modal/modal0
+    ID:         $Id$
+    Author:     Martin Coen
+    Copyright   1991  University of Cambridge
+*)
+
+structure Modal0_rls = 
+struct
+
+val rewrite_rls = [Modal0.strimp_def,Modal0.streqv_def];
+
+local
+  val iffR = prove_goal thy 
+      "[| $H,P |- $E,Q,$F;  $H,Q |- $E,P,$F |] ==> $H |- $E, P <-> Q, $F"
+   (fn prems=>
+    [ (rewtac iff_def),
+      (REPEAT (resolve_tac (prems@[conjR,impR]) 1)) ]);
+
+  val iffL = prove_goal thy 
+     "[| $H,$G |- $E,P,Q;  $H,Q,P,$G |- $E |] ==> $H, P <-> Q, $G |- $E"
+   (fn prems=>
+    [ rewtac iff_def,
+      (REPEAT (resolve_tac (prems@[conjL,impL,basic]) 1)) ])
+in
+val safe_rls   = [basic,conjL,conjR,disjL,disjR,impL,impR,notL,notR,iffL,iffR];
+val unsafe_rls = [allR,exL];
+val bound_rls  = [allL,exR];
+end
+
+end;

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Sequents/Modal0.thy	Wed Oct 09 13:32:33 1996 +0200
@@ -0,0 +1,40 @@
+(*  Title:      Modal/modal0
+    ID:         $Id$
+    Author:     Martin Coen
+    Copyright   1991  University of Cambridge
+*)
+
+Modal0 = LK +
+
+consts
+  box           :: "o=>o"       ("[]_" [50] 50)
+  dia           :: "o=>o"       ("<>_" [50] 50)
+  "--<",">-<"   :: "[o,o]=>o"   (infixr 25)
+  "@Lstar"      :: "two_seqe"   ("(_)|L>(_)" [6,6] 5)
+  "@Rstar"      :: "two_seqe"   ("(_)|R>(_)" [6,6] 5)
+  Lstar,Rstar   :: "two_seqi"
+
+rules
+  (* Definitions *)
+
+  strimp_def    "P --< Q == [](P --> Q)"
+  streqv_def    "P >-< Q == (P --< Q) & (Q --< P)"
+end
+
+ML
+
+local
+
+  val Lstar = "Lstar";
+  val Rstar = "Rstar";
+  val SLstar = "@Lstar";
+  val SRstar = "@Rstar";
+
+  fun star_tr c [s1,s2] =
+      Const(c,dummyT)$Sequents.seq_tr s1$Sequents.seq_tr s2;
+  fun star_tr' c [s1,s2] = 
+      Const(c,dummyT) $ Sequents.seq_tr' s1 $ Sequents.seq_tr' s2;
+in
+val parse_translation = [(SLstar,star_tr Lstar), (SRstar,star_tr Rstar)];
+val print_translation = [(Lstar,star_tr' SLstar), (Rstar,star_tr' SRstar)]
+end;

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Sequents/README.html	Wed Oct 09 13:32:33 1996 +0200
@@ -0,0 +1,67 @@
+<!-- $Id$ -->
+<HTML><HEAD><TITLE>Sequents/ReadMe</TITLE></HEAD><BODY>
+
+<H2>Sequents: Various Sequent Calculi</H2>
+
+This directory contains the Standard ML sources of the Isabelle system for
+various Sequent, Linear, and Modal Logic.  Important files include
+
+<DL>
+<DT>ROOT.ML
+<DD>loads all source files.  Enter an ML image containing Pure
+Isabelle and type:    use "ROOT.ML";
+
+<DT>Makefile
+<DD>compiles the files under Poly/ML or SML of New Jersey
+
+
+<DT>ex
+<DD>subdirectory containing examples.  Files are arranged in
+subdirectories. To execute all of them, enter an ML image containing
+Sequents and type 
+<PRE>
+	use "ex/ROOT.ML";
+</PRE>
+To execute examples in a particular logic (LK/ILL/Modal) use the
+appropriate command:
+<PRE>
+	use "ex/LK/ROOT.ML";
+	use "ex/ILL/ROOT.ML";
+	use "ex/Modal/ROOT.ML";
+</PRE>
+</DL>
+
+<P>Much of the work in Modal logic was done by Martin Coen. Thanks to
+Rajeev Gore' for supplying the inference system for S43. Sara Kalvala
+reorganized the files and supplied Linear Logic. Jacob Frost provided
+some improvements to the syntax of sequents.
+
+<P>Useful references on sequent calculi:
+
+<UL>
+<LI>Steve Reeves and Michael Clarke,<BR>
+    Logic for Computer Science (Addison-Wesley, 1990)
+<LI>G. Takeuti,<BR>
+    Proof Theory (North Holland, 1987)
+</UL>
+
+Useful references on Modal Logics:
+<UL>
+<LI>Melvin C Fitting,<BR>
+    Proof Methods for Modal and Intuitionistic Logics (Reidel, 1983)
+
+<LI>Lincoln A. Wallen,<BR>
+    Automated Deduction in Nonclassical Logics (MIT Press, 1990)
+</UL>
+
+Useful references on Linear Logic:
+<UL>
+<LI>A. S. Troelstra<BR>
+    Lectures on Linear Logic (CSLI, 1992)
+
+<LI>S. Kalvala and V. de Paiva<BR>
+    Linear Logic in Isabelle (in TR 379, University of Cambridge
+				Computer Lab, 1995, ed L. Paulson)
+</UL>
+</UL>
+</BODY></HTML>

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Sequents/ROOT.ML	Wed Oct 09 13:32:33 1996 +0200
@@ -0,0 +1,30 @@
+(*  Title:      Sequents/ROOT
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1991  University of Cambridge
+
+Adds Classical Sequent Calculus to a database containing pure Isabelle. 
+*)
+
+val banner = "Sequent Calculii";
+writeln banner;
+
+init_thy_reader();
+
+print_depth 1;  
+
+use_thy "Sequents";
+use "prover.ML";
+
+use_thy "LK";
+use_thy "ILL";
+
+use_thy "Modal0";
+use_thy"T";
+use_thy"S4";
+use_thy"S43";
+
+use "../Pure/install_pp.ML";
+print_depth 8;
+
+val Sequents_build_completed = ();    (*indicate successful build*)

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Sequents/S4.ML	Wed Oct 09 13:32:33 1996 +0200
@@ -0,0 +1,17 @@
+(*  Title:      Modal/S4
+    ID:         $Id$
+    Author:     Martin Coen
+    Copyright   1991  University of Cambridge
+*)
+
+local open Modal0_rls S4
+in structure MP_Rule : MODAL_PROVER_RULE =
+   struct
+    val rewrite_rls = rewrite_rls
+    val safe_rls    = safe_rls
+    val unsafe_rls  = unsafe_rls @ [boxR,diaL]
+    val bound_rls   = bound_rls @ [boxL,diaR]
+    val aside_rls   = [lstar0,lstar1,lstar2,rstar0,rstar1,rstar2]
+   end;
+end;
+structure S4_Prover = Modal_ProverFun(MP_Rule);

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Sequents/S4.thy	Wed Oct 09 13:32:33 1996 +0200
@@ -0,0 +1,31 @@
+(*  Title:      Modal/S4
+    ID:         $Id$
+    Author:     Martin Coen
+    Copyright   1991  University of Cambridge
+*)
+
+S4 = Modal0 +
+rules
+(* Definition of the star operation using a set of Horn clauses *)
+(* For system S4:  gamma * == {[]P | []P : gamma}               *)
+(*                 delta * == {<>P | <>P : delta}               *)
+
+  lstar0         "|L>"
+  lstar1         "$G |L> $H ==> []P, $G |L> []P, $H"
+  lstar2         "$G |L> $H ==>   P, $G |L>      $H"
+  rstar0         "|R>"
+  rstar1         "$G |R> $H ==> <>P, $G |R> <>P, $H"
+  rstar2         "$G |R> $H ==>   P, $G |R>      $H"
+
+(* Rules for [] and <> *)
+
+  boxR
+   "[| $E |L> $E';  $F |R> $F';  $G |R> $G';  
+           $E'         |- $F', P, $G'|] ==> $E          |- $F, []P, $G"
+  boxL     "$E,P,$F,[]P |-         $G    ==> $E, []P, $F |-          $G"
+
+  diaR     "$E          |- $F,P,$G,<>P   ==> $E          |- $F, <>P, $G"
+  diaL
+   "[| $E |L> $E';  $F |L> $F';  $G |R> $G';  
+           $E', P, $F' |-         $G'|] ==> $E, <>P, $F |- $G"
+end

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Sequents/S43.ML	Wed Oct 09 13:32:33 1996 +0200
@@ -0,0 +1,19 @@
+(*  Title:      Modal/S43
+    ID:         $Id$
+    Author:     Martin Coen
+    Copyright   1991  University of Cambridge
+
+This implements Rajeev Gore's sequent calculus for S43.
+*)
+
+local open Modal0_rls S43
+in structure MP_Rule : MODAL_PROVER_RULE =
+   struct
+    val rewrite_rls = rewrite_rls
+    val safe_rls    = safe_rls
+    val unsafe_rls  = unsafe_rls @ [pi1,pi2]
+    val bound_rls   = bound_rls @ [boxL,diaR]
+    val aside_rls   = [lstar0,lstar1,lstar2,rstar0,rstar1,rstar2,S43pi0,S43pi1,S43pi2]
+   end;
+end;
+structure S43_Prover = Modal_ProverFun(MP_Rule);  

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Sequents/S43.thy	Wed Oct 09 13:32:33 1996 +0200
@@ -0,0 +1,78 @@
+(*  Title:      Modal/S43
+    ID:         $Id$
+    Author:     Martin Coen
+    Copyright   1991  University of Cambridge
+
+This implements Rajeev Gore's sequent calculus for S43.
+*)
+
+S43 = Modal0 +
+
+consts
+  S43pi :: "[seq'=>seq', seq'=>seq', seq'=>seq',
+             seq'=>seq', seq'=>seq', seq'=>seq'] => prop"
+  "@S43pi" :: "[seq, seq, seq, seq, seq, seq] => prop"
+                         ("S43pi((_);(_);(_);(_);(_);(_))" [] 5)
+
+rules
+(* Definition of the star operation using a set of Horn clauses  *)
+(* For system S43: gamma * == {[]P | []P : gamma}                *)
+(*                 delta * == {<>P | <>P : delta}                *)
+
+  lstar0         "|L>"
+  lstar1         "$G |L> $H ==> []P, $G |L> []P, $H"
+  lstar2         "$G |L> $H ==>   P, $G |L>      $H"
+  rstar0         "|R>"
+  rstar1         "$G |R> $H ==> <>P, $G |R> <>P, $H"
+  rstar2         "$G |R> $H ==>   P, $G |R>      $H"
+
+(* Set of Horn clauses to generate the antecedents for the S43 pi rule       *)
+(* ie                                                                        *)
+(*           S1...Sk,Sk+1...Sk+m                                             *)
+(*     ----------------------------------                                    *)
+(*     <>P1...<>Pk, $G |- $H, []Q1...[]Qm                                    *)
+(*                                                                           *)
+(*  where Si == <>P1...<>Pi-1,<>Pi+1,..<>Pk,Pi, $G * |- $H *, []Q1...[]Qm    *)
+(*    and Sj == <>P1...<>Pk, $G * |- $H *, []Q1...[]Qj-1,[]Qj+1...[]Qm,Qj    *)
+(*    and 1<=i<=k and k<j<=k+m                                               *)
+
+  S43pi0         "S43pi $L;; $R;; $Lbox; $Rdia"
+  S43pi1
+   "[| (S43pi <>P,$L';     $L;; $R; $Lbox;$Rdia);   $L',P,$L,$Lbox |- $R,$Rdia |] ==> 
+       S43pi     $L'; <>P,$L;; $R; $Lbox;$Rdia"
+  S43pi2
+   "[| (S43pi $L';; []P,$R';     $R; $Lbox;$Rdia);  $L',$Lbox |- $R',P,$R,$Rdia |] ==> 
+       S43pi $L';;     $R'; []P,$R; $Lbox;$Rdia"
+
+(* Rules for [] and <> for S43 *)
+
+  boxL           "$E, P, $F, []P |- $G ==> $E, []P, $F |- $G"
+  diaR           "$E |- $F, P, $G, <>P ==> $E |- $F, <>P, $G"
+  pi1
+   "[| $L1,<>P,$L2 |L> $Lbox;  $L1,<>P,$L2 |R> $Ldia;  $R |L> $Rbox;  $R |R> $Rdia;  
+      S43pi ; $Ldia;; $Rbox; $Lbox; $Rdia |] ==> 
+   $L1, <>P, $L2 |- $R"
+  pi2
+   "[| $L |L> $Lbox;  $L |R> $Ldia;  $R1,[]P,$R2 |L> $Rbox;  $R1,[]P,$R2 |R> $Rdia;  
+      S43pi ; $Ldia;; $Rbox; $Lbox; $Rdia |] ==> 
+   $L |- $R1, []P, $R2"
+end
+
+ML
+
+local
+
+  val S43pi  = "S43pi";
+  val SS43pi = "@S43pi";
+
+  val tr  = Sequents.seq_tr;
+  val tr' = Sequents.seq_tr';
+
+  fun s43pi_tr[s1,s2,s3,s4,s5,s6]=
+        Const(S43pi,dummyT)$tr s1$tr s2$tr s3$tr s4$tr s5$tr s6;
+  fun s43pi_tr'[s1,s2,s3,s4,s5,s6] =
+        Const(SS43pi,dummyT)$tr' s1$tr' s2$tr' s3$tr' s4$tr' s5$tr' s6;
+in
+val parse_translation = [(SS43pi,s43pi_tr)];
+val print_translation = [(S43pi,s43pi_tr')]
+end

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Sequents/Sequents.thy	Wed Oct 09 13:32:33 1996 +0200
@@ -0,0 +1,147 @@
+(*  Title: 	LK/lk.thy
+    ID:         $Id$
+    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1993  University of Cambridge
+
+Classical First-Order Sequent Calculus
+*)
+
+Sequents = Pure +
+
+types
+  o 
+
+arities
+  o :: logic
+
+
+(* Sequences *)
+
+types
+ seq'
+
+consts
+ SeqO'         :: "[o,seq']=>seq'"
+ Seq1'         :: "o=>seq'"
+    
+
+(* concrete syntax *)
+
+types
+  seq seqobj seqcont
+
+
+syntax
+ SeqEmp         :: "seq"                                ("")
+ SeqApp         :: "[seqobj,seqcont] => seq"            ("__")
+
+ SeqContEmp     :: "seqcont"                            ("")
+ SeqContApp     :: "[seqobj,seqcont] => seqcont"        (",/ __")
+  
+ SeqO           :: "o => seqobj"                        ("_")
+ SeqId          :: "id => seqobj"                       ("$_")
+ SeqVar         :: "var => seqobj"                      ("$_")
+
+types
+    
+ single_seqe = "[seq,seqobj] => prop"
+ single_seqi = "[seq'=>seq',seq'=>seq'] => prop"
+ two_seqi = "[seq'=>seq', seq'=>seq'] => prop"
+ two_seqe = "[seq, seq] => prop"
+ three_seqi = "[seq'=>seq', seq'=>seq', seq'=>seq'] => prop"
+ three_seqe = "[seq, seq, seq] => prop"
+ four_seqi = "[seq'=>seq', seq'=>seq', seq'=>seq', seq'=>seq'] => prop"
+ four_seqe = "[seq, seq, seq, seq] => prop"
+
+end
+
+ML
+
+(* parse translation for sequences *)
+
+fun abs_seq' t = Abs("s", Type("seq'",[]), t);
+
+fun seqobj_tr(Const("SeqO",_)$f) = Const("SeqO'",dummyT)$f |
+    seqobj_tr(_$i) = i;
+    
+fun seqcont_tr(Const("SeqContEmp",_)) = Bound 0 |
+    seqcont_tr(Const("SeqContApp",_)$so$sc) = 
+      (seqobj_tr so)$(seqcont_tr sc);
+
+fun seq_tr(Const("SeqEmp",_)) = abs_seq'(Bound 0) |
+    seq_tr(Const("SeqApp",_)$so$sc) = 
+      abs_seq'(seqobj_tr(so)$seqcont_tr(sc));
+
+
+fun singlobj_tr(Const("SeqO",_)$f) =
+    abs_seq' ((Const("SeqO'",dummyT)$f)$Bound 0);
+    
+
+    
+(* print translation for sequences *)
+
+fun seqcont_tr' (Bound 0) = 
+      Const("SeqContEmp",dummyT) |
+    seqcont_tr' (Const("SeqO'",_)$f$s) =
+      Const("SeqContApp",dummyT)$
+      (Const("SeqO",dummyT)$f)$
+      (seqcont_tr' s) |
+(*    seqcont_tr' ((a as Abs(_,_,_))$s)= 
+      seqcont_tr'(betapply(a,s)) | *)
+    seqcont_tr' (i$s) = 
+      Const("SeqContApp",dummyT)$
+      (Const("SeqId",dummyT)$i)$
+      (seqcont_tr' s);
+
+fun seq_tr' s =
+    let fun seq_itr' (Bound 0) = 
+              Const("SeqEmp",dummyT) |
+            seq_itr' (Const("SeqO'",_)$f$s) =
+              Const("SeqApp",dummyT)$
+              (Const("SeqO",dummyT)$f)$(seqcont_tr' s) |
+(*            seq_itr' ((a as Abs(_,_,_))$s) =
+              seq_itr'(betapply(a,s)) |    *)
+            seq_itr' (i$s) =
+              Const("SeqApp",dummyT)$
+              (Const("SeqId",dummyT)$i)$
+              (seqcont_tr' s)
+    in case s of 
+         Abs(_,_,t) => seq_itr' t |
+         _ => s$(Bound 0)
+    end;
+
+
+
+
+fun single_tr c [s1,s2] =
+    Const(c,dummyT)$seq_tr s1$singlobj_tr s2;
+
+fun two_seq_tr c [s1,s2] =
+    Const(c,dummyT)$seq_tr s1$seq_tr s2;
+
+fun three_seq_tr c [s1,s2,s3] =
+    Const(c,dummyT)$seq_tr s1$seq_tr s2$seq_tr s3;
+
+fun four_seq_tr c [s1,s2,s3,s4] =
+    Const(c,dummyT)$seq_tr s1$seq_tr s2$seq_tr s3$seq_tr s4;
+
+
+fun singlobj_tr'(Const("SeqO'",_)$fm) = fm |
+    singlobj_tr'(id) = Const("@SeqId",dummyT)$id;
+
+
+fun single_tr' c [s1, s2] =
+(Const (c, dummyT)$seq_tr' s1$seq_tr' s2 ); 
+
+
+fun two_seq_tr' c [s1, s2] =
+  Const (c, dummyT)$seq_tr' s1$seq_tr' s2; 
+
+fun three_seq_tr' c [s1, s2, s3] =
+  Const (c, dummyT)$seq_tr' s1$seq_tr' s2$seq_tr' s3; 
+
+fun four_seq_tr' c [s1, s2, s3, s4] =
+  Const (c, dummyT)$seq_tr' s1$seq_tr' s2$seq_tr' s3$seq_tr' s4; 
+
+
+			 

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Sequents/T.ML	Wed Oct 09 13:32:33 1996 +0200
@@ -0,0 +1,17 @@
+(*  Title:      Modal/T
+    ID:         $Id$
+    Author:     Martin Coen
+    Copyright   1991  University of Cambridge
+*)
+
+local open Modal0_rls T
+in structure MP_Rule : MODAL_PROVER_RULE =
+   struct
+    val rewrite_rls = rewrite_rls
+    val safe_rls    = safe_rls
+    val unsafe_rls  = unsafe_rls @ [boxR,diaL]
+    val bound_rls   = bound_rls @ [boxL,diaR]
+    val aside_rls   = [lstar0,lstar1,lstar2,rstar0,rstar1,rstar2]
+   end
+end;
+structure T_Prover = Modal_ProverFun(MP_Rule);  

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Sequents/T.thy	Wed Oct 09 13:32:33 1996 +0200
@@ -0,0 +1,30 @@
+(*  Title:      Modal/T
+    ID:         $Id$
+    Author:     Martin Coen
+    Copyright   1991  University of Cambridge
+*)
+
+T = Modal0 +
+rules
+(* Definition of the star operation using a set of Horn clauses *)
+(* For system T:  gamma * == {P | []P : gamma}                  *)
+(*                delta * == {P | <>P : delta}                  *)
+
+  lstar0         "|L>"
+  lstar1         "$G |L> $H ==> []P, $G |L> P, $H"
+  lstar2         "$G |L> $H ==>   P, $G |L>    $H"
+  rstar0         "|R>"
+  rstar1         "$G |R> $H ==> <>P, $G |R> P, $H"
+  rstar2         "$G |R> $H ==>   P, $G |R>    $H"
+
+(* Rules for [] and <> *)
+
+  boxR
+   "[| $E |L> $E';  $F |R> $F';  $G |R> $G';  
+               $E'        |- $F', P, $G'|] ==> $E          |- $F, []P, $G"
+  boxL     "$E, P, $F  |-         $G    ==> $E, []P, $F |-          $G"
+  diaR     "$E         |- $F, P,  $G    ==> $E          |- $F, <>P, $G"
+  diaL
+   "[| $E |L> $E';  $F |L> $F';  $G |R> $G';  
+               $E', P, $F'|-         $G'|] ==> $E, <>P, $F |-          $G"
+end

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Sequents/ex/ILL/ILL_kleene_lemmas.ML	Wed Oct 09 13:32:33 1996 +0200
@@ -0,0 +1,81 @@
+
+(* from [kleene 52] pp 118,119 *)
+
+
+val k49a = auto1 "|- [* A > ( - ( - A)) *]";
+
+val k49b = auto1 "|- [*( - ( - ( - A))) = ( - A)*]";
+
+val k49c = auto1 "|- [* (A | - A) > ( - - A = A) *]";
+
+val k50a = auto2 "|- [* - (A = - A) *]";
+
+(*
+         [rtac impr_contract 1 THEN REPEAT (rtac conj_lemma 1),
+	  res_inst_tac [("A","!((! A) -o 0)")] cut 1
+	  THEN rtac context1 1
+	  THEN ALLGOALS (best_tac power_cs)]);
+*)
+
+val k51a = auto2 "|- [* - - (A | - A) *]";
+    
+val k51b = auto2 "|- [* - - (- - A > A) *]";
+    
+val k56a = auto1 "|- [* (A | B) > - (- A & - B) *]";
+
+val k56b = auto1 "|- [* (-A | B) > - (A & -B) *]";
+    
+val k57a = auto1 "|- [* (A & B) > - (-A | -B) *]";
+    
+val k57b = auto2 "|- [* (A & -B) > -(-A | B) *]";
+    
+val k58a = auto1 "|- [* (A > B) > - (A & -B) *]";
+    
+val k58b = auto1 "|- [* (A > -B) = -(A & B) *]";
+    
+val k58c = auto1 "|- [* - (A & B) = (- - A > - B) *]";
+    
+val k58d = auto1 "|- [* (- - A > - B) = - - (-A | -B) *]";
+    
+val k58e = auto1 "! [* - -B > B *] |- [* (- -A > B) = (A > B) *]";
+    
+val k58f = auto1 "! [* - -B > B *] |- [* (A > B) = - (A & -B) *]";
+    
+val k58g = auto1 "|- [* (- -A > B) > - (A & -B) *]";
+    
+val k59a = auto1 "|- [* (-A | B) > (A > B) *]";
+
+val k59b = auto2 "|- [* (A > B) > - - (-A | B) *]";
+    
+val k59c = auto2 "|- [* (-A > B) > - -(A | B) *]";
+    
+val k60a = auto1 "|- [* (A & B) > - (A > -B) *]";
+    
+val k60b = auto1 "|- [* (A & -B) > - (A > B) *]";
+    
+val k60c = auto1 "|- [* ( - - A & B) > - (A > -B) *]";
+    
+val k60d = auto1 "|- [* (- - A & - B) = - (A > B) *]";
+    
+val k60e = auto1 "|- [* - (A > B) = - (-A | B) *]";
+    
+val k60f = auto1 "|- [* - (-A | B) = - - (A & -B) *]";
+    
+val k60g = auto2 "|- [* - - (A > B) = - (A & -B) *]";
+    
+(*
+ [step_tac safe_cs 1, best_tac safe_cs 1,
+ rtac impr 1 THEN rtac impr_contract 1
+ THEN best_tac safe_cs 1];
+*)
+
+val k60h = auto1 "|- [* - (A & -B) = (A > - -B) *]";
+
+val k60i = auto1 "|- [* (A > - -B) = (- -A > - -B) *]";
+
+val k61a = auto1 "|- [* (A | B) > (-A > B) *]";
+
+val k61b = auto2 "|- [* - (A | B) = - (-A > B) *]";
+
+val k62a = auto1 "|- [* (-A | -B) > - (A & B) *]";
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Sequents/ex/ILL/ILL_predlog.ML	Wed Oct 09 13:32:33 1996 +0200
@@ -0,0 +1,9 @@
+
+open ILL_predlog;
+
+
+fun auto1 x = prove_goal thy x
+ (fn prems => [best_tac safe_cs 1]) ;
+
+fun auto2 x = prove_goal thy x
+ (fn prems => [best_tac power_cs 1]) ;

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Sequents/ex/ILL/ILL_predlog.thy	Wed Oct 09 13:32:33 1996 +0200
@@ -0,0 +1,42 @@
+(* 
+    File:	 /Nfs/toton/usr20/sk/isa_files/ll/NEW/pred_log.thy
+    Theory Name: pred_log
+    Logic Image: HOL
+*)
+
+ILL_predlog  =  ILL +
+
+types
+
+    plf
+    
+arities
+
+    plf :: logic
+    
+consts
+
+  "&"   :: "[plf,plf] => plf"   (infixr 35)
+  "|"   :: "[plf,plf] => plf"   (infixr 35)
+  ">"   :: "[plf,plf] => plf"   (infixr 35)
+  "="   :: "[plf,plf] => plf"   (infixr 35)
+  "@NG" :: "plf => plf"   ("- _ " [50] 55)
+  ff    :: "plf"
+  
+  PL    :: "plf => o"      ("[* / _ / *]" [] 100)
+
+
+translations
+
+  "[* A & B *]" == "[*A*] && [*B*]" 
+  "[* A | B *]" == "![*A*] ++ ![*B*]"
+  "[* - A *]"   == "[*A > ff*]"
+  "[* ff *]"    == "0"
+  "[* A = B *]" => "[* (A > B) & (B > A) *]"
+  
+  "[* A > B *]" == "![*A*] -o [*B*]"
+  
+(* another translations for linear implication:
+  "[* A > B *]" == "!([*A*] -o [*B*])" *)
+
+end

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Sequents/ex/ILL/ROOT.ML	Wed Oct 09 13:32:33 1996 +0200
@@ -0,0 +1,12 @@
+
+Sequents_build_completed;    (*Cause examples to fail if LK did*)
+
+writeln"Root file for ILL examples";
+
+proof_timing := true;
+time_use_thy "ex/ILL/washing";
+
+time_use_thy "ex/ILL/ILL_predlog";
+time_use "ex/ILL/ILL_kleene_lemmas.ML";
+
+maketest"END: Root file for ILL examples";

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Sequents/ex/ILL/washing.ML	Wed Oct 09 13:32:33 1996 +0200
@@ -0,0 +1,33 @@
+
+open washing;
+
+(* "activate" definitions for use in proof *)
+
+val changeI = [context1] RL ([change] RLN (2,[cut]));
+val load1I =  [context1] RL ([load1]  RLN (2,[cut]));
+val washI =   [context1] RL ([wash]   RLN (2,[cut]));
+val dryI =    [context1] RL ([dry]    RLN (2,[cut]));
+
+
+
+(* a load of dirty clothes and two dollars gives you clean clothes *)
+
+goal thy "dollar , dollar , dirty |- clean";
+
+by (best_tac (lazy_cs add_safes (changeI @ load1I @ washI @ dryI)) 1);
+
+
+(* order of premises doesn't matter *)
+
+prove_goal thy "dollar , dirty , dollar |- clean"
+(fn _ => [best_tac (lazy_cs add_safes (changeI @ load1I @ washI @ dryI)) 1]);
+
+
+(* alternative formulation *)
+
+prove_goal thy "dollar , dollar |- dirty -o clean"
+(fn _ => [best_tac (lazy_cs add_safes (changeI @ load1I @ washI @ dryI)) 1]);
+
+
+
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Sequents/ex/ILL/washing.thy	Wed Oct 09 13:32:33 1996 +0200
@@ -0,0 +1,33 @@
+
+
+(* code by Sara Kalvala, based on Paulson's LK 
+                           and Moore's tisl.ML *)
+
+washing = ILL +
+
+consts
+
+dollar,quarter,loaded,dirty,wet,clean        :: "o"			
+
+  
+rules
+
+
+  change
+  "dollar |- (quarter >< quarter >< quarter >< quarter)"
+
+  load1
+  "quarter , quarter , quarter , quarter , quarter |- loaded"
+
+  load2
+  "dollar , quarter |- loaded"
+
+  wash
+  "loaded , dirty |- wet"
+
+  dry
+  "wet, quarter , quarter , quarter |- clean"
+
+end
+
+  
\ No newline at end of file

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Sequents/ex/LK/ROOT.ML	Wed Oct 09 13:32:33 1996 +0200
@@ -0,0 +1,18 @@
+(*  Title:      LK/ex/ROOT
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1992  University of Cambridge
+
+Executes all examples for Classical Logic. 
+*)
+
+Sequents_build_completed;    (*Cause examples to fail if LK did*)
+
+writeln"Root file for LK examples";
+
+proof_timing := true;
+time_use "ex/LK/prop.ML";
+time_use "ex/LK/quant.ML";
+time_use "ex/LK/hardquant.ML";
+
+maketest"END: Root file for LK examples";

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Sequents/ex/LK/hardquant.ML	Wed Oct 09 13:32:33 1996 +0200
@@ -0,0 +1,278 @@
+(*  Title:      LK/ex/hard-quant
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1992  University of Cambridge
+
+Hard examples with quantifiers.  Can be read to test the LK system.
+From  F. J. Pelletier,
+  Seventy-Five Problems for Testing Automatic Theorem Provers,
+  J. Automated Reasoning 2 (1986), 191-216.
+  Errata, JAR 4 (1988), 236-236.
+
+Uses pc_tac rather than fast_tac when the former is significantly faster.
+*)
+
+writeln"File LK/ex/hard-quant.";
+
+goal LK.thy "|- (ALL x. P(x) & Q(x)) <-> (ALL x. P(x))  &  (ALL x. Q(x))";
+by (fast_tac LK_pack 1);
+result(); 
+
+goal LK.thy "|- (EX x. P-->Q(x))  <->  (P --> (EX x.Q(x)))";
+by (fast_tac LK_pack 1);
+result(); 
+
+goal LK.thy "|- (EX x.P(x)-->Q)  <->  (ALL x.P(x)) --> Q";
+by (fast_tac LK_pack 1);
+result(); 
+
+goal LK.thy "|- (ALL x.P(x)) | Q  <->  (ALL x. P(x) | Q)";
+by (fast_tac LK_pack 1);
+result(); 
+
+writeln"Problems requiring quantifier duplication";
+
+(*Not provable by fast_tac LK_pack: needs multiple instantiation of ALL*)
+goal LK.thy "|- (ALL x. P(x)-->P(f(x)))  &  P(d)-->P(f(f(f(d))))";
+by (best_tac LK_dup_pack 1);
+result();
+
+(*Needs double instantiation of the quantifier*)
+goal LK.thy "|- EX x. P(x) --> P(a) & P(b)";
+by (fast_tac LK_dup_pack 1);
+result();
+
+goal LK.thy "|- EX z. P(z) --> (ALL x. P(x))";
+by (best_tac LK_dup_pack 1);
+result();
+
+writeln"Hard examples with quantifiers";
+
+writeln"Problem 18";
+goal LK.thy "|- EX y. ALL x. P(y)-->P(x)";
+by (best_tac LK_dup_pack 1);
+result(); 
+
+writeln"Problem 19";
+goal LK.thy "|- EX x. ALL y z. (P(y)-->Q(z)) --> (P(x)-->Q(x))";
+by (best_tac LK_dup_pack 1);
+result();
+
+writeln"Problem 20";
+goal LK.thy "|- (ALL x y. EX z. ALL w. (P(x)&Q(y)-->R(z)&S(w)))     \
+\   --> (EX x y. P(x) & Q(y)) --> (EX z. R(z))";
+by (fast_tac LK_pack 1); 
+result();
+
+writeln"Problem 21";
+goal LK.thy "|- (EX x. P-->Q(x)) & (EX x. Q(x)-->P) --> (EX x. P<->Q(x))";
+by (best_tac LK_dup_pack 1);
+result();
+
+writeln"Problem 22";
+goal LK.thy "|- (ALL x. P <-> Q(x))  -->  (P <-> (ALL x. Q(x)))";
+by (fast_tac LK_pack 1); 
+result();
+
+writeln"Problem 23";
+goal LK.thy "|- (ALL x. P | Q(x))  <->  (P | (ALL x. Q(x)))";
+by (best_tac LK_pack 1);  
+result();
+
+writeln"Problem 24";
+goal LK.thy "|- ~(EX x. S(x)&Q(x)) & (ALL x. P(x) --> Q(x)|R(x)) &  \
+\    ~(EX x.P(x)) --> (EX x.Q(x)) & (ALL x. Q(x)|R(x) --> S(x))  \
+\   --> (EX x. P(x)&R(x))";
+by (pc_tac LK_pack 1);
+result();
+
+writeln"Problem 25";
+goal LK.thy "|- (EX x. P(x)) &  \
+\       (ALL x. L(x) --> ~ (M(x) & R(x))) &  \
+\       (ALL x. P(x) --> (M(x) & L(x))) &   \
+\       ((ALL x. P(x)-->Q(x)) | (EX x. P(x)&R(x)))  \
+\   --> (EX x. Q(x)&P(x))";
+by (best_tac LK_pack 1);  
+result();
+
+writeln"Problem 26";
+goal LK.thy "|- ((EX x. p(x)) <-> (EX x. q(x))) &       \
+\     (ALL x. ALL y. p(x) & q(y) --> (r(x) <-> s(y)))   \
+\ --> ((ALL x. p(x)-->r(x)) <-> (ALL x. q(x)-->s(x)))";
+by (pc_tac LK_pack 1);
+result();
+
+writeln"Problem 27";
+goal LK.thy "|- (EX x. P(x) & ~Q(x)) &   \
+\             (ALL x. P(x) --> R(x)) &   \
+\             (ALL x. M(x) & L(x) --> P(x)) &   \
+\             ((EX x. R(x) & ~ Q(x)) --> (ALL x. L(x) --> ~ R(x)))  \
+\         --> (ALL x. M(x) --> ~L(x))";
+by (pc_tac LK_pack 1); 
+result();
+
+writeln"Problem 28.  AMENDED";
+goal LK.thy "|- (ALL x. P(x) --> (ALL x. Q(x))) &   \
+\       ((ALL x. Q(x)|R(x)) --> (EX x. Q(x)&S(x))) &  \
+\       ((EX x.S(x)) --> (ALL x. L(x) --> M(x)))  \
+\   --> (ALL x. P(x) & L(x) --> M(x))";
+by (pc_tac LK_pack 1);  
+result();
+
+writeln"Problem 29.  Essentially the same as Principia Mathematica *11.71";
+goal LK.thy "|- (EX x. P(x)) & (EX y. Q(y))  \
+\   --> ((ALL x. P(x)-->R(x)) & (ALL y. Q(y)-->S(y))   <->     \
+\        (ALL x y. P(x) & Q(y) --> R(x) & S(y)))";
+by (pc_tac LK_pack 1); 
+result();
+
+writeln"Problem 30";
+goal LK.thy "|- (ALL x. P(x) | Q(x) --> ~ R(x)) & \
+\       (ALL x. (Q(x) --> ~ S(x)) --> P(x) & R(x))  \
+\   --> (ALL x. S(x))";
+by (fast_tac LK_pack 1);  
+result();
+
+writeln"Problem 31";
+goal LK.thy "|- ~(EX x.P(x) & (Q(x) | R(x))) & \
+\       (EX x. L(x) & P(x)) & \
+\       (ALL x. ~ R(x) --> M(x))  \
+\   --> (EX x. L(x) & M(x))";
+by (fast_tac LK_pack 1);
+result();
+
+writeln"Problem 32";
+goal LK.thy "|- (ALL x. P(x) & (Q(x)|R(x))-->S(x)) & \
+\       (ALL x. S(x) & R(x) --> L(x)) & \
+\       (ALL x. M(x) --> R(x))  \
+\   --> (ALL x. P(x) & M(x) --> L(x))";
+by (best_tac LK_pack 1);
+result();
+
+writeln"Problem 33";
+goal LK.thy "|- (ALL x. P(a) & (P(x)-->P(b))-->P(c))  <->    \
+\    (ALL x. (~P(a) | P(x) | P(c)) & (~P(a) | ~P(b) | P(c)))";
+by (fast_tac LK_pack 1);
+result();
+
+writeln"Problem 34  AMENDED (TWICE!!)  NOT PROVED AUTOMATICALLY";
+(*Andrews's challenge*)
+goal LK.thy "|- ((EX x. ALL y. p(x) <-> p(y))  <->              \
+\              ((EX x. q(x)) <-> (ALL y. p(y))))     <->        \
+\             ((EX x. ALL y. q(x) <-> q(y))  <->                \
+\              ((EX x. p(x)) <-> (ALL y. q(y))))";
+by (safe_goal_tac LK_pack 1);   (*53 secs*) (*13 secs*)
+by (TRYALL (fast_tac LK_pack)); (*165 secs*)  (*117 secs*)  (*138 secs*)
+(*for some reason, pc_tac leaves 14 subgoals instead of 6*)
+by (TRYALL (best_tac LK_dup_pack)); (*55 secs*) (*29 secs*) (*54 secs*)
+result();
+
+
+writeln"Problem 35";
+goal LK.thy "|- EX x y. P(x,y) -->  (ALL u v. P(u,v))";
+by (best_tac LK_dup_pack 1);  (*27 secs??*)
+result();
+
+writeln"Problem 36";
+goal LK.thy "|- (ALL x. EX y. J(x,y)) & \
+\       (ALL x. EX y. G(x,y)) & \
+\       (ALL x y. J(x,y) | G(x,y) -->   \
+\       (ALL z. J(y,z) | G(y,z) --> H(x,z)))   \
+\   --> (ALL x. EX y. H(x,y))";
+by (fast_tac LK_pack 1);
+result();
+
+writeln"Problem 37";
+goal LK.thy "|- (ALL z. EX w. ALL x. EX y. \
+\          (P(x,z)-->P(y,w)) & P(y,z) & (P(y,w) --> (EX u.Q(u,w)))) & \
+\       (ALL x z. ~P(x,z) --> (EX y. Q(y,z))) & \
+\       ((EX x y. Q(x,y)) --> (ALL x. R(x,x)))  \
+\   --> (ALL x. EX y. R(x,y))";
+by (pc_tac LK_pack 1);
+result();
+
+writeln"Problem 38";
+goal LK.thy
+ "|- (ALL x. p(a) & (p(x) --> (EX y. p(y) & r(x,y))) -->        \
+\            (EX z. EX w. p(z) & r(x,w) & r(w,z)))  <->         \
+\    (ALL x. (~p(a) | p(x) | (EX z. EX w. p(z) & r(x,w) & r(w,z))) &    \
+\            (~p(a) | ~(EX y. p(y) & r(x,y)) |                          \
+\             (EX z. EX w. p(z) & r(x,w) & r(w,z))))";
+by (pc_tac LK_pack 1);
+result();
+
+writeln"Problem 39";
+goal LK.thy "|- ~ (EX x. ALL y. F(y,x) <-> ~F(y,y))";
+by (fast_tac LK_pack 1);
+result();
+
+writeln"Problem 40.  AMENDED";
+goal LK.thy "|- (EX y. ALL x. F(x,y) <-> F(x,x)) -->  \
+\                    ~(ALL x. EX y. ALL z. F(z,y) <-> ~ F(z,x))";
+by (fast_tac LK_pack 1);
+result();
+
+writeln"Problem 41";
+goal LK.thy "|- (ALL z. EX y. ALL x. f(x,y) <-> f(x,z) & ~ f(x,x))      \
+\         --> ~ (EX z. ALL x. f(x,z))";
+by (fast_tac LK_pack 1);
+result();
+
+writeln"Problem 42";
+goal LK.thy "|- ~ (EX y. ALL x. p(x,y) <-> ~ (EX z. p(x,z) & p(z,x)))";
+
+writeln"Problem 43  NOT PROVED AUTOMATICALLY";
+goal LK.thy "|- (ALL x. ALL y. q(x,y) <-> (ALL z. p(z,x) <-> p(z,y))) \
+\         --> (ALL x. (ALL y. q(x,y) <-> q(y,x)))";
+
+writeln"Problem 44";
+goal LK.thy "|- (ALL x. f(x) -->                                        \
+\             (EX y. g(y) & h(x,y) & (EX y. g(y) & ~ h(x,y))))  &       \
+\             (EX x. j(x) & (ALL y. g(y) --> h(x,y)))                   \
+\             --> (EX x. j(x) & ~f(x))";
+by (fast_tac LK_pack 1);
+result();
+
+writeln"Problem 45";
+goal LK.thy "|- (ALL x. f(x) & (ALL y. g(y) & h(x,y) --> j(x,y))        \
+\                     --> (ALL y. g(y) & h(x,y) --> k(y))) &    \
+\     ~ (EX y. l(y) & k(y)) &                                   \
+\     (EX x. f(x) & (ALL y. h(x,y) --> l(y))                    \
+\                  & (ALL y. g(y) & h(x,y) --> j(x,y)))         \
+\     --> (EX x. f(x) & ~ (EX y. g(y) & h(x,y)))";
+by (best_tac LK_pack 1); 
+result();
+
+
+writeln"Problem 50";  
+goal LK.thy
+    "|- (ALL x. P(a,x) | (ALL y.P(x,y))) --> (EX x. ALL y.P(x,y))";
+by (best_tac LK_dup_pack 1);
+result();
+
+writeln"Problem 57";
+goal LK.thy
+    "|- P(f(a,b), f(b,c)) & P(f(b,c), f(a,c)) & \
+\    (ALL x y z. P(x,y) & P(y,z) --> P(x,z))    -->   P(f(a,b), f(a,c))";
+by (fast_tac LK_pack 1);
+result();
+
+writeln"Problem 59";
+(*Unification works poorly here -- the abstraction %sobj prevents efficient
+  operation of the occurs check*)
+Unify.trace_bound := !Unify.search_bound - 1; 
+goal LK.thy "|- (ALL x. P(x) <-> ~P(f(x))) --> (EX x. P(x) & ~P(f(x)))";
+by (best_tac LK_dup_pack 1);
+result();
+
+writeln"Problem 60";
+goal LK.thy
+    "|- ALL x. P(x,f(x)) <-> (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))";
+by (fast_tac LK_pack 1);
+result();
+
+writeln"Reached end of file.";
+
+(*18 June 92: loaded in 372 secs*)
+(*19 June 92: loaded in 166 secs except #34, using repeat_goal_tac*)
+(*29 June 92: loaded in 370 secs*)

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Sequents/ex/LK/prop.ML	Wed Oct 09 13:32:33 1996 +0200
@@ -0,0 +1,194 @@
+(*  Title:      LK/ex/prop
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1992  University of Cambridge
+
+Classical sequent calculus: examples with propositional connectives
+Can be read to test the LK system.
+*)
+
+writeln"LK/ex/prop: propositional examples";
+
+writeln"absorptive laws of & and | ";
+
+goal LK.thy "|- P & P <-> P";
+by (fast_tac prop_pack 1);
+result();
+
+goal LK.thy "|- P | P <-> P";
+by (fast_tac prop_pack 1);
+result();
+
+writeln"commutative laws of & and | ";
+
+goal LK.thy "|- P & Q  <->  Q & P";
+by (fast_tac prop_pack 1);
+result();
+
+goal LK.thy "|- P | Q  <->  Q | P";
+by (fast_tac prop_pack 1);
+result();
+
+
+writeln"associative laws of & and | ";
+
+goal LK.thy "|- (P & Q) & R  <->  P & (Q & R)";
+by (fast_tac prop_pack 1);
+result();
+
+goal LK.thy "|- (P | Q) | R  <->  P | (Q | R)";
+by (fast_tac prop_pack 1);
+result();
+
+writeln"distributive laws of & and | ";
+goal LK.thy "|- (P & Q) | R  <-> (P | R) & (Q | R)";
+by (fast_tac prop_pack 1);
+result();
+
+goal LK.thy "|- (P | Q) & R  <-> (P & R) | (Q & R)";
+by (fast_tac prop_pack 1);
+result();
+
+writeln"Laws involving implication";
+
+goal LK.thy "|- (P|Q --> R) <-> (P-->R) & (Q-->R)";
+by (fast_tac prop_pack 1);
+result(); 
+
+goal LK.thy "|- (P & Q --> R) <-> (P--> (Q-->R))";
+by (fast_tac prop_pack 1);
+result(); 
+
+
+goal LK.thy "|- (P --> Q & R) <-> (P-->Q)  &  (P-->R)";
+by (fast_tac prop_pack 1);
+result();
+
+
+writeln"Classical theorems";
+
+goal LK.thy "|- P|Q --> P| ~P&Q";
+by (fast_tac prop_pack 1);
+result();
+
+
+goal LK.thy "|- (P-->Q)&(~P-->R)  -->  (P&Q | R)";
+by (fast_tac prop_pack 1);
+result();
+
+
+goal LK.thy "|- P&Q | ~P&R  <->  (P-->Q)&(~P-->R)";
+by (fast_tac prop_pack 1);
+result();
+
+
+goal LK.thy "|- (P-->Q) | (P-->R)  <->  (P --> Q | R)";
+by (fast_tac prop_pack 1);
+result();
+
+
+(*If and only if*)
+
+goal LK.thy "|- (P<->Q) <-> (Q<->P)";
+by (fast_tac prop_pack 1);
+result();
+
+goal LK.thy "|- ~ (P <-> ~P)";
+by (fast_tac prop_pack 1);
+result();
+
+
+(*Sample problems from 
+  F. J. Pelletier, 
+  Seventy-Five Problems for Testing Automatic Theorem Provers,
+  J. Automated Reasoning 2 (1986), 191-216.
+  Errata, JAR 4 (1988), 236-236.
+*)
+
+(*1*)
+goal LK.thy "|- (P-->Q)  <->  (~Q --> ~P)";
+by (fast_tac prop_pack 1);
+result();
+
+(*2*)
+goal LK.thy "|- ~ ~ P  <->  P";
+by (fast_tac prop_pack 1);
+result();
+
+(*3*)
+goal LK.thy "|- ~(P-->Q) --> (Q-->P)";
+by (fast_tac prop_pack 1);
+result();
+
+(*4*)
+goal LK.thy "|- (~P-->Q)  <->  (~Q --> P)";
+by (fast_tac prop_pack 1);
+result();
+
+(*5*)
+goal LK.thy "|- ((P|Q)-->(P|R)) --> (P|(Q-->R))";
+by (fast_tac prop_pack 1);
+result();
+
+(*6*)
+goal LK.thy "|- P | ~ P";
+by (fast_tac prop_pack 1);
+result();
+
+(*7*)
+goal LK.thy "|- P | ~ ~ ~ P";
+by (fast_tac prop_pack 1);
+result();
+
+(*8.  Peirce's law*)
+goal LK.thy "|- ((P-->Q) --> P)  -->  P";
+by (fast_tac prop_pack 1);
+result();
+
+(*9*)
+goal LK.thy "|- ((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)";
+by (fast_tac prop_pack 1);
+result();
+
+(*10*)
+goal LK.thy "Q-->R, R-->P&Q, P-->(Q|R) |- P<->Q";
+by (fast_tac prop_pack 1);
+result();
+
+(*11.  Proved in each direction (incorrectly, says Pelletier!!)  *)
+goal LK.thy "|- P<->P";
+by (fast_tac prop_pack 1);
+result();
+
+(*12.  "Dijkstra's law"*)
+goal LK.thy "|- ((P <-> Q) <-> R)  <->  (P <-> (Q <-> R))";
+by (fast_tac prop_pack 1);
+result();
+
+(*13.  Distributive law*)
+goal LK.thy "|- P | (Q & R)  <-> (P | Q) & (P | R)";
+by (fast_tac prop_pack 1);
+result();
+
+(*14*)
+goal LK.thy "|- (P <-> Q) <-> ((Q | ~P) & (~Q|P))";
+by (fast_tac prop_pack 1);
+result();
+
+
+(*15*)
+goal LK.thy "|- (P --> Q) <-> (~P | Q)";
+by (fast_tac prop_pack 1);
+result();
+
+(*16*)
+goal LK.thy "|- (P-->Q) | (Q-->P)";
+by (fast_tac prop_pack 1);
+result();
+
+(*17*)
+goal LK.thy "|- ((P & (Q-->R))-->S) <-> ((~P | Q | S) & (~P | ~R | S))";
+by (fast_tac prop_pack 1);
+result();
+
+writeln"Reached end of file.";

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Sequents/ex/LK/quant.ML	Wed Oct 09 13:32:33 1996 +0200
@@ -0,0 +1,160 @@
+(*  Title:      LK/ex/quant
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1992  University of Cambridge
+
+Classical sequent calculus: examples with quantifiers.
+*)
+
+
+writeln"LK/ex/quant: Examples with quantifiers";
+
+goal LK.thy "|- (ALL x. P)  <->  P";
+by (fast_tac LK_pack 1);
+result(); 
+
+goal LK.thy "|- (ALL x y.P(x,y))  <->  (ALL y x.P(x,y))";
+by (fast_tac LK_pack 1);
+result(); 
+
+goal LK.thy "ALL u.P(u), ALL v.Q(v) |- ALL u v. P(u) & Q(v)";
+by (fast_tac LK_pack 1);
+result(); 
+
+writeln"Permutation of existential quantifier.";
+goal LK.thy "|- (EX x y.P(x,y)) <-> (EX y x.P(x,y))";
+by (fast_tac LK_pack 1);
+result(); 
+
+goal LK.thy "|- (ALL x. P(x) & Q(x)) <-> (ALL x.P(x)) & (ALL x.Q(x))";
+by (fast_tac LK_pack 1);
+result(); 
+
+
+(*Converse is invalid*)
+goal LK.thy "|- (ALL x. P(x)) | (ALL x. Q(x)) --> (ALL x. P(x)|Q(x))";
+by (fast_tac LK_pack 1);
+result(); 
+
+
+writeln"Pushing ALL into an implication.";
+goal LK.thy "|- (ALL x. P --> Q(x))  <->  (P --> (ALL x. Q(x)))";
+by (fast_tac LK_pack 1);
+result(); 
+
+
+goal LK.thy "|- (ALL x.P(x)-->Q)  <->  ((EX x.P(x)) --> Q)";
+by (fast_tac LK_pack 1);
+result(); 
+
+
+goal LK.thy "|- (EX x. P)  <->  P";
+by (fast_tac LK_pack 1);
+result(); 
+
+
+writeln"Distribution of EX over disjunction.";
+goal LK.thy "|- (EX x. P(x) | Q(x)) <-> (EX x. P(x))  |  (EX x. Q(x))";
+by (fast_tac LK_pack 1);
+result(); 
+(*5 secs*)
+
+(*Converse is invalid*)
+goal LK.thy "|- (EX x. P(x) & Q(x))  -->  (EX x. P(x))  &  (EX x. Q(x))";
+by (fast_tac LK_pack 1);
+result(); 
+
+
+writeln"Harder examples: classical theorems.";
+
+goal LK.thy "|- (EX x. P-->Q(x))  <->  (P --> (EX x.Q(x)))";
+by (fast_tac LK_pack 1);
+result(); 
+(*3 secs*)
+
+
+goal LK.thy "|- (EX x.P(x)-->Q)  <->  (ALL x.P(x)) --> Q";
+by (fast_tac LK_pack 1);
+result(); 
+(*5 secs*)
+
+
+goal LK.thy "|- (ALL x.P(x)) | Q  <->  (ALL x. P(x) | Q)";
+by (fast_tac LK_pack 1);
+result(); 
+
+
+writeln"Basic test of quantifier reasoning";
+goal LK.thy
+   "|- (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))";
+by (fast_tac LK_pack 1);
+result();  
+
+
+goal LK.thy "|- (ALL x. Q(x))  -->  (EX x. Q(x))";
+by (fast_tac LK_pack 1);
+result();  
+
+
+writeln"The following are invalid!";
+
+(*INVALID*)
+goal LK.thy "|- (ALL x. EX y. Q(x,y))  -->  (EX y. ALL x. Q(x,y))";
+by (fast_tac LK_pack 1) handle ERROR => writeln"Failed, as expected"; 
+(*Check that subgoals remain: proof failed.*)
+getgoal 1; 
+
+(*INVALID*)
+goal LK.thy "|- (EX x. Q(x))  -->  (ALL x. Q(x))";
+by (fast_tac LK_pack 1) handle ERROR => writeln"Failed, as expected";
+getgoal 1; 
+
+goal LK.thy "|- P(?a) --> (ALL x.P(x))";
+by (fast_tac LK_pack 1) handle ERROR => writeln"Failed, as expected";
+(*Check that subgoals remain: proof failed.*)
+getgoal 1;  
+
+goal LK.thy "|- (P(?a) --> (ALL x.Q(x))) --> (ALL x. P(x) --> Q(x))";
+by (fast_tac LK_pack 1) handle ERROR => writeln"Failed, as expected";
+getgoal 1;  
+
+
+writeln"Back to things that are provable...";
+
+goal LK.thy "|- (ALL x. P(x)-->Q(x)) & (EX x.P(x)) --> (EX x.Q(x))";
+by (fast_tac LK_pack 1); 
+result();  
+
+(*An example of why exR should be delayed as long as possible*)
+goal LK.thy "|- (P--> (EX x.Q(x))) & P--> (EX x.Q(x))";
+by (fast_tac LK_pack 1);
+result();  
+
+writeln"Solving for a Var";
+goal LK.thy 
+   "|- (ALL x. P(x)-->Q(f(x))) & (ALL x. Q(x)-->R(g(x))) & P(d) --> R(?a)";
+by (fast_tac LK_pack 1);
+result();
+
+
+writeln"Principia Mathematica *11.53";
+goal LK.thy 
+    "|- (ALL x y. P(x) --> Q(y)) <-> ((EX x. P(x)) --> (ALL y. Q(y)))";
+by (fast_tac LK_pack 1);
+result();
+
+
+writeln"Principia Mathematica *11.55";
+goal LK.thy "|- (EX x y. P(x) & Q(x,y)) <-> (EX x. P(x) & (EX y.Q(x,y)))";
+by (fast_tac LK_pack 1);
+result();
+
+writeln"Principia Mathematica *11.61";
+goal LK.thy
+   "|- (EX y. ALL x. P(x) --> Q(x,y)) --> (ALL x. P(x) --> (EX y. Q(x,y)))";
+by (fast_tac LK_pack 1);
+result();
+
+writeln"Reached end of file.";
+
+(*21 August 88: loaded in 45.7 secs*)

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Sequents/ex/Modal/ROOT.ML	Wed Oct 09 13:32:33 1996 +0200
@@ -0,0 +1,28 @@
+(*  Title:      Modal/ex/ROOT
+    ID:         $Id$
+    Author:     Martin Coen
+    Copyright   1991  University of Cambridge
+*)
+
+Sequents_build_completed;    (*Cause examples to fail if Modal did*)
+
+proof_timing := true;
+
+writeln "\nTheorems of T\n";
+fun try s = (writeln s; prove_goal T.thy s (fn _=> [T_Prover.solve_tac 2]));
+time_use "ex/Modal/Tthms.ML";
+
+writeln "\nTheorems of S4\n";
+fun try s = (writeln s; prove_goal S4.thy s (fn _=> [S4_Prover.solve_tac 2]));
+time_use "ex/Modal/Tthms.ML";
+time_use "ex/Modal/S4thms.ML";
+
+writeln "\nTheorems of S43\n";
+fun try s = (writeln s;
+             prove_goal S43.thy s (fn _=> [S43_Prover.solve_tac 2 ORELSE 
+                                           S43_Prover.solve_tac 3]));
+time_use "ex/Modal/Tthms.ML";
+time_use "ex/Modal/S4thms.ML";
+time_use "ex/Modal/S43thms.ML";
+
+maketest"END: Root file for Modal examples";

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Sequents/ex/Modal/S43thms.ML	Wed Oct 09 13:32:33 1996 +0200
@@ -0,0 +1,49 @@
+(*  Title:      91/Modal/ex/S43thms
+    ID:         $Id$
+    Author:     Martin Coen
+    Copyright   1991  University of Cambridge
+*)
+
+(* Theorems of system S43 *)
+
+try "|- <>[]P --> []<>P";
+try "|- <>[]P --> [][]<>P";
+try "|- [](<>P | <>Q) --> []<>P | []<>Q";
+try "|- <>[]P & <>[]Q --> <>([]P & []Q)";
+try "|- []([]P --> []Q) | []([]Q --> []P)";
+try "|- [](<>P --> <>Q) | [](<>Q --> <>P)";
+try "|- []([]P --> Q) | []([]Q --> P)";
+try "|- [](P --> <>Q) | [](Q --> <>P)";
+try "|- [](P --> []Q-->R) | [](P | ([]R --> Q))";
+try "|- [](P | (Q --> <>C)) | [](P --> C --> <>Q)";
+try "|- []([]P | Q) & [](P | []Q) --> []P | []Q";
+try "|- <>P & <>Q --> <>(<>P & Q) | <>(P & <>Q)";
+try "|- [](P | Q) & []([]P | Q) & [](P | []Q) --> []P | []Q";
+try "|- <>P & <>Q --> <>(P & Q) | <>(<>P & Q) | <>(P & <>Q)";
+try "|- <>[]<>P <-> []<>P";
+try "|- []<>[]P <-> <>[]P";
+
+(* These are from Hailpern, LNCS 129 *)
+
+try "|- [](P & Q) <-> []P & []Q";
+try "|- <>(P | Q) <-> <>P | <>Q";
+try "|- <>(P --> Q) <-> []P --> <>Q";
+
+try "|- [](P --> Q) --> <>P --> <>Q";
+try "|- []P --> []<>P";
+try "|- <>[]P --> <>P";
+try "|- []<>[]P --> []<>P";
+try "|- <>[]P --> <>[]<>P";
+try "|- <>[]P --> []<>P";
+try "|- []<>[]P <-> <>[]P";
+try "|- <>[]<>P <-> []<>P";
+
+try "|- []P | []Q --> [](P | Q)";
+try "|- <>(P & Q) --> <>P & <>Q";
+try "|- [](P | Q) --> []P | <>Q";
+try "|- <>P & []Q --> <>(P & Q)";
+try "|- [](P | Q) --> <>P | []Q";
+try "|- [](P | Q) --> []<>P | []<>Q";
+try "|- <>[]P & <>[]Q --> <>(P & Q)";
+try "|- <>[](P & Q) <-> <>[]P & <>[]Q";
+try "|- []<>(P | Q) <-> []<>P | []<>Q";

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Sequents/ex/Modal/S4thms.ML	Wed Oct 09 13:32:33 1996 +0200
@@ -0,0 +1,40 @@
+(*  Title:      91/Modal/ex/S4thms
+    ID:         $Id$
+    Author:     Martin Coen
+    Copyright   1991  University of Cambridge
+*)
+
+(* Theorems of system S4 from Hughes and Cresswell, p.46 *)
+
+try "|- []A --> A";             (* refexivity *)
+try "|- []A --> [][]A";         (* transitivity *)
+try "|- []A --> <>A";           (* seriality *)
+try "|- <>[](<>A --> []<>A)";
+try "|- <>[](<>[]A --> []A)";
+try "|- []P <-> [][]P";
+try "|- <>P <-> <><>P";
+try "|- <>[]<>P --> <>P";
+try "|- []<>P <-> []<>[]<>P";
+try "|- <>[]P <-> <>[]<>[]P";
+
+(* Theorems for system S4 from Hughes and Cresswell, p.60 *)
+
+try "|- []P | []Q <-> []([]P | []Q)";
+try "|- ((P>-<Q) --< R) --> ((P>-<Q) --< []R)";
+
+(* These are from Hailpern, LNCS 129 *)
+
+try "|- [](P & Q) <-> []P & []Q";
+try "|- <>(P | Q) <-> <>P | <>Q";
+try "|- <>(P --> Q) <-> ([]P --> <>Q)";
+
+try "|- [](P --> Q) --> (<>P --> <>Q)";
+try "|- []P --> []<>P";
+try "|- <>[]P --> <>P";
+
+try "|- []P | []Q --> [](P | Q)";
+try "|- <>(P & Q) --> <>P & <>Q";
+try "|- [](P | Q) --> []P | <>Q";
+try "|- <>P & []Q --> <>(P & Q)";
+try "|- [](P | Q) --> <>P | []Q";
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Sequents/ex/Modal/Tthms.ML	Wed Oct 09 13:32:33 1996 +0200
@@ -0,0 +1,31 @@
+(*  Title:      91/Modal/ex/Tthms
+    ID:         $Id$
+    Author:     Martin Coen
+    Copyright   1991  University of Cambridge
+*)
+
+(* Theorems of system T from Hughes and Cresswell and Hailpern, LNCS 129 *)
+
+try "|- []P --> P";
+try "|- [](P-->Q) --> ([]P-->[]Q)";    (* normality*)
+try "|- (P--<Q) --> []P --> []Q";
+try "|- P --> <>P";
+
+try "|-  [](P & Q) <-> []P & []Q";
+try "|-  <>(P | Q) <-> <>P | <>Q";
+try "|-  [](P<->Q) <-> (P>-<Q)";
+try "|-  <>(P-->Q) <-> ([]P--><>Q)";
+try "|-        []P <-> ~<>(~P)";
+try "|-     [](~P) <-> ~<>P";
+try "|-       ~[]P <-> <>(~P)";
+try "|-      [][]P <-> ~<><>(~P)";
+try "|- ~<>(P | Q) <-> ~<>P & ~<>Q";
+
+try "|- []P | []Q --> [](P | Q)";
+try "|- <>(P & Q) --> <>P & <>Q";
+try "|- [](P | Q) --> []P | <>Q";
+try "|- <>P & []Q --> <>(P & Q)";
+try "|- [](P | Q) --> <>P | []Q";
+try "|- <>(P-->(Q & R)) --> ([]P --> <>Q) & ([]P--><>R)";
+try "|- (P--<Q) & (Q--<R) --> (P--<R)";
+try "|- []P --> <>Q --> <>(P & Q)";

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Sequents/ex/ROOT.ML	Wed Oct 09 13:32:33 1996 +0200
@@ -0,0 +1,4 @@
+
+use "ex/LK/ROOT.ML";
+use "ex/ILL/ROOT.ML";
+use "ex/Modal/ROOT.ML";

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Sequents/index.html	Wed Oct 09 13:32:33 1996 +0200
@@ -0,0 +1,15 @@
+<HTML><HEAD><TITLE>Isabelle/Sequents</TITLE></HEAD>
+<BODY><H2>Isabelle/Sequents</H2>
+The name of every theory is linked to its theory file<BR>
+<IMG SRC = "../Tools/red_arrow.gif" ALT = \/></A> stands for subtheories (child theories)<BR>
+<IMG SRC = "../Tools/blue_arrow.gif" ALT = /\></A> stands for supertheories (parent theories)<P>
+<A HREF = "../index.html">Back</A> to the index of Isabelle logics
+<BR>View the <A HREF = "README.html">ReadMe</A> file.
+<HR><A HREF = ".Sequents_sub.html"><IMG SRC = "../Tools/red_arrow.gif" BORDER=0 ALT = \/></A><A HREF = ".Sequents_sup.html"><IMG SRC = "../Tools/blue_arrow.gif" BORDER=0 ALT = /\></A> <A HREF = ".Sequents.html">Sequents</A><BR>
+<A HREF = ".LK_sub.html"><IMG SRC = "../Tools/red_arrow.gif" BORDER=0 ALT = \/></A><A HREF = ".LK_sup.html"><IMG SRC = "../Tools/blue_arrow.gif" BORDER=0 ALT = /\></A> <A HREF = ".LK.html">LK</A><BR>
+<A HREF = ".ILL_sub.html"><IMG SRC = "../Tools/red_arrow.gif" BORDER=0 ALT = \/></A><A HREF = ".ILL_sup.html"><IMG SRC = "../Tools/blue_arrow.gif" BORDER=0 ALT = /\></A> <A HREF = ".ILL.html">ILL</A><BR>
+<A HREF = ".Modal0_sub.html"><IMG SRC = "../Tools/red_arrow.gif" BORDER=0 ALT = \/></A><A HREF = ".Modal0_sup.html"><IMG SRC = "../Tools/blue_arrow.gif" BORDER=0 ALT = /\></A> <A HREF = ".Modal0.html">Modal0</A><BR>
+<A HREF = ".T_sub.html"><IMG SRC = "../Tools/red_arrow.gif" BORDER=0 ALT = \/></A><A HREF = ".T_sup.html"><IMG SRC = "../Tools/blue_arrow.gif" BORDER=0 ALT = /\></A> <A HREF = ".T.html">T</A><BR>
+<A HREF = ".S4_sub.html"><IMG SRC = "../Tools/red_arrow.gif" BORDER=0 ALT = \/></A><A HREF = ".S4_sup.html"><IMG SRC = "../Tools/blue_arrow.gif" BORDER=0 ALT = /\></A> <A HREF = ".S4.html">S4</A><BR>
+<A HREF = ".S43_sub.html"><IMG SRC = "../Tools/red_arrow.gif" BORDER=0 ALT = \/></A><A HREF = ".S43_sup.html"><IMG SRC = "../Tools/blue_arrow.gif" BORDER=0 ALT = /\></A> <A HREF = ".S43.html">S43</A><BR>
+<!-->
\ No newline at end of file

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Sequents/prover.ML	Wed Oct 09 13:32:33 1996 +0200
@@ -0,0 +1,223 @@
+(*  Title:      LK/LK.ML
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1992  University of Cambridge
+*)
+
+
+(**** Theorem Packs ****)
+
+(* based largely on LK *)
+
+datatype pack = Pack of thm list * thm list;
+
+(*A theorem pack has the form  (safe rules, unsafe rules)
+  An unsafe rule is incomplete or introduces variables in subgoals,
+  and is tried only when the safe rules are not applicable.  *)
+
+fun less (rl1,rl2) = (nprems_of rl1) < (nprems_of rl2);
+
+val empty_pack = Pack([],[]);
+
+infix 4 add_safes add_unsafes;
+
+fun (Pack(safes,unsafes)) add_safes ths   = 
+    Pack(sort less (ths@safes), unsafes);
+
+fun (Pack(safes,unsafes)) add_unsafes ths = 
+    Pack(safes, sort less (ths@unsafes));
+
+
+(*Returns the list of all formulas in the sequent*)
+fun forms_of_seq (Const("SeqO'",_) $ P $ u) = P :: forms_of_seq u
+  | forms_of_seq (H $ u) = forms_of_seq u
+  | forms_of_seq _ = [];
+
+(*Tests whether two sequences (left or right sides) could be resolved.
+  seqp is a premise (subgoal), seqc is a conclusion of an object-rule.
+  Assumes each formula in seqc is surrounded by sequence variables
+  -- checks that each concl formula looks like some subgoal formula.
+  It SHOULD check order as well, using recursion rather than forall/exists*)
+fun could_res (seqp,seqc) =
+      forall (fn Qc => exists (fn Qp => could_unify (Qp,Qc)) 
+                              (forms_of_seq seqp))
+             (forms_of_seq seqc);
+
+
+(*Tests whether two sequents or pairs of sequents could be resolved*)
+fun could_resolve_seq (prem,conc) =
+  case (prem,conc) of
+      (_ $ Abs(_,_,leftp) $ Abs(_,_,rightp),
+       _ $ Abs(_,_,leftc) $ Abs(_,_,rightc)) =>
+	  could_res (leftp,leftc) andalso could_res (rightp,rightc)
+    | (_ $ Abs(_,_,leftp) $ rightp,
+       _ $ Abs(_,_,leftc) $ rightc) =>
+	  could_res (leftp,leftc)  andalso  could_unify (rightp,rightc)
+    | _ => false;
+
+
+(*Like filt_resolve_tac, using could_resolve_seq
+  Much faster than resolve_tac when there are many rules.
+  Resolve subgoal i using the rules, unless more than maxr are compatible. *)
+fun filseq_resolve_tac rules maxr = SUBGOAL(fn (prem,i) =>
+  let val rls = filter_thms could_resolve_seq (maxr+1, prem, rules)
+  in  if length rls > maxr  then  no_tac
+	  else (*((rtac derelict 1 THEN rtac impl 1
+		 THEN (rtac identity 2 ORELSE rtac ll_mp 2)
+		 THEN rtac context1 1)
+		 ORELSE *) resolve_tac rls i
+  end);
+
+
+(*Predicate: does the rule have n premises? *)
+fun has_prems n rule =  (nprems_of rule = n);
+
+(*Continuation-style tactical for resolution.
+  The list of rules is partitioned into 0, 1, 2 premises.
+  The resulting tactic, gtac, tries to resolve with rules.
+  If successful, it recursively applies nextac to the new subgoals only.
+  Else fails.  (Treatment of goals due to Ph. de Groote) 
+  Bind (RESOLVE_THEN rules) to a variable: it preprocesses the rules. *)
+
+(*Takes rule lists separated in to 0, 1, 2, >2 premises.
+  The abstraction over state prevents needless divergence in recursion.
+  The 9999 should be a parameter, to delay treatment of flexible goals. *)
+
+fun RESOLVE_THEN rules =
+  let val [rls0,rls1,rls2] = partition_list has_prems 0 2 rules;
+      fun tac nextac i = STATE (fn state =>  
+	  filseq_resolve_tac rls0 9999 i 
+	  ORELSE
+	  (DETERM(filseq_resolve_tac rls1 9999 i) THEN  TRY(nextac i))
+	  ORELSE
+	  (DETERM(filseq_resolve_tac rls2 9999 i) THEN  TRY(nextac(i+1))
+					THEN  TRY(nextac i)) )
+  in  tac  end;
+
+
+
+(*repeated resolution applied to the designated goal*)
+fun reresolve_tac rules = 
+  let val restac = RESOLVE_THEN rules;  (*preprocessing done now*)
+      fun gtac i = restac gtac i
+  in  gtac  end; 
+
+(*tries the safe rules repeatedly before the unsafe rules. *)
+fun repeat_goal_tac (Pack(safes,unsafes)) = 
+  let val restac  =    RESOLVE_THEN safes
+      and lastrestac = RESOLVE_THEN unsafes;
+      fun gtac i = restac gtac i  ORELSE  (print_tac THEN lastrestac gtac i)
+  in  gtac  end; 
+
+
+(*Tries safe rules only*)
+fun safe_goal_tac (Pack(safes,unsafes)) = reresolve_tac safes;
+
+(*Tries a safe rule or else a unsafe rule.  Single-step for tracing. *)
+fun step_tac (thm_pack as Pack(safes,unsafes)) =
+    safe_goal_tac thm_pack  ORELSE'
+    filseq_resolve_tac unsafes 9999;
+
+
+(* Tactic for reducing a goal, using Predicate Calculus rules.
+   A decision procedure for Propositional Calculus, it is incomplete
+   for Predicate-Calculus because of allL_thin and exR_thin.  
+   Fails if it can do nothing.      *)
+fun pc_tac thm_pack = SELECT_GOAL (DEPTH_SOLVE (repeat_goal_tac thm_pack 1));
+
+
+(*The following two tactics are analogous to those provided by 
+  Provers/classical.  In fact, pc_tac is usually FASTER than fast_tac!*)
+fun fast_tac thm_pack =
+  SELECT_GOAL (DEPTH_SOLVE (step_tac thm_pack 1));
+
+fun best_tac thm_pack  = 
+  SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, size_of_thm) 
+	       (step_tac thm_pack 1));
+
+
+
+signature MODAL_PROVER_RULE =
+sig
+    val rewrite_rls      : thm list
+    val safe_rls         : thm list
+    val unsafe_rls       : thm list
+    val bound_rls        : thm list
+    val aside_rls        : thm list
+end;
+
+signature MODAL_PROVER = 
+sig
+    val rule_tac   : thm list -> int ->tactic
+    val step_tac   : int -> tactic
+    val solven_tac : int -> int -> tactic
+    val solve_tac  : int -> tactic
+end;
+
+functor Modal_ProverFun (Modal_Rule: MODAL_PROVER_RULE) : MODAL_PROVER = 
+struct
+local open Modal_Rule
+in 
+
+(*Returns the list of all formulas in the sequent*)
+fun forms_of_seq (Const("SeqO",_) $ P $ u) = P :: forms_of_seq u
+  | forms_of_seq (H $ u) = forms_of_seq u
+  | forms_of_seq _ = [];
+
+(*Tests whether two sequences (left or right sides) could be resolved.
+  seqp is a premise (subgoal), seqc is a conclusion of an object-rule.
+  Assumes each formula in seqc is surrounded by sequence variables
+  -- checks that each concl formula looks like some subgoal formula.*)
+fun could_res (seqp,seqc) =
+      forall (fn Qc => exists (fn Qp => could_unify (Qp,Qc)) 
+                              (forms_of_seq seqp))
+             (forms_of_seq seqc);
+
+(*Tests whether two sequents G|-H could be resolved, comparing each side.*)
+fun could_resolve_seq (prem,conc) =
+  case (prem,conc) of
+      (_ $ Abs(_,_,leftp) $ Abs(_,_,rightp),
+       _ $ Abs(_,_,leftc) $ Abs(_,_,rightc)) =>
+          could_res (leftp,leftc)  andalso  could_res (rightp,rightc)
+    | _ => false;
+
+(*Like filt_resolve_tac, using could_resolve_seq
+  Much faster than resolve_tac when there are many rules.
+  Resolve subgoal i using the rules, unless more than maxr are compatible. *)
+fun filseq_resolve_tac rules maxr = SUBGOAL(fn (prem,i) =>
+  let val rls = filter_thms could_resolve_seq (maxr+1, prem, rules)
+  in  if length rls > maxr  then  no_tac  else resolve_tac rls i
+  end);
+
+fun fresolve_tac rls n = filseq_resolve_tac rls 999 n;
+
+(* NB No back tracking possible with aside rules *)
+
+fun aside_tac n = DETERM(REPEAT (filt_resolve_tac aside_rls 999 n));
+fun rule_tac rls n = fresolve_tac rls n THEN aside_tac n;
+
+val fres_safe_tac = fresolve_tac safe_rls;
+val fres_unsafe_tac = fresolve_tac unsafe_rls THEN' aside_tac;
+val fres_bound_tac = fresolve_tac bound_rls;
+
+fun UPTOGOAL n tf = let fun tac i = if i<n then all_tac
+                                    else tf(i) THEN tac(i-1)
+                    in STATE(fn state=> tac(nprems_of state)) end;
+
+(* Depth first search bounded by d *)
+fun solven_tac d n = STATE (fn state =>
+        if d<0 then no_tac
+        else if (nprems_of state = 0) then all_tac 
+        else (DETERM(fres_safe_tac n) THEN UPTOGOAL n (solven_tac d)) ORELSE
+                 ((fres_unsafe_tac n  THEN UPTOGOAL n (solven_tac d)) APPEND
+                   (fres_bound_tac n  THEN UPTOGOAL n (solven_tac (d-1)))));
+
+fun solve_tac d = rewrite_goals_tac rewrite_rls THEN solven_tac d 1;
+
+fun step_tac n = STATE (fn state =>  
+      if (nprems_of state = 0) then all_tac 
+      else (DETERM(fres_safe_tac n)) ORELSE 
+           (fres_unsafe_tac n APPEND fres_bound_tac n));
+
+end;
+end;