equal
deleted
inserted
replaced
1 theory CoreHaskell |
1 theory CoreHaskell |
2 imports "../NewParser" |
2 imports "../NewParser" |
3 begin |
3 begin |
4 |
4 |
5 (* core haskell *) |
5 (* Core Haskell *) |
6 |
|
7 (* at the moment it is hard coded that shallow binders |
|
8 need to use bind_set *) |
|
9 |
6 |
10 atom_decl var |
7 atom_decl var |
11 atom_decl cvar |
8 atom_decl cvar |
12 atom_decl tvar |
9 atom_decl tvar |
|
10 |
|
11 declare [[STEPS = 4]] |
13 |
12 |
14 nominal_datatype tkind = |
13 nominal_datatype tkind = |
15 KStar |
14 KStar |
16 | KFun "tkind" "tkind" |
15 | KFun "tkind" "tkind" |
17 and ckind = |
16 and ckind = |
83 | "bv_vs (VsCons v k t) = (atom v) # bv_vs t" |
82 | "bv_vs (VsCons v k t) = (atom v) # bv_vs t" |
84 | "bv_tvs TvsNil = []" |
83 | "bv_tvs TvsNil = []" |
85 | "bv_tvs (TvsCons v k t) = (atom v) # bv_tvs t" |
84 | "bv_tvs (TvsCons v k t) = (atom v) # bv_tvs t" |
86 | "bv_cvs CvsNil = []" |
85 | "bv_cvs CvsNil = []" |
87 | "bv_cvs (CvsCons v k t) = (atom v) # bv_cvs t" |
86 | "bv_cvs (CvsCons v k t) = (atom v) # bv_cvs t" |
|
87 |
|
88 |
88 |
89 |
89 lemmas fv_supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.supp(1-9,11,13,15) |
90 lemmas fv_supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.supp(1-9,11,13,15) |
90 lemmas supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.fv[simplified fv_supp] |
91 lemmas supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.fv[simplified fv_supp] |
91 lemmas perm=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.perm |
92 lemmas perm=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.perm |
92 lemmas eq_iff=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.eq_iff |
93 lemmas eq_iff=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.eq_iff |