src/HOLCF/explicit_domains/Stream.thy
changeset 2679 3eac428cdd1b
parent 2678 d5fe793293ac
child 2680 20fa49e610ca
     1.1 --- a/src/HOLCF/explicit_domains/Stream.thy	Mon Feb 24 09:46:12 1997 +0100
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,117 +0,0 @@
     1.4 -(* 
     1.5 -    ID:         $Id$
     1.6 -    Author:     Franz Regensburger
     1.7 -    Copyright   1993 Technische Universitaet Muenchen
     1.8 -
     1.9 -NOT SUPPORTED ANY MORE. USE HOLCF/ex/Stream.thy INSTEAD.
    1.10 -
    1.11 -Theory for streams without defined empty stream 
    1.12 -  'a stream = 'a ** ('a stream)u
    1.13 -
    1.14 -The type is axiomatized as the least solution of the domain equation above.
    1.15 -The functor term that specifies the domain equation is: 
    1.16 -
    1.17 -  FT = <**,K_{'a},U>
    1.18 -
    1.19 -For details see chapter 5 of:
    1.20 -
    1.21 -[Franz Regensburger] HOLCF: Eine konservative Erweiterung von HOL um LCF,
    1.22 -                     Dissertation, Technische Universit"at M"unchen, 1994
    1.23 -*)
    1.24 -
    1.25 -Stream = Dnat2 +
    1.26 -
    1.27 -types stream 1
    1.28 -
    1.29 -(* ----------------------------------------------------------------------- *)
    1.30 -(* arity axiom is validated by semantic reasoning                          *)
    1.31 -(* partial ordering is implicit in the isomorphism axioms and their cont.  *)
    1.32 -
    1.33 -arities stream::(pcpo)pcpo
    1.34 -
    1.35 -consts
    1.36 -
    1.37 -(* ----------------------------------------------------------------------- *)
    1.38 -(* essential constants                                                     *)
    1.39 -
    1.40 -stream_rep      :: "('a stream) -> ('a ** ('a stream)u)"
    1.41 -stream_abs      :: "('a ** ('a stream)u) -> ('a stream)"
    1.42 -
    1.43 -(* ----------------------------------------------------------------------- *)
    1.44 -(* abstract constants and auxiliary constants                              *)
    1.45 -
    1.46 -stream_copy     :: "('a stream -> 'a stream) ->'a stream -> 'a stream"
    1.47 -
    1.48 -scons           :: "'a -> 'a stream -> 'a stream"
    1.49 -stream_when     :: "('a -> 'a stream -> 'b) -> 'a stream -> 'b"
    1.50 -is_scons        :: "'a stream -> tr"
    1.51 -shd             :: "'a stream -> 'a"
    1.52 -stl             :: "'a stream -> 'a stream"
    1.53 -stream_take     :: "nat => 'a stream -> 'a stream"
    1.54 -stream_finite   :: "'a stream => bool"
    1.55 -stream_bisim    :: "('a stream => 'a stream => bool) => bool"
    1.56 -
    1.57 -rules
    1.58 -
    1.59 -(* ----------------------------------------------------------------------- *)
    1.60 -(* axiomatization of recursive type 'a stream                              *)
    1.61 -(* ----------------------------------------------------------------------- *)
    1.62 -(* ('a stream,stream_abs) is the initial F-algebra where                   *)
    1.63 -(* F is the locally continuous functor determined by functor term FT.      *)
    1.64 -(* domain equation: 'a stream = 'a ** ('a stream)u                         *)
    1.65 -(* functor term:    FT = <**,K_{'a},U>                                     *)
    1.66 -(* ----------------------------------------------------------------------- *)
    1.67 -(* stream_abs is an isomorphism with inverse stream_rep                    *)
    1.68 -(* identity is the least endomorphism on 'a stream                         *)
    1.69 -
    1.70 -stream_abs_iso  "stream_rep`(stream_abs`x) = x"
    1.71 -stream_rep_iso  "stream_abs`(stream_rep`x) = x"
    1.72 -stream_copy_def "stream_copy == (LAM f. stream_abs oo 
    1.73 -                (ssplit`(LAM x y. (|x , (fup`(up oo f))`y|) )) oo stream_rep)"
    1.74 -stream_reach    "(fix`stream_copy)`x = x"
    1.75 -
    1.76 -defs
    1.77 -(* ----------------------------------------------------------------------- *)
    1.78 -(* properties of additional constants                                      *)
    1.79 -(* ----------------------------------------------------------------------- *)
    1.80 -(* constructors                                                            *)
    1.81 -
    1.82 -scons_def       "scons == (LAM x l. stream_abs`(| x, up`l |))"
    1.83 -
    1.84 -(* ----------------------------------------------------------------------- *)
    1.85 -(* discriminator functional                                                *)
    1.86 -
    1.87 -stream_when_def 
    1.88 -"stream_when == (LAM f l.ssplit `(LAM x l.f`x`(fup`ID`l)) `(stream_rep`l))"
    1.89 -
    1.90 -(* ----------------------------------------------------------------------- *)
    1.91 -(* discriminators and selectors                                            *)
    1.92 -
    1.93 -is_scons_def    "is_scons == stream_when`(LAM x l.TT)"
    1.94 -shd_def         "shd == stream_when`(LAM x l.x)"
    1.95 -stl_def         "stl == stream_when`(LAM x l.l)"
    1.96 -
    1.97 -(* ----------------------------------------------------------------------- *)
    1.98 -(* the taker for streams                                                   *)
    1.99 -
   1.100 -stream_take_def "stream_take == (%n.iterate n stream_copy UU)"
   1.101 -
   1.102 -(* ----------------------------------------------------------------------- *)
   1.103 -
   1.104 -stream_finite_def       "stream_finite == (%s.? n.stream_take n `s=s)"
   1.105 -
   1.106 -(* ----------------------------------------------------------------------- *)
   1.107 -(* definition of bisimulation is determined by domain equation             *)
   1.108 -(* simplification and rewriting for abstract constants yields def below    *)
   1.109 -
   1.110 -stream_bisim_def "stream_bisim ==
   1.111 -(%R.!s1 s2.
   1.112 -        R s1 s2 -->
   1.113 -  ((s1=UU & s2=UU) |
   1.114 -  (? x s11 s21. x~=UU & s1=scons`x`s11 & s2 = scons`x`s21 & R s11 s21)))"
   1.115 -
   1.116 -end
   1.117 -
   1.118 -
   1.119 -
   1.120 -