--- a/src/FOL/FOL.ML Fri Oct 10 15:51:38 1997 +0200
+++ b/src/FOL/FOL.ML Fri Oct 10 15:52:12 1997 +0200
@@ -22,14 +22,14 @@
(*introduction rule involving only EX*)
qed_goal "ex_classical" FOL.thy
- "( ~(EX x. P(x)) ==> P(a)) ==> EX x.P(x)"
+ "( ~(EX x. P(x)) ==> P(a)) ==> EX x. P(x)"
(fn prems=>
[ (rtac classical 1),
(eresolve_tac (prems RL [exI]) 1) ]);
(*version of above, simplifying ~EX to ALL~ *)
qed_goal "exCI" FOL.thy
- "(ALL x. ~P(x) ==> P(a)) ==> EX x.P(x)"
+ "(ALL x. ~P(x) ==> P(a)) ==> EX x. P(x)"
(fn [prem]=>
[ (rtac ex_classical 1),
(resolve_tac [notI RS allI RS prem] 1),
--- a/src/FOL/IFOL.ML Fri Oct 10 15:51:38 1997 +0200
+++ b/src/FOL/IFOL.ML Fri Oct 10 15:52:12 1997 +0200
@@ -26,12 +26,12 @@
(fn prems=> [ (REPEAT (resolve_tac (prems@[mp]) 1)) ]);
qed_goal "allE" IFOL.thy
- "[| ALL x.P(x); P(x) ==> R |] ==> R"
+ "[| ALL x. P(x); P(x) ==> R |] ==> R"
(fn prems=> [ (REPEAT (resolve_tac (prems@[spec]) 1)) ]);
(*Duplicates the quantifier; for use with eresolve_tac*)
qed_goal "all_dupE" IFOL.thy
- "[| ALL x.P(x); [| P(x); ALL x.P(x) |] ==> R \
+ "[| ALL x. P(x); [| P(x); ALL x. P(x) |] ==> R \
\ |] ==> R"
(fn prems=> [ (REPEAT (resolve_tac (prems@[spec]) 1)) ]);
@@ -126,12 +126,12 @@
(*Sometimes easier to use: the premises have no shared variables. Safe!*)
qed_goal "ex_ex1I" IFOL.thy
- "[| EX x.P(x); !!x y. [| P(x); P(y) |] ==> x=y |] ==> EX! x. P(x)"
+ "[| EX x. P(x); !!x y. [| P(x); P(y) |] ==> x=y |] ==> EX! x. P(x)"
(fn [ex,eq] => [ (rtac (ex RS exE) 1),
(REPEAT (ares_tac [ex1I,eq] 1)) ]);
qed_goalw "ex1E" IFOL.thy [ex1_def]
- "[| EX! x.P(x); !!x. [| P(x); ALL y. P(y) --> y=x |] ==> R |] ==> R"
+ "[| EX! x. P(x); !!x. [| P(x); ALL y. P(y) --> y=x |] ==> R |] ==> R"
(fn prems =>
[ (cut_facts_tac prems 1),
(REPEAT (eresolve_tac [exE,conjE] 1 ORELSE ares_tac prems 1)) ]);
@@ -194,21 +194,21 @@
ORELSE eresolve_tac [iffE,notE] 1)) ]);
qed_goal "all_cong" IFOL.thy
- "(!!x.P(x) <-> Q(x)) ==> (ALL x.P(x)) <-> (ALL x.Q(x))"
+ "(!!x. P(x) <-> Q(x)) ==> (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)) ]);
qed_goal "ex_cong" IFOL.thy
- "(!!x.P(x) <-> Q(x)) ==> (EX x.P(x)) <-> (EX x.Q(x))"
+ "(!!x. P(x) <-> Q(x)) ==> (EX x. P(x)) <-> (EX x. Q(x))"
(fn prems =>
[ (REPEAT (etac exE 1 ORELSE ares_tac [iffI,exI] 1
ORELSE mp_tac 1
ORELSE iff_tac prems 1)) ]);
qed_goal "ex1_cong" IFOL.thy
- "(!!x.P(x) <-> Q(x)) ==> (EX! x.P(x)) <-> (EX! x.Q(x))"
+ "(!!x. P(x) <-> Q(x)) ==> (EX! x. P(x)) <-> (EX! x. Q(x))"
(fn prems =>
[ (REPEAT (eresolve_tac [ex1E, spec RS mp] 1 ORELSE ares_tac [iffI,ex1I] 1
ORELSE mp_tac 1
@@ -231,7 +231,7 @@
(*A special case of ex1E that would otherwise need quantifier expansion*)
qed_goal "ex1_equalsE" IFOL.thy
- "[| EX! x.P(x); P(a); P(b) |] ==> a=b"
+ "[| EX! x. P(x); P(a); P(b) |] ==> a=b"
(fn prems =>
[ (cut_facts_tac prems 1),
(etac ex1E 1),
@@ -352,13 +352,13 @@
(*What if (ALL x.~~P(x)) --> ~~(ALL x.P(x)) is an assumption? UNSAFE*)
qed_goal "all_impE" IFOL.thy
- "[| (ALL x.P(x))-->S; !!x.P(x); S ==> R |] ==> R"
+ "[| (ALL x. P(x))-->S; !!x. P(x); S ==> R |] ==> 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. *)
qed_goal "ex_impE" IFOL.thy
- "[| (EX x.P(x))-->S; P(x)-->S ==> R |] ==> R"
+ "[| (EX x. P(x))-->S; P(x)-->S ==> R |] ==> R"
(fn major::prems=>
[ (REPEAT (ares_tac ([exI, impI, major RS mp]@prems) 1)) ]);
--- a/src/FOL/IFOL.thy Fri Oct 10 15:51:38 1997 +0200
+++ b/src/FOL/IFOL.thy Fri Oct 10 15:52:12 1997 +0200
@@ -96,11 +96,11 @@
(* Quantifiers *)
- allI "(!!x. P(x)) ==> (ALL x.P(x))"
- spec "(ALL x.P(x)) ==> P(x)"
+ allI "(!!x. P(x)) ==> (ALL x. P(x))"
+ spec "(ALL x. P(x)) ==> P(x)"
- exI "P(x) ==> (EX x.P(x))"
- exE "[| EX x.P(x); !!x. P(x) ==> R |] ==> R"
+ exI "P(x) ==> (EX x. P(x))"
+ exE "[| EX x. P(x); !!x. P(x) ==> R |] ==> R"
(* Reflection *)
--- a/src/FOL/cladata.ML Fri Oct 10 15:51:38 1997 +0200
+++ b/src/FOL/cladata.ML Fri Oct 10 15:52:12 1997 +0200
@@ -25,7 +25,7 @@
(*Better for fast_tac: needs no quantifier duplication!*)
qed_goal "alt_ex1E" IFOL.thy
- "[| EX! x.P(x); \
+ "[| EX! x. P(x); \
\ !!x. [| P(x); ALL y y'. P(y) & P(y') --> y=y' |] ==> R \
\ |] ==> R"
(fn major::prems =>
--- a/src/FOL/ex/List.ML Fri Oct 10 15:51:38 1997 +0200
+++ b/src/FOL/ex/List.ML Fri Oct 10 15:52:12 1997 +0200
@@ -8,7 +8,7 @@
open List;
-val prems = goal List.thy "[| P([]); !!x l. P(x.l) |] ==> All(P)";
+val prems = goal List.thy "[| P([]); !!x l. P(x. l) |] ==> All(P)";
by (rtac list_ind 1);
by (REPEAT (resolve_tac (prems@[allI,impI]) 1));
qed "list_exh";
@@ -37,7 +37,7 @@
by (IND_TAC list_ind Simp_tac "l" 1);
qed "forall_app";
-goal List.thy "forall(l,%x.P(x)&Q(x)) <-> forall(l,P) & forall(l,Q)";
+goal List.thy "forall(l,%x. P(x)&Q(x)) <-> forall(l,P) & forall(l,Q)";
by (IND_TAC list_ind Simp_tac "l" 1);
by (Fast_tac 1);
qed "forall_conj";
@@ -59,7 +59,7 @@
by (ALL_IND_TAC nat_exh Asm_simp_tac 1);
qed "at_app1";
-goal List.thy "at(l1++(x.l2), len(l1)) = x";
+goal List.thy "at(l1++(x. l2), len(l1)) = x";
by (IND_TAC list_ind Simp_tac "l1" 1);
qed "at_app_hd2";
--- a/src/FOL/ex/List.thy Fri Oct 10 15:51:38 1997 +0200
+++ b/src/FOL/ex/List.thy Fri Oct 10 15:52:12 1997 +0200
@@ -22,28 +22,28 @@
"++" :: ['a list, 'a list] => 'a list (infixr 70)
rules
- list_ind "[| P([]); ALL x l. P(l)-->P(x.l) |] ==> All(P)"
+ list_ind "[| P([]); ALL x l. P(l)-->P(x. l) |] ==> All(P)"
forall_cong
"[| l = l'; !!x. P(x)<->P'(x) |] ==> forall(l,P) <-> forall(l',P')"
- list_distinct1 "~[] = x.l"
- list_distinct2 "~x.l = []"
+ list_distinct1 "~[] = x. l"
+ list_distinct2 "~x. l = []"
- list_free "x.l = x'.l' <-> x=x' & l=l'"
+ list_free "x. l = x'. l' <-> x=x' & l=l'"
app_nil "[]++l = l"
- app_cons "(x.l)++l' = x.(l++l')"
- tl_eq "tl(m.q) = q"
- hd_eq "hd(m.q) = m"
+ app_cons "(x. l)++l' = x.(l++l')"
+ tl_eq "tl(m. q) = q"
+ hd_eq "hd(m. q) = m"
forall_nil "forall([],P)"
- forall_cons "forall(x.l,P) <-> P(x) & forall(l,P)"
+ forall_cons "forall(x. l,P) <-> P(x) & forall(l,P)"
len_nil "len([]) = 0"
- len_cons "len(m.q) = succ(len(q))"
+ len_cons "len(m. q) = succ(len(q))"
- at_0 "at(m.q,0) = m"
- at_succ "at(m.q,succ(n)) = at(q,n)"
+ at_0 "at(m. q,0) = m"
+ at_succ "at(m. q,succ(n)) = at(q,n)"
end
--- a/src/FOL/ex/cla.ML Fri Oct 10 15:51:38 1997 +0200
+++ b/src/FOL/ex/cla.ML Fri Oct 10 15:52:12 1997 +0200
@@ -127,22 +127,22 @@
by (Blast_tac 1);
result();
-goal FOL.thy "(EX x. P-->Q(x)) <-> (P --> (EX x.Q(x)))";
+goal FOL.thy "(EX x. P-->Q(x)) <-> (P --> (EX x. Q(x)))";
by (Blast_tac 1);
result();
-goal FOL.thy "(EX x.P(x)-->Q) <-> (ALL x.P(x)) --> Q";
+goal FOL.thy "(EX x. P(x)-->Q) <-> (ALL x. P(x)) --> Q";
by (Blast_tac 1);
result();
-goal FOL.thy "(ALL x.P(x)) | Q <-> (ALL x. P(x) | Q)";
+goal FOL.thy "(ALL x. P(x)) | Q <-> (ALL x. P(x) | Q)";
by (Blast_tac 1);
result();
(*Discussed in Avron, Gentzen-Type Systems, Resolution and Tableaux,
JAR 10 (265-281), 1993. Proof is trivial!*)
goal FOL.thy
- "~ ((EX x.~P(x)) & ((EX x.P(x)) | (EX x.P(x) & Q(x))) & ~ (EX x.P(x)))";
+ "~ ((EX x.~P(x)) & ((EX x. P(x)) | (EX x. P(x) & Q(x))) & ~ (EX x. P(x)))";
by (Blast_tac 1);
result();
@@ -207,7 +207,7 @@
writeln"Problem 24";
goal FOL.thy "~(EX x. S(x)&Q(x)) & (ALL x. P(x) --> Q(x)|R(x)) & \
-\ (~(EX x.P(x)) --> (EX x.Q(x))) & (ALL x. Q(x)|R(x) --> S(x)) \
+\ (~(EX x. P(x)) --> (EX x. Q(x))) & (ALL x. Q(x)|R(x) --> S(x)) \
\ --> (EX x. P(x)&R(x))";
by (Blast_tac 1);
result();
@@ -240,7 +240,7 @@
writeln"Problem 28. AMENDED";
goal FOL.thy "(ALL x. P(x) --> (ALL x. Q(x))) & \
\ ((ALL x. Q(x)|R(x)) --> (EX x. Q(x)&S(x))) & \
-\ ((EX x.S(x)) --> (ALL x. L(x) --> M(x))) \
+\ ((EX x. S(x)) --> (ALL x. L(x) --> M(x))) \
\ --> (ALL x. P(x) & L(x) --> M(x))";
by (Blast_tac 1);
result();
@@ -260,7 +260,7 @@
result();
writeln"Problem 31";
-goal FOL.thy "~(EX x.P(x) & (Q(x) | R(x))) & \
+goal FOL.thy "~(EX x. P(x) & (Q(x) | R(x))) & \
\ (EX x. L(x) & P(x)) & \
\ (ALL x. ~ R(x) --> M(x)) \
\ --> (EX x. L(x) & M(x))";
@@ -306,7 +306,7 @@
writeln"Problem 37";
goal FOL.thy "(ALL z. EX w. ALL x. EX y. \
-\ (P(x,z)-->P(y,w)) & P(y,z) & (P(y,w) --> (EX u.Q(u,w)))) & \
+\ (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))";
@@ -385,7 +385,7 @@
(*Hard because it involves substitution for Vars;
the type constraint ensures that x,y,z have the same type as a,b,u. *)
goal FOL.thy "(EX x y::'a. ALL z. z=x | z=y) & P(a) & P(b) & a~=b \
-\ --> (ALL u::'a.P(u))";
+\ --> (ALL u::'a. P(u))";
by Safe_tac;
by (res_inst_tac [("x","a")] allE 1);
by (assume_tac 1);
@@ -396,7 +396,7 @@
writeln"Problem 50";
(*What has this to do with equality?*)
-goal FOL.thy "(ALL x. P(a,x) | (ALL y.P(x,y))) --> (EX x. ALL y.P(x,y))";
+goal FOL.thy "(ALL x. P(a,x) | (ALL y. P(x,y))) --> (EX x. ALL y. P(x,y))";
by (Blast_tac 1);
result();
--- a/src/FOL/ex/foundn.ML Fri Oct 10 15:51:38 1997 +0200
+++ b/src/FOL/ex/foundn.ML Fri Oct 10 15:52:12 1997 +0200
@@ -99,7 +99,7 @@
(*Parallel lifting example. *)
-goal IFOL.thy "EX u.ALL x.EX v.ALL y.EX w. P(u,x,v,y,w)";
+goal IFOL.thy "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 IFOL.thy "(EX z.F(z)) & B ==> (EX z. F(z) & B)";
+goal IFOL.thy "(EX z. F(z)) & B ==> (EX z. F(z) & B)";
by (rtac conjE 1);
by (resolve_tac prems 1);
by (rtac exE 1);
--- a/src/FOL/ex/int.ML Fri Oct 10 15:51:38 1997 +0200
+++ b/src/FOL/ex/int.ML Fri Oct 10 15:52:12 1997 +0200
@@ -211,11 +211,11 @@
writeln"The converse is classical in the following implications...";
-goal IFOL.thy "(EX x.P(x)-->Q) --> (ALL x.P(x)) --> Q";
+goal IFOL.thy "(EX x. P(x)-->Q) --> (ALL x. P(x)) --> Q";
by (IntPr.fast_tac 1);
result();
-goal IFOL.thy "((ALL x.P(x))-->Q) --> ~ (ALL x. P(x) & ~Q)";
+goal IFOL.thy "((ALL x. P(x))-->Q) --> ~ (ALL x. P(x) & ~Q)";
by (IntPr.fast_tac 1);
result();
@@ -223,7 +223,7 @@
by (IntPr.fast_tac 1);
result();
-goal IFOL.thy "(ALL x.P(x)) | Q --> (ALL x. P(x) | Q)";
+goal IFOL.thy "(ALL x. P(x)) | Q --> (ALL x. P(x) | Q)";
by (IntPr.fast_tac 1);
result();
@@ -237,15 +237,15 @@
writeln"The following are not constructively valid!";
(*The attempt to prove them terminates quickly!*)
-goal IFOL.thy "((ALL x.P(x))-->Q) --> (EX x.P(x)-->Q)";
+goal IFOL.thy "((ALL x. P(x))-->Q) --> (EX x. P(x)-->Q)";
by (IntPr.fast_tac 1) handle ERROR => writeln"Failed, as expected";
getgoal 1;
-goal IFOL.thy "(P --> (EX x.Q(x))) --> (EX x. P-->Q(x))";
+goal IFOL.thy "(P --> (EX x. Q(x))) --> (EX x. P-->Q(x))";
by (IntPr.fast_tac 1) handle ERROR => writeln"Failed, as expected";
getgoal 1;
-goal IFOL.thy "(ALL x. P(x) | Q) --> ((ALL x.P(x)) | Q)";
+goal IFOL.thy "(ALL x. P(x) | Q) --> ((ALL x. P(x)) | Q)";
by (IntPr.fast_tac 1) handle ERROR => writeln"Failed, as expected";
getgoal 1;
@@ -294,7 +294,7 @@
writeln"Problem 24";
goal IFOL.thy "~(EX x. S(x)&Q(x)) & (ALL x. P(x) --> Q(x)|R(x)) & \
-\ (~(EX x.P(x)) --> (EX x.Q(x))) & (ALL x. Q(x)|R(x) --> S(x)) \
+\ (~(EX x. P(x)) --> (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;
@@ -330,7 +330,7 @@
writeln"Problem ~~28. AMENDED";
goal IFOL.thy "(ALL x. P(x) --> (ALL x. Q(x))) & \
\ (~~(ALL x. Q(x)|R(x)) --> (EX x. Q(x)&S(x))) & \
-\ (~~(EX x.S(x)) --> (ALL x. L(x) --> M(x))) \
+\ (~~(EX x. S(x)) --> (ALL x. L(x) --> M(x))) \
\ --> (ALL x. P(x) & L(x) --> M(x))";
by (IntPr.fast_tac 1); (*48 secs*)
result();
@@ -350,7 +350,7 @@
result();
writeln"Problem 31";
-goal IFOL.thy "~(EX x.P(x) & (Q(x) | R(x))) & \
+goal IFOL.thy "~(EX x. P(x) & (Q(x) | R(x))) & \
\ (EX x. L(x) & P(x)) & \
\ (ALL x. ~ R(x) --> M(x)) \
\ --> (EX x. L(x) & M(x))";
@@ -384,7 +384,7 @@
writeln"Problem 37";
goal IFOL.thy
"(ALL z. EX w. ALL x. EX y. \
-\ ~~(P(x,z)-->P(y,w)) & P(y,z) & (P(y,w) --> (EX u.Q(u,w)))) & \
+\ ~~(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))";
--- a/src/FOL/ex/intro.ML Fri Oct 10 15:51:38 1997 +0200
+++ b/src/FOL/ex/intro.ML Fri Oct 10 15:52:12 1997 +0200
@@ -32,7 +32,7 @@
result();
(*Correct version, delaying use of "spec" until last*)
-goal FOL.thy "(ALL x y.P(x,y)) --> (ALL z w.P(w,z))";
+goal FOL.thy "(ALL x y. P(x,y)) --> (ALL z w. P(w,z))";
by (rtac impI 1);
by (rtac allI 1);
by (rtac allI 1);
--- a/src/FOL/ex/mini.ML Fri Oct 10 15:51:38 1997 +0200
+++ b/src/FOL/ex/mini.ML Fri Oct 10 15:52:12 1997 +0200
@@ -26,8 +26,8 @@
["~(P&Q) <-> ~P | ~Q",
"~(P|Q) <-> ~P & ~Q",
"~~P <-> P",
- "~(ALL x.P(x)) <-> (EX x. ~P(x))",
- "~(EX x.P(x)) <-> (ALL x. ~P(x))"];
+ "~(ALL x. P(x)) <-> (EX x. ~P(x))",
+ "~(EX x. P(x)) <-> (ALL x. ~P(x))"];
(*** Removal of --> and <-> (positive and negative occurrences) ***)
(*Last one is important for computing a compact CNF*)
@@ -43,21 +43,21 @@
val ex_simps = map prove_fun
["(EX x. P) <-> P",
- "(EX x. P(x) & Q) <-> (EX x.P(x)) & Q",
- "(EX x. P & Q(x)) <-> P & (EX x.Q(x))",
- "(EX x. P(x) | Q(x)) <-> (EX x.P(x)) | (EX x.Q(x))",
- "(EX x. P(x) | Q) <-> (EX x.P(x)) | Q",
- "(EX x. P | Q(x)) <-> P | (EX x.Q(x))"];
+ "(EX x. P(x) & Q) <-> (EX x. P(x)) & Q",
+ "(EX x. P & Q(x)) <-> P & (EX x. Q(x))",
+ "(EX x. P(x) | Q(x)) <-> (EX x. P(x)) | (EX x. Q(x))",
+ "(EX x. P(x) | Q) <-> (EX x. P(x)) | Q",
+ "(EX x. P | Q(x)) <-> P | (EX x. Q(x))"];
(*** Pushing in the universal quantifiers ***)
val all_simps = map prove_fun
["(ALL x. P) <-> P",
- "(ALL x. P(x) & Q(x)) <-> (ALL x.P(x)) & (ALL x.Q(x))",
- "(ALL x. P(x) & Q) <-> (ALL x.P(x)) & Q",
- "(ALL x. P & Q(x)) <-> P & (ALL x.Q(x))",
- "(ALL x. P(x) | Q) <-> (ALL x.P(x)) | Q",
- "(ALL x. P | Q(x)) <-> P | (ALL x.Q(x))"];
+ "(ALL x. P(x) & Q(x)) <-> (ALL x. P(x)) & (ALL x. Q(x))",
+ "(ALL x. P(x) & Q) <-> (ALL x. P(x)) & Q",
+ "(ALL x. P & Q(x)) <-> P & (ALL x. Q(x))",
+ "(ALL x. P(x) | Q) <-> (ALL x. P(x)) | Q",
+ "(ALL x. P | Q(x)) <-> P | (ALL x. Q(x))"];
val mini_ss=FOL_basic_ss addsimps (demorgans @ nnf_simps @ ex_simps @ all_simps);
--- a/src/FOL/ex/quant.ML Fri Oct 10 15:51:38 1997 +0200
+++ b/src/FOL/ex/quant.ML Fri Oct 10 15:52:12 1997 +0200
@@ -9,40 +9,40 @@
writeln"File FOL/ex/quant.";
-goal thy "(ALL x y.P(x,y)) --> (ALL y x.P(x,y))";
+goal thy "(ALL x y. P(x,y)) --> (ALL y x. P(x,y))";
by tac;
result();
-goal thy "(EX x y.P(x,y)) --> (EX y x.P(x,y))";
+goal thy "(EX x y. P(x,y)) --> (EX y x. P(x,y))";
by tac;
result();
(*Converse is false*)
-goal thy "(ALL x.P(x)) | (ALL x.Q(x)) --> (ALL x. P(x) | Q(x))";
+goal thy "(ALL x. P(x)) | (ALL x. Q(x)) --> (ALL x. P(x) | Q(x))";
by tac;
result();
-goal thy "(ALL x. P-->Q(x)) <-> (P--> (ALL x.Q(x)))";
+goal thy "(ALL x. P-->Q(x)) <-> (P--> (ALL x. Q(x)))";
by tac;
result();
-goal thy "(ALL x.P(x)-->Q) <-> ((EX x.P(x)) --> Q)";
+goal thy "(ALL x. P(x)-->Q) <-> ((EX x. P(x)) --> Q)";
by tac;
result();
writeln"Some harder ones";
-goal thy "(EX x. P(x) | Q(x)) <-> (EX x.P(x)) | (EX x.Q(x))";
+goal thy "(EX x. P(x) | Q(x)) <-> (EX x. P(x)) | (EX x. Q(x))";
by tac;
result();
(*6 secs*)
(*Converse is false*)
-goal thy "(EX x. P(x)&Q(x)) --> (EX x.P(x)) & (EX x.Q(x))";
+goal thy "(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(?a) --> (ALL x.P(x))";
+goal thy "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(?a) --> (ALL x.Q(x))) --> (ALL x. P(x) --> Q(x))";
+ "(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 "(ALL x.P(x)-->Q(x)) & (EX x.P(x)) --> (EX x.Q(x))";
+goal thy "(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 --> (EX x.Q(x))) & P --> (EX x.Q(x))";
+goal thy "(P --> (EX x. Q(x))) & P --> (EX x. Q(x))";
by tac;
result();
--- a/src/FOL/simpdata.ML Fri Oct 10 15:51:38 1997 +0200
+++ b/src/FOL/simpdata.ML Fri Oct 10 15:52:12 1997 +0200
@@ -42,7 +42,7 @@
"(False <-> P) <-> ~P", "(P <-> False) <-> ~P"];
val quant_simps = 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_simps = map int_prove_fun
@@ -103,23 +103,23 @@
val ex_simps = map prove_fun
["(EX x. x=t & P(x)) <-> P(t)",
"(EX x. t=x & P(x)) <-> P(t)",
- "(EX x. P(x) & Q) <-> (EX x.P(x)) & Q",
- "(EX x. P & Q(x)) <-> P & (EX x.Q(x))",
- "(EX x. P(x) | Q) <-> (EX x.P(x)) | Q",
- "(EX x. P | Q(x)) <-> P | (EX x.Q(x))",
- "(EX x. P(x) --> Q) <-> (ALL x.P(x)) --> Q",
- "(EX x. P --> Q(x)) <-> P --> (EX x.Q(x))"];
+ "(EX x. P(x) & Q) <-> (EX x. P(x)) & Q",
+ "(EX x. P & Q(x)) <-> P & (EX x. Q(x))",
+ "(EX x. P(x) | Q) <-> (EX x. P(x)) | Q",
+ "(EX x. P | Q(x)) <-> P | (EX x. Q(x))",
+ "(EX x. P(x) --> Q) <-> (ALL x. P(x)) --> Q",
+ "(EX x. P --> Q(x)) <-> P --> (EX x. Q(x))"];
(*Miniscoping: pushing in universal quantifiers*)
val all_simps = map prove_fun
["(ALL x. x=t --> P(x)) <-> P(t)",
"(ALL x. t=x --> P(x)) <-> P(t)",
- "(ALL x. P(x) & Q) <-> (ALL x.P(x)) & Q",
- "(ALL x. P & Q(x)) <-> P & (ALL x.Q(x))",
- "(ALL x. P(x) | Q) <-> (ALL x.P(x)) | Q",
- "(ALL x. P | Q(x)) <-> P | (ALL x.Q(x))",
- "(ALL x. P(x) --> Q) <-> (EX x.P(x)) --> Q",
- "(ALL x. P --> Q(x)) <-> P --> (ALL x.Q(x))"];
+ "(ALL x. P(x) & Q) <-> (ALL x. P(x)) & Q",
+ "(ALL x. P & Q(x)) <-> P & (ALL x. Q(x))",
+ "(ALL x. P(x) | Q) <-> (ALL x. P(x)) | Q",
+ "(ALL x. P | Q(x)) <-> P | (ALL x. Q(x))",
+ "(ALL x. P(x) --> Q) <-> (EX x. P(x)) --> Q",
+ "(ALL x. P --> Q(x)) <-> P --> (ALL x. Q(x))"];
fun int_prove nm thm = qed_goal nm IFOL.thy thm
(fn prems => [ (cut_facts_tac prems 1),
@@ -150,9 +150,9 @@
prove "not_iff" "~(P <-> Q) <-> (P <-> ~Q)";
-prove "not_all" "(~ (ALL x.P(x))) <-> (EX x.~P(x))";
-prove "imp_all" "((ALL x.P(x)) --> Q) <-> (EX x.P(x) --> Q)";
-int_prove "not_ex" "(~ (EX x.P(x))) <-> (ALL x.~P(x))";
+prove "not_all" "(~ (ALL x. P(x))) <-> (EX x.~P(x))";
+prove "imp_all" "((ALL x. P(x)) --> Q) <-> (EX x. P(x) --> Q)";
+int_prove "not_ex" "(~ (EX x. P(x))) <-> (ALL x.~P(x))";
int_prove "imp_ex" "((EX x. P(x)) --> Q) <-> (ALL x. P(x) --> Q)";
int_prove "ex_disj_distrib"
--- a/src/Provers/splitter.ML Fri Oct 10 15:51:38 1997 +0200
+++ b/src/Provers/splitter.ML Fri Oct 10 15:52:12 1997 +0200
@@ -32,7 +32,7 @@
val lift =
let val ct = read_cterm (#sign(rep_thm iffD))
("[| !!x::'b::logic. Q(x) == R(x) |] ==> \
- \P(%x.Q(x)) == P(%x.R(x))::'a::logic",propT)
+ \P(%x. Q(x)) == P(%x. R(x))::'a::logic",propT)
in prove_goalw_cterm [] ct
(fn [prem] => [rewtac prem, rtac reflexive_thm 1])
end;