--- a/Nominal/Ex/ExCoreHaskell.thy	Tue Apr 27 12:23:06 2010 +0200
+++ b/Nominal/Ex/ExCoreHaskell.thy	Tue Apr 27 14:29:59 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 \<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]