author  wenzelm 
Mon, 04 Jun 2007 21:04:19 +0200  
changeset 23237  ac9d126456e1 
parent 22902  ac833b4bb7ee 
child 23356  dbe3731241c3 
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 

21687  11 
val CONJUNCTS: tactic > int > tactic 
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 
20250
c3f209752749
prove: proper assumption context, more tactic arguments;
wenzelm
parents:
20228
diff
changeset

24 
val prove_raw: 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 

21687  32 
val conjunction_tac: int > tactic 
33 
val precise_conjunction_tac: int > int > tactic 

34 
val asm_rewrite_goal_tac: bool * bool * bool > (simpset > tactic) > simpset > int > tactic 

35 
val rewrite_goal_tac: thm list > int > tactic 

36 
val norm_hhf_tac: int > tactic 

37 
val compose_hhf: thm > int > thm > thm Seq.seq 

38 
val compose_hhf_tac: thm > int > tactic 

39 
val comp_hhf: thm > thm > thm 

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 

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

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

91 

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 
val close_result = 
1af327306c8e
added norm/close_result (supercede local_standard etc.);
wenzelm
parents:
21579
diff
changeset

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

100 
#> Drule.close_derivation; 
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 

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

103 

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

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

105 

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

106 
(* prove_raw  no checks, no normalization of result! *) 
c3f209752749
prove: proper assumption context, more tactic arguments;
wenzelm
parents:
20228
diff
changeset

107 

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

108 
fun prove_raw casms cprop tac = 
c3f209752749
prove: proper assumption context, more tactic arguments;
wenzelm
parents:
20228
diff
changeset

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

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

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

112 

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

113 

18119  114 
(* prove_multi *) 
17986  115 

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

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

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

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

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

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

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

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

128 
val cprops = map cert_safe props; 
17980  129 

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

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

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

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

133 
> Assumption.add_assumes casms; 
17980  134 

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

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

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

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

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

139 
 SOME res => res); 
20250
c3f209752749
prove: proper assumption context, more tactic arguments;
wenzelm
parents:
20228
diff
changeset

140 
val [results] = Conjunction.elim_precise [length props] (finish res) 
c3f209752749
prove: proper assumption context, more tactic arguments;
wenzelm
parents:
20228
diff
changeset

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

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

148 
> map Drule.zero_var_indexes 
17980  149 
end; 
150 

151 

18119  152 
(* prove *) 
17980  153 

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

156 
fun prove_global thy xs asms prop tac = 

21516  157 
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

158 

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

159 

17980  160 

21687  161 
(** goal structure **) 
162 

163 
(* nested goals *) 

18207  164 

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

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

19423  168 
else Seq.single (foldr1 Conjunction.mk_conjunction (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 

19423  173 
else st > Drule.rotate_prems (i  1) > Conjunction.uncurry n > Drule.rotate_prems (1  i)) 
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 

183 
val conj_tac = SUBGOAL (fn (goal, i) => 

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

185 
else no_tac); 

186 

187 
val conjunction_tac = TRY o REPEAT_ALL_NEW conj_tac; 

188 

189 
val precise_conjunction_tac = 

190 
let 

191 
fun tac 0 i = eq_assume_tac i 

192 
 tac 1 i = SUBGOAL (K all_tac) i 

193 
 tac n i = conj_tac i THEN TRY (fn st => tac (n  1) (i + 1) st); 

194 
in TRY oo tac end; 

195 

196 
fun CONJUNCTS tac = 

197 
SELECT_GOAL (conjunction_tac 1 

198 
THEN tac 

199 
THEN PRIMITIVE (Conjunction.uncurry ~1)); 

200 

201 
fun PRECISE_CONJUNCTS n tac = 

202 
SELECT_GOAL (precise_conjunction_tac n 1 

203 
THEN tac 

204 
THEN PRIMITIVE (Conjunction.uncurry ~1)); 

205 

206 

207 
(* rewriting *) 

208 

209 
(*Rewrite subgoal i only. SELECT_GOAL avoids inefficiencies in goals_conv.*) 

210 
fun asm_rewrite_goal_tac mode prover_tac ss = 

211 
SELECT_GOAL 

212 
(PRIMITIVE (MetaSimplifier.rewrite_goal_rule mode (SINGLE o prover_tac) ss 1)); 

213 

214 
fun rewrite_goal_tac rews = 

215 
let val ss = MetaSimplifier.empty_ss addsimps rews in 

216 
fn i => fn st => asm_rewrite_goal_tac (true, false, false) (K no_tac) 

217 
(MetaSimplifier.theory_context (Thm.theory_of_thm st) ss) i st 

218 
end; 

219 

220 

221 
(* hhf normal form *) 

222 

223 
val norm_hhf_tac = 

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

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

226 
if Drule.is_norm_hhf t then all_tac 

227 
else rewrite_goal_tac [Drule.norm_hhf_eq] i); 

228 

229 
fun compose_hhf tha i thb = 

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

231 

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

233 

234 
fun comp_hhf tha thb = 

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

236 
([th], _) => th 

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

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

239 

23237  240 

241 
(* nonatomic goal assumptions *) 

242 

243 
fun assume_rule_tac ctxt = norm_hhf_tac THEN' CSUBGOAL (fn (goal, i) => 

244 
let 

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

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

247 
val Rs = filter_out (Logic.is_atomic o Thm.term_of) (Drule.strip_imp_prems goal''); 

248 
val tacs = Rs > map (fn R => 

249 
Tactic.etac (MetaSimplifier.norm_hhf (Thm.trivial R)) THEN_ALL_NEW assume_tac); 

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

251 

18207  252 
end; 
253 

17980  254 
structure BasicGoal: BASIC_GOAL = Goal; 
255 
open BasicGoal; 