equal
deleted
inserted
replaced
264 using a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 |
264 using a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 |
265 apply - |
265 apply - |
266 apply(tactic {* procedure_tac @{context} @{thm akind_aty_atrm.induct} 1 *}) |
266 apply(tactic {* procedure_tac @{context} @{thm akind_aty_atrm.induct} 1 *}) |
267 apply(tactic {* regularize_tac @{context} @{thms alpha_EQUIVs} 1 *}) |
267 apply(tactic {* regularize_tac @{context} @{thms alpha_EQUIVs} 1 *}) |
268 prefer 2 |
268 prefer 2 |
269 apply(tactic {* clean_tac @{context} quot defs 1 *}) |
269 apply(tactic {* simp_tac ((Simplifier.context @{context} empty_ss) addsimps @{thms perm_kind_def perm_ty_def perm_trm_def}) 1 *}) |
270 |
270 apply(tactic {* clean_tac @{context} quot 1 *}) |
271 (* |
271 (* |
272 Profiling: |
272 Profiling: |
273 ML_prf {* fun ith i = (#concl (fst (Subgoal.focus @{context} i (#goal (Isar.goal ()))))) *} |
273 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)) *} |
274 ML_prf {* profile 2 Seq.list_of ((clean_tac @{context} quot defs 1) (ith 3)) *} |
275 ML_prf {* profile 2 Seq.list_of ((regularize_tac @{context} @{thms alpha_EQUIVs} 1) (ith 1)) *} |
275 ML_prf {* profile 2 Seq.list_of ((regularize_tac @{context} @{thms alpha_EQUIVs} 1) (ith 1)) *} |
276 *) |
|
277 ML_prf {* PolyML.profiling 1 *} |
276 ML_prf {* PolyML.profiling 1 *} |
278 ML_prf {* profile 2 Seq.list_of ((all_inj_repabs_tac @{context} quot rel_refl trans2 1) (#goal (Isar.goal ()))) *} |
277 ML_prf {* profile 2 Seq.list_of ((all_inj_repabs_tac @{context} quot rel_refl trans2 1) (#goal (Isar.goal ()))) *} |
279 |
278 *) |
280 apply(tactic {* all_inj_repabs_tac @{context} quot rel_refl trans2 1 *}) |
279 apply(tactic {* all_inj_repabs_tac @{context} quot rel_refl trans2 1 *}) |
281 done |
280 done |
282 |
281 |
283 (* Does not work: |
282 (* Does not work: |
284 lemma |
283 lemma |
305 \<And>ty name trm. \<lbrakk>P2 ty; P3 trm\<rbrakk> \<Longrightarrow> P3 (LAM ty name trm)\<rbrakk> |
304 \<And>ty name trm. \<lbrakk>P2 ty; P3 trm\<rbrakk> \<Longrightarrow> P3 (LAM ty name trm)\<rbrakk> |
306 \<Longrightarrow> P1 mkind \<and> P2 mty \<and> P3 mtrm" |
305 \<Longrightarrow> P1 mkind \<and> P2 mty \<and> P3 mtrm" |
307 apply(tactic {* procedure_tac @{context} @{thm kind_ty_trm.induct} 1 *}) |
306 apply(tactic {* procedure_tac @{context} @{thm kind_ty_trm.induct} 1 *}) |
308 apply(tactic {* regularize_tac @{context} @{thms alpha_EQUIVs} 1 *}) |
307 apply(tactic {* regularize_tac @{context} @{thms alpha_EQUIVs} 1 *}) |
309 apply(tactic {* all_inj_repabs_tac @{context} quot rel_refl trans2 1 *}) |
308 apply(tactic {* all_inj_repabs_tac @{context} quot rel_refl trans2 1 *}) |
310 apply(tactic {* clean_tac @{context} quot defs 1 *}) |
309 apply(tactic {* clean_tac @{context} quot 1 *}) |
311 done |
310 done |
312 |
311 |
313 print_quotients |
312 print_quotients |
314 |
313 |
315 end |
314 end |