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}{FIXME}
3.30 -\glossary{Term}{FIXME}%
3.31 + \glossary{Type arity}{FIXME}
3.32 +
3.33 + \glossary{Sort}{FIXME}
3.34 +
3.35 + FIXME classes and sorts
3.36 +
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 +\glossary{Term}{FIXME}
3.56
3.57 -\glossary{Type constructor}{FIXME}
3.58 -
3.59 -\glossary{Type class}{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 + \item either a singleton ASCII character ``\isa{c}'' (with
4.487 + character code 0--127), for example ``\verb,a,'',
4.488
4.489 -\item or a regular symbol ``\verb,\,\verb,<,\isa{ident}\verb,>,'',
4.490 -for example ``\verb,\,\verb,<alpha>,'',
4.491 + \item or a regular symbol ``\verb,\,\verb,<,\isa{ident}\verb,>,'', for example ``\verb,\,\verb,<alpha>,'',
4.492
4.493 -\item or a control symbol ``\verb,\,\verb,<^,\isa{ident}\verb,>,'', for example ``\verb,\,\verb,<^bold>,'',
4.494 + \item or a control symbol ``\verb,\,\verb,<^,\isa{ident}\verb,>,'', for example ``\verb,\,\verb,<^bold>,'',
4.495
4.496 -\item or a raw control symbol ``\verb,\,\verb,<^raw:,\isa{{\isasymdots}}\verb,>,'' where ``\isa{{\isasymdots}}'' refers to any
4.497 -printable ASCII character (excluding ``\verb,.,'' and ``\verb,>,'') or
4.498 -non-ASCII character, for example ``\verb,\,\verb,<^raw:$\sum_{i = 1}^n$>,'',
4.499 + \item or a raw control symbol ``\verb,\,\verb,<^raw:,\isa{{\isasymdots}}\verb,>,'' where ``\isa{{\isasymdots}}'' refers to any printable ASCII
4.500 + character (excluding ``\verb,.,'' and ``\verb,>,'') or non-ASCII
4.501 + character, for example ``\verb,\,\verb,<^raw:$\sum_{i = 1}^n$>,'',
4.502
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 + \item or a numbered raw control symbol ``\verb,\,\verb,<^raw,\isa{nnn}\verb,>, where \isa{nnn} are digits, for example
4.506 + ``\verb,\,\verb,<^raw42>,''.
4.507
4.508 -\end{enumerate}
4.509 + \end{enumerate}
4.510
4.511 -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.512 -control symbols available, but a certain collection of standard
4.513 -symbols is treated specifically. For example,
4.514 -``\verb,\,\verb,<alpha>,'' is classified as a (non-ASCII) letter,
4.515 -which means it may occur within regular Isabelle identifier syntax.
4.516 + 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.517 + \isa{digit\ {\isacharequal}\ {\isadigit{0}}{\isachardot}{\isachardot}{\isadigit{9}}}. There are infinitely many regular symbols
4.518 + and control symbols available, but a certain collection of standard
4.519 + symbols is treated specifically. For example,
4.520 + ``\verb,\,\verb,<alpha>,'' is classified as a (non-ASCII) letter,
4.521 + which means it may occur within regular Isabelle identifier syntax.
4.522
4.523 -Output of symbols depends on the print mode (\secref{sec:print-mode}).
4.524 -For example, the standard {\LaTeX} setup of the Isabelle document
4.525 -preparation system would present ``\verb,\,\verb,<alpha>,'' as \isa{{\isasymalpha}}, and ``\verb,\,\verb,<^bold>,\verb,\,\verb,<alpha>,'' as \isa{\isactrlbold {\isasymalpha}}.
4.526 + Output of symbols depends on the print mode
4.527 + (\secref{sec:print-mode}). For example, the standard {\LaTeX} setup
4.528 + of the Isabelle document preparation system would present
4.529 + ``\verb,\,\verb,<alpha>,'' as \isa{{\isasymalpha}}, and
4.530 + ``\verb,\,\verb,<^bold>,\verb,\,\verb,<alpha>,'' as \isa{\isactrlbold {\isasymalpha}}.
4.531
4.532 -\medskip It is important to note that the character set underlying
4.533 -Isabelle symbols is plain 7-bit ASCII. Since 8-bit characters are
4.534 -passed through transparently, Isabelle may easily process actual
4.535 -Unicode/UCS data (using the well-known UTF-8 encoding, for example).
4.536 -Unicode provides its own collection of mathematical symbols, but there
4.537 -is presently no link to Isabelle's named ones; both kinds of symbols
4.538 -coexist independently.%
4.539 + \medskip It is important to note that the character set underlying
4.540 + Isabelle symbols is plain 7-bit ASCII. Since 8-bit characters are
4.541 + passed through transparently, Isabelle may easily process
4.542 + Unicode/UCS data as well (using UTF-8 encoding). Unicode provides
4.543 + its own collection of mathematical symbols, but there is no built-in
4.544 + link to the ones of Isabelle.%
4.545 \end{isamarkuptext}%
4.546 \isamarkuptrue%
4.547 %
4.548 @@ -555,33 +574,32 @@
4.549 \indexml{Symbol.is-letter}\verb|Symbol.is_letter: Symbol.symbol -> bool| \\
4.550 \indexml{Symbol.is-digit}\verb|Symbol.is_digit: Symbol.symbol -> bool| \\
4.551 \indexml{Symbol.is-quasi}\verb|Symbol.is_quasi: Symbol.symbol -> bool| \\
4.552 - \indexml{Symbol.is-blank}\verb|Symbol.is_blank: Symbol.symbol -> bool| \\
4.553 + \indexml{Symbol.is-blank}\verb|Symbol.is_blank: Symbol.symbol -> bool| \\[1ex]
4.554 \indexmltype{Symbol.sym}\verb|type Symbol.sym| \\
4.555 \indexml{Symbol.decode}\verb|Symbol.decode: Symbol.symbol -> Symbol.sym| \\
4.556 \end{mldecls}
4.557
4.558 \begin{description}
4.559
4.560 - \item \verb|Symbol.symbol| represents Isabelle symbols; this type
4.561 - is merely an alias for \verb|string|, but emphasizes the
4.562 + \item \verb|Symbol.symbol| represents Isabelle symbols. This
4.563 + type is an alias for \verb|string|, but emphasizes the
4.564 specific format encountered here.
4.565
4.566 \item \verb|Symbol.explode|~\isa{s} produces a symbol list from
4.567 - the packed form usually encountered as user input. This function
4.568 - replaces \verb|String.explode| for virtually all purposes of
4.569 - manipulating text in Isabelle! Plain \verb|implode| may be used
4.570 - for the reverse operation.
4.571 + the packed form that is encountered in most practical situations.
4.572 + This function supercedes \verb|String.explode| for virtually all
4.573 + purposes of manipulating text in Isabelle! Plain \verb|implode|
4.574 + may still be used for the reverse operation.
4.575
4.576 \item \verb|Symbol.is_letter|, \verb|Symbol.is_digit|, \verb|Symbol.is_quasi|, \verb|Symbol.is_blank| classify certain symbols
4.577 (both ASCII and several named ones) according to fixed syntactic
4.578 - convections of Isabelle, e.g.\ see \cite{isabelle-isar-ref}.
4.579 + conventions of Isabelle, cf.\ \cite{isabelle-isar-ref}.
4.580
4.581 \item \verb|Symbol.sym| is a concrete datatype that represents
4.582 - the different kinds of symbols explicitly as \verb|Symbol.Char|,
4.583 - \verb|Symbol.Sym|, \verb|Symbol.Ctrl|, or \verb|Symbol.Raw|.
4.584 + the different kinds of symbols explicitly with constructors \verb|Symbol.Char|, \verb|Symbol.Sym|, \verb|Symbol.Ctrl|, or \verb|Symbol.Raw|.
4.585
4.586 \item \verb|Symbol.decode| converts the string representation of a
4.587 - symbol into the explicit datatype version.
4.588 + symbol into the datatype version.
4.589
4.590 \end{description}%
4.591 \end{isamarkuptext}%
4.592 @@ -599,49 +617,43 @@
4.593 \isamarkuptrue%
4.594 %
4.595 \begin{isamarkuptext}%
4.596 -FIXME
4.597 +A \emph{qualified name} essentially consists of a non-empty list of
4.598 + basic name components. The packad notation uses a dot as separator,
4.599 + as in \isa{A{\isachardot}b}, for example. The very last component is called
4.600 + \emph{base} name, the remaining prefix \emph{qualifier} (which may
4.601 + be empty).
4.602
4.603 - Qualified names are constructed according to implicit naming
4.604 - principles of the present context.
4.605 + A \isa{naming} policy tells how to produce fully qualified names
4.606 + from a given specification. The \isa{full} operation applies
4.607 + performs naming of a name; the policy is usually taken from the
4.608 + context. For example, a common policy is to attach an implicit
4.609 + prefix.
4.610
4.611 + A \isa{name\ space} manages declarations of fully qualified
4.612 + names. There are separate operations to \isa{declare}, \isa{intern}, and \isa{extern} names.
4.613
4.614 - The last component is called \emph{base name}; the remaining prefix
4.615 - of qualification may be empty.
4.616 -
4.617 - Some practical conventions help to organize named entities more
4.618 - systematically:
4.619 -
4.620 - \begin{itemize}
4.621 -
4.622 - \item Names are qualified first by the theory name, second by an
4.623 - optional ``structure''. For example, a constant \isa{c}
4.624 - declared as part of a certain structure \isa{b} (say a type
4.625 - definition) in theory \isa{A} will be named \isa{A{\isachardot}b{\isachardot}c}
4.626 - internally.
4.627 -
4.628 - \item
4.629 -
4.630 - \item
4.631 -
4.632 - \item
4.633 -
4.634 - \item
4.635 -
4.636 - \end{itemize}
4.637 -
4.638 - Names of different kinds of entities are basically independent, but
4.639 - some practical naming conventions relate them to each other. For
4.640 - example, a constant \isa{foo} may be accompanied with theorems
4.641 - \isa{foo{\isachardot}intro}, \isa{foo{\isachardot}elim}, \isa{foo{\isachardot}simps} etc.
4.642 - The same may happen for a type \isa{foo}, which is then apt to
4.643 - cause clashes in the theorem name space! To avoid this, we
4.644 - occasionally follow an additional convention of suffixes that
4.645 - determine the original kind of entity that a name has been derived.
4.646 - For example, constant \isa{foo} is associated with theorem
4.647 - \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.648 + FIXME%
4.649 \end{isamarkuptext}%
4.650 \isamarkuptrue%
4.651 %
4.652 +\isadelimmlref
4.653 +%
4.654 +\endisadelimmlref
4.655 +%
4.656 +\isatagmlref
4.657 +%
4.658 +\begin{isamarkuptext}%
4.659 +FIXME%
4.660 +\end{isamarkuptext}%
4.661 +\isamarkuptrue%
4.662 +%
4.663 +\endisatagmlref
4.664 +{\isafoldmlref}%
4.665 +%
4.666 +\isadelimmlref
4.667 +%
4.668 +\endisadelimmlref
4.669 +%
4.670 \isamarkupsection{Structured output%
4.671 }
4.672 \isamarkuptrue%
4.673 @@ -664,7 +676,7 @@
4.674 \end{isamarkuptext}%
4.675 \isamarkuptrue%
4.676 %
4.677 -\isamarkupsubsection{Print modes%
4.678 +\isamarkupsubsection{Print modes \label{sec:print-mode}%
4.679 }
4.680 \isamarkuptrue%
4.681 %
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,44 +5,41 @@
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 +section {* Terms \label{sec:terms} *}
9.39
9.40 text {*
9.41 + \glossary{Term}{FIXME}
9.42
9.43 -FIXME
9.44 -
9.45 -\glossary{Type}{FIXME}
9.46 -\glossary{Term}{FIXME}
9.47 -
9.48 + FIXME de-Bruijn representation of lambda terms
9.49 *}
9.50
9.51 -subsection {* The order-sorted algebra of types *}
9.52 -
9.53 -text {*
9.54 -
9.55 -FIXME
9.56 -
9.57 -\glossary{Type constructor}{FIXME}
9.58 -
9.59 -\glossary{Type class}{FIXME}
9.60 -
9.61 -\glossary{Type arity}{FIXME}
9.62 -
9.63 -\glossary{Sort}{FIXME}
9.64 -
9.65 -*}
9.66 -
9.67 -
9.68 -subsection {* Type-inference and schematic polymorphism *}
9.69
9.70 text {*
9.71
9.72 @@ -55,21 +52,7 @@
9.73 *}
9.74
9.75
9.76 -section {* Theory *}
9.77 -
9.78 -text {*
9.79 -
9.80 -FIXME
9.81 -
9.82 -\glossary{Constant}{Essentially a \seeglossary{fixed variable} of the
9.83 -theory context, but slightly more flexible since it may be used at
9.84 -different type-instances, due to \seeglossary{schematic
9.85 -polymorphism.}}
9.86 -
9.87 -*}
9.88 -
9.89 -
9.90 -section {* Deduction *}
9.91 +section {* Theorems \label{sec:thms} *}
9.92
9.93 text {*
9.94
9.95 @@ -139,8 +122,21 @@
9.96 text FIXME
9.97
9.98
9.99 -section {* Proof terms *}
9.100 +section {* Low-level specifications *}
9.101
9.102 -text FIXME
9.103 +text {*
9.104 +
9.105 +FIXME
9.106 +
9.107 +\glossary{Constant}{Essentially a \seeglossary{fixed variable} of the
9.108 +theory context, but slightly more flexible since it may be used at
9.109 +different type-instances, due to \seeglossary{schematic
9.110 +polymorphism.}}
9.111 +
9.112 +\glossary{Axiom}{FIXME}
9.113 +
9.114 +\glossary{Primitive definition}{FIXME}
9.115 +
9.116 +*}
9.117
9.118 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 -Each name space is organized as a collection of \emph{qualified
10.453 -names}, which consist of a sequence of basic name components separated
10.454 -by dots: @{text "Bar.bar.foo"}, @{text "Bar.foo"}, and @{text "foo"}
10.455 -are examples for valid qualified names. Name components are
10.456 -subdivided into \emph{symbols}, which constitute the smallest textual
10.457 -unit in Isabelle --- raw characters are normally not encountered
10.458 -directly. *}
10.459 + Name spaces are organized uniformly, as a collection of qualified
10.460 + names consisting of a sequence of basic name components separated by
10.461 + dots: @{text "Bar.bar.foo"}, @{text "Bar.foo"}, and @{text "foo"}
10.462 + are examples for qualified names.
10.463 +
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,49 +539,26 @@
10.627 subsection {* Qualified names and name spaces *}
10.628
10.629 text {*
10.630 + A \emph{qualified name} essentially consists of a non-empty list of
10.631 + basic name components. The packad notation uses a dot as separator,
10.632 + as in @{text "A.b"}, for example. The very last component is called
10.633 + \emph{base} name, the remaining prefix \emph{qualifier} (which may
10.634 + be empty).
10.635 +
10.636 + A @{text "naming"} policy tells how to produce fully qualified names
10.637 + from a given specification. The @{text "full"} operation applies
10.638 + performs naming of a name; the policy is usually taken from the
10.639 + context. For example, a common policy is to attach an implicit
10.640 + prefix.
10.641 +
10.642 + A @{text "name space"} manages declarations of fully qualified
10.643 + names. There are separate operations to @{text "declare"}, @{text
10.644 + "intern"}, and @{text "extern"} names.
10.645 +
10.646 FIXME
10.647 +*}
10.648
10.649 - Qualified names are constructed according to implicit naming
10.650 - principles of the present context.
10.651 -
10.652 -
10.653 - The last component is called \emph{base name}; the remaining prefix
10.654 - of qualification may be empty.
10.655 -
10.656 - Some practical conventions help to organize named entities more
10.657 - systematically:
10.658 -
10.659 - \begin{itemize}
10.660 -
10.661 - \item Names are qualified first by the theory name, second by an
10.662 - optional ``structure''. For example, a constant @{text "c"}
10.663 - declared as part of a certain structure @{text "b"} (say a type
10.664 - definition) in theory @{text "A"} will be named @{text "A.b.c"}
10.665 - internally.
10.666 -
10.667 - \item
10.668 -
10.669 - \item
10.670 -
10.671 - \item
10.672 -
10.673 - \item
10.674 -
10.675 - \end{itemize}
10.676 -
10.677 - Names of different kinds of entities are basically independent, but
10.678 - some practical naming conventions relate them to each other. For
10.679 - example, a constant @{text "foo"} may be accompanied with theorems
10.680 - @{text "foo.intro"}, @{text "foo.elim"}, @{text "foo.simps"} etc.
10.681 - The same may happen for a type @{text "foo"}, which is then apt to
10.682 - cause clashes in the theorem name space! To avoid this, we
10.683 - occasionally follow an additional convention of suffixes that
10.684 - determine the original kind of entity that a name has been derived.
10.685 - For example, constant @{text "foo"} is associated with theorem
10.686 - @{text "foo.intro"}, type @{text "foo"} with theorem @{text
10.687 - "foo_type.intro"}, and type class @{text "foo"} with @{text
10.688 - "foo_class.intro"}.
10.689 -*}
10.690 +text %mlref FIXME
10.691
10.692
10.693 section {* Structured output *}
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}