--- a/Nominal-General/Nominal2_Base.thy	Wed Nov 10 13:46:21 2010 +0000
+++ b/Nominal-General/Nominal2_Base.thy	Fri Nov 12 01:20:53 2010 +0000
@@ -142,6 +142,7 @@
   "Rep_perm p1 = Rep_perm p2 \<Longrightarrow> p1 = p2"
   by (simp add: fun_eq_iff Rep_perm_inject [symmetric])
 
+instance perm :: size ..
 
 subsection {* Permutations form a group *}
 

--- a/Nominal-General/nominal_library.ML	Wed Nov 10 13:46:21 2010 +0000
+++ b/Nominal-General/nominal_library.ML	Fri Nov 12 01:20:53 2010 +0000
@@ -258,22 +258,37 @@
 
 fun prove_termination_tac size_simps ctxt =
   let
-    fun mk_size_measure (Type (@{type_name Sum_Type.sum}, [fT, sT])) =
-        SumTree.mk_sumcase fT sT @{typ nat} (mk_size_measure fT) (mk_size_measure sT)
-      | mk_size_measure T = size_const T
+    val natT = @{typ nat}
+    fun prod_size_const fT sT = 
+      let
+        val fT_fun = fT --> natT
+        val sT_fun = sT --> natT
+        val prodT = Type (@{type_name prod}, [fT, sT])
+      in
+        Const (@{const_name prod_size}, [fT_fun, sT_fun, prodT] ---> natT)
+      end
+
+    fun mk_size_measure T =
+      case T of    
+        (Type (@{type_name Sum_Type.sum}, [fT, sT])) =>
+           SumTree.mk_sumcase fT sT natT (mk_size_measure fT) (mk_size_measure sT)
+      | (Type (@{type_name Product_Type.prod}, [fT, sT])) =>
+           prod_size_const fT sT $ (mk_size_measure fT) $ (mk_size_measure sT)
+      | _ => size_const T
 
     fun mk_measure_trm T = 
       HOLogic.dest_setT T
       |> fst o HOLogic.dest_prodT
       |> mk_size_measure 
-      |> curry (op $) (Const (@{const_name measure}, dummyT))
+      |> curry (op $) (Const (@{const_name "measure"}, dummyT))
       |> Syntax.check_term ctxt
-
+      
     val ss = HOL_ss addsimps @{thms in_measure wf_measure sum.cases add_Suc_right add.right_neutral 
-      zero_less_Suc} @ size_simps addsimprocs Nat_Numeral_Simprocs.cancel_numerals
+      zero_less_Suc prod.size(1) mult_Suc_right} @ size_simps 
+    val ss' = ss addsimprocs Nat_Numeral_Simprocs.cancel_numerals
   in
     Function_Relation.relation_tac ctxt mk_measure_trm
-    THEN_ALL_NEW simp_tac ss
+    THEN_ALL_NEW simp_tac ss'
   end
 
 fun prove_termination size_simps ctxt = 

--- a/Nominal/Ex/Foo1.thy	Wed Nov 10 13:46:21 2010 +0000
+++ b/Nominal/Ex/Foo1.thy	Fri Nov 12 01:20:53 2010 +0000
@@ -42,21 +42,6 @@
 thm foo.supp
 thm foo.fresh
 
-primrec
-  permute_bn1_raw
-where
-  "permute_bn1_raw p (As_raw x y t) = As_raw (p \<bullet> x) y t"
-
-primrec
-  permute_bn2_raw
-where
-  "permute_bn2_raw p (As_raw x y t) = As_raw x (p \<bullet> y) t"
-
-primrec
-  permute_bn3_raw
-where
-  "permute_bn3_raw p (As_raw x y t) = As_raw (p \<bullet> x) (p \<bullet> y) t"
-
 quotient_definition
   "permute_bn1 :: perm \<Rightarrow> assg \<Rightarrow> assg"
 is

--- a/Nominal/Ex/Let.thy	Wed Nov 10 13:46:21 2010 +0000
+++ b/Nominal/Ex/Let.thy	Fri Nov 12 01:20:53 2010 +0000
@@ -18,6 +18,8 @@
   "bn ANil = []"
 | "bn (ACons x t as) = (atom x) # (bn as)"
 
+thm permute_bn_raw.simps
+
 thm at_set_avoiding2
 thm trm_assn.fv_defs
 thm trm_assn.eq_iff 
@@ -30,12 +32,6 @@
 thm trm_assn.fresh
 thm trm_assn.exhaust[where y="t", no_vars]
 
-primrec
-  permute_bn_raw
-where
-  "permute_bn_raw p (ANil_raw) = ANil_raw"
-| "permute_bn_raw p (ACons_raw a t l) = ACons_raw (p \<bullet> a) t (permute_bn_raw p l)"
-
 quotient_definition
   "permute_bn :: perm \<Rightarrow> assn \<Rightarrow> assn"
 is

--- a/Nominal/Ex/SingleLet.thy	Wed Nov 10 13:46:21 2010 +0000
+++ b/Nominal/Ex/SingleLet.thy	Fri Nov 12 01:20:53 2010 +0000
@@ -36,11 +36,6 @@
 thm single_let.supp
 thm single_let.fresh
 
-primrec
-  permute_bn_raw
-where
-  "permute_bn_raw p (As_raw x y t) = As_raw (p \<bullet> x) y t"
-
 quotient_definition
   "permute_bn :: perm \<Rightarrow> assg \<Rightarrow> assg"
 is

--- a/Nominal/Nominal2.thy	Wed Nov 10 13:46:21 2010 +0000
+++ b/Nominal/Nominal2.thy	Fri Nov 12 01:20:53 2010 +0000
@@ -169,6 +169,7 @@
   in
     (dt_index, (bn_fun, (cnstr_head, rhs_elements)))
   end
+
   fun order dts i ts = 
   let
     val dt = nth dts i
@@ -190,7 +191,6 @@
   ordered'
 end
 
-
 fun define_raw_bns dt_names dts raw_bn_funs raw_bn_eqs constr_thms size_thms lthy =
   if null raw_bn_funs 
   then ([], [], [], [], lthy)
@@ -210,6 +210,7 @@
     in
       (fs, raw_bn_eqs, raw_bn_info, raw_bn_induct, lthy2)
     end
+
 *}
 
 ML {*
@@ -298,33 +299,40 @@
   (* definitions of raw permutations by primitive recursion *)
   val _ = warning "Definition of raw permutations";
   val ((raw_perm_funs, raw_perm_simps, raw_perm_laws), lthy2a) =
-    if get_STEPS lthy0 > 1 
+    if get_STEPS lthy0 > 0 
     then define_raw_perms raw_full_ty_names raw_tys tvs raw_constrs raw_induct_thm lthy0
     else raise TEST lthy0
  
   (* noting the raw permutations as eqvt theorems *)
   val (_, lthy3) = Local_Theory.note ((Binding.empty, [eqvt_attr]), raw_perm_simps) lthy2a
 
-  (* definition of raw fv_functions *)
-  val _ = warning "Definition of raw fv-functions";
+  (* definition of raw fv and bn functions *)
+  val _ = warning "Definition of raw fv- and bn-functions";
   val (raw_bns, raw_bn_defs, raw_bn_info, raw_bn_induct, lthy3a) =
-    if get_STEPS lthy3 > 2 
+    if get_STEPS lthy3 > 1
     then define_raw_bns raw_full_ty_names raw_dts raw_bn_funs raw_bn_eqs 
       (raw_inject_thms @ raw_distinct_thms) raw_size_thms lthy3
     else raise TEST lthy3
 
-  val (raw_fvs, raw_fv_bns, raw_fv_defs, raw_fv_bns_induct, lthy3b) = 
-    if get_STEPS lthy3a > 3 
-    then define_raw_fvs raw_full_ty_names raw_tys raw_cns_info raw_bn_info raw_bclauses 
+  (* defining the permute_bn functions *)
+  val (_, _, lthy3b) = 
+    if get_STEPS lthy3a > 2
+    then define_raw_bn_perms raw_tys raw_bn_info raw_cns_info 
       (raw_inject_thms @ raw_distinct_thms) raw_size_thms lthy3a
     else raise TEST lthy3a
 
+  val (raw_fvs, raw_fv_bns, raw_fv_defs, raw_fv_bns_induct, lthy3c) = 
+    if get_STEPS lthy3b > 3 
+    then define_raw_fvs raw_full_ty_names raw_tys raw_cns_info raw_bn_info raw_bclauses 
+      (raw_inject_thms @ raw_distinct_thms) raw_size_thms lthy3b
+    else raise TEST lthy3b
+
   (* definition of raw alphas *)
   val _ = warning "Definition of alphas";
   val (alpha_trms, alpha_bn_trms, alpha_intros, alpha_cases, alpha_induct, lthy4) =
-    if get_STEPS lthy3b > 4 
-    then define_raw_alpha raw_full_ty_names raw_tys raw_cns_info raw_bn_info raw_bclauses raw_fvs lthy3b
-    else raise TEST lthy3b
+    if get_STEPS lthy3c > 4 
+    then define_raw_alpha raw_full_ty_names raw_tys raw_cns_info raw_bn_info raw_bclauses raw_fvs lthy3c
+    else raise TEST lthy3c
   val alpha_tys = map (domain_type o fastype_of) alpha_trms  
 
   (* definition of alpha-distinct lemmas *)

--- a/Nominal/nominal_dt_alpha.ML	Wed Nov 10 13:46:21 2010 +0000
+++ b/Nominal/nominal_dt_alpha.ML	Fri Nov 12 01:20:53 2010 +0000
@@ -7,8 +7,9 @@
 
 signature NOMINAL_DT_ALPHA =
 sig
-  val define_raw_alpha: string list -> typ list -> cns_info list -> bn_info -> bclause list list list -> 
-    term list -> Proof.context -> term list * term list * thm list * thm list * thm * local_theory
+  val define_raw_alpha: string list -> typ list -> cns_info list -> bn_info list -> 
+    bclause list list list -> term list -> Proof.context -> 
+    term list * term list * thm list * thm list * thm * local_theory
 
   val mk_alpha_distincts: Proof.context -> thm list -> thm list -> 
     term list -> typ list -> thm list

--- 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]}