--- a/Nominal/NewParser.thy	Mon May 03 09:57:05 2010 +0200
+++ b/Nominal/NewParser.thy	Mon May 03 10:15:23 2010 +0200
@@ -258,6 +258,23 @@
 end
 *}
 
+lemma equivp_hack: "equivp x"
+sorry
+ML {*
+fun equivp_hack ctxt rel =
+let
+  val thy = ProofContext.theory_of ctxt
+  val ty = domain_type (fastype_of rel)
+  val cty = ctyp_of thy ty
+  val ct = cterm_of thy rel
+in
+  Drule.instantiate' [SOME cty] [SOME ct] @{thm equivp_hack}
+end
+*}
+
+ML {* val cheat_alpha_eqvt = Unsynchronized.ref true *}
+ML {* val cheat_equivp = Unsynchronized.ref true *}
+ML {* val cheat_fv_rsp = Unsynchronized.ref true *}
 
 text {* 
   nominal_datatype2 does the following things in order:
@@ -385,7 +402,9 @@
   val _ = warning "Proving equivariance";
   val (bv_eqvt, lthy5) = prove_eqvt raw_tys induct (raw_bn_eqs @ raw_perm_def) (map fst bns) lthy4
   val (fv_eqvt, lthy6) = prove_eqvt raw_tys induct (fv_def @ raw_perm_def) (fv @ fvbn) lthy5
-  fun alpha_eqvt_tac' _ = Skip_Proof.cheat_tac thy
+  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) lthy6 1
   val alpha_eqvt = build_alpha_eqvts alpha_ts alpha_eqvt_tac' lthy6;
 
   (* provind alpha equivalence *)
@@ -393,7 +412,8 @@
   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 alpha_eq_iff lthy6;
   val alpha_equivp =
-    build_equivps alpha_ts reflps alpha_induct
+    if !cheat_equivp then map (equivp_hack lthy6) alpha_ts
+    else build_equivps alpha_ts reflps alpha_induct
       inject alpha_eq_iff distincts alpha_cases alpha_eqvt lthy6;
   val qty_binds = map (fn (_, b, _, _) => b) dts;
   val qty_names = map Name.of_binding qty_binds;
@@ -412,8 +432,9 @@
     fn (bn_t, _) => prove_const_rsp qtys Binding.empty [bn_t] (fn _ =>
        resolve_tac bns_rsp_pre' 1)) bns lthy8;
   val bns_rsp = flat (map snd bns_rsp_pre);
-  (*val _ = map tracing (map PolyML.makestring fv_alpha_all);*)
-  fun fv_rsp_tac _ = Skip_Proof.cheat_tac thy
+
+  fun fv_rsp_tac _ = if !cheat_fv_rsp then Skip_Proof.cheat_tac thy
+    else fvbv_rsp_tac alpha_induct fv_def lthy8 1;
   val fv_rsps = prove_fv_rsp fv_alpha_all alpha_ts fv_rsp_tac lthy9;
   val (fv_rsp_pre, lthy10) = fold_map
     (fn fv => fn ctxt => prove_const_rsp qtys Binding.empty [fv]
@@ -421,6 +442,7 @@
   val fv_rsp = flat (map snd fv_rsp_pre);
   val (perms_rsp, lthy11) = prove_const_rsp qtys Binding.empty perms
     (fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy10;
+(*  val alpha_bn_rsp_pre = prove_alpha_bn_rsp alpha_ts alpha_induct (alpha_eq_iff @ rel_dists @ rel_dists_bn) alpha_equivp exhausts alpha_ts_bn lthy11;*)
   val (alpha_bn_rsps, lthy11a) = fold_map (fn cnst => prove_const_rsp qtys Binding.empty [cnst]
         (fn _ => Skip_Proof.cheat_tac thy)) alpha_ts_bn lthy11
   fun const_rsp_tac _ =
@@ -486,11 +508,11 @@
   val lthy22 = Class.prove_instantiation_instance tac lthy21
   val fv_alpha_all = combine_fv_alpha_bns (qfv_ts_nobn, qfv_ts_bn) (alpha_ts_nobn, qalpha_ts_bn) bn_nos;
   val (names, supp_eq_t) = supp_eq fv_alpha_all;
-  val _ = warning "Support Equations";
+(*  val _ = warning "Support Equations";
   val q_supp = HOLogic.conj_elims (Goal.prove lthy22 names [] supp_eq_t (fn _ => supp_eq_tac q_induct q_fv q_perm q_eq_iff lthy22 1)) handle _ => [];
-  val lthy23 = note_suffix "supp" q_supp lthy22;
+  val lthy23 = note_suffix "supp" q_supp lthy22;*)
 in
-  (0, lthy23)
+  (0, lthy22)
 end
 *}
 
@@ -660,7 +682,7 @@
   (main_parser >> nominal_datatype2_cmd)
 *}
 
-atom_decl name
+(*atom_decl name
 
 nominal_datatype lam =
   Var name
@@ -740,7 +762,7 @@
 thm ty_tys.fv[simplified ty_tys.supp]
 thm ty_tys.eq_iff
 
-
+*)
 
 (* some further tests *)