--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarImplementation/IsaMakefile Mon Jan 02 20:16:52 2006 +0100
@@ -0,0 +1,33 @@
+
+## targets
+
+default: Thy
+images:
+test: Thy
+
+all: images test
+
+
+## global settings
+
+SRC = $(ISABELLE_HOME)/src
+OUT = $(ISABELLE_OUTPUT)
+LOG = $(OUT)/log
+
+USEDIR = $(ISATOOL) usedir -v true -i false -d false -C false -D document
+
+
+## Thy
+
+Thy: $(LOG)/Pure-Thy.gz
+
+$(LOG)/Pure-Thy.gz: Thy/ROOT.ML Thy/base.thy Thy/integration.thy \
+ Thy/locale.thy Thy/logic.thy Thy/prelim.thy Thy/proof.thy Thy/tactic.thy \
+ Thy/ML.thy Thy/setup.ML
+ @$(USEDIR) Pure Thy
+
+
+## clean
+
+clean:
+ @rm -f $(LOG)/Pure-Thy.gz
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarImplementation/Makefile Mon Jan 02 20:16:52 2006 +0100
@@ -0,0 +1,46 @@
+#
+# $Id$
+#
+
+## targets
+
+default: dvi
+
+
+## dependencies
+
+include ../Makefile.in
+
+MAKEGLOSSARY = ./makeglossary
+
+NAME = implementation
+
+FILES = implementation.tex intro.tex Thy/document/prelim.tex Thy/document/logic.tex \
+ Thy/document/tactic.tex Thy/document/proof.tex Thy/document/locale.tex \
+ Thy/document/integration.tex style.sty ../iman.sty ../extra.sty ../isar.sty \
+ ../manual.bib ../proof.sty
+
+dvi: $(NAME).dvi
+
+$(NAME).dvi: $(FILES) isabelle_isar.eps
+ $(LATEX) $(NAME)
+ $(BIBTEX) $(NAME)
+ $(LATEX) $(NAME)
+ $(LATEX) $(NAME)
+ $(MAKEGLOSSARY) $(NAME)
+ $(SEDINDEX) $(NAME)
+ $(LATEX) $(NAME)
+ $(LATEX) $(NAME)
+
+pdf: $(NAME).pdf
+
+$(NAME).pdf: $(FILES) isabelle_isar.pdf
+ $(PDFLATEX) $(NAME)
+ $(BIBTEX) $(NAME)
+ $(PDFLATEX) $(NAME)
+ $(PDFLATEX) $(NAME)
+ $(MAKEGLOSSARY) $(NAME)
+ $(SEDINDEX) $(NAME)
+ $(FIXBOOKMARKS) $(NAME).out
+ $(PDFLATEX) $(NAME)
+ $(PDFLATEX) $(NAME)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarImplementation/Thy/ML.thy Mon Jan 02 20:16:52 2006 +0100
@@ -0,0 +1,2 @@
+
+theory "ML" imports Pure begin end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarImplementation/Thy/ROOT.ML Mon Jan 02 20:16:52 2006 +0100
@@ -0,0 +1,10 @@
+
+(* $Id$ *)
+
+use_thy "prelim";
+use_thy "logic";
+use_thy "tactic";
+use_thy "proof";
+use_thy "locale";
+use_thy "integration";
+use_thy "ML";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarImplementation/Thy/base.thy Mon Jan 02 20:16:52 2006 +0100
@@ -0,0 +1,9 @@
+
+(* $Id$ *)
+
+theory base
+imports CPure
+uses "setup.ML"
+begin
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarImplementation/Thy/document/ML.tex Mon Jan 02 20:16:52 2006 +0100
@@ -0,0 +1,25 @@
+%
+\begin{isabellebody}%
+\def\isabellecontext{ML}%
+%
+\isadelimtheory
+\isanewline
+%
+\endisadelimtheory
+%
+\isatagtheory
+\isacommand{theory}\isamarkupfalse%
+\ {\isachardoublequoteopen}ML{\isachardoublequoteclose}\ \isakeyword{imports}\ Pure\ \isakeyword{begin}\ \isacommand{end}\isamarkupfalse%
+%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+\isanewline
+%
+\endisadelimtheory
+\end{isabellebody}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarImplementation/Thy/document/base.tex Mon Jan 02 20:16:52 2006 +0100
@@ -0,0 +1,32 @@
+%
+\begin{isabellebody}%
+\def\isabellecontext{base}%
+%
+\isadelimtheory
+\isanewline
+\isanewline
+\isanewline
+%
+\endisadelimtheory
+%
+\isatagtheory
+\isacommand{theory}\isamarkupfalse%
+\ base\isanewline
+\isakeyword{imports}\ CPure\isanewline
+\isakeyword{uses}\ {\isachardoublequoteopen}setup{\isachardot}ML{\isachardoublequoteclose}\isanewline
+\isakeyword{begin}\isanewline
+\isanewline
+\isacommand{end}\isamarkupfalse%
+%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+\isanewline
+%
+\endisadelimtheory
+\end{isabellebody}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarImplementation/Thy/document/integration.tex Mon Jan 02 20:16:52 2006 +0100
@@ -0,0 +1,536 @@
+%
+\begin{isabellebody}%
+\def\isabellecontext{integration}%
+%
+\isadelimtheory
+\isanewline
+\isanewline
+\isanewline
+%
+\endisadelimtheory
+%
+\isatagtheory
+\isacommand{theory}\isamarkupfalse%
+\ integration\ \isakeyword{imports}\ base\ \isakeyword{begin}%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isamarkupchapter{System integration%
+}
+\isamarkuptrue%
+%
+\isamarkupsection{Isar toplevel%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+The Isar toplevel may be considered the centeral hub of the
+ Isabelle/Isar system, where all key components and sub-systems are
+ integrated into a single read-eval-print loop of Isar commands.
+ Here we even incorporate the existing {\ML} toplevel of the compiler
+ and run-time system (cf.\ \secref{sec:ML-toplevel}).
+
+ Isabelle/Isar departs from original ``LCF system architecture''
+ where {\ML} was really The Meta Language for defining theories and
+ conducting proofs. Instead, {\ML} merely serves as the
+ implementation language for the system (and user extensions), while
+ our specific Isar toplevel supports particular notions of
+ incremental theory and proof development more directly. This
+ includes the graph structure of theories and the block structure of
+ proofs, support for unlimited undo, facilities for tracing,
+ debugging, timing, profiling.
+
+ \medskip The toplevel maintains an implicit state, which is
+ transformed by a sequence of transitions -- either interactively or
+ in batch-mode. In interactive mode, Isar state transitions are
+ encapsulated as safe transactions, such that both failure and undo
+ are handled conveniently without destroying the underlying draft
+ theory (cf.~\secref{sec:context-theory}). In batch mode,
+ transitions operate in a strictly linear (destructive) fashion, such
+ that error conditions abort the present attempt to construct a
+ theory altogether.
+
+ The toplevel state is a disjoint sum of empty \isa{toplevel}, or
+ \isa{theory}, or \isa{proof}. On entering the main Isar loop we
+ start with an empty toplevel. A theory is commenced by giving a
+ \isa{{\isasymTHEORY}} header; within a theory we may issue theory
+ commands such as \isa{{\isasymCONSTS}} or \isa{{\isasymDEFS}}, or state a
+ \isa{{\isasymTHEOREM}} to be proven. Now we are within a proof state,
+ with a rich collection of Isar proof commands for structured proof
+ composition, or unstructured proof scripts. When the proof is
+ concluded we get back to the theory, which is then updated by
+ storing the resulting fact. Further theory declarations or theorem
+ statements with proofs may follow, until we eventually conclude the
+ theory development by issuing \isa{{\isasymEND}}. The resulting theory
+ is then stored within the theory database and we are back to the
+ empty toplevel.
+
+ In addition to these proper state transformations, there are also
+ some diagnostic commands for peeking at the toplevel state without
+ modifying it (e.g.\ \isakeyword{thm}, \isakeyword{term},
+ \isakeyword{print-cases}).%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isatagmlref
+%
+\begin{isamarkuptext}%
+\begin{mldecls}
+ \indexmltype{Toplevel.state}\verb|type Toplevel.state| \\
+ \indexml{Toplevel.UNDEF}\verb|Toplevel.UNDEF: exn| \\
+ \indexml{Toplevel.is-toplevel}\verb|Toplevel.is_toplevel: Toplevel.state -> bool| \\
+ \indexml{Toplevel.theory-of}\verb|Toplevel.theory_of: Toplevel.state -> theory| \\
+ \indexml{Toplevel.proof-of}\verb|Toplevel.proof_of: Toplevel.state -> Proof.state| \\
+ \indexml{Toplevel.debug}\verb|Toplevel.debug: bool ref| \\
+ \indexml{Toplevel.timing}\verb|Toplevel.timing: bool ref| \\
+ \indexml{Toplevel.profiling}\verb|Toplevel.profiling: int ref| \\
+ \end{mldecls}
+
+ \begin{description}
+
+ \item \verb|Toplevel.state| represents Isar toplevel states,
+ which are normally only manipulated through the toplevel transition
+ concept (\secref{sec:toplevel-transition}). Also note that a
+ toplevel state is subject to the same linerarity restrictions as a
+ theory context (cf.~\secref{sec:context-theory}).
+
+ \item \verb|Toplevel.UNDEF| is raised for undefined toplevel
+ operations: \verb|Toplevel.state| is a sum type, many operations
+ work only partially for certain cases.
+
+ \item \verb|Toplevel.is_toplevel| checks for an empty toplevel state.
+
+ \item \verb|Toplevel.theory_of| gets the theory of a theory or proof
+ (!), otherwise raises \verb|Toplevel.UNDEF|.
+
+ \item \verb|Toplevel.proof_of| gets the Isar proof state if
+ available, otherwise raises \verb|Toplevel.UNDEF|.
+
+ \item \verb|set Toplevel.debug| makes the toplevel print further
+ details about internal error conditions, exceptions being raised
+ etc.
+
+ \item \verb|set Toplevel.timing| makes the toplevel print timing
+ information for each Isar command being executed.
+
+ \item \verb|Toplevel.profiling| controls low-level profiling of the
+ underlying {\ML} runtime system.\footnote{For Poly/ML, 1 means time
+ and 2 space profiling.}
+
+ \end{description}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagmlref
+{\isafoldmlref}%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isamarkupsubsection{Toplevel transitions%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+An Isar toplevel transition consists of a partial
+ function on the toplevel state, with additional information for
+ diagnostics and error reporting: there are fields for command name,
+ source position, optional source text, as well as flags for
+ interactive-only commands (which issue a warning in batch-mode),
+ printing of result state, etc.
+
+ The operational part is represented as a sequential union of a list
+ of partial functions, which are tried in turn until the first one
+ succeeds (i.e.\ does not raise \verb|Toplevel.UNDEF|). For example,
+ a single Isar command like \isacommand{qed} consists of the union of
+ some function \verb|Proof.state -> Proof.state| for proofs
+ within proofs, plus \verb|Proof.state -> theory| for proofs at
+ the outer theory level.
+
+ Toplevel transitions are composed via transition transformers.
+ Internally, Isar commands are put together from an empty transition
+ extended by name and source position (and optional source text). It
+ is then left to the individual command parser to turn the given
+ syntax body into a suitable transition transformer that adjoin
+ actual operations on a theory or proof state etc.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isatagmlref
+%
+\begin{isamarkuptext}%
+\begin{mldecls}
+ \indexml{Toplevel.print}\verb|Toplevel.print: Toplevel.transition -> Toplevel.transition| \\
+ \indexml{Toplevel.no-timing}\verb|Toplevel.no_timing: Toplevel.transition -> Toplevel.transition| \\
+ \indexml{Toplevel.keep}\verb|Toplevel.keep: (Toplevel.state -> unit) ->|\isasep\isanewline%
+\verb| Toplevel.transition -> Toplevel.transition| \\
+ \indexml{Toplevel.theory}\verb|Toplevel.theory: (theory -> theory) ->|\isasep\isanewline%
+\verb| Toplevel.transition -> Toplevel.transition| \\
+ \indexml{Toplevel.theory-to-proof}\verb|Toplevel.theory_to_proof: (theory -> Proof.state) ->|\isasep\isanewline%
+\verb| Toplevel.transition -> Toplevel.transition| \\
+ \indexml{Toplevel.proof}\verb|Toplevel.proof: (Proof.state -> Proof.state) ->|\isasep\isanewline%
+\verb| Toplevel.transition -> Toplevel.transition| \\
+ \indexml{Toplevel.proofs}\verb|Toplevel.proofs: (Proof.state -> Proof.state Seq.seq) ->|\isasep\isanewline%
+\verb| Toplevel.transition -> Toplevel.transition| \\
+ \indexml{Toplevel.proof-to-theory}\verb|Toplevel.proof_to_theory: (Proof.state -> theory) ->|\isasep\isanewline%
+\verb| Toplevel.transition -> Toplevel.transition| \\
+ \end{mldecls}
+
+ \begin{description}
+
+ \item \verb|Toplevel.print| sets the print flag, which causes the
+ resulting state of the transition to be echoed in interactive mode.
+
+ \item \verb|Toplevel.no_timing| indicates that the transition should
+ never show timing information, e.g.\ because it is merely a
+ diagnostic command.
+
+ \item \verb|Toplevel.keep| adjoins a diagnostic function.
+
+ \item \verb|Toplevel.theory| adjoins a theory transformer.
+
+ \item \verb|Toplevel.theory_to_proof| adjoins a global goal function,
+ which turns a theory into a proof state. The theory must not be
+ changed here! The generic Isar goal setup includes an argument that
+ specifies how to apply the proven result to the theory, when the
+ proof is finished.
+
+ \item \verb|Toplevel.proof| adjoins a deterministic proof command,
+ with a singleton result state.
+
+ \item \verb|Toplevel.proofs| adjoins a general proof command, with
+ zero or more result states (represented as a lazy list).
+
+ \item \verb|Toplevel.proof_to_theory| adjoins a concluding proof
+ command, that returns the resulting theory, after storing the
+ resulting facts etc.
+
+ \end{description}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagmlref
+{\isafoldmlref}%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isamarkupsubsection{Toplevel control%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Apart from regular toplevel transactions there are a few
+ special control commands that modify the behavior the toplevel
+ itself, and only make sense in interactive mode. Under normal
+ circumstances, the user encounters these only implicitly as part of
+ the protocol between the Isabelle/Isar system and a user-interface
+ such as ProofGeneral.
+
+ \begin{description}
+
+ \item \isacommand{undo} follows the three-level hierarchy of empty
+ toplevel vs.\ theory vs.\ proof: undo within a proof reverts to the
+ previous proof context, undo after a proof reverts to the theory
+ before the initial goal statement, undo of a theory command reverts
+ to the previous theory value, undo of a theory header discontinues
+ the current theory development and removes it from the theory
+ database (\secref{sec:theory-database}).
+
+ \item \isacommand{kill} aborts the current level of development:
+ kill in a proof context reverts to the theory before the initial
+ goal statement, kill in a theory context aborts the current theory
+ development, removing it from the database.
+
+ \item \isacommand{exit} drops out of the Isar toplevel into the
+ underlying {\ML} toplevel (\secref{sec:ML-toplevel}). The Isar
+ toplevel state is preserved and may be continued later.
+
+ \item \isacommand{quit} terminates the Isabelle/Isar process without
+ saving.
+
+ \end{description}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsection{ML toplevel \label{sec:ML-toplevel}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+The {\ML} toplevel provides a read-compile-eval-print loop for
+ {\ML} values, types, structures, and functors. {\ML} declarations
+ operate on the global system state, which consists of the compiler
+ environment plus the values of {\ML} reference variables. There is
+ no clean way to undo {\ML} declarations, except for reverting to a
+ previously saved state of the whole Isabelle process. {\ML} input
+ is either read interactively from a TTY, or from a string (usually
+ within a theory text), or from a source file (usually associated
+ with a theory).
+
+ Whenever the {\ML} toplevel is active, the current Isabelle theory
+ context is passed as an internal reference variable. Thus {\ML}
+ code may access the theory context during compilation, it may even
+ change the value of a theory being under construction --- following
+ the usual linearity restrictions (cf.~\secref{sec:context-theory}).%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isatagmlref
+%
+\begin{isamarkuptext}%
+\begin{mldecls}
+ \indexml{context}\verb|context: theory -> unit| \\
+ \indexml{the-context}\verb|the_context: unit -> theory| \\
+ \indexml{Context.$>$$>$ }\verb|Context.>> : (theory -> theory) -> unit| \\
+ \end{mldecls}
+
+ \begin{description}
+
+ \item \verb|context|~\isa{thy} sets the {\ML} theory context to
+ \isa{thy}. This is usually performed automatically by the system,
+ when dropping out of the interactive Isar toplevel into {\ML}, or
+ when Isar invokes {\ML} to process code from a string or a file.
+
+ \item \verb|the_context ()| refers to the theory context of the
+ {\ML} toplevel --- at compile time! {\ML} code needs to take care
+ to refer to \verb|the_context ()| correctly, recall that evaluation
+ of a function body is delayed until actual runtime. Moreover,
+ persistent {\ML} toplevel bindings to an unfinished theory should be
+ avoided: code should either project out the desired information
+ immediately, or produce an explicit \verb|theory_ref| (cf.\
+ \secref{sec:context-theory}).
+
+ \item \verb|Context.>>|~\isa{f} applies theory transformation
+ \isa{f} to the current theory of the {\ML} toplevel. In order to
+ work as expected, the theory should be still under construction, and
+ the Isar language element that invoked the {\ML} compiler in the
+ first place shoule be ready to accept the changed theory value
+ (e.g.\ \isakeyword{ML-setup}, but not plain \isakeyword{ML}).
+ Otherwise the theory may get destroyed!
+
+ \end{description}
+
+ It is very important to note that the above functions are really
+ restricted to the compile time, even though the {\ML} compiler is
+ invoked at runtime! The majority of {\ML} code uses explicit
+ functional arguments of a theory or proof context, as required.
+ Thus it may get run in an arbitrary context later on.
+
+ \bigskip
+
+ \begin{mldecls}
+ \indexml{Isar.main}\verb|Isar.main: unit -> unit| \\
+ \indexml{Isar.loop}\verb|Isar.loop: unit -> unit| \\
+ \indexml{Isar.state}\verb|Isar.state: unit -> Toplevel.state| \\
+ \indexml{Isar.exn}\verb|Isar.exn: unit -> (exn * string) option| \\
+ \end{mldecls}
+
+ \begin{description}
+
+ \item \verb|Isar.main ()| invokes the Isar toplevel from {\ML},
+ initializing the state to empty toplevel state.
+
+ \item \verb|Isar.loop ()| continues the Isar toplevel with the
+ current state, after dropping out of the Isar toplevel loop.
+
+ \item \verb|Isar.state ()| and \verb|Isar.exn ()| get current
+ toplevel state and optional error condition, respectively. This
+ only works after dropping out of the Isar toplevel loop.
+
+ \end{description}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagmlref
+{\isafoldmlref}%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isamarkupsection{Theory database%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+The theory database maintains a collection of theories,
+ together with some administrative information about the original
+ sources, which are held in an external store (i.e.\ a collection of
+ directories within the regular file system of the underlying
+ platform).
+
+ The theory database is organized as a directed acyclic graph, with
+ entries referenced by theory name. Although some external
+ interfaces allow to include a directory specification, this is only
+ a hint to the underlying theory loader mechanism: the internal
+ theory name space is flat.
+
+ Theory \isa{A} is associated with the main theory file \isa{A}\verb,.thy,, which needs to be accessible through the theory
+ loader path. A number of optional {\ML} source files may be
+ associated with each theory, by declaring these dependencies in the
+ theory header as \isa{{\isasymUSES}}, and loading them consecutively
+ within the theory context. The system keeps track of incoming {\ML}
+ sources and associates them with the current theory. The special
+ theory {\ML} file \isa{A}\verb,.ML, is loaded after a theory has
+ been concluded, in order to support legacy proof {\ML} proof
+ scripts.
+
+ The basic internal actions of the theory database are \isa{update}\indexbold{\isa{update} theory}, \isa{outdate}\indexbold{\isa{outdate} theory}, and \isa{remove}\indexbold{\isa{remove} theory}:
+
+ \begin{itemize}
+
+ \item \isa{update\ A} introduces a link of \isa{A} with a
+ \isa{theory} value of the same name; it asserts that the theory
+ sources are consistent with that value.
+
+ \item \isa{outdate\ A} invalidates the link of a theory database
+ entry to its sources, but retains the present theory value.
+
+ \item \isa{remove\ A} removes entry \isa{A} from the theory
+ database.
+
+ \end{itemize}
+
+ These actions are propagated to sub- or super-graphs of a theory
+ entry in the usual way, in order to preserve global consistency of
+ the state of all loaded theories with the sources of the external
+ store. This implies causal dependencies of certain actions: \isa{update} or \isa{outdate} of an entry will \isa{outdate}
+ all descendants; \isa{remove} will \isa{remove} all
+ descendants.
+
+ \medskip There are separate user-level interfaces to operate on the
+ theory database directly or indirectly. The primitive actions then
+ just happen automatically while working with the system. In
+ particular, processing a theory header \isa{{\isasymTHEORY}\ A\ {\isasymIMPORTS}\ B\isactrlsub {\isadigit{1}}\ {\isasymdots}\ B\isactrlsub n\ {\isasymBEGIN}} ensure that the
+ sub-graph of the collective imports \isa{B\isactrlsub {\isadigit{1}}\ {\isasymdots}\ B\isactrlsub n}
+ is up-to-date. Earlier theories are reloaded as required, with
+ \isa{update} actions proceeding in topological order according to
+ theory dependencies. There may be also a wave of implied \isa{outdate} actions for derived theory nodes until a stable situation
+ is achieved eventually.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isatagmlref
+%
+\begin{isamarkuptext}%
+\begin{mldecls}
+ \indexml{theory}\verb|theory: string -> theory| \\
+ \indexml{use-thy}\verb|use_thy: string -> unit| \\
+ \indexml{update-thy}\verb|update_thy: string -> unit| \\
+ \indexml{use-thy-only}\verb|use_thy_only: string -> unit| \\
+ \indexml{update-thy-only}\verb|update_thy_only: string -> unit| \\
+ \indexml{touch-thy}\verb|touch_thy: string -> unit| \\
+ \indexml{remove-thy}\verb|remove_thy: string -> unit| \\[1ex]
+ \indexml{ThyInfo.begin-theory}\verb|ThyInfo.begin_theory|\verb|: ... -> bool -> theory| \\
+ \indexml{ThyInfo.end-theory}\verb|ThyInfo.end_theory: theory -> theory| \\
+ \indexml{ThyInfo.register-theory}\verb|ThyInfo.register_theory: theory -> unit| \\[1ex]
+ \verb|datatype action = Update |\verb,|,\verb| Outdate |\verb,|,\verb| Remove| \\
+ \indexml{ThyInfo.add-hook}\verb|ThyInfo.add_hook: (ThyInfo.action -> string -> unit) -> unit| \\
+ \end{mldecls}
+
+ \begin{description}
+
+ \item \verb|theory|~\isa{A} retrieves the theory value presently
+ associated with \isa{A}. The result is not necessarily
+ up-to-date!
+
+ \item \verb|use_thy|~\isa{A} loads theory \isa{A} if it is absent
+ or out-of-date. It ensures that all parent theories are available
+ as well, but does not reload them if older versions are already
+ present.
+
+ \item \verb|update_thy| is similar to \verb|use_thy|, but ensures that
+ the \isa{A} and all of its ancestors are fully up-to-date.
+
+ \item \verb|use_thy_only|~\isa{A} is like \verb|use_thy|~\isa{A},
+ but refrains from loading the attached \isa{A}\verb,.ML, file.
+ This is occasionally useful in replaying legacy {\ML} proof scripts
+ by hand.
+
+ \item \verb|update_thy_only| is analogous to \verb|use_thy_only|, but
+ proceeds like \verb|update_thy| for ancestors.
+
+ \item \verb|touch_thy|~\isa{A} performs \isa{outdate} action on
+ theory \isa{A} and all of its descendants.
+
+ \item \verb|remove_thy|~\isa{A} removes \isa{A} and all of its
+ descendants from the theory database.
+
+ \item \verb|ThyInfo.begin_theory| is the basic operation behind a
+ \isa{{\isasymTHEORY}} header declaration. The boolean argument
+ indicates the strictness of treating ancestors: for \verb|true| (as
+ in interactive mode) like \verb|update_thy|, and for \verb|false| (as
+ in batch mode) like \verb|use_thy|. This is {\ML} functions is
+ normally not invoked directly.
+
+ \item \verb|ThyInfo.end_theory| concludes the loading of a theory
+ proper; an attached theory {\ML} file may be still loaded later on.
+ This is {\ML} functions is normally not invoked directly.
+
+ \item \verb|ThyInfo.register_theory|~{text thy} registers an existing
+ theory value with the theory loader database. There is no
+ management of associated sources; this is mainly for bootstrapping.
+
+ \item \verb|ThyInfo.add_hook|~\isa{f} registers function \isa{f} as a hook for theory database actions. The function will be
+ invoked with the action and theory name being involved; thus derived
+ actions may be performed in associated system components, e.g.\
+ maintaining the state of an editor for theory sources.
+
+ The kind and order of actions occurring in practice depends both on
+ user interactions and the internal process of resolving theory
+ imports. Hooks should not rely on a particular policy here! Any
+ exceptions raised by the hook are ignored by the theory database.
+
+ \end{description}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagmlref
+{\isafoldmlref}%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isatagtheory
+\isacommand{end}\isamarkupfalse%
+%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+\isanewline
+\end{isabellebody}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarImplementation/Thy/document/locale.tex Mon Jan 02 20:16:52 2006 +0100
@@ -0,0 +1,62 @@
+%
+\begin{isabellebody}%
+\def\isabellecontext{locale}%
+%
+\isadelimtheory
+\isanewline
+\isanewline
+\isanewline
+%
+\endisadelimtheory
+%
+\isatagtheory
+\isacommand{theory}\isamarkupfalse%
+\ {\isachardoublequoteopen}locale{\isachardoublequoteclose}\ \isakeyword{imports}\ base\ \isakeyword{begin}%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isamarkupchapter{Structured specifications%
+}
+\isamarkuptrue%
+%
+\isamarkupsection{Specification elements%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+FIXME%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsection{Locales%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+FIXME%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isatagtheory
+\isacommand{end}\isamarkupfalse%
+%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+\isanewline
+\end{isabellebody}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarImplementation/Thy/document/logic.tex Mon Jan 02 20:16:52 2006 +0100
@@ -0,0 +1,192 @@
+%
+\begin{isabellebody}%
+\def\isabellecontext{logic}%
+%
+\isadelimtheory
+\isanewline
+\isanewline
+\isanewline
+%
+\endisadelimtheory
+%
+\isatagtheory
+\isacommand{theory}\isamarkupfalse%
+\ logic\ \isakeyword{imports}\ base\ \isakeyword{begin}%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isamarkupchapter{Pure logic%
+}
+\isamarkuptrue%
+%
+\isamarkupsection{Syntax%
+}
+\isamarkuptrue%
+%
+\isamarkupsubsection{Simply-typed lambda calculus%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+FIXME
+
+\glossary{Type}{FIXME}
+\glossary{Term}{FIXME}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{The order-sorted algebra of types%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+FIXME
+
+\glossary{Type constructor}{FIXME}
+
+\glossary{Type class}{FIXME}
+
+\glossary{Type arity}{FIXME}
+
+\glossary{Sort}{FIXME}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Type-inference and schematic polymorphism%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+FIXME
+
+\glossary{Schematic polymorphism}{FIXME}
+
+\glossary{Type variable}{FIXME}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsection{Theory%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+FIXME
+
+\glossary{Constant}{Essentially a \seeglossary{fixed variable} of the
+theory context, but slightly more flexible since it may be used at
+different type-instances, due to \seeglossary{schematic
+polymorphism.}}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsection{Deduction%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+FIXME
+
+\glossary{Proposition}{A \seeglossary{term} of \seeglossary{type}
+\isa{prop}. Internally, there is nothing special about
+propositions apart from their type, but the concrete syntax enforces a
+clear distinction. Propositions are structured via implication \isa{A\ {\isasymLongrightarrow}\ B} or universal quantification \isa{{\isasymAnd}x{\isachardot}\ B\ x} --- anything
+else is considered atomic. The canonical form for propositions is
+that of a \seeglossary{Hereditary Harrop Formula}.}
+
+\glossary{Theorem}{A proven proposition within a certain theory and
+proof context, formally \isa{{\isasymGamma}\ {\isasymturnstile}\isactrlsub {\isasymTheta}\ {\isasymphi}}; both contexts are
+rarely spelled out explicitly. Theorems are usually normalized
+according to the \seeglossary{HHF} format.}
+
+\glossary{Fact}{Sometimes used interchangably for
+\seeglossary{theorem}. Strictly speaking, a list of theorems,
+essentially an extra-logical conjunction. Facts emerge either as
+local assumptions, or as results of local goal statements --- both may
+be simultaneous, hence the list representation.}
+
+\glossary{Schematic variable}{FIXME}
+
+\glossary{Fixed variable}{A variable that is bound within a certain
+proof context; an arbitrary-but-fixed entity within a portion of proof
+text.}
+
+\glossary{Free variable}{Synonymous for \seeglossary{fixed variable}.}
+
+\glossary{Bound variable}{FIXME}
+
+\glossary{Variable}{See \seeglossary{schematic variable},
+\seeglossary{fixed variable}, \seeglossary{bound variable}, or
+\seeglossary{type variable}. The distinguishing feature of different
+variables is their binding scope.}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Primitive inferences%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+FIXME%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Higher-order resolution%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+FIXME
+
+\glossary{Hereditary Harrop Formula}{The set of propositions in HHF
+format is defined inductively as \isa{H\ {\isacharequal}\ {\isacharparenleft}{\isasymAnd}x\isactrlsup {\isacharasterisk}{\isachardot}\ H\isactrlsup {\isacharasterisk}\ {\isasymLongrightarrow}\ A{\isacharparenright}}, for variables \isa{x} and atomic propositions \isa{A}.
+Any proposition may be put into HHF form by normalizing with the rule
+\isa{{\isacharparenleft}A\ {\isasymLongrightarrow}\ {\isacharparenleft}{\isasymAnd}x{\isachardot}\ B\ x{\isacharparenright}{\isacharparenright}\ {\isasymequiv}\ {\isacharparenleft}{\isasymAnd}x{\isachardot}\ A\ {\isasymLongrightarrow}\ B\ x{\isacharparenright}}. In Isabelle, the outermost
+quantifier prefix is represented via \seeglossary{schematic
+variables}, such that the top-level structure is merely that of a
+\seeglossary{Horn Clause}}.
+
+\glossary{HHF}{See \seeglossary{Hereditary Harrop Formula}.}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Equational reasoning%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+FIXME%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsection{Proof terms%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+FIXME%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isatagtheory
+\isacommand{end}\isamarkupfalse%
+%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+\isanewline
+\end{isabellebody}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarImplementation/Thy/document/prelim.tex Mon Jan 02 20:16:52 2006 +0100
@@ -0,0 +1,443 @@
+%
+\begin{isabellebody}%
+\def\isabellecontext{prelim}%
+%
+\isadelimtheory
+\isanewline
+\isanewline
+\isanewline
+%
+\endisadelimtheory
+%
+\isatagtheory
+\isacommand{theory}\isamarkupfalse%
+\ prelim\ \isakeyword{imports}\ base\ \isakeyword{begin}%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isamarkupchapter{Preliminaries%
+}
+\isamarkuptrue%
+%
+\isamarkupsection{Named entities%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Named entities of different kinds (logical constant, type,
+type class, theorem, method etc.) live in separate name spaces. It is
+usually clear from the occurrence of a name which kind of entity it
+refers to. For example, proof method \isa{foo} vs.\ theorem
+\isa{foo} vs.\ logical constant \isa{foo} are easily
+distinguished by means of the syntactic context. A notable exception
+are logical identifiers within a term (\secref{sec:terms}): constants,
+fixed variables, and bound variables all share the same identifier
+syntax, but are distinguished by their scope.
+
+Each name space is organized as a collection of \emph{qualified
+names}, which consist of a sequence of basic name components separated
+by dots: \isa{Bar{\isachardot}bar{\isachardot}foo}, \isa{Bar{\isachardot}foo}, and \isa{foo}
+are examples for valid qualified names. Name components are
+subdivided into \emph{symbols}, which constitute the smallest textual
+unit in Isabelle --- raw characters are normally not encountered
+directly.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Strings of symbols%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Isabelle strings consist of a sequence of
+symbols\glossary{Symbol}{The smalles unit of text in Isabelle,
+subsumes plain ASCII characters as well as an infinite collection of
+named symbols (for greek, math etc.).}, which are either packed as an
+actual \isa{string}, or represented as a list. Each symbol is in
+itself a small string of the following form:
+
+\begin{enumerate}
+
+\item either a singleton ASCII character ``\isa{c}'' (with
+character code 0--127), for example ``\verb,a,'',
+
+\item or a regular symbol ``\verb,\,\verb,<,\isa{ident}\verb,>,'',
+for example ``\verb,\,\verb,<alpha>,'',
+
+\item or a control symbol ``\verb,\,\verb,<^,\isa{ident}\verb,>,'', for example ``\verb,\,\verb,<^bold>,'',
+
+\item or a raw control symbol ``\verb,\,\verb,<^raw:,\isa{{\isasymdots}}\verb,>,'' where ``\isa{{\isasymdots}}'' refers to any printable ASCII
+character (excluding ``\verb,>,'') or non-ASCII character, for example
+``\verb,\,\verb,<^raw:$\sum_{i = 1}^n$>,'',
+
+\item or a numbered raw control symbol ``\verb,\,\verb,<^raw,\isa{nnn}\verb,>, where \isa{nnn} are digits, for example
+``\verb,\,\verb,<^raw42>,''.
+
+\end{enumerate}
+
+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
+control symbols available, but a certain collection of standard
+symbols is treated specifically. For example,
+``\verb,\,\verb,<alpha>,'' is classified as a (non-ASCII) letter,
+which means it may occur within regular Isabelle identifier syntax.
+
+Output of symbols depends on the print mode (\secref{sec:print-mode}).
+For example, the standard {\LaTeX} setup of the Isabelle document
+preparation system would present ``\verb,\,\verb,<alpha>,'' as \isa{{\isasymalpha}}, and ``\verb,\,\verb,<^bold>,\verb,\,\verb,<alpha>,'' as \isa{\isactrlbold {\isasymalpha}}.
+
+\medskip It is important to note that the character set underlying
+Isabelle symbols is plain 7-bit ASCII. Since 8-bit characters are
+passed through transparently, Isabelle may easily process actual
+Unicode/UCS data (using the well-known UTF-8 encoding, for example).
+Unicode provides its own collection of mathematical symbols, but there
+is presently no link to Isabelle's named ones; both kinds of symbols
+coexist independently.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isatagmlref
+%
+\begin{isamarkuptext}%
+\begin{mldecls}
+ \indexmltype{Symbol.symbol}\verb|type Symbol.symbol| \\
+ \indexml{Symbol.explode}\verb|Symbol.explode: string -> Symbol.symbol list| \\
+ \indexml{Symbol.is-letter}\verb|Symbol.is_letter: Symbol.symbol -> bool| \\
+ \indexml{Symbol.is-digit}\verb|Symbol.is_digit: Symbol.symbol -> bool| \\
+ \indexml{Symbol.is-quasi}\verb|Symbol.is_quasi: Symbol.symbol -> bool| \\
+ \indexml{Symbol.is-blank}\verb|Symbol.is_blank: Symbol.symbol -> bool| \\
+ \indexmltype{Symbol.sym}\verb|type Symbol.sym| \\
+ \indexml{Symbol.decode}\verb|Symbol.decode: Symbol.symbol -> Symbol.sym| \\
+ \end{mldecls}
+
+ \begin{description}
+
+ \item \verb|Symbol.symbol| represents Isabelle symbols; this type
+ is merely an alias for \verb|string|, but emphasizes the
+ specific format encountered here.
+
+ \item \verb|Symbol.explode|~\isa{s} produces an actual symbol
+ list from the packed form usually encountered as user input. This
+ function replaces \verb|String.explode| for virtually all purposes
+ of manipulating text in Isabelle! Plain \isa{implode} may be
+ used for the reverse operation.
+
+ \item \verb|Symbol.is_letter|, \verb|Symbol.is_digit|, \verb|Symbol.is_quasi|, \verb|Symbol.is_blank| classify certain symbols
+ (both ASCII and several named ones) according to fixed syntactic
+ convections of Isabelle, e.g.\ see \cite{isabelle-isar-ref}.
+
+ \item \verb|Symbol.sym| is a concrete datatype that represents
+ the different kinds of symbols explicitly as \verb|Symbol.Char|,
+ \verb|Symbol.Sym|, \verb|Symbol.Ctrl|, or \verb|Symbol.Raw|.
+
+ \item \verb|Symbol.decode| converts the string representation of a
+ symbol into the explicit datatype version.
+
+ \end{description}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagmlref
+{\isafoldmlref}%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isamarkupsubsection{Qualified names and name spaces%
+}
+\isamarkuptrue%
+%
+\isadelimFIXME
+%
+\endisadelimFIXME
+%
+\isatagFIXME
+%
+\begin{isamarkuptext}%
+Qualified names are constructed according to implicit naming
+principles of the present context.
+
+
+The last component is called \emph{base name}; the remaining prefix of
+qualification may be empty.
+
+Some practical conventions help to organize named entities more
+systematically:
+
+\begin{itemize}
+
+\item Names are qualified first by the theory name, second by an
+optional ``structure''. For example, a constant \isa{c} declared
+as part of a certain structure \isa{b} (say a type definition) in
+theory \isa{A} will be named \isa{A{\isachardot}b{\isachardot}c} internally.
+
+\item
+
+\item
+
+\item
+
+\item
+
+\end{itemize}
+
+Names of different kinds of entities are basically independent, but
+some practical naming conventions relate them to each other. For
+example, a constant \isa{foo} may be accompanied with theorems
+\isa{foo{\isachardot}intro}, \isa{foo{\isachardot}elim}, \isa{foo{\isachardot}simps} etc. The
+same may happen for a type \isa{foo}, which is then apt to cause
+clashes in the theorem name space! To avoid this, we occasionally
+follow an additional convention of suffixes that determine the
+original kind of entity that a name has been derived. For example,
+constant \isa{foo} is associated with 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}.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagFIXME
+{\isafoldFIXME}%
+%
+\isadelimFIXME
+%
+\endisadelimFIXME
+%
+\isamarkupsection{Structured output%
+}
+\isamarkuptrue%
+%
+\isamarkupsubsection{Pretty printing%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+FIXME%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Output channels%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+FIXME%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Print modes%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+FIXME%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsection{Context \label{sec:context}%
+}
+\isamarkuptrue%
+%
+\isadelimFIXME
+%
+\endisadelimFIXME
+%
+\isatagFIXME
+%
+\begin{isamarkuptext}%
+What is a context anyway? A highly advanced
+technological and cultural achievement, which took humanity several
+thousands of years to be develop, is writing with pen-and-paper. Here
+the paper is the context, or medium. It accommodates a certain range
+of different kinds of pens, but also has some inherent limitations.
+For example, carved inscriptions are better done on solid material
+like wood or stone.
+
+Isabelle/Isar distinguishes two key notions of context: \emph{theory
+ context}\indexbold{theory context} and \emph{proof context}.\indexbold{proof
+ context} To motivate this fundamental division consider the very idea of
+logical reasoning which is about judgments $\Gamma \Drv{\Theta} \phi$, where
+$\Theta$ is the background theory with declarations of operators and axioms
+stating their properties, and $\Gamma$ a collection of hypotheses emerging
+temporarily during proof. For example, the rule of implication-introduction
+\[
+\infer{\Gamma \Drv{\Theta} A \Imp B}{\Gamma, A \Drv{\Theta} B}
+\]
+can be read as ``to show $A \Imp B$ we may assume $A$ as hypothesis and need
+to show $B$''. It is characteristic that $\Theta$ is unchanged and $\Gamma$
+is only modified according to some general patterns of ``assuming'' and
+``discharging'' hypotheses. This admits the following abbreviated notation,
+where the fixed $\Theta$ and locally changed $\Gamma$ are left implicit:
+\[
+\infer{A \Imp B}{\infer*{B}{[A]}}
+\]
+
+In some logical traditions (e.g.\ Type Theory) there is a tendency to
+unify all kinds of declarations within a single notion of context.
+This is theoretically very nice, but also more demanding, because
+everything is internalized into the logical calculus itself.
+Isabelle/Pure is a very simple logic, but achieves many practically
+useful concepts by differentiating various basic elements.
+
+Take polymorphism, for example. Instead of embarking on the
+adventurous enterprise of full higher-order logic with full
+type-quantification and polymorphic entities, Isabelle/Pure merely
+takes a stripped-down version of Church's Simple Type Theory
+\cite{church40}. Then after the tradition of Gordon's HOL
+\cite{mgordon-hol} it is fairly easy to introduce syntactic notions of
+type variables and type-constructors, and require every theory
+$\Theta$ being closed by type instantiation. Whenever we wish to
+reason with a polymorphic constant or axiom scheme at a particular
+type, we may assume that it has been referenced initially at that very
+instance (due to the Deduction Theorem). Thus we achieve the
+following \emph{admissible
+ rule}\glossary{Admissible rule}{FIXME} of schematic type-instantiation:
+
+\[
+\infer{\phi(\tau)}{\infer*{\phi(\alpha)}{[\alpha]}}
+\]
+
+Using this approach, the structured Isar proof language offers
+schematic polymorphism within nested sub-proofs -- similar to that of
+polymorphic let-bindings according to Hindley-Milner.\
+\cite{milner78}. All of this is achieved without disintegrating the
+rather simplistic logical core. On the other hand, the succinct rule
+presented above already involves rather delicate interaction of the
+theory and proof context (with side-conditions not mentioned here),
+and unwinding an admissible rule involves induction over derivations.
+All of this diversity needs to be accomodated by the system
+architecture and actual implementation.
+
+\medskip Despite these important observations, Isabelle/Isar is not just a
+logical calculus, there are further extra-logical aspects to be considered.
+Practical experience over the years suggests two context data structures which
+are used in rather dissimilar manners, even though there is a considerable
+overlap of underlying ideas.
+
+From the system's perspective the mode of use of theory vs.\ proof context is
+the key distinction. The actual content is merely a generic slot for
+\emph{theory data} and \emph{proof data}, respectively. There are generic
+interfaces to declare data entries at any time. Even the core logic of
+Isabelle/Pure registers its very own notion of theory context data (types,
+constants, axioms etc.) like any other Isabelle tool out there. Likewise, the
+essentials of Isar proof contexts are one proof data slot among many others,
+notably those of derived Isar concepts (e.g.\ calculational reasoning rules).
+
+In that respect, a theory is more like a stone tablet to carve long-lasting
+inscriptions -- but take care not to break it! While a proof context is like
+a block of paper to scribble and dispose quickly. More recently Isabelle has
+started to cultivate the paper-based craftsmanship a bit further, by
+maintaining small collections of paper booklets, better known as locales.
+
+Thus we achive ``thick'' augmented versions of {\boldmath$\Theta$} and
+{\boldmath$\Gamma$} to support realistic structured reasoning within a
+practically usable system.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagFIXME
+{\isafoldFIXME}%
+%
+\isadelimFIXME
+%
+\endisadelimFIXME
+%
+\isamarkupsubsection{Theory context \label{sec:context-theory}%
+}
+\isamarkuptrue%
+%
+\isadelimFIXME
+%
+\endisadelimFIXME
+%
+\isatagFIXME
+%
+\begin{isamarkuptext}%
+A theory context consists of management information plus the
+actual data, which may be declared by other software modules later on.
+The management part is surprisingly complex, we illustrate it by the
+following typical situation of incremental theory development.
+
+\begin{tabular}{rcccl}
+ & & $Pure$ \\
+ & & $\downarrow$ \\
+ & & $FOL$ \\
+ & $\swarrow$ & & $\searrow$ & \\
+ $Nat$ & & & & $List$ \\
+ & $\searrow$ & & $\swarrow$ \\
+ & & $Length$ \\
+ & & \multicolumn{3}{l}{~~$\isarkeyword{imports}$} \\
+ & & \multicolumn{3}{l}{~~$\isarkeyword{begin}$} \\
+ & & $\vdots$~~ \\
+ & & $\bullet$~~ \\
+ & & $\vdots$~~ \\
+ & & $\bullet$~~ \\
+ & & $\vdots$~~ \\
+ & & \multicolumn{3}{l}{~~$\isarkeyword{end}$} \\
+\end{tabular}
+
+\begin{itemize}
+\item \emph{name}, \emph{parents} and \emph{ancestors}
+\item \emph{identity}
+\item \emph{intermediate versions}
+\end{itemize}
+
+\begin{description}
+\item [draft]
+\item [intermediate]
+\item [finished]
+\end{description}
+
+\emph{theory reference}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagFIXME
+{\isafoldFIXME}%
+%
+\isadelimFIXME
+%
+\endisadelimFIXME
+%
+\isamarkupsubsection{Proof context \label{sec:context-proof}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+FIXME
+
+\glossary{Proof context}{The static context of a structured proof,
+acts like a local ``theory'' of the current portion of Isar proof
+text, generalizes the idea of local hypotheses \isa{{\isasymGamma}} in
+judgments \isa{{\isasymGamma}\ {\isasymturnstile}\ {\isasymphi}} of natural deduction calculi. There is a
+generic notion of introducing and discharging hypotheses. Arbritrary
+auxiliary context data may be adjoined.}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isatagtheory
+\isacommand{end}\isamarkupfalse%
+%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+\isanewline
+\end{isabellebody}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarImplementation/Thy/document/proof.tex Mon Jan 02 20:16:52 2006 +0100
@@ -0,0 +1,91 @@
+%
+\begin{isabellebody}%
+\def\isabellecontext{proof}%
+%
+\isadelimtheory
+\isanewline
+\isanewline
+\isanewline
+%
+\endisadelimtheory
+%
+\isatagtheory
+\isacommand{theory}\isamarkupfalse%
+\ {\isachardoublequoteopen}proof{\isachardoublequoteclose}\ \isakeyword{imports}\ base\ \isakeyword{begin}%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isamarkupchapter{Structured reasoning%
+}
+\isamarkuptrue%
+%
+\isamarkupsection{Proof context%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+FIXME%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsection{Proof state%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+FIXME
+
+\glossary{Proof state}{The whole configuration of a structured proof,
+consisting of a \seeglossary{proof context} and an optional
+\seeglossary{structured goal}. Internally, an Isar proof state is
+organized as a stack to accomodate block structure of proof texts.
+For historical reasons, a low-level \seeglossary{tactical goal} is
+occasionally called ``proof state'' as well.}
+
+\glossary{Structured goal}{FIXME}
+
+\glossary{Goal}{See \seeglossary{tactical goal} or \seeglossary{structured goal}. \norefpage}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsection{Methods%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+FIXME%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsection{Attributes%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+FIXME%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isatagtheory
+\isacommand{end}\isamarkupfalse%
+%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+\isanewline
+\end{isabellebody}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarImplementation/Thy/document/session.tex Mon Jan 02 20:16:52 2006 +0100
@@ -0,0 +1,20 @@
+\input{base.tex}
+
+\input{prelim.tex}
+
+\input{logic.tex}
+
+\input{tactic.tex}
+
+\input{proof.tex}
+
+\input{locale.tex}
+
+\input{integration.tex}
+
+\input{ML.tex}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarImplementation/Thy/document/tactic.tex Mon Jan 02 20:16:52 2006 +0100
@@ -0,0 +1,252 @@
+%
+\begin{isabellebody}%
+\def\isabellecontext{tactic}%
+%
+\isadelimtheory
+\isanewline
+\isanewline
+\isanewline
+%
+\endisadelimtheory
+%
+\isatagtheory
+\isacommand{theory}\isamarkupfalse%
+\ tactic\ \isakeyword{imports}\ base\ \isakeyword{begin}%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isamarkupchapter{Tactical theorem proving%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+The basic idea of tactical theorem proving is to refine the
+initial claim in a backwards fashion, until a solved form is reached.
+An intermediate goal consists of several subgoals that need to be
+solved in order to achieve the main statement; zero subgoals means
+that the proof may be finished. Goal refinement operations are called
+tactics; combinators for composing tactics are called tacticals.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsection{Goals \label{sec:tactical-goals}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Isabelle/Pure represents a goal\glossary{Tactical goal}{A
+theorem of \seeglossary{Horn Clause} form stating that a number of
+subgoals imply the main conclusion, which is marked as a protected
+proposition.} as a theorem stating that the subgoals imply the main
+goal: \isa{A\isactrlsub {\isadigit{1}}\ {\isasymLongrightarrow}\ {\isasymdots}\ {\isasymLongrightarrow}\ A\isactrlsub n\ {\isasymLongrightarrow}\ C}. The outermost goal
+structure is that of a Horn Clause\glossary{Horn Clause}{An iterated
+implication \isa{A\isactrlsub {\isadigit{1}}\ {\isasymLongrightarrow}\ {\isasymdots}\ {\isasymLongrightarrow}\ A\isactrlsub n\ {\isasymLongrightarrow}\ C}, without any
+outermost quantifiers. Strictly speaking, propositions \isa{A\isactrlsub i} need to be atomic in Horn Clauses, but Isabelle admits
+arbitrary substructure here (nested \isa{{\isasymLongrightarrow}} and \isa{{\isasymAnd}}
+connectives).}: an iterated implication without any
+quantifiers\footnote{Recall that outermost \isa{{\isasymAnd}x{\isachardot}\ {\isasymphi}{\isacharbrackleft}x{\isacharbrackright}} is
+always represented via schematic variables in the body: \isa{{\isasymphi}{\isacharbrackleft}{\isacharquery}x{\isacharbrackright}}. These may get instantiated during the course of
+reasoning.}. For \isa{n\ {\isacharequal}\ {\isadigit{0}}} a goal is solved.
+
+The structure of each subgoal \isa{A\isactrlsub i} is that of a general
+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
+\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
+certain types, and \isa{H\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ H\isactrlsub m} are goal
+hypotheses, i.e.\ facts that may be assumed locally. Together, this
+forms the goal context of the conclusion \isa{B} to be established.
+The goal hypotheses may be again arbitrary Harrop Formulas, although
+the level of nesting rarely exceeds 1--2 in practice.
+
+The main conclusion \isa{C} is internally marked as a protected
+proposition\glossary{Protected proposition}{An arbitrarily structured
+proposition \isa{C} which is forced to appear as atomic by
+wrapping it into a propositional identity operator; notation \isa{{\isacharhash}C}. Protecting a proposition prevents basic inferences from
+entering into that structure for the time being.}, which is
+occasionally represented explicitly by the notation \isa{{\isacharhash}C}.
+This ensures that the decomposition into subgoals and main conclusion
+is well-defined for arbitrarily structured claims.
+
+\medskip Basic goal management is performed via the following
+Isabelle/Pure rules:
+
+ \[
+ \infer[\isa{{\isacharparenleft}init{\isacharparenright}}]{\isa{C\ {\isasymLongrightarrow}\ {\isacharhash}C}}{} \qquad
+ \infer[\isa{{\isacharparenleft}finish{\isacharparenright}}]{\isa{{\isacharhash}C}}{\isa{C}}
+ \]
+
+ \medskip The following low-level variants admit general reasoning
+ with protected propositions:
+
+ \[
+ \infer[\isa{{\isacharparenleft}protect{\isacharparenright}}]{\isa{{\isacharhash}C}}{\isa{C}} \qquad
+ \infer[\isa{{\isacharparenleft}conclude{\isacharparenright}}]{\isa{A\isactrlsub {\isadigit{1}}\ {\isasymLongrightarrow}\ {\isasymdots}\ {\isasymLongrightarrow}\ A\isactrlsub n\ {\isasymLongrightarrow}\ C}}{\isa{A\isactrlsub {\isadigit{1}}\ {\isasymLongrightarrow}\ {\isasymdots}\ {\isasymLongrightarrow}\ A\isactrlsub n\ {\isasymLongrightarrow}\ {\isacharhash}C}}
+ \]%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isatagmlref
+%
+\begin{isamarkuptext}%
+\begin{mldecls}
+ \indexml{Goal.init}\verb|Goal.init: cterm -> thm| \\
+ \indexml{Goal.finish}\verb|Goal.finish: thm -> thm| \\
+ \indexml{Goal.protect}\verb|Goal.protect: thm -> thm| \\
+ \indexml{Goal.conclude}\verb|Goal.conclude: thm -> thm| \\
+ \end{mldecls}
+
+ \begin{description}
+
+ \item \verb|Goal.init|~\isa{{\isasymphi}} initializes a tactical goal with
+ the type-checked proposition \isa{{\isasymphi}}.
+
+ \item \verb|Goal.finish|~\isa{th} checks whether theorem \isa{th} is a solved goal configuration (zero subgoals), and concludes
+ the result by removing the goal protection.
+
+ \item \verb|Goal.protect|~\isa{th} protects the whole statement
+ of theorem \isa{th}.
+
+ \item \verb|Goal.conclude|~\isa{th} removes the goal protection
+ for any number of pending subgoals.
+
+ \end{description}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagmlref
+{\isafoldmlref}%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isamarkupsection{Tactics%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+FIXME
+
+\glossary{Tactic}{Any function that maps a \seeglossary{tactical goal}
+to a lazy sequence of possible sucessors. This scheme subsumes
+failure (empty result sequence), as well as lazy enumeration of proof
+search results. Error conditions are usually mapped to an empty
+result, which gives further tactics a chance to try in turn.
+Commonly, tactics either take an argument to address a particular
+subgoal, or operate on a certain range of subgoals in a uniform
+fashion. In any case, the main conclusion is normally left untouched,
+apart from instantiating \seeglossary{schematic variables}.}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsection{Tacticals%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+FIXME
+
+\glossary{Tactical}{A functional combinator for building up complex
+tactics from simpler ones. Typical tactical perform sequential
+composition, disjunction (choice), iteration, or goal addressing.
+Various search strategies may be expressed via tacticals.}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsection{Programmed proofs%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+In order to perform a complete tactical proof under program control,
+ one needs to set up an initial goal configuration, apply a tactic,
+ and finish the result, cf.\ the rules given in
+ \secref{sec:tactical-goals}. Further checks are required to ensure
+ that the result is actually an instance of the original claim --
+ ill-behaved tactics could have destroyed that information.
+
+ Several simultaneous claims may be handled within a single goal
+ statement by using meta-level conjunction internally.\footnote{This
+ is merely syntax for certain derived statements within
+ Isabelle/Pure, there is no need to introduce a separate conjunction
+ operator.} The whole configuration may be considered within a
+ context of arbitrary-but-fixed parameters and hypotheses, which will
+ be available as local facts during the proof and discharged into
+ implications in the result.
+
+ All of these administrative tasks are packaged into a separate
+ operation, such that the user merely needs to provide the statement
+ and tactic to be applied.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isatagmlref
+%
+\begin{isamarkuptext}%
+\begin{mldecls}
+ \indexml{Goal.prove}\verb|Goal.prove: theory -> string list -> term list -> term ->|\isasep\isanewline%
+\verb| (thm list -> tactic) -> thm| \\
+ \indexml{Goal.prove-multi}\verb|Goal.prove_multi: theory -> string list -> term list -> term list ->|\isasep\isanewline%
+\verb| (thm list -> tactic) -> thm list| \\
+ \end{mldecls}
+
+ \begin{description}
+
+ \item \verb|Goal.prove|~\isa{thy\ xs\ As\ C\ tac} states goal \isa{C} in the context of arbitrary-but-fixed parameters \isa{xs}
+ and hypotheses \isa{As} and applies tactic \isa{tac} to
+ solve it. The latter may depend on the local assumptions being
+ presented as facts. The result is essentially \isa{{\isasymAnd}xs{\isachardot}\ As\ {\isasymLongrightarrow}\ C}, but is normalized by pulling \isa{{\isasymAnd}} before \isa{{\isasymLongrightarrow}}
+ (the conclusion \isa{C} itself may be a rule statement), turning
+ the quantifier prefix into schematic variables, and generalizing
+ implicit type-variables.
+
+ Any additional fixed variables or hypotheses not being mentioned in
+ the initial statement are left unchanged --- programmed proofs may
+ well occur in a larger context.
+
+ \item \verb|Goal.prove_multi| is simular to \verb|Goal.prove|, but
+ states several conclusions simultaneously. \verb|Tactic.conjunction_tac| may be used to split these into individual
+ subgoals before commencing the actual proof.
+
+ \end{description}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagmlref
+{\isafoldmlref}%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isatagtheory
+\isacommand{end}\isamarkupfalse%
+%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+\isanewline
+\isanewline
+\end{isabellebody}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarImplementation/Thy/integration.thy Mon Jan 02 20:16:52 2006 +0100
@@ -0,0 +1,439 @@
+
+(* $Id$ *)
+
+theory integration imports base begin
+
+chapter {* System integration *}
+
+section {* Isar toplevel *}
+
+text {* The Isar toplevel may be considered the centeral hub of the
+ Isabelle/Isar system, where all key components and sub-systems are
+ integrated into a single read-eval-print loop of Isar commands.
+ Here we even incorporate the existing {\ML} toplevel of the compiler
+ and run-time system (cf.\ \secref{sec:ML-toplevel}).
+
+ Isabelle/Isar departs from original ``LCF system architecture''
+ where {\ML} was really The Meta Language for defining theories and
+ conducting proofs. Instead, {\ML} merely serves as the
+ implementation language for the system (and user extensions), while
+ our specific Isar toplevel supports particular notions of
+ incremental theory and proof development more directly. This
+ includes the graph structure of theories and the block structure of
+ proofs, support for unlimited undo, facilities for tracing,
+ debugging, timing, profiling.
+
+ \medskip The toplevel maintains an implicit state, which is
+ transformed by a sequence of transitions -- either interactively or
+ in batch-mode. In interactive mode, Isar state transitions are
+ encapsulated as safe transactions, such that both failure and undo
+ are handled conveniently without destroying the underlying draft
+ theory (cf.~\secref{sec:context-theory}). In batch mode,
+ transitions operate in a strictly linear (destructive) fashion, such
+ that error conditions abort the present attempt to construct a
+ theory altogether.
+
+ The toplevel state is a disjoint sum of empty @{text toplevel}, or
+ @{text theory}, or @{text proof}. On entering the main Isar loop we
+ start with an empty toplevel. A theory is commenced by giving a
+ @{text \<THEORY>} header; within a theory we may issue theory
+ commands such as @{text \<CONSTS>} or @{text \<DEFS>}, or state a
+ @{text \<THEOREM>} to be proven. Now we are within a proof state,
+ with a rich collection of Isar proof commands for structured proof
+ composition, or unstructured proof scripts. When the proof is
+ concluded we get back to the theory, which is then updated by
+ storing the resulting fact. Further theory declarations or theorem
+ statements with proofs may follow, until we eventually conclude the
+ theory development by issuing @{text \<END>}. The resulting theory
+ is then stored within the theory database and we are back to the
+ empty toplevel.
+
+ In addition to these proper state transformations, there are also
+ some diagnostic commands for peeking at the toplevel state without
+ modifying it (e.g.\ \isakeyword{thm}, \isakeyword{term},
+ \isakeyword{print-cases}).
+*}
+
+text %mlref {*
+ \begin{mldecls}
+ @{index_ML_type Toplevel.state} \\
+ @{index_ML Toplevel.UNDEF: "exn"} \\
+ @{index_ML Toplevel.is_toplevel: "Toplevel.state -> bool"} \\
+ @{index_ML Toplevel.theory_of: "Toplevel.state -> theory"} \\
+ @{index_ML Toplevel.proof_of: "Toplevel.state -> Proof.state"} \\
+ @{index_ML Toplevel.debug: "bool ref"} \\
+ @{index_ML Toplevel.timing: "bool ref"} \\
+ @{index_ML Toplevel.profiling: "int ref"} \\
+ \end{mldecls}
+
+ \begin{description}
+
+ \item @{ML_type Toplevel.state} represents Isar toplevel states,
+ which are normally only manipulated through the toplevel transition
+ concept (\secref{sec:toplevel-transition}). Also note that a
+ toplevel state is subject to the same linerarity restrictions as a
+ theory context (cf.~\secref{sec:context-theory}).
+
+ \item @{ML Toplevel.UNDEF} is raised for undefined toplevel
+ operations: @{ML_type Toplevel.state} is a sum type, many operations
+ work only partially for certain cases.
+
+ \item @{ML Toplevel.is_toplevel} checks for an empty toplevel state.
+
+ \item @{ML Toplevel.theory_of} gets the theory of a theory or proof
+ (!), otherwise raises @{ML Toplevel.UNDEF}.
+
+ \item @{ML Toplevel.proof_of} gets the Isar proof state if
+ available, otherwise raises @{ML Toplevel.UNDEF}.
+
+ \item @{ML "set Toplevel.debug"} makes the toplevel print further
+ details about internal error conditions, exceptions being raised
+ etc.
+
+ \item @{ML "set Toplevel.timing"} makes the toplevel print timing
+ information for each Isar command being executed.
+
+ \item @{ML Toplevel.profiling} controls low-level profiling of the
+ underlying {\ML} runtime system.\footnote{For Poly/ML, 1 means time
+ and 2 space profiling.}
+
+ \end{description}
+*}
+
+
+subsection {* Toplevel transitions *}
+
+text {* An Isar toplevel transition consists of a partial
+ function on the toplevel state, with additional information for
+ diagnostics and error reporting: there are fields for command name,
+ source position, optional source text, as well as flags for
+ interactive-only commands (which issue a warning in batch-mode),
+ printing of result state, etc.
+
+ The operational part is represented as a sequential union of a list
+ of partial functions, which are tried in turn until the first one
+ succeeds (i.e.\ does not raise @{ML Toplevel.UNDEF}). For example,
+ a single Isar command like \isacommand{qed} consists of the union of
+ some function @{ML_type "Proof.state -> Proof.state"} for proofs
+ within proofs, plus @{ML_type "Proof.state -> theory"} for proofs at
+ the outer theory level.
+
+ Toplevel transitions are composed via transition transformers.
+ Internally, Isar commands are put together from an empty transition
+ extended by name and source position (and optional source text). It
+ is then left to the individual command parser to turn the given
+ syntax body into a suitable transition transformer that adjoin
+ actual operations on a theory or proof state etc.
+*}
+
+text %mlref {*
+ \begin{mldecls}
+ @{index_ML Toplevel.print: "Toplevel.transition -> Toplevel.transition"} \\
+ @{index_ML Toplevel.no_timing: "Toplevel.transition -> Toplevel.transition"} \\
+ @{index_ML Toplevel.keep: "(Toplevel.state -> unit) ->
+ Toplevel.transition -> Toplevel.transition"} \\
+ @{index_ML Toplevel.theory: "(theory -> theory) ->
+ Toplevel.transition -> Toplevel.transition"} \\
+ @{index_ML Toplevel.theory_to_proof: "(theory -> Proof.state) ->
+ Toplevel.transition -> Toplevel.transition"} \\
+ @{index_ML Toplevel.proof: "(Proof.state -> Proof.state) ->
+ Toplevel.transition -> Toplevel.transition"} \\
+ @{index_ML Toplevel.proofs: "(Proof.state -> Proof.state Seq.seq) ->
+ Toplevel.transition -> Toplevel.transition"} \\
+ @{index_ML Toplevel.proof_to_theory: "(Proof.state -> theory) ->
+ Toplevel.transition -> Toplevel.transition"} \\
+ \end{mldecls}
+
+ \begin{description}
+
+ \item @{ML Toplevel.print} sets the print flag, which causes the
+ resulting state of the transition to be echoed in interactive mode.
+
+ \item @{ML Toplevel.no_timing} indicates that the transition should
+ never show timing information, e.g.\ because it is merely a
+ diagnostic command.
+
+ \item @{ML Toplevel.keep} adjoins a diagnostic function.
+
+ \item @{ML Toplevel.theory} adjoins a theory transformer.
+
+ \item @{ML Toplevel.theory_to_proof} adjoins a global goal function,
+ which turns a theory into a proof state. The theory must not be
+ changed here! The generic Isar goal setup includes an argument that
+ specifies how to apply the proven result to the theory, when the
+ proof is finished.
+
+ \item @{ML Toplevel.proof} adjoins a deterministic proof command,
+ with a singleton result state.
+
+ \item @{ML Toplevel.proofs} adjoins a general proof command, with
+ zero or more result states (represented as a lazy list).
+
+ \item @{ML Toplevel.proof_to_theory} adjoins a concluding proof
+ command, that returns the resulting theory, after storing the
+ resulting facts etc.
+
+ \end{description}
+*}
+
+
+subsection {* Toplevel control *}
+
+text {* Apart from regular toplevel transactions there are a few
+ special control commands that modify the behavior the toplevel
+ itself, and only make sense in interactive mode. Under normal
+ circumstances, the user encounters these only implicitly as part of
+ the protocol between the Isabelle/Isar system and a user-interface
+ such as ProofGeneral.
+
+ \begin{description}
+
+ \item \isacommand{undo} follows the three-level hierarchy of empty
+ toplevel vs.\ theory vs.\ proof: undo within a proof reverts to the
+ previous proof context, undo after a proof reverts to the theory
+ before the initial goal statement, undo of a theory command reverts
+ to the previous theory value, undo of a theory header discontinues
+ the current theory development and removes it from the theory
+ database (\secref{sec:theory-database}).
+
+ \item \isacommand{kill} aborts the current level of development:
+ kill in a proof context reverts to the theory before the initial
+ goal statement, kill in a theory context aborts the current theory
+ development, removing it from the database.
+
+ \item \isacommand{exit} drops out of the Isar toplevel into the
+ underlying {\ML} toplevel (\secref{sec:ML-toplevel}). The Isar
+ toplevel state is preserved and may be continued later.
+
+ \item \isacommand{quit} terminates the Isabelle/Isar process without
+ saving.
+
+ \end{description}
+*}
+
+
+section {* ML toplevel \label{sec:ML-toplevel} *}
+
+text {* The {\ML} toplevel provides a read-compile-eval-print loop for
+ {\ML} values, types, structures, and functors. {\ML} declarations
+ operate on the global system state, which consists of the compiler
+ environment plus the values of {\ML} reference variables. There is
+ no clean way to undo {\ML} declarations, except for reverting to a
+ previously saved state of the whole Isabelle process. {\ML} input
+ is either read interactively from a TTY, or from a string (usually
+ within a theory text), or from a source file (usually associated
+ with a theory).
+
+ Whenever the {\ML} toplevel is active, the current Isabelle theory
+ context is passed as an internal reference variable. Thus {\ML}
+ code may access the theory context during compilation, it may even
+ change the value of a theory being under construction --- following
+ the usual linearity restrictions (cf.~\secref{sec:context-theory}).
+*}
+
+text %mlref {*
+ \begin{mldecls}
+ @{index_ML context: "theory -> unit"} \\
+ @{index_ML the_context: "unit -> theory"} \\
+ @{index_ML "Context.>> ": "(theory -> theory) -> unit"} \\
+ \end{mldecls}
+
+ \begin{description}
+
+ \item @{ML context}~@{text thy} sets the {\ML} theory context to
+ @{text thy}. This is usually performed automatically by the system,
+ when dropping out of the interactive Isar toplevel into {\ML}, or
+ when Isar invokes {\ML} to process code from a string or a file.
+
+ \item @{ML "the_context ()"} refers to the theory context of the
+ {\ML} toplevel --- at compile time! {\ML} code needs to take care
+ to refer to @{ML "the_context ()"} correctly, recall that evaluation
+ of a function body is delayed until actual runtime. Moreover,
+ persistent {\ML} toplevel bindings to an unfinished theory should be
+ avoided: code should either project out the desired information
+ immediately, or produce an explicit @{ML_type theory_ref} (cf.\
+ \secref{sec:context-theory}).
+
+ \item @{ML "Context.>>"}~@{text f} applies theory transformation
+ @{text f} to the current theory of the {\ML} toplevel. In order to
+ work as expected, the theory should be still under construction, and
+ the Isar language element that invoked the {\ML} compiler in the
+ first place shoule be ready to accept the changed theory value
+ (e.g.\ \isakeyword{ML-setup}, but not plain \isakeyword{ML}).
+ Otherwise the theory may get destroyed!
+
+ \end{description}
+
+ It is very important to note that the above functions are really
+ restricted to the compile time, even though the {\ML} compiler is
+ invoked at runtime! The majority of {\ML} code uses explicit
+ functional arguments of a theory or proof context, as required.
+ Thus it may get run in an arbitrary context later on.
+
+ \bigskip
+
+ \begin{mldecls}
+ @{index_ML Isar.main: "unit -> unit"} \\
+ @{index_ML Isar.loop: "unit -> unit"} \\
+ @{index_ML Isar.state: "unit -> Toplevel.state"} \\
+ @{index_ML Isar.exn: "unit -> (exn * string) option"} \\
+ \end{mldecls}
+
+ \begin{description}
+
+ \item @{ML "Isar.main ()"} invokes the Isar toplevel from {\ML},
+ initializing the state to empty toplevel state.
+
+ \item @{ML "Isar.loop ()"} continues the Isar toplevel with the
+ current state, after dropping out of the Isar toplevel loop.
+
+ \item @{ML "Isar.state ()"} and @{ML "Isar.exn ()"} get current
+ toplevel state and optional error condition, respectively. This
+ only works after dropping out of the Isar toplevel loop.
+
+ \end{description}
+*}
+
+
+section {* Theory database *}
+
+text {* The theory database maintains a collection of theories,
+ together with some administrative information about the original
+ sources, which are held in an external store (i.e.\ a collection of
+ directories within the regular file system of the underlying
+ platform).
+
+ The theory database is organized as a directed acyclic graph, with
+ entries referenced by theory name. Although some external
+ interfaces allow to include a directory specification, this is only
+ a hint to the underlying theory loader mechanism: the internal
+ theory name space is flat.
+
+ Theory @{text A} is associated with the main theory file @{text
+ A}\verb,.thy,, which needs to be accessible through the theory
+ loader path. A number of optional {\ML} source files may be
+ associated with each theory, by declaring these dependencies in the
+ theory header as @{text \<USES>}, and loading them consecutively
+ within the theory context. The system keeps track of incoming {\ML}
+ sources and associates them with the current theory. The special
+ theory {\ML} file @{text A}\verb,.ML, is loaded after a theory has
+ been concluded, in order to support legacy proof {\ML} proof
+ scripts.
+
+ The basic internal actions of the theory database are @{text
+ "update"}\indexbold{@{text "update"} theory}, @{text
+ "outdate"}\indexbold{@{text "outdate"} theory}, and @{text
+ "remove"}\indexbold{@{text "remove"} theory}:
+
+ \begin{itemize}
+
+ \item @{text "update A"} introduces a link of @{text "A"} with a
+ @{text "theory"} value of the same name; it asserts that the theory
+ sources are consistent with that value.
+
+ \item @{text "outdate A"} invalidates the link of a theory database
+ entry to its sources, but retains the present theory value.
+
+ \item @{text "remove A"} removes entry @{text "A"} from the theory
+ database.
+
+ \end{itemize}
+
+ These actions are propagated to sub- or super-graphs of a theory
+ entry in the usual way, in order to preserve global consistency of
+ the state of all loaded theories with the sources of the external
+ store. This implies causal dependencies of certain actions: @{text
+ "update"} or @{text "outdate"} of an entry will @{text "outdate"}
+ all descendants; @{text "remove"} will @{text "remove"} all
+ descendants.
+
+ \medskip There are separate user-level interfaces to operate on the
+ theory database directly or indirectly. The primitive actions then
+ just happen automatically while working with the system. In
+ particular, processing a theory header @{text "\<THEORY> A
+ \<IMPORTS> B\<^sub>1 \<dots> B\<^sub>n \<BEGIN>"} ensure that the
+ sub-graph of the collective imports @{text "B\<^sub>1 \<dots> B\<^sub>n"}
+ is up-to-date. Earlier theories are reloaded as required, with
+ @{text update} actions proceeding in topological order according to
+ theory dependencies. There may be also a wave of implied @{text
+ outdate} actions for derived theory nodes until a stable situation
+ is achieved eventually.
+*}
+
+text %mlref {*
+ \begin{mldecls}
+ @{index_ML theory: "string -> theory"} \\
+ @{index_ML use_thy: "string -> unit"} \\
+ @{index_ML update_thy: "string -> unit"} \\
+ @{index_ML use_thy_only: "string -> unit"} \\
+ @{index_ML update_thy_only: "string -> unit"} \\
+ @{index_ML touch_thy: "string -> unit"} \\
+ @{index_ML remove_thy: "string -> unit"} \\[1ex]
+ @{index_ML ThyInfo.begin_theory}@{verbatim ": ... -> bool -> theory"} \\
+ @{index_ML ThyInfo.end_theory: "theory -> theory"} \\
+ @{index_ML ThyInfo.register_theory: "theory -> unit"} \\[1ex]
+ @{verbatim "datatype action = Update | Outdate | Remove"} \\
+ @{index_ML ThyInfo.add_hook: "(ThyInfo.action -> string -> unit) -> unit"} \\
+ \end{mldecls}
+
+ \begin{description}
+
+ \item @{ML theory}~@{text A} retrieves the theory value presently
+ associated with @{text A}. The result is not necessarily
+ up-to-date!
+
+ \item @{ML use_thy}~@{text A} loads theory @{text A} if it is absent
+ or out-of-date. It ensures that all parent theories are available
+ as well, but does not reload them if older versions are already
+ present.
+
+ \item @{ML update_thy} is similar to @{ML use_thy}, but ensures that
+ the @{text A} and all of its ancestors are fully up-to-date.
+
+ \item @{ML use_thy_only}~@{text A} is like @{ML use_thy}~@{text A},
+ but refrains from loading the attached @{text A}\verb,.ML, file.
+ This is occasionally useful in replaying legacy {\ML} proof scripts
+ by hand.
+
+ \item @{ML update_thy_only} is analogous to @{ML use_thy_only}, but
+ proceeds like @{ML update_thy} for ancestors.
+
+ \item @{ML touch_thy}~@{text A} performs @{text outdate} action on
+ theory @{text A} and all of its descendants.
+
+ \item @{ML remove_thy}~@{text A} removes @{text A} and all of its
+ descendants from the theory database.
+
+ \item @{ML ThyInfo.begin_theory} is the basic operation behind a
+ @{text \<THEORY>} header declaration. The boolean argument
+ indicates the strictness of treating ancestors: for @{ML true} (as
+ in interactive mode) like @{ML update_thy}, and for @{ML false} (as
+ in batch mode) like @{ML use_thy}. This is {\ML} functions is
+ normally not invoked directly.
+
+ \item @{ML ThyInfo.end_theory} concludes the loading of a theory
+ proper; an attached theory {\ML} file may be still loaded later on.
+ This is {\ML} functions is normally not invoked directly.
+
+ \item @{ML ThyInfo.register_theory}~{text thy} registers an existing
+ theory value with the theory loader database. There is no
+ management of associated sources; this is mainly for bootstrapping.
+
+ \item @{ML "ThyInfo.add_hook"}~@{text f} registers function @{text
+ f} as a hook for theory database actions. The function will be
+ invoked with the action and theory name being involved; thus derived
+ actions may be performed in associated system components, e.g.\
+ maintaining the state of an editor for theory sources.
+
+ The kind and order of actions occurring in practice depends both on
+ user interactions and the internal process of resolving theory
+ imports. Hooks should not rely on a particular policy here! Any
+ exceptions raised by the hook are ignored by the theory database.
+
+ \end{description}
+*}
+
+
+(* FIXME section {* Sessions and document preparation *} *)
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarImplementation/Thy/locale.thy Mon Jan 02 20:16:52 2006 +0100
@@ -0,0 +1,16 @@
+
+(* $Id$ *)
+
+theory "locale" imports base begin
+
+chapter {* Structured specifications *}
+
+section {* Specification elements *}
+
+text FIXME
+
+section {* Locales *}
+
+text FIXME
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarImplementation/Thy/logic.thy Mon Jan 02 20:16:52 2006 +0100
@@ -0,0 +1,139 @@
+
+(* $Id$ *)
+
+theory logic imports base begin
+
+chapter {* Pure logic *}
+
+section {* Syntax *}
+
+subsection {* Simply-typed lambda calculus *}
+
+text {*
+
+FIXME
+
+\glossary{Type}{FIXME}
+\glossary{Term}{FIXME}
+
+*}
+
+subsection {* The order-sorted algebra of types *}
+
+text {*
+
+FIXME
+
+\glossary{Type constructor}{FIXME}
+
+\glossary{Type class}{FIXME}
+
+\glossary{Type arity}{FIXME}
+
+\glossary{Sort}{FIXME}
+
+*}
+
+
+subsection {* Type-inference and schematic polymorphism *}
+
+text {*
+
+FIXME
+
+\glossary{Schematic polymorphism}{FIXME}
+
+\glossary{Type variable}{FIXME}
+
+*}
+
+
+section {* Theory *}
+
+text {*
+
+FIXME
+
+\glossary{Constant}{Essentially a \seeglossary{fixed variable} of the
+theory context, but slightly more flexible since it may be used at
+different type-instances, due to \seeglossary{schematic
+polymorphism.}}
+
+*}
+
+
+section {* Deduction *}
+
+text {*
+
+ FIXME
+
+\glossary{Proposition}{A \seeglossary{term} of \seeglossary{type}
+@{text "prop"}. Internally, there is nothing special about
+propositions apart from their type, but the concrete syntax enforces a
+clear distinction. Propositions are structured via implication @{text
+"A \<Longrightarrow> B"} or universal quantification @{text "\<And>x. B x"} --- anything
+else is considered atomic. The canonical form for propositions is
+that of a \seeglossary{Hereditary Harrop Formula}.}
+
+\glossary{Theorem}{A proven proposition within a certain theory and
+proof context, formally @{text "\<Gamma> \<turnstile>\<^sub>\<Theta> \<phi>"}; both contexts are
+rarely spelled out explicitly. Theorems are usually normalized
+according to the \seeglossary{HHF} format.}
+
+\glossary{Fact}{Sometimes used interchangably for
+\seeglossary{theorem}. Strictly speaking, a list of theorems,
+essentially an extra-logical conjunction. Facts emerge either as
+local assumptions, or as results of local goal statements --- both may
+be simultaneous, hence the list representation.}
+
+\glossary{Schematic variable}{FIXME}
+
+\glossary{Fixed variable}{A variable that is bound within a certain
+proof context; an arbitrary-but-fixed entity within a portion of proof
+text.}
+
+\glossary{Free variable}{Synonymous for \seeglossary{fixed variable}.}
+
+\glossary{Bound variable}{FIXME}
+
+\glossary{Variable}{See \seeglossary{schematic variable},
+\seeglossary{fixed variable}, \seeglossary{bound variable}, or
+\seeglossary{type variable}. The distinguishing feature of different
+variables is their binding scope.}
+
+*}
+
+subsection {* Primitive inferences *}
+
+text FIXME
+
+subsection {* Higher-order resolution *}
+
+text {*
+
+FIXME
+
+\glossary{Hereditary Harrop Formula}{The set of propositions in HHF
+format is defined inductively as @{text "H = (\<And>x\<^sup>*. H\<^sup>* \<Longrightarrow>
+A)"}, for variables @{text "x"} and atomic propositions @{text "A"}.
+Any proposition may be put into HHF form by normalizing with the rule
+@{text "(A \<Longrightarrow> (\<And>x. B x)) \<equiv> (\<And>x. A \<Longrightarrow> B x)"}. In Isabelle, the outermost
+quantifier prefix is represented via \seeglossary{schematic
+variables}, such that the top-level structure is merely that of a
+\seeglossary{Horn Clause}}.
+
+\glossary{HHF}{See \seeglossary{Hereditary Harrop Formula}.}
+
+*}
+
+subsection {* Equational reasoning *}
+
+text FIXME
+
+
+section {* Proof terms *}
+
+text FIXME
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarImplementation/Thy/prelim.thy Mon Jan 02 20:16:52 2006 +0100
@@ -0,0 +1,328 @@
+
+(* $Id$ *)
+
+theory prelim imports base begin
+
+chapter {* Preliminaries *}
+
+section {* Named entities *}
+
+text {* Named entities of different kinds (logical constant, type,
+type class, theorem, method etc.) live in separate name spaces. It is
+usually clear from the occurrence of a name which kind of entity it
+refers to. For example, proof method @{text "foo"} vs.\ theorem
+@{text "foo"} vs.\ logical constant @{text "foo"} are easily
+distinguished by means of the syntactic context. A notable exception
+are logical identifiers within a term (\secref{sec:terms}): constants,
+fixed variables, and bound variables all share the same identifier
+syntax, but are distinguished by their scope.
+
+Each name space is organized as a collection of \emph{qualified
+names}, which consist of a sequence of basic name components separated
+by dots: @{text "Bar.bar.foo"}, @{text "Bar.foo"}, and @{text "foo"}
+are examples for valid qualified names. Name components are
+subdivided into \emph{symbols}, which constitute the smallest textual
+unit in Isabelle --- raw characters are normally not encountered
+directly. *}
+
+
+subsection {* Strings of symbols *}
+
+text {* Isabelle strings consist of a sequence of
+symbols\glossary{Symbol}{The smalles unit of text in Isabelle,
+subsumes plain ASCII characters as well as an infinite collection of
+named symbols (for greek, math etc.).}, which are either packed as an
+actual @{text "string"}, or represented as a list. Each symbol is in
+itself a small string of the following form:
+
+\begin{enumerate}
+
+\item either a singleton ASCII character ``@{text "c"}'' (with
+character code 0--127), for example ``\verb,a,'',
+
+\item or a regular symbol ``\verb,\,\verb,<,@{text "ident"}\verb,>,'',
+for example ``\verb,\,\verb,<alpha>,'',
+
+\item or a control symbol ``\verb,\,\verb,<^,@{text
+"ident"}\verb,>,'', for example ``\verb,\,\verb,<^bold>,'',
+
+\item or a raw control symbol ``\verb,\,\verb,<^raw:,@{text
+"\<dots>"}\verb,>,'' where ``@{text "\<dots>"}'' refers to any printable ASCII
+character (excluding ``\verb,>,'') or non-ASCII character, for example
+``\verb,\,\verb,<^raw:$\sum_{i = 1}^n$>,'',
+
+\item or a numbered raw control symbol ``\verb,\,\verb,<^raw,@{text
+"nnn"}\verb,>, where @{text "nnn"} are digits, for example
+``\verb,\,\verb,<^raw42>,''.
+
+\end{enumerate}
+
+The @{text "ident"} syntax for symbol names is @{text "letter (letter
+| digit)\<^sup>*"}, where @{text "letter = A..Za..Z"} and @{text
+"digit = 0..9"}. There are infinitely many regular symbols and
+control symbols available, but a certain collection of standard
+symbols is treated specifically. For example,
+``\verb,\,\verb,<alpha>,'' is classified as a (non-ASCII) letter,
+which means it may occur within regular Isabelle identifier syntax.
+
+Output of symbols depends on the print mode (\secref{sec:print-mode}).
+For example, the standard {\LaTeX} setup of the Isabelle document
+preparation system would present ``\verb,\,\verb,<alpha>,'' as @{text
+"\<alpha>"}, and ``\verb,\,\verb,<^bold>,\verb,\,\verb,<alpha>,'' as @{text
+"\<^bold>\<alpha>"}.
+
+\medskip It is important to note that the character set underlying
+Isabelle symbols is plain 7-bit ASCII. Since 8-bit characters are
+passed through transparently, Isabelle may easily process actual
+Unicode/UCS data (using the well-known UTF-8 encoding, for example).
+Unicode provides its own collection of mathematical symbols, but there
+is presently no link to Isabelle's named ones; both kinds of symbols
+coexist independently. *}
+
+text %mlref {*
+ \begin{mldecls}
+ @{index_ML_type "Symbol.symbol"} \\
+ @{index_ML Symbol.explode: "string -> Symbol.symbol list"} \\
+ @{index_ML Symbol.is_letter: "Symbol.symbol -> bool"} \\
+ @{index_ML Symbol.is_digit: "Symbol.symbol -> bool"} \\
+ @{index_ML Symbol.is_quasi: "Symbol.symbol -> bool"} \\
+ @{index_ML Symbol.is_blank: "Symbol.symbol -> bool"} \\
+ @{index_ML_type "Symbol.sym"} \\
+ @{index_ML Symbol.decode: "Symbol.symbol -> Symbol.sym"} \\
+ \end{mldecls}
+
+ \begin{description}
+
+ \item @{ML_type "Symbol.symbol"} represents Isabelle symbols; this type
+ is merely an alias for @{ML_type "string"}, but emphasizes the
+ specific format encountered here.
+
+ \item @{ML "Symbol.explode"}~@{text "s"} produces an actual symbol
+ list from the packed form usually encountered as user input. This
+ function replaces @{ML "String.explode"} for virtually all purposes
+ of manipulating text in Isabelle! Plain @{text "implode"} may be
+ used for the reverse operation.
+
+ \item @{ML "Symbol.is_letter"}, @{ML "Symbol.is_digit"}, @{ML
+ "Symbol.is_quasi"}, @{ML "Symbol.is_blank"} classify certain symbols
+ (both ASCII and several named ones) according to fixed syntactic
+ convections of Isabelle, e.g.\ see \cite{isabelle-isar-ref}.
+
+ \item @{ML_type "Symbol.sym"} is a concrete datatype that represents
+ the different kinds of symbols explicitly as @{ML "Symbol.Char"},
+ @{ML "Symbol.Sym"}, @{ML "Symbol.Ctrl"}, or @{ML "Symbol.Raw"}.
+
+ \item @{ML "Symbol.decode"} converts the string representation of a
+ symbol into the explicit datatype version.
+
+ \end{description}
+*}
+
+
+subsection {* Qualified names and name spaces *}
+
+text %FIXME {* Qualified names are constructed according to implicit naming
+principles of the present context.
+
+
+The last component is called \emph{base name}; the remaining prefix of
+qualification may be empty.
+
+Some practical conventions help to organize named entities more
+systematically:
+
+\begin{itemize}
+
+\item Names are qualified first by the theory name, second by an
+optional ``structure''. For example, a constant @{text "c"} declared
+as part of a certain structure @{text "b"} (say a type definition) in
+theory @{text "A"} will be named @{text "A.b.c"} internally.
+
+\item
+
+\item
+
+\item
+
+\item
+
+\end{itemize}
+
+Names of different kinds of entities are basically independent, but
+some practical naming conventions relate them to each other. For
+example, a constant @{text "foo"} may be accompanied with theorems
+@{text "foo.intro"}, @{text "foo.elim"}, @{text "foo.simps"} etc. The
+same may happen for a type @{text "foo"}, which is then apt to cause
+clashes in the theorem name space! To avoid this, we occasionally
+follow an additional convention of suffixes that determine the
+original kind of entity that a name has been derived. For example,
+constant @{text "foo"} is associated with theorem @{text "foo.intro"},
+type @{text "foo"} with theorem @{text "foo_type.intro"}, and type
+class @{text "foo"} with @{text "foo_class.intro"}.
+
+*}
+
+
+section {* Structured output *}
+
+subsection {* Pretty printing *}
+
+text FIXME
+
+subsection {* Output channels *}
+
+text FIXME
+
+subsection {* Print modes *}
+
+text FIXME
+
+
+section {* Context \label{sec:context} *}
+
+text %FIXME {* What is a context anyway? A highly advanced
+technological and cultural achievement, which took humanity several
+thousands of years to be develop, is writing with pen-and-paper. Here
+the paper is the context, or medium. It accommodates a certain range
+of different kinds of pens, but also has some inherent limitations.
+For example, carved inscriptions are better done on solid material
+like wood or stone.
+
+Isabelle/Isar distinguishes two key notions of context: \emph{theory
+ context}\indexbold{theory context} and \emph{proof context}.\indexbold{proof
+ context} To motivate this fundamental division consider the very idea of
+logical reasoning which is about judgments $\Gamma \Drv{\Theta} \phi$, where
+$\Theta$ is the background theory with declarations of operators and axioms
+stating their properties, and $\Gamma$ a collection of hypotheses emerging
+temporarily during proof. For example, the rule of implication-introduction
+\[
+\infer{\Gamma \Drv{\Theta} A \Imp B}{\Gamma, A \Drv{\Theta} B}
+\]
+can be read as ``to show $A \Imp B$ we may assume $A$ as hypothesis and need
+to show $B$''. It is characteristic that $\Theta$ is unchanged and $\Gamma$
+is only modified according to some general patterns of ``assuming'' and
+``discharging'' hypotheses. This admits the following abbreviated notation,
+where the fixed $\Theta$ and locally changed $\Gamma$ are left implicit:
+\[
+\infer{A \Imp B}{\infer*{B}{[A]}}
+\]
+
+In some logical traditions (e.g.\ Type Theory) there is a tendency to
+unify all kinds of declarations within a single notion of context.
+This is theoretically very nice, but also more demanding, because
+everything is internalized into the logical calculus itself.
+Isabelle/Pure is a very simple logic, but achieves many practically
+useful concepts by differentiating various basic elements.
+
+Take polymorphism, for example. Instead of embarking on the
+adventurous enterprise of full higher-order logic with full
+type-quantification and polymorphic entities, Isabelle/Pure merely
+takes a stripped-down version of Church's Simple Type Theory
+\cite{church40}. Then after the tradition of Gordon's HOL
+\cite{mgordon-hol} it is fairly easy to introduce syntactic notions of
+type variables and type-constructors, and require every theory
+$\Theta$ being closed by type instantiation. Whenever we wish to
+reason with a polymorphic constant or axiom scheme at a particular
+type, we may assume that it has been referenced initially at that very
+instance (due to the Deduction Theorem). Thus we achieve the
+following \emph{admissible
+ rule}\glossary{Admissible rule}{FIXME} of schematic type-instantiation:
+
+\[
+\infer{\phi(\tau)}{\infer*{\phi(\alpha)}{[\alpha]}}
+\]
+
+Using this approach, the structured Isar proof language offers
+schematic polymorphism within nested sub-proofs -- similar to that of
+polymorphic let-bindings according to Hindley-Milner.\
+\cite{milner78}. All of this is achieved without disintegrating the
+rather simplistic logical core. On the other hand, the succinct rule
+presented above already involves rather delicate interaction of the
+theory and proof context (with side-conditions not mentioned here),
+and unwinding an admissible rule involves induction over derivations.
+All of this diversity needs to be accomodated by the system
+architecture and actual implementation.
+
+\medskip Despite these important observations, Isabelle/Isar is not just a
+logical calculus, there are further extra-logical aspects to be considered.
+Practical experience over the years suggests two context data structures which
+are used in rather dissimilar manners, even though there is a considerable
+overlap of underlying ideas.
+
+From the system's perspective the mode of use of theory vs.\ proof context is
+the key distinction. The actual content is merely a generic slot for
+\emph{theory data} and \emph{proof data}, respectively. There are generic
+interfaces to declare data entries at any time. Even the core logic of
+Isabelle/Pure registers its very own notion of theory context data (types,
+constants, axioms etc.) like any other Isabelle tool out there. Likewise, the
+essentials of Isar proof contexts are one proof data slot among many others,
+notably those of derived Isar concepts (e.g.\ calculational reasoning rules).
+
+In that respect, a theory is more like a stone tablet to carve long-lasting
+inscriptions -- but take care not to break it! While a proof context is like
+a block of paper to scribble and dispose quickly. More recently Isabelle has
+started to cultivate the paper-based craftsmanship a bit further, by
+maintaining small collections of paper booklets, better known as locales.
+
+Thus we achive ``thick'' augmented versions of {\boldmath$\Theta$} and
+{\boldmath$\Gamma$} to support realistic structured reasoning within a
+practically usable system.
+*}
+
+
+subsection {* Theory context \label{sec:context-theory} *}
+
+text %FIXME {* A theory context consists of management information plus the
+actual data, which may be declared by other software modules later on.
+The management part is surprisingly complex, we illustrate it by the
+following typical situation of incremental theory development.
+
+\begin{tabular}{rcccl}
+ & & $Pure$ \\
+ & & $\downarrow$ \\
+ & & $FOL$ \\
+ & $\swarrow$ & & $\searrow$ & \\
+ $Nat$ & & & & $List$ \\
+ & $\searrow$ & & $\swarrow$ \\
+ & & $Length$ \\
+ & & \multicolumn{3}{l}{~~$\isarkeyword{imports}$} \\
+ & & \multicolumn{3}{l}{~~$\isarkeyword{begin}$} \\
+ & & $\vdots$~~ \\
+ & & $\bullet$~~ \\
+ & & $\vdots$~~ \\
+ & & $\bullet$~~ \\
+ & & $\vdots$~~ \\
+ & & \multicolumn{3}{l}{~~$\isarkeyword{end}$} \\
+\end{tabular}
+
+\begin{itemize}
+\item \emph{name}, \emph{parents} and \emph{ancestors}
+\item \emph{identity}
+\item \emph{intermediate versions}
+\end{itemize}
+
+\begin{description}
+\item [draft]
+\item [intermediate]
+\item [finished]
+\end{description}
+
+\emph{theory reference}
+*}
+
+
+subsection {* Proof context \label{sec:context-proof} *}
+
+text {*
+ FIXME
+
+\glossary{Proof context}{The static context of a structured proof,
+acts like a local ``theory'' of the current portion of Isar proof
+text, generalizes the idea of local hypotheses @{text "\<Gamma>"} in
+judgments @{text "\<Gamma> \<turnstile> \<phi>"} of natural deduction calculi. There is a
+generic notion of introducing and discharging hypotheses. Arbritrary
+auxiliary context data may be adjoined.}
+
+*}
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarImplementation/Thy/proof.thy Mon Jan 02 20:16:52 2006 +0100
@@ -0,0 +1,39 @@
+
+(* $Id$ *)
+
+theory "proof" imports base begin
+
+chapter {* Structured reasoning *}
+
+section {* Proof context *}
+
+text FIXME
+
+section {* Proof state *}
+
+text {*
+ FIXME
+
+\glossary{Proof state}{The whole configuration of a structured proof,
+consisting of a \seeglossary{proof context} and an optional
+\seeglossary{structured goal}. Internally, an Isar proof state is
+organized as a stack to accomodate block structure of proof texts.
+For historical reasons, a low-level \seeglossary{tactical goal} is
+occasionally called ``proof state'' as well.}
+
+\glossary{Structured goal}{FIXME}
+
+\glossary{Goal}{See \seeglossary{tactical goal} or \seeglossary{structured goal}. \norefpage}
+
+
+*}
+
+section {* Methods *}
+
+text FIXME
+
+section {* Attributes *}
+
+text FIXME
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarImplementation/Thy/setup.ML Mon Jan 02 20:16:52 2006 +0100
@@ -0,0 +1,38 @@
+
+local structure O = IsarOutput
+
+val str_of_source = space_implode " " o map Args.string_of o #2 o #1 o Args.dest_src;
+
+fun ml_val txt = "fn _ => (" ^ txt ^ ");";
+fun ml_type txt = "val _ = NONE : (" ^ txt ^ ") option;";
+fun ml_structure txt = "functor DUMMY_FUNCTOR() = struct structure DUMMY = " ^ txt ^ " end;"
+fun ml_functor txt = "val _ = ();"; (*no check!*)
+
+val verbatim = space_implode "\\verb,|," o map (enclose "\\verb|" "|") o space_explode "|";
+
+fun index_ml kind ml src ctxt (txt1, txt2) =
+ let
+ val txt = if txt2 = "" then txt1 else txt1 ^ ": " ^ txt2;
+ val txt' = if kind = "" then txt else kind ^ " " ^ txt;
+ val _ = Context.use_mltext (ml txt) false (SOME (ProofContext.theory_of ctxt));
+ in
+ "\\indexml" ^ kind ^ enclose "{" "}"
+ (translate_string (fn "_" => "-" | ">" => "$>$" | c => c) txt1) ^
+ ((if ! O.source then str_of_source src else txt')
+ |> (if ! O.quotes then quote else I)
+ |> (if ! O.display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"
+ else split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n"))
+ end;
+
+fun output_verbatim _ _ = split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n";
+
+fun arguments x = O.args (Scan.lift (Args.name -- Scan.optional (Args.colon |-- Args.name) "")) x;
+
+val _ = O.add_commands
+ [("index_ML", arguments (index_ml "" ml_val)),
+ ("index_ML_type", arguments (index_ml "type" ml_type)),
+ ("index_ML_structure", arguments (index_ml "structure" ml_structure)),
+ ("index_ML_functor", arguments (index_ml "functor" ml_functor)),
+ ("verbatim", O.args (Scan.lift Args.name) output_verbatim)];
+
+in val _ = () end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarImplementation/Thy/tactic.thy Mon Jan 02 20:16:52 2006 +0100
@@ -0,0 +1,188 @@
+
+(* $Id$ *)
+
+theory tactic imports base begin
+
+chapter {* Tactical theorem proving *}
+
+text {* The basic idea of tactical theorem proving is to refine the
+initial claim in a backwards fashion, until a solved form is reached.
+An intermediate goal consists of several subgoals that need to be
+solved in order to achieve the main statement; zero subgoals means
+that the proof may be finished. Goal refinement operations are called
+tactics; combinators for composing tactics are called tacticals. *}
+
+
+section {* Goals \label{sec:tactical-goals} *}
+
+text {* Isabelle/Pure represents a goal\glossary{Tactical goal}{A
+theorem of \seeglossary{Horn Clause} form stating that a number of
+subgoals imply the main conclusion, which is marked as a protected
+proposition.} as a theorem stating that the subgoals imply the main
+goal: @{text "A\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^sub>n \<Longrightarrow> C"}. The outermost goal
+structure is that of a Horn Clause\glossary{Horn Clause}{An iterated
+implication @{text "A\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^sub>n \<Longrightarrow> C"}, without any
+outermost quantifiers. Strictly speaking, propositions @{text
+"A\<^sub>i"} need to be atomic in Horn Clauses, but Isabelle admits
+arbitrary substructure here (nested @{text "\<Longrightarrow>"} and @{text "\<And>"}
+connectives).}: an iterated implication without any
+quantifiers\footnote{Recall that outermost @{text "\<And>x. \<phi>[x]"} is
+always represented via schematic variables in the body: @{text
+"\<phi>[?x]"}. These may get instantiated during the course of
+reasoning.}. For @{text "n = 0"} a goal is solved.
+
+The structure of each subgoal @{text "A\<^sub>i"} is that of a general
+Heriditary Harrop Formula @{text "\<And>x\<^sub>1 \<dots> \<And>x\<^sub>k. H\<^sub>1 \<Longrightarrow>
+\<dots> \<Longrightarrow> H\<^sub>m \<Longrightarrow> B"} according to the normal form where any local
+@{text \<And>} is pulled before @{text \<Longrightarrow>}. Here @{text "x\<^sub>1, \<dots>,
+x\<^sub>k"} are goal parameters, i.e.\ arbitrary-but-fixed entities of
+certain types, and @{text "H\<^sub>1, \<dots>, H\<^sub>m"} are goal
+hypotheses, i.e.\ facts that may be assumed locally. Together, this
+forms the goal context of the conclusion @{text B} to be established.
+The goal hypotheses may be again arbitrary Harrop Formulas, although
+the level of nesting rarely exceeds 1--2 in practice.
+
+The main conclusion @{text C} is internally marked as a protected
+proposition\glossary{Protected proposition}{An arbitrarily structured
+proposition @{text "C"} which is forced to appear as atomic by
+wrapping it into a propositional identity operator; notation @{text
+"#C"}. Protecting a proposition prevents basic inferences from
+entering into that structure for the time being.}, which is
+occasionally represented explicitly by the notation @{text "#C"}.
+This ensures that the decomposition into subgoals and main conclusion
+is well-defined for arbitrarily structured claims.
+
+\medskip Basic goal management is performed via the following
+Isabelle/Pure rules:
+
+ \[
+ \infer[@{text "(init)"}]{@{text "C \<Longrightarrow> #C"}}{} \qquad
+ \infer[@{text "(finish)"}]{@{text "#C"}}{@{text "C"}}
+ \]
+
+ \medskip The following low-level variants admit general reasoning
+ with protected propositions:
+
+ \[
+ \infer[@{text "(protect)"}]{@{text "#C"}}{@{text "C"}} \qquad
+ \infer[@{text "(conclude)"}]{@{text "A\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^sub>n \<Longrightarrow> C"}}{@{text "A\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^sub>n \<Longrightarrow> #C"}}
+ \]
+*}
+
+text %mlref {*
+ \begin{mldecls}
+ @{index_ML Goal.init: "cterm -> thm"} \\
+ @{index_ML Goal.finish: "thm -> thm"} \\
+ @{index_ML Goal.protect: "thm -> thm"} \\
+ @{index_ML Goal.conclude: "thm -> thm"} \\
+ \end{mldecls}
+
+ \begin{description}
+
+ \item @{ML "Goal.init"}~@{text "\<phi>"} initializes a tactical goal with
+ the type-checked proposition @{text \<phi>}.
+
+ \item @{ML "Goal.finish"}~@{text "th"} checks whether theorem @{text
+ "th"} is a solved goal configuration (zero subgoals), and concludes
+ the result by removing the goal protection.
+
+ \item @{ML "Goal.protect"}~@{text "th"} protects the whole statement
+ of theorem @{text "th"}.
+
+ \item @{ML "Goal.conclude"}~@{text "th"} removes the goal protection
+ for any number of pending subgoals.
+
+ \end{description}
+*}
+
+
+section {* Tactics *}
+
+text {*
+
+FIXME
+
+\glossary{Tactic}{Any function that maps a \seeglossary{tactical goal}
+to a lazy sequence of possible sucessors. This scheme subsumes
+failure (empty result sequence), as well as lazy enumeration of proof
+search results. Error conditions are usually mapped to an empty
+result, which gives further tactics a chance to try in turn.
+Commonly, tactics either take an argument to address a particular
+subgoal, or operate on a certain range of subgoals in a uniform
+fashion. In any case, the main conclusion is normally left untouched,
+apart from instantiating \seeglossary{schematic variables}.}
+
+
+*}
+
+section {* Tacticals *}
+
+text {*
+
+FIXME
+
+\glossary{Tactical}{A functional combinator for building up complex
+tactics from simpler ones. Typical tactical perform sequential
+composition, disjunction (choice), iteration, or goal addressing.
+Various search strategies may be expressed via tacticals.}
+
+*}
+
+section {* Programmed proofs *}
+
+text {*
+ In order to perform a complete tactical proof under program control,
+ one needs to set up an initial goal configuration, apply a tactic,
+ and finish the result, cf.\ the rules given in
+ \secref{sec:tactical-goals}. Further checks are required to ensure
+ that the result is actually an instance of the original claim --
+ ill-behaved tactics could have destroyed that information.
+
+ Several simultaneous claims may be handled within a single goal
+ statement by using meta-level conjunction internally.\footnote{This
+ is merely syntax for certain derived statements within
+ Isabelle/Pure, there is no need to introduce a separate conjunction
+ operator.} The whole configuration may be considered within a
+ context of arbitrary-but-fixed parameters and hypotheses, which will
+ be available as local facts during the proof and discharged into
+ implications in the result.
+
+ All of these administrative tasks are packaged into a separate
+ operation, such that the user merely needs to provide the statement
+ and tactic to be applied.
+*}
+
+text %mlref {*
+ \begin{mldecls}
+ @{index_ML Goal.prove: "theory -> string list -> term list -> term ->
+ (thm list -> tactic) -> thm"} \\
+ @{index_ML Goal.prove_multi: "theory -> string list -> term list -> term list ->
+ (thm list -> tactic) -> thm list"} \\
+ \end{mldecls}
+
+ \begin{description}
+
+ \item @{ML Goal.prove}~@{text "thy xs As C tac"} states goal @{text
+ "C"} in the context of arbitrary-but-fixed parameters @{text "xs"}
+ and hypotheses @{text "As"} and applies tactic @{text "tac"} to
+ solve it. The latter may depend on the local assumptions being
+ presented as facts. The result is essentially @{text "\<And>xs. As \<Longrightarrow>
+ C"}, but is normalized by pulling @{text "\<And>"} before @{text "\<Longrightarrow>"}
+ (the conclusion @{text "C"} itself may be a rule statement), turning
+ the quantifier prefix into schematic variables, and generalizing
+ implicit type-variables.
+
+ Any additional fixed variables or hypotheses not being mentioned in
+ the initial statement are left unchanged --- programmed proofs may
+ well occur in a larger context.
+
+ \item @{ML Goal.prove_multi} is simular to @{ML Goal.prove}, but
+ states several conclusions simultaneously. @{ML
+ Tactic.conjunction_tac} may be used to split these into individual
+ subgoals before commencing the actual proof.
+
+ \end{description}
+*}
+
+end
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarImplementation/Thy/unused.thy Mon Jan 02 20:16:52 2006 +0100
@@ -0,0 +1,16 @@
+
+text {*
+ The Isar toplevel works differently for interactive developments
+ vs.\ batch processing of theory sources. For example, diagnostic
+ commands produce a warning batch mode, because they are considered
+ alien to the final theory document being produced eventually.
+ Moreover, full @{text undo} with intermediate checkpoints to protect
+ against destroying theories accidentally are limited to interactive
+ mode. In batch mode there is only a single strictly linear stream
+ of potentially desctructive theory transformations.
+*}
+
+ \item @{ML Toplevel.empty} is an empty transition; the Isar command
+ dispatcher internally applies @{ML Toplevel.name} (for the command)
+ name and @{ML Toplevel.position} for the source position.
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarImplementation/checkglossary Mon Jan 02 20:16:52 2006 +0100
@@ -0,0 +1,28 @@
+#!/usr/bin/env perl
+# $Id$
+
+use strict;
+
+my %defs = ();
+my %refs = ();
+
+while (<ARGV>) {
+ if (m,\\glossaryentry\{\w*\\bf *((\w|\s)+)@,) {
+ $defs{lc $1} = 1;
+ }
+ while (m,\\seeglossary *\{((\w|\s)+)\},g) {
+ $refs{lc $1} = 1;
+ }
+}
+
+print "Glossary definitions:\n";
+foreach (sort(keys(%defs))) {
+ print " \"$_\"\n";
+}
+
+foreach (keys(%refs)) {
+ s,s$,,;
+ if (!defined($defs{$_})) {
+ print "### Undefined glossary reference: \"$_\"\n";
+ }
+}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarImplementation/implementation.tex Mon Jan 02 20:16:52 2006 +0100
@@ -0,0 +1,75 @@
+
+%% $Id$
+
+\documentclass[12pt,a4paper,fleqn]{report}
+\usepackage{latexsym,graphicx}
+\usepackage[refpage]{nomencl}
+\usepackage{../iman,../extra,../isar,../proof}
+\usepackage{Thy/document/isabelle,Thy/document/isabellesym}
+\usepackage{style}
+\usepackage{../pdfsetup}
+
+
+\hyphenation{Isabelle}
+\hyphenation{Isar}
+
+\isadroptag{theory}
+\title{\includegraphics[scale=0.5]{isabelle_isar}
+ \\[4ex] The Isabelle/Isar Implementation}
+\author{\emph{Makarius M. M. Wenzel}}
+
+\makeglossary
+\makeindex
+
+
+\begin{document}
+
+\maketitle
+
+\begin{abstract}
+ We describe the key concepts underlying the Isabelle/Isar
+ implementation, including ML references for the most important
+ elements. The aim is to give some insight into the overall system
+ architecture, and provide clues on implementing user extensions.
+\end{abstract}
+
+\pagenumbering{roman} \tableofcontents \clearfirst
+
+\input{intro.tex}
+\input{Thy/document/prelim.tex}
+\input{Thy/document/logic.tex}
+\input{Thy/document/tactic.tex}
+\input{Thy/document/proof.tex}
+\input{Thy/document/locale.tex}
+\input{Thy/document/integration.tex}
+
+% Isabelle was not designed; it evolved.
+% Not everyone likes this idea. Specification experts rightly abhor trial-and-error programming.
+% They suggest that no one should write a program without First writing a complete
+% formal specification. But university departments are not software houses. Programs like
+% Isabelle are not products: when they have served their purpose, they are discarded.
+%
+% L.C. Paulson, Isabelle: The Next 700 Theorem Provers
+
+\appendix
+\input{Thy/document/ML.tex}
+
+\begingroup
+\tocentry{\bibname}
+\bibliographystyle{plain} \small\raggedright\frenchspacing
+\bibliography{../manual}
+\endgroup
+
+\tocentry{\glossaryname}
+\printglossary
+
+\tocentry{\indexname}
+\printindex
+
+\end{document}
+
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: t
+%%% End:
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarImplementation/intro.tex Mon Jan 02 20:16:52 2006 +0100
@@ -0,0 +1,13 @@
+
+%% $Id$
+
+\chapter{Introduction}
+
+FIXME
+
+\nocite{Wenzel-PhD}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "implementation"
+%%% End:
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarImplementation/makeglossary Mon Jan 02 20:16:52 2006 +0100
@@ -0,0 +1,6 @@
+#!/bin/sh
+# $Id$
+
+NAME="$1"
+makeindex -s nomencl -o "${NAME}.gls" "${NAME}.glo"
+./checkglossary "${NAME}.glo"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarImplementation/style.sty Mon Jan 02 20:16:52 2006 +0100
@@ -0,0 +1,59 @@
+
+%% $Id$
+
+%% toc
+\newcommand{\tocentry}[1]{\cleardoublepage\phantomsection\addcontentsline{toc}{chapter}{#1}}
+
+%% references
+\newcommand{\secref}[1]{\S\ref{#1}}
+\newcommand{\figref}[1]{figure~\ref{#1}}
+
+%% glossary
+\renewcommand{\glossary}[2]{\nomenclature{\bf #1}{#2}}
+\newcommand{\seeglossary}[1]{\emph{#1}}
+\def\glossaryname{Glossary}
+\renewcommand{\nomname}{\glossaryname}
+\renewcommand{\pagedeclaration}[1]{\nobreak\quad\dotfill~page~\bold{#1}}
+
+\newcommand{\drv}{\mathrel{\vdash}}
+\newcommand{\edrv}{\mathop{\drv}\nolimits}
+\newcommand{\Drv}[1]{\mathrel{\vdash_{#1}}}
+\newcommand{\Or}{\mathrel{\;|\;}}
+
+\renewcommand{\vec}[1]{\overline{#1}}
+\renewcommand{\phi}{\varphi}
+
+\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}
+
+\pagestyle{headings}
+\sloppy
+\binperiod
+\underscoreon
+
+\newenvironment{mldecls}{\par\noindent\begingroup\def\isanewline{\\}\begin{tabular}{l}}{\end{tabular}\medskip\endgroup}
+
+\isafoldtag{FIXME}
+\isakeeptag{mlref}
+\renewcommand{\isatagmlref}{\subsection*{\makebox[0pt][r]{\fbox{\ML}~~}Reference}\begingroup\def\isastyletext{\rm}\small}
+\renewcommand{\endisatagmlref}{\endgroup}
+
+\newcommand{\indexml}[1]{\index{\emph{#1} ({\ML})|bold}}
+\newcommand{\indexmltype}[1]{\index{\emph{#1} ({\ML} type)|bold}}
+\newcommand{\indexmlstructure}[1]{\index{\emph{#1} ({\ML} structure)|bold}}
+\newcommand{\indexmlfunctor}[1]{\index{\emph{#1} ({\ML} functor)|bold}}
+
+\newcommand{\isasymTHEORY}{\isakeyword{theory}}
+\newcommand{\isasymIMPORTS}{\isakeyword{imports}}
+\newcommand{\isasymUSES}{\isakeyword{uses}}
+\newcommand{\isasymBEGIN}{\isakeyword{begin}}
+\newcommand{\isasymEND}{\isakeyword{end}}
+\newcommand{\isasymCONSTS}{\isakeyword{consts}}
+\newcommand{\isasymDEFS}{\isakeyword{defs}}
+\newcommand{\isasymTHEOREM}{\isakeyword{theorem}}
+
+\isabellestyle{it}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "implementation"
+%%% End: