tuned;
authorwenzelm
Thu Sep 07 20:12:08 2006 +0200 (2006-09-07)
changeset 2049198ba42f19995
parent 20490 e502690952be
child 20492 c9bfc874488c
tuned;
doc-src/IsarImplementation/Thy/ML.thy
doc-src/IsarImplementation/Thy/document/ML.tex
doc-src/IsarImplementation/Thy/document/integration.tex
doc-src/IsarImplementation/Thy/document/logic.tex
doc-src/IsarImplementation/Thy/document/proof.tex
doc-src/IsarImplementation/Thy/integration.thy
doc-src/IsarImplementation/Thy/logic.thy
doc-src/IsarImplementation/Thy/proof.thy
doc-src/IsarImplementation/Thy/unused.thy
doc-src/IsarImplementation/style.sty
     1.1 --- a/doc-src/IsarImplementation/Thy/ML.thy	Thu Sep 07 15:16:51 2006 +0200
     1.2 +++ b/doc-src/IsarImplementation/Thy/ML.thy	Thu Sep 07 20:12:08 2006 +0200
     1.3 @@ -18,7 +18,7 @@
     1.4  
     1.5  chapter {* Cookbook *}
     1.6  
     1.7 -section {* Defining a method that depends on declarations in the context *}
     1.8 +section {* A method that depends on declarations in the context *}
     1.9  
    1.10  text FIXME
    1.11  
     2.1 --- a/doc-src/IsarImplementation/Thy/document/ML.tex	Thu Sep 07 15:16:51 2006 +0200
     2.2 +++ b/doc-src/IsarImplementation/Thy/document/ML.tex	Thu Sep 07 20:12:08 2006 +0200
     2.3 @@ -43,7 +43,7 @@
     2.4  }
     2.5  \isamarkuptrue%
     2.6  %
     2.7 -\isamarkupsection{Defining a method that depends on declarations in the context%
     2.8 +\isamarkupsection{A method that depends on declarations in the context%
     2.9  }
    2.10  \isamarkuptrue%
    2.11  %
     3.1 --- a/doc-src/IsarImplementation/Thy/document/integration.tex	Thu Sep 07 15:16:51 2006 +0200
     3.2 +++ b/doc-src/IsarImplementation/Thy/document/integration.tex	Thu Sep 07 20:12:08 2006 +0200
     3.3 @@ -510,15 +510,6 @@
     3.4  %
     3.5  \endisadelimmlref
     3.6  %
     3.7 -\isamarkupsection{Sessions and document preparation%
     3.8 -}
     3.9 -\isamarkuptrue%
    3.10 -%
    3.11 -\begin{isamarkuptext}%
    3.12 -FIXME%
    3.13 -\end{isamarkuptext}%
    3.14 -\isamarkuptrue%
    3.15 -%
    3.16  \isadelimtheory
    3.17  %
    3.18  \endisadelimtheory
     4.1 --- a/doc-src/IsarImplementation/Thy/document/logic.tex	Thu Sep 07 15:16:51 2006 +0200
     4.2 +++ b/doc-src/IsarImplementation/Thy/document/logic.tex	Thu Sep 07 20:12:08 2006 +0200
     4.3 @@ -28,15 +28,18 @@
     4.4    which has been introduced as a natural-deduction framework in
     4.5    \cite{paulson700}.  This is essentially the same logic as ``\isa{{\isasymlambda}HOL}'' in the more abstract framework of Pure Type Systems (PTS)
     4.6    \cite{Barendregt-Geuvers:2001}, although there are some key
     4.7 -  differences in the practical treatment of simple types.
     4.8 +  differences in the specific treatment of simple types in
     4.9 +  Isabelle/Pure.
    4.10  
    4.11    Following type-theoretic parlance, the Pure logic consists of three
    4.12    levels of \isa{{\isasymlambda}}-calculus with corresponding arrows: \isa{{\isasymRightarrow}} for syntactic function space (terms depending on terms), \isa{{\isasymAnd}} for universal quantification (proofs depending on terms), and
    4.13    \isa{{\isasymLongrightarrow}} for implication (proofs depending on proofs).
    4.14  
    4.15    Pure derivations are relative to a logical theory, which declares
    4.16 -  type constructors, term constants, and axioms.  Term constants and
    4.17 -  axioms support schematic polymorphism.%
    4.18 +  type constructors, term constants, and axioms.  Theory declarations
    4.19 +  support schematic polymorphism, which is strictly speaking outside
    4.20 +  the logic.\footnote{Incidently, this is the main logical reason, why
    4.21 +  the theory context \isa{{\isasymTheta}} is separate from the context \isa{{\isasymGamma}} of the core calculus.}%
    4.22  \end{isamarkuptext}%
    4.23  \isamarkuptrue%
    4.24  %
    4.25 @@ -50,38 +53,42 @@
    4.26  
    4.27    \medskip A \emph{type class} is an abstract syntactic entity
    4.28    declared in the theory context.  The \emph{subclass relation} \isa{c\isactrlisub {\isadigit{1}}\ {\isasymsubseteq}\ c\isactrlisub {\isadigit{2}}} is specified by stating an acyclic
    4.29 -  generating relation; the transitive closure maintained internally.
    4.30 +  generating relation; the transitive closure is maintained
    4.31 +  internally.  The resulting relation is an ordering: reflexive,
    4.32 +  transitive, and antisymmetric.
    4.33  
    4.34    A \emph{sort} is a list of type classes written as \isa{{\isacharbraceleft}c\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlisub m{\isacharbraceright}}, which represents symbolic
    4.35    intersection.  Notationally, the curly braces are omitted for
    4.36    singleton intersections, i.e.\ any class \isa{c} may be read as
    4.37    a sort \isa{{\isacharbraceleft}c{\isacharbraceright}}.  The ordering on type classes is extended to
    4.38 -  sorts in the canonical fashion: \isa{{\isacharbraceleft}c\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}\ c\isactrlisub m{\isacharbraceright}\ {\isasymsubseteq}\ {\isacharbraceleft}d\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ d\isactrlisub n{\isacharbraceright}} iff \isa{{\isasymforall}j{\isachardot}\ {\isasymexists}i{\isachardot}\ c\isactrlisub i\ {\isasymsubseteq}\ d\isactrlisub j}.  The empty intersection \isa{{\isacharbraceleft}{\isacharbraceright}} refers to the
    4.39 -  universal sort, which is the largest element wrt.\ the sort order.
    4.40 -  The intersections of all (i.e.\ finitely many) classes declared in
    4.41 -  the current theory are the minimal elements wrt.\ sort order.
    4.42 +  sorts according to the meaning of intersections: \isa{{\isacharbraceleft}c\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}\ c\isactrlisub m{\isacharbraceright}\ {\isasymsubseteq}\ {\isacharbraceleft}d\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ d\isactrlisub n{\isacharbraceright}} iff
    4.43 +  \isa{{\isasymforall}j{\isachardot}\ {\isasymexists}i{\isachardot}\ c\isactrlisub i\ {\isasymsubseteq}\ d\isactrlisub j}.  The empty intersection
    4.44 +  \isa{{\isacharbraceleft}{\isacharbraceright}} refers to the universal sort, which is the largest
    4.45 +  element wrt.\ the sort order.  The intersections of all (finitely
    4.46 +  many) classes declared in the current theory are the minimal
    4.47 +  elements wrt.\ the sort order.
    4.48  
    4.49 -  \medskip A \emph{fixed type variable} is pair of a basic name
    4.50 +  \medskip A \emph{fixed type variable} is a pair of a basic name
    4.51    (starting with \isa{{\isacharprime}} character) and a sort constraint.  For
    4.52    example, \isa{{\isacharparenleft}{\isacharprime}a{\isacharcomma}\ s{\isacharparenright}} which is usually printed as \isa{{\isasymalpha}\isactrlisub s}.  A \emph{schematic type variable} is a pair of an
    4.53 -  indexname and a sort constraint.  For example, \isa{{\isacharparenleft}{\isacharparenleft}{\isacharprime}a{\isacharcomma}\ {\isadigit{0}}{\isacharparenright}{\isacharcomma}\ s{\isacharparenright}} which is usually printed \isa{{\isacharquery}{\isasymalpha}\isactrlisub s}.
    4.54 +  indexname and a sort constraint.  For example, \isa{{\isacharparenleft}{\isacharparenleft}{\isacharprime}a{\isacharcomma}\ {\isadigit{0}}{\isacharparenright}{\isacharcomma}\ s{\isacharparenright}} which is usually printed as \isa{{\isacharquery}{\isasymalpha}\isactrlisub s}.
    4.55  
    4.56    Note that \emph{all} syntactic components contribute to the identity
    4.57 -  of a type variables, including the literal sort constraint.  The
    4.58 -  core logic handles type variables with the same name but different
    4.59 -  sorts as different, even though the outer layers of the system make
    4.60 -  it hard to produce anything like this.
    4.61 +  of type variables, including the literal sort constraint.  The core
    4.62 +  logic handles type variables with the same name but different sorts
    4.63 +  as different, although some outer layers of the system make it hard
    4.64 +  to produce anything like this.
    4.65  
    4.66 -  A \emph{type constructor} is an \isa{k}-ary type operator
    4.67 -  declared in the theory.
    4.68 +  A \emph{type constructor} is a \isa{k}-ary operator on types
    4.69 +  declared in the theory.  Type constructor application is usually
    4.70 +  written postfix.  For \isa{k\ {\isacharequal}\ {\isadigit{0}}} the argument tuple is omitted,
    4.71 +  e.g.\ \isa{prop} instead of \isa{{\isacharparenleft}{\isacharparenright}prop}.  For \isa{k\ {\isacharequal}\ {\isadigit{1}}} the parentheses are omitted, e.g.\ \isa{{\isasymalpha}\ list} instead of
    4.72 +  \isa{{\isacharparenleft}{\isasymalpha}{\isacharparenright}list}.  Further notation is provided for specific
    4.73 +  constructors, notably right-associative infix \isa{{\isasymalpha}\ {\isasymRightarrow}\ {\isasymbeta}}
    4.74 +  instead of \isa{{\isacharparenleft}{\isasymalpha}{\isacharcomma}\ {\isasymbeta}{\isacharparenright}fun} constructor.
    4.75    
    4.76    A \emph{type} is defined inductively over type variables and type
    4.77 -  constructors: \isa{{\isasymtau}\ {\isacharequal}\ {\isasymalpha}\isactrlisub s\ {\isacharbar}\ {\isacharquery}{\isasymalpha}\isactrlisub s\ {\isacharbar}\ {\isacharparenleft}{\isasymtau}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymtau}\isactrlsub k{\isacharparenright}c}.  Type constructor application is usually written
    4.78 -  postfix.  For \isa{k\ {\isacharequal}\ {\isadigit{0}}} the argument tuple is omitted, e.g.\
    4.79 -  \isa{prop} instead of \isa{{\isacharparenleft}{\isacharparenright}prop}.  For \isa{k\ {\isacharequal}\ {\isadigit{1}}} the
    4.80 -  parentheses are omitted, e.g.\ \isa{{\isasymtau}\ list} instead of \isa{{\isacharparenleft}{\isasymtau}{\isacharparenright}\ list}.  Further notation is provided for specific
    4.81 -  constructors, notably right-associative infix \isa{{\isasymtau}\isactrlisub {\isadigit{1}}\ {\isasymRightarrow}\ {\isasymtau}\isactrlisub {\isadigit{2}}} instead of \isa{{\isacharparenleft}{\isasymtau}\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymtau}\isactrlisub {\isadigit{2}}{\isacharparenright}fun}
    4.82 -  constructor.
    4.83 +  constructors as follows: \isa{{\isasymtau}\ {\isacharequal}\ {\isasymalpha}\isactrlisub s\ {\isacharbar}\ {\isacharquery}{\isasymalpha}\isactrlisub s\ {\isacharbar}\ {\isacharparenleft}{\isasymtau}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymtau}\isactrlsub k{\isacharparenright}c}.
    4.84  
    4.85    A \emph{type abbreviation} is a syntactic abbreviation of an
    4.86    arbitrary type expression of the theory.  Type abbreviations looks
    4.87 @@ -89,21 +96,23 @@
    4.88    core logic encounters them.
    4.89  
    4.90    A \emph{type arity} declares the image behavior of a type
    4.91 -  constructor wrt.\ the algebra of sorts: \isa{c\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}s\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ s\isactrlisub n{\isacharparenright}s} means that \isa{{\isacharparenleft}{\isasymtau}\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymtau}\isactrlisub k{\isacharparenright}c} is
    4.92 +  constructor wrt.\ the algebra of sorts: \isa{c\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}s\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ s\isactrlisub k{\isacharparenright}s} means that \isa{{\isacharparenleft}{\isasymtau}\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymtau}\isactrlisub k{\isacharparenright}c} is
    4.93    of sort \isa{s} if each argument type \isa{{\isasymtau}\isactrlisub i} is of
    4.94 -  sort \isa{s\isactrlisub i}.  The sort algebra is always maintained as
    4.95 -  \emph{coregular}, which means that type arities are consistent with
    4.96 -  the subclass relation: for each type constructor \isa{c} and
    4.97 -  classes \isa{c\isactrlisub {\isadigit{1}}\ {\isasymsubseteq}\ c\isactrlisub {\isadigit{2}}}, any arity \isa{c\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}\isactrlvec s\isactrlisub {\isadigit{1}}{\isacharparenright}c\isactrlisub {\isadigit{1}}} has a corresponding arity \isa{c\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}\isactrlvec s\isactrlisub {\isadigit{2}}{\isacharparenright}c\isactrlisub {\isadigit{2}}} where \isa{\isactrlvec s\isactrlisub {\isadigit{1}}\ {\isasymsubseteq}\ \isactrlvec s\isactrlisub {\isadigit{2}}} holds pointwise for all argument sorts.
    4.98 +  sort \isa{s\isactrlisub i}.  Arity declarations are implicitly
    4.99 +  completed, i.e.\ \isa{c\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}\isactrlvec s{\isacharparenright}c} entails \isa{c\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}\isactrlvec s{\isacharparenright}c{\isacharprime}} for any \isa{c{\isacharprime}\ {\isasymsupseteq}\ c}.
   4.100  
   4.101 -  The key property of the order-sorted algebra of types is that sort
   4.102 +  \medskip The sort algebra is always maintained as \emph{coregular},
   4.103 +  which means that type arities are consistent with the subclass
   4.104 +  relation: for each type constructor \isa{c} and classes \isa{c\isactrlisub {\isadigit{1}}\ {\isasymsubseteq}\ c\isactrlisub {\isadigit{2}}}, any arity \isa{c\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}\isactrlvec s\isactrlisub {\isadigit{1}}{\isacharparenright}c\isactrlisub {\isadigit{1}}} has a corresponding arity \isa{c\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}\isactrlvec s\isactrlisub {\isadigit{2}}{\isacharparenright}c\isactrlisub {\isadigit{2}}} where \isa{\isactrlvec s\isactrlisub {\isadigit{1}}\ {\isasymsubseteq}\ \isactrlvec s\isactrlisub {\isadigit{2}}} holds pointwise for all argument sorts.
   4.105 +
   4.106 +  The key property of a coregular order-sorted algebra is that sort
   4.107    constraints may be always fulfilled in a most general fashion: for
   4.108    each type constructor \isa{c} and sort \isa{s} there is a
   4.109 -  most general vector of argument sorts \isa{{\isacharparenleft}s\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ s\isactrlisub k{\isacharparenright}} such that \isa{{\isacharparenleft}{\isasymtau}\isactrlbsub s\isactrlisub {\isadigit{1}}\isactrlesub {\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymtau}\isactrlbsub s\isactrlisub k\isactrlesub {\isacharparenright}} for arbitrary \isa{{\isasymtau}\isactrlisub i} of
   4.110 -  sort \isa{s\isactrlisub i}.  This means the unification problem on
   4.111 -  the algebra of types has most general solutions (modulo renaming and
   4.112 -  equivalence of sorts).  As a consequence, type-inference is able to
   4.113 -  produce primary types.%
   4.114 +  most general vector of argument sorts \isa{{\isacharparenleft}s\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ s\isactrlisub k{\isacharparenright}} such that a type scheme \isa{{\isacharparenleft}{\isasymalpha}\isactrlbsub s\isactrlisub {\isadigit{1}}\isactrlesub {\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlbsub s\isactrlisub k\isactrlesub {\isacharparenright}c} is
   4.115 +  of sort \isa{s}.  Consequently, the unification problem on the
   4.116 +  algebra of types has most general solutions (modulo renaming and
   4.117 +  equivalence of sorts).  Moreover, the usual type-inference algorithm
   4.118 +  will produce primary types as expected \cite{nipkow-prehofer}.%
   4.119  \end{isamarkuptext}%
   4.120  \isamarkuptrue%
   4.121  %
   4.122 @@ -147,18 +156,18 @@
   4.123    tests the subsort relation \isa{s\isactrlisub {\isadigit{1}}\ {\isasymsubseteq}\ s\isactrlisub {\isadigit{2}}}.
   4.124  
   4.125    \item \verb|Sign.of_sort|~\isa{thy\ {\isacharparenleft}{\isasymtau}{\isacharcomma}\ s{\isacharparenright}} tests whether a type
   4.126 -  expression of of a given sort.
   4.127 +  is of a given sort.
   4.128  
   4.129    \item \verb|Sign.add_types|~\isa{{\isacharbrackleft}{\isacharparenleft}c{\isacharcomma}\ k{\isacharcomma}\ mx{\isacharparenright}{\isacharcomma}\ {\isasymdots}{\isacharbrackright}} declares new
   4.130 -  type constructors \isa{c} with \isa{k} arguments, and
   4.131 +  type constructors \isa{c} with \isa{k} arguments and
   4.132    optional mixfix syntax.
   4.133  
   4.134    \item \verb|Sign.add_tyabbrs_i|~\isa{{\isacharbrackleft}{\isacharparenleft}c{\isacharcomma}\ \isactrlvec {\isasymalpha}{\isacharcomma}\ {\isasymtau}{\isacharcomma}\ mx{\isacharparenright}{\isacharcomma}\ {\isasymdots}{\isacharbrackright}}
   4.135 -  defines type abbreviation \isa{{\isacharparenleft}\isactrlvec {\isasymalpha}{\isacharparenright}c} (with optional
   4.136 -  mixfix syntax) as \isa{{\isasymtau}}.
   4.137 +  defines a new type abbreviation \isa{{\isacharparenleft}\isactrlvec {\isasymalpha}{\isacharparenright}c\ {\isacharequal}\ {\isasymtau}} with
   4.138 +  optional mixfix syntax.
   4.139  
   4.140    \item \verb|Sign.primitive_class|~\isa{{\isacharparenleft}c{\isacharcomma}\ {\isacharbrackleft}c\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlisub n{\isacharbrackright}{\isacharparenright}} declares new class \isa{c} derived together with
   4.141 -  class relations \isa{c\ {\isasymsubseteq}\ c\isactrlisub i}.
   4.142 +  class relations \isa{c\ {\isasymsubseteq}\ c\isactrlisub i}, for \isa{i\ {\isacharequal}\ {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ n}.
   4.143  
   4.144    \item \verb|Sign.primitive_classrel|~\isa{{\isacharparenleft}c\isactrlisub {\isadigit{1}}{\isacharcomma}\ c\isactrlisub {\isadigit{2}}{\isacharparenright}} declares class relation \isa{c\isactrlisub {\isadigit{1}}\ {\isasymsubseteq}\ c\isactrlisub {\isadigit{2}}}.
   4.145  
   4.146 @@ -183,6 +192,13 @@
   4.147  \begin{isamarkuptext}%
   4.148  \glossary{Term}{FIXME}
   4.149  
   4.150 +  The language of terms is that of simply-typed \isa{{\isasymlambda}}-calculus
   4.151 +  with de-Bruijn indices for bound variables, and named free
   4.152 +  variables, and constants.  Terms with loose bound variables are
   4.153 +  usually considered malformed.  The types of variables and constants
   4.154 +  is stored explicitly at each occurrence in the term (which is a
   4.155 +  known performance issue).
   4.156 +
   4.157    FIXME de-Bruijn representation of lambda terms
   4.158  
   4.159    Term syntax provides explicit abstraction \isa{{\isasymlambda}x\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}{\isachardot}\ b{\isacharparenleft}x{\isacharparenright}}
   4.160 @@ -203,15 +219,6 @@
   4.161  \end{isamarkuptext}%
   4.162  \isamarkuptrue%
   4.163  %
   4.164 -\isamarkupsection{Proof terms%
   4.165 -}
   4.166 -\isamarkuptrue%
   4.167 -%
   4.168 -\begin{isamarkuptext}%
   4.169 -FIXME%
   4.170 -\end{isamarkuptext}%
   4.171 -\isamarkuptrue%
   4.172 -%
   4.173  \isamarkupsection{Theorems \label{sec:thms}%
   4.174  }
   4.175  \isamarkuptrue%
   4.176 @@ -267,22 +274,53 @@
   4.177  \end{isamarkuptext}%
   4.178  \isamarkuptrue%
   4.179  %
   4.180 -\isamarkupsubsection{Primitive inferences%
   4.181 +\isamarkupsection{Proof terms%
   4.182  }
   4.183  \isamarkuptrue%
   4.184  %
   4.185  \begin{isamarkuptext}%
   4.186 -FIXME%
   4.187 +FIXME !?%
   4.188  \end{isamarkuptext}%
   4.189  \isamarkuptrue%
   4.190  %
   4.191 -\isamarkupsubsection{Higher-order resolution%
   4.192 +\isamarkupsection{Rules \label{sec:rules}%
   4.193  }
   4.194  \isamarkuptrue%
   4.195  %
   4.196  \begin{isamarkuptext}%
   4.197  FIXME
   4.198  
   4.199 +  A \emph{rule} is any Pure theorem in HHF normal form; there is a
   4.200 +  separate calculus for rule composition, which is modeled after
   4.201 +  Gentzen's Natural Deduction \cite{Gentzen:1935}, but allows
   4.202 +  rules to be nested arbitrarily, similar to \cite{extensions91}.
   4.203 +
   4.204 +  Normally, all theorems accessible to the user are proper rules.
   4.205 +  Low-level inferences are occasional required internally, but the
   4.206 +  result should be always presented in canonical form.  The higher
   4.207 +  interfaces of Isabelle/Isar will always produce proper rules.  It is
   4.208 +  important to maintain this invariant in add-on applications!
   4.209 +
   4.210 +  There are two main principles of rule composition: \isa{resolution} (i.e.\ backchaining of rules) and \isa{by{\isacharminus}assumption} (i.e.\ closing a branch); both principles are
   4.211 +  combined in the variants of \isa{elim{\isacharminus}resosultion} and \isa{dest{\isacharminus}resolution}.  Raw \isa{composition} is occasionally
   4.212 +  useful as well, also it is strictly speaking outside of the proper
   4.213 +  rule calculus.
   4.214 +
   4.215 +  Rules are treated modulo general higher-order unification, which is
   4.216 +  unification modulo the equational theory of \isa{{\isasymalpha}{\isasymbeta}{\isasymeta}}-conversion
   4.217 +  on \isa{{\isasymlambda}}-terms.  Moreover, propositions are understood modulo
   4.218 +  the (derived) equivalence \isa{{\isacharparenleft}A\ {\isasymLongrightarrow}\ {\isacharparenleft}{\isasymAnd}x{\isachardot}\ B\ x{\isacharparenright}{\isacharparenright}\ {\isasymequiv}\ {\isacharparenleft}{\isasymAnd}x{\isachardot}\ A\ {\isasymLongrightarrow}\ B\ x{\isacharparenright}}.
   4.219 +
   4.220 +  This means that any operations within the rule calculus may be
   4.221 +  subject to spontaneous \isa{{\isasymalpha}{\isasymbeta}{\isasymeta}}-HHF conversions.  It is common
   4.222 +  practice not to contract or expand unnecessarily.  Some mechanisms
   4.223 +  prefer an one form, others the opposite, so there is a potential
   4.224 +  danger to produce some oscillation!
   4.225 +
   4.226 +  Only few operations really work \emph{modulo} HHF conversion, but
   4.227 +  expect a normal form: quantifiers \isa{{\isasymAnd}} before implications
   4.228 +  \isa{{\isasymLongrightarrow}} at each level of nesting.
   4.229 +
   4.230  \glossary{Hereditary Harrop Formula}{The set of propositions in HHF
   4.231  format is defined inductively as \isa{H\ {\isacharequal}\ {\isacharparenleft}{\isasymAnd}x\isactrlsup {\isacharasterisk}{\isachardot}\ H\isactrlsup {\isacharasterisk}\ {\isasymLongrightarrow}\ A{\isacharparenright}}, for variables \isa{x} and atomic propositions \isa{A}.
   4.232  Any proposition may be put into HHF form by normalizing with the rule
   4.233 @@ -295,15 +333,6 @@
   4.234  \end{isamarkuptext}%
   4.235  \isamarkuptrue%
   4.236  %
   4.237 -\isamarkupsubsection{Equational reasoning%
   4.238 -}
   4.239 -\isamarkuptrue%
   4.240 -%
   4.241 -\begin{isamarkuptext}%
   4.242 -FIXME%
   4.243 -\end{isamarkuptext}%
   4.244 -\isamarkuptrue%
   4.245 -%
   4.246  \isadelimtheory
   4.247  %
   4.248  \endisadelimtheory
     5.1 --- a/doc-src/IsarImplementation/Thy/document/proof.tex	Thu Sep 07 15:16:51 2006 +0200
     5.2 +++ b/doc-src/IsarImplementation/Thy/document/proof.tex	Thu Sep 07 20:12:08 2006 +0200
     5.3 @@ -217,7 +217,7 @@
     5.4    definition works by fixing \isa{x} and assuming \isa{x\ {\isasymequiv}\ t},
     5.5    with the following export rule to reverse the effect:
     5.6    \[
     5.7 -  \infer{\isa{{\isasymGamma}\ {\isacharbackslash}\ x\ {\isasymequiv}\ t\ {\isasymturnstile}\ B\ t}}{\isa{{\isasymGamma}\ {\isasymturnstile}\ B\ x}}
     5.8 +  \infer[(\isa{{\isasymequiv}{\isacharminus}expand})]{\isa{{\isasymGamma}\ {\isacharbackslash}\ x\ {\isasymequiv}\ t\ {\isasymturnstile}\ B\ t}}{\isa{{\isasymGamma}\ {\isasymturnstile}\ B\ x}}
     5.9    \]
    5.10    This works, because the assumption \isa{x\ {\isasymequiv}\ t} was introduced in
    5.11    a context with \isa{x} being fresh, so \isa{x} does not
    5.12 @@ -291,22 +291,30 @@
    5.13    references to free variables or assumptions not present in the proof
    5.14    context.
    5.15  
    5.16 -  \medskip The \isa{prove} operation provides an interface for
    5.17 -  structured backwards reasoning under program control, with some
    5.18 -  explicit sanity checks of the result.  The goal context can be
    5.19 -  augmented by additional fixed variables (cf.\
    5.20 -  \secref{sec:variables}) and assumptions (cf.\
    5.21 -  \secref{sec:assumptions}), which will be available as local facts
    5.22 -  during the proof and discharged into implications in the result.
    5.23 -  Type and term variables are generalized as usual, according to the
    5.24 -  context.
    5.25 +  \medskip The \isa{SUBPROOF} combinator allows to structure a
    5.26 +  tactical proof recursively by decomposing a selected sub-goal:
    5.27 +  \isa{{\isacharparenleft}{\isasymAnd}x{\isachardot}\ A{\isacharparenleft}x{\isacharparenright}\ {\isasymLongrightarrow}\ B{\isacharparenleft}x{\isacharparenright}{\isacharparenright}\ {\isasymLongrightarrow}\ {\isasymdots}} is turned into \isa{B{\isacharparenleft}x{\isacharparenright}\ {\isasymLongrightarrow}\ {\isasymdots}}
    5.28 +  after fixing \isa{x} and assuming \isa{A{\isacharparenleft}x{\isacharparenright}}.  This means
    5.29 +  the tactic needs to solve the conclusion, but may use the premise as
    5.30 +  a local fact, for locally fixed variables.
    5.31  
    5.32 -  The \isa{prove{\isacharunderscore}multi} operation handles several simultaneous
    5.33 -  claims within a single goal, by using Pure conjunction internally.
    5.34 +  The \isa{prove} operation provides an interface for structured
    5.35 +  backwards reasoning under program control, with some explicit sanity
    5.36 +  checks of the result.  The goal context can be augmented by
    5.37 +  additional fixed variables (cf.\ \secref{sec:variables}) and
    5.38 +  assumptions (cf.\ \secref{sec:assumptions}), which will be available
    5.39 +  as local facts during the proof and discharged into implications in
    5.40 +  the result.  Type and term variables are generalized as usual,
    5.41 +  according to the context.
    5.42  
    5.43 -  \medskip Tactical proofs may be structured recursively by
    5.44 -  decomposing a sub-goal: \isa{{\isacharparenleft}{\isasymAnd}x{\isachardot}\ A{\isacharparenleft}x{\isacharparenright}\ {\isasymLongrightarrow}\ B{\isacharparenleft}x{\isacharparenright}{\isacharparenright}\ {\isasymLongrightarrow}\ {\isasymdots}} is turned
    5.45 -  into \isa{B{\isacharparenleft}x{\isacharparenright}\ {\isasymLongrightarrow}\ {\isasymdots}} after fixing \isa{x} and assuming \isa{A{\isacharparenleft}x{\isacharparenright}}.%
    5.46 +  The \isa{obtain} operation produces results by eliminating
    5.47 +  existing facts by means of a given tactic.  This acts like a dual
    5.48 +  conclusion: the proof demonstrates that the context may be augmented
    5.49 +  by certain fixed variables and assumptions.  See also
    5.50 +  \cite{isabelle-isar-ref} for the user-level \isa{{\isasymOBTAIN}} and
    5.51 +  \isa{{\isasymGUESS}} elements.  Final results, which may not refer to
    5.52 +  the parameters in the conclusion, need to exported explicitly into
    5.53 +  the original context.%
    5.54  \end{isamarkuptext}%
    5.55  \isamarkuptrue%
    5.56  %
    5.57 @@ -318,31 +326,39 @@
    5.58  %
    5.59  \begin{isamarkuptext}%
    5.60  \begin{mldecls}
    5.61 +  \indexml{SUBPROOF}\verb|SUBPROOF: ({context: Proof.context, schematics: ctyp list * cterm list,|\isasep\isanewline%
    5.62 +\verb|    params: cterm list, asms: cterm list, concl: cterm,|\isasep\isanewline%
    5.63 +\verb|    prems: thm list} -> tactic) -> Proof.context -> int -> tactic| \\
    5.64    \indexml{Goal.prove}\verb|Goal.prove: Proof.context -> string list -> term list -> term ->|\isasep\isanewline%
    5.65  \verb|  ({prems: thm list, context: Proof.context} -> tactic) -> thm| \\
    5.66    \indexml{Goal.prove-multi}\verb|Goal.prove_multi: Proof.context -> string list -> term list -> term list ->|\isasep\isanewline%
    5.67  \verb|  ({prems: thm list, context: Proof.context} -> tactic) -> thm list| \\
    5.68 -  \indexml{SUBPROOF}\verb|SUBPROOF: ({context: Proof.context, schematics: ctyp list * cterm list,|\isasep\isanewline%
    5.69 -\verb|    params: cterm list, asms: cterm list, concl: cterm,|\isasep\isanewline%
    5.70 -\verb|    prems: thm list} -> tactic) -> Proof.context -> int -> tactic|
    5.71 +  \indexml{Obtain.result}\verb|Obtain.result: (Proof.context -> tactic) ->|\isasep\isanewline%
    5.72 +\verb|  thm list -> Proof.context -> (cterm list * thm list) * Proof.context|
    5.73    \end{mldecls}
    5.74  
    5.75    \begin{description}
    5.76  
    5.77 +  \item \verb|SUBPROOF|~\isa{tac} decomposes the structure of a
    5.78 +  particular sub-goal, producing an extended context and a reduced
    5.79 +  goal, which needs to be solved by the given tactic.  All schematic
    5.80 +  parameters of the goal are imported into the context as fixed ones,
    5.81 +  which may not be instantiated in the sub-proof.
    5.82 +
    5.83    \item \verb|Goal.prove|~\isa{ctxt\ xs\ As\ C\ tac} states goal \isa{C} in the context augmented by fixed variables \isa{xs} and
    5.84    assumptions \isa{As}, and applies tactic \isa{tac} to solve
    5.85    it.  The latter may depend on the local assumptions being presented
    5.86    as facts.  The result is in HHF normal form.
    5.87  
    5.88    \item \verb|Goal.prove_multi| is simular to \verb|Goal.prove|, but
    5.89 -  states several conclusions simultaneously.  \verb|Tactic.conjunction_tac| may be used to split these into individual
    5.90 -  subgoals before commencing the actual proof.
    5.91 +  states several conclusions simultaneously.  The goal is encoded by
    5.92 +  means of Pure conjunction; \verb|Tactic.conjunction_tac| will turn
    5.93 +  this into a collection of individual subgoals.
    5.94  
    5.95 -  \item \verb|SUBPROOF|~\isa{tac} decomposes the structure of a
    5.96 -  particular sub-goal, producing an extended context and a reduced
    5.97 -  goal, which needs to be solved by the given tactic.  All schematic
    5.98 -  parameters of the goal are imported into the context as fixed ones,
    5.99 -  which may not be instantiated in the sub-proof.
   5.100 +  \item \verb|Obtain.result|~\isa{tac\ thms\ ctxt} eliminates the
   5.101 +  given facts using a tactic, which results in additional fixed
   5.102 +  variables and assumptions in the context.  Final results need to be
   5.103 +  exported explicitly.
   5.104  
   5.105    \end{description}%
   5.106  \end{isamarkuptext}%
     6.1 --- a/doc-src/IsarImplementation/Thy/integration.thy	Thu Sep 07 15:16:51 2006 +0200
     6.2 +++ b/doc-src/IsarImplementation/Thy/integration.thy	Thu Sep 07 20:12:08 2006 +0200
     6.3 @@ -432,9 +432,4 @@
     6.4    \end{description}
     6.5  *}
     6.6  
     6.7 -
     6.8 -section {* Sessions and document preparation *}
     6.9 -
    6.10 -text FIXME
    6.11 -
    6.12  end
     7.1 --- a/doc-src/IsarImplementation/Thy/logic.thy	Thu Sep 07 15:16:51 2006 +0200
     7.2 +++ b/doc-src/IsarImplementation/Thy/logic.thy	Thu Sep 07 20:12:08 2006 +0200
     7.3 @@ -11,7 +11,8 @@
     7.4    \cite{paulson700}.  This is essentially the same logic as ``@{text
     7.5    "\<lambda>HOL"}'' in the more abstract framework of Pure Type Systems (PTS)
     7.6    \cite{Barendregt-Geuvers:2001}, although there are some key
     7.7 -  differences in the practical treatment of simple types.
     7.8 +  differences in the specific treatment of simple types in
     7.9 +  Isabelle/Pure.
    7.10  
    7.11    Following type-theoretic parlance, the Pure logic consists of three
    7.12    levels of @{text "\<lambda>"}-calculus with corresponding arrows: @{text
    7.13 @@ -20,8 +21,11 @@
    7.14    @{text "\<Longrightarrow>"} for implication (proofs depending on proofs).
    7.15  
    7.16    Pure derivations are relative to a logical theory, which declares
    7.17 -  type constructors, term constants, and axioms.  Term constants and
    7.18 -  axioms support schematic polymorphism.
    7.19 +  type constructors, term constants, and axioms.  Theory declarations
    7.20 +  support schematic polymorphism, which is strictly speaking outside
    7.21 +  the logic.\footnote{Incidently, this is the main logical reason, why
    7.22 +  the theory context @{text "\<Theta>"} is separate from the context @{text
    7.23 +  "\<Gamma>"} of the core calculus.}
    7.24  *}
    7.25  
    7.26  
    7.27 @@ -34,46 +38,48 @@
    7.28    \medskip A \emph{type class} is an abstract syntactic entity
    7.29    declared in the theory context.  The \emph{subclass relation} @{text
    7.30    "c\<^isub>1 \<subseteq> c\<^isub>2"} is specified by stating an acyclic
    7.31 -  generating relation; the transitive closure maintained internally.
    7.32 +  generating relation; the transitive closure is maintained
    7.33 +  internally.  The resulting relation is an ordering: reflexive,
    7.34 +  transitive, and antisymmetric.
    7.35  
    7.36    A \emph{sort} is a list of type classes written as @{text
    7.37    "{c\<^isub>1, \<dots>, c\<^isub>m}"}, which represents symbolic
    7.38    intersection.  Notationally, the curly braces are omitted for
    7.39    singleton intersections, i.e.\ any class @{text "c"} may be read as
    7.40    a sort @{text "{c}"}.  The ordering on type classes is extended to
    7.41 -  sorts in the canonical fashion: @{text "{c\<^isub>1, \<dots> c\<^isub>m} \<subseteq>
    7.42 -  {d\<^isub>1, \<dots>, d\<^isub>n}"} iff @{text "\<forall>j. \<exists>i. c\<^isub>i \<subseteq>
    7.43 -  d\<^isub>j"}.  The empty intersection @{text "{}"} refers to the
    7.44 -  universal sort, which is the largest element wrt.\ the sort order.
    7.45 -  The intersections of all (i.e.\ finitely many) classes declared in
    7.46 -  the current theory are the minimal elements wrt.\ sort order.
    7.47 +  sorts according to the meaning of intersections: @{text
    7.48 +  "{c\<^isub>1, \<dots> c\<^isub>m} \<subseteq> {d\<^isub>1, \<dots>, d\<^isub>n}"} iff
    7.49 +  @{text "\<forall>j. \<exists>i. c\<^isub>i \<subseteq> d\<^isub>j"}.  The empty intersection
    7.50 +  @{text "{}"} refers to the universal sort, which is the largest
    7.51 +  element wrt.\ the sort order.  The intersections of all (finitely
    7.52 +  many) classes declared in the current theory are the minimal
    7.53 +  elements wrt.\ the sort order.
    7.54  
    7.55 -  \medskip A \emph{fixed type variable} is pair of a basic name
    7.56 +  \medskip A \emph{fixed type variable} is a pair of a basic name
    7.57    (starting with @{text "'"} character) and a sort constraint.  For
    7.58    example, @{text "('a, s)"} which is usually printed as @{text
    7.59    "\<alpha>\<^isub>s"}.  A \emph{schematic type variable} is a pair of an
    7.60    indexname and a sort constraint.  For example, @{text "(('a, 0),
    7.61 -  s)"} which is usually printed @{text "?\<alpha>\<^isub>s"}.
    7.62 +  s)"} which is usually printed as @{text "?\<alpha>\<^isub>s"}.
    7.63  
    7.64    Note that \emph{all} syntactic components contribute to the identity
    7.65 -  of a type variables, including the literal sort constraint.  The
    7.66 -  core logic handles type variables with the same name but different
    7.67 -  sorts as different, even though the outer layers of the system make
    7.68 -  it hard to produce anything like this.
    7.69 +  of type variables, including the literal sort constraint.  The core
    7.70 +  logic handles type variables with the same name but different sorts
    7.71 +  as different, although some outer layers of the system make it hard
    7.72 +  to produce anything like this.
    7.73  
    7.74 -  A \emph{type constructor} is an @{text "k"}-ary type operator
    7.75 -  declared in the theory.
    7.76 +  A \emph{type constructor} is a @{text "k"}-ary operator on types
    7.77 +  declared in the theory.  Type constructor application is usually
    7.78 +  written postfix.  For @{text "k = 0"} the argument tuple is omitted,
    7.79 +  e.g.\ @{text "prop"} instead of @{text "()prop"}.  For @{text "k =
    7.80 +  1"} the parentheses are omitted, e.g.\ @{text "\<alpha> list"} instead of
    7.81 +  @{text "(\<alpha>)list"}.  Further notation is provided for specific
    7.82 +  constructors, notably right-associative infix @{text "\<alpha> \<Rightarrow> \<beta>"}
    7.83 +  instead of @{text "(\<alpha>, \<beta>)fun"} constructor.
    7.84    
    7.85    A \emph{type} is defined inductively over type variables and type
    7.86 -  constructors: @{text "\<tau> = \<alpha>\<^isub>s | ?\<alpha>\<^isub>s | (\<tau>\<^sub>1, \<dots>,
    7.87 -  \<tau>\<^sub>k)c"}.  Type constructor application is usually written
    7.88 -  postfix.  For @{text "k = 0"} the argument tuple is omitted, e.g.\
    7.89 -  @{text "prop"} instead of @{text "()prop"}.  For @{text "k = 1"} the
    7.90 -  parentheses are omitted, e.g.\ @{text "\<tau> list"} instead of @{text
    7.91 -  "(\<tau>) list"}.  Further notation is provided for specific
    7.92 -  constructors, notably right-associative infix @{text "\<tau>\<^isub>1 \<Rightarrow>
    7.93 -  \<tau>\<^isub>2"} instead of @{text "(\<tau>\<^isub>1, \<tau>\<^isub>2)fun"}
    7.94 -  constructor.
    7.95 +  constructors as follows: @{text "\<tau> = \<alpha>\<^isub>s | ?\<alpha>\<^isub>s |
    7.96 +  (\<tau>\<^sub>1, \<dots>, \<tau>\<^sub>k)c"}.
    7.97  
    7.98    A \emph{type abbreviation} is a syntactic abbreviation of an
    7.99    arbitrary type expression of the theory.  Type abbreviations looks
   7.100 @@ -82,26 +88,30 @@
   7.101  
   7.102    A \emph{type arity} declares the image behavior of a type
   7.103    constructor wrt.\ the algebra of sorts: @{text "c :: (s\<^isub>1, \<dots>,
   7.104 -  s\<^isub>n)s"} means that @{text "(\<tau>\<^isub>1, \<dots>, \<tau>\<^isub>k)c"} is
   7.105 +  s\<^isub>k)s"} means that @{text "(\<tau>\<^isub>1, \<dots>, \<tau>\<^isub>k)c"} is
   7.106    of sort @{text "s"} if each argument type @{text "\<tau>\<^isub>i"} is of
   7.107 -  sort @{text "s\<^isub>i"}.  The sort algebra is always maintained as
   7.108 -  \emph{coregular}, which means that type arities are consistent with
   7.109 -  the subclass relation: for each type constructor @{text "c"} and
   7.110 -  classes @{text "c\<^isub>1 \<subseteq> c\<^isub>2"}, any arity @{text "c ::
   7.111 +  sort @{text "s\<^isub>i"}.  Arity declarations are implicitly
   7.112 +  completed, i.e.\ @{text "c :: (\<^vec>s)c"} entails @{text "c ::
   7.113 +  (\<^vec>s)c'"} for any @{text "c' \<supseteq> c"}.
   7.114 +
   7.115 +  \medskip The sort algebra is always maintained as \emph{coregular},
   7.116 +  which means that type arities are consistent with the subclass
   7.117 +  relation: for each type constructor @{text "c"} and classes @{text
   7.118 +  "c\<^isub>1 \<subseteq> c\<^isub>2"}, any arity @{text "c ::
   7.119    (\<^vec>s\<^isub>1)c\<^isub>1"} has a corresponding arity @{text "c
   7.120    :: (\<^vec>s\<^isub>2)c\<^isub>2"} where @{text "\<^vec>s\<^isub>1 \<subseteq>
   7.121    \<^vec>s\<^isub>2"} holds pointwise for all argument sorts.
   7.122  
   7.123 -  The key property of the order-sorted algebra of types is that sort
   7.124 +  The key property of a coregular order-sorted algebra is that sort
   7.125    constraints may be always fulfilled in a most general fashion: for
   7.126    each type constructor @{text "c"} and sort @{text "s"} there is a
   7.127    most general vector of argument sorts @{text "(s\<^isub>1, \<dots>,
   7.128 -  s\<^isub>k)"} such that @{text "(\<tau>\<^bsub>s\<^isub>1\<^esub>, \<dots>,
   7.129 -  \<tau>\<^bsub>s\<^isub>k\<^esub>)"} for arbitrary @{text "\<tau>\<^isub>i"} of
   7.130 -  sort @{text "s\<^isub>i"}.  This means the unification problem on
   7.131 -  the algebra of types has most general solutions (modulo renaming and
   7.132 -  equivalence of sorts).  As a consequence, type-inference is able to
   7.133 -  produce primary types.
   7.134 +  s\<^isub>k)"} such that a type scheme @{text
   7.135 +  "(\<alpha>\<^bsub>s\<^isub>1\<^esub>, \<dots>, \<alpha>\<^bsub>s\<^isub>k\<^esub>)c"} is
   7.136 +  of sort @{text "s"}.  Consequently, the unification problem on the
   7.137 +  algebra of types has most general solutions (modulo renaming and
   7.138 +  equivalence of sorts).  Moreover, the usual type-inference algorithm
   7.139 +  will produce primary types as expected \cite{nipkow-prehofer}.
   7.140  *}
   7.141  
   7.142  text %mlref {*
   7.143 @@ -139,19 +149,19 @@
   7.144    tests the subsort relation @{text "s\<^isub>1 \<subseteq> s\<^isub>2"}.
   7.145  
   7.146    \item @{ML Sign.of_sort}~@{text "thy (\<tau>, s)"} tests whether a type
   7.147 -  expression of of a given sort.
   7.148 +  is of a given sort.
   7.149  
   7.150    \item @{ML Sign.add_types}~@{text "[(c, k, mx), \<dots>]"} declares new
   7.151 -  type constructors @{text "c"} with @{text "k"} arguments, and
   7.152 +  type constructors @{text "c"} with @{text "k"} arguments and
   7.153    optional mixfix syntax.
   7.154  
   7.155    \item @{ML Sign.add_tyabbrs_i}~@{text "[(c, \<^vec>\<alpha>, \<tau>, mx), \<dots>]"}
   7.156 -  defines type abbreviation @{text "(\<^vec>\<alpha>)c"} (with optional
   7.157 -  mixfix syntax) as @{text "\<tau>"}.
   7.158 +  defines a new type abbreviation @{text "(\<^vec>\<alpha>)c = \<tau>"} with
   7.159 +  optional mixfix syntax.
   7.160  
   7.161    \item @{ML Sign.primitive_class}~@{text "(c, [c\<^isub>1, \<dots>,
   7.162    c\<^isub>n])"} declares new class @{text "c"} derived together with
   7.163 -  class relations @{text "c \<subseteq> c\<^isub>i"}.
   7.164 +  class relations @{text "c \<subseteq> c\<^isub>i"}, for @{text "i = 1, \<dots>, n"}.
   7.165  
   7.166    \item @{ML Sign.primitive_classrel}~@{text "(c\<^isub>1,
   7.167    c\<^isub>2)"} declares class relation @{text "c\<^isub>1 \<subseteq>
   7.168 @@ -170,6 +180,13 @@
   7.169  text {*
   7.170    \glossary{Term}{FIXME}
   7.171  
   7.172 +  The language of terms is that of simply-typed @{text "\<lambda>"}-calculus
   7.173 +  with de-Bruijn indices for bound variables, and named free
   7.174 +  variables, and constants.  Terms with loose bound variables are
   7.175 +  usually considered malformed.  The types of variables and constants
   7.176 +  is stored explicitly at each occurrence in the term (which is a
   7.177 +  known performance issue).
   7.178 +
   7.179    FIXME de-Bruijn representation of lambda terms
   7.180  
   7.181    Term syntax provides explicit abstraction @{text "\<lambda>x :: \<alpha>. b(x)"}
   7.182 @@ -193,13 +210,6 @@
   7.183  *}
   7.184  
   7.185  
   7.186 -section {* Proof terms *}
   7.187 -
   7.188 -text {*
   7.189 -  FIXME
   7.190 -*}
   7.191 -
   7.192 -
   7.193  section {* Theorems \label{sec:thms} *}
   7.194  
   7.195  text {*
   7.196 @@ -258,17 +268,54 @@
   7.197  
   7.198  *}
   7.199  
   7.200 -subsection {* Primitive inferences *}
   7.201 +
   7.202 +section {* Proof terms *}
   7.203  
   7.204 -text FIXME
   7.205 +text {*
   7.206 +  FIXME !?
   7.207 +*}
   7.208  
   7.209  
   7.210 -subsection {* Higher-order resolution *}
   7.211 +section {* Rules \label{sec:rules} *}
   7.212  
   7.213  text {*
   7.214  
   7.215  FIXME
   7.216  
   7.217 +  A \emph{rule} is any Pure theorem in HHF normal form; there is a
   7.218 +  separate calculus for rule composition, which is modeled after
   7.219 +  Gentzen's Natural Deduction \cite{Gentzen:1935}, but allows
   7.220 +  rules to be nested arbitrarily, similar to \cite{extensions91}.
   7.221 +
   7.222 +  Normally, all theorems accessible to the user are proper rules.
   7.223 +  Low-level inferences are occasional required internally, but the
   7.224 +  result should be always presented in canonical form.  The higher
   7.225 +  interfaces of Isabelle/Isar will always produce proper rules.  It is
   7.226 +  important to maintain this invariant in add-on applications!
   7.227 +
   7.228 +  There are two main principles of rule composition: @{text
   7.229 +  "resolution"} (i.e.\ backchaining of rules) and @{text
   7.230 +  "by-assumption"} (i.e.\ closing a branch); both principles are
   7.231 +  combined in the variants of @{text "elim-resosultion"} and @{text
   7.232 +  "dest-resolution"}.  Raw @{text "composition"} is occasionally
   7.233 +  useful as well, also it is strictly speaking outside of the proper
   7.234 +  rule calculus.
   7.235 +
   7.236 +  Rules are treated modulo general higher-order unification, which is
   7.237 +  unification modulo the equational theory of @{text "\<alpha>\<beta>\<eta>"}-conversion
   7.238 +  on @{text "\<lambda>"}-terms.  Moreover, propositions are understood modulo
   7.239 +  the (derived) equivalence @{text "(A \<Longrightarrow> (\<And>x. B x)) \<equiv> (\<And>x. A \<Longrightarrow> B x)"}.
   7.240 +
   7.241 +  This means that any operations within the rule calculus may be
   7.242 +  subject to spontaneous @{text "\<alpha>\<beta>\<eta>"}-HHF conversions.  It is common
   7.243 +  practice not to contract or expand unnecessarily.  Some mechanisms
   7.244 +  prefer an one form, others the opposite, so there is a potential
   7.245 +  danger to produce some oscillation!
   7.246 +
   7.247 +  Only few operations really work \emph{modulo} HHF conversion, but
   7.248 +  expect a normal form: quantifiers @{text "\<And>"} before implications
   7.249 +  @{text "\<Longrightarrow>"} at each level of nesting.
   7.250 +
   7.251  \glossary{Hereditary Harrop Formula}{The set of propositions in HHF
   7.252  format is defined inductively as @{text "H = (\<And>x\<^sup>*. H\<^sup>* \<Longrightarrow>
   7.253  A)"}, for variables @{text "x"} and atomic propositions @{text "A"}.
   7.254 @@ -282,9 +329,4 @@
   7.255  
   7.256  *}
   7.257  
   7.258 -subsection {* Equational reasoning *}
   7.259 -
   7.260 -text FIXME
   7.261 -
   7.262 -
   7.263  end
     8.1 --- a/doc-src/IsarImplementation/Thy/proof.thy	Thu Sep 07 15:16:51 2006 +0200
     8.2 +++ b/doc-src/IsarImplementation/Thy/proof.thy	Thu Sep 07 20:12:08 2006 +0200
     8.3 @@ -196,7 +196,7 @@
     8.4    definition works by fixing @{text "x"} and assuming @{text "x \<equiv> t"},
     8.5    with the following export rule to reverse the effect:
     8.6    \[
     8.7 -  \infer{@{text "\<Gamma> \\ x \<equiv> t \<turnstile> B t"}}{@{text "\<Gamma> \<turnstile> B x"}}
     8.8 +  \infer[(@{text "\<equiv>-expand"})]{@{text "\<Gamma> \\ x \<equiv> t \<turnstile> B t"}}{@{text "\<Gamma> \<turnstile> B x"}}
     8.9    \]
    8.10    This works, because the assumption @{text "x \<equiv> t"} was introduced in
    8.11    a context with @{text "x"} being fresh, so @{text "x"} does not
    8.12 @@ -258,39 +258,54 @@
    8.13    references to free variables or assumptions not present in the proof
    8.14    context.
    8.15  
    8.16 -  \medskip The @{text "prove"} operation provides an interface for
    8.17 -  structured backwards reasoning under program control, with some
    8.18 -  explicit sanity checks of the result.  The goal context can be
    8.19 -  augmented by additional fixed variables (cf.\
    8.20 -  \secref{sec:variables}) and assumptions (cf.\
    8.21 -  \secref{sec:assumptions}), which will be available as local facts
    8.22 -  during the proof and discharged into implications in the result.
    8.23 -  Type and term variables are generalized as usual, according to the
    8.24 -  context.
    8.25 +  \medskip The @{text "SUBPROOF"} combinator allows to structure a
    8.26 +  tactical proof recursively by decomposing a selected sub-goal:
    8.27 +  @{text "(\<And>x. A(x) \<Longrightarrow> B(x)) \<Longrightarrow> \<dots>"} is turned into @{text "B(x) \<Longrightarrow> \<dots>"}
    8.28 +  after fixing @{text "x"} and assuming @{text "A(x)"}.  This means
    8.29 +  the tactic needs to solve the conclusion, but may use the premise as
    8.30 +  a local fact, for locally fixed variables.
    8.31  
    8.32 -  The @{text "prove_multi"} operation handles several simultaneous
    8.33 -  claims within a single goal, by using Pure conjunction internally.
    8.34 +  The @{text "prove"} operation provides an interface for structured
    8.35 +  backwards reasoning under program control, with some explicit sanity
    8.36 +  checks of the result.  The goal context can be augmented by
    8.37 +  additional fixed variables (cf.\ \secref{sec:variables}) and
    8.38 +  assumptions (cf.\ \secref{sec:assumptions}), which will be available
    8.39 +  as local facts during the proof and discharged into implications in
    8.40 +  the result.  Type and term variables are generalized as usual,
    8.41 +  according to the context.
    8.42  
    8.43 -  \medskip Tactical proofs may be structured recursively by
    8.44 -  decomposing a sub-goal: @{text "(\<And>x. A(x) \<Longrightarrow> B(x)) \<Longrightarrow> \<dots>"} is turned
    8.45 -  into @{text "B(x) \<Longrightarrow> \<dots>"} after fixing @{text "x"} and assuming @{text
    8.46 -  "A(x)"}.
    8.47 +  The @{text "obtain"} operation produces results by eliminating
    8.48 +  existing facts by means of a given tactic.  This acts like a dual
    8.49 +  conclusion: the proof demonstrates that the context may be augmented
    8.50 +  by certain fixed variables and assumptions.  See also
    8.51 +  \cite{isabelle-isar-ref} for the user-level @{text "\<OBTAIN>"} and
    8.52 +  @{text "\<GUESS>"} elements.  Final results, which may not refer to
    8.53 +  the parameters in the conclusion, need to exported explicitly into
    8.54 +  the original context.
    8.55  *}
    8.56  
    8.57  text %mlref {*
    8.58    \begin{mldecls}
    8.59 +  @{index_ML SUBPROOF:
    8.60 +  "({context: Proof.context, schematics: ctyp list * cterm list,
    8.61 +    params: cterm list, asms: cterm list, concl: cterm,
    8.62 +    prems: thm list} -> tactic) -> Proof.context -> int -> tactic"} \\
    8.63    @{index_ML Goal.prove: "Proof.context -> string list -> term list -> term ->
    8.64    ({prems: thm list, context: Proof.context} -> tactic) -> thm"} \\
    8.65    @{index_ML Goal.prove_multi: "Proof.context -> string list -> term list -> term list ->
    8.66    ({prems: thm list, context: Proof.context} -> tactic) -> thm list"} \\
    8.67 -  @{index_ML SUBPROOF:
    8.68 -  "({context: Proof.context, schematics: ctyp list * cterm list,
    8.69 -    params: cterm list, asms: cterm list, concl: cterm,
    8.70 -    prems: thm list} -> tactic) -> Proof.context -> int -> tactic"}
    8.71 +  @{index_ML Obtain.result: "(Proof.context -> tactic) ->
    8.72 +  thm list -> Proof.context -> (cterm list * thm list) * Proof.context"}
    8.73    \end{mldecls}
    8.74  
    8.75    \begin{description}
    8.76  
    8.77 +  \item @{ML SUBPROOF}~@{text "tac"} decomposes the structure of a
    8.78 +  particular sub-goal, producing an extended context and a reduced
    8.79 +  goal, which needs to be solved by the given tactic.  All schematic
    8.80 +  parameters of the goal are imported into the context as fixed ones,
    8.81 +  which may not be instantiated in the sub-proof.
    8.82 +
    8.83    \item @{ML Goal.prove}~@{text "ctxt xs As C tac"} states goal @{text
    8.84    "C"} in the context augmented by fixed variables @{text "xs"} and
    8.85    assumptions @{text "As"}, and applies tactic @{text "tac"} to solve
    8.86 @@ -298,15 +313,14 @@
    8.87    as facts.  The result is in HHF normal form.
    8.88  
    8.89    \item @{ML Goal.prove_multi} is simular to @{ML Goal.prove}, but
    8.90 -  states several conclusions simultaneously.  @{ML
    8.91 -  Tactic.conjunction_tac} may be used to split these into individual
    8.92 -  subgoals before commencing the actual proof.
    8.93 +  states several conclusions simultaneously.  The goal is encoded by
    8.94 +  means of Pure conjunction; @{ML Tactic.conjunction_tac} will turn
    8.95 +  this into a collection of individual subgoals.
    8.96  
    8.97 -  \item @{ML SUBPROOF}~@{text "tac"} decomposes the structure of a
    8.98 -  particular sub-goal, producing an extended context and a reduced
    8.99 -  goal, which needs to be solved by the given tactic.  All schematic
   8.100 -  parameters of the goal are imported into the context as fixed ones,
   8.101 -  which may not be instantiated in the sub-proof.
   8.102 +  \item @{ML Obtain.result}~@{text "tac thms ctxt"} eliminates the
   8.103 +  given facts using a tactic, which results in additional fixed
   8.104 +  variables and assumptions in the context.  Final results need to be
   8.105 +  exported explicitly.
   8.106  
   8.107    \end{description}
   8.108  *}
     9.1 --- a/doc-src/IsarImplementation/Thy/unused.thy	Thu Sep 07 15:16:51 2006 +0200
     9.2 +++ b/doc-src/IsarImplementation/Thy/unused.thy	Thu Sep 07 20:12:08 2006 +0200
     9.3 @@ -1,3 +1,6 @@
     9.4 +
     9.5 +section {* Sessions and document preparation *}
     9.6 +
     9.7  section {* Structured output *}
     9.8  
     9.9  subsection {* Pretty printing *}
    10.1 --- a/doc-src/IsarImplementation/style.sty	Thu Sep 07 15:16:51 2006 +0200
    10.2 +++ b/doc-src/IsarImplementation/style.sty	Thu Sep 07 20:12:08 2006 +0200
    10.3 @@ -49,6 +49,8 @@
    10.4  \renewcommand{\isatagmlref}{\subsection*{\makebox[0pt][r]{\fbox{\ML}~~}Reference}\begingroup\def\isastyletext{\rm}\small}
    10.5  \renewcommand{\endisatagmlref}{\endgroup}
    10.6  
    10.7 +\newcommand{\isasymGUESS}{\isakeyword{guess}}
    10.8 +\newcommand{\isasymOBTAIN}{\isakeyword{obtain}}
    10.9  \newcommand{\isasymTHEORY}{\isakeyword{theory}}
   10.10  \newcommand{\isasymIMPORTS}{\isakeyword{imports}}
   10.11  \newcommand{\isasymUSES}{\isakeyword{uses}}