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