--- a/Nominal/nominal_dt_alpha.ML	Wed Aug 11 16:23:50 2010 +0800
+++ b/Nominal/nominal_dt_alpha.ML	Wed Aug 11 19:53:57 2010 +0800
@@ -28,6 +28,7 @@
   val raw_fv_bn_rsp_aux: term list -> term list -> term list -> term list -> 
     term list -> thm -> thm list -> Proof.context -> thm list
   val raw_size_rsp_aux: term list -> thm -> thm list -> Proof.context -> thm list
+  val raw_constrs_rsp: term list -> term list -> thm list -> thm list -> Proof.context -> thm list
 
   val resolve_fun_rel: thm -> thm
 end
@@ -624,6 +625,7 @@
     (K (asm_full_simp_tac ss)) ctxt
 end
 
+
 (* respectfulness for size *)
 
 fun raw_size_rsp_aux all_alpha_trms alpha_induct simps ctxt =
@@ -644,6 +646,50 @@
 end
 
 
+(* respectfulness for constructors *)
+
+fun raw_constr_rsp_tac alpha_intros simps = 
+let
+  val pre_ss = HOL_ss addsimps @{thms fun_rel_def}
+  val post_ss = HOL_ss addsimps @{thms alphas prod_alpha_def prod_rel.simps 
+    prod_fv.simps fresh_star_zero permute_zero prod.cases} @ simps
+  (* funs_rsp alpha_bn_simps *)
+in
+  asm_full_simp_tac pre_ss
+  THEN' REPEAT o (resolve_tac @{thms allI impI})
+  THEN' resolve_tac alpha_intros
+  THEN_ALL_NEW (TRY o (rtac exi_zero) THEN' asm_full_simp_tac post_ss)
+end
+
+
+fun raw_constrs_rsp constrs alpha_trms alpha_intros simps ctxt =
+let
+  val alpha_arg_tys = map (domain_type o fastype_of) alpha_trms
+  
+  fun lookup ty = 
+    case AList.lookup (op=) (alpha_arg_tys ~~ alpha_trms) ty of
+      NONE => HOLogic.eq_const ty
+    | SOME alpha => alpha 
+  
+  fun fun_rel_app t1 t2 = 
+    Const (@{const_name "fun_rel"}, dummyT) $ t1 $ t2
+
+  fun prep_goal trm =
+    trm
+    |> strip_type o fastype_of
+    |>> map lookup
+    ||> lookup
+    |> uncurry (fold_rev fun_rel_app)
+    |> (fn t => t $ trm $ trm)
+    |> Syntax.check_term ctxt
+    |> HOLogic.mk_Trueprop
+in
+  Goal.prove_multi ctxt [] [] (map prep_goal constrs)
+    (K (HEADGOAL 
+      (Goal.conjunction_tac THEN_ALL_NEW raw_constr_rsp_tac alpha_intros simps)))
+end
+
+
 (* resolve with @{thm fun_relI} *)
 
 fun resolve_fun_rel thm =