--- a/doc-src/TutorialI/Advanced/Partial.thy Thu Nov 29 20:02:23 2001 +0100
+++ b/doc-src/TutorialI/Advanced/Partial.thy Thu Nov 29 21:12:37 2001 +0100
@@ -146,9 +146,9 @@
text{*If the recursive function happens to be tail recursive, its
definition becomes a triviality if based on the predefined \cdx{while}
-combinator. The latter lives in the Library theory
-\thydx{While_Combinator}, which is not part of @{text Main} but needs to
-be included explicitly among the ancestor theories.
+combinator. The latter lives in the Library theory \thydx{While_Combinator}.
+% which is not part of {text Main} but needs to
+% be included explicitly among the ancestor theories.
Constant @{term while} is of type @{text"('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a"}
and satisfies the recursion equation @{thm[display]while_unfold[no_vars]}
--- a/doc-src/TutorialI/Advanced/document/Partial.tex Thu Nov 29 20:02:23 2001 +0100
+++ b/doc-src/TutorialI/Advanced/document/Partial.tex Thu Nov 29 21:12:37 2001 +0100
@@ -178,9 +178,9 @@
\begin{isamarkuptext}%
If the recursive function happens to be tail recursive, its
definition becomes a triviality if based on the predefined \cdx{while}
-combinator. The latter lives in the Library theory
-\thydx{While_Combinator}, which is not part of \isa{Main} but needs to
-be included explicitly among the ancestor theories.
+combinator. The latter lives in the Library theory \thydx{While_Combinator}.
+% which is not part of {text Main} but needs to
+% be included explicitly among the ancestor theories.
Constant \isa{while} is of type \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a}
and satisfies the recursion equation \begin{isabelle}%
--- a/doc-src/TutorialI/CTL/CTL.thy Thu Nov 29 20:02:23 2001 +0100
+++ b/doc-src/TutorialI/CTL/CTL.thy Thu Nov 29 21:12:37 2001 +0100
@@ -459,8 +459,8 @@
Let us close this section with a few words about the executability of our model checkers.
It is clear that if all sets are finite, they can be represented as lists and the usual
set operations are easily implemented. Only @{term lfp} requires a little thought.
-Fortunately, the HOL Library%
-\footnote{See theory \isa{While_Combinator}.}
+Fortunately, the
+Library\footnote{See theory \isa{While_Combinator}.}~\cite{isabelle-HOL-lib}
provides a theorem stating that
in the case of finite sets and a monotone function~@{term F},
the value of \mbox{@{term"lfp F"}} can be computed by iterated application of @{term F} to~@{term"{}"} until
--- a/doc-src/TutorialI/CTL/document/CTL.tex Thu Nov 29 20:02:23 2001 +0100
+++ b/doc-src/TutorialI/CTL/document/CTL.tex Thu Nov 29 21:12:37 2001 +0100
@@ -468,8 +468,8 @@
Let us close this section with a few words about the executability of our model checkers.
It is clear that if all sets are finite, they can be represented as lists and the usual
set operations are easily implemented. Only \isa{lfp} requires a little thought.
-Fortunately, the HOL Library%
-\footnote{See theory \isa{While_Combinator}.}
+Fortunately, the
+Library\footnote{See theory \isa{While_Combinator}.}~\cite{isabelle-HOL-lib}
provides a theorem stating that
in the case of finite sets and a monotone function~\isa{F},
the value of \mbox{\isa{lfp\ F}} can be computed by iterated application of \isa{F} to~\isa{{\isacharbraceleft}{\isacharbraceright}} until
--- a/doc-src/TutorialI/Inductive/AB.thy Thu Nov 29 20:02:23 2001 +0100
+++ b/doc-src/TutorialI/Inductive/AB.thy Thu Nov 29 21:12:37 2001 +0100
@@ -132,7 +132,7 @@
discuss it.
*}
-apply(induct w)
+apply(induct_tac w)
apply(simp)
by(force simp add: zabs_def take_Cons split: nat.split if_splits)
--- a/doc-src/TutorialI/Inductive/document/AB.tex Thu Nov 29 20:02:23 2001 +0100
+++ b/doc-src/TutorialI/Inductive/document/AB.tex Thu Nov 29 21:12:37 2001 +0100
@@ -144,7 +144,7 @@
discuss it.%
\end{isamarkuptxt}%
\isamarkuptrue%
-\isacommand{apply}{\isacharparenleft}induct\ w{\isacharparenright}\isanewline
+\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ w{\isacharparenright}\isanewline
\ \isamarkupfalse%
\isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline
\isamarkupfalse%
--- a/doc-src/TutorialI/Misc/appendix.thy Thu Nov 29 20:02:23 2001 +0100
+++ b/doc-src/TutorialI/Misc/appendix.thy Thu Nov 29 21:12:37 2001 +0100
@@ -8,7 +8,8 @@
\begin{tabular}{lll}
Constant & Type & Syntax \\
\hline
-@{term 0} & @{text "'a::zero"} \\
+@{text 0} & @{text "'a::zero"} \\
+@{text 1} & @{text "'a::one"} \\
@{text"+"} & @{text "('a::plus) \<Rightarrow> 'a \<Rightarrow> 'a"} & (infixl 65) \\
@{text"-"} & @{text "('a::minus) \<Rightarrow> 'a \<Rightarrow> 'a"} & (infixl 65) \\
@{text"-"} & @{text "('a::minus) \<Rightarrow> 'a"} \\
--- a/doc-src/TutorialI/Misc/document/appendix.tex Thu Nov 29 20:02:23 2001 +0100
+++ b/doc-src/TutorialI/Misc/document/appendix.tex Thu Nov 29 21:12:37 2001 +0100
@@ -9,7 +9,8 @@
\begin{tabular}{lll}
Constant & Type & Syntax \\
\hline
-\isa{{\isadigit{0}}{\isasymColon}{\isacharprime}a} & \isa{{\isacharprime}a{\isacharcolon}{\isacharcolon}zero} \\
+\isa{{\isadigit{0}}} & \isa{{\isacharprime}a{\isacharcolon}{\isacharcolon}zero} \\
+\isa{{\isadigit{1}}} & \isa{{\isacharprime}a{\isacharcolon}{\isacharcolon}one} \\
\isa{{\isacharplus}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}plus{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} & (infixl 65) \\
\isa{{\isacharminus}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}minus{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} & (infixl 65) \\
\isa{{\isacharminus}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}minus{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a} \\
--- a/doc-src/TutorialI/Misc/document/natsum.tex Thu Nov 29 20:02:23 2001 +0100
+++ b/doc-src/TutorialI/Misc/document/natsum.tex Thu Nov 29 21:12:37 2001 +0100
@@ -34,7 +34,7 @@
\newcommand{\mystar}{*%
}
\index{arithmetic operations!for \protect\isa{nat}}%
-The usual arithmetic operations \ttindexboldpos{+}{$HOL2arithfun},
+The arithmetic operations \ttindexboldpos{+}{$HOL2arithfun},
\ttindexboldpos{-}{$HOL2arithfun}, \ttindexboldpos{\mystar}{$HOL2arithfun},
\sdx{div}, \sdx{mod}, \cdx{min} and
\cdx{max} are predefined, as are the relations
@@ -47,8 +47,8 @@
\ttindexboldpos{+}{$HOL2arithfun}, \ttindexboldpos{-}{$HOL2arithfun},
\ttindexboldpos{\mystar}{$HOL2arithfun}, \cdx{min},
\cdx{max}, \indexboldpos{\isasymle}{$HOL2arithrel} and
- \ttindexboldpos{<}{$HOL2arithrel} are overloaded, i.e.\ they are available
- not just for natural numbers but at other types as well.
+ \ttindexboldpos{<}{$HOL2arithrel} are overloaded: they are available
+ not just for natural numbers but for other types as well.
For example, given the goal \isa{x\ {\isacharplus}\ {\isadigit{0}}\ {\isacharequal}\ x}, there is nothing to indicate
that you are talking about natural numbers. Hence Isabelle can only infer
that \isa{x} is of some arbitrary type where \isa{{\isadigit{0}}} and \isa{{\isacharplus}} are
@@ -65,7 +65,7 @@
overloaded operations.
\end{warn}
\begin{warn}
- Constant \isa{{\isadigit{1}}{\isacharcolon}{\isacharcolon}nat} is defined to be \isa{Suc\ {\isadigit{0}}}. This definition
+ Constant \isa{{\isadigit{1}}{\isacharcolon}{\isacharcolon}nat} is defined to equal \isa{Suc\ {\isadigit{0}}}. This definition
(see \S\ref{sec:ConstDefinitions}) is unfolded automatically by some
tactics (like \isa{auto}, \isa{simp} and \isa{arith}) but not by
others (especially the single step tactics in Chapter~\ref{chap:rules}).
--- a/doc-src/TutorialI/Misc/document/simp.tex Thu Nov 29 20:02:23 2001 +0100
+++ b/doc-src/TutorialI/Misc/document/simp.tex Thu Nov 29 21:12:37 2001 +0100
@@ -45,6 +45,13 @@
$g(x) = f(x)$ are simplification rules. It is the user's responsibility not
to include simplification rules that can lead to nontermination, either on
their own or in combination with other simplification rules.
+\end{warn}
+\begin{warn}
+ It is inadvisable to toggle the simplification attribute of a
+ theorem from a \emph{parent} theory $A$ in a child theory $B$ for good.
+ The reason is that if some theory $C$ is based both on $B$ and (via a
+ differnt path) on $A$, it is not defined what the simplification attribute
+ of that theorem will be in $C$: it could be either.
\end{warn}%
\end{isamarkuptext}%
\isamarkuptrue%
--- a/doc-src/TutorialI/Misc/simp.thy Thu Nov 29 20:02:23 2001 +0100
+++ b/doc-src/TutorialI/Misc/simp.thy Thu Nov 29 21:12:37 2001 +0100
@@ -42,6 +42,13 @@
to include simplification rules that can lead to nontermination, either on
their own or in combination with other simplification rules.
\end{warn}
+\begin{warn}
+ It is inadvisable to toggle the simplification attribute of a
+ theorem from a parent theory $A$ in a child theory $B$ for good.
+ The reason is that if some theory $C$ is based both on $B$ and (via a
+ differnt path) on $A$, it is not defined what the simplification attribute
+ of that theorem will be in $C$: it could be either.
+\end{warn}
*}
subsection{*The {\tt\slshape simp} Method*}
--- a/doc-src/TutorialI/Recdef/document/termination.tex Thu Nov 29 20:02:23 2001 +0100
+++ b/doc-src/TutorialI/Recdef/document/termination.tex Thu Nov 29 21:12:37 2001 +0100
@@ -24,12 +24,10 @@
\ \ {\isachardoublequote}f{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ x\ {\isasymle}\ y\ then\ x\ else\ f{\isacharparenleft}x{\isacharcomma}y{\isacharplus}{\isadigit{1}}{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
%
\begin{isamarkuptext}%
-\noindent
-Isabelle prints a
-\REMARK{error or warning? change this part? rename g to f?}
-message showing you what it was unable to prove. You will then
-have to prove it as a separate lemma before you attempt the definition
-of your function once more. In our case the required lemma is the obvious one:%
+\noindent This definition fails, and Isabelle prints an error message
+showing you what it was unable to prove. You will then have to prove it as a
+separate lemma before you attempt the definition of your function once
+more. In our case the required lemma is the obvious one:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{lemma}\ termi{\isacharunderscore}lem{\isacharcolon}\ {\isachardoublequote}{\isasymnot}\ x\ {\isasymle}\ y\ {\isasymLongrightarrow}\ x\ {\isacharminus}\ Suc\ y\ {\isacharless}\ x\ {\isacharminus}\ y{\isachardoublequote}\isamarkupfalse%
@@ -48,24 +46,24 @@
\noindent
Because \isacommand{recdef}'s termination prover involves simplification,
we include in our second attempt a hint: the \attrdx{recdef_simp} attribute
-says to use \isa{termi{\isacharunderscore}lem} as
-a simplification rule.%
+says to use \isa{termi{\isacharunderscore}lem} as a simplification rule.%
\end{isamarkuptext}%
\isamarkuptrue%
-\isacommand{consts}\ g\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat{\isasymtimes}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
+\isamarkupfalse%
\isamarkupfalse%
-\isacommand{recdef}\ g\ {\isachardoublequote}measure{\isacharparenleft}{\isasymlambda}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}{\isachardot}\ x{\isacharminus}y{\isacharparenright}{\isachardoublequote}\isanewline
-\ \ {\isachardoublequote}g{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ x\ {\isasymle}\ y\ then\ x\ else\ g{\isacharparenleft}x{\isacharcomma}y{\isacharplus}{\isadigit{1}}{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isanewline
+\isacommand{recdef}\ f\ {\isachardoublequote}measure{\isacharparenleft}{\isasymlambda}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}{\isachardot}\ x{\isacharminus}y{\isacharparenright}{\isachardoublequote}\isanewline
+\ \ {\isachardoublequote}f{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ x\ {\isasymle}\ y\ then\ x\ else\ f{\isacharparenleft}x{\isacharcomma}y{\isacharplus}{\isadigit{1}}{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isanewline
{\isacharparenleft}\isakeyword{hints}\ recdef{\isacharunderscore}simp{\isacharcolon}\ termi{\isacharunderscore}lem{\isacharparenright}\isamarkupfalse%
+\isamarkupfalse%
%
\begin{isamarkuptext}%
\noindent
-This time everything works fine. Now \isa{g{\isachardot}simps} contains precisely
-the stated recursion equation for \isa{g}, which has been stored as a
+This time everything works fine. Now \isa{f{\isachardot}simps} contains precisely
+the stated recursion equation for \isa{{\isacharquery}{\isacharquery}{\isachardot}f}, which has been stored as a
simplification rule. Thus we can automatically prove results such as this one:%
\end{isamarkuptext}%
\isamarkuptrue%
-\isacommand{theorem}\ {\isachardoublequote}g{\isacharparenleft}{\isadigit{1}}{\isacharcomma}{\isadigit{0}}{\isacharparenright}\ {\isacharequal}\ g{\isacharparenleft}{\isadigit{1}}{\isacharcomma}{\isadigit{1}}{\isacharparenright}{\isachardoublequote}\isanewline
+\isacommand{theorem}\ {\isachardoublequote}f{\isacharparenleft}{\isadigit{1}}{\isacharcomma}{\isadigit{0}}{\isacharparenright}\ {\isacharequal}\ f{\isacharparenleft}{\isadigit{1}}{\isacharcomma}{\isadigit{1}}{\isacharparenright}{\isachardoublequote}\isanewline
\isamarkupfalse%
\isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline
\isamarkupfalse%
@@ -78,22 +76,7 @@
If the termination proof requires a new lemma that is of general use, you can
turn it permanently into a simplification rule, in which case the above
\isacommand{hint} is not necessary. But our \isa{termi{\isacharunderscore}lem} is not
-sufficiently general to warrant this distinction.
-
-The attentive reader may wonder why we chose to call our function \isa{g}
-rather than \isa{f} the second time around. The reason is that, despite
-the failed termination proof, the definition of \isa{f} did not
-fail, and thus we could not define it a second time. However, all theorems
-about \isa{f}, for example \isa{f{\isachardot}simps}, carry as a precondition
-the unproved termination condition. Moreover, the theorems
-\isa{f{\isachardot}simps} are not stored as simplification rules.
-However, this mechanism
-allows a delayed proof of termination: instead of proving
-\isa{termi{\isacharunderscore}lem} up front, we could prove
-it later on and then use it to remove the preconditions from the theorems
-about \isa{f}. In most cases this is more cumbersome than proving things
-up front.
-\REMARK{FIXME, with one exception: nested recursion.}%
+sufficiently general to warrant this distinction.%
\end{isamarkuptext}%
\isamarkuptrue%
\isamarkupfalse%
--- a/doc-src/TutorialI/Recdef/termination.thy Thu Nov 29 20:02:23 2001 +0100
+++ b/doc-src/TutorialI/Recdef/termination.thy Thu Nov 29 21:12:37 2001 +0100
@@ -20,13 +20,10 @@
recdef (*<*)(permissive)(*>*)f "measure(\<lambda>(x,y). x-y)"
"f(x,y) = (if x \<le> y then x else f(x,y+1))"
-text{*\noindent
-Isabelle prints a
-\REMARK{error or warning? change this part? rename g to f?}
-message showing you what it was unable to prove. You will then
-have to prove it as a separate lemma before you attempt the definition
-of your function once more. In our case the required lemma is the obvious one:
-*}
+text{*\noindent This definition fails, and Isabelle prints an error message
+showing you what it was unable to prove. You will then have to prove it as a
+separate lemma before you attempt the definition of your function once
+more. In our case the required lemma is the obvious one: *}
lemma termi_lem: "\<not> x \<le> y \<Longrightarrow> x - Suc y < x - y"
@@ -41,22 +38,21 @@
text{*\noindent
Because \isacommand{recdef}'s termination prover involves simplification,
we include in our second attempt a hint: the \attrdx{recdef_simp} attribute
-says to use @{thm[source]termi_lem} as
-a simplification rule.
+says to use @{thm[source]termi_lem} as a simplification rule.
*}
-consts g :: "nat\<times>nat \<Rightarrow> nat"
-recdef g "measure(\<lambda>(x,y). x-y)"
- "g(x,y) = (if x \<le> y then x else g(x,y+1))"
+(*<*)global consts f :: "nat\<times>nat \<Rightarrow> nat" (*>*)
+recdef f "measure(\<lambda>(x,y). x-y)"
+ "f(x,y) = (if x \<le> y then x else f(x,y+1))"
(hints recdef_simp: termi_lem)
-
+(*<*)local(*>*)
text{*\noindent
-This time everything works fine. Now @{thm[source]g.simps} contains precisely
-the stated recursion equation for @{term g}, which has been stored as a
+This time everything works fine. Now @{thm[source]f.simps} contains precisely
+the stated recursion equation for @{term f}, which has been stored as a
simplification rule. Thus we can automatically prove results such as this one:
*}
-theorem "g(1,0) = g(1,1)"
+theorem "f(1,0) = f(1,1)"
apply(simp)
done
@@ -67,23 +63,7 @@
turn it permanently into a simplification rule, in which case the above
\isacommand{hint} is not necessary. But our @{thm[source]termi_lem} is not
sufficiently general to warrant this distinction.
-
-The attentive reader may wonder why we chose to call our function @{term g}
-rather than @{term f} the second time around. The reason is that, despite
-the failed termination proof, the definition of @{term f} did not
-fail, and thus we could not define it a second time. However, all theorems
-about @{term f}, for example @{thm[source]f.simps}, carry as a precondition
-the unproved termination condition. Moreover, the theorems
-@{thm[source]f.simps} are not stored as simplification rules.
-However, this mechanism
-allows a delayed proof of termination: instead of proving
-@{thm[source]termi_lem} up front, we could prove
-it later on and then use it to remove the preconditions from the theorems
-about @{term f}. In most cases this is more cumbersome than proving things
-up front.
-\REMARK{FIXME, with one exception: nested recursion.}
*}
-
(*<*)
end
(*>*)
--- a/doc-src/TutorialI/Sets/sets.tex Thu Nov 29 20:02:23 2001 +0100
+++ b/doc-src/TutorialI/Sets/sets.tex Thu Nov 29 21:12:37 2001 +0100
@@ -965,8 +965,8 @@
the well-founded relation used to prove termination.
The \bfindex{multiset ordering}, useful for hard termination proofs, is
-available in the Library. Baader and Nipkow \cite[{\S}2.5]{Baader-Nipkow}
-discuss it.
+available in the Library~\cite{isabelle-HOL-lib}.
+Baader and Nipkow \cite[{\S}2.5]{Baader-Nipkow} discuss it.
\medskip
Induction\index{induction!well-founded|(}
--- a/doc-src/TutorialI/ToyList/ToyList.thy Thu Nov 29 20:02:23 2001 +0100
+++ b/doc-src/TutorialI/ToyList/ToyList.thy Thu Nov 29 21:12:37 2001 +0100
@@ -142,19 +142,12 @@
@{term"xs"}.
\end{itemize}
The name and the simplification attribute are optional.
-Isabelle's response is to print the initial proof state
-\begin{isabelle}
-proof(prove):~step~0\isanewline
-\isanewline
-goal~(theorem~rev\_rev):\isanewline
-rev~(rev~xs)~=~xs\isanewline
-~1.~rev~(rev~xs)~=~xs
-\end{isabelle}
-The first three lines tell us that we are 0 steps into the proof of
-theorem @{text"rev_rev"}; for compactness reasons we rarely show these
-initial lines in this tutorial. The remaining lines display the current
-\rmindex{proof state}.
-Until we have finished a proof, the proof state always looks like this:
+Isabelle's response is to print the initial proof state consisting
+of some header information (like how many subgoals there are) followed by
+@{goals[display,indent=0]}
+For compactness reasons we omit the header in this tutorial.
+Until we have finished a proof, the \rmindex{proof state} proper
+always looks like this:
\begin{isabelle}
$G$\isanewline
~1.~$G\sb{1}$\isanewline
@@ -165,7 +158,7 @@
is the overall goal that we are trying to prove, and the numbered lines
contain the subgoals $G\sb{1}$, \dots, $G\sb{n}$ that we need to prove to
establish $G$.\index{subgoals}
-At @{text"step 0"} there is only one subgoal, which is
+Initially there is only one subgoal, which is
identical with the overall goal. Normally $G$ is constant and only serves as
a reminder. Hence we rarely show it in this tutorial.
--- a/doc-src/TutorialI/ToyList/document/ToyList.tex Thu Nov 29 20:02:23 2001 +0100
+++ b/doc-src/TutorialI/ToyList/document/ToyList.tex Thu Nov 29 21:12:37 2001 +0100
@@ -150,19 +150,15 @@
\isa{xs}.
\end{itemize}
The name and the simplification attribute are optional.
-Isabelle's response is to print the initial proof state
-\begin{isabelle}
-proof(prove):~step~0\isanewline
-\isanewline
-goal~(theorem~rev\_rev):\isanewline
-rev~(rev~xs)~=~xs\isanewline
-~1.~rev~(rev~xs)~=~xs
+Isabelle's response is to print the initial proof state consisting
+of some header information (like how many subgoals there are) followed by
+\begin{isabelle}%
+rev\ {\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs\isanewline
+\ {\isadigit{1}}{\isachardot}\ rev\ {\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs%
\end{isabelle}
-The first three lines tell us that we are 0 steps into the proof of
-theorem \isa{rev{\isacharunderscore}rev}; for compactness reasons we rarely show these
-initial lines in this tutorial. The remaining lines display the current
-\rmindex{proof state}.
-Until we have finished a proof, the proof state always looks like this:
+For compactness reasons we omit the header in this tutorial.
+Until we have finished a proof, the \rmindex{proof state} proper
+always looks like this:
\begin{isabelle}
$G$\isanewline
~1.~$G\sb{1}$\isanewline
@@ -173,7 +169,7 @@
is the overall goal that we are trying to prove, and the numbered lines
contain the subgoals $G\sb{1}$, \dots, $G\sb{n}$ that we need to prove to
establish $G$.\index{subgoals}
-At \isa{step\ {\isadigit{0}}} there is only one subgoal, which is
+Initially there is only one subgoal, which is
identical with the overall goal. Normally $G$ is constant and only serves as
a reminder. Hence we rarely show it in this tutorial.
--- a/doc-src/TutorialI/Types/Axioms.thy Thu Nov 29 20:02:23 2001 +0100
+++ b/doc-src/TutorialI/Types/Axioms.thy Thu Nov 29 21:12:37 2001 +0100
@@ -242,6 +242,10 @@
belong to that class. Thus you may be able to prove @{prop False}
from your axioms, but Isabelle will remind you that this
theorem has the hidden hypothesis that the class is non-empty.
+
+Even if each individual class is consistent, intersections of (unrelated)
+classes readily become inconsistent in practice. Now we know this need not
+worry us.
*}
(*
--- a/doc-src/TutorialI/Types/Overloading0.thy Thu Nov 29 20:02:23 2001 +0100
+++ b/doc-src/TutorialI/Types/Overloading0.thy Thu Nov 29 21:12:37 2001 +0100
@@ -35,7 +35,7 @@
However, there is nothing to prevent the user from forming terms such as
@{text"inverse []"} and proving theorems such as @{text"inverse []
= inverse []"} when inverse is not defined on lists. Proving theorems about
-undefined constants does not endanger soundness, but it is pointless.
+unspecified constants does not endanger soundness, but it is pointless.
To prevent such terms from even being formed requires the use of type classes.
*}
(*<*)end(*>*)
--- a/doc-src/TutorialI/Types/Typedefs.thy Thu Nov 29 20:02:23 2001 +0100
+++ b/doc-src/TutorialI/Types/Typedefs.thy Thu Nov 29 21:12:37 2001 +0100
@@ -257,7 +257,7 @@
example to demonstrate \isacommand{typedef} because its simplicity makes the
key concepts particularly easy to grasp. If you would like to see a
non-trivial example that cannot be defined more directly, we recommend the
-definition of \emph{finite multisets} in the HOL Library.
+definition of \emph{finite multisets} in the Library~\cite{isabelle-HOL-lib}.
Let us conclude by summarizing the above procedure for defining a new type.
Given some abstract axiomatic description $P$ of a type $ty$ in terms of a
--- a/doc-src/TutorialI/Types/document/Axioms.tex Thu Nov 29 20:02:23 2001 +0100
+++ b/doc-src/TutorialI/Types/document/Axioms.tex Thu Nov 29 21:12:37 2001 +0100
@@ -283,7 +283,11 @@
unless the type variable is instantiated with a type that has been shown to
belong to that class. Thus you may be able to prove \isa{False}
from your axioms, but Isabelle will remind you that this
-theorem has the hidden hypothesis that the class is non-empty.%
+theorem has the hidden hypothesis that the class is non-empty.
+
+Even if each individual class is consistent, intersections of (unrelated)
+classes readily become inconsistent in practice. Now we know this need not
+worry us.%
\end{isamarkuptext}%
\isamarkuptrue%
\isamarkupfalse%
--- a/doc-src/TutorialI/Types/document/Numbers.tex Thu Nov 29 20:02:23 2001 +0100
+++ b/doc-src/TutorialI/Types/document/Numbers.tex Thu Nov 29 21:12:37 2001 +0100
@@ -292,7 +292,7 @@
REALS
\begin{isabelle}%
-{\isasymbar}r{\isasymbar}\ {\isacharcircum}\ n\ {\isacharequal}\ {\isasymbar}r\ {\isacharcircum}\ n{\isasymbar}%
+{\isasymbar}r\ {\isacharcircum}\ n{\isasymbar}\ {\isacharequal}\ {\isasymbar}r{\isasymbar}\ {\isacharcircum}\ n%
\end{isabelle}
\rulename{realpow_abs}
@@ -302,7 +302,7 @@
\rulename{real_dense}
\begin{isabelle}%
-{\isasymbar}r{\isasymbar}\ {\isacharcircum}\ n\ {\isacharequal}\ {\isasymbar}r\ {\isacharcircum}\ n{\isasymbar}%
+{\isasymbar}r\ {\isacharcircum}\ n{\isasymbar}\ {\isacharequal}\ {\isasymbar}r{\isasymbar}\ {\isacharcircum}\ n%
\end{isabelle}
\rulename{realpow_abs}
--- a/doc-src/TutorialI/Types/document/Overloading0.tex Thu Nov 29 20:02:23 2001 +0100
+++ b/doc-src/TutorialI/Types/document/Overloading0.tex Thu Nov 29 21:12:37 2001 +0100
@@ -45,7 +45,7 @@
However, there is nothing to prevent the user from forming terms such as
\isa{inverse\ {\isacharbrackleft}{\isacharbrackright}} and proving theorems such as \isa{inverse\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ inverse\ {\isacharbrackleft}{\isacharbrackright}} when inverse is not defined on lists. Proving theorems about
-undefined constants does not endanger soundness, but it is pointless.
+unspecified constants does not endanger soundness, but it is pointless.
To prevent such terms from even being formed requires the use of type classes.%
\end{isamarkuptext}%
\isamarkuptrue%
--- a/doc-src/TutorialI/Types/document/Typedefs.tex Thu Nov 29 20:02:23 2001 +0100
+++ b/doc-src/TutorialI/Types/document/Typedefs.tex Thu Nov 29 21:12:37 2001 +0100
@@ -293,7 +293,7 @@
example to demonstrate \isacommand{typedef} because its simplicity makes the
key concepts particularly easy to grasp. If you would like to see a
non-trivial example that cannot be defined more directly, we recommend the
-definition of \emph{finite multisets} in the HOL Library.
+definition of \emph{finite multisets} in the Library~\cite{isabelle-HOL-lib}.
Let us conclude by summarizing the above procedure for defining a new type.
Given some abstract axiomatic description $P$ of a type $ty$ in terms of a
--- a/doc-src/TutorialI/basics.tex Thu Nov 29 20:02:23 2001 +0100
+++ b/doc-src/TutorialI/basics.tex Thu Nov 29 21:12:37 2001 +0100
@@ -88,7 +88,10 @@
predefined theories like arithmetic, lists, sets, etc.
Unless you know what you are doing, always include \isa{Main}
as a direct or indirect parent of all your theories.
-\end{warn}%
+\end{warn}
+There is also a growing Library~\cite{isabelle-library}\index{Library}
+of useful theories that are not part of \isa{Main} but can to be included
+among the parents of a theory and will then be included automatically.%
\index{theories|)}
--- a/doc-src/TutorialI/fp.tex Thu Nov 29 20:02:23 2001 +0100
+++ b/doc-src/TutorialI/fp.tex Thu Nov 29 21:12:37 2001 +0100
@@ -61,6 +61,16 @@
\item a basic repertoire of proof commands.
\end{itemize}
+\begin{warn}
+It is tempting to think that all lemmas should have the \isa{simp} attribute
+just because this was the case in the example above. However, in that example
+all lemmas were equations, and the right-hand side was simpler than the
+left-hand side --- an ideal situation for simplification purposes. Unless
+this is clearly the case, novices should refrain from awarding a lemma the
+\isa{simp} attribute, which has a global effect. Instead, lemmas can be
+applied locally where they are needed, which is discussed in the following
+chapter.
+\end{warn}
\section{Some Helpful Commands}
\label{sec:commands-and-hints}
@@ -513,7 +523,6 @@
\input{Recdef/document/examples.tex}
\subsection{Proving Termination}
-
\input{Recdef/document/termination.tex}
\subsection{Simplification and Recursive Functions}
--- a/doc-src/TutorialI/todo.tobias Thu Nov 29 20:02:23 2001 +0100
+++ b/doc-src/TutorialI/todo.tobias Thu Nov 29 21:12:37 2001 +0100
@@ -1,7 +1,5 @@
"You know my methods. Apply them!"
-Explain indentation of apply's
-
Implementation
==============