src/HOLCF/stream.thy
author wenzelm
Thu Aug 27 20:46:36 1998 +0200 (1998-08-27)
changeset 5400 645f46a24c72
parent 243 c22b85994e17
permissions -rw-r--r--
made tutorial first;
     1 (*  Title: 	HOLCF/stream.thy
     2     ID:         $Id$
     3     Author: 	Franz Regensburger
     4     Copyright   1993 Technische Universitaet Muenchen
     5 
     6 Theory for streams without defined empty stream
     7 *)
     8 
     9 Stream = Dnat2 +
    10 
    11 types stream 1
    12 
    13 (* ----------------------------------------------------------------------- *)
    14 (* arity axiom is validated by semantic reasoning                          *)
    15 (* partial ordering is implicit in the isomorphism axioms and their cont.  *)
    16 
    17 arities stream::(pcpo)pcpo
    18 
    19 consts
    20 
    21 (* ----------------------------------------------------------------------- *)
    22 (* essential constants                                                     *)
    23 
    24 stream_rep	:: "('a stream) -> ('a ** ('a stream)u)"
    25 stream_abs	:: "('a ** ('a stream)u) -> ('a stream)"
    26 
    27 (* ----------------------------------------------------------------------- *)
    28 (* abstract constants and auxiliary constants                              *)
    29 
    30 stream_copy	:: "('a stream -> 'a stream) ->'a stream -> 'a stream"
    31 
    32 scons		:: "'a -> 'a stream -> 'a stream"
    33 stream_when	:: "('a -> 'a stream -> 'b) -> 'a stream -> 'b"
    34 is_scons	:: "'a stream -> tr"
    35 shd		:: "'a stream -> 'a"
    36 stl		:: "'a stream -> 'a stream"
    37 stream_take	:: "nat => 'a stream -> 'a stream"
    38 stream_finite	:: "'a stream => bool"
    39 stream_bisim	:: "('a stream => 'a stream => bool) => bool"
    40 
    41 rules
    42 
    43 (* ----------------------------------------------------------------------- *)
    44 (* axiomatization of recursive type 'a stream                              *)
    45 (* ----------------------------------------------------------------------- *)
    46 (* ('a stream,stream_abs) is the initial F-algebra where                   *)
    47 (* F is the locally continuous functor determined by domain equation       *)
    48 (* X = 'a ** (X)u                                                          *)
    49 (* ----------------------------------------------------------------------- *)
    50 (* stream_abs is an isomorphism with inverse stream_rep                    *)
    51 (* identity is the least endomorphism on 'a stream                         *)
    52 
    53 stream_abs_iso	"stream_rep[stream_abs[x]] = x"
    54 stream_rep_iso	"stream_abs[stream_rep[x]] = x"
    55 stream_copy_def	"stream_copy == (LAM f. stream_abs oo \
    56 \ 		(ssplit[LAM x y. x ## (lift[up oo f])[y]] oo stream_rep))"
    57 stream_reach	"(fix[stream_copy])[x]=x"
    58 
    59 (* ----------------------------------------------------------------------- *)
    60 (* properties of additional constants                                      *)
    61 (* ----------------------------------------------------------------------- *)
    62 (* constructors                                                            *)
    63 
    64 scons_def	"scons == (LAM x l. stream_abs[x##up[l]])"
    65 
    66 (* ----------------------------------------------------------------------- *)
    67 (* discriminator functional                                                *)
    68 
    69 stream_when_def 
    70 "stream_when == (LAM f l.ssplit[LAM x l.f[x][lift[ID][l]]][stream_rep[l]])"
    71 
    72 (* ----------------------------------------------------------------------- *)
    73 (* discriminators and selectors                                            *)
    74 
    75 is_scons_def	"is_scons == stream_when[LAM x l.TT]"
    76 shd_def		"shd == stream_when[LAM x l.x]"
    77 stl_def		"stl == stream_when[LAM x l.l]"
    78 
    79 (* ----------------------------------------------------------------------- *)
    80 (* the taker for streams                                                   *)
    81 
    82 stream_take_def "stream_take == (%n.iterate(n,stream_copy,UU))"
    83 
    84 (* ----------------------------------------------------------------------- *)
    85 
    86 stream_finite_def	"stream_finite == (%s.? n.stream_take(n)[s]=s)"
    87 
    88 (* ----------------------------------------------------------------------- *)
    89 (* definition of bisimulation is determined by domain equation             *)
    90 (* simplification and rewriting for abstract constants yields def below    *)
    91 
    92 stream_bisim_def "stream_bisim ==\
    93 \(%R.!s1 s2.\
    94 \ 	R(s1,s2) -->\
    95 \  ((s1=UU & s2=UU) |\
    96 \  (? x s11 s21. x~=UU & s1=scons[x][s11] & s2 = scons[x][s21] & R(s11,s21))))"
    97 
    98 end
    99 
   100 
   101 
   102