author  wenzelm 
Tue, 23 Sep 2008 22:04:30 +0200  
changeset 28340  e8597242f649 
parent 27218  4548c83cd508 
child 28341  383f512314b9 
permissions  rwrr 
17980  1 
(* Title: Pure/goal.ML 
2 
ID: $Id$ 

3 
Author: Makarius and Lawrence C Paulson 

4 

18139  5 
Goals in tactical theorem proving. 
17980  6 
*) 
7 

8 
signature BASIC_GOAL = 

9 
sig 

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 
17980  13 
end; 
14 

15 
signature GOAL = 

16 
sig 

17 
include BASIC_GOAL 

18 
val init: cterm > thm 

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

19 
val protect: thm > thm 
17980  20 
val conclude: thm > thm 
21 
val finish: thm > thm 

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

22 
val norm_result: thm > thm 
28340  23 
val promise_result: Proof.context > (unit > thm) > term > thm 
23356  24 
val prove_internal: cterm list > cterm > (thm list > tactic) > thm 
20290  25 
val prove_multi: Proof.context > string list > term list > term list > 
26 
({prems: thm list, context: Proof.context} > tactic) > thm list 

28340  27 
val prove_promise: Proof.context > string list > term list > term > 
28 
({prems: thm list, context: Proof.context} > tactic) > thm 

20290  29 
val prove: Proof.context > string list > term list > term > 
30 
({prems: thm list, context: Proof.context} > tactic) > thm 

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

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

32 
({prems: thm list, context: Proof.context} > tactic) > thm 
19184  33 
val extract: int > int > thm > thm Seq.seq 
34 
val retrofit: int > int > thm > thm > thm Seq.seq 

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

36 
val precise_conjunction_tac: int > int > tactic 
23418  37 
val recover_conjunction_tac: tactic 
21687  38 
val norm_hhf_tac: int > tactic 
39 
val compose_hhf_tac: thm > int > tactic 

23237  40 
val assume_rule_tac: Proof.context > int > tactic 
17980  41 
end; 
42 

43 
structure Goal: GOAL = 

44 
struct 

45 

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

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

47 

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

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

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

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

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

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

56 
(* 

18119  57 
C 
58 
 (protect) 

59 
#C 

17980  60 
*) 
21579  61 
fun protect th = th COMP_INCR Drule.protectI; 
17980  62 

63 
(* 

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

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

65 
 (conclude) 
17980  66 
A ==> ... ==> C 
67 
*) 

68 
fun conclude th = 

18497  69 
(case SINGLE (Thm.compose_no_flatten false (th, Thm.nprems_of th) 1) 
18027
09ab79d4e8e1
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17986
diff
changeset

70 
(Drule.incr_indexes th Drule.protectD) of 
17980  71 
SOME th' => th' 
72 
 NONE => raise THM ("Failed to conclude goal", 0, [th])); 

73 

74 
(* 

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

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

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

77 
C 
17983  78 
*) 
17980  79 
fun finish th = 
80 
(case Thm.nprems_of th of 

81 
0 => conclude th 

82 
 n => raise THM ("Proof failed.\n" ^ 

83 
Pretty.string_of (Pretty.chunks (Display.pretty_goals n th)) ^ 

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

85 

86 

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

87 

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

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

89 

28340  90 
(* normal form *) 
91 

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

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

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

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

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

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

97 

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

98 

28340  99 
(* promise *) 
100 

101 
fun promise_result ctxt result prop = 

102 
let 

103 
val thy = ProofContext.theory_of ctxt; 

104 
val _ = Context.reject_draft thy; 

105 
val cert = Thm.cterm_of thy; 

106 
val certT = Thm.ctyp_of thy; 

107 

108 
val assms = Assumption.assms_of ctxt; 

109 
val As = map Thm.term_of assms; 

110 

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

112 
val fixes = map cert xs; 

113 

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

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

116 

117 
val global_prop = 

118 
Term.map_types Logic.varifyT (fold_rev Logic.all xs (Logic.list_implies (As, prop))); 

119 
val global_result = 

120 
Thm.generalize (map #1 tfrees, []) 0 o 

121 
Drule.forall_intr_list fixes o 

122 
Drule.implies_intr_list assms o 

123 
Thm.adjust_maxidx_thm ~1 o result; 

124 
val local_result = 

125 
Thm.promise (Future.fork_irrelevant global_result) (cert global_prop) 

126 
> Thm.instantiate (instT, []) 

127 
> Drule.forall_elim_list fixes 

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

129 
in local_result end; 

130 

131 

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

132 

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

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

134 

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

136 

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

138 
(case SINGLE (tac (map Assumption.assume casms)) (init cprop) of 
c3f209752749
prove: proper assumption context, more tactic arguments;
wenzelm
parents:
20228
diff
changeset

139 
SOME th => Drule.implies_intr_list casms (finish th) 
c3f209752749
prove: proper assumption context, more tactic arguments;
wenzelm
parents:
20228
diff
changeset

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

141 

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

142 

28340  143 
(* prove_common etc. *) 
17986  144 

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

148 
val string_of_term = Syntax.string_of_term ctxt; 
20056  149 

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

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

151 
("The error(s) above occurred for the goal statement:\n" ^ 
c3f209752749
prove: proper assumption context, more tactic arguments;
wenzelm
parents:
20228
diff
changeset

152 
string_of_term (Logic.list_implies (asms, Logic.mk_conjunction_list props))); 
17980  153 

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

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

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

157 
val cprops = map cert_safe props; 
17980  158 

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

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

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

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

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

163 
> Variable.set_body true; 
17980  164 

28340  165 
val stmt = Conjunction.mk_conjunction_balanced cprops; 
166 

167 
fun result () = 

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

169 
NONE => err "Tactic failed." 
28340  170 
 SOME st => 
171 
let val res = finish st handle THM (msg, _, _) => err msg in 

172 
if Unify.matches_list thy [Thm.term_of stmt] [Thm.prop_of res] then res 

173 
else err ("Proved a different theorem: " ^ string_of_term (Thm.prop_of res)) 

174 
end); 

175 
val res = 

176 
if immediate orelse #maxidx (Thm.rep_cterm stmt) >= 0 then result () 

177 
else promise_result ctxt result (Thm.term_of stmt); 

17980  178 
in 
28340  179 
Conjunction.elim_balanced (length props) res 
20290  180 
> map (Assumption.export false ctxt' ctxt) 
20056  181 
> Variable.export ctxt' ctxt 
20250
c3f209752749
prove: proper assumption context, more tactic arguments;
wenzelm
parents:
20228
diff
changeset

182 
> map Drule.zero_var_indexes 
17980  183 
end; 
184 

28340  185 
val prove_multi = prove_common false; 
17980  186 

28340  187 
fun prove_promise ctxt xs asms prop tac = hd (prove_common false ctxt xs asms [prop] tac); 
188 
fun prove ctxt xs asms prop tac = hd (prove_common true ctxt xs asms [prop] tac); 

20056  189 

190 
fun prove_global thy xs asms prop tac = 

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

191 
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

192 

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

193 

17980  194 

21687  195 
(** goal structure **) 
196 

197 
(* nested goals *) 

18207  198 

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

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

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

20260  204 
> Seq.map (Thm.adjust_maxidx_cterm ~1 #> init); 
17980  205 

19221  206 
fun retrofit i n st' st = 
207 
(if n = 1 then st 

23418  208 
else st > Drule.with_subgoal i (Conjunction.uncurry_balanced n)) 
19221  209 
> Thm.compose_no_flatten false (conclude st', Thm.nprems_of st') i; 
18207  210 

17980  211 
fun SELECT_GOAL tac i st = 
19191  212 
if Thm.nprems_of st = 1 andalso i = 1 then tac st 
19184  213 
else Seq.lifts (retrofit i 1) (Seq.maps tac (extract i 1 st)) st; 
17980  214 

21687  215 

216 
(* multiple goals *) 

217 

23418  218 
fun precise_conjunction_tac 0 i = eq_assume_tac i 
219 
 precise_conjunction_tac 1 i = SUBGOAL (K all_tac) i 

220 
 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

221 

23418  222 
val adhoc_conjunction_tac = REPEAT_ALL_NEW 
223 
(SUBGOAL (fn (goal, i) => 

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

225 
else no_tac)); 

21687  226 

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

229 
TRY (adhoc_conjunction_tac i)); 

21687  230 

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

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

233 

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

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

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

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

238 

21687  239 
fun CONJUNCTS tac = 
240 
SELECT_GOAL (conjunction_tac 1 

241 
THEN tac 

23418  242 
THEN recover_conjunction_tac); 
21687  243 

244 

245 
(* hhf normal form *) 

246 

247 
val norm_hhf_tac = 

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

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

250 
if Drule.is_norm_hhf t then all_tac 

23536
60a1672e298e
moved (asm_)rewrite_goal_tac from goal.ML to meta_simplifier.ML (no longer depends on SELECT_GOAL);
wenzelm
parents:
23418
diff
changeset

251 
else MetaSimplifier.rewrite_goal_tac [Drule.norm_hhf_eq] i); 
21687  252 

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

21687  255 

23237  256 

257 
(* nonatomic goal assumptions *) 

258 

23356  259 
fun non_atomic (Const ("==>", _) $ _ $ _) = true 
260 
 non_atomic (Const ("all", _) $ _) = true 

261 
 non_atomic _ = false; 

262 

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

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

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

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

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

271 

18207  272 
end; 
273 

17980  274 
structure BasicGoal: BASIC_GOAL = Goal; 
275 
open BasicGoal; 