196 (* context *) |
196 (* context *) |
197 |
197 |
198 val context_of = #context o current; |
198 val context_of = #context o current; |
199 val theory_of = Proof_Context.theory_of o context_of; |
199 val theory_of = Proof_Context.theory_of o context_of; |
200 |
200 |
|
201 fun map_node_context f = |
|
202 map_node (fn (ctxt, facts, mode, goal) => (f ctxt, facts, mode, goal)); |
|
203 |
201 fun map_context f = |
204 fun map_context f = |
202 map_current (fn (ctxt, facts, mode, goal) => (f ctxt, facts, mode, goal)); |
205 map_current (fn (ctxt, facts, mode, goal) => (f ctxt, facts, mode, goal)); |
203 |
206 |
204 fun map_context_result f state = |
207 fun map_context_result f state = |
205 f (context_of state) ||> (fn ctxt => map_context (K ctxt) state); |
208 f (context_of state) ||> (fn ctxt => map_context (K ctxt) state); |
290 val before_qed = #before_qed o #2 o current_goal; |
293 val before_qed = #before_qed o #2 o current_goal; |
291 |
294 |
292 |
295 |
293 (* nested goal *) |
296 (* nested goal *) |
294 |
297 |
295 fun map_goal f g (State (Node {context, facts, mode, goal = SOME goal}, nodes)) = |
298 fun map_goal f g h (State (Node {context, facts, mode, goal = SOME goal}, node :: nodes)) = |
296 let |
299 let |
297 val Goal {statement, messages, using, goal, before_qed, after_qed} = goal; |
300 val Goal {statement, messages, using, goal, before_qed, after_qed} = goal; |
298 val goal' = make_goal (g (statement, messages, using, goal, before_qed, after_qed)); |
301 val goal' = make_goal (g (statement, messages, using, goal, before_qed, after_qed)); |
299 in State (make_node (f context, facts, mode, SOME goal'), nodes) end |
302 val node' = map_node_context h node; |
300 | map_goal f g (State (nd, node :: nodes)) = |
303 in State (make_node (f context, facts, mode, SOME goal'), node' :: nodes) end |
301 let val State (node', nodes') = map_goal f g (State (node, nodes)) |
304 | map_goal f g h (State (nd, node :: nodes)) = |
302 in map_context f (State (nd, node' :: nodes')) end |
305 let |
303 | map_goal _ _ state = state; |
306 val nd' = map_node_context f nd; |
|
307 val State (node', nodes') = map_goal f g h (State (node, nodes)); |
|
308 in State (nd', node' :: nodes') end |
|
309 | map_goal _ _ _ state = state; |
304 |
310 |
305 fun provide_goal goal = map_goal I (fn (statement, _, using, _, before_qed, after_qed) => |
311 fun provide_goal goal = map_goal I (fn (statement, _, using, _, before_qed, after_qed) => |
306 (statement, [], using, goal, before_qed, after_qed)); |
312 (statement, [], using, goal, before_qed, after_qed)) I; |
307 |
313 |
308 fun goal_message msg = map_goal I (fn (statement, messages, using, goal, before_qed, after_qed) => |
314 fun goal_message msg = map_goal I (fn (statement, messages, using, goal, before_qed, after_qed) => |
309 (statement, msg :: messages, using, goal, before_qed, after_qed)); |
315 (statement, msg :: messages, using, goal, before_qed, after_qed)) I; |
310 |
316 |
311 fun using_facts using = map_goal I (fn (statement, _, _, goal, before_qed, after_qed) => |
317 fun using_facts using = map_goal I (fn (statement, _, _, goal, before_qed, after_qed) => |
312 (statement, [], using, goal, before_qed, after_qed)); |
318 (statement, [], using, goal, before_qed, after_qed)) I; |
313 |
319 |
314 local |
320 local |
315 fun find i state = |
321 fun find i state = |
316 (case try current_goal state of |
322 (case try current_goal state of |
317 SOME (ctxt, goal) => (ctxt, (i, goal)) |
323 SOME (ctxt, goal) => (ctxt, (i, goal)) |
405 Method.apply meth ctxt using goal |> Seq.map (fn (meth_cases, goal') => |
411 Method.apply meth ctxt using goal |> Seq.map (fn (meth_cases, goal') => |
406 state |
412 state |
407 |> map_goal |
413 |> map_goal |
408 (Proof_Context.add_cases false (no_goal_cases goal @ goal_cases goal') #> |
414 (Proof_Context.add_cases false (no_goal_cases goal @ goal_cases goal') #> |
409 Proof_Context.add_cases true meth_cases) |
415 Proof_Context.add_cases true meth_cases) |
410 (K (statement, [], using, goal', before_qed, after_qed))) |
416 (K (statement, [], using, goal', before_qed, after_qed)) I) |
411 end; |
417 end; |
412 |
418 |
413 fun select_goals n meth state = |
419 fun select_goals n meth state = |
414 state |
420 state |
415 |> (#2 o #2 o get_goal) |
421 |> (#2 o #2 o get_goal) |
715 |> (fn (named_facts, state') => |
721 |> (fn (named_facts, state') => |
716 state' |> map_goal I (fn (statement, _, using, goal, before_qed, after_qed) => |
722 state' |> map_goal I (fn (statement, _, using, goal, before_qed, after_qed) => |
717 let |
723 let |
718 val ctxt = context_of state'; |
724 val ctxt = context_of state'; |
719 val ths = maps snd named_facts; |
725 val ths = maps snd named_facts; |
720 in (statement, [], f ctxt ths using, g ctxt ths goal, before_qed, after_qed) end)); |
726 in (statement, [], f ctxt ths using, g ctxt ths goal, before_qed, after_qed) end) I); |
721 |
727 |
722 fun append_using _ ths using = using @ filter_out Thm.is_dummy ths; |
728 fun append_using _ ths using = using @ filter_out Thm.is_dummy ths; |
723 fun unfold_using ctxt ths = map (Local_Defs.unfold ctxt ths); |
729 fun unfold_using ctxt ths = map (Local_Defs.unfold ctxt ths); |
724 val unfold_goals = Local_Defs.unfold_goals; |
730 val unfold_goals = Local_Defs.unfold_goals; |
725 |
731 |
1072 fun future_proof done get_context fork_proof state = |
1078 fun future_proof done get_context fork_proof state = |
1073 let |
1079 let |
1074 val _ = assert_backward state; |
1080 val _ = assert_backward state; |
1075 val (goal_ctxt, (_, goal)) = find_goal state; |
1081 val (goal_ctxt, (_, goal)) = find_goal state; |
1076 val {statement as (kind, _, prop), messages, using, goal, before_qed, after_qed} = goal; |
1082 val {statement as (kind, _, prop), messages, using, goal, before_qed, after_qed} = goal; |
1077 val goal_txt = prop :: map Thm.term_of (Assumption.all_assms_of goal_ctxt); |
1083 val goal_tfrees = |
|
1084 fold Term.add_tfrees |
|
1085 (prop :: map Thm.term_of (Assumption.all_assms_of goal_ctxt)) []; |
1078 |
1086 |
1079 val _ = is_relevant state andalso error "Cannot fork relevant proof"; |
1087 val _ = is_relevant state andalso error "Cannot fork relevant proof"; |
1080 |
1088 |
1081 val prop' = Logic.protect prop; |
1089 val prop' = Logic.protect prop; |
1082 val statement' = (kind, [[], [prop']], prop'); |
1090 val statement' = (kind, [[], [prop']], prop'); |
1088 val after_qed' = (after_local', after_global'); |
1096 val after_qed' = (after_local', after_global'); |
1089 val this_name = Proof_Context.full_name goal_ctxt (Binding.name Auto_Bind.thisN); |
1097 val this_name = Proof_Context.full_name goal_ctxt (Binding.name Auto_Bind.thisN); |
1090 |
1098 |
1091 val result_ctxt = |
1099 val result_ctxt = |
1092 state |
1100 state |
1093 |> map_contexts (fold Variable.declare_term goal_txt) |
|
1094 |> map_goal I (K (statement', messages, using, goal', before_qed, after_qed')) |
1101 |> map_goal I (K (statement', messages, using, goal', before_qed, after_qed')) |
|
1102 (fold (Variable.declare_typ o TFree) goal_tfrees) |
1095 |> fork_proof; |
1103 |> fork_proof; |
1096 |
1104 |
1097 val future_thm = result_ctxt |> Future.map (fn (_, x) => |
1105 val future_thm = result_ctxt |> Future.map (fn (_, x) => |
1098 Proof_Context.get_fact_single (get_context x) (Facts.named this_name)); |
1106 Proof_Context.get_fact_single (get_context x) (Facts.named this_name)); |
1099 val finished_goal = Goal.future_result goal_ctxt future_thm prop'; |
1107 val finished_goal = Goal.future_result goal_ctxt future_thm prop'; |
1100 val state' = |
1108 val state' = |
1101 state |
1109 state |
1102 |> map_goal I (K (statement, messages, using, finished_goal, NONE, after_qed)) |
1110 |> map_goal I (K (statement, messages, using, finished_goal, NONE, after_qed)) I |
1103 |> done; |
1111 |> done; |
1104 in (Future.map #1 result_ctxt, state') end; |
1112 in (Future.map #1 result_ctxt, state') end; |
1105 |
1113 |
1106 in |
1114 in |
1107 |
1115 |