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