doc-src/TutorialI/basics.tex
 author nipkow Mon Jun 06 21:20:54 2005 +0200 (2005-06-06) changeset 16306 8117e2037d3b parent 15429 b08a5eaf22e3 child 16359 af7239e3054d permissions -rw-r--r--
updating...
 wenzelm@12668  1 \chapter{The Basics}  nipkow@8743  2 nipkow@8743  3 \section{Introduction}  nipkow@8743  4 paulson@11405  5 This book is a tutorial on how to use the theorem prover Isabelle/HOL as a  paulson@11405  6 specification and verification system. Isabelle is a generic system for  paulson@11405  7 implementing logical formalisms, and Isabelle/HOL is the specialization  paulson@11405  8 of Isabelle for HOL, which abbreviates Higher-Order Logic. We introduce  paulson@11405  9 HOL step by step following the equation  nipkow@8743  10 $\mbox{HOL} = \mbox{Functional Programming} + \mbox{Logic}.$  paulson@11456  11 We do not assume that you are familiar with mathematical logic.  paulson@11456  12 However, we do assume that  paulson@11456  13 you are used to logical and set theoretic notation, as covered  paulson@11456  14 in a good discrete mathematics course~\cite{Rosen-DMA}, and  paulson@11450  15 that you are familiar with the basic concepts of functional  nipkow@11209  16 programming~\cite{Bird-Haskell,Hudak-Haskell,paulson-ml2,Thompson-Haskell}.  nipkow@11209  17 Although this tutorial initially concentrates on functional programming, do  nipkow@11209  18 not be misled: HOL can express most mathematical concepts, and functional  nipkow@11209  19 programming is just one particularly simple and ubiquitous instance.  nipkow@8743  20 nipkow@11205  21 Isabelle~\cite{paulson-isa-book} is implemented in ML~\cite{SML}. This has  nipkow@11205  22 influenced some of Isabelle/HOL's concrete syntax but is otherwise irrelevant  paulson@11450  23 for us: this tutorial is based on  nipkow@11213  24 Isabelle/Isar~\cite{isabelle-isar-ref}, an extension of Isabelle which hides  nipkow@11213  25 the implementation language almost completely. Thus the full name of the  nipkow@11213  26 system should be Isabelle/Isar/HOL, but that is a bit of a mouthful.  nipkow@11213  27 nipkow@11213  28 There are other implementations of HOL, in particular the one by Mike Gordon  paulson@11450  29 \index{Gordon, Mike}%  nipkow@11213  30 \emph{et al.}, which is usually referred to as the HOL system''  nipkow@11213  31 \cite{mgordon-hol}. For us, HOL refers to the logical system, and sometimes  paulson@11450  32 its incarnation Isabelle/HOL\@.  nipkow@8743  33 nipkow@8743  34 A tutorial is by definition incomplete. Currently the tutorial only  nipkow@8743  35 introduces the rudiments of Isar's proof language. To fully exploit the power  nipkow@11213  36 of Isar, in particular the ability to write readable and structured proofs,  nipkow@15429  37 you should start with Nipkow's overview~\cite{Nipkow-TYPES02} and consult  nipkow@15429  38 the Isabelle/Isar Reference Manual~\cite{isabelle-isar-ref} and Wenzel's  nipkow@15429  39 PhD thesis~\cite{Wenzel-PhD} (which discusses many proof patterns)  nipkow@15429  40 for further details. If you want to use Isabelle's ML level  nipkow@8743  41 directly (for example for writing your own proof procedures) see the Isabelle  nipkow@8743  42 Reference Manual~\cite{isabelle-ref}; for details relating to HOL see the  nipkow@8743  43 Isabelle/HOL manual~\cite{isabelle-HOL}. All manuals have a comprehensive  nipkow@8743  44 index.  nipkow@8743  45 nipkow@8743  46 \section{Theories}  nipkow@8743  47 \label{sec:Basic:Theories}  nipkow@8743  48 paulson@11428  49 \index{theories|(}%  nipkow@8743  50 Working with Isabelle means creating theories. Roughly speaking, a  paulson@11428  51 \textbf{theory} is a named collection of types, functions, and theorems,  nipkow@8743  52 much like a module in a programming language or a specification in a  nipkow@8743  53 specification language. In fact, theories in HOL can be either. The general  nipkow@8743  54 format of a theory \texttt{T} is  nipkow@8743  55 \begin{ttbox}  nipkow@15136  56 theory T  nipkow@15141  57 imports B$$@1$$ $$\ldots$$ B$$@n$$  nipkow@15136  58 begin  paulson@11450  59 {\rmfamily\textit{declarations, definitions, and proofs}}  nipkow@8743  60 end  nipkow@15358  61 \end{ttbox}\cmmdx{theory}\cmmdx{imports}  nipkow@15136  62 where \texttt{B}$@1$ \dots\ \texttt{B}$@n$ are the names of existing  paulson@11450  63 theories that \texttt{T} is based on and \textit{declarations,  paulson@11450  64  definitions, and proofs} represents the newly introduced concepts  nipkow@8771  65 (types, functions etc.) and proofs about them. The \texttt{B}$@i$ are the  paulson@11450  66 direct \textbf{parent theories}\indexbold{parent theories} of~\texttt{T}\@.  paulson@11450  67 Everything defined in the parent theories (and their parents, recursively) is  nipkow@8743  68 automatically visible. To avoid name clashes, identifiers can be  paulson@11450  69 \textbf{qualified}\indexbold{identifiers!qualified}  paulson@11450  70 by theory names as in \texttt{T.f} and~\texttt{B.f}.  paulson@11450  71 Each theory \texttt{T} must  paulson@11428  72 reside in a \textbf{theory file}\index{theory files} named \texttt{T.thy}.  nipkow@8743  73 nipkow@8743  74 This tutorial is concerned with introducing you to the different linguistic  paulson@11450  75 constructs that can fill the \textit{declarations, definitions, and  paulson@11450  76  proofs} above. A complete grammar of the basic  nipkow@12327  77 constructs is found in the Isabelle/Isar Reference  nipkow@12327  78 Manual~\cite{isabelle-isar-ref}.  nipkow@8743  79 nipkow@8743  80 \begin{warn}  paulson@11428  81  HOL contains a theory \thydx{Main}, the union of all the basic  paulson@10885  82  predefined theories like arithmetic, lists, sets, etc.  paulson@10885  83  Unless you know what you are doing, always include \isa{Main}  nipkow@10971  84  as a direct or indirect parent of all your theories.  nipkow@12332  85 \end{warn}  nipkow@16306  86 HOL's theory collection is available online at  nipkow@16306  87 \begin{center}\small  nipkow@16306  88  \url{http://isabelle.in.tum.de/library/HOL/}  nipkow@16306  89 \end{center}  nipkow@16306  90 and is recommended browsing.  nipkow@12473  91 There is also a growing Library~\cite{HOL-Library}\index{Library}  nipkow@13814  92 of useful theories that are not part of \isa{Main} but can be included  nipkow@16306  93 among the parents of a theory and will then be loaded automatically.  nipkow@16306  94 nipkow@16306  95 For the more adventurous, there is the \emph{Archive of Formal Proofs},  nipkow@16306  96 a journal-like collection of more advanced Isabelle theories:  nipkow@16306  97 \begin{center}\small  nipkow@16306  98  \url{http://afp.sourceforge.net/}  nipkow@16306  99 \end{center}  nipkow@16306  100 We hope that you will contribute to it yourself one day.%  paulson@11428  101 \index{theories|)}  nipkow@8743  102 nipkow@8743  103 paulson@10885  104 \section{Types, Terms and Formulae}  nipkow@8743  105 \label{sec:TypesTermsForms}  nipkow@8743  106 paulson@10795  107 Embedded in a theory are the types, terms and formulae of HOL\@. HOL is a typed  nipkow@8771  108 logic whose type system resembles that of functional programming languages  paulson@11450  109 like ML or Haskell. Thus there are  paulson@11450  110 \index{types|(}  nipkow@8743  111 \begin{description}  paulson@11450  112 \item[base types,]  paulson@11450  113 in particular \tydx{bool}, the type of truth values,  paulson@11428  114 and \tydx{nat}, the type of natural numbers.  paulson@11450  115 \item[type constructors,]\index{type constructors}  paulson@11450  116  in particular \tydx{list}, the type of  paulson@11428  117 lists, and \tydx{set}, the type of sets. Type constructors are written  nipkow@8771  118 postfix, e.g.\ \isa{(nat)list} is the type of lists whose elements are  nipkow@8743  119 natural numbers. Parentheses around single arguments can be dropped (as in  nipkow@8771  120 \isa{nat list}), multiple arguments are separated by commas (as in  nipkow@8771  121 \isa{(bool,nat)ty}).  paulson@11450  122 \item[function types,]\index{function types}  paulson@11450  123 denoted by \isasymFun\indexbold{$IsaFun@\isasymFun}.  nipkow@8771  124  In HOL \isasymFun\ represents \emph{total} functions only. As is customary,  nipkow@8771  125  \isa{$\tau@1$\isasymFun~$\tau@2$\isasymFun~$\tau@3$} means  nipkow@8771  126  \isa{$\tau@1$\isasymFun~($\tau@2$\isasymFun~$\tau@3$)}. Isabelle also  nipkow@8771  127  supports the notation \isa{[$\tau@1,\dots,\tau@n$] \isasymFun~$\tau$}  nipkow@8771  128  which abbreviates \isa{$\tau@1$\isasymFun~$\cdots$\isasymFun~$\tau@n$ nipkow@8743  129  \isasymFun~$\tau$}.  paulson@11450  130 \item[type variables,]\index{type variables}\index{variables!type}  paulson@10795  131  denoted by \ttindexboldpos{'a}{$Isatype}, \isa{'b} etc., just like in ML\@. They give rise  nipkow@8771  132  to polymorphic types like \isa{'a \isasymFun~'a}, the type of the identity  nipkow@8771  133  function.  nipkow@8743  134 \end{description}  nipkow@8743  135 \begin{warn}  nipkow@8743  136  Types are extremely important because they prevent us from writing  nipkow@8743  137  nonsense. Isabelle insists that all terms and formulae must be well-typed  nipkow@8743  138  and will print an error message if a type mismatch is encountered. To  nipkow@8743  139  reduce the amount of explicit type information that needs to be provided by  nipkow@8743  140  the user, Isabelle infers the type of all variables automatically (this is  nipkow@8743  141  called \bfindex{type inference}) and keeps quiet about it. Occasionally  nipkow@8743  142  this may lead to misunderstandings between you and the system. If anything  nipkow@16306  143  strange happens, we recommend that you ask Isabelle to display all type  nipkow@16306  144  information. This is best done through the Proof General interface; see  nipkow@16306  145  \S\ref{sec:interface} for details.  paulson@11450  146 \end{warn}%  paulson@11450  147 \index{types|)}  nipkow@8743  148 nipkow@8743  149 paulson@11450  150 \index{terms|(}  paulson@11450  151 \textbf{Terms} are formed as in functional programming by  nipkow@8771  152 applying functions to arguments. If \isa{f} is a function of type  nipkow@8771  153 \isa{$\tau@1$ \isasymFun~$\tau@2$} and \isa{t} is a term of type  nipkow@8771  154 $\tau@1$ then \isa{f~t} is a term of type $\tau@2$. HOL also supports  nipkow@8771  155 infix functions like \isa{+} and some basic constructs from functional  paulson@11428  156 programming, such as conditional expressions:  nipkow@8743  157 \begin{description}  paulson@11450  158 \item[\isa{if $b$ then $t@1$ else $t@2$}]\index{*if expressions}  paulson@11428  159 Here $b$ is of type \isa{bool} and $t@1$ and $t@2$ are of the same type.  paulson@11450  160 \item[\isa{let $x$ = $t$ in $u$}]\index{*let expressions}  nipkow@13814  161 is equivalent to $u$ where all free occurrences of $x$ have been replaced by  nipkow@8743  162 $t$. For example,  nipkow@8771  163 \isa{let x = 0 in x+x} is equivalent to \isa{0+0}. Multiple bindings are separated  nipkow@13814  164 by semicolons: \isa{let $x@1$ = $t@1$;\dots; $x@n$ = $t@n$ in $u$}.  nipkow@8771  165 \item[\isa{case $e$ of $c@1$ \isasymFun~$e@1$ |~\dots~| $c@n$ \isasymFun~$e@n$}]  paulson@11450  166 \index{*case expressions}  nipkow@8771  167 evaluates to $e@i$ if $e$ is of the form $c@i$.  nipkow@8743  168 \end{description}  nipkow@8743  169 nipkow@8743  170 Terms may also contain  paulson@11450  171 \isasymlambda-abstractions.\index{lambda@$\lambda$ expressions}  paulson@11450  172 For example,  nipkow@8771  173 \isa{\isasymlambda{}x.~x+1} is the function that takes an argument \isa{x} and  nipkow@8771  174 returns \isa{x+1}. Instead of  nipkow@8771  175 \isa{\isasymlambda{}x.\isasymlambda{}y.\isasymlambda{}z.~$t$} we can write  paulson@11450  176 \isa{\isasymlambda{}x~y~z.~$t$}.%  paulson@11450  177 \index{terms|)}  nipkow@8743  178 paulson@11450  179 \index{formulae|(}%  paulson@11450  180 \textbf{Formulae} are terms of type \tydx{bool}.  paulson@11428  181 There are the basic constants \cdx{True} and \cdx{False} and  nipkow@8771  182 the usual logical connectives (in decreasing order of priority):  paulson@11420  183 \indexboldpos{\protect\isasymnot}{$HOL0not}, \indexboldpos{\protect\isasymand}{$HOL0and},  paulson@11420  184 \indexboldpos{\protect\isasymor}{$HOL0or}, and \indexboldpos{\protect\isasymimp}{$HOL0imp},  nipkow@8743  185 all of which (except the unary \isasymnot) associate to the right. In  nipkow@8771  186 particular \isa{A \isasymimp~B \isasymimp~C} means \isa{A \isasymimp~(B  nipkow@8771  187  \isasymimp~C)} and is thus logically equivalent to \isa{A \isasymand~B  nipkow@8771  188  \isasymimp~C} (which is \isa{(A \isasymand~B) \isasymimp~C}).  nipkow@8743  189 paulson@11450  190 Equality\index{equality} is available in the form of the infix function  paulson@11450  191 \isa{=} of type \isa{'a \isasymFun~'a  nipkow@8771  192  \isasymFun~bool}. Thus \isa{$t@1$ = $t@2$} is a formula provided $t@1$  paulson@11450  193 and $t@2$ are terms of the same type. If $t@1$ and $t@2$ are of type  paulson@11450  194 \isa{bool} then \isa{=} acts as \rmindex{if-and-only-if}.  paulson@11450  195 The formula  nipkow@8771  196 \isa{$t@1$~\isasymnoteq~$t@2$} is merely an abbreviation for  nipkow@8771  197 \isa{\isasymnot($t@1$ = $t@2$)}.  nipkow@8743  198 paulson@11450  199 Quantifiers\index{quantifiers} are written as  paulson@11450  200 \isa{\isasymforall{}x.~$P$} and \isa{\isasymexists{}x.~$P$}.  paulson@11420  201 There is even  paulson@11450  202 \isa{\isasymuniqex{}x.~$P$}, which  paulson@11420  203 means that there exists exactly one \isa{x} that satisfies \isa{$P$}.  paulson@11420  204 Nested quantifications can be abbreviated:  paulson@11420  205 \isa{\isasymforall{}x~y~z.~$P$} means  paulson@11450  206 \isa{\isasymforall{}x.\isasymforall{}y.\isasymforall{}z.~$P$}.%  paulson@11450  207 \index{formulae|)}  nipkow@8743  208 nipkow@8743  209 Despite type inference, it is sometimes necessary to attach explicit  paulson@11428  210 \bfindex{type constraints} to a term. The syntax is  nipkow@8771  211 \isa{$t$::$\tau$} as in \isa{x < (y::nat)}. Note that  nipkow@10538  212 \ttindexboldpos{::}{$Isatype} binds weakly and should therefore be enclosed  paulson@11450  213 in parentheses. For instance,  paulson@11450  214 \isa{x < y::nat} is ill-typed because it is interpreted as  paulson@11450  215 \isa{(x < y)::nat}. Type constraints may be needed to disambiguate  paulson@11450  216 expressions  paulson@11450  217 involving overloaded functions such as~\isa{+},  paulson@11450  218 \isa{*} and~\isa{<}. Section~\ref{sec:overloading}  paulson@11450  219 discusses overloading, while Table~\ref{tab:overloading} presents the most  nipkow@10695  220 important overloaded function symbols.  nipkow@8743  221 paulson@11450  222 In general, HOL's concrete \rmindex{syntax} tries to follow the conventions of  paulson@11450  223 functional programming and mathematics. Here are the main rules that you  paulson@11450  224 should be familiar with to avoid certain syntactic traps:  nipkow@8743  225 \begin{itemize}  nipkow@8743  226 \item  nipkow@8771  227 Remember that \isa{f t u} means \isa{(f t) u} and not \isa{f(t u)}!  nipkow@8743  228 \item  nipkow@8771  229 Isabelle allows infix functions like \isa{+}. The prefix form of function  nipkow@8771  230 application binds more strongly than anything else and hence \isa{f~x + y}  nipkow@8771  231 means \isa{(f~x)~+~y} and not \isa{f(x+y)}.  nipkow@8743  232 \item Remember that in HOL if-and-only-if is expressed using equality. But  nipkow@8743  233  equality has a high priority, as befitting a relation, while if-and-only-if  nipkow@8771  234  typically has the lowest priority. Thus, \isa{\isasymnot~\isasymnot~P =  nipkow@8771  235  P} means \isa{\isasymnot\isasymnot(P = P)} and not  nipkow@8771  236  \isa{(\isasymnot\isasymnot P) = P}. When using \isa{=} to mean  nipkow@8771  237  logical equivalence, enclose both operands in parentheses, as in \isa{(A  nipkow@8743  238  \isasymand~B) = (B \isasymand~A)}.  nipkow@8743  239 \item  nipkow@8743  240 Constructs with an opening but without a closing delimiter bind very weakly  nipkow@8743  241 and should therefore be enclosed in parentheses if they appear in subterms, as  paulson@11450  242 in \isa{(\isasymlambda{}x.~x) = f}. This includes  paulson@11450  243 \isa{if},\index{*if expressions}  paulson@11450  244 \isa{let},\index{*let expressions}  paulson@11450  245 \isa{case},\index{*case expressions}  paulson@11450  246 \isa{\isasymlambda}, and quantifiers.  nipkow@8743  247 \item  nipkow@8771  248 Never write \isa{\isasymlambda{}x.x} or \isa{\isasymforall{}x.x=x}  nipkow@12327  249 because \isa{x.x} is always taken as a single qualified identifier. Write  nipkow@8771  250 \isa{\isasymlambda{}x.~x} and \isa{\isasymforall{}x.~x=x} instead.  paulson@11450  251 \item Identifiers\indexbold{identifiers} may contain the characters \isa{_}  nipkow@12327  252 and~\isa{'}, except at the beginning.  nipkow@8743  253 \end{itemize}  nipkow@8743  254 paulson@11450  255 For the sake of readability, we use the usual mathematical symbols throughout  nipkow@10983  256 the tutorial. Their \textsc{ascii}-equivalents are shown in table~\ref{tab:ascii} in  nipkow@8771  257 the appendix.  nipkow@8771  258 paulson@11450  259 \begin{warn}  paulson@11450  260 A particular  paulson@11450  261 problem for novices can be the priority of operators. If you are unsure, use  paulson@11450  262 additional parentheses. In those cases where Isabelle echoes your  paulson@11450  263 input, you can see which parentheses are dropped --- they were superfluous. If  paulson@11450  264 you are unsure how to interpret Isabelle's output because you don't know  paulson@11450  265 where the (dropped) parentheses go, set the flag\index{flags}  paulson@11450  266 \isa{show_brackets}\index{*show_brackets (flag)}:  paulson@11450  267 \begin{ttbox}  paulson@11450  268 ML "set show_brackets"; $$\dots$$; ML "reset show_brackets";  paulson@11450  269 \end{ttbox}  paulson@11450  270 \end{warn}  paulson@11450  271 nipkow@8743  272 nipkow@8743  273 \section{Variables}  nipkow@8743  274 \label{sec:variables}  paulson@11450  275 \index{variables|(}  nipkow@8743  276 paulson@11450  277 Isabelle distinguishes free and bound variables, as is customary. Bound  nipkow@8743  278 variables are automatically renamed to avoid clashes with free variables. In  paulson@11428  279 addition, Isabelle has a third kind of variable, called a \textbf{schematic  paulson@11428  280  variable}\index{variables!schematic} or \textbf{unknown}\index{unknowns},  nipkow@13439  281 which must have a~\isa{?} as its first character.  paulson@11428  282 Logically, an unknown is a free variable. But it may be  nipkow@8743  283 instantiated by another term during the proof process. For example, the  nipkow@8771  284 mathematical theorem$x = x$is represented in Isabelle as \isa{?x = ?x},  nipkow@8743  285 which means that Isabelle can instantiate it arbitrarily. This is in contrast  nipkow@8743  286 to ordinary variables, which remain fixed. The programming language Prolog  nipkow@8743  287 calls unknowns {\em logical\/} variables.  nipkow@8743  288 nipkow@8743  289 Most of the time you can and should ignore unknowns and work with ordinary  nipkow@8743  290 variables. Just don't be surprised that after you have finished the proof of  paulson@11450  291 a theorem, Isabelle will turn your free variables into unknowns. It  nipkow@8743  292 indicates that Isabelle will automatically instantiate those unknowns  nipkow@8743  293 suitably when the theorem is used in some other proof.  nipkow@9689  294 Note that for readability we often drop the \isa{?}s when displaying a theorem.  nipkow@8743  295 \begin{warn}  paulson@11450  296  For historical reasons, Isabelle accepts \isa{?} as an ASCII representation  paulson@11450  297  of the $$\exists$$ symbol. However, the \isa{?} character must then be followed  paulson@11450  298  by a space, as in \isa{?~x. f(x) = 0}. Otherwise, \isa{?x} is  paulson@11450  299  interpreted as a schematic variable. The preferred ASCII representation of  paulson@11450  300  the $$\exists$$ symbol is \isa{EX}\@.  paulson@11450  301 \end{warn}%  paulson@11450  302 \index{variables|)}  nipkow@8743  303 paulson@10885  304 \section{Interaction and Interfaces}  nipkow@16306  305 \label{sec:interface}  nipkow@8771  306 nipkow@8771  307 Interaction with Isabelle can either occur at the shell level or through more  paulson@11301  308 advanced interfaces. To keep the tutorial independent of the interface, we  paulson@11301  309 have phrased the description of the interaction in a neutral language. For  nipkow@8771  310 example, the phrase to abandon a proof'' means to type \isacommand{oops} at the  nipkow@8771  311 shell level, which is explained the first time the phrase is used. Other  nipkow@8771  312 interfaces perform the same act by cursor movements and/or mouse clicks.  nipkow@8771  313 Although shell-based interaction is quite feasible for the kind of proof  nipkow@8771  314 scripts currently presented in this tutorial, the recommended interface for  nipkow@8771  315 Isabelle/Isar is the Emacs-based \bfindex{Proof  paulson@11450  316  General}~\cite{proofgeneral,Aspinall:TACAS:2000}.  nipkow@8771  317 nipkow@16306  318 \begin{pgnote}  nipkow@16306  319 Proof General specific information is always displayed in paragraphs  nipkow@16306  320 identified by this miniature Proof General icon.  nipkow@8771  321 nipkow@16306  322 On particularly nice feature of Proof General is its support for a special  nipkow@16306  323 fonts with mathematical symbols. Most symbols have  nipkow@16306  324 \textsc{ascii}-equivalents: for example, you can enter either \verb!&!  nipkow@16306  325 or \verb!\! to obtain$\land\$. For a list of the most frequent symbols  nipkow@16306  326 see table~\ref{tab:ascii} in the appendix.  nipkow@16306  327 \end{pgnote}  nipkow@8771  328 nipkow@16306  329 \begin{pgnote}  nipkow@16306  330 Proof General offers an \texttt{Isabelle} menu for displaying information  nipkow@16306  331 and setting flags. A particularly useful flag is \texttt{Show Types}  nipkow@16306  332 which causes Isabelle to output the type information that is usually  nipkow@16306  333 suppressed. This is indispensible in case of errors of all kinds  nipkow@16306  334 because often the types reveal the source of the problem. Once you have  nipkow@16306  335 diagnosed the problem you may no longer want to see the types because they  nipkow@16306  336 clutter all output. Simply reset the flag.  nipkow@16306  337 \end{pgnote}  nipkow@8771  338 paulson@10885  339 \section{Getting Started}  nipkow@8743  340 nipkow@8743  341 Assuming you have installed Isabelle, you start it by typing \texttt{isabelle  nipkow@8743  342  -I HOL} in a shell window.\footnote{Simply executing \texttt{isabelle -I}  nipkow@8743  343  starts the default logic, which usually is already \texttt{HOL}. This is  nipkow@8743  344  controlled by the \texttt{ISABELLE_LOGIC} setting, see \emph{The Isabelle  nipkow@8743  345  System Manual} for more details.} This presents you with Isabelle's most  nipkow@10983  346 basic \textsc{ascii} interface. In addition you need to open an editor window to  paulson@11450  347 create theory files. While you are developing a theory, we recommend that you  nipkow@8743  348 type each command into the file first and then enter it into Isabelle by  nipkow@8743  349 copy-and-paste, thus ensuring that you have a complete record of your theory.  nipkow@8771  350 As mentioned above, Proof General offers a much superior interface.  paulson@10795  351 If you have installed Proof General, you can start it by typing \texttt{Isabelle}.