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