--- a/Nominal/LFex.thy	Mon Mar 22 18:19:13 2010 +0100
+++ b/Nominal/LFex.thy	Mon Mar 22 18:20:06 2010 +0100
@@ -5,8 +5,6 @@
 atom_decl name
 atom_decl ident
 
-ML {* val _ = cheat_fv_rsp := false *}
-ML {* val _ = cheat_alpha_bn_rsp := false *}
 ML {* val _ = cheat_equivp := false *}
 
 nominal_datatype kind =

--- a/Nominal/Parser.thy	Mon Mar 22 18:19:13 2010 +0100
+++ b/Nominal/Parser.thy	Mon Mar 22 18:20:06 2010 +0100
@@ -265,13 +265,13 @@
 end
 *}
 
-ML {* val cheat_alpha_bn_rsp = Unsynchronized.ref true *}
 ML {* val cheat_equivp = Unsynchronized.ref true *}
 
-(* These 3 are not needed any more *)
+(* These 4 are not needed any more *)
 ML {* val cheat_fv_rsp = Unsynchronized.ref false *}
 ML {* val cheat_fv_eqvt = Unsynchronized.ref false *}
 ML {* val cheat_alpha_eqvt = Unsynchronized.ref false *}
+ML {* val cheat_alpha_bn_rsp = Unsynchronized.ref false *}
 
 
 ML {*
@@ -300,6 +300,7 @@
   val rel_distinct = map #distinct rel_dtinfos;
   val induct = #induct dtinfo;
   val inducts = #inducts dtinfo;
+  val exhausts = map #exhaust dtinfos;
   val _ = tracing "Defining permutations, fv and alpha";
   val ((raw_perm_def, raw_perm_simps, perms), lthy3) =
     Local_Theory.theory_result (define_raw_perms dtinfo (length dts)) lthy2;
@@ -308,11 +309,15 @@
     define_fv_alpha_export dtinfo raw_binds_flat bn_funs_decls lthy3;
   val (fv_ts_nobn, fv_ts_bn) = chop (length perms) fv_ts;
   val (alpha_ts_nobn, alpha_ts_bn) = chop (length perms) alpha_ts
-  val alpha_inducts = Project_Rule.projects lthy4 (1 upto (length dts)) alpha_induct
+  val alpha_inducts = Project_Rule.projects lthy4 (1 upto (length dts)) alpha_induct;
   val dts_names = map (fn (i, (s, _, _)) => (s, i)) (#descr dtinfo);
   val bn_tys = map (domain_type o fastype_of) raw_bn_funs;
   val bn_nos = map (dtyp_no_of_typ dts_names) bn_tys;
   val bns = raw_bn_funs ~~ bn_nos;
+  val rel_dists = flat (map (distinct_rel lthy4 alpha_cases)
+    (rel_distinct ~~ alpha_ts_nobn));
+  val rel_dists_bn = flat (map (distinct_rel lthy4 alpha_cases)
+    ((map (fn i => nth rel_distinct i) bn_nos) ~~ alpha_ts_bn))
   val alpha_eq_iff = build_alpha_inj alpha_intros (inject @ distincts) alpha_cases lthy4
   val _ = tracing "Proving equivariance";
   val (bv_eqvts, lthy5) = fold_map (build_bv_eqvt (raw_bn_eqs @ raw_perm_def) inducts) bns lthy4;
@@ -368,11 +373,11 @@
     (fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy10;
   val alpha_alphabn = build_alpha_alphabn fv_alpha_all alpha_inducts alpha_eq_iff lthy11;
   fun const_rsp_tac _ = constr_rsp_tac alpha_eq_iff (fv_rsp @ bns_rsp @ reflps @ alpha_alphabn) 1
-  fun alpha_bn_rsp_tac x = if !cheat_alpha_bn_rsp then Skip_Proof.cheat_tac thy else const_rsp_tac x
   val (const_rsps, lthy11a) = fold_map (fn cnst => prove_const_rsp Binding.empty [cnst]
     const_rsp_tac) raw_consts lthy11
+  val alpha_bn_rsp_pre = flat (map (prove_alpha_bn_rsp alpha_ts_nobn alpha_inducts exhausts (alpha_eq_iff @ rel_dists @ rel_dists_bn) (alpha_equivp) lthy11a) (alpha_ts_bn ~~ bn_nos))
   val (alpha_bn_rsps, lthy12) = fold_map (fn cnst => prove_const_rsp Binding.empty [cnst]
-    alpha_bn_rsp_tac) alpha_ts_bn lthy11a
+    (fn _ => asm_simp_tac (HOL_ss addsimps alpha_bn_rsp_pre) 1)) alpha_ts_bn lthy11a
   val qfv_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) ordered_fv_ts
   val (qfv_ts, qfv_defs, lthy12a) = quotient_lift_consts_export (qfv_names ~~ ordered_fv_ts) lthy12;
   val (qfv_ts_nobn, qfv_ts_bn) = chop (length perms) qfv_ts;
@@ -411,8 +416,6 @@
   val q_eq_iff_pre2 = map (Local_Defs.fold lthy17 @{thms alpha_gen2}) q_eq_iff_pre1
   val q_eq_iff = map (Local_Defs.fold lthy17 @{thms alpha_gen}) q_eq_iff_pre2
   val (_, lthy18) = Local_Theory.note ((suffix_bind "eq_iff", []), q_eq_iff) lthy17;
-  val rel_dists = flat (map (distinct_rel lthy18 alpha_cases)
-    (rel_distinct ~~ (List.take (alpha_ts, (length dts)))))
   val q_dis = map (lift_thm lthy18) rel_dists;
   val lthy19 = note_simp_suffix "distinct" q_dis lthy18;
   val q_eqvt = map (lift_thm lthy19) raw_fv_bv_eqvt;

--- a/Nominal/Rsp.thy	Mon Mar 22 18:19:13 2010 +0100
+++ b/Nominal/Rsp.thy	Mon Mar 22 18:20:06 2010 +0100
@@ -270,34 +270,37 @@
   by blast
 
 ML {*
-fun prove_alpha_bn_rsp alphas inducts inj_dis equivps ctxt (alpha_bn, n) =
+fun prove_alpha_bn_rsp alphas inducts exhausts 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 ([x, y, a], ctxt') = Variable.variant_fixes ["x","y","a"] ctxt;
+  val [l, r] = map (fn x => (Free (x, ty))) [x, y]
+  val lhs = HOLogic.mk_Trueprop (alpha $ l $ r)
   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))))
+    Logic.mk_implies (lhs,
+      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))))
+    Logic.mk_implies (lhs,
+      HOLogic.mk_Trueprop (HOLogic.mk_all (a, ty,
+        HOLogic.mk_eq (alpha_bn $ Bound 0 $ l, alpha_bn $ Bound 0 $ r))));
+  val resl = map (fn x => @{thm equivp_rspl} OF [x]) equivps;
+  val resr = map (fn x => @{thm equivp_rspr} OF [x]) equivps;
   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
+    split_conjs THEN_ALL_NEW
+    InductTacs.case_rule_tac context a (nth exhausts n) 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
+    TRY o REPEAT_ALL_NEW (rtac @{thm arg_cong2[of _ _ _ _ "op \<and>"]}) THEN_ALL_NEW
+    TRY o eresolve_tac (resl @ resr) THEN_ALL_NEW
+    asm_full_simp_tac (HOL_ss addsimps inj_dis)
   ) 1;
-  val t1 = Goal.prove ctxt names [] g1 tac;
-  val t2 = Goal.prove ctxt names [] g2 tac;
+  val t1 = Goal.prove ctxt [] [] g1 tac;
+  val t2 = Goal.prove ctxt [] [] g2 tac;
 in
-  [t1, t2]
+  Variable.export ctxt' ctxt [t1, t2]
 end
 *}
 

--- a/Nominal/Term5.thy	Mon Mar 22 18:19:13 2010 +0100
+++ b/Nominal/Term5.thy	Mon Mar 22 18:20:06 2010 +0100
@@ -183,7 +183,7 @@
 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
 
-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)) *}
+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 rtrm5.exhaust rlts.exhaust} @{thms alpha5_inj alpha_dis} @{thms alpha5_equivp} @{context} (@{term alpha_rbv5}, 1)) *}
 thm alpha_bn_rsp
 
 lemma [quot_respect]:
@@ -203,6 +203,7 @@
   apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv)
 done
 
+
 lemma
   shows "(alpha_rlts ===> op =) rbv5 rbv5"
   by (simp add: bv_list_rsp)

--- a/Nominal/TySch.thy	Mon Mar 22 18:19:13 2010 +0100
+++ b/Nominal/TySch.thy	Mon Mar 22 18:20:06 2010 +0100
@@ -4,8 +4,6 @@
 
 atom_decl name
 
-ML {* val _ = cheat_fv_rsp := false *}
-ML {* val _ = cheat_alpha_bn_rsp := false *}
 ML {* val _ = cheat_equivp := false *}
 
 nominal_datatype t =

--- a/TODO	Mon Mar 22 18:19:13 2010 +0100
+++ b/TODO	Mon Mar 22 18:20:06 2010 +0100
@@ -27,7 +27,7 @@
 - check support equations for more bindings per constructor
 
 - automate the proofs that are currently proved with sorry:
-  alpha_equivp, alpha_bn_rsp
+  alpha_equivp
 
 - store information about defined nominal datatypes, so that
   it can be used to define new types that depend on these