author  wenzelm 
Sat, 01 Sep 2012 19:27:28 +0200  
changeset 49061  7449b804073b 
parent 49041  9edfd36a0355 
child 49829  2bc5924b117f 
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 
32197  24 
val check_finished: Proof.context > thm > unit 
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 
7449b804073b
central management of forked goals wrt. transaction id;
wenzelm
parents:
49041
diff
changeset

30 
val cancel_futures: unit > unit 
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 
32197  88 
0 => () 
17980  89 
 n => raise THM ("Proof failed.\n" ^ 
32197  90 
Pretty.string_of (Pretty.chunks 
39125
f45d332a90e3
pretty_goals: turned some global references and function arguments into configuration options (goals_limit = 10, goals_total = true, show_main_goal = false) depending on the context;
wenzelm
parents:
38875
diff
changeset

91 
(Goal_Display.pretty_goals 
f45d332a90e3
pretty_goals: turned some global references and function arguments into configuration options (goals_limit = 10, goals_total = true, show_main_goal = false) depending on the context;
wenzelm
parents:
38875
diff
changeset

92 
(ctxt 
f45d332a90e3
pretty_goals: turned some global references and function arguments into configuration options (goals_limit = 10, goals_total = true, show_main_goal = false) depending on the context;
wenzelm
parents:
38875
diff
changeset

93 
> Config.put Goal_Display.goals_limit n 
f45d332a90e3
pretty_goals: turned some global references and function arguments into configuration options (goals_limit = 10, goals_total = true, show_main_goal = false) depending on the context;
wenzelm
parents:
38875
diff
changeset

94 
> Config.put Goal_Display.show_main_goal true) th)) ^ 
32197  95 
"\n" ^ string_of_int n ^ " unsolved goal(s)!", 0, [th])); 
96 

97 
fun finish ctxt th = (check_finished ctxt th; conclude th); 

17980  98 

99 

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

100 

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

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

102 

28340  103 
(* normal form *) 
104 

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

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

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

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

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

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

110 

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

111 

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

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

113 

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

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

115 

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

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

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

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

119 

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

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

121 
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

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

123 
val n = m + i; 
d27950860514
parallelization of nested Isar proofs is subject to Goal.parallel_proofs_threshold;
wenzelm
parents:
41683
diff
changeset

124 
val _ = 
41776  125 
Multithreading.tracing 2 (fn () => 
41703
d27950860514
parallelization of nested Isar proofs is subject to Goal.parallel_proofs_threshold;
wenzelm
parents:
41683
diff
changeset

126 
("PROOFS " ^ Time.toString (Time.now ()) ^ ": " ^ string_of_int n)); 
49061
7449b804073b
central management of forked goals wrt. transaction id;
wenzelm
parents:
49041
diff
changeset

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

128 

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

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

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

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

132 
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

133 
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

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

135 

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

136 
fun status task markups = 
4680c4046814
further refinement of command status, to accomodate forked proofs;
wenzelm
parents:
49012
diff
changeset

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

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

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

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

141 

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

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

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

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

146 
(case Position.get_id (Position.thread_data ()) of 
7449b804073b
central management of forked goals wrt. transaction id;
wenzelm
parents:
49041
diff
changeset

147 
NONE => 0 
7449b804073b
central management of forked goals wrt. transaction id;
wenzelm
parents:
49041
diff
changeset

148 
 SOME id => Markup.parse_int id); 
7449b804073b
central management of forked goals wrt. transaction id;
wenzelm
parents:
49041
diff
changeset

149 
val _ = count_forked 1; 
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) 
47415
c486ac962b89
tuned future priorities: print 0, goal ~1, execute ~2;
wenzelm
parents:
45458
diff
changeset

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

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 ()); 
4680c4046814
further refinement of command status, to accomodate forked proofs;
wenzelm
parents:
49012
diff
changeset

156 
val _ = status task [Isabelle_Markup.running]; 
4680c4046814
further refinement of command status, to accomodate forked proofs;
wenzelm
parents:
49012
diff
changeset

157 
val result = Exn.capture (Future.interruptible_task e) (); 
49037
d7a1973b063c
more markup for failed goal forks, reusing "bad";
wenzelm
parents:
49036
diff
changeset

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

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

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

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

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

163 
(status task [Isabelle_Markup.failed]; 
9edfd36a0355
more informative error message from failed goal forks (violating oldstyle TTY protocol!);
wenzelm
parents:
49037
diff
changeset

164 
Output.report (Markup.markup_only Isabelle_Markup.bad); 
9edfd36a0355
more informative error message from failed goal forks (violating oldstyle TTY protocol!);
wenzelm
parents:
49037
diff
changeset

165 
Output.error_msg (ML_Compiler.exn_message exn))); 
49061
7449b804073b
central management of forked goals wrt. transaction id;
wenzelm
parents:
49041
diff
changeset

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

167 
in Exn.release result end); 
4680c4046814
further refinement of command status, to accomodate forked proofs;
wenzelm
parents:
49012
diff
changeset

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

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

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

171 

41677  172 
fun fork e = fork_name "Goal.fork" e; 
173 

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

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

175 

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

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

177 
Inttab.lookup_list (#3 (Synchronized.value forked_proofs)) id; 
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 
fun cancel_futures () = 
7449b804073b
central management of forked goals wrt. transaction id;
wenzelm
parents:
49041
diff
changeset

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

181 
(List.app Future.cancel_group groups; (0, [], Inttab.empty))); 
7449b804073b
central management of forked goals wrt. transaction id;
wenzelm
parents:
49041
diff
changeset

182 

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

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

184 

41677  185 

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

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

187 

32738  188 
val parallel_proofs = Unsynchronized.ref 1; 
41819
2d84831dc1a0
scale parallel_proofs_threshold with max_threads_value to improve saturation of cores;
wenzelm
parents:
41776
diff
changeset

189 
val parallel_proofs_threshold = Unsynchronized.ref 50; 
29448
34b9652b2f45
added Goal.future_enabled abstraction  now also checks that this is already
wenzelm
parents:
29435
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_level n = 
8686c36fa27d
refined treatment of forked proofs at transaction boundaries, including proof commands (see also 7ee000ce5390);
wenzelm
parents:
49009
diff
changeset

192 
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

193 
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

194 

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

195 
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

196 

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

197 
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

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

199 
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

200 

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

201 

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

202 
(* future_result *) 
28340  203 

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

204 
fun future_result ctxt result prop = 
28340  205 
let 
42360  206 
val thy = Proof_Context.theory_of ctxt; 
28340  207 
val _ = Context.reject_draft thy; 
208 
val cert = Thm.cterm_of thy; 

209 
val certT = Thm.ctyp_of thy; 

210 

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

211 
val assms = Assumption.all_assms_of ctxt; 
28340  212 
val As = map Thm.term_of assms; 
213 

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

215 
val fixes = map cert xs; 

216 

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

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

219 

220 
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

221 
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

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

223 
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

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

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

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

227 
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

228 
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

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

231 
Thm.future global_result global_prop 
28340  232 
> Thm.instantiate (instT, []) 
233 
> Drule.forall_elim_list fixes 

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

235 
in local_result end; 

236 

237 

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

238 

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

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

240 

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

242 

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

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

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

248 

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

249 

28340  250 
(* prove_common etc. *) 
17986  251 

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

255 
val string_of_term = Syntax.string_of_term ctxt; 
20056  256 

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

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

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

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

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

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

266 
val cprops = map cert_safe props; 
17980  267 

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

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

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

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

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

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

273 
val sorts = Variable.sorts_of ctxt'; 
17980  274 

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

275 
val stmt = Thm.weaken_sorts sorts (Conjunction.mk_conjunction_balanced cprops); 
28340  276 

277 
fun result () = 

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

279 
NONE => err "Tactic failed" 
28340  280 
 SOME st => 
32197  281 
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

282 
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

283 
then Thm.check_shyps sorts res 
28340  284 
else err ("Proved a different theorem: " ^ string_of_term (Thm.prop_of res)) 
285 
end); 

286 
val res = 

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

287 
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

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

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

294 
> map Drule.zero_var_indexes 
17980  295 
end; 
296 

28341  297 
val prove_multi = prove_common true; 
17980  298 

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

299 
fun prove_future ctxt xs asms prop tac = hd (prove_common false ctxt xs asms [prop] tac); 
28340  300 
fun prove ctxt xs asms prop tac = hd (prove_common true ctxt xs asms [prop] tac); 
20056  301 

302 
fun prove_global thy xs asms prop tac = 

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

304 

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

305 

17980  306 

21687  307 
(** goal structure **) 
308 

309 
(* nested goals *) 

18207  310 

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

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

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

20260  316 
> Seq.map (Thm.adjust_maxidx_cterm ~1 #> init); 
17980  317 

19221  318 
fun retrofit i n st' st = 
319 
(if n = 1 then st 

23418  320 
else st > Drule.with_subgoal i (Conjunction.uncurry_balanced n)) 
19221  321 
> Thm.compose_no_flatten false (conclude st', Thm.nprems_of st') i; 
18207  322 

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

21687  327 

328 
(* multiple goals *) 

329 

23418  330 
fun precise_conjunction_tac 0 i = eq_assume_tac i 
331 
 precise_conjunction_tac 1 i = SUBGOAL (K all_tac) i 

332 
 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

333 

23418  334 
val adhoc_conjunction_tac = REPEAT_ALL_NEW 
335 
(SUBGOAL (fn (goal, i) => 

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

337 
else no_tac)); 

21687  338 

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

341 
TRY (adhoc_conjunction_tac i)); 

21687  342 

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

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

345 

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

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

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

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

350 

21687  351 
fun CONJUNCTS tac = 
352 
SELECT_GOAL (conjunction_tac 1 

353 
THEN tac 

23418  354 
THEN recover_conjunction_tac); 
21687  355 

356 

357 
(* hhf normal form *) 

358 

359 
val norm_hhf_tac = 

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

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

362 
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

363 
else rewrite_goal_tac Drule.norm_hhf_eqs i); 
21687  364 

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

21687  367 

23237  368 

369 
(* nonatomic goal assumptions *) 

370 

23356  371 
fun non_atomic (Const ("==>", _) $ _ $ _) = true 
372 
 non_atomic (Const ("all", _) $ _) = true 

373 
 non_atomic _ = false; 

374 

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

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

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

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

32365  384 

385 
(* parallel tacticals *) 

386 

387 
(*parallel choice of single results*) 

388 
fun PARALLEL_CHOICE tacs st = 

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

390 
NONE => Seq.empty 

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

392 

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

394 
exception FAILED of unit; 
42370  395 
fun PARALLEL_GOALS tac = 
396 
Thm.adjust_maxidx_thm ~1 #> 

397 
(fn st => 

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

398 
if not (Multithreading.enabled ()) orelse Thm.maxidx_of st >= 0 orelse Thm.nprems_of st <= 1 
42370  399 
then DETERM tac st 
400 
else 

401 
let 

402 
fun try_tac g = 

403 
(case SINGLE tac g of 

404 
NONE => raise FAILED () 

405 
 SOME g' => g'); 

32365  406 

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

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

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

32365  411 

18207  412 
end; 
413 

32365  414 
structure Basic_Goal: BASIC_GOAL = Goal; 
415 
open Basic_Goal; 