263 shows "((x1 :: KIND) = x2 \<longrightarrow> P1 x1 x2) \<and> |
263 shows "((x1 :: KIND) = x2 \<longrightarrow> P1 x1 x2) \<and> |
264 ((x3 ::TY) = x4 \<longrightarrow> P2 x3 x4) \<and> |
264 ((x3 ::TY) = x4 \<longrightarrow> P2 x3 x4) \<and> |
265 ((x5 :: TRM) = x6 \<longrightarrow> P3 x5 x6)" |
265 ((x5 :: TRM) = x6 \<longrightarrow> P3 x5 x6)" |
266 using a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 |
266 using a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 |
267 apply - |
267 apply - |
268 apply (tactic {* (ObjectLogic.full_atomize_tac THEN' gen_frees_tac @{context}) 1 *}) |
|
269 ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *} |
|
270 ML_prf {* val aps = find_aps (prop_of (atomize_thm @{thm akind_aty_atrm.induct})) (term_of qtm) *} |
|
271 apply(tactic {* procedure_tac @{context} @{thm akind_aty_atrm.induct} 1 *}) |
268 apply(tactic {* procedure_tac @{context} @{thm akind_aty_atrm.induct} 1 *}) |
272 apply(tactic {* regularize_tac @{context} @{thms alpha_EQUIVs} 1 *}) |
269 apply(tactic {* regularize_tac @{context} @{thms alpha_EQUIVs} 1 *}) |
273 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
270 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
274 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
271 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
275 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
272 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
459 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
456 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
460 apply(tactic {* all_inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
457 apply(tactic {* all_inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
461 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
458 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
462 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
459 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
463 apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1*}) |
460 apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1*}) |
464 apply(tactic {* clean_tac @{context} quot defs aps 1 *}) |
461 apply(tactic {* clean_tac @{context} quot defs 1 *}) |
465 done |
462 done |
466 |
463 |
467 (* Does not work: |
464 (* Does not work: |
468 lemma |
465 lemma |
469 assumes a0: "P1 TYP" |
466 assumes a0: "P1 TYP" |
486 \<And>ty1 name ty2. \<lbrakk>P2 ty1; P2 ty2\<rbrakk> \<Longrightarrow> P2 (TPI ty1 name ty2); |
483 \<And>ty1 name ty2. \<lbrakk>P2 ty1; P2 ty2\<rbrakk> \<Longrightarrow> P2 (TPI ty1 name ty2); |
487 \<And>id. P3 (CONS id); \<And>name. P3 (VAR name); |
484 \<And>id. P3 (CONS id); \<And>name. P3 (VAR name); |
488 \<And>trm1 trm2. \<lbrakk>P3 trm1; P3 trm2\<rbrakk> \<Longrightarrow> P3 (APP trm1 trm2); |
485 \<And>trm1 trm2. \<lbrakk>P3 trm1; P3 trm2\<rbrakk> \<Longrightarrow> P3 (APP trm1 trm2); |
489 \<And>ty name trm. \<lbrakk>P2 ty; P3 trm\<rbrakk> \<Longrightarrow> P3 (LAM ty name trm)\<rbrakk> |
486 \<And>ty name trm. \<lbrakk>P2 ty; P3 trm\<rbrakk> \<Longrightarrow> P3 (LAM ty name trm)\<rbrakk> |
490 \<Longrightarrow> P1 mkind \<and> P2 mty \<and> P3 mtrm" |
487 \<Longrightarrow> P1 mkind \<and> P2 mty \<and> P3 mtrm" |
491 |
|
492 apply (tactic {* (ObjectLogic.full_atomize_tac THEN' gen_frees_tac @{context}) 1 *}) |
|
493 ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *} |
|
494 ML_prf {* val aps = find_aps (prop_of (atomize_thm @{thm kind_ty_trm.induct})) (term_of qtm) *} |
|
495 apply(tactic {* procedure_tac @{context} @{thm kind_ty_trm.induct} 1 *}) |
488 apply(tactic {* procedure_tac @{context} @{thm kind_ty_trm.induct} 1 *}) |
496 apply(tactic {* regularize_tac @{context} @{thms alpha_EQUIVs} 1 *}) |
489 apply(tactic {* regularize_tac @{context} @{thms alpha_EQUIVs} 1 *}) |
497 prefer 2 |
|
498 apply(tactic {* clean_tac @{context} quot defs aps 1 *}) |
|
499 apply(tactic {* inj_repabs_tac @{context} @{typ kind } quot rel_refl trans2 1 *}) |
490 apply(tactic {* inj_repabs_tac @{context} @{typ kind } quot rel_refl trans2 1 *}) |
500 apply(tactic {* inj_repabs_tac @{context} @{typ kind } quot rel_refl trans2 1 *}) |
491 apply(tactic {* inj_repabs_tac @{context} @{typ kind } quot rel_refl trans2 1 *}) |
501 apply(tactic {* inj_repabs_tac @{context} @{typ kind } quot rel_refl trans2 1 *}) |
492 apply(tactic {* inj_repabs_tac @{context} @{typ kind } quot rel_refl trans2 1 *}) |
502 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *}) |
493 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *}) |
503 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *}) |
494 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *}) |
585 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *}) |
576 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *}) |
586 apply(tactic {* all_inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1 *}) |
577 apply(tactic {* all_inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1 *}) |
587 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *}) |
578 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *}) |
588 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *}) |
579 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *}) |
589 apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1 *}) |
580 apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1 *}) |
|
581 apply(tactic {* clean_tac @{context} quot defs 1 *}) |
590 done |
582 done |
591 |
583 |
592 print_quotients |
584 print_quotients |
593 |
585 |
594 end |
586 end |