--- a/Nominal/Rsp.thy	Fri Mar 26 10:55:13 2010 +0100
+++ b/Nominal/Rsp.thy	Fri Mar 26 16:20:39 2010 +0100
@@ -3,17 +3,6 @@
 begin
 
 ML {*
-fun define_quotient_type args tac ctxt =
-let
-  val mthd = Method.SIMPLE_METHOD tac
-  val mthdt = Method.Basic (fn _ => mthd)
-  val bymt = Proof.global_terminal_proof (mthdt, NONE)
-in
-  bymt (Quotient_Type.quotient_type args ctxt)
-end
-*}
-
-ML {*
 fun const_rsp lthy const =
 let
   val nty = fastype_of (Quotient_Term.quotient_lift_const ("", const) lthy)
@@ -50,10 +39,6 @@
 *}
 
 ML {*
-fun repeat_mp thm = repeat_mp (mp OF [thm]) handle THM _ => thm
-*}
-
-ML {*
 fun prove_const_rsp bind consts tac ctxt =
 let
   val rsp_goals = map (const_rsp ctxt) consts
@@ -120,16 +105,9 @@
 
 
 ML {*
-fun mk_minimal_ss ctxt =
-  Simplifier.context ctxt empty_ss
-    setsubgoaler asm_simp_tac
-    setmksimps (mksimps [])
-*}
-
-ML {*
 fun alpha_eqvt_tac induct simps ctxt =
   rel_indtac induct THEN_ALL_NEW
-  simp_tac ((mk_minimal_ss ctxt) addsimps simps) THEN_ALL_NEW
+  simp_tac (HOL_basic_ss addsimps simps) THEN_ALL_NEW
   REPEAT o etac @{thm exi[of _ _ "p"]} THEN' split_conj_tac THEN_ALL_NEW
   asm_full_simp_tac (HOL_ss addsimps (all_eqvts ctxt @ simps)) THEN_ALL_NEW
   asm_full_simp_tac (HOL_ss addsimps 
@@ -153,8 +131,6 @@
 end
 *}
 
-ML {* fold_map build_alpha_eqvt *}
-
 ML {*
 fun build_alpha_eqvts funs tac ctxt =
 let
@@ -256,4 +232,44 @@
 end
 *}
 
+ML {*
+fun build_alpha_alpha_bn_gl alphas alpha_bn ctxt =
+let
+  val ty = domain_type (fastype_of alpha_bn);
+  val (l, r) = the (AList.lookup (op=) alphas ty);
+in
+  ([alpha_bn $ l $ r], ctxt)
 end
+*}
+
+ML {*
+fun prove_alpha_alphabn alphas ind simps alpha_bns ctxt =
+  prove_by_rel_induct alphas build_alpha_alpha_bn_gl ind
+    (fn _ => asm_full_simp_tac (HOL_ss addsimps simps)) alpha_bns ctxt
+*}
+
+ML {*
+fun build_rsp_gl alphas fnctn ctxt =
+let
+  val typ = domain_type (fastype_of fnctn);
+  val (argl, argr) = the (AList.lookup (op=) alphas typ);
+in
+  ([HOLogic.mk_eq (fnctn $ argl, fnctn $ argr)], ctxt)
+end
+*}
+
+ML {*
+fun fvbv_rsp_tac' simps ctxt =
+  asm_full_simp_tac (HOL_basic_ss addsimps @{thms alpha_gen2}) THEN_ALL_NEW
+  asm_full_simp_tac (HOL_ss addsimps (@{thm alpha_gen} :: simps)) THEN_ALL_NEW
+  REPEAT o eresolve_tac [conjE, exE] THEN_ALL_NEW
+  asm_full_simp_tac (HOL_ss addsimps simps) THEN_ALL_NEW
+  TRY o blast_tac (claset_of ctxt)
+*}
+
+ML {*
+fun build_fvbv_rsps alphas ind simps fnctns ctxt =
+  prove_by_rel_induct alphas build_rsp_gl ind (fvbv_rsp_tac' simps) fnctns ctxt
+*}
+
+end