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=<x,y> & (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=<x,y> & (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=<x,y> & (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=<x,y> & (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=<x,y> & (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=<x,y> & (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();