--- a/src/LK/LK.ML Thu Oct 10 10:57:33 1996 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,194 +0,0 @@
-(* 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) ]);
-
-
-(**** Theorem Packs ****)
-
-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([],[]);
-
-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));
-
-(*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];
-
-
-
-(*Returns the list of all formulas in the sequent*)
-fun forms_of_seq (Const("Seqof",_) $ 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 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);
-
-
-(*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 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));
-
-(** 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)) ]);
--- a/src/LK/LK.thy Thu Oct 10 10:57:33 1996 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,135 +0,0 @@
-(* 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 = Pure +
-
-classes term < logic
-
-default term
-
-types
- o sequence seqobj seqcont sobj
-
-arities
- o :: logic
-
-consts
- 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)
-
- (*Representation of sequents*)
- Trueprop :: [sobj=>sobj, sobj=>sobj] => prop
- Seqof :: [o, sobj] => sobj
-
-syntax
- "@Trueprop" :: [sequence,sequence] => prop ("((_)/ |- (_))" [6,6] 5)
- NullSeq :: sequence ("" [] 1000)
- NonNullSeq :: [seqobj,seqcont] => sequence ("__" [] 1000)
- NullSeqCont :: seqcont ("" [] 1000)
- SeqCont :: [seqobj,seqcont] => seqcont (",/ __" [] 1000)
- "" :: o => seqobj ("_" [] 1000)
- SeqId :: id => seqobj ("$_" [] 1000)
- SeqVar :: var => seqobj ("$_")
-
-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
-
-(*Abstract over "sobj" -- representation of a sequence of formulae *)
-fun abs_sobj t = Abs("sobj", Type("sobj",[]), t);
-
-(*Representation of empty sequence*)
-val Sempty = abs_sobj (Bound 0);
-
-fun seq_obj_tr (Const("SeqId",_)$id) = id
- | seq_obj_tr (Const("SeqVar",_)$id) = id
- | seq_obj_tr (fm) = Const("Seqof",dummyT)$fm;
-
-fun seq_tr (_$obj$seq) = seq_obj_tr(obj)$seq_tr(seq)
- | seq_tr (_) = Bound 0;
-
-fun seq_tr1 (Const("NullSeq",_)) = Sempty
- | seq_tr1 (seq) = abs_sobj(seq_tr seq);
-
-fun true_tr[s1,s2] = Const("Trueprop",dummyT)$seq_tr1 s1$seq_tr1 s2;
-
-fun seq_obj_tr' (Const("Seqof",_)$fm) = fm
- | seq_obj_tr' (id) = Const("SeqId",dummyT)$id;
-
-fun seq_tr' (obj$sq,C) =
- let val sq' = case sq of
- Bound 0 => Const("NullSeqCont",dummyT)
- | _ => seq_tr'(sq,Const("SeqCont",dummyT))
- in C $ seq_obj_tr' obj $ sq' end;
-
-fun seq_tr1' (Bound 0) = Const("NullSeq",dummyT)
- | seq_tr1' s = seq_tr'(s,Const("NonNullSeq",dummyT));
-
-fun true_tr' [Abs(_,_,s1),Abs(_,_,s2)] =
- Const("@Trueprop",dummyT)$seq_tr1' s1$seq_tr1' s2;
-
-val parse_translation = [("@Trueprop",true_tr)];
-val print_translation = [("Trueprop",true_tr')];
--- a/src/LK/Makefile Thu Oct 10 10:57:33 1996 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,62 +0,0 @@
-# $Id$
-#########################################################################
-# #
-# Makefile for Isabelle (LK) #
-# #
-#########################################################################
-
-#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 Isabelle (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)
-FILES = ROOT.ML LK.thy LK.ML
-EX_FILES = ex/ROOT.ML ex/hardquant.ML ex/prop.ML ex/quant.ML
-
-$(BIN)/LK: $(BIN)/Pure $(FILES)
- case "$(COMP)" in \
- poly*) echo 'make_database"$(BIN)/LK"; quit();' \
- | $(COMP) $(BIN)/Pure;\
- if [ "$${MAKE_HTML}" = "true" ]; \
- then echo 'open PolyML; make_html := true; exit_use_dir".";' \
- | $(COMP) $(BIN)/LK;\
- elif [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
- then echo 'open PolyML; make_html := true; exit_use_dir"."; make_html := false;' | $(COMP) $(BIN)/LK;\
- else echo 'open PolyML; exit_use_dir".";' | $(COMP) $(BIN)/LK;\
- fi;\
- discgarb -c $(BIN)/LK;;\
- sml*) if [ "$${MAKE_HTML}" = "true" ]; \
- then echo 'make_html := true; exit_use_dir"."; xML"$(BIN)/LK" banner;' | $(BIN)/Pure;\
- elif [ "$${MAKE_HTML-undefined}" != "undefined" ];\
- then echo 'make_html := true; exit_use_dir"."; make_html := false; xML"$(BIN)/LK" banner;' \
- | $(BIN)/Pure;\
- else echo 'exit_use_dir"."; xML"$(BIN)/LK" banner;' \
- | $(BIN)/Pure;\
- fi;;\
- *) echo Bad value for ISABELLECOMP: \
- $(COMP) is not poly or sml;;\
- esac
-
-$(BIN)/Pure:
- cd ../Pure; $(MAKE)
-
-test: ex/ROOT.ML $(BIN)/LK $(EX_FILES)
- case "$(COMP)" in \
- poly*) echo 'exit_use"ex/ROOT.ML"; quit();' | $(COMP) $(BIN)/LK ;;\
- sml*) echo 'exit_use"ex/ROOT.ML";' | $(BIN)/LK;;\
- *) echo Bad value for ISABELLECOMP: \
- $(COMP) is not poly or sml;;\
- esac
-
-.PRECIOUS: $(BIN)/Pure $(BIN)/LK
--- a/src/LK/README.html Thu Oct 10 10:57:33 1996 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,30 +0,0 @@
-<HTML><HEAD><TITLE>LK/ReadMe</TITLE></HEAD><BODY>
-
-<H2>LK: Classical First-Order Sequent Calculus</H2>
-
-This directory contains the Standard ML sources of the Isabelle system for
-First-Order Logic as a classical sequent calculus. (For a Natural Deduction
-version, see FOL.) Important files include
-
-<DL>
-<DT>ROOT.ML
-<DD>loads all source files. Enter an ML image containing Pure
-Isabelle and type: use "ROOT.ML";<P>
-
-<DT>Makefile
-<DD>compiles the files under Poly/ML or SML of New Jersey<P>
-
-<DT>ex
-<DD>subdirectory containing examples. To execute them, enter an ML image
-containing LK and type: use "ex/ROOT.ML";<P>
-</DL>
-
-Useful references on First-Order Logic:
-
-<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>
-</BODY></HTML>
--- a/src/LK/ROOT.ML Thu Oct 10 10:57:33 1996 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,22 +0,0 @@
-(* Title: LK/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.
-Should be executed in the subdirectory LK.
-*)
-
-val banner = "Classical First-Order Sequent Calculus";
-writeln banner;
-
-init_thy_reader();
-
-print_depth 1;
-
-use_thy "LK";
-
-use "../Pure/install_pp.ML";
-print_depth 8;
-
-val LK_build_completed = (); (*indicate successful build*)
--- a/src/LK/ex/ROOT.ML Thu Oct 10 10:57:33 1996 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,18 +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.
-*)
-
-LK_build_completed; (*Cause examples to fail if LK did*)
-
-writeln"Root file for LK examples";
-
-proof_timing := true;
-time_use "ex/prop.ML";
-time_use "ex/quant.ML";
-time_use "ex/hardquant.ML";
-
-maketest"END: Root file for LK examples";
--- a/src/LK/ex/hardquant.ML Thu Oct 10 10:57:33 1996 +0200
+++ /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/LK/ex/prop.ML Thu Oct 10 10:57:33 1996 +0200
+++ /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/LK/ex/quant.ML Thu Oct 10 10:57:33 1996 +0200
+++ /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*)