1 (* Title: HOLCF/dlist.thy |
|
2 |
|
3 Author: Franz Regensburger |
|
4 ID: $ $ |
|
5 Copyright 1994 Technische Universitaet Muenchen |
|
6 |
|
7 Theory for finite lists 'a dlist = one ++ ('a ** 'a dlist) |
|
8 |
|
9 The type is axiomatized as the least solution of the domain equation above. |
|
10 The functor term that specifies the domain equation is: |
|
11 |
|
12 FT = <++,K_{one},<**,K_{'a},I>> |
|
13 |
|
14 For details see chapter 5 of: |
|
15 |
|
16 [Franz Regensburger] HOLCF: Eine konservative Erweiterung von HOL um LCF, |
|
17 Dissertation, Technische Universit"at M"unchen, 1994 |
|
18 |
|
19 |
|
20 *) |
|
21 |
|
22 Dlist = Stream2 + |
|
23 |
|
24 types dlist 1 |
|
25 |
|
26 (* ----------------------------------------------------------------------- *) |
|
27 (* arity axiom is validated by semantic reasoning *) |
|
28 (* partial ordering is implicit in the isomorphism axioms and their cont. *) |
|
29 |
|
30 arities dlist::(pcpo)pcpo |
|
31 |
|
32 consts |
|
33 |
|
34 (* ----------------------------------------------------------------------- *) |
|
35 (* essential constants *) |
|
36 |
|
37 dlist_rep :: "('a dlist) -> (one ++ 'a ** 'a dlist)" |
|
38 dlist_abs :: "(one ++ 'a ** 'a dlist) -> ('a dlist)" |
|
39 |
|
40 (* ----------------------------------------------------------------------- *) |
|
41 (* abstract constants and auxiliary constants *) |
|
42 |
|
43 dlist_copy :: "('a dlist -> 'a dlist) ->'a dlist -> 'a dlist" |
|
44 |
|
45 dnil :: "'a dlist" |
|
46 dcons :: "'a -> 'a dlist -> 'a dlist" |
|
47 dlist_when :: " 'b -> ('a -> 'a dlist -> 'b) -> 'a dlist -> 'b" |
|
48 is_dnil :: "'a dlist -> tr" |
|
49 is_dcons :: "'a dlist -> tr" |
|
50 dhd :: "'a dlist -> 'a" |
|
51 dtl :: "'a dlist -> 'a dlist" |
|
52 dlist_take :: "nat => 'a dlist -> 'a dlist" |
|
53 dlist_finite :: "'a dlist => bool" |
|
54 dlist_bisim :: "('a dlist => 'a dlist => bool) => bool" |
|
55 |
|
56 rules |
|
57 |
|
58 (* ----------------------------------------------------------------------- *) |
|
59 (* axiomatization of recursive type 'a dlist *) |
|
60 (* ----------------------------------------------------------------------- *) |
|
61 (* ('a dlist,dlist_abs) is the initial F-algebra where *) |
|
62 (* F is the locally continuous functor determined by functor term FT. *) |
|
63 (* domain equation: 'a dlist = one ++ ('a ** 'a dlist) *) |
|
64 (* functor term: FT = <++,K_{one},<**,K_{'a},I>> *) |
|
65 (* ----------------------------------------------------------------------- *) |
|
66 (* dlist_abs is an isomorphism with inverse dlist_rep *) |
|
67 (* identity is the least endomorphism on 'a dlist *) |
|
68 |
|
69 dlist_abs_iso "dlist_rep`(dlist_abs`x) = x" |
|
70 dlist_rep_iso "dlist_abs`(dlist_rep`x) = x" |
|
71 dlist_copy_def "dlist_copy == (LAM f. dlist_abs oo \ |
|
72 \ (sswhen`sinl`(sinr oo (ssplit`(LAM x y. (|x,f`y|) ))))\ |
|
73 \ oo dlist_rep)" |
|
74 dlist_reach "(fix`dlist_copy)`x=x" |
|
75 |
|
76 |
|
77 defs |
|
78 (* ----------------------------------------------------------------------- *) |
|
79 (* properties of additional constants *) |
|
80 (* ----------------------------------------------------------------------- *) |
|
81 (* constructors *) |
|
82 |
|
83 dnil_def "dnil == dlist_abs`(sinl`one)" |
|
84 dcons_def "dcons == (LAM x l. dlist_abs`(sinr`(|x,l|) ))" |
|
85 |
|
86 (* ----------------------------------------------------------------------- *) |
|
87 (* discriminator functional *) |
|
88 |
|
89 dlist_when_def |
|
90 "dlist_when == (LAM f1 f2 l.\ |
|
91 \ sswhen`(LAM x.f1) `(ssplit`(LAM x l.f2`x`l)) `(dlist_rep`l))" |
|
92 |
|
93 (* ----------------------------------------------------------------------- *) |
|
94 (* discriminators and selectors *) |
|
95 |
|
96 is_dnil_def "is_dnil == dlist_when`TT`(LAM x l.FF)" |
|
97 is_dcons_def "is_dcons == dlist_when`FF`(LAM x l.TT)" |
|
98 dhd_def "dhd == dlist_when`UU`(LAM x l.x)" |
|
99 dtl_def "dtl == dlist_when`UU`(LAM x l.l)" |
|
100 |
|
101 (* ----------------------------------------------------------------------- *) |
|
102 (* the taker for dlists *) |
|
103 |
|
104 dlist_take_def "dlist_take == (%n.iterate n dlist_copy UU)" |
|
105 |
|
106 (* ----------------------------------------------------------------------- *) |
|
107 |
|
108 dlist_finite_def "dlist_finite == (%s.? n.dlist_take n`s=s)" |
|
109 |
|
110 (* ----------------------------------------------------------------------- *) |
|
111 (* definition of bisimulation is determined by domain equation *) |
|
112 (* simplification and rewriting for abstract constants yields def below *) |
|
113 |
|
114 dlist_bisim_def "dlist_bisim == |
|
115 ( %R.!l1 l2. |
|
116 R l1 l2 --> |
|
117 ((l1=UU & l2=UU) | |
|
118 (l1=dnil & l2=dnil) | |
|
119 (? x l11 l21. x~=UU & l11~=UU & l21~=UU & |
|
120 l1=dcons`x`l11 & l2 = dcons`x`l21 & R l11 l21)))" |
|
121 |
|
122 end |
|
123 |
|
124 |
|
125 |
|
126 |
|