src/Pure/Isar/proof.ML

--- a/src/Pure/Isar/proof.ML	Sat Oct 15 00:08:07 2005 +0200
+++ b/src/Pure/Isar/proof.ML	Sat Oct 15 00:08:08 2005 +0200
@@ -87,14 +87,16 @@
   val local_goal: (context -> ((string * string) * (string * thm list) list) -> unit) ->
     (theory -> 'a -> context attribute) ->
     (context * 'b list -> context * (term list list * (context -> context))) ->
-    string -> (context * thm list -> thm list list -> state -> state Seq.seq) ->
+    string -> Method.text option ->
+    (context * thm list -> thm list list -> state -> state Seq.seq) ->
     ((string * 'a list) * 'b) list -> state -> state
   val local_qed: Method.text option * bool -> state -> state Seq.seq
   val global_goal: (context -> (string * string) * (string * thm list) list -> unit) ->
     (theory -> 'a -> theory attribute) ->
     (context * 'b list -> context * (term list list * (context -> context))) ->
-    string -> (context * thm list -> thm list list -> theory -> theory) -> string option ->
-    string * 'a list -> ((string * 'a list) * 'b) list -> context -> state
+    string -> Method.text option ->
+    (context * thm list -> thm list list -> theory -> theory) ->
+    string option -> string * 'a list -> ((string * 'a list) * 'b) list -> context -> state
   val global_qed: Method.text option * bool -> state -> theory * context
   val local_terminal_proof: Method.text * Method.text option -> state -> state Seq.seq
   val local_default_proof: state -> state Seq.seq
@@ -106,23 +108,29 @@
   val global_immediate_proof: state -> theory * context
   val global_done_proof: state -> theory * context
   val global_skip_proof: bool -> state -> theory * context
-  val have: (context * thm list -> thm list list -> state -> state Seq.seq) ->
+  val have: Method.text option ->
+    (context * thm list -> thm list list -> state -> state Seq.seq) ->
     ((string * Attrib.src list) * (string * (string list * string list)) list) list ->
     bool -> state -> state
-  val have_i: (context * thm list -> thm list list -> state -> state Seq.seq) ->
+  val have_i: Method.text option ->
+    (context * thm list -> thm list list -> state -> state Seq.seq) ->
     ((string * context attribute list) * (term * (term list * term list)) list) list ->
     bool -> state -> state
-  val show: (context * thm list -> thm list list -> state -> state Seq.seq) ->
+  val show: Method.text option ->
+    (context * thm list -> thm list list -> state -> state Seq.seq) ->
     ((string * Attrib.src list) * (string * (string list * string list)) list) list ->
     bool -> state -> state
-  val show_i: (context * thm list -> thm list list -> state -> state Seq.seq) ->
+  val show_i: Method.text option ->
+    (context * thm list -> thm list list -> state -> state Seq.seq) ->
     ((string * context attribute list) * (term * (term list * term list)) list) list ->
     bool -> state -> state
-  val theorem: string -> (context * thm list -> thm list list -> theory -> theory) ->
+  val theorem: string -> Method.text option ->
+    (context * thm list -> thm list list -> theory -> theory) ->
     string option -> string * Attrib.src list ->
     ((string * Attrib.src list) * (string * (string list * string list)) list) list ->
     context -> state
-  val theorem_i: string -> (context * thm list -> thm list list -> theory -> theory) ->
+  val theorem_i: string -> Method.text option ->
+    (context * thm list -> thm list list -> theory -> theory) ->
     string option -> string * theory attribute list ->
     ((string * theory attribute list) * (term * (term list * term list)) list) list ->
     context -> state
@@ -154,14 +162,16 @@
    {statement: string * term list list,     (*goal kind and statement*)
     using: thm list,                        (*goal facts*)
     goal: thm,                              (*subgoals ==> statement*)
+    before_qed: Method.text option,
     after_qed:   (* FIXME results only *)
       (context * thm list -> thm list list -> state -> state Seq.seq) *
       (context * thm list -> thm list list -> theory -> theory)};
 
 exception STATE of string * state;
 
-fun make_goal (statement, using, goal, after_qed) =
-  Goal {statement = statement, using = using, goal = goal, after_qed = after_qed};
+fun make_goal (statement, using, goal, before_qed, after_qed) =
+  Goal {statement = statement, using = using, goal = goal,
+    before_qed = before_qed, after_qed = after_qed};
 
 fun make_node (context, facts, mode, goal) =
   Node {context = context, facts = facts, mode = mode, goal = goal};
@@ -205,7 +215,7 @@
   map_current (fn (ctxt, facts, mode, goal) => (f ctxt, facts, mode, goal));
 
 fun map_context_result f state =
-  f (context_of state) |> swap ||> (fn ctxt => map_context (K ctxt) state);
+  f (context_of state) ||> (fn ctxt => map_context (K ctxt) state);
 
 val warn_extra_tfrees = map_context o ProofContext.warn_extra_tfrees o context_of;
 val add_binds_i = map_context o ProofContext.add_binds_i;
@@ -282,21 +292,23 @@
 
 fun put_goal goal = map_current (fn (ctxt, using, mode, _) => (ctxt, using, mode, goal));
 
+val before_qed = #before_qed o #2 o current_goal;
+
 
 (* nested goal *)
 
 fun map_goal f g (State (Node {context, facts, mode, goal = SOME goal}, nodes)) =
       let
-        val Goal {statement, using, goal, after_qed} = goal;
-        val goal' = make_goal (g (statement, using, goal, after_qed));
+        val Goal {statement, using, goal, before_qed, after_qed} = goal;
+        val goal' = make_goal (g (statement, using, goal, before_qed, after_qed));
       in State (make_node (f context, facts, mode, SOME goal'), nodes) end
   | map_goal f g (State (nd, node :: nodes)) =
       let val State (node', nodes') = map_goal f g (State (node, nodes))
       in map_context f (State (nd, node' :: nodes')) end
   | map_goal _ _ state = state;
 
-fun using_facts using =
-  map_goal I (fn (statement, _, goal, after_qed) => (statement, using, goal, after_qed));
+fun using_facts using = map_goal I (fn (statement, _, goal, before_qed, after_qed) =>
+  (statement, using, goal, before_qed, after_qed));
 
 local
   fun find i state =
@@ -340,7 +352,7 @@
       (case filter_out (equal "") strs of [] => ""
       | strs' => enclose " (" ")" (commas strs'));
 
-    fun prt_goal (SOME (ctxt, (i, {statement = (kind, _), using, goal, after_qed = _}))) =
+    fun prt_goal (SOME (ctxt, (i, {statement = (kind, _), using, goal, before_qed, after_qed}))) =
           pretty_facts "using " ctxt
             (if mode <> Backward orelse null using then NONE else SOME using) @
           [Pretty.str ("goal" ^ description [kind, levels_up (i div 2),
@@ -389,7 +401,7 @@
 
 fun apply_method current_context meth_fun state =
   let
-    val (goal_ctxt, (_, {statement, using, goal, after_qed})) = find_goal state;
+    val (goal_ctxt, (_, {statement, using, goal, before_qed, after_qed})) = find_goal state;
     val meth = meth_fun (if current_context then context_of state else goal_ctxt);
   in
     Method.apply meth using goal |> Seq.map (fn (goal', meth_cases) =>
@@ -397,7 +409,7 @@
       |> check_theory (Thm.theory_of_thm goal')
       |> map_goal
           (ProofContext.add_cases (no_goal_cases goal @ goal_cases goal' @ meth_cases))
-          (K (statement, using, goal', after_qed)))
+          (K (statement, using, goal', before_qed, after_qed)))
   end;
 
 fun apply_text cc text state =
@@ -431,14 +443,15 @@
     else all_tac));
 
 fun refine_goal print_rule inner raw_rule state =
-  let val (outer, (_, {statement, using, goal, after_qed})) = find_goal state in
+  let val (outer, (_, {statement, using, goal, before_qed, after_qed})) = find_goal state in
     raw_rule
     |> ProofContext.export true inner outer
     |> Seq.maps (fn rule =>
       (print_rule outer rule;
         goal
         |> FINDGOAL (refine_tac rule)
-        |> Seq.map (fn goal' => map_goal I (K (statement, using, goal', after_qed)) state)))
+        |> Seq.map (fn goal' =>
+          map_goal I (K (statement, using, goal', before_qed, after_qed)) state)))
   end;
 
 in
@@ -506,9 +519,9 @@
 
 local
 
-fun gen_fix fx args =
+fun gen_fix fix_ctxt args =
   assert_forward
-  #> map_context (fx args)
+  #> map_context (fix_ctxt args)
   #> put_facts NONE;
 
 in
@@ -634,8 +647,8 @@
   state
   |> assert_backward
   |> map_context_result (note (Attrib.map_facts (prep_atts (theory_of state)) (no_binding args)))
-  |-> (fn named_facts => map_goal I (fn (statement, using, goal, after_qed) =>
-    (statement, using @ List.concat (map snd named_facts), goal, after_qed)));
+  |-> (fn named_facts => map_goal I (fn (statement, using, goal, before_qed, after_qed) =>
+    (statement, using @ List.concat (map snd named_facts), goal, before_qed, after_qed)));
 
 in
 
@@ -704,7 +717,7 @@
 
 fun proof opt_text =
   assert_backward
-  #> refine (if_none opt_text Method.default_text)
+  #> refine (the_default Method.default_text opt_text)
   #> Seq.map (using_facts [] #> enter_forward);
 
 fun end_proof bot txt =
@@ -713,7 +726,8 @@
   #> close_block
   #> assert_current_goal true
   #> using_facts []
-  #> refine (Method.finish_text txt);
+  #> `before_qed #-> (refine o the_default Method.succeed_text)
+  #> Seq.maps (refine (Method.finish_text txt));
 
 
 (* unstructured refinement *)
@@ -756,7 +770,7 @@
   | vars => warning ("Goal statement contains unbound schematic variable(s): " ^
       commas (map (ProofContext.string_of_term (context_of state) o Var) vars)));
 
-fun generic_goal prepp kind after_qed raw_propp state =
+fun generic_goal prepp kind before_qed after_qed raw_propp state =
   let
     val thy = theory_of state;
     val chaining = can assert_chain state;
@@ -766,7 +780,7 @@
       |> assert_forward_or_chain
       |> enter_forward
       |> open_block
-      |> map_context_result (fn ctxt => prepp (ctxt, raw_propp));
+      |> map_context_result (fn ctxt => swap (prepp (ctxt, raw_propp)));
 
     val props = List.concat propss;
     val goal = Drule.mk_triv_goal (Thm.cterm_of thy (Logic.mk_conjunction_list props));
@@ -778,7 +792,7 @@
     goal_state
     |> tap (check_tvars props)
     |> tap (check_vars props)
-    |> put_goal (SOME (make_goal ((kind, propss), [], goal, after_qed')))
+    |> put_goal (SOME (make_goal ((kind, propss), [], goal, before_qed, after_qed')))
     |> map_context (ProofContext.add_cases (AutoBind.cases thy props))
     |> map_context (ProofContext.auto_bind_goal props)
     |> K chaining ? (`the_facts #-> using_facts)
@@ -791,7 +805,8 @@
 
 fun generic_qed state =
   let
-    val (goal_ctxt, {statement = (_, stmt), using, goal, after_qed}) = current_goal state;
+    val (goal_ctxt, {statement = (_, stmt), using, goal, before_qed = _, after_qed}) =
+      current_goal state;
     val outer_state = state |> close_block;
     val outer_ctxt = context_of outer_state;
 
@@ -810,7 +825,7 @@
 
 (* local goals *)
 
-fun local_goal print_results prep_att prepp kind after_qed stmt state =
+fun local_goal print_results prep_att prepp kind before_qed after_qed stmt state =
   let
     val ((names, attss), propp) = prep_names (prep_att (theory_of state)) stmt;
 
@@ -820,7 +835,7 @@
       #> after_qed raw_results results;
   in
     state
-    |> generic_goal prepp (kind ^ goal_names NONE "" names) (after_qed', K (K I)) propp
+    |> generic_goal prepp (kind ^ goal_names NONE "" names) before_qed (after_qed', K (K I)) propp
     |> warn_extra_tfrees state
   end;
 
@@ -834,7 +849,7 @@
 (* global goals *)
 
 fun global_goal print_results prep_att prepp
-    kind after_qed target (name, raw_atts) stmt ctxt =
+    kind before_qed after_qed target (name, raw_atts) stmt ctxt =
   let
     val thy = ProofContext.theory_of ctxt;
     val thy_ctxt = ProofContext.init thy;
@@ -859,7 +874,7 @@
   in
     init ctxt
     |> generic_goal (prepp #> ProofContext.auto_fix) (kind ^ goal_names target name names)
-      (K (K Seq.single), after_qed') propp
+      before_qed (K (K Seq.single), after_qed') propp
   end;
 
 fun check_result msg state sq =
@@ -911,10 +926,10 @@
 
 local
 
-fun gen_have prep_att prepp after_qed stmt int =
-  local_goal (ProofDisplay.print_results int) prep_att prepp "have" after_qed stmt;
+fun gen_have prep_att prepp before_qed after_qed stmt int =
+  local_goal (ProofDisplay.print_results int) prep_att prepp "have" before_qed after_qed stmt;
 
-fun gen_show prep_att prepp after_qed stmt int state =
+fun gen_show prep_att prepp before_qed after_qed stmt int state =
   let
     val testing = ref false;
     val rule = ref (NONE: thm option);
@@ -941,7 +956,7 @@
       #> Seq.maps (after_qed raw_results results);
   in
     state
-    |> local_goal print_results prep_att prepp "show" after_qed' stmt
+    |> local_goal print_results prep_att prepp "show" before_qed after_qed' stmt
     |> K int ? (fn goal_state =>
       (case test_proof goal_state of
         Result (SOME _) => goal_state
@@ -950,8 +965,8 @@
       | Exn exn => raise EXCEPTION (exn, fail_msg (context_of goal_state))))
   end;
 
-fun gen_theorem prep_att prepp kind after_qed target a =
-  global_goal ProofDisplay.present_results prep_att prepp kind after_qed target a;
+fun gen_theorem prep_att prepp kind before_qed after_qed target a =
+  global_goal ProofDisplay.present_results prep_att prepp kind before_qed after_qed target a;
 
 in