--- a/Quot/Nominal/Terms.thy	Tue Feb 23 12:49:45 2010 +0100
+++ b/Quot/Nominal/Terms.thy	Tue Feb 23 14:19:44 2010 +0100
@@ -32,7 +32,7 @@
 setup {* snd o define_raw_perms ["rtrm1", "bp"] ["Terms.rtrm1", "Terms.bp"] *}
 thm permute_rtrm1_permute_bp.simps
 
-local_setup {* 
+local_setup {*
   snd o define_fv_alpha "Terms.rtrm1"
   [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[(SOME @{term bv1}, 0)], [], [(SOME @{term bv1}, 0)]]],
   [[], [[]], [[], []]]] *}
@@ -145,8 +145,21 @@
 *}
 print_theorems
 
-prove fv_rtrm1_rsp': {*
- (@{term Trueprop} $ (Quotient_Term.equiv_relation_chk @{context} (fastype_of @{term fv_rtrm1}, fastype_of @{term fv_trm1}) $ @{term fv_rtrm1} $ @{term fv_rtrm1})) *}
+
+ML {*
+fun const_rsp const lthy =
+let
+  val nty = fastype_of (Quotient_Term.quotient_lift_const ("", const) lthy)
+  val rel = Quotient_Term.equiv_relation_chk lthy (fastype_of const, nty);
+in
+  HOLogic.mk_Trueprop (rel $ const $ const)
+end
+*}
+
+(*local_setup {*
+snd o Local_Theory.note ((Binding.empty, [Attrib.internal (fn _ => Quotient_Info.rsp_rules_add)]), @{thms refl}) *} *)
+ 
+prove fv_rtrm1_rsp': {* const_rsp @{term fv_rtrm1} @{context} *}
 by (tactic {*
   (rtac @{thm fun_rel_id} THEN'
   eresolve_tac @{thms alpha_rtrm1_alpha_bp.inducts} THEN_ALL_NEW
@@ -175,6 +188,33 @@
 end
 *}
 
+ML {*
+fun remove_alls trm =
+let
+  val fs = rev (map Free (strip_all_vars trm))
+in
+  subst_bounds (fs, (strip_all_body trm))
+end
+*}
+
+ML {*
+fun rsp_goal thy trm =
+let
+  val goalstate = Goal.init (cterm_of thy trm);
+  val tac = REPEAT o rtac @{thm fun_rel_id};
+in
+  case (SINGLE (tac 1) goalstate) of
+    NONE => error "rsp_goal failed"
+  | SOME th => remove_alls (term_of (cprem_of th 1))
+end
+*}
+
+prove rAp1_rsp': {* rsp_goal @{theory} (const_rsp @{term rAp1} @{context}) *}
+by (tactic {* contr_rsp_tac @{thms alpha1_inj} @{thms fv_rtrm1_rsp} @{thms alpha1_equivp} 1 *})
+
+thm apply_rsp'[OF apply_rsp'[OF rAp1_rsp']]
+
+
 lemma [quot_respect]:
  "(op = ===> alpha_rtrm1) rVr1 rVr1"
  "(alpha_rtrm1 ===> alpha_rtrm1 ===> alpha_rtrm1) rAp1 rAp1"