author  wenzelm 
Thu, 19 Nov 2009 17:29:39 +0100  
changeset 33768  bba9eac8aa25 
parent 32788  a65deb8f9434 
child 35021  c839a4c670c6 
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 
17980  10 
val SELECT_GOAL: tactic > int > tactic 
23418  11 
val CONJUNCTS: tactic > int > tactic 
23414
927203ad4b3a
tuned conjunction tactics: slightly smaller proof terms;
wenzelm
parents:
23356
diff
changeset

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

17980  15 
end; 
16 

17 
signature GOAL = 

18 
sig 

19 
include BASIC_GOAL 

20 
val init: cterm > thm 

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

21 
val protect: thm > thm 
17980  22 
val conclude: thm > thm 
32197  23 
val check_finished: Proof.context > thm > unit 
24 
val finish: Proof.context > thm > thm 

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

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

26 
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

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

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

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

32 
val prove_future: Proof.context > string list > term list > term > 
28340  33 
({prems: thm list, context: Proof.context} > tactic) > thm 
20290  34 
val prove: Proof.context > string list > term list > term > 
35 
({prems: thm list, context: Proof.context} > tactic) > thm 

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

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

37 
({prems: thm list, context: Proof.context} > tactic) > thm 
19184  38 
val extract: int > int > thm > thm Seq.seq 
39 
val retrofit: int > int > thm > thm > thm Seq.seq 

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

41 
val precise_conjunction_tac: int > int > tactic 
23418  42 
val recover_conjunction_tac: tactic 
21687  43 
val norm_hhf_tac: int > tactic 
44 
val compose_hhf_tac: thm > int > tactic 

23237  45 
val assume_rule_tac: Proof.context > int > tactic 
17980  46 
end; 
47 

48 
structure Goal: GOAL = 

49 
struct 

50 

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

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

52 

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

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

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

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

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

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

61 
(* 

18119  62 
C 
63 
 (protect) 

64 
#C 

17980  65 
*) 
29345  66 
fun protect th = Drule.comp_no_flatten (th, 0) 1 Drule.protectI; 
17980  67 

68 
(* 

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

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

70 
 (conclude) 
17980  71 
A ==> ... ==> C 
72 
*) 

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

75 
(* 

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

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

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

78 
C 
17983  79 
*) 
32197  80 
fun check_finished ctxt th = 
17980  81 
(case Thm.nprems_of th of 
32197  82 
0 => () 
17980  83 
 n => raise THM ("Proof failed.\n" ^ 
32197  84 
Pretty.string_of (Pretty.chunks 
85 
(Goal_Display.pretty_goals ctxt {total = true, main = true, maxgoals = n} th)) ^ 

86 
"\n" ^ string_of_int n ^ " unsolved goal(s)!", 0, [th])); 

87 

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

17980  89 

90 

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

91 

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

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

93 

28340  94 
(* normal form *) 
95 

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

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

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

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

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

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

101 

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

102 

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

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

104 

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

106 

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

107 
fun future_enabled () = 
32255
d302f1c9e356
eliminated separate Future.enabled  let Future.join fail explicitly in critical section, instead of entering sequential mode silently;
wenzelm
parents:
32197
diff
changeset

108 
Multithreading.enabled () andalso Future.is_worker () andalso ! parallel_proofs >= 1; 
32061
11f8ee55662d
parallel_proofs: more finegrained control with optional parallel checking of nested Isar proofs;
wenzelm
parents:
32058
diff
changeset

109 

11f8ee55662d
parallel_proofs: more finegrained control with optional parallel checking of nested Isar proofs;
wenzelm
parents:
32058
diff
changeset

110 
fun local_future_enabled () = future_enabled () andalso ! parallel_proofs >= 2; 
29448
34b9652b2f45
added Goal.future_enabled abstraction  now also checks that this is already
wenzelm
parents:
29435
diff
changeset

111 

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

112 

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

113 
(* future_result *) 
28340  114 

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

115 
fun future_result ctxt result prop = 
28340  116 
let 
117 
val thy = ProofContext.theory_of ctxt; 

118 
val _ = Context.reject_draft thy; 

119 
val cert = Thm.cterm_of thy; 

120 
val certT = Thm.ctyp_of thy; 

121 

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

122 
val assms = Assumption.all_assms_of ctxt; 
28340  123 
val As = map Thm.term_of assms; 
124 

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

126 
val fixes = map cert xs; 

127 

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

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

130 

131 
val global_prop = 

32056
f4b74cbecdaf
future_result: explicitly impose Variable.sorts_of again;
wenzelm
parents:
30473
diff
changeset

132 
cert (Term.map_types Logic.varifyT (fold_rev Logic.all xs (Logic.list_implies (As, prop)))) 
f4b74cbecdaf
future_result: explicitly impose Variable.sorts_of again;
wenzelm
parents:
30473
diff
changeset

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

134 
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

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

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

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

138 
Drule.forall_intr_list fixes #> 
c549650d1442
future proofs: pass actual futures to facilitate composite computations;
wenzelm
parents:
28619
diff
changeset

139 
Thm.generalize (map #1 tfrees, []) 0); 
28340  140 
val local_result = 
32056
f4b74cbecdaf
future_result: explicitly impose Variable.sorts_of again;
wenzelm
parents:
30473
diff
changeset

141 
Thm.future global_result global_prop 
28340  142 
> Thm.instantiate (instT, []) 
143 
> Drule.forall_elim_list fixes 

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

145 
in local_result end; 

146 

147 

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

148 

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

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

150 

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

152 

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

154 
(case SINGLE (tac (map Assumption.assume casms)) (init cprop) of 
32197  155 
SOME th => Drule.implies_intr_list casms 
156 
(finish (Syntax.init_pretty_global (Thm.theory_of_thm th)) th) 

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

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

158 

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

159 

28340  160 
(* prove_common etc. *) 
17986  161 

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

165 
val string_of_term = Syntax.string_of_term ctxt; 
20056  166 

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

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

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

17980  172 

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

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

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

176 
val cprops = map cert_safe props; 
17980  177 

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

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

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

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

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

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

183 
val sorts = Variable.sorts_of ctxt'; 
17980  184 

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

185 
val stmt = Thm.weaken_sorts sorts (Conjunction.mk_conjunction_balanced cprops); 
28340  186 

187 
fun result () = 

188 
(case SINGLE (tac {prems = prems, context = ctxt'}) (init stmt) of 

19774
5fe7731d0836
allow nontrivial schematic goals (via embedded term vars);
wenzelm
parents:
19619
diff
changeset

189 
NONE => err "Tactic failed." 
28340  190 
 SOME st => 
32197  191 
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

192 
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

193 
then Thm.check_shyps sorts res 
28340  194 
else err ("Proved a different theorem: " ^ string_of_term (Thm.prop_of res)) 
195 
end); 

196 
val res = 

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

197 
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

198 
then result () 
32062
457f5bcd3d76
Proof.future_proof: declare all assumptions as well;
wenzelm
parents:
32061
diff
changeset

199 
else future_result ctxt' (Future.fork_pri ~1 result) (Thm.term_of stmt); 
17980  200 
in 
28340  201 
Conjunction.elim_balanced (length props) res 
20290  202 
> map (Assumption.export false ctxt' ctxt) 
20056  203 
> Variable.export ctxt' ctxt 
20250
c3f209752749
prove: proper assumption context, more tactic arguments;
wenzelm
parents:
20228
diff
changeset

204 
> map Drule.zero_var_indexes 
17980  205 
end; 
206 

28341  207 
val prove_multi = prove_common true; 
17980  208 

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

209 
fun prove_future ctxt xs asms prop tac = hd (prove_common false ctxt xs asms [prop] tac); 
28340  210 
fun prove ctxt xs asms prop tac = hd (prove_common true ctxt xs asms [prop] tac); 
20056  211 

212 
fun prove_global thy xs asms prop tac = 

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

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

214 

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

215 

17980  216 

21687  217 
(** goal structure **) 
218 

219 
(* nested goals *) 

18207  220 

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

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

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

20260  226 
> Seq.map (Thm.adjust_maxidx_cterm ~1 #> init); 
17980  227 

19221  228 
fun retrofit i n st' st = 
229 
(if n = 1 then st 

23418  230 
else st > Drule.with_subgoal i (Conjunction.uncurry_balanced n)) 
19221  231 
> Thm.compose_no_flatten false (conclude st', Thm.nprems_of st') i; 
18207  232 

17980  233 
fun SELECT_GOAL tac i st = 
19191  234 
if Thm.nprems_of st = 1 andalso i = 1 then tac st 
19184  235 
else Seq.lifts (retrofit i 1) (Seq.maps tac (extract i 1 st)) st; 
17980  236 

21687  237 

238 
(* multiple goals *) 

239 

23418  240 
fun precise_conjunction_tac 0 i = eq_assume_tac i 
241 
 precise_conjunction_tac 1 i = SUBGOAL (K all_tac) i 

242 
 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

243 

23418  244 
val adhoc_conjunction_tac = REPEAT_ALL_NEW 
245 
(SUBGOAL (fn (goal, i) => 

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

247 
else no_tac)); 

21687  248 

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

251 
TRY (adhoc_conjunction_tac i)); 

21687  252 

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

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

255 

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

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

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

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

260 

21687  261 
fun CONJUNCTS tac = 
262 
SELECT_GOAL (conjunction_tac 1 

263 
THEN tac 

23418  264 
THEN recover_conjunction_tac); 
21687  265 

266 

267 
(* hhf normal form *) 

268 

269 
val norm_hhf_tac = 

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

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

272 
if Drule.is_norm_hhf t then all_tac 

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

273 
else MetaSimplifier.rewrite_goal_tac Drule.norm_hhf_eqs i); 
21687  274 

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

21687  277 

23237  278 

279 
(* nonatomic goal assumptions *) 

280 

23356  281 
fun non_atomic (Const ("==>", _) $ _ $ _) = true 
282 
 non_atomic (Const ("all", _) $ _) = true 

283 
 non_atomic _ = false; 

284 

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

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

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

23356  289 
val Rs = filter (non_atomic o Thm.term_of) (Drule.strip_imp_prems goal''); 
23237  290 
val tacs = Rs > map (fn R => 
291 
Tactic.etac (MetaSimplifier.norm_hhf (Thm.trivial R)) THEN_ALL_NEW assume_tac); 

292 
in fold_rev (curry op APPEND') tacs (K no_tac) i end); 

293 

32365  294 

295 
(* parallel tacticals *) 

296 

297 
(*parallel choice of single results*) 

298 
fun PARALLEL_CHOICE tacs st = 

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

300 
NONE => Seq.empty 

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

302 

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

304 
exception FAILED of unit; 
32365  305 
fun PARALLEL_GOALS tac st = 
306 
let 

307 
val st0 = Thm.adjust_maxidx_thm ~1 st; 

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

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

310 

311 
fun try_tac g = 

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

313 
NONE => raise FAILED () 
32365  314 
 SOME g' => g'); 
315 

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

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

318 
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

319 
handle FAILED () => Seq.empty; 
32365  320 

18207  321 
end; 
322 

32365  323 
structure Basic_Goal: BASIC_GOAL = Goal; 
324 
open Basic_Goal; 