Goal.prove_multi is superseded by the fully general Goal.prove_common;
authorwenzelm
Mon Feb 23 14:50:30 2015 +0100 (2015-02-23)
changeset 59564fdc03c8daacc
parent 59563 c422ef7b9fae
child 59565 96e860a17b9a
Goal.prove_multi is superseded by the fully general Goal.prove_common;
NEWS
src/Doc/Implementation/Proof.thy
src/Pure/axclass.ML
src/Pure/goal.ML
     1.1 --- a/NEWS	Mon Feb 23 14:48:40 2015 +0100
     1.2 +++ b/NEWS	Mon Feb 23 14:50:30 2015 +0100
     1.3 @@ -282,6 +282,9 @@
     1.4  * Synchronized.value (ML) is actually synchronized (as in Scala):
     1.5  subtle change of semantics with minimal potential for INCOMPATIBILITY.
     1.6  
     1.7 +* Goal.prove_multi is superseded by the fully general Goal.prove_common,
     1.8 +which also allows to specify a fork priority.
     1.9 +
    1.10  
    1.11  *** System ***
    1.12  
     2.1 --- a/src/Doc/Implementation/Proof.thy	Mon Feb 23 14:48:40 2015 +0100
     2.2 +++ b/src/Doc/Implementation/Proof.thy	Mon Feb 23 14:50:30 2015 +0100
     2.3 @@ -402,7 +402,8 @@
     2.4    \begin{mldecls}
     2.5    @{index_ML Goal.prove: "Proof.context -> string list -> term list -> term ->
     2.6    ({prems: thm list, context: Proof.context} -> tactic) -> thm"} \\
     2.7 -  @{index_ML Goal.prove_multi: "Proof.context -> string list -> term list -> term list ->
     2.8 +  @{index_ML Goal.prove_common: "Proof.context -> int option ->
     2.9 +  string list -> term list -> term list ->
    2.10    ({prems: thm list, context: Proof.context} -> tactic) -> thm list"} \\
    2.11    \end{mldecls}
    2.12    \begin{mldecls}
    2.13 @@ -436,10 +437,22 @@
    2.14    it.  The latter may depend on the local assumptions being presented
    2.15    as facts.  The result is in HHF normal form.
    2.16  
    2.17 -  \item @{ML Goal.prove_multi} is similar to @{ML Goal.prove}, but
    2.18 -  states several conclusions simultaneously.  The goal is encoded by
    2.19 -  means of Pure conjunction; @{ML Goal.conjunction_tac} will turn this
    2.20 -  into a collection of individual subgoals.
    2.21 +  \item @{ML Goal.prove_common}~@{text "ctxt fork_pri"} is the general form
    2.22 +  to state and prove a simultaneous goal statement, where @{ML Goal.prove}
    2.23 +  is a convenient shorthand for the most common application.
    2.24 +
    2.25 +  The given list of simultaneous conclusions is encoded in the goal state by
    2.26 +  means of Pure conjunction: @{ML Goal.conjunction_tac} will turn this into
    2.27 +  a collection of individual subgoals, but note that the original multi-goal
    2.28 +  state is usually required for advanced induction.
    2.29 +
    2.30 +  It is possible to provide an optional priority for a forked proof,
    2.31 +  typically @{ML "SOME ~1"}, while @{ML NONE} means the proof is immediate
    2.32 +  (sequential) as for @{ML Goal.prove}. Note that a forked proof does not
    2.33 +  exhibit any failures in the usual way via exceptions in ML, but
    2.34 +  accumulates error situations under the execution id of the running
    2.35 +  transaction. Thus the system is able to expose error messages ultimately
    2.36 +  to the end-user, even though the subsequent ML code misses them.
    2.37  
    2.38    \item @{ML Obtain.result}~@{text "tac thms ctxt"} eliminates the
    2.39    given facts using a tactic, which results in additional fixed
     3.1 --- a/src/Pure/axclass.ML	Mon Feb 23 14:48:40 2015 +0100
     3.2 +++ b/src/Pure/axclass.ML	Mon Feb 23 14:50:30 2015 +0100
     3.3 @@ -457,7 +457,7 @@
     3.4      val names = map (prefix arity_prefix) (Logic.name_arities arity);
     3.5      val props = Logic.mk_arities arity;
     3.6      val ths =
     3.7 -      Goal.prove_multi ctxt [] [] props
     3.8 +      Goal.prove_common ctxt NONE [] [] props
     3.9        (fn {context, ...} => Goal.precise_conjunction_tac (length props) 1 THEN tac context)
    3.10          handle ERROR msg =>
    3.11            cat_error msg ("The error(s) above occurred while trying to prove type arity " ^
     4.1 --- a/src/Pure/goal.ML	Mon Feb 23 14:48:40 2015 +0100
     4.2 +++ b/src/Pure/goal.ML	Mon Feb 23 14:50:30 2015 +0100
     4.3 @@ -28,7 +28,7 @@
     4.4    val future_result: Proof.context -> thm future -> term -> thm
     4.5    val prove_internal: Proof.context -> cterm list -> cterm -> (thm list -> tactic) -> thm
     4.6    val is_schematic: term -> bool
     4.7 -  val prove_multi: Proof.context -> string list -> term list -> term list ->
     4.8 +  val prove_common: Proof.context -> int option -> string list -> term list -> term list ->
     4.9      ({prems: thm list, context: Proof.context} -> tactic) -> thm list
    4.10    val prove_future: Proof.context -> string list -> term list -> term ->
    4.11      ({prems: thm list, context: Proof.context} -> tactic) -> thm
    4.12 @@ -176,11 +176,12 @@
    4.13    Term.exists_subterm Term.is_Var t orelse
    4.14    Term.exists_type (Term.exists_subtype Term.is_TVar) t;
    4.15  
    4.16 -fun prove_common immediate pri ctxt xs asms props tac =
    4.17 +fun prove_common ctxt fork_pri xs asms props tac =
    4.18    let
    4.19      val thy = Proof_Context.theory_of ctxt;
    4.20  
    4.21      val schematic = exists is_schematic props;
    4.22 +    val immediate = is_none fork_pri;
    4.23      val future = future_enabled 1;
    4.24      val skip = not immediate andalso not schematic andalso future andalso skip_proofs_enabled ();
    4.25  
    4.26 @@ -229,7 +230,8 @@
    4.27        if immediate orelse schematic orelse not future orelse skip then result ()
    4.28        else
    4.29          future_result ctxt'
    4.30 -          (Execution.fork {name = "Goal.prove", pos = Position.thread_data (), pri = pri} result)
    4.31 +          (Execution.fork {name = "Goal.prove", pos = Position.thread_data (), pri = the fork_pri}
    4.32 +            result)
    4.33            (Thm.term_of stmt);
    4.34    in
    4.35      Conjunction.elim_balanced (length props) res
    4.36 @@ -238,14 +240,12 @@
    4.37      |> map Drule.zero_var_indexes
    4.38    end;
    4.39  
    4.40 -val prove_multi = prove_common true 0;
    4.41 +fun prove_future_pri ctxt pri xs asms prop tac =
    4.42 +  hd (prove_common ctxt (SOME pri) xs asms [prop] tac);
    4.43  
    4.44 -fun prove_future_pri pri ctxt xs asms prop tac =
    4.45 -  hd (prove_common false pri ctxt xs asms [prop] tac);
    4.46 +fun prove_future ctxt = prove_future_pri ctxt ~1;
    4.47  
    4.48 -val prove_future = prove_future_pri ~1;
    4.49 -
    4.50 -fun prove ctxt xs asms prop tac = hd (prove_multi ctxt xs asms [prop] tac);
    4.51 +fun prove ctxt xs asms prop tac = hd (prove_common ctxt NONE xs asms [prop] tac);
    4.52  
    4.53  fun prove_global_future thy xs asms prop tac =
    4.54    Drule.export_without_context (prove_future (Proof_Context.init_global thy) xs asms prop tac);
    4.55 @@ -256,7 +256,7 @@
    4.56  fun prove_sorry ctxt xs asms prop tac =
    4.57    if Config.get ctxt quick_and_dirty then
    4.58      prove ctxt xs asms prop (fn _ => ALLGOALS (Skip_Proof.cheat_tac ctxt))
    4.59 -  else (if future_enabled 1 then prove_future_pri ~2 else prove) ctxt xs asms prop tac;
    4.60 +  else (if future_enabled 1 then prove_future_pri ctxt ~2 else prove ctxt) xs asms prop tac;
    4.61  
    4.62  fun prove_sorry_global thy xs asms prop tac =
    4.63    Drule.export_without_context