theory ExCoreHaskell

imports "../Parser"

begin

(* core haskell *)

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

(* this should not be an equivariance rule *)

(* for the moment, we force it to be       *)

setup {* Context.theory_map (Nominal_ThmDecls.add_thm @{thm "permute_pure"}) *}

thm eqvts

(*declare permute_pure[eqvt]*)

atom_decl var

atom_decl cvar

atom_decl tvar

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

ML {* val _ = alpha_type := AlphaLst *}

nominal_datatype tkind =

  KStar

| KFun "tkind" "tkind"

and ckind =

  CKEq "ty" "ty"

and ty =

  TVar "tvar"

| TC "string"

| TApp "ty" "ty"

| TFun "string" "ty_lst"

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

| TEq "ckind" "ty"

and ty_lst =

  TsNil

| TsCons "ty" "ty_lst"

and co =

  CVar "cvar"

| CConst "string"

| CApp "co" "co"

| CFun "string" "co_lst"

| CAll cv::"cvar" "ckind" C::"co"  bind cv in C

| CEq "ckind" "co"

| CRefl "ty"

| CSym "co"

| CCir "co" "co"

| CAt "co" "ty"

| CLeft "co"

| CRight "co"

| CSim "co" "co"

| CRightc "co"

| CLeftc "co"

| CCoe "co" "co"

and co_lst =

  CsNil

| CsCons "co" "co_lst"

and trm =

  Var "var"

| K "string"

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

| LAMC cv::"cvar" "ckind" t::"trm" bind cv in t

| AppT "trm" "ty"

| AppC "trm" "co"

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

  Kpat "string" "tvars" "cvars" "vars"

and vars =

  VsNil

| VsCons "var" "ty" "vars"

and tvars =

  TvsNil

| TvsCons "tvar" "tkind" "tvars"

and cvars =

  CvsNil

| CvsCons "cvar" "ckind" "cvars"

binder

    bv :: "pat \<Rightarrow> atom list"

and bv_vs :: "vars \<Rightarrow> atom list"

and bv_tvs :: "tvars \<Rightarrow> atom list"

and bv_cvs :: "cvars \<Rightarrow> atom list"

where

  "bv (Kpat s tvts tvcs vs) = append (bv_tvs tvts) (append (bv_cvs tvcs) (bv_vs vs))"

| "bv_vs VsNil = []"

| "bv_vs (VsCons v k t) = (atom v) # bv_vs t"

| "bv_tvs TvsNil = []"

| "bv_tvs (TvsCons v k t) = (atom v) # bv_tvs t"

| "bv_cvs CvsNil = []"

| "bv_cvs (CvsCons v k t) = (atom v) # bv_cvs t"

(*

function

rfv_tkind_raw and rfv_ckind_raw and rfv_ty_raw and rfv_ty_lst_raw and rfv_co_raw and rfv_co_lst_raw and rfv_trm_raw and rfv_assoc_lst_raw and rfv_bv_raw and rfv_bv_vs_raw and rfv_bv_tvs_raw and rfv_bv_cvs_raw and rfv_pat_raw and rfv_vars_raw and rfv_tvars_raw and rfv_cvars_raw

where

  "rfv_tkind_raw KStar_raw = {}"

| "rfv_tkind_raw (KFun_raw tkind_raw1 tkind_raw2) = rfv_tkind_raw tkind_raw1 \<union> rfv_tkind_raw tkind_raw2"

| "rfv_ckind_raw (CKEq_raw ty_raw1 ty_raw2) = rfv_ty_raw ty_raw1 \<union> rfv_ty_raw ty_raw2"

| "rfv_ty_raw (TVar_raw tvar) = {atom tvar}"

| "rfv_ty_raw (TC_raw list) = {}"

| "rfv_ty_raw (TApp_raw ty_raw1 ty_raw2) = rfv_ty_raw ty_raw1 \<union> rfv_ty_raw ty_raw2"

| "rfv_ty_raw (TFun_raw list ty_lst_raw) = rfv_ty_lst_raw ty_lst_raw"

| "rfv_ty_raw (TAll_raw tvar tkind_raw ty_raw) =

 rfv_tkind_raw tkind_raw \<union> (rfv_ty_raw ty_raw - {atom tvar})"

| "rfv_ty_raw (TEq_raw ckind_raw ty_raw) = rfv_ckind_raw ckind_raw \<union> rfv_ty_raw ty_raw"

| "rfv_ty_lst_raw TsNil_raw = {}"

| "rfv_ty_lst_raw (TsCons_raw ty_raw ty_lst_raw) = rfv_ty_raw ty_raw \<union> rfv_ty_lst_raw ty_lst_raw"

| "rfv_co_raw (CVar_raw cvar) = {atom cvar}"

| "rfv_co_raw (CConst_raw list) = {}"

| "rfv_co_raw (CApp_raw co_raw1 co_raw2) = rfv_co_raw co_raw1 \<union> rfv_co_raw co_raw2"

| "rfv_co_raw (CFun_raw list co_lst_raw) = rfv_co_lst_raw co_lst_raw"

| "rfv_co_raw (CAll_raw cvar ckind_raw co_raw) =

 rfv_ckind_raw ckind_raw \<union> (rfv_co_raw co_raw - {atom cvar})"

| "rfv_co_raw (CEq_raw ckind_raw co_raw) = rfv_ckind_raw ckind_raw \<union> rfv_co_raw co_raw"

| "rfv_co_raw (CRefl_raw ty_raw) = rfv_ty_raw ty_raw"

| "rfv_co_raw (CSym_raw co_raw) = rfv_co_raw co_raw"

| "rfv_co_raw (CCir_raw co_raw1 co_raw2) = rfv_co_raw co_raw1 \<union> rfv_co_raw co_raw2"

| "rfv_co_raw (CAt_raw co_raw ty_raw) = rfv_co_raw co_raw \<union> rfv_ty_raw ty_raw"

| "rfv_co_raw (CLeft_raw co_raw) = rfv_co_raw co_raw"

| "rfv_co_raw (CRight_raw co_raw) = rfv_co_raw co_raw"

| "rfv_co_raw (CSim_raw co_raw1 co_raw2) = rfv_co_raw co_raw1 \<union> rfv_co_raw co_raw2"

| "rfv_co_raw (CRightc_raw co_raw) = rfv_co_raw co_raw"

| "rfv_co_raw (CLeftc_raw co_raw) = rfv_co_raw co_raw"

| "rfv_co_raw (CCoe_raw co_raw1 co_raw2) = rfv_co_raw co_raw1 \<union> rfv_co_raw co_raw2"

| "rfv_co_lst_raw CsNil_raw = {}"

| "rfv_co_lst_raw (CsCons_raw co_raw co_lst_raw) = rfv_co_raw co_raw \<union> rfv_co_lst_raw co_lst_raw"

| "rfv_trm_raw (Var_raw var) = {atom var}"

| "rfv_trm_raw (K_raw list) = {}"

| "rfv_trm_raw (LAMT_raw tvar tkind_raw trm_raw) =

 rfv_tkind_raw tkind_raw \<union> (rfv_trm_raw trm_raw - {atom tvar})"

| "rfv_trm_raw (LAMC_raw cvar ckind_raw trm_raw) =

 rfv_ckind_raw ckind_raw \<union> (rfv_trm_raw trm_raw - {atom cvar})"

| "rfv_trm_raw (AppT_raw trm_raw ty_raw) = rfv_trm_raw trm_raw \<union> rfv_ty_raw ty_raw"

| "rfv_trm_raw (AppC_raw trm_raw co_raw) = rfv_trm_raw trm_raw \<union> rfv_co_raw co_raw"

| "rfv_trm_raw (Lam_raw var ty_raw trm_raw) = rfv_ty_raw ty_raw \<union> (rfv_trm_raw trm_raw - {atom var})"

| "rfv_trm_raw (App_raw trm_raw1 trm_raw2) = rfv_trm_raw trm_raw1 \<union> rfv_trm_raw trm_raw2"

| "rfv_trm_raw (Let_raw var ty_raw trm_raw1 trm_raw2) =

 rfv_ty_raw ty_raw \<union> (rfv_trm_raw trm_raw1 \<union> (rfv_trm_raw trm_raw2 - {atom var}))"

| "rfv_trm_raw (Case_raw trm_raw assoc_lst_raw) = rfv_trm_raw trm_raw \<union> rfv_assoc_lst_raw assoc_lst_raw"

| "rfv_trm_raw (Cast_raw trm_raw ty_raw) = rfv_trm_raw trm_raw \<union> rfv_ty_raw ty_raw"

| "rfv_assoc_lst_raw ANil_raw = {}"

| "rfv_assoc_lst_raw (ACons_raw pat_raw trm_raw assoc_lst_raw) =

 rfv_bv_raw pat_raw \<union> (rfv_trm_raw trm_raw - set (bv_raw pat_raw) \<union> rfv_assoc_lst_raw assoc_lst_raw)"

| "rfv_bv_raw (Kpat_raw list tvars_raw cvars_raw vars_raw) =

 rfv_bv_tvs_raw tvars_raw \<union> (rfv_bv_cvs_raw cvars_raw \<union> rfv_bv_vs_raw vars_raw)"

| "rfv_bv_vs_raw VsNil_raw = {}"

| "rfv_bv_vs_raw (VsCons_raw var ty_raw vars_raw) = rfv_ty_raw ty_raw \<union> rfv_bv_vs_raw vars_raw"

| "rfv_bv_tvs_raw TvsNil_raw = {}"

| "rfv_bv_tvs_raw (TvsCons_raw tvar tkind_raw tvars_raw) =

 rfv_tkind_raw tkind_raw \<union> rfv_bv_tvs_raw tvars_raw"

| "rfv_bv_cvs_raw CvsNil_raw = {}"

| "rfv_bv_cvs_raw (CvsCons_raw cvar ckind_raw cvars_raw) =

 rfv_ckind_raw ckind_raw \<union> rfv_bv_cvs_raw cvars_raw"

| "rfv_pat_raw (Kpat_raw list tvars_raw cvars_raw vars_raw) =

 rfv_tvars_raw tvars_raw \<union> (rfv_cvars_raw cvars_raw \<union> rfv_vars_raw vars_raw)"

| "rfv_vars_raw VsNil_raw = {}"

| "rfv_vars_raw (VsCons_raw var ty_raw vars_raw) =

 {atom var} \<union> (rfv_ty_raw ty_raw \<union> rfv_vars_raw vars_raw)"

| "rfv_tvars_raw TvsNil_raw = {}"

| "rfv_tvars_raw (TvsCons_raw tvar tkind_raw tvars_raw) =

 {atom tvar} \<union> (rfv_tkind_raw tkind_raw \<union> rfv_tvars_raw tvars_raw)"

| "rfv_cvars_raw CvsNil_raw = {}"

| "rfv_cvars_raw (CvsCons_raw cvar ckind_raw cvars_raw) =

 {atom cvar} \<union> (rfv_ckind_raw ckind_raw \<union> rfv_cvars_raw cvars_raw)"

apply pat_completeness

apply auto

done

termination

by lexicographic_order

*)

lemmas fv_supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.supp(1-9,11,13,15)

lemmas supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.fv[simplified fv_supp]

lemmas perm=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.perm

lemmas eq_iff=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.eq_iff

lemmas inducts=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.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_vars_raw_alpha_tvars_raw_alpha_cvars_raw_alpha_bv_raw_alpha_bv_vs_raw_alpha_bv_tvs_raw_alpha_bv_cvs_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_vars_raw_alpha_tvars_raw_alpha_cvars_raw_alpha_bv_raw_alpha_bv_vs_raw_alpha_bv_tvs_raw_alpha_bv_cvs_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_vs_raw

where "permute_bv_vs_raw p VsNil_raw = VsNil_raw"

|     "permute_bv_vs_raw p (VsCons_raw v t l) = VsCons_raw (p \<bullet> v) t (permute_bv_vs_raw p l)"

primrec permute_bv_cvs_raw

where "permute_bv_cvs_raw p CvsNil_raw = CvsNil_raw"

|     "permute_bv_cvs_raw p (CvsCons_raw v t l) = CvsCons_raw (p \<bullet> v) t (permute_bv_cvs_raw p l)"

primrec permute_bv_tvs_raw

where "permute_bv_tvs_raw p TvsNil_raw = TvsNil_raw"

|     "permute_bv_tvs_raw p (TvsCons_raw v t l) = TvsCons_raw (p \<bullet> v) t (permute_bv_tvs_raw p l)"

primrec permute_bv_raw

where "permute_bv_raw p (Kpat_raw c l1 l2 l3) =

     Kpat_raw c (permute_bv_tvs_raw p l1) (permute_bv_cvs_raw p l2) (permute_bv_vs_raw p l3)"

quotient_definition "permute_bv_vs :: perm \<Rightarrow> vars \<Rightarrow> vars"

is "permute_bv_vs_raw"

quotient_definition "permute_bv_cvs :: perm \<Rightarrow> cvars \<Rightarrow> cvars"

is "permute_bv_cvs_raw"

quotient_definition "permute_bv_tvs :: perm \<Rightarrow> tvars \<Rightarrow> tvars"

is "permute_bv_tvs_raw"

quotient_definition "permute_bv :: perm \<Rightarrow> pat \<Rightarrow> pat"

is "permute_bv_raw"

lemma rsp_pre:

 "alpha_tvars_raw d a \<Longrightarrow> alpha_tvars_raw (permute_bv_tvs_raw x d) (permute_bv_tvs_raw x a)"

 "alpha_cvars_raw e b \<Longrightarrow> alpha_cvars_raw (permute_bv_cvs_raw x e) (permute_bv_cvs_raw x b)"

 "alpha_vars_raw f c \<Longrightarrow> alpha_vars_raw (permute_bv_vs_raw x f) (permute_bv_vs_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_tvars_raw ===> alpha_tvars_raw) permute_bv_tvs_raw permute_bv_tvs_raw"

 "(op = ===> alpha_cvars_raw ===> alpha_cvars_raw) permute_bv_cvs_raw permute_bv_cvs_raw"

 "(op = ===> alpha_vars_raw ===> alpha_vars_raw) permute_bv_vs_raw permute_bv_vs_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

thm permute_bv_raw.simps[no_vars]

 permute_bv_vs_raw.simps[quot_lifted]

 permute_bv_cvs_raw.simps[quot_lifted]

 permute_bv_tvs_raw.simps[quot_lifted]

lemma permute_bv_pre:

  "permute_bv p (Kpat c l1 l2 l3) =

   Kpat c (permute_bv_tvs p l1) (permute_bv_cvs p l2) (permute_bv_vs p l3)"

  by (lifting permute_bv_raw.simps)

lemmas permute_bv[simp] =

 permute_bv_pre

 permute_bv_vs_raw.simps[quot_lifted]

 permute_bv_cvs_raw.simps[quot_lifted]

 permute_bv_tvs_raw.simps[quot_lifted]

lemma perm_bv1:

  "p \<bullet> bv_cvs b = bv_cvs (permute_bv_cvs p b)"

  "p \<bullet> bv_tvs c = bv_tvs (permute_bv_tvs p c)"

  "p \<bullet> bv_vs d = bv_vs (permute_bv_vs 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_tvs tvars (permute_bv_tvs q tvars)"

 "alpha_bv_cvs cvars (permute_bv_cvs q cvars)"

 "alpha_bv_vs vars (permute_bv_vs q vars)"

  apply(induct tvars rule: inducts(11))

  apply(simp_all add:permute_bv eqvts eq_iff)

  apply(induct cvars rule: inducts(12))

  apply(simp_all add:permute_bv eqvts eq_iff)

  apply(induct vars 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_lst (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_cvs 0 b = b"

  "permute_bv_tvs 0 c = c"

  "permute_bv_vs 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_tvs x \<sharp>* pa \<Longrightarrow> alpha_bv_tvs (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_cvs x \<sharp>* pa \<Longrightarrow> alpha_bv_cvs (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_vs x \<sharp>* pa \<Longrightarrow> alpha_bv_vs (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_tvs 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_cvs 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_vs 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 (set (bv_tvs 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 (set (bv_cvs 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 (set (bv_vs 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 (set (bv x))"

apply (induct x rule: inducts(9))

apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *})

apply (simp add: finb1 finb2 finb3)

done

thm tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.induct

lemma strong_induction_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>string b. P3 b (TC string)"

  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>string ty_lst b. \<lbrakk>\<And>c. P4 c ty_lst\<rbrakk> \<Longrightarrow> P3 b (TFun string 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>ck ty b. \<lbrakk>\<And>c. P2 c ck; \<And>c. P3 c ty\<rbrakk> \<Longrightarrow> P3 b (TEq ck ty)"

  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>string b. P5 b (CVar string)"

  and a12a:"\<And>str b. P5 b (CConst str)"

  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>string co_lst b. \<lbrakk>\<And>c. P6 c co_lst\<rbrakk> \<Longrightarrow> P5 b (CFun string 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>ck co b. \<lbrakk>\<And>c. P2 c ck; \<And>c. P5 c co\<rbrakk> \<Longrightarrow> P5 b (CEq ck co)"

  and a17: "\<And>ty b. \<lbrakk>\<And>c. P3 c ty\<rbrakk> \<Longrightarrow> P5 b (CRefl ty)"

  and a17a: "\<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 a18a:"\<And>co ty b. \<lbrakk>\<And>c. P5 c co; \<And>c. P3 c ty\<rbrakk> \<Longrightarrow> P5 b (CAt co ty)"

  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>co1 co2 b. \<lbrakk>\<And>c. P5 c co1; \<And>c. P5 c co2\<rbrakk> \<Longrightarrow> P5 b (CSim co1 co2)"

  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>string b. P7 b (K string)"

  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 (AppT trm ty)"

  and a31a:"\<And>trm co b. \<lbrakk>\<And>c. P7 c trm; \<And>c. P5 c co\<rbrakk> \<Longrightarrow> P7 b (AppC trm co)"

  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; set (bv (pat)) \<sharp>* b\<rbrakk>

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

  and a39: "\<And>string tvars cvars vars b. \<lbrakk>\<And>c. P11 c tvars; \<And>c. P12 c cvars; \<And>c. P10 c vars\<rbrakk>

    \<Longrightarrow> P9 b (Kpat string tvars cvars vars)"

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

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

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

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

    \<Longrightarrow> P11 b (TvsCons tvar tkind tvars)"

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

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

    \<Longrightarrow> P12 b (CvsCons tvar ckind cvars)"

  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) vars \<and>

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

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

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_vs q (p \<bullet> vars)))" and a3:"(\<forall>p q k. P11 k ( permute_bv_tvs q (p \<bullet> tvars)))" and a4:"(\<forall>p q l. P12 l (permute_bv_cvs q (p \<bullet> cvars)))"

    apply (induct rule: tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.inducts)

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