author  wenzelm 
Wed, 13 Dec 2006 16:26:45 +0100  
changeset 21827  0b1d07f79c1e 
parent 20797  c1f0bc7e7d80 
child 22568  ed7aa5a350ef 
permissions  rwrr 
18537  1 
% 
2 
\begin{isabellebody}% 

3 
\def\isabellecontext{proof}% 

4 
% 

5 
\isadelimtheory 

6 
\isanewline 

7 
\isanewline 

8 
\isanewline 

9 
% 

10 
\endisadelimtheory 

11 
% 

12 
\isatagtheory 

13 
\isacommand{theory}\isamarkupfalse% 

14 
\ {\isachardoublequoteopen}proof{\isachardoublequoteclose}\ \isakeyword{imports}\ base\ \isakeyword{begin}% 

15 
\endisatagtheory 

16 
{\isafoldtheory}% 

17 
% 

18 
\isadelimtheory 

19 
% 

20 
\endisadelimtheory 

21 
% 

20451  22 
\isamarkupchapter{Structured proofs% 
18537  23 
} 
24 
\isamarkuptrue% 

25 
% 

20474  26 
\isamarkupsection{Variables \label{sec:variables}% 
20027  27 
} 
28 
\isamarkuptrue% 

29 
% 

20063  30 
\begin{isamarkuptext}% 
20471  31 
Any variable that is not explicitly bound by \isa{{\isasymlambda}}abstraction 
32 
is considered as ``free''. Logically, free variables act like 

20474  33 
outermost universal quantification at the sequent level: \isa{A\isactrlisub {\isadigit{1}}{\isacharparenleft}x{\isacharparenright}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ A\isactrlisub n{\isacharparenleft}x{\isacharparenright}\ {\isasymturnstile}\ B{\isacharparenleft}x{\isacharparenright}} means that the result 
20471  34 
holds \emph{for all} values of \isa{x}. Free variables for 
20474  35 
terms (not types) can be fully internalized into the logic: \isa{{\isasymturnstile}\ B{\isacharparenleft}x{\isacharparenright}} and \isa{{\isasymturnstile}\ {\isasymAnd}x{\isachardot}\ B{\isacharparenleft}x{\isacharparenright}} are interchangeable, provided 
36 
that \isa{x} does not occur elsewhere in the context. 

37 
Inspecting \isa{{\isasymturnstile}\ {\isasymAnd}x{\isachardot}\ B{\isacharparenleft}x{\isacharparenright}} more closely, we see that inside the 

20471  38 
quantifier, \isa{x} is essentially ``arbitrary, but fixed'', 
39 
while from outside it appears as a placeholder for instantiation 

20474  40 
(thanks to \isa{{\isasymAnd}} elimination). 
20471  41 

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

20471  44 
categories for \emph{fixed variables} (e.g.\ \isa{x}) vs.\ 
45 
\emph{schematic variables} (e.g.\ \isa{{\isacharquery}x}). Incidently, a 

20474  46 
universal result \isa{{\isasymturnstile}\ {\isasymAnd}x{\isachardot}\ B{\isacharparenleft}x{\isacharparenright}} has the HHF normal form \isa{{\isasymturnstile}\ B{\isacharparenleft}{\isacharquery}x{\isacharparenright}}, which represents its generality nicely without requiring 
47 
an explicit quantifier. The same principle works for type 

48 
variables: \isa{{\isasymturnstile}\ B{\isacharparenleft}{\isacharquery}{\isasymalpha}{\isacharparenright}} represents the idea of ``\isa{{\isasymturnstile}\ {\isasymforall}{\isasymalpha}{\isachardot}\ B{\isacharparenleft}{\isasymalpha}{\isacharparenright}}'' without demanding a truly polymorphic framework. 

20471  49 

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

51 
way that facilitates typeinference. In principle, term variables 

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

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

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

55 
\isa{{\isasymGamma}\ {\isacharequal}\ {\isasymalpha}{\isacharcolon}\ type{\isacharcomma}\ x{\isacharcolon}\ {\isasymalpha}{\isacharcomma}\ a{\isacharcolon}\ A{\isacharparenleft}x\isactrlisub {\isasymalpha}{\isacharparenright}}. 

56 

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

58 
variables \isa{x} are fixed without specifying a type yet 

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

20474  60 
\isa{x\isactrlisub {\isasymtau}} are fixed); the first occurrence of \isa{x} 
61 
within a specific term assigns its most general type, which is then 

62 
maintained consistently in the context. The above example becomes 

63 
\isa{{\isasymGamma}\ {\isacharequal}\ x{\isacharcolon}\ term{\isacharcomma}\ {\isasymalpha}{\isacharcolon}\ type{\isacharcomma}\ A{\isacharparenleft}x\isactrlisub {\isasymalpha}{\isacharparenright}}, where type \isa{{\isasymalpha}} is fixed \emph{after} term \isa{x}, and the constraint 

64 
\isa{x\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}} is an implicit consequence of the occurrence of 

65 
\isa{x\isactrlisub {\isasymalpha}} in the subsequent proposition. 

20471  66 

67 
This twist of dependencies is also accommodated by the reverse 

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

69 
\isa{{\isasymalpha}} is considered fixed as long as it occurs in some fixed 

20474  70 
term variable of the context. For example, exporting \isa{x{\isacharcolon}\ term{\isacharcomma}\ {\isasymalpha}{\isacharcolon}\ type\ {\isasymturnstile}\ x\isactrlisub {\isasymalpha}\ {\isacharequal}\ x\isactrlisub {\isasymalpha}} produces in the first step 
71 
\isa{x{\isacharcolon}\ term\ {\isasymturnstile}\ x\isactrlisub {\isasymalpha}\ {\isacharequal}\ x\isactrlisub {\isasymalpha}} for fixed \isa{{\isasymalpha}}, 

72 
and only in the second step \isa{{\isasymturnstile}\ {\isacharquery}x\isactrlisub {\isacharquery}\isactrlisub {\isasymalpha}\ {\isacharequal}\ {\isacharquery}x\isactrlisub {\isacharquery}\isactrlisub {\isasymalpha}} for schematic \isa{{\isacharquery}x} and \isa{{\isacharquery}{\isasymalpha}}. 

20471  73 

74 
\medskip The Isabelle/Isar proof context manages the gory details of 

75 
term vs.\ type variables, with highlevel principles for moving the 

20474  76 
frontier between fixed and schematic variables. 
77 

78 
The \isa{add{\isacharunderscore}fixes} operation explictly declares fixed 

79 
variables; the \isa{declare{\isacharunderscore}term} operation absorbs a term into 

80 
a context by fixing new type variables and adding syntactic 

81 
constraints. 

20471  82 

20474  83 
The \isa{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 \isa{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 \isa{export} later, 

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

91 
the original modulo renaming of schematic variables. 

20471  92 

93 
The \isa{focus} operation provides a variant of \isa{import} 

20474  94 
for nested propositions (with explicit quantification): \isa{{\isasymAnd}x\isactrlisub {\isadigit{1}}\ {\isasymdots}\ x\isactrlisub n{\isachardot}\ B{\isacharparenleft}x\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ x\isactrlisub n{\isacharparenright}} is 
95 
decomposed by inventing fixed variables \isa{x\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ x\isactrlisub n} for the body.% 

20063  96 
\end{isamarkuptext}% 
97 
\isamarkuptrue% 

98 
% 

20027  99 
\isadelimmlref 
100 
% 

101 
\endisadelimmlref 

102 
% 

103 
\isatagmlref 

104 
% 

105 
\begin{isamarkuptext}% 

106 
\begin{mldecls} 

20474  107 
\indexml{Variable.addfixes}\verbVariable.add_fixes: \isasep\isanewline% 
108 
\verb string list > Proof.context > string list * Proof.context \\ 

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

109 
\indexml{Variable.variantfixes}\verbVariable.variant_fixes: \isasep\isanewline% 
20474  110 
\verb string list > Proof.context > string list * Proof.context \\ 
20027  111 
\indexml{Variable.declareterm}\verbVariable.declare_term: term > Proof.context > Proof.context \\ 
20471  112 
\indexml{Variable.declareconstraints}\verbVariable.declare_constraints: term > Proof.context > Proof.context \\ 
113 
\indexml{Variable.export}\verbVariable.export: Proof.context > Proof.context > thm list > thm list \\ 

114 
\indexml{Variable.polymorphic}\verbVariable.polymorphic: Proof.context > term list > term list \\ 

20474  115 
\indexml{Variable.import}\verbVariable.import: bool > thm list > Proof.context >\isasep\isanewline% 
116 
\verb ((ctyp list * cterm list) * thm list) * Proof.context \\ 

20471  117 
\indexml{Variable.focus}\verbVariable.focus: cterm > Proof.context > (cterm list * cterm) * Proof.context \\ 
20027  118 
\end{mldecls} 
119 

120 
\begin{description} 

121 

20471  122 
\item \verbVariable.add_fixes~\isa{xs\ ctxt} fixes term 
123 
variables \isa{xs}, returning the resulting internal names. By 

124 
default, the internal representation coincides with the external 

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

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

20471  128 

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

129 
\item \verbVariable.variant_fixes is similar to \verbVariable.add_fixes, but always produces fresh variants of the given 
20474  130 
names. 
20471  131 

20063  132 
\item \verbVariable.declare_term~\isa{t\ ctxt} declares term 
20471  133 
\isa{t} to belong to the context. This automatically fixes new 
134 
type variables, but not term variables. Syntactic constraints for 

20474  135 
type and term variables are declared uniformly, though. 
20063  136 

20474  137 
\item \verbVariable.declare_constraints~\isa{t\ ctxt} declares 
138 
syntactic constraints from term \isa{t}, without making it part 

139 
of the context yet. 

20471  140 

141 
\item \verbVariable.export~\isa{inner\ outer\ thms} generalizes 

142 
fixed type and term variables in \isa{thms} according to the 

143 
difference of the \isa{inner} and \isa{outer} context, 

144 
following the principles sketched above. 

20063  145 

20471  146 
\item \verbVariable.polymorphic~\isa{ctxt\ ts} generalizes type 
147 
variables in \isa{ts} as far as possible, even those occurring 

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

20474  149 
fix newly introduced type variables, which is essentially reversed 
150 
with \verbVariable.polymorphic: here the given terms are detached 

151 
from the context as far as possible. 

20027  152 

20474  153 
\item \verbVariable.import~\isa{open\ thms\ ctxt} invents fixed 
154 
type and term variables for the schematic ones occurring in \isa{thms}. The \isa{open} flag indicates whether the fixed names 

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

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

20027  157 

20474  158 
\item \verbVariable.focus~\isa{B} decomposes the outermost \isa{{\isasymAnd}} prefix of proposition \isa{B}. 
20027  159 

160 
\end{description}% 

161 
\end{isamarkuptext}% 

162 
\isamarkuptrue% 

163 
% 

164 
\endisatagmlref 

165 
{\isafoldmlref}% 

166 
% 

167 
\isadelimmlref 

168 
% 

169 
\endisadelimmlref 

170 
% 

20474  171 
\isamarkupsection{Assumptions \label{sec:assumptions}% 
20451  172 
} 
173 
\isamarkuptrue% 

174 
% 

175 
\begin{isamarkuptext}% 

20458  176 
An \emph{assumption} is a proposition that it is postulated in the 
177 
current context. Local conclusions may use assumptions as 

178 
additional facts, but this imposes implicit hypotheses that weaken 

179 
the overall statement. 

180 

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

20458  183 
Nevertheless, the result will be in HHF normal form with outermost 
20474  184 
quantifiers stripped. For example, by assuming \isa{{\isasymAnd}x\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}{\isachardot}\ P\ x} we get \isa{{\isasymAnd}x\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}{\isachardot}\ P\ x\ {\isasymturnstile}\ P\ {\isacharquery}x} for schematic \isa{{\isacharquery}x} 
185 
of fixed type \isa{{\isasymalpha}}. Local derivations accumulate more and 

186 
more explicit references to hypotheses: \isa{A\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ A\isactrlisub n\ {\isasymturnstile}\ B} where \isa{A\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ A\isactrlisub n} needs to 

20458  187 
be covered by the assumptions of the current context. 
188 

20459  189 
\medskip The \isa{add{\isacharunderscore}assms} operation augments the context by 
190 
local assumptions, which are parameterized by an arbitrary \isa{export} rule (see below). 

20458  191 

192 
The \isa{export} operation moves facts from a (larger) inner 

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

194 
difference of the assumptions as specified by the associated export 

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

20459  196 
difference contexts, not the facts being exported! There is a 
197 
separate flag to indicate a goal context, where the result is meant 

198 
to refine an enclosing subgoal of a structured proof state (cf.\ 

199 
\secref{sec:isarproofstate}). 

20458  200 

201 
\medskip The most basic export rule discharges assumptions directly 

202 
by means of the \isa{{\isasymLongrightarrow}} introduction rule: 

203 
\[ 

204 
\infer[(\isa{{\isasymLongrightarrow}{\isacharunderscore}intro})]{\isa{{\isasymGamma}\ {\isacharbackslash}\ A\ {\isasymturnstile}\ A\ {\isasymLongrightarrow}\ B}}{\isa{{\isasymGamma}\ {\isasymturnstile}\ B}} 

205 
\] 

206 

207 
The variant for goal refinements marks the newly introduced 

20474  208 
premises, which causes the canonical Isar goal refinement scheme to 
20458  209 
enforce unification with local premises within the goal: 
210 
\[ 

211 
\infer[(\isa{{\isacharhash}{\isasymLongrightarrow}{\isacharunderscore}intro})]{\isa{{\isasymGamma}\ {\isacharbackslash}\ A\ {\isasymturnstile}\ {\isacharhash}A\ {\isasymLongrightarrow}\ B}}{\isa{{\isasymGamma}\ {\isasymturnstile}\ B}} 

212 
\] 

213 

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

20459  216 
hypotheses is removed from the given facts. For example, a local 
217 
definition works by fixing \isa{x} and assuming \isa{x\ {\isasymequiv}\ t}, 

218 
with the following export rule to reverse the effect: 

20458  219 
\[ 
20491  220 
\infer[(\isa{{\isasymequiv}{\isacharminus}expand})]{\isa{{\isasymGamma}\ {\isacharbackslash}\ x\ {\isasymequiv}\ t\ {\isasymturnstile}\ B\ t}}{\isa{{\isasymGamma}\ {\isasymturnstile}\ B\ x}} 
20458  221 
\] 
20474  222 
This works, because the assumption \isa{x\ {\isasymequiv}\ t} was introduced in 
223 
a context with \isa{x} being fresh, so \isa{x} does not 

224 
occur in \isa{{\isasymGamma}} here.% 

20451  225 
\end{isamarkuptext}% 
226 
\isamarkuptrue% 

227 
% 

20458  228 
\isadelimmlref 
229 
% 

230 
\endisadelimmlref 

231 
% 

232 
\isatagmlref 

233 
% 

234 
\begin{isamarkuptext}% 

235 
\begin{mldecls} 

236 
\indexmltype{Assumption.export}\verbtype Assumption.export \\ 

237 
\indexml{Assumption.assume}\verbAssumption.assume: cterm > thm \\ 

20459  238 
\indexml{Assumption.addassms}\verbAssumption.add_assms: Assumption.export >\isasep\isanewline% 
239 
\verb cterm list > Proof.context > thm list * Proof.context \\ 

240 
\indexml{Assumption.addassumes}\verbAssumption.add_assumes: \isasep\isanewline% 

241 
\verb cterm list > Proof.context > thm list * Proof.context \\ 

20458  242 
\indexml{Assumption.export}\verbAssumption.export: bool > Proof.context > Proof.context > thm > thm \\ 
243 
\end{mldecls} 

244 

245 
\begin{description} 

246 

20459  247 
\item \verbAssumption.export represents arbitrary export 
248 
rules, which is any function of type \verbbool > cterm list > thm > thm, 

249 
where the \verbbool indicates goal mode, and the \verbcterm list the collection of assumptions to be discharged 

250 
simultaneously. 

20458  251 

20459  252 
\item \verbAssumption.assume~\isa{A} turns proposition \isa{A} into a raw assumption \isa{A\ {\isasymturnstile}\ A{\isacharprime}}, where the conclusion 
253 
\isa{A{\isacharprime}} is in HHF normal form. 

20458  254 

20474  255 
\item \verbAssumption.add_assms~\isa{r\ As} augments the context 
256 
by assumptions \isa{As} with export rule \isa{r}. The 

257 
resulting facts are hypothetical theorems as produced by the raw 

258 
\verbAssumption.assume. 

20459  259 

260 
\item \verbAssumption.add_assumes~\isa{As} is a special case of 

261 
\verbAssumption.add_assms where the export rule performs \isa{{\isasymLongrightarrow}{\isacharunderscore}intro} or \isa{{\isacharhash}{\isasymLongrightarrow}{\isacharunderscore}intro}, depending on goal mode. 

20458  262 

20474  263 
\item \verbAssumption.export~\isa{is{\isacharunderscore}goal\ inner\ outer\ thm} 
264 
exports result \isa{thm} from the the \isa{inner} context 

20459  265 
back into the \isa{outer} one; \isa{is{\isacharunderscore}goal\ {\isacharequal}\ true} means 
266 
this is a goal context. The result is in HHF normal form. Note 

267 
that \verbProofContext.export combines \verbVariable.export 

268 
and \verbAssumption.export in the canonical way. 

20458  269 

270 
\end{description}% 

271 
\end{isamarkuptext}% 

272 
\isamarkuptrue% 

273 
% 

274 
\endisatagmlref 

275 
{\isafoldmlref}% 

276 
% 

277 
\isadelimmlref 

278 
% 

279 
\endisadelimmlref 

280 
% 

20520  281 
\isamarkupsection{Results% 
20451  282 
} 
283 
\isamarkuptrue% 

284 
% 

285 
\begin{isamarkuptext}% 

20472  286 
Local results are established by monotonic reasoning from facts 
20474  287 
within a context. This allows common combinations of theorems, 
288 
e.g.\ via \isa{{\isasymAnd}{\isacharslash}{\isasymLongrightarrow}} elimination, resolution rules, or equational 

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

290 
should be avoided, notably raw \isa{{\isasymAnd}{\isacharslash}{\isasymLongrightarrow}} introduction or adhoc 

20472  291 
references to free variables or assumptions not present in the proof 
292 
context. 

293 

20491  294 
\medskip The \isa{SUBPROOF} combinator allows to structure a 
295 
tactical proof recursively by decomposing a selected subgoal: 

296 
\isa{{\isacharparenleft}{\isasymAnd}x{\isachardot}\ A{\isacharparenleft}x{\isacharparenright}\ {\isasymLongrightarrow}\ B{\isacharparenleft}x{\isacharparenright}{\isacharparenright}\ {\isasymLongrightarrow}\ {\isasymdots}} is turned into \isa{B{\isacharparenleft}x{\isacharparenright}\ {\isasymLongrightarrow}\ {\isasymdots}} 

297 
after fixing \isa{x} and assuming \isa{A{\isacharparenleft}x{\isacharparenright}}. This means 

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

299 
a local fact, for locally fixed variables. 

20472  300 

20491  301 
The \isa{prove} operation provides an interface for structured 
302 
backwards reasoning under program control, with some explicit sanity 

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

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

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

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

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

308 
according to the context. 

20472  309 

20491  310 
The \isa{obtain} operation produces results by eliminating 
311 
existing facts by means of a given tactic. This acts like a dual 

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

313 
by certain fixed variables and assumptions. See also 

314 
\cite{isabelleisarref} for the userlevel \isa{{\isasymOBTAIN}} and 

315 
\isa{{\isasymGUESS}} elements. Final results, which may not refer to 

316 
the parameters in the conclusion, need to exported explicitly into 

317 
the original context.% 

20451  318 
\end{isamarkuptext}% 
319 
\isamarkuptrue% 

320 
% 

20472  321 
\isadelimmlref 
322 
% 

323 
\endisadelimmlref 

324 
% 

325 
\isatagmlref 

18537  326 
% 
327 
\begin{isamarkuptext}% 

20472  328 
\begin{mldecls} 
20491  329 
\indexml{SUBPROOF}\verbSUBPROOF: ({context: Proof.context, schematics: ctyp list * cterm list,\isasep\isanewline% 
330 
\verb params: cterm list, asms: cterm list, concl: cterm,\isasep\isanewline% 

331 
\verb prems: thm list} > tactic) > Proof.context > int > tactic \\ 

20547  332 
\end{mldecls} 
333 
\begin{mldecls} 

20472  334 
\indexml{Goal.prove}\verbGoal.prove: Proof.context > string list > term list > term >\isasep\isanewline% 
335 
\verb ({prems: thm list, context: Proof.context} > tactic) > thm \\ 

336 
\indexml{Goal.provemulti}\verbGoal.prove_multi: Proof.context > string list > term list > term list >\isasep\isanewline% 

337 
\verb ({prems: thm list, context: Proof.context} > tactic) > thm list \\ 

20547  338 
\end{mldecls} 
339 
\begin{mldecls} 

20491  340 
\indexml{Obtain.result}\verbObtain.result: (Proof.context > tactic) >\isasep\isanewline% 
20542  341 
\verb thm list > Proof.context > (cterm list * thm list) * Proof.context \\ 
20472  342 
\end{mldecls} 
343 

344 
\begin{description} 

18537  345 

20491  346 
\item \verbSUBPROOF~\isa{tac} decomposes the structure of a 
347 
particular subgoal, producing an extended context and a reduced 

348 
goal, which needs to be solved by the given tactic. All schematic 

349 
parameters of the goal are imported into the context as fixed ones, 

350 
which may not be instantiated in the subproof. 

351 

20474  352 
\item \verbGoal.prove~\isa{ctxt\ xs\ As\ C\ tac} states goal \isa{C} in the context augmented by fixed variables \isa{xs} and 
353 
assumptions \isa{As}, and applies tactic \isa{tac} to solve 

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

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

18537  356 

20472  357 
\item \verbGoal.prove_multi is simular to \verbGoal.prove, but 
20491  358 
states several conclusions simultaneously. The goal is encoded by 
21827  359 
means of Pure conjunction; \verbGoal.conjunction_tac will turn this 
360 
into a collection of individual subgoals. 

18537  361 

20491  362 
\item \verbObtain.result~\isa{tac\ thms\ ctxt} eliminates the 
363 
given facts using a tactic, which results in additional fixed 

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

365 
exported explicitly. 

20472  366 

367 
\end{description}% 

18537  368 
\end{isamarkuptext}% 
369 
\isamarkuptrue% 

370 
% 

20472  371 
\endisatagmlref 
372 
{\isafoldmlref}% 

18537  373 
% 
20472  374 
\isadelimmlref 
18537  375 
% 
20472  376 
\endisadelimmlref 
18537  377 
% 
378 
\isadelimtheory 

379 
% 

380 
\endisadelimtheory 

381 
% 

382 
\isatagtheory 

383 
\isacommand{end}\isamarkupfalse% 

384 
% 

385 
\endisatagtheory 

386 
{\isafoldtheory}% 

387 
% 

388 
\isadelimtheory 

389 
% 

390 
\endisadelimtheory 

391 
\isanewline 

392 
\end{isabellebody}% 

393 
%%% Local Variables: 

394 
%%% mode: latex 

395 
%%% TeXmaster: "root" 

396 
%%% End: 