revisions and indexing
authorpaulson
Thu Jul 26 16:43:02 2001 +0200 (2001-07-26)
changeset 114567eb63f63e6c6
parent 11455 e07927b980ec
child 11457 279da0358aa9
revisions and indexing
doc-src/TutorialI/Ifexpr/Ifexpr.thy
doc-src/TutorialI/Ifexpr/document/Ifexpr.tex
doc-src/TutorialI/Misc/Translations.thy
doc-src/TutorialI/Misc/Tree.thy
doc-src/TutorialI/Misc/case_exprs.thy
doc-src/TutorialI/Misc/document/Translations.tex
doc-src/TutorialI/Misc/document/Tree.tex
doc-src/TutorialI/Misc/document/case_exprs.tex
doc-src/TutorialI/Misc/document/natsum.tex
doc-src/TutorialI/Misc/document/pairs.tex
doc-src/TutorialI/Misc/document/prime_def.tex
doc-src/TutorialI/Misc/document/types.tex
doc-src/TutorialI/Misc/natsum.thy
doc-src/TutorialI/Misc/pairs.thy
doc-src/TutorialI/Misc/prime_def.thy
doc-src/TutorialI/Misc/types.thy
doc-src/TutorialI/Rules/Basic.thy
doc-src/TutorialI/Rules/Force.thy
doc-src/TutorialI/ToyList/ToyList.thy
doc-src/TutorialI/ToyList/document/ToyList.tex
doc-src/TutorialI/basics.tex
doc-src/TutorialI/fp.tex
doc-src/TutorialI/tutorial.sty
doc-src/TutorialI/tutorial.tex
     1.1 --- a/doc-src/TutorialI/Ifexpr/Ifexpr.thy	Wed Jul 25 18:21:01 2001 +0200
     1.2 +++ b/doc-src/TutorialI/Ifexpr/Ifexpr.thy	Thu Jul 26 16:43:02 2001 +0200
     1.3 @@ -4,7 +4,7 @@
     1.4  
     1.5  subsection{*Case Study: Boolean Expressions*}
     1.6  
     1.7 -text{*\label{sec:boolex}
     1.8 +text{*\label{sec:boolex}\index{boolean expressions example|(}
     1.9  The aim of this case study is twofold: it shows how to model boolean
    1.10  expressions and some algorithms for manipulating them, and it demonstrates
    1.11  the constructs introduced above.
    1.12 @@ -120,7 +120,7 @@
    1.13  "norm (IF b t e) = normif b (norm t) (norm e)";
    1.14  
    1.15  text{*\noindent
    1.16 -Their interplay is a bit tricky, and we leave it to the reader to develop an
    1.17 +Their interplay is tricky; we leave it to you to develop an
    1.18  intuitive understanding. Fortunately, Isabelle can help us to verify that the
    1.19  transformation preserves the value of the expression:
    1.20  *}
    1.21 @@ -129,7 +129,7 @@
    1.22  
    1.23  text{*\noindent
    1.24  The proof is canonical, provided we first show the following simplification
    1.25 -lemma (which also helps to understand what @{term"normif"} does):
    1.26 +lemma, which also helps to understand what @{term"normif"} does:
    1.27  *}
    1.28  
    1.29  lemma [simp]:
    1.30 @@ -147,7 +147,7 @@
    1.31  of the theorem shown above because of the @{text"[simp]"} attribute.
    1.32  
    1.33  But how can we be sure that @{term"norm"} really produces a normal form in
    1.34 -the above sense? We define a function that tests If-expressions for normality
    1.35 +the above sense? We define a function that tests If-expressions for normality:
    1.36  *}
    1.37  
    1.38  consts normal :: "ifex \<Rightarrow> bool";
    1.39 @@ -158,7 +158,7 @@
    1.40       (case b of CIF b \<Rightarrow> True | VIF x \<Rightarrow> True | IF x y z \<Rightarrow> False))";
    1.41  
    1.42  text{*\noindent
    1.43 -and prove @{term"normal(norm b)"}. Of course, this requires a lemma about
    1.44 +Now we prove @{term"normal(norm b)"}. Of course, this requires a lemma about
    1.45  normality of @{term"normif"}:
    1.46  *}
    1.47  
    1.48 @@ -186,6 +186,7 @@
    1.49    some of the goals as implications (@{text"\<longrightarrow>"}) rather than
    1.50    equalities (@{text"="}).)
    1.51  \end{exercise}
    1.52 +\index{boolean expressions example|)}
    1.53  *}
    1.54  (*<*)
    1.55  end
     2.1 --- a/doc-src/TutorialI/Ifexpr/document/Ifexpr.tex	Wed Jul 25 18:21:01 2001 +0200
     2.2 +++ b/doc-src/TutorialI/Ifexpr/document/Ifexpr.tex	Thu Jul 26 16:43:02 2001 +0200
     2.3 @@ -6,7 +6,7 @@
     2.4  }
     2.5  %
     2.6  \begin{isamarkuptext}%
     2.7 -\label{sec:boolex}
     2.8 +\label{sec:boolex}\index{boolean expressions example|(}
     2.9  The aim of this case study is twofold: it shows how to model boolean
    2.10  expressions and some algorithms for manipulating them, and it demonstrates
    2.11  the constructs introduced above.%
    2.12 @@ -114,7 +114,7 @@
    2.13  {\isachardoublequote}norm\ {\isacharparenleft}IF\ b\ t\ e{\isacharparenright}\ {\isacharequal}\ normif\ b\ {\isacharparenleft}norm\ t{\isacharparenright}\ {\isacharparenleft}norm\ e{\isacharparenright}{\isachardoublequote}%
    2.14  \begin{isamarkuptext}%
    2.15  \noindent
    2.16 -Their interplay is a bit tricky, and we leave it to the reader to develop an
    2.17 +Their interplay is tricky; we leave it to you to develop an
    2.18  intuitive understanding. Fortunately, Isabelle can help us to verify that the
    2.19  transformation preserves the value of the expression:%
    2.20  \end{isamarkuptext}%
    2.21 @@ -122,7 +122,7 @@
    2.22  \begin{isamarkuptext}%
    2.23  \noindent
    2.24  The proof is canonical, provided we first show the following simplification
    2.25 -lemma (which also helps to understand what \isa{normif} does):%
    2.26 +lemma, which also helps to understand what \isa{normif} does:%
    2.27  \end{isamarkuptext}%
    2.28  \isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\isanewline
    2.29  \ \ {\isachardoublequote}{\isasymforall}t\ e{\isachardot}\ valif\ {\isacharparenleft}normif\ b\ t\ e{\isacharparenright}\ env\ {\isacharequal}\ valif\ {\isacharparenleft}IF\ b\ t\ e{\isacharparenright}\ env{\isachardoublequote}%
    2.30 @@ -132,7 +132,7 @@
    2.31  of the theorem shown above because of the \isa{{\isacharbrackleft}simp{\isacharbrackright}} attribute.
    2.32  
    2.33  But how can we be sure that \isa{norm} really produces a normal form in
    2.34 -the above sense? We define a function that tests If-expressions for normality%
    2.35 +the above sense? We define a function that tests If-expressions for normality:%
    2.36  \end{isamarkuptext}%
    2.37  \isacommand{consts}\ normal\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}ifex\ {\isasymRightarrow}\ bool{\isachardoublequote}\isanewline
    2.38  \isacommand{primrec}\isanewline
    2.39 @@ -142,7 +142,7 @@
    2.40  \ \ \ \ \ {\isacharparenleft}case\ b\ of\ CIF\ b\ {\isasymRightarrow}\ True\ {\isacharbar}\ VIF\ x\ {\isasymRightarrow}\ True\ {\isacharbar}\ IF\ x\ y\ z\ {\isasymRightarrow}\ False{\isacharparenright}{\isacharparenright}{\isachardoublequote}%
    2.41  \begin{isamarkuptext}%
    2.42  \noindent
    2.43 -and prove \isa{normal\ {\isacharparenleft}norm\ b{\isacharparenright}}. Of course, this requires a lemma about
    2.44 +Now we prove \isa{normal\ {\isacharparenleft}norm\ b{\isacharparenright}}. Of course, this requires a lemma about
    2.45  normality of \isa{normif}:%
    2.46  \end{isamarkuptext}%
    2.47  \isacommand{lemma}{\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isasymforall}t\ e{\isachardot}\ normal{\isacharparenleft}normif\ b\ t\ e{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}normal\ t\ {\isasymand}\ normal\ e{\isacharparenright}{\isachardoublequote}%
    2.48 @@ -160,7 +160,8 @@
    2.49    development to this changed requirement. (Hint: you may need to formulate
    2.50    some of the goals as implications (\isa{{\isasymlongrightarrow}}) rather than
    2.51    equalities (\isa{{\isacharequal}}).)
    2.52 -\end{exercise}%
    2.53 +\end{exercise}
    2.54 +\index{boolean expressions example|)}%
    2.55  \end{isamarkuptext}%
    2.56  \end{isabellebody}%
    2.57  %%% Local Variables:
     3.1 --- a/doc-src/TutorialI/Misc/Translations.thy	Wed Jul 25 18:21:01 2001 +0200
     3.2 +++ b/doc-src/TutorialI/Misc/Translations.thy	Thu Jul 26 16:43:02 2001 +0200
     3.3 @@ -4,34 +4,34 @@
     3.4  subsection{*Syntax Translations*}
     3.5  
     3.6  text{*\label{sec:def-translations}
     3.7 -\indexbold{syntax translations|(}%
     3.8 -\indexbold{translations@\isacommand {translations} (command)|(}
     3.9 -Isabelle offers an additional definition-like facility,
    3.10 +\index{syntax translations|(}%
    3.11 +\index{translations@\isacommand {translations} (command)|(}
    3.12 +Isabelle offers an additional definitional facility,
    3.13  \textbf{syntax translations}.
    3.14  They resemble macros: upon parsing, the defined concept is immediately
    3.15 -replaced by its definition, and this is reversed upon printing. For example,
    3.16 +replaced by its definition.  This effect is reversed upon printing.  For example,
    3.17  the symbol @{text"\<noteq>"} is defined via a syntax translation:
    3.18  *}
    3.19  
    3.20  translations "x \<noteq> y" \<rightleftharpoons> "\<not>(x = y)"
    3.21  
    3.22 -text{*\indexbold{$IsaEqTrans@\isasymrightleftharpoons}
    3.23 +text{*\index{$IsaEqTrans@\isasymrightleftharpoons}
    3.24  \noindent
    3.25  Internally, @{text"\<noteq>"} never appears.
    3.26  
    3.27  In addition to @{text"\<rightleftharpoons>"} there are
    3.28 -@{text"\<rightharpoonup>"}\indexbold{$IsaEqTrans1@\isasymrightharpoonup}
    3.29 -and @{text"\<leftharpoondown>"}\indexbold{$IsaEqTrans2@\isasymleftharpoondown}
    3.30 +@{text"\<rightharpoonup>"}\index{$IsaEqTrans1@\isasymrightharpoonup}
    3.31 +and @{text"\<leftharpoondown>"}\index{$IsaEqTrans2@\isasymleftharpoondown}
    3.32  for uni-directional translations, which only affect
    3.33 -parsing or printing.  We do not want to cover the details of
    3.34 -translations at this point.  We have mentioned the concept merely because it
    3.35 -crops up occasionally: a number of HOL's built-in constructs are defined
    3.36 +parsing or printing.  This tutorial will not cover the details of
    3.37 +translations.  We have mentioned the concept merely because it
    3.38 +crops up occasionally; a number of HOL's built-in constructs are defined
    3.39  via translations.  Translations are preferable to definitions when the new 
    3.40  concept is a trivial variation on an existing one.  For example, we
    3.41  don't need to derive new theorems about @{text"\<noteq>"}, since existing theorems
    3.42  about @{text"="} still apply.%
    3.43 -\indexbold{syntax translations|)}%
    3.44 -\indexbold{translations@\isacommand {translations} (command)|)}
    3.45 +\index{syntax translations|)}%
    3.46 +\index{translations@\isacommand {translations} (command)|)}
    3.47  *}
    3.48  
    3.49  (*<*)
     4.1 --- a/doc-src/TutorialI/Misc/Tree.thy	Wed Jul 25 18:21:01 2001 +0200
     4.2 +++ b/doc-src/TutorialI/Misc/Tree.thy	Thu Jul 26 16:43:02 2001 +0200
     4.3 @@ -3,7 +3,7 @@
     4.4  (*>*)
     4.5  
     4.6  text{*\noindent
     4.7 -Define the datatype of binary trees
     4.8 +Define the datatype of \rmindex{binary trees}:
     4.9  *}
    4.10  
    4.11  datatype 'a tree = Tip | Node "'a tree" 'a "'a tree";(*<*)
    4.12 @@ -14,7 +14,7 @@
    4.13  "mirror (Node l x r) = Node (mirror r) x (mirror l)";(*>*)
    4.14  
    4.15  text{*\noindent
    4.16 -and a function @{term"mirror"} that mirrors a binary tree
    4.17 +Define a function @{term"mirror"} that mirrors a binary tree
    4.18  by swapping subtrees recursively. Prove
    4.19  *}
    4.20  
     5.1 --- a/doc-src/TutorialI/Misc/case_exprs.thy	Wed Jul 25 18:21:01 2001 +0200
     5.2 +++ b/doc-src/TutorialI/Misc/case_exprs.thy	Thu Jul 26 16:43:02 2001 +0200
     5.3 @@ -4,8 +4,8 @@
     5.4  
     5.5  subsection{*Case Expressions*}
     5.6  
     5.7 -text{*\label{sec:case-expressions}
     5.8 -HOL also features \sdx{case}-expressions for analyzing
     5.9 +text{*\label{sec:case-expressions}\index{*case expressions}%
    5.10 +HOL also features \isa{case}-expressions for analyzing
    5.11  elements of a datatype. For example,
    5.12  @{term[display]"case xs of [] => 1 | y#ys => y"}
    5.13  evaluates to @{term"1"} if @{term"xs"} is @{term"[]"} and to @{term"y"} if 
    5.14 @@ -43,14 +43,11 @@
    5.15  subsection{*Structural Induction and Case Distinction*}
    5.16  
    5.17  text{*\label{sec:struct-ind-case}
    5.18 -\indexbold{structural induction}
    5.19 -\indexbold{induction!structural}
    5.20 -\indexbold{case distinction}
    5.21 -Almost all the basic laws about a datatype are applied automatically during
    5.22 -simplification. Only induction is invoked by hand via \methdx{induct_tac},
    5.23 -which works for any datatype. In some cases, induction is overkill and a case
    5.24 -distinction over all constructors of the datatype suffices. This is performed
    5.25 -by \methdx{case_tac}. A trivial example:
    5.26 +\index{case distinctions}\index{induction!structural}%
    5.27 +Induction is invoked by \methdx{induct_tac}, as we have seen above; 
    5.28 +it works for any datatype.  In some cases, induction is overkill and a case
    5.29 +distinction over all constructors of the datatype suffices.  This is performed
    5.30 +by \methdx{case_tac}.  Here is a trivial example:
    5.31  *}
    5.32  
    5.33  lemma "(case xs of [] \<Rightarrow> [] | y#ys \<Rightarrow> xs) = xs";
    5.34 @@ -67,8 +64,11 @@
    5.35  text{*
    5.36  Note that we do not need to give a lemma a name if we do not intend to refer
    5.37  to it explicitly in the future.
    5.38 +Other basic laws about a datatype are applied automatically during
    5.39 +simplification, so no special methods are provided for them.
    5.40  
    5.41  \begin{warn}
    5.42 + 
    5.43    Induction is only allowed on free (or \isasymAnd-bound) variables that
    5.44    should not occur among the assumptions of the subgoal; see
    5.45    \S\ref{sec:ind-var-in-prems} for details. Case distinction
     6.1 --- a/doc-src/TutorialI/Misc/document/Translations.tex	Wed Jul 25 18:21:01 2001 +0200
     6.2 +++ b/doc-src/TutorialI/Misc/document/Translations.tex	Thu Jul 26 16:43:02 2001 +0200
     6.3 @@ -7,33 +7,33 @@
     6.4  %
     6.5  \begin{isamarkuptext}%
     6.6  \label{sec:def-translations}
     6.7 -\indexbold{syntax translations|(}%
     6.8 -\indexbold{translations@\isacommand {translations} (command)|(}
     6.9 -Isabelle offers an additional definition-like facility,
    6.10 +\index{syntax translations|(}%
    6.11 +\index{translations@\isacommand {translations} (command)|(}
    6.12 +Isabelle offers an additional definitional facility,
    6.13  \textbf{syntax translations}.
    6.14  They resemble macros: upon parsing, the defined concept is immediately
    6.15 -replaced by its definition, and this is reversed upon printing. For example,
    6.16 +replaced by its definition.  This effect is reversed upon printing.  For example,
    6.17  the symbol \isa{{\isasymnoteq}} is defined via a syntax translation:%
    6.18  \end{isamarkuptext}%
    6.19  \isacommand{translations}\ {\isachardoublequote}x\ {\isasymnoteq}\ y{\isachardoublequote}\ {\isasymrightleftharpoons}\ {\isachardoublequote}{\isasymnot}{\isacharparenleft}x\ {\isacharequal}\ y{\isacharparenright}{\isachardoublequote}%
    6.20  \begin{isamarkuptext}%
    6.21 -\indexbold{$IsaEqTrans@\isasymrightleftharpoons}
    6.22 +\index{$IsaEqTrans@\isasymrightleftharpoons}
    6.23  \noindent
    6.24  Internally, \isa{{\isasymnoteq}} never appears.
    6.25  
    6.26  In addition to \isa{{\isasymrightleftharpoons}} there are
    6.27 -\isa{{\isasymrightharpoonup}}\indexbold{$IsaEqTrans1@\isasymrightharpoonup}
    6.28 -and \isa{{\isasymleftharpoondown}}\indexbold{$IsaEqTrans2@\isasymleftharpoondown}
    6.29 +\isa{{\isasymrightharpoonup}}\index{$IsaEqTrans1@\isasymrightharpoonup}
    6.30 +and \isa{{\isasymleftharpoondown}}\index{$IsaEqTrans2@\isasymleftharpoondown}
    6.31  for uni-directional translations, which only affect
    6.32 -parsing or printing.  We do not want to cover the details of
    6.33 -translations at this point.  We have mentioned the concept merely because it
    6.34 -crops up occasionally: a number of HOL's built-in constructs are defined
    6.35 +parsing or printing.  This tutorial will not cover the details of
    6.36 +translations.  We have mentioned the concept merely because it
    6.37 +crops up occasionally; a number of HOL's built-in constructs are defined
    6.38  via translations.  Translations are preferable to definitions when the new 
    6.39  concept is a trivial variation on an existing one.  For example, we
    6.40  don't need to derive new theorems about \isa{{\isasymnoteq}}, since existing theorems
    6.41  about \isa{{\isacharequal}} still apply.%
    6.42 -\indexbold{syntax translations|)}%
    6.43 -\indexbold{translations@\isacommand {translations} (command)|)}%
    6.44 +\index{syntax translations|)}%
    6.45 +\index{translations@\isacommand {translations} (command)|)}%
    6.46  \end{isamarkuptext}%
    6.47  \end{isabellebody}%
    6.48  %%% Local Variables:
     7.1 --- a/doc-src/TutorialI/Misc/document/Tree.tex	Wed Jul 25 18:21:01 2001 +0200
     7.2 +++ b/doc-src/TutorialI/Misc/document/Tree.tex	Thu Jul 26 16:43:02 2001 +0200
     7.3 @@ -4,12 +4,12 @@
     7.4  %
     7.5  \begin{isamarkuptext}%
     7.6  \noindent
     7.7 -Define the datatype of binary trees%
     7.8 +Define the datatype of \rmindex{binary trees}:%
     7.9  \end{isamarkuptext}%
    7.10  \isacommand{datatype}\ {\isacharprime}a\ tree\ {\isacharequal}\ Tip\ {\isacharbar}\ Node\ {\isachardoublequote}{\isacharprime}a\ tree{\isachardoublequote}\ {\isacharprime}a\ {\isachardoublequote}{\isacharprime}a\ tree{\isachardoublequote}%
    7.11  \begin{isamarkuptext}%
    7.12  \noindent
    7.13 -and a function \isa{mirror} that mirrors a binary tree
    7.14 +Define a function \isa{mirror} that mirrors a binary tree
    7.15  by swapping subtrees recursively. Prove%
    7.16  \end{isamarkuptext}%
    7.17  \isacommand{lemma}\ mirror{\isacharunderscore}mirror{\isacharcolon}\ {\isachardoublequote}mirror{\isacharparenleft}mirror\ t{\isacharparenright}\ {\isacharequal}\ t{\isachardoublequote}%
     8.1 --- a/doc-src/TutorialI/Misc/document/case_exprs.tex	Wed Jul 25 18:21:01 2001 +0200
     8.2 +++ b/doc-src/TutorialI/Misc/document/case_exprs.tex	Thu Jul 26 16:43:02 2001 +0200
     8.3 @@ -6,8 +6,8 @@
     8.4  }
     8.5  %
     8.6  \begin{isamarkuptext}%
     8.7 -\label{sec:case-expressions}
     8.8 -HOL also features \sdx{case}-expressions for analyzing
     8.9 +\label{sec:case-expressions}\index{*case expressions}%
    8.10 +HOL also features \isa{case}-expressions for analyzing
    8.11  elements of a datatype. For example,
    8.12  \begin{isabelle}%
    8.13  \ \ \ \ \ case\ xs\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ {\isadigit{1}}\ {\isacharbar}\ y\ {\isacharhash}\ ys\ {\isasymRightarrow}\ y%
    8.14 @@ -54,14 +54,11 @@
    8.15  %
    8.16  \begin{isamarkuptext}%
    8.17  \label{sec:struct-ind-case}
    8.18 -\indexbold{structural induction}
    8.19 -\indexbold{induction!structural}
    8.20 -\indexbold{case distinction}
    8.21 -Almost all the basic laws about a datatype are applied automatically during
    8.22 -simplification. Only induction is invoked by hand via \methdx{induct_tac},
    8.23 -which works for any datatype. In some cases, induction is overkill and a case
    8.24 -distinction over all constructors of the datatype suffices. This is performed
    8.25 -by \methdx{case_tac}. A trivial example:%
    8.26 +\index{case distinctions}\index{induction!structural}%
    8.27 +Induction is invoked by \methdx{induct_tac}, as we have seen above; 
    8.28 +it works for any datatype.  In some cases, induction is overkill and a case
    8.29 +distinction over all constructors of the datatype suffices.  This is performed
    8.30 +by \methdx{case_tac}.  Here is a trivial example:%
    8.31  \end{isamarkuptext}%
    8.32  \isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}case\ xs\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbar}\ y{\isacharhash}ys\ {\isasymRightarrow}\ xs{\isacharparenright}\ {\isacharequal}\ xs{\isachardoublequote}\isanewline
    8.33  \isacommand{apply}{\isacharparenleft}case{\isacharunderscore}tac\ xs{\isacharparenright}%
    8.34 @@ -79,8 +76,11 @@
    8.35  \begin{isamarkuptext}%
    8.36  Note that we do not need to give a lemma a name if we do not intend to refer
    8.37  to it explicitly in the future.
    8.38 +Other basic laws about a datatype are applied automatically during
    8.39 +simplification, so no special methods are provided for them.
    8.40  
    8.41  \begin{warn}
    8.42 + 
    8.43    Induction is only allowed on free (or \isasymAnd-bound) variables that
    8.44    should not occur among the assumptions of the subgoal; see
    8.45    \S\ref{sec:ind-var-in-prems} for details. Case distinction
     9.1 --- a/doc-src/TutorialI/Misc/document/natsum.tex	Wed Jul 25 18:21:01 2001 +0200
     9.2 +++ b/doc-src/TutorialI/Misc/document/natsum.tex	Thu Jul 26 16:43:02 2001 +0200
     9.3 @@ -24,6 +24,7 @@
     9.4  \begin{isamarkuptext}%
     9.5  \newcommand{\mystar}{*%
     9.6  }
     9.7 +\index{arithmetic operations!for \protect\isa{nat}}%
     9.8  The usual arithmetic operations \ttindexboldpos{+}{$HOL2arithfun},
     9.9  \ttindexboldpos{-}{$HOL2arithfun}, \ttindexboldpos{\mystar}{$HOL2arithfun},
    9.10  \sdx{div}, \sdx{mod}, \cdx{min} and
    9.11 @@ -31,13 +32,15 @@
    9.12  \indexboldpos{\isasymle}{$HOL2arithrel} and
    9.13  \ttindexboldpos{<}{$HOL2arithrel}. As usual, \isa{m\ {\isacharminus}\ n\ {\isacharequal}\ {\isadigit{0}}} if
    9.14  \isa{m\ {\isacharless}\ n}. There is even a least number operation
    9.15 -\sdx{LEAST}\@.  For example, \isa{{\isacharparenleft}LEAST\ n{\isachardot}\ {\isadigit{1}}\ {\isacharless}\ n{\isacharparenright}\ {\isacharequal}\ {\isadigit{2}}}, although
    9.16 -Isabelle does not prove this automatically. Note that \isa{{\isadigit{1}}}
    9.17 +\sdx{LEAST}\@.  For example, \isa{{\isacharparenleft}LEAST\ n{\isachardot}\ {\isadigit{1}}\ {\isacharless}\ n{\isacharparenright}\ {\isacharequal}\ {\isadigit{2}}}. 
    9.18 +\REMARK{Isabelle CAN prove it automatically, using \isa{auto intro: Least_equality}.
    9.19 + The following needs changing with our new system of numbers.}
    9.20 +Note that \isa{{\isadigit{1}}}
    9.21  and \isa{{\isadigit{2}}} are available as abbreviations for the corresponding
    9.22  \isa{Suc}-expressions. If you need the full set of numerals,
    9.23  see~\S\ref{sec:numerals}.
    9.24  
    9.25 -\begin{warn}
    9.26 +\begin{warn}\index{overloading}
    9.27    The constant \cdx{0} and the operations
    9.28    \ttindexboldpos{+}{$HOL2arithfun}, \ttindexboldpos{-}{$HOL2arithfun},
    9.29    \ttindexboldpos{\mystar}{$HOL2arithfun}, \cdx{min},
    9.30 @@ -60,23 +63,23 @@
    9.31    operations.
    9.32  \end{warn}
    9.33  
    9.34 -Simple arithmetic goals are proved automatically by both \isa{auto} and the
    9.35 -simplification method introduced in \S\ref{sec:Simplification}.  For
    9.36 -example,%
    9.37 +Both \isa{auto} and \isa{simp}
    9.38 +(a method introduced below, \S\ref{sec:Simplification}) prove 
    9.39 +simple arithmetic goals automatically:%
    9.40  \end{isamarkuptext}%
    9.41  \isacommand{lemma}\ {\isachardoublequote}{\isasymlbrakk}\ {\isasymnot}\ m\ {\isacharless}\ n{\isacharsemicolon}\ m\ {\isacharless}\ n{\isacharplus}{\isadigit{1}}\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ m\ {\isacharequal}\ n{\isachardoublequote}%
    9.42  \begin{isamarkuptext}%
    9.43  \noindent
    9.44 -is proved automatically. The main restriction is that only addition is taken
    9.45 -into account; other arithmetic operations and quantified formulae are ignored.
    9.46 +For efficiency's sake, this built-in prover ignores quantified formulae and all 
    9.47 +arithmetic operations apart from addition.
    9.48  
    9.49 -For more complex goals, there is the special method \methdx{arith}
    9.50 -(which attacks the first subgoal). It proves arithmetic goals involving the
    9.51 +The method \methdx{arith} is more general.  It attempts to prove
    9.52 +the first subgoal provided it is a quantifier free \textbf{linear arithmetic} formula.
    9.53 +Such formulas may involve the
    9.54  usual logical connectives (\isa{{\isasymnot}}, \isa{{\isasymand}}, \isa{{\isasymor}},
    9.55  \isa{{\isasymlongrightarrow}}), the relations \isa{{\isacharequal}}, \isa{{\isasymle}} and \isa{{\isacharless}},
    9.56  and the operations
    9.57 -\isa{{\isacharplus}}, \isa{{\isacharminus}}, \isa{min} and \isa{max}. Technically, this is
    9.58 -known as the class of (quantifier free) \textbf{linear arithmetic} formulae.
    9.59 +\isa{{\isacharplus}}, \isa{{\isacharminus}}, \isa{min} and \isa{max}. 
    9.60  For example,%
    9.61  \end{isamarkuptext}%
    9.62  \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.63 @@ -88,7 +91,7 @@
    9.64  \isacommand{lemma}\ {\isachardoublequote}n{\isacharasterisk}n\ {\isacharequal}\ n\ {\isasymLongrightarrow}\ n{\isacharequal}{\isadigit{0}}\ {\isasymor}\ n{\isacharequal}{\isadigit{1}}{\isachardoublequote}%
    9.65  \begin{isamarkuptext}%
    9.66  \noindent
    9.67 -is not even proved by \isa{arith} because the proof relies essentially
    9.68 +is not proved even by \isa{arith} because the proof relies 
    9.69  on properties of multiplication.
    9.70  
    9.71  \begin{warn}
    9.72 @@ -96,10 +99,9 @@
    9.73    of \ttindexboldpos{-}{$HOL2arithfun}, \cdx{min} and
    9.74    \cdx{max} because they are first eliminated by case distinctions.
    9.75  
    9.76 -  \isa{arith} is incomplete even for the restricted class of
    9.77 -  linear arithmetic formulae. If divisibility plays a
    9.78 +  Even for linear arithmetic formulae, \isa{arith} is incomplete. If divisibility plays a
    9.79    role, it may fail to prove a valid formula, for example
    9.80 -  \isa{m\ {\isacharplus}\ m\ {\isasymnoteq}\ n\ {\isacharplus}\ n\ {\isacharplus}\ {\isadigit{1}}}. Fortunately, such examples are rare in practice.
    9.81 +  \isa{m\ {\isacharplus}\ m\ {\isasymnoteq}\ n\ {\isacharplus}\ n\ {\isacharplus}\ {\isadigit{1}}}. Fortunately, such examples are rare.
    9.82  \end{warn}%
    9.83  \end{isamarkuptext}%
    9.84  \end{isabellebody}%
    10.1 --- a/doc-src/TutorialI/Misc/document/pairs.tex	Wed Jul 25 18:21:01 2001 +0200
    10.2 +++ b/doc-src/TutorialI/Misc/document/pairs.tex	Thu Jul 26 16:43:02 2001 +0200
    10.3 @@ -18,7 +18,7 @@
    10.4  \begin{itemize}
    10.5  \item
    10.6  There is also the type \tydx{unit}, which contains exactly one
    10.7 -element denoted by \ttindexboldpos{()}{$Isatype}. This type can be viewed
    10.8 +element denoted by~\cdx{()}.  This type can be viewed
    10.9  as a degenerate product with 0 components.
   10.10  \item
   10.11  Products, like type \isa{nat}, are datatypes, which means
    11.1 --- a/doc-src/TutorialI/Misc/document/prime_def.tex	Wed Jul 25 18:21:01 2001 +0200
    11.2 +++ b/doc-src/TutorialI/Misc/document/prime_def.tex	Thu Jul 26 16:43:02 2001 +0200
    11.3 @@ -5,14 +5,14 @@
    11.4  \begin{isamarkuptext}%
    11.5  \begin{warn}
    11.6  A common mistake when writing definitions is to introduce extra free
    11.7 -variables on the right-hand side as in the following fictitious definition:
    11.8 +variables on the right-hand side.  Consider the following, flawed definition
    11.9 +(where \isa{dvd} means ``divides''):
   11.10  \begin{isabelle}%
   11.11  \ \ \ \ \ {\isachardoublequote}prime\ p\ {\isasymequiv}\ {\isadigit{1}}\ {\isacharless}\ p\ {\isasymand}\ {\isacharparenleft}m\ dvd\ p\ {\isasymlongrightarrow}\ m\ {\isacharequal}\ {\isadigit{1}}\ {\isasymor}\ m\ {\isacharequal}\ p{\isacharparenright}{\isachardoublequote}%
   11.12  \end{isabelle}
   11.13 -where \isa{dvd} means ``divides''.
   11.14  Isabelle rejects this ``definition'' because of the extra \isa{m} on the
   11.15 -right-hand side, which would introduce an inconsistency (why?). What you
   11.16 -should have written is
   11.17 +right-hand side, which would introduce an inconsistency (why?). 
   11.18 +The correct version is
   11.19  \begin{isabelle}%
   11.20  \ \ \ \ \ {\isachardoublequote}prime\ p\ {\isasymequiv}\ {\isadigit{1}}\ {\isacharless}\ p\ {\isasymand}\ {\isacharparenleft}{\isasymforall}m{\isachardot}\ m\ dvd\ p\ {\isasymlongrightarrow}\ m\ {\isacharequal}\ {\isadigit{1}}\ {\isasymor}\ m\ {\isacharequal}\ p{\isacharparenright}{\isachardoublequote}%
   11.21  \end{isabelle}
    12.1 --- a/doc-src/TutorialI/Misc/document/types.tex	Wed Jul 25 18:21:01 2001 +0200
    12.2 +++ b/doc-src/TutorialI/Misc/document/types.tex	Thu Jul 26 16:43:02 2001 +0200
    12.3 @@ -9,7 +9,7 @@
    12.4  Internally all synonyms are fully expanded.  As a consequence Isabelle's
    12.5  output never contains synonyms.  Their main purpose is to improve the
    12.6  readability of theories.  Synonyms can be used just like any other
    12.7 -type:%
    12.8 +type.  Here, we declare two constants of type \isa{gate}:%
    12.9  \end{isamarkuptext}%
   12.10  \isacommand{consts}\ nand\ {\isacharcolon}{\isacharcolon}\ gate\isanewline
   12.11  \ \ \ \ \ \ \ xor\ \ {\isacharcolon}{\isacharcolon}\ gate%
   12.12 @@ -18,19 +18,20 @@
   12.13  %
   12.14  \begin{isamarkuptext}%
   12.15  \label{sec:ConstDefinitions}\indexbold{definitions}%
   12.16 -The above constants \isa{nand} and \isa{xor} are non-recursive and can
   12.17 -therefore be defined directly by%
   12.18 +The constants \isa{nand} and \isa{xor} above are non-recursive and can 
   12.19 +be defined directly:%
   12.20  \end{isamarkuptext}%
   12.21  \isacommand{defs}\ nand{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequote}nand\ A\ B\ {\isasymequiv}\ {\isasymnot}{\isacharparenleft}A\ {\isasymand}\ B{\isacharparenright}{\isachardoublequote}\isanewline
   12.22  \ \ \ \ \ xor{\isacharunderscore}def{\isacharcolon}\ \ {\isachardoublequote}xor\ A\ B\ \ {\isasymequiv}\ A\ {\isasymand}\ {\isasymnot}B\ {\isasymor}\ {\isasymnot}A\ {\isasymand}\ B{\isachardoublequote}%
   12.23  \begin{isamarkuptext}%
   12.24  \noindent%
   12.25 -where \commdx{defs} is a keyword and
   12.26 +Here \commdx{defs} is a keyword and
   12.27  \isa{nand{\isacharunderscore}def} and \isa{xor{\isacharunderscore}def} are user-supplied names.
   12.28  The symbol \indexboldpos{\isasymequiv}{$IsaEq} is a special form of equality
   12.29  that must be used in constant definitions.
   12.30 -Declarations and definitions can also be merged in a \commdx{constdefs} 
   12.31 -command:%
   12.32 +A \commdx{constdefs} command combines the effects of \isacommand{consts} and 
   12.33 +\isacommand{defs}.  For instance, we can introduce \isa{nand} and \isa{xor} by a 
   12.34 +single command:%
   12.35  \end{isamarkuptext}%
   12.36  \isacommand{constdefs}\ nor\ {\isacharcolon}{\isacharcolon}\ gate\isanewline
   12.37  \ \ \ \ \ \ \ \ \ {\isachardoublequote}nor\ A\ B\ {\isasymequiv}\ {\isasymnot}{\isacharparenleft}A\ {\isasymor}\ B{\isacharparenright}{\isachardoublequote}\isanewline
    13.1 --- a/doc-src/TutorialI/Misc/natsum.thy	Wed Jul 25 18:21:01 2001 +0200
    13.2 +++ b/doc-src/TutorialI/Misc/natsum.thy	Thu Jul 26 16:43:02 2001 +0200
    13.3 @@ -22,6 +22,7 @@
    13.4  
    13.5  text{*\newcommand{\mystar}{*%
    13.6  }
    13.7 +\index{arithmetic operations!for \protect\isa{nat}}%
    13.8  The usual arithmetic operations \ttindexboldpos{+}{$HOL2arithfun},
    13.9  \ttindexboldpos{-}{$HOL2arithfun}, \ttindexboldpos{\mystar}{$HOL2arithfun},
   13.10  \sdx{div}, \sdx{mod}, \cdx{min} and
   13.11 @@ -29,13 +30,15 @@
   13.12  \indexboldpos{\isasymle}{$HOL2arithrel} and
   13.13  \ttindexboldpos{<}{$HOL2arithrel}. As usual, @{prop"m-n = 0"} if
   13.14  @{prop"m<n"}. There is even a least number operation
   13.15 -\sdx{LEAST}\@.  For example, @{prop"(LEAST n. 1 < n) = 2"}, although
   13.16 -Isabelle does not prove this automatically. Note that @{term 1}
   13.17 +\sdx{LEAST}\@.  For example, @{prop"(LEAST n. 1 < n) = 2"}. 
   13.18 +\REMARK{Isabelle CAN prove it automatically, using \isa{auto intro: Least_equality}.
   13.19 + The following needs changing with our new system of numbers.}
   13.20 +Note that @{term 1}
   13.21  and @{term 2} are available as abbreviations for the corresponding
   13.22  @{term Suc}-expressions. If you need the full set of numerals,
   13.23  see~\S\ref{sec:numerals}.
   13.24  
   13.25 -\begin{warn}
   13.26 +\begin{warn}\index{overloading}
   13.27    The constant \cdx{0} and the operations
   13.28    \ttindexboldpos{+}{$HOL2arithfun}, \ttindexboldpos{-}{$HOL2arithfun},
   13.29    \ttindexboldpos{\mystar}{$HOL2arithfun}, \cdx{min},
   13.30 @@ -58,25 +61,25 @@
   13.31    operations.
   13.32  \end{warn}
   13.33  
   13.34 -Simple arithmetic goals are proved automatically by both @{term auto} and the
   13.35 -simplification method introduced in \S\ref{sec:Simplification}.  For
   13.36 -example,
   13.37 +Both @{text auto} and @{text simp}
   13.38 +(a method introduced below, \S\ref{sec:Simplification}) prove 
   13.39 +simple arithmetic goals automatically:
   13.40  *}
   13.41  
   13.42  lemma "\<lbrakk> \<not> m < n; m < n+1 \<rbrakk> \<Longrightarrow> m = n"
   13.43  (*<*)by(auto)(*>*)
   13.44  
   13.45  text{*\noindent
   13.46 -is proved automatically. The main restriction is that only addition is taken
   13.47 -into account; other arithmetic operations and quantified formulae are ignored.
   13.48 +For efficiency's sake, this built-in prover ignores quantified formulae and all 
   13.49 +arithmetic operations apart from addition.
   13.50  
   13.51 -For more complex goals, there is the special method \methdx{arith}
   13.52 -(which attacks the first subgoal). It proves arithmetic goals involving the
   13.53 +The method \methdx{arith} is more general.  It attempts to prove
   13.54 +the first subgoal provided it is a quantifier free \textbf{linear arithmetic} formula.
   13.55 +Such formulas may involve the
   13.56  usual logical connectives (@{text"\<not>"}, @{text"\<and>"}, @{text"\<or>"},
   13.57  @{text"\<longrightarrow>"}), the relations @{text"="}, @{text"\<le>"} and @{text"<"},
   13.58  and the operations
   13.59 -@{text"+"}, @{text"-"}, @{term min} and @{term max}. Technically, this is
   13.60 -known as the class of (quantifier free) \textbf{linear arithmetic} formulae.
   13.61 +@{text"+"}, @{text"-"}, @{term min} and @{term max}. 
   13.62  For example,
   13.63  *}
   13.64  
   13.65 @@ -92,7 +95,7 @@
   13.66  (*<*)oops(*>*)
   13.67  
   13.68  text{*\noindent
   13.69 -is not even proved by @{text arith} because the proof relies essentially
   13.70 +is not proved even by @{text arith} because the proof relies 
   13.71  on properties of multiplication.
   13.72  
   13.73  \begin{warn}
   13.74 @@ -100,10 +103,9 @@
   13.75    of \ttindexboldpos{-}{$HOL2arithfun}, \cdx{min} and
   13.76    \cdx{max} because they are first eliminated by case distinctions.
   13.77  
   13.78 -  \isa{arith} is incomplete even for the restricted class of
   13.79 -  linear arithmetic formulae. If divisibility plays a
   13.80 +  Even for linear arithmetic formulae, \isa{arith} is incomplete. If divisibility plays a
   13.81    role, it may fail to prove a valid formula, for example
   13.82 -  @{prop"m+m \<noteq> n+n+1"}. Fortunately, such examples are rare in practice.
   13.83 +  @{prop"m+m \<noteq> n+n+1"}. Fortunately, such examples are rare.
   13.84  \end{warn}
   13.85  *}
   13.86  
    14.1 --- a/doc-src/TutorialI/Misc/pairs.thy	Wed Jul 25 18:21:01 2001 +0200
    14.2 +++ b/doc-src/TutorialI/Misc/pairs.thy	Thu Jul 26 16:43:02 2001 +0200
    14.3 @@ -16,7 +16,7 @@
    14.4  \begin{itemize}
    14.5  \item
    14.6  There is also the type \tydx{unit}, which contains exactly one
    14.7 -element denoted by \ttindexboldpos{()}{$Isatype}. This type can be viewed
    14.8 +element denoted by~\cdx{()}.  This type can be viewed
    14.9  as a degenerate product with 0 components.
   14.10  \item
   14.11  Products, like type @{typ nat}, are datatypes, which means
    15.1 --- a/doc-src/TutorialI/Misc/prime_def.thy	Wed Jul 25 18:21:01 2001 +0200
    15.2 +++ b/doc-src/TutorialI/Misc/prime_def.thy	Thu Jul 26 16:43:02 2001 +0200
    15.3 @@ -5,12 +5,12 @@
    15.4  text{*
    15.5  \begin{warn}
    15.6  A common mistake when writing definitions is to introduce extra free
    15.7 -variables on the right-hand side as in the following fictitious definition:
    15.8 +variables on the right-hand side.  Consider the following, flawed definition
    15.9 +(where @{text"dvd"} means ``divides''):
   15.10  @{term[display,quotes]"prime(p) == 1 < p & (m dvd p --> (m=1 | m=p))"}
   15.11 -where @{text"dvd"} means ``divides''.
   15.12  Isabelle rejects this ``definition'' because of the extra @{term"m"} on the
   15.13 -right-hand side, which would introduce an inconsistency (why?). What you
   15.14 -should have written is
   15.15 +right-hand side, which would introduce an inconsistency (why?). 
   15.16 +The correct version is
   15.17  @{term[display,quotes]"prime(p) == 1 < p & (!m. m dvd p --> (m=1 | m=p))"}
   15.18  \end{warn}
   15.19  *}
    16.1 --- a/doc-src/TutorialI/Misc/types.thy	Wed Jul 25 18:21:01 2001 +0200
    16.2 +++ b/doc-src/TutorialI/Misc/types.thy	Thu Jul 26 16:43:02 2001 +0200
    16.3 @@ -7,7 +7,7 @@
    16.4  Internally all synonyms are fully expanded.  As a consequence Isabelle's
    16.5  output never contains synonyms.  Their main purpose is to improve the
    16.6  readability of theories.  Synonyms can be used just like any other
    16.7 -type:
    16.8 +type.  Here, we declare two constants of type \isa{gate}:
    16.9  *}
   16.10  
   16.11  consts nand :: gate
   16.12 @@ -16,20 +16,21 @@
   16.13  subsection{*Constant Definitions*}
   16.14  
   16.15  text{*\label{sec:ConstDefinitions}\indexbold{definitions}%
   16.16 -The above constants @{term"nand"} and @{term"xor"} are non-recursive and can
   16.17 -therefore be defined directly by
   16.18 +The constants @{term"nand"} and @{term"xor"} above are non-recursive and can 
   16.19 +be defined directly:
   16.20  *}
   16.21  
   16.22  defs nand_def: "nand A B \<equiv> \<not>(A \<and> B)"
   16.23       xor_def:  "xor A B  \<equiv> A \<and> \<not>B \<or> \<not>A \<and> B";
   16.24  
   16.25  text{*\noindent%
   16.26 -where \commdx{defs} is a keyword and
   16.27 +Here \commdx{defs} is a keyword and
   16.28  @{thm[source]nand_def} and @{thm[source]xor_def} are user-supplied names.
   16.29  The symbol \indexboldpos{\isasymequiv}{$IsaEq} is a special form of equality
   16.30  that must be used in constant definitions.
   16.31 -Declarations and definitions can also be merged in a \commdx{constdefs} 
   16.32 -command: 
   16.33 +A \commdx{constdefs} command combines the effects of \isacommand{consts} and 
   16.34 +\isacommand{defs}.  For instance, we can introduce @{term"nand"} and @{term"xor"} by a 
   16.35 +single command: 
   16.36  *}
   16.37  
   16.38  constdefs nor :: gate
    17.1 --- a/doc-src/TutorialI/Rules/Basic.thy	Wed Jul 25 18:21:01 2001 +0200
    17.2 +++ b/doc-src/TutorialI/Rules/Basic.thy	Thu Jul 26 16:43:02 2001 +0200
    17.3 @@ -309,13 +309,13 @@
    17.4  
    17.5  theorem Least_equality:
    17.6       "\<lbrakk> P (k::nat);  \<forall>x. P x \<longrightarrow> k \<le> x \<rbrakk> \<Longrightarrow> (LEAST x. P(x)) = k"
    17.7 -apply (simp add: Least_def LeastM_def)
    17.8 +apply (simp add: Least_def)
    17.9   
   17.10  txt{*omit maybe?
   17.11  @{subgoals[display,indent=0,margin=65]}
   17.12  *};
   17.13     
   17.14 -apply (rule some_equality)
   17.15 +apply (rule the_equality)
   17.16  
   17.17  txt{*
   17.18  @{subgoals[display,indent=0,margin=65]}
    18.1 --- a/doc-src/TutorialI/Rules/Force.thy	Wed Jul 25 18:21:01 2001 +0200
    18.2 +++ b/doc-src/TutorialI/Rules/Force.thy	Thu Jul 26 16:43:02 2001 +0200
    18.3 @@ -1,6 +1,7 @@
    18.4  (* ID:         $Id$ *)
    18.5 -theory Force = Divides: (*Divides rather than Main so that the first proof
    18.6 -                         isn't done by the nat_divide_cancel_factor simprocs.*)
    18.7 +theory Force = Main: 
    18.8 +  (*Use Divides rather than Main to experiment with the first proof.
    18.9 +    Otherwise, it is done by the nat_divide_cancel_factor simprocs.*)
   18.10  
   18.11  declare div_mult_self_is_m [simp del];
   18.12  
    19.1 --- a/doc-src/TutorialI/ToyList/ToyList.thy	Wed Jul 25 18:21:01 2001 +0200
    19.2 +++ b/doc-src/TutorialI/ToyList/ToyList.thy	Thu Jul 26 16:43:02 2001 +0200
    19.3 @@ -33,10 +33,11 @@
    19.4  The @{text 65} is the priority of the infix @{text"#"}.
    19.5  
    19.6  \begin{warn}
    19.7 -  Syntax annotations are a powerful but optional feature. You
    19.8 +  Syntax annotations are can be powerful, but they are difficult to master and 
    19.9 +  are never necessary.  You
   19.10    could drop them from theory @{text"ToyList"} and go back to the identifiers
   19.11    @{term[source]Nil} and @{term[source]Cons}.
   19.12 -  We recommend that novices avoid using
   19.13 +  Novices should avoid using
   19.14    syntax annotations in their own theories.
   19.15  \end{warn}
   19.16  Next, two functions @{text"app"} and \cdx{rev} are declared:
   19.17 @@ -49,7 +50,7 @@
   19.18  \noindent
   19.19  In contrast to many functional programming languages,
   19.20  Isabelle insists on explicit declarations of all functions
   19.21 -(keyword \isacommand{consts}).  Apart from the declaration-before-use
   19.22 +(keyword \commdx{consts}).  Apart from the declaration-before-use
   19.23  restriction, the order of items in a theory file is unconstrained. Function
   19.24  @{text"app"} is annotated with concrete syntax too. Instead of the
   19.25  prefix syntax @{text"app xs ys"} the infix
   19.26 @@ -66,7 +67,7 @@
   19.27  "rev (x # xs)  = (rev xs) @ (x # [])";
   19.28  
   19.29  text{*
   19.30 -\noindent
   19.31 +\noindent\index{*rev (constant)|(}\index{append function|(}
   19.32  The equations for @{text"app"} and @{term"rev"} hardly need comments:
   19.33  @{text"app"} appends two lists and @{term"rev"} reverses a list.  The
   19.34  keyword \commdx{primrec} indicates that the recursion is
   19.35 @@ -82,16 +83,16 @@
   19.36  % However, this is a subtle issue that we cannot discuss here further.
   19.37  
   19.38  \begin{warn}
   19.39 -  As we have indicated, the requirement for total functions is not a gratuitous
   19.40 -  restriction but an essential characteristic of HOL\@. It is only
   19.41 +  As we have indicated, the requirement for total functions is an essential characteristic of HOL\@. It is only
   19.42    because of totality that reasoning in HOL is comparatively easy.  More
   19.43 -  generally, the philosophy in HOL is not to allow arbitrary axioms (such as
   19.44 +  generally, the philosophy in HOL is to refrain from asserting arbitrary axioms (such as
   19.45    function definitions whose totality has not been proved) because they
   19.46    quickly lead to inconsistencies. Instead, fixed constructs for introducing
   19.47    types and functions are offered (such as \isacommand{datatype} and
   19.48    \isacommand{primrec}) which are guaranteed to preserve consistency.
   19.49  \end{warn}
   19.50  
   19.51 +\index{syntax}%
   19.52  A remark about syntax.  The textual definition of a theory follows a fixed
   19.53  syntax with keywords like \isacommand{datatype} and \isacommand{end}.
   19.54  % (see Fig.~\ref{fig:keywords} in Appendix~\ref{sec:Appendix} for a full list).
   19.55 @@ -108,7 +109,7 @@
   19.56  
   19.57  text{*\noindent
   19.58  When Isabelle prints a syntax error message, it refers to the HOL syntax as
   19.59 -the \bfindex{inner syntax} and the enclosing theory language as the \bfindex{outer syntax}.
   19.60 +the \textbf{inner syntax} and the enclosing theory language as the \textbf{outer syntax}.
   19.61  
   19.62  
   19.63  \section{An Introductory Proof}
   19.64 @@ -119,27 +120,24 @@
   19.65  illustrate not just the basic proof commands but also the typical proof
   19.66  process.
   19.67  
   19.68 -\subsubsection*{Main Goal: @{text"rev(rev xs) = xs"}.}
   19.69 +\subsubsection*{Main Goal}
   19.70  
   19.71  Our goal is to show that reversing a list twice produces the original
   19.72 -list. The input line
   19.73 +list.
   19.74  *}
   19.75  
   19.76  theorem rev_rev [simp]: "rev(rev xs) = xs";
   19.77  
   19.78  txt{*\index{theorem@\isacommand {theorem} (command)|bold}%
   19.79 -\index{*simp (attribute)|bold}
   19.80  \noindent
   19.81 -does several things.  It
   19.82 +This \isacommand{theorem} command does several things:
   19.83  \begin{itemize}
   19.84  \item
   19.85 -establishes a new theorem to be proved, namely @{prop"rev(rev xs) = xs"},
   19.86 +It establishes a new theorem to be proved, namely @{prop"rev(rev xs) = xs"}.
   19.87  \item
   19.88 -gives that theorem the name @{text"rev_rev"} by which it can be
   19.89 -referred to,
   19.90 +It gives that theorem the name @{text"rev_rev"}, for later reference.
   19.91  \item
   19.92 -and tells Isabelle (via @{text"[simp]"}) to use the theorem (once it has been
   19.93 -proved) as a simplification rule, i.e.\ all future proofs involving
   19.94 +It tells Isabelle (via the bracketed attribute \attrdx{simp}) to take the eventual theorem as a simplification rule: future proofs involving
   19.95  simplification will replace occurrences of @{term"rev(rev xs)"} by
   19.96  @{term"xs"}.
   19.97  
   19.98 @@ -156,7 +154,7 @@
   19.99  The first three lines tell us that we are 0 steps into the proof of
  19.100  theorem @{text"rev_rev"}; for compactness reasons we rarely show these
  19.101  initial lines in this tutorial. The remaining lines display the current
  19.102 -proof state.
  19.103 +\rmindex{proof state}.
  19.104  Until we have finished a proof, the proof state always looks like this:
  19.105  \begin{isabelle}
  19.106  $G$\isanewline
  19.107 @@ -167,7 +165,8 @@
  19.108  where $G$
  19.109  is the overall goal that we are trying to prove, and the numbered lines
  19.110  contain the subgoals $G\sb{1}$, \dots, $G\sb{n}$ that we need to prove to
  19.111 -establish $G$. At @{text"step 0"} there is only one subgoal, which is
  19.112 +establish $G$.\index{subgoals}
  19.113 +At @{text"step 0"} there is only one subgoal, which is
  19.114  identical with the overall goal.  Normally $G$ is constant and only serves as
  19.115  a reminder. Hence we rarely show it in this tutorial.
  19.116  
  19.117 @@ -187,16 +186,18 @@
  19.118  (@{term[source]Cons}):
  19.119  @{subgoals[display,indent=0,margin=65]}
  19.120  
  19.121 -The induction step is an example of the general format of a subgoal:
  19.122 +The induction step is an example of the general format of a subgoal:\index{subgoals}
  19.123  \begin{isabelle}
  19.124  ~$i$.~{\isasymAnd}$x\sb{1}$~\dots~$x\sb{n}$.~{\it assumptions}~{\isasymLongrightarrow}~{\it conclusion}
  19.125  \end{isabelle}\index{$IsaAnd@\isasymAnd|bold}
  19.126  The prefix of bound variables \isasymAnd$x\sb{1}$~\dots~$x\sb{n}$ can be
  19.127  ignored most of the time, or simply treated as a list of variables local to
  19.128  this subgoal. Their deeper significance is explained in Chapter~\ref{chap:rules}.
  19.129 -The {\it assumptions} are the local assumptions for this subgoal and {\it
  19.130 -  conclusion} is the actual proposition to be proved. Typical proof steps
  19.131 -that add new assumptions are induction or case distinction. In our example
  19.132 +The {\it assumptions}\index{assumptions!of subgoal}
  19.133 +are the local assumptions for this subgoal and {\it
  19.134 +  conclusion}\index{conclusion!of subgoal} is the actual proposition to be proved. 
  19.135 +Typical proof steps
  19.136 +that add new assumptions are induction and case distinction. In our example
  19.137  the only assumption is the induction hypothesis @{term"rev (rev list) =
  19.138    list"}, where @{term"list"} is a variable name chosen by Isabelle. If there
  19.139  are multiple assumptions, they are enclosed in the bracket pair
  19.140 @@ -262,7 +263,7 @@
  19.141  subsubsection{*Second Lemma*}
  19.142  
  19.143  text{*
  19.144 -This time the canonical proof procedure
  19.145 +We again try the canonical proof procedure:
  19.146  *}
  19.147  
  19.148  lemma app_Nil2 [simp]: "xs @ [] = xs";
  19.149 @@ -271,7 +272,7 @@
  19.150  
  19.151  txt{*
  19.152  \noindent
  19.153 -leads to the desired message @{text"No subgoals!"}:
  19.154 +It works, yielding the desired message @{text"No subgoals!"}:
  19.155  @{goals[display,indent=0]}
  19.156  We still need to confirm that the proof is now finished:
  19.157  *}
  19.158 @@ -312,10 +313,11 @@
  19.159  *}
  19.160  (*<*)oops(*>*)
  19.161  
  19.162 -subsubsection{*Third Lemma: @{text"(xs @ ys) @ zs = xs @ (ys @ zs)"}*}
  19.163 +subsubsection{*Third Lemma*}
  19.164  
  19.165  text{*
  19.166 -Abandoning the previous proof, the canonical proof procedure
  19.167 +Abandoning the previous attempt, the canonical proof procedure
  19.168 +succeeds without further ado.
  19.169  *}
  19.170  
  19.171  lemma app_assoc [simp]: "(xs @ ys) @ zs = xs @ (ys @ zs)";
  19.172 @@ -325,8 +327,7 @@
  19.173  
  19.174  text{*
  19.175  \noindent
  19.176 -succeeds without further ado.
  19.177 -Now we can prove the first lemma
  19.178 +Now we can prove the first lemma:
  19.179  *}
  19.180  
  19.181  lemma rev_app [simp]: "rev(xs @ ys) = (rev ys) @ (rev xs)";
  19.182 @@ -335,7 +336,7 @@
  19.183  done
  19.184  
  19.185  text{*\noindent
  19.186 -and then prove our main theorem:
  19.187 +Finally, we prove our main theorem:
  19.188  *}
  19.189  
  19.190  theorem rev_rev [simp]: "rev(rev xs) = xs";
  19.191 @@ -344,8 +345,9 @@
  19.192  done
  19.193  
  19.194  text{*\noindent
  19.195 -The final \isacommand{end} tells Isabelle to close the current theory because
  19.196 -we are finished with its development:
  19.197 +The final \commdx{end} tells Isabelle to close the current theory because
  19.198 +we are finished with its development:%
  19.199 +\index{*rev (constant)|)}\index{append function|)}
  19.200  *}
  19.201  
  19.202  end
    20.1 --- a/doc-src/TutorialI/ToyList/document/ToyList.tex	Wed Jul 25 18:21:01 2001 +0200
    20.2 +++ b/doc-src/TutorialI/ToyList/document/ToyList.tex	Thu Jul 26 16:43:02 2001 +0200
    20.3 @@ -35,10 +35,11 @@
    20.4  The \isa{{\isadigit{6}}{\isadigit{5}}} is the priority of the infix \isa{{\isacharhash}}.
    20.5  
    20.6  \begin{warn}
    20.7 -  Syntax annotations are a powerful but optional feature. You
    20.8 +  Syntax annotations are can be powerful, but they are difficult to master and 
    20.9 +  are never necessary.  You
   20.10    could drop them from theory \isa{ToyList} and go back to the identifiers
   20.11    \isa{Nil} and \isa{Cons}.
   20.12 -  We recommend that novices avoid using
   20.13 +  Novices should avoid using
   20.14    syntax annotations in their own theories.
   20.15  \end{warn}
   20.16  Next, two functions \isa{app} and \cdx{rev} are declared:%
   20.17 @@ -49,7 +50,7 @@
   20.18  \noindent
   20.19  In contrast to many functional programming languages,
   20.20  Isabelle insists on explicit declarations of all functions
   20.21 -(keyword \isacommand{consts}).  Apart from the declaration-before-use
   20.22 +(keyword \commdx{consts}).  Apart from the declaration-before-use
   20.23  restriction, the order of items in a theory file is unconstrained. Function
   20.24  \isa{app} is annotated with concrete syntax too. Instead of the
   20.25  prefix syntax \isa{app\ xs\ ys} the infix
   20.26 @@ -64,7 +65,7 @@
   20.27  {\isachardoublequote}rev\ {\isacharbrackleft}{\isacharbrackright}\ \ \ \ \ \ \ \ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequote}\isanewline
   20.28  {\isachardoublequote}rev\ {\isacharparenleft}x\ {\isacharhash}\ xs{\isacharparenright}\ \ {\isacharequal}\ {\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharat}\ {\isacharparenleft}x\ {\isacharhash}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}{\isachardoublequote}%
   20.29  \begin{isamarkuptext}%
   20.30 -\noindent
   20.31 +\noindent\index{*rev (constant)|(}\index{append function|(}
   20.32  The equations for \isa{app} and \isa{rev} hardly need comments:
   20.33  \isa{app} appends two lists and \isa{rev} reverses a list.  The
   20.34  keyword \commdx{primrec} indicates that the recursion is
   20.35 @@ -80,16 +81,16 @@
   20.36  % However, this is a subtle issue that we cannot discuss here further.
   20.37  
   20.38  \begin{warn}
   20.39 -  As we have indicated, the requirement for total functions is not a gratuitous
   20.40 -  restriction but an essential characteristic of HOL\@. It is only
   20.41 +  As we have indicated, the requirement for total functions is an essential characteristic of HOL\@. It is only
   20.42    because of totality that reasoning in HOL is comparatively easy.  More
   20.43 -  generally, the philosophy in HOL is not to allow arbitrary axioms (such as
   20.44 +  generally, the philosophy in HOL is to refrain from asserting arbitrary axioms (such as
   20.45    function definitions whose totality has not been proved) because they
   20.46    quickly lead to inconsistencies. Instead, fixed constructs for introducing
   20.47    types and functions are offered (such as \isacommand{datatype} and
   20.48    \isacommand{primrec}) which are guaranteed to preserve consistency.
   20.49  \end{warn}
   20.50  
   20.51 +\index{syntax}%
   20.52  A remark about syntax.  The textual definition of a theory follows a fixed
   20.53  syntax with keywords like \isacommand{datatype} and \isacommand{end}.
   20.54  % (see Fig.~\ref{fig:keywords} in Appendix~\ref{sec:Appendix} for a full list).
   20.55 @@ -105,7 +106,7 @@
   20.56  \begin{isamarkuptext}%
   20.57  \noindent
   20.58  When Isabelle prints a syntax error message, it refers to the HOL syntax as
   20.59 -the \bfindex{inner syntax} and the enclosing theory language as the \bfindex{outer syntax}.
   20.60 +the \textbf{inner syntax} and the enclosing theory language as the \textbf{outer syntax}.
   20.61  
   20.62  
   20.63  \section{An Introductory Proof}
   20.64 @@ -116,26 +117,23 @@
   20.65  illustrate not just the basic proof commands but also the typical proof
   20.66  process.
   20.67  
   20.68 -\subsubsection*{Main Goal: \isa{rev{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs}.}
   20.69 +\subsubsection*{Main Goal}
   20.70  
   20.71  Our goal is to show that reversing a list twice produces the original
   20.72 -list. The input line%
   20.73 +list.%
   20.74  \end{isamarkuptext}%
   20.75  \isacommand{theorem}\ rev{\isacharunderscore}rev\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}rev{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs{\isachardoublequote}%
   20.76  \begin{isamarkuptxt}%
   20.77  \index{theorem@\isacommand {theorem} (command)|bold}%
   20.78 -\index{*simp (attribute)|bold}
   20.79  \noindent
   20.80 -does several things.  It
   20.81 +This \isacommand{theorem} command does several things:
   20.82  \begin{itemize}
   20.83  \item
   20.84 -establishes a new theorem to be proved, namely \isa{rev\ {\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs},
   20.85 +It establishes a new theorem to be proved, namely \isa{rev\ {\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs}.
   20.86  \item
   20.87 -gives that theorem the name \isa{rev{\isacharunderscore}rev} by which it can be
   20.88 -referred to,
   20.89 +It gives that theorem the name \isa{rev{\isacharunderscore}rev}, for later reference.
   20.90  \item
   20.91 -and tells Isabelle (via \isa{{\isacharbrackleft}simp{\isacharbrackright}}) to use the theorem (once it has been
   20.92 -proved) as a simplification rule, i.e.\ all future proofs involving
   20.93 +It tells Isabelle (via the bracketed attribute \attrdx{simp}) to take the eventual theorem as a simplification rule: future proofs involving
   20.94  simplification will replace occurrences of \isa{rev\ {\isacharparenleft}rev\ xs{\isacharparenright}} by
   20.95  \isa{xs}.
   20.96  
   20.97 @@ -152,7 +150,7 @@
   20.98  The first three lines tell us that we are 0 steps into the proof of
   20.99  theorem \isa{rev{\isacharunderscore}rev}; for compactness reasons we rarely show these
  20.100  initial lines in this tutorial. The remaining lines display the current
  20.101 -proof state.
  20.102 +\rmindex{proof state}.
  20.103  Until we have finished a proof, the proof state always looks like this:
  20.104  \begin{isabelle}
  20.105  $G$\isanewline
  20.106 @@ -163,7 +161,8 @@
  20.107  where $G$
  20.108  is the overall goal that we are trying to prove, and the numbered lines
  20.109  contain the subgoals $G\sb{1}$, \dots, $G\sb{n}$ that we need to prove to
  20.110 -establish $G$. At \isa{step\ {\isadigit{0}}} there is only one subgoal, which is
  20.111 +establish $G$.\index{subgoals}
  20.112 +At \isa{step\ {\isadigit{0}}} there is only one subgoal, which is
  20.113  identical with the overall goal.  Normally $G$ is constant and only serves as
  20.114  a reminder. Hence we rarely show it in this tutorial.
  20.115  
  20.116 @@ -186,16 +185,18 @@
  20.117  \isaindent{\ {\isadigit{2}}{\isachardot}\ \ \ \ }rev\ {\isacharparenleft}rev\ list{\isacharparenright}\ {\isacharequal}\ list\ {\isasymLongrightarrow}\ rev\ {\isacharparenleft}rev\ {\isacharparenleft}a\ {\isacharhash}\ list{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ a\ {\isacharhash}\ list%
  20.118  \end{isabelle}
  20.119  
  20.120 -The induction step is an example of the general format of a subgoal:
  20.121 +The induction step is an example of the general format of a subgoal:\index{subgoals}
  20.122  \begin{isabelle}
  20.123  ~$i$.~{\isasymAnd}$x\sb{1}$~\dots~$x\sb{n}$.~{\it assumptions}~{\isasymLongrightarrow}~{\it conclusion}
  20.124  \end{isabelle}\index{$IsaAnd@\isasymAnd|bold}
  20.125  The prefix of bound variables \isasymAnd$x\sb{1}$~\dots~$x\sb{n}$ can be
  20.126  ignored most of the time, or simply treated as a list of variables local to
  20.127  this subgoal. Their deeper significance is explained in Chapter~\ref{chap:rules}.
  20.128 -The {\it assumptions} are the local assumptions for this subgoal and {\it
  20.129 -  conclusion} is the actual proposition to be proved. Typical proof steps
  20.130 -that add new assumptions are induction or case distinction. In our example
  20.131 +The {\it assumptions}\index{assumptions!of subgoal}
  20.132 +are the local assumptions for this subgoal and {\it
  20.133 +  conclusion}\index{conclusion!of subgoal} is the actual proposition to be proved. 
  20.134 +Typical proof steps
  20.135 +that add new assumptions are induction and case distinction. In our example
  20.136  the only assumption is the induction hypothesis \isa{rev\ {\isacharparenleft}rev\ list{\isacharparenright}\ {\isacharequal}\ list}, where \isa{list} is a variable name chosen by Isabelle. If there
  20.137  are multiple assumptions, they are enclosed in the bracket pair
  20.138  \indexboldpos{\isasymlbrakk}{$Isabrl} and
  20.139 @@ -256,14 +257,14 @@
  20.140  }
  20.141  %
  20.142  \begin{isamarkuptext}%
  20.143 -This time the canonical proof procedure%
  20.144 +We again try the canonical proof procedure:%
  20.145  \end{isamarkuptext}%
  20.146  \isacommand{lemma}\ app{\isacharunderscore}Nil{\isadigit{2}}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}xs\ {\isacharat}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ xs{\isachardoublequote}\isanewline
  20.147  \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}\isanewline
  20.148  \isacommand{apply}{\isacharparenleft}auto{\isacharparenright}%
  20.149  \begin{isamarkuptxt}%
  20.150  \noindent
  20.151 -leads to the desired message \isa{No\ subgoals{\isacharbang}}:
  20.152 +It works, yielding the desired message \isa{No\ subgoals{\isacharbang}}:
  20.153  \begin{isabelle}%
  20.154  xs\ {\isacharat}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ xs\isanewline
  20.155  No\ subgoals{\isacharbang}%
  20.156 @@ -307,11 +308,12 @@
  20.157  and the missing lemma is associativity of \isa{{\isacharat}}.%
  20.158  \end{isamarkuptxt}%
  20.159  %
  20.160 -\isamarkupsubsubsection{Third Lemma: \isa{{\isacharparenleft}xs\ {\isacharat}\ ys{\isacharparenright}\ {\isacharat}\ zs\ {\isacharequal}\ xs\ {\isacharat}\ {\isacharparenleft}ys\ {\isacharat}\ zs{\isacharparenright}}%
  20.161 +\isamarkupsubsubsection{Third Lemma%
  20.162  }
  20.163  %
  20.164  \begin{isamarkuptext}%
  20.165 -Abandoning the previous proof, the canonical proof procedure%
  20.166 +Abandoning the previous attempt, the canonical proof procedure
  20.167 +succeeds without further ado.%
  20.168  \end{isamarkuptext}%
  20.169  \isacommand{lemma}\ app{\isacharunderscore}assoc\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}xs\ {\isacharat}\ ys{\isacharparenright}\ {\isacharat}\ zs\ {\isacharequal}\ xs\ {\isacharat}\ {\isacharparenleft}ys\ {\isacharat}\ zs{\isacharparenright}{\isachardoublequote}\isanewline
  20.170  \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}\isanewline
  20.171 @@ -319,8 +321,7 @@
  20.172  \isacommand{done}%
  20.173  \begin{isamarkuptext}%
  20.174  \noindent
  20.175 -succeeds without further ado.
  20.176 -Now we can prove the first lemma%
  20.177 +Now we can prove the first lemma:%
  20.178  \end{isamarkuptext}%
  20.179  \isacommand{lemma}\ rev{\isacharunderscore}app\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}rev{\isacharparenleft}xs\ {\isacharat}\ ys{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}rev\ ys{\isacharparenright}\ {\isacharat}\ {\isacharparenleft}rev\ xs{\isacharparenright}{\isachardoublequote}\isanewline
  20.180  \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}\isanewline
  20.181 @@ -328,7 +329,7 @@
  20.182  \isacommand{done}%
  20.183  \begin{isamarkuptext}%
  20.184  \noindent
  20.185 -and then prove our main theorem:%
  20.186 +Finally, we prove our main theorem:%
  20.187  \end{isamarkuptext}%
  20.188  \isacommand{theorem}\ rev{\isacharunderscore}rev\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}rev{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs{\isachardoublequote}\isanewline
  20.189  \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}\isanewline
  20.190 @@ -336,8 +337,9 @@
  20.191  \isacommand{done}%
  20.192  \begin{isamarkuptext}%
  20.193  \noindent
  20.194 -The final \isacommand{end} tells Isabelle to close the current theory because
  20.195 +The final \commdx{end} tells Isabelle to close the current theory because
  20.196  we are finished with its development:%
  20.197 +\index{*rev (constant)|)}\index{append function|)}%
  20.198  \end{isamarkuptext}%
  20.199  \isacommand{end}\isanewline
  20.200  \end{isabellebody}%
    21.1 --- a/doc-src/TutorialI/basics.tex	Wed Jul 25 18:21:01 2001 +0200
    21.2 +++ b/doc-src/TutorialI/basics.tex	Thu Jul 26 16:43:02 2001 +0200
    21.3 @@ -8,10 +8,10 @@
    21.4  of Isabelle for HOL, which abbreviates Higher-Order Logic. We introduce
    21.5  HOL step by step following the equation
    21.6  \[ \mbox{HOL} = \mbox{Functional Programming} + \mbox{Logic}. \]
    21.7 -We do not assume that you are familiar with mathematical logic but that
    21.8 -you are used to logical and set theoretic notation, such as covered
    21.9 -in a good discrete mathematics course~\cite{Rosen-DMA}. 
   21.10 -In contrast, we do assume
   21.11 +We do not assume that you are familiar with mathematical logic. 
   21.12 +However, we do assume that
   21.13 +you are used to logical and set theoretic notation, as covered
   21.14 +in a good discrete mathematics course~\cite{Rosen-DMA}, and
   21.15  that you are familiar with the basic concepts of functional
   21.16  programming~\cite{Bird-Haskell,Hudak-Haskell,paulson-ml2,Thompson-Haskell}.
   21.17  Although this tutorial initially concentrates on functional programming, do
    22.1 --- a/doc-src/TutorialI/fp.tex	Wed Jul 25 18:21:01 2001 +0200
    22.2 +++ b/doc-src/TutorialI/fp.tex	Thu Jul 26 16:43:02 2001 +0200
    22.3 @@ -70,7 +70,7 @@
    22.4  There are two kinds of commands used during a proof: the actual proof
    22.5  commands and auxiliary commands for examining the proof state and controlling
    22.6  the display. Simple proof commands are of the form
    22.7 -\commdx{apply}\isa{(method)}, where \isa{method} is typically 
    22.8 +\commdx{apply}\isa{(\textit{method})}, where \textit{method} is typically 
    22.9  \isa{induct_tac} or \isa{auto}.  All such theorem proving operations
   22.10  are referred to as \bfindex{methods}, and further ones are
   22.11  introduced throughout the tutorial.  Unless stated otherwise, you may
   22.12 @@ -98,8 +98,9 @@
   22.13    \commdx{thm}~\textit{name}$@1$~\dots~\textit{name}$@n$
   22.14    prints the named theorems.
   22.15  \item[Displaying types:] We have already mentioned the flag
   22.16 -  \ttindex{show_types} above. It can also be useful for detecting typos in
   22.17 -  formulae early on. For example, if \texttt{show_types} is set and the goal
   22.18 +  \texttt{show_types} above.\index{*show_types (flag)}
   22.19 +  It can also be useful for detecting misspellings in
   22.20 +  formulae. For example, if \texttt{show_types} is set and the goal
   22.21    \isa{rev(rev xs) = xs} is started, Isabelle prints the additional output
   22.22  \par\noindent
   22.23  \begin{isabelle}%
   22.24 @@ -124,7 +125,7 @@
   22.25    \commdx{typ} \textit{string} reads and prints the given
   22.26    string as a type in the current context.
   22.27  \item[(Re)loading theories:] When you start your interaction you must open a
   22.28 -  named theory with the line \isa{\isacommand{theory}~T~=~\dots~:}. Isabelle
   22.29 +  named theory with the line \commdx{theory}~\isa{T~=~\dots~:}. Isabelle
   22.30    automatically loads all the required parent theories from their respective
   22.31    files (which may take a moment, unless the theories are already loaded and
   22.32    the files have not been modified).
   22.33 @@ -152,6 +153,7 @@
   22.34  \section{Datatypes}
   22.35  \label{sec:datatype}
   22.36  
   22.37 +\index{datatypes|(}%
   22.38  Inductive datatypes are part of almost every non-trivial application of HOL.
   22.39  First we take another look at a very important example, the datatype of
   22.40  lists, before we turn to datatypes in general. The section closes with a
   22.41 @@ -161,8 +163,7 @@
   22.42  \subsection{Lists}
   22.43  
   22.44  \index{*list (type)}%
   22.45 -Lists are one of the essential datatypes in computing. Readers of this
   22.46 -tutorial and users of HOL need to be familiar with their basic operations.
   22.47 +Lists are one of the essential datatypes in computing.  You need to be familiar with their basic operations.
   22.48  Theory \isa{ToyList} is only a small fragment of HOL's predefined theory
   22.49  \thydx{List}\footnote{\url{http://isabelle.in.tum.de/library/HOL/List.html}}.
   22.50  The latter contains many further operations. For example, the functions
   22.51 @@ -199,9 +200,14 @@
   22.52  Every datatype $t$ comes equipped with a \isa{size} function from $t$ into
   22.53  the natural numbers (see~{\S}\ref{sec:nat} below). For lists, \isa{size} is
   22.54  just the length, i.e.\ \isa{size [] = 0} and \isa{size(x \# xs) = size xs +
   22.55 -  1}.  In general, \cdx{size} returns \isa{0} for all constructors
   22.56 -that do not have an argument of type $t$, and for all other constructors
   22.57 -\isa{1 +} the sum of the sizes of all arguments of type $t$. Note that because
   22.58 +  1}.  In general, \cdx{size} returns 
   22.59 +\begin{itemize}
   22.60 +\item \isa{0} for all constructors
   22.61 +that do not have an argument of type $t$\\
   22.62 +\item for all other constructors,
   22.63 +one plus the sum of the sizes of all arguments of type~$t$.
   22.64 +\end{itemize}
   22.65 +Note that because
   22.66  \isa{size} is defined on every datatype, it is overloaded; on lists
   22.67  \isa{size} is also called \sdx{length}, which is not overloaded.
   22.68  Isabelle will always show \isa{size} on lists as \isa{length}.
   22.69 @@ -209,6 +215,7 @@
   22.70  
   22.71  \subsection{Primitive Recursion}
   22.72  
   22.73 +\index{recursion!primitive}%
   22.74  Functions on datatypes are usually defined by recursion. In fact, most of the
   22.75  time they are defined by what is called \textbf{primitive recursion}.
   22.76  The keyword \commdx{primrec} is followed by a list of
   22.77 @@ -229,12 +236,14 @@
   22.78  \input{Misc/document/case_exprs.tex}
   22.79  
   22.80  \input{Ifexpr/document/Ifexpr.tex}
   22.81 +\index{datatypes|)}
   22.82 +
   22.83  
   22.84  \section{Some Basic Types}
   22.85  
   22.86  
   22.87  \subsection{Natural Numbers}
   22.88 -\label{sec:nat}
   22.89 +\label{sec:nat}\index{natural numbers}%
   22.90  \index{linear arithmetic|(}
   22.91  
   22.92  \input{Misc/document/fakenat.tex}
   22.93 @@ -256,23 +265,23 @@
   22.94  A definition is simply an abbreviation, i.e.\ a new name for an existing
   22.95  construction. In particular, definitions cannot be recursive. Isabelle offers
   22.96  definitions on the level of types and terms. Those on the type level are
   22.97 -called type synonyms, those on the term level are called (constant)
   22.98 +called \textbf{type synonyms}; those on the term level are simply called 
   22.99  definitions.
  22.100  
  22.101  
  22.102  \subsection{Type Synonyms}
  22.103  
  22.104 -\indexbold{type synonyms|(}%
  22.105 -Type synonyms are similar to those found in ML\@. They are issued by a 
  22.106 +\index{type synonyms|(}%
  22.107 +Type synonyms are similar to those found in ML\@. They are created by a 
  22.108  \commdx{types} command:
  22.109  
  22.110  \input{Misc/document/types.tex}%
  22.111  
  22.112 -Note that pattern-matching is not allowed, i.e.\ each definition must be of
  22.113 +Pattern-matching is not allowed, i.e.\ each definition must be of
  22.114  the form $f\,x@1\,\dots\,x@n~\isasymequiv~t$.
  22.115  Section~{\S}\ref{sec:Simp-with-Defs} explains how definitions are used
  22.116  in proofs.%
  22.117 -\indexbold{type synonyms|)}
  22.118 +\index{type synonyms|)}
  22.119  
  22.120  \input{Misc/document/prime_def.tex}
  22.121  
  22.122 @@ -283,23 +292,16 @@
  22.123  \label{sec:definitional}
  22.124  
  22.125  As we pointed out at the beginning of the chapter, asserting arbitrary
  22.126 -axioms, e.g. $f(n) = f(n) + 1$, may easily lead to contradictions. In order
  22.127 +axioms such as $f(n) = f(n) + 1$ can easily lead to contradictions. In order
  22.128  to avoid this danger, this tutorial advocates the definitional rather than
  22.129 -the axiomatic approach: introduce new concepts by definitions, thus
  22.130 -preserving consistency. However, on the face of it, Isabelle/HOL seems to
  22.131 -support many more constructs than just definitions, for example
  22.132 -\isacommand{primrec}. The crucial point is that internally, everything
  22.133 -(except real axioms) is reduced to a definition. For example, given some
  22.134 -\isacommand{primrec} function definition, this is turned into a proper
  22.135 -(nonrecursive!) definition, and the user-supplied recursion equations are
  22.136 -derived as theorems from that definition. This tricky process is completely
  22.137 -hidden from the user and it is not necessary to understand the details. The
  22.138 -result of the definitional approach is that \isacommand{primrec} is as safe
  22.139 -as pure \isacommand{defs} are, but more convenient. And this is not just the
  22.140 -case for \isacommand{primrec} but also for the other commands described
  22.141 -later, like \isacommand{recdef} and \isacommand{inductive}.
  22.142 -This strict adherence to the definitional approach reduces the risk of 
  22.143 -soundness errors inside Isabelle/HOL.
  22.144 +the axiomatic approach: introduce new concepts by definitions. However,  Isabelle/HOL seems to
  22.145 +support many richer definitional constructs, such as
  22.146 +\isacommand{primrec}. The point is that Isabelle reduces such constructs to first principles. For example, each
  22.147 +\isacommand{primrec} function definition is turned into a proper
  22.148 +(nonrecursive!) definition from which the user-supplied recursion equations are
  22.149 +derived as theorems.  This process is
  22.150 +hidden from the user, who does not have to understand the details.  Other commands described
  22.151 +later, like \isacommand{recdef} and \isacommand{inductive}, are treated similarly.  This strict adherence to the definitional approach reduces the risk of soundness errors.
  22.152  
  22.153  \chapter{More Functional Programming}
  22.154  
    23.1 --- a/doc-src/TutorialI/tutorial.sty	Wed Jul 25 18:21:01 2001 +0200
    23.2 +++ b/doc-src/TutorialI/tutorial.sty	Thu Jul 26 16:43:02 2001 +0200
    23.3 @@ -50,8 +50,12 @@
    23.4  \newcommand\ttindex[1]{\texttt{#1}\index{#1@\texttt{#1}}\@}
    23.5  \newcommand\ttindexbold[1]{\texttt{#1}\index{#1@\texttt{#1}|bold}\@}
    23.6  
    23.7 -\newcommand{\indexboldpos}[2]{#1\index{#2@#1|bold}\@}
    23.8 -\newcommand{\ttindexboldpos}[2]{\texttt{#1}\index{#2@\texttt{#1}|bold}\@}
    23.9 +%Commented-out the original versions to see what the index looks like without them.
   23.10 +%   In any event, they need to use \isa or \protect\isa rather than \texttt.
   23.11 +%%\newcommand{\indexboldpos}[2]{#1\index{#2@#1|bold}\@}
   23.12 +%%\newcommand{\ttindexboldpos}[2]{\texttt{#1}\index{#2@\texttt{#1}|bold}\@}
   23.13 +\newcommand{\indexboldpos}[2]{#1\@}
   23.14 +\newcommand{\ttindexboldpos}[2]{\isa{#1}\@}
   23.15  
   23.16  %\newtheorem{theorem}{Theorem}[section]
   23.17  \newtheorem{Exercise}{Exercise}[section]
    24.1 --- a/doc-src/TutorialI/tutorial.tex	Wed Jul 25 18:21:01 2001 +0200
    24.2 +++ b/doc-src/TutorialI/tutorial.tex	Thu Jul 26 16:43:02 2001 +0200
    24.3 @@ -11,8 +11,9 @@
    24.4  \makeindex
    24.5  
    24.6  \index{conditional expressions|see{\isa{if} expressions}}
    24.7 -\index{primitive recursion|see{\isacommand{primrec}}}
    24.8 +\index{primitive recursion|see{recursion, primitive}}
    24.9  \index{product type|see{pairs and tuples}}
   24.10 +\index{structural induction|see{induction, structural}}
   24.11  \index{termination|see{functions, total}}
   24.12  \index{tuples|see{pairs and tuples}}
   24.13  \index{settings|see{flags}}