# HG changeset patch # User wenzelm # Date 918245657 -3600 # Node ID 935f183bf406f7239dbcc343eac05b2f70bc6680 # Parent 4d89d4f0ab17f7fefbbf88dbb48b3b211278ce48 examples made separate dirs; diff -r 4d89d4f0ab17 -r 935f183bf406 src/Sequents/ILL/ILL_kleene_lemmas.ML --- /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) *]"; + diff -r 4d89d4f0ab17 -r 935f183bf406 src/Sequents/ILL/ILL_predlog.ML --- /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]) ; diff -r 4d89d4f0ab17 -r 935f183bf406 src/Sequents/ILL/ILL_predlog.thy --- /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 diff -r 4d89d4f0ab17 -r 935f183bf406 src/Sequents/ILL/ROOT.ML --- /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"; diff -r 4d89d4f0ab17 -r 935f183bf406 src/Sequents/ILL/washing.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]); + + + + diff -r 4d89d4f0ab17 -r 935f183bf406 src/Sequents/ILL/washing.thy --- /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 diff -r 4d89d4f0ab17 -r 935f183bf406 src/Sequents/IsaMakefile --- 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 diff -r 4d89d4f0ab17 -r 935f183bf406 src/Sequents/LK/ROOT.ML --- /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"; diff -r 4d89d4f0ab17 -r 935f183bf406 src/Sequents/LK/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*) diff -r 4d89d4f0ab17 -r 935f183bf406 src/Sequents/LK/prop.ML --- /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."; diff -r 4d89d4f0ab17 -r 935f183bf406 src/Sequents/LK/quant.ML --- /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*) diff -r 4d89d4f0ab17 -r 935f183bf406 src/Sequents/Modal/ROOT.ML --- /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"; diff -r 4d89d4f0ab17 -r 935f183bf406 src/Sequents/Modal/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"; diff -r 4d89d4f0ab17 -r 935f183bf406 src/Sequents/Modal/S4thms.ML --- /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>- ((P>- []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"; + diff -r 4d89d4f0ab17 -r 935f183bf406 src/Sequents/Modal/Tthms.ML --- /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-- []P --> []Q"; +try "|- P --> <>P"; + +try "|- [](P & Q) <-> []P & []Q"; +try "|- <>(P | Q) <-> <>P | <>Q"; +try "|- [](P<->Q) <-> (P>-(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-- (P-- <>Q --> <>(P & Q)"; diff -r 4d89d4f0ab17 -r 935f183bf406 src/Sequents/ex/ILL/ILL_kleene_lemmas.ML --- 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) *]"; - diff -r 4d89d4f0ab17 -r 935f183bf406 src/Sequents/ex/ILL/ILL_predlog.ML --- 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]) ; diff -r 4d89d4f0ab17 -r 935f183bf406 src/Sequents/ex/ILL/ILL_predlog.thy --- 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 diff -r 4d89d4f0ab17 -r 935f183bf406 src/Sequents/ex/ILL/ROOT.ML --- 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"; diff -r 4d89d4f0ab17 -r 935f183bf406 src/Sequents/ex/ILL/washing.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]); - - - - diff -r 4d89d4f0ab17 -r 935f183bf406 src/Sequents/ex/ILL/washing.thy --- 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 diff -r 4d89d4f0ab17 -r 935f183bf406 src/Sequents/ex/LK/ROOT.ML --- 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"; diff -r 4d89d4f0ab17 -r 935f183bf406 src/Sequents/ex/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*) diff -r 4d89d4f0ab17 -r 935f183bf406 src/Sequents/ex/LK/prop.ML --- 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."; diff -r 4d89d4f0ab17 -r 935f183bf406 src/Sequents/ex/LK/quant.ML --- 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*) diff -r 4d89d4f0ab17 -r 935f183bf406 src/Sequents/ex/Modal/ROOT.ML --- 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"; diff -r 4d89d4f0ab17 -r 935f183bf406 src/Sequents/ex/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"; diff -r 4d89d4f0ab17 -r 935f183bf406 src/Sequents/ex/Modal/S4thms.ML --- 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>- ((P>- []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"; - diff -r 4d89d4f0ab17 -r 935f183bf406 src/Sequents/ex/Modal/Tthms.ML --- 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-- []P --> []Q"; -try "|- P --> <>P"; - -try "|- [](P & Q) <-> []P & []Q"; -try "|- <>(P | Q) <-> <>P | <>Q"; -try "|- [](P<->Q) <-> (P>-(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-- (P-- <>Q --> <>(P & Q)"; diff -r 4d89d4f0ab17 -r 935f183bf406 src/Sequents/ex/ROOT.ML --- 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";