# HG changeset patch # User wenzelm # Date 1424699430 -3600 # Node ID fdc03c8daaccacad6537c01d2e9a8a6ca1a85528 # Parent c422ef7b9fae33f4a2bc1cb1a806c7412ad01edf Goal.prove_multi is superseded by the fully general Goal.prove_common; diff -r c422ef7b9fae -r fdc03c8daacc NEWS --- 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 *** diff -r c422ef7b9fae -r fdc03c8daacc src/Doc/Implementation/Proof.thy --- 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 diff -r c422ef7b9fae -r fdc03c8daacc src/Pure/axclass.ML --- 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 " ^ diff -r c422ef7b9fae -r fdc03c8daacc src/Pure/goal.ML --- 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