1.1 --- a/NEWS	Tue Aug 11 20:40:02 2009 +0200
     1.2 +++ b/NEWS	Wed Aug 12 00:26:01 2009 +0200
     1.3 @@ -148,6 +148,9 @@
     1.4  
     1.5  *** ML ***
     1.6  
     1.7 +* PARALLEL_CHOICE and PARALLEL_GOALS provide basic support for
     1.8 +parallel tactical reasoning.
     1.9 +
    1.10  * Tactical FOCUS is similar to SUBPROOF, but allows the body tactic to
    1.11  introduce new subgoals and schematic variables.  FOCUS_PARAMS is
    1.12  similar, but focuses on the parameter prefix only, leaving subgoal

     2.1 --- a/src/Pure/goal.ML	Tue Aug 11 20:40:02 2009 +0200
     2.2 +++ b/src/Pure/goal.ML	Wed Aug 12 00:26:01 2009 +0200
     2.3 @@ -10,6 +10,8 @@
     2.4    val SELECT_GOAL: tactic -> int -> tactic
     2.5    val CONJUNCTS: tactic -> int -> tactic
     2.6    val PRECISE_CONJUNCTS: int -> tactic -> int -> tactic
     2.7 +  val PARALLEL_CHOICE: tactic list -> tactic
     2.8 +  val PARALLEL_GOALS: tactic -> tactic
     2.9  end;
    2.10  
    2.11  signature GOAL =
    2.12 @@ -288,7 +290,34 @@
    2.13        Tactic.etac (MetaSimplifier.norm_hhf (Thm.trivial R)) THEN_ALL_NEW assume_tac);
    2.14    in fold_rev (curry op APPEND') tacs (K no_tac) i end);
    2.15  
    2.16 +
    2.17 +(* parallel tacticals *)
    2.18 +
    2.19 +(*parallel choice of single results*)
    2.20 +fun PARALLEL_CHOICE tacs st =
    2.21 +  (case Par_List.get_some (fn tac => SINGLE tac st) tacs of
    2.22 +    NONE => Seq.empty
    2.23 +  | SOME st' => Seq.single st');
    2.24 +
    2.25 +(*parallel refinement of non-schematic goal by single results*)
    2.26 +fun PARALLEL_GOALS tac st =
    2.27 +  let
    2.28 +    val st0 = Thm.adjust_maxidx_thm ~1 st;
    2.29 +    val _ = Thm.maxidx_of st0 >= 0 andalso
    2.30 +      raise THM ("PARALLEL_GOALS: schematic goal state", 0, [st]);
    2.31 +
    2.32 +    exception FAILED;
    2.33 +    fun try_tac g =
    2.34 +      (case SINGLE tac g of
    2.35 +        NONE => raise FAILED
    2.36 +      | SOME g' => g');
    2.37 +
    2.38 +    val goals = Drule.strip_imp_prems (Thm.cprop_of st0);
    2.39 +    val results = Par_List.map (try_tac o init) goals;
    2.40 +  in ALLGOALS (fn i => retrofit i 1 (nth results (i - 1))) st0 end
    2.41 +  handle FAILED => Seq.empty;
    2.42 +
    2.43  end;
    2.44  
    2.45 -structure BasicGoal: BASIC_GOAL = Goal;
    2.46 -open BasicGoal;
    2.47 +structure Basic_Goal: BASIC_GOAL = Goal;
    2.48 +open Basic_Goal;