6 |
6 |
7 signature NOMINAL_LIBRARY = |
7 signature NOMINAL_LIBRARY = |
8 sig |
8 sig |
9 val last2: 'a list -> 'a * 'a |
9 val last2: 'a list -> 'a * 'a |
10 val order: ('a * 'a -> bool) -> 'a list -> ('a * 'b) list -> 'b list |
10 val order: ('a * 'a -> bool) -> 'a list -> ('a * 'b) list -> 'b list |
|
11 val remove_dups: ('a * 'a -> bool) -> 'a list -> 'a list |
11 |
12 |
12 val is_true: term -> bool |
13 val is_true: term -> bool |
13 |
14 |
14 val dest_listT: typ -> typ |
15 val dest_listT: typ -> typ |
15 val dest_fsetT: typ -> typ |
16 val dest_fsetT: typ -> typ |
45 val is_atom: Proof.context -> typ -> bool |
46 val is_atom: Proof.context -> typ -> bool |
46 val is_atom_set: Proof.context -> typ -> bool |
47 val is_atom_set: Proof.context -> typ -> bool |
47 val is_atom_fset: Proof.context -> typ -> bool |
48 val is_atom_fset: Proof.context -> typ -> bool |
48 val is_atom_list: Proof.context -> typ -> bool |
49 val is_atom_list: Proof.context -> typ -> bool |
49 |
50 |
|
51 val to_atom_set: term -> term |
|
52 val to_set_ty: typ -> term -> term |
|
53 val to_set: term -> term |
|
54 |
50 val setify_ty: Proof.context -> typ -> term -> term |
55 val setify_ty: Proof.context -> typ -> term -> term |
51 val setify: Proof.context -> term -> term |
56 val setify: Proof.context -> term -> term |
52 val listify_ty: Proof.context -> typ -> term -> term |
57 val listify_ty: Proof.context -> typ -> term -> term |
53 val listify: Proof.context -> term -> term |
58 val listify: Proof.context -> term -> term |
54 |
59 |
55 val fresh_ty: typ -> typ -> typ |
60 val fresh_star_ty: typ -> typ |
56 val fresh_star_const: typ -> typ -> term |
61 val fresh_star_const: typ -> term |
57 val mk_fresh_star_ty: typ -> typ -> term -> term -> term |
62 val mk_fresh_star_ty: typ -> term -> term -> term |
58 val mk_fresh_star: term -> term -> term |
63 val mk_fresh_star: term -> term -> term |
59 |
64 |
60 val supp_ty: typ -> typ |
65 val supp_ty: typ -> typ |
61 val supp_const: typ -> term |
66 val supp_const: typ -> term |
62 val mk_supp_ty: typ -> term -> term |
67 val mk_supp_ty: typ -> term -> term |
84 val fold_union: term list -> term |
89 val fold_union: term list -> term |
85 val fold_append: term list -> term |
90 val fold_append: term list -> term |
86 val mk_conj: term * term -> term |
91 val mk_conj: term * term -> term |
87 val fold_conj: term list -> term |
92 val fold_conj: term list -> term |
88 |
93 |
89 val to_set: term -> term |
|
90 |
|
91 (* fresh arguments for a term *) |
94 (* fresh arguments for a term *) |
92 val fresh_args: Proof.context -> term -> term list |
95 val fresh_args: Proof.context -> term -> term list |
93 |
96 |
94 (* datatype operations *) |
97 (* datatype operations *) |
95 type cns_info = (term * typ * typ list * bool list) list |
98 type cns_info = (term * typ * typ list * bool list) list |
119 |
122 |
120 (* orders an AList according to keys *) |
123 (* orders an AList according to keys *) |
121 fun order eq keys list = |
124 fun order eq keys list = |
122 map (the o AList.lookup eq list) keys |
125 map (the o AList.lookup eq list) keys |
123 |
126 |
|
127 fun remove_dups eq [] = [] |
|
128 | remove_dups eq (x::xs) = |
|
129 if (member eq xs x) |
|
130 then remove_dups eq xs |
|
131 else x::(remove_dups eq xs) |
|
132 |
|
133 |
124 fun last2 [] = raise Empty |
134 fun last2 [] = raise Empty |
125 | last2 [_] = raise Empty |
135 | last2 [_] = raise Empty |
126 | last2 [x, y] = (x, y) |
136 | last2 [x, y] = (x, y) |
127 | last2 (_ :: xs) = last2 xs |
137 | last2 (_ :: xs) = last2 xs |
128 |
138 |
204 |
214 |
205 fun mk_atom_set t = mk_atom_set_ty (fastype_of t) t |
215 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 |
216 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 |
217 fun mk_atom_list t = mk_atom_list_ty (fastype_of t) t |
208 |
218 |
|
219 (* coerces a list into a set *) |
|
220 fun to_atom_set t = @{term "set :: atom list => atom set"} $ t |
|
221 |
|
222 fun to_set_ty ty t = |
|
223 if ty = @{typ "atom list"} |
|
224 then to_atom_set t else t |
|
225 |
|
226 fun to_set t = to_set_ty (fastype_of t) t |
209 |
227 |
210 |
228 |
211 (* testing for concrete atom types *) |
229 (* testing for concrete atom types *) |
212 fun is_atom ctxt ty = |
230 fun is_atom ctxt ty = |
213 Sign.of_sort (ProofContext.theory_of ctxt) (ty, @{sort at_base}) |
231 Sign.of_sort (ProofContext.theory_of ctxt) (ty, @{sort at_base}) |
214 |
232 |
215 fun is_atom_set ctxt (Type ("fun", [t, @{typ bool}])) = is_atom ctxt t |
233 fun is_atom_set ctxt (Type ("fun", [ty, @{typ bool}])) = is_atom ctxt ty |
216 | is_atom_set _ _ = false; |
234 | is_atom_set _ _ = false; |
217 |
235 |
218 fun is_atom_fset ctxt (Type (@{type_name "fset"}, [t])) = is_atom ctxt t |
236 fun is_atom_fset ctxt (Type (@{type_name "fset"}, [ty])) = is_atom ctxt ty |
219 | is_atom_fset _ _ = false; |
237 | is_atom_fset _ _ = false; |
220 |
238 |
221 fun is_atom_list ctxt (Type (@{type_name "list"}, [t])) = is_atom ctxt t |
239 fun is_atom_list ctxt (Type (@{type_name "list"}, [ty])) = is_atom ctxt ty |
222 | is_atom_list _ _ = false |
240 | is_atom_list _ _ = false |
223 |
241 |
224 |
242 |
225 (* functions that coerces singletons, sets and fsets of concrete atoms |
243 (* functions that coerces singletons, sets and fsets of concrete atoms |
226 into sets of general atoms *) |
244 into sets of general atoms *) |
229 then HOLogic.mk_set @{typ atom} [mk_atom_ty ty t] |
247 then HOLogic.mk_set @{typ atom} [mk_atom_ty ty t] |
230 else if is_atom_set ctxt ty |
248 else if is_atom_set ctxt ty |
231 then mk_atom_set_ty ty t |
249 then mk_atom_set_ty ty t |
232 else if is_atom_fset ctxt ty |
250 else if is_atom_fset ctxt ty |
233 then mk_atom_fset_ty ty t |
251 then mk_atom_fset_ty ty t |
|
252 else if is_atom_list ctxt ty |
|
253 then to_atom_set (mk_atom_list_ty ty t) |
234 else raise TERM ("setify", [t]) |
254 else raise TERM ("setify", [t]) |
|
255 |
235 |
256 |
236 (* functions that coerces singletons and lists of concrete atoms |
257 (* functions that coerces singletons and lists of concrete atoms |
237 into lists of general atoms *) |
258 into lists of general atoms *) |
238 fun listify_ty ctxt ty t = |
259 fun listify_ty ctxt ty t = |
239 if is_atom ctxt ty |
260 if is_atom ctxt ty |
243 else raise TERM ("listify", [t]) |
264 else raise TERM ("listify", [t]) |
244 |
265 |
245 fun setify ctxt t = setify_ty ctxt (fastype_of t) t |
266 fun setify ctxt t = setify_ty ctxt (fastype_of t) t |
246 fun listify ctxt t = listify_ty ctxt (fastype_of t) t |
267 fun listify ctxt t = listify_ty ctxt (fastype_of t) t |
247 |
268 |
248 fun fresh_ty ty1 ty2 = [ty1, ty2] ---> @{typ bool} |
269 fun fresh_star_ty ty = [@{typ "atom set"}, ty] ---> @{typ bool} |
249 fun fresh_star_const ty1 ty2 = Const (@{const_name fresh_star}, fresh_ty ty1 ty2) |
270 fun fresh_star_const ty = Const (@{const_name fresh_star}, fresh_star_ty ty) |
250 fun mk_fresh_star_ty ty1 ty2 t1 t2 = fresh_star_const ty1 ty2 $ t1 $ t2 |
271 fun mk_fresh_star_ty ty t1 t2 = fresh_star_const ty $ t1 $ t2 |
251 fun mk_fresh_star t1 t2 = mk_fresh_star_ty (fastype_of t1) (fastype_of t2) t1 t2 |
272 fun mk_fresh_star t1 t2 = mk_fresh_star_ty (fastype_of t2) t1 t2 |
252 |
273 |
253 fun supp_ty ty = ty --> @{typ "atom set"}; |
274 fun supp_ty ty = ty --> @{typ "atom set"}; |
254 fun supp_const ty = Const (@{const_name supp}, supp_ty ty) |
275 fun supp_const ty = Const (@{const_name supp}, supp_ty ty) |
255 fun mk_supp_ty ty t = supp_const ty $ t |
276 fun mk_supp_ty ty t = supp_const ty $ t |
256 fun mk_supp t = mk_supp_ty (fastype_of t) t |
277 fun mk_supp t = mk_supp_ty (fastype_of t) t |
298 fun mk_conj (t1, @{term "True"}) = t1 |
319 fun mk_conj (t1, @{term "True"}) = t1 |
299 | mk_conj (@{term "True"}, t2) = t2 |
320 | mk_conj (@{term "True"}, t2) = t2 |
300 | mk_conj (t1, t2) = HOLogic.mk_conj (t1, t2) |
321 | mk_conj (t1, t2) = HOLogic.mk_conj (t1, t2) |
301 |
322 |
302 fun fold_conj trms = fold_rev (curry mk_conj) trms @{term "True"} |
323 fun fold_conj trms = fold_rev (curry mk_conj) trms @{term "True"} |
303 |
|
304 |
|
305 (* coerces a list into a set *) |
|
306 fun to_set t = |
|
307 if fastype_of t = @{typ "atom list"} |
|
308 then @{term "set :: atom list => atom set"} $ t |
|
309 else t |
|
310 |
|
311 |
|
312 |
324 |
313 |
325 |
314 (* produces fresh arguments for a term *) |
326 (* produces fresh arguments for a term *) |
315 |
327 |
316 fun fresh_args ctxt f = |
328 fun fresh_args ctxt f = |