--- a/Nominal/Fv.thy	Thu Mar 18 11:16:53 2010 +0100
+++ b/Nominal/Fv.thy	Thu Mar 18 11:29:12 2010 +0100
@@ -2,7 +2,9 @@
 imports "Nominal2_Atoms" "Abs" "Perm" "Rsp"
 begin
 
-(* Bindings are a list of lists of lists of triples.
+(* The bindings data structure:
+
+  Bindings are a list of lists of lists of triples.
 
    The first list represents the datatypes defined.
    The second list represents the constructors.
@@ -28,34 +30,50 @@
 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,
-  For each of the constructors,
-  It creates a union of free variables for each argument.
+(*
+The overview of the generation of free variables:
+
+1) fv_bn functions are generated only for the non-recursive binds.
+
+   An fv_bn for a constructor is a union of values for the arguments:
 
-  For an argument the free variables are the variables minus
-  bound variables.
+   For an argument x that is in the bn function
+   - if it is a recursive argument bn' we return: fv_bn' x
+   - otherwise empty
+
+   For an argument x that is not in the bn function
+   - for atom we return: {atom x}
+   - for atom set we return: atom ` x
+   - for a recursive call to type ty' we return: fv_ty' x
+     with fv of the appropriate type
+   - otherwise empty
+
+2) fv functions generated for all new datatypes:
 
-  The variables are:
-    For an atom, a singleton set with the atom itself.
-    For an atom set, the atom set itself.
-    For a recursive argument, the appropriate fv function applied to it.
-    (* TODO: This one is not implemented *)
-    For other arguments it should be an appropriate fv function stored
-      in the database.
-  The bound variables are a union of results of all bindings that
-  involve the given argument. For a paricular binding the result is:
-    For a function applied to an argument this function with the argument.
-    For an atom, a singleton set with the atom itself.
-    For an atom set, the atom set itself.
-    For a recursive argument, the appropriate fv function applied to it.
-    (* TODO: This one is not implemented *)
-    For other arguments it should be an appropriate fv function stored
-      in the database.
+   An fv for a constructor is a union of values for the arguments.
+
+   For an argument x that bound in a non-recursive binding
+   we return: fv_bn x.
+
+   Otherwise we return the free variables of the argument minus the
+   bound variables of the argument.
 
-  For every argument that is a binding, we add a the same binding in its
-  body.
+   The free variables for an argument x are:
+   - for an atom: {atom x}
+   - for atom set: atom ` x
+   - for recursive call to type ty' return: fv_ty' x
+   - for nominal datatype ty' return: fv_ty' x
+
+   The bound variables are a union of results of all bindings that
+   involve the given argument. For a paricular binding:
+
+   - for a binding function bn: bn x
+   - for an atom: {atom x}
+   - for atom set: atom ` x
+   - for a recursive argument of type ty': fv_fy' x
+   - for nominal datatype ty' return: fv_ty' x
 *)
 
 ML {*
@@ -188,6 +206,7 @@
 *}
 
 (* We assume no bindings in the type on which bn is defined *)
+(* TODO: currently works only with current fv_bn function *)
 ML {*
 fun fv_bn thy (dt_info : Datatype_Aux.info) fv_frees (bn, ith_dtyp, args_in_bns) =
 let
@@ -331,8 +350,6 @@
       fun fv_binds args relevant = mk_union (map (fv_bind args) relevant)
       fun find_nonrec_binder j (SOME (f, false), i, _) = if i = j then SOME f else NONE
         | find_nonrec_binder _ _ = NONE
-      fun find_compound_binder j (SOME (f, r), i, _) = if i = j then SOME (f, r) else NONE
-        | find_compound_binder _ _ = NONE
       fun fv_arg ((dt, x), arg_no) =
         case get_first (find_nonrec_binder arg_no) bindcs of
           SOME f =>