author | nipkow |

Wed Nov 29 13:44:26 2000 +0100 (2000-11-29) | |

changeset 10538 | d1bf9ca9008d |

parent 10537 | 1d2f15504d38 |

child 10539 | 5929460a41df |

*** empty log message ***

1.1 --- a/doc-src/TutorialI/IsaMakefile Wed Nov 29 10:22:38 2000 +0100 1.2 +++ b/doc-src/TutorialI/IsaMakefile Wed Nov 29 13:44:26 2000 +0100 1.3 @@ -142,7 +142,8 @@ 1.4 1.5 HOL-Types: HOL $(LOG)/HOL-Types.gz 1.6 1.7 -$(LOG)/HOL-Types.gz: $(OUT)/HOL Types/ROOT.ML Types/Typedef.thy \ 1.8 +$(LOG)/HOL-Types.gz: $(OUT)/HOL Types/ROOT.ML Types/Pairs.thy \ 1.9 + Types/Typedef.thy \ 1.10 Types/Overloading0.thy Types/Overloading1.thy Types/Overloading2.thy \ 1.11 Types/Overloading.thy Types/Axioms.thy 1.12 @$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL Types 1.13 @@ -155,7 +156,6 @@ 1.14 $(LOG)/HOL-Misc.gz: $(OUT)/HOL Misc/ROOT.ML Misc/Tree.thy Misc/Tree2.thy \ 1.15 Misc/fakenat.thy Misc/natsum.thy Misc/pairs.thy Misc/types.thy \ 1.16 Misc/prime_def.thy Misc/case_exprs.thy \ 1.17 - Misc/arith1.thy Misc/arith2.thy Misc/arith3.thy \ 1.18 Misc/simp.thy Misc/Itrev.thy Misc/AdvancedInd.thy 1.19 @$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL Misc 1.20 @rm -f tutorial.dvi

2.1 --- a/doc-src/TutorialI/Misc/ROOT.ML Wed Nov 29 10:22:38 2000 +0100 2.2 +++ b/doc-src/TutorialI/Misc/ROOT.ML Wed Nov 29 13:44:26 2000 +0100 2.3 @@ -4,9 +4,6 @@ 2.4 use_thy "case_exprs"; 2.5 use_thy "fakenat"; 2.6 use_thy "natsum"; 2.7 -use_thy "arith1"; 2.8 -use_thy "arith2"; 2.9 -use_thy "arith3"; 2.10 use_thy "pairs"; 2.11 use_thy "types"; 2.12 use_thy "prime_def";

3.1 --- a/doc-src/TutorialI/Misc/arith1.thy Wed Nov 29 10:22:38 2000 +0100 3.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 3.3 @@ -1,8 +0,0 @@ 3.4 -(*<*) 3.5 -theory arith1 = Main:; 3.6 -(*>*) 3.7 -lemma "\<lbrakk> \<not> m < n; m < n+1 \<rbrakk> \<Longrightarrow> m = n"; 3.8 -(**)(*<*) 3.9 -by(auto); 3.10 -end 3.11 -(*>*)

4.1 --- a/doc-src/TutorialI/Misc/arith2.thy Wed Nov 29 10:22:38 2000 +0100 4.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 4.3 @@ -1,9 +0,0 @@ 4.4 -(*<*) 4.5 -theory arith2 = Main:; 4.6 -(*>*) 4.7 -lemma "min i (max j (k*k)) = max (min (k*k) i) (min i (j::nat))"; 4.8 -apply(arith); 4.9 -(**)(*<*) 4.10 -done 4.11 -end 4.12 -(*>*)

5.1 --- a/doc-src/TutorialI/Misc/arith3.thy Wed Nov 29 10:22:38 2000 +0100 5.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 5.3 @@ -1,8 +0,0 @@ 5.4 -(*<*) 5.5 -theory arith3 = Main:; 5.6 -(*>*) 5.7 -lemma "n*n = n \\<Longrightarrow> n=0 \\<or> n=1"; 5.8 -(**)(*<*) 5.9 -oops; 5.10 -end 5.11 -(*>*)

6.1 --- a/doc-src/TutorialI/Misc/document/arith1.tex Wed Nov 29 10:22:38 2000 +0100 6.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 6.3 @@ -1,9 +0,0 @@ 6.4 -% 6.5 -\begin{isabellebody}% 6.6 -\def\isabellecontext{arith{\isadigit{1}}}% 6.7 -\isacommand{lemma}\ {\isachardoublequote}{\isasymlbrakk}\ {\isasymnot}\ m\ {\isacharless}\ n{\isacharsemicolon}\ m\ {\isacharless}\ n{\isacharplus}{\isadigit{1}}\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ m\ {\isacharequal}\ n{\isachardoublequote}\isanewline 6.8 -\end{isabellebody}% 6.9 -%%% Local Variables: 6.10 -%%% mode: latex 6.11 -%%% TeX-master: "root" 6.12 -%%% End:

7.1 --- a/doc-src/TutorialI/Misc/document/arith2.tex Wed Nov 29 10:22:38 2000 +0100 7.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 7.3 @@ -1,10 +0,0 @@ 7.4 -% 7.5 -\begin{isabellebody}% 7.6 -\def\isabellecontext{arith{\isadigit{2}}}% 7.7 -\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 7.8 -\isacommand{apply}{\isacharparenleft}arith{\isacharparenright}\isanewline 7.9 -\end{isabellebody}% 7.10 -%%% Local Variables: 7.11 -%%% mode: latex 7.12 -%%% TeX-master: "root" 7.13 -%%% End:

8.1 --- a/doc-src/TutorialI/Misc/document/arith3.tex Wed Nov 29 10:22:38 2000 +0100 8.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 8.3 @@ -1,9 +0,0 @@ 8.4 -% 8.5 -\begin{isabellebody}% 8.6 -\def\isabellecontext{arith{\isadigit{3}}}% 8.7 -\isacommand{lemma}\ {\isachardoublequote}n{\isacharasterisk}n\ {\isacharequal}\ n\ {\isasymLongrightarrow}\ n{\isacharequal}{\isadigit{0}}\ {\isasymor}\ n{\isacharequal}{\isadigit{1}}{\isachardoublequote}\isanewline 8.8 -\end{isabellebody}% 8.9 -%%% Local Variables: 8.10 -%%% mode: latex 8.11 -%%% TeX-master: "root" 8.12 -%%% End:

9.1 --- a/doc-src/TutorialI/Misc/document/natsum.tex Wed Nov 29 10:22:38 2000 +0100 9.2 +++ b/doc-src/TutorialI/Misc/document/natsum.tex Wed Nov 29 13:44:26 2000 +0100 9.3 @@ -20,7 +20,80 @@ 9.4 \isacommand{lemma}\ {\isachardoublequote}sum\ n\ {\isacharplus}\ sum\ n\ {\isacharequal}\ n{\isacharasterisk}{\isacharparenleft}Suc\ n{\isacharparenright}{\isachardoublequote}\isanewline 9.5 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ n{\isacharparenright}\isanewline 9.6 \isacommand{apply}{\isacharparenleft}auto{\isacharparenright}\isanewline 9.7 -\isacommand{done}\isanewline 9.8 +\isacommand{done}% 9.9 +\begin{isamarkuptext}% 9.10 +\newcommand{\mystar}{*% 9.11 +} 9.12 +The usual arithmetic operations \ttindexboldpos{+}{$HOL2arithfun}, 9.13 +\ttindexboldpos{-}{$HOL2arithfun}, \ttindexboldpos{\mystar}{$HOL2arithfun}, 9.14 +\isaindexbold{div}, \isaindexbold{mod}, \isaindexbold{min} and 9.15 +\isaindexbold{max} are predefined, as are the relations 9.16 +\indexboldpos{\isasymle}{$HOL2arithrel} and 9.17 +\ttindexboldpos{<}{$HOL2arithrel}. There is even a least number operation 9.18 +\isaindexbold{LEAST}. For example, \isa{{\isacharparenleft}LEAST\ n{\isachardot}\ {\isadigit{1}}\ {\isacharless}\ n{\isacharparenright}\ {\isacharequal}\ {\isadigit{2}}}, although 9.19 +Isabelle does not prove this completely automatically. Note that \isa{{\isadigit{1}}} 9.20 +and \isa{{\isadigit{2}}} are available as abbreviations for the corresponding 9.21 +\isa{Suc}-expressions. If you need the full set of numerals, 9.22 +see~\S\ref{nat-numerals}. 9.23 + 9.24 +\begin{warn} 9.25 + The constant \ttindexbold{0} and the operations 9.26 + \ttindexboldpos{+}{$HOL2arithfun}, \ttindexboldpos{-}{$HOL2arithfun}, 9.27 + \ttindexboldpos{\mystar}{$HOL2arithfun}, \isaindexbold{min}, 9.28 + \isaindexbold{max}, \indexboldpos{\isasymle}{$HOL2arithrel} and 9.29 + \ttindexboldpos{<}{$HOL2arithrel} are overloaded, i.e.\ they are available 9.30 + not just for natural numbers but at other types as well (see 9.31 + \S\ref{sec:overloading}). For example, given the goal \isa{x\ {\isacharplus}\ {\isadigit{0}}\ {\isacharequal}\ x}, 9.32 + there is nothing to indicate that you are talking about natural numbers. 9.33 + Hence Isabelle can only infer that \isa{x} is of some arbitrary type where 9.34 + \isa{{\isadigit{0}}} and \isa{{\isacharplus}} are declared. As a consequence, you will be unable 9.35 + to prove the goal (although it may take you some time to realize what has 9.36 + happened if \isa{show{\isacharunderscore}types} is not set). In this particular example, 9.37 + you need to include an explicit type constraint, for example 9.38 + \isa{x\ {\isacharplus}\ {\isadigit{0}}\ {\isacharequal}\ x}. If there is enough contextual information this 9.39 + may not be necessary: \isa{Suc\ x\ {\isacharequal}\ x} automatically implies 9.40 + \isa{x{\isacharcolon}{\isacharcolon}nat} because \isa{Suc} is not overloaded. 9.41 +\end{warn} 9.42 + 9.43 +Simple arithmetic goals are proved automatically by both \isa{auto} and the 9.44 +simplification methods introduced in \S\ref{sec:Simplification}. For 9.45 +example,% 9.46 +\end{isamarkuptext}% 9.47 +\isacommand{lemma}\ {\isachardoublequote}{\isasymlbrakk}\ {\isasymnot}\ m\ {\isacharless}\ n{\isacharsemicolon}\ m\ {\isacharless}\ n{\isacharplus}{\isadigit{1}}\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ m\ {\isacharequal}\ n{\isachardoublequote}% 9.48 +\begin{isamarkuptext}% 9.49 +\noindent 9.50 +is proved automatically. The main restriction is that only addition is taken 9.51 +into account; other arithmetic operations and quantified formulae are ignored. 9.52 + 9.53 +For more complex goals, there is the special method \isaindexbold{arith} 9.54 +(which attacks the first subgoal). It proves arithmetic goals involving the 9.55 +usual logical connectives (\isa{{\isasymnot}}, \isa{{\isasymand}}, \isa{{\isasymor}}, 9.56 +\isa{{\isasymlongrightarrow}}), the relations \isa{{\isasymle}} and \isa{{\isacharless}}, and the operations 9.57 +\isa{{\isacharplus}}, \isa{{\isacharminus}}, \isa{min} and \isa{max}. For example,% 9.58 +\end{isamarkuptext}% 9.59 +\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 9.60 +\isacommand{apply}{\isacharparenleft}arith{\isacharparenright}% 9.61 +\begin{isamarkuptext}% 9.62 +\noindent 9.63 +succeeds because \isa{k\ {\isacharasterisk}\ k} can be treated as atomic. In contrast,% 9.64 +\end{isamarkuptext}% 9.65 +\isacommand{lemma}\ {\isachardoublequote}n{\isacharasterisk}n\ {\isacharequal}\ n\ {\isasymLongrightarrow}\ n{\isacharequal}{\isadigit{0}}\ {\isasymor}\ n{\isacharequal}{\isadigit{1}}{\isachardoublequote}% 9.66 +\begin{isamarkuptext}% 9.67 +\noindent 9.68 +is not even proved by \isa{arith} because the proof relies essentially 9.69 +on properties of multiplication. 9.70 + 9.71 +\begin{warn} 9.72 + The running time of \isa{arith} is exponential in the number of occurrences 9.73 + of \ttindexboldpos{-}{$HOL2arithfun}, \isaindexbold{min} and 9.74 + \isaindexbold{max} because they are first eliminated by case distinctions. 9.75 + 9.76 + \isa{arith} is incomplete even for the restricted class of formulae 9.77 + described above (known as ``linear arithmetic''). If divisibility plays a 9.78 + role, it may fail to prove a valid formula, for example 9.79 + \isa{m\ {\isacharplus}\ m\ {\isasymnoteq}\ n\ {\isacharplus}\ n\ {\isacharplus}\ {\isadigit{1}}}. Fortunately, such examples are rare in practice. 9.80 +\end{warn}% 9.81 +\end{isamarkuptext}% 9.82 \end{isabellebody}% 9.83 %%% Local Variables: 9.84 %%% mode: latex

10.1 --- a/doc-src/TutorialI/Misc/document/pairs.tex Wed Nov 29 10:22:38 2000 +0100 10.2 +++ b/doc-src/TutorialI/Misc/document/pairs.tex Wed Nov 29 13:44:26 2000 +0100 10.3 @@ -3,25 +3,28 @@ 10.4 \def\isabellecontext{pairs}% 10.5 % 10.6 \begin{isamarkuptext}% 10.7 +\label{sec:pairs}\indexbold{product type} 10.8 +\index{pair|see{product type}}\index{tuple|see{product type}} 10.9 HOL also has pairs: \isa{($a@1$,$a@2$)} is of type $\tau@1$ 10.10 -\indexboldpos{\isasymtimes}{$IsaFun} $\tau@2$ provided each $a@i$ is of type 10.11 -$\tau@i$. The components of a pair are extracted by \isa{fst} and 10.12 -\isa{snd}: \isa{fst($x$,$y$) = $x$} and \isa{snd($x$,$y$) = $y$}. Tuples 10.13 +\indexboldpos{\isasymtimes}{$Isatype} $\tau@2$ provided each $a@i$ is of type 10.14 +$\tau@i$. The components of a pair are extracted by \isaindexbold{fst} and 10.15 +\isaindexbold{snd}: 10.16 + \isa{fst($x$,$y$) = $x$} and \isa{snd($x$,$y$) = $y$}. Tuples 10.17 are simulated by pairs nested to the right: \isa{($a@1$,$a@2$,$a@3$)} stands 10.18 for \isa{($a@1$,($a@2$,$a@3$))} and $\tau@1 \times \tau@2 \times \tau@3$ for 10.19 $\tau@1 \times (\tau@2 \times \tau@3)$. Therefore we have 10.20 \isa{fst(snd($a@1$,$a@2$,$a@3$)) = $a@2$}. 10.21 10.22 -It is possible to use (nested) tuples as patterns in abstractions, for 10.23 -example \isa{\isasymlambda(x,y,z).x+y+z} and 10.24 -\isa{\isasymlambda((x,y),z).x+y+z}. 10.25 -In addition to explicit $\lambda$-abstractions, tuple patterns can be used in 10.26 -most variable binding constructs. Typical examples are 10.27 -\begin{quote} 10.28 -\isa{let\ {\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isacharequal}\ f\ z\ in\ {\isacharparenleft}y{\isacharcomma}\ x{\isacharparenright}}\\ 10.29 -\isa{case\ xs\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ {\isadigit{0}}\ {\isacharbar}\ {\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isacharhash}\ zs\ {\isasymRightarrow}\ x\ {\isacharplus}\ y} 10.30 -\end{quote} 10.31 -Further important examples are quantifiers and sets (see~\S\ref{quant-pats}).% 10.32 +There is also the type \isaindexbold{unit}, which contains exactly one 10.33 +element denoted by \ttindexboldpos{()}{$Isatype}. This type can be viewed 10.34 +as a degenerate Cartesian product of 0 types. 10.35 + 10.36 +Note that products, like type \isa{nat}, are datatypes, which means 10.37 +in particular that \isa{induct{\isacharunderscore}tac} and \isa{case{\isacharunderscore}tac} are applicable to 10.38 +products (see \S\ref{sec:products}). 10.39 + 10.40 +Instead of tuples with many components (where ``many'' is not much above 2), 10.41 +it is far preferable to use records (see \S\ref{sec:records}).% 10.42 \end{isamarkuptext}% 10.43 \end{isabellebody}% 10.44 %%% Local Variables:

11.1 --- a/doc-src/TutorialI/Misc/natsum.thy Wed Nov 29 10:22:38 2000 +0100 11.2 +++ b/doc-src/TutorialI/Misc/natsum.thy Wed Nov 29 13:44:26 2000 +0100 11.3 @@ -7,7 +7,7 @@ 11.4 primitive recursion, for example 11.5 *} 11.6 11.7 -consts sum :: "nat \\<Rightarrow> nat"; 11.8 +consts sum :: "nat \<Rightarrow> nat"; 11.9 primrec "sum 0 = 0" 11.10 "sum (Suc n) = Suc n + sum n"; 11.11 11.12 @@ -20,6 +20,85 @@ 11.13 apply(auto); 11.14 done 11.15 11.16 +text{*\newcommand{\mystar}{*% 11.17 +} 11.18 +The usual arithmetic operations \ttindexboldpos{+}{$HOL2arithfun}, 11.19 +\ttindexboldpos{-}{$HOL2arithfun}, \ttindexboldpos{\mystar}{$HOL2arithfun}, 11.20 +\isaindexbold{div}, \isaindexbold{mod}, \isaindexbold{min} and 11.21 +\isaindexbold{max} are predefined, as are the relations 11.22 +\indexboldpos{\isasymle}{$HOL2arithrel} and 11.23 +\ttindexboldpos{<}{$HOL2arithrel}. There is even a least number operation 11.24 +\isaindexbold{LEAST}. For example, @{prop"(LEAST n. 1 < n) = 2"}, although 11.25 +Isabelle does not prove this completely automatically. Note that @{term 1} 11.26 +and @{term 2} are available as abbreviations for the corresponding 11.27 +@{term Suc}-expressions. If you need the full set of numerals, 11.28 +see~\S\ref{nat-numerals}. 11.29 + 11.30 +\begin{warn} 11.31 + The constant \ttindexbold{0} and the operations 11.32 + \ttindexboldpos{+}{$HOL2arithfun}, \ttindexboldpos{-}{$HOL2arithfun}, 11.33 + \ttindexboldpos{\mystar}{$HOL2arithfun}, \isaindexbold{min}, 11.34 + \isaindexbold{max}, \indexboldpos{\isasymle}{$HOL2arithrel} and 11.35 + \ttindexboldpos{<}{$HOL2arithrel} are overloaded, i.e.\ they are available 11.36 + not just for natural numbers but at other types as well (see 11.37 + \S\ref{sec:overloading}). For example, given the goal @{prop"x+0 = x"}, 11.38 + there is nothing to indicate that you are talking about natural numbers. 11.39 + Hence Isabelle can only infer that @{term x} is of some arbitrary type where 11.40 + @{term 0} and @{text"+"} are declared. As a consequence, you will be unable 11.41 + to prove the goal (although it may take you some time to realize what has 11.42 + happened if @{text show_types} is not set). In this particular example, 11.43 + you need to include an explicit type constraint, for example 11.44 + @{prop"x+0 = (x::nat)"}. If there is enough contextual information this 11.45 + may not be necessary: @{prop"Suc x = x"} automatically implies 11.46 + @{text"x::nat"} because @{term Suc} is not overloaded. 11.47 +\end{warn} 11.48 + 11.49 +Simple arithmetic goals are proved automatically by both @{term auto} and the 11.50 +simplification methods introduced in \S\ref{sec:Simplification}. For 11.51 +example, 11.52 +*} 11.53 + 11.54 +lemma "\<lbrakk> \<not> m < n; m < n+1 \<rbrakk> \<Longrightarrow> m = n" 11.55 +(*<*)by(auto)(*>*) 11.56 + 11.57 +text{*\noindent 11.58 +is proved automatically. The main restriction is that only addition is taken 11.59 +into account; other arithmetic operations and quantified formulae are ignored. 11.60 + 11.61 +For more complex goals, there is the special method \isaindexbold{arith} 11.62 +(which attacks the first subgoal). It proves arithmetic goals involving the 11.63 +usual logical connectives (@{text"\<not>"}, @{text"\<and>"}, @{text"\<or>"}, 11.64 +@{text"\<longrightarrow>"}), the relations @{text"\<le>"} and @{text"<"}, and the operations 11.65 +@{text"+"}, @{text"-"}, @{term min} and @{term max}. For example, 11.66 +*} 11.67 + 11.68 +lemma "min i (max j (k*k)) = max (min (k*k) i) (min i (j::nat))"; 11.69 +apply(arith) 11.70 +(*<*)done(*>*) 11.71 + 11.72 +text{*\noindent 11.73 +succeeds because @{term"k*k"} can be treated as atomic. In contrast, 11.74 +*} 11.75 + 11.76 +lemma "n*n = n \<Longrightarrow> n=0 \<or> n=1" 11.77 +(*<*)oops(*>*) 11.78 + 11.79 +text{*\noindent 11.80 +is not even proved by @{text arith} because the proof relies essentially 11.81 +on properties of multiplication. 11.82 + 11.83 +\begin{warn} 11.84 + The running time of @{text arith} is exponential in the number of occurrences 11.85 + of \ttindexboldpos{-}{$HOL2arithfun}, \isaindexbold{min} and 11.86 + \isaindexbold{max} because they are first eliminated by case distinctions. 11.87 + 11.88 + \isa{arith} is incomplete even for the restricted class of formulae 11.89 + described above (known as ``linear arithmetic''). If divisibility plays a 11.90 + role, it may fail to prove a valid formula, for example 11.91 + @{prop"m+m \<noteq> n+n+1"}. Fortunately, such examples are rare in practice. 11.92 +\end{warn} 11.93 +*} 11.94 + 11.95 (*<*) 11.96 end 11.97 (*>*)

12.1 --- a/doc-src/TutorialI/Misc/pairs.thy Wed Nov 29 10:22:38 2000 +0100 12.2 +++ b/doc-src/TutorialI/Misc/pairs.thy Wed Nov 29 13:44:26 2000 +0100 12.3 @@ -1,26 +1,28 @@ 12.4 (*<*) 12.5 theory pairs = Main:; 12.6 (*>*) 12.7 -text{* 12.8 +text{*\label{sec:pairs}\indexbold{product type} 12.9 +\index{pair|see{product type}}\index{tuple|see{product type}} 12.10 HOL also has pairs: \isa{($a@1$,$a@2$)} is of type $\tau@1$ 12.11 -\indexboldpos{\isasymtimes}{$IsaFun} $\tau@2$ provided each $a@i$ is of type 12.12 -$\tau@i$. The components of a pair are extracted by @{term"fst"} and 12.13 -@{term"snd"}: \isa{fst($x$,$y$) = $x$} and \isa{snd($x$,$y$) = $y$}. Tuples 12.14 +\indexboldpos{\isasymtimes}{$Isatype} $\tau@2$ provided each $a@i$ is of type 12.15 +$\tau@i$. The components of a pair are extracted by \isaindexbold{fst} and 12.16 +\isaindexbold{snd}: 12.17 + \isa{fst($x$,$y$) = $x$} and \isa{snd($x$,$y$) = $y$}. Tuples 12.18 are simulated by pairs nested to the right: \isa{($a@1$,$a@2$,$a@3$)} stands 12.19 for \isa{($a@1$,($a@2$,$a@3$))} and $\tau@1 \times \tau@2 \times \tau@3$ for 12.20 $\tau@1 \times (\tau@2 \times \tau@3)$. Therefore we have 12.21 \isa{fst(snd($a@1$,$a@2$,$a@3$)) = $a@2$}. 12.22 12.23 -It is possible to use (nested) tuples as patterns in abstractions, for 12.24 -example \isa{\isasymlambda(x,y,z).x+y+z} and 12.25 -\isa{\isasymlambda((x,y),z).x+y+z}. 12.26 -In addition to explicit $\lambda$-abstractions, tuple patterns can be used in 12.27 -most variable binding constructs. Typical examples are 12.28 -\begin{quote} 12.29 -@{term"let (x,y) = f z in (y,x)"}\\ 12.30 -@{term"case xs of [] => 0 | (x,y)#zs => x+y"} 12.31 -\end{quote} 12.32 -Further important examples are quantifiers and sets (see~\S\ref{quant-pats}). 12.33 +There is also the type \isaindexbold{unit}, which contains exactly one 12.34 +element denoted by \ttindexboldpos{()}{$Isatype}. This type can be viewed 12.35 +as a degenerate Cartesian product of 0 types. 12.36 + 12.37 +Note that products, like type @{typ nat}, are datatypes, which means 12.38 +in particular that @{text induct_tac} and @{text case_tac} are applicable to 12.39 +products (see \S\ref{sec:products}). 12.40 + 12.41 +Instead of tuples with many components (where ``many'' is not much above 2), 12.42 +it is far preferable to use records (see \S\ref{sec:records}). 12.43 *} 12.44 (*<*) 12.45 end

13.1 --- a/doc-src/TutorialI/Types/Overloading0.thy Wed Nov 29 10:22:38 2000 +0100 13.2 +++ b/doc-src/TutorialI/Types/Overloading0.thy Wed Nov 29 13:44:26 2000 +0100 13.3 @@ -25,18 +25,19 @@ 13.4 Isabelle will not complain because the three definitions do not overlap: no 13.5 two of the three types @{typ bool}, @{typ"'a set"} and @{typ"'a \<times> 'b"} have a 13.6 common instance. What is more, the recursion in @{thm[source]inverse_pair} is 13.7 -benign because the type of @{term inverse} becomes smaller: on the left it is 13.8 -@{typ"'a \<times> 'b \<Rightarrow> 'a \<times> 'b"} but on the right @{typ"'a \<Rightarrow> 'a"} and @{typ"'b \<Rightarrow> 13.9 -'b"}. The annotation @{text"(overloaded)"} tells Isabelle that the definitions do 13.10 -intentionally define @{term inverse} only at instances of its declared type 13.11 -@{typ"'a \<Rightarrow> 'a"} --- this merely supresses warnings to that effect. 13.12 +benign because the type of @{term[source]inverse} becomes smaller: on the 13.13 +left it is @{typ"'a \<times> 'b \<Rightarrow> 'a \<times> 'b"} but on the right @{typ"'a \<Rightarrow> 'a"} and 13.14 +@{typ"'b \<Rightarrow> 'b"}. The annotation @{text"(overloaded)"} tells Isabelle that 13.15 +the definitions do intentionally define @{term[source]inverse} only at 13.16 +instances of its declared type @{typ"'a \<Rightarrow> 'a"} --- this merely supresses 13.17 +warnings to that effect. 13.18 13.19 However, there is nothing to prevent the user from forming terms such as 13.20 -@{term"inverse []"} and proving theorems as @{prop"inverse [] = inverse []"}, 13.21 -although we never defined inverse on lists. We hasten to say that there is 13.22 -nothing wrong with such terms and theorems. But it would be nice if we could 13.23 -prevent their formation, simply because it is very likely that the user did 13.24 -not mean to write what he did. Thus he had better not waste his time pursuing 13.25 -it further. This requires the use of type classes. 13.26 +@{term[source]"inverse []"} and proving theorems as @{prop[source]"inverse [] 13.27 += inverse []"}, although we never defined inverse on lists. We hasten to say 13.28 +that there is nothing wrong with such terms and theorems. But it would be 13.29 +nice if we could prevent their formation, simply because it is very likely 13.30 +that the user did not mean to write what he did. Thus he had better not waste 13.31 +his time pursuing it further. This requires the use of type classes. 13.32 *} 13.33 (*<*)end(*>*)

14.1 --- a/doc-src/TutorialI/Types/ROOT.ML Wed Nov 29 10:22:38 2000 +0100 14.2 +++ b/doc-src/TutorialI/Types/ROOT.ML Wed Nov 29 13:44:26 2000 +0100 14.3 @@ -1,4 +1,5 @@ 14.4 use "../settings.ML"; 14.5 +use_thy "Pairs"; 14.6 use_thy "Typedef"; 14.7 use_thy "Overloading0"; 14.8 use_thy "Overloading2";

15.1 --- a/doc-src/TutorialI/Types/document/Overloading0.tex Wed Nov 29 10:22:38 2000 +0100 15.2 +++ b/doc-src/TutorialI/Types/document/Overloading0.tex Wed Nov 29 13:44:26 2000 +0100 15.3 @@ -29,18 +29,19 @@ 15.4 Isabelle will not complain because the three definitions do not overlap: no 15.5 two of the three types \isa{bool}, \isa{{\isacharprime}a\ set} and \isa{{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b} have a 15.6 common instance. What is more, the recursion in \isa{inverse{\isacharunderscore}pair} is 15.7 -benign because the type of \isa{Overloading{\isadigit{0}}{\isachardot}inverse} becomes smaller: on the left it is 15.8 -\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 15.9 -intentionally define \isa{Overloading{\isadigit{0}}{\isachardot}inverse} only at instances of its declared type 15.10 -\isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} --- this merely supresses warnings to that effect. 15.11 +benign because the type of \isa{inverse} becomes smaller: on the 15.12 +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 15.13 +\isa{{\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}b}. The annotation \isa{{\isacharparenleft}overloaded{\isacharparenright}} tells Isabelle that 15.14 +the definitions do intentionally define \isa{inverse} only at 15.15 +instances of its declared type \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} --- this merely supresses 15.16 +warnings to that effect. 15.17 15.18 However, there is nothing to prevent the user from forming terms such as 15.19 -\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}}, 15.20 -although we never defined inverse on lists. We hasten to say that there is 15.21 -nothing wrong with such terms and theorems. But it would be nice if we could 15.22 -prevent their formation, simply because it is very likely that the user did 15.23 -not mean to write what he did. Thus he had better not waste his time pursuing 15.24 -it further. This requires the use of type classes.% 15.25 +\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 15.26 +that there is nothing wrong with such terms and theorems. But it would be 15.27 +nice if we could prevent their formation, simply because it is very likely 15.28 +that the user did not mean to write what he did. Thus he had better not waste 15.29 +his time pursuing it further. This requires the use of type classes.% 15.30 \end{isamarkuptext}% 15.31 \end{isabellebody}% 15.32 %%% Local Variables:

16.1 --- a/doc-src/TutorialI/Types/types.tex Wed Nov 29 10:22:38 2000 +0100 16.2 +++ b/doc-src/TutorialI/Types/types.tex Wed Nov 29 13:44:26 2000 +0100 16.3 @@ -6,25 +6,23 @@ 16.4 advanced material: 16.5 \begin{itemize} 16.6 \item More about basic types: numbers ({\S}\ref{sec:numbers}), pairs 16.7 - ({\S}\ref{sec:products}) and records ({\S}\ref{sec:records}), and how to reason 16.8 - about them. 16.9 + ({\S}\ref{sec:products}) and records ({\S}\ref{sec:records}), and how to 16.10 + reason about them. 16.11 \item Introducing your own types: how to introduce your own new types that 16.12 - cannot be constructed with any of the basic methods ({\S}\ref{sec:adv-typedef}). 16.13 + cannot be constructed with any of the basic methods 16.14 + ({\S}\ref{sec:adv-typedef}). 16.15 \item Type classes: how to specify and reason about axiomatic collections of 16.16 types ({\S}\ref{sec:axclass}). 16.17 \end{itemize} 16.18 16.19 -\section{Basic types} 16.20 - 16.21 -\subsection{Numbers} 16.22 +\section{Numbers} 16.23 \label{sec:numbers} 16.24 16.25 -\subsection{Pairs} 16.26 -\label{sec:products} 16.27 +\input{Types/document/Pairs} 16.28 % Check refs to this section to see what is expected of it. 16.29 % Mention type unit 16.30 16.31 -\subsection{Records} 16.32 +\section{Records} 16.33 \label{sec:records} 16.34 16.35 \input{Types/document/Typedef}

17.1 --- a/doc-src/TutorialI/appendix.tex Wed Nov 29 10:22:38 2000 +0100 17.2 +++ b/doc-src/TutorialI/appendix.tex Wed Nov 29 13:44:26 2000 +0100 17.3 @@ -61,7 +61,7 @@ 17.4 \indexboldpos{\isasymle}{$HOL2arithrel}& 17.5 \ttindexboldpos{<=}{$HOL2arithrel}& 17.6 \verb$\<le>$\\ 17.7 -\indexboldpos{\isasymtimes}{$IsaFun}& 17.8 +\indexboldpos{\isasymtimes}{$Isatype}& 17.9 \ttindexboldpos{*}{$HOL2arithfun} & 17.10 \verb$\<times>$\\ 17.11 \indexboldpos{\isasymin}{$HOL3Set0a}&

18.1 --- a/doc-src/TutorialI/basics.tex Wed Nov 29 10:22:38 2000 +0100 18.2 +++ b/doc-src/TutorialI/basics.tex Wed Nov 29 13:44:26 2000 +0100 18.3 @@ -102,7 +102,7 @@ 18.4 which abbreviates \isa{$\tau@1$ \isasymFun~$\cdots$ \isasymFun~$\tau@n$ 18.5 \isasymFun~$\tau$}. 18.6 \item[type variables,]\indexbold{type variable}\indexbold{variable!type} 18.7 - denoted by \isaindexbold{'a}, \isa{'b} etc., just like in ML. They give rise 18.8 + denoted by \ttindexboldpos{'a}{$Isatype}, \isa{'b} etc., just like in ML. They give rise 18.9 to polymorphic types like \isa{'a \isasymFun~'a}, the type of the identity 18.10 function. 18.11 \end{description} 18.12 @@ -183,10 +183,10 @@ 18.13 Despite type inference, it is sometimes necessary to attach explicit 18.14 \textbf{type constraints}\indexbold{type constraint} to a term. The syntax is 18.15 \isa{$t$::$\tau$} as in \isa{x < (y::nat)}. Note that 18.16 -\ttindexboldpos{::}{$Isalamtc} binds weakly and should therefore be enclosed 18.17 +\ttindexboldpos{::}{$Isatype} binds weakly and should therefore be enclosed 18.18 in parentheses: \isa{x < y::nat} is ill-typed because it is interpreted as 18.19 \isa{(x < y)::nat}. The main reason for type constraints are overloaded 18.20 -functions like \isa{+}, \isa{*} and \isa{<}. See \S\ref{sec:overloading} for 18.21 +functions like \isa{+}, \isa{*} and \isa{<}. See {\S}\ref{sec:overloading} for 18.22 a full discussion of overloading. 18.23 18.24 \begin{warn}

19.1 --- a/doc-src/TutorialI/fp.tex Wed Nov 29 10:22:38 2000 +0100 19.2 +++ b/doc-src/TutorialI/fp.tex Wed Nov 29 13:44:26 2000 +0100 19.3 @@ -186,7 +186,7 @@ 19.4 primitive recursive function definitions. 19.5 19.6 Every datatype $t$ comes equipped with a \isa{size} function from $t$ into 19.7 -the natural numbers (see~\S\ref{sec:nat} below). For lists, \isa{size} is 19.8 +the natural numbers (see~{\S}\ref{sec:nat} below). For lists, \isa{size} is 19.9 just the length, i.e.\ \isa{size [] = 0} and \isa{size(x \# xs) = size xs + 19.10 1}. In general, \isaindexbold{size} returns \isa{0} for all constructors 19.11 that do not have an argument of type $t$, and for all other constructors 19.12 @@ -209,7 +209,7 @@ 19.13 becomes smaller with every recursive call. There must be exactly one equation 19.14 for each constructor. Their order is immaterial. 19.15 A more general method for defining total recursive functions is introduced in 19.16 -\S\ref{sec:recdef}. 19.17 +{\S}\ref{sec:recdef}. 19.18 19.19 \begin{exercise}\label{ex:Tree} 19.20 \input{Misc/document/Tree.tex}% 19.21 @@ -220,7 +220,7 @@ 19.22 \begin{warn} 19.23 Induction is only allowed on free (or \isasymAnd-bound) variables that 19.24 should not occur among the assumptions of the subgoal; see 19.25 - \S\ref{sec:ind-var-in-prems} for details. Case distinction 19.26 + {\S}\ref{sec:ind-var-in-prems} for details. Case distinction 19.27 (\isa{case_tac}) works for arbitrary terms, which need to be 19.28 quoted if they are non-atomic. 19.29 \end{warn} 19.30 @@ -238,94 +238,12 @@ 19.31 \input{Misc/document/fakenat.tex} 19.32 \input{Misc/document/natsum.tex} 19.33 19.34 -The usual arithmetic operations \ttindexboldpos{+}{$HOL2arithfun}, 19.35 -\ttindexboldpos{-}{$HOL2arithfun}, \ttindexboldpos{*}{$HOL2arithfun}, 19.36 -\isaindexbold{div}, \isaindexbold{mod}, \isaindexbold{min} and 19.37 -\isaindexbold{max} are predefined, as are the relations 19.38 -\indexboldpos{\isasymle}{$HOL2arithrel} and 19.39 -\ttindexboldpos{<}{$HOL2arithrel}. There is even a least number operation 19.40 -\isaindexbold{LEAST}. For example, \isa{(LEAST n.$\,$1 < n) = 2}, although 19.41 -Isabelle does not prove this completely automatically. Note that \isa{1} and 19.42 -\isa{2} are available as abbreviations for the corresponding 19.43 -\isa{Suc}-expressions. If you need the full set of numerals, 19.44 -see~\S\ref{nat-numerals}. 19.45 - 19.46 -\begin{warn} 19.47 - The constant \ttindexbold{0} and the operations 19.48 - \ttindexboldpos{+}{$HOL2arithfun}, \ttindexboldpos{-}{$HOL2arithfun}, 19.49 - \ttindexboldpos{*}{$HOL2arithfun}, \isaindexbold{min}, \isaindexbold{max}, 19.50 - \indexboldpos{\isasymle}{$HOL2arithrel} and 19.51 - \ttindexboldpos{<}{$HOL2arithrel} are overloaded, i.e.\ they are available 19.52 - not just for natural numbers but at other types as well (see 19.53 - \S\ref{sec:overloading}). For example, given the goal \isa{x+0 = x}, there 19.54 - is nothing to indicate that you are talking about natural numbers. Hence 19.55 - Isabelle can only infer that \isa{x} is of some arbitrary type where 19.56 - \isa{0} and \isa{+} are declared. As a consequence, you will be unable to 19.57 - prove the goal (although it may take you some time to realize what has 19.58 - happened if \texttt{show_types} is not set). In this particular example, 19.59 - you need to include an explicit type constraint, for example \isa{x+0 = 19.60 - (x::nat)}. If there is enough contextual information this may not be 19.61 - necessary: \isa{Suc x = x} automatically implies \isa{x::nat} because 19.62 - \isa{Suc} is not overloaded. 19.63 -\end{warn} 19.64 - 19.65 -Simple arithmetic goals are proved automatically by both \isa{auto} 19.66 -and the simplification methods introduced in \S\ref{sec:Simplification}. For 19.67 -example, 19.68 - 19.69 -\input{Misc/document/arith1.tex}% 19.70 -is proved automatically. The main restriction is that only addition is taken 19.71 -into account; other arithmetic operations and quantified formulae are ignored. 19.72 - 19.73 -For more complex goals, there is the special method 19.74 -\isaindexbold{arith} (which attacks the first subgoal). It proves 19.75 -arithmetic goals involving the usual logical connectives (\isasymnot, 19.76 -\isasymand, \isasymor, \isasymimp), the relations \isasymle\ and \isa{<}, and 19.77 -the operations \isa{+}, \isa{-}, \isa{min} and \isa{max}. For example, 19.78 - 19.79 -\input{Misc/document/arith2.tex}% 19.80 -succeeds because \isa{k*k} can be treated as atomic. 19.81 -In contrast, 19.82 - 19.83 -\input{Misc/document/arith3.tex}% 19.84 -is not even proved by \isa{arith} because the proof relies essentially 19.85 -on properties of multiplication. 19.86 - 19.87 -\begin{warn} 19.88 - The running time of \isa{arith} is exponential in the number of occurrences 19.89 - of \ttindexboldpos{-}{$HOL2arithfun}, \isaindexbold{min} and 19.90 - \isaindexbold{max} because they are first eliminated by case distinctions. 19.91 - 19.92 - \isa{arith} is incomplete even for the restricted class of formulae 19.93 - described above (known as ``linear arithmetic''). If divisibility plays a 19.94 - role, it may fail to prove a valid formula, for example $m+m \neq n+n+1$. 19.95 - Fortunately, such examples are rare in practice. 19.96 -\end{warn} 19.97 - 19.98 \index{arithmetic|)} 19.99 19.100 19.101 \subsection{Pairs} 19.102 \input{Misc/document/pairs.tex} 19.103 19.104 -%FIXME move stuff below into section on proofs about products? 19.105 -\begin{warn} 19.106 - Abstraction over pairs and tuples is merely a convenient shorthand for a 19.107 - more complex internal representation. Thus the internal and external form 19.108 - of a term may differ, which can affect proofs. If you want to avoid this 19.109 - complication, use \isa{fst} and \isa{snd}, i.e.\ write 19.110 - \isa{\isasymlambda{}p.~fst p + snd p} instead of 19.111 - \isa{\isasymlambda(x,y).~x + y}. See~\S\ref{sec:products} for 19.112 - theorem proving with tuple patterns. 19.113 -\end{warn} 19.114 - 19.115 -Note that products, like type \isa{nat}, are datatypes, which means 19.116 -in particular that \isa{induct_tac} and \isa{case_tac} are applicable to 19.117 -products (see \S\ref{sec:products}). 19.118 - 19.119 -Instead of tuples with many components (where ``many'' is not much above 2), 19.120 -it is far preferable to use records (see \S\ref{sec:records}). 19.121 - 19.122 \section{Definitions} 19.123 \label{sec:Definitions} 19.124 19.125 @@ -346,7 +264,7 @@ 19.126 19.127 Note that pattern-matching is not allowed, i.e.\ each definition must be of 19.128 the form $f\,x@1\,\dots\,x@n~\isasymequiv~t$. 19.129 -Section~\S\ref{sec:Simplification} explains how definitions are used 19.130 +Section~{\S}\ref{sec:Simplification} explains how definitions are used 19.131 in proofs. 19.132 19.133 \input{Misc/document/prime_def.tex} 19.134 @@ -357,15 +275,15 @@ 19.135 The purpose of this chapter is to deepen the reader's understanding of the 19.136 concepts encountered so far and to introduce advanced forms of datatypes and 19.137 recursive functions. The first two sections give a structured presentation of 19.138 -theorem proving by simplification (\S\ref{sec:Simplification}) and discuss 19.139 -important heuristics for induction (\S\ref{sec:InductionHeuristics}). They can 19.140 +theorem proving by simplification ({\S}\ref{sec:Simplification}) and discuss 19.141 +important heuristics for induction ({\S}\ref{sec:InductionHeuristics}). They can 19.142 be skipped by readers less interested in proofs. They are followed by a case 19.143 -study, a compiler for expressions (\S\ref{sec:ExprCompiler}). Advanced 19.144 +study, a compiler for expressions ({\S}\ref{sec:ExprCompiler}). Advanced 19.145 datatypes, including those involving function spaces, are covered in 19.146 -\S\ref{sec:advanced-datatypes}, which closes with another case study, search 19.147 +{\S}\ref{sec:advanced-datatypes}, which closes with another case study, search 19.148 trees (``tries''). Finally we introduce \isacommand{recdef}, a very general 19.149 form of recursive function definition which goes well beyond what 19.150 -\isacommand{primrec} allows (\S\ref{sec:recdef}). 19.151 +\isacommand{primrec} allows ({\S}\ref{sec:recdef}). 19.152 19.153 19.154 \section{Simplification} 19.155 @@ -382,7 +300,7 @@ 19.156 many other systems. The tool itself is called the \bfindex{simplifier}. The 19.157 purpose of this section is introduce the many features of the simplifier. 19.158 Anybody intending to use HOL should read this section. Later on 19.159 -(\S\ref{sec:simplification-II}) we explain some more advanced features and a 19.160 +({\S}\ref{sec:simplification-II}) we explain some more advanced features and a 19.161 little bit of how the simplifier works. The serious student should read that 19.162 section as well, in particular in order to understand what happened if things 19.163 do not simplify as expected. 19.164 @@ -550,7 +468,7 @@ 19.165 recursion need not involve datatypes, and termination is proved by showing 19.166 that the arguments of all recursive calls are smaller in a suitable (user 19.167 supplied) sense. In this section we ristrict ourselves to measure functions; 19.168 -more advanced termination proofs are discussed in \S\ref{sec:beyond-measure}. 19.169 +more advanced termination proofs are discussed in {\S}\ref{sec:beyond-measure}. 19.170 19.171 \subsection{Defining recursive functions} 19.172