summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | paulson |

Thu, 08 May 2003 12:51:55 +0200 | |

changeset 13978 | a241cdd9c1c9 |

parent 13977 | eb5fe146a4e0 |

child 13979 | 4c3a638828b9 |

auto update

--- a/doc-src/TutorialI/ToyList/document/ToyList.tex Thu May 08 12:50:27 2003 +0200 +++ b/doc-src/TutorialI/ToyList/document/ToyList.tex Thu May 08 12:51:55 2003 +0200 @@ -153,25 +153,22 @@ Isabelle's response is to print the initial proof state consisting of some header information (like how many subgoals there are) followed by \begin{isabelle}% -rev\ {\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs\isanewline \ {\isadigit{1}}{\isachardot}\ rev\ {\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs% \end{isabelle} For compactness reasons we omit the header in this tutorial. Until we have finished a proof, the \rmindex{proof state} proper always looks like this: \begin{isabelle} -$G$\isanewline ~1.~$G\sb{1}$\isanewline ~~\vdots~~\isanewline ~$n$.~$G\sb{n}$ \end{isabelle} -where $G$ -is the overall goal that we are trying to prove, and the numbered lines -contain the subgoals $G\sb{1}$, \dots, $G\sb{n}$ that we need to prove to -establish $G$.\index{subgoals} -Initially there is only one subgoal, which is -identical with the overall goal. Normally $G$ is constant and only serves as -a reminder. Hence we rarely show it in this tutorial. +The numbered lines contain the subgoals $G\sb{1}$, \dots, $G\sb{n}$ +that we need to prove to establish the main goal.\index{subgoals} +Initially there is only one subgoal, which is identical with the +main goal. (If you always want to see the main goal as well, +set the flag \isa{Proof.show_main_goal}\index{*show_main_goal (flag)} +--- this flag used to be set by default.) Let us now get back to \isa{rev\ {\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs}. Properties of recursively defined functions are best established by induction. In this case there is