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;