# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1268208592 -3600
# Node ID 8399236f901bf15da4622919eaf6b62894f4435c
# Parent  71bd178e478557324a3bf8b935e7a4015785684a
Use alpha_bns in normal alpha defs.

diff -r 71bd178e4785 -r 8399236f901b Nominal/Fv.thy
--- 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