# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1250635780 -7200
# Node ID 05cbe2430b76692dba52857430061190e94c3a27
# Parent  ee864694315ba54d46d4a22de31398bc9c87f074
added exercise

diff -r ee864694315b -r 05cbe2430b76 ProgTutorial/FirstSteps.thy
--- a/ProgTutorial/FirstSteps.thy	Tue Aug 18 01:05:56 2009 +0200
+++ b/ProgTutorial/FirstSteps.thy	Wed Aug 19 00:49:40 2009 +0200
@@ -1167,6 +1167,31 @@
   in @{ML_file "HOL/Tools/hologic.ML"}.
   \end{readmore}
 
+  \begin{exercise}\label{ex:debruijn}
+  Implement the function,\footnote{Personal communication of
+  de Bruijn to Dyckhoff.} called deBruijn n, that constructs terms of the form:
+  
+  \begin{center}
+  \begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
+  {\it rhs n} & $\dn$ & $\bigwedge${\it i=1\ldots n.  P\,i}\\
+  {\it lhs n} & $\dn$ & $\bigwedge${\it i=1\ldots n. P\,i = P (i + 1 mod n)}
+                        $\longrightarrow$ {\it rhs n}\\
+  {\it deBruijn n} & $\dn$ & {\it lhs n} $\longrightarrow$ {\it rhs n}\\
+  \end{tabular}
+  \end{center}
+
+  For n=3 this function returns the term
+
+  \begin{center}
+  \begin{tabular}{l}
+  (P 2 = P 3 $\longrightarrow$ P 3 $\wedge$ P 2 $\wedge$ P 1) $\wedge$\\
+  (P 1 = P 2 $\longrightarrow$ P 3 $\wedge$ P 2 $\wedge$ P 1) $\wedge$\\ 
+  (P 1 = P 3 $\longrightarrow$ P 3 $\wedge$ P 2 $\wedge$ P 1) $\longrightarrow$ P 3 $\wedge$ P 2 $\wedge$ P 1
+  \end{tabular}
+  \end{center}
+
+  \end{exercise}
+
   When constructing terms manually, there are a few subtle issues with
   constants. They usually crop up when pattern matching terms or types, or
   when constructing them. While it is perfectly ok to write the function
diff -r ee864694315b -r 05cbe2430b76 ProgTutorial/Solutions.thy
--- a/ProgTutorial/Solutions.thy	Tue Aug 18 01:05:56 2009 +0200
+++ b/ProgTutorial/Solutions.thy	Wed Aug 19 00:49:40 2009 +0200
@@ -4,6 +4,20 @@
 
 chapter {* Solutions to Most Exercises\label{ch:solutions} *}
 
+text {* \solution{ex:debruijn} *}
+
+ML{*fun P n = @{term "P::nat \<Rightarrow> bool"} $ (HOLogic.mk_number @{typ "nat"} n) 
+
+fun rhs 1 = P 1
+  | rhs n = HOLogic.mk_conj (P n, rhs (n - 1))
+
+fun lhs 1 n = HOLogic.mk_imp (HOLogic.mk_eq (P 1, P n), rhs n)
+  | lhs m n = HOLogic.mk_conj (HOLogic.mk_imp 
+                 (HOLogic.mk_eq (P (m - 1), P m), rhs n), lhs (m - 1) n)
+
+fun de_bruijn n =
+  HOLogic.mk_Trueprop (HOLogic.mk_imp (lhs n n, rhs n))*}
+
 text {* \solution{fun:revsum} *}
 
 ML{*fun rev_sum ((p as Const (@{const_name plus}, _)) $ t $ u) = 
diff -r ee864694315b -r 05cbe2430b76 ProgTutorial/document/root.tex
--- a/ProgTutorial/document/root.tex	Tue Aug 18 01:05:56 2009 +0200
+++ b/ProgTutorial/document/root.tex	Wed Aug 19 00:49:40 2009 +0200
@@ -69,9 +69,11 @@
 \MakeFramed {\advance\hsize-\width \FrameRestore}}%
 {\endMakeFramed}
 
-
 \newenvironment{readmore}%
 {\begin{leftrightbar}\small\it{\textbf{Read More}}\\}{\end{leftrightbar}}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% some mathematical notation
+\newcommand{\dn}{\stackrel{\mbox{\scriptsize def}}{=}}
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 % this is to draw a gray box around code
diff -r ee864694315b -r 05cbe2430b76 progtutorial.pdf
Binary file progtutorial.pdf has changed