author  wenzelm 
Wed, 27 Mar 2013 16:38:25 +0100  
changeset 51553  63327f679cff 
parent 51552  c713c9505f68 
child 51605  eca8acb42e4a 
permissions  rwrr 
17980  1 
(* Title: Pure/goal.ML 
29345  2 
Author: Makarius 
17980  3 

49061
7449b804073b
central management of forked goals wrt. transaction id;
wenzelm
parents:
49041
diff
changeset

4 
Goals in tactical theorem proving, with support for forked proofs. 
17980  5 
*) 
6 

7 
signature BASIC_GOAL = 

8 
sig 

51553
63327f679cff
more ambitious Goal.skip_proofs: covers Goal.prove forms as well, and do not insist in quick_and_dirty (for the sake of Isabelle/jEdit);
wenzelm
parents:
51552
diff
changeset

9 
val skip_proofs: bool Unsynchronized.ref 
32738  10 
val parallel_proofs: int Unsynchronized.ref 
51423
e5f9a6d9ca82
clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
wenzelm
parents:
51276
diff
changeset

11 
val parallel_subproofs_saturation: int Unsynchronized.ref 
e5f9a6d9ca82
clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
wenzelm
parents:
51276
diff
changeset

12 
val parallel_subproofs_threshold: real Unsynchronized.ref 
17980  13 
val SELECT_GOAL: tactic > int > tactic 
23418  14 
val CONJUNCTS: tactic > int > tactic 
23414
927203ad4b3a
tuned conjunction tactics: slightly smaller proof terms;
wenzelm
parents:
23356
diff
changeset

15 
val PRECISE_CONJUNCTS: int > tactic > int > tactic 
32365  16 
val PARALLEL_CHOICE: tactic list > tactic 
17 
val PARALLEL_GOALS: tactic > tactic 

17980  18 
end; 
19 

20 
signature GOAL = 

21 
sig 

22 
include BASIC_GOAL 

23 
val init: cterm > thm 

18027
09ab79d4e8e1
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17986
diff
changeset

24 
val protect: thm > thm 
17980  25 
val conclude: thm > thm 
49845  26 
val check_finished: Proof.context > thm > thm 
32197  27 
val finish: Proof.context > thm > thm 
21604
1af327306c8e
added norm/close_result (supercede local_standard etc.);
wenzelm
parents:
21579
diff
changeset

28 
val norm_result: thm > thm 
51222
8c3e5fb41139
improved scheduling of forked proofs, based on elapsed time estimate (from last run via session log file);
wenzelm
parents:
51118
diff
changeset

29 
val fork_name: string > int > (unit > 'a) > 'a future 
8c3e5fb41139
improved scheduling of forked proofs, based on elapsed time estimate (from last run via session log file);
wenzelm
parents:
51118
diff
changeset

30 
val fork: int > (unit > 'a) > 'a future 
49061
7449b804073b
central management of forked goals wrt. transaction id;
wenzelm
parents:
49041
diff
changeset

31 
val peek_futures: serial > unit future list 
49931
85780e6f8fd2
more basic Goal.reset_futures as snapshot of implicit state;
wenzelm
parents:
49893
diff
changeset

32 
val reset_futures: unit > Future.group list 
51276  33 
val shutdown_futures: unit > unit 
49012
8686c36fa27d
refined treatment of forked proofs at transaction boundaries, including proof commands (see also 7ee000ce5390);
wenzelm
parents:
49009
diff
changeset

34 
val future_enabled_level: int > bool 
29448
34b9652b2f45
added Goal.future_enabled abstraction  now also checks that this is already
wenzelm
parents:
29435
diff
changeset

35 
val future_enabled: unit > bool 
49012
8686c36fa27d
refined treatment of forked proofs at transaction boundaries, including proof commands (see also 7ee000ce5390);
wenzelm
parents:
49009
diff
changeset

36 
val future_enabled_nested: int > bool 
51423
e5f9a6d9ca82
clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
wenzelm
parents:
51276
diff
changeset

37 
val future_enabled_timing: Time.time > bool 
28973
c549650d1442
future proofs: pass actual futures to facilitate composite computations;
wenzelm
parents:
28619
diff
changeset

38 
val future_result: Proof.context > thm future > term > thm 
23356  39 
val prove_internal: cterm list > cterm > (thm list > tactic) > thm 
51553
63327f679cff
more ambitious Goal.skip_proofs: covers Goal.prove forms as well, and do not insist in quick_and_dirty (for the sake of Isabelle/jEdit);
wenzelm
parents:
51552
diff
changeset

40 
val is_schematic: term > bool 
20290  41 
val prove_multi: Proof.context > string list > term list > term list > 
42 
({prems: thm list, context: Proof.context} > tactic) > thm list 

28446
a01de3b3fa2e
renamed promise to future, tuned related interfaces;
wenzelm
parents:
28363
diff
changeset

43 
val prove_future: Proof.context > string list > term list > term > 
28340  44 
({prems: thm list, context: Proof.context} > tactic) > thm 
20290  45 
val prove: Proof.context > string list > term list > term > 
46 
({prems: thm list, context: Proof.context} > tactic) > thm 

51118
32a5994dd205
tuned signature  legacy packages might want to fork proofs as well;
wenzelm
parents:
51110
diff
changeset

47 
val prove_global_future: theory > string list > term list > term > 
32a5994dd205
tuned signature  legacy packages might want to fork proofs as well;
wenzelm
parents:
51110
diff
changeset

48 
({prems: thm list, context: Proof.context} > tactic) > thm 
26713
1c6181def1d0
prove_global: Variable.set_body true, pass context;
wenzelm
parents:
26628
diff
changeset

49 
val prove_global: theory > string list > term list > term > 
1c6181def1d0
prove_global: Variable.set_body true, pass context;
wenzelm
parents:
26628
diff
changeset

50 
({prems: thm list, context: Proof.context} > tactic) > thm 
51551  51 
val prove_sorry: Proof.context > string list > term list > term > 
52 
({prems: thm list, context: Proof.context} > tactic) > thm 

53 
val prove_sorry_global: theory > string list > term list > term > 

54 
({prems: thm list, context: Proof.context} > tactic) > thm 

19184  55 
val extract: int > int > thm > thm Seq.seq 
56 
val retrofit: int > int > thm > thm > thm Seq.seq 

23418  57 
val conjunction_tac: int > tactic 
23414
927203ad4b3a
tuned conjunction tactics: slightly smaller proof terms;
wenzelm
parents:
23356
diff
changeset

58 
val precise_conjunction_tac: int > int > tactic 
23418  59 
val recover_conjunction_tac: tactic 
21687  60 
val norm_hhf_tac: int > tactic 
61 
val compose_hhf_tac: thm > int > tactic 

23237  62 
val assume_rule_tac: Proof.context > int > tactic 
17980  63 
end; 
64 

65 
structure Goal: GOAL = 

66 
struct 

67 

18027
09ab79d4e8e1
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17986
diff
changeset

68 
(** goals **) 
09ab79d4e8e1
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17986
diff
changeset

69 

09ab79d4e8e1
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17986
diff
changeset

70 
(* 
09ab79d4e8e1
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17986
diff
changeset

71 
 (init) 
09ab79d4e8e1
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17986
diff
changeset

72 
C ==> #C 
09ab79d4e8e1
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17986
diff
changeset

73 
*) 
20290  74 
val init = 
22902
ac833b4bb7ee
moved some Drule operations to Thm (see more_thm.ML);
wenzelm
parents:
21687
diff
changeset

75 
let val A = #1 (Thm.dest_implies (Thm.cprop_of Drule.protectI)) 
20290  76 
in fn C => Thm.instantiate ([], [(A, C)]) Drule.protectI end; 
17980  77 

78 
(* 

18119  79 
C 
80 
 (protect) 

81 
#C 

17980  82 
*) 
29345  83 
fun protect th = Drule.comp_no_flatten (th, 0) 1 Drule.protectI; 
17980  84 

85 
(* 

18027
09ab79d4e8e1
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17986
diff
changeset

86 
A ==> ... ==> #C 
09ab79d4e8e1
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17986
diff
changeset

87 
 (conclude) 
17980  88 
A ==> ... ==> C 
89 
*) 

29345  90 
fun conclude th = Drule.comp_no_flatten (th, Thm.nprems_of th) 1 Drule.protectD; 
17980  91 

92 
(* 

18027
09ab79d4e8e1
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17986
diff
changeset

93 
#C 
09ab79d4e8e1
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17986
diff
changeset

94 
 (finish) 
09ab79d4e8e1
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17986
diff
changeset

95 
C 
17983  96 
*) 
32197  97 
fun check_finished ctxt th = 
17980  98 
(case Thm.nprems_of th of 
49845  99 
0 => th 
17980  100 
 n => raise THM ("Proof failed.\n" ^ 
49847  101 
Pretty.string_of (Goal_Display.pretty_goal {main = true, limit = false} ctxt th), 0, [th])); 
32197  102 

49845  103 
fun finish ctxt = check_finished ctxt #> conclude; 
17980  104 

105 

18027
09ab79d4e8e1
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17986
diff
changeset

106 

09ab79d4e8e1
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17986
diff
changeset

107 
(** results **) 
09ab79d4e8e1
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17986
diff
changeset

108 

28340  109 
(* normal form *) 
110 

21604
1af327306c8e
added norm/close_result (supercede local_standard etc.);
wenzelm
parents:
21579
diff
changeset

111 
val norm_result = 
1af327306c8e
added norm/close_result (supercede local_standard etc.);
wenzelm
parents:
21579
diff
changeset

112 
Drule.flexflex_unique 
41228
e1fce873b814
renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
wenzelm
parents:
39125
diff
changeset

113 
#> Raw_Simplifier.norm_hhf_protect 
21604
1af327306c8e
added norm/close_result (supercede local_standard etc.);
wenzelm
parents:
21579
diff
changeset

114 
#> Thm.strip_shyps 
1af327306c8e
added norm/close_result (supercede local_standard etc.);
wenzelm
parents:
21579
diff
changeset

115 
#> Drule.zero_var_indexes; 
1af327306c8e
added norm/close_result (supercede local_standard etc.);
wenzelm
parents:
21579
diff
changeset

116 

1af327306c8e
added norm/close_result (supercede local_standard etc.);
wenzelm
parents:
21579
diff
changeset

117 

41703
d27950860514
parallelization of nested Isar proofs is subject to Goal.parallel_proofs_threshold;
wenzelm
parents:
41683
diff
changeset

118 
(* forked proofs *) 
d27950860514
parallelization of nested Isar proofs is subject to Goal.parallel_proofs_threshold;
wenzelm
parents:
41683
diff
changeset

119 

49061
7449b804073b
central management of forked goals wrt. transaction id;
wenzelm
parents:
49041
diff
changeset

120 
local 
41703
d27950860514
parallelization of nested Isar proofs is subject to Goal.parallel_proofs_threshold;
wenzelm
parents:
41683
diff
changeset

121 

49061
7449b804073b
central management of forked goals wrt. transaction id;
wenzelm
parents:
49041
diff
changeset

122 
val forked_proofs = 
7449b804073b
central management of forked goals wrt. transaction id;
wenzelm
parents:
49041
diff
changeset

123 
Synchronized.var "forked_proofs" 
7449b804073b
central management of forked goals wrt. transaction id;
wenzelm
parents:
49041
diff
changeset

124 
(0, []: Future.group list, Inttab.empty: unit future list Inttab.table); 
7449b804073b
central management of forked goals wrt. transaction id;
wenzelm
parents:
49041
diff
changeset

125 

7449b804073b
central management of forked goals wrt. transaction id;
wenzelm
parents:
49041
diff
changeset

126 
fun count_forked i = 
7449b804073b
central management of forked goals wrt. transaction id;
wenzelm
parents:
49041
diff
changeset

127 
Synchronized.change forked_proofs (fn (m, groups, tab) => 
41703
d27950860514
parallelization of nested Isar proofs is subject to Goal.parallel_proofs_threshold;
wenzelm
parents:
41683
diff
changeset

128 
let 
d27950860514
parallelization of nested Isar proofs is subject to Goal.parallel_proofs_threshold;
wenzelm
parents:
41683
diff
changeset

129 
val n = m + i; 
50974
55f8bd61b029
added "tasks_proof" statistics, via slighly odd global reference Future.forked_proofs (NB: Future.report_status is intertwined with scheduler thread);
wenzelm
parents:
50914
diff
changeset

130 
val _ = Future.forked_proofs := n; 
49061
7449b804073b
central management of forked goals wrt. transaction id;
wenzelm
parents:
49041
diff
changeset

131 
in (n, groups, tab) end); 
7449b804073b
central management of forked goals wrt. transaction id;
wenzelm
parents:
49041
diff
changeset

132 

7449b804073b
central management of forked goals wrt. transaction id;
wenzelm
parents:
49041
diff
changeset

133 
fun register_forked id future = 
7449b804073b
central management of forked goals wrt. transaction id;
wenzelm
parents:
49041
diff
changeset

134 
Synchronized.change forked_proofs (fn (m, groups, tab) => 
7449b804073b
central management of forked goals wrt. transaction id;
wenzelm
parents:
49041
diff
changeset

135 
let 
7449b804073b
central management of forked goals wrt. transaction id;
wenzelm
parents:
49041
diff
changeset

136 
val groups' = Task_Queue.group_of_task (Future.task_of future) :: groups; 
7449b804073b
central management of forked goals wrt. transaction id;
wenzelm
parents:
49041
diff
changeset

137 
val tab' = Inttab.cons_list (id, Future.map (K ()) future) tab; 
7449b804073b
central management of forked goals wrt. transaction id;
wenzelm
parents:
49041
diff
changeset

138 
in (m, groups', tab') end); 
37186
349e9223c685
explicit markup for forked goals, as indicated by Goal.fork;
wenzelm
parents:
36613
diff
changeset

139 

49036
4680c4046814
further refinement of command status, to accomodate forked proofs;
wenzelm
parents:
49012
diff
changeset

140 
fun status task markups = 
50201
c26369c9eda6
Isabellespecific implementation of quasiabstract markup elements  back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49931
diff
changeset

141 
let val props = Markup.properties [(Markup.taskN, Task_Queue.str_of_task task)] 
49036
4680c4046814
further refinement of command status, to accomodate forked proofs;
wenzelm
parents:
49012
diff
changeset

142 
in Output.status (implode (map (Markup.markup_only o props) markups)) end; 
49009  143 

49061
7449b804073b
central management of forked goals wrt. transaction id;
wenzelm
parents:
49041
diff
changeset

144 
in 
7449b804073b
central management of forked goals wrt. transaction id;
wenzelm
parents:
49041
diff
changeset

145 

51222
8c3e5fb41139
improved scheduling of forked proofs, based on elapsed time estimate (from last run via session log file);
wenzelm
parents:
51118
diff
changeset

146 
fun fork_name name pri e = 
41703
d27950860514
parallelization of nested Isar proofs is subject to Goal.parallel_proofs_threshold;
wenzelm
parents:
41683
diff
changeset

147 
uninterruptible (fn _ => fn () => 
d27950860514
parallelization of nested Isar proofs is subject to Goal.parallel_proofs_threshold;
wenzelm
parents:
41683
diff
changeset

148 
let 
50914
fe4714886d92
identify future results more carefully, to avoid odd duplication of error messages, notably from forked goals;
wenzelm
parents:
50911
diff
changeset

149 
val pos = Position.thread_data (); 
fe4714886d92
identify future results more carefully, to avoid odd duplication of error messages, notably from forked goals;
wenzelm
parents:
50911
diff
changeset

150 
val id = the_default 0 (Position.parse_id pos); 
49061
7449b804073b
central management of forked goals wrt. transaction id;
wenzelm
parents:
49041
diff
changeset

151 
val _ = count_forked 1; 
50914
fe4714886d92
identify future results more carefully, to avoid odd duplication of error messages, notably from forked goals;
wenzelm
parents:
50911
diff
changeset

152 

41703
d27950860514
parallelization of nested Isar proofs is subject to Goal.parallel_proofs_threshold;
wenzelm
parents:
41683
diff
changeset

153 
val future = 
44302  154 
(singleton o Future.forks) 
51222
8c3e5fb41139
improved scheduling of forked proofs, based on elapsed time estimate (from last run via session log file);
wenzelm
parents:
51118
diff
changeset

155 
{name = name, group = NONE, deps = [], pri = pri, interrupts = false} 
49036
4680c4046814
further refinement of command status, to accomodate forked proofs;
wenzelm
parents:
49012
diff
changeset

156 
(fn () => 
4680c4046814
further refinement of command status, to accomodate forked proofs;
wenzelm
parents:
49012
diff
changeset

157 
let 
4680c4046814
further refinement of command status, to accomodate forked proofs;
wenzelm
parents:
49012
diff
changeset

158 
val task = the (Future.worker_task ()); 
50201
c26369c9eda6
Isabellespecific implementation of quasiabstract markup elements  back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49931
diff
changeset

159 
val _ = status task [Markup.running]; 
50914
fe4714886d92
identify future results more carefully, to avoid odd duplication of error messages, notably from forked goals;
wenzelm
parents:
50911
diff
changeset

160 
val result = 
fe4714886d92
identify future results more carefully, to avoid odd duplication of error messages, notably from forked goals;
wenzelm
parents:
50911
diff
changeset

161 
Exn.capture (Future.interruptible_task e) () 
fe4714886d92
identify future results more carefully, to avoid odd duplication of error messages, notably from forked goals;
wenzelm
parents:
50911
diff
changeset

162 
> Future.identify_result pos; 
50201
c26369c9eda6
Isabellespecific implementation of quasiabstract markup elements  back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49931
diff
changeset

163 
val _ = status task [Markup.finished, Markup.joined]; 
49036
4680c4046814
further refinement of command status, to accomodate forked proofs;
wenzelm
parents:
49012
diff
changeset

164 
val _ = 
49041
9edfd36a0355
more informative error message from failed goal forks (violating oldstyle TTY protocol!);
wenzelm
parents:
49037
diff
changeset

165 
(case result of 
9edfd36a0355
more informative error message from failed goal forks (violating oldstyle TTY protocol!);
wenzelm
parents:
49037
diff
changeset

166 
Exn.Res _ => () 
9edfd36a0355
more informative error message from failed goal forks (violating oldstyle TTY protocol!);
wenzelm
parents:
49037
diff
changeset

167 
 Exn.Exn exn => 
49830
28d207ba9340
no special treatment of errors inside goal forks without transaction id, to avoid duplication in plain build with sequential log, for example;
wenzelm
parents:
49829
diff
changeset

168 
if id = 0 orelse Exn.is_interrupt exn then () 
49829
2bc5924b117f
do not treat interrupt as error here, to avoid confusion in log etc.;
wenzelm
parents:
49061
diff
changeset

169 
else 
50201
c26369c9eda6
Isabellespecific implementation of quasiabstract markup elements  back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49931
diff
changeset

170 
(status task [Markup.failed]; 
c26369c9eda6
Isabellespecific implementation of quasiabstract markup elements  back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49931
diff
changeset

171 
Output.report (Markup.markup_only Markup.bad); 
50914
fe4714886d92
identify future results more carefully, to avoid odd duplication of error messages, notably from forked goals;
wenzelm
parents:
50911
diff
changeset

172 
List.app (Future.error_msg pos) (ML_Compiler.exn_messages_ids exn))); 
49061
7449b804073b
central management of forked goals wrt. transaction id;
wenzelm
parents:
49041
diff
changeset

173 
val _ = count_forked ~1; 
49036
4680c4046814
further refinement of command status, to accomodate forked proofs;
wenzelm
parents:
49012
diff
changeset

174 
in Exn.release result end); 
50201
c26369c9eda6
Isabellespecific implementation of quasiabstract markup elements  back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49931
diff
changeset

175 
val _ = status (Future.task_of future) [Markup.forked]; 
49061
7449b804073b
central management of forked goals wrt. transaction id;
wenzelm
parents:
49041
diff
changeset

176 
val _ = register_forked id future; 
41703
d27950860514
parallelization of nested Isar proofs is subject to Goal.parallel_proofs_threshold;
wenzelm
parents:
41683
diff
changeset

177 
in future end) (); 
29448
34b9652b2f45
added Goal.future_enabled abstraction  now also checks that this is already
wenzelm
parents:
29435
diff
changeset

178 

51222
8c3e5fb41139
improved scheduling of forked proofs, based on elapsed time estimate (from last run via session log file);
wenzelm
parents:
51118
diff
changeset

179 
fun fork pri e = fork_name "Goal.fork" pri e; 
41677  180 

49061
7449b804073b
central management of forked goals wrt. transaction id;
wenzelm
parents:
49041
diff
changeset

181 
fun forked_count () = #1 (Synchronized.value forked_proofs); 
7449b804073b
central management of forked goals wrt. transaction id;
wenzelm
parents:
49041
diff
changeset

182 

7449b804073b
central management of forked goals wrt. transaction id;
wenzelm
parents:
49041
diff
changeset

183 
fun peek_futures id = 
7449b804073b
central management of forked goals wrt. transaction id;
wenzelm
parents:
49041
diff
changeset

184 
Inttab.lookup_list (#3 (Synchronized.value forked_proofs)) id; 
7449b804073b
central management of forked goals wrt. transaction id;
wenzelm
parents:
49041
diff
changeset

185 

49931
85780e6f8fd2
more basic Goal.reset_futures as snapshot of implicit state;
wenzelm
parents:
49893
diff
changeset

186 
fun reset_futures () = 
85780e6f8fd2
more basic Goal.reset_futures as snapshot of implicit state;
wenzelm
parents:
49893
diff
changeset

187 
Synchronized.change_result forked_proofs (fn (m, groups, tab) => 
50974
55f8bd61b029
added "tasks_proof" statistics, via slighly odd global reference Future.forked_proofs (NB: Future.report_status is intertwined with scheduler thread);
wenzelm
parents:
50914
diff
changeset

188 
(Future.forked_proofs := 0; (groups, (0, [], Inttab.empty)))); 
49061
7449b804073b
central management of forked goals wrt. transaction id;
wenzelm
parents:
49041
diff
changeset

189 

51276  190 
fun shutdown_futures () = 
191 
(Future.shutdown (); 

192 
(case map_filter Task_Queue.group_status (reset_futures ()) of 

193 
[] => () 

194 
 exns => raise Par_Exn.make exns)); 

195 

49061
7449b804073b
central management of forked goals wrt. transaction id;
wenzelm
parents:
49041
diff
changeset

196 
end; 
7449b804073b
central management of forked goals wrt. transaction id;
wenzelm
parents:
49041
diff
changeset

197 

41677  198 

41703
d27950860514
parallelization of nested Isar proofs is subject to Goal.parallel_proofs_threshold;
wenzelm
parents:
41683
diff
changeset

199 
(* scheduling parameters *) 
d27950860514
parallelization of nested Isar proofs is subject to Goal.parallel_proofs_threshold;
wenzelm
parents:
41683
diff
changeset

200 

51553
63327f679cff
more ambitious Goal.skip_proofs: covers Goal.prove forms as well, and do not insist in quick_and_dirty (for the sake of Isabelle/jEdit);
wenzelm
parents:
51552
diff
changeset

201 
val skip_proofs = Unsynchronized.ref false; 
63327f679cff
more ambitious Goal.skip_proofs: covers Goal.prove forms as well, and do not insist in quick_and_dirty (for the sake of Isabelle/jEdit);
wenzelm
parents:
51552
diff
changeset

202 

32738  203 
val parallel_proofs = Unsynchronized.ref 1; 
51423
e5f9a6d9ca82
clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
wenzelm
parents:
51276
diff
changeset

204 
val parallel_subproofs_saturation = Unsynchronized.ref 100; 
e5f9a6d9ca82
clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
wenzelm
parents:
51276
diff
changeset

205 
val parallel_subproofs_threshold = Unsynchronized.ref 0.01; 
29448
34b9652b2f45
added Goal.future_enabled abstraction  now also checks that this is already
wenzelm
parents:
29435
diff
changeset

206 

49012
8686c36fa27d
refined treatment of forked proofs at transaction boundaries, including proof commands (see also 7ee000ce5390);
wenzelm
parents:
49009
diff
changeset

207 
fun future_enabled_level n = 
8686c36fa27d
refined treatment of forked proofs at transaction boundaries, including proof commands (see also 7ee000ce5390);
wenzelm
parents:
49009
diff
changeset

208 
Multithreading.enabled () andalso ! parallel_proofs >= n andalso 
41703
d27950860514
parallelization of nested Isar proofs is subject to Goal.parallel_proofs_threshold;
wenzelm
parents:
41683
diff
changeset

209 
is_some (Future.worker_task ()); 
32061
11f8ee55662d
parallel_proofs: more finegrained control with optional parallel checking of nested Isar proofs;
wenzelm
parents:
32058
diff
changeset

210 

49012
8686c36fa27d
refined treatment of forked proofs at transaction boundaries, including proof commands (see also 7ee000ce5390);
wenzelm
parents:
49009
diff
changeset

211 
fun future_enabled () = future_enabled_level 1; 
8686c36fa27d
refined treatment of forked proofs at transaction boundaries, including proof commands (see also 7ee000ce5390);
wenzelm
parents:
49009
diff
changeset

212 

8686c36fa27d
refined treatment of forked proofs at transaction boundaries, including proof commands (see also 7ee000ce5390);
wenzelm
parents:
49009
diff
changeset

213 
fun future_enabled_nested n = 
8686c36fa27d
refined treatment of forked proofs at transaction boundaries, including proof commands (see also 7ee000ce5390);
wenzelm
parents:
49009
diff
changeset

214 
future_enabled_level n andalso 
51423
e5f9a6d9ca82
clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
wenzelm
parents:
51276
diff
changeset

215 
forked_count () < ! parallel_subproofs_saturation * Multithreading.max_threads_value (); 
e5f9a6d9ca82
clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
wenzelm
parents:
51276
diff
changeset

216 

e5f9a6d9ca82
clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
wenzelm
parents:
51276
diff
changeset

217 
fun future_enabled_timing t = 
e5f9a6d9ca82
clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
wenzelm
parents:
51276
diff
changeset

218 
future_enabled () andalso Time.toReal t >= ! parallel_subproofs_threshold; 
29448
34b9652b2f45
added Goal.future_enabled abstraction  now also checks that this is already
wenzelm
parents:
29435
diff
changeset

219 

34b9652b2f45
added Goal.future_enabled abstraction  now also checks that this is already
wenzelm
parents:
29435
diff
changeset

220 

28446
a01de3b3fa2e
renamed promise to future, tuned related interfaces;
wenzelm
parents:
28363
diff
changeset

221 
(* future_result *) 
28340  222 

28446
a01de3b3fa2e
renamed promise to future, tuned related interfaces;
wenzelm
parents:
28363
diff
changeset

223 
fun future_result ctxt result prop = 
28340  224 
let 
42360  225 
val thy = Proof_Context.theory_of ctxt; 
28340  226 
val _ = Context.reject_draft thy; 
227 
val cert = Thm.cterm_of thy; 

228 
val certT = Thm.ctyp_of thy; 

229 

30473
e0b66c11e7e4
Assumption.all_prems_of, Assumption.all_assms_of;
wenzelm
parents:
29448
diff
changeset

230 
val assms = Assumption.all_assms_of ctxt; 
28340  231 
val As = map Thm.term_of assms; 
232 

233 
val xs = map Free (fold Term.add_frees (prop :: As) []); 

234 
val fixes = map cert xs; 

235 

236 
val tfrees = fold Term.add_tfrees (prop :: As) []; 

237 
val instT = map (fn (a, S) => (certT (TVar ((a, 0), S)), certT (TFree (a, S)))) tfrees; 

238 

239 
val global_prop = 

45344
e209da839ff4
added Logic.varify_types_global/unvarify_types_global, which avoids somewhat expensive Term.map_types;
wenzelm
parents:
44302
diff
changeset

240 
cert (Logic.varify_types_global (fold_rev Logic.all xs (Logic.list_implies (As, prop)))) 
32056
f4b74cbecdaf
future_result: explicitly impose Variable.sorts_of again;
wenzelm
parents:
30473
diff
changeset

241 
> Thm.weaken_sorts (Variable.sorts_of ctxt); 
28973
c549650d1442
future proofs: pass actual futures to facilitate composite computations;
wenzelm
parents:
28619
diff
changeset

242 
val global_result = result > Future.map 
33768
bba9eac8aa25
future_result: purge flexflex pairs, which should normally be trivial anyway  prevent Thm.future_result from complaining about tpairs;
wenzelm
parents:
32788
diff
changeset

243 
(Drule.flexflex_unique #> 
bba9eac8aa25
future_result: purge flexflex pairs, which should normally be trivial anyway  prevent Thm.future_result from complaining about tpairs;
wenzelm
parents:
32788
diff
changeset

244 
Thm.adjust_maxidx_thm ~1 #> 
28973
c549650d1442
future proofs: pass actual futures to facilitate composite computations;
wenzelm
parents:
28619
diff
changeset

245 
Drule.implies_intr_list assms #> 
c549650d1442
future proofs: pass actual futures to facilitate composite computations;
wenzelm
parents:
28619
diff
changeset

246 
Drule.forall_intr_list fixes #> 
36613
f3157c288aca
simplified primitive Thm.future: more direct theory check, do not hardwire strip_shyps here;
wenzelm
parents:
36610
diff
changeset

247 
Thm.generalize (map #1 tfrees, []) 0 #> 
f3157c288aca
simplified primitive Thm.future: more direct theory check, do not hardwire strip_shyps here;
wenzelm
parents:
36610
diff
changeset

248 
Thm.strip_shyps); 
28340  249 
val local_result = 
32056
f4b74cbecdaf
future_result: explicitly impose Variable.sorts_of again;
wenzelm
parents:
30473
diff
changeset

250 
Thm.future global_result global_prop 
50987
616789281413
always close derivation at the bottom of forked proofs (despite increased nondeterminism of proof terms)  improve parallel performance by avoiding dynamic dependency within large Isar proofs, e.g. Slicing/JinjaVM/SemanticsWF.thy in AFP/bf9b14cbc707;
wenzelm
parents:
50974
diff
changeset

251 
> Thm.close_derivation 
28340  252 
> Thm.instantiate (instT, []) 
253 
> Drule.forall_elim_list fixes 

254 
> fold (Thm.elim_implies o Thm.assume) assms; 

255 
in local_result end; 

256 

257 

18027
09ab79d4e8e1
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17986
diff
changeset

258 

09ab79d4e8e1
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17986
diff
changeset

259 
(** tactical theorem proving **) 
09ab79d4e8e1
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17986
diff
changeset

260 

23356  261 
(* prove_internal  minimal checks, no normalization of result! *) 
20250
c3f209752749
prove: proper assumption context, more tactic arguments;
wenzelm
parents:
20228
diff
changeset

262 

23356  263 
fun prove_internal casms cprop tac = 
20250
c3f209752749
prove: proper assumption context, more tactic arguments;
wenzelm
parents:
20228
diff
changeset

264 
(case SINGLE (tac (map Assumption.assume casms)) (init cprop) of 
32197  265 
SOME th => Drule.implies_intr_list casms 
266 
(finish (Syntax.init_pretty_global (Thm.theory_of_thm th)) th) 

38875
c7a66b584147
tuned messages: discontinued spurious fullstops (messages are occasionally composed unexpectedly);
wenzelm
parents:
38236
diff
changeset

267 
 NONE => error "Tactic failed"); 
20250
c3f209752749
prove: proper assumption context, more tactic arguments;
wenzelm
parents:
20228
diff
changeset

268 

c3f209752749
prove: proper assumption context, more tactic arguments;
wenzelm
parents:
20228
diff
changeset

269 

51553
63327f679cff
more ambitious Goal.skip_proofs: covers Goal.prove forms as well, and do not insist in quick_and_dirty (for the sake of Isabelle/jEdit);
wenzelm
parents:
51552
diff
changeset

270 
(* prove variations *) 
63327f679cff
more ambitious Goal.skip_proofs: covers Goal.prove forms as well, and do not insist in quick_and_dirty (for the sake of Isabelle/jEdit);
wenzelm
parents:
51552
diff
changeset

271 

63327f679cff
more ambitious Goal.skip_proofs: covers Goal.prove forms as well, and do not insist in quick_and_dirty (for the sake of Isabelle/jEdit);
wenzelm
parents:
51552
diff
changeset

272 
fun is_schematic t = 
63327f679cff
more ambitious Goal.skip_proofs: covers Goal.prove forms as well, and do not insist in quick_and_dirty (for the sake of Isabelle/jEdit);
wenzelm
parents:
51552
diff
changeset

273 
Term.exists_subterm Term.is_Var t orelse 
63327f679cff
more ambitious Goal.skip_proofs: covers Goal.prove forms as well, and do not insist in quick_and_dirty (for the sake of Isabelle/jEdit);
wenzelm
parents:
51552
diff
changeset

274 
Term.exists_type (Term.exists_subtype Term.is_TVar) t; 
17986  275 

28340  276 
fun prove_common immediate ctxt xs asms props tac = 
17980  277 
let 
42360  278 
val thy = Proof_Context.theory_of ctxt; 
26939
1035c89b4c02
moved global pretty/string_of functions from Sign to Syntax;
wenzelm
parents:
26713
diff
changeset

279 
val string_of_term = Syntax.string_of_term ctxt; 
20056  280 

51553
63327f679cff
more ambitious Goal.skip_proofs: covers Goal.prove forms as well, and do not insist in quick_and_dirty (for the sake of Isabelle/jEdit);
wenzelm
parents:
51552
diff
changeset

281 
val schematic = exists is_schematic props; 
63327f679cff
more ambitious Goal.skip_proofs: covers Goal.prove forms as well, and do not insist in quick_and_dirty (for the sake of Isabelle/jEdit);
wenzelm
parents:
51552
diff
changeset

282 
val future = future_enabled (); 
63327f679cff
more ambitious Goal.skip_proofs: covers Goal.prove forms as well, and do not insist in quick_and_dirty (for the sake of Isabelle/jEdit);
wenzelm
parents:
51552
diff
changeset

283 
val skip = not immediate andalso not schematic andalso future andalso ! skip_proofs; 
63327f679cff
more ambitious Goal.skip_proofs: covers Goal.prove forms as well, and do not insist in quick_and_dirty (for the sake of Isabelle/jEdit);
wenzelm
parents:
51552
diff
changeset

284 

28355  285 
val pos = Position.thread_data (); 
20250
c3f209752749
prove: proper assumption context, more tactic arguments;
wenzelm
parents:
20228
diff
changeset

286 
fun err msg = cat_error msg 
c3f209752749
prove: proper assumption context, more tactic arguments;
wenzelm
parents:
20228
diff
changeset

287 
("The error(s) above occurred for the goal statement:\n" ^ 
28355  288 
string_of_term (Logic.list_implies (asms, Logic.mk_conjunction_list props)) ^ 
48992  289 
(case Position.here pos of "" => ""  s => "\n" ^ s)); 
17980  290 

20250
c3f209752749
prove: proper assumption context, more tactic arguments;
wenzelm
parents:
20228
diff
changeset

291 
fun cert_safe t = Thm.cterm_of thy (Envir.beta_norm (Term.no_dummy_patterns t)) 
17980  292 
handle TERM (msg, _) => err msg  TYPE (msg, _, _) => err msg; 
20250
c3f209752749
prove: proper assumption context, more tactic arguments;
wenzelm
parents:
20228
diff
changeset

293 
val casms = map cert_safe asms; 
c3f209752749
prove: proper assumption context, more tactic arguments;
wenzelm
parents:
20228
diff
changeset

294 
val cprops = map cert_safe props; 
17980  295 

20250
c3f209752749
prove: proper assumption context, more tactic arguments;
wenzelm
parents:
20228
diff
changeset

296 
val (prems, ctxt') = ctxt 
c3f209752749
prove: proper assumption context, more tactic arguments;
wenzelm
parents:
20228
diff
changeset

297 
> Variable.add_fixes_direct xs 
27218
4548c83cd508
prove: full Variable.declare_term, including constraints;
wenzelm
parents:
26939
diff
changeset

298 
> fold Variable.declare_term (asms @ props) 
26713
1c6181def1d0
prove_global: Variable.set_body true, pass context;
wenzelm
parents:
26628
diff
changeset

299 
> Assumption.add_assumes casms 
1c6181def1d0
prove_global: Variable.set_body true, pass context;
wenzelm
parents:
26628
diff
changeset

300 
> Variable.set_body true; 
28619
89f9dd800a22
prove_common: include all sorts from context into statement, check shyps of result;
wenzelm
parents:
28446
diff
changeset

301 
val sorts = Variable.sorts_of ctxt'; 
17980  302 

28619
89f9dd800a22
prove_common: include all sorts from context into statement, check shyps of result;
wenzelm
parents:
28446
diff
changeset

303 
val stmt = Thm.weaken_sorts sorts (Conjunction.mk_conjunction_balanced cprops); 
28340  304 

51553
63327f679cff
more ambitious Goal.skip_proofs: covers Goal.prove forms as well, and do not insist in quick_and_dirty (for the sake of Isabelle/jEdit);
wenzelm
parents:
51552
diff
changeset

305 
fun tac' args st = 
63327f679cff
more ambitious Goal.skip_proofs: covers Goal.prove forms as well, and do not insist in quick_and_dirty (for the sake of Isabelle/jEdit);
wenzelm
parents:
51552
diff
changeset

306 
if skip then ALLGOALS Skip_Proof.cheat_tac st before Skip_Proof.report ctxt 
63327f679cff
more ambitious Goal.skip_proofs: covers Goal.prove forms as well, and do not insist in quick_and_dirty (for the sake of Isabelle/jEdit);
wenzelm
parents:
51552
diff
changeset

307 
else tac args st; 
28340  308 
fun result () = 
51553
63327f679cff
more ambitious Goal.skip_proofs: covers Goal.prove forms as well, and do not insist in quick_and_dirty (for the sake of Isabelle/jEdit);
wenzelm
parents:
51552
diff
changeset

309 
(case SINGLE (tac' {prems = prems, context = ctxt'}) (init stmt) of 
38875
c7a66b584147
tuned messages: discontinued spurious fullstops (messages are occasionally composed unexpectedly);
wenzelm
parents:
38236
diff
changeset

310 
NONE => err "Tactic failed" 
28340  311 
 SOME st => 
32197  312 
let val res = finish ctxt' st handle THM (msg, _, _) => err msg in 
28619
89f9dd800a22
prove_common: include all sorts from context into statement, check shyps of result;
wenzelm
parents:
28446
diff
changeset

313 
if Unify.matches_list thy [Thm.term_of stmt] [Thm.prop_of res] 
89f9dd800a22
prove_common: include all sorts from context into statement, check shyps of result;
wenzelm
parents:
28446
diff
changeset

314 
then Thm.check_shyps sorts res 
28340  315 
else err ("Proved a different theorem: " ^ string_of_term (Thm.prop_of res)) 
316 
end); 

317 
val res = 

51553
63327f679cff
more ambitious Goal.skip_proofs: covers Goal.prove forms as well, and do not insist in quick_and_dirty (for the sake of Isabelle/jEdit);
wenzelm
parents:
51552
diff
changeset

318 
if immediate orelse schematic orelse not future orelse skip 
29088
95a239a5e055
future proofs: more robust check via Future.enabled;
wenzelm
parents:
28973
diff
changeset

319 
then result () 
51222
8c3e5fb41139
improved scheduling of forked proofs, based on elapsed time estimate (from last run via session log file);
wenzelm
parents:
51118
diff
changeset

320 
else future_result ctxt' (fork ~1 result) (Thm.term_of stmt); 
17980  321 
in 
28340  322 
Conjunction.elim_balanced (length props) res 
20290  323 
> map (Assumption.export false ctxt' ctxt) 
20056  324 
> Variable.export ctxt' ctxt 
20250
c3f209752749
prove: proper assumption context, more tactic arguments;
wenzelm
parents:
20228
diff
changeset

325 
> map Drule.zero_var_indexes 
17980  326 
end; 
327 

28341  328 
val prove_multi = prove_common true; 
17980  329 

28446
a01de3b3fa2e
renamed promise to future, tuned related interfaces;
wenzelm
parents:
28363
diff
changeset

330 
fun prove_future ctxt xs asms prop tac = hd (prove_common false ctxt xs asms [prop] tac); 
51118
32a5994dd205
tuned signature  legacy packages might want to fork proofs as well;
wenzelm
parents:
51110
diff
changeset

331 

28340  332 
fun prove ctxt xs asms prop tac = hd (prove_common true ctxt xs asms [prop] tac); 
20056  333 

51118
32a5994dd205
tuned signature  legacy packages might want to fork proofs as well;
wenzelm
parents:
51110
diff
changeset

334 
fun prove_global_future thy xs asms prop tac = 
32a5994dd205
tuned signature  legacy packages might want to fork proofs as well;
wenzelm
parents:
51110
diff
changeset

335 
Drule.export_without_context (prove_future (Proof_Context.init_global thy) xs asms prop tac); 
32a5994dd205
tuned signature  legacy packages might want to fork proofs as well;
wenzelm
parents:
51110
diff
changeset

336 

20056  337 
fun prove_global thy xs asms prop tac = 
42360  338 
Drule.export_without_context (prove (Proof_Context.init_global thy) xs asms prop tac); 
18027
09ab79d4e8e1
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17986
diff
changeset

339 

51551  340 
fun prove_sorry ctxt xs asms prop tac = 
341 
if ! quick_and_dirty then 

51552
c713c9505f68
clarified Skip_Proof.cheat_tac: more standard tactic;
wenzelm
parents:
51551
diff
changeset

342 
prove ctxt xs asms prop (fn _ => ALLGOALS Skip_Proof.cheat_tac) 
51551  343 
else (if future_enabled () then prove_future else prove) ctxt xs asms prop tac; 
344 

345 
fun prove_sorry_global thy xs asms prop tac = 

346 
Drule.export_without_context 

347 
(prove_sorry (Proof_Context.init_global thy) xs asms prop tac); 

348 

18027
09ab79d4e8e1
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17986
diff
changeset

349 

17980  350 

21687  351 
(** goal structure **) 
352 

353 
(* nested goals *) 

18207  354 

19184  355 
fun extract i n st = 
356 
(if i < 1 orelse n < 1 orelse i + n  1 > Thm.nprems_of st then Seq.empty 

357 
else if n = 1 then Seq.single (Thm.cprem_of st i) 

23418  358 
else 
359 
Seq.single (Conjunction.mk_conjunction_balanced (map (Thm.cprem_of st) (i upto i + n  1)))) 

20260  360 
> Seq.map (Thm.adjust_maxidx_cterm ~1 #> init); 
17980  361 

19221  362 
fun retrofit i n st' st = 
363 
(if n = 1 then st 

23418  364 
else st > Drule.with_subgoal i (Conjunction.uncurry_balanced n)) 
19221  365 
> Thm.compose_no_flatten false (conclude st', Thm.nprems_of st') i; 
18207  366 

17980  367 
fun SELECT_GOAL tac i st = 
19191  368 
if Thm.nprems_of st = 1 andalso i = 1 then tac st 
19184  369 
else Seq.lifts (retrofit i 1) (Seq.maps tac (extract i 1 st)) st; 
17980  370 

21687  371 

372 
(* multiple goals *) 

373 

23418  374 
fun precise_conjunction_tac 0 i = eq_assume_tac i 
375 
 precise_conjunction_tac 1 i = SUBGOAL (K all_tac) i 

376 
 precise_conjunction_tac n i = PRIMITIVE (Drule.with_subgoal i (Conjunction.curry_balanced n)); 

23414
927203ad4b3a
tuned conjunction tactics: slightly smaller proof terms;
wenzelm
parents:
23356
diff
changeset

377 

23418  378 
val adhoc_conjunction_tac = REPEAT_ALL_NEW 
379 
(SUBGOAL (fn (goal, i) => 

380 
if can Logic.dest_conjunction goal then rtac Conjunction.conjunctionI i 

381 
else no_tac)); 

21687  382 

23418  383 
val conjunction_tac = SUBGOAL (fn (goal, i) => 
384 
precise_conjunction_tac (length (Logic.dest_conjunctions goal)) i ORELSE 

385 
TRY (adhoc_conjunction_tac i)); 

21687  386 

23418  387 
val recover_conjunction_tac = PRIMITIVE (fn th => 
388 
Conjunction.uncurry_balanced (Thm.nprems_of th) th); 

23414
927203ad4b3a
tuned conjunction tactics: slightly smaller proof terms;
wenzelm
parents:
23356
diff
changeset

389 

927203ad4b3a
tuned conjunction tactics: slightly smaller proof terms;
wenzelm
parents:
23356
diff
changeset

390 
fun PRECISE_CONJUNCTS n tac = 
927203ad4b3a
tuned conjunction tactics: slightly smaller proof terms;
wenzelm
parents:
23356
diff
changeset

391 
SELECT_GOAL (precise_conjunction_tac n 1 
927203ad4b3a
tuned conjunction tactics: slightly smaller proof terms;
wenzelm
parents:
23356
diff
changeset

392 
THEN tac 
23418  393 
THEN recover_conjunction_tac); 
23414
927203ad4b3a
tuned conjunction tactics: slightly smaller proof terms;
wenzelm
parents:
23356
diff
changeset

394 

21687  395 
fun CONJUNCTS tac = 
396 
SELECT_GOAL (conjunction_tac 1 

397 
THEN tac 

23418  398 
THEN recover_conjunction_tac); 
21687  399 

400 

401 
(* hhf normal form *) 

402 

403 
val norm_hhf_tac = 

404 
rtac Drule.asm_rl (*cheap approximation  thanks to builtin Logic.flatten_params*) 

405 
THEN' SUBGOAL (fn (t, i) => 

406 
if Drule.is_norm_hhf t then all_tac 

41228
e1fce873b814
renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
wenzelm
parents:
39125
diff
changeset

407 
else rewrite_goal_tac Drule.norm_hhf_eqs i); 
21687  408 

25301  409 
fun compose_hhf_tac th i st = 
410 
PRIMSEQ (Thm.bicompose false (false, Drule.lift_all (Thm.cprem_of st i) th, 0) i) st; 

21687  411 

23237  412 

413 
(* nonatomic goal assumptions *) 

414 

23356  415 
fun non_atomic (Const ("==>", _) $ _ $ _) = true 
416 
 non_atomic (Const ("all", _) $ _) = true 

417 
 non_atomic _ = false; 

418 

23237  419 
fun assume_rule_tac ctxt = norm_hhf_tac THEN' CSUBGOAL (fn (goal, i) => 
420 
let 

42495
1af81b70cf09
clarified Variable.focus vs. Variable.focus_cterm  eliminated clone;
wenzelm
parents:
42371
diff
changeset

421 
val ((_, goal'), ctxt') = Variable.focus_cterm goal ctxt; 
23237  422 
val goal'' = Drule.cterm_rule (singleton (Variable.export ctxt' ctxt)) goal'; 
23356  423 
val Rs = filter (non_atomic o Thm.term_of) (Drule.strip_imp_prems goal''); 
23237  424 
val tacs = Rs > map (fn R => 
41228
e1fce873b814
renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
wenzelm
parents:
39125
diff
changeset

425 
Tactic.etac (Raw_Simplifier.norm_hhf (Thm.trivial R)) THEN_ALL_NEW assume_tac); 
23237  426 
in fold_rev (curry op APPEND') tacs (K no_tac) i end); 
427 

32365  428 

429 
(* parallel tacticals *) 

430 

431 
(*parallel choice of single results*) 

432 
fun PARALLEL_CHOICE tacs st = 

433 
(case Par_List.get_some (fn tac => SINGLE tac st) tacs of 

434 
NONE => Seq.empty 

435 
 SOME st' => Seq.single st'); 

436 

437 
(*parallel refinement of nonschematic goal by single results*) 

32788
a65deb8f9434
PARALLEL_GOALS: proper scope for exception FAILED, with dummy argument to prevent its interpretation as variable;
wenzelm
parents:
32738
diff
changeset

438 
exception FAILED of unit; 
42370  439 
fun PARALLEL_GOALS tac = 
440 
Thm.adjust_maxidx_thm ~1 #> 

441 
(fn st => 

42371
5900f06b4198
enable PARALLEL_GOALS more liberally, unlike forked proofs (cf. 34b9652b2f45);
wenzelm
parents:
42370
diff
changeset

442 
if not (Multithreading.enabled ()) orelse Thm.maxidx_of st >= 0 orelse Thm.nprems_of st <= 1 
42370  443 
then DETERM tac st 
444 
else 

445 
let 

446 
fun try_tac g = 

447 
(case SINGLE tac g of 

448 
NONE => raise FAILED () 

449 
 SOME g' => g'); 

32365  450 

42370  451 
val goals = Drule.strip_imp_prems (Thm.cprop_of st); 
452 
val results = Par_List.map (try_tac o init) goals; 

453 
in ALLGOALS (fn i => retrofit i 1 (nth results (i  1))) st end 

454 
handle FAILED () => Seq.empty); 

32365  455 

18207  456 
end; 
457 

32365  458 
structure Basic_Goal: BASIC_GOAL = Goal; 
459 
open Basic_Goal; 