author  wenzelm 
Fri, 19 Jul 2013 17:58:57 +0200  
changeset 52710  52790e3961fe 
parent 52696  38466f4f3483 
child 52732  b4da1f2ec73f 
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 

32738  9 
val parallel_proofs: int Unsynchronized.ref 
17980  10 
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

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

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

17980  16 
end; 
17 

18 
signature GOAL = 

19 
sig 

20 
include BASIC_GOAL 

21 
val init: cterm > thm 

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

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

27 
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

28 
val fork: int > (unit > 'a) > 'a future 
52607
33a133d50616
clarified execution: maintain running execs only, check "stable" separately via memo (again);
wenzelm
parents:
52499
diff
changeset

29 
val peek_futures: int > unit future list 
33a133d50616
clarified execution: maintain running execs only, check "stable" separately via memo (again);
wenzelm
parents:
52499
diff
changeset

30 
val stable_futures: int> bool 
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 
52499  33 
val skip_proofs_enabled: unit > bool 
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 

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

55 
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

56 
val unrestrict: int > thm > thm 
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 
23237  61 
val assume_rule_tac: Proof.context > int > tactic 
17980  62 
end; 
63 

64 
structure Goal: GOAL = 

65 
struct 

66 

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

67 
(** goals **) 
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 
(* 
09ab79d4e8e1
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17986
diff
changeset

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

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

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

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

77 
(* 

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

80 
A1 ==> ... ==> An ==> #C 

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

84 
(* 

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

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

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

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

91 
(* 

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

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

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

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

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

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

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

103 

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

104 

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

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

106 

28340  107 
(* normal form *) 
108 

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

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

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

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

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

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

114 

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

115 

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

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

117 

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

118 
local 
41703
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 
val forked_proofs = 
7449b804073b
central management of forked goals wrt. transaction id;
wenzelm
parents:
49041
diff
changeset

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

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

123 

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

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

125 
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

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

127 
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

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

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

130 

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

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

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

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

134 
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

135 
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

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

137 

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

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

139 
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

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

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

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

143 

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

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

145 
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

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

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

148 
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

149 

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

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

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

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

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

155 
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

156 
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

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

158 
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

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

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

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

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

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

164 
 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

165 
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

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

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

168 
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

169 
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

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

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

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

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

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

175 

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

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

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

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

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

180 

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

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

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

183 

52607
33a133d50616
clarified execution: maintain running execs only, check "stable" separately via memo (again);
wenzelm
parents:
52499
diff
changeset

184 
fun stable_futures id = 
33a133d50616
clarified execution: maintain running execs only, check "stable" separately via memo (again);
wenzelm
parents:
52499
diff
changeset

185 
not (Par_Exn.is_interrupted (Future.join_results (peek_futures id))); 
33a133d50616
clarified execution: maintain running execs only, check "stable" separately via memo (again);
wenzelm
parents:
52499
diff
changeset

186 

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

187 
fun reset_futures () = 
51608  188 
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

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

190 

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

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

194 
[] => () 

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

196 

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

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

198 

41677  199 

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

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

201 

52499  202 
fun skip_proofs_enabled () = 
52710
52790e3961fe
just one option "skip_proofs", without direct access within the editor (it makes document processing stateful without strong reasons  monotonic updates already handle goal forks smoothly);
wenzelm
parents:
52696
diff
changeset

203 
let val skip = Options.default_bool "skip_proofs" in 
52499  204 
if Proofterm.proofs_enabled () andalso skip then 
205 
(warning "Proof terms enabled  cannot skip proofs"; false) 

206 
else skip 

207 
end; 

208 

32738  209 
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

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_level n = 
8686c36fa27d
refined treatment of forked proofs at transaction boundaries, including proof commands (see also 7ee000ce5390);
wenzelm
parents:
49009
diff
changeset

212 
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

213 
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

214 

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

215 
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

216 

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

217 
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

218 
future_enabled_level n andalso 
52104  219 
forked_count () < 
220 
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

221 

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

222 
fun future_enabled_timing t = 
52104  223 
future_enabled () andalso 
224 
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

225 

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

226 

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

227 
(* future_result *) 
28340  228 

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

229 
fun future_result ctxt result prop = 
28340  230 
let 
42360  231 
val thy = Proof_Context.theory_of ctxt; 
28340  232 
val cert = Thm.cterm_of thy; 
233 
val certT = Thm.ctyp_of thy; 

234 

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

235 
val assms = Assumption.all_assms_of ctxt; 
28340  236 
val As = map Thm.term_of assms; 
237 

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

239 
val fixes = map cert xs; 

240 

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

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

243 

244 
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

245 
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

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

247 
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

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

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

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

251 
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

252 
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

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

255 
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

256 
> Thm.close_derivation 
28340  257 
> Thm.instantiate (instT, []) 
258 
> Drule.forall_elim_list fixes 

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

260 
in local_result end; 

261 

262 

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

263 

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

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

265 

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

267 

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

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

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

273 

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

274 

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

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

276 

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

277 
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

278 
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

279 
Term.exists_type (Term.exists_subtype Term.is_TVar) t; 
17986  280 

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

284 
val string_of_term = Syntax.string_of_term ctxt; 
20056  285 

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

286 
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

287 
val future = future_enabled (); 
52499  288 
val skip = not immediate andalso not schematic andalso future andalso skip_proofs_enabled (); 
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

289 

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

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

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

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

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

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

299 
val cprops = map cert_safe props; 
17980  300 

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

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

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

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

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

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

306 
val sorts = Variable.sorts_of ctxt'; 
17980  307 

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

308 
val stmt = Thm.weaken_sorts sorts (Conjunction.mk_conjunction_balanced cprops); 
28340  309 

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

310 
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

311 
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

312 
else tac args st; 
28340  313 
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

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

315 
NONE => err "Tactic failed" 
28340  316 
 SOME st => 
32197  317 
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

318 
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

319 
then Thm.check_shyps sorts res 
28340  320 
else err ("Proved a different theorem: " ^ string_of_term (Thm.prop_of res)) 
321 
end); 

322 
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

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

324 
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

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

330 
> map Drule.zero_var_indexes 
17980  331 
end; 
332 

28341  333 
val prove_multi = prove_common true; 
17980  334 

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

335 
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

336 

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

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

339 
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

340 
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

341 

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

344 

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

347 
prove ctxt xs asms prop (fn _ => ALLGOALS Skip_Proof.cheat_tac) 
51551  348 
else (if future_enabled () then prove_future else prove) ctxt xs asms prop tac; 
349 

350 
fun prove_sorry_global thy xs asms prop tac = 

351 
Drule.export_without_context 

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

353 

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

354 

17980  355 

21687  356 
(** goal structure **) 
357 

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

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

359 

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

360 
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

361 
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

362 
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

363 
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

364 

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

365 
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

366 

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

367 
(*with structural marker*) 
17980  368 
fun SELECT_GOAL tac i st = 
19191  369 
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

370 
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

371 

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

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

373 
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

374 
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

375 
else (PRIMITIVE (rotate_prems (i  1)) THEN tac THEN PRIMITIVE (rotate_prems (1  i))) st; 
17980  376 

21687  377 

378 
(* multiple goals *) 

379 

23418  380 
fun precise_conjunction_tac 0 i = eq_assume_tac i 
381 
 precise_conjunction_tac 1 i = SUBGOAL (K all_tac) i 

382 
 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

383 

23418  384 
val adhoc_conjunction_tac = REPEAT_ALL_NEW 
385 
(SUBGOAL (fn (goal, i) => 

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

387 
else no_tac)); 

21687  388 

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

391 
TRY (adhoc_conjunction_tac i)); 

21687  392 

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

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

395 

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

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

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

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

400 

21687  401 
fun CONJUNCTS tac = 
402 
SELECT_GOAL (conjunction_tac 1 

403 
THEN tac 

23418  404 
THEN recover_conjunction_tac); 
21687  405 

406 

407 
(* hhf normal form *) 

408 

409 
val norm_hhf_tac = 

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

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

412 
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

413 
else rewrite_goal_tac Drule.norm_hhf_eqs i); 
21687  414 

23237  415 

416 
(* nonatomic goal assumptions *) 

417 

23356  418 
fun non_atomic (Const ("==>", _) $ _ $ _) = true 
419 
 non_atomic (Const ("all", _) $ _) = true 

420 
 non_atomic _ = false; 

421 

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

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

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

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

32365  431 

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

432 

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

433 
(** parallel tacticals **) 
32365  434 

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

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

436 

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

439 
NONE => Seq.empty 

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

441 

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

442 

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

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

444 

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

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

446 

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

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

448 

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

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

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

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

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

453 

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

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

455 

42370  456 
fun PARALLEL_GOALS tac = 
457 
Thm.adjust_maxidx_thm ~1 #> 

458 
(fn st => 

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

459 
if not (Multithreading.enabled ()) orelse Thm.maxidx_of st >= 0 orelse Thm.nprems_of st <= 1 
42370  460 
then DETERM tac st 
461 
else 

462 
let 

463 
fun try_tac g = 

464 
(case SINGLE tac g of 

465 
NONE => raise FAILED () 

466 
 SOME g' => g'); 

32365  467 

42370  468 
val goals = Drule.strip_imp_prems (Thm.cprop_of st); 
469 
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

470 
in EVERY (map retrofit (rev results)) st end 
42370  471 
handle FAILED () => Seq.empty); 
32365  472 

18207  473 
end; 
474 

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

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

476 

32365  477 
structure Basic_Goal: BASIC_GOAL = Goal; 
478 
open Basic_Goal; 