--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Sequents/ILL/ILL_kleene_lemmas.ML Fri Feb 05 21:14:17 1999 +0100
@@ -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/ILL/ILL_predlog.ML Fri Feb 05 21:14:17 1999 +0100
@@ -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/ILL/ILL_predlog.thy Fri Feb 05 21:14:17 1999 +0100
@@ -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/ILL/ROOT.ML Fri Feb 05 21:14:17 1999 +0100
@@ -0,0 +1,10 @@
+
+Sequents_build_completed; (*Cause examples to fail if Sequents did*)
+writeln"Root file for ILL examples";
+
+set proof_timing;
+
+time_use_thy "washing";
+
+time_use_thy "ILL_predlog";
+time_use "ILL_kleene_lemmas.ML";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Sequents/ILL/washing.ML Fri Feb 05 21:14:17 1999 +0100
@@ -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 "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/ILL/washing.thy Fri Feb 05 21:14:17 1999 +0100
@@ -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
--- a/src/Sequents/IsaMakefile Fri Feb 05 21:12:45 1999 +0100
+++ b/src/Sequents/IsaMakefile Fri Feb 05 21:14:17 1999 +0100
@@ -8,7 +8,7 @@
default: Sequents
images: Sequents
-test: Sequents-ex
+test: Sequents-ILL Sequents-LK Sequents-Modal
all: images test
@@ -31,19 +31,36 @@
@$(ISATOOL) usedir -b $(OUT)/Pure Sequents
-## Sequents-ex
+## Sequents-ILL
+
+Sequents-ILL: Sequents $(LOG)/Sequents-ILL.gz
-Sequents-ex: Sequents $(LOG)/Sequents-ex.gz
+$(LOG)/Sequents-ILL.gz: $(OUT)/Sequents ILL/ILL_kleene_lemmas.ML \
+ ILL/ILL_predlog.ML ILL/ILL_predlog.thy ILL/ROOT.ML ILL/washing.ML \
+ ILL/washing.thy
+ @$(ISATOOL) usedir $(OUT)/Sequents ILL
+
+
+## Sequents-LK
-$(LOG)/Sequents-ex.gz: $(OUT)/Sequents ex/ILL/ILL_kleene_lemmas.ML \
- ex/ILL/ILL_predlog.ML ex/ILL/ILL_predlog.thy ex/ILL/washing.ML \
- ex/ILL/washing.thy 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/ROOT.ML
- @$(ISATOOL) usedir $(OUT)/Sequents ex
+Sequents-LK: Sequents $(LOG)/Sequents-LK.gz
+
+$(LOG)/Sequents-LK.gz: $(OUT)/Sequents LK/ROOT.ML LK/hardquant.ML \
+ LK/prop.ML LK/quant.ML
+ @$(ISATOOL) usedir $(OUT)/Sequents LK
+
+
+## Sequents-Modal
+
+Sequents-Modal: Sequents $(LOG)/Sequents-Modal.gz
+
+$(LOG)/Sequents-Modal.gz: $(OUT)/Sequents Modal/ROOT.ML \
+ Modal/S43thms.ML Modal/S4thms.ML Modal/Tthms.ML ROOT.ML
+ @$(ISATOOL) usedir $(OUT)/Sequents Modal
## clean
clean:
- @rm -f $(OUT)/Sequents $(LOG)/Sequents.gz $(LOG)/Sequents-ex.gz
+ @rm -f $(OUT)/Sequents $(LOG)/Sequents.gz $(LOG)/Sequents-ILL.gz \
+ $(LOG)/Sequents-LK.gz $(LOG)/Sequents-Modal.gz
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Sequents/LK/ROOT.ML Fri Feb 05 21:14:17 1999 +0100
@@ -0,0 +1,16 @@
+(* 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 Sequents did*)
+
+writeln"Root file for LK examples";
+
+set proof_timing;
+time_use "prop.ML";
+time_use "quant.ML";
+time_use "hardquant.ML";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Sequents/LK/hardquant.ML Fri Feb 05 21:14:17 1999 +0100
@@ -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/LK/prop.ML Fri Feb 05 21:14:17 1999 +0100
@@ -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/LK/quant.ML Fri Feb 05 21:14:17 1999 +0100
@@ -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/Modal/ROOT.ML Fri Feb 05 21:14:17 1999 +0100
@@ -0,0 +1,26 @@
+(* Title: Modal/ex/ROOT
+ ID: $Id$
+ Author: Martin Coen
+ Copyright 1991 University of Cambridge
+*)
+
+Sequents_build_completed; (*Cause examples to fail if Sequents did*)
+
+set proof_timing;
+
+writeln "\nTheorems of T\n";
+fun try s = (writeln s; prove_goal T.thy s (fn _=> [T_Prover.solve_tac 2]));
+time_use "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 "Tthms.ML";
+time_use "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 "Tthms.ML";
+time_use "S4thms.ML";
+time_use "S43thms.ML";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Sequents/Modal/S43thms.ML Fri Feb 05 21:14:17 1999 +0100
@@ -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/Modal/S4thms.ML Fri Feb 05 21:14:17 1999 +0100
@@ -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/Modal/Tthms.ML Fri Feb 05 21:14:17 1999 +0100
@@ -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)";
--- a/src/Sequents/ex/ILL/ILL_kleene_lemmas.ML Fri Feb 05 21:12:45 1999 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,81 +0,0 @@
-
-(* 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) *]";
-
--- a/src/Sequents/ex/ILL/ILL_predlog.ML Fri Feb 05 21:12:45 1999 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,9 +0,0 @@
-
-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]) ;
--- a/src/Sequents/ex/ILL/ILL_predlog.thy Fri Feb 05 21:12:45 1999 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,42 +0,0 @@
-(*
- 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
--- a/src/Sequents/ex/ILL/ROOT.ML Fri Feb 05 21:12:45 1999 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,10 +0,0 @@
-
-Sequents_build_completed; (*Cause examples to fail if Sequents did*)
-writeln"Root file for ILL examples";
-
-set proof_timing;
-
-time_use_thy "ILL/washing";
-
-time_use_thy "ILL/ILL_predlog";
-time_use "ILL/ILL_kleene_lemmas.ML";
--- a/src/Sequents/ex/ILL/washing.ML Fri Feb 05 21:12:45 1999 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,33 +0,0 @@
-
-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 "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]);
-
-
-
-
--- a/src/Sequents/ex/ILL/washing.thy Fri Feb 05 21:12:45 1999 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,33 +0,0 @@
-
-
-(* 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
--- a/src/Sequents/ex/LK/ROOT.ML Fri Feb 05 21:12:45 1999 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,16 +0,0 @@
-(* 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 Sequents did*)
-
-writeln"Root file for LK examples";
-
-set proof_timing;
-time_use "LK/prop.ML";
-time_use "LK/quant.ML";
-time_use "LK/hardquant.ML";
--- a/src/Sequents/ex/LK/hardquant.ML Fri Feb 05 21:12:45 1999 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,278 +0,0 @@
-(* 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*)
--- a/src/Sequents/ex/LK/prop.ML Fri Feb 05 21:12:45 1999 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,194 +0,0 @@
-(* 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.";
--- a/src/Sequents/ex/LK/quant.ML Fri Feb 05 21:12:45 1999 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,160 +0,0 @@
-(* 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*)
--- a/src/Sequents/ex/Modal/ROOT.ML Fri Feb 05 21:12:45 1999 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,26 +0,0 @@
-(* Title: Modal/ex/ROOT
- ID: $Id$
- Author: Martin Coen
- Copyright 1991 University of Cambridge
-*)
-
-Sequents_build_completed; (*Cause examples to fail if Sequents did*)
-
-set proof_timing;
-
-writeln "\nTheorems of T\n";
-fun try s = (writeln s; prove_goal T.thy s (fn _=> [T_Prover.solve_tac 2]));
-time_use "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 "Modal/Tthms.ML";
-time_use "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 "Modal/Tthms.ML";
-time_use "Modal/S4thms.ML";
-time_use "Modal/S43thms.ML";
--- a/src/Sequents/ex/Modal/S43thms.ML Fri Feb 05 21:12:45 1999 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,49 +0,0 @@
-(* 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";
--- a/src/Sequents/ex/Modal/S4thms.ML Fri Feb 05 21:12:45 1999 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,40 +0,0 @@
-(* 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";
-
--- a/src/Sequents/ex/Modal/Tthms.ML Fri Feb 05 21:12:45 1999 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,31 +0,0 @@
-(* 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)";
--- a/src/Sequents/ex/ROOT.ML Fri Feb 05 21:12:45 1999 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,7 +0,0 @@
-
-writeln"Root file for Sequents examples";
-Sequents_build_completed;
-
-use "LK/ROOT.ML";
-use "ILL/ROOT.ML";
-use "Modal/ROOT.ML";