# HG changeset patch # User wenzelm # Date 1306411934 -7200 # Node ID 6834af822a8bb3b7ab9f8851bcf5973f87fc90f2 # Parent 66b189dc5b83802e138cd58263f7b706eb2503e4 updated and simplified HOL datatype examples (NB: special treatment of distinctness has been discontinued in the vicinity of 542b34b178ec); diff -r 66b189dc5b83 -r 6834af822a8b doc-src/HOL/HOL.tex --- 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}} diff -r 66b189dc5b83 -r 6834af822a8b doc-src/IsarRef/Thy/HOL_Specific.thy --- 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 \ 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 \ Empty" + by simp +next + case (Seq y ys) + txt {* The step case is proved similarly. *} + show "Seq x (Seq y ys) \ Seq y ys" + using `Seq y ys \ ys` by simp +qed + +text {* Here is a more succinct version of the same proof: *} + +lemma "Seq x xs \ xs" + by (induct xs arbitrary: x) simp_all + + section {* Records \label{sec:hol-record} *} text {* diff -r 66b189dc5b83 -r 6834af822a8b doc-src/IsarRef/Thy/document/HOL_Specific.tex --- 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%