theory ExCoreHaskell
imports "Parser"
begin

(* core haskell *)

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

(* 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}) *}

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]


end