src/CCL/ex/Stream.ML
 author paulson Mon Dec 07 18:26:25 1998 +0100 (1998-12-07) changeset 6019 0e55c2fb2ebb parent 5062 fbdb0b541314 child 17456 bcf7544875b2 permissions -rw-r--r--
tidying
 clasohm@1459 ` 1` ```(* Title: CCL/ex/stream ``` clasohm@0 ` 2` ``` ID: \$Id\$ ``` clasohm@1459 ` 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 ``` wenzelm@3837 ` 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@1459 ` 22` ```by (etac (XH_to_E ListsXH) 1); ``` clasohm@0 ` 23` ```by (EQgen_tac list_ss [] 1); ``` lcp@8 ` 24` ```by (simp_tac list_ss 1); ``` clasohm@0 ` 25` ```by (fast_tac ccl_cs 1); ``` clasohm@757 ` 26` ```qed "map_comp"; ``` clasohm@0 ` 27` clasohm@0 ` 28` ```(*** Mapping the identity function leaves a list unchanged ***) ``` clasohm@0 ` 29` wenzelm@3837 ` 30` ```val prems = goal Stream.thy "l:Lists(A) ==> map(%x. x,l) = l"; ``` clasohm@0 ` 31` ```by (eq_coinduct3_tac ``` wenzelm@3837 ` 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@1459 ` 35` ```by (etac (XH_to_E ListsXH) 1); ``` clasohm@0 ` 36` ```by (EQgen_tac list_ss [] 1); ``` clasohm@0 ` 37` ```by (fast_tac ccl_cs 1); ``` clasohm@757 ` 38` ```qed "map_id"; ``` 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)"; ``` wenzelm@3837 ` 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@1459 ` 48` ```by (etac (XH_to_E ListsXH) 1); ``` clasohm@0 ` 49` ```by (EQgen_tac list_ss [] 1); ``` clasohm@1459 ` 50` ```by (etac (XH_to_E ListsXH) 1); ``` clasohm@0 ` 51` ```by (EQgen_tac list_ss [] 1); ``` clasohm@0 ` 52` ```by (fast_tac ccl_cs 1); ``` clasohm@757 ` 53` ```qed "map_append"; ``` 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"; ``` lcp@1001 ` 59` ```by (eq_coinduct3_tac ``` wenzelm@3837 ` 60` ``` "{p. EX x y. p= & (EX k:Lists(A).EX l:Lists(A).EX m:Lists(A). \ ``` lcp@1001 ` 61` ```\ x=k @ l @ m & y=(k @ l) @ m)}" 1); ``` clasohm@0 ` 62` ```by (fast_tac (ccl_cs addSIs prems) 1); ``` clasohm@0 ` 63` ```by (safe_tac type_cs); ``` clasohm@1459 ` 64` ```by (etac (XH_to_E ListsXH) 1); ``` clasohm@0 ` 65` ```by (EQgen_tac list_ss [] 1); ``` lcp@1001 ` 66` ```by (fast_tac ccl_cs 2); ``` lcp@1001 ` 67` ```by (DEPTH_SOLVE (etac (XH_to_E ListsXH) 1 THEN EQgen_tac list_ss [] 1)); ``` clasohm@757 ` 68` ```qed "append_assoc"; ``` clasohm@0 ` 69` clasohm@0 ` 70` ```(*** Appending anything to an infinite list doesn't alter it ****) ``` clasohm@0 ` 71` clasohm@0 ` 72` ```val prems = goal Stream.thy "l:ILists(A) ==> l @ m = l"; ``` lcp@1001 ` 73` ```by (eq_coinduct3_tac ``` wenzelm@3837 ` 74` ``` "{p. EX x y. p= & (EX l:ILists(A).EX m. x=l@m & y=l)}" 1); ``` clasohm@0 ` 75` ```by (fast_tac (ccl_cs addSIs prems) 1); ``` clasohm@0 ` 76` ```by (safe_tac set_cs); ``` clasohm@1459 ` 77` ```by (etac (XH_to_E IListsXH) 1); ``` clasohm@0 ` 78` ```by (EQgen_tac list_ss [] 1); ``` clasohm@0 ` 79` ```by (fast_tac ccl_cs 1); ``` clasohm@757 ` 80` ```qed "ilist_append"; ``` clasohm@0 ` 81` clasohm@0 ` 82` ```(*** The equivalance of two versions of an iteration function ***) ``` clasohm@0 ` 83` ```(* *) ``` clasohm@290 ` 84` ```(* fun iter1(f,a) = a\$iter1(f,f(a)) *) ``` clasohm@290 ` 85` ```(* fun iter2(f,a) = a\$map(f,iter2(f,a)) *) ``` clasohm@0 ` 86` wenzelm@5062 ` 87` ```Goalw [iter1_def] "iter1(f,a) = a\$iter1(f,f(a))"; ``` clasohm@1459 ` 88` ```by (rtac (letrecB RS trans) 1); ``` lcp@8 ` 89` ```by (simp_tac term_ss 1); ``` clasohm@757 ` 90` ```qed "iter1B"; ``` clasohm@0 ` 91` wenzelm@5062 ` 92` ```Goalw [iter2_def] "iter2(f,a) = a \$ map(f,iter2(f,a))"; ``` clasohm@1459 ` 93` ```by (rtac (letrecB RS trans) 1); ``` clasohm@1459 ` 94` ```by (rtac refl 1); ``` clasohm@757 ` 95` ```qed "iter2B"; ``` clasohm@0 ` 96` clasohm@0 ` 97` ```val [prem] =goal Stream.thy ``` lcp@1001 ` 98` ``` "n:Nat ==> \ ``` lcp@1001 ` 99` ```\ map(f) ^ n ` iter2(f,a) = (f ^ n ` a) \$ (map(f) ^ n ` map(f,iter2(f,a)))"; ``` lcp@1001 ` 100` ```by (res_inst_tac [("P", "%x. ?lhs(x) = ?rhs")] (iter2B RS ssubst) 1); ``` lcp@8 ` 101` ```by (simp_tac (list_ss addsimps [prem RS nmapBcons]) 1); ``` clasohm@757 ` 102` ```qed "iter2Blemma"; ``` clasohm@0 ` 103` wenzelm@5062 ` 104` ```Goal "iter1(f,a) = iter2(f,a)"; ``` clasohm@0 ` 105` ```by (eq_coinduct3_tac ``` wenzelm@3837 ` 106` ``` "{p. EX x y. p= & (EX n:Nat. x=iter1(f,f^n`a) & y=map(f)^n`iter2(f,a))}" ``` lcp@8 ` 107` ``` 1); ``` lcp@8 ` 108` ```by (fast_tac (type_cs addSIs [napplyBzero RS sym, ``` clasohm@1459 ` 109` ``` napplyBzero RS sym RS arg_cong]) 1); ``` clasohm@0 ` 110` ```by (EQgen_tac list_ss [iter1B,iter2Blemma] 1); ``` paulson@2035 ` 111` ```by (stac napply_f 1 THEN atac 1); ``` clasohm@0 ` 112` ```by (res_inst_tac [("f1","f")] (napplyBsucc RS subst) 1); ``` clasohm@0 ` 113` ```by (fast_tac type_cs 1); ``` clasohm@757 ` 114` ```qed "iter1_iter2_eq"; ```