src/CCL/ex/stream.ML
 author clasohm Thu Sep 16 12:20:38 1993 +0200 (1993-09-16) changeset 0 a5a9c433f639 child 8 c3d2c6dcf3f0 permissions -rw-r--r--
Initial revision
 clasohm@0 ` 1` ```(* Title: CCL/ex/stream ``` clasohm@0 ` 2` ``` ID: \$Id\$ ``` clasohm@0 ` 3` ``` Author: Martin Coen, Cambridge University Computer Laboratory ``` clasohm@0 ` 4` ``` Copyright 1993 University of Cambridge ``` clasohm@0 ` 5` clasohm@0 ` 6` ```For stream.thy. ``` clasohm@0 ` 7` clasohm@0 ` 8` ```Proving properties about infinite lists using coinduction: ``` clasohm@0 ` 9` ``` Lists(A) is the set of all finite and infinite lists of elements of A. ``` clasohm@0 ` 10` ``` ILists(A) is the set of infinite lists of elements of A. ``` clasohm@0 ` 11` ```*) ``` clasohm@0 ` 12` clasohm@0 ` 13` ```open Stream; ``` clasohm@0 ` 14` clasohm@0 ` 15` ```(*** Map of composition is composition of maps ***) ``` clasohm@0 ` 16` clasohm@0 ` 17` ```val prems = goal Stream.thy "l:Lists(A) ==> map(f o g,l) = map(f,map(g,l))"; ``` clasohm@0 ` 18` ```by (eq_coinduct3_tac ``` clasohm@0 ` 19` ``` "{p. EX x y.p= & (EX l:Lists(A).x=map(f o g,l) & y=map(f,map(g,l)))}" 1); ``` clasohm@0 ` 20` ```by (fast_tac (ccl_cs addSIs prems) 1); ``` clasohm@0 ` 21` ```by (safe_tac type_cs); ``` clasohm@0 ` 22` ```be (XH_to_E ListsXH) 1; ``` clasohm@0 ` 23` ```by (EQgen_tac list_ss [] 1); ``` clasohm@0 ` 24` ```by (SIMP_TAC list_ss 1); ``` clasohm@0 ` 25` ```by (fast_tac ccl_cs 1); ``` clasohm@0 ` 26` ```val map_comp = result(); ``` clasohm@0 ` 27` clasohm@0 ` 28` ```(*** Mapping the identity function leaves a list unchanged ***) ``` clasohm@0 ` 29` clasohm@0 ` 30` ```val prems = goal Stream.thy "l:Lists(A) ==> map(%x.x,l) = l"; ``` clasohm@0 ` 31` ```by (eq_coinduct3_tac ``` clasohm@0 ` 32` ``` "{p. EX x y.p= & (EX l:Lists(A).x=map(%x.x,l) & y=l)}" 1); ``` clasohm@0 ` 33` ```by (fast_tac (ccl_cs addSIs prems) 1); ``` clasohm@0 ` 34` ```by (safe_tac type_cs); ``` clasohm@0 ` 35` ```be (XH_to_E ListsXH) 1; ``` clasohm@0 ` 36` ```by (EQgen_tac list_ss [] 1); ``` clasohm@0 ` 37` ```by (fast_tac ccl_cs 1); ``` clasohm@0 ` 38` ```val map_id = result(); ``` clasohm@0 ` 39` clasohm@0 ` 40` ```(*** Mapping distributes over append ***) ``` clasohm@0 ` 41` clasohm@0 ` 42` ```val prems = goal Stream.thy ``` clasohm@0 ` 43` ``` "[| l:Lists(A); m:Lists(A) |] ==> map(f,l@m) = map(f,l) @ map(f,m)"; ``` clasohm@0 ` 44` ```by (eq_coinduct3_tac "{p. EX x y.p= & (EX l:Lists(A).EX m:Lists(A). \ ``` clasohm@0 ` 45` ```\ x=map(f,l@m) & y=map(f,l) @ map(f,m))}" 1); ``` clasohm@0 ` 46` ```by (fast_tac (ccl_cs addSIs prems) 1); ``` clasohm@0 ` 47` ```by (safe_tac type_cs); ``` clasohm@0 ` 48` ```be (XH_to_E ListsXH) 1; ``` clasohm@0 ` 49` ```by (EQgen_tac list_ss [] 1); ``` clasohm@0 ` 50` ```be (XH_to_E ListsXH) 1; ``` clasohm@0 ` 51` ```by (EQgen_tac list_ss [] 1); ``` clasohm@0 ` 52` ```by (fast_tac ccl_cs 1); ``` clasohm@0 ` 53` ```val map_append = result(); ``` clasohm@0 ` 54` clasohm@0 ` 55` ```(*** Append is associative ***) ``` clasohm@0 ` 56` clasohm@0 ` 57` ```val prems = goal Stream.thy ``` clasohm@0 ` 58` ``` "[| k:Lists(A); l:Lists(A); m:Lists(A) |] ==> k @ l @ m = (k @ l) @ m"; ``` clasohm@0 ` 59` ```by (eq_coinduct3_tac "{p. EX x y.p= & (EX k:Lists(A).EX l:Lists(A).EX m:Lists(A). \ ``` clasohm@0 ` 60` ```\ x=k @ l @ m & y=(k @ l) @ m)}" 1); ``` clasohm@0 ` 61` ```by (fast_tac (ccl_cs addSIs prems) 1); ``` clasohm@0 ` 62` ```by (safe_tac type_cs); ``` clasohm@0 ` 63` ```be (XH_to_E ListsXH) 1; ``` clasohm@0 ` 64` ```by (EQgen_tac list_ss [] 1); ``` clasohm@0 ` 65` ```be (XH_to_E ListsXH) 1;back(); ``` clasohm@0 ` 66` ```by (EQgen_tac list_ss [] 1); ``` clasohm@0 ` 67` ```be (XH_to_E ListsXH) 1; ``` clasohm@0 ` 68` ```by (EQgen_tac list_ss [] 1); ``` clasohm@0 ` 69` ```by (fast_tac ccl_cs 1); ``` clasohm@0 ` 70` ```val append_assoc = result(); ``` clasohm@0 ` 71` clasohm@0 ` 72` ```(*** Appending anything to an infinite list doesn't alter it ****) ``` clasohm@0 ` 73` clasohm@0 ` 74` ```val prems = goal Stream.thy "l:ILists(A) ==> l @ m = l"; ``` clasohm@0 ` 75` ```by (eq_coinduct3_tac "{p. EX x y.p= & (EX l:ILists(A).EX m.x=l@m & y=l)}" 1); ``` clasohm@0 ` 76` ```by (fast_tac (ccl_cs addSIs prems) 1); ``` clasohm@0 ` 77` ```by (safe_tac set_cs); ``` clasohm@0 ` 78` ```be (XH_to_E IListsXH) 1; ``` clasohm@0 ` 79` ```by (EQgen_tac list_ss [] 1); ``` clasohm@0 ` 80` ```by (fast_tac ccl_cs 1); ``` clasohm@0 ` 81` ```val ilist_append = result(); ``` clasohm@0 ` 82` clasohm@0 ` 83` ```(*** The equivalance of two versions of an iteration function ***) ``` clasohm@0 ` 84` ```(* *) ``` clasohm@0 ` 85` ```(* fun iter1(f,a) = a.iter1(f,f(a)) *) ``` clasohm@0 ` 86` ```(* fun iter2(f,a) = a.map(f,iter2(f,a)) *) ``` clasohm@0 ` 87` clasohm@0 ` 88` ```goalw Stream.thy [iter1_def] "iter1(f,a) = a.iter1(f,f(a))"; ``` clasohm@0 ` 89` ```br (letrecB RS trans) 1; ``` clasohm@0 ` 90` ```by (SIMP_TAC term_ss 1); ``` clasohm@0 ` 91` ```val iter1B = result(); ``` clasohm@0 ` 92` clasohm@0 ` 93` ```goalw Stream.thy [iter2_def] "iter2(f,a) = a . map(f,iter2(f,a))"; ``` clasohm@0 ` 94` ```br (letrecB RS trans) 1; ``` clasohm@0 ` 95` ```br refl 1; ``` clasohm@0 ` 96` ```val iter2B = result(); ``` clasohm@0 ` 97` clasohm@0 ` 98` ```val [prem] =goal Stream.thy ``` clasohm@0 ` 99` ``` "n:Nat ==> map(f) ^ n ` iter2(f,a) = f ^ n ` a . map(f) ^ n ` map(f,iter2(f,a))"; ``` clasohm@0 ` 100` ```br (iter2B RS ssubst) 1;back();back(); ``` clasohm@0 ` 101` ```by (SIMP_TAC (list_ss addrews [prem RS nmapBcons]) 1); ``` clasohm@0 ` 102` ```val iter2Blemma = result(); ``` clasohm@0 ` 103` clasohm@0 ` 104` ```goal Stream.thy "iter1(f,a) = iter2(f,a)"; ``` clasohm@0 ` 105` ```by (eq_coinduct3_tac ``` clasohm@0 ` 106` ``` "{p. EX x y.p= & (EX n:Nat.x=iter1(f,f^n`a) & y=map(f)^n`iter2(f,a))}" 1); ``` clasohm@0 ` 107` ```by (fast_tac (type_cs addSIs [napplyBzero RS sym,napplyBzero RS sym RS arg_cong]) 1); ``` clasohm@0 ` 108` ```by (EQgen_tac list_ss [iter1B,iter2Blemma] 1); ``` clasohm@0 ` 109` ```by (rtac (napply_f RS ssubst) 1 THEN atac 1); ``` clasohm@0 ` 110` ```by (res_inst_tac [("f1","f")] (napplyBsucc RS subst) 1); ``` clasohm@0 ` 111` ```by (fast_tac type_cs 1); ``` clasohm@0 ` 112` ```val iter1_iter2_eq = result(); ```