--- a/Nominal/Ex/Classical.thy	Wed May 12 16:33:25 2010 +0100
+++ b/Nominal/Ex/Classical.thy	Wed May 12 16:33:50 2010 +0100
@@ -12,9 +12,7 @@
 atom_decl name
 atom_decl coname
 
-ML {* val _ = cheat_alpha_eqvt := true *}
 ML {* val _ = cheat_equivp := true *}
-ML {* val _ = cheat_fv_rsp := true *}
 
 nominal_datatype trm =
    Ax "name" "coname"

--- a/Nominal/Ex/ExPS3.thy	Wed May 12 16:33:25 2010 +0100
+++ b/Nominal/Ex/ExPS3.thy	Wed May 12 16:33:50 2010 +0100
@@ -6,7 +6,6 @@
 
 atom_decl name
 
-ML {* val _ = cheat_alpha_eqvt := true *}
 ML {* val _ = cheat_equivp := true *}
 ML {* val _ = cheat_alpha_bn_rsp := true *}
 

--- a/Nominal/Ex/ExPS8.thy	Wed May 12 16:33:25 2010 +0100
+++ b/Nominal/Ex/ExPS8.thy	Wed May 12 16:33:50 2010 +0100
@@ -7,6 +7,7 @@
 atom_decl name
 
 ML {* val _ = cheat_fv_rsp := true *}
+ML {* val _ = cheat_equivp := true *}
 ML {* val _ = cheat_alpha_bn_rsp := true *}
 
 nominal_datatype exp =

--- a/Nominal/NewParser.thy	Wed May 12 16:33:25 2010 +0100
+++ b/Nominal/NewParser.thy	Wed May 12 16:33:50 2010 +0100
@@ -278,7 +278,6 @@
 end
 *}
 
-ML {* val cheat_alpha_eqvt = Unsynchronized.ref false *}
 ML {* val cheat_equivp = Unsynchronized.ref false *}
 ML {* val cheat_fv_rsp = Unsynchronized.ref false *}
 ML {* val cheat_alpha_bn_rsp = Unsynchronized.ref false *}
@@ -436,23 +435,20 @@
   val _ = warning "Proving equivariance";
   val (bv_eqvt, lthy5) = prove_eqvt raw_tys induct_thm (raw_bn_eqs @ raw_perm_def) (map fst bns) lthy4
   val (fv_eqvt, lthy6) = prove_eqvt raw_tys induct_thm (fv_def @ raw_perm_def) (fv @ fvbn) lthy5
-  fun alpha_eqvt_tac' _ =
-    if !cheat_alpha_eqvt then Skip_Proof.cheat_tac thy
-    else alpha_eqvt_tac alpha_induct (raw_perm_def @ alpha_eq_iff_simp) lthy6 1
-  val alpha_eqvt = build_alpha_eqvts alpha_ts alpha_eqvt_tac' lthy6;
+  val (alpha_eqvt, lthy6a) = Nominal_Eqvt.equivariance alpha_ts alpha_induct alpha_intros lthy6;
 
   (* proving alpha equivalence *)
   val _ = warning "Proving equivalence";
   val fv_alpha_all = combine_fv_alpha_bns (fv, fvbn) (alpha_ts_nobn, alpha_ts_bn) bn_nos;
-  val reflps = build_alpha_refl fv_alpha_all alpha_ts induct_thm alpha_eq_iff_simp lthy6;
+  val reflps = build_alpha_refl fv_alpha_all alpha_ts induct_thm alpha_eq_iff_simp lthy6a;
   val alpha_equivp =
-    if !cheat_equivp then map (equivp_hack lthy6) alpha_ts
+    if !cheat_equivp then map (equivp_hack lthy6a) alpha_ts
     else build_equivps alpha_ts reflps alpha_induct
-      inject_thms alpha_eq_iff_simp distinct_thms alpha_cases alpha_eqvt lthy6;
+      inject_thms alpha_eq_iff_simp distinct_thms alpha_cases alpha_eqvt lthy6a;
   val qty_binds = map (fn (_, b, _, _) => b) dts;
   val qty_names = map Name.of_binding qty_binds;
   val qty_full_names = map (Long_Name.qualify thy_name) qty_names
-  val (qtys, lthy7) = define_quotient_types qty_binds all_typs alpha_ts_nobn alpha_equivp lthy6;
+  val (qtys, lthy7) = define_quotient_types qty_binds all_typs alpha_ts_nobn alpha_equivp lthy6a;
   val const_names = map Name.of_binding (flat (map (fn (_, _, _, t) => map (fn (b, _, _) => b) t) dts));
   val raw_consts =
     flat (map (fn (i, (_, _, l)) =>

--- a/Nominal/Rsp.thy	Wed May 12 16:33:25 2010 +0100
+++ b/Nominal/Rsp.thy	Wed May 12 16:33:50 2010 +0100
@@ -62,8 +62,7 @@
 fun fvbv_rsp_tac induct fvbv_simps ctxt =
   rtac induct THEN_ALL_NEW
   (TRY o rtac @{thm TrueI}) THEN_ALL_NEW
-  asm_full_simp_tac (HOL_basic_ss addsimps @{thms alphas2}) THEN_ALL_NEW
-  asm_full_simp_tac (HOL_ss addsimps (@{thms alphas prod_rel.simps prod_fv.simps} @ fvbv_simps)) THEN_ALL_NEW
+  asm_full_simp_tac (HOL_ss addsimps (@{thms prod_fv.simps prod_rel.simps set.simps append.simps alphas} @ fvbv_simps)) THEN_ALL_NEW
   REPEAT o eresolve_tac [conjE, exE] THEN_ALL_NEW
   asm_full_simp_tac (HOL_ss addsimps fvbv_simps) THEN_ALL_NEW
   TRY o blast_tac (claset_of ctxt)
@@ -87,51 +86,6 @@
   ))
 *}
 
-
-lemma exi: "\<exists>(pi :: perm). P pi \<Longrightarrow> (\<And>(p :: perm). P p \<Longrightarrow> Q (pi \<bullet> p)) \<Longrightarrow> \<exists>pi. Q pi"
-apply (erule exE)
-apply (rule_tac x="pi \<bullet> pia" in exI)
-by auto
-
-
-ML {*
-fun alpha_eqvt_tac induct simps ctxt =
-  rtac induct THEN_ALL_NEW
-  simp_tac (HOL_basic_ss addsimps simps) THEN_ALL_NEW split_conj_tac 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 
-    @{thms supp_eqvt[symmetric] inter_eqvt[symmetric] empty_eqvt alphas prod_rel.simps prod_fv.simps}) THEN_ALL_NEW
-  (split_conj_tac THEN_ALL_NEW TRY o resolve_tac
-    @{thms fresh_star_permute_iff[of "- p", THEN iffD1] permute_eq_iff[of "- p", THEN iffD1]})
-  THEN_ALL_NEW
-  asm_full_simp_tac (HOL_ss addsimps (@{thms split_conv permute_minus_cancel permute_plus permute_eqvt[symmetric]} @ all_eqvts ctxt @ simps))
-*}
-
-ML {*
-fun build_alpha_eqvt alpha names =
-let
-  val pi = Free ("p", @{typ perm});
-  val (tys, _) = strip_type (fastype_of alpha)
-  val indnames = Name.variant_list names (Datatype_Prop.make_tnames (map body_type tys));
-  val args = map Free (indnames ~~ tys);
-  val perm_args = map (fn x => mk_perm pi x) args
-in
-  (HOLogic.mk_imp (list_comb (alpha, args), list_comb (alpha, perm_args)), indnames @ names)
-end
-*}
-
-ML {*
-fun build_alpha_eqvts funs tac ctxt =
-let
-  val (gls, names) = fold_map build_alpha_eqvt funs ["p"]
-  val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj gls)
-  val thm = Goal.prove ctxt names [] gl tac
-in
-  map (fn x => mp OF [x]) (HOLogic.conj_elims thm)
-end
-*}
-
 ML {*
 fun prove_fv_rsp fv_alphas_lst all_alphas tac ctxt =
 let

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Unused.thy	Wed May 12 16:33:50 2010 +0100
@@ -0,0 +1,43 @@
+lemma exi: "\<exists>(pi :: perm). P pi \<Longrightarrow> (\<And>(p :: perm). P p \<Longrightarrow> Q (pi \<bullet> p)) \<Longrightarrow> \<exists>pi. Q pi"
+apply (erule exE)
+apply (rule_tac x="pi \<bullet> pia" in exI)
+by auto
+
+ML {*
+fun alpha_eqvt_tac induct simps ctxt =
+  rtac induct THEN_ALL_NEW
+  simp_tac (HOL_basic_ss addsimps simps) THEN_ALL_NEW split_conj_tac 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
+    @{thms supp_eqvt[symmetric] inter_eqvt[symmetric] empty_eqvt alphas prod_rel.simps prod_fv.simps}) THEN_ALL_NEW
+  (split_conj_tac THEN_ALL_NEW TRY o resolve_tac
+    @{thms fresh_star_permute_iff[of "- p", THEN iffD1] permute_eq_iff[of "- p", THEN iffD1]})
+  THEN_ALL_NEW
+  asm_full_simp_tac (HOL_ss addsimps (@{thms split_conv permute_minus_cancel permute_plus permute_eqvt[symmetric]} @ all_eqvts ctxt @ simps))
+*}
+
+ML {*
+fun build_alpha_eqvt alpha names =
+let
+  val pi = Free ("p", @{typ perm});
+  val (tys, _) = strip_type (fastype_of alpha)
+  val indnames = Name.variant_list names (Datatype_Prop.make_tnames (map body_type tys));
+  val args = map Free (indnames ~~ tys);
+  val perm_args = map (fn x => mk_perm pi x) args
+in
+  (HOLogic.mk_imp (list_comb (alpha, args), list_comb (alpha, perm_args)), indnames @ names)
+end
+*}
+
+ML {*
+fun build_alpha_eqvts funs tac ctxt =
+let
+  val (gls, names) = fold_map build_alpha_eqvt funs ["p"]
+  val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj gls)
+  val thm = Goal.prove ctxt names [] gl tac
+in
+  map (fn x => mp OF [x]) (HOLogic.conj_elims thm)
+end
+*}
+