--- a/Nominal/ExCoreHaskell.thy	Wed Mar 24 11:13:39 2010 +0100
+++ b/Nominal/ExCoreHaskell.thy	Wed Mar 24 12:03:48 2010 +0100
@@ -85,73 +85,8 @@
 | "bv_tvck TVCKNil = {}"
 | "bv_tvck (TVCKCons v k t) = {atom v} \<union> bv_tvck t"
 
-ML {* Sign.of_sort @{theory} (@{typ tkind}, @{sort fs}) *}
-
-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_ckind ckind = supp ckind \<and>
-  fv_ty ty = supp ty \<and>
-  fv_ty_lst ty_lst = supp ty_lst \<and>
-  fv_co co = supp co \<and>
-  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_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 =
-  asm_full_simp_tac (HOL_basic_ss addsimps fv) THEN_ALL_NEW
-  asm_full_simp_tac (HOL_basic_ss addsimps @{thms supp_Abs[symmetric]}) THEN_ALL_NEW
-  simp_tac (HOL_basic_ss addsimps @{thms supp_abs_sum}) THEN_ALL_NEW
-  simp_tac (HOL_basic_ss addsimps @{thms supp_def}) THEN_ALL_NEW
-  simp_tac (HOL_basic_ss addsimps (@{thm permute_ABS} :: perm)) THEN_ALL_NEW
-  simp_tac (HOL_basic_ss addsimps (@{thm Abs_eq_iff} :: eqiff)) THEN_ALL_NEW
-  simp_tac (HOL_basic_ss addsimps @{thms alpha_gen2}) THEN_ALL_NEW
-  simp_tac (HOL_basic_ss addsimps @{thms alpha_gen}) THEN_ALL_NEW
-  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 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 
-  @{thms tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vt_lst_tvtk_lst_tvck_lst.fv}
-  @{thms tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vt_lst_tvtk_lst_tvck_lst.perm}
-  @{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: 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_gen)
-apply (simp only: eqvts[symmetric])
-apply (simp only: eqvts)
-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)
-
-thm supp
-thm tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vt_lst_tvtk_lst_tvck_lst.fv[simplified supp]
+lemmas fv_supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vt_lst_tvtk_lst_tvck_lst.supp(1-9,11,13,15)
+lemmas supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vt_lst_tvtk_lst_tvck_lst.fv[simplified fv_supp]
 
 
 end