664 thm apply_rsp |
664 thm apply_rsp |
665 |
665 |
666 ML {* |
666 ML {* |
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) (* why is this test necessary *) |
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 (type_of f) (* why type_of, not fast_type? *) |
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 thm = Drule.instantiate' ty_inst [] @{thm apply_rsp} |
683 val t_inst = map (SOME o (cterm_of thy)) [R2, f, g, x, y]; |
684 val te = solve_quotient_assums context thm |
684 val thm' = Drule.instantiate' ty_inst [] @{thm apply_rsp} |
685 val t_inst = map (SOME o (cterm_of thy)) [R2, f, g, x, y]; |
685 val te = solve_quotient_assums context thm' |
686 (* why not instantiate terms 3 lines earlier *) |
|
687 val thm = Drule.instantiate' [] t_inst te |
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 ??? *) |
688 in |
690 in |
689 compose_tac (false, thm, 2) 1 |
691 compose_tac (false, thm, 2) 1 |
690 end |
692 end |
691 end |
693 end |
692 handle ERROR "find_qt_asm: no pair" => no_tac) |
694 handle ERROR "find_qt_asm: no pair" => no_tac) |