|
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 |