--- a/doc-src/TutorialI/IsaMakefile Wed Nov 29 10:22:38 2000 +0100
+++ b/doc-src/TutorialI/IsaMakefile Wed Nov 29 13:44:26 2000 +0100
@@ -142,7 +142,8 @@
HOL-Types: HOL $(LOG)/HOL-Types.gz
-$(LOG)/HOL-Types.gz: $(OUT)/HOL Types/ROOT.ML Types/Typedef.thy \
+$(LOG)/HOL-Types.gz: $(OUT)/HOL Types/ROOT.ML Types/Pairs.thy \
+ Types/Typedef.thy \
Types/Overloading0.thy Types/Overloading1.thy Types/Overloading2.thy \
Types/Overloading.thy Types/Axioms.thy
@$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL Types
@@ -155,7 +156,6 @@
$(LOG)/HOL-Misc.gz: $(OUT)/HOL Misc/ROOT.ML Misc/Tree.thy Misc/Tree2.thy \
Misc/fakenat.thy Misc/natsum.thy Misc/pairs.thy Misc/types.thy \
Misc/prime_def.thy Misc/case_exprs.thy \
- Misc/arith1.thy Misc/arith2.thy Misc/arith3.thy \
Misc/simp.thy Misc/Itrev.thy Misc/AdvancedInd.thy
@$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL Misc
@rm -f tutorial.dvi
--- a/doc-src/TutorialI/Misc/ROOT.ML Wed Nov 29 10:22:38 2000 +0100
+++ b/doc-src/TutorialI/Misc/ROOT.ML Wed Nov 29 13:44:26 2000 +0100
@@ -4,9 +4,6 @@
use_thy "case_exprs";
use_thy "fakenat";
use_thy "natsum";
-use_thy "arith1";
-use_thy "arith2";
-use_thy "arith3";
use_thy "pairs";
use_thy "types";
use_thy "prime_def";
--- a/doc-src/TutorialI/Misc/arith1.thy Wed Nov 29 10:22:38 2000 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,8 +0,0 @@
-(*<*)
-theory arith1 = Main:;
-(*>*)
-lemma "\<lbrakk> \<not> m < n; m < n+1 \<rbrakk> \<Longrightarrow> m = n";
-(**)(*<*)
-by(auto);
-end
-(*>*)
--- a/doc-src/TutorialI/Misc/arith2.thy Wed Nov 29 10:22:38 2000 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,9 +0,0 @@
-(*<*)
-theory arith2 = Main:;
-(*>*)
-lemma "min i (max j (k*k)) = max (min (k*k) i) (min i (j::nat))";
-apply(arith);
-(**)(*<*)
-done
-end
-(*>*)
--- a/doc-src/TutorialI/Misc/arith3.thy Wed Nov 29 10:22:38 2000 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,8 +0,0 @@
-(*<*)
-theory arith3 = Main:;
-(*>*)
-lemma "n*n = n \\<Longrightarrow> n=0 \\<or> n=1";
-(**)(*<*)
-oops;
-end
-(*>*)
--- a/doc-src/TutorialI/Misc/document/arith1.tex Wed Nov 29 10:22:38 2000 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,9 +0,0 @@
-%
-\begin{isabellebody}%
-\def\isabellecontext{arith{\isadigit{1}}}%
-\isacommand{lemma}\ {\isachardoublequote}{\isasymlbrakk}\ {\isasymnot}\ m\ {\isacharless}\ n{\isacharsemicolon}\ m\ {\isacharless}\ n{\isacharplus}{\isadigit{1}}\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ m\ {\isacharequal}\ n{\isachardoublequote}\isanewline
-\end{isabellebody}%
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: "root"
-%%% End:
--- a/doc-src/TutorialI/Misc/document/arith2.tex Wed Nov 29 10:22:38 2000 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,10 +0,0 @@
-%
-\begin{isabellebody}%
-\def\isabellecontext{arith{\isadigit{2}}}%
-\isacommand{lemma}\ {\isachardoublequote}min\ i\ {\isacharparenleft}max\ j\ {\isacharparenleft}k{\isacharasterisk}k{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ max\ {\isacharparenleft}min\ {\isacharparenleft}k{\isacharasterisk}k{\isacharparenright}\ i{\isacharparenright}\ {\isacharparenleft}min\ i\ {\isacharparenleft}j{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isanewline
-\isacommand{apply}{\isacharparenleft}arith{\isacharparenright}\isanewline
-\end{isabellebody}%
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: "root"
-%%% End:
--- a/doc-src/TutorialI/Misc/document/arith3.tex Wed Nov 29 10:22:38 2000 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,9 +0,0 @@
-%
-\begin{isabellebody}%
-\def\isabellecontext{arith{\isadigit{3}}}%
-\isacommand{lemma}\ {\isachardoublequote}n{\isacharasterisk}n\ {\isacharequal}\ n\ {\isasymLongrightarrow}\ n{\isacharequal}{\isadigit{0}}\ {\isasymor}\ n{\isacharequal}{\isadigit{1}}{\isachardoublequote}\isanewline
-\end{isabellebody}%
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: "root"
-%%% End:
--- a/doc-src/TutorialI/Misc/document/natsum.tex Wed Nov 29 10:22:38 2000 +0100
+++ b/doc-src/TutorialI/Misc/document/natsum.tex Wed Nov 29 13:44:26 2000 +0100
@@ -20,7 +20,80 @@
\isacommand{lemma}\ {\isachardoublequote}sum\ n\ {\isacharplus}\ sum\ n\ {\isacharequal}\ n{\isacharasterisk}{\isacharparenleft}Suc\ n{\isacharparenright}{\isachardoublequote}\isanewline
\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ n{\isacharparenright}\isanewline
\isacommand{apply}{\isacharparenleft}auto{\isacharparenright}\isanewline
-\isacommand{done}\isanewline
+\isacommand{done}%
+\begin{isamarkuptext}%
+\newcommand{\mystar}{*%
+}
+The usual arithmetic operations \ttindexboldpos{+}{$HOL2arithfun},
+\ttindexboldpos{-}{$HOL2arithfun}, \ttindexboldpos{\mystar}{$HOL2arithfun},
+\isaindexbold{div}, \isaindexbold{mod}, \isaindexbold{min} and
+\isaindexbold{max} are predefined, as are the relations
+\indexboldpos{\isasymle}{$HOL2arithrel} and
+\ttindexboldpos{<}{$HOL2arithrel}. There is even a least number operation
+\isaindexbold{LEAST}. For example, \isa{{\isacharparenleft}LEAST\ n{\isachardot}\ {\isadigit{1}}\ {\isacharless}\ n{\isacharparenright}\ {\isacharequal}\ {\isadigit{2}}}, although
+Isabelle does not prove this completely automatically. Note that \isa{{\isadigit{1}}}
+and \isa{{\isadigit{2}}} are available as abbreviations for the corresponding
+\isa{Suc}-expressions. If you need the full set of numerals,
+see~\S\ref{nat-numerals}.
+
+\begin{warn}
+ The constant \ttindexbold{0} and the operations
+ \ttindexboldpos{+}{$HOL2arithfun}, \ttindexboldpos{-}{$HOL2arithfun},
+ \ttindexboldpos{\mystar}{$HOL2arithfun}, \isaindexbold{min},
+ \isaindexbold{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 (see
+ \S\ref{sec:overloading}). 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 (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}\ x}. 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.
+\end{warn}
+
+Simple arithmetic goals are proved automatically by both \isa{auto} and the
+simplification methods introduced in \S\ref{sec:Simplification}. For
+example,%
+\end{isamarkuptext}%
+\isacommand{lemma}\ {\isachardoublequote}{\isasymlbrakk}\ {\isasymnot}\ m\ {\isacharless}\ n{\isacharsemicolon}\ m\ {\isacharless}\ n{\isacharplus}{\isadigit{1}}\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ m\ {\isacharequal}\ n{\isachardoublequote}%
+\begin{isamarkuptext}%
+\noindent
+is proved automatically. The main restriction is that only addition is taken
+into account; other arithmetic operations and quantified formulae are ignored.
+
+For more complex goals, there is the special method \isaindexbold{arith}
+(which attacks the first subgoal). It proves arithmetic goals involving the
+usual logical connectives (\isa{{\isasymnot}}, \isa{{\isasymand}}, \isa{{\isasymor}},
+\isa{{\isasymlongrightarrow}}), the relations \isa{{\isasymle}} and \isa{{\isacharless}}, and the operations
+\isa{{\isacharplus}}, \isa{{\isacharminus}}, \isa{min} and \isa{max}. For example,%
+\end{isamarkuptext}%
+\isacommand{lemma}\ {\isachardoublequote}min\ i\ {\isacharparenleft}max\ j\ {\isacharparenleft}k{\isacharasterisk}k{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ max\ {\isacharparenleft}min\ {\isacharparenleft}k{\isacharasterisk}k{\isacharparenright}\ i{\isacharparenright}\ {\isacharparenleft}min\ i\ {\isacharparenleft}j{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isanewline
+\isacommand{apply}{\isacharparenleft}arith{\isacharparenright}%
+\begin{isamarkuptext}%
+\noindent
+succeeds because \isa{k\ {\isacharasterisk}\ k} can be treated as atomic. In contrast,%
+\end{isamarkuptext}%
+\isacommand{lemma}\ {\isachardoublequote}n{\isacharasterisk}n\ {\isacharequal}\ n\ {\isasymLongrightarrow}\ n{\isacharequal}{\isadigit{0}}\ {\isasymor}\ n{\isacharequal}{\isadigit{1}}{\isachardoublequote}%
+\begin{isamarkuptext}%
+\noindent
+is not even proved by \isa{arith} because the proof relies essentially
+on properties of multiplication.
+
+\begin{warn}
+ The running time of \isa{arith} is exponential in the number of occurrences
+ of \ttindexboldpos{-}{$HOL2arithfun}, \isaindexbold{min} and
+ \isaindexbold{max} because they are first eliminated by case distinctions.
+
+ \isa{arith} is incomplete even for the restricted class of formulae
+ described above (known as ``linear arithmetic''). If divisibility plays a
+ role, it may fail to prove a valid formula, for example
+ \isa{m\ {\isacharplus}\ m\ {\isasymnoteq}\ n\ {\isacharplus}\ n\ {\isacharplus}\ {\isadigit{1}}}. Fortunately, such examples are rare in practice.
+\end{warn}%
+\end{isamarkuptext}%
\end{isabellebody}%
%%% Local Variables:
%%% mode: latex
--- a/doc-src/TutorialI/Misc/document/pairs.tex Wed Nov 29 10:22:38 2000 +0100
+++ b/doc-src/TutorialI/Misc/document/pairs.tex Wed Nov 29 13:44:26 2000 +0100
@@ -3,25 +3,28 @@
\def\isabellecontext{pairs}%
%
\begin{isamarkuptext}%
+\label{sec:pairs}\indexbold{product type}
+\index{pair|see{product type}}\index{tuple|see{product type}}
HOL also has pairs: \isa{($a@1$,$a@2$)} is of type $\tau@1$
-\indexboldpos{\isasymtimes}{$IsaFun} $\tau@2$ provided each $a@i$ is of type
-$\tau@i$. The components of a pair are extracted by \isa{fst} and
-\isa{snd}: \isa{fst($x$,$y$) = $x$} and \isa{snd($x$,$y$) = $y$}. Tuples
+\indexboldpos{\isasymtimes}{$Isatype} $\tau@2$ provided each $a@i$ is of type
+$\tau@i$. The components of a pair are extracted by \isaindexbold{fst} and
+\isaindexbold{snd}:
+ \isa{fst($x$,$y$) = $x$} and \isa{snd($x$,$y$) = $y$}. Tuples
are simulated by pairs nested to the right: \isa{($a@1$,$a@2$,$a@3$)} stands
for \isa{($a@1$,($a@2$,$a@3$))} and $\tau@1 \times \tau@2 \times \tau@3$ for
$\tau@1 \times (\tau@2 \times \tau@3)$. Therefore we have
\isa{fst(snd($a@1$,$a@2$,$a@3$)) = $a@2$}.
-It is possible to use (nested) tuples as patterns in abstractions, for
-example \isa{\isasymlambda(x,y,z).x+y+z} and
-\isa{\isasymlambda((x,y),z).x+y+z}.
-In addition to explicit $\lambda$-abstractions, tuple patterns can be used in
-most variable binding constructs. Typical examples are
-\begin{quote}
-\isa{let\ {\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isacharequal}\ f\ z\ in\ {\isacharparenleft}y{\isacharcomma}\ x{\isacharparenright}}\\
-\isa{case\ xs\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ {\isadigit{0}}\ {\isacharbar}\ {\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isacharhash}\ zs\ {\isasymRightarrow}\ x\ {\isacharplus}\ y}
-\end{quote}
-Further important examples are quantifiers and sets (see~\S\ref{quant-pats}).%
+There is also the type \isaindexbold{unit}, which contains exactly one
+element denoted by \ttindexboldpos{()}{$Isatype}. This type can be viewed
+as a degenerate Cartesian product of 0 types.
+
+Note that products, like type \isa{nat}, are datatypes, which means
+in particular that \isa{induct{\isacharunderscore}tac} and \isa{case{\isacharunderscore}tac} are applicable to
+products (see \S\ref{sec:products}).
+
+Instead of tuples with many components (where ``many'' is not much above 2),
+it is far preferable to use records (see \S\ref{sec:records}).%
\end{isamarkuptext}%
\end{isabellebody}%
%%% Local Variables:
--- a/doc-src/TutorialI/Misc/natsum.thy Wed Nov 29 10:22:38 2000 +0100
+++ b/doc-src/TutorialI/Misc/natsum.thy Wed Nov 29 13:44:26 2000 +0100
@@ -7,7 +7,7 @@
primitive recursion, for example
*}
-consts sum :: "nat \\<Rightarrow> nat";
+consts sum :: "nat \<Rightarrow> nat";
primrec "sum 0 = 0"
"sum (Suc n) = Suc n + sum n";
@@ -20,6 +20,85 @@
apply(auto);
done
+text{*\newcommand{\mystar}{*%
+}
+The usual arithmetic operations \ttindexboldpos{+}{$HOL2arithfun},
+\ttindexboldpos{-}{$HOL2arithfun}, \ttindexboldpos{\mystar}{$HOL2arithfun},
+\isaindexbold{div}, \isaindexbold{mod}, \isaindexbold{min} and
+\isaindexbold{max} are predefined, as are the relations
+\indexboldpos{\isasymle}{$HOL2arithrel} and
+\ttindexboldpos{<}{$HOL2arithrel}. There is even a least number operation
+\isaindexbold{LEAST}. For example, @{prop"(LEAST n. 1 < n) = 2"}, although
+Isabelle does not prove this completely automatically. 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{nat-numerals}.
+
+\begin{warn}
+ The constant \ttindexbold{0} and the operations
+ \ttindexboldpos{+}{$HOL2arithfun}, \ttindexboldpos{-}{$HOL2arithfun},
+ \ttindexboldpos{\mystar}{$HOL2arithfun}, \isaindexbold{min},
+ \isaindexbold{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 (see
+ \S\ref{sec:overloading}). 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
+ @{prop"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.
+\end{warn}
+
+Simple arithmetic goals are proved automatically by both @{term auto} and the
+simplification methods introduced in \S\ref{sec:Simplification}. For
+example,
+*}
+
+lemma "\<lbrakk> \<not> m < n; m < n+1 \<rbrakk> \<Longrightarrow> m = n"
+(*<*)by(auto)(*>*)
+
+text{*\noindent
+is proved automatically. The main restriction is that only addition is taken
+into account; other arithmetic operations and quantified formulae are ignored.
+
+For more complex goals, there is the special method \isaindexbold{arith}
+(which attacks the first subgoal). It proves arithmetic goals involving the
+usual logical connectives (@{text"\<not>"}, @{text"\<and>"}, @{text"\<or>"},
+@{text"\<longrightarrow>"}), the relations @{text"\<le>"} and @{text"<"}, and the operations
+@{text"+"}, @{text"-"}, @{term min} and @{term max}. For example,
+*}
+
+lemma "min i (max j (k*k)) = max (min (k*k) i) (min i (j::nat))";
+apply(arith)
+(*<*)done(*>*)
+
+text{*\noindent
+succeeds because @{term"k*k"} can be treated as atomic. In contrast,
+*}
+
+lemma "n*n = n \<Longrightarrow> n=0 \<or> n=1"
+(*<*)oops(*>*)
+
+text{*\noindent
+is not even proved by @{text arith} because the proof relies essentially
+on properties of multiplication.
+
+\begin{warn}
+ The running time of @{text arith} is exponential in the number of occurrences
+ of \ttindexboldpos{-}{$HOL2arithfun}, \isaindexbold{min} and
+ \isaindexbold{max} because they are first eliminated by case distinctions.
+
+ \isa{arith} is incomplete even for the restricted class of formulae
+ described above (known as ``linear arithmetic''). If divisibility plays a
+ role, it may fail to prove a valid formula, for example
+ @{prop"m+m \<noteq> n+n+1"}. Fortunately, such examples are rare in practice.
+\end{warn}
+*}
+
(*<*)
end
(*>*)
--- a/doc-src/TutorialI/Misc/pairs.thy Wed Nov 29 10:22:38 2000 +0100
+++ b/doc-src/TutorialI/Misc/pairs.thy Wed Nov 29 13:44:26 2000 +0100
@@ -1,26 +1,28 @@
(*<*)
theory pairs = Main:;
(*>*)
-text{*
+text{*\label{sec:pairs}\indexbold{product type}
+\index{pair|see{product type}}\index{tuple|see{product type}}
HOL also has pairs: \isa{($a@1$,$a@2$)} is of type $\tau@1$
-\indexboldpos{\isasymtimes}{$IsaFun} $\tau@2$ provided each $a@i$ is of type
-$\tau@i$. The components of a pair are extracted by @{term"fst"} and
-@{term"snd"}: \isa{fst($x$,$y$) = $x$} and \isa{snd($x$,$y$) = $y$}. Tuples
+\indexboldpos{\isasymtimes}{$Isatype} $\tau@2$ provided each $a@i$ is of type
+$\tau@i$. The components of a pair are extracted by \isaindexbold{fst} and
+\isaindexbold{snd}:
+ \isa{fst($x$,$y$) = $x$} and \isa{snd($x$,$y$) = $y$}. Tuples
are simulated by pairs nested to the right: \isa{($a@1$,$a@2$,$a@3$)} stands
for \isa{($a@1$,($a@2$,$a@3$))} and $\tau@1 \times \tau@2 \times \tau@3$ for
$\tau@1 \times (\tau@2 \times \tau@3)$. Therefore we have
\isa{fst(snd($a@1$,$a@2$,$a@3$)) = $a@2$}.
-It is possible to use (nested) tuples as patterns in abstractions, for
-example \isa{\isasymlambda(x,y,z).x+y+z} and
-\isa{\isasymlambda((x,y),z).x+y+z}.
-In addition to explicit $\lambda$-abstractions, tuple patterns can be used in
-most variable binding constructs. Typical examples are
-\begin{quote}
-@{term"let (x,y) = f z in (y,x)"}\\
-@{term"case xs of [] => 0 | (x,y)#zs => x+y"}
-\end{quote}
-Further important examples are quantifiers and sets (see~\S\ref{quant-pats}).
+There is also the type \isaindexbold{unit}, which contains exactly one
+element denoted by \ttindexboldpos{()}{$Isatype}. This type can be viewed
+as a degenerate Cartesian product of 0 types.
+
+Note that products, like type @{typ nat}, are datatypes, which means
+in particular that @{text induct_tac} and @{text case_tac} are applicable to
+products (see \S\ref{sec:products}).
+
+Instead of tuples with many components (where ``many'' is not much above 2),
+it is far preferable to use records (see \S\ref{sec:records}).
*}
(*<*)
end
--- a/doc-src/TutorialI/Types/Overloading0.thy Wed Nov 29 10:22:38 2000 +0100
+++ b/doc-src/TutorialI/Types/Overloading0.thy Wed Nov 29 13:44:26 2000 +0100
@@ -25,18 +25,19 @@
Isabelle will not complain because the three definitions do not overlap: no
two of the three types @{typ bool}, @{typ"'a set"} and @{typ"'a \<times> 'b"} have a
common instance. What is more, the recursion in @{thm[source]inverse_pair} is
-benign because the type of @{term inverse} becomes smaller: on the left it is
-@{typ"'a \<times> 'b \<Rightarrow> 'a \<times> 'b"} but on the right @{typ"'a \<Rightarrow> 'a"} and @{typ"'b \<Rightarrow>
-'b"}. The annotation @{text"(overloaded)"} tells Isabelle that the definitions do
-intentionally define @{term inverse} only at instances of its declared type
-@{typ"'a \<Rightarrow> 'a"} --- this merely supresses warnings to that effect.
+benign because the type of @{term[source]inverse} becomes smaller: on the
+left it is @{typ"'a \<times> 'b \<Rightarrow> 'a \<times> 'b"} but on the right @{typ"'a \<Rightarrow> 'a"} and
+@{typ"'b \<Rightarrow> 'b"}. The annotation @{text"(overloaded)"} tells Isabelle that
+the definitions do intentionally define @{term[source]inverse} only at
+instances of its declared type @{typ"'a \<Rightarrow> 'a"} --- this merely supresses
+warnings to that effect.
However, there is nothing to prevent the user from forming terms such as
-@{term"inverse []"} and proving theorems as @{prop"inverse [] = inverse []"},
-although we never defined inverse on lists. We hasten to say that there is
-nothing wrong with such terms and theorems. But it would be nice if we could
-prevent their formation, simply because it is very likely that the user did
-not mean to write what he did. Thus he had better not waste his time pursuing
-it further. This requires the use of type classes.
+@{term[source]"inverse []"} and proving theorems as @{prop[source]"inverse []
+= inverse []"}, although we never defined inverse on lists. We hasten to say
+that there is nothing wrong with such terms and theorems. But it would be
+nice if we could prevent their formation, simply because it is very likely
+that the user did not mean to write what he did. Thus he had better not waste
+his time pursuing it further. This requires the use of type classes.
*}
(*<*)end(*>*)
--- a/doc-src/TutorialI/Types/ROOT.ML Wed Nov 29 10:22:38 2000 +0100
+++ b/doc-src/TutorialI/Types/ROOT.ML Wed Nov 29 13:44:26 2000 +0100
@@ -1,4 +1,5 @@
use "../settings.ML";
+use_thy "Pairs";
use_thy "Typedef";
use_thy "Overloading0";
use_thy "Overloading2";
--- a/doc-src/TutorialI/Types/document/Overloading0.tex Wed Nov 29 10:22:38 2000 +0100
+++ b/doc-src/TutorialI/Types/document/Overloading0.tex Wed Nov 29 13:44:26 2000 +0100
@@ -29,18 +29,19 @@
Isabelle will not complain because the three definitions do not overlap: no
two of the three types \isa{bool}, \isa{{\isacharprime}a\ set} and \isa{{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b} have a
common instance. What is more, the recursion in \isa{inverse{\isacharunderscore}pair} is
-benign because the type of \isa{Overloading{\isadigit{0}}{\isachardot}inverse} becomes smaller: on the left it is
-\isa{{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b} but on the right \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} and \isa{{\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}b}. The annotation \isa{{\isacharparenleft}overloaded{\isacharparenright}} tells Isabelle that the definitions do
-intentionally define \isa{Overloading{\isadigit{0}}{\isachardot}inverse} only at instances of its declared type
-\isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} --- this merely supresses warnings to that effect.
+benign because the type of \isa{inverse} becomes smaller: on the
+left it is \isa{{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b} but on the right \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} and
+\isa{{\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}b}. The annotation \isa{{\isacharparenleft}overloaded{\isacharparenright}} tells Isabelle that
+the definitions do intentionally define \isa{inverse} only at
+instances of its declared type \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} --- this merely supresses
+warnings to that effect.
However, there is nothing to prevent the user from forming terms such as
-\isa{Overloading{\isadigit{0}}{\isachardot}inverse\ {\isacharbrackleft}{\isacharbrackright}} and proving theorems as \isa{Overloading{\isadigit{0}}{\isachardot}inverse\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ Overloading{\isadigit{0}}{\isachardot}inverse\ {\isacharbrackleft}{\isacharbrackright}},
-although we never defined inverse on lists. We hasten to say that there is
-nothing wrong with such terms and theorems. But it would be nice if we could
-prevent their formation, simply because it is very likely that the user did
-not mean to write what he did. Thus he had better not waste his time pursuing
-it further. This requires the use of type classes.%
+\isa{{\isachardoublequote}inverse\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequote}} and proving theorems as \isa{{\isachardoublequote}inverse\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ inverse\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequote}}, although we never defined inverse on lists. We hasten to say
+that there is nothing wrong with such terms and theorems. But it would be
+nice if we could prevent their formation, simply because it is very likely
+that the user did not mean to write what he did. Thus he had better not waste
+his time pursuing it further. This requires the use of type classes.%
\end{isamarkuptext}%
\end{isabellebody}%
%%% Local Variables:
--- a/doc-src/TutorialI/Types/types.tex Wed Nov 29 10:22:38 2000 +0100
+++ b/doc-src/TutorialI/Types/types.tex Wed Nov 29 13:44:26 2000 +0100
@@ -6,25 +6,23 @@
advanced material:
\begin{itemize}
\item More about basic types: numbers ({\S}\ref{sec:numbers}), pairs
- ({\S}\ref{sec:products}) and records ({\S}\ref{sec:records}), and how to reason
- about them.
+ ({\S}\ref{sec:products}) and records ({\S}\ref{sec:records}), and how to
+ reason about them.
\item Introducing your own types: how to introduce your own new types that
- cannot be constructed with any of the basic methods ({\S}\ref{sec:adv-typedef}).
+ cannot be constructed with any of the basic methods
+ ({\S}\ref{sec:adv-typedef}).
\item Type classes: how to specify and reason about axiomatic collections of
types ({\S}\ref{sec:axclass}).
\end{itemize}
-\section{Basic types}
-
-\subsection{Numbers}
+\section{Numbers}
\label{sec:numbers}
-\subsection{Pairs}
-\label{sec:products}
+\input{Types/document/Pairs}
% Check refs to this section to see what is expected of it.
% Mention type unit
-\subsection{Records}
+\section{Records}
\label{sec:records}
\input{Types/document/Typedef}
--- a/doc-src/TutorialI/appendix.tex Wed Nov 29 10:22:38 2000 +0100
+++ b/doc-src/TutorialI/appendix.tex Wed Nov 29 13:44:26 2000 +0100
@@ -61,7 +61,7 @@
\indexboldpos{\isasymle}{$HOL2arithrel}&
\ttindexboldpos{<=}{$HOL2arithrel}&
\verb$\<le>$\\
-\indexboldpos{\isasymtimes}{$IsaFun}&
+\indexboldpos{\isasymtimes}{$Isatype}&
\ttindexboldpos{*}{$HOL2arithfun} &
\verb$\<times>$\\
\indexboldpos{\isasymin}{$HOL3Set0a}&
--- a/doc-src/TutorialI/basics.tex Wed Nov 29 10:22:38 2000 +0100
+++ b/doc-src/TutorialI/basics.tex Wed Nov 29 13:44:26 2000 +0100
@@ -102,7 +102,7 @@
which abbreviates \isa{$\tau@1$ \isasymFun~$\cdots$ \isasymFun~$\tau@n$
\isasymFun~$\tau$}.
\item[type variables,]\indexbold{type variable}\indexbold{variable!type}
- denoted by \isaindexbold{'a}, \isa{'b} etc., just like in ML. They give rise
+ denoted by \ttindexboldpos{'a}{$Isatype}, \isa{'b} etc., just like in ML. They give rise
to polymorphic types like \isa{'a \isasymFun~'a}, the type of the identity
function.
\end{description}
@@ -183,10 +183,10 @@
Despite type inference, it is sometimes necessary to attach explicit
\textbf{type constraints}\indexbold{type constraint} to a term. The syntax is
\isa{$t$::$\tau$} as in \isa{x < (y::nat)}. Note that
-\ttindexboldpos{::}{$Isalamtc} binds weakly and should therefore be enclosed
+\ttindexboldpos{::}{$Isatype} binds weakly and should therefore be enclosed
in parentheses: \isa{x < y::nat} is ill-typed because it is interpreted as
\isa{(x < y)::nat}. The main reason for type constraints are overloaded
-functions like \isa{+}, \isa{*} and \isa{<}. See \S\ref{sec:overloading} for
+functions like \isa{+}, \isa{*} and \isa{<}. See {\S}\ref{sec:overloading} for
a full discussion of overloading.
\begin{warn}
--- a/doc-src/TutorialI/fp.tex Wed Nov 29 10:22:38 2000 +0100
+++ b/doc-src/TutorialI/fp.tex Wed Nov 29 13:44:26 2000 +0100
@@ -186,7 +186,7 @@
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
+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, \isaindexbold{size} returns \isa{0} for all constructors
that do not have an argument of type $t$, and for all other constructors
@@ -209,7 +209,7 @@
becomes smaller with every recursive call. There must be exactly one equation
for each constructor. Their order is immaterial.
A more general method for defining total recursive functions is introduced in
-\S\ref{sec:recdef}.
+{\S}\ref{sec:recdef}.
\begin{exercise}\label{ex:Tree}
\input{Misc/document/Tree.tex}%
@@ -220,7 +220,7 @@
\begin{warn}
Induction is only allowed on free (or \isasymAnd-bound) variables that
should not occur among the assumptions of the subgoal; see
- \S\ref{sec:ind-var-in-prems} for details. Case distinction
+ {\S}\ref{sec:ind-var-in-prems} for details. Case distinction
(\isa{case_tac}) works for arbitrary terms, which need to be
quoted if they are non-atomic.
\end{warn}
@@ -238,94 +238,12 @@
\input{Misc/document/fakenat.tex}
\input{Misc/document/natsum.tex}
-The usual arithmetic operations \ttindexboldpos{+}{$HOL2arithfun},
-\ttindexboldpos{-}{$HOL2arithfun}, \ttindexboldpos{*}{$HOL2arithfun},
-\isaindexbold{div}, \isaindexbold{mod}, \isaindexbold{min} and
-\isaindexbold{max} are predefined, as are the relations
-\indexboldpos{\isasymle}{$HOL2arithrel} and
-\ttindexboldpos{<}{$HOL2arithrel}. There is even a least number operation
-\isaindexbold{LEAST}. For example, \isa{(LEAST n.$\,$1 < n) = 2}, although
-Isabelle does not prove this completely automatically. Note that \isa{1} and
-\isa{2} are available as abbreviations for the corresponding
-\isa{Suc}-expressions. If you need the full set of numerals,
-see~\S\ref{nat-numerals}.
-
-\begin{warn}
- The constant \ttindexbold{0} and the operations
- \ttindexboldpos{+}{$HOL2arithfun}, \ttindexboldpos{-}{$HOL2arithfun},
- \ttindexboldpos{*}{$HOL2arithfun}, \isaindexbold{min}, \isaindexbold{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 (see
- \S\ref{sec:overloading}). For example, given the goal \isa{x+0 = 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{0} and \isa{+} 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 \texttt{show_types} is not set). In this particular example,
- you need to include an explicit type constraint, for example \isa{x+0 =
- (x::nat)}. If there is enough contextual information this may not be
- necessary: \isa{Suc x = x} automatically implies \isa{x::nat} because
- \isa{Suc} is not overloaded.
-\end{warn}
-
-Simple arithmetic goals are proved automatically by both \isa{auto}
-and the simplification methods introduced in \S\ref{sec:Simplification}. For
-example,
-
-\input{Misc/document/arith1.tex}%
-is proved automatically. The main restriction is that only addition is taken
-into account; other arithmetic operations and quantified formulae are ignored.
-
-For more complex goals, there is the special method
-\isaindexbold{arith} (which attacks the first subgoal). It proves
-arithmetic goals involving the usual logical connectives (\isasymnot,
-\isasymand, \isasymor, \isasymimp), the relations \isasymle\ and \isa{<}, and
-the operations \isa{+}, \isa{-}, \isa{min} and \isa{max}. For example,
-
-\input{Misc/document/arith2.tex}%
-succeeds because \isa{k*k} can be treated as atomic.
-In contrast,
-
-\input{Misc/document/arith3.tex}%
-is not even proved by \isa{arith} because the proof relies essentially
-on properties of multiplication.
-
-\begin{warn}
- The running time of \isa{arith} is exponential in the number of occurrences
- of \ttindexboldpos{-}{$HOL2arithfun}, \isaindexbold{min} and
- \isaindexbold{max} because they are first eliminated by case distinctions.
-
- \isa{arith} is incomplete even for the restricted class of formulae
- described above (known as ``linear arithmetic''). If divisibility plays a
- role, it may fail to prove a valid formula, for example $m+m \neq n+n+1$.
- Fortunately, such examples are rare in practice.
-\end{warn}
-
\index{arithmetic|)}
\subsection{Pairs}
\input{Misc/document/pairs.tex}
-%FIXME move stuff below into section on proofs about products?
-\begin{warn}
- Abstraction over pairs and tuples is merely a convenient shorthand for a
- more complex internal representation. Thus the internal and external form
- of a term may differ, which can affect proofs. If you want to avoid this
- complication, use \isa{fst} and \isa{snd}, i.e.\ write
- \isa{\isasymlambda{}p.~fst p + snd p} instead of
- \isa{\isasymlambda(x,y).~x + y}. See~\S\ref{sec:products} for
- theorem proving with tuple patterns.
-\end{warn}
-
-Note that products, like type \isa{nat}, are datatypes, which means
-in particular that \isa{induct_tac} and \isa{case_tac} are applicable to
-products (see \S\ref{sec:products}).
-
-Instead of tuples with many components (where ``many'' is not much above 2),
-it is far preferable to use records (see \S\ref{sec:records}).
-
\section{Definitions}
\label{sec:Definitions}
@@ -346,7 +264,7 @@
Note that pattern-matching is not allowed, i.e.\ each definition must be of
the form $f\,x@1\,\dots\,x@n~\isasymequiv~t$.
-Section~\S\ref{sec:Simplification} explains how definitions are used
+Section~{\S}\ref{sec:Simplification} explains how definitions are used
in proofs.
\input{Misc/document/prime_def.tex}
@@ -357,15 +275,15 @@
The purpose of this chapter is to deepen the reader's understanding of the
concepts encountered so far and to introduce advanced forms of datatypes and
recursive functions. The first two sections give a structured presentation of
-theorem proving by simplification (\S\ref{sec:Simplification}) and discuss
-important heuristics for induction (\S\ref{sec:InductionHeuristics}). They can
+theorem proving by simplification ({\S}\ref{sec:Simplification}) and discuss
+important heuristics for induction ({\S}\ref{sec:InductionHeuristics}). They can
be skipped by readers less interested in proofs. They are followed by a case
-study, a compiler for expressions (\S\ref{sec:ExprCompiler}). Advanced
+study, a compiler for expressions ({\S}\ref{sec:ExprCompiler}). Advanced
datatypes, including those involving function spaces, are covered in
-\S\ref{sec:advanced-datatypes}, which closes with another case study, search
+{\S}\ref{sec:advanced-datatypes}, which closes with another case study, search
trees (``tries''). Finally we introduce \isacommand{recdef}, a very general
form of recursive function definition which goes well beyond what
-\isacommand{primrec} allows (\S\ref{sec:recdef}).
+\isacommand{primrec} allows ({\S}\ref{sec:recdef}).
\section{Simplification}
@@ -382,7 +300,7 @@
many other systems. The tool itself is called the \bfindex{simplifier}. The
purpose of this section is introduce the many features of the simplifier.
Anybody intending to use HOL should read this section. Later on
-(\S\ref{sec:simplification-II}) we explain some more advanced features and a
+({\S}\ref{sec:simplification-II}) we explain some more advanced features and a
little bit of how the simplifier works. The serious student should read that
section as well, in particular in order to understand what happened if things
do not simplify as expected.
@@ -550,7 +468,7 @@
recursion need not involve datatypes, and termination is proved by showing
that the arguments of all recursive calls are smaller in a suitable (user
supplied) sense. In this section we ristrict ourselves to measure functions;
-more advanced termination proofs are discussed in \S\ref{sec:beyond-measure}.
+more advanced termination proofs are discussed in {\S}\ref{sec:beyond-measure}.
\subsection{Defining recursive functions}