215 transformations on export, as long as the corresponding portion of |
215 transformations on export, as long as the corresponding portion of |
216 hypotheses is removed from the given facts. For example, a local |
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}, |
217 definition works by fixing \isa{x} and assuming \isa{x\ {\isasymequiv}\ t}, |
218 with the following export rule to reverse the effect: |
218 with the following export rule to reverse the effect: |
219 \[ |
219 \[ |
220 \infer{\isa{{\isasymGamma}\ {\isacharbackslash}\ x\ {\isasymequiv}\ t\ {\isasymturnstile}\ B\ t}}{\isa{{\isasymGamma}\ {\isasymturnstile}\ B\ x}} |
220 \infer[(\isa{{\isasymequiv}{\isacharminus}expand})]{\isa{{\isasymGamma}\ {\isacharbackslash}\ x\ {\isasymequiv}\ t\ {\isasymturnstile}\ B\ t}}{\isa{{\isasymGamma}\ {\isasymturnstile}\ B\ x}} |
221 \] |
221 \] |
222 This works, because the assumption \isa{x\ {\isasymequiv}\ t} was introduced in |
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 |
223 a context with \isa{x} being fresh, so \isa{x} does not |
224 occur in \isa{{\isasymGamma}} here.% |
224 occur in \isa{{\isasymGamma}} here.% |
225 \end{isamarkuptext}% |
225 \end{isamarkuptext}% |
289 reasoning, see \secref{sec:thms}. Unaccounted context manipulations |
289 reasoning, see \secref{sec:thms}. Unaccounted context manipulations |
290 should be avoided, notably raw \isa{{\isasymAnd}{\isacharslash}{\isasymLongrightarrow}} introduction or ad-hoc |
290 should be avoided, notably raw \isa{{\isasymAnd}{\isacharslash}{\isasymLongrightarrow}} introduction or ad-hoc |
291 references to free variables or assumptions not present in the proof |
291 references to free variables or assumptions not present in the proof |
292 context. |
292 context. |
293 |
293 |
294 \medskip The \isa{prove} operation provides an interface for |
294 \medskip The \isa{SUBPROOF} combinator allows to structure a |
295 structured backwards reasoning under program control, with some |
295 tactical proof recursively by decomposing a selected sub-goal: |
296 explicit sanity checks of the result. The goal context can be |
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 augmented by additional fixed variables (cf.\ |
297 after fixing \isa{x} and assuming \isa{A{\isacharparenleft}x{\isacharparenright}}. This means |
298 \secref{sec:variables}) and assumptions (cf.\ |
298 the tactic needs to solve the conclusion, but may use the premise as |
299 \secref{sec:assumptions}), which will be available as local facts |
299 a local fact, for locally fixed variables. |
300 during the proof and discharged into implications in the result. |
300 |
301 Type and term variables are generalized as usual, according to the |
301 The \isa{prove} operation provides an interface for structured |
302 context. |
302 backwards reasoning under program control, with some explicit sanity |
303 |
303 checks of the result. The goal context can be augmented by |
304 The \isa{prove{\isacharunderscore}multi} operation handles several simultaneous |
304 additional fixed variables (cf.\ \secref{sec:variables}) and |
305 claims within a single goal, by using Pure conjunction internally. |
305 assumptions (cf.\ \secref{sec:assumptions}), which will be available |
306 |
306 as local facts during the proof and discharged into implications in |
307 \medskip Tactical proofs may be structured recursively by |
307 the result. Type and term variables are generalized as usual, |
308 decomposing a sub-goal: \isa{{\isacharparenleft}{\isasymAnd}x{\isachardot}\ A{\isacharparenleft}x{\isacharparenright}\ {\isasymLongrightarrow}\ B{\isacharparenleft}x{\isacharparenright}{\isacharparenright}\ {\isasymLongrightarrow}\ {\isasymdots}} is turned |
308 according to the context. |
309 into \isa{B{\isacharparenleft}x{\isacharparenright}\ {\isasymLongrightarrow}\ {\isasymdots}} after fixing \isa{x} and assuming \isa{A{\isacharparenleft}x{\isacharparenright}}.% |
309 |
|
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{isabelle-isar-ref} for the user-level \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.% |
310 \end{isamarkuptext}% |
318 \end{isamarkuptext}% |
311 \isamarkuptrue% |
319 \isamarkuptrue% |
312 % |
320 % |
313 \isadelimmlref |
321 \isadelimmlref |
314 % |
322 % |
316 % |
324 % |
317 \isatagmlref |
325 \isatagmlref |
318 % |
326 % |
319 \begin{isamarkuptext}% |
327 \begin{isamarkuptext}% |
320 \begin{mldecls} |
328 \begin{mldecls} |
|
329 \indexml{SUBPROOF}\verb|SUBPROOF: ({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| \\ |
321 \indexml{Goal.prove}\verb|Goal.prove: Proof.context -> string list -> term list -> term ->|\isasep\isanewline% |
332 \indexml{Goal.prove}\verb|Goal.prove: Proof.context -> string list -> term list -> term ->|\isasep\isanewline% |
322 \verb| ({prems: thm list, context: Proof.context} -> tactic) -> thm| \\ |
333 \verb| ({prems: thm list, context: Proof.context} -> tactic) -> thm| \\ |
323 \indexml{Goal.prove-multi}\verb|Goal.prove_multi: Proof.context -> string list -> term list -> term list ->|\isasep\isanewline% |
334 \indexml{Goal.prove-multi}\verb|Goal.prove_multi: Proof.context -> string list -> term list -> term list ->|\isasep\isanewline% |
324 \verb| ({prems: thm list, context: Proof.context} -> tactic) -> thm list| \\ |
335 \verb| ({prems: thm list, context: Proof.context} -> tactic) -> thm list| \\ |
325 \indexml{SUBPROOF}\verb|SUBPROOF: ({context: Proof.context, schematics: ctyp list * cterm list,|\isasep\isanewline% |
336 \indexml{Obtain.result}\verb|Obtain.result: (Proof.context -> tactic) ->|\isasep\isanewline% |
326 \verb| params: cterm list, asms: cterm list, concl: cterm,|\isasep\isanewline% |
337 \verb| thm list -> Proof.context -> (cterm list * thm list) * Proof.context| |
327 \verb| prems: thm list} -> tactic) -> Proof.context -> int -> tactic| |
|
328 \end{mldecls} |
338 \end{mldecls} |
329 |
339 |
330 \begin{description} |
340 \begin{description} |
331 |
|
332 \item \verb|Goal.prove|~\isa{ctxt\ xs\ As\ C\ tac} states goal \isa{C} in the context augmented by fixed variables \isa{xs} and |
|
333 assumptions \isa{As}, and applies tactic \isa{tac} to solve |
|
334 it. The latter may depend on the local assumptions being presented |
|
335 as facts. The result is in HHF normal form. |
|
336 |
|
337 \item \verb|Goal.prove_multi| is simular to \verb|Goal.prove|, but |
|
338 states several conclusions simultaneously. \verb|Tactic.conjunction_tac| may be used to split these into individual |
|
339 subgoals before commencing the actual proof. |
|
340 |
341 |
341 \item \verb|SUBPROOF|~\isa{tac} decomposes the structure of a |
342 \item \verb|SUBPROOF|~\isa{tac} decomposes the structure of a |
342 particular sub-goal, producing an extended context and a reduced |
343 particular sub-goal, producing an extended context and a reduced |
343 goal, which needs to be solved by the given tactic. All schematic |
344 goal, which needs to be solved by the given tactic. All schematic |
344 parameters of the goal are imported into the context as fixed ones, |
345 parameters of the goal are imported into the context as fixed ones, |
345 which may not be instantiated in the sub-proof. |
346 which may not be instantiated in the sub-proof. |
|
347 |
|
348 \item \verb|Goal.prove|~\isa{ctxt\ xs\ As\ C\ tac} states goal \isa{C} in the context augmented by fixed variables \isa{xs} and |
|
349 assumptions \isa{As}, and applies tactic \isa{tac} to solve |
|
350 it. The latter may depend on the local assumptions being presented |
|
351 as facts. The result is in HHF normal form. |
|
352 |
|
353 \item \verb|Goal.prove_multi| is simular to \verb|Goal.prove|, but |
|
354 states several conclusions simultaneously. The goal is encoded by |
|
355 means of Pure conjunction; \verb|Tactic.conjunction_tac| will turn |
|
356 this into a collection of individual subgoals. |
|
357 |
|
358 \item \verb|Obtain.result|~\isa{tac\ thms\ ctxt} eliminates the |
|
359 given facts using a tactic, which results in additional fixed |
|
360 variables and assumptions in the context. Final results need to be |
|
361 exported explicitly. |
346 |
362 |
347 \end{description}% |
363 \end{description}% |
348 \end{isamarkuptext}% |
364 \end{isamarkuptext}% |
349 \isamarkuptrue% |
365 \isamarkuptrue% |
350 % |
366 % |