362 val rel_in_simp_binds = filter (fn ((NONE, i, _), _) => i = arg_no | _ => false) bind_pis; |
362 val rel_in_simp_binds = filter (fn ((NONE, i, _), _) => i = arg_no | _ => false) bind_pis; |
363 val rel_in_comp_binds = filter (fn ((SOME _, i, _), _) => i = arg_no | _ => false) bind_pis; |
363 val rel_in_comp_binds = filter (fn ((SOME _, i, _), _) => i = arg_no | _ => false) bind_pis; |
364 val rel_has_binds = filter (fn ((NONE, _, j), _) => j = arg_no |
364 val rel_has_binds = filter (fn ((NONE, _, j), _) => j = arg_no |
365 | ((SOME (_, false), _, j), _) => j = arg_no |
365 | ((SOME (_, false), _, j), _) => j = arg_no |
366 | _ => false) bind_pis; |
366 | _ => false) bind_pis; |
|
367 val rel_has_rec_binds = filter |
|
368 (fn ((SOME (_, true), _, j), _) => j = arg_no | _ => false) bind_pis; |
367 in |
369 in |
368 case (rel_in_simp_binds, rel_in_comp_binds, rel_has_binds) of |
370 case (rel_in_simp_binds, rel_in_comp_binds, rel_has_binds, rel_has_rec_binds) of |
369 ([], [], []) => |
371 ([], [], [], []) => |
370 if is_rec_type dt then (nth alpha_frees (body_index dt) $ arg $ arg2) |
372 if is_rec_type dt then (nth alpha_frees (body_index dt) $ arg $ arg2) |
371 else (HOLogic.mk_eq (arg, arg2)) |
373 else (HOLogic.mk_eq (arg, arg2)) |
372 | (_, [], []) => @{term True} |
374 | (_, [], [], []) => @{term True} |
373 | ([], ((((SOME (bn, is_rec)), _, _), pi) :: _), []) => |
375 | ([], [], [], _) => @{term True} |
|
376 | ([], ((((SOME (bn, is_rec)), _, _), pi) :: _), [], []) => |
374 if not (bns_same rel_in_comp_binds) then error "incompatible bindings for an argument" else |
377 if not (bns_same rel_in_comp_binds) then error "incompatible bindings for an argument" else |
375 if is_rec then |
378 if is_rec then |
376 let |
379 let |
377 val (rbinds, rpis) = split_list rel_in_comp_binds |
380 val (rbinds, rpis) = split_list rel_in_comp_binds |
378 val bound_in_nos = map (fn (_, _, i) => i) rbinds |
381 val bound_in_nos = map (fn (_, _, i) => i) rbinds |
407 val ty = fastype_of (bn $ arg) |
410 val ty = fastype_of (bn $ arg) |
408 val permute = Const(@{const_name permute}, @{typ perm} --> ty --> ty) |
411 val permute = Const(@{const_name permute}, @{typ perm} --> ty --> ty) |
409 in |
412 in |
410 alpha_bn_const $ arg $ arg2 |
413 alpha_bn_const $ arg $ arg2 |
411 end |
414 end |
412 | ([], [], relevant) => |
415 | ([], [], relevant, []) => |
413 let |
416 let |
414 val (rbinds, rpis) = split_list relevant |
417 val (rbinds, rpis) = split_list relevant |
415 val lhs_binds = fv_binds args rbinds |
418 val lhs_binds = fv_binds args rbinds |
416 val lhs = mk_pair (lhs_binds, arg); |
419 val lhs = mk_pair (lhs_binds, arg); |
417 val rhs_binds = fv_binds args2 rbinds; |
420 val rhs_binds = fv_binds args2 rbinds; |