# HG changeset patch # User wenzelm # Date 1408465289 -7200 # Node ID 568840962230b1a3a5de7b1c2dcab9f26653317e # Parent 52181f7b4468922ee72dbae7b3dfbd0288ae9598# Parent 987c848d509b9d1400728fbd10d1a7a66903af17 merged diff -r 52181f7b4468 -r 568840962230 NEWS --- a/NEWS Tue Aug 19 16:46:33 2014 +0200 +++ b/NEWS Tue Aug 19 18:21:29 2014 +0200 @@ -52,6 +52,12 @@ min +*** ML *** + +* Tactical PARALLEL_ALLGOALS is the most common way to refer to +PARALLEL_GOALS. + + New in Isabelle2014 (August 2014) --------------------------------- diff -r 52181f7b4468 -r 568840962230 src/HOL/Fun_Def.thy --- a/src/HOL/Fun_Def.thy Tue Aug 19 16:46:33 2014 +0200 +++ b/src/HOL/Fun_Def.thy Tue Aug 19 18:21:29 2014 +0200 @@ -103,7 +103,7 @@ ML_file "Tools/Function/induction_schema.ML" method_setup induction_schema = {* - Scan.succeed (RAW_METHOD o Induction_Schema.induction_schema_tac) + Scan.succeed (NO_CASES oo Induction_Schema.induction_schema_tac) *} "prove an induction principle" setup {* diff -r 52181f7b4468 -r 568840962230 src/HOL/Nominal/nominal_induct.ML --- a/src/HOL/Nominal/nominal_induct.ML Tue Aug 19 16:46:33 2014 +0200 +++ b/src/HOL/Nominal/nominal_induct.ML Tue Aug 19 18:21:29 2014 +0200 @@ -172,9 +172,8 @@ Scan.lift (Args.mode Induct.no_simpN) -- (Parse.and_list' (Scan.repeat (unless_more_args def_inst)) -- avoiding -- fixing -- rule_spec) >> - (fn (no_simp, (((x, y), z), w)) => fn ctxt => - RAW_METHOD_CASES (fn facts => - HEADGOAL (nominal_induct_tac ctxt (not no_simp) x y z w facts))); + (fn (no_simp, (((x, y), z), w)) => fn ctxt => fn facts => + HEADGOAL (nominal_induct_tac ctxt (not no_simp) x y z w facts)); end; diff -r 52181f7b4468 -r 568840962230 src/HOL/Nominal/nominal_primrec.ML --- a/src/HOL/Nominal/nominal_primrec.ML Tue Aug 19 16:46:33 2014 +0200 +++ b/src/HOL/Nominal/nominal_primrec.ML Tue Aug 19 18:21:29 2014 +0200 @@ -373,9 +373,10 @@ |> snd end) [goals] |> - Proof.apply (Method.Basic (fn ctxt => RAW_METHOD (fn _ => - rewrite_goals_tac ctxt defs_thms THEN - compose_tac (false, rule, length rule_prems) 1))) |> + Proof.apply (Method.Basic (fn ctxt => fn _ => + NO_CASES + (rewrite_goals_tac ctxt defs_thms THEN + compose_tac (false, rule, length rule_prems) 1))) |> Seq.hd end; diff -r 52181f7b4468 -r 568840962230 src/HOL/Tools/coinduction.ML --- a/src/HOL/Tools/coinduction.ML Tue Aug 19 16:46:33 2014 +0200 +++ b/src/HOL/Tools/coinduction.ML Tue Aug 19 18:21:29 2014 +0200 @@ -149,9 +149,8 @@ val setup = Method.setup @{binding coinduction} (arbitrary -- Scan.option coinduct_rule >> - (fn (arbitrary, opt_rule) => fn ctxt => - RAW_METHOD_CASES (fn facts => - Seq.DETERM (coinduction_tac ctxt arbitrary opt_rule facts)))) + (fn (arbitrary, opt_rule) => fn ctxt => fn facts => + Seq.DETERM (coinduction_tac ctxt arbitrary opt_rule facts))) "coinduction on types or predicates/sets"; end; diff -r 52181f7b4468 -r 568840962230 src/HOL/Tools/try0.ML --- a/src/HOL/Tools/try0.ML Tue Aug 19 16:46:33 2014 +0200 +++ b/src/HOL/Tools/try0.ML Tue Aug 19 18:21:29 2014 +0200 @@ -59,7 +59,7 @@ parse_method #> Method.method_cmd ctxt #> Method.Basic - #> (fn m => Method.Select_Goals (Method.no_combinator_info, 1, m)) + #> (fn m => Method.Combinator (Method.no_combinator_info, Method.Select_Goals 1, [m])) #> Proof.refine; fun add_attr_text (NONE, _) s = s diff -r 52181f7b4468 -r 568840962230 src/Provers/clasimp.ML --- a/src/Provers/clasimp.ML Tue Aug 19 16:46:33 2014 +0200 +++ b/src/Provers/clasimp.ML Tue Aug 19 18:21:29 2014 +0200 @@ -146,7 +146,7 @@ ORELSE' (CHANGED o nodup_depth_tac (addss ctxt) n); (* slower but more general *) in - PARALLEL_GOALS (ALLGOALS (Simplifier.asm_full_simp_tac ctxt)) THEN + PARALLEL_ALLGOALS (Simplifier.asm_full_simp_tac ctxt) THEN TRY (Classical.safe_tac ctxt) THEN REPEAT_DETERM (FIRSTGOAL main_tac) THEN TRY (Classical.safe_tac (addSss ctxt)) THEN diff -r 52181f7b4468 -r 568840962230 src/Pure/Isar/element.ML --- a/src/Pure/Isar/element.ML Tue Aug 19 16:46:33 2014 +0200 +++ b/src/Pure/Isar/element.ML Tue Aug 19 18:21:29 2014 +0200 @@ -270,8 +270,8 @@ local val refine_witness = - Proof.refine (Method.Basic (K (RAW_METHOD - (K (ALLGOALS (CONJUNCTS (ALLGOALS (CONJUNCTS (TRYALL (rtac Drule.protectI)))))))))); + Proof.refine (Method.Basic (K (NO_CASES o + K (ALLGOALS (CONJUNCTS (ALLGOALS (CONJUNCTS (TRYALL (rtac Drule.protectI))))))))); fun gen_witness_proof proof after_qed wit_propss eq_props = let diff -r 52181f7b4468 -r 568840962230 src/Pure/Isar/method.ML --- a/src/Pure/Isar/method.ML Tue Aug 19 16:46:33 2014 +0200 +++ b/src/Pure/Isar/method.ML Tue Aug 19 18:21:29 2014 +0200 @@ -6,10 +6,7 @@ signature METHOD = sig - type method - val apply: (Proof.context -> method) -> Proof.context -> thm list -> cases_tactic - val RAW_METHOD_CASES: (thm list -> cases_tactic) -> method - val RAW_METHOD: (thm list -> tactic) -> method + type method = thm list -> cases_tactic val METHOD_CASES: (thm list -> cases_tactic) -> method val METHOD: (thm list -> tactic) -> method val fail: method @@ -47,14 +44,12 @@ type src = Args.src type combinator_info val no_combinator_info: combinator_info + datatype combinator = Then | Orelse | Try | Repeat1 | Select_Goals of int datatype text = Source of src | Basic of Proof.context -> method | - Then of combinator_info * text list | - Orelse of combinator_info * text list | - Try of combinator_info * text | - Repeat1 of combinator_info * text | - Select_Goals of combinator_info * int * text + Combinator of combinator_info * combinator * text list + val map_source: (src -> src) -> text -> text val primitive_text: (Proof.context -> thm -> thm) -> text val succeed_text: text val default_text: text @@ -64,14 +59,16 @@ val finish_text: text option * bool -> text val print_methods: Proof.context -> unit val check_name: Proof.context -> xstring * Position.T -> string - val method: Proof.context -> src -> Proof.context -> method - val method_cmd: Proof.context -> src -> Proof.context -> method val method_syntax: (Proof.context -> method) context_parser -> Args.src -> Proof.context -> method val setup: binding -> (Proof.context -> method) context_parser -> string -> theory -> theory val local_setup: binding -> (Proof.context -> method) context_parser -> string -> local_theory -> local_theory val method_setup: bstring * Position.T -> Symbol_Pos.source -> string -> local_theory -> local_theory + val method: Proof.context -> src -> Proof.context -> method + val method_closure: Proof.context -> src -> src + val method_cmd: Proof.context -> src -> Proof.context -> method + val evaluate: text -> Proof.context -> method type modifier = (Proof.context -> Proof.context) * attribute val section: modifier parser list -> thm list context_parser val sections: modifier parser list -> thm list list context_parser @@ -88,20 +85,12 @@ (** proof methods **) -(* datatype method *) - -datatype method = Meth of thm list -> cases_tactic; - -fun apply meth ctxt = let val Meth m = meth ctxt in m end; +(* method *) -val RAW_METHOD_CASES = Meth; - -fun RAW_METHOD tac = RAW_METHOD_CASES (NO_CASES o tac); +type method = thm list -> cases_tactic; -fun METHOD_CASES tac = RAW_METHOD_CASES (fn facts => - Seq.THEN (ALLGOALS Goal.conjunction_tac, tac facts)); - -fun METHOD tac = RAW_METHOD (fn facts => ALLGOALS Goal.conjunction_tac THEN tac facts); +fun METHOD_CASES tac facts = Seq.THEN (ALLGOALS Goal.conjunction_tac, tac facts); +fun METHOD tac facts = NO_CASES (ALLGOALS Goal.conjunction_tac THEN tac facts); val fail = METHOD (K no_tac); val succeed = METHOD (K all_tac); @@ -154,7 +143,7 @@ fun atomize false ctxt = SIMPLE_METHOD' (CHANGED_PROP o Object_Logic.atomize_prems_tac ctxt) | atomize true ctxt = - RAW_METHOD (K (HEADGOAL (CHANGED_PROP o Object_Logic.full_atomize_tac ctxt))); + NO_CASES o K (HEADGOAL (CHANGED_PROP o Object_Logic.full_atomize_tac ctxt)); (* this -- resolve facts directly *) @@ -277,7 +266,7 @@ in Context.setmp_thread_data (SOME (Context.Proof ctxt)) (ML_Tactic.get ctxt') end; fun tactic source ctxt = METHOD (ml_tactic source ctxt); -fun raw_tactic source ctxt = RAW_METHOD (ml_tactic source ctxt); +fun raw_tactic source ctxt = NO_CASES o ml_tactic source ctxt; @@ -291,14 +280,16 @@ fun combinator_info keywords = Combinator_Info {keywords = keywords}; val no_combinator_info = combinator_info []; +datatype combinator = Then | Orelse | Try | Repeat1 | Select_Goals of int; + datatype text = Source of src | Basic of Proof.context -> method | - Then of combinator_info * text list | - Orelse of combinator_info * text list | - Try of combinator_info * text | - Repeat1 of combinator_info * text | - Select_Goals of combinator_info * int * text; + Combinator of combinator_info * combinator * text list; + +fun map_source f (Source src) = Source (f src) + | map_source _ (Basic meth) = Basic meth + | map_source f (Combinator (info, comb, txts)) = Combinator (info, comb, map (map_source f) txts); fun primitive_text r = Basic (SIMPLE_METHOD o PRIMITIVE o r); val succeed_text = Basic (K succeed); @@ -308,7 +299,8 @@ fun sorry_text int = Basic (fn ctxt => cheating ctxt int); fun finish_text (NONE, immed) = Basic (finish immed) - | finish_text (SOME txt, immed) = Then (no_combinator_info, [txt, Basic (finish immed)]); + | finish_text (SOME txt, immed) = + Combinator (no_combinator_info, Then, [txt, Basic (finish immed)]); (* method definitions *) @@ -365,23 +357,6 @@ fun check_src ctxt src = Args.check_src ctxt (get_methods ctxt) src; -(* get methods *) - -fun method ctxt = - let val table = get_methods ctxt - in fn src => #1 (Name_Space.get table (#1 (Args.name_of_src src))) src end; - -fun method_closure ctxt0 src0 = - let - val (src1, meth) = check_src ctxt0 src0; - val src2 = Args.init_assignable src1; - val ctxt = Context_Position.not_really ctxt0; - val _ = Seq.pull (apply (method ctxt src2) ctxt [] (Goal.protect 0 Drule.dummy_thm)); - in Args.closure src2 end; - -fun method_cmd ctxt = method ctxt o method_closure ctxt; - - (* method setup *) fun method_syntax scan src ctxt : method = @@ -400,6 +375,67 @@ |> Context.proof_map; +(* prepare methods *) + +fun method ctxt = + let val table = get_methods ctxt + in fn src => #1 (Name_Space.get table (#1 (Args.name_of_src src))) src end; + +fun method_closure ctxt0 src0 = + let + val (src1, meth) = check_src ctxt0 src0; + val src2 = Args.init_assignable src1; + val ctxt = Context_Position.not_really ctxt0; + val _ = Seq.pull (method ctxt src2 ctxt [] (Goal.protect 0 Drule.dummy_thm)); + in Args.closure src2 end; + +fun method_cmd ctxt = method ctxt o method_closure ctxt; + + +(* evaluate method text *) + +local + +fun APPEND_CASES (meth: cases_tactic) (cases, st) = + meth st |> Seq.map (fn (cases', st') => (cases @ cases', st')); + +fun BYPASS_CASES (tac: tactic) (cases, st) = + tac st |> Seq.map (pair cases); + +val op THEN = Seq.THEN; + +fun SELECT_GOALS n method = + BYPASS_CASES + (ALLGOALS Goal.conjunction_tac THEN PRIMITIVE (Goal.restrict 1 n) THEN Goal.conjunction_tac 1) + THEN method + THEN BYPASS_CASES (PRIMITIVE (Goal.unrestrict 1)); + +fun COMBINATOR1 comb [meth] = comb meth + | COMBINATOR1 _ _ = raise Fail "Method combinator requires exactly one argument"; + +fun combinator Then = Seq.EVERY + | combinator Orelse = Seq.FIRST + | combinator Try = COMBINATOR1 Seq.TRY + | combinator Repeat1 = COMBINATOR1 Seq.REPEAT1 + | combinator (Select_Goals n) = COMBINATOR1 (SELECT_GOALS n); + +in + +fun evaluate text ctxt = + let + fun eval (Basic meth) = APPEND_CASES o meth ctxt + | eval (Source src) = APPEND_CASES o method_cmd ctxt src ctxt + | eval (Combinator (_, c, txts)) = + let + val comb = combinator c; + val meths = map eval txts; + in fn facts => comb (map (fn meth => meth facts) meths) end; + val meth = eval text; + in fn facts => fn st => meth facts ([], st) end; + +end; + + (** concrete syntax **) @@ -446,16 +482,8 @@ fun keyword_positions (Source _) = [] | keyword_positions (Basic _) = [] - | keyword_positions (Then (Combinator_Info {keywords}, texts)) = - keywords @ maps keyword_positions texts - | keyword_positions (Orelse (Combinator_Info {keywords}, texts)) = - keywords @ maps keyword_positions texts - | keyword_positions (Try (Combinator_Info {keywords}, text)) = - keywords @ keyword_positions text - | keyword_positions (Repeat1 (Combinator_Info {keywords}, text)) = - keywords @ keyword_positions text - | keyword_positions (Select_Goals (Combinator_Info {keywords}, _, text)) = - keywords @ keyword_positions text; + | keyword_positions (Combinator (Combinator_Info {keywords}, _, texts)) = + keywords @ maps keyword_positions texts; in @@ -483,23 +511,23 @@ Parse.$$$ "(" |-- Parse.!!! (meth0 --| Parse.$$$ ")")) x and meth3 x = (meth4 -- Parse.position (Parse.$$$ "?") - >> (fn (m, (_, pos)) => Try (combinator_info [pos], m)) || + >> (fn (m, (_, pos)) => Combinator (combinator_info [pos], Try, [m])) || meth4 -- Parse.position (Parse.$$$ "+") - >> (fn (m, (_, pos)) => Repeat1 (combinator_info [pos], m)) || + >> (fn (m, (_, pos)) => Combinator (combinator_info [pos], Repeat1, [m])) || meth4 -- (Parse.position (Parse.$$$ "[") -- Scan.optional Parse.nat 1 -- Parse.position (Parse.$$$ "]")) >> (fn (m, (((_, pos1), n), (_, pos2))) => - Select_Goals (combinator_info [pos1, pos2], n, m)) || + Combinator (combinator_info [pos1, pos2], Select_Goals n, [m])) || meth4) x and meth2 x = (Parse.position Parse.xname -- Parse.args1 is_symid_meth >> (Source o uncurry Args.src) || meth3) x and meth1 x = (Parse.enum1_positions "," meth2 - >> (fn ([m], _) => m | (ms, ps) => Then (combinator_info ps, ms))) x + >> (fn ([m], _) => m | (ms, ps) => Combinator (combinator_info ps, Then, ms))) x and meth0 x = (Parse.enum1_positions "|" meth1 - >> (fn ([m], _) => m | (ms, ps) => Orelse (combinator_info ps, ms))) x; + >> (fn ([m], _) => m | (ms, ps) => Combinator (combinator_info ps, Orelse, ms))) x; in @@ -553,8 +581,6 @@ end; -val RAW_METHOD_CASES = Method.RAW_METHOD_CASES; -val RAW_METHOD = Method.RAW_METHOD; val METHOD_CASES = Method.METHOD_CASES; val METHOD = Method.METHOD; val SIMPLE_METHOD = Method.SIMPLE_METHOD; diff -r 52181f7b4468 -r 568840962230 src/Pure/Isar/proof.ML --- a/src/Pure/Isar/proof.ML Tue Aug 19 16:46:33 2014 +0200 +++ b/src/Pure/Isar/proof.ML Tue Aug 19 18:21:29 2014 +0200 @@ -395,48 +395,24 @@ Rule_Cases.make_common (Thm.theory_of_thm st, Thm.prop_of st) (map (rpair [] o rpair []) (goals st)); -fun apply_method current_context method state = - let - val (goal_ctxt, (_, {statement, messages = _, using, goal, before_qed, after_qed})) = - find_goal state; - val ctxt = if current_context then context_of state else goal_ctxt; - in - Method.apply method ctxt using goal |> Seq.map (fn (meth_cases, goal') => +fun apply_method text ctxt state = + #2 (#2 (find_goal state)) + |> (fn {statement, messages = _, using, goal, before_qed, after_qed} => + Method.evaluate text ctxt using goal + |> Seq.map (fn (meth_cases, goal') => state |> map_goal (Proof_Context.update_cases false (no_goal_cases goal @ goal_cases goal') #> Proof_Context.update_cases true meth_cases) - (K (statement, [], using, goal', before_qed, after_qed)) I) - end; - -fun select_goals n meth state = - ALLGOALS Goal.conjunction_tac (#2 (#2 (get_goal state))) - |> Seq.maps (fn goal => - state - |> Seq.lift provide_goal ((PRIMITIVE (Goal.restrict 1 n) THEN Goal.conjunction_tac 1) goal) - |> Seq.maps meth - |> Seq.maps (fn state' => state' - |> Seq.lift provide_goal (PRIMITIVE (Goal.unrestrict 1) (#2 (#2 (get_goal state'))))) - |> Seq.maps (apply_method true (K Method.succeed))); - -fun apply_text current_context text state = - let - val ctxt = context_of state; - - fun eval (Method.Basic m) = apply_method current_context m - | eval (Method.Source src) = apply_method current_context (Method.method_cmd ctxt src) - | eval (Method.Then (_, txts)) = Seq.EVERY (map eval txts) - | eval (Method.Orelse (_, txts)) = Seq.FIRST (map eval txts) - | eval (Method.Try (_, txt)) = Seq.TRY (eval txt) - | eval (Method.Repeat1 (_, txt)) = Seq.REPEAT1 (eval txt) - | eval (Method.Select_Goals (_, n, txt)) = select_goals n (eval txt); - in eval text state end; + (K (statement, [], using, goal', before_qed, after_qed)) I)); in -val refine = apply_text true; -val refine_end = apply_text false; -fun refine_insert ths = Seq.hd o refine (Method.Basic (K (Method.insert ths))); +fun refine text state = apply_method text (context_of state) state; +fun refine_end text state = apply_method text (#1 (find_goal state)) state; + +fun refine_insert ths = + Seq.hd o refine (Method.Basic (K (Method.insert ths))); end; @@ -892,9 +868,9 @@ in map (Logic.mk_term o Var) vars end; fun refine_terms n = - refine (Method.Basic (K (RAW_METHOD - (K (HEADGOAL (PRECISE_CONJUNCTS n - (HEADGOAL (CONJUNCTS (ALLGOALS (rtac Drule.termI)))))))))) + refine (Method.Basic (K (NO_CASES o + K (HEADGOAL (PRECISE_CONJUNCTS n + (HEADGOAL (CONJUNCTS (ALLGOALS (rtac Drule.termI))))))))) #> Seq.hd; in diff -r 52181f7b4468 -r 568840962230 src/Pure/ROOT --- a/src/Pure/ROOT Tue Aug 19 16:46:33 2014 +0200 +++ b/src/Pure/ROOT Tue Aug 19 18:21:29 2014 +0200 @@ -233,6 +233,7 @@ "morphism.ML" "name.ML" "net.ML" + "par_tactical.ML" "pattern.ML" "primitive_defs.ML" "proofterm.ML" diff -r 52181f7b4468 -r 568840962230 src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Tue Aug 19 16:46:33 2014 +0200 +++ b/src/Pure/ROOT.ML Tue Aug 19 18:21:29 2014 +0200 @@ -255,6 +255,7 @@ (** bootstrap phase 2: towards Pure.thy and final ML toplevel setup *) (*basic proof engine*) +use "par_tactical.ML"; use "Isar/proof_display.ML"; use "Isar/attrib.ML"; use "Isar/context_rules.ML"; diff -r 52181f7b4468 -r 568840962230 src/Pure/goal.ML --- a/src/Pure/goal.ML Tue Aug 19 16:46:33 2014 +0200 +++ b/src/Pure/goal.ML Tue Aug 19 18:21:29 2014 +0200 @@ -11,8 +11,6 @@ val PREFER_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 = @@ -340,50 +338,6 @@ etac (Raw_Simplifier.norm_hhf ctxt (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 *) - -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 => - if not (Multithreading.enabled ()) orelse Thm.maxidx_of st >= 0 orelse Thm.nprems_of st <= 1 - then DETERM tac st - else - let - fun try_tac g = - (case SINGLE tac g of - NONE => raise FAILED () - | SOME g' => g'); - - val goals = Drule.strip_imp_prems (Thm.cprop_of st); - val results = Par_List.map (try_tac o init) goals; - in EVERY (map retrofit (rev results)) st end - handle FAILED () => Seq.empty); - -end; - end; structure Basic_Goal: BASIC_GOAL = Goal; diff -r 52181f7b4468 -r 568840962230 src/Pure/more_thm.ML --- a/src/Pure/more_thm.ML Tue Aug 19 16:46:33 2014 +0200 +++ b/src/Pure/more_thm.ML Tue Aug 19 18:21:29 2014 +0200 @@ -234,7 +234,7 @@ fun is_dummy thm = (case try Logic.dest_term (Thm.concl_of thm) of NONE => false - | SOME t => Term.is_dummy_pattern t); + | SOME t => Term.is_dummy_pattern (Term.head_of t)); fun plain_prop_of raw_thm = let diff -r 52181f7b4468 -r 568840962230 src/Pure/par_tactical.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/par_tactical.ML Tue Aug 19 18:21:29 2014 +0200 @@ -0,0 +1,68 @@ +(* Title: Pure/par_tactical.ML + Author: Makarius + +Parallel tacticals. +*) + +signature BASIC_PAR_TACTICAL = +sig + val PARALLEL_CHOICE: tactic list -> tactic + val PARALLEL_GOALS: tactic -> tactic + val PARALLEL_ALLGOALS: (int -> tactic) -> tactic +end; + +signature PAR_TACTICAL = +sig + include BASIC_PAR_TACTICAL +end; + +structure Par_Tactical: PAR_TACTICAL = +struct + +(* 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 *) + +local + +exception FAILED of unit; + +fun retrofit st' = + rotate_prems ~1 #> + Thm.bicompose {flatten = false, match = false, incremented = false} + (false, Goal.conclude st', Thm.nprems_of st') 1; + +in + +fun PARALLEL_GOALS tac = + Thm.adjust_maxidx_thm ~1 #> + (fn st => + if not (Multithreading.enabled ()) orelse Thm.maxidx_of st >= 0 orelse Thm.nprems_of st <= 1 + then DETERM tac st + else + let + fun try_tac g = + (case SINGLE tac g of + NONE => raise FAILED () + | SOME g' => g'); + + val goals = Drule.strip_imp_prems (Thm.cprop_of st); + val results = Par_List.map (try_tac o Goal.init) goals; + in EVERY (map retrofit (rev results)) st end + handle FAILED () => Seq.empty); + +end; + +val PARALLEL_ALLGOALS = PARALLEL_GOALS o ALLGOALS; + +end; + +structure Basic_Par_Tactical: BASIC_PAR_TACTICAL = Par_Tactical; +open Basic_Par_Tactical; + diff -r 52181f7b4468 -r 568840962230 src/Pure/simplifier.ML --- a/src/Pure/simplifier.ML Tue Aug 19 16:46:33 2014 +0200 +++ b/src/Pure/simplifier.ML Tue Aug 19 18:21:29 2014 +0200 @@ -374,7 +374,7 @@ Method.setup @{binding simp_all} (simp_method more_mods (fn ctxt => fn tac => fn facts => ALLGOALS (Method.insert_tac facts) THEN - (CHANGED_PROP o PARALLEL_GOALS o ALLGOALS o tac) ctxt)) + (CHANGED_PROP o PARALLEL_ALLGOALS o tac) ctxt)) "simplification (all goals)"; fun easy_setup reflect trivs = method_setup [] #> Context.theory_map (map_ss (fn ctxt0 => diff -r 52181f7b4468 -r 568840962230 src/Tools/induct.ML --- a/src/Tools/induct.ML Tue Aug 19 16:46:33 2014 +0200 +++ b/src/Tools/induct.ML Tue Aug 19 18:21:29 2014 +0200 @@ -932,15 +932,13 @@ (cases_tac ctxt (not no_simp) insts opt_rule facts))))) "case analysis on types or predicates/sets"; -fun gen_induct_setup binding itac = +fun gen_induct_setup binding tac = Method.setup binding (Scan.lift (Args.mode no_simpN) -- (Parse.and_list' (Scan.repeat (unless_more_args def_inst)) -- (arbitrary -- taking -- Scan.option induct_rule)) >> - (fn (no_simp, (insts, ((arbitrary, taking), opt_rule))) => fn ctxt => - RAW_METHOD_CASES (fn facts => - Seq.DETERM - (HEADGOAL (itac ctxt (not no_simp) insts arbitrary taking opt_rule facts))))) + (fn (no_simp, (insts, ((arbitrary, taking), opt_rule))) => fn ctxt => fn facts => + Seq.DETERM (HEADGOAL (tac ctxt (not no_simp) insts arbitrary taking opt_rule facts)))) "induction on types or predicates/sets"; val induct_setup = gen_induct_setup @{binding induct} induct_tac; @@ -948,9 +946,8 @@ val coinduct_setup = Method.setup @{binding coinduct} (Scan.repeat (unless_more_args inst) -- taking -- Scan.option coinduct_rule >> - (fn ((insts, taking), opt_rule) => fn ctxt => - RAW_METHOD_CASES (fn facts => - Seq.DETERM (HEADGOAL (coinduct_tac ctxt insts taking opt_rule facts))))) + (fn ((insts, taking), opt_rule) => fn ctxt => fn facts => + Seq.DETERM (HEADGOAL (coinduct_tac ctxt insts taking opt_rule facts)))) "coinduction on types or predicates/sets"; end;