--- a/Nominal-General/nominal_library.ML	Wed May 19 12:44:03 2010 +0100
+++ b/Nominal-General/nominal_library.ML	Thu May 20 21:23:53 2010 +0100
@@ -6,6 +6,8 @@
 
 signature NOMINAL_LIBRARY =
 sig
+  val dest_listT: typ -> typ
+
   val mk_minus: term -> term
   val mk_plus: term -> term -> term
 
@@ -25,12 +27,25 @@
 
   val mk_equiv: thm -> thm
   val safe_mk_equiv: thm -> thm
+
+  (* datatype operations *)
+  val nth_dtyp: Datatype_Aux.descr -> (string * sort) list -> int -> typ
+  val all_dtyp_constrs_types: Datatype_Aux.descr -> (string * sort) list -> 
+    (term * typ * typ list) list list
+  val nth_dtyp_constrs_types: Datatype_Aux.descr -> (string * sort) list -> int -> 
+    (term * typ * typ list) list
+  val prefix_dt_names: Datatype_Aux.descr -> (string * sort) list -> string -> string list
+
 end
 
 
 structure Nominal_Library: NOMINAL_LIBRARY =
 struct
 
+(* this function should be in hologic.ML *)
+fun dest_listT (Type (@{type_name list}, [T])) = T
+  | dest_listT T = raise TYPE ("dest_listT: list type expected", [T], [])
+
 fun mk_minus p = @{term "uminus::perm => perm"} $ p;
 
 fun mk_plus p q = @{term "plus::perm => perm => perm"} $ p $ q;
@@ -59,6 +74,49 @@
 fun safe_mk_equiv r = mk_equiv r handle Thm.THM _ => r;
 
 
+(** datatypes **)
+
+
+(* returns the type of the nth datatype *)
+fun nth_dtyp descr sorts n = 
+  Datatype_Aux.typ_of_dtyp descr sorts (Datatype_Aux.DtRec n);
+
+(* returns info about constructors in a datatype *)
+fun all_dtyp_constrs_info descr = 
+  map (fn (_, (ty, vs, constrs)) => map (pair (ty, vs)) constrs) descr
+
+(* returns the constants of the constructors plus the 
+   corresponding type and types of arguments *)
+fun all_dtyp_constrs_types descr sorts = 
+let
+  fun aux ((ty_name, vs), (cname, args)) =
+  let
+    val vs_tys = map (Datatype_Aux.typ_of_dtyp descr sorts) vs
+    val ty = Type (ty_name, vs_tys)
+    val arg_tys = map (Datatype_Aux.typ_of_dtyp descr sorts) args
+  in
+    (Const (cname, arg_tys ---> ty), ty, arg_tys)
+  end
+in
+  map (map aux) (all_dtyp_constrs_info descr)
+end
+
+fun nth_dtyp_constrs_types descr sorts n =
+  nth (all_dtyp_constrs_types descr sorts) n
+
+
+(* generates for every datatype a name str ^ dt_name 
+   plus and index for multiple occurences of a string *)
+fun prefix_dt_names descr sorts str = 
+let
+  fun get_nth_name (i, _) = 
+    Datatype_Aux.name_of_typ (nth_dtyp descr sorts i) 
+in
+  Datatype_Prop.indexify_names 
+    (map (prefix str o get_nth_name) descr)
+end
+
+
 end (* structure *)
 
 open Nominal_Library;
\ No newline at end of file

--- a/Nominal/Equivp.thy	Wed May 19 12:44:03 2010 +0100
+++ b/Nominal/Equivp.thy	Thu May 20 21:23:53 2010 +0100
@@ -194,7 +194,7 @@
     else mk_supp ty x
   val lhss = map mk_supp_arg (frees ~~ tys)
   val supports = Const(@{const_name "supports"}, @{typ "atom set"} --> ty --> @{typ bool})
-  val eq = HOLogic.mk_Trueprop (supports $ mk_union lhss $ rhs)
+  val eq = HOLogic.mk_Trueprop (supports $ fold_union lhss $ rhs)
 in
   (names, eq)
 end
@@ -203,7 +203,7 @@
 ML {*
 fun prove_supports ctxt perms cnst =
 let
-  val (names, eq) = mk_supports_eq (ProofContext.theory_of ctxt) cnst
+  val (names, eq) = mk_supports_eq ctxt cnst
 in
   Goal.prove ctxt names [] eq (fn _ => supports_tac perms 1)
 end

--- a/Nominal/Ex/SingleLet.thy	Wed May 19 12:44:03 2010 +0100
+++ b/Nominal/Ex/SingleLet.thy	Thu May 20 21:23:53 2010 +0100
@@ -4,6 +4,9 @@
 
 atom_decl name
 
+ML {* print_depth 50 *}
+declare [[STEPS = 19]]
+
 nominal_datatype trm =
   Var "name"
 | App "trm" "trm"
@@ -16,6 +19,8 @@
 where
   "bn (As x t) = {atom x}"
 
+thm fv_trm_raw.simps[no_vars] fv_assg_raw.simps[no_vars] fv_bn_raw.simps[no_vars]
+
 ML {* Inductive.the_inductive *}
 thm trm_assg.fv
 thm trm_assg.supp
@@ -26,8 +31,10 @@
 thm trm_assg.inducts
 thm trm_assg.distinct
 ML {* Sign.of_sort @{theory} (@{typ trm}, @{sort fs}) *}
+
+(* TEMPORARY
 thm trm_assg.fv[simplified trm_assg.supp(1-2)]
-
+*)
 
 
 

--- a/Nominal/Ex/Test.thy	Wed May 19 12:44:03 2010 +0100
+++ b/Nominal/Ex/Test.thy	Thu May 20 21:23:53 2010 +0100
@@ -13,6 +13,7 @@
 
 thm fv_trm_raw.simps[no_vars]
 *)
+
 (* This file contains only the examples that are not supposed to work yet. *)
 
 
@@ -29,7 +30,6 @@
 | Ap "trm" "trm list"
 | Lm x::"name" t::"trm"  bind x in t
 
-
 (*
 thm alpha_trm4_raw_alpha_trm4_raw_list.intros[no_vars]
 thm fv_trm4_raw_fv_trm4_raw_list.simps[no_vars]

--- a/Nominal/NewAlpha.thy	Wed May 19 12:44:03 2010 +0100
+++ b/Nominal/NewAlpha.thy	Thu May 20 21:23:53 2010 +0100
@@ -1,7 +1,18 @@
 theory NewAlpha
-imports "NewFv"
+imports "Abs" "Perm" "Nominal2_FSet"
+uses ("nominal_dt_rawperm.ML")
+     ("nominal_dt_rawfuns.ML")
 begin
 
+use "nominal_dt_rawperm.ML"
+use "nominal_dt_rawfuns.ML"
+
+ML {*
+open Nominal_Dt_RawPerm
+open Nominal_Dt_RawFuns
+*}
+
+
 ML {*
 fun mk_binop2 ctxt s (l, r) =
   Syntax.check_term ctxt (Const (s, dummyT) $ l $ r)
@@ -16,17 +27,16 @@
 fun alpha_bm_lsts lthy dt_descr sorts dts args args2 alpha_frees fv_frees
   bn_alphabn alpha_const binds bodys =
 let
-  val thy = ProofContext.theory_of lthy;
-  fun bind_set args (NONE, no) = setify thy (nth args no)
+  fun bind_set args (NONE, no) = setify lthy (nth args no)
     | bind_set args (SOME f, no) = f $ (nth args no)
-  fun bind_lst args (NONE, no) = listify thy (nth args no)
+  fun bind_lst args (NONE, no) = listify lthy (nth args no)
     | bind_lst args (SOME f, no) = f $ (nth args no)
   fun append (t1, t2) =
     Const(@{const_name append}, @{typ "atom list \<Rightarrow> atom list \<Rightarrow> atom list"}) $ t1 $ t2;
   fun binds_fn args nos =
     if alpha_const = @{const_name alpha_lst}
     then foldr1 append (map (bind_lst args) nos)
-    else mk_union (map (bind_set args) nos);
+    else fold_union (map (bind_set args) nos);
   val lhs_binds = binds_fn args binds;
   val rhs_binds = binds_fn args2 binds;
   val lhs_bodys = foldr1 HOLogic.mk_prod (map (nth args) bodys);
@@ -64,7 +74,7 @@
 ML {*
 fun alpha_bn_bm lthy dt_descr sorts dts args args2 alpha_frees fv_frees bn_alphabn args_in_bn bm =
 case bm of
-  BEmy i =>
+  BC (_, [], [i]) =>
     let
       val arg = nth args i;
       val arg2 = nth args2 i;
@@ -77,11 +87,11 @@
       | SOME (SOME (f : term)) => [(the (AList.lookup (op=) bn_alphabn f)) $ arg $ arg2]
       | SOME NONE => []
     end
-| BLst (x, y) => alpha_bm_lsts lthy dt_descr sorts dts args args2 alpha_frees
+| BC (Lst, x, y) => alpha_bm_lsts lthy dt_descr sorts dts args args2 alpha_frees
     fv_frees bn_alphabn @{const_name alpha_lst} x y
-| BSet (x, y) => alpha_bm_lsts lthy dt_descr sorts dts args args2 alpha_frees
+| BC (Set, x, y) => alpha_bm_lsts lthy dt_descr sorts dts args args2 alpha_frees
     fv_frees bn_alphabn @{const_name alpha_gen} x y
-| BRes (x, y) => alpha_bm_lsts lthy dt_descr sorts dts args args2 alpha_frees
+| BC (Res, x, y) => alpha_bm_lsts lthy dt_descr sorts dts args args2 alpha_frees
     fv_frees bn_alphabn @{const_name alpha_res} x y
 *}
 
@@ -137,7 +147,7 @@
 ML {*
 fun alpha_bm lthy dt_descr sorts dts args args2 alpha_frees fv_frees bn_alphabn bm =
 case bm of
-  BEmy i =>
+  BC (_, [], [i]) =>
     let
       val arg = nth args i;
       val arg2 = nth args2 i;
@@ -147,11 +157,11 @@
       then [(nth alpha_frees (Datatype_Aux.body_index dt)) $ arg $ arg2]
       else [HOLogic.mk_eq (arg, arg2)]
     end
-| BLst (x, y) => alpha_bm_lsts lthy dt_descr sorts dts args args2 alpha_frees
+| BC (Lst, x, y) => alpha_bm_lsts lthy dt_descr sorts dts args args2 alpha_frees
     fv_frees bn_alphabn @{const_name alpha_lst} x y
-| BSet (x, y) => alpha_bm_lsts lthy dt_descr sorts dts args args2 alpha_frees
+| BC (Set, x, y) => alpha_bm_lsts lthy dt_descr sorts dts args args2 alpha_frees
     fv_frees bn_alphabn @{const_name alpha_gen} x y
-| BRes (x, y) => alpha_bm_lsts lthy dt_descr sorts dts args args2 alpha_frees
+| BC (Res, x, y) => alpha_bm_lsts lthy dt_descr sorts dts args args2 alpha_frees
     fv_frees bn_alphabn @{const_name alpha_res} x y
 *}
 

--- a/Nominal/NewFv.thy	Wed May 19 12:44:03 2010 +0100
+++ b/Nominal/NewFv.thy	Thu May 20 21:23:53 2010 +0100
@@ -4,38 +4,42 @@
 begin
 
 ML {*
-(* binding modes *)
+(* binding modes  and binding clauses *)
 
-datatype bmodes =
-   BEmy of int
-|  BLst of ((term option * int) list) * (int list)
-|  BSet of ((term option * int) list) * (int list)
-|  BRes of ((term option * int) list) * (int list)
+datatype bmode = Lst | Res | Set
+
+datatype bclause =
+  BC of bmode * (term option * int) list * int list
 *}
 
 ML {*
-fun mk_singleton_atom x = HOLogic.mk_set @{typ atom} [mk_atom x];
-
-val noatoms = @{term "{} :: atom set"};
+fun mk_diff (@{term "{}::atom set"}, _) = @{term "{}::atom set"}
+  | mk_diff (t1, @{term "{}::atom set"}) = t1
+  | mk_diff (t1, t2) = HOLogic.mk_binop @{const_name minus} (t1, t2)
 
-fun mk_union sets =
-  fold (fn a => fn b =>
-  if a = noatoms then b else
-  if b = noatoms then a else
-  if a = b then a else
-  HOLogic.mk_binop @{const_name sup} (a, b)) (rev sets) noatoms;
+fun mk_union (@{term "{}::atom set"}, @{term "{}::atom set"}) = @{term "{}::atom set"}
+  | mk_union (t1 , @{term "{}::atom set"}) = t1
+  | mk_union (@{term "{}::atom set"}, t2) = t2
+  | mk_union (t1, t2) = HOLogic.mk_binop @{const_name sup} (t1, t2)  
+ 
+fun fold_union trms = fold (curry mk_union) trms @{term "{}::atom set"}
 *}
 
 ML {*
-fun is_atom thy ty =
-  Sign.of_sort thy (ty, @{sort at_base})
+fun is_atom ctxt ty =
+  Sign.of_sort (ProofContext.theory_of ctxt) (ty, @{sort at_base})
 
-fun is_atom_set thy (Type ("fun", [t, @{typ bool}])) = is_atom thy t
+fun is_atom_set ctxt (Type ("fun", [t, @{typ bool}])) = is_atom ctxt t
   | is_atom_set _ _ = false;
 
-fun is_atom_fset thy (Type ("FSet.fset", [t])) = is_atom thy t
+fun is_atom_fset ctxt (Type (@{type_name "fset"}, [t])) = is_atom ctxt t
   | is_atom_fset _ _ = false;
 
+fun is_atom_list ctxt (Type (@{type_name "list"}, [t])) = is_atom ctxt t
+  | is_atom_list _ _ = false
+*}
+
+ML {*
 fun mk_atom_set t =
 let
   val ty = fastype_of t;
@@ -55,23 +59,6 @@
   fset_to_set $ (Const (@{const_name fmap}, fmap_ty) $ Const (@{const_name atom}, atom_ty) $ t)
 end;
 
-fun mk_diff a b =
-  if b = noatoms then a else
-  if b = a then noatoms else
-  HOLogic.mk_binop @{const_name minus} (a, b);
-*}
-
-ML {*
-fun is_atom_list (Type (@{type_name list}, [T])) = true
-  | is_atom_list _ = false
-*}
-
-ML {*
-fun dest_listT (Type (@{type_name list}, [T])) = T
-  | dest_listT T = raise TYPE ("dest_listT: list type expected", [T], [])
-*}
-
-ML {*
 fun mk_atom_list t =
 let
   val ty = fastype_of t;
@@ -83,191 +70,170 @@
 *}
 
 ML {*
-fun setify thy t =
+fun setify ctxt t =
 let
   val ty = fastype_of t;
 in
-  if is_atom thy ty
-    then mk_singleton_atom t
-  else if is_atom_set thy ty
+  if is_atom ctxt ty
+    then  HOLogic.mk_set @{typ atom} [mk_atom t]
+  else if is_atom_set ctxt ty
     then mk_atom_set t
-  else if is_atom_fset thy ty
+  else if is_atom_fset ctxt ty
     then mk_atom_fset t
   else error ("setify" ^ (PolyML.makestring (t, ty)))
 end
 *}
 
 ML {*
-fun listify thy t =
+fun listify ctxt t =
 let
   val ty = fastype_of t;
 in
-  if is_atom thy ty
+  if is_atom ctxt ty
     then HOLogic.mk_list @{typ atom} [mk_atom t]
-  else if is_atom_list ty
+  else if is_atom_list ctxt ty
     then mk_atom_set t
   else error "listify"
 end
 *}
 
 ML {*
-fun set x =
+fun to_set x =
   if fastype_of x = @{typ "atom list"}
   then @{term "set::atom list \<Rightarrow> atom set"} $ x
   else x
 *}
 
 ML {*
-fun fv_body thy dts args fv_frees supp i =
+fun make_body fv_map args i = 
 let
-  val x = nth args i;
-  val dt = nth dts i;
+  val arg = nth args i
+  val ty = fastype_of arg
 in
-  if Datatype_Aux.is_rec_type dt
-  then nth fv_frees (Datatype_Aux.body_index dt) $ x
-  else (if supp then mk_supp x else setify thy x)
-end
+  case (AList.lookup (op=) fv_map ty) of
+    NONE => mk_supp arg
+  | SOME fv => fv $ arg
+end  
 *}
 
 ML {*
-fun fv_bm_lsts thy dts args fv_frees bn_fvbn binds bodys =
+fun make_binder lthy fv_bn_map args (bn_option, i) = 
 let
-  val fv_bodys = mk_union (map (fv_body thy dts args fv_frees true) bodys)
-  fun bound_var (SOME bn, i) = set (bn $ nth args i)
-    | bound_var (NONE, i) = fv_body thy dts args fv_frees false i
-  val bound_vars = mk_union (map bound_var binds);
-  fun non_rec_var (SOME bn, i) =
-      if member (op =) bodys i
-      then noatoms
-      else ((the (AList.lookup (op=) bn_fvbn bn)) $ nth args i)
-    | non_rec_var (NONE, _) = noatoms
+  val arg = nth args i
 in
-  mk_union ((mk_diff fv_bodys bound_vars) :: (map non_rec_var binds))
+  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  
+*}
+
+ML {*
+fun make_fv_rhs lthy fv_map fv_bn_map args (BC (_, binders, bodies)) =
+let
+  val t1 = map (make_body fv_map args) bodies
+  val (t2, t3) = split_list (map (make_binder lthy fv_bn_map args) binders)
+in 
+  fold_union (mk_diff (fold_union t1, fold_union t2)::t3)
 end
 *}
 
 ML {*
-fun fv_bn_bm thy dts args fv_frees bn_fvbn args_in_bn bm =
-case bm of
-  BEmy i =>
-    let
-      val x = nth args i;
-      val dt = nth dts i;
-    in
-      case AList.lookup (op=) args_in_bn i of
-        NONE => if Datatype_Aux.is_rec_type dt
-                then nth fv_frees (Datatype_Aux.body_index dt) $ x
-                else mk_supp x
-      | SOME (SOME (f : term)) => (the (AList.lookup (op=) bn_fvbn f)) $ x
-      | SOME NONE => noatoms
-    end
-| BLst (x, y) => fv_bm_lsts thy dts args fv_frees bn_fvbn x y
-| BSet (x, y) => fv_bm_lsts thy dts args fv_frees bn_fvbn x y
-| BRes (x, y) => fv_bm_lsts thy dts args fv_frees bn_fvbn x y
-*}
-
-ML {*
-fun fv_bn thy dt_descr sorts fv_frees bn_fvbn bclausess (fvbn, (_, ith_dtyp, args_in_bns)) =
+fun make_fv_eq lthy fv_map fv_bn_map (constr, ty, arg_tys) bclauses = 
 let
-  fun fv_bn_constr (cname, dts) (args_in_bn, bclauses) =
-  let
-    val Ts = map (Datatype_Aux.typ_of_dtyp dt_descr sorts) dts;
-    val names = Datatype_Prop.make_tnames Ts;
-    val args = map Free (names ~~ Ts);
-    val c = Const (cname, Ts ---> (nth_dtyp dt_descr sorts ith_dtyp));
-    val fv_bn_bm = fv_bn_bm thy dts args fv_frees bn_fvbn args_in_bn
-  in
-    HOLogic.mk_Trueprop (HOLogic.mk_eq
-      (fvbn $ list_comb (c, args), mk_union (map fv_bn_bm bclauses)))
-  end;
-  val (_, (_, _, constrs)) = nth dt_descr ith_dtyp;
+  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
-  map2 fv_bn_constr constrs (args_in_bns ~~ bclausess)
+  HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
 end
 *}
 
 ML {*
-fun fv_bns thy dt_descr sorts fv_frees bn_funs bclausesss =
+fun make_bn_body fv_map fv_bn_map bn_args args i = 
 let
-  fun mk_fvbn_free (bn, ith, _) =
-    let
-      val fvbn_name = "fv_" ^ (Long_Name.base_name (fst (dest_Const bn)));
-    in
-      (fvbn_name, Free (fvbn_name, fastype_of (nth fv_frees ith)))
-    end;
+  val arg = nth args i
+  val ty = fastype_of arg
+in
+  case AList.lookup (op=) bn_args i of
+    NONE => (case (AList.lookup (op=) fv_map ty) of
+              NONE => mk_supp arg
+            | SOME fv => fv $ arg)
+  | SOME (NONE) => @{term "{}::atom set"}
+  | SOME (SOME bn) => the (AList.lookup (op=) fv_bn_map bn) $ arg
+end  
+*}
 
-  val (fvbn_names, fvbn_frees) = split_list (map mk_fvbn_free bn_funs);
-  val bn_fvbn = (map (fn (bn, _, _) => bn) bn_funs) ~~ fvbn_frees
-  val bclausessl = map (fn (_, i, _) => nth bclausesss i) bn_funs;
-  val eqs = map2 (fv_bn thy dt_descr sorts fv_frees bn_fvbn) bclausessl (fvbn_frees ~~ bn_funs);
+ML {*
+fun make_fv_bn_rhs lthy fv_map fv_bn_map bn_args args bclause =
+  case bclause of
+    BC (_, [], bodies) => fold_union (map (make_bn_body fv_map fv_bn_map bn_args args) bodies)
+  | BC (_, binders, bodies) => 
+      let
+        val t1 = map (make_body fv_map args) bodies
+        val (t2, t3) = split_list (map (make_binder lthy fv_bn_map args) binders)
+      in 
+        fold_union (mk_diff (fold_union t1, fold_union t2)::t3)
+      end
+*}
+
+ML {*
+fun make_fv_bn_eq lthy bn_trm fv_map fv_bn_map (bn_args, (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_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 = fold_union rhs_trms
 in
-  (bn_fvbn, fvbn_names, eqs)
+  HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
 end
 *}
 
 ML {*
-fun fv_bm thy dts args fv_frees bn_fvbn bm =
-case bm of
-  BEmy i =>
-    let
-      val x = nth args i;
-      val dt = nth dts i;
-    in
-      if Datatype_Aux.is_rec_type dt
-      then nth fv_frees (Datatype_Aux.body_index dt) $ x
-      else mk_supp x
-    end
-| BLst (x, y) => fv_bm_lsts thy dts args fv_frees bn_fvbn x y
-| BSet (x, y) => fv_bm_lsts thy dts args fv_frees bn_fvbn x y
-| BRes (x, y) => fv_bm_lsts thy dts args fv_frees bn_fvbn x y
-*}
-
-ML {*
-fun fv thy dt_descr sorts fv_frees bn_fvbn bclausess (fv_free, ith_dtyp) =
+fun make_fv_bn_eqs lthy fv_map fv_bn_map constrs_info bclausesss (bn_trm, bn_n, bn_argss) = 
 let
-  fun fv_constr (cname, dts) bclauses =
-  let
-    val Ts = map (Datatype_Aux.typ_of_dtyp dt_descr sorts) dts;
-    val names = Datatype_Prop.make_tnames Ts;
-    val args = map Free (names ~~ Ts);
-    val c = Const (cname, Ts ---> (nth_dtyp dt_descr sorts ith_dtyp));
-    val fv_bn_bm = fv_bm thy dts args fv_frees bn_fvbn
-  in
-    HOLogic.mk_Trueprop (HOLogic.mk_eq
-      (fv_free $ list_comb (c, args), mk_union (map fv_bn_bm bclauses)))
-  end;
-  val (_, (_, _, constrs)) = nth dt_descr ith_dtyp;
+  val nth_constrs_info = nth constrs_info bn_n
+  val nth_bclausess = nth bclausesss bn_n
 in
-  map2 fv_constr constrs bclausess
+  map2 (make_fv_bn_eq lthy bn_trm fv_map fv_bn_map) (bn_argss ~~ nth_constrs_info) nth_bclausess
 end
 *}
 
 ML {*
-fun define_raw_fvs dt_descr sorts bn_funs bclausesss lthy =
+fun define_raw_fvs dt_descr sorts bn_funs bn_funs2 bclausesss lthy =
 let
-  val thy = ProofContext.theory_of lthy;
 
   val fv_names = prefix_dt_names dt_descr sorts "fv_"
-  val fv_types = map (fn (i, _) => nth_dtyp dt_descr sorts i --> @{typ "atom set"}) dt_descr;
-  val fv_frees = map Free (fv_names ~~ fv_types);
+  val fv_arg_tys = map (fn (i, _) => nth_dtyp dt_descr sorts i) dt_descr;
+  val fv_tys = map (fn ty => ty --> @{typ "atom set"}) fv_arg_tys;
+  val fv_frees = map Free (fv_names ~~ fv_tys);
+  val fv_map = fv_arg_tys ~~ fv_frees
 
-  (* free variables for the bn-functions *)
-  val (bn_fvbn_map, fv_bn_names, fv_bn_eqs) =
-    fv_bns thy dt_descr sorts fv_frees bn_funs bclausesss;
+  val (bns, bn_tys) = split_list (map (fn (bn, i, _) => (bn, i)) bn_funs)
+  val (bns2, bn_tys2) = split_list (map (fn (bn, i, _) => (bn, i)) bn_funs2)
+  val bn_args2 = map (fn (_, _, arg) => arg) bn_funs2
+  val fv_bn_names2 = map (fn bn => "fv_" ^ (fst (dest_Free bn))) bns2
+  val fv_bn_arg_tys2 = map (fn i => nth_dtyp dt_descr sorts i) bn_tys2
+  val fv_bn_tys2 = map (fn ty => ty --> @{typ "atom set"}) fv_bn_arg_tys2
+  val fv_bn_frees2 = map Free (fv_bn_names2 ~~ fv_bn_tys2)
+  val fv_bn_map2 = bns ~~ fv_bn_frees2
+  val fv_bn_map3 = bns2 ~~ fv_bn_frees2
+ 
+  val constrs_info = all_dtyp_constrs_types dt_descr sorts
 
-  val _ = tracing ("bn_fvbn_map" ^ commas (map @{make_string} bn_fvbn_map))
+  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_bns = map snd bn_fvbn_map;
-  val fv_nums = 0 upto (length fv_frees - 1)
-
-  val fv_eqs = map2 (fv thy dt_descr sorts fv_frees bn_fvbn_map) bclausesss (fv_frees ~~ fv_nums);
+  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)
 
-  val all_fv_names = map (fn s => (Binding.name s, NONE, NoSyn)) (fv_names @ fv_bn_names)
-  val all_fv_eqs = map (pair Attrib.empty_binding) (flat fv_eqs @ flat fv_bn_eqs)
-
-  fun pat_completeness_auto ctxt =
-    Pat_Completeness.pat_completeness_tac ctxt 1
-      THEN auto_tac (clasimpset_of ctxt)
+  fun pat_completeness_auto lthy =
+    Pat_Completeness.pat_completeness_tac lthy 1
+      THEN auto_tac (clasimpset_of lthy)
 
   fun prove_termination lthy =
     Function.prove_termination NONE
@@ -290,21 +256,8 @@
 end
 *}
 
-(**************************************************)
 
-datatype foo =
-  C1 nat
-| C2 foo int
 
-(*
-ML {* 
-fun mk_body descr sorts fv_ty_map dtyp =
-let
-  val nth_dtyp_constr_tys descr sorts
-in
-  true
-end
-*}
-*)
+
 
 end

--- a/Nominal/NewParser.thy	Wed May 19 12:44:03 2010 +0100
+++ b/Nominal/NewParser.thy	Thu May 20 21:23:53 2010 +0100
@@ -2,9 +2,10 @@
 imports "../Nominal-General/Nominal2_Base" 
         "../Nominal-General/Nominal2_Eqvt" 
         "../Nominal-General/Nominal2_Supp" 
-        "Perm" "NewFv" "NewAlpha" "Tacs" "Equivp" "Lift"
+        "Perm" "NewAlpha" "Tacs" "Equivp" "Lift"
 begin
 
+
 section{* Interface for nominal_datatype *}
 
 
@@ -154,10 +155,7 @@
   fun rawify_bnds bnds = 
     map (apfst (Option.map (replace_term (cnstrs_env @ bn_fun_env) dts_env))) bnds
 
-  fun rawify_bclause (BEmy n) = BEmy n
-    | rawify_bclause (BLst (bnds, bdys)) = BLst (rawify_bnds bnds, bdys)
-    | rawify_bclause (BSet (bnds, bdys)) = BSet (rawify_bnds bnds, bdys)
-    | rawify_bclause (BRes (bnds, bdys)) = BRes (rawify_bnds bnds, bdys)
+  fun rawify_bclause (BC (mode, bnds, bdys)) = BC (mode, rawify_bnds bnds, bdys)
 in
   map (map (map rawify_bclause)) bclauses
 end
@@ -219,9 +217,9 @@
   val ordered = map (fn (x, y) => (x, map (fn (v, z) => (v, order dts x z)) y)) unordered' 
   val ordered' = flat (map (fn (ith, l) => map (fn (bn, data) => (bn, ith, data)) l) ordered)
 
-  val _ = tracing ("eqs\n" ^ cat_lines (map (Syntax.string_of_term lthy) eqs))
+  (*val _ = tracing ("eqs\n" ^ cat_lines (map (Syntax.string_of_term lthy) eqs))*)
   (*val _ = tracing ("map eqs\n" ^ @{make_string} (map aux2 eqs))*)
-  val _ = tracing ("ordered'\n" ^ @{make_string} ordered')
+  (*val _ = tracing ("ordered'\n" ^ @{make_string} ordered')*)
 in
   ordered'
 end
@@ -263,7 +261,7 @@
   fun export_fun f (t, n , l) = (f t, n, map (map (apsnd (Option.map f))) l);
   val bn_funs_decls = map (export_fun (Morphism.term morphism_2_0)) raw_bns;
 in
-  (raw_dt_names, raw_bn_eqs, raw_bclauses, bn_funs_decls, lthy2)
+  (raw_dt_names, raw_bn_eqs, raw_bclauses, bn_funs_decls, raw_bns, lthy2)
 end
 *}
 
@@ -372,10 +370,13 @@
 fun nominal_datatype2 dts bn_funs bn_eqs bclauses lthy =
 let
   (* definition of the raw datatypes and raw bn-functions *)
-  val (raw_dt_names, raw_bn_eqs, raw_bclauses, raw_bns, lthy1) =
+  val (raw_dt_names, raw_bn_eqs, raw_bclauses, raw_bns, raw_bns2, lthy1) =
     if get_STEPS lthy > 1 then raw_nominal_decls dts bn_funs bn_eqs bclauses lthy
     else raise TEST lthy
 
+  (*val _ = tracing ("exported: " ^ commas (map @{make_string} raw_bns))*)
+  (*val _ = tracing ("plain: " ^ commas (map @{make_string} raw_bns2))*)
+
   val dtinfo = Datatype.the_info (ProofContext.theory_of lthy1) (hd raw_dt_names)
   val {descr, sorts, ...} = dtinfo
   val all_tys = map (fn (i, _) => nth_dtyp descr sorts i) descr
@@ -408,7 +409,7 @@
 
   val (fv, fvbn, fv_def, lthy3a) = 
     if get_STEPS lthy2 > 3 
-    then define_raw_fvs descr sorts raw_bns raw_bclauses lthy3
+    then define_raw_fvs descr sorts raw_bns raw_bns2 raw_bclauses lthy3
     else raise TEST lthy3
   
   (* definition of raw alphas *)
@@ -431,7 +432,8 @@
   (* definition of raw_alpha_eq_iff  lemmas *)
   val alpha_eq_iff = build_rel_inj alpha_intros (inject_thms @ distinct_thms) alpha_cases lthy4
   val alpha_eq_iff_simp = map remove_loop alpha_eq_iff;
-  val _ = map tracing (map PolyML.makestring alpha_eq_iff_simp);
+  
+  (*val _ = map tracing (map PolyML.makestring alpha_eq_iff_simp);*)
 
   (* proving equivariance lemmas *)
   val _ = warning "Proving equivariance";
@@ -639,16 +641,16 @@
  
   fun prep_body env bn_str = index_lookup env bn_str
 
-  fun prep_mode "bind"     = BLst 
-    | prep_mode "bind_set" = BSet 
-    | prep_mode "bind_res" = BRes 
+  fun prep_mode "bind"     = Lst 
+    | prep_mode "bind_set" = Set 
+    | prep_mode "bind_res" = Res 
 
   fun prep_bclause env (mode, binders, bodies) = 
   let
     val binders' = map (prep_binder env) binders
     val bodies' = map (prep_body env) bodies
   in  
-    prep_mode mode (binders', bodies')
+    BC (prep_mode mode, binders', bodies')
   end
 
   fun prep_bclauses (annos, bclause_strs) = 
@@ -670,10 +672,7 @@
 ML {*
 fun included i bcs = 
 let
-  fun incl (BEmy j) = i = j
-    | incl (BLst (bns, bds)) = (member (op =) (map snd bns) i) orelse (member (op =) bds i)
-    | incl (BSet (bns, bds)) = (member (op =) (map snd bns) i) orelse (member (op =) bds i)
-    | incl (BRes (bns, bds)) = (member (op =) (map snd bns) i) orelse (member (op =) bds i)
+  fun incl (BC (_, bns, bds)) = (member (op =) (map snd bns) i) orelse (member (op =) bds i)
 in
   exists incl bcs 
 end
@@ -688,7 +687,7 @@
 
   fun complt n bcs = 
   let
-    fun add bcs i = (if included i bcs then [] else [BEmy i]) 
+    fun add bcs i = (if included i bcs then [] else [BC (Lst, [], [i])]) 
   in
     bcs @ (flat (map_range (add bcs) n))
   end

--- a/Nominal/Perm.thy	Wed May 19 12:44:03 2010 +0100
+++ b/Nominal/Perm.thy	Thu May 20 21:23:53 2010 +0100
@@ -1,180 +1,9 @@
 theory Perm
-imports "../Nominal-General/Nominal2_Atoms"
+imports 
+  "../Nominal-General/Nominal2_Base"
+  "../Nominal-General/Nominal2_Atoms"
 begin
 
-(* definitions of the permute function for raw nominal datatypes *)
-
-
-ML {*
-(* returns the type of the nth datatype *)
-fun nth_dtyp descr sorts n = 
-  Datatype_Aux.typ_of_dtyp descr sorts (Datatype_Aux.DtRec n);
-
-(* returns the constructors of the nth datatype *)
-fun nth_dtyp_constrs descr n = 
-let
-  val (_, (_, _, constrs)) = nth descr n
-in
-  constrs
-end
-
-(* returns the types of the constructors of the nth datatype *)
-fun nth_dtyp_constr_typs descr sorts n = 
-  map (map (Datatype_Aux.typ_of_dtyp descr sorts) o snd) (nth_dtyp_constrs descr n)
-*}
-
-ML {*
-(* generates for every datatype a name str ^ dt_name 
-   plus and index for multiple occurences of a string *)
-fun prefix_dt_names descr sorts str = 
-let
-  fun get_nth_name (i, _) = 
-    Datatype_Aux.name_of_typ (nth_dtyp descr sorts i) 
-in
-  Datatype_Prop.indexify_names 
-    (map (prefix str o get_nth_name) descr)
-end
-*}
-
-
-ML {*
-(* permutation function for one argument 
-   
-    - in case the argument is recursive it returns 
-
-         permute_fn p arg
-
-    - in case the argument is non-recursive it will return
-
-         p o arg
-
-*)
-fun perm_arg permute_fn_frees p (arg_dty, arg) =
-  if Datatype_Aux.is_rec_type arg_dty 
-  then (nth permute_fn_frees (Datatype_Aux.body_index arg_dty)) $ p $ arg
-  else mk_perm p arg
-*}
-
-ML {*
-(* generates the equation for the permutation function for one constructor;
-   i is the index of the corresponding datatype *)
-fun perm_eq_constr dt_descr sorts permute_fn_frees i (cnstr_name, dts) =
-let
-  val p = Free ("p", @{typ perm})
-  val arg_tys = map (Datatype_Aux.typ_of_dtyp dt_descr sorts) dts
-  val arg_names = Name.variant_list ["p"] (Datatype_Prop.make_tnames arg_tys)
-  val args = map Free (arg_names ~~ arg_tys)
-  val cnstr = Const (cnstr_name, arg_tys ---> (nth_dtyp dt_descr sorts i))
-  val lhs = (nth permute_fn_frees i) $ p $ list_comb (cnstr, args)
-  val rhs = list_comb (cnstr, map (perm_arg permute_fn_frees p) (dts ~~ args))
-  val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
-in
-  (Attrib.empty_binding, eq)
-end
-*}
-
-ML {*
-(* proves the two pt-type class properties *)
-fun prove_permute_zero lthy induct perm_defs perm_fns =
-let
-  val perm_types = map (body_type o fastype_of) perm_fns
-  val perm_indnames = Datatype_Prop.make_tnames perm_types
-  
-  fun single_goal ((perm_fn, T), x) =
-    HOLogic.mk_eq (perm_fn $ @{term "0::perm"} $ Free (x, T), Free (x, T))
-
-  val goals =
-    HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
-      (map single_goal (perm_fns ~~ perm_types ~~ perm_indnames)))
-
-  val simps = HOL_basic_ss addsimps (@{thm permute_zero} :: perm_defs)
-
-  val tac = (Datatype_Aux.indtac induct perm_indnames 
-             THEN_ALL_NEW asm_simp_tac simps) 1
-in
-  Goal.prove lthy perm_indnames [] goals (K tac)
-  |> Datatype_Aux.split_conj_thm
-end
-*}
-
-ML {*
-fun prove_permute_plus lthy induct perm_defs perm_fns =
-let
-  val p = Free ("p", @{typ perm})
-  val q = Free ("q", @{typ perm})
-  val perm_types = map (body_type o fastype_of) perm_fns
-  val perm_indnames = Datatype_Prop.make_tnames perm_types
-  
-  fun single_goal ((perm_fn, T), x) = HOLogic.mk_eq 
-      (perm_fn $ (mk_plus p q) $ Free (x, T), perm_fn $ p $ (perm_fn $ q $ Free (x, T)))
-
-  val goals =
-    HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
-      (map single_goal (perm_fns ~~ perm_types ~~ perm_indnames)))
-
-  val simps = HOL_basic_ss addsimps (@{thm permute_plus} :: perm_defs)
-
-  val tac = (Datatype_Aux.indtac induct perm_indnames
-             THEN_ALL_NEW asm_simp_tac simps) 1
-in
-  Goal.prove lthy ("p" :: "q" :: perm_indnames) [] goals (K tac)
-  |> Datatype_Aux.split_conj_thm 
-end
-*}
-
-ML {*
-(* defines the permutation functions for raw datatypes and
-   proves that they are instances of pt
-
-   user_dt_nos refers to the number of "un-unfolded" datatypes
-   given by the user
-*)
-fun define_raw_perms dt_descr sorts induct_thm user_dt_nos thy =
-let
-  val all_full_tnames = map (fn (_, (n, _, _)) => n) dt_descr;
-  val user_full_tnames = List.take (all_full_tnames, user_dt_nos);
-
-  val perm_fn_names = prefix_dt_names dt_descr sorts "permute_"
-  val perm_fn_types = map (fn (i, _) => perm_ty (nth_dtyp dt_descr sorts i)) dt_descr
-  val perm_fn_frees = map Free (perm_fn_names ~~ perm_fn_types)
-
-  fun perm_eq (i, (_, _, constrs)) = 
-    map (perm_eq_constr dt_descr sorts perm_fn_frees i) constrs;
-
-  val perm_eqs = maps perm_eq dt_descr;
-
-  val lthy =
-    Theory_Target.instantiation (user_full_tnames, [], @{sort pt}) thy;
-   
-  val ((perm_funs, perm_eq_thms), lthy') =
-    Primrec.add_primrec
-      (map (fn s => (Binding.name s, NONE, NoSyn)) perm_fn_names) perm_eqs lthy;
-    
-  val perm_zero_thms = prove_permute_zero lthy' induct_thm perm_eq_thms perm_funs
-  val perm_plus_thms = prove_permute_plus lthy' induct_thm perm_eq_thms perm_funs
-  val perm_zero_thms' = List.take (perm_zero_thms, user_dt_nos);
-  val perm_plus_thms' = List.take (perm_plus_thms, user_dt_nos)
-  val perms_name = space_implode "_" perm_fn_names
-  val perms_zero_bind = Binding.name (perms_name ^ "_zero")
-  val perms_plus_bind = Binding.name (perms_name ^ "_plus")
-  
-  fun tac _ (_, _, simps) =
-    Class.intro_classes_tac [] THEN ALLGOALS (resolve_tac simps)
-  
-  fun morphism phi (fvs, dfs, simps) =
-    (map (Morphism.term phi) fvs, map (Morphism.thm phi) dfs, map (Morphism.thm phi) simps);
-in
-  lthy'
-  |> snd o (Local_Theory.note ((perms_zero_bind, []), perm_zero_thms'))
-  |> snd o (Local_Theory.note ((perms_plus_bind, []), perm_plus_thms'))
-  |> Class_Target.prove_instantiation_exit_result morphism tac 
-       (perm_funs, perm_eq_thms, perm_zero_thms' @ perm_plus_thms')
-end
-*}
-
-
-
-
 
 (* permutations for quotient types *)
 

--- a/Nominal/ROOT.ML	Wed May 19 12:44:03 2010 +0100
+++ b/Nominal/ROOT.ML	Thu May 20 21:23:53 2010 +0100
@@ -14,6 +14,6 @@
     "Ex/ExPS3",
     "Ex/ExPS7",
     "Ex/CoreHaskell",
-    "Ex/Test",
-    "Manual/Term4"
+    "Ex/Test"(*,
+    "Manual/Term4"*)
     ];

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/nominal_dt_rawfuns.ML	Thu May 20 21:23:53 2010 +0100
@@ -0,0 +1,262 @@
+(*  Title:      nominal_dt_rawperm.ML
+    Author:     Cezary Kaliszyk
+    Author:     Christian Urban
+
+  Definitions of the raw bn, fv and fv_bn
+  functions
+*)
+
+signature NOMINAL_DT_RAWFUNS =
+sig
+  (* binding modes and binding clauses *)
+
+  datatype bmode = Lst | Res | Set
+
+  datatype bclause = BC of bmode * (term option * int) list * int list
+
+  val setify: Proof.context -> term -> term
+  val listify: Proof.context -> term -> term
+  val fold_union: term list -> 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
+end
+
+
+structure Nominal_Dt_RawFuns: NOMINAL_DT_RAWFUNS =
+struct
+
+datatype bmode = Lst | Res | Set
+datatype bclause = BC of bmode * (term option * int) list * int list
+
+(* functions that construct differences and unions
+   but avoid producing empty atom sets *)
+
+fun mk_diff (@{term "{}::atom set"}, _) = @{term "{}::atom set"}
+  | mk_diff (t1, @{term "{}::atom set"}) = t1
+  | mk_diff (t1, t2) = HOLogic.mk_binop @{const_name minus} (t1, t2)
+
+fun mk_union (@{term "{}::atom set"}, @{term "{}::atom set"}) = @{term "{}::atom set"}
+  | mk_union (t1 , @{term "{}::atom set"}) = t1
+  | mk_union (@{term "{}::atom set"}, t2) = t2
+  | mk_union (t1, t2) = HOLogic.mk_binop @{const_name sup} (t1, t2)  
+ 
+fun fold_union trms = fold (curry mk_union) trms @{term "{}::atom set"}
+
+
+(* atom types *)
+fun is_atom ctxt ty =
+  Sign.of_sort (ProofContext.theory_of ctxt) (ty, @{sort at_base})
+
+fun is_atom_set ctxt (Type ("fun", [t, @{typ bool}])) = is_atom ctxt t
+  | is_atom_set _ _ = false;
+
+fun is_atom_fset ctxt (Type (@{type_name "fset"}, [t])) = is_atom ctxt t
+  | is_atom_fset _ _ = false;
+
+fun is_atom_list ctxt (Type (@{type_name "list"}, [t])) = is_atom ctxt t
+  | is_atom_list _ _ = false
+
+
+(* functions for producing sets, fsets and lists *)
+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;
+
+fun mk_atom_fset t =
+let
+  val ty = fastype_of t;
+  val atom_ty = dest_fsetT ty --> @{typ atom};
+  val fmap_ty = atom_ty --> ty --> @{typ "atom fset"};
+  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;
+
+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;
+
+
+(* functions that coerces atoms, sets and fsets into atom sets ? *)
+fun setify ctxt t =
+let
+  val ty = fastype_of t;
+in
+  if is_atom ctxt ty
+    then  HOLogic.mk_set @{typ atom} [mk_atom t]
+  else if is_atom_set ctxt ty
+    then mk_atom_set t
+  else if is_atom_fset ctxt ty
+    then mk_atom_fset t
+  else raise TERM ("setify", [t])
+end
+
+(* functions that coerces atoms and lists into atom lists ? *)
+fun listify ctxt t =
+let
+  val ty = fastype_of t;
+in
+  if is_atom ctxt ty
+    then HOLogic.mk_list @{typ atom} [mk_atom t]
+  else if is_atom_list ctxt ty
+    then mk_atom_set t
+  else raise TERM ("listify", [t])
+end
+
+(* coerces a list into a set *)
+fun to_set x =
+  if fastype_of x = @{typ "atom list"}
+  then @{term "set::atom list => atom set"} $ x
+  else x
+
+
+
+fun make_body fv_map args i = 
+let
+  val arg = nth args i
+  val ty = fastype_of arg
+in
+  case (AList.lookup (op=) fv_map ty) of
+    NONE => mk_supp arg
+  | SOME fv => fv $ arg
+end  
+
+fun make_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_body fv_map args) bodies
+  val (t2, t3) = split_list (map (make_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_bn_body fv_map fv_bn_map bn_args args i = 
+let
+  val arg = nth args i
+  val ty = fastype_of arg
+in
+  case AList.lookup (op=) bn_args i of
+    NONE => (case (AList.lookup (op=) fv_map ty) of
+              NONE => mk_supp arg
+            | SOME fv => fv $ arg)
+  | SOME (NONE) => @{term "{}::atom set"}
+  | 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 =
+  case bclause of
+    BC (_, [], bodies) => fold_union (map (make_bn_body fv_map fv_bn_map bn_args args) bodies)
+  | BC (_, binders, bodies) => 
+      let
+        val t1 = map (make_body fv_map args) bodies
+        val (t2, t3) = split_list (map (make_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, ty, 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 = 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) = 
+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
+end
+
+fun define_raw_fvs dt_descr sorts bn_funs bn_funs2 bclausesss lthy =
+let
+
+  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;
+  val fv_tys = map (fn ty => ty --> @{typ "atom set"}) fv_arg_tys;
+  val fv_frees = map Free (fv_names ~~ fv_tys);
+  val fv_map = fv_arg_tys ~~ fv_frees
+
+  val (bns, bn_tys) = split_list (map (fn (bn, i, _) => (bn, i)) bn_funs)
+  val (bns2, bn_tys2) = split_list (map (fn (bn, i, _) => (bn, i)) bn_funs2)
+  val bn_args2 = map (fn (_, _, arg) => arg) bn_funs2
+  val fv_bn_names2 = map (fn bn => "fv_" ^ (fst (dest_Free bn))) bns2
+  val fv_bn_arg_tys2 = map (fn i => nth_dtyp dt_descr sorts i) bn_tys2
+  val fv_bn_tys2 = map (fn ty => ty --> @{typ "atom set"}) fv_bn_arg_tys2
+  val fv_bn_frees2 = map Free (fv_bn_names2 ~~ fv_bn_tys2)
+  val fv_bn_map2 = bns ~~ fv_bn_frees2
+  val fv_bn_map3 = bns2 ~~ fv_bn_frees2
+ 
+  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 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)
+
+  fun pat_completeness_auto lthy =
+    Pat_Completeness.pat_completeness_tac lthy 1
+      THEN auto_tac (clasimpset_of lthy)
+
+  fun prove_termination lthy =
+    Function.prove_termination NONE
+      (Lexicographic_Order.lexicographic_order_tac true lthy) lthy
+
+  val (_, lthy') = Function.add_function all_fv_names all_fv_eqs
+    Function_Common.default_config pat_completeness_auto lthy
+
+  val (info, lthy'') = prove_termination (Local_Theory.restore lthy')
+
+  val {fs, simps, ...} = info;
+
+  val morphism = ProofContext.export_morphism lthy'' lthy
+  val fs_exp = map (Morphism.term morphism) fs
+
+  val (fv_frees_exp, fv_bns_exp) = chop (length fv_frees) fs_exp
+  val simps_exp = Morphism.fact morphism (the simps)
+in
+  (fv_frees_exp, fv_bns_exp, simps_exp, lthy'')
+end
+
+end (* structure *)
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/nominal_dt_rawperm.ML	Thu May 20 21:23:53 2010 +0100
@@ -0,0 +1,150 @@
+(*  Title:      nominal_dt_rawperm.ML
+    Author:     Cezary Kaliszyk
+    Author:     Christian Urban
+
+  Definitions of the raw permutations and
+  proof that the raw datatypes are in the
+  pt-class.
+*)
+
+signature NOMINAL_DT_RAWPERM =
+sig
+  val define_raw_perms: Datatype.descr -> (string * sort) list -> thm -> int -> theory -> 
+    (term list * thm list * thm list) * theory
+end
+
+
+structure Nominal_Dt_RawPerm: NOMINAL_DT_RAWPERM =
+struct
+
+
+(* permutation function for one argument 
+   
+    - in case the argument is recursive it returns 
+
+         permute_fn p arg
+
+    - in case the argument is non-recursive it will return
+
+         p o arg
+
+*)
+fun perm_arg permute_fn_frees p (arg_dty, arg) =
+  if Datatype_Aux.is_rec_type arg_dty 
+  then (nth permute_fn_frees (Datatype_Aux.body_index arg_dty)) $ p $ arg
+  else mk_perm p arg
+
+
+(* generates the equation for the permutation function for one constructor;
+   i is the index of the corresponding datatype *)
+fun perm_eq_constr dt_descr sorts permute_fn_frees i (cnstr_name, dts) =
+let
+  val p = Free ("p", @{typ perm})
+  val arg_tys = map (Datatype_Aux.typ_of_dtyp dt_descr sorts) dts
+  val arg_names = Name.variant_list ["p"] (Datatype_Prop.make_tnames arg_tys)
+  val args = map Free (arg_names ~~ arg_tys)
+  val cnstr = Const (cnstr_name, arg_tys ---> (nth_dtyp dt_descr sorts i))
+  val lhs = (nth permute_fn_frees i) $ p $ list_comb (cnstr, args)
+  val rhs = list_comb (cnstr, map (perm_arg permute_fn_frees p) (dts ~~ args))
+  val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
+in
+  (Attrib.empty_binding, eq)
+end
+
+
+(** proves the two pt-type class properties **)
+
+fun prove_permute_zero lthy induct perm_defs perm_fns =
+let
+  val perm_types = map (body_type o fastype_of) perm_fns
+  val perm_indnames = Datatype_Prop.make_tnames perm_types
+  
+  fun single_goal ((perm_fn, T), x) =
+    HOLogic.mk_eq (perm_fn $ @{term "0::perm"} $ Free (x, T), Free (x, T))
+
+  val goals =
+    HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
+      (map single_goal (perm_fns ~~ perm_types ~~ perm_indnames)))
+
+  val simps = HOL_basic_ss addsimps (@{thm permute_zero} :: perm_defs)
+
+  val tac = (Datatype_Aux.indtac induct perm_indnames 
+             THEN_ALL_NEW asm_simp_tac simps) 1
+in
+  Goal.prove lthy perm_indnames [] goals (K tac)
+  |> Datatype_Aux.split_conj_thm
+end
+
+
+fun prove_permute_plus lthy induct perm_defs perm_fns =
+let
+  val p = Free ("p", @{typ perm})
+  val q = Free ("q", @{typ perm})
+  val perm_types = map (body_type o fastype_of) perm_fns
+  val perm_indnames = Datatype_Prop.make_tnames perm_types
+  
+  fun single_goal ((perm_fn, T), x) = HOLogic.mk_eq 
+      (perm_fn $ (mk_plus p q) $ Free (x, T), perm_fn $ p $ (perm_fn $ q $ Free (x, T)))
+
+  val goals =
+    HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
+      (map single_goal (perm_fns ~~ perm_types ~~ perm_indnames)))
+
+  val simps = HOL_basic_ss addsimps (@{thm permute_plus} :: perm_defs)
+
+  val tac = (Datatype_Aux.indtac induct perm_indnames
+             THEN_ALL_NEW asm_simp_tac simps) 1
+in
+  Goal.prove lthy ("p" :: "q" :: perm_indnames) [] goals (K tac)
+  |> Datatype_Aux.split_conj_thm 
+end
+
+
+(* user_dt_nos refers to the number of "un-unfolded" datatypes
+   given by the user
+*)
+fun define_raw_perms (dt_descr:Datatype.descr) sorts induct_thm user_dt_nos thy =
+let
+  val all_full_tnames = map (fn (_, (n, _, _)) => n) dt_descr;
+  val user_full_tnames = List.take (all_full_tnames, user_dt_nos);
+
+  val perm_fn_names = prefix_dt_names dt_descr sorts "permute_"
+  val perm_fn_types = map (fn (i, _) => perm_ty (nth_dtyp dt_descr sorts i)) dt_descr
+  val perm_fn_frees = map Free (perm_fn_names ~~ perm_fn_types)
+
+  fun perm_eq (i, (_, _, constrs)) = 
+    map (perm_eq_constr dt_descr sorts perm_fn_frees i) constrs;
+
+  val perm_eqs = maps perm_eq dt_descr;
+
+  val lthy =
+    Theory_Target.instantiation (user_full_tnames, [], @{sort pt}) thy;
+   
+  val ((perm_funs, perm_eq_thms), lthy') =
+    Primrec.add_primrec
+      (map (fn s => (Binding.name s, NONE, NoSyn)) perm_fn_names) perm_eqs lthy;
+    
+  val perm_zero_thms = prove_permute_zero lthy' induct_thm perm_eq_thms perm_funs
+  val perm_plus_thms = prove_permute_plus lthy' induct_thm perm_eq_thms perm_funs
+  val perm_zero_thms' = List.take (perm_zero_thms, user_dt_nos);
+  val perm_plus_thms' = List.take (perm_plus_thms, user_dt_nos)
+  val perms_name = space_implode "_" perm_fn_names
+  val perms_zero_bind = Binding.name (perms_name ^ "_zero")
+  val perms_plus_bind = Binding.name (perms_name ^ "_plus")
+  
+  fun tac _ (_, _, simps) =
+    Class.intro_classes_tac [] THEN ALLGOALS (resolve_tac simps)
+  
+  fun morphism phi (fvs, dfs, simps) =
+    (map (Morphism.term phi) fvs, map (Morphism.thm phi) dfs, map (Morphism.thm phi) simps);
+in
+  lthy'
+  |> snd o (Local_Theory.note ((perms_zero_bind, []), perm_zero_thms'))
+  |> snd o (Local_Theory.note ((perms_plus_bind, []), perm_plus_thms'))
+  |> Class_Target.prove_instantiation_exit_result morphism tac 
+       (perm_funs, perm_eq_thms, perm_zero_thms' @ perm_plus_thms')
+end
+
+
+end (* structure *)
+