updated and simplified HOL datatype examples (NB: special treatment of distinctness has been discontinued in the vicinity of 542b34b178ec);

--- a/doc-src/HOL/HOL.tex	Thu May 26 13:37:11 2011 +0200
+++ b/doc-src/HOL/HOL.tex	Thu May 26 14:12:14 2011 +0200
@@ -1938,103 +1938,6 @@
 and \texttt{simps} are contained in a separate structure named $t@1_\ldots_t@n$.
 
 
-\subsection{Examples}
-
-\subsubsection{The datatype $\alpha~mylist$}
-
-We want to define a type $\alpha~mylist$. To do this we have to build a new
-theory that contains the type definition.  We start from the theory
-\texttt{Datatype} instead of \texttt{Main} in order to avoid clashes with the
-\texttt{List} theory of Isabelle/HOL.
-\begin{ttbox}
-MyList = Datatype +
-  datatype 'a mylist = Nil | Cons 'a ('a mylist)
-end
-\end{ttbox}
-After loading the theory, we can prove $Cons~x~xs\neq xs$, for example.  To
-ease the induction applied below, we state the goal with $x$ quantified at the
-object-level.  This will be stripped later using \ttindex{qed_spec_mp}.
-\begin{ttbox}
-Goal "!x. Cons x xs ~= xs";
-{\out Level 0}
-{\out ! x. Cons x xs ~= xs}
-{\out  1. ! x. Cons x xs ~= xs}
-\end{ttbox}
-This can be proved by the structural induction tactic:
-\begin{ttbox}
-by (induct_tac "xs" 1);
-{\out Level 1}
-{\out ! x. Cons x xs ~= xs}
-{\out  1. ! x. Cons x Nil ~= Nil}
-{\out  2. !!a mylist.}
-{\out        ! x. Cons x mylist ~= mylist ==>}
-{\out        ! x. Cons x (Cons a mylist) ~= Cons a mylist}
-\end{ttbox}
-The first subgoal can be proved using the simplifier.  Isabelle/HOL has
-already added the freeness properties of lists to the default simplification
-set.
-\begin{ttbox}
-by (Simp_tac 1);
-{\out Level 2}
-{\out ! x. Cons x xs ~= xs}
-{\out  1. !!a mylist.}
-{\out        ! x. Cons x mylist ~= mylist ==>}
-{\out        ! x. Cons x (Cons a mylist) ~= Cons a mylist}
-\end{ttbox}
-Similarly, we prove the remaining goal.
-\begin{ttbox}
-by (Asm_simp_tac 1);
-{\out Level 3}
-{\out ! x. Cons x xs ~= xs}
-{\out No subgoals!}
-\ttbreak
-qed_spec_mp "not_Cons_self";
-{\out val not_Cons_self = "Cons x xs ~= xs" : thm}
-\end{ttbox}
-Because both subgoals could have been proved by \texttt{Asm_simp_tac}
-we could have done that in one step:
-\begin{ttbox}
-by (ALLGOALS Asm_simp_tac);
-\end{ttbox}
-
-
-\subsubsection{The datatype $\alpha~mylist$ with mixfix syntax}
-
-In this example we define the type $\alpha~mylist$ again but this time
-we want to write \texttt{[]} for \texttt{Nil} and we want to use infix
-notation \verb|#| for \texttt{Cons}.  To do this we simply add mixfix
-annotations after the constructor declarations as follows:
-\begin{ttbox}
-MyList = Datatype +
-  datatype 'a mylist =
-    Nil ("[]")  |
-    Cons 'a ('a mylist)  (infixr "#" 70)
-end
-\end{ttbox}
-Now the theorem in the previous example can be written \verb|x#xs ~= xs|.
-
-
-\subsubsection{A datatype for weekdays}
-
-This example shows a datatype that consists of 7 constructors:
-\begin{ttbox}
-Days = Main +
-  datatype days = Mon | Tue | Wed | Thu | Fri | Sat | Sun
-end
-\end{ttbox}
-Because there are more than 6 constructors, inequality is expressed via a function
-\verb|days_ord|.  The theorem \verb|Mon ~= Tue| is not directly
-contained among the distinctness theorems, but the simplifier can
-prove it thanks to rewrite rules inherited from theory \texttt{NatArith}:
-\begin{ttbox}
-Goal "Mon ~= Tue";
-by (Simp_tac 1);
-\end{ttbox}
-You need not derive such inequalities explicitly: the simplifier will dispose
-of them automatically.
-\index{*datatype|)}
-
-
 \section{Recursive function definitions}\label{sec:HOL:recursive}
 \index{recursive functions|see{recursion}}
 

--- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Thu May 26 13:37:11 2011 +0200
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Thu May 26 14:12:14 2011 +0200
@@ -489,6 +489,37 @@
 *}
 
 
+subsubsection {* Examples *}
+
+text {* We define a type of finite sequences, with slightly different
+  names than the existing @{typ "'a list"} that is already in @{theory
+  Main}: *}
+
+datatype 'a seq = Empty | Seq 'a "'a seq"
+
+text {* We can now prove some simple lemma by structural induction: *}
+
+lemma "Seq x xs \<noteq> xs"
+proof (induct xs arbitrary: x)
+  case Empty
+  txt {* This case can be proved using the simplifier: the freeness
+    properties of the datatype are already declared as @{attribute
+    simp} rules. *}
+  show "Seq x Empty \<noteq> Empty"
+    by simp
+next
+  case (Seq y ys)
+  txt {* The step case is proved similarly. *}
+  show "Seq x (Seq y ys) \<noteq> Seq y ys"
+    using `Seq y ys \<noteq> ys` by simp
+qed
+
+text {* Here is a more succinct version of the same proof: *}
+
+lemma "Seq x xs \<noteq> xs"
+  by (induct xs arbitrary: x) simp_all
+
+
 section {* Records \label{sec:hol-record} *}
 
 text {*

--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Thu May 26 13:37:11 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Thu May 26 14:12:14 2011 +0200
@@ -758,6 +758,85 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
+\isamarkupsubsubsection{Examples%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+We define a type of finite sequences, with slightly different
+  names than the existing \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{27}{\isacharprime}}a\ list{\isaliteral{22}{\isachardoublequote}}} that is already in \hyperlink{theory.Main}{\mbox{\isa{Main}}}:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{datatype}\isamarkupfalse%
+\ {\isaliteral{27}{\isacharprime}}a\ seq\ {\isaliteral{3D}{\isacharequal}}\ Empty\ {\isaliteral{7C}{\isacharbar}}\ Seq\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ seq{\isaliteral{22}{\isachardoublequoteclose}}%
+\begin{isamarkuptext}%
+We can now prove some simple lemma by structural induction:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}Seq\ x\ xs\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ xs{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+\isacommand{proof}\isamarkupfalse%
+\ {\isaliteral{28}{\isacharparenleft}}induct\ xs\ arbitrary{\isaliteral{3A}{\isacharcolon}}\ x{\isaliteral{29}{\isacharparenright}}\isanewline
+\ \ \isacommand{case}\isamarkupfalse%
+\ Empty%
+\begin{isamarkuptxt}%
+This case can be proved using the simplifier: the freeness
+    properties of the datatype are already declared as \hyperlink{attribute.simp}{\mbox{\isa{simp}}} rules.%
+\end{isamarkuptxt}%
+\isamarkuptrue%
+\ \ \isacommand{show}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}Seq\ x\ Empty\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ Empty{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+\ \ \ \ \isacommand{by}\isamarkupfalse%
+\ simp\isanewline
+\isacommand{next}\isamarkupfalse%
+\isanewline
+\ \ \isacommand{case}\isamarkupfalse%
+\ {\isaliteral{28}{\isacharparenleft}}Seq\ y\ ys{\isaliteral{29}{\isacharparenright}}%
+\begin{isamarkuptxt}%
+The step case is proved similarly.%
+\end{isamarkuptxt}%
+\isamarkuptrue%
+\ \ \isacommand{show}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}Seq\ x\ {\isaliteral{28}{\isacharparenleft}}Seq\ y\ ys{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ Seq\ y\ ys{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+\ \ \ \ \isacommand{using}\isamarkupfalse%
+\ {\isaliteral{60}{\isacharbackquoteopen}}Seq\ y\ ys\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ ys{\isaliteral{60}{\isacharbackquoteclose}}\ \isacommand{by}\isamarkupfalse%
+\ simp\isanewline
+\isacommand{qed}\isamarkupfalse%
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\begin{isamarkuptext}%
+Here is a more succinct version of the same proof:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}Seq\ x\ xs\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ xs{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{by}\isamarkupfalse%
+\ {\isaliteral{28}{\isacharparenleft}}induct\ xs\ arbitrary{\isaliteral{3A}{\isacharcolon}}\ x{\isaliteral{29}{\isacharparenright}}\ simp{\isaliteral{5F}{\isacharunderscore}}all%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
 \isamarkupsection{Records \label{sec:hol-record}%
 }
 \isamarkuptrue%