equal
deleted
inserted
replaced
213 "(atrm ===> op =) fv_trm fv_trm" sorry |
213 "(atrm ===> op =) fv_trm fv_trm" sorry |
214 |
214 |
215 |
215 |
216 thm akind_aty_atrm.induct |
216 thm akind_aty_atrm.induct |
217 thm kind_ty_trm.induct |
217 thm kind_ty_trm.induct |
218 |
|
219 ML {* val defs = |
|
220 @{thms TYP_def KPI_def TCONST_def TAPP_def TPI_def VAR_def CONS_def APP_def LAM_def |
|
221 FV_kind_def FV_ty_def FV_trm_def perm_kind_def perm_ty_def perm_trm_def} |
|
222 *} |
|
223 |
218 |
224 ML {* |
219 ML {* |
225 val quot = @{thms QUOTIENT_KIND QUOTIENT_TY QUOTIENT_TRM} |
220 val quot = @{thms QUOTIENT_KIND QUOTIENT_TY QUOTIENT_TRM} |
226 val rel_refl = map (fn x => @{thm EQUIV_REFL} OF [x]) @{thms alpha_EQUIVs} |
221 val rel_refl = map (fn x => @{thm EQUIV_REFL} OF [x]) @{thms alpha_EQUIVs} |
227 val trans2 = map (fn x => @{thm equiv_trans2} OF [x]) @{thms alpha_EQUIVs} |
222 val trans2 = map (fn x => @{thm equiv_trans2} OF [x]) @{thms alpha_EQUIVs} |
264 using a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 |
259 using a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 |
265 apply - |
260 apply - |
266 apply(tactic {* procedure_tac @{context} @{thm akind_aty_atrm.induct} 1 *}) |
261 apply(tactic {* procedure_tac @{context} @{thm akind_aty_atrm.induct} 1 *}) |
267 apply(tactic {* regularize_tac @{context} @{thms alpha_EQUIVs} 1 *}) |
262 apply(tactic {* regularize_tac @{context} @{thms alpha_EQUIVs} 1 *}) |
268 prefer 2 |
263 prefer 2 |
269 apply(tactic {* simp_tac ((Simplifier.context @{context} empty_ss) addsimps @{thms perm_kind_def perm_ty_def perm_trm_def}) 1 *}) |
|
270 apply(tactic {* clean_tac @{context} quot 1 *}) |
264 apply(tactic {* clean_tac @{context} quot 1 *}) |
271 (* |
265 (* |
272 Profiling: |
266 Profiling: |
273 ML_prf {* fun ith i = (#concl (fst (Subgoal.focus @{context} i (#goal (Isar.goal ()))))) *} |
267 ML_prf {* fun ith i = (#concl (fst (Subgoal.focus @{context} i (#goal (Isar.goal ()))))) *} |
274 ML_prf {* profile 2 Seq.list_of ((clean_tac @{context} quot defs 1) (ith 3)) *} |
268 ML_prf {* profile 2 Seq.list_of ((clean_tac @{context} quot defs 1) (ith 3)) *} |