287 val start_rule = |
287 val start_rule = |
288 if equiv then @{thm transfer_start} else @{thm transfer_start'} |
288 if equiv then @{thm transfer_start} else @{thm transfer_start'} |
289 val rules = get_transfer_raw ctxt |
289 val rules = get_transfer_raw ctxt |
290 (* allow unsolved subgoals only for standard transfer method, not for transfer' *) |
290 (* allow unsolved subgoals only for standard transfer method, not for transfer' *) |
291 val end_tac = if equiv then K all_tac else K no_tac |
291 val end_tac = if equiv then K all_tac else K no_tac |
|
292 val err_msg = "Transfer failed to convert goal to an object-logic formula" |
|
293 fun main_tac (t, i) = |
|
294 rtac start_rule i THEN |
|
295 (rtac (transfer_rule_of_term ctxt (HOLogic.dest_Trueprop t)) |
|
296 THEN_ALL_NEW |
|
297 (SOLVED' (REPEAT_ALL_NEW (resolve_tac rules)) |
|
298 ORELSE' end_tac)) (i + 1) |
|
299 handle TERM (_, ts) => raise TERM (err_msg, ts) |
292 in |
300 in |
293 EVERY |
301 EVERY |
294 [rewrite_goal_tac pre_simps i THEN |
302 [rewrite_goal_tac pre_simps i THEN |
295 SUBGOAL (fn (t, i) => |
303 SUBGOAL main_tac i, |
296 rtac start_rule i THEN |
|
297 (rtac (transfer_rule_of_term ctxt (HOLogic.dest_Trueprop t)) |
|
298 THEN_ALL_NEW |
|
299 (SOLVED' (REPEAT_ALL_NEW (resolve_tac rules)) |
|
300 ORELSE' end_tac)) (i + 1)) i, |
|
301 (* FIXME: rewrite_goal_tac does unwanted eta-contraction *) |
304 (* FIXME: rewrite_goal_tac does unwanted eta-contraction *) |
302 rewrite_goal_tac post_simps i, |
305 rewrite_goal_tac post_simps i, |
303 rtac @{thm _} i] |
306 rtac @{thm _} i] |
304 end |
307 end |
305 |
308 |