--- 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) *]";
-
--- 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]) ;
--- 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
--- 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";
--- 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]);
--- 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
-
--- /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
--- 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
--- /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
--- 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();
--- 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 \<Longrightarrow> $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
--- /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
--- /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
--- 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";
--- 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*)
--- 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();
--- 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*)
--- 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";
--- 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
--- 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";
--- 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";
--- 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>-<Q) --< R) --> ((P>-<Q) --< []R)";
-
-(* These are from Hailpern, LNCS 129 *)
-
-try "|- [](P & Q) <-> []P & []Q";
-try "|- <>(P | Q) <-> <>P | <>Q";
-try "|- <>(P --> Q) <-> ([]P --> <>Q)";
-
-try "|- [](P --> Q) --> (<>P --> <>Q)";
-try "|- []P --> []<>P";
-try "|- <>[]P --> <>P";
-
-try "|- []P | []Q --> [](P | Q)";
-try "|- <>(P & Q) --> <>P & <>Q";
-try "|- [](P | Q) --> []P | <>Q";
-try "|- <>P & []Q --> <>(P & Q)";
-try "|- [](P | Q) --> <>P | []Q";
-
--- a/src/Sequents/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--<Q) --> []P --> []Q";
-try "|- P --> <>P";
-
-try "|- [](P & Q) <-> []P & []Q";
-try "|- <>(P | Q) <-> <>P | <>Q";
-try "|- [](P<->Q) <-> (P>-<Q)";
-try "|- <>(P-->Q) <-> ([]P--><>Q)";
-try "|- []P <-> ~<>(~P)";
-try "|- [](~P) <-> ~<>P";
-try "|- ~[]P <-> <>(~P)";
-try "|- [][]P <-> ~<><>(~P)";
-try "|- ~<>(P | Q) <-> ~<>P & ~<>Q";
-
-try "|- []P | []Q --> [](P | Q)";
-try "|- <>(P & Q) --> <>P & <>Q";
-try "|- [](P | Q) --> []P | <>Q";
-try "|- <>P & []Q --> <>(P & Q)";
-try "|- [](P | Q) --> <>P | []Q";
-try "|- <>(P-->(Q & R)) --> ([]P --> <>Q) & ([]P--><>R)";
-try "|- (P--<Q) & (Q--<R) --> (P--<R)";
-try "|- []P --> <>Q --> <>(P & Q)";
--- a/src/Sequents/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;
--- 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
--- 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";
--- 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);
--- 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--<Q) --> []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>-<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 <-> <>(~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--<Q) & (Q--<R) --> (P--<R)" by S4_solve
+lemma "|- []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>-<Q) --< R) --> ((P>-<Q) --< []R)" by S4_solve
+
+(* These are from Hailpern, LNCS 129 *)
+
+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 --> []<>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
--- 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);
--- 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--<Q) --> []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>-<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 | 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--<Q) & (Q--<R) --> (P--<R)" by S43_solve
+lemma "|- []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>-<Q) --< R) --> ((P>-<Q) --< []R)" 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 | []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
--- 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);
--- 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--<Q) --> []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>-<Q)" by T_solve
+lemma "|- <>(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--<Q) & (Q--<R) --> (P--<R)" by T_solve
+lemma "|- []P --> <>Q --> <>(P & Q)" by T_solve
end
--- /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
--- 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.*)