1.1 --- a/doc-src/TutorialI/Inductive/AB.thy Thu Jun 16 11:38:52 2005 +0200
1.2 +++ b/doc-src/TutorialI/Inductive/AB.thy Thu Jun 16 18:25:54 2005 +0200
1.3 @@ -101,7 +101,7 @@
1.4 right increases or decreases the difference by 1, we must have passed through
1.5 1 on our way from 0 to 2. Formally, we appeal to the following discrete
1.6 intermediate value theorem @{thm[source]nat0_intermed_int_val}
1.7 -@{thm[display]nat0_intermed_int_val[no_vars]}
1.8 +@{thm[display,margin=60]nat0_intermed_int_val[no_vars]}
1.9 where @{term f} is of type @{typ"nat \<Rightarrow> int"}, @{typ int} are the integers,
1.10 @{text"\<bar>.\<bar>"} is the absolute value function\footnote{See
1.11 Table~\ref{tab:ascii} in the Appendix for the correct \textsc{ascii}
2.1 --- a/doc-src/TutorialI/Inductive/document/AB.tex Thu Jun 16 11:38:52 2005 +0200
2.2 +++ b/doc-src/TutorialI/Inductive/document/AB.tex Thu Jun 16 18:25:54 2005 +0200
2.3 @@ -110,7 +110,8 @@
2.4 1 on our way from 0 to 2. Formally, we appeal to the following discrete
2.5 intermediate value theorem \isa{nat{\isadigit{0}}{\isacharunderscore}intermed{\isacharunderscore}int{\isacharunderscore}val}
2.6 \begin{isabelle}%
2.7 -\ \ \ \ \ {\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%
2.8 +\ \ \ \ \ {\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
2.9 +\isaindent{\ \ \ \ \ }{\isasymLongrightarrow}\ {\isasymexists}i{\isasymle}n{\isachardot}\ f\ i\ {\isacharequal}\ k%
2.10 \end{isabelle}
2.11 where \isa{f} is of type \isa{nat\ {\isasymRightarrow}\ int}, \isa{int} are the integers,
2.12 \isa{{\isasymbar}{\isachardot}{\isasymbar}} is the absolute value function\footnote{See
3.1 --- a/doc-src/TutorialI/Rules/rules.tex Thu Jun 16 11:38:52 2005 +0200
3.2 +++ b/doc-src/TutorialI/Rules/rules.tex Thu Jun 16 18:25:54 2005 +0200
3.3 @@ -640,6 +640,7 @@
3.4 which makes Isabelle show the cause of unification failures (in Proof
3.5 General's \textsf{Trace} buffer).
3.6 \end{pgnote}
3.7 +\noindent
3.8 For example, suppose we are trying to prove this subgoal by assumption:
3.9 \begin{isabelle}
3.10 \ 1.\ P\ (a,\ f\ (b,\ g\ (e,\ a),\ b),\ a)\ \isasymLongrightarrow \ P\ (a,\ f\ (b,\ g\ (c,\ a),\ b),\ a)
3.11 @@ -648,10 +649,9 @@
3.12 \begin{isabelle}
3.13 \isacommand{apply} assumption
3.14 \end{isabelle}
3.15 -Even in this trivial case, the output is unexpectedly verbose, but it yields the necessary information that \isa{e} clashes with \isa{c}:
3.16 +In this trivial case, the output clearly shows that \isa{e} clashes with \isa{c}:
3.17 \begin{isabelle}
3.18 -Clash: e =/= c\isanewline
3.19 -Clash: == =/= Trueprop
3.20 +Clash: e =/= c
3.21 \end{isabelle}
3.22
3.23 Isabelle uses
4.1 --- a/doc-src/TutorialI/Types/numerics.tex Thu Jun 16 11:38:52 2005 +0200
4.2 +++ b/doc-src/TutorialI/Types/numerics.tex Thu Jun 16 18:25:54 2005 +0200
4.3 @@ -398,10 +398,13 @@
4.4 \rulename{mult_cancel_right}
4.5 \end{isabelle}
4.6 Theorems \isa{field_mult_eq_0_iff} and \isa{field_mult_cancel_right}
4.7 -express the same properties, only for fields. When working with such
4.8 -theorems, setting the \texttt{show_sorts}\index{*show_sorts (flag)}
4.9 -flag will display the type classes of all type variables. Here is how the
4.10 -theorem \isa{field_mult_cancel_right} appears with the flag set.
4.11 +express the same properties, only for fields.
4.12 +\begin{pgnote}
4.13 +Setting the flag \textsf{Isabelle} $>$ \textsf{Settings} $>$
4.14 +\textsf{Show Sorts} will display the type classes of all type variables.
4.15 +\end{pgnote}
4.16 +\noindent
4.17 +Here is how the theorem \isa{field_mult_cancel_right} appears with the flag set.
4.18 \begin{isabelle}
4.19 ((a::'a::field)\ *\ (c::'a::field)\ =\ (b::'a::field)\ *\ c)\ =\isanewline
4.20 (c\ =\ (0::'a::field)\ \isasymor \ a\ =\ b)
5.1 --- a/doc-src/TutorialI/fp.tex Thu Jun 16 11:38:52 2005 +0200
5.2 +++ b/doc-src/TutorialI/fp.tex Thu Jun 16 18:25:54 2005 +0200
5.3 @@ -90,73 +90,26 @@
5.4
5.5 The most useful auxiliary commands are as follows:
5.6 \begin{description}
5.7 -\item[Undoing:] \commdx{undo} undoes the effect of
5.8 -the
5.9 - last command; \isacommand{undo} can be undone by
5.10 - \commdx{redo}. Both are only needed at the shell
5.11 - level and should not occur in the final theory.
5.12 -\item[Printing the current state:] \commdx{pr}
5.13 -redisplays
5.14 - the current proof state, for example when it has scrolled past the top of
5.15 - the screen.
5.16 -\item[Limiting the number of subgoals:] \isacommand{pr}~$n$ tells Isabelle to
5.17 - print only the first $n$ subgoals from now on and redisplays the current
5.18 - proof state. This is helpful when there are many subgoals.
5.19 \item[Modifying the order of subgoals:]
5.20 \commdx{defer} moves the first subgoal to the end and
5.21 \commdx{prefer}~$n$ moves subgoal $n$ to the front.
5.22 \item[Printing theorems:]
5.23 \commdx{thm}~\textit{name}$@1$~\dots~\textit{name}$@n$
5.24 prints the named theorems.
5.25 -\item[Displaying types:] We have already mentioned the flag
5.26 - \texttt{show_types} above.\index{*show_types (flag)}
5.27 - It can also be useful for detecting misspellings in
5.28 - formulae. For example, if \texttt{show_types} is set and the goal
5.29 - \isa{rev(rev xs) = xs} is started, Isabelle prints the additional output
5.30 -\par\noindent
5.31 -\begin{isabelle}%
5.32 -variables:\isanewline
5.33 -~~xs~::~'a~list
5.34 -\end{isabelle}%
5.35 -\par\noindent
5.36 -which tells us that Isabelle has correctly inferred that
5.37 -\isa{xs} is a variable of list type. On the other hand, had we
5.38 -made a typo as in \isa{rev(re xs) = xs}, the response
5.39 -\par\noindent
5.40 -\begin{isabelle}%
5.41 -variables:\isanewline
5.42 -~~re~::~'a~list~{\isasymRightarrow}~'a~list\isanewline
5.43 -~~xs~::~'a~list%
5.44 -\end{isabelle}%
5.45 -\par\noindent
5.46 -would have alerted us because of the unexpected variable \isa{re}.
5.47 \item[Reading terms and types:] \commdx{term}
5.48 \textit{string} reads, type-checks and prints the given string as a term in
5.49 the current context; the inferred type is output as well.
5.50 \commdx{typ} \textit{string} reads and prints the given
5.51 string as a type in the current context.
5.52 -\item[(Re)loading theories:] When you start your interaction you must open a
5.53 - named theory with \commdx{theory}~\isa{T} \isacommand{imports} \dots
5.54 - \isacommand{begin}. Isabelle automatically loads all the required parent
5.55 - theories from their respective files (which may take a moment, unless the
5.56 - theories are already loaded and the files have not been modified).
5.57 -
5.58 - If you suddenly discover that you need to modify a parent theory of your
5.59 - current theory, you must first abandon your current theory%
5.60 - \indexbold{abandoning a theory}\indexbold{theories!abandoning} (at the
5.61 - shell level type \commdx{kill}). After the parent theory has been modified,
5.62 - you go back to your original theory. When its opening
5.63 - \isacommand{theory}~\isa{T} \dots \isacommand{begin} is processed, the
5.64 - modified parent is reloaded automatically.
5.65 -
5.66 -% The only time when you need to load a theory by hand is when you simply
5.67 -% want to check if it loads successfully without wanting to make use of the
5.68 -% theory itself. This you can do by typing
5.69 -% \isa{\commdx{use\_thy}~"T"}.
5.70 \end{description}
5.71 Further commands are found in the Isabelle/Isar Reference
5.72 Manual~\cite{isabelle-isar-ref}.
5.73
5.74 +\begin{pgnote}
5.75 +Clicking on the \textsf{State} button redisplays the current proof state.
5.76 +This is helpful in case commands like \isacommand{thm} have overwritten it.
5.77 +\end{pgnote}
5.78 +
5.79 We now examine Isabelle's functional programming constructs systematically,
5.80 starting with inductive datatypes.
5.81