282 | map_goal f g (State (nd, node :: nodes)) = |
282 | map_goal f g (State (nd, node :: nodes)) = |
283 let val State (node', nodes') = map_goal f g (State (node, nodes)) |
283 let val State (node', nodes') = map_goal f g (State (node, nodes)) |
284 in map_context f (State (nd, node' :: nodes')) end |
284 in map_context f (State (nd, node' :: nodes')) end |
285 | map_goal _ _ state = state; |
285 | map_goal _ _ state = state; |
286 |
286 |
287 fun set_goal goal = map_goal I (fn (statement, messages, using, _, before_qed, after_qed) => |
287 fun set_goal goal = map_goal I (fn (statement, _, using, _, before_qed, after_qed) => |
288 (statement, messages, using, goal, before_qed, after_qed)); |
288 (statement, [], using, goal, before_qed, after_qed)); |
289 |
289 |
290 fun goal_message msg = map_goal I (fn (statement, messages, using, goal, before_qed, after_qed) => |
290 fun goal_message msg = map_goal I (fn (statement, messages, using, goal, before_qed, after_qed) => |
291 (statement, msg :: messages, using, goal, before_qed, after_qed)); |
291 (statement, msg :: messages, using, goal, before_qed, after_qed)); |
292 |
292 |
293 fun using_facts using = map_goal I (fn (statement, messages, _, goal, before_qed, after_qed) => |
293 fun using_facts using = map_goal I (fn (statement, _, _, goal, before_qed, after_qed) => |
294 (statement, messages, using, goal, before_qed, after_qed)); |
294 (statement, [], using, goal, before_qed, after_qed)); |
295 |
295 |
296 local |
296 local |
297 fun find i state = |
297 fun find i state = |
298 (case try current_goal state of |
298 (case try current_goal state of |
299 SOME (ctxt, goal) => (ctxt, (i, goal)) |
299 SOME (ctxt, goal) => (ctxt, (i, goal)) |
385 fun goal_cases st = |
385 fun goal_cases st = |
386 RuleCases.make_common true (Thm.theory_of_thm st, Thm.prop_of st) (map (rpair []) (goals st)); |
386 RuleCases.make_common true (Thm.theory_of_thm st, Thm.prop_of st) (map (rpair []) (goals st)); |
387 |
387 |
388 fun apply_method current_context pos meth_fun state = |
388 fun apply_method current_context pos meth_fun state = |
389 let |
389 let |
390 val (goal_ctxt, (_, {statement, messages, using, goal, before_qed, after_qed})) = |
390 val (goal_ctxt, (_, {statement, messages = _, using, goal, before_qed, after_qed})) = |
391 find_goal state; |
391 find_goal state; |
392 val ctxt = ContextPosition.put pos (if current_context then context_of state else goal_ctxt); |
392 val ctxt = ContextPosition.put pos (if current_context then context_of state else goal_ctxt); |
393 val meth = meth_fun ctxt; |
393 val meth = meth_fun ctxt; |
394 in |
394 in |
395 Method.apply meth using goal |> Seq.map (fn (meth_cases, goal') => |
395 Method.apply meth using goal |> Seq.map (fn (meth_cases, goal') => |
396 state |
396 state |
397 |> map_goal |
397 |> map_goal |
398 (ProofContext.add_cases false (no_goal_cases goal @ goal_cases goal') #> |
398 (ProofContext.add_cases false (no_goal_cases goal @ goal_cases goal') #> |
399 ProofContext.add_cases true meth_cases) |
399 ProofContext.add_cases true meth_cases) |
400 (K (statement, messages, using, goal', before_qed, after_qed))) |
400 (K (statement, [], using, goal', before_qed, after_qed))) |
401 end; |
401 end; |
402 |
402 |
403 fun select_goals n meth state = |
403 fun select_goals n meth state = |
404 state |
404 state |
405 |> (#2 o #2 o get_goal) |
405 |> (#2 o #2 o get_goal) |
651 state |
651 state |
652 |> assert_backward |
652 |> assert_backward |
653 |> map_context_result |
653 |> map_context_result |
654 (note "" (Attrib.map_facts (prep_atts (theory_of state)) (no_binding args))) |
654 (note "" (Attrib.map_facts (prep_atts (theory_of state)) (no_binding args))) |
655 |> (fn (named_facts, state') => |
655 |> (fn (named_facts, state') => |
656 state' |> map_goal I (fn (statement, messages, using, goal, before_qed, after_qed) => |
656 state' |> map_goal I (fn (statement, _, using, goal, before_qed, after_qed) => |
657 let |
657 let |
658 val ctxt = context_of state'; |
658 val ctxt = context_of state'; |
659 val ths = maps snd named_facts; |
659 val ths = maps snd named_facts; |
660 in (statement, messages, f ctxt ths using, g ctxt ths goal, before_qed, after_qed) end)); |
660 in (statement, [], f ctxt ths using, g ctxt ths goal, before_qed, after_qed) end)); |
661 |
661 |
662 fun append_using _ ths using = using @ filter_out Thm.is_dummy ths; |
662 fun append_using _ ths using = using @ filter_out Thm.is_dummy ths; |
663 fun unfold_using ctxt ths = map (LocalDefs.unfold ctxt ths); |
663 fun unfold_using ctxt ths = map (LocalDefs.unfold ctxt ths); |
664 val unfold_goals = LocalDefs.unfold_goals; |
664 val unfold_goals = LocalDefs.unfold_goals; |
665 |
665 |