287 \end{isabelle} |
287 \end{isabelle} |
288 \caption{The figure shows a proof where each intermediate goal state is |
288 \caption{The figure shows a proof where each intermediate goal state is |
289 printed by the Isabelle system and by @{ML my_print_tac}. The latter shows |
289 printed by the Isabelle system and by @{ML my_print_tac}. The latter shows |
290 the goal state as represented internally (highlighted boxes). This |
290 the goal state as represented internally (highlighted boxes). This |
291 illustrates that every goal state in Isabelle is represented by a theorem: |
291 illustrates that every goal state in Isabelle is represented by a theorem: |
292 when we start the proof of \mbox{@{text "\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B"}} the theorem is |
292 when you start the proof of \mbox{@{text "\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B"}} the theorem is |
293 @{text "(\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B) \<Longrightarrow> (\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B)"}; when we finish the proof the |
293 @{text "(\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B) \<Longrightarrow> (\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B)"}; when you finish the proof the |
294 theorem is @{text "\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B"}.\label{fig:goalstates}} |
294 theorem is @{text "\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B"}.\label{fig:goalstates}} |
295 \end{figure} |
295 \end{figure} |
296 *} |
296 *} |
297 |
297 |
298 |
298 |
326 |
326 |
327 section {* Simple Tactics *} |
327 section {* Simple Tactics *} |
328 |
328 |
329 text {* |
329 text {* |
330 Let us start with the tactic @{ML print_tac}, which is quite useful for low-level |
330 Let us start with the tactic @{ML print_tac}, which is quite useful for low-level |
331 debugging of tactics. It just prints out a message and the current goal state. |
331 debugging of tactics. It just prints out a message and the current goal state |
332 Processing the proof |
332 (unlike @{ML my_print_tac} it prints the goal state as the user would see it). |
|
333 For example, processing the proof |
333 *} |
334 *} |
334 |
335 |
335 lemma shows "False \<Longrightarrow> True" |
336 lemma shows "False \<Longrightarrow> True" |
336 apply(tactic {* print_tac "foo message" *}) |
337 apply(tactic {* print_tac "foo message" *}) |
337 txt{*gives:\medskip |
338 txt{*gives:\medskip |
384 \end{minipage}*} |
385 \end{minipage}*} |
385 (*<*)oops(*>*) |
386 (*<*)oops(*>*) |
386 |
387 |
387 text {* |
388 text {* |
388 Note the number in each tactic call. Also as mentioned in the previous section, most |
389 Note the number in each tactic call. Also as mentioned in the previous section, most |
389 basic tactics take such an argument; it addresses the subgoal they are analysing. |
390 basic tactics take such a number as argument; it addresses the subgoal they are analysing. |
390 In the proof below, we first split up the conjunction in the second subgoal by |
391 In the proof below, we first split up the conjunction in the second subgoal by |
391 focusing on this subgoal first. |
392 focusing on this subgoal first. |
392 *} |
393 *} |
393 |
394 |
394 lemma shows "Foo" and "P \<and> Q" |
395 lemma shows "Foo" and "P \<and> Q" |
690 analysed. Similarly with meta-implications in the next line. While for the |
691 analysed. Similarly with meta-implications in the next line. While for the |
691 first five patterns we can use the @{text "@term"}-antiquotation to |
692 first five patterns we can use the @{text "@term"}-antiquotation to |
692 construct the patterns, the pattern in Line 8 cannot be constructed in this |
693 construct the patterns, the pattern in Line 8 cannot be constructed in this |
693 way. The reason is that an antiquotation would fix the type of the |
694 way. The reason is that an antiquotation would fix the type of the |
694 quantified variable. So you really have to construct the pattern using the |
695 quantified variable. So you really have to construct the pattern using the |
695 basic term-constructors. This is not necessary in other cases, because their type |
696 basic term-constructors. This is not necessary in other cases, because their |
696 is always fixed to function types involving only the type @{typ bool}. For the |
697 type is always fixed to function types involving only the type @{typ |
697 final pattern, we chose to just return @{ML all_tac}. Consequently, |
698 bool}. (See Section \ref{sec:terms_types_manually} about constructing terms |
698 @{ML select_tac} never fails. |
699 manually.) For the catch-all pattern, we chose to just return @{ML all_tac}. |
|
700 Consequently, @{ML select_tac} never fails. |
|
701 |
699 |
702 |
700 Let us now see how to apply this tactic. Consider the four goals: |
703 Let us now see how to apply this tactic. Consider the four goals: |
701 *} |
704 *} |
702 |
705 |
703 |
706 |
922 because otherwise @{ML REPEAT} runs into an infinite loop (it applies the |
925 because otherwise @{ML REPEAT} runs into an infinite loop (it applies the |
923 tactic as long as it succeeds). The function |
926 tactic as long as it succeeds). The function |
924 @{ML REPEAT1} is similar, but runs the tactic at least once (failing if |
927 @{ML REPEAT1} is similar, but runs the tactic at least once (failing if |
925 this is not possible). |
928 this is not possible). |
926 |
929 |
927 If you are after the ``primed'' version of @{ML repeat_xmp} then you |
930 If you are after the ``primed'' version of @{ML repeat_xmp}, then you |
928 need to implement it as |
931 need to implement it as |
929 *} |
932 *} |
930 |
933 |
931 ML{*val repeat_xmp' = REPEAT o CHANGED o select_tac'*} |
934 ML{*val repeat_xmp' = REPEAT o CHANGED o select_tac'*} |
932 |
935 |