21 val order_default: ('a * 'a -> bool) -> 'b -> 'a list -> ('a * 'b) list -> 'b list |
22 val order_default: ('a * 'a -> bool) -> 'b -> 'a list -> ('a * 'b) list -> 'b list |
22 val remove_dups: ('a * 'a -> bool) -> 'a list -> 'a list |
23 val remove_dups: ('a * 'a -> bool) -> 'a list -> 'a list |
23 val map4: ('a -> 'b -> 'c -> 'd -> 'e) -> 'a list -> 'b list -> 'c list -> 'd list -> 'e list |
24 val map4: ('a -> 'b -> 'c -> 'd -> 'e) -> 'a list -> 'b list -> 'c list -> 'd list -> 'e list |
24 val split_filter: ('a -> bool) -> 'a list -> 'a list * 'a list |
25 val split_filter: ('a -> bool) -> 'a list -> 'a list * 'a list |
25 val fold_left: ('a * 'a -> 'a) -> 'a list -> 'a -> 'a |
26 val fold_left: ('a * 'a -> 'a) -> 'a list -> 'a -> 'a |
26 |
27 |
27 val is_true: term -> bool |
28 val is_true: term -> bool |
28 |
29 |
29 val dest_listT: typ -> typ |
30 val dest_listT: typ -> typ |
30 val dest_fsetT: typ -> typ |
31 val dest_fsetT: typ -> typ |
31 |
32 |
32 val mk_id: term -> term |
33 val mk_id: term -> term |
33 val mk_all: (string * typ) -> term -> term |
34 val mk_all: (string * typ) -> term -> term |
47 val perm_const: typ -> term |
48 val perm_const: typ -> term |
48 val mk_perm_ty: typ -> term -> term -> term |
49 val mk_perm_ty: typ -> term -> term -> term |
49 val mk_perm: term -> term -> term |
50 val mk_perm: term -> term -> term |
50 val dest_perm: term -> term * term |
51 val dest_perm: term -> term * term |
51 |
52 |
|
53 (* functions to deal with constants in local contexts *) |
|
54 val long_name: Proof.context -> string -> string |
|
55 val is_fixed: Proof.context -> term -> bool |
|
56 val fixed_nonfixed_args: Proof.context -> term -> term * term list |
52 end |
57 end |
53 |
58 |
54 |
59 |
55 structure Nominal_Basic: NOMINAL_BASIC = |
60 structure Nominal_Basic: NOMINAL_BASIC = |
56 struct |
61 struct |
124 (* to be used with left-infix binop-operations *) |
129 (* to be used with left-infix binop-operations *) |
125 fun fold_left f [] z = z |
130 fun fold_left f [] z = z |
126 | fold_left f [x] z = x |
131 | fold_left f [x] z = x |
127 | fold_left f (x :: y :: xs) z = fold_left f (f (x, y) :: xs) z |
132 | fold_left f (x :: y :: xs) z = fold_left f (f (x, y) :: xs) z |
128 |
133 |
129 |
|
130 |
|
131 fun is_true @{term "Trueprop True"} = true |
134 fun is_true @{term "Trueprop True"} = true |
132 | is_true _ = false |
135 | is_true _ = false |
133 |
136 |
134 fun dest_listT (Type (@{type_name list}, [T])) = T |
137 fun dest_listT (Type (@{type_name list}, [T])) = T |
135 | dest_listT T = raise TYPE ("dest_listT: list type expected", [T], []) |
138 | dest_listT T = raise TYPE ("dest_listT: list type expected", [T], []) |
136 |
139 |
137 fun dest_fsetT (Type (@{type_name fset}, [T])) = T |
140 fun dest_fsetT (Type (@{type_name fset}, [T])) = T |
138 | dest_fsetT T = raise TYPE ("dest_fsetT: fset type expected", [T], []); |
141 | dest_fsetT T = raise TYPE ("dest_fsetT: fset type expected", [T], []) |
139 |
|
140 |
142 |
141 fun mk_id trm = HOLogic.id_const (fastype_of trm) $ trm |
143 fun mk_id trm = HOLogic.id_const (fastype_of trm) $ trm |
142 |
144 |
143 fun mk_all (a, T) t = Logic.all_const T $ Abs (a, T, t) |
145 fun mk_all (a, T) t = Logic.all_const T $ Abs (a, T, t) |
144 |
146 |
145 fun mk_All (a, T) t = HOLogic.all_const T $ Abs (a, T, t) |
147 fun mk_All (a, T) t = HOLogic.all_const T $ Abs (a, T, t) |
146 |
148 |
147 fun mk_exists (a, T) t = HOLogic.exists_const T $ Abs (a, T, t) |
149 fun mk_exists (a, T) t = HOLogic.exists_const T $ Abs (a, T, t) |
148 |
150 |
149 fun sum_case_const ty1 ty2 ty3 = |
151 fun sum_case_const ty1 ty2 ty3 = |
150 Const (@{const_name sum_case}, [ty1 --> ty3, ty2 --> ty3, Type (@{type_name sum}, [ty1, ty2])] ---> ty3) |
152 Const (@{const_name sum_case}, [ty1 --> ty3, ty2 --> ty3, Type (@{type_name sum}, [ty1, ty2])] ---> ty3) |
151 |
153 |
152 fun mk_sum_case trm1 trm2 = |
154 fun mk_sum_case trm1 trm2 = |
153 let |
155 let |
154 val ([ty1], ty3) = strip_type (fastype_of trm1) |
156 val ([ty1], ty3) = strip_type (fastype_of trm1) |
155 val ty2 = domain_type (fastype_of trm2) |
157 val ty2 = domain_type (fastype_of trm2) |
156 in |
158 in |
157 sum_case_const ty1 ty2 ty3 $ trm1 $ trm2 |
159 sum_case_const ty1 ty2 ty3 $ trm1 $ trm2 |
158 end |
160 end |
159 |
161 |
160 |
162 fun mk_equiv r = r RS @{thm eq_reflection} |
161 fun mk_equiv r = r RS @{thm eq_reflection}; |
163 fun safe_mk_equiv r = mk_equiv r handle Thm.THM _ => r |
162 fun safe_mk_equiv r = mk_equiv r handle Thm.THM _ => r; |
|
163 |
|
164 |
164 |
165 fun mk_minus p = @{term "uminus::perm => perm"} $ p |
165 fun mk_minus p = @{term "uminus::perm => perm"} $ p |
166 |
166 |
167 fun mk_plus p q = @{term "plus::perm => perm => perm"} $ p $ q |
167 fun mk_plus p q = @{term "plus::perm => perm => perm"} $ p $ q |
168 |
168 |
170 fun perm_const ty = Const (@{const_name "permute"}, perm_ty ty) |
170 fun perm_const ty = Const (@{const_name "permute"}, perm_ty ty) |
171 fun mk_perm_ty ty p trm = perm_const ty $ p $ trm |
171 fun mk_perm_ty ty p trm = perm_const ty $ p $ trm |
172 fun mk_perm p trm = mk_perm_ty (fastype_of trm) p trm |
172 fun mk_perm p trm = mk_perm_ty (fastype_of trm) p trm |
173 |
173 |
174 fun dest_perm (Const (@{const_name "permute"}, _) $ p $ t) = (p, t) |
174 fun dest_perm (Const (@{const_name "permute"}, _) $ p $ t) = (p, t) |
175 | dest_perm t = raise TERM ("dest_perm", [t]); |
175 | dest_perm t = raise TERM ("dest_perm", [t]) |
|
176 |
|
177 |
|
178 (** functions to deal with constants in local contexts **) |
|
179 |
|
180 (* returns the fully qualified name of a constant *) |
|
181 fun long_name ctxt name = |
|
182 case head_of (Syntax.read_term ctxt name) of |
|
183 Const (s, _) => s |
|
184 | _ => error ("Undeclared constant: " ^ quote name) |
|
185 |
|
186 (* returns true iff the argument term is a fixed Free *) |
|
187 fun is_fixed_Free ctxt (Free (s, _)) = Variable.is_fixed ctxt s |
|
188 | is_fixed_Free _ _ = false |
|
189 |
|
190 (* returns true iff c is a constant or fixed Free applied to |
|
191 fixed parameters *) |
|
192 fun is_fixed ctxt c = |
|
193 let |
|
194 val (c, args) = strip_comb c |
|
195 in |
|
196 (is_Const c orelse is_fixed_Free ctxt c) |
|
197 andalso List.all (is_fixed_Free ctxt) args |
|
198 end |
|
199 |
|
200 (* splits a list into the longest prefix containing only elements |
|
201 that satisfy p, and the rest of the list *) |
|
202 fun chop_while p = |
|
203 let |
|
204 fun chop_while_aux acc [] = |
|
205 (rev acc, []) |
|
206 | chop_while_aux acc (x::xs) = |
|
207 if p x then chop_while_aux (x::acc) xs else (rev acc, x::xs) |
|
208 in |
|
209 chop_while_aux [] |
|
210 end |
|
211 |
|
212 (* takes a combination "c $ fixed1 $ ... $ fixedN $ not-fixed $ ..." |
|
213 to the pair ("c $ fixed1 $ ... $ fixedN", ["not-fixed", ...]). *) |
|
214 fun fixed_nonfixed_args ctxt c_args = |
|
215 let |
|
216 val (c, args) = strip_comb c_args |
|
217 val (frees, args) = chop_while (is_fixed_Free ctxt) args |
|
218 val c_frees = list_comb (c, frees) |
|
219 in |
|
220 (c_frees, args) |
|
221 end |
176 |
222 |
177 end (* structure *) |
223 end (* structure *) |
178 |
224 |
179 open Nominal_Basic; |
225 open Nominal_Basic; |