doc-src/Exercises/2002/a6/generated/a6.tex
author obua
Sun, 09 May 2004 23:04:36 +0200
changeset 14722 8e739a6eaf11
parent 13841 ed4e97874454
permissions -rw-r--r--
replaced apply-style proof for instance Multiset :: plus_ac0 by recommended Isar proof style
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
13841
ed4e97874454 keep a copy of generated files in repository
kleing
parents:
diff changeset
     1
%
ed4e97874454 keep a copy of generated files in repository
kleing
parents:
diff changeset
     2
\begin{isabellebody}%
ed4e97874454 keep a copy of generated files in repository
kleing
parents:
diff changeset
     3
\def\isabellecontext{a{\isadigit{6}}}%
ed4e97874454 keep a copy of generated files in repository
kleing
parents:
diff changeset
     4
\isamarkupfalse%
ed4e97874454 keep a copy of generated files in repository
kleing
parents:
diff changeset
     5
%
ed4e97874454 keep a copy of generated files in repository
kleing
parents:
diff changeset
     6
\isamarkupsubsection{The towers of Hanoi%
ed4e97874454 keep a copy of generated files in repository
kleing
parents:
diff changeset
     7
}
ed4e97874454 keep a copy of generated files in repository
kleing
parents:
diff changeset
     8
\isamarkuptrue%
ed4e97874454 keep a copy of generated files in repository
kleing
parents:
diff changeset
     9
%
ed4e97874454 keep a copy of generated files in repository
kleing
parents:
diff changeset
    10
\begin{isamarkuptext}%
ed4e97874454 keep a copy of generated files in repository
kleing
parents:
diff changeset
    11
In section \ref{psv2000hanoi} we introduced the towers of Hanoi and
ed4e97874454 keep a copy of generated files in repository
kleing
parents:
diff changeset
    12
defined a function \isa{moves} to generate the moves to solve the
ed4e97874454 keep a copy of generated files in repository
kleing
parents:
diff changeset
    13
puzzle.  Now it is time to show that \isa{moves} is correct. This
ed4e97874454 keep a copy of generated files in repository
kleing
parents:
diff changeset
    14
means that
ed4e97874454 keep a copy of generated files in repository
kleing
parents:
diff changeset
    15
\begin{itemize}
ed4e97874454 keep a copy of generated files in repository
kleing
parents:
diff changeset
    16
\item when executing the list of moves, the result is indeed the
ed4e97874454 keep a copy of generated files in repository
kleing
parents:
diff changeset
    17
intended one, i.e.\ all disks are moved from one peg to another, and
ed4e97874454 keep a copy of generated files in repository
kleing
parents:
diff changeset
    18
\item all of the moves are legal, i.e.\ never place a larger disk
ed4e97874454 keep a copy of generated files in repository
kleing
parents:
diff changeset
    19
on top of a smaller one.
ed4e97874454 keep a copy of generated files in repository
kleing
parents:
diff changeset
    20
\end{itemize}
ed4e97874454 keep a copy of generated files in repository
kleing
parents:
diff changeset
    21
Hint: this is a nontrivial undertaking. The complexity of your proofs
ed4e97874454 keep a copy of generated files in repository
kleing
parents:
diff changeset
    22
will depend crucially on your choice of model and you may have to
ed4e97874454 keep a copy of generated files in repository
kleing
parents:
diff changeset
    23
revise your model as you proceed with the proof.%
ed4e97874454 keep a copy of generated files in repository
kleing
parents:
diff changeset
    24
\end{isamarkuptext}%
ed4e97874454 keep a copy of generated files in repository
kleing
parents:
diff changeset
    25
\isamarkuptrue%
ed4e97874454 keep a copy of generated files in repository
kleing
parents:
diff changeset
    26
\isamarkupfalse%
ed4e97874454 keep a copy of generated files in repository
kleing
parents:
diff changeset
    27
\end{isabellebody}%
ed4e97874454 keep a copy of generated files in repository
kleing
parents:
diff changeset
    28
%%% Local Variables:
ed4e97874454 keep a copy of generated files in repository
kleing
parents:
diff changeset
    29
%%% mode: latex
ed4e97874454 keep a copy of generated files in repository
kleing
parents:
diff changeset
    30
%%% TeX-master: "root"
ed4e97874454 keep a copy of generated files in repository
kleing
parents:
diff changeset
    31
%%% End: