# 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