--- a/Nominal/Perm.thy	Tue May 04 16:17:46 2010 +0200
+++ b/Nominal/Perm.thy	Tue May 04 16:18:07 2010 +0200
@@ -32,29 +32,29 @@
 
          permute_fn p arg
 
-    - in case the argument is non-recursive it will build
+    - in case the argument is non-recursive it will return
 
          p o arg
 
 *)
-fun perm_arg permute_fns pi (arg_dty, arg) =
+fun perm_arg permute_fn_frees p (arg_dty, arg) =
   if Datatype_Aux.is_rec_type arg_dty 
-  then Free (nth permute_fns (Datatype_Aux.body_index arg_dty)) $ pi $ arg
-  else mk_perm pi arg
+  then (nth permute_fn_frees (Datatype_Aux.body_index arg_dty)) $ p $ arg
+  else mk_perm p arg
 *}
 
 ML {*
-(* equation for permutation function for one constructor;
-   i is the index of the correspodning datatype *)
-fun perm_eq_constr dt_descr sorts permute_fns i (cnstr_name, dts) =
+(* 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 pi = Free ("p", @{typ perm})
+  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 = Free (nth permute_fns i) $ pi $ list_comb (cnstr, args)
-  val rhs = list_comb (cnstr, map (perm_arg permute_fns pi) (dts ~~ args))
+  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)
@@ -87,13 +87,13 @@
 ML {*
 fun prove_permute_plus lthy induct perm_defs perm_fns =
 let
-  val pi1 = Free ("p", @{typ perm})
-  val pi2 = Free ("q", @{typ perm})
+  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, T), x) = HOLogic.mk_eq 
-      (perm $ (mk_plus pi1 pi2) $ Free (x, T), perm $ pi1 $ (perm $ pi2 $ Free (x, T)))
+  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
@@ -113,37 +113,34 @@
 (* defines the permutation functions for raw datatypes and
    proves that they are instances of pt
 
-   dt_nos refers to the number of "un-unfolded" datatypes
+   user_dt_nos refers to the number of "un-unfolded" datatypes
    given by the user
 *)
-fun define_raw_perms (dt_info : Datatype_Aux.info) dt_nos thy =
+fun define_raw_perms dt_descr sorts induct_thm user_dt_nos thy =
 let
-  val {descr as dt_descr, induct, sorts, ...} = dt_info;
   val all_full_tnames = map (fn (_, (n, _, _)) => n) dt_descr;
-  val full_tnames = List.take (all_full_tnames, dt_nos);
+  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_types = map (fn (i, _) => perm_ty (nth_dtyp dt_descr sorts i)) dt_descr
-
-  val permute_fns = perm_fn_names ~~ perm_types
+  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 permute_fns 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 (full_tnames, [], @{sort pt}) thy;
+    Theory_Target.instantiation (user_full_tnames, [], @{sort pt}) thy;
    
-  val ((perm_fns, perm_ldef), lthy') =
+  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 perm_ldef perm_fns
-  val perm_plus_thms = prove_permute_plus lthy' induct perm_ldef perm_fns
-  val perm_zero_thms' = List.take (perm_zero_thms, dt_nos);
-  val perm_plus_thms' = List.take (perm_plus_thms, dt_nos)
+  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")
@@ -158,10 +155,14 @@
   |> 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_ldef, perm_zero_thms' @ perm_plus_thms', perm_fns)
+       (perm_eq_thms, perm_zero_thms' @ perm_plus_thms', perm_funs)
 end
 *}
 
+
+
+
+
 (* permutations for quotient types *)
 
 ML {*