author  wenzelm 
Fri, 18 Feb 2011 16:11:58 +0100  
changeset 41776  3bd83302a3c3 
parent 41703  d27950860514 
child 41819  2d84831dc1a0 
permissions  rwrr 
17980  1 
(* Title: Pure/goal.ML 
29345  2 
Author: Makarius 
17980  3 

18139  4 
Goals in tactical theorem proving. 
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 
29448
34b9652b2f45
added Goal.future_enabled abstraction  now also checks that this is already
wenzelm
parents:
29435
diff
changeset

29 
val future_enabled: unit > bool 
32061
11f8ee55662d
parallel_proofs: more finegrained control with optional parallel checking of nested Isar proofs;
wenzelm
parents:
32058
diff
changeset

30 
val local_future_enabled: unit > bool 
28973
c549650d1442
future proofs: pass actual futures to facilitate composite computations;
wenzelm
parents:
28619
diff
changeset

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

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

35 
val prove_future: Proof.context > string list > term list > term > 
28340  36 
({prems: thm list, context: Proof.context} > tactic) > thm 
20290  37 
val prove: Proof.context > string list > term list > term > 
38 
({prems: thm list, context: Proof.context} > tactic) > thm 

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

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

40 
({prems: thm list, context: Proof.context} > tactic) > thm 
19184  41 
val extract: int > int > thm > thm Seq.seq 
42 
val retrofit: int > int > thm > thm > thm Seq.seq 

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

44 
val precise_conjunction_tac: int > int > tactic 
23418  45 
val recover_conjunction_tac: tactic 
21687  46 
val norm_hhf_tac: int > tactic 
47 
val compose_hhf_tac: thm > int > tactic 

23237  48 
val assume_rule_tac: Proof.context > int > tactic 
17980  49 
end; 
50 

51 
structure Goal: GOAL = 

52 
struct 

53 

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

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

55 

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

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

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

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

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

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

64 
(* 

18119  65 
C 
66 
 (protect) 

67 
#C 

17980  68 
*) 
29345  69 
fun protect th = Drule.comp_no_flatten (th, 0) 1 Drule.protectI; 
17980  70 

71 
(* 

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

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

73 
 (conclude) 
17980  74 
A ==> ... ==> C 
75 
*) 

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

78 
(* 

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

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

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

81 
C 
17983  82 
*) 
32197  83 
fun check_finished ctxt th = 
17980  84 
(case Thm.nprems_of th of 
32197  85 
0 => () 
17980  86 
 n => raise THM ("Proof failed.\n" ^ 
32197  87 
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

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

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

90 
> 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

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

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

17980  95 

96 

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

97 

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

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

99 

28340  100 
(* normal form *) 
101 

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

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

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

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

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

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

107 

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

108 

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

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

110 

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

111 
val forked_proofs = Synchronized.var "forked_proofs" 0; 
d27950860514
parallelization of nested Isar proofs is subject to Goal.parallel_proofs_threshold;
wenzelm
parents:
41683
diff
changeset

112 

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

113 
fun forked i = 
d27950860514
parallelization of nested Isar proofs is subject to Goal.parallel_proofs_threshold;
wenzelm
parents:
41683
diff
changeset

114 
Synchronized.change forked_proofs (fn m => 
d27950860514
parallelization of nested Isar proofs is subject to Goal.parallel_proofs_threshold;
wenzelm
parents:
41683
diff
changeset

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

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

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

119 
("PROOFS " ^ Time.toString (Time.now ()) ^ ": " ^ string_of_int n)); 
d27950860514
parallelization of nested Isar proofs is subject to Goal.parallel_proofs_threshold;
wenzelm
parents:
41683
diff
changeset

120 
in n end); 
37186
349e9223c685
explicit markup for forked goals, as indicated by Goal.fork;
wenzelm
parents:
36613
diff
changeset

121 

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

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

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

125 
val _ = forked 1; 
d27950860514
parallelization of nested Isar proofs is subject to Goal.parallel_proofs_threshold;
wenzelm
parents:
41683
diff
changeset

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

127 
singleton (Future.forks {name = name, group = NONE, deps = [], pri = ~1}) 
d27950860514
parallelization of nested Isar proofs is subject to Goal.parallel_proofs_threshold;
wenzelm
parents:
41683
diff
changeset

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

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

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

131 
(Exn.capture Future.status e before forked ~1 
d27950860514
parallelization of nested Isar proofs is subject to Goal.parallel_proofs_threshold;
wenzelm
parents:
41683
diff
changeset

132 
handle exn => (forked ~1; reraise exn))); 
d27950860514
parallelization of nested Isar proofs is subject to Goal.parallel_proofs_threshold;
wenzelm
parents:
41683
diff
changeset

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

134 

41677  135 
fun fork e = fork_name "Goal.fork" e; 
136 

137 

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

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

139 

32738  140 
val parallel_proofs = Unsynchronized.ref 1; 
41703
d27950860514
parallelization of nested Isar proofs is subject to Goal.parallel_proofs_threshold;
wenzelm
parents:
41683
diff
changeset

141 
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

142 

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

143 
fun future_enabled () = 
41703
d27950860514
parallelization of nested Isar proofs is subject to Goal.parallel_proofs_threshold;
wenzelm
parents:
41683
diff
changeset

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

145 
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

146 

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

147 
fun local_future_enabled () = 
d27950860514
parallelization of nested Isar proofs is subject to Goal.parallel_proofs_threshold;
wenzelm
parents:
41683
diff
changeset

148 
future_enabled () andalso ! parallel_proofs >= 2 andalso 
d27950860514
parallelization of nested Isar proofs is subject to Goal.parallel_proofs_threshold;
wenzelm
parents:
41683
diff
changeset

149 
Synchronized.value forked_proofs < ! parallel_proofs_threshold; 
29448
34b9652b2f45
added Goal.future_enabled abstraction  now also checks that this is already
wenzelm
parents:
29435
diff
changeset

150 

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

151 

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

152 
(* future_result *) 
28340  153 

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

154 
fun future_result ctxt result prop = 
28340  155 
let 
156 
val thy = ProofContext.theory_of ctxt; 

157 
val _ = Context.reject_draft thy; 

158 
val cert = Thm.cterm_of thy; 

159 
val certT = Thm.ctyp_of thy; 

160 

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

161 
val assms = Assumption.all_assms_of ctxt; 
28340  162 
val As = map Thm.term_of assms; 
163 

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

165 
val fixes = map cert xs; 

166 

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

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

169 

170 
val global_prop = 

35845
e5980f0ad025
renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
wenzelm
parents:
35021
diff
changeset

171 
cert (Term.map_types Logic.varifyT_global 
e5980f0ad025
renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
wenzelm
parents:
35021
diff
changeset

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

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

174 
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

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

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

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

178 
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

179 
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

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

182 
Thm.future global_result global_prop 
28340  183 
> Thm.instantiate (instT, []) 
184 
> Drule.forall_elim_list fixes 

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

186 
in local_result end; 

187 

188 

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

189 

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

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

191 

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

193 

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

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

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

199 

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

200 

28340  201 
(* prove_common etc. *) 
17986  202 

28340  203 
fun prove_common immediate ctxt xs asms props tac = 
17980  204 
let 
21516  205 
val thy = ProofContext.theory_of ctxt; 
26939
1035c89b4c02
moved global pretty/string_of functions from Sign to Syntax;
wenzelm
parents:
26713
diff
changeset

206 
val string_of_term = Syntax.string_of_term ctxt; 
20056  207 

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

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

210 
("The error(s) above occurred for the goal statement:\n" ^ 
28355  211 
string_of_term (Logic.list_implies (asms, Logic.mk_conjunction_list props)) ^ 
212 
(case Position.str_of pos of "" => ""  s => "\n" ^ s)); 

17980  213 

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

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

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

217 
val cprops = map cert_safe props; 
17980  218 

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

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

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

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

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

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

224 
val sorts = Variable.sorts_of ctxt'; 
17980  225 

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

226 
val stmt = Thm.weaken_sorts sorts (Conjunction.mk_conjunction_balanced cprops); 
28340  227 

228 
fun result () = 

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

230 
NONE => err "Tactic failed" 
28340  231 
 SOME st => 
32197  232 
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

233 
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

234 
then Thm.check_shyps sorts res 
28340  235 
else err ("Proved a different theorem: " ^ string_of_term (Thm.prop_of res)) 
236 
end); 

237 
val res = 

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

238 
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

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

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

245 
> map Drule.zero_var_indexes 
17980  246 
end; 
247 

28341  248 
val prove_multi = prove_common true; 
17980  249 

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

250 
fun prove_future ctxt xs asms prop tac = hd (prove_common false ctxt xs asms [prop] tac); 
28340  251 
fun prove ctxt xs asms prop tac = hd (prove_common true ctxt xs asms [prop] tac); 
20056  252 

253 
fun prove_global thy xs asms prop tac = 

36610
bafd82950e24
renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
wenzelm
parents:
35845
diff
changeset

254 
Drule.export_without_context (prove (ProofContext.init_global thy) xs asms prop tac); 
18027
09ab79d4e8e1
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17986
diff
changeset

255 

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

256 

17980  257 

21687  258 
(** goal structure **) 
259 

260 
(* nested goals *) 

18207  261 

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

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

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

20260  267 
> Seq.map (Thm.adjust_maxidx_cterm ~1 #> init); 
17980  268 

19221  269 
fun retrofit i n st' st = 
270 
(if n = 1 then st 

23418  271 
else st > Drule.with_subgoal i (Conjunction.uncurry_balanced n)) 
19221  272 
> Thm.compose_no_flatten false (conclude st', Thm.nprems_of st') i; 
18207  273 

17980  274 
fun SELECT_GOAL tac i st = 
19191  275 
if Thm.nprems_of st = 1 andalso i = 1 then tac st 
19184  276 
else Seq.lifts (retrofit i 1) (Seq.maps tac (extract i 1 st)) st; 
17980  277 

21687  278 

279 
(* multiple goals *) 

280 

23418  281 
fun precise_conjunction_tac 0 i = eq_assume_tac i 
282 
 precise_conjunction_tac 1 i = SUBGOAL (K all_tac) i 

283 
 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

284 

23418  285 
val adhoc_conjunction_tac = REPEAT_ALL_NEW 
286 
(SUBGOAL (fn (goal, i) => 

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

288 
else no_tac)); 

21687  289 

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

292 
TRY (adhoc_conjunction_tac i)); 

21687  293 

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

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

296 

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

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

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

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

301 

21687  302 
fun CONJUNCTS tac = 
303 
SELECT_GOAL (conjunction_tac 1 

304 
THEN tac 

23418  305 
THEN recover_conjunction_tac); 
21687  306 

307 

308 
(* hhf normal form *) 

309 

310 
val norm_hhf_tac = 

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

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

313 
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

314 
else rewrite_goal_tac Drule.norm_hhf_eqs i); 
21687  315 

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

21687  318 

23237  319 

320 
(* nonatomic goal assumptions *) 

321 

23356  322 
fun non_atomic (Const ("==>", _) $ _ $ _) = true 
323 
 non_atomic (Const ("all", _) $ _) = true 

324 
 non_atomic _ = false; 

325 

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

328 
val ((_, goal'), ctxt') = Variable.focus goal ctxt; 

329 
val goal'' = Drule.cterm_rule (singleton (Variable.export ctxt' ctxt)) goal'; 

23356  330 
val Rs = filter (non_atomic o Thm.term_of) (Drule.strip_imp_prems goal''); 
23237  331 
val tacs = Rs > map (fn R => 
41228
e1fce873b814
renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
wenzelm
parents:
39125
diff
changeset

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

32365  335 

336 
(* parallel tacticals *) 

337 

338 
(*parallel choice of single results*) 

339 
fun PARALLEL_CHOICE tacs st = 

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

341 
NONE => Seq.empty 

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

343 

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

345 
exception FAILED of unit; 
32365  346 
fun PARALLEL_GOALS tac st = 
347 
let 

348 
val st0 = Thm.adjust_maxidx_thm ~1 st; 

349 
val _ = Thm.maxidx_of st0 >= 0 andalso 

350 
raise THM ("PARALLEL_GOALS: schematic goal state", 0, [st]); 

351 

352 
fun try_tac g = 

353 
(case SINGLE tac g of 

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

354 
NONE => raise FAILED () 
32365  355 
 SOME g' => g'); 
356 

357 
val goals = Drule.strip_imp_prems (Thm.cprop_of st0); 

358 
val results = Par_List.map (try_tac o init) goals; 

359 
in ALLGOALS (fn i => retrofit i 1 (nth results (i  1))) st0 end 

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

360 
handle FAILED () => Seq.empty; 
32365  361 

18207  362 
end; 
363 

32365  364 
structure Basic_Goal: BASIC_GOAL = Goal; 
365 
open Basic_Goal; 