theory ExCoreHaskell

imports "Parser"

begin

(* core haskell *)

atom_decl var

atom_decl tvar

(* there are types, coercion types and regular types list-data-structure *)

nominal_datatype tkind =

  KStar

| KFun "tkind" "tkind"

and ckind =

  CKEq "ty" "ty"

and ty =

  TVar "tvar"

| TC "char"

| TApp "ty" "ty"

| TFun "char" "ty_lst"

| TAll tv::"tvar" "tkind" T::"ty"  bind tv in T

| TEq "ty" "ty" "ty"

and ty_lst =

  TsNil

| TsCons "ty" "ty_lst"

and co =

  CC "char"

| CApp "co" "co"

| CFun "char" "co_lst"

| CAll tv::"tvar" "ckind" C::"co"  bind tv in C

| CEq "co" "co" "co"

| CSym "co"

| CCir "co" "co"

| CLeft "co"

| CRight "co"

| CSim "co"

| CRightc "co"

| CLeftc "co"

| CCoe "co" "co"

and co_lst =

  CsNil

| CsCons "co" "co_lst"

and trm =

  Var "var"

| C "char"

| LAMT tv::"tvar" "tkind" t::"trm" bind tv in t

| LAMC tv::"tvar" "ckind" t::"trm" bind tv in t

| APP "trm" "ty"

| Lam v::"var" "ty" t::"trm"       bind v in t

| App "trm" "trm"

| Let x::"var" "ty" "trm" t::"trm" bind x in t

| Case "trm" "assoc_lst"

| Cast "trm" "ty"                  --"ty is supposed to be a coercion type only"

and assoc_lst =

  ANil

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

binder

    bv :: "pat \<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"

where

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

ML {* Sign.of_sort @{theory} (@{typ tkind}, @{sort fs}) *}

by auto

lemma supp:

  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>

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 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: 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: de_Morgan_conj[symmetric])

apply (simp only: helper)

thm tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vt_lst_tvtk_lst_tvck_lst.fv[simplified supp]

end