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"

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]

lemmas perm=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vt_lst_tvtk_lst_tvck_lst.perm

lemma fresh_star_minus_perm: "as \<sharp>* - p = as \<sharp>* (p :: perm)"

  unfolding fresh_star_def Ball_def

  by auto (simp_all add: fresh_minus_perm)

lemma 

  assumes a01: "\<And>b. P1 b KStar"

  and a02: "\<And>tkind1 tkind2 b. \<lbrakk>\<And>c. P1 c tkind1; \<And>c. P1 c tkind2\<rbrakk> \<Longrightarrow> P1 b (KFun tkind1 tkind2)"

  and a03: "\<And>ty1 ty2 b. \<lbrakk>\<And>c. P3 c ty1; \<And>c. P3 c ty2\<rbrakk> \<Longrightarrow> P2 b (CKEq ty1 ty2)"

  and a04: "\<And>tvar b. P3 b (TVar tvar)"

  and a05: "\<And>char b. P3 b (TC char)"

  and a06: "\<And>ty1 ty2 b. \<lbrakk>\<And>c. P3 c ty1; \<And>c. P3 c ty2\<rbrakk> \<Longrightarrow> P3 b (TApp ty1 ty2)"

  and a07: "\<And>char ty_lst b. \<lbrakk>\<And>c. P4 c ty_lst\<rbrakk> \<Longrightarrow> P3 b (TFun char ty_lst)"

  and a08: "\<And>tvar tkind ty b. \<lbrakk>\<And>c. P1 c tkind; \<And>c. P3 c ty; atom tvar \<sharp> b\<rbrakk>

    \<Longrightarrow> P3 b (TAll tvar tkind ty)"

  and a09: "\<And>ty1 ty2 ty3 b. \<lbrakk>\<And>c. P3 c ty1; \<And>c. P3 c ty2; \<And>c. P3 c ty3\<rbrakk> \<Longrightarrow> P3 b (TEq ty1 ty2 ty3)"

  and a10: "\<And>b. P4 b TsNil"

  and a11: "\<And>ty ty_lst b. \<lbrakk>\<And>c. P3 c ty; \<And>c. P4 c ty_lst\<rbrakk> \<Longrightarrow> P4 b (TsCons ty ty_lst)"

  and a12: "\<And>char b. P5 b (CC char)"

  and a13: "\<And>co1 co2 b. \<lbrakk>\<And>c. P5 c co1; \<And>c. P5 c co2\<rbrakk> \<Longrightarrow> P5 b (CApp co1 co2)"

  and a14: "\<And>char co_lst b. \<lbrakk>\<And>c. P6 c co_lst\<rbrakk> \<Longrightarrow> P5 b (CFun char co_lst)"

  and a15: "\<And>tvar ckind co b. \<lbrakk>\<And>c. P2 c ckind; \<And>c. P5 c co; atom tvar \<sharp> b\<rbrakk>

    \<Longrightarrow> P5 b (CAll tvar ckind co)"

  and a16: "\<And>co1 co2 co3 b. \<lbrakk>\<And>c. P5 c co1; \<And>c. P5 c co2; \<And>c. P5 c co3\<rbrakk> \<Longrightarrow> P5 b (CEq co1 co2 co3)"

  and a17: "\<And>co b. \<lbrakk>\<And>c. P5 c co\<rbrakk> \<Longrightarrow> P5 b (CSym co)"

  and a18: "\<And>co1 co2 b. \<lbrakk>\<And>c. P5 c co1; \<And>c. P5 c co2\<rbrakk> \<Longrightarrow> P5 b (CCir co1 co2)"

  and a19: "\<And>co b. \<lbrakk>\<And>c. P5 c co\<rbrakk> \<Longrightarrow> P5 b (CLeft co)"

  and a20: "\<And>co b. \<lbrakk>\<And>c. P5 c co\<rbrakk> \<Longrightarrow> P5 b (CRight co)"

  and a21: "\<And>co b. \<lbrakk>\<And>c. P5 c co\<rbrakk> \<Longrightarrow> P5 b (CSim co)"

  and a22: "\<And>co b. \<lbrakk>\<And>c. P5 c co\<rbrakk> \<Longrightarrow> P5 b (CRightc co)"

  and a23: "\<And>co b. \<lbrakk>\<And>c. P5 c co\<rbrakk> \<Longrightarrow> P5 b (CLeftc co)"

  and a24: "\<And>co1 co2 b. \<lbrakk>\<And>c. P5 c co1; \<And>c. P5 c co2\<rbrakk> \<Longrightarrow> P5 b (CCoe co1 co2)"

  and a25: "\<And>b. P6 b CsNil"

  and a26: "\<And>co co_lst b. \<lbrakk>\<And>c. P5 c co; \<And>c. P6 c co_lst\<rbrakk> \<Longrightarrow> P6 b (CsCons co co_lst)"

  and a27: "\<And>var b. P7 b (Var var)"

  and a28: "\<And>char b. P7 b (C char)"

  and a29: "\<And>tvar tkind trm b. \<lbrakk>\<And>c. P1 c tkind; \<And>c. P7 c trm; atom tvar \<sharp> b\<rbrakk>

    \<Longrightarrow> P7 b (LAMT tvar tkind trm)"

  and a30: "\<And>tvar ckind trm b. \<lbrakk>\<And>c. P2 c ckind; \<And>c. P7 c trm; atom tvar \<sharp> b\<rbrakk>

    \<Longrightarrow> P7 b (LAMC tvar ckind trm)"

  and a31: "\<And>trm ty b. \<lbrakk>\<And>c. P7 c trm; \<And>c. P3 c ty\<rbrakk> \<Longrightarrow> P7 b (APP trm ty)"

  and a32: "\<And>var ty trm b. \<lbrakk>\<And>c. P3 c ty; \<And>c. P7 c trm; atom var \<sharp> b\<rbrakk> \<Longrightarrow> P7 b (Lam var ty trm)"

  and a33: "\<And>trm1 trm2 b. \<lbrakk>\<And>c. P7 c trm1; \<And>c. P7 c trm2\<rbrakk> \<Longrightarrow> P7 b (App trm1 trm2)"

  and a34: "\<And>var ty trm1 trm2 b. \<lbrakk>\<And>c. P3 c ty; \<And>c. P7 c trm1; \<And>c. P7 c trm2; atom var \<sharp> b\<rbrakk>

    \<Longrightarrow> P7 b (Let var ty trm1 trm2)"

  and a35: "\<And>trm assoc_lst b. \<lbrakk>\<And>c. P7 c trm; \<And>c. P8 c assoc_lst\<rbrakk> \<Longrightarrow> P7 b (Case trm assoc_lst)"

  and a36: "\<And>trm ty b. \<lbrakk>\<And>c. P7 c trm; \<And>c. P3 c ty\<rbrakk> \<Longrightarrow> P7 b (Cast trm ty)"

  and a37: "\<And>b. P8 b ANil"

  and a38: "\<And>pat trm assoc_lst b. \<lbrakk>\<And>c. P9 c pat; \<And>c. P7 c trm; \<And>c. P8 c assoc_lst; bv(pat) \<sharp>* b\<rbrakk>

    \<Longrightarrow> P8 b (ACons pat trm assoc_lst)"

  and a39: "\<And>char tvtk_lst tvck_lst vt_lst b. \<lbrakk>\<And>c. P11 c tvtk_lst; \<And>c. P12 c tvck_lst; \<And>c. P10 c vt_lst\<rbrakk>

    \<Longrightarrow> P9 b (K char tvtk_lst tvck_lst vt_lst)"

  and a40: "\<And>b. P10 b VTNil"

  and a41: "\<And>var ty vt_lst b. \<lbrakk>\<And>c. P3 c ty; \<And>c. P10 c vt_lst\<rbrakk> \<Longrightarrow> P10 b (VTCons var ty vt_lst)"

  and a42: "\<And>b. P11 b TVTKNil"

  and a43: "\<And>tvar tkind tvtk_lst b. \<lbrakk>\<And>c. P1 c tkind; \<And>c. P11 c tvtk_lst\<rbrakk>

    \<Longrightarrow> P11 b (TVTKCons tvar tkind tvtk_lst)"

  and a44: "\<And>b. P12 b TVCKNil"

  and a45: "\<And>tvar ckind tvck_lst b. \<lbrakk>\<And>c. P2 c ckind; \<And>c. P12 c tvck_lst\<rbrakk>

    \<Longrightarrow> P12 b (TVCKCons tvar ckind tvck_lst)"

  shows "P1 (a :: 'a :: pt) tkind \<and>

         P2 (b :: 'b :: pt) ckind \<and>

         P3 (c :: 'c :: {pt,fs}) ty \<and>

         P4 (d :: 'd :: pt) ty_lst \<and>

         P6 (f :: 'f :: pt) co_lst \<and>

         P7 (g :: 'g :: pt) trm \<and>

         P9 (i :: 'i :: pt) pat \<and>

         P10 (j :: 'j :: pt) vt_lst \<and>

         P11 (k :: 'k :: pt) tvtk_lst \<and>

         P12 (l :: 'l :: pt) tvck_lst"

proof -

  have a: "(\<forall>p a. P1 a (p \<bullet> tkind)) \<and> (\<forall>p b. P2 b (p \<bullet> ckind)) \<and> (\<forall>p c. P3 c (p \<bullet> ty)) \<and> (\<forall>p d. P4 d (p \<bullet> ty_lst)) \<and> (\<forall>p e. P5 e (p \<bullet> co)) \<and> (\<forall>p f. P6 f (p \<bullet> co_lst)) \<and> (\<forall>p g. P7 g (p \<bullet> trm)) \<and> (\<forall>p h. P8 h (p \<bullet> assoc_lst)) \<and> (\<forall>p i. P9 i (p \<bullet> pat)) \<and> (\<forall>p j. P10 j (p \<bullet> vt_lst)) \<and> (\<forall>p k. P11 k (p \<bullet> tvtk_lst)) \<and> (\<forall>p l. P12 l (p \<bullet> tvck_lst))"

    apply (rule tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vt_lst_tvtk_lst_tvck_lst.induct)

    apply (tactic {* ALLGOALS (REPEAT o rtac allI) *})

    apply (tactic {* ALLGOALS (TRY o SOLVED' (simp_tac @{simpset} THEN_ALL_NEW resolve_tac @{thms assms} THEN_ALL_NEW asm_full_simp_tac @{simpset})) *})

    apply (rule at_set_avoiding2_atom)

    apply (simp add: finite_supp)

    apply (simp add: finite_supp)

    apply (simp add: fresh_def)

    apply (simp only: supp_Abs eqvts)

    apply blast

    apply clarify

    apply (simp only: perm)

    apply (rule_tac x="-pa" in exI)

    apply (rule conjI)

    apply (rule supp_perm_eq)

    apply (simp add: eqvts)

    apply (subst supp_finite_atom_set)

    apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp)

    apply (simp add: eqvts)

    apply (simp add: eqvts)

    apply (subst supp_perm_eq)

    apply (subst supp_finite_atom_set)

    apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp)

    apply (simp add: eqvts)

    apply assumption

    apply (simp add: fresh_star_minus_perm)

    sorry

  have g1: "P1 a (0 \<bullet> tkind)" using a[THEN conjunct1] by blast

  have g2: "P2 b (0 \<bullet> ckind)" using a[THEN conjunct2,THEN conjunct1] by blast

  have g3: "P3 c (0 \<bullet> ty) \<and>

        P4 d (0 \<bullet> ty_lst) \<and> P5 e (0 \<bullet> co) \<and> P6 f (0 \<bullet> co_lst) \<and>

        P7 g (0 \<bullet> trm) \<and> P8 h (0 \<bullet> assoc_lst) \<and> P9 i (0 \<bullet> pat) \<and>

        P10 j (0 \<bullet> vt_lst) \<and> P11 k (0 \<bullet> tvtk_lst) \<and> P12 l (0 \<bullet> tvck_lst)" using a by blast

  show ?thesis using g1 g2 g3 by simp

qed

end