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