# HG changeset patch # User wenzelm # Date 1164062830 -3600 # Node ID 87ac12bed1ab43e936e7be7f13738468b37b8af4 # Parent c11ab38b78a7968d51fd9733effaa6dbae767563 converted legacy ML scripts; diff -r c11ab38b78a7 -r 87ac12bed1ab src/Sequents/ILL/ILL_kleene_lemmas.ML --- a/src/Sequents/ILL/ILL_kleene_lemmas.ML Mon Nov 20 21:23:12 2006 +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 c11ab38b78a7 -r 87ac12bed1ab src/Sequents/ILL/ILL_predlog.ML --- a/src/Sequents/ILL/ILL_predlog.ML Mon Nov 20 21:23:12 2006 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,6 +0,0 @@ - -fun auto1 x = prove_goal (the_context ()) x - (fn prems => [best_tac safe_cs 1]) ; - -fun auto2 x = prove_goal (the_context ()) x - (fn prems => [best_tac power_cs 1]) ; diff -r c11ab38b78a7 -r 87ac12bed1ab src/Sequents/ILL/ILL_predlog.thy --- a/src/Sequents/ILL/ILL_predlog.thy Mon Nov 20 21:23:12 2006 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,33 +0,0 @@ -(* $Id$ *) - -theory ILL_predlog -imports ILL -begin - -typedecl plf - -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 c11ab38b78a7 -r 87ac12bed1ab src/Sequents/ILL/ROOT.ML --- a/src/Sequents/ILL/ROOT.ML Mon Nov 20 21:23:12 2006 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,5 +0,0 @@ -(* $Id$ *) - -time_use_thy "washing"; -time_use_thy "ILL_predlog"; -time_use "ILL_kleene_lemmas.ML"; diff -r c11ab38b78a7 -r 87ac12bed1ab src/Sequents/ILL/washing.ML --- a/src/Sequents/ILL/washing.ML Mon Nov 20 21:23:12 2006 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,28 +0,0 @@ -(* $Id$ *) - -(* "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 (the_context ()) "dollar , dirty , dollar |- clean" -(fn _ => [best_tac (lazy_cs add_safes (changeI @ load1I @ washI @ dryI)) 1]); - - -(* alternative formulation *) - -prove_goal (the_context ()) "dollar , dollar |- dirty -o clean" -(fn _ => [best_tac (lazy_cs add_safes (changeI @ load1I @ washI @ dryI)) 1]); diff -r c11ab38b78a7 -r 87ac12bed1ab src/Sequents/ILL/washing.thy --- a/src/Sequents/ILL/washing.thy Mon Nov 20 21:23:12 2006 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,38 +0,0 @@ - -(* $Id$ *) - -(* code by Sara Kalvala, based on Paulson's LK - and Moore's tisl.ML *) - -theory washing -imports ILL -begin - -consts - dollar :: o - quarter :: o - loaded :: o - dirty :: o - wet :: o - clean :: o - -axioms - 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" - -ML {* use_legacy_bindings (the_context ()) *} - -end - diff -r c11ab38b78a7 -r 87ac12bed1ab src/Sequents/ILL_predlog.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Sequents/ILL_predlog.thy Mon Nov 20 23:47:10 2006 +0100 @@ -0,0 +1,135 @@ +(* $Id$ *) + +theory ILL_predlog +imports ILL +begin + +typedecl plf + +consts + conj :: "[plf,plf] => plf" (infixr "&" 35) + disj :: "[plf,plf] => plf" (infixr "|" 35) + impl :: "[plf,plf] => plf" (infixr ">" 35) + eq :: "[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*])" *) + +method_setup auto1 = + {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (best_tac safe_cs)) *} "" +method_setup auto2 = + {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (best_tac power_cs)) *} "" + +(* from [kleene 52] pp 118,119 *) + +lemma k49a: "|- [* A > ( - ( - A)) *]" + by auto1 + +lemma k49b: "|- [*( - ( - ( - A))) = ( - A)*]" + by auto1 + +lemma k49c: "|- [* (A | - A) > ( - - A = A) *]" + by auto1 + +lemma k50a: "|- [* - (A = - A) *]" + by auto2 + +lemma k51a: "|- [* - - (A | - A) *]" + by auto1 + +lemma k51b: "|- [* - - (- - A > A) *]" + by auto2 + +lemma k56a: "|- [* (A | B) > - (- A & - B) *]" + by auto1 + +lemma k56b: "|- [* (-A | B) > - (A & -B) *]" + by auto1 + +lemma k57a: "|- [* (A & B) > - (-A | -B) *]" + by auto1 + +lemma k57b: "|- [* (A & -B) > -(-A | B) *]" + by auto2 + +lemma k58a: "|- [* (A > B) > - (A & -B) *]" + by auto1 + +lemma k58b: "|- [* (A > -B) = -(A & B) *]" + by auto1 + +lemma k58c: "|- [* - (A & B) = (- - A > - B) *]" + by auto1 + +lemma k58d: "|- [* (- - A > - B) = - - (-A | -B) *]" + by auto1 + +lemma k58e: "! [* - -B > B *] |- [* (- -A > B) = (A > B) *]" + by auto1 + +lemma k58f: "! [* - -B > B *] |- [* (A > B) = - (A & -B) *]" + by auto1 + +lemma k58g: "|- [* (- -A > B) > - (A & -B) *]" + by auto1 + +lemma k59a: "|- [* (-A | B) > (A > B) *]" + by auto1 + +lemma k59b: "|- [* (A > B) > - - (-A | B) *]" + by auto2 + +lemma k59c: "|- [* (-A > B) > - -(A | B) *]" + by auto2 + +lemma k60a: "|- [* (A & B) > - (A > -B) *]" + by auto1 + +lemma k60b: "|- [* (A & -B) > - (A > B) *]" + by auto1 + +lemma k60c: "|- [* ( - - A & B) > - (A > -B) *]" + by auto1 + +lemma k60d: "|- [* (- - A & - B) = - (A > B) *]" + by auto1 + +lemma k60e: "|- [* - (A > B) = - (-A | B) *]" + by auto1 + +lemma k60f: "|- [* - (-A | B) = - - (A & -B) *]" + by auto1 + +lemma k60g: "|- [* - - (A > B) = - (A & -B) *]" + by auto2 + +lemma k60h: "|- [* - (A & -B) = (A > - -B) *]" + by auto1 + +lemma k60i: "|- [* (A > - -B) = (- -A > - -B) *]" + by auto1 + +lemma k61a: "|- [* (A | B) > (-A > B) *]" + by auto1 + +lemma k61b: "|- [* - (A | B) = - (-A > B) *]" + by auto2 + +lemma k62a: "|- [* (-A | -B) > - (A & B) *]" + by auto1 + +end diff -r c11ab38b78a7 -r 87ac12bed1ab src/Sequents/IsaMakefile --- a/src/Sequents/IsaMakefile Mon Nov 20 21:23:12 2006 +0100 +++ b/src/Sequents/IsaMakefile Mon Nov 20 23:47:10 2006 +0100 @@ -8,7 +8,7 @@ default: Sequents images: Sequents -test: Sequents-ILL Sequents-LK Sequents-Modal +test: Sequents-LK all: images test @@ -26,42 +26,22 @@ Pure: @cd $(SRC)/Pure; $(ISATOOL) make Pure -$(OUT)/Sequents: $(OUT)/Pure ILL.ML ILL.thy LK0.ML LK0.thy LK.thy \ - modal.ML ROOT.ML simpdata.ML S4.ML \ - S4.thy S43.ML S43.thy Sequents.thy T.ML T.thy prover.ML +$(OUT)/Sequents: $(OUT)/Pure ILL.ML ILL.thy LK0.thy LK.thy \ + modal.ML ROOT.ML simpdata.ML S4.thy S43.thy Sequents.thy T.thy prover.ML \ + ILL_predlog.thy Washing.thy @$(ISATOOL) usedir -b $(OUT)/Pure Sequents -## Sequents-ILL - -Sequents-ILL: Sequents $(LOG)/Sequents-ILL.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 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 LK/Nat.thy LK/Nat.ML +$(LOG)/Sequents-LK.gz: $(OUT)/Sequents LK/ROOT.ML LK/Hard_Quantifiers.thy \ + LK/Propositional.thy LK/Quantifiers.thy LK/Nat.thy @$(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-ILL.gz \ - $(LOG)/Sequents-LK.gz $(LOG)/Sequents-Modal.gz + @rm -f $(OUT)/Sequents $(LOG)/Sequents.gz $(LOG)/Sequents-LK.gz diff -r c11ab38b78a7 -r 87ac12bed1ab src/Sequents/LK/Hard_Quantifiers.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Sequents/LK/Hard_Quantifiers.thy Mon Nov 20 23:47:10 2006 +0100 @@ -0,0 +1,271 @@ +(* Title: LK/Hard_Quantifiers.thy + 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. +*) + +theory Hard_Quantifiers +imports LK +begin + +lemma "|- (ALL x. P(x) & Q(x)) <-> (ALL x. P(x)) & (ALL x. Q(x))" + by fast + +lemma "|- (EX x. P-->Q(x)) <-> (P --> (EX x. Q(x)))" + by fast + +lemma "|- (EX x. P(x)-->Q) <-> (ALL x. P(x)) --> Q" + by fast + +lemma "|- (ALL x. P(x)) | Q <-> (ALL x. P(x) | Q)" + by fast + + +text "Problems requiring quantifier duplication" + +(*Not provable by fast: needs multiple instantiation of ALL*) +lemma "|- (ALL x. P(x)-->P(f(x))) & P(d)-->P(f(f(f(d))))" + by best_dup + +(*Needs double instantiation of the quantifier*) +lemma "|- EX x. P(x) --> P(a) & P(b)" + by fast_dup + +lemma "|- EX z. P(z) --> (ALL x. P(x))" + by best_dup + + +text "Hard examples with quantifiers" + +text "Problem 18" +lemma "|- EX y. ALL x. P(y)-->P(x)" + by best_dup + +text "Problem 19" +lemma "|- EX x. ALL y z. (P(y)-->Q(z)) --> (P(x)-->Q(x))" + by best_dup + +text "Problem 20" +lemma "|- (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 + +text "Problem 21" +lemma "|- (EX x. P-->Q(x)) & (EX x. Q(x)-->P) --> (EX x. P<->Q(x))" + by best_dup + +text "Problem 22" +lemma "|- (ALL x. P <-> Q(x)) --> (P <-> (ALL x. Q(x)))" + by fast + +text "Problem 23" +lemma "|- (ALL x. P | Q(x)) <-> (P | (ALL x. Q(x)))" + by best + +text "Problem 24" +lemma "|- ~(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 (tactic "pc_tac LK_pack 1") + +text "Problem 25" +lemma "|- (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 + +text "Problem 26" +lemma "|- ((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 (tactic "pc_tac LK_pack 1") + +text "Problem 27" +lemma "|- (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 (tactic "pc_tac LK_pack 1") + +text "Problem 28. AMENDED" +lemma "|- (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 (tactic "pc_tac LK_pack 1") + +text "Problem 29. Essentially the same as Principia Mathematica *11.71" +lemma "|- (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 (tactic "pc_tac LK_pack 1") + +text "Problem 30" +lemma "|- (ALL x. P(x) | Q(x) --> ~ R(x)) & + (ALL x. (Q(x) --> ~ S(x)) --> P(x) & R(x)) + --> (ALL x. S(x))" + by fast + +text "Problem 31" +lemma "|- ~(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 + +text "Problem 32" +lemma "|- (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 + +text "Problem 33" +lemma "|- (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 + +text "Problem 34 AMENDED (TWICE!!)" +(*Andrews's challenge*) +lemma "|- ((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 best_dup + +text "Problem 35" +lemma "|- EX x y. P(x,y) --> (ALL u v. P(u,v))" + by best_dup + +text "Problem 36" +lemma "|- (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 + +text "Problem 37" +lemma "|- (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 (tactic "pc_tac LK_pack 1") + +text "Problem 38" +lemma "|- (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 (tactic "pc_tac LK_pack 1") + +text "Problem 39" +lemma "|- ~ (EX x. ALL y. F(y,x) <-> ~F(y,y))" + by fast + +text "Problem 40. AMENDED" +lemma "|- (EX y. ALL x. F(x,y) <-> F(x,x)) --> + ~(ALL x. EX y. ALL z. F(z,y) <-> ~ F(z,x))" + by fast + +text "Problem 41" +lemma "|- (ALL z. EX y. ALL x. f(x,y) <-> f(x,z) & ~ f(x,x)) + --> ~ (EX z. ALL x. f(x,z))" + by fast + +text "Problem 42" +lemma "|- ~ (EX y. ALL x. p(x,y) <-> ~ (EX z. p(x,z) & p(z,x)))" + oops + +text "Problem 43" +lemma "|- (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)))" + oops + +text "Problem 44" +lemma "|- (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 + +text "Problem 45" +lemma "|- (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 + + +text "Problems (mainly) involving equality or functions" + +text "Problem 48" +lemma "|- (a=b | c=d) & (a=c | b=d) --> a=d | b=c" + by (tactic {* fast_tac (LK_pack add_safes [thm "subst"]) 1 *}) + +text "Problem 50" +lemma "|- (ALL x. P(a,x) | (ALL y. P(x,y))) --> (EX x. ALL y. P(x,y))" + by best_dup + +text "Problem 51" +lemma "|- (EX z w. ALL x y. P(x,y) <-> (x=z & y=w)) --> + (EX z. ALL x. EX w. (ALL y. P(x,y) <-> y=w) <-> x=z)" + by (tactic {* fast_tac (LK_pack add_safes [thm "subst"]) 1 *}) + +text "Problem 52" (*Almost the same as 51. *) +lemma "|- (EX z w. ALL x y. P(x,y) <-> (x=z & y=w)) --> + (EX w. ALL y. EX z. (ALL x. P(x,y) <-> x=z) <-> y=w)" + by (tactic {* fast_tac (LK_pack add_safes [thm "subst"]) 1 *}) + +text "Problem 56" +lemma "|- (ALL x.(EX y. P(y) & x=f(y)) --> P(x)) <-> (ALL x. P(x) --> P(f(x)))" + by (tactic {* best_tac (LK_pack add_unsafes [thm "symL", thm "subst"]) 1 *}) + (*requires tricker to orient the equality properly*) + +text "Problem 57" +lemma "|- 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 + +text "Problem 58!" +lemma "|- (ALL x y. f(x)=g(y)) --> (ALL x y. f(f(x))=f(g(y)))" + by (tactic {* fast_tac (LK_pack add_safes [thm "subst"]) 1 *}) + +text "Problem 59" +(*Unification works poorly here -- the abstraction %sobj prevents efficient + operation of the occurs check*) +ML {* Unify.trace_bound := !Unify.search_bound - 1 *} +lemma "|- (ALL x. P(x) <-> ~P(f(x))) --> (EX x. P(x) & ~P(f(x)))" + by best_dup + +text "Problem 60" +lemma "|- ALL x. P(x,f(x)) <-> (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))" + by fast + +text "Problem 62 as corrected in JAR 18 (1997), page 135" +lemma "|- (ALL x. p(a) & (p(x) --> p(f(x))) --> p(f(f(x)))) <-> + (ALL x. (~p(a) | p(x) | p(f(f(x)))) & + (~p(a) | ~p(f(x)) | p(f(f(x)))))" + by fast + +(*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*) +(*18 September 2005: loaded in 1.809 secs*) + +end diff -r c11ab38b78a7 -r 87ac12bed1ab src/Sequents/LK/Nat.ML --- a/src/Sequents/LK/Nat.ML Mon Nov 20 21:23:12 2006 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,49 +0,0 @@ -(* Title: Sequents/LK/Nat.ML - ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1999 University of Cambridge -*) - -Addsimps [Suc_neq_0]; - -Add_safes [Suc_inject RS L_of_imp]; - -Goal "|- Suc(k) ~= k"; -by (res_inst_tac [("n","k")] induct 1); -by (Simp_tac 1); -by (Fast_tac 1); -qed "Suc_n_not_n"; - -Goalw [add_def] "|- 0+n = n"; -by (rtac rec_0 1); -qed "add_0"; - -Goalw [add_def] "|- Suc(m)+n = Suc(m+n)"; -by (rtac rec_Suc 1); -qed "add_Suc"; - -Addsimps [add_0, add_Suc]; - -Goal "|- (k+m)+n = k+(m+n)"; -by (res_inst_tac [("n","k")] induct 1); -by (Simp_tac 1); -by (Asm_simp_tac 1); -qed "add_assoc"; - -Goal "|- m+0 = m"; -by (res_inst_tac [("n","m")] induct 1); -by (Simp_tac 1); -by (Asm_simp_tac 1); -qed "add_0_right"; - -Goal "|- m+Suc(n) = Suc(m+n)"; -by (res_inst_tac [("n","m")] induct 1); -by (ALLGOALS (Asm_simp_tac)); -qed "add_Suc_right"; - -(*Example used in Reference Manual, Doc/Ref/simplifier.tex*) -val [prem] = Goal "(!!n. |- f(Suc(n)) = Suc(f(n))) ==> |- f(i+j) = i+f(j)"; -by (res_inst_tac [("n","i")] induct 1); -by (Simp_tac 1); -by (simp_tac (simpset() addsimps [prem]) 1); -result(); diff -r c11ab38b78a7 -r 87ac12bed1ab src/Sequents/LK/Nat.thy --- a/src/Sequents/LK/Nat.thy Mon Nov 20 21:23:12 2006 +0100 +++ b/src/Sequents/LK/Nat.thy Mon Nov 20 23:47:10 2006 +0100 @@ -27,6 +27,52 @@ rec_Suc: "|- rec(Suc(m), a, f) = f(m, rec(m,a,f))" add_def: "m+n == rec(m, n, %x y. Suc(y))" -ML {* use_legacy_bindings (the_context ()) *} + +declare Suc_neq_0 [simp] + +lemma Suc_inject_rule: "$H, $G, m = n |- $E \ $H, Suc(m) = Suc(n), $G |- $E" + by (rule L_of_imp [OF Suc_inject]) + +lemma Suc_n_not_n: "|- Suc(k) ~= k" + apply (rule_tac n = k in induct) + apply (tactic {* simp_tac (LK_ss addsimps [thm "Suc_neq_0"]) 1 *}) + apply (tactic {* fast_tac (LK_pack add_safes [thm "Suc_inject_rule"]) 1 *}) + done + +lemma add_0: "|- 0+n = n" + apply (unfold add_def) + apply (rule rec_0) + done + +lemma add_Suc: "|- Suc(m)+n = Suc(m+n)" + apply (unfold add_def) + apply (rule rec_Suc) + done + +declare add_0 [simp] add_Suc [simp] + +lemma add_assoc: "|- (k+m)+n = k+(m+n)" + apply (rule_tac n = "k" in induct) + apply (tactic {* simp_tac (LK_ss addsimps [thm "add_0"]) 1 *}) + apply (tactic {* simp_tac (LK_ss addsimps [thm "add_Suc"]) 1 *}) + done + +lemma add_0_right: "|- m+0 = m" + apply (rule_tac n = "m" in induct) + apply (tactic {* simp_tac (LK_ss addsimps [thm "add_0"]) 1 *}) + apply (tactic {* simp_tac (LK_ss addsimps [thm "add_Suc"]) 1 *}) + done + +lemma add_Suc_right: "|- m+Suc(n) = Suc(m+n)" + apply (rule_tac n = "m" in induct) + apply (tactic {* simp_tac (LK_ss addsimps [thm "add_0"]) 1 *}) + apply (tactic {* simp_tac (LK_ss addsimps [thm "add_Suc"]) 1 *}) + done + +lemma "(!!n. |- f(Suc(n)) = Suc(f(n))) ==> |- f(i+j) = i+f(j)" + apply (rule_tac n = "i" in induct) + apply (tactic {* simp_tac (LK_ss addsimps [thm "add_0"]) 1 *}) + apply (tactic {* asm_simp_tac (LK_ss addsimps [thm "add_Suc"]) 1 *}) + done end diff -r c11ab38b78a7 -r 87ac12bed1ab src/Sequents/LK/Propositional.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Sequents/LK/Propositional.thy Mon Nov 20 23:47:10 2006 +0100 @@ -0,0 +1,160 @@ +(* Title: LK/Propositional.thy + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1992 University of Cambridge +*) + +header {* Classical sequent calculus: examples with propositional connectives *} + +theory Propositional +imports LK +begin + +text "absorptive laws of & and | " + +lemma "|- P & P <-> P" + by fast_prop + +lemma "|- P | P <-> P" + by fast_prop + + +text "commutative laws of & and | " + +lemma "|- P & Q <-> Q & P" + by fast_prop + +lemma "|- P | Q <-> Q | P" + by fast_prop + + +text "associative laws of & and | " + +lemma "|- (P & Q) & R <-> P & (Q & R)" + by fast_prop + +lemma "|- (P | Q) | R <-> P | (Q | R)" + by fast_prop + + +text "distributive laws of & and | " + +lemma "|- (P & Q) | R <-> (P | R) & (Q | R)" + by fast_prop + +lemma "|- (P | Q) & R <-> (P & R) | (Q & R)" + by fast_prop + + +text "Laws involving implication" + +lemma "|- (P|Q --> R) <-> (P-->R) & (Q-->R)" + by fast_prop + +lemma "|- (P & Q --> R) <-> (P--> (Q-->R))" + by fast_prop + +lemma "|- (P --> Q & R) <-> (P-->Q) & (P-->R)" + by fast_prop + + +text "Classical theorems" + +lemma "|- P|Q --> P| ~P&Q" + by fast_prop + +lemma "|- (P-->Q)&(~P-->R) --> (P&Q | R)" + by fast_prop + +lemma "|- P&Q | ~P&R <-> (P-->Q)&(~P-->R)" + by fast_prop + +lemma "|- (P-->Q) | (P-->R) <-> (P --> Q | R)" + by fast_prop + + +(*If and only if*) + +lemma "|- (P<->Q) <-> (Q<->P)" + by fast_prop + +lemma "|- ~ (P <-> ~P)" + by fast_prop + + +(*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*) +lemma "|- (P-->Q) <-> (~Q --> ~P)" + by fast_prop + +(*2*) +lemma "|- ~ ~ P <-> P" + by fast_prop + +(*3*) +lemma "|- ~(P-->Q) --> (Q-->P)" + by fast_prop + +(*4*) +lemma "|- (~P-->Q) <-> (~Q --> P)" + by fast_prop + +(*5*) +lemma "|- ((P|Q)-->(P|R)) --> (P|(Q-->R))" + by fast_prop + +(*6*) +lemma "|- P | ~ P" + by fast_prop + +(*7*) +lemma "|- P | ~ ~ ~ P" + by fast_prop + +(*8. Peirce's law*) +lemma "|- ((P-->Q) --> P) --> P" + by fast_prop + +(*9*) +lemma "|- ((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)" + by fast_prop + +(*10*) +lemma "Q-->R, R-->P&Q, P-->(Q|R) |- P<->Q" + by fast_prop + +(*11. Proved in each direction (incorrectly, says Pelletier!!) *) +lemma "|- P<->P" + by fast_prop + +(*12. "Dijkstra's law"*) +lemma "|- ((P <-> Q) <-> R) <-> (P <-> (Q <-> R))" + by fast_prop + +(*13. Distributive law*) +lemma "|- P | (Q & R) <-> (P | Q) & (P | R)" + by fast_prop + +(*14*) +lemma "|- (P <-> Q) <-> ((Q | ~P) & (~Q|P))" + by fast_prop + +(*15*) +lemma "|- (P --> Q) <-> (~P | Q)" + by fast_prop + +(*16*) +lemma "|- (P-->Q) | (Q-->P)" + by fast_prop + +(*17*) +lemma "|- ((P & (Q-->R))-->S) <-> ((~P | Q | S) & (~P | ~R | S))" + by fast_prop + +end diff -r c11ab38b78a7 -r 87ac12bed1ab src/Sequents/LK/Quantifiers.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Sequents/LK/Quantifiers.thy Mon Nov 20 23:47:10 2006 +0100 @@ -0,0 +1,143 @@ +(* Title: LK/Quantifiers.ML + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1992 University of Cambridge + +Classical sequent calculus: examples with quantifiers. +*) + +theory Quantifiers +imports LK +begin + +lemma "|- (ALL x. P) <-> P" + by fast + +lemma "|- (ALL x y. P(x,y)) <-> (ALL y x. P(x,y))" + by fast + +lemma "ALL u. P(u), ALL v. Q(v) |- ALL u v. P(u) & Q(v)" + by fast + + +text "Permutation of existential quantifier." + +lemma "|- (EX x y. P(x,y)) <-> (EX y x. P(x,y))" + by fast + +lemma "|- (ALL x. P(x) & Q(x)) <-> (ALL x. P(x)) & (ALL x. Q(x))" + by fast + +(*Converse is invalid*) +lemma "|- (ALL x. P(x)) | (ALL x. Q(x)) --> (ALL x. P(x)|Q(x))" + by fast + + +text "Pushing ALL into an implication." + +lemma "|- (ALL x. P --> Q(x)) <-> (P --> (ALL x. Q(x)))" + by fast + +lemma "|- (ALL x. P(x)-->Q) <-> ((EX x. P(x)) --> Q)" + by fast + +lemma "|- (EX x. P) <-> P" + by fast + + +text "Distribution of EX over disjunction." + +lemma "|- (EX x. P(x) | Q(x)) <-> (EX x. P(x)) | (EX x. Q(x))" + by fast + +(*Converse is invalid*) +lemma "|- (EX x. P(x) & Q(x)) --> (EX x. P(x)) & (EX x. Q(x))" + by fast + + +text "Harder examples: classical theorems." + +lemma "|- (EX x. P-->Q(x)) <-> (P --> (EX x. Q(x)))" + by fast + +lemma "|- (EX x. P(x)-->Q) <-> (ALL x. P(x)) --> Q" + by fast + +lemma "|- (ALL x. P(x)) | Q <-> (ALL x. P(x) | Q)" + by fast + + +text "Basic test of quantifier reasoning" + +lemma "|- (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))" + by fast + +lemma "|- (ALL x. Q(x)) --> (EX x. Q(x))" + by fast + + +text "The following are invalid!" + +(*INVALID*) +lemma "|- (ALL x. EX y. Q(x,y)) --> (EX y. ALL x. Q(x,y))" + apply fast? + apply (rule _) + oops + +(*INVALID*) +lemma "|- (EX x. Q(x)) --> (ALL x. Q(x))" + apply fast? + apply (rule _) + oops + +(*INVALID*) +lemma "|- P(?a) --> (ALL x. P(x))" + apply fast? + apply (rule _) + oops + +(*INVALID*) +lemma "|- (P(?a) --> (ALL x. Q(x))) --> (ALL x. P(x) --> Q(x))" + apply fast? + apply (rule _) + oops + + +text "Back to things that are provable..." + +lemma "|- (ALL x. P(x)-->Q(x)) & (EX x. P(x)) --> (EX x. Q(x))" + by fast + +(*An example of why exR should be delayed as long as possible*) +lemma "|- (P--> (EX x. Q(x))) & P--> (EX x. Q(x))" + by fast + + +text "Solving for a Var" + +lemma "|- (ALL x. P(x)-->Q(f(x))) & (ALL x. Q(x)-->R(g(x))) & P(d) --> R(?a)" + by fast + + +text "Principia Mathematica *11.53" + +lemma "|- (ALL x y. P(x) --> Q(y)) <-> ((EX x. P(x)) --> (ALL y. Q(y)))" + by fast + + +text "Principia Mathematica *11.55" + +lemma "|- (EX x y. P(x) & Q(x,y)) <-> (EX x. P(x) & (EX y. Q(x,y)))" + by fast + + +text "Principia Mathematica *11.61" + +lemma "|- (EX y. ALL x. P(x) --> Q(x,y)) --> (ALL x. P(x) --> (EX y. Q(x,y)))" + by fast + + +(*21 August 88: loaded in 45.7 secs*) +(*18 September 2005: loaded in 0.114 secs*) + +end diff -r c11ab38b78a7 -r 87ac12bed1ab src/Sequents/LK/ROOT.ML --- a/src/Sequents/LK/ROOT.ML Mon Nov 20 21:23:12 2006 +0100 +++ b/src/Sequents/LK/ROOT.ML Mon Nov 20 23:47:10 2006 +0100 @@ -6,7 +6,7 @@ Examples for Classical Logic. *) -time_use "prop.ML"; -time_use "quant.ML"; -time_use "hardquant.ML"; -time_use_thy "Nat"; +use_thy "Propositional"; +use_thy "Quantifiers"; +use_thy "Hard_Quantifiers"; +use_thy "Nat"; diff -r c11ab38b78a7 -r 87ac12bed1ab src/Sequents/LK/hardquant.ML --- a/src/Sequents/LK/hardquant.ML Mon Nov 20 21:23:12 2006 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,308 +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. -*) - -context (theory "LK"); - -Goal "|- (ALL x. P(x) & Q(x)) <-> (ALL x. P(x)) & (ALL x. Q(x))"; -by (Fast_tac 1); -result(); - -Goal "|- (EX x. P-->Q(x)) <-> (P --> (EX x. Q(x)))"; -by (Fast_tac 1); -result(); - -Goal "|- (EX x. P(x)-->Q) <-> (ALL x. P(x)) --> Q"; -by (Fast_tac 1); -result(); - -Goal "|- (ALL x. P(x)) | Q <-> (ALL x. P(x) | Q)"; -by (Fast_tac 1); -result(); - -writeln"Problems requiring quantifier duplication"; - -(*Not provable by Fast_tac: needs multiple instantiation of ALL*) -Goal "|- (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 "|- EX x. P(x) --> P(a) & P(b)"; -by (fast_tac LK_dup_pack 1); -result(); - -Goal "|- 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 "|- EX y. ALL x. P(y)-->P(x)"; -by (best_tac LK_dup_pack 1); -result(); - -writeln"Problem 19"; -Goal "|- 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 "|- (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 1); -result(); - -writeln"Problem 21"; -Goal "|- (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 "|- (ALL x. P <-> Q(x)) --> (P <-> (ALL x. Q(x)))"; -by (Fast_tac 1); -result(); - -writeln"Problem 23"; -Goal "|- (ALL x. P | Q(x)) <-> (P | (ALL x. Q(x)))"; -by (best_tac LK_pack 1); -result(); - -writeln"Problem 24"; -Goal "|- ~(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 "|- (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 "|- ((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 "|- (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 "|- (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 "|- (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 "|- (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 1); -result(); - -writeln"Problem 31"; -Goal "|- ~(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 1); -result(); - -writeln"Problem 32"; -Goal "|- (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 "|- (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 1); -result(); - -writeln"Problem 34 AMENDED (TWICE!!)"; -(*Andrews's challenge*) -Goal "|- ((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 (best_tac LK_dup_pack 1); (*10 secs!*) -result(); - - -writeln"Problem 35"; -Goal "|- EX x y. P(x,y) --> (ALL u v. P(u,v))"; -by (best_tac LK_dup_pack 1); -result(); - -writeln"Problem 36"; -Goal "|- (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 1); -result(); - -writeln"Problem 37"; -Goal "|- (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 "|- (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 "|- ~ (EX x. ALL y. F(y,x) <-> ~F(y,y))"; -by (Fast_tac 1); -result(); - -writeln"Problem 40. AMENDED"; -Goal "|- (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 1); -result(); - -writeln"Problem 41"; -Goal "|- (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 1); -result(); - -writeln"Problem 42"; -Goal "|- ~ (EX y. ALL x. p(x,y) <-> ~ (EX z. p(x,z) & p(z,x)))"; - -writeln"Problem 43 NOT PROVED AUTOMATICALLY"; -Goal "|- (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 "|- (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 1); -result(); - -writeln"Problem 45"; -Goal "|- (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"Problems (mainly) involving equality or functions"; - -writeln"Problem 48"; -Goal "|- (a=b | c=d) & (a=c | b=d) --> a=d | b=c"; -by (fast_tac (pack() add_safes [subst]) 1); -result(); - -writeln"Problem 50"; -Goal "|- (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 51"; -Goal "|- (EX z w. ALL x y. P(x,y) <-> (x=z & y=w)) --> \ -\ (EX z. ALL x. EX w. (ALL y. P(x,y) <-> y=w) <-> x=z)"; -by (fast_tac (pack() add_safes [subst]) 1); -result(); - -writeln"Problem 52"; -(*Almost the same as 51. *) -Goal "|- (EX z w. ALL x y. P(x,y) <-> (x=z & y=w)) --> \ -\ (EX w. ALL y. EX z. (ALL x. P(x,y) <-> x=z) <-> y=w)"; -by (fast_tac (pack() add_safes [subst]) 1); -result(); - -writeln"Problem 56"; -Goal "|- (ALL x.(EX y. P(y) & x=f(y)) --> P(x)) <-> (ALL x. P(x) --> P(f(x)))"; -by (best_tac (pack() add_unsafes [symL, subst]) 1); -(*requires tricker to orient the equality properly*) -result(); - -writeln"Problem 57"; -Goal "|- 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 1); -result(); - -writeln"Problem 58!"; -Goal "|- (ALL x y. f(x)=g(y)) --> (ALL x y. f(f(x))=f(g(y)))"; -by (fast_tac (pack() add_safes [subst]) 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 "|- (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 "|- ALL x. P(x,f(x)) <-> (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))"; -by (Fast_tac 1); -result(); - -writeln"Problem 62 as corrected in JAR 18 (1997), page 135"; -Goal "|- (ALL x. p(a) & (p(x) --> p(f(x))) --> p(f(f(x)))) <-> \ -\ (ALL x. (~p(a) | p(x) | p(f(f(x)))) & \ -\ (~p(a) | ~p(f(x)) | p(f(f(x)))))"; -by (Fast_tac 1); -result(); - -(*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*) -(*18 September 2005: loaded in 1.809 secs*) diff -r c11ab38b78a7 -r 87ac12bed1ab src/Sequents/LK/prop.ML --- a/src/Sequents/LK/prop.ML Mon Nov 20 21:23:12 2006 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,190 +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"absorptive laws of & and | "; - -goal (theory "LK") "|- P & P <-> P"; -by (fast_tac prop_pack 1); -result(); - -goal (theory "LK") "|- P | P <-> P"; -by (fast_tac prop_pack 1); -result(); - -writeln"commutative laws of & and | "; - -goal (theory "LK") "|- P & Q <-> Q & P"; -by (fast_tac prop_pack 1); -result(); - -goal (theory "LK") "|- P | Q <-> Q | P"; -by (fast_tac prop_pack 1); -result(); - - -writeln"associative laws of & and | "; - -goal (theory "LK") "|- (P & Q) & R <-> P & (Q & R)"; -by (fast_tac prop_pack 1); -result(); - -goal (theory "LK") "|- (P | Q) | R <-> P | (Q | R)"; -by (fast_tac prop_pack 1); -result(); - -writeln"distributive laws of & and | "; -goal (theory "LK") "|- (P & Q) | R <-> (P | R) & (Q | R)"; -by (fast_tac prop_pack 1); -result(); - -goal (theory "LK") "|- (P | Q) & R <-> (P & R) | (Q & R)"; -by (fast_tac prop_pack 1); -result(); - -writeln"Laws involving implication"; - -goal (theory "LK") "|- (P|Q --> R) <-> (P-->R) & (Q-->R)"; -by (fast_tac prop_pack 1); -result(); - -goal (theory "LK") "|- (P & Q --> R) <-> (P--> (Q-->R))"; -by (fast_tac prop_pack 1); -result(); - - -goal (theory "LK") "|- (P --> Q & R) <-> (P-->Q) & (P-->R)"; -by (fast_tac prop_pack 1); -result(); - - -writeln"Classical theorems"; - -goal (theory "LK") "|- P|Q --> P| ~P&Q"; -by (fast_tac prop_pack 1); -result(); - - -goal (theory "LK") "|- (P-->Q)&(~P-->R) --> (P&Q | R)"; -by (fast_tac prop_pack 1); -result(); - - -goal (theory "LK") "|- P&Q | ~P&R <-> (P-->Q)&(~P-->R)"; -by (fast_tac prop_pack 1); -result(); - - -goal (theory "LK") "|- (P-->Q) | (P-->R) <-> (P --> Q | R)"; -by (fast_tac prop_pack 1); -result(); - - -(*If and only if*) - -goal (theory "LK") "|- (P<->Q) <-> (Q<->P)"; -by (fast_tac prop_pack 1); -result(); - -goal (theory "LK") "|- ~ (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 (theory "LK") "|- (P-->Q) <-> (~Q --> ~P)"; -by (fast_tac prop_pack 1); -result(); - -(*2*) -goal (theory "LK") "|- ~ ~ P <-> P"; -by (fast_tac prop_pack 1); -result(); - -(*3*) -goal (theory "LK") "|- ~(P-->Q) --> (Q-->P)"; -by (fast_tac prop_pack 1); -result(); - -(*4*) -goal (theory "LK") "|- (~P-->Q) <-> (~Q --> P)"; -by (fast_tac prop_pack 1); -result(); - -(*5*) -goal (theory "LK") "|- ((P|Q)-->(P|R)) --> (P|(Q-->R))"; -by (fast_tac prop_pack 1); -result(); - -(*6*) -goal (theory "LK") "|- P | ~ P"; -by (fast_tac prop_pack 1); -result(); - -(*7*) -goal (theory "LK") "|- P | ~ ~ ~ P"; -by (fast_tac prop_pack 1); -result(); - -(*8. Peirce's law*) -goal (theory "LK") "|- ((P-->Q) --> P) --> P"; -by (fast_tac prop_pack 1); -result(); - -(*9*) -goal (theory "LK") "|- ((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)"; -by (fast_tac prop_pack 1); -result(); - -(*10*) -goal (theory "LK") "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 (theory "LK") "|- P<->P"; -by (fast_tac prop_pack 1); -result(); - -(*12. "Dijkstra's law"*) -goal (theory "LK") "|- ((P <-> Q) <-> R) <-> (P <-> (Q <-> R))"; -by (fast_tac prop_pack 1); -result(); - -(*13. Distributive law*) -goal (theory "LK") "|- P | (Q & R) <-> (P | Q) & (P | R)"; -by (fast_tac prop_pack 1); -result(); - -(*14*) -goal (theory "LK") "|- (P <-> Q) <-> ((Q | ~P) & (~Q|P))"; -by (fast_tac prop_pack 1); -result(); - - -(*15*) -goal (theory "LK") "|- (P --> Q) <-> (~P | Q)"; -by (fast_tac prop_pack 1); -result(); - -(*16*) -goal (theory "LK") "|- (P-->Q) | (Q-->P)"; -by (fast_tac prop_pack 1); -result(); - -(*17*) -goal (theory "LK") "|- ((P & (Q-->R))-->S) <-> ((~P | Q | S) & (~P | ~R | S))"; -by (fast_tac prop_pack 1); -result(); diff -r c11ab38b78a7 -r 87ac12bed1ab src/Sequents/LK/quant.ML --- a/src/Sequents/LK/quant.ML Mon Nov 20 21:23:12 2006 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,156 +0,0 @@ -(* Title: LK/ex/quant.ML - ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1992 University of Cambridge - -Classical sequent calculus: examples with quantifiers. -*) - -goal (theory "LK") "|- (ALL x. P) <-> P"; -by (fast_tac LK_pack 1); -result(); - -goal (theory "LK") "|- (ALL x y. P(x,y)) <-> (ALL y x. P(x,y))"; -by (fast_tac LK_pack 1); -result(); - -goal (theory "LK") "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 (theory "LK") "|- (EX x y. P(x,y)) <-> (EX y x. P(x,y))"; -by (fast_tac LK_pack 1); -result(); - -goal (theory "LK") "|- (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 (theory "LK") "|- (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 (theory "LK") "|- (ALL x. P --> Q(x)) <-> (P --> (ALL x. Q(x)))"; -by (fast_tac LK_pack 1); -result(); - - -goal (theory "LK") "|- (ALL x. P(x)-->Q) <-> ((EX x. P(x)) --> Q)"; -by (fast_tac LK_pack 1); -result(); - - -goal (theory "LK") "|- (EX x. P) <-> P"; -by (fast_tac LK_pack 1); -result(); - - -writeln"Distribution of EX over disjunction."; -goal (theory "LK") "|- (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 (theory "LK") "|- (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 (theory "LK") "|- (EX x. P-->Q(x)) <-> (P --> (EX x. Q(x)))"; -by (fast_tac LK_pack 1); -result(); -(*3 secs*) - - -goal (theory "LK") "|- (EX x. P(x)-->Q) <-> (ALL x. P(x)) --> Q"; -by (fast_tac LK_pack 1); -result(); -(*5 secs*) - - -goal (theory "LK") "|- (ALL x. P(x)) | Q <-> (ALL x. P(x) | Q)"; -by (fast_tac LK_pack 1); -result(); - - -writeln"Basic test of quantifier reasoning"; -goal (theory "LK") - "|- (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))"; -by (fast_tac LK_pack 1); -result(); - - -goal (theory "LK") "|- (ALL x. Q(x)) --> (EX x. Q(x))"; -by (fast_tac LK_pack 1); -result(); - - -writeln"The following are invalid!"; - -(*INVALID*) -goal (theory "LK") "|- (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 (theory "LK") "|- (EX x. Q(x)) --> (ALL x. Q(x))"; -by (fast_tac LK_pack 1) handle ERROR _ => writeln"Failed, as expected"; -getgoal 1; - -goal (theory "LK") "|- 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 (theory "LK") "|- (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 (theory "LK") "|- (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 (theory "LK") "|- (P--> (EX x. Q(x))) & P--> (EX x. Q(x))"; -by (fast_tac LK_pack 1); -result(); - -writeln"Solving for a Var"; -goal (theory "LK") - "|- (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 (theory "LK") - "|- (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 (theory "LK") "|- (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 (theory "LK") - "|- (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(); - -(*21 August 88: loaded in 45.7 secs*) -(*18 September 2005: loaded in 0.114 secs*) diff -r c11ab38b78a7 -r 87ac12bed1ab src/Sequents/LK0.ML --- a/src/Sequents/LK0.ML Mon Nov 20 21:23:12 2006 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,200 +0,0 @@ -(* Title: LK/LK0.ML - ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1992 University of Cambridge - -Tactics and lemmas for LK (thanks also to Philippe de Groote) - -Structural rules by Soren Heilmann -*) - -(** Structural Rules on formulas **) - -(*contraction*) - -Goal "$H |- $E, P, P, $F ==> $H |- $E, P, $F"; -by (etac contRS 1); -qed "contR"; - -Goal "$H, P, P, $G |- $E ==> $H, P, $G |- $E"; -by (etac contLS 1); -qed "contL"; - -(*thinning*) - -Goal "$H |- $E, $F ==> $H |- $E, P, $F"; -by (etac thinRS 1); -qed "thinR"; - -Goal "$H, $G |- $E ==> $H, P, $G |- $E"; -by (etac thinLS 1); -qed "thinL"; - -(*exchange*) - -Goal "$H |- $E, Q, P, $F ==> $H |- $E, P, Q, $F"; -by (etac exchRS 1); -qed "exchR"; - -Goal "$H, Q, P, $G |- $E ==> $H, P, Q, $G |- $E"; -by (etac exchLS 1); -qed "exchL"; - -(*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 **) -Goalw [iff_def] - "[| $H,P |- $E,Q,$F; $H,Q |- $E,P,$F |] ==> $H |- $E, P <-> Q, $F"; -by (REPEAT (ares_tac [conjR,impR] 1)); -qed "iffR"; - -Goalw [iff_def] - "[| $H,$G |- $E,P,Q; $H,Q,P,$G |- $E |] ==> $H, P <-> Q, $G |- $E"; -by (REPEAT (ares_tac [conjL,impL,basic] 1)); -qed "iffL"; - -Goal "$H |- $E, (P <-> P), $F"; -by (REPEAT (resolve_tac [iffR,basic] 1)); -qed "iff_refl"; - -Goalw [True_def] "$H |- $E, True, $F"; -by (rtac impR 1); -by (rtac basic 1); -qed "TrueR"; - -(*Descriptions*) -val [p1,p2] = Goal - "[| $H |- $E, P(a), $F; !!x. $H, P(x) |- $E, x=a, $F |] \ -\ ==> $H |- $E, (THE x. P(x)) = a, $F"; -by (rtac cut 1); -by (rtac p2 2); -by (rtac The 1 THEN rtac thinR 1 THEN rtac exchRS 1 THEN rtac p1 1); -by (rtac thinR 1 THEN rtac exchRS 1 THEN rtac p2 1); -qed "the_equality"; - -(** Weakened quantifier rules. Incomplete, they let the search terminate.**) - -Goal "$H, P(x), $G |- $E ==> $H, ALL x. P(x), $G |- $E"; -by (rtac allL 1); -by (etac thinL 1); -qed "allL_thin"; - -Goal "$H |- $E, P(x), $F ==> $H |- $E, EX x. P(x), $F"; -by (rtac exR 1); -by (etac thinR 1); -qed "exR_thin"; - - -(*The rules of LK*) -val prop_pack = empty_pack add_safes - [basic, refl, TrueR, FalseL, - 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, the_equality]; - -val LK_dup_pack = prop_pack add_safes [allR, exL] - add_unsafes [allL, exR, the_equality]; - - -pack_ref() := LK_pack; - -fun lemma_tac th i = - rtac (thinR RS cut) i THEN REPEAT (rtac thinL i) THEN rtac th i; - -val [major,minor] = goal (the_context ()) - "[| $H |- $E, $F, P --> Q; $H |- $E, $F, P |] ==> $H |- $E, Q, $F"; -by (rtac (thinRS RS cut) 1 THEN rtac major 1); -by (Step_tac 1); -by (rtac thinR 1 THEN rtac minor 1); -qed "mp_R"; - -val [major,minor] = goal (the_context ()) - "[| $H, $G |- $E, P --> Q; $H, $G, Q |- $E |] ==> $H, P, $G |- $E"; -by (rtac (thinL RS cut) 1 THEN rtac major 1); -by (Step_tac 1); -by (rtac thinL 1 THEN rtac minor 1); -qed "mp_L"; - - -(** Two rules to generate left- and right- rules from implications **) - -val [major,minor] = goal (the_context ()) - "[| |- P --> Q; $H |- $E, $F, P |] ==> $H |- $E, Q, $F"; -by (rtac mp_R 1); -by (rtac minor 2); -by (rtac thinRS 1 THEN rtac (major RS thinLS) 1); -qed "R_of_imp"; - -val [major,minor] = goal (the_context ()) - "[| |- P --> Q; $H, $G, Q |- $E |] ==> $H, P, $G |- $E"; -by (rtac mp_L 1); -by (rtac minor 2); -by (rtac thinRS 1 THEN rtac (major RS thinLS) 1); -qed "L_of_imp"; - -(*Can be used to create implications in a subgoal*) -val [prem] = goal (the_context ()) - "[| $H, $G |- $E, $F, P --> Q |] ==> $H, P, $G |- $E, Q, $F"; -by (rtac mp_L 1); -by (rtac basic 2); -by (rtac thinR 1 THEN rtac prem 1); -qed "backwards_impR"; - -Goal "|-P&Q ==> |-P"; -by (etac (thinR RS cut) 1); -by (Fast_tac 1); -qed "conjunct1"; - -Goal "|-P&Q ==> |-Q"; -by (etac (thinR RS cut) 1); -by (Fast_tac 1); -qed "conjunct2"; - -Goal "|- (ALL x. P(x)) ==> |- P(x)"; -by (etac (thinR RS cut) 1); -by (Fast_tac 1); -qed "spec"; - -(** Equality **) - -Goal "|- a=b --> b=a"; -by (safe_tac (LK_pack add_safes [subst]) 1); -qed "sym"; - -Goal "|- a=b --> b=c --> a=c"; -by (safe_tac (LK_pack add_safes [subst]) 1); -qed "trans"; - -(* Symmetry of equality in hypotheses *) -bind_thm ("symL", sym RS L_of_imp); - -(* Symmetry of equality in hypotheses *) -bind_thm ("symR", sym RS R_of_imp); - -Goal "[| $H|- $E, $F, a=b; $H|- $E, $F, b=c |] ==> $H|- $E, a=c, $F"; -by (rtac (trans RS R_of_imp RS mp_R) 1); -by (ALLGOALS assume_tac); -qed "transR"; - - -(* Two theorms for rewriting only one instance of a definition: - the first for definitions of formulae and the second for terms *) - -val prems = goal (the_context ()) "(A == B) ==> |- A <-> B"; -by (rewrite_goals_tac prems); -by (rtac iff_refl 1); -qed "def_imp_iff"; - -val prems = goal (the_context ()) "(A == B) ==> |- A = B"; -by (rewrite_goals_tac prems); -by (rtac refl 1); -qed "meta_eq_to_obj_eq"; diff -r c11ab38b78a7 -r 87ac12bed1ab src/Sequents/LK0.thy --- a/src/Sequents/LK0.thy Mon Nov 20 21:23:12 2006 +0100 +++ b/src/Sequents/LK0.thy Mon Nov 20 23:47:10 2006 +0100 @@ -132,8 +132,262 @@ setup prover_setup -ML {* use_legacy_bindings (the_context ()) *} + +(** Structural Rules on formulas **) + +(*contraction*) + +lemma contR: "$H |- $E, P, P, $F ==> $H |- $E, P, $F" + by (rule contRS) + +lemma contL: "$H, P, P, $G |- $E ==> $H, P, $G |- $E" + by (rule contLS) + +(*thinning*) + +lemma thinR: "$H |- $E, $F ==> $H |- $E, P, $F" + by (rule thinRS) + +lemma thinL: "$H, $G |- $E ==> $H, P, $G |- $E" + by (rule thinLS) + +(*exchange*) + +lemma exchR: "$H |- $E, Q, P, $F ==> $H |- $E, P, Q, $F" + by (rule exchRS) + +lemma exchL: "$H, Q, P, $G |- $E ==> $H, P, Q, $G |- $E" + by (rule exchLS) + +ML {* +local + val thinR = thm "thinR" + val thinL = thm "thinL" + val cut = thm "cut" +in + +(*Cut and thin, replacing the right-side formula*) +fun cutR_tac s i = + res_inst_tac [ ("P", s) ] cut i THEN rtac thinR i + +(*Cut and thin, replacing the left-side formula*) +fun cutL_tac s i = + res_inst_tac [("P", s)] cut i THEN rtac thinL (i+1) end +*} + + +(** If-and-only-if rules **) +lemma iffR: + "[| $H,P |- $E,Q,$F; $H,Q |- $E,P,$F |] ==> $H |- $E, P <-> Q, $F" + apply (unfold iff_def) + apply (assumption | rule conjR impR)+ + done + +lemma iffL: + "[| $H,$G |- $E,P,Q; $H,Q,P,$G |- $E |] ==> $H, P <-> Q, $G |- $E" + apply (unfold iff_def) + apply (assumption | rule conjL impL basic)+ + done + +lemma iff_refl: "$H |- $E, (P <-> P), $F" + apply (rule iffR basic)+ + done + +lemma TrueR: "$H |- $E, True, $F" + apply (unfold True_def) + apply (rule impR) + apply (rule basic) + done + +(*Descriptions*) +lemma the_equality: + assumes p1: "$H |- $E, P(a), $F" + and p2: "!!x. $H, P(x) |- $E, x=a, $F" + shows "$H |- $E, (THE x. P(x)) = a, $F" + apply (rule cut) + apply (rule_tac [2] p2) + apply (rule The, rule thinR, rule exchRS, rule p1) + apply (rule thinR, rule exchRS, rule p2) + done + + +(** Weakened quantifier rules. Incomplete, they let the search terminate.**) + +lemma allL_thin: "$H, P(x), $G |- $E ==> $H, ALL x. P(x), $G |- $E" + apply (rule allL) + apply (erule thinL) + done + +lemma exR_thin: "$H |- $E, P(x), $F ==> $H |- $E, EX x. P(x), $F" + apply (rule exR) + apply (erule thinR) + done + +(*The rules of LK*) + +ML {* +val prop_pack = empty_pack add_safes + [thm "basic", thm "refl", thm "TrueR", thm "FalseL", + thm "conjL", thm "conjR", thm "disjL", thm "disjR", thm "impL", thm "impR", + thm "notL", thm "notR", thm "iffL", thm "iffR"]; + +val LK_pack = prop_pack add_safes [thm "allR", thm "exL"] + add_unsafes [thm "allL_thin", thm "exR_thin", thm "the_equality"]; + +val LK_dup_pack = prop_pack add_safes [thm "allR", thm "exL"] + add_unsafes [thm "allL", thm "exR", thm "the_equality"]; + + +pack_ref() := LK_pack; + +local + val thinR = thm "thinR" + val thinL = thm "thinL" + val cut = thm "cut" +in + +fun lemma_tac th i = + rtac (thinR RS cut) i THEN REPEAT (rtac thinL i) THEN rtac th i; + +end; +*} + +method_setup fast_prop = + {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (fast_tac prop_pack)) *} + "propositional reasoning" + +method_setup fast = + {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (fast_tac LK_pack)) *} + "classical reasoning" + +method_setup fast_dup = + {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (fast_tac LK_dup_pack)) *} + "classical reasoning" + +method_setup best = + {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (best_tac LK_pack)) *} + "classical reasoning" + +method_setup best_dup = + {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (best_tac LK_dup_pack)) *} + "classical reasoning" +lemma mp_R: + assumes major: "$H |- $E, $F, P --> Q" + and minor: "$H |- $E, $F, P" + shows "$H |- $E, Q, $F" + apply (rule thinRS [THEN cut], rule major) + apply (tactic "step_tac LK_pack 1") + apply (rule thinR, rule minor) + done + +lemma mp_L: + assumes major: "$H, $G |- $E, P --> Q" + and minor: "$H, $G, Q |- $E" + shows "$H, P, $G |- $E" + apply (rule thinL [THEN cut], rule major) + apply (tactic "step_tac LK_pack 1") + apply (rule thinL, rule minor) + done + + +(** Two rules to generate left- and right- rules from implications **) + +lemma R_of_imp: + assumes major: "|- P --> Q" + and minor: "$H |- $E, $F, P" + shows "$H |- $E, Q, $F" + apply (rule mp_R) + apply (rule_tac [2] minor) + apply (rule thinRS, rule major [THEN thinLS]) + done + +lemma L_of_imp: + assumes major: "|- P --> Q" + and minor: "$H, $G, Q |- $E" + shows "$H, P, $G |- $E" + apply (rule mp_L) + apply (rule_tac [2] minor) + apply (rule thinRS, rule major [THEN thinLS]) + done + +(*Can be used to create implications in a subgoal*) +lemma backwards_impR: + assumes prem: "$H, $G |- $E, $F, P --> Q" + shows "$H, P, $G |- $E, Q, $F" + apply (rule mp_L) + apply (rule_tac [2] basic) + apply (rule thinR, rule prem) + done + +lemma conjunct1: "|-P&Q ==> |-P" + apply (erule thinR [THEN cut]) + apply fast + done + +lemma conjunct2: "|-P&Q ==> |-Q" + apply (erule thinR [THEN cut]) + apply fast + done + +lemma spec: "|- (ALL x. P(x)) ==> |- P(x)" + apply (erule thinR [THEN cut]) + apply fast + done + + +(** Equality **) + +lemma sym: "|- a=b --> b=a" + by (tactic {* safe_tac (LK_pack add_safes [thm "subst"]) 1 *}) + +lemma trans: "|- a=b --> b=c --> a=c" + by (tactic {* safe_tac (LK_pack add_safes [thm "subst"]) 1 *}) + +(* Symmetry of equality in hypotheses *) +lemmas symL = sym [THEN L_of_imp, standard] + +(* Symmetry of equality in hypotheses *) +lemmas symR = sym [THEN R_of_imp, standard] + +lemma transR: "[| $H|- $E, $F, a=b; $H|- $E, $F, b=c |] ==> $H|- $E, a=c, $F" + by (rule trans [THEN R_of_imp, THEN mp_R]) + +(* Two theorms for rewriting only one instance of a definition: + the first for definitions of formulae and the second for terms *) + +lemma def_imp_iff: "(A == B) ==> |- A <-> B" + apply unfold + apply (rule iff_refl) + done + +lemma meta_eq_to_obj_eq: "(A == B) ==> |- A = B" + apply unfold + apply (rule refl) + done + + +(** if-then-else rules **) + +lemma if_True: "|- (if True then x else y) = x" + unfolding If_def by fast + +lemma if_False: "|- (if False then x else y) = y" + unfolding If_def by fast + +lemma if_P: "|- P ==> |- (if P then x else y) = x" + apply (unfold If_def) + apply (erule thinR [THEN cut]) + apply fast + done + +lemma if_not_P: "|- ~P ==> |- (if P then x else y) = y"; + apply (unfold If_def) + apply (erule thinR [THEN cut]) + apply fast + done + +end diff -r c11ab38b78a7 -r 87ac12bed1ab src/Sequents/Modal/ROOT.ML --- a/src/Sequents/Modal/ROOT.ML Mon Nov 20 21:23:12 2006 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,22 +0,0 @@ -(* Title: Modal/ex/ROOT.ML - ID: $Id$ - Author: Martin Coen - Copyright 1991 University of Cambridge -*) - -writeln "\nTheorems of T\n"; -fun try s = (writeln s; prove_goal (theory "T") s (fn _=> [T_Prover.solve_tac 2])); -time_use "Tthms.ML"; - -writeln "\nTheorems of S4\n"; -fun try s = (writeln s; prove_goal (theory "S4") 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 (theory "S43") 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 c11ab38b78a7 -r 87ac12bed1ab src/Sequents/Modal/S43thms.ML --- a/src/Sequents/Modal/S43thms.ML Mon Nov 20 21:23:12 2006 +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 c11ab38b78a7 -r 87ac12bed1ab src/Sequents/Modal/S4thms.ML --- a/src/Sequents/Modal/S4thms.ML Mon Nov 20 21:23:12 2006 +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 c11ab38b78a7 -r 87ac12bed1ab src/Sequents/Modal/Tthms.ML --- a/src/Sequents/Modal/Tthms.ML Mon Nov 20 21:23:12 2006 +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 c11ab38b78a7 -r 87ac12bed1ab src/Sequents/Modal0.ML --- a/src/Sequents/Modal0.ML Mon Nov 20 21:23:12 2006 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,30 +0,0 @@ -(* Title: Modal/modal0 - ID: $Id$ - Author: Martin Coen - Copyright 1991 University of Cambridge -*) - -structure Modal0_rls = -struct - -val rewrite_rls = [strimp_def,streqv_def]; - -local - val iffR = prove_goal (the_context ()) - "[| $H,P |- $E,Q,$F; $H,Q |- $E,P,$F |] ==> $H |- $E, P <-> Q, $F" - (fn prems=> - [ (rewtac iff_def), - (REPEAT (resolve_tac (prems@[conjR,impR]) 1)) ]); - - val iffL = prove_goal (the_context ()) - "[| $H,$G |- $E,P,Q; $H,Q,P,$G |- $E |] ==> $H, P <-> Q, $G |- $E" - (fn prems=> - [ rewtac iff_def, - (REPEAT (resolve_tac (prems@[conjL,impL,basic]) 1)) ]) -in -val safe_rls = [basic,conjL,conjR,disjL,disjR,impL,impR,notL,notR,iffL,iffR]; -val unsafe_rls = [allR,exL]; -val bound_rls = [allL,exR]; -end - -end; diff -r c11ab38b78a7 -r 87ac12bed1ab src/Sequents/Modal0.thy --- a/src/Sequents/Modal0.thy Mon Nov 20 21:23:12 2006 +0100 +++ b/src/Sequents/Modal0.thy Mon Nov 20 23:47:10 2006 +0100 @@ -12,8 +12,8 @@ consts box :: "o=>o" ("[]_" [50] 50) dia :: "o=>o" ("<>_" [50] 50) - "--<" :: "[o,o]=>o" (infixr 25) - ">-<" :: "[o,o]=>o" (infixr 25) + strimp :: "[o,o]=>o" (infixr "--<" 25) + streqv :: "[o,o]=>o" (infixr ">-<" 25) Lstar :: "two_seqi" Rstar :: "two_seqi" @@ -38,6 +38,23 @@ strimp_def: "P --< Q == [](P --> Q)" streqv_def: "P >-< Q == (P --< Q) & (Q --< P)" -ML {* use_legacy_bindings (the_context ()) *} + +lemmas rewrite_rls = strimp_def streqv_def + +lemma iffR: + "[| $H,P |- $E,Q,$F; $H,Q |- $E,P,$F |] ==> $H |- $E, P <-> Q, $F" + apply (unfold iff_def) + apply (assumption | rule conjR impR)+ + done + +lemma iffL: + "[| $H,$G |- $E,P,Q; $H,Q,P,$G |- $E |] ==> $H, P <-> Q, $G |- $E" + apply (unfold iff_def) + apply (assumption | rule conjL impL basic)+ + done + +lemmas safe_rls = basic conjL conjR disjL disjR impL impR notL notR iffL iffR + and unsafe_rls = allR exL + and bound_rls = allL exR end diff -r c11ab38b78a7 -r 87ac12bed1ab src/Sequents/ROOT.ML --- a/src/Sequents/ROOT.ML Mon Nov 20 21:23:12 2006 +0100 +++ b/src/Sequents/ROOT.ML Mon Nov 20 23:47:10 2006 +0100 @@ -13,7 +13,11 @@ Unify.search_bound := 40; use_thy "LK"; + use_thy "ILL"; +use_thy "ILL_predlog"; +use_thy "Washing"; + use_thy "Modal0"; use_thy"T"; use_thy"S4"; diff -r c11ab38b78a7 -r 87ac12bed1ab src/Sequents/S4.ML --- a/src/Sequents/S4.ML Mon Nov 20 21:23:12 2006 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,17 +0,0 @@ -(* Title: Modal/S4.ML - ID: $Id$ - Author: Martin Coen - Copyright 1991 University of Cambridge -*) - -local open Modal0_rls -in structure MP_Rule : MODAL_PROVER_RULE = - struct - val rewrite_rls = rewrite_rls - val safe_rls = safe_rls - val unsafe_rls = unsafe_rls @ [boxR,diaL] - val bound_rls = bound_rls @ [boxL,diaR] - val aside_rls = [lstar0,lstar1,lstar2,rstar0,rstar1,rstar2] - end; -end; -structure S4_Prover = Modal_ProverFun(MP_Rule); diff -r c11ab38b78a7 -r 87ac12bed1ab src/Sequents/S4.thy --- a/src/Sequents/S4.thy Mon Nov 20 21:23:12 2006 +0100 +++ b/src/Sequents/S4.thy Mon Nov 20 23:47:10 2006 +0100 @@ -32,6 +32,81 @@ "[| $E |L> $E'; $F |L> $F'; $G |R> $G'; $E', P, $F' |- $G'|] ==> $E, <>P, $F |- $G" -ML {* use_legacy_bindings (the_context ()) *} +ML {* +structure S4_Prover = Modal_ProverFun +( + val rewrite_rls = thms "rewrite_rls" + val safe_rls = thms "safe_rls" + val unsafe_rls = thms "unsafe_rls" @ [thm "boxR", thm "diaL"] + val bound_rls = thms "bound_rls" @ [thm "boxL", thm "diaR"] + val aside_rls = [thm "lstar0", thm "lstar1", thm "lstar2", thm "rstar0", + thm "rstar1", thm "rstar2"] +) +*} + +method_setup S4_solve = +{* Method.no_args (Method.SIMPLE_METHOD (S4_Prover.solve_tac 2)) *} "S4 solver" + + +(* Theorems of system T from Hughes and Cresswell and Hailpern, LNCS 129 *) + +lemma "|- []P --> P" by S4_solve +lemma "|- [](P-->Q) --> ([]P-->[]Q)" by S4_solve (* normality*) +lemma "|- (P-- []P --> []Q" by S4_solve +lemma "|- P --> <>P" by S4_solve + +lemma "|- [](P & Q) <-> []P & []Q" by S4_solve +lemma "|- <>(P | Q) <-> <>P | <>Q" by S4_solve +lemma "|- [](P<->Q) <-> (P>-(P-->Q) <-> ([]P--><>Q)" by S4_solve +lemma "|- []P <-> ~<>(~P)" by S4_solve +lemma "|- [](~P) <-> ~<>P" by S4_solve +lemma "|- ~[]P <-> <>(~P)" by S4_solve +lemma "|- [][]P <-> ~<><>(~P)" by S4_solve +lemma "|- ~<>(P | Q) <-> ~<>P & ~<>Q" by S4_solve + +lemma "|- []P | []Q --> [](P | Q)" by S4_solve +lemma "|- <>(P & Q) --> <>P & <>Q" by S4_solve +lemma "|- [](P | Q) --> []P | <>Q" by S4_solve +lemma "|- <>P & []Q --> <>(P & Q)" by S4_solve +lemma "|- [](P | Q) --> <>P | []Q" by S4_solve +lemma "|- <>(P-->(Q & R)) --> ([]P --> <>Q) & ([]P--><>R)" by S4_solve +lemma "|- (P-- (P-- <>Q --> <>(P & Q)" by S4_solve + + +(* Theorems of system S4 from Hughes and Cresswell, p.46 *) + +lemma "|- []A --> A" by S4_solve (* refexivity *) +lemma "|- []A --> [][]A" by S4_solve (* transitivity *) +lemma "|- []A --> <>A" by S4_solve (* seriality *) +lemma "|- <>[](<>A --> []<>A)" by S4_solve +lemma "|- <>[](<>[]A --> []A)" by S4_solve +lemma "|- []P <-> [][]P" by S4_solve +lemma "|- <>P <-> <><>P" by S4_solve +lemma "|- <>[]<>P --> <>P" by S4_solve +lemma "|- []<>P <-> []<>[]<>P" by S4_solve +lemma "|- <>[]P <-> <>[]<>[]P" by S4_solve + +(* Theorems for system S4 from Hughes and Cresswell, p.60 *) + +lemma "|- []P | []Q <-> []([]P | []Q)" by S4_solve +lemma "|- ((P>- ((P>- []P & []Q" by S4_solve +lemma "|- <>(P | Q) <-> <>P | <>Q" by S4_solve +lemma "|- <>(P --> Q) <-> ([]P --> <>Q)" by S4_solve + +lemma "|- [](P --> Q) --> (<>P --> <>Q)" by S4_solve +lemma "|- []P --> []<>P" by S4_solve +lemma "|- <>[]P --> <>P" by S4_solve + +lemma "|- []P | []Q --> [](P | Q)" by S4_solve +lemma "|- <>(P & Q) --> <>P & <>Q" by S4_solve +lemma "|- [](P | Q) --> []P | <>Q" by S4_solve +lemma "|- <>P & []Q --> <>(P & Q)" by S4_solve +lemma "|- [](P | Q) --> <>P | []Q" by S4_solve end diff -r c11ab38b78a7 -r 87ac12bed1ab src/Sequents/S43.ML --- a/src/Sequents/S43.ML Mon Nov 20 21:23:12 2006 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,17 +0,0 @@ -(* Title: Modal/S43 - ID: $Id$ - Author: Martin Coen - Copyright 1991 University of Cambridge -*) - -local open Modal0_rls -in structure MP_Rule : MODAL_PROVER_RULE = - struct - val rewrite_rls = rewrite_rls - val safe_rls = safe_rls - val unsafe_rls = unsafe_rls @ [pi1,pi2] - val bound_rls = bound_rls @ [boxL,diaR] - val aside_rls = [lstar0,lstar1,lstar2,rstar0,rstar1,rstar2,S43pi0,S43pi1,S43pi2] - end; -end; -structure S43_Prover = Modal_ProverFun(MP_Rule); diff -r c11ab38b78a7 -r 87ac12bed1ab src/Sequents/S43.thy --- a/src/Sequents/S43.thy Mon Nov 20 21:23:12 2006 +0100 +++ b/src/Sequents/S43.thy Mon Nov 20 23:47:10 2006 +0100 @@ -77,6 +77,130 @@ S43pi ; $Ldia;; $Rbox; $Lbox; $Rdia |] ==> $L |- $R1, []P, $R2" -ML {* use_legacy_bindings (the_context ()) *} + +ML {* +structure S43_Prover = Modal_ProverFun +( + val rewrite_rls = thms "rewrite_rls" + val safe_rls = thms "safe_rls" + val unsafe_rls = thms "unsafe_rls" @ [thm "pi1", thm "pi2"] + val bound_rls = thms "bound_rls" @ [thm "boxL", thm "diaR"] + val aside_rls = [thm "lstar0", thm "lstar1", thm "lstar2", thm "rstar0", + thm "rstar1", thm "rstar2", thm "S43pi0", thm "S43pi1", thm "S43pi2"] +) +*} + + +method_setup S43_solve = {* + Method.no_args (Method.SIMPLE_METHOD + (S43_Prover.solve_tac 2 ORELSE S43_Prover.solve_tac 3)) +*} "S4 solver" + + +(* Theorems of system T from Hughes and Cresswell and Hailpern, LNCS 129 *) + +lemma "|- []P --> P" by S43_solve +lemma "|- [](P-->Q) --> ([]P-->[]Q)" by S43_solve (* normality*) +lemma "|- (P-- []P --> []Q" by S43_solve +lemma "|- P --> <>P" by S43_solve + +lemma "|- [](P & Q) <-> []P & []Q" by S43_solve +lemma "|- <>(P | Q) <-> <>P | <>Q" by S43_solve +lemma "|- [](P<->Q) <-> (P>-(P-->Q) <-> ([]P--><>Q)" by S43_solve +lemma "|- []P <-> ~<>(~P)" by S43_solve +lemma "|- [](~P) <-> ~<>P" by S43_solve +lemma "|- ~[]P <-> <>(~P)" by S43_solve +lemma "|- [][]P <-> ~<><>(~P)" by S43_solve +lemma "|- ~<>(P | Q) <-> ~<>P & ~<>Q" by S43_solve + +lemma "|- []P | []Q --> [](P | Q)" by S43_solve +lemma "|- <>(P & Q) --> <>P & <>Q" by S43_solve +lemma "|- [](P | Q) --> []P | <>Q" by S43_solve +lemma "|- <>P & []Q --> <>(P & Q)" by S43_solve +lemma "|- [](P | Q) --> <>P | []Q" by S43_solve +lemma "|- <>(P-->(Q & R)) --> ([]P --> <>Q) & ([]P--><>R)" by S43_solve +lemma "|- (P-- (P-- <>Q --> <>(P & Q)" by S43_solve + + +(* Theorems of system S4 from Hughes and Cresswell, p.46 *) + +lemma "|- []A --> A" by S43_solve (* refexivity *) +lemma "|- []A --> [][]A" by S43_solve (* transitivity *) +lemma "|- []A --> <>A" by S43_solve (* seriality *) +lemma "|- <>[](<>A --> []<>A)" by S43_solve +lemma "|- <>[](<>[]A --> []A)" by S43_solve +lemma "|- []P <-> [][]P" by S43_solve +lemma "|- <>P <-> <><>P" by S43_solve +lemma "|- <>[]<>P --> <>P" by S43_solve +lemma "|- []<>P <-> []<>[]<>P" by S43_solve +lemma "|- <>[]P <-> <>[]<>[]P" by S43_solve + +(* Theorems for system S4 from Hughes and Cresswell, p.60 *) + +lemma "|- []P | []Q <-> []([]P | []Q)" by S43_solve +lemma "|- ((P>- ((P>- []P & []Q" by S43_solve +lemma "|- <>(P | Q) <-> <>P | <>Q" by S43_solve +lemma "|- <>(P --> Q) <-> ([]P --> <>Q)" by S43_solve + +lemma "|- [](P --> Q) --> (<>P --> <>Q)" by S43_solve +lemma "|- []P --> []<>P" by S43_solve +lemma "|- <>[]P --> <>P" by S43_solve + +lemma "|- []P | []Q --> [](P | Q)" by S43_solve +lemma "|- <>(P & Q) --> <>P & <>Q" by S43_solve +lemma "|- [](P | Q) --> []P | <>Q" by S43_solve +lemma "|- <>P & []Q --> <>(P & Q)" by S43_solve +lemma "|- [](P | Q) --> <>P | []Q" by S43_solve + + +(* Theorems of system S43 *) + +lemma "|- <>[]P --> []<>P" by S43_solve +lemma "|- <>[]P --> [][]<>P" by S43_solve +lemma "|- [](<>P | <>Q) --> []<>P | []<>Q" by S43_solve +lemma "|- <>[]P & <>[]Q --> <>([]P & []Q)" by S43_solve +lemma "|- []([]P --> []Q) | []([]Q --> []P)" by S43_solve +lemma "|- [](<>P --> <>Q) | [](<>Q --> <>P)" by S43_solve +lemma "|- []([]P --> Q) | []([]Q --> P)" by S43_solve +lemma "|- [](P --> <>Q) | [](Q --> <>P)" by S43_solve +lemma "|- [](P --> []Q-->R) | [](P | ([]R --> Q))" by S43_solve +lemma "|- [](P | (Q --> <>C)) | [](P --> C --> <>Q)" by S43_solve +lemma "|- []([]P | Q) & [](P | []Q) --> []P | []Q" by S43_solve +lemma "|- <>P & <>Q --> <>(<>P & Q) | <>(P & <>Q)" by S43_solve +lemma "|- [](P | Q) & []([]P | Q) & [](P | []Q) --> []P | []Q" by S43_solve +lemma "|- <>P & <>Q --> <>(P & Q) | <>(<>P & Q) | <>(P & <>Q)" by S43_solve +lemma "|- <>[]<>P <-> []<>P" by S43_solve +lemma "|- []<>[]P <-> <>[]P" by S43_solve + +(* These are from Hailpern, LNCS 129 *) + +lemma "|- [](P & Q) <-> []P & []Q" by S43_solve +lemma "|- <>(P | Q) <-> <>P | <>Q" by S43_solve +lemma "|- <>(P --> Q) <-> []P --> <>Q" by S43_solve + +lemma "|- [](P --> Q) --> <>P --> <>Q" by S43_solve +lemma "|- []P --> []<>P" by S43_solve +lemma "|- <>[]P --> <>P" by S43_solve +lemma "|- []<>[]P --> []<>P" by S43_solve +lemma "|- <>[]P --> <>[]<>P" by S43_solve +lemma "|- <>[]P --> []<>P" by S43_solve +lemma "|- []<>[]P <-> <>[]P" by S43_solve +lemma "|- <>[]<>P <-> []<>P" by S43_solve + +lemma "|- []P | []Q --> [](P | Q)" by S43_solve +lemma "|- <>(P & Q) --> <>P & <>Q" by S43_solve +lemma "|- [](P | Q) --> []P | <>Q" by S43_solve +lemma "|- <>P & []Q --> <>(P & Q)" by S43_solve +lemma "|- [](P | Q) --> <>P | []Q" by S43_solve +lemma "|- [](P | Q) --> []<>P | []<>Q" by S43_solve +lemma "|- <>[]P & <>[]Q --> <>(P & Q)" by S43_solve +lemma "|- <>[](P & Q) <-> <>[]P & <>[]Q" by S43_solve +lemma "|- []<>(P | Q) <-> []<>P | []<>Q" by S43_solve end diff -r c11ab38b78a7 -r 87ac12bed1ab src/Sequents/T.ML --- a/src/Sequents/T.ML Mon Nov 20 21:23:12 2006 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,17 +0,0 @@ -(* Title: Modal/T.ML - ID: $Id$ - Author: Martin Coen - Copyright 1991 University of Cambridge -*) - -local open Modal0_rls -in structure MP_Rule : MODAL_PROVER_RULE = - struct - val rewrite_rls = rewrite_rls - val safe_rls = safe_rls - val unsafe_rls = unsafe_rls @ [boxR,diaL] - val bound_rls = bound_rls @ [boxL,diaR] - val aside_rls = [lstar0,lstar1,lstar2,rstar0,rstar1,rstar2] - end -end; -structure T_Prover = Modal_ProverFun(MP_Rule); diff -r c11ab38b78a7 -r 87ac12bed1ab src/Sequents/T.thy --- a/src/Sequents/T.thy Mon Nov 20 21:23:12 2006 +0100 +++ b/src/Sequents/T.thy Mon Nov 20 23:47:10 2006 +0100 @@ -31,6 +31,46 @@ "[| $E |L> $E'; $F |L> $F'; $G |R> $G'; $E', P, $F'|- $G'|] ==> $E, <>P, $F |- $G" -ML {* use_legacy_bindings (the_context ()) *} +ML {* +structure T_Prover = Modal_ProverFun +( + val rewrite_rls = thms "rewrite_rls" + val safe_rls = thms "safe_rls" + val unsafe_rls = thms "unsafe_rls" @ [thm "boxR", thm "diaL"] + val bound_rls = thms "bound_rls" @ [thm "boxL", thm "diaR"] + val aside_rls = [thm "lstar0", thm "lstar1", thm "lstar2", thm "rstar0", + thm "rstar1", thm "rstar2"] +) +*} + +method_setup T_solve = +{* Method.no_args (Method.SIMPLE_METHOD (T_Prover.solve_tac 2)) *} "T solver" + + +(* Theorems of system T from Hughes and Cresswell and Hailpern, LNCS 129 *) + +lemma "|- []P --> P" by T_solve +lemma "|- [](P-->Q) --> ([]P-->[]Q)" by T_solve (* normality*) +lemma "|- (P-- []P --> []Q" by T_solve +lemma "|- P --> <>P" by T_solve + +lemma "|- [](P & Q) <-> []P & []Q" by T_solve +lemma "|- <>(P | Q) <-> <>P | <>Q" by T_solve +lemma "|- [](P<->Q) <-> (P>-(P-->Q) <-> ([]P--><>Q)" by T_solve +lemma "|- []P <-> ~<>(~P)" by T_solve +lemma "|- [](~P) <-> ~<>P" by T_solve +lemma "|- ~[]P <-> <>(~P)" by T_solve +lemma "|- [][]P <-> ~<><>(~P)" by T_solve +lemma "|- ~<>(P | Q) <-> ~<>P & ~<>Q" by T_solve + +lemma "|- []P | []Q --> [](P | Q)" by T_solve +lemma "|- <>(P & Q) --> <>P & <>Q" by T_solve +lemma "|- [](P | Q) --> []P | <>Q" by T_solve +lemma "|- <>P & []Q --> <>(P & Q)" by T_solve +lemma "|- [](P | Q) --> <>P | []Q" by T_solve +lemma "|- <>(P-->(Q & R)) --> ([]P --> <>Q) & ([]P--><>R)" by T_solve +lemma "|- (P-- (P-- <>Q --> <>(P & Q)" by T_solve end diff -r c11ab38b78a7 -r 87ac12bed1ab src/Sequents/Washing.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Sequents/Washing.thy Mon Nov 20 23:47:10 2006 +0100 @@ -0,0 +1,61 @@ + +(* $Id$ *) + +(* code by Sara Kalvala, based on Paulson's LK + and Moore's tisl.ML *) + +theory Washing +imports ILL +begin + +consts + dollar :: o + quarter :: o + loaded :: o + dirty :: o + wet :: o + clean :: o + +axioms + 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" + + +(* "activate" definitions for use in proof *) + +ML_setup {* bind_thms ("changeI", [thm "context1"] RL ([thm "change"] RLN (2,[thm "cut"]))) *} +ML_setup {* bind_thms ("load1I", [thm "context1"] RL ([thm "load1"] RLN (2,[thm "cut"]))) *} +ML_setup {* bind_thms ("washI", [thm "context1"] RL ([thm "wash"] RLN (2,[thm "cut"]))) *} +ML_setup {* bind_thms ("dryI", [thm "context1"] RL ([thm "dry"] RLN (2,[thm "cut"]))) *} + +(* a load of dirty clothes and two dollars gives you clean clothes *) + +lemma "dollar , dollar , dirty |- clean" + apply (tactic {* best_tac (lazy_cs add_safes (thms "changeI" @ thms "load1I" @ thms "washI" @ thms "dryI")) 1 *}) + done + +(* order of premises doesn't matter *) + +lemma "dollar , dirty , dollar |- clean" + apply (tactic {* best_tac (lazy_cs add_safes (thms "changeI" @ thms "load1I" @ thms "washI" @ thms "dryI")) 1 *}) + done + +(* alternative formulation *) + +lemma "dollar , dollar |- dirty -o clean" + apply (tactic {* best_tac (lazy_cs add_safes (thms "changeI" @ thms "load1I" @ thms "washI" @ thms "dryI")) 1 *}) + done + +end diff -r c11ab38b78a7 -r 87ac12bed1ab src/Sequents/simpdata.ML --- a/src/Sequents/simpdata.ML Mon Nov 20 21:23:12 2006 +0100 +++ b/src/Sequents/simpdata.ML Mon Nov 20 23:47:10 2006 +0100 @@ -10,11 +10,16 @@ (*** Rewrite rules ***) +local + val subst = thm "subst" +in + fun prove_fun s = (writeln s; prove_goal (the_context ()) s (fn prems => [ (cut_facts_tac prems 1), (fast_tac (pack() add_safes [subst]) 1) ])); +end; val conj_simps = map prove_fun ["|- P & True <-> P", "|- True & P <-> P", @@ -83,6 +88,12 @@ (** Conversion into rewrite rules **) +local + val mp_R = thm "mp_R"; + val conjunct1 = thm "conjunct1"; + val conjunct2 = thm "conjunct2"; + val spec = thm "spec"; +in (*Make atomic rewrite rules*) fun atomize r = case concl_of r of @@ -99,22 +110,26 @@ | _ => [r]) | _ => []) (*ignore theorem unless it has precisely one conclusion*) | _ => [r]; - +end; Goal "|- ~P ==> |- (P <-> False)"; -by (etac (thinR RS cut) 1); +by (etac (thm "thinR" RS (thm "cut")) 1); by (Fast_tac 1); qed "P_iff_F"; -val iff_reflection_F = P_iff_F RS iff_reflection; +bind_thm ("iff_reflection_F", thm "P_iff_F" RS thm "iff_reflection"); Goal "|- P ==> |- (P <-> True)"; -by (etac (thinR RS cut) 1); +by (etac (thm "thinR" RS (thm "cut")) 1); by (Fast_tac 1); qed "P_iff_T"; -val iff_reflection_T = P_iff_T RS iff_reflection; +bind_thm ("iff_reflection_T", thm "P_iff_T" RS thm "iff_reflection"); +local + val eq_reflection = thm "eq_reflection" + val iff_reflection = thm "iff_reflection" +in (*Make meta-equalities.*) fun mk_meta_eq th = case concl_of th of Const("==",_)$_$_ => th @@ -128,12 +143,12 @@ | _ => th RS iff_reflection_T) | _ => error ("addsimps: unable to use theorem\n" ^ string_of_thm th)); - +end; (*Replace premises x=y, X<->Y by X==Y*) val mk_meta_prems = rule_by_tactic - (REPEAT_FIRST (resolve_tac [meta_eq_to_obj_eq, def_imp_iff])); + (REPEAT_FIRST (resolve_tac [thm "meta_eq_to_obj_eq", thm "def_imp_iff"])); (*Congruence rules for = or <-> (instead of ==)*) fun mk_meta_cong rl = @@ -179,9 +194,9 @@ "[| |- P <-> P'; |- P' ==> |- Q <-> Q' |] ==> |- (P-->Q) <-> (P'-->Q')"; by (lemma_tac p1 1); by (Safe_tac 1); -by (REPEAT (rtac cut 1 +by (REPEAT (rtac (thm "cut") 1 THEN - DEPTH_SOLVE_1 (resolve_tac [thinL, thinR, p2 COMP monotonic] 1) + DEPTH_SOLVE_1 (resolve_tac [thm "thinL", thm "thinR", p2 COMP thm "monotonic"] 1) THEN Safe_tac 1)); qed "imp_cong"; @@ -190,42 +205,23 @@ "[| |- P <-> P'; |- P' ==> |- Q <-> Q' |] ==> |- (P&Q) <-> (P'&Q')"; by (lemma_tac p1 1); by (Safe_tac 1); -by (REPEAT (rtac cut 1 +by (REPEAT (rtac (thm "cut") 1 THEN - DEPTH_SOLVE_1 (resolve_tac [thinL, thinR, p2 COMP monotonic] 1) + DEPTH_SOLVE_1 (resolve_tac [thm "thinL", thm "thinR", p2 COMP thm "monotonic"] 1) THEN Safe_tac 1)); qed "conj_cong"; Goal "|- (x=y) <-> (y=x)"; -by (fast_tac (pack() add_safes [subst]) 1); +by (fast_tac (pack() add_safes [thm "subst"]) 1); qed "eq_sym_conv"; -(** if-then-else rules **) - -Goalw [If_def] "|- (if True then x else y) = x"; -by (Fast_tac 1); -qed "if_True"; - -Goalw [If_def] "|- (if False then x else y) = y"; -by (Fast_tac 1); -qed "if_False"; - -Goalw [If_def] "|- P ==> |- (if P then x else y) = x"; -by (etac (thinR RS cut) 1); -by (Fast_tac 1); -qed "if_P"; - -Goalw [If_def] "|- ~P ==> |- (if P then x else y) = y"; -by (etac (thinR RS cut) 1); -by (Fast_tac 1); -qed "if_not_P"; - (*** Standard simpsets ***) -val triv_rls = [FalseL, TrueR, basic, refl, iff_refl, reflexive_thm]; +val triv_rls = [thm "FalseL", thm "TrueR", thm "basic", thm "refl", + thm "iff_refl", reflexive_thm]; fun unsafe_solver prems = FIRST'[resolve_tac (triv_rls@prems), assume_tac]; @@ -244,7 +240,7 @@ val LK_simps = [triv_forall_equality, (* prunes params *) - refl RS P_iff_T] @ + thm "refl" RS P_iff_T] @ conj_simps @ disj_simps @ not_simps @ imp_simps @ iff_simps @quant_simps @ all_simps @ ex_simps @ [de_Morgan_conj, de_Morgan_disj, imp_disj1, imp_disj2] @ @@ -269,10 +265,10 @@ asm_simp_tac LK_basic_ss 1]); Goal "|- P(if Q then x else y) <-> ((Q --> P(x)) & (~Q --> P(y)))"; -by (res_inst_tac [ ("P","Q") ] cut 1); -by (simp_tac (simpset() addsimps [if_P]) 2); -by (res_inst_tac [ ("P","~Q") ] cut 1); -by (simp_tac (simpset() addsimps [if_not_P]) 2); +by (res_inst_tac [ ("P","Q") ] (thm "cut") 1); +by (simp_tac (simpset() addsimps [thm "if_P"]) 2); +by (res_inst_tac [ ("P","~Q") ] (thm "cut") 1); +by (simp_tac (simpset() addsimps [thm "if_not_P"]) 2); by (Fast_tac 1); qed "split_if"; @@ -284,8 +280,8 @@ Goal "|- (if x=y then y else x) = x"; by (lemma_tac split_if 1); by (Safe_tac 1); -by (rtac symL 1); -by (rtac basic 1); +by (rtac (thm "symL") 1); +by (rtac (thm "basic") 1); qed "if_eq_cancel"; (*Putting in automatic case splits seems to require a lot of work.*)