# HG changeset patch # User wenzelm # Date 1286740165 -3600 # Node ID eb47307ab9301881de154032c24055aab6e9dd89 # Parent eacb7825025d56849007715f367cdfa5e96d3b70 removed some obsolete reference material; diff -r eacb7825025d -r eb47307ab930 doc-src/Ref/introduction.tex --- a/doc-src/Ref/introduction.tex Sun Oct 10 20:42:10 2010 +0100 +++ b/doc-src/Ref/introduction.tex Sun Oct 10 20:49:25 2010 +0100 @@ -1,5 +1,5 @@ -\chapter{Basic Use of Isabelle}\index{sessions|(} +\chapter{Basic Use of Isabelle} \section{Ending a session} \begin{ttbox} @@ -22,108 +22,6 @@ Typing control-D also finishes the session in essentially the same way as the sequence {\tt commit(); quit();} would. - -\section{Reading ML files} -\index{files!reading} -\begin{ttbox} -cd : string -> unit -pwd : unit -> string -use : string -> unit -time_use : string -> unit -\end{ttbox} -\begin{ttdescription} -\item[\ttindexbold{cd} "{\it dir}";] changes the current directory to - {\it dir}. This is the default directory for reading files. - -\item[\ttindexbold{pwd}();] returns the full path of the current - directory. - -\item[\ttindexbold{use} "$file$";] -reads the given {\it file} as input to the \ML{} session. Reading a file -of Isabelle commands is the usual way of replaying a proof. - -\item[\ttindexbold{time_use} "$file$";] -performs {\tt use~"$file$"} and prints the total execution time. -\end{ttdescription} - -The $dir$ and $file$ specifications of the \texttt{cd} and \texttt{use} -commands may contain path variables (e.g.\ \texttt{\$ISABELLE_HOME}) that are -expanded appropriately. Note that \texttt{\~\relax} abbreviates -\texttt{\$HOME}, and \texttt{\~\relax\~\relax} abbreviates -\texttt{\$ISABELLE_HOME}\index{*\$ISABELLE_HOME}. The syntax for path -specifications follows Unix conventions. - - -\section{Reading theories}\label{sec:intro-theories} -\index{theories!reading} - -In Isabelle, any kind of declarations, definitions, etc.\ are organized around -named \emph{theory} objects. Logical reasoning always takes place within a -certain theory context, which may be switched at any time. Theory $name$ is -defined by a theory file $name$\texttt{.thy}, containing declarations of -\texttt{consts}, \texttt{types}, \texttt{defs}, etc.\ (see -\S\ref{sec:ref-defining-theories} for more details on concrete syntax). -Furthermore, there may be an associated {\ML} file $name$\texttt{.ML} with -proof scripts that are to be run in the context of the theory. - -\begin{ttbox} -context : theory -> unit -the_context : unit -> theory -theory : string -> theory -use_thy : string -> unit -time_use_thy : string -> unit -update_thy : string -> unit -\end{ttbox} - -\begin{ttdescription} - -\item[\ttindexbold{context} $thy$;] switches the current theory context. Any - subsequent command with ``implicit theory argument'' (e.g.\ \texttt{Goal}) - will refer to $thy$ as its theory. - -\item[\ttindexbold{the_context}();] obtains the current theory context, or - raises an error if absent. - -\item[\ttindexbold{theory} "$name$";] retrieves the theory called $name$ from - the internal data\-base of loaded theories, raising an error if absent. - -\item[\ttindexbold{use_thy} "$name$";] reads theory $name$ from the file - system, looking for $name$\texttt{.thy} and $name$\texttt{.ML} (the latter - being optional). It also ensures that all parent theories are loaded as - well. In case some older versions have already been present, - \texttt{use_thy} only tries to reload $name$ itself, but is content with any - version of its ancestors. - -\item[\ttindexbold{time_use_thy} "$name$";] same as \texttt{use_thy}, but - reports the time taken to process the actual theory parts and {\ML} files - separately. - -\item[\ttindexbold{update_thy} "$name$";] is similar to \texttt{use_thy}, but - ensures that theory $name$ is fully up-to-date with respect to the file - system --- apart from theory $name$ itself, any of its ancestors may be - reloaded as well. - -\end{ttdescription} - -Note that theories of pre-built logic images (e.g.\ HOL) are marked as -\emph{finished} and cannot be updated any more. See \S\ref{sec:more-theories} -for further information on Isabelle's theory loader. - - -\section{Timing} -\index{timing statistics}\index{proofs!timing} -\begin{ttbox} -timing: bool ref \hfill{\bf initially false} -\end{ttbox} - -\begin{ttdescription} -\item[set \ttindexbold{timing};] enables global timing in Isabelle. - This information is compiler-dependent. -\end{ttdescription} - -\index{sessions|)} - - %%% Local Variables: %%% mode: latex %%% TeX-master: "ref" diff -r eacb7825025d -r eb47307ab930 doc-src/Ref/theories.tex --- a/doc-src/Ref/theories.tex Sun Oct 10 20:42:10 2010 +0100 +++ b/doc-src/Ref/theories.tex Sun Oct 10 20:49:25 2010 +0100 @@ -7,37 +7,6 @@ Isabelle's theory loader manages dependencies of the internal graph of theory nodes (the \emph{theory database}) and the external view of the file system. -See \S\ref{sec:intro-theories} for its most basic commands, such as -\texttt{use_thy}. There are a few more operations available. - -\begin{ttbox} -use_thy_only : string -> unit -update_thy_only : string -> unit -touch_thy : string -> unit -remove_thy : string -> unit -delete_tmpfiles : bool ref \hfill\textbf{initially true} -\end{ttbox} - -\begin{ttdescription} -\item[\ttindexbold{use_thy_only} "$name$";] is similar to \texttt{use_thy}, - but processes the actual theory file $name$\texttt{.thy} only, ignoring - $name$\texttt{.ML}. This might be useful in replaying proof scripts by hand - from the very beginning, starting with the fresh theory. - -\item[\ttindexbold{update_thy_only} "$name$";] is similar to - \texttt{update_thy}, but processes the actual theory file - $name$\texttt{.thy} only, ignoring $name$\texttt{.ML}. - -\item[\ttindexbold{touch_thy} "$name$";] marks theory node $name$ of the - internal graph as outdated. While the theory remains usable, subsequent - operations such as \texttt{use_thy} may cause a reload. - -\item[\ttindexbold{remove_thy} "$name$";] deletes theory node $name$, - including \emph{all} of its descendants. Beware! This is a quick way to - dispose a large number of theories at once. Note that {\ML} bindings to - theorems etc.\ of removed theories may still persist. - -\end{ttdescription} \medskip Theory and {\ML} files are located by skimming through the directories listed in Isabelle's internal load path, which merely contains the @@ -83,133 +52,18 @@ \subsection{*Theory inclusion} \begin{ttbox} -subthy : theory * theory -> bool -eq_thy : theory * theory -> bool transfer : theory -> thm -> thm -transfer_sg : Sign.sg -> thm -> thm \end{ttbox} -Inclusion and equality of theories is determined by unique -identification stamps that are created when declaring new components. -Theorems contain a reference to the theory (actually to its signature) -they have been derived in. Transferring theorems to super theories -has no logical significance, but may affect some operations in subtle -ways (e.g.\ implicit merges of signatures when applying rules, or -pretty printing of theorems). +Transferring theorems to super theories has no logical significance, +but may affect some operations in subtle ways (e.g.\ implicit merges +of signatures when applying rules, or pretty printing of theorems). \begin{ttdescription} -\item[\ttindexbold{subthy} ($thy@1$, $thy@2$)] determines if $thy@1$ - is included in $thy@2$ wrt.\ identification stamps. - -\item[\ttindexbold{eq_thy} ($thy@1$, $thy@2$)] determines if $thy@1$ - is exactly the same as $thy@2$. - \item[\ttindexbold{transfer} $thy$ $thm$] transfers theorem $thm$ to theory $thy$, provided the latter includes the theory of $thm$. -\item[\ttindexbold{transfer_sg} $sign$ $thm$] is similar to - \texttt{transfer}, but identifies the super theory via its - signature. - -\end{ttdescription} - - -\subsection{*Primitive theories} -\begin{ttbox} -ProtoPure.thy : theory -Pure.thy : theory -CPure.thy : theory -\end{ttbox} -\begin{description} -\item[\ttindexbold{ProtoPure.thy}, \ttindexbold{Pure.thy}, - \ttindexbold{CPure.thy}] contain the syntax and signature of the - meta-logic. There are basically no axioms: meta-level inferences - are carried out by \ML\ functions. \texttt{Pure} and \texttt{CPure} - just differ in their concrete syntax of prefix function application: - $t(u@1, \ldots, u@n)$ in \texttt{Pure} vs.\ $t\,u@1,\ldots\,u@n$ in - \texttt{CPure}. \texttt{ProtoPure} is their common parent, - containing no syntax for printing prefix applications at all! - -%% FIXME -%\item [\ttindexbold{extend_theory} $thy$ {\tt"}$T${\tt"} $\cdots$] extends -% the theory $thy$ with new types, constants, etc. $T$ identifies the theory -% internally. When a theory is redeclared, say to change an incorrect axiom, -% bindings to the old axiom may persist. Isabelle ensures that the old and -% new theories are not involved in the same proof. Attempting to combine -% different theories having the same name $T$ yields the fatal error -%extend_theory : theory -> string -> \(\cdots\) -> theory -%\begin{ttbox} -%Attempt to merge different versions of theory: \(T\) -%\end{ttbox} -\end{description} - -%% FIXME -%\item [\ttindexbold{extend_theory} $thy$ {\tt"}$T${\tt"} -% ($classes$, $default$, $types$, $arities$, $consts$, $sextopt$) $rules$] -%\hfill\break %%% include if line is just too short -%is the \ML{} equivalent of the following theory definition: -%\begin{ttbox} -%\(T\) = \(thy\) + -%classes \(c\) < \(c@1\),\(\dots\),\(c@m\) -% \dots -%default {\(d@1,\dots,d@r\)} -%types \(tycon@1\),\dots,\(tycon@i\) \(n\) -% \dots -%arities \(tycon@1'\),\dots,\(tycon@j'\) :: (\(s@1\),\dots,\(s@n\))\(c\) -% \dots -%consts \(b@1\),\dots,\(b@k\) :: \(\tau\) -% \dots -%rules \(name\) \(rule\) -% \dots -%end -%\end{ttbox} -%where -%\begin{tabular}[t]{l@{~=~}l} -%$classes$ & \tt[("$c$",["$c@1$",\dots,"$c@m$"]),\dots] \\ -%$default$ & \tt["$d@1$",\dots,"$d@r$"]\\ -%$types$ & \tt[([$tycon@1$,\dots,$tycon@i$], $n$),\dots] \\ -%$arities$ & \tt[([$tycon'@1$,\dots,$tycon'@j$], ([$s@1$,\dots,$s@n$],$c$)),\dots] -%\\ -%$consts$ & \tt[([$b@1$,\dots,$b@k$],$\tau$),\dots] \\ -%$rules$ & \tt[("$name$",$rule$),\dots] -%\end{tabular} - - -\subsection{Inspecting a theory}\label{sec:inspct-thy} -\index{theories!inspecting|bold} -\begin{ttbox} -print_syntax : theory -> unit -print_theory : theory -> unit -parents_of : theory -> theory list -ancestors_of : theory -> theory list -sign_of : theory -> Sign.sg -Sign.stamp_names_of : Sign.sg -> string list -\end{ttbox} -These provide means of viewing a theory's components. -\begin{ttdescription} -\item[\ttindexbold{print_syntax} $thy$] prints the syntax of $thy$ - (grammar, macros, translation functions etc., see - page~\pageref{pg:print_syn} for more details). - -\item[\ttindexbold{print_theory} $thy$] prints the logical parts of - $thy$, excluding the syntax. - -\item[\ttindexbold{parents_of} $thy$] returns the direct ancestors - of~$thy$. - -\item[\ttindexbold{ancestors_of} $thy$] returns all ancestors of~$thy$ - (not including $thy$ itself). - -\item[\ttindexbold{sign_of} $thy$] returns the signature associated - with~$thy$. It is useful with functions like {\tt - read_instantiate_sg}, which take a signature as an argument. - -\item[\ttindexbold{Sign.stamp_names_of} $sg$]\index{signatures} - returns the names of the identification \rmindex{stamps} of ax - signature. These coincide with the names of its full ancestry - including that of $sg$ itself. - \end{ttdescription}