--- a/Nominal/nominal_dt_alpha.ML	Mon Aug 16 19:57:41 2010 +0800
+++ b/Nominal/nominal_dt_alpha.ML	Tue Aug 17 06:39:27 2010 +0800
@@ -23,12 +23,14 @@
   val raw_prove_refl: term list -> term list -> thm list -> thm -> Proof.context -> thm list
   val raw_prove_sym: term list -> thm list -> thm -> Proof.context -> thm list
   val raw_prove_trans: term list -> thm list -> thm list -> thm -> thm list -> Proof.context -> thm list
-  val raw_prove_equivp: term list -> thm list -> thm list -> thm list -> Proof.context -> thm list
+  val raw_prove_equivp: term list -> term list -> thm list -> thm list -> thm list -> 
+    Proof.context -> thm list * thm list
   val raw_prove_bn_imp: term list -> term list -> thm list -> thm -> Proof.context -> thm list
   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 raw_alpha_bn_rsp: thm list -> thm list -> thm list
 
   val mk_funs_rsp: thm -> thm
   val mk_alpha_permute_rsp: thm -> thm 
@@ -563,7 +565,7 @@
   @{lemma "transp R == !x y. R x y --> (!z. R y z --> R x z)" 
     by (rule eq_reflection, auto simp add: transp_def)}
 
-fun raw_prove_equivp alphas refl symm trans ctxt = 
+fun raw_prove_equivp alphas alpha_bns refl symm trans ctxt = 
 let
   val refl' = map (fold_rule @{thms reflp_def} o atomize) refl
   val symm' = map (fold_rule @{thms symp_def} o atomize) symm
@@ -572,9 +574,10 @@
   fun prep_goal t = 
     HOLogic.mk_Trueprop (Const (@{const_name "equivp"}, fastype_of t --> @{typ bool}) $ t) 
 in    
-  Goal.prove_multi ctxt [] [] (map prep_goal alphas)
+  Goal.prove_multi ctxt [] [] (map prep_goal (alphas @ alpha_bns))
   (K (HEADGOAL (Goal.conjunction_tac THEN_ALL_NEW (rtac @{thm equivpI} THEN' 
      RANGE [resolve_tac refl', resolve_tac symm', resolve_tac trans']))))
+  |> chop (length alphas)
 end
 
 
@@ -691,6 +694,21 @@
 end
 
 
+(* rsp lemmas for alpha_bn relations *)
+
+val rsp_equivp =
+  @{lemma "[|equivp Q; !!x y. R x y ==> Q x y|] ==> (R ===> R ===> op =) Q Q"
+    by (simp only: fun_rel_def equivp_def, metis)}
+
+fun raw_alpha_bn_rsp alpha_bn_equivp alpha_bn_imps =
+let
+  fun mk_thm thm1 thm2 = 
+    (forall_intr_vars thm2) COMP (thm1 RS rsp_equivp)
+in
+  map2 mk_thm alpha_bn_equivp alpha_bn_imps
+end
+
+
 (* transformation of the natural rsp-lemmas into standard form *)
 
 val fun_rsp = @{lemma
@@ -715,5 +733,6 @@
 
 
 
+
 end (* structure *)