--- a/Nominal-General/nominal_library.ML	Sat Aug 14 16:54:41 2010 +0800
+++ b/Nominal-General/nominal_library.ML	Sat Aug 14 23:33:23 2010 +0800
@@ -58,6 +58,7 @@
 
   (* transformation into the object logic *)
   val atomize: thm -> thm
+
 end
 
 
@@ -262,7 +263,6 @@
 (* transformes a theorem into one of the object logic *)
 val atomize = Conv.fconv_rule Object_Logic.atomize o forall_intr_vars
 
-
 end (* structure *)
 
 open Nominal_Library;
\ No newline at end of file

--- a/Nominal/Ex/CoreHaskell.thy	Sat Aug 14 16:54:41 2010 +0800
+++ b/Nominal/Ex/CoreHaskell.thy	Sat Aug 14 23:33:23 2010 +0800
@@ -8,7 +8,7 @@
 atom_decl cvar
 atom_decl tvar
 
-declare [[STEPS = 17]]
+declare [[STEPS = 18]]
 
 nominal_datatype tkind =
   KStar

--- a/Nominal/Ex/SingleLet.thy	Sat Aug 14 16:54:41 2010 +0800
+++ b/Nominal/Ex/SingleLet.thy	Sat Aug 14 23:33:23 2010 +0800
@@ -4,7 +4,7 @@
 
 atom_decl name
 
-declare [[STEPS = 17]]
+declare [[STEPS = 18]]
 
 nominal_datatype trm  =
   Var "name"
@@ -25,37 +25,13 @@
 thm distinct
 thm trm_raw_assg_raw.inducts
 thm fv_defs
-
-
-(* cannot lift yet *)
-thm eq_iff
-thm eq_iff_simps
 thm perm_simps
 thm perm_laws
 thm trm_raw_assg_raw.size(9 - 16)
 
-(* rsp lemmas *)
-thm size_rsp
-thm funs_rsp
-thm constrs_rsp
-thm permute_rsp
-
-declare constrs_rsp[quot_respect]
-declare funs_rsp[quot_respect] 
-declare size_rsp[quot_respect]
-declare permute_rsp[quot_respect]
-
-ML {*
-  val thms_d = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms distinct}
-*}
-
-ML {* 
-  val thms_i = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms trm_raw_assg_raw.inducts}
-*}
-
-ML {*
-  val thms_f = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms fv_defs}
-*}
+(* cannot lift yet *)
+thm eq_iff
+thm eq_iff_simps
 
 instantiation trm and assg :: size 
 begin
@@ -72,12 +48,6 @@
 
 end 
 
-ML {* 
-  val thms_i = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms trm_raw_assg_raw.size(9 - 16)}
-*}
-
-
-
 instantiation trm and assg :: pt
 begin
 
@@ -101,13 +71,36 @@
 
 end
 
+ML {*
+  val thms_d = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms distinct}
+*}
 
-(*
-lemma [quot_respect]:
-  "(alpha_assg_raw ===> alpha_assg_raw ===> op =) alpha_bn_raw alpha_bn_raw"
-apply(simp)
-sorry
-*)
+ML {* 
+  val thms_i = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms trm_raw_assg_raw.inducts}
+*}
+
+ML {*
+  val thms_f = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms fv_defs}
+*}
+
+ML {* 
+  val thms_i = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms trm_raw_assg_raw.size(9 - 16)}
+*}
+
+ML {*
+  val thms_p = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms perm_simps}
+*}
+
+ML {*
+  val thms_f = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms perm_laws}
+*}
+
+
+
+
+
+section {* NOT *} 
+
 
 ML {*
   val thms_e = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms eq_iff[unfolded alphas prod_fv.simps prod_rel.simps prod_alpha_def]}
@@ -134,21 +127,6 @@
 
 section {* NOT *}
 
-
-ML {* 
-  val thms_i = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms trm_raw_assg_raw.size(9 - 16)}
-*}
-
-
-ML {*
-  val thms_p = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms perm_simps(1)}
-*}
-
-ML {*
-  val thms_f = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms perm_laws}
-*}
-
-
 ML {*
   val thms_p = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms perm_simps(1)}
 *}

--- a/Nominal/NewParser.thy	Sat Aug 14 16:54:41 2010 +0800
+++ b/Nominal/NewParser.thy	Sat Aug 14 23:33:23 2010 +0800
@@ -13,6 +13,13 @@
 
 section{* Interface for nominal_datatype *}
 
+ML {*
+(* attributes *)
+val eqvt_attrib = Attrib.internal (K Nominal_ThmDecls.eqvt_add)
+val rsp_attrib = Attrib.internal (K Quotient_Info.rsp_rules_add)
+
+*}
+
 
 ML {* 
 (* nominal datatype parser *)
@@ -305,11 +312,11 @@
 
   val dtinfo = Datatype.the_info (ProofContext.theory_of lthy0) (hd raw_dt_names)
   val {descr, sorts, ...} = dtinfo
-  val all_raw_tys = all_dtyps descr sorts
-  val all_raw_ty_names = map (fn (_, (n, _, _)) => n) descr
   val all_raw_constrs = 
     flat (map (map (fn (c, _, _, _) => c)) (all_dtyp_constrs_types descr sorts))
-
+  val all_raw_tys = all_dtyps descr sorts
+  val all_raw_ty_names = map (fst o dest_Type) all_raw_tys
+  
   val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy0)) all_raw_ty_names  
   val inject_thms = flat (map #inject dtinfos);
   val distinct_thms = flat (map #distinct dtinfos);
@@ -329,20 +336,16 @@
   val _ = warning "Definition of raw permutations";
   val ((raw_perm_funs, raw_perm_simps, raw_perm_laws), lthy2) =
     if get_STEPS lthy0 > 1 
-    then Local_Theory.theory_result (define_raw_perms descr sorts raw_induct_thm (length dts)) lthy0
+    then Local_Theory.theory_result 
+      (define_raw_perms all_raw_ty_names all_raw_tys all_raw_constrs raw_induct_thm) lthy0
     else raise TEST lthy0
+  val lthy2a = Named_Target.reinit lthy2 lthy2
  
   (* noting the raw permutations as eqvt theorems *)
-  val eqvt_attrib = Attrib.internal (K Nominal_ThmDecls.eqvt_add)
-  val (_, lthy2a) = Local_Theory.note ((Binding.empty, [eqvt_attrib]), raw_perm_simps) lthy2
-
-  val thy = Local_Theory.exit_global lthy2a;
-  val thy_name = Context.theory_name thy
+  val (_, lthy3) = Local_Theory.note ((Binding.empty, [eqvt_attrib]), raw_perm_simps) lthy2a
 
   (* definition of raw fv_functions *)
   val _ = warning "Definition of raw fv-functions";
-  val lthy3 = Named_Target.init NONE thy;
-
   val (raw_bns, raw_bn_eqs, raw_bn_info, raw_bn_induct, lthy3a) =
     if get_STEPS lthy3 > 2 
     then raw_bn_decls all_raw_ty_names raw_dts raw_bn_funs raw_bn_eqs constr_thms lthy3
@@ -382,8 +385,7 @@
     else raise TEST lthy4
 
   (* noting the bn_eqvt lemmas in a temprorary theory *)
-  val add_eqvt = Attrib.internal (K Nominal_ThmDecls.eqvt_add)
-  val lthy_tmp = snd (Local_Theory.note ((Binding.empty, [add_eqvt]), bn_eqvt) lthy4)
+  val lthy_tmp = snd (Local_Theory.note ((Binding.empty, [eqvt_attrib]), bn_eqvt) lthy4)
 
   val fv_eqvt = 
     if get_STEPS lthy > 7
@@ -399,7 +401,7 @@
       |> map (fn thm => thm RS @{thm sym})
     else raise TEST lthy4
  
-  val lthy5 = snd (Local_Theory.note ((Binding.empty, [add_eqvt]), fv_eqvt) lthy_tmp)
+  val lthy5 = snd (Local_Theory.note ((Binding.empty, [eqvt_attrib]), fv_eqvt) lthy_tmp)
 
   val (alpha_eqvt, lthy6) =
     if get_STEPS lthy > 9
@@ -452,17 +454,23 @@
 
   val alpha_permute_rsp = map mk_alpha_permute_rsp alpha_eqvt
 
+  (* noting the quot_respects lemmas *)
+  val (_, lthy6a) = 
+    if get_STEPS lthy > 15
+    then Local_Theory.note ((Binding.empty, [rsp_attrib]),
+      raw_constrs_rsp @ raw_funs_rsp @ raw_size_rsp @ alpha_permute_rsp) lthy6
+    else raise TEST lthy6
+
   (* defining the quotient type *)
   val _ = warning "Declaring the quotient types"
   val qty_descr = map (fn (vs, bind, mx, _) => (vs, bind, mx)) dts
   val qty_binds = map (fn (_, bind, _, _) => bind) dts        
   val qty_names = map Name.of_binding qty_binds;              
-  val qty_full_names = map (Long_Name.qualify thy_name) qty_names (* not used *)
   
   val (qty_infos, lthy7) = 
-    if get_STEPS lthy > 15
-    then qtype_defs qty_descr alpha_tys alpha_trms alpha_equivp_thms lthy6
-    else raise TEST lthy6
+    if get_STEPS lthy > 16
+    then qtype_defs qty_descr alpha_tys alpha_trms alpha_equivp_thms lthy6a
+    else raise TEST lthy6a
 
   val qtys = map #qtyp qty_infos
   
@@ -479,13 +487,16 @@
     map2 (fn n => fn t => ("fv_" ^ n, t, NoSyn)) qty_names raw_fvs
 
   val qfv_bns_descr = 
-    map2 (fn (b, _, _) => fn t => ("fv_" ^ Name.of_binding b, t, NoSyn)) bn_funs  raw_fv_bns
+    map2 (fn (b, _, _) => fn t => ("fv_" ^ Name.of_binding b, t, NoSyn)) bn_funs raw_fv_bns
 
   val qalpha_bns_descr = 
     map2 (fn (b, _, _) => fn t => ("alpha_" ^ Name.of_binding b, t, NoSyn)) bn_funs  alpha_bn_trms
 
+  val qperm_descr =
+    map2 (fn n => fn t => ("permute_" ^ n, t, NoSyn)) qty_names raw_perm_funs
+
   val (((((qconstrs_info, qbns_info), qfvs_info), qfv_bns_info), qalpha_bns_info), lthy8) = 
-    if get_STEPS lthy > 16
+    if get_STEPS lthy > 17
     then 
       lthy7
       |> qconst_defs qtys qconstrs_descr 
@@ -495,12 +506,17 @@
       ||>> qconst_defs qtys qalpha_bns_descr
     else raise TEST lthy7
 
+  (*val _ = Local_Theory.theory_result 
+    (qperm_defs qtys qty_full_names qperm_descr raw_perm_laws) lthy8*) 
+
+
   val qconstrs = map #qconst qconstrs_info
   val qbns = map #qconst qbns_info
   val qfvs = map #qconst qfvs_info
   val qfv_bns = map #qconst qfv_bns_info
   val qalpha_bns = map #qconst qalpha_bns_info
 
+  
   (* temporary theorem bindings *)
 
   val (_, lthy8') = lthy8
@@ -511,17 +527,17 @@
      ||>> Local_Theory.note ((@{binding "perm_simps"}, []), raw_perm_simps) 
      ||>> Local_Theory.note ((@{binding "perm_laws"}, []), raw_perm_laws) 
      ||>> Local_Theory.note ((@{binding "alpha_bn_imps"}, []), alpha_bn_imp_thms)
-     ||>> Local_Theory.note ((@{binding "funs_rsp"}, []), raw_funs_rsp)
-     ||>> Local_Theory.note ((@{binding "size_rsp"}, []), raw_size_rsp)
-     ||>> Local_Theory.note ((@{binding "constrs_rsp"}, []), raw_constrs_rsp)
-     ||>> Local_Theory.note ((@{binding "permute_rsp"}, []), alpha_permute_rsp)
 
   val _ = 
-    if get_STEPS lthy > 17
+    if get_STEPS lthy > 18
     then true else raise TEST lthy8'
   
   (* old stuff *)
 
+  val thy = ProofContext.theory_of lthy8'
+  val thy_name = Context.theory_name thy  
+  val qty_full_names = map (Long_Name.qualify thy_name) qty_names 
+
   val _ = warning "Proving respects";
 
   val bn_nos = map (fn (_, i, _) => i) raw_bn_info;
@@ -578,7 +594,7 @@
   val dd = map2 (fn x => fn y => (x, y, NoSyn)) perm_names raw_perm_funs
   (* use Local_Theory.theory_result *)
   val thy' = qperm_defs qtys qty_full_names dd raw_perm_laws thy;
-  val lthy13 = Named_Target.init NONE thy';
+  val lthy13 = Named_Target.init "" thy';
   
   val q_name = space_implode "_" qty_names;
   fun suffix_bind s = Binding.qualify true q_name (Binding.name s);

--- a/Nominal/nominal_dt_quot.ML	Sat Aug 14 16:54:41 2010 +0800
+++ b/Nominal/nominal_dt_quot.ML	Sat Aug 14 23:33:23 2010 +0800
@@ -42,18 +42,21 @@
 
 
 (* defines the quotient permutations *)
-fun qperm_defs qtys full_tnames name_term_pairs thms thy =
+fun qperm_defs qtys full_tnames perm_specs thms thy =
 let
   val lthy =
     Class.instantiation (full_tnames, [], @{sort pt}) thy;
-  val (_, lthy') = qconst_defs qtys name_term_pairs lthy;
+  
+  val (_, lthy') = qconst_defs qtys perm_specs lthy;
+
   val lifted_thms = map (Quotient_Tacs.lifted qtys lthy') thms;
+
   fun tac _ =
     Class.intro_classes_tac [] THEN
-    (ALLGOALS (resolve_tac lifted_thms))
-  val lthy'' = Class.prove_instantiation_instance tac lthy'
+      (ALLGOALS (resolve_tac lifted_thms))
 in
-  Local_Theory.exit_global lthy''
+  lthy'
+  |> Class.prove_instantiation_exit tac 
 end
 
 

--- a/Nominal/nominal_dt_rawperm.ML	Sat Aug 14 16:54:41 2010 +0800
+++ b/Nominal/nominal_dt_rawperm.ML	Sat Aug 14 23:33:23 2010 +0800
@@ -9,7 +9,7 @@
 
 signature NOMINAL_DT_RAWPERM =
 sig
-  val define_raw_perms: Datatype.descr -> (string * sort) list -> thm -> int -> theory -> 
+  val define_raw_perms: string list -> typ list -> term list -> thm -> theory -> 
     (term list * thm list * thm list) * theory
 end
 
@@ -18,39 +18,6 @@
 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 =
@@ -99,49 +66,62 @@
 end
 
 
-(* 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 =
+fun mk_perm_eq ty_perm_assoc cnstr = 
 let
-  val all_full_tnames = map (fn (_, (n, _, _)) => n) dt_descr;
-  val user_full_tnames = List.take (all_full_tnames, user_dt_nos);
+  fun lookup_perm p (ty, arg) = 
+    case (AList.lookup (op=) ty_perm_assoc ty) of
+      SOME perm => perm $ p $ arg
+    | NONE => Const (@{const_name permute}, perm_ty ty) $ p $ arg
+
+  val p = Free ("p", @{typ perm})
+  val (arg_tys, ty) =
+    fastype_of cnstr
+    |> strip_type
+
+  val arg_names = Name.variant_list ["p"] (Datatype_Prop.make_tnames arg_tys)
+  val args = map Free (arg_names ~~ arg_tys)
 
-  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)
+  val lhs = lookup_perm p (ty, list_comb (cnstr, args))
+  val rhs = list_comb (cnstr, map (lookup_perm p) (arg_tys ~~ args))
+  
+  val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))  
+in
+  (Attrib.empty_binding, eq)
+end
+
 
-  fun perm_eq (i, (_, _, constrs)) = 
-    map (perm_eq_constr dt_descr sorts perm_fn_frees i) constrs;
+fun define_raw_perms full_ty_names tys constrs induct_thm thy =
+let
+  val perm_fn_names = full_ty_names
+    |> map Long_Name.base_name
+    |> map (prefix "permute_")
 
-  val perm_eqs = maps perm_eq dt_descr;
+  val perm_fn_types = map perm_ty tys
+  val perm_fn_frees = map Free (perm_fn_names ~~ perm_fn_types)
+  val perm_fn_binds = map (fn s => (Binding.name s, NONE, NoSyn)) perm_fn_names
+
+  val perm_eqs = map (mk_perm_eq (tys ~~ perm_fn_frees)) constrs
 
   val lthy =
-    Class.instantiation (user_full_tnames, [], @{sort pt}) thy;
+    Class.instantiation (full_ty_names, [], @{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;
+    Primrec.add_primrec perm_fn_binds 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);
+    (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.prove_instantiation_exit_result morphism tac 
-       (perm_funs, perm_eq_thms, perm_zero_thms' @ perm_plus_thms')
+       (perm_funs, perm_eq_thms, perm_zero_thms @ perm_plus_thms)
 end