src/Pure/goal.ML
changeset 52461 ef4c16887f83
parent 52458 210bca64b894
child 52499 812215680f6d
     1.1 --- a/src/Pure/goal.ML	Wed Jun 26 22:18:06 2013 +0200
     1.2 +++ b/src/Pure/goal.ML	Thu Jun 27 10:08:41 2013 +0200
     1.3 @@ -51,8 +51,6 @@
     1.4      ({prems: thm list, context: Proof.context} -> tactic) -> thm
     1.5    val prove_sorry_global: theory -> string list -> term list -> term ->
     1.6      ({prems: thm list, context: Proof.context} -> tactic) -> thm
     1.7 -  val extract: int -> int -> thm -> thm Seq.seq
     1.8 -  val retrofit: int -> int -> thm -> thm -> thm Seq.seq
     1.9    val restrict: int -> int -> thm -> thm
    1.10    val unrestrict: int -> thm -> thm
    1.11    val conjunction_tac: int -> tactic
    1.12 @@ -349,22 +347,6 @@
    1.13  
    1.14  (** goal structure **)
    1.15  
    1.16 -(* nested goals *)
    1.17 -
    1.18 -fun extract i n st =
    1.19 -  (if i < 1 orelse n < 1 orelse i + n - 1 > Thm.nprems_of st then Seq.empty
    1.20 -   else if n = 1 then Seq.single (Thm.cprem_of st i)
    1.21 -   else
    1.22 -     Seq.single (Conjunction.mk_conjunction_balanced (map (Thm.cprem_of st) (i upto i + n - 1))))
    1.23 -  |> Seq.map (Thm.adjust_maxidx_cterm ~1 #> init);
    1.24 -
    1.25 -fun retrofit i n st' st =
    1.26 -  (if n = 1 then st
    1.27 -   else st |> Drule.with_subgoal i (Conjunction.uncurry_balanced n))
    1.28 -  |> Thm.bicompose {flatten = false, match = false, incremented = false}
    1.29 -      (false, conclude st', Thm.nprems_of st') i;
    1.30 -
    1.31 -
    1.32  (* rearrange subgoals *)
    1.33  
    1.34  fun restrict i n st =
    1.35 @@ -439,16 +421,30 @@
    1.36    in fold_rev (curry op APPEND') tacs (K no_tac) i end);
    1.37  
    1.38  
    1.39 -(* parallel tacticals *)
    1.40 +
    1.41 +(** parallel tacticals **)
    1.42  
    1.43 -(*parallel choice of single results*)
    1.44 +(* parallel choice of single results *)
    1.45 +
    1.46  fun PARALLEL_CHOICE tacs st =
    1.47    (case Par_List.get_some (fn tac => SINGLE tac st) tacs of
    1.48      NONE => Seq.empty
    1.49    | SOME st' => Seq.single st');
    1.50  
    1.51 -(*parallel refinement of non-schematic goal by single results*)
    1.52 +
    1.53 +(* parallel refinement of non-schematic goal by single results *)
    1.54 +
    1.55 +local
    1.56 +
    1.57  exception FAILED of unit;
    1.58 +
    1.59 +fun retrofit st' =
    1.60 +  rotate_prems ~1 #>
    1.61 +  Thm.bicompose {flatten = false, match = false, incremented = false}
    1.62 +      (false, conclude st', Thm.nprems_of st') 1;
    1.63 +
    1.64 +in
    1.65 +
    1.66  fun PARALLEL_GOALS tac =
    1.67    Thm.adjust_maxidx_thm ~1 #>
    1.68    (fn st =>
    1.69 @@ -463,10 +459,12 @@
    1.70  
    1.71          val goals = Drule.strip_imp_prems (Thm.cprop_of st);
    1.72          val results = Par_List.map (try_tac o init) goals;
    1.73 -      in ALLGOALS (fn i => retrofit i 1 (nth results (i - 1))) st end
    1.74 +      in EVERY (map retrofit (rev results)) st end
    1.75        handle FAILED () => Seq.empty);
    1.76  
    1.77  end;
    1.78  
    1.79 +end;
    1.80 +
    1.81  structure Basic_Goal: BASIC_GOAL = Goal;
    1.82  open Basic_Goal;