doc-src/TutorialI/ToyList/ToyList.thy
author nipkow
Tue Mar 18 17:54:27 2003 +0100 (2003-03-18)
changeset 13868 01b516b64233
parent 13191 05a9929ee10e
child 15136 1275417e3930
permissions -rw-r--r--
*** empty log message ***
     1 theory ToyList = PreList:
     2 
     3 text{*\noindent
     4 HOL already has a predefined theory of lists called @{text"List"} ---
     5 @{text"ToyList"} is merely a small fragment of it chosen as an example. In
     6 contrast to what is recommended in \S\ref{sec:Basic:Theories},
     7 @{text"ToyList"} is not based on @{text"Main"} but on @{text"PreList"}, a
     8 theory that contains pretty much everything but lists, thus avoiding
     9 ambiguities caused by defining lists twice.
    10 *}
    11 
    12 datatype 'a list = Nil                          ("[]")
    13                  | Cons 'a "'a list"            (infixr "#" 65);
    14 
    15 text{*\noindent
    16 The datatype\index{datatype@\isacommand {datatype} (command)}
    17 \tydx{list} introduces two
    18 constructors \cdx{Nil} and \cdx{Cons}, the
    19 empty~list and the operator that adds an element to the front of a list. For
    20 example, the term \isa{Cons True (Cons False Nil)} is a value of
    21 type @{typ"bool list"}, namely the list with the elements @{term"True"} and
    22 @{term"False"}. Because this notation quickly becomes unwieldy, the
    23 datatype declaration is annotated with an alternative syntax: instead of
    24 @{term[source]Nil} and \isa{Cons x xs} we can write
    25 @{term"[]"}\index{$HOL2list@\texttt{[]}|bold} and
    26 @{term"x # xs"}\index{$HOL2list@\texttt{\#}|bold}. In fact, this
    27 alternative syntax is the familiar one.  Thus the list \isa{Cons True
    28 (Cons False Nil)} becomes @{term"True # False # []"}. The annotation
    29 \isacommand{infixr}\index{infixr@\isacommand{infixr} (annotation)} 
    30 means that @{text"#"} associates to
    31 the right: the term @{term"x # y # z"} is read as @{text"x # (y # z)"}
    32 and not as @{text"(x # y) # z"}.
    33 The @{text 65} is the priority of the infix @{text"#"}.
    34 
    35 \begin{warn}
    36   Syntax annotations can be powerful, but they are difficult to master and 
    37   are never necessary.  You
    38   could drop them from theory @{text"ToyList"} and go back to the identifiers
    39   @{term[source]Nil} and @{term[source]Cons}.
    40   Novices should avoid using
    41   syntax annotations in their own theories.
    42 \end{warn}
    43 Next, two functions @{text"app"} and \cdx{rev} are declared:
    44 *}
    45 
    46 consts app :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"   (infixr "@" 65)
    47        rev :: "'a list \<Rightarrow> 'a list";
    48 
    49 text{*
    50 \noindent
    51 In contrast to many functional programming languages,
    52 Isabelle insists on explicit declarations of all functions
    53 (keyword \commdx{consts}).  Apart from the declaration-before-use
    54 restriction, the order of items in a theory file is unconstrained. Function
    55 @{text"app"} is annotated with concrete syntax too. Instead of the
    56 prefix syntax @{text"app xs ys"} the infix
    57 @{term"xs @ ys"}\index{$HOL2list@\texttt{\at}|bold} becomes the preferred
    58 form. Both functions are defined recursively:
    59 *}
    60 
    61 primrec
    62 "[] @ ys       = ys"
    63 "(x # xs) @ ys = x # (xs @ ys)";
    64 
    65 primrec
    66 "rev []        = []"
    67 "rev (x # xs)  = (rev xs) @ (x # [])";
    68 
    69 text{*
    70 \noindent\index{*rev (constant)|(}\index{append function|(}
    71 The equations for @{text"app"} and @{term"rev"} hardly need comments:
    72 @{text"app"} appends two lists and @{term"rev"} reverses a list.  The
    73 keyword \commdx{primrec} indicates that the recursion is
    74 of a particularly primitive kind where each recursive call peels off a datatype
    75 constructor from one of the arguments.  Thus the
    76 recursion always terminates, i.e.\ the function is \textbf{total}.
    77 \index{functions!total}
    78 
    79 The termination requirement is absolutely essential in HOL, a logic of total
    80 functions. If we were to drop it, inconsistencies would quickly arise: the
    81 ``definition'' $f(n) = f(n)+1$ immediately leads to $0 = 1$ by subtracting
    82 $f(n)$ on both sides.
    83 % However, this is a subtle issue that we cannot discuss here further.
    84 
    85 \begin{warn}
    86   As we have indicated, the requirement for total functions is an essential characteristic of HOL\@. It is only
    87   because of totality that reasoning in HOL is comparatively easy.  More
    88   generally, the philosophy in HOL is to refrain from asserting arbitrary axioms (such as
    89   function definitions whose totality has not been proved) because they
    90   quickly lead to inconsistencies. Instead, fixed constructs for introducing
    91   types and functions are offered (such as \isacommand{datatype} and
    92   \isacommand{primrec}) which are guaranteed to preserve consistency.
    93 \end{warn}
    94 
    95 \index{syntax}%
    96 A remark about syntax.  The textual definition of a theory follows a fixed
    97 syntax with keywords like \isacommand{datatype} and \isacommand{end}.
    98 % (see Fig.~\ref{fig:keywords} in Appendix~\ref{sec:Appendix} for a full list).
    99 Embedded in this syntax are the types and formulae of HOL, whose syntax is
   100 extensible (see \S\ref{sec:concrete-syntax}), e.g.\ by new user-defined infix operators.
   101 To distinguish the two levels, everything
   102 HOL-specific (terms and types) should be enclosed in
   103 \texttt{"}\dots\texttt{"}. 
   104 To lessen this burden, quotation marks around a single identifier can be
   105 dropped, unless the identifier happens to be a keyword, as in
   106 *}
   107 
   108 consts "end" :: "'a list \<Rightarrow> 'a"
   109 
   110 text{*\noindent
   111 When Isabelle prints a syntax error message, it refers to the HOL syntax as
   112 the \textbf{inner syntax} and the enclosing theory language as the \textbf{outer syntax}.
   113 
   114 
   115 \section{An Introductory Proof}
   116 \label{sec:intro-proof}
   117 
   118 Assuming you have input the declarations and definitions of \texttt{ToyList}
   119 presented so far, we are ready to prove a few simple theorems. This will
   120 illustrate not just the basic proof commands but also the typical proof
   121 process.
   122 
   123 \subsubsection*{Main Goal.}
   124 
   125 Our goal is to show that reversing a list twice produces the original
   126 list.
   127 *}
   128 
   129 theorem rev_rev [simp]: "rev(rev xs) = xs";
   130 
   131 txt{*\index{theorem@\isacommand {theorem} (command)|bold}%
   132 \noindent
   133 This \isacommand{theorem} command does several things:
   134 \begin{itemize}
   135 \item
   136 It establishes a new theorem to be proved, namely @{prop"rev(rev xs) = xs"}.
   137 \item
   138 It gives that theorem the name @{text"rev_rev"}, for later reference.
   139 \item
   140 It tells Isabelle (via the bracketed attribute \attrdx{simp}) to take the eventual theorem as a simplification rule: future proofs involving
   141 simplification will replace occurrences of @{term"rev(rev xs)"} by
   142 @{term"xs"}.
   143 \end{itemize}
   144 The name and the simplification attribute are optional.
   145 Isabelle's response is to print the initial proof state consisting
   146 of some header information (like how many subgoals there are) followed by
   147 @{subgoals[display,indent=0]}
   148 For compactness reasons we omit the header in this tutorial.
   149 Until we have finished a proof, the \rmindex{proof state} proper
   150 always looks like this:
   151 \begin{isabelle}
   152 ~1.~$G\sb{1}$\isanewline
   153 ~~\vdots~~\isanewline
   154 ~$n$.~$G\sb{n}$
   155 \end{isabelle}
   156 The numbered lines contain the subgoals $G\sb{1}$, \dots, $G\sb{n}$
   157 that we need to prove to establish the main goal.\index{subgoals}
   158 Initially there is only one subgoal, which is identical with the
   159 main goal. (If you always want to see the main goal as well,
   160 set the flag \isa{Proof.show_main_goal}\index{*show_main_goal (flag)}
   161 --- this flag used to be set by default.)
   162 
   163 Let us now get back to @{prop"rev(rev xs) = xs"}. Properties of recursively
   164 defined functions are best established by induction. In this case there is
   165 nothing obvious except induction on @{term"xs"}:
   166 *}
   167 
   168 apply(induct_tac xs);
   169 
   170 txt{*\noindent\index{*induct_tac (method)}%
   171 This tells Isabelle to perform induction on variable @{term"xs"}. The suffix
   172 @{term"tac"} stands for \textbf{tactic},\index{tactics}
   173 a synonym for ``theorem proving function''.
   174 By default, induction acts on the first subgoal. The new proof state contains
   175 two subgoals, namely the base case (@{term[source]Nil}) and the induction step
   176 (@{term[source]Cons}):
   177 @{subgoals[display,indent=0,margin=65]}
   178 
   179 The induction step is an example of the general format of a subgoal:\index{subgoals}
   180 \begin{isabelle}
   181 ~$i$.~{\isasymAnd}$x\sb{1}$~\dots$x\sb{n}$.~{\it assumptions}~{\isasymLongrightarrow}~{\it conclusion}
   182 \end{isabelle}\index{$IsaAnd@\isasymAnd|bold}
   183 The prefix of bound variables \isasymAnd$x\sb{1}$~\dots~$x\sb{n}$ can be
   184 ignored most of the time, or simply treated as a list of variables local to
   185 this subgoal. Their deeper significance is explained in Chapter~\ref{chap:rules}.
   186 The {\it assumptions}\index{assumptions!of subgoal}
   187 are the local assumptions for this subgoal and {\it
   188   conclusion}\index{conclusion!of subgoal} is the actual proposition to be proved. 
   189 Typical proof steps
   190 that add new assumptions are induction and case distinction. In our example
   191 the only assumption is the induction hypothesis @{term"rev (rev list) =
   192   list"}, where @{term"list"} is a variable name chosen by Isabelle. If there
   193 are multiple assumptions, they are enclosed in the bracket pair
   194 \indexboldpos{\isasymlbrakk}{$Isabrl} and
   195 \indexboldpos{\isasymrbrakk}{$Isabrr} and separated by semicolons.
   196 
   197 Let us try to solve both goals automatically:
   198 *}
   199 
   200 apply(auto);
   201 
   202 txt{*\noindent
   203 This command tells Isabelle to apply a proof strategy called
   204 @{text"auto"} to all subgoals. Essentially, @{text"auto"} tries to
   205 simplify the subgoals.  In our case, subgoal~1 is solved completely (thanks
   206 to the equation @{prop"rev [] = []"}) and disappears; the simplified version
   207 of subgoal~2 becomes the new subgoal~1:
   208 @{subgoals[display,indent=0,margin=70]}
   209 In order to simplify this subgoal further, a lemma suggests itself.
   210 *}
   211 (*<*)
   212 oops
   213 (*>*)
   214 
   215 subsubsection{*First Lemma*}
   216 
   217 text{*
   218 \indexbold{abandoning a proof}\indexbold{proofs!abandoning}
   219 After abandoning the above proof attempt (at the shell level type
   220 \commdx{oops}) we start a new proof:
   221 *}
   222 
   223 lemma rev_app [simp]: "rev(xs @ ys) = (rev ys) @ (rev xs)";
   224 
   225 txt{*\noindent The keywords \commdx{theorem} and
   226 \commdx{lemma} are interchangeable and merely indicate
   227 the importance we attach to a proposition.  Therefore we use the words
   228 \emph{theorem} and \emph{lemma} pretty much interchangeably, too.
   229 
   230 There are two variables that we could induct on: @{term"xs"} and
   231 @{term"ys"}. Because @{text"@"} is defined by recursion on
   232 the first argument, @{term"xs"} is the correct one:
   233 *}
   234 
   235 apply(induct_tac xs);
   236 
   237 txt{*\noindent
   238 This time not even the base case is solved automatically:
   239 *}
   240 
   241 apply(auto);
   242 
   243 txt{*
   244 @{subgoals[display,indent=0,goals_limit=1]}
   245 Again, we need to abandon this proof attempt and prove another simple lemma
   246 first. In the future the step of abandoning an incomplete proof before
   247 embarking on the proof of a lemma usually remains implicit.
   248 *}
   249 (*<*)
   250 oops
   251 (*>*)
   252 
   253 subsubsection{*Second Lemma*}
   254 
   255 text{*
   256 We again try the canonical proof procedure:
   257 *}
   258 
   259 lemma app_Nil2 [simp]: "xs @ [] = xs";
   260 apply(induct_tac xs);
   261 apply(auto);
   262 
   263 txt{*
   264 \noindent
   265 It works, yielding the desired message @{text"No subgoals!"}:
   266 @{goals[display,indent=0]}
   267 We still need to confirm that the proof is now finished:
   268 *}
   269 
   270 done
   271 
   272 text{*\noindent
   273 As a result of that final \commdx{done}, Isabelle associates the lemma just proved
   274 with its name. In this tutorial, we sometimes omit to show that final \isacommand{done}
   275 if it is obvious from the context that the proof is finished.
   276 
   277 % Instead of \isacommand{apply} followed by a dot, you can simply write
   278 % \isacommand{by}\indexbold{by}, which we do most of the time.
   279 Notice that in lemma @{thm[source]app_Nil2},
   280 as printed out after the final \isacommand{done}, the free variable @{term"xs"} has been
   281 replaced by the unknown @{text"?xs"}, just as explained in
   282 \S\ref{sec:variables}.
   283 
   284 Going back to the proof of the first lemma
   285 *}
   286 
   287 lemma rev_app [simp]: "rev(xs @ ys) = (rev ys) @ (rev xs)";
   288 apply(induct_tac xs);
   289 apply(auto);
   290 
   291 txt{*
   292 \noindent
   293 we find that this time @{text"auto"} solves the base case, but the
   294 induction step merely simplifies to
   295 @{subgoals[display,indent=0,goals_limit=1]}
   296 Now we need to remember that @{text"@"} associates to the right, and that
   297 @{text"#"} and @{text"@"} have the same priority (namely the @{text"65"}
   298 in their \isacommand{infixr} annotation). Thus the conclusion really is
   299 \begin{isabelle}
   300 ~~~~~(rev~ys~@~rev~list)~@~(a~\#~[])~=~rev~ys~@~(rev~list~@~(a~\#~[]))
   301 \end{isabelle}
   302 and the missing lemma is associativity of @{text"@"}.
   303 *}
   304 (*<*)oops(*>*)
   305 
   306 subsubsection{*Third Lemma*}
   307 
   308 text{*
   309 Abandoning the previous attempt, the canonical proof procedure
   310 succeeds without further ado.
   311 *}
   312 
   313 lemma app_assoc [simp]: "(xs @ ys) @ zs = xs @ (ys @ zs)";
   314 apply(induct_tac xs);
   315 apply(auto);
   316 done
   317 
   318 text{*
   319 \noindent
   320 Now we can prove the first lemma:
   321 *}
   322 
   323 lemma rev_app [simp]: "rev(xs @ ys) = (rev ys) @ (rev xs)";
   324 apply(induct_tac xs);
   325 apply(auto);
   326 done
   327 
   328 text{*\noindent
   329 Finally, we prove our main theorem:
   330 *}
   331 
   332 theorem rev_rev [simp]: "rev(rev xs) = xs";
   333 apply(induct_tac xs);
   334 apply(auto);
   335 done
   336 
   337 text{*\noindent
   338 The final \commdx{end} tells Isabelle to close the current theory because
   339 we are finished with its development:%
   340 \index{*rev (constant)|)}\index{append function|)}
   341 *}
   342 
   343 end