# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1268208611 -3600
# Node ID adeb3746ec8fd3765bf8918c4eedde12e373f977
# Parent  8399236f901bf15da4622919eaf6b62894f4435c# Parent  09899b909772a3bc5aae9d0a9f4fc8bfaff5860e
merge

diff -r 09899b909772 -r adeb3746ec8f Nominal/Fv.thy
--- a/Nominal/Fv.thy	Tue Mar 09 22:10:10 2010 +0100
+++ b/Nominal/Fv.thy	Wed Mar 10 09:10:11 2010 +0100
@@ -215,6 +215,9 @@
     "alpha_" ^ name_of_typ (nth_dtyp i)) descr);
   val alpha_types = map (fn (i, _) => nth_dtyp i --> nth_dtyp i --> @{typ bool}) descr;
   val alpha_frees = map Free (alpha_names ~~ alpha_types);
+  val alpha_bnnames = map (fn (bn, _, _) => "alpha_" ^ (Long_Name.base_name (fst (dest_Const bn)))) bns;
+  val alpha_bntypes = map (fn (_, i, _) => @{typ perm} --> nth_dtyp i --> nth_dtyp i --> @{typ bool}) bns;
+  val alpha_bnfrees = map Free (alpha_bnnames ~~ alpha_bntypes);
   fun fv_alpha_constr ith_dtyp (cname, dts) bindcs =
     let
       val Ts = map (typ_of_dtyp descr sorts) dts;
@@ -269,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);
@@ -290,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