# HG changeset patch # User nipkow # Date 1007037225 -3600 # Node ID 5a4d782044924026ad49cb05fe59461073b46935 # Parent b4e706774e961defe02f691b8abe8b344c9d4a84 *** empty log message *** diff -r b4e706774e96 -r 5a4d78204492 doc-src/TutorialI/Ifexpr/Ifexpr.thy --- 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]: "\t e. normal(normif b t e) = (normal t \ normal e)"; +lemma [simp]: "\t e. normal(normif b t e) = (normal t \ normal e)"; (*<*) apply(induct_tac b); by(auto); diff -r b4e706774e96 -r 5a4d78204492 doc-src/TutorialI/Ifexpr/document/Ifexpr.tex --- 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% diff -r b4e706774e96 -r 5a4d78204492 doc-src/TutorialI/Misc/document/natsum.tex --- 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} diff -r b4e706774e96 -r 5a4d78204492 doc-src/TutorialI/Misc/natsum.thy --- 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*) types number = nat gate = "bool \ bool \ bool" - ('a,'b)alist = "('a \ 'b)list"; + ('a,'b)alist = "('a \ '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 \ \(A \ B)" - xor_def: "xor A B \ A \ \B \ \A \ B"; + xor_def: "xor A B \ A \ \B \ \A \ B" text{*\noindent% Here \commdx{defs} is a keyword and @@ -41,7 +41,7 @@ constdefs nor :: gate "nor A B \ \(A \ B)" xor2 :: gate - "xor2 A B \ (A \ B) \ (\A \ \B)"; + "xor2 A B \ (A \ B) \ (\A \ \B)" text{*\noindent The default name of each definition is $f$@{text"_def"}, where diff -r b4e706774e96 -r 5a4d78204492 doc-src/TutorialI/ToyList/ToyList.thy --- 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 diff -r b4e706774e96 -r 5a4d78204492 doc-src/TutorialI/ToyList/document/ToyList.tex --- 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 diff -r b4e706774e96 -r 5a4d78204492 doc-src/TutorialI/basics.tex --- 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 diff -r b4e706774e96 -r 5a4d78204492 doc-src/TutorialI/fp.tex --- 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 diff -r b4e706774e96 -r 5a4d78204492 doc-src/TutorialI/preface.tex --- 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