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