doc-src/Intro/getting.tex
changeset 3103 98af809fee46
parent 1878 ac8e534b4834
child 3127 4cc2fe62f7c3
--- a/doc-src/Intro/getting.tex	Mon May 05 12:15:53 1997 +0200
+++ b/doc-src/Intro/getting.tex	Mon May 05 13:24:11 1997 +0200
@@ -1,19 +1,25 @@
 %% $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 applying certain
-\ML{} functions, which update a stored proof state.  All syntax must be
-expressed using {\sc ascii} characters.  Menu-driven graphical interfaces
-are under construction, but Isabelle users will always need to know some
-\ML, at least to use tacticals.
+Let us consider how to perform simple proofs using Isabelle.  At
+present, Isabelle's user interface is \ML.  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
+alternative syntaxes, for example using mathematical symbols from a
+special screen font. The meta-logic and major object-logics already
+provide such fancy output as an option.
 
-Object-logics are built upon Pure Isabelle, which implements the meta-logic
-and provides certain fundamental data structures: types, terms, signatures,
-theorems and theories, tactics and tacticals.  These data structures have
-the corresponding \ML{} types {\tt typ}, {\tt term}, {\tt Sign.sg}, {\tt thm},
-{\tt theory} and {\tt tactic}; tacticals have function types such as {\tt
-tactic->tactic}.  Isabelle users can operate on these data structures by
-writing \ML{} programs.
+%FIXME remove
+%Menu-driven graphical interfaces are under construction, but Isabelle
+%users will always need to know some \ML, at least to use tacticals.
+
+Object-logics are built upon Pure Isabelle, which implements the
+meta-logic and provides certain fundamental data structures: types,
+terms, signatures, theorems and theories, tactics and tacticals.
+These data structures have the corresponding \ML{} types {\tt typ},
+{\tt term}, {\tt Sign.sg}, {\tt thm}, {\tt theory} and {\tt tactic};
+tacticals have function types such as {\tt tactic->tactic}.  Isabelle
+users can operate on these data structures by writing \ML{} programs.
 
 \section{Forward proof}\label{sec:forward} \index{forward proof|(}
 This section describes the concrete syntax for types, terms and theorems,
@@ -65,10 +71,11 @@
 contains the `logical' types.  Sorts are lists of classes enclosed in
 braces~\} and \{; singleton sorts may be abbreviated by dropping the braces.
 
-\index{types!syntax of|bold}\index{sort constraints}
-Types are written with a syntax like \ML's.  The built-in type \tydx{prop}
-is the type of propositions.  Type variables can be constrained to particular
-classes or sorts, for example {\tt 'a::term} and {\tt ?'b::\{ord,arith\}}.
+\index{types!syntax of|bold}\index{sort constraints} Types are written
+with a syntax like \ML's.  The built-in type \tydx{prop} is the type
+of propositions.  Type variables can be constrained to particular
+classes or sorts, for example {\tt 'a::term} and {\tt ?'b::\ttlbrace
+  ord, arith\ttrbrace}.
 \[\dquotes
 \index{*:: symbol}\index{*=> symbol}
 \index{{}@{\tt\ttlbrace} symbol}\index{{}@{\tt\ttrbrace} symbol}
@@ -76,7 +83,7 @@
 \begin{array}{lll}
     \multicolumn{3}{c}{\hbox{ASCII Notation for Types}} \\ \hline
   \alpha "::" C              & \alpha :: C        & \hbox{class constraint} \\
-  \alpha "::" "\{" C@1 "," \ldots "," C@n "\}" &
+  \alpha "::" "\ttlbrace" C@1 "," \ldots "," C@n "\ttrbrace" &
      \alpha :: \{C@1,\dots,C@n\}             & \hbox{sort constraint} \\
   \sigma " => " \tau        & \sigma\To\tau & \hbox{function type} \\
   "[" \sigma@1 "," \ldots "," \sigma@n "] => " \tau &
@@ -118,7 +125,7 @@
   \List{\phi@1;\ldots;\phi@n} \Imp \psi & \hbox{nested implication} \\
   "!!" x "." \phi & \Forall x.\phi & \hbox{meta-quantification} \\
   "!!" x@1\ldots x@n "." \phi & 
-  \Forall x@1. \ldots \Forall x@n.\phi & \hbox{nested quantification}
+  \Forall x@1. \ldots x@n.\phi & \hbox{nested quantification}
   \end{array}
 \]
 Flex-flex constraints are meta-equalities arising from unification; they
@@ -138,8 +145,8 @@
 PROP ?psi ==> PROP ?theta 
 \end{ttbox}
 
-Symbols of object-logics also must be rendered into {\sc ascii}, typically
-as follows:
+Symbols of object-logics are typically rendered into {\sc ascii} as
+follows:
 \[ \begin{tabular}{l@{\quad}l@{\quad}l}
       \tt True          & $\top$        & true \\
       \tt False         & $\bot$        & false \\
@@ -154,9 +161,8 @@
 \]
 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) $$
-Using the {\tt [|\ldots|]} shorthand, $({\conj}I)$ translates into
-{\sc ascii} characters as
+$$ \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
 \end{ttbox}
@@ -406,14 +412,19 @@
 applies the {\it tactic\/} to the current proof
 state, raising an exception if the tactic fails.
 
-\item[\ttindex{undo}(); ] 
+\item[\ttindex{undo}(); ]
   reverts to the previous proof state.  Undo can be repeated but cannot be
   undone.  Do not omit the parentheses; typing {\tt\ \ undo;\ \ } merely
   causes \ML\ to echo the value of that function.
 
-\item[\ttindex{result}()] 
+\item[\ttindex{result}();]
 returns the theorem just proved, in a standard format.  It fails if
 unproved subgoals are left, etc.
+
+\item[\ttindex{qed} {\it name};] is the usual way of ending a proof.
+  It gets the theorem using {\tt result}, stores it in Isabelle's
+  theorem database and binds it to an \ML{} identifier.
+
 \end{ttdescription}
 The commands and tactics given above are cumbersome for interactive use.
 Although our examples will use the full commands, you may prefer Isabelle's
@@ -494,9 +505,9 @@
 {\out No subgoals!}
 \end{ttbox}
 Isabelle tells us that there are no longer any subgoals: the proof is
-complete.  Calling {\tt result} returns the theorem.
+complete.  Calling {\tt qed} stores the theorem.
 \begin{ttbox}
-val mythm = result(); 
+qed "mythm";
 {\out val mythm = "?P | ?P --> ?P" : thm} 
 \end{ttbox}
 Isabelle has replaced the free variable~{\tt P} by the scheme
@@ -664,7 +675,7 @@
 The reflexivity axiom does not unify with subgoal~1.
 \begin{ttbox}
 by (resolve_tac [refl] 1);
-{\out by: tactic returned no results}
+{\out by: tactic failed}
 \end{ttbox}
 There can be no proof of $\exists y.\forall x.x=y$ by the soundness of
 first-order logic.  I have elsewhere proved the faithfulness of Isabelle's
@@ -727,7 +738,7 @@
 proof by assumption will fail.
 \begin{ttbox}
 by (assume_tac 1);
-{\out by: tactic returned no results}
+{\out by: tactic failed}
 {\out uncaught exception ERROR}
 \end{ttbox}