Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/CCL/ex/Stream.ML
changeset 17456 bcf7544875b2
parent 5062 fbdb0b541314 
--- a/src/CCL/ex/Stream.ML	Sat Sep 17 14:02:31 2005 +0200
+++ b/src/CCL/ex/Stream.ML	Sat Sep 17 17:35:26 2005 +0200
@@ -1,21 +1,17 @@
-(*  Title:      CCL/ex/stream
+(*  Title:      CCL/ex/Stream.ML
     ID:         $Id$
     Author:     Martin Coen, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
 
-For stream.thy.
-
 Proving properties about infinite lists using coinduction:
     Lists(A)  is the set of all finite and infinite lists of elements of A.
     ILists(A) is the set of infinite lists of elements of A.
 *)
 
-open Stream;
-
 (*** 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 
+val prems = goal (the_context ()) "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);
 by (fast_tac (ccl_cs addSIs prems) 1);
 by (safe_tac type_cs);
@@ -27,8 +23,8 @@
 
 (*** Mapping the identity function leaves a list unchanged ***)
 
-val prems = goal Stream.thy "l:Lists(A) ==> map(%x. x,l) = l";
-by (eq_coinduct3_tac 
+val prems = goal (the_context ()) "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);
 by (fast_tac (ccl_cs addSIs prems) 1);
 by (safe_tac type_cs);
@@ -39,7 +35,7 @@
 
 (*** Mapping distributes over append ***)
 
-val prems = goal Stream.thy 
+val prems = goal (the_context ())
         "[| 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). \
 \                                           x=map(f,l@m) & y=map(f,l) @ map(f,m))}"  1);
@@ -54,9 +50,9 @@
 
 (*** Append is associative ***)
 
-val prems = goal Stream.thy 
+val prems = goal (the_context ())
         "[| k:Lists(A); l:Lists(A); m:Lists(A) |] ==> k @ l @ m = (k @ l) @ m";
-by (eq_coinduct3_tac 
+by (eq_coinduct3_tac
     "{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);
@@ -69,7 +65,7 @@
 
 (*** Appending anything to an infinite list doesn't alter it ****)
 
-val prems = goal Stream.thy "l:ILists(A) ==> l @ m = l";
+val prems = goal (the_context ()) "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);
 by (fast_tac (ccl_cs addSIs prems) 1);
@@ -94,7 +90,7 @@
 by (rtac refl 1);
 qed "iter2B";
 
-val [prem] =goal Stream.thy
+val [prem] =goal (the_context ())
    "n:Nat ==> \
 \   map(f) ^ n ` iter2(f,a) = (f ^ n ` a) $ (map(f) ^ n ` map(f,iter2(f,a)))";
 by (res_inst_tac [("P", "%x. ?lhs(x) = ?rhs")] (iter2B RS ssubst) 1);
@@ -102,7 +98,7 @@
 qed "iter2Blemma";
 
 Goal "iter1(f,a) = iter2(f,a)";
-by (eq_coinduct3_tac 
+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))}"
     1);
 by (fast_tac (type_cs addSIs [napplyBzero RS sym,
isabelle