equal
deleted
inserted
replaced
65 by \methdx{case_tac}. Here is a trivial example:% |
65 by \methdx{case_tac}. Here is a trivial example:% |
66 \end{isamarkuptext}% |
66 \end{isamarkuptext}% |
67 \isamarkuptrue% |
67 \isamarkuptrue% |
68 \isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}case\ xs\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbar}\ y{\isacharhash}ys\ {\isasymRightarrow}\ xs{\isacharparenright}\ {\isacharequal}\ xs{\isachardoublequote}\isanewline |
68 \isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}case\ xs\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbar}\ y{\isacharhash}ys\ {\isasymRightarrow}\ xs{\isacharparenright}\ {\isacharequal}\ xs{\isachardoublequote}\isanewline |
69 \isamarkupfalse% |
69 \isamarkupfalse% |
70 \isacommand{apply}{\isacharparenleft}case{\isacharunderscore}tac\ xs{\isacharparenright}\isamarkupfalse% |
70 \isamarkupfalse% |
71 % |
|
72 \begin{isamarkuptxt}% |
|
73 \noindent |
|
74 results in the proof state |
|
75 \begin{isabelle}% |
|
76 \ {\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 |
|
77 \ {\isadigit{2}}{\isachardot}\ {\isasymAnd}a\ list{\isachardot}\isanewline |
|
78 \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% |
|
79 \end{isabelle} |
|
80 which is solved automatically:% |
|
81 \end{isamarkuptxt}% |
|
82 \isamarkuptrue% |
71 \isamarkuptrue% |
83 \isacommand{apply}{\isacharparenleft}auto{\isacharparenright}\isamarkupfalse% |
72 \isamarkupfalse% |
84 \isamarkupfalse% |
73 \isamarkupfalse% |
85 % |
74 % |
86 \begin{isamarkuptext}% |
75 \begin{isamarkuptext}% |
87 Note that we do not need to give a lemma a name if we do not intend to refer |
76 Note that we do not need to give a lemma a name if we do not intend to refer |
88 to it explicitly in the future. |
77 to it explicitly in the future. |