# HG changeset patch # User nipkow # Date 980433091 -3600 # Node ID 5eebea8f359f579656f0fa784642de46afba2858 # Parent 4b47d8aaf5af627c16d6b81351a9e1db640f6c24 *** empty log message *** diff -r 4b47d8aaf5af -r 5eebea8f359f doc-src/TutorialI/Advanced/document/simp.tex --- a/doc-src/TutorialI/Advanced/document/simp.tex Thu Jan 25 11:59:52 2001 +0100 +++ b/doc-src/TutorialI/Advanced/document/simp.tex Thu Jan 25 15:31:31 2001 +0100 @@ -94,8 +94,8 @@ once they apply, they can be used forever. The simplifier is aware of this danger and treats permutative rules by means of a special strategy, called \bfindex{ordered rewriting}: a permutative rewrite -rule is only applied if the term becomes ``smaller'' (with respect to a fixed -lexicographic ordering on terms). For example, commutativity rewrites +rule is only applied if the term becomes smaller with respect to a fixed +lexicographic ordering on terms. For example, commutativity rewrites \isa{b\ {\isacharplus}\ a} to \isa{a\ {\isacharplus}\ b}, but then stops because \isa{a\ {\isacharplus}\ b} is strictly smaller than \isa{b\ {\isacharplus}\ a}. Permutative rewrite rules can be turned into simplification rules in the usual manner via the \isa{simp} attribute; the @@ -150,7 +150,7 @@ form (this will always be the case unless you have done something strange) where each occurrence of an unknown is of the form $\Var{f}~x@1~\dots~x@n$, where the $x@i$ are distinct bound -variables. Thus all ``standard'' rewrite rules, where all unknowns are +variables. Thus all ordinary rewrite rules, where all unknowns are of base type, for example \isa{{\isacharquery}m\ {\isacharplus}\ {\isacharquery}n\ {\isacharplus}\ {\isacharquery}k\ {\isacharequal}\ {\isacharquery}m\ {\isacharplus}\ {\isacharparenleft}{\isacharquery}n\ {\isacharplus}\ {\isacharquery}k{\isacharparenright}}, are OK: if an unknown is of base type, it cannot have any arguments. Additionally, the rule \isa{{\isacharparenleft}{\isasymforall}x{\isachardot}\ {\isacharquery}P\ x\ {\isasymand}\ {\isacharquery}Q\ x{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isacharparenleft}{\isasymforall}x{\isachardot}\ {\isacharquery}P\ x{\isacharparenright}\ {\isasymand}\ {\isacharparenleft}{\isasymforall}x{\isachardot}\ {\isacharquery}Q\ x{\isacharparenright}{\isacharparenright}} is also OK, in diff -r 4b47d8aaf5af -r 5eebea8f359f doc-src/TutorialI/Advanced/simp.thy --- a/doc-src/TutorialI/Advanced/simp.thy Thu Jan 25 11:59:52 2001 +0100 +++ b/doc-src/TutorialI/Advanced/simp.thy Thu Jan 25 15:31:31 2001 +0100 @@ -79,8 +79,8 @@ once they apply, they can be used forever. The simplifier is aware of this danger and treats permutative rules by means of a special strategy, called \bfindex{ordered rewriting}: a permutative rewrite -rule is only applied if the term becomes ``smaller'' (with respect to a fixed -lexicographic ordering on terms). For example, commutativity rewrites +rule is only applied if the term becomes smaller with respect to a fixed +lexicographic ordering on terms. For example, commutativity rewrites @{term"b+a"} to @{term"a+b"}, but then stops because @{term"a+b"} is strictly smaller than @{term"b+a"}. Permutative rewrite rules can be turned into simplification rules in the usual manner via the @{text simp} attribute; the @@ -131,7 +131,7 @@ form (this will always be the case unless you have done something strange) where each occurrence of an unknown is of the form $\Var{f}~x@1~\dots~x@n$, where the $x@i$ are distinct bound -variables. Thus all ``standard'' rewrite rules, where all unknowns are +variables. Thus all ordinary rewrite rules, where all unknowns are of base type, for example @{thm add_assoc}, are OK: if an unknown is of base type, it cannot have any arguments. Additionally, the rule @{text"(\x. ?P x \ ?Q x) = ((\x. ?P x) \ (\x. ?Q x))"} is also OK, in diff -r 4b47d8aaf5af -r 5eebea8f359f doc-src/TutorialI/Ifexpr/Ifexpr.thy --- a/doc-src/TutorialI/Ifexpr/Ifexpr.thy Thu Jan 25 11:59:52 2001 +0100 +++ b/doc-src/TutorialI/Ifexpr/Ifexpr.thy Thu Jan 25 15:31:31 2001 +0100 @@ -10,7 +10,7 @@ the constructs introduced above. *} -subsubsection{*How Can We Model Boolean Expressions?*} +subsubsection{*Modelling Boolean Expressions*} text{* We want to represent boolean expressions built up from variables and @@ -28,7 +28,7 @@ For example, the formula $P@0 \land \neg P@1$ is represented by the term @{term"And (Var 0) (Neg(Var 1))"}. -\subsubsection{What is the Value of a Boolean Expression?} +\subsubsection{The Value of a Boolean Expression} The value of a boolean expression depends on the value of its variables. Hence the function @{text"value"} takes an additional parameter, an @@ -66,9 +66,8 @@ else valif e env)"; text{* -\subsubsection{Transformation Into and of If-Expressions} +\subsubsection{Converting Boolean and If-Expressions} -\REMARK{is this the title you wanted?} The type @{typ"boolex"} is close to the customary representation of logical formulae, whereas @{typ"ifex"} is designed for efficiency. It is easy to translate from @{typ"boolex"} into @{typ"ifex"}: diff -r 4b47d8aaf5af -r 5eebea8f359f doc-src/TutorialI/Ifexpr/document/Ifexpr.tex --- a/doc-src/TutorialI/Ifexpr/document/Ifexpr.tex Thu Jan 25 11:59:52 2001 +0100 +++ b/doc-src/TutorialI/Ifexpr/document/Ifexpr.tex Thu Jan 25 15:31:31 2001 +0100 @@ -12,7 +12,7 @@ the constructs introduced above.% \end{isamarkuptext}% % -\isamarkupsubsubsection{How Can We Model Boolean Expressions?% +\isamarkupsubsubsection{Modelling Boolean Expressions% } % \begin{isamarkuptext}% @@ -30,7 +30,7 @@ For example, the formula $P@0 \land \neg P@1$ is represented by the term \isa{And\ {\isacharparenleft}Var\ {\isadigit{0}}{\isacharparenright}\ {\isacharparenleft}Neg\ {\isacharparenleft}Var\ {\isadigit{1}}{\isacharparenright}{\isacharparenright}}. -\subsubsection{What is the Value of a Boolean Expression?} +\subsubsection{The Value of a Boolean Expression} The value of a boolean expression depends on the value of its variables. Hence the function \isa{value} takes an additional parameter, an @@ -64,9 +64,8 @@ {\isachardoublequote}valif\ {\isacharparenleft}IF\ b\ t\ e{\isacharparenright}\ env\ {\isacharequal}\ {\isacharparenleft}if\ valif\ b\ env\ then\ valif\ t\ env\isanewline \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ else\ valif\ e\ env{\isacharparenright}{\isachardoublequote}% \begin{isamarkuptext}% -\subsubsection{Transformation Into and of If-Expressions} +\subsubsection{Converting Boolean and If-Expressions} -\REMARK{is this the title you wanted?} The type \isa{boolex} is close to the customary representation of logical formulae, whereas \isa{ifex} is designed for efficiency. It is easy to translate from \isa{boolex} into \isa{ifex}:% diff -r 4b47d8aaf5af -r 5eebea8f359f doc-src/TutorialI/Inductive/advanced-examples.tex --- a/doc-src/TutorialI/Inductive/advanced-examples.tex Thu Jan 25 11:59:52 2001 +0100 +++ b/doc-src/TutorialI/Inductive/advanced-examples.tex Thu Jan 25 15:31:31 2001 +0100 @@ -137,7 +137,7 @@ Applying this as an elimination rule yields one case where \isa{even.cases} would yield two. Rule inversion works well when the conclusions of the introduction rules involve datatype constructors like \isa{Suc} and \isa{\#} -(list `cons'); freeness reasoning discards all but one or two cases. +(list ``cons''); freeness reasoning discards all but one or two cases. In the \isacommand{inductive\_cases} command we supplied an attribute, \isa{elim!}, indicating that this elimination rule can be applied diff -r 4b47d8aaf5af -r 5eebea8f359f doc-src/TutorialI/IsaMakefile --- a/doc-src/TutorialI/IsaMakefile Thu Jan 25 11:59:52 2001 +0100 +++ b/doc-src/TutorialI/IsaMakefile Thu Jan 25 15:31:31 2001 +0100 @@ -165,7 +165,7 @@ $(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/Option2.thy \ Misc/types.thy Misc/prime_def.thy Misc/case_exprs.thy \ - Misc/simp.thy Misc/Itrev.thy Misc/AdvancedInd.thy + Misc/simp.thy Misc/Itrev.thy Misc/AdvancedInd.thy Misc/appendix.thy $(USEDIR) Misc @rm -f tutorial.dvi diff -r 4b47d8aaf5af -r 5eebea8f359f doc-src/TutorialI/Misc/ROOT.ML --- a/doc-src/TutorialI/Misc/ROOT.ML Thu Jan 25 11:59:52 2001 +0100 +++ b/doc-src/TutorialI/Misc/ROOT.ML Thu Jan 25 15:31:31 2001 +0100 @@ -11,3 +11,4 @@ use_thy "simp"; use_thy "Itrev"; use_thy "AdvancedInd"; +use_thy "appendix"; diff -r 4b47d8aaf5af -r 5eebea8f359f doc-src/TutorialI/Misc/document/natsum.tex --- a/doc-src/TutorialI/Misc/document/natsum.tex Thu Jan 25 11:59:52 2001 +0100 +++ b/doc-src/TutorialI/Misc/document/natsum.tex Thu Jan 25 15:31:31 2001 +0100 @@ -43,8 +43,8 @@ \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}, + not just for natural numbers but at other types as well. + 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 @@ -54,6 +54,10 @@ \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. \end{warn} Simple arithmetic goals are proved automatically by both \isa{auto} and the diff -r 4b47d8aaf5af -r 5eebea8f359f doc-src/TutorialI/Misc/natsum.thy --- a/doc-src/TutorialI/Misc/natsum.thy Thu Jan 25 11:59:52 2001 +0100 +++ b/doc-src/TutorialI/Misc/natsum.thy Thu Jan 25 15:31:31 2001 +0100 @@ -41,8 +41,8 @@ \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"}, + not just for natural numbers but at other types as well. + For example, given the goal @{prop"x+0 = x"}, there is nothing to indicate that you are talking about natural numbers. Hence Isabelle can only infer that @{term x} is of some arbitrary type where @{term 0} and @{text"+"} are declared. As a consequence, you will be unable @@ -52,6 +52,10 @@ @{text"x+0 = (x::nat)"}. If there is enough contextual information this may not be necessary: @{prop"Suc x = x"} automatically implies @{text"x::nat"} because @{term Suc} is not overloaded. + + For details see \S\ref{sec:numbers} and \S\ref{sec:overloading}; + Table~\ref{tab:overloading} in the appendix shows the most important overloaded + operations. \end{warn} Simple arithmetic goals are proved automatically by both @{term auto} and the diff -r 4b47d8aaf5af -r 5eebea8f359f doc-src/TutorialI/Rules/rules.tex --- a/doc-src/TutorialI/Rules/rules.tex Thu Jan 25 11:59:52 2001 +0100 +++ b/doc-src/TutorialI/Rules/rules.tex Thu Jan 25 15:31:31 2001 +0100 @@ -234,8 +234,8 @@ Recall that the conjunction elimination rules --- whose Isabelle names are \isa{conjunct1} and \isa{conjunct2} --- simply return the first or second half of a conjunction. Rules of this sort (where the conclusion is a subformula of a -premise) are called \textbf{destruction} rules, by analogy with the destructor -functions of functional programming.% +premise) are called \textbf{destruction} rules because they take apart and destroy +a premise.% \footnote{This Isabelle terminology has no counterpart in standard logic texts, although the distinction between the two forms of elimination rule is well known. Girard \cite[page 74]{girard89}, for example, writes ``The elimination rules @@ -365,7 +365,7 @@ conclusion. \medskip -\indexbold{by} +\indexbold{*by} The \isacommand{by} command is useful for proofs like these that use \isa{assumption} heavily. It executes an \isacommand{apply} command, then tries to prove all remaining subgoals using @@ -781,7 +781,7 @@ To see how this works, let us derive a rule about reducing the scope of a universal quantifier. In mathematical notation we write \[ \infer{P\imp\forall x.\,Q}{\forall x.\,P\imp Q} \] -with the proviso `$x$ not free in~$P$.' Isabelle's treatment of +with the proviso ``$x$ not free in~$P$.'' Isabelle's treatment of substitution makes the proviso unnecessary. The conclusion is expressed as \isa{P\ \isasymlongrightarrow\ ({\isasymforall}x.\ Q\ x)}. No substitution for the @@ -860,7 +860,7 @@ \isacommand{apply}\ (rename_tac\ v\ w)\isanewline \ 1.\ \isasymAnd v\ w.\ x\ <\ y\ \isasymLongrightarrow \ P\ v\ (f\ w) \end{isabelle} -Recall that \isa{rule_tac}\index{rule_tac|and renaming} instantiates a +Recall that \isa{rule_tac}\index{*rule_tac!and renaming} instantiates a theorem with specified terms. These terms may involve the goal's bound variables, but beware of referring to variables like~\isa{xa}. A future change to your theories could change the set of names @@ -1686,7 +1686,7 @@ The next step is to put the theorem \isa{gcd_mult_0} into a simplified form, performing the steps -$\gcd(1,n)=1$ and $k\times1=k$. The \isa{simplified}\indexbold{simplified} +$\gcd(1,n)=1$ and $k\times1=k$. The \isaindexbold{simplified} attribute takes a theorem and returns the result of simplifying it, with respect to the default simplification rules: @@ -1769,7 +1769,7 @@ \end{isabelle} \medskip -The \isa{rule_format}\indexbold{rule_format} directive replaces a common usage +The \isaindexbold{rule_format} directive replaces a common usage of \isa{THEN}\@. It is needed in proofs by induction when the induction formula must be expressed using \isa{\isasymlongrightarrow} and \isa{\isasymforall}. For example, in diff -r 4b47d8aaf5af -r 5eebea8f359f doc-src/TutorialI/Sets/sets.tex --- a/doc-src/TutorialI/Sets/sets.tex Thu Jan 25 11:59:52 2001 +0100 +++ b/doc-src/TutorialI/Sets/sets.tex Thu Jan 25 15:31:31 2001 +0100 @@ -871,7 +871,7 @@ Many familiar induction principles are instances of this rule. For example, the predecessor relation on the natural numbers is well-founded; induction over it is mathematical induction. -The `tail of' relation on lists is well-founded; induction over +The ``tail of'' relation on lists is well-founded; induction over it is structural induction. Well-foundedness can be difficult to show. The various diff -r 4b47d8aaf5af -r 5eebea8f359f doc-src/TutorialI/ToyList/ToyList.thy --- a/doc-src/TutorialI/ToyList/ToyList.thy Thu Jan 25 11:59:52 2001 +0100 +++ b/doc-src/TutorialI/ToyList/ToyList.thy Thu Jan 25 15:31:31 2001 +0100 @@ -177,7 +177,7 @@ txt{*\noindent\index{*induct_tac}% This tells Isabelle to perform induction on variable @{term"xs"}. The suffix -@{term"tac"} stands for ``tactic'', a synonym for ``theorem proving function''. +@{term"tac"} stands for \bfindex{tactic}, a synonym for ``theorem proving function''. By default, induction acts on the first subgoal. The new proof state contains two subgoals, namely the base case (@{term[source]Nil}) and the induction step (@{term[source]Cons}): @@ -207,7 +207,7 @@ txt{*\noindent This command tells Isabelle to apply a proof strategy called @{text"auto"} to all subgoals. Essentially, @{text"auto"} tries to -``simplify'' the subgoals. In our case, subgoal~1 is solved completely (thanks +simplify the subgoals. In our case, subgoal~1 is solved completely (thanks to the equation @{prop"rev [] = []"}) and disappears; the simplified version of subgoal~2 becomes the new subgoal~1: @{subgoals[display,indent=0,margin=70]} diff -r 4b47d8aaf5af -r 5eebea8f359f doc-src/TutorialI/ToyList/document/ToyList.tex --- a/doc-src/TutorialI/ToyList/document/ToyList.tex Thu Jan 25 11:59:52 2001 +0100 +++ b/doc-src/TutorialI/ToyList/document/ToyList.tex Thu Jan 25 15:31:31 2001 +0100 @@ -172,7 +172,7 @@ \begin{isamarkuptxt}% \noindent\index{*induct_tac}% This tells Isabelle to perform induction on variable \isa{xs}. The suffix -\isa{tac} stands for ``tactic'', a synonym for ``theorem proving function''. +\isa{tac} stands for \bfindex{tactic}, a synonym for ``theorem proving function''. By default, induction acts on the first subgoal. The new proof state contains two subgoals, namely the base case (\isa{Nil}) and the induction step (\isa{Cons}): @@ -204,7 +204,7 @@ \noindent This command tells Isabelle to apply a proof strategy called \isa{auto} to all subgoals. Essentially, \isa{auto} tries to -``simplify'' the subgoals. In our case, subgoal~1 is solved completely (thanks +simplify the subgoals. In our case, subgoal~1 is solved completely (thanks to the equation \isa{rev\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}}) and disappears; the simplified version of subgoal~2 becomes the new subgoal~1: \begin{isabelle}% diff -r 4b47d8aaf5af -r 5eebea8f359f doc-src/TutorialI/Trie/Trie.thy --- a/doc-src/TutorialI/Trie/Trie.thy Thu Jan 25 11:59:52 2001 +0100 +++ b/doc-src/TutorialI/Trie/Trie.thy Thu Jan 25 15:31:31 2001 +0100 @@ -132,7 +132,7 @@ proof states are invisible, and we rely on the (possibly brittle) magic of @{text auto} (@{text simp_all} will not do --- try it) to split the subgoals of the induction up in such a way that case distinction on @{term bs} makes -sense and solves the proof. Part~\ref{Isar} shows you how to write readable +sense and solves the proof. Chapter~\ref{ch:Isar} shows you how to write readable and stable proofs. *}; diff -r 4b47d8aaf5af -r 5eebea8f359f doc-src/TutorialI/Trie/document/Trie.tex --- a/doc-src/TutorialI/Trie/document/Trie.tex Thu Jan 25 11:59:52 2001 +0100 +++ b/doc-src/TutorialI/Trie/document/Trie.tex Thu Jan 25 15:31:31 2001 +0100 @@ -122,7 +122,7 @@ proof states are invisible, and we rely on the (possibly brittle) magic of \isa{auto} (\isa{simp{\isacharunderscore}all} will not do --- try it) to split the subgoals of the induction up in such a way that case distinction on \isa{bs} makes -sense and solves the proof. Part~\ref{Isar} shows you how to write readable +sense and solves the proof. Chapter~\ref{ch:Isar} shows you how to write readable and stable proofs.% \end{isamarkuptext}% \end{isabellebody}% diff -r 4b47d8aaf5af -r 5eebea8f359f doc-src/TutorialI/Types/Overloading2.thy --- a/doc-src/TutorialI/Types/Overloading2.thy Thu Jan 25 11:59:52 2001 +0100 +++ b/doc-src/TutorialI/Types/Overloading2.thy Thu Jan 25 15:31:31 2001 +0100 @@ -22,38 +22,10 @@ text{* HOL comes with a number of overloaded constants and corresponding classes. -The most important ones are listed in Table~\ref{tab:overloading}. They are +The most important ones are listed in Table~\ref{tab:overloading} in the appendix. They are defined on all numeric types and sometimes on other types as well, for example @{text"-"}, @{text"\"} and @{text"<"} on sets. -\begin{table}[htbp] -\begin{center} -\begin{tabular}{lll} -Constant & Type & Syntax \\ -\hline -@{term 0} & @{text "'a::zero"} \\ -@{text"+"} & @{text "('a::plus) \ 'a \ 'a"} & (infixl 65) \\ -@{text"-"} & @{text "('a::minus) \ 'a \ 'a"} & (infixl 65) \\ -@{text"-"} & @{text "('a::minus) \ 'a"} \\ -@{text"*"} & @{text "('a::times) \ 'a \ 'a"} & (infixl 70) \\ -@{text div} & @{text "('a::div) \ 'a \ 'a"} & (infixl 70) \\ -@{text mod} & @{text "('a::div) \ 'a \ 'a"} & (infixl 70) \\ -@{text dvd} & @{text "('a::times) \ 'a \ bool"} & (infixl 50) \\ -@{text"/"} & @{text "('a::inverse) \ 'a \ 'a"} & (infixl 70) \\ -@{text"^"} & @{text "('a::power) \ nat \ 'a"} & (infixr 80) \\ -@{term abs} & @{text "('a::minus) \ 'a"} & ${\mid} x {\mid}$\\ -@{text"\"} & @{text "('a::ord) \ 'a \ bool"} & (infixl 50) \\ -@{text"<"} & @{text "('a::ord) \ 'a \ bool"} & (infixl 50) \\ -@{term min} & @{text "('a::ord) \ 'a \ 'a"} \\ -@{term max} & @{text "('a::ord) \ 'a \ 'a"} \\ -@{term Least} & @{text "('a::ord \ bool) \ 'a"} & -@{text LEAST}$~x.~P$ -\end{tabular} -\caption{Overloaded Constants in HOL} -\label{tab:overloading} -\end{center} -\end{table} - In addition there is a special input syntax for bounded quantifiers: \begin{center} \begin{tabular}{lcl} diff -r 4b47d8aaf5af -r 5eebea8f359f doc-src/TutorialI/Types/document/Overloading2.tex --- a/doc-src/TutorialI/Types/document/Overloading2.tex Thu Jan 25 11:59:52 2001 +0100 +++ b/doc-src/TutorialI/Types/document/Overloading2.tex Thu Jan 25 15:31:31 2001 +0100 @@ -24,38 +24,10 @@ % \begin{isamarkuptext}% HOL comes with a number of overloaded constants and corresponding classes. -The most important ones are listed in Table~\ref{tab:overloading}. They are +The most important ones are listed in Table~\ref{tab:overloading} in the appendix. They are defined on all numeric types and sometimes on other types as well, for example \isa{{\isacharminus}}, \isa{{\isasymle}} and \isa{{\isacharless}} on sets. -\begin{table}[htbp] -\begin{center} -\begin{tabular}{lll} -Constant & Type & Syntax \\ -\hline -\isa{{\isadigit{0}}} & \isa{{\isacharprime}a{\isacharcolon}{\isacharcolon}zero} \\ -\isa{{\isacharplus}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}plus{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} & (infixl 65) \\ -\isa{{\isacharminus}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}minus{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} & (infixl 65) \\ -\isa{{\isacharminus}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}minus{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a} \\ -\isa{{\isacharasterisk}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}times{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} & (infixl 70) \\ -\isa{div} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}div{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} & (infixl 70) \\ -\isa{mod} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}div{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} & (infixl 70) \\ -\isa{dvd} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}times{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool} & (infixl 50) \\ -\isa{{\isacharslash}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}inverse{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} & (infixl 70) \\ -\isa{{\isacharcircum}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}power{\isacharparenright}\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ {\isacharprime}a} & (infixr 80) \\ -\isa{abs} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}minus{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a} & ${\mid} x {\mid}$\\ -\isa{{\isasymle}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}ord{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool} & (infixl 50) \\ -\isa{{\isacharless}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}ord{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool} & (infixl 50) \\ -\isa{min} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}ord{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} \\ -\isa{max} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}ord{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} \\ -\isa{Least} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}ord\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a} & -\isa{LEAST}$~x.~P$ -\end{tabular} -\caption{Overloaded Constants in HOL} -\label{tab:overloading} -\end{center} -\end{table} - In addition there is a special input syntax for bounded quantifiers: \begin{center} \begin{tabular}{lcl} diff -r 4b47d8aaf5af -r 5eebea8f359f doc-src/TutorialI/Types/numerics.tex --- a/doc-src/TutorialI/Types/numerics.tex Thu Jan 25 11:59:52 2001 +0100 +++ b/doc-src/TutorialI/Types/numerics.tex Thu Jan 25 15:31:31 2001 +0100 @@ -6,7 +6,10 @@ \isa{int} of \textbf{integers}, which lack induction but support true subtraction. The logic HOL-Real also has the type \isa{real} of real numbers. Isabelle has no subtyping, so the numeric types are distinct and -there are functions to convert between them. +there are functions to convert between them. Fortunately most numeric +operations are overloaded: the same symbol can be used at all numeric types. +Table~\ref{tab:overloading} in the appendix shows the most important operations, +together with the priorities of the infix symbols. The integers are preferable to the natural numbers for reasoning about complicated arithmetic expressions. For example, a termination proof diff -r 4b47d8aaf5af -r 5eebea8f359f doc-src/TutorialI/appendix.tex --- a/doc-src/TutorialI/appendix.tex Thu Jan 25 11:59:52 2001 +0100 +++ b/doc-src/TutorialI/appendix.tex Thu Jan 25 15:31:31 2001 +0100 @@ -3,7 +3,7 @@ \chapter{Appendix} \label{sec:Appendix} -\begin{figure}[htbp] +\begin{table}[htbp] \begin{center} \begin{tabular}{|l|l|l|} \hline @@ -98,11 +98,13 @@ \hline \end{tabular} \end{center} -\caption{Mathematical symbols, their ASCII-equivalents and ProofGeneral codes} -\label{fig:ascii} -\end{figure}\indexbold{ASCII symbols} +\caption{Mathematical symbols, their ASCII-equivalents and X-Symbol codes} +\label{tab:ascii} +\end{table}\indexbold{ASCII symbols} -\begin{figure}[htbp] +\input{Misc/document/appendix.tex} + +\begin{table}[htbp] \begin{center} \begin{tabular}{|lllllllll|} \hline @@ -143,11 +145,11 @@ \end{tabular} \end{center} \caption{Reserved words in HOL terms} -\label{fig:ReservedWords} -\end{figure} +\label{tab:ReservedWords} +\end{table} -%\begin{figure}[htbp] +%\begin{table}[htbp] %\begin{center} %\begin{tabular}{|lllll|} %\hline @@ -175,5 +177,5 @@ %\end{tabular} %\end{center} %\caption{Minor keywords in HOL theories} -%\label{fig:keywords} -%\end{figure} +%\label{tab:keywords} +%\end{table} diff -r 4b47d8aaf5af -r 5eebea8f359f doc-src/TutorialI/basics.tex --- a/doc-src/TutorialI/basics.tex Thu Jan 25 11:59:52 2001 +0100 +++ b/doc-src/TutorialI/basics.tex Thu Jan 25 15:31:31 2001 +0100 @@ -62,7 +62,7 @@ HOL's theory collection is available online at \begin{center}\small - \url{http://isabelle.in.tum.de/library/} + \url{http://isabelle.in.tum.de/library/HOL/} \end{center} and is recommended browsing. Note that most of the theories are based on classical Isabelle without the Isar extension. This means that @@ -233,7 +233,7 @@ \end{itemize} For the sake of readability the usual mathematical symbols are used throughout -the tutorial. Their ASCII-equivalents are shown in figure~\ref{fig:ascii} in +the tutorial. Their ASCII-equivalents are shown in table~\ref{tab:ascii} in the appendix. @@ -279,7 +279,7 @@ Some interfaces (including the shell level) offer special fonts with mathematical symbols. For those that do not, remember that ASCII-equivalents -are shown in figure~\ref{fig:ascii} in the appendix. +are shown in table~\ref{tab:ascii} in the appendix. Finally, a word about semicolons.\indexbold{$Isar@\texttt{;}} Commands may but need not be terminated by semicolons. diff -r 4b47d8aaf5af -r 5eebea8f359f doc-src/TutorialI/fp.tex --- a/doc-src/TutorialI/fp.tex Thu Jan 25 11:59:52 2001 +0100 +++ b/doc-src/TutorialI/fp.tex Thu Jan 25 15:31:31 2001 +0100 @@ -129,10 +129,10 @@ \isa{\isacommand{theory}~T~=~\dots~:} is processed, the modified parent is reloaded automatically. - The only time when you need to load a theory by hand is when you simply - want to check if it loads successfully without wanting to make use of the - theory itself. This you can do by typing - \isa{\isacommand{use\_thy}\indexbold{*use_thy}~"T"}. +% The only time when you need to load a theory by hand is when you simply +% want to check if it loads successfully without wanting to make use of the +% theory itself. This you can do by typing +% \isa{\isacommand{use\_thy}\indexbold{*use_thy}~"T"}. \end{description} Further commands are found in the Isabelle/Isar Reference Manual. @@ -302,7 +302,7 @@ section as well, in particular in order to understand what happened if things do not simplify as expected. -\subsubsection{What is Simplification?} +\subsubsection{What is Simplification} In its most basic form, simplification means repeated application of equations from left to right. For example, taking the rules for \isa{\at} diff -r 4b47d8aaf5af -r 5eebea8f359f doc-src/TutorialI/tutorial.tex --- a/doc-src/TutorialI/tutorial.tex Thu Jan 25 11:59:52 2001 +0100 +++ b/doc-src/TutorialI/tutorial.tex Thu Jan 25 15:31:31 2001 +0100 @@ -91,6 +91,7 @@ \chapter{Theory Presentation} \chapter{Case Study: Verifying a Cryptographic Protocol} \chapter{Structured Proofs} +\label{ch:Isar} %\chapter{Case Study: UNIX File-System Security} %\chapter{The Tricks of the Trade} \input{appendix}