equal
deleted
inserted
replaced
262 ((x3 ::TY) = x4 \<longrightarrow> P2 x3 x4) \<and> |
262 ((x3 ::TY) = x4 \<longrightarrow> P2 x3 x4) \<and> |
263 ((x5 :: TRM) = x6 \<longrightarrow> P3 x5 x6)" |
263 ((x5 :: TRM) = x6 \<longrightarrow> P3 x5 x6)" |
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 *}) |
|
268 prefer 2 |
|
269 apply(tactic {* clean_tac @{context} quot defs 1 *}) |
|
270 |
267 (* |
271 (* |
268 Profiling: |
272 Profiling: |
269 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 ()))))) *} |
270 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)) *} |
271 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)) *} |
272 *) |
276 *) |
273 apply(tactic {* regularize_tac @{context} @{thms alpha_EQUIVs} 1 *}) |
277 ML_prf {* PolyML.profiling 1 *} |
274 prefer 2 |
278 ML_prf {* profile 2 Seq.list_of ((all_inj_repabs_tac @{context} quot rel_refl trans2 1) (#goal (Isar.goal ()))) *} |
275 apply(tactic {* clean_tac @{context} quot defs 1 *}) |
279 |
276 apply(tactic {* all_inj_repabs_tac @{context} quot rel_refl trans2 1*}) |
280 apply(tactic {* all_inj_repabs_tac @{context} quot rel_refl trans2 1 *}) |
277 done |
281 done |
278 |
282 |
279 (* Does not work: |
283 (* Does not work: |
280 lemma |
284 lemma |
281 assumes a0: "P1 TYP" |
285 assumes a0: "P1 TYP" |