--- a/Nominal/Ex/CoreHaskell.thy	Mon Aug 16 19:57:41 2010 +0800
+++ b/Nominal/Ex/CoreHaskell.thy	Tue Aug 17 06:39:27 2010 +0800
@@ -88,6 +88,7 @@
 (* can lift *)
 thm distinct
 thm fv_defs
+thm alpha_bn_imps alpha_equivp
 
 thm tkind_raw_ckind_raw_ty_raw_ty_lst_raw_co_raw_co_lst_raw_trm_raw_assoc_lst_raw_pat_raw_vars_raw_tvars_raw_cvars_raw.inducts
 thm perm_simps
@@ -128,7 +129,11 @@
   val thms_f = map (lift_thm qtys @{context}) @{thms perm_laws}
 *}
 
-
+ML {*
+ val thms_e = map (lift_thm qtys @{context}) 
+   @{thms eq_iff[unfolded alphas permute_prod.simps prod_fv.simps prod_alpha_def prod_rel.simps
+    prod.cases]}
+*}
 
 
 lemmas fv_supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.supp(1-9,11,13,15)

--- a/Nominal/Ex/SingleLet.thy	Mon Aug 16 19:57:41 2010 +0800
+++ b/Nominal/Ex/SingleLet.thy	Tue Aug 17 06:39:27 2010 +0800
@@ -62,11 +62,6 @@
 
 section {* NOT *} 
 
-lemma [quot_respect]:
-  "(alpha_assg_raw ===> alpha_assg_raw ===> op =) alpha_bn_raw alpha_bn_raw"
-sorry
-
-
 ML {*
  val thms_e = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) 
    @{thms eq_iff[unfolded alphas permute_prod.simps prod_fv.simps prod_alpha_def prod_rel.simps

--- a/Nominal/NewParser.thy	Mon Aug 16 19:57:41 2010 +0800
+++ b/Nominal/NewParser.thy	Tue Aug 17 06:39:27 2010 +0800
@@ -423,9 +423,10 @@
            alpha_intros alpha_induct alpha_cases lthy6
     else raise TEST lthy6
 
-  val alpha_equivp_thms = 
+  val (alpha_equivp_thms, alpha_bn_equivp_thms) = 
     if get_STEPS lthy > 13
-    then raw_prove_equivp alpha_trms alpha_refl_thms alpha_sym_thms alpha_trans_thms lthy6
+    then raw_prove_equivp alpha_trms alpha_bn_trms alpha_refl_thms alpha_sym_thms 
+       alpha_trans_thms lthy6
     else raise TEST lthy6
 
   (* proving alpha implies alpha_bn *)
@@ -450,11 +451,13 @@
 
   val alpha_permute_rsp = map mk_alpha_permute_rsp alpha_eqvt
 
+  val alpha_bn_rsp = raw_alpha_bn_rsp alpha_bn_equivp_thms alpha_bn_imp_thms
+
   (* 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
+      raw_constrs_rsp @ raw_funs_rsp @ raw_size_rsp @ alpha_permute_rsp @ alpha_bn_rsp) lthy6
     else raise TEST lthy6
 
   (* defining the quotient type *)
@@ -534,6 +537,7 @@
      ||>> 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 "alpha_equivp"}, []), alpha_equivp_thms)
 
   val _ = 
     if get_STEPS lthy > 20

--- 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 *)