src/HOLCF/explicit_domains/Dnat.thy
changeset 2679 3eac428cdd1b
parent 2678 d5fe793293ac
child 2680 20fa49e610ca
     1.1 --- a/src/HOLCF/explicit_domains/Dnat.thy	Mon Feb 24 09:46:12 1997 +0100
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,112 +0,0 @@
     1.4 -(*  Title:      HOLCF/Dnat.thy
     1.5 -    ID:         $Id$
     1.6 -    Author:     Franz Regensburger
     1.7 -    Copyright   1993 Technische Universitaet Muenchen
     1.8 -
     1.9 -NOT SUPPORTED ANY MORE. USE HOLCF/ex/Dnat.thy INSTEAD.
    1.10 -
    1.11 -Theory for the domain of natural numbers  dnat = one ++ dnat
    1.12 -
    1.13 -The type is axiomatized as the least solution of the domain equation above.
    1.14 -The functor term that specifies the domain equation is: 
    1.15 -
    1.16 -  FT = <++,K_{one},I>
    1.17 -
    1.18 -For details see chapter 5 of:
    1.19 -
    1.20 -[Franz Regensburger] HOLCF: Eine konservative Erweiterung von HOL um LCF,
    1.21 -                     Dissertation, Technische Universit"at M"unchen, 1994
    1.22 -
    1.23 -*)
    1.24 -
    1.25 -Dnat = HOLCF +
    1.26 -
    1.27 -types dnat 0
    1.28 -
    1.29 -(* ----------------------------------------------------------------------- *)
    1.30 -(* arrity axiom is valuated by semantical reasoning                        *)
    1.31 -
    1.32 -arities dnat::pcpo
    1.33 -
    1.34 -consts
    1.35 -
    1.36 -(* ----------------------------------------------------------------------- *)
    1.37 -(* essential constants                                                     *)
    1.38 -
    1.39 -dnat_rep        :: " dnat -> (one ++ dnat)"
    1.40 -dnat_abs        :: "(one ++ dnat) -> dnat"
    1.41 -
    1.42 -(* ----------------------------------------------------------------------- *)
    1.43 -(* abstract constants and auxiliary constants                              *)
    1.44 -
    1.45 -dnat_copy       :: "(dnat -> dnat) -> dnat -> dnat"
    1.46 -
    1.47 -dzero           :: "dnat"
    1.48 -dsucc           :: "dnat -> dnat"
    1.49 -dnat_when       :: "'b -> (dnat -> 'b) -> dnat -> 'b"
    1.50 -is_dzero        :: "dnat -> tr"
    1.51 -is_dsucc        :: "dnat -> tr"
    1.52 -dpred           :: "dnat -> dnat"
    1.53 -dnat_take       :: "nat => dnat -> dnat"
    1.54 -dnat_bisim      :: "(dnat => dnat => bool) => bool"
    1.55 -
    1.56 -rules
    1.57 -
    1.58 -(* ----------------------------------------------------------------------- *)
    1.59 -(* axiomatization of recursive type dnat                                   *)
    1.60 -(* ----------------------------------------------------------------------- *)
    1.61 -(* (dnat,dnat_abs) is the initial F-algebra where                          *)
    1.62 -(* F is the locally continuous functor determined by functor term FT.      *)
    1.63 -(* domain equation: dnat = one ++ dnat                                     *)
    1.64 -(* functor term:    FT = <++,K_{one},I>                                    *) 
    1.65 -(* ----------------------------------------------------------------------- *)
    1.66 -(* dnat_abs is an isomorphism with inverse dnat_rep                        *)
    1.67 -(* identity is the least endomorphism on dnat                              *)
    1.68 -
    1.69 -dnat_abs_iso    "dnat_rep`(dnat_abs`x) = x"
    1.70 -dnat_rep_iso    "dnat_abs`(dnat_rep`x) = x"
    1.71 -dnat_copy_def   "dnat_copy == (LAM f. dnat_abs oo 
    1.72 -                 (sswhen`sinl`(sinr oo f)) oo dnat_rep )"
    1.73 -dnat_reach      "(fix`dnat_copy)`x=x"
    1.74 -
    1.75 -
    1.76 -defs
    1.77 -(* ----------------------------------------------------------------------- *)
    1.78 -(* properties of additional constants                                      *)
    1.79 -(* ----------------------------------------------------------------------- *)
    1.80 -(* constructors                                                            *)
    1.81 -
    1.82 -dzero_def       "dzero == dnat_abs`(sinl`one)"
    1.83 -dsucc_def       "dsucc == (LAM n. dnat_abs`(sinr`n))"
    1.84 -
    1.85 -(* ----------------------------------------------------------------------- *)
    1.86 -(* discriminator functional                                                *)
    1.87 -
    1.88 -dnat_when_def   "dnat_when == (LAM f1 f2 n.sswhen`(LAM x.f1)`f2`(dnat_rep`n))"
    1.89 -
    1.90 -
    1.91 -(* ----------------------------------------------------------------------- *)
    1.92 -(* discriminators and selectors                                            *)
    1.93 -
    1.94 -is_dzero_def    "is_dzero == dnat_when`TT`(LAM x.FF)"
    1.95 -is_dsucc_def    "is_dsucc == dnat_when`FF`(LAM x.TT)"
    1.96 -dpred_def       "dpred == dnat_when`UU`(LAM x.x)"
    1.97 -
    1.98 -
    1.99 -(* ----------------------------------------------------------------------- *)
   1.100 -(* the taker for dnats                                                   *)
   1.101 -
   1.102 -dnat_take_def "dnat_take == (%n.iterate n dnat_copy UU)"
   1.103 -
   1.104 -(* ----------------------------------------------------------------------- *)
   1.105 -(* definition of bisimulation is determined by domain equation             *)
   1.106 -(* simplification and rewriting for abstract constants yields def below    *)
   1.107 -
   1.108 -dnat_bisim_def "dnat_bisim ==
   1.109 -(%R.!s1 s2.
   1.110 -        R s1 s2 -->
   1.111 -  ((s1=UU & s2=UU) |(s1=dzero & s2=dzero) |
   1.112 -  (? s11 s21. s11~=UU & s21~=UU & s1=dsucc`s11 &
   1.113 -                 s2 = dsucc`s21 & R s11 s21)))"
   1.114 -
   1.115 -end