equal
deleted
inserted
replaced
68 Isabelle Reference Manual. |
68 Isabelle Reference Manual. |
69 \end{readmore} |
69 \end{readmore} |
70 |
70 |
71 Note that in the code above we used antiquotations for referencing the theorems. Many theorems |
71 Note that in the code above we used antiquotations for referencing the theorems. Many theorems |
72 also have ML-bindings with the same name. Therefore, we could also just have |
72 also have ML-bindings with the same name. Therefore, we could also just have |
73 written @{ML "etac disjE 1"}, or in case there are no ML-binding obtained |
73 written @{ML "etac disjE 1"}, or in case where there are no ML-binding obtain |
74 the theorem dynamically using the function @{ML thm}; for example |
74 the theorem dynamically using the function @{ML thm}; for example |
75 \mbox{@{ML "etac (thm \"disjE\") 1"}}. Both ways however are considered bad style! |
75 \mbox{@{ML "etac (thm \"disjE\") 1"}}. Both ways however are considered bad style! |
76 The reason |
76 The reason |
77 is that the binding for @{ML disjE} can be re-assigned by the user and thus |
77 is that the binding for @{ML disjE} can be re-assigned by the user and thus |
78 one does not have complete control over which theorem is actually |
78 one does not have complete control over which theorem is actually |
282 \end{minipage}\medskip |
282 \end{minipage}\medskip |
283 *} |
283 *} |
284 done |
284 done |
285 text_raw {* |
285 text_raw {* |
286 \end{isabelle} |
286 \end{isabelle} |
287 \caption{A proof where we show the goal state as printed |
287 \caption{The figure shows a proof where each intermediate goal state is |
288 by the Isabelle system and as represented internally |
288 printed by the Isabelle system and by @{ML my_print_tac}. The latter shows |
289 (highlighted boxes).\label{fig:goalstates}} |
289 the goal state as represented internally (highlighted boxes). This |
|
290 illustrates that every goal state in Isabelle is represented by a theorem: |
|
291 when we start the proof of \mbox{@{text "\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B"}} the theorem is |
|
292 @{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 theorem is @{text "\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B"}.\label{fig:goalstates}} |
290 \end{figure} |
294 \end{figure} |
291 *} |
295 *} |
292 |
296 |
293 |
297 |
294 text {* |
298 text {* |
441 shown above. The reason is that a number of rules introduce meta-variables |
445 shown above. The reason is that a number of rules introduce meta-variables |
442 into the goal state. Consider for example the proof |
446 into the goal state. Consider for example the proof |
443 *} |
447 *} |
444 |
448 |
445 lemma shows "\<forall>x\<in>A. P x \<Longrightarrow> Q x" |
449 lemma shows "\<forall>x\<in>A. P x \<Longrightarrow> Q x" |
446 apply(drule bspec) |
450 apply(tactic {* dtac @{thm bspec} 1 *}) |
447 txt{*\begin{minipage}{\textwidth} |
451 txt{*\begin{minipage}{\textwidth} |
448 @{subgoals [display]} |
452 @{subgoals [display]} |
449 \end{minipage}*} |
453 \end{minipage}*} |
450 (*<*)oops(*>*) |
454 (*<*)oops(*>*) |
451 |
455 |
593 |
597 |
594 apply(rule impI) |
598 apply(rule impI) |
595 apply(tactic {* SUBPROOF sp_tac @{context} 1 *})? |
599 apply(tactic {* SUBPROOF sp_tac @{context} 1 *})? |
596 |
600 |
597 txt {* |
601 txt {* |
598 then tactic prints out |
602 then the tactic prints out: |
599 |
603 |
600 \begin{quote}\small |
604 \begin{quote}\small |
601 \begin{tabular}{ll} |
605 \begin{tabular}{ll} |
602 params: & @{term x}, @{term y}\\ |
606 params: & @{term x}, @{term y}\\ |
603 schematics: & @{term z}\\ |
607 schematics: & @{term z}\\ |
685 first five patterns we can use the @{text "@term"}-antiquotation to |
689 first five patterns we can use the @{text "@term"}-antiquotation to |
686 construct the patterns, the pattern in Line 8 cannot be constructed in this |
690 construct the patterns, the pattern in Line 8 cannot be constructed in this |
687 way. The reason is that an antiquotation would fix the type of the |
691 way. The reason is that an antiquotation would fix the type of the |
688 quantified variable. So you really have to construct the pattern using the |
692 quantified variable. So you really have to construct the pattern using the |
689 basic term-constructors. This is not necessary in other cases, because their type |
693 basic term-constructors. This is not necessary in other cases, because their type |
690 is always fixed to function types involving only the type @{typ bool}. The |
694 is always fixed to function types involving only the type @{typ bool}. For the |
691 final pattern, we chose to just return @{ML all_tac}. Consequently, |
695 final pattern, we chose to just return @{ML all_tac}. Consequently, |
692 @{ML select_tac} never fails. |
696 @{ML select_tac} never fails. |
693 |
697 |
694 Let us now see how to apply this tactic. Consider the four goals: |
698 Let us now see how to apply this tactic. Consider the four goals: |
695 *} |
699 *} |
782 |
786 |
783 ML{*val foo_tac1 = EVERY1 [etac @{thm disjE}, rtac @{thm disjI2}, |
787 ML{*val foo_tac1 = EVERY1 [etac @{thm disjE}, rtac @{thm disjI2}, |
784 atac, rtac @{thm disjI1}, atac]*} |
788 atac, rtac @{thm disjI1}, atac]*} |
785 |
789 |
786 text {* |
790 text {* |
787 and just call @{ML foo_tac1}. |
791 and call @{ML foo_tac1}. |
788 |
792 |
789 With the combinators @{ML THEN'}, @{ML EVERY'} and @{ML EVERY1} it must be |
793 With the combinators @{ML THEN'}, @{ML EVERY'} and @{ML EVERY1} it must be |
790 guaranteed that all component tactics successfully apply; otherwise the |
794 guaranteed that all component tactics successfully apply; otherwise the |
791 whole tactic will fail. If you rather want to try out a number of tactics, |
795 whole tactic will fail. If you rather want to try out a number of tactics, |
792 then you can use the combinator @{ML ORELSE'} for two tactics, and @{ML |
796 then you can use the combinator @{ML ORELSE'} for two tactics, and @{ML |
822 rtac @{thm notI}, rtac @{thm allI}, K all_tac]*} |
826 rtac @{thm notI}, rtac @{thm allI}, K all_tac]*} |
823 |
827 |
824 text {* |
828 text {* |
825 Since we like to mimic the behaviour of @{ML select_tac} as closely as possible, |
829 Since we like to mimic the behaviour of @{ML select_tac} as closely as possible, |
826 we must include @{ML all_tac} at the end of the list, otherwise the tactic will |
830 we must include @{ML all_tac} at the end of the list, otherwise the tactic will |
827 fail if no rule applies (we laso have to wrap @{ML all_tac} using the |
831 fail if no rule applies (we also have to wrap @{ML all_tac} using the |
828 @{ML K}-combinator, because it does not take a subgoal number as argument). You can |
832 @{ML K}-combinator, because it does not take a subgoal number as argument). You can |
829 test the tactic on the same goals: |
833 test the tactic on the same goals: |
830 *} |
834 *} |
831 |
835 |
832 lemma shows "A \<and> B" and "A \<longrightarrow> B \<longrightarrow>C" and "\<forall>x. D x" and "E \<Longrightarrow> F" |
836 lemma shows "A \<and> B" and "A \<longrightarrow> B \<longrightarrow>C" and "\<forall>x. D x" and "E \<Longrightarrow> F" |
990 txt {*\begin{minipage}{\textwidth} |
994 txt {*\begin{minipage}{\textwidth} |
991 @{subgoals [display]} |
995 @{subgoals [display]} |
992 \end{minipage} *} |
996 \end{minipage} *} |
993 (*<*)oops(*>*) |
997 (*<*)oops(*>*) |
994 text {* |
998 text {* |
995 This will combinator prune the search space to just the first successful application. |
999 This combinator will prune the search space to just the first successful application. |
996 Attempting to apply \isacommand{back} in this goal states gives the |
1000 Attempting to apply \isacommand{back} in this goal states gives the |
997 error message: |
1001 error message: |
998 |
1002 |
999 \begin{isabelle} |
1003 \begin{isabelle} |
1000 @{text "*** back: no alternatives"}\\ |
1004 @{text "*** back: no alternatives"}\\ |