1.1 --- a/doc-src/IsarRef/Thy/Proof.thy Thu Nov 13 21:37:18 2008 +0100
1.2 +++ b/doc-src/IsarRef/Thy/Proof.thy Thu Nov 13 21:38:02 2008 +0100
1.3 @@ -42,6 +42,81 @@
1.4 *}
1.5
1.6
1.7 +section {* Proof structure *}
1.8 +
1.9 +subsection {* Blocks *}
1.10 +
1.11 +text {*
1.12 + \begin{matharray}{rcl}
1.13 + @{command_def "next"} & : & \isartrans{proof(state)}{proof(state)} \\
1.14 + @{command_def "{"} & : & \isartrans{proof(state)}{proof(state)} \\
1.15 + @{command_def "}"} & : & \isartrans{proof(state)}{proof(state)} \\
1.16 + \end{matharray}
1.17 +
1.18 + While Isar is inherently block-structured, opening and closing
1.19 + blocks is mostly handled rather casually, with little explicit
1.20 + user-intervention. Any local goal statement automatically opens
1.21 + \emph{two} internal blocks, which are closed again when concluding
1.22 + the sub-proof (by @{command "qed"} etc.). Sections of different
1.23 + context within a sub-proof may be switched via @{command "next"},
1.24 + which is just a single block-close followed by block-open again.
1.25 + The effect of @{command "next"} is to reset the local proof context;
1.26 + there is no goal focus involved here!
1.27 +
1.28 + For slightly more advanced applications, there are explicit block
1.29 + parentheses as well. These typically achieve a stronger forward
1.30 + style of reasoning.
1.31 +
1.32 + \begin{descr}
1.33 +
1.34 + \item [@{command "next"}] switches to a fresh block within a
1.35 + sub-proof, resetting the local context to the initial one.
1.36 +
1.37 + \item [@{command "{"} and @{command "}"}] explicitly open and close
1.38 + blocks. Any current facts pass through ``@{command "{"}''
1.39 + unchanged, while ``@{command "}"}'' causes any result to be
1.40 + \emph{exported} into the enclosing context. Thus fixed variables
1.41 + are generalized, assumptions discharged, and local definitions
1.42 + unfolded (cf.\ \secref{sec:proof-context}). There is no difference
1.43 + of @{command "assume"} and @{command "presume"} in this mode of
1.44 + forward reasoning --- in contrast to plain backward reasoning with
1.45 + the result exported at @{command "show"} time.
1.46 +
1.47 + \end{descr}
1.48 +*}
1.49 +
1.50 +
1.51 +subsection {* Omitting proofs *}
1.52 +
1.53 +text {*
1.54 + \begin{matharray}{rcl}
1.55 + @{command_def "oops"} & : & \isartrans{proof}{theory} \\
1.56 + \end{matharray}
1.57 +
1.58 + The @{command "oops"} command discontinues the current proof
1.59 + attempt, while considering the partial proof text as properly
1.60 + processed. This is conceptually quite different from ``faking''
1.61 + actual proofs via @{command_ref "sorry"} (see
1.62 + \secref{sec:proof-steps}): @{command "oops"} does not observe the
1.63 + proof structure at all, but goes back right to the theory level.
1.64 + Furthermore, @{command "oops"} does not produce any result theorem
1.65 + --- there is no intended claim to be able to complete the proof
1.66 + anyhow.
1.67 +
1.68 + A typical application of @{command "oops"} is to explain Isar proofs
1.69 + \emph{within} the system itself, in conjunction with the document
1.70 + preparation tools of Isabelle described in \cite{isabelle-sys}.
1.71 + Thus partial or even wrong proof attempts can be discussed in a
1.72 + logically sound manner. Note that the Isabelle {\LaTeX} macros can
1.73 + be easily adapted to print something like ``@{text "\<dots>"}'' instead of
1.74 + the keyword ``@{command "oops"}''.
1.75 +
1.76 + \medskip The @{command "oops"} command is undo-able, unlike
1.77 + @{command_ref "kill"} (see \secref{sec:history}). The effect is to
1.78 + get back to the theory just before the opening of the proof.
1.79 +*}
1.80 +
1.81 +
1.82 section {* Statements *}
1.83
1.84 subsection {* Context elements \label{sec:proof-context} *}
1.85 @@ -822,79 +897,6 @@
1.86 *}
1.87
1.88
1.89 -section {* Block structure *}
1.90 -
1.91 -text {*
1.92 - \begin{matharray}{rcl}
1.93 - @{command_def "next"} & : & \isartrans{proof(state)}{proof(state)} \\
1.94 - @{command_def "{"} & : & \isartrans{proof(state)}{proof(state)} \\
1.95 - @{command_def "}"} & : & \isartrans{proof(state)}{proof(state)} \\
1.96 - \end{matharray}
1.97 -
1.98 - While Isar is inherently block-structured, opening and closing
1.99 - blocks is mostly handled rather casually, with little explicit
1.100 - user-intervention. Any local goal statement automatically opens
1.101 - \emph{two} internal blocks, which are closed again when concluding
1.102 - the sub-proof (by @{command "qed"} etc.). Sections of different
1.103 - context within a sub-proof may be switched via @{command "next"},
1.104 - which is just a single block-close followed by block-open again.
1.105 - The effect of @{command "next"} is to reset the local proof context;
1.106 - there is no goal focus involved here!
1.107 -
1.108 - For slightly more advanced applications, there are explicit block
1.109 - parentheses as well. These typically achieve a stronger forward
1.110 - style of reasoning.
1.111 -
1.112 - \begin{descr}
1.113 -
1.114 - \item [@{command "next"}] switches to a fresh block within a
1.115 - sub-proof, resetting the local context to the initial one.
1.116 -
1.117 - \item [@{command "{"} and @{command "}"}] explicitly open and close
1.118 - blocks. Any current facts pass through ``@{command "{"}''
1.119 - unchanged, while ``@{command "}"}'' causes any result to be
1.120 - \emph{exported} into the enclosing context. Thus fixed variables
1.121 - are generalized, assumptions discharged, and local definitions
1.122 - unfolded (cf.\ \secref{sec:proof-context}). There is no difference
1.123 - of @{command "assume"} and @{command "presume"} in this mode of
1.124 - forward reasoning --- in contrast to plain backward reasoning with
1.125 - the result exported at @{command "show"} time.
1.126 -
1.127 - \end{descr}
1.128 -*}
1.129 -
1.130 -
1.131 -section {* Omitting proofs *}
1.132 -
1.133 -text {*
1.134 - \begin{matharray}{rcl}
1.135 - @{command_def "oops"} & : & \isartrans{proof}{theory} \\
1.136 - \end{matharray}
1.137 -
1.138 - The @{command "oops"} command discontinues the current proof
1.139 - attempt, while considering the partial proof text as properly
1.140 - processed. This is conceptually quite different from ``faking''
1.141 - actual proofs via @{command_ref "sorry"} (see
1.142 - \secref{sec:proof-steps}): @{command "oops"} does not observe the
1.143 - proof structure at all, but goes back right to the theory level.
1.144 - Furthermore, @{command "oops"} does not produce any result theorem
1.145 - --- there is no intended claim to be able to complete the proof
1.146 - anyhow.
1.147 -
1.148 - A typical application of @{command "oops"} is to explain Isar proofs
1.149 - \emph{within} the system itself, in conjunction with the document
1.150 - preparation tools of Isabelle described in \cite{isabelle-sys}.
1.151 - Thus partial or even wrong proof attempts can be discussed in a
1.152 - logically sound manner. Note that the Isabelle {\LaTeX} macros can
1.153 - be easily adapted to print something like ``@{text "\<dots>"}'' instead of
1.154 - the keyword ``@{command "oops"}''.
1.155 -
1.156 - \medskip The @{command "oops"} command is undo-able, unlike
1.157 - @{command_ref "kill"} (see \secref{sec:history}). The effect is to
1.158 - get back to the theory just before the opening of the proof.
1.159 -*}
1.160 -
1.161 -
1.162 section {* Generalized elimination \label{sec:obtain} *}
1.163
1.164 text {*