src/CCL/ex/Stream.ML

 
 (*** Map of composition is composition of maps ***)
 
 val prems = goal Stream.thy "l:Lists(A) ==> map(f o g,l) = map(f,map(g,l))";
 by (eq_coinduct3_tac 
-       "{p. EX x y.p=<x,y> & (EX l:Lists(A).x=map(f o g,l) & y=map(f,map(g,l)))}"  1);
+       "{p. EX x y. p=<x,y> & (EX l:Lists(A).x=map(f o g,l) & y=map(f,map(g,l)))}"  1);
 by (fast_tac (ccl_cs addSIs prems) 1);
 by (safe_tac type_cs);
 by (etac (XH_to_E ListsXH) 1);
 by (EQgen_tac list_ss [] 1);
 by (simp_tac list_ss 1);
 by (fast_tac ccl_cs 1);
 qed "map_comp";
 
 (*** Mapping the identity function leaves a list unchanged ***)
 
-val prems = goal Stream.thy "l:Lists(A) ==> map(%x.x,l) = l";
+val prems = goal Stream.thy "l:Lists(A) ==> map(%x. x,l) = l";
 by (eq_coinduct3_tac 
-       "{p. EX x y.p=<x,y> & (EX l:Lists(A).x=map(%x.x,l) & y=l)}"  1);
+       "{p. EX x y. p=<x,y> & (EX l:Lists(A).x=map(%x. x,l) & y=l)}"  1);
 by (fast_tac (ccl_cs addSIs prems) 1);
 by (safe_tac type_cs);
 by (etac (XH_to_E ListsXH) 1);
 by (EQgen_tac list_ss [] 1);
 by (fast_tac ccl_cs 1);

 
 (*** Mapping distributes over append ***)
 
 val prems = goal Stream.thy 
         "[| l:Lists(A); m:Lists(A) |] ==> map(f,l@m) = map(f,l) @ map(f,m)";
-by (eq_coinduct3_tac "{p. EX x y.p=<x,y> & (EX l:Lists(A).EX m:Lists(A). \
+by (eq_coinduct3_tac "{p. EX x y. p=<x,y> & (EX l:Lists(A).EX m:Lists(A). \
 \                                           x=map(f,l@m) & y=map(f,l) @ map(f,m))}"  1);
 by (fast_tac (ccl_cs addSIs prems) 1);
 by (safe_tac type_cs);
 by (etac (XH_to_E ListsXH) 1);
 by (EQgen_tac list_ss [] 1);

 (*** Append is associative ***)
 
 val prems = goal Stream.thy 
         "[| k:Lists(A); l:Lists(A); m:Lists(A) |] ==> k @ l @ m = (k @ l) @ m";
 by (eq_coinduct3_tac 
-    "{p. EX x y.p=<x,y> & (EX k:Lists(A).EX l:Lists(A).EX m:Lists(A). \
+    "{p. EX x y. p=<x,y> & (EX k:Lists(A).EX l:Lists(A).EX m:Lists(A). \
 \                          x=k @ l @ m & y=(k @ l) @ m)}"  1);
 by (fast_tac (ccl_cs addSIs prems) 1);
 by (safe_tac type_cs);
 by (etac (XH_to_E ListsXH) 1);
 by (EQgen_tac list_ss [] 1);

 
 (*** Appending anything to an infinite list doesn't alter it ****)
 
 val prems = goal Stream.thy "l:ILists(A) ==> l @ m = l";
 by (eq_coinduct3_tac
-    "{p. EX x y.p=<x,y> & (EX l:ILists(A).EX m.x=l@m & y=l)}" 1);
+    "{p. EX x y. p=<x,y> & (EX l:ILists(A).EX m. x=l@m & y=l)}" 1);
 by (fast_tac (ccl_cs addSIs prems) 1);
 by (safe_tac set_cs);
 by (etac (XH_to_E IListsXH) 1);
 by (EQgen_tac list_ss [] 1);
 by (fast_tac ccl_cs 1);

 by (simp_tac (list_ss addsimps [prem RS nmapBcons]) 1);
 qed "iter2Blemma";
 
 goal Stream.thy "iter1(f,a) = iter2(f,a)";
 by (eq_coinduct3_tac 
-    "{p. EX x y.p=<x,y> & (EX n:Nat.x=iter1(f,f^n`a) & y=map(f)^n`iter2(f,a))}"
+    "{p. EX x y. p=<x,y> & (EX n:Nat. x=iter1(f,f^n`a) & y=map(f)^n`iter2(f,a))}"
     1);
 by (fast_tac (type_cs addSIs [napplyBzero RS sym,
                               napplyBzero RS sym RS arg_cong]) 1);
 by (EQgen_tac list_ss [iter1B,iter2Blemma] 1);
 by (stac napply_f 1 THEN atac 1);