"The Isabelle/Isar Implementation" manual;
authorwenzelm
Mon Jan 02 20:16:52 2006 +0100 (2006-01-02)
changeset 185372681f9e34390
parent 18536 ab3f32f86847
child 18538 88fe84d4d151
"The Isabelle/Isar Implementation" manual;
doc-src/IsarImplementation/IsaMakefile
doc-src/IsarImplementation/Makefile
doc-src/IsarImplementation/Thy/ML.thy
doc-src/IsarImplementation/Thy/ROOT.ML
doc-src/IsarImplementation/Thy/base.thy
doc-src/IsarImplementation/Thy/document/ML.tex
doc-src/IsarImplementation/Thy/document/base.tex
doc-src/IsarImplementation/Thy/document/integration.tex
doc-src/IsarImplementation/Thy/document/locale.tex
doc-src/IsarImplementation/Thy/document/logic.tex
doc-src/IsarImplementation/Thy/document/prelim.tex
doc-src/IsarImplementation/Thy/document/proof.tex
doc-src/IsarImplementation/Thy/document/session.tex
doc-src/IsarImplementation/Thy/document/tactic.tex
doc-src/IsarImplementation/Thy/integration.thy
doc-src/IsarImplementation/Thy/locale.thy
doc-src/IsarImplementation/Thy/logic.thy
doc-src/IsarImplementation/Thy/prelim.thy
doc-src/IsarImplementation/Thy/proof.thy
doc-src/IsarImplementation/Thy/setup.ML
doc-src/IsarImplementation/Thy/tactic.thy
doc-src/IsarImplementation/Thy/unused.thy
doc-src/IsarImplementation/checkglossary
doc-src/IsarImplementation/implementation.tex
doc-src/IsarImplementation/intro.tex
doc-src/IsarImplementation/makeglossary
doc-src/IsarImplementation/style.sty
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/doc-src/IsarImplementation/IsaMakefile	Mon Jan 02 20:16:52 2006 +0100
     1.3 @@ -0,0 +1,33 @@
     1.4 +
     1.5 +## targets
     1.6 +
     1.7 +default: Thy
     1.8 +images: 
     1.9 +test: Thy
    1.10 +
    1.11 +all: images test
    1.12 +
    1.13 +
    1.14 +## global settings
    1.15 +
    1.16 +SRC = $(ISABELLE_HOME)/src
    1.17 +OUT = $(ISABELLE_OUTPUT)
    1.18 +LOG = $(OUT)/log
    1.19 +
    1.20 +USEDIR = $(ISATOOL) usedir -v true -i false -d false -C false -D document
    1.21 +
    1.22 +
    1.23 +## Thy
    1.24 +
    1.25 +Thy: $(LOG)/Pure-Thy.gz
    1.26 +
    1.27 +$(LOG)/Pure-Thy.gz: Thy/ROOT.ML Thy/base.thy Thy/integration.thy \
    1.28 +  Thy/locale.thy Thy/logic.thy Thy/prelim.thy Thy/proof.thy Thy/tactic.thy \
    1.29 +  Thy/ML.thy Thy/setup.ML
    1.30 +	@$(USEDIR) Pure Thy
    1.31 +
    1.32 +
    1.33 +## clean
    1.34 +
    1.35 +clean:
    1.36 +	@rm -f $(LOG)/Pure-Thy.gz
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/doc-src/IsarImplementation/Makefile	Mon Jan 02 20:16:52 2006 +0100
     2.3 @@ -0,0 +1,46 @@
     2.4 +#
     2.5 +# $Id$
     2.6 +#
     2.7 +
     2.8 +## targets
     2.9 +
    2.10 +default: dvi
    2.11 +
    2.12 +
    2.13 +## dependencies
    2.14 +
    2.15 +include ../Makefile.in
    2.16 +
    2.17 +MAKEGLOSSARY = ./makeglossary
    2.18 +
    2.19 +NAME = implementation
    2.20 +
    2.21 +FILES = implementation.tex intro.tex Thy/document/prelim.tex Thy/document/logic.tex \
    2.22 +  Thy/document/tactic.tex Thy/document/proof.tex Thy/document/locale.tex \
    2.23 +  Thy/document/integration.tex style.sty ../iman.sty ../extra.sty ../isar.sty \
    2.24 +  ../manual.bib ../proof.sty
    2.25 +
    2.26 +dvi: $(NAME).dvi
    2.27 +
    2.28 +$(NAME).dvi: $(FILES) isabelle_isar.eps
    2.29 +	$(LATEX) $(NAME)
    2.30 +	$(BIBTEX) $(NAME)
    2.31 +	$(LATEX) $(NAME)
    2.32 +	$(LATEX) $(NAME)
    2.33 +	$(MAKEGLOSSARY) $(NAME)
    2.34 +	$(SEDINDEX) $(NAME)
    2.35 +	$(LATEX) $(NAME)
    2.36 +	$(LATEX) $(NAME)
    2.37 +
    2.38 +pdf: $(NAME).pdf
    2.39 +
    2.40 +$(NAME).pdf: $(FILES) isabelle_isar.pdf
    2.41 +	$(PDFLATEX) $(NAME)
    2.42 +	$(BIBTEX) $(NAME)
    2.43 +	$(PDFLATEX) $(NAME)
    2.44 +	$(PDFLATEX) $(NAME)
    2.45 +	$(MAKEGLOSSARY) $(NAME)
    2.46 +	$(SEDINDEX) $(NAME)
    2.47 +	$(FIXBOOKMARKS) $(NAME).out
    2.48 +	$(PDFLATEX) $(NAME)
    2.49 +	$(PDFLATEX) $(NAME)
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/doc-src/IsarImplementation/Thy/ML.thy	Mon Jan 02 20:16:52 2006 +0100
     3.3 @@ -0,0 +1,2 @@
     3.4 +
     3.5 +theory "ML" imports Pure begin end
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/doc-src/IsarImplementation/Thy/ROOT.ML	Mon Jan 02 20:16:52 2006 +0100
     4.3 @@ -0,0 +1,10 @@
     4.4 +
     4.5 +(* $Id$ *)
     4.6 +
     4.7 +use_thy "prelim";
     4.8 +use_thy "logic";
     4.9 +use_thy "tactic";
    4.10 +use_thy "proof";
    4.11 +use_thy "locale";
    4.12 +use_thy "integration";
    4.13 +use_thy "ML";
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/doc-src/IsarImplementation/Thy/base.thy	Mon Jan 02 20:16:52 2006 +0100
     5.3 @@ -0,0 +1,9 @@
     5.4 +
     5.5 +(* $Id$ *)
     5.6 +
     5.7 +theory base
     5.8 +imports CPure
     5.9 +uses "setup.ML"
    5.10 +begin
    5.11 +
    5.12 +end
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/doc-src/IsarImplementation/Thy/document/ML.tex	Mon Jan 02 20:16:52 2006 +0100
     6.3 @@ -0,0 +1,25 @@
     6.4 +%
     6.5 +\begin{isabellebody}%
     6.6 +\def\isabellecontext{ML}%
     6.7 +%
     6.8 +\isadelimtheory
     6.9 +\isanewline
    6.10 +%
    6.11 +\endisadelimtheory
    6.12 +%
    6.13 +\isatagtheory
    6.14 +\isacommand{theory}\isamarkupfalse%
    6.15 +\ {\isachardoublequoteopen}ML{\isachardoublequoteclose}\ \isakeyword{imports}\ Pure\ \isakeyword{begin}\ \isacommand{end}\isamarkupfalse%
    6.16 +%
    6.17 +\endisatagtheory
    6.18 +{\isafoldtheory}%
    6.19 +%
    6.20 +\isadelimtheory
    6.21 +\isanewline
    6.22 +%
    6.23 +\endisadelimtheory
    6.24 +\end{isabellebody}%
    6.25 +%%% Local Variables:
    6.26 +%%% mode: latex
    6.27 +%%% TeX-master: "root"
    6.28 +%%% End:
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/doc-src/IsarImplementation/Thy/document/base.tex	Mon Jan 02 20:16:52 2006 +0100
     7.3 @@ -0,0 +1,32 @@
     7.4 +%
     7.5 +\begin{isabellebody}%
     7.6 +\def\isabellecontext{base}%
     7.7 +%
     7.8 +\isadelimtheory
     7.9 +\isanewline
    7.10 +\isanewline
    7.11 +\isanewline
    7.12 +%
    7.13 +\endisadelimtheory
    7.14 +%
    7.15 +\isatagtheory
    7.16 +\isacommand{theory}\isamarkupfalse%
    7.17 +\ base\isanewline
    7.18 +\isakeyword{imports}\ CPure\isanewline
    7.19 +\isakeyword{uses}\ {\isachardoublequoteopen}setup{\isachardot}ML{\isachardoublequoteclose}\isanewline
    7.20 +\isakeyword{begin}\isanewline
    7.21 +\isanewline
    7.22 +\isacommand{end}\isamarkupfalse%
    7.23 +%
    7.24 +\endisatagtheory
    7.25 +{\isafoldtheory}%
    7.26 +%
    7.27 +\isadelimtheory
    7.28 +\isanewline
    7.29 +%
    7.30 +\endisadelimtheory
    7.31 +\end{isabellebody}%
    7.32 +%%% Local Variables:
    7.33 +%%% mode: latex
    7.34 +%%% TeX-master: "root"
    7.35 +%%% End:
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/doc-src/IsarImplementation/Thy/document/integration.tex	Mon Jan 02 20:16:52 2006 +0100
     8.3 @@ -0,0 +1,536 @@
     8.4 +%
     8.5 +\begin{isabellebody}%
     8.6 +\def\isabellecontext{integration}%
     8.7 +%
     8.8 +\isadelimtheory
     8.9 +\isanewline
    8.10 +\isanewline
    8.11 +\isanewline
    8.12 +%
    8.13 +\endisadelimtheory
    8.14 +%
    8.15 +\isatagtheory
    8.16 +\isacommand{theory}\isamarkupfalse%
    8.17 +\ integration\ \isakeyword{imports}\ base\ \isakeyword{begin}%
    8.18 +\endisatagtheory
    8.19 +{\isafoldtheory}%
    8.20 +%
    8.21 +\isadelimtheory
    8.22 +%
    8.23 +\endisadelimtheory
    8.24 +%
    8.25 +\isamarkupchapter{System integration%
    8.26 +}
    8.27 +\isamarkuptrue%
    8.28 +%
    8.29 +\isamarkupsection{Isar toplevel%
    8.30 +}
    8.31 +\isamarkuptrue%
    8.32 +%
    8.33 +\begin{isamarkuptext}%
    8.34 +The Isar toplevel may be considered the centeral hub of the
    8.35 +  Isabelle/Isar system, where all key components and sub-systems are
    8.36 +  integrated into a single read-eval-print loop of Isar commands.
    8.37 +  Here we even incorporate the existing {\ML} toplevel of the compiler
    8.38 +  and run-time system (cf.\ \secref{sec:ML-toplevel}).
    8.39 +
    8.40 +  Isabelle/Isar departs from original ``LCF system architecture''
    8.41 +  where {\ML} was really The Meta Language for defining theories and
    8.42 +  conducting proofs.  Instead, {\ML} merely serves as the
    8.43 +  implementation language for the system (and user extensions), while
    8.44 +  our specific Isar toplevel supports particular notions of
    8.45 +  incremental theory and proof development more directly.  This
    8.46 +  includes the graph structure of theories and the block structure of
    8.47 +  proofs, support for unlimited undo, facilities for tracing,
    8.48 +  debugging, timing, profiling.
    8.49 +
    8.50 +  \medskip The toplevel maintains an implicit state, which is
    8.51 +  transformed by a sequence of transitions -- either interactively or
    8.52 +  in batch-mode.  In interactive mode, Isar state transitions are
    8.53 +  encapsulated as safe transactions, such that both failure and undo
    8.54 +  are handled conveniently without destroying the underlying draft
    8.55 +  theory (cf.~\secref{sec:context-theory}).  In batch mode,
    8.56 +  transitions operate in a strictly linear (destructive) fashion, such
    8.57 +  that error conditions abort the present attempt to construct a
    8.58 +  theory altogether.
    8.59 +
    8.60 +  The toplevel state is a disjoint sum of empty \isa{toplevel}, or
    8.61 +  \isa{theory}, or \isa{proof}.  On entering the main Isar loop we
    8.62 +  start with an empty toplevel.  A theory is commenced by giving a
    8.63 +  \isa{{\isasymTHEORY}} header; within a theory we may issue theory
    8.64 +  commands such as \isa{{\isasymCONSTS}} or \isa{{\isasymDEFS}}, or state a
    8.65 +  \isa{{\isasymTHEOREM}} to be proven.  Now we are within a proof state,
    8.66 +  with a rich collection of Isar proof commands for structured proof
    8.67 +  composition, or unstructured proof scripts.  When the proof is
    8.68 +  concluded we get back to the theory, which is then updated by
    8.69 +  storing the resulting fact.  Further theory declarations or theorem
    8.70 +  statements with proofs may follow, until we eventually conclude the
    8.71 +  theory development by issuing \isa{{\isasymEND}}.  The resulting theory
    8.72 +  is then stored within the theory database and we are back to the
    8.73 +  empty toplevel.
    8.74 +
    8.75 +  In addition to these proper state transformations, there are also
    8.76 +  some diagnostic commands for peeking at the toplevel state without
    8.77 +  modifying it (e.g.\ \isakeyword{thm}, \isakeyword{term},
    8.78 +  \isakeyword{print-cases}).%
    8.79 +\end{isamarkuptext}%
    8.80 +\isamarkuptrue%
    8.81 +%
    8.82 +\isadelimmlref
    8.83 +%
    8.84 +\endisadelimmlref
    8.85 +%
    8.86 +\isatagmlref
    8.87 +%
    8.88 +\begin{isamarkuptext}%
    8.89 +\begin{mldecls}
    8.90 +  \indexmltype{Toplevel.state}\verb|type Toplevel.state| \\
    8.91 +  \indexml{Toplevel.UNDEF}\verb|Toplevel.UNDEF: exn| \\
    8.92 +  \indexml{Toplevel.is-toplevel}\verb|Toplevel.is_toplevel: Toplevel.state -> bool| \\
    8.93 +  \indexml{Toplevel.theory-of}\verb|Toplevel.theory_of: Toplevel.state -> theory| \\
    8.94 +  \indexml{Toplevel.proof-of}\verb|Toplevel.proof_of: Toplevel.state -> Proof.state| \\
    8.95 +  \indexml{Toplevel.debug}\verb|Toplevel.debug: bool ref| \\
    8.96 +  \indexml{Toplevel.timing}\verb|Toplevel.timing: bool ref| \\
    8.97 +  \indexml{Toplevel.profiling}\verb|Toplevel.profiling: int ref| \\
    8.98 +  \end{mldecls}
    8.99 +
   8.100 +  \begin{description}
   8.101 +
   8.102 +  \item \verb|Toplevel.state| represents Isar toplevel states,
   8.103 +  which are normally only manipulated through the toplevel transition
   8.104 +  concept (\secref{sec:toplevel-transition}).  Also note that a
   8.105 +  toplevel state is subject to the same linerarity restrictions as a
   8.106 +  theory context (cf.~\secref{sec:context-theory}).
   8.107 +
   8.108 +  \item \verb|Toplevel.UNDEF| is raised for undefined toplevel
   8.109 +  operations: \verb|Toplevel.state| is a sum type, many operations
   8.110 +  work only partially for certain cases.
   8.111 +
   8.112 +  \item \verb|Toplevel.is_toplevel| checks for an empty toplevel state.
   8.113 +
   8.114 +  \item \verb|Toplevel.theory_of| gets the theory of a theory or proof
   8.115 +  (!), otherwise raises \verb|Toplevel.UNDEF|.
   8.116 +
   8.117 +  \item \verb|Toplevel.proof_of| gets the Isar proof state if
   8.118 +  available, otherwise raises \verb|Toplevel.UNDEF|.
   8.119 +
   8.120 +  \item \verb|set Toplevel.debug| makes the toplevel print further
   8.121 +  details about internal error conditions, exceptions being raised
   8.122 +  etc.
   8.123 +
   8.124 +  \item \verb|set Toplevel.timing| makes the toplevel print timing
   8.125 +  information for each Isar command being executed.
   8.126 +
   8.127 +  \item \verb|Toplevel.profiling| controls low-level profiling of the
   8.128 +  underlying {\ML} runtime system.\footnote{For Poly/ML, 1 means time
   8.129 +  and 2 space profiling.}
   8.130 +
   8.131 +  \end{description}%
   8.132 +\end{isamarkuptext}%
   8.133 +\isamarkuptrue%
   8.134 +%
   8.135 +\endisatagmlref
   8.136 +{\isafoldmlref}%
   8.137 +%
   8.138 +\isadelimmlref
   8.139 +%
   8.140 +\endisadelimmlref
   8.141 +%
   8.142 +\isamarkupsubsection{Toplevel transitions%
   8.143 +}
   8.144 +\isamarkuptrue%
   8.145 +%
   8.146 +\begin{isamarkuptext}%
   8.147 +An Isar toplevel transition consists of a partial
   8.148 +  function on the toplevel state, with additional information for
   8.149 +  diagnostics and error reporting: there are fields for command name,
   8.150 +  source position, optional source text, as well as flags for
   8.151 +  interactive-only commands (which issue a warning in batch-mode),
   8.152 +  printing of result state, etc.
   8.153 +
   8.154 +  The operational part is represented as a sequential union of a list
   8.155 +  of partial functions, which are tried in turn until the first one
   8.156 +  succeeds (i.e.\ does not raise \verb|Toplevel.UNDEF|).  For example,
   8.157 +  a single Isar command like \isacommand{qed} consists of the union of
   8.158 +  some function \verb|Proof.state -> Proof.state| for proofs
   8.159 +  within proofs, plus \verb|Proof.state -> theory| for proofs at
   8.160 +  the outer theory level.
   8.161 +
   8.162 +  Toplevel transitions are composed via transition transformers.
   8.163 +  Internally, Isar commands are put together from an empty transition
   8.164 +  extended by name and source position (and optional source text).  It
   8.165 +  is then left to the individual command parser to turn the given
   8.166 +  syntax body into a suitable transition transformer that adjoin
   8.167 +  actual operations on a theory or proof state etc.%
   8.168 +\end{isamarkuptext}%
   8.169 +\isamarkuptrue%
   8.170 +%
   8.171 +\isadelimmlref
   8.172 +%
   8.173 +\endisadelimmlref
   8.174 +%
   8.175 +\isatagmlref
   8.176 +%
   8.177 +\begin{isamarkuptext}%
   8.178 +\begin{mldecls}
   8.179 +  \indexml{Toplevel.print}\verb|Toplevel.print: Toplevel.transition -> Toplevel.transition| \\
   8.180 +  \indexml{Toplevel.no-timing}\verb|Toplevel.no_timing: Toplevel.transition -> Toplevel.transition| \\
   8.181 +  \indexml{Toplevel.keep}\verb|Toplevel.keep: (Toplevel.state -> unit) ->|\isasep\isanewline%
   8.182 +\verb|  Toplevel.transition -> Toplevel.transition| \\
   8.183 +  \indexml{Toplevel.theory}\verb|Toplevel.theory: (theory -> theory) ->|\isasep\isanewline%
   8.184 +\verb|  Toplevel.transition -> Toplevel.transition| \\
   8.185 +  \indexml{Toplevel.theory-to-proof}\verb|Toplevel.theory_to_proof: (theory -> Proof.state) ->|\isasep\isanewline%
   8.186 +\verb|  Toplevel.transition -> Toplevel.transition| \\
   8.187 +  \indexml{Toplevel.proof}\verb|Toplevel.proof: (Proof.state -> Proof.state) ->|\isasep\isanewline%
   8.188 +\verb|  Toplevel.transition -> Toplevel.transition| \\
   8.189 +  \indexml{Toplevel.proofs}\verb|Toplevel.proofs: (Proof.state -> Proof.state Seq.seq) ->|\isasep\isanewline%
   8.190 +\verb|  Toplevel.transition -> Toplevel.transition| \\
   8.191 +  \indexml{Toplevel.proof-to-theory}\verb|Toplevel.proof_to_theory: (Proof.state -> theory) ->|\isasep\isanewline%
   8.192 +\verb|  Toplevel.transition -> Toplevel.transition| \\
   8.193 +  \end{mldecls}
   8.194 +
   8.195 +  \begin{description}
   8.196 +
   8.197 +  \item \verb|Toplevel.print| sets the print flag, which causes the
   8.198 +  resulting state of the transition to be echoed in interactive mode.
   8.199 +
   8.200 +  \item \verb|Toplevel.no_timing| indicates that the transition should
   8.201 +  never show timing information, e.g.\ because it is merely a
   8.202 +  diagnostic command.
   8.203 +
   8.204 +  \item \verb|Toplevel.keep| adjoins a diagnostic function.
   8.205 +
   8.206 +  \item \verb|Toplevel.theory| adjoins a theory transformer.
   8.207 +
   8.208 +  \item \verb|Toplevel.theory_to_proof| adjoins a global goal function,
   8.209 +  which turns a theory into a proof state.  The theory must not be
   8.210 +  changed here!  The generic Isar goal setup includes an argument that
   8.211 +  specifies how to apply the proven result to the theory, when the
   8.212 +  proof is finished.
   8.213 +
   8.214 +  \item \verb|Toplevel.proof| adjoins a deterministic proof command,
   8.215 +  with a singleton result state.
   8.216 +
   8.217 +  \item \verb|Toplevel.proofs| adjoins a general proof command, with
   8.218 +  zero or more result states (represented as a lazy list).
   8.219 +
   8.220 +  \item \verb|Toplevel.proof_to_theory| adjoins a concluding proof
   8.221 +  command, that returns the resulting theory, after storing the
   8.222 +  resulting facts etc.
   8.223 +
   8.224 +  \end{description}%
   8.225 +\end{isamarkuptext}%
   8.226 +\isamarkuptrue%
   8.227 +%
   8.228 +\endisatagmlref
   8.229 +{\isafoldmlref}%
   8.230 +%
   8.231 +\isadelimmlref
   8.232 +%
   8.233 +\endisadelimmlref
   8.234 +%
   8.235 +\isamarkupsubsection{Toplevel control%
   8.236 +}
   8.237 +\isamarkuptrue%
   8.238 +%
   8.239 +\begin{isamarkuptext}%
   8.240 +Apart from regular toplevel transactions there are a few
   8.241 +  special control commands that modify the behavior the toplevel
   8.242 +  itself, and only make sense in interactive mode.  Under normal
   8.243 +  circumstances, the user encounters these only implicitly as part of
   8.244 +  the protocol between the Isabelle/Isar system and a user-interface
   8.245 +  such as ProofGeneral.
   8.246 +
   8.247 +  \begin{description}
   8.248 +
   8.249 +  \item \isacommand{undo} follows the three-level hierarchy of empty
   8.250 +  toplevel vs.\ theory vs.\ proof: undo within a proof reverts to the
   8.251 +  previous proof context, undo after a proof reverts to the theory
   8.252 +  before the initial goal statement, undo of a theory command reverts
   8.253 +  to the previous theory value, undo of a theory header discontinues
   8.254 +  the current theory development and removes it from the theory
   8.255 +  database (\secref{sec:theory-database}).
   8.256 +
   8.257 +  \item \isacommand{kill} aborts the current level of development:
   8.258 +  kill in a proof context reverts to the theory before the initial
   8.259 +  goal statement, kill in a theory context aborts the current theory
   8.260 +  development, removing it from the database.
   8.261 +
   8.262 +  \item \isacommand{exit} drops out of the Isar toplevel into the
   8.263 +  underlying {\ML} toplevel (\secref{sec:ML-toplevel}).  The Isar
   8.264 +  toplevel state is preserved and may be continued later.
   8.265 +
   8.266 +  \item \isacommand{quit} terminates the Isabelle/Isar process without
   8.267 +  saving.
   8.268 +
   8.269 +  \end{description}%
   8.270 +\end{isamarkuptext}%
   8.271 +\isamarkuptrue%
   8.272 +%
   8.273 +\isamarkupsection{ML toplevel \label{sec:ML-toplevel}%
   8.274 +}
   8.275 +\isamarkuptrue%
   8.276 +%
   8.277 +\begin{isamarkuptext}%
   8.278 +The {\ML} toplevel provides a read-compile-eval-print loop for
   8.279 +  {\ML} values, types, structures, and functors.  {\ML} declarations
   8.280 +  operate on the global system state, which consists of the compiler
   8.281 +  environment plus the values of {\ML} reference variables.  There is
   8.282 +  no clean way to undo {\ML} declarations, except for reverting to a
   8.283 +  previously saved state of the whole Isabelle process.  {\ML} input
   8.284 +  is either read interactively from a TTY, or from a string (usually
   8.285 +  within a theory text), or from a source file (usually associated
   8.286 +  with a theory).
   8.287 +
   8.288 +  Whenever the {\ML} toplevel is active, the current Isabelle theory
   8.289 +  context is passed as an internal reference variable.  Thus {\ML}
   8.290 +  code may access the theory context during compilation, it may even
   8.291 +  change the value of a theory being under construction --- following
   8.292 +  the usual linearity restrictions (cf.~\secref{sec:context-theory}).%
   8.293 +\end{isamarkuptext}%
   8.294 +\isamarkuptrue%
   8.295 +%
   8.296 +\isadelimmlref
   8.297 +%
   8.298 +\endisadelimmlref
   8.299 +%
   8.300 +\isatagmlref
   8.301 +%
   8.302 +\begin{isamarkuptext}%
   8.303 +\begin{mldecls}
   8.304 +  \indexml{context}\verb|context: theory -> unit| \\
   8.305 +  \indexml{the-context}\verb|the_context: unit -> theory| \\
   8.306 +  \indexml{Context.$>$$>$ }\verb|Context.>> : (theory -> theory) -> unit| \\
   8.307 +  \end{mldecls}
   8.308 +
   8.309 +  \begin{description}
   8.310 +
   8.311 +  \item \verb|context|~\isa{thy} sets the {\ML} theory context to
   8.312 +  \isa{thy}.  This is usually performed automatically by the system,
   8.313 +  when dropping out of the interactive Isar toplevel into {\ML}, or
   8.314 +  when Isar invokes {\ML} to process code from a string or a file.
   8.315 +
   8.316 +  \item \verb|the_context ()| refers to the theory context of the
   8.317 +  {\ML} toplevel --- at compile time!  {\ML} code needs to take care
   8.318 +  to refer to \verb|the_context ()| correctly, recall that evaluation
   8.319 +  of a function body is delayed until actual runtime.  Moreover,
   8.320 +  persistent {\ML} toplevel bindings to an unfinished theory should be
   8.321 +  avoided: code should either project out the desired information
   8.322 +  immediately, or produce an explicit \verb|theory_ref| (cf.\
   8.323 +  \secref{sec:context-theory}).
   8.324 +
   8.325 +  \item \verb|Context.>>|~\isa{f} applies theory transformation
   8.326 +  \isa{f} to the current theory of the {\ML} toplevel.  In order to
   8.327 +  work as expected, the theory should be still under construction, and
   8.328 +  the Isar language element that invoked the {\ML} compiler in the
   8.329 +  first place shoule be ready to accept the changed theory value
   8.330 +  (e.g.\ \isakeyword{ML-setup}, but not plain \isakeyword{ML}).
   8.331 +  Otherwise the theory may get destroyed!
   8.332 +
   8.333 +  \end{description}
   8.334 +
   8.335 +  It is very important to note that the above functions are really
   8.336 +  restricted to the compile time, even though the {\ML} compiler is
   8.337 +  invoked at runtime!  The majority of {\ML} code uses explicit
   8.338 +  functional arguments of a theory or proof context, as required.
   8.339 +  Thus it may get run in an arbitrary context later on.
   8.340 +
   8.341 +  \bigskip
   8.342 +
   8.343 +  \begin{mldecls}
   8.344 +  \indexml{Isar.main}\verb|Isar.main: unit -> unit| \\
   8.345 +  \indexml{Isar.loop}\verb|Isar.loop: unit -> unit| \\
   8.346 +  \indexml{Isar.state}\verb|Isar.state: unit -> Toplevel.state| \\
   8.347 +  \indexml{Isar.exn}\verb|Isar.exn: unit -> (exn * string) option| \\
   8.348 +  \end{mldecls}
   8.349 +
   8.350 +  \begin{description}
   8.351 +
   8.352 +  \item \verb|Isar.main ()| invokes the Isar toplevel from {\ML},
   8.353 +  initializing the state to empty toplevel state.
   8.354 +
   8.355 +  \item \verb|Isar.loop ()| continues the Isar toplevel with the
   8.356 +  current state, after dropping out of the Isar toplevel loop.
   8.357 +
   8.358 +  \item \verb|Isar.state ()| and \verb|Isar.exn ()| get current
   8.359 +  toplevel state and optional error condition, respectively.  This
   8.360 +  only works after dropping out of the Isar toplevel loop.
   8.361 +
   8.362 +  \end{description}%
   8.363 +\end{isamarkuptext}%
   8.364 +\isamarkuptrue%
   8.365 +%
   8.366 +\endisatagmlref
   8.367 +{\isafoldmlref}%
   8.368 +%
   8.369 +\isadelimmlref
   8.370 +%
   8.371 +\endisadelimmlref
   8.372 +%
   8.373 +\isamarkupsection{Theory database%
   8.374 +}
   8.375 +\isamarkuptrue%
   8.376 +%
   8.377 +\begin{isamarkuptext}%
   8.378 +The theory database maintains a collection of theories,
   8.379 +  together with some administrative information about the original
   8.380 +  sources, which are held in an external store (i.e.\ a collection of
   8.381 +  directories within the regular file system of the underlying
   8.382 +  platform).
   8.383 +
   8.384 +  The theory database is organized as a directed acyclic graph, with
   8.385 +  entries referenced by theory name.  Although some external
   8.386 +  interfaces allow to include a directory specification, this is only
   8.387 +  a hint to the underlying theory loader mechanism: the internal
   8.388 +  theory name space is flat.
   8.389 +
   8.390 +  Theory \isa{A} is associated with the main theory file \isa{A}\verb,.thy,, which needs to be accessible through the theory
   8.391 +  loader path.  A number of optional {\ML} source files may be
   8.392 +  associated with each theory, by declaring these dependencies in the
   8.393 +  theory header as \isa{{\isasymUSES}}, and loading them consecutively
   8.394 +  within the theory context.  The system keeps track of incoming {\ML}
   8.395 +  sources and associates them with the current theory.  The special
   8.396 +  theory {\ML} file \isa{A}\verb,.ML, is loaded after a theory has
   8.397 +  been concluded, in order to support legacy proof {\ML} proof
   8.398 +  scripts.
   8.399 +
   8.400 +  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}:
   8.401 +
   8.402 +  \begin{itemize}
   8.403 +
   8.404 +  \item \isa{update\ A} introduces a link of \isa{A} with a
   8.405 +  \isa{theory} value of the same name; it asserts that the theory
   8.406 +  sources are consistent with that value.
   8.407 +
   8.408 +  \item \isa{outdate\ A} invalidates the link of a theory database
   8.409 +  entry to its sources, but retains the present theory value.
   8.410 +
   8.411 +  \item \isa{remove\ A} removes entry \isa{A} from the theory
   8.412 +  database.
   8.413 +  
   8.414 +  \end{itemize}
   8.415 +
   8.416 +  These actions are propagated to sub- or super-graphs of a theory
   8.417 +  entry in the usual way, in order to preserve global consistency of
   8.418 +  the state of all loaded theories with the sources of the external
   8.419 +  store.  This implies causal dependencies of certain actions: \isa{update} or \isa{outdate} of an entry will \isa{outdate}
   8.420 +  all descendants; \isa{remove} will \isa{remove} all
   8.421 +  descendants.
   8.422 +
   8.423 +  \medskip There are separate user-level interfaces to operate on the
   8.424 +  theory database directly or indirectly.  The primitive actions then
   8.425 +  just happen automatically while working with the system.  In
   8.426 +  particular, processing a theory header \isa{{\isasymTHEORY}\ A\ {\isasymIMPORTS}\ B\isactrlsub {\isadigit{1}}\ {\isasymdots}\ B\isactrlsub n\ {\isasymBEGIN}} ensure that the
   8.427 +  sub-graph of the collective imports \isa{B\isactrlsub {\isadigit{1}}\ {\isasymdots}\ B\isactrlsub n}
   8.428 +  is up-to-date.  Earlier theories are reloaded as required, with
   8.429 +  \isa{update} actions proceeding in topological order according to
   8.430 +  theory dependencies.  There may be also a wave of implied \isa{outdate} actions for derived theory nodes until a stable situation
   8.431 +  is achieved eventually.%
   8.432 +\end{isamarkuptext}%
   8.433 +\isamarkuptrue%
   8.434 +%
   8.435 +\isadelimmlref
   8.436 +%
   8.437 +\endisadelimmlref
   8.438 +%
   8.439 +\isatagmlref
   8.440 +%
   8.441 +\begin{isamarkuptext}%
   8.442 +\begin{mldecls}
   8.443 +  \indexml{theory}\verb|theory: string -> theory| \\
   8.444 +  \indexml{use-thy}\verb|use_thy: string -> unit| \\
   8.445 +  \indexml{update-thy}\verb|update_thy: string -> unit| \\
   8.446 +  \indexml{use-thy-only}\verb|use_thy_only: string -> unit| \\
   8.447 +  \indexml{update-thy-only}\verb|update_thy_only: string -> unit| \\
   8.448 +  \indexml{touch-thy}\verb|touch_thy: string -> unit| \\
   8.449 +  \indexml{remove-thy}\verb|remove_thy: string -> unit| \\[1ex]
   8.450 +  \indexml{ThyInfo.begin-theory}\verb|ThyInfo.begin_theory|\verb|: ... -> bool -> theory| \\
   8.451 +  \indexml{ThyInfo.end-theory}\verb|ThyInfo.end_theory: theory -> theory| \\
   8.452 +  \indexml{ThyInfo.register-theory}\verb|ThyInfo.register_theory: theory -> unit| \\[1ex]
   8.453 +  \verb|datatype action = Update |\verb,|,\verb| Outdate |\verb,|,\verb| Remove| \\
   8.454 +  \indexml{ThyInfo.add-hook}\verb|ThyInfo.add_hook: (ThyInfo.action -> string -> unit) -> unit| \\
   8.455 +  \end{mldecls}
   8.456 +
   8.457 +  \begin{description}
   8.458 +
   8.459 +  \item \verb|theory|~\isa{A} retrieves the theory value presently
   8.460 +  associated with \isa{A}.  The result is not necessarily
   8.461 +  up-to-date!
   8.462 +
   8.463 +  \item \verb|use_thy|~\isa{A} loads theory \isa{A} if it is absent
   8.464 +  or out-of-date.  It ensures that all parent theories are available
   8.465 +  as well, but does not reload them if older versions are already
   8.466 +  present.
   8.467 +
   8.468 +  \item \verb|update_thy| is similar to \verb|use_thy|, but ensures that
   8.469 +  the \isa{A} and all of its ancestors are fully up-to-date.
   8.470 +
   8.471 +  \item \verb|use_thy_only|~\isa{A} is like \verb|use_thy|~\isa{A},
   8.472 +  but refrains from loading the attached \isa{A}\verb,.ML, file.
   8.473 +  This is occasionally useful in replaying legacy {\ML} proof scripts
   8.474 +  by hand.
   8.475 +  
   8.476 +  \item \verb|update_thy_only| is analogous to \verb|use_thy_only|, but
   8.477 +  proceeds like \verb|update_thy| for ancestors.
   8.478 +
   8.479 +  \item \verb|touch_thy|~\isa{A} performs \isa{outdate} action on
   8.480 +  theory \isa{A} and all of its descendants.
   8.481 +
   8.482 +  \item \verb|remove_thy|~\isa{A} removes \isa{A} and all of its
   8.483 +  descendants from the theory database.
   8.484 +
   8.485 +  \item \verb|ThyInfo.begin_theory| is the basic operation behind a
   8.486 +  \isa{{\isasymTHEORY}} header declaration.  The boolean argument
   8.487 +  indicates the strictness of treating ancestors: for \verb|true| (as
   8.488 +  in interactive mode) like \verb|update_thy|, and for \verb|false| (as
   8.489 +  in batch mode) like \verb|use_thy|.  This is {\ML} functions is
   8.490 +  normally not invoked directly.
   8.491 +
   8.492 +  \item \verb|ThyInfo.end_theory| concludes the loading of a theory
   8.493 +  proper; an attached theory {\ML} file may be still loaded later on.
   8.494 +  This is {\ML} functions is normally not invoked directly.
   8.495 +
   8.496 +  \item \verb|ThyInfo.register_theory|~{text thy} registers an existing
   8.497 +  theory value with the theory loader database.  There is no
   8.498 +  management of associated sources; this is mainly for bootstrapping.
   8.499 +
   8.500 +  \item \verb|ThyInfo.add_hook|~\isa{f} registers function \isa{f} as a hook for theory database actions.  The function will be
   8.501 +  invoked with the action and theory name being involved; thus derived
   8.502 +  actions may be performed in associated system components, e.g.\
   8.503 +  maintaining the state of an editor for theory sources.
   8.504 +
   8.505 +  The kind and order of actions occurring in practice depends both on
   8.506 +  user interactions and the internal process of resolving theory
   8.507 +  imports.  Hooks should not rely on a particular policy here!  Any
   8.508 +  exceptions raised by the hook are ignored by the theory database.
   8.509 +
   8.510 +  \end{description}%
   8.511 +\end{isamarkuptext}%
   8.512 +\isamarkuptrue%
   8.513 +%
   8.514 +\endisatagmlref
   8.515 +{\isafoldmlref}%
   8.516 +%
   8.517 +\isadelimmlref
   8.518 +%
   8.519 +\endisadelimmlref
   8.520 +%
   8.521 +\isadelimtheory
   8.522 +%
   8.523 +\endisadelimtheory
   8.524 +%
   8.525 +\isatagtheory
   8.526 +\isacommand{end}\isamarkupfalse%
   8.527 +%
   8.528 +\endisatagtheory
   8.529 +{\isafoldtheory}%
   8.530 +%
   8.531 +\isadelimtheory
   8.532 +%
   8.533 +\endisadelimtheory
   8.534 +\isanewline
   8.535 +\end{isabellebody}%
   8.536 +%%% Local Variables:
   8.537 +%%% mode: latex
   8.538 +%%% TeX-master: "root"
   8.539 +%%% End:
     9.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.2 +++ b/doc-src/IsarImplementation/Thy/document/locale.tex	Mon Jan 02 20:16:52 2006 +0100
     9.3 @@ -0,0 +1,62 @@
     9.4 +%
     9.5 +\begin{isabellebody}%
     9.6 +\def\isabellecontext{locale}%
     9.7 +%
     9.8 +\isadelimtheory
     9.9 +\isanewline
    9.10 +\isanewline
    9.11 +\isanewline
    9.12 +%
    9.13 +\endisadelimtheory
    9.14 +%
    9.15 +\isatagtheory
    9.16 +\isacommand{theory}\isamarkupfalse%
    9.17 +\ {\isachardoublequoteopen}locale{\isachardoublequoteclose}\ \isakeyword{imports}\ base\ \isakeyword{begin}%
    9.18 +\endisatagtheory
    9.19 +{\isafoldtheory}%
    9.20 +%
    9.21 +\isadelimtheory
    9.22 +%
    9.23 +\endisadelimtheory
    9.24 +%
    9.25 +\isamarkupchapter{Structured specifications%
    9.26 +}
    9.27 +\isamarkuptrue%
    9.28 +%
    9.29 +\isamarkupsection{Specification elements%
    9.30 +}
    9.31 +\isamarkuptrue%
    9.32 +%
    9.33 +\begin{isamarkuptext}%
    9.34 +FIXME%
    9.35 +\end{isamarkuptext}%
    9.36 +\isamarkuptrue%
    9.37 +%
    9.38 +\isamarkupsection{Locales%
    9.39 +}
    9.40 +\isamarkuptrue%
    9.41 +%
    9.42 +\begin{isamarkuptext}%
    9.43 +FIXME%
    9.44 +\end{isamarkuptext}%
    9.45 +\isamarkuptrue%
    9.46 +%
    9.47 +\isadelimtheory
    9.48 +%
    9.49 +\endisadelimtheory
    9.50 +%
    9.51 +\isatagtheory
    9.52 +\isacommand{end}\isamarkupfalse%
    9.53 +%
    9.54 +\endisatagtheory
    9.55 +{\isafoldtheory}%
    9.56 +%
    9.57 +\isadelimtheory
    9.58 +%
    9.59 +\endisadelimtheory
    9.60 +\isanewline
    9.61 +\end{isabellebody}%
    9.62 +%%% Local Variables:
    9.63 +%%% mode: latex
    9.64 +%%% TeX-master: "root"
    9.65 +%%% End:
    10.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.2 +++ b/doc-src/IsarImplementation/Thy/document/logic.tex	Mon Jan 02 20:16:52 2006 +0100
    10.3 @@ -0,0 +1,192 @@
    10.4 +%
    10.5 +\begin{isabellebody}%
    10.6 +\def\isabellecontext{logic}%
    10.7 +%
    10.8 +\isadelimtheory
    10.9 +\isanewline
   10.10 +\isanewline
   10.11 +\isanewline
   10.12 +%
   10.13 +\endisadelimtheory
   10.14 +%
   10.15 +\isatagtheory
   10.16 +\isacommand{theory}\isamarkupfalse%
   10.17 +\ logic\ \isakeyword{imports}\ base\ \isakeyword{begin}%
   10.18 +\endisatagtheory
   10.19 +{\isafoldtheory}%
   10.20 +%
   10.21 +\isadelimtheory
   10.22 +%
   10.23 +\endisadelimtheory
   10.24 +%
   10.25 +\isamarkupchapter{Pure logic%
   10.26 +}
   10.27 +\isamarkuptrue%
   10.28 +%
   10.29 +\isamarkupsection{Syntax%
   10.30 +}
   10.31 +\isamarkuptrue%
   10.32 +%
   10.33 +\isamarkupsubsection{Simply-typed lambda calculus%
   10.34 +}
   10.35 +\isamarkuptrue%
   10.36 +%
   10.37 +\begin{isamarkuptext}%
   10.38 +FIXME
   10.39 +
   10.40 +\glossary{Type}{FIXME}
   10.41 +\glossary{Term}{FIXME}%
   10.42 +\end{isamarkuptext}%
   10.43 +\isamarkuptrue%
   10.44 +%
   10.45 +\isamarkupsubsection{The order-sorted algebra of types%
   10.46 +}
   10.47 +\isamarkuptrue%
   10.48 +%
   10.49 +\begin{isamarkuptext}%
   10.50 +FIXME
   10.51 +
   10.52 +\glossary{Type constructor}{FIXME}
   10.53 +
   10.54 +\glossary{Type class}{FIXME}
   10.55 +
   10.56 +\glossary{Type arity}{FIXME}
   10.57 +
   10.58 +\glossary{Sort}{FIXME}%
   10.59 +\end{isamarkuptext}%
   10.60 +\isamarkuptrue%
   10.61 +%
   10.62 +\isamarkupsubsection{Type-inference and schematic polymorphism%
   10.63 +}
   10.64 +\isamarkuptrue%
   10.65 +%
   10.66 +\begin{isamarkuptext}%
   10.67 +FIXME
   10.68 +
   10.69 +\glossary{Schematic polymorphism}{FIXME}
   10.70 +
   10.71 +\glossary{Type variable}{FIXME}%
   10.72 +\end{isamarkuptext}%
   10.73 +\isamarkuptrue%
   10.74 +%
   10.75 +\isamarkupsection{Theory%
   10.76 +}
   10.77 +\isamarkuptrue%
   10.78 +%
   10.79 +\begin{isamarkuptext}%
   10.80 +FIXME
   10.81 +
   10.82 +\glossary{Constant}{Essentially a \seeglossary{fixed variable} of the
   10.83 +theory context, but slightly more flexible since it may be used at
   10.84 +different type-instances, due to \seeglossary{schematic
   10.85 +polymorphism.}}%
   10.86 +\end{isamarkuptext}%
   10.87 +\isamarkuptrue%
   10.88 +%
   10.89 +\isamarkupsection{Deduction%
   10.90 +}
   10.91 +\isamarkuptrue%
   10.92 +%
   10.93 +\begin{isamarkuptext}%
   10.94 +FIXME
   10.95 +
   10.96 +\glossary{Proposition}{A \seeglossary{term} of \seeglossary{type}
   10.97 +\isa{prop}.  Internally, there is nothing special about
   10.98 +propositions apart from their type, but the concrete syntax enforces a
   10.99 +clear distinction.  Propositions are structured via implication \isa{A\ {\isasymLongrightarrow}\ B} or universal quantification \isa{{\isasymAnd}x{\isachardot}\ B\ x} --- anything
  10.100 +else is considered atomic.  The canonical form for propositions is
  10.101 +that of a \seeglossary{Hereditary Harrop Formula}.}
  10.102 +
  10.103 +\glossary{Theorem}{A proven proposition within a certain theory and
  10.104 +proof context, formally \isa{{\isasymGamma}\ {\isasymturnstile}\isactrlsub {\isasymTheta}\ {\isasymphi}}; both contexts are
  10.105 +rarely spelled out explicitly.  Theorems are usually normalized
  10.106 +according to the \seeglossary{HHF} format.}
  10.107 +
  10.108 +\glossary{Fact}{Sometimes used interchangably for
  10.109 +\seeglossary{theorem}.  Strictly speaking, a list of theorems,
  10.110 +essentially an extra-logical conjunction.  Facts emerge either as
  10.111 +local assumptions, or as results of local goal statements --- both may
  10.112 +be simultaneous, hence the list representation.}
  10.113 +
  10.114 +\glossary{Schematic variable}{FIXME}
  10.115 +
  10.116 +\glossary{Fixed variable}{A variable that is bound within a certain
  10.117 +proof context; an arbitrary-but-fixed entity within a portion of proof
  10.118 +text.}
  10.119 +
  10.120 +\glossary{Free variable}{Synonymous for \seeglossary{fixed variable}.}
  10.121 +
  10.122 +\glossary{Bound variable}{FIXME}
  10.123 +
  10.124 +\glossary{Variable}{See \seeglossary{schematic variable},
  10.125 +\seeglossary{fixed variable}, \seeglossary{bound variable}, or
  10.126 +\seeglossary{type variable}.  The distinguishing feature of different
  10.127 +variables is their binding scope.}%
  10.128 +\end{isamarkuptext}%
  10.129 +\isamarkuptrue%
  10.130 +%
  10.131 +\isamarkupsubsection{Primitive inferences%
  10.132 +}
  10.133 +\isamarkuptrue%
  10.134 +%
  10.135 +\begin{isamarkuptext}%
  10.136 +FIXME%
  10.137 +\end{isamarkuptext}%
  10.138 +\isamarkuptrue%
  10.139 +%
  10.140 +\isamarkupsubsection{Higher-order resolution%
  10.141 +}
  10.142 +\isamarkuptrue%
  10.143 +%
  10.144 +\begin{isamarkuptext}%
  10.145 +FIXME
  10.146 +
  10.147 +\glossary{Hereditary Harrop Formula}{The set of propositions in HHF
  10.148 +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}.
  10.149 +Any proposition may be put into HHF form by normalizing with the rule
  10.150 +\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
  10.151 +quantifier prefix is represented via \seeglossary{schematic
  10.152 +variables}, such that the top-level structure is merely that of a
  10.153 +\seeglossary{Horn Clause}}.
  10.154 +
  10.155 +\glossary{HHF}{See \seeglossary{Hereditary Harrop Formula}.}%
  10.156 +\end{isamarkuptext}%
  10.157 +\isamarkuptrue%
  10.158 +%
  10.159 +\isamarkupsubsection{Equational reasoning%
  10.160 +}
  10.161 +\isamarkuptrue%
  10.162 +%
  10.163 +\begin{isamarkuptext}%
  10.164 +FIXME%
  10.165 +\end{isamarkuptext}%
  10.166 +\isamarkuptrue%
  10.167 +%
  10.168 +\isamarkupsection{Proof terms%
  10.169 +}
  10.170 +\isamarkuptrue%
  10.171 +%
  10.172 +\begin{isamarkuptext}%
  10.173 +FIXME%
  10.174 +\end{isamarkuptext}%
  10.175 +\isamarkuptrue%
  10.176 +%
  10.177 +\isadelimtheory
  10.178 +%
  10.179 +\endisadelimtheory
  10.180 +%
  10.181 +\isatagtheory
  10.182 +\isacommand{end}\isamarkupfalse%
  10.183 +%
  10.184 +\endisatagtheory
  10.185 +{\isafoldtheory}%
  10.186 +%
  10.187 +\isadelimtheory
  10.188 +%
  10.189 +\endisadelimtheory
  10.190 +\isanewline
  10.191 +\end{isabellebody}%
  10.192 +%%% Local Variables:
  10.193 +%%% mode: latex
  10.194 +%%% TeX-master: "root"
  10.195 +%%% End:
    11.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    11.2 +++ b/doc-src/IsarImplementation/Thy/document/prelim.tex	Mon Jan 02 20:16:52 2006 +0100
    11.3 @@ -0,0 +1,443 @@
    11.4 +%
    11.5 +\begin{isabellebody}%
    11.6 +\def\isabellecontext{prelim}%
    11.7 +%
    11.8 +\isadelimtheory
    11.9 +\isanewline
   11.10 +\isanewline
   11.11 +\isanewline
   11.12 +%
   11.13 +\endisadelimtheory
   11.14 +%
   11.15 +\isatagtheory
   11.16 +\isacommand{theory}\isamarkupfalse%
   11.17 +\ prelim\ \isakeyword{imports}\ base\ \isakeyword{begin}%
   11.18 +\endisatagtheory
   11.19 +{\isafoldtheory}%
   11.20 +%
   11.21 +\isadelimtheory
   11.22 +%
   11.23 +\endisadelimtheory
   11.24 +%
   11.25 +\isamarkupchapter{Preliminaries%
   11.26 +}
   11.27 +\isamarkuptrue%
   11.28 +%
   11.29 +\isamarkupsection{Named entities%
   11.30 +}
   11.31 +\isamarkuptrue%
   11.32 +%
   11.33 +\begin{isamarkuptext}%
   11.34 +Named entities of different kinds (logical constant, type,
   11.35 +type class, theorem, method etc.) live in separate name spaces.  It is
   11.36 +usually clear from the occurrence of a name which kind of entity it
   11.37 +refers to.  For example, proof method \isa{foo} vs.\ theorem
   11.38 +\isa{foo} vs.\ logical constant \isa{foo} are easily
   11.39 +distinguished by means of the syntactic context.  A notable exception
   11.40 +are logical identifiers within a term (\secref{sec:terms}): constants,
   11.41 +fixed variables, and bound variables all share the same identifier
   11.42 +syntax, but are distinguished by their scope.
   11.43 +
   11.44 +Each name space is organized as a collection of \emph{qualified
   11.45 +names}, which consist of a sequence of basic name components separated
   11.46 +by dots: \isa{Bar{\isachardot}bar{\isachardot}foo}, \isa{Bar{\isachardot}foo}, and \isa{foo}
   11.47 +are examples for valid qualified names.  Name components are
   11.48 +subdivided into \emph{symbols}, which constitute the smallest textual
   11.49 +unit in Isabelle --- raw characters are normally not encountered
   11.50 +directly.%
   11.51 +\end{isamarkuptext}%
   11.52 +\isamarkuptrue%
   11.53 +%
   11.54 +\isamarkupsubsection{Strings of symbols%
   11.55 +}
   11.56 +\isamarkuptrue%
   11.57 +%
   11.58 +\begin{isamarkuptext}%
   11.59 +Isabelle strings consist of a sequence of
   11.60 +symbols\glossary{Symbol}{The smalles unit of text in Isabelle,
   11.61 +subsumes plain ASCII characters as well as an infinite collection of
   11.62 +named symbols (for greek, math etc.).}, which are either packed as an
   11.63 +actual \isa{string}, or represented as a list.  Each symbol is in
   11.64 +itself a small string of the following form:
   11.65 +
   11.66 +\begin{enumerate}
   11.67 +
   11.68 +\item either a singleton ASCII character ``\isa{c}'' (with
   11.69 +character code 0--127), for example ``\verb,a,'',
   11.70 +
   11.71 +\item or a regular symbol ``\verb,\,\verb,<,\isa{ident}\verb,>,'',
   11.72 +for example ``\verb,\,\verb,<alpha>,'',
   11.73 +
   11.74 +\item or a control symbol ``\verb,\,\verb,<^,\isa{ident}\verb,>,'', for example ``\verb,\,\verb,<^bold>,'',
   11.75 +
   11.76 +\item or a raw control symbol ``\verb,\,\verb,<^raw:,\isa{{\isasymdots}}\verb,>,'' where ``\isa{{\isasymdots}}'' refers to any printable ASCII
   11.77 +character (excluding ``\verb,>,'') or non-ASCII character, for example
   11.78 +``\verb,\,\verb,<^raw:$\sum_{i = 1}^n$>,'',
   11.79 +
   11.80 +\item or a numbered raw control symbol ``\verb,\,\verb,<^raw,\isa{nnn}\verb,>, where \isa{nnn} are digits, for example
   11.81 +``\verb,\,\verb,<^raw42>,''.
   11.82 +
   11.83 +\end{enumerate}
   11.84 +
   11.85 +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
   11.86 +control symbols available, but a certain collection of standard
   11.87 +symbols is treated specifically.  For example,
   11.88 +``\verb,\,\verb,<alpha>,'' is classified as a (non-ASCII) letter,
   11.89 +which means it may occur within regular Isabelle identifier syntax.
   11.90 +
   11.91 +Output of symbols depends on the print mode (\secref{sec:print-mode}).
   11.92 +For example, the standard {\LaTeX} setup of the Isabelle document
   11.93 +preparation system would present ``\verb,\,\verb,<alpha>,'' as \isa{{\isasymalpha}}, and ``\verb,\,\verb,<^bold>,\verb,\,\verb,<alpha>,'' as \isa{\isactrlbold {\isasymalpha}}.
   11.94 +
   11.95 +\medskip It is important to note that the character set underlying
   11.96 +Isabelle symbols is plain 7-bit ASCII.  Since 8-bit characters are
   11.97 +passed through transparently, Isabelle may easily process actual
   11.98 +Unicode/UCS data (using the well-known UTF-8 encoding, for example).
   11.99 +Unicode provides its own collection of mathematical symbols, but there
  11.100 +is presently no link to Isabelle's named ones; both kinds of symbols
  11.101 +coexist independently.%
  11.102 +\end{isamarkuptext}%
  11.103 +\isamarkuptrue%
  11.104 +%
  11.105 +\isadelimmlref
  11.106 +%
  11.107 +\endisadelimmlref
  11.108 +%
  11.109 +\isatagmlref
  11.110 +%
  11.111 +\begin{isamarkuptext}%
  11.112 +\begin{mldecls}
  11.113 +  \indexmltype{Symbol.symbol}\verb|type Symbol.symbol| \\
  11.114 +  \indexml{Symbol.explode}\verb|Symbol.explode: string -> Symbol.symbol list| \\
  11.115 +  \indexml{Symbol.is-letter}\verb|Symbol.is_letter: Symbol.symbol -> bool| \\
  11.116 +  \indexml{Symbol.is-digit}\verb|Symbol.is_digit: Symbol.symbol -> bool| \\
  11.117 +  \indexml{Symbol.is-quasi}\verb|Symbol.is_quasi: Symbol.symbol -> bool| \\
  11.118 +  \indexml{Symbol.is-blank}\verb|Symbol.is_blank: Symbol.symbol -> bool| \\
  11.119 +  \indexmltype{Symbol.sym}\verb|type Symbol.sym| \\
  11.120 +  \indexml{Symbol.decode}\verb|Symbol.decode: Symbol.symbol -> Symbol.sym| \\
  11.121 +  \end{mldecls}
  11.122 +
  11.123 +  \begin{description}
  11.124 +
  11.125 +  \item \verb|Symbol.symbol| represents Isabelle symbols; this type
  11.126 +  is merely an alias for \verb|string|, but emphasizes the
  11.127 +  specific format encountered here.
  11.128 +
  11.129 +  \item \verb|Symbol.explode|~\isa{s} produces an actual symbol
  11.130 +  list from the packed form usually encountered as user input.  This
  11.131 +  function replaces \verb|String.explode| for virtually all purposes
  11.132 +  of manipulating text in Isabelle!  Plain \isa{implode} may be
  11.133 +  used for the reverse operation.
  11.134 +
  11.135 +  \item \verb|Symbol.is_letter|, \verb|Symbol.is_digit|, \verb|Symbol.is_quasi|, \verb|Symbol.is_blank| classify certain symbols
  11.136 +  (both ASCII and several named ones) according to fixed syntactic
  11.137 +  convections of Isabelle, e.g.\ see \cite{isabelle-isar-ref}.
  11.138 +
  11.139 +  \item \verb|Symbol.sym| is a concrete datatype that represents
  11.140 +  the different kinds of symbols explicitly as \verb|Symbol.Char|,
  11.141 +  \verb|Symbol.Sym|, \verb|Symbol.Ctrl|, or \verb|Symbol.Raw|.
  11.142 +
  11.143 +  \item \verb|Symbol.decode| converts the string representation of a
  11.144 +  symbol into the explicit datatype version.
  11.145 +
  11.146 +  \end{description}%
  11.147 +\end{isamarkuptext}%
  11.148 +\isamarkuptrue%
  11.149 +%
  11.150 +\endisatagmlref
  11.151 +{\isafoldmlref}%
  11.152 +%
  11.153 +\isadelimmlref
  11.154 +%
  11.155 +\endisadelimmlref
  11.156 +%
  11.157 +\isamarkupsubsection{Qualified names and name spaces%
  11.158 +}
  11.159 +\isamarkuptrue%
  11.160 +%
  11.161 +\isadelimFIXME
  11.162 +%
  11.163 +\endisadelimFIXME
  11.164 +%
  11.165 +\isatagFIXME
  11.166 +%
  11.167 +\begin{isamarkuptext}%
  11.168 +Qualified names are constructed according to implicit naming
  11.169 +principles of the present context.
  11.170 +
  11.171 +
  11.172 +The last component is called \emph{base name}; the remaining prefix of
  11.173 +qualification may be empty.
  11.174 +
  11.175 +Some practical conventions help to organize named entities more
  11.176 +systematically:
  11.177 +
  11.178 +\begin{itemize}
  11.179 +
  11.180 +\item Names are qualified first by the theory name, second by an
  11.181 +optional ``structure''.  For example, a constant \isa{c} declared
  11.182 +as part of a certain structure \isa{b} (say a type definition) in
  11.183 +theory \isa{A} will be named \isa{A{\isachardot}b{\isachardot}c} internally.
  11.184 +
  11.185 +\item
  11.186 +
  11.187 +\item
  11.188 +
  11.189 +\item
  11.190 +
  11.191 +\item
  11.192 +
  11.193 +\end{itemize}
  11.194 +
  11.195 +Names of different kinds of entities are basically independent, but
  11.196 +some practical naming conventions relate them to each other.  For
  11.197 +example, a constant \isa{foo} may be accompanied with theorems
  11.198 +\isa{foo{\isachardot}intro}, \isa{foo{\isachardot}elim}, \isa{foo{\isachardot}simps} etc.  The
  11.199 +same may happen for a type \isa{foo}, which is then apt to cause
  11.200 +clashes in the theorem name space!  To avoid this, we occasionally
  11.201 +follow an additional convention of suffixes that determine the
  11.202 +original kind of entity that a name has been derived.  For example,
  11.203 +constant \isa{foo} is associated with theorem \isa{foo{\isachardot}intro},
  11.204 +type \isa{foo} with theorem \isa{foo{\isacharunderscore}type{\isachardot}intro}, and type
  11.205 +class \isa{foo} with \isa{foo{\isacharunderscore}class{\isachardot}intro}.%
  11.206 +\end{isamarkuptext}%
  11.207 +\isamarkuptrue%
  11.208 +%
  11.209 +\endisatagFIXME
  11.210 +{\isafoldFIXME}%
  11.211 +%
  11.212 +\isadelimFIXME
  11.213 +%
  11.214 +\endisadelimFIXME
  11.215 +%
  11.216 +\isamarkupsection{Structured output%
  11.217 +}
  11.218 +\isamarkuptrue%
  11.219 +%
  11.220 +\isamarkupsubsection{Pretty printing%
  11.221 +}
  11.222 +\isamarkuptrue%
  11.223 +%
  11.224 +\begin{isamarkuptext}%
  11.225 +FIXME%
  11.226 +\end{isamarkuptext}%
  11.227 +\isamarkuptrue%
  11.228 +%
  11.229 +\isamarkupsubsection{Output channels%
  11.230 +}
  11.231 +\isamarkuptrue%
  11.232 +%
  11.233 +\begin{isamarkuptext}%
  11.234 +FIXME%
  11.235 +\end{isamarkuptext}%
  11.236 +\isamarkuptrue%
  11.237 +%
  11.238 +\isamarkupsubsection{Print modes%
  11.239 +}
  11.240 +\isamarkuptrue%
  11.241 +%
  11.242 +\begin{isamarkuptext}%
  11.243 +FIXME%
  11.244 +\end{isamarkuptext}%
  11.245 +\isamarkuptrue%
  11.246 +%
  11.247 +\isamarkupsection{Context \label{sec:context}%
  11.248 +}
  11.249 +\isamarkuptrue%
  11.250 +%
  11.251 +\isadelimFIXME
  11.252 +%
  11.253 +\endisadelimFIXME
  11.254 +%
  11.255 +\isatagFIXME
  11.256 +%
  11.257 +\begin{isamarkuptext}%
  11.258 +What is a context anyway?  A highly advanced
  11.259 +technological and cultural achievement, which took humanity several
  11.260 +thousands of years to be develop, is writing with pen-and-paper.  Here
  11.261 +the paper is the context, or medium.  It accommodates a certain range
  11.262 +of different kinds of pens, but also has some inherent limitations.
  11.263 +For example, carved inscriptions are better done on solid material
  11.264 +like wood or stone.
  11.265 +
  11.266 +Isabelle/Isar distinguishes two key notions of context: \emph{theory
  11.267 +  context}\indexbold{theory context} and \emph{proof context}.\indexbold{proof
  11.268 +  context} To motivate this fundamental division consider the very idea of
  11.269 +logical reasoning which is about judgments $\Gamma \Drv{\Theta} \phi$, where
  11.270 +$\Theta$ is the background theory with declarations of operators and axioms
  11.271 +stating their properties, and $\Gamma$ a collection of hypotheses emerging
  11.272 +temporarily during proof.  For example, the rule of implication-introduction
  11.273 +\[
  11.274 +\infer{\Gamma \Drv{\Theta} A \Imp B}{\Gamma, A \Drv{\Theta} B}
  11.275 +\]
  11.276 +can be read as ``to show $A \Imp B$ we may assume $A$ as hypothesis and need
  11.277 +to show $B$''.  It is characteristic that $\Theta$ is unchanged and $\Gamma$
  11.278 +is only modified according to some general patterns of ``assuming'' and
  11.279 +``discharging'' hypotheses.  This admits the following abbreviated notation,
  11.280 +where the fixed $\Theta$ and locally changed $\Gamma$ are left implicit:
  11.281 +\[
  11.282 +\infer{A \Imp B}{\infer*{B}{[A]}}
  11.283 +\]
  11.284 +
  11.285 +In some logical traditions (e.g.\ Type Theory) there is a tendency to
  11.286 +unify all kinds of declarations within a single notion of context.
  11.287 +This is theoretically very nice, but also more demanding, because
  11.288 +everything is internalized into the logical calculus itself.
  11.289 +Isabelle/Pure is a very simple logic, but achieves many practically
  11.290 +useful concepts by differentiating various basic elements.
  11.291 +
  11.292 +Take polymorphism, for example.  Instead of embarking on the
  11.293 +adventurous enterprise of full higher-order logic with full
  11.294 +type-quantification and polymorphic entities, Isabelle/Pure merely
  11.295 +takes a stripped-down version of Church's Simple Type Theory
  11.296 +\cite{church40}.  Then after the tradition of Gordon's HOL
  11.297 +\cite{mgordon-hol} it is fairly easy to introduce syntactic notions of
  11.298 +type variables and type-constructors, and require every theory
  11.299 +$\Theta$ being closed by type instantiation.  Whenever we wish to
  11.300 +reason with a polymorphic constant or axiom scheme at a particular
  11.301 +type, we may assume that it has been referenced initially at that very
  11.302 +instance (due to the Deduction Theorem).  Thus we achieve the
  11.303 +following \emph{admissible
  11.304 +  rule}\glossary{Admissible rule}{FIXME} of schematic type-instantiation:
  11.305 +
  11.306 +\[
  11.307 +\infer{\phi(\tau)}{\infer*{\phi(\alpha)}{[\alpha]}}
  11.308 +\]
  11.309 +
  11.310 +Using this approach, the structured Isar proof language offers
  11.311 +schematic polymorphism within nested sub-proofs -- similar to that of
  11.312 +polymorphic let-bindings according to Hindley-Milner.\
  11.313 +\cite{milner78}.  All of this is achieved without disintegrating the
  11.314 +rather simplistic logical core.  On the other hand, the succinct rule
  11.315 +presented above already involves rather delicate interaction of the
  11.316 +theory and proof context (with side-conditions not mentioned here),
  11.317 +and unwinding an admissible rule involves induction over derivations.
  11.318 +All of this diversity needs to be accomodated by the system
  11.319 +architecture and actual implementation.
  11.320 +
  11.321 +\medskip Despite these important observations, Isabelle/Isar is not just a
  11.322 +logical calculus, there are further extra-logical aspects to be considered.
  11.323 +Practical experience over the years suggests two context data structures which
  11.324 +are used in rather dissimilar manners, even though there is a considerable
  11.325 +overlap of underlying ideas.
  11.326 +
  11.327 +From the system's perspective the mode of use of theory vs.\ proof context is
  11.328 +the key distinction.  The actual content is merely a generic slot for
  11.329 +\emph{theory data} and \emph{proof data}, respectively.  There are generic
  11.330 +interfaces to declare data entries at any time.  Even the core logic of
  11.331 +Isabelle/Pure registers its very own notion of theory context data (types,
  11.332 +constants, axioms etc.) like any other Isabelle tool out there.  Likewise, the
  11.333 +essentials of Isar proof contexts are one proof data slot among many others,
  11.334 +notably those of derived Isar concepts (e.g.\ calculational reasoning rules).
  11.335 +
  11.336 +In that respect, a theory is more like a stone tablet to carve long-lasting
  11.337 +inscriptions -- but take care not to break it!  While a proof context is like
  11.338 +a block of paper to scribble and dispose quickly.  More recently Isabelle has
  11.339 +started to cultivate the paper-based craftsmanship a bit further, by
  11.340 +maintaining small collections of paper booklets, better known as locales.
  11.341 +
  11.342 +Thus we achive ``thick'' augmented versions of {\boldmath$\Theta$} and
  11.343 +{\boldmath$\Gamma$} to support realistic structured reasoning within a
  11.344 +practically usable system.%
  11.345 +\end{isamarkuptext}%
  11.346 +\isamarkuptrue%
  11.347 +%
  11.348 +\endisatagFIXME
  11.349 +{\isafoldFIXME}%
  11.350 +%
  11.351 +\isadelimFIXME
  11.352 +%
  11.353 +\endisadelimFIXME
  11.354 +%
  11.355 +\isamarkupsubsection{Theory context \label{sec:context-theory}%
  11.356 +}
  11.357 +\isamarkuptrue%
  11.358 +%
  11.359 +\isadelimFIXME
  11.360 +%
  11.361 +\endisadelimFIXME
  11.362 +%
  11.363 +\isatagFIXME
  11.364 +%
  11.365 +\begin{isamarkuptext}%
  11.366 +A theory context consists of management information plus the
  11.367 +actual data, which may be declared by other software modules later on.
  11.368 +The management part is surprisingly complex, we illustrate it by the
  11.369 +following typical situation of incremental theory development.
  11.370 +
  11.371 +\begin{tabular}{rcccl}
  11.372 +        &            & $Pure$ \\
  11.373 +        &            & $\downarrow$ \\
  11.374 +        &            & $FOL$ \\
  11.375 +        & $\swarrow$ &              & $\searrow$ & \\
  11.376 +  $Nat$ &            &              &            & $List$ \\
  11.377 +        & $\searrow$ &              & $\swarrow$ \\
  11.378 +        &            & $Length$ \\
  11.379 +        &            & \multicolumn{3}{l}{~~$\isarkeyword{imports}$} \\
  11.380 +        &            & \multicolumn{3}{l}{~~$\isarkeyword{begin}$} \\
  11.381 +        &            & $\vdots$~~ \\
  11.382 +        &            & $\bullet$~~ \\
  11.383 +        &            & $\vdots$~~ \\
  11.384 +        &            & $\bullet$~~ \\
  11.385 +        &            & $\vdots$~~ \\
  11.386 +        &            & \multicolumn{3}{l}{~~$\isarkeyword{end}$} \\
  11.387 +\end{tabular}
  11.388 +
  11.389 +\begin{itemize}
  11.390 +\item \emph{name}, \emph{parents} and \emph{ancestors}
  11.391 +\item \emph{identity}
  11.392 +\item \emph{intermediate versions}
  11.393 +\end{itemize}
  11.394 +
  11.395 +\begin{description}
  11.396 +\item [draft]
  11.397 +\item [intermediate]
  11.398 +\item [finished]
  11.399 +\end{description}
  11.400 +
  11.401 +\emph{theory reference}%
  11.402 +\end{isamarkuptext}%
  11.403 +\isamarkuptrue%
  11.404 +%
  11.405 +\endisatagFIXME
  11.406 +{\isafoldFIXME}%
  11.407 +%
  11.408 +\isadelimFIXME
  11.409 +%
  11.410 +\endisadelimFIXME
  11.411 +%
  11.412 +\isamarkupsubsection{Proof context \label{sec:context-proof}%
  11.413 +}
  11.414 +\isamarkuptrue%
  11.415 +%
  11.416 +\begin{isamarkuptext}%
  11.417 +FIXME
  11.418 +
  11.419 +\glossary{Proof context}{The static context of a structured proof,
  11.420 +acts like a local ``theory'' of the current portion of Isar proof
  11.421 +text, generalizes the idea of local hypotheses \isa{{\isasymGamma}} in
  11.422 +judgments \isa{{\isasymGamma}\ {\isasymturnstile}\ {\isasymphi}} of natural deduction calculi.  There is a
  11.423 +generic notion of introducing and discharging hypotheses.  Arbritrary
  11.424 +auxiliary context data may be adjoined.}%
  11.425 +\end{isamarkuptext}%
  11.426 +\isamarkuptrue%
  11.427 +%
  11.428 +\isadelimtheory
  11.429 +%
  11.430 +\endisadelimtheory
  11.431 +%
  11.432 +\isatagtheory
  11.433 +\isacommand{end}\isamarkupfalse%
  11.434 +%
  11.435 +\endisatagtheory
  11.436 +{\isafoldtheory}%
  11.437 +%
  11.438 +\isadelimtheory
  11.439 +%
  11.440 +\endisadelimtheory
  11.441 +\isanewline
  11.442 +\end{isabellebody}%
  11.443 +%%% Local Variables:
  11.444 +%%% mode: latex
  11.445 +%%% TeX-master: "root"
  11.446 +%%% End:
    12.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    12.2 +++ b/doc-src/IsarImplementation/Thy/document/proof.tex	Mon Jan 02 20:16:52 2006 +0100
    12.3 @@ -0,0 +1,91 @@
    12.4 +%
    12.5 +\begin{isabellebody}%
    12.6 +\def\isabellecontext{proof}%
    12.7 +%
    12.8 +\isadelimtheory
    12.9 +\isanewline
   12.10 +\isanewline
   12.11 +\isanewline
   12.12 +%
   12.13 +\endisadelimtheory
   12.14 +%
   12.15 +\isatagtheory
   12.16 +\isacommand{theory}\isamarkupfalse%
   12.17 +\ {\isachardoublequoteopen}proof{\isachardoublequoteclose}\ \isakeyword{imports}\ base\ \isakeyword{begin}%
   12.18 +\endisatagtheory
   12.19 +{\isafoldtheory}%
   12.20 +%
   12.21 +\isadelimtheory
   12.22 +%
   12.23 +\endisadelimtheory
   12.24 +%
   12.25 +\isamarkupchapter{Structured reasoning%
   12.26 +}
   12.27 +\isamarkuptrue%
   12.28 +%
   12.29 +\isamarkupsection{Proof context%
   12.30 +}
   12.31 +\isamarkuptrue%
   12.32 +%
   12.33 +\begin{isamarkuptext}%
   12.34 +FIXME%
   12.35 +\end{isamarkuptext}%
   12.36 +\isamarkuptrue%
   12.37 +%
   12.38 +\isamarkupsection{Proof state%
   12.39 +}
   12.40 +\isamarkuptrue%
   12.41 +%
   12.42 +\begin{isamarkuptext}%
   12.43 +FIXME
   12.44 +
   12.45 +\glossary{Proof state}{The whole configuration of a structured proof,
   12.46 +consisting of a \seeglossary{proof context} and an optional
   12.47 +\seeglossary{structured goal}.  Internally, an Isar proof state is
   12.48 +organized as a stack to accomodate block structure of proof texts.
   12.49 +For historical reasons, a low-level \seeglossary{tactical goal} is
   12.50 +occasionally called ``proof state'' as well.}
   12.51 +
   12.52 +\glossary{Structured goal}{FIXME}
   12.53 +
   12.54 +\glossary{Goal}{See \seeglossary{tactical goal} or \seeglossary{structured goal}. \norefpage}%
   12.55 +\end{isamarkuptext}%
   12.56 +\isamarkuptrue%
   12.57 +%
   12.58 +\isamarkupsection{Methods%
   12.59 +}
   12.60 +\isamarkuptrue%
   12.61 +%
   12.62 +\begin{isamarkuptext}%
   12.63 +FIXME%
   12.64 +\end{isamarkuptext}%
   12.65 +\isamarkuptrue%
   12.66 +%
   12.67 +\isamarkupsection{Attributes%
   12.68 +}
   12.69 +\isamarkuptrue%
   12.70 +%
   12.71 +\begin{isamarkuptext}%
   12.72 +FIXME%
   12.73 +\end{isamarkuptext}%
   12.74 +\isamarkuptrue%
   12.75 +%
   12.76 +\isadelimtheory
   12.77 +%
   12.78 +\endisadelimtheory
   12.79 +%
   12.80 +\isatagtheory
   12.81 +\isacommand{end}\isamarkupfalse%
   12.82 +%
   12.83 +\endisatagtheory
   12.84 +{\isafoldtheory}%
   12.85 +%
   12.86 +\isadelimtheory
   12.87 +%
   12.88 +\endisadelimtheory
   12.89 +\isanewline
   12.90 +\end{isabellebody}%
   12.91 +%%% Local Variables:
   12.92 +%%% mode: latex
   12.93 +%%% TeX-master: "root"
   12.94 +%%% End:
    13.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    13.2 +++ b/doc-src/IsarImplementation/Thy/document/session.tex	Mon Jan 02 20:16:52 2006 +0100
    13.3 @@ -0,0 +1,20 @@
    13.4 +\input{base.tex}
    13.5 +
    13.6 +\input{prelim.tex}
    13.7 +
    13.8 +\input{logic.tex}
    13.9 +
   13.10 +\input{tactic.tex}
   13.11 +
   13.12 +\input{proof.tex}
   13.13 +
   13.14 +\input{locale.tex}
   13.15 +
   13.16 +\input{integration.tex}
   13.17 +
   13.18 +\input{ML.tex}
   13.19 +
   13.20 +%%% Local Variables:
   13.21 +%%% mode: latex
   13.22 +%%% TeX-master: "root"
   13.23 +%%% End:
    14.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    14.2 +++ b/doc-src/IsarImplementation/Thy/document/tactic.tex	Mon Jan 02 20:16:52 2006 +0100
    14.3 @@ -0,0 +1,252 @@
    14.4 +%
    14.5 +\begin{isabellebody}%
    14.6 +\def\isabellecontext{tactic}%
    14.7 +%
    14.8 +\isadelimtheory
    14.9 +\isanewline
   14.10 +\isanewline
   14.11 +\isanewline
   14.12 +%
   14.13 +\endisadelimtheory
   14.14 +%
   14.15 +\isatagtheory
   14.16 +\isacommand{theory}\isamarkupfalse%
   14.17 +\ tactic\ \isakeyword{imports}\ base\ \isakeyword{begin}%
   14.18 +\endisatagtheory
   14.19 +{\isafoldtheory}%
   14.20 +%
   14.21 +\isadelimtheory
   14.22 +%
   14.23 +\endisadelimtheory
   14.24 +%
   14.25 +\isamarkupchapter{Tactical theorem proving%
   14.26 +}
   14.27 +\isamarkuptrue%
   14.28 +%
   14.29 +\begin{isamarkuptext}%
   14.30 +The basic idea of tactical theorem proving is to refine the
   14.31 +initial claim in a backwards fashion, until a solved form is reached.
   14.32 +An intermediate goal consists of several subgoals that need to be
   14.33 +solved in order to achieve the main statement; zero subgoals means
   14.34 +that the proof may be finished.  Goal refinement operations are called
   14.35 +tactics; combinators for composing tactics are called tacticals.%
   14.36 +\end{isamarkuptext}%
   14.37 +\isamarkuptrue%
   14.38 +%
   14.39 +\isamarkupsection{Goals \label{sec:tactical-goals}%
   14.40 +}
   14.41 +\isamarkuptrue%
   14.42 +%
   14.43 +\begin{isamarkuptext}%
   14.44 +Isabelle/Pure represents a goal\glossary{Tactical goal}{A
   14.45 +theorem of \seeglossary{Horn Clause} form stating that a number of
   14.46 +subgoals imply the main conclusion, which is marked as a protected
   14.47 +proposition.} as a theorem stating that the subgoals imply the main
   14.48 +goal: \isa{A\isactrlsub {\isadigit{1}}\ {\isasymLongrightarrow}\ {\isasymdots}\ {\isasymLongrightarrow}\ A\isactrlsub n\ {\isasymLongrightarrow}\ C}.  The outermost goal
   14.49 +structure is that of a Horn Clause\glossary{Horn Clause}{An iterated
   14.50 +implication \isa{A\isactrlsub {\isadigit{1}}\ {\isasymLongrightarrow}\ {\isasymdots}\ {\isasymLongrightarrow}\ A\isactrlsub n\ {\isasymLongrightarrow}\ C}, without any
   14.51 +outermost quantifiers.  Strictly speaking, propositions \isa{A\isactrlsub i} need to be atomic in Horn Clauses, but Isabelle admits
   14.52 +arbitrary substructure here (nested \isa{{\isasymLongrightarrow}} and \isa{{\isasymAnd}}
   14.53 +connectives).}: an iterated implication without any
   14.54 +quantifiers\footnote{Recall that outermost \isa{{\isasymAnd}x{\isachardot}\ {\isasymphi}{\isacharbrackleft}x{\isacharbrackright}} is
   14.55 +always represented via schematic variables in the body: \isa{{\isasymphi}{\isacharbrackleft}{\isacharquery}x{\isacharbrackright}}.  These may get instantiated during the course of
   14.56 +reasoning.}.  For \isa{n\ {\isacharequal}\ {\isadigit{0}}} a goal is solved.
   14.57 +
   14.58 +The structure of each subgoal \isa{A\isactrlsub i} is that of a general
   14.59 +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
   14.60 +\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
   14.61 +certain types, and \isa{H\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ H\isactrlsub m} are goal
   14.62 +hypotheses, i.e.\ facts that may be assumed locally.  Together, this
   14.63 +forms the goal context of the conclusion \isa{B} to be established.
   14.64 +The goal hypotheses may be again arbitrary Harrop Formulas, although
   14.65 +the level of nesting rarely exceeds 1--2 in practice.
   14.66 +
   14.67 +The main conclusion \isa{C} is internally marked as a protected
   14.68 +proposition\glossary{Protected proposition}{An arbitrarily structured
   14.69 +proposition \isa{C} which is forced to appear as atomic by
   14.70 +wrapping it into a propositional identity operator; notation \isa{{\isacharhash}C}.  Protecting a proposition prevents basic inferences from
   14.71 +entering into that structure for the time being.}, which is
   14.72 +occasionally represented explicitly by the notation \isa{{\isacharhash}C}.
   14.73 +This ensures that the decomposition into subgoals and main conclusion
   14.74 +is well-defined for arbitrarily structured claims.
   14.75 +
   14.76 +\medskip Basic goal management is performed via the following
   14.77 +Isabelle/Pure rules:
   14.78 +
   14.79 +  \[
   14.80 +  \infer[\isa{{\isacharparenleft}init{\isacharparenright}}]{\isa{C\ {\isasymLongrightarrow}\ {\isacharhash}C}}{} \qquad
   14.81 +  \infer[\isa{{\isacharparenleft}finish{\isacharparenright}}]{\isa{{\isacharhash}C}}{\isa{C}}
   14.82 +  \]
   14.83 +
   14.84 +  \medskip The following low-level variants admit general reasoning
   14.85 +  with protected propositions:
   14.86 +
   14.87 +  \[
   14.88 +  \infer[\isa{{\isacharparenleft}protect{\isacharparenright}}]{\isa{{\isacharhash}C}}{\isa{C}} \qquad
   14.89 +  \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}}
   14.90 +  \]%
   14.91 +\end{isamarkuptext}%
   14.92 +\isamarkuptrue%
   14.93 +%
   14.94 +\isadelimmlref
   14.95 +%
   14.96 +\endisadelimmlref
   14.97 +%
   14.98 +\isatagmlref
   14.99 +%
  14.100 +\begin{isamarkuptext}%
  14.101 +\begin{mldecls}
  14.102 +  \indexml{Goal.init}\verb|Goal.init: cterm -> thm| \\
  14.103 +  \indexml{Goal.finish}\verb|Goal.finish: thm -> thm| \\
  14.104 +  \indexml{Goal.protect}\verb|Goal.protect: thm -> thm| \\
  14.105 +  \indexml{Goal.conclude}\verb|Goal.conclude: thm -> thm| \\
  14.106 +  \end{mldecls}
  14.107 +
  14.108 +  \begin{description}
  14.109 +
  14.110 +  \item \verb|Goal.init|~\isa{{\isasymphi}} initializes a tactical goal with
  14.111 +  the type-checked proposition \isa{{\isasymphi}}.
  14.112 +
  14.113 +  \item \verb|Goal.finish|~\isa{th} checks whether theorem \isa{th} is a solved goal configuration (zero subgoals), and concludes
  14.114 +  the result by removing the goal protection.
  14.115 +
  14.116 +  \item \verb|Goal.protect|~\isa{th} protects the whole statement
  14.117 +  of theorem \isa{th}.
  14.118 +
  14.119 +  \item \verb|Goal.conclude|~\isa{th} removes the goal protection
  14.120 +  for any number of pending subgoals.
  14.121 +
  14.122 +  \end{description}%
  14.123 +\end{isamarkuptext}%
  14.124 +\isamarkuptrue%
  14.125 +%
  14.126 +\endisatagmlref
  14.127 +{\isafoldmlref}%
  14.128 +%
  14.129 +\isadelimmlref
  14.130 +%
  14.131 +\endisadelimmlref
  14.132 +%
  14.133 +\isamarkupsection{Tactics%
  14.134 +}
  14.135 +\isamarkuptrue%
  14.136 +%
  14.137 +\begin{isamarkuptext}%
  14.138 +FIXME
  14.139 +
  14.140 +\glossary{Tactic}{Any function that maps a \seeglossary{tactical goal}
  14.141 +to a lazy sequence of possible sucessors.  This scheme subsumes
  14.142 +failure (empty result sequence), as well as lazy enumeration of proof
  14.143 +search results.  Error conditions are usually mapped to an empty
  14.144 +result, which gives further tactics a chance to try in turn.
  14.145 +Commonly, tactics either take an argument to address a particular
  14.146 +subgoal, or operate on a certain range of subgoals in a uniform
  14.147 +fashion.  In any case, the main conclusion is normally left untouched,
  14.148 +apart from instantiating \seeglossary{schematic variables}.}%
  14.149 +\end{isamarkuptext}%
  14.150 +\isamarkuptrue%
  14.151 +%
  14.152 +\isamarkupsection{Tacticals%
  14.153 +}
  14.154 +\isamarkuptrue%
  14.155 +%
  14.156 +\begin{isamarkuptext}%
  14.157 +FIXME
  14.158 +
  14.159 +\glossary{Tactical}{A functional combinator for building up complex
  14.160 +tactics from simpler ones.  Typical tactical perform sequential
  14.161 +composition, disjunction (choice), iteration, or goal addressing.
  14.162 +Various search strategies may be expressed via tacticals.}%
  14.163 +\end{isamarkuptext}%
  14.164 +\isamarkuptrue%
  14.165 +%
  14.166 +\isamarkupsection{Programmed proofs%
  14.167 +}
  14.168 +\isamarkuptrue%
  14.169 +%
  14.170 +\begin{isamarkuptext}%
  14.171 +In order to perform a complete tactical proof under program control,
  14.172 +  one needs to set up an initial goal configuration, apply a tactic,
  14.173 +  and finish the result, cf.\ the rules given in
  14.174 +  \secref{sec:tactical-goals}.  Further checks are required to ensure
  14.175 +  that the result is actually an instance of the original claim --
  14.176 +  ill-behaved tactics could have destroyed that information.
  14.177 +
  14.178 +  Several simultaneous claims may be handled within a single goal
  14.179 +  statement by using meta-level conjunction internally.\footnote{This
  14.180 +  is merely syntax for certain derived statements within
  14.181 +  Isabelle/Pure, there is no need to introduce a separate conjunction
  14.182 +  operator.}  The whole configuration may be considered within a
  14.183 +  context of arbitrary-but-fixed parameters and hypotheses, which will
  14.184 +  be available as local facts during the proof and discharged into
  14.185 +  implications in the result.
  14.186 +
  14.187 +  All of these administrative tasks are packaged into a separate
  14.188 +  operation, such that the user merely needs to provide the statement
  14.189 +  and tactic to be applied.%
  14.190 +\end{isamarkuptext}%
  14.191 +\isamarkuptrue%
  14.192 +%
  14.193 +\isadelimmlref
  14.194 +%
  14.195 +\endisadelimmlref
  14.196 +%
  14.197 +\isatagmlref
  14.198 +%
  14.199 +\begin{isamarkuptext}%
  14.200 +\begin{mldecls}
  14.201 +  \indexml{Goal.prove}\verb|Goal.prove: theory -> string list -> term list -> term ->|\isasep\isanewline%
  14.202 +\verb|  (thm list -> tactic) -> thm| \\
  14.203 +  \indexml{Goal.prove-multi}\verb|Goal.prove_multi: theory -> string list -> term list -> term list ->|\isasep\isanewline%
  14.204 +\verb|  (thm list -> tactic) -> thm list| \\
  14.205 +  \end{mldecls}
  14.206 +
  14.207 +  \begin{description}
  14.208 +
  14.209 +  \item \verb|Goal.prove|~\isa{thy\ xs\ As\ C\ tac} states goal \isa{C} in the context of arbitrary-but-fixed parameters \isa{xs}
  14.210 +  and hypotheses \isa{As} and applies tactic \isa{tac} to
  14.211 +  solve it.  The latter may depend on the local assumptions being
  14.212 +  presented as facts.  The result is essentially \isa{{\isasymAnd}xs{\isachardot}\ As\ {\isasymLongrightarrow}\ C}, but is normalized by pulling \isa{{\isasymAnd}} before \isa{{\isasymLongrightarrow}}
  14.213 +  (the conclusion \isa{C} itself may be a rule statement), turning
  14.214 +  the quantifier prefix into schematic variables, and generalizing
  14.215 +  implicit type-variables.
  14.216 +
  14.217 +  Any additional fixed variables or hypotheses not being mentioned in
  14.218 +  the initial statement are left unchanged --- programmed proofs may
  14.219 +  well occur in a larger context.
  14.220 +
  14.221 +  \item \verb|Goal.prove_multi| is simular to \verb|Goal.prove|, but
  14.222 +  states several conclusions simultaneously.  \verb|Tactic.conjunction_tac| may be used to split these into individual
  14.223 +  subgoals before commencing the actual proof.
  14.224 +
  14.225 +  \end{description}%
  14.226 +\end{isamarkuptext}%
  14.227 +\isamarkuptrue%
  14.228 +%
  14.229 +\endisatagmlref
  14.230 +{\isafoldmlref}%
  14.231 +%
  14.232 +\isadelimmlref
  14.233 +%
  14.234 +\endisadelimmlref
  14.235 +%
  14.236 +\isadelimtheory
  14.237 +%
  14.238 +\endisadelimtheory
  14.239 +%
  14.240 +\isatagtheory
  14.241 +\isacommand{end}\isamarkupfalse%
  14.242 +%
  14.243 +\endisatagtheory
  14.244 +{\isafoldtheory}%
  14.245 +%
  14.246 +\isadelimtheory
  14.247 +%
  14.248 +\endisadelimtheory
  14.249 +\isanewline
  14.250 +\isanewline
  14.251 +\end{isabellebody}%
  14.252 +%%% Local Variables:
  14.253 +%%% mode: latex
  14.254 +%%% TeX-master: "root"
  14.255 +%%% End:
    15.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    15.2 +++ b/doc-src/IsarImplementation/Thy/integration.thy	Mon Jan 02 20:16:52 2006 +0100
    15.3 @@ -0,0 +1,439 @@
    15.4 +
    15.5 +(* $Id$ *)
    15.6 +
    15.7 +theory integration imports base begin
    15.8 +
    15.9 +chapter {* System integration *}
   15.10 +
   15.11 +section {* Isar toplevel *}
   15.12 +
   15.13 +text {* The Isar toplevel may be considered the centeral hub of the
   15.14 +  Isabelle/Isar system, where all key components and sub-systems are
   15.15 +  integrated into a single read-eval-print loop of Isar commands.
   15.16 +  Here we even incorporate the existing {\ML} toplevel of the compiler
   15.17 +  and run-time system (cf.\ \secref{sec:ML-toplevel}).
   15.18 +
   15.19 +  Isabelle/Isar departs from original ``LCF system architecture''
   15.20 +  where {\ML} was really The Meta Language for defining theories and
   15.21 +  conducting proofs.  Instead, {\ML} merely serves as the
   15.22 +  implementation language for the system (and user extensions), while
   15.23 +  our specific Isar toplevel supports particular notions of
   15.24 +  incremental theory and proof development more directly.  This
   15.25 +  includes the graph structure of theories and the block structure of
   15.26 +  proofs, support for unlimited undo, facilities for tracing,
   15.27 +  debugging, timing, profiling.
   15.28 +
   15.29 +  \medskip The toplevel maintains an implicit state, which is
   15.30 +  transformed by a sequence of transitions -- either interactively or
   15.31 +  in batch-mode.  In interactive mode, Isar state transitions are
   15.32 +  encapsulated as safe transactions, such that both failure and undo
   15.33 +  are handled conveniently without destroying the underlying draft
   15.34 +  theory (cf.~\secref{sec:context-theory}).  In batch mode,
   15.35 +  transitions operate in a strictly linear (destructive) fashion, such
   15.36 +  that error conditions abort the present attempt to construct a
   15.37 +  theory altogether.
   15.38 +
   15.39 +  The toplevel state is a disjoint sum of empty @{text toplevel}, or
   15.40 +  @{text theory}, or @{text proof}.  On entering the main Isar loop we
   15.41 +  start with an empty toplevel.  A theory is commenced by giving a
   15.42 +  @{text \<THEORY>} header; within a theory we may issue theory
   15.43 +  commands such as @{text \<CONSTS>} or @{text \<DEFS>}, or state a
   15.44 +  @{text \<THEOREM>} to be proven.  Now we are within a proof state,
   15.45 +  with a rich collection of Isar proof commands for structured proof
   15.46 +  composition, or unstructured proof scripts.  When the proof is
   15.47 +  concluded we get back to the theory, which is then updated by
   15.48 +  storing the resulting fact.  Further theory declarations or theorem
   15.49 +  statements with proofs may follow, until we eventually conclude the
   15.50 +  theory development by issuing @{text \<END>}.  The resulting theory
   15.51 +  is then stored within the theory database and we are back to the
   15.52 +  empty toplevel.
   15.53 +
   15.54 +  In addition to these proper state transformations, there are also
   15.55 +  some diagnostic commands for peeking at the toplevel state without
   15.56 +  modifying it (e.g.\ \isakeyword{thm}, \isakeyword{term},
   15.57 +  \isakeyword{print-cases}).
   15.58 +*}
   15.59 +
   15.60 +text %mlref {*
   15.61 +  \begin{mldecls}
   15.62 +  @{index_ML_type Toplevel.state} \\
   15.63 +  @{index_ML Toplevel.UNDEF: "exn"} \\
   15.64 +  @{index_ML Toplevel.is_toplevel: "Toplevel.state -> bool"} \\
   15.65 +  @{index_ML Toplevel.theory_of: "Toplevel.state -> theory"} \\
   15.66 +  @{index_ML Toplevel.proof_of: "Toplevel.state -> Proof.state"} \\
   15.67 +  @{index_ML Toplevel.debug: "bool ref"} \\
   15.68 +  @{index_ML Toplevel.timing: "bool ref"} \\
   15.69 +  @{index_ML Toplevel.profiling: "int ref"} \\
   15.70 +  \end{mldecls}
   15.71 +
   15.72 +  \begin{description}
   15.73 +
   15.74 +  \item @{ML_type Toplevel.state} represents Isar toplevel states,
   15.75 +  which are normally only manipulated through the toplevel transition
   15.76 +  concept (\secref{sec:toplevel-transition}).  Also note that a
   15.77 +  toplevel state is subject to the same linerarity restrictions as a
   15.78 +  theory context (cf.~\secref{sec:context-theory}).
   15.79 +
   15.80 +  \item @{ML Toplevel.UNDEF} is raised for undefined toplevel
   15.81 +  operations: @{ML_type Toplevel.state} is a sum type, many operations
   15.82 +  work only partially for certain cases.
   15.83 +
   15.84 +  \item @{ML Toplevel.is_toplevel} checks for an empty toplevel state.
   15.85 +
   15.86 +  \item @{ML Toplevel.theory_of} gets the theory of a theory or proof
   15.87 +  (!), otherwise raises @{ML Toplevel.UNDEF}.
   15.88 +
   15.89 +  \item @{ML Toplevel.proof_of} gets the Isar proof state if
   15.90 +  available, otherwise raises @{ML Toplevel.UNDEF}.
   15.91 +
   15.92 +  \item @{ML "set Toplevel.debug"} makes the toplevel print further
   15.93 +  details about internal error conditions, exceptions being raised
   15.94 +  etc.
   15.95 +
   15.96 +  \item @{ML "set Toplevel.timing"} makes the toplevel print timing
   15.97 +  information for each Isar command being executed.
   15.98 +
   15.99 +  \item @{ML Toplevel.profiling} controls low-level profiling of the
  15.100 +  underlying {\ML} runtime system.\footnote{For Poly/ML, 1 means time
  15.101 +  and 2 space profiling.}
  15.102 +
  15.103 +  \end{description}
  15.104 +*}
  15.105 +
  15.106 +
  15.107 +subsection {* Toplevel transitions *}
  15.108 +
  15.109 +text {* An Isar toplevel transition consists of a partial
  15.110 +  function on the toplevel state, with additional information for
  15.111 +  diagnostics and error reporting: there are fields for command name,
  15.112 +  source position, optional source text, as well as flags for
  15.113 +  interactive-only commands (which issue a warning in batch-mode),
  15.114 +  printing of result state, etc.
  15.115 +
  15.116 +  The operational part is represented as a sequential union of a list
  15.117 +  of partial functions, which are tried in turn until the first one
  15.118 +  succeeds (i.e.\ does not raise @{ML Toplevel.UNDEF}).  For example,
  15.119 +  a single Isar command like \isacommand{qed} consists of the union of
  15.120 +  some function @{ML_type "Proof.state -> Proof.state"} for proofs
  15.121 +  within proofs, plus @{ML_type "Proof.state -> theory"} for proofs at
  15.122 +  the outer theory level.
  15.123 +
  15.124 +  Toplevel transitions are composed via transition transformers.
  15.125 +  Internally, Isar commands are put together from an empty transition
  15.126 +  extended by name and source position (and optional source text).  It
  15.127 +  is then left to the individual command parser to turn the given
  15.128 +  syntax body into a suitable transition transformer that adjoin
  15.129 +  actual operations on a theory or proof state etc.
  15.130 +*}
  15.131 +
  15.132 +text %mlref {*
  15.133 +  \begin{mldecls}
  15.134 +  @{index_ML Toplevel.print: "Toplevel.transition -> Toplevel.transition"} \\
  15.135 +  @{index_ML Toplevel.no_timing: "Toplevel.transition -> Toplevel.transition"} \\
  15.136 +  @{index_ML Toplevel.keep: "(Toplevel.state -> unit) ->
  15.137 +  Toplevel.transition -> Toplevel.transition"} \\
  15.138 +  @{index_ML Toplevel.theory: "(theory -> theory) ->
  15.139 +  Toplevel.transition -> Toplevel.transition"} \\
  15.140 +  @{index_ML Toplevel.theory_to_proof: "(theory -> Proof.state) ->
  15.141 +  Toplevel.transition -> Toplevel.transition"} \\
  15.142 +  @{index_ML Toplevel.proof: "(Proof.state -> Proof.state) ->
  15.143 +  Toplevel.transition -> Toplevel.transition"} \\
  15.144 +  @{index_ML Toplevel.proofs: "(Proof.state -> Proof.state Seq.seq) ->
  15.145 +  Toplevel.transition -> Toplevel.transition"} \\
  15.146 +  @{index_ML Toplevel.proof_to_theory: "(Proof.state -> theory) ->
  15.147 +  Toplevel.transition -> Toplevel.transition"} \\
  15.148 +  \end{mldecls}
  15.149 +
  15.150 +  \begin{description}
  15.151 +
  15.152 +  \item @{ML Toplevel.print} sets the print flag, which causes the
  15.153 +  resulting state of the transition to be echoed in interactive mode.
  15.154 +
  15.155 +  \item @{ML Toplevel.no_timing} indicates that the transition should
  15.156 +  never show timing information, e.g.\ because it is merely a
  15.157 +  diagnostic command.
  15.158 +
  15.159 +  \item @{ML Toplevel.keep} adjoins a diagnostic function.
  15.160 +
  15.161 +  \item @{ML Toplevel.theory} adjoins a theory transformer.
  15.162 +
  15.163 +  \item @{ML Toplevel.theory_to_proof} adjoins a global goal function,
  15.164 +  which turns a theory into a proof state.  The theory must not be
  15.165 +  changed here!  The generic Isar goal setup includes an argument that
  15.166 +  specifies how to apply the proven result to the theory, when the
  15.167 +  proof is finished.
  15.168 +
  15.169 +  \item @{ML Toplevel.proof} adjoins a deterministic proof command,
  15.170 +  with a singleton result state.
  15.171 +
  15.172 +  \item @{ML Toplevel.proofs} adjoins a general proof command, with
  15.173 +  zero or more result states (represented as a lazy list).
  15.174 +
  15.175 +  \item @{ML Toplevel.proof_to_theory} adjoins a concluding proof
  15.176 +  command, that returns the resulting theory, after storing the
  15.177 +  resulting facts etc.
  15.178 +
  15.179 +  \end{description}
  15.180 +*}
  15.181 +
  15.182 +
  15.183 +subsection {* Toplevel control *}
  15.184 +
  15.185 +text {* Apart from regular toplevel transactions there are a few
  15.186 +  special control commands that modify the behavior the toplevel
  15.187 +  itself, and only make sense in interactive mode.  Under normal
  15.188 +  circumstances, the user encounters these only implicitly as part of
  15.189 +  the protocol between the Isabelle/Isar system and a user-interface
  15.190 +  such as ProofGeneral.
  15.191 +
  15.192 +  \begin{description}
  15.193 +
  15.194 +  \item \isacommand{undo} follows the three-level hierarchy of empty
  15.195 +  toplevel vs.\ theory vs.\ proof: undo within a proof reverts to the
  15.196 +  previous proof context, undo after a proof reverts to the theory
  15.197 +  before the initial goal statement, undo of a theory command reverts
  15.198 +  to the previous theory value, undo of a theory header discontinues
  15.199 +  the current theory development and removes it from the theory
  15.200 +  database (\secref{sec:theory-database}).
  15.201 +
  15.202 +  \item \isacommand{kill} aborts the current level of development:
  15.203 +  kill in a proof context reverts to the theory before the initial
  15.204 +  goal statement, kill in a theory context aborts the current theory
  15.205 +  development, removing it from the database.
  15.206 +
  15.207 +  \item \isacommand{exit} drops out of the Isar toplevel into the
  15.208 +  underlying {\ML} toplevel (\secref{sec:ML-toplevel}).  The Isar
  15.209 +  toplevel state is preserved and may be continued later.
  15.210 +
  15.211 +  \item \isacommand{quit} terminates the Isabelle/Isar process without
  15.212 +  saving.
  15.213 +
  15.214 +  \end{description}
  15.215 +*}
  15.216 +
  15.217 +
  15.218 +section {* ML toplevel \label{sec:ML-toplevel} *}
  15.219 +
  15.220 +text {* The {\ML} toplevel provides a read-compile-eval-print loop for
  15.221 +  {\ML} values, types, structures, and functors.  {\ML} declarations
  15.222 +  operate on the global system state, which consists of the compiler
  15.223 +  environment plus the values of {\ML} reference variables.  There is
  15.224 +  no clean way to undo {\ML} declarations, except for reverting to a
  15.225 +  previously saved state of the whole Isabelle process.  {\ML} input
  15.226 +  is either read interactively from a TTY, or from a string (usually
  15.227 +  within a theory text), or from a source file (usually associated
  15.228 +  with a theory).
  15.229 +
  15.230 +  Whenever the {\ML} toplevel is active, the current Isabelle theory
  15.231 +  context is passed as an internal reference variable.  Thus {\ML}
  15.232 +  code may access the theory context during compilation, it may even
  15.233 +  change the value of a theory being under construction --- following
  15.234 +  the usual linearity restrictions (cf.~\secref{sec:context-theory}).
  15.235 +*}
  15.236 +
  15.237 +text %mlref {*
  15.238 +  \begin{mldecls}
  15.239 +  @{index_ML context: "theory -> unit"} \\
  15.240 +  @{index_ML the_context: "unit -> theory"} \\
  15.241 +  @{index_ML "Context.>> ": "(theory -> theory) -> unit"} \\
  15.242 +  \end{mldecls}
  15.243 +
  15.244 +  \begin{description}
  15.245 +
  15.246 +  \item @{ML context}~@{text thy} sets the {\ML} theory context to
  15.247 +  @{text thy}.  This is usually performed automatically by the system,
  15.248 +  when dropping out of the interactive Isar toplevel into {\ML}, or
  15.249 +  when Isar invokes {\ML} to process code from a string or a file.
  15.250 +
  15.251 +  \item @{ML "the_context ()"} refers to the theory context of the
  15.252 +  {\ML} toplevel --- at compile time!  {\ML} code needs to take care
  15.253 +  to refer to @{ML "the_context ()"} correctly, recall that evaluation
  15.254 +  of a function body is delayed until actual runtime.  Moreover,
  15.255 +  persistent {\ML} toplevel bindings to an unfinished theory should be
  15.256 +  avoided: code should either project out the desired information
  15.257 +  immediately, or produce an explicit @{ML_type theory_ref} (cf.\
  15.258 +  \secref{sec:context-theory}).
  15.259 +
  15.260 +  \item @{ML "Context.>>"}~@{text f} applies theory transformation
  15.261 +  @{text f} to the current theory of the {\ML} toplevel.  In order to
  15.262 +  work as expected, the theory should be still under construction, and
  15.263 +  the Isar language element that invoked the {\ML} compiler in the
  15.264 +  first place shoule be ready to accept the changed theory value
  15.265 +  (e.g.\ \isakeyword{ML-setup}, but not plain \isakeyword{ML}).
  15.266 +  Otherwise the theory may get destroyed!
  15.267 +
  15.268 +  \end{description}
  15.269 +
  15.270 +  It is very important to note that the above functions are really
  15.271 +  restricted to the compile time, even though the {\ML} compiler is
  15.272 +  invoked at runtime!  The majority of {\ML} code uses explicit
  15.273 +  functional arguments of a theory or proof context, as required.
  15.274 +  Thus it may get run in an arbitrary context later on.
  15.275 +
  15.276 +  \bigskip
  15.277 +
  15.278 +  \begin{mldecls}
  15.279 +  @{index_ML Isar.main: "unit -> unit"} \\
  15.280 +  @{index_ML Isar.loop: "unit -> unit"} \\
  15.281 +  @{index_ML Isar.state: "unit -> Toplevel.state"} \\
  15.282 +  @{index_ML Isar.exn: "unit -> (exn * string) option"} \\
  15.283 +  \end{mldecls}
  15.284 +
  15.285 +  \begin{description}
  15.286 +
  15.287 +  \item @{ML "Isar.main ()"} invokes the Isar toplevel from {\ML},
  15.288 +  initializing the state to empty toplevel state.
  15.289 +
  15.290 +  \item @{ML "Isar.loop ()"} continues the Isar toplevel with the
  15.291 +  current state, after dropping out of the Isar toplevel loop.
  15.292 +
  15.293 +  \item @{ML "Isar.state ()"} and @{ML "Isar.exn ()"} get current
  15.294 +  toplevel state and optional error condition, respectively.  This
  15.295 +  only works after dropping out of the Isar toplevel loop.
  15.296 +
  15.297 +  \end{description}
  15.298 +*}
  15.299 +
  15.300 +
  15.301 +section {* Theory database *}
  15.302 +
  15.303 +text {* The theory database maintains a collection of theories,
  15.304 +  together with some administrative information about the original
  15.305 +  sources, which are held in an external store (i.e.\ a collection of
  15.306 +  directories within the regular file system of the underlying
  15.307 +  platform).
  15.308 +
  15.309 +  The theory database is organized as a directed acyclic graph, with
  15.310 +  entries referenced by theory name.  Although some external
  15.311 +  interfaces allow to include a directory specification, this is only
  15.312 +  a hint to the underlying theory loader mechanism: the internal
  15.313 +  theory name space is flat.
  15.314 +
  15.315 +  Theory @{text A} is associated with the main theory file @{text
  15.316 +  A}\verb,.thy,, which needs to be accessible through the theory
  15.317 +  loader path.  A number of optional {\ML} source files may be
  15.318 +  associated with each theory, by declaring these dependencies in the
  15.319 +  theory header as @{text \<USES>}, and loading them consecutively
  15.320 +  within the theory context.  The system keeps track of incoming {\ML}
  15.321 +  sources and associates them with the current theory.  The special
  15.322 +  theory {\ML} file @{text A}\verb,.ML, is loaded after a theory has
  15.323 +  been concluded, in order to support legacy proof {\ML} proof
  15.324 +  scripts.
  15.325 +
  15.326 +  The basic internal actions of the theory database are @{text
  15.327 +  "update"}\indexbold{@{text "update"} theory}, @{text
  15.328 +  "outdate"}\indexbold{@{text "outdate"} theory}, and @{text
  15.329 +  "remove"}\indexbold{@{text "remove"} theory}:
  15.330 +
  15.331 +  \begin{itemize}
  15.332 +
  15.333 +  \item @{text "update A"} introduces a link of @{text "A"} with a
  15.334 +  @{text "theory"} value of the same name; it asserts that the theory
  15.335 +  sources are consistent with that value.
  15.336 +
  15.337 +  \item @{text "outdate A"} invalidates the link of a theory database
  15.338 +  entry to its sources, but retains the present theory value.
  15.339 +
  15.340 +  \item @{text "remove A"} removes entry @{text "A"} from the theory
  15.341 +  database.
  15.342 +  
  15.343 +  \end{itemize}
  15.344 +
  15.345 +  These actions are propagated to sub- or super-graphs of a theory
  15.346 +  entry in the usual way, in order to preserve global consistency of
  15.347 +  the state of all loaded theories with the sources of the external
  15.348 +  store.  This implies causal dependencies of certain actions: @{text
  15.349 +  "update"} or @{text "outdate"} of an entry will @{text "outdate"}
  15.350 +  all descendants; @{text "remove"} will @{text "remove"} all
  15.351 +  descendants.
  15.352 +
  15.353 +  \medskip There are separate user-level interfaces to operate on the
  15.354 +  theory database directly or indirectly.  The primitive actions then
  15.355 +  just happen automatically while working with the system.  In
  15.356 +  particular, processing a theory header @{text "\<THEORY> A
  15.357 +  \<IMPORTS> B\<^sub>1 \<dots> B\<^sub>n \<BEGIN>"} ensure that the
  15.358 +  sub-graph of the collective imports @{text "B\<^sub>1 \<dots> B\<^sub>n"}
  15.359 +  is up-to-date.  Earlier theories are reloaded as required, with
  15.360 +  @{text update} actions proceeding in topological order according to
  15.361 +  theory dependencies.  There may be also a wave of implied @{text
  15.362 +  outdate} actions for derived theory nodes until a stable situation
  15.363 +  is achieved eventually.
  15.364 +*}
  15.365 +
  15.366 +text %mlref {*
  15.367 +  \begin{mldecls}
  15.368 +  @{index_ML theory: "string -> theory"} \\
  15.369 +  @{index_ML use_thy: "string -> unit"} \\
  15.370 +  @{index_ML update_thy: "string -> unit"} \\
  15.371 +  @{index_ML use_thy_only: "string -> unit"} \\
  15.372 +  @{index_ML update_thy_only: "string -> unit"} \\
  15.373 +  @{index_ML touch_thy: "string -> unit"} \\
  15.374 +  @{index_ML remove_thy: "string -> unit"} \\[1ex]
  15.375 +  @{index_ML ThyInfo.begin_theory}@{verbatim ": ... -> bool -> theory"} \\
  15.376 +  @{index_ML ThyInfo.end_theory: "theory -> theory"} \\
  15.377 +  @{index_ML ThyInfo.register_theory: "theory -> unit"} \\[1ex]
  15.378 +  @{verbatim "datatype action = Update | Outdate | Remove"} \\
  15.379 +  @{index_ML ThyInfo.add_hook: "(ThyInfo.action -> string -> unit) -> unit"} \\
  15.380 +  \end{mldecls}
  15.381 +
  15.382 +  \begin{description}
  15.383 +
  15.384 +  \item @{ML theory}~@{text A} retrieves the theory value presently
  15.385 +  associated with @{text A}.  The result is not necessarily
  15.386 +  up-to-date!
  15.387 +
  15.388 +  \item @{ML use_thy}~@{text A} loads theory @{text A} if it is absent
  15.389 +  or out-of-date.  It ensures that all parent theories are available
  15.390 +  as well, but does not reload them if older versions are already
  15.391 +  present.
  15.392 +
  15.393 +  \item @{ML update_thy} is similar to @{ML use_thy}, but ensures that
  15.394 +  the @{text A} and all of its ancestors are fully up-to-date.
  15.395 +
  15.396 +  \item @{ML use_thy_only}~@{text A} is like @{ML use_thy}~@{text A},
  15.397 +  but refrains from loading the attached @{text A}\verb,.ML, file.
  15.398 +  This is occasionally useful in replaying legacy {\ML} proof scripts
  15.399 +  by hand.
  15.400 +  
  15.401 +  \item @{ML update_thy_only} is analogous to @{ML use_thy_only}, but
  15.402 +  proceeds like @{ML update_thy} for ancestors.
  15.403 +
  15.404 +  \item @{ML touch_thy}~@{text A} performs @{text outdate} action on
  15.405 +  theory @{text A} and all of its descendants.
  15.406 +
  15.407 +  \item @{ML remove_thy}~@{text A} removes @{text A} and all of its
  15.408 +  descendants from the theory database.
  15.409 +
  15.410 +  \item @{ML ThyInfo.begin_theory} is the basic operation behind a
  15.411 +  @{text \<THEORY>} header declaration.  The boolean argument
  15.412 +  indicates the strictness of treating ancestors: for @{ML true} (as
  15.413 +  in interactive mode) like @{ML update_thy}, and for @{ML false} (as
  15.414 +  in batch mode) like @{ML use_thy}.  This is {\ML} functions is
  15.415 +  normally not invoked directly.
  15.416 +
  15.417 +  \item @{ML ThyInfo.end_theory} concludes the loading of a theory
  15.418 +  proper; an attached theory {\ML} file may be still loaded later on.
  15.419 +  This is {\ML} functions is normally not invoked directly.
  15.420 +
  15.421 +  \item @{ML ThyInfo.register_theory}~{text thy} registers an existing
  15.422 +  theory value with the theory loader database.  There is no
  15.423 +  management of associated sources; this is mainly for bootstrapping.
  15.424 +
  15.425 +  \item @{ML "ThyInfo.add_hook"}~@{text f} registers function @{text
  15.426 +  f} as a hook for theory database actions.  The function will be
  15.427 +  invoked with the action and theory name being involved; thus derived
  15.428 +  actions may be performed in associated system components, e.g.\
  15.429 +  maintaining the state of an editor for theory sources.
  15.430 +
  15.431 +  The kind and order of actions occurring in practice depends both on
  15.432 +  user interactions and the internal process of resolving theory
  15.433 +  imports.  Hooks should not rely on a particular policy here!  Any
  15.434 +  exceptions raised by the hook are ignored by the theory database.
  15.435 +
  15.436 +  \end{description}
  15.437 +*}
  15.438 +
  15.439 +
  15.440 +(* FIXME section {* Sessions and document preparation *} *)
  15.441 +
  15.442 +end
    16.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    16.2 +++ b/doc-src/IsarImplementation/Thy/locale.thy	Mon Jan 02 20:16:52 2006 +0100
    16.3 @@ -0,0 +1,16 @@
    16.4 +
    16.5 +(* $Id$ *)
    16.6 +
    16.7 +theory "locale" imports base begin
    16.8 +
    16.9 +chapter {* Structured specifications *}
   16.10 +
   16.11 +section {* Specification elements *}
   16.12 +
   16.13 +text FIXME
   16.14 +
   16.15 +section {* Locales *}
   16.16 +
   16.17 +text FIXME
   16.18 +
   16.19 +end
    17.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    17.2 +++ b/doc-src/IsarImplementation/Thy/logic.thy	Mon Jan 02 20:16:52 2006 +0100
    17.3 @@ -0,0 +1,139 @@
    17.4 +
    17.5 +(* $Id$ *)
    17.6 +
    17.7 +theory logic imports base begin
    17.8 +
    17.9 +chapter {* Pure logic *}
   17.10 +
   17.11 +section {* Syntax *}
   17.12 +
   17.13 +subsection {* Simply-typed lambda calculus *}
   17.14 +
   17.15 +text {*
   17.16 +
   17.17 +FIXME
   17.18 +
   17.19 +\glossary{Type}{FIXME}
   17.20 +\glossary{Term}{FIXME}
   17.21 +
   17.22 +*}
   17.23 +
   17.24 +subsection {* The order-sorted algebra of types *}
   17.25 +
   17.26 +text {*
   17.27 +
   17.28 +FIXME
   17.29 +
   17.30 +\glossary{Type constructor}{FIXME}
   17.31 +
   17.32 +\glossary{Type class}{FIXME}
   17.33 +
   17.34 +\glossary{Type arity}{FIXME}
   17.35 +
   17.36 +\glossary{Sort}{FIXME}
   17.37 +
   17.38 +*}
   17.39 +
   17.40 +
   17.41 +subsection {* Type-inference and schematic polymorphism *}
   17.42 +
   17.43 +text {*
   17.44 +
   17.45 +FIXME
   17.46 +
   17.47 +\glossary{Schematic polymorphism}{FIXME}
   17.48 +
   17.49 +\glossary{Type variable}{FIXME}
   17.50 +
   17.51 +*}
   17.52 +
   17.53 +
   17.54 +section {* Theory *}
   17.55 +
   17.56 +text {*
   17.57 +
   17.58 +FIXME
   17.59 +
   17.60 +\glossary{Constant}{Essentially a \seeglossary{fixed variable} of the
   17.61 +theory context, but slightly more flexible since it may be used at
   17.62 +different type-instances, due to \seeglossary{schematic
   17.63 +polymorphism.}}
   17.64 +
   17.65 +*}
   17.66 +
   17.67 +
   17.68 +section {* Deduction *}
   17.69 +
   17.70 +text {*
   17.71 +
   17.72 +  FIXME
   17.73 +
   17.74 +\glossary{Proposition}{A \seeglossary{term} of \seeglossary{type}
   17.75 +@{text "prop"}.  Internally, there is nothing special about
   17.76 +propositions apart from their type, but the concrete syntax enforces a
   17.77 +clear distinction.  Propositions are structured via implication @{text
   17.78 +"A \<Longrightarrow> B"} or universal quantification @{text "\<And>x. B x"} --- anything
   17.79 +else is considered atomic.  The canonical form for propositions is
   17.80 +that of a \seeglossary{Hereditary Harrop Formula}.}
   17.81 +
   17.82 +\glossary{Theorem}{A proven proposition within a certain theory and
   17.83 +proof context, formally @{text "\<Gamma> \<turnstile>\<^sub>\<Theta> \<phi>"}; both contexts are
   17.84 +rarely spelled out explicitly.  Theorems are usually normalized
   17.85 +according to the \seeglossary{HHF} format.}
   17.86 +
   17.87 +\glossary{Fact}{Sometimes used interchangably for
   17.88 +\seeglossary{theorem}.  Strictly speaking, a list of theorems,
   17.89 +essentially an extra-logical conjunction.  Facts emerge either as
   17.90 +local assumptions, or as results of local goal statements --- both may
   17.91 +be simultaneous, hence the list representation.}
   17.92 +
   17.93 +\glossary{Schematic variable}{FIXME}
   17.94 +
   17.95 +\glossary{Fixed variable}{A variable that is bound within a certain
   17.96 +proof context; an arbitrary-but-fixed entity within a portion of proof
   17.97 +text.}
   17.98 +
   17.99 +\glossary{Free variable}{Synonymous for \seeglossary{fixed variable}.}
  17.100 +
  17.101 +\glossary{Bound variable}{FIXME}
  17.102 +
  17.103 +\glossary{Variable}{See \seeglossary{schematic variable},
  17.104 +\seeglossary{fixed variable}, \seeglossary{bound variable}, or
  17.105 +\seeglossary{type variable}.  The distinguishing feature of different
  17.106 +variables is their binding scope.}
  17.107 +
  17.108 +*}
  17.109 +
  17.110 +subsection {* Primitive inferences *}
  17.111 +
  17.112 +text FIXME
  17.113 +
  17.114 +subsection {* Higher-order resolution *}
  17.115 +
  17.116 +text {*
  17.117 +
  17.118 +FIXME
  17.119 +
  17.120 +\glossary{Hereditary Harrop Formula}{The set of propositions in HHF
  17.121 +format is defined inductively as @{text "H = (\<And>x\<^sup>*. H\<^sup>* \<Longrightarrow>
  17.122 +A)"}, for variables @{text "x"} and atomic propositions @{text "A"}.
  17.123 +Any proposition may be put into HHF form by normalizing with the rule
  17.124 +@{text "(A \<Longrightarrow> (\<And>x. B x)) \<equiv> (\<And>x. A \<Longrightarrow> B x)"}.  In Isabelle, the outermost
  17.125 +quantifier prefix is represented via \seeglossary{schematic
  17.126 +variables}, such that the top-level structure is merely that of a
  17.127 +\seeglossary{Horn Clause}}.
  17.128 +
  17.129 +\glossary{HHF}{See \seeglossary{Hereditary Harrop Formula}.}
  17.130 +
  17.131 +*}
  17.132 +
  17.133 +subsection {* Equational reasoning *}
  17.134 +
  17.135 +text FIXME
  17.136 +
  17.137 +
  17.138 +section {* Proof terms *}
  17.139 +
  17.140 +text FIXME
  17.141 +
  17.142 +end
    18.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    18.2 +++ b/doc-src/IsarImplementation/Thy/prelim.thy	Mon Jan 02 20:16:52 2006 +0100
    18.3 @@ -0,0 +1,328 @@
    18.4 +
    18.5 +(* $Id$ *)
    18.6 +
    18.7 +theory prelim imports base begin
    18.8 +
    18.9 +chapter {* Preliminaries *}
   18.10 +
   18.11 +section {* Named entities *}
   18.12 +
   18.13 +text {* Named entities of different kinds (logical constant, type,
   18.14 +type class, theorem, method etc.) live in separate name spaces.  It is
   18.15 +usually clear from the occurrence of a name which kind of entity it
   18.16 +refers to.  For example, proof method @{text "foo"} vs.\ theorem
   18.17 +@{text "foo"} vs.\ logical constant @{text "foo"} are easily
   18.18 +distinguished by means of the syntactic context.  A notable exception
   18.19 +are logical identifiers within a term (\secref{sec:terms}): constants,
   18.20 +fixed variables, and bound variables all share the same identifier
   18.21 +syntax, but are distinguished by their scope.
   18.22 +
   18.23 +Each name space is organized as a collection of \emph{qualified
   18.24 +names}, which consist of a sequence of basic name components separated
   18.25 +by dots: @{text "Bar.bar.foo"}, @{text "Bar.foo"}, and @{text "foo"}
   18.26 +are examples for valid qualified names.  Name components are
   18.27 +subdivided into \emph{symbols}, which constitute the smallest textual
   18.28 +unit in Isabelle --- raw characters are normally not encountered
   18.29 +directly. *}
   18.30 +
   18.31 +
   18.32 +subsection {* Strings of symbols *}
   18.33 +
   18.34 +text {* Isabelle strings consist of a sequence of
   18.35 +symbols\glossary{Symbol}{The smalles unit of text in Isabelle,
   18.36 +subsumes plain ASCII characters as well as an infinite collection of
   18.37 +named symbols (for greek, math etc.).}, which are either packed as an
   18.38 +actual @{text "string"}, or represented as a list.  Each symbol is in
   18.39 +itself a small string of the following form:
   18.40 +
   18.41 +\begin{enumerate}
   18.42 +
   18.43 +\item either a singleton ASCII character ``@{text "c"}'' (with
   18.44 +character code 0--127), for example ``\verb,a,'',
   18.45 +
   18.46 +\item or a regular symbol ``\verb,\,\verb,<,@{text "ident"}\verb,>,'',
   18.47 +for example ``\verb,\,\verb,<alpha>,'',
   18.48 +
   18.49 +\item or a control symbol ``\verb,\,\verb,<^,@{text
   18.50 +"ident"}\verb,>,'', for example ``\verb,\,\verb,<^bold>,'',
   18.51 +
   18.52 +\item or a raw control symbol ``\verb,\,\verb,<^raw:,@{text
   18.53 +"\<dots>"}\verb,>,'' where ``@{text "\<dots>"}'' refers to any printable ASCII
   18.54 +character (excluding ``\verb,>,'') or non-ASCII character, for example
   18.55 +``\verb,\,\verb,<^raw:$\sum_{i = 1}^n$>,'',
   18.56 +
   18.57 +\item or a numbered raw control symbol ``\verb,\,\verb,<^raw,@{text
   18.58 +"nnn"}\verb,>, where @{text "nnn"} are digits, for example
   18.59 +``\verb,\,\verb,<^raw42>,''.
   18.60 +
   18.61 +\end{enumerate}
   18.62 +
   18.63 +The @{text "ident"} syntax for symbol names is @{text "letter (letter
   18.64 +| digit)\<^sup>*"}, where @{text "letter = A..Za..Z"} and @{text
   18.65 +"digit = 0..9"}.  There are infinitely many regular symbols and
   18.66 +control symbols available, but a certain collection of standard
   18.67 +symbols is treated specifically.  For example,
   18.68 +``\verb,\,\verb,<alpha>,'' is classified as a (non-ASCII) letter,
   18.69 +which means it may occur within regular Isabelle identifier syntax.
   18.70 +
   18.71 +Output of symbols depends on the print mode (\secref{sec:print-mode}).
   18.72 +For example, the standard {\LaTeX} setup of the Isabelle document
   18.73 +preparation system would present ``\verb,\,\verb,<alpha>,'' as @{text
   18.74 +"\<alpha>"}, and ``\verb,\,\verb,<^bold>,\verb,\,\verb,<alpha>,'' as @{text
   18.75 +"\<^bold>\<alpha>"}.
   18.76 +
   18.77 +\medskip It is important to note that the character set underlying
   18.78 +Isabelle symbols is plain 7-bit ASCII.  Since 8-bit characters are
   18.79 +passed through transparently, Isabelle may easily process actual
   18.80 +Unicode/UCS data (using the well-known UTF-8 encoding, for example).
   18.81 +Unicode provides its own collection of mathematical symbols, but there
   18.82 +is presently no link to Isabelle's named ones; both kinds of symbols
   18.83 +coexist independently. *}
   18.84 +
   18.85 +text %mlref {*
   18.86 +  \begin{mldecls}
   18.87 +  @{index_ML_type "Symbol.symbol"} \\
   18.88 +  @{index_ML Symbol.explode: "string -> Symbol.symbol list"} \\
   18.89 +  @{index_ML Symbol.is_letter: "Symbol.symbol -> bool"} \\
   18.90 +  @{index_ML Symbol.is_digit: "Symbol.symbol -> bool"} \\
   18.91 +  @{index_ML Symbol.is_quasi: "Symbol.symbol -> bool"} \\
   18.92 +  @{index_ML Symbol.is_blank: "Symbol.symbol -> bool"} \\
   18.93 +  @{index_ML_type "Symbol.sym"} \\
   18.94 +  @{index_ML Symbol.decode: "Symbol.symbol -> Symbol.sym"} \\
   18.95 +  \end{mldecls}
   18.96 +
   18.97 +  \begin{description}
   18.98 +
   18.99 +  \item @{ML_type "Symbol.symbol"} represents Isabelle symbols; this type
  18.100 +  is merely an alias for @{ML_type "string"}, but emphasizes the
  18.101 +  specific format encountered here.
  18.102 +
  18.103 +  \item @{ML "Symbol.explode"}~@{text "s"} produces an actual symbol
  18.104 +  list from the packed form usually encountered as user input.  This
  18.105 +  function replaces @{ML "String.explode"} for virtually all purposes
  18.106 +  of manipulating text in Isabelle!  Plain @{text "implode"} may be
  18.107 +  used for the reverse operation.
  18.108 +
  18.109 +  \item @{ML "Symbol.is_letter"}, @{ML "Symbol.is_digit"}, @{ML
  18.110 +  "Symbol.is_quasi"}, @{ML "Symbol.is_blank"} classify certain symbols
  18.111 +  (both ASCII and several named ones) according to fixed syntactic
  18.112 +  convections of Isabelle, e.g.\ see \cite{isabelle-isar-ref}.
  18.113 +
  18.114 +  \item @{ML_type "Symbol.sym"} is a concrete datatype that represents
  18.115 +  the different kinds of symbols explicitly as @{ML "Symbol.Char"},
  18.116 +  @{ML "Symbol.Sym"}, @{ML "Symbol.Ctrl"}, or @{ML "Symbol.Raw"}.
  18.117 +
  18.118 +  \item @{ML "Symbol.decode"} converts the string representation of a
  18.119 +  symbol into the explicit datatype version.
  18.120 +
  18.121 +  \end{description}
  18.122 +*}
  18.123 +
  18.124 +
  18.125 +subsection {* Qualified names and name spaces *}
  18.126 +
  18.127 +text %FIXME {* Qualified names are constructed according to implicit naming
  18.128 +principles of the present context.
  18.129 +
  18.130 +
  18.131 +The last component is called \emph{base name}; the remaining prefix of
  18.132 +qualification may be empty.
  18.133 +
  18.134 +Some practical conventions help to organize named entities more
  18.135 +systematically:
  18.136 +
  18.137 +\begin{itemize}
  18.138 +
  18.139 +\item Names are qualified first by the theory name, second by an
  18.140 +optional ``structure''.  For example, a constant @{text "c"} declared
  18.141 +as part of a certain structure @{text "b"} (say a type definition) in
  18.142 +theory @{text "A"} will be named @{text "A.b.c"} internally.
  18.143 +
  18.144 +\item
  18.145 +
  18.146 +\item
  18.147 +
  18.148 +\item
  18.149 +
  18.150 +\item
  18.151 +
  18.152 +\end{itemize}
  18.153 +
  18.154 +Names of different kinds of entities are basically independent, but
  18.155 +some practical naming conventions relate them to each other.  For
  18.156 +example, a constant @{text "foo"} may be accompanied with theorems
  18.157 +@{text "foo.intro"}, @{text "foo.elim"}, @{text "foo.simps"} etc.  The
  18.158 +same may happen for a type @{text "foo"}, which is then apt to cause
  18.159 +clashes in the theorem name space!  To avoid this, we occasionally
  18.160 +follow an additional convention of suffixes that determine the
  18.161 +original kind of entity that a name has been derived.  For example,
  18.162 +constant @{text "foo"} is associated with theorem @{text "foo.intro"},
  18.163 +type @{text "foo"} with theorem @{text "foo_type.intro"}, and type
  18.164 +class @{text "foo"} with @{text "foo_class.intro"}.
  18.165 +
  18.166 +*}
  18.167 +
  18.168 +
  18.169 +section {* Structured output *}
  18.170 +
  18.171 +subsection {* Pretty printing *}
  18.172 +
  18.173 +text FIXME
  18.174 +
  18.175 +subsection {* Output channels *}
  18.176 +
  18.177 +text FIXME
  18.178 +
  18.179 +subsection {* Print modes *}
  18.180 +
  18.181 +text FIXME
  18.182 +
  18.183 +
  18.184 +section {* Context \label{sec:context} *}
  18.185 +
  18.186 +text %FIXME {* What is a context anyway?  A highly advanced
  18.187 +technological and cultural achievement, which took humanity several
  18.188 +thousands of years to be develop, is writing with pen-and-paper.  Here
  18.189 +the paper is the context, or medium.  It accommodates a certain range
  18.190 +of different kinds of pens, but also has some inherent limitations.
  18.191 +For example, carved inscriptions are better done on solid material
  18.192 +like wood or stone.
  18.193 +
  18.194 +Isabelle/Isar distinguishes two key notions of context: \emph{theory
  18.195 +  context}\indexbold{theory context} and \emph{proof context}.\indexbold{proof
  18.196 +  context} To motivate this fundamental division consider the very idea of
  18.197 +logical reasoning which is about judgments $\Gamma \Drv{\Theta} \phi$, where
  18.198 +$\Theta$ is the background theory with declarations of operators and axioms
  18.199 +stating their properties, and $\Gamma$ a collection of hypotheses emerging
  18.200 +temporarily during proof.  For example, the rule of implication-introduction
  18.201 +\[
  18.202 +\infer{\Gamma \Drv{\Theta} A \Imp B}{\Gamma, A \Drv{\Theta} B}
  18.203 +\]
  18.204 +can be read as ``to show $A \Imp B$ we may assume $A$ as hypothesis and need
  18.205 +to show $B$''.  It is characteristic that $\Theta$ is unchanged and $\Gamma$
  18.206 +is only modified according to some general patterns of ``assuming'' and
  18.207 +``discharging'' hypotheses.  This admits the following abbreviated notation,
  18.208 +where the fixed $\Theta$ and locally changed $\Gamma$ are left implicit:
  18.209 +\[
  18.210 +\infer{A \Imp B}{\infer*{B}{[A]}}
  18.211 +\]
  18.212 +
  18.213 +In some logical traditions (e.g.\ Type Theory) there is a tendency to
  18.214 +unify all kinds of declarations within a single notion of context.
  18.215 +This is theoretically very nice, but also more demanding, because
  18.216 +everything is internalized into the logical calculus itself.
  18.217 +Isabelle/Pure is a very simple logic, but achieves many practically
  18.218 +useful concepts by differentiating various basic elements.
  18.219 +
  18.220 +Take polymorphism, for example.  Instead of embarking on the
  18.221 +adventurous enterprise of full higher-order logic with full
  18.222 +type-quantification and polymorphic entities, Isabelle/Pure merely
  18.223 +takes a stripped-down version of Church's Simple Type Theory
  18.224 +\cite{church40}.  Then after the tradition of Gordon's HOL
  18.225 +\cite{mgordon-hol} it is fairly easy to introduce syntactic notions of
  18.226 +type variables and type-constructors, and require every theory
  18.227 +$\Theta$ being closed by type instantiation.  Whenever we wish to
  18.228 +reason with a polymorphic constant or axiom scheme at a particular
  18.229 +type, we may assume that it has been referenced initially at that very
  18.230 +instance (due to the Deduction Theorem).  Thus we achieve the
  18.231 +following \emph{admissible
  18.232 +  rule}\glossary{Admissible rule}{FIXME} of schematic type-instantiation:
  18.233 +
  18.234 +\[
  18.235 +\infer{\phi(\tau)}{\infer*{\phi(\alpha)}{[\alpha]}}
  18.236 +\]
  18.237 +
  18.238 +Using this approach, the structured Isar proof language offers
  18.239 +schematic polymorphism within nested sub-proofs -- similar to that of
  18.240 +polymorphic let-bindings according to Hindley-Milner.\
  18.241 +\cite{milner78}.  All of this is achieved without disintegrating the
  18.242 +rather simplistic logical core.  On the other hand, the succinct rule
  18.243 +presented above already involves rather delicate interaction of the
  18.244 +theory and proof context (with side-conditions not mentioned here),
  18.245 +and unwinding an admissible rule involves induction over derivations.
  18.246 +All of this diversity needs to be accomodated by the system
  18.247 +architecture and actual implementation.
  18.248 +
  18.249 +\medskip Despite these important observations, Isabelle/Isar is not just a
  18.250 +logical calculus, there are further extra-logical aspects to be considered.
  18.251 +Practical experience over the years suggests two context data structures which
  18.252 +are used in rather dissimilar manners, even though there is a considerable
  18.253 +overlap of underlying ideas.
  18.254 +
  18.255 +From the system's perspective the mode of use of theory vs.\ proof context is
  18.256 +the key distinction.  The actual content is merely a generic slot for
  18.257 +\emph{theory data} and \emph{proof data}, respectively.  There are generic
  18.258 +interfaces to declare data entries at any time.  Even the core logic of
  18.259 +Isabelle/Pure registers its very own notion of theory context data (types,
  18.260 +constants, axioms etc.) like any other Isabelle tool out there.  Likewise, the
  18.261 +essentials of Isar proof contexts are one proof data slot among many others,
  18.262 +notably those of derived Isar concepts (e.g.\ calculational reasoning rules).
  18.263 +
  18.264 +In that respect, a theory is more like a stone tablet to carve long-lasting
  18.265 +inscriptions -- but take care not to break it!  While a proof context is like
  18.266 +a block of paper to scribble and dispose quickly.  More recently Isabelle has
  18.267 +started to cultivate the paper-based craftsmanship a bit further, by
  18.268 +maintaining small collections of paper booklets, better known as locales.
  18.269 +
  18.270 +Thus we achive ``thick'' augmented versions of {\boldmath$\Theta$} and
  18.271 +{\boldmath$\Gamma$} to support realistic structured reasoning within a
  18.272 +practically usable system.
  18.273 +*}
  18.274 +
  18.275 +
  18.276 +subsection {* Theory context \label{sec:context-theory} *}
  18.277 +
  18.278 +text %FIXME {* A theory context consists of management information plus the
  18.279 +actual data, which may be declared by other software modules later on.
  18.280 +The management part is surprisingly complex, we illustrate it by the
  18.281 +following typical situation of incremental theory development.
  18.282 +
  18.283 +\begin{tabular}{rcccl}
  18.284 +        &            & $Pure$ \\
  18.285 +        &            & $\downarrow$ \\
  18.286 +        &            & $FOL$ \\
  18.287 +        & $\swarrow$ &              & $\searrow$ & \\
  18.288 +  $Nat$ &            &              &            & $List$ \\
  18.289 +        & $\searrow$ &              & $\swarrow$ \\
  18.290 +        &            & $Length$ \\
  18.291 +        &            & \multicolumn{3}{l}{~~$\isarkeyword{imports}$} \\
  18.292 +        &            & \multicolumn{3}{l}{~~$\isarkeyword{begin}$} \\
  18.293 +        &            & $\vdots$~~ \\
  18.294 +        &            & $\bullet$~~ \\
  18.295 +        &            & $\vdots$~~ \\
  18.296 +        &            & $\bullet$~~ \\
  18.297 +        &            & $\vdots$~~ \\
  18.298 +        &            & \multicolumn{3}{l}{~~$\isarkeyword{end}$} \\
  18.299 +\end{tabular}
  18.300 +
  18.301 +\begin{itemize}
  18.302 +\item \emph{name}, \emph{parents} and \emph{ancestors}
  18.303 +\item \emph{identity}
  18.304 +\item \emph{intermediate versions}
  18.305 +\end{itemize}
  18.306 +
  18.307 +\begin{description}
  18.308 +\item [draft]
  18.309 +\item [intermediate]
  18.310 +\item [finished]
  18.311 +\end{description}
  18.312 +
  18.313 +\emph{theory reference}
  18.314 +*}
  18.315 +
  18.316 +
  18.317 +subsection {* Proof context \label{sec:context-proof} *}
  18.318 +
  18.319 +text {*
  18.320 +  FIXME
  18.321 +
  18.322 +\glossary{Proof context}{The static context of a structured proof,
  18.323 +acts like a local ``theory'' of the current portion of Isar proof
  18.324 +text, generalizes the idea of local hypotheses @{text "\<Gamma>"} in
  18.325 +judgments @{text "\<Gamma> \<turnstile> \<phi>"} of natural deduction calculi.  There is a
  18.326 +generic notion of introducing and discharging hypotheses.  Arbritrary
  18.327 +auxiliary context data may be adjoined.}
  18.328 +
  18.329 +*}
  18.330 +
  18.331 +end
    19.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    19.2 +++ b/doc-src/IsarImplementation/Thy/proof.thy	Mon Jan 02 20:16:52 2006 +0100
    19.3 @@ -0,0 +1,39 @@
    19.4 +
    19.5 +(* $Id$ *)
    19.6 +
    19.7 +theory "proof" imports base begin
    19.8 +
    19.9 +chapter {* Structured reasoning *}
   19.10 +
   19.11 +section {* Proof context *}
   19.12 +
   19.13 +text FIXME
   19.14 +
   19.15 +section {* Proof state *}
   19.16 +
   19.17 +text {*
   19.18 +  FIXME
   19.19 +
   19.20 +\glossary{Proof state}{The whole configuration of a structured proof,
   19.21 +consisting of a \seeglossary{proof context} and an optional
   19.22 +\seeglossary{structured goal}.  Internally, an Isar proof state is
   19.23 +organized as a stack to accomodate block structure of proof texts.
   19.24 +For historical reasons, a low-level \seeglossary{tactical goal} is
   19.25 +occasionally called ``proof state'' as well.}
   19.26 +
   19.27 +\glossary{Structured goal}{FIXME}
   19.28 +
   19.29 +\glossary{Goal}{See \seeglossary{tactical goal} or \seeglossary{structured goal}. \norefpage}
   19.30 +
   19.31 +
   19.32 +*}
   19.33 +
   19.34 +section {* Methods *}
   19.35 +
   19.36 +text FIXME
   19.37 +
   19.38 +section {* Attributes *}
   19.39 +
   19.40 +text FIXME
   19.41 +
   19.42 +end
    20.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    20.2 +++ b/doc-src/IsarImplementation/Thy/setup.ML	Mon Jan 02 20:16:52 2006 +0100
    20.3 @@ -0,0 +1,38 @@
    20.4 +
    20.5 +local structure O = IsarOutput
    20.6 +
    20.7 +val str_of_source = space_implode " " o map Args.string_of o #2 o #1 o Args.dest_src;
    20.8 +
    20.9 +fun ml_val txt = "fn _ => (" ^ txt ^ ");";
   20.10 +fun ml_type txt = "val _ = NONE : (" ^ txt ^ ") option;";
   20.11 +fun ml_structure txt = "functor DUMMY_FUNCTOR() = struct structure DUMMY = " ^ txt ^ " end;"
   20.12 +fun ml_functor txt = "val _ = ();";  (*no check!*)
   20.13 +
   20.14 +val verbatim = space_implode "\\verb,|," o map (enclose "\\verb|" "|") o space_explode "|";
   20.15 +
   20.16 +fun index_ml kind ml src ctxt (txt1, txt2) =
   20.17 +  let
   20.18 +    val txt = if txt2 = "" then txt1 else txt1 ^ ": " ^ txt2;
   20.19 +    val txt' = if kind = "" then txt else kind ^ " " ^ txt;
   20.20 +    val _ = Context.use_mltext (ml txt) false (SOME (ProofContext.theory_of ctxt));
   20.21 +  in
   20.22 +    "\\indexml" ^ kind ^ enclose "{" "}"
   20.23 +      (translate_string (fn "_" => "-" | ">" => "$>$" | c => c) txt1) ^
   20.24 +    ((if ! O.source then str_of_source src else txt')
   20.25 +    |> (if ! O.quotes then quote else I)
   20.26 +    |> (if ! O.display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"
   20.27 +    else split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n"))
   20.28 +  end;
   20.29 +
   20.30 +fun output_verbatim _ _ = split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n";
   20.31 +
   20.32 +fun arguments x = O.args (Scan.lift (Args.name -- Scan.optional (Args.colon |-- Args.name) "")) x;
   20.33 +
   20.34 +val _ = O.add_commands
   20.35 + [("index_ML", arguments (index_ml "" ml_val)),
   20.36 +  ("index_ML_type", arguments (index_ml "type" ml_type)),
   20.37 +  ("index_ML_structure", arguments (index_ml "structure" ml_structure)),
   20.38 +  ("index_ML_functor", arguments (index_ml "functor" ml_functor)),
   20.39 +  ("verbatim", O.args (Scan.lift Args.name) output_verbatim)];
   20.40 +
   20.41 +in val _ = () end;
    21.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    21.2 +++ b/doc-src/IsarImplementation/Thy/tactic.thy	Mon Jan 02 20:16:52 2006 +0100
    21.3 @@ -0,0 +1,188 @@
    21.4 +
    21.5 +(* $Id$ *)
    21.6 +
    21.7 +theory tactic imports base begin
    21.8 +
    21.9 +chapter {* Tactical theorem proving *}
   21.10 +
   21.11 +text {* The basic idea of tactical theorem proving is to refine the
   21.12 +initial claim in a backwards fashion, until a solved form is reached.
   21.13 +An intermediate goal consists of several subgoals that need to be
   21.14 +solved in order to achieve the main statement; zero subgoals means
   21.15 +that the proof may be finished.  Goal refinement operations are called
   21.16 +tactics; combinators for composing tactics are called tacticals.  *}
   21.17 +
   21.18 +
   21.19 +section {* Goals \label{sec:tactical-goals} *}
   21.20 +
   21.21 +text {* Isabelle/Pure represents a goal\glossary{Tactical goal}{A
   21.22 +theorem of \seeglossary{Horn Clause} form stating that a number of
   21.23 +subgoals imply the main conclusion, which is marked as a protected
   21.24 +proposition.} as a theorem stating that the subgoals imply the main
   21.25 +goal: @{text "A\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^sub>n \<Longrightarrow> C"}.  The outermost goal
   21.26 +structure is that of a Horn Clause\glossary{Horn Clause}{An iterated
   21.27 +implication @{text "A\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^sub>n \<Longrightarrow> C"}, without any
   21.28 +outermost quantifiers.  Strictly speaking, propositions @{text
   21.29 +"A\<^sub>i"} need to be atomic in Horn Clauses, but Isabelle admits
   21.30 +arbitrary substructure here (nested @{text "\<Longrightarrow>"} and @{text "\<And>"}
   21.31 +connectives).}: an iterated implication without any
   21.32 +quantifiers\footnote{Recall that outermost @{text "\<And>x. \<phi>[x]"} is
   21.33 +always represented via schematic variables in the body: @{text
   21.34 +"\<phi>[?x]"}.  These may get instantiated during the course of
   21.35 +reasoning.}.  For @{text "n = 0"} a goal is solved.
   21.36 +
   21.37 +The structure of each subgoal @{text "A\<^sub>i"} is that of a general
   21.38 +Heriditary Harrop Formula @{text "\<And>x\<^sub>1 \<dots> \<And>x\<^sub>k. H\<^sub>1 \<Longrightarrow>
   21.39 +\<dots> \<Longrightarrow> H\<^sub>m \<Longrightarrow> B"} according to the normal form where any local
   21.40 +@{text \<And>} is pulled before @{text \<Longrightarrow>}.  Here @{text "x\<^sub>1, \<dots>,
   21.41 +x\<^sub>k"} are goal parameters, i.e.\ arbitrary-but-fixed entities of
   21.42 +certain types, and @{text "H\<^sub>1, \<dots>, H\<^sub>m"} are goal
   21.43 +hypotheses, i.e.\ facts that may be assumed locally.  Together, this
   21.44 +forms the goal context of the conclusion @{text B} to be established.
   21.45 +The goal hypotheses may be again arbitrary Harrop Formulas, although
   21.46 +the level of nesting rarely exceeds 1--2 in practice.
   21.47 +
   21.48 +The main conclusion @{text C} is internally marked as a protected
   21.49 +proposition\glossary{Protected proposition}{An arbitrarily structured
   21.50 +proposition @{text "C"} which is forced to appear as atomic by
   21.51 +wrapping it into a propositional identity operator; notation @{text
   21.52 +"#C"}.  Protecting a proposition prevents basic inferences from
   21.53 +entering into that structure for the time being.}, which is
   21.54 +occasionally represented explicitly by the notation @{text "#C"}.
   21.55 +This ensures that the decomposition into subgoals and main conclusion
   21.56 +is well-defined for arbitrarily structured claims.
   21.57 +
   21.58 +\medskip Basic goal management is performed via the following
   21.59 +Isabelle/Pure rules:
   21.60 +
   21.61 +  \[
   21.62 +  \infer[@{text "(init)"}]{@{text "C \<Longrightarrow> #C"}}{} \qquad
   21.63 +  \infer[@{text "(finish)"}]{@{text "#C"}}{@{text "C"}}
   21.64 +  \]
   21.65 +
   21.66 +  \medskip The following low-level variants admit general reasoning
   21.67 +  with protected propositions:
   21.68 +
   21.69 +  \[
   21.70 +  \infer[@{text "(protect)"}]{@{text "#C"}}{@{text "C"}} \qquad
   21.71 +  \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"}}
   21.72 +  \]
   21.73 +*}
   21.74 +
   21.75 +text %mlref {*
   21.76 +  \begin{mldecls}
   21.77 +  @{index_ML Goal.init: "cterm -> thm"} \\
   21.78 +  @{index_ML Goal.finish: "thm -> thm"} \\
   21.79 +  @{index_ML Goal.protect: "thm -> thm"} \\
   21.80 +  @{index_ML Goal.conclude: "thm -> thm"} \\
   21.81 +  \end{mldecls}
   21.82 +
   21.83 +  \begin{description}
   21.84 +
   21.85 +  \item @{ML "Goal.init"}~@{text "\<phi>"} initializes a tactical goal with
   21.86 +  the type-checked proposition @{text \<phi>}.
   21.87 +
   21.88 +  \item @{ML "Goal.finish"}~@{text "th"} checks whether theorem @{text
   21.89 +  "th"} is a solved goal configuration (zero subgoals), and concludes
   21.90 +  the result by removing the goal protection.
   21.91 +
   21.92 +  \item @{ML "Goal.protect"}~@{text "th"} protects the whole statement
   21.93 +  of theorem @{text "th"}.
   21.94 +
   21.95 +  \item @{ML "Goal.conclude"}~@{text "th"} removes the goal protection
   21.96 +  for any number of pending subgoals.
   21.97 +
   21.98 +  \end{description}
   21.99 +*}
  21.100 +
  21.101 +
  21.102 +section {* Tactics *}
  21.103 +
  21.104 +text {*
  21.105 +
  21.106 +FIXME
  21.107 +
  21.108 +\glossary{Tactic}{Any function that maps a \seeglossary{tactical goal}
  21.109 +to a lazy sequence of possible sucessors.  This scheme subsumes
  21.110 +failure (empty result sequence), as well as lazy enumeration of proof
  21.111 +search results.  Error conditions are usually mapped to an empty
  21.112 +result, which gives further tactics a chance to try in turn.
  21.113 +Commonly, tactics either take an argument to address a particular
  21.114 +subgoal, or operate on a certain range of subgoals in a uniform
  21.115 +fashion.  In any case, the main conclusion is normally left untouched,
  21.116 +apart from instantiating \seeglossary{schematic variables}.}
  21.117 +
  21.118 +
  21.119 +*}
  21.120 +
  21.121 +section {* Tacticals *}
  21.122 +
  21.123 +text {*
  21.124 +
  21.125 +FIXME
  21.126 +
  21.127 +\glossary{Tactical}{A functional combinator for building up complex
  21.128 +tactics from simpler ones.  Typical tactical perform sequential
  21.129 +composition, disjunction (choice), iteration, or goal addressing.
  21.130 +Various search strategies may be expressed via tacticals.}
  21.131 +
  21.132 +*}
  21.133 +
  21.134 +section {* Programmed proofs *}
  21.135 +
  21.136 +text {*
  21.137 +  In order to perform a complete tactical proof under program control,
  21.138 +  one needs to set up an initial goal configuration, apply a tactic,
  21.139 +  and finish the result, cf.\ the rules given in
  21.140 +  \secref{sec:tactical-goals}.  Further checks are required to ensure
  21.141 +  that the result is actually an instance of the original claim --
  21.142 +  ill-behaved tactics could have destroyed that information.
  21.143 +
  21.144 +  Several simultaneous claims may be handled within a single goal
  21.145 +  statement by using meta-level conjunction internally.\footnote{This
  21.146 +  is merely syntax for certain derived statements within
  21.147 +  Isabelle/Pure, there is no need to introduce a separate conjunction
  21.148 +  operator.}  The whole configuration may be considered within a
  21.149 +  context of arbitrary-but-fixed parameters and hypotheses, which will
  21.150 +  be available as local facts during the proof and discharged into
  21.151 +  implications in the result.
  21.152 +
  21.153 +  All of these administrative tasks are packaged into a separate
  21.154 +  operation, such that the user merely needs to provide the statement
  21.155 +  and tactic to be applied.
  21.156 +*}
  21.157 +
  21.158 +text %mlref {*
  21.159 +  \begin{mldecls}
  21.160 +  @{index_ML Goal.prove: "theory -> string list -> term list -> term ->
  21.161 +  (thm list -> tactic) -> thm"} \\
  21.162 +  @{index_ML Goal.prove_multi: "theory -> string list -> term list -> term list ->
  21.163 +  (thm list -> tactic) -> thm list"} \\
  21.164 +  \end{mldecls}
  21.165 +
  21.166 +  \begin{description}
  21.167 +
  21.168 +  \item @{ML Goal.prove}~@{text "thy xs As C tac"} states goal @{text
  21.169 +  "C"} in the context of arbitrary-but-fixed parameters @{text "xs"}
  21.170 +  and hypotheses @{text "As"} and applies tactic @{text "tac"} to
  21.171 +  solve it.  The latter may depend on the local assumptions being
  21.172 +  presented as facts.  The result is essentially @{text "\<And>xs. As \<Longrightarrow>
  21.173 +  C"}, but is normalized by pulling @{text "\<And>"} before @{text "\<Longrightarrow>"}
  21.174 +  (the conclusion @{text "C"} itself may be a rule statement), turning
  21.175 +  the quantifier prefix into schematic variables, and generalizing
  21.176 +  implicit type-variables.
  21.177 +
  21.178 +  Any additional fixed variables or hypotheses not being mentioned in
  21.179 +  the initial statement are left unchanged --- programmed proofs may
  21.180 +  well occur in a larger context.
  21.181 +
  21.182 +  \item @{ML Goal.prove_multi} is simular to @{ML Goal.prove}, but
  21.183 +  states several conclusions simultaneously.  @{ML
  21.184 +  Tactic.conjunction_tac} may be used to split these into individual
  21.185 +  subgoals before commencing the actual proof.
  21.186 +
  21.187 +  \end{description}
  21.188 +*}
  21.189 +
  21.190 +end
  21.191 +
    22.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    22.2 +++ b/doc-src/IsarImplementation/Thy/unused.thy	Mon Jan 02 20:16:52 2006 +0100
    22.3 @@ -0,0 +1,16 @@
    22.4 +
    22.5 +text {*
    22.6 +  The Isar toplevel works differently for interactive developments
    22.7 +  vs.\ batch processing of theory sources.  For example, diagnostic
    22.8 +  commands produce a warning batch mode, because they are considered
    22.9 +  alien to the final theory document being produced eventually.
   22.10 +  Moreover, full @{text undo} with intermediate checkpoints to protect
   22.11 +  against destroying theories accidentally are limited to interactive
   22.12 +  mode.  In batch mode there is only a single strictly linear stream
   22.13 +  of potentially desctructive theory transformations.
   22.14 +*}
   22.15 +
   22.16 +  \item @{ML Toplevel.empty} is an empty transition; the Isar command
   22.17 +  dispatcher internally applies @{ML Toplevel.name} (for the command)
   22.18 +  name and @{ML Toplevel.position} for the source position.
   22.19 +
    23.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    23.2 +++ b/doc-src/IsarImplementation/checkglossary	Mon Jan 02 20:16:52 2006 +0100
    23.3 @@ -0,0 +1,28 @@
    23.4 +#!/usr/bin/env perl
    23.5 +# $Id$
    23.6 +
    23.7 +use strict;
    23.8 +
    23.9 +my %defs = ();
   23.10 +my %refs = ();
   23.11 +
   23.12 +while (<ARGV>) {
   23.13 +    if (m,\\glossaryentry\{\w*\\bf *((\w|\s)+)@,) {
   23.14 +	$defs{lc $1} = 1;
   23.15 +    }
   23.16 +    while (m,\\seeglossary *\{((\w|\s)+)\},g) {
   23.17 +	$refs{lc $1} = 1;
   23.18 +    }
   23.19 +}
   23.20 +
   23.21 +print "Glossary definitions:\n";
   23.22 +foreach (sort(keys(%defs))) {
   23.23 +    print "  \"$_\"\n";
   23.24 +}
   23.25 +
   23.26 +foreach (keys(%refs)) {
   23.27 +    s,s$,,;
   23.28 +    if (!defined($defs{$_})) {
   23.29 +	print "### Undefined glossary reference: \"$_\"\n";
   23.30 +    }
   23.31 +}
    24.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    24.2 +++ b/doc-src/IsarImplementation/implementation.tex	Mon Jan 02 20:16:52 2006 +0100
    24.3 @@ -0,0 +1,75 @@
    24.4 +
    24.5 +%% $Id$
    24.6 +
    24.7 +\documentclass[12pt,a4paper,fleqn]{report}
    24.8 +\usepackage{latexsym,graphicx}
    24.9 +\usepackage[refpage]{nomencl}
   24.10 +\usepackage{../iman,../extra,../isar,../proof}
   24.11 +\usepackage{Thy/document/isabelle,Thy/document/isabellesym}
   24.12 +\usepackage{style}
   24.13 +\usepackage{../pdfsetup}
   24.14 +
   24.15 +
   24.16 +\hyphenation{Isabelle}
   24.17 +\hyphenation{Isar}
   24.18 +
   24.19 +\isadroptag{theory}
   24.20 +\title{\includegraphics[scale=0.5]{isabelle_isar}
   24.21 +  \\[4ex] The Isabelle/Isar Implementation}
   24.22 +\author{\emph{Makarius M. M. Wenzel}}
   24.23 +
   24.24 +\makeglossary
   24.25 +\makeindex
   24.26 +
   24.27 +
   24.28 +\begin{document}
   24.29 +
   24.30 +\maketitle 
   24.31 +
   24.32 +\begin{abstract}
   24.33 +  We describe the key concepts underlying the Isabelle/Isar
   24.34 +  implementation, including ML references for the most important
   24.35 +  elements.  The aim is to give some insight into the overall system
   24.36 +  architecture, and provide clues on implementing user extensions.
   24.37 +\end{abstract}
   24.38 +
   24.39 +\pagenumbering{roman} \tableofcontents \clearfirst
   24.40 +
   24.41 +\input{intro.tex}
   24.42 +\input{Thy/document/prelim.tex}
   24.43 +\input{Thy/document/logic.tex}
   24.44 +\input{Thy/document/tactic.tex}
   24.45 +\input{Thy/document/proof.tex}
   24.46 +\input{Thy/document/locale.tex}
   24.47 +\input{Thy/document/integration.tex}
   24.48 +
   24.49 +% Isabelle was not designed; it evolved.
   24.50 +% Not everyone likes this idea. Specification experts rightly abhor trial-and-error programming.
   24.51 +% They suggest that no one should write a program without First writing a complete
   24.52 +% formal specification. But university departments are not software houses. Programs like
   24.53 +% Isabelle are not products: when they have served their purpose, they are discarded.
   24.54 +%
   24.55 +% L.C. Paulson, Isabelle: The Next 700 Theorem Provers
   24.56 +
   24.57 +\appendix
   24.58 +\input{Thy/document/ML.tex}
   24.59 +
   24.60 +\begingroup
   24.61 +\tocentry{\bibname}
   24.62 +\bibliographystyle{plain} \small\raggedright\frenchspacing
   24.63 +\bibliography{../manual}
   24.64 +\endgroup
   24.65 +
   24.66 +\tocentry{\glossaryname}
   24.67 +\printglossary
   24.68 +
   24.69 +\tocentry{\indexname}
   24.70 +\printindex
   24.71 +
   24.72 +\end{document}
   24.73 +
   24.74 +
   24.75 +%%% Local Variables: 
   24.76 +%%% mode: latex
   24.77 +%%% TeX-master: t
   24.78 +%%% End: 
    25.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    25.2 +++ b/doc-src/IsarImplementation/intro.tex	Mon Jan 02 20:16:52 2006 +0100
    25.3 @@ -0,0 +1,13 @@
    25.4 +
    25.5 +%% $Id$
    25.6 +
    25.7 +\chapter{Introduction}
    25.8 +
    25.9 +FIXME
   25.10 +
   25.11 +\nocite{Wenzel-PhD}
   25.12 +
   25.13 +%%% Local Variables: 
   25.14 +%%% mode: latex
   25.15 +%%% TeX-master: "implementation"
   25.16 +%%% End: 
    26.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    26.2 +++ b/doc-src/IsarImplementation/makeglossary	Mon Jan 02 20:16:52 2006 +0100
    26.3 @@ -0,0 +1,6 @@
    26.4 +#!/bin/sh
    26.5 +# $Id$
    26.6 +
    26.7 +NAME="$1"
    26.8 +makeindex -s nomencl -o "${NAME}.gls" "${NAME}.glo"
    26.9 +./checkglossary "${NAME}.glo"
    27.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    27.2 +++ b/doc-src/IsarImplementation/style.sty	Mon Jan 02 20:16:52 2006 +0100
    27.3 @@ -0,0 +1,59 @@
    27.4 +
    27.5 +%% $Id$
    27.6 +
    27.7 +%% toc
    27.8 +\newcommand{\tocentry}[1]{\cleardoublepage\phantomsection\addcontentsline{toc}{chapter}{#1}}
    27.9 +
   27.10 +%% references
   27.11 +\newcommand{\secref}[1]{\S\ref{#1}}
   27.12 +\newcommand{\figref}[1]{figure~\ref{#1}}
   27.13 +
   27.14 +%% glossary
   27.15 +\renewcommand{\glossary}[2]{\nomenclature{\bf #1}{#2}}
   27.16 +\newcommand{\seeglossary}[1]{\emph{#1}}
   27.17 +\def\glossaryname{Glossary}
   27.18 +\renewcommand{\nomname}{\glossaryname}
   27.19 +\renewcommand{\pagedeclaration}[1]{\nobreak\quad\dotfill~page~\bold{#1}}
   27.20 +
   27.21 +\newcommand{\drv}{\mathrel{\vdash}}
   27.22 +\newcommand{\edrv}{\mathop{\drv}\nolimits}
   27.23 +\newcommand{\Drv}[1]{\mathrel{\vdash_{#1}}}
   27.24 +\newcommand{\Or}{\mathrel{\;|\;}}
   27.25 +
   27.26 +\renewcommand{\vec}[1]{\overline{#1}}
   27.27 +\renewcommand{\phi}{\varphi}
   27.28 +
   27.29 +\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}
   27.30 +
   27.31 +\pagestyle{headings}
   27.32 +\sloppy
   27.33 +\binperiod
   27.34 +\underscoreon
   27.35 +
   27.36 +\newenvironment{mldecls}{\par\noindent\begingroup\def\isanewline{\\}\begin{tabular}{l}}{\end{tabular}\medskip\endgroup}
   27.37 +
   27.38 +\isafoldtag{FIXME}
   27.39 +\isakeeptag{mlref}
   27.40 +\renewcommand{\isatagmlref}{\subsection*{\makebox[0pt][r]{\fbox{\ML}~~}Reference}\begingroup\def\isastyletext{\rm}\small}
   27.41 +\renewcommand{\endisatagmlref}{\endgroup}
   27.42 +
   27.43 +\newcommand{\indexml}[1]{\index{\emph{#1} ({\ML})|bold}}
   27.44 +\newcommand{\indexmltype}[1]{\index{\emph{#1} ({\ML} type)|bold}}
   27.45 +\newcommand{\indexmlstructure}[1]{\index{\emph{#1} ({\ML} structure)|bold}}
   27.46 +\newcommand{\indexmlfunctor}[1]{\index{\emph{#1} ({\ML} functor)|bold}}
   27.47 +
   27.48 +\newcommand{\isasymTHEORY}{\isakeyword{theory}}
   27.49 +\newcommand{\isasymIMPORTS}{\isakeyword{imports}}
   27.50 +\newcommand{\isasymUSES}{\isakeyword{uses}}
   27.51 +\newcommand{\isasymBEGIN}{\isakeyword{begin}}
   27.52 +\newcommand{\isasymEND}{\isakeyword{end}}
   27.53 +\newcommand{\isasymCONSTS}{\isakeyword{consts}}
   27.54 +\newcommand{\isasymDEFS}{\isakeyword{defs}}
   27.55 +\newcommand{\isasymTHEOREM}{\isakeyword{theorem}}
   27.56 +
   27.57 +\isabellestyle{it}
   27.58 +
   27.59 +%%% Local Variables: 
   27.60 +%%% mode: latex
   27.61 +%%% TeX-master: "implementation"
   27.62 +%%% End: