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 (* 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 |
|
510 lemma "\<lbrakk>P1 TYP; |
|
511 \<And>ty name kind. \<lbrakk>P2 ty; P1 kind\<rbrakk> \<Longrightarrow> P1 (KPI ty name kind); |
|
512 \<And>id. P2 (TCONST id); |
|
513 \<And>ty trm. \<lbrakk>P2 ty; P3 trm\<rbrakk> \<Longrightarrow> P2 (TAPP ty trm); |
|
514 \<And>ty1 name ty2. \<lbrakk>P2 ty1; P2 ty2\<rbrakk> \<Longrightarrow> P2 (TPI ty1 name ty2); |
|
515 \<And>id. P3 (CONS id); \<And>name. P3 (VAR name); |
|
516 \<And>trm1 trm2. \<lbrakk>P3 trm1; P3 trm2\<rbrakk> \<Longrightarrow> P3 (APP trm1 trm2); |
|
517 \<And>ty name trm. \<lbrakk>P2 ty; P3 trm\<rbrakk> \<Longrightarrow> P3 (LAM ty name trm)\<rbrakk> |
|
518 \<Longrightarrow> P1 mkind \<and> P2 mty \<and> P3 mtrm" |
|
519 |
|
520 apply (tactic {* (ObjectLogic.full_atomize_tac THEN' gen_frees_tac @{context}) 1 *}) |
|
521 ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *} |
|
522 ML_prf {* val aps = find_aps (prop_of (atomize_thm @{thm kind_ty_trm.induct})) (term_of qtm) *} |
|
523 apply(tactic {* procedure_tac @{context} @{thm kind_ty_trm.induct} 1 *}) |
|
524 apply(tactic {* regularize_tac @{context} @{thms alpha_EQUIVs} 1 *}) |
|
525 prefer 2 |
|
526 apply(tactic {* clean_tac @{context} quot defs aps 1 *}) |
|
527 apply(tactic {* inj_repabs_tac @{context} @{typ kind } quot rel_refl trans2 1 *}) |
|
528 apply(tactic {* inj_repabs_tac @{context} @{typ kind } quot rel_refl trans2 1 *}) |
|
529 apply(tactic {* inj_repabs_tac @{context} @{typ kind } quot rel_refl trans2 1 *}) |
|
530 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *}) |
|
531 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *}) |
|
532 apply(tactic {* inj_repabs_tac @{context} @{typ ty} 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 {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *}) |
|
545 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *}) |
|
546 apply(tactic {* all_inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1 *}) |
|
547 apply(tactic {* inj_repabs_tac @{context} @{typ nat} 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 {* inj_repabs_tac @{context} @{typ nat} 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 ty} quot rel_refl trans2 1 *}) |
|
561 apply(tactic {* all_inj_repabs_tac @{context} @{typ kind} 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 {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *}) |
|
566 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *}) |
|
567 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *}) |
|
568 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *}) |
|
569 apply(tactic {* inj_repabs_tac @{context} @{typ nat} 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 nat} quot rel_refl trans2 1 *}) |
|
572 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *}) |
|
573 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *}) |
|
574 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *}) |
|
575 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *}) |
|
576 apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1 *}) |
|
577 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *}) |
|
578 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *}) |
|
579 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *}) |
|
580 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *}) |
|
581 apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1 *}) |
|
582 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *}) |
|
583 apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1 *}) |
|
584 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *}) |
|
585 apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1 *}) |
|
586 apply(tactic {* inj_repabs_tac @{context} @{typ nat} 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 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *}) |
|
594 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *}) |
|
595 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *}) |
|
596 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *}) |
|
597 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *}) |
|
598 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *}) |
|
599 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *}) |
|
600 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *}) |
|
601 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *}) |
|
602 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *}) |
|
603 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *}) |
|
604 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *}) |
|
605 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *}) |
|
606 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *}) |
|
607 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *}) |
|
608 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *}) |
|
609 (* LOOP! *) |
|
610 (* apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *}) *) |
|
611 apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1 *}) |
|
612 apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1 *}) |
|
613 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *}) |
|
614 apply(tactic {* all_inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1 *}) |
|
615 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *}) |
|
616 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *}) |
|
617 apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1 *}) |
|
618 done |
|
619 |
497 print_quotients |
620 print_quotients |
498 |
621 |
499 end |
622 end |
500 |
623 |
501 |
624 |