256 reasoning, see \secref{sec:thms}. Unaccounted context manipulations |
256 reasoning, see \secref{sec:thms}. Unaccounted context manipulations |
257 should be avoided, notably raw @{text "\<And>/\<Longrightarrow>"} introduction or ad-hoc |
257 should be avoided, notably raw @{text "\<And>/\<Longrightarrow>"} introduction or ad-hoc |
258 references to free variables or assumptions not present in the proof |
258 references to free variables or assumptions not present in the proof |
259 context. |
259 context. |
260 |
260 |
261 \medskip The @{text "prove"} operation provides an interface for |
261 \medskip The @{text "SUBPROOF"} combinator allows to structure a |
262 structured backwards reasoning under program control, with some |
262 tactical proof recursively by decomposing a selected sub-goal: |
263 explicit sanity checks of the result. The goal context can be |
263 @{text "(\<And>x. A(x) \<Longrightarrow> B(x)) \<Longrightarrow> \<dots>"} is turned into @{text "B(x) \<Longrightarrow> \<dots>"} |
264 augmented by additional fixed variables (cf.\ |
264 after fixing @{text "x"} and assuming @{text "A(x)"}. This means |
265 \secref{sec:variables}) and assumptions (cf.\ |
265 the tactic needs to solve the conclusion, but may use the premise as |
266 \secref{sec:assumptions}), which will be available as local facts |
266 a local fact, for locally fixed variables. |
267 during the proof and discharged into implications in the result. |
267 |
268 Type and term variables are generalized as usual, according to the |
268 The @{text "prove"} operation provides an interface for structured |
269 context. |
269 backwards reasoning under program control, with some explicit sanity |
270 |
270 checks of the result. The goal context can be augmented by |
271 The @{text "prove_multi"} operation handles several simultaneous |
271 additional fixed variables (cf.\ \secref{sec:variables}) and |
272 claims within a single goal, by using Pure conjunction internally. |
272 assumptions (cf.\ \secref{sec:assumptions}), which will be available |
273 |
273 as local facts during the proof and discharged into implications in |
274 \medskip Tactical proofs may be structured recursively by |
274 the result. Type and term variables are generalized as usual, |
275 decomposing a sub-goal: @{text "(\<And>x. A(x) \<Longrightarrow> B(x)) \<Longrightarrow> \<dots>"} is turned |
275 according to the context. |
276 into @{text "B(x) \<Longrightarrow> \<dots>"} after fixing @{text "x"} and assuming @{text |
276 |
277 "A(x)"}. |
277 The @{text "obtain"} operation produces results by eliminating |
|
278 existing facts by means of a given tactic. This acts like a dual |
|
279 conclusion: the proof demonstrates that the context may be augmented |
|
280 by certain fixed variables and assumptions. See also |
|
281 \cite{isabelle-isar-ref} for the user-level @{text "\<OBTAIN>"} and |
|
282 @{text "\<GUESS>"} elements. Final results, which may not refer to |
|
283 the parameters in the conclusion, need to exported explicitly into |
|
284 the original context. |
278 *} |
285 *} |
279 |
286 |
280 text %mlref {* |
287 text %mlref {* |
281 \begin{mldecls} |
288 \begin{mldecls} |
|
289 @{index_ML SUBPROOF: |
|
290 "({context: Proof.context, schematics: ctyp list * cterm list, |
|
291 params: cterm list, asms: cterm list, concl: cterm, |
|
292 prems: thm list} -> tactic) -> Proof.context -> int -> tactic"} \\ |
282 @{index_ML Goal.prove: "Proof.context -> string list -> term list -> term -> |
293 @{index_ML Goal.prove: "Proof.context -> string list -> term list -> term -> |
283 ({prems: thm list, context: Proof.context} -> tactic) -> thm"} \\ |
294 ({prems: thm list, context: Proof.context} -> tactic) -> thm"} \\ |
284 @{index_ML Goal.prove_multi: "Proof.context -> string list -> term list -> term list -> |
295 @{index_ML Goal.prove_multi: "Proof.context -> string list -> term list -> term list -> |
285 ({prems: thm list, context: Proof.context} -> tactic) -> thm list"} \\ |
296 ({prems: thm list, context: Proof.context} -> tactic) -> thm list"} \\ |
286 @{index_ML SUBPROOF: |
297 @{index_ML Obtain.result: "(Proof.context -> tactic) -> |
287 "({context: Proof.context, schematics: ctyp list * cterm list, |
298 thm list -> Proof.context -> (cterm list * thm list) * Proof.context"} |
288 params: cterm list, asms: cterm list, concl: cterm, |
|
289 prems: thm list} -> tactic) -> Proof.context -> int -> tactic"} |
|
290 \end{mldecls} |
299 \end{mldecls} |
291 |
300 |
292 \begin{description} |
301 \begin{description} |
|
302 |
|
303 \item @{ML SUBPROOF}~@{text "tac"} decomposes the structure of a |
|
304 particular sub-goal, producing an extended context and a reduced |
|
305 goal, which needs to be solved by the given tactic. All schematic |
|
306 parameters of the goal are imported into the context as fixed ones, |
|
307 which may not be instantiated in the sub-proof. |
293 |
308 |
294 \item @{ML Goal.prove}~@{text "ctxt xs As C tac"} states goal @{text |
309 \item @{ML Goal.prove}~@{text "ctxt xs As C tac"} states goal @{text |
295 "C"} in the context augmented by fixed variables @{text "xs"} and |
310 "C"} in the context augmented by fixed variables @{text "xs"} and |
296 assumptions @{text "As"}, and applies tactic @{text "tac"} to solve |
311 assumptions @{text "As"}, and applies tactic @{text "tac"} to solve |
297 it. The latter may depend on the local assumptions being presented |
312 it. The latter may depend on the local assumptions being presented |
298 as facts. The result is in HHF normal form. |
313 as facts. The result is in HHF normal form. |
299 |
314 |
300 \item @{ML Goal.prove_multi} is simular to @{ML Goal.prove}, but |
315 \item @{ML Goal.prove_multi} is simular to @{ML Goal.prove}, but |
301 states several conclusions simultaneously. @{ML |
316 states several conclusions simultaneously. The goal is encoded by |
302 Tactic.conjunction_tac} may be used to split these into individual |
317 means of Pure conjunction; @{ML Tactic.conjunction_tac} will turn |
303 subgoals before commencing the actual proof. |
318 this into a collection of individual subgoals. |
304 |
319 |
305 \item @{ML SUBPROOF}~@{text "tac"} decomposes the structure of a |
320 \item @{ML Obtain.result}~@{text "tac thms ctxt"} eliminates the |
306 particular sub-goal, producing an extended context and a reduced |
321 given facts using a tactic, which results in additional fixed |
307 goal, which needs to be solved by the given tactic. All schematic |
322 variables and assumptions in the context. Final results need to be |
308 parameters of the goal are imported into the context as fixed ones, |
323 exported explicitly. |
309 which may not be instantiated in the sub-proof. |
|
310 |
324 |
311 \end{description} |
325 \end{description} |
312 *} |
326 *} |
313 |
327 |
314 end |
328 end |