theory CoreHaskell
imports "../Nominal2"
begin

(* Core Haskell *)

atom_decl var
atom_decl cvar
atom_decl tvar

nominal_datatype core_haskell: 
 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"

(* generated theorems *)

thm core_haskell.permute_bn
thm core_haskell.perm_bn_alpha
thm core_haskell.perm_bn_simps
thm core_haskell.bn_finite

thm core_haskell.distinct
thm core_haskell.induct
thm core_haskell.exhaust
thm core_haskell.fv_defs
thm core_haskell.bn_defs
thm core_haskell.perm_simps
thm core_haskell.eq_iff
thm core_haskell.fv_bn_eqvt
thm core_haskell.size_eqvt
thm core_haskell.supp

lemma strong_induction_principle:
  fixes c::"'a::fs"
  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 c tkind"
        "P2 c ckind"
        "P3 c ty"
        "P4 c ty_lst"
        "P5 c co"
        "P6 c co_lst"
        "P7 c trm"
        "P8 c assoc_lst"
        "P9 c pt"
        "P10 c vars"
        "P11 c tvars"
        "P12 c cvars"
oops

end