--- a/src/Cube/ex/ex.ML Fri Oct 10 15:52:12 1997 +0200
+++ b/src/Cube/ex/ex.ML Fri Oct 10 16:29:41 1997 +0200
@@ -19,37 +19,37 @@
by (DEPTH_SOLVE (ares_tac simple 1));
uresult();
-goal thy "A:* |- Lam a:A.a : ?T";
+goal thy "A:* |- Lam a:A. a : ?T";
by (DEPTH_SOLVE (ares_tac simple 1));
uresult();
-goal thy "A:* B:* b:B |- Lam x:A.b : ?T";
+goal thy "A:* B:* b:B |- Lam x:A. b : ?T";
by (DEPTH_SOLVE (ares_tac simple 1));
uresult();
-goal thy "A:* b:A |- (Lam a:A.a)^b: ?T";
+goal thy "A:* b:A |- (Lam a:A. a)^b: ?T";
by (DEPTH_SOLVE (ares_tac simple 1));
uresult();
-goal thy "A:* B:* c:A b:B |- (Lam x:A.b)^ c: ?T";
+goal thy "A:* B:* c:A b:B |- (Lam x:A. b)^ c: ?T";
by (DEPTH_SOLVE (ares_tac simple 1));
uresult();
-goal thy "A:* B:* |- Lam a:A.Lam b:B.a : ?T";
+goal thy "A:* B:* |- Lam a:A. Lam b:B. a : ?T";
by (DEPTH_SOLVE (ares_tac simple 1));
uresult();
(* SECOND-ORDER TYPES *)
-goal L2_thy "|- Lam A:*. Lam a:A.a : ?T";
+goal L2_thy "|- Lam A:*. Lam a:A. a : ?T";
by (DEPTH_SOLVE (ares_tac L2 1));
uresult();
-goal L2_thy "A:* |- (Lam B:*.Lam b:B.b)^A : ?T";
+goal L2_thy "A:* |- (Lam B:*.Lam b:B. b)^A : ?T";
by (DEPTH_SOLVE (ares_tac L2 1));
uresult();
-goal L2_thy "A:* b:A |- (Lam B:*.Lam b:B.b) ^ A ^ b: ?T";
+goal L2_thy "A:* b:A |- (Lam B:*.Lam b:B. b) ^ A ^ b: ?T";
by (DEPTH_SOLVE (ares_tac L2 1));
uresult();
@@ -67,7 +67,7 @@
by (DEPTH_SOLVE (ares_tac Lomega 1));
uresult();
-goal Lomega_thy "B:* b:B |- (Lam y:B.b): ?T";
+goal Lomega_thy "B:* b:B |- (Lam y:B. b): ?T";
by (DEPTH_SOLVE (ares_tac Lomega 1));
uresult();
@@ -89,28 +89,28 @@
by (DEPTH_SOLVE (ares_tac LP 1));
uresult();
-goal LP_thy "A:* P:A->A->* a:A |- Pi a:A.P^a^a: ?T";
+goal LP_thy "A:* P:A->A->* a:A |- Pi a:A. P^a^a: ?T";
by (DEPTH_SOLVE (ares_tac LP 1));
uresult();
-goal LP_thy "A:* P:A->* Q:A->* |- Pi a:A.P^a -> Q^a: ?T";
+goal LP_thy "A:* P:A->* Q:A->* |- Pi a:A. P^a -> Q^a: ?T";
by (DEPTH_SOLVE (ares_tac LP 1));
uresult();
-goal LP_thy "A:* P:A->* |- Pi a:A.P^a -> P^a: ?T";
+goal LP_thy "A:* P:A->* |- Pi a:A. P^a -> P^a: ?T";
by (DEPTH_SOLVE (ares_tac LP 1));
uresult();
-goal LP_thy "A:* P:A->* |- Lam a:A.Lam x:P^a.x: ?T";
+goal LP_thy "A:* P:A->* |- Lam a:A. Lam x:P^a. x: ?T";
by (DEPTH_SOLVE (ares_tac LP 1));
uresult();
-goal LP_thy "A:* P:A->* Q:* |- (Pi a:A.P^a->Q) -> (Pi a:A.P^a) -> Q : ?T";
+goal LP_thy "A:* P:A->* Q:* |- (Pi a:A. P^a->Q) -> (Pi a:A. P^a) -> Q : ?T";
by (DEPTH_SOLVE (ares_tac LP 1));
uresult();
goal LP_thy "A:* P:A->* Q:* a0:A |- \
-\ Lam x:Pi a:A.P^a->Q. Lam y:Pi a:A.P^a. x^a0^(y^a0): ?T";
+\ Lam x:Pi a:A. P^a->Q. Lam y:Pi a:A. P^a. x^a0^(y^a0): ?T";
by (DEPTH_SOLVE (ares_tac LP 1));
uresult();
@@ -124,7 +124,7 @@
by (DEPTH_SOLVE (ares_tac LOmega 1));
uresult();
-goal LOmega_thy "|- Lam A:*.Lam B:*.Lam x:A.Lam y:B.x : ?T";
+goal LOmega_thy "|- Lam A:*.Lam B:*.Lam x:A. Lam y:B. x : ?T";
by (DEPTH_SOLVE (ares_tac LOmega 1));
uresult();
@@ -148,18 +148,18 @@
(* Second-order Predicate Logic *)
-goal LP2_thy "A:* P:A->* |- Lam a:A.P^a->(Pi A:*.A) : ?T";
+goal LP2_thy "A:* P:A->* |- Lam a:A. P^a->(Pi A:*.A) : ?T";
by (DEPTH_SOLVE (ares_tac LP2 1));
uresult();
goal LP2_thy "A:* P:A->A->* |- \
-\ (Pi a:A.Pi b:A.P^a^b->P^b^a->Pi P:*.P) -> Pi a:A.P^a^a->Pi P:*.P : ?T";
+\ (Pi a:A. Pi b:A. P^a^b->P^b^a->Pi P:*.P) -> Pi a:A. P^a^a->Pi P:*.P : ?T";
by (DEPTH_SOLVE (ares_tac LP2 1));
uresult();
(* Antisymmetry implies irreflexivity: *)
goal LP2_thy "A:* P:A->A->* |- \
-\ ?p: (Pi a:A.Pi b:A.P^a^b->P^b^a->Pi P:*.P) -> Pi a:A.P^a^a->Pi P:*.P";
+\ ?p: (Pi a:A. Pi b:A. P^a^b->P^b^a->Pi P:*.P) -> Pi a:A. P^a^a->Pi P:*.P";
by (strip_asms_tac LP2 1);
by (rtac lam_ss 1);
by (DEPTH_SOLVE_1(ares_tac LP2 1));
@@ -175,25 +175,25 @@
(* LPomega *)
-goal LPomega_thy "A:* |- Lam P:A->A->*.Lam a:A.P^a^a : ?T";
+goal LPomega_thy "A:* |- Lam P:A->A->*.Lam a:A. P^a^a : ?T";
by (DEPTH_SOLVE (ares_tac LPomega 1));
uresult();
-goal LPomega_thy "|- Lam A:*.Lam P:A->A->*.Lam a:A.P^a^a : ?T";
+goal LPomega_thy "|- Lam A:*.Lam P:A->A->*.Lam a:A. P^a^a : ?T";
by (DEPTH_SOLVE (ares_tac LPomega 1));
uresult();
(* CONSTRUCTIONS *)
-goal CC_thy "|- Lam A:*.Lam P:A->*.Lam a:A.P^a->Pi P:*.P: ?T";
+goal CC_thy "|- Lam A:*.Lam P:A->*.Lam a:A. P^a->Pi P:*.P: ?T";
by (DEPTH_SOLVE (ares_tac CC 1));
uresult();
-goal CC_thy "|- Lam A:*.Lam P:A->*.Pi a:A.P^a: ?T";
+goal CC_thy "|- Lam A:*.Lam P:A->*.Pi a:A. P^a: ?T";
by (DEPTH_SOLVE (ares_tac CC 1));
uresult();
-goal CC_thy "A:* P:A->* a:A |- ?p : (Pi a:A.P^a)->P^a";
+goal CC_thy "A:* P:A->* a:A |- ?p : (Pi a:A. P^a)->P^a";
by (strip_asms_tac CC 1);
by (rtac lam_ss 1);
by (DEPTH_SOLVE_1(ares_tac CC 1));
@@ -208,7 +208,7 @@
by (DEPTH_SOLVE(ares_tac LP2 1));
uresult();
-goal CC_thy "Lam A:*.Lam c:A.Lam f:A->A. \
+goal CC_thy "Lam A:*.Lam c:A. Lam f:A->A. \
\ Lam a:A. Pi P:A->*.P^c -> (Pi x:A. P^x->P^(f^x)) -> P^a : ?T";
by (DEPTH_SOLVE(ares_tac CC 1));
uresult();
@@ -219,7 +219,7 @@
by (rtac lam_ss 1);
by (DEPTH_SOLVE_1(ares_tac LP2 1));
by (DEPTH_SOLVE_1(ares_tac LP2 2));
-by (eres_inst_tac [("a","Lam x:A.Pi Q:A->*.Q^x->Q^a")] pi_elim 1);
+by (eres_inst_tac [("a","Lam x:A. Pi Q:A->*.Q^x->Q^a")] pi_elim 1);
by (DEPTH_SOLVE_1(ares_tac LP2 1));
by (rewtac beta);
by (etac imp_elim 1);
--- a/src/FOLP/FOLP.ML Fri Oct 10 15:52:12 1997 +0200
+++ b/src/FOLP/FOLP.ML Fri Oct 10 16:29:41 1997 +0200
@@ -27,7 +27,7 @@
(*** Classical introduction rules for | and EX ***)
val disjCI = prove_goal FOLP.thy
- "(!!x.x:~Q ==> f(x):P) ==> ?p : P|Q"
+ "(!!x. x:~Q ==> f(x):P) ==> ?p : P|Q"
(fn prems=>
[ (rtac classical 1),
(REPEAT (ares_tac (prems@[disjI1,notI]) 1)),
@@ -35,14 +35,14 @@
(*introduction rule involving only EX*)
val ex_classical = prove_goal FOLP.thy
- "( !!u.u:~(EX x. P(x)) ==> f(u):P(a)) ==> ?p : EX x.P(x)"
+ "( !!u. u:~(EX x. P(x)) ==> f(u):P(a)) ==> ?p : EX x. P(x)"
(fn prems=>
[ (rtac classical 1),
(eresolve_tac (prems RL [exI]) 1) ]);
(*version of above, simplifying ~EX to ALL~ *)
val exCI = prove_goal FOLP.thy
- "(!!u.u:ALL x. ~P(x) ==> f(u):P(a)) ==> ?p : EX x.P(x)"
+ "(!!u. u:ALL x. ~P(x) ==> f(u):P(a)) ==> ?p : EX x. P(x)"
(fn [prem]=>
[ (rtac ex_classical 1),
(resolve_tac [notI RS allI RS prem] 1),
@@ -58,7 +58,7 @@
(*Classical implies (-->) elimination. *)
val impCE = prove_goal FOLP.thy
- "[| p:P-->Q; !!x.x:~P ==> f(x):R; !!y.y:Q ==> g(y):R |] ==> ?p : R"
+ "[| p:P-->Q; !!x. x:~P ==> f(x):R; !!y. y:Q ==> g(y):R |] ==> ?p : R"
(fn major::prems=>
[ (resolve_tac [excluded_middle RS disjE] 1),
(DEPTH_SOLVE (ares_tac (prems@[major RS mp]) 1)) ]);
@@ -84,7 +84,7 @@
(*Should be used as swap since ~P becomes redundant*)
val swap = prove_goal FOLP.thy
- "p:~P ==> (!!x.x:~Q ==> f(x):P) ==> ?p : Q"
+ "p:~P ==> (!!x. x:~Q ==> f(x):P) ==> ?p : Q"
(fn major::prems=>
[ (rtac classical 1),
(rtac (major RS notE) 1),
--- a/src/FOLP/FOLP.thy Fri Oct 10 15:52:12 1997 +0200
+++ b/src/FOLP/FOLP.thy Fri Oct 10 16:29:41 1997 +0200
@@ -10,5 +10,5 @@
consts
cla :: "[p=>p]=>p"
rules
- classical "(!!x.x:~P ==> f(x):P) ==> cla(f):P"
+ classical "(!!x. x:~P ==> f(x):P) ==> cla(f):P"
end
--- a/src/FOLP/IFOLP.ML Fri Oct 10 15:52:12 1997 +0200
+++ b/src/FOLP/IFOLP.ML Fri Oct 10 16:29:41 1997 +0200
@@ -82,23 +82,23 @@
resolve_tac prems 1))) ]);
val impE = prove_goal IFOLP.thy
- "[| p:P-->Q; q:P; !!x.x:Q ==> r(x):R |] ==> ?p:R"
+ "[| p:P-->Q; q:P; !!x. x:Q ==> r(x):R |] ==> ?p:R"
(fn prems=> [ (REPEAT (resolve_tac (prems@[mp]) 1)) ]);
val allE = prove_goal IFOLP.thy
- "[| p:ALL x.P(x); !!y.y:P(x) ==> q(y):R |] ==> ?p:R"
+ "[| p:ALL x. P(x); !!y. y:P(x) ==> q(y):R |] ==> ?p:R"
(fn prems=> [ (REPEAT (resolve_tac (prems@[spec]) 1)) ]);
(*Duplicates the quantifier; for use with eresolve_tac*)
val all_dupE = prove_goal IFOLP.thy
- "[| p:ALL x.P(x); !!y z.[| y:P(x); z:ALL x.P(x) |] ==> q(y,z):R \
+ "[| p:ALL x. P(x); !!y z.[| y:P(x); z:ALL x. P(x) |] ==> q(y,z):R \
\ |] ==> ?p:R"
(fn prems=> [ (REPEAT (resolve_tac (prems@[spec]) 1)) ]);
(*** Negation rules, which translate between ~P and P-->False ***)
-val notI = prove_goalw IFOLP.thy [not_def] "(!!x.x:P ==> q(x):False) ==> ?p:~P"
+val notI = prove_goalw IFOLP.thy [not_def] "(!!x. x:P ==> q(x):False) ==> ?p:~P"
(fn prems=> [ (REPEAT (ares_tac (prems@[impI]) 1)) ]);
val notE = prove_goalw IFOLP.thy [not_def] "[| p:~P; q:P |] ==> ?p:R"
@@ -108,7 +108,7 @@
(*This is useful with the special implication rules for each kind of P. *)
val not_to_imp = prove_goal IFOLP.thy
- "[| p:~P; !!x.x:(P-->False) ==> q(x):Q |] ==> ?p:Q"
+ "[| p:~P; !!x. x:(P-->False) ==> q(x):Q |] ==> ?p:Q"
(fn prems=> [ (REPEAT (ares_tac (prems@[impI,notE]) 1)) ]);
@@ -121,7 +121,7 @@
(*Contrapositive of an inference rule*)
-val contrapos = prove_goal IFOLP.thy "[| p:~Q; !!y.y:P==>q(y):Q |] ==> ?a:~P"
+val contrapos = prove_goal IFOLP.thy "[| p:~Q; !!y. y:P==>q(y):Q |] ==> ?a:~P"
(fn [major,minor]=>
[ (rtac (major RS notE RS notI) 1),
(etac minor 1) ]);
@@ -161,7 +161,7 @@
(*** If-and-only-if ***)
val iffI = prove_goalw IFOLP.thy [iff_def]
- "[| !!x.x:P ==> q(x):Q; !!x.x:Q ==> r(x):P |] ==> ?p:P<->Q"
+ "[| !!x. x:P ==> q(x):Q; !!x. x:Q ==> r(x):P |] ==> ?p:P<->Q"
(fn prems=> [ (REPEAT (ares_tac (prems@[conjI, impI]) 1)) ]);
@@ -201,11 +201,11 @@
***)
val ex1I = prove_goalw IFOLP.thy [ex1_def]
- "[| p:P(a); !!x u.u:P(x) ==> f(u) : x=a |] ==> ?p:EX! x. P(x)"
+ "[| p:P(a); !!x u. u:P(x) ==> f(u) : x=a |] ==> ?p:EX! x. P(x)"
(fn prems => [ (REPEAT (ares_tac (prems@[exI,conjI,allI,impI]) 1)) ]);
val ex1E = prove_goalw IFOLP.thy [ex1_def]
- "[| p:EX! x.P(x); \
+ "[| p:EX! x. P(x); \
\ !!x u v. [| u:P(x); v:ALL y. P(y) --> y=x |] ==> f(x,u,v):R |] ==>\
\ ?a : R"
(fn prems =>
@@ -221,7 +221,7 @@
REPEAT1 (eresolve_tac [asm_rl,mp] i);
val conj_cong = prove_goal IFOLP.thy
- "[| p:P <-> P'; !!x.x:P' ==> q(x):Q <-> Q' |] ==> ?p:(P&Q) <-> (P'&Q')"
+ "[| p:P <-> P'; !!x. x:P' ==> q(x):Q <-> Q' |] ==> ?p:(P&Q) <-> (P'&Q')"
(fn prems =>
[ (cut_facts_tac prems 1),
(REPEAT (ares_tac [iffI,conjI] 1
@@ -237,7 +237,7 @@
ORELSE mp_tac 1)) ]);
val imp_cong = prove_goal IFOLP.thy
- "[| p:P <-> P'; !!x.x:P' ==> q(x):Q <-> Q' |] ==> ?p:(P-->Q) <-> (P'-->Q')"
+ "[| p:P <-> P'; !!x. x:P' ==> q(x):Q <-> Q' |] ==> ?p:(P-->Q) <-> (P'-->Q')"
(fn prems =>
[ (cut_facts_tac prems 1),
(REPEAT (ares_tac [iffI,impI] 1
@@ -261,14 +261,14 @@
ORELSE eresolve_tac [iffE,notE] 1)) ]);
val all_cong = prove_goal IFOLP.thy
- "(!!x.f(x):P(x) <-> Q(x)) ==> ?p:(ALL x.P(x)) <-> (ALL x.Q(x))"
+ "(!!x. f(x):P(x) <-> Q(x)) ==> ?p:(ALL x. P(x)) <-> (ALL x. Q(x))"
(fn prems =>
[ (REPEAT (ares_tac [iffI,allI] 1
ORELSE mp_tac 1
ORELSE etac allE 1 ORELSE iff_tac prems 1)) ]);
val ex_cong = prove_goal IFOLP.thy
- "(!!x.f(x):P(x) <-> Q(x)) ==> ?p:(EX x.P(x)) <-> (EX x.Q(x))"
+ "(!!x. f(x):P(x) <-> Q(x)) ==> ?p:(EX x. P(x)) <-> (EX x. Q(x))"
(fn prems =>
[ (REPEAT (etac exE 1 ORELSE ares_tac [iffI,exI] 1
ORELSE mp_tac 1
@@ -306,7 +306,7 @@
(*A special case of ex1E that would otherwise need quantifier expansion*)
val ex1_equalsE = prove_goal IFOLP.thy
- "[| p:EX! x.P(x); q:P(a); r:P(b) |] ==> ?d:a=b"
+ "[| p:EX! x. P(x); q:P(a); r:P(b) |] ==> ?d:a=b"
(fn prems =>
[ (cut_facts_tac prems 1),
(etac ex1E 1),
@@ -395,7 +395,7 @@
(preprint, University of St Andrews, 1991) ***)
val conj_impE = prove_goal IFOLP.thy
- "[| p:(P&Q)-->S; !!x.x:P-->(Q-->S) ==> q(x):R |] ==> ?p:R"
+ "[| p:(P&Q)-->S; !!x. x:P-->(Q-->S) ==> q(x):R |] ==> ?p:R"
(fn major::prems=>
[ (REPEAT (ares_tac ([conjI, impI, major RS mp]@prems) 1)) ]);
@@ -407,7 +407,7 @@
(*Simplifies the implication. Classical version is stronger.
Still UNSAFE since Q must be provable -- backtracking needed. *)
val imp_impE = prove_goal IFOLP.thy
- "[| p:(P-->Q)-->S; !!x y.[| x:P; y:Q-->S |] ==> q(x,y):Q; !!x.x:S ==> r(x):R |] ==> \
+ "[| p:(P-->Q)-->S; !!x y.[| x:P; y:Q-->S |] ==> q(x,y):Q; !!x. x:S ==> r(x):R |] ==> \
\ ?p:R"
(fn major::prems=>
[ (REPEAT (ares_tac ([impI, major RS mp]@prems) 1)) ]);
@@ -415,26 +415,26 @@
(*Simplifies the implication. Classical version is stronger.
Still UNSAFE since ~P must be provable -- backtracking needed. *)
val not_impE = prove_goal IFOLP.thy
- "[| p:~P --> S; !!y.y:P ==> q(y):False; !!y.y:S ==> r(y):R |] ==> ?p:R"
+ "[| p:~P --> S; !!y. y:P ==> q(y):False; !!y. y:S ==> r(y):R |] ==> ?p:R"
(fn major::prems=>
[ (REPEAT (ares_tac ([notI, impI, major RS mp]@prems) 1)) ]);
(*Simplifies the implication. UNSAFE. *)
val iff_impE = prove_goal IFOLP.thy
"[| p:(P<->Q)-->S; !!x y.[| x:P; y:Q-->S |] ==> q(x,y):Q; \
-\ !!x y.[| x:Q; y:P-->S |] ==> r(x,y):P; !!x.x:S ==> s(x):R |] ==> ?p:R"
+\ !!x y.[| x:Q; y:P-->S |] ==> r(x,y):P; !!x. x:S ==> s(x):R |] ==> ?p:R"
(fn major::prems=>
[ (REPEAT (ares_tac ([iffI, impI, major RS mp]@prems) 1)) ]);
(*What if (ALL x.~~P(x)) --> ~~(ALL x.P(x)) is an assumption? UNSAFE*)
val all_impE = prove_goal IFOLP.thy
- "[| p:(ALL x.P(x))-->S; !!x.q:P(x); !!y.y:S ==> r(y):R |] ==> ?p:R"
+ "[| p:(ALL x. P(x))-->S; !!x. q:P(x); !!y. y:S ==> r(y):R |] ==> ?p:R"
(fn major::prems=>
[ (REPEAT (ares_tac ([allI, impI, major RS mp]@prems) 1)) ]);
(*Unsafe: (EX x.P(x))-->S is equivalent to ALL x.P(x)-->S. *)
val ex_impE = prove_goal IFOLP.thy
- "[| p:(EX x.P(x))-->S; !!y.y:P(a)-->S ==> q(y):R |] ==> ?p:R"
+ "[| p:(EX x. P(x))-->S; !!y. y:P(a)-->S ==> q(y):R |] ==> ?p:R"
(fn major::prems=>
[ (REPEAT (ares_tac ([exI, impI, major RS mp]@prems) 1)) ]);
--- a/src/FOLP/IFOLP.thy Fri Oct 10 15:52:12 1997 +0200
+++ b/src/FOLP/IFOLP.thy Fri Oct 10 16:29:41 1997 +0200
@@ -67,7 +67,7 @@
(* Like Intensional Equality in MLTT - but proofs distinct from terms *)
ieqI "ideq(a) : a=a"
-ieqE "[| p : a=b; !!x.f(x) : P(x,x) |] ==> idpeel(p,f) : P(a,b)"
+ieqE "[| p : a=b; !!x. f(x) : P(x,x) |] ==> idpeel(p,f) : P(a,b)"
(* Truth and Falsity *)
@@ -84,21 +84,21 @@
disjI1 "a:P ==> inl(a):P|Q"
disjI2 "b:Q ==> inr(b):P|Q"
-disjE "[| a:P|Q; !!x.x:P ==> f(x):R; !!x.x:Q ==> g(x):R
+disjE "[| a:P|Q; !!x. x:P ==> f(x):R; !!x. x:Q ==> g(x):R
|] ==> when(a,f,g):R"
(* Implication *)
-impI "(!!x.x:P ==> f(x):Q) ==> lam x.f(x):P-->Q"
+impI "(!!x. x:P ==> f(x):Q) ==> lam x. f(x):P-->Q"
mp "[| f:P-->Q; a:P |] ==> f`a:Q"
(*Quantifiers*)
-allI "(!!x. f(x) : P(x)) ==> all x.f(x) : ALL x.P(x)"
-spec "(f:ALL x.P(x)) ==> f^x : P(x)"
+allI "(!!x. f(x) : P(x)) ==> all x. f(x) : ALL x. P(x)"
+spec "(f:ALL x. P(x)) ==> f^x : P(x)"
-exI "p : P(x) ==> [x,p] : EX x.P(x)"
-exE "[| p: EX x.P(x); !!x u. u:P(x) ==> f(x,u) : R |] ==> xsplit(p,f):R"
+exI "p : P(x) ==> [x,p] : EX x. P(x)"
+exE "[| p: EX x. P(x); !!x u. u:P(x) ==> f(x,u) : R |] ==> xsplit(p,f):R"
(**** Equality between proofs ****)
@@ -106,20 +106,20 @@
psym "a = b : P ==> b = a : P"
ptrans "[| a = b : P; b = c : P |] ==> a = c : P"
-idpeelB "[| !!x.f(x) : P(x,x) |] ==> idpeel(ideq(a),f) = f(a) : P(a,a)"
+idpeelB "[| !!x. f(x) : P(x,x) |] ==> idpeel(ideq(a),f) = f(a) : P(a,a)"
fstB "a:P ==> fst(<a,b>) = a : P"
sndB "b:Q ==> snd(<a,b>) = b : Q"
pairEC "p:P&Q ==> p = <fst(p),snd(p)> : P&Q"
-whenBinl "[| a:P; !!x.x:P ==> f(x) : Q |] ==> when(inl(a),f,g) = f(a) : Q"
-whenBinr "[| b:P; !!x.x:P ==> g(x) : Q |] ==> when(inr(b),f,g) = g(b) : Q"
-plusEC "a:P|Q ==> when(a,%x.inl(x),%y.inr(y)) = p : P|Q"
+whenBinl "[| a:P; !!x. x:P ==> f(x) : Q |] ==> when(inl(a),f,g) = f(a) : Q"
+whenBinr "[| b:P; !!x. x:P ==> g(x) : Q |] ==> when(inr(b),f,g) = g(b) : Q"
+plusEC "a:P|Q ==> when(a,%x. inl(x),%y. inr(y)) = p : P|Q"
-applyB "[| a:P; !!x.x:P ==> b(x) : Q |] ==> (lam x.b(x)) ` a = b(a) : Q"
-funEC "f:P ==> f = lam x.f`x : P"
+applyB "[| a:P; !!x. x:P ==> b(x) : Q |] ==> (lam x. b(x)) ` a = b(a) : Q"
+funEC "f:P ==> f = lam x. f`x : P"
-specB "[| !!x.f(x) : P(x) |] ==> (all x.f(x)) ^ a = f(a) : P(a)"
+specB "[| !!x. f(x) : P(x) |] ==> (all x. f(x)) ^ a = f(a) : P(a)"
(**** Definitions ****)
--- a/src/FOLP/ROOT.ML Fri Oct 10 15:52:12 1997 +0200
+++ b/src/FOLP/ROOT.ML Fri Oct 10 16:29:41 1997 +0200
@@ -33,7 +33,7 @@
(*etac rev_cut_eq moves an equality to be the last premise. *)
val rev_cut_eq = prove_goal IFOLP.thy
- "[| p:a=b; !!x.x:a=b ==> f(x):R |] ==> ?p:R"
+ "[| p:a=b; !!x. x:a=b ==> f(x):R |] ==> ?p:R"
(fn prems => [ REPEAT(resolve_tac prems 1) ]);
val rev_mp = rev_mp
--- a/src/FOLP/ex/If.ML Fri Oct 10 15:52:12 1997 +0200
+++ b/src/FOLP/ex/If.ML Fri Oct 10 16:29:41 1997 +0200
@@ -10,7 +10,7 @@
open Cla; (*in case structure Int is open!*)
val prems = goalw If.thy [if_def]
- "[| !!x.x:P ==> f(x):Q; !!x.x:~P ==> g(x):R |] ==> ?p:if(P,Q,R)";
+ "[| !!x. x:P ==> f(x):Q; !!x. x:~P ==> g(x):R |] ==> ?p:if(P,Q,R)";
by (fast_tac (FOLP_cs addIs prems) 1);
val ifI = result();
--- a/src/FOLP/ex/cla.ML Fri Oct 10 15:52:12 1997 +0200
+++ b/src/FOLP/ex/cla.ML Fri Oct 10 16:29:41 1997 +0200
@@ -127,15 +127,15 @@
by (fast_tac FOLP_cs 1);
result();
-goal FOLP.thy "?p : (EX x. P-->Q(x)) <-> (P --> (EX x.Q(x)))";
+goal FOLP.thy "?p : (EX x. P-->Q(x)) <-> (P --> (EX x. Q(x)))";
by (fast_tac FOLP_cs 1);
result();
-goal FOLP.thy "?p : (EX x.P(x)-->Q) <-> (ALL x.P(x)) --> Q";
+goal FOLP.thy "?p : (EX x. P(x)-->Q) <-> (ALL x. P(x)) --> Q";
by (fast_tac FOLP_cs 1);
result();
-goal FOLP.thy "?p : (ALL x.P(x)) | Q <-> (ALL x. P(x) | Q)";
+goal FOLP.thy "?p : (ALL x. P(x)) | Q <-> (ALL x. P(x) | Q)";
by (fast_tac FOLP_cs 1);
result();
@@ -192,7 +192,7 @@
writeln"Problem 24";
goal FOLP.thy "?p : ~(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)) --> (EX x. Q(x))) & (ALL x. Q(x)|R(x) --> S(x)) \
\ --> (EX x. P(x)&R(x))";
by (fast_tac FOLP_cs 1);
result();
@@ -225,7 +225,7 @@
writeln"Problem 28. AMENDED";
goal FOLP.thy "?p : (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))) \
+\ ((EX x. S(x)) --> (ALL x. L(x) --> M(x))) \
\ --> (ALL x. P(x) & L(x) --> M(x))";
by (fast_tac FOLP_cs 1);
result();
@@ -245,7 +245,7 @@
result();
writeln"Problem 31";
-goal FOLP.thy "?p : ~(EX x.P(x) & (Q(x) | R(x))) & \
+goal FOLP.thy "?p : ~(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))";
@@ -282,7 +282,7 @@
writeln"Problem 37";
goal FOLP.thy "?p : (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)))) & \
+\ (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))";
@@ -323,7 +323,7 @@
writeln"Problem 50";
(*What has this to do with equality?*)
-goal FOLP.thy "?p : (ALL x. P(a,x) | (ALL y.P(x,y))) --> (EX x. ALL y.P(x,y))";
+goal FOLP.thy "?p : (ALL x. P(a,x) | (ALL y. P(x,y))) --> (EX x. ALL y. P(x,y))";
by (best_tac FOLP_dup_cs 1);
result();
--- a/src/FOLP/ex/foundn.ML Fri Oct 10 15:52:12 1997 +0200
+++ b/src/FOLP/ex/foundn.ML Fri Oct 10 16:29:41 1997 +0200
@@ -99,7 +99,7 @@
(*Parallel lifting example. *)
-goal IFOLP.thy "?p : EX u.ALL x.EX v.ALL y.EX w. P(u,x,v,y,w)";
+goal IFOLP.thy "?p : EX u. ALL x. EX v. ALL y. EX w. P(u,x,v,y,w)";
by (resolve_tac [exI, allI] 1);
by (resolve_tac [exI, allI] 1);
by (resolve_tac [exI, allI] 1);
@@ -108,7 +108,7 @@
val prems =
-goal IFOLP.thy "p : (EX z.F(z)) & B ==> ?p:(EX z. F(z) & B)";
+goal IFOLP.thy "p : (EX z. F(z)) & B ==> ?p:(EX z. F(z) & B)";
by (rtac conjE 1);
by (resolve_tac prems 1);
by (rtac exE 1);
--- a/src/FOLP/ex/int.ML Fri Oct 10 15:52:12 1997 +0200
+++ b/src/FOLP/ex/int.ML Fri Oct 10 16:29:41 1997 +0200
@@ -180,11 +180,11 @@
writeln"The converse is classical in the following implications...";
-goal IFOLP.thy "?p : (EX x.P(x)-->Q) --> (ALL x.P(x)) --> Q";
+goal IFOLP.thy "?p : (EX x. P(x)-->Q) --> (ALL x. P(x)) --> Q";
by (IntPr.fast_tac 1);
result();
-goal IFOLP.thy "?p : ((ALL x.P(x))-->Q) --> ~ (ALL x. P(x) & ~Q)";
+goal IFOLP.thy "?p : ((ALL x. P(x))-->Q) --> ~ (ALL x. P(x) & ~Q)";
by (IntPr.fast_tac 1);
result();
@@ -192,7 +192,7 @@
by (IntPr.fast_tac 1);
result();
-goal IFOLP.thy "?p : (ALL x.P(x)) | Q --> (ALL x. P(x) | Q)";
+goal IFOLP.thy "?p : (ALL x. P(x)) | Q --> (ALL x. P(x) | Q)";
by (IntPr.fast_tac 1);
result();
@@ -206,15 +206,15 @@
writeln"The following are not constructively valid!";
(*The attempt to prove them terminates quickly!*)
-goal IFOLP.thy "?p : ((ALL x.P(x))-->Q) --> (EX x.P(x)-->Q)";
+goal IFOLP.thy "?p : ((ALL x. P(x))-->Q) --> (EX x. P(x)-->Q)";
by (IntPr.fast_tac 1) handle ERROR => writeln"Failed, as expected";
getgoal 1;
-goal IFOLP.thy "?p : (P --> (EX x.Q(x))) --> (EX x. P-->Q(x))";
+goal IFOLP.thy "?p : (P --> (EX x. Q(x))) --> (EX x. P-->Q(x))";
by (IntPr.fast_tac 1) handle ERROR => writeln"Failed, as expected";
getgoal 1;
-goal IFOLP.thy "?p : (ALL x. P(x) | Q) --> ((ALL x.P(x)) | Q)";
+goal IFOLP.thy "?p : (ALL x. P(x) | Q) --> ((ALL x. P(x)) | Q)";
by (IntPr.fast_tac 1) handle ERROR => writeln"Failed, as expected";
getgoal 1;
@@ -264,7 +264,7 @@
writeln"Problem 24";
goal IFOLP.thy "?p : ~(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)) --> (EX x. Q(x))) & (ALL x. Q(x)|R(x) --> S(x)) \
\ --> ~~(EX x. P(x)&R(x))";
(*Not clear why fast_tac, best_tac, ASTAR and ITER_DEEPEN all take forever*)
by IntPr.safe_tac;
@@ -297,7 +297,7 @@
result();
writeln"Problem 31";
-goal IFOLP.thy "?p : ~(EX x.P(x) & (Q(x) | R(x))) & \
+goal IFOLP.thy "?p : ~(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))";
--- a/src/FOLP/ex/intro.ML Fri Oct 10 15:52:12 1997 +0200
+++ b/src/FOLP/ex/intro.ML Fri Oct 10 16:29:41 1997 +0200
@@ -32,7 +32,7 @@
result();
(*Correct version, delaying use of "spec" until last*)
-goal FOLP.thy "?p:(ALL x y.P(x,y)) --> (ALL z w.P(w,z))";
+goal FOLP.thy "?p:(ALL x y. P(x,y)) --> (ALL z w. P(w,z))";
by (rtac impI 1);
by (rtac allI 1);
by (rtac allI 1);
@@ -69,7 +69,7 @@
(** Derivation of negation introduction **)
-val prems = goal FOLP.thy "(!!x.x:P ==> f(x):False) ==> ?p:~P";
+val prems = goal FOLP.thy "(!!x. x:P ==> f(x):False) ==> ?p:~P";
by (rewtac not_def);
by (rtac impI 1);
by (resolve_tac prems 1);
--- a/src/FOLP/ex/quant.ML Fri Oct 10 15:52:12 1997 +0200
+++ b/src/FOLP/ex/quant.ML Fri Oct 10 16:29:41 1997 +0200
@@ -9,40 +9,40 @@
writeln"File FOLP/ex/quant.ML";
-goal thy "?p : (ALL x y.P(x,y)) --> (ALL y x.P(x,y))";
+goal thy "?p : (ALL x y. P(x,y)) --> (ALL y x. P(x,y))";
by tac;
result();
-goal thy "?p : (EX x y.P(x,y)) --> (EX y x.P(x,y))";
+goal thy "?p : (EX x y. P(x,y)) --> (EX y x. P(x,y))";
by tac;
result();
(*Converse is false*)
-goal thy "?p : (ALL x.P(x)) | (ALL x.Q(x)) --> (ALL x. P(x) | Q(x))";
+goal thy "?p : (ALL x. P(x)) | (ALL x. Q(x)) --> (ALL x. P(x) | Q(x))";
by tac;
result();
-goal thy "?p : (ALL x. P-->Q(x)) <-> (P--> (ALL x.Q(x)))";
+goal thy "?p : (ALL x. P-->Q(x)) <-> (P--> (ALL x. Q(x)))";
by tac;
result();
-goal thy "?p : (ALL x.P(x)-->Q) <-> ((EX x.P(x)) --> Q)";
+goal thy "?p : (ALL x. P(x)-->Q) <-> ((EX x. P(x)) --> Q)";
by tac;
result();
writeln"Some harder ones";
-goal thy "?p : (EX x. P(x) | Q(x)) <-> (EX x.P(x)) | (EX x.Q(x))";
+goal thy "?p : (EX x. P(x) | Q(x)) <-> (EX x. P(x)) | (EX x. Q(x))";
by tac;
result();
(*6 secs*)
(*Converse is false*)
-goal thy "?p : (EX x. P(x)&Q(x)) --> (EX x.P(x)) & (EX x.Q(x))";
+goal thy "?p : (EX x. P(x)&Q(x)) --> (EX x. P(x)) & (EX x. Q(x))";
by tac;
result();
@@ -70,26 +70,26 @@
by tac handle ERROR => writeln"Failed, as expected";
getgoal 1;
-goal thy "?p : P(?a) --> (ALL x.P(x))";
+goal thy "?p : P(?a) --> (ALL x. P(x))";
by tac handle ERROR => writeln"Failed, as expected";
(*Check that subgoals remain: proof failed.*)
getgoal 1;
goal thy
- "?p : (P(?a) --> (ALL x.Q(x))) --> (ALL x. P(x) --> Q(x))";
+ "?p : (P(?a) --> (ALL x. Q(x))) --> (ALL x. P(x) --> Q(x))";
by tac handle ERROR => writeln"Failed, as expected";
getgoal 1;
writeln"Back to things that are provable...";
-goal thy "?p : (ALL x.P(x)-->Q(x)) & (EX x.P(x)) --> (EX x.Q(x))";
+goal thy "?p : (ALL x. P(x)-->Q(x)) & (EX x. P(x)) --> (EX x. Q(x))";
by tac;
result();
(*An example of why exI should be delayed as long as possible*)
-goal thy "?p : (P --> (EX x.Q(x))) & P --> (EX x.Q(x))";
+goal thy "?p : (P --> (EX x. Q(x))) & P --> (EX x. Q(x))";
by tac;
result();
--- a/src/FOLP/simpdata.ML Fri Oct 10 15:52:12 1997 +0200
+++ b/src/FOLP/simpdata.ML Fri Oct 10 16:29:41 1997 +0200
@@ -41,17 +41,17 @@
"(False <-> P) <-> ~P", "(P <-> False) <-> ~P"];
val quant_rews = map int_prove_fun
- ["(ALL x.P) <-> P", "(EX x.P) <-> P"];
+ ["(ALL x. P) <-> P", "(EX x. P) <-> P"];
(*These are NOT supplied by default!*)
val distrib_rews = map int_prove_fun
["~(P|Q) <-> ~P & ~Q",
"P & (Q | R) <-> P&Q | P&R", "(Q | R) & P <-> Q&P | R&P",
"(P | Q --> R) <-> (P --> R) & (Q --> R)",
- "~(EX x.NORM(P(x))) <-> (ALL x. ~NORM(P(x)))",
- "((EX x.NORM(P(x))) --> Q) <-> (ALL x. NORM(P(x)) --> Q)",
- "(EX x.NORM(P(x))) & NORM(Q) <-> (EX x. NORM(P(x)) & NORM(Q))",
- "NORM(Q) & (EX x.NORM(P(x))) <-> (EX x. NORM(Q) & NORM(P(x)))"];
+ "~(EX x. NORM(P(x))) <-> (ALL x. ~NORM(P(x)))",
+ "((EX x. NORM(P(x))) --> Q) <-> (ALL x. NORM(P(x)) --> Q)",
+ "(EX x. NORM(P(x))) & NORM(Q) <-> (EX x. NORM(P(x)) & NORM(Q))",
+ "NORM(Q) & (EX x. NORM(P(x))) <-> (EX x. NORM(Q) & NORM(P(x)))"];
val P_Imp_P_iff_T = int_prove_fun_raw "p:P ==> ?p:(P <-> True)";