summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/Pure/Isar/proof.ML

changeset 24556 | 22ac3c8d78a5 |

parent 24550 | ec228ae5a620 |

child 24794 | 5740b01a1553 |

equal
deleted
inserted
replaced

24555:ea220faa69e7 | 24556:22ac3c8d78a5 |
---|---|

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 |