258 apply (tactic {* (ObjectLogic.full_atomize_tac THEN' gen_frees_tac @{context}) 1 *}) |
268 apply (tactic {* (ObjectLogic.full_atomize_tac THEN' gen_frees_tac @{context}) 1 *}) |
259 ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *} |
269 ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *} |
260 ML_prf {* val aps = find_aps (prop_of (atomize_thm @{thm akind_aty_atrm.induct})) (term_of qtm) *} |
270 ML_prf {* val aps = find_aps (prop_of (atomize_thm @{thm akind_aty_atrm.induct})) (term_of qtm) *} |
261 apply(tactic {* procedure_tac @{context} @{thm akind_aty_atrm.induct} 1 *}) |
271 apply(tactic {* procedure_tac @{context} @{thm akind_aty_atrm.induct} 1 *}) |
262 apply(tactic {* regularize_tac @{context} @{thms alpha_EQUIVs} 1 *}) |
272 apply(tactic {* regularize_tac @{context} @{thms alpha_EQUIVs} 1 *}) |
263 (* injecting *) |
|
264 ML_prf {* val quot = @{thms QUOTIENT_KIND QUOTIENT_TY QUOTIENT_TRM} *} |
|
265 ML_prf {* |
|
266 val rel_refl = map (fn x => @{thm EQUIV_REFL} OF [x]) @{thms alpha_EQUIVs} |
|
267 val trans2 = map (fn x => @{thm equiv_trans2} OF [x]) @{thms alpha_EQUIVs} |
|
268 *} |
|
269 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 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 ty} quot rel_refl trans2 1*}) |
276 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
273 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
277 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
455 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
459 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
456 apply(tactic {* all_inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
460 apply(tactic {* all_inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
457 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
461 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
458 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} 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 trm} quot rel_refl trans2 1*}) |
463 apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1*}) |
460 (* cleaning *) |
|
461 ML_prf {* val quot = @{thms QUOTIENT_KIND QUOTIENT_TY QUOTIENT_TRM} *} |
|
462 (*apply(tactic {* clean_tac @{context} quot defs aps 1 *}) *) |
464 (*apply(tactic {* clean_tac @{context} quot defs aps 1 *}) *) |
463 apply (tactic {* lambda_prs_tac @{context} quot 1 *}) |
465 apply (tactic {* lambda_prs_tac @{context} quot 1 *}) |
464 ML_prf {* val lower = flat (map (add_lower_defs @{context}) defs) *} |
|
465 ML_prf {* val meta_lower = map (fn x => @{thm eq_reflection} OF [x]) lower *} |
|
466 ML_prf {* val reps_same = map (fn x => @{thm QUOTIENT_REL_REP} OF [x]) quot *} |
|
467 ML_prf {* val meta_reps_same = map (fn x => @{thm eq_reflection} OF [x]) reps_same *} |
|
468 apply (tactic {* simp_tac ((Simplifier.context @{context} empty_ss) addsimps (meta_reps_same @ meta_lower)) 1 *}) |
466 apply (tactic {* simp_tac ((Simplifier.context @{context} empty_ss) addsimps (meta_reps_same @ meta_lower)) 1 *}) |
469 apply (tactic {* REPEAT_ALL_NEW (allex_prs_tac @{context} quot) 1 *}) |
467 apply (tactic {* REPEAT_ALL_NEW (allex_prs_tac @{context} quot) 1 *}) |
470 ML_prf {* val absrep = map (fn x => @{thm QUOTIENT_ABS_REP} OF [x]) quot *} |
468 ML_prf {* val absrep = map (fn x => @{thm QUOTIENT_ABS_REP} OF [x]) quot *} |
471 ML_prf {* val aps_thms = map (applic_prs @{context} absrep) aps *} |
469 ML_prf {* val aps_thms = map (applic_prs @{context} absrep) aps *} |
472 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) apply (rule refl) apply (rule ext) |
470 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) apply (rule refl) apply (rule ext) |
492 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) |
493 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) |
494 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) |
495 done |
493 done |
496 |
494 |
|
495 lemma "\<lbrakk>P1 TYP; |
|
496 \<And>ty name kind. \<lbrakk>P2 ty; P1 kind\<rbrakk> \<Longrightarrow> P1 (KPI ty name kind); |
|
497 \<And>id. P2 (TCONST id); |
|
498 \<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); |
|
500 \<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); |
|
502 \<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" |
|
504 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 ())))) *} |
|
506 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 *}) |
|
508 apply(tactic {* regularize_tac @{context} @{thms alpha_EQUIVs} 1 *}) |
|
509 prefer 2 |
|
510 apply(tactic {* clean_tac @{context} quot defs aps 1 *}) |
|
511 apply(tactic {* inj_repabs_tac @{context} @{typ kind } quot rel_refl trans2 1 *}) |
|
512 apply(tactic {* inj_repabs_tac @{context} @{typ kind } quot rel_refl trans2 1 *}) |
|
513 apply(tactic {* inj_repabs_tac @{context} @{typ kind } quot rel_refl trans2 1 *}) |
|
514 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *}) |
|
515 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *}) |
|
516 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *}) |
|
517 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *}) |
|
518 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *}) |
|
519 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *}) |
|
520 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *}) |
|
521 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *}) |
|
522 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *}) |
|
523 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *}) |
|
524 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *}) |
|
525 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *}) |
|
526 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *}) |
|
527 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *}) |
|
528 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *}) |
|
529 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *}) |
|
530 apply(tactic {* all_inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1 *}) |
|
531 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *}) |
|
532 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *}) |
|
533 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *}) |
|
534 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *}) |
|
535 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *}) |
|
536 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *}) |
|
537 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *}) |
|
538 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *}) |
|
539 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *}) |
|
540 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *}) |
|
541 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *}) |
|
542 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *}) |
|
543 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *}) |
|
544 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *}) |
|
545 apply(tactic {* all_inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1 *}) |
|
546 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *}) |
|
547 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *}) |
|
548 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *}) |
|
549 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *}) |
|
550 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *}) |
|
551 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *}) |
|
552 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *}) |
|
553 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *}) |
|
554 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *}) |
|
555 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *}) |
|
556 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *}) |
|
557 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *}) |
|
558 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *}) |
|
559 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *}) |
|
560 apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1 *}) |
|
561 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *}) |
|
562 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *}) |
|
563 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *}) |
|
564 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *}) |
|
565 apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1 *}) |
|
566 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *}) |
|
567 apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1 *}) |
|
568 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *}) |
|
569 apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1 *}) |
|
570 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *}) |
|
571 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *}) |
|
572 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *}) |
|
573 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *}) |
|
574 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *}) |
|
575 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 *}) |
|
577 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 *}) |
|
579 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *}) |
|
580 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *}) |
|
581 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *}) |
|
582 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *}) |
|
583 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *}) |
|
584 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 *}) |
|
586 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *}) |
|
587 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *}) |
|
588 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *}) |
|
589 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *}) |
|
590 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *}) |
|
591 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *}) |
|
592 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *}) |
|
593 (* LOOP! *) |
|
594 (* apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *}) *) |
|
595 apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1 *}) |
|
596 apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1 *}) |
|
597 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *}) |
|
598 apply(tactic {* all_inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1 *}) |
|
599 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *}) |
|
600 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *}) |
|
601 apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1 *}) |
|
602 done |
|
603 |
497 print_quotients |
604 print_quotients |
498 |
605 |
499 end |
606 end |
500 |
607 |
501 |
608 |