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