--- a/Nominal/Fv.thy Wed Mar 10 08:44:19 2010 +0100
+++ b/Nominal/Fv.thy Wed Mar 10 09:09:52 2010 +0100
@@ -272,14 +272,20 @@
HOLogic.mk_Trueprop (alpha $ (list_comb (c, args)) $ (list_comb (c, args2)));
fun alpha_arg ((dt, arg_no), (arg, arg2)) =
let
- val relevant = filter (fn ((_, i, j), _) => i = arg_no orelse j = arg_no) bind_pis;
+ val rel_in_simp_binds = filter (fn ((NONE, i, _), _) => i = arg_no | _ => false) bind_pis;
+ val rel_in_comp_binds = filter (fn ((SOME _, i, _), _) => i = arg_no | _ => false) bind_pis;
+ val rel_has_binds = filter (fn ((SOME _, _, j), _) => j = arg_no | _ => false) bind_pis;
in
- if relevant = [] then (
- if is_rec_type dt then (nth alpha_frees (body_index dt) $ arg $ arg2)
- else (HOLogic.mk_eq (arg, arg2)))
- else
- if is_rec_type dt then let
- (* THE HARD CASE *)
+ case (rel_in_simp_binds, rel_in_comp_binds, rel_has_binds) of
+ ([], [], []) =>
+ if is_rec_type dt then (nth alpha_frees (body_index dt) $ arg $ arg2)
+ else (HOLogic.mk_eq (arg, arg2))
+ (* TODO: if more then check and accept *)
+ | (_, [], []) => @{term True}
+ | ([], [(((SOME (bn, _)), _, _), pi)], []) =>
+ nth alpha_bnfrees (find_index (fn (b, _, _) => b = bn) bns) $ pi $ arg $ arg2
+ | ([], [], relevant) =>
+ let
val (rbinds, rpis) = split_list relevant
val lhs_binds = fv_binds args rbinds
val lhs = mk_pair (lhs_binds, arg);
@@ -293,10 +299,9 @@
(* val pi_supps = map ((curry op $) @{term "supp :: perm \<Rightarrow> atom set"}) rpis;
val pi_supps_eq = HOLogic.mk_eq (mk_inter pi_supps, @{term "{} :: atom set"}) *)
in
- (*if length pi_supps > 1 then HOLogic.mk_conj (alpha_gen, pi_supps_eq) else*)
+(* if length pi_supps > 1 then HOLogic.mk_conj (alpha_gen, pi_supps_eq) else*)
alpha_gen
- (* TODO Add some test that is makes sense *)
- end else @{term "True"}
+ end
end
val alphas = map alpha_arg (dts ~~ arg_nos ~~ (args ~~ args2))
val alpha_lhss = mk_conjl alphas