# HG changeset patch # User paulson # Date 844938543 -7200 # Node ID bcc9cbed10b1d2009aafe6884dc09accd952b306 # Parent 5963238bc1b607023f77fb938748a1e60c415c8f Removed LK since Sequents contains everything in it diff -r 5963238bc1b6 -r bcc9cbed10b1 src/LK/LK.ML --- 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)) ]); diff -r 5963238bc1b6 -r bcc9cbed10b1 src/LK/LK.thy --- 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')]; diff -r 5963238bc1b6 -r bcc9cbed10b1 src/LK/Makefile --- 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 diff -r 5963238bc1b6 -r bcc9cbed10b1 src/LK/README.html --- 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 @@ -LK/ReadMe - -

LK: Classical First-Order Sequent Calculus

- -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 - -
-
ROOT.ML -
loads all source files. Enter an ML image containing Pure -Isabelle and type: use "ROOT.ML";

- -

Makefile -
compiles the files under Poly/ML or SML of New Jersey

- -

ex -
subdirectory containing examples. To execute them, enter an ML image -containing LK and type: use "ex/ROOT.ML";

-

- -Useful references on First-Order Logic: - - - diff -r 5963238bc1b6 -r bcc9cbed10b1 src/LK/ROOT.ML --- 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*) diff -r 5963238bc1b6 -r bcc9cbed10b1 src/LK/ex/ROOT.ML --- 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"; diff -r 5963238bc1b6 -r bcc9cbed10b1 src/LK/ex/hardquant.ML --- 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*) diff -r 5963238bc1b6 -r bcc9cbed10b1 src/LK/ex/prop.ML --- 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."; diff -r 5963238bc1b6 -r bcc9cbed10b1 src/LK/ex/quant.ML --- 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*)