144 code $verbatim$. |
144 code $verbatim$. |
145 |
145 |
146 \item[$oracle$] links the theory to a trusted external reasoner. It is |
146 \item[$oracle$] links the theory to a trusted external reasoner. It is |
147 allowed to create theorems, but each theorem carries a proof object |
147 allowed to create theorems, but each theorem carries a proof object |
148 describing the oracle invocation. See \S\ref{sec:oracles} for details. |
148 describing the oracle invocation. See \S\ref{sec:oracles} for details. |
|
149 |
|
150 \item[$local, global$] changes the current name declaration mode. |
|
151 Initially, theories start in $local$ mode, causing all names of |
|
152 types, constants, axioms etc.\ to be automatically qualified by the |
|
153 theory name. Changing this to $global$ causes all names to be |
|
154 declared as short base names only. |
|
155 |
|
156 The $local$ and $global$ declarations act like switches, affecting |
|
157 all following theory sections until changed again explicitly. Also |
|
158 note that the final state at the end of the theory will persist. In |
|
159 particular, this determines how the names of theorems stored later |
|
160 on are handled. |
149 |
161 |
150 \item[$ml$] \index{*ML section} |
162 \item[$ml$] \index{*ML section} |
151 consists of \ML\ code, typically for parse and print translation functions. |
163 consists of \ML\ code, typically for parse and print translation functions. |
152 \end{description} |
164 \end{description} |
153 % |
165 % |
236 \end{ttdescription} |
248 \end{ttdescription} |
237 % |
249 % |
238 Each theory definition must reside in a separate file. Let the file |
250 Each theory definition must reside in a separate file. Let the file |
239 {\it T}{\tt.thy} contain the definition of a theory called~$T$, whose |
251 {\it T}{\tt.thy} contain the definition of a theory called~$T$, whose |
240 parent theories are $TB@1$ \dots $TB@n$. Calling |
252 parent theories are $TB@1$ \dots $TB@n$. Calling |
241 \ttindex{use_thy}~{\tt"{\it T\/}"} reads the file {\it T}{\tt.thy}, |
253 \texttt{use_thy}~{\tt"{\it T\/}"} reads the file {\it T}{\tt.thy}, |
242 writes a temporary \ML{} file {\tt.{\it T}.thy.ML}, and reads the |
254 writes a temporary \ML{} file {\tt.{\it T}.thy.ML}, and reads the |
243 latter file. Recursive {\tt use_thy} calls load those parent theories |
255 latter file. Recursive {\tt use_thy} calls load those parent theories |
244 that have not been loaded previously; the recursive calls may continue |
256 that have not been loaded previously; the recursive calls may continue |
245 to any depth. One {\tt use_thy} call can read an entire logic |
257 to any depth. One {\tt use_thy} call can read an entire logic |
246 provided all theories are linked appropriately. |
258 provided all theories are linked appropriately. |
260 {\tt.ML} file must declare an \ML\ structure having the theory's name and a |
272 {\tt.ML} file must declare an \ML\ structure having the theory's name and a |
261 component {\tt thy} containing the new theory object. |
273 component {\tt thy} containing the new theory object. |
262 Section~\ref{sec:pseudo-theories} below describes a way of linking such |
274 Section~\ref{sec:pseudo-theories} below describes a way of linking such |
263 theories to their parents. |
275 theories to their parents. |
264 |
276 |
265 \begin{warn} |
|
266 Temporary files are written to the current directory, so this must be |
|
267 writable. Isabelle inherits the current directory from the operating |
|
268 system; you can change it within Isabelle by typing {\tt |
|
269 cd"$dir$"}\index{*cd}. |
|
270 \end{warn} |
|
271 |
|
272 |
277 |
273 \section{Reloading modified theories}\label{sec:reloading-theories} |
278 \section{Reloading modified theories}\label{sec:reloading-theories} |
274 \indexbold{theories!reloading} |
279 \indexbold{theories!reloading} |
275 \begin{ttbox} |
280 \begin{ttbox} |
276 update : unit -> unit |
281 update : unit -> unit |
280 descended from it. However, {\tt use_thy} reads only one theory, even if |
285 descended from it. However, {\tt use_thy} reads only one theory, even if |
281 some of the parent theories are out of date. In this case you should call |
286 some of the parent theories are out of date. In this case you should call |
282 {\tt update()}. |
287 {\tt update()}. |
283 |
288 |
284 Isabelle keeps track of all loaded theories and their files. If |
289 Isabelle keeps track of all loaded theories and their files. If |
285 \ttindex{use_thy} finds that the theory to be loaded has been read before, |
290 \texttt{use_thy} finds that the theory to be loaded has been read |
286 it determines whether to reload the theory as follows. First it looks for |
291 before, it determines whether to reload the theory as follows. First |
287 the theory's files in their previous location. If it finds them, it |
292 it looks for the theory's files in their previous location. If it |
288 compares their modification times to the internal data and stops if they |
293 finds them, it compares their modification times to the internal data |
289 are equal. If the files have been moved, {\tt use_thy} searches for them |
294 and stops if they are equal. If the files have been moved, {\tt |
290 as it would for a new theory. After {\tt use_thy} reloads a theory, it |
295 use_thy} searches for them as it would for a new theory. After {\tt |
291 marks the children as out-of-date. |
296 use_thy} reloads a theory, it marks the children as out-of-date. |
292 |
297 |
293 \begin{ttdescription} |
298 \begin{ttdescription} |
294 \item[\ttindexbold{update}()] |
299 \item[\ttindexbold{update}()] |
295 reloads all modified theories and their descendants in the correct order. |
300 reloads all modified theories and their descendants in the correct order. |
296 |
301 |
700 displays $t$ as a string, using the syntax of~$sign$. |
705 displays $t$ as a string, using the syntax of~$sign$. |
701 \end{ttdescription} |
706 \end{ttdescription} |
702 |
707 |
703 \subsection{Making and inspecting certified terms} |
708 \subsection{Making and inspecting certified terms} |
704 \begin{ttbox} |
709 \begin{ttbox} |
705 cterm_of : Sign.sg -> term -> cterm |
710 cterm_of : Sign.sg -> term -> cterm |
706 read_cterm : Sign.sg -> string * typ -> cterm |
711 read_cterm : Sign.sg -> string * typ -> cterm |
707 cert_axm : Sign.sg -> string * term -> string * term |
712 cert_axm : Sign.sg -> string * term -> string * term |
708 read_axm : Sign.sg -> string * string -> string * term |
713 read_axm : Sign.sg -> string * string -> string * term |
709 rep_cterm : cterm -> {\ttlbrace}T:typ, t:term, sign:Sign.sg, maxidx:int\ttrbrace |
714 rep_cterm : cterm -> {\ttlbrace}T:typ, t:term, sign:Sign.sg, maxidx:int\ttrbrace |
710 \end{ttbox} |
715 Sign.certify_term : Sign.sg -> term -> term * typ * int |
711 \begin{ttdescription} |
716 \end{ttbox} |
712 \item[\ttindexbold{cterm_of} $sign$ $t$] \index{signatures} |
717 \begin{ttdescription} |
713 certifies $t$ with respect to signature~$sign$. |
718 |
714 |
719 \item[\ttindexbold{cterm_of} $sign$ $t$] \index{signatures} certifies |
715 \item[\ttindexbold{read_cterm} $sign$ ($s$, $T$)] |
720 $t$ with respect to signature~$sign$. |
716 reads the string~$s$ using the syntax of~$sign$, creating a certified term. |
721 |
717 The term is checked to have type~$T$; this type also tells the parser what |
722 \item[\ttindexbold{read_cterm} $sign$ ($s$, $T$)] reads the string~$s$ |
718 kind of phrase to parse. |
723 using the syntax of~$sign$, creating a certified term. The term is |
719 |
724 checked to have type~$T$; this type also tells the parser what kind |
720 \item[\ttindexbold{cert_axm} $sign$ ($name$, $t$)] |
725 of phrase to parse. |
721 certifies $t$ with respect to $sign$ as a meta-proposition and converts all |
726 |
722 exceptions to an error, including the final message |
727 \item[\ttindexbold{cert_axm} $sign$ ($name$, $t$)] certifies $t$ with |
|
728 respect to $sign$ as a meta-proposition and converts all exceptions |
|
729 to an error, including the final message |
723 \begin{ttbox} |
730 \begin{ttbox} |
724 The error(s) above occurred in axiom "\(name\)" |
731 The error(s) above occurred in axiom "\(name\)" |
725 \end{ttbox} |
732 \end{ttbox} |
726 |
733 |
727 \item[\ttindexbold{read_axm} $sign$ ($name$, $s$)] |
734 \item[\ttindexbold{read_axm} $sign$ ($name$, $s$)] similar to {\tt |
728 similar to {\tt cert_axm}, but first reads the string $s$ using the syntax of |
735 cert_axm}, but first reads the string $s$ using the syntax of |
729 $sign$. |
736 $sign$. |
730 |
737 |
731 \item[\ttindexbold{rep_cterm} $ct$] |
738 \item[\ttindexbold{rep_cterm} $ct$] decomposes $ct$ as a record |
732 decomposes $ct$ as a record containing its type, the term itself, its |
739 containing its type, the term itself, its signature, and the maximum |
733 signature, and the maximum subscript of its unknowns. The type and maximum |
740 subscript of its unknowns. The type and maximum subscript are |
734 subscript are computed during certification. |
741 computed during certification. |
|
742 |
|
743 \item[\ttindexbold{Sign.certify_term}] is a more primitive version of |
|
744 \texttt{cterm_of}, returning the internal representation instead of |
|
745 an abstract \texttt{cterm}. |
|
746 |
735 \end{ttdescription} |
747 \end{ttdescription} |
736 |
748 |
737 |
749 |
738 \section{Types}\index{types|bold} |
750 \section{Types}\index{types|bold} |
739 Types belong to the \ML\ type \mltydx{typ}, which is a concrete datatype with |
751 Types belong to the \ML\ type \mltydx{typ}, which is a concrete datatype with |
791 \end{ttdescription} |
803 \end{ttdescription} |
792 |
804 |
793 |
805 |
794 \subsection{Making and inspecting certified types} |
806 \subsection{Making and inspecting certified types} |
795 \begin{ttbox} |
807 \begin{ttbox} |
796 ctyp_of : Sign.sg -> typ -> ctyp |
808 ctyp_of : Sign.sg -> typ -> ctyp |
797 rep_ctyp : ctyp -> {\ttlbrace}T: typ, sign: Sign.sg\ttrbrace |
809 rep_ctyp : ctyp -> {\ttlbrace}T: typ, sign: Sign.sg\ttrbrace |
798 \end{ttbox} |
810 Sign.certify_typ : Sign.sg -> typ -> typ |
799 \begin{ttdescription} |
811 \end{ttbox} |
800 \item[\ttindexbold{ctyp_of} $sign$ $T$] \index{signatures} |
812 \begin{ttdescription} |
801 certifies $T$ with respect to signature~$sign$. |
813 |
802 |
814 \item[\ttindexbold{ctyp_of} $sign$ $T$] \index{signatures} certifies |
803 \item[\ttindexbold{rep_ctyp} $cT$] |
815 $T$ with respect to signature~$sign$. |
804 decomposes $cT$ as a record containing the type itself and its signature. |
816 |
|
817 \item[\ttindexbold{rep_ctyp} $cT$] decomposes $cT$ as a record |
|
818 containing the type itself and its signature. |
|
819 |
|
820 \item[\ttindexbold{Sign.certify_typ}] is a more primitive version of |
|
821 \texttt{ctyp_of}, returning the internal representation instead of |
|
822 an abstract \texttt{ctyp}. |
|
823 |
805 \end{ttdescription} |
824 \end{ttdescription} |
806 |
825 |
807 |
826 |
808 \section{Oracles: calling trusted external reasoners} |
827 \section{Oracles: calling trusted external reasoners} |
809 \label{sec:oracles} |
828 \label{sec:oracles} |