diff -r 373cd788d327 -r a40dbea68d0b Nominal/ExCoreHaskell.thy
--- a/Nominal/ExCoreHaskell.thy	Tue Mar 23 17:44:43 2010 +0100
+++ b/Nominal/ExCoreHaskell.thy	Wed Mar 24 08:45:54 2010 +0100
@@ -59,30 +59,92 @@
 | ACons p::"pat" t::"trm" "assoc_lst" bind "bv p" in t
 and pat =
   K "char" "tvtk_lst" "tvck_lst" "vt_lst"
+and vt_lst =
+  VTNil
+| VTCons "var" "ty" "vt_lst"
 and tvtk_lst =
   TVTKNil
 | TVTKCons "tvar" "tkind" "tvtk_lst"
 and tvck_lst =
   TVCKNil
 | TVCKCons "tvar" "ckind" "tvck_lst"
-and vt_lst =
-  VTNil
-| VTCons "var" "ty" "vt_lst"
 binder
     bv :: "pat \<Rightarrow> atom set"
-(*and bv_vt :: "vt_lst \<Rightarrow> atom set"
+and bv_vt :: "vt_lst \<Rightarrow> atom set"
 and bv_tvtk :: "tvtk_lst \<Rightarrow> atom set"
-and bv_tvck :: "tvck_lst \<Rightarrow> atom set"*)
+and bv_tvck :: "tvck_lst \<Rightarrow> atom set"
 where
-  "bv (K s tvts tvcs vs) = {}" (*(bv_tvtk tvts) \<union> (bv_tvck tvcs) \<union> (bv_vt vs) *)
-(*| "bv_vt VTNil = {}"
+  "bv (K s tvts tvcs vs) = (bv_tvtk tvts) \<union> (bv_tvck tvcs) \<union> (bv_vt vs)"
+| "bv_vt VTNil = {}"
 | "bv_vt (VTCons v k t) = {atom v} \<union> bv_vt t"
 | "bv_tvtk TVTKNil = {}"
 | "bv_tvtk (TVTKCons v k t) = {atom v} \<union> bv_tvtk t"
 | "bv_tvck TVCKNil = {}"
-| "bv_tvck (TVCKCons v k t) = {atom v} \<union> bv_tvck t"*)
+| "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))"
+by auto
 
-thm tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_tvtk_lst_tvck_lst_vt_lst.fv
+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_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"
+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 infinite_Un[symmetric] Collect_disj_eq[symmetric]}) THEN_ALL_NEW
+  simp_tac (HOL_basic_ss addsimps @{thms de_Morgan_conj[symmetric]}) 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: 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: de_Morgan_conj[symmetric])
+apply (simp only: helper)
+by (simp)
+
+thm tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vt_lst_tvtk_lst_tvck_lst.fv[simplified supp]
 
 
 end