# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1268039311 -3600
# Node ID 42b7abf779ec92252838e1505945c6521685f7b9
# Parent  094811120a68a0e713d54cfddb4d3b6ad8916b63
Gather bindings with same binder, and generate only one permutation for them.

diff -r 094811120a68 -r 42b7abf779ec Nominal/Fv.thy
--- a/Nominal/Fv.thy	Mon Mar 08 02:40:16 2010 +0100
+++ b/Nominal/Fv.thy	Mon Mar 08 10:08:31 2010 +0100
@@ -2,6 +2,7 @@
 imports "Nominal2_Atoms" "Abs" "Perm" "Rsp"
 begin
 
+(* TODO: update the comment *)
 (* Bindings are given as a list which has a length being equal
    to the length of the number of constructors.
 
@@ -62,6 +63,29 @@
 *}
 
 ML {*
+fun gather_binds binds =
+let
+  fun gather_binds_cons binds =
+    let
+      val common = map (fn (f, bi, _) => (f, bi)) binds
+      val nodups = distinct (op =) common
+      fun find_bodys (sf, sbi) =
+        filter (fn (f, bi, _) => f = sf andalso bi = sbi) binds
+      val bodys = map ((map (fn (_, _, bo) => bo)) o find_bodys) nodups
+    in
+      nodups ~~ bodys
+    end
+in
+  map (map gather_binds_cons) binds
+end
+*}
+
+ML {*
+fun un_gather_binds_cons binds =
+  flat (map (fn (((f, bi), bos), pi) => map (fn bo => ((f, bi, bo), pi)) bos) binds)
+*}
+
+ML {*
   open Datatype_Aux; (* typ_of_dtyp, DtRec, ... *);
   (* TODO: It is the same as one in 'nominal_atoms' *)
   fun mk_atom ty = Const (@{const_name atom}, ty --> @{typ atom});
@@ -110,7 +134,6 @@
 ML {*
 fun define_fv_alpha (dt_info : Datatype_Aux.info) bindsall lthy =
 let
-  val thy = ProofContext.theory_of lthy;
   val {descr, sorts, ...} = dt_info;
   fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i);
   val fv_names = Datatype_Prop.indexify_names (map (fn (i, _) =>
@@ -128,7 +151,9 @@
       val pi_strs_same = replicate bindslen "pi"
       val pi_strs = Name.variant_list [] pi_strs_same;
       val pis = map (fn ps => Free (ps, @{typ perm})) pi_strs;
-      val bind_pis = bindcs ~~ pis;
+      val bind_pis_gath = bindcs ~~ pis;
+      val bind_pis = un_gather_binds_cons bind_pis_gath;
+      val bindcs = map fst bind_pis;
       val names = Name.variant_list pi_strs (Datatype_Prop.make_tnames Ts);
       val args = map Free (names ~~ Ts);
       val names2 = Name.variant_list (pi_strs @ names) (Datatype_Prop.make_tnames Ts);
@@ -181,11 +206,11 @@
               val pi = foldr1 add_perm rpis;
               val alpha_gen_pre = Const (@{const_name alpha_gen}, dummyT) $ lhs $ alpha $ fv $ pi $ rhs;
               val alpha_gen = Syntax.check_term lthy alpha_gen_pre
-              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"})
+(*              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*) alpha_gen
+              (*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
@@ -198,7 +223,7 @@
       (fv_eq, alpha_eq)
     end;
   fun fv_alpha_eq (i, (_, _, constrs)) binds = map2i (fv_alpha_constr i) constrs binds;
-  val (fv_eqs, alpha_eqs) = split_list (flat (map2i fv_alpha_eq descr bindsall))
+  val (fv_eqs, alpha_eqs) = split_list (flat (map2i fv_alpha_eq descr (gather_binds bindsall)))
   val add_binds = map (fn x => (Attrib.empty_binding, x))
   val (fvs, lthy') = (Primrec.add_primrec
     (map (fn s => (Binding.name s, NONE, NoSyn)) fv_names) (add_binds fv_eqs) lthy)