# HG changeset patch
# User wenzelm
# Date 1231356425 -3600
# Node ID c96b91bab2e60bf11e44b71e6441c3f108b0beb1
# Parent  a3c7e9ae9b7165ceb304dc89e575dc026fe3bb36
future_proof: refined version covers local_future_proof and global_future_proof;
future_proof: refrain from full Variable.auto_fixes -- not all contexts in the stack are in body mode;
refined is_relevant: mode check;
added local/global_future_terminal_proof;

diff -r a3c7e9ae9b71 -r c96b91bab2e6 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Wed Jan 07 17:26:03 2009 +0100
+++ b/src/Pure/Isar/proof.ML	Wed Jan 07 20:27:05 2009 +0100
@@ -30,7 +30,6 @@
   val enter_forward: state -> state
   val goal_message: (unit -> Pretty.T) -> state -> state
   val get_goal: state -> context * (thm list * thm)
-  val schematic_goal: state -> bool
   val show_main_goal: bool ref
   val verbose: bool ref
   val pretty_state: int -> state -> Pretty.T list
@@ -113,9 +112,14 @@
     (Attrib.binding * (string * string list) list) list -> bool -> state -> state
   val show_i: Method.text option -> (thm list list -> state -> state) ->
     ((Binding.T * attribute list) * (term * term list) list) list -> bool -> state -> state
+  val schematic_goal: state -> bool
   val is_relevant: state -> bool
-  val future_proof: (state -> ('a * context) future) -> state -> 'a future * context
-  val future_terminal_proof: Method.text * Method.text option -> bool -> state -> context
+  val local_future_proof: (state -> ('a * state) Future.future) ->
+    state -> 'a Future.future * state
+  val global_future_proof: (state -> ('a * Proof.context) Future.future) ->
+    state -> 'a Future.future * context
+  val local_future_terminal_proof: Method.text * Method.text option -> bool -> state -> state
+  val global_future_terminal_proof: Method.text * Method.text option -> bool -> state -> context
 end;
 
 structure Proof: PROOF =
@@ -312,12 +316,6 @@
   let val (ctxt, (_, {using, goal, ...})) = find_goal state
   in (ctxt, (using, goal)) end;
 
-fun schematic_goal state =
-  let val (_, (_, {statement = (_, _, prop), ...})) = find_goal state in
-    Term.exists_subterm Term.is_Var prop orelse
-    Term.exists_type (Term.exists_subtype Term.is_TVar) prop
-  end;
-
 
 
 (** pretty_state **)
@@ -972,24 +970,31 @@
 end;
 
 
-(* fork global proofs *)
+
+(** future proofs **)
+
+(* relevant proof states *)
+
+fun is_schematic t =
+  Term.exists_subterm Term.is_Var t orelse
+  Term.exists_type (Term.exists_subtype Term.is_TVar) t;
+
+fun schematic_goal state =
+  let val (_, (_, {statement = (_, _, prop), ...})) = find_goal state
+  in is_schematic prop end;
+
+fun is_relevant state =
+  (case try find_goal state of
+    NONE => true
+  | SOME (_, (_, {statement = (_, _, prop), goal, ...})) =>
+      is_schematic prop orelse not (Logic.protect prop aconv Thm.concl_of goal));
+
+
+(* full proofs *)
 
 local
 
-fun is_original state =
-  (case try find_goal state of
-    NONE => false
-  | SOME (_, (_, {statement = (_, _, prop), goal, ...})) =>
-      Logic.protect prop aconv Thm.concl_of goal);
-
-in
-
-fun is_relevant state =
-  can (assert_bottom false) state orelse
-  not (is_original state) orelse
-  schematic_goal state;
-
-fun future_proof fork_proof state =
+fun future_proof done get_context fork_proof state =
   let
     val _ = assert_backward state;
     val (goal_ctxt, (_, goal)) = find_goal state;
@@ -1001,31 +1006,53 @@
     val statement' = (kind, [[], [prop']], prop');
     val goal' = Thm.adjust_maxidx_thm (Thm.maxidx_of goal)
       (Drule.comp_no_flatten (goal, Thm.nprems_of goal) 1 Drule.protectI);
-    fun after_qed' [[th]] = ProofContext.put_thms false (AutoBind.thisN, SOME [th]);
+
+    fun after_local' [[th]] = put_thms false (AutoBind.thisN, SOME [th]);
+    fun after_global' [[th]] = ProofContext.put_thms false (AutoBind.thisN, SOME [th]);
+    val after_qed' = (after_local', after_global');
     val this_name = ProofContext.full_bname goal_ctxt AutoBind.thisN;
 
     val result_ctxt =
       state
-      |> map_contexts (Variable.auto_fixes prop)
-      |> map_goal I (K (statement', messages, using, goal', before_qed, (#1 after_qed, after_qed')))
+      |> map_contexts (Variable.declare_term prop)
+      |> map_goal I (K (statement', messages, using, goal', before_qed, after_qed'))
       |> fork_proof;
 
-    val future_thm = result_ctxt |> Future.map (fn (_, ctxt) =>
-      ProofContext.get_fact_single ctxt (Facts.named this_name));
-    val finished_goal = Goal.future_result goal_ctxt future_thm prop';
+    val future_thm = result_ctxt |> Future.map (fn (_, x) =>
+      ProofContext.get_fact_single (get_context x) (Facts.named this_name));
+    val finished_goal = exception_trace (fn () => Goal.future_result goal_ctxt future_thm prop');
     val state' =
       state
       |> map_goal I (K (statement, messages, using, finished_goal, NONE, after_qed))
-      |> global_done_proof;
+      |> done;
   in (Future.map #1 result_ctxt, state') end;
 
+in
+
+fun local_future_proof x = future_proof local_done_proof context_of x;
+fun global_future_proof x = future_proof global_done_proof I x;
+
 end;
 
-fun future_terminal_proof meths int state =
+
+(* terminal proofs *)
+
+local
+
+fun future_terminal_proof proof1 proof2 meths int state =
   if int orelse is_relevant state orelse not (Future.enabled ())
-  then global_terminal_proof meths state
-  else #2 (state |> future_proof (fn state' =>
-    Future.fork_pri ~1 (fn () => ((), global_terminal_proof meths state'))));
+  then proof1 meths state
+  else snd (state |> proof2 (fn state' => Future.fork_pri ~1 (fn () => ((), proof1 meths state'))));
+
+in
+
+fun local_future_terminal_proof x =
+  future_terminal_proof local_terminal_proof local_future_proof x;
+
+fun global_future_terminal_proof x =
+  future_terminal_proof global_terminal_proof global_future_proof x;
 
 end;
 
+end;
+