author | paulson |

Thu Jul 26 16:43:02 2001 +0200 (2001-07-26) | |

changeset 11456 | 7eb63f63e6c6 |

parent 11455 | e07927b980ec |

child 11457 | 279da0358aa9 |

revisions and indexing

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}}