*** empty log message ***
authornipkow
Thu Jun 16 18:25:54 2005 +0200 (2005-06-16)
changeset 1641250eab0183aea
parent 16411 04cc6b4b3439
child 16413 47ffc49c7d7b
*** empty log message ***
doc-src/TutorialI/Inductive/AB.thy
doc-src/TutorialI/Inductive/document/AB.tex
doc-src/TutorialI/Rules/rules.tex
doc-src/TutorialI/Types/numerics.tex
doc-src/TutorialI/fp.tex
     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