author | nipkow |

Fri Jun 10 18:36:47 2005 +0200 (2005-06-10) | |

changeset 16359 | af7239e3054d |

parent 16358 | 2e2a506553a3 |

child 16360 | 6897b5958be7 |

tuning

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