--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/dlist.thy Thu Mar 24 13:43:45 1994 +0100
@@ -0,0 +1,111 @@
+(* Title: HOLCF/dlist.thy
+
+ Author: Franz Regensburger
+ ID: $ $
+ Copyright 1994 Technische Universitaet Muenchen
+
+Theory for lists
+*)
+
+Dlist = Stream2 +
+
+types dlist 1
+
+(* ----------------------------------------------------------------------- *)
+(* arity axiom is validated by semantic reasoning *)
+(* partial ordering is implicit in the isomorphism axioms and their cont. *)
+
+arities dlist::(pcpo)pcpo
+
+consts
+
+(* ----------------------------------------------------------------------- *)
+(* essential constants *)
+
+dlist_rep :: "('a dlist) -> (one ++ 'a ** 'a dlist)"
+dlist_abs :: "(one ++ 'a ** 'a dlist) -> ('a dlist)"
+
+(* ----------------------------------------------------------------------- *)
+(* abstract constants and auxiliary constants *)
+
+dlist_copy :: "('a dlist -> 'a dlist) ->'a dlist -> 'a dlist"
+
+dnil :: "'a dlist"
+dcons :: "'a -> 'a dlist -> 'a dlist"
+dlist_when :: " 'b -> ('a -> 'a dlist -> 'b) -> 'a dlist -> 'b"
+is_dnil :: "'a dlist -> tr"
+is_dcons :: "'a dlist -> tr"
+dhd :: "'a dlist -> 'a"
+dtl :: "'a dlist -> 'a dlist"
+dlist_take :: "nat => 'a dlist -> 'a dlist"
+dlist_finite :: "'a dlist => bool"
+dlist_bisim :: "('a dlist => 'a dlist => bool) => bool"
+
+rules
+
+(* ----------------------------------------------------------------------- *)
+(* axiomatization of recursive type 'a dlist *)
+(* ----------------------------------------------------------------------- *)
+(* ('a dlist,dlist_abs) is the initial F-algebra where *)
+(* F is the locally continuous functor determined by domain equation *)
+(* X = one ++ 'a ** X *)
+(* ----------------------------------------------------------------------- *)
+(* dlist_abs is an isomorphism with inverse dlist_rep *)
+(* identity is the least endomorphism on 'a dlist *)
+
+dlist_abs_iso "dlist_rep[dlist_abs[x]] = x"
+dlist_rep_iso "dlist_abs[dlist_rep[x]] = x"
+dlist_copy_def "dlist_copy == (LAM f. dlist_abs oo \
+\ (when[sinl][sinr oo (ssplit[LAM x y. x ## f[y]])])\
+\ oo dlist_rep)"
+dlist_reach "(fix[dlist_copy])[x]=x"
+
+(* ----------------------------------------------------------------------- *)
+(* properties of additional constants *)
+(* ----------------------------------------------------------------------- *)
+(* constructors *)
+
+dnil_def "dnil == dlist_abs[sinl[one]]"
+dcons_def "dcons == (LAM x l. dlist_abs[sinr[x##l]])"
+
+(* ----------------------------------------------------------------------- *)
+(* discriminator functional *)
+
+dlist_when_def
+"dlist_when == (LAM f1 f2 l.\
+\ when[LAM x.f1][ssplit[LAM x l.f2[x][l]]][dlist_rep[l]])"
+
+(* ----------------------------------------------------------------------- *)
+(* discriminators and selectors *)
+
+is_dnil_def "is_dnil == dlist_when[TT][LAM x l.FF]"
+is_dcons_def "is_dcons == dlist_when[FF][LAM x l.TT]"
+dhd_def "dhd == dlist_when[UU][LAM x l.x]"
+dtl_def "dtl == dlist_when[UU][LAM x l.l]"
+
+(* ----------------------------------------------------------------------- *)
+(* the taker for dlists *)
+
+dlist_take_def "dlist_take == (%n.iterate(n,dlist_copy,UU))"
+
+(* ----------------------------------------------------------------------- *)
+
+dlist_finite_def "dlist_finite == (%s.? n.dlist_take(n)[s]=s)"
+
+(* ----------------------------------------------------------------------- *)
+(* definition of bisimulation is determined by domain equation *)
+(* simplification and rewriting for abstract constants yields def below *)
+
+dlist_bisim_def "dlist_bisim ==\
+\ ( %R.!l1 l2.\
+\ R(l1,l2) -->\
+\ ((l1=UU & l2=UU) |\
+\ (l1=dnil & l2=dnil) |\
+\ (? x l11 l21. x~=UU & l11~=UU & l21~=UU & \
+\ l1=dcons[x][l11] & l2 = dcons[x][l21] & R(l11,l21))))"
+
+end
+
+
+
+