328 if is_rec_type dt then (nth alpha_frees (body_index dt) $ arg $ arg2) |
328 if is_rec_type dt then (nth alpha_frees (body_index dt) $ arg $ arg2) |
329 else (HOLogic.mk_eq (arg, arg2)) |
329 else (HOLogic.mk_eq (arg, arg2)) |
330 (* TODO: if more then check and accept *) |
330 (* TODO: if more then check and accept *) |
331 | (_, [], []) => @{term True} |
331 | (_, [], []) => @{term True} |
332 | ([], [(((SOME (bn, _)), _, _), pi)], []) => |
332 | ([], [(((SOME (bn, _)), _, _), pi)], []) => |
333 nth alpha_bn_frees (find_index (fn (b, _, _) => b = bn) bns) $ pi $ arg $ arg2 |
333 let |
|
334 val alpha_bn = nth alpha_bn_frees (find_index (fn (b, _, _) => b = bn) bns) $ pi $ arg $ arg2 |
|
335 val ty = fastype_of (bn $ arg) |
|
336 val permute = Const(@{const_name permute}, @{typ perm} --> ty --> ty) |
|
337 in |
|
338 HOLogic.mk_conj (alpha_bn, HOLogic.mk_eq (permute $ pi $ (bn $ arg), (bn $ arg2))) |
|
339 end |
334 | ([], [], relevant) => |
340 | ([], [], relevant) => |
335 let |
341 let |
336 val (rbinds, rpis) = split_list relevant |
342 val (rbinds, rpis) = split_list relevant |
337 val lhs_binds = fv_binds args rbinds |
343 val lhs_binds = fv_binds args rbinds |
338 val lhs = mk_pair (lhs_binds, arg); |
344 val lhs = mk_pair (lhs_binds, arg); |