theory CoreHaskell

imports "../NewParser"

begin

(* Core Haskell *)

atom_decl var

atom_decl cvar

atom_decl tvar

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_set 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_set 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_set tv in t

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

| AppT "trm" "ty"

| AppC "trm" "co"

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

| App "trm" "trm"

| Let x::"var" "ty" "trm" t::"trm" bind_set 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"

lemma alpha_gen_sym_test:

  assumes a: "R (p \<bullet> x) y \<Longrightarrow> R y (p \<bullet> x)" 

  and     b: "p \<bullet> R = R"

  shows "(bs, x) \<approx>gen R f p (cs, y) \<Longrightarrow> (cs, y) \<approx>gen R f (- p) (bs, x)"

  and   "(bs, x) \<approx>res R f p (cs, y) \<Longrightarrow> (cs, y) \<approx>res R f (- p) (bs, x)"

  and   "(ds, x) \<approx>lst R f p (es, y) \<Longrightarrow> (es, y) \<approx>lst R f (- p) (ds, x)"

  unfolding alphas fresh_star_def

  apply(auto simp add:  fresh_minus_perm)

  apply(rule_tac p="p" in permute_boolE)

  apply(perm_simp add: permute_minus_cancel b)

  apply(simp add: a)

  apply(rule_tac p="p" in permute_boolE)

  apply(perm_simp add: permute_minus_cancel b)

  apply(simp add: a)

  apply(rule_tac p="p" in permute_boolE)

  apply(perm_simp add: permute_minus_cancel b)

  apply(simp add: a)

  done  

ML {*

(* for equalities *)

val tac1 = rtac @{thm sym} THEN' atac 

(* for "unbound" premises *)

val tac2 = atac

fun trans_prem_tac pred_names ctxt = 

  SUBPROOF (fn {prems, context as ctxt, ...} =>

    let

      val prems' = map (transform_prem1 ctxt pred_names) prems

      val _ = tracing ("prems'\n" ^ cat_lines (map (Syntax.string_of_term ctxt o prop_of) prems'))

    in

      print_tac "goal" THEN resolve_tac prems' 1

    end) ctxt

(* for "bound" premises *) 

fun tac3 pred_names ctxt = 

  EVERY' [etac @{thm exi_neg},

          resolve_tac @{thms alpha_gen_sym_test},

          asm_full_simp_tac (HOL_ss addsimps @{thms split_conv permute_prod.simps 

                prod_alpha_def prod_rel.simps alphas}),

          Nominal_Permeq.eqvt_tac ctxt [] [] THEN' rtac @{thm refl},

          trans_prem_tac pred_names ctxt] 

fun tac intro pred_names ctxt = 

  resolve_tac intro THEN_ALL_NEW FIRST' [tac1, tac2, tac3 pred_names ctxt]

*}

lemma [eqvt]:

shows "p \<bullet> alpha_tkind_raw = alpha_tkind_raw" 

and   "p \<bullet> alpha_ckind_raw = alpha_ckind_raw" 

and   "p \<bullet> alpha_ty_raw = alpha_ty_raw" 

and   "p \<bullet> alpha_ty_lst_raw = alpha_ty_lst_raw" 

and   "p \<bullet> alpha_co_raw = alpha_co_raw" 

and   "p \<bullet> alpha_co_lst_raw = alpha_co_lst_raw"

and   "p \<bullet> alpha_trm_raw = alpha_trm_raw"

and   "p \<bullet> alpha_assoc_lst_raw = alpha_assoc_lst_raw"

and   "p \<bullet> alpha_pat_raw = alpha_pat_raw"

and   "p \<bullet> alpha_vars_raw = alpha_vars_raw"

and   "p \<bullet> alpha_tvars_raw = alpha_tvars_raw"

and   "p \<bullet> alpha_cvars_raw = alpha_cvars_raw"

and   "p \<bullet> alpha_bv_raw = alpha_bv_raw"

and   "p \<bullet> alpha_bv_vs_raw = alpha_bv_vs_raw"

and   "p \<bullet> alpha_bv_tvs_raw = alpha_bv_tvs_raw"

and   "p \<bullet> alpha_bv_cvs_raw = alpha_bv_cvs_raw"

sorry

lemmas ii = 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 ij = 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

ML {*

val pp = ["CoreHaskel.alpha_tkind_raw", "CoreHaskell.alpha_ckind_raw", "CoreHaskell.alpha_ty_raw", "CoreHaskell.alpha_ty_lst_raw", "CoreHaskell.alpha_co_raw", "CoreHaskell.alpha_co_lst_raw", "CoreHaskell.alpha_trm_raw", "CoreHaskell.alpha_assoc_lst_raw", "CoreHaskell.alpha_pat_raw", "CoreHaskell.alpha_vars_raw", "CoreHaskell.alpha_tvars_raw", "CoreHaskell.alpha_cvars_raw", "CoreHaskell.alpha_bv_raw", "CoreHaskell.alpha_bv_vs_raw", "CoreHaskell.alpha_bv_tvs_raw", "CoreHaskell.alpha_bv_cvs_raw"]

*}

lemma

shows "alpha_tkind_raw x1 y1 ==> alpha_tkind_raw y1 x1" 

and   "alpha_ckind_raw x2 y2 ==> alpha_ckind_raw y2 x2" 

and   "alpha_ty_raw x3 y3 ==> alpha_ty_raw y3 x3" 

and   "alpha_ty_lst_raw x4 y4 ==> alpha_ty_lst_raw y4 x4" 

and   "alpha_co_raw x5 y5 ==> alpha_co_raw y5 x5" 

and   "alpha_co_lst_raw x6 y6 ==> alpha_co_lst_raw y6 x6"

and   "alpha_trm_raw x7 y7 ==> alpha_trm_raw y7 x7"

and   "alpha_assoc_lst_raw x8 y8 ==> alpha_assoc_lst_raw y8 x8"

and   "alpha_pat_raw x9 y9 ==> alpha_pat_raw y9 x9"

and   "alpha_vars_raw xa ya ==> alpha_vars_raw ya xa"

and   "alpha_tvars_raw xb yb ==> alpha_tvars_raw yb xb"

and   "alpha_cvars_raw xc yc ==> alpha_cvars_raw yc xc"

and   "alpha_bv_raw xd yd ==> alpha_bv_raw yd xd"

and   "alpha_bv_vs_raw xe ye ==> alpha_bv_vs_raw ye xe"

and   "alpha_bv_tvs_raw xf yf ==> alpha_bv_tvs_raw yf xf"

and   "alpha_bv_cvs_raw xg yg ==> alpha_bv_cvs_raw yg xg"

apply(induct rule: ii)

apply(tactic {* tac @{thms ij} pp @{context} 1 *})+

done

lemma

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

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 only: alpha_intros perm permute_bv_tvs_raw.simps permute_bv_cvs_raw.simps permute_bv_vs_raw.simps)

 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(simp_all add:permute_bv eqvts)

  apply(induct c rule: inducts(11))

  apply(simp_all add:permute_bv eqvts)

  apply(induct d rule: inducts(10))

  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(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 pt (permute_bv q pt)"

  apply(induct pt rule: inducts(9))

  apply(simp_all add:permute_bv eqvts eq_iff alpha_perm_bn1)

  done

lemma ACons_subst:

  "supp (Abs_lst (bv pt) trm) \<sharp>* q \<Longrightarrow> (ACons pt trm al) = ACons (permute_bv q pt) (q \<bullet> trm) al"

  apply (simp only: eq_iff)

  apply (simp add: alpha_perm_bn)

  apply (rule_tac x="q" in exI)

  apply (simp add: alphas)

  apply (simp add: perm_bv2[symmetric])

  apply (simp add: supp_abs)

  apply (simp add: fv_supp)

  apply (simp add: supp_eqvt[symmetric] set_eqvt[symmetric] Diff_eqvt[symmetric])

  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(simp_all add:permute_bv eqvts)

  apply(induct c rule: inducts(11))

  apply(simp_all add:permute_bv eqvts)

  apply(induct d rule: inducts(10))

  apply(simp_all add:permute_bv eqvts)

  done

lemma permute_bv_zero2:

  "permute_bv 0 a = a"

  apply(induct a rule: inducts(9))

  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 (simp_all add: eq_iff fresh_star_union)

  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 (rule 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 (rule TrueI)+

apply (simp_all add: fresh_star_union eq_iff)

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 (rule TrueI)+

apply (simp_all add: eq_iff fresh_star_union)

apply (simp add: fv_alpha1 fv_alpha2 fv_alpha3)

apply (subst supp_perm_eq)

apply (simp_all add: fv_supp)

done

lemma fin1: "finite (fv_bv_tvs x)"

apply (induct x rule: inducts(11))

apply (simp_all add: fv_supp finite_supp)

done

lemma fin2: "finite (fv_bv_cvs x)"

apply (induct x rule: inducts(12))

apply (simp_all add: fv_supp finite_supp)

done

lemma fin3: "finite (fv_bv_vs x)"

apply (induct x rule: inducts(10))

apply (simp_all add: fv_supp finite_supp)

done

lemma fin_fv_bv: "finite (fv_bv x)"

apply (induct x rule: inducts(9))

apply (rule TrueI)+

defer

apply (rule TrueI)+

apply (simp add: fin1 fin2 fin3)

apply (rule finite_supp)

done

lemma finb1: "finite (set (bv_tvs x))"

apply (induct x rule: inducts(11))

apply (simp_all add: fv_supp finite_supp)

done

lemma finb2: "finite (set (bv_cvs x))"

apply (induct x rule: inducts(12))

apply (simp_all add: fv_supp finite_supp)

done

lemma finb3: "finite (set (bv_vs x))"

apply (induct x rule: inducts(10))

apply (simp_all add: fv_supp finite_supp)

done

lemma fin_bv: "finite (set (bv x))"

apply (induct x rule: inducts(9))

apply (simp_all add: finb1 finb2 finb3)

done

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>pt trm assoc_lst b. \<lbrakk>\<And>c. P9 c pt; \<And>c. P7 c trm; \<And>c. P8 c assoc_lst; set (bv (pt)) \<sharp>* b\<rbrakk>

    \<Longrightarrow> P8 b (ACons pt 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) pt \<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> pt)))" 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) *})

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