# HG changeset patch # User wenzelm # Date 876493781 -7200 # Node ID f1a1817659e628cb255010593174ce987e8c0239 # Parent 9a5a4e123859a5a68adca90804a8aeca10189ae3 fixed dots; diff -r 9a5a4e123859 -r f1a1817659e6 src/Cube/ex/ex.ML --- 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); diff -r 9a5a4e123859 -r f1a1817659e6 src/FOLP/FOLP.ML --- 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), diff -r 9a5a4e123859 -r f1a1817659e6 src/FOLP/FOLP.thy --- 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 diff -r 9a5a4e123859 -r f1a1817659e6 src/FOLP/IFOLP.ML --- 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)) ]); diff -r 9a5a4e123859 -r f1a1817659e6 src/FOLP/IFOLP.thy --- 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 : P" sndB "b:Q ==> snd() = b : Q" pairEC "p:P&Q ==> 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 ****) diff -r 9a5a4e123859 -r f1a1817659e6 src/FOLP/ROOT.ML --- 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 diff -r 9a5a4e123859 -r f1a1817659e6 src/FOLP/ex/If.ML --- 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(); diff -r 9a5a4e123859 -r f1a1817659e6 src/FOLP/ex/cla.ML --- 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(); diff -r 9a5a4e123859 -r f1a1817659e6 src/FOLP/ex/foundn.ML --- 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); diff -r 9a5a4e123859 -r f1a1817659e6 src/FOLP/ex/int.ML --- 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))"; diff -r 9a5a4e123859 -r f1a1817659e6 src/FOLP/ex/intro.ML --- 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); diff -r 9a5a4e123859 -r f1a1817659e6 src/FOLP/ex/quant.ML --- 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(); diff -r 9a5a4e123859 -r f1a1817659e6 src/FOLP/simpdata.ML --- 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)";