--- a/doc-src/TutorialI/Ifexpr/Ifexpr.thy Thu Nov 29 01:51:38 2001 +0100
+++ b/doc-src/TutorialI/Ifexpr/Ifexpr.thy Thu Nov 29 13:33:45 2001 +0100
@@ -162,7 +162,7 @@
normality of @{term"normif"}:
*}
-lemma[simp]: "\<forall>t e. normal(normif b t e) = (normal t \<and> normal e)";
+lemma [simp]: "\<forall>t e. normal(normif b t e) = (normal t \<and> normal e)";
(*<*)
apply(induct_tac b);
by(auto);
--- a/doc-src/TutorialI/Ifexpr/document/Ifexpr.tex Thu Nov 29 01:51:38 2001 +0100
+++ b/doc-src/TutorialI/Ifexpr/document/Ifexpr.tex Thu Nov 29 13:33:45 2001 +0100
@@ -187,7 +187,7 @@
normality of \isa{normif}:%
\end{isamarkuptext}%
\isamarkuptrue%
-\isacommand{lemma}{\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isasymforall}t\ e{\isachardot}\ normal{\isacharparenleft}normif\ b\ t\ e{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}normal\ t\ {\isasymand}\ normal\ e{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
+\isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isasymforall}t\ e{\isachardot}\ normal{\isacharparenleft}normif\ b\ t\ e{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}normal\ t\ {\isasymand}\ normal\ e{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
\isamarkupfalse%
\isamarkupfalse%
\isamarkupfalse%
--- a/doc-src/TutorialI/Misc/document/natsum.tex Thu Nov 29 01:51:38 2001 +0100
+++ b/doc-src/TutorialI/Misc/document/natsum.tex Thu Nov 29 13:33:45 2001 +0100
@@ -39,37 +39,38 @@
\sdx{div}, \sdx{mod}, \cdx{min} and
\cdx{max} are predefined, as are the relations
\indexboldpos{\isasymle}{$HOL2arithrel} and
-\ttindexboldpos{<}{$HOL2arithrel}. As usual, \isa{m\ {\isacharminus}\ n\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isacharparenright}} if
+\ttindexboldpos{<}{$HOL2arithrel}. As usual, \isa{m\ {\isacharminus}\ n\ {\isacharequal}\ {\isadigit{0}}} if
\isa{m\ {\isacharless}\ n}. There is even a least number operation
-\sdx{LEAST}\@. For example, \isa{{\isacharparenleft}LEAST\ n{\isachardot}\ {\isacharparenleft}{\isadigit{1}}{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isacharless}\ n{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isadigit{2}}{\isasymColon}{\isacharprime}a{\isacharparenright}}.
-\REMARK{Isabelle CAN prove it automatically, using \isa{auto intro: Least_equality}.
- The following needs changing with our new system of numbers.}
-Note that \isa{{\isadigit{1}}{\isasymColon}{\isacharprime}a}
-and \isa{{\isadigit{2}}{\isasymColon}{\isacharprime}a} are available as abbreviations for the corresponding
-\isa{Suc}-expressions. If you need the full set of numerals,
-see~\S\ref{sec:numerals}.
-
+\sdx{LEAST}\@. For example, \isa{{\isacharparenleft}LEAST\ n{\isachardot}\ {\isadigit{0}}\ {\isacharless}\ n{\isacharparenright}\ {\isacharequal}\ Suc\ {\isadigit{0}}}.
\begin{warn}\index{overloading}
- The constant \cdx{0} and the operations
+ The constants \cdx{0} and \cdx{1} and the operations
\ttindexboldpos{+}{$HOL2arithfun}, \ttindexboldpos{-}{$HOL2arithfun},
\ttindexboldpos{\mystar}{$HOL2arithfun}, \cdx{min},
\cdx{max}, \indexboldpos{\isasymle}{$HOL2arithrel} and
\ttindexboldpos{<}{$HOL2arithrel} are overloaded, i.e.\ they are available
not just for natural numbers but at other types as well.
- For example, given the goal \isa{x\ {\isacharplus}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isacharequal}\ x},
- there is nothing to indicate that you are talking about natural numbers.
- Hence Isabelle can only infer that \isa{x} is of some arbitrary type where
- \isa{{\isadigit{0}}{\isasymColon}{\isacharprime}a} and \isa{{\isacharplus}} are declared. As a consequence, you will be unable
- to prove the goal (although it may take you some time to realize what has
- happened if \isa{show{\isacharunderscore}types} is not set). In this particular example,
- you need to include an explicit type constraint, for example
- \isa{x{\isacharplus}{\isadigit{0}}\ {\isacharequal}\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}}. If there is enough contextual information this
- may not be necessary: \isa{Suc\ x\ {\isacharequal}\ x} automatically implies
- \isa{x{\isacharcolon}{\isacharcolon}nat} because \isa{Suc} is not overloaded.
+ For example, given the goal \isa{x\ {\isacharplus}\ {\isadigit{0}}\ {\isacharequal}\ x}, there is nothing to indicate
+ that you are talking about natural numbers. Hence Isabelle can only infer
+ that \isa{x} is of some arbitrary type where \isa{{\isadigit{0}}} and \isa{{\isacharplus}} are
+ declared. As a consequence, you will be unable to prove the
+ goal. To alert you to such pitfalls, Isabelle flags numerals without a
+ fixed type in its output: \isa{x\ {\isacharplus}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isacharequal}\ x}. (In the absence of a numeral,
+ it may take you some time to realize what has happened if \isa{show{\isacharunderscore}types} is not set). In this particular example, you need to include
+ an explicit type constraint, for example \isa{x{\isacharplus}{\isadigit{0}}\ {\isacharequal}\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}}. If there
+ is enough contextual information this may not be necessary: \isa{Suc\ x\ {\isacharequal}\ x} automatically implies \isa{x{\isacharcolon}{\isacharcolon}nat} because \isa{Suc} is not
+ overloaded.
- For details see \S\ref{sec:numbers} and \S\ref{sec:overloading};
- Table~\ref{tab:overloading} in the appendix shows the most important overloaded
- operations.
+ For details on overloading see \S\ref{sec:overloading}.
+ Table~\ref{tab:overloading} in the appendix shows the most important
+ overloaded operations.
+\end{warn}
+\begin{warn}
+ Constant \isa{{\isadigit{1}}{\isacharcolon}{\isacharcolon}nat} is defined to be \isa{Suc\ {\isadigit{0}}}. This definition
+ (see \S\ref{sec:ConstDefinitions}) is unfolded automatically by some
+ tactics (like \isa{auto}, \isa{simp} and \isa{arith}) but not by
+ others (especially the single step tactics in Chapter~\ref{chap:rules}).
+ If you need the full set of numerals, see~\S\ref{sec:numerals}.
+ \emph{Novices are advised to stick to \isa{{\isadigit{0}}} and of \isa{Suc}.}
\end{warn}
Both \isa{auto} and \isa{simp}
--- a/doc-src/TutorialI/Misc/natsum.thy Thu Nov 29 01:51:38 2001 +0100
+++ b/doc-src/TutorialI/Misc/natsum.thy Thu Nov 29 13:33:45 2001 +0100
@@ -28,37 +28,40 @@
\sdx{div}, \sdx{mod}, \cdx{min} and
\cdx{max} are predefined, as are the relations
\indexboldpos{\isasymle}{$HOL2arithrel} and
-\ttindexboldpos{<}{$HOL2arithrel}. As usual, @{prop"m-n = 0"} if
+\ttindexboldpos{<}{$HOL2arithrel}. As usual, @{prop"m-n = (0::nat)"} if
@{prop"m<n"}. There is even a least number operation
-\sdx{LEAST}\@. For example, @{prop"(LEAST n. 1 < n) = 2"}.
-\REMARK{Isabelle CAN prove it automatically, using \isa{auto intro: Least_equality}.
- The following needs changing with our new system of numbers.}
-Note that @{term 1}
-and @{term 2} are available as abbreviations for the corresponding
-@{term Suc}-expressions. If you need the full set of numerals,
-see~\S\ref{sec:numerals}.
-
+\sdx{LEAST}\@. For example, @{prop"(LEAST n. 0 < n) = Suc 0"}.
\begin{warn}\index{overloading}
- The constant \cdx{0} and the operations
+ The constants \cdx{0} and \cdx{1} and the operations
\ttindexboldpos{+}{$HOL2arithfun}, \ttindexboldpos{-}{$HOL2arithfun},
\ttindexboldpos{\mystar}{$HOL2arithfun}, \cdx{min},
\cdx{max}, \indexboldpos{\isasymle}{$HOL2arithrel} and
\ttindexboldpos{<}{$HOL2arithrel} are overloaded, i.e.\ they are available
not just for natural numbers but at other types as well.
- For example, given the goal @{prop"x+0 = x"},
- there is nothing to indicate that you are talking about natural numbers.
- Hence Isabelle can only infer that @{term x} is of some arbitrary type where
- @{term 0} and @{text"+"} are declared. As a consequence, you will be unable
- to prove the goal (although it may take you some time to realize what has
- happened if @{text show_types} is not set). In this particular example,
- you need to include an explicit type constraint, for example
- @{text"x+0 = (x::nat)"}. If there is enough contextual information this
- may not be necessary: @{prop"Suc x = x"} automatically implies
- @{text"x::nat"} because @{term Suc} is not overloaded.
+ For example, given the goal @{text"x + 0 = x"}, there is nothing to indicate
+ that you are talking about natural numbers. Hence Isabelle can only infer
+ that @{term x} is of some arbitrary type where @{text 0} and @{text"+"} are
+ declared. As a consequence, you will be unable to prove the
+ goal. To alert you to such pitfalls, Isabelle flags numerals without a
+ fixed type in its output: @{prop"x+0 = x"}. (In the absence of a numeral,
+ it may take you some time to realize what has happened if @{text
+ show_types} is not set). In this particular example, you need to include
+ an explicit type constraint, for example @{text"x+0 = (x::nat)"}. If there
+ is enough contextual information this may not be necessary: @{prop"Suc x =
+ x"} automatically implies @{text"x::nat"} because @{term Suc} is not
+ overloaded.
- For details see \S\ref{sec:numbers} and \S\ref{sec:overloading};
- Table~\ref{tab:overloading} in the appendix shows the most important overloaded
- operations.
+ For details on overloading see \S\ref{sec:overloading}.
+ Table~\ref{tab:overloading} in the appendix shows the most important
+ overloaded operations.
+\end{warn}
+\begin{warn}
+ Constant @{text"1::nat"} is defined to be @{term"Suc 0"}. This definition
+ (see \S\ref{sec:ConstDefinitions}) is unfolded automatically by some
+ tactics (like @{text auto}, @{text simp} and @{text arith}) but not by
+ others (especially the single step tactics in Chapter~\ref{chap:rules}).
+ If you need the full set of numerals, see~\S\ref{sec:numerals}.
+ \emph{Novices are advised to stick to @{term"0::nat"} and @{term Suc}.}
\end{warn}
Both @{text auto} and @{text simp}
--- a/doc-src/TutorialI/Misc/types.thy Thu Nov 29 01:51:38 2001 +0100
+++ b/doc-src/TutorialI/Misc/types.thy Thu Nov 29 13:33:45 2001 +0100
@@ -1,7 +1,7 @@
(*<*)theory "types" = Main:(*>*)
types number = nat
gate = "bool \<Rightarrow> bool \<Rightarrow> bool"
- ('a,'b)alist = "('a \<times> 'b)list";
+ ('a,'b)alist = "('a \<times> 'b)list"
text{*\noindent
Internally all synonyms are fully expanded. As a consequence Isabelle's
@@ -11,7 +11,7 @@
*}
consts nand :: gate
- xor :: gate;
+ xor :: gate
subsection{*Constant Definitions*}
@@ -21,7 +21,7 @@
*}
defs nand_def: "nand A B \<equiv> \<not>(A \<and> B)"
- xor_def: "xor A B \<equiv> A \<and> \<not>B \<or> \<not>A \<and> B";
+ xor_def: "xor A B \<equiv> A \<and> \<not>B \<or> \<not>A \<and> B"
text{*\noindent%
Here \commdx{defs} is a keyword and
@@ -41,7 +41,7 @@
constdefs nor :: gate
"nor A B \<equiv> \<not>(A \<or> B)"
xor2 :: gate
- "xor2 A B \<equiv> (A \<or> B) \<and> (\<not>A \<or> \<not>B)";
+ "xor2 A B \<equiv> (A \<or> B) \<and> (\<not>A \<or> \<not>B)"
text{*\noindent
The default name of each definition is $f$@{text"_def"}, where
--- a/doc-src/TutorialI/ToyList/ToyList.thy Thu Nov 29 01:51:38 2001 +0100
+++ b/doc-src/TutorialI/ToyList/ToyList.thy Thu Nov 29 13:33:45 2001 +0100
@@ -13,8 +13,8 @@
| Cons 'a "'a list" (infixr "#" 65);
text{*\noindent
-\index{datatype@\isacommand {datatype} (command)}
-The datatype \tydx{list} introduces two
+The datatype\index{datatype@\isacommand {datatype} (command)}
+\tydx{list} introduces two
constructors \cdx{Nil} and \cdx{Cons}, the
empty~list and the operator that adds an element to the front of a list. For
example, the term \isa{Cons True (Cons False Nil)} is a value of
@@ -142,7 +142,7 @@
@{term"xs"}.
\end{itemize}
The name and the simplification attribute are optional.
-Isabelle's response is to print
+Isabelle's response is to print the initial proof state
\begin{isabelle}
proof(prove):~step~0\isanewline
\isanewline
@@ -187,7 +187,7 @@
The induction step is an example of the general format of a subgoal:\index{subgoals}
\begin{isabelle}
-~$i$.~{\isasymAnd}$x\sb{1}$~\dots~$x\sb{n}$.~{\it assumptions}~{\isasymLongrightarrow}~{\it conclusion}
+~$i$.~{\isasymAnd}$x\sb{1}$~\dots$x\sb{n}$.~{\it assumptions}~{\isasymLongrightarrow}~{\it conclusion}
\end{isabelle}\index{$IsaAnd@\isasymAnd|bold}
The prefix of bound variables \isasymAnd$x\sb{1}$~\dots~$x\sb{n}$ can be
ignored most of the time, or simply treated as a list of variables local to
--- a/doc-src/TutorialI/ToyList/document/ToyList.tex Thu Nov 29 01:51:38 2001 +0100
+++ b/doc-src/TutorialI/ToyList/document/ToyList.tex Thu Nov 29 13:33:45 2001 +0100
@@ -18,8 +18,8 @@
%
\begin{isamarkuptext}%
\noindent
-\index{datatype@\isacommand {datatype} (command)}
-The datatype \tydx{list} introduces two
+The datatype\index{datatype@\isacommand {datatype} (command)}
+\tydx{list} introduces two
constructors \cdx{Nil} and \cdx{Cons}, the
empty~list and the operator that adds an element to the front of a list. For
example, the term \isa{Cons True (Cons False Nil)} is a value of
@@ -150,7 +150,7 @@
\isa{xs}.
\end{itemize}
The name and the simplification attribute are optional.
-Isabelle's response is to print
+Isabelle's response is to print the initial proof state
\begin{isabelle}
proof(prove):~step~0\isanewline
\isanewline
@@ -200,7 +200,7 @@
The induction step is an example of the general format of a subgoal:\index{subgoals}
\begin{isabelle}
-~$i$.~{\isasymAnd}$x\sb{1}$~\dots~$x\sb{n}$.~{\it assumptions}~{\isasymLongrightarrow}~{\it conclusion}
+~$i$.~{\isasymAnd}$x\sb{1}$~\dots$x\sb{n}$.~{\it assumptions}~{\isasymLongrightarrow}~{\it conclusion}
\end{isabelle}\index{$IsaAnd@\isasymAnd|bold}
The prefix of bound variables \isasymAnd$x\sb{1}$~\dots~$x\sb{n}$ can be
ignored most of the time, or simply treated as a list of variables local to
--- a/doc-src/TutorialI/basics.tex Thu Nov 29 01:51:38 2001 +0100
+++ b/doc-src/TutorialI/basics.tex Thu Nov 29 13:33:45 2001 +0100
@@ -35,7 +35,8 @@
introduces the rudiments of Isar's proof language. To fully exploit the power
of Isar, in particular the ability to write readable and structured proofs,
you need to consult the Isabelle/Isar Reference
-Manual~\cite{isabelle-isar-ref}. If you want to use Isabelle's ML level
+Manual~\cite{isabelle-isar-ref} and Wenzel's PhD thesis~\cite{Wenzel-PhD}
+which discusses many proof patterns. If you want to use Isabelle's ML level
directly (for example for writing your own proof procedures) see the Isabelle
Reference Manual~\cite{isabelle-ref}; for details relating to HOL see the
Isabelle/HOL manual~\cite{isabelle-HOL}. All manuals have a comprehensive
@@ -70,7 +71,8 @@
This tutorial is concerned with introducing you to the different linguistic
constructs that can fill the \textit{declarations, definitions, and
proofs} above. A complete grammar of the basic
-constructs is found in the Isabelle/Isar Reference Manual.
+constructs is found in the Isabelle/Isar Reference
+Manual~\cite{isabelle-isar-ref}.
HOL's theory collection is available online at
\begin{center}\small
@@ -244,11 +246,10 @@
\isa{\isasymlambda}, and quantifiers.
\item
Never write \isa{\isasymlambda{}x.x} or \isa{\isasymforall{}x.x=x}
-because \isa{x.x} is always taken as a single qualified identifier that
-refers to an item \isa{x} in theory \isa{x}. Write
+because \isa{x.x} is always taken as a single qualified identifier. Write
\isa{\isasymlambda{}x.~x} and \isa{\isasymforall{}x.~x=x} instead.
\item Identifiers\indexbold{identifiers} may contain the characters \isa{_}
-and~\isa{'}.
+and~\isa{'}, except at the beginning.
\end{itemize}
For the sake of readability, we use the usual mathematical symbols throughout
--- a/doc-src/TutorialI/fp.tex Thu Nov 29 01:51:38 2001 +0100
+++ b/doc-src/TutorialI/fp.tex Thu Nov 29 13:33:45 2001 +0100
@@ -37,8 +37,9 @@
The complete proof script is shown in Fig.\ts\ref{fig:ToyList-proofs}. The
concatenation of Figs.\ts\ref{fig:ToyList} and~\ref{fig:ToyList-proofs}
constitutes the complete theory \texttt{ToyList} and should reside in file
-\texttt{ToyList.thy}. It is good practice to present all declarations and
-definitions at the beginning of a theory to facilitate browsing.%
+\texttt{ToyList.thy}.
+% It is good practice to present all declarations and
+%definitions at the beginning of a theory to facilitate browsing.%
\index{*ToyList example|)}
\begin{figure}[htbp]
@@ -70,7 +71,7 @@
There are two kinds of commands used during a proof: the actual proof
commands and auxiliary commands for examining the proof state and controlling
the display. Simple proof commands are of the form
-\commdx{apply}\isa{(\textit{method})}, where \textit{method} is typically
+\commdx{apply}(\textit{method}), where \textit{method} is typically
\isa{induct_tac} or \isa{auto}. All such theorem proving operations
are referred to as \bfindex{methods}, and further ones are
introduced throughout the tutorial. Unless stated otherwise, you may
@@ -144,7 +145,8 @@
% theory itself. This you can do by typing
% \isa{\commdx{use\_thy}~"T"}.
\end{description}
-Further commands are found in the Isabelle/Isar Reference Manual.
+Further commands are found in the Isabelle/Isar Reference
+Manual~\cite{isabelle-isar-ref}.
We now examine Isabelle's functional programming constructs systematically,
starting with inductive datatypes.
@@ -175,7 +177,7 @@
Theory \isa{List} also contains
more syntactic sugar: \isa{[}$x@1$\isa{,}\dots\isa{,}$x@n$\isa{]} abbreviates
$x@1$\isa{\#}\dots\isa{\#}$x@n$\isa{\#[]}. In the rest of the tutorial we
-always use HOL's predefined lists.
+always use HOL's predefined lists by building on theory \isa{Main}.
\subsection{The General Format}
@@ -198,10 +200,12 @@
during proofs by simplification. The same is true for the equations in
primitive recursive function definitions.
-Every datatype $t$ comes equipped with a \isa{size} function from $t$ into
-the natural numbers (see~{\S}\ref{sec:nat} below). For lists, \isa{size} is
-just the length, i.e.\ \isa{size [] = 0} and \isa{size(x \# xs) = size xs +
- 1}. In general, \cdx{size} returns
+Every\footnote{Except for advanced datatypes where the recursion involves
+``\isasymRightarrow'' as in {\S}\ref{sec:nested-fun-datatype}.} datatype $t$
+comes equipped with a \isa{size} function from $t$ into the natural numbers
+(see~{\S}\ref{sec:nat} below). For lists, \isa{size} is just the length, i.e.\
+\isa{size [] = 0} and \isa{size(x \# xs) = size xs + 1}. In general,
+\cdx{size} returns
\begin{itemize}
\item zero for all constructors
that do not have an argument of type $t$\\
@@ -275,12 +279,11 @@
\subsection{Type Synonyms}
-\index{type synonyms|(}%
+\index{type synonyms}%
Type synonyms are similar to those found in ML\@. They are created by a
\commdx{types} command:
-\input{Misc/document/types.tex}%
-\index{type synonyms|)}
+\input{Misc/document/types.tex}
\input{Misc/document/prime_def.tex}
@@ -397,6 +400,7 @@
\subsection{The Limits of Nested Recursion}
+\label{sec:nested-fun-datatype}
How far can we push nested recursion? By the unfolding argument above, we can
reduce nested to mutual recursion provided the nested recursion only involves
--- a/doc-src/TutorialI/preface.tex Thu Nov 29 01:51:38 2001 +0100
+++ b/doc-src/TutorialI/preface.tex Thu Nov 29 13:33:45 2001 +0100
@@ -16,9 +16,11 @@
eight simplification tactics with a single method, namely \isa{simp},
with associated options.
-The typesetting relies on Wenzel's proof presentation tools. A possibly
-annotated theory file is run, typesetting the theory and any requested
-Isabelle responses in the form of a \TeX{} source file. This book is
+\REMARK{mention Wenzel once author?}
+The typesetting relies on Wenzel's theory presentation tools. An
+annotated source file is run, typesetting the theory
+% and any requested Isabelle responses
+in the form of a \TeX\ source file. This book is
derived almost entirely from output generated in this way.
This tutorial owes a lot to the constant discussions with and the valuable