31 fun mk_all (x, t) = HOLogic.all_const (fastype_of x) $ Term.lambda x t |
31 fun mk_all (x, t) = HOLogic.all_const (fastype_of x) $ Term.lambda x t |
32 |
32 |
33 |
33 |
34 (*** Basic HOLCF concepts ***) |
34 (*** Basic HOLCF concepts ***) |
35 |
35 |
36 fun mk_bottom T = Const (@{const_name bottom}, T) |
36 fun mk_bottom T = Const (\<^const_name>\<open>bottom\<close>, T) |
37 |
37 |
38 fun below_const T = Const (@{const_name below}, [T, T] ---> boolT) |
38 fun below_const T = Const (\<^const_name>\<open>below\<close>, [T, T] ---> boolT) |
39 fun mk_below (t, u) = below_const (fastype_of t) $ t $ u |
39 fun mk_below (t, u) = below_const (fastype_of t) $ t $ u |
40 |
40 |
41 fun mk_undef t = mk_eq (t, mk_bottom (fastype_of t)) |
41 fun mk_undef t = mk_eq (t, mk_bottom (fastype_of t)) |
42 |
42 |
43 fun mk_defined t = mk_not (mk_undef t) |
43 fun mk_defined t = mk_not (mk_undef t) |
44 |
44 |
45 fun mk_adm t = |
45 fun mk_adm t = |
46 Const (@{const_name adm}, fastype_of t --> boolT) $ t |
46 Const (\<^const_name>\<open>adm\<close>, fastype_of t --> boolT) $ t |
47 |
47 |
48 fun mk_compact t = |
48 fun mk_compact t = |
49 Const (@{const_name compact}, fastype_of t --> boolT) $ t |
49 Const (\<^const_name>\<open>compact\<close>, fastype_of t --> boolT) $ t |
50 |
50 |
51 fun mk_cont t = |
51 fun mk_cont t = |
52 Const (@{const_name cont}, fastype_of t --> boolT) $ t |
52 Const (\<^const_name>\<open>cont\<close>, fastype_of t --> boolT) $ t |
53 |
53 |
54 fun mk_chain t = |
54 fun mk_chain t = |
55 Const (@{const_name chain}, Term.fastype_of t --> boolT) $ t |
55 Const (\<^const_name>\<open>chain\<close>, Term.fastype_of t --> boolT) $ t |
56 |
56 |
57 fun mk_lub t = |
57 fun mk_lub t = |
58 let |
58 let |
59 val T = Term.range_type (Term.fastype_of t) |
59 val T = Term.range_type (Term.fastype_of t) |
60 val lub_const = Const (@{const_name lub}, mk_setT T --> T) |
60 val lub_const = Const (\<^const_name>\<open>lub\<close>, mk_setT T --> T) |
61 val UNIV_const = @{term "UNIV :: nat set"} |
61 val UNIV_const = \<^term>\<open>UNIV :: nat set\<close> |
62 val image_type = (natT --> T) --> mk_setT natT --> mk_setT T |
62 val image_type = (natT --> T) --> mk_setT natT --> mk_setT T |
63 val image_const = Const (@{const_name image}, image_type) |
63 val image_const = Const (\<^const_name>\<open>image\<close>, image_type) |
64 in |
64 in |
65 lub_const $ (image_const $ t $ UNIV_const) |
65 lub_const $ (image_const $ t $ UNIV_const) |
66 end |
66 end |
67 |
67 |
68 |
68 |
69 (*** Continuous function space ***) |
69 (*** Continuous function space ***) |
70 |
70 |
71 fun mk_cfunT (T, U) = Type(@{type_name cfun}, [T, U]) |
71 fun mk_cfunT (T, U) = Type(\<^type_name>\<open>cfun\<close>, [T, U]) |
72 |
72 |
73 val (op ->>) = mk_cfunT |
73 val (op ->>) = mk_cfunT |
74 val (op -->>) = Library.foldr mk_cfunT |
74 val (op -->>) = Library.foldr mk_cfunT |
75 |
75 |
76 fun dest_cfunT (Type(@{type_name cfun}, [T, U])) = (T, U) |
76 fun dest_cfunT (Type(\<^type_name>\<open>cfun\<close>, [T, U])) = (T, U) |
77 | dest_cfunT T = raise TYPE ("dest_cfunT", [T], []) |
77 | dest_cfunT T = raise TYPE ("dest_cfunT", [T], []) |
78 |
78 |
79 fun capply_const (S, T) = |
79 fun capply_const (S, T) = |
80 Const(@{const_name Rep_cfun}, (S ->> T) --> (S --> T)) |
80 Const(\<^const_name>\<open>Rep_cfun\<close>, (S ->> T) --> (S --> T)) |
81 |
81 |
82 fun cabs_const (S, T) = |
82 fun cabs_const (S, T) = |
83 Const(@{const_name Abs_cfun}, (S --> T) --> (S ->> T)) |
83 Const(\<^const_name>\<open>Abs_cfun\<close>, (S --> T) --> (S ->> T)) |
84 |
84 |
85 fun mk_cabs t = |
85 fun mk_cabs t = |
86 let val T = fastype_of t |
86 let val T = fastype_of t |
87 in cabs_const (Term.dest_funT T) $ t end |
87 in cabs_const (Term.dest_funT T) $ t end |
88 |
88 |
99 | big_lambdas (v::vs) rhs = big_lambda v (big_lambdas vs rhs) |
99 | big_lambdas (v::vs) rhs = big_lambda v (big_lambdas vs rhs) |
100 |
100 |
101 fun mk_capply (t, u) = |
101 fun mk_capply (t, u) = |
102 let val (S, T) = |
102 let val (S, T) = |
103 case fastype_of t of |
103 case fastype_of t of |
104 Type(@{type_name cfun}, [S, T]) => (S, T) |
104 Type(\<^type_name>\<open>cfun\<close>, [S, T]) => (S, T) |
105 | _ => raise TERM ("mk_capply " ^ ML_Syntax.print_list ML_Syntax.print_term [t, u], [t, u]) |
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 |
106 in capply_const (S, T) $ t $ u end |
107 |
107 |
108 val (op `) = mk_capply |
108 val (op `) = mk_capply |
109 |
109 |
110 val list_ccomb : term * term list -> term = Library.foldl mk_capply |
110 val list_ccomb : term * term list -> term = Library.foldl mk_capply |
111 |
111 |
112 fun mk_ID T = Const (@{const_name ID}, T ->> T) |
112 fun mk_ID T = Const (\<^const_name>\<open>ID\<close>, T ->> T) |
113 |
113 |
114 fun cfcomp_const (T, U, V) = |
114 fun cfcomp_const (T, U, V) = |
115 Const (@{const_name cfcomp}, (U ->> V) ->> (T ->> U) ->> (T ->> V)) |
115 Const (\<^const_name>\<open>cfcomp\<close>, (U ->> V) ->> (T ->> U) ->> (T ->> V)) |
116 |
116 |
117 fun mk_cfcomp (f, g) = |
117 fun mk_cfcomp (f, g) = |
118 let |
118 let |
119 val (U, V) = dest_cfunT (fastype_of f) |
119 val (U, V) = dest_cfunT (fastype_of f) |
120 val (T, U') = dest_cfunT (fastype_of g) |
120 val (T, U') = dest_cfunT (fastype_of g) |
152 HOLogic.mk_case_prod (Term.lambda v (lambda_tuple vs rhs)) |
152 HOLogic.mk_case_prod (Term.lambda v (lambda_tuple vs rhs)) |
153 |
153 |
154 |
154 |
155 (*** Lifted cpo type ***) |
155 (*** Lifted cpo type ***) |
156 |
156 |
157 fun mk_upT T = Type(@{type_name "u"}, [T]) |
157 fun mk_upT T = Type(\<^type_name>\<open>u\<close>, [T]) |
158 |
158 |
159 fun dest_upT (Type(@{type_name "u"}, [T])) = T |
159 fun dest_upT (Type(\<^type_name>\<open>u\<close>, [T])) = T |
160 | dest_upT T = raise TYPE ("dest_upT", [T], []) |
160 | dest_upT T = raise TYPE ("dest_upT", [T], []) |
161 |
161 |
162 fun up_const T = Const(@{const_name up}, T ->> mk_upT T) |
162 fun up_const T = Const(\<^const_name>\<open>up\<close>, T ->> mk_upT T) |
163 |
163 |
164 fun mk_up t = up_const (fastype_of t) ` t |
164 fun mk_up t = up_const (fastype_of t) ` t |
165 |
165 |
166 fun fup_const (T, U) = |
166 fun fup_const (T, U) = |
167 Const(@{const_name fup}, (T ->> U) ->> mk_upT T ->> U) |
167 Const(\<^const_name>\<open>fup\<close>, (T ->> U) ->> mk_upT T ->> U) |
168 |
168 |
169 fun mk_fup t = fup_const (dest_cfunT (fastype_of t)) ` t |
169 fun mk_fup t = fup_const (dest_cfunT (fastype_of t)) ` t |
170 |
170 |
171 fun from_up T = fup_const (T, T) ` mk_ID T |
171 fun from_up T = fup_const (T, T) ` mk_ID T |
172 |
172 |
173 |
173 |
174 (*** Lifted unit type ***) |
174 (*** Lifted unit type ***) |
175 |
175 |
176 val oneT = @{typ "one"} |
176 val oneT = \<^typ>\<open>one\<close> |
177 |
177 |
178 fun one_case_const T = Const (@{const_name one_case}, T ->> oneT ->> T) |
178 fun one_case_const T = Const (\<^const_name>\<open>one_case\<close>, T ->> oneT ->> T) |
179 fun mk_one_case t = one_case_const (fastype_of t) ` t |
179 fun mk_one_case t = one_case_const (fastype_of t) ` t |
180 |
180 |
181 |
181 |
182 (*** Strict product type ***) |
182 (*** Strict product type ***) |
183 |
183 |
184 fun mk_sprodT (T, U) = Type(@{type_name sprod}, [T, U]) |
184 fun mk_sprodT (T, U) = Type(\<^type_name>\<open>sprod\<close>, [T, U]) |
185 |
185 |
186 fun dest_sprodT (Type(@{type_name sprod}, [T, U])) = (T, U) |
186 fun dest_sprodT (Type(\<^type_name>\<open>sprod\<close>, [T, U])) = (T, U) |
187 | dest_sprodT T = raise TYPE ("dest_sprodT", [T], []) |
187 | dest_sprodT T = raise TYPE ("dest_sprodT", [T], []) |
188 |
188 |
189 fun spair_const (T, U) = |
189 fun spair_const (T, U) = |
190 Const(@{const_name spair}, T ->> U ->> mk_sprodT (T, U)) |
190 Const(\<^const_name>\<open>spair\<close>, T ->> U ->> mk_sprodT (T, U)) |
191 |
191 |
192 (* builds the expression (:t, u:) *) |
192 (* builds the expression (:t, u:) *) |
193 fun mk_spair (t, u) = |
193 fun mk_spair (t, u) = |
194 spair_const (fastype_of t, fastype_of u) ` t ` u |
194 spair_const (fastype_of t, fastype_of u) ` t ` u |
195 |
195 |
196 (* builds the expression (:t1,t2,..,tn:) *) |
196 (* builds the expression (:t1,t2,..,tn:) *) |
197 fun mk_stuple [] = @{term "ONE"} |
197 fun mk_stuple [] = \<^term>\<open>ONE\<close> |
198 | mk_stuple (t::[]) = t |
198 | mk_stuple (t::[]) = t |
199 | mk_stuple (t::ts) = mk_spair (t, mk_stuple ts) |
199 | mk_stuple (t::ts) = mk_spair (t, mk_stuple ts) |
200 |
200 |
201 fun sfst_const (T, U) = |
201 fun sfst_const (T, U) = |
202 Const(@{const_name sfst}, mk_sprodT (T, U) ->> T) |
202 Const(\<^const_name>\<open>sfst\<close>, mk_sprodT (T, U) ->> T) |
203 |
203 |
204 fun ssnd_const (T, U) = |
204 fun ssnd_const (T, U) = |
205 Const(@{const_name ssnd}, mk_sprodT (T, U) ->> U) |
205 Const(\<^const_name>\<open>ssnd\<close>, mk_sprodT (T, U) ->> U) |
206 |
206 |
207 fun ssplit_const (T, U, V) = |
207 fun ssplit_const (T, U, V) = |
208 Const (@{const_name ssplit}, (T ->> U ->> V) ->> mk_sprodT (T, U) ->> V) |
208 Const (\<^const_name>\<open>ssplit\<close>, (T ->> U ->> V) ->> mk_sprodT (T, U) ->> V) |
209 |
209 |
210 fun mk_ssplit t = |
210 fun mk_ssplit t = |
211 let val (T, (U, V)) = apsnd dest_cfunT (dest_cfunT (fastype_of t)) |
211 let val (T, (U, V)) = apsnd dest_cfunT (dest_cfunT (fastype_of t)) |
212 in ssplit_const (T, U, V) ` t end |
212 in ssplit_const (T, U, V) ` t end |
213 |
213 |
214 |
214 |
215 (*** Strict sum type ***) |
215 (*** Strict sum type ***) |
216 |
216 |
217 fun mk_ssumT (T, U) = Type(@{type_name ssum}, [T, U]) |
217 fun mk_ssumT (T, U) = Type(\<^type_name>\<open>ssum\<close>, [T, U]) |
218 |
218 |
219 fun dest_ssumT (Type(@{type_name ssum}, [T, U])) = (T, U) |
219 fun dest_ssumT (Type(\<^type_name>\<open>ssum\<close>, [T, U])) = (T, U) |
220 | dest_ssumT T = raise TYPE ("dest_ssumT", [T], []) |
220 | dest_ssumT T = raise TYPE ("dest_ssumT", [T], []) |
221 |
221 |
222 fun sinl_const (T, U) = Const(@{const_name sinl}, T ->> mk_ssumT (T, U)) |
222 fun sinl_const (T, U) = Const(\<^const_name>\<open>sinl\<close>, T ->> mk_ssumT (T, U)) |
223 fun sinr_const (T, U) = Const(@{const_name sinr}, U ->> mk_ssumT (T, U)) |
223 fun sinr_const (T, U) = Const(\<^const_name>\<open>sinr\<close>, U ->> mk_ssumT (T, U)) |
224 |
224 |
225 (* builds the list [sinl(t1), sinl(sinr(t2)), ... sinr(...sinr(tn))] *) |
225 (* builds the list [sinl(t1), sinl(sinr(t2)), ... sinr(...sinr(tn))] *) |
226 fun mk_sinjects ts = |
226 fun mk_sinjects ts = |
227 let |
227 let |
228 val Ts = map fastype_of ts |
228 val Ts = map fastype_of ts |
256 sscase_const (T, U, U) ` mk_bottom (T ->> U) ` mk_ID U |
256 sscase_const (T, U, U) ` mk_bottom (T ->> U) ` mk_ID U |
257 |
257 |
258 |
258 |
259 (*** pattern match monad type ***) |
259 (*** pattern match monad type ***) |
260 |
260 |
261 fun mk_matchT T = Type (@{type_name "match"}, [T]) |
261 fun mk_matchT T = Type (\<^type_name>\<open>match\<close>, [T]) |
262 |
262 |
263 fun dest_matchT (Type(@{type_name "match"}, [T])) = T |
263 fun dest_matchT (Type(\<^type_name>\<open>match\<close>, [T])) = T |
264 | dest_matchT T = raise TYPE ("dest_matchT", [T], []) |
264 | dest_matchT T = raise TYPE ("dest_matchT", [T], []) |
265 |
265 |
266 fun mk_fail T = Const (@{const_name "Fixrec.fail"}, mk_matchT T) |
266 fun mk_fail T = Const (\<^const_name>\<open>Fixrec.fail\<close>, mk_matchT T) |
267 |
267 |
268 fun succeed_const T = Const (@{const_name "Fixrec.succeed"}, T ->> mk_matchT T) |
268 fun succeed_const T = Const (\<^const_name>\<open>Fixrec.succeed\<close>, T ->> mk_matchT T) |
269 fun mk_succeed t = succeed_const (fastype_of t) ` t |
269 fun mk_succeed t = succeed_const (fastype_of t) ` t |
270 |
270 |
271 |
271 |
272 (*** lifted boolean type ***) |
272 (*** lifted boolean type ***) |
273 |
273 |
274 val trT = @{typ "tr"} |
274 val trT = \<^typ>\<open>tr\<close> |
275 |
275 |
276 |
276 |
277 (*** theory of fixed points ***) |
277 (*** theory of fixed points ***) |
278 |
278 |
279 fun mk_fix t = |
279 fun mk_fix t = |
280 let val (T, _) = dest_cfunT (fastype_of t) |
280 let val (T, _) = dest_cfunT (fastype_of t) |
281 in mk_capply (Const(@{const_name fix}, (T ->> T) ->> T), t) end |
281 in mk_capply (Const(\<^const_name>\<open>fix\<close>, (T ->> T) ->> T), t) end |
282 |
282 |
283 fun iterate_const T = |
283 fun iterate_const T = |
284 Const (@{const_name iterate}, natT --> (T ->> T) ->> (T ->> T)) |
284 Const (\<^const_name>\<open>iterate\<close>, natT --> (T ->> T) ->> (T ->> T)) |
285 |
285 |
286 fun mk_iterate (n, f) = |
286 fun mk_iterate (n, f) = |
287 let val (T, _) = dest_cfunT (Term.fastype_of f) |
287 let val (T, _) = dest_cfunT (Term.fastype_of f) |
288 in (iterate_const T $ n) ` f ` mk_bottom T end |
288 in (iterate_const T $ n) ` f ` mk_bottom T end |
289 |
289 |