258 (rtac inst_thm THEN' quotient_tac context) 1 |
258 (rtac inst_thm THEN' quotient_tac context) 1 |
259 end |
259 end |
260 | _ => no_tac |
260 | _ => no_tac |
261 end) |
261 end) |
262 |
262 |
|
263 (* Instantiates and applies 'equals_rsp'. Since the theorem is |
|
264 complex we rely on instantiation to tell us if it applies *) |
263 fun equals_rsp_tac R ctxt = |
265 fun equals_rsp_tac R ctxt = |
264 let |
266 let |
265 val ty = domain_type (fastype_of R); |
|
266 val thy = ProofContext.theory_of ctxt |
267 val thy = ProofContext.theory_of ctxt |
267 val thm = Drule.instantiate' |
268 in |
268 [SOME (ctyp_of thy ty)] [SOME (cterm_of thy R)] @{thm equals_rsp} |
269 case try (cterm_of thy) R of (* There can be loose bounds in R *) |
269 in |
270 SOME ctm => |
270 rtac thm THEN' quotient_tac ctxt |
271 let |
271 end |
272 val ty = domain_type (fastype_of R) |
272 (* TODO: Are they raised by instantiate'? *) |
273 in |
|
274 case try (Drule.instantiate' [SOME (ctyp_of thy ty)] |
|
275 [SOME (cterm_of thy R)]) @{thm equals_rsp} of |
|
276 SOME thm => rtac thm THEN' quotient_tac ctxt |
|
277 | NONE => K no_tac |
|
278 end |
|
279 | _ => K no_tac |
|
280 end |
273 (* TODO: Again, can one specify more concretely *) |
281 (* TODO: Again, can one specify more concretely *) |
274 (* TODO: in terms of R when no_tac should be returned? *) |
282 (* 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 |
|
278 |
283 |
279 fun rep_abs_rsp_tac ctxt = |
284 fun rep_abs_rsp_tac ctxt = |
280 SUBGOAL (fn (goal, i) => |
285 SUBGOAL (fn (goal, i) => |
281 case (bare_concl goal) of |
286 case (bare_concl goal) of |
282 (rel $ _ $ (rep $ (abs $ _))) => |
287 (rel $ _ $ (rep $ (abs $ _))) => |