397 shows "equivp R \<Longrightarrow> a = b \<longrightarrow> R a b" |
397 shows "equivp R \<Longrightarrow> a = b \<longrightarrow> R a b" |
398 by (simp add: equivp_reflp) |
398 by (simp add: equivp_reflp) |
399 |
399 |
400 ML {* |
400 ML {* |
401 fun quotient_tac ctxt = |
401 fun quotient_tac ctxt = |
402 REPEAT_ALL_NEW (FIRST' |
402 DETERM o REPEAT_ALL_NEW (FIRST' |
403 [rtac @{thm identity_quotient}, |
403 [rtac @{thm identity_quotient}, |
404 resolve_tac (quotient_rules_get ctxt)]) |
404 resolve_tac (quotient_rules_get ctxt)]) |
405 |
405 |
406 fun quotient_solver_tac ss = quotient_tac (Simplifier.the_context ss) |
406 fun quotient_solver_tac ss = quotient_tac (Simplifier.the_context ss) |
407 val quotient_solver = Simplifier.mk_solver' "Quotient goal solver" quotient_solver_tac |
407 val quotient_solver = Simplifier.mk_solver' "Quotient goal solver" quotient_solver_tac |
408 *} |
408 *} |
|
409 |
|
410 ML {* |
|
411 fun solve_quotient_assums ctxt thm = |
|
412 let |
|
413 val goal = hd (Drule.strip_imp_prems (cprop_of thm)) |
|
414 in |
|
415 thm OF [Goal.prove_internal [] goal (fn _ => quotient_tac ctxt 1)] |
|
416 end |
|
417 handle _ => error "solve_quotient_assums failed. Maybe a quotient_thm is missing" |
|
418 *} |
|
419 |
409 |
420 |
410 (* 0. preliminary simplification step according to *) |
421 (* 0. preliminary simplification step according to *) |
411 thm ball_reg_eqv bex_reg_eqv babs_reg_eqv (* the latter of no use *) |
422 thm ball_reg_eqv bex_reg_eqv babs_reg_eqv (* the latter of no use *) |
412 ball_reg_eqv_range bex_reg_eqv_range |
423 ball_reg_eqv_range bex_reg_eqv_range |
413 (* 1. eliminating simple Ball/Bex instances*) |
424 (* 1. eliminating simple Ball/Bex instances*) |
644 |
647 |
645 ML {* |
648 ML {* |
646 val bare_concl = HOLogic.dest_Trueprop o Logic.strip_assums_concl |
649 val bare_concl = HOLogic.dest_Trueprop o Logic.strip_assums_concl |
647 *} |
650 *} |
648 |
651 |
|
652 thm apply_rsp |
|
653 |
649 ML {* |
654 ML {* |
650 val apply_rsp_tac = |
655 val apply_rsp_tac = |
651 Subgoal.FOCUS (fn {concl, asms, context,...} => |
656 Subgoal.FOCUS (fn {concl, asms, context,...} => |
652 case ((HOLogic.dest_Trueprop (term_of concl))) of |
657 case ((HOLogic.dest_Trueprop (term_of concl))) of |
653 ((R2 $ (f $ x) $ (g $ y))) => |
658 (R2 $ (f $ x) $ (g $ y)) => |
654 (let |
659 (let |
655 val (asmf, asma) = find_qt_asm (map term_of asms); |
660 val (asmf, asma) = find_qt_asm (map term_of asms); |
656 in |
661 in |
657 if (fastype_of asmf) = (fastype_of f) then no_tac else let |
662 if (fastype_of asmf) = (fastype_of f) (* why is this test necessary *) |
658 val ty_a = fastype_of x; |
663 then no_tac |
659 val ty_b = fastype_of asma; |
664 else |
660 val ty_c = range_type (type_of f); |
665 let |
661 val thy = ProofContext.theory_of context; |
666 val ty_a = fastype_of x; |
662 val ty_inst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c]; |
667 val ty_b = fastype_of asma; |
663 val thm = Drule.instantiate' ty_inst [] @{thm apply_rsp} |
668 val ty_c = range_type (type_of f); (* why type_of, not fast_type? *) |
664 val te = solve_quotient_assums context thm |
669 val thy = ProofContext.theory_of context; |
665 val t_inst = map (SOME o (cterm_of thy)) [R2, f, g, x, y]; |
670 val ty_inst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c]; |
666 val thm = Drule.instantiate' [] t_inst te |
671 val thm = Drule.instantiate' ty_inst [] @{thm apply_rsp} |
667 in |
672 val te = solve_quotient_assums context thm |
668 compose_tac (false, thm, 2) 1 |
673 val t_inst = map (SOME o (cterm_of thy)) [R2, f, g, x, y]; |
669 end |
674 (* why not instantiate terms 3 lines earlier *) |
670 end |
675 val thm = Drule.instantiate' [] t_inst te |
|
676 in |
|
677 compose_tac (false, thm, 2) 1 |
|
678 end |
|
679 end |
671 handle ERROR "find_qt_asm: no pair" => no_tac) |
680 handle ERROR "find_qt_asm: no pair" => no_tac) |
672 | _ => no_tac) |
681 | _ => no_tac) |
673 *} |
682 *} |
674 |
683 |
675 ML {* |
684 ML {* |
676 fun equals_rsp_tac R ctxt = |
685 fun equals_rsp_tac R ctxt = |
677 let |
686 let |
678 val ty = domain_type (fastype_of R); |
687 val ty = domain_type (fastype_of R); |
679 val thy = ProofContext.theory_of ctxt |
688 val thy = ProofContext.theory_of ctxt |
680 val thm = Drule.instantiate' |
689 val thm = Drule.instantiate' |
681 [SOME (ctyp_of thy ty)] [SOME (cterm_of thy R)] @{thm equals_rsp} |
690 [SOME (ctyp_of thy ty)] [SOME (cterm_of thy R)] @{thm equals_rsp} |
682 in |
691 in |
683 rtac thm THEN' quotient_tac ctxt |
692 rtac thm THEN' quotient_tac ctxt |
684 end |
693 end |
685 handle THM _ => K no_tac |
694 handle THM _ => K no_tac |
686 | TYPE _ => K no_tac |
695 | TYPE _ => K no_tac |
687 | TERM _ => K no_tac |
696 | TERM _ => K no_tac |
688 *} |
697 *} |
689 |
698 |
690 ML {* |
699 thm rep_abs_rsp |
691 fun rep_abs_rsp_tac ctxt = |
700 |
|
701 ML {* |
|
702 fun rep_abs_rsp_tac ctxt = |
692 SUBGOAL (fn (goal, i) => |
703 SUBGOAL (fn (goal, i) => |
693 case (bare_concl goal) of |
704 case (bare_concl goal) of |
694 (rel $ _ $ (rep $ (abs $ _))) => |
705 (rel $ _ $ (rep $ (abs $ _))) => |
695 (let |
706 (let |
696 val thy = ProofContext.theory_of ctxt; |
707 val thy = ProofContext.theory_of ctxt; |
697 val (ty_a, ty_b) = dest_fun_type (fastype_of abs); |
708 val (ty_a, ty_b) = dest_fun_type (fastype_of abs); |
698 val ty_inst = map (SOME o (ctyp_of thy)) [ty_a, ty_b]; |
709 val ty_inst = map (SOME o (ctyp_of thy)) [ty_a, ty_b]; |
699 val t_inst = map (SOME o (cterm_of thy)) [rel, abs, rep]; |
710 val t_inst = map (SOME o (cterm_of thy)) [rel, abs, rep]; |
700 val thm = Drule.instantiate' ty_inst t_inst @{thm rep_abs_rsp} |
711 val thm = Drule.instantiate' ty_inst t_inst @{thm rep_abs_rsp} |
701 val te = solve_quotient_assums ctxt thm |
|
702 in |
712 in |
703 rtac te i |
713 (rtac thm THEN' quotient_tac ctxt) i |
704 end |
714 end |
705 handle _ => no_tac) |
715 handle _ => no_tac) (* what is the catch for ? *) |
706 | _ => no_tac) |
716 | _ => no_tac) |
707 *} |
717 *} |
708 |
718 |
709 ML {* |
719 ML {* |
710 fun inj_repabs_tac_match ctxt = SUBGOAL (fn (goal, i) => |
720 fun inj_repabs_tac_match ctxt = SUBGOAL (fn (goal, i) => |