--- 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)
---------------------------------
--- 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 {*
--- 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;
--- 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;
--- 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;
--- 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
--- 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
--- 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
--- 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;
--- 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
--- 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"
--- 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";
--- 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;
--- 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
--- /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;
+
--- 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 =>
--- 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;