src/HOLCF/dnat.thy
author wenzelm
Thu Aug 27 20:46:36 1998 +0200 (1998-08-27)
changeset 5400 645f46a24c72
parent 243 c22b85994e17
permissions -rw-r--r--
made tutorial first;
     1 (*  Title: 	HOLCF/dnat.thy
     2     ID:         $Id$
     3     Author: 	Franz Regensburger
     4     Copyright   1993 Technische Universitaet Muenchen
     5 
     6 Theory for the domain of natural numbers
     7 
     8 *)
     9 
    10 Dnat = HOLCF +
    11 
    12 types dnat 0
    13 
    14 (* ----------------------------------------------------------------------- *)
    15 (* arrity axiom is valuated by semantical reasoning                        *)
    16 
    17 arities dnat::pcpo
    18 
    19 consts
    20 
    21 (* ----------------------------------------------------------------------- *)
    22 (* essential constants                                                     *)
    23 
    24 dnat_rep	:: " dnat -> (one ++ dnat)"
    25 dnat_abs	:: "(one ++ dnat) -> dnat"
    26 
    27 (* ----------------------------------------------------------------------- *)
    28 (* abstract constants and auxiliary constants                              *)
    29 
    30 dnat_copy	:: "(dnat -> dnat) -> dnat -> dnat"
    31 
    32 dzero		:: "dnat"
    33 dsucc		:: "dnat -> dnat"
    34 dnat_when	:: "'b -> (dnat -> 'b) -> dnat -> 'b"
    35 is_dzero	:: "dnat -> tr"
    36 is_dsucc	:: "dnat -> tr"
    37 dpred		:: "dnat -> dnat"
    38 dnat_take	:: "nat => dnat -> dnat"
    39 dnat_bisim	:: "(dnat => dnat => bool) => bool"
    40 
    41 rules
    42 
    43 (* ----------------------------------------------------------------------- *)
    44 (* axiomatization of recursive type dnat                                   *)
    45 (* ----------------------------------------------------------------------- *)
    46 (* (dnat,dnat_abs) is the initial F-algebra where                          *)
    47 (* F is the locally continuous functor determined by domain equation       *)
    48 (* X = one ++ X                                                            *)
    49 (* ----------------------------------------------------------------------- *)
    50 (* dnat_abs is an isomorphism with inverse dnat_rep                        *)
    51 (* identity is the least endomorphism on dnat                              *)
    52 
    53 dnat_abs_iso	"dnat_rep[dnat_abs[x]] = x"
    54 dnat_rep_iso	"dnat_abs[dnat_rep[x]] = x"
    55 dnat_copy_def	"dnat_copy == (LAM f. dnat_abs oo \
    56 \		 (when[sinl][sinr oo f]) oo dnat_rep )"
    57 dnat_reach	"(fix[dnat_copy])[x]=x"
    58 
    59 (* ----------------------------------------------------------------------- *)
    60 (* properties of additional constants                                      *)
    61 (* ----------------------------------------------------------------------- *)
    62 (* constructors                                                            *)
    63 
    64 dzero_def	"dzero == dnat_abs[sinl[one]]"
    65 dsucc_def	"dsucc == (LAM n. dnat_abs[sinr[n]])"
    66 
    67 (* ----------------------------------------------------------------------- *)
    68 (* discriminator functional                                                *)
    69 
    70 dnat_when_def	"dnat_when == (LAM f1 f2 n.when[LAM x.f1][f2][dnat_rep[n]])"
    71 
    72 
    73 (* ----------------------------------------------------------------------- *)
    74 (* discriminators and selectors                                            *)
    75 
    76 is_dzero_def	"is_dzero == dnat_when[TT][LAM x.FF]"
    77 is_dsucc_def	"is_dsucc == dnat_when[FF][LAM x.TT]"
    78 dpred_def	"dpred == dnat_when[UU][LAM x.x]"
    79 
    80 
    81 (* ----------------------------------------------------------------------- *)
    82 (* the taker for dnats                                                   *)
    83 
    84 dnat_take_def "dnat_take == (%n.iterate(n,dnat_copy,UU))"
    85 
    86 (* ----------------------------------------------------------------------- *)
    87 (* definition of bisimulation is determined by domain equation             *)
    88 (* simplification and rewriting for abstract constants yields def below    *)
    89 
    90 dnat_bisim_def "dnat_bisim ==\
    91 \(%R.!s1 s2.\
    92 \ 	R(s1,s2) -->\
    93 \  ((s1=UU & s2=UU) |(s1=dzero & s2=dzero) |\
    94 \  (? s11 s21. s11~=UU & s21~=UU & s1=dsucc[s11] &\
    95 \		 s2 = dsucc[s21] & R(s11,s21))))"
    96 
    97 end
    98 
    99 
   100 
   101