667 val apply_rsp_tac = |
667 val apply_rsp_tac = |
668 Subgoal.FOCUS (fn {concl, asms, context,...} => |
668 Subgoal.FOCUS (fn {concl, asms, context,...} => |
669 case (HOLogic.dest_Trueprop (term_of concl)) of |
669 case (HOLogic.dest_Trueprop (term_of concl)) of |
670 (R2 $ (f $ x) $ (g $ y)) => |
670 (R2 $ (f $ x) $ (g $ y)) => |
671 (let |
671 (let |
672 val (asmf, asma) = find_qt_asm (map term_of asms); |
672 val (asmf, asma) = find_qt_asm (map term_of asms) |
673 in |
673 in |
674 if (fastype_of asmf) = (fastype_of f) (* why is this test necessary *) |
674 if (fastype_of asmf) = (fastype_of f) |
675 then no_tac |
675 then no_tac |
676 else |
676 else |
677 let |
677 let |
678 val ty_a = fastype_of x |
678 val ty_a = fastype_of x |
679 val ty_b = fastype_of asma |
679 val ty_b = fastype_of asma |
680 val ty_c = range_type (type_of f) (* why type_of, not fast_type? *) |
680 val ty_c = range_type (fastype_of f) |
681 val thy = ProofContext.theory_of context |
681 val thy = ProofContext.theory_of context |
682 val ty_inst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c] |
682 val ty_inst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c] |
683 val t_inst = map (SOME o (cterm_of thy)) [R2, f, g, x, y]; |
683 val t_inst = map (SOME o (cterm_of thy)) [R2, f, g, x, y]; |
684 val thm' = Drule.instantiate' ty_inst [] @{thm apply_rsp} |
684 val thm = Drule.instantiate' ty_inst ([NONE, NONE, NONE] @ t_inst) @{thm apply_rsp} |
685 val te = solve_quotient_assums context thm' |
|
686 val thm = Drule.instantiate' [] t_inst te |
|
687 (* why not instantiate terms 3 lines earlier *) |
|
688 (* \<dots> if done one gets an instantiate type conlict error ??? *) |
|
689 (* why is necessary to get rid of the quot-assms first ??? *) |
|
690 in |
685 in |
691 compose_tac (false, thm, 2) 1 |
686 (rtac thm THEN' quotient_tac context) 1 |
692 end |
687 end |
693 end |
688 end |
694 handle ERROR "find_qt_asm: no pair" => no_tac) |
689 handle ERROR "find_qt_asm: no pair" => no_tac) |
695 | _ => no_tac) |
690 | _ => no_tac) |
696 *} |
691 *} |