# HG changeset patch # User Cezary Kaliszyk # Date 1272371444 -7200 # Node ID 4223770814ef8a8384dd55fd5fa5942c39ddbbfd # Parent e2e19188576ee38d6a48e9f1aa142cd1007e058b# Parent 47430fe78912e9229b59140a1f24474c2459a938 merge diff -r 47430fe78912 -r 4223770814ef Nominal/Ex/ExCoreHaskell.thy --- a/Nominal/Ex/ExCoreHaskell.thy Tue Apr 27 13:44:27 2010 +0200 +++ b/Nominal/Ex/ExCoreHaskell.thy Tue Apr 27 14:30:44 2010 +0200 @@ -93,6 +93,85 @@ | "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 \ rfv_tkind_raw tkind_raw2" +| "rfv_ckind_raw (CKEq_raw ty_raw1 ty_raw2) = rfv_ty_raw ty_raw1 \ 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 \ 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 \ (rfv_ty_raw ty_raw - {atom tvar})" +| "rfv_ty_raw (TEq_raw ckind_raw ty_raw) = rfv_ckind_raw ckind_raw \ 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 \ 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 \ 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 \ (rfv_co_raw co_raw - {atom cvar})" +| "rfv_co_raw (CEq_raw ckind_raw co_raw) = rfv_ckind_raw ckind_raw \ 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 \ rfv_co_raw co_raw2" +| "rfv_co_raw (CAt_raw co_raw ty_raw) = rfv_co_raw co_raw \ 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 \ 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 \ 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 \ 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 \ (rfv_trm_raw trm_raw - {atom tvar})" +| "rfv_trm_raw (LAMC_raw cvar ckind_raw trm_raw) = + rfv_ckind_raw ckind_raw \ (rfv_trm_raw trm_raw - {atom cvar})" +| "rfv_trm_raw (AppT_raw trm_raw ty_raw) = rfv_trm_raw trm_raw \ rfv_ty_raw ty_raw" +| "rfv_trm_raw (AppC_raw trm_raw co_raw) = rfv_trm_raw trm_raw \ rfv_co_raw co_raw" +| "rfv_trm_raw (Lam_raw var ty_raw trm_raw) = rfv_ty_raw ty_raw \ (rfv_trm_raw trm_raw - {atom var})" +| "rfv_trm_raw (App_raw trm_raw1 trm_raw2) = rfv_trm_raw trm_raw1 \ rfv_trm_raw trm_raw2" +| "rfv_trm_raw (Let_raw var ty_raw trm_raw1 trm_raw2) = + rfv_ty_raw ty_raw \ (rfv_trm_raw trm_raw1 \ (rfv_trm_raw trm_raw2 - {atom var}))" +| "rfv_trm_raw (Case_raw trm_raw assoc_lst_raw) = rfv_trm_raw trm_raw \ rfv_assoc_lst_raw assoc_lst_raw" +| "rfv_trm_raw (Cast_raw trm_raw ty_raw) = rfv_trm_raw trm_raw \ 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 \ (rfv_trm_raw trm_raw - set (bv_raw pat_raw) \ 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 \ (rfv_bv_cvs_raw cvars_raw \ 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 \ 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 \ 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 \ rfv_bv_cvs_raw cvars_raw" +| "rfv_pat_raw (Kpat_raw list tvars_raw cvars_raw vars_raw) = + rfv_tvars_raw tvars_raw \ (rfv_cvars_raw cvars_raw \ rfv_vars_raw vars_raw)" +| "rfv_vars_raw VsNil_raw = {}" +| "rfv_vars_raw (VsCons_raw var ty_raw vars_raw) = + {atom var} \ (rfv_ty_raw ty_raw \ rfv_vars_raw vars_raw)" +| "rfv_tvars_raw TvsNil_raw = {}" +| "rfv_tvars_raw (TvsCons_raw tvar tkind_raw tvars_raw) = + {atom tvar} \ (rfv_tkind_raw tkind_raw \ rfv_tvars_raw tvars_raw)" +| "rfv_cvars_raw CvsNil_raw = {}" +| "rfv_cvars_raw (CvsCons_raw cvar ckind_raw cvars_raw) = + {atom cvar} \ (rfv_ckind_raw ckind_raw \ 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]