--- 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