misc cleanup;
authorwenzelm
Thu Aug 31 22:55:49 2006 +0200 (2006-08-31)
changeset 2045127ea2ba48fa3
parent 20450 725a91601ed1
child 20452 6d8b29c7a960
misc cleanup;
doc-src/IsarImplementation/Thy/document/integration.tex
doc-src/IsarImplementation/Thy/document/locale.tex
doc-src/IsarImplementation/Thy/document/logic.tex
doc-src/IsarImplementation/Thy/document/prelim.tex
doc-src/IsarImplementation/Thy/document/proof.tex
doc-src/IsarImplementation/Thy/document/tactic.tex
doc-src/IsarImplementation/Thy/integration.thy
doc-src/IsarImplementation/Thy/locale.thy
doc-src/IsarImplementation/Thy/logic.thy
doc-src/IsarImplementation/Thy/prelim.thy
doc-src/IsarImplementation/Thy/proof.thy
doc-src/IsarImplementation/Thy/tactic.thy
doc-src/IsarImplementation/implementation.tex
doc-src/IsarImplementation/style.sty
     1.1 --- a/doc-src/IsarImplementation/Thy/document/integration.tex	Thu Aug 31 18:27:40 2006 +0200
     1.2 +++ b/doc-src/IsarImplementation/Thy/document/integration.tex	Thu Aug 31 22:55:49 2006 +0200
     1.3 @@ -30,19 +30,18 @@
     1.4  \begin{isamarkuptext}%
     1.5  The Isar toplevel may be considered the centeral hub of the
     1.6    Isabelle/Isar system, where all key components and sub-systems are
     1.7 -  integrated into a single read-eval-print loop of Isar commands.
     1.8 -  Here we even incorporate the existing {\ML} toplevel of the compiler
     1.9 +  integrated into a single read-eval-print loop of Isar commands.  We
    1.10 +  shall even incorporate the existing {\ML} toplevel of the compiler
    1.11    and run-time system (cf.\ \secref{sec:ML-toplevel}).
    1.12  
    1.13 -  Isabelle/Isar departs from original ``LCF system architecture''
    1.14 +  Isabelle/Isar departs from the original ``LCF system architecture''
    1.15    where {\ML} was really The Meta Language for defining theories and
    1.16 -  conducting proofs.  Instead, {\ML} merely serves as the
    1.17 +  conducting proofs.  Instead, {\ML} now only serves as the
    1.18    implementation language for the system (and user extensions), while
    1.19 -  our specific Isar toplevel supports particular notions of
    1.20 -  incremental theory and proof development more directly.  This
    1.21 -  includes the graph structure of theories and the block structure of
    1.22 -  proofs, support for unlimited undo, facilities for tracing,
    1.23 -  debugging, timing, profiling.
    1.24 +  the specific Isar toplevel supports the concepts of theory and proof
    1.25 +  development natively.  This includes the graph structure of theories
    1.26 +  and the block structure of proofs, support for unlimited undo,
    1.27 +  facilities for tracing, debugging, timing, profiling etc.
    1.28  
    1.29    \medskip The toplevel maintains an implicit state, which is
    1.30    transformed by a sequence of transitions -- either interactively or
    1.31 @@ -50,9 +49,9 @@
    1.32    encapsulated as safe transactions, such that both failure and undo
    1.33    are handled conveniently without destroying the underlying draft
    1.34    theory (cf.~\secref{sec:context-theory}).  In batch mode,
    1.35 -  transitions operate in a strictly linear (destructive) fashion, such
    1.36 -  that error conditions abort the present attempt to construct a
    1.37 -  theory altogether.
    1.38 +  transitions operate in a linear (destructive) fashion, such that
    1.39 +  error conditions abort the present attempt to construct a theory or
    1.40 +  proof altogether.
    1.41  
    1.42    The toplevel state is a disjoint sum of empty \isa{toplevel}, or
    1.43    \isa{theory}, or \isa{proof}.  On entering the main Isar loop we
    1.44 @@ -96,22 +95,23 @@
    1.45    \begin{description}
    1.46  
    1.47    \item \verb|Toplevel.state| represents Isar toplevel states,
    1.48 -  which are normally only manipulated through the toplevel transition
    1.49 -  concept (\secref{sec:toplevel-transition}).  Also note that a
    1.50 -  toplevel state is subject to the same linerarity restrictions as a
    1.51 -  theory context (cf.~\secref{sec:context-theory}).
    1.52 +  which are normally manipulated through the concept of toplevel
    1.53 +  transitions only (\secref{sec:toplevel-transition}).  Also note that
    1.54 +  a raw toplevel state is subject to the same linearity restrictions
    1.55 +  as a theory context (cf.~\secref{sec:context-theory}).
    1.56  
    1.57    \item \verb|Toplevel.UNDEF| is raised for undefined toplevel
    1.58 -  operations: \verb|Toplevel.state| is a sum type, many operations
    1.59 -  work only partially for certain cases.
    1.60 +  operations.  Many operations work only partially for certain cases,
    1.61 +  since \verb|Toplevel.state| is a sum type.
    1.62  
    1.63 -  \item \verb|Toplevel.is_toplevel| checks for an empty toplevel state.
    1.64 +  \item \verb|Toplevel.is_toplevel|~\isa{state} checks for an empty
    1.65 +  toplevel state.
    1.66  
    1.67 -  \item \verb|Toplevel.theory_of| gets the theory of a theory or proof
    1.68 -  (!), otherwise raises \verb|Toplevel.UNDEF|.
    1.69 +  \item \verb|Toplevel.theory_of|~\isa{state} selects the theory of
    1.70 +  a theory or proof (!), otherwise raises \verb|Toplevel.UNDEF|.
    1.71  
    1.72 -  \item \verb|Toplevel.proof_of| gets the Isar proof state if
    1.73 -  available, otherwise raises \verb|Toplevel.UNDEF|.
    1.74 +  \item \verb|Toplevel.proof_of|~\isa{state} selects the Isar proof
    1.75 +  state if available, otherwise raises \verb|Toplevel.UNDEF|.
    1.76  
    1.77    \item \verb|set Toplevel.debug| makes the toplevel print further
    1.78    details about internal error conditions, exceptions being raised
    1.79 @@ -120,9 +120,10 @@
    1.80    \item \verb|set Toplevel.timing| makes the toplevel print timing
    1.81    information for each Isar command being executed.
    1.82  
    1.83 -  \item \verb|Toplevel.profiling| controls low-level profiling of the
    1.84 -  underlying {\ML} runtime system.\footnote{For Poly/ML, 1 means time
    1.85 -  and 2 space profiling.}
    1.86 +  \item \verb|Toplevel.profiling|~\verb|:=|~\isa{n} controls
    1.87 +  low-level profiling of the underlying {\ML} runtime system.  For
    1.88 +  Poly/ML, \isa{n\ {\isacharequal}\ {\isadigit{1}}} means time and \isa{n\ {\isacharequal}\ {\isadigit{2}}} space
    1.89 +  profiling.
    1.90  
    1.91    \end{description}%
    1.92  \end{isamarkuptext}%
    1.93 @@ -135,31 +136,30 @@
    1.94  %
    1.95  \endisadelimmlref
    1.96  %
    1.97 -\isamarkupsubsection{Toplevel transitions%
    1.98 +\isamarkupsubsection{Toplevel transitions \label{sec:toplevel-transition}%
    1.99  }
   1.100  \isamarkuptrue%
   1.101  %
   1.102  \begin{isamarkuptext}%
   1.103 -An Isar toplevel transition consists of a partial
   1.104 -  function on the toplevel state, with additional information for
   1.105 -  diagnostics and error reporting: there are fields for command name,
   1.106 -  source position, optional source text, as well as flags for
   1.107 -  interactive-only commands (which issue a warning in batch-mode),
   1.108 -  printing of result state, etc.
   1.109 +An Isar toplevel transition consists of a partial function on the
   1.110 +  toplevel state, with additional information for diagnostics and
   1.111 +  error reporting: there are fields for command name, source position,
   1.112 +  optional source text, as well as flags for interactive-only commands
   1.113 +  (which issue a warning in batch-mode), printing of result state,
   1.114 +  etc.
   1.115  
   1.116 -  The operational part is represented as a sequential union of a list
   1.117 -  of partial functions, which are tried in turn until the first one
   1.118 -  succeeds (i.e.\ does not raise \verb|Toplevel.UNDEF|).  For example,
   1.119 -  a single Isar command like \isacommand{qed} consists of the union of
   1.120 -  some function \verb|Proof.state -> Proof.state| for proofs
   1.121 -  within proofs, plus \verb|Proof.state -> theory| for proofs at
   1.122 -  the outer theory level.
   1.123 +  The operational part is represented as the sequential union of a
   1.124 +  list of partial functions, which are tried in turn until the first
   1.125 +  one succeeds (i.e.\ does not raise \verb|Toplevel.UNDEF|).  This acts
   1.126 +  like an outer case-expression for various alternative state
   1.127 +  transitions.  For example, \isakeyword{qed} acts differently for a
   1.128 +  local proofs vs.\ the global ending of the main proof.
   1.129  
   1.130    Toplevel transitions are composed via transition transformers.
   1.131    Internally, Isar commands are put together from an empty transition
   1.132    extended by name and source position (and optional source text).  It
   1.133    is then left to the individual command parser to turn the given
   1.134 -  syntax body into a suitable transition transformer that adjoin
   1.135 +  concrete syntax into a suitable transition transformer that adjoin
   1.136    actual operations on a theory or proof state etc.%
   1.137  \end{isamarkuptext}%
   1.138  \isamarkuptrue%
   1.139 @@ -190,32 +190,36 @@
   1.140  
   1.141    \begin{description}
   1.142  
   1.143 -  \item \verb|Toplevel.print| sets the print flag, which causes the
   1.144 -  resulting state of the transition to be echoed in interactive mode.
   1.145 +  \item \verb|Toplevel.print|~\isa{tr} sets the print flag, which
   1.146 +  causes the toplevel loop to echo the result state (in interactive
   1.147 +  mode).
   1.148  
   1.149 -  \item \verb|Toplevel.no_timing| indicates that the transition should
   1.150 -  never show timing information, e.g.\ because it is merely a
   1.151 -  diagnostic command.
   1.152 +  \item \verb|Toplevel.no_timing|~\isa{tr} indicates that the
   1.153 +  transition should never show timing information, e.g.\ because it is
   1.154 +  a diagnostic command.
   1.155  
   1.156 -  \item \verb|Toplevel.keep| adjoins a diagnostic function.
   1.157 +  \item \verb|Toplevel.keep|~\isa{tr} adjoins a diagnostic
   1.158 +  function.
   1.159  
   1.160 -  \item \verb|Toplevel.theory| adjoins a theory transformer.
   1.161 +  \item \verb|Toplevel.theory|~\isa{tr} adjoins a theory
   1.162 +  transformer.
   1.163  
   1.164 -  \item \verb|Toplevel.theory_to_proof| adjoins a global goal function,
   1.165 -  which turns a theory into a proof state.  The theory may be changed
   1.166 -  before entering the proof; the generic Isar goal setup includes an
   1.167 -  argument that specifies how to apply the proven result to the
   1.168 -  theory, when the proof is finished.
   1.169 +  \item \verb|Toplevel.theory_to_proof|~\isa{tr} adjoins a global
   1.170 +  goal function, which turns a theory into a proof state.  The theory
   1.171 +  may be changed before entering the proof; the generic Isar goal
   1.172 +  setup includes an argument that specifies how to apply the proven
   1.173 +  result to the theory, when the proof is finished.
   1.174  
   1.175 -  \item \verb|Toplevel.proof| adjoins a deterministic proof command,
   1.176 -  with a singleton result state.
   1.177 +  \item \verb|Toplevel.proof|~\isa{tr} adjoins a deterministic
   1.178 +  proof command, with a singleton result.
   1.179  
   1.180 -  \item \verb|Toplevel.proofs| adjoins a general proof command, with
   1.181 -  zero or more result states (represented as a lazy list).
   1.182 +  \item \verb|Toplevel.proofs|~\isa{tr} adjoins a general proof
   1.183 +  command, with zero or more result states (represented as a lazy
   1.184 +  list).
   1.185  
   1.186 -  \item \verb|Toplevel.proof_to_theory| adjoins a concluding proof
   1.187 -  command, that returns the resulting theory, after storing the
   1.188 -  resulting facts etc.
   1.189 +  \item \verb|Toplevel.proof_to_theory|~\isa{tr} adjoins a
   1.190 +  concluding proof command, that returns the resulting theory, after
   1.191 +  storing the resulting facts etc.
   1.192  
   1.193    \end{description}%
   1.194  \end{isamarkuptext}%
   1.195 @@ -233,12 +237,11 @@
   1.196  \isamarkuptrue%
   1.197  %
   1.198  \begin{isamarkuptext}%
   1.199 -Apart from regular toplevel transactions there are a few
   1.200 -  special control commands that modify the behavior the toplevel
   1.201 -  itself, and only make sense in interactive mode.  Under normal
   1.202 -  circumstances, the user encounters these only implicitly as part of
   1.203 -  the protocol between the Isabelle/Isar system and a user-interface
   1.204 -  such as ProofGeneral.
   1.205 +There are a few special control commands that modify the behavior
   1.206 +  the toplevel itself, and only make sense in interactive mode.  Under
   1.207 +  normal circumstances, the user encounters these only implicitly as
   1.208 +  part of the protocol between the Isabelle/Isar system and a
   1.209 +  user-interface such as ProofGeneral.
   1.210  
   1.211    \begin{description}
   1.212  
   1.213 @@ -278,14 +281,15 @@
   1.214    no clean way to undo {\ML} declarations, except for reverting to a
   1.215    previously saved state of the whole Isabelle process.  {\ML} input
   1.216    is either read interactively from a TTY, or from a string (usually
   1.217 -  within a theory text), or from a source file (usually associated
   1.218 -  with a theory).
   1.219 +  within a theory text), or from a source file (usually loaded from a
   1.220 +  theory).
   1.221  
   1.222    Whenever the {\ML} toplevel is active, the current Isabelle theory
   1.223    context is passed as an internal reference variable.  Thus {\ML}
   1.224    code may access the theory context during compilation, it may even
   1.225 -  change the value of a theory being under construction --- following
   1.226 -  the usual linearity restrictions (cf.~\secref{sec:context-theory}).%
   1.227 +  change the value of a theory being under construction --- while
   1.228 +  observing the usual linearity restrictions
   1.229 +  (cf.~\secref{sec:context-theory}).%
   1.230  \end{isamarkuptext}%
   1.231  \isamarkuptrue%
   1.232  %
   1.233 @@ -311,28 +315,28 @@
   1.234  
   1.235    \item \verb|the_context ()| refers to the theory context of the
   1.236    {\ML} toplevel --- at compile time!  {\ML} code needs to take care
   1.237 -  to refer to \verb|the_context ()| correctly, recall that evaluation
   1.238 -  of a function body is delayed until actual runtime.  Moreover,
   1.239 -  persistent {\ML} toplevel bindings to an unfinished theory should be
   1.240 -  avoided: code should either project out the desired information
   1.241 -  immediately, or produce an explicit \verb|theory_ref| (cf.\
   1.242 -  \secref{sec:context-theory}).
   1.243 +  to refer to \verb|the_context ()| correctly.  Recall that
   1.244 +  evaluation of a function body is delayed until actual runtime.
   1.245 +  Moreover, persistent {\ML} toplevel bindings to an unfinished theory
   1.246 +  should be avoided: code should either project out the desired
   1.247 +  information immediately, or produce an explicit \verb|theory_ref| (cf.\ \secref{sec:context-theory}).
   1.248  
   1.249    \item \verb|Context.>>|~\isa{f} applies theory transformation
   1.250    \isa{f} to the current theory of the {\ML} toplevel.  In order to
   1.251    work as expected, the theory should be still under construction, and
   1.252    the Isar language element that invoked the {\ML} compiler in the
   1.253 -  first place shoule be ready to accept the changed theory value
   1.254 +  first place should be ready to accept the changed theory value
   1.255    (e.g.\ \isakeyword{ML-setup}, but not plain \isakeyword{ML}).
   1.256 -  Otherwise the theory may get destroyed!
   1.257 +  Otherwise the theory becomes stale!
   1.258  
   1.259    \end{description}
   1.260  
   1.261    It is very important to note that the above functions are really
   1.262    restricted to the compile time, even though the {\ML} compiler is
   1.263    invoked at runtime!  The majority of {\ML} code uses explicit
   1.264 -  functional arguments of a theory or proof context, as required.
   1.265 -  Thus it may get run in an arbitrary context later on.
   1.266 +  functional arguments of a theory or proof context instead.  Thus it
   1.267 +  may be invoked for an arbitrary context later on, without having to
   1.268 +  worry about any operational details.
   1.269  
   1.270    \bigskip
   1.271  
   1.272 @@ -347,16 +351,17 @@
   1.273    \begin{description}
   1.274  
   1.275    \item \verb|Isar.main ()| invokes the Isar toplevel from {\ML},
   1.276 -  initializing the state to empty toplevel state.
   1.277 +  initializing an empty toplevel state.
   1.278  
   1.279    \item \verb|Isar.loop ()| continues the Isar toplevel with the
   1.280 -  current state, after dropping out of the Isar toplevel loop.
   1.281 +  current state, after having dropped out of the Isar toplevel loop.
   1.282  
   1.283    \item \verb|Isar.state ()| and \verb|Isar.exn ()| get current
   1.284 -  toplevel state and optional error condition, respectively.  This
   1.285 -  only works after dropping out of the Isar toplevel loop.
   1.286 +  toplevel state and error condition, respectively.  This only works
   1.287 +  after having dropped out of the Isar toplevel loop.
   1.288  
   1.289 -  \item \verb|Isar.context ()| produces the proof context from \verb|Isar.state ()|.
   1.290 +  \item \verb|Isar.context ()| produces the proof context from \verb|Isar.state ()|, analogous to \verb|Context.proof_of|
   1.291 +  (\secref{sec:generic-context}).
   1.292  
   1.293    \end{description}%
   1.294  \end{isamarkuptext}%
   1.295 @@ -369,32 +374,30 @@
   1.296  %
   1.297  \endisadelimmlref
   1.298  %
   1.299 -\isamarkupsection{Theory database%
   1.300 +\isamarkupsection{Theory database \label{sec:theory-database}%
   1.301  }
   1.302  \isamarkuptrue%
   1.303  %
   1.304  \begin{isamarkuptext}%
   1.305 -The theory database maintains a collection of theories,
   1.306 -  together with some administrative information about the original
   1.307 -  sources, which are held in an external store (i.e.\ a collection of
   1.308 -  directories within the regular file system of the underlying
   1.309 -  platform).
   1.310 +The theory database maintains a collection of theories, together
   1.311 +  with some administrative information about their original sources,
   1.312 +  which are held in an external store (i.e.\ some directory within the
   1.313 +  regular file system).
   1.314  
   1.315 -  The theory database is organized as a directed acyclic graph, with
   1.316 -  entries referenced by theory name.  Although some external
   1.317 -  interfaces allow to include a directory specification, this is only
   1.318 -  a hint to the underlying theory loader mechanism: the internal
   1.319 -  theory name space is flat.
   1.320 +  The theory database is organized as a directed acyclic graph;
   1.321 +  entries are referenced by theory name.  Although some additional
   1.322 +  interfaces allow to include a directory specification as well, this
   1.323 +  is only a hint to the underlying theory loader.  The internal theory
   1.324 +  name space is flat!
   1.325  
   1.326    Theory \isa{A} is associated with the main theory file \isa{A}\verb,.thy,, which needs to be accessible through the theory
   1.327 -  loader path.  A number of optional {\ML} source files may be
   1.328 +  loader path.  Any number of additional {\ML} source files may be
   1.329    associated with each theory, by declaring these dependencies in the
   1.330    theory header as \isa{{\isasymUSES}}, and loading them consecutively
   1.331    within the theory context.  The system keeps track of incoming {\ML}
   1.332 -  sources and associates them with the current theory.  The special
   1.333 -  theory {\ML} file \isa{A}\verb,.ML, is loaded after a theory has
   1.334 -  been concluded, in order to support legacy proof {\ML} proof
   1.335 -  scripts.
   1.336 +  sources and associates them with the current theory.  The file
   1.337 +  \isa{A}\verb,.ML, is loaded after a theory has been concluded, in
   1.338 +  order to support legacy proof {\ML} proof scripts.
   1.339  
   1.340    The basic internal actions of the theory database are \isa{update}, \isa{outdate}, and \isa{remove}:
   1.341  
   1.342 @@ -402,29 +405,29 @@
   1.343  
   1.344    \item \isa{update\ A} introduces a link of \isa{A} with a
   1.345    \isa{theory} value of the same name; it asserts that the theory
   1.346 -  sources are consistent with that value.
   1.347 +  sources are now consistent with that value;
   1.348  
   1.349    \item \isa{outdate\ A} invalidates the link of a theory database
   1.350 -  entry to its sources, but retains the present theory value.
   1.351 +  entry to its sources, but retains the present theory value;
   1.352  
   1.353 -  \item \isa{remove\ A} removes entry \isa{A} from the theory
   1.354 +  \item \isa{remove\ A} deletes entry \isa{A} from the theory
   1.355    database.
   1.356    
   1.357    \end{itemize}
   1.358  
   1.359    These actions are propagated to sub- or super-graphs of a theory
   1.360 -  entry in the usual way, in order to preserve global consistency of
   1.361 -  the state of all loaded theories with the sources of the external
   1.362 -  store.  This implies causal dependencies of certain actions: \isa{update} or \isa{outdate} of an entry will \isa{outdate}
   1.363 -  all descendants; \isa{remove} will \isa{remove} all
   1.364 -  descendants.
   1.365 +  entry as expected, in order to preserve global consistency of the
   1.366 +  state of all loaded theories with the sources of the external store.
   1.367 +  This implies certain causalities between actions: \isa{update}
   1.368 +  or \isa{outdate} of an entry will \isa{outdate} all
   1.369 +  descendants; \isa{remove} will \isa{remove} all descendants.
   1.370  
   1.371    \medskip There are separate user-level interfaces to operate on the
   1.372    theory database directly or indirectly.  The primitive actions then
   1.373    just happen automatically while working with the system.  In
   1.374 -  particular, processing a theory header \isa{{\isasymTHEORY}\ A\ {\isasymIMPORTS}\ B\isactrlsub {\isadigit{1}}\ {\isasymdots}\ B\isactrlsub n\ {\isasymBEGIN}} ensure that the
   1.375 +  particular, processing a theory header \isa{{\isasymTHEORY}\ A\ {\isasymIMPORTS}\ B\isactrlsub {\isadigit{1}}\ {\isasymdots}\ B\isactrlsub n\ {\isasymBEGIN}} ensures that the
   1.376    sub-graph of the collective imports \isa{B\isactrlsub {\isadigit{1}}\ {\isasymdots}\ B\isactrlsub n}
   1.377 -  is up-to-date.  Earlier theories are reloaded as required, with
   1.378 +  is up-to-date, too.  Earlier theories are reloaded as required, with
   1.379    \isa{update} actions proceeding in topological order according to
   1.380    theory dependencies.  There may be also a wave of implied \isa{outdate} actions for derived theory nodes until a stable situation
   1.381    is achieved eventually.%
   1.382 @@ -442,8 +445,6 @@
   1.383    \indexml{theory}\verb|theory: string -> theory| \\
   1.384    \indexml{use-thy}\verb|use_thy: string -> unit| \\
   1.385    \indexml{update-thy}\verb|update_thy: string -> unit| \\
   1.386 -  \indexml{use-thy-only}\verb|use_thy_only: string -> unit| \\
   1.387 -  \indexml{update-thy-only}\verb|update_thy_only: string -> unit| \\
   1.388    \indexml{touch-thy}\verb|touch_thy: string -> unit| \\
   1.389    \indexml{remove-thy}\verb|remove_thy: string -> unit| \\[1ex]
   1.390    \indexml{ThyInfo.begin-theory}\verb|ThyInfo.begin_theory|\verb|: ... -> bool -> theory| \\
   1.391 @@ -456,8 +457,8 @@
   1.392    \begin{description}
   1.393  
   1.394    \item \verb|theory|~\isa{A} retrieves the theory value presently
   1.395 -  associated with \isa{A}.  The result is not necessarily
   1.396 -  up-to-date!
   1.397 +  associated with name \isa{A}.  Note that the result might be
   1.398 +  outdated.
   1.399  
   1.400    \item \verb|use_thy|~\isa{A} loads theory \isa{A} if it is absent
   1.401    or out-of-date.  It ensures that all parent theories are available
   1.402 @@ -465,20 +466,12 @@
   1.403    present.
   1.404  
   1.405    \item \verb|update_thy| is similar to \verb|use_thy|, but ensures that
   1.406 -  the \isa{A} and all of its ancestors are fully up-to-date.
   1.407 +  theory \isa{A} and all ancestors are fully up-to-date.
   1.408  
   1.409 -  \item \verb|use_thy_only|~\isa{A} is like \verb|use_thy|~\isa{A},
   1.410 -  but refrains from loading the attached \isa{A}\verb,.ML, file.
   1.411 -  This is occasionally useful in replaying legacy {\ML} proof scripts
   1.412 -  by hand.
   1.413 -  
   1.414 -  \item \verb|update_thy_only| is analogous to \verb|use_thy_only|, but
   1.415 -  proceeds like \verb|update_thy| for ancestors.
   1.416 +  \item \verb|touch_thy|~\isa{A} performs and \isa{outdate} action
   1.417 +  on theory \isa{A} and all descendants.
   1.418  
   1.419 -  \item \verb|touch_thy|~\isa{A} performs \isa{outdate} action on
   1.420 -  theory \isa{A} and all of its descendants.
   1.421 -
   1.422 -  \item \verb|remove_thy|~\isa{A} removes \isa{A} and all of its
   1.423 +  \item \verb|remove_thy|~\isa{A} deletes theory \isa{A} and all
   1.424    descendants from the theory database.
   1.425  
   1.426    \item \verb|ThyInfo.begin_theory| is the basic operation behind a
   1.427 @@ -489,22 +482,22 @@
   1.428    normally not invoked directly.
   1.429  
   1.430    \item \verb|ThyInfo.end_theory| concludes the loading of a theory
   1.431 -  proper; an attached theory {\ML} file may be still loaded later on.
   1.432 -  This is {\ML} functions is normally not invoked directly.
   1.433 +  proper.  An attached theory {\ML} file may be still loaded later on.
   1.434 +  This is function is normally not invoked directly.
   1.435  
   1.436 -  \item \verb|ThyInfo.register_theory|~{text thy} registers an existing
   1.437 -  theory value with the theory loader database.  There is no
   1.438 -  management of associated sources; this is mainly for bootstrapping.
   1.439 +  \item \verb|ThyInfo.register_theory|~\isa{text\ thy} registers an
   1.440 +  existing theory value with the theory loader database.  There is no
   1.441 +  management of associated sources.
   1.442  
   1.443    \item \verb|ThyInfo.add_hook|~\isa{f} registers function \isa{f} as a hook for theory database actions.  The function will be
   1.444    invoked with the action and theory name being involved; thus derived
   1.445    actions may be performed in associated system components, e.g.\
   1.446 -  maintaining the state of an editor for theory sources.
   1.447 +  maintaining the state of an editor for the theory sources.
   1.448  
   1.449    The kind and order of actions occurring in practice depends both on
   1.450    user interactions and the internal process of resolving theory
   1.451    imports.  Hooks should not rely on a particular policy here!  Any
   1.452 -  exceptions raised by the hook are ignored by the theory database.
   1.453 +  exceptions raised by the hook are ignored.
   1.454  
   1.455    \end{description}%
   1.456  \end{isamarkuptext}%
   1.457 @@ -517,6 +510,15 @@
   1.458  %
   1.459  \endisadelimmlref
   1.460  %
   1.461 +\isamarkupsection{Sessions and document preparation%
   1.462 +}
   1.463 +\isamarkuptrue%
   1.464 +%
   1.465 +\begin{isamarkuptext}%
   1.466 +FIXME%
   1.467 +\end{isamarkuptext}%
   1.468 +\isamarkuptrue%
   1.469 +%
   1.470  \isadelimtheory
   1.471  %
   1.472  \endisadelimtheory
     2.1 --- a/doc-src/IsarImplementation/Thy/document/locale.tex	Thu Aug 31 18:27:40 2006 +0200
     2.2 +++ b/doc-src/IsarImplementation/Thy/document/locale.tex	Thu Aug 31 22:55:49 2006 +0200
     2.3 @@ -32,7 +32,7 @@
     2.4  \end{isamarkuptext}%
     2.5  \isamarkuptrue%
     2.6  %
     2.7 -\isamarkupsection{Locales%
     2.8 +\isamarkupsection{Type-checking specifications%
     2.9  }
    2.10  \isamarkuptrue%
    2.11  %
    2.12 @@ -41,6 +41,17 @@
    2.13  \end{isamarkuptext}%
    2.14  \isamarkuptrue%
    2.15  %
    2.16 +\isamarkupsection{Localized theory specifications%
    2.17 +}
    2.18 +\isamarkuptrue%
    2.19 +%
    2.20 +\begin{isamarkuptext}%
    2.21 +FIXME
    2.22 +
    2.23 +  \glossary{Local theory}{FIXME}%
    2.24 +\end{isamarkuptext}%
    2.25 +\isamarkuptrue%
    2.26 +%
    2.27  \isadelimtheory
    2.28  %
    2.29  \endisadelimtheory
     3.1 --- a/doc-src/IsarImplementation/Thy/document/logic.tex	Thu Aug 31 18:27:40 2006 +0200
     3.2 +++ b/doc-src/IsarImplementation/Thy/document/logic.tex	Thu Aug 31 22:55:49 2006 +0200
     3.3 @@ -23,11 +23,7 @@
     3.4  }
     3.5  \isamarkuptrue%
     3.6  %
     3.7 -\isamarkupsection{Syntax%
     3.8 -}
     3.9 -\isamarkuptrue%
    3.10 -%
    3.11 -\isamarkupsubsection{Variable names%
    3.12 +\isamarkupsection{Variable names%
    3.13  }
    3.14  \isamarkuptrue%
    3.15  %
    3.16 @@ -36,39 +32,41 @@
    3.17  \end{isamarkuptext}%
    3.18  \isamarkuptrue%
    3.19  %
    3.20 -\isamarkupsubsection{Simply-typed lambda calculus%
    3.21 +\isamarkupsection{Types \label{sec:types}%
    3.22  }
    3.23  \isamarkuptrue%
    3.24  %
    3.25  \begin{isamarkuptext}%
    3.26 -FIXME
    3.27 +\glossary{Type class}{FIXME}
    3.28 +
    3.29 +  \glossary{Type arity}{FIXME}
    3.30 +
    3.31 +  \glossary{Sort}{FIXME}
    3.32 +
    3.33 +  FIXME classes and sorts
    3.34  
    3.35 -\glossary{Type}{FIXME}
    3.36 -\glossary{Term}{FIXME}%
    3.37 +
    3.38 +  \glossary{Type}{FIXME}
    3.39 +
    3.40 +  \glossary{Type constructor}{FIXME}
    3.41 +
    3.42 +  \glossary{Type variable}{FIXME}
    3.43 +
    3.44 +  FIXME simple types%
    3.45  \end{isamarkuptext}%
    3.46  \isamarkuptrue%
    3.47  %
    3.48 -\isamarkupsubsection{The order-sorted algebra of types%
    3.49 +\isamarkupsection{Terms \label{sec:terms}%
    3.50  }
    3.51  \isamarkuptrue%
    3.52  %
    3.53  \begin{isamarkuptext}%
    3.54 -FIXME
    3.55 -
    3.56 -\glossary{Type constructor}{FIXME}
    3.57 -
    3.58 -\glossary{Type class}{FIXME}
    3.59 +\glossary{Term}{FIXME}
    3.60  
    3.61 -\glossary{Type arity}{FIXME}
    3.62 -
    3.63 -\glossary{Sort}{FIXME}%
    3.64 +  FIXME de-Bruijn representation of lambda terms%
    3.65  \end{isamarkuptext}%
    3.66  \isamarkuptrue%
    3.67  %
    3.68 -\isamarkupsubsection{Type-inference and schematic polymorphism%
    3.69 -}
    3.70 -\isamarkuptrue%
    3.71 -%
    3.72  \begin{isamarkuptext}%
    3.73  FIXME
    3.74  
    3.75 @@ -78,21 +76,7 @@
    3.76  \end{isamarkuptext}%
    3.77  \isamarkuptrue%
    3.78  %
    3.79 -\isamarkupsection{Theory%
    3.80 -}
    3.81 -\isamarkuptrue%
    3.82 -%
    3.83 -\begin{isamarkuptext}%
    3.84 -FIXME
    3.85 -
    3.86 -\glossary{Constant}{Essentially a \seeglossary{fixed variable} of the
    3.87 -theory context, but slightly more flexible since it may be used at
    3.88 -different type-instances, due to \seeglossary{schematic
    3.89 -polymorphism.}}%
    3.90 -\end{isamarkuptext}%
    3.91 -\isamarkuptrue%
    3.92 -%
    3.93 -\isamarkupsection{Deduction%
    3.94 +\isamarkupsection{Theorems \label{sec:thms}%
    3.95  }
    3.96  \isamarkuptrue%
    3.97  %
    3.98 @@ -171,12 +155,21 @@
    3.99  \end{isamarkuptext}%
   3.100  \isamarkuptrue%
   3.101  %
   3.102 -\isamarkupsection{Proof terms%
   3.103 +\isamarkupsection{Low-level specifications%
   3.104  }
   3.105  \isamarkuptrue%
   3.106  %
   3.107  \begin{isamarkuptext}%
   3.108 -FIXME%
   3.109 +FIXME
   3.110 +
   3.111 +\glossary{Constant}{Essentially a \seeglossary{fixed variable} of the
   3.112 +theory context, but slightly more flexible since it may be used at
   3.113 +different type-instances, due to \seeglossary{schematic
   3.114 +polymorphism.}}
   3.115 +
   3.116 +\glossary{Axiom}{FIXME}
   3.117 +
   3.118 +\glossary{Primitive definition}{FIXME}%
   3.119  \end{isamarkuptext}%
   3.120  \isamarkuptrue%
   3.121  %
     4.1 --- a/doc-src/IsarImplementation/Thy/document/prelim.tex	Thu Aug 31 18:27:40 2006 +0200
     4.2 +++ b/doc-src/IsarImplementation/Thy/document/prelim.tex	Thu Aug 31 22:55:49 2006 +0200
     4.3 @@ -28,19 +28,20 @@
     4.4  \isamarkuptrue%
     4.5  %
     4.6  \begin{isamarkuptext}%
     4.7 -A logical context represents the background that is taken for
     4.8 -  granted when formulating statements and composing proofs.  It acts
     4.9 -  as a medium to produce formal content, depending on earlier material
    4.10 -  (declarations, results etc.).
    4.11 +A logical context represents the background that is required for
    4.12 +  formulating statements and composing proofs.  It acts as a medium to
    4.13 +  produce formal content, depending on earlier material (declarations,
    4.14 +  results etc.).
    4.15  
    4.16 -  In particular, derivations within the primitive Pure logic can be
    4.17 -  described as a judgment \isa{{\isasymGamma}\ {\isasymturnstile}\isactrlsub {\isasymTheta}\ {\isasymphi}}, meaning that a
    4.18 +  For example, derivations within the Isabelle/Pure logic can be
    4.19 +  described as a judgment \isa{{\isasymGamma}\ {\isasymturnstile}\isactrlsub {\isasymTheta}\ {\isasymphi}}, which means that a
    4.20    proposition \isa{{\isasymphi}} is derivable from hypotheses \isa{{\isasymGamma}}
    4.21    within the theory \isa{{\isasymTheta}}.  There are logical reasons for
    4.22 -  keeping \isa{{\isasymTheta}} and \isa{{\isasymGamma}} separate: theories support type
    4.23 -  constructors and schematic polymorphism of constants and axioms,
    4.24 -  while the inner calculus of \isa{{\isasymGamma}\ {\isasymturnstile}\ {\isasymphi}} is limited to Simple
    4.25 -  Type Theory (with fixed type variables in the assumptions).
    4.26 +  keeping \isa{{\isasymTheta}} and \isa{{\isasymGamma}} separate: theories can be
    4.27 +  liberal about supporting type constructors and schematic
    4.28 +  polymorphism of constants and axioms, while the inner calculus of
    4.29 +  \isa{{\isasymGamma}\ {\isasymturnstile}\ {\isasymphi}} is strictly limited to Simple Type Theory (with
    4.30 +  fixed type variables in the assumptions).
    4.31  
    4.32    \medskip Contexts and derivations are linked by the following key
    4.33    principles:
    4.34 @@ -48,43 +49,43 @@
    4.35    \begin{itemize}
    4.36  
    4.37    \item Transfer: monotonicity of derivations admits results to be
    4.38 -  transferred into a larger context, i.e.\ \isa{{\isasymGamma}\ {\isasymturnstile}\isactrlsub {\isasymTheta}\ {\isasymphi}}
    4.39 -  implies \isa{{\isasymGamma}{\isacharprime}\ {\isasymturnstile}\isactrlsub {\isasymTheta}\isactrlsub {\isacharprime}\ {\isasymphi}} for contexts \isa{{\isasymTheta}{\isacharprime}\ {\isasymsupseteq}\ {\isasymTheta}} and \isa{{\isasymGamma}{\isacharprime}\ {\isasymsupseteq}\ {\isasymGamma}}.
    4.40 +  transferred into a \emph{larger} context, i.e.\ \isa{{\isasymGamma}\ {\isasymturnstile}\isactrlsub {\isasymTheta}\ {\isasymphi}} implies \isa{{\isasymGamma}{\isacharprime}\ {\isasymturnstile}\isactrlsub {\isasymTheta}\isactrlsub {\isacharprime}\ {\isasymphi}} for contexts \isa{{\isasymTheta}{\isacharprime}\ {\isasymsupseteq}\ {\isasymTheta}} and \isa{{\isasymGamma}{\isacharprime}\ {\isasymsupseteq}\ {\isasymGamma}}.
    4.41  
    4.42    \item Export: discharge of hypotheses admits results to be exported
    4.43 -  into a smaller context, i.e.\ \isa{{\isasymGamma}{\isacharprime}\ {\isasymturnstile}\isactrlsub {\isasymTheta}\ {\isasymphi}} implies
    4.44 -  \isa{{\isasymGamma}\ {\isasymturnstile}\isactrlsub {\isasymTheta}\ {\isasymDelta}\ {\isasymLongrightarrow}\ {\isasymphi}} where \isa{{\isasymGamma}{\isacharprime}\ {\isasymsupseteq}\ {\isasymGamma}} and \isa{{\isasymDelta}\ {\isacharequal}\ {\isasymGamma}{\isacharprime}\ {\isacharminus}\ {\isasymGamma}}.  Note that \isa{{\isasymTheta}} remains unchanged here, only the
    4.45 -  \isa{{\isasymGamma}} part is affected.
    4.46 +  into a \emph{smaller} context, i.e.\ \isa{{\isasymGamma}{\isacharprime}\ {\isasymturnstile}\isactrlsub {\isasymTheta}\ {\isasymphi}}
    4.47 +  implies \isa{{\isasymGamma}\ {\isasymturnstile}\isactrlsub {\isasymTheta}\ {\isasymDelta}\ {\isasymLongrightarrow}\ {\isasymphi}} where \isa{{\isasymGamma}{\isacharprime}\ {\isasymsupseteq}\ {\isasymGamma}} and
    4.48 +  \isa{{\isasymDelta}\ {\isacharequal}\ {\isasymGamma}{\isacharprime}\ {\isacharminus}\ {\isasymGamma}}.  Note that \isa{{\isasymTheta}} remains unchanged here,
    4.49 +  only the \isa{{\isasymGamma}} part is affected.
    4.50  
    4.51    \end{itemize}
    4.52  
    4.53 -  \medskip Isabelle/Isar provides two different notions of abstract
    4.54 -  containers called \emph{theory context} and \emph{proof context},
    4.55 -  respectively.  These model the main characteristics of the primitive
    4.56 -  \isa{{\isasymTheta}} and \isa{{\isasymGamma}} above, without subscribing to any
    4.57 -  particular kind of content yet.  Instead, contexts merely impose a
    4.58 -  certain policy of managing arbitrary \emph{context data}.  The
    4.59 -  system provides strongly typed mechanisms to declare new kinds of
    4.60 +  \medskip By modeling the main characteristics of the primitive
    4.61 +  \isa{{\isasymTheta}} and \isa{{\isasymGamma}} above, and abstracting over any
    4.62 +  particular logical content, we arrive at the fundamental notions of
    4.63 +  \emph{theory context} and \emph{proof context} in Isabelle/Isar.
    4.64 +  These implement a certain policy to manage arbitrary \emph{context
    4.65 +  data}.  There is a strongly-typed mechanism to declare new kinds of
    4.66    data at compile time.
    4.67  
    4.68 -  Thus the internal bootstrap process of Isabelle/Pure eventually
    4.69 -  reaches a stage where certain data slots provide the logical content
    4.70 -  of \isa{{\isasymTheta}} and \isa{{\isasymGamma}} sketched above, but this does not
    4.71 -  stop there!  Various additional data slots support all kinds of
    4.72 -  mechanisms that are not necessarily part of the core logic.
    4.73 +  The internal bootstrap process of Isabelle/Pure eventually reaches a
    4.74 +  stage where certain data slots provide the logical content of \isa{{\isasymTheta}} and \isa{{\isasymGamma}} sketched above, but this does not stop there!
    4.75 +  Various additional data slots support all kinds of mechanisms that
    4.76 +  are not necessarily part of the core logic.
    4.77  
    4.78    For example, there would be data for canonical introduction and
    4.79    elimination rules for arbitrary operators (depending on the
    4.80    object-logic and application), which enables users to perform
    4.81 -  standard proof steps implicitly (cf.\ the \isa{rule} method).
    4.82 +  standard proof steps implicitly (cf.\ the \isa{rule} method
    4.83 +  \cite{isabelle-isar-ref}).
    4.84  
    4.85 -  Isabelle is able to bring forth more and more concepts successively.
    4.86 -  In particular, an object-logic like Isabelle/HOL continues the
    4.87 -  Isabelle/Pure setup by adding specific components for automated
    4.88 -  reasoning (classical reasoner, tableau prover, structured induction
    4.89 -  etc.) and derived specification mechanisms (inductive predicates,
    4.90 -  recursive functions etc.).  All of this is based on the generic data
    4.91 -  management by theory and proof contexts.%
    4.92 +  \medskip Thus Isabelle/Isar is able to bring forth more and more
    4.93 +  concepts successively.  In particular, an object-logic like
    4.94 +  Isabelle/HOL continues the Isabelle/Pure setup by adding specific
    4.95 +  components for automated reasoning (classical reasoner, tableau
    4.96 +  prover, structured induction etc.) and derived specification
    4.97 +  mechanisms (inductive predicates, recursive functions etc.).  All of
    4.98 +  this is ultimately based on the generic data management by theory
    4.99 +  and proof contexts introduced here.%
   4.100  \end{isamarkuptext}%
   4.101  \isamarkuptrue%
   4.102  %
   4.103 @@ -95,31 +96,27 @@
   4.104  \begin{isamarkuptext}%
   4.105  \glossary{Theory}{FIXME}
   4.106  
   4.107 -  Each theory is explicitly named and holds a unique identifier.
   4.108 -  There is a separate \emph{theory reference} for pointing backwards
   4.109 -  to the enclosing theory context of derived entities.  Theories are
   4.110 -  related by a (nominal) sub-theory relation, which corresponds to the
   4.111 -  canonical dependency graph: each theory is derived from a certain
   4.112 -  sub-graph of ancestor theories.  The \isa{merge} of two theories
   4.113 -  refers to the least upper bound, which actually degenerates into
   4.114 -  absorption of one theory into the other, due to the nominal
   4.115 -  sub-theory relation this.
   4.116 +  A \emph{theory} is a data container with explicit named and unique
   4.117 +  identifier.  Theories are related by a (nominal) sub-theory
   4.118 +  relation, which corresponds to the dependency graph of the original
   4.119 +  construction; each theory is derived from a certain sub-graph of
   4.120 +  ancestor theories.
   4.121 +
   4.122 +  The \isa{merge} operation produces the least upper bound of two
   4.123 +  theories, which actually degenerates into absorption of one theory
   4.124 +  into the other (due to the nominal sub-theory relation).
   4.125  
   4.126    The \isa{begin} operation starts a new theory by importing
   4.127    several parent theories and entering a special \isa{draft} mode,
   4.128    which is sustained until the final \isa{end} operation.  A draft
   4.129 -  mode theory acts like a linear type, where updates invalidate
   4.130 -  earlier drafts, but theory reference values will be propagated
   4.131 -  automatically.  Thus derived entities that ``belong'' to a draft
   4.132 -  might be transferred spontaneously to a larger context.  An
   4.133 -  invalidated draft is called ``stale''.
   4.134 +  theory acts like a linear type, where updates invalidate earlier
   4.135 +  versions.  An invalidated draft is called ``stale''.
   4.136  
   4.137    The \isa{checkpoint} operation produces an intermediate stepping
   4.138 -  stone that will survive the next update unscathed: both the original
   4.139 -  and the changed theory remain valid and are related by the
   4.140 -  sub-theory relation.  Checkpointing essentially recovers purely
   4.141 -  functional theory values, at the expense of some extra internal
   4.142 -  bookkeeping.
   4.143 +  stone that will survive the next update: both the original and the
   4.144 +  changed theory remain valid and are related by the sub-theory
   4.145 +  relation.  Checkpointing essentially recovers purely functional
   4.146 +  theory values, at the expense of some extra internal bookkeeping.
   4.147  
   4.148    The \isa{copy} operation produces an auxiliary version that has
   4.149    the same data content, but is unrelated to the original: updates of
   4.150 @@ -127,11 +124,11 @@
   4.151    relation hold.
   4.152  
   4.153    \medskip The example in \figref{fig:ex-theory} below shows a theory
   4.154 -  graph derived from \isa{Pure}. Theory \isa{Length} imports
   4.155 -  \isa{Nat} and \isa{List}.  The theory body consists of a
   4.156 -  sequence of updates, working mostly on drafts.  Intermediate
   4.157 -  checkpoints may occur as well, due to the history mechanism provided
   4.158 -  by the Isar top-level, cf.\ \secref{sec:isar-toplevel}.
   4.159 +  graph derived from \isa{Pure}, with theory \isa{Length}
   4.160 +  importing \isa{Nat} and \isa{List}.  The body of \isa{Length} consists of a sequence of updates, working mostly on
   4.161 +  drafts.  Intermediate checkpoints may occur as well, due to the
   4.162 +  history mechanism provided by the Isar top-level, cf.\
   4.163 +  \secref{sec:isar-toplevel}.
   4.164  
   4.165    \begin{figure}[htb]
   4.166    \begin{center}
   4.167 @@ -152,9 +149,19 @@
   4.168          &            & $\vdots$~~ \\
   4.169          &            & \multicolumn{3}{l}{~~$\isarkeyword{end}$} \\
   4.170    \end{tabular}
   4.171 -  \caption{Theory definition depending on ancestors}\label{fig:ex-theory}
   4.172 +  \caption{A theory definition depending on ancestors}\label{fig:ex-theory}
   4.173    \end{center}
   4.174 -  \end{figure}%
   4.175 +  \end{figure}
   4.176 +
   4.177 +  \medskip There is a separate notion of \emph{theory reference} for
   4.178 +  maintaining a live link to an evolving theory context: updates on
   4.179 +  drafts are propagated automatically.  The dynamic stops after an
   4.180 +  explicit \isa{end} only.
   4.181 +
   4.182 +  Derived entities may store a theory reference in order to indicate
   4.183 +  the context they belong to.  This implicitly assumes monotonic
   4.184 +  reasoning, because the referenced context may become larger without
   4.185 +  further notice.%
   4.186  \end{isamarkuptext}%
   4.187  \isamarkuptrue%
   4.188  %
   4.189 @@ -178,9 +185,9 @@
   4.190  
   4.191    \begin{description}
   4.192  
   4.193 -  \item \verb|theory| represents theory contexts.  This is a
   4.194 -  linear type!  Most operations destroy the old version, which then
   4.195 -  becomes ``stale''.
   4.196 +  \item \verb|theory| represents theory contexts.  This is
   4.197 +  essentially a linear type!  Most operations destroy the original
   4.198 +  version, which then becomes ``stale''.
   4.199  
   4.200    \item \verb|Theory.subthy|~\isa{{\isacharparenleft}thy\isactrlsub {\isadigit{1}}{\isacharcomma}\ thy\isactrlsub {\isadigit{2}}{\isacharparenright}}
   4.201    compares theories according to the inherent graph structure of the
   4.202 @@ -195,15 +202,15 @@
   4.203    stepping stone in the linear development of \isa{thy}.  The next
   4.204    update will result in two related, valid theories.
   4.205  
   4.206 -  \item \verb|Theory.copy|~\isa{thy} produces a variant of \isa{thy} that holds a copy of the same data.  The copy is not related
   4.207 -  to the original, which is not touched at all.
   4.208 +  \item \verb|Theory.copy|~\isa{thy} produces a variant of \isa{thy} that holds a copy of the same data.  The result is not
   4.209 +  related to the original; the original is unchanched.
   4.210  
   4.211 -  \item \verb|theory_ref| represents a sliding reference to a
   4.212 -  valid theory --- updates on the original are propagated
   4.213 +  \item \verb|theory_ref| represents a sliding reference to an
   4.214 +  always valid theory; updates on the original are propagated
   4.215    automatically.
   4.216  
   4.217    \item \verb|Theory.self_ref|~\isa{thy} and \verb|Theory.deref|~\isa{thy{\isacharunderscore}ref} convert between \verb|theory| and \verb|theory_ref|.  As the referenced theory
   4.218 -  evolves monotonically over time, later invocations of \verb|Theory.deref| may refer to larger contexts.
   4.219 +  evolves monotonically over time, later invocations of \verb|Theory.deref| may refer to a larger context.
   4.220  
   4.221    \end{description}%
   4.222  \end{isamarkuptext}%
   4.223 @@ -230,28 +237,28 @@
   4.224  
   4.225    A proof context is a container for pure data with a back-reference
   4.226    to the theory it belongs to.  The \isa{init} operation creates a
   4.227 -  proof context derived from a given theory.  Modifications to draft
   4.228 -  theories are propagated to the proof context as usual, but there is
   4.229 -  also an explicit \isa{transfer} operation to force
   4.230 -  resynchronization with more substantial updates to the underlying
   4.231 -  theory.  The actual context data does not require any special
   4.232 -  bookkeeping, thanks to the lack of destructive features.
   4.233 +  proof context from a given theory.  Modifications to draft theories
   4.234 +  are propagated to the proof context as usual, but there is also an
   4.235 +  explicit \isa{transfer} operation to force resynchronization
   4.236 +  with more substantial updates to the underlying theory.  The actual
   4.237 +  context data does not require any special bookkeeping, thanks to the
   4.238 +  lack of destructive features.
   4.239  
   4.240    Entities derived in a proof context need to record inherent logical
   4.241    requirements explicitly, since there is no separate context
   4.242    identification as for theories.  For example, hypotheses used in
   4.243 -  primitive derivations (cf.\ \secref{sec:thm}) are recorded
   4.244 +  primitive derivations (cf.\ \secref{sec:thms}) are recorded
   4.245    separately within the sequent \isa{{\isasymGamma}\ {\isasymturnstile}\ {\isasymphi}}, just to make double
   4.246    sure.  Results could still leak into an alien proof context do to
   4.247    programming errors, but Isabelle/Isar includes some extra validity
   4.248    checks in critical positions, notably at the end of sub-proof.
   4.249  
   4.250 -  Proof contexts may be produced in arbitrary ways, although the
   4.251 -  common discipline is to follow block structure as a mental model: a
   4.252 -  given context is extended consecutively, and results are exported
   4.253 -  back into the original context.  Note that the Isar proof states
   4.254 -  model block-structured reasoning explicitly, using a stack of proof
   4.255 -  contexts, cf.\ \secref{isar-proof-state}.%
   4.256 +  Proof contexts may be manipulated arbitrarily, although the common
   4.257 +  discipline is to follow block structure as a mental model: a given
   4.258 +  context is extended consecutively, and results are exported back
   4.259 +  into the original context.  Note that the Isar proof states model
   4.260 +  block-structured reasoning explicitly, using a stack of proof
   4.261 +  contexts internally, cf.\ \secref{sec:isar-proof-state}.%
   4.262  \end{isamarkuptext}%
   4.263  \isamarkuptrue%
   4.264  %
   4.265 @@ -279,7 +286,8 @@
   4.266    derived from \isa{thy}, initializing all data.
   4.267  
   4.268    \item \verb|ProofContext.theory_of|~\isa{ctxt} selects the
   4.269 -  background theory from \isa{ctxt}.
   4.270 +  background theory from \isa{ctxt}, dereferencing its internal
   4.271 +  \verb|theory_ref|.
   4.272  
   4.273    \item \verb|ProofContext.transfer|~\isa{thy\ ctxt} promotes the
   4.274    background theory of \isa{ctxt} to the super theory \isa{thy}.
   4.275 @@ -295,21 +303,21 @@
   4.276  %
   4.277  \endisadelimmlref
   4.278  %
   4.279 -\isamarkupsubsection{Generic contexts%
   4.280 +\isamarkupsubsection{Generic contexts \label{sec:generic-context}%
   4.281  }
   4.282  \isamarkuptrue%
   4.283  %
   4.284  \begin{isamarkuptext}%
   4.285  A generic context is the disjoint sum of either a theory or proof
   4.286 -  context.  Occasionally, this simplifies uniform treatment of generic
   4.287 +  context.  Occasionally, this enables uniform treatment of generic
   4.288    context data, typically extra-logical information.  Operations on
   4.289    generic contexts include the usual injections, partial selections,
   4.290    and combinators for lifting operations on either component of the
   4.291    disjoint sum.
   4.292  
   4.293    Moreover, there are total operations \isa{theory{\isacharunderscore}of} and \isa{proof{\isacharunderscore}of} to convert a generic context into either kind: a theory
   4.294 -  can always be selected, while a proof context may have to be
   4.295 -  constructed by an ad-hoc \isa{init} operation.%
   4.296 +  can always be selected from the sum, while a proof context might
   4.297 +  have to be constructed by an ad-hoc \isa{init} operation.%
   4.298  \end{isamarkuptext}%
   4.299  \isamarkuptrue%
   4.300  %
   4.301 @@ -328,15 +336,15 @@
   4.302  
   4.303    \begin{description}
   4.304  
   4.305 -  \item \verb|Context.generic| is the direct sum of \verb|theory| and \verb|Proof.context|, with datatype constructors
   4.306 -  \verb|Context.Theory| and \verb|Context.Proof|.
   4.307 +  \item \verb|Context.generic| is the direct sum of \verb|theory| and \verb|Proof.context|, with the datatype
   4.308 +  constructors \verb|Context.Theory| and \verb|Context.Proof|.
   4.309  
   4.310    \item \verb|Context.theory_of|~\isa{context} always produces a
   4.311    theory from the generic \isa{context}, using \verb|ProofContext.theory_of| as required.
   4.312  
   4.313    \item \verb|Context.proof_of|~\isa{context} always produces a
   4.314 -  proof context from the generic \isa{context}, using \verb|ProofContext.init| as required.  Note that this re-initializes the
   4.315 -  context data with each invocation.
   4.316 +  proof context from the generic \isa{context}, using \verb|ProofContext.init| as required (note that this re-initializes the
   4.317 +  context data with each invocation).
   4.318  
   4.319    \end{description}%
   4.320  \end{isamarkuptext}%
   4.321 @@ -354,23 +362,23 @@
   4.322  \isamarkuptrue%
   4.323  %
   4.324  \begin{isamarkuptext}%
   4.325 -Both theory and proof contexts manage arbitrary data, which is the
   4.326 -  main purpose of contexts in the first place.  Data can be declared
   4.327 -  incrementally at compile --- Isabelle/Pure and major object-logics
   4.328 -  are bootstrapped that way.
   4.329 +The main purpose of theory and proof contexts is to manage arbitrary
   4.330 +  data.  New data types can be declared incrementally at compile time.
   4.331 +  There are separate declaration mechanisms for any of the three kinds
   4.332 +  of contexts: theory, proof, generic.
   4.333  
   4.334    \paragraph{Theory data} may refer to destructive entities, which are
   4.335 -  maintained in correspondence to the linear evolution of theory
   4.336 -  values, or explicit copies.\footnote{Most existing instances of
   4.337 -  destructive theory data are merely historical relics (e.g.\ the
   4.338 -  destructive theorem storage, and destructive hints for the
   4.339 -  Simplifier and Classical rules).}  A theory data declaration needs
   4.340 -  to implement the following specification:
   4.341 +  maintained in direct correspondence to the linear evolution of
   4.342 +  theory values, including explicit copies.\footnote{Most existing
   4.343 +  instances of destructive theory data are merely historical relics
   4.344 +  (e.g.\ the destructive theorem storage, and destructive hints for
   4.345 +  the Simplifier and Classical rules).}  A theory data declaration
   4.346 +  needs to implement the following specification (depending on type
   4.347 +  \isa{T}):
   4.348  
   4.349    \medskip
   4.350    \begin{tabular}{ll}
   4.351    \isa{name{\isacharcolon}\ string} \\
   4.352 -  \isa{T} & the ML type \\
   4.353    \isa{empty{\isacharcolon}\ T} & initial value \\
   4.354    \isa{copy{\isacharcolon}\ T\ {\isasymrightarrow}\ T} & refresh impure data \\
   4.355    \isa{extend{\isacharcolon}\ T\ {\isasymrightarrow}\ T} & re-initialize on import \\
   4.356 @@ -384,26 +392,25 @@
   4.357    should also include the functionality of \isa{copy} for impure
   4.358    data.
   4.359  
   4.360 -  \paragraph{Proof context data} is purely functional.  It is declared
   4.361 -  by implementing the following specification:
   4.362 +  \paragraph{Proof context data} is purely functional.  A declaration
   4.363 +  needs to implement the following specification:
   4.364  
   4.365    \medskip
   4.366    \begin{tabular}{ll}
   4.367    \isa{name{\isacharcolon}\ string} \\
   4.368 -  \isa{T} & the ML type \\
   4.369    \isa{init{\isacharcolon}\ theory\ {\isasymrightarrow}\ T} & produce initial value \\
   4.370    \isa{print{\isacharcolon}\ T\ {\isasymrightarrow}\ unit} & diagnostic output \\
   4.371    \end{tabular}
   4.372    \medskip
   4.373  
   4.374    \noindent The \isa{init} operation is supposed to produce a pure
   4.375 -  value from the given background theory.  The rest is analogous to
   4.376 -  (pure) theory data.
   4.377 +  value from the given background theory.  The remainder is analogous
   4.378 +  to theory data.
   4.379  
   4.380 -  \paragraph{Generic data} provides a hybrid interface for both kinds.
   4.381 -  The declaration is essentially the same as for pure theory data,
   4.382 -  without \isa{copy} (it is always the identity).  The \isa{init} operation for proof contexts selects the current data value
   4.383 -  from the background theory.
   4.384 +  \paragraph{Generic data} provides a hybrid interface for both theory
   4.385 +  and proof data.  The declaration is essentially the same as for
   4.386 +  (pure) theory data, without \isa{copy}, though.  The \isa{init} operation for proof contexts merely selects the current data
   4.387 +  value from the background theory.
   4.388  
   4.389    \bigskip In any case, a data declaration of type \isa{T} results
   4.390    in the following interface:
   4.391 @@ -423,9 +430,9 @@
   4.392    other operations provide access for the particular kind of context
   4.393    (theory, proof, or generic context).  Note that this is a safe
   4.394    interface: there is no other way to access the corresponding data
   4.395 -  slot within a context.  By keeping these operations private, a
   4.396 -  component may maintain abstract values authentically, without other
   4.397 -  components interfering.%
   4.398 +  slot of a context.  By keeping these operations private, a component
   4.399 +  may maintain abstract values authentically, without other components
   4.400 +  interfering.%
   4.401  \end{isamarkuptext}%
   4.402  \isamarkuptrue%
   4.403  %
   4.404 @@ -446,8 +453,8 @@
   4.405  
   4.406    \item \verb|TheoryDataFun|\isa{{\isacharparenleft}spec{\isacharparenright}} declares data for
   4.407    type \verb|theory| according to the specification provided as
   4.408 -  argument structure.  The result structure provides init and access
   4.409 -  operations as described above.
   4.410 +  argument structure.  The resulting structure provides data init and
   4.411 +  access operations as described above.
   4.412  
   4.413    \item \verb|ProofDataFun|\isa{{\isacharparenleft}spec{\isacharparenright}} is analogous for
   4.414    type \verb|Proof.context|.
   4.415 @@ -471,23 +478,34 @@
   4.416  \isamarkuptrue%
   4.417  %
   4.418  \begin{isamarkuptext}%
   4.419 -Named entities of different kinds (logical constant, type,
   4.420 -type class, theorem, method etc.) live in separate name spaces.  It is
   4.421 -usually clear from the occurrence of a name which kind of entity it
   4.422 -refers to.  For example, proof method \isa{foo} vs.\ theorem
   4.423 -\isa{foo} vs.\ logical constant \isa{foo} are easily
   4.424 -distinguished by means of the syntactic context.  A notable exception
   4.425 -are logical identifiers within a term (\secref{sec:terms}): constants,
   4.426 -fixed variables, and bound variables all share the same identifier
   4.427 -syntax, but are distinguished by their scope.
   4.428 +By general convention, each kind of formal entities (logical
   4.429 +  constant, type, type class, theorem, method etc.) lives in a
   4.430 +  separate name space.  It is usually clear from the syntactic context
   4.431 +  of a name, which kind of entity it refers to.  For example, proof
   4.432 +  method \isa{foo} vs.\ theorem \isa{foo} vs.\ logical
   4.433 +  constant \isa{foo} are easily distinguished thanks to the design
   4.434 +  of the concrete outer syntax.  A notable exception are logical
   4.435 +  identifiers within a term (\secref{sec:terms}): constants, fixed
   4.436 +  variables, and bound variables all share the same identifier syntax,
   4.437 +  but are distinguished by their scope.
   4.438  
   4.439 -Each name space is organized as a collection of \emph{qualified
   4.440 -names}, which consist of a sequence of basic name components separated
   4.441 -by dots: \isa{Bar{\isachardot}bar{\isachardot}foo}, \isa{Bar{\isachardot}foo}, and \isa{foo}
   4.442 -are examples for valid qualified names.  Name components are
   4.443 -subdivided into \emph{symbols}, which constitute the smallest textual
   4.444 -unit in Isabelle --- raw characters are normally not encountered
   4.445 -directly.%
   4.446 +  Name spaces are organized uniformly, as a collection of qualified
   4.447 +  names consisting of a sequence of basic name components separated by
   4.448 +  dots: \isa{Bar{\isachardot}bar{\isachardot}foo}, \isa{Bar{\isachardot}foo}, and \isa{foo}
   4.449 +  are examples for qualified names.
   4.450 +
   4.451 +  Despite the independence of names of different kinds, certain naming
   4.452 +  conventions may relate them to each other.  For example, a constant
   4.453 +  \isa{foo} could be accompanied with theorems \isa{foo{\isachardot}intro}, \isa{foo{\isachardot}elim}, \isa{foo{\isachardot}simps} etc.  The same
   4.454 +  could happen for a type \isa{foo}, but this is apt to cause
   4.455 +  clashes in the theorem name space!  To avoid this, there is an
   4.456 +  additional convention to add a suffix that determines the original
   4.457 +  kind.  For example, constant \isa{foo} could associated with
   4.458 +  theorem \isa{foo{\isachardot}intro}, type \isa{foo} with theorem \isa{foo{\isacharunderscore}type{\isachardot}intro}, and type class \isa{foo} with \isa{foo{\isacharunderscore}class{\isachardot}intro}.
   4.459 +
   4.460 +  \medskip Name components are subdivided into \emph{symbols}, which
   4.461 +  constitute the smallest textual unit in Isabelle --- raw characters
   4.462 +  are normally not encountered.%
   4.463  \end{isamarkuptext}%
   4.464  \isamarkuptrue%
   4.465  %
   4.466 @@ -497,48 +515,49 @@
   4.467  %
   4.468  \begin{isamarkuptext}%
   4.469  Isabelle strings consist of a sequence of
   4.470 -symbols\glossary{Symbol}{The smallest unit of text in Isabelle,
   4.471 -subsumes plain ASCII characters as well as an infinite collection of
   4.472 -named symbols (for greek, math etc.).}, which are either packed as an
   4.473 -actual \isa{string}, or represented as a list.  Each symbol is in
   4.474 -itself a small string of the following form:
   4.475 +  symbols\glossary{Symbol}{The smallest unit of text in Isabelle,
   4.476 +  subsumes plain ASCII characters as well as an infinite collection of
   4.477 +  named symbols (for greek, math etc.).}, which are either packed as
   4.478 +  an actual \isa{string}, or represented as a list.  Each symbol
   4.479 +  is in itself a small string of the following form:
   4.480  
   4.481 -\begin{enumerate}
   4.482 +  \begin{enumerate}
   4.483 +
   4.484 +  \item either a singleton ASCII character ``\isa{c}'' (with
   4.485 +  character code 0--127), for example ``\verb,a,'',
   4.486  
   4.487 -\item either a singleton ASCII character ``\isa{c}'' (with
   4.488 -character code 0--127), for example ``\verb,a,'',
   4.489 +  \item or a regular symbol ``\verb,\,\verb,<,\isa{ident}\verb,>,'', for example ``\verb,\,\verb,<alpha>,'',
   4.490  
   4.491 -\item or a regular symbol ``\verb,\,\verb,<,\isa{ident}\verb,>,'',
   4.492 -for example ``\verb,\,\verb,<alpha>,'',
   4.493 +  \item or a control symbol ``\verb,\,\verb,<^,\isa{ident}\verb,>,'', for example ``\verb,\,\verb,<^bold>,'',
   4.494  
   4.495 -\item or a control symbol ``\verb,\,\verb,<^,\isa{ident}\verb,>,'', for example ``\verb,\,\verb,<^bold>,'',
   4.496 +  \item or a raw control symbol ``\verb,\,\verb,<^raw:,\isa{{\isasymdots}}\verb,>,'' where ``\isa{{\isasymdots}}'' refers to any printable ASCII
   4.497 +  character (excluding ``\verb,.,'' and ``\verb,>,'') or non-ASCII
   4.498 +  character, for example ``\verb,\,\verb,<^raw:$\sum_{i = 1}^n$>,'',
   4.499  
   4.500 -\item or a raw control symbol ``\verb,\,\verb,<^raw:,\isa{{\isasymdots}}\verb,>,'' where ``\isa{{\isasymdots}}'' refers to any
   4.501 -printable ASCII character (excluding ``\verb,.,'' and ``\verb,>,'') or
   4.502 -non-ASCII character, for example ``\verb,\,\verb,<^raw:$\sum_{i = 1}^n$>,'',
   4.503 +  \item or a numbered raw control symbol ``\verb,\,\verb,<^raw,\isa{nnn}\verb,>, where \isa{nnn} are digits, for example
   4.504 +  ``\verb,\,\verb,<^raw42>,''.
   4.505  
   4.506 -\item or a numbered raw control symbol ``\verb,\,\verb,<^raw,\isa{nnn}\verb,>, where \isa{nnn} are digits, for example
   4.507 -``\verb,\,\verb,<^raw42>,''.
   4.508 -
   4.509 -\end{enumerate}
   4.510 +  \end{enumerate}
   4.511  
   4.512 -The \isa{ident} syntax for symbol names is \isa{letter\ {\isacharparenleft}letter\ {\isacharbar}\ digit{\isacharparenright}\isactrlsup {\isacharasterisk}}, where \isa{letter\ {\isacharequal}\ A{\isachardot}{\isachardot}Za{\isachardot}{\isachardot}Z} and \isa{digit\ {\isacharequal}\ {\isadigit{0}}{\isachardot}{\isachardot}{\isadigit{9}}}.  There are infinitely many regular symbols and
   4.513 -control symbols available, but a certain collection of standard
   4.514 -symbols is treated specifically.  For example,
   4.515 -``\verb,\,\verb,<alpha>,'' is classified as a (non-ASCII) letter,
   4.516 -which means it may occur within regular Isabelle identifier syntax.
   4.517 +  The \isa{ident} syntax for symbol names is \isa{letter\ {\isacharparenleft}letter\ {\isacharbar}\ digit{\isacharparenright}\isactrlsup {\isacharasterisk}}, where \isa{letter\ {\isacharequal}\ A{\isachardot}{\isachardot}Za{\isachardot}{\isachardot}z} and
   4.518 +  \isa{digit\ {\isacharequal}\ {\isadigit{0}}{\isachardot}{\isachardot}{\isadigit{9}}}.  There are infinitely many regular symbols
   4.519 +  and control symbols available, but a certain collection of standard
   4.520 +  symbols is treated specifically.  For example,
   4.521 +  ``\verb,\,\verb,<alpha>,'' is classified as a (non-ASCII) letter,
   4.522 +  which means it may occur within regular Isabelle identifier syntax.
   4.523  
   4.524 -Output of symbols depends on the print mode (\secref{sec:print-mode}).
   4.525 -For example, the standard {\LaTeX} setup of the Isabelle document
   4.526 -preparation system would present ``\verb,\,\verb,<alpha>,'' as \isa{{\isasymalpha}}, and ``\verb,\,\verb,<^bold>,\verb,\,\verb,<alpha>,'' as \isa{\isactrlbold {\isasymalpha}}.
   4.527 +  Output of symbols depends on the print mode
   4.528 +  (\secref{sec:print-mode}).  For example, the standard {\LaTeX} setup
   4.529 +  of the Isabelle document preparation system would present
   4.530 +  ``\verb,\,\verb,<alpha>,'' as \isa{{\isasymalpha}}, and
   4.531 +  ``\verb,\,\verb,<^bold>,\verb,\,\verb,<alpha>,'' as \isa{\isactrlbold {\isasymalpha}}.
   4.532  
   4.533 -\medskip It is important to note that the character set underlying
   4.534 -Isabelle symbols is plain 7-bit ASCII.  Since 8-bit characters are
   4.535 -passed through transparently, Isabelle may easily process actual
   4.536 -Unicode/UCS data (using the well-known UTF-8 encoding, for example).
   4.537 -Unicode provides its own collection of mathematical symbols, but there
   4.538 -is presently no link to Isabelle's named ones; both kinds of symbols
   4.539 -coexist independently.%
   4.540 +  \medskip It is important to note that the character set underlying
   4.541 +  Isabelle symbols is plain 7-bit ASCII.  Since 8-bit characters are
   4.542 +  passed through transparently, Isabelle may easily process
   4.543 +  Unicode/UCS data as well (using UTF-8 encoding).  Unicode provides
   4.544 +  its own collection of mathematical symbols, but there is no built-in
   4.545 +  link to the ones of Isabelle.%
   4.546  \end{isamarkuptext}%
   4.547  \isamarkuptrue%
   4.548  %
   4.549 @@ -555,33 +574,32 @@
   4.550    \indexml{Symbol.is-letter}\verb|Symbol.is_letter: Symbol.symbol -> bool| \\
   4.551    \indexml{Symbol.is-digit}\verb|Symbol.is_digit: Symbol.symbol -> bool| \\
   4.552    \indexml{Symbol.is-quasi}\verb|Symbol.is_quasi: Symbol.symbol -> bool| \\
   4.553 -  \indexml{Symbol.is-blank}\verb|Symbol.is_blank: Symbol.symbol -> bool| \\
   4.554 +  \indexml{Symbol.is-blank}\verb|Symbol.is_blank: Symbol.symbol -> bool| \\[1ex]
   4.555    \indexmltype{Symbol.sym}\verb|type Symbol.sym| \\
   4.556    \indexml{Symbol.decode}\verb|Symbol.decode: Symbol.symbol -> Symbol.sym| \\
   4.557    \end{mldecls}
   4.558  
   4.559    \begin{description}
   4.560  
   4.561 -  \item \verb|Symbol.symbol| represents Isabelle symbols; this type
   4.562 -  is merely an alias for \verb|string|, but emphasizes the
   4.563 +  \item \verb|Symbol.symbol| represents Isabelle symbols.  This
   4.564 +  type is an alias for \verb|string|, but emphasizes the
   4.565    specific format encountered here.
   4.566  
   4.567    \item \verb|Symbol.explode|~\isa{s} produces a symbol list from
   4.568 -  the packed form usually encountered as user input.  This function
   4.569 -  replaces \verb|String.explode| for virtually all purposes of
   4.570 -  manipulating text in Isabelle!  Plain \verb|implode| may be used
   4.571 -  for the reverse operation.
   4.572 +  the packed form that is encountered in most practical situations.
   4.573 +  This function supercedes \verb|String.explode| for virtually all
   4.574 +  purposes of manipulating text in Isabelle!  Plain \verb|implode|
   4.575 +  may still be used for the reverse operation.
   4.576  
   4.577    \item \verb|Symbol.is_letter|, \verb|Symbol.is_digit|, \verb|Symbol.is_quasi|, \verb|Symbol.is_blank| classify certain symbols
   4.578    (both ASCII and several named ones) according to fixed syntactic
   4.579 -  convections of Isabelle, e.g.\ see \cite{isabelle-isar-ref}.
   4.580 +  conventions of Isabelle, cf.\ \cite{isabelle-isar-ref}.
   4.581  
   4.582    \item \verb|Symbol.sym| is a concrete datatype that represents
   4.583 -  the different kinds of symbols explicitly as \verb|Symbol.Char|,
   4.584 -  \verb|Symbol.Sym|, \verb|Symbol.Ctrl|, or \verb|Symbol.Raw|.
   4.585 +  the different kinds of symbols explicitly with constructors \verb|Symbol.Char|, \verb|Symbol.Sym|, \verb|Symbol.Ctrl|, or \verb|Symbol.Raw|.
   4.586  
   4.587    \item \verb|Symbol.decode| converts the string representation of a
   4.588 -  symbol into the explicit datatype version.
   4.589 +  symbol into the datatype version.
   4.590  
   4.591    \end{description}%
   4.592  \end{isamarkuptext}%
   4.593 @@ -599,49 +617,43 @@
   4.594  \isamarkuptrue%
   4.595  %
   4.596  \begin{isamarkuptext}%
   4.597 -FIXME
   4.598 -
   4.599 -  Qualified names are constructed according to implicit naming
   4.600 -  principles of the present context.
   4.601 -
   4.602 -
   4.603 -  The last component is called \emph{base name}; the remaining prefix
   4.604 -  of qualification may be empty.
   4.605 -
   4.606 -  Some practical conventions help to organize named entities more
   4.607 -  systematically:
   4.608 -
   4.609 -  \begin{itemize}
   4.610 -
   4.611 -  \item Names are qualified first by the theory name, second by an
   4.612 -  optional ``structure''.  For example, a constant \isa{c}
   4.613 -  declared as part of a certain structure \isa{b} (say a type
   4.614 -  definition) in theory \isa{A} will be named \isa{A{\isachardot}b{\isachardot}c}
   4.615 -  internally.
   4.616 +A \emph{qualified name} essentially consists of a non-empty list of
   4.617 +  basic name components.  The packad notation uses a dot as separator,
   4.618 +  as in \isa{A{\isachardot}b}, for example.  The very last component is called
   4.619 +  \emph{base} name, the remaining prefix \emph{qualifier} (which may
   4.620 +  be empty).
   4.621  
   4.622 -  \item
   4.623 -
   4.624 -  \item
   4.625 -
   4.626 -  \item
   4.627 -
   4.628 -  \item
   4.629 -
   4.630 -  \end{itemize}
   4.631 +  A \isa{naming} policy tells how to produce fully qualified names
   4.632 +  from a given specification.  The \isa{full} operation applies
   4.633 +  performs naming of a name; the policy is usually taken from the
   4.634 +  context.  For example, a common policy is to attach an implicit
   4.635 +  prefix.
   4.636  
   4.637 -  Names of different kinds of entities are basically independent, but
   4.638 -  some practical naming conventions relate them to each other.  For
   4.639 -  example, a constant \isa{foo} may be accompanied with theorems
   4.640 -  \isa{foo{\isachardot}intro}, \isa{foo{\isachardot}elim}, \isa{foo{\isachardot}simps} etc.
   4.641 -  The same may happen for a type \isa{foo}, which is then apt to
   4.642 -  cause clashes in the theorem name space!  To avoid this, we
   4.643 -  occasionally follow an additional convention of suffixes that
   4.644 -  determine the original kind of entity that a name has been derived.
   4.645 -  For example, constant \isa{foo} is associated with theorem
   4.646 -  \isa{foo{\isachardot}intro}, type \isa{foo} with theorem \isa{foo{\isacharunderscore}type{\isachardot}intro}, and type class \isa{foo} with \isa{foo{\isacharunderscore}class{\isachardot}intro}.%
   4.647 +  A \isa{name\ space} manages declarations of fully qualified
   4.648 +  names.  There are separate operations to \isa{declare}, \isa{intern}, and \isa{extern} names.
   4.649 +
   4.650 +  FIXME%
   4.651  \end{isamarkuptext}%
   4.652  \isamarkuptrue%
   4.653  %
   4.654 +\isadelimmlref
   4.655 +%
   4.656 +\endisadelimmlref
   4.657 +%
   4.658 +\isatagmlref
   4.659 +%
   4.660 +\begin{isamarkuptext}%
   4.661 +FIXME%
   4.662 +\end{isamarkuptext}%
   4.663 +\isamarkuptrue%
   4.664 +%
   4.665 +\endisatagmlref
   4.666 +{\isafoldmlref}%
   4.667 +%
   4.668 +\isadelimmlref
   4.669 +%
   4.670 +\endisadelimmlref
   4.671 +%
   4.672  \isamarkupsection{Structured output%
   4.673  }
   4.674  \isamarkuptrue%
   4.675 @@ -664,7 +676,7 @@
   4.676  \end{isamarkuptext}%
   4.677  \isamarkuptrue%
   4.678  %
   4.679 -\isamarkupsubsection{Print modes%
   4.680 +\isamarkupsubsection{Print modes \label{sec:print-mode}%
   4.681  }
   4.682  \isamarkuptrue%
   4.683  %
     5.1 --- a/doc-src/IsarImplementation/Thy/document/proof.tex	Thu Aug 31 18:27:40 2006 +0200
     5.2 +++ b/doc-src/IsarImplementation/Thy/document/proof.tex	Thu Aug 31 22:55:49 2006 +0200
     5.3 @@ -19,15 +19,11 @@
     5.4  %
     5.5  \endisadelimtheory
     5.6  %
     5.7 -\isamarkupchapter{Structured reasoning%
     5.8 +\isamarkupchapter{Structured proofs%
     5.9  }
    5.10  \isamarkuptrue%
    5.11  %
    5.12 -\isamarkupsection{Proof context%
    5.13 -}
    5.14 -\isamarkuptrue%
    5.15 -%
    5.16 -\isamarkupsubsection{Local variables%
    5.17 +\isamarkupsection{Local variables%
    5.18  }
    5.19  \isamarkuptrue%
    5.20  %
    5.21 @@ -105,7 +101,34 @@
    5.22  \end{isamarkuptext}%
    5.23  \isamarkuptrue%
    5.24  %
    5.25 -\isamarkupsection{Proof state%
    5.26 +\isamarkupsection{Schematic polymorphism%
    5.27 +}
    5.28 +\isamarkuptrue%
    5.29 +%
    5.30 +\begin{isamarkuptext}%
    5.31 +FIXME%
    5.32 +\end{isamarkuptext}%
    5.33 +\isamarkuptrue%
    5.34 +%
    5.35 +\isamarkupsection{Assumptions%
    5.36 +}
    5.37 +\isamarkuptrue%
    5.38 +%
    5.39 +\begin{isamarkuptext}%
    5.40 +FIXME%
    5.41 +\end{isamarkuptext}%
    5.42 +\isamarkuptrue%
    5.43 +%
    5.44 +\isamarkupsection{Conclusions%
    5.45 +}
    5.46 +\isamarkuptrue%
    5.47 +%
    5.48 +\begin{isamarkuptext}%
    5.49 +FIXME%
    5.50 +\end{isamarkuptext}%
    5.51 +\isamarkuptrue%
    5.52 +%
    5.53 +\isamarkupsection{Structured proofs \label{sec:isar-proof-state}%
    5.54  }
    5.55  \isamarkuptrue%
    5.56  %
    5.57 @@ -125,7 +148,7 @@
    5.58  \end{isamarkuptext}%
    5.59  \isamarkuptrue%
    5.60  %
    5.61 -\isamarkupsection{Methods%
    5.62 +\isamarkupsection{Proof methods%
    5.63  }
    5.64  \isamarkuptrue%
    5.65  %
    5.66 @@ -139,7 +162,7 @@
    5.67  \isamarkuptrue%
    5.68  %
    5.69  \begin{isamarkuptext}%
    5.70 -FIXME%
    5.71 +FIXME ?!%
    5.72  \end{isamarkuptext}%
    5.73  \isamarkuptrue%
    5.74  %
     6.1 --- a/doc-src/IsarImplementation/Thy/document/tactic.tex	Thu Aug 31 18:27:40 2006 +0200
     6.2 +++ b/doc-src/IsarImplementation/Thy/document/tactic.tex	Thu Aug 31 22:55:49 2006 +0200
     6.3 @@ -19,17 +19,19 @@
     6.4  %
     6.5  \endisadelimtheory
     6.6  %
     6.7 -\isamarkupchapter{Tactical theorem proving%
     6.8 +\isamarkupchapter{Goal-directed reasoning%
     6.9  }
    6.10  \isamarkuptrue%
    6.11  %
    6.12  \begin{isamarkuptext}%
    6.13 -The basic idea of tactical theorem proving is to refine the
    6.14 -initial claim in a backwards fashion, until a solved form is reached.
    6.15 -An intermediate goal consists of several subgoals that need to be
    6.16 -solved in order to achieve the main statement; zero subgoals means
    6.17 -that the proof may be finished.  Goal refinement operations are called
    6.18 -tactics; combinators for composing tactics are called tacticals.%
    6.19 +The basic idea of tactical theorem proving is to refine the initial
    6.20 +  claim in a backwards fashion, until a solved form is reached.  An
    6.21 +  intermediate goal consists of several subgoals that need to be
    6.22 +  solved in order to achieve the main statement; zero subgoals means
    6.23 +  that the proof may be finished.  A \isa{tactic} is a refinement
    6.24 +  operation that maps a goal to a lazy sequence of potential
    6.25 +  successors.  A \isa{tactical} is a combinator for composing
    6.26 +  tactics.%
    6.27  \end{isamarkuptext}%
    6.28  \isamarkuptrue%
    6.29  %
    6.30 @@ -38,40 +40,41 @@
    6.31  \isamarkuptrue%
    6.32  %
    6.33  \begin{isamarkuptext}%
    6.34 -Isabelle/Pure represents a goal\glossary{Tactical goal}{A
    6.35 -theorem of \seeglossary{Horn Clause} form stating that a number of
    6.36 -subgoals imply the main conclusion, which is marked as a protected
    6.37 -proposition.} as a theorem stating that the subgoals imply the main
    6.38 -goal: \isa{A\isactrlsub {\isadigit{1}}\ {\isasymLongrightarrow}\ {\isasymdots}\ {\isasymLongrightarrow}\ A\isactrlsub n\ {\isasymLongrightarrow}\ C}.  The outermost goal
    6.39 -structure is that of a Horn Clause\glossary{Horn Clause}{An iterated
    6.40 -implication \isa{A\isactrlsub {\isadigit{1}}\ {\isasymLongrightarrow}\ {\isasymdots}\ {\isasymLongrightarrow}\ A\isactrlsub n\ {\isasymLongrightarrow}\ C}, without any
    6.41 -outermost quantifiers.  Strictly speaking, propositions \isa{A\isactrlsub i} need to be atomic in Horn Clauses, but Isabelle admits
    6.42 -arbitrary substructure here (nested \isa{{\isasymLongrightarrow}} and \isa{{\isasymAnd}}
    6.43 -connectives).}: an iterated implication without any
    6.44 -quantifiers\footnote{Recall that outermost \isa{{\isasymAnd}x{\isachardot}\ {\isasymphi}{\isacharbrackleft}x{\isacharbrackright}} is
    6.45 -always represented via schematic variables in the body: \isa{{\isasymphi}{\isacharbrackleft}{\isacharquery}x{\isacharbrackright}}.  These may get instantiated during the course of
    6.46 -reasoning.}.  For \isa{n\ {\isacharequal}\ {\isadigit{0}}} a goal is solved.
    6.47 +Isabelle/Pure represents a goal\glossary{Tactical goal}{A theorem of
    6.48 +  \seeglossary{Horn Clause} form stating that a number of subgoals
    6.49 +  imply the main conclusion, which is marked as a protected
    6.50 +  proposition.} as a theorem stating that the subgoals imply the main
    6.51 +  goal: \isa{A\isactrlsub {\isadigit{1}}\ {\isasymLongrightarrow}\ {\isasymdots}\ {\isasymLongrightarrow}\ A\isactrlsub n\ {\isasymLongrightarrow}\ C}.  The outermost goal
    6.52 +  structure is that of a Horn Clause\glossary{Horn Clause}{An iterated
    6.53 +  implication \isa{A\isactrlsub {\isadigit{1}}\ {\isasymLongrightarrow}\ {\isasymdots}\ {\isasymLongrightarrow}\ A\isactrlsub n\ {\isasymLongrightarrow}\ C}, without any
    6.54 +  outermost quantifiers.  Strictly speaking, propositions \isa{A\isactrlsub i} need to be atomic in Horn Clauses, but Isabelle admits
    6.55 +  arbitrary substructure here (nested \isa{{\isasymLongrightarrow}} and \isa{{\isasymAnd}}
    6.56 +  connectives).}: i.e.\ an iterated implication without any
    6.57 +  quantifiers\footnote{Recall that outermost \isa{{\isasymAnd}x{\isachardot}\ {\isasymphi}{\isacharbrackleft}x{\isacharbrackright}} is
    6.58 +  always represented via schematic variables in the body: \isa{{\isasymphi}{\isacharbrackleft}{\isacharquery}x{\isacharbrackright}}.  These variables may get instantiated during the course of
    6.59 +  reasoning.}.  For \isa{n\ {\isacharequal}\ {\isadigit{0}}} a goal is called ``solved''.
    6.60  
    6.61 -The structure of each subgoal \isa{A\isactrlsub i} is that of a general
    6.62 -Heriditary Harrop Formula \isa{{\isasymAnd}x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ {\isasymAnd}x\isactrlsub k{\isachardot}\ H\isactrlsub {\isadigit{1}}\ {\isasymLongrightarrow}\ {\isasymdots}\ {\isasymLongrightarrow}\ H\isactrlsub m\ {\isasymLongrightarrow}\ B} according to the normal form where any local
    6.63 -\isa{{\isasymAnd}} is pulled before \isa{{\isasymLongrightarrow}}.  Here \isa{x\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ x\isactrlsub k} are goal parameters, i.e.\ arbitrary-but-fixed entities of
    6.64 -certain types, and \isa{H\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ H\isactrlsub m} are goal
    6.65 -hypotheses, i.e.\ facts that may be assumed locally.  Together, this
    6.66 -forms the goal context of the conclusion \isa{B} to be established.
    6.67 -The goal hypotheses may be again arbitrary Harrop Formulas, although
    6.68 -the level of nesting rarely exceeds 1--2 in practice.
    6.69 +  The structure of each subgoal \isa{A\isactrlsub i} is that of a
    6.70 +  general Hereditary Harrop Formula \isa{{\isasymAnd}x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ {\isasymAnd}x\isactrlsub k{\isachardot}\ H\isactrlsub {\isadigit{1}}\ {\isasymLongrightarrow}\ {\isasymdots}\ {\isasymLongrightarrow}\ H\isactrlsub m\ {\isasymLongrightarrow}\ B} according to the normal
    6.71 +  form where any local \isa{{\isasymAnd}} is pulled before \isa{{\isasymLongrightarrow}}.  Here
    6.72 +  \isa{x\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ x\isactrlsub k} are goal parameters, i.e.\
    6.73 +  arbitrary-but-fixed entities of certain types, and \isa{H\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ H\isactrlsub m} are goal hypotheses, i.e.\ facts that may
    6.74 +  be assumed locally.  Together, this forms the goal context of the
    6.75 +  conclusion \isa{B} to be established.  The goal hypotheses may be
    6.76 +  again Hereditary Harrop Formulas, although the level of nesting
    6.77 +  rarely exceeds 1--2 in practice.
    6.78  
    6.79 -The main conclusion \isa{C} is internally marked as a protected
    6.80 -proposition\glossary{Protected proposition}{An arbitrarily structured
    6.81 -proposition \isa{C} which is forced to appear as atomic by
    6.82 -wrapping it into a propositional identity operator; notation \isa{{\isacharhash}C}.  Protecting a proposition prevents basic inferences from
    6.83 -entering into that structure for the time being.}, which is
    6.84 -occasionally represented explicitly by the notation \isa{{\isacharhash}C}.
    6.85 -This ensures that the decomposition into subgoals and main conclusion
    6.86 -is well-defined for arbitrarily structured claims.
    6.87 +  The main conclusion \isa{C} is internally marked as a protected
    6.88 +  proposition\glossary{Protected proposition}{An arbitrarily
    6.89 +  structured proposition \isa{C} which is forced to appear as
    6.90 +  atomic by wrapping it into a propositional identity operator;
    6.91 +  notation \isa{{\isacharhash}C}.  Protecting a proposition prevents basic
    6.92 +  inferences from entering into that structure for the time being.},
    6.93 +  which is occasionally represented explicitly by the notation \isa{{\isacharhash}C}.  This ensures that the decomposition into subgoals and main
    6.94 +  conclusion is well-defined for arbitrarily structured claims.
    6.95  
    6.96 -\medskip Basic goal management is performed via the following
    6.97 -Isabelle/Pure rules:
    6.98 +  \medskip Basic goal management is performed via the following
    6.99 +  Isabelle/Pure rules:
   6.100  
   6.101    \[
   6.102    \infer[\isa{{\isacharparenleft}init{\isacharparenright}}]{\isa{C\ {\isasymLongrightarrow}\ {\isacharhash}C}}{} \qquad
   6.103 @@ -104,13 +107,13 @@
   6.104  
   6.105    \begin{description}
   6.106  
   6.107 -  \item \verb|Goal.init|~\isa{{\isasymphi}} initializes a tactical goal with
   6.108 +  \item \verb|Goal.init|~\isa{{\isasymphi}} initializes a tactical goal from
   6.109    the type-checked proposition \isa{{\isasymphi}}.
   6.110  
   6.111 -  \item \verb|Goal.finish|~\isa{th} checks whether theorem \isa{th} is a solved goal configuration (zero subgoals), and concludes
   6.112 +  \item \verb|Goal.finish|~\isa{th} checks whether theorem \isa{th} is a solved goal configuration (no subgoals), and concludes
   6.113    the result by removing the goal protection.
   6.114  
   6.115 -  \item \verb|Goal.protect|~\isa{th} protects the whole statement
   6.116 +  \item \verb|Goal.protect|~\isa{th} protects the full statement
   6.117    of theorem \isa{th}.
   6.118  
   6.119    \item \verb|Goal.conclude|~\isa{th} removes the goal protection
   6.120 @@ -173,12 +176,10 @@
   6.121    ill-behaved tactics could have destroyed that information.
   6.122  
   6.123    Several simultaneous claims may be handled within a single goal
   6.124 -  statement by using meta-level conjunction internally.\footnote{This
   6.125 -  is merely syntax for certain derived statements within
   6.126 -  Isabelle/Pure, there is no need to introduce a separate conjunction
   6.127 -  operator.}  The whole configuration may be considered within a
   6.128 -  context of arbitrary-but-fixed parameters and hypotheses, which will
   6.129 -  be available as local facts during the proof and discharged into
   6.130 +  statement by using meta-level conjunction internally.  The whole
   6.131 +  configuration may be considered within a context of
   6.132 +  arbitrary-but-fixed parameters and hypotheses, which will be
   6.133 +  available as local facts during the proof and discharged into
   6.134    implications in the result.
   6.135  
   6.136    All of these administrative tasks are packaged into a separate
     7.1 --- a/doc-src/IsarImplementation/Thy/integration.thy	Thu Aug 31 18:27:40 2006 +0200
     7.2 +++ b/doc-src/IsarImplementation/Thy/integration.thy	Thu Aug 31 22:55:49 2006 +0200
     7.3 @@ -9,19 +9,18 @@
     7.4  
     7.5  text {* The Isar toplevel may be considered the centeral hub of the
     7.6    Isabelle/Isar system, where all key components and sub-systems are
     7.7 -  integrated into a single read-eval-print loop of Isar commands.
     7.8 -  Here we even incorporate the existing {\ML} toplevel of the compiler
     7.9 +  integrated into a single read-eval-print loop of Isar commands.  We
    7.10 +  shall even incorporate the existing {\ML} toplevel of the compiler
    7.11    and run-time system (cf.\ \secref{sec:ML-toplevel}).
    7.12  
    7.13 -  Isabelle/Isar departs from original ``LCF system architecture''
    7.14 +  Isabelle/Isar departs from the original ``LCF system architecture''
    7.15    where {\ML} was really The Meta Language for defining theories and
    7.16 -  conducting proofs.  Instead, {\ML} merely serves as the
    7.17 +  conducting proofs.  Instead, {\ML} now only serves as the
    7.18    implementation language for the system (and user extensions), while
    7.19 -  our specific Isar toplevel supports particular notions of
    7.20 -  incremental theory and proof development more directly.  This
    7.21 -  includes the graph structure of theories and the block structure of
    7.22 -  proofs, support for unlimited undo, facilities for tracing,
    7.23 -  debugging, timing, profiling.
    7.24 +  the specific Isar toplevel supports the concepts of theory and proof
    7.25 +  development natively.  This includes the graph structure of theories
    7.26 +  and the block structure of proofs, support for unlimited undo,
    7.27 +  facilities for tracing, debugging, timing, profiling etc.
    7.28  
    7.29    \medskip The toplevel maintains an implicit state, which is
    7.30    transformed by a sequence of transitions -- either interactively or
    7.31 @@ -29,9 +28,9 @@
    7.32    encapsulated as safe transactions, such that both failure and undo
    7.33    are handled conveniently without destroying the underlying draft
    7.34    theory (cf.~\secref{sec:context-theory}).  In batch mode,
    7.35 -  transitions operate in a strictly linear (destructive) fashion, such
    7.36 -  that error conditions abort the present attempt to construct a
    7.37 -  theory altogether.
    7.38 +  transitions operate in a linear (destructive) fashion, such that
    7.39 +  error conditions abort the present attempt to construct a theory or
    7.40 +  proof altogether.
    7.41  
    7.42    The toplevel state is a disjoint sum of empty @{text toplevel}, or
    7.43    @{text theory}, or @{text proof}.  On entering the main Isar loop we
    7.44 @@ -69,22 +68,23 @@
    7.45    \begin{description}
    7.46  
    7.47    \item @{ML_type Toplevel.state} represents Isar toplevel states,
    7.48 -  which are normally only manipulated through the toplevel transition
    7.49 -  concept (\secref{sec:toplevel-transition}).  Also note that a
    7.50 -  toplevel state is subject to the same linerarity restrictions as a
    7.51 -  theory context (cf.~\secref{sec:context-theory}).
    7.52 +  which are normally manipulated through the concept of toplevel
    7.53 +  transitions only (\secref{sec:toplevel-transition}).  Also note that
    7.54 +  a raw toplevel state is subject to the same linearity restrictions
    7.55 +  as a theory context (cf.~\secref{sec:context-theory}).
    7.56  
    7.57    \item @{ML Toplevel.UNDEF} is raised for undefined toplevel
    7.58 -  operations: @{ML_type Toplevel.state} is a sum type, many operations
    7.59 -  work only partially for certain cases.
    7.60 +  operations.  Many operations work only partially for certain cases,
    7.61 +  since @{ML_type Toplevel.state} is a sum type.
    7.62  
    7.63 -  \item @{ML Toplevel.is_toplevel} checks for an empty toplevel state.
    7.64 +  \item @{ML Toplevel.is_toplevel}~@{text "state"} checks for an empty
    7.65 +  toplevel state.
    7.66  
    7.67 -  \item @{ML Toplevel.theory_of} gets the theory of a theory or proof
    7.68 -  (!), otherwise raises @{ML Toplevel.UNDEF}.
    7.69 +  \item @{ML Toplevel.theory_of}~@{text "state"} selects the theory of
    7.70 +  a theory or proof (!), otherwise raises @{ML Toplevel.UNDEF}.
    7.71  
    7.72 -  \item @{ML Toplevel.proof_of} gets the Isar proof state if
    7.73 -  available, otherwise raises @{ML Toplevel.UNDEF}.
    7.74 +  \item @{ML Toplevel.proof_of}~@{text "state"} selects the Isar proof
    7.75 +  state if available, otherwise raises @{ML Toplevel.UNDEF}.
    7.76  
    7.77    \item @{ML "set Toplevel.debug"} makes the toplevel print further
    7.78    details about internal error conditions, exceptions being raised
    7.79 @@ -93,36 +93,37 @@
    7.80    \item @{ML "set Toplevel.timing"} makes the toplevel print timing
    7.81    information for each Isar command being executed.
    7.82  
    7.83 -  \item @{ML Toplevel.profiling} controls low-level profiling of the
    7.84 -  underlying {\ML} runtime system.\footnote{For Poly/ML, 1 means time
    7.85 -  and 2 space profiling.}
    7.86 +  \item @{ML Toplevel.profiling}~@{verbatim ":="}~@{text "n"} controls
    7.87 +  low-level profiling of the underlying {\ML} runtime system.  For
    7.88 +  Poly/ML, @{text "n = 1"} means time and @{text "n = 2"} space
    7.89 +  profiling.
    7.90  
    7.91    \end{description}
    7.92  *}
    7.93  
    7.94  
    7.95 -subsection {* Toplevel transitions *}
    7.96 +subsection {* Toplevel transitions \label{sec:toplevel-transition} *}
    7.97  
    7.98 -text {* An Isar toplevel transition consists of a partial
    7.99 -  function on the toplevel state, with additional information for
   7.100 -  diagnostics and error reporting: there are fields for command name,
   7.101 -  source position, optional source text, as well as flags for
   7.102 -  interactive-only commands (which issue a warning in batch-mode),
   7.103 -  printing of result state, etc.
   7.104 +text {*
   7.105 +  An Isar toplevel transition consists of a partial function on the
   7.106 +  toplevel state, with additional information for diagnostics and
   7.107 +  error reporting: there are fields for command name, source position,
   7.108 +  optional source text, as well as flags for interactive-only commands
   7.109 +  (which issue a warning in batch-mode), printing of result state,
   7.110 +  etc.
   7.111  
   7.112 -  The operational part is represented as a sequential union of a list
   7.113 -  of partial functions, which are tried in turn until the first one
   7.114 -  succeeds (i.e.\ does not raise @{ML Toplevel.UNDEF}).  For example,
   7.115 -  a single Isar command like \isacommand{qed} consists of the union of
   7.116 -  some function @{ML_type "Proof.state -> Proof.state"} for proofs
   7.117 -  within proofs, plus @{ML_type "Proof.state -> theory"} for proofs at
   7.118 -  the outer theory level.
   7.119 +  The operational part is represented as the sequential union of a
   7.120 +  list of partial functions, which are tried in turn until the first
   7.121 +  one succeeds (i.e.\ does not raise @{ML Toplevel.UNDEF}).  This acts
   7.122 +  like an outer case-expression for various alternative state
   7.123 +  transitions.  For example, \isakeyword{qed} acts differently for a
   7.124 +  local proofs vs.\ the global ending of the main proof.
   7.125  
   7.126    Toplevel transitions are composed via transition transformers.
   7.127    Internally, Isar commands are put together from an empty transition
   7.128    extended by name and source position (and optional source text).  It
   7.129    is then left to the individual command parser to turn the given
   7.130 -  syntax body into a suitable transition transformer that adjoin
   7.131 +  concrete syntax into a suitable transition transformer that adjoin
   7.132    actual operations on a theory or proof state etc.
   7.133  *}
   7.134  
   7.135 @@ -146,32 +147,36 @@
   7.136  
   7.137    \begin{description}
   7.138  
   7.139 -  \item @{ML Toplevel.print} sets the print flag, which causes the
   7.140 -  resulting state of the transition to be echoed in interactive mode.
   7.141 +  \item @{ML Toplevel.print}~@{text "tr"} sets the print flag, which
   7.142 +  causes the toplevel loop to echo the result state (in interactive
   7.143 +  mode).
   7.144  
   7.145 -  \item @{ML Toplevel.no_timing} indicates that the transition should
   7.146 -  never show timing information, e.g.\ because it is merely a
   7.147 -  diagnostic command.
   7.148 +  \item @{ML Toplevel.no_timing}~@{text "tr"} indicates that the
   7.149 +  transition should never show timing information, e.g.\ because it is
   7.150 +  a diagnostic command.
   7.151  
   7.152 -  \item @{ML Toplevel.keep} adjoins a diagnostic function.
   7.153 +  \item @{ML Toplevel.keep}~@{text "tr"} adjoins a diagnostic
   7.154 +  function.
   7.155  
   7.156 -  \item @{ML Toplevel.theory} adjoins a theory transformer.
   7.157 +  \item @{ML Toplevel.theory}~@{text "tr"} adjoins a theory
   7.158 +  transformer.
   7.159  
   7.160 -  \item @{ML Toplevel.theory_to_proof} adjoins a global goal function,
   7.161 -  which turns a theory into a proof state.  The theory may be changed
   7.162 -  before entering the proof; the generic Isar goal setup includes an
   7.163 -  argument that specifies how to apply the proven result to the
   7.164 -  theory, when the proof is finished.
   7.165 +  \item @{ML Toplevel.theory_to_proof}~@{text "tr"} adjoins a global
   7.166 +  goal function, which turns a theory into a proof state.  The theory
   7.167 +  may be changed before entering the proof; the generic Isar goal
   7.168 +  setup includes an argument that specifies how to apply the proven
   7.169 +  result to the theory, when the proof is finished.
   7.170  
   7.171 -  \item @{ML Toplevel.proof} adjoins a deterministic proof command,
   7.172 -  with a singleton result state.
   7.173 +  \item @{ML Toplevel.proof}~@{text "tr"} adjoins a deterministic
   7.174 +  proof command, with a singleton result.
   7.175  
   7.176 -  \item @{ML Toplevel.proofs} adjoins a general proof command, with
   7.177 -  zero or more result states (represented as a lazy list).
   7.178 +  \item @{ML Toplevel.proofs}~@{text "tr"} adjoins a general proof
   7.179 +  command, with zero or more result states (represented as a lazy
   7.180 +  list).
   7.181  
   7.182 -  \item @{ML Toplevel.proof_to_theory} adjoins a concluding proof
   7.183 -  command, that returns the resulting theory, after storing the
   7.184 -  resulting facts etc.
   7.185 +  \item @{ML Toplevel.proof_to_theory}~@{text "tr"} adjoins a
   7.186 +  concluding proof command, that returns the resulting theory, after
   7.187 +  storing the resulting facts etc.
   7.188  
   7.189    \end{description}
   7.190  *}
   7.191 @@ -179,12 +184,12 @@
   7.192  
   7.193  subsection {* Toplevel control *}
   7.194  
   7.195 -text {* Apart from regular toplevel transactions there are a few
   7.196 -  special control commands that modify the behavior the toplevel
   7.197 -  itself, and only make sense in interactive mode.  Under normal
   7.198 -  circumstances, the user encounters these only implicitly as part of
   7.199 -  the protocol between the Isabelle/Isar system and a user-interface
   7.200 -  such as ProofGeneral.
   7.201 +text {*
   7.202 +  There are a few special control commands that modify the behavior
   7.203 +  the toplevel itself, and only make sense in interactive mode.  Under
   7.204 +  normal circumstances, the user encounters these only implicitly as
   7.205 +  part of the protocol between the Isabelle/Isar system and a
   7.206 +  user-interface such as ProofGeneral.
   7.207  
   7.208    \begin{description}
   7.209  
   7.210 @@ -221,14 +226,15 @@
   7.211    no clean way to undo {\ML} declarations, except for reverting to a
   7.212    previously saved state of the whole Isabelle process.  {\ML} input
   7.213    is either read interactively from a TTY, or from a string (usually
   7.214 -  within a theory text), or from a source file (usually associated
   7.215 -  with a theory).
   7.216 +  within a theory text), or from a source file (usually loaded from a
   7.217 +  theory).
   7.218  
   7.219    Whenever the {\ML} toplevel is active, the current Isabelle theory
   7.220    context is passed as an internal reference variable.  Thus {\ML}
   7.221    code may access the theory context during compilation, it may even
   7.222 -  change the value of a theory being under construction --- following
   7.223 -  the usual linearity restrictions (cf.~\secref{sec:context-theory}).
   7.224 +  change the value of a theory being under construction --- while
   7.225 +  observing the usual linearity restrictions
   7.226 +  (cf.~\secref{sec:context-theory}).
   7.227  *}
   7.228  
   7.229  text %mlref {*
   7.230 @@ -247,28 +253,29 @@
   7.231  
   7.232    \item @{ML "the_context ()"} refers to the theory context of the
   7.233    {\ML} toplevel --- at compile time!  {\ML} code needs to take care
   7.234 -  to refer to @{ML "the_context ()"} correctly, recall that evaluation
   7.235 -  of a function body is delayed until actual runtime.  Moreover,
   7.236 -  persistent {\ML} toplevel bindings to an unfinished theory should be
   7.237 -  avoided: code should either project out the desired information
   7.238 -  immediately, or produce an explicit @{ML_type theory_ref} (cf.\
   7.239 -  \secref{sec:context-theory}).
   7.240 +  to refer to @{ML "the_context ()"} correctly.  Recall that
   7.241 +  evaluation of a function body is delayed until actual runtime.
   7.242 +  Moreover, persistent {\ML} toplevel bindings to an unfinished theory
   7.243 +  should be avoided: code should either project out the desired
   7.244 +  information immediately, or produce an explicit @{ML_type
   7.245 +  theory_ref} (cf.\ \secref{sec:context-theory}).
   7.246  
   7.247    \item @{ML "Context.>>"}~@{text f} applies theory transformation
   7.248    @{text f} to the current theory of the {\ML} toplevel.  In order to
   7.249    work as expected, the theory should be still under construction, and
   7.250    the Isar language element that invoked the {\ML} compiler in the
   7.251 -  first place shoule be ready to accept the changed theory value
   7.252 +  first place should be ready to accept the changed theory value
   7.253    (e.g.\ \isakeyword{ML-setup}, but not plain \isakeyword{ML}).
   7.254 -  Otherwise the theory may get destroyed!
   7.255 +  Otherwise the theory becomes stale!
   7.256  
   7.257    \end{description}
   7.258  
   7.259    It is very important to note that the above functions are really
   7.260    restricted to the compile time, even though the {\ML} compiler is
   7.261    invoked at runtime!  The majority of {\ML} code uses explicit
   7.262 -  functional arguments of a theory or proof context, as required.
   7.263 -  Thus it may get run in an arbitrary context later on.
   7.264 +  functional arguments of a theory or proof context instead.  Thus it
   7.265 +  may be invoked for an arbitrary context later on, without having to
   7.266 +  worry about any operational details.
   7.267  
   7.268    \bigskip
   7.269  
   7.270 @@ -283,46 +290,46 @@
   7.271    \begin{description}
   7.272  
   7.273    \item @{ML "Isar.main ()"} invokes the Isar toplevel from {\ML},
   7.274 -  initializing the state to empty toplevel state.
   7.275 +  initializing an empty toplevel state.
   7.276  
   7.277    \item @{ML "Isar.loop ()"} continues the Isar toplevel with the
   7.278 -  current state, after dropping out of the Isar toplevel loop.
   7.279 +  current state, after having dropped out of the Isar toplevel loop.
   7.280  
   7.281    \item @{ML "Isar.state ()"} and @{ML "Isar.exn ()"} get current
   7.282 -  toplevel state and optional error condition, respectively.  This
   7.283 -  only works after dropping out of the Isar toplevel loop.
   7.284 +  toplevel state and error condition, respectively.  This only works
   7.285 +  after having dropped out of the Isar toplevel loop.
   7.286  
   7.287    \item @{ML "Isar.context ()"} produces the proof context from @{ML
   7.288 -  "Isar.state ()"}.
   7.289 +  "Isar.state ()"}, analogous to @{ML Context.proof_of}
   7.290 +  (\secref{sec:generic-context}).
   7.291  
   7.292    \end{description}
   7.293  *}
   7.294  
   7.295  
   7.296 -section {* Theory database *}
   7.297 +section {* Theory database \label{sec:theory-database} *}
   7.298  
   7.299 -text {* The theory database maintains a collection of theories,
   7.300 -  together with some administrative information about the original
   7.301 -  sources, which are held in an external store (i.e.\ a collection of
   7.302 -  directories within the regular file system of the underlying
   7.303 -  platform).
   7.304 +text {*
   7.305 +  The theory database maintains a collection of theories, together
   7.306 +  with some administrative information about their original sources,
   7.307 +  which are held in an external store (i.e.\ some directory within the
   7.308 +  regular file system).
   7.309  
   7.310 -  The theory database is organized as a directed acyclic graph, with
   7.311 -  entries referenced by theory name.  Although some external
   7.312 -  interfaces allow to include a directory specification, this is only
   7.313 -  a hint to the underlying theory loader mechanism: the internal
   7.314 -  theory name space is flat.
   7.315 +  The theory database is organized as a directed acyclic graph;
   7.316 +  entries are referenced by theory name.  Although some additional
   7.317 +  interfaces allow to include a directory specification as well, this
   7.318 +  is only a hint to the underlying theory loader.  The internal theory
   7.319 +  name space is flat!
   7.320  
   7.321    Theory @{text A} is associated with the main theory file @{text
   7.322    A}\verb,.thy,, which needs to be accessible through the theory
   7.323 -  loader path.  A number of optional {\ML} source files may be
   7.324 +  loader path.  Any number of additional {\ML} source files may be
   7.325    associated with each theory, by declaring these dependencies in the
   7.326    theory header as @{text \<USES>}, and loading them consecutively
   7.327    within the theory context.  The system keeps track of incoming {\ML}
   7.328 -  sources and associates them with the current theory.  The special
   7.329 -  theory {\ML} file @{text A}\verb,.ML, is loaded after a theory has
   7.330 -  been concluded, in order to support legacy proof {\ML} proof
   7.331 -  scripts.
   7.332 +  sources and associates them with the current theory.  The file
   7.333 +  @{text A}\verb,.ML, is loaded after a theory has been concluded, in
   7.334 +  order to support legacy proof {\ML} proof scripts.
   7.335  
   7.336    The basic internal actions of the theory database are @{text
   7.337    "update"}, @{text "outdate"}, and @{text "remove"}:
   7.338 @@ -331,31 +338,30 @@
   7.339  
   7.340    \item @{text "update A"} introduces a link of @{text "A"} with a
   7.341    @{text "theory"} value of the same name; it asserts that the theory
   7.342 -  sources are consistent with that value.
   7.343 +  sources are now consistent with that value;
   7.344  
   7.345    \item @{text "outdate A"} invalidates the link of a theory database
   7.346 -  entry to its sources, but retains the present theory value.
   7.347 +  entry to its sources, but retains the present theory value;
   7.348  
   7.349 -  \item @{text "remove A"} removes entry @{text "A"} from the theory
   7.350 +  \item @{text "remove A"} deletes entry @{text "A"} from the theory
   7.351    database.
   7.352    
   7.353    \end{itemize}
   7.354  
   7.355    These actions are propagated to sub- or super-graphs of a theory
   7.356 -  entry in the usual way, in order to preserve global consistency of
   7.357 -  the state of all loaded theories with the sources of the external
   7.358 -  store.  This implies causal dependencies of certain actions: @{text
   7.359 -  "update"} or @{text "outdate"} of an entry will @{text "outdate"}
   7.360 -  all descendants; @{text "remove"} will @{text "remove"} all
   7.361 -  descendants.
   7.362 +  entry as expected, in order to preserve global consistency of the
   7.363 +  state of all loaded theories with the sources of the external store.
   7.364 +  This implies certain causalities between actions: @{text "update"}
   7.365 +  or @{text "outdate"} of an entry will @{text "outdate"} all
   7.366 +  descendants; @{text "remove"} will @{text "remove"} all descendants.
   7.367  
   7.368    \medskip There are separate user-level interfaces to operate on the
   7.369    theory database directly or indirectly.  The primitive actions then
   7.370    just happen automatically while working with the system.  In
   7.371    particular, processing a theory header @{text "\<THEORY> A
   7.372 -  \<IMPORTS> B\<^sub>1 \<dots> B\<^sub>n \<BEGIN>"} ensure that the
   7.373 +  \<IMPORTS> B\<^sub>1 \<dots> B\<^sub>n \<BEGIN>"} ensures that the
   7.374    sub-graph of the collective imports @{text "B\<^sub>1 \<dots> B\<^sub>n"}
   7.375 -  is up-to-date.  Earlier theories are reloaded as required, with
   7.376 +  is up-to-date, too.  Earlier theories are reloaded as required, with
   7.377    @{text update} actions proceeding in topological order according to
   7.378    theory dependencies.  There may be also a wave of implied @{text
   7.379    outdate} actions for derived theory nodes until a stable situation
   7.380 @@ -367,8 +373,6 @@
   7.381    @{index_ML theory: "string -> theory"} \\
   7.382    @{index_ML use_thy: "string -> unit"} \\
   7.383    @{index_ML update_thy: "string -> unit"} \\
   7.384 -  @{index_ML use_thy_only: "string -> unit"} \\
   7.385 -  @{index_ML update_thy_only: "string -> unit"} \\
   7.386    @{index_ML touch_thy: "string -> unit"} \\
   7.387    @{index_ML remove_thy: "string -> unit"} \\[1ex]
   7.388    @{index_ML ThyInfo.begin_theory}@{verbatim ": ... -> bool -> theory"} \\
   7.389 @@ -381,8 +385,8 @@
   7.390    \begin{description}
   7.391  
   7.392    \item @{ML theory}~@{text A} retrieves the theory value presently
   7.393 -  associated with @{text A}.  The result is not necessarily
   7.394 -  up-to-date!
   7.395 +  associated with name @{text A}.  Note that the result might be
   7.396 +  outdated.
   7.397  
   7.398    \item @{ML use_thy}~@{text A} loads theory @{text A} if it is absent
   7.399    or out-of-date.  It ensures that all parent theories are available
   7.400 @@ -390,20 +394,12 @@
   7.401    present.
   7.402  
   7.403    \item @{ML update_thy} is similar to @{ML use_thy}, but ensures that
   7.404 -  the @{text A} and all of its ancestors are fully up-to-date.
   7.405 +  theory @{text A} and all ancestors are fully up-to-date.
   7.406  
   7.407 -  \item @{ML use_thy_only}~@{text A} is like @{ML use_thy}~@{text A},
   7.408 -  but refrains from loading the attached @{text A}\verb,.ML, file.
   7.409 -  This is occasionally useful in replaying legacy {\ML} proof scripts
   7.410 -  by hand.
   7.411 -  
   7.412 -  \item @{ML update_thy_only} is analogous to @{ML use_thy_only}, but
   7.413 -  proceeds like @{ML update_thy} for ancestors.
   7.414 +  \item @{ML touch_thy}~@{text A} performs and @{text outdate} action
   7.415 +  on theory @{text A} and all descendants.
   7.416  
   7.417 -  \item @{ML touch_thy}~@{text A} performs @{text outdate} action on
   7.418 -  theory @{text A} and all of its descendants.
   7.419 -
   7.420 -  \item @{ML remove_thy}~@{text A} removes @{text A} and all of its
   7.421 +  \item @{ML remove_thy}~@{text A} deletes theory @{text A} and all
   7.422    descendants from the theory database.
   7.423  
   7.424    \item @{ML ThyInfo.begin_theory} is the basic operation behind a
   7.425 @@ -414,28 +410,30 @@
   7.426    normally not invoked directly.
   7.427  
   7.428    \item @{ML ThyInfo.end_theory} concludes the loading of a theory
   7.429 -  proper; an attached theory {\ML} file may be still loaded later on.
   7.430 -  This is {\ML} functions is normally not invoked directly.
   7.431 +  proper.  An attached theory {\ML} file may be still loaded later on.
   7.432 +  This is function is normally not invoked directly.
   7.433  
   7.434 -  \item @{ML ThyInfo.register_theory}~{text thy} registers an existing
   7.435 -  theory value with the theory loader database.  There is no
   7.436 -  management of associated sources; this is mainly for bootstrapping.
   7.437 +  \item @{ML ThyInfo.register_theory}~@{text "text thy"} registers an
   7.438 +  existing theory value with the theory loader database.  There is no
   7.439 +  management of associated sources.
   7.440  
   7.441    \item @{ML "ThyInfo.add_hook"}~@{text f} registers function @{text
   7.442    f} as a hook for theory database actions.  The function will be
   7.443    invoked with the action and theory name being involved; thus derived
   7.444    actions may be performed in associated system components, e.g.\
   7.445 -  maintaining the state of an editor for theory sources.
   7.446 +  maintaining the state of an editor for the theory sources.
   7.447  
   7.448    The kind and order of actions occurring in practice depends both on
   7.449    user interactions and the internal process of resolving theory
   7.450    imports.  Hooks should not rely on a particular policy here!  Any
   7.451 -  exceptions raised by the hook are ignored by the theory database.
   7.452 +  exceptions raised by the hook are ignored.
   7.453  
   7.454    \end{description}
   7.455  *}
   7.456  
   7.457  
   7.458 -(* FIXME section {* Sessions and document preparation *} *)
   7.459 +section {* Sessions and document preparation *}
   7.460 +
   7.461 +text FIXME
   7.462  
   7.463  end
     8.1 --- a/doc-src/IsarImplementation/Thy/locale.thy	Thu Aug 31 18:27:40 2006 +0200
     8.2 +++ b/doc-src/IsarImplementation/Thy/locale.thy	Thu Aug 31 22:55:49 2006 +0200
     8.3 @@ -9,8 +9,18 @@
     8.4  
     8.5  text FIXME
     8.6  
     8.7 -section {* Locales *}
     8.8 +
     8.9 +section {* Type-checking specifications *}
    8.10  
    8.11  text FIXME
    8.12  
    8.13 +
    8.14 +section {* Localized theory specifications *}
    8.15 +
    8.16 +text {*
    8.17 +  FIXME
    8.18 +
    8.19 +  \glossary{Local theory}{FIXME}
    8.20 +*}
    8.21 +
    8.22  end
     9.1 --- a/doc-src/IsarImplementation/Thy/logic.thy	Thu Aug 31 18:27:40 2006 +0200
     9.2 +++ b/doc-src/IsarImplementation/Thy/logic.thy	Thu Aug 31 22:55:49 2006 +0200
     9.3 @@ -5,45 +5,42 @@
     9.4  
     9.5  chapter {* Primitive logic *}
     9.6  
     9.7 -section {* Syntax *}
     9.8 +section {* Variable names *}
     9.9  
    9.10 -subsection {* Variable names *}
    9.11 +text FIXME
    9.12 +
    9.13 +
    9.14 +section {* Types \label{sec:types} *}
    9.15  
    9.16  text {*
    9.17 -  FIXME
    9.18 +  \glossary{Type class}{FIXME}
    9.19 +
    9.20 +  \glossary{Type arity}{FIXME}
    9.21 +
    9.22 +  \glossary{Sort}{FIXME}
    9.23 +
    9.24 +  FIXME classes and sorts
    9.25 +
    9.26 +
    9.27 +  \glossary{Type}{FIXME}
    9.28 +
    9.29 +  \glossary{Type constructor}{FIXME}
    9.30 +
    9.31 +  \glossary{Type variable}{FIXME}
    9.32 +
    9.33 +  FIXME simple types
    9.34  *}
    9.35  
    9.36  
    9.37 -subsection {* Simply-typed lambda calculus *}
    9.38 -
    9.39 -text {*
    9.40 -
    9.41 -FIXME
    9.42 -
    9.43 -\glossary{Type}{FIXME}
    9.44 -\glossary{Term}{FIXME}
    9.45 -
    9.46 -*}
    9.47 -
    9.48 -subsection {* The order-sorted algebra of types *}
    9.49 +section {* Terms \label{sec:terms} *}
    9.50  
    9.51  text {*
    9.52 -
    9.53 -FIXME
    9.54 -
    9.55 -\glossary{Type constructor}{FIXME}
    9.56 +  \glossary{Term}{FIXME}
    9.57  
    9.58 -\glossary{Type class}{FIXME}
    9.59 -
    9.60 -\glossary{Type arity}{FIXME}
    9.61 -
    9.62 -\glossary{Sort}{FIXME}
    9.63 -
    9.64 +  FIXME de-Bruijn representation of lambda terms
    9.65  *}
    9.66  
    9.67  
    9.68 -subsection {* Type-inference and schematic polymorphism *}
    9.69 -
    9.70  text {*
    9.71  
    9.72  FIXME
    9.73 @@ -55,21 +52,7 @@
    9.74  *}
    9.75  
    9.76  
    9.77 -section {* Theory *}
    9.78 -
    9.79 -text {*
    9.80 -
    9.81 -FIXME
    9.82 -
    9.83 -\glossary{Constant}{Essentially a \seeglossary{fixed variable} of the
    9.84 -theory context, but slightly more flexible since it may be used at
    9.85 -different type-instances, due to \seeglossary{schematic
    9.86 -polymorphism.}}
    9.87 -
    9.88 -*}
    9.89 -
    9.90 -
    9.91 -section {* Deduction *}
    9.92 +section {* Theorems \label{sec:thms} *}
    9.93  
    9.94  text {*
    9.95  
    9.96 @@ -139,8 +122,21 @@
    9.97  text FIXME
    9.98  
    9.99  
   9.100 -section {* Proof terms *}
   9.101 +section {* Low-level specifications *}
   9.102 +
   9.103 +text {*
   9.104 +
   9.105 +FIXME
   9.106  
   9.107 -text FIXME
   9.108 +\glossary{Constant}{Essentially a \seeglossary{fixed variable} of the
   9.109 +theory context, but slightly more flexible since it may be used at
   9.110 +different type-instances, due to \seeglossary{schematic
   9.111 +polymorphism.}}
   9.112 +
   9.113 +\glossary{Axiom}{FIXME}
   9.114 +
   9.115 +\glossary{Primitive definition}{FIXME}
   9.116 +
   9.117 +*}
   9.118  
   9.119  end
    10.1 --- a/doc-src/IsarImplementation/Thy/prelim.thy	Thu Aug 31 18:27:40 2006 +0200
    10.2 +++ b/doc-src/IsarImplementation/Thy/prelim.thy	Thu Aug 31 22:55:49 2006 +0200
    10.3 @@ -8,19 +8,20 @@
    10.4  section {* Contexts \label{sec:context} *}
    10.5  
    10.6  text {*
    10.7 -  A logical context represents the background that is taken for
    10.8 -  granted when formulating statements and composing proofs.  It acts
    10.9 -  as a medium to produce formal content, depending on earlier material
   10.10 -  (declarations, results etc.).
   10.11 +  A logical context represents the background that is required for
   10.12 +  formulating statements and composing proofs.  It acts as a medium to
   10.13 +  produce formal content, depending on earlier material (declarations,
   10.14 +  results etc.).
   10.15  
   10.16 -  In particular, derivations within the primitive Pure logic can be
   10.17 -  described as a judgment @{text "\<Gamma> \<turnstile>\<^sub>\<Theta> \<phi>"}, meaning that a
   10.18 +  For example, derivations within the Isabelle/Pure logic can be
   10.19 +  described as a judgment @{text "\<Gamma> \<turnstile>\<^sub>\<Theta> \<phi>"}, which means that a
   10.20    proposition @{text "\<phi>"} is derivable from hypotheses @{text "\<Gamma>"}
   10.21    within the theory @{text "\<Theta>"}.  There are logical reasons for
   10.22 -  keeping @{text "\<Theta>"} and @{text "\<Gamma>"} separate: theories support type
   10.23 -  constructors and schematic polymorphism of constants and axioms,
   10.24 -  while the inner calculus of @{text "\<Gamma> \<turnstile> \<phi>"} is limited to Simple
   10.25 -  Type Theory (with fixed type variables in the assumptions).
   10.26 +  keeping @{text "\<Theta>"} and @{text "\<Gamma>"} separate: theories can be
   10.27 +  liberal about supporting type constructors and schematic
   10.28 +  polymorphism of constants and axioms, while the inner calculus of
   10.29 +  @{text "\<Gamma> \<turnstile> \<phi>"} is strictly limited to Simple Type Theory (with
   10.30 +  fixed type variables in the assumptions).
   10.31  
   10.32    \medskip Contexts and derivations are linked by the following key
   10.33    principles:
   10.34 @@ -28,45 +29,46 @@
   10.35    \begin{itemize}
   10.36  
   10.37    \item Transfer: monotonicity of derivations admits results to be
   10.38 -  transferred into a larger context, i.e.\ @{text "\<Gamma> \<turnstile>\<^sub>\<Theta> \<phi>"}
   10.39 -  implies @{text "\<Gamma>' \<turnstile>\<^sub>\<Theta>\<^sub>' \<phi>"} for contexts @{text "\<Theta>' \<supseteq>
   10.40 -  \<Theta>"} and @{text "\<Gamma>' \<supseteq> \<Gamma>"}.
   10.41 +  transferred into a \emph{larger} context, i.e.\ @{text "\<Gamma> \<turnstile>\<^sub>\<Theta>
   10.42 +  \<phi>"} implies @{text "\<Gamma>' \<turnstile>\<^sub>\<Theta>\<^sub>' \<phi>"} for contexts @{text "\<Theta>'
   10.43 +  \<supseteq> \<Theta>"} and @{text "\<Gamma>' \<supseteq> \<Gamma>"}.
   10.44  
   10.45    \item Export: discharge of hypotheses admits results to be exported
   10.46 -  into a smaller context, i.e.\ @{text "\<Gamma>' \<turnstile>\<^sub>\<Theta> \<phi>"} implies
   10.47 -  @{text "\<Gamma> \<turnstile>\<^sub>\<Theta> \<Delta> \<Longrightarrow> \<phi>"} where @{text "\<Gamma>' \<supseteq> \<Gamma>"} and @{text "\<Delta> =
   10.48 -  \<Gamma>' - \<Gamma>"}.  Note that @{text "\<Theta>"} remains unchanged here, only the
   10.49 -  @{text "\<Gamma>"} part is affected.
   10.50 +  into a \emph{smaller} context, i.e.\ @{text "\<Gamma>' \<turnstile>\<^sub>\<Theta> \<phi>"}
   10.51 +  implies @{text "\<Gamma> \<turnstile>\<^sub>\<Theta> \<Delta> \<Longrightarrow> \<phi>"} where @{text "\<Gamma>' \<supseteq> \<Gamma>"} and
   10.52 +  @{text "\<Delta> = \<Gamma>' - \<Gamma>"}.  Note that @{text "\<Theta>"} remains unchanged here,
   10.53 +  only the @{text "\<Gamma>"} part is affected.
   10.54  
   10.55    \end{itemize}
   10.56  
   10.57 -  \medskip Isabelle/Isar provides two different notions of abstract
   10.58 -  containers called \emph{theory context} and \emph{proof context},
   10.59 -  respectively.  These model the main characteristics of the primitive
   10.60 -  @{text "\<Theta>"} and @{text "\<Gamma>"} above, without subscribing to any
   10.61 -  particular kind of content yet.  Instead, contexts merely impose a
   10.62 -  certain policy of managing arbitrary \emph{context data}.  The
   10.63 -  system provides strongly typed mechanisms to declare new kinds of
   10.64 +  \medskip By modeling the main characteristics of the primitive
   10.65 +  @{text "\<Theta>"} and @{text "\<Gamma>"} above, and abstracting over any
   10.66 +  particular logical content, we arrive at the fundamental notions of
   10.67 +  \emph{theory context} and \emph{proof context} in Isabelle/Isar.
   10.68 +  These implement a certain policy to manage arbitrary \emph{context
   10.69 +  data}.  There is a strongly-typed mechanism to declare new kinds of
   10.70    data at compile time.
   10.71  
   10.72 -  Thus the internal bootstrap process of Isabelle/Pure eventually
   10.73 -  reaches a stage where certain data slots provide the logical content
   10.74 -  of @{text "\<Theta>"} and @{text "\<Gamma>"} sketched above, but this does not
   10.75 -  stop there!  Various additional data slots support all kinds of
   10.76 -  mechanisms that are not necessarily part of the core logic.
   10.77 +  The internal bootstrap process of Isabelle/Pure eventually reaches a
   10.78 +  stage where certain data slots provide the logical content of @{text
   10.79 +  "\<Theta>"} and @{text "\<Gamma>"} sketched above, but this does not stop there!
   10.80 +  Various additional data slots support all kinds of mechanisms that
   10.81 +  are not necessarily part of the core logic.
   10.82  
   10.83    For example, there would be data for canonical introduction and
   10.84    elimination rules for arbitrary operators (depending on the
   10.85    object-logic and application), which enables users to perform
   10.86 -  standard proof steps implicitly (cf.\ the @{text "rule"} method).
   10.87 +  standard proof steps implicitly (cf.\ the @{text "rule"} method
   10.88 +  \cite{isabelle-isar-ref}).
   10.89  
   10.90 -  Isabelle is able to bring forth more and more concepts successively.
   10.91 -  In particular, an object-logic like Isabelle/HOL continues the
   10.92 -  Isabelle/Pure setup by adding specific components for automated
   10.93 -  reasoning (classical reasoner, tableau prover, structured induction
   10.94 -  etc.) and derived specification mechanisms (inductive predicates,
   10.95 -  recursive functions etc.).  All of this is based on the generic data
   10.96 -  management by theory and proof contexts.
   10.97 +  \medskip Thus Isabelle/Isar is able to bring forth more and more
   10.98 +  concepts successively.  In particular, an object-logic like
   10.99 +  Isabelle/HOL continues the Isabelle/Pure setup by adding specific
  10.100 +  components for automated reasoning (classical reasoner, tableau
  10.101 +  prover, structured induction etc.) and derived specification
  10.102 +  mechanisms (inductive predicates, recursive functions etc.).  All of
  10.103 +  this is ultimately based on the generic data management by theory
  10.104 +  and proof contexts introduced here.
  10.105  *}
  10.106  
  10.107  
  10.108 @@ -75,31 +77,27 @@
  10.109  text {*
  10.110    \glossary{Theory}{FIXME}
  10.111  
  10.112 -  Each theory is explicitly named and holds a unique identifier.
  10.113 -  There is a separate \emph{theory reference} for pointing backwards
  10.114 -  to the enclosing theory context of derived entities.  Theories are
  10.115 -  related by a (nominal) sub-theory relation, which corresponds to the
  10.116 -  canonical dependency graph: each theory is derived from a certain
  10.117 -  sub-graph of ancestor theories.  The @{text "merge"} of two theories
  10.118 -  refers to the least upper bound, which actually degenerates into
  10.119 -  absorption of one theory into the other, due to the nominal
  10.120 -  sub-theory relation this.
  10.121 +  A \emph{theory} is a data container with explicit named and unique
  10.122 +  identifier.  Theories are related by a (nominal) sub-theory
  10.123 +  relation, which corresponds to the dependency graph of the original
  10.124 +  construction; each theory is derived from a certain sub-graph of
  10.125 +  ancestor theories.
  10.126 +
  10.127 +  The @{text "merge"} operation produces the least upper bound of two
  10.128 +  theories, which actually degenerates into absorption of one theory
  10.129 +  into the other (due to the nominal sub-theory relation).
  10.130  
  10.131    The @{text "begin"} operation starts a new theory by importing
  10.132    several parent theories and entering a special @{text "draft"} mode,
  10.133    which is sustained until the final @{text "end"} operation.  A draft
  10.134 -  mode theory acts like a linear type, where updates invalidate
  10.135 -  earlier drafts, but theory reference values will be propagated
  10.136 -  automatically.  Thus derived entities that ``belong'' to a draft
  10.137 -  might be transferred spontaneously to a larger context.  An
  10.138 -  invalidated draft is called ``stale''.
  10.139 +  theory acts like a linear type, where updates invalidate earlier
  10.140 +  versions.  An invalidated draft is called ``stale''.
  10.141  
  10.142    The @{text "checkpoint"} operation produces an intermediate stepping
  10.143 -  stone that will survive the next update unscathed: both the original
  10.144 -  and the changed theory remain valid and are related by the
  10.145 -  sub-theory relation.  Checkpointing essentially recovers purely
  10.146 -  functional theory values, at the expense of some extra internal
  10.147 -  bookkeeping.
  10.148 +  stone that will survive the next update: both the original and the
  10.149 +  changed theory remain valid and are related by the sub-theory
  10.150 +  relation.  Checkpointing essentially recovers purely functional
  10.151 +  theory values, at the expense of some extra internal bookkeeping.
  10.152  
  10.153    The @{text "copy"} operation produces an auxiliary version that has
  10.154    the same data content, but is unrelated to the original: updates of
  10.155 @@ -107,11 +105,12 @@
  10.156    relation hold.
  10.157  
  10.158    \medskip The example in \figref{fig:ex-theory} below shows a theory
  10.159 -  graph derived from @{text "Pure"}. Theory @{text "Length"} imports
  10.160 -  @{text "Nat"} and @{text "List"}.  The theory body consists of a
  10.161 -  sequence of updates, working mostly on drafts.  Intermediate
  10.162 -  checkpoints may occur as well, due to the history mechanism provided
  10.163 -  by the Isar top-level, cf.\ \secref{sec:isar-toplevel}.
  10.164 +  graph derived from @{text "Pure"}, with theory @{text "Length"}
  10.165 +  importing @{text "Nat"} and @{text "List"}.  The body of @{text
  10.166 +  "Length"} consists of a sequence of updates, working mostly on
  10.167 +  drafts.  Intermediate checkpoints may occur as well, due to the
  10.168 +  history mechanism provided by the Isar top-level, cf.\
  10.169 +  \secref{sec:isar-toplevel}.
  10.170  
  10.171    \begin{figure}[htb]
  10.172    \begin{center}
  10.173 @@ -132,9 +131,19 @@
  10.174          &            & $\vdots$~~ \\
  10.175          &            & \multicolumn{3}{l}{~~$\isarkeyword{end}$} \\
  10.176    \end{tabular}
  10.177 -  \caption{Theory definition depending on ancestors}\label{fig:ex-theory}
  10.178 +  \caption{A theory definition depending on ancestors}\label{fig:ex-theory}
  10.179    \end{center}
  10.180    \end{figure}
  10.181 +
  10.182 +  \medskip There is a separate notion of \emph{theory reference} for
  10.183 +  maintaining a live link to an evolving theory context: updates on
  10.184 +  drafts are propagated automatically.  The dynamic stops after an
  10.185 +  explicit @{text "end"} only.
  10.186 +
  10.187 +  Derived entities may store a theory reference in order to indicate
  10.188 +  the context they belong to.  This implicitly assumes monotonic
  10.189 +  reasoning, because the referenced context may become larger without
  10.190 +  further notice.
  10.191  *}
  10.192  
  10.193  text %mlref {*
  10.194 @@ -151,9 +160,9 @@
  10.195  
  10.196    \begin{description}
  10.197  
  10.198 -  \item @{ML_type theory} represents theory contexts.  This is a
  10.199 -  linear type!  Most operations destroy the old version, which then
  10.200 -  becomes ``stale''.
  10.201 +  \item @{ML_type theory} represents theory contexts.  This is
  10.202 +  essentially a linear type!  Most operations destroy the original
  10.203 +  version, which then becomes ``stale''.
  10.204  
  10.205    \item @{ML "Theory.subthy"}~@{text "(thy\<^sub>1, thy\<^sub>2)"}
  10.206    compares theories according to the inherent graph structure of the
  10.207 @@ -169,18 +178,18 @@
  10.208    update will result in two related, valid theories.
  10.209  
  10.210    \item @{ML "Theory.copy"}~@{text "thy"} produces a variant of @{text
  10.211 -  "thy"} that holds a copy of the same data.  The copy is not related
  10.212 -  to the original, which is not touched at all.
  10.213 +  "thy"} that holds a copy of the same data.  The result is not
  10.214 +  related to the original; the original is unchanched.
  10.215  
  10.216 -  \item @{ML_type theory_ref} represents a sliding reference to a
  10.217 -  valid theory --- updates on the original are propagated
  10.218 +  \item @{ML_type theory_ref} represents a sliding reference to an
  10.219 +  always valid theory; updates on the original are propagated
  10.220    automatically.
  10.221  
  10.222    \item @{ML "Theory.self_ref"}~@{text "thy"} and @{ML
  10.223    "Theory.deref"}~@{text "thy_ref"} convert between @{ML_type
  10.224    "theory"} and @{ML_type "theory_ref"}.  As the referenced theory
  10.225    evolves monotonically over time, later invocations of @{ML
  10.226 -  "Theory.deref"} may refer to larger contexts.
  10.227 +  "Theory.deref"} may refer to a larger context.
  10.228  
  10.229    \end{description}
  10.230  *}
  10.231 @@ -198,28 +207,28 @@
  10.232  
  10.233    A proof context is a container for pure data with a back-reference
  10.234    to the theory it belongs to.  The @{text "init"} operation creates a
  10.235 -  proof context derived from a given theory.  Modifications to draft
  10.236 -  theories are propagated to the proof context as usual, but there is
  10.237 -  also an explicit @{text "transfer"} operation to force
  10.238 -  resynchronization with more substantial updates to the underlying
  10.239 -  theory.  The actual context data does not require any special
  10.240 -  bookkeeping, thanks to the lack of destructive features.
  10.241 +  proof context from a given theory.  Modifications to draft theories
  10.242 +  are propagated to the proof context as usual, but there is also an
  10.243 +  explicit @{text "transfer"} operation to force resynchronization
  10.244 +  with more substantial updates to the underlying theory.  The actual
  10.245 +  context data does not require any special bookkeeping, thanks to the
  10.246 +  lack of destructive features.
  10.247  
  10.248    Entities derived in a proof context need to record inherent logical
  10.249    requirements explicitly, since there is no separate context
  10.250    identification as for theories.  For example, hypotheses used in
  10.251 -  primitive derivations (cf.\ \secref{sec:thm}) are recorded
  10.252 +  primitive derivations (cf.\ \secref{sec:thms}) are recorded
  10.253    separately within the sequent @{text "\<Gamma> \<turnstile> \<phi>"}, just to make double
  10.254    sure.  Results could still leak into an alien proof context do to
  10.255    programming errors, but Isabelle/Isar includes some extra validity
  10.256    checks in critical positions, notably at the end of sub-proof.
  10.257  
  10.258 -  Proof contexts may be produced in arbitrary ways, although the
  10.259 -  common discipline is to follow block structure as a mental model: a
  10.260 -  given context is extended consecutively, and results are exported
  10.261 -  back into the original context.  Note that the Isar proof states
  10.262 -  model block-structured reasoning explicitly, using a stack of proof
  10.263 -  contexts, cf.\ \secref{isar-proof-state}.
  10.264 +  Proof contexts may be manipulated arbitrarily, although the common
  10.265 +  discipline is to follow block structure as a mental model: a given
  10.266 +  context is extended consecutively, and results are exported back
  10.267 +  into the original context.  Note that the Isar proof states model
  10.268 +  block-structured reasoning explicitly, using a stack of proof
  10.269 +  contexts internally, cf.\ \secref{sec:isar-proof-state}.
  10.270  *}
  10.271  
  10.272  text %mlref {*
  10.273 @@ -240,7 +249,8 @@
  10.274    derived from @{text "thy"}, initializing all data.
  10.275  
  10.276    \item @{ML ProofContext.theory_of}~@{text "ctxt"} selects the
  10.277 -  background theory from @{text "ctxt"}.
  10.278 +  background theory from @{text "ctxt"}, dereferencing its internal
  10.279 +  @{ML_type theory_ref}.
  10.280  
  10.281    \item @{ML ProofContext.transfer}~@{text "thy ctxt"} promotes the
  10.282    background theory of @{text "ctxt"} to the super theory @{text
  10.283 @@ -250,12 +260,11 @@
  10.284  *}
  10.285  
  10.286  
  10.287 -
  10.288 -subsection {* Generic contexts *}
  10.289 +subsection {* Generic contexts \label{sec:generic-context} *}
  10.290  
  10.291  text {*
  10.292    A generic context is the disjoint sum of either a theory or proof
  10.293 -  context.  Occasionally, this simplifies uniform treatment of generic
  10.294 +  context.  Occasionally, this enables uniform treatment of generic
  10.295    context data, typically extra-logical information.  Operations on
  10.296    generic contexts include the usual injections, partial selections,
  10.297    and combinators for lifting operations on either component of the
  10.298 @@ -263,8 +272,8 @@
  10.299  
  10.300    Moreover, there are total operations @{text "theory_of"} and @{text
  10.301    "proof_of"} to convert a generic context into either kind: a theory
  10.302 -  can always be selected, while a proof context may have to be
  10.303 -  constructed by an ad-hoc @{text "init"} operation.
  10.304 +  can always be selected from the sum, while a proof context might
  10.305 +  have to be constructed by an ad-hoc @{text "init"} operation.
  10.306  *}
  10.307  
  10.308  text %mlref {*
  10.309 @@ -277,8 +286,8 @@
  10.310    \begin{description}
  10.311  
  10.312    \item @{ML_type Context.generic} is the direct sum of @{ML_type
  10.313 -  "theory"} and @{ML_type "Proof.context"}, with datatype constructors
  10.314 -  @{ML "Context.Theory"} and @{ML "Context.Proof"}.
  10.315 +  "theory"} and @{ML_type "Proof.context"}, with the datatype
  10.316 +  constructors @{ML "Context.Theory"} and @{ML "Context.Proof"}.
  10.317  
  10.318    \item @{ML Context.theory_of}~@{text "context"} always produces a
  10.319    theory from the generic @{text "context"}, using @{ML
  10.320 @@ -286,8 +295,8 @@
  10.321  
  10.322    \item @{ML Context.proof_of}~@{text "context"} always produces a
  10.323    proof context from the generic @{text "context"}, using @{ML
  10.324 -  "ProofContext.init"} as required.  Note that this re-initializes the
  10.325 -  context data with each invocation.
  10.326 +  "ProofContext.init"} as required (note that this re-initializes the
  10.327 +  context data with each invocation).
  10.328  
  10.329    \end{description}
  10.330  *}
  10.331 @@ -295,23 +304,23 @@
  10.332  subsection {* Context data *}
  10.333  
  10.334  text {*
  10.335 -  Both theory and proof contexts manage arbitrary data, which is the
  10.336 -  main purpose of contexts in the first place.  Data can be declared
  10.337 -  incrementally at compile --- Isabelle/Pure and major object-logics
  10.338 -  are bootstrapped that way.
  10.339 +  The main purpose of theory and proof contexts is to manage arbitrary
  10.340 +  data.  New data types can be declared incrementally at compile time.
  10.341 +  There are separate declaration mechanisms for any of the three kinds
  10.342 +  of contexts: theory, proof, generic.
  10.343  
  10.344    \paragraph{Theory data} may refer to destructive entities, which are
  10.345 -  maintained in correspondence to the linear evolution of theory
  10.346 -  values, or explicit copies.\footnote{Most existing instances of
  10.347 -  destructive theory data are merely historical relics (e.g.\ the
  10.348 -  destructive theorem storage, and destructive hints for the
  10.349 -  Simplifier and Classical rules).}  A theory data declaration needs
  10.350 -  to implement the following specification:
  10.351 +  maintained in direct correspondence to the linear evolution of
  10.352 +  theory values, including explicit copies.\footnote{Most existing
  10.353 +  instances of destructive theory data are merely historical relics
  10.354 +  (e.g.\ the destructive theorem storage, and destructive hints for
  10.355 +  the Simplifier and Classical rules).}  A theory data declaration
  10.356 +  needs to implement the following specification (depending on type
  10.357 +  @{text "T"}):
  10.358  
  10.359    \medskip
  10.360    \begin{tabular}{ll}
  10.361    @{text "name: string"} \\
  10.362 -  @{text "T"} & the ML type \\
  10.363    @{text "empty: T"} & initial value \\
  10.364    @{text "copy: T \<rightarrow> T"} & refresh impure data \\
  10.365    @{text "extend: T \<rightarrow> T"} & re-initialize on import \\
  10.366 @@ -326,27 +335,26 @@
  10.367    should also include the functionality of @{text "copy"} for impure
  10.368    data.
  10.369  
  10.370 -  \paragraph{Proof context data} is purely functional.  It is declared
  10.371 -  by implementing the following specification:
  10.372 +  \paragraph{Proof context data} is purely functional.  A declaration
  10.373 +  needs to implement the following specification:
  10.374  
  10.375    \medskip
  10.376    \begin{tabular}{ll}
  10.377    @{text "name: string"} \\
  10.378 -  @{text "T"} & the ML type \\
  10.379    @{text "init: theory \<rightarrow> T"} & produce initial value \\
  10.380    @{text "print: T \<rightarrow> unit"} & diagnostic output \\
  10.381    \end{tabular}
  10.382    \medskip
  10.383  
  10.384    \noindent The @{text "init"} operation is supposed to produce a pure
  10.385 -  value from the given background theory.  The rest is analogous to
  10.386 -  (pure) theory data.
  10.387 +  value from the given background theory.  The remainder is analogous
  10.388 +  to theory data.
  10.389  
  10.390 -  \paragraph{Generic data} provides a hybrid interface for both kinds.
  10.391 -  The declaration is essentially the same as for pure theory data,
  10.392 -  without @{text "copy"} (it is always the identity).  The @{text
  10.393 -  "init"} operation for proof contexts selects the current data value
  10.394 -  from the background theory.
  10.395 +  \paragraph{Generic data} provides a hybrid interface for both theory
  10.396 +  and proof data.  The declaration is essentially the same as for
  10.397 +  (pure) theory data, without @{text "copy"}, though.  The @{text
  10.398 +  "init"} operation for proof contexts merely selects the current data
  10.399 +  value from the background theory.
  10.400  
  10.401    \bigskip In any case, a data declaration of type @{text "T"} results
  10.402    in the following interface:
  10.403 @@ -366,9 +374,9 @@
  10.404    other operations provide access for the particular kind of context
  10.405    (theory, proof, or generic context).  Note that this is a safe
  10.406    interface: there is no other way to access the corresponding data
  10.407 -  slot within a context.  By keeping these operations private, a
  10.408 -  component may maintain abstract values authentically, without other
  10.409 -  components interfering.
  10.410 +  slot of a context.  By keeping these operations private, a component
  10.411 +  may maintain abstract values authentically, without other components
  10.412 +  interfering.
  10.413  *}
  10.414  
  10.415  text %mlref {*
  10.416 @@ -382,8 +390,8 @@
  10.417  
  10.418    \item @{ML_functor TheoryDataFun}@{text "(spec)"} declares data for
  10.419    type @{ML_type theory} according to the specification provided as
  10.420 -  argument structure.  The result structure provides init and access
  10.421 -  operations as described above.
  10.422 +  argument structure.  The resulting structure provides data init and
  10.423 +  access operations as described above.
  10.424  
  10.425    \item @{ML_functor ProofDataFun}@{text "(spec)"} is analogous for
  10.426    type @{ML_type Proof.context}.
  10.427 @@ -397,77 +405,95 @@
  10.428  
  10.429  section {* Named entities *}
  10.430  
  10.431 -text {* Named entities of different kinds (logical constant, type,
  10.432 -type class, theorem, method etc.) live in separate name spaces.  It is
  10.433 -usually clear from the occurrence of a name which kind of entity it
  10.434 -refers to.  For example, proof method @{text "foo"} vs.\ theorem
  10.435 -@{text "foo"} vs.\ logical constant @{text "foo"} are easily
  10.436 -distinguished by means of the syntactic context.  A notable exception
  10.437 -are logical identifiers within a term (\secref{sec:terms}): constants,
  10.438 -fixed variables, and bound variables all share the same identifier
  10.439 -syntax, but are distinguished by their scope.
  10.440 +text {*
  10.441 +  By general convention, each kind of formal entities (logical
  10.442 +  constant, type, type class, theorem, method etc.) lives in a
  10.443 +  separate name space.  It is usually clear from the syntactic context
  10.444 +  of a name, which kind of entity it refers to.  For example, proof
  10.445 +  method @{text "foo"} vs.\ theorem @{text "foo"} vs.\ logical
  10.446 +  constant @{text "foo"} are easily distinguished thanks to the design
  10.447 +  of the concrete outer syntax.  A notable exception are logical
  10.448 +  identifiers within a term (\secref{sec:terms}): constants, fixed
  10.449 +  variables, and bound variables all share the same identifier syntax,
  10.450 +  but are distinguished by their scope.
  10.451 +
  10.452 +  Name spaces are organized uniformly, as a collection of qualified
  10.453 +  names consisting of a sequence of basic name components separated by
  10.454 +  dots: @{text "Bar.bar.foo"}, @{text "Bar.foo"}, and @{text "foo"}
  10.455 +  are examples for qualified names.
  10.456  
  10.457 -Each name space is organized as a collection of \emph{qualified
  10.458 -names}, which consist of a sequence of basic name components separated
  10.459 -by dots: @{text "Bar.bar.foo"}, @{text "Bar.foo"}, and @{text "foo"}
  10.460 -are examples for valid qualified names.  Name components are
  10.461 -subdivided into \emph{symbols}, which constitute the smallest textual
  10.462 -unit in Isabelle --- raw characters are normally not encountered
  10.463 -directly. *}
  10.464 +  Despite the independence of names of different kinds, certain naming
  10.465 +  conventions may relate them to each other.  For example, a constant
  10.466 +  @{text "foo"} could be accompanied with theorems @{text
  10.467 +  "foo.intro"}, @{text "foo.elim"}, @{text "foo.simps"} etc.  The same
  10.468 +  could happen for a type @{text "foo"}, but this is apt to cause
  10.469 +  clashes in the theorem name space!  To avoid this, there is an
  10.470 +  additional convention to add a suffix that determines the original
  10.471 +  kind.  For example, constant @{text "foo"} could associated with
  10.472 +  theorem @{text "foo.intro"}, type @{text "foo"} with theorem @{text
  10.473 +  "foo_type.intro"}, and type class @{text "foo"} with @{text
  10.474 +  "foo_class.intro"}.
  10.475 +
  10.476 +  \medskip Name components are subdivided into \emph{symbols}, which
  10.477 +  constitute the smallest textual unit in Isabelle --- raw characters
  10.478 +  are normally not encountered.
  10.479 +*}
  10.480  
  10.481  
  10.482  subsection {* Strings of symbols *}
  10.483  
  10.484 -text {* Isabelle strings consist of a sequence of
  10.485 -symbols\glossary{Symbol}{The smallest unit of text in Isabelle,
  10.486 -subsumes plain ASCII characters as well as an infinite collection of
  10.487 -named symbols (for greek, math etc.).}, which are either packed as an
  10.488 -actual @{text "string"}, or represented as a list.  Each symbol is in
  10.489 -itself a small string of the following form:
  10.490 +text {*
  10.491 +  Isabelle strings consist of a sequence of
  10.492 +  symbols\glossary{Symbol}{The smallest unit of text in Isabelle,
  10.493 +  subsumes plain ASCII characters as well as an infinite collection of
  10.494 +  named symbols (for greek, math etc.).}, which are either packed as
  10.495 +  an actual @{text "string"}, or represented as a list.  Each symbol
  10.496 +  is in itself a small string of the following form:
  10.497  
  10.498 -\begin{enumerate}
  10.499 +  \begin{enumerate}
  10.500  
  10.501 -\item either a singleton ASCII character ``@{text "c"}'' (with
  10.502 -character code 0--127), for example ``\verb,a,'',
  10.503 +  \item either a singleton ASCII character ``@{text "c"}'' (with
  10.504 +  character code 0--127), for example ``\verb,a,'',
  10.505  
  10.506 -\item or a regular symbol ``\verb,\,\verb,<,@{text "ident"}\verb,>,'',
  10.507 -for example ``\verb,\,\verb,<alpha>,'',
  10.508 +  \item or a regular symbol ``\verb,\,\verb,<,@{text
  10.509 +  "ident"}\verb,>,'', for example ``\verb,\,\verb,<alpha>,'',
  10.510  
  10.511 -\item or a control symbol ``\verb,\,\verb,<^,@{text
  10.512 -"ident"}\verb,>,'', for example ``\verb,\,\verb,<^bold>,'',
  10.513 +  \item or a control symbol ``\verb,\,\verb,<^,@{text
  10.514 +  "ident"}\verb,>,'', for example ``\verb,\,\verb,<^bold>,'',
  10.515  
  10.516 -\item or a raw control symbol ``\verb,\,\verb,<^raw:,@{text
  10.517 -"\<dots>"}\verb,>,'' where ``@{text "\<dots>"}'' refers to any
  10.518 -printable ASCII character (excluding ``\verb,.,'' and ``\verb,>,'') or
  10.519 -non-ASCII character, for example ``\verb,\,\verb,<^raw:$\sum_{i = 1}^n$>,'',
  10.520 +  \item or a raw control symbol ``\verb,\,\verb,<^raw:,@{text
  10.521 +  "\<dots>"}\verb,>,'' where ``@{text "\<dots>"}'' refers to any printable ASCII
  10.522 +  character (excluding ``\verb,.,'' and ``\verb,>,'') or non-ASCII
  10.523 +  character, for example ``\verb,\,\verb,<^raw:$\sum_{i = 1}^n$>,'',
  10.524  
  10.525 -\item or a numbered raw control symbol ``\verb,\,\verb,<^raw,@{text
  10.526 -"nnn"}\verb,>, where @{text "nnn"} are digits, for example
  10.527 -``\verb,\,\verb,<^raw42>,''.
  10.528 +  \item or a numbered raw control symbol ``\verb,\,\verb,<^raw,@{text
  10.529 +  "nnn"}\verb,>, where @{text "nnn"} are digits, for example
  10.530 +  ``\verb,\,\verb,<^raw42>,''.
  10.531  
  10.532 -\end{enumerate}
  10.533 +  \end{enumerate}
  10.534  
  10.535 -The @{text "ident"} syntax for symbol names is @{text "letter (letter
  10.536 -| digit)\<^sup>*"}, where @{text "letter = A..Za..Z"} and @{text
  10.537 -"digit = 0..9"}.  There are infinitely many regular symbols and
  10.538 -control symbols available, but a certain collection of standard
  10.539 -symbols is treated specifically.  For example,
  10.540 -``\verb,\,\verb,<alpha>,'' is classified as a (non-ASCII) letter,
  10.541 -which means it may occur within regular Isabelle identifier syntax.
  10.542 +  The @{text "ident"} syntax for symbol names is @{text "letter
  10.543 +  (letter | digit)\<^sup>*"}, where @{text "letter = A..Za..z"} and
  10.544 +  @{text "digit = 0..9"}.  There are infinitely many regular symbols
  10.545 +  and control symbols available, but a certain collection of standard
  10.546 +  symbols is treated specifically.  For example,
  10.547 +  ``\verb,\,\verb,<alpha>,'' is classified as a (non-ASCII) letter,
  10.548 +  which means it may occur within regular Isabelle identifier syntax.
  10.549  
  10.550 -Output of symbols depends on the print mode (\secref{sec:print-mode}).
  10.551 -For example, the standard {\LaTeX} setup of the Isabelle document
  10.552 -preparation system would present ``\verb,\,\verb,<alpha>,'' as @{text
  10.553 -"\<alpha>"}, and ``\verb,\,\verb,<^bold>,\verb,\,\verb,<alpha>,'' as @{text
  10.554 -"\<^bold>\<alpha>"}.
  10.555 +  Output of symbols depends on the print mode
  10.556 +  (\secref{sec:print-mode}).  For example, the standard {\LaTeX} setup
  10.557 +  of the Isabelle document preparation system would present
  10.558 +  ``\verb,\,\verb,<alpha>,'' as @{text "\<alpha>"}, and
  10.559 +  ``\verb,\,\verb,<^bold>,\verb,\,\verb,<alpha>,'' as @{text
  10.560 +  "\<^bold>\<alpha>"}.
  10.561  
  10.562 -\medskip It is important to note that the character set underlying
  10.563 -Isabelle symbols is plain 7-bit ASCII.  Since 8-bit characters are
  10.564 -passed through transparently, Isabelle may easily process actual
  10.565 -Unicode/UCS data (using the well-known UTF-8 encoding, for example).
  10.566 -Unicode provides its own collection of mathematical symbols, but there
  10.567 -is presently no link to Isabelle's named ones; both kinds of symbols
  10.568 -coexist independently. *}
  10.569 +  \medskip It is important to note that the character set underlying
  10.570 +  Isabelle symbols is plain 7-bit ASCII.  Since 8-bit characters are
  10.571 +  passed through transparently, Isabelle may easily process
  10.572 +  Unicode/UCS data as well (using UTF-8 encoding).  Unicode provides
  10.573 +  its own collection of mathematical symbols, but there is no built-in
  10.574 +  link to the ones of Isabelle.
  10.575 +*}
  10.576  
  10.577  text %mlref {*
  10.578    \begin{mldecls}
  10.579 @@ -476,34 +502,35 @@
  10.580    @{index_ML Symbol.is_letter: "Symbol.symbol -> bool"} \\
  10.581    @{index_ML Symbol.is_digit: "Symbol.symbol -> bool"} \\
  10.582    @{index_ML Symbol.is_quasi: "Symbol.symbol -> bool"} \\
  10.583 -  @{index_ML Symbol.is_blank: "Symbol.symbol -> bool"} \\
  10.584 +  @{index_ML Symbol.is_blank: "Symbol.symbol -> bool"} \\[1ex]
  10.585    @{index_ML_type "Symbol.sym"} \\
  10.586    @{index_ML Symbol.decode: "Symbol.symbol -> Symbol.sym"} \\
  10.587    \end{mldecls}
  10.588  
  10.589    \begin{description}
  10.590  
  10.591 -  \item @{ML_type "Symbol.symbol"} represents Isabelle symbols; this type
  10.592 -  is merely an alias for @{ML_type "string"}, but emphasizes the
  10.593 +  \item @{ML_type "Symbol.symbol"} represents Isabelle symbols.  This
  10.594 +  type is an alias for @{ML_type "string"}, but emphasizes the
  10.595    specific format encountered here.
  10.596  
  10.597    \item @{ML "Symbol.explode"}~@{text "s"} produces a symbol list from
  10.598 -  the packed form usually encountered as user input.  This function
  10.599 -  replaces @{ML "String.explode"} for virtually all purposes of
  10.600 -  manipulating text in Isabelle!  Plain @{ML "implode"} may be used
  10.601 -  for the reverse operation.
  10.602 +  the packed form that is encountered in most practical situations.
  10.603 +  This function supercedes @{ML "String.explode"} for virtually all
  10.604 +  purposes of manipulating text in Isabelle!  Plain @{ML "implode"}
  10.605 +  may still be used for the reverse operation.
  10.606  
  10.607    \item @{ML "Symbol.is_letter"}, @{ML "Symbol.is_digit"}, @{ML
  10.608    "Symbol.is_quasi"}, @{ML "Symbol.is_blank"} classify certain symbols
  10.609    (both ASCII and several named ones) according to fixed syntactic
  10.610 -  convections of Isabelle, e.g.\ see \cite{isabelle-isar-ref}.
  10.611 +  conventions of Isabelle, cf.\ \cite{isabelle-isar-ref}.
  10.612  
  10.613    \item @{ML_type "Symbol.sym"} is a concrete datatype that represents
  10.614 -  the different kinds of symbols explicitly as @{ML "Symbol.Char"},
  10.615 -  @{ML "Symbol.Sym"}, @{ML "Symbol.Ctrl"}, or @{ML "Symbol.Raw"}.
  10.616 +  the different kinds of symbols explicitly with constructors @{ML
  10.617 +  "Symbol.Char"}, @{ML "Symbol.Sym"}, @{ML "Symbol.Ctrl"}, or @{ML
  10.618 +  "Symbol.Raw"}.
  10.619  
  10.620    \item @{ML "Symbol.decode"} converts the string representation of a
  10.621 -  symbol into the explicit datatype version.
  10.622 +  symbol into the datatype version.
  10.623  
  10.624    \end{description}
  10.625  *}
  10.626 @@ -512,50 +539,27 @@
  10.627  subsection {* Qualified names and name spaces *}
  10.628  
  10.629  text {*
  10.630 -  FIXME
  10.631 -
  10.632 -  Qualified names are constructed according to implicit naming
  10.633 -  principles of the present context.
  10.634 -
  10.635 -
  10.636 -  The last component is called \emph{base name}; the remaining prefix
  10.637 -  of qualification may be empty.
  10.638 -
  10.639 -  Some practical conventions help to organize named entities more
  10.640 -  systematically:
  10.641 -
  10.642 -  \begin{itemize}
  10.643 -
  10.644 -  \item Names are qualified first by the theory name, second by an
  10.645 -  optional ``structure''.  For example, a constant @{text "c"}
  10.646 -  declared as part of a certain structure @{text "b"} (say a type
  10.647 -  definition) in theory @{text "A"} will be named @{text "A.b.c"}
  10.648 -  internally.
  10.649 -
  10.650 -  \item
  10.651 +  A \emph{qualified name} essentially consists of a non-empty list of
  10.652 +  basic name components.  The packad notation uses a dot as separator,
  10.653 +  as in @{text "A.b"}, for example.  The very last component is called
  10.654 +  \emph{base} name, the remaining prefix \emph{qualifier} (which may
  10.655 +  be empty).
  10.656  
  10.657 -  \item
  10.658 -
  10.659 -  \item
  10.660 -
  10.661 -  \item
  10.662 -
  10.663 -  \end{itemize}
  10.664 +  A @{text "naming"} policy tells how to produce fully qualified names
  10.665 +  from a given specification.  The @{text "full"} operation applies
  10.666 +  performs naming of a name; the policy is usually taken from the
  10.667 +  context.  For example, a common policy is to attach an implicit
  10.668 +  prefix.
  10.669  
  10.670 -  Names of different kinds of entities are basically independent, but
  10.671 -  some practical naming conventions relate them to each other.  For
  10.672 -  example, a constant @{text "foo"} may be accompanied with theorems
  10.673 -  @{text "foo.intro"}, @{text "foo.elim"}, @{text "foo.simps"} etc.
  10.674 -  The same may happen for a type @{text "foo"}, which is then apt to
  10.675 -  cause clashes in the theorem name space!  To avoid this, we
  10.676 -  occasionally follow an additional convention of suffixes that
  10.677 -  determine the original kind of entity that a name has been derived.
  10.678 -  For example, constant @{text "foo"} is associated with theorem
  10.679 -  @{text "foo.intro"}, type @{text "foo"} with theorem @{text
  10.680 -  "foo_type.intro"}, and type class @{text "foo"} with @{text
  10.681 -  "foo_class.intro"}.
  10.682 +  A @{text "name space"} manages declarations of fully qualified
  10.683 +  names.  There are separate operations to @{text "declare"}, @{text
  10.684 +  "intern"}, and @{text "extern"} names.
  10.685 +
  10.686 +  FIXME
  10.687  *}
  10.688  
  10.689 +text %mlref FIXME
  10.690 +
  10.691  
  10.692  section {* Structured output *}
  10.693  
  10.694 @@ -567,7 +571,7 @@
  10.695  
  10.696  text FIXME
  10.697  
  10.698 -subsection {* Print modes *}
  10.699 +subsection {* Print modes \label{sec:print-mode} *}
  10.700  
  10.701  text FIXME
  10.702  
    11.1 --- a/doc-src/IsarImplementation/Thy/proof.thy	Thu Aug 31 18:27:40 2006 +0200
    11.2 +++ b/doc-src/IsarImplementation/Thy/proof.thy	Thu Aug 31 22:55:49 2006 +0200
    11.3 @@ -3,11 +3,9 @@
    11.4  
    11.5  theory "proof" imports base begin
    11.6  
    11.7 -chapter {* Structured reasoning *}
    11.8 +chapter {* Structured proofs *}
    11.9  
   11.10 -section {* Proof context *}
   11.11 -
   11.12 -subsection {* Local variables *}
   11.13 +section {* Local variables *}
   11.14  
   11.15  text FIXME
   11.16  
   11.17 @@ -66,7 +64,23 @@
   11.18  
   11.19  text FIXME
   11.20  
   11.21 -section {* Proof state *}
   11.22 +
   11.23 +section {* Schematic polymorphism *}
   11.24 +
   11.25 +text FIXME
   11.26 +
   11.27 +
   11.28 +section {* Assumptions *}
   11.29 +
   11.30 +text FIXME
   11.31 +
   11.32 +
   11.33 +section {* Conclusions *}
   11.34 +
   11.35 +text FIXME
   11.36 +
   11.37 +
   11.38 +section {* Structured proofs \label{sec:isar-proof-state} *}
   11.39  
   11.40  text {*
   11.41    FIXME
   11.42 @@ -85,12 +99,12 @@
   11.43  
   11.44  *}
   11.45  
   11.46 -section {* Methods *}
   11.47 +section {* Proof methods *}
   11.48  
   11.49  text FIXME
   11.50  
   11.51  section {* Attributes *}
   11.52  
   11.53 -text FIXME
   11.54 +text "FIXME ?!"
   11.55  
   11.56  end
    12.1 --- a/doc-src/IsarImplementation/Thy/tactic.thy	Thu Aug 31 18:27:40 2006 +0200
    12.2 +++ b/doc-src/IsarImplementation/Thy/tactic.thy	Thu Aug 31 22:55:49 2006 +0200
    12.3 @@ -3,57 +3,63 @@
    12.4  
    12.5  theory tactic imports base begin
    12.6  
    12.7 -chapter {* Tactical theorem proving *}
    12.8 +chapter {* Goal-directed reasoning *}
    12.9  
   12.10 -text {* The basic idea of tactical theorem proving is to refine the
   12.11 -initial claim in a backwards fashion, until a solved form is reached.
   12.12 -An intermediate goal consists of several subgoals that need to be
   12.13 -solved in order to achieve the main statement; zero subgoals means
   12.14 -that the proof may be finished.  Goal refinement operations are called
   12.15 -tactics; combinators for composing tactics are called tacticals.  *}
   12.16 +text {*
   12.17 +  The basic idea of tactical theorem proving is to refine the initial
   12.18 +  claim in a backwards fashion, until a solved form is reached.  An
   12.19 +  intermediate goal consists of several subgoals that need to be
   12.20 +  solved in order to achieve the main statement; zero subgoals means
   12.21 +  that the proof may be finished.  A @{text "tactic"} is a refinement
   12.22 +  operation that maps a goal to a lazy sequence of potential
   12.23 +  successors.  A @{text "tactical"} is a combinator for composing
   12.24 +  tactics.
   12.25 +*}
   12.26  
   12.27  
   12.28  section {* Goals \label{sec:tactical-goals} *}
   12.29  
   12.30 -text {* Isabelle/Pure represents a goal\glossary{Tactical goal}{A
   12.31 -theorem of \seeglossary{Horn Clause} form stating that a number of
   12.32 -subgoals imply the main conclusion, which is marked as a protected
   12.33 -proposition.} as a theorem stating that the subgoals imply the main
   12.34 -goal: @{text "A\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^sub>n \<Longrightarrow> C"}.  The outermost goal
   12.35 -structure is that of a Horn Clause\glossary{Horn Clause}{An iterated
   12.36 -implication @{text "A\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^sub>n \<Longrightarrow> C"}, without any
   12.37 -outermost quantifiers.  Strictly speaking, propositions @{text
   12.38 -"A\<^sub>i"} need to be atomic in Horn Clauses, but Isabelle admits
   12.39 -arbitrary substructure here (nested @{text "\<Longrightarrow>"} and @{text "\<And>"}
   12.40 -connectives).}: an iterated implication without any
   12.41 -quantifiers\footnote{Recall that outermost @{text "\<And>x. \<phi>[x]"} is
   12.42 -always represented via schematic variables in the body: @{text
   12.43 -"\<phi>[?x]"}.  These may get instantiated during the course of
   12.44 -reasoning.}.  For @{text "n = 0"} a goal is solved.
   12.45 +text {*
   12.46 +  Isabelle/Pure represents a goal\glossary{Tactical goal}{A theorem of
   12.47 +  \seeglossary{Horn Clause} form stating that a number of subgoals
   12.48 +  imply the main conclusion, which is marked as a protected
   12.49 +  proposition.} as a theorem stating that the subgoals imply the main
   12.50 +  goal: @{text "A\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^sub>n \<Longrightarrow> C"}.  The outermost goal
   12.51 +  structure is that of a Horn Clause\glossary{Horn Clause}{An iterated
   12.52 +  implication @{text "A\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^sub>n \<Longrightarrow> C"}, without any
   12.53 +  outermost quantifiers.  Strictly speaking, propositions @{text
   12.54 +  "A\<^sub>i"} need to be atomic in Horn Clauses, but Isabelle admits
   12.55 +  arbitrary substructure here (nested @{text "\<Longrightarrow>"} and @{text "\<And>"}
   12.56 +  connectives).}: i.e.\ an iterated implication without any
   12.57 +  quantifiers\footnote{Recall that outermost @{text "\<And>x. \<phi>[x]"} is
   12.58 +  always represented via schematic variables in the body: @{text
   12.59 +  "\<phi>[?x]"}.  These variables may get instantiated during the course of
   12.60 +  reasoning.}.  For @{text "n = 0"} a goal is called ``solved''.
   12.61  
   12.62 -The structure of each subgoal @{text "A\<^sub>i"} is that of a general
   12.63 -Heriditary Harrop Formula @{text "\<And>x\<^sub>1 \<dots> \<And>x\<^sub>k. H\<^sub>1 \<Longrightarrow>
   12.64 -\<dots> \<Longrightarrow> H\<^sub>m \<Longrightarrow> B"} according to the normal form where any local
   12.65 -@{text \<And>} is pulled before @{text \<Longrightarrow>}.  Here @{text "x\<^sub>1, \<dots>,
   12.66 -x\<^sub>k"} are goal parameters, i.e.\ arbitrary-but-fixed entities of
   12.67 -certain types, and @{text "H\<^sub>1, \<dots>, H\<^sub>m"} are goal
   12.68 -hypotheses, i.e.\ facts that may be assumed locally.  Together, this
   12.69 -forms the goal context of the conclusion @{text B} to be established.
   12.70 -The goal hypotheses may be again arbitrary Harrop Formulas, although
   12.71 -the level of nesting rarely exceeds 1--2 in practice.
   12.72 +  The structure of each subgoal @{text "A\<^sub>i"} is that of a
   12.73 +  general Hereditary Harrop Formula @{text "\<And>x\<^sub>1 \<dots>
   12.74 +  \<And>x\<^sub>k. H\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> H\<^sub>m \<Longrightarrow> B"} according to the normal
   12.75 +  form where any local @{text \<And>} is pulled before @{text \<Longrightarrow>}.  Here
   12.76 +  @{text "x\<^sub>1, \<dots>, x\<^sub>k"} are goal parameters, i.e.\
   12.77 +  arbitrary-but-fixed entities of certain types, and @{text
   12.78 +  "H\<^sub>1, \<dots>, H\<^sub>m"} are goal hypotheses, i.e.\ facts that may
   12.79 +  be assumed locally.  Together, this forms the goal context of the
   12.80 +  conclusion @{text B} to be established.  The goal hypotheses may be
   12.81 +  again Hereditary Harrop Formulas, although the level of nesting
   12.82 +  rarely exceeds 1--2 in practice.
   12.83  
   12.84 -The main conclusion @{text C} is internally marked as a protected
   12.85 -proposition\glossary{Protected proposition}{An arbitrarily structured
   12.86 -proposition @{text "C"} which is forced to appear as atomic by
   12.87 -wrapping it into a propositional identity operator; notation @{text
   12.88 -"#C"}.  Protecting a proposition prevents basic inferences from
   12.89 -entering into that structure for the time being.}, which is
   12.90 -occasionally represented explicitly by the notation @{text "#C"}.
   12.91 -This ensures that the decomposition into subgoals and main conclusion
   12.92 -is well-defined for arbitrarily structured claims.
   12.93 +  The main conclusion @{text C} is internally marked as a protected
   12.94 +  proposition\glossary{Protected proposition}{An arbitrarily
   12.95 +  structured proposition @{text "C"} which is forced to appear as
   12.96 +  atomic by wrapping it into a propositional identity operator;
   12.97 +  notation @{text "#C"}.  Protecting a proposition prevents basic
   12.98 +  inferences from entering into that structure for the time being.},
   12.99 +  which is occasionally represented explicitly by the notation @{text
  12.100 +  "#C"}.  This ensures that the decomposition into subgoals and main
  12.101 +  conclusion is well-defined for arbitrarily structured claims.
  12.102  
  12.103 -\medskip Basic goal management is performed via the following
  12.104 -Isabelle/Pure rules:
  12.105 +  \medskip Basic goal management is performed via the following
  12.106 +  Isabelle/Pure rules:
  12.107  
  12.108    \[
  12.109    \infer[@{text "(init)"}]{@{text "C \<Longrightarrow> #C"}}{} \qquad
  12.110 @@ -79,14 +85,14 @@
  12.111  
  12.112    \begin{description}
  12.113  
  12.114 -  \item @{ML "Goal.init"}~@{text "\<phi>"} initializes a tactical goal with
  12.115 +  \item @{ML "Goal.init"}~@{text "\<phi>"} initializes a tactical goal from
  12.116    the type-checked proposition @{text \<phi>}.
  12.117  
  12.118    \item @{ML "Goal.finish"}~@{text "th"} checks whether theorem @{text
  12.119 -  "th"} is a solved goal configuration (zero subgoals), and concludes
  12.120 +  "th"} is a solved goal configuration (no subgoals), and concludes
  12.121    the result by removing the goal protection.
  12.122  
  12.123 -  \item @{ML "Goal.protect"}~@{text "th"} protects the whole statement
  12.124 +  \item @{ML "Goal.protect"}~@{text "th"} protects the full statement
  12.125    of theorem @{text "th"}.
  12.126  
  12.127    \item @{ML "Goal.conclude"}~@{text "th"} removes the goal protection
  12.128 @@ -139,12 +145,10 @@
  12.129    ill-behaved tactics could have destroyed that information.
  12.130  
  12.131    Several simultaneous claims may be handled within a single goal
  12.132 -  statement by using meta-level conjunction internally.\footnote{This
  12.133 -  is merely syntax for certain derived statements within
  12.134 -  Isabelle/Pure, there is no need to introduce a separate conjunction
  12.135 -  operator.}  The whole configuration may be considered within a
  12.136 -  context of arbitrary-but-fixed parameters and hypotheses, which will
  12.137 -  be available as local facts during the proof and discharged into
  12.138 +  statement by using meta-level conjunction internally.  The whole
  12.139 +  configuration may be considered within a context of
  12.140 +  arbitrary-but-fixed parameters and hypotheses, which will be
  12.141 +  available as local facts during the proof and discharged into
  12.142    implications in the result.
  12.143  
  12.144    All of these administrative tasks are packaged into a separate
    13.1 --- a/doc-src/IsarImplementation/implementation.tex	Thu Aug 31 18:27:40 2006 +0200
    13.2 +++ b/doc-src/IsarImplementation/implementation.tex	Thu Aug 31 22:55:49 2006 +0200
    13.3 @@ -29,7 +29,7 @@
    13.4  \begin{abstract}
    13.5    We describe the key concepts underlying the Isabelle/Isar
    13.6    implementation, including ML references for the most important
    13.7 -  elements.  The aim is to give some insight into the overall system
    13.8 +  functions.  The aim is to give some insight into the overall system
    13.9    architecture, and provide clues on implementing user extensions.
   13.10  \end{abstract}
   13.11  
    14.1 --- a/doc-src/IsarImplementation/style.sty	Thu Aug 31 18:27:40 2006 +0200
    14.2 +++ b/doc-src/IsarImplementation/style.sty	Thu Aug 31 22:55:49 2006 +0200
    14.3 @@ -38,6 +38,8 @@
    14.4  \binperiod
    14.5  \underscoreon
    14.6  
    14.7 +\renewcommand{\isadigit}[1]{\isamath{#1}}
    14.8 +
    14.9  \newenvironment{mldecls}{\par\noindent\begingroup\footnotesize\def\isanewline{\\}\begin{tabular}{l}}{\end{tabular}\medskip\endgroup}
   14.10  
   14.11  \isafoldtag{FIXME}