249 x \<notin> FV_ty B'; x \<notin> FV_trm M' - {x'}\<rbrakk> \<Longrightarrow> P3 (LAM A x M) (LAM A' x' M')" |
249 x \<notin> FV_ty B'; x \<notin> FV_trm M' - {x'}\<rbrakk> \<Longrightarrow> P3 (LAM A x M) (LAM A' x' M')" |
250 shows "((x1 :: KIND) = x2 \<longrightarrow> P1 x1 x2) \<and> |
250 shows "((x1 :: KIND) = x2 \<longrightarrow> P1 x1 x2) \<and> |
251 ((x3 ::TY) = x4 \<longrightarrow> P2 x3 x4) \<and> |
251 ((x3 ::TY) = x4 \<longrightarrow> P2 x3 x4) \<and> |
252 ((x5 :: TRM) = x6 \<longrightarrow> P3 x5 x6)" |
252 ((x5 :: TRM) = x6 \<longrightarrow> P3 x5 x6)" |
253 using a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 |
253 using a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 |
254 apply(lifting akind_aty_atrm.induct) |
254 apply(lifting_setup akind_aty_atrm.induct) |
255 (* |
255 defer |
256 Profiling: |
256 apply injection |
257 ML_prf {* fun ith i = (#concl (fst (Subgoal.focus @{context} i (#goal (Isar.goal ()))))) *} |
257 apply cleaning |
258 ML_prf {* profile 2 Seq.list_of ((clean_tac @{context} quot defs 1) (ith 3)) *} |
258 apply (simp only: ball_reg_eqv[OF KIND_equivp] ball_reg_eqv[OF TRM_equivp] ball_reg_eqv[OF TY_equivp]) |
259 ML_prf {* profile 2 Seq.list_of ((regularize_tac @{context} @{thms alpha_equivps} 1) (ith 1)) *} |
259 apply (rule ball_reg_right)+ |
260 ML_prf {* PolyML.profiling 1 *} |
260 apply (tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
261 ML_prf {* profile 2 Seq.list_of ((all_inj_repabs_tac @{context} quot rel_refl trans2 1) (#goal (Isar.goal ()))) *} |
261 apply (tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
262 *) |
262 apply (tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
263 done |
263 apply (tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
|
264 apply (tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
|
265 apply (tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
|
266 apply (tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
|
267 apply simp |
|
268 apply (tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
|
269 apply simp |
|
270 apply (tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
|
271 apply simp |
|
272 apply (tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
|
273 apply simp |
|
274 apply (tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
|
275 apply simp |
|
276 apply (tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
|
277 apply simp |
|
278 apply (tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
|
279 apply simp |
|
280 apply (tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
|
281 apply (tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
|
282 apply (tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
|
283 defer |
|
284 apply (tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
|
285 apply (tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
|
286 apply (tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
|
287 defer |
|
288 apply (tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
|
289 apply (tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
|
290 defer |
|
291 apply (tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
|
292 apply simp |
|
293 apply (tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
|
294 apply simp |
|
295 apply simp |
|
296 apply regularize+ |
|
297 done |
264 |
298 |
265 (* Does not work: |
299 (* Does not work: |
266 lemma |
300 lemma |
267 assumes a0: "P1 TYP" |
301 assumes a0: "P1 TYP" |
268 and a1: "\<And>ty name kind. \<lbrakk>P2 ty; P1 kind\<rbrakk> \<Longrightarrow> P1 (KPI ty name kind)" |
302 and a1: "\<And>ty name kind. \<lbrakk>P2 ty; P1 kind\<rbrakk> \<Longrightarrow> P1 (KPI ty name kind)" |