--- a/Nominal/ExCoreHaskell.thy	Wed Mar 24 10:49:50 2010 +0100
+++ b/Nominal/ExCoreHaskell.thy	Wed Mar 24 10:55:59 2010 +0100
@@ -4,8 +4,11 @@
 
 (* core haskell *)
 
-ML {* val _ = recursive := false  *}
-
+ML {* val _ = recursive := false *}
+ML {* val _ = cheat_bn_eqvt := true *}
+ML {* val _ = cheat_bn_rsp := true *}
+ML {* val _ = cheat_const_rsp := true *}
+ML {* val _ = cheat_alpha_bn_rsp := true *}
 atom_decl var
 atom_decl tvar
 
@@ -84,11 +87,13 @@
 
 ML {* Sign.of_sort @{theory} (@{typ tkind}, @{sort fs}) *}
 
-lemma helper: "((\<exists>p. P p) \<and> Q) = (\<exists>p. (P p \<and> Q))"
+lemma helper: 
+  "((\<exists>p. P p) \<and> Q) = (\<exists>p. (P p \<and> Q))"
+  "(Q \<and> (\<exists>p. P p)) = (\<exists>p. (Q \<and> P p))"
 by auto
 
 lemma supp:
- "fv_tkind tkind = supp tkind \<and>
+  "fv_tkind tkind = supp tkind \<and>
   fv_ckind ckind = supp ckind \<and>
   fv_ty ty = supp ty \<and>
   fv_ty_lst ty_lst = supp ty_lst \<and>
@@ -96,10 +101,13 @@
   fv_co_lst co_lst = supp co_lst \<and>
   fv_trm trm = supp trm \<and>
   fv_assoc_lst assoc_lst = supp assoc_lst \<and>
-  fv_pat pat = supp pat \<and>
-  fv_vt_lst vt_lst = supp vt_lst \<and>
-  fv_tvtk_lst tvtk_lst = supp tvtk_lst \<and>
-  fv_tvck_lst tvck_lst = supp tvck_lst"
+  (fv_pat pat = supp pat \<and> fv_bv pat = {a. infinite {b. \<not> alpha_bv ((a \<rightleftharpoons> b) \<bullet> pat) pat}}) \<and>
+  (fv_vt_lst vt_lst = supp vt_lst \<and>
+   fv_bv_vt vt_lst = {a. infinite {b. \<not> alpha_bv_vt ((a \<rightleftharpoons> b) \<bullet> vt_lst) vt_lst}}) \<and>
+  (fv_tvtk_lst tvtk_lst = supp tvtk_lst \<and>
+   fv_bv_tvtk tvtk_lst = {a. infinite {b. \<not> alpha_bv_tvtk ((a \<rightleftharpoons> b) \<bullet> tvtk_lst) tvtk_lst}}) \<and>
+  fv_tvck_lst tvck_lst = supp tvck_lst \<and>
+  fv_bv_tvck tvck_lst = {a. infinite {b. \<not> alpha_bv_tvck ((a \<rightleftharpoons> b) \<bullet> tvck_lst) tvck_lst}}"
 apply(rule tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vt_lst_tvtk_lst_tvck_lst.induct)
 ML_prf {*
 fun supp_eq_tac fv perm eqiff ctxt =
@@ -114,8 +122,11 @@
   asm_full_simp_tac (HOL_basic_ss addsimps (@{thm supp_Pair} :: sym_eqvts ctxt)) THEN_ALL_NEW
   asm_full_simp_tac (HOL_basic_ss addsimps (@{thm Pair_eq} :: all_eqvts ctxt)) THEN_ALL_NEW
   simp_tac (HOL_basic_ss addsimps @{thms supp_at_base[symmetric,simplified supp_def]}) THEN_ALL_NEW
-  simp_tac (HOL_basic_ss addsimps @{thms infinite_Un[symmetric] Collect_disj_eq[symmetric]}) THEN_ALL_NEW
+  simp_tac (HOL_basic_ss addsimps @{thms Collect_disj_eq[symmetric]}) THEN_ALL_NEW
+  simp_tac (HOL_basic_ss addsimps @{thms infinite_Un[symmetric]}) THEN_ALL_NEW
+  simp_tac (HOL_basic_ss addsimps @{thms Collect_disj_eq[symmetric]}) THEN_ALL_NEW
   simp_tac (HOL_basic_ss addsimps @{thms de_Morgan_conj[symmetric]}) THEN_ALL_NEW
+  simp_tac (HOL_basic_ss addsimps @{thms helper}) THEN_ALL_NEW
   simp_tac (HOL_ss addsimps @{thms Collect_const finite.emptyI})
 *}
 apply (tactic {* ALLGOALS (TRY o SOLVED' (supp_eq_tac 
@@ -124,26 +135,22 @@
   @{thms tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vt_lst_tvtk_lst_tvck_lst.eq_iff}
   @{context})) *})
 apply (simp only: tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vt_lst_tvtk_lst_tvck_lst.fv)
-apply (simp only: Un_assoc[symmetric])
-apply (simp only: Un_Diff[symmetric])
-apply (simp only: supp_Pair[symmetric])
 apply (simp only: supp_Abs[symmetric])
 apply (simp (no_asm) only: supp_def)
 apply (simp only: permute_ABS)
 apply (simp only: tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vt_lst_tvtk_lst_tvck_lst.perm)
 apply (simp only: Abs_eq_iff)
 apply (simp only: tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vt_lst_tvtk_lst_tvck_lst.eq_iff)
-apply (simp only: alpha_gen2)
 apply (simp only: alpha_gen)
 apply (simp only: eqvts[symmetric])
-apply (simp only: supp_Pair)
 apply (simp only: eqvts)
-apply (simp only: Pair_eq)
-apply (simp only: infinite_Un[symmetric] Collect_disj_eq[symmetric])
+apply (simp only: Collect_disj_eq[symmetric])
+apply (simp only: infinite_Un[symmetric])
+apply (simp only: Collect_disj_eq[symmetric])
 apply (simp only: de_Morgan_conj[symmetric])
 apply (simp only: helper)
-by (simp)
 
+thm supp
 thm tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vt_lst_tvtk_lst_tvck_lst.fv[simplified supp]