src/Pure/goal.ML
changeset 32365 9b74d0339c44
parent 32255 d302f1c9e356
child 32738 15bb09ca0378
     1.1 --- a/src/Pure/goal.ML	Tue Aug 11 20:40:02 2009 +0200
     1.2 +++ b/src/Pure/goal.ML	Wed Aug 12 00:26:01 2009 +0200
     1.3 @@ -10,6 +10,8 @@
     1.4    val SELECT_GOAL: tactic -> int -> tactic
     1.5    val CONJUNCTS: tactic -> int -> tactic
     1.6    val PRECISE_CONJUNCTS: int -> tactic -> int -> tactic
     1.7 +  val PARALLEL_CHOICE: tactic list -> tactic
     1.8 +  val PARALLEL_GOALS: tactic -> tactic
     1.9  end;
    1.10  
    1.11  signature GOAL =
    1.12 @@ -288,7 +290,34 @@
    1.13        Tactic.etac (MetaSimplifier.norm_hhf (Thm.trivial R)) THEN_ALL_NEW assume_tac);
    1.14    in fold_rev (curry op APPEND') tacs (K no_tac) i end);
    1.15  
    1.16 +
    1.17 +(* parallel tacticals *)
    1.18 +
    1.19 +(*parallel choice of single results*)
    1.20 +fun PARALLEL_CHOICE tacs st =
    1.21 +  (case Par_List.get_some (fn tac => SINGLE tac st) tacs of
    1.22 +    NONE => Seq.empty
    1.23 +  | SOME st' => Seq.single st');
    1.24 +
    1.25 +(*parallel refinement of non-schematic goal by single results*)
    1.26 +fun PARALLEL_GOALS tac st =
    1.27 +  let
    1.28 +    val st0 = Thm.adjust_maxidx_thm ~1 st;
    1.29 +    val _ = Thm.maxidx_of st0 >= 0 andalso
    1.30 +      raise THM ("PARALLEL_GOALS: schematic goal state", 0, [st]);
    1.31 +
    1.32 +    exception FAILED;
    1.33 +    fun try_tac g =
    1.34 +      (case SINGLE tac g of
    1.35 +        NONE => raise FAILED
    1.36 +      | SOME g' => g');
    1.37 +
    1.38 +    val goals = Drule.strip_imp_prems (Thm.cprop_of st0);
    1.39 +    val results = Par_List.map (try_tac o init) goals;
    1.40 +  in ALLGOALS (fn i => retrofit i 1 (nth results (i - 1))) st0 end
    1.41 +  handle FAILED => Seq.empty;
    1.42 +
    1.43  end;
    1.44  
    1.45 -structure BasicGoal: BASIC_GOAL = Goal;
    1.46 -open BasicGoal;
    1.47 +structure Basic_Goal: BASIC_GOAL = Goal;
    1.48 +open Basic_Goal;