doc-src/Exercises/2000/a1/Hanoi.thy

Removed ~10000 hack in function idx that can lead to inconsistencies
when unifying terms with a large number of abstractions.

(*<*)
theory Hanoi = Main:
(*>*)
subsection {* The towers of Hanoi \label{psv2000hanoi} *}

text {*

We are given 3 pegs $A$, $B$ and $C$, and $n$ disks with a hole, such
that no two disks have the same diameter.  Initially all $n$ disks
rest on peg $A$, ordered according to their size, with the largest one
at the bottom. The aim is to transfer all $n$ disks from $A$ to $C$ by
a sequence of single-disk moves such that we never place a larger disk
on top of a smaller one. Peg $B$ may be used for intermediate storage.

\begin{center}
\includegraphics[width=0.8\textwidth]{Hanoi}
\end{center}

\medskip The pegs and moves can be modelled as follows:
*};  

datatype peg = A | B | C
types move = "peg * peg"

text {*
Define a primitive recursive function
*};

consts
  moves :: "nat => peg => peg => peg => move list";

text {* such that @{term moves}$~n~a~b~c$ returns a list of (legal)
moves that transfer $n$ disks from peg $a$ via $b$ to $c$.
Show that this requires $2^n - 1$ moves:
*}

theorem "length (moves n a b c) = 2^n - 1"
(*<*)oops(*>*)

text {* Hint: You need to strengthen the theorem for the
induction to go through. Beware: subtraction on natural numbers
behaves oddly: $n - m = 0$ if $n \le m$. *}

(*<*)
end
(*>*)