503 ML {* |
503 ML {* |
504 fun regularize_tac ctxt rel_eqv rel_refl = |
504 fun regularize_tac ctxt rel_eqv rel_refl = |
505 (ObjectLogic.full_atomize_tac) THEN' |
505 (ObjectLogic.full_atomize_tac) THEN' |
506 REPEAT_ALL_NEW (FIRST' |
506 REPEAT_ALL_NEW (FIRST' |
507 [(K (print_tac "start")) THEN' (K no_tac), |
507 [(K (print_tac "start")) THEN' (K no_tac), |
508 DT ctxt "1" (FIRST' (map rtac rel_refl)), |
508 DT ctxt "1" (resolve_tac rel_refl), |
509 DT ctxt "2" atac, |
509 DT ctxt "2" atac, |
510 DT ctxt "3" (rtac @{thm universal_twice}), |
510 DT ctxt "3" (rtac @{thm universal_twice}), |
511 DT ctxt "4" (rtac @{thm impI} THEN' atac), |
511 DT ctxt "4" (rtac @{thm impI} THEN' atac), |
512 DT ctxt "5" (rtac @{thm implication_twice}), |
512 DT ctxt "5" (rtac @{thm implication_twice}), |
513 DT ctxt "6" (EqSubst.eqsubst_tac ctxt [0] |
513 DT ctxt "6" (EqSubst.eqsubst_tac ctxt [0] |
514 [(@{thm equiv_res_forall} OF [rel_eqv]), |
514 [(@{thm equiv_res_forall} OF [rel_eqv]), |
515 (@{thm equiv_res_exists} OF [rel_eqv])]), |
515 (@{thm equiv_res_exists} OF [rel_eqv])]), |
516 (* For a = b \<longrightarrow> a \<approx> b *) |
516 (* For a = b \<longrightarrow> a \<approx> b *) |
517 DT ctxt "7" (rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' (FIRST' (map rtac rel_refl))), |
517 DT ctxt "7" (rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' (resolve_tac rel_refl)), |
518 DT ctxt "8" (rtac @{thm RIGHT_RES_FORALL_REGULAR}) |
518 DT ctxt "8" (rtac @{thm RIGHT_RES_FORALL_REGULAR}) |
519 ]); |
519 ]); |
520 *} |
520 *} |
521 |
521 |
522 lemma move_forall: |
522 lemma move_forall: |
570 done |
570 done |
571 |
571 |
572 (* FIXME: OPTION_EQUIV, PAIR_EQUIV, ... *) |
572 (* FIXME: OPTION_EQUIV, PAIR_EQUIV, ... *) |
573 ML {* |
573 ML {* |
574 fun equiv_tac rel_eqvs = |
574 fun equiv_tac rel_eqvs = |
575 REPEAT_ALL_NEW(FIRST' [ |
575 REPEAT_ALL_NEW (FIRST' |
576 FIRST' (map rtac rel_eqvs), |
576 [resolve_tac rel_eqvs, |
577 rtac @{thm IDENTITY_EQUIV}, |
577 rtac @{thm IDENTITY_EQUIV}, |
578 rtac @{thm LIST_EQUIV} |
578 rtac @{thm LIST_EQUIV}]) |
579 ]) |
|
580 *} |
579 *} |
581 |
580 |
582 ML {* |
581 ML {* |
583 fun SOLVES' tac = tac THEN_ALL_NEW (fn _ => no_tac) |
582 fun SOLVES' tac = tac THEN_ALL_NEW (fn _ => no_tac) |
584 *} |
583 *} |
591 val subs = map (fn x => @{thm eq_reflection} OF [x]) (subs1 @ subs2) |
590 val subs = map (fn x => @{thm eq_reflection} OF [x]) (subs1 @ subs2) |
592 in |
591 in |
593 (ObjectLogic.full_atomize_tac) THEN' |
592 (ObjectLogic.full_atomize_tac) THEN' |
594 (simp_tac ((Simplifier.context ctxt empty_ss) addsimps subs)) |
593 (simp_tac ((Simplifier.context ctxt empty_ss) addsimps subs)) |
595 THEN' |
594 THEN' |
596 REPEAT_ALL_NEW (FIRST' [ |
595 REPEAT_ALL_NEW (FIRST' |
597 (rtac @{thm RIGHT_RES_FORALL_REGULAR}), |
596 [(rtac @{thm RIGHT_RES_FORALL_REGULAR}), |
598 (rtac @{thm LEFT_RES_EXISTS_REGULAR}), |
597 (rtac @{thm LEFT_RES_EXISTS_REGULAR}), |
599 (resolve_tac (Inductive.get_monos ctxt)), |
598 (resolve_tac (Inductive.get_monos ctxt)), |
600 (rtac @{thm ball_respects_refl} THEN' (RANGE [SOLVES' (equiv_tac rel_eqvs)])), |
599 (rtac @{thm ball_respects_refl} THEN' (RANGE [SOLVES' (equiv_tac rel_eqvs)])), |
601 (rtac @{thm bex_respects_refl} THEN' (RANGE [SOLVES' (equiv_tac rel_eqvs)])), |
600 (rtac @{thm bex_respects_refl} THEN' (RANGE [SOLVES' (equiv_tac rel_eqvs)])), |
602 rtac @{thm move_forall}, |
601 rtac @{thm move_forall}, |
603 rtac @{thm move_exists}, |
602 rtac @{thm move_exists}, |
604 (rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' FIRST' (map rtac rel_refl)) |
603 (rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' (resolve_tac rel_refl))]) |
605 ]) |
|
606 end |
604 end |
607 *} |
605 *} |
608 |
606 |
609 section {* Injections of REP and ABSes *} |
607 section {* Injections of REP and ABSes *} |
610 |
608 |
730 *} |
728 *} |
731 |
729 |
732 |
730 |
733 ML {* |
731 ML {* |
734 fun quotient_tac quot_thms = |
732 fun quotient_tac quot_thms = |
735 REPEAT_ALL_NEW (FIRST' [ |
733 REPEAT_ALL_NEW (FIRST' |
736 rtac @{thm FUN_QUOTIENT}, |
734 [rtac @{thm FUN_QUOTIENT}, |
737 FIRST' (map rtac quot_thms), |
735 resolve_tac quot_thms, |
738 rtac @{thm IDENTITY_QUOTIENT}, |
736 rtac @{thm IDENTITY_QUOTIENT}, |
739 (* For functional identity quotients, (op = ---> op =) *) |
737 (* For functional identity quotients, (op = ---> op =) *) |
740 (* TODO: think about the other way around, if we need to shorten the relation *) |
738 (* TODO: think about the other way around, if we need to shorten the relation *) |
741 CHANGED o (simp_tac (HOL_ss addsimps @{thms id_simps})) |
739 CHANGED o (simp_tac (HOL_ss addsimps @{thms id_simps}))]) |
742 ]) |
|
743 *} |
740 *} |
744 |
741 |
745 ML {* |
742 ML {* |
746 fun LAMBDA_RES_TAC ctxt i st = |
743 fun LAMBDA_RES_TAC ctxt i st = |
747 (case (term_of o #concl o fst) (Subgoal.focus ctxt i st) of |
744 (case (term_of o #concl o fst) (Subgoal.focus ctxt i st) of |
815 *} |
812 *} |
816 |
813 |
817 ML {* |
814 ML {* |
818 fun r_mk_comb_tac ctxt rty quot_thms rel_refl trans2 rsp_thms = |
815 fun r_mk_comb_tac ctxt rty quot_thms rel_refl trans2 rsp_thms = |
819 (FIRST' [ |
816 (FIRST' [ |
820 FIRST' (map rtac trans2), |
817 resolve_tac trans2, |
821 LAMBDA_RES_TAC ctxt, |
818 LAMBDA_RES_TAC ctxt, |
822 rtac @{thm RES_FORALL_RSP}, |
819 rtac @{thm RES_FORALL_RSP}, |
823 ball_rsp_tac ctxt, |
820 ball_rsp_tac ctxt, |
824 rtac @{thm RES_EXISTS_RSP}, |
821 rtac @{thm RES_EXISTS_RSP}, |
825 bex_rsp_tac ctxt, |
822 bex_rsp_tac ctxt, |
826 FIRST' (map rtac rsp_thms), |
823 resolve_tac rsp_thms, |
827 rtac refl, |
824 rtac @{thm refl}, |
828 (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' |
825 (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' |
829 (RANGE [SOLVES' (quotient_tac quot_thms)])), |
826 (RANGE [SOLVES' (quotient_tac quot_thms)])), |
830 (APPLY_RSP_TAC rty ctxt THEN' |
827 (APPLY_RSP_TAC rty ctxt THEN' |
831 (RANGE [SOLVES' (quotient_tac quot_thms), SOLVES' (quotient_tac quot_thms)])), |
828 (RANGE [SOLVES' (quotient_tac quot_thms), SOLVES' (quotient_tac quot_thms)])), |
832 Cong_Tac.cong_tac @{thm cong}, |
829 Cong_Tac.cong_tac @{thm cong}, |
833 rtac @{thm ext}, |
830 rtac @{thm ext}, |
834 FIRST' (map rtac rel_refl), |
831 resolve_tac rel_refl, |
835 atac, |
832 atac, |
836 SOLVES' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps})), |
833 SOLVES' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps})), |
837 WEAK_LAMBDA_RES_TAC ctxt, |
834 WEAK_LAMBDA_RES_TAC ctxt, |
838 CHANGED o (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ})) |
835 CHANGED o (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ})) |
839 ]) |
836 ]) |
861 14) simplifying (= ===> =) for simpler respectfulness |
858 14) simplifying (= ===> =) for simpler respectfulness |
862 |
859 |
863 *) |
860 *) |
864 |
861 |
865 ML {* |
862 ML {* |
866 fun r_mk_comb_tac' ctxt rty quot_thms reflex_thm trans_thm rsp_thms = |
863 fun r_mk_comb_tac' ctxt rty quot_thms rel_refl trans2 rsp_thms = |
867 REPEAT_ALL_NEW (FIRST' [ |
864 REPEAT_ALL_NEW (FIRST' [ |
868 (K (print_tac "start")) THEN' (K no_tac), |
865 (K (print_tac "start")) THEN' (K no_tac), |
869 DT ctxt "1" (rtac trans_thm), |
866 DT ctxt "1" (resolve_tac trans2), |
870 DT ctxt "2" (LAMBDA_RES_TAC ctxt), |
867 DT ctxt "2" (LAMBDA_RES_TAC ctxt), |
871 DT ctxt "3" (rtac @{thm RES_FORALL_RSP}), |
868 DT ctxt "3" (rtac @{thm RES_FORALL_RSP}), |
872 DT ctxt "4" (ball_rsp_tac ctxt), |
869 DT ctxt "4" (ball_rsp_tac ctxt), |
873 DT ctxt "5" (rtac @{thm RES_EXISTS_RSP}), |
870 DT ctxt "5" (rtac @{thm RES_EXISTS_RSP}), |
874 DT ctxt "6" (bex_rsp_tac ctxt), |
871 DT ctxt "6" (bex_rsp_tac ctxt), |
875 DT ctxt "7" (FIRST' (map rtac rsp_thms)), |
872 DT ctxt "7" (resolve_tac rsp_thms), |
876 DT ctxt "8" (rtac refl), |
873 DT ctxt "8" (rtac @{thm refl}), |
877 DT ctxt "9" ((instantiate_tac @{thm REP_ABS_RSP(1)} ctxt |
874 DT ctxt "9" ((instantiate_tac @{thm REP_ABS_RSP(1)} ctxt |
878 THEN' (RANGE [SOLVES' (quotient_tac quot_thms)]))), |
875 THEN' (RANGE [SOLVES' (quotient_tac quot_thms)]))), |
879 DT ctxt "A" ((APPLY_RSP_TAC rty ctxt THEN' |
876 DT ctxt "A" ((APPLY_RSP_TAC rty ctxt THEN' |
880 (RANGE [SOLVES' (quotient_tac quot_thms), SOLVES' (quotient_tac quot_thms)]))), |
877 (RANGE [SOLVES' (quotient_tac quot_thms), SOLVES' (quotient_tac quot_thms)]))), |
881 DT ctxt "B" (Cong_Tac.cong_tac @{thm cong}), |
878 DT ctxt "B" (Cong_Tac.cong_tac @{thm cong}), |
882 DT ctxt "C" (rtac @{thm ext}), |
879 DT ctxt "C" (rtac @{thm ext}), |
883 DT ctxt "D" (rtac reflex_thm), |
880 DT ctxt "D" (resolve_tac rel_refl), |
884 DT ctxt "E" (atac), |
881 DT ctxt "E" (atac), |
885 DT ctxt "F" (SOLVES' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))), |
882 DT ctxt "F" (SOLVES' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))), |
886 DT ctxt "G" (WEAK_LAMBDA_RES_TAC ctxt), |
883 DT ctxt "G" (WEAK_LAMBDA_RES_TAC ctxt), |
887 DT ctxt "H" (CHANGED o (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ}))) |
884 DT ctxt "H" (CHANGED o (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ}))) |
888 ]) |
885 ]) |
936 *} |
933 *} |
937 |
934 |
938 ML {* |
935 ML {* |
939 fun allex_prs_tac lthy quot = |
936 fun allex_prs_tac lthy quot = |
940 (EqSubst.eqsubst_tac lthy [0] @{thms FORALL_PRS[symmetric] EXISTS_PRS[symmetric]}) |
937 (EqSubst.eqsubst_tac lthy [0] @{thms FORALL_PRS[symmetric] EXISTS_PRS[symmetric]}) |
941 THEN' (quotient_tac quot); |
938 THEN' (quotient_tac quot) |
942 *} |
939 *} |
943 |
940 |
944 ML {* |
941 ML {* |
945 fun prep_trm thy (x, (T, t)) = |
942 fun prep_trm thy (x, (T, t)) = |
946 (cterm_of thy (Var (x, T)), cterm_of thy t) |
943 (cterm_of thy (Var (x, T)), cterm_of thy t) |