equal
deleted
inserted
replaced
458 (* FIXME: OPTION_equivp, PAIR_equivp, ... *) |
458 (* FIXME: OPTION_equivp, PAIR_equivp, ... *) |
459 ML {* |
459 ML {* |
460 fun equiv_tac rel_eqvs = |
460 fun equiv_tac rel_eqvs = |
461 REPEAT_ALL_NEW (FIRST' |
461 REPEAT_ALL_NEW (FIRST' |
462 [resolve_tac rel_eqvs, |
462 [resolve_tac rel_eqvs, |
463 rtac @{thm IDENTITY_equivp}, |
463 rtac @{thm identity_equivp}, |
464 rtac @{thm list_equivp}]) |
464 rtac @{thm list_equivp}]) |
465 *} |
465 *} |
466 |
466 |
467 ML {* |
467 ML {* |
468 fun ball_reg_eqv_simproc rel_eqvs ss redex = |
468 fun ball_reg_eqv_simproc rel_eqvs ss redex = |
722 *} |
722 *} |
723 |
723 |
724 ML {* |
724 ML {* |
725 fun quotient_tac ctxt = |
725 fun quotient_tac ctxt = |
726 REPEAT_ALL_NEW (FIRST' |
726 REPEAT_ALL_NEW (FIRST' |
727 [rtac @{thm IDENTITY_Quotient}, |
727 [rtac @{thm identity_quotient}, |
728 resolve_tac (quotient_rules_get ctxt)]) |
728 resolve_tac (quotient_rules_get ctxt)]) |
729 *} |
729 *} |
730 |
730 |
731 lemma fun_rel_id: |
731 lemma fun_rel_id: |
732 assumes a: "\<And>x y. R1 x y \<Longrightarrow> R2 (f x) (g y)" |
732 assumes a: "\<And>x y. R1 x y \<Longrightarrow> R2 (f x) (g y)" |
893 (let |
893 (let |
894 val thy = ProofContext.theory_of context; |
894 val thy = ProofContext.theory_of context; |
895 val (ty_a, ty_b) = dest_fun_type (fastype_of abs); |
895 val (ty_a, ty_b) = dest_fun_type (fastype_of abs); |
896 val ty_inst = map (SOME o (ctyp_of thy)) [ty_a, ty_b]; |
896 val ty_inst = map (SOME o (ctyp_of thy)) [ty_a, ty_b]; |
897 val t_inst = map (SOME o (cterm_of thy)) [rel, abs, rep]; |
897 val t_inst = map (SOME o (cterm_of thy)) [rel, abs, rep]; |
898 val thm = Drule.instantiate' ty_inst t_inst @{thm REP_ABS_RSP} |
898 val thm = Drule.instantiate' ty_inst t_inst @{thm rep_abs_rsp} |
899 val te = solve_quotient_assums context thm |
899 val te = solve_quotient_assums context thm |
900 val t_inst = map (SOME o (cterm_of thy)) [lhs, rhs]; |
900 val t_inst = map (SOME o (cterm_of thy)) [lhs, rhs]; |
901 val thm = Drule.instantiate' [] t_inst te |
901 val thm = Drule.instantiate' [] t_inst te |
902 in |
902 in |
903 compose_tac (false, thm, 1) 1 |
903 compose_tac (false, thm, 1) 1 |