src/HOLCF/explicit_domains/Dlist.thy
changeset 2679 3eac428cdd1b
parent 2678 d5fe793293ac
child 2680 20fa49e610ca
     1.1 --- a/src/HOLCF/explicit_domains/Dlist.thy	Mon Feb 24 09:46:12 1997 +0100
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,128 +0,0 @@
     1.4 -(*  Title:      HOLCF/Dlist.thy
     1.5 -
     1.6 -    Author:     Franz Regensburger
     1.7 -    ID:         $ $
     1.8 -    Copyright   1994 Technische Universitaet Muenchen
     1.9 -
    1.10 -NOT SUPPORTED ANY MORE. USE HOLCF/ex/Dlist.thy INSTEAD.
    1.11 -
    1.12 -Theory for finite lists  'a dlist = one ++ ('a ** 'a dlist)
    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_{one},<**,K_{'a},I>>
    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 -*)
    1.26 -
    1.27 -Dlist = Stream2 +
    1.28 -
    1.29 -types dlist 1
    1.30 -
    1.31 -(* ----------------------------------------------------------------------- *)
    1.32 -(* arity axiom is validated by semantic reasoning                          *)
    1.33 -(* partial ordering is implicit in the isomorphism axioms and their cont.  *)
    1.34 -
    1.35 -arities dlist::(pcpo)pcpo
    1.36 -
    1.37 -consts
    1.38 -
    1.39 -(* ----------------------------------------------------------------------- *)
    1.40 -(* essential constants                                                     *)
    1.41 -
    1.42 -dlist_rep       :: "('a dlist) -> (one ++ 'a ** 'a dlist)"
    1.43 -dlist_abs       :: "(one ++ 'a ** 'a dlist) -> ('a dlist)"
    1.44 -
    1.45 -(* ----------------------------------------------------------------------- *)
    1.46 -(* abstract constants and auxiliary constants                              *)
    1.47 -
    1.48 -dlist_copy      :: "('a dlist -> 'a dlist) ->'a dlist -> 'a dlist"
    1.49 -
    1.50 -dnil            :: "'a dlist"
    1.51 -dcons           :: "'a -> 'a dlist -> 'a dlist"
    1.52 -dlist_when      :: " 'b -> ('a -> 'a dlist -> 'b) -> 'a dlist -> 'b"
    1.53 -is_dnil         :: "'a dlist -> tr"
    1.54 -is_dcons        :: "'a dlist -> tr"
    1.55 -dhd             :: "'a dlist -> 'a"
    1.56 -dtl             :: "'a dlist -> 'a dlist"
    1.57 -dlist_take      :: "nat => 'a dlist -> 'a dlist"
    1.58 -dlist_finite    :: "'a dlist => bool"
    1.59 -dlist_bisim     :: "('a dlist => 'a dlist => bool) => bool"
    1.60 -
    1.61 -rules
    1.62 -
    1.63 -(* ----------------------------------------------------------------------- *)
    1.64 -(* axiomatization of recursive type 'a dlist                               *)
    1.65 -(* ----------------------------------------------------------------------- *)
    1.66 -(* ('a dlist,dlist_abs) is the initial F-algebra where                     *)
    1.67 -(* F is the locally continuous functor determined by functor term FT.      *)
    1.68 -(* domain equation: 'a dlist = one ++ ('a ** 'a dlist)                     *)
    1.69 -(* functor term:    FT = <++,K_{one},<**,K_{'a},I>>                        *)
    1.70 -(* ----------------------------------------------------------------------- *)
    1.71 -(* dlist_abs is an isomorphism with inverse dlist_rep                      *)
    1.72 -(* identity is the least endomorphism on 'a dlist                          *)
    1.73 -
    1.74 -dlist_abs_iso   "dlist_rep`(dlist_abs`x) = x"
    1.75 -dlist_rep_iso   "dlist_abs`(dlist_rep`x) = x"
    1.76 -dlist_copy_def  "dlist_copy == (LAM f. dlist_abs oo \
    1.77 -\               (sswhen`sinl`(sinr oo (ssplit`(LAM x y. (|x,f`y|) ))))\
    1.78 -\                                oo dlist_rep)"
    1.79 -dlist_reach     "(fix`dlist_copy)`x=x"
    1.80 -
    1.81 -
    1.82 -defs
    1.83 -(* ----------------------------------------------------------------------- *)
    1.84 -(* properties of additional constants                                      *)
    1.85 -(* ----------------------------------------------------------------------- *)
    1.86 -(* constructors                                                            *)
    1.87 -
    1.88 -dnil_def        "dnil  == dlist_abs`(sinl`one)"
    1.89 -dcons_def       "dcons == (LAM x l. dlist_abs`(sinr`(|x,l|) ))"
    1.90 -
    1.91 -(* ----------------------------------------------------------------------- *)
    1.92 -(* discriminator functional                                                *)
    1.93 -
    1.94 -dlist_when_def 
    1.95 -"dlist_when == (LAM f1 f2 l.\
    1.96 -\   sswhen`(LAM x.f1) `(ssplit`(LAM x l.f2`x`l)) `(dlist_rep`l))"
    1.97 -
    1.98 -(* ----------------------------------------------------------------------- *)
    1.99 -(* discriminators and selectors                                            *)
   1.100 -
   1.101 -is_dnil_def     "is_dnil  == dlist_when`TT`(LAM x l.FF)"
   1.102 -is_dcons_def    "is_dcons == dlist_when`FF`(LAM x l.TT)"
   1.103 -dhd_def         "dhd == dlist_when`UU`(LAM x l.x)"
   1.104 -dtl_def         "dtl == dlist_when`UU`(LAM x l.l)"
   1.105 -
   1.106 -(* ----------------------------------------------------------------------- *)
   1.107 -(* the taker for dlists                                                   *)
   1.108 -
   1.109 -dlist_take_def "dlist_take == (%n.iterate n dlist_copy UU)"
   1.110 -
   1.111 -(* ----------------------------------------------------------------------- *)
   1.112 -
   1.113 -dlist_finite_def        "dlist_finite == (%s.? n.dlist_take n`s=s)"
   1.114 -
   1.115 -(* ----------------------------------------------------------------------- *)
   1.116 -(* definition of bisimulation is determined by domain equation             *)
   1.117 -(* simplification and rewriting for abstract constants yields def below    *)
   1.118 -
   1.119 -dlist_bisim_def "dlist_bisim ==
   1.120 - ( %R.!l1 l2.
   1.121 -        R l1 l2 -->
   1.122 -  ((l1=UU & l2=UU) |
   1.123 -   (l1=dnil & l2=dnil) |
   1.124 -   (? x l11 l21. x~=UU & l11~=UU & l21~=UU & 
   1.125 -               l1=dcons`x`l11 & l2 = dcons`x`l21 & R l11 l21)))"
   1.126 -
   1.127 -end
   1.128 -
   1.129 -
   1.130 -
   1.131 -