--- a/NEWS Sat Apr 16 21:45:47 2011 +0200
+++ b/NEWS Sat Apr 16 22:21:34 2011 +0200
@@ -112,6 +112,9 @@
* Typed print translation: discontinued show_sorts argument, which is
already available via context of "advanced" translation.
+* Refined PARALLEL_GOALS tactical: degrades gracefully for schematic
+goal states; body tactic needs to address all subgoals uniformly.
+
New in Isabelle2011 (January 2011)
--- a/src/HOL/Boogie/Tools/boogie_tactics.ML Sat Apr 16 21:45:47 2011 +0200
+++ b/src/HOL/Boogie/Tools/boogie_tactics.ML Sat Apr 16 22:21:34 2011 +0200
@@ -37,7 +37,7 @@
THEN' SMT_Solver.smt_tac ctxt (Boogie_Axioms.get ctxt @ boogie_rules @ rules)
fun boogie_all_tac ctxt rules =
- PARALLEL_GOALS (HEADGOAL (boogie_tac ctxt rules))
+ PARALLEL_GOALS (ALLGOALS (boogie_tac ctxt rules))
fun boogie_method all =
Scan.optional Attrib.thms [] >> (fn thms => fn ctxt => METHOD (fn facts =>
--- a/src/Pure/goal.ML Sat Apr 16 21:45:47 2011 +0200
+++ b/src/Pure/goal.ML Sat Apr 16 22:21:34 2011 +0200
@@ -344,21 +344,22 @@
(*parallel refinement of non-schematic goal by single results*)
exception FAILED of unit;
-fun PARALLEL_GOALS tac st =
- let
- val st0 = Thm.adjust_maxidx_thm ~1 st;
- val _ = Thm.maxidx_of st0 >= 0 andalso
- raise THM ("PARALLEL_GOALS: schematic goal state", 0, [st]);
+fun PARALLEL_GOALS tac =
+ Thm.adjust_maxidx_thm ~1 #>
+ (fn st =>
+ if not (future_enabled ()) orelse Thm.maxidx_of st >= 0 orelse Thm.nprems_of st <= 1
+ then DETERM tac st
+ else
+ let
+ fun try_tac g =
+ (case SINGLE tac g of
+ NONE => raise FAILED ()
+ | SOME g' => g');
- fun try_tac g =
- (case SINGLE tac g of
- NONE => raise FAILED ()
- | SOME g' => g');
-
- val goals = Drule.strip_imp_prems (Thm.cprop_of st0);
- val results = Par_List.map (try_tac o init) goals;
- in ALLGOALS (fn i => retrofit i 1 (nth results (i - 1))) st0 end
- handle FAILED () => Seq.empty;
+ val goals = Drule.strip_imp_prems (Thm.cprop_of st);
+ val results = Par_List.map (try_tac o init) goals;
+ in ALLGOALS (fn i => retrofit i 1 (nth results (i - 1))) st end
+ handle FAILED () => Seq.empty);
end;