91 | "bv_tvs TvsNil = []" |
91 | "bv_tvs TvsNil = []" |
92 | "bv_tvs (TvsCons v k t) = (atom v) # bv_tvs t" |
92 | "bv_tvs (TvsCons v k t) = (atom v) # bv_tvs t" |
93 | "bv_cvs CvsNil = []" |
93 | "bv_cvs CvsNil = []" |
94 | "bv_cvs (CvsCons v k t) = (atom v) # bv_cvs t" |
94 | "bv_cvs (CvsCons v k t) = (atom v) # bv_cvs t" |
95 |
95 |
|
96 (* |
|
97 function |
|
98 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 |
|
99 where |
|
100 "rfv_tkind_raw KStar_raw = {}" |
|
101 | "rfv_tkind_raw (KFun_raw tkind_raw1 tkind_raw2) = rfv_tkind_raw tkind_raw1 \<union> rfv_tkind_raw tkind_raw2" |
|
102 | "rfv_ckind_raw (CKEq_raw ty_raw1 ty_raw2) = rfv_ty_raw ty_raw1 \<union> rfv_ty_raw ty_raw2" |
|
103 | "rfv_ty_raw (TVar_raw tvar) = {atom tvar}" |
|
104 | "rfv_ty_raw (TC_raw list) = {}" |
|
105 | "rfv_ty_raw (TApp_raw ty_raw1 ty_raw2) = rfv_ty_raw ty_raw1 \<union> rfv_ty_raw ty_raw2" |
|
106 | "rfv_ty_raw (TFun_raw list ty_lst_raw) = rfv_ty_lst_raw ty_lst_raw" |
|
107 | "rfv_ty_raw (TAll_raw tvar tkind_raw ty_raw) = |
|
108 rfv_tkind_raw tkind_raw \<union> (rfv_ty_raw ty_raw - {atom tvar})" |
|
109 | "rfv_ty_raw (TEq_raw ckind_raw ty_raw) = rfv_ckind_raw ckind_raw \<union> rfv_ty_raw ty_raw" |
|
110 | "rfv_ty_lst_raw TsNil_raw = {}" |
|
111 | "rfv_ty_lst_raw (TsCons_raw ty_raw ty_lst_raw) = rfv_ty_raw ty_raw \<union> rfv_ty_lst_raw ty_lst_raw" |
|
112 | "rfv_co_raw (CVar_raw cvar) = {atom cvar}" |
|
113 | "rfv_co_raw (CConst_raw list) = {}" |
|
114 | "rfv_co_raw (CApp_raw co_raw1 co_raw2) = rfv_co_raw co_raw1 \<union> rfv_co_raw co_raw2" |
|
115 | "rfv_co_raw (CFun_raw list co_lst_raw) = rfv_co_lst_raw co_lst_raw" |
|
116 | "rfv_co_raw (CAll_raw cvar ckind_raw co_raw) = |
|
117 rfv_ckind_raw ckind_raw \<union> (rfv_co_raw co_raw - {atom cvar})" |
|
118 | "rfv_co_raw (CEq_raw ckind_raw co_raw) = rfv_ckind_raw ckind_raw \<union> rfv_co_raw co_raw" |
|
119 | "rfv_co_raw (CRefl_raw ty_raw) = rfv_ty_raw ty_raw" |
|
120 | "rfv_co_raw (CSym_raw co_raw) = rfv_co_raw co_raw" |
|
121 | "rfv_co_raw (CCir_raw co_raw1 co_raw2) = rfv_co_raw co_raw1 \<union> rfv_co_raw co_raw2" |
|
122 | "rfv_co_raw (CAt_raw co_raw ty_raw) = rfv_co_raw co_raw \<union> rfv_ty_raw ty_raw" |
|
123 | "rfv_co_raw (CLeft_raw co_raw) = rfv_co_raw co_raw" |
|
124 | "rfv_co_raw (CRight_raw co_raw) = rfv_co_raw co_raw" |
|
125 | "rfv_co_raw (CSim_raw co_raw1 co_raw2) = rfv_co_raw co_raw1 \<union> rfv_co_raw co_raw2" |
|
126 | "rfv_co_raw (CRightc_raw co_raw) = rfv_co_raw co_raw" |
|
127 | "rfv_co_raw (CLeftc_raw co_raw) = rfv_co_raw co_raw" |
|
128 | "rfv_co_raw (CCoe_raw co_raw1 co_raw2) = rfv_co_raw co_raw1 \<union> rfv_co_raw co_raw2" |
|
129 | "rfv_co_lst_raw CsNil_raw = {}" |
|
130 | "rfv_co_lst_raw (CsCons_raw co_raw co_lst_raw) = rfv_co_raw co_raw \<union> rfv_co_lst_raw co_lst_raw" |
|
131 | "rfv_trm_raw (Var_raw var) = {atom var}" |
|
132 | "rfv_trm_raw (K_raw list) = {}" |
|
133 | "rfv_trm_raw (LAMT_raw tvar tkind_raw trm_raw) = |
|
134 rfv_tkind_raw tkind_raw \<union> (rfv_trm_raw trm_raw - {atom tvar})" |
|
135 | "rfv_trm_raw (LAMC_raw cvar ckind_raw trm_raw) = |
|
136 rfv_ckind_raw ckind_raw \<union> (rfv_trm_raw trm_raw - {atom cvar})" |
|
137 | "rfv_trm_raw (AppT_raw trm_raw ty_raw) = rfv_trm_raw trm_raw \<union> rfv_ty_raw ty_raw" |
|
138 | "rfv_trm_raw (AppC_raw trm_raw co_raw) = rfv_trm_raw trm_raw \<union> rfv_co_raw co_raw" |
|
139 | "rfv_trm_raw (Lam_raw var ty_raw trm_raw) = rfv_ty_raw ty_raw \<union> (rfv_trm_raw trm_raw - {atom var})" |
|
140 | "rfv_trm_raw (App_raw trm_raw1 trm_raw2) = rfv_trm_raw trm_raw1 \<union> rfv_trm_raw trm_raw2" |
|
141 | "rfv_trm_raw (Let_raw var ty_raw trm_raw1 trm_raw2) = |
|
142 rfv_ty_raw ty_raw \<union> (rfv_trm_raw trm_raw1 \<union> (rfv_trm_raw trm_raw2 - {atom var}))" |
|
143 | "rfv_trm_raw (Case_raw trm_raw assoc_lst_raw) = rfv_trm_raw trm_raw \<union> rfv_assoc_lst_raw assoc_lst_raw" |
|
144 | "rfv_trm_raw (Cast_raw trm_raw ty_raw) = rfv_trm_raw trm_raw \<union> rfv_ty_raw ty_raw" |
|
145 | "rfv_assoc_lst_raw ANil_raw = {}" |
|
146 | "rfv_assoc_lst_raw (ACons_raw pat_raw trm_raw assoc_lst_raw) = |
|
147 rfv_bv_raw pat_raw \<union> (rfv_trm_raw trm_raw - set (bv_raw pat_raw) \<union> rfv_assoc_lst_raw assoc_lst_raw)" |
|
148 | "rfv_bv_raw (Kpat_raw list tvars_raw cvars_raw vars_raw) = |
|
149 rfv_bv_tvs_raw tvars_raw \<union> (rfv_bv_cvs_raw cvars_raw \<union> rfv_bv_vs_raw vars_raw)" |
|
150 | "rfv_bv_vs_raw VsNil_raw = {}" |
|
151 | "rfv_bv_vs_raw (VsCons_raw var ty_raw vars_raw) = rfv_ty_raw ty_raw \<union> rfv_bv_vs_raw vars_raw" |
|
152 | "rfv_bv_tvs_raw TvsNil_raw = {}" |
|
153 | "rfv_bv_tvs_raw (TvsCons_raw tvar tkind_raw tvars_raw) = |
|
154 rfv_tkind_raw tkind_raw \<union> rfv_bv_tvs_raw tvars_raw" |
|
155 | "rfv_bv_cvs_raw CvsNil_raw = {}" |
|
156 | "rfv_bv_cvs_raw (CvsCons_raw cvar ckind_raw cvars_raw) = |
|
157 rfv_ckind_raw ckind_raw \<union> rfv_bv_cvs_raw cvars_raw" |
|
158 | "rfv_pat_raw (Kpat_raw list tvars_raw cvars_raw vars_raw) = |
|
159 rfv_tvars_raw tvars_raw \<union> (rfv_cvars_raw cvars_raw \<union> rfv_vars_raw vars_raw)" |
|
160 | "rfv_vars_raw VsNil_raw = {}" |
|
161 | "rfv_vars_raw (VsCons_raw var ty_raw vars_raw) = |
|
162 {atom var} \<union> (rfv_ty_raw ty_raw \<union> rfv_vars_raw vars_raw)" |
|
163 | "rfv_tvars_raw TvsNil_raw = {}" |
|
164 | "rfv_tvars_raw (TvsCons_raw tvar tkind_raw tvars_raw) = |
|
165 {atom tvar} \<union> (rfv_tkind_raw tkind_raw \<union> rfv_tvars_raw tvars_raw)" |
|
166 | "rfv_cvars_raw CvsNil_raw = {}" |
|
167 | "rfv_cvars_raw (CvsCons_raw cvar ckind_raw cvars_raw) = |
|
168 {atom cvar} \<union> (rfv_ckind_raw ckind_raw \<union> rfv_cvars_raw cvars_raw)" |
|
169 apply pat_completeness |
|
170 apply auto |
|
171 done |
|
172 termination |
|
173 by lexicographic_order |
|
174 *) |
96 |
175 |
97 lemmas fv_supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.supp(1-9,11,13,15) |
176 lemmas fv_supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.supp(1-9,11,13,15) |
98 lemmas supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.fv[simplified fv_supp] |
177 lemmas supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.fv[simplified fv_supp] |
99 lemmas perm=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.perm |
178 lemmas perm=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.perm |
100 lemmas eq_iff=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.eq_iff |
179 lemmas eq_iff=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.eq_iff |