151 \end{itemize} |
151 \end{itemize} |
152 The name and the simplification attribute are optional. |
152 The name and the simplification attribute are optional. |
153 Isabelle's response is to print the initial proof state consisting |
153 Isabelle's response is to print the initial proof state consisting |
154 of some header information (like how many subgoals there are) followed by |
154 of some header information (like how many subgoals there are) followed by |
155 \begin{isabelle}% |
155 \begin{isabelle}% |
156 rev\ {\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs\isanewline |
|
157 \ {\isadigit{1}}{\isachardot}\ rev\ {\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs% |
156 \ {\isadigit{1}}{\isachardot}\ rev\ {\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs% |
158 \end{isabelle} |
157 \end{isabelle} |
159 For compactness reasons we omit the header in this tutorial. |
158 For compactness reasons we omit the header in this tutorial. |
160 Until we have finished a proof, the \rmindex{proof state} proper |
159 Until we have finished a proof, the \rmindex{proof state} proper |
161 always looks like this: |
160 always looks like this: |
162 \begin{isabelle} |
161 \begin{isabelle} |
163 $G$\isanewline |
|
164 ~1.~$G\sb{1}$\isanewline |
162 ~1.~$G\sb{1}$\isanewline |
165 ~~\vdots~~\isanewline |
163 ~~\vdots~~\isanewline |
166 ~$n$.~$G\sb{n}$ |
164 ~$n$.~$G\sb{n}$ |
167 \end{isabelle} |
165 \end{isabelle} |
168 where $G$ |
166 The numbered lines contain the subgoals $G\sb{1}$, \dots, $G\sb{n}$ |
169 is the overall goal that we are trying to prove, and the numbered lines |
167 that we need to prove to establish the main goal.\index{subgoals} |
170 contain the subgoals $G\sb{1}$, \dots, $G\sb{n}$ that we need to prove to |
168 Initially there is only one subgoal, which is identical with the |
171 establish $G$.\index{subgoals} |
169 main goal. (If you always want to see the main goal as well, |
172 Initially there is only one subgoal, which is |
170 set the flag \isa{Proof.show_main_goal}\index{*show_main_goal (flag)} |
173 identical with the overall goal. Normally $G$ is constant and only serves as |
171 --- this flag used to be set by default.) |
174 a reminder. Hence we rarely show it in this tutorial. |
|
175 |
172 |
176 Let us now get back to \isa{rev\ {\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs}. Properties of recursively |
173 Let us now get back to \isa{rev\ {\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs}. Properties of recursively |
177 defined functions are best established by induction. In this case there is |
174 defined functions are best established by induction. In this case there is |
178 nothing obvious except induction on \isa{xs}:% |
175 nothing obvious except induction on \isa{xs}:% |
179 \end{isamarkuptxt}% |
176 \end{isamarkuptxt}% |