(* 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