234 val (_, (_, _, constrs)) = nth descr ith_dtyp; |
234 val (_, (_, _, constrs)) = nth descr ith_dtyp; |
235 val eqs = map2i alpha_bn_constr constrs args_in_bns |
235 val eqs = map2i alpha_bn_constr constrs args_in_bns |
236 in |
236 in |
237 ((bn, alpha_bn_free), (alpha_bn_name, eqs)) |
237 ((bn, alpha_bn_free), (alpha_bn_name, eqs)) |
238 end |
238 end |
|
239 *} |
|
240 |
|
241 (* Checks that a list of bindings contains only compatible ones *) |
|
242 ML {* |
|
243 fun bns_same l = |
|
244 length (distinct (op =) (map (fn ((b, _, _), _) => b) l)) = 1 |
239 *} |
245 *} |
240 |
246 |
241 ML {* fn x => split_list(flat x) *} |
247 ML {* fn x => split_list(flat x) *} |
242 ML {* fn x => apsnd flat (split_list (map split_list x)) *} |
248 ML {* fn x => apsnd flat (split_list (map split_list x)) *} |
243 (* TODO: Notice datatypes without bindings and replace alpha with equality *) |
249 (* TODO: Notice datatypes without bindings and replace alpha with equality *) |
326 case (rel_in_simp_binds, rel_in_comp_binds, rel_has_binds) of |
332 case (rel_in_simp_binds, rel_in_comp_binds, rel_has_binds) of |
327 ([], [], []) => |
333 ([], [], []) => |
328 if is_rec_type dt then (nth alpha_frees (body_index dt) $ arg $ arg2) |
334 if is_rec_type dt then (nth alpha_frees (body_index dt) $ arg $ arg2) |
329 else (HOLogic.mk_eq (arg, arg2)) |
335 else (HOLogic.mk_eq (arg, arg2)) |
330 | (_, [], []) => @{term True} |
336 | (_, [], []) => @{term True} |
331 (* TODO: if more then check that they are the same and accept *) |
337 | ([], ((((SOME (bn, _)), _, _), pi) :: _), []) => |
332 | ([], [(((SOME (bn, _)), _, _), pi)], []) => |
|
333 let |
338 let |
334 val alpha_bn = nth alpha_bn_frees (find_index (fn (b, _, _) => b = bn) bns) $ pi $ arg $ arg2 |
339 val alpha_bn = nth alpha_bn_frees (find_index (fn (b, _, _) => b = bn) bns) $ pi $ arg $ arg2 |
335 val ty = fastype_of (bn $ arg) |
340 val ty = fastype_of (bn $ arg) |
336 val permute = Const(@{const_name permute}, @{typ perm} --> ty --> ty) |
341 val permute = Const(@{const_name permute}, @{typ perm} --> ty --> ty) |
337 in |
342 in |
338 HOLogic.mk_conj (alpha_bn, HOLogic.mk_eq (permute $ pi $ (bn $ arg), (bn $ arg2))) |
343 if bns_same rel_in_comp_binds then |
|
344 HOLogic.mk_conj (alpha_bn, HOLogic.mk_eq (permute $ pi $ (bn $ arg), (bn $ arg2))) |
|
345 else error "incompatible bindings for one argument" |
339 end |
346 end |
340 | ([], [], relevant) => |
347 | ([], [], relevant) => |
341 let |
348 let |
342 val (rbinds, rpis) = split_list relevant |
349 val (rbinds, rpis) = split_list relevant |
343 val lhs_binds = fv_binds args rbinds |
350 val lhs_binds = fv_binds args rbinds |