5 *) |
5 *) |
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 split_last2: 'a list -> 'a list * 'a * 'a |
10 val order: ('a * 'a -> bool) -> 'a list -> ('a * 'b) list -> 'b list |
11 val order: ('a * 'a -> bool) -> 'a list -> ('a * 'b) list -> 'b list |
|
12 val order_default: ('a * 'a -> bool) -> 'b -> 'a list -> ('a * 'b) list -> 'b list |
11 val remove_dups: ('a * 'a -> bool) -> 'a list -> 'a list |
13 val remove_dups: ('a * 'a -> bool) -> 'a list -> 'a list |
12 val map4: ('a -> 'b -> 'c -> 'd -> 'e) -> 'a list -> 'b list -> 'c list -> 'd list -> 'e list |
14 val map4: ('a -> 'b -> 'c -> 'd -> 'e) -> 'a list -> 'b list -> 'c list -> 'd list -> 'e list |
13 val split_filter: ('a -> bool) -> 'a list -> 'a list * 'a list |
15 val split_filter: ('a -> bool) -> 'a list -> 'a list * 'a list |
14 val fold_left: ('a * 'a -> 'a) -> 'a list -> 'a -> 'a |
16 val fold_left: ('a * 'a -> 'a) -> 'a list -> 'a -> 'a |
15 |
17 |
18 val dest_listT: typ -> typ |
20 val dest_listT: typ -> typ |
19 val dest_fsetT: typ -> typ |
21 val dest_fsetT: typ -> typ |
20 |
22 |
21 val mk_id: term -> term |
23 val mk_id: term -> term |
22 val mk_all: (string * typ) -> term -> term |
24 val mk_all: (string * typ) -> term -> term |
|
25 val mk_All: (string * typ) -> term -> term |
23 |
26 |
24 val sum_case_const: typ -> typ -> typ -> term |
27 val sum_case_const: typ -> typ -> typ -> term |
25 val mk_sum_case: term -> term -> term |
28 val mk_sum_case: term -> term -> term |
26 |
29 |
27 val mk_minus: term -> term |
30 val mk_minus: term -> term |
28 val mk_plus: term -> term -> term |
31 val mk_plus: term -> term -> term |
29 |
32 |
30 val perm_ty: typ -> typ |
33 val perm_ty: typ -> typ |
|
34 val perm_const: typ -> term |
31 val mk_perm_ty: typ -> term -> term -> term |
35 val mk_perm_ty: typ -> term -> term -> term |
32 val mk_perm: term -> term -> term |
36 val mk_perm: term -> term -> term |
33 val dest_perm: term -> term * term |
37 val dest_perm: term -> term * term |
34 |
38 |
35 val mk_sort_of: term -> term |
39 val mk_sort_of: term -> term |
134 |
138 |
135 |
139 |
136 structure Nominal_Library: NOMINAL_LIBRARY = |
140 structure Nominal_Library: NOMINAL_LIBRARY = |
137 struct |
141 struct |
138 |
142 |
139 (* orders an AList according to keys *) |
143 (* orders an AList according to keys - every key needs to be there *) |
140 fun order eq keys list = |
144 fun order eq keys list = |
141 map (the o AList.lookup eq list) keys |
145 map (the o AList.lookup eq list) keys |
|
146 |
|
147 (* orders an AList according to keys - returns default for non-existing keys *) |
|
148 fun order_default eq default keys list = |
|
149 map (the_default default o AList.lookup eq list) keys |
142 |
150 |
143 (* remove duplicates *) |
151 (* remove duplicates *) |
144 fun remove_dups eq [] = [] |
152 fun remove_dups eq [] = [] |
145 | remove_dups eq (x :: xs) = |
153 | remove_dups eq (x :: xs) = |
146 if member eq xs x |
154 if member eq xs x |
149 |
157 |
150 fun last2 [] = raise Empty |
158 fun last2 [] = raise Empty |
151 | last2 [_] = raise Empty |
159 | last2 [_] = raise Empty |
152 | last2 [x, y] = (x, y) |
160 | last2 [x, y] = (x, y) |
153 | last2 (_ :: xs) = last2 xs |
161 | last2 (_ :: xs) = last2 xs |
|
162 |
|
163 fun split_last2 xs = |
|
164 let |
|
165 val (xs', x) = split_last xs |
|
166 val (xs'', y) = split_last xs' |
|
167 in |
|
168 (xs'', y, x) |
|
169 end |
154 |
170 |
155 fun map4 _ [] [] [] [] = [] |
171 fun map4 _ [] [] [] [] = [] |
156 | map4 f (x :: xs) (y :: ys) (z :: zs) (u :: us) = f x y z u :: map4 f xs ys zs us |
172 | map4 f (x :: xs) (y :: ys) (z :: zs) (u :: us) = f x y z u :: map4 f xs ys zs us |
157 |
173 |
158 fun split_filter f [] = ([], []) |
174 fun split_filter f [] = ([], []) |
184 |
200 |
185 fun mk_id trm = HOLogic.id_const (fastype_of trm) $ trm |
201 fun mk_id trm = HOLogic.id_const (fastype_of trm) $ trm |
186 |
202 |
187 fun mk_all (a, T) t = Term.all T $ Abs (a, T, t) |
203 fun mk_all (a, T) t = Term.all T $ Abs (a, T, t) |
188 |
204 |
|
205 fun mk_All (a, T) t = HOLogic.all_const T $ Abs (a, T, t) |
|
206 |
189 fun sum_case_const ty1 ty2 ty3 = |
207 fun sum_case_const ty1 ty2 ty3 = |
190 Const (@{const_name sum_case}, [ty1 --> ty3, ty2 --> ty3, Type (@{type_name sum}, [ty1, ty2])] ---> ty3) |
208 Const (@{const_name sum_case}, [ty1 --> ty3, ty2 --> ty3, Type (@{type_name sum}, [ty1, ty2])] ---> ty3) |
191 |
209 |
192 fun mk_sum_case trm1 trm2 = |
210 fun mk_sum_case trm1 trm2 = |
193 let |
211 let |
202 fun mk_minus p = @{term "uminus::perm => perm"} $ p |
220 fun mk_minus p = @{term "uminus::perm => perm"} $ p |
203 |
221 |
204 fun mk_plus p q = @{term "plus::perm => perm => perm"} $ p $ q |
222 fun mk_plus p q = @{term "plus::perm => perm => perm"} $ p $ q |
205 |
223 |
206 fun perm_ty ty = @{typ "perm"} --> ty --> ty |
224 fun perm_ty ty = @{typ "perm"} --> ty --> ty |
207 fun mk_perm_ty ty p trm = Const (@{const_name "permute"}, perm_ty ty) $ p $ trm |
225 fun perm_const ty = Const (@{const_name "permute"}, perm_ty ty) |
|
226 fun mk_perm_ty ty p trm = perm_const ty $ p $ trm |
208 fun mk_perm p trm = mk_perm_ty (fastype_of trm) p trm |
227 fun mk_perm p trm = mk_perm_ty (fastype_of trm) p trm |
209 |
228 |
210 fun dest_perm (Const (@{const_name "permute"}, _) $ p $ t) = (p, t) |
229 fun dest_perm (Const (@{const_name "permute"}, _) $ p $ t) = (p, t) |
211 | dest_perm t = raise TERM ("dest_perm", [t]); |
230 | dest_perm t = raise TERM ("dest_perm", [t]); |
212 |
231 |