256 shows "((x1 :: KIND) = x2 \<longrightarrow> P1 x1 x2) \<and> |
256 shows "((x1 :: KIND) = x2 \<longrightarrow> P1 x1 x2) \<and> |
257 ((x3 ::TY) = x4 \<longrightarrow> P2 x3 x4) \<and> |
257 ((x3 ::TY) = x4 \<longrightarrow> P2 x3 x4) \<and> |
258 ((x5 :: TRM) = x6 \<longrightarrow> P3 x5 x6)" |
258 ((x5 :: TRM) = x6 \<longrightarrow> P3 x5 x6)" |
259 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 |
260 apply - |
260 apply - |
261 apply(tactic {* procedure_tac @{context} @{thm akind_aty_atrm.induct} 1 *}) |
261 apply(tactic {* lift_tac @{context} @{thm akind_aty_atrm.induct} @{thms alpha_EQUIVs} 1 *}) |
262 apply(tactic {* regularize_tac @{context} @{thms alpha_EQUIVs} 1 *}) |
262 (*apply(tactic {* regularize_tac @{context} @{thms alpha_EQUIVs} 1 *}) |
263 prefer 2 |
263 apply(tactic {* all_inj_repabs_tac' @{context} rel_refl trans2 1 *}) |
264 apply(tactic {* clean_tac @{context} 1 *}) |
264 apply(tactic {* clean_tac @{context} 1 *}) |
|
265 *) |
|
266 (*apply(tactic {* all_inj_repabs_tac @{context} rel_refl trans2 1 *})*) |
265 (* |
267 (* |
266 Profiling: |
268 Profiling: |
267 ML_prf {* fun ith i = (#concl (fst (Subgoal.focus @{context} i (#goal (Isar.goal ()))))) *} |
269 ML_prf {* fun ith i = (#concl (fst (Subgoal.focus @{context} i (#goal (Isar.goal ()))))) *} |
268 ML_prf {* profile 2 Seq.list_of ((clean_tac @{context} quot defs 1) (ith 3)) *} |
270 ML_prf {* profile 2 Seq.list_of ((clean_tac @{context} quot defs 1) (ith 3)) *} |
269 ML_prf {* profile 2 Seq.list_of ((regularize_tac @{context} @{thms alpha_EQUIVs} 1) (ith 1)) *} |
271 ML_prf {* profile 2 Seq.list_of ((regularize_tac @{context} @{thms alpha_EQUIVs} 1) (ith 1)) *} |
270 ML_prf {* PolyML.profiling 1 *} |
272 ML_prf {* PolyML.profiling 1 *} |
271 ML_prf {* profile 2 Seq.list_of ((all_inj_repabs_tac @{context} quot rel_refl trans2 1) (#goal (Isar.goal ()))) *} |
273 ML_prf {* profile 2 Seq.list_of ((all_inj_repabs_tac @{context} quot rel_refl trans2 1) (#goal (Isar.goal ()))) *} |
272 *) |
274 *) |
273 apply(tactic {* all_inj_repabs_tac' @{context} rel_refl trans2 1 *}) |
|
274 (*apply(tactic {* all_inj_repabs_tac @{context} rel_refl trans2 1 *})*) |
|
275 done |
275 done |
276 |
276 |
277 (* Does not work: |
277 (* Does not work: |
278 lemma |
278 lemma |
279 assumes a0: "P1 TYP" |
279 assumes a0: "P1 TYP" |