279 | _ => K no_tac |
279 | _ => K no_tac |
280 end |
280 end |
281 (* TODO: Again, can one specify more concretely *) |
281 (* TODO: Again, can one specify more concretely *) |
282 (* TODO: in terms of R when no_tac should be returned? *) |
282 (* TODO: in terms of R when no_tac should be returned? *) |
283 |
283 |
284 fun rep_abs_rsp_tac ctxt = |
284 fun rep_abs_rsp_tac ctxt = |
285 SUBGOAL (fn (goal, i) => |
285 SUBGOAL (fn (goal, i) => |
286 case (bare_concl goal) of |
286 case (try bare_concl goal) of |
287 (rel $ _ $ (rep $ (abs $ _))) => |
287 SOME (rel $ _ $ (rep $ (abs $ _))) => |
288 (let |
288 let |
289 val thy = ProofContext.theory_of ctxt; |
289 val thy = ProofContext.theory_of ctxt; |
290 val (ty_a, ty_b) = dest_fun_type (fastype_of abs); |
290 val (ty_a, ty_b) = dest_fun_type (fastype_of abs); |
291 val ty_inst = map (SOME o (ctyp_of thy)) [ty_a, ty_b]; |
291 val ty_inst = map (SOME o (ctyp_of thy)) [ty_a, ty_b]; |
292 val t_inst = map (SOME o (cterm_of thy)) [rel, abs, rep]; |
292 in |
293 val inst_thm = Drule.instantiate' ty_inst t_inst @{thm rep_abs_rsp} |
293 case try (map (SOME o (cterm_of thy))) [rel, abs, rep] of |
294 in |
294 SOME t_inst => |
295 (rtac inst_thm THEN' quotient_tac ctxt) i |
295 (case try (Drule.instantiate' ty_inst t_inst) @{thm rep_abs_rsp} of |
296 end |
296 SOME inst_thm => (rtac inst_thm THEN' quotient_tac ctxt) i |
297 handle THM _ => no_tac | TYPE _ => no_tac) (* TODO: same here *) |
297 | NONE => no_tac) |
|
298 | NONE => no_tac |
|
299 end |
298 | _ => no_tac) |
300 | _ => no_tac) |
299 |
301 |
300 |
302 |
301 (* |
303 (* |
302 To prove that the regularised theorem implies the abs/rep injected, |
304 To prove that the regularised theorem implies the abs/rep injected, |