summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | nipkow |

Fri, 10 Jun 2005 18:36:47 +0200 | |

changeset 16359 | af7239e3054d |

parent 16358 | 2e2a506553a3 |

child 16360 | 6897b5958be7 |

tuning

--- a/doc-src/TutorialI/Misc/document/simp.tex Fri Jun 10 17:59:12 2005 +0200 +++ b/doc-src/TutorialI/Misc/document/simp.tex Fri Jun 10 18:36:47 2005 +0200 @@ -441,13 +441,9 @@ \begin{isamarkuptext}% \indexbold{tracing the simplifier} Using the simplifier effectively may take a bit of experimentation. Set the -\isa{trace_simp}\index{*trace_simp (flag)} flag\index{flags} -to get a better idea of what is going -on:% +Proof General flag \textsf{Isabelle} $>$ \textsf{Settings} $>$ \textsf{Trace Simplifier} to get a better idea of what is going on:% \end{isamarkuptext}% \isamarkuptrue% -\isacommand{ML}\ {\isachardoublequote}set\ trace{\isacharunderscore}simp{\isachardoublequote}\isanewline -\isamarkupfalse% \isacommand{lemma}\ {\isachardoublequote}rev\ {\isacharbrackleft}a{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequote}\isanewline \isamarkupfalse% \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isamarkupfalse% @@ -455,40 +451,50 @@ % \begin{isamarkuptext}% \noindent -produces the trace +produces the following trace in Proof General's \textsf{Trace} buffer: \begin{ttbox}\makeatother -Applying instance of rewrite rule: -rev (?x1 \# ?xs1) == rev ?xs1 @ [?x1] -Rewriting: -rev [a] == rev [] @ [a] -Applying instance of rewrite rule: -rev [] == [] -Rewriting: -rev [] == [] -Applying instance of rewrite rule: -[] @ ?y == ?y -Rewriting: -[] @ [a] == [a] -Applying instance of rewrite rule: -?x3 \# ?t3 = ?t3 == False -Rewriting: -[a] = [] == False +[0]Applying instance of rewrite rule "List.rev.simps_2": +rev (?x1 # ?xs1) \(\equiv\) rev ?xs1 @ [?x1] + +[0]Rewriting: +rev [a] \(\equiv\) rev [] @ [a] + +[0]Applying instance of rewrite rule "List.rev.simps_1": +rev [] \(\equiv\) [] + +[0]Rewriting: +rev [] \(\equiv\) [] + +[0]Applying instance of rewrite rule "List.op @.append_Nil": +[] @ ?y \(\equiv\) ?y + +[0]Rewriting: +[] @ [a] \(\equiv\) [a] + +[0]Applying instance of rewrite rule +?x2 # ?t1 = ?t1 \(\equiv\) False + +[0]Rewriting: +[a] = [] \(\equiv\) False \end{ttbox} +The trace lists each rule being applied, both in its general form and +the instance being used. The \texttt{[}$i$\texttt{]} in front (where +above $i$ is always \texttt{0}) indicates that we are inside the $i$th +recursive invocation of the simplifier. Each attempt to apply a +conditional rule shows the rule followed by the trace of the +(recursive!) simplification of the conditions, the latter prefixed by +\texttt{[}$i+1$\texttt{]} instead of \texttt{[}$i$\texttt{]}. +Another source of recursive invocations of the simplifier are +proofs of arithmetic formulae. -The trace lists each rule being applied, both in its general form and the -instance being used. For conditional rules, the trace lists the rule -it is trying to rewrite and gives the result of attempting to prove -each of the rule's conditions. Many other hints about the simplifier's -actions will appear. +Many other hints about the simplifier's actions may appear. -In more complicated cases, the trace can be quite lengthy. Invocations of the -simplifier are often nested, for instance when solving conditions of rewrite -rules. Thus it is advisable to reset it:% +In more complicated cases, the trace can be very lengthy. Thus it is +advisable to reset the \textsf{Trace Simplifier} flag after having +obtained the desired trace.% \end{isamarkuptext}% \isamarkuptrue% -\isacommand{ML}\ {\isachardoublequote}reset\ trace{\isacharunderscore}simp{\isachardoublequote}\isanewline -\isamarkupfalse% \isamarkupfalse% \end{isabellebody}% %%% Local Variables:

--- a/doc-src/TutorialI/Misc/simp.thy Fri Jun 10 17:59:12 2005 +0200 +++ b/doc-src/TutorialI/Misc/simp.thy Fri Jun 10 18:36:47 2005 +0200 @@ -367,50 +367,56 @@ subsection{*Tracing*} text{*\indexbold{tracing the simplifier} Using the simplifier effectively may take a bit of experimentation. Set the -\isa{trace_simp}\index{*trace_simp (flag)} flag\index{flags} -to get a better idea of what is going -on: +Proof General flag \textsf{Isabelle} $>$ \textsf{Settings} $>$ \textsf{Trace Simplifier} to get a better idea of what is going on: *} -ML "set trace_simp" lemma "rev [a] = []" apply(simp) (*<*)oops(*>*) text{*\noindent -produces the trace +produces the following trace in Proof General's \textsf{Trace} buffer: \begin{ttbox}\makeatother -Applying instance of rewrite rule: -rev (?x1 \# ?xs1) == rev ?xs1 @ [?x1] -Rewriting: -rev [a] == rev [] @ [a] -Applying instance of rewrite rule: -rev [] == [] -Rewriting: -rev [] == [] -Applying instance of rewrite rule: -[] @ ?y == ?y -Rewriting: -[] @ [a] == [a] -Applying instance of rewrite rule: -?x3 \# ?t3 = ?t3 == False -Rewriting: -[a] = [] == False +[0]Applying instance of rewrite rule "List.rev.simps_2": +rev (?x1 # ?xs1) \(\equiv\) rev ?xs1 @ [?x1] + +[0]Rewriting: +rev [a] \(\equiv\) rev [] @ [a] + +[0]Applying instance of rewrite rule "List.rev.simps_1": +rev [] \(\equiv\) [] + +[0]Rewriting: +rev [] \(\equiv\) [] + +[0]Applying instance of rewrite rule "List.op @.append_Nil": +[] @ ?y \(\equiv\) ?y + +[0]Rewriting: +[] @ [a] \(\equiv\) [a] + +[0]Applying instance of rewrite rule +?x2 # ?t1 = ?t1 \(\equiv\) False + +[0]Rewriting: +[a] = [] \(\equiv\) False \end{ttbox} - -The trace lists each rule being applied, both in its general form and the -instance being used. For conditional rules, the trace lists the rule -it is trying to rewrite and gives the result of attempting to prove -each of the rule's conditions. Many other hints about the simplifier's -actions will appear. +The trace lists each rule being applied, both in its general form and +the instance being used. The \texttt{[}$i$\texttt{]} in front (where +above $i$ is always \texttt{0}) indicates that we are inside the $i$th +recursive invocation of the simplifier. Each attempt to apply a +conditional rule shows the rule followed by the trace of the +(recursive!) simplification of the conditions, the latter prefixed by +\texttt{[}$i+1$\texttt{]} instead of \texttt{[}$i$\texttt{]}. +Another source of recursive invocations of the simplifier are +proofs of arithmetic formulae. -In more complicated cases, the trace can be quite lengthy. Invocations of the -simplifier are often nested, for instance when solving conditions of rewrite -rules. Thus it is advisable to reset it: -*} +Many other hints about the simplifier's actions may appear. -ML "reset trace_simp" +In more complicated cases, the trace can be very lengthy. Thus it is +advisable to reset the \textsf{Trace Simplifier} flag after having +obtained the desired trace. *} (*<*) end

--- a/doc-src/TutorialI/Rules/rules.tex Fri Jun 10 17:59:12 2005 +0200 +++ b/doc-src/TutorialI/Rules/rules.tex Fri Jun 10 18:36:47 2005 +0200 @@ -634,14 +634,18 @@ as $\exists x.\,P$, they let us proceed with a proof. They can be filled in later, sometimes in stages and often automatically. -If unification fails when you think it should succeed, try setting the flag \index{flags}\isa{trace_unify_fail}\index{*trace_unify_fail (flag)}, -which makes Isabelle show the cause of unification failures. For example, suppose we are trying to prove this subgoal by assumption: +\begin{pgnote} +If unification fails when you think it should succeed, try setting the Proof General flag \textsf{Isabelle} $>$ \textsf{Settings} $>$ +\textsf{Trace Unification}, +which makes Isabelle show the cause of unification failures (in Proof +General's \textsf{Trace} buffer). +\end{pgnote} +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) \end{isabelle} The \isa{assumption} method having failed, we try again with the flag set: \begin{isabelle} -\isacommand{ML}\ "set\ trace\_unify\_fail"\isanewline \isacommand{apply} assumption \end{isabelle} Even in this trivial case, the output is unexpectedly verbose, but it yields the necessary information:

--- a/doc-src/TutorialI/Types/numerics.tex Fri Jun 10 17:59:12 2005 +0200 +++ b/doc-src/TutorialI/Types/numerics.tex Fri Jun 10 18:36:47 2005 +0200 @@ -309,6 +309,7 @@ \subsection{The Types of Rational, Real and Complex Numbers} +\label{sec:real} \index{rational numbers|(}\index{*rat (type)|(}% \index{real numbers|(}\index{*real (type)|(}% @@ -340,15 +341,12 @@ is performed. \begin{warn} -Type \isa{real} is only available in the logic HOL-Complex, which -is HOL extended with a definitional development of the real and complex -numbers. Base your theory upon theory -\thydx{Complex_Main}, not the usual \isa{Main}.% +Type \isa{real} is only available in the logic HOL-Complex, which is +HOL extended with a definitional development of the real and complex +numbers. Base your theory upon theory \thydx{Complex_Main}, not the +usual \isa{Main}, and set the Proof General menu item \textsf{Isabelle} $>$ +\textsf{Logics} $>$ \textsf{HOL-Complex}.% \index{real numbers|)}\index{*real (type)|)} -Launch Isabelle using the command -\begin{verbatim} -Isabelle -l HOL-Complex -\end{verbatim} \end{warn} Also available in HOL-Complex is the

--- a/doc-src/TutorialI/basics.tex Fri Jun 10 17:59:12 2005 +0200 +++ b/doc-src/TutorialI/basics.tex Fri Jun 10 18:36:47 2005 +0200 @@ -87,10 +87,10 @@ \begin{center}\small \url{http://isabelle.in.tum.de/library/HOL/} \end{center} -and is recommended browsing. -There is also a growing Library~\cite{HOL-Library}\index{Library} -of useful theories that are not part of \isa{Main} but can be included -among the parents of a theory and will then be loaded automatically. +and is recommended browsing. In subdirectory \texttt{Library} you find +a growing library of useful theories that are not part of \isa{Main} +but can be included among the parents of a theory and will then be +loaded automatically. For the more adventurous, there is the \emph{Archive of Formal Proofs}, a journal-like collection of more advanced Isabelle theories: @@ -134,15 +134,17 @@ \end{description} \begin{warn} Types are extremely important because they prevent us from writing - nonsense. Isabelle insists that all terms and formulae must be well-typed - and will print an error message if a type mismatch is encountered. To - reduce the amount of explicit type information that needs to be provided by - the user, Isabelle infers the type of all variables automatically (this is - called \bfindex{type inference}) and keeps quiet about it. Occasionally - this may lead to misunderstandings between you and the system. If anything - strange happens, we recommend that you ask Isabelle to display all type - information. This is best done through the Proof General interface; see - \S\ref{sec:interface} for details. + nonsense. Isabelle insists that all terms and formulae must be + well-typed and will print an error message if a type mismatch is + encountered. To reduce the amount of explicit type information that + needs to be provided by the user, Isabelle infers the type of all + variables automatically (this is called \bfindex{type inference}) + and keeps quiet about it. Occasionally this may lead to + misunderstandings between you and the system. If anything strange + happens, we recommend that you ask Isabelle to display all type + information via the Proof General menu item \textsf{Isabelle} $>$ + \textsf{Settings} $>$ \textsf{Show Types} (see \S\ref{sec:interface} + for details). \end{warn}% \index{types|)} @@ -257,16 +259,13 @@ the appendix. \begin{warn} -A particular -problem for novices can be the priority of operators. If you are unsure, use -additional parentheses. In those cases where Isabelle echoes your -input, you can see which parentheses are dropped --- they were superfluous. If -you are unsure how to interpret Isabelle's output because you don't know -where the (dropped) parentheses go, set the flag\index{flags} -\isa{show_brackets}\index{*show_brackets (flag)}: -\begin{ttbox} -ML "set show_brackets"; \(\dots\); ML "reset show_brackets"; -\end{ttbox} +A particular problem for novices can be the priority of operators. If +you are unsure, use additional parentheses. In those cases where +Isabelle echoes your input, you can see which parentheses are dropped +--- they were superfluous. If you are unsure how to interpret +Isabelle's output because you don't know where the (dropped) +parentheses go, set the Proof General flag \textsf{Isabelle} $>$ +\textsf{Settings} $>$ \textsf{Show Brackets} (see \S\ref{sec:interface}). \end{warn} @@ -304,48 +303,52 @@ \section{Interaction and Interfaces} \label{sec:interface} -Interaction with Isabelle can either occur at the shell level or through more -advanced interfaces. To keep the tutorial independent of the interface, we -have phrased the description of the interaction in a neutral language. For -example, the phrase ``to abandon a proof'' means to type \isacommand{oops} at the -shell level, which is explained the first time the phrase is used. Other -interfaces perform the same act by cursor movements and/or mouse clicks. -Although shell-based interaction is quite feasible for the kind of proof -scripts currently presented in this tutorial, the recommended interface for -Isabelle/Isar is the Emacs-based \bfindex{Proof - General}~\cite{proofgeneral,Aspinall:TACAS:2000}. +The recommended interface for Isabelle/Isar is the (X)Emacs-based +\bfindex{Proof General}~\cite{proofgeneral,Aspinall:TACAS:2000}. +Interaction with Isabelle at the shell level, although possible, +should be avoided. Most of the tutorial is independent of the +interface and is phrased in a neutral language. For example, the +phrase ``to abandon a proof'' corresponds to the obvious +action of clicking on the \textsf{Undo} symbol in Proof General. +Proof General specific information is often displayed in paragraphs +identified by a miniature Proof General icon. Here are two examples: +\begin{pgnote} +Proof General supports a special font with mathematical symbols known +as ``x-symbols''. All symbols have \textsc{ascii}-equivalents: for +example, you can enter either \verb!&! or \verb!\<and>! to obtain +$\land$. For a list of the most frequent symbols see table~\ref{tab:ascii} +in the appendix. -\begin{pgnote} -Proof General specific information is always displayed in paragraphs -identified by this miniature Proof General icon. - -On particularly nice feature of Proof General is its support for a special -fonts with mathematical symbols. Most symbols have -\textsc{ascii}-equivalents: for example, you can enter either \verb!&! -or \verb!\<and>! to obtain $\land$. For a list of the most frequent symbols -see table~\ref{tab:ascii} in the appendix. +Note that by default x-symbols are not enabled. You have to switch +them on via the menu item \textsf{Proof-General} $>$ \textsf{Options} $>$ +\textsf{X-Symbols} (and save the option via the top-level +\textsf{Options} menu). \end{pgnote} \begin{pgnote} -Proof General offers an \texttt{Isabelle} menu for displaying information -and setting flags. A particularly useful flag is \texttt{Show Types} -which causes Isabelle to output the type information that is usually +Proof General offers the \textsf{Isabelle} menu for displaying +information and setting flags. A particularly useful flag is +\textsf{Isabelle} $>$ \textsf{Settings} $>$ \textsf{Show Types} which +causes Isabelle to output the type information that is usually suppressed. This is indispensible in case of errors of all kinds -because often the types reveal the source of the problem. Once you have -diagnosed the problem you may no longer want to see the types because they -clutter all output. Simply reset the flag. +because often the types reveal the source of the problem. Once you +have diagnosed the problem you may no longer want to see the types +because they clutter all output. Simply reset the flag. \end{pgnote} \section{Getting Started} -Assuming you have installed Isabelle, you start it by typing \texttt{isabelle - -I HOL} in a shell window.\footnote{Simply executing \texttt{isabelle -I} - starts the default logic, which usually is already \texttt{HOL}. This is - controlled by the \texttt{ISABELLE_LOGIC} setting, see \emph{The Isabelle - System Manual} for more details.} This presents you with Isabelle's most -basic \textsc{ascii} interface. In addition you need to open an editor window to -create theory files. While you are developing a theory, we recommend that you -type each command into the file first and then enter it into Isabelle by -copy-and-paste, thus ensuring that you have a complete record of your theory. -As mentioned above, Proof General offers a much superior interface. -If you have installed Proof General, you can start it by typing \texttt{Isabelle}. +Assuming you have installed Isabelle and Proof General, you start it by typing +\texttt{Isabelle} in a shell window. This launches a Proof General window. +By default, you are in HOL\footnote{This is controlled by the +\texttt{ISABELLE_LOGIC} setting, see \emph{The Isabelle System Manual} +for more details.}. + +\begin{pgnote} +You can choose a different logic via the \textsf{Isabelle} $>$ +\textsf{Logics} menu. For example, you may want to work in the real +numbers, an extension of HOL (see \S\ref{sec:real}). +% This is just excess baggage: +%(You have to restart Proof General if you only compile the new logic +%after having launching Proof General already). +\end{pgnote}

--- a/doc-src/TutorialI/tutorial.tex Fri Jun 10 17:59:12 2005 +0200 +++ b/doc-src/TutorialI/tutorial.tex Fri Jun 10 18:36:47 2005 +0200 @@ -18,7 +18,6 @@ \index{structural induction|see{induction, structural}} \index{termination|see{functions, total}} \index{tuples|see{pairs and tuples}} -\index{settings|see{flags}} \index{*<*lex*>|see{lexicographic product}} \underscoreoff