# HG changeset patch # User wenzelm # Date 1372320521 -7200 # Node ID ef4c16887f8342ace8fca003437a9e578e92f408 # Parent 365ca7cb0d812adbb6d7b86913de6f8da6e058a4 more scalable PARALLEL_GOALS, using more elementary retrofit; tuned signature; diff -r 365ca7cb0d81 -r ef4c16887f83 src/Pure/goal.ML --- a/src/Pure/goal.ML Wed Jun 26 22:18:06 2013 +0200 +++ b/src/Pure/goal.ML Thu Jun 27 10:08:41 2013 +0200 @@ -51,8 +51,6 @@ ({prems: thm list, context: Proof.context} -> tactic) -> thm val prove_sorry_global: theory -> string list -> term list -> term -> ({prems: thm list, context: Proof.context} -> tactic) -> thm - val extract: int -> int -> thm -> thm Seq.seq - val retrofit: int -> int -> thm -> thm -> thm Seq.seq val restrict: int -> int -> thm -> thm val unrestrict: int -> thm -> thm val conjunction_tac: int -> tactic @@ -349,22 +347,6 @@ (** goal structure **) -(* nested goals *) - -fun extract i n st = - (if i < 1 orelse n < 1 orelse i + n - 1 > Thm.nprems_of st then Seq.empty - else if n = 1 then Seq.single (Thm.cprem_of st i) - else - Seq.single (Conjunction.mk_conjunction_balanced (map (Thm.cprem_of st) (i upto i + n - 1)))) - |> Seq.map (Thm.adjust_maxidx_cterm ~1 #> init); - -fun retrofit i n st' st = - (if n = 1 then st - else st |> Drule.with_subgoal i (Conjunction.uncurry_balanced n)) - |> Thm.bicompose {flatten = false, match = false, incremented = false} - (false, conclude st', Thm.nprems_of st') i; - - (* rearrange subgoals *) fun restrict i n st = @@ -439,16 +421,30 @@ in fold_rev (curry op APPEND') tacs (K no_tac) i end); -(* parallel tacticals *) + +(** parallel tacticals **) -(*parallel choice of single results*) +(* 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*) + +(* parallel refinement of non-schematic goal by single results *) + +local + exception FAILED of unit; + +fun retrofit st' = + rotate_prems ~1 #> + Thm.bicompose {flatten = false, match = false, incremented = false} + (false, conclude st', Thm.nprems_of st') 1; + +in + fun PARALLEL_GOALS tac = Thm.adjust_maxidx_thm ~1 #> (fn st => @@ -463,10 +459,12 @@ 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 + in EVERY (map retrofit (rev results)) st end handle FAILED () => Seq.empty); end; +end; + structure Basic_Goal: BASIC_GOAL = Goal; open Basic_Goal;