author  wenzelm 
Thu, 26 Jan 2012 15:28:17 +0100  
changeset 46265  b6ab3cdea163 
parent 42666  fee67c099d03 
permissions  rwrr 
29755  1 
theory Proof 
2 
imports Base 

3 
begin 

18537  4 

20451  5 
chapter {* Structured proofs *} 
18537  6 

20474  7 
section {* Variables \label{sec:variables} *} 
20026  8 

20470  9 
text {* 
10 
Any variable that is not explicitly bound by @{text "\<lambda>"}abstraction 

11 
is considered as ``free''. Logically, free variables act like 

20474  12 
outermost universal quantification at the sequent level: @{text 
20470  13 
"A\<^isub>1(x), \<dots>, A\<^isub>n(x) \<turnstile> B(x)"} means that the result 
14 
holds \emph{for all} values of @{text "x"}. Free variables for 

15 
terms (not types) can be fully internalized into the logic: @{text 

20474  16 
"\<turnstile> B(x)"} and @{text "\<turnstile> \<And>x. B(x)"} are interchangeable, provided 
17 
that @{text "x"} does not occur elsewhere in the context. 

18 
Inspecting @{text "\<turnstile> \<And>x. B(x)"} more closely, we see that inside the 

20470  19 
quantifier, @{text "x"} is essentially ``arbitrary, but fixed'', 
20 
while from outside it appears as a placeholder for instantiation 

20474  21 
(thanks to @{text "\<And>"} elimination). 
20470  22 

20474  23 
The Pure logic represents the idea of variables being either inside 
24 
or outside the current scope by providing separate syntactic 

20470  25 
categories for \emph{fixed variables} (e.g.\ @{text "x"}) vs.\ 
26 
\emph{schematic variables} (e.g.\ @{text "?x"}). Incidently, a 

20474  27 
universal result @{text "\<turnstile> \<And>x. B(x)"} has the HHF normal form @{text 
34930  28 
"\<turnstile> B(?x)"}, which represents its generality without requiring an 
29 
explicit quantifier. The same principle works for type variables: 

30 
@{text "\<turnstile> B(?\<alpha>)"} represents the idea of ``@{text "\<turnstile> \<forall>\<alpha>. B(\<alpha>)"}'' 

31 
without demanding a truly polymorphic framework. 

20470  32 

33 
\medskip Additional care is required to treat type variables in a 

34 
way that facilitates typeinference. In principle, term variables 

35 
depend on type variables, which means that type variables would have 

36 
to be declared first. For example, a raw typetheoretic framework 

37 
would demand the context to be constructed in stages as follows: 

38 
@{text "\<Gamma> = \<alpha>: type, x: \<alpha>, a: A(x\<^isub>\<alpha>)"}. 

39 

40 
We allow a slightly less formalistic mode of operation: term 

41 
variables @{text "x"} are fixed without specifying a type yet 

42 
(essentially \emph{all} potential occurrences of some instance 

20474  43 
@{text "x\<^isub>\<tau>"} are fixed); the first occurrence of @{text "x"} 
44 
within a specific term assigns its most general type, which is then 

45 
maintained consistently in the context. The above example becomes 

46 
@{text "\<Gamma> = x: term, \<alpha>: type, A(x\<^isub>\<alpha>)"}, where type @{text 

47 
"\<alpha>"} is fixed \emph{after} term @{text "x"}, and the constraint 

48 
@{text "x :: \<alpha>"} is an implicit consequence of the occurrence of 

49 
@{text "x\<^isub>\<alpha>"} in the subsequent proposition. 

20470  50 

51 
This twist of dependencies is also accommodated by the reverse 

52 
operation of exporting results from a context: a type variable 

53 
@{text "\<alpha>"} is considered fixed as long as it occurs in some fixed 

54 
term variable of the context. For example, exporting @{text "x: 

39841  55 
term, \<alpha>: type \<turnstile> x\<^isub>\<alpha> \<equiv> x\<^isub>\<alpha>"} produces in the first step @{text "x: term 
56 
\<turnstile> x\<^isub>\<alpha> \<equiv> x\<^isub>\<alpha>"} for fixed @{text "\<alpha>"}, and only in the second step 

57 
@{text "\<turnstile> ?x\<^isub>?\<^isub>\<alpha> \<equiv> ?x\<^isub>?\<^isub>\<alpha>"} for schematic @{text "?x"} and @{text "?\<alpha>"}. 

58 
The following Isar source text illustrates this scenario. 

59 
*} 

20470  60 

40964  61 
notepad 
62 
begin 

39841  63 
{ 
64 
fix x  {* all potential occurrences of some @{text "x::\<tau>"} are fixed *} 

65 
{ 

66 
have "x::'a \<equiv> x"  {* implicit type assigment by concrete occurrence *} 

67 
by (rule reflexive) 

68 
} 

69 
thm this  {* result still with fixed type @{text "'a"} *} 

70 
} 

71 
thm this  {* fully general result for arbitrary @{text "?x::?'a"} *} 

40964  72 
end 
39841  73 

39861
b8d89db3e238
use continental paragraph style, which works better with mixture of (in)formal text;
wenzelm
parents:
39853
diff
changeset

74 
text {* The Isabelle/Isar proof context manages the details of term 
b8d89db3e238
use continental paragraph style, which works better with mixture of (in)formal text;
wenzelm
parents:
39853
diff
changeset

75 
vs.\ type variables, with highlevel principles for moving the 
20474  76 
frontier between fixed and schematic variables. 
77 

78 
The @{text "add_fixes"} operation explictly declares fixed 

79 
variables; the @{text "declare_term"} operation absorbs a term into 

80 
a context by fixing new type variables and adding syntactic 

81 
constraints. 

20470  82 

20474  83 
The @{text "export"} operation is able to perform the main work of 
84 
generalizing term and type variables as sketched above, assuming 

85 
that fixing variables and terms have been declared properly. 

86 

87 
There @{text "import"} operation makes a generalized fact a genuine 

88 
part of the context, by inventing fixed variables for the schematic 

89 
ones. The effect can be reversed by using @{text "export"} later, 

90 
potentially with an extended context; the result is equivalent to 

91 
the original modulo renaming of schematic variables. 

20470  92 

93 
The @{text "focus"} operation provides a variant of @{text "import"} 

94 
for nested propositions (with explicit quantification): @{text 

20474  95 
"\<And>x\<^isub>1 \<dots> x\<^isub>n. B(x\<^isub>1, \<dots>, x\<^isub>n)"} is 
96 
decomposed by inventing fixed variables @{text "x\<^isub>1, \<dots>, 

97 
x\<^isub>n"} for the body. 

20470  98 
*} 
20064  99 

20026  100 
text %mlref {* 
101 
\begin{mldecls} 

20474  102 
@{index_ML Variable.add_fixes: " 
103 
string list > Proof.context > string list * Proof.context"} \\ 

20797
c1f0bc7e7d80
renamed Variable.invent_fixes to Variable.variant_fixes;
wenzelm
parents:
20547
diff
changeset

104 
@{index_ML Variable.variant_fixes: " 
20474  105 
string list > Proof.context > string list * Proof.context"} \\ 
20026  106 
@{index_ML Variable.declare_term: "term > Proof.context > Proof.context"} \\ 
20470  107 
@{index_ML Variable.declare_constraints: "term > Proof.context > Proof.context"} \\ 
108 
@{index_ML Variable.export: "Proof.context > Proof.context > thm list > thm list"} \\ 

109 
@{index_ML Variable.polymorphic: "Proof.context > term list > term list"} \\ 

31794
71af1fd6a5e4
renamed Variable.import_thms to Variable.import (back again cf. ed7aa5a350ef  Alice is no longer supported);
wenzelm
parents:
30272
diff
changeset

110 
@{index_ML Variable.import: "bool > thm list > Proof.context > 
32302  111 
(((ctyp * ctyp) list * (cterm * cterm) list) * thm list) * Proof.context"} \\ 
42509  112 
@{index_ML Variable.focus: "term > Proof.context > 
113 
((string * (string * typ)) list * term) * Proof.context"} \\ 

20026  114 
\end{mldecls} 
115 

116 
\begin{description} 

117 

20064  118 
\item @{ML Variable.add_fixes}~@{text "xs ctxt"} fixes term 
20470  119 
variables @{text "xs"}, returning the resulting internal names. By 
120 
default, the internal representation coincides with the external 

20474  121 
one, which also means that the given variables must not be fixed 
122 
already. There is a different policy within a local proof body: the 

123 
given names are just hints for newly invented Skolem variables. 

20064  124 

20797
c1f0bc7e7d80
renamed Variable.invent_fixes to Variable.variant_fixes;
wenzelm
parents:
20547
diff
changeset

125 
\item @{ML Variable.variant_fixes} is similar to @{ML 
20470  126 
Variable.add_fixes}, but always produces fresh variants of the given 
20474  127 
names. 
20470  128 

129 
\item @{ML Variable.declare_term}~@{text "t ctxt"} declares term 

130 
@{text "t"} to belong to the context. This automatically fixes new 

131 
type variables, but not term variables. Syntactic constraints for 

20474  132 
type and term variables are declared uniformly, though. 
20470  133 

20474  134 
\item @{ML Variable.declare_constraints}~@{text "t ctxt"} declares 
135 
syntactic constraints from term @{text "t"}, without making it part 

136 
of the context yet. 

20026  137 

20470  138 
\item @{ML Variable.export}~@{text "inner outer thms"} generalizes 
139 
fixed type and term variables in @{text "thms"} according to the 

140 
difference of the @{text "inner"} and @{text "outer"} context, 

141 
following the principles sketched above. 

142 

143 
\item @{ML Variable.polymorphic}~@{text "ctxt ts"} generalizes type 

144 
variables in @{text "ts"} as far as possible, even those occurring 

145 
in fixed term variables. The default policy of typeinference is to 

20474  146 
fix newly introduced type variables, which is essentially reversed 
147 
with @{ML Variable.polymorphic}: here the given terms are detached 

148 
from the context as far as possible. 

20470  149 

31794
71af1fd6a5e4
renamed Variable.import_thms to Variable.import (back again cf. ed7aa5a350ef  Alice is no longer supported);
wenzelm
parents:
30272
diff
changeset

150 
\item @{ML Variable.import}~@{text "open thms ctxt"} invents fixed 
20474  151 
type and term variables for the schematic ones occurring in @{text 
152 
"thms"}. The @{text "open"} flag indicates whether the fixed names 

153 
should be accessible to the user, otherwise newly introduced names 

154 
are marked as ``internal'' (\secref{sec:names}). 

20026  155 

20474  156 
\item @{ML Variable.focus}~@{text B} decomposes the outermost @{text 
157 
"\<And>"} prefix of proposition @{text "B"}. 

20026  158 

159 
\end{description} 

160 
*} 

161 

39846  162 
text %mlex {* The following example shows how to work with fixed term 
163 
and type parameters and with typeinference. *} 

34932  164 

165 
ML {* 

166 
(*static compiletime context  for testing only*) 

167 
val ctxt0 = @{context}; 

168 

169 
(*locally fixed parameters  no type assignment yet*) 

170 
val ([x, y], ctxt1) = ctxt0 > Variable.add_fixes ["x", "y"]; 

171 

172 
(*t1: most general fixed type; t1': most general arbitrary type*) 

173 
val t1 = Syntax.read_term ctxt1 "x"; 

174 
val t1' = singleton (Variable.polymorphic ctxt1) t1; 

175 

176 
(*term u enforces specific type assignment*) 

39846  177 
val u = Syntax.read_term ctxt1 "(x::nat) \<equiv> y"; 
34932  178 

179 
(*official declaration of u  propagates constraints etc.*) 

180 
val ctxt2 = ctxt1 > Variable.declare_term u; 

39846  181 
val t2 = Syntax.read_term ctxt2 "x"; (*x::nat is enforced*) 
34932  182 
*} 
183 

40126  184 
text {* In the above example, the starting context is derived from the 
185 
toplevel theory, which means that fixed variables are internalized 

40153  186 
literally: @{text "x"} is mapped again to @{text "x"}, and 
40126  187 
attempting to fix it again in the subsequent context is an error. 
188 
Alternatively, fixed parameters can be renamed explicitly as 

189 
follows: *} 

34932  190 

191 
ML {* 

192 
val ctxt0 = @{context}; 

193 
val ([x1, x2, x3], ctxt1) = 

194 
ctxt0 > Variable.variant_fixes ["x", "x", "x"]; 

195 
*} 

196 

39861
b8d89db3e238
use continental paragraph style, which works better with mixture of (in)formal text;
wenzelm
parents:
39853
diff
changeset

197 
text {* The following ML code can now work with the invented names of 
40153  198 
@{text x1}, @{text x2}, @{text x3}, without depending on 
39861
b8d89db3e238
use continental paragraph style, which works better with mixture of (in)formal text;
wenzelm
parents:
39853
diff
changeset

199 
the details on the system policy for introducing these variants. 
b8d89db3e238
use continental paragraph style, which works better with mixture of (in)formal text;
wenzelm
parents:
39853
diff
changeset

200 
Recall that within a proof body the system always invents fresh 
b8d89db3e238
use continental paragraph style, which works better with mixture of (in)formal text;
wenzelm
parents:
39853
diff
changeset

201 
``skolem constants'', e.g.\ as follows: *} 
34932  202 

40964  203 
notepad 
204 
begin 

34932  205 
ML_prf %"ML" {* 
206 
val ctxt0 = @{context}; 

207 

208 
val ([x1], ctxt1) = ctxt0 > Variable.add_fixes ["x"]; 

209 
val ([x2], ctxt2) = ctxt1 > Variable.add_fixes ["x"]; 

210 
val ([x3], ctxt3) = ctxt2 > Variable.add_fixes ["x"]; 

211 

212 
val ([y1, y2], ctxt4) = 

213 
ctxt3 > Variable.variant_fixes ["y", "y"]; 

214 
*} 

40964  215 
end 
34932  216 

39861
b8d89db3e238
use continental paragraph style, which works better with mixture of (in)formal text;
wenzelm
parents:
39853
diff
changeset

217 
text {* In this situation @{ML Variable.add_fixes} and @{ML 
34932  218 
Variable.variant_fixes} are very similar, but identical name 
219 
proposals given in a row are only accepted by the second version. 

39861
b8d89db3e238
use continental paragraph style, which works better with mixture of (in)formal text;
wenzelm
parents:
39853
diff
changeset

220 
*} 
34932  221 

18537  222 

20474  223 
section {* Assumptions \label{sec:assumptions} *} 
20451  224 

20458  225 
text {* 
226 
An \emph{assumption} is a proposition that it is postulated in the 

227 
current context. Local conclusions may use assumptions as 

228 
additional facts, but this imposes implicit hypotheses that weaken 

229 
the overall statement. 

230 

20474  231 
Assumptions are restricted to fixed nonschematic statements, i.e.\ 
232 
all generality needs to be expressed by explicit quantifiers. 

20458  233 
Nevertheless, the result will be in HHF normal form with outermost 
234 
quantifiers stripped. For example, by assuming @{text "\<And>x :: \<alpha>. P 

20474  235 
x"} we get @{text "\<And>x :: \<alpha>. P x \<turnstile> P ?x"} for schematic @{text "?x"} 
236 
of fixed type @{text "\<alpha>"}. Local derivations accumulate more and 

237 
more explicit references to hypotheses: @{text "A\<^isub>1, \<dots>, 

20458  238 
A\<^isub>n \<turnstile> B"} where @{text "A\<^isub>1, \<dots>, A\<^isub>n"} needs to 
239 
be covered by the assumptions of the current context. 

240 

20459  241 
\medskip The @{text "add_assms"} operation augments the context by 
242 
local assumptions, which are parameterized by an arbitrary @{text 

243 
"export"} rule (see below). 

20458  244 

245 
The @{text "export"} operation moves facts from a (larger) inner 

246 
context into a (smaller) outer context, by discharging the 

247 
difference of the assumptions as specified by the associated export 

248 
rules. Note that the discharged portion is determined by the 

34930  249 
difference of contexts, not the facts being exported! There is a 
20459  250 
separate flag to indicate a goal context, where the result is meant 
29760  251 
to refine an enclosing subgoal of a structured proof state. 
20458  252 

253 
\medskip The most basic export rule discharges assumptions directly 

254 
by means of the @{text "\<Longrightarrow>"} introduction rule: 

255 
\[ 

42666  256 
\infer[(@{text "\<Longrightarrow>\<hyphen>intro"})]{@{text "\<Gamma>  A \<turnstile> A \<Longrightarrow> B"}}{@{text "\<Gamma> \<turnstile> B"}} 
20458  257 
\] 
258 

259 
The variant for goal refinements marks the newly introduced 

20474  260 
premises, which causes the canonical Isar goal refinement scheme to 
20458  261 
enforce unification with local premises within the goal: 
262 
\[ 

42666  263 
\infer[(@{text "#\<Longrightarrow>\<hyphen>intro"})]{@{text "\<Gamma>  A \<turnstile> #A \<Longrightarrow> B"}}{@{text "\<Gamma> \<turnstile> B"}} 
20458  264 
\] 
265 

20474  266 
\medskip Alternative versions of assumptions may perform arbitrary 
267 
transformations on export, as long as the corresponding portion of 

20459  268 
hypotheses is removed from the given facts. For example, a local 
269 
definition works by fixing @{text "x"} and assuming @{text "x \<equiv> t"}, 

270 
with the following export rule to reverse the effect: 

20458  271 
\[ 
42666  272 
\infer[(@{text "\<equiv>\<hyphen>expand"})]{@{text "\<Gamma>  (x \<equiv> t) \<turnstile> B t"}}{@{text "\<Gamma> \<turnstile> B x"}} 
20458  273 
\] 
20474  274 
This works, because the assumption @{text "x \<equiv> t"} was introduced in 
275 
a context with @{text "x"} being fresh, so @{text "x"} does not 

276 
occur in @{text "\<Gamma>"} here. 

20458  277 
*} 
278 

279 
text %mlref {* 

280 
\begin{mldecls} 

281 
@{index_ML_type Assumption.export} \\ 

282 
@{index_ML Assumption.assume: "cterm > thm"} \\ 

283 
@{index_ML Assumption.add_assms: 

20459  284 
"Assumption.export > 
285 
cterm list > Proof.context > thm list * Proof.context"} \\ 

286 
@{index_ML Assumption.add_assumes: " 

287 
cterm list > Proof.context > thm list * Proof.context"} \\ 

20458  288 
@{index_ML Assumption.export: "bool > Proof.context > Proof.context > thm > thm"} \\ 
289 
\end{mldecls} 

290 

291 
\begin{description} 

292 

39864  293 
\item Type @{ML_type Assumption.export} represents arbitrary export 
294 
rules, which is any function of type @{ML_type "bool > cterm list 

295 
> thm > thm"}, where the @{ML_type "bool"} indicates goal mode, 

296 
and the @{ML_type "cterm list"} the collection of assumptions to be 

297 
discharged simultaneously. 

20458  298 

20459  299 
\item @{ML Assumption.assume}~@{text "A"} turns proposition @{text 
34930  300 
"A"} into a primitive assumption @{text "A \<turnstile> A'"}, where the 
301 
conclusion @{text "A'"} is in HHF normal form. 

20458  302 

20474  303 
\item @{ML Assumption.add_assms}~@{text "r As"} augments the context 
304 
by assumptions @{text "As"} with export rule @{text "r"}. The 

305 
resulting facts are hypothetical theorems as produced by the raw 

306 
@{ML Assumption.assume}. 

20459  307 

308 
\item @{ML Assumption.add_assumes}~@{text "As"} is a special case of 

309 
@{ML Assumption.add_assms} where the export rule performs @{text 

42666  310 
"\<Longrightarrow>\<hyphen>intro"} or @{text "#\<Longrightarrow>\<hyphen>intro"}, depending on goal 
34930  311 
mode. 
20458  312 

20474  313 
\item @{ML Assumption.export}~@{text "is_goal inner outer thm"} 
314 
exports result @{text "thm"} from the the @{text "inner"} context 

20459  315 
back into the @{text "outer"} one; @{text "is_goal = true"} means 
316 
this is a goal context. The result is in HHF normal form. Note 

42361  317 
that @{ML "Proof_Context.export"} combines @{ML "Variable.export"} 
20459  318 
and @{ML "Assumption.export"} in the canonical way. 
20458  319 

320 
\end{description} 

321 
*} 

20451  322 

34932  323 
text %mlex {* The following example demonstrates how rules can be 
324 
derived by building up a context of assumptions first, and exporting 

325 
some local fact afterwards. We refer to @{theory Pure} equality 

326 
here for testing purposes. 

327 
*} 

328 

329 
ML {* 

330 
(*static compiletime context  for testing only*) 

331 
val ctxt0 = @{context}; 

332 

333 
val ([eq], ctxt1) = 

334 
ctxt0 > Assumption.add_assumes [@{cprop "x \<equiv> y"}]; 

335 
val eq' = Thm.symmetric eq; 

336 

337 
(*back to original context  discharges assumption*) 

338 
val r = Assumption.export false ctxt1 ctxt0 eq'; 

339 
*} 

340 

39861
b8d89db3e238
use continental paragraph style, which works better with mixture of (in)formal text;
wenzelm
parents:
39853
diff
changeset

341 
text {* Note that the variables of the resulting rule are not 
b8d89db3e238
use continental paragraph style, which works better with mixture of (in)formal text;
wenzelm
parents:
39853
diff
changeset

342 
generalized. This would have required to fix them properly in the 
b8d89db3e238
use continental paragraph style, which works better with mixture of (in)formal text;
wenzelm
parents:
39853
diff
changeset

343 
context beforehand, and export wrt.\ variables afterwards (cf.\ @{ML 
42361  344 
Variable.export} or the combined @{ML "Proof_Context.export"}). *} 
34932  345 

20451  346 

34930  347 
section {* Structured goals and results \label{sec:structgoals} *} 
20451  348 

18537  349 
text {* 
20472  350 
Local results are established by monotonic reasoning from facts 
20474  351 
within a context. This allows common combinations of theorems, 
352 
e.g.\ via @{text "\<And>/\<Longrightarrow>"} elimination, resolution rules, or equational 

353 
reasoning, see \secref{sec:thms}. Unaccounted context manipulations 

354 
should be avoided, notably raw @{text "\<And>/\<Longrightarrow>"} introduction or adhoc 

20472  355 
references to free variables or assumptions not present in the proof 
356 
context. 

18537  357 

20491  358 
\medskip The @{text "SUBPROOF"} combinator allows to structure a 
359 
tactical proof recursively by decomposing a selected subgoal: 

360 
@{text "(\<And>x. A(x) \<Longrightarrow> B(x)) \<Longrightarrow> \<dots>"} is turned into @{text "B(x) \<Longrightarrow> \<dots>"} 

361 
after fixing @{text "x"} and assuming @{text "A(x)"}. This means 

362 
the tactic needs to solve the conclusion, but may use the premise as 

363 
a local fact, for locally fixed variables. 

18537  364 

34930  365 
The family of @{text "FOCUS"} combinators is similar to @{text 
366 
"SUBPROOF"}, but allows to retain schematic variables and pending 

367 
subgoals in the resulting goal state. 

368 

20491  369 
The @{text "prove"} operation provides an interface for structured 
370 
backwards reasoning under program control, with some explicit sanity 

371 
checks of the result. The goal context can be augmented by 

372 
additional fixed variables (cf.\ \secref{sec:variables}) and 

373 
assumptions (cf.\ \secref{sec:assumptions}), which will be available 

374 
as local facts during the proof and discharged into implications in 

375 
the result. Type and term variables are generalized as usual, 

376 
according to the context. 

18537  377 

20491  378 
The @{text "obtain"} operation produces results by eliminating 
379 
existing facts by means of a given tactic. This acts like a dual 

380 
conclusion: the proof demonstrates that the context may be augmented 

34930  381 
by parameters and assumptions, without affecting any conclusions 
382 
that do not mention these parameters. See also 

39851  383 
\cite{isabelleisarref} for the userlevel @{command obtain} and 
384 
@{command guess} elements. Final results, which may not refer to 

20491  385 
the parameters in the conclusion, need to exported explicitly into 
39851  386 
the original context. *} 
18537  387 

20472  388 
text %mlref {* 
389 
\begin{mldecls} 

46265  390 
@{index_ML SELECT_GOAL: "tactic > int > tactic"} \\ 
39821  391 
@{index_ML SUBPROOF: "(Subgoal.focus > tactic) > 
392 
Proof.context > int > tactic"} \\ 

393 
@{index_ML Subgoal.FOCUS: "(Subgoal.focus > tactic) > 

394 
Proof.context > int > tactic"} \\ 

395 
@{index_ML Subgoal.FOCUS_PREMS: "(Subgoal.focus > tactic) > 

396 
Proof.context > int > tactic"} \\ 

397 
@{index_ML Subgoal.FOCUS_PARAMS: "(Subgoal.focus > tactic) > 

398 
Proof.context > int > tactic"} \\ 

39853  399 
@{index_ML Subgoal.focus: "Proof.context > int > thm > Subgoal.focus * thm"} \\ 
400 
@{index_ML Subgoal.focus_prems: "Proof.context > int > thm > Subgoal.focus * thm"} \\ 

401 
@{index_ML Subgoal.focus_params: "Proof.context > int > thm > Subgoal.focus * thm"} \\ 

20547  402 
\end{mldecls} 
34930  403 

20547  404 
\begin{mldecls} 
20472  405 
@{index_ML Goal.prove: "Proof.context > string list > term list > term > 
406 
({prems: thm list, context: Proof.context} > tactic) > thm"} \\ 

407 
@{index_ML Goal.prove_multi: "Proof.context > string list > term list > term list > 

408 
({prems: thm list, context: Proof.context} > tactic) > thm list"} \\ 

20547  409 
\end{mldecls} 
410 
\begin{mldecls} 

39821  411 
@{index_ML Obtain.result: "(Proof.context > tactic) > thm list > 
412 
Proof.context > ((string * cterm) list * thm list) * Proof.context"} \\ 

20472  413 
\end{mldecls} 
18537  414 

20472  415 
\begin{description} 
18537  416 

46265  417 
\item @{ML SELECT_GOAL}~@{text "tac i"} confines a tactic to the 
418 
specified subgoal @{text "i"}. This introduces a nested goal state, 

419 
without decomposing the internal structure of the subgoal yet. 

420 

29761  421 
\item @{ML SUBPROOF}~@{text "tac ctxt i"} decomposes the structure 
422 
of the specified subgoal, producing an extended context and a 

423 
reduced goal, which needs to be solved by the given tactic. All 

424 
schematic parameters of the goal are imported into the context as 

425 
fixed ones, which may not be instantiated in the subproof. 

20491  426 

34930  427 
\item @{ML Subgoal.FOCUS}, @{ML Subgoal.FOCUS_PREMS}, and @{ML 
428 
Subgoal.FOCUS_PARAMS} are similar to @{ML SUBPROOF}, but are 

429 
slightly more flexible: only the specified parts of the subgoal are 

430 
imported into the context, and the body tactic may introduce new 

431 
subgoals and schematic variables. 

432 

39853  433 
\item @{ML Subgoal.focus}, @{ML Subgoal.focus_prems}, @{ML 
434 
Subgoal.focus_params} extract the focus information from a goal 

435 
state in the same way as the corresponding tacticals above. This is 

436 
occasionally useful to experiment without writing actual tactics 

437 
yet. 

438 

20472  439 
\item @{ML Goal.prove}~@{text "ctxt xs As C tac"} states goal @{text 
20474  440 
"C"} in the context augmented by fixed variables @{text "xs"} and 
441 
assumptions @{text "As"}, and applies tactic @{text "tac"} to solve 

442 
it. The latter may depend on the local assumptions being presented 

443 
as facts. The result is in HHF normal form. 

18537  444 

20472  445 
\item @{ML Goal.prove_multi} is simular to @{ML Goal.prove}, but 
20491  446 
states several conclusions simultaneously. The goal is encoded by 
21827  447 
means of Pure conjunction; @{ML Goal.conjunction_tac} will turn this 
448 
into a collection of individual subgoals. 

20472  449 

20491  450 
\item @{ML Obtain.result}~@{text "tac thms ctxt"} eliminates the 
451 
given facts using a tactic, which results in additional fixed 

452 
variables and assumptions in the context. Final results need to be 

453 
exported explicitly. 

20472  454 

455 
\end{description} 

456 
*} 

30272  457 

39853  458 
text %mlex {* The following minimal example illustrates how to access 
459 
the focus information of a structured goal state. *} 

460 

40964  461 
notepad 
462 
begin 

39853  463 
fix A B C :: "'a \<Rightarrow> bool" 
464 

465 
have "\<And>x. A x \<Longrightarrow> B x \<Longrightarrow> C x" 

466 
ML_val 

467 
{* 

468 
val {goal, context = goal_ctxt, ...} = @{Isar.goal}; 

469 
val (focus as {params, asms, concl, ...}, goal') = 

470 
Subgoal.focus goal_ctxt 1 goal; 

471 
val [A, B] = #prems focus; 

472 
val [(_, x)] = #params focus; 

473 
*} 

474 
oops 

475 

476 
text {* \medskip The next example demonstrates forwardelimination in 

477 
a local context, using @{ML Obtain.result}. *} 

39851  478 

40964  479 
notepad 
480 
begin 

39851  481 
assume ex: "\<exists>x. B x" 
482 

483 
ML_prf %"ML" {* 

484 
val ctxt0 = @{context}; 

485 
val (([(_, x)], [B]), ctxt1) = ctxt0 

486 
> Obtain.result (fn _ => etac @{thm exE} 1) [@{thm ex}]; 

487 
*} 

488 
ML_prf %"ML" {* 

42361  489 
singleton (Proof_Context.export ctxt1 ctxt0) @{thm refl}; 
39851  490 
*} 
491 
ML_prf %"ML" {* 

42361  492 
Proof_Context.export ctxt1 ctxt0 [Thm.reflexive x] 
39851  493 
handle ERROR msg => (warning msg; []); 
494 
*} 

40964  495 
end 
39851  496 

18537  497 
end 