equal
deleted
inserted
replaced
262 |
262 |
263 fun equals_rsp_tac R ctxt = |
263 fun equals_rsp_tac R ctxt = |
264 let |
264 let |
265 val ty = domain_type (fastype_of R); |
265 val ty = domain_type (fastype_of R); |
266 val thy = ProofContext.theory_of ctxt |
266 val thy = ProofContext.theory_of ctxt |
267 in |
267 val thm = Drule.instantiate' |
268 case try (Drule.instantiate' [SOME (ctyp_of thy ty)] [SOME (cterm_of thy R)]) |
268 [SOME (ctyp_of thy ty)] [SOME (cterm_of thy R)] @{thm equals_rsp} |
269 @{thm equals_rsp} of |
269 in |
270 NONE => K no_tac |
270 rtac thm THEN' quotient_tac ctxt |
271 | SOME thm => rtac thm THEN' quotient_tac ctxt |
271 end |
272 end |
272 (* TODO: Are they raised by instantiate'? *) |
273 (* TODO: Again, can one specify more concretely *) |
273 (* TODO: Again, can one specify more concretely *) |
274 (* TODO: in terms of R when no_tac should be returned? *) |
274 (* TODO: in terms of R when no_tac should be returned? *) |
|
275 handle THM _ => K no_tac |
|
276 | TYPE _ => K no_tac |
|
277 | TERM _ => K no_tac |
275 |
278 |
276 fun rep_abs_rsp_tac ctxt = |
279 fun rep_abs_rsp_tac ctxt = |
277 SUBGOAL (fn (goal, i) => |
280 SUBGOAL (fn (goal, i) => |
278 case (bare_concl goal) of |
281 case (bare_concl goal) of |
279 (rel $ _ $ (rep $ (abs $ _))) => |
282 (rel $ _ $ (rep $ (abs $ _))) => |