--- a/Nominal/nominal_dt_rawfuns.ML	Wed Nov 10 13:46:21 2010 +0000
+++ b/Nominal/nominal_dt_rawfuns.ML	Fri Nov 12 01:20:53 2010 +0000
@@ -11,7 +11,7 @@
   type dt_info = string list * binding * mixfix * ((binding * typ list * mixfix) list) list
 
   (* info of raw binding functions *)
-  type bn_info = (term * int * (int * term option) list list) list
+  type bn_info = term * int * (int * term option) list list
 
   
   (* binding modes and binding clauses *)
@@ -28,13 +28,17 @@
   val setify: Proof.context -> term -> term
   val listify: Proof.context -> term -> term
 
-  (* TODO: should be here
+  (* FIXME: should be here - currently in Nominal2.thy
   val define_raw_bns: string list -> dt_info -> (binding * typ option * mixfix) list ->
     (Attrib.binding * term) list -> thm list -> thm list -> local_theory ->
-    (term list * thm list * bn_info * thm list * local_theory) *)
+    (term list * thm list * bn_info list * thm list * local_theory) 
+  *)
 
-  val define_raw_fvs: string list -> typ list -> cns_info list -> bn_info -> bclause list list list -> 
+  val define_raw_fvs: string list -> typ list -> cns_info list -> bn_info list -> bclause list list list -> 
     thm list -> thm list -> Proof.context -> term list * term list * thm list * thm list * local_theory
+
+  val define_raw_bn_perms: typ list -> bn_info list -> cns_info list -> thm list -> thm list -> 
+    local_theory -> (term list * thm list * local_theory)
  
   val raw_prove_eqvt: term list -> thm list -> thm list -> Proof.context -> thm list
 end
@@ -56,7 +60,7 @@
    int * term option - is number of the corresponding argument with possibly
                        recursive call with bn-function term 
 *)  
-type bn_info = (term * int * (int * term option) list list) list
+type bn_info = term * int * (int * term option) list list
 
 
 datatype bmode = Lst | Res | Set
@@ -148,7 +152,6 @@
   else t
 
 
-
 (** functions that construct the equations for fv and fv_bn **)
 
 fun mk_fv_rhs lthy fv_map fv_bn_map args (BC (bmode, binders, bodies)) =
@@ -284,6 +287,68 @@
   end
 
 
+(** definition of raw permute_bn functions **)
+
+fun mk_perm_bn_eq_rhs p perm_bn_map bn_args (i, arg) = 
+  case AList.lookup (op=) bn_args i of
+    NONE => arg
+  | SOME (NONE) => mk_perm p arg
+  | SOME (SOME bn) => (lookup perm_bn_map bn) $ p $ arg   
+
+
+fun mk_perm_bn_eq lthy bn_trm perm_bn_map bn_args (constr, _, arg_tys, _) =
+  let
+    val p = Free ("p", @{typ perm})
+    val arg_names = Datatype_Prop.make_tnames arg_tys
+    val args = map Free (arg_names ~~ arg_tys)
+    val perm_bn = lookup perm_bn_map bn_trm
+    val lhs = perm_bn $ p $ list_comb (constr, args)
+    val rhs = list_comb (constr, map_index (mk_perm_bn_eq_rhs p perm_bn_map bn_args) args)
+  in
+    HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
+  end
+
+fun mk_perm_bn_eqs lthy perm_bn_map cns_info (bn_trm, bn_n, bn_argss) = 
+  let
+    val nth_cns_info = nth cns_info bn_n
+  in
+    map2 (mk_perm_bn_eq lthy bn_trm perm_bn_map) bn_argss nth_cns_info
+  end
+
+fun define_raw_bn_perms raw_tys bn_info cns_info cns_thms size_thms lthy =
+  if null bn_info
+  then ([], [], lthy)
+  else
+    let
+      val (bns, bn_tys) = split_list (map (fn (bn, i, _) => (bn, i)) bn_info)
+      val bn_names = map (fn bn => Long_Name.base_name (fst (dest_Const bn))) bns
+      val perm_bn_names = map (prefix "permute_") bn_names
+      val perm_bn_arg_tys = map (nth raw_tys) bn_tys
+      val perm_bn_tys = map (fn ty => @{typ "perm"} --> ty --> ty) perm_bn_arg_tys
+      val perm_bn_frees = map Free (perm_bn_names ~~ perm_bn_tys)
+      val perm_bn_map = bns ~~ perm_bn_frees
+
+      val perm_bn_eqs = map (mk_perm_bn_eqs lthy perm_bn_map cns_info) bn_info
+
+      val all_fun_names = map (fn s => (Binding.name s, NONE, NoSyn)) perm_bn_names
+      val all_fun_eqs = map (pair Attrib.empty_binding) (flat perm_bn_eqs)
+
+      val prod_simps = @{thms prod.inject HOL.simp_thms}
+
+      val (_, lthy') = Function.add_function all_fun_names all_fun_eqs
+        Function_Common.default_config (pat_completeness_simp (prod_simps @ cns_thms)) lthy
+    
+      val (info, lthy'') = prove_termination size_thms (Local_Theory.restore lthy')
+
+      val {fs, simps, ...} = info;
+
+      val morphism = ProofContext.export_morphism lthy'' lthy
+      val simps_exp = map (Morphism.thm morphism) (the simps)
+    in
+      (fs, simps_exp, lthy'')
+    end
+
+
 (** equivarance proofs **)
 
 val eqvt_apply_sym = @{thm eqvt_apply[symmetric]}