14 steps until all of them are solved. However, there are also more structured |
14 steps until all of them are solved. However, there are also more structured |
15 operations available on the ML-level that help with the handling of |
15 operations available on the ML-level that help with the handling of |
16 variables and assumptions. |
16 variables and assumptions. |
17 |
17 |
18 *} |
18 *} |
|
19 |
19 |
20 |
20 section {* Basics of Reasoning with Tactics*} |
21 section {* Basics of Reasoning with Tactics*} |
21 |
22 |
22 text {* |
23 text {* |
23 To see how tactics work, let us first transcribe a simple \isacommand{apply}-style proof |
24 To see how tactics work, let us first transcribe a simple \isacommand{apply}-style proof |
220 text_raw {* |
221 text_raw {* |
221 \begin{figure}[p] |
222 \begin{figure}[p] |
222 \begin{boxedminipage}{\textwidth} |
223 \begin{boxedminipage}{\textwidth} |
223 \begin{isabelle} |
224 \begin{isabelle} |
224 *} |
225 *} |
|
226 notation (output) "prop" ("#_" [1000] 1000) |
|
227 |
225 lemma shows "\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B" |
228 lemma shows "\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B" |
226 apply(tactic {* my_print_tac @{context} *}) |
229 apply(tactic {* my_print_tac @{context} *}) |
227 |
230 |
228 txt{* \begin{minipage}{\textwidth} |
231 txt{* \begin{minipage}{\textwidth} |
229 @{subgoals [display]} |
232 @{subgoals [display]} |
247 |
250 |
248 \begin{minipage}{\textwidth} |
251 \begin{minipage}{\textwidth} |
249 \small\colorbox{gray!20}{ |
252 \small\colorbox{gray!20}{ |
250 \begin{tabular}{@ {}l@ {}} |
253 \begin{tabular}{@ {}l@ {}} |
251 internal goal state:\\ |
254 internal goal state:\\ |
252 @{text "(\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A) \<Longrightarrow> (\<lbrakk>A; B\<rbrakk> \<Longrightarrow> B) \<Longrightarrow> (\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B)"} |
255 @{raw_goal_state} |
253 \end{tabular}} |
256 \end{tabular}} |
254 \end{minipage}\medskip |
257 \end{minipage}\medskip |
255 *} |
258 *} |
256 |
259 |
257 apply(assumption) |
260 apply(assumption) |
279 |
282 |
280 \begin{minipage}{\textwidth} |
283 \begin{minipage}{\textwidth} |
281 \small\colorbox{gray!20}{ |
284 \small\colorbox{gray!20}{ |
282 \begin{tabular}{@ {}l@ {}} |
285 \begin{tabular}{@ {}l@ {}} |
283 internal goal state:\\ |
286 internal goal state:\\ |
284 @{text "\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B"} |
287 @{raw_goal_state} |
285 \end{tabular}} |
288 \end{tabular}} |
286 \end{minipage}\medskip |
289 \end{minipage}\medskip |
287 *} |
290 *} |
288 done |
291 (*<*)oops(*>*) |
289 text_raw {* |
292 text_raw {* |
290 \end{isabelle} |
293 \end{isabelle} |
291 \end{boxedminipage} |
294 \end{boxedminipage} |
292 \caption{The figure shows a proof where each intermediate goal state is |
295 \caption{The figure shows a proof where each intermediate goal state is |
293 printed by the Isabelle system and by @{ML my_print_tac}. The latter shows |
296 printed by the Isabelle system and by @{ML my_print_tac}. The latter shows |
294 the goal state as represented internally (highlighted boxes). This |
297 the goal state as represented internally (highlighted boxes). This |
295 tactic shows that every goal state in Isabelle is represented by a theorem: |
298 tactic shows that every goal state in Isabelle is represented by a theorem: |
296 when you start the proof of \mbox{@{text "\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B"}} the theorem is |
299 when you start the proof of \mbox{@{text "\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B"}} the theorem is |
297 @{text "(\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B) \<Longrightarrow> (\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B)"}; when you finish the proof the |
300 @{text "(\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B) \<Longrightarrow> #(\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B)"}; when you finish the proof the |
298 theorem is @{text "\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B"}.\label{fig:goalstates}} |
301 theorem is @{text "#(\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B)"}.\label{fig:goalstates}} |
299 \end{figure} |
302 \end{figure} |
300 *} |
303 *} |
301 |
304 |
302 |
305 |
303 text {* |
306 text {* |
305 Section~\ref{sec:printing}) and then behaves like @{ML all_tac}. With this |
308 Section~\ref{sec:printing}) and then behaves like @{ML all_tac}. With this |
306 tactic we are in the position to inspect every goal state in a |
309 tactic we are in the position to inspect every goal state in a |
307 proof. Consider now the proof in Figure~\ref{fig:goalstates}: as can be seen, |
310 proof. Consider now the proof in Figure~\ref{fig:goalstates}: as can be seen, |
308 internally every goal state is an implication of the form |
311 internally every goal state is an implication of the form |
309 |
312 |
310 @{text[display] "A\<^isub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^isub>n \<Longrightarrow> (C)"} |
313 @{text[display] "A\<^isub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^isub>n \<Longrightarrow> #C"} |
311 |
314 |
312 where @{term C} is the goal to be proved and the @{term "A\<^isub>i"} are |
315 where @{term C} is the goal to be proved and the @{term "A\<^isub>i"} are |
313 the subgoals. So after setting up the lemma, the goal state is always of the |
316 the subgoals. So after setting up the lemma, the goal state is always of the |
314 form @{text "C \<Longrightarrow> (C)"}; when the proof is finished we are left with @{text |
317 form @{text "C \<Longrightarrow> #C"}; when the proof is finished we are left with @{text |
315 "(C)"}.\footnote{This only applies to single statements. If the lemma |
318 "#C"}.\footnote{This only applies to single statements. If the lemma |
316 contains more than one statement, then one has more such implications.} |
319 contains more than one statement, then one has more such implications.} |
317 Since the goal @{term C} can potentially be an implication, there is a |
320 Since the goal @{term C} can potentially be an implication, there is a |
318 ``protector'' wrapped around it (the wrapper is the outermost constant |
321 ``protector'' wrapped around it (the wrapper is the outermost constant |
319 @{text "Const (\"prop\", bool \<Rightarrow> bool)"}; however this constant is invisible |
322 @{text "Const (\"prop\", bool \<Rightarrow> bool)"}; in the figure we make it visible |
320 in the figure). This wrapper prevents that premises of @{text C} are |
323 as an @{text #}). This wrapper prevents that premises of @{text C} are |
321 misinterpreted as open subgoals. While tactics can operate on the subgoals |
324 misinterpreted as open subgoals. While tactics can operate on the subgoals |
322 (the @{text "A\<^isub>i"} above), they are expected to leave the conclusion |
325 (the @{text "A\<^isub>i"} above), they are expected to leave the conclusion |
323 @{term C} intact, with the exception of possibly instantiating schematic |
326 @{term C} intact, with the exception of possibly instantiating schematic |
324 variables. If you use the predefined tactics, which we describe in the next |
327 variables. If you use the predefined tactics, which we describe in the next |
325 section, this will always be the case. |
328 section, this will always be the case. |