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