250 x \<notin> FV_ty B'; x \<notin> FV_trm M' - {x'}\<rbrakk> \<Longrightarrow> P3 (LAM A x M) (LAM A' x' M')" |
250 x \<notin> FV_ty B'; x \<notin> FV_trm M' - {x'}\<rbrakk> \<Longrightarrow> P3 (LAM A x M) (LAM A' x' M')" |
251 shows "((x1 :: KIND) = x2 \<longrightarrow> P1 x1 x2) \<and> |
251 shows "((x1 :: KIND) = x2 \<longrightarrow> P1 x1 x2) \<and> |
252 ((x3 ::TY) = x4 \<longrightarrow> P2 x3 x4) \<and> |
252 ((x3 ::TY) = x4 \<longrightarrow> P2 x3 x4) \<and> |
253 ((x5 :: TRM) = x6 \<longrightarrow> P3 x5 x6)" |
253 ((x5 :: TRM) = x6 \<longrightarrow> P3 x5 x6)" |
254 using a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 |
254 using a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 |
255 apply - |
255 apply(lifting akind_aty_atrm.induct) |
256 apply(tactic {* procedure_tac @{context} @{thm akind_aty_atrm.induct} 1 *}) |
256 (* FIXME: with overloaded definitions *) |
257 apply(tactic {* regularize_tac @{context} 1 *}) |
|
258 apply(tactic {* all_inj_repabs_tac @{context} 1 *}) |
|
259 apply(fold perm_kind_def perm_ty_def perm_trm_def) |
257 apply(fold perm_kind_def perm_ty_def perm_trm_def) |
260 apply(tactic {* clean_tac @{context} 1 *}) |
258 apply(cleaning) |
261 (* |
259 (* |
262 Profiling: |
260 Profiling: |
263 ML_prf {* fun ith i = (#concl (fst (Subgoal.focus @{context} i (#goal (Isar.goal ()))))) *} |
261 ML_prf {* fun ith i = (#concl (fst (Subgoal.focus @{context} i (#goal (Isar.goal ()))))) *} |
264 ML_prf {* profile 2 Seq.list_of ((clean_tac @{context} quot defs 1) (ith 3)) *} |
262 ML_prf {* profile 2 Seq.list_of ((clean_tac @{context} quot defs 1) (ith 3)) *} |
265 ML_prf {* profile 2 Seq.list_of ((regularize_tac @{context} @{thms alpha_equivps} 1) (ith 1)) *} |
263 ML_prf {* profile 2 Seq.list_of ((regularize_tac @{context} @{thms alpha_equivps} 1) (ith 1)) *} |
290 \<And>ty1 name ty2. \<lbrakk>Q ty1; Q ty2\<rbrakk> \<Longrightarrow> Q (TPI ty1 name ty2); |
288 \<And>ty1 name ty2. \<lbrakk>Q ty1; Q ty2\<rbrakk> \<Longrightarrow> Q (TPI ty1 name ty2); |
291 \<And>id. R (CONS id); \<And>name. R (VAR name); |
289 \<And>id. R (CONS id); \<And>name. R (VAR name); |
292 \<And>trm1 trm2. \<lbrakk>R trm1; R trm2\<rbrakk> \<Longrightarrow> R (APP trm1 trm2); |
290 \<And>trm1 trm2. \<lbrakk>R trm1; R trm2\<rbrakk> \<Longrightarrow> R (APP trm1 trm2); |
293 \<And>ty name trm. \<lbrakk>Q ty; R trm\<rbrakk> \<Longrightarrow> R (LAM ty name trm)\<rbrakk> |
291 \<And>ty name trm. \<lbrakk>Q ty; R trm\<rbrakk> \<Longrightarrow> R (LAM ty name trm)\<rbrakk> |
294 \<Longrightarrow> P mkind \<and> Q mty \<and> R mtrm" |
292 \<Longrightarrow> P mkind \<and> Q mty \<and> R mtrm" |
295 apply(tactic {* lift_tac @{context} @{thm kind_ty_trm.induct} 1 *}) |
293 apply(lifting kind_ty_trm.induct) |
296 done |
294 done |
297 |
295 |
298 end |
296 end |
299 |
297 |
300 |
298 |