author  wenzelm 
Wed, 13 Feb 2013 21:53:02 +0100  
changeset 51110  ef0592498418 
parent 50987  616789281413 
child 51118  32a5994dd205 
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 
41703
d27950860514
parallelization of nested Isar proofs is subject to Goal.parallel_proofs_threshold;
wenzelm
parents:
41683
diff
changeset

10 
val parallel_proofs_threshold: int Unsynchronized.ref 
17980  11 
val SELECT_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 

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

22 
val protect: 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 
41677  27 
val fork_name: string > (unit > 'a) > 'a future 
37186
349e9223c685
explicit markup for forked goals, as indicated by Goal.fork;
wenzelm
parents:
36613
diff
changeset

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

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

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

31 
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

32 
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

33 
val future_enabled_nested: int > bool 
28973
c549650d1442
future proofs: pass actual futures to facilitate composite computations;
wenzelm
parents:
28619
diff
changeset

34 
val future_result: Proof.context > thm future > term > thm 
23356  35 
val prove_internal: cterm list > cterm > (thm list > tactic) > thm 
20290  36 
val prove_multi: Proof.context > string list > term list > term list > 
37 
({prems: thm list, context: Proof.context} > tactic) > thm list 

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

38 
val prove_future: Proof.context > string list > term list > term > 
28340  39 
({prems: thm list, context: Proof.context} > tactic) > thm 
20290  40 
val prove: Proof.context > string list > term list > term > 
41 
({prems: thm list, context: Proof.context} > tactic) > thm 

26713
1c6181def1d0
prove_global: Variable.set_body true, pass context;
wenzelm
parents:
26628
diff
changeset

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

43 
({prems: thm list, context: Proof.context} > tactic) > thm 
19184  44 
val extract: int > int > thm > thm Seq.seq 
45 
val retrofit: int > int > thm > thm > thm Seq.seq 

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

47 
val precise_conjunction_tac: int > int > tactic 
23418  48 
val recover_conjunction_tac: tactic 
21687  49 
val norm_hhf_tac: int > tactic 
50 
val compose_hhf_tac: thm > int > tactic 

23237  51 
val assume_rule_tac: Proof.context > int > tactic 
17980  52 
end; 
53 

54 
structure Goal: GOAL = 

55 
struct 

56 

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

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

58 

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

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

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

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

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

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

67 
(* 

18119  68 
C 
69 
 (protect) 

70 
#C 

17980  71 
*) 
29345  72 
fun protect th = Drule.comp_no_flatten (th, 0) 1 Drule.protectI; 
17980  73 

74 
(* 

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

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

76 
 (conclude) 
17980  77 
A ==> ... ==> C 
78 
*) 

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

81 
(* 

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

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

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

84 
C 
17983  85 
*) 
32197  86 
fun check_finished ctxt th = 
17980  87 
(case Thm.nprems_of th of 
49845  88 
0 => th 
17980  89 
 n => raise THM ("Proof failed.\n" ^ 
49847  90 
Pretty.string_of (Goal_Display.pretty_goal {main = true, limit = false} ctxt th), 0, [th])); 
32197  91 

49845  92 
fun finish ctxt = check_finished ctxt #> conclude; 
17980  93 

94 

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

95 

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

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

97 

28340  98 
(* normal form *) 
99 

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

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

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

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

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

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

105 

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

106 

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

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

108 

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

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

110 

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

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

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

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

114 

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

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

116 
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

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

118 
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

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

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

121 

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

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

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

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

125 
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

126 
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

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

128 

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

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

130 
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

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

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

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

134 

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

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

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

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

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

140 
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

141 

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

142 
val future = 
44302  143 
(singleton o Future.forks) 
47415
c486ac962b89
tuned future priorities: print 0, goal ~1, execute ~2;
wenzelm
parents:
45458
diff
changeset

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

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

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

147 
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

148 
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

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

150 
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

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

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

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

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

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

156 
 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

157 
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

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

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

160 
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

161 
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

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

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

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

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

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

167 

41677  168 
fun fork e = fork_name "Goal.fork" e; 
169 

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

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

171 

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

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

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

174 

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

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

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

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

178 

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

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

180 

41677  181 

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

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

183 

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

186 

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

187 
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

188 
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

189 
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

190 

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

191 
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

192 

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

193 
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

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

195 
forked_count () < ! parallel_proofs_threshold * Multithreading.max_threads_value (); 
29448
34b9652b2f45
added Goal.future_enabled abstraction  now also checks that this is already
wenzelm
parents:
29435
diff
changeset

196 

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

197 

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

198 
(* future_result *) 
28340  199 

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

200 
fun future_result ctxt result prop = 
28340  201 
let 
42360  202 
val thy = Proof_Context.theory_of ctxt; 
28340  203 
val _ = Context.reject_draft thy; 
204 
val cert = Thm.cterm_of thy; 

205 
val certT = Thm.ctyp_of thy; 

206 

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

207 
val assms = Assumption.all_assms_of ctxt; 
28340  208 
val As = map Thm.term_of assms; 
209 

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

211 
val fixes = map cert xs; 

212 

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

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

215 

216 
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

217 
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

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

219 
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

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

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

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

223 
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

224 
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

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

227 
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

228 
> Thm.close_derivation 
28340  229 
> Thm.instantiate (instT, []) 
230 
> Drule.forall_elim_list fixes 

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

232 
in local_result end; 

233 

234 

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

235 

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

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

237 

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

239 

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

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

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

245 

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

246 

28340  247 
(* prove_common etc. *) 
17986  248 

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

252 
val string_of_term = Syntax.string_of_term ctxt; 
20056  253 

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

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

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

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

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

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

263 
val cprops = map cert_safe props; 
17980  264 

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

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

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

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

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

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

270 
val sorts = Variable.sorts_of ctxt'; 
17980  271 

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

272 
val stmt = Thm.weaken_sorts sorts (Conjunction.mk_conjunction_balanced cprops); 
28340  273 

274 
fun result () = 

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

276 
NONE => err "Tactic failed" 
28340  277 
 SOME st => 
32197  278 
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

279 
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

280 
then Thm.check_shyps sorts res 
28340  281 
else err ("Proved a different theorem: " ^ string_of_term (Thm.prop_of res)) 
282 
end); 

283 
val res = 

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

284 
if immediate orelse #maxidx (Thm.rep_cterm stmt) >= 0 orelse not (future_enabled ()) 
29088
95a239a5e055
future proofs: more robust check via Future.enabled;
wenzelm
parents:
28973
diff
changeset

285 
then result () 
37186
349e9223c685
explicit markup for forked goals, as indicated by Goal.fork;
wenzelm
parents:
36613
diff
changeset

286 
else future_result ctxt' (fork result) (Thm.term_of stmt); 
17980  287 
in 
28340  288 
Conjunction.elim_balanced (length props) res 
20290  289 
> map (Assumption.export false ctxt' ctxt) 
20056  290 
> Variable.export ctxt' ctxt 
20250
c3f209752749
prove: proper assumption context, more tactic arguments;
wenzelm
parents:
20228
diff
changeset

291 
> map Drule.zero_var_indexes 
17980  292 
end; 
293 

28341  294 
val prove_multi = prove_common true; 
17980  295 

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

296 
fun prove_future ctxt xs asms prop tac = hd (prove_common false ctxt xs asms [prop] tac); 
28340  297 
fun prove ctxt xs asms prop tac = hd (prove_common true ctxt xs asms [prop] tac); 
20056  298 

299 
fun prove_global thy xs asms prop tac = 

42360  300 
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

301 

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

302 

17980  303 

21687  304 
(** goal structure **) 
305 

306 
(* nested goals *) 

18207  307 

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

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

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

20260  313 
> Seq.map (Thm.adjust_maxidx_cterm ~1 #> init); 
17980  314 

19221  315 
fun retrofit i n st' st = 
316 
(if n = 1 then st 

23418  317 
else st > Drule.with_subgoal i (Conjunction.uncurry_balanced n)) 
19221  318 
> Thm.compose_no_flatten false (conclude st', Thm.nprems_of st') i; 
18207  319 

17980  320 
fun SELECT_GOAL tac i st = 
19191  321 
if Thm.nprems_of st = 1 andalso i = 1 then tac st 
19184  322 
else Seq.lifts (retrofit i 1) (Seq.maps tac (extract i 1 st)) st; 
17980  323 

21687  324 

325 
(* multiple goals *) 

326 

23418  327 
fun precise_conjunction_tac 0 i = eq_assume_tac i 
328 
 precise_conjunction_tac 1 i = SUBGOAL (K all_tac) i 

329 
 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

330 

23418  331 
val adhoc_conjunction_tac = REPEAT_ALL_NEW 
332 
(SUBGOAL (fn (goal, i) => 

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

334 
else no_tac)); 

21687  335 

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

338 
TRY (adhoc_conjunction_tac i)); 

21687  339 

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

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

342 

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

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

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

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

347 

21687  348 
fun CONJUNCTS tac = 
349 
SELECT_GOAL (conjunction_tac 1 

350 
THEN tac 

23418  351 
THEN recover_conjunction_tac); 
21687  352 

353 

354 
(* hhf normal form *) 

355 

356 
val norm_hhf_tac = 

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

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

359 
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

360 
else rewrite_goal_tac Drule.norm_hhf_eqs i); 
21687  361 

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

21687  364 

23237  365 

366 
(* nonatomic goal assumptions *) 

367 

23356  368 
fun non_atomic (Const ("==>", _) $ _ $ _) = true 
369 
 non_atomic (Const ("all", _) $ _) = true 

370 
 non_atomic _ = false; 

371 

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

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

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

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

32365  381 

382 
(* parallel tacticals *) 

383 

384 
(*parallel choice of single results*) 

385 
fun PARALLEL_CHOICE tacs st = 

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

387 
NONE => Seq.empty 

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

389 

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

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

391 
exception FAILED of unit; 
42370  392 
fun PARALLEL_GOALS tac = 
393 
Thm.adjust_maxidx_thm ~1 #> 

394 
(fn st => 

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

395 
if not (Multithreading.enabled ()) orelse Thm.maxidx_of st >= 0 orelse Thm.nprems_of st <= 1 
42370  396 
then DETERM tac st 
397 
else 

398 
let 

399 
fun try_tac g = 

400 
(case SINGLE tac g of 

401 
NONE => raise FAILED () 

402 
 SOME g' => g'); 

32365  403 

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

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

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

32365  408 

18207  409 
end; 
410 

32365  411 
structure Basic_Goal: BASIC_GOAL = Goal; 
412 
open Basic_Goal; 