--- a/Nominal/Fv.thy	Mon Mar 08 15:01:01 2010 +0100
+++ b/Nominal/Fv.thy	Mon Mar 08 15:01:26 2010 +0100
@@ -2,14 +2,15 @@
 imports "Nominal2_Atoms" "Abs" "Perm" "Rsp"
 begin
 
-(* Bindings are given as a list which has a length being equal
-   to the length of the number of constructors.
+(* Bindings are a list of lists of lists of triples.
 
-   Each element is a list whose length is equal to the number
-   of arguents.
+   The first list represents the datatypes defined.
+   The second list represents the constructors.
+   The internal list is a list of all the bndings that
+   concern the constructor.
 
-   Every element specifies bindings of this argument given as
-   a tuple: function, bound argument.
+   Every triple consists of a function, the binding and
+   the body.
 
   Eg:
 nominal_datatype
@@ -21,12 +22,12 @@
 yields:
 [
  [],
- [[], [], [(NONE, 0)]],
- [[], [], [(SOME (Const f), 0), (Some (Const g), 1)]]]
+ [(NONE, 0, 2)],
+ [(SOME (Const f), 0, 2), (Some (Const g), 1, 2)]]
 
-A SOME binding has to have a function returning an atom set,
-and a NONE binding has to be on an argument that is an atom
-or an atom set.
+A SOME binding has to have a function which takes an appropriate
+argument and returns an atom set. A NONE binding has to be on an
+argument that is an atom or an atom set.
 
 How the procedure works:
   For each of the defined datatypes,
@@ -52,15 +53,50 @@
     (* TODO: This one is not implemented *)
     For other arguments it should be an appropriate fv function stored
       in the database.
+
+  For every argument that is a binding, we add a the same binding in its
+  body.
 *)
 
 ML {*
+fun is_atom thy typ =
+  Sign.of_sort thy (typ, @{sort at})
+*}
+
+
+(* Like map2, only if the second list is empty passes empty lists insted of error *)
+ML {*
 fun map2i _ [] [] = []
   | map2i f (x :: xs) (y :: ys) = f x y :: map2i f xs ys
   | map2i f (x :: xs) [] = f x [] :: map2i f xs []
   | map2i _ _ _ = raise UnequalLengths;
 *}
 
+(* Finds bindings with the same function and binding, and gathers all
+   bodys for such pairs *)
+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' *)
@@ -110,7 +146,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 +163,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);
@@ -178,14 +215,14 @@
               val rhs = mk_pair (rhs_binds, arg2);
               val alpha = nth alpha_frees (body_index dt);
               val fv = nth fv_frees (body_index dt);
-              val pi = foldr1 add_perm rpis;
+              val pi = foldr1 add_perm (distinct (op =) 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 +235,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)
@@ -236,7 +273,7 @@
 
 (* to be given by the user *)
 
-primrec 
+primrec
   bv1
 where
   "bv1 (BUnit) = {}"