1.1 --- a/doc-src/TutorialI/Advanced/Partial.thy Fri Feb 16 08:10:28 2001 +0100
1.2 +++ b/doc-src/TutorialI/Advanced/Partial.thy Fri Feb 16 08:27:17 2001 +0100
1.3 @@ -69,7 +69,7 @@
1.4 @{prop[display]"find(f,x) = (if f x = x then x else find(f, f x))"}
1.5 This may be viewed as a fixed point finder or as one half of the well known
1.6 \emph{Union-Find} algorithm.
1.7 -The snag is that it may not terminate if @{term f} has nontrivial cycles.
1.8 +The snag is that it may not terminate if @{term f} has non-trivial cycles.
1.9 Phrased differently, the relation
1.10 *}
1.11
2.1 --- a/doc-src/TutorialI/Advanced/document/Partial.tex Fri Feb 16 08:10:28 2001 +0100
2.2 +++ b/doc-src/TutorialI/Advanced/document/Partial.tex Fri Feb 16 08:27:17 2001 +0100
2.3 @@ -74,7 +74,7 @@
2.4 \end{isabelle}
2.5 This may be viewed as a fixed point finder or as one half of the well known
2.6 \emph{Union-Find} algorithm.
2.7 -The snag is that it may not terminate if \isa{f} has nontrivial cycles.
2.8 +The snag is that it may not terminate if \isa{f} has non-trivial cycles.
2.9 Phrased differently, the relation%
2.10 \end{isamarkuptext}%
2.11 \isacommand{constdefs}\ step{\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}set{\isachardoublequote}\isanewline
3.1 --- a/doc-src/TutorialI/CTL/CTL.thy Fri Feb 16 08:10:28 2001 +0100
3.2 +++ b/doc-src/TutorialI/CTL/CTL.thy Fri Feb 16 08:27:17 2001 +0100
3.3 @@ -247,7 +247,7 @@
3.4 What is worth noting here is that we have used @{text fast} rather than
3.5 @{text blast}. The reason is that @{text blast} would fail because it cannot
3.6 cope with @{thm[source]someI2_ex}: unifying its conclusion with the current
3.7 -subgoal is nontrivial because of the nested schematic variables. For
3.8 +subgoal is non-trivial because of the nested schematic variables. For
3.9 efficiency reasons @{text blast} does not even attempt such unifications.
3.10 Although @{text fast} can in principle cope with complicated unification
3.11 problems, in practice the number of unifiers arising is often prohibitive and
4.1 --- a/doc-src/TutorialI/CTL/document/CTL.tex Fri Feb 16 08:10:28 2001 +0100
4.2 +++ b/doc-src/TutorialI/CTL/document/CTL.tex Fri Feb 16 08:27:17 2001 +0100
4.3 @@ -206,7 +206,7 @@
4.4 What is worth noting here is that we have used \isa{fast} rather than
4.5 \isa{blast}. The reason is that \isa{blast} would fail because it cannot
4.6 cope with \isa{someI{\isadigit{2}}{\isacharunderscore}ex}: unifying its conclusion with the current
4.7 -subgoal is nontrivial because of the nested schematic variables. For
4.8 +subgoal is non-trivial because of the nested schematic variables. For
4.9 efficiency reasons \isa{blast} does not even attempt such unifications.
4.10 Although \isa{fast} can in principle cope with complicated unification
4.11 problems, in practice the number of unifiers arising is often prohibitive and
5.1 --- a/doc-src/TutorialI/Types/Pairs.thy Fri Feb 16 08:10:28 2001 +0100
5.2 +++ b/doc-src/TutorialI/Types/Pairs.thy Fri Feb 16 08:27:17 2001 +0100
5.3 @@ -5,7 +5,7 @@
5.4 text{*\label{sec:products}
5.5 Pairs were already introduced in \S\ref{sec:pairs}, but only with a minimal
5.6 repertoire of operations: pairing and the two projections @{term fst} and
5.7 -@{term snd}. In any nontrivial application of pairs you will find that this
5.8 +@{term snd}. In any non-trivial application of pairs you will find that this
5.9 quickly leads to unreadable formulae involvings nests of projections. This
5.10 section is concerned with introducing some syntactic sugar to overcome this
5.11 problem: pattern matching with tuples.
5.12 @@ -26,9 +26,6 @@
5.13 @{text"{(x,y,z). x=z}"}\\
5.14 @{term"\<Union>(x,y)\<in>A. {x+y}"}
5.15 \end{quote}
5.16 -*}
5.17 -
5.18 -text{*
5.19 The intuitive meanings of these expressions should be obvious.
5.20 Unfortunately, we need to know in more detail what the notation really stands
5.21 for once we have to reason about it. Abstraction
5.22 @@ -62,7 +59,7 @@
5.23 by(simp add:split_def)
5.24
5.25 text{* This works well if rewriting with @{thm[source]split_def} finishes the
5.26 -proof, as it does above. But if it doesn't, you end up with exactly what
5.27 +proof, as it does above. But if it does not, you end up with exactly what
5.28 we are trying to avoid: nests of @{term fst} and @{term snd}. Thus this
5.29 approach is neither elegant nor very practical in large examples, although it
5.30 can be effective in small ones.
6.1 --- a/doc-src/TutorialI/Types/Typedef.thy Fri Feb 16 08:10:28 2001 +0100
6.2 +++ b/doc-src/TutorialI/Types/Typedef.thy Fri Feb 16 08:27:17 2001 +0100
6.3 @@ -265,7 +265,7 @@
6.4 Although @{typ three} could be defined in one line, we have chosen this
6.5 example to demonstrate \isacommand{typedef} because its simplicity makes the
6.6 key concepts particularly easy to grasp. If you would like to see a
6.7 -nontrivial example that cannot be defined more directly, we recommend the
6.8 +non-trivial example that cannot be defined more directly, we recommend the
6.9 definition of \emph{finite multisets} in the HOL Library.
6.10
6.11 Let us conclude by summarizing the above procedure for defining a new type.
7.1 --- a/doc-src/TutorialI/Types/document/Pairs.tex Fri Feb 16 08:10:28 2001 +0100
7.2 +++ b/doc-src/TutorialI/Types/document/Pairs.tex Fri Feb 16 08:27:17 2001 +0100
7.3 @@ -9,7 +9,7 @@
7.4 \label{sec:products}
7.5 Pairs were already introduced in \S\ref{sec:pairs}, but only with a minimal
7.6 repertoire of operations: pairing and the two projections \isa{fst} and
7.7 -\isa{snd}. In any nontrivial application of pairs you will find that this
7.8 +\isa{snd}. In any non-trivial application of pairs you will find that this
7.9 quickly leads to unreadable formulae involvings nests of projections. This
7.10 section is concerned with introducing some syntactic sugar to overcome this
7.11 problem: pattern matching with tuples.%
7.12 @@ -30,10 +30,7 @@
7.13 \isa{{\isasymforall}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}{\isasymin}A{\isachardot}\ x{\isacharequal}y}\\
7.14 \isa{{\isacharbraceleft}{\isacharparenleft}x{\isacharcomma}y{\isacharcomma}z{\isacharparenright}{\isachardot}\ x{\isacharequal}z{\isacharbraceright}}\\
7.15 \isa{{\isasymUnion}{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}{\isasymin}A{\isachardot}\ {\isacharbraceleft}x\ {\isacharplus}\ y{\isacharbraceright}}
7.16 -\end{quote}%
7.17 -\end{isamarkuptext}%
7.18 -%
7.19 -\begin{isamarkuptext}%
7.20 +\end{quote}
7.21 The intuitive meanings of these expressions should be obvious.
7.22 Unfortunately, we need to know in more detail what the notation really stands
7.23 for once we have to reason about it. Abstraction
7.24 @@ -66,7 +63,7 @@
7.25 \isacommand{by}{\isacharparenleft}simp\ add{\isacharcolon}split{\isacharunderscore}def{\isacharparenright}%
7.26 \begin{isamarkuptext}%
7.27 This works well if rewriting with \isa{split{\isacharunderscore}def} finishes the
7.28 -proof, as it does above. But if it doesn't, you end up with exactly what
7.29 +proof, as it does above. But if it does not, you end up with exactly what
7.30 we are trying to avoid: nests of \isa{fst} and \isa{snd}. Thus this
7.31 approach is neither elegant nor very practical in large examples, although it
7.32 can be effective in small ones.
8.1 --- a/doc-src/TutorialI/Types/document/Typedef.tex Fri Feb 16 08:10:28 2001 +0100
8.2 +++ b/doc-src/TutorialI/Types/document/Typedef.tex Fri Feb 16 08:27:17 2001 +0100
8.3 @@ -262,7 +262,7 @@
8.4 Although \isa{three} could be defined in one line, we have chosen this
8.5 example to demonstrate \isacommand{typedef} because its simplicity makes the
8.6 key concepts particularly easy to grasp. If you would like to see a
8.7 -nontrivial example that cannot be defined more directly, we recommend the
8.8 +non-trivial example that cannot be defined more directly, we recommend the
8.9 definition of \emph{finite multisets} in the HOL Library.
8.10
8.11 Let us conclude by summarizing the above procedure for defining a new type.
9.1 --- a/doc-src/TutorialI/Types/types.tex Fri Feb 16 08:10:28 2001 +0100
9.2 +++ b/doc-src/TutorialI/Types/types.tex Fri Feb 16 08:27:17 2001 +0100
9.3 @@ -9,13 +9,18 @@
9.4 \item More about basic types: numbers ({\S}\ref{sec:numbers}), pairs
9.5 ({\S}\ref{sec:products}) and records ({\S}\ref{sec:records}), and how to
9.6 reason about them.
9.7 +\item Type classes: how to specify and reason about axiomatic collections of
9.8 + types ({\S}\ref{sec:axclass}).
9.9 \item Introducing your own types: how to introduce new types that
9.10 cannot be constructed with any of the basic methods
9.11 ({\S}\ref{sec:adv-typedef}).
9.12 -\item Type classes: how to specify and reason about axiomatic collections of
9.13 - types ({\S}\ref{sec:axclass}).
9.14 \end{itemize}
9.15
9.16 +The material in this section goes beyond the needs of most novices. Serious
9.17 +users should at least skim the sections on basic types and on type classes.
9.18 +The latter is fairly advanced: read the beginning to understand what it is
9.19 +about, but consult the rest only when necessary.
9.20 +
9.21 \section{Numbers}
9.22 \label{sec:numbers}
9.23
9.24 @@ -28,8 +33,6 @@
9.25 \section{Records}
9.26 \label{sec:records}
9.27
9.28 -\input{Types/document/Typedef}
9.29 -
9.30 \section{Axiomatic type classes}
9.31 \label{sec:axclass}
9.32 \index{axiomatic type class|(}
9.33 @@ -62,3 +65,6 @@
9.34
9.35 \index{axiomatic type class|)}
9.36 \index{*axclass|)}
9.37 +
9.38 +
9.39 +\input{Types/document/Typedef}