# HG changeset patch # User wenzelm # Date 925749348 -7200 # Node ID b38bc78d9a9d6abe14b6c7650fdd9eb0551582fb # Parent 8338dd394144f3eaa5d5fccbc252da9b27361d2d theory loader stuff updated and improved; diff -r 8338dd394144 -r b38bc78d9a9d doc-src/Ref/introduction.tex --- a/doc-src/Ref/introduction.tex Mon May 03 14:43:52 1999 +0200 +++ b/doc-src/Ref/introduction.tex Mon May 03 18:35:48 1999 +0200 @@ -15,17 +15,17 @@ finally esoteric functions. Use the Index when you are looking for the definition of a particular Isabelle function. -A few examples are presented. Many examples files are distributed with +A few examples are presented. Many example files are distributed with Isabelle, however; please experiment interactively. \section{Basic interaction with Isabelle} \index{starting up|bold}\nobreak % -We assume that your local Isabelle administrator (this might be you!) -has already installed the \Pure\ system and several object-logics -properly --- otherwise see the {\tt INSTALL} file in the top-level -directory of the distribution on how to build it. +We assume that your local Isabelle administrator (this might be you!) has +already installed the Isabelle system together with appropriate object-logics +--- otherwise see the \texttt{README} and \texttt{INSTALL} files in the +top-level directory of the distribution on how to do this. \medskip Let $\langle isabellehome \rangle$ denote the location where the distribution has been installed. To run Isabelle from a the shell @@ -33,61 +33,67 @@ \begin{ttbox} \({\langle}isabellehome{\rangle}\)/bin/isabelle \end{ttbox} -This should start an interactive \ML{} session with the default -object-logic already preloaded. +This should start an interactive \ML{} session with the default object-logic +(usually {\HOL}) already pre-loaded. -Subsequently we assume that {\tt \(\langle isabellehome \rangle\)/bin} -has been added to your shell's search path, in order to avoid typing -full path specifications of the executable files. +Subsequently, we assume that the \texttt{isabelle} executable is determined +automatically by the shell, e.g.\ by adding {\tt \(\langle isabellehome + \rangle\)/bin} to your search path.\footnote{Depending on your installation, + there might be also stand-alone binaries located in some global directory + such as \texttt{/usr/bin}. Do not attempt to copy {\tt \(\langle + isabellehome \rangle\)/bin/isabelle}, though! See \texttt{isatool + install} in \emph{The Isabelle System Manual} of how to do this properly.} -The object-logic image to load may be also specified explicitly as an -argument to the {\tt isabelle} command, e.g. +The object-logic image to load may be also specified explicitly as an argument +to the {\tt isabelle} command, e.g. \begin{ttbox} isabelle FOL \end{ttbox} -This should put you into the world of polymorphic first-order logic -(assuming that {\FOL} has been pre-built). +This should put you into the world of polymorphic first-order logic (assuming +that an image of {\FOL} has been pre-built). -\index{saving your work|bold} Isabelle provides no means of storing -theorems or internal proof objects on files. Theorems are simply part -of the \ML{} state. To save your work between sessions, you must dump -the \ML{} system state to a file. This is done automatically when -ending the session normally (e.g.\ by typing control-D), provided that -the image has been opened \emph{writable} in the first place. The -standard object-logic images are usually read-only, so you probably -have to create a private working copy first. For example, the -following shell command puts you into a writable Isabelle session of -name \texttt{Foo} that initially contains just \FOL: +\index{saving your session|bold} Isabelle provides no means of storing +theorems or internal proof objects on files. Theorems are simply part of the +\ML{} state. To save your work between sessions, you may dump the \ML{} +system state to a file. This is done automatically when ending the session +normally (e.g.\ by typing control-D), provided that the image has been opened +\emph{writable} in the first place. The standard object-logic images are +usually read-only, so you have to create a private working copy first. For +example, the following shell command puts you into a writable Isabelle session +of name \texttt{Foo} that initially contains just plain \HOL: \begin{ttbox} -isabelle FOL Foo +isabelle HOL Foo \end{ttbox} Ending the \texttt{Foo} session with control-D will cause the complete -\ML{} world to be saved somewhere in your home directory\footnote{The - default location is in \texttt{\~\relax/isabelle/heaps}, but this - depends on your local configuration.}. Make sure there is enough -space available! Then one may later continue at exactly the same point -by running +\ML-world to be saved somewhere in your home directory\footnote{The default + location is in \texttt{\~\relax/isabelle/heaps}, but this depends on your + local configuration.}. Make sure there is enough space available! Then one +may later continue at exactly the same point by running \begin{ttbox} isabelle Foo \end{ttbox} -More details about the \texttt{isabelle} command may be found in \emph{The - Isabelle System Manual}. +\medskip Saving the {\ML} state is not enough. Record, on a file, the +top-level commands that generate your theories and proofs. Such a record +allows you to replay the proofs whenever required, for instance after making +minor changes to the axioms. Ideally, your these sources will be somewhat +intelligible to others as a formal description of your work. -\medskip Saving the state is not enough. Record, on a file, the -top-level commands that generate your theories and proofs. Such a -record allows you to replay the proofs whenever required, for instance -after making minor changes to the axioms. Ideally, your record will -be somewhat intelligible to others as a formal description of your -work. +It is good practice to put all source files that constitute a separate +Isabelle session into an individual directory, together with an {\ML} file +called \texttt{ROOT.ML} that contains appropriate commands to load all other +files required. Running \texttt{isabelle} with option \texttt{-u} +automatically loads \texttt{ROOT.ML} on entering the session. The +\texttt{isatool usedir} utility provides some more options to manage your +sessions, such as automatic generation of theory browsing information. -\medskip There are more comfortable user interfaces than the -bare-bones \ML{} top-level run from a text terminal. The -\texttt{Isabelle} executable (note the capital I) runs one such -interface, depending on your local configuration. Furthermore there -are a number of external utilities available. These are started -uniformly via the \texttt{isatool} wrapper. See the \emph{System - Manual} for more information user interfaces and utilities. +\medskip More details about the \texttt{isabelle} and \texttt{isatool} +commands may be found in \emph{The Isabelle System Manual}. + +\medskip There are more comfortable user interfaces than the bare-bones \ML{} +top-level run from a text terminal. The \texttt{Isabelle} executable (note +the capital I) runs one such interface, depending on your local configuration. +Again, see \emph{The Isabelle System Manual} for more information. \section{Ending a session} @@ -139,8 +145,55 @@ 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}. Section~\ref{LoadingTheories} describes commands -for loading theory files. +\texttt{\$ISABELLE_HOME}. + + +\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 +\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 database 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 (optionally) $name$\texttt{.ML}; also + makes sure 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 parents. + +\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. + +\end{ttdescription} + +See \S\ref{sec:more-theories} for further information on Isabelle's theory +loader. \section{Setting flags} @@ -263,10 +316,9 @@ \index{error messages} \index{warnings} -Isabelle conceptually provides three output channels for different -kinds of messages: ordinary text, warnings, errors. Depending on the -user interface involved, these messages may appear in different text -styles or colours, even within separate windows. +Isabelle conceptually provides three output channels for different kinds of +messages: ordinary text, warnings, errors. Depending on the user interface +involved, these messages may appear in different text styles or colours. The default setup of an \texttt{isabelle} terminal session is as follows: plain output of ordinary text, warnings prefixed by diff -r 8338dd394144 -r b38bc78d9a9d doc-src/Ref/ref.ind --- a/doc-src/Ref/ref.ind Mon May 03 14:43:52 1999 +0200 +++ b/doc-src/Ref/ref.ind Mon May 03 18:35:48 1999 +0200 @@ -24,8 +24,9 @@ \item {\tt Abs}, \bold{62}, 88 \item {\tt abstract_over}, \bold{63} - \item {\tt abstract_rule}, \bold{48} + \item {\tt abstract_rule}, \bold{49} \item {\tt aconv}, \bold{63} + \item {\tt add_path}, \bold{59} \item {\tt addaltern}, \bold{137} \item {\tt addbefore}, \bold{137} \item {\tt Addcongs}, \bold{107} @@ -61,96 +62,96 @@ \item {\tt addSSolver}, \bold{113} \item {\tt addSWrapper}, \bold{137} \item {\tt addWrapper}, \bold{137} - \item {\tt all_tac}, \bold{33} - \item {\tt ALLGOALS}, \bold{37}, 119, 122 + \item {\tt all_tac}, \bold{34} + \item {\tt ALLGOALS}, \bold{38}, 119, 122 \item ambiguity \subitem of parsed expressions, 81 \item {\tt ancestors_of}, \bold{61} \item {\tt any} nonterminal, \bold{70} - \item {\tt APPEND}, \bold{31}, 33 - \item {\tt APPEND'}, 38 + \item {\tt APPEND}, \bold{32}, 34 + \item {\tt APPEND'}, 39 \item {\tt Appl}, 85 \item {\tt aprop} nonterminal, \bold{72} - \item {\tt ares_tac}, \bold{22} + \item {\tt ares_tac}, \bold{23} \item {\tt args} nonterminal, 95 \item {\tt Arith} theory, 121 \item arities - \subitem context conditions, 57 + \subitem context conditions, 58 \item {\tt Asm_full_simp_tac}, \bold{106} - \item {\tt asm_full_simp_tac}, 25, \bold{116}, 120 + \item {\tt asm_full_simp_tac}, 26, \bold{116}, 120 \item {\tt asm_full_simplify}, 116 - \item {\tt asm_rl} theorem, 24 + \item {\tt asm_rl} theorem, 25 \item {\tt Asm_simp_tac}, \bold{105}, 118 \item {\tt asm_simp_tac}, \bold{116}, 128 \item {\tt asm_simplify}, 116 \item associative-commutative operators, 121 - \item {\tt assume}, \bold{47} - \item {\tt assume_ax}, 9, \bold{11} - \item {\tt assume_tac}, \bold{20}, 134 - \item {\tt assumption}, \bold{50} + \item {\tt assume}, \bold{48} + \item {\tt assume_ax}, 10, \bold{12} + \item {\tt assume_tac}, \bold{21}, 134 + \item {\tt assumption}, \bold{51} \item assumptions \subitem contradictory, 142 - \subitem deleting, 25 + \subitem deleting, 26 \subitem in simplification, 105, 114 - \subitem inserting, 22 + \subitem inserting, 23 \subitem negated, 132 - \subitem of main goal, 8, 9, 11, 16, 17 + \subitem of main goal, 9, 10, 12, 17, 18 \subitem reordering, 120 - \subitem rotating, 25 + \subitem rotating, 26 \subitem substitution in, 102 - \subitem tactics for, 20 + \subitem tactics for, 21 \item ASTs, 85--90 \subitem made from parse trees, 86 \subitem made from terms, 88 - \item {\tt atac}, \bold{22} + \item {\tt atac}, \bold{23} \item {\tt Auto_tac}, \bold{142} \item {\tt auto_tac} $(cs,ss)$, \bold{139} - \item {\tt axclass} section, 56 - \item axiomatic type class, 56 + \item {\tt axclass} section, 57 + \item axiomatic type class, 57 \item axioms - \subitem extracting, 10 - \item {\tt axioms_of}, \bold{10} + \subitem extracting, 11 + \item {\tt axioms_of}, \bold{11} \indexspace - \item {\tt ba}, \bold{13} - \item {\tt back}, \bold{12} - \item batch execution, 15 - \item {\tt bd}, \bold{13} - \item {\tt bds}, \bold{13} - \item {\tt be}, \bold{13} - \item {\tt bes}, \bold{13} - \item {\tt BEST_FIRST}, \bold{34}, 35 + \item {\tt ba}, \bold{14} + \item {\tt back}, \bold{13} + \item batch execution, 16 + \item {\tt bd}, \bold{14} + \item {\tt bds}, \bold{14} + \item {\tt be}, \bold{14} + \item {\tt bes}, \bold{14} + \item {\tt BEST_FIRST}, \bold{35}, 36 \item {\tt Best_tac}, \bold{142} \item {\tt best_tac}, \bold{140} - \item {\tt beta_conversion}, \bold{48} - \item {\tt bicompose}, \bold{51} - \item {\tt bimatch_tac}, \bold{26} - \item {\tt bind_thm}, \bold{10}, 11, 41 + \item {\tt beta_conversion}, \bold{49} + \item {\tt bicompose}, \bold{52} + \item {\tt bimatch_tac}, \bold{27} + \item {\tt bind_thm}, \bold{11}, 12, 42 \item binders, \bold{80} - \item {\tt biresolution}, \bold{50} - \item {\tt biresolve_tac}, \bold{26}, 143 + \item {\tt biresolution}, \bold{51} + \item {\tt biresolve_tac}, \bold{27}, 143 \item {\tt Blast.depth_tac}, \bold{139} \item {\tt Blast.trace}, \bold{139} \item {\tt Blast_tac}, \bold{142} \item {\tt blast_tac}, \bold{138} \item {\tt Bound}, \bold{62}, 86, 88, 89 \item {\tt bound_hyp_subst_tac}, \bold{102} - \item {\tt br}, \bold{13} - \item {\tt BREADTH_FIRST}, \bold{34} - \item {\tt brs}, \bold{13} - \item {\tt bw}, \bold{14} - \item {\tt bws}, \bold{14} - \item {\tt by}, \bold{8}, 11--13, 17 - \item {\tt byev}, \bold{9} + \item {\tt br}, \bold{14} + \item {\tt BREADTH_FIRST}, \bold{35} + \item {\tt brs}, \bold{14} + \item {\tt bw}, \bold{15} + \item {\tt bws}, \bold{15} + \item {\tt by}, \bold{9}, 12--14, 18 + \item {\tt byev}, \bold{10} \indexspace \item {\tt cd}, \bold{3} \item {\tt cert_axm}, \bold{64} - \item {\tt CHANGED}, \bold{33} - \item {\tt chop}, \bold{11}, 16 - \item {\tt choplev}, \bold{12} + \item {\tt CHANGED}, \bold{34} + \item {\tt chop}, \bold{12}, 17 + \item {\tt choplev}, \bold{13} \item {\tt Clarify_step_tac}, \bold{142} \item {\tt clarify_step_tac}, \bold{139} \item {\tt Clarify_tac}, \bold{142} @@ -162,54 +163,55 @@ \item {\tt claset} ML type, 135 \item {\tt ClasimpFun}, 144 \item classes - \subitem context conditions, 57 + \subitem context conditions, 58 \item classical reasoner, 130--144 \subitem setting up, 143 \subitem tactics, 138 \item classical sets, 134 \item {\tt ClassicalFun}, 143 - \item {\tt combination}, \bold{48} - \item {\tt commit}, \bold{2} - \item {\tt COMP}, \bold{50} - \item {\tt compose}, \bold{50} - \item {\tt compose_tac}, \bold{26} - \item {\tt concl_of}, \bold{44} - \item {\tt COND}, \bold{35} + \item {\tt combination}, \bold{49} + \item {\tt commit}, \bold{3} + \item {\tt COMP}, \bold{51} + \item {\tt compose}, \bold{51} + \item {\tt compose_tac}, \bold{27} + \item {\tt concl_of}, \bold{45} + \item {\tt COND}, \bold{36} \item congruence rules, 111 \item {\tt Const}, \bold{62}, 88, 98 \item {\tt Constant}, 85, 98 \item constants, \bold{62} \subitem for translations, 75 \subitem syntactic, 90 - \item {\tt context}, 105 + \item {\tt context}, \bold{4}, 105 \item {\tt contr_tac}, \bold{142} - \item {\tt could_unify}, \bold{28} - \item {\tt cprems_of}, \bold{44} - \item {\tt cprop_of}, \bold{43} - \item {\tt CPure} theory, 54 - \item {\tt CPure.thy}, \bold{61} - \item {\tt crep_thm}, \bold{44} + \item {\tt could_unify}, \bold{29} + \item {\tt cprems_of}, \bold{45} + \item {\tt cprop_of}, \bold{44} + \item {\tt CPure} theory, 55 + \item {\tt CPure.thy}, \bold{60} + \item {\tt crep_thm}, \bold{45} \item {\tt cterm} ML type, 64 - \item {\tt cterm_instantiate}, \bold{42} - \item {\tt cterm_of}, 8, 16, \bold{64} + \item {\tt cterm_instantiate}, \bold{43} + \item {\tt cterm_of}, 9, 17, \bold{64} \item {\tt ctyp}, \bold{65} \item {\tt ctyp_of}, \bold{66} - \item {\tt cut_facts_tac}, \bold{22}, 103 - \item {\tt cut_inst_tac}, \bold{22} - \item {\tt cut_rl} theorem, 24 + \item {\tt cut_facts_tac}, \bold{23}, 103 + \item {\tt cut_inst_tac}, \bold{23} + \item {\tt cut_rl} theorem, 25 \indexspace \item {\tt datatype}, 107 \item {\tt Deepen_tac}, \bold{142} \item {\tt deepen_tac}, \bold{140} - \item {\tt defer_tac}, \bold{23} - \item definitions, \see{rewriting, meta-level}{1}, 23, \bold{57} - \subitem unfolding, 8, 9 + \item {\tt defer_tac}, \bold{24} + \item definitions, \see{rewriting, meta-level}{1}, 24, \bold{58} + \subitem unfolding, 9, 10 + \item {\tt del_path}, \bold{59} \item {\tt Delcongs}, \bold{107} \item {\tt delcongs}, \bold{112} \item {\tt deleqcongs}, \bold{112} - \item {\tt delete_tmpfiles}, \bold{58} + \item {\tt delete_tmpfiles}, \bold{59} \item delimiters, \bold{72}, 75, 76, 78 \item {\tt delloop}, \bold{114} \item {\tt delrules}, \bold{135} @@ -221,58 +223,58 @@ \item {\tt delSWrapper}, \bold{137} \item {\tt delWrapper}, \bold{137} \item {\tt dependent_tr'}, 96, \bold{98} - \item {\tt DEPTH_FIRST}, \bold{34} - \item {\tt DEPTH_SOLVE}, \bold{34} - \item {\tt DEPTH_SOLVE_1}, \bold{34} + \item {\tt DEPTH_FIRST}, \bold{35} + \item {\tt DEPTH_SOLVE}, \bold{35} + \item {\tt DEPTH_SOLVE_1}, \bold{35} \item {\tt depth_tac}, \bold{140} - \item {\tt Deriv.drop}, \bold{52} - \item {\tt Deriv.linear}, \bold{52} - \item {\tt Deriv.size}, \bold{52} - \item {\tt Deriv.tree}, \bold{52} + \item {\tt Deriv.drop}, \bold{53} + \item {\tt Deriv.linear}, \bold{53} + \item {\tt Deriv.size}, \bold{53} + \item {\tt Deriv.tree}, \bold{53} \item {\tt dest_eq}, \bold{103} \item {\tt dest_imp}, \bold{103} - \item {\tt dest_state}, \bold{44} + \item {\tt dest_state}, \bold{45} \item {\tt dest_Trueprop}, \bold{103} - \item destruct-resolution, 20 - \item {\tt DETERM}, \bold{35} - \item discrimination nets, \bold{27} - \item {\tt distinct_subgoals_tac}, \bold{25} - \item {\tt dmatch_tac}, \bold{20} + \item destruct-resolution, 21 + \item {\tt DETERM}, \bold{36} + \item discrimination nets, \bold{28} + \item {\tt distinct_subgoals_tac}, \bold{26} + \item {\tt dmatch_tac}, \bold{21} \item {\tt domain_type}, \bold{104} - \item {\tt dres_inst_tac}, \bold{21} - \item {\tt dresolve_tac}, \bold{20} - \item {\tt dtac}, \bold{22} + \item {\tt dres_inst_tac}, \bold{22} + \item {\tt dresolve_tac}, \bold{21} + \item {\tt dtac}, \bold{23} \item {\tt dummyT}, 88, 89, 99 \item duplicate subgoals - \subitem removing, 25 + \subitem removing, 26 \indexspace - \item elim-resolution, 19 - \item {\tt ematch_tac}, \bold{20} + \item elim-resolution, 20 + \item {\tt ematch_tac}, \bold{21} \item {\tt empty} constant, 94 \item {\tt empty_cs}, \bold{135} \item {\tt empty_ss}, \bold{109} - \item {\tt eq_assume_tac}, \bold{20}, 134 - \item {\tt eq_assumption}, \bold{50} + \item {\tt eq_assume_tac}, \bold{21}, 134 + \item {\tt eq_assumption}, \bold{51} \item {\tt eq_mp_tac}, \bold{142} \item {\tt eq_reflection} theorem, \bold{104}, 125 - \item {\tt eq_thm}, \bold{35} + \item {\tt eq_thm}, \bold{36} \item {\tt eq_thy}, \bold{60} - \item {\tt equal_elim}, \bold{47} - \item {\tt equal_intr}, \bold{47} + \item {\tt equal_elim}, \bold{48} + \item {\tt equal_intr}, \bold{48} \item equality, 101--104 - \item {\tt eres_inst_tac}, \bold{21} - \item {\tt eresolve_tac}, \bold{19} - \subitem on other than first premise, 43 - \item {\tt ERROR}, 5 - \item {\tt error}, 5 - \item error messages, 5 - \item {\tt eta_contract}, \bold{5}, 92 - \item {\tt etac}, \bold{22} - \item {\tt EVERY}, \bold{32} - \item {\tt EVERY'}, 38 - \item {\tt EVERY1}, \bold{39} + \item {\tt eres_inst_tac}, \bold{22} + \item {\tt eresolve_tac}, \bold{20} + \subitem on other than first premise, 44 + \item {\tt ERROR}, 6 + \item {\tt error}, 6 + \item error messages, 6 + \item {\tt eta_contract}, \bold{6}, 92 + \item {\tt etac}, \bold{23} + \item {\tt EVERY}, \bold{33} + \item {\tt EVERY'}, 39 + \item {\tt EVERY1}, \bold{40} \item examples \subitem of logic definitions, 82 \subitem of macros, 94, 95 @@ -280,56 +282,56 @@ \subitem of simplification, 117 \subitem of translations, 98 \item exceptions - \subitem printing of, 6 - \item {\tt exit}, \bold{2} - \item {\tt extensional}, \bold{48} + \subitem printing of, 7 + \item {\tt exit}, \bold{3} + \item {\tt extensional}, \bold{49} \indexspace - \item {\tt fa}, \bold{14} + \item {\tt fa}, \bold{15} \item {\tt Fast_tac}, \bold{142} \item {\tt fast_tac}, \bold{140} - \item {\tt fd}, \bold{14} - \item {\tt fds}, \bold{14} - \item {\tt fe}, \bold{14} - \item {\tt fes}, \bold{14} + \item {\tt fd}, \bold{15} + \item {\tt fds}, \bold{15} + \item {\tt fe}, \bold{15} + \item {\tt fes}, \bold{15} \item files - \subitem reading, 3, 58 - \item {\tt filt_resolve_tac}, \bold{28} - \item {\tt FILTER}, \bold{33} - \item {\tt filter_goal}, \bold{18} - \item {\tt filter_thms}, \bold{28} - \item {\tt findE}, \bold{11} - \item {\tt findEs}, \bold{11} - \item {\tt findI}, \bold{11} - \item {\tt FIRST}, \bold{32} - \item {\tt FIRST'}, 38 - \item {\tt FIRST1}, \bold{39} - \item {\tt FIRSTGOAL}, \bold{37} - \item flex-flex constraints, 25, 43, 51 - \item {\tt flexflex_rule}, \bold{51} - \item {\tt flexflex_tac}, \bold{25} + \subitem reading, 3, 59 + \item {\tt filt_resolve_tac}, \bold{29} + \item {\tt FILTER}, \bold{34} + \item {\tt filter_goal}, \bold{19} + \item {\tt filter_thms}, \bold{29} + \item {\tt findE}, \bold{12} + \item {\tt findEs}, \bold{12} + \item {\tt findI}, \bold{12} + \item {\tt FIRST}, \bold{33} + \item {\tt FIRST'}, 39 + \item {\tt FIRST1}, \bold{40} + \item {\tt FIRSTGOAL}, \bold{38} + \item flex-flex constraints, 26, 44, 52 + \item {\tt flexflex_rule}, \bold{52} + \item {\tt flexflex_tac}, \bold{26} \item {\tt FOL_basic_ss}, \bold{128} \item {\tt FOL_ss}, \bold{128} - \item {\tt fold_goals_tac}, \bold{23} - \item {\tt fold_tac}, \bold{23} - \item {\tt forall_elim}, \bold{49} - \item {\tt forall_elim_list}, \bold{49} - \item {\tt forall_elim_var}, \bold{49} - \item {\tt forall_elim_vars}, \bold{49} - \item {\tt forall_intr}, \bold{48} - \item {\tt forall_intr_frees}, \bold{49} - \item {\tt forall_intr_list}, \bold{49} - \item {\tt force_strip_shyps}, \bold{44} + \item {\tt fold_goals_tac}, \bold{24} + \item {\tt fold_tac}, \bold{24} + \item {\tt forall_elim}, \bold{50} + \item {\tt forall_elim_list}, \bold{50} + \item {\tt forall_elim_var}, \bold{50} + \item {\tt forall_elim_vars}, \bold{50} + \item {\tt forall_intr}, \bold{49} + \item {\tt forall_intr_frees}, \bold{50} + \item {\tt forall_intr_list}, \bold{50} + \item {\tt force_strip_shyps}, \bold{45} \item {\tt Force_tac}, \bold{142} \item {\tt force_tac}, \bold{139} - \item {\tt forw_inst_tac}, \bold{21} - \item forward proof, 20, 41 - \item {\tt forward_tac}, \bold{20} - \item {\tt fr}, \bold{14} + \item {\tt forw_inst_tac}, \bold{22} + \item forward proof, 21, 42 + \item {\tt forward_tac}, \bold{21} + \item {\tt fr}, \bold{15} \item {\tt Free}, \bold{62}, 88 - \item {\tt freezeT}, \bold{49} - \item {\tt frs}, \bold{14} + \item {\tt freezeT}, \bold{50} + \item {\tt frs}, \bold{15} \item {\tt Full_simp_tac}, \bold{105} \item {\tt full_simp_tac}, \bold{116} \item {\tt full_simplify}, 116 @@ -338,21 +340,22 @@ \indexspace - \item {\tt get_axiom}, \bold{10} - \item {\tt get_thm}, \bold{10} - \item {\tt get_thms}, \bold{10} - \item {\tt getgoal}, \bold{17} - \item {\tt gethyps}, \bold{18}, 37 - \item {\tt Goal}, \bold{8}, 16 - \item {\tt goal}, \bold{8} - \item {\tt goals_limit}, \bold{12} - \item {\tt Goalw}, \bold{8} - \item {\tt goalw}, \bold{8} - \item {\tt goalw_cterm}, \bold{8} + \item {\tt get_axiom}, \bold{11} + \item {\tt get_thm}, \bold{11} + \item {\tt get_thms}, \bold{11} + \item {\tt getenv}, 59 + \item {\tt getgoal}, \bold{18} + \item {\tt gethyps}, \bold{19}, 38 + \item {\tt Goal}, \bold{9}, 17 + \item {\tt goal}, \bold{9} + \item {\tt goals_limit}, \bold{13} + \item {\tt Goalw}, \bold{9} + \item {\tt goalw}, \bold{9} + \item {\tt goalw_cterm}, \bold{9} \indexspace - \item {\tt has_fewer_prems}, \bold{35} + \item {\tt has_fewer_prems}, \bold{36} \item higher-order pattern, \bold{110} \item {\tt HOL_basic_ss}, \bold{109} \item {\tt hyp_subst_tac}, \bold{102} @@ -365,26 +368,26 @@ \item identifiers, 72 \item {\tt idt} nonterminal, 92 \item {\tt idts} nonterminal, \bold{72}, 80 - \item {\tt IF_UNSOLVED}, \bold{35} + \item {\tt IF_UNSOLVED}, \bold{36} \item {\tt iff_reflection} theorem, 125 \item {\tt IFOL_ss}, \bold{128} \item {\tt imp_intr} theorem, \bold{104} - \item {\tt implies_elim}, \bold{47} - \item {\tt implies_elim_list}, \bold{47} - \item {\tt implies_intr}, \bold{47} - \item {\tt implies_intr_hyps}, \bold{47} - \item {\tt implies_intr_list}, \bold{47} + \item {\tt implies_elim}, \bold{48} + \item {\tt implies_elim_list}, \bold{48} + \item {\tt implies_intr}, \bold{48} + \item {\tt implies_intr_hyps}, \bold{48} + \item {\tt implies_intr_list}, \bold{48} \item {\tt incr_boundvars}, \bold{63}, 98 \item {\tt indexname} ML type, 62, 73 \item infixes, \bold{79} \item {\tt insert} constant, 94 \item {\tt inst_step_tac}, \bold{141} - \item {\tt instance} section, 56 - \item {\tt instantiate}, \bold{49} - \item {\tt instantiate'}, \bold{42}, 49 - \item instantiation, 21, 42, 49 - \item {\tt INTLEAVE}, \bold{31}, 33 - \item {\tt INTLEAVE'}, 38 + \item {\tt instance} section, 57 + \item {\tt instantiate}, \bold{50} + \item {\tt instantiate'}, \bold{43}, 50 + \item instantiation, 22, 43, 50 + \item {\tt INTLEAVE}, \bold{32}, 34 + \item {\tt INTLEAVE'}, 39 \item {\tt invoke_oracle}, \bold{66} \item {\tt is} nonterminal, 94 @@ -394,66 +397,65 @@ \indexspace - \item {\tt keep_derivs}, \bold{52} + \item {\tt keep_derivs}, \bold{53} \indexspace - \item $\lambda$-abstractions, 27, \bold{62} - \item $\lambda$-calculus, 46, 48, 72 - \item {\tt lessb}, \bold{27} + \item $\lambda$-abstractions, 28, \bold{62} + \item $\lambda$-calculus, 47, 49, 72 + \item {\tt lessb}, \bold{28} \item lexer, \bold{72} - \item {\tt lift_rule}, \bold{51} - \item lifting, 51 - \item {\tt loadpath}, \bold{58} + \item {\tt lift_rule}, \bold{52} + \item lifting, 52 \item {\tt logic} class, 72, 77 \item {\tt logic} nonterminal, \bold{72} - \item {\tt Logic.auto_rename}, \bold{25} - \item {\tt Logic.set_rename_prefix}, \bold{24} - \item {\tt long_names}, \bold{5} + \item {\tt Logic.auto_rename}, \bold{26} + \item {\tt Logic.set_rename_prefix}, \bold{25} + \item {\tt long_names}, \bold{6} \item {\tt loose_bnos}, \bold{63}, 99 \indexspace \item macros, 90--96 - \item {\tt make_elim}, \bold{43}, 136 + \item {\tt make_elim}, \bold{44}, 136 \item {\tt Match} exception, 97 - \item {\tt match_tac}, \bold{20}, 134 + \item {\tt match_tac}, \bold{21}, 134 \item {\tt max_pri}, 70, \bold{76} \item {\tt merge_ss}, \bold{109} \item {\tt merge_theories}, \bold{61} - \item meta-assumptions, 36, 45, 47, 50 - \subitem printing of, 4 - \item meta-equality, 46--48 - \item meta-implication, 46, 47 - \item meta-quantifiers, 46, 48 - \item meta-rewriting, 8, 14, 15, \bold{23}, + \item meta-assumptions, 37, 46, 48, 51 + \subitem printing of, 5 + \item meta-equality, 47--49 + \item meta-implication, 47, 48 + \item meta-quantifiers, 47, 49 + \item meta-rewriting, 9, 15, 16, \bold{24}, \seealso{tactics, theorems}{145} - \subitem in theorems, 42 - \item meta-rules, \see{meta-rules}{1}, 45--51 - \item {\tt METAHYPS}, 18, \bold{36} - \item mixfix declarations, 55, 75--80 + \subitem in theorems, 43 + \item meta-rules, \see{meta-rules}{1}, 46--52 + \item {\tt METAHYPS}, 19, \bold{37} + \item mixfix declarations, 56, 75--80 \item {\tt mk_atomize}, \bold{127} \item {\tt mk_simproc}, \bold{123} \item {\tt ML} section, 57, 97, 99 \item model checkers, 81 \item {\tt mp} theorem, \bold{143} \item {\tt mp_tac}, \bold{142} - \item {\tt MRL}, \bold{41} - \item {\tt MRS}, \bold{41} + \item {\tt MRL}, \bold{42} + \item {\tt MRS}, \bold{42} \indexspace \item name tokens, \bold{72} \item {\tt nat_cancel}, \bold{111} - \item {\tt net_bimatch_tac}, \bold{27} - \item {\tt net_biresolve_tac}, \bold{27} - \item {\tt net_match_tac}, \bold{27} - \item {\tt net_resolve_tac}, \bold{27} - \item {\tt no_tac}, \bold{33} - \item {\tt None}, \bold{29} - \item {\tt nonterminal} symbols, 55 + \item {\tt net_bimatch_tac}, \bold{28} + \item {\tt net_biresolve_tac}, \bold{28} + \item {\tt net_match_tac}, \bold{28} + \item {\tt net_resolve_tac}, \bold{28} + \item {\tt no_tac}, \bold{34} + \item {\tt None}, \bold{30} + \item {\tt nonterminal} symbols, 56 \item {\tt not_elim} theorem, \bold{143} - \item {\tt nprems_of}, \bold{44} + \item {\tt nprems_of}, \bold{45} \item numerals, 72 \indexspace @@ -461,151 +463,152 @@ \item {\textit {o}} type, 82 \item {\tt object}, 66 \item {\tt op} symbol, 79 - \item {\tt option} ML type, 29 + \item {\tt option} ML type, 30 \item oracles, 66--68 - \item {\tt ORELSE}, \bold{31}, 33, 37 - \item {\tt ORELSE'}, 38 + \item {\tt ORELSE}, \bold{32}, 34, 38 + \item {\tt ORELSE'}, 39 \indexspace \item parameters - \subitem removing unused, 25 - \subitem renaming, 14, 24, 51 + \subitem removing unused, 26 + \subitem renaming, 15, 25, 52 \item {\tt parents_of}, \bold{61} \item parse trees, 85 \item {\tt parse_rules}, 92 \item pattern, higher-order, \bold{110} - \item {\tt pause_tac}, \bold{29} - \item Poly/{\ML} compiler, 6 - \item {\tt pop_proof}, \bold{16} - \item {\tt pr}, \bold{12} - \item {\tt premises}, \bold{8}, 16 - \item {\tt prems_of}, \bold{44} + \item {\tt pause_tac}, \bold{30} + \item Poly/{\ML} compiler, 7 + \item {\tt pop_proof}, \bold{17} + \item {\tt pr}, \bold{13} + \item {\tt premises}, \bold{9}, 17 + \item {\tt prems_of}, \bold{45} \item {\tt prems_of_ss}, \bold{113} \item pretty printing, 76, 78--79, 95 - \item {\tt Pretty.setdepth}, \bold{4} - \item {\tt Pretty.setmargin}, \bold{4} - \item {\tt PRIMITIVE}, \bold{28} + \item {\tt Pretty.setdepth}, \bold{5} + \item {\tt Pretty.setmargin}, \bold{5} + \item {\tt PRIMITIVE}, \bold{29} \item {\tt primrec}, 107 - \item {\tt prin}, 6, \bold{17} - \item print mode, 55, 99 + \item {\tt prin}, 7, \bold{18} + \item print mode, 56, 99 \item print modes, 80--81 \item {\tt print_cs}, \bold{135} - \item {\tt print_depth}, \bold{4} - \item {\tt print_exn}, \bold{6}, 40 - \item {\tt print_goals}, \bold{41} + \item {\tt print_depth}, \bold{5} + \item {\tt print_exn}, \bold{7}, 41 + \item {\tt print_goals}, \bold{42} \item {\tt print_mode}, 80 \item {\tt print_modes}, 75 \item {\tt print_rules}, 92 \item {\tt print_simpset}, \bold{109} \item {\tt print_ss}, \bold{108} \item {\tt print_syntax}, \bold{61}, \bold{74} - \item {\tt print_tac}, \bold{29} + \item {\tt print_tac}, \bold{30} \item {\tt print_theory}, \bold{61} - \item {\tt print_thm}, \bold{41} - \item printing control, 3--5 - \item {\tt printyp}, \bold{17} + \item {\tt print_thm}, \bold{42} + \item printing control, 4--6 + \item {\tt printyp}, \bold{18} \item priorities, 69, \bold{76} \item priority grammars, 69--70 - \item {\tt prlev}, \bold{12} - \item {\tt prlim}, \bold{12} + \item {\tt prlev}, \bold{13} + \item {\tt prlim}, \bold{13} \item productions, 69, 75, 76 \subitem copy, \bold{75}, 76, 87 - \item {\tt proof} ML type, 17 - \item proof objects, 51--53 - \item proof state, 7 - \subitem printing of, 12 - \item {\tt proof_timing}, \bold{13} - \item proofs, 7--18 - \subitem inspecting the state, 17 - \subitem managing multiple, 16 - \subitem saving and restoring, 17 - \subitem stacking, 16 - \subitem starting, 7 - \subitem timing, 13 + \item {\tt proof} ML type, 18 + \item proof objects, 52--54 + \item proof state, 8 + \subitem printing of, 13 + \item {\tt proof_timing}, \bold{14} + \item proofs, 8--19 + \subitem inspecting the state, 18 + \subitem managing multiple, 17 + \subitem saving and restoring, 18 + \subitem stacking, 17 + \subitem starting, 8 + \subitem timing, 14 \item {\tt PROP} symbol, 71 \item {\textit {prop}} type, 65, 72 \item {\tt prop} nonterminal, \bold{70}, 82 - \item {\tt ProtoPure.thy}, \bold{61} - \item {\tt prove_goal}, 13, \bold{15} - \item {\tt prove_goalw}, \bold{15} - \item {\tt prove_goalw_cterm}, \bold{15} - \item {\tt prth}, \bold{40} - \item {\tt prthq}, \bold{41} - \item {\tt prths}, \bold{41} - \item {\tt prune_params_tac}, \bold{25} + \item {\tt ProtoPure.thy}, \bold{60} + \item {\tt prove_goal}, 14, \bold{16} + \item {\tt prove_goalw}, \bold{16} + \item {\tt prove_goalw_cterm}, \bold{16} + \item {\tt prth}, \bold{41} + \item {\tt prthq}, \bold{42} + \item {\tt prths}, \bold{42} + \item {\tt prune_params_tac}, \bold{26} \item {\tt pttrn} nonterminal, \bold{72} \item {\tt pttrns} nonterminal, \bold{72} - \item {\tt Pure} theory, 54, 70, 74 - \item {\tt Pure.thy}, \bold{61} - \item {\tt push_proof}, \bold{16} + \item {\tt Pure} theory, 55, 70, 74 + \item {\tt Pure.thy}, \bold{60} + \item {\tt push_proof}, \bold{17} \item {\tt pwd}, \bold{3} \indexspace - \item {\tt qed}, \bold{9}, 11 - \item {\tt qed_goal}, \bold{15} - \item {\tt qed_goalw}, \bold{15} + \item {\tt qed}, \bold{10}, 12 + \item {\tt qed_goal}, \bold{16} + \item {\tt qed_goalw}, \bold{16} \item quantifiers, 80 - \item {\tt quit}, \bold{2} + \item {\tt quit}, \bold{3} \indexspace - \item {\tt read}, \bold{17} + \item {\tt read}, \bold{18} \item {\tt read_axm}, \bold{64} \item {\tt read_cterm}, \bold{64} - \item {\tt read_instantiate}, \bold{42} - \item {\tt read_instantiate_sg}, \bold{42} + \item {\tt read_instantiate}, \bold{43} + \item {\tt read_instantiate_sg}, \bold{43} \item reading - \subitem axioms, \see{{\tt assume_ax}}{54} - \subitem goals, \see{proofs, starting}{7} - \item {\tt reflexive}, \bold{48} - \item {\tt ren}, \bold{14} - \item {\tt rename_last_tac}, \bold{24} - \item {\tt rename_params_rule}, \bold{51} - \item {\tt rename_tac}, \bold{24} + \subitem axioms, \see{{\tt assume_ax}}{55} + \subitem goals, \see{proofs, starting}{8} + \item {\tt reflexive}, \bold{49} + \item {\tt ren}, \bold{15} + \item {\tt rename_last_tac}, \bold{25} + \item {\tt rename_params_rule}, \bold{52} + \item {\tt rename_tac}, \bold{25} \item {\tt rep_cs}, \bold{135} - \item {\tt rep_cterm}, \bold{65} + \item {\tt rep_cterm}, \bold{64} \item {\tt rep_ctyp}, \bold{66} \item {\tt rep_ss}, \bold{108} - \item {\tt rep_thm}, \bold{44} - \item {\tt REPEAT}, \bold{32, 33} - \item {\tt REPEAT1}, \bold{32} - \item {\tt REPEAT_DETERM}, \bold{32} - \item {\tt REPEAT_FIRST}, \bold{38} - \item {\tt REPEAT_SOME}, \bold{37} - \item {\tt res_inst_tac}, \bold{21}, 25, 26 + \item {\tt rep_thm}, \bold{45} + \item {\tt REPEAT}, \bold{33, 34} + \item {\tt REPEAT1}, \bold{33} + \item {\tt REPEAT_DETERM}, \bold{33} + \item {\tt REPEAT_FIRST}, \bold{39} + \item {\tt REPEAT_SOME}, \bold{38} + \item {\tt res_inst_tac}, \bold{22}, 26, 27 \item reserved words, 72, 95 - \item {\tt reset}, 3 - \item resolution, 41, 50 - \subitem tactics, 19 - \subitem without lifting, 50 - \item {\tt resolve_tac}, \bold{19}, 134 - \item {\tt restore_proof}, \bold{17} - \item {\tt result}, \bold{9}, 11, 17 + \item {\tt reset}, 4 + \item {\tt reset_path}, \bold{60} + \item resolution, 42, 51 + \subitem tactics, 20 + \subitem without lifting, 51 + \item {\tt resolve_tac}, \bold{20}, 134 + \item {\tt restore_proof}, \bold{18} + \item {\tt result}, \bold{10}, 12, 18 \item {\tt rev_mp} theorem, \bold{104} \item rewrite rules, 110 \subitem permutative, 120--123 - \item {\tt rewrite_goals_rule}, \bold{42} - \item {\tt rewrite_goals_tac}, \bold{23}, 42 - \item {\tt rewrite_rule}, \bold{42} - \item {\tt rewrite_tac}, 9, \bold{23} + \item {\tt rewrite_goals_rule}, \bold{43} + \item {\tt rewrite_goals_tac}, \bold{24}, 43 + \item {\tt rewrite_rule}, \bold{43} + \item {\tt rewrite_tac}, 10, \bold{24} \item rewriting \subitem object-level, \see{simplification}{1} \subitem ordered, 121 \subitem syntactic, 90--96 - \item {\tt rewtac}, \bold{22} - \item {\tt RL}, \bold{41} - \item {\tt RLN}, \bold{41} - \item {\tt rotate_prems}, \bold{43} - \item {\tt rotate_proof}, \bold{16} - \item {\tt rotate_tac}, \bold{25} - \item {\tt RS}, \bold{41} - \item {\tt RSN}, \bold{41} - \item {\tt rtac}, \bold{22} - \item {\tt rule_by_tactic}, 25, \bold{43} + \item {\tt rewtac}, \bold{23} + \item {\tt RL}, \bold{42} + \item {\tt RLN}, \bold{42} + \item {\tt rotate_prems}, \bold{44} + \item {\tt rotate_proof}, \bold{17} + \item {\tt rotate_tac}, \bold{26} + \item {\tt RS}, \bold{42} + \item {\tt RSN}, \bold{42} + \item {\tt rtac}, \bold{23} + \item {\tt rule_by_tactic}, 26, \bold{44} \item rules - \subitem converting destruction to elimination, 43 + \subitem converting destruction to elimination, 44 \indexspace @@ -614,16 +617,16 @@ \item {\tt safe_step_tac}, 136, \bold{141} \item {\tt Safe_tac}, \bold{142} \item {\tt safe_tac}, \bold{141} - \item {\tt save_proof}, \bold{17} - \item saving your work, \bold{1} - \item search, 31 - \subitem tacticals, 33--35 - \item {\tt SELECT_GOAL}, 23, \bold{36} - \item {\tt Seq.seq} ML type, 28 - \item sequences (lazy lists), \bold{29} + \item {\tt save_proof}, \bold{18} + \item saving your session, \bold{2} + \item search, 32 + \subitem tacticals, 34--36 + \item {\tt SELECT_GOAL}, 24, \bold{37} + \item {\tt Seq.seq} ML type, 29 + \item sequences (lazy lists), \bold{30} \item sequent calculus, 131 - \item sessions, 1--6 - \item {\tt set}, 3 + \item sessions, 1--7 + \item {\tt set}, 4 \item {\tt setloop}, \bold{114} \item {\tt setmksimps}, 110, \bold{126}, 128 \item {\tt setSolver}, \bold{113}, 128 @@ -632,25 +635,26 @@ \item {\tt settermless}, \bold{121} \item {\tt setup} \subitem simplifier, 129 - \subitem theory, 56 + \subitem theory, 57 \item shortcuts - \subitem for \texttt{by} commands, 13 - \subitem for tactics, 22 - \item {\tt show_brackets}, \bold{4} - \item {\tt show_consts}, \bold{5} - \item {\tt show_hyps}, \bold{4} - \item {\tt show_sorts}, \bold{4}, 89, 97 - \item {\tt show_tags}, \bold{4} - \item {\tt show_types}, \bold{4}, 89, 92, 99 - \item {\tt Sign.certify_term}, \bold{65} + \subitem for \texttt{by} commands, 14 + \subitem for tactics, 23 + \item {\tt show_brackets}, \bold{5} + \item {\tt show_consts}, \bold{6} + \item {\tt show_hyps}, \bold{5} + \item {\tt show_path}, \bold{59} + \item {\tt show_sorts}, \bold{5}, 89, 97 + \item {\tt show_tags}, \bold{5} + \item {\tt show_types}, \bold{5}, 89, 92, 99 + \item {\tt Sign.certify_term}, \bold{64} \item {\tt Sign.certify_typ}, \bold{66} - \item {\tt Sign.sg} ML type, 54 - \item {\tt Sign.stamp_names_of}, \bold{62} + \item {\tt Sign.sg} ML type, 55 + \item {\tt Sign.stamp_names_of}, \bold{61} \item {\tt Sign.string_of_term}, \bold{64} - \item {\tt Sign.string_of_typ}, \bold{66} - \item {\tt sign_of}, 8, 16, \bold{62} - \item {\tt sign_of_thm}, \bold{44} - \item signatures, \bold{54}, 62, 64, 66 + \item {\tt Sign.string_of_typ}, \bold{65} + \item {\tt sign_of}, 9, 17, \bold{61} + \item {\tt sign_of_thm}, \bold{45} + \item signatures, \bold{55}, 61, 63, 64, 66 \item {\tt Simp_tac}, \bold{105} \item {\tt simp_tac}, \bold{116} \item simplification, 105--129 @@ -676,36 +680,36 @@ \item {\tt simpset_of}, \bold{109} \item {\tt simpset_ref}, \bold{109} \item {\tt simpset_ref_of}, \bold{109} - \item {\tt size_of_thm}, 34, \bold{35}, 143 + \item {\tt size_of_thm}, 35, \bold{36}, 143 \item {\tt sizef}, \bold{143} \item {\tt slow_best_tac}, \bold{140} \item {\tt slow_step_tac}, 136, \bold{141} \item {\tt slow_tac}, \bold{140} - \item {\tt SOLVE}, \bold{35} - \item {\tt Some}, \bold{29} - \item {\tt SOMEGOAL}, \bold{37} + \item {\tt SOLVE}, \bold{36} + \item {\tt Some}, \bold{30} + \item {\tt SOMEGOAL}, \bold{38} \item {\tt sort} nonterminal, \bold{72} \item sort constraints, 71 - \item sort hypotheses, 44, 46 + \item sort hypotheses, 45, 47 \item sorts - \subitem printing of, 4 + \subitem printing of, 5 \item {\tt ssubst} theorem, \bold{101} \item {\tt stac}, \bold{102} - \item stamps, \bold{54}, 62 - \item {\tt standard}, \bold{43} + \item stamps, \bold{55}, 61 + \item {\tt standard}, \bold{44} \item starting up, \bold{1} \item {\tt Step_tac}, \bold{142} \item {\tt step_tac}, 136, \bold{141} - \item {\tt store_thm}, \bold{10} + \item {\tt store_thm}, \bold{11} \item {\tt string_of_cterm}, \bold{64} - \item {\tt string_of_ctyp}, \bold{66} - \item {\tt string_of_thm}, \bold{41} + \item {\tt string_of_ctyp}, \bold{65} + \item {\tt string_of_thm}, \bold{42} \item strings, 72 - \item {\tt SUBGOAL}, \bold{28} - \item subgoal module, 7--18 - \item {\tt subgoal_tac}, \bold{22} - \item {\tt subgoals_of_brl}, \bold{26} - \item {\tt subgoals_tac}, \bold{23} + \item {\tt SUBGOAL}, \bold{29} + \item subgoal module, 8--19 + \item {\tt subgoal_tac}, \bold{23} + \item {\tt subgoals_of_brl}, \bold{27} + \item {\tt subgoals_tac}, \bold{24} \item {\tt subst} theorem, 101, \bold{104} \item substitution \subitem rules, 101 @@ -714,12 +718,12 @@ \item {\tt swap_res_tac}, \bold{143} \item {\tt swapify}, \bold{143} \item {\tt sym} theorem, 102, \bold{104} - \item {\tt symmetric}, \bold{48} + \item {\tt symmetric}, \bold{49} \item {\tt syn_of}, \bold{74} \item syntax \subitem Pure, 70--75 \subitem transformations, 85--99 - \item {\tt syntax} section, 55 + \item {\tt syntax} section, 56 \item {\tt Syntax.ast} ML type, 85 \item {\tt Syntax.mark_boundT}, 99 \item {\tt Syntax.print_gram}, \bold{74} @@ -733,118 +737,118 @@ \indexspace - \item {\tt tactic} ML type, 19 - \item tacticals, 31--39 - \subitem conditional, 35 - \subitem deterministic, 35 - \subitem for filtering, 33 - \subitem for restriction to a subgoal, 36 - \subitem identities for, 32 - \subitem joining a list of tactics, 32 - \subitem joining tactic functions, 38 - \subitem joining two tactics, 31 - \subitem repetition, 32 - \subitem scanning for subgoals, 37 - \subitem searching, 34 - \item tactics, 19--30 - \subitem assumption, \bold{20}, 22 - \subitem commands for applying, 8 - \subitem debugging, 17 - \subitem filtering results of, 33 - \subitem for composition, 26 + \item {\tt tactic} ML type, 20 + \item tacticals, 32--40 + \subitem conditional, 36 + \subitem deterministic, 36 + \subitem for filtering, 34 + \subitem for restriction to a subgoal, 37 + \subitem identities for, 33 + \subitem joining a list of tactics, 33 + \subitem joining tactic functions, 39 + \subitem joining two tactics, 32 + \subitem repetition, 33 + \subitem scanning for subgoals, 38 + \subitem searching, 35 + \item tactics, 20--31 + \subitem assumption, \bold{21}, 23 + \subitem commands for applying, 9 + \subitem debugging, 18 + \subitem filtering results of, 34 + \subitem for composition, 27 \subitem for contradiction, 142 - \subitem for inserting facts, 22 + \subitem for inserting facts, 23 \subitem for Modus Ponens, 142 - \subitem instantiation, 21 - \subitem matching, 20 - \subitem meta-rewriting, 22, \bold{23} - \subitem primitives for coding, 28 - \subitem resolution, \bold{19}, 22, 26, 27 - \subitem restricting to a subgoal, 36 + \subitem instantiation, 22 + \subitem matching, 21 + \subitem meta-rewriting, 23, \bold{24} + \subitem primitives for coding, 29 + \subitem resolution, \bold{20}, 23, 27, 28 + \subitem restricting to a subgoal, 37 \subitem simplification, 115 \subitem substitution, 101--104 - \subitem tracing, 29 + \subitem tracing, 30 \item {\tt TERM}, 64 \item {\tt term} ML type, 62, 88 \item terms, \bold{62} - \subitem certified, \bold{64} + \subitem certified, \bold{63} \subitem made from ASTs, 88 - \subitem printing of, 17, 64 - \subitem reading of, 17 + \subitem printing of, 18, 64 + \subitem reading of, 18 \item {\tt TFree}, \bold{65} - \item {\tt THEN}, \bold{31}, 33, 37 - \item {\tt THEN'}, 38 - \item {\tt THEN_BEST_FIRST}, \bold{34} - \item theorems, 40--53 - \subitem equality of, 35 - \subitem extracting, 10 - \subitem extracting proved, 9 - \subitem joining by resolution, 41 - \subitem of pure theory, 24 - \subitem printing of, 40 - \subitem retrieving, 11 - \subitem size of, 35 - \subitem standardizing, 43 - \subitem storing, 10 - \subitem taking apart, 43 - \item theories, 54--68 - \subitem axioms of, 10 - \subitem constructing, \bold{61} + \item {\tt the_context}, \bold{4} + \item {\tt THEN}, \bold{32}, 34, 38 + \item {\tt THEN'}, 39 + \item {\tt THEN_BEST_FIRST}, \bold{35} + \item theorems, 41--54 + \subitem equality of, 36 + \subitem extracting, 11 + \subitem extracting proved, 10 + \subitem joining by resolution, 42 + \subitem of pure theory, 25 + \subitem printing of, 41 + \subitem retrieving, 12 + \subitem size of, 36 + \subitem standardizing, 44 + \subitem storing, 11 + \subitem taking apart, 44 + \item theories, 55--68 + \subitem axioms of, 11 + \subitem constructing, \bold{60} \subitem inspecting, \bold{61} - \subitem loading, 58 - \subitem parent, \bold{54} - \subitem pseudo, \bold{59} - \subitem reloading, \bold{59} - \subitem removing, \bold{59} - \subitem theorems of, 10 - \item {\tt THEORY} exception, 10, 54 - \item {\tt theory} ML type, 54 + \subitem parent, \bold{55} + \subitem reading, 3, 59 + \subitem theorems of, 11 + \item {\tt THEORY} exception, 11, 55 + \item {\tt theory}, \bold{4} + \item {\tt theory} ML type, 55 \item {\tt Theory.add_oracle}, \bold{66} - \item {\tt theory_of_thm}, \bold{44} + \item {\tt theory_of_thm}, \bold{45} \item {\tt thin_refl} theorem, \bold{104} - \item {\tt thin_tac}, \bold{25} - \item {\tt THM} exception, 40, 41, 45, 50 - \item {\tt thm}, \bold{10} - \item {\tt thm} ML type, 40 - \item {\tt thms}, \bold{10} - \item {\tt thms_containing}, \bold{11} - \item {\tt thms_of}, \bold{10} + \item {\tt thin_tac}, \bold{26} + \item {\tt THM} exception, 41, 42, 46, 51 + \item {\tt thm}, \bold{11} + \item {\tt thm} ML type, 41 + \item {\tt thms}, \bold{11} + \item {\tt thms_containing}, \bold{12} + \item {\tt thms_of}, \bold{11} \item {\tt tid} nonterminal, \bold{72}, 86, 93 \item {\tt time_use}, \bold{3} - \item {\tt time_use_thy}, \bold{58} - \item timing statistics, 13 - \item {\tt toggle}, 3 + \item {\tt time_use_thy}, \bold{4} + \item timing statistics, 14 + \item {\tt toggle}, 4 \item token class, 99 \item token translations, 99--100 \item token_translation, 100 \item {\tt token_translation}, 100 - \item {\tt topthm}, \bold{17} - \item {\tt tpairs_of}, \bold{44} - \item {\tt trace_BEST_FIRST}, \bold{34} - \item {\tt trace_DEPTH_FIRST}, \bold{34} - \item {\tt trace_goalno_tac}, \bold{38} - \item {\tt trace_REPEAT}, \bold{32} + \item {\tt topthm}, \bold{18} + \item {\tt touch_thy}, \bold{59} + \item {\tt tpairs_of}, \bold{45} + \item {\tt trace_BEST_FIRST}, \bold{35} + \item {\tt trace_DEPTH_FIRST}, \bold{35} + \item {\tt trace_goalno_tac}, \bold{39} + \item {\tt trace_REPEAT}, \bold{33} \item {\tt trace_simp}, \bold{106}, 118 \item tracing \subitem of classical prover, 139 \subitem of macros, 94 - \subitem of searching tacticals, 34 + \subitem of searching tacticals, 35 \subitem of simplification, 107, 118--119 - \subitem of tactics, 29 - \subitem of unification, 45 + \subitem of tactics, 30 + \subitem of unification, 46 \item {\tt transfer}, \bold{60} \item {\tt transfer_sg}, \bold{60} - \item {\tt transitive}, \bold{48} + \item {\tt transitive}, \bold{49} \item translations, 96--99 \subitem parse, 80, 88 \subitem parse AST, \bold{86}, 87 \subitem print, 80 \subitem print AST, \bold{89} \item {\tt translations} section, 91 - \item {\tt trivial}, \bold{51} + \item {\tt trivial}, \bold{52} \item {\tt Trueprop} constant, 82 - \item {\tt TRY}, \bold{32, 33} - \item {\tt TRYALL}, \bold{37} + \item {\tt TRY}, \bold{33, 34} + \item {\tt TRYALL}, \bold{38} \item {\tt TVar}, \bold{65} \item {\tt tvar} nonterminal, \bold{72, 73}, 86, 93 \item {\tt typ} ML type, 65 @@ -854,23 +858,23 @@ \item type constraints, 72, 80, 89 \item type constructors, \bold{65} \item type identifiers, 72 - \item type synonyms, \bold{55} + \item type synonyms, \bold{56} \item type unknowns, \bold{65}, 72 - \subitem freezing/thawing of, 49 + \subitem freezing/thawing of, 50 \item type variables, \bold{65} \item types, \bold{65} \subitem certified, \bold{65} - \subitem printing of, 4, 17, 65 + \subitem printing of, 5, 18, 65 \indexspace - \item {\tt undo}, 7, \bold{12}, 16 + \item {\tt undo}, 8, \bold{13}, 17 \item unknowns, \bold{62}, 72 - \item {\tt unlink_thy}, \bold{59} - \item {\tt update}, \bold{59} - \item {\tt uresult}, \bold{9}, 11, 17 + \item {\tt update_thy}, \bold{59} + \item {\tt uresult}, \bold{10}, 12, 18 \item {\tt use}, \bold{3} - \item {\tt use_thy}, \bold{58} + \item {\tt use_thy}, \bold{4} + \item {\tt use_thy_only}, \bold{59} \indexspace @@ -881,13 +885,13 @@ \subitem bound, \bold{62} \subitem free, \bold{62} \item {\tt variant_abs}, \bold{63} - \item {\tt varifyT}, \bold{49} + \item {\tt varifyT}, \bold{50} \indexspace - \item {\tt warning}, 5 - \item warnings, 5 - \item {\tt writeln}, 5 + \item {\tt warning}, 6 + \item warnings, 6 + \item {\tt writeln}, 6 \indexspace @@ -896,6 +900,6 @@ \indexspace - \item {\tt zero_var_indexes}, \bold{43} + \item {\tt zero_var_indexes}, \bold{44} \end{theindex} diff -r 8338dd394144 -r b38bc78d9a9d doc-src/Ref/ref.tex --- a/doc-src/Ref/ref.tex Mon May 03 14:43:52 1999 +0200 +++ b/doc-src/Ref/ref.tex Mon May 03 18:35:48 1999 +0200 @@ -2,7 +2,7 @@ \usepackage{graphicx,a4,../iman,../extra,../proof,../rail,../pdfsetup} %% $Id$ -%%\includeonly{} +%\includeonly{introduction} %%% to index ids: \[\\tt \([a-zA-Z0-9][a-zA-Z0-9_'.]*\) [\\ttindexbold{\1} %%% to delete old ones: \\indexbold{\*[^}]*} %% run sedindex ref to prepare index file diff -r 8338dd394144 -r b38bc78d9a9d doc-src/Ref/theories.tex --- a/doc-src/Ref/theories.tex Mon May 03 14:43:52 1999 +0200 +++ b/doc-src/Ref/theories.tex Mon May 03 18:35:48 1999 +0200 @@ -33,16 +33,12 @@ Appendix~\ref{app:TheorySyntax} presents the concrete syntax for theory definitions; here is an explanation of the constituent parts: \begin{description} -\item[{\it theoryDef}] is the full definition. The new theory is - called $id$. It is the union of the named {\bf parent +\item[{\it theoryDef}] is the full definition. The new theory is called $id$. + It is the union of the named {\bf parent theories}\indexbold{theories!parent}, possibly extended with new - components. \thydx{Pure} and \thydx{CPure} are the basic theories, - which contain only the meta-logic. They differ just in their - concrete syntax for function applications. - - Normally each {\it name\/} is an identifier, the name of the parent theory. - Quoted strings can be used to document additional file dependencies; see - \S\ref{LoadingTheories} for details. + components. \thydx{Pure} and \thydx{CPure} are the basic theories, which + contain only the meta-logic. They differ just in their concrete syntax for + function applications. \item[$classes$] is a series of class declarations. Declaring {\tt$id$ < $id@1$ \dots\ @@ -231,143 +227,75 @@ \end{itemize} -\section{Loading a new theory}\label{LoadingTheories} -\index{theories!loading}\index{files!reading} +\section{The theory loader}\label{sec:more-theories} +\index{theories!reading}\index{files!reading} + +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 : string -> unit -time_use_thy : string -> unit -loadpath : string list ref \hfill{\bf initially {\tt["."]}} +use_thy_only : string -> unit +update_thy : string -> unit +touch_thy : string -> unit delete_tmpfiles : bool ref \hfill{\bf initially true} \end{ttbox} \begin{ttdescription} -\item[\ttindexbold{use_thy} $thyname$] - reads the theory $thyname$ and creates an \ML{} structure as described below. - -\item[\ttindexbold{time_use_thy} $thyname$] - calls {\tt use_thy} $thyname$ and reports the time taken. - -\item[\ttindexbold{loadpath}] - contains a list of directories to search when locating the files that - define a theory. This list is only used if the theory name in {\tt - use_thy} does not specify the path explicitly. - -\item[reset \ttindexbold{delete_tmpfiles};] -suppresses the deletion of temporary files. +\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} $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 $name$ itself its parents may be reloaded as well. + +\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[reset \ttindexbold{delete_tmpfiles};] processing theory files usually + involves temporary {\ML} files to be created. By default, these are deleted + afterwards. Resetting the \texttt{delete_tmpfiles} flag inhibits this, + leaving the generated code for debugging purposes. The basic location for + temporary files is determined by the \texttt{ISABELLE_TMP} environment + variable, which is private to the running Isabelle process (it may be + retrieved by \ttindex{getenv} from {\ML}). \end{ttdescription} -% -Each theory definition must reside in a separate file. Let the file -{\it T}{\tt.thy} contain the definition of a theory called~$T$, whose -parent theories are $TB@1$ \dots $TB@n$. Calling -\texttt{use_thy}~{\tt"{\it T\/}"} reads the file {\it T}{\tt.thy}, -writes a temporary \ML{} file {\tt.{\it T}.thy.ML}, and reads the -latter file. Recursive {\tt use_thy} calls load those parent theories -that have not been loaded previously; the recursive calls may continue -to any depth. One {\tt use_thy} call can read an entire logic -provided all theories are linked appropriately. - -The result is an \ML\ structure~$T$ containing at least a component -{\tt thy} for the new theory and components for each of the rules. -The structure also contains the definitions of the {\tt ML} section, -if present. The file {\tt.{\it T}.thy.ML} is then deleted if {\tt - delete_tmpfiles} is set and no errors occurred. -Finally the file {\it T}{\tt.ML} is read, if it exists. The structure -$T$ is automatically open in this context. Proof scripts typically -refer to its components by unqualified names. +\medskip Theory and {\ML} files are located by skimming through the +directories listed in Isabelle's internal load path, which merely contains the +current directory ``\texttt{.}'' by default. The load path may be accessed by +the following operations. -Some applications construct theories directly by calling \ML\ functions. In -this situation there is no {\tt.thy} file, only an {\tt.ML} file. The -{\tt.ML} file must declare an \ML\ structure having the theory's name and a -component {\tt thy} containing the new theory object. -Section~\ref{sec:pseudo-theories} below describes a way of linking such -theories to their parents. - - -\section{Reloading modified theories}\label{sec:reloading-theories} -\indexbold{theories!reloading} \begin{ttbox} -update : unit -> unit -unlink_thy : string -> unit +show_path: unit -> string list +add_path: string -> unit +del_path: string -> unit +reset_path: unit -> unit \end{ttbox} -Changing a theory on disk often makes it necessary to reload all theories -descended from it. However, {\tt use_thy} reads only one theory, even if -some of the parent theories are out of date. In this case you should call -{\tt update()}. - -Isabelle keeps track of all loaded theories and their files. If -\texttt{use_thy} finds that the theory to be loaded has been read -before, it determines whether to reload the theory as follows. First -it looks for the theory's files in their previous location. If it -finds them, it compares their modification times to the internal data -and stops if they are equal. If the files have been moved, {\tt - use_thy} searches for them as it would for a new theory. After {\tt - use_thy} reloads a theory, it marks the children as out-of-date. \begin{ttdescription} -\item[\ttindexbold{update}()] - reloads all modified theories and their descendants in the correct order. - -\item[\ttindexbold{unlink_thy} $thyname$]\indexbold{theories!removing} - informs Isabelle that theory $thyname$ no longer exists. If you delete the - theory files for $thyname$ then you must execute {\tt unlink_thy}; - otherwise {\tt update} will complain about a missing file. +\item[\ttindexbold{show_path}();] displays the load path components in + canonical string representation, which is always according to Unix rules. + +\item[\ttindexbold{add_path} $dir$;] adds component $dir$ to the beginning of + the load path. + +\item[\ttindexbold{del_path} $dir$;] removes any occurrences of component + $dir$ from the load path. + +\item[\ttindexbold{reset_path}();] resets the load path to ``\texttt{.}'' + (current directory) only. \end{ttdescription} - -\subsection{*Pseudo theories}\label{sec:pseudo-theories} -\indexbold{theories!pseudo}% -Any automatic reloading facility requires complete knowledge of all -dependencies. Sometimes theories depend on objects created in \ML{} files -with no associated theory definition file. These objects may be theories but -they could also be theorems, proof procedures, etc. - -Unless such dependencies are documented, {\tt update} fails to reload these -\ML{} files and the system is left in a state where some objects, such as -theorems, still refer to old versions of theories. This may lead to the -error -\begin{ttbox} -Attempt to merge different versions of theories: \dots -\end{ttbox} -Therefore there is a way to link theories and {\bf orphaned} \ML{} files --- -those not associated with a theory definition. - -Let us assume we have an orphaned \ML{} file named {\tt orphan.ML} and a -theory~$B$ that depends on {\tt orphan.ML} --- for example, {\tt B.ML} uses -theorems proved in {\tt orphan.ML}. Then {\tt B.thy} should -mention this dependency as follows: -\begin{ttbox} -B = \(\ldots\) + "orphan" + \(\ldots\) -\end{ttbox} -Quoted strings stand for theories which have to be loaded before the -current theory is read but which are not used in building the base of -theory~$B$. Whenever {\tt orphan} changes and is reloaded, Isabelle -knows that $B$ has to be updated, too. - -Note that it's necessary for {\tt orphan} to declare a special ML -object of type {\tt theory} which is present in all theories. This is -normally achieved by adding the file {\tt orphan.thy} to make {\tt -orphan} a {\bf pseudo theory}. A minimum version of {\tt orphan.thy} -would be - -\begin{ttbox} -orphan = Pure -\end{ttbox} - -which uses {\tt Pure} to make a dummy theory. Normally though the -orphaned file has its own dependencies. If {\tt orphan.ML} depends on -theories or files $A@1$, \ldots, $A@n$, record this by creating the -pseudo theory in the following way: -\begin{ttbox} -orphan = \(A@1\) + \(\ldots\) + \(A@n\) -\end{ttbox} -The resulting theory ensures that {\tt update} reloads {\tt orphan} -whenever it reloads one of the $A@i$. - -For an extensive example of how this technique can be used to link -lots of theory files and load them by just a few {\tt use_thy} calls -see the sources of one of the major object-logics (e.g.\ \ZF). - +In operations referring indirectly to some file, such as +\texttt{use_thy}~$name$, the argument may be prefixed by some directory that +will be used as temporary load path. Note that, depending on which parts of +the ancestry of $name$ are already loaded, the dynamic change of paths might +be hard to predict. Use this feature with care only. \section{Basic operations on theories}\label{BasicOperationsOnTheories}