31 fun mk_all (x, t) = HOLogic.all_const (fastype_of x) $ Term.lambda x t |
27 fun mk_all (x, t) = HOLogic.all_const (fastype_of x) $ Term.lambda x t |
32 |
28 |
33 |
29 |
34 (*** Basic HOLCF concepts ***) |
30 (*** Basic HOLCF concepts ***) |
35 |
31 |
36 fun mk_bottom T = Const (\<^const_name>\<open>bottom\<close>, T) |
32 fun mk_bottom T = \<^Const>\<open>bottom T\<close> |
37 |
33 |
38 fun below_const T = Const (\<^const_name>\<open>below\<close>, [T, T] ---> boolT) |
34 fun below_const T = \<^Const>\<open>below T\<close> |
39 fun mk_below (t, u) = below_const (fastype_of t) $ t $ u |
35 fun mk_below (t, u) = below_const (fastype_of t) $ t $ u |
40 |
36 |
41 fun mk_undef t = mk_eq (t, mk_bottom (fastype_of t)) |
37 fun mk_undef t = mk_eq (t, mk_bottom (fastype_of t)) |
42 |
38 |
43 fun mk_defined t = mk_not (mk_undef t) |
39 fun mk_defined t = mk_not (mk_undef t) |
44 |
40 |
45 fun mk_adm t = |
41 fun mk_adm t = |
46 Const (\<^const_name>\<open>adm\<close>, fastype_of t --> boolT) $ t |
42 let val T = Term.domain_type (fastype_of t) |
|
43 in \<^Const>\<open>adm T for t\<close> end |
47 |
44 |
48 fun mk_compact t = |
45 fun mk_compact t = |
49 Const (\<^const_name>\<open>compact\<close>, fastype_of t --> boolT) $ t |
46 let val T = fastype_of t |
|
47 in \<^Const>\<open>compact T for t\<close> end |
50 |
48 |
51 fun mk_cont t = |
49 fun mk_cont t = |
52 Const (\<^const_name>\<open>cont\<close>, fastype_of t --> boolT) $ t |
50 let val \<^Type>\<open>fun A B\<close> = fastype_of t |
|
51 in \<^Const>\<open>cont A B for t\<close> end |
53 |
52 |
54 fun mk_chain t = |
53 fun mk_chain t = |
55 Const (\<^const_name>\<open>chain\<close>, Term.fastype_of t --> boolT) $ t |
54 let val T = Term.range_type (Term.fastype_of t) |
|
55 in \<^Const>\<open>chain T for t\<close> end |
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>\<open>lub\<close>, mk_setT T --> T) |
|
61 val UNIV_const = \<^term>\<open>UNIV :: nat set\<close> |
60 val UNIV_const = \<^term>\<open>UNIV :: nat set\<close> |
62 val image_type = (natT --> T) --> mk_setT natT --> mk_setT T |
61 in \<^Const>\<open>lub T for \<open>\<^Const>\<open>image \<open>\<^Type>\<open>nat\<close>\<close> T for t UNIV_const\<close>\<close>\<close> end |
63 val image_const = Const (\<^const_name>\<open>image\<close>, image_type) |
|
64 in |
|
65 lub_const $ (image_const $ t $ UNIV_const) |
|
66 end |
|
67 |
62 |
68 |
63 |
69 (*** Continuous function space ***) |
64 (*** Continuous function space ***) |
70 |
65 |
71 fun mk_cfunT (T, U) = Type(\<^type_name>\<open>cfun\<close>, [T, U]) |
66 fun mk_cfunT (T, U) = \<^Type>\<open>cfun T U\<close> |
72 |
67 |
73 val (op ->>) = mk_cfunT |
68 val (op ->>) = mk_cfunT |
74 val (op -->>) = Library.foldr mk_cfunT |
69 val (op -->>) = Library.foldr mk_cfunT |
75 |
70 |
76 fun dest_cfunT (Type(\<^type_name>\<open>cfun\<close>, [T, U])) = (T, U) |
71 fun dest_cfunT \<^Type>\<open>cfun T U\<close> = (T, U) |
77 | dest_cfunT T = raise TYPE ("dest_cfunT", [T], []) |
72 | dest_cfunT T = raise TYPE ("dest_cfunT", [T], []) |
78 |
73 |
79 fun capply_const (S, T) = |
74 fun capply_const (S, T) = \<^Const>\<open>Rep_cfun S T\<close> |
80 Const(\<^const_name>\<open>Rep_cfun\<close>, (S ->> T) --> (S --> T)) |
75 fun cabs_const (S, T) = \<^Const>\<open>Abs_cfun S T\<close> |
81 |
|
82 fun cabs_const (S, T) = |
|
83 Const(\<^const_name>\<open>Abs_cfun\<close>, (S --> T) --> (S ->> T)) |
|
84 |
76 |
85 fun mk_cabs t = |
77 fun mk_cabs t = |
86 let val T = fastype_of t |
78 let val T = fastype_of t |
87 in cabs_const (Term.dest_funT T) $ t end |
79 in cabs_const (Term.dest_funT T) $ t end |
88 |
80 |
99 | big_lambdas (v::vs) rhs = big_lambda v (big_lambdas vs rhs) |
91 | big_lambdas (v::vs) rhs = big_lambda v (big_lambdas vs rhs) |
100 |
92 |
101 fun mk_capply (t, u) = |
93 fun mk_capply (t, u) = |
102 let val (S, T) = |
94 let val (S, T) = |
103 case fastype_of t of |
95 case fastype_of t of |
104 Type(\<^type_name>\<open>cfun\<close>, [S, T]) => (S, T) |
96 \<^Type>\<open>cfun S T\<close> => (S, T) |
105 | _ => raise TERM ("mk_capply " ^ ML_Syntax.print_list ML_Syntax.print_term [t, u], [t, u]) |
97 | _ => 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 |
98 in capply_const (S, T) $ t $ u end |
107 |
99 |
108 val (op `) = mk_capply |
100 val (op `) = mk_capply |
109 |
101 |
110 val list_ccomb : term * term list -> term = Library.foldl mk_capply |
102 val list_ccomb : term * term list -> term = Library.foldl mk_capply |
111 |
103 |
112 fun mk_ID T = Const (\<^const_name>\<open>ID\<close>, T ->> T) |
104 fun mk_ID T = \<^Const>\<open>ID T\<close> |
113 |
|
114 fun cfcomp_const (T, U, V) = |
|
115 Const (\<^const_name>\<open>cfcomp\<close>, (U ->> V) ->> (T ->> U) ->> (T ->> V)) |
|
116 |
105 |
117 fun mk_cfcomp (f, g) = |
106 fun mk_cfcomp (f, g) = |
118 let |
107 let |
119 val (U, V) = dest_cfunT (fastype_of f) |
108 val (U, V) = dest_cfunT (fastype_of f) |
120 val (T, U') = dest_cfunT (fastype_of g) |
109 val (T, U') = dest_cfunT (fastype_of g) |
121 in |
110 in |
122 if U = U' |
111 if U = U' |
123 then mk_capply (mk_capply (cfcomp_const (T, U, V), f), g) |
112 then mk_capply (mk_capply (\<^Const>\<open>cfcomp U V T\<close>, f), g) |
124 else raise TYPE ("mk_cfcomp", [U, U'], [f, g]) |
113 else raise TYPE ("mk_cfcomp", [U, U'], [f, g]) |
125 end |
114 end |
126 |
115 |
127 fun strictify_const T = Const (\<^const_name>\<open>strictify\<close>, T ->> T) |
116 fun mk_strictify t = |
128 fun mk_strictify t = strictify_const (fastype_of t) ` t |
117 let val (T, U) = dest_cfunT (fastype_of t) |
|
118 in \<^Const>\<open>strictify T U\<close> ` t end; |
129 |
119 |
130 fun mk_strict t = |
120 fun mk_strict t = |
131 let val (T, U) = dest_cfunT (fastype_of t) |
121 let val (T, U) = dest_cfunT (fastype_of t) |
132 in mk_eq (t ` mk_bottom T, mk_bottom U) end |
122 in mk_eq (t ` mk_bottom T, mk_bottom U) end |
133 |
123 |
152 HOLogic.mk_case_prod (Term.lambda v (lambda_tuple vs rhs)) |
142 HOLogic.mk_case_prod (Term.lambda v (lambda_tuple vs rhs)) |
153 |
143 |
154 |
144 |
155 (*** Lifted cpo type ***) |
145 (*** Lifted cpo type ***) |
156 |
146 |
157 fun mk_upT T = Type(\<^type_name>\<open>u\<close>, [T]) |
147 fun mk_upT T = \<^Type>\<open>u T\<close> |
158 |
148 |
159 fun dest_upT (Type(\<^type_name>\<open>u\<close>, [T])) = T |
149 fun dest_upT \<^Type>\<open>u T\<close> = T |
160 | dest_upT T = raise TYPE ("dest_upT", [T], []) |
150 | dest_upT T = raise TYPE ("dest_upT", [T], []) |
161 |
151 |
162 fun up_const T = Const(\<^const_name>\<open>up\<close>, T ->> mk_upT T) |
152 fun up_const T = \<^Const>\<open>up T\<close> |
163 |
153 |
164 fun mk_up t = up_const (fastype_of t) ` t |
154 fun mk_up t = up_const (fastype_of t) ` t |
165 |
155 |
166 fun fup_const (T, U) = |
156 fun fup_const (T, U) = \<^Const>\<open>fup T U\<close> |
167 Const(\<^const_name>\<open>fup\<close>, (T ->> U) ->> mk_upT T ->> U) |
|
168 |
157 |
169 fun mk_fup t = fup_const (dest_cfunT (fastype_of t)) ` t |
158 fun mk_fup t = fup_const (dest_cfunT (fastype_of t)) ` t |
170 |
159 |
171 fun from_up T = fup_const (T, T) ` mk_ID T |
160 fun from_up T = fup_const (T, T) ` mk_ID T |
172 |
161 |
173 |
162 |
174 (*** Lifted unit type ***) |
163 (*** Lifted unit type ***) |
175 |
164 |
176 val oneT = \<^typ>\<open>one\<close> |
165 val oneT = \<^typ>\<open>one\<close> |
177 |
166 |
178 fun one_case_const T = Const (\<^const_name>\<open>one_case\<close>, T ->> oneT ->> T) |
167 fun one_case_const T = \<^Const>\<open>one_case T\<close> |
179 fun mk_one_case t = one_case_const (fastype_of t) ` t |
168 fun mk_one_case t = one_case_const (fastype_of t) ` t |
180 |
169 |
181 |
170 |
182 (*** Strict product type ***) |
171 (*** Strict product type ***) |
183 |
172 |
184 fun mk_sprodT (T, U) = Type(\<^type_name>\<open>sprod\<close>, [T, U]) |
173 fun mk_sprodT (T, U) = \<^Type>\<open>sprod T U\<close> |
185 |
174 |
186 fun dest_sprodT (Type(\<^type_name>\<open>sprod\<close>, [T, U])) = (T, U) |
175 fun dest_sprodT \<^Type>\<open>sprod T U\<close> = (T, U) |
187 | dest_sprodT T = raise TYPE ("dest_sprodT", [T], []) |
176 | dest_sprodT T = raise TYPE ("dest_sprodT", [T], []) |
188 |
177 |
189 fun spair_const (T, U) = |
178 fun spair_const (T, U) = \<^Const>\<open>spair T U\<close> |
190 Const(\<^const_name>\<open>spair\<close>, T ->> U ->> mk_sprodT (T, U)) |
|
191 |
179 |
192 (* builds the expression (:t, u:) *) |
180 (* builds the expression (:t, u:) *) |
193 fun mk_spair (t, u) = |
181 fun mk_spair (t, u) = |
194 spair_const (fastype_of t, fastype_of u) ` t ` u |
182 spair_const (fastype_of t, fastype_of u) ` t ` u |
195 |
183 |
196 (* builds the expression (:t1,t2,..,tn:) *) |
184 (* builds the expression (:t1,t2,..,tn:) *) |
197 fun mk_stuple [] = \<^term>\<open>ONE\<close> |
185 fun mk_stuple [] = \<^term>\<open>ONE\<close> |
198 | mk_stuple (t::[]) = t |
186 | mk_stuple (t::[]) = t |
199 | mk_stuple (t::ts) = mk_spair (t, mk_stuple ts) |
187 | mk_stuple (t::ts) = mk_spair (t, mk_stuple ts) |
200 |
188 |
201 fun sfst_const (T, U) = |
189 fun sfst_const (T, U) = \<^Const>\<open>sfst T U\<close> |
202 Const(\<^const_name>\<open>sfst\<close>, mk_sprodT (T, U) ->> T) |
190 |
203 |
191 fun ssnd_const (T, U) = \<^Const>\<open>ssnd T U\<close> |
204 fun ssnd_const (T, U) = |
192 |
205 Const(\<^const_name>\<open>ssnd\<close>, mk_sprodT (T, U) ->> U) |
193 fun ssplit_const (T, U, V) = \<^Const>\<open>ssplit T U V\<close> |
206 |
|
207 fun ssplit_const (T, U, V) = |
|
208 Const (\<^const_name>\<open>ssplit\<close>, (T ->> U ->> V) ->> mk_sprodT (T, U) ->> V) |
|
209 |
194 |
210 fun mk_ssplit t = |
195 fun mk_ssplit t = |
211 let val (T, (U, V)) = apsnd dest_cfunT (dest_cfunT (fastype_of t)) |
196 let val (T, (U, V)) = apsnd dest_cfunT (dest_cfunT (fastype_of t)) |
212 in ssplit_const (T, U, V) ` t end |
197 in ssplit_const (T, U, V) ` t end |
213 |
198 |
214 |
199 |
215 (*** Strict sum type ***) |
200 (*** Strict sum type ***) |
216 |
201 |
217 fun mk_ssumT (T, U) = Type(\<^type_name>\<open>ssum\<close>, [T, U]) |
202 fun mk_ssumT (T, U) = \<^Type>\<open>ssum T U\<close> |
218 |
203 |
219 fun dest_ssumT (Type(\<^type_name>\<open>ssum\<close>, [T, U])) = (T, U) |
204 fun dest_ssumT \<^Type>\<open>ssum T U\<close> = (T, U) |
220 | dest_ssumT T = raise TYPE ("dest_ssumT", [T], []) |
205 | dest_ssumT T = raise TYPE ("dest_ssumT", [T], []) |
221 |
206 |
222 fun sinl_const (T, U) = Const(\<^const_name>\<open>sinl\<close>, T ->> mk_ssumT (T, U)) |
207 fun sinl_const (T, U) = \<^Const>\<open>sinl T U\<close> |
223 fun sinr_const (T, U) = Const(\<^const_name>\<open>sinr\<close>, U ->> mk_ssumT (T, U)) |
208 fun sinr_const (T, U) = \<^Const>\<open>sinr U T\<close> |
224 |
209 |
225 (* builds the list [sinl(t1), sinl(sinr(t2)), ... sinr(...sinr(tn))] *) |
210 (* builds the list [sinl(t1), sinl(sinr(t2)), ... sinr(...sinr(tn))] *) |
226 fun mk_sinjects ts = |
211 fun mk_sinjects ts = |
227 let |
212 let |
228 val Ts = map fastype_of ts |
213 val Ts = map fastype_of ts |