319 HOLogic.mk_Trueprop (alpha $ (list_comb (c, args)) $ (list_comb (c, args2))); |
319 HOLogic.mk_Trueprop (alpha $ (list_comb (c, args)) $ (list_comb (c, args2))); |
320 fun alpha_arg ((dt, arg_no), (arg, arg2)) = |
320 fun alpha_arg ((dt, arg_no), (arg, arg2)) = |
321 let |
321 let |
322 val rel_in_simp_binds = filter (fn ((NONE, i, _), _) => i = arg_no | _ => false) bind_pis; |
322 val rel_in_simp_binds = filter (fn ((NONE, i, _), _) => i = arg_no | _ => false) bind_pis; |
323 val rel_in_comp_binds = filter (fn ((SOME _, i, _), _) => i = arg_no | _ => false) bind_pis; |
323 val rel_in_comp_binds = filter (fn ((SOME _, i, _), _) => i = arg_no | _ => false) bind_pis; |
324 val rel_has_binds = filter (fn ((SOME _, _, j), _) => j = arg_no | _ => false) bind_pis; |
324 val rel_has_binds = filter (fn ((_, _, j), _) => j = arg_no | _ => false) bind_pis; |
325 in |
325 in |
326 case (rel_in_simp_binds, rel_in_comp_binds, rel_has_binds) of |
326 case (rel_in_simp_binds, rel_in_comp_binds, rel_has_binds) of |
327 ([], [], []) => |
327 ([], [], []) => |
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 *) |
|
331 | (_, [], []) => @{term True} |
330 | (_, [], []) => @{term True} |
|
331 (* TODO: if more then check that they are the same and accept *) |
332 | ([], [(((SOME (bn, _)), _, _), pi)], []) => |
332 | ([], [(((SOME (bn, _)), _, _), pi)], []) => |
333 let |
333 let |
334 val alpha_bn = nth alpha_bn_frees (find_index (fn (b, _, _) => b = bn) bns) $ pi $ arg $ arg2 |
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) |
335 val ty = fastype_of (bn $ arg) |
336 val permute = Const(@{const_name permute}, @{typ perm} --> ty --> ty) |
336 val permute = Const(@{const_name permute}, @{typ perm} --> ty --> ty) |