fixed dots;
authorwenzelm
Fri Oct 10 15:52:12 1997 +0200 (1997-10-10 ago)
changeset 38359a5a4e123859
parent 3834 278f0a1e5986
child 3836 f1a1817659e6
fixed dots;
src/FOL/FOL.ML
src/FOL/IFOL.ML
src/FOL/IFOL.thy
src/FOL/cladata.ML
src/FOL/ex/List.ML
src/FOL/ex/List.thy
src/FOL/ex/cla.ML
src/FOL/ex/foundn.ML
src/FOL/ex/int.ML
src/FOL/ex/intro.ML
src/FOL/ex/mini.ML
src/FOL/ex/quant.ML
src/FOL/simpdata.ML
src/Provers/splitter.ML
     1.1 --- a/src/FOL/FOL.ML	Fri Oct 10 15:51:38 1997 +0200
     1.2 +++ b/src/FOL/FOL.ML	Fri Oct 10 15:52:12 1997 +0200
     1.3 @@ -22,14 +22,14 @@
     1.4  
     1.5  (*introduction rule involving only EX*)
     1.6  qed_goal "ex_classical" FOL.thy 
     1.7 -   "( ~(EX x. P(x)) ==> P(a)) ==> EX x.P(x)"
     1.8 +   "( ~(EX x. P(x)) ==> P(a)) ==> EX x. P(x)"
     1.9   (fn prems=>
    1.10    [ (rtac classical 1),
    1.11      (eresolve_tac (prems RL [exI]) 1) ]);
    1.12  
    1.13  (*version of above, simplifying ~EX to ALL~ *)
    1.14  qed_goal "exCI" FOL.thy 
    1.15 -   "(ALL x. ~P(x) ==> P(a)) ==> EX x.P(x)"
    1.16 +   "(ALL x. ~P(x) ==> P(a)) ==> EX x. P(x)"
    1.17   (fn [prem]=>
    1.18    [ (rtac ex_classical 1),
    1.19      (resolve_tac [notI RS allI RS prem] 1),
     2.1 --- a/src/FOL/IFOL.ML	Fri Oct 10 15:51:38 1997 +0200
     2.2 +++ b/src/FOL/IFOL.ML	Fri Oct 10 15:52:12 1997 +0200
     2.3 @@ -26,12 +26,12 @@
     2.4   (fn prems=> [ (REPEAT (resolve_tac (prems@[mp]) 1)) ]);
     2.5  
     2.6  qed_goal "allE" IFOL.thy 
     2.7 -    "[| ALL x.P(x); P(x) ==> R |] ==> R"
     2.8 +    "[| ALL x. P(x); P(x) ==> R |] ==> R"
     2.9   (fn prems=> [ (REPEAT (resolve_tac (prems@[spec]) 1)) ]);
    2.10  
    2.11  (*Duplicates the quantifier; for use with eresolve_tac*)
    2.12  qed_goal "all_dupE" IFOL.thy 
    2.13 -    "[| ALL x.P(x);  [| P(x); ALL x.P(x) |] ==> R \
    2.14 +    "[| ALL x. P(x);  [| P(x); ALL x. P(x) |] ==> R \
    2.15  \    |] ==> R"
    2.16   (fn prems=> [ (REPEAT (resolve_tac (prems@[spec]) 1)) ]);
    2.17  
    2.18 @@ -126,12 +126,12 @@
    2.19  
    2.20  (*Sometimes easier to use: the premises have no shared variables.  Safe!*)
    2.21  qed_goal "ex_ex1I" IFOL.thy
    2.22 -    "[| EX x.P(x);  !!x y. [| P(x); P(y) |] ==> x=y |] ==> EX! x. P(x)"
    2.23 +    "[| EX x. P(x);  !!x y. [| P(x); P(y) |] ==> x=y |] ==> EX! x. P(x)"
    2.24   (fn [ex,eq] => [ (rtac (ex RS exE) 1),
    2.25                    (REPEAT (ares_tac [ex1I,eq] 1)) ]);
    2.26  
    2.27  qed_goalw "ex1E" IFOL.thy [ex1_def]
    2.28 -    "[| EX! x.P(x);  !!x. [| P(x);  ALL y. P(y) --> y=x |] ==> R |] ==> R"
    2.29 +    "[| EX! x. P(x);  !!x. [| P(x);  ALL y. P(y) --> y=x |] ==> R |] ==> R"
    2.30   (fn prems =>
    2.31    [ (cut_facts_tac prems 1),
    2.32      (REPEAT (eresolve_tac [exE,conjE] 1 ORELSE ares_tac prems 1)) ]);
    2.33 @@ -194,21 +194,21 @@
    2.34        ORELSE  eresolve_tac [iffE,notE] 1)) ]);
    2.35  
    2.36  qed_goal "all_cong" IFOL.thy 
    2.37 -    "(!!x.P(x) <-> Q(x)) ==> (ALL x.P(x)) <-> (ALL x.Q(x))"
    2.38 +    "(!!x. P(x) <-> Q(x)) ==> (ALL x. P(x)) <-> (ALL x. Q(x))"
    2.39   (fn prems =>
    2.40    [ (REPEAT   (ares_tac [iffI,allI] 1
    2.41        ORELSE   mp_tac 1
    2.42        ORELSE   etac allE 1 ORELSE iff_tac prems 1)) ]);
    2.43  
    2.44  qed_goal "ex_cong" IFOL.thy 
    2.45 -    "(!!x.P(x) <-> Q(x)) ==> (EX x.P(x)) <-> (EX x.Q(x))"
    2.46 +    "(!!x. P(x) <-> Q(x)) ==> (EX x. P(x)) <-> (EX x. Q(x))"
    2.47   (fn prems =>
    2.48    [ (REPEAT   (etac exE 1 ORELSE ares_tac [iffI,exI] 1
    2.49        ORELSE   mp_tac 1
    2.50        ORELSE   iff_tac prems 1)) ]);
    2.51  
    2.52  qed_goal "ex1_cong" IFOL.thy 
    2.53 -    "(!!x.P(x) <-> Q(x)) ==> (EX! x.P(x)) <-> (EX! x.Q(x))"
    2.54 +    "(!!x. P(x) <-> Q(x)) ==> (EX! x. P(x)) <-> (EX! x. Q(x))"
    2.55   (fn prems =>
    2.56    [ (REPEAT   (eresolve_tac [ex1E, spec RS mp] 1 ORELSE ares_tac [iffI,ex1I] 1
    2.57        ORELSE   mp_tac 1
    2.58 @@ -231,7 +231,7 @@
    2.59  
    2.60  (*A special case of ex1E that would otherwise need quantifier expansion*)
    2.61  qed_goal "ex1_equalsE" IFOL.thy
    2.62 -    "[| EX! x.P(x);  P(a);  P(b) |] ==> a=b"
    2.63 +    "[| EX! x. P(x);  P(a);  P(b) |] ==> a=b"
    2.64   (fn prems =>
    2.65    [ (cut_facts_tac prems 1),
    2.66      (etac ex1E 1),
    2.67 @@ -352,13 +352,13 @@
    2.68  
    2.69  (*What if (ALL x.~~P(x)) --> ~~(ALL x.P(x)) is an assumption? UNSAFE*)
    2.70  qed_goal "all_impE" IFOL.thy 
    2.71 -    "[| (ALL x.P(x))-->S;  !!x.P(x);  S ==> R |] ==> R"
    2.72 +    "[| (ALL x. P(x))-->S;  !!x. P(x);  S ==> R |] ==> R"
    2.73   (fn major::prems=>
    2.74    [ (REPEAT (ares_tac ([allI, impI, major RS mp]@prems) 1)) ]);
    2.75  
    2.76  (*Unsafe: (EX x.P(x))-->S  is equivalent to  ALL x.P(x)-->S.  *)
    2.77  qed_goal "ex_impE" IFOL.thy 
    2.78 -    "[| (EX x.P(x))-->S;  P(x)-->S ==> R |] ==> R"
    2.79 +    "[| (EX x. P(x))-->S;  P(x)-->S ==> R |] ==> R"
    2.80   (fn major::prems=>
    2.81    [ (REPEAT (ares_tac ([exI, impI, major RS mp]@prems) 1)) ]);
    2.82  
     3.1 --- a/src/FOL/IFOL.thy	Fri Oct 10 15:51:38 1997 +0200
     3.2 +++ b/src/FOL/IFOL.thy	Fri Oct 10 15:52:12 1997 +0200
     3.3 @@ -96,11 +96,11 @@
     3.4  
     3.5    (* Quantifiers *)
     3.6  
     3.7 -  allI          "(!!x. P(x)) ==> (ALL x.P(x))"
     3.8 -  spec          "(ALL x.P(x)) ==> P(x)"
     3.9 +  allI          "(!!x. P(x)) ==> (ALL x. P(x))"
    3.10 +  spec          "(ALL x. P(x)) ==> P(x)"
    3.11  
    3.12 -  exI           "P(x) ==> (EX x.P(x))"
    3.13 -  exE           "[| EX x.P(x);  !!x. P(x) ==> R |] ==> R"
    3.14 +  exI           "P(x) ==> (EX x. P(x))"
    3.15 +  exE           "[| EX x. P(x);  !!x. P(x) ==> R |] ==> R"
    3.16  
    3.17    (* Reflection *)
    3.18  
     4.1 --- a/src/FOL/cladata.ML	Fri Oct 10 15:51:38 1997 +0200
     4.2 +++ b/src/FOL/cladata.ML	Fri Oct 10 15:52:12 1997 +0200
     4.3 @@ -25,7 +25,7 @@
     4.4  
     4.5  (*Better for fast_tac: needs no quantifier duplication!*)
     4.6  qed_goal "alt_ex1E" IFOL.thy
     4.7 -    "[| EX! x.P(x);                                              \
     4.8 +    "[| EX! x. P(x);                                              \
     4.9  \       !!x. [| P(x);  ALL y y'. P(y) & P(y') --> y=y' |] ==> R  \
    4.10  \    |] ==> R"
    4.11   (fn major::prems =>
     5.1 --- a/src/FOL/ex/List.ML	Fri Oct 10 15:51:38 1997 +0200
     5.2 +++ b/src/FOL/ex/List.ML	Fri Oct 10 15:52:12 1997 +0200
     5.3 @@ -8,7 +8,7 @@
     5.4  
     5.5  open List;
     5.6  
     5.7 -val prems = goal List.thy "[| P([]);  !!x l. P(x.l) |] ==> All(P)";
     5.8 +val prems = goal List.thy "[| P([]);  !!x l. P(x. l) |] ==> All(P)";
     5.9  by (rtac list_ind 1);
    5.10  by (REPEAT (resolve_tac (prems@[allI,impI]) 1));
    5.11  qed "list_exh";
    5.12 @@ -37,7 +37,7 @@
    5.13  by (IND_TAC list_ind Simp_tac "l" 1);
    5.14  qed "forall_app";
    5.15  
    5.16 -goal List.thy "forall(l,%x.P(x)&Q(x)) <-> forall(l,P) & forall(l,Q)";
    5.17 +goal List.thy "forall(l,%x. P(x)&Q(x)) <-> forall(l,P) & forall(l,Q)";
    5.18  by (IND_TAC list_ind Simp_tac "l" 1);
    5.19  by (Fast_tac 1);
    5.20  qed "forall_conj";
    5.21 @@ -59,7 +59,7 @@
    5.22  by (ALL_IND_TAC nat_exh Asm_simp_tac 1);
    5.23  qed "at_app1";
    5.24  
    5.25 -goal List.thy "at(l1++(x.l2), len(l1)) = x";
    5.26 +goal List.thy "at(l1++(x. l2), len(l1)) = x";
    5.27  by (IND_TAC list_ind Simp_tac "l1" 1);
    5.28  qed "at_app_hd2";
    5.29  
     6.1 --- a/src/FOL/ex/List.thy	Fri Oct 10 15:51:38 1997 +0200
     6.2 +++ b/src/FOL/ex/List.thy	Fri Oct 10 15:52:12 1997 +0200
     6.3 @@ -22,28 +22,28 @@
     6.4     "++"         :: ['a list, 'a list] => 'a list     (infixr 70)
     6.5  
     6.6  rules
     6.7 - list_ind "[| P([]);  ALL x l. P(l)-->P(x.l) |] ==> All(P)"
     6.8 + list_ind "[| P([]);  ALL x l. P(l)-->P(x. l) |] ==> All(P)"
     6.9  
    6.10   forall_cong 
    6.11    "[| l = l';  !!x. P(x)<->P'(x) |] ==> forall(l,P) <-> forall(l',P')"
    6.12  
    6.13 - list_distinct1 "~[] = x.l"
    6.14 - list_distinct2 "~x.l = []"
    6.15 + list_distinct1 "~[] = x. l"
    6.16 + list_distinct2 "~x. l = []"
    6.17  
    6.18 - list_free      "x.l = x'.l' <-> x=x' & l=l'"
    6.19 + list_free      "x. l = x'. l' <-> x=x' & l=l'"
    6.20  
    6.21   app_nil        "[]++l = l"
    6.22 - app_cons       "(x.l)++l' = x.(l++l')"
    6.23 - tl_eq  "tl(m.q) = q"
    6.24 - hd_eq  "hd(m.q) = m"
    6.25 + app_cons       "(x. l)++l' = x.(l++l')"
    6.26 + tl_eq  "tl(m. q) = q"
    6.27 + hd_eq  "hd(m. q) = m"
    6.28  
    6.29   forall_nil "forall([],P)"
    6.30 - forall_cons "forall(x.l,P) <-> P(x) & forall(l,P)"
    6.31 + forall_cons "forall(x. l,P) <-> P(x) & forall(l,P)"
    6.32  
    6.33   len_nil "len([]) = 0"
    6.34 - len_cons "len(m.q) = succ(len(q))"
    6.35 + len_cons "len(m. q) = succ(len(q))"
    6.36  
    6.37 - at_0 "at(m.q,0) = m"
    6.38 - at_succ "at(m.q,succ(n)) = at(q,n)"
    6.39 + at_0 "at(m. q,0) = m"
    6.40 + at_succ "at(m. q,succ(n)) = at(q,n)"
    6.41  
    6.42  end
     7.1 --- a/src/FOL/ex/cla.ML	Fri Oct 10 15:51:38 1997 +0200
     7.2 +++ b/src/FOL/ex/cla.ML	Fri Oct 10 15:52:12 1997 +0200
     7.3 @@ -127,22 +127,22 @@
     7.4  by (Blast_tac 1);
     7.5  result(); 
     7.6  
     7.7 -goal FOL.thy "(EX x. P-->Q(x))  <->  (P --> (EX x.Q(x)))";
     7.8 +goal FOL.thy "(EX x. P-->Q(x))  <->  (P --> (EX x. Q(x)))";
     7.9  by (Blast_tac 1);
    7.10  result(); 
    7.11  
    7.12 -goal FOL.thy "(EX x.P(x)-->Q)  <->  (ALL x.P(x)) --> Q";
    7.13 +goal FOL.thy "(EX x. P(x)-->Q)  <->  (ALL x. P(x)) --> Q";
    7.14  by (Blast_tac 1);
    7.15  result(); 
    7.16  
    7.17 -goal FOL.thy "(ALL x.P(x)) | Q  <->  (ALL x. P(x) | Q)";
    7.18 +goal FOL.thy "(ALL x. P(x)) | Q  <->  (ALL x. P(x) | Q)";
    7.19  by (Blast_tac 1);
    7.20  result(); 
    7.21  
    7.22  (*Discussed in Avron, Gentzen-Type Systems, Resolution and Tableaux,
    7.23    JAR 10 (265-281), 1993.  Proof is trivial!*)
    7.24  goal FOL.thy
    7.25 -    "~ ((EX x.~P(x)) & ((EX x.P(x)) | (EX x.P(x) & Q(x))) & ~ (EX x.P(x)))";
    7.26 +    "~ ((EX x.~P(x)) & ((EX x. P(x)) | (EX x. P(x) & Q(x))) & ~ (EX x. P(x)))";
    7.27  by (Blast_tac 1);
    7.28  result();
    7.29  
    7.30 @@ -207,7 +207,7 @@
    7.31  
    7.32  writeln"Problem 24";
    7.33  goal FOL.thy "~(EX x. S(x)&Q(x)) & (ALL x. P(x) --> Q(x)|R(x)) &  \
    7.34 -\    (~(EX x.P(x)) --> (EX x.Q(x))) & (ALL x. Q(x)|R(x) --> S(x))  \
    7.35 +\    (~(EX x. P(x)) --> (EX x. Q(x))) & (ALL x. Q(x)|R(x) --> S(x))  \
    7.36  \   --> (EX x. P(x)&R(x))";
    7.37  by (Blast_tac 1); 
    7.38  result();
    7.39 @@ -240,7 +240,7 @@
    7.40  writeln"Problem 28.  AMENDED";
    7.41  goal FOL.thy "(ALL x. P(x) --> (ALL x. Q(x))) &   \
    7.42  \       ((ALL x. Q(x)|R(x)) --> (EX x. Q(x)&S(x))) &  \
    7.43 -\       ((EX x.S(x)) --> (ALL x. L(x) --> M(x)))  \
    7.44 +\       ((EX x. S(x)) --> (ALL x. L(x) --> M(x)))  \
    7.45  \   --> (ALL x. P(x) & L(x) --> M(x))";
    7.46  by (Blast_tac 1);  
    7.47  result();
    7.48 @@ -260,7 +260,7 @@
    7.49  result();
    7.50  
    7.51  writeln"Problem 31";
    7.52 -goal FOL.thy "~(EX x.P(x) & (Q(x) | R(x))) & \
    7.53 +goal FOL.thy "~(EX x. P(x) & (Q(x) | R(x))) & \
    7.54  \       (EX x. L(x) & P(x)) & \
    7.55  \       (ALL x. ~ R(x) --> M(x))  \
    7.56  \   --> (EX x. L(x) & M(x))";
    7.57 @@ -306,7 +306,7 @@
    7.58  
    7.59  writeln"Problem 37";
    7.60  goal FOL.thy "(ALL z. EX w. ALL x. EX y. \
    7.61 -\          (P(x,z)-->P(y,w)) & P(y,z) & (P(y,w) --> (EX u.Q(u,w)))) & \
    7.62 +\          (P(x,z)-->P(y,w)) & P(y,z) & (P(y,w) --> (EX u. Q(u,w)))) & \
    7.63  \       (ALL x z. ~P(x,z) --> (EX y. Q(y,z))) & \
    7.64  \       ((EX x y. Q(x,y)) --> (ALL x. R(x,x)))  \
    7.65  \   --> (ALL x. EX y. R(x,y))";
    7.66 @@ -385,7 +385,7 @@
    7.67  (*Hard because it involves substitution for Vars;
    7.68    the type constraint ensures that x,y,z have the same type as a,b,u. *)
    7.69  goal FOL.thy "(EX x y::'a. ALL z. z=x | z=y) & P(a) & P(b) & a~=b \
    7.70 -\               --> (ALL u::'a.P(u))";
    7.71 +\               --> (ALL u::'a. P(u))";
    7.72  by Safe_tac;
    7.73  by (res_inst_tac [("x","a")] allE 1);
    7.74  by (assume_tac 1);
    7.75 @@ -396,7 +396,7 @@
    7.76  
    7.77  writeln"Problem 50";  
    7.78  (*What has this to do with equality?*)
    7.79 -goal FOL.thy "(ALL x. P(a,x) | (ALL y.P(x,y))) --> (EX x. ALL y.P(x,y))";
    7.80 +goal FOL.thy "(ALL x. P(a,x) | (ALL y. P(x,y))) --> (EX x. ALL y. P(x,y))";
    7.81  by (Blast_tac 1);
    7.82  result();
    7.83  
     8.1 --- a/src/FOL/ex/foundn.ML	Fri Oct 10 15:51:38 1997 +0200
     8.2 +++ b/src/FOL/ex/foundn.ML	Fri Oct 10 15:52:12 1997 +0200
     8.3 @@ -99,7 +99,7 @@
     8.4  
     8.5  
     8.6  (*Parallel lifting example. *)
     8.7 -goal IFOL.thy "EX u.ALL x.EX v.ALL y.EX w. P(u,x,v,y,w)";
     8.8 +goal IFOL.thy "EX u. ALL x. EX v. ALL y. EX w. P(u,x,v,y,w)";
     8.9  by (resolve_tac [exI, allI] 1);
    8.10  by (resolve_tac [exI, allI] 1);
    8.11  by (resolve_tac [exI, allI] 1);
    8.12 @@ -108,7 +108,7 @@
    8.13  
    8.14  
    8.15  val prems =
    8.16 -goal IFOL.thy "(EX z.F(z)) & B ==> (EX z. F(z) & B)";
    8.17 +goal IFOL.thy "(EX z. F(z)) & B ==> (EX z. F(z) & B)";
    8.18  by (rtac conjE 1);
    8.19  by (resolve_tac prems 1);
    8.20  by (rtac exE 1);
     9.1 --- a/src/FOL/ex/int.ML	Fri Oct 10 15:51:38 1997 +0200
     9.2 +++ b/src/FOL/ex/int.ML	Fri Oct 10 15:52:12 1997 +0200
     9.3 @@ -211,11 +211,11 @@
     9.4  
     9.5  writeln"The converse is classical in the following implications...";
     9.6  
     9.7 -goal IFOL.thy "(EX x.P(x)-->Q)  -->  (ALL x.P(x)) --> Q";
     9.8 +goal IFOL.thy "(EX x. P(x)-->Q)  -->  (ALL x. P(x)) --> Q";
     9.9  by (IntPr.fast_tac 1); 
    9.10  result();  
    9.11  
    9.12 -goal IFOL.thy "((ALL x.P(x))-->Q) --> ~ (ALL x. P(x) & ~Q)";
    9.13 +goal IFOL.thy "((ALL x. P(x))-->Q) --> ~ (ALL x. P(x) & ~Q)";
    9.14  by (IntPr.fast_tac 1); 
    9.15  result();  
    9.16  
    9.17 @@ -223,7 +223,7 @@
    9.18  by (IntPr.fast_tac 1); 
    9.19  result();  
    9.20  
    9.21 -goal IFOL.thy "(ALL x.P(x)) | Q  -->  (ALL x. P(x) | Q)";
    9.22 +goal IFOL.thy "(ALL x. P(x)) | Q  -->  (ALL x. P(x) | Q)";
    9.23  by (IntPr.fast_tac 1); 
    9.24  result();  
    9.25  
    9.26 @@ -237,15 +237,15 @@
    9.27  writeln"The following are not constructively valid!";
    9.28  (*The attempt to prove them terminates quickly!*)
    9.29  
    9.30 -goal IFOL.thy "((ALL x.P(x))-->Q) --> (EX x.P(x)-->Q)";
    9.31 +goal IFOL.thy "((ALL x. P(x))-->Q) --> (EX x. P(x)-->Q)";
    9.32  by (IntPr.fast_tac 1) handle ERROR => writeln"Failed, as expected";  
    9.33  getgoal 1; 
    9.34  
    9.35 -goal IFOL.thy "(P --> (EX x.Q(x))) --> (EX x. P-->Q(x))";
    9.36 +goal IFOL.thy "(P --> (EX x. Q(x))) --> (EX x. P-->Q(x))";
    9.37  by (IntPr.fast_tac 1) handle ERROR => writeln"Failed, as expected";  
    9.38  getgoal 1; 
    9.39  
    9.40 -goal IFOL.thy "(ALL x. P(x) | Q) --> ((ALL x.P(x)) | Q)";
    9.41 +goal IFOL.thy "(ALL x. P(x) | Q) --> ((ALL x. P(x)) | Q)";
    9.42  by (IntPr.fast_tac 1) handle ERROR => writeln"Failed, as expected";  
    9.43  getgoal 1; 
    9.44  
    9.45 @@ -294,7 +294,7 @@
    9.46  
    9.47  writeln"Problem 24";
    9.48  goal IFOL.thy "~(EX x. S(x)&Q(x)) & (ALL x. P(x) --> Q(x)|R(x)) &  \
    9.49 -\    (~(EX x.P(x)) --> (EX x.Q(x))) & (ALL x. Q(x)|R(x) --> S(x))  \
    9.50 +\    (~(EX x. P(x)) --> (EX x. Q(x))) & (ALL x. Q(x)|R(x) --> S(x))  \
    9.51  \   --> ~~(EX x. P(x)&R(x))";
    9.52  (*Not clear why fast_tac, best_tac, ASTAR and ITER_DEEPEN all take forever*)
    9.53  by IntPr.safe_tac; 
    9.54 @@ -330,7 +330,7 @@
    9.55  writeln"Problem ~~28.  AMENDED";
    9.56  goal IFOL.thy "(ALL x. P(x) --> (ALL x. Q(x))) &   \
    9.57  \       (~~(ALL x. Q(x)|R(x)) --> (EX x. Q(x)&S(x))) &  \
    9.58 -\       (~~(EX x.S(x)) --> (ALL x. L(x) --> M(x)))  \
    9.59 +\       (~~(EX x. S(x)) --> (ALL x. L(x) --> M(x)))  \
    9.60  \   --> (ALL x. P(x) & L(x) --> M(x))";
    9.61  by (IntPr.fast_tac 1);  (*48 secs*)
    9.62  result();
    9.63 @@ -350,7 +350,7 @@
    9.64  result();
    9.65  
    9.66  writeln"Problem 31";
    9.67 -goal IFOL.thy "~(EX x.P(x) & (Q(x) | R(x))) & \
    9.68 +goal IFOL.thy "~(EX x. P(x) & (Q(x) | R(x))) & \
    9.69  \       (EX x. L(x) & P(x)) & \
    9.70  \       (ALL x. ~ R(x) --> M(x))  \
    9.71  \   --> (EX x. L(x) & M(x))";
    9.72 @@ -384,7 +384,7 @@
    9.73  writeln"Problem 37";
    9.74  goal IFOL.thy
    9.75         "(ALL z. EX w. ALL x. EX y. \
    9.76 -\          ~~(P(x,z)-->P(y,w)) & P(y,z) & (P(y,w) --> (EX u.Q(u,w)))) & \
    9.77 +\          ~~(P(x,z)-->P(y,w)) & P(y,z) & (P(y,w) --> (EX u. Q(u,w)))) & \
    9.78  \       (ALL x z. ~P(x,z) --> (EX y. Q(y,z))) & \
    9.79  \       (~~(EX x y. Q(x,y)) --> (ALL x. R(x,x)))  \
    9.80  \   --> ~~(ALL x. EX y. R(x,y))";
    10.1 --- a/src/FOL/ex/intro.ML	Fri Oct 10 15:51:38 1997 +0200
    10.2 +++ b/src/FOL/ex/intro.ML	Fri Oct 10 15:52:12 1997 +0200
    10.3 @@ -32,7 +32,7 @@
    10.4  result();
    10.5  
    10.6  (*Correct version, delaying use of "spec" until last*)
    10.7 -goal FOL.thy "(ALL x y.P(x,y))  -->  (ALL z w.P(w,z))";
    10.8 +goal FOL.thy "(ALL x y. P(x,y))  -->  (ALL z w. P(w,z))";
    10.9  by (rtac impI 1);
   10.10  by (rtac allI 1);
   10.11  by (rtac allI 1);
    11.1 --- a/src/FOL/ex/mini.ML	Fri Oct 10 15:51:38 1997 +0200
    11.2 +++ b/src/FOL/ex/mini.ML	Fri Oct 10 15:52:12 1997 +0200
    11.3 @@ -26,8 +26,8 @@
    11.4                    ["~(P&Q) <-> ~P | ~Q",
    11.5                     "~(P|Q) <-> ~P & ~Q",
    11.6                     "~~P <-> P",
    11.7 -                   "~(ALL x.P(x)) <-> (EX x. ~P(x))",
    11.8 -                   "~(EX x.P(x)) <-> (ALL x. ~P(x))"];
    11.9 +                   "~(ALL x. P(x)) <-> (EX x. ~P(x))",
   11.10 +                   "~(EX x. P(x)) <-> (ALL x. ~P(x))"];
   11.11  
   11.12  (*** Removal of --> and <-> (positive and negative occurrences) ***)
   11.13  (*Last one is important for computing a compact CNF*)
   11.14 @@ -43,21 +43,21 @@
   11.15  
   11.16  val ex_simps = map prove_fun 
   11.17                  ["(EX x. P) <-> P",
   11.18 -                 "(EX x. P(x) & Q) <-> (EX x.P(x)) & Q",
   11.19 -                 "(EX x. P & Q(x)) <-> P & (EX x.Q(x))",
   11.20 -                 "(EX x. P(x) | Q(x)) <-> (EX x.P(x)) | (EX x.Q(x))",
   11.21 -                 "(EX x. P(x) | Q) <-> (EX x.P(x)) | Q",
   11.22 -                 "(EX x. P | Q(x)) <-> P | (EX x.Q(x))"];
   11.23 +                 "(EX x. P(x) & Q) <-> (EX x. P(x)) & Q",
   11.24 +                 "(EX x. P & Q(x)) <-> P & (EX x. Q(x))",
   11.25 +                 "(EX x. P(x) | Q(x)) <-> (EX x. P(x)) | (EX x. Q(x))",
   11.26 +                 "(EX x. P(x) | Q) <-> (EX x. P(x)) | Q",
   11.27 +                 "(EX x. P | Q(x)) <-> P | (EX x. Q(x))"];
   11.28  
   11.29  (*** Pushing in the universal quantifiers ***)
   11.30  
   11.31  val all_simps = map prove_fun
   11.32                  ["(ALL x. P) <-> P",
   11.33 -                 "(ALL x. P(x) & Q(x)) <-> (ALL x.P(x)) & (ALL x.Q(x))",
   11.34 -                 "(ALL x. P(x) & Q) <-> (ALL x.P(x)) & Q",
   11.35 -                 "(ALL x. P & Q(x)) <-> P & (ALL x.Q(x))",
   11.36 -                 "(ALL x. P(x) | Q) <-> (ALL x.P(x)) | Q",
   11.37 -                 "(ALL x. P | Q(x)) <-> P | (ALL x.Q(x))"];
   11.38 +                 "(ALL x. P(x) & Q(x)) <-> (ALL x. P(x)) & (ALL x. Q(x))",
   11.39 +                 "(ALL x. P(x) & Q) <-> (ALL x. P(x)) & Q",
   11.40 +                 "(ALL x. P & Q(x)) <-> P & (ALL x. Q(x))",
   11.41 +                 "(ALL x. P(x) | Q) <-> (ALL x. P(x)) | Q",
   11.42 +                 "(ALL x. P | Q(x)) <-> P | (ALL x. Q(x))"];
   11.43  
   11.44  
   11.45  val mini_ss=FOL_basic_ss addsimps (demorgans @ nnf_simps @ ex_simps @ all_simps);
    12.1 --- a/src/FOL/ex/quant.ML	Fri Oct 10 15:51:38 1997 +0200
    12.2 +++ b/src/FOL/ex/quant.ML	Fri Oct 10 15:52:12 1997 +0200
    12.3 @@ -9,40 +9,40 @@
    12.4  
    12.5  writeln"File FOL/ex/quant.";
    12.6  
    12.7 -goal thy "(ALL x y.P(x,y))  -->  (ALL y x.P(x,y))";
    12.8 +goal thy "(ALL x y. P(x,y))  -->  (ALL y x. P(x,y))";
    12.9  by tac;
   12.10  result();  
   12.11  
   12.12  
   12.13 -goal thy "(EX x y.P(x,y)) --> (EX y x.P(x,y))";
   12.14 +goal thy "(EX x y. P(x,y)) --> (EX y x. P(x,y))";
   12.15  by tac;
   12.16  result();  
   12.17  
   12.18  
   12.19  (*Converse is false*)
   12.20 -goal thy "(ALL x.P(x)) | (ALL x.Q(x)) --> (ALL x. P(x) | Q(x))";
   12.21 +goal thy "(ALL x. P(x)) | (ALL x. Q(x)) --> (ALL x. P(x) | Q(x))";
   12.22  by tac;
   12.23  result();  
   12.24  
   12.25 -goal thy "(ALL x. P-->Q(x))  <->  (P--> (ALL x.Q(x)))";
   12.26 +goal thy "(ALL x. P-->Q(x))  <->  (P--> (ALL x. Q(x)))";
   12.27  by tac;
   12.28  result();  
   12.29  
   12.30  
   12.31 -goal thy "(ALL x.P(x)-->Q)  <->  ((EX x.P(x)) --> Q)";
   12.32 +goal thy "(ALL x. P(x)-->Q)  <->  ((EX x. P(x)) --> Q)";
   12.33  by tac;
   12.34  result();  
   12.35  
   12.36  
   12.37  writeln"Some harder ones";
   12.38  
   12.39 -goal thy "(EX x. P(x) | Q(x)) <-> (EX x.P(x)) | (EX x.Q(x))";
   12.40 +goal thy "(EX x. P(x) | Q(x)) <-> (EX x. P(x)) | (EX x. Q(x))";
   12.41  by tac;
   12.42  result();  
   12.43  (*6 secs*)
   12.44  
   12.45  (*Converse is false*)
   12.46 -goal thy "(EX x. P(x)&Q(x)) --> (EX x.P(x))  &  (EX x.Q(x))";
   12.47 +goal thy "(EX x. P(x)&Q(x)) --> (EX x. P(x))  &  (EX x. Q(x))";
   12.48  by tac;
   12.49  result();  
   12.50  
   12.51 @@ -70,26 +70,26 @@
   12.52  by tac handle ERROR => writeln"Failed, as expected";  
   12.53  getgoal 1; 
   12.54  
   12.55 -goal thy "P(?a) --> (ALL x.P(x))";
   12.56 +goal thy "P(?a) --> (ALL x. P(x))";
   12.57  by tac handle ERROR => writeln"Failed, as expected";
   12.58  (*Check that subgoals remain: proof failed.*)
   12.59  getgoal 1;  
   12.60  
   12.61  goal thy
   12.62 -    "(P(?a) --> (ALL x.Q(x))) --> (ALL x. P(x) --> Q(x))";
   12.63 +    "(P(?a) --> (ALL x. Q(x))) --> (ALL x. P(x) --> Q(x))";
   12.64  by tac handle ERROR => writeln"Failed, as expected";
   12.65  getgoal 1;  
   12.66  
   12.67  
   12.68  writeln"Back to things that are provable...";
   12.69  
   12.70 -goal thy "(ALL x.P(x)-->Q(x)) & (EX x.P(x)) --> (EX x.Q(x))";
   12.71 +goal thy "(ALL x. P(x)-->Q(x)) & (EX x. P(x)) --> (EX x. Q(x))";
   12.72  by tac;  
   12.73  result();  
   12.74  
   12.75  
   12.76  (*An example of why exI should be delayed as long as possible*)
   12.77 -goal thy "(P --> (EX x.Q(x))) & P --> (EX x.Q(x))";
   12.78 +goal thy "(P --> (EX x. Q(x))) & P --> (EX x. Q(x))";
   12.79  by tac;  
   12.80  result();  
   12.81  
    13.1 --- a/src/FOL/simpdata.ML	Fri Oct 10 15:51:38 1997 +0200
    13.2 +++ b/src/FOL/simpdata.ML	Fri Oct 10 15:52:12 1997 +0200
    13.3 @@ -42,7 +42,7 @@
    13.4    "(False <-> P) <-> ~P",       "(P <-> False) <-> ~P"];
    13.5  
    13.6  val quant_simps = map int_prove_fun
    13.7 - ["(ALL x.P) <-> P",    "(EX x.P) <-> P"];
    13.8 + ["(ALL x. P) <-> P",    "(EX x. P) <-> P"];
    13.9  
   13.10  (*These are NOT supplied by default!*)
   13.11  val distrib_simps  = map int_prove_fun
   13.12 @@ -103,23 +103,23 @@
   13.13  val ex_simps = map prove_fun 
   13.14                  ["(EX x. x=t & P(x)) <-> P(t)",
   13.15                   "(EX x. t=x & P(x)) <-> P(t)",
   13.16 -                 "(EX x. P(x) & Q) <-> (EX x.P(x)) & Q",
   13.17 -                 "(EX x. P & Q(x)) <-> P & (EX x.Q(x))",
   13.18 -                 "(EX x. P(x) | Q) <-> (EX x.P(x)) | Q",
   13.19 -                 "(EX x. P | Q(x)) <-> P | (EX x.Q(x))",
   13.20 -                 "(EX x. P(x) --> Q) <-> (ALL x.P(x)) --> Q",
   13.21 -                 "(EX x. P --> Q(x)) <-> P --> (EX x.Q(x))"];
   13.22 +                 "(EX x. P(x) & Q) <-> (EX x. P(x)) & Q",
   13.23 +                 "(EX x. P & Q(x)) <-> P & (EX x. Q(x))",
   13.24 +                 "(EX x. P(x) | Q) <-> (EX x. P(x)) | Q",
   13.25 +                 "(EX x. P | Q(x)) <-> P | (EX x. Q(x))",
   13.26 +                 "(EX x. P(x) --> Q) <-> (ALL x. P(x)) --> Q",
   13.27 +                 "(EX x. P --> Q(x)) <-> P --> (EX x. Q(x))"];
   13.28  
   13.29  (*Miniscoping: pushing in universal quantifiers*)
   13.30  val all_simps = map prove_fun
   13.31                  ["(ALL x. x=t --> P(x)) <-> P(t)",
   13.32                   "(ALL x. t=x --> P(x)) <-> P(t)",
   13.33 -                 "(ALL x. P(x) & Q) <-> (ALL x.P(x)) & Q",
   13.34 -                 "(ALL x. P & Q(x)) <-> P & (ALL x.Q(x))",
   13.35 -                 "(ALL x. P(x) | Q) <-> (ALL x.P(x)) | Q",
   13.36 -                 "(ALL x. P | Q(x)) <-> P | (ALL x.Q(x))",
   13.37 -                 "(ALL x. P(x) --> Q) <-> (EX x.P(x)) --> Q",
   13.38 -                 "(ALL x. P --> Q(x)) <-> P --> (ALL x.Q(x))"];
   13.39 +                 "(ALL x. P(x) & Q) <-> (ALL x. P(x)) & Q",
   13.40 +                 "(ALL x. P & Q(x)) <-> P & (ALL x. Q(x))",
   13.41 +                 "(ALL x. P(x) | Q) <-> (ALL x. P(x)) | Q",
   13.42 +                 "(ALL x. P | Q(x)) <-> P | (ALL x. Q(x))",
   13.43 +                 "(ALL x. P(x) --> Q) <-> (EX x. P(x)) --> Q",
   13.44 +                 "(ALL x. P --> Q(x)) <-> P --> (ALL x. Q(x))"];
   13.45  
   13.46  fun int_prove nm thm  = qed_goal nm IFOL.thy thm
   13.47      (fn prems => [ (cut_facts_tac prems 1), 
   13.48 @@ -150,9 +150,9 @@
   13.49  
   13.50  prove     "not_iff" "~(P <-> Q) <-> (P <-> ~Q)";
   13.51  
   13.52 -prove     "not_all" "(~ (ALL x.P(x))) <-> (EX x.~P(x))";
   13.53 -prove     "imp_all" "((ALL x.P(x)) --> Q) <-> (EX x.P(x) --> Q)";
   13.54 -int_prove "not_ex"  "(~ (EX x.P(x))) <-> (ALL x.~P(x))";
   13.55 +prove     "not_all" "(~ (ALL x. P(x))) <-> (EX x.~P(x))";
   13.56 +prove     "imp_all" "((ALL x. P(x)) --> Q) <-> (EX x. P(x) --> Q)";
   13.57 +int_prove "not_ex"  "(~ (EX x. P(x))) <-> (ALL x.~P(x))";
   13.58  int_prove "imp_ex" "((EX x. P(x)) --> Q) <-> (ALL x. P(x) --> Q)";
   13.59  
   13.60  int_prove "ex_disj_distrib"
    14.1 --- a/src/Provers/splitter.ML	Fri Oct 10 15:51:38 1997 +0200
    14.2 +++ b/src/Provers/splitter.ML	Fri Oct 10 15:52:12 1997 +0200
    14.3 @@ -32,7 +32,7 @@
    14.4  val lift =
    14.5    let val ct = read_cterm (#sign(rep_thm iffD))
    14.6             ("[| !!x::'b::logic. Q(x) == R(x) |] ==> \
    14.7 -            \P(%x.Q(x)) == P(%x.R(x))::'a::logic",propT)
    14.8 +            \P(%x. Q(x)) == P(%x. R(x))::'a::logic",propT)
    14.9    in prove_goalw_cterm [] ct
   14.10       (fn [prem] => [rewtac prem, rtac reflexive_thm 1])
   14.11    end;