# HG changeset patch
# User wenzelm
# Date 1350144251 -7200
# Node ID 8fae089f5a0c30ddd2098e4795d3e26ee35e5a59
# Parent  9b19c0e8116620d3e063458bee80707abd946d84
refined Proof.the_finished_goal with more informative error;
more permissive Method.all_assm_tac: do not insist in solving by assumption here to postpone failure;
clarified Method.finish_text: no Thm.no_prems filtering here to postpone failure;

diff -r 9b19c0e81166 -r 8fae089f5a0c src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Sat Oct 13 16:19:16 2012 +0200
+++ b/src/Pure/Isar/method.ML	Sat Oct 13 18:04:11 2012 +0200
@@ -33,7 +33,6 @@
   val assm_tac: Proof.context -> int -> tactic
   val all_assm_tac: Proof.context -> tactic
   val assumption: Proof.context -> method
-  val close: bool -> Proof.context -> method
   val rule_trace: bool Config.T
   val trace: Proof.context -> thm list -> unit
   val rule_tac: thm list -> thm list -> int -> tactic
@@ -184,15 +183,20 @@
   cond_rtac (can Logic.dest_equals) Drule.reflexive_thm APPEND'
   cond_rtac (can Logic.dest_term) Drule.termI;
 
-fun all_assm_tac ctxt st = EVERY1 (replicate (Thm.nprems_of st) (assm_tac ctxt)) st;
+fun all_assm_tac ctxt =
+  let
+    fun tac i st =
+      if i > Thm.nprems_of st then all_tac st
+      else ((assm_tac ctxt i THEN tac i) ORELSE tac (i + 1)) st;
+  in tac 1 end;
 
 fun assumption ctxt = METHOD (HEADGOAL o
   (fn [] => assm_tac ctxt
     | [fact] => solve_tac [fact]
     | _ => K no_tac));
 
-fun close immed ctxt = METHOD (K
-  (FILTER Thm.no_prems ((if immed then all_assm_tac ctxt else all_tac) THEN flexflex_tac)));
+fun finish immed ctxt =
+  METHOD (K ((if immed then all_assm_tac ctxt else all_tac) THEN flexflex_tac));
 
 end;
 
@@ -299,8 +303,8 @@
 val done_text = Basic (K (SIMPLE_METHOD all_tac));
 fun sorry_text int = Basic (cheating int);
 
-fun finish_text (NONE, immed) = Basic (close immed)
-  | finish_text (SOME txt, immed) = Then [txt, Basic (close immed)];
+fun finish_text (NONE, immed) = Basic (finish immed)
+  | finish_text (SOME txt, immed) = Then [txt, Basic (finish immed)];
 
 
 (* method definitions *)
diff -r 9b19c0e81166 -r 8fae089f5a0c src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Sat Oct 13 16:19:16 2012 +0200
+++ b/src/Pure/Isar/proof.ML	Sat Oct 13 18:04:11 2012 +0200
@@ -488,7 +488,12 @@
 end;
 
 
-(* conclude_goal *)
+(* conclude goal *)
+
+fun unfinished_goal_msg ctxt goal =
+  Pretty.string_of (Pretty.chunks
+    (Goal_Display.pretty_goals ctxt goal @
+      [Pretty.str (string_of_int (Thm.nprems_of goal) ^ " unsolved goal(s)")]));
 
 fun conclude_goal ctxt goal propss =
   let
@@ -496,10 +501,7 @@
     val string_of_term = Syntax.string_of_term ctxt;
     val string_of_thm = Display.string_of_thm ctxt;
 
-    val ngoals = Thm.nprems_of goal;
-    val _ = ngoals = 0 orelse error (Pretty.string_of (Pretty.chunks
-      (Goal_Display.pretty_goals ctxt goal @
-        [Pretty.str (string_of_int ngoals ^ " unsolved goal(s)")])));
+    val _ = Thm.no_prems goal orelse error (unfinished_goal_msg ctxt goal);
 
     val extra_hyps = Assumption.extra_hyps ctxt goal;
     val _ = null extra_hyps orelse
@@ -525,6 +527,18 @@
       | recover_result _ _ = lost_structure ();
   in recover_result propss results end;
 
+fun the_finished_goal results =
+  (case Seq.pull results of
+    SOME ((f1, state1), rest) =>
+      let val (ctxt1, (_, goal1)) = get_goal state1 in
+        if Thm.no_prems goal1 then f1 state1
+        else
+          (case Seq.pull (Seq.filter (Thm.no_prems o #2 o #2 o get_goal o #2) rest) of
+            SOME ((f, state), _) => f state
+          | NONE => error ("Failed to finish proof:\n" ^ unfinished_goal_msg ctxt1 goal1))
+      end
+  | NONE => error "Failed to finish proof");
+
 
 (* goal views -- corresponding to methods *)
 
@@ -836,8 +850,6 @@
     NONE => error msg
   | SOME (s, _) => s);
 
-fun check_finish sq = check_result "Failed to finish proof" sq;
-
 
 (* unstructured refinement *)
 
@@ -952,10 +964,10 @@
 
 fun local_qeds txt =
   end_proof false txt
-  #> Seq.map (generic_qed Proof_Context.auto_bind_facts #->
-    (fn ((after_qed, _), results) => after_qed results));
+  #> Seq.map (pair (generic_qed Proof_Context.auto_bind_facts #->
+    (fn ((after_qed, _), results) => after_qed results)));
 
-fun local_qed txt = local_qeds txt #> check_finish;
+fun local_qed txt = local_qeds txt #> the_finished_goal;
 
 
 (* global goals *)
@@ -973,16 +985,16 @@
 
 fun global_qeds txt =
   end_proof true txt
-  #> Seq.map (generic_qed (K I) #> (fn (((_, after_qed), results), state) =>
-    after_qed results (context_of state)));
+  #> Seq.map (pair (generic_qed (K I) #> (fn (((_, after_qed), results), state) =>
+    after_qed results (context_of state))));
 
-fun global_qed txt = global_qeds txt #> check_finish;
+fun global_qed txt = global_qeds txt #> the_finished_goal;
 
 
 (* concluding steps *)
 
-fun terminal_proof qed initial terminal =
-  proof (SOME initial) #> Seq.maps (qed terminal) #> check_finish;
+fun terminal_proof qeds initial terminal =
+  proof (SOME initial) #> Seq.maps (qeds terminal) #> the_finished_goal;
 
 fun local_terminal_proof (text, opt_text) = terminal_proof local_qeds text (opt_text, true);
 val local_default_proof = local_terminal_proof (Method.default_text, NONE);