author  wenzelm 
Mon, 31 Jan 2011 23:53:07 +0100  
changeset 41677  fa0da47131d2 
parent 41674  7da257539a8d 
child 41683  73dde8006820 
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 
41677  26 
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

27 
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

28 
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

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

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

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

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

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

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

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

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

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

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

50 
structure Goal: GOAL = 

51 
struct 

52 

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

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

54 

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 
 (init) 
09ab79d4e8e1
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17986
diff
changeset

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

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

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

63 
(* 

18119  64 
C 
65 
 (protect) 

66 
#C 

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

70 
(* 

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

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

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

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

77 
(* 

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

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

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

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

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

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

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

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

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

17980  94 

95 

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

96 

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

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

98 

28340  99 
(* normal form *) 
100 

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

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

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

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

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

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

106 

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

107 

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

108 
(* parallel proofs *) 
349e9223c685
explicit markup for forked goals, as indicated by Goal.fork;
wenzelm
parents:
36613
diff
changeset

109 

41677  110 
fun fork_name name e = 
111 
singleton (Future.forks {name = name, group = NONE, deps = [], pri = ~1}) 

41673  112 
(fn () => Future.status e); 
29448
34b9652b2f45
added Goal.future_enabled abstraction  now also checks that this is already
wenzelm
parents:
29435
diff
changeset

113 

41677  114 
fun fork e = fork_name "Goal.fork" e; 
115 

116 

32738  117 
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

118 

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

119 
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

120 
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

121 

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

122 
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

123 

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

124 

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

125 
(* future_result *) 
28340  126 

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

127 
fun future_result ctxt result prop = 
28340  128 
let 
129 
val thy = ProofContext.theory_of ctxt; 

130 
val _ = Context.reject_draft thy; 

131 
val cert = Thm.cterm_of thy; 

132 
val certT = Thm.ctyp_of thy; 

133 

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

134 
val assms = Assumption.all_assms_of ctxt; 
28340  135 
val As = map Thm.term_of assms; 
136 

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

138 
val fixes = map cert xs; 

139 

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

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

142 

143 
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

144 
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

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

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

147 
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

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

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

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

151 
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

152 
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

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

155 
Thm.future global_result global_prop 
28340  156 
> Thm.instantiate (instT, []) 
157 
> Drule.forall_elim_list fixes 

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

159 
in local_result end; 

160 

161 

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

162 

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

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

164 

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

166 

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

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

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

172 

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

173 

28340  174 
(* prove_common etc. *) 
17986  175 

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

179 
val string_of_term = Syntax.string_of_term ctxt; 
20056  180 

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

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

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

17980  186 

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

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

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

190 
val cprops = map cert_safe props; 
17980  191 

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

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

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

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

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

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

197 
val sorts = Variable.sorts_of ctxt'; 
17980  198 

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

199 
val stmt = Thm.weaken_sorts sorts (Conjunction.mk_conjunction_balanced cprops); 
28340  200 

201 
fun result () = 

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

203 
NONE => err "Tactic failed" 
28340  204 
 SOME st => 
32197  205 
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

206 
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

207 
then Thm.check_shyps sorts res 
28340  208 
else err ("Proved a different theorem: " ^ string_of_term (Thm.prop_of res)) 
209 
end); 

210 
val res = 

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

211 
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

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

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

218 
> map Drule.zero_var_indexes 
17980  219 
end; 
220 

28341  221 
val prove_multi = prove_common true; 
17980  222 

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

223 
fun prove_future ctxt xs asms prop tac = hd (prove_common false ctxt xs asms [prop] tac); 
28340  224 
fun prove ctxt xs asms prop tac = hd (prove_common true ctxt xs asms [prop] tac); 
20056  225 

226 
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

227 
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

228 

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

229 

17980  230 

21687  231 
(** goal structure **) 
232 

233 
(* nested goals *) 

18207  234 

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

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

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

20260  240 
> Seq.map (Thm.adjust_maxidx_cterm ~1 #> init); 
17980  241 

19221  242 
fun retrofit i n st' st = 
243 
(if n = 1 then st 

23418  244 
else st > Drule.with_subgoal i (Conjunction.uncurry_balanced n)) 
19221  245 
> Thm.compose_no_flatten false (conclude st', Thm.nprems_of st') i; 
18207  246 

17980  247 
fun SELECT_GOAL tac i st = 
19191  248 
if Thm.nprems_of st = 1 andalso i = 1 then tac st 
19184  249 
else Seq.lifts (retrofit i 1) (Seq.maps tac (extract i 1 st)) st; 
17980  250 

21687  251 

252 
(* multiple goals *) 

253 

23418  254 
fun precise_conjunction_tac 0 i = eq_assume_tac i 
255 
 precise_conjunction_tac 1 i = SUBGOAL (K all_tac) i 

256 
 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

257 

23418  258 
val adhoc_conjunction_tac = REPEAT_ALL_NEW 
259 
(SUBGOAL (fn (goal, i) => 

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

261 
else no_tac)); 

21687  262 

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

265 
TRY (adhoc_conjunction_tac i)); 

21687  266 

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

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

269 

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

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

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

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

274 

21687  275 
fun CONJUNCTS tac = 
276 
SELECT_GOAL (conjunction_tac 1 

277 
THEN tac 

23418  278 
THEN recover_conjunction_tac); 
21687  279 

280 

281 
(* hhf normal form *) 

282 

283 
val norm_hhf_tac = 

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

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

286 
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

287 
else rewrite_goal_tac Drule.norm_hhf_eqs i); 
21687  288 

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

21687  291 

23237  292 

293 
(* nonatomic goal assumptions *) 

294 

23356  295 
fun non_atomic (Const ("==>", _) $ _ $ _) = true 
296 
 non_atomic (Const ("all", _) $ _) = true 

297 
 non_atomic _ = false; 

298 

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

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

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

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

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

32365  308 

309 
(* parallel tacticals *) 

310 

311 
(*parallel choice of single results*) 

312 
fun PARALLEL_CHOICE tacs st = 

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

314 
NONE => Seq.empty 

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

316 

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

318 
exception FAILED of unit; 
32365  319 
fun PARALLEL_GOALS tac st = 
320 
let 

321 
val st0 = Thm.adjust_maxidx_thm ~1 st; 

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

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

324 

325 
fun try_tac g = 

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

327 
NONE => raise FAILED () 
32365  328 
 SOME g' => g'); 
329 

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

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

332 
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

333 
handle FAILED () => Seq.empty; 
32365  334 

18207  335 
end; 
336 

32365  337 
structure Basic_Goal: BASIC_GOAL = Goal; 
338 
open Basic_Goal; 