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