doc-src/Intro/advanced.tex

 %% $Id$
 \part{Advanced Methods}
 Before continuing, it might be wise to try some of your own examples in
 Isabelle, reinforcing your knowledge of the basic functions.
 
-Look through {\em Isabelle's Object-Logics\/} and try proving some simple
-theorems.  You probably should begin with first-order logic ({\tt FOL}
-or~{\tt LK}).  Try working some of the examples provided, and others from
-the literature.  Set theory~({\tt ZF}) and Constructive Type Theory~({\tt
-  CTT}) form a richer world for mathematical reasoning and, again, many
-examples are in the literature.  Higher-order logic~({\tt HOL}) is
-Isabelle's most sophisticated logic because its types and functions are
-identified with those of the meta-logic.
+Look through {\em Isabelle's Object-Logics\/} and try proving some
+simple theorems.  You probably should begin with first-order logic
+({\tt FOL} or~{\tt LK}).  Try working some of the examples provided,
+and others from the literature.  Set theory~({\tt ZF}) and
+Constructive Type Theory~({\tt CTT}) form a richer world for
+mathematical reasoning and, again, many examples are in the
+literature.  Higher-order logic~({\tt HOL}) is Isabelle's most
+elaborate logic. Its types and functions are identified with those of
+the meta-logic.
 
 Choose a logic that you already understand.  Isabelle is a proof
 tool, not a teaching tool; if you do not know how to do a particular proof
 on paper, then you certainly will not be able to do it on the machine.
 Even experienced users plan large proofs on paper.

 \subsection{Deriving a rule using tactics and meta-level assumptions} 
 \label{deriving-example}
 \index{examples!of deriving rules}\index{assumptions!of main goal}
 
 The subgoal module supports the derivation of rules, as discussed in
-\S\ref{deriving}.  The \ttindex{goal} command, when supplied a goal of the
-form $\List{\theta@1; \ldots; \theta@k} \Imp \phi$, creates $\phi\Imp\phi$
-as the initial proof state 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 {\tt result} to discharge them
+\S\ref{deriving}.  The \ttindex{goal} command, when supplied a goal of
+the form $\List{\theta@1; \ldots; \theta@k} \Imp \phi$, creates
+$\phi\Imp\phi$ as the initial proof state 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 {\tt result} (which is called by {\tt qed}) to discharge them
 in the original order.
 
 Let us derive $\conj$ elimination using Isabelle.
 Until now, calling {\tt goal} has returned an empty list, which we have
 thrown away.  In this example, the list contains the two premises of the

 {\out Level 3}
 {\out R}
 {\out No subgoals!}
 \end{ttbox}
 Calling \ttindex{topthm} returns the current proof state as a theorem.
-Note that it contains assumptions.  Calling \ttindex{result} discharges the
-assumptions --- both occurrences of $P\conj Q$ are discharged as one ---
-and makes the variables schematic.
+Note that it contains assumptions.  Calling \ttindex{qed} discharges
+the assumptions --- both occurrences of $P\conj Q$ are discharged as
+one --- and makes the variables schematic.
 \begin{ttbox}
 topthm();
 {\out val it = "R  [P & Q, P & Q, [| P; Q |] ==> R]" : thm}
-val conjE = result();
+qed "conjE";
 {\out val conjE = "[| ?P & ?Q; [| ?P; ?Q |] ==> ?R |] ==> ?R" : thm}
 \end{ttbox}
 
 
 \subsection{Definitions and derived rules} \label{definitions}

 For example, the intuitionistic definition of negation given above may seem
 peculiar.  Using Isabelle, we shall derive pleasanter negation rules:
 \[  \infer[({\neg}I)]{\neg P}{\infer*{\bot}{[P]}}   \qquad
     \infer[({\neg}E)]{Q}{\neg P & P}  \]
 This requires proving the following meta-formulae:
-$$ (P\Imp\bot)    \Imp \neg P   \eqno(\neg I)$$
-$$ \List{\neg P; P} \Imp Q.       \eqno(\neg E)$$
+$$ (P\Imp\bot)    \Imp \neg P   \eqno(\neg I) $$
+$$ \List{\neg P; P} \Imp Q.       \eqno(\neg E) $$
 
 
 \subsection{Deriving the $\neg$ introduction rule}
 To derive $(\neg I)$, we may call {\tt goal} with the appropriate
 formula.  Again, {\tt goal} returns a list consisting of the rule's

 by (assume_tac 1);
 {\out Level 4}
 {\out ~P}
 {\out No subgoals!}
 \ttbreak
-val notI = result();
+qed "notI";
 {\out val notI = "(?P ==> False) ==> ~?P" : thm}
 \end{ttbox}
 \indexbold{*notI theorem}
 
 There is a simpler way of conducting this proof.  The \ttindex{goalw}

 \begin{ttbox}
 by (resolve_tac [minor] 1);
 {\out Level 4}
 {\out R}
 {\out No subgoals!}
-val notE = result();
+qed "notE";
 {\out val notE = "[| ~?P; ?P |] ==> ?R" : thm}
 \end{ttbox}
 \indexbold{*notE theorem}
 
 \medskip

 by (assume_tac 1);
 {\out Level 3}
 {\out !!P R. [| ~ P; P |] ==> R}
 {\out No subgoals!}
 \end{ttbox}
-Calling \ttindex{result} strips the meta-quantifiers, so the resulting
+Calling \ttindex{qed} strips the meta-quantifiers, so the resulting
 theorem is the same as before.
 \begin{ttbox}
-val notE = result();
+qed "notE";
 {\out val notE = "[| ~?P; ?P |] ==> ?R" : thm}
 \end{ttbox}
 Do not use the {\tt!!}\ trick if the premises contain meta-level
 connectives, because \ttindex{eresolve_tac} and \ttindex{assume_tac} would
 not be able to handle the resulting assumptions.  The trick is not suitable

 
 
 \section{Defining theories}\label{sec:defining-theories}
 \index{theories!defining|(}
 
-Isabelle makes no distinction between simple extensions of a logic --- like
-defining a type~$bool$ with constants~$true$ and~$false$ --- and defining
-an entire logic.  A theory definition has the form
+Isabelle makes no distinction between simple extensions of a logic ---
+like specifying a type~$bool$ with constants~$true$ and~$false$ ---
+and defining an entire logic.  A theory definition has a form like
 \begin{ttbox}
 \(T\) = \(S@1\) + \(\cdots\) + \(S@n\) +
 classes      {\it class declarations}
 default      {\it sort}
 types        {\it type declarations and synonyms}
-arities      {\it arity declarations}
+arities      {\it type arity declarations}
 consts       {\it constant declarations}
-translations {\it translation declarations}
-defs         {\it definitions}
+syntax       {\it syntactic constant declarations}
+translations {\it ast translation rules}
+defs         {\it meta-logical definitions}
 rules        {\it rule declarations}
 end
 ML           {\it ML code}
 \end{ttbox}
 This declares the theory $T$ to extend the existing theories
-$S@1$,~\ldots,~$S@n$.  It may declare new classes, types, arities
-(overloadings of existing types), constants and rules; it can specify the
-default sort for type variables.  A constant declaration can specify an
-associated concrete syntax.  The translations section specifies rewrite
-rules on abstract syntax trees, for defining notations and abbreviations.
-\index{*ML section}
-The {\tt ML} section contains code to perform arbitrary syntactic
-transformations.  The main declaration forms are discussed below.
-The full syntax can be found in \iflabelundefined{app:TheorySyntax}{the
-  appendix of the {\it Reference Manual}}{App.\ts\ref{app:TheorySyntax}}.
-
-All the declaration parts can be omitted or repeated and may appear in any
-order, except that the {\ML} section must be last.  In the simplest case, $T$
-is just the union of $S@1$,~\ldots,~$S@n$.  New theories always extend one or
-more other theories, inheriting their types, constants, syntax, etc.  The
-theory \thydx{Pure} contains nothing but Isabelle's meta-logic.
-
-Each theory definition must reside in a separate file, whose name is the
-theory's with {\tt.thy} appended.  For example, theory {\tt ListFn} resides
-on a file named {\tt ListFn.thy}.  Isabelle uses this convention to locate the
-file containing a given theory; \ttindexbold{use_thy} automatically loads a
-theory's parents before loading the theory itself.
-
-Calling \ttindexbold{use_thy}~{\tt"{\it T\/}"} reads a theory from the
-file {\it T}{\tt.thy}, writes the corresponding {\ML} code to the file
-{\tt.{\it T}.thy.ML}, reads the latter file, and deletes it if no errors
-occurred.  This declares the {\ML} structure~$T$, which contains a component
-{\tt thy} denoting the new theory, a component for each rule, and everything
-declared in {\it ML code}.
-
-Errors may arise during the translation to {\ML} (say, a misspelled keyword)
-or during creation of the new theory (say, a type error in a rule).  But if
-all goes well, {\tt use_thy} will finally read the file {\it T}{\tt.ML}, if
-it exists.  This file typically begins with the {\ML} declaration {\tt
-open}~$T$ and contains proofs that refer to the components of~$T$.
-
-When a theory file is modified, many theories may have to be reloaded.
-Isabelle records the modification times and dependencies of theory files.
-See 
+$S@1$,~\ldots,~$S@n$.  It may introduce new classes, types, arities
+(of existing types), constants and rules; it can specify the default
+sort for type variables.  A constant declaration can specify an
+associated concrete syntax.  The translations section specifies
+rewrite rules on abstract syntax trees, handling notations and
+abbreviations.  \index{*ML section} The {\tt ML} section may contain
+code to perform arbitrary syntactic transformations.  The main
+declaration forms are discussed below.  The full syntax can be found
+in \iflabelundefined{app:TheorySyntax}{an appendix of the {\it
+    Reference Manual}}{App.\ts\ref{app:TheorySyntax}}.  Also note that
+object-logics may add further theory sections, for example {\tt
+  typedef}, {\tt datatype} in \HOL.
+
+All the declaration parts can be omitted or repeated and may appear in
+any order, except that the {\ML} section must be last (after the {\tt
+  end} keyword).  In the simplest case, $T$ is just the union of
+$S@1$,~\ldots,~$S@n$.  New theories always extend one or more other
+theories, inheriting their types, constants, syntax, etc.  The theory
+\thydx{Pure} contains nothing but Isabelle's meta-logic. The variant
+\thydx{CPure} offers the more usual higher-order function application
+syntax $t\,u@1\ldots\,u@n$ instead of $t(u@1,\ldots,u@n)$.
+
+Each theory definition must reside in a separate file, whose name is
+the theory's with {\tt.thy} appended.  Calling
+\ttindexbold{use_thy}~{\tt"{\it T\/}"} reads the definition from {\it
+  T}{\tt.thy}, writes a corresponding file of {\ML} code {\tt.{\it
+    T}.thy.ML}, reads the latter file, and deletes it if no errors
+occurred.  This declares the {\ML} structure~$T$, which contains a
+component {\tt thy} denoting the new theory, a component for each
+rule, and everything declared in {\it ML code}.
+
+Errors may arise during the translation to {\ML} (say, a misspelled
+keyword) or during creation of the new theory (say, a type error in a
+rule).  But if all goes well, {\tt use_thy} will finally read the file
+{\it T}{\tt.ML} (if it exists).  This file typically contains proofs
+that refer to the components of~$T$. The structure is automatically
+opened, so its components may be referred to by unqualified names,
+e.g.\ just {\tt thy} instead of $T${\tt .thy}.
+
+\ttindexbold{use_thy} automatically loads a theory's parents before
+loading the theory itself.  When a theory file is modified, many
+theories may have to be reloaded.  Isabelle records the modification
+times and dependencies of theory files.  See
 \iflabelundefined{sec:reloading-theories}{the {\em Reference Manual\/}}%
                  {\S\ref{sec:reloading-theories}}
 for more details.
 
 

 \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.
 
-\indexbold{definitions} The {\bf definition part} is similar, but with the
-keyword {\tt defs} instead of {\tt rules}.  {\bf Definitions} are rules of the
-form $s \equiv t$, and should serve only as abbreviations. The simplest form
-of a definition is $f \equiv t$, where $f$ is a constant. Isabelle also
-allows a derived form where the arguments of~$f$ appear on the left:
-\begin{itemize}
-\item In uncurried syntax: $f(x@1,\dots,x@n) \equiv u$ (\FOL, \ZF, \dots)
-\item In curried syntax: $f~x@1~\dots~x@n \equiv u$ (\HOL, \HOLCF)
-\end{itemize}
-Isabelle checks for common errors in definitions, such as extra variables on
-the right-hand side.  Determined users can write non-conservative
-`definitions' by using mutual recursion, for example; the consequences of
-such actions are their responsibility.
-
-\index{examples!of theories} 
-This theory extends first-order logic by declaring and defining two constants,
-{\em nand} and {\em xor}:
+\indexbold{definitions} The {\bf definition part} is similar, but with
+the keyword {\tt defs} instead of {\tt rules}.  {\bf Definitions} are
+rules of the form $s \equiv t$, and should serve only as
+abbreviations. The simplest form of a definition is $f \equiv t$,
+where $f$ is a constant. Also allowed are $\eta$-equivalent forms,
+where the arguments of~$f$ appear applied on the left-hand side 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.
+
+\index{examples!of theories} This example theory extends first-order
+logic by declaring and defining two constants, {\em nand} and {\em
+  xor}:
 \begin{ttbox}
 Gate = FOL +
 consts  nand,xor :: [o,o] => o
 defs    nand_def "nand(P,Q) == ~(P & Q)"
         xor_def  "xor(P,Q)  == P & ~Q | ~P & Q"

 Multiple arity declarations may be abbreviated to a single line:
 \begin{ttbox}
 arities \(tycon@1\), \ldots, \(tycon@n\) :: \(arity\)
 \end{ttbox}
 
-\begin{warn}
-Arity declarations resemble constant declarations, but there are {\it no\/}
-quotation marks!  Types and rules must be quoted because the theory
-translator passes them verbatim to the {\ML} output file.
-\end{warn}
+%\begin{warn}
+%Arity declarations resemble constant declarations, but there are {\it no\/}
+%quotation marks!  Types and rules must be quoted because the theory
+%translator passes them verbatim to the {\ML} output file.
+%\end{warn}
 
 \subsection{Type synonyms}\indexbold{type synonyms}
 Isabelle supports {\bf type synonyms} ({\bf abbreviations}) which are similar
 to those found in \ML.  Such synonyms are defined in the type declaration part
 and are fairly self explanatory:

 types nat
       'a stream = nat => 'a
       signal    = nat stream
       'a list
 \end{ttbox}
-A synonym is merely an abbreviation for some existing type expression.  Hence
-synonyms may not be recursive!  Internally all synonyms are fully expanded.  As
-a consequence Isabelle output never contains synonyms.  Their main purpose is
-to improve the readability of theories.  Synonyms can be used just like any
-other type:
+A synonym is merely an abbreviation for some existing type expression.
+Hence synonyms may not be recursive!  Internally all synonyms are
+fully expanded.  As a consequence Isabelle output never contains
+synonyms.  Their main purpose is to improve the readability of theory
+definitions.  Synonyms can be used just like any other type:
 \begin{ttbox}
 consts and,or :: gate
        negate :: signal => signal
 \end{ttbox}
 

 \end{ttbox}
 This declares a constant $If$ of type $[o,o,o] \To o$ with concrete syntax {\tt
   if~$P$ then~$Q$ else~$R$} as well as {\tt If($P$,$Q$,$R$)}.  Underscores
 denote argument positions.  
 
-The declaration above does not allow the {\tt if}-{\tt then}-{\tt else}
-construct to be split across several lines, even if it is too long to fit
-on one line.  Pretty-printing information can be added to specify the
-layout of mixfix operators.  For details, see
+The declaration above does not allow the {\tt if}-{\tt then}-{\tt
+  else} construct to be printed split across several lines, even if it
+is too long to fit on one line.  Pretty-printing information can be
+added to specify the layout of mixfix operators.  For details, see
 \iflabelundefined{Defining-Logics}%
     {the {\it Reference Manual}, chapter `Defining Logics'}%
     {Chap.\ts\ref{Defining-Logics}}.
 
 Mixfix declarations can be annotated with priorities, just like

         snd     "snd(<a,b>) = b"
 end
 \end{ttbox}
 
 \begin{warn}
-The name of the type constructor is~{\tt *} and not {\tt op~*}, as it would
-be in the case of an infix constant.  Only infix type constructors can have
-symbolic names like~{\tt *}.  There is no general mixfix syntax for types.
+  The name of the type constructor is~{\tt *} and not {\tt op~*}, as
+  it would be in the case of an infix constant.  Only infix type
+  constructors can have symbolic names like~{\tt *}.  General mixfix
+  syntax for types may be introduced via appropriate {\tt syntax}
+  declarations.
 \end{warn}
 
 
 \subsection{Overloading}
 \index{overloading}\index{examples!of theories}

         add_def     "m+n == rec(m, n, \%x y. Suc(y))"
 end
 \end{ttbox}
 In axiom {\tt add_def}, recall that \verb|%| stands for~$\lambda$.
 Loading this theory file creates the \ML\ structure {\tt Nat}, which
-contains the theory and axioms.  Opening structure {\tt Nat} lets us write
-{\tt induct} instead of {\tt Nat.induct}, and so forth.
-\begin{ttbox}
-open Nat;
-\end{ttbox}
+contains the theory and axioms.
 
 \subsection{Proving some recursion equations}
 File {\tt FOL/ex/Nat.ML} contains proofs involving this theory of the
 natural numbers.  As a trivial example, let us derive recursion equations
 for \verb$+$.  Here is the zero case:

 \ttbreak
 by (resolve_tac [rec_0] 1);
 {\out Level 1}
 {\out 0 + n = n}
 {\out No subgoals!}
-val add_0 = result();
+qed "add_0";
 \end{ttbox}
 And here is the successor case:
 \begin{ttbox}
 goalw Nat.thy [add_def] "Suc(m)+n = Suc(m+n)";
 {\out Level 0}

 \ttbreak
 by (resolve_tac [rec_Suc] 1);
 {\out Level 1}
 {\out Suc(m) + n = Suc(m + n)}
 {\out No subgoals!}
-val add_Suc = result();
+qed "add_Suc";
 \end{ttbox}
 The induction rule raises some complications, which are discussed next.
 \index{theories!defining|)}