490 apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *}) apply (rule refl) |
490 apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *}) apply (rule refl) |
491 apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *}) apply (rule refl) |
491 apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *}) apply (rule refl) |
492 apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *}) apply (rule refl) |
492 apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *}) apply (rule refl) |
493 done |
493 done |
494 |
494 |
|
495 (* Does not work: |
|
496 lemma |
|
497 assumes a0: "P1 TYP" |
|
498 and a1: "\<And>ty name kind. \<lbrakk>P2 ty; P1 kind\<rbrakk> \<Longrightarrow> P1 (KPI ty name kind)" |
|
499 and a2: "\<And>id. P2 (TCONST id)" |
|
500 and a3: "\<And>ty trm. \<lbrakk>P2 ty; P3 trm\<rbrakk> \<Longrightarrow> P2 (TAPP ty trm)" |
|
501 and a4: "\<And>ty1 name ty2. \<lbrakk>P2 ty1; P2 ty2\<rbrakk> \<Longrightarrow> P2 (TPI ty1 name ty2)" |
|
502 and a5: "\<And>id. P3 (CONS id)" |
|
503 and a6: "\<And>name. P3 (VAR name)" |
|
504 and a7: "\<And>trm1 trm2. \<lbrakk>P3 trm1; P3 trm2\<rbrakk> \<Longrightarrow> P3 (APP trm1 trm2)" |
|
505 and a8: "\<And>ty name trm. \<lbrakk>P2 ty; P3 trm\<rbrakk> \<Longrightarrow> P3 (LAM ty name trm)" |
|
506 shows "P1 mkind \<and> P2 mty \<and> P3 mtrm" |
|
507 using a0 a1 a2 a3 a4 a5 a6 a7 a8 |
|
508 *) |
|
509 |
495 lemma "\<lbrakk>P1 TYP; |
510 lemma "\<lbrakk>P1 TYP; |
496 \<And>ty name kind. \<lbrakk>P2 ty; P1 kind\<rbrakk> \<Longrightarrow> P1 (KPI ty name kind); |
511 \<And>ty name kind. \<lbrakk>P2 ty; P1 kind\<rbrakk> \<Longrightarrow> P1 (KPI ty name kind); |
497 \<And>id. P2 (TCONST id); |
512 \<And>id. P2 (TCONST id); |
498 \<And>ty trm. \<lbrakk>P2 ty; P3 trm\<rbrakk> \<Longrightarrow> P2 (TAPP ty trm); |
513 \<And>ty trm. \<lbrakk>P2 ty; P3 trm\<rbrakk> \<Longrightarrow> P2 (TAPP ty trm); |
499 \<And>ty1 name ty2. \<lbrakk>P2 ty1; P2 ty2\<rbrakk> \<Longrightarrow> P2 (TPI ty1 name ty2); |
514 \<And>ty1 name ty2. \<lbrakk>P2 ty1; P2 ty2\<rbrakk> \<Longrightarrow> P2 (TPI ty1 name ty2); |
500 \<And>id. P3 (CONS id); \<And>name. P3 (VAR name); |
515 \<And>id. P3 (CONS id); \<And>name. P3 (VAR name); |
501 \<And>trm1 trm2. \<lbrakk>P3 trm1; P3 trm2\<rbrakk> \<Longrightarrow> P3 (APP trm1 trm2); |
516 \<And>trm1 trm2. \<lbrakk>P3 trm1; P3 trm2\<rbrakk> \<Longrightarrow> P3 (APP trm1 trm2); |
502 \<And>ty name trm. \<lbrakk>P2 ty; P3 trm\<rbrakk> \<Longrightarrow> P3 (LAM ty name trm)\<rbrakk> |
517 \<And>ty name trm. \<lbrakk>P2 ty; P3 trm\<rbrakk> \<Longrightarrow> P3 (LAM ty name trm)\<rbrakk> |
503 \<Longrightarrow> P1 mkind \<and> P2 mty \<and> P3 mtrm" |
518 \<Longrightarrow> P1 mkind \<and> P2 mty \<and> P3 mtrm" |
|
519 |
504 apply (tactic {* (ObjectLogic.full_atomize_tac THEN' gen_frees_tac @{context}) 1 *}) |
520 apply (tactic {* (ObjectLogic.full_atomize_tac THEN' gen_frees_tac @{context}) 1 *}) |
505 ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *} |
521 ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *} |
506 ML_prf {* val aps = find_aps (prop_of (atomize_thm @{thm kind_ty_trm.induct})) (term_of qtm) *} |
522 ML_prf {* val aps = find_aps (prop_of (atomize_thm @{thm kind_ty_trm.induct})) (term_of qtm) *} |
507 apply(tactic {* procedure_tac @{context} @{thm kind_ty_trm.induct} 1 *}) |
523 apply(tactic {* procedure_tac @{context} @{thm kind_ty_trm.induct} 1 *}) |
508 apply(tactic {* regularize_tac @{context} @{thms alpha_EQUIVs} 1 *}) |
524 apply(tactic {* regularize_tac @{context} @{thms alpha_EQUIVs} 1 *}) |