404 fun goalN i = "goal" ^ string_of_int i; |
404 fun goalN i = "goal" ^ string_of_int i; |
405 fun goals st = map goalN (1 upto Thm.nprems_of st); |
405 fun goals st = map goalN (1 upto Thm.nprems_of st); |
406 |
406 |
407 fun no_goal_cases st = map (rpair NONE) (goals st); |
407 fun no_goal_cases st = map (rpair NONE) (goals st); |
408 |
408 |
409 fun goal_cases st = |
409 fun goal_cases ctxt st = |
410 Rule_Cases.make_common |
410 Rule_Cases.make_common ctxt (Thm.prop_of st) (map (rpair [] o rpair []) (goals st)); |
411 (Thm.theory_of_thm st, Thm.prop_of st) (map (rpair [] o rpair []) (goals st)); |
|
412 |
411 |
413 fun apply_method text ctxt state = |
412 fun apply_method text ctxt state = |
414 #2 (#2 (find_goal state)) |> (fn {statement, using, goal, before_qed, after_qed} => |
413 #2 (#2 (find_goal state)) |> (fn {statement, using, goal, before_qed, after_qed} => |
415 Method.evaluate text ctxt using goal |
414 Method.evaluate text ctxt using goal |
416 |> Seq.map (fn (meth_cases, goal') => |
415 |> Seq.map (fn (meth_cases, goal') => |
417 state |
416 state |
418 |> map_goal |
417 |> map_goal |
419 (Proof_Context.update_cases false (no_goal_cases goal @ goal_cases goal') #> |
418 (Proof_Context.update_cases false (no_goal_cases goal @ goal_cases ctxt goal') #> |
420 Proof_Context.update_cases true meth_cases) |
419 Proof_Context.update_cases true meth_cases) |
421 (K (statement, using, goal', before_qed, after_qed)) I)); |
420 (K (statement, using, goal', before_qed, after_qed)) I)); |
422 |
421 |
423 in |
422 in |
424 |
423 |