15 val dest_listT: typ -> typ |
15 val dest_listT: typ -> typ |
16 val dest_fsetT: typ -> typ |
16 val dest_fsetT: typ -> typ |
17 |
17 |
18 val mk_id: term -> term |
18 val mk_id: term -> term |
19 val mk_all: (string * typ) -> term -> term |
19 val mk_all: (string * typ) -> term -> term |
20 |
|
21 val size_const: typ -> term |
|
22 |
20 |
23 val sum_case_const: typ -> typ -> typ -> term |
21 val sum_case_const: typ -> typ -> typ -> term |
24 val mk_sum_case: term -> term -> term |
22 val mk_sum_case: term -> term -> term |
25 |
23 |
26 val mk_minus: term -> term |
24 val mk_minus: term -> term |
47 val is_atom: Proof.context -> typ -> bool |
45 val is_atom: Proof.context -> typ -> bool |
48 val is_atom_set: Proof.context -> typ -> bool |
46 val is_atom_set: Proof.context -> typ -> bool |
49 val is_atom_fset: Proof.context -> typ -> bool |
47 val is_atom_fset: Proof.context -> typ -> bool |
50 val is_atom_list: Proof.context -> typ -> bool |
48 val is_atom_list: Proof.context -> typ -> bool |
51 |
49 |
52 val to_atom_set: term -> term |
|
53 val to_set_ty: typ -> term -> term |
50 val to_set_ty: typ -> term -> term |
54 val to_set: term -> term |
51 val to_set: term -> term |
55 |
52 |
|
53 val atomify_ty: Proof.context -> typ -> term -> term |
|
54 val atomify: Proof.context -> term -> term |
56 val setify_ty: Proof.context -> typ -> term -> term |
55 val setify_ty: Proof.context -> typ -> term -> term |
57 val setify: Proof.context -> term -> term |
56 val setify: Proof.context -> term -> term |
58 val listify_ty: Proof.context -> typ -> term -> term |
57 val listify_ty: Proof.context -> typ -> term -> term |
59 val listify: Proof.context -> term -> term |
58 val listify: Proof.context -> term -> term |
60 |
59 |
123 |
122 |
124 (* orders an AList according to keys *) |
123 (* orders an AList according to keys *) |
125 fun order eq keys list = |
124 fun order eq keys list = |
126 map (the o AList.lookup eq list) keys |
125 map (the o AList.lookup eq list) keys |
127 |
126 |
|
127 (* remove duplicates *) |
128 fun remove_dups eq [] = [] |
128 fun remove_dups eq [] = [] |
129 | remove_dups eq (x::xs) = |
129 | remove_dups eq (x :: xs) = |
130 if (member eq xs x) |
130 if member eq xs x |
131 then remove_dups eq xs |
131 then remove_dups eq xs |
132 else x::(remove_dups eq xs) |
132 else x :: remove_dups eq xs |
133 |
|
134 |
133 |
135 fun last2 [] = raise Empty |
134 fun last2 [] = raise Empty |
136 | last2 [_] = raise Empty |
135 | last2 [_] = raise Empty |
137 | last2 [x, y] = (x, y) |
136 | last2 [x, y] = (x, y) |
138 | last2 (_ :: xs) = last2 xs |
137 | last2 (_ :: xs) = last2 xs |
139 |
138 |
140 |
|
141 fun is_true @{term "Trueprop True"} = true |
139 fun is_true @{term "Trueprop True"} = true |
142 | is_true _ = false |
140 | is_true _ = false |
143 |
141 |
144 fun dest_listT (Type (@{type_name list}, [T])) = T |
142 fun dest_listT (Type (@{type_name list}, [T])) = T |
145 | dest_listT T = raise TYPE ("dest_listT: list type expected", [T], []) |
143 | dest_listT T = raise TYPE ("dest_listT: list type expected", [T], []) |
146 |
144 |
147 fun dest_fsetT (Type (@{type_name fset}, [T])) = T |
145 fun dest_fsetT (Type (@{type_name fset}, [T])) = T |
148 | dest_fsetT T = raise TYPE ("dest_fsetT: fset type expected", [T], []); |
146 | dest_fsetT T = raise TYPE ("dest_fsetT: fset type expected", [T], []); |
|
147 |
149 |
148 |
150 |
149 |
151 fun mk_id trm = |
150 fun mk_id trm = |
152 let |
151 let |
153 val ty = fastype_of trm |
152 val ty = fastype_of trm |
155 Const (@{const_name id}, ty --> ty) $ trm |
154 Const (@{const_name id}, ty --> ty) $ trm |
156 end |
155 end |
157 |
156 |
158 fun mk_all (a, T) t = Term.all T $ Abs (a, T, t) |
157 fun mk_all (a, T) t = Term.all T $ Abs (a, T, t) |
159 |
158 |
160 |
|
161 fun size_const ty = Const (@{const_name size}, ty --> @{typ nat}) |
|
162 |
|
163 fun sum_case_const ty1 ty2 ty3 = |
159 fun sum_case_const ty1 ty2 ty3 = |
164 Const (@{const_name sum_case}, [ty1 --> ty3, ty2 --> ty3, Type (@{type_name sum}, [ty1, ty2])] ---> ty3) |
160 Const (@{const_name sum_case}, [ty1 --> ty3, ty2 --> ty3, Type (@{type_name sum}, [ty1, ty2])] ---> ty3) |
|
161 |
165 fun mk_sum_case trm1 trm2 = |
162 fun mk_sum_case trm1 trm2 = |
166 let |
163 let |
167 val ([ty1], ty3) = strip_type (fastype_of trm1) |
164 val ([ty1], ty3) = strip_type (fastype_of trm1) |
168 val ty2 = domain_type (fastype_of trm2) |
165 val ty2 = domain_type (fastype_of trm2) |
169 in |
166 in |
190 fun mk_atom_ty ty t = atom_const ty $ t; |
187 fun mk_atom_ty ty t = atom_const ty $ t; |
191 fun mk_atom t = mk_atom_ty (fastype_of t) t; |
188 fun mk_atom t = mk_atom_ty (fastype_of t) t; |
192 |
189 |
193 fun mk_atom_set_ty ty t = |
190 fun mk_atom_set_ty ty t = |
194 let |
191 let |
195 val atom_ty = HOLogic.dest_setT ty --> @{typ "atom"}; |
192 val atom_ty = HOLogic.dest_setT ty |
196 val img_ty = atom_ty --> ty --> @{typ "atom set"}; |
193 val img_ty = (atom_ty --> @{typ atom}) --> ty --> @{typ "atom set"}; |
197 in |
194 in |
198 Const (@{const_name image}, img_ty) $ mk_atom_ty atom_ty t |
195 Const (@{const_name image}, img_ty) $ atom_const atom_ty $ t |
199 end |
196 end |
200 |
197 |
201 fun mk_atom_fset_ty ty t = |
198 fun mk_atom_fset_ty ty t = |
202 let |
199 let |
203 val atom_ty = dest_fsetT ty |
200 val atom_ty = dest_fsetT ty |
204 val fmap_ty = (atom_ty --> @{typ atom}) --> ty --> @{typ "atom fset"}; |
201 val fmap_ty = (atom_ty --> @{typ atom}) --> ty --> @{typ "atom fset"}; |
205 val fset = @{term "fset :: atom fset => atom set"} |
202 in |
206 in |
203 Const (@{const_name map_fset}, fmap_ty) $ atom_const atom_ty $ t |
207 fset $ (Const (@{const_name map_fset}, fmap_ty) $ (atom_const atom_ty) $ t) |
|
208 end |
204 end |
209 |
205 |
210 fun mk_atom_list_ty ty t = |
206 fun mk_atom_list_ty ty t = |
211 let |
207 let |
212 val atom_ty = dest_listT ty |
208 val atom_ty = dest_listT ty |
213 val map_ty = (atom_ty --> @{typ atom}) --> ty --> @{typ "atom list"} |
209 val map_ty = (atom_ty --> @{typ atom}) --> ty --> @{typ "atom list"} |
214 in |
210 in |
215 Const (@{const_name map}, map_ty) $ (atom_const atom_ty) $ t |
211 Const (@{const_name map}, map_ty) $ atom_const atom_ty $ t |
216 end |
212 end |
217 |
213 |
218 fun mk_atom_set t = mk_atom_set_ty (fastype_of t) t |
214 fun mk_atom_set t = mk_atom_set_ty (fastype_of t) t |
219 fun mk_atom_fset t = mk_atom_fset_ty (fastype_of t) t |
215 fun mk_atom_fset t = mk_atom_fset_ty (fastype_of t) t |
220 fun mk_atom_list t = mk_atom_list_ty (fastype_of t) t |
216 fun mk_atom_list t = mk_atom_list_ty (fastype_of t) t |
221 |
217 |
222 (* coerces a list into a set *) |
218 (* coerces a list into a set *) |
223 fun to_atom_set t = @{term "set :: atom list => atom set"} $ t |
|
224 |
219 |
225 fun to_set_ty ty t = |
220 fun to_set_ty ty t = |
226 if ty = @{typ "atom list"} |
221 case ty of |
227 then to_atom_set t else t |
222 @{typ "atom list"} => @{term "set :: atom list => atom set"} $ t |
|
223 | @{typ "atom fset"} => @{term "fset :: atom fset => atom set"} $ t |
|
224 | _ => t |
228 |
225 |
229 fun to_set t = to_set_ty (fastype_of t) t |
226 fun to_set t = to_set_ty (fastype_of t) t |
230 |
227 |
231 |
228 |
232 (* testing for concrete atom types *) |
229 (* testing for concrete atom types *) |
241 |
238 |
242 fun is_atom_list ctxt (Type (@{type_name "list"}, [ty])) = is_atom ctxt ty |
239 fun is_atom_list ctxt (Type (@{type_name "list"}, [ty])) = is_atom ctxt ty |
243 | is_atom_list _ _ = false |
240 | is_atom_list _ _ = false |
244 |
241 |
245 |
242 |
246 (* functions that coerces singletons, sets and fsets of concrete atoms |
243 (* functions that coerce singletons, sets, fsets and lists of concrete |
247 into sets of general atoms *) |
244 atoms into general atoms sets / lists *) |
|
245 fun atomify_ty ctxt ty t = |
|
246 if is_atom ctxt ty |
|
247 then mk_atom_ty ty t |
|
248 else if is_atom_set ctxt ty |
|
249 then mk_atom_set_ty ty t |
|
250 else if is_atom_fset ctxt ty |
|
251 then mk_atom_fset_ty ty t |
|
252 else if is_atom_list ctxt ty |
|
253 then mk_atom_list_ty ty t |
|
254 else raise TERM ("atomify", [t]) |
|
255 |
248 fun setify_ty ctxt ty t = |
256 fun setify_ty ctxt ty t = |
249 if is_atom ctxt ty |
257 if is_atom ctxt ty |
250 then HOLogic.mk_set @{typ atom} [mk_atom_ty ty t] |
258 then HOLogic.mk_set @{typ atom} [mk_atom_ty ty t] |
251 else if is_atom_set ctxt ty |
259 else if is_atom_set ctxt ty |
252 then mk_atom_set_ty ty t |
260 then mk_atom_set_ty ty t |
253 else if is_atom_fset ctxt ty |
261 else if is_atom_fset ctxt ty |
254 then mk_atom_fset_ty ty t |
262 then @{term "fset :: atom fset => atom set"} $ mk_atom_fset_ty ty t |
255 else if is_atom_list ctxt ty |
263 else if is_atom_list ctxt ty |
256 then to_atom_set (mk_atom_list_ty ty t) |
264 then @{term "set :: atom list => atom set"} $ mk_atom_list_ty ty t |
257 else raise TERM ("setify", [t]) |
265 else raise TERM ("setify", [t]) |
258 |
266 |
259 |
|
260 (* functions that coerces singletons and lists of concrete atoms |
|
261 into lists of general atoms *) |
|
262 fun listify_ty ctxt ty t = |
267 fun listify_ty ctxt ty t = |
263 if is_atom ctxt ty |
268 if is_atom ctxt ty |
264 then HOLogic.mk_list @{typ atom} [mk_atom_ty ty t] |
269 then HOLogic.mk_list @{typ atom} [mk_atom_ty ty t] |
265 else if is_atom_list ctxt ty |
270 else if is_atom_list ctxt ty |
266 then mk_atom_list_ty ty t |
271 then mk_atom_list_ty ty t |
267 else raise TERM ("listify", [t]) |
272 else raise TERM ("listify", [t]) |
268 |
273 |
269 fun setify ctxt t = setify_ty ctxt (fastype_of t) t |
274 fun atomify ctxt t = atomify_ty ctxt (fastype_of t) t |
|
275 fun setify ctxt t = setify_ty ctxt (fastype_of t) t |
270 fun listify ctxt t = listify_ty ctxt (fastype_of t) t |
276 fun listify ctxt t = listify_ty ctxt (fastype_of t) t |
271 |
277 |
272 fun fresh_star_ty ty = [@{typ "atom set"}, ty] ---> @{typ bool} |
278 fun fresh_star_ty ty = [@{typ "atom set"}, ty] ---> @{typ bool} |
273 fun fresh_star_const ty = Const (@{const_name fresh_star}, fresh_star_ty ty) |
279 fun fresh_star_const ty = Const (@{const_name fresh_star}, fresh_star_ty ty) |
274 fun mk_fresh_star_ty ty t1 t2 = fresh_star_const ty $ t1 $ t2 |
280 fun mk_fresh_star_ty ty t1 t2 = fresh_star_const ty $ t1 $ t2 |
420 case T of |
426 case T of |
421 (Type (@{type_name Sum_Type.sum}, [fT, sT])) => |
427 (Type (@{type_name Sum_Type.sum}, [fT, sT])) => |
422 SumTree.mk_sumcase fT sT natT (mk_size_measure fT) (mk_size_measure sT) |
428 SumTree.mk_sumcase fT sT natT (mk_size_measure fT) (mk_size_measure sT) |
423 | (Type (@{type_name Product_Type.prod}, [fT, sT])) => |
429 | (Type (@{type_name Product_Type.prod}, [fT, sT])) => |
424 prod_size_const fT sT $ (mk_size_measure fT) $ (mk_size_measure sT) |
430 prod_size_const fT sT $ (mk_size_measure fT) $ (mk_size_measure sT) |
425 | _ => size_const T |
431 | _ => HOLogic.size_const T |
426 |
432 |
427 fun mk_measure_trm T = |
433 fun mk_measure_trm T = |
428 HOLogic.dest_setT T |
434 HOLogic.dest_setT T |
429 |> fst o HOLogic.dest_prodT |
435 |> fst o HOLogic.dest_prodT |
430 |> mk_size_measure |
436 |> mk_size_measure |