author | huffman |
Fri, 12 Aug 2011 07:18:28 -0700 | |
changeset 44169 | bdcc11b2fdc8 |
parent 44080 | 53d95b52954c |
child 61424 | c3658c18b7bc |
permissions | -rw-r--r-- |
42151 | 1 |
(* Title: HOL/HOLCF/Tools/holcf_library.ML |
35475 | 2 |
Author: Brian Huffman |
3 |
||
4 |
Functions for constructing HOLCF types and terms. |
|
5 |
*) |
|
6 |
||
7 |
structure HOLCF_Library = |
|
8 |
struct |
|
9 |
||
40832 | 10 |
infixr 6 ->> |
11 |
infixr -->> |
|
12 |
infix 9 ` |
|
35476 | 13 |
|
35475 | 14 |
(*** Operations from Isabelle/HOL ***) |
15 |
||
40832 | 16 |
val boolT = HOLogic.boolT |
17 |
val natT = HOLogic.natT |
|
44169 | 18 |
val mk_setT = HOLogic.mk_setT |
35475 | 19 |
|
40832 | 20 |
val mk_equals = Logic.mk_equals |
21 |
val mk_eq = HOLogic.mk_eq |
|
22 |
val mk_trp = HOLogic.mk_Trueprop |
|
23 |
val mk_fst = HOLogic.mk_fst |
|
24 |
val mk_snd = HOLogic.mk_snd |
|
25 |
val mk_not = HOLogic.mk_not |
|
26 |
val mk_conj = HOLogic.mk_conj |
|
27 |
val mk_disj = HOLogic.mk_disj |
|
28 |
val mk_imp = HOLogic.mk_imp |
|
35475 | 29 |
|
40832 | 30 |
fun mk_ex (x, t) = HOLogic.exists_const (fastype_of x) $ Term.lambda x t |
31 |
fun mk_all (x, t) = HOLogic.all_const (fastype_of x) $ Term.lambda x t |
|
35475 | 32 |
|
33 |
||
34 |
(*** Basic HOLCF concepts ***) |
|
35 |
||
41429
cf5f025bc3c7
renamed constant 'UU' to 'bottom', keeping 'UU' as alternative input syntax;
huffman
parents:
40840
diff
changeset
|
36 |
fun mk_bottom T = Const (@{const_name bottom}, T) |
35475 | 37 |
|
40832 | 38 |
fun below_const T = Const (@{const_name below}, [T, T] ---> boolT) |
39 |
fun mk_below (t, u) = below_const (fastype_of t) $ t $ u |
|
35475 | 40 |
|
40832 | 41 |
fun mk_undef t = mk_eq (t, mk_bottom (fastype_of t)) |
35475 | 42 |
|
40832 | 43 |
fun mk_defined t = mk_not (mk_undef t) |
35475 | 44 |
|
40021 | 45 |
fun mk_adm t = |
40832 | 46 |
Const (@{const_name adm}, fastype_of t --> boolT) $ t |
40021 | 47 |
|
35475 | 48 |
fun mk_compact t = |
40832 | 49 |
Const (@{const_name compact}, fastype_of t --> boolT) $ t |
35475 | 50 |
|
51 |
fun mk_cont t = |
|
40832 | 52 |
Const (@{const_name cont}, fastype_of t --> boolT) $ t |
35475 | 53 |
|
35489 | 54 |
fun mk_chain t = |
40832 | 55 |
Const (@{const_name chain}, Term.fastype_of t --> boolT) $ t |
35489 | 56 |
|
35555 | 57 |
fun mk_lub t = |
58 |
let |
|
40832 | 59 |
val T = Term.range_type (Term.fastype_of t) |
44169 | 60 |
val lub_const = Const (@{const_name lub}, mk_setT T --> T) |
40832 | 61 |
val UNIV_const = @{term "UNIV :: nat set"} |
44169 | 62 |
val image_type = (natT --> T) --> mk_setT natT --> mk_setT T |
40832 | 63 |
val image_const = Const (@{const_name image}, image_type) |
35555 | 64 |
in |
65 |
lub_const $ (image_const $ t $ UNIV_const) |
|
40832 | 66 |
end |
35555 | 67 |
|
35475 | 68 |
|
69 |
(*** Continuous function space ***) |
|
70 |
||
40832 | 71 |
fun mk_cfunT (T, U) = Type(@{type_name cfun}, [T, U]) |
35475 | 72 |
|
40832 | 73 |
val (op ->>) = mk_cfunT |
74 |
val (op -->>) = Library.foldr mk_cfunT |
|
35475 | 75 |
|
35525 | 76 |
fun dest_cfunT (Type(@{type_name cfun}, [T, U])) = (T, U) |
40832 | 77 |
| dest_cfunT T = raise TYPE ("dest_cfunT", [T], []) |
35475 | 78 |
|
79 |
fun capply_const (S, T) = |
|
40832 | 80 |
Const(@{const_name Rep_cfun}, (S ->> T) --> (S --> T)) |
35475 | 81 |
|
82 |
fun cabs_const (S, T) = |
|
40832 | 83 |
Const(@{const_name Abs_cfun}, (S --> T) --> (S ->> T)) |
35475 | 84 |
|
85 |
fun mk_cabs t = |
|
86 |
let val T = fastype_of t |
|
40840 | 87 |
in cabs_const (Term.dest_funT T) $ t end |
35475 | 88 |
|
89 |
(* builds the expression (% v1 v2 .. vn. rhs) *) |
|
90 |
fun lambdas [] rhs = rhs |
|
40832 | 91 |
| lambdas (v::vs) rhs = Term.lambda v (lambdas vs rhs) |
35475 | 92 |
|
93 |
(* builds the expression (LAM v. rhs) *) |
|
94 |
fun big_lambda v rhs = |
|
40832 | 95 |
cabs_const (fastype_of v, fastype_of rhs) $ Term.lambda v rhs |
35475 | 96 |
|
97 |
(* builds the expression (LAM v1 v2 .. vn. rhs) *) |
|
98 |
fun big_lambdas [] rhs = rhs |
|
40832 | 99 |
| big_lambdas (v::vs) rhs = big_lambda v (big_lambdas vs rhs) |
35475 | 100 |
|
101 |
fun mk_capply (t, u) = |
|
102 |
let val (S, T) = |
|
103 |
case fastype_of t of |
|
35525 | 104 |
Type(@{type_name cfun}, [S, T]) => (S, T) |
40832 | 105 |
| _ => raise TERM ("mk_capply " ^ ML_Syntax.print_list ML_Syntax.print_term [t, u], [t, u]) |
106 |
in capply_const (S, T) $ t $ u end |
|
35475 | 107 |
|
40832 | 108 |
val (op `) = mk_capply |
35475 | 109 |
|
40832 | 110 |
val list_ccomb : term * term list -> term = Library.foldl mk_capply |
35475 | 111 |
|
40832 | 112 |
fun mk_ID T = Const (@{const_name ID}, T ->> T) |
35475 | 113 |
|
114 |
fun cfcomp_const (T, U, V) = |
|
40832 | 115 |
Const (@{const_name cfcomp}, (U ->> V) ->> (T ->> U) ->> (T ->> V)) |
35475 | 116 |
|
117 |
fun mk_cfcomp (f, g) = |
|
118 |
let |
|
40832 | 119 |
val (U, V) = dest_cfunT (fastype_of f) |
120 |
val (T, U') = dest_cfunT (fastype_of g) |
|
35475 | 121 |
in |
122 |
if U = U' |
|
123 |
then mk_capply (mk_capply (cfcomp_const (T, U, V), f), g) |
|
124 |
else raise TYPE ("mk_cfcomp", [U, U'], [f, g]) |
|
40832 | 125 |
end |
35475 | 126 |
|
40832 | 127 |
fun strictify_const T = Const (@{const_name strictify}, T ->> T) |
128 |
fun mk_strictify t = strictify_const (fastype_of t) ` t |
|
35785 | 129 |
|
35475 | 130 |
fun mk_strict t = |
40832 | 131 |
let val (T, U) = dest_cfunT (fastype_of t) |
132 |
in mk_eq (t ` mk_bottom T, mk_bottom U) end |
|
35475 | 133 |
|
134 |
||
135 |
(*** Product type ***) |
|
136 |
||
137 |
val mk_prodT = HOLogic.mk_prodT |
|
138 |
||
139 |
fun mk_tupleT [] = HOLogic.unitT |
|
140 |
| mk_tupleT [T] = T |
|
40832 | 141 |
| mk_tupleT (T :: Ts) = mk_prodT (T, mk_tupleT Ts) |
35475 | 142 |
|
143 |
(* builds the expression (v1,v2,..,vn) *) |
|
144 |
fun mk_tuple [] = HOLogic.unit |
|
145 |
| mk_tuple (t::[]) = t |
|
40832 | 146 |
| mk_tuple (t::ts) = HOLogic.mk_prod (t, mk_tuple ts) |
35475 | 147 |
|
148 |
(* builds the expression (%(v1,v2,..,vn). rhs) *) |
|
149 |
fun lambda_tuple [] rhs = Term.lambda (Free("unit", HOLogic.unitT)) rhs |
|
150 |
| lambda_tuple (v::[]) rhs = Term.lambda v rhs |
|
151 |
| lambda_tuple (v::vs) rhs = |
|
40832 | 152 |
HOLogic.mk_split (Term.lambda v (lambda_tuple vs rhs)) |
35475 | 153 |
|
154 |
||
155 |
(*** Lifted cpo type ***) |
|
156 |
||
40832 | 157 |
fun mk_upT T = Type(@{type_name "u"}, [T]) |
35475 | 158 |
|
159 |
fun dest_upT (Type(@{type_name "u"}, [T])) = T |
|
40832 | 160 |
| dest_upT T = raise TYPE ("dest_upT", [T], []) |
35475 | 161 |
|
40832 | 162 |
fun up_const T = Const(@{const_name up}, T ->> mk_upT T) |
35475 | 163 |
|
40832 | 164 |
fun mk_up t = up_const (fastype_of t) ` t |
35475 | 165 |
|
166 |
fun fup_const (T, U) = |
|
40832 | 167 |
Const(@{const_name fup}, (T ->> U) ->> mk_upT T ->> U) |
35475 | 168 |
|
40832 | 169 |
fun mk_fup t = fup_const (dest_cfunT (fastype_of t)) ` t |
35785 | 170 |
|
40832 | 171 |
fun from_up T = fup_const (T, T) ` mk_ID T |
35475 | 172 |
|
173 |
||
35785 | 174 |
(*** Lifted unit type ***) |
35475 | 175 |
|
40832 | 176 |
val oneT = @{typ "one"} |
35475 | 177 |
|
40832 | 178 |
fun one_case_const T = Const (@{const_name one_case}, T ->> oneT ->> T) |
179 |
fun mk_one_case t = one_case_const (fastype_of t) ` t |
|
35785 | 180 |
|
181 |
||
182 |
(*** Strict product type ***) |
|
183 |
||
40832 | 184 |
fun mk_sprodT (T, U) = Type(@{type_name sprod}, [T, U]) |
35475 | 185 |
|
35525 | 186 |
fun dest_sprodT (Type(@{type_name sprod}, [T, U])) = (T, U) |
40832 | 187 |
| dest_sprodT T = raise TYPE ("dest_sprodT", [T], []) |
35475 | 188 |
|
189 |
fun spair_const (T, U) = |
|
40832 | 190 |
Const(@{const_name spair}, T ->> U ->> mk_sprodT (T, U)) |
35475 | 191 |
|
192 |
(* builds the expression (:t, u:) *) |
|
193 |
fun mk_spair (t, u) = |
|
40832 | 194 |
spair_const (fastype_of t, fastype_of u) ` t ` u |
35475 | 195 |
|
196 |
(* builds the expression (:t1,t2,..,tn:) *) |
|
197 |
fun mk_stuple [] = @{term "ONE"} |
|
198 |
| mk_stuple (t::[]) = t |
|
40832 | 199 |
| mk_stuple (t::ts) = mk_spair (t, mk_stuple ts) |
35475 | 200 |
|
201 |
fun sfst_const (T, U) = |
|
40832 | 202 |
Const(@{const_name sfst}, mk_sprodT (T, U) ->> T) |
35475 | 203 |
|
204 |
fun ssnd_const (T, U) = |
|
40832 | 205 |
Const(@{const_name ssnd}, mk_sprodT (T, U) ->> U) |
35475 | 206 |
|
35785 | 207 |
fun ssplit_const (T, U, V) = |
40832 | 208 |
Const (@{const_name ssplit}, (T ->> U ->> V) ->> mk_sprodT (T, U) ->> V) |
35785 | 209 |
|
210 |
fun mk_ssplit t = |
|
40832 | 211 |
let val (T, (U, V)) = apsnd dest_cfunT (dest_cfunT (fastype_of t)) |
212 |
in ssplit_const (T, U, V) ` t end |
|
35785 | 213 |
|
35475 | 214 |
|
215 |
(*** Strict sum type ***) |
|
216 |
||
40832 | 217 |
fun mk_ssumT (T, U) = Type(@{type_name ssum}, [T, U]) |
35475 | 218 |
|
35525 | 219 |
fun dest_ssumT (Type(@{type_name ssum}, [T, U])) = (T, U) |
40832 | 220 |
| dest_ssumT T = raise TYPE ("dest_ssumT", [T], []) |
35475 | 221 |
|
40832 | 222 |
fun sinl_const (T, U) = Const(@{const_name sinl}, T ->> mk_ssumT (T, U)) |
223 |
fun sinr_const (T, U) = Const(@{const_name sinr}, U ->> mk_ssumT (T, U)) |
|
35475 | 224 |
|
225 |
(* builds the list [sinl(t1), sinl(sinr(t2)), ... sinr(...sinr(tn))] *) |
|
226 |
fun mk_sinjects ts = |
|
227 |
let |
|
40832 | 228 |
val Ts = map fastype_of ts |
35475 | 229 |
fun combine (t, T) (us, U) = |
230 |
let |
|
40832 | 231 |
val v = sinl_const (T, U) ` t |
232 |
val vs = map (fn u => sinr_const (T, U) ` u) us |
|
35475 | 233 |
in |
234 |
(v::vs, mk_ssumT (T, U)) |
|
235 |
end |
|
35912 | 236 |
fun inj [] = raise Fail "mk_sinjects: empty list" |
35475 | 237 |
| inj ((t, T)::[]) = ([t], T) |
40832 | 238 |
| inj ((t, T)::ts) = combine (t, T) (inj ts) |
35475 | 239 |
in |
240 |
fst (inj (ts ~~ Ts)) |
|
40832 | 241 |
end |
35475 | 242 |
|
243 |
fun sscase_const (T, U, V) = |
|
244 |
Const(@{const_name sscase}, |
|
40832 | 245 |
(T ->> V) ->> (U ->> V) ->> mk_ssumT (T, U) ->> V) |
35475 | 246 |
|
35785 | 247 |
fun mk_sscase (t, u) = |
44080
53d95b52954c
HOLCF: fix warnings about unreferenced identifiers
huffman
parents:
42151
diff
changeset
|
248 |
let val (T, _) = dest_cfunT (fastype_of t) |
40832 | 249 |
val (U, V) = dest_cfunT (fastype_of u) |
250 |
in sscase_const (T, U, V) ` t ` u end |
|
35785 | 251 |
|
35475 | 252 |
fun from_sinl (T, U) = |
40832 | 253 |
sscase_const (T, U, T) ` mk_ID T ` mk_bottom (U ->> T) |
35475 | 254 |
|
255 |
fun from_sinr (T, U) = |
|
40832 | 256 |
sscase_const (T, U, U) ` mk_bottom (T ->> U) ` mk_ID U |
35475 | 257 |
|
258 |
||
259 |
(*** pattern match monad type ***) |
|
260 |
||
40832 | 261 |
fun mk_matchT T = Type (@{type_name "match"}, [T]) |
35475 | 262 |
|
37108
00f13d3ad474
rename type 'a maybe to 'a match; rename Fixrec.return to Fixrec.succeed
huffman
parents:
35912
diff
changeset
|
263 |
fun dest_matchT (Type(@{type_name "match"}, [T])) = T |
40832 | 264 |
| dest_matchT T = raise TYPE ("dest_matchT", [T], []) |
35475 | 265 |
|
40832 | 266 |
fun mk_fail T = Const (@{const_name "Fixrec.fail"}, mk_matchT T) |
35475 | 267 |
|
40832 | 268 |
fun succeed_const T = Const (@{const_name "Fixrec.succeed"}, T ->> mk_matchT T) |
269 |
fun mk_succeed t = succeed_const (fastype_of t) ` t |
|
35475 | 270 |
|
271 |
||
272 |
(*** lifted boolean type ***) |
|
273 |
||
40832 | 274 |
val trT = @{typ "tr"} |
35475 | 275 |
|
276 |
||
277 |
(*** theory of fixed points ***) |
|
278 |
||
279 |
fun mk_fix t = |
|
280 |
let val (T, _) = dest_cfunT (fastype_of t) |
|
40832 | 281 |
in mk_capply (Const(@{const_name fix}, (T ->> T) ->> T), t) end |
35475 | 282 |
|
35489 | 283 |
fun iterate_const T = |
40832 | 284 |
Const (@{const_name iterate}, natT --> (T ->> T) ->> (T ->> T)) |
35489 | 285 |
|
286 |
fun mk_iterate (n, f) = |
|
40832 | 287 |
let val (T, _) = dest_cfunT (Term.fastype_of f) |
288 |
in (iterate_const T $ n) ` f ` mk_bottom T end |
|
35475 | 289 |
|
40832 | 290 |
end |