--- a/doc-src/TutorialI/Inductive/AB.thy Thu Jun 16 11:38:52 2005 +0200
+++ b/doc-src/TutorialI/Inductive/AB.thy Thu Jun 16 18:25:54 2005 +0200
@@ -101,7 +101,7 @@
right increases or decreases the difference by 1, we must have passed through
1 on our way from 0 to 2. Formally, we appeal to the following discrete
intermediate value theorem @{thm[source]nat0_intermed_int_val}
-@{thm[display]nat0_intermed_int_val[no_vars]}
+@{thm[display,margin=60]nat0_intermed_int_val[no_vars]}
where @{term f} is of type @{typ"nat \<Rightarrow> int"}, @{typ int} are the integers,
@{text"\<bar>.\<bar>"} is the absolute value function\footnote{See
Table~\ref{tab:ascii} in the Appendix for the correct \textsc{ascii}
--- a/doc-src/TutorialI/Inductive/document/AB.tex Thu Jun 16 11:38:52 2005 +0200
+++ b/doc-src/TutorialI/Inductive/document/AB.tex Thu Jun 16 18:25:54 2005 +0200
@@ -110,7 +110,8 @@
1 on our way from 0 to 2. Formally, we appeal to the following discrete
intermediate value theorem \isa{nat{\isadigit{0}}{\isacharunderscore}intermed{\isacharunderscore}int{\isacharunderscore}val}
\begin{isabelle}%
-\ \ \ \ \ {\isasymlbrakk}{\isasymforall}i{\isacharless}n{\isachardot}\ {\isasymbar}f\ {\isacharparenleft}i\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}\ {\isacharminus}\ f\ i{\isasymbar}\ {\isasymle}\ {\isadigit{1}}{\isacharsemicolon}\ f\ {\isadigit{0}}\ {\isasymle}\ k{\isacharsemicolon}\ k\ {\isasymle}\ f\ n{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isasymexists}i{\isasymle}n{\isachardot}\ f\ i\ {\isacharequal}\ k%
+\ \ \ \ \ {\isasymlbrakk}{\isasymforall}i{\isacharless}n{\isachardot}\ {\isasymbar}f\ {\isacharparenleft}i\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}\ {\isacharminus}\ f\ i{\isasymbar}\ {\isasymle}\ {\isadigit{1}}{\isacharsemicolon}\ f\ {\isadigit{0}}\ {\isasymle}\ k{\isacharsemicolon}\ k\ {\isasymle}\ f\ n{\isasymrbrakk}\isanewline
+\isaindent{\ \ \ \ \ }{\isasymLongrightarrow}\ {\isasymexists}i{\isasymle}n{\isachardot}\ f\ i\ {\isacharequal}\ k%
\end{isabelle}
where \isa{f} is of type \isa{nat\ {\isasymRightarrow}\ int}, \isa{int} are the integers,
\isa{{\isasymbar}{\isachardot}{\isasymbar}} is the absolute value function\footnote{See
--- a/doc-src/TutorialI/Rules/rules.tex Thu Jun 16 11:38:52 2005 +0200
+++ b/doc-src/TutorialI/Rules/rules.tex Thu Jun 16 18:25:54 2005 +0200
@@ -640,6 +640,7 @@
which makes Isabelle show the cause of unification failures (in Proof
General's \textsf{Trace} buffer).
\end{pgnote}
+\noindent
For example, suppose we are trying to prove this subgoal by assumption:
\begin{isabelle}
\ 1.\ P\ (a,\ f\ (b,\ g\ (e,\ a),\ b),\ a)\ \isasymLongrightarrow \ P\ (a,\ f\ (b,\ g\ (c,\ a),\ b),\ a)
@@ -648,10 +649,9 @@
\begin{isabelle}
\isacommand{apply} assumption
\end{isabelle}
-Even in this trivial case, the output is unexpectedly verbose, but it yields the necessary information that \isa{e} clashes with \isa{c}:
+In this trivial case, the output clearly shows that \isa{e} clashes with \isa{c}:
\begin{isabelle}
-Clash: e =/= c\isanewline
-Clash: == =/= Trueprop
+Clash: e =/= c
\end{isabelle}
Isabelle uses
--- a/doc-src/TutorialI/Types/numerics.tex Thu Jun 16 11:38:52 2005 +0200
+++ b/doc-src/TutorialI/Types/numerics.tex Thu Jun 16 18:25:54 2005 +0200
@@ -398,10 +398,13 @@
\rulename{mult_cancel_right}
\end{isabelle}
Theorems \isa{field_mult_eq_0_iff} and \isa{field_mult_cancel_right}
-express the same properties, only for fields. When working with such
-theorems, setting the \texttt{show_sorts}\index{*show_sorts (flag)}
-flag will display the type classes of all type variables. Here is how the
-theorem \isa{field_mult_cancel_right} appears with the flag set.
+express the same properties, only for fields.
+\begin{pgnote}
+Setting the flag \textsf{Isabelle} $>$ \textsf{Settings} $>$
+\textsf{Show Sorts} will display the type classes of all type variables.
+\end{pgnote}
+\noindent
+Here is how the theorem \isa{field_mult_cancel_right} appears with the flag set.
\begin{isabelle}
((a::'a::field)\ *\ (c::'a::field)\ =\ (b::'a::field)\ *\ c)\ =\isanewline
(c\ =\ (0::'a::field)\ \isasymor \ a\ =\ b)
--- a/doc-src/TutorialI/fp.tex Thu Jun 16 11:38:52 2005 +0200
+++ b/doc-src/TutorialI/fp.tex Thu Jun 16 18:25:54 2005 +0200
@@ -90,73 +90,26 @@
The most useful auxiliary commands are as follows:
\begin{description}
-\item[Undoing:] \commdx{undo} undoes the effect of
-the
- last command; \isacommand{undo} can be undone by
- \commdx{redo}. Both are only needed at the shell
- level and should not occur in the final theory.
-\item[Printing the current state:] \commdx{pr}
-redisplays
- the current proof state, for example when it has scrolled past the top of
- the screen.
-\item[Limiting the number of subgoals:] \isacommand{pr}~$n$ tells Isabelle to
- print only the first $n$ subgoals from now on and redisplays the current
- proof state. This is helpful when there are many subgoals.
\item[Modifying the order of subgoals:]
\commdx{defer} moves the first subgoal to the end and
\commdx{prefer}~$n$ moves subgoal $n$ to the front.
\item[Printing theorems:]
\commdx{thm}~\textit{name}$@1$~\dots~\textit{name}$@n$
prints the named theorems.
-\item[Displaying types:] We have already mentioned the flag
- \texttt{show_types} above.\index{*show_types (flag)}
- It can also be useful for detecting misspellings in
- formulae. For example, if \texttt{show_types} is set and the goal
- \isa{rev(rev xs) = xs} is started, Isabelle prints the additional output
-\par\noindent
-\begin{isabelle}%
-variables:\isanewline
-~~xs~::~'a~list
-\end{isabelle}%
-\par\noindent
-which tells us that Isabelle has correctly inferred that
-\isa{xs} is a variable of list type. On the other hand, had we
-made a typo as in \isa{rev(re xs) = xs}, the response
-\par\noindent
-\begin{isabelle}%
-variables:\isanewline
-~~re~::~'a~list~{\isasymRightarrow}~'a~list\isanewline
-~~xs~::~'a~list%
-\end{isabelle}%
-\par\noindent
-would have alerted us because of the unexpected variable \isa{re}.
\item[Reading terms and types:] \commdx{term}
\textit{string} reads, type-checks and prints the given string as a term in
the current context; the inferred type is output as well.
\commdx{typ} \textit{string} reads and prints the given
string as a type in the current context.
-\item[(Re)loading theories:] When you start your interaction you must open a
- named theory with \commdx{theory}~\isa{T} \isacommand{imports} \dots
- \isacommand{begin}. Isabelle automatically loads all the required parent
- theories from their respective files (which may take a moment, unless the
- theories are already loaded and the files have not been modified).
-
- If you suddenly discover that you need to modify a parent theory of your
- current theory, you must first abandon your current theory%
- \indexbold{abandoning a theory}\indexbold{theories!abandoning} (at the
- shell level type \commdx{kill}). After the parent theory has been modified,
- you go back to your original theory. When its opening
- \isacommand{theory}~\isa{T} \dots \isacommand{begin} is processed, the
- modified parent is reloaded automatically.
-
-% The only time when you need to load a theory by hand is when you simply
-% want to check if it loads successfully without wanting to make use of the
-% theory itself. This you can do by typing
-% \isa{\commdx{use\_thy}~"T"}.
\end{description}
Further commands are found in the Isabelle/Isar Reference
Manual~\cite{isabelle-isar-ref}.
+\begin{pgnote}
+Clicking on the \textsf{State} button redisplays the current proof state.
+This is helpful in case commands like \isacommand{thm} have overwritten it.
+\end{pgnote}
+
We now examine Isabelle's functional programming constructs systematically,
starting with inductive datatypes.