src/HOLCF/dlist.thy
author wenzelm
Thu Aug 27 20:46:36 1998 +0200 (1998-08-27)
changeset 5400 645f46a24c72
parent 298 3a0485439396
permissions -rw-r--r--
made tutorial first;
     1 (*  Title: 	HOLCF/dlist.thy
     2 
     3     Author: 	Franz Regensburger
     4     ID:         $ $
     5     Copyright   1994 Technische Universitaet Muenchen
     6 
     7 Theory for lists
     8 *)
     9 
    10 Dlist = Stream2 +
    11 
    12 types dlist 1
    13 
    14 (* ----------------------------------------------------------------------- *)
    15 (* arity axiom is validated by semantic reasoning                          *)
    16 (* partial ordering is implicit in the isomorphism axioms and their cont.  *)
    17 
    18 arities dlist::(pcpo)pcpo
    19 
    20 consts
    21 
    22 (* ----------------------------------------------------------------------- *)
    23 (* essential constants                                                     *)
    24 
    25 dlist_rep	:: "('a dlist) -> (one ++ 'a ** 'a dlist)"
    26 dlist_abs	:: "(one ++ 'a ** 'a dlist) -> ('a dlist)"
    27 
    28 (* ----------------------------------------------------------------------- *)
    29 (* abstract constants and auxiliary constants                              *)
    30 
    31 dlist_copy	:: "('a dlist -> 'a dlist) ->'a dlist -> 'a dlist"
    32 
    33 dnil            :: "'a dlist"
    34 dcons		:: "'a -> 'a dlist -> 'a dlist"
    35 dlist_when	:: " 'b -> ('a -> 'a dlist -> 'b) -> 'a dlist -> 'b"
    36 is_dnil    	:: "'a dlist -> tr"
    37 is_dcons	:: "'a dlist -> tr"
    38 dhd		:: "'a dlist -> 'a"
    39 dtl		:: "'a dlist -> 'a dlist"
    40 dlist_take	:: "nat => 'a dlist -> 'a dlist"
    41 dlist_finite	:: "'a dlist => bool"
    42 dlist_bisim	:: "('a dlist => 'a dlist => bool) => bool"
    43 
    44 rules
    45 
    46 (* ----------------------------------------------------------------------- *)
    47 (* axiomatization of recursive type 'a dlist                               *)
    48 (* ----------------------------------------------------------------------- *)
    49 (* ('a dlist,dlist_abs) is the initial F-algebra where                     *)
    50 (* F is the locally continuous functor determined by domain equation       *)
    51 (* X = one ++ 'a ** X                                                      *)
    52 (* ----------------------------------------------------------------------- *)
    53 (* dlist_abs is an isomorphism with inverse dlist_rep                      *)
    54 (* identity is the least endomorphism on 'a dlist                          *)
    55 
    56 dlist_abs_iso	"dlist_rep[dlist_abs[x]] = x"
    57 dlist_rep_iso	"dlist_abs[dlist_rep[x]] = x"
    58 dlist_copy_def	"dlist_copy == (LAM f. dlist_abs oo \
    59 \ 		(when[sinl][sinr oo (ssplit[LAM x y. x ## f[y]])])\
    60 \                                oo dlist_rep)"
    61 dlist_reach	"(fix[dlist_copy])[x]=x"
    62 
    63 (* ----------------------------------------------------------------------- *)
    64 (* properties of additional constants                                      *)
    65 (* ----------------------------------------------------------------------- *)
    66 (* constructors                                                            *)
    67 
    68 dnil_def	"dnil  == dlist_abs[sinl[one]]"
    69 dcons_def	"dcons == (LAM x l. dlist_abs[sinr[x##l]])"
    70 
    71 (* ----------------------------------------------------------------------- *)
    72 (* discriminator functional                                                *)
    73 
    74 dlist_when_def 
    75 "dlist_when == (LAM f1 f2 l.\
    76 \   when[LAM x.f1][ssplit[LAM x l.f2[x][l]]][dlist_rep[l]])"
    77 
    78 (* ----------------------------------------------------------------------- *)
    79 (* discriminators and selectors                                            *)
    80 
    81 is_dnil_def	"is_dnil  == dlist_when[TT][LAM x l.FF]"
    82 is_dcons_def	"is_dcons == dlist_when[FF][LAM x l.TT]"
    83 dhd_def		"dhd == dlist_when[UU][LAM x l.x]"
    84 dtl_def		"dtl == dlist_when[UU][LAM x l.l]"
    85 
    86 (* ----------------------------------------------------------------------- *)
    87 (* the taker for dlists                                                   *)
    88 
    89 dlist_take_def "dlist_take == (%n.iterate(n,dlist_copy,UU))"
    90 
    91 (* ----------------------------------------------------------------------- *)
    92 
    93 dlist_finite_def	"dlist_finite == (%s.? n.dlist_take(n)[s]=s)"
    94 
    95 (* ----------------------------------------------------------------------- *)
    96 (* definition of bisimulation is determined by domain equation             *)
    97 (* simplification and rewriting for abstract constants yields def below    *)
    98 
    99 dlist_bisim_def "dlist_bisim ==\
   100 \ ( %R.!l1 l2.\
   101 \ 	R(l1,l2) -->\
   102 \  ((l1=UU & l2=UU) |\
   103 \   (l1=dnil & l2=dnil) |\
   104 \   (? x l11 l21. x~=UU & l11~=UU & l21~=UU & \
   105 \               l1=dcons[x][l11] & l2 = dcons[x][l21] & R(l11,l21))))"
   106 
   107 end
   108 
   109 
   110 
   111