# HG changeset patch
# User wenzelm
# Date 1250029561 -7200
# Node ID 9b74d0339c443619fb42b9411bd0edb19f384607
# Parent  40d952bd6d47babaabd58600680f28f28e190912
added PARALLEL_CHOICE, PARALLEL_GOALS;

diff -r 40d952bd6d47 -r 9b74d0339c44 NEWS
--- a/NEWS	Tue Aug 11 20:40:02 2009 +0200
+++ b/NEWS	Wed Aug 12 00:26:01 2009 +0200
@@ -148,6 +148,9 @@
 
 *** ML ***
 
+* PARALLEL_CHOICE and PARALLEL_GOALS provide basic support for
+parallel tactical reasoning.
+
 * Tactical FOCUS is similar to SUBPROOF, but allows the body tactic to
 introduce new subgoals and schematic variables.  FOCUS_PARAMS is
 similar, but focuses on the parameter prefix only, leaving subgoal
diff -r 40d952bd6d47 -r 9b74d0339c44 src/Pure/goal.ML
--- a/src/Pure/goal.ML	Tue Aug 11 20:40:02 2009 +0200
+++ b/src/Pure/goal.ML	Wed Aug 12 00:26:01 2009 +0200
@@ -10,6 +10,8 @@
   val SELECT_GOAL: tactic -> int -> tactic
   val CONJUNCTS: tactic -> int -> tactic
   val PRECISE_CONJUNCTS: int -> tactic -> int -> tactic
+  val PARALLEL_CHOICE: tactic list -> tactic
+  val PARALLEL_GOALS: tactic -> tactic
 end;
 
 signature GOAL =
@@ -288,7 +290,34 @@
       Tactic.etac (MetaSimplifier.norm_hhf (Thm.trivial R)) THEN_ALL_NEW assume_tac);
   in fold_rev (curry op APPEND') tacs (K no_tac) i end);
 
+
+(* parallel tacticals *)
+
+(*parallel choice of single results*)
+fun PARALLEL_CHOICE tacs st =
+  (case Par_List.get_some (fn tac => SINGLE tac st) tacs of
+    NONE => Seq.empty
+  | SOME st' => Seq.single st');
+
+(*parallel refinement of non-schematic goal by single results*)
+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]);
+
+    exception FAILED;
+    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;
+
 end;
 
-structure BasicGoal: BASIC_GOAL = Goal;
-open BasicGoal;
+structure Basic_Goal: BASIC_GOAL = Goal;
+open Basic_Goal;