880 fun dest_fun_type (Type("fun", [T, S])) = (T, S) |
880 fun dest_fun_type (Type("fun", [T, S])) = (T, S) |
881 | dest_fun_type _ = error "dest_fun_type" |
881 | dest_fun_type _ = error "dest_fun_type" |
882 *} |
882 *} |
883 |
883 |
884 ML {* |
884 ML {* |
885 val rep_abs_rsp_tac = |
885 fun rep_abs_rsp_tac ctxt = |
886 Subgoal.FOCUS (fn {concl, context, ...} => |
886 SUBGOAL (fn (goal, i) => |
887 case HOLogic.dest_Trueprop (term_of concl) of (rel $ lhs $ (rep $ (abs $ rhs))) => |
887 case HOLogic.dest_Trueprop (Logic.strip_assums_concl goal) of (rel $ _ $ (rep $ (abs $ _))) => |
888 (let |
888 (let |
889 val thy = ProofContext.theory_of context; |
889 val thy = ProofContext.theory_of ctxt; |
890 val (ty_a, ty_b) = dest_fun_type (fastype_of abs); |
890 val (ty_a, ty_b) = dest_fun_type (fastype_of abs); |
891 val ty_inst = map (SOME o (ctyp_of thy)) [ty_a, ty_b]; |
891 val ty_inst = map (SOME o (ctyp_of thy)) [ty_a, ty_b]; |
892 val t_inst = map (SOME o (cterm_of thy)) [rel, abs, rep]; |
892 val t_inst = map (SOME o (cterm_of thy)) [rel, abs, rep]; |
893 val thm = Drule.instantiate' ty_inst t_inst @{thm rep_abs_rsp} |
893 val thm = Drule.instantiate' ty_inst t_inst @{thm rep_abs_rsp} |
894 val te = solve_quotient_assums context thm |
894 val te = solve_quotient_assums ctxt thm |
895 val t_inst = map (SOME o (cterm_of thy)) [lhs, rhs]; |
|
896 val thm = Drule.instantiate' [] t_inst te |
|
897 in |
895 in |
898 compose_tac (false, thm, 1) 1 |
896 rtac te i |
899 end |
897 end |
900 handle _ => no_tac) |
898 handle _ => no_tac) |
901 | _ => no_tac) |
899 | _ => no_tac) |
902 *} |
900 *} |
903 |
901 |