equal
deleted
inserted
replaced
178 quotient_def |
178 quotient_def |
179 perm_trm :: "'x prm \<Rightarrow> TRM \<Rightarrow> TRM" |
179 perm_trm :: "'x prm \<Rightarrow> TRM \<Rightarrow> TRM" |
180 where |
180 where |
181 "perm_trm \<equiv> (perm::'x prm \<Rightarrow> trm \<Rightarrow> trm)" |
181 "perm_trm \<equiv> (perm::'x prm \<Rightarrow> trm \<Rightarrow> trm)" |
182 |
182 |
|
183 |
|
184 |
|
185 |
|
186 |
|
187 |
|
188 |
|
189 |
|
190 |
|
191 |
|
192 ML {* val defs = |
|
193 @{thms TYP_def KPI_def TCONST_def TAPP_def TPI_def VAR_def CONS_def APP_def LAM_def |
|
194 FV_kind_def FV_ty_def FV_trm_def perm_kind_def perm_ty_def perm_trm_def} |
|
195 *} |
|
196 ML {* val consts = lookup_quot_consts defs *} |
|
197 |
|
198 thm akind_aty_atrm.induct |
|
199 |
|
200 ML {* |
|
201 val rty_qty_rel = |
|
202 [(@{typ kind}, (@{typ KIND}, @{term akind})), |
|
203 (@{typ ty}, (@{typ TY}, @{term aty})), |
|
204 (@{typ trm}, (@{typ TRM}, @{term atrm}))] |
|
205 *} |
|
206 |
|
207 print_quotients |
|
208 |
|
209 ML {* val rty = [@{typ }] |
|
210 ML {* val defs_sym = flat (map (add_lower_defs @{context}) defs) *} |
|
211 ML {* val t_a = atomize_thm @{thm akind_aty_atrm.induct} *} |
|
212 prove {* build_regularize_goal t_a rty rel @{context} |
|
213 |
183 end |
214 end |
184 |
215 |
185 |
216 |
186 |
217 |