--- a/NEWS Mon Feb 23 14:48:40 2015 +0100
+++ b/NEWS Mon Feb 23 14:50:30 2015 +0100
@@ -282,6 +282,9 @@
* Synchronized.value (ML) is actually synchronized (as in Scala):
subtle change of semantics with minimal potential for INCOMPATIBILITY.
+* Goal.prove_multi is superseded by the fully general Goal.prove_common,
+which also allows to specify a fork priority.
+
*** System ***
--- a/src/Doc/Implementation/Proof.thy Mon Feb 23 14:48:40 2015 +0100
+++ b/src/Doc/Implementation/Proof.thy Mon Feb 23 14:50:30 2015 +0100
@@ -402,7 +402,8 @@
\begin{mldecls}
@{index_ML Goal.prove: "Proof.context -> string list -> term list -> term ->
({prems: thm list, context: Proof.context} -> tactic) -> thm"} \\
- @{index_ML Goal.prove_multi: "Proof.context -> string list -> term list -> term list ->
+ @{index_ML Goal.prove_common: "Proof.context -> int option ->
+ string list -> term list -> term list ->
({prems: thm list, context: Proof.context} -> tactic) -> thm list"} \\
\end{mldecls}
\begin{mldecls}
@@ -436,10 +437,22 @@
it. The latter may depend on the local assumptions being presented
as facts. The result is in HHF normal form.
- \item @{ML Goal.prove_multi} is similar to @{ML Goal.prove}, but
- states several conclusions simultaneously. The goal is encoded by
- means of Pure conjunction; @{ML Goal.conjunction_tac} will turn this
- into a collection of individual subgoals.
+ \item @{ML Goal.prove_common}~@{text "ctxt fork_pri"} is the general form
+ to state and prove a simultaneous goal statement, where @{ML Goal.prove}
+ is a convenient shorthand for the most common application.
+
+ The given list of simultaneous conclusions is encoded in the goal state by
+ means of Pure conjunction: @{ML Goal.conjunction_tac} will turn this into
+ a collection of individual subgoals, but note that the original multi-goal
+ state is usually required for advanced induction.
+
+ It is possible to provide an optional priority for a forked proof,
+ typically @{ML "SOME ~1"}, while @{ML NONE} means the proof is immediate
+ (sequential) as for @{ML Goal.prove}. Note that a forked proof does not
+ exhibit any failures in the usual way via exceptions in ML, but
+ accumulates error situations under the execution id of the running
+ transaction. Thus the system is able to expose error messages ultimately
+ to the end-user, even though the subsequent ML code misses them.
\item @{ML Obtain.result}~@{text "tac thms ctxt"} eliminates the
given facts using a tactic, which results in additional fixed
--- a/src/Pure/axclass.ML Mon Feb 23 14:48:40 2015 +0100
+++ b/src/Pure/axclass.ML Mon Feb 23 14:50:30 2015 +0100
@@ -457,7 +457,7 @@
val names = map (prefix arity_prefix) (Logic.name_arities arity);
val props = Logic.mk_arities arity;
val ths =
- Goal.prove_multi ctxt [] [] props
+ Goal.prove_common ctxt NONE [] [] props
(fn {context, ...} => Goal.precise_conjunction_tac (length props) 1 THEN tac context)
handle ERROR msg =>
cat_error msg ("The error(s) above occurred while trying to prove type arity " ^
--- a/src/Pure/goal.ML Mon Feb 23 14:48:40 2015 +0100
+++ b/src/Pure/goal.ML Mon Feb 23 14:50:30 2015 +0100
@@ -28,7 +28,7 @@
val future_result: Proof.context -> thm future -> term -> thm
val prove_internal: Proof.context -> cterm list -> cterm -> (thm list -> tactic) -> thm
val is_schematic: term -> bool
- val prove_multi: Proof.context -> string list -> term list -> term list ->
+ val prove_common: Proof.context -> int option -> string list -> term list -> term list ->
({prems: thm list, context: Proof.context} -> tactic) -> thm list
val prove_future: Proof.context -> string list -> term list -> term ->
({prems: thm list, context: Proof.context} -> tactic) -> thm
@@ -176,11 +176,12 @@
Term.exists_subterm Term.is_Var t orelse
Term.exists_type (Term.exists_subtype Term.is_TVar) t;
-fun prove_common immediate pri ctxt xs asms props tac =
+fun prove_common ctxt fork_pri xs asms props tac =
let
val thy = Proof_Context.theory_of ctxt;
val schematic = exists is_schematic props;
+ val immediate = is_none fork_pri;
val future = future_enabled 1;
val skip = not immediate andalso not schematic andalso future andalso skip_proofs_enabled ();
@@ -229,7 +230,8 @@
if immediate orelse schematic orelse not future orelse skip then result ()
else
future_result ctxt'
- (Execution.fork {name = "Goal.prove", pos = Position.thread_data (), pri = pri} result)
+ (Execution.fork {name = "Goal.prove", pos = Position.thread_data (), pri = the fork_pri}
+ result)
(Thm.term_of stmt);
in
Conjunction.elim_balanced (length props) res
@@ -238,14 +240,12 @@
|> map Drule.zero_var_indexes
end;
-val prove_multi = prove_common true 0;
+fun prove_future_pri ctxt pri xs asms prop tac =
+ hd (prove_common ctxt (SOME pri) xs asms [prop] tac);
-fun prove_future_pri pri ctxt xs asms prop tac =
- hd (prove_common false pri ctxt xs asms [prop] tac);
+fun prove_future ctxt = prove_future_pri ctxt ~1;
-val prove_future = prove_future_pri ~1;
-
-fun prove ctxt xs asms prop tac = hd (prove_multi ctxt xs asms [prop] tac);
+fun prove ctxt xs asms prop tac = hd (prove_common ctxt NONE xs asms [prop] tac);
fun prove_global_future thy xs asms prop tac =
Drule.export_without_context (prove_future (Proof_Context.init_global thy) xs asms prop tac);
@@ -256,7 +256,7 @@
fun prove_sorry ctxt xs asms prop tac =
if Config.get ctxt quick_and_dirty then
prove ctxt xs asms prop (fn _ => ALLGOALS (Skip_Proof.cheat_tac ctxt))
- else (if future_enabled 1 then prove_future_pri ~2 else prove) ctxt xs asms prop tac;
+ else (if future_enabled 1 then prove_future_pri ctxt ~2 else prove ctxt) xs asms prop tac;
fun prove_sorry_global thy xs asms prop tac =
Drule.export_without_context