author  paulson 
Fri, 05 Oct 2007 09:59:03 +0200  
changeset 24854  0ebcd575d3c6 
parent 23536  60a1672e298e 
child 25301  24e027f55f45 
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 
1af327306c8e
added norm/close_result (supercede local_standard etc.);
wenzelm
parents:
21579
diff
changeset

23 
val close_result: thm > 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 

27 
val prove: Proof.context > string list > term list > term > 

28 
({prems: thm list, context: Proof.context} > tactic) > thm 

20056  29 
val prove_global: theory > string list > term list > term > (thm list > tactic) > thm 
19184  30 
val extract: int > int > thm > thm Seq.seq 
31 
val retrofit: int > int > thm > thm > thm Seq.seq 

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

33 
val precise_conjunction_tac: int > int > tactic 
23418  34 
val recover_conjunction_tac: tactic 
21687  35 
val norm_hhf_tac: int > tactic 
36 
val compose_hhf: thm > int > thm > thm Seq.seq 

37 
val compose_hhf_tac: thm > int > tactic 

38 
val comp_hhf: thm > thm > thm 

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

42 
structure Goal: GOAL = 

43 
struct 

44 

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

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

46 

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

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

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

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

55 
(* 

18119  56 
C 
57 
 (protect) 

58 
#C 

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

62 
(* 

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

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

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

67 
fun conclude th = 

18497  68 
(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

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

72 

73 
(* 

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

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

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

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

80 
0 => conclude th 

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

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

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

84 

85 

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

86 

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

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

88 

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

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

90 

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

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

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

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

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

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

96 

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

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

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

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

100 

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

101 

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

102 

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

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

104 

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

106 

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

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

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

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

111 

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

112 

18119  113 
(* prove_multi *) 
17986  114 

20056  115 
fun prove_multi ctxt xs asms props tac = 
17980  116 
let 
21516  117 
val thy = ProofContext.theory_of ctxt; 
20056  118 
val string_of_term = Sign.string_of_term thy; 
119 

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

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

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

122 
string_of_term (Logic.list_implies (asms, Logic.mk_conjunction_list props))); 
17980  123 

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

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

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

127 
val cprops = map cert_safe props; 
17980  128 

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

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

130 
> Variable.add_fixes_direct xs 
c3f209752749
prove: proper assumption context, more tactic arguments;
wenzelm
parents:
20228
diff
changeset

131 
> fold Variable.declare_internal (asms @ props) 
c3f209752749
prove: proper assumption context, more tactic arguments;
wenzelm
parents:
20228
diff
changeset

132 
> Assumption.add_assumes casms; 
17980  133 

23418  134 
val goal = init (Conjunction.mk_conjunction_balanced cprops); 
19774
5fe7731d0836
allow nontrivial schematic goals (via embedded term vars);
wenzelm
parents:
19619
diff
changeset

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

136 
(case SINGLE (tac {prems = prems, context = ctxt'}) goal of 
19774
5fe7731d0836
allow nontrivial schematic goals (via embedded term vars);
wenzelm
parents:
19619
diff
changeset

137 
NONE => err "Tactic failed." 
5fe7731d0836
allow nontrivial schematic goals (via embedded term vars);
wenzelm
parents:
19619
diff
changeset

138 
 SOME res => res); 
23418  139 
val results = Conjunction.elim_balanced (length props) (finish res) 
20250
c3f209752749
prove: proper assumption context, more tactic arguments;
wenzelm
parents:
20228
diff
changeset

140 
handle THM (msg, _, _) => err msg; 
c3f209752749
prove: proper assumption context, more tactic arguments;
wenzelm
parents:
20228
diff
changeset

141 
val _ = Unify.matches_list thy (map Thm.term_of cprops) (map Thm.prop_of results) 
20056  142 
orelse err ("Proved a different theorem: " ^ string_of_term (Thm.prop_of res)); 
17980  143 
in 
20056  144 
results 
20290  145 
> map (Assumption.export false ctxt' ctxt) 
20056  146 
> Variable.export ctxt' ctxt 
20250
c3f209752749
prove: proper assumption context, more tactic arguments;
wenzelm
parents:
20228
diff
changeset

147 
> map Drule.zero_var_indexes 
17980  148 
end; 
149 

150 

18119  151 
(* prove *) 
17980  152 

20056  153 
fun prove ctxt xs asms prop tac = hd (prove_multi ctxt xs asms [prop] tac); 
154 

155 
fun prove_global thy xs asms prop tac = 

21516  156 
Drule.standard (prove (ProofContext.init thy) xs asms prop (fn {prems, ...} => tac prems)); 
18027
09ab79d4e8e1
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17986
diff
changeset

157 

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

158 

17980  159 

21687  160 
(** goal structure **) 
161 

162 
(* nested goals *) 

18207  163 

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

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

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

20260  169 
> Seq.map (Thm.adjust_maxidx_cterm ~1 #> init); 
17980  170 

19221  171 
fun retrofit i n st' st = 
172 
(if n = 1 then st 

23418  173 
else st > Drule.with_subgoal i (Conjunction.uncurry_balanced n)) 
19221  174 
> Thm.compose_no_flatten false (conclude st', Thm.nprems_of st') i; 
18207  175 

17980  176 
fun SELECT_GOAL tac i st = 
19191  177 
if Thm.nprems_of st = 1 andalso i = 1 then tac st 
19184  178 
else Seq.lifts (retrofit i 1) (Seq.maps tac (extract i 1 st)) st; 
17980  179 

21687  180 

181 
(* multiple goals *) 

182 

23418  183 
fun precise_conjunction_tac 0 i = eq_assume_tac i 
184 
 precise_conjunction_tac 1 i = SUBGOAL (K all_tac) i 

185 
 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

186 

23418  187 
val adhoc_conjunction_tac = REPEAT_ALL_NEW 
188 
(SUBGOAL (fn (goal, i) => 

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

190 
else no_tac)); 

21687  191 

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

194 
TRY (adhoc_conjunction_tac i)); 

21687  195 

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

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

198 

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

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

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

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

203 

21687  204 
fun CONJUNCTS tac = 
205 
SELECT_GOAL (conjunction_tac 1 

206 
THEN tac 

23418  207 
THEN recover_conjunction_tac); 
21687  208 

209 

210 
(* hhf normal form *) 

211 

212 
val norm_hhf_tac = 

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

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

215 
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

216 
else MetaSimplifier.rewrite_goal_tac [Drule.norm_hhf_eq] i); 
21687  217 

218 
fun compose_hhf tha i thb = 

219 
Thm.bicompose false (false, Drule.lift_all (Thm.cprem_of thb i) tha, 0) i thb; 

220 

221 
fun compose_hhf_tac th i = PRIMSEQ (compose_hhf th i); 

222 

223 
fun comp_hhf tha thb = 

224 
(case Seq.chop 2 (compose_hhf tha 1 thb) of 

225 
([th], _) => th 

226 
 ([], _) => raise THM ("comp_hhf: no unifiers", 1, [tha, thb]) 

227 
 _ => raise THM ("comp_hhf: multiple unifiers", 1, [tha, thb])); 

228 

23237  229 

230 
(* nonatomic goal assumptions *) 

231 

23356  232 
fun non_atomic (Const ("==>", _) $ _ $ _) = true 
233 
 non_atomic (Const ("all", _) $ _) = true 

234 
 non_atomic _ = false; 

235 

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

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

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

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

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

244 

18207  245 
end; 
246 

17980  247 
structure BasicGoal: BASIC_GOAL = Goal; 
248 
open BasicGoal; 