tuning
authornipkow
Fri Jun 10 18:36:47 2005 +0200 (2005-06-10)
changeset 16359af7239e3054d
parent 16358 2e2a506553a3
child 16360 6897b5958be7
tuning
doc-src/TutorialI/Misc/document/simp.tex
doc-src/TutorialI/Misc/simp.thy
doc-src/TutorialI/Rules/rules.tex
doc-src/TutorialI/Types/numerics.tex
doc-src/TutorialI/basics.tex
doc-src/TutorialI/tutorial.tex
     1.1 --- a/doc-src/TutorialI/Misc/document/simp.tex	Fri Jun 10 17:59:12 2005 +0200
     1.2 +++ b/doc-src/TutorialI/Misc/document/simp.tex	Fri Jun 10 18:36:47 2005 +0200
     1.3 @@ -441,13 +441,9 @@
     1.4  \begin{isamarkuptext}%
     1.5  \indexbold{tracing the simplifier}
     1.6  Using the simplifier effectively may take a bit of experimentation.  Set the
     1.7 -\isa{trace_simp}\index{*trace_simp (flag)} flag\index{flags} 
     1.8 -to get a better idea of what is going
     1.9 -on:%
    1.10 +Proof General flag \textsf{Isabelle} $>$ \textsf{Settings} $>$ \textsf{Trace Simplifier} to get a better idea of what is going on:%
    1.11  \end{isamarkuptext}%
    1.12  \isamarkuptrue%
    1.13 -\isacommand{ML}\ {\isachardoublequote}set\ trace{\isacharunderscore}simp{\isachardoublequote}\isanewline
    1.14 -\isamarkupfalse%
    1.15  \isacommand{lemma}\ {\isachardoublequote}rev\ {\isacharbrackleft}a{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequote}\isanewline
    1.16  \isamarkupfalse%
    1.17  \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isamarkupfalse%
    1.18 @@ -455,40 +451,50 @@
    1.19  %
    1.20  \begin{isamarkuptext}%
    1.21  \noindent
    1.22 -produces the trace
    1.23 +produces the following trace in Proof General's \textsf{Trace} buffer:
    1.24  
    1.25  \begin{ttbox}\makeatother
    1.26 -Applying instance of rewrite rule:
    1.27 -rev (?x1 \# ?xs1) == rev ?xs1 @ [?x1]
    1.28 -Rewriting:
    1.29 -rev [a] == rev [] @ [a]
    1.30 -Applying instance of rewrite rule:
    1.31 -rev [] == []
    1.32 -Rewriting:
    1.33 -rev [] == []
    1.34 -Applying instance of rewrite rule:
    1.35 -[] @ ?y == ?y
    1.36 -Rewriting:
    1.37 -[] @ [a] == [a]
    1.38 -Applying instance of rewrite rule:
    1.39 -?x3 \# ?t3 = ?t3 == False
    1.40 -Rewriting:
    1.41 -[a] = [] == False
    1.42 +[0]Applying instance of rewrite rule "List.rev.simps_2":
    1.43 +rev (?x1 # ?xs1) \(\equiv\) rev ?xs1 @ [?x1]
    1.44 +
    1.45 +[0]Rewriting:
    1.46 +rev [a] \(\equiv\) rev [] @ [a]
    1.47 +
    1.48 +[0]Applying instance of rewrite rule "List.rev.simps_1":
    1.49 +rev [] \(\equiv\) []
    1.50 +
    1.51 +[0]Rewriting:
    1.52 +rev [] \(\equiv\) []
    1.53 +
    1.54 +[0]Applying instance of rewrite rule "List.op @.append_Nil":
    1.55 +[] @ ?y \(\equiv\) ?y
    1.56 +
    1.57 +[0]Rewriting:
    1.58 +[] @ [a] \(\equiv\) [a]
    1.59 +
    1.60 +[0]Applying instance of rewrite rule
    1.61 +?x2 # ?t1 = ?t1 \(\equiv\) False
    1.62 +
    1.63 +[0]Rewriting:
    1.64 +[a] = [] \(\equiv\) False
    1.65  \end{ttbox}
    1.66 +The trace lists each rule being applied, both in its general form and
    1.67 +the instance being used. The \texttt{[}$i$\texttt{]} in front (where
    1.68 +above $i$ is always \texttt{0}) indicates that we are inside the $i$th
    1.69 +recursive invocation of the simplifier. Each attempt to apply a
    1.70 +conditional rule shows the rule followed by the trace of the
    1.71 +(recursive!) simplification of the conditions, the latter prefixed by
    1.72 +\texttt{[}$i+1$\texttt{]} instead of \texttt{[}$i$\texttt{]}.
    1.73 +Another source of recursive invocations of the simplifier are
    1.74 +proofs of arithmetic formulae.
    1.75  
    1.76 -The trace lists each rule being applied, both in its general form and the 
    1.77 -instance being used.  For conditional rules, the trace lists the rule
    1.78 -it is trying to rewrite and gives the result of attempting to prove
    1.79 -each of the rule's conditions.  Many other hints about the simplifier's
    1.80 -actions will appear.
    1.81 +Many other hints about the simplifier's actions may appear.
    1.82  
    1.83 -In more complicated cases, the trace can be quite lengthy.  Invocations of the
    1.84 -simplifier are often nested, for instance when solving conditions of rewrite
    1.85 -rules.  Thus it is advisable to reset it:%
    1.86 +In more complicated cases, the trace can be very lengthy.  Thus it is
    1.87 +advisable to reset the \textsf{Trace Simplifier} flag after having
    1.88 +obtained the desired trace.%
    1.89  \end{isamarkuptext}%
    1.90  \isamarkuptrue%
    1.91 -\isacommand{ML}\ {\isachardoublequote}reset\ trace{\isacharunderscore}simp{\isachardoublequote}\isanewline
    1.92 -\isamarkupfalse%
    1.93  \isamarkupfalse%
    1.94  \end{isabellebody}%
    1.95  %%% Local Variables:
     2.1 --- a/doc-src/TutorialI/Misc/simp.thy	Fri Jun 10 17:59:12 2005 +0200
     2.2 +++ b/doc-src/TutorialI/Misc/simp.thy	Fri Jun 10 18:36:47 2005 +0200
     2.3 @@ -367,50 +367,56 @@
     2.4  subsection{*Tracing*}
     2.5  text{*\indexbold{tracing the simplifier}
     2.6  Using the simplifier effectively may take a bit of experimentation.  Set the
     2.7 -\isa{trace_simp}\index{*trace_simp (flag)} flag\index{flags} 
     2.8 -to get a better idea of what is going
     2.9 -on:
    2.10 +Proof General flag \textsf{Isabelle} $>$ \textsf{Settings} $>$ \textsf{Trace Simplifier} to get a better idea of what is going on:
    2.11  *}
    2.12  
    2.13 -ML "set trace_simp"
    2.14  lemma "rev [a] = []"
    2.15  apply(simp)
    2.16  (*<*)oops(*>*)
    2.17  
    2.18  text{*\noindent
    2.19 -produces the trace
    2.20 +produces the following trace in Proof General's \textsf{Trace} buffer:
    2.21  
    2.22  \begin{ttbox}\makeatother
    2.23 -Applying instance of rewrite rule:
    2.24 -rev (?x1 \# ?xs1) == rev ?xs1 @ [?x1]
    2.25 -Rewriting:
    2.26 -rev [a] == rev [] @ [a]
    2.27 -Applying instance of rewrite rule:
    2.28 -rev [] == []
    2.29 -Rewriting:
    2.30 -rev [] == []
    2.31 -Applying instance of rewrite rule:
    2.32 -[] @ ?y == ?y
    2.33 -Rewriting:
    2.34 -[] @ [a] == [a]
    2.35 -Applying instance of rewrite rule:
    2.36 -?x3 \# ?t3 = ?t3 == False
    2.37 -Rewriting:
    2.38 -[a] = [] == False
    2.39 +[0]Applying instance of rewrite rule "List.rev.simps_2":
    2.40 +rev (?x1 # ?xs1) \(\equiv\) rev ?xs1 @ [?x1]
    2.41 +
    2.42 +[0]Rewriting:
    2.43 +rev [a] \(\equiv\) rev [] @ [a]
    2.44 +
    2.45 +[0]Applying instance of rewrite rule "List.rev.simps_1":
    2.46 +rev [] \(\equiv\) []
    2.47 +
    2.48 +[0]Rewriting:
    2.49 +rev [] \(\equiv\) []
    2.50 +
    2.51 +[0]Applying instance of rewrite rule "List.op @.append_Nil":
    2.52 +[] @ ?y \(\equiv\) ?y
    2.53 +
    2.54 +[0]Rewriting:
    2.55 +[] @ [a] \(\equiv\) [a]
    2.56 +
    2.57 +[0]Applying instance of rewrite rule
    2.58 +?x2 # ?t1 = ?t1 \(\equiv\) False
    2.59 +
    2.60 +[0]Rewriting:
    2.61 +[a] = [] \(\equiv\) False
    2.62  \end{ttbox}
    2.63 -
    2.64 -The trace lists each rule being applied, both in its general form and the 
    2.65 -instance being used.  For conditional rules, the trace lists the rule
    2.66 -it is trying to rewrite and gives the result of attempting to prove
    2.67 -each of the rule's conditions.  Many other hints about the simplifier's
    2.68 -actions will appear.
    2.69 +The trace lists each rule being applied, both in its general form and
    2.70 +the instance being used. The \texttt{[}$i$\texttt{]} in front (where
    2.71 +above $i$ is always \texttt{0}) indicates that we are inside the $i$th
    2.72 +recursive invocation of the simplifier. Each attempt to apply a
    2.73 +conditional rule shows the rule followed by the trace of the
    2.74 +(recursive!) simplification of the conditions, the latter prefixed by
    2.75 +\texttt{[}$i+1$\texttt{]} instead of \texttt{[}$i$\texttt{]}.
    2.76 +Another source of recursive invocations of the simplifier are
    2.77 +proofs of arithmetic formulae.
    2.78  
    2.79 -In more complicated cases, the trace can be quite lengthy.  Invocations of the
    2.80 -simplifier are often nested, for instance when solving conditions of rewrite
    2.81 -rules.  Thus it is advisable to reset it:
    2.82 -*}
    2.83 +Many other hints about the simplifier's actions may appear.
    2.84  
    2.85 -ML "reset trace_simp"
    2.86 +In more complicated cases, the trace can be very lengthy.  Thus it is
    2.87 +advisable to reset the \textsf{Trace Simplifier} flag after having
    2.88 +obtained the desired trace.  *}
    2.89  
    2.90  (*<*)
    2.91  end
     3.1 --- a/doc-src/TutorialI/Rules/rules.tex	Fri Jun 10 17:59:12 2005 +0200
     3.2 +++ b/doc-src/TutorialI/Rules/rules.tex	Fri Jun 10 18:36:47 2005 +0200
     3.3 @@ -634,14 +634,18 @@
     3.4  as $\exists x.\,P$, they let us proceed with a proof.  They can be 
     3.5  filled in later, sometimes in stages and often automatically. 
     3.6  
     3.7 -If unification fails when you think it should succeed, try setting the flag \index{flags}\isa{trace_unify_fail}\index{*trace_unify_fail (flag)},
     3.8 -which makes Isabelle show the cause of unification failures.  For example, suppose we are trying to prove this subgoal by assumption:
     3.9 +\begin{pgnote}
    3.10 +If unification fails when you think it should succeed, try setting the Proof General flag \textsf{Isabelle} $>$ \textsf{Settings} $>$
    3.11 +\textsf{Trace Unification},
    3.12 +which makes Isabelle show the cause of unification failures (in Proof
    3.13 +General's \textsf{Trace} buffer).
    3.14 +\end{pgnote}
    3.15 +For example, suppose we are trying to prove this subgoal by assumption:
    3.16  \begin{isabelle}
    3.17  \ 1.\ P\ (a,\ f\ (b,\ g\ (e,\ a),\ b),\ a)\ \isasymLongrightarrow \ P\ (a,\ f\ (b,\ g\ (c,\ a),\ b),\ a)
    3.18  \end{isabelle}
    3.19  The \isa{assumption} method having failed, we try again with the flag set:
    3.20  \begin{isabelle}
    3.21 -\isacommand{ML}\ "set\ trace\_unify\_fail"\isanewline
    3.22  \isacommand{apply} assumption
    3.23  \end{isabelle}
    3.24  Even in this trivial case, the output is unexpectedly verbose, but it yields the necessary information:
     4.1 --- a/doc-src/TutorialI/Types/numerics.tex	Fri Jun 10 17:59:12 2005 +0200
     4.2 +++ b/doc-src/TutorialI/Types/numerics.tex	Fri Jun 10 18:36:47 2005 +0200
     4.3 @@ -309,6 +309,7 @@
     4.4  
     4.5  
     4.6  \subsection{The Types of Rational, Real and Complex Numbers}
     4.7 +\label{sec:real}
     4.8  
     4.9  \index{rational numbers|(}\index{*rat (type)|(}%
    4.10  \index{real numbers|(}\index{*real (type)|(}%
    4.11 @@ -340,15 +341,12 @@
    4.12  is performed.
    4.13  
    4.14  \begin{warn}
    4.15 -Type \isa{real} is only available in the logic HOL-Complex, which
    4.16 -is  HOL extended with a definitional development of the real and complex
    4.17 -numbers.  Base your theory upon theory
    4.18 -\thydx{Complex_Main}, not the usual \isa{Main}.%
    4.19 +Type \isa{real} is only available in the logic HOL-Complex, which is
    4.20 +HOL extended with a definitional development of the real and complex
    4.21 +numbers.  Base your theory upon theory \thydx{Complex_Main}, not the
    4.22 +usual \isa{Main}, and set the Proof General menu item \textsf{Isabelle} $>$
    4.23 +\textsf{Logics} $>$ \textsf{HOL-Complex}.%
    4.24  \index{real numbers|)}\index{*real (type)|)}
    4.25 -Launch Isabelle using the command 
    4.26 -\begin{verbatim}
    4.27 -Isabelle -l HOL-Complex
    4.28 -\end{verbatim}
    4.29  \end{warn}
    4.30  
    4.31  Also available in HOL-Complex is the
     5.1 --- a/doc-src/TutorialI/basics.tex	Fri Jun 10 17:59:12 2005 +0200
     5.2 +++ b/doc-src/TutorialI/basics.tex	Fri Jun 10 18:36:47 2005 +0200
     5.3 @@ -87,10 +87,10 @@
     5.4  \begin{center}\small
     5.5      \url{http://isabelle.in.tum.de/library/HOL/}
     5.6  \end{center}
     5.7 -and is recommended browsing.
     5.8 -There is also a growing Library~\cite{HOL-Library}\index{Library}
     5.9 -of useful theories that are not part of \isa{Main} but can be included
    5.10 -among the parents of a theory and will then be loaded automatically.
    5.11 +and is recommended browsing. In subdirectory \texttt{Library} you find
    5.12 +a growing library of useful theories that are not part of \isa{Main}
    5.13 +but can be included among the parents of a theory and will then be
    5.14 +loaded automatically.
    5.15  
    5.16  For the more adventurous, there is the \emph{Archive of Formal Proofs},
    5.17  a journal-like collection of more advanced Isabelle theories:
    5.18 @@ -134,15 +134,17 @@
    5.19  \end{description}
    5.20  \begin{warn}
    5.21    Types are extremely important because they prevent us from writing
    5.22 -  nonsense.  Isabelle insists that all terms and formulae must be well-typed
    5.23 -  and will print an error message if a type mismatch is encountered. To
    5.24 -  reduce the amount of explicit type information that needs to be provided by
    5.25 -  the user, Isabelle infers the type of all variables automatically (this is
    5.26 -  called \bfindex{type inference}) and keeps quiet about it. Occasionally
    5.27 -  this may lead to misunderstandings between you and the system. If anything
    5.28 -  strange happens, we recommend that you ask Isabelle to display all type
    5.29 -  information. This is best done through the Proof General interface; see
    5.30 -  \S\ref{sec:interface} for details.
    5.31 +  nonsense.  Isabelle insists that all terms and formulae must be
    5.32 +  well-typed and will print an error message if a type mismatch is
    5.33 +  encountered. To reduce the amount of explicit type information that
    5.34 +  needs to be provided by the user, Isabelle infers the type of all
    5.35 +  variables automatically (this is called \bfindex{type inference})
    5.36 +  and keeps quiet about it. Occasionally this may lead to
    5.37 +  misunderstandings between you and the system. If anything strange
    5.38 +  happens, we recommend that you ask Isabelle to display all type
    5.39 +  information via the Proof General menu item \textsf{Isabelle} $>$
    5.40 +  \textsf{Settings} $>$ \textsf{Show Types} (see \S\ref{sec:interface}
    5.41 +  for details).
    5.42  \end{warn}%
    5.43  \index{types|)}
    5.44  
    5.45 @@ -257,16 +259,13 @@
    5.46  the appendix.
    5.47  
    5.48  \begin{warn}
    5.49 -A particular
    5.50 -problem for novices can be the priority of operators. If you are unsure, use
    5.51 -additional parentheses. In those cases where Isabelle echoes your
    5.52 -input, you can see which parentheses are dropped --- they were superfluous. If
    5.53 -you are unsure how to interpret Isabelle's output because you don't know
    5.54 -where the (dropped) parentheses go, set the flag\index{flags}
    5.55 -\isa{show_brackets}\index{*show_brackets (flag)}:
    5.56 -\begin{ttbox}
    5.57 -ML "set show_brackets"; \(\dots\); ML "reset show_brackets";
    5.58 -\end{ttbox}
    5.59 +A particular problem for novices can be the priority of operators. If
    5.60 +you are unsure, use additional parentheses. In those cases where
    5.61 +Isabelle echoes your input, you can see which parentheses are dropped
    5.62 +--- they were superfluous. If you are unsure how to interpret
    5.63 +Isabelle's output because you don't know where the (dropped)
    5.64 +parentheses go, set the Proof General flag \textsf{Isabelle} $>$
    5.65 +\textsf{Settings} $>$ \textsf{Show Brackets} (see \S\ref{sec:interface}).
    5.66  \end{warn}
    5.67  
    5.68  
    5.69 @@ -304,48 +303,52 @@
    5.70  \section{Interaction and Interfaces}
    5.71  \label{sec:interface}
    5.72  
    5.73 -Interaction with Isabelle can either occur at the shell level or through more
    5.74 -advanced interfaces. To keep the tutorial independent of the interface, we
    5.75 -have phrased the description of the interaction in a neutral language. For
    5.76 -example, the phrase ``to abandon a proof'' means to type \isacommand{oops} at the
    5.77 -shell level, which is explained the first time the phrase is used. Other
    5.78 -interfaces perform the same act by cursor movements and/or mouse clicks.
    5.79 -Although shell-based interaction is quite feasible for the kind of proof
    5.80 -scripts currently presented in this tutorial, the recommended interface for
    5.81 -Isabelle/Isar is the Emacs-based \bfindex{Proof
    5.82 -  General}~\cite{proofgeneral,Aspinall:TACAS:2000}.
    5.83 +The recommended interface for Isabelle/Isar is the (X)Emacs-based
    5.84 +\bfindex{Proof General}~\cite{proofgeneral,Aspinall:TACAS:2000}.
    5.85 +Interaction with Isabelle at the shell level, although possible,
    5.86 +should be avoided. Most of the tutorial is independent of the
    5.87 +interface and is phrased in a neutral language. For example, the
    5.88 +phrase ``to abandon a proof'' corresponds to the obvious
    5.89 +action of clicking on the \textsf{Undo} symbol in Proof General.
    5.90 +Proof General specific information is often displayed in paragraphs
    5.91 +identified by a miniature Proof General icon. Here are two examples:
    5.92 +\begin{pgnote}
    5.93 +Proof General supports a special font with mathematical symbols known
    5.94 +as ``x-symbols''. All symbols have \textsc{ascii}-equivalents: for
    5.95 +example, you can enter either \verb!&!  or \verb!\<and>! to obtain
    5.96 +$\land$. For a list of the most frequent symbols see table~\ref{tab:ascii}
    5.97 +in the appendix.
    5.98  
    5.99 -\begin{pgnote}
   5.100 -Proof General specific information is always displayed in paragraphs
   5.101 -identified by this miniature Proof General icon.
   5.102 -
   5.103 -On particularly nice feature of Proof General is its support for a special
   5.104 -fonts with mathematical symbols. Most symbols have
   5.105 -\textsc{ascii}-equivalents: for example, you can enter either \verb!&!
   5.106 -or \verb!\<and>! to obtain $\land$. For a list of the most frequent symbols
   5.107 -see table~\ref{tab:ascii} in the appendix.
   5.108 +Note that by default x-symbols are not enabled. You have to switch
   5.109 +them on via the menu item \textsf{Proof-General} $>$ \textsf{Options} $>$
   5.110 +\textsf{X-Symbols} (and save the option via the top-level
   5.111 +\textsf{Options} menu).
   5.112  \end{pgnote}
   5.113  
   5.114  \begin{pgnote}
   5.115 -Proof General offers an \texttt{Isabelle} menu for displaying information
   5.116 -and setting flags. A particularly useful flag is \texttt{Show Types}
   5.117 -which causes Isabelle to output the type information that is usually
   5.118 +Proof General offers the \textsf{Isabelle} menu for displaying
   5.119 +information and setting flags. A particularly useful flag is
   5.120 +\textsf{Isabelle} $>$ \textsf{Settings} $>$ \textsf{Show Types} which
   5.121 +causes Isabelle to output the type information that is usually
   5.122  suppressed. This is indispensible in case of errors of all kinds
   5.123 -because often the types reveal the source of the problem. Once you have
   5.124 -diagnosed the problem you may no longer want to see the types because they
   5.125 -clutter all output. Simply reset the flag.
   5.126 +because often the types reveal the source of the problem. Once you
   5.127 +have diagnosed the problem you may no longer want to see the types
   5.128 +because they clutter all output. Simply reset the flag.
   5.129  \end{pgnote}
   5.130  
   5.131  \section{Getting Started}
   5.132  
   5.133 -Assuming you have installed Isabelle, you start it by typing \texttt{isabelle
   5.134 -  -I HOL} in a shell window.\footnote{Simply executing \texttt{isabelle -I}
   5.135 -  starts the default logic, which usually is already \texttt{HOL}.  This is
   5.136 -  controlled by the \texttt{ISABELLE_LOGIC} setting, see \emph{The Isabelle
   5.137 -    System Manual} for more details.} This presents you with Isabelle's most
   5.138 -basic \textsc{ascii} interface.  In addition you need to open an editor window to
   5.139 -create theory files.  While you are developing a theory, we recommend that you
   5.140 -type each command into the file first and then enter it into Isabelle by
   5.141 -copy-and-paste, thus ensuring that you have a complete record of your theory.
   5.142 -As mentioned above, Proof General offers a much superior interface.
   5.143 -If you have installed Proof General, you can start it by typing \texttt{Isabelle}.
   5.144 +Assuming you have installed Isabelle and Proof General, you start it by typing
   5.145 +\texttt{Isabelle} in a shell window. This launches a Proof General window.
   5.146 +By default, you are in HOL\footnote{This is controlled by the
   5.147 +\texttt{ISABELLE_LOGIC} setting, see \emph{The Isabelle System Manual}
   5.148 +for more details.}.
   5.149 +
   5.150 +\begin{pgnote}
   5.151 +You can choose a different logic via the \textsf{Isabelle} $>$
   5.152 +\textsf{Logics} menu. For example, you may want to work in the real
   5.153 +numbers, an extension of HOL (see \S\ref{sec:real}).
   5.154 +% This is just excess baggage:
   5.155 +%(You have to restart Proof General if you only compile the new logic
   5.156 +%after having launching Proof General already).
   5.157 +\end{pgnote}
     6.1 --- a/doc-src/TutorialI/tutorial.tex	Fri Jun 10 17:59:12 2005 +0200
     6.2 +++ b/doc-src/TutorialI/tutorial.tex	Fri Jun 10 18:36:47 2005 +0200
     6.3 @@ -18,7 +18,6 @@
     6.4  \index{structural induction|see{induction, structural}}
     6.5  \index{termination|see{functions, total}}
     6.6  \index{tuples|see{pairs and tuples}}
     6.7 -\index{settings|see{flags}}
     6.8  \index{*<*lex*>|see{lexicographic product}}
     6.9  
    6.10  \underscoreoff