--- a/Nominal/Rsp.thy	Mon Mar 22 14:07:35 2010 +0100
+++ b/Nominal/Rsp.thy	Mon Mar 22 15:27:01 2010 +0100
@@ -259,5 +259,47 @@
 end
 *}
 
+lemma equivp_rspl:
+  "equivp r \<Longrightarrow> r a b \<Longrightarrow> r a c = r b c"
+  unfolding equivp_reflp_symp_transp symp_def transp_def 
+  by blast
+
+lemma equivp_rspr:
+  "equivp r \<Longrightarrow> r a b \<Longrightarrow> r c a = r c b"
+  unfolding equivp_reflp_symp_transp symp_def transp_def 
+  by blast
+
+ML {*
+fun prove_alpha_bn_rsp alphas inducts inj_dis equivps ctxt (alpha_bn, n) =
+let
+  val alpha = nth alphas n;
+  val ty = domain_type (fastype_of alpha);
+  val names = Datatype_Prop.make_tnames [ty, ty];
+  val [l, r] = map (fn x => (Free (x, ty))) names;
+  val g1 =
+    Logic.mk_implies (HOLogic.mk_Trueprop (alpha $ l $ r),
+      HOLogic.mk_Trueprop (HOLogic.mk_all ("a", ty,
+        HOLogic.mk_eq (alpha_bn $ l $ Bound 0, alpha_bn $ r $ Bound 0))))
+  val g2 =
+    Logic.mk_implies (HOLogic.mk_Trueprop (alpha $ l $ r),
+      HOLogic.mk_Trueprop (HOLogic.mk_all ("a", ty,
+        HOLogic.mk_eq (alpha_bn $ Bound 0 $ l, alpha_bn $ Bound 0 $ r))))
+  fun tac {context, ...} = (
+    etac (nth inducts n) THEN_ALL_NEW
+    (TRY o rtac @{thm TrueI}) THEN_ALL_NEW rtac allI THEN_ALL_NEW
+    InductTacs.case_tac context "a" THEN_ALL_NEW split_conjs THEN_ALL_NEW
+    asm_full_simp_tac (HOL_ss addsimps inj_dis) THEN_ALL_NEW
+    REPEAT_ALL_NEW (rtac @{thm arg_cong2[of _ _ _ _ "op \<and>"]}) THEN_ALL_NEW
+    TRY o eresolve_tac (map (fn x => @{thm equivp_rspl} OF [x]) equivps) THEN_ALL_NEW
+    TRY o eresolve_tac (map (fn x => @{thm equivp_rspr} OF [x]) equivps) THEN_ALL_NEW
+    TRY o rtac refl
+  ) 1;
+  val t1 = Goal.prove ctxt names [] g1 tac;
+  val t2 = Goal.prove ctxt names [] g2 tac;
+in
+  [t1, t2]
+end
+*}
+
 
 end

--- a/Nominal/Term5.thy	Mon Mar 22 14:07:35 2010 +0100
+++ b/Nominal/Term5.thy	Mon Mar 22 15:27:01 2010 +0100
@@ -183,32 +183,8 @@
 local_setup {* snd o Local_Theory.note ((@{binding alpha_dis}, []), (flat (map (distinct_rel @{context} @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases}) [(@{thms rtrm5.distinct}, @{term alpha_rtrm5}), (@{thms rlts.distinct}, @{term alpha_rlts}), (@{thms rlts.distinct}, @{term alpha_rbv5})]))) *}
 print_theorems
 
-
-lemma alpha_rbv_rsp_pre:
-  "x \<approx>l y \<Longrightarrow> \<forall>z. alpha_rbv5 x z = alpha_rbv5 y z"
-  apply (erule alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts(2))
-  apply (simp_all add: alpha_dis alpha5_inj)
-  apply clarify
-  apply (case_tac [!] z)
-  apply (simp_all add: alpha_dis alpha5_inj)
-  apply clarify
-  apply auto
-  apply (meson alpha5_symp alpha5_transp)
-  apply (meson alpha5_symp alpha5_transp)
-  done
-
-lemma alpha_rbv_rsp_pre2:
-  "x \<approx>l y \<Longrightarrow> \<forall>z. alpha_rbv5 z x = alpha_rbv5 z y"
-  apply (erule alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts(2))
-  apply (simp_all add: alpha_dis alpha5_inj)
-  apply clarify
-  apply (case_tac [!] z)
-  apply (simp_all add: alpha_dis alpha5_inj)
-  apply clarify
-  apply auto
-  apply (meson alpha5_symp alpha5_transp)
-  apply (meson alpha5_symp alpha5_transp)
-  done
+local_setup {* snd o Local_Theory.note ((@{binding alpha_bn_rsp}, []), prove_alpha_bn_rsp [@{term alpha_rtrm5}, @{term alpha_rlts}] @{thms alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts} @{thms alpha5_inj alpha_dis} @{thms alpha5_equivp} @{context} (@{term alpha_rbv5}, 1)) *}
+thm alpha_bn_rsp
 
 lemma [quot_respect]:
   "(alpha_rlts ===> op =) fv_rlts fv_rlts"
@@ -221,13 +197,10 @@
   "(op = ===> alpha_rtrm5 ===> alpha_rtrm5) permute permute"
   "(op = ===> alpha_rlts ===> alpha_rlts) permute permute"
   "(alpha_rlts ===> alpha_rlts ===> op =) alpha_rbv5 alpha_rbv5"
-  apply (simp_all add: alpha5_inj alpha5_rfv alpha5_eqvt bv_list_rsp)
+  apply (simp_all add: alpha5_inj alpha5_rfv alpha5_eqvt bv_list_rsp alpha_bn_rsp)
   apply (clarify)
   apply (rule_tac x="0" in exI)
   apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv)
-  apply clarify
-  apply (simp add: alpha_rbv_rsp_pre2)
-  apply (simp add: alpha_rbv_rsp_pre)
 done
 
 lemma

--- a/Nominal/Term5n.thy	Mon Mar 22 14:07:35 2010 +0100
+++ b/Nominal/Term5n.thy	Mon Mar 22 15:27:01 2010 +0100
@@ -123,31 +123,9 @@
 local_setup {* snd o Local_Theory.note ((@{binding alpha_dis}, []), (flat (map (distinct_rel @{context} @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases}) [(@{thms rtrm5.distinct}, @{term alpha_rtrm5}), (@{thms rlts.distinct}, @{term alpha_rlts}), (@{thms rlts.distinct}, @{term alpha_rbv5})]))) *}
 print_theorems
 
-lemma alpha_rbv_rsp_pre:
-  "x \<approx>l y \<Longrightarrow> \<forall>z. alpha_rbv5 x z = alpha_rbv5 y z"
-  apply (erule alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts(2))
-  apply (simp_all add: alpha_dis alpha5_inj)
-  apply clarify
-  apply (case_tac [!] z)
-  apply (simp_all add: alpha_dis alpha5_inj)
-  apply clarify
-  apply auto
-  apply (meson alpha5_symp alpha5_transp)
-  apply (meson alpha5_symp alpha5_transp)
-  done
+local_setup {* snd o Local_Theory.note ((@{binding alpha_bn_rsp}, []), prove_alpha_bn_rsp [@{term alpha_rtrm5}, @{term alpha_rlts}] @{thms alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts} @{thms alpha5_inj alpha_dis} @{thms alpha5_equivp} @{context} (@{term alpha_rbv5}, 1)) *}
+thm alpha_bn_rsp
 
-lemma alpha_rbv_rsp_pre2:
-  "x \<approx>l y \<Longrightarrow> \<forall>z. alpha_rbv5 z x = alpha_rbv5 z y"
-  apply (erule alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts(2))
-  apply (simp_all add: alpha_dis alpha5_inj)
-  apply clarify
-  apply (case_tac [!] z)
-  apply (simp_all add: alpha_dis alpha5_inj)
-  apply clarify
-  apply auto
-  apply (meson alpha5_symp alpha5_transp)
-  apply (meson alpha5_symp alpha5_transp)
-  done
 
 lemma [quot_respect]:
   "(alpha_rlts ===> op =) fv_rlts fv_rlts"
@@ -161,7 +139,7 @@
   "(op = ===> alpha_rtrm5 ===> alpha_rtrm5) permute permute"
   "(op = ===> alpha_rlts ===> alpha_rlts) permute permute"
   "(alpha_rlts ===> alpha_rlts ===> op =) alpha_rbv5 alpha_rbv5"
-  apply (simp_all add: alpha5_inj alpha5_rfv alpha5_eqvt bv_list_rsp alpha_rbv_rsp_pre alpha_rbv_rsp_pre2 alpha5_reflp)
+  apply (simp_all add: alpha5_inj alpha5_rfv alpha5_eqvt bv_list_rsp alpha5_reflp alpha_bn_rsp)
   apply (clarify)
   apply (rule_tac x="0" in exI) apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv)
 done