author  wenzelm 
Wed, 12 Aug 2009 00:26:01 +0200  
changeset 32365  9b74d0339c44 
parent 32255  d302f1c9e356 
child 32738  15bb09ca0378 
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 

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

9 
val parallel_proofs: int 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 

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

105 
val parallel_proofs = 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 
c549650d1442
future proofs: pass actual futures to facilitate composite computations;
wenzelm
parents:
28619
diff
changeset

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

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

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

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

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

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

144 
in local_result end; 

145 

146 

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

147 

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

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

149 

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

151 

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

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

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

157 

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

158 

28340  159 
(* prove_common etc. *) 
17986  160 

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

164 
val string_of_term = Syntax.string_of_term ctxt; 
20056  165 

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

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

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

17980  171 

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

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

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

175 
val cprops = map cert_safe props; 
17980  176 

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

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

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

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

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

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

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

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

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

186 
fun result () = 

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

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

191 
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

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

195 
val res = 

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

196 
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

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

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

203 
> map Drule.zero_var_indexes 
17980  204 
end; 
205 

28341  206 
val prove_multi = prove_common true; 
17980  207 

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

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

211 
fun prove_global thy xs asms prop tac = 

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

212 
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

213 

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

214 

17980  215 

21687  216 
(** goal structure **) 
217 

218 
(* nested goals *) 

18207  219 

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

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

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

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

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

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

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

21687  236 

237 
(* multiple goals *) 

238 

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

241 
 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

242 

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

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

246 
else no_tac)); 

21687  247 

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

250 
TRY (adhoc_conjunction_tac i)); 

21687  251 

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

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

254 

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

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

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

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

259 

21687  260 
fun CONJUNCTS tac = 
261 
SELECT_GOAL (conjunction_tac 1 

262 
THEN tac 

23418  263 
THEN recover_conjunction_tac); 
21687  264 

265 

266 
(* hhf normal form *) 

267 

268 
val norm_hhf_tac = 

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

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

271 
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

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

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

21687  276 

23237  277 

278 
(* nonatomic goal assumptions *) 

279 

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

282 
 non_atomic _ = false; 

283 

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

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

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

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

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

292 

32365  293 

294 
(* parallel tacticals *) 

295 

296 
(*parallel choice of single results*) 

297 
fun PARALLEL_CHOICE tacs st = 

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

299 
NONE => Seq.empty 

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

301 

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

303 
fun PARALLEL_GOALS tac st = 

304 
let 

305 
val st0 = Thm.adjust_maxidx_thm ~1 st; 

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

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

308 

309 
exception FAILED; 

310 
fun try_tac g = 

311 
(case SINGLE tac g of 

312 
NONE => raise FAILED 

313 
 SOME g' => g'); 

314 

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

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

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

318 
handle FAILED => Seq.empty; 

319 

18207  320 
end; 
321 

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