# HG changeset patch # User paulson # Date 1060789441 -7200 # Node ID 6580d374a509c4de4854bca34618380fc3c04ffc # Parent 331ab35e81f2387b1278391eaa02604b2ab6e320 corrections by Viktor Kuncak and minor updating diff -r 331ab35e81f2 -r 6580d374a509 doc-src/Intro/advanced.tex --- a/doc-src/Intro/advanced.tex Wed Aug 13 17:24:59 2003 +0200 +++ b/doc-src/Intro/advanced.tex Wed Aug 13 17:44:01 2003 +0200 @@ -48,14 +48,20 @@ \item If one or more premises involves the meta-connectives $\Forall$ or $\Imp$, then the command sets the goal to be $\phi$ and returns a list consisting of the theorems ${\theta@i\;[\theta@i]}$, for $i=1$, \ldots,~$k$. - These meta-assumptions are also recorded internally, allowing + These meta-level assumptions are also recorded internally, allowing \texttt{result} (which is called by \texttt{qed}) to discharge them in the original order. \end{itemize} Rules that discharge assumptions or introduce eigenvariables have complex -premises, and the second case applies. +premises, and the second case applies. In this section, many of the +theorems are subject to meta-level assumptions, so we make them visible by by setting the +\ttindex{show_hyps} flag: +\begin{ttbox} +set show_hyps; +{\out val it = true : bool} +\end{ttbox} -Let us derive $\conj$ elimination. Until now, calling \texttt{Goal} has +Now, we are ready to derive $\conj$ elimination. Until now, calling \texttt{Goal} has returned an empty list, which we have ignored. In this example, the list contains the two premises of the rule, since one of them involves the $\Imp$ connective. We bind them to the \ML\ identifiers \texttt{major} and {\tt @@ -357,7 +363,9 @@ \end{ttbox} where $id@1$, \ldots, $id@n$ are \ML{} identifiers and $rule@1$, \ldots, $rule@n$ are expressions of type~$prop$. Each rule {\em must\/} be -enclosed in quotation marks. +enclosed in quotation marks. Rules are simply axioms; they are +called \emph{rules} because they are mainly used to specify the inference +rules when defining a new logic. \indexbold{definitions} The {\bf definition part} is similar, but with the keyword \texttt{defs} instead of \texttt{rules}. {\bf Definitions} are @@ -368,10 +376,10 @@ of the equation instead of abstracted on the right-hand side. Isabelle checks for common errors in definitions, such as extra -variables on the right-hand side, but currently does not a complete -test of well-formedness. Thus determined users can write -non-conservative `definitions' by using mutual recursion, for example; -the consequences of such actions are their responsibility. +variables on the right-hand side and cyclic dependencies, that could +least to inconsistency. It is still essential to take care: +theorems proved on the basis of incorrect definitions are useless, +your system can be consistent and yet still wrong. \index{examples!of theories} This example theory extends first-order logic by declaring and defining two constants, {\em nand} and {\em @@ -682,7 +690,8 @@ \end{ttbox} Because $nat$ and $bool$ have class $arith$, we can use $0$, $1$ and $+$ at either type. The type constraints in the axioms are vital. Without -constraints, the $x$ in $1+x = x$ would have type $\alpha{::}arith$ +constraints, the $x$ in $1+x = 1$ (axiom \texttt{or1l}) +would have type $\alpha{::}arith$ and the axiom would hold for any type of class $arith$. This would collapse $nat$ to a trivial type: \[ Suc(1) = Suc(0+1) = Suc(0)+1 = 1+1 = 1! \] @@ -998,7 +1007,7 @@ {\out Suc(x) + m + n = Suc(x) + (m + n)} \end{ttbox} The inductive step requires rewriting by the equations for addition -together the induction hypothesis, which is also an equation. The +and with the induction hypothesis, which is also an equation. The tactic~\ttindex{Asm_simp_tac} rewrites using the implicit simplification set and any useful assumptions: \begin{ttbox} @@ -1219,7 +1228,7 @@ {\out rev(?x, a : b : c : Nil)} {\out 1. rev(?x, a : b : c : Nil)} \ttbreak -by (DEPTH_FIRST (has_fewer_prems 1) (resolve_tac rules 1)); +by prolog_tac; {\out Level 1} {\out rev(c : b : a : Nil, a : b : c : Nil)} {\out No subgoals!} diff -r 331ab35e81f2 -r 6580d374a509 doc-src/Intro/deriv.txt --- a/doc-src/Intro/deriv.txt Wed Aug 13 17:24:59 2003 +0200 +++ b/doc-src/Intro/deriv.txt Wed Aug 13 17:44:01 2003 +0200 @@ -4,7 +4,7 @@ print_depth 0; -val [major,minor] = goal Int_Rule.thy +val [major,minor] = goal IFOL.thy "[| P&Q; [| P; Q |] ==> R |] ==> R"; prth minor; by (resolve_tac [minor] 1); diff -r 331ab35e81f2 -r 6580d374a509 doc-src/Intro/getting.tex --- a/doc-src/Intro/getting.tex Wed Aug 13 17:24:59 2003 +0200 +++ b/doc-src/Intro/getting.tex Wed Aug 13 17:44:01 2003 +0200 @@ -1,12 +1,13 @@ %% $Id$ -\part{Getting Started with Isabelle}\label{chap:getting} -Let us consider how to perform simple proofs using Isabelle. At -present, Isabelle's user interface is \ML. Proofs are conducted by +\part{Using Isabelle from the ML Top-Level}\label{chap:getting} + +Most Isabelle users write proof scripts using the Isar language, as described in the \emph{Tutorial}, and debug them through the Proof General user interface~\cite{proofgeneral}. Isabelle's original user interface --- based on the \ML{} top-level --- is still available, however. +Proofs are conducted by applying certain \ML{} functions, which update a stored proof state. -Basically, all syntax must be expressed using plain {\sc ascii} -characters. There are also mechanisms built into Isabelle that support +All syntax can be expressed using plain {\sc ascii} +characters, but Isabelle can support alternative syntaxes, for example using mathematical symbols from a -special screen font. The meta-logic and major object-logics already +special screen font. The meta-logic and main object-logics already provide such fancy output as an option. Object-logics are built upon Pure Isabelle, which implements the @@ -167,7 +168,7 @@ \] To illustrate the notation, consider two axioms for first-order logic: $$ \List{P; Q} \Imp P\conj Q \eqno(\conj I) $$ -$$ \List{\exists x.P(x); \Forall x. P(x)\imp Q} \Imp Q \eqno(\exists E) $$ +$$ \List{\exists x. P(x); \Forall x. P(x)\imp Q} \Imp Q \eqno(\exists E) $$ $({\conj}I)$ translates into {\sc ascii} characters as \begin{ttbox} [| ?P; ?Q |] ==> ?P & ?Q @@ -188,7 +189,7 @@ For a final example, the rule $(\exists E)$ is rendered in {\sc ascii} as \begin{ttbox} -[| EX x.P(x); !!x. P(x) ==> Q |] ==> Q +[| EX x. P(x); !!x. P(x) ==> Q |] ==> Q \end{ttbox} @@ -251,8 +252,8 @@ session illustrates two formats for the display of theorems. Isabelle's top-level displays theorems as \ML{} values, enclosed in quotes. Printing commands like \texttt{prth} omit the quotes and the surrounding \texttt{val - \ldots :\ thm}. Ignoring their side-effects, the commands are identity -functions. + \ldots :\ thm}. Ignoring their side-effects, the printing commands are +identity functions. To contrast \texttt{RS} with \texttt{RSN}, we resolve \tdx{conjunct1}, which stands for~$(\conj E1)$, with~\tdx{mp}. @@ -309,7 +310,17 @@ exI; {\out val it = "?P(?x) ==> EX x. ?P(x)" : thm} refl RS exI; -{\out val it = "?a3(?x) =?= ?a2(?x) ==> EX x. ?a3(x) = ?a2(x)" : thm} +{\out val it = "EX x. ?a3(x) = ?a2(x)" [.] : thm} +\end{ttbox} +% +The mysterious symbol \texttt{[.]} indicates that the result is subject to +a meta-level hypothesis. We can make all such hypotheses visible by setting the +\ttindexbold{show_hyps} flag: +\begin{ttbox} +set show_hyps; +{\out val it = true : bool} +refl RS exI; +{\out val it = "EX x. ?a3(x) = ?a2(x)" ["?a3(?x) =?= ?a2(?x)"] : thm} \end{ttbox} \noindent @@ -348,7 +359,9 @@ unique unifier: \begin{ttbox} reflk RS exI; -{\out uncaught exception THM} +{\out uncaught exception} +{\out THM ("RSN: multiple unifiers", 1,} +{\out ["k = k", "?P(?x) ==> EX x. ?P(x)"])} \end{ttbox} Using \ttindex{RL} this time, we discover that there are four unifiers, and four resolvents: @@ -411,8 +424,7 @@ its many commands, most important are the following: \begin{ttdescription} \item[\ttindex{Goal} {\it formula}; ] -begins a new proof, where $theory$ is usually an \ML\ identifier -and the {\it formula\/} is written as an \ML\ string. +begins a new proof, where the {\it formula\/} is written as an \ML\ string. \item[\ttindex{by} {\it tactic}; ] applies the {\it tactic\/} to the current proof @@ -825,7 +837,7 @@ Since $\imp$ is nested to the right, $({\imp}I)$ can be applied twice; we use \texttt{REPEAT}: \begin{ttbox} -Goal "(ALL x.P(x) --> Q) --> (EX x.P(x)) --> Q"; +Goal "(ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q"; {\out Level 0} {\out (ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q} {\out 1. (ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q} @@ -878,11 +890,13 @@ \subsection{The classical reasoner} \index{classical reasoner} -Although Isabelle cannot compete with fully automatic theorem provers, it -provides enough automation to tackle substantial examples. The classical +Isabelle provides enough automation to tackle substantial examples. +The classical reasoner can be set up for any classical natural deduction logic; see \iflabelundefined{chap:classical}{the {\em Reference Manual\/}}% {Chap.\ts\ref{chap:classical}}. +It cannot compete with fully automatic theorem provers, but it is +competitive with tools found in other interactive provers. Rules are packaged into {\bf classical sets}. The classical reasoner provides several tactics, which apply rules using naive algorithms. diff -r 331ab35e81f2 -r 6580d374a509 doc-src/Intro/intro.tex --- a/doc-src/Intro/intro.tex Wed Aug 13 17:24:59 2003 +0200 +++ b/doc-src/Intro/intro.tex Wed Aug 13 17:44:01 2003 +0200 @@ -31,6 +31,16 @@ \pagestyle{empty} \begin{titlepage} \maketitle +\emph{Note}: this document is part of the earlier Isabelle documentation, +which is largely superseded by the Isabelle/HOL +\emph{Tutorial}~\cite{isa-tutorial}. It describes the old-style theory +syntax and shows how to conduct proofs using the +ML top level. This style of interaction is largely obsolete: +most Isabelle proofs are now written using the Isar +language and the Proof General interface. However, this paper contains valuable +information that is not available elsewhere. Its examples are based +on first-order logic rather than higher-order logic. + \thispagestyle{empty} \vfill {\small Copyright \copyright{} \number\year{} by Lawrence C. Paulson} @@ -58,12 +68,13 @@ several generic tools, such as simplifiers and classical theorem provers, which can be applied to object-logics. +Isabelle is a large system, but beginners can get by with a small +repertoire of commands and a basic knowledge of how Isabelle works. +The Isabelle/HOL \emph{Tutorial}~\cite{isa-tutorial} describes how to get started. Advanced Isabelle users will benefit from some +knowledge of Standard~\ML{}, because Isabelle is written in \ML{}; \index{ML} -Isabelle is a large system, but beginners can get by with a small -repertoire of commands and a basic knowledge of how Isabelle works. Some -knowledge of Standard~\ML{} is essential, because \ML{} is Isabelle's user -interface. Advanced Isabelle theorem proving can involve writing \ML{} -code, possibly with Isabelle's sources at hand. My book +if you are prepared to writing \ML{} +code, you can get Isabelle to do almost anything. My book on~\ML{}~\cite{paulson-ml2} covers much material connected with Isabelle, including a simple theorem prover. Users must be familiar with logic as used in computer science; there are many good @@ -83,8 +94,10 @@ treatment of quantifiers. The 1988 version added limited polymorphism and support for natural deduction. The 1989 version included a parser and pretty printer generator. The 1992 version introduced type classes, to -support many-sorted and higher-order logics. The current version provides -greater support for theories and is much faster. Isabelle is still under +support many-sorted and higher-order logics. The 1994 version introduced +greater support for theories. The most important recent change is the +introduction of the Isar proof language, thanks to Markus Wenzel. +Isabelle is still under development and will continue to change. \subsubsection*{Overview} @@ -101,7 +114,7 @@ \subsubsection*{Acknowledgements} Tobias Nipkow contributed most of the section on defining theories. -Stefan Berghofer and Sara Kalvala suggested improvements. +Stefan Berghofer, Sara Kalvala and Viktor Kuncak suggested improvements. Tobias Nipkow has made immense contributions to Isabelle, including the parser generator, type classes, and the simplifier. Carsten Clasohm and Markus