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