theory ExCoreHaskell
imports "Parser"
begin

(* core haskell *)

ML {* val _ = recursive := false *}

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
lemmas eq_iff=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vt_lst_tvtk_lst_tvck_lst.eq_iff
lemmas inducts=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vt_lst_tvtk_lst_tvck_lst.inducts

lemmas alpha_inducts=alpha_tkind_raw_alpha_ckind_raw_alpha_ty_raw_alpha_ty_lst_raw_alpha_co_raw_alpha_co_lst_raw_alpha_trm_raw_alpha_assoc_lst_raw_alpha_pat_raw_alpha_vt_lst_raw_alpha_tvtk_lst_raw_alpha_tvck_lst_raw_alpha_bv_raw_alpha_bv_vt_raw_alpha_bv_tvtk_raw_alpha_bv_tvck_raw.inducts
lemmas alpha_intros=alpha_tkind_raw_alpha_ckind_raw_alpha_ty_raw_alpha_ty_lst_raw_alpha_co_raw_alpha_co_lst_raw_alpha_trm_raw_alpha_assoc_lst_raw_alpha_pat_raw_alpha_vt_lst_raw_alpha_tvtk_lst_raw_alpha_tvck_lst_raw_alpha_bv_raw_alpha_bv_vt_raw_alpha_bv_tvtk_raw_alpha_bv_tvck_raw.intros

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)

primrec permute_bv_vt_raw
where "permute_bv_vt_raw p VTNil_raw = VTNil_raw"
|     "permute_bv_vt_raw p (VTCons_raw v t l) = VTCons_raw (p \<bullet> v) t (permute_bv_vt_raw p l)"
primrec permute_bv_tvck_raw
where "permute_bv_tvck_raw p TVCKNil_raw = TVCKNil_raw"
|     "permute_bv_tvck_raw p (TVCKCons_raw v t l) = TVCKCons_raw (p \<bullet> v) t (permute_bv_tvck_raw p l)"
primrec permute_bv_tvtk_raw
where "permute_bv_tvtk_raw p TVTKNil_raw = TVTKNil_raw"
|     "permute_bv_tvtk_raw p (TVTKCons_raw v t l) = TVTKCons_raw (p \<bullet> v) t (permute_bv_tvtk_raw p l)"
primrec permute_bv_raw
where "permute_bv_raw p (K_raw c l1 l2 l3) =
     K_raw c (permute_bv_tvtk_raw p l1) (permute_bv_tvck_raw p l2) (permute_bv_vt_raw p l3)"

quotient_definition "permute_bv_vt :: perm \<Rightarrow> vt_lst \<Rightarrow> vt_lst"
is "permute_bv_vt_raw"
quotient_definition "permute_bv_tvck :: perm \<Rightarrow> tvck_lst \<Rightarrow> tvck_lst"
is "permute_bv_tvck_raw"
quotient_definition "permute_bv_tvtk :: perm \<Rightarrow> tvtk_lst \<Rightarrow> tvtk_lst"
is "permute_bv_tvtk_raw"
quotient_definition "permute_bv :: perm \<Rightarrow> pat \<Rightarrow> pat"
is "permute_bv_raw"

lemma rsp_pre:
 "alpha_tvtk_lst_raw d a \<Longrightarrow> alpha_tvtk_lst_raw (permute_bv_tvtk_raw x d) (permute_bv_tvtk_raw x a)"
 "alpha_tvck_lst_raw e b \<Longrightarrow> alpha_tvck_lst_raw (permute_bv_tvck_raw x e) (permute_bv_tvck_raw x b)"
 "alpha_vt_lst_raw f c \<Longrightarrow> alpha_vt_lst_raw (permute_bv_vt_raw x f) (permute_bv_vt_raw x c)"
 apply (erule_tac [!] alpha_inducts)
 apply simp_all
 apply (rule_tac [!] alpha_intros)
 apply simp_all
 done

lemma [quot_respect]:
 "(op = ===> alpha_pat_raw ===> alpha_pat_raw) permute_bv_raw permute_bv_raw"
 "(op = ===> alpha_tvtk_lst_raw ===> alpha_tvtk_lst_raw) permute_bv_tvtk_raw permute_bv_tvtk_raw"
 "(op = ===> alpha_tvck_lst_raw ===> alpha_tvck_lst_raw) permute_bv_tvck_raw permute_bv_tvck_raw"
 "(op = ===> alpha_vt_lst_raw ===> alpha_vt_lst_raw) permute_bv_vt_raw permute_bv_vt_raw"
 apply (simp_all add: rsp_pre)
 apply clarify
 apply (erule_tac alpha_inducts)
 apply (simp_all)
 apply (rule alpha_intros)
 apply (simp_all add: rsp_pre)
 done

lemmas permute_bv[simp] = permute_bv_raw.simps[quot_lifted]
 permute_bv_vt_raw.simps[quot_lifted]
 permute_bv_tvck_raw.simps[quot_lifted]
 permute_bv_tvtk_raw.simps[quot_lifted]

lemma perm_bv1:
  "p \<bullet> bv_tvck b = bv_tvck (permute_bv_tvck p b)"
  "p \<bullet> bv_tvtk c = bv_tvtk (permute_bv_tvtk p c)"
  "p \<bullet> bv_vt d = bv_vt (permute_bv_vt p d)"
  apply(induct b rule: inducts(12))
  apply(rule TrueI)
  apply(simp_all add:permute_bv eqvts)
  apply(induct c rule: inducts(11))
  apply(rule TrueI)
  apply(simp_all add:permute_bv eqvts)
  apply(induct d rule: inducts(10))
  apply(rule TrueI)
  apply(simp_all add:permute_bv eqvts)
  done

lemma perm_bv2:
  "p \<bullet> bv l = bv (permute_bv p l)"
  apply(induct l rule: inducts(9))
  apply(rule TrueI)
  apply(simp_all add:permute_bv)
  apply(simp add: perm_bv1[symmetric])
  apply(simp add: eqvts)
  done

lemma alpha_perm_bn1:
 " alpha_bv_tvtk tvtk_lst (permute_bv_tvtk q tvtk_lst)"
 "alpha_bv_tvck tvck_lst (permute_bv_tvck q tvck_lst)"
 "alpha_bv_vt vt_lst (permute_bv_vt q vt_lst)"
  apply(induct tvtk_lst rule: inducts(11))
  apply(simp_all add:permute_bv eqvts eq_iff)
  apply(induct tvck_lst rule: inducts(12))
  apply(simp_all add:permute_bv eqvts eq_iff)
  apply(induct vt_lst rule: inducts(10))
  apply(simp_all add:permute_bv eqvts eq_iff)
  done

lemma alpha_perm_bn:
  "alpha_bv pat (permute_bv q pat)"
  apply(induct pat rule: inducts(9))
  apply(simp_all add:permute_bv eqvts eq_iff alpha_perm_bn1)
  done

lemma ACons_subst:
  "supp (Abs (bv pat) trm) \<sharp>* q \<Longrightarrow> (ACons pat trm al) = ACons (permute_bv q pat) (q \<bullet> trm) al"
  apply (simp only: eq_iff)
  apply (rule_tac x="q" in exI)
  apply (simp add: alphas)
  apply (simp add: perm_bv2[symmetric])
  apply (simp add: eqvts[symmetric])
  apply (simp add: supp_abs)
  apply (simp add: fv_supp)
  apply (simp add: alpha_perm_bn)
  apply (rule supp_perm_eq[symmetric])
  apply (subst supp_finite_atom_set)
  apply (rule finite_Diff)
  apply (simp add: finite_supp)
  apply (assumption)
  done

lemma permute_bv_zero1:
  "permute_bv_tvck 0 b = b"
  "permute_bv_tvtk 0 c = c"
  "permute_bv_vt 0 d = d"
  apply(induct b rule: inducts(12))
  apply(rule TrueI)
  apply(simp_all add:permute_bv eqvts)
  apply(induct c rule: inducts(11))
  apply(rule TrueI)
  apply(simp_all add:permute_bv eqvts)
  apply(induct d rule: inducts(10))
  apply(rule TrueI)
  apply(simp_all add:permute_bv eqvts)
  done

lemma permute_bv_zero2:
  "permute_bv 0 a = a"
  apply(induct a rule: inducts(9))
  apply(rule TrueI)
  apply(simp_all add:permute_bv eqvts permute_bv_zero1)
  done

lemma fv_alpha1: "fv_bv_tvtk x \<sharp>* pa \<Longrightarrow> alpha_bv_tvtk (pa \<bullet> x) x"
apply (induct x rule: inducts(11))
apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *})
apply (simp_all add: eq_iff fresh_star_union)
apply (subst supp_perm_eq)
apply (simp_all add: fv_supp)
done

lemma fv_alpha2: "fv_bv_tvck x \<sharp>* pa \<Longrightarrow> alpha_bv_tvck (pa \<bullet> x) x"
apply (induct x rule: inducts(12))
apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *})
apply (simp_all add: eq_iff fresh_star_union)
apply (subst supp_perm_eq)
apply (simp_all add: fv_supp)
done

lemma fv_alpha3: "fv_bv_vt x \<sharp>* pa \<Longrightarrow> alpha_bv_vt (pa \<bullet> x) x"
apply (induct x rule: inducts(10))
apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *})
apply (simp_all add: eq_iff fresh_star_union)
apply (subst supp_perm_eq)
apply (simp_all add: fv_supp)
done

lemma fv_alpha: "fv_bv x \<sharp>* pa \<Longrightarrow> alpha_bv (pa \<bullet> x) x"
apply (induct x rule: inducts(9))
apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *})
apply (simp_all add: eq_iff fresh_star_union)
apply (simp add: fv_alpha1 fv_alpha2 fv_alpha3)
apply (simp add: eqvts)
done

lemma fin1: "finite (fv_bv_tvtk x)"
apply (induct x rule: inducts(11))
apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *})
apply (simp_all add: fv_supp finite_supp)
done

lemma fin2: "finite (fv_bv_tvck x)"
apply (induct x rule: inducts(12))
apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *})
apply (simp_all add: fv_supp finite_supp)
done

lemma fin3: "finite (fv_bv_vt x)"
apply (induct x rule: inducts(10))
apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *})
apply (simp_all add: fv_supp finite_supp)
done

lemma fin_fv_bv: "finite (fv_bv x)"
apply (induct x rule: inducts(9))
apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *})
apply (simp add: fin1 fin2 fin3)
done

lemma finb1: "finite (bv_tvtk x)"
apply (induct x rule: inducts(11))
apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *})
apply (simp_all add: fv_supp finite_supp)
done

lemma finb2: "finite (bv_tvck x)"
apply (induct x rule: inducts(12))
apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *})
apply (simp_all add: fv_supp finite_supp)
done

lemma finb3: "finite (bv_vt x)"
apply (induct x rule: inducts(10))
apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *})
apply (simp_all add: fv_supp finite_supp)
done

lemma fin_bv: "finite (bv x)"
apply (induct x rule: inducts(9))
apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *})
apply (simp add: finb1 finb2 finb3)
done

lemma "bv x \<sharp>* fv_bv x"
apply (induct x rule: inducts(9))
apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *})
apply (simp)
oops

lemma strong_inudction_principle:
  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>
         P5 (e :: 'e :: {pt,fs}) co \<and>
         P6 (f :: 'f :: pt) co_lst \<and>
         P7 (g :: 'g :: {pt,fs}) trm \<and>
         P8 (h :: 'h :: {pt,fs}) assoc_lst \<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 a1: "(\<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 a1:"(\<forall>p q i. P9 i (permute_bv p (q \<bullet> pat)))" and a2:"(\<forall>p q j. P10 j (permute_bv_vt q (p \<bullet> vt_lst)))" and a3:"(\<forall>p q k. P11 k ( permute_bv_tvtk q (p \<bullet> tvtk_lst)))" and a4:"(\<forall>p q l. P12 l (permute_bv_tvck q (p \<bullet> tvck_lst)))"
    apply (induct rule: tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vt_lst_tvtk_lst_tvck_lst.inducts)
    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})) *})

(* GOAL1 *)
    apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (atom (p \<bullet> tvar))) \<sharp> c \<and>
                       supp (Abs (p \<bullet> {atom tvar}) (p \<bullet> ty)) \<sharp>* pa)")
    apply clarify
    apply (simp only: perm)
    apply(rule_tac t="TAll (p \<bullet> tvar) (p \<bullet> tkind) (p \<bullet> ty)"
               and s="TAll (pa \<bullet> p \<bullet> tvar) (p \<bullet> tkind) (pa \<bullet> p \<bullet> ty)" in subst)
    apply (simp only: eq_iff)
    apply (rule_tac x="-pa" in exI)
    apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp)
    apply (rule_tac t="supp (pa \<bullet> p \<bullet> ty) - {atom (pa \<bullet> p \<bullet> tvar)}"
                and s="pa \<bullet> (p \<bullet> supp ty - {p \<bullet> atom tvar})" in subst)
    apply (simp add: eqvts)
    apply (simp add: eqvts[symmetric])
    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)
    apply (rule a08)
    apply simp
    apply(rotate_tac 1)
    apply(erule_tac x="(pa + p)" in allE)
    apply simp
    apply (simp add: eqvts eqvts_raw)
    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

(* GOAL2 *)
    apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (atom (p \<bullet> tvar))) \<sharp> e \<and>
                       supp (Abs (p \<bullet> {atom tvar}) (p \<bullet> co)) \<sharp>* pa)")
    apply clarify
    apply (simp only: perm)
    apply(rule_tac t="CAll (p \<bullet> tvar) (p \<bullet> ckind) (p \<bullet> co)"
               and s="CAll (pa \<bullet> p \<bullet> tvar) (p \<bullet> ckind) (pa \<bullet> p \<bullet> co)" in subst)
    apply (simp only: eq_iff)
    apply (rule_tac x="-pa" in exI)
    apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp)
    apply (rule_tac t="supp (pa \<bullet> p \<bullet> co) - {atom (pa \<bullet> p \<bullet> tvar)}"
                and s="pa \<bullet> (p \<bullet> supp co - {p \<bullet> atom tvar})" in subst)
    apply (simp add: eqvts)
    apply (simp add: eqvts[symmetric])
    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)
    apply (rule a15)
    apply simp
    apply(rotate_tac 1)
    apply(erule_tac x="(pa + p)" in allE)
    apply simp
    apply (simp add: eqvts eqvts_raw)
    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


(* GOAL3 a copy-and-paste of Goal2 with consts and variable names changed *)
    apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (atom (p \<bullet> tvar))) \<sharp> g \<and>
                       supp (Abs (p \<bullet> {atom tvar}) (p \<bullet> trm)) \<sharp>* pa)")
    apply clarify
    apply (simp only: perm)
    apply(rule_tac t="LAMT (p \<bullet> tvar) (p \<bullet> tkind) (p \<bullet> trm)"
               and s="LAMT (pa \<bullet> p \<bullet> tvar) (p \<bullet> tkind) (pa \<bullet> p \<bullet> trm)" in subst)
    apply (simp only: eq_iff)
    apply (rule_tac x="-pa" in exI)
    apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp)
    apply (rule_tac t="supp (pa \<bullet> p \<bullet> trm) - {atom (pa \<bullet> p \<bullet> tvar)}"
                and s="pa \<bullet> (p \<bullet> supp trm - {p \<bullet> atom tvar})" in subst)
    apply (simp add: eqvts)
    apply (simp add: eqvts[symmetric])
    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)
    apply (rule a29)
    apply simp
    apply(rotate_tac 1)
    apply(erule_tac x="(pa + p)" in allE)
    apply simp
    apply (simp add: eqvts eqvts_raw)
    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

(* GOAL4 a copy-and-paste *)
    apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (atom (p \<bullet> tvar))) \<sharp> g \<and>
                       supp (Abs (p \<bullet> {atom tvar}) (p \<bullet> trm)) \<sharp>* pa)")
    apply clarify
    apply (simp only: perm)
    apply(rule_tac t="LAMC (p \<bullet> tvar) (p \<bullet> ckind) (p \<bullet> trm)"
               and s="LAMC (pa \<bullet> p \<bullet> tvar) (p \<bullet> ckind) (pa \<bullet> p \<bullet> trm)" in subst)
    apply (simp only: eq_iff)
    apply (rule_tac x="-pa" in exI)
    apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp)
    apply (rule_tac t="supp (pa \<bullet> p \<bullet> trm) - {atom (pa \<bullet> p \<bullet> tvar)}"
                and s="pa \<bullet> (p \<bullet> supp trm - {p \<bullet> atom tvar})" in subst)
    apply (simp add: eqvts)
    apply (simp add: eqvts[symmetric])
    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)
    apply (rule a30)
    apply simp
    apply(rotate_tac 1)
    apply(erule_tac x="(pa + p)" in allE)
    apply simp
    apply (simp add: eqvts eqvts_raw)
    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


(* GOAL5 a copy-and-paste *)
    apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (atom (p \<bullet> var))) \<sharp> g \<and>
                       supp (Abs (p \<bullet> {atom var}) (p \<bullet> trm)) \<sharp>* pa)")
    apply clarify
    apply (simp only: perm)
    apply(rule_tac t="Lam (p \<bullet> var) (p \<bullet> ty) (p \<bullet> trm)"
               and s="Lam (pa \<bullet> p \<bullet> var) (p \<bullet> ty) (pa \<bullet> p \<bullet> trm)" in subst)
    apply (simp only: eq_iff)
    apply (rule_tac x="-pa" in exI)
    apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp)
    apply (rule_tac t="supp (pa \<bullet> p \<bullet> trm) - {atom (pa \<bullet> p \<bullet> var)}"
                and s="pa \<bullet> (p \<bullet> supp trm - {p \<bullet> atom var})" in subst)
    apply (simp add: eqvts)
    apply (simp add: eqvts[symmetric])
    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)
    apply (rule a32)
    apply simp
    apply(rotate_tac 1)
    apply(erule_tac x="(pa + p)" in allE)
    apply simp
    apply (simp add: eqvts eqvts_raw)
    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


(* GOAL6 a copy-and-paste *)
    apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (atom (p \<bullet> var))) \<sharp> g \<and>
                       supp (Abs (p \<bullet> {atom var}) (p \<bullet> trm2)) \<sharp>* pa)")
    apply clarify
    apply (simp only: perm)
    apply(rule_tac t="Let (p \<bullet> var) (p \<bullet> ty) (p \<bullet> trm1) (p \<bullet> trm2)"
               and s="Let (pa \<bullet> p \<bullet> var) (p \<bullet> ty) (p \<bullet> trm1) (pa \<bullet> p \<bullet> trm2)" in subst)
    apply (simp only: eq_iff)
    apply (rule_tac x="-pa" in exI)
    apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp)
    apply (rule_tac t="supp (pa \<bullet> p \<bullet> trm2) - {atom (pa \<bullet> p \<bullet> var)}"
                and s="pa \<bullet> (p \<bullet> supp trm2 - {p \<bullet> atom var})" in subst)
    apply (simp add: eqvts)
    apply (simp add: eqvts[symmetric])
    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)
    apply (rule a34)
    apply simp
    apply simp
    apply(rotate_tac 2)
    apply(erule_tac x="(pa + p)" in allE)
    apply simp
    apply (simp add: eqvts eqvts_raw)
    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

(* MAIN ACons Goal *)
    apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (bv (p \<bullet> pat))) \<sharp>* h \<and>
                       supp (Abs (p \<bullet> (bv pat)) (p \<bullet> trm)) \<sharp>* pa)")
    apply clarify
    apply (simp only: perm eqvts)
    apply (subst ACons_subst)
    apply assumption
    apply (rule a38)
    apply simp
    apply(rotate_tac 1)
    apply(erule_tac x="(pa + p)" in allE)
    apply simp
    apply simp
    apply (simp add: perm_bv2[symmetric])
    apply (simp add: eqvts eqvts_raw)
    apply (rule at_set_avoiding2)
    apply (simp add: fin_bv)
    apply (simp add: finite_supp)
    apply (simp add: supp_abs)
    apply (rule finite_Diff)
    apply (simp add: finite_supp)
    apply (simp add: fresh_star_def fresh_def supp_abs eqvts)
    done
  then have b: "P1 a (0 \<bullet> tkind)" and "P2 b (0 \<bullet> ckind)" "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)" by (blast+)
  moreover have "P9  i (permute_bv 0 (0 \<bullet> pat))" and "P10 j (permute_bv_vt 0 (0 \<bullet> vt_lst))" and "P11 k (permute_bv_tvtk 0 (0 \<bullet> tvtk_lst))" and "P12 l (permute_bv_tvck 0 (0 \<bullet> tvck_lst))" using a1 a2 a3 a4 by (blast+)
  ultimately show ?thesis by (simp_all add: permute_bv_zero1 permute_bv_zero2)
qed

end

