author  wenzelm 
Thu, 27 Jun 2013 10:08:41 +0200  
changeset 52461  ef4c16887f83 
parent 52458  210bca64b894 
child 52499  812215680f6d 
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 
17980  11 
val SELECT_GOAL: tactic > int > tactic 
52458
210bca64b894
less intrusive SELECT_GOAL: merely rearrange subgoals without detaching goal state, and thus preserve maxidx context;
wenzelm
parents:
52456
diff
changeset

12 
val PREFER_GOAL: tactic > int > tactic 
23418  13 
val CONJUNCTS: tactic > int > tactic 
23414
927203ad4b3a
tuned conjunction tactics: slightly smaller proof terms;
wenzelm
parents:
23356
diff
changeset

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

17980  17 
end; 
18 

19 
signature GOAL = 

20 
sig 

21 
include BASIC_GOAL 

22 
val init: cterm > thm 

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

27 
val norm_result: thm > thm 
51605
eca8acb42e4a
more explicit Goal.fork_params  avoid implicit arguments via thread data;
wenzelm
parents:
51553
diff
changeset

28 
val fork_params: {name: string, pos: Position.T, pri: int} > (unit > 'a) > 'a future 
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: int > (unit > 'a) > 'a future 
49061
7449b804073b
central management of forked goals wrt. transaction id;
wenzelm
parents:
49041
diff
changeset

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

31 
val reset_futures: unit > Future.group list 
51276  32 
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

33 
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

34 
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

35 
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

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

37 
val future_result: Proof.context > thm future > term > thm 
23356  38 
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

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

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

42 
val prove_future: Proof.context > string list > term list > term > 
28340  43 
({prems: thm list, context: Proof.context} > tactic) > thm 
20290  44 
val prove: Proof.context > string list > term list > term > 
45 
({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

46 
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

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

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

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

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

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

52458
210bca64b894
less intrusive SELECT_GOAL: merely rearrange subgoals without detaching goal state, and thus preserve maxidx context;
wenzelm
parents:
52456
diff
changeset

54 
val restrict: int > int > thm > thm 
210bca64b894
less intrusive SELECT_GOAL: merely rearrange subgoals without detaching goal state, and thus preserve maxidx context;
wenzelm
parents:
52456
diff
changeset

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

57 
val precise_conjunction_tac: int > int > tactic 
23418  58 
val recover_conjunction_tac: tactic 
21687  59 
val norm_hhf_tac: int > tactic 
23237  60 
val assume_rule_tac: Proof.context > int > tactic 
17980  61 
end; 
62 

63 
structure Goal: GOAL = 

64 
struct 

65 

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

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

67 

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

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

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

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

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

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

76 
(* 

52456  77 
A1 ==> ... ==> An ==> C 
78 
 (protect n) 

79 
A1 ==> ... ==> An ==> #C 

17980  80 
*) 
52456  81 
fun protect n th = Drule.comp_no_flatten (th, n) 1 Drule.protectI; 
17980  82 

83 
(* 

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

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

85 
 (conclude) 
17980  86 
A ==> ... ==> C 
87 
*) 

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

90 
(* 

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

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

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

93 
C 
17983  94 
*) 
32197  95 
fun check_finished ctxt th = 
51608  96 
if Thm.no_prems th then th 
97 
else 

51958
bca32217b304
retain goal display options when printing error messages, to avoid breakdown for huge goals;
wenzelm
parents:
51608
diff
changeset

98 
raise THM ("Proof failed.\n" ^ Pretty.string_of (Goal_Display.pretty_goal ctxt th), 0, [th]); 
32197  99 

49845  100 
fun finish ctxt = check_finished ctxt #> conclude; 
17980  101 

102 

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

103 

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

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

105 

28340  106 
(* normal form *) 
107 

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

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

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

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

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

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

113 

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

114 

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

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

116 

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

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

118 

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

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

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

121 
(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

122 

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

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

124 
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

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

126 
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

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

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

129 

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

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

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

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

133 
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

134 
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

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

136 

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

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

138 
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

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

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

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

142 

51605
eca8acb42e4a
more explicit Goal.fork_params  avoid implicit arguments via thread data;
wenzelm
parents:
51553
diff
changeset

143 
fun fork_params {name, pos, pri} e = 
51607
ee3398dfee9a
recover implicit thread position for status messages (cf. eca8acb42e4a);
wenzelm
parents:
51605
diff
changeset

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

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

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

147 
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

148 

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

149 
val future = 
44302  150 
(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

151 
{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

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

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

154 
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

155 
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

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

157 
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

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

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

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

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

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

163 
 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

164 
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

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

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

167 
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

168 
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

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

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

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

172 
val _ = register_forked id future; 
51607
ee3398dfee9a
recover implicit thread position for status messages (cf. eca8acb42e4a);
wenzelm
parents:
51605
diff
changeset

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

174 

51605
eca8acb42e4a
more explicit Goal.fork_params  avoid implicit arguments via thread data;
wenzelm
parents:
51553
diff
changeset

175 
fun fork pri e = 
eca8acb42e4a
more explicit Goal.fork_params  avoid implicit arguments via thread data;
wenzelm
parents:
51553
diff
changeset

176 
fork_params {name = "Goal.fork", pos = Position.thread_data (), pri = pri} e; 
41677  177 

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

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

179 

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

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

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

182 

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

183 
fun reset_futures () = 
51608  184 
Synchronized.change_result forked_proofs (fn (_, groups, _) => 
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

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

186 

51276  187 
fun shutdown_futures () = 
188 
(Future.shutdown (); 

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

190 
[] => () 

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

192 

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

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

194 

41677  195 

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

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

197 

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

198 
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

199 

32738  200 
val parallel_proofs = Unsynchronized.ref 1; 
29448
34b9652b2f45
added Goal.future_enabled abstraction  now also checks that this is already
wenzelm
parents:
29435
diff
changeset

201 

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

202 
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

203 
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

204 
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

205 

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

206 
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

207 

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

208 
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

209 
future_enabled_level n andalso 
52104  210 
forked_count () < 
211 
Options.default_int "parallel_subproofs_saturation" * Multithreading.max_threads_value (); 

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

212 

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

213 
fun future_enabled_timing t = 
52104  214 
future_enabled () andalso 
215 
Time.toReal t >= Options.default_real "parallel_subproofs_threshold"; 

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

216 

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

217 

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

218 
(* future_result *) 
28340  219 

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

220 
fun future_result ctxt result prop = 
28340  221 
let 
42360  222 
val thy = Proof_Context.theory_of ctxt; 
28340  223 
val _ = Context.reject_draft thy; 
224 
val cert = Thm.cterm_of thy; 

225 
val certT = Thm.ctyp_of thy; 

226 

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

227 
val assms = Assumption.all_assms_of ctxt; 
28340  228 
val As = map Thm.term_of assms; 
229 

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

231 
val fixes = map cert xs; 

232 

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

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

235 

236 
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

237 
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

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

239 
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

240 
(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

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

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

243 
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

244 
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

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

247 
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

248 
> Thm.close_derivation 
28340  249 
> Thm.instantiate (instT, []) 
250 
> Drule.forall_elim_list fixes 

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

252 
in local_result end; 

253 

254 

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

255 

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

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

257 

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

259 

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

261 
(case SINGLE (tac (map Assumption.assume casms)) (init cprop) of 
32197  262 
SOME th => Drule.implies_intr_list casms 
263 
(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

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

265 

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

266 

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

267 
(* 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

268 

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

269 
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

270 
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

271 
Term.exists_type (Term.exists_subtype Term.is_TVar) t; 
17986  272 

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

276 
val string_of_term = Syntax.string_of_term ctxt; 
20056  277 

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

278 
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

279 
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

280 
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

281 

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

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

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

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

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

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

291 
val cprops = map cert_safe props; 
17980  292 

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

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

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

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

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

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

298 
val sorts = Variable.sorts_of ctxt'; 
17980  299 

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

300 
val stmt = Thm.weaken_sorts sorts (Conjunction.mk_conjunction_balanced cprops); 
28340  301 

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

302 
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

303 
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

304 
else tac args st; 
28340  305 
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

306 
(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

307 
NONE => err "Tactic failed" 
28340  308 
 SOME st => 
32197  309 
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

310 
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

311 
then Thm.check_shyps sorts res 
28340  312 
else err ("Proved a different theorem: " ^ string_of_term (Thm.prop_of res)) 
313 
end); 

314 
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

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

316 
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

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

322 
> map Drule.zero_var_indexes 
17980  323 
end; 
324 

28341  325 
val prove_multi = prove_common true; 
17980  326 

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

327 
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

328 

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

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

331 
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

332 
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

333 

20056  334 
fun prove_global thy xs asms prop tac = 
42360  335 
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

336 

51551  337 
fun prove_sorry ctxt xs asms prop tac = 
52059  338 
if Config.get ctxt quick_and_dirty then 
51552
c713c9505f68
clarified Skip_Proof.cheat_tac: more standard tactic;
wenzelm
parents:
51551
diff
changeset

339 
prove ctxt xs asms prop (fn _ => ALLGOALS Skip_Proof.cheat_tac) 
51551  340 
else (if future_enabled () then prove_future else prove) ctxt xs asms prop tac; 
341 

342 
fun prove_sorry_global thy xs asms prop tac = 

343 
Drule.export_without_context 

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

345 

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

346 

17980  347 

21687  348 
(** goal structure **) 
349 

52458
210bca64b894
less intrusive SELECT_GOAL: merely rearrange subgoals without detaching goal state, and thus preserve maxidx context;
wenzelm
parents:
52456
diff
changeset

350 
(* rearrange subgoals *) 
210bca64b894
less intrusive SELECT_GOAL: merely rearrange subgoals without detaching goal state, and thus preserve maxidx context;
wenzelm
parents:
52456
diff
changeset

351 

210bca64b894
less intrusive SELECT_GOAL: merely rearrange subgoals without detaching goal state, and thus preserve maxidx context;
wenzelm
parents:
52456
diff
changeset

352 
fun restrict i n st = 
210bca64b894
less intrusive SELECT_GOAL: merely rearrange subgoals without detaching goal state, and thus preserve maxidx context;
wenzelm
parents:
52456
diff
changeset

353 
if i < 1 orelse n < 1 orelse i + n  1 > Thm.nprems_of st 
210bca64b894
less intrusive SELECT_GOAL: merely rearrange subgoals without detaching goal state, and thus preserve maxidx context;
wenzelm
parents:
52456
diff
changeset

354 
then raise THM ("Goal.restrict", i, [st]) 
210bca64b894
less intrusive SELECT_GOAL: merely rearrange subgoals without detaching goal state, and thus preserve maxidx context;
wenzelm
parents:
52456
diff
changeset

355 
else rotate_prems (i  1) st > protect n; 
210bca64b894
less intrusive SELECT_GOAL: merely rearrange subgoals without detaching goal state, and thus preserve maxidx context;
wenzelm
parents:
52456
diff
changeset

356 

210bca64b894
less intrusive SELECT_GOAL: merely rearrange subgoals without detaching goal state, and thus preserve maxidx context;
wenzelm
parents:
52456
diff
changeset

357 
fun unrestrict i = conclude #> rotate_prems (1  i); 
210bca64b894
less intrusive SELECT_GOAL: merely rearrange subgoals without detaching goal state, and thus preserve maxidx context;
wenzelm
parents:
52456
diff
changeset

358 

210bca64b894
less intrusive SELECT_GOAL: merely rearrange subgoals without detaching goal state, and thus preserve maxidx context;
wenzelm
parents:
52456
diff
changeset

359 
(*with structural marker*) 
17980  360 
fun SELECT_GOAL tac i st = 
19191  361 
if Thm.nprems_of st = 1 andalso i = 1 then tac st 
52458
210bca64b894
less intrusive SELECT_GOAL: merely rearrange subgoals without detaching goal state, and thus preserve maxidx context;
wenzelm
parents:
52456
diff
changeset

362 
else (PRIMITIVE (restrict i 1) THEN tac THEN PRIMITIVE (unrestrict i)) st; 
210bca64b894
less intrusive SELECT_GOAL: merely rearrange subgoals without detaching goal state, and thus preserve maxidx context;
wenzelm
parents:
52456
diff
changeset

363 

210bca64b894
less intrusive SELECT_GOAL: merely rearrange subgoals without detaching goal state, and thus preserve maxidx context;
wenzelm
parents:
52456
diff
changeset

364 
(*without structural marker*) 
210bca64b894
less intrusive SELECT_GOAL: merely rearrange subgoals without detaching goal state, and thus preserve maxidx context;
wenzelm
parents:
52456
diff
changeset

365 
fun PREFER_GOAL tac i st = 
210bca64b894
less intrusive SELECT_GOAL: merely rearrange subgoals without detaching goal state, and thus preserve maxidx context;
wenzelm
parents:
52456
diff
changeset

366 
if i < 1 orelse i > Thm.nprems_of st then Seq.empty 
210bca64b894
less intrusive SELECT_GOAL: merely rearrange subgoals without detaching goal state, and thus preserve maxidx context;
wenzelm
parents:
52456
diff
changeset

367 
else (PRIMITIVE (rotate_prems (i  1)) THEN tac THEN PRIMITIVE (rotate_prems (1  i))) st; 
17980  368 

21687  369 

370 
(* multiple goals *) 

371 

23418  372 
fun precise_conjunction_tac 0 i = eq_assume_tac i 
373 
 precise_conjunction_tac 1 i = SUBGOAL (K all_tac) i 

374 
 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

375 

23418  376 
val adhoc_conjunction_tac = REPEAT_ALL_NEW 
377 
(SUBGOAL (fn (goal, i) => 

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

379 
else no_tac)); 

21687  380 

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

383 
TRY (adhoc_conjunction_tac i)); 

21687  384 

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

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

387 

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

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

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

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

392 

21687  393 
fun CONJUNCTS tac = 
394 
SELECT_GOAL (conjunction_tac 1 

395 
THEN tac 

23418  396 
THEN recover_conjunction_tac); 
21687  397 

398 

399 
(* hhf normal form *) 

400 

401 
val norm_hhf_tac = 

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

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

404 
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

405 
else rewrite_goal_tac Drule.norm_hhf_eqs i); 
21687  406 

23237  407 

408 
(* nonatomic goal assumptions *) 

409 

23356  410 
fun non_atomic (Const ("==>", _) $ _ $ _) = true 
411 
 non_atomic (Const ("all", _) $ _) = true 

412 
 non_atomic _ = false; 

413 

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

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

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

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

32365  423 

52461
ef4c16887f83
more scalable PARALLEL_GOALS, using more elementary retrofit;
wenzelm
parents:
52458
diff
changeset

424 

ef4c16887f83
more scalable PARALLEL_GOALS, using more elementary retrofit;
wenzelm
parents:
52458
diff
changeset

425 
(** parallel tacticals **) 
32365  426 

52461
ef4c16887f83
more scalable PARALLEL_GOALS, using more elementary retrofit;
wenzelm
parents:
52458
diff
changeset

427 
(* parallel choice of single results *) 
ef4c16887f83
more scalable PARALLEL_GOALS, using more elementary retrofit;
wenzelm
parents:
52458
diff
changeset

428 

32365  429 
fun PARALLEL_CHOICE tacs st = 
430 
(case Par_List.get_some (fn tac => SINGLE tac st) tacs of 

431 
NONE => Seq.empty 

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

433 

52461
ef4c16887f83
more scalable PARALLEL_GOALS, using more elementary retrofit;
wenzelm
parents:
52458
diff
changeset

434 

ef4c16887f83
more scalable PARALLEL_GOALS, using more elementary retrofit;
wenzelm
parents:
52458
diff
changeset

435 
(* parallel refinement of nonschematic goal by single results *) 
ef4c16887f83
more scalable PARALLEL_GOALS, using more elementary retrofit;
wenzelm
parents:
52458
diff
changeset

436 

ef4c16887f83
more scalable PARALLEL_GOALS, using more elementary retrofit;
wenzelm
parents:
52458
diff
changeset

437 
local 
ef4c16887f83
more scalable PARALLEL_GOALS, using more elementary retrofit;
wenzelm
parents:
52458
diff
changeset

438 

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

439 
exception FAILED of unit; 
52461
ef4c16887f83
more scalable PARALLEL_GOALS, using more elementary retrofit;
wenzelm
parents:
52458
diff
changeset

440 

ef4c16887f83
more scalable PARALLEL_GOALS, using more elementary retrofit;
wenzelm
parents:
52458
diff
changeset

441 
fun retrofit st' = 
ef4c16887f83
more scalable PARALLEL_GOALS, using more elementary retrofit;
wenzelm
parents:
52458
diff
changeset

442 
rotate_prems ~1 #> 
ef4c16887f83
more scalable PARALLEL_GOALS, using more elementary retrofit;
wenzelm
parents:
52458
diff
changeset

443 
Thm.bicompose {flatten = false, match = false, incremented = false} 
ef4c16887f83
more scalable PARALLEL_GOALS, using more elementary retrofit;
wenzelm
parents:
52458
diff
changeset

444 
(false, conclude st', Thm.nprems_of st') 1; 
ef4c16887f83
more scalable PARALLEL_GOALS, using more elementary retrofit;
wenzelm
parents:
52458
diff
changeset

445 

ef4c16887f83
more scalable PARALLEL_GOALS, using more elementary retrofit;
wenzelm
parents:
52458
diff
changeset

446 
in 
ef4c16887f83
more scalable PARALLEL_GOALS, using more elementary retrofit;
wenzelm
parents:
52458
diff
changeset

447 

42370  448 
fun PARALLEL_GOALS tac = 
449 
Thm.adjust_maxidx_thm ~1 #> 

450 
(fn st => 

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

451 
if not (Multithreading.enabled ()) orelse Thm.maxidx_of st >= 0 orelse Thm.nprems_of st <= 1 
42370  452 
then DETERM tac st 
453 
else 

454 
let 

455 
fun try_tac g = 

456 
(case SINGLE tac g of 

457 
NONE => raise FAILED () 

458 
 SOME g' => g'); 

32365  459 

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

52461
ef4c16887f83
more scalable PARALLEL_GOALS, using more elementary retrofit;
wenzelm
parents:
52458
diff
changeset

462 
in EVERY (map retrofit (rev results)) st end 
42370  463 
handle FAILED () => Seq.empty); 
32365  464 

18207  465 
end; 
466 

52461
ef4c16887f83
more scalable PARALLEL_GOALS, using more elementary retrofit;
wenzelm
parents:
52458
diff
changeset

467 
end; 
ef4c16887f83
more scalable PARALLEL_GOALS, using more elementary retrofit;
wenzelm
parents:
52458
diff
changeset

468 

32365  469 
structure Basic_Goal: BASIC_GOAL = Goal; 
470 
open Basic_Goal; 