corrections by Viktor Kuncak and minor updating
authorpaulson
Wed Aug 13 17:44:01 2003 +0200 (2003-08-13)
changeset 141486580d374a509
parent 14147 331ab35e81f2
child 14149 fac076f0c71c
corrections by Viktor Kuncak and minor updating
doc-src/Intro/advanced.tex
doc-src/Intro/deriv.txt
doc-src/Intro/getting.tex
doc-src/Intro/intro.tex
     1.1 --- a/doc-src/Intro/advanced.tex	Wed Aug 13 17:24:59 2003 +0200
     1.2 +++ b/doc-src/Intro/advanced.tex	Wed Aug 13 17:44:01 2003 +0200
     1.3 @@ -48,14 +48,20 @@
     1.4  \item If one or more premises involves the meta-connectives $\Forall$ or
     1.5    $\Imp$, then the command sets the goal to be $\phi$ and returns a list
     1.6    consisting of the theorems ${\theta@i\;[\theta@i]}$, for $i=1$, \ldots,~$k$.
     1.7 -  These meta-assumptions are also recorded internally, allowing
     1.8 +  These meta-level assumptions are also recorded internally, allowing
     1.9    \texttt{result} (which is called by \texttt{qed}) to discharge them in the
    1.10    original order.
    1.11  \end{itemize}
    1.12  Rules that discharge assumptions or introduce eigenvariables have complex
    1.13 -premises, and the second case applies.
    1.14 +premises, and the second case applies.  In this section, many of the
    1.15 +theorems are subject to meta-level assumptions, so we make them visible by by setting the 
    1.16 +\ttindex{show_hyps} flag:
    1.17 +\begin{ttbox} 
    1.18 +set show_hyps;
    1.19 +{\out val it = true : bool}
    1.20 +\end{ttbox}
    1.21  
    1.22 -Let us derive $\conj$ elimination.  Until now, calling \texttt{Goal} has
    1.23 +Now, we are ready to derive $\conj$ elimination.  Until now, calling \texttt{Goal} has
    1.24  returned an empty list, which we have ignored.  In this example, the list
    1.25  contains the two premises of the rule, since one of them involves the $\Imp$
    1.26  connective.  We bind them to the \ML\ identifiers \texttt{major} and {\tt
    1.27 @@ -357,7 +363,9 @@
    1.28  \end{ttbox}
    1.29  where $id@1$, \ldots, $id@n$ are \ML{} identifiers and $rule@1$, \ldots,
    1.30  $rule@n$ are expressions of type~$prop$.  Each rule {\em must\/} be
    1.31 -enclosed in quotation marks.
    1.32 +enclosed in quotation marks.  Rules are simply axioms; they are 
    1.33 +called \emph{rules} because they are mainly used to specify the inference
    1.34 +rules when defining a new logic.
    1.35  
    1.36  \indexbold{definitions} The {\bf definition part} is similar, but with
    1.37  the keyword \texttt{defs} instead of \texttt{rules}.  {\bf Definitions} are
    1.38 @@ -368,10 +376,10 @@
    1.39  of the equation instead of abstracted on the right-hand side.
    1.40  
    1.41  Isabelle checks for common errors in definitions, such as extra
    1.42 -variables on the right-hand side, but currently does not a complete
    1.43 -test of well-formedness.  Thus determined users can write
    1.44 -non-conservative `definitions' by using mutual recursion, for example;
    1.45 -the consequences of such actions are their responsibility.
    1.46 +variables on the right-hand side and cyclic dependencies, that could
    1.47 +least to inconsistency.  It is still essential to take care:
    1.48 +theorems proved on the basis of incorrect definitions are useless,
    1.49 +your system can be consistent and yet still wrong.
    1.50  
    1.51  \index{examples!of theories} This example theory extends first-order
    1.52  logic by declaring and defining two constants, {\em nand} and {\em
    1.53 @@ -682,7 +690,8 @@
    1.54  \end{ttbox}
    1.55  Because $nat$ and $bool$ have class $arith$, we can use $0$, $1$ and $+$ at
    1.56  either type.  The type constraints in the axioms are vital.  Without
    1.57 -constraints, the $x$ in $1+x = x$ would have type $\alpha{::}arith$
    1.58 +constraints, the $x$ in $1+x = 1$ (axiom \texttt{or1l})
    1.59 +would have type $\alpha{::}arith$
    1.60  and the axiom would hold for any type of class $arith$.  This would
    1.61  collapse $nat$ to a trivial type:
    1.62  \[ Suc(1) = Suc(0+1) = Suc(0)+1 = 1+1 = 1! \]
    1.63 @@ -998,7 +1007,7 @@
    1.64  {\out          Suc(x) + m + n = Suc(x) + (m + n)}
    1.65  \end{ttbox}
    1.66  The inductive step requires rewriting by the equations for addition
    1.67 -together the induction hypothesis, which is also an equation.  The
    1.68 +and with the induction hypothesis, which is also an equation.  The
    1.69  tactic~\ttindex{Asm_simp_tac} rewrites using the implicit
    1.70  simplification set and any useful assumptions:
    1.71  \begin{ttbox}
    1.72 @@ -1219,7 +1228,7 @@
    1.73  {\out rev(?x, a : b : c : Nil)}
    1.74  {\out  1. rev(?x, a : b : c : Nil)}
    1.75  \ttbreak
    1.76 -by (DEPTH_FIRST (has_fewer_prems 1) (resolve_tac rules 1));
    1.77 +by prolog_tac;
    1.78  {\out Level 1}
    1.79  {\out rev(c : b : a : Nil, a : b : c : Nil)}
    1.80  {\out No subgoals!}
     2.1 --- a/doc-src/Intro/deriv.txt	Wed Aug 13 17:24:59 2003 +0200
     2.2 +++ b/doc-src/Intro/deriv.txt	Wed Aug 13 17:44:01 2003 +0200
     2.3 @@ -4,7 +4,7 @@
     2.4  print_depth 0;
     2.5  
     2.6  
     2.7 -val [major,minor] = goal Int_Rule.thy
     2.8 +val [major,minor] = goal IFOL.thy
     2.9      "[| P&Q;  [| P; Q |] ==> R |] ==> R";
    2.10  prth minor;
    2.11  by (resolve_tac [minor] 1);
     3.1 --- a/doc-src/Intro/getting.tex	Wed Aug 13 17:24:59 2003 +0200
     3.2 +++ b/doc-src/Intro/getting.tex	Wed Aug 13 17:44:01 2003 +0200
     3.3 @@ -1,12 +1,13 @@
     3.4  %% $Id$
     3.5 -\part{Getting Started with Isabelle}\label{chap:getting}
     3.6 -Let us consider how to perform simple proofs using Isabelle.  At
     3.7 -present, Isabelle's user interface is \ML.  Proofs are conducted by
     3.8 +\part{Using Isabelle from the ML Top-Level}\label{chap:getting}
     3.9 +
    3.10 +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.  
    3.11 +Proofs are conducted by
    3.12  applying certain \ML{} functions, which update a stored proof state.
    3.13 -Basically, all syntax must be expressed using plain {\sc ascii}
    3.14 -characters.  There are also mechanisms built into Isabelle that support
    3.15 +All syntax can be expressed using plain {\sc ascii}
    3.16 +characters, but Isabelle can support
    3.17  alternative syntaxes, for example using mathematical symbols from a
    3.18 -special screen font.  The meta-logic and major object-logics already
    3.19 +special screen font.  The meta-logic and main object-logics already
    3.20  provide such fancy output as an option.
    3.21  
    3.22  Object-logics are built upon Pure Isabelle, which implements the
    3.23 @@ -167,7 +168,7 @@
    3.24  \]
    3.25  To illustrate the notation, consider two axioms for first-order logic:
    3.26  $$ \List{P; Q} \Imp P\conj Q                 \eqno(\conj I) $$
    3.27 -$$ \List{\exists x.P(x); \Forall x. P(x)\imp Q} \Imp Q \eqno(\exists E) $$
    3.28 +$$ \List{\exists x. P(x); \Forall x. P(x)\imp Q} \Imp Q \eqno(\exists E) $$
    3.29  $({\conj}I)$ translates into {\sc ascii} characters as
    3.30  \begin{ttbox}
    3.31  [| ?P; ?Q |] ==> ?P & ?Q
    3.32 @@ -188,7 +189,7 @@
    3.33  
    3.34  For a final example, the rule $(\exists E)$ is rendered in {\sc ascii} as
    3.35  \begin{ttbox}
    3.36 -[| EX x.P(x);  !!x. P(x) ==> Q |] ==> Q
    3.37 +[| EX x. P(x);  !!x. P(x) ==> Q |] ==> Q
    3.38  \end{ttbox}
    3.39  
    3.40  
    3.41 @@ -251,8 +252,8 @@
    3.42  session illustrates two formats for the display of theorems.  Isabelle's
    3.43  top-level displays theorems as \ML{} values, enclosed in quotes.  Printing
    3.44  commands like \texttt{prth} omit the quotes and the surrounding \texttt{val
    3.45 -  \ldots :\ thm}.  Ignoring their side-effects, the commands are identity
    3.46 -functions.
    3.47 +  \ldots :\ thm}.  Ignoring their side-effects, the printing commands are 
    3.48 +identity functions.
    3.49  
    3.50  To contrast \texttt{RS} with \texttt{RSN}, we resolve
    3.51  \tdx{conjunct1}, which stands for~$(\conj E1)$, with~\tdx{mp}.
    3.52 @@ -309,7 +310,17 @@
    3.53  exI;
    3.54  {\out val it = "?P(?x) ==> EX x. ?P(x)" : thm}
    3.55  refl RS exI;
    3.56 -{\out val it = "?a3(?x) =?= ?a2(?x) ==> EX x. ?a3(x) = ?a2(x)" : thm}
    3.57 +{\out val it = "EX x. ?a3(x) = ?a2(x)"  [.] : thm}
    3.58 +\end{ttbox}
    3.59 +%
    3.60 +The mysterious symbol \texttt{[.]} indicates that the result is subject to 
    3.61 +a meta-level hypothesis. We can make all such hypotheses visible by setting the 
    3.62 +\ttindexbold{show_hyps} flag:
    3.63 +\begin{ttbox} 
    3.64 +set show_hyps;
    3.65 +{\out val it = true : bool}
    3.66 +refl RS exI;
    3.67 +{\out val it = "EX x. ?a3(x) = ?a2(x)"  ["?a3(?x) =?= ?a2(?x)"] : thm}
    3.68  \end{ttbox}
    3.69  
    3.70  \noindent
    3.71 @@ -348,7 +359,9 @@
    3.72  unique unifier:
    3.73  \begin{ttbox} 
    3.74  reflk RS exI;
    3.75 -{\out uncaught exception THM}
    3.76 +{\out uncaught exception}
    3.77 +{\out    THM ("RSN: multiple unifiers", 1,}
    3.78 +{\out         ["k = k", "?P(?x) ==> EX x. ?P(x)"])}
    3.79  \end{ttbox}
    3.80  Using \ttindex{RL} this time, we discover that there are four unifiers, and
    3.81  four resolvents:
    3.82 @@ -411,8 +424,7 @@
    3.83  its many commands, most important are the following:
    3.84  \begin{ttdescription}
    3.85  \item[\ttindex{Goal} {\it formula}; ] 
    3.86 -begins a new proof, where $theory$ is usually an \ML\ identifier
    3.87 -and the {\it formula\/} is written as an \ML\ string.
    3.88 +begins a new proof, where the {\it formula\/} is written as an \ML\ string.
    3.89  
    3.90  \item[\ttindex{by} {\it tactic}; ] 
    3.91  applies the {\it tactic\/} to the current proof
    3.92 @@ -825,7 +837,7 @@
    3.93  Since $\imp$ is nested to the right, $({\imp}I)$ can be applied twice; we
    3.94  use \texttt{REPEAT}:
    3.95  \begin{ttbox}
    3.96 -Goal "(ALL x.P(x) --> Q) --> (EX x.P(x)) --> Q";
    3.97 +Goal "(ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q";
    3.98  {\out Level 0}
    3.99  {\out (ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q}
   3.100  {\out  1. (ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q}
   3.101 @@ -878,11 +890,13 @@
   3.102  
   3.103  \subsection{The classical reasoner}
   3.104  \index{classical reasoner}
   3.105 -Although Isabelle cannot compete with fully automatic theorem provers, it
   3.106 -provides enough automation to tackle substantial examples.  The classical
   3.107 +Isabelle provides enough automation to tackle substantial examples.  
   3.108 +The classical
   3.109  reasoner can be set up for any classical natural deduction logic;
   3.110  see \iflabelundefined{chap:classical}{the {\em Reference Manual\/}}%
   3.111          {Chap.\ts\ref{chap:classical}}. 
   3.112 +It cannot compete with fully automatic theorem provers, but it is 
   3.113 +competitive with tools found in other interactive provers.
   3.114  
   3.115  Rules are packaged into {\bf classical sets}.  The classical reasoner
   3.116  provides several tactics, which apply rules using naive algorithms.
     4.1 --- a/doc-src/Intro/intro.tex	Wed Aug 13 17:24:59 2003 +0200
     4.2 +++ b/doc-src/Intro/intro.tex	Wed Aug 13 17:44:01 2003 +0200
     4.3 @@ -31,6 +31,16 @@
     4.4  \pagestyle{empty}
     4.5  \begin{titlepage}
     4.6  \maketitle 
     4.7 +\emph{Note}: this document is part of the earlier Isabelle documentation, 
     4.8 +which is largely superseded by the Isabelle/HOL
     4.9 +\emph{Tutorial}~\cite{isa-tutorial}. It describes the old-style theory 
    4.10 +syntax and shows how to conduct proofs using the 
    4.11 +ML top level. This style of interaction is largely obsolete:
    4.12 +most Isabelle proofs are now written using the Isar 
    4.13 +language and the Proof General interface. However, this paper contains valuable 
    4.14 +information that is not available elsewhere. Its examples are based 
    4.15 +on first-order logic rather than higher-order logic.
    4.16 +
    4.17  \thispagestyle{empty}
    4.18  \vfill
    4.19  {\small Copyright \copyright{} \number\year{} by Lawrence C. Paulson}
    4.20 @@ -58,12 +68,13 @@
    4.21  several generic tools, such as simplifiers and classical theorem provers,
    4.22  which can be applied to object-logics.
    4.23  
    4.24 +Isabelle is a large system, but beginners can get by with a small
    4.25 +repertoire of commands and a basic knowledge of how Isabelle works.  
    4.26 +The Isabelle/HOL \emph{Tutorial}~\cite{isa-tutorial} describes how to get started. Advanced Isabelle users will benefit from some
    4.27 +knowledge of Standard~\ML{}, because Isabelle is written in \ML{};
    4.28  \index{ML}
    4.29 -Isabelle is a large system, but beginners can get by with a small
    4.30 -repertoire of commands and a basic knowledge of how Isabelle works.  Some
    4.31 -knowledge of Standard~\ML{} is essential, because \ML{} is Isabelle's user
    4.32 -interface.  Advanced Isabelle theorem proving can involve writing \ML{}
    4.33 -code, possibly with Isabelle's sources at hand.  My book
    4.34 +if you are prepared to writing \ML{}
    4.35 +code, you can get Isabelle to do almost anything.  My book
    4.36  on~\ML{}~\cite{paulson-ml2} covers much material connected with Isabelle,
    4.37  including a simple theorem prover.  Users must be familiar with logic as
    4.38  used in computer science; there are many good
    4.39 @@ -83,8 +94,10 @@
    4.40  treatment of quantifiers.  The 1988 version added limited polymorphism and
    4.41  support for natural deduction.  The 1989 version included a parser and
    4.42  pretty printer generator.  The 1992 version introduced type classes, to
    4.43 -support many-sorted and higher-order logics.  The current version provides
    4.44 -greater support for theories and is much faster.  Isabelle is still under
    4.45 +support many-sorted and higher-order logics.  The 1994 version introduced
    4.46 +greater support for theories.  The most important recent change is the
    4.47 +introduction of the Isar proof language, thanks to Markus Wenzel.  
    4.48 +Isabelle is still under
    4.49  development and will continue to change.
    4.50  
    4.51  \subsubsection*{Overview} 
    4.52 @@ -101,7 +114,7 @@
    4.53  
    4.54  \subsubsection*{Acknowledgements} 
    4.55  Tobias Nipkow contributed most of the section on defining theories.
    4.56 -Stefan Berghofer and Sara Kalvala suggested improvements.
    4.57 +Stefan Berghofer, Sara Kalvala and Viktor Kuncak suggested improvements.
    4.58  
    4.59  Tobias Nipkow has made immense contributions to Isabelle, including the parser
    4.60  generator, type classes, and the simplifier.  Carsten Clasohm and Markus