diff -r 20ee31bc34d5 -r d134bd4f6d1b Nominal/nominal_dt_rawfuns.ML
--- a/Nominal/nominal_dt_rawfuns.ML	Fri May 21 00:44:39 2010 +0100
+++ b/Nominal/nominal_dt_rawfuns.ML	Fri May 21 05:58:23 2010 +0100
@@ -17,9 +17,13 @@
   val setify: Proof.context -> term -> term
   val listify: Proof.context -> term -> term
 
-  val define_raw_fvs: Datatype_Aux.descr -> (string * sort) list ->
-    (term * 'a * 'b) list -> (term * int * (int * term option) list list) list ->
-      bclause list list list -> Proof.context -> term list * term list * thm list * local_theory
+  val define_raw_fvs: 
+     string list -> term list -> 
+     Datatype_Aux.descr ->
+     (string * sort) list ->
+     (term * int * (int * term option) list list) list ->
+     (term * int * (int * term option) list list) list ->
+     bclause list list list -> Proof.context -> term list * term list * thm list * local_theory
 end
 
 
@@ -29,7 +33,7 @@
 datatype bmode = Lst | Res | Set
 datatype bclause = BC of bmode * (term option * int) list * int list
 
-(* atom types *)
+(* testing for concrete atom types *)
 fun is_atom ctxt ty =
   Sign.of_sort (ProofContext.theory_of ctxt) (ty, @{sort at_base})
 
@@ -43,15 +47,16 @@
   | is_atom_list _ _ = false
 
 
-(* functions for producing sets, fsets and lists *)
+(* functions for producing sets, fsets and lists of general atom type
+   out from concrete atom types *)
 fun mk_atom_set t =
 let
   val ty = fastype_of t;
   val atom_ty = HOLogic.dest_setT ty --> @{typ "atom"};
   val img_ty = atom_ty --> ty --> @{typ "atom set"};
 in
-  (Const (@{const_name image}, img_ty) $ mk_atom_ty atom_ty t)
-end;
+  Const (@{const_name image}, img_ty) $ mk_atom_ty atom_ty t
+end
 
 fun mk_atom_fset t =
 let
@@ -61,20 +66,19 @@
   val fset_to_set = @{term "fset_to_set :: atom fset => atom set"}
 in
   fset_to_set $ (Const (@{const_name fmap}, fmap_ty) $ Const (@{const_name atom}, atom_ty) $ t)
-end;
+end
 
-(*
 fun mk_atom_list t =
 let
   val ty = fastype_of t;
   val atom_ty = dest_listT ty --> @{typ atom};
   val map_ty = atom_ty --> ty --> @{typ "atom list"};
 in
-  (Const (@{const_name map}, map_ty) $ mk_atom_ty atom_ty t)
-end;
-*)
+  Const (@{const_name map}, map_ty) $ mk_atom_ty atom_ty t
+end
 
-(* functions that coerces atoms, sets and fsets into atom sets ? *)
+(* functions that coerces concrete atoms, sets and fsets into sets
+   of general atoms *)
 fun setify ctxt t =
 let
   val ty = fastype_of t;
@@ -88,7 +92,8 @@
   else raise TERM ("setify", [t])
 end
 
-(* functions that coerces atoms and lists into atom lists ? *)
+(* functions that coerces concrete atoms and lists into lists of 
+   general atoms  *)
 fun listify ctxt t =
 let
   val ty = fastype_of t;
@@ -109,7 +114,7 @@
 
 (* functions that construct the equations for fv and fv_bn *)
 
-fun make_fv_body fv_map args i = 
+fun mk_fv_body fv_map args i = 
 let
   val arg = nth args i
   val ty = fastype_of arg
@@ -119,37 +124,7 @@
   | SOME fv => fv $ arg
 end  
 
-fun make_fv_binder lthy fv_bn_map args (bn_option, i) = 
-let
-  val arg = nth args i
-in
-  case bn_option of
-    NONE => (setify lthy arg, @{term "{}::atom set"})
-  | SOME bn => (to_set (bn $ arg), the (AList.lookup (op=) fv_bn_map bn) $ arg)
-end  
-
-fun make_fv_rhs lthy fv_map fv_bn_map args (BC (_, binders, bodies)) =
-let
-  val t1 = map (make_fv_body fv_map args) bodies
-  val (t2, t3) = split_list (map (make_fv_binder lthy fv_bn_map args) binders)
-in 
-  fold_union (mk_diff (fold_union t1, fold_union t2)::t3)
-end
-
-fun make_fv_eq lthy fv_map fv_bn_map (constr, ty, arg_tys) bclauses = 
-let
-  val arg_names = Datatype_Prop.make_tnames arg_tys
-  val args = map Free (arg_names ~~ arg_tys)
-  val fv = the (AList.lookup (op=) fv_map ty)
-  val lhs = fv $ list_comb (constr, args)
-  val rhs_trms = map (make_fv_rhs lthy fv_map fv_bn_map args) bclauses
-  val rhs = fold_union rhs_trms
-in
-  HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
-end
-
-
-fun make_fv_bn_body fv_map fv_bn_map bn_args args i = 
+fun mk_fv_bn_body fv_map fv_bn_map bn_args args i = 
 let
   val arg = nth args i
   val ty = fastype_of arg
@@ -162,39 +137,70 @@
   | SOME (SOME bn) => the (AList.lookup (op=) fv_bn_map bn) $ arg
 end  
 
-fun make_fv_bn_rhs lthy fv_map fv_bn_map bn_args args bclause =
+fun mk_fv_binder lthy fv_bn_map args (bn_option, i) = 
+let
+  val arg = nth args i
+in
+  case bn_option of
+    NONE => (setify lthy arg, @{term "{}::atom set"})
+  | SOME bn => (to_set (bn $ arg), the (AList.lookup (op=) fv_bn_map bn) $ arg)
+end  
+
+fun mk_fv_rhs lthy fv_map fv_bn_map args (BC (_, binders, bodies)) =
+let
+  val t1 = map (mk_fv_body fv_map args) bodies
+  val (t2, t3) = split_list (map (mk_fv_binder lthy fv_bn_map args) binders)
+in 
+  fold_union (mk_diff (fold_union t1, fold_union t2)::t3)
+end
+
+fun mk_fv_bn_rhs lthy fv_map fv_bn_map bn_args args bclause =
   case bclause of
-    BC (_, [], bodies) => fold_union (map (make_fv_bn_body fv_map fv_bn_map bn_args args) bodies)
+    BC (_, [], bodies) => fold_union (map (mk_fv_bn_body fv_map fv_bn_map bn_args args) bodies)
   | BC (_, binders, bodies) => 
       let
-        val t1 = map (make_fv_body fv_map args) bodies
-        val (t2, t3) = split_list (map (make_fv_binder lthy fv_bn_map args) binders)
+        val t1 = map (mk_fv_body fv_map args) bodies
+        val (t2, t3) = split_list (map (mk_fv_binder lthy fv_bn_map args) binders)
       in 
         fold_union (mk_diff (fold_union t1, fold_union t2)::t3)
       end
 
-fun make_fv_bn_eq lthy bn_trm fv_map fv_bn_map (bn_args, (constr, _, arg_tys)) bclauses =
+fun mk_fv_eq lthy fv_map fv_bn_map (constr, ty, arg_tys) bclauses = 
+let
+  val arg_names = Datatype_Prop.make_tnames arg_tys
+  val args = map Free (arg_names ~~ arg_tys)
+  val fv = the (AList.lookup (op=) fv_map ty)
+  val lhs = fv $ list_comb (constr, args)
+  val rhs_trms = map (mk_fv_rhs lthy fv_map fv_bn_map args) bclauses
+  val rhs = fold_union rhs_trms
+in
+  HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
+end
+
+fun mk_fv_bn_eq lthy bn_trm fv_map fv_bn_map (bn_args, (constr, _, arg_tys)) bclauses =
 let
   val arg_names = Datatype_Prop.make_tnames arg_tys
   val args = map Free (arg_names ~~ arg_tys)
   val fv_bn = the (AList.lookup (op=) fv_bn_map bn_trm)
   val lhs = fv_bn $ list_comb (constr, args)
-  val rhs_trms = map (make_fv_bn_rhs lthy fv_map fv_bn_map bn_args args) bclauses
+  val rhs_trms = map (mk_fv_bn_rhs lthy fv_map fv_bn_map bn_args args) bclauses
   val rhs = fold_union rhs_trms
 in
   HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
 end
 
-fun make_fv_bn_eqs lthy fv_map fv_bn_map constrs_info bclausesss (bn_trm, bn_n, bn_argss) = 
+fun mk_fv_bn_eqs lthy fv_map fv_bn_map constrs_info bclausesss (bn_trm, bn_n, bn_argss) = 
 let
   val nth_constrs_info = nth constrs_info bn_n
   val nth_bclausess = nth bclausesss bn_n
 in
-  map2 (make_fv_bn_eq lthy bn_trm fv_map fv_bn_map) (bn_argss ~~ nth_constrs_info) nth_bclausess
+  map2 (mk_fv_bn_eq lthy bn_trm fv_map fv_bn_map) (bn_argss ~~ nth_constrs_info) nth_bclausess
 end
 
-fun define_raw_fvs dt_descr sorts bn_funs bn_funs2 bclausesss lthy =
+fun define_raw_fvs t1 t2 dt_descr sorts bn_funs bn_funs2 bclausesss lthy =
 let
+  val _ = tracing ("bn-functions to be defined\n " ^ commas t1)
+  val _ = tracing ("bn-equations\n " ^ cat_lines (map (Syntax.string_of_term lthy) t2))
 
   val fv_names = prefix_dt_names dt_descr sorts "fv_"
   val fv_arg_tys = map (fn (i, _) => nth_dtyp dt_descr sorts i) dt_descr;
@@ -212,11 +218,17 @@
   val fv_bn_map2 = bns ~~ fv_bn_frees2
   val fv_bn_map3 = bns2 ~~ fv_bn_frees2
  
+  val _ = tracing ("fn_bn_map2 " ^ @{make_string} fv_bn_map2)
+  val _ = tracing ("fn_bn_map3 " ^ @{make_string} fv_bn_map3)
+
   val constrs_info = all_dtyp_constrs_types dt_descr sorts
 
-  val fv_eqs2 = map2 (map2 (make_fv_eq lthy fv_map fv_bn_map2)) constrs_info bclausesss 
-  val fv_bn_eqs2 = map (make_fv_bn_eqs lthy fv_map fv_bn_map3 constrs_info bclausesss) bn_funs2
+  val fv_eqs2 = map2 (map2 (mk_fv_eq lthy fv_map fv_bn_map2)) constrs_info bclausesss 
+  val fv_bn_eqs2 = map (mk_fv_bn_eqs lthy fv_map fv_bn_map3 constrs_info bclausesss) bn_funs2
   
+  val _ = tracing ("functions to be defined\n " ^ @{make_string} (fv_names @ fv_bn_names2))
+  val _ = tracing ("equations\n " ^ cat_lines (map (Syntax.string_of_term lthy) (flat fv_eqs2 @ flat fv_bn_eqs2)))
+
   val all_fv_names = map (fn s => (Binding.name s, NONE, NoSyn)) (fv_names @ fv_bn_names2)
   val all_fv_eqs = map (pair Attrib.empty_binding) (flat fv_eqs2 @ flat fv_bn_eqs2)