31 val mk_sort_of: term -> term |
32 val mk_sort_of: term -> term |
32 val atom_ty: typ -> typ |
33 val atom_ty: typ -> typ |
33 val atom_const: typ -> term |
34 val atom_const: typ -> term |
34 val mk_atom_ty: typ -> term -> term |
35 val mk_atom_ty: typ -> term -> term |
35 val mk_atom: term -> term |
36 val mk_atom: term -> term |
|
37 |
|
38 val mk_atom_set_ty: typ -> term -> term |
|
39 val mk_atom_set: term -> term |
|
40 val mk_atom_fset_ty: typ -> term -> term |
|
41 val mk_atom_fset: term -> term |
|
42 val mk_atom_list_ty: typ -> term -> term |
|
43 val mk_atom_list: term -> term |
|
44 |
|
45 val is_atom: Proof.context -> typ -> bool |
|
46 val is_atom_set: Proof.context -> typ -> bool |
|
47 val is_atom_fset: Proof.context -> typ -> bool |
|
48 val is_atom_list: Proof.context -> typ -> bool |
|
49 |
|
50 val setify_ty: Proof.context -> typ -> term -> term |
|
51 val setify: Proof.context -> term -> term |
|
52 val listify_ty: Proof.context -> typ -> term -> term |
|
53 val listify: Proof.context -> term -> term |
|
54 |
|
55 val fresh_ty: typ -> typ -> typ |
|
56 val fresh_star_const: typ -> typ -> term |
|
57 val mk_fresh_star_ty: typ -> typ -> term -> term -> term |
|
58 val mk_fresh_star: term -> term -> term |
36 |
59 |
37 val supp_ty: typ -> typ |
60 val supp_ty: typ -> typ |
38 val supp_const: typ -> term |
61 val supp_const: typ -> term |
39 val mk_supp_ty: typ -> term -> term |
62 val mk_supp_ty: typ -> term -> term |
40 val mk_supp: term -> term |
63 val mk_supp: term -> term |
108 | is_true _ = false |
131 | is_true _ = false |
109 |
132 |
110 fun dest_listT (Type (@{type_name list}, [T])) = T |
133 fun dest_listT (Type (@{type_name list}, [T])) = T |
111 | dest_listT T = raise TYPE ("dest_listT: list type expected", [T], []) |
134 | dest_listT T = raise TYPE ("dest_listT: list type expected", [T], []) |
112 |
135 |
|
136 fun dest_fsetT (Type (@{type_name fset}, [T])) = T |
|
137 | dest_fsetT T = raise TYPE ("dest_fsetT: fset type expected", [T], []); |
|
138 |
|
139 |
113 fun mk_id trm = |
140 fun mk_id trm = |
114 let |
141 let |
115 val ty = fastype_of trm |
142 val ty = fastype_of trm |
116 in |
143 in |
117 Const (@{const_name id}, ty --> ty) $ trm |
144 Const (@{const_name id}, ty --> ty) $ trm |
147 |
174 |
148 fun atom_ty ty = ty --> @{typ "atom"}; |
175 fun atom_ty ty = ty --> @{typ "atom"}; |
149 fun atom_const ty = Const (@{const_name "atom"}, atom_ty ty) |
176 fun atom_const ty = Const (@{const_name "atom"}, atom_ty ty) |
150 fun mk_atom_ty ty t = atom_const ty $ t; |
177 fun mk_atom_ty ty t = atom_const ty $ t; |
151 fun mk_atom t = mk_atom_ty (fastype_of t) t; |
178 fun mk_atom t = mk_atom_ty (fastype_of t) t; |
|
179 |
|
180 fun mk_atom_set_ty ty t = |
|
181 let |
|
182 val atom_ty = HOLogic.dest_setT ty --> @{typ "atom"}; |
|
183 val img_ty = atom_ty --> ty --> @{typ "atom set"}; |
|
184 in |
|
185 Const (@{const_name image}, img_ty) $ mk_atom_ty atom_ty t |
|
186 end |
|
187 |
|
188 fun mk_atom_fset_ty ty t = |
|
189 let |
|
190 val atom_ty = dest_fsetT ty |
|
191 val fmap_ty = (atom_ty --> @{typ atom}) --> ty --> @{typ "atom fset"}; |
|
192 val fset = @{term "fset :: atom fset => atom set"} |
|
193 in |
|
194 fset $ (Const (@{const_name map_fset}, fmap_ty) $ (atom_const atom_ty) $ t) |
|
195 end |
|
196 |
|
197 fun mk_atom_list_ty ty t = |
|
198 let |
|
199 val atom_ty = dest_listT ty |
|
200 val map_ty = (atom_ty --> @{typ atom}) --> ty --> @{typ "atom list"} |
|
201 in |
|
202 Const (@{const_name map}, map_ty) $ (atom_const atom_ty) $ t |
|
203 end |
|
204 |
|
205 fun mk_atom_set t = mk_atom_set_ty (fastype_of t) t |
|
206 fun mk_atom_fset t = mk_atom_fset_ty (fastype_of t) t |
|
207 fun mk_atom_list t = mk_atom_list_ty (fastype_of t) t |
|
208 |
|
209 |
|
210 |
|
211 (* testing for concrete atom types *) |
|
212 fun is_atom ctxt ty = |
|
213 Sign.of_sort (ProofContext.theory_of ctxt) (ty, @{sort at_base}) |
|
214 |
|
215 fun is_atom_set ctxt (Type ("fun", [t, @{typ bool}])) = is_atom ctxt t |
|
216 | is_atom_set _ _ = false; |
|
217 |
|
218 fun is_atom_fset ctxt (Type (@{type_name "fset"}, [t])) = is_atom ctxt t |
|
219 | is_atom_fset _ _ = false; |
|
220 |
|
221 fun is_atom_list ctxt (Type (@{type_name "list"}, [t])) = is_atom ctxt t |
|
222 | is_atom_list _ _ = false |
|
223 |
|
224 |
|
225 (* functions that coerces singletons, sets and fsets of concrete atoms |
|
226 into sets of general atoms *) |
|
227 fun setify_ty ctxt ty t = |
|
228 if is_atom ctxt ty |
|
229 then HOLogic.mk_set @{typ atom} [mk_atom_ty ty t] |
|
230 else if is_atom_set ctxt ty |
|
231 then mk_atom_set_ty ty t |
|
232 else if is_atom_fset ctxt ty |
|
233 then mk_atom_fset_ty ty t |
|
234 else raise TERM ("setify", [t]) |
|
235 |
|
236 (* functions that coerces singletons and lists of concrete atoms |
|
237 into lists of general atoms *) |
|
238 fun listify_ty ctxt ty t = |
|
239 if is_atom ctxt ty |
|
240 then HOLogic.mk_list @{typ atom} [mk_atom_ty ty t] |
|
241 else if is_atom_list ctxt ty |
|
242 then mk_atom_list_ty ty t |
|
243 else raise TERM ("listify", [t]) |
|
244 |
|
245 fun setify ctxt t = setify_ty ctxt (fastype_of t) t |
|
246 fun listify ctxt t = listify_ty ctxt (fastype_of t) t |
|
247 |
|
248 fun fresh_ty ty1 ty2 = [ty1, ty2] ---> @{typ bool} |
|
249 fun fresh_star_const ty1 ty2 = Const (@{const_name fresh_star}, fresh_ty ty1 ty2) |
|
250 fun mk_fresh_star_ty ty1 ty2 t1 t2 = fresh_star_const ty1 ty2 $ t1 $ t2 |
|
251 fun mk_fresh_star t1 t2 = mk_fresh_star_ty (fastype_of t1) (fastype_of t2) t1 t2 |
152 |
252 |
153 fun supp_ty ty = ty --> @{typ "atom set"}; |
253 fun supp_ty ty = ty --> @{typ "atom set"}; |
154 fun supp_const ty = Const (@{const_name supp}, supp_ty ty) |
254 fun supp_const ty = Const (@{const_name supp}, supp_ty ty) |
155 fun mk_supp_ty ty t = supp_const ty $ t |
255 fun mk_supp_ty ty t = supp_const ty $ t |
156 fun mk_supp t = mk_supp_ty (fastype_of t) t |
256 fun mk_supp t = mk_supp_ty (fastype_of t) t |