75 Induction is invoked by \methdx{induct_tac}, as we have seen above; |
75 Induction is invoked by \methdx{induct_tac}, as we have seen above; |
76 it works for any datatype. In some cases, induction is overkill and a case |
76 it works for any datatype. In some cases, induction is overkill and a case |
77 distinction over all constructors of the datatype suffices. This is performed |
77 distinction over all constructors of the datatype suffices. This is performed |
78 by \methdx{case_tac}. Here is a trivial example:% |
78 by \methdx{case_tac}. Here is a trivial example:% |
79 \end{isamarkuptext}% |
79 \end{isamarkuptext}% |
80 \isamarkupfalse% |
80 \isamarkuptrue% |
81 \isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}case\ xs\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbar}\ y{\isacharhash}ys\ {\isasymRightarrow}\ xs{\isacharparenright}\ {\isacharequal}\ xs{\isachardoublequote}\isanewline |
81 \isacommand{lemma}\isamarkupfalse% |
|
82 \ {\isachardoublequoteopen}{\isacharparenleft}case\ xs\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbar}\ y{\isacharhash}ys\ {\isasymRightarrow}\ xs{\isacharparenright}\ {\isacharequal}\ xs{\isachardoublequoteclose}\isanewline |
82 % |
83 % |
83 \isadelimproof |
84 \isadelimproof |
84 % |
85 % |
85 \endisadelimproof |
86 \endisadelimproof |
86 % |
87 % |
87 \isatagproof |
88 \isatagproof |
88 \isamarkupfalse% |
89 \isacommand{apply}\isamarkupfalse% |
89 \isacommand{apply}{\isacharparenleft}case{\isacharunderscore}tac\ xs{\isacharparenright}\isamarkuptrue% |
90 {\isacharparenleft}case{\isacharunderscore}tac\ xs{\isacharparenright}% |
90 % |
|
91 \begin{isamarkuptxt}% |
91 \begin{isamarkuptxt}% |
92 \noindent |
92 \noindent |
93 results in the proof state |
93 results in the proof state |
94 \begin{isabelle}% |
94 \begin{isabelle}% |
95 \ {\isadigit{1}}{\isachardot}\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymLongrightarrow}\ {\isacharparenleft}case\ xs\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbar}\ y\ {\isacharhash}\ ys\ {\isasymRightarrow}\ xs{\isacharparenright}\ {\isacharequal}\ xs\isanewline |
95 \ {\isadigit{1}}{\isachardot}\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymLongrightarrow}\ {\isacharparenleft}case\ xs\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbar}\ y\ {\isacharhash}\ ys\ {\isasymRightarrow}\ xs{\isacharparenright}\ {\isacharequal}\ xs\isanewline |
96 \ {\isadigit{2}}{\isachardot}\ {\isasymAnd}a\ list{\isachardot}\isanewline |
96 \ {\isadigit{2}}{\isachardot}\ {\isasymAnd}a\ list{\isachardot}\isanewline |
97 \isaindent{\ {\isadigit{2}}{\isachardot}\ \ \ \ }xs\ {\isacharequal}\ a\ {\isacharhash}\ list\ {\isasymLongrightarrow}\ {\isacharparenleft}case\ xs\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbar}\ y\ {\isacharhash}\ ys\ {\isasymRightarrow}\ xs{\isacharparenright}\ {\isacharequal}\ xs% |
97 \isaindent{\ {\isadigit{2}}{\isachardot}\ \ \ \ }xs\ {\isacharequal}\ a\ {\isacharhash}\ list\ {\isasymLongrightarrow}\ {\isacharparenleft}case\ xs\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbar}\ y\ {\isacharhash}\ ys\ {\isasymRightarrow}\ xs{\isacharparenright}\ {\isacharequal}\ xs% |
98 \end{isabelle} |
98 \end{isabelle} |
99 which is solved automatically:% |
99 which is solved automatically:% |
100 \end{isamarkuptxt}% |
100 \end{isamarkuptxt}% |
101 \isamarkupfalse% |
101 \isamarkuptrue% |
102 \isacommand{apply}{\isacharparenleft}auto{\isacharparenright}% |
102 \isacommand{apply}\isamarkupfalse% |
|
103 {\isacharparenleft}auto{\isacharparenright}\isamarkupfalse% |
|
104 % |
103 \endisatagproof |
105 \endisatagproof |
104 {\isafoldproof}% |
106 {\isafoldproof}% |
105 % |
107 % |
106 \isadelimproof |
108 \isadelimproof |
107 % |
109 % |
108 \endisadelimproof |
110 \endisadelimproof |
109 \isamarkuptrue% |
|
110 % |
111 % |
111 \begin{isamarkuptext}% |
112 \begin{isamarkuptext}% |
112 Note that we do not need to give a lemma a name if we do not intend to refer |
113 Note that we do not need to give a lemma a name if we do not intend to refer |
113 to it explicitly in the future. |
114 to it explicitly in the future. |
114 Other basic laws about a datatype are applied automatically during |
115 Other basic laws about a datatype are applied automatically during |