1.1 --- a/doc-src/Ref/classical.tex Mon May 05 21:18:01 1997 +0200
1.2 +++ b/doc-src/Ref/classical.tex Tue May 06 12:50:16 1997 +0200
1.3 @@ -3,10 +3,11 @@
1.4 \index{classical reasoner|(}
1.5 \newcommand\ainfer[2]{\begin{array}{r@{\,}l}#2\\ \hline#1\end{array}}
1.6
1.7 -Although Isabelle is generic, many users will be working in some extension
1.8 -of classical first-order logic. Isabelle's set theory~{\tt ZF} is built
1.9 -upon theory~{\tt FOL}, while higher-order logic contains first-order logic
1.10 -as a fragment. Theorem-proving in predicate logic is undecidable, but many
1.11 +Although Isabelle is generic, many users will be working in some
1.12 +extension of classical first-order logic. Isabelle's set theory~{\tt
1.13 + ZF} is built upon theory~{\tt FOL}, while higher-order logic
1.14 +conceptually contains first-order logic as a fragment.
1.15 +Theorem-proving in predicate logic is undecidable, but many
1.16 researchers have developed strategies to assist in this task.
1.17
1.18 Isabelle's classical reasoner is an \ML{} functor that accepts certain
1.19 @@ -38,9 +39,10 @@
1.20 effectively, you need to know how it works and how to choose among the many
1.21 tactics available, including {\tt Fast_tac} and {\tt Best_tac}.
1.22
1.23 -We shall first discuss the underlying principles, then present the classical
1.24 -reasoner. Finally, we shall see how to instantiate it for new logics. The
1.25 -logics {\tt FOL}, {\tt HOL} and {\tt ZF} have it already installed.
1.26 +We shall first discuss the underlying principles, then present the
1.27 +classical reasoner. Finally, we shall see how to instantiate it for
1.28 +new logics. The logics \FOL, \ZF, {\HOL} and {\HOLCF} have it already
1.29 +installed.
1.30
1.31
1.32 \section{The sequent calculus}
1.33 @@ -71,14 +73,18 @@
1.34 \iflabelundefined{fol-fig}{from {\it Introduction to Isabelle}}%
1.35 {Fig.\ts\ref{fol-fig}}.
1.36 The sequent calculus analogue of~$({\imp}I)$ is the rule
1.37 -$$ \ainfer{\Gamma &\turn \Delta, P\imp Q}{P,\Gamma &\turn \Delta,Q}
1.38 - \eqno({\imp}R) $$
1.39 +$$
1.40 +\ainfer{\Gamma &\turn \Delta, P\imp Q}{P,\Gamma &\turn \Delta,Q}
1.41 +\eqno({\imp}R)
1.42 +$$
1.43 This breaks down some implication on the right side of a sequent; $\Gamma$
1.44 and $\Delta$ stand for the sets of formulae that are unaffected by the
1.45 inference. The analogue of the pair~$({\disj}I1)$ and~$({\disj}I2)$ is the
1.46 single rule
1.47 -$$ \ainfer{\Gamma &\turn \Delta, P\disj Q}{\Gamma &\turn \Delta,P,Q}
1.48 - \eqno({\disj}R) $$
1.49 +$$
1.50 +\ainfer{\Gamma &\turn \Delta, P\disj Q}{\Gamma &\turn \Delta,P,Q}
1.51 +\eqno({\disj}R)
1.52 +$$
1.53 This breaks down some disjunction on the right side, replacing it by both
1.54 disjuncts. Thus, the sequent calculus is a kind of multiple-conclusion logic.
1.55
1.56 @@ -115,15 +121,16 @@
1.57 other connectives, we use sequent-style elimination rules instead of
1.58 destruction rules such as $({\conj}E1,2)$ and $(\forall E)$. But note that
1.59 the rule $(\neg L)$ has no effect under our representation of sequents!
1.60 -$$ \ainfer{\neg P,\Gamma &\turn \Delta}{\Gamma &\turn \Delta,P}
1.61 - \eqno({\neg}L) $$
1.62 +$$
1.63 +\ainfer{\neg P,\Gamma &\turn \Delta}{\Gamma &\turn \Delta,P}\eqno({\neg}L)
1.64 +$$
1.65 What about reasoning on the right? Introduction rules can only affect the
1.66 formula in the conclusion, namely~$Q@1$. The other right-side formulae are
1.67 represented as negated assumptions, $\neg Q@2$, \ldots,~$\neg Q@n$.
1.68 \index{assumptions!negated}
1.69 In order to operate on one of these, it must first be exchanged with~$Q@1$.
1.70 Elim-resolution with the {\bf swap} rule has this effect:
1.71 -$$ \List{\neg P; \; \neg R\Imp P} \Imp R \eqno(swap)$$
1.72 +$$ \List{\neg P; \; \neg R\Imp P} \Imp R \eqno(swap) $$
1.73 To ensure that swaps occur only when necessary, each introduction rule is
1.74 converted into a swapped form: it is resolved with the second premise
1.75 of~$(swap)$. The swapped form of~$({\conj}I)$, which might be
1.76 @@ -172,8 +179,10 @@
1.77 $$ \List{\forall x{.}P(x); P(t)\Imp Q} \Imp Q \eqno(\forall E@2) $$
1.78 Elim-resolution with this rule will delete the universal formula after a
1.79 single use. To replicate universal quantifiers, replace the rule by
1.80 -$$ \List{\forall x{.}P(x);\; \List{P(t); \forall x{.}P(x)}\Imp Q} \Imp Q.
1.81 - \eqno(\forall E@3) $$
1.82 +$$
1.83 +\List{\forall x{.}P(x);\; \List{P(t); \forall x{.}P(x)}\Imp Q} \Imp Q.
1.84 +\eqno(\forall E@3)
1.85 +$$
1.86 To replicate existential quantifiers, replace $(\exists I)$ by
1.87 \[ \List{\neg(\exists x{.}P(x)) \Imp P(t)} \Imp \exists x{.}P(x). \]
1.88 All introduction rules mentioned above are also useful in swapped form.
1.89 @@ -290,14 +299,15 @@
1.90 below). They may perform a form of Modus Ponens: if there are assumptions
1.91 $P\imp Q$ and~$P$, then replace $P\imp Q$ by~$Q$.
1.92
1.93 -The classical reasoning tactics---except {\tt blast_tac}!---allow you to
1.94 -modify this basic proof strategy by
1.95 -applying two arbitrary {\bf wrapper tacticals} to it. This affects each step of
1.96 -the search. Usually they are the identity tacticals, but they could apply
1.97 -another tactic before or after the step tactic. The first one, which is
1.98 -considered to be safe, affects \ttindex{safe_step_tac} and all the tactics that
1.99 -call it. The the second one, which may be unsafe, affects
1.100 -\ttindex{step_tac}, \ttindex{slow_step_tac} and the tactics that call them.
1.101 +The classical reasoning tactics --- except {\tt blast_tac}! --- allow
1.102 +you to modify this basic proof strategy by applying two arbitrary {\bf
1.103 + wrapper tacticals} to it. This affects each step of the search.
1.104 +Usually they are the identity tacticals, but they could apply another
1.105 +tactic before or after the step tactic. The first one, which is
1.106 +considered to be safe, affects \ttindex{safe_step_tac} and all the
1.107 +tactics that call it. The the second one, which may be unsafe, affects
1.108 +\ttindex{step_tac}, \ttindex{slow_step_tac} and the tactics that call
1.109 +them.
1.110
1.111 \begin{ttbox}
1.112 addss : claset * simpset -> claset \hfill{\bf infix 4}
1.113 @@ -315,10 +325,12 @@
1.114 (int -> tactic)) -> claset \hfill{\bf infix 4}
1.115 \end{ttbox}
1.116 %
1.117 -\index{simplification!from classical reasoner}
1.118 -The wrapper tacticals underly the operator \ttindex{addss}, which combines
1.119 -each search step by simplification. Strictly speaking, {\tt addss} is not
1.120 -part of the classical reasoner. It should be defined (using {\tt addSaltern (CHANGED o (safe_asm_more_full_simp_tac ss)}) when the simplifier is installed.
1.121 +\index{simplification!from classical reasoner} The wrapper tacticals
1.122 +underly the operator addss, which combines each search step by
1.123 +simplification. Strictly speaking, {\tt addss} is not part of the
1.124 +classical reasoner. It should be defined (using {\tt addSaltern
1.125 + (CHANGED o (safe_asm_more_full_simp_tac ss)}) when the simplifier is
1.126 +installed.
1.127
1.128 \begin{ttdescription}
1.129 \item[$cs$ addss $ss$] \indexbold{*addss}
1.130 @@ -501,7 +513,7 @@
1.131 warnings. Just like simpsets, clasets can be associated with theories. The
1.132 tactics
1.133 \begin{ttbox}
1.134 -Blast_tac : int -> tactic
1.135 +Blast_tac : int -> tactic
1.136 Fast_tac : int -> tactic
1.137 Best_tac : int -> tactic
1.138 Deepen_tac : int -> int -> tactic
1.139 @@ -620,8 +632,8 @@
1.140 tactics are assumed to be safe!
1.141 \end{ttdescription}
1.142 The functor is not at all sensitive to the formalization of the
1.143 -object-logic. It does not even examine the rules, but merely applies them
1.144 -according to its fixed strategy. The functor resides in {\tt
1.145 -Provers/classical.ML} in the Isabelle distribution directory.
1.146 +object-logic. It does not even examine the rules, but merely applies
1.147 +them according to its fixed strategy. The functor resides in {\tt
1.148 + Provers/classical.ML} in the Isabelle sources.
1.149
1.150 \index{classical reasoner|)}
2.1 --- a/doc-src/Ref/defining.tex Mon May 05 21:18:01 1997 +0200
2.2 +++ b/doc-src/Ref/defining.tex Tue May 06 12:50:16 1997 +0200
2.3 @@ -266,7 +266,7 @@
2.4 abstract syntax tree.
2.5
2.6
2.7 -\subsection{*Inspecting the syntax}
2.8 +\subsection{*Inspecting the syntax} \label{pg:print_syn}
2.9 \begin{ttbox}
2.10 syn_of : theory -> Syntax.syntax
2.11 print_syntax : theory -> unit
2.12 @@ -311,6 +311,7 @@
2.13 {\out type = tvar "::" sort[0] => "_ofsort" (1000)}
2.14 {\out \vdots}
2.15 \ttbreak
2.16 +{\out print modes: "symbols" "xterm"}
2.17 {\out consts: "_K" "_appl" "_aprop" "_args" "_asms" "_bigimpl" \dots}
2.18 {\out parse_ast_translation: "_appl" "_bigimpl" "_bracket"}
2.19 {\out "_idtyp" "_lambda" "_tapp" "_tappl"}
2.20 @@ -353,6 +354,9 @@
2.21 conceptually, they are removed from the grammar by adding new
2.22 productions. Priority information attached to chain productions is
2.23 ignored; only the dummy value $-1$ is displayed.
2.24 +
2.25 + \item[\ttindex{print_modes}] lists the alternative print modes
2.26 + provided by this syntax (see \S\ref{sec:prmodes}).
2.27
2.28 \item[{\tt consts}, {\tt parse_rules}, {\tt print_rules}]
2.29 relate to macros (see \S\ref{sec:macros}).
2.30 @@ -483,7 +487,7 @@
2.31 declarations encoding the priority grammar from
2.32 \S\ref{sec:priority_grammars}:
2.33 \begin{ttbox}
2.34 -EXP = Pure +
2.35 +ExpSyntax = Pure +
2.36 types
2.37 exp
2.38 syntax
2.39 @@ -493,10 +497,10 @@
2.40 "-" :: exp => exp ("- _" [3] 3)
2.41 end
2.42 \end{ttbox}
2.43 -If you put this into a file {\tt EXP.thy} and load it via {\tt use_thy"EXP"},
2.44 -you can run some tests:
2.45 +If you put this into a file {\tt ExpSyntax.thy} and load it via {\tt
2.46 + use_thy"ExpSyntax"}, you can run some tests:
2.47 \begin{ttbox}
2.48 -val read_exp = Syntax.test_read (syn_of EXP.thy) "exp";
2.49 +val read_exp = Syntax.test_read (syn_of ExpSyntax.thy) "exp";
2.50 {\out val it = fn : string -> unit}
2.51 read_exp "0 * 0 * 0 * 0 + 0 + 0 + 0";
2.52 {\out tokens: "0" "*" "0" "*" "0" "*" "0" "+" "0" "+" "0" "+" "0"}
2.53 @@ -515,18 +519,19 @@
2.54 Executing {\tt Syntax.print_gram} reveals the productions derived from the
2.55 above mixfix declarations (lots of additional information deleted):
2.56 \begin{ttbox}
2.57 -Syntax.print_gram (syn_of EXP.thy);
2.58 +Syntax.print_gram (syn_of ExpSyntax.thy);
2.59 {\out exp = "0" => "0" (9)}
2.60 {\out exp = exp[0] "+" exp[1] => "+" (0)}
2.61 {\out exp = exp[3] "*" exp[2] => "*" (2)}
2.62 {\out exp = "-" exp[3] => "-" (3)}
2.63 \end{ttbox}
2.64
2.65 -Note that because {\tt exp} is not of class {\tt logic}, it has been retained
2.66 -as a separate nonterminal. This also entails that the syntax does not provide
2.67 -for identifiers or paranthesized expressions. Normally you would also want to
2.68 -add the declaration {\tt arities exp :: logic} and use {\tt consts} instead
2.69 -of {\tt syntax}. Try this as an exercise and study the changes in the
2.70 +Note that because {\tt exp} is not of class {\tt logic}, it has been
2.71 +retained as a separate nonterminal. This also entails that the syntax
2.72 +does not provide for identifiers or paranthesized expressions.
2.73 +Normally you would also want to add the declaration {\tt arities
2.74 + exp::logic} after {\tt types} and use {\tt consts} instead of {\tt
2.75 + syntax}. Try this as an exercise and study the changes in the
2.76 grammar.
2.77
2.78 \subsection{The mixfix template}
2.79 @@ -576,10 +581,9 @@
2.80 \subsection{Infixes}
2.81 \indexbold{infixes}
2.82
2.83 -Infix operators associating to the left or right can be declared
2.84 -using {\tt infixl} or {\tt infixr}.
2.85 -Roughly speaking, the form {\tt $c$ ::\ $\sigma$ (infixl $p$)}
2.86 -abbreviates the mixfix declarations
2.87 +Infix operators associating to the left or right can be declared using
2.88 +{\tt infixl} or {\tt infixr}. Basically, the form {\tt $c$ ::\
2.89 + $\sigma$ (infixl $p$)} abbreviates the mixfix declarations
2.90 \begin{ttbox}
2.91 "op \(c\)" :: \(\sigma\) ("(_ \(c\)/ _)" [\(p\), \(p+1\)] \(p\))
2.92 "op \(c\)" :: \(\sigma\) ("op \(c\)")
2.93 @@ -594,6 +598,16 @@
2.94 function symbols, as in \ML. Special characters occurring in~$c$ must be
2.95 escaped, as in delimiters, using a single quote.
2.96
2.97 +A slightly more general form of infix declarations allows constant
2.98 +names to be independent from their concrete syntax, namely \texttt{$c$
2.99 + ::\ $\sigma$\ (infixl "$sy$" $p$)}, the same for \texttt{infixr}. As
2.100 +an example consider:
2.101 +\begin{ttbox}
2.102 +and :: [bool, bool] => bool (infixr "&" 35)
2.103 +\end{ttbox}
2.104 +The internal constant name will then be just \texttt{and}, without any
2.105 +\texttt{op} prefixed.
2.106 +
2.107
2.108 \subsection{Binders}
2.109 \indexbold{binders}
2.110 @@ -642,6 +656,45 @@
2.111
2.112 \index{mixfix declarations|)}
2.113
2.114 +
2.115 +\section{*Alternative print modes} \label{sec:prmodes}
2.116 +\index{print modes|(}
2.117 +%
2.118 +Isabelle's pretty printer supports alternative output syntaxes. These
2.119 +may be used independently or in cooperation. The currently active
2.120 +print modes (with precedence from left to right) are determined by a
2.121 +reference variable.
2.122 +\begin{ttbox}\index{*print_mode}
2.123 +print_mode: string list ref
2.124 +\end{ttbox}
2.125 +Initially this may already contain some print mode identifiers,
2.126 +depending on how Isabelle has been invoked (e.g.\ by some user
2.127 +interface). So changes should be incremental --- adding or deleting
2.128 +modes relative to the current value.
2.129 +
2.130 +Any \ML{} string is a legal print mode identifier, without any
2.131 +predeclaration required. The following names should be considered
2.132 +reserved, though: \texttt{""} (yes, the empty string),
2.133 +\texttt{symbols}, \texttt{latex}, \texttt{xterm}.
2.134 +
2.135 +There is a separate table of mixfix productions for pretty printing
2.136 +associated with each print mode. The currently active ones are
2.137 +conceptually just concatenated from left to right, with the standard
2.138 +syntax output table always coming last as default. Thus mixfix
2.139 +productions of preceding modes in the list may override those of later
2.140 +ones. Also note that token translations are always relative to some
2.141 +print mode (see \S\ref{sec:tok_tr}).
2.142 +
2.143 +\medskip The canonical application of print modes is optional printing
2.144 +of mathematical symbols from a special screen font instead of {\sc
2.145 + ascii}. Another example is to re-use Isabelle's advanced
2.146 +$\lambda$-term printing mechanisms to generate completely different
2.147 +output, say for interfacing external tools like model checkers (e.g.\
2.148 +see \texttt{HOL/ex/EindhovenMC.thy}).
2.149 +
2.150 +\index{print modes|)}
2.151 +
2.152 +
2.153 \section{Ambiguity of parsed expressions} \label{sec:ambiguity}
2.154 \index{ambiguity!of parsed expressions}
2.155
2.156 @@ -810,12 +863,7 @@
2.157 end
2.158 \end{ttbox}
2.159 And if we want to have all three connectives together, we create and load a
2.160 -theory file consisting of a single line:\footnote{We can combine the
2.161 - theories without creating a theory file using the ML declaration
2.162 -\begin{ttbox}
2.163 -val MinIFC_thy = merge_theories(MinIF,MinC)
2.164 -\end{ttbox}
2.165 -\index{*merge_theories|fnote}}
2.166 +theory file consisting of a single line:
2.167 \begin{ttbox}
2.168 MinIFC = MinIF + MinC
2.169 \end{ttbox}
3.1 --- a/doc-src/Ref/goals.tex Mon May 05 21:18:01 1997 +0200
3.2 +++ b/doc-src/Ref/goals.tex Tue May 06 12:50:16 1997 +0200
3.3 @@ -25,14 +25,14 @@
3.4
3.5 \section{Basic commands}
3.6 Most proofs begin with {\tt goal} or {\tt goalw} and require no other
3.7 -commands than {\tt by}, {\tt chop} and {\tt undo}. They typically end with
3.8 -a call to {\tt result}.
3.9 +commands than {\tt by}, {\tt chop} and {\tt undo}. They typically end
3.10 +with a call to {\tt qed}.
3.11 \subsection{Starting a backward proof}
3.12 \index{proofs!starting}
3.13 \begin{ttbox}
3.14 goal : theory -> string -> thm list
3.15 goalw : theory -> thm list -> string -> thm list
3.16 -goalw_cterm : thm list -> Sign.cterm -> thm list
3.17 +goalw_cterm : thm list -> cterm -> thm list
3.18 premises : unit -> thm list
3.19 \end{ttbox}
3.20 The {\tt goal} commands start a new proof by setting the goal. They
3.21 @@ -46,10 +46,11 @@
3.22 \begin{ttbox}
3.23 val prems = goal{\it theory\/ formula};
3.24 \end{ttbox}\index{assumptions!of main goal}
3.25 -These assumptions serve as the premises when you are deriving a rule. They
3.26 -are also stored internally and can be retrieved later by the function {\tt
3.27 - premises}. When the proof is finished, {\tt result} compares the
3.28 -stored assumptions with the actual assumptions in the proof state.
3.29 +These assumptions serve as the premises when you are deriving a rule.
3.30 +They are also stored internally and can be retrieved later by the
3.31 +function {\tt premises}. When the proof is finished, {\tt qed}
3.32 +compares the stored assumptions with the actual assumptions in the
3.33 +proof state.
3.34
3.35 \index{definitions!unfolding}
3.36 Some of the commands unfold definitions using meta-rewrite rules. This
3.37 @@ -74,11 +75,11 @@
3.38 meta-rewrite rules to the first subgoal and the premises.
3.39 \index{meta-rewriting}
3.40
3.41 -\item[\ttindexbold{goalw_cterm} {\it theory} {\it defs} {\it ct};]
3.42 -is a version of {\tt goalw} for programming applications. The main goal is
3.43 -supplied as a cterm, not as a string. Typically, the cterm is created from
3.44 -a term~$t$ by \hbox{\tt Sign.cterm_of (sign_of thy) $t$}.
3.45 -\index{*Sign.cterm_of}\index{*sign_of}
3.46 +\item[\ttindexbold{goalw_cterm} {\it theory} {\it defs} {\it ct};] is
3.47 + a version of {\tt goalw} for programming applications. The main
3.48 + goal is supplied as a cterm, not as a string. Typically, the cterm
3.49 + is created from a term~$t$ by \hbox{\tt cterm_of (sign_of thy) $t$}.
3.50 + \index{*cterm_of}\index{*sign_of}
3.51
3.52 \item[\ttindexbold{premises}()]
3.53 returns the list of meta-hypotheses associated with the current proof (in
3.54 @@ -398,7 +399,7 @@
3.55 qed_goal : string->theory-> string->(thm list->tactic list)->unit
3.56 prove_goalw: theory->thm list->string->(thm list->tactic list)->thm
3.57 qed_goalw : string->theory->thm list->string->(thm list->tactic list)->unit
3.58 -prove_goalw_cterm: thm list->Sign.cterm->(thm list->tactic list)->thm
3.59 +prove_goalw_cterm: thm list->cterm->(thm list->tactic list)->thm
3.60 \end{ttbox}
3.61 These batch functions create an initial proof state, then apply a tactic to
3.62 it, yielding a sequence of final proof states. The head of the sequence is
3.63 @@ -413,11 +414,11 @@
3.64 \begin{ttbox}
3.65 val prems = goal {\it theory} {\it formula};
3.66 by \(tac@1\); \ldots by \(tac@n\);
3.67 -val my_thm = result();
3.68 +qed "my_thm";
3.69 \end{ttbox}
3.70 can be transformed to an expression as follows:
3.71 \begin{ttbox}
3.72 -val my_thm = prove_goal {\it theory} {\it formula}
3.73 +qed_goal "my_thm" {\it theory} {\it formula}
3.74 (fn prems=> [ \(tac@1\), \ldots, \(tac@n\) ]);
3.75 \end{ttbox}
3.76 The methods perform identical processing of the initial {\it formula} and
3.77 @@ -449,9 +450,9 @@
3.78 goal is supplied as a cterm, not as a string. Typically, the cterm is
3.79 created from a term~$t$ as follows:
3.80 \begin{ttbox}
3.81 -Sign.cterm_of (sign_of thy) \(t\)
3.82 +cterm_of (sign_of thy) \(t\)
3.83 \end{ttbox}
3.84 -\index{*Sign.cterm_of}\index{*sign_of}
3.85 +\index{*cterm_of}\index{*sign_of}
3.86 \end{ttdescription}
3.87
3.88
4.1 --- a/doc-src/Ref/introduction.tex Mon May 05 21:18:01 1997 +0200
4.2 +++ b/doc-src/Ref/introduction.tex Tue May 06 12:50:16 1997 +0200
4.3 @@ -1,9 +1,11 @@
4.4 %% $Id$
4.5 +
4.6 \chapter{Basic Use of Isabelle}\index{sessions|(}
4.7 -The Reference Manual is a comprehensive description of Isabelle, including
4.8 -all commands, functions and packages. It really is intended for reference,
4.9 -perhaps for browsing, but not for reading through. It is not a tutorial,
4.10 -but assumes familiarity with the basic concepts of Isabelle.
4.11 +The Reference Manual is a comprehensive description of Isabelle
4.12 +proper, including all \ML{} commands, functions and packages. It
4.13 +really is intended for reference, perhaps for browsing, but not for
4.14 +reading through. It is not a tutorial, but assumes familiarity with
4.15 +the basic logical concepts of Isabelle.
4.16
4.17 When you are looking for a way of performing some task, scan the Table of
4.18 Contents for a relevant heading. Functions are organized by their purpose,
4.19 @@ -19,76 +21,98 @@
4.20 \section{Basic interaction with Isabelle}
4.21 \index{starting up|bold}\nobreak
4.22 %
4.23 -First, read the instructions on file {\tt README} in the top-level
4.24 -distribution directory. Follow them to create the object-logics you need
4.25 -on a directory you have created to hold binary images. Suppose the
4.26 -environment variable {\tt ISABELLEBIN} refers to this directory. The
4.27 -instructions for starting up a logic (say {\tt HOL}) depend upon which
4.28 -Standard ML compiler you are using.
4.29 -\begin{itemize}
4.30 -\item With Standard ML of New Jersey, type \verb|$ISABELLEBIN/HOL|.
4.31 -\item With Poly/ML, type \verb|poly $ISABELLEBIN/HOL|, possibly prefixing the
4.32 - command with the directory where {\tt poly} is kept.
4.33 -\end{itemize}
4.34 -Either way, you will find yourself at the \ML{} top level. All Isabelle
4.35 -commands are bound to \ML{} identifiers.
4.36 +We assume that your local Isabelle administrator (this might be you!)
4.37 +has already installed the \Pure\ system and several object-logics
4.38 +properly --- otherwise see the {\tt INSTALL} file in the top-level
4.39 +directory of the distribution on how to build it.
4.40
4.41 -\index{saving your work|bold}
4.42 -Isabelle provides no means of storing theorems or proofs on files.
4.43 -Theorems are simply part of the \ML{} state and are named by \ML{}
4.44 -identifiers. To save your work between sessions, you must save a copy of
4.45 -the \ML{} image. The procedure for doing so is compiler-dependent:
4.46 -\begin{itemize}\index{Poly/{\ML} compiler}
4.47 -\item At the end of a session, Poly/\ML{} saves the state, provided you
4.48 - have created a database for your own use. You can create a database by
4.49 - copying an existing one, or by calling the Poly/\ML{} function {\tt
4.50 - make_database}; the latter course uses much less disc space. A
4.51 - Poly/\ML{} database {\em does not\/} save the contents of references,
4.52 - such as the current state of a backward proof.
4.53 +\medskip Let $\langle isabellehome \rangle$ denote the location where
4.54 +the distribution has been installed. To run Isabelle from a the shell
4.55 +prompt within an ordinary text terminal session, simply type:
4.56 +\begin{ttbox}
4.57 +\({\langle}isabellehome{\rangle}\)/bin/isabelle
4.58 +\end{ttbox}
4.59 +This should start an interactive \ML{} session with the default
4.60 +object-logic already preloaded. All Isabelle commands are bound to
4.61 +\ML{} identifiers.
4.62
4.63 -\item With New Jersey \ML{} you must save the state explicitly before
4.64 -ending the session. While a Poly/\ML{} database can be small, a New Jersey
4.65 -image occupies several megabytes.
4.66 -\end{itemize}
4.67 -See your \ML{} compiler's documentation for full instructions on saving the
4.68 -state.
4.69 +Subsequently we assume that {\tt \(\langle isabellehome \rangle\)/bin}
4.70 +has been added to your shell's search path, in order to avoid typing
4.71 +full path specifications of the executable files.
4.72
4.73 -Saving the state is not enough. Record, on a file, the top-level commands
4.74 -that generate your theories and proofs. Such a record allows you to replay
4.75 -the proofs whenever required, for instance after making minor changes to
4.76 -the axioms. Ideally, your record will be intelligible to others as a
4.77 -formal description of your work.
4.78 +The object-logic image to load may be also specified explicitly as an
4.79 +argument to the {\tt isabelle} command, e.g.:
4.80 +\begin{ttbox}
4.81 +isabelle FOL
4.82 +\end{ttbox}
4.83 +This should put you into the world of polymorphic first-order logic
4.84 +(assuming that {\FOL} has been pre-built).
4.85
4.86 -Since Isabelle's user interface is the \ML{} top level, some kind of window
4.87 -support is essential. One window displays the Isabelle session, while the
4.88 -other displays a file --- your proof record --- being edited. The Emacs
4.89 -editor supports windows and can manage interactive sessions.
4.90 +\index{saving your work|bold} Isabelle provides no means of storing
4.91 +theorems or proofs on files. Theorems are simply part of the \ML{}
4.92 +state and are named by \ML{} identifiers. To save your work between
4.93 +sessions, you must dump the \ML{} system state to a file. This is done
4.94 +automatically when ending the session normally (e.g.\ by typing
4.95 +control-D), provided that the image has been opened \emph{writable} in
4.96 +the first place. The standard object-logics are usually read-only, so
4.97 +you probably have to create a private working copy first. For example,
4.98 +the following shell command puts you into a writable Isabelle session
4.99 +of name \texttt{Foo} that initially contains just \FOL:
4.100 +\begin{ttbox}
4.101 +isabelle FOL Foo
4.102 +\end{ttbox}
4.103 +Ending the \texttt{Foo} session with control-D will cause the complete
4.104 +\ML{} world to be saved somewhere in your home directory\footnote{The
4.105 + default location is in \texttt{\~\relax/isabelle/heaps}, but this
4.106 + depends on your local configuration.}. Make sure there is enough
4.107 +space available! Then one may later continue at exactly the same point
4.108 +by running
4.109 +\begin{ttbox}
4.110 +isabelle Foo
4.111 +\end{ttbox}
4.112 +
4.113 +%FIXME not yet
4.114 +%More details about \texttt{isabelle} may be found in the \emph{System
4.115 +% Manual}.
4.116 +
4.117 +\medskip Saving the state is not enough. Record, on a file, the
4.118 +top-level commands that generate your theories and proofs. Such a
4.119 +record allows you to replay the proofs whenever required, for instance
4.120 +after making minor changes to the axioms. Ideally, your record will
4.121 +be somewhat intelligible to others as a formal description of your
4.122 +work.
4.123 +
4.124 +\medskip There are more comfortable user interfaces than the
4.125 +bare-bones \ML{} top-level run from a text terminal. The
4.126 +\texttt{Isabelle} executable (note the capital I) runs one such
4.127 +interface, depending on your local configuration. Furthermore there
4.128 +are a number of external utilities available. These are started
4.129 +uniformly via the \texttt{isatool} wrapper.
4.130 +
4.131 +%FIXME not yet
4.132 +%Again, see the \emph{System Manual} for more information user
4.133 +%interfaces and utilities.
4.134
4.135
4.136 \section{Ending a session}
4.137 \begin{ttbox}
4.138 -quit : unit -> unit
4.139 -commit : unit -> unit \hfill{\bf Poly/ML only}
4.140 -exportML : string -> bool \hfill{\bf New Jersey ML only}
4.141 +quit : unit -> unit
4.142 +exit : int -> unit
4.143 +commit : unit -> unit
4.144 \end{ttbox}
4.145 \begin{ttdescription}
4.146 -\item[\ttindexbold{quit}();]
4.147 -aborts the Isabelle session, without saving the state.
4.148 +\item[\ttindexbold{quit}();] ends the Isabelle session, without saving
4.149 + the state.
4.150
4.151 -\item[\ttindexbold{commit}();]
4.152 - saves the current state in your Poly/\ML{} database without ending the
4.153 - session. The contents of references are lost, so never do this during an
4.154 - interactive proof!\index{Poly/{\ML} compiler}
4.155 +\item[\ttindexbold{exit}();] same as {\tt quit}, passing a return code
4.156 + to the operating system.
4.157
4.158 -\item[\ttindexbold{exportML} "{\it file}";] saves an
4.159 -image of your session to the given {\it file}.
4.160 +\item[\ttindexbold{commit}();] saves the current state without ending
4.161 + the session, provided that the logic image is opened read-write.
4.162 \end{ttdescription}
4.163
4.164 -\begin{warn}
4.165 -Typing control-D also finishes the session, but its effect is
4.166 -compiler-dependent. Poly/\ML{} will then save the state, if you have a
4.167 -private database. New Jersey \ML{} will discard the state!
4.168 -\end{warn}
4.169 +Typing control-D also finishes the session in essentially the same way
4.170 +as the sequence {\tt commit(); quit();} would.
4.171
4.172
4.173 \section{Reading ML files}
4.174 @@ -105,7 +129,7 @@
4.175 changes the current directory to {\it dir}. This is the default directory
4.176 for reading files and for writing temporary files.
4.177
4.178 -\item[\ttindexbold{pwd} ();] returns the path of the current directory.
4.179 +\item[\ttindexbold{pwd}();] returns the path of the current directory.
4.180
4.181 \item[\ttindexbold{use} "$file$";]
4.182 reads the given {\it file} as input to the \ML{} session. Reading a file
4.183 @@ -116,6 +140,16 @@
4.184 \end{ttdescription}
4.185
4.186
4.187 +\section{Setting flags}
4.188 +\begin{ttbox}
4.189 +set : bool ref -> bool
4.190 +reset : bool ref -> bool
4.191 +toggle : bool ref -> bool
4.192 +\end{ttbox}\index{*set}\index{*reset}\index{*toggle}
4.193 +These are some shorthands for manipulating boolean references. The new
4.194 +value is returned.
4.195 +
4.196 +
4.197 \section{Printing of terms and theorems}\label{sec:printing-control}
4.198 \index{printing control|(}
4.199 Isabelle's pretty printer is controlled by a number of parameters.
4.200 @@ -236,35 +270,36 @@
4.201 theory used in the last interactive proof.
4.202 \end{warn}
4.203
4.204 -\section{Shell scripts}\label{sec:shell-scripts}
4.205 -\index{shell scripts|bold} The following files are distributed with
4.206 -Isabelle, and work under Unix$^{\rm TM}$. They can be executed as commands
4.207 -to the Unix shell. Some of them depend upon shell environment variables.
4.208 -\begin{ttdescription}
4.209 -\item[make-all $switches$] \index{*make-all shell script}
4.210 - compiles the Isabelle system, when executed on the source directory.
4.211 - Environment variables specify which \ML{} compiler to use. These
4.212 - variables, and the {\it switches}, are documented on the file itself.
4.213 -
4.214 -\item[teeinput $program$] \index{*teeinput shell script}
4.215 - executes the {\it program}, while piping the standard input to a log file
4.216 - designated by the \verb|$LISTEN| environment variable. Normally the
4.217 - program is Isabelle, and the log file receives a copy of all the Isabelle
4.218 - commands.
4.219 -
4.220 -\item[xlisten $program$] \index{*xlisten shell script}
4.221 - is a trivial `user interface' for the X Window System. It creates two
4.222 - windows using {\tt xterm}. One executes an interactive session via
4.223 - \hbox{\tt teeinput $program$}, while the other displays the log file. To
4.224 - make a proof record, simply paste lines from the log file into an editor
4.225 - window.
4.226 -
4.227 -\item[expandshort $files$] \index{*expandshort shell script}
4.228 - reads the {\it files\/} and replaces all occurrences of the shorthand
4.229 - commands {\tt br}, {\tt be}, {\tt brs}, {\tt bes}, etc., with the
4.230 - corresponding full commands. Shorthand commands should appear one
4.231 - per line. The old versions of the files
4.232 - are renamed to have the suffix~\verb'~~'.
4.233 -\end{ttdescription}
4.234 +%FIXME remove
4.235 +%\section{Shell scripts}\label{sec:shell-scripts}
4.236 +%\index{shell scripts|bold} The following files are distributed with
4.237 +%Isabelle, and work under Unix$^{\rm TM}$. They can be executed as commands
4.238 +%to the Unix shell. Some of them depend upon shell environment variables.
4.239 +%\begin{ttdescription}
4.240 +%\item[make-all $switches$] \index{*make-all shell script}
4.241 +% compiles the Isabelle system, when executed on the source directory.
4.242 +% Environment variables specify which \ML{} compiler to use. These
4.243 +% variables, and the {\it switches}, are documented on the file itself.
4.244 +%
4.245 +%\item[teeinput $program$] \index{*teeinput shell script}
4.246 +% executes the {\it program}, while piping the standard input to a log file
4.247 +% designated by the \verb|$LISTEN| environment variable. Normally the
4.248 +% program is Isabelle, and the log file receives a copy of all the Isabelle
4.249 +% commands.
4.250 +%
4.251 +%\item[xlisten $program$] \index{*xlisten shell script}
4.252 +% is a trivial `user interface' for the X Window System. It creates two
4.253 +% windows using {\tt xterm}. One executes an interactive session via
4.254 +% \hbox{\tt teeinput $program$}, while the other displays the log file. To
4.255 +% make a proof record, simply paste lines from the log file into an editor
4.256 +% window.
4.257 +%
4.258 +%\item[expandshort $files$] \index{*expandshort shell script}
4.259 +% reads the {\it files\/} and replaces all occurrences of the shorthand
4.260 +% commands {\tt br}, {\tt be}, {\tt brs}, {\tt bes}, etc., with the
4.261 +% corresponding full commands. Shorthand commands should appear one
4.262 +% per line. The old versions of the files
4.263 +% are renamed to have the suffix~\verb'~~'.
4.264 +%\end{ttdescription}
4.265
4.266 \index{sessions|)}
5.1 --- a/doc-src/Ref/ref.ind Mon May 05 21:18:01 1997 +0200
5.2 +++ b/doc-src/Ref/ref.ind Tue May 06 12:50:16 1997 +0200
5.3 @@ -1,806 +1,811 @@
5.4 \begin{theindex}
5.5
5.6 - \item {\ptt !!} symbol, 64
5.7 + \item {\tt !!} symbol, 65
5.8 \subitem in main goal, 7
5.9 - \item {\tt\$}, \bold{56}, 79
5.10 - \item {\tt\%} symbol, 64
5.11 + \item {\tt\$}, \bold{57}, 82
5.12 + \item {\tt\%} symbol, 65
5.13 \item *
5.14 - \subitem claset, 121
5.15 - \subitem simpset, 99
5.16 - \item {\ptt ::} symbol, 64, 65
5.17 - \item {\ptt ==} symbol, 64
5.18 - \item {\ptt ==>} symbol, 64
5.19 - \item {\ptt =>} symbol, 64
5.20 - \item {\ptt =?=} symbol, 64
5.21 - \item {\tt\at Enum} constant, 85
5.22 - \item {\tt\at Finset} constant, 85
5.23 - \item {\ptt [} symbol, 64
5.24 - \item {\ptt [|} symbol, 64
5.25 - \item {\ptt ]} symbol, 64
5.26 - \item {\ptt _K} constant, 86, 88
5.27 - \item \verb'{}' symbol, 85
5.28 - \item {\tt\ttlbrace} symbol, 64
5.29 - \item {\tt\ttrbrace} symbol, 64
5.30 - \item {\ptt |]} symbol, 64
5.31 + \subitem claset, 127
5.32 + \subitem simpset, 106
5.33 + \item {\tt ::} symbol, 65, 66
5.34 + \item {\tt ==} symbol, 65
5.35 + \item {\tt ==>} symbol, 65
5.36 + \item {\tt =>} symbol, 65
5.37 + \item {\tt =?=} symbol, 65
5.38 + \item {\tt\at Enum} constant, 88
5.39 + \item {\tt\at Finset} constant, 88, 89
5.40 + \item {\tt [} symbol, 65
5.41 + \item {\tt [|} symbol, 65
5.42 + \item {\tt ]} symbol, 65
5.43 + \item {\tt _K} constant, 90, 92
5.44 + \item \verb'{}' symbol, 88
5.45 + \item {\tt\ttlbrace} symbol, 65
5.46 + \item {\tt\ttrbrace} symbol, 65
5.47 + \item {\tt |]} symbol, 65
5.48
5.49 \indexspace
5.50
5.51 - \item {\ptt Abs}, \bold{56}, 79
5.52 - \item {\ptt abstract_over}, \bold{57}
5.53 - \item {\ptt abstract_rule}, \bold{41}
5.54 - \item {\ptt aconv}, \bold{57}
5.55 - \item {\ptt addaltern}, \bold{118}
5.56 - \item {\ptt addbefore}, \bold{118}
5.57 - \item {\ptt addcongs}, 97, 110, \bold{110}
5.58 - \item {\ptt AddDs}, \bold{121}
5.59 - \item {\ptt addDs}, \bold{116}
5.60 - \item {\ptt addeqcongs}, \bold{97}, 100, 110
5.61 - \item {\ptt AddEs}, \bold{121}
5.62 - \item {\ptt addEs}, \bold{116}
5.63 - \item {\ptt AddIs}, \bold{121}
5.64 - \item {\ptt addIs}, \bold{116}
5.65 - \item {\ptt addloop}, 99, 100
5.66 - \item {\ptt addSaltern}, \bold{118}
5.67 - \item {\ptt addSbefore}, \bold{118}
5.68 - \item {\ptt AddSDs}, \bold{121}
5.69 - \item {\ptt addSDs}, \bold{116}
5.70 - \item {\ptt AddSEs}, \bold{121}
5.71 - \item {\ptt addSEs}, \bold{116}
5.72 - \item {\ptt Addsimps}, \bold{95}, 99, 100
5.73 - \item {\ptt addsimps}, 96, 99, 100, 110
5.74 - \item {\ptt AddSIs}, \bold{121}
5.75 - \item {\ptt addSIs}, \bold{116}
5.76 - \item {\ptt addSolver}, 98, 100
5.77 - \item {\ptt addss}, 117, \bold{117}, 118
5.78 - \item {\ptt addSSolver}, 98, 100
5.79 - \item {\ptt all_tac}, \bold{27}
5.80 - \item {\ptt ALLGOALS}, \bold{32}, 103, 106
5.81 + \item {\tt Abs}, \bold{57}, 82
5.82 + \item {\tt abstract_over}, \bold{58}
5.83 + \item {\tt abstract_rule}, \bold{44}
5.84 + \item {\tt aconv}, \bold{58}
5.85 + \item {\tt addaltern}, \bold{124}
5.86 + \item {\tt addbefore}, \bold{124}
5.87 + \item {\tt addcongs}, 103, \bold{115}, 116
5.88 + \item {\tt AddDs}, \bold{127}
5.89 + \item {\tt addDs}, \bold{123}
5.90 + \item {\tt addeqcongs}, \bold{103}, 105, 115
5.91 + \item {\tt AddEs}, \bold{127}
5.92 + \item {\tt addEs}, \bold{123}
5.93 + \item {\tt AddIs}, \bold{127}
5.94 + \item {\tt addIs}, \bold{123}
5.95 + \item {\tt addloop}, 104, 105
5.96 + \item {\tt addSaltern}, \bold{124}
5.97 + \item {\tt addSbefore}, \bold{124}
5.98 + \item {\tt AddSDs}, \bold{127}
5.99 + \item {\tt addSDs}, \bold{123}
5.100 + \item {\tt AddSEs}, \bold{127}
5.101 + \item {\tt addSEs}, \bold{123}
5.102 + \item {\tt Addsimps}, \bold{100}, 105, 106
5.103 + \item {\tt addsimps}, 102, 105, 106, 116
5.104 + \item {\tt AddSIs}, \bold{127}
5.105 + \item {\tt addSIs}, \bold{123}
5.106 + \item {\tt addSolver}, 104, 105
5.107 + \item {\tt addss}, \bold{124}, 125
5.108 + \item {\tt addSSolver}, 104, 105
5.109 + \item {\tt all_tac}, \bold{30}
5.110 + \item {\tt ALLGOALS}, \bold{34}, 108, 112
5.111 \item ambiguity
5.112 - \subitem of parsed expressions, 72
5.113 - \item {\ptt any} nonterminal, \bold{63}
5.114 - \item {\ptt APPEND}, \bold{26}, 27
5.115 - \item {\ptt APPEND'}, 33
5.116 - \item {\ptt Appl}, 76
5.117 - \item {\ptt aprop} nonterminal, \bold{63}
5.118 - \item {\ptt ares_tac}, \bold{18}
5.119 - \item {\ptt args} nonterminal, 85
5.120 - \item {\ptt Arith} theory, 105
5.121 + \subitem of parsed expressions, 75
5.122 + \item {\tt any} nonterminal, \bold{64}
5.123 + \item {\tt APPEND}, \bold{28}, 30
5.124 + \item {\tt APPEND'}, 35
5.125 + \item {\tt Appl}, 79
5.126 + \item {\tt aprop} nonterminal, \bold{66}
5.127 + \item {\tt ares_tac}, \bold{19}
5.128 + \item {\tt args} nonterminal, 89
5.129 + \item {\tt Arith} theory, 111
5.130 \item arities
5.131 - \subitem context conditions, 48
5.132 - \item {\ptt Asm_full_simp_tac}, \bold{95}, 100
5.133 - \item {\ptt asm_full_simp_tac}, 20, \bold{99}, 100, 104
5.134 - \item {\ptt asm_rl} theorem, 19
5.135 - \item {\ptt Asm_simp_tac}, \bold{94}, 100
5.136 - \item {\ptt asm_simp_tac}, \bold{99}, 100, 102, 110
5.137 - \item associative-commutative operators, 105
5.138 - \item {\ptt assume}, \bold{40}
5.139 - \item {\ptt assume_ax}, 8, \bold{52}
5.140 - \item {\ptt assume_tac}, \bold{16}, 116
5.141 - \item {\ptt assumption}, \bold{43}
5.142 + \subitem context conditions, 52
5.143 + \item {\tt Asm_full_simp_tac}, \bold{100}, 105
5.144 + \item {\tt asm_full_simp_tac}, 22, 105, \bold{106}, 109
5.145 + \item {\tt asm_rl} theorem, 21
5.146 + \item {\tt Asm_simp_tac}, \bold{100}, 105
5.147 + \item {\tt asm_simp_tac}, 105, \bold{106}, 107, 116
5.148 + \item associative-commutative operators, 110
5.149 + \item {\tt assume}, \bold{42}
5.150 + \item {\tt assume_ax}, 8, \bold{55}
5.151 + \item {\tt assume_tac}, \bold{17}, 122
5.152 + \item {\tt assumption}, \bold{45}
5.153 \item assumptions
5.154 - \subitem contradictory, 121
5.155 - \subitem deleting, 20
5.156 - \subitem in simplification, 94, 98
5.157 - \subitem inserting, 18
5.158 - \subitem negated, 114
5.159 - \subitem of main goal, 6, 8, 13
5.160 - \subitem reordering, 104
5.161 - \subitem rotating, 20
5.162 - \subitem substitution in, 91
5.163 - \subitem tactics for, 16
5.164 - \item ASTs, 76--80
5.165 - \subitem made from parse trees, 77
5.166 - \subitem made from terms, 79
5.167 - \item {\ptt atac}, \bold{17}
5.168 + \subitem contradictory, 128
5.169 + \subitem deleting, 22
5.170 + \subitem in simplification, 99, 104
5.171 + \subitem inserting, 19
5.172 + \subitem negated, 120
5.173 + \subitem of main goal, 7--9, 14
5.174 + \subitem reordering, 109
5.175 + \subitem rotating, 22
5.176 + \subitem substitution in, 96
5.177 + \subitem tactics for, 17
5.178 + \item ASTs, 79--84
5.179 + \subitem made from parse trees, 80
5.180 + \subitem made from terms, 82
5.181 + \item {\tt atac}, \bold{19}
5.182 + \item {\tt axclass} section, 51
5.183 + \item axiomatic type class, 51
5.184 \item axioms
5.185 - \subitem extracting, 51
5.186 - \item {\ptt axioms_of}, \bold{52}
5.187 + \subitem extracting, 55
5.188 + \item {\tt axioms_of}, \bold{56}
5.189
5.190 \indexspace
5.191
5.192 - \item {\ptt ba}, \bold{10}
5.193 - \item {\ptt back}, \bold{9}
5.194 - \item batch execution, 11
5.195 - \item {\ptt bd}, \bold{10}
5.196 - \item {\ptt bds}, \bold{10}
5.197 - \item {\ptt be}, \bold{10}
5.198 - \item {\ptt bes}, \bold{10}
5.199 - \item {\ptt BEST_FIRST}, \bold{29}, 30
5.200 - \item {\ptt Best_tac}, \bold{121}
5.201 - \item {\ptt best_tac}, \bold{119}
5.202 - \item {\ptt beta_conversion}, \bold{41}
5.203 - \item {\ptt bicompose}, \bold{43}
5.204 - \item {\ptt bimatch_tac}, \bold{22}
5.205 - \item {\ptt bind_thm}, 8, \bold{8}, 35
5.206 - \item binders, \bold{72}
5.207 - \item {\ptt biresolution}, \bold{43}
5.208 - \item {\ptt biresolve_tac}, \bold{22}, 121
5.209 - \item {\ptt Blast.depth_tac}, \bold{119}
5.210 - \item {\ptt Blast.trace}, \bold{119}
5.211 - \item {\ptt Blast_tac}, \bold{121}
5.212 - \item {\ptt blast_tac}, \bold{119}
5.213 - \item {\ptt Bound}, \bold{56}, 77, 79, 80
5.214 - \item {\ptt bound_hyp_subst_tac}, \bold{91}
5.215 - \item {\ptt br}, \bold{10}
5.216 - \item {\ptt BREADTH_FIRST}, \bold{29}
5.217 - \item {\ptt brs}, \bold{10}
5.218 - \item {\ptt bw}, \bold{11}
5.219 - \item {\ptt bws}, \bold{11}
5.220 - \item {\ptt by}, \bold{7}, 9, 10, 14
5.221 - \item {\ptt byev}, \bold{7}
5.222 + \item {\tt ba}, \bold{11}
5.223 + \item {\tt back}, \bold{9}
5.224 + \item batch execution, 12
5.225 + \item {\tt bd}, \bold{11}
5.226 + \item {\tt bds}, \bold{11}
5.227 + \item {\tt be}, \bold{11}
5.228 + \item {\tt bes}, \bold{11}
5.229 + \item {\tt BEST_FIRST}, \bold{31}, 32
5.230 + \item {\tt Best_tac}, \bold{127}
5.231 + \item {\tt best_tac}, \bold{126}
5.232 + \item {\tt beta_conversion}, \bold{43}
5.233 + \item {\tt bicompose}, \bold{46}
5.234 + \item {\tt bimatch_tac}, \bold{23}
5.235 + \item {\tt bind_thm}, \bold{8}, 9, 37
5.236 + \item binders, \bold{74}
5.237 + \item {\tt biresolution}, \bold{45}
5.238 + \item {\tt biresolve_tac}, \bold{23}, 128
5.239 + \item {\tt Blast.depth_tac}, \bold{125}
5.240 + \item {\tt Blast.trace}, \bold{125}
5.241 + \item {\tt Blast_tac}, \bold{127}
5.242 + \item {\tt blast_tac}, \bold{125}
5.243 + \item {\tt Bound}, \bold{57}, 80, 82, 83
5.244 + \item {\tt bound_hyp_subst_tac}, \bold{96}
5.245 + \item {\tt br}, \bold{11}
5.246 + \item {\tt BREADTH_FIRST}, \bold{31}
5.247 + \item {\tt brs}, \bold{11}
5.248 + \item {\tt bw}, \bold{12}
5.249 + \item {\tt bws}, \bold{12}
5.250 + \item {\tt by}, \bold{7}, 9, 10, 15
5.251 + \item {\tt byev}, \bold{7}
5.252
5.253 \indexspace
5.254
5.255 - \item {\ptt cd}, \bold{2}, 50
5.256 - \item {\ptt cert_axm}, \bold{58}
5.257 - \item {\ptt CHANGED}, \bold{28}
5.258 - \item {\ptt chop}, \bold{9}, 13
5.259 - \item {\ptt choplev}, \bold{9}
5.260 + \item {\tt cd}, \bold{3}, 53
5.261 + \item {\tt cert_axm}, \bold{59}
5.262 + \item {\tt CHANGED}, \bold{30}
5.263 + \item {\tt chop}, \bold{9}, 13
5.264 + \item {\tt choplev}, \bold{9}
5.265 \item claset
5.266 - \subitem current, 120
5.267 - \item {\ptt claset} ML type, 116
5.268 + \subitem current, 127
5.269 + \item {\tt claset} ML type, 122
5.270 \item classes
5.271 - \subitem context conditions, 48
5.272 - \item classical reasoner, 112--122
5.273 - \subitem setting up, 122
5.274 - \subitem tactics, 118
5.275 - \item classical sets, 115
5.276 - \item {\ptt ClassicalFun}, 122
5.277 - \item {\ptt combination}, \bold{41}
5.278 - \item {\ptt commit}, \bold{2}
5.279 - \item {\ptt COMP}, \bold{43}
5.280 - \item {\ptt compose}, \bold{43}
5.281 - \item {\ptt compose_tac}, \bold{21}
5.282 - \item {\ptt compSWrapper}, \bold{118}
5.283 - \item {\ptt compWrapper}, \bold{118}
5.284 - \item {\ptt concl_of}, \bold{37}
5.285 - \item {\ptt COND}, \bold{30}
5.286 - \item congruence rules, 97
5.287 - \item {\ptt Const}, \bold{56}, 79, 88
5.288 - \item {\ptt Constant}, 76, 88
5.289 - \item constants, \bold{56}
5.290 - \subitem for translations, 68
5.291 - \subitem syntactic, 81
5.292 - \item {\ptt contr_tac}, \bold{121}
5.293 - \item {\ptt could_unify}, \bold{23}
5.294 - \item {\ptt cterm} ML type, 58
5.295 - \item {\ptt cterm_instantiate}, \bold{36}
5.296 - \item {\ptt cterm_of}, \bold{58}
5.297 - \item {\ptt ctyp}, \bold{59}
5.298 - \item {\ptt ctyp_of}, \bold{59}
5.299 - \item {\ptt cut_facts_tac}, 7, \bold{18}, 92
5.300 - \item {\ptt cut_inst_tac}, \bold{18}
5.301 - \item {\ptt cut_rl} theorem, 19
5.302 + \subitem context conditions, 52
5.303 + \item classical reasoner, 118--129
5.304 + \subitem setting up, 128
5.305 + \subitem tactics, 124
5.306 + \item classical sets, 122
5.307 + \item {\tt ClassicalFun}, 129
5.308 + \item {\tt combination}, \bold{44}
5.309 + \item {\tt commit}, \bold{2}
5.310 + \item {\tt COMP}, \bold{46}
5.311 + \item {\tt compose}, \bold{46}
5.312 + \item {\tt compose_tac}, \bold{22}
5.313 + \item {\tt compSWrapper}, \bold{124}
5.314 + \item {\tt compWrapper}, \bold{124}
5.315 + \item {\tt concl_of}, \bold{39}
5.316 + \item {\tt COND}, \bold{32}
5.317 + \item congruence rules, 102
5.318 + \item {\tt Const}, \bold{57}, 82, 92
5.319 + \item {\tt Constant}, 79, 92
5.320 + \item constants, \bold{57}
5.321 + \subitem for translations, 69
5.322 + \subitem syntactic, 84
5.323 + \item {\tt contr_tac}, \bold{128}
5.324 + \item {\tt could_unify}, \bold{24}
5.325 + \item {\tt CPure} theory, 49
5.326 + \item {\tt CPure.thy}, \bold{55}
5.327 + \item {\tt cterm} ML type, 59
5.328 + \item {\tt cterm_instantiate}, \bold{38}
5.329 + \item {\tt cterm_of}, 7, 13, \bold{59}
5.330 + \item {\tt ctyp}, \bold{60}
5.331 + \item {\tt ctyp_of}, \bold{61}
5.332 + \item {\tt cut_facts_tac}, 7, \bold{19}, 97
5.333 + \item {\tt cut_inst_tac}, \bold{19}
5.334 + \item {\tt cut_rl} theorem, 21
5.335
5.336 \indexspace
5.337
5.338 - \item {\ptt datatype}, 95
5.339 - \item {\ptt Deepen_tac}, \bold{121}
5.340 - \item {\ptt deepen_tac}, \bold{120}
5.341 - \item {\ptt defer_tac}, \bold{18}
5.342 - \item definitions, \see{rewriting, meta-level}{0}, 18, \bold{48}
5.343 + \item {\tt datatype}, 100
5.344 + \item {\tt Deepen_tac}, \bold{127}
5.345 + \item {\tt deepen_tac}, \bold{126}
5.346 + \item {\tt defer_tac}, \bold{20}
5.347 + \item definitions, \see{rewriting, meta-level}{1}, 20, \bold{51}
5.348 \subitem unfolding, 7, 8
5.349 - \item {\ptt delcongs}, 97
5.350 - \item {\ptt deleqcongs}, 97, 100
5.351 - \item {\ptt delete_tmpfiles}, \bold{49}
5.352 - \item delimiters, \bold{65}, 67, 68, 70
5.353 - \item {\ptt delrules}, \bold{116}
5.354 - \item {\ptt Delsimps}, \bold{95}, 99, 100
5.355 - \item {\ptt delsimps}, 99, 100
5.356 - \item {\ptt dependent_tr'}, 86, \bold{88}
5.357 - \item {\ptt DEPTH_FIRST}, \bold{29}
5.358 - \item {\ptt DEPTH_SOLVE}, \bold{29}
5.359 - \item {\ptt DEPTH_SOLVE_1}, \bold{29}
5.360 - \item {\ptt depth_tac}, \bold{120}
5.361 - \item {\ptt Deriv.drop}, \bold{45}
5.362 - \item {\ptt Deriv.linear}, \bold{45}
5.363 - \item {\ptt Deriv.size}, \bold{45}
5.364 - \item {\ptt Deriv.tree}, \bold{45}
5.365 - \item {\ptt dest_eq}, \bold{92}
5.366 - \item {\ptt dest_state}, \bold{37}
5.367 - \item destruct-resolution, 15
5.368 - \item {\ptt DETERM}, \bold{30}
5.369 - \item discrimination nets, \bold{22}
5.370 - \item {\ptt dmatch_tac}, \bold{16}
5.371 - \item {\ptt dres_inst_tac}, \bold{17}
5.372 - \item {\ptt dresolve_tac}, \bold{15}
5.373 - \item {\ptt dtac}, \bold{17}
5.374 - \item {\ptt dummyT}, 79, 80, 89
5.375 + \item {\tt delcongs}, 103
5.376 + \item {\tt deleqcongs}, 103, 105
5.377 + \item {\tt delete_tmpfiles}, \bold{53}
5.378 + \item delimiters, \bold{66}, 69, 70, 72
5.379 + \item {\tt delrules}, \bold{123}
5.380 + \item {\tt Delsimps}, \bold{100}, 105, 106
5.381 + \item {\tt delsimps}, 105, 106
5.382 + \item {\tt dependent_tr'}, 90, \bold{92}
5.383 + \item {\tt DEPTH_FIRST}, \bold{31}
5.384 + \item {\tt DEPTH_SOLVE}, \bold{31}
5.385 + \item {\tt DEPTH_SOLVE_1}, \bold{31}
5.386 + \item {\tt depth_tac}, \bold{126}
5.387 + \item {\tt Deriv.drop}, \bold{48}
5.388 + \item {\tt Deriv.linear}, \bold{48}
5.389 + \item {\tt Deriv.size}, \bold{48}
5.390 + \item {\tt Deriv.tree}, \bold{48}
5.391 + \item {\tt dest_eq}, \bold{97}
5.392 + \item {\tt dest_state}, \bold{39}
5.393 + \item destruct-resolution, 17
5.394 + \item {\tt DETERM}, \bold{32}
5.395 + \item discrimination nets, \bold{24}
5.396 + \item {\tt dmatch_tac}, \bold{17}
5.397 + \item {\tt dres_inst_tac}, \bold{18}
5.398 + \item {\tt dresolve_tac}, \bold{17}
5.399 + \item {\tt dtac}, \bold{19}
5.400 + \item {\tt dummyT}, 82, 83, 93
5.401
5.402 \indexspace
5.403
5.404 - \item elim-resolution, 15
5.405 - \item {\ptt ematch_tac}, \bold{16}
5.406 - \item {\ptt empty} constant, 85
5.407 - \item {\ptt empty_cs}, \bold{116}
5.408 - \item {\ptt empty_ss}, 100, 110
5.409 - \item {\ptt eq_assume_tac}, \bold{16}, 116
5.410 - \item {\ptt eq_assumption}, \bold{43}
5.411 - \item {\ptt eq_mp_tac}, \bold{121}
5.412 - \item {\ptt eq_reflection} theorem, \bold{92}, 107
5.413 - \item {\ptt eq_thm}, \bold{30}
5.414 - \item {\ptt equal_elim}, \bold{41}
5.415 - \item {\ptt equal_intr}, \bold{40}
5.416 - \item equality, 90--93
5.417 - \item {\ptt eres_inst_tac}, \bold{17}
5.418 - \item {\ptt eresolve_tac}, \bold{15}
5.419 - \item {\ptt eta_contract}, \bold{4}, 83
5.420 - \item {\ptt etac}, \bold{17}
5.421 - \item {\ptt EVERY}, \bold{27}
5.422 - \item {\ptt EVERY'}, 33
5.423 - \item {\ptt EVERY1}, \bold{33}
5.424 + \item elim-resolution, 16
5.425 + \item {\tt ematch_tac}, \bold{17}
5.426 + \item {\tt empty} constant, 88
5.427 + \item {\tt empty_cs}, \bold{122}
5.428 + \item {\tt empty_ss}, 105, 116
5.429 + \item {\tt eq_assume_tac}, \bold{17}, 122
5.430 + \item {\tt eq_assumption}, \bold{45}
5.431 + \item {\tt eq_mp_tac}, \bold{128}
5.432 + \item {\tt eq_reflection} theorem, \bold{97}, 113
5.433 + \item {\tt eq_thm}, \bold{32}
5.434 + \item {\tt equal_elim}, \bold{43}
5.435 + \item {\tt equal_intr}, \bold{43}
5.436 + \item equality, 95--98
5.437 + \item {\tt eres_inst_tac}, \bold{18}
5.438 + \item {\tt eresolve_tac}, \bold{16}
5.439 + \item {\tt eta_contract}, \bold{4}, 86
5.440 + \item {\tt etac}, \bold{19}
5.441 + \item {\tt EVERY}, \bold{29}
5.442 + \item {\tt EVERY'}, 35
5.443 + \item {\tt EVERY1}, \bold{35}
5.444 \item examples
5.445 - \subitem of logic definitions, 73
5.446 - \subitem of macros, 85, 86
5.447 - \subitem of mixfix declarations, 70
5.448 - \subitem of simplification, 101
5.449 - \subitem of translations, 88
5.450 + \subitem of logic definitions, 76
5.451 + \subitem of macros, 88, 89
5.452 + \subitem of mixfix declarations, 71
5.453 + \subitem of simplification, 106
5.454 + \subitem of translations, 92
5.455 \item exceptions
5.456 \subitem printing of, 4
5.457 - \item {\ptt expandshort} shell script, 5
5.458 - \item {\ptt exportML}, \bold{2}
5.459 - \item {\ptt extensional}, \bold{41}
5.460 + \item {\tt exit}, \bold{2}
5.461 + \item {\tt extensional}, \bold{44}
5.462
5.463 \indexspace
5.464
5.465 - \item {\ptt fa}, \bold{11}
5.466 - \item {\ptt Fast_tac}, \bold{121}
5.467 - \item {\ptt fast_tac}, \bold{119}
5.468 - \item {\ptt fd}, \bold{11}
5.469 - \item {\ptt fds}, \bold{11}
5.470 - \item {\ptt fe}, \bold{11}
5.471 - \item {\ptt fes}, \bold{11}
5.472 + \item {\tt fa}, \bold{11}
5.473 + \item {\tt Fast_tac}, \bold{127}
5.474 + \item {\tt fast_tac}, \bold{126}
5.475 + \item {\tt fd}, \bold{11}
5.476 + \item {\tt fds}, \bold{11}
5.477 + \item {\tt fe}, \bold{11}
5.478 + \item {\tt fes}, \bold{11}
5.479 \item files
5.480 - \subitem reading, 2, 49
5.481 - \item {\ptt filt_resolve_tac}, \bold{23}
5.482 - \item {\ptt FILTER}, \bold{28}
5.483 - \item {\ptt filter_goal}, \bold{14}
5.484 - \item {\ptt filter_thms}, \bold{23}
5.485 - \item {\ptt findE}, \bold{9}
5.486 - \item {\ptt findEs}, \bold{9}
5.487 - \item {\ptt findI}, \bold{8}
5.488 - \item {\ptt finish_html}, \bold{54}
5.489 - \item {\ptt FIRST}, \bold{27}
5.490 - \item {\ptt FIRST'}, 33
5.491 - \item {\ptt FIRST1}, \bold{33}
5.492 - \item {\ptt FIRSTGOAL}, \bold{32}
5.493 - \item flex-flex constraints, 20, 37, 44
5.494 - \item {\ptt flexflex_rule}, \bold{44}
5.495 - \item {\ptt flexflex_tac}, \bold{21}
5.496 - \item {\ptt fold_goals_tac}, \bold{19}
5.497 - \item {\ptt fold_tac}, \bold{19}
5.498 - \item {\ptt forall_elim}, \bold{42}
5.499 - \item {\ptt forall_elim_list}, \bold{42}
5.500 - \item {\ptt forall_elim_var}, \bold{42}
5.501 - \item {\ptt forall_elim_vars}, \bold{42}
5.502 - \item {\ptt forall_intr}, \bold{41}
5.503 - \item {\ptt forall_intr_frees}, \bold{42}
5.504 - \item {\ptt forall_intr_list}, \bold{42}
5.505 - \item {\ptt force_strip_shyps}, \bold{37}
5.506 - \item {\ptt forw_inst_tac}, \bold{17}
5.507 - \item forward proof, 15, 16, 35
5.508 - \item {\ptt forward_tac}, \bold{16}
5.509 - \item {\ptt fr}, \bold{11}
5.510 - \item {\ptt Free}, \bold{56}, 79
5.511 - \item {\ptt freezeT}, \bold{42}
5.512 - \item {\ptt frs}, \bold{11}
5.513 - \item {\ptt Full_simp_tac}, \bold{94}, 100
5.514 - \item {\ptt full_simp_tac}, \bold{99}, 100
5.515 - \item {\ptt fun} type, 59
5.516 - \item function applications, \bold{56}
5.517 + \subitem reading, 3, 52
5.518 + \item {\tt filt_resolve_tac}, \bold{24}
5.519 + \item {\tt FILTER}, \bold{30}
5.520 + \item {\tt filter_goal}, \bold{15}
5.521 + \item {\tt filter_thms}, \bold{25}
5.522 + \item {\tt findE}, \bold{9}
5.523 + \item {\tt findEs}, \bold{9}
5.524 + \item {\tt findI}, \bold{9}
5.525 + \item {\tt FIRST}, \bold{29}
5.526 + \item {\tt FIRST'}, 35
5.527 + \item {\tt FIRST1}, \bold{35}
5.528 + \item {\tt FIRSTGOAL}, \bold{34}
5.529 + \item flex-flex constraints, 22, 39, 47
5.530 + \item {\tt flexflex_rule}, \bold{47}
5.531 + \item {\tt flexflex_tac}, \bold{22}
5.532 + \item {\tt fold_goals_tac}, \bold{20}
5.533 + \item {\tt fold_tac}, \bold{20}
5.534 + \item {\tt forall_elim}, \bold{44}
5.535 + \item {\tt forall_elim_list}, \bold{44}
5.536 + \item {\tt forall_elim_var}, \bold{44}
5.537 + \item {\tt forall_elim_vars}, \bold{45}
5.538 + \item {\tt forall_intr}, \bold{44}
5.539 + \item {\tt forall_intr_frees}, \bold{44}
5.540 + \item {\tt forall_intr_list}, \bold{44}
5.541 + \item {\tt force_strip_shyps}, \bold{40}
5.542 + \item {\tt forw_inst_tac}, \bold{18}
5.543 + \item forward proof, 17, 37
5.544 + \item {\tt forward_tac}, \bold{17}
5.545 + \item {\tt fr}, \bold{11}
5.546 + \item {\tt Free}, \bold{57}, 82
5.547 + \item {\tt freezeT}, \bold{45}
5.548 + \item {\tt frs}, \bold{11}
5.549 + \item {\tt Full_simp_tac}, \bold{100}, 105
5.550 + \item {\tt full_simp_tac}, 105, \bold{106}
5.551 + \item {\tt fun} type, 60
5.552 + \item function applications, \bold{57}
5.553
5.554 \indexspace
5.555
5.556 - \item {\ptt get_axiom}, \bold{51}
5.557 - \item {\ptt get_thm}, \bold{51}
5.558 - \item {\ptt getgoal}, \bold{14}
5.559 - \item {\ptt gethyps}, \bold{14}, 31
5.560 - \item {\ptt goal}, \bold{7}, 13
5.561 - \item {\ptt goals_limit}, \bold{10}
5.562 - \item {\ptt goalw}, \bold{7}
5.563 - \item {\ptt goalw_cterm}, \bold{7}
5.564 + \item {\tt get_axiom}, \bold{55}
5.565 + \item {\tt get_thm}, \bold{55}
5.566 + \item {\tt getgoal}, \bold{15}
5.567 + \item {\tt gethyps}, \bold{15}, 33
5.568 + \item {\tt goal}, \bold{7}, 13
5.569 + \item {\tt goals_limit}, \bold{10}
5.570 + \item {\tt goalw}, \bold{7}
5.571 + \item {\tt goalw_cterm}, \bold{7}
5.572
5.573 \indexspace
5.574
5.575 - \item {\ptt has_fewer_prems}, \bold{30}
5.576 - \item HTML, \bold{53}
5.577 - \item {\ptt hyp_subst_tac}, \bold{91}
5.578 - \item {\ptt hyp_subst_tacs}, \bold{122}
5.579 - \item {\ptt HypsubstFun}, 92, 122
5.580 + \item {\tt has_fewer_prems}, \bold{32}
5.581 + \item {\tt hyp_subst_tac}, \bold{96}
5.582 + \item {\tt hyp_subst_tacs}, \bold{129}
5.583 + \item {\tt HypsubstFun}, 97, 129
5.584
5.585 \indexspace
5.586
5.587 - \item {\ptt id} nonterminal, \bold{65}, 77, 84
5.588 - \item identifiers, 65
5.589 - \item {\ptt idt} nonterminal, 83
5.590 - \item {\ptt idts} nonterminal, \bold{65}, 72
5.591 - \item {\ptt IF_UNSOLVED}, \bold{30}
5.592 - \item {\ptt iff_reflection} theorem, 107
5.593 - \item {\ptt imp_intr} theorem, \bold{92}
5.594 - \item {\ptt implies_elim}, \bold{40}
5.595 - \item {\ptt implies_elim_list}, \bold{40}
5.596 - \item {\ptt implies_intr}, \bold{40}
5.597 - \item {\ptt implies_intr_hyps}, \bold{40}
5.598 - \item {\ptt implies_intr_list}, \bold{40}
5.599 - \item {\ptt incr_boundvars}, \bold{57}, 88
5.600 - \item {\ptt indexname} ML type, 56, 66
5.601 - \item infixes, \bold{71}
5.602 - \item {\ptt init_html}, \bold{54}
5.603 - \item {\ptt insert} constant, 85
5.604 - \item {\ptt inst_step_tac}, \bold{120}
5.605 - \item {\ptt instantiate}, \bold{42}
5.606 - \item instantiation, 16, 36, 42
5.607 - \item {\ptt INTLEAVE}, \bold{26}, 27
5.608 - \item {\ptt INTLEAVE'}, 33
5.609 - \item {\ptt invoke_oracle}, \bold{60}
5.610 - \item {\ptt is} nonterminal, 85
5.611 + \item {\tt id} nonterminal, \bold{66}, 80, 87
5.612 + \item identifiers, 66
5.613 + \item {\tt idt} nonterminal, 86
5.614 + \item {\tt idts} nonterminal, \bold{66}, 74
5.615 + \item {\tt IF_UNSOLVED}, \bold{32}
5.616 + \item {\tt iff_reflection} theorem, 113
5.617 + \item {\tt imp_intr} theorem, \bold{97}
5.618 + \item {\tt implies_elim}, \bold{43}
5.619 + \item {\tt implies_elim_list}, \bold{43}
5.620 + \item {\tt implies_intr}, \bold{42}
5.621 + \item {\tt implies_intr_hyps}, \bold{43}
5.622 + \item {\tt implies_intr_list}, \bold{42}
5.623 + \item {\tt incr_boundvars}, \bold{58}, 92
5.624 + \item {\tt indexname} ML type, 57, 67
5.625 + \item infixes, \bold{73}
5.626 + \item {\tt insert} constant, 88
5.627 + \item {\tt inst_step_tac}, \bold{127}
5.628 + \item {\tt instance} section, 51
5.629 + \item {\tt instantiate}, \bold{45}
5.630 + \item instantiation, 17, 38, 45
5.631 + \item {\tt INTLEAVE}, \bold{28}, 30
5.632 + \item {\tt INTLEAVE'}, 35
5.633 + \item {\tt invoke_oracle}, \bold{61}
5.634 + \item {\tt is} nonterminal, 88
5.635
5.636 \indexspace
5.637
5.638 - \item {\ptt joinrules}, \bold{121}
5.639 + \item {\tt joinrules}, \bold{128}
5.640
5.641 \indexspace
5.642
5.643 - \item {\ptt keep_derivs}, \bold{45}
5.644 + \item {\tt keep_derivs}, \bold{48}
5.645
5.646 \indexspace
5.647
5.648 - \item $\lambda$-abstractions, 22, \bold{56}
5.649 - \item $\lambda$-calculus, 39, 41, 65
5.650 - \item {\ptt lessb}, \bold{22}
5.651 - \item lexer, \bold{65}
5.652 - \item {\ptt lift_rule}, \bold{44}
5.653 - \item lifting, 44
5.654 - \item {\ptt loadpath}, \bold{49}
5.655 - \item {\ptt logic} class, 63, 65, 69
5.656 - \item {\ptt logic} nonterminal, \bold{63}
5.657 - \item {\ptt Logic.auto_rename}, \bold{20}
5.658 - \item {\ptt Logic.set_rename_prefix}, \bold{20}
5.659 - \item {\ptt loose_bnos}, \bold{57}, 89
5.660 + \item $\lambda$-abstractions, 24, \bold{57}
5.661 + \item $\lambda$-calculus, 42, 43, 66
5.662 + \item {\tt lessb}, \bold{23}
5.663 + \item lexer, \bold{66}
5.664 + \item {\tt lift_rule}, \bold{46}
5.665 + \item lifting, 46
5.666 + \item {\tt loadpath}, \bold{53}
5.667 + \item {\tt logic} class, 66, 71
5.668 + \item {\tt logic} nonterminal, \bold{66}
5.669 + \item {\tt Logic.auto_rename}, \bold{21}
5.670 + \item {\tt Logic.set_rename_prefix}, \bold{21}
5.671 + \item {\tt loose_bnos}, \bold{58}, 93
5.672
5.673 \indexspace
5.674
5.675 - \item macros, 81--86
5.676 - \item {\ptt make-all} shell script, 5
5.677 - \item {\ptt make_elim}, \bold{37}, 117
5.678 - \item {\ptt make_html}, \bold{54}
5.679 - \item {\ptt Match} exception, 88, 92
5.680 - \item {\ptt match_tac}, \bold{16}, 116
5.681 - \item {\ptt max_pri}, 63, \bold{69}
5.682 - \item {\ptt merge_ss}, 100
5.683 - \item {\ptt merge_theories}, \bold{52}, \fnote{75}
5.684 - \item meta-assumptions, 31, 39, 40, 43
5.685 - \subitem printing of, 3
5.686 - \item meta-equality, 39--41
5.687 - \item meta-implication, 39, 40
5.688 - \item meta-quantifiers, 40, 41
5.689 - \item meta-rewriting, 7, 11, 12, \bold{18},
5.690 - \seealso{tactics, theorems}{123}
5.691 - \subitem in terms, 44
5.692 - \subitem in theorems, 35
5.693 - \item meta-rules, \see{meta-rules}{0}, 39--44
5.694 - \item {\ptt METAHYPS}, 14, \bold{31}
5.695 - \item mixfix declarations, 47, 68--72
5.696 - \item {\ptt mk_case_split_tac}, \bold{111}
5.697 - \item {\ptt ML} section, 48, 87, 89
5.698 - \item {\ptt mp} theorem, \bold{122}
5.699 - \item {\ptt mp_tac}, \bold{121}
5.700 - \item {\ptt MRL}, \bold{35}
5.701 - \item {\ptt MRS}, \bold{35}
5.702 + \item macros, 84--90
5.703 + \item {\tt make_elim}, \bold{39}, 123
5.704 + \item {\tt Match} exception, 91, 97
5.705 + \item {\tt match_tac}, \bold{17}, 122
5.706 + \item {\tt max_pri}, 64, \bold{70}
5.707 + \item {\tt merge_ss}, 105
5.708 + \item {\tt merge_theories}, \bold{55}
5.709 + \item meta-assumptions, 33, 41, 42, 45
5.710 + \subitem printing of, 4
5.711 + \item meta-equality, 41, 43
5.712 + \item meta-implication, 41, 42
5.713 + \item meta-quantifiers, 42, 44
5.714 + \item meta-rewriting, 7, 12, 13, \bold{20},
5.715 + \seealso{tactics, theorems}{130}
5.716 + \subitem in terms, 47
5.717 + \subitem in theorems, 38
5.718 + \item meta-rules, \see{meta-rules}{1}, 41--47
5.719 + \item {\tt METAHYPS}, 15, \bold{33}
5.720 + \item mixfix declarations, 50, 69--74
5.721 + \item {\tt mk_case_split_tac}, \bold{116}
5.722 + \item {\tt ML} section, 51, 91, 93
5.723 + \item {\tt mp} theorem, \bold{129}
5.724 + \item {\tt mp_tac}, \bold{128}
5.725 + \item {\tt MRL}, \bold{37}
5.726 + \item {\tt MRS}, \bold{37}
5.727
5.728 \indexspace
5.729
5.730 - \item name tokens, \bold{65}
5.731 - \item {\ptt net_bimatch_tac}, \bold{23}
5.732 - \item {\ptt net_biresolve_tac}, \bold{23}
5.733 - \item {\ptt net_match_tac}, \bold{23}
5.734 - \item {\ptt net_resolve_tac}, \bold{22}
5.735 - \item {\ptt no_tac}, \bold{27}
5.736 - \item {\ptt None}, \bold{24}
5.737 - \item {\ptt not_elim} theorem, \bold{122}
5.738 - \item {\ptt nprems_of}, \bold{37}
5.739 - \item numerals, 65
5.740 + \item name tokens, \bold{66}
5.741 + \item {\tt net_bimatch_tac}, \bold{24}
5.742 + \item {\tt net_biresolve_tac}, \bold{24}
5.743 + \item {\tt net_match_tac}, \bold{24}
5.744 + \item {\tt net_resolve_tac}, \bold{24}
5.745 + \item {\tt no_tac}, \bold{30}
5.746 + \item {\tt None}, \bold{26}
5.747 + \item {\tt not_elim} theorem, \bold{129}
5.748 + \item {\tt nprems_of}, \bold{39}
5.749 + \item numerals, 66
5.750
5.751 \indexspace
5.752
5.753 - \item {\ptt o} type, 73
5.754 - \item {\ptt op} symbol, 71
5.755 - \item {\ptt option} ML type, 24
5.756 - \item oracles, 60--61
5.757 - \item {\ptt ORELSE}, \bold{26}, 27, 28, 32
5.758 - \item {\ptt ORELSE'}, 33
5.759 + \item {\tt o} type, 76
5.760 + \item {\tt op} symbol, 73
5.761 + \item {\tt option} ML type, 26
5.762 + \item oracles, 61--62
5.763 + \item {\tt ORELSE}, \bold{28}, 30, 34
5.764 + \item {\tt ORELSE'}, 35
5.765
5.766 \indexspace
5.767
5.768 \item parameters
5.769 - \subitem removing unused, 20
5.770 - \subitem renaming, 11, 19, 44
5.771 - \item {\ptt parents_of}, \bold{52}
5.772 - \item parse trees, 76
5.773 - \item {\ptt parse_ast_translation}, 87
5.774 - \item {\ptt parse_rules}, 83
5.775 - \item {\ptt parse_translation}, 87
5.776 - \item {\ptt pause_tac}, \bold{24}
5.777 - \item Poly/{\ML} compiler, 1, 2, 4, 50
5.778 - \item {\ptt pop_proof}, \bold{13}
5.779 - \item {\ptt pr}, \bold{10}
5.780 - \item {\ptt premises}, \bold{7}, 13
5.781 - \item {\ptt prems_of}, \bold{37}
5.782 - \item {\ptt prems_of_ss}, 100
5.783 - \item pretty printing, 68, 71, 85
5.784 - \item {\ptt Pretty.setdepth}, \bold{3}
5.785 - \item {\ptt Pretty.setmargin}, \bold{3}
5.786 - \item {\ptt PRIMITIVE}, \bold{24}
5.787 - \item {\ptt primrec}, 95
5.788 - \item {\ptt prin}, 4, \bold{14}
5.789 - \item {\ptt print_ast_translation}, 87
5.790 - \item {\ptt print_cs}, \bold{116}
5.791 - \item {\ptt print_depth}, \bold{3}
5.792 - \item {\ptt print_exn}, \bold{4}, 34
5.793 - \item {\ptt print_goals}, \bold{35}
5.794 - \item {\ptt print_rules}, 83
5.795 - \item {\ptt print_syntax}, \bold{66}
5.796 - \item {\ptt print_tac}, \bold{24}
5.797 - \item {\ptt print_theory}, \bold{52}
5.798 - \item {\ptt print_thm}, \bold{35}
5.799 - \item {\ptt print_translation}, 87
5.800 + \subitem removing unused, 22
5.801 + \subitem renaming, 12, 21, 47
5.802 + \item {\tt parents_of}, \bold{56}
5.803 + \item parse trees, 79
5.804 + \item {\tt parse_ast_translation}, 91
5.805 + \item {\tt parse_rules}, 86
5.806 + \item {\tt parse_translation}, 91
5.807 + \item {\tt pause_tac}, \bold{26}
5.808 + \item Poly/{\ML} compiler, 5
5.809 + \item {\tt pop_proof}, \bold{14}
5.810 + \item {\tt pr}, \bold{10}
5.811 + \item {\tt premises}, \bold{7}, 14
5.812 + \item {\tt prems_of}, \bold{39}
5.813 + \item {\tt prems_of_ss}, 105
5.814 + \item pretty printing, 70, 72--73, 89
5.815 + \item {\tt Pretty.setdepth}, \bold{3}
5.816 + \item {\tt Pretty.setmargin}, \bold{3}
5.817 + \item {\tt PRIMITIVE}, \bold{25}
5.818 + \item {\tt primrec}, 100
5.819 + \item {\tt prin}, 5, \bold{14}
5.820 + \item print mode, 50, 93
5.821 + \item print modes, 74--75
5.822 + \item {\tt print_ast_translation}, 91
5.823 + \item {\tt print_cs}, \bold{122}
5.824 + \item {\tt print_depth}, \bold{4}
5.825 + \item {\tt print_exn}, \bold{5}, 36
5.826 + \item {\tt print_goals}, \bold{37}
5.827 + \item {\tt print_mode}, 74
5.828 + \item {\tt print_modes}, 69
5.829 + \item {\tt print_rules}, 86
5.830 + \item {\tt print_syntax}, \bold{56}, \bold{68}
5.831 + \item {\tt print_tac}, \bold{26}
5.832 + \item {\tt print_theory}, \bold{56}
5.833 + \item {\tt print_thm}, \bold{37}
5.834 + \item {\tt print_translation}, 91
5.835 \item printing control, 3--4
5.836 - \item {\ptt printyp}, \bold{14}
5.837 - \item priorities, 62, \bold{69}
5.838 - \item priority grammars, 62--63
5.839 - \item {\ptt prlev}, \bold{10}
5.840 - \item {\ptt prlim}, \bold{10}
5.841 - \item productions, 62, 67, 68
5.842 - \subitem copy, \bold{67}, 68, 77
5.843 - \item {\ptt proof} ML type, 13
5.844 - \item proof objects, 44--45
5.845 + \item {\tt printyp}, \bold{14}
5.846 + \item priorities, 63, \bold{70}
5.847 + \item priority grammars, 63--64
5.848 + \item {\tt prlev}, \bold{10}
5.849 + \item {\tt prlim}, \bold{10}
5.850 + \item productions, 63, 69, 70
5.851 + \subitem copy, \bold{69}, 70, 81
5.852 + \item {\tt proof} ML type, 14
5.853 + \item proof objects, 47--48
5.854 \item proof state, 6
5.855 - \subitem printing of, 9
5.856 - \item {\ptt proof_timing}, \bold{10}
5.857 - \item proofs, 6--14
5.858 - \subitem inspecting the state, 14
5.859 - \subitem managing multiple, 12
5.860 - \subitem saving and restoring, 13
5.861 + \subitem printing of, 10
5.862 + \item {\tt proof_timing}, \bold{10}
5.863 + \item proofs, 6--15
5.864 + \subitem inspecting the state, 15
5.865 + \subitem managing multiple, 13
5.866 + \subitem saving and restoring, 14
5.867 \subitem stacking, 13
5.868 \subitem starting, 6
5.869 \subitem timing, 10
5.870 - \item {\ptt PROP} symbol, 64
5.871 - \item {\ptt prop} nonterminal, \bold{63}, 73
5.872 - \item {\ptt prop} type, 59, 63
5.873 - \item {\ptt prove_goal}, 10, \bold{12}
5.874 - \item {\ptt prove_goalw}, \bold{12}
5.875 - \item {\ptt prove_goalw_cterm}, \bold{12}
5.876 - \item {\ptt prth}, \bold{34}
5.877 - \item {\ptt prthq}, \bold{35}
5.878 - \item {\ptt prths}, \bold{34}
5.879 - \item {\ptt prune_params_tac}, \bold{21}
5.880 - \item {\ptt Pure} theory, 46, 63, 67
5.881 - \item {\ptt pure_thy}, \bold{52}
5.882 - \item {\ptt push_proof}, \bold{13}
5.883 - \item {\ptt pwd}, \bold{2}
5.884 + \item {\tt PROP} symbol, 65
5.885 + \item {\tt prop} nonterminal, \bold{64}, 76
5.886 + \item {\tt prop} type, 60, 66
5.887 + \item {\tt prove_goal}, 10, \bold{12}
5.888 + \item {\tt prove_goalw}, \bold{13}
5.889 + \item {\tt prove_goalw_cterm}, \bold{13}
5.890 + \item {\tt prth}, \bold{36}
5.891 + \item {\tt prthq}, \bold{37}
5.892 + \item {\tt prths}, \bold{37}
5.893 + \item {\tt prune_params_tac}, \bold{22}
5.894 + \item {\tt Pure} theory, 49, 64, 68
5.895 + \item {\tt Pure.thy}, \bold{55}
5.896 + \item {\tt push_proof}, \bold{14}
5.897 + \item {\tt pwd}, \bold{3}
5.898
5.899 \indexspace
5.900
5.901 - \item {\ptt qed}, 8, \bold{8}
5.902 - \item {\ptt qed_goal}, \bold{12}
5.903 - \item {\ptt qed_goalw}, \bold{12}
5.904 - \item quantifiers, 72
5.905 - \item {\ptt quit}, \bold{2}
5.906 + \item {\tt qed}, \bold{8}, 9
5.907 + \item {\tt qed_goal}, \bold{13}
5.908 + \item {\tt qed_goalw}, \bold{13}
5.909 + \item quantifiers, 74
5.910 + \item {\tt quit}, \bold{2}
5.911
5.912 \indexspace
5.913
5.914 - \item {\ptt read}, \bold{14}
5.915 - \item {\ptt read_axm}, \bold{58}
5.916 - \item {\ptt read_cterm}, \bold{58}
5.917 - \item {\ptt read_instantiate}, \bold{36}
5.918 - \item {\ptt read_instantiate_sg}, \bold{36}
5.919 + \item {\tt read}, \bold{14}
5.920 + \item {\tt read_axm}, \bold{59}
5.921 + \item {\tt read_cterm}, \bold{59}
5.922 + \item {\tt read_instantiate}, \bold{38}
5.923 + \item {\tt read_instantiate_sg}, \bold{38}
5.924 \item reading
5.925 - \subitem axioms, \see{{\tt assume_ax}}{46}
5.926 + \subitem axioms, \see{{\tt assume_ax}}{49}
5.927 \subitem goals, \see{proofs, starting}{6}
5.928 - \item {\ptt reflexive}, \bold{41}
5.929 - \item {\ptt ren}, \bold{11}
5.930 - \item {\ptt rename_last_tac}, \bold{20}
5.931 - \item {\ptt rename_params_rule}, \bold{44}
5.932 - \item {\ptt rename_tac}, \bold{20}
5.933 - \item {\ptt rep_cterm}, \bold{58}
5.934 - \item {\ptt rep_ctyp}, \bold{59}
5.935 - \item {\ptt rep_ss}, 100
5.936 - \item {\ptt rep_thm}, \bold{37}
5.937 - \item {\ptt REPEAT}, \bold{27, 28}
5.938 - \item {\ptt REPEAT1}, \bold{27}
5.939 - \item {\ptt REPEAT_DETERM}, \bold{27}
5.940 - \item {\ptt REPEAT_FIRST}, \bold{32}
5.941 - \item {\ptt REPEAT_SOME}, \bold{32}
5.942 - \item {\ptt res_inst_tac}, \bold{17}, 21
5.943 - \item reserved words, 65, 86
5.944 - \item resolution, 35, 43
5.945 - \subitem tactics, 15
5.946 - \subitem without lifting, 43
5.947 - \item {\ptt resolve_tac}, \bold{15}, 116
5.948 - \item {\ptt restore_proof}, \bold{13}
5.949 - \item {\ptt result}, \bold{8}, 14, 52
5.950 - \item {\ptt rev_mp} theorem, \bold{92}
5.951 - \item rewrite rules, 96--97
5.952 - \subitem permutative, 104--107
5.953 - \item {\ptt rewrite_cterm}, \bold{44}
5.954 - \item {\ptt rewrite_goals_rule}, \bold{36}
5.955 - \item {\ptt rewrite_goals_tac}, \bold{19}, 36
5.956 - \item {\ptt rewrite_rule}, \bold{36}
5.957 - \item {\ptt rewrite_tac}, 8, \bold{19}
5.958 + \item {\tt reflexive}, \bold{43}
5.959 + \item {\tt ren}, \bold{12}
5.960 + \item {\tt rename_last_tac}, \bold{21}
5.961 + \item {\tt rename_params_rule}, \bold{46}
5.962 + \item {\tt rename_tac}, \bold{21}
5.963 + \item {\tt rep_cterm}, \bold{59}
5.964 + \item {\tt rep_ctyp}, \bold{61}
5.965 + \item {\tt rep_ss}, 105
5.966 + \item {\tt rep_thm}, \bold{40}
5.967 + \item {\tt REPEAT}, \bold{29, 30}
5.968 + \item {\tt REPEAT1}, \bold{29}
5.969 + \item {\tt REPEAT_DETERM}, \bold{29}
5.970 + \item {\tt REPEAT_FIRST}, \bold{34}
5.971 + \item {\tt REPEAT_SOME}, \bold{34}
5.972 + \item {\tt res_inst_tac}, \bold{18}, 22
5.973 + \item reserved words, 66, 89
5.974 + \item {\tt reset}, 3
5.975 + \item resolution, 37, 45
5.976 + \subitem tactics, 16
5.977 + \subitem without lifting, 46
5.978 + \item {\tt resolve_tac}, \bold{16}, 122
5.979 + \item {\tt restore_proof}, \bold{14}
5.980 + \item {\tt result}, \bold{8}, 15, 55
5.981 + \item {\tt rev_mp} theorem, \bold{97}
5.982 + \item rewrite rules, 101--102
5.983 + \subitem permutative, 110--113
5.984 + \item {\tt rewrite_cterm}, \bold{47}
5.985 + \item {\tt rewrite_goals_rule}, \bold{38}
5.986 + \item {\tt rewrite_goals_tac}, \bold{20}, 38
5.987 + \item {\tt rewrite_rule}, \bold{38}
5.988 + \item {\tt rewrite_tac}, 8, \bold{20}
5.989 \item rewriting
5.990 - \subitem object-level, \see{simplification}{0}
5.991 - \subitem ordered, 104
5.992 - \subitem syntactic, 81--86
5.993 - \item {\ptt rewtac}, \bold{18}
5.994 - \item {\ptt RL}, \bold{35}
5.995 - \item {\ptt RLN}, \bold{35}
5.996 - \item {\ptt rotate_proof}, \bold{13}
5.997 - \item {\ptt rotate_tac}, \bold{20}
5.998 - \item {\ptt RS}, \bold{35}
5.999 - \item {\ptt RSN}, \bold{35}
5.1000 - \item {\ptt rtac}, \bold{17}
5.1001 - \item {\ptt rule_by_tactic}, 21, \bold{37}
5.1002 + \subitem object-level, \see{simplification}{1}
5.1003 + \subitem ordered, 110
5.1004 + \subitem syntactic, 84--90
5.1005 + \item {\tt rewtac}, \bold{19}
5.1006 + \item {\tt RL}, \bold{37}
5.1007 + \item {\tt RLN}, \bold{37}
5.1008 + \item {\tt rotate_proof}, \bold{14}
5.1009 + \item {\tt rotate_tac}, \bold{22}
5.1010 + \item {\tt RS}, \bold{37}
5.1011 + \item {\tt RSN}, \bold{37}
5.1012 + \item {\tt rtac}, \bold{19}
5.1013 + \item {\tt rule_by_tactic}, 22, \bold{39}
5.1014 \item rules
5.1015 - \subitem converting destruction to elimination, 37
5.1016 + \subitem converting destruction to elimination, 39
5.1017
5.1018 \indexspace
5.1019
5.1020 - \item {\ptt safe_asm_full_simp_tac}, \bold{98}, 100
5.1021 - \item {\ptt safe_step_tac}, 117, \bold{120}
5.1022 - \item {\ptt safe_tac}, \bold{120}
5.1023 - \item {\ptt save_proof}, \bold{13}
5.1024 + \item {\tt safe_asm_full_simp_tac}, \bold{104}, 105
5.1025 + \item {\tt safe_step_tac}, 123, \bold{126}
5.1026 + \item {\tt safe_tac}, \bold{127}
5.1027 + \item {\tt save_proof}, \bold{14}
5.1028 \item saving your work, \bold{1}
5.1029 - \item search, 26
5.1030 - \subitem tacticals, 28--30
5.1031 - \item {\ptt SELECT_GOAL}, 19, \bold{30}
5.1032 - \item {\ptt Sequence.seq} ML type, 23
5.1033 - \item sequences (lazy lists), \bold{24}
5.1034 - \item sequent calculus, 112
5.1035 + \item search, 28
5.1036 + \subitem tacticals, 30--32
5.1037 + \item {\tt SELECT_GOAL}, 20, \bold{33}
5.1038 + \item {\tt Sequence.seq} ML type, 25
5.1039 + \item sequences (lazy lists), \bold{26}
5.1040 + \item sequent calculus, 118
5.1041 \item sessions, 1--5
5.1042 - \item {\ptt set_current_thy}, 96
5.1043 - \item {\ptt set_oracle}, \bold{60}
5.1044 - \item {\ptt setloop}, 99, 100
5.1045 - \item {\ptt setmksimps}, 96, 100, 110
5.1046 - \item {\ptt setSolver}, 98, 100, 110
5.1047 - \item {\ptt setSSolver}, 98, 100, 110
5.1048 - \item {\ptt setsubgoaler}, 98, 100, 110
5.1049 - \item {\ptt setSWrapper}, \bold{118}
5.1050 - \item {\ptt setWrapper}, \bold{118}
5.1051 - \item shell scripts, \bold{4}
5.1052 + \item {\tt set}, 3
5.1053 + \item {\tt set_current_thy}, 101
5.1054 + \item {\tt set_oracle}, \bold{61}
5.1055 + \item {\tt setloop}, 104, 105
5.1056 + \item {\tt setmksimps}, 102, 105, 116
5.1057 + \item {\tt setSolver}, 104, 105, 116
5.1058 + \item {\tt setSSolver}, 104, 105, 116
5.1059 + \item {\tt setsubgoaler}, 103, 105, 116
5.1060 + \item {\tt setSWrapper}, \bold{124}
5.1061 + \item {\tt setWrapper}, \bold{124}
5.1062 \item shortcuts
5.1063 - \subitem for tactics, 17
5.1064 + \subitem for tactics, 18
5.1065 \subitem for {\tt by} commands, 10
5.1066 - \item {\ptt show_brackets}, \bold{3}
5.1067 - \item {\ptt show_hyps}, \bold{3}
5.1068 - \item {\ptt show_sorts}, \bold{3}, 80
5.1069 - \item {\ptt show_types}, \bold{3}, 80, 83, 89
5.1070 - \item {\ptt Sign.cterm_of}, 7, 12
5.1071 - \item {\ptt Sign.sg} ML type, 46
5.1072 - \item {\ptt Sign.string_of_term}, \bold{58}
5.1073 - \item {\ptt Sign.string_of_typ}, \bold{59}
5.1074 - \item {\ptt sign_of}, 7, 12, \bold{52}
5.1075 - \item signatures, \bold{46}, 53, 57--59
5.1076 - \item {\ptt Simp_tac}, \bold{94}, 100
5.1077 - \item {\ptt simp_tac}, \bold{99}, 100
5.1078 - \item simplification, 94--111
5.1079 - \subitem from classical reasoner, 117
5.1080 - \subitem setting up, 107
5.1081 - \subitem tactics, 99
5.1082 - \item simplification sets, 96
5.1083 + \item {\tt show_brackets}, \bold{4}
5.1084 + \item {\tt show_hyps}, \bold{4}
5.1085 + \item {\tt show_sorts}, \bold{4}, 83
5.1086 + \item {\tt show_types}, \bold{4}, 83, 86, 93
5.1087 + \item {\tt Sign.sg} ML type, 49
5.1088 + \item {\tt Sign.string_of_term}, \bold{59}
5.1089 + \item {\tt Sign.string_of_typ}, \bold{60}
5.1090 + \item {\tt sign_of}, 7, 13, \bold{56}
5.1091 + \item signatures, \bold{49}, 56, 58, 59, 61
5.1092 + \item {\tt Simp_tac}, \bold{99}, 105
5.1093 + \item {\tt simp_tac}, 105, \bold{106}
5.1094 + \item simplification, 99--117
5.1095 + \subitem from classical reasoner, 124
5.1096 + \subitem setting up, 113
5.1097 + \subitem tactics, 106
5.1098 + \item simplification sets, 101
5.1099 \item simpset
5.1100 - \subitem current, 94, 96, 99
5.1101 - \item {\ptt simpset}, 100
5.1102 - \item {\ptt simpset} ML type, 100
5.1103 - \item {\tt simpset} ML value, 96
5.1104 - \item {\ptt simpset_of}, 101
5.1105 - \item {\ptt size_of_thm}, 29, \bold{30}, 122
5.1106 - \item {\ptt sizef}, \bold{122}
5.1107 - \item {\ptt slow_best_tac}, \bold{119}
5.1108 - \item {\ptt slow_step_tac}, 117, \bold{120}
5.1109 - \item {\ptt slow_tac}, \bold{119}
5.1110 - \item {\ptt Some}, \bold{24}
5.1111 - \item {\ptt SOMEGOAL}, \bold{32}
5.1112 - \item {\ptt sort} nonterminal, \bold{65}
5.1113 - \item sort constraints, 64
5.1114 - \item sort hypotheses, 37
5.1115 + \subitem current, 99, 101, 106
5.1116 + \item {\tt simpset}, 105
5.1117 + \item {\tt simpset} ML type, 105
5.1118 + \item {\tt simpset} ML value, 101
5.1119 + \item {\tt simpset_of}, 106
5.1120 + \item {\tt size_of_thm}, 31, \bold{32}, 129
5.1121 + \item {\tt sizef}, \bold{129}
5.1122 + \item {\tt slow_best_tac}, \bold{126}
5.1123 + \item {\tt slow_step_tac}, 123, \bold{127}
5.1124 + \item {\tt slow_tac}, \bold{126}
5.1125 + \item {\tt Some}, \bold{26}
5.1126 + \item {\tt SOMEGOAL}, \bold{34}
5.1127 + \item {\tt sort} nonterminal, \bold{66}
5.1128 + \item sort constraints, 65
5.1129 + \item sort hypotheses, 40
5.1130 \item sorts
5.1131 - \subitem printing of, 3
5.1132 - \item {\ptt split_tac}, \bold{111}
5.1133 - \item {\ptt ssubst} theorem, \bold{90}
5.1134 - \item {\ptt stac}, \bold{91}
5.1135 - \item stamps, 37, \bold{46}, 53
5.1136 - \item {\ptt stamps_of_thm}, \bold{37}
5.1137 - \item {\ptt stamps_of_thy}, \bold{53}
5.1138 - \item {\ptt standard}, \bold{36}
5.1139 + \subitem printing of, 4
5.1140 + \item {\tt split_tac}, \bold{116}
5.1141 + \item {\tt ssubst} theorem, \bold{95}
5.1142 + \item {\tt stac}, \bold{96}
5.1143 + \item stamps, 39, \bold{49}, 56
5.1144 + \item {\tt stamps_of_thm}, \bold{39}
5.1145 + \item {\tt stamps_of_thy}, \bold{56}
5.1146 + \item {\tt standard}, \bold{39}
5.1147 \item starting up, \bold{1}
5.1148 - \item {\ptt STATE}, \bold{24}
5.1149 - \item {\ptt Step_tac}, \bold{121}
5.1150 - \item {\ptt step_tac}, 117, \bold{120}
5.1151 - \item {\ptt store_thm}, \bold{8}
5.1152 - \item {\ptt string_of_cterm}, \bold{58}
5.1153 - \item {\ptt string_of_ctyp}, \bold{59}
5.1154 - \item {\ptt string_of_thm}, \bold{35}
5.1155 - \item strings, 65
5.1156 - \item {\ptt SUBGOAL}, \bold{24}
5.1157 - \item subgoal module, 6--14
5.1158 - \item {\ptt subgoal_tac}, \bold{18}
5.1159 - \item {\ptt subgoals_of_brl}, \bold{22}
5.1160 - \item {\ptt subgoals_tac}, \bold{18}
5.1161 - \item {\ptt subst} theorem, 90, \bold{92}
5.1162 + \item {\tt STATE}, \bold{25}
5.1163 + \item {\tt Step_tac}, \bold{127}
5.1164 + \item {\tt step_tac}, 123, \bold{127}
5.1165 + \item {\tt store_thm}, \bold{8}
5.1166 + \item {\tt string_of_cterm}, \bold{59}
5.1167 + \item {\tt string_of_ctyp}, \bold{60}
5.1168 + \item {\tt string_of_thm}, \bold{37}
5.1169 + \item strings, 66
5.1170 + \item {\tt SUBGOAL}, \bold{25}
5.1171 + \item subgoal module, 6--15
5.1172 + \item {\tt subgoal_tac}, \bold{19}
5.1173 + \item {\tt subgoals_of_brl}, \bold{23}
5.1174 + \item {\tt subgoals_tac}, \bold{19}
5.1175 + \item {\tt subst} theorem, 95, \bold{97}
5.1176 \item substitution
5.1177 - \subitem rules, 90
5.1178 - \item {\ptt swap} theorem, \bold{122}
5.1179 - \item {\ptt swap_res_tac}, \bold{121}
5.1180 - \item {\ptt swapify}, \bold{121}
5.1181 - \item {\ptt sym} theorem, 91, \bold{92}
5.1182 - \item {\ptt symmetric}, \bold{41}
5.1183 - \item {\ptt syn_of}, \bold{66}
5.1184 + \subitem rules, 95
5.1185 + \item {\tt swap} theorem, \bold{129}
5.1186 + \item {\tt swap_res_tac}, \bold{128}
5.1187 + \item {\tt swapify}, \bold{128}
5.1188 + \item {\tt sym} theorem, 96, \bold{97}
5.1189 + \item {\tt symmetric}, \bold{43}
5.1190 + \item {\tt syn_of}, \bold{68}
5.1191 \item syntax
5.1192 - \subitem Pure, 63--68
5.1193 - \subitem transformations, 76--89
5.1194 - \item {\ptt syntax} section, 47
5.1195 - \item {\ptt Syntax.ast} ML type, 76
5.1196 - \item {\ptt Syntax.print_gram}, \bold{67}
5.1197 - \item {\ptt Syntax.print_syntax}, \bold{66}
5.1198 - \item {\ptt Syntax.print_trans}, \bold{67}
5.1199 - \item {\ptt Syntax.stat_norm_ast}, 84
5.1200 - \item {\ptt Syntax.syntax} ML type, 66
5.1201 - \item {\ptt Syntax.test_read}, 70, 84
5.1202 - \item {\ptt Syntax.trace_norm_ast}, 84
5.1203 + \subitem Pure, 64--69
5.1204 + \subitem transformations, 79--93
5.1205 + \item {\tt syntax} section, 50
5.1206 + \item {\tt Syntax.ast} ML type, 79
5.1207 + \item {\tt Syntax.mark_boundT}, 93
5.1208 + \item {\tt Syntax.print_gram}, \bold{68}
5.1209 + \item {\tt Syntax.print_syntax}, \bold{68}
5.1210 + \item {\tt Syntax.print_trans}, \bold{68}
5.1211 + \item {\tt Syntax.stat_norm_ast}, 88
5.1212 + \item {\tt Syntax.syntax} ML type, 68
5.1213 + \item {\tt Syntax.test_read}, 72, 88
5.1214 + \item {\tt Syntax.trace_norm_ast}, 88
5.1215 + \item {\tt Syntax.variant_abs'}, 93
5.1216
5.1217 \indexspace
5.1218
5.1219 - \item {\ptt Tactic}, \bold{24}
5.1220 - \item {\ptt tactic} ML type, 15
5.1221 - \item tacticals, 26--33
5.1222 - \subitem conditional, 29
5.1223 - \subitem deterministic, 29
5.1224 - \subitem for filtering, 28
5.1225 - \subitem for restriction to a subgoal, 30
5.1226 - \subitem identities for, 27
5.1227 - \subitem joining a list of tactics, 26
5.1228 - \subitem joining tactic functions, 32, 33
5.1229 - \subitem joining two tactics, 26
5.1230 - \subitem repetition, 27
5.1231 - \subitem scanning for subgoals, 31
5.1232 - \subitem searching, 28, 29
5.1233 - \item tactics, 15--25
5.1234 - \subitem assumption, \bold{16}, 17
5.1235 + \item {\tt tactic} ML type, 16
5.1236 + \item tacticals, 28--35
5.1237 + \subitem conditional, 32
5.1238 + \subitem deterministic, 32
5.1239 + \subitem for filtering, 30
5.1240 + \subitem for restriction to a subgoal, 33
5.1241 + \subitem identities for, 29
5.1242 + \subitem joining a list of tactics, 29
5.1243 + \subitem joining tactic functions, 35
5.1244 + \subitem joining two tactics, 28
5.1245 + \subitem repetition, 29
5.1246 + \subitem scanning for subgoals, 34
5.1247 + \subitem searching, 31
5.1248 + \item tactics, 16--27
5.1249 + \subitem assumption, \bold{17}, 18
5.1250 \subitem commands for applying, 7
5.1251 - \subitem debugging, 13
5.1252 - \subitem filtering results of, 28
5.1253 - \subitem for composition, 21
5.1254 - \subitem for contradiction, 121
5.1255 - \subitem for inserting facts, 18
5.1256 - \subitem for Modus Ponens, 121
5.1257 - \subitem instantiation, 16
5.1258 - \subitem matching, 16
5.1259 - \subitem meta-rewriting, 17, \bold{18}
5.1260 - \subitem primitives for coding, 23
5.1261 - \subitem resolution, \bold{15}, 17, 21, 22
5.1262 - \subitem restricting to a subgoal, 30
5.1263 - \subitem simplification, 99
5.1264 - \subitem substitution, 90--93
5.1265 - \subitem tracing, 24
5.1266 - \item {\ptt tapply}, \bold{23}
5.1267 - \item {\ptt teeinput} shell script, 5
5.1268 - \item {\ptt TERM}, 58
5.1269 - \item {\ptt term} ML type, 56, 79
5.1270 - \item terms, \bold{56}
5.1271 - \subitem certified, \bold{57}
5.1272 - \subitem made from ASTs, 79
5.1273 - \subitem printing of, 14, 58
5.1274 + \subitem debugging, 14
5.1275 + \subitem filtering results of, 30
5.1276 + \subitem for composition, 22
5.1277 + \subitem for contradiction, 128
5.1278 + \subitem for inserting facts, 19
5.1279 + \subitem for Modus Ponens, 128
5.1280 + \subitem instantiation, 17
5.1281 + \subitem matching, 17
5.1282 + \subitem meta-rewriting, 18, \bold{20}
5.1283 + \subitem primitives for coding, 25
5.1284 + \subitem resolution, \bold{16}, 18, 23, 24
5.1285 + \subitem restricting to a subgoal, 33
5.1286 + \subitem simplification, 106
5.1287 + \subitem substitution, 95--98
5.1288 + \subitem tracing, 25
5.1289 + \item {\tt TERM}, 59
5.1290 + \item {\tt term} ML type, 57, 82
5.1291 + \item terms, \bold{57}
5.1292 + \subitem certified, \bold{58}
5.1293 + \subitem made from ASTs, 82
5.1294 + \subitem printing of, 14, 59
5.1295 \subitem reading of, 14
5.1296 - \item {\ptt TFree}, \bold{59}
5.1297 - \item {\ptt THEN}, \bold{26}, 27, 32
5.1298 - \item {\ptt THEN'}, 33
5.1299 - \item {\ptt THEN_BEST_FIRST}, \bold{29}
5.1300 - \item theorems, 34--45
5.1301 - \subitem equality of, 30
5.1302 - \subitem extracting, 51
5.1303 + \item {\tt TFree}, \bold{60}
5.1304 + \item {\tt THEN}, \bold{28}, 30, 34
5.1305 + \item {\tt THEN'}, 35
5.1306 + \item {\tt THEN_BEST_FIRST}, \bold{31}
5.1307 + \item theorems, 36--48
5.1308 + \subitem equality of, 32
5.1309 + \subitem extracting, 55
5.1310 \subitem extracting proved, 8
5.1311 - \subitem joining by resolution, 35
5.1312 - \subitem of pure theory, 19
5.1313 - \subitem printing of, 34
5.1314 - \subitem retrieving, 8
5.1315 - \subitem size of, 30
5.1316 - \subitem standardizing, 36
5.1317 + \subitem joining by resolution, 37
5.1318 + \subitem of pure theory, 20
5.1319 + \subitem printing of, 36
5.1320 + \subitem retrieving, 9
5.1321 + \subitem size of, 32
5.1322 + \subitem standardizing, 38
5.1323 \subitem storing, 8
5.1324 - \subitem taking apart, 37
5.1325 - \item theories, 46--61
5.1326 - \subitem axioms of, 51
5.1327 - \subitem constructing, \bold{52}
5.1328 - \subitem inspecting, \bold{52}
5.1329 - \subitem loading, 49
5.1330 - \subitem parent, \bold{46}
5.1331 - \subitem pseudo, \bold{50}
5.1332 - \subitem reloading, \bold{50}
5.1333 - \subitem removing, \bold{50}
5.1334 - \subitem theorems of, 51
5.1335 - \item {\ptt THEORY} exception, 46, 51
5.1336 - \item {\ptt theory} ML type, 46
5.1337 - \item {\ptt theory_of_thm}, \bold{37}
5.1338 - \item {\ptt thin_tac}, \bold{20}
5.1339 - \item {\ptt THM} exception, 34, 35, 39, 43
5.1340 - \item {\ptt thm} ML type, 34
5.1341 - \item {\ptt thms_containing}, \bold{9}
5.1342 - \item {\ptt thms_of}, \bold{52}
5.1343 - \item {\ptt tid} nonterminal, \bold{65}, 77, 84
5.1344 - \item {\ptt time_use}, \bold{2}
5.1345 - \item {\ptt time_use_thy}, \bold{49}
5.1346 + \subitem taking apart, 39
5.1347 + \item theories, 49--62
5.1348 + \subitem axioms of, 55
5.1349 + \subitem constructing, \bold{55}
5.1350 + \subitem inspecting, \bold{56}
5.1351 + \subitem loading, 52
5.1352 + \subitem parent, \bold{49}
5.1353 + \subitem pseudo, \bold{54}
5.1354 + \subitem reloading, \bold{53}
5.1355 + \subitem removing, \bold{54}
5.1356 + \subitem theorems of, 55
5.1357 + \item {\tt THEORY} exception, 49, 55
5.1358 + \item {\tt theory} ML type, 49
5.1359 + \item {\tt theory_of_thm}, \bold{39}
5.1360 + \item {\tt thin_tac}, \bold{22}
5.1361 + \item {\tt THM} exception, 36, 37, 41, 46
5.1362 + \item {\tt thm} ML type, 36
5.1363 + \item {\tt thms_containing}, \bold{9}
5.1364 + \item {\tt thms_of}, \bold{56}
5.1365 + \item {\tt tid} nonterminal, \bold{66}, 80, 87
5.1366 + \item {\tt time_use}, \bold{3}
5.1367 + \item {\tt time_use_thy}, \bold{53}
5.1368 \item timing statistics, 10
5.1369 - \item {\ptt topthm}, \bold{14}
5.1370 - \item {\ptt tpairs_of}, \bold{37}
5.1371 - \item {\ptt trace_BEST_FIRST}, \bold{29}
5.1372 - \item {\ptt trace_DEPTH_FIRST}, \bold{29}
5.1373 - \item {\ptt trace_goalno_tac}, \bold{32}
5.1374 - \item {\ptt trace_REPEAT}, \bold{27}
5.1375 - \item {\ptt trace_simp}, 95, 102--103
5.1376 + \item {\tt toggle}, 3
5.1377 + \item token class, 93
5.1378 + \item token translations, 93--94
5.1379 + \item token_translation, 94
5.1380 + \item {\tt token_translation}, 94
5.1381 + \item {\tt topthm}, \bold{15}
5.1382 + \item {\tt tpairs_of}, \bold{39}
5.1383 + \item {\tt trace_BEST_FIRST}, \bold{31}
5.1384 + \item {\tt trace_DEPTH_FIRST}, \bold{31}
5.1385 + \item {\tt trace_goalno_tac}, \bold{34}
5.1386 + \item {\tt trace_REPEAT}, \bold{29}
5.1387 + \item {\tt trace_simp}, 100, 108
5.1388 \item tracing
5.1389 - \subitem of classical prover, 119
5.1390 - \subitem of macros, 84
5.1391 - \subitem of searching tacticals, 28, 29
5.1392 - \subitem of simplification, 95, 102--103
5.1393 - \subitem of tactics, 24
5.1394 - \subitem of unification, 38
5.1395 - \item {\ptt transitive}, \bold{41}
5.1396 - \item translations, 86--89
5.1397 - \subitem parse, 72, 79
5.1398 - \subitem parse AST, \bold{77}, 78
5.1399 - \subitem print, 72
5.1400 - \subitem print AST, \bold{80}
5.1401 - \item {\ptt translations} section, 82
5.1402 - \item {\ptt trivial}, \bold{44}
5.1403 - \item {\ptt Trueprop} constant, 73
5.1404 - \item {\ptt TRY}, \bold{27, 28}
5.1405 - \item {\ptt TRYALL}, \bold{32}
5.1406 - \item {\ptt TVar}, \bold{59}
5.1407 - \item {\ptt tvar} nonterminal, \bold{65, 66}, 77, 84
5.1408 - \item {\ptt typ} ML type, 58
5.1409 - \item {\ptt Type}, \bold{59}
5.1410 - \item {\ptt type} nonterminal, \bold{65}
5.1411 - \item {\ptt type} type, 69
5.1412 - \item type constraints, 65, 72, 80
5.1413 - \item type constructors, \bold{59}
5.1414 - \item type identifiers, 65
5.1415 - \item type synonyms, \bold{47}
5.1416 - \item type unknowns, \bold{59}, 65
5.1417 - \subitem freezing/thawing of, 42
5.1418 - \item type variables, \bold{59}
5.1419 - \item types, \bold{58}
5.1420 - \subitem certified, \bold{59}
5.1421 - \subitem printing of, 3, 14, 59
5.1422 + \subitem of classical prover, 125
5.1423 + \subitem of macros, 88
5.1424 + \subitem of searching tacticals, 31
5.1425 + \subitem of simplification, 100, 108--109
5.1426 + \subitem of tactics, 25
5.1427 + \subitem of unification, 40
5.1428 + \item {\tt transitive}, \bold{43}
5.1429 + \item translations, 90--93
5.1430 + \subitem parse, 74, 82
5.1431 + \subitem parse AST, \bold{80}, 81
5.1432 + \subitem print, 74
5.1433 + \subitem print AST, \bold{83}
5.1434 + \item {\tt translations} section, 85
5.1435 + \item {\tt trivial}, \bold{46}
5.1436 + \item {\tt Trueprop} constant, 76
5.1437 + \item {\tt TRY}, \bold{29, 30}
5.1438 + \item {\tt TRYALL}, \bold{34}
5.1439 + \item {\tt TVar}, \bold{60}
5.1440 + \item {\tt tvar} nonterminal, \bold{66, 67}, 80, 87
5.1441 + \item {\tt typ} ML type, 60
5.1442 + \item {\tt Type}, \bold{60}
5.1443 + \item {\tt type} nonterminal, \bold{66}
5.1444 + \item {\tt type} type, 71
5.1445 + \item type constraints, 66, 74, 83
5.1446 + \item type constructors, \bold{60}
5.1447 + \item type identifiers, 66
5.1448 + \item type synonyms, \bold{50}
5.1449 + \item type unknowns, \bold{60}, 66
5.1450 + \subitem freezing/thawing of, 45
5.1451 + \item type variables, \bold{60}
5.1452 + \item types, \bold{60}
5.1453 + \subitem certified, \bold{60}
5.1454 + \subitem printing of, 4, 14, 60
5.1455
5.1456 \indexspace
5.1457
5.1458 - \item {\ptt undo}, 6, \bold{9}, 13
5.1459 - \item unknowns, \bold{56}, 65
5.1460 - \item {\ptt unlink_thy}, \bold{50}
5.1461 - \item {\ptt update}, \bold{50}
5.1462 - \item {\ptt uresult}, \bold{8}, 14, 52
5.1463 - \item {\ptt use}, \bold{2}
5.1464 - \item use_dir, 54, 55
5.1465 - \item {\ptt use_thy}, \bold{49}, 50
5.1466 + \item {\tt undo}, 6, \bold{9}, 13
5.1467 + \item unknowns, \bold{57}, 66
5.1468 + \item {\tt unlink_thy}, \bold{54}
5.1469 + \item {\tt update}, \bold{54}
5.1470 + \item {\tt uresult}, \bold{8}, 15, 55
5.1471 + \item {\tt use}, \bold{3}
5.1472 + \item {\tt use_thy}, \bold{52}, 53
5.1473
5.1474 \indexspace
5.1475
5.1476 - \item {\ptt Var}, \bold{56}, 79
5.1477 - \item {\ptt var} nonterminal, \bold{65, 66}, 77, 84
5.1478 - \item {\ptt Variable}, 76
5.1479 + \item {\tt Var}, \bold{57}, 82
5.1480 + \item {\tt var} nonterminal, \bold{66, 67}, 80, 87
5.1481 + \item {\tt Variable}, 79
5.1482 \item variables
5.1483 - \subitem bound, \bold{56}
5.1484 - \subitem free, \bold{56}
5.1485 - \item {\ptt variant_abs}, \bold{57}, 89
5.1486 - \item {\ptt varifyT}, \bold{42}
5.1487 + \subitem bound, \bold{57}
5.1488 + \subitem free, \bold{57}
5.1489 + \item {\tt variant_abs}, \bold{58}
5.1490 + \item {\tt varifyT}, \bold{45}
5.1491
5.1492 \indexspace
5.1493
5.1494 - \item {\ptt xlisten} shell script, 5
5.1495 - \item {\ptt xnum} nonterminal, \bold{65}, 77, 84
5.1496 - \item {\ptt xstr} nonterminal, \bold{65}, 77, 84
5.1497 + \item {\tt xnum} nonterminal, \bold{66}, 80, 87
5.1498 + \item {\tt xstr} nonterminal, \bold{66}, 80, 87
5.1499
5.1500 \indexspace
5.1501
5.1502 - \item {\ptt zero_var_indexes}, \bold{36}
5.1503 + \item {\tt zero_var_indexes}, \bold{39}
5.1504
5.1505 \end{theindex}
6.1 --- a/doc-src/Ref/ref.rao Mon May 05 21:18:01 1997 +0200
6.2 +++ b/doc-src/Ref/ref.rao Tue May 06 12:50:16 1997 +0200
6.3 @@ -1,7 +1,7 @@
6.4 -% This file was generated by '/usr/stud/berghofe/latex/rail/rail' from 'ref.rai'
6.5 +% This file was generated by 'rail' from 'ref.rai'
6.6 \rail@t {lbrace}
6.7 \rail@t {rbrace}
6.8 -\rail@i {1}{ \par theoryDef : id '=' (name + '+') ('+' extension | ()); \par name: id | string; \par extension : (section +) 'end' ( () | ml ); \par section : classes | default | types | arities | consts | constdefs | trans | defs | rules | oracle ; \par classes : 'classes' ( ( id ( () | '<' (id + ',') ) ) + ) ; \par default : 'default' sort ; \par sort : id | lbrace (id * ',') rbrace ; \par types : 'types' ( ( typeDecl ( () | '(' infix ')' ) ) + ) ; \par infix : ( 'infixr' | 'infixl' ) nat; \par typeDecl : typevarlist name ( () | '=' ( string | type ) ); \par typevarlist : () | tid | '(' ( tid + ',' ) ')'; \par type : simpleType | '(' type ')' | type '=>' type | '[' ( type + "," ) ']' '=>' type; \par simpleType: id | ( tid ( () | '::' id ) ) | '(' ( type + "," ) ')' id | simpleType id; \par \par arities : 'arities' ((( name + ',' ) '::' arity ) + ) ; \par arity : ( () | '(' (sort + ',') ')' ) id ; \par \par consts : 'consts' ( ( constDecl ( () | ( '(' mixfix ')' ) ) ) + ) ; \par constDecl : ( name + ',') '::' (string | type); \par mixfix : string ( () | ( () | ('[' (nat + ',') ']')) nat ) | infix | 'binder' string nat ; \par constdefs : 'constdefs' (id '::' (string | type) string +) ; \par trans : 'translations' ( pat ( '==' | '=>' | '<=' ) pat + ) ; \par pat : ( () | ( '(' id ')' ) ) string; \par rules : 'rules' (( id string ) + ) ; \par defs : 'defs' (( id string ) + ) ; \par oracle : 'oracle' name ; \par ml : 'ML' text ; \par }
6.9 +\rail@i {1}{ \par theoryDef : id '=' (name + '+') ('+' extension | ()) ; \par name: id | string ; \par extension : (section +) 'end' ( () | ml ) ; \par section : classes | default | types | arities | consts | syntax | trans | defs | constdefs | rules | axclass | instance | oracle ; \par classes : 'classes' ( classDecl + ) ; \par classDecl : (id (() | '<' (id + ','))) ; \par default : 'default' sort ; \par sort : id | lbrace (id * ',') rbrace ; \par types : 'types' ( ( typeDecl ( () | '(' infix ')' ) ) + ) ; \par infix : ( 'infixr' | 'infixl' ) nat ; \par typeDecl : typevarlist name ( () | '=' ( string | type ) ); \par typevarlist : () | tid | '(' ( tid + ',' ) ')'; \par type : simpleType | '(' type ')' | type '=>' type | '[' ( type + "," ) ']' '=>' type; \par simpleType: id | ( tid ( () | '::' id ) ) | '(' ( type + "," ) ')' id | simpleType id ; \par arities : 'arities' ((name + ',') '::' arity +) ; \par arity : ( () | '(' (sort + ',') ')' ) sort ; \par consts : 'consts' ( mixfixConstDecl + ) ; \par syntax : 'syntax' (() | mode) ( mixfixConstDecl + ); \par mode : '(' name (() | 'output') ')' ; \par mixfixConstDecl : constDecl (() | ( '(' mixfix ')' )) ; \par constDecl : ( name + ',') '::' (string | type); \par mixfix : string ( () | ( () | ('[' (nat + ',') ']')) nat ) | ( 'infixr' | 'infixl' ) (() | string) nat | 'binder' string nat ; \par trans : 'translations' ( pat ( '==' | '=>' | '<=' ) pat + ) ; \par pat : ( () | ( '(' id ')' ) ) string; \par rules : 'rules' (( id string ) + ) ; \par defs : 'defs' (( id string ) + ) ; \par constdefs : 'constdefs' (id '::' (string | type) string +) ; \par axclass : 'axclass' classDecl (() | ( id string ) +) ; \par instance : 'instance' ( name '<' name | name '::' arity) witness ; \par witness : (() | ((string | longident) + ',')) (() | verbatim) ; \par oracle : 'oracle' name ; \par ml : 'ML' text ; \par }
6.10 \rail@o {1}{
6.11 \rail@begin{2}{theoryDef}
6.12 \rail@nont{id}[]
6.13 @@ -35,7 +35,7 @@
6.14 \rail@nont{ml}[]
6.15 \rail@endbar
6.16 \rail@end
6.17 -\rail@begin{10}{section}
6.18 +\rail@begin{13}{section}
6.19 \rail@bar
6.20 \rail@nont{classes}[]
6.21 \rail@nextbar{1}
6.22 @@ -47,20 +47,31 @@
6.23 \rail@nextbar{4}
6.24 \rail@nont{consts}[]
6.25 \rail@nextbar{5}
6.26 -\rail@nont{constdefs}[]
6.27 +\rail@nont{syntax}[]
6.28 \rail@nextbar{6}
6.29 \rail@nont{trans}[]
6.30 \rail@nextbar{7}
6.31 \rail@nont{defs}[]
6.32 \rail@nextbar{8}
6.33 +\rail@nont{constdefs}[]
6.34 +\rail@nextbar{9}
6.35 \rail@nont{rules}[]
6.36 -\rail@nextbar{9}
6.37 +\rail@nextbar{10}
6.38 +\rail@nont{axclass}[]
6.39 +\rail@nextbar{11}
6.40 +\rail@nont{instance}[]
6.41 +\rail@nextbar{12}
6.42 \rail@nont{oracle}[]
6.43 \rail@endbar
6.44 \rail@end
6.45 -\rail@begin{4}{classes}
6.46 +\rail@begin{2}{classes}
6.47 \rail@term{classes}[]
6.48 \rail@plus
6.49 +\rail@nont{classDecl}[]
6.50 +\rail@nextplus{1}
6.51 +\rail@endplus
6.52 +\rail@end
6.53 +\rail@begin{3}{classDecl}
6.54 \rail@nont{id}[]
6.55 \rail@bar
6.56 \rail@nextbar{1}
6.57 @@ -71,8 +82,6 @@
6.58 \rail@cterm{,}[]
6.59 \rail@endplus
6.60 \rail@endbar
6.61 -\rail@nextplus{3}
6.62 -\rail@endplus
6.63 \rail@end
6.64 \rail@begin{1}{default}
6.65 \rail@term{default}[]
6.66 @@ -213,11 +222,36 @@
6.67 \rail@endplus
6.68 \rail@term{)}[]
6.69 \rail@endbar
6.70 -\rail@nont{id}[]
6.71 +\rail@nont{sort}[]
6.72 \rail@end
6.73 -\rail@begin{3}{consts}
6.74 +\rail@begin{2}{consts}
6.75 \rail@term{consts}[]
6.76 \rail@plus
6.77 +\rail@nont{mixfixConstDecl}[]
6.78 +\rail@nextplus{1}
6.79 +\rail@endplus
6.80 +\rail@end
6.81 +\rail@begin{2}{syntax}
6.82 +\rail@term{syntax}[]
6.83 +\rail@bar
6.84 +\rail@nextbar{1}
6.85 +\rail@nont{mode}[]
6.86 +\rail@endbar
6.87 +\rail@plus
6.88 +\rail@nont{mixfixConstDecl}[]
6.89 +\rail@nextplus{1}
6.90 +\rail@endplus
6.91 +\rail@end
6.92 +\rail@begin{2}{mode}
6.93 +\rail@term{(}[]
6.94 +\rail@nont{name}[]
6.95 +\rail@bar
6.96 +\rail@nextbar{1}
6.97 +\rail@term{output}[]
6.98 +\rail@endbar
6.99 +\rail@term{)}[]
6.100 +\rail@end
6.101 +\rail@begin{2}{mixfixConstDecl}
6.102 \rail@nont{constDecl}[]
6.103 \rail@bar
6.104 \rail@nextbar{1}
6.105 @@ -225,8 +259,6 @@
6.106 \rail@nont{mixfix}[]
6.107 \rail@term{)}[]
6.108 \rail@endbar
6.109 -\rail@nextplus{2}
6.110 -\rail@endplus
6.111 \rail@end
6.112 \rail@begin{2}{constDecl}
6.113 \rail@plus
6.114 @@ -241,7 +273,7 @@
6.115 \rail@nont{type}[]
6.116 \rail@endbar
6.117 \rail@end
6.118 -\rail@begin{6}{mixfix}
6.119 +\rail@begin{7}{mixfix}
6.120 \rail@bar
6.121 \rail@nont{string}[]
6.122 \rail@bar
6.123 @@ -259,27 +291,22 @@
6.124 \rail@nont{nat}[]
6.125 \rail@endbar
6.126 \rail@nextbar{4}
6.127 -\rail@nont{infix}[]
6.128 +\rail@bar
6.129 +\rail@term{infixr}[]
6.130 \rail@nextbar{5}
6.131 +\rail@term{infixl}[]
6.132 +\rail@endbar
6.133 +\rail@bar
6.134 +\rail@nextbar{5}
6.135 +\rail@nont{string}[]
6.136 +\rail@endbar
6.137 +\rail@nont{nat}[]
6.138 +\rail@nextbar{6}
6.139 \rail@term{binder}[]
6.140 \rail@nont{string}[]
6.141 \rail@nont{nat}[]
6.142 \rail@endbar
6.143 \rail@end
6.144 -\rail@begin{3}{constdefs}
6.145 -\rail@term{constdefs}[]
6.146 -\rail@plus
6.147 -\rail@nont{id}[]
6.148 -\rail@term{::}[]
6.149 -\rail@bar
6.150 -\rail@nont{string}[]
6.151 -\rail@nextbar{1}
6.152 -\rail@nont{type}[]
6.153 -\rail@endbar
6.154 -\rail@nont{string}[]
6.155 -\rail@nextplus{2}
6.156 -\rail@endplus
6.157 -\rail@end
6.158 \rail@begin{4}{trans}
6.159 \rail@term{translations}[]
6.160 \rail@plus
6.161 @@ -320,6 +347,63 @@
6.162 \rail@nextplus{1}
6.163 \rail@endplus
6.164 \rail@end
6.165 +\rail@begin{3}{constdefs}
6.166 +\rail@term{constdefs}[]
6.167 +\rail@plus
6.168 +\rail@nont{id}[]
6.169 +\rail@term{::}[]
6.170 +\rail@bar
6.171 +\rail@nont{string}[]
6.172 +\rail@nextbar{1}
6.173 +\rail@nont{type}[]
6.174 +\rail@endbar
6.175 +\rail@nont{string}[]
6.176 +\rail@nextplus{2}
6.177 +\rail@endplus
6.178 +\rail@end
6.179 +\rail@begin{3}{axclass}
6.180 +\rail@term{axclass}[]
6.181 +\rail@nont{classDecl}[]
6.182 +\rail@bar
6.183 +\rail@nextbar{1}
6.184 +\rail@plus
6.185 +\rail@nont{id}[]
6.186 +\rail@nont{string}[]
6.187 +\rail@nextplus{2}
6.188 +\rail@endplus
6.189 +\rail@endbar
6.190 +\rail@end
6.191 +\rail@begin{2}{instance}
6.192 +\rail@term{instance}[]
6.193 +\rail@bar
6.194 +\rail@nont{name}[]
6.195 +\rail@term{<}[]
6.196 +\rail@nont{name}[]
6.197 +\rail@nextbar{1}
6.198 +\rail@nont{name}[]
6.199 +\rail@term{::}[]
6.200 +\rail@nont{arity}[]
6.201 +\rail@endbar
6.202 +\rail@nont{witness}[]
6.203 +\rail@end
6.204 +\rail@begin{4}{witness}
6.205 +\rail@bar
6.206 +\rail@nextbar{1}
6.207 +\rail@plus
6.208 +\rail@bar
6.209 +\rail@nont{string}[]
6.210 +\rail@nextbar{2}
6.211 +\rail@nont{longident}[]
6.212 +\rail@endbar
6.213 +\rail@nextplus{3}
6.214 +\rail@cterm{,}[]
6.215 +\rail@endplus
6.216 +\rail@endbar
6.217 +\rail@bar
6.218 +\rail@nextbar{1}
6.219 +\rail@nont{verbatim}[]
6.220 +\rail@endbar
6.221 +\rail@end
6.222 \rail@begin{1}{oracle}
6.223 \rail@term{oracle}[]
6.224 \rail@nont{name}[]
7.1 --- a/doc-src/Ref/ref.tex Mon May 05 21:18:01 1997 +0200
7.2 +++ b/doc-src/Ref/ref.tex Tue May 06 12:50:16 1997 +0200
7.3 @@ -32,19 +32,19 @@
7.4
7.5 \makeindex
7.6
7.7 -\underscoreoff
7.8 -
7.9 \setcounter{secnumdepth}{1} \setcounter{tocdepth}{2}
7.10
7.11 \pagestyle{headings}
7.12 \sloppy
7.13 \binperiod %%%treat . like a binary operator
7.14
7.15 -\railalias{lbrace}{\{}
7.16 -\railalias{rbrace}{\}}
7.17 +\railalias{lbrace}{\ttlbrace}
7.18 +\railalias{rbrace}{\ttrbrace}
7.19 \railterm{lbrace,rbrace}
7.20
7.21 \begin{document}
7.22 +\underscoreoff
7.23 +
7.24 \index{definitions|see{rewriting, meta-level}}
7.25 \index{rewriting!object-level|see{simplification}}
7.26 \index{meta-rules|see{meta-rules}}
8.1 --- a/doc-src/Ref/simplifier.tex Mon May 05 21:18:01 1997 +0200
8.2 +++ b/doc-src/Ref/simplifier.tex Tue May 06 12:50:16 1997 +0200
8.3 @@ -83,9 +83,9 @@
8.4 \S\ref{sec:reordering-asms} for ways around this problem.
8.5 \end{warn}
8.6
8.7 -Using the simplifier effectively may take a bit of experimentation.
8.8 -\index{tracing!of simplification|)}\ttindex{trace_simp}
8.9 -The tactics can be traced with the ML command \verb$trace_simp := true$.
8.10 +Using the simplifier effectively may take a bit of experimentation.
8.11 +\index{tracing!of simplification}\index{*trace_simp} The tactics can
8.12 +be traced by setting \verb$trace_simp := true$.
8.13
8.14 There is not just one global current simpset, but one associated with each
8.15 theory as well. How are these simpset built up?
8.16 @@ -145,10 +145,9 @@
8.17 defaults so that most simplifier calls specify only rewrite rules.
8.18 Experienced users can exploit the other components to streamline proofs.
8.19
8.20 -Logics like \HOL, which support a current simpset\index{simpset!current},
8.21 -store its value in an ML reference variable usually called {\tt
8.22 - simpset}\index{simpset@{\tt simpset} ML value}. It can be accessed via
8.23 -{\tt!simpset} and updated via {\tt simpset := \dots}.
8.24 +Logics like \HOL, which support a current
8.25 +simpset\index{simpset!current}, store its value in an ML reference
8.26 +variable called {\tt simpset}\index{simpset@{\tt simpset} ML value}.
8.27
8.28 \subsection{Rewrite rules}
8.29 \index{rewrite rules|(}
8.30 @@ -159,7 +158,7 @@
8.31 \Var{A} \un \Var{B} &\equiv& \{x.x\in \Var{A} \disj x\in \Var{B}\}
8.32 \end{eqnarray*}
8.33 Conditional rewrites such as $\Var{m}<\Var{n} \Imp \Var{m}/\Var{n} =
8.34 -0$ are permitted; the conditions can be arbitrary terms.
8.35 +0$ are permitted; the conditions can be arbitrary formulas.
8.36
8.37 Internally, all rewrite rules are translated into meta-equalities, theorems
8.38 with conclusion $lhs \equiv rhs$. Each simpset contains a function for
8.39 @@ -200,7 +199,7 @@
8.40
8.41 \subsection{*Congruence rules}\index{congruence rules}
8.42 Congruence rules are meta-equalities of the form
8.43 -\[ \List{\dots} \Imp
8.44 +\[ \dots \Imp
8.45 f(\Var{x@1},\ldots,\Var{x@n}) \equiv f(\Var{y@1},\ldots,\Var{y@n}).
8.46 \]
8.47 This governs the simplification of the arguments of~$f$. For
8.48 @@ -272,26 +271,27 @@
8.49 True} and $t=t$. It could use sophisticated means such as {\tt
8.50 fast_tac}, though that could make simplification expensive.
8.51
8.52 -Rewriting does not instantiate unknowns. For example, rewriting cannot
8.53 -prove $a\in \Var{A}$ since this requires instantiating~$\Var{A}$. The
8.54 -solver, however, is an arbitrary tactic and may instantiate unknowns as it
8.55 -pleases. This is the only way the simplifier can handle a conditional
8.56 -rewrite rule whose condition contains extra variables. When a simplification
8.57 -tactic is to be combined with other provers, especially with the classical
8.58 -reasoner, it is important whether it can be considered safe or not. Therefore,
8.59 -the solver is split into a safe and anunsafe part. Both parts can be set
8.60 -independently of each other using
8.61 -\ttindex{setSSolver} (with a safe tactic as argument) and \ttindex{setSolver}
8.62 -(with an unsafe tactic) . Additional solvers, which are tried after the already
8.63 -set solvers, may be added using \ttindex{addSSolver} and \ttindex{addSolver}.
8.64 +Rewriting does not instantiate unknowns. For example, rewriting
8.65 +cannot prove $a\in \Var{A}$ since this requires
8.66 +instantiating~$\Var{A}$. The solver, however, is an arbitrary tactic
8.67 +and may instantiate unknowns as it pleases. This is the only way the
8.68 +simplifier can handle a conditional rewrite rule whose condition
8.69 +contains extra variables. When a simplification tactic is to be
8.70 +combined with other provers, especially with the classical reasoner,
8.71 +it is important whether it can be considered safe or not. Therefore,
8.72 +the solver is split into a safe and an unsafe part. Both parts can be
8.73 +set independently, using either \ttindex{setSSolver} with a safe
8.74 +tactic as argument, or \ttindex{setSolver} with an unsafe tactic.
8.75 +Additional solvers, which are tried after the already set solvers, may
8.76 +be added using \ttindex{addSSolver} and \ttindex{addSolver}.
8.77
8.78 -The standard simplification procedures uses solely the unsafe solver, which is
8.79 -appropriate in most cases. But for special applications, where the simplification
8.80 -process is not allowed to instantiate unknowns within the goal, the tactic
8.81 -\ttindexbold{safe_asm_full_simp_tac} is provided. Like {\tt asm_full_simp_tac},
8.82 -it uses the unsafe solver for any embedded simplification steps
8.83 -(i.e. for solving subgoals created by the subgoaler),
8.84 -but for the current subgoal, it applies the safe solver.
8.85 +The standard simplification strategy solely uses the unsafe solver,
8.86 +which is appropriate in most cases. But for special applications where
8.87 +the simplification process is not allowed to instantiate unknowns
8.88 +within the goal, the tactic \ttindexbold{safe_asm_full_simp_tac} is
8.89 +provided. It uses the \emph{safe} solver for the current subgoal, but
8.90 +applies ordinary unsafe {\tt asm_full_simp_tac} for recursive internal
8.91 +simplifications (for conditional rules or congruences).
8.92
8.93 \index{assumptions!in simplification}
8.94 The tactic is presented with the full goal, including the asssumptions.
8.95 @@ -308,16 +308,17 @@
8.96 \Var{x}$, usually by reflexivity. In particular, reflexivity should be
8.97 tried before any of the fancy tactics like {\tt fast_tac}.
8.98
8.99 -It may even happen that, due to simplification, the subgoal is no longer an
8.100 -equality. For example $False \bimp \Var{Q}$ could be rewritten to
8.101 -$\neg\Var{Q}$. To cover this case, the solver could try resolving with the
8.102 -theorem $\neg False$.
8.103 +It may even happen that due to simplification the subgoal is no longer
8.104 +an equality. For example $False \bimp \Var{Q}$ could be rewritten to
8.105 +$\neg\Var{Q}$. To cover this case, the solver could try resolving
8.106 +with the theorem $\neg False$.
8.107
8.108 \begin{warn}
8.109 - If the simplifier aborts with the message {\tt Failed congruence proof!},
8.110 - then the subgoaler or solver has failed to prove a premise of a
8.111 - congruence rule. This should never occur; it indicates that some
8.112 - congruence rule, or possibly the subgoaler or solver, is faulty.
8.113 + If the simplifier aborts with the message {\tt Failed congruence
8.114 + proof!}, then the subgoaler or solver has failed to prove a
8.115 + premise of a congruence rule. This should never occur under normal
8.116 + circumstances; it indicates that some congruence rule, or possibly
8.117 + the subgoaler or solver, is faulty.
8.118 \end{warn}
8.119
8.120
8.121 @@ -430,9 +431,9 @@
8.122 in conditional rewrite rules are solved recursively before the rewrite rule
8.123 is applied.
8.124
8.125 -The infix operations \ttindex{addsimps}/\ttindex{delsimps} add/delete rewrite
8.126 -rules to/from a simpset. They are used to implement \ttindex{Addsimps} and
8.127 -\ttindex{Delsimps}, e.g.
8.128 +The infix operation \ttindex{addsimps} adds rewrite rules to a
8.129 +simpset, while \ttindex{delsimps} deletes them. They are used to
8.130 +implement \ttindex{Addsimps} and \ttindex{Delsimps}, e.g.
8.131 \begin{ttbox}
8.132 fun Addsimps thms = (simpset := (!simpset addsimps thms));
8.133 \end{ttbox}
8.134 @@ -515,7 +516,7 @@
8.135 \end{ttbox}
8.136
8.137 \subsection{An example of tracing}
8.138 -\index{tracing!of simplification|(}\ttindex{trace_simp|(}
8.139 +\index{tracing!of simplification|(}\index{*trace_simp}
8.140 Let us prove a similar result involving more complex terms. The two
8.141 equations together can be used to prove that addition is commutative.
8.142 \begin{ttbox}
8.143 @@ -572,7 +573,7 @@
8.144 {\out m + Suc(n) = Suc(m + n)}
8.145 {\out No subgoals!}
8.146 \end{ttbox}
8.147 -\index{tracing!of simplification|)}\ttindex{trace_simp|)}
8.148 +\index{tracing!of simplification|)}
8.149
8.150 \subsection{Free variables and simplification}
8.151 Here is a conjecture to be proved for an arbitrary function~$f$ satisfying
8.152 @@ -663,7 +664,7 @@
8.153
8.154 Because ordinary rewriting loops given such rules, the simplifier employs a
8.155 special strategy, called {\bf ordered rewriting}\index{rewriting!ordered}.
8.156 -There is a built-in lexicographic ordering on terms. A permutative rewrite
8.157 +There is a standard lexicographic ordering on terms. A permutative rewrite
8.158 rule is applied only if it decreases the given term with respect to this
8.159 ordering. For example, commutativity rewrites~$b+a$ to $a+b$, but then
8.160 stops because $a+b$ is strictly less than $b+a$. The Boyer-Moore theorem
8.161 @@ -692,74 +693,73 @@
8.162 examples; other algebraic structures are amenable to ordered rewriting,
8.163 such as boolean rings.
8.164
8.165 -\subsection{Example: sums of integers}
8.166 -This example is set in Isabelle's higher-order logic. Theory
8.167 -\thydx{Arith} contains the theory of arithmetic. The simpset {\tt
8.168 - arith_ss} contains many arithmetic laws including distributivity
8.169 -of~$\times$ over~$+$, while {\tt add_ac} is a list consisting of the A, C
8.170 -and LC laws for~$+$. Let us prove the theorem
8.171 +\subsection{Example: sums of natural numbers}
8.172 +This example is set in \HOL\ (see \texttt{HOL/ex/NatSum}). Theory
8.173 +\thydx{Arith} contains natural numbers arithmetic. Its associated
8.174 +simpset contains many arithmetic laws including distributivity
8.175 +of~$\times$ over~$+$, while {\tt add_ac} is a list consisting of the
8.176 +A, C and LC laws for~$+$ on type \texttt{nat}. Let us prove the
8.177 +theorem
8.178 \[ \sum@{i=1}^n i = n\times(n+1)/2. \]
8.179 %
8.180 A functional~{\tt sum} represents the summation operator under the
8.181 -interpretation ${\tt sum}(f,n+1) = \sum@{i=0}^n f(i)$. We extend {\tt
8.182 - Arith} using a theory file:
8.183 +interpretation ${\tt sum} \, f \, (n + 1) = \sum@{i=0}^n f\,i$. We
8.184 +extend {\tt Arith} using a theory file:
8.185 \begin{ttbox}
8.186 NatSum = Arith +
8.187 consts sum :: [nat=>nat, nat] => nat
8.188 -rules sum_0 "sum(f,0) = 0"
8.189 - sum_Suc "sum(f,Suc(n)) = f(n) + sum(f,n)"
8.190 +rules sum_0 "sum f 0 = 0"
8.191 + sum_Suc "sum f (Suc n) = f n + sum f n"
8.192 end
8.193 \end{ttbox}
8.194 -After declaring {\tt open NatSum}, we make the required simpset by adding
8.195 -the AC-rules for~$+$ and the axioms for~{\tt sum}:
8.196 +We make the required simpset by adding the AC-rules for~$+$ and the
8.197 +axioms for~{\tt sum}:
8.198 \begin{ttbox}
8.199 -val natsum_ss = arith_ss addsimps ([sum_0,sum_Suc] \at add_ac);
8.200 -{\out val natsum_ss = SS \{\ldots\} : simpset}
8.201 +val natsum_ss = simpset_of "Arith" addsimps ([sum_0,sum_Suc] \at add_ac);
8.202 +{\out val natsum_ss = \ldots : simpset}
8.203 \end{ttbox}
8.204 -Our desired theorem now reads ${\tt sum}(\lambda i.i,n+1) =
8.205 +Our desired theorem now reads ${\tt sum} \, (\lambda i.i) \, (n+1) =
8.206 n\times(n+1)/2$. The Isabelle goal has both sides multiplied by~$2$:
8.207 \begin{ttbox}
8.208 -goal NatSum.thy "Suc(Suc(0))*sum(\%i.i,Suc(n)) = n*Suc(n)";
8.209 +goal NatSum.thy "2 * sum (\%i.i) (Suc n) = n * Suc n";
8.210 {\out Level 0}
8.211 -{\out Suc(Suc(0)) * sum(\%i. i, Suc(n)) = n * Suc(n)}
8.212 -{\out 1. Suc(Suc(0)) * sum(\%i. i, Suc(n)) = n * Suc(n)}
8.213 +{\out 2 * sum (\%i. i) (Suc n) = n * Suc n}
8.214 +{\out 1. 2 * sum (\%i. i) (Suc n) = n * Suc n}
8.215 \end{ttbox}
8.216 -Induction should not be applied until the goal is in the simplest form:
8.217 +Induction should not be applied until the goal is in the simplest
8.218 +form:
8.219 \begin{ttbox}
8.220 by (simp_tac natsum_ss 1);
8.221 {\out Level 1}
8.222 -{\out Suc(Suc(0)) * sum(\%i. i, Suc(n)) = n * Suc(n)}
8.223 -{\out 1. n + (n + (sum(\%i. i, n) + sum(\%i. i, n))) = n + n * n}
8.224 +{\out 2 * sum (\%i. i) (Suc n) = n * Suc n}
8.225 +{\out 1. n + (sum (\%i. i) n + sum (\%i. i) n) = n * n}
8.226 \end{ttbox}
8.227 -Ordered rewriting has sorted the terms in the left-hand side.
8.228 -The subgoal is now ready for induction:
8.229 +Ordered rewriting has sorted the terms in the left-hand side. The
8.230 +subgoal is now ready for induction:
8.231 \begin{ttbox}
8.232 by (nat_ind_tac "n" 1);
8.233 {\out Level 2}
8.234 -{\out Suc(Suc(0)) * sum(\%i. i, Suc(n)) = n * Suc(n)}
8.235 -{\out 1. 0 + (0 + (sum(\%i. i, 0) + sum(\%i. i, 0))) = 0 + 0 * 0}
8.236 +{\out 2 * sum (\%i. i) (Suc n) = n * Suc n}
8.237 +{\out 1. 0 + (sum (\%i. i) 0 + sum (\%i. i) 0) = 0 * 0}
8.238 \ttbreak
8.239 -{\out 2. !!n1. n1 + (n1 + (sum(\%i. i, n1) + sum(\%i. i, n1))) =}
8.240 -{\out n1 + n1 * n1 ==>}
8.241 -{\out Suc(n1) +}
8.242 -{\out (Suc(n1) + (sum(\%i. i, Suc(n1)) + sum(\%i. i, Suc(n1)))) =}
8.243 -{\out Suc(n1) + Suc(n1) * Suc(n1)}
8.244 +{\out 2. !!n1. n1 + (sum (\%i. i) n1 + sum (\%i. i) n1) = n1 * n1}
8.245 +{\out ==> Suc n1 + (sum (\%i. i) (Suc n1) + sum (\%i. i) (Suc n1)) =}
8.246 +{\out Suc n1 * Suc n1}
8.247 \end{ttbox}
8.248 Simplification proves both subgoals immediately:\index{*ALLGOALS}
8.249 \begin{ttbox}
8.250 by (ALLGOALS (asm_simp_tac natsum_ss));
8.251 {\out Level 3}
8.252 -{\out Suc(Suc(0)) * sum(\%i. i, Suc(n)) = n * Suc(n)}
8.253 +{\out 2 * sum (\%i. i) (Suc n) = n * Suc n}
8.254 {\out No subgoals!}
8.255 \end{ttbox}
8.256 If we had omitted {\tt add_ac} from the simpset, simplification would have
8.257 failed to prove the induction step:
8.258 \begin{ttbox}
8.259 -Suc(Suc(0)) * sum(\%i. i, Suc(n)) = n * Suc(n)
8.260 - 1. !!n1. n1 + (n1 + (sum(\%i. i, n1) + sum(\%i. i, n1))) =
8.261 - n1 + n1 * n1 ==>
8.262 - n1 + (n1 + (n1 + sum(\%i. i, n1) + (n1 + sum(\%i. i, n1)))) =
8.263 - n1 + (n1 + (n1 + n1 * n1))
8.264 +2 * sum (\%i. i) (Suc n) = n * Suc n
8.265 + 1. !!n1. n1 + sum (\%i. i) n1 + (n1 + sum (\%i. i) n1) = n1 + n1 * n1
8.266 + ==> n1 + (n1 + sum (\%i. i) n1) + (n1 + (n1 + sum (\%i. i) n1)) =
8.267 + n1 + (n1 + (n1 + n1 * n1))
8.268 \end{ttbox}
8.269 Ordered rewriting proves this by sorting the left-hand side. Proving
8.270 arithmetic theorems without ordered rewriting requires explicit use of
8.271 @@ -811,7 +811,7 @@
8.272 Simplification works by reducing various object-equalities to
8.273 meta-equality. It requires rules stating that equal terms and equivalent
8.274 formulae are also equal at the meta-level. The rule declaration part of
8.275 -the file {\tt FOL/ifol.thy} contains the two lines
8.276 +the file {\tt FOL/IFOL.thy} contains the two lines
8.277 \begin{ttbox}\index{*eq_reflection theorem}\index{*iff_reflection theorem}
8.278 eq_reflection "(x=y) ==> (x==y)"
8.279 iff_reflection "(P<->Q) ==> (P==Q)"
9.1 --- a/doc-src/Ref/substitution.tex Mon May 05 21:18:01 1997 +0200
9.2 +++ b/doc-src/Ref/substitution.tex Tue May 06 12:50:16 1997 +0200
9.3 @@ -21,8 +21,10 @@
9.4 \section{Substitution rules}
9.5 \index{substitution!rules}\index{*subst theorem}
9.6 Many logics include a substitution rule of the form
9.7 -$$ \List{\Var{a}=\Var{b}; \Var{P}(\Var{a})} \Imp
9.8 - \Var{P}(\Var{b}) \eqno(subst)$$
9.9 +$$
9.10 +\List{\Var{a}=\Var{b}; \Var{P}(\Var{a})} \Imp
9.11 +\Var{P}(\Var{b}) \eqno(subst)
9.12 +$$
9.13 In backward proof, this may seem difficult to use: the conclusion
9.14 $\Var{P}(\Var{b})$ admits far too many unifiers. But, if the theorem {\tt
9.15 eqth} asserts $t=u$, then \hbox{\tt eqth RS subst} is the derived rule
9.16 @@ -42,8 +44,10 @@
9.17 resolve_tac [eqth RS ssubst] \(i\){\it,}
9.18 \end{ttbox}
9.19 where \tdxbold{ssubst} is the `swapped' substitution rule
9.20 -$$ \List{\Var{a}=\Var{b}; \Var{P}(\Var{b})} \Imp
9.21 - \Var{P}(\Var{a}). \eqno(ssubst)$$
9.22 +$$
9.23 +\List{\Var{a}=\Var{b}; \Var{P}(\Var{b})} \Imp
9.24 +\Var{P}(\Var{a}). \eqno(ssubst)
9.25 +$$
9.26 If \tdx{sym} denotes the symmetry rule
9.27 \(\Var{a}=\Var{b}\Imp\Var{b}=\Var{a}\), then {\tt ssubst} is just
9.28 \hbox{\tt sym RS subst}. Many logics with equality include the rules {\tt
9.29 @@ -57,7 +61,7 @@
9.30 eresolve_tac [subst] \(i\) {\rm or} eresolve_tac [ssubst] \(i\){\it.}
9.31 \end{ttbox}
9.32
9.33 -Logics HOL, FOL and ZF define the tactic \ttindexbold{stac} by
9.34 +Logics \HOL, {\FOL} and {\ZF} define the tactic \ttindexbold{stac} by
9.35 \begin{ttbox}
9.36 fun stac eqth = CHANGED o rtac (eqth RS ssubst);
9.37 \end{ttbox}
10.1 --- a/doc-src/Ref/syntax.tex Mon May 05 21:18:01 1997 +0200
10.2 +++ b/doc-src/Ref/syntax.tex Tue May 06 12:50:16 1997 +0200
10.3 @@ -31,7 +31,7 @@
10.4 \begin{center}
10.5 \begin{tabular}{cl}
10.6 string & \\
10.7 -$\downarrow$ & parser \\
10.8 +$\downarrow$ & lexer, parser \\
10.9 parse tree & \\
10.10 $\downarrow$ & parse \AST{} translation \\
10.11 \AST{} & \\
10.12 @@ -43,7 +43,7 @@
10.13 \AST{} & \\
10.14 $\downarrow$ & \AST{} rewriting (macros) \\
10.15 \AST{} & \\
10.16 -$\downarrow$ & print \AST{} translation, printer \\
10.17 +$\downarrow$ & print \AST{} translation, token translation \\
10.18 string &
10.19 \end{tabular}
10.20
10.21 @@ -304,11 +304,13 @@
10.22 and their syntactic sugar (denoted by \dots{} above) are joined to make a
10.23 single string.
10.24
10.25 -If an application $(\mtt"c\mtt"~ x@1 \ldots x@m)$ has more arguments than the
10.26 -corresponding production, it is first split into $((\mtt"c\mtt"~ x@1 \ldots
10.27 -x@n) ~ x@{n+1} \ldots x@m)$. Applications with too few arguments or with
10.28 -non-constant head or without a corresponding production are printed as
10.29 -$f(x@1, \ldots, x@l)$ or $(\alpha@1, \ldots, \alpha@l) ty$. An occurrence of
10.30 +If an application $(\mtt"c\mtt"~ x@1 \ldots x@m)$ has more arguments
10.31 +than the corresponding production, it is first split into
10.32 +$((\mtt"c\mtt"~ x@1 \ldots x@n) ~ x@{n+1} \ldots x@m)$. Applications
10.33 +with too few arguments or with non-constant head or without a
10.34 +corresponding production are printed as $f(x@1, \ldots, x@l)$ or
10.35 +$(\alpha@1, \ldots, \alpha@l) ty$. Multiple productions associated
10.36 +with some name $c$ are tried in order of appearance. An occurrence of
10.37 $\Variable x$ is simply printed as~$x$.
10.38
10.39 Blanks are {\em not\/} inserted automatically. If blanks are required to
10.40 @@ -318,7 +320,7 @@
10.41
10.42
10.43
10.44 -\section{Macros: Syntactic rewriting} \label{sec:macros}
10.45 +\section{Macros: syntactic rewriting} \label{sec:macros}
10.46 \index{macros|(}\index{rewriting!syntactic|(}
10.47
10.48 Mixfix declarations alone can handle situations where there is a direct
10.49 @@ -338,19 +340,20 @@
10.50 on abstract syntax trees. They are usually easy to read and write, and can
10.51 express all but the most obscure translations.
10.52
10.53 -Figure~\ref{fig:set_trans} defines a fragment of first-order logic and set
10.54 -theory.\footnote{This and the following theories are complete working
10.55 - examples, though they specify only syntax, no axioms. The file {\tt
10.56 - ZF/ZF.thy} presents a full set theory definition, including many
10.57 - macro rules.} Theory {\tt SET} defines constants for set comprehension
10.58 -({\tt Collect}), replacement ({\tt Replace}) and bounded universal
10.59 -quantification ({\tt Ball}). Each of these binds some variables. Without
10.60 -additional syntax we should have to write $\forall x \in A. P$ as {\tt
10.61 - Ball(A,\%x.P)}, and similarly for the others.
10.62 +Figure~\ref{fig:set_trans} defines a fragment of first-order logic and
10.63 +set theory.\footnote{This and the following theories are complete
10.64 + working examples, though they specify only syntax, no axioms. The
10.65 + file {\tt ZF/ZF.thy} presents a full set theory definition,
10.66 + including many macro rules.} Theory {\tt SetSyntax} declares
10.67 +constants for set comprehension ({\tt Collect}), replacement ({\tt
10.68 + Replace}) and bounded universal quantification ({\tt Ball}). Each
10.69 +of these binds some variables. Without additional syntax we should
10.70 +have to write $\forall x \in A. P$ as {\tt Ball(A,\%x.P)}, and
10.71 +similarly for the others.
10.72
10.73 \begin{figure}
10.74 \begin{ttbox}
10.75 -SET = Pure +
10.76 +SetSyntax = Pure +
10.77 types
10.78 i o
10.79 arities
10.80 @@ -425,8 +428,8 @@
10.81 \item Every variable in~$r$ must also occur in~$l$.
10.82 \end{itemize}
10.83
10.84 -Macro rules may refer to any syntax from the parent theories. They may
10.85 -also refer to anything defined before the {\tt .thy} file's {\tt
10.86 +Macro rules may refer to any syntax from the parent theories. They
10.87 +may also refer to anything defined before the current {\tt
10.88 translations} section --- including any mixfix declarations.
10.89
10.90 Upon declaration, both sides of the macro rule undergo parsing and parse
10.91 @@ -440,10 +443,11 @@
10.92 matching. These are all names that have been declared as classes, types or
10.93 constants (logical and syntactic).
10.94
10.95 -The result of this preprocessing is two lists of macro rules, each stored
10.96 -as a pair of \AST{}s. They can be viewed using {\tt print_syntax}
10.97 -(sections \ttindex{parse_rules} and \ttindex{print_rules}). For
10.98 -theory~{\tt SET} of Fig.~\ref{fig:set_trans} these are
10.99 +The result of this preprocessing is two lists of macro rules, each
10.100 +stored as a pair of \AST{}s. They can be viewed using {\tt
10.101 + print_syntax} (sections \ttindex{parse_rules} and
10.102 +\ttindex{print_rules}). For theory~{\tt SetSyntax} of
10.103 +Fig.~\ref{fig:set_trans} these are
10.104 \begin{ttbox}
10.105 parse_rules:
10.106 ("{\at}Collect" x A P) -> ("Collect" A ("_abs" x P))
10.107 @@ -484,9 +488,7 @@
10.108
10.109 To allow such constraints to be re-read, your syntax should specify bound
10.110 variables using the nonterminal~\ndx{idt}. This is the case in our
10.111 -example. Choosing {\tt id} instead of {\tt idt} is a common error,
10.112 -especially since it appears in former versions of most of Isabelle's
10.113 -object-logics.
10.114 +example. Choosing {\tt id} instead of {\tt idt} is a common error.
10.115 \end{warn}
10.116
10.117
10.118 @@ -552,17 +554,17 @@
10.119 The term \verb|%Nil.t| will be printed as \verb|%[].t|, which might not be
10.120 expected! Guess how type~{\tt Nil} is printed?
10.121
10.122 -Normalizing an \AST{} involves repeatedly applying macro rules until none
10.123 -are applicable. Macro rules are chosen in the order that they appear in the
10.124 -{\tt translations} section. You can watch the normalization of \AST{}s
10.125 -during parsing and printing by setting \ttindex{Syntax.trace_norm_ast} to
10.126 -{\tt true}.\index{tracing!of macros} Alternatively, use
10.127 +Normalizing an \AST{} involves repeatedly applying macro rules until
10.128 +none are applicable. Macro rules are chosen in order of appearance in
10.129 +the theory definitions. You can watch the normalization of \AST{}s
10.130 +during parsing and printing by setting \ttindex{Syntax.trace_norm_ast}
10.131 +to {\tt true}.\index{tracing!of macros} Alternatively, use
10.132 \ttindex{Syntax.test_read}. The information displayed when tracing
10.133 -includes the \AST{} before normalization ({\tt pre}), redexes with results
10.134 -({\tt rewrote}), the normal form finally reached ({\tt post}) and some
10.135 -statistics ({\tt normalize}). If tracing is off,
10.136 -\ttindex{Syntax.stat_norm_ast} can be set to {\tt true} in order to enable
10.137 -printing of the normal form and statistics only.
10.138 +includes the \AST{} before normalization ({\tt pre}), redexes with
10.139 +results ({\tt rewrote}), the normal form finally reached ({\tt post})
10.140 +and some statistics ({\tt normalize}). If tracing is off,
10.141 +\ttindex{Syntax.stat_norm_ast} can be set to {\tt true} in order to
10.142 +enable printing of the normal form and statistics only.
10.143
10.144
10.145 \subsection{Example: the syntax of finite sets}
10.146 @@ -574,7 +576,7 @@
10.147 \index{"@Enum@{\tt\at Enum} constant}
10.148 \index{"@Finset@{\tt\at Finset} constant}
10.149 \begin{ttbox}
10.150 -FINSET = SET +
10.151 +FinSyntax = SetSyntax +
10.152 types
10.153 is
10.154 syntax
10.155 @@ -654,7 +656,7 @@
10.156 readable in some cases: {\em calling\/} translation functions by parse
10.157 macros:
10.158 \begin{ttbox}
10.159 -PROD = FINSET +
10.160 +ProdSyntax = FinSyntax +
10.161 consts
10.162 Pi :: [i, i => i] => i
10.163 syntax
10.164 @@ -693,10 +695,10 @@
10.165 \index{translations|(}
10.166 %
10.167 This section describes the translation function mechanism. By writing
10.168 -\ML{} functions, you can do almost everything with terms or \AST{}s during
10.169 -parsing and printing. The logic \LK\ is a good example of sophisticated
10.170 -transformations between internal and external representations of sequents;
10.171 -here, macros would be useless.
10.172 +\ML{} functions, you can do almost everything to terms or \AST{}s
10.173 +during parsing and printing. The logic \LK\ is a good example of
10.174 +sophisticated transformations between internal and external
10.175 +representations of sequents; here, macros would be useless.
10.176
10.177 A full understanding of translations requires some familiarity
10.178 with Isabelle's internals, especially the datatypes {\tt term}, {\tt typ},
10.179 @@ -705,50 +707,55 @@
10.180 use translation functions.
10.181
10.182 \subsection{Declaring translation functions}
10.183 -There are four kinds of translation functions. Each such function is
10.184 -associated with a name, which triggers calls to it. Such names can be
10.185 -constants (logical or syntactic) or type constructors.
10.186 +There are four kinds of translation functions, with one of these
10.187 +coming in two variants. Each such function is associated with a name,
10.188 +which triggers calls to it. Such names can be constants (logical or
10.189 +syntactic) or type constructors.
10.190
10.191 {\tt print_syntax} displays the sets of names associated with the
10.192 -translation functions of a {\tt Syntax.syntax} under
10.193 +translation functions of a theory under
10.194 \ttindex{parse_ast_translation}, \ttindex{parse_translation},
10.195 -\ttindex{print_translation} and \ttindex{print_ast_translation}. You can
10.196 -add new ones via the {\tt ML} section\index{*ML section} of
10.197 -a {\tt .thy} file. There may never be more than one function of the same
10.198 -kind per name. Even though the {\tt ML} section is the very last part of a
10.199 -{\tt .thy} file, newly installed translation functions are effective when
10.200 -processing the preceding section.
10.201 +\ttindex{print_translation} and \ttindex{print_ast_translation}. You
10.202 +can add new ones via the {\tt ML} section\index{*ML section} of a
10.203 +theory definition file. There may never be more than one function of
10.204 +the same kind per name. Even though the {\tt ML} section is the very
10.205 +last part of the file, newly installed translation functions are
10.206 +already effective when processing all of the preceding sections.
10.207
10.208 -The {\tt ML} section is copied verbatim near the beginning of the \ML\ file
10.209 -generated from a {\tt .thy} file. Definitions made here are accessible as
10.210 -components of an \ML\ structure; to make some definitions private, use an
10.211 -\ML{} {\tt local} declaration. The {\tt ML} section may install translation
10.212 -functions by declaring any of the following identifiers:
10.213 +The {\tt ML} section's contents are simply copied verbatim near the
10.214 +beginning of the \ML\ file generated from a theory definition file.
10.215 +Definitions made here are accessible as components of an \ML\
10.216 +structure; to make some parts private, use an \ML{} {\tt local}
10.217 +declaration. The {\ML} code may install translation functions by
10.218 +declaring any of the following identifiers:
10.219 \begin{ttbox}
10.220 -val parse_ast_translation : (string * (ast list -> ast)) list
10.221 -val print_ast_translation : (string * (ast list -> ast)) list
10.222 -val parse_translation : (string * (term list -> term)) list
10.223 -val print_translation : (string * (term list -> term)) list
10.224 +val parse_ast_translation : (string * (ast list -> ast)) list
10.225 +val print_ast_translation : (string * (ast list -> ast)) list
10.226 +val parse_translation : (string * (term list -> term)) list
10.227 +val print_translation : (string * (term list -> term)) list
10.228 +val typed_print_translation : (string * (typ -> term list -> term)) list
10.229 \end{ttbox}
10.230
10.231 \subsection{The translation strategy}
10.232 -All four kinds of translation functions are treated similarly. They are
10.233 -called during the transformations between parse trees, \AST{}s and terms
10.234 -(recall Fig.\ts\ref{fig:parse_print}). Whenever a combination of the form
10.235 -$(\mtt"c\mtt"~x@1 \ldots x@n)$ is encountered, and a translation function
10.236 -$f$ of appropriate kind exists for $c$, the result is computed by the \ML{}
10.237 -function call $f \mtt[ x@1, \ldots, x@n \mtt]$.
10.238 +The different kinds of translation functions are called during the
10.239 +transformations between parse trees, \AST{}s and terms (recall
10.240 +Fig.\ts\ref{fig:parse_print}). Whenever a combination of the form
10.241 +$(\mtt"c\mtt"~x@1 \ldots x@n)$ is encountered, and a translation
10.242 +function $f$ of appropriate kind exists for $c$, the result is
10.243 +computed by the \ML{} function call $f \mtt[ x@1, \ldots, x@n \mtt]$.
10.244
10.245 -For \AST{} translations, the arguments $x@1, \ldots, x@n$ are \AST{}s. A
10.246 -combination has the form $\Constant c$ or $\Appl{\Constant c, x@1, \ldots,
10.247 - x@n}$. For term translations, the arguments are terms and a combination
10.248 -has the form $\ttfct{Const} (c, \tau)$ or $\ttfct{Const} (c, \tau) \ttapp
10.249 -x@1 \ttapp \ldots \ttapp x@n$. Terms allow more sophisticated
10.250 -transformations than \AST{}s do, typically involving abstractions and bound
10.251 -variables.
10.252 +For \AST{} translations, the arguments $x@1, \ldots, x@n$ are \AST{}s.
10.253 +A combination has the form $\Constant c$ or $\Appl{\Constant c, x@1,
10.254 + \ldots, x@n}$. For term translations, the arguments are terms and a
10.255 +combination has the form $\ttfct{Const} (c, \tau)$ or $\ttfct{Const}
10.256 +(c, \tau) \ttapp x@1 \ttapp \ldots \ttapp x@n$. Terms allow more
10.257 +sophisticated transformations than \AST{}s do, typically involving
10.258 +abstractions and bound variables. {\em Typed} print translations may
10.259 +even peek at the type $\tau$ of the constant they are invoked on.
10.260
10.261 -Regardless of whether they act on terms or \AST{}s, parse translations differ
10.262 -from print translations in their overall behaviour fundamentally:
10.263 +Regardless of whether they act on terms or \AST{}s, translation
10.264 +functions called during the parsing process differ from those for
10.265 +printing more fundamentally in their overall behaviour:
10.266 \begin{description}
10.267 \item[Parse translations] are applied bottom-up. The arguments are already
10.268 in translated form. The translations must not fail; exceptions trigger
10.269 @@ -804,40 +811,93 @@
10.270 \begin{ttbox}
10.271 fun dependent_tr' (q, r) (A :: Abs (x, T, B) :: ts) =
10.272 if 0 mem (loose_bnos B) then
10.273 - let val (x', B') = variant_abs (x, dummyT, B);
10.274 - in list_comb (Const (q, dummyT) $ Free (x', T) $ A $ B', ts)
10.275 + let val (x', B') = Syntax.variant_abs' (x, dummyT, B) in
10.276 + list_comb
10.277 + (Const (q, dummyT) $ Syntax.mark_boundT (x', T) $ A $ B', ts)
10.278 end
10.279 else list_comb (Const (r, dummyT) $ A $ B, ts)
10.280 | dependent_tr' _ _ = raise Match;
10.281 \end{ttbox}
10.282 -The argument {\tt (q,r)} is supplied to the curried function {\tt
10.283 - dependent_tr'} by a partial application during its installation. We
10.284 -can set up print translations for both {\tt Pi} and {\tt Sigma} by
10.285 -including
10.286 +The argument {\tt (q, r)} is supplied to the curried function {\tt
10.287 + dependent_tr'} by a partial application during its installation.
10.288 +For example, we could set up print translations for both {\tt Pi} and
10.289 +{\tt Sigma} by including
10.290 \begin{ttbox}\index{*ML section}
10.291 val print_translation =
10.292 [("Pi", dependent_tr' ("{\at}PROD", "{\at}->")),
10.293 ("Sigma", dependent_tr' ("{\at}SUM", "{\at}*"))];
10.294 \end{ttbox}
10.295 -within the {\tt ML} section. The first of these transforms ${\tt Pi}(A,
10.296 -\mtt{Abs}(x, T, B))$ into $\hbox{\tt{\at}PROD}(x', A, B')$ or
10.297 -$\hbox{\tt{\at}->}(A, B)$, choosing the latter form if $B$ does not depend
10.298 -on~$x$. It checks this using \ttindex{loose_bnos}, yet another function
10.299 -from {\tt Pure/term.ML}. Note that $x'$ is a version of $x$ renamed away
10.300 -from all names in $B$, and $B'$ is the body $B$ with {\tt Bound} nodes
10.301 -referring to the {\tt Abs} node replaced by $\ttfct{Free} (x',
10.302 -\mtt{dummyT})$.
10.303 +within the {\tt ML} section. The first of these transforms ${\tt
10.304 + Pi}(A, \mtt{Abs}(x, T, B))$ into $\hbox{\tt{\at}PROD}(x', A, B')$ or
10.305 +$\hbox{\tt{\at}->}(A, B)$, choosing the latter form if $B$ does not
10.306 +depend on~$x$. It checks this using \ttindex{loose_bnos}, yet another
10.307 +function from {\tt Pure/term.ML}. Note that $x'$ is a version of $x$
10.308 +renamed away from all names in $B$, and $B'$ is the body $B$ with {\tt
10.309 + Bound} nodes referring to the {\tt Abs} node replaced by
10.310 +$\ttfct{Free} (x', \mtt{dummyT})$ (but marked as representing a bound
10.311 +variable).
10.312
10.313 We must be careful with types here. While types of {\tt Const}s are
10.314 ignored, type constraints may be printed for some {\tt Free}s and
10.315 {\tt Var}s if \ttindex{show_types} is set to {\tt true}. Variables of type
10.316 \ttindex{dummyT} are never printed with constraint, though. The line
10.317 \begin{ttbox}
10.318 - let val (x', B') = variant_abs (x, dummyT, B);
10.319 -\end{ttbox}\index{*variant_abs}
10.320 + let val (x', B') = Syntax.variant_abs' (x, dummyT, B);
10.321 +\end{ttbox}\index{*Syntax.variant_abs'}
10.322 replaces bound variable occurrences in~$B$ by the free variable $x'$ with
10.323 type {\tt dummyT}. Only the binding occurrence of~$x'$ is given the
10.324 correct type~{\tt T}, so this is the only place where a type
10.325 constraint might appear.
10.326 -\index{translations|)}
10.327 -\index{syntax!transformations|)}
10.328 +
10.329 +Also note that we are responsible to mark free identifiers that
10.330 +actually represent bound variables. This is achieved by
10.331 +\ttindex{Syntax.variant_abs'} and \ttindex{Syntax.mark_boundT} above.
10.332 +Failing to do so may cause these names to be printed in the wrong
10.333 +style. \index{translations|)} \index{syntax!transformations|)}
10.334 +
10.335 +
10.336 +\section{Token translations} \label{sec:tok_tr}
10.337 +\index{token translations|(}
10.338 +%
10.339 +Isabelle's meta-logic features quite a lot of different kinds of
10.340 +identifiers, namely {\em class}, {\em tfree}, {\em tvar}, {\em free},
10.341 +{\em bound}, {\em var}. One might want to have these printed in
10.342 +different styles, e.g.\ in bold or italic, or even transcribed into
10.343 +something more readable like $\alpha, \alpha', \beta$ instead of {\tt
10.344 + 'a}, {\tt 'aa}, {\tt 'b} for type variables. Token translations
10.345 +provide a means to such ends, enabling the user to install certain
10.346 +\ML{} functions associated with any logical \rmindex{token class} and
10.347 +depending on some \rmindex{print mode}.
10.348 +
10.349 +The logical class of identifiers can not necessarily be determined by
10.350 +its syntactic category, though. For example, consider free vs.\ bound
10.351 +variables. So Isabelle's pretty printing mechanism, starting from
10.352 +fully typed terms, has to be careful to preserve this additional
10.353 +information\footnote{This is done by marking atoms in abstract syntax
10.354 + trees appropriately. The marks are actually visible by print
10.355 + translation functions -- they are just special constants applied to
10.356 + atomic asts, for example \texttt{("_bound" x)}.}. In particular,
10.357 +user-supplied print translation functions operating on terms have to
10.358 +be well-behaved in this respect. Free identifiers introduced to
10.359 +represent bound variables have to be marked appropriately (cf.\ the
10.360 +example at the end of \S\ref{sec:tr_funs}).
10.361 +
10.362 +\medskip Token translations may be installed by declaring the
10.363 +\ttindex{token_translation} value within the \texttt{ML} section of a
10.364 +theory definition file:
10.365 +\begin{ttbox}
10.366 +val token_translation: (string * string * (string -> string * int)) list
10.367 +\end{ttbox}\index{token_translation}
10.368 +The elements of this list are of the form $(m, c, f)$, where $m$ is a
10.369 +print mode identifier, $c$ a token class, and $f\colon string \to
10.370 +string \times int$ the actual translation function. Assuming that $x$
10.371 +is of identifier class $c$, and print mode $m$ is the first one of all
10.372 +currently active modes that provide some translation for $c$, then $x$
10.373 +is output according to $f(x) = (x', len)$. Thereby $x'$ is the
10.374 +modified identifier name and $len$ its visual length approximated in
10.375 +terms of whole characters. Thus $x'$ may include non-printing parts
10.376 +like control sequences or markup information for typesetting systems.
10.377 +
10.378 +%FIXME example (?)
10.379 +
10.380 +\index{token translations|)}
11.1 --- a/doc-src/Ref/tactic.tex Mon May 05 21:18:01 1997 +0200
11.2 +++ b/doc-src/Ref/tactic.tex Tue May 06 12:50:16 1997 +0200
11.3 @@ -1,10 +1,10 @@
11.4 %% $Id$
11.5 \chapter{Tactics} \label{tactics}
11.6 -\index{tactics|(}
11.7 -Tactics have type \mltydx{tactic}. They are essentially
11.8 -functions from theorems to theorem sequences, where the theorems represent
11.9 -states of a backward proof. Tactics seldom need to be coded from scratch,
11.10 -as functions; instead they are expressed using basic tactics and tacticals.
11.11 +\index{tactics|(} Tactics have type \mltydx{tactic}. This is just an
11.12 +abbreviation for functions from theorems to theorem sequences, where
11.13 +the theorems represent states of a backward proof. Tactics seldom
11.14 +need to be coded from scratch, as functions; instead they are
11.15 +expressed using basic tactics and tacticals.
11.16
11.17 This chapter only presents the primitive tactics. Substantial proofs require
11.18 the power of simplification (Chapter~\ref{simp-chap}) and classical reasoning
11.19 @@ -561,26 +561,17 @@
11.20 \index{tactics!primitives for coding}
11.21 A tactic maps theorems to theorem sequences (lazy lists). The type
11.22 constructor for sequences is called \mltydx{Sequence.seq}. To simplify the
11.23 -types of tactics and tacticals, Isabelle defines a type of tactics:
11.24 +types of tactics and tacticals, Isabelle defines a type abbreviations:
11.25 \begin{ttbox}
11.26 -datatype tactic = Tactic of thm -> thm Sequence.seq
11.27 +type tactic = thm -> thm Sequence.seq
11.28 \end{ttbox}
11.29 -{\tt Tactic} and {\tt tapply} convert between tactics and functions. The
11.30 -other operations provide means for coding tactics in a clean style.
11.31 +The following operations provide means for coding tactics in a clean style.
11.32 \begin{ttbox}
11.33 -tapply : tactic * thm -> thm Sequence.seq
11.34 -Tactic : (thm -> thm Sequence.seq) -> tactic
11.35 PRIMITIVE : (thm -> thm) -> tactic
11.36 STATE : (thm -> tactic) -> tactic
11.37 SUBGOAL : ((term*int) -> tactic) -> int -> tactic
11.38 \end{ttbox}
11.39 \begin{ttdescription}
11.40 -\item[\ttindexbold{tapply}({\it tac}, {\it thm})]
11.41 -returns the result of applying the tactic, as a function, to {\it thm}.
11.42 -
11.43 -\item[\ttindexbold{Tactic} {\it f}]
11.44 -packages {\it f} as a tactic.
11.45 -
11.46 \item[\ttindexbold{PRIMITIVE} $f$]
11.47 applies $f$ to the proof state and returns the result as a
11.48 one-element sequence. This packages the meta-rule~$f$ as a tactic.
12.1 --- a/doc-src/Ref/tctical.tex Mon May 05 21:18:01 1997 +0200
12.2 +++ b/doc-src/Ref/tctical.tex Tue May 06 12:50:16 1997 +0200
12.3 @@ -126,9 +126,8 @@
12.4 \begin{ttbox}
12.5 fun TRY tac = tac ORELSE all_tac;
12.6
12.7 -fun REPEAT tac = Tactic
12.8 - (fn state => tapply((tac THEN REPEAT tac) ORELSE all_tac,
12.9 - state));
12.10 +fun REPEAT tac =
12.11 + (fn state => ((tac THEN REPEAT tac) ORELSE all_tac) state);
12.12 \end{ttbox}
12.13 If $tac$ can return multiple outcomes then so can \hbox{\tt REPEAT $tac$}.
12.14 Since {\tt REPEAT} uses \ttindex{ORELSE} and not {\tt APPEND} or {\tt
13.1 --- a/doc-src/Ref/theories.tex Mon May 05 21:18:01 1997 +0200
13.2 +++ b/doc-src/Ref/theories.tex Tue May 06 12:50:16 1997 +0200
13.3 @@ -2,12 +2,12 @@
13.4
13.5 \chapter{Theories, Terms and Types} \label{theories}
13.6 \index{theories|(}\index{signatures|bold}
13.7 -\index{reading!axioms|see{{\tt assume_ax}}}
13.8 -Theories organize the syntax, declarations and axioms of a mathematical
13.9 -development. They are built, starting from the Pure theory, by extending
13.10 -and merging existing theories. They have the \ML\ type \mltydx{theory}.
13.11 -Theory operations signal errors by raising exception \xdx{THEORY},
13.12 -returning a message and a list of theories.
13.13 +\index{reading!axioms|see{{\tt assume_ax}}} Theories organize the
13.14 +syntax, declarations and axioms of a mathematical development. They
13.15 +are built, starting from the {\Pure} or {\CPure} theory, by extending
13.16 +and merging existing theories. They have the \ML\ type
13.17 +\mltydx{theory}. Theory operations signal errors by raising exception
13.18 +\xdx{THEORY}, returning a message and a list of theories.
13.19
13.20 Signatures, which contain information about sorts, types, constants and
13.21 syntax, have the \ML\ type~\mltydx{Sign.sg}. For identification, each
13.22 @@ -32,11 +32,12 @@
13.23 Appendix~\ref{app:TheorySyntax} presents the concrete syntax for theory
13.24 definitions; here is an explanation of the constituent parts:
13.25 \begin{description}
13.26 -\item[{\it theoryDef}]
13.27 - is the full definition. The new theory is called $id$. It is the union
13.28 - of the named {\bf parent theories}\indexbold{theories!parent}, possibly
13.29 - extended with new classes, etc. The basic theory, which contains only
13.30 - the meta-logic, is called \thydx{Pure}.
13.31 +\item[{\it theoryDef}] is the full definition. The new theory is
13.32 + called $id$. It is the union of the named {\bf parent
13.33 + theories}\indexbold{theories!parent}, possibly extended with new
13.34 + components. \thydx{Pure} and \thydx{CPure} are the basic theories,
13.35 + which contain only the meta-logic. They differ just in their
13.36 + concrete syntax for function applications.
13.37
13.38 Normally each {\it name\/} is an identifier, the name of the parent theory.
13.39 Quoted strings can be used to document additional file dependencies; see
13.40 @@ -56,10 +57,9 @@
13.41 variables created internally. If omitted, the default sort is the listwise
13.42 union of the default sorts of the parent theories (i.e.\ their logical
13.43 intersection).
13.44 -
13.45 -\item[$sort$]
13.46 - is a finite set of classes. A single class $id$ abbreviates the singleton
13.47 - set {\tt\{}$id${\tt\}}.
13.48 +
13.49 +\item[$sort$] is a finite set of classes. A single class $id$
13.50 + abbreviates the sort $\ttlbrace id\ttrbrace$.
13.51
13.52 \item[$types$]
13.53 is a series of type declarations. Each declares a new type constructor
13.54 @@ -75,19 +75,23 @@
13.55 declares a type or constant to be an infix operator of priority $nat$
13.56 associating to the left ({\tt infixl}) or right ({\tt infixr}). Only
13.57 2-place type constructors can have infix status; an example is {\tt
13.58 - ('a,'b)~"*"~(infixr~20)}, which expresses binary product types.
13.59 + ('a,'b)~"*"~(infixr~20)}, which may express binary product types.
13.60
13.61 -\item[$arities$]
13.62 - is a series of arity declarations. Each assigns arities to type
13.63 - constructors. The $name$ must be an existing type constructor, which is
13.64 - given the additional arity $arity$.
13.65 -
13.66 -\item[$constDecl$]
13.67 - is a series of constant declarations. Each new constant $name$ is given
13.68 - the specified type. The optional $mixfix$ annotations may
13.69 - attach concrete syntax to the constant. A variant of {\tt consts} is the
13.70 - {\tt syntax} section\index{*syntax section}, which adds just syntax without
13.71 - declaring logical constants.
13.72 +\item[$arities$] is a series of type arity declarations. Each assigns
13.73 + arities to type constructors. The $name$ must be an existing type
13.74 + constructor, which is given the additional arity $arity$.
13.75 +
13.76 +\item[$consts$] is a series of constant declarations. Each new
13.77 + constant $name$ is given the specified type. The optional $mixfix$
13.78 + annotations may attach concrete syntax to the constant.
13.79 +
13.80 +\item[$syntax$] \index{*syntax section}\index{print mode} is a variant
13.81 + of $consts$ which adds just syntax without actually declaring
13.82 + logical constants. This gives full control over a theory's context
13.83 + free grammar. The optional $mode$ specifies the print mode where the
13.84 + mixfix productions should be added. If there is no \texttt{output}
13.85 + option given, all productions are also added to the input syntax
13.86 + (regardless of the print mode).
13.87
13.88 \item[$mixfix$] \index{mixfix declarations}
13.89 annotations can take three forms:
13.90 @@ -115,13 +119,28 @@
13.91 \item[$rules$]
13.92 is a series of rule declarations. Each has a name $id$ and the formula is
13.93 given by the $string$. Rule names must be distinct within any single
13.94 - theory file.
13.95 + theory.
13.96
13.97 \item[$defs$] is a series of definitions. They are just like $rules$, except
13.98 that every $string$ must be a definition (see below for details).
13.99
13.100 \item[$constdefs$] combines the declaration of constants and their
13.101 definition. The first $string$ is the type, the second the definition.
13.102 +
13.103 +\item[$axclass$] \index{*axclass section} defines an
13.104 + \rmindex{axiomatic type class} as the intersection of existing
13.105 + classes, with additional axioms holding. Class axioms may not
13.106 + contain more than one type variable. The class axioms (with implicit
13.107 + sort constraints added) are bound to the given names. Furthermore a
13.108 + class introduction rule is generated, which is automatically
13.109 + employed by $instance$ to prove instantiations of this class.
13.110 +
13.111 +\item[$instance$] \index{*instance section} proves class inclusions or
13.112 + type arities at the logical level and then transfers these to the
13.113 + type signature. The instantiation is proven and checked properly.
13.114 + The user has to supply sufficient witness information: theorems
13.115 + ($longident$), axioms ($string$), or even arbitrary \ML{} tactic
13.116 + code $verbatim$.
13.117
13.118 \item[$oracle$] links the theory to a trusted external reasoner. It is
13.119 allowed to create theorems, but each theorem carries a proof object
13.120 @@ -137,18 +156,19 @@
13.121
13.122 \subsection{Definitions}\indexbold{definitions}
13.123
13.124 -{\bf Definitions} are intended to express abbreviations. The simplest form of
13.125 -a definition is $f \equiv t$, where $f$ is a constant. Isabelle also allows a
13.126 -derived form where the arguments of~$f$ appear on the left, abbreviating a
13.127 -string of $\lambda$-abstractions.
13.128 +{\bf Definitions} are intended to express abbreviations. The simplest
13.129 +form of a definition is $f \equiv t$, where $f$ is a constant.
13.130 +Isabelle also allows a derived forms where the arguments of~$f$ appear
13.131 +on the left, abbreviating a string of $\lambda$-abstractions.
13.132
13.133 Isabelle makes the following checks on definitions:
13.134 \begin{itemize}
13.135 -\item Arguments (on the left-hand side) must be distinct variables
13.136 +\item Arguments (on the left-hand side) must be distinct variables.
13.137 \item All variables on the right-hand side must also appear on the left-hand
13.138 side.
13.139 -\item All type variables on the right-hand side must also appear on the
13.140 - left-hand side; this prohibits definitions such as {\tt zero == length []}.
13.141 +\item All type variables on the right-hand side must also appear on
13.142 + the left-hand side; this prohibits definitions such as {\tt
13.143 + (zero::nat) == length ([]::'a list)}.
13.144 \item The definition must not be recursive. Most object-logics provide
13.145 definitional principles that can be used to express recursion safely.
13.146 \end{itemize}
13.147 @@ -164,31 +184,26 @@
13.148 In order to guarantee principal types~\cite{nipkow-prehofer},
13.149 arity declarations must obey two conditions:
13.150 \begin{itemize}
13.151 -\item There must be no two declarations $ty :: (\vec{r})c$ and $ty ::
13.152 - (\vec{s})c$ with $\vec{r} \neq \vec{s}$. For example, the following is
13.153 - forbidden:
13.154 +\item There must not be any two declarations $ty :: (\vec{r})c$ and
13.155 + $ty :: (\vec{s})c$ with $\vec{r} \neq \vec{s}$. For example, this
13.156 + excludes the following:
13.157 \begin{ttbox}
13.158 -types
13.159 - 'a ty
13.160 arities
13.161 - ty :: ({\ttlbrace}logic{\ttrbrace}) logic
13.162 - ty :: ({\ttlbrace}{\ttrbrace})logic
13.163 + foo :: ({\ttlbrace}logic{\ttrbrace}) logic
13.164 + foo :: ({\ttlbrace}{\ttrbrace})logic
13.165 \end{ttbox}
13.166
13.167 \item If there are two declarations $ty :: (s@1,\dots,s@n)c$ and $ty ::
13.168 (s@1',\dots,s@n')c'$ such that $c' < c$ then $s@i' \preceq s@i$ must hold
13.169 for $i=1,\dots,n$. The relationship $\preceq$, defined as
13.170 \[ s' \preceq s \iff \forall c\in s. \exists c'\in s'.~ c'\le c, \]
13.171 -expresses that the set of types represented by $s'$ is a subset of the set of
13.172 -types represented by $s$. For example, the following is forbidden:
13.173 +expresses that the set of types represented by $s'$ is a subset of the
13.174 +set of types represented by $s$. Assuming $term \preceq logic$, the
13.175 +following is forbidden:
13.176 \begin{ttbox}
13.177 -classes
13.178 - term < logic
13.179 -types
13.180 - 'a ty
13.181 arities
13.182 - ty :: ({\ttlbrace}logic{\ttrbrace})logic
13.183 - ty :: ({\ttlbrace}{\ttrbrace})term
13.184 + foo :: ({\ttlbrace}logic{\ttrbrace})logic
13.185 + foo :: ({\ttlbrace}{\ttrbrace})term
13.186 \end{ttbox}
13.187
13.188 \end{itemize}
13.189 @@ -219,14 +234,15 @@
13.190 suppresses the deletion of temporary files.
13.191 \end{ttdescription}
13.192 %
13.193 -Each theory definition must reside in a separate file. Let the file {\it
13.194 - T}{\tt.thy} contain the definition of a theory called~$T$, whose parent
13.195 -theories are $TB@1$ \dots $TB@n$. Calling \ttindexbold{use_thy}~{\tt"{\it
13.196 - T\/}"} reads the file {\it T}{\tt.thy}, writes a temporary \ML{}
13.197 -file {\tt.{\it T}.thy.ML}, and reads the latter file. Recursive {\tt
13.198 - use_thy} calls load those parent theories that have not been loaded
13.199 -previously; the recursive calls may continue to any depth. One {\tt use_thy}
13.200 -call can read an entire logic provided all theories are linked appropriately.
13.201 +Each theory definition must reside in a separate file. Let the file
13.202 +{\it T}{\tt.thy} contain the definition of a theory called~$T$, whose
13.203 +parent theories are $TB@1$ \dots $TB@n$. Calling
13.204 +\ttindex{use_thy}~{\tt"{\it T\/}"} reads the file {\it T}{\tt.thy},
13.205 +writes a temporary \ML{} file {\tt.{\it T}.thy.ML}, and reads the
13.206 +latter file. Recursive {\tt use_thy} calls load those parent theories
13.207 +that have not been loaded previously; the recursive calls may continue
13.208 +to any depth. One {\tt use_thy} call can read an entire logic
13.209 +provided all theories are linked appropriately.
13.210
13.211 The result is an \ML\ structure~$T$ containing at least a component {\tt thy}
13.212 for the new theory and components for each of the rules. The structure also
13.213 @@ -234,9 +250,9 @@
13.214 {\tt.{\it T}.thy.ML} is then deleted if {\tt delete_tmpfiles} is set to {\tt
13.215 true} and no errors occurred.
13.216
13.217 -Finally the file {\it T}{\tt.ML} is read, if it exists. This file normally
13.218 -begins with the declaration {\tt open~$T$} and contains proofs involving
13.219 -the new theory.
13.220 +Finally the file {\it T}{\tt.ML} is read, if it exists. Since the
13.221 +structure $T$ is automatically open in this context, proof scripts may
13.222 +(or even should) refer to its components by unqualified names.
13.223
13.224 Some applications construct theories directly by calling \ML\ functions. In
13.225 this situation there is no {\tt.thy} file, only an {\tt.ML} file. The
13.226 @@ -284,17 +300,18 @@
13.227 \end{ttdescription}
13.228
13.229
13.230 -\goodbreak
13.231 -\subsection{Important note for Poly/ML users}\index{Poly/{\ML} compiler}
13.232 -The theory mechanism depends upon reference variables. At the end of a
13.233 -Poly/\ML{} session, the contents of references are lost unless they are
13.234 -declared in the current database. In particular, assignments to references
13.235 -of the {\tt Pure} database are lost, including all information about loaded
13.236 -theories. To avoid losing this information simply call
13.237 -\begin{ttbox}
13.238 -init_thy_reader();
13.239 -\end{ttbox}
13.240 -when building the new database.
13.241 +%FIXME remove
13.242 +%\goodbreak
13.243 +%\subsection{Important note for Poly/ML users}\index{Poly/{\ML} compiler}
13.244 +%The theory mechanism depends upon reference variables. At the end of a
13.245 +%Poly/\ML{} session, the contents of references are lost unless they are
13.246 +%declared in the current database. In particular, assignments to references
13.247 +%of the {\tt Pure} database are lost, including all information about loaded
13.248 +%theories. To avoid losing this information simply call
13.249 +%\begin{ttbox}
13.250 +%init_thy_reader();
13.251 +%\end{ttbox}
13.252 +%when building the new database.
13.253
13.254
13.255 \subsection{*Pseudo theories}\label{sec:pseudo-theories}
13.256 @@ -346,9 +363,9 @@
13.257 The resulting theory ensures that {\tt update} reloads {\tt orphan}
13.258 whenever it reloads one of the $A@i$.
13.259
13.260 -For an extensive example of how this technique can be used to link lots of
13.261 -theory files and load them by just a few {\tt use_thy} calls, consult the
13.262 -sources of \ZF{} set theory.
13.263 +For an extensive example of how this technique can be used to link
13.264 +lots of theory files and load them by just a few {\tt use_thy} calls
13.265 +see the sources of one of the major object-logics (e.g.\ \ZF).
13.266
13.267
13.268
13.269 @@ -384,17 +401,21 @@
13.270 \hbox{\verb'?a=?b ==> ?b=?a [!!a b. a=b ==> b=a]'}
13.271 \end{ttdescription}
13.272
13.273 -\subsection{Building a theory}
13.274 +\subsection{*Building a theory}
13.275 \label{BuildingATheory}
13.276 \index{theories!constructing|bold}
13.277 \begin{ttbox}
13.278 -pure_thy : theory
13.279 +Pure.thy : theory
13.280 +CPure.thy : theory
13.281 merge_theories : theory * theory -> theory
13.282 \end{ttbox}
13.283 -\begin{ttdescription}
13.284 -\item[\ttindexbold{pure_thy}] contains just the syntax and signature
13.285 - of the meta-logic. There are no axioms: meta-level inferences are carried
13.286 - out by \ML\ functions.
13.287 +\begin{description}
13.288 +\item[\ttindexbold{Pure.thy}, \ttindexbold{CPure.thy}] contain the
13.289 + syntax and signature of the meta-logic. There are no axioms:
13.290 + meta-level inferences are carried out by \ML\ functions. The two
13.291 + \Pure s just differ in their concrete syntax of function
13.292 + application: $t(u@1, \ldots, u@n)$ vs.\ $t\,u@1,\ldots\,u@n$.
13.293 +
13.294 \item[\ttindexbold{merge_theories} ($thy@1$, $thy@2$)] merges the two
13.295 theories $thy@1$ and $thy@2$. The resulting theory contains all of the
13.296 syntax, signature and axioms of the constituent theories. Merging theories
13.297 @@ -419,7 +440,7 @@
13.298 %\begin{ttbox}
13.299 %Attempt to merge different versions of theory: \(T\)
13.300 %\end{ttbox}
13.301 -\end{ttdescription}
13.302 +\end{description}
13.303
13.304 %% FIXME
13.305 %\item [\ttindexbold{extend_theory} $thy$ {\tt"}$T${\tt"}
13.306 @@ -456,6 +477,7 @@
13.307 \subsection{Inspecting a theory}\label{sec:inspct-thy}
13.308 \index{theories!inspecting|bold}
13.309 \begin{ttbox}
13.310 +print_syntax : theory -> unit
13.311 print_theory : theory -> unit
13.312 axioms_of : theory -> (string * thm) list
13.313 thms_of : theory -> (string * thm) list
13.314 @@ -465,9 +487,12 @@
13.315 \end{ttbox}
13.316 These provide means of viewing a theory's components.
13.317 \begin{ttdescription}
13.318 -\item[\ttindexbold{print_theory} $thy$]
13.319 -prints the contents of $thy$ excluding the syntax related parts (which are
13.320 -shown by {\tt print_syntax}). The output is quite verbose.
13.321 +\item[\ttindexbold{print_syntax} $thy$] prints the syntax of $thy$
13.322 + (grammar, macros, translation functions etc., see
13.323 + page~\pageref{pg:print_syn} for more details).
13.324 +
13.325 +\item[\ttindexbold{print_theory} $thy$] prints the logical parts of
13.326 + $thy$, excluding the syntax.
13.327
13.328 \item[\ttindexbold{axioms_of} $thy$]
13.329 returns the additional axioms of the most recent extend node of~$thy$.
13.330 @@ -487,223 +512,224 @@
13.331 with~$thy$.
13.332 \end{ttdescription}
13.333
13.334 +%FIXME move to sysman!
13.335 +%\section{Generating HTML documents}
13.336 +%\index{HTML|bold}
13.337 +%
13.338 +%Isabelle is able to make HTML documents that show a theory's
13.339 +%definition, the theorems proved in its ML file and the relationship
13.340 +%with its ancestors and descendants. HTML stands for Hypertext Markup
13.341 +%Language and is used in the World Wide Web to represent text
13.342 +%containing images and links to other documents. Web browsers like
13.343 +%{\tt xmosaic} or {\tt netscape} are used to view these documents.
13.344 +%
13.345 +%Besides the three HTML files that are made for every theory
13.346 +%(definition and theorems, ancestors, descendants), Isabelle stores
13.347 +%links to all theories in an index file. These indexes are themself
13.348 +%linked with other indexes to represent the hierarchic structure of
13.349 +%Isabelle's logics.
13.350 +%
13.351 +%To make HTML files for logics that are part of the Isabelle
13.352 +%distribution, simply set the shell environment variable {\tt
13.353 +%MAKE_HTML} before compiling a logic. This works for single logics as
13.354 +%well as for the shell script {\tt make-all} (see
13.355 +%\ref{sec:shell-scripts}). To make HTML files for {\tt FOL} using a
13.356 +%{\tt csh} style shell, the following commands can be used:
13.357 +%
13.358 +%\begin{ttbox}
13.359 +%cd FOL
13.360 +%setenv MAKE_HTML
13.361 +%make
13.362 +%\end{ttbox}
13.363 +%
13.364 +%The databases made this way do not differ from the ones made with an
13.365 +%unset {\tt MAKE_HTML}; in particular no HTML files are written if the
13.366 +%database is used to manually load a theory.
13.367 +%
13.368 +%As you will see below, the HTML generation is controlled by a boolean
13.369 +%reference variable. If you want to make databases which define this
13.370 +%variable's value as {\tt true} and where therefore HTML files are
13.371 +%written each time {\tt use_thy} is invoked, you have to set {\tt
13.372 +%MAKE_HTML} to ``{\tt true}'':
13.373 +%
13.374 +%\begin{ttbox}
13.375 +%cd FOL
13.376 +%setenv MAKE_HTML true
13.377 +%make
13.378 +%\end{ttbox}
13.379 +%
13.380 +%All theories loaded from within the {\tt FOL} database and all
13.381 +%databases derived from it will now cause HTML files to be written.
13.382 +%This behaviour can be changed by assigning a value of {\tt false} to
13.383 +%the boolean reference variable {\tt make_html}. Be careful when making
13.384 +%such databases publicly available since it means that your users will
13.385 +%generate HTML files though they might not intend to do so.
13.386 +%
13.387 +%As some of Isabelle's logics are based on others (e.g. {\tt ZF} on
13.388 +%{\tt FOL}) and because the HTML files list a theory's ancestors, you
13.389 +%should not make HTML files for a logic if the HTML files for the base
13.390 +%logic do not exist. Otherwise some of the hypertext links might point
13.391 +%to non-existing documents.
13.392 +%
13.393 +%The entry point to all logics is the {\tt index.html} file located in
13.394 +%Isabelle's main directory. You can also access a HTML version of the
13.395 +%distribution package at
13.396 +%
13.397 +%\begin{ttbox}
13.398 +%http://www4.informatik.tu-muenchen.de/~nipkow/isabelle/
13.399 +%\end{ttbox}
13.400 +%
13.401 +%
13.402 +%\subsection*{Manual HTML generation}
13.403 +%
13.404 +%To manually control the generation of HTML files the following
13.405 +%commands and reference variables are used:
13.406 +%
13.407 +%\begin{ttbox}
13.408 +%init_html : unit -> unit
13.409 +%make_html : bool ref
13.410 +%finish_html : unit -> unit
13.411 +%\end{ttbox}
13.412 +%
13.413 +%\begin{ttdescription}
13.414 +%\item[\ttindexbold{init_html}]
13.415 +%activates the HTML facility. It stores the current working directory
13.416 +%as the place where the {\tt index.html} file for all theories loaded
13.417 +%afterwards will be stored.
13.418 +%
13.419 +%\item[\ttindexbold{make_html}]
13.420 +%is a boolean reference variable read by {\tt use_thy} and other
13.421 +%functions to decide whether HTML files should be made. After you have
13.422 +%used {\tt init_html} you can manually change {\tt make_html}'s value
13.423 +%to temporarily disable HTML generation.
13.424 +%
13.425 +%\item[\ttindexbold{finish_html}]
13.426 +%has to be called after all theories have been read that should be
13.427 +%listed in the current {\tt index.html} file. It reads a temporary
13.428 +%file with information about the theories read since the last use of
13.429 +%{\tt init_html} and makes the {\tt index.html} file. If {\tt
13.430 +%make_html} is {\tt false} nothing is done.
13.431 +%
13.432 +%The indexes made by this function also contain a link to the {\tt
13.433 +%README} file if there exists one in the directory where the index is
13.434 +%stored. If there's a {\tt README.html} file it is used instead of
13.435 +%{\tt README}.
13.436 +%
13.437 +%\end{ttdescription}
13.438 +%
13.439 +%The above functions could be used in the following way:
13.440 +%
13.441 +%\begin{ttbox}
13.442 +%init_html();
13.443 +%{\out Setting path for index.html to "/home/clasohm/isabelle/HOL"}
13.444 +%use_thy "List";
13.445 +%\dots
13.446 +%finish_html();
13.447 +%\end{ttbox}
13.448 +%
13.449 +%Please note that HTML files are made only for those theories that are
13.450 +%read while {\tt make_html} is {\tt true}. These files may contain
13.451 +%links to theories that were read with a {\tt false} {\tt make_html}
13.452 +%and therefore point to non-existing files.
13.453 +%
13.454 +%
13.455 +%\subsection*{Extending or adding a logic}
13.456 +%
13.457 +%If you add a new subdirectory to Isabelle's logics (or add a completly
13.458 +%new logic), you would have to call {\tt init_html} at the start of every
13.459 +%directory's {\tt ROOT.ML} file and {\tt finish_html} at the end of
13.460 +%it. This is automatically done if you use
13.461 +%
13.462 +%\begin{ttbox}\index{use_dir}
13.463 +%use_dir : string -> unit
13.464 +%\end{ttbox}
13.465 +%
13.466 +%This function takes a path as its parameter, changes the working
13.467 +%directory, calls {\tt init_html} if {\tt make_html} is {\tt true},
13.468 +%executes {\tt ROOT.ML}, and calls {\tt finish_html}. The {\tt
13.469 +%index.html} file written in this directory will be automatically
13.470 +%linked to the first index found in the (recursively searched)
13.471 +%superdirectories.
13.472 +%
13.473 +%Instead of adding something like
13.474 +%
13.475 +%\begin{ttbox}
13.476 +%use"ex/ROOT.ML";
13.477 +%\end{ttbox}
13.478 +%
13.479 +%to the logic's makefile you have to use this:
13.480 +%
13.481 +%\begin{ttbox}
13.482 +%use_dir"ex";
13.483 +%\end{ttbox}
13.484 +%
13.485 +%Since {\tt use_dir} calls {\tt init_html} only if {\tt make_html} is
13.486 +%{\tt true} the generation of HTML files depends on the value this
13.487 +%reference variable has. It can either be inherited from the used \ML{}
13.488 +%database or set in the makefile before {\tt use_dir} is invoked,
13.489 +%e.g. to set it's value according to the environment variable {\tt
13.490 +%MAKE_HTML}.
13.491 +%
13.492 +%The generated HTML files contain all theorems that were proved in the
13.493 +%theory's \ML{} file with {\tt qed}, {\tt qed_goal} and {\tt qed_goalw},
13.494 +%or stored with {\tt bind_thm} and {\tt store_thm}. Additionally there
13.495 +%is a hypertext link to the whole \ML{} file.
13.496 +%
13.497 +%You can add section headings to the list of theorems by using
13.498 +%
13.499 +%\begin{ttbox}\index{use_dir}
13.500 +%section: string -> unit
13.501 +%\end{ttbox}
13.502 +%
13.503 +%in a theory's ML file, which converts a plain string to a HTML
13.504 +%heading and inserts it before the next theorem proved or stored with
13.505 +%one of the above functions. If {\tt make_html} is {\tt false} nothing
13.506 +%is done.
13.507 +%
13.508 +%
13.509 +%\subsection*{Using someone else's database}
13.510 +%
13.511 +%To make them independent from their storage place, the HTML files only
13.512 +%contain relative paths which are derived from absolute ones like the
13.513 +%current working directory, {\tt gif_path} or {\tt base_path}. The
13.514 +%latter two are reference variables which are initialized at the time
13.515 +%when the {\tt Pure} database is made. Because you need write access
13.516 +%for the current directory to make HTML files and therefore (probably)
13.517 +%generate them in your home directory, the absolute {\tt base_path} is
13.518 +%not correct if you use someone else's database or a database derived
13.519 +%from it.
13.520 +%
13.521 +%In that case you first should set {\tt base_path} to the value of {\em
13.522 +%your} Isabelle main directory, i.e. the directory that contains the
13.523 +%subdirectories where standard logics like {\tt FOL} and {\tt HOL} or
13.524 +%your own logics are stored. If you do not do this, the generated HTML
13.525 +%files will still be usable but may contain incomplete titles and lack
13.526 +%some hypertext links.
13.527 +%
13.528 +%It's also a good idea to set {\tt gif_path} which points to the
13.529 +%directory containing two GIF images used in the HTML
13.530 +%documents. Normally this is the {\tt Tools} subdirectory of Isabelle's
13.531 +%main directory. While its value in general is still valid, your HTML
13.532 +%files would depend on files not owned by you. This prevents you from
13.533 +%changing the location of the HTML files (as they contain relative
13.534 +%paths) and also causes trouble if the database's maker (re)moves the
13.535 +%GIFs.
13.536 +%
13.537 +%Here's what you should do before invoking {\tt init_html} using
13.538 +%someone else's \ML{} database:
13.539 +%
13.540 +%\begin{ttbox}
13.541 +%base_path := "/home/smith/isabelle";
13.542 +%gif_path := "/home/smith/isabelle/Tools";
13.543 +%init_html();
13.544 +%\dots
13.545 +%\end{ttbox}
13.546
13.547 -\section{Generating HTML documents}
13.548 -\index{HTML|bold}
13.549 -
13.550 -Isabelle is able to make HTML documents that show a theory's
13.551 -definition, the theorems proved in its ML file and the relationship
13.552 -with its ancestors and descendants. HTML stands for Hypertext Markup
13.553 -Language and is used in the World Wide Web to represent text
13.554 -containing images and links to other documents. Web browsers like
13.555 -{\tt xmosaic} or {\tt netscape} are used to view these documents.
13.556 -
13.557 -Besides the three HTML files that are made for every theory
13.558 -(definition and theorems, ancestors, descendants), Isabelle stores
13.559 -links to all theories in an index file. These indexes are themself
13.560 -linked with other indexes to represent the hierarchic structure of
13.561 -Isabelle's logics.
13.562 -
13.563 -To make HTML files for logics that are part of the Isabelle
13.564 -distribution, simply set the shell environment variable {\tt
13.565 -MAKE_HTML} before compiling a logic. This works for single logics as
13.566 -well as for the shell script {\tt make-all} (see
13.567 -\ref{sec:shell-scripts}). To make HTML files for {\tt FOL} using a
13.568 -{\tt csh} style shell, the following commands can be used:
13.569 -
13.570 -\begin{ttbox}
13.571 -cd FOL
13.572 -setenv MAKE_HTML
13.573 -make
13.574 -\end{ttbox}
13.575 -
13.576 -The databases made this way do not differ from the ones made with an
13.577 -unset {\tt MAKE_HTML}; in particular no HTML files are written if the
13.578 -database is used to manually load a theory.
13.579 -
13.580 -As you will see below, the HTML generation is controlled by a boolean
13.581 -reference variable. If you want to make databases which define this
13.582 -variable's value as {\tt true} and where therefore HTML files are
13.583 -written each time {\tt use_thy} is invoked, you have to set {\tt
13.584 -MAKE_HTML} to ``{\tt true}'':
13.585 -
13.586 -\begin{ttbox}
13.587 -cd FOL
13.588 -setenv MAKE_HTML true
13.589 -make
13.590 -\end{ttbox}
13.591 -
13.592 -All theories loaded from within the {\tt FOL} database and all
13.593 -databases derived from it will now cause HTML files to be written.
13.594 -This behaviour can be changed by assigning a value of {\tt false} to
13.595 -the boolean reference variable {\tt make_html}. Be careful when making
13.596 -such databases publicly available since it means that your users will
13.597 -generate HTML files though they might not intend to do so.
13.598 -
13.599 -As some of Isabelle's logics are based on others (e.g. {\tt ZF} on
13.600 -{\tt FOL}) and because the HTML files list a theory's ancestors, you
13.601 -should not make HTML files for a logic if the HTML files for the base
13.602 -logic do not exist. Otherwise some of the hypertext links might point
13.603 -to non-existing documents.
13.604 -
13.605 -The entry point to all logics is the {\tt index.html} file located in
13.606 -Isabelle's main directory. You can also access a HTML version of the
13.607 -distribution package at
13.608 -
13.609 -\begin{ttbox}
13.610 -http://www4.informatik.tu-muenchen.de/~nipkow/isabelle
13.611 -\end{ttbox}
13.612 -
13.613 -
13.614 -\subsection*{Manual HTML generation}
13.615 -
13.616 -To manually control the generation of HTML files the following
13.617 -commands and reference variables are used:
13.618 -
13.619 -\begin{ttbox}
13.620 -init_html : unit -> unit
13.621 -make_html : bool ref
13.622 -finish_html : unit -> unit
13.623 -\end{ttbox}
13.624 -
13.625 -\begin{ttdescription}
13.626 -\item[\ttindexbold{init_html}]
13.627 -activates the HTML facility. It stores the current working directory
13.628 -as the place where the {\tt index.html} file for all theories loaded
13.629 -afterwards will be stored.
13.630 -
13.631 -\item[\ttindexbold{make_html}]
13.632 -is a boolean reference variable read by {\tt use_thy} and other
13.633 -functions to decide whether HTML files should be made. After you have
13.634 -used {\tt init_html} you can manually change {\tt make_html}'s value
13.635 -to temporarily disable HTML generation.
13.636 -
13.637 -\item[\ttindexbold{finish_html}]
13.638 -has to be called after all theories have been read that should be
13.639 -listed in the current {\tt index.html} file. It reads a temporary
13.640 -file with information about the theories read since the last use of
13.641 -{\tt init_html} and makes the {\tt index.html} file. If {\tt
13.642 -make_html} is {\tt false} nothing is done.
13.643 -
13.644 -The indexes made by this function also contain a link to the {\tt
13.645 -README} file if there exists one in the directory where the index is
13.646 -stored. If there's a {\tt README.html} file it is used instead of
13.647 -{\tt README}.
13.648 -
13.649 -\end{ttdescription}
13.650 -
13.651 -The above functions could be used in the following way:
13.652 -
13.653 -\begin{ttbox}
13.654 -init_html();
13.655 -{\out Setting path for index.html to "/home/clasohm/isabelle/HOL"}
13.656 -use_thy "List";
13.657 -\dots
13.658 -finish_html();
13.659 -\end{ttbox}
13.660 -
13.661 -Please note that HTML files are made only for those theories that are
13.662 -read while {\tt make_html} is {\tt true}. These files may contain
13.663 -links to theories that were read with a {\tt false} {\tt make_html}
13.664 -and therefore point to non-existing files.
13.665 -
13.666 -
13.667 -\subsection*{Extending or adding a logic}
13.668 -
13.669 -If you add a new subdirectory to Isabelle's logics (or add a completly
13.670 -new logic), you would have to call {\tt init_html} at the start of every
13.671 -directory's {\tt ROOT.ML} file and {\tt finish_html} at the end of
13.672 -it. This is automatically done if you use
13.673 -
13.674 -\begin{ttbox}\index{use_dir}
13.675 -use_dir : string -> unit
13.676 -\end{ttbox}
13.677 -
13.678 -This function takes a path as its parameter, changes the working
13.679 -directory, calls {\tt init_html} if {\tt make_html} is {\tt true},
13.680 -executes {\tt ROOT.ML}, and calls {\tt finish_html}. The {\tt
13.681 -index.html} file written in this directory will be automatically
13.682 -linked to the first index found in the (recursively searched)
13.683 -superdirectories.
13.684 -
13.685 -Instead of adding something like
13.686 -
13.687 -\begin{ttbox}
13.688 -use"ex/ROOT.ML";
13.689 -\end{ttbox}
13.690 -
13.691 -to the logic's makefile you have to use this:
13.692 -
13.693 -\begin{ttbox}
13.694 -use_dir"ex";
13.695 -\end{ttbox}
13.696 -
13.697 -Since {\tt use_dir} calls {\tt init_html} only if {\tt make_html} is
13.698 -{\tt true} the generation of HTML files depends on the value this
13.699 -reference variable has. It can either be inherited from the used \ML{}
13.700 -database or set in the makefile before {\tt use_dir} is invoked,
13.701 -e.g. to set it's value according to the environment variable {\tt
13.702 -MAKE_HTML}.
13.703 -
13.704 -The generated HTML files contain all theorems that were proved in the
13.705 -theory's \ML{} file with {\tt qed}, {\tt qed_goal} and {\tt qed_goalw},
13.706 -or stored with {\tt bind_thm} and {\tt store_thm}. Additionally there
13.707 -is a hypertext link to the whole \ML{} file.
13.708 -
13.709 -You can add section headings to the list of theorems by using
13.710 -
13.711 -\begin{ttbox}\index{use_dir}
13.712 -section: string -> unit
13.713 -\end{ttbox}
13.714 -
13.715 -in a theory's ML file, which converts a plain string to a HTML
13.716 -heading and inserts it before the next theorem proved or stored with
13.717 -one of the above functions. If {\tt make_html} is {\tt false} nothing
13.718 -is done.
13.719 -
13.720 -
13.721 -\subsection*{Using someone else's database}
13.722 -
13.723 -To make them independent from their storage place, the HTML files only
13.724 -contain relative paths which are derived from absolute ones like the
13.725 -current working directory, {\tt gif_path} or {\tt base_path}. The
13.726 -latter two are reference variables which are initialized at the time
13.727 -when the {\tt Pure} database is made. Because you need write access
13.728 -for the current directory to make HTML files and therefore (probably)
13.729 -generate them in your home directory, the absolute {\tt base_path} is
13.730 -not correct if you use someone else's database or a database derived
13.731 -from it.
13.732 -
13.733 -In that case you first should set {\tt base_path} to the value of {\em
13.734 -your} Isabelle main directory, i.e. the directory that contains the
13.735 -subdirectories where standard logics like {\tt FOL} and {\tt HOL} or
13.736 -your own logics are stored. If you do not do this, the generated HTML
13.737 -files will still be usable but may contain incomplete titles and lack
13.738 -some hypertext links.
13.739 -
13.740 -It's also a good idea to set {\tt gif_path} which points to the
13.741 -directory containing two GIF images used in the HTML
13.742 -documents. Normally this is the {\tt Tools} subdirectory of Isabelle's
13.743 -main directory. While its value in general is still valid, your HTML
13.744 -files would depend on files not owned by you. This prevents you from
13.745 -changing the location of the HTML files (as they contain relative
13.746 -paths) and also causes trouble if the database's maker (re)moves the
13.747 -GIFs.
13.748 -
13.749 -Here's what you should do before invoking {\tt init_html} using
13.750 -someone else's \ML{} database:
13.751 -
13.752 -\begin{ttbox}
13.753 -base_path := "/home/smith/isabelle";
13.754 -gif_path := "/home/smith/isabelle/Tools";
13.755 -init_html();
13.756 -\dots
13.757 -\end{ttbox}
13.758
13.759 \section{Terms}
13.760 \index{terms|bold}
13.761 Terms belong to the \ML\ type \mltydx{term}, which is a concrete datatype
13.762 -with six constructors: there are six kinds of term.
13.763 +with six constructors:
13.764 \begin{ttbox}
13.765 type indexname = string * int;
13.766 infix 9 $;
13.767 @@ -844,7 +870,7 @@
13.768 read_cterm : Sign.sg -> string * typ -> cterm
13.769 cert_axm : Sign.sg -> string * term -> string * term
13.770 read_axm : Sign.sg -> string * string -> string * term
13.771 -rep_cterm : cterm -> \{T:typ, t:term, sign:Sign.sg, maxidx:int\}
13.772 +rep_cterm : cterm -> {\ttlbrace}T:typ, t:term, sign:Sign.sg, maxidx:int\ttrbrace
13.773 \end{ttbox}
13.774 \begin{ttdescription}
13.775 \item[\ttindexbold{cterm_of} $sign$ $t$] \index{signatures}
13.776 @@ -932,7 +958,7 @@
13.777 \subsection{Making and inspecting certified types}
13.778 \begin{ttbox}
13.779 ctyp_of : Sign.sg -> typ -> ctyp
13.780 -rep_ctyp : ctyp -> \{T: typ, sign: Sign.sg\}
13.781 +rep_ctyp : ctyp -> {\ttlbrace}T: typ, sign: Sign.sg\ttrbrace
13.782 \end{ttbox}
13.783 \begin{ttdescription}
13.784 \item[\ttindexbold{ctyp_of} $sign$ $T$] \index{signatures}
13.785 @@ -968,7 +994,7 @@
13.786
13.787 \item[\ttindexbold{set_oracle} $fn$ $thy$] sets the oracle of theory $thy$ to
13.788 be $fn$. It is seldom called explicitly, as there is syntax for oracles in
13.789 - theory files. A theory can have at most one oracle.
13.790 + theory files. Any theory node can have at most one oracle.
13.791 \end{ttdescription}
13.792
13.793 A curious feature of {\ML} exceptions is that they are ordinary constructors.
14.1 --- a/doc-src/Ref/theory-syntax.tex Mon May 05 21:18:01 1997 +0200
14.2 +++ b/doc-src/Ref/theory-syntax.tex Tue May 06 12:50:16 1997 +0200
14.3 @@ -4,45 +4,59 @@
14.4 \newlinechar=-1 %mathsing.sty sets \newlinechar=`\|, which would cause mayhem
14.5
14.6 \chapter{Syntax of Isabelle Theories}\label{app:TheorySyntax}
14.7 -Chapter~\ref{sec:ref-defining-theories} explains the meanings of these
14.8 -constructs. The syntax obeys the following conventions:
14.9 +
14.10 +Below we present the full syntax of theory definition files as
14.11 +provided by {\Pure} Isabelle --- object-logics may add their own
14.12 +sections. \S\ref{sec:ref-defining-theories} explains the meanings of
14.13 +these constructs. The syntax obeys the following conventions:
14.14 \begin{itemize}
14.15 \item {\tt Typewriter font} denotes terminal symbols.
14.16 -\item $id$, $tid$, $nat$, $string$ and $text$ are the lexical classes of
14.17 - identifiers, type identifiers, natural numbers, \ML\ strings (with their
14.18 - quotation marks, but without the need for \verb$\$ at the end of a line and
14.19 - the beginning of the next line) and arbitrary \ML\ text. The first three
14.20 - are fully defined in \iflabelundefined{Defining-Logics}%
14.21 - {{\it The Isabelle Reference Manual}, chapter `Defining Logics'}%
14.22 - {Chap.\ts\ref{Defining-Logics}}.
14.23 +
14.24 +\item $id$, $tid$, $nat$, $string$ and $longident$ are the lexical
14.25 + classes of identifiers, type identifiers, natural numbers, quoted
14.26 + strings (without the need for \verb$\$\dots\verb$\$ between lines)
14.27 + and long qualified \ML{} identifiers.
14.28 + The categories $id$, $tid$, $nat$ are fully defined in \iflabelundefined{Defining-Logics}%
14.29 + {{\it The Isabelle Reference Manual}, chapter `Defining Logics'}%
14.30 + {\S\ref{Defining-Logics}}.
14.31 +
14.32 +\item $text$ is all text from the current position to the end of file,
14.33 + $verbatim$ is any text enclosed in \verb.{|.\dots\verb.|}.
14.34 +
14.35 +\item Comments in theories take the form {\tt (*}\dots{\tt*)} and may
14.36 + be nested, just as in \ML.
14.37 \end{itemize}
14.38 -Comments in theories take the form {\tt (*} {\it text\/} {\tt*)}, where
14.39 -{\it text\/} should not contain the character sequence {\tt*)}.
14.40
14.41 \begin{rail}
14.42
14.43 -theoryDef : id '=' (name + '+') ('+' extension | ());
14.44 +theoryDef : id '=' (name + '+') ('+' extension | ())
14.45 + ;
14.46
14.47 -name: id | string;
14.48 +name: id | string
14.49 + ;
14.50
14.51 -extension : (section +) 'end' ( () | ml );
14.52 +extension : (section +) 'end' ( () | ml )
14.53 + ;
14.54
14.55 section : classes
14.56 | default
14.57 | types
14.58 | arities
14.59 | consts
14.60 - | constdefs
14.61 + | syntax
14.62 | trans
14.63 | defs
14.64 + | constdefs
14.65 | rules
14.66 + | axclass
14.67 + | instance
14.68 | oracle
14.69 ;
14.70
14.71 -classes : 'classes' ( ( id ( ()
14.72 - | '<' (id + ',')
14.73 - )
14.74 - ) + )
14.75 +classes : 'classes' ( classDecl + )
14.76 + ;
14.77 +
14.78 +classDecl : (id (() | '<' (id + ',')))
14.79 ;
14.80
14.81 default : 'default' sort
14.82 @@ -55,7 +69,8 @@
14.83 types : 'types' ( ( typeDecl ( () | '(' infix ')' ) ) + )
14.84 ;
14.85
14.86 -infix : ( 'infixr' | 'infixl' ) nat;
14.87 +infix : ( 'infixr' | 'infixl' ) nat
14.88 + ;
14.89
14.90 typeDecl : typevarlist name
14.91 ( () | '=' ( string | type ) );
14.92 @@ -66,30 +81,32 @@
14.93 '[' ( type + "," ) ']' '=>' type;
14.94
14.95 simpleType: id | ( tid ( () | '::' id ) ) |
14.96 - '(' ( type + "," ) ')' id | simpleType id;
14.97 + '(' ( type + "," ) ')' id | simpleType id
14.98 + ;
14.99
14.100 -
14.101 -arities : 'arities' ((( name + ',' ) '::' arity ) + )
14.102 +arities : 'arities' ((name + ',') '::' arity +)
14.103 ;
14.104
14.105 -arity : ( ()
14.106 - | '(' (sort + ',') ')'
14.107 - ) id
14.108 - ;
14.109 +arity : ( () | '(' (sort + ',') ')' ) sort
14.110 + ;
14.111
14.112 +consts : 'consts' ( mixfixConstDecl + )
14.113 + ;
14.114
14.115 -consts : 'consts' ( ( constDecl ( () | ( '(' mixfix ')' ) ) ) + )
14.116 - ;
14.117 +syntax : 'syntax' (() | mode) ( mixfixConstDecl + );
14.118 +
14.119 +mode : '(' name (() | 'output') ')'
14.120 + ;
14.121 +
14.122 +mixfixConstDecl : constDecl (() | ( '(' mixfix ')' ))
14.123 + ;
14.124
14.125 constDecl : ( name + ',') '::' (string | type);
14.126
14.127 mixfix : string ( () | ( () | ('[' (nat + ',') ']')) nat )
14.128 - | infix
14.129 + | ( 'infixr' | 'infixl' ) (() | string) nat
14.130 | 'binder' string nat ;
14.131
14.132 -constdefs : 'constdefs' (id '::' (string | type) string +)
14.133 - ;
14.134 -
14.135 trans : 'translations' ( pat ( '==' | '=>' | '<=' ) pat + )
14.136 ;
14.137
14.138 @@ -101,6 +118,18 @@
14.139 defs : 'defs' (( id string ) + )
14.140 ;
14.141
14.142 +constdefs : 'constdefs' (id '::' (string | type) string +)
14.143 + ;
14.144 +
14.145 +axclass : 'axclass' classDecl (() | ( id string ) +)
14.146 + ;
14.147 +
14.148 +instance : 'instance' ( name '<' name | name '::' arity) witness
14.149 + ;
14.150 +
14.151 +witness : (() | ((string | longident) + ',')) (() | verbatim)
14.152 + ;
14.153 +
14.154 oracle : 'oracle' name
14.155 ;
14.156
15.1 --- a/doc-src/Ref/thm.tex Mon May 05 21:18:01 1997 +0200
15.2 +++ b/doc-src/Ref/thm.tex Tue May 06 12:50:16 1997 +0200
15.3 @@ -2,15 +2,16 @@
15.4 \chapter{Theorems and Forward Proof}
15.5 \index{theorems|(}
15.6
15.7 -Theorems, which represent the axioms, theorems and rules of object-logics,
15.8 -have type \mltydx{thm}. This chapter begins by describing operations that
15.9 -print theorems and that join them in forward proof. Most theorem
15.10 -operations are intended for advanced applications, such as programming new
15.11 -proof procedures. Many of these operations refer to signatures, certified
15.12 -terms and certified types, which have the \ML{} types {\tt Sign.sg}, {\tt
15.13 - Sign.cterm} and {\tt Sign.ctyp} and are discussed in
15.14 -Chapter~\ref{theories}. Beginning users should ignore such complexities
15.15 ---- and skip all but the first section of this chapter.
15.16 +Theorems, which represent the axioms, theorems and rules of
15.17 +object-logics, have type \mltydx{thm}. This chapter begins by
15.18 +describing operations that print theorems and that join them in
15.19 +forward proof. Most theorem operations are intended for advanced
15.20 +applications, such as programming new proof procedures. Many of these
15.21 +operations refer to signatures, certified terms and certified types,
15.22 +which have the \ML{} types {\tt Sign.sg}, {\tt cterm} and {\tt ctyp}
15.23 +and are discussed in Chapter~\ref{theories}. Beginning users should
15.24 +ignore such complexities --- and skip all but the first section of
15.25 +this chapter.
15.26
15.27 The theorem operations do not print error messages. Instead, they raise
15.28 exception~\xdx{THM}\@. Use \ttindex{print_exn} to display
15.29 @@ -134,9 +135,9 @@
15.30 \subsection{Instantiating a theorem}
15.31 \index{instantiation}
15.32 \begin{ttbox}
15.33 -read_instantiate : (string*string)list -> thm -> thm
15.34 -read_instantiate_sg : Sign.sg -> (string*string)list -> thm -> thm
15.35 -cterm_instantiate : (Sign.cterm*Sign.cterm)list -> thm -> thm
15.36 +read_instantiate : (string * string) list -> thm -> thm
15.37 +read_instantiate_sg : Sign.sg -> (string * string) list -> thm -> thm
15.38 +cterm_instantiate : (cterm * cterm) list -> thm -> thm
15.39 \end{ttbox}
15.40 These meta-rules instantiate type and term unknowns in a theorem. They are
15.41 occasionally useful. They can prevent difficulties with higher-order
15.42 @@ -177,10 +178,11 @@
15.43 rule_by_tactic : tactic -> thm -> thm
15.44 \end{ttbox}
15.45 \begin{ttdescription}
15.46 -\item[\ttindexbold{standard} $thm$]
15.47 -puts $thm$ into the standard form of object-rules. It discharges all
15.48 -meta-assumptions, replaces free variables by schematic variables, and
15.49 -renames schematic variables to have subscript zero.
15.50 +\item[\ttindexbold{standard} $thm$] puts $thm$ into the standard form
15.51 + of object-rules. It discharges all meta-assumptions, replaces free
15.52 + variables by schematic variables, renames schematic variables to
15.53 + have subscript zero, also strips outer (meta) quantifiers and
15.54 + removes dangling sort hypotheses.
15.55
15.56 \item[\ttindexbold{zero_var_indexes} $thm$]
15.57 makes all schematic variables have subscript zero, renaming them to avoid
15.58 @@ -213,8 +215,8 @@
15.59 stamps_of_thy : thm -> string ref list
15.60 theory_of_thm : thm -> theory
15.61 dest_state : thm*int -> (term*term)list*term list*term*term
15.62 -rep_thm : thm -> \{prop: term, hyps: term list, der: deriv,
15.63 - maxidx: int, sign: Sign.sg, shyps: sort list\}
15.64 +rep_thm : thm -> {\ttlbrace}prop: term, hyps: term list, der: deriv,
15.65 + maxidx: int, sign: Sign.sg, shyps: sort list\ttrbrace
15.66 \end{ttbox}
15.67 \begin{ttdescription}
15.68 \item[\ttindexbold{concl_of} $thm$]
15.69 @@ -267,10 +269,11 @@
15.70 this may result in some sorts becoming {\em empty\/}: where one cannot exhibit
15.71 a type belonging to it because certain axioms are unsatisfiable.
15.72
15.73 -If a theorem contain a type variable whose sort is empty, then that theorem
15.74 -has no instances. In effect, it asserts nothing. But what if it is used to
15.75 -prove another theorem that no longer involves that sort? The latter theorem
15.76 -holds only if the sort is non-empty.
15.77 +If a theorem contains a type variable that is constrained by an empty
15.78 +sort, then that theorem has no instances. It is basically an instance
15.79 +of {\em ex falso quodlibet}. But what if it is used to prove another
15.80 +theorem that no longer involves that sort? The latter theorem holds
15.81 +only if under an additional non-emptiness assumption.
15.82
15.83 Therefore, Isabelle's theorems carry around sort hypotheses. The {\tt
15.84 shyps} field is a list of sorts occurring in type variables in the current
15.85 @@ -334,9 +337,11 @@
15.86 of the assumptions of the premises. Formally, the system works with
15.87 assertions of the form
15.88 \[ \phi \quad [\phi@1,\ldots,\phi@n], \]
15.89 -where $\phi@1$,~\ldots,~$\phi@n$ are the assumptions. Do not confuse
15.90 -meta-level assumptions with the object-level assumptions in a subgoal,
15.91 -which are represented in the meta-logic using~$\Imp$.
15.92 +where $\phi@1$,~\ldots,~$\phi@n$ are the assumptions. This can be
15.93 +also read as a single conclusion sequent $\phi@1,\ldots,\phi@n \vdash
15.94 +\phi$. Do not confuse meta-level assumptions with the object-level
15.95 +assumptions in a subgoal, which are represented in the meta-logic
15.96 +using~$\Imp$.
15.97
15.98 Each theorem has a signature. Certified terms have a signature. When a
15.99 rule takes several premises and certified terms, it merges the signatures
15.100 @@ -385,7 +390,7 @@
15.101 \subsection{Assumption rule}
15.102 \index{meta-assumptions}
15.103 \begin{ttbox}
15.104 -assume: Sign.cterm -> thm
15.105 +assume: cterm -> thm
15.106 \end{ttbox}
15.107 \begin{ttdescription}
15.108 \item[\ttindexbold{assume} $ct$]
15.109 @@ -397,8 +402,8 @@
15.110 \subsection{Implication rules}
15.111 \index{meta-implication}
15.112 \begin{ttbox}
15.113 -implies_intr : Sign.cterm -> thm -> thm
15.114 -implies_intr_list : Sign.cterm list -> thm -> thm
15.115 +implies_intr : cterm -> thm -> thm
15.116 +implies_intr_list : cterm list -> thm -> thm
15.117 implies_intr_hyps : thm -> thm
15.118 implies_elim : thm -> thm -> thm
15.119 implies_elim_list : thm -> thm list -> thm
15.120 @@ -450,7 +455,7 @@
15.121 \subsection{Equality rules}
15.122 \index{meta-equality}
15.123 \begin{ttbox}
15.124 -reflexive : Sign.cterm -> thm
15.125 +reflexive : cterm -> thm
15.126 symmetric : thm -> thm
15.127 transitive : thm -> thm -> thm
15.128 \end{ttbox}
15.129 @@ -469,9 +474,9 @@
15.130 \subsection{The $\lambda$-conversion rules}
15.131 \index{lambda calc@$\lambda$-calculus}
15.132 \begin{ttbox}
15.133 -beta_conversion : Sign.cterm -> thm
15.134 +beta_conversion : cterm -> thm
15.135 extensional : thm -> thm
15.136 -abstract_rule : string -> Sign.cterm -> thm -> thm
15.137 +abstract_rule : string -> cterm -> thm -> thm
15.138 combination : thm -> thm -> thm
15.139 \end{ttbox}
15.140 There is no rule for $\alpha$-conversion because Isabelle regards
15.141 @@ -503,9 +508,9 @@
15.142 \subsection{Forall introduction rules}
15.143 \index{meta-quantifiers}
15.144 \begin{ttbox}
15.145 -forall_intr : Sign.cterm -> thm -> thm
15.146 -forall_intr_list : Sign.cterm list -> thm -> thm
15.147 -forall_intr_frees : thm -> thm
15.148 +forall_intr : cterm -> thm -> thm
15.149 +forall_intr_list : cterm list -> thm -> thm
15.150 +forall_intr_frees : thm -> thm
15.151 \end{ttbox}
15.152
15.153 \begin{ttdescription}
15.154 @@ -526,10 +531,10 @@
15.155
15.156 \subsection{Forall elimination rules}
15.157 \begin{ttbox}
15.158 -forall_elim : Sign.cterm -> thm -> thm
15.159 -forall_elim_list : Sign.cterm list -> thm -> thm
15.160 -forall_elim_var : int -> thm -> thm
15.161 -forall_elim_vars : int -> thm -> thm
15.162 +forall_elim : cterm -> thm -> thm
15.163 +forall_elim_list : cterm list -> thm -> thm
15.164 +forall_elim_var : int -> thm -> thm
15.165 +forall_elim_vars : int -> thm -> thm
15.166 \end{ttbox}
15.167
15.168 \begin{ttdescription}
15.169 @@ -552,8 +557,7 @@
15.170 \subsection{Instantiation of unknowns}
15.171 \index{instantiation}
15.172 \begin{ttbox}
15.173 -instantiate: (indexname*Sign.ctyp)list *
15.174 - (Sign.cterm*Sign.cterm)list -> thm -> thm
15.175 +instantiate: (indexname * ctyp) list * (cterm * cterm) list -> thm -> thm
15.176 \end{ttbox}
15.177 \begin{ttdescription}
15.178 \item[\ttindexbold{instantiate} ($tyinsts$, $insts$) $thm$]
15.179 @@ -656,10 +660,10 @@
15.180
15.181 \subsection{Other meta-rules}
15.182 \begin{ttbox}
15.183 -trivial : Sign.cterm -> thm
15.184 +trivial : cterm -> thm
15.185 lift_rule : (thm * int) -> thm -> thm
15.186 rename_params_rule : string list * int -> thm -> thm
15.187 -rewrite_cterm : thm list -> Sign.cterm -> thm
15.188 +rewrite_cterm : thm list -> cterm -> thm
15.189 flexflex_rule : thm -> thm Sequence.seq
15.190 \end{ttbox}
15.191 \begin{ttdescription}
15.192 @@ -730,8 +734,7 @@
15.193 record:
15.194 \begin{ttbox}
15.195 #der (rep_thm conjI);
15.196 -{\out Join (Theorem ({ProtoPure, CPure, HOL},"conjI"),}
15.197 -{\out [Join (MinProof,[])]) : deriv}
15.198 +{\out Join (Theorem "conjI", [Join (MinProof,[])]) : deriv}
15.199 \end{ttbox}
15.200 This proof object identifies a labelled theorem, {\tt conjI}, whose underlying
15.201 proof has not been recorded; all we have is {\tt MinProof}.