summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | lcp |

Fri, 22 Apr 1994 18:18:37 +0200 | |

changeset 332 | 01b87a921967 |

parent 331 | 13660d5f6a77 |

child 333 | 2ca08f62df33 |

final Springer copy

--- a/doc-src/Ref/classical.tex Fri Apr 22 18:08:57 1994 +0200 +++ b/doc-src/Ref/classical.tex Fri Apr 22 18:18:37 1994 +0200 @@ -28,9 +28,10 @@ be traced, and their components can be called directly; in this manner, any proof can be viewed interactively. -The logics {\tt FOL}, {\tt HOL} and {\tt ZF} have the classical reasoner -already installed. We shall first consider how to use it, then see how to -instantiate it for new logics. +We shall first discuss the underlying principles, then consider how to use +the classical reasoner. Finally, we shall see how to instantiate it for +new logics. The logics {\tt FOL}, {\tt HOL} and {\tt ZF} have it already +installed. \section{The sequent calculus} @@ -136,7 +137,7 @@ simulates $({\disj}R)$: \[ (\neg Q\Imp P) \Imp P\disj Q \] The destruction rule $({\imp}E)$ is replaced by -\[ \List{P\imp Q;\; \neg P\imp R;\; Q\imp R} \Imp R. \] +\[ \List{P\imp Q;\; \neg P\Imp R;\; Q\Imp R} \Imp R. \] Quantifier replication also requires special rules. In classical logic, $\exists x{.}P$ is equivalent to $\neg\forall x{.}\neg P$; the rules $(\exists R)$ and $(\forall L)$ are dual: @@ -165,7 +166,7 @@ $$ \List{\forall x{.}P(x);\; \List{P(t); \forall x{.}P(x)}\Imp Q} \Imp Q. \eqno(\forall E@3) $$ To replicate existential quantifiers, replace $(\exists I)$ by -\[ \Bigl(\neg(\exists x{.}P(x)) \Imp P(t)\Bigr) \Imp \exists x{.}P(x). \] +\[ \List{\neg(\exists x{.}P(x)) \Imp P(t)} \Imp \exists x{.}P(x). \] All introduction rules mentioned above are also useful in swapped form. Replication makes the search space infinite; we must apply the rules with @@ -263,6 +264,25 @@ If installed, the classical module provides several tactics (and other operations) for simulating the classical sequent calculus. +\subsection{The automatic tactics} +\begin{ttbox} +fast_tac : claset -> int -> tactic +best_tac : claset -> int -> tactic +\end{ttbox} +Both of these tactics work by applying {\tt step_tac} repeatedly. Their +effect is restricted (by {\tt SELECT_GOAL}) to one subgoal; they either +solve this subgoal or fail. +\begin{ttdescription} +\item[\ttindexbold{fast_tac} $cs$ $i$] applies {\tt step_tac} using +depth-first search, to solve subgoal~$i$. + +\item[\ttindexbold{best_tac} $cs$ $i$] applies {\tt step_tac} using +best-first search, to solve subgoal~$i$. A heuristic function --- +typically, the total size of the proof state --- guides the search. This +function is supplied when the classical reasoner is set up. +\end{ttdescription} + + \subsection{Single-step tactics} \begin{ttbox} safe_step_tac : claset -> int -> tactic @@ -286,7 +306,7 @@ \item[\ttindexbold{inst_step_tac} $cs$ $i$] is like {\tt safe_step_tac}, but allows unknowns to be instantiated. -\item[\ttindexbold{step_tac} $cs$ $i$] tries {\tt safe_tac}. IF this +\item[\ttindexbold{step_tac} $cs$ $i$] tries {\tt safe_tac}. If this fails, it tries {\tt inst_step_tac}, or applies an unsafe rule from~$cs$. This is the basic step of the proof procedure. @@ -299,25 +319,6 @@ \end{ttdescription} -\subsection{The automatic tactics} -\begin{ttbox} -fast_tac : claset -> int -> tactic -best_tac : claset -> int -> tactic -\end{ttbox} -Both of these tactics work by applying {\tt step_tac} repeatedly. Their -effect is restricted (by {\tt SELECT_GOAL}) to one subgoal; they either -solve this subgoal or fail. -\begin{ttdescription} -\item[\ttindexbold{fast_tac} $cs$ $i$] applies {\tt step_tac} using -depth-first search, to solve subgoal~$i$. - -\item[\ttindexbold{best_tac} $cs$ $i$] applies {\tt step_tac} using -best-first search, to solve subgoal~$i$. A heuristic function --- -typically, the total size of the proof state --- guides the search. This -function is supplied when the classical reasoner is set up. -\end{ttdescription} - - \subsection{Other useful tactics} \index{tactics!for contradiction} \index{tactics!for Modus Ponens}

--- a/doc-src/Ref/defining.tex Fri Apr 22 18:08:57 1994 +0200 +++ b/doc-src/Ref/defining.tex Fri Apr 22 18:18:37 1994 +0200 @@ -117,7 +117,8 @@ \index{*PROP symbol} \index{*== symbol}\index{*=?= symbol}\index{*==> symbol} \index{*:: symbol}\index{*=> symbol} -%index command: percent is permitted, but braces must match! +\index{sort constraints} +%the index command: a percent is permitted, but braces must match! \index{%@{\tt\%} symbol} \index{{}@{\tt\ttlbrace} symbol}\index{{}@{\tt\ttrbrace} symbol} \index{*[ symbol}\index{*] symbol} @@ -164,6 +165,7 @@ treating {\tt y} like a type constructor applied to {\tt nat}. The likely result is an error message. To avoid this interpretation, use parentheses and write \verb|(x::nat) y|. + \index{type constraints}\index{*:: symbol} Similarly, \verb|x::nat y::nat| is parsed as \verb|x::(nat y::nat)| and yields an error. The correct form is \verb|(x::nat) (y::nat)|. @@ -295,7 +297,7 @@ {\out print_ast_translation: "==>" "_abs" "_idts" "fun"} \end{ttbox} -As you can see, the output is divided into labeled sections. The grammar +As you can see, the output is divided into labelled sections. The grammar is represented by {\tt lexicon}, {\tt roots} and {\tt prods}. The rest refers to syntactic translations and macro expansion. Here is an explanation of the various sections. @@ -378,7 +380,7 @@ first-order logic, type~$i$ stands for terms and~$o$ for formulae. Only the outermost type constructor is taken into account. For example, any type of the form $\sigma list$ stands for a list; productions may refer -to the symbol {\tt list} and will apply lists of any type. +to the symbol {\tt list} and will apply to lists of any type. The symbol associated with a type is called its {\bf root} since it may serve as the root of a parse tree. Precisely, the root of $(\tau@1, \dots, @@ -411,7 +413,7 @@ \begin{center} {\tt $c$ ::\ "$\sigma$" ("$template$" $ps$ $p$)} \end{center} -This constant declaration and mixfix annotation is interpreted as follows: +This constant declaration and mixfix annotation are interpreted as follows: \begin{itemize}\index{productions} \item The string {\tt $c$} is the name of the constant associated with the production; unless it is a valid identifier, it must be enclosed in @@ -488,7 +490,7 @@ end \end{ttbox} The {\tt arities} declaration causes {\tt exp} to be added as a new root. -If you put this into a file {\tt exp.thy} and load it via {\tt +If you put this into a file {\tt EXP.thy} and load it via {\tt use_thy "EXP"}, you can run some tests: \begin{ttbox} val read_exp = Syntax.test_read (syn_of EXP.thy) "exp"; @@ -607,6 +609,7 @@ "\(\Q\)"\hskip-3pt :: "[idts, \(\tau@2\)] => \(\tau@3\)" ("(3\(\Q\)_./ _)" \(p\)) \end{ttbox} Here \ndx{idts} is the nonterminal symbol for a list of identifiers with +\index{type constraints} optional type constraints (see Fig.\ts\ref{fig:pure_gram}). The declaration also installs a parse translation\index{translations!parse} for~$\Q$ and a print translation\index{translations!print} for~$c$ to @@ -657,7 +660,7 @@ end \end{ttbox} The constant \cdx{Trueprop} (the name is arbitrary) acts as an invisible -coercion function. Assuming this definition resides in a file {\tt base.thy}, +coercion function. Assuming this definition resides in a file {\tt Base.thy}, you have to load it with the command {\tt use_thy "Base"}. One of the simplest nontrivial logics is {\bf minimal logic} of @@ -673,7 +676,7 @@ MP "[| P --> Q; P |] ==> Q" end \end{ttbox} -After loading this definition from the file {\tt hilbert.thy}, you can +After loading this definition from the file {\tt Hilbert.thy}, you can start to prove theorems in the logic: \begin{ttbox} goal Hilbert.thy "P --> P";

--- a/doc-src/Ref/goals.tex Fri Apr 22 18:08:57 1994 +0200 +++ b/doc-src/Ref/goals.tex Fri Apr 22 18:18:37 1994 +0200 @@ -44,7 +44,7 @@ this list is non-empty, bind its value to an \ML{} identifier by typing something like \begin{ttbox} -val prems = it; +val prems = goal{\it theory\/ formula}; \end{ttbox}\index{assumptions!of main goal} These assumptions serve as the premises when you are deriving a rule. They are also stored internally and can be retrieved later by the function {\tt @@ -53,7 +53,7 @@ \index{definitions!unfolding} Some of the commands unfold definitions using meta-rewrite rules. This -expansion affects both the first subgoal and the premises, which would +expansion affects both the initial subgoal and the premises, which would otherwise require use of {\tt rewrite_goals_tac} and {\tt rewrite_rule}. @@ -321,8 +321,8 @@ \item[\ttindexbold{ren} {\it names} {\it i};] performs \hbox{\tt by (rename_tac {\it names} {\it i});} it renames -parameters in subgoal~$i$. (Ignore the message {\tt Warning:\ same as -previous level}.) +parameters in subgoal~$i$. (Ignore the message {\footnotesize\tt Warning:\ + same as previous level}.) \index{parameters!renaming} \end{ttdescription} @@ -341,9 +341,9 @@ are analogous to {\tt goal}, {\tt goalw} and {\tt goalw_cterm}. The tactic is specified by a function from theorem lists to tactic lists. -The function is applied to the list of meta-hypotheses taken from the main -goal. The resulting tactics are applied in sequence (using {\tt EVERY}). -For example, a proof consisting of the commands +The function is applied to the list of meta-assumptions taken from +the main goal. The resulting tactics are applied in sequence (using {\tt + EVERY}). For example, a proof consisting of the commands \begin{ttbox} val prems = goal {\it theory} {\it formula}; by \(tac@1\); \ldots by \(tac@n\); @@ -355,17 +355,10 @@ (fn prems=> [ \(tac@1\), \ldots, \(tac@n\) ]); \end{ttbox} The methods perform identical processing of the initial {\it formula} and -the final proof state, but {\tt prove_goal} executes the tactic as a -atomic operation, bypassing the subgoal module. - -A batch proof may alternatively consist of subgoal commands encapsulated -using~{\tt let}: -\begin{ttbox} -val my_thm = - let val prems = goal {\it theory} {\it formula} - in by \(tac@1\); \ldots by \(tac@n\); result() end; -\end{ttbox} - +the final proof state. But {\tt prove_goal} executes the tactic as a +atomic operation, bypassing the subgoal module; the current interactive +proof is unaffected. +% \begin{ttdescription} \item[\ttindexbold{prove_goal} {\it theory} {\it formula} {\it tacsf};] executes a proof of the {\it formula\/} in the given {\it theory}, using @@ -429,7 +422,7 @@ \item[\ttindexbold{pop_proof}();] discards the top element of the stack. It returns the list of -meta-hypotheses associated with the new proof; you should bind these to an +assumptions associated with the new proof; you should bind these to an \ML\ identifier. They can also be obtained by calling \ttindex{premises}. \item[\ttindexbold{rotate_proof}();]

--- a/doc-src/Ref/introduction.tex Fri Apr 22 18:08:57 1994 +0200 +++ b/doc-src/Ref/introduction.tex Fri Apr 22 18:18:37 1994 +0200 @@ -142,7 +142,7 @@ \begin{ttdescription} \item[\ttindexbold{show_hyps} := false;] -makes Isabelle show each meta-level hypotheses as a dot. +makes Isabelle show each meta-level hypothesis as a dot. \item[\ttindexbold{show_types} := true;] makes Isabelle show types when printing a term or theorem. @@ -160,7 +160,7 @@ The {\bf $\eta$-contraction law} asserts $(\lambda x.f(x))\equiv f$, provided $x$ is not free in ~$f$. It asserts {\bf extensionality} of functions: $f\equiv g$ if $f(x)\equiv g(x)$ for all~$x$. Higher-order -unification occasionally puts terms into a fully $\eta$-expanded form. For +unification frequently puts terms into a fully $\eta$-expanded form. For example, if $F$ has type $(\tau\To\tau)\To\tau$ then its expanded form is $\lambda h.F(\lambda x.h(x))$. By default, the user sees this expanded form.

--- a/doc-src/Ref/simplifier.tex Fri Apr 22 18:08:57 1994 +0200 +++ b/doc-src/Ref/simplifier.tex Fri Apr 22 18:18:37 1994 +0200 @@ -19,7 +19,8 @@ Experienced users can exploit the other components to streamline proofs. -\subsection{Rewrite rules}\index{rewrite rules} +\subsection{Rewrite rules} +\index{rewrite rules|(} Rewrite rules are theorems expressing some form of equality: \begin{eqnarray*} Suc(\Var{m}) + \Var{n} &=& \Var{m} + Suc(\Var{n}) \\ @@ -41,18 +42,22 @@ local assumptions. -\begin{warn}\index{rewrite rules} +\begin{warn} The left-hand side of a rewrite rule must look like a first-order term: - after eta-contraction, none of its unknowns should have arguments. Hence - ${\Var{i}+(\Var{j}+\Var{k})} = {(\Var{i}+\Var{j})+\Var{k}}$ and $\neg(\forall - x.\Var{P}(x)) \bimp (\exists x.\neg\Var{P}(x))$ are acceptable, whereas - $\Var{f}(\Var{x})\in {\tt range}(\Var{f}) = True$ is not. However, you can - replace the offending subterms by new variables and conditions: $\Var{y} = - \Var{f}(\Var{x}) \Imp \Var{y}\in {\tt range}(\Var{f}) = True$ is again - acceptable. + none of its unknowns should have arguments. Hence + ${\Var{i}+(\Var{j}+\Var{k})} = {(\Var{i}+\Var{j})+\Var{k}}$ is + acceptable. Even $\neg(\forall x.\Var{P}(x)) \bimp (\exists + x.\neg\Var{P}(x))$ is acceptable because its left-hand side is + $\neg(All(\Var{P}))$ after $\eta$-contraction. But ${\Var{f}(\Var{x})\in + {\tt range}(\Var{f})} = True$ is not acceptable. However, you can + replace the offending subterms by adding new variables and conditions: + $\Var{y} = \Var{f}(\Var{x}) \Imp \Var{y}\in {\tt range}(\Var{f}) = True$ + is acceptable as a conditional rewrite rule. \end{warn} -\subsection {Congruence rules}\index{congruence rules} +\index{rewrite rules|)} + +\subsection{*Congruence rules}\index{congruence rules} Congruence rules are meta-equalities of the form \[ \List{\dots} \Imp f(\Var{x@1},\ldots,\Var{x@n}) \equiv f(\Var{y@1},\ldots,\Var{y@n}). @@ -108,10 +113,11 @@ The subgoaler can be set explicitly with \ttindex{setsubgoaler}. For example, the subgoaler \begin{ttbox} -fun subgoal_tac ss = resolve_tac (prems_of_ss ss) ORELSE' +fun subgoal_tac ss = assume_tac ORELSE' + resolve_tac (prems_of_ss ss) ORELSE' asm_simp_tac ss; \end{ttbox} -tries to solve the subgoal with one of the premises and calls +tries to solve the subgoal by assumption or with one of the premises, calling simplification only if that fails; here {\tt prems_of_ss} extracts the current premises from a simpset. @@ -229,9 +235,10 @@ is like \verb$simp_tac$, but extracts additional rewrite rules from the assumptions. -\item[\ttindexbold{asm_full_simp_tac}] is like \verb$asm_simp_tac$, but also - simplifies the assumptions one by one, using each assumption in the - simplification of the following ones. +\item[\ttindexbold{asm_full_simp_tac}] + is like \verb$asm_simp_tac$, but also simplifies the assumptions one by + one. Working from left to right, it uses each assumption in the + simplification of those following. \end{ttdescription} Using the simplifier effectively may take a bit of experimentation. The tactics can be traced with the ML command \verb$trace_simp := true$. To @@ -253,7 +260,7 @@ \Var{P}(Suc(x))} \Imp \Var{P}(\Var{n})$. \item[FOL_ss] is a basic simpset for {\tt FOL}.% -\footnote{These examples reside on the file {\tt FOL/ex/nat.ML}.} +\footnote{These examples reside on the file {\tt FOL/ex/Nat.ML}.} \end{ttdescription} We create a simpset for natural numbers by extending~{\tt FOL_ss}: @@ -397,7 +404,7 @@ \end{ttbox} -\section{*Permutative rewrite rules} +\section{Permutative rewrite rules} \index{rewrite rules!permutative|(} A rewrite rule is {\bf permutative} if the left-hand side and right-hand @@ -455,7 +462,7 @@ sum_Suc "sum(f,Suc(n)) = f(n) + sum(f,n)" end \end{ttbox} -After declaring {\tt open Natsum}, we make the required simpset by adding +After declaring {\tt open NatSum}, we make the required simpset by adding the AC-rules for~$+$ and the axioms for~{\tt sum}: \begin{ttbox} val natsum_ss = arith_ss addsimps ([sum_0,sum_Suc] \at add_ac); @@ -564,7 +571,7 @@ Of course, you should only assert such rules if they are true for your particular logic. In Constructive Type Theory, equality is a ternary relation of the form $a=b\in A$; the type~$A$ determines the meaning of the -equality effectively as a partial equivalence relation. The present +equality essentially as a partial equivalence relation. The present simplifier cannot be used. Rewriting in {\tt CTT} uses another simplifier, which resides in the file {\tt typedsimp.ML} and is not documented. Even this does not work for later variants of Constructive Type Theory that use

--- a/doc-src/Ref/substitution.tex Fri Apr 22 18:08:57 1994 +0200 +++ b/doc-src/Ref/substitution.tex Fri Apr 22 18:18:37 1994 +0200 @@ -3,19 +3,18 @@ \index{tactics!substitution|(}\index{equality|(} Replacing equals by equals is a basic form of reasoning. Isabelle supports -several kinds of equality reasoning. {\bf Substitution} means to replace +several kinds of equality reasoning. {\bf Substitution} means replacing free occurrences of~$t$ by~$u$ in a subgoal. This is easily done, given an -equality $t=u$, provided the logic possesses the appropriate rule --- -unless you want to substitute even in the assumptions. The tactic -{\tt hyp_subst_tac} performs substitution in the assumptions, but it -works via object-level implication, and therefore must be specially set up -for each suitable object-logic. +equality $t=u$, provided the logic possesses the appropriate rule. The +tactic {\tt hyp_subst_tac} performs substitution even in the assumptions. +But it works via object-level implication, and therefore must be specially +set up for each suitable object-logic. Substitution should not be confused with object-level {\bf rewriting}. Given equalities of the form $t=u$, rewriting replaces instances of~$t$ by corresponding instances of~$u$, and continues until it reaches a normal form. Substitution handles `one-off' replacements by particular -equalities, while rewriting handles general equalities. +equalities while rewriting handles general equations. Chapter~\ref{simp-chap} discusses Isabelle's rewriting tactics. @@ -35,12 +34,12 @@ the first unifier includes all the occurrences.} To replace $u$ by~$t$ in subgoal~$i$, use \begin{ttbox} -resolve_tac [eqth RS subst] \(i\) {\it.} +resolve_tac [eqth RS subst] \(i\){\it.} \end{ttbox} To replace $t$ by~$u$ in subgoal~$i$, use \begin{ttbox} -resolve_tac [eqth RS ssubst] \(i\) {\it,} +resolve_tac [eqth RS ssubst] \(i\){\it,} \end{ttbox} where \tdxbold{ssubst} is the `swapped' substitution rule $$ \List{\Var{a}=\Var{b}; \Var{P}(\Var{b})} \Imp @@ -55,7 +54,7 @@ Elim-resolution is well-behaved with assumptions of the form $t=u$. To replace $u$ by~$t$ or $t$ by~$u$ in subgoal~$i$, use \begin{ttbox} -eresolve_tac [subst] \(i\) {\it or} eresolve_tac [ssubst] \(i\) {\it.} +eresolve_tac [subst] \(i\) {\rm or} eresolve_tac [ssubst] \(i\){\it.} \end{ttbox} @@ -93,7 +92,7 @@ contradict a theorem that states $0\not=1$, rather than to replace 0 by~1 in the subgoal! -Replacing a free variable causes similar problems if they appear in the +Substitution for free variables is also unhelpful if they appear in the premises of a rule being derived --- the substitution affects object-level assumptions, not meta-level assumptions. For instance, replacing~$a$ by~$b$ could make the premise~$P(a)$ worthless. To avoid this problem, use @@ -153,7 +152,7 @@ Here {\tt Trueprop} is the coercion from type~$o$ to type~$prop$, while \hbox{\tt op =} is the internal name of the infix operator~{\tt=}. Pattern-matching expresses the function concisely, using wildcards~({\tt_}) -to hide the types. +for the types. Here is how {\tt hyp_subst_tac} works. Given a subgoal of the form \[ \List{P@1; \cdots ; t=u; \cdots ; P@n} \Imp Q, \] it locates a suitable

--- a/doc-src/Ref/syntax.tex Fri Apr 22 18:08:57 1994 +0200 +++ b/doc-src/Ref/syntax.tex Fri Apr 22 18:18:37 1994 +0200 @@ -64,7 +64,7 @@ % Isabelle uses an S-expression syntax for abstract syntax trees. Constant atoms are shown as quoted strings, variable atoms as non-quoted strings and -applications as a parenthesized list of subtrees. For example, the \AST +applications as a parenthesised list of subtrees. For example, the \AST \begin{ttbox} Appl [Constant "_constrain", Appl [Constant "_abs", Variable "x", Variable "t"], @@ -270,11 +270,11 @@ \] \end{itemize} % -Type constraints are inserted to allow the printing of types. This is -governed by the boolean variable \ttindex{show_types}: +Type constraints\index{type constraints} are inserted to allow the printing +of types. This is governed by the boolean variable \ttindex{show_types}: \begin{itemize} \item $constrain(x, \tau) = x$ \ if $\tau = \mtt{dummyT}$ \index{*dummyT} or - \ttindex{show_types} not set to {\tt true}. + \ttindex{show_types} is set to {\tt false}. \item $constrain(x, \tau) = \Appl{\Constant \mtt{"_constrain"}, x, \astofterm{\tau}}$ \ otherwise. @@ -289,7 +289,7 @@ % The \AST{}, after application of macros (see \S\ref{sec:macros}), is transformed into the final output string. The built-in {\bf print AST - translations}\indexbold{translations!print AST} effectively reverse the + translations}\indexbold{translations!print AST} reverse the parse \AST{} translations of Fig.\ts\ref{fig:parse_ast_tr}. For the actual printing process, the names attached to productions @@ -338,11 +338,11 @@ Figure~\ref{fig:set_trans} defines a fragment of first-order logic and set theory.\footnote{This and the following theories are complete working examples, though they specify only syntax, no axioms. The file {\tt - ZF/zf.thy} presents the full set theory definition, including many + ZF/ZF.thy} presents the full set theory definition, including many macro rules.} Theory {\tt SET} defines constants for set comprehension ({\tt Collect}), replacement ({\tt Replace}) and bounded universal quantification ({\tt Ball}). Each of these binds some variables. Without -additional syntax we should have to express $\forall x \in A. P$ as {\tt +additional syntax we should have to write $\forall x \in A. P$ as {\tt Ball(A,\%x.P)}, and similarly for the others. \begin{figure} @@ -464,7 +464,7 @@ If \ttindex{eta_contract} is set to {\tt true}, terms will be $\eta$-contracted {\em before\/} the \AST{} rewriter sees them. Thus some abstraction nodes needed for print rules to match may vanish. For example, -\verb|Ball(A, %x. P(x))| contracts {\tt Ball(A, P)}; the print rule does +\verb|Ball(A, %x. P(x))| contracts to {\tt Ball(A, P)}; the print rule does not apply and the output will be {\tt Ball(A, P)}. This problem would not occur if \ML{} translation functions were used instead of macros (as is done for binder declarations). @@ -491,10 +491,10 @@ \subsection{Applying rules} As a term is being parsed or printed, an \AST{} is generated as an intermediate form (recall Fig.\ts\ref{fig:parse_print}). The \AST{} is -normalized by applying macro rules in the manner of a traditional term +normalised by applying macro rules in the manner of a traditional term rewriting system. We first examine how a single rule is applied. -Let $t$ be the abstract syntax tree to be normalized and $(l, r)$ some +Let $t$ be the abstract syntax tree to be normalised and $(l, r)$ some translation rule. A subtree~$u$ of $t$ is a {\bf redex} if it is an instance of~$l$; in this case $l$ is said to {\bf match}~$u$. A redex matched by $l$ may be replaced by the corresponding instance of~$r$, thus @@ -546,10 +546,10 @@ \end{ttbox} The term {\tt Nil} will be printed as {\tt []}, just as expected. The term \verb|%Nil.t| will be printed as \verb|%[].t|, which might not be -expected! +expected! How is the type~{\tt Nil} printed? Normalizing an \AST{} involves repeatedly applying macro rules until none -is applicable. Macro rules are chosen in the order that they appear in the +are applicable. Macro rules are chosen in the order that they appear in the {\tt translations} section. You can watch the normalization of \AST{}s during parsing and printing by setting \ttindex{Syntax.trace_norm_ast} to {\tt true}.\index{tracing!of macros} Alternatively, use @@ -626,7 +626,7 @@ The parse rules only work in the order given. \begin{warn} - The \AST{} rewriter cannot discern constants from variables and looks + The \AST{} rewriter cannot distinguish constants from variables and looks only for names of atoms. Thus the names of {\tt Constant}s occurring in the (internal) left-hand side of translation rules should be regarded as \rmindex{reserved words}. Choose non-identifiers like {\tt\at Finset} or @@ -635,7 +635,7 @@ \begin{ttbox} \%empty insert. insert(x, empty) \end{ttbox} - gets printed as \verb|%empty insert. {x}|. +\par\noindent is printed as \verb|%empty insert. {x}|. \end{warn} @@ -690,8 +690,8 @@ This section describes the translation function mechanism. By writing \ML{} functions, you can do almost everything with terms or \AST{}s during parsing and printing. The logic \LK\ is a good example of sophisticated -transformations between internal and external representations of -associative sequences; here, macros would be useless. +transformations between internal and external representations of sequents; +here, macros would be useless. A full understanding of translations requires some familiarity with Isabelle's internals, especially the datatypes {\tt term}, {\tt typ}, @@ -805,9 +805,10 @@ else list_comb (Const (r, dummyT) $ A $ B, ts) | dependent_tr' _ _ = raise Match; \end{ttbox} -The argument {\tt (q,r)} is supplied to {\tt dependent_tr'} by a curried -function application during its installation. We could set up print -translations for both {\tt Pi} and {\tt Sigma} by including +The argument {\tt (q,r)} is supplied to the curried function {\tt + dependent_tr'} by a partial application during its installation. We +can set up print translations for both {\tt Pi} and {\tt Sigma} by +including \begin{ttbox}\index{*ML section} val print_translation = [("Pi", dependent_tr' ("{\at}PROD", "{\at}->")), @@ -815,11 +816,11 @@ \end{ttbox} within the {\tt ML} section. The first of these transforms ${\tt Pi}(A, \mtt{Abs}(x, T, B))$ into $\hbox{\tt{\at}PROD}(x', A, B')$ or -$\hbox{\tt{\at}->}r(A, B)$, choosing the latter form if $B$ does not depend +$\hbox{\tt{\at}->}(A, B)$, choosing the latter form if $B$ does not depend on~$x$. It checks this using \ttindex{loose_bnos}, yet another function from {\tt Pure/term.ML}. Note that $x'$ is a version of $x$ renamed away -from all names in $B$, and $B'$ the body $B$ with {\tt Bound} nodes -referring to our {\tt Abs} node replaced by $\ttfct{Free} (x', +from all names in $B$, and $B'$ is the body $B$ with {\tt Bound} nodes +referring to the {\tt Abs} node replaced by $\ttfct{Free} (x', \mtt{dummyT})$. We must be careful with types here. While types of {\tt Const}s are

--- a/doc-src/Ref/tactic.tex Fri Apr 22 18:08:57 1994 +0200 +++ b/doc-src/Ref/tactic.tex Fri Apr 22 18:18:37 1994 +0200 @@ -109,19 +109,20 @@ \end{ttbox} These tactics are designed for applying rules such as substitution and induction, which cause difficulties for higher-order unification. The -tactics accept explicit instantiations for schematic variables in the rule ---- typically, in the rule's conclusion. Each instantiation is a pair -{\tt($v$,$e$)}, where $v$ can be a type variable or ordinary variable: +tactics accept explicit instantiations for unknowns in the rule --- +typically, in the rule's conclusion. Each instantiation is a pair +{\tt($v$,$e$)}, where $v$ is an unknown {\em without\/} its leading +question mark! \begin{itemize} -\item If $v$ is the {\bf type variable} {\tt'a}, then -the rule must contain a schematic type variable \verb$?'a$ of some +\item If $v$ is the type unknown {\tt'a}, then +the rule must contain a type unknown \verb$?'a$ of some sort~$s$, and $e$ should be a type of sort $s$. -\item If $v$ is the {\bf variable} {\tt P}, then -the rule must contain a schematic variable \verb$?P$ of some type~$\tau$, +\item If $v$ is the unknown {\tt P}, then +the rule must contain an unknown \verb$?P$ of some type~$\tau$, and $e$ should be a term of some type~$\sigma$ such that $\tau$ and $\sigma$ are unifiable. If the unification of $\tau$ and $\sigma$ -instantiates any schematic type variables in $\tau$, these instantiations +instantiates any type unknowns in $\tau$, these instantiations are recorded for application to the rule. \end{itemize} Types are instantiated before terms. Because type instantiations are @@ -142,7 +143,7 @@ instantiates the rule {\it thm} with the instantiations {\it insts}, as described above, and then performs resolution on subgoal~$i$. Resolution typically causes further instantiations; you need not give explicit -instantiations for every variable in the rule. +instantiations for every unknown in the rule. \item[\ttindexbold{eres_inst_tac}] is like {\tt res_inst_tac}, but performs elim-resolution. @@ -162,17 +163,17 @@ \index{tactics!meta-rewriting|bold}\index{meta-rewriting|bold} \index{definitions} -Definitions in Isabelle have the form $t\equiv u$, where typically $t$ is a +Definitions in Isabelle have the form $t\equiv u$, where $t$ is typically a constant or a constant applied to a list of variables, for example $\it sqr(n)\equiv n\times n$. (Conditional definitions, $\phi\Imp t\equiv u$, -are not supported.) {\bf Unfolding} the definition $t\equiv u$ means using +are not supported.) {\bf Unfolding} the definition ${t\equiv u}$ means using it as a rewrite rule, replacing~$t$ by~$u$ throughout a theorem. {\bf Folding} $t\equiv u$ means replacing~$u$ by~$t$. Rewriting continues until no rewrites are applicable to any subterm. There are rules for unfolding and folding definitions; Isabelle does not do this automatically. The corresponding tactics rewrite the proof state, -yielding a unique result. See also the {\tt goalw} command, which is the +yielding a single next state. See also the {\tt goalw} command, which is the easiest way of handling definitions. \begin{ttbox} rewrite_goals_tac : thm list -> tactic @@ -204,12 +205,12 @@ \index{tactics!resolution}\index{tactics!assumption} \index{tactics!meta-rewriting} \begin{ttbox} -rtac : thm -> int ->tactic -etac : thm -> int ->tactic -dtac : thm -> int ->tactic -atac : int ->tactic +rtac : thm -> int -> tactic +etac : thm -> int -> tactic +dtac : thm -> int -> tactic +atac : int -> tactic ares_tac : thm list -> int -> tactic -rewtac : thm -> tactic +rewtac : thm -> tactic \end{ttbox} These abbreviate common uses of tactics. \begin{ttdescription} @@ -224,7 +225,7 @@ destruct-resolution. \item[\ttindexbold{atac} {\it i}] -is a synonym for \hbox{\tt assume_tac {\it i}}, doing proof by assumption. +abbreviates \hbox{\tt assume_tac {\it i}}, doing proof by assumption. \item[\ttindexbold{ares_tac} {\it thms} {\it i}] tries proof by assumption and resolution; it abbreviates @@ -244,8 +245,7 @@ cut_inst_tac : (string*string)list -> thm -> int -> tactic subgoal_tac : string -> int -> tactic \end{ttbox} -These tactics add assumptions --- which must be proved, sooner or later --- -to a given subgoal. +These tactics add assumptions to a given subgoal. \begin{ttdescription} \item[\ttindexbold{cut_facts_tac} {\it thms} {\it i}] adds the {\it thms} as new assumptions to subgoal~$i$. Once they have @@ -367,7 +367,7 @@ \begin{ttbox} compose_tac: (bool * thm * int) -> int -> tactic \end{ttbox} -{\bf Composing} two rules means to resolve them without prior lifting or +{\bf Composing} two rules means resolving them without prior lifting or renaming of unknowns. This low-level operation, which underlies the resolution tactics, may occasionally be useful for special effects. A typical application is \ttindex{res_inst_tac}, which lifts and instantiates a @@ -422,7 +422,7 @@ \item[\ttindexbold{lessb} ({\it brl1},{\it brl2})] returns the result of \begin{ttbox} -subgoals_of_brl {\it brl1} < subgoals_of_brl {\it brl2} +subgoals_of_brl{\it brl1} < subgoals_of_brl{\it brl2} \end{ttbox} \end{ttdescription} Note that \hbox{\tt sort lessb {\it brls}} sorts a list of $\it @@ -463,7 +463,7 @@ several functions for `compiling' long lists of rules into fast resolution tactics. When supplied with a list of theorems, these functions build a discrimination net; the net is used when the tactic is applied to a -goal. To avoid repreatedly constructing the nets, use currying: bind the +goal. To avoid repeatedly constructing the nets, use currying: bind the resulting tactics to \ML{} identifiers. \begin{ttdescription} @@ -562,15 +562,15 @@ pause_tac: tactic print_tac: tactic \end{ttbox} -These violate the functional behaviour of tactics by printing information -when they are applied to a proof state. Their output may be difficult to -interpret. Note that certain of the searching tacticals, such as {\tt -REPEAT}, have built-in tracing options. +These tactics print tracing information when they are applied to a proof +state. Their output may be difficult to interpret. Note that certain of +the searching tacticals, such as {\tt REPEAT}, have built-in tracing +options. \begin{ttdescription} \item[\ttindexbold{pause_tac}] -prints {\tt** Press RETURN to continue:} and then reads a line from the -terminal. If this line is blank then it returns the proof state unchanged; -otherwise it fails (which may terminate a repetition). +prints {\footnotesize\tt** Press RETURN to continue:} and then reads a line +from the terminal. If this line is blank then it returns the proof state +unchanged; otherwise it fails (which may terminate a repetition). \item[\ttindexbold{print_tac}] returns the proof state unchanged, with the side effect of printing it at @@ -612,7 +612,7 @@ \item[Sequence.pull $s$] returns {\tt None} if the sequence is empty and {\tt Some($x$,$s'$)} if the sequence has head~$x$ and tail~$s'$. Warning: calling \hbox{Sequence.pull -$s$} again will {\bf recompute} the value of~$x$; it is not stored! +$s$} again will {\it recompute\/} the value of~$x$; it is not stored! \end{ttdescription} @@ -623,7 +623,7 @@ s_of_list : 'a list -> 'a seq \end{ttbox} \begin{ttdescription} -\item[Sequence.chop ($n$, $s$)] +\item[Sequence.chop($n$,$s$)] returns the first~$n$ elements of~$s$ as a list, paired with the remaining elements of~$s$. If $s$ has fewer than~$n$ elements, then so will the list. @@ -645,10 +645,10 @@ filters : ('a -> bool) -> 'a seq -> 'a seq \end{ttbox} \begin{ttdescription} -\item[Sequence.append ($s@1$, $s@2$)] +\item[Sequence.append($s@1$,$s@2$)] concatenates $s@1$ to $s@2$. -\item[Sequence.interleave ($s@1$, $s@2$)] +\item[Sequence.interleave($s@1$,$s@2$)] joins $s@1$ with $s@2$ by interleaving their elements. The result contains all the elements of the sequences, even if both are infinite.

--- a/doc-src/Ref/tctical.tex Fri Apr 22 18:08:57 1994 +0200 +++ b/doc-src/Ref/tctical.tex Fri Apr 22 18:18:37 1994 +0200 @@ -139,7 +139,7 @@ Note {\tt REPEAT}'s explicit abstraction over the proof state. Recursive tacticals must be coded in this awkward fashion to avoid infinite recursion. With the following definition, \hbox{\tt REPEAT $tac$} would -loop: +loop due to \ML's eager evaluation strategy: \begin{ttbox} fun REPEAT tac = (tac THEN REPEAT tac) ORELSE all_tac; \end{ttbox} @@ -185,8 +185,8 @@ \index{tracing!of searching tacticals} \begin{ttbox} DEPTH_FIRST : (thm->bool) -> tactic -> tactic -DEPTH_SOLVE : tactic -> tactic -DEPTH_SOLVE_1 : tactic -> tactic +DEPTH_SOLVE : tactic -> tactic +DEPTH_SOLVE_1 : tactic -> tactic trace_DEPTH_FIRST: bool ref \hfill{\bf initially false} \end{ttbox} \begin{ttdescription} @@ -213,7 +213,7 @@ \index{tacticals!searching} \index{tracing!of searching tacticals} \begin{ttbox} -BREADTH_FIRST : (thm->bool) -> tactic -> tactic +BREADTH_FIRST : (thm->bool) -> tactic -> tactic BEST_FIRST : (thm->bool)*(thm->int) -> tactic -> tactic THEN_BEST_FIRST : tactic * ((thm->bool) * (thm->int) * tactic) -> tactic \hfill{\bf infix 1} @@ -330,11 +330,11 @@ \hbox{\tt SELECT_GOAL {\it tac} $i$}. {\tt SELECT_GOAL} works by creating a state of the form $\phi\Imp\phi$, -with the one subgoal~$\phi$. If subgoal~$i$ has the form then -$(\psi\Imp\theta)\Imp(\psi\Imp\theta)$ is in fact $\List{\psi\Imp\theta;\; - \psi}\Imp\theta$, a proof state with two subgoals. Such a proof state -might cause tactics to go astray. Therefore {\tt SELECT_GOAL} inserts a -quantifier to create the state +with the one subgoal~$\phi$. If subgoal~$i$ has the form $\psi\Imp\theta$ +then $(\psi\Imp\theta)\Imp(\psi\Imp\theta)$ is in fact +$\List{\psi\Imp\theta;\; \psi}\Imp\theta$, a proof state with two subgoals. +Such a proof state might cause tactics to go astray. Therefore {\tt + SELECT_GOAL} inserts a quantifier to create the state \[ (\Forall x.\psi\Imp\theta)\Imp(\Forall x.\psi\Imp\theta). \] \item[\ttindexbold{METAHYPS} {\it tacf} $i$]\index{meta-assumptions} @@ -362,6 +362,8 @@ \begin{ttbox} val hyp_res_tac = METAHYPS (fn prems => resolve_tac prems 1); \end{ttbox} +The function \ttindex{gethyps} is useful for debugging applications of {\tt + METAHYPS}. \end{ttdescription} \begin{warn}

--- a/doc-src/Ref/theories.tex Fri Apr 22 18:08:57 1994 +0200 +++ b/doc-src/Ref/theories.tex Fri Apr 22 18:18:37 1994 +0200 @@ -10,8 +10,8 @@ returning a message and a list of theories. Signatures, which contain information about sorts, types, constants and -syntax, have the \ML\ type~\mltydx{Sign.sg}. For identification, -each signature carries a unique list of {\bf stamps}, which are \ML\ +syntax, have the \ML\ type~\mltydx{Sign.sg}. For identification, each +signature carries a unique list of \bfindex{stamps}, which are \ML\ references to strings. The strings serve as human-readable names; the references serve as unique identifiers. Each primitive signature has a single stamp. When two signatures are merged, their lists of stamps are @@ -68,7 +68,7 @@ Only 2-place type constructors can have infix status and symbolic names; an example is {\tt ('a,'b)"*"}, which expresses binary product types. - A {\bf type synonym}\indexbold{types!synonyms} is an abbreviation + A {\bf type synonym}\indexbold{type synonyms} is an abbreviation $(\alpha@1,\dots,\alpha@n)name = \mbox{\tt"}\tau\mbox{\tt"}$, where $name$ can be a string and $\tau$ must be enclosed in quotation marks. @@ -177,41 +177,37 @@ \end{ttdescription} % Each theory definition must reside in a separate file. Let the file {\it - tf}{\tt.thy} contain the definition of a theory called $TF$ with parent -theories $TB@1$ \dots $TB@n$. Calling \ttindexbold{use_thy}~{\tt"}{\it - TF\/}{\tt"} reads file {\it tf}{\tt.thy}, writes a temporary \ML{} -file {\tt.}{\it tf}{\tt.thy.ML}, and reads the latter file. Recursive {\tt + T}{\tt.thy} contain the definition of a theory called~$T$, whose parent +theories are $TB@1$ \dots $TB@n$. Calling \ttindexbold{use_thy}~{\tt"{\it + T\/}"} reads the file {\it T}{\tt.thy}, writes a temporary \ML{} +file {\tt.{\it T}.thy.ML}, and reads the latter file. Recursive {\tt use_thy} calls load those parent theories that have not been loaded -previously; the recursion may continue to any depth. One {\tt use_thy} -call can read an entire logic if all theories are linked appropriately. - -The result is an \ML\ structure~$TF$ containing a component {\tt thy} for -the new theory and components $r@1$ \dots $r@n$ for the rules. The -structure also contains the definitions of the {\tt ML} section, if -present. The file {\tt.}{\it tf}{\tt.thy.ML} is then deleted if -{\tt delete_tmpfiles} is set to {\tt true} and no errors occurred. +previously; the recursive calls may continue to any depth. One {\tt use_thy} +call can read an entire logic provided all theories are linked appropriately. -Finally the file {\it tf}{\tt.ML} is read, if it exists. This file -normally contains proofs involving the new theory. It is also possible to -provide only a {\tt.ML} file, with no {\tt.thy} file. In this case the -{\tt.ML} file must declare an \ML\ structure having the theory's name. If -both the {\tt.thy} file and a structure declaration in the {\tt.ML} file -exist, then the latter declaration is used. See {\tt ZF/ex/llist.ML} for -an example. +The result is an \ML\ structure~$T$ containing a component {\tt thy} for +the new theory and components for each of the rules. The structure also +contains the definitions of the {\tt ML} section, if present. The file +{\tt.{\it T}.thy.ML} is then deleted if {\tt delete_tmpfiles} is set +to {\tt true} and no errors occurred. -\indexbold{theories!names of}\indexbold{files!names of} -\begin{warn} - Case is significant. The argument of \ttindex{use_thy} should be the - exact theory name, as defined in the theory file. The corresponding - filenames are derived by appending {\tt.thy} or {\tt.ML} to the theory's - name {\it after conversion to lower case}. -\end{warn} +Finally the file {\it T}{\tt.ML} is read, if it exists. This file normally +begins with the declaration {\tt open~$T$} and contains proofs involving +the new theory. + +Special applications, such as \ZF's inductive definition package, construct +theories directly by calling the \ML{} function {\tt extend_theory}. In +this situation there is no {\tt.thy} file, only an {\tt.ML} file. The +{\tt.ML} file must declare an \ML\ structure having the theory's name. See +the file {\tt ZF/ex/LList.ML} for an example. +Section~\ref{sec:pseudo-theories} below describes a way of linking such +theories to their parents. \begin{warn} - Temporary files are written to the current directory, which therefore - must be writable. Isabelle inherits the current directory from the - operating system; you can change it within Isabelle by typing - \hbox{\tt\ \ \ttindex{cd} "{\it dir}";\ \ }. +Temporary files are written to the current directory, which therefore must +be writable. Isabelle inherits the current directory from the operating +system; you can change it within Isabelle by typing \hbox{\tt\ \ + \ttindex{cd} "{\it dir}";\ \ }. \end{warn} @@ -221,6 +217,11 @@ update : unit -> unit unlink_thy : string -> unit \end{ttbox} +Changing a theory on disk often makes it necessary to reload all theories +descended from it. However, {\tt use_thy} reads only one theory, even if +some of the parent theories are out of date. In this case you should call +{\tt update()}. + Isabelle keeps track of all loaded theories and their files. If \ttindex{use_thy} finds that the theory to be loaded has been read before, it determines whether to reload the theory as follows. First it looks for @@ -229,15 +230,9 @@ are equal. If the files have been moved, {\tt use_thy} searches for them as it would for a new theory. After {\tt use_thy} reloads a theory, it marks the children as out-of-date. -\begin{warn} - Changing a theory on disk often makes it necessary to reload all theories - descended from it. However, {\tt use_thy} reads only one theory, even if - some of the parent theories are out of date. In this case you should - call {\tt update()}. -\end{warn} \begin{ttdescription} -\item[\ttindexbold{update} ()] +\item[\ttindexbold{update}()] reloads all modified theories and their descendants in the correct order. \item[\ttindexbold{unlink_thy} $thyname$]\indexbold{theories!removing} @@ -247,6 +242,7 @@ \end{ttdescription} +\goodbreak \subsection{Important note for Poly/ML users}\index{Poly/{\ML} compiler} The theory mechanism depends upon reference variables. At the end of a Poly/\ML{} session, the contents of references are lost unless they are @@ -266,13 +262,17 @@ has no loaded theories, since they allocate new references. -\subsection{*Pseudo theories}\indexbold{theories!pseudo} +\subsection{*Pseudo theories}\label{sec:pseudo-theories} +\indexbold{theories!pseudo}% Any automatic reloading facility requires complete knowledge of all dependencies. Sometimes theories depend on objects created in \ML{} files -with no associated {\tt.thy} file. Unless such dependencies are documented, -{\tt update} fails to reload these \ML{} files and the system is left in a -state where some objects, such as theorems, still refer to old versions of -theories. This may lead to the error +with no associated {\tt.thy} file. These objects may be theories but they +could also be theorems, proof procedures, etc. + +Unless such dependencies are documented, {\tt update} fails to reload these +\ML{} files and the system is left in a state where some objects, such as +theorems, still refer to old versions of theories. This may lead to the +error \begin{ttbox} Attempt to merge different versions of theory: \(T\) \end{ttbox} @@ -280,8 +280,8 @@ those without associated {\tt.thy} file. Let us assume we have an orphaned \ML{} file named {\tt orphan.ML} and a -theory~$B$ that depends on {\tt orphan.ML} --- for example, {\tt b.ML} uses -theorems proved in {\tt orphan.ML}. Then {\tt b.thy} should +theory~$B$ that depends on {\tt orphan.ML} --- for example, {\tt B.ML} uses +theorems proved in {\tt orphan.ML}. Then {\tt B.thy} should mention this dependence by means of a string: \begin{ttbox} B = ... + "orphan" + ... @@ -327,17 +327,17 @@ complains about additional assumptions, but \ttindex{uresult} does not. For example, if {\it formula} is -\hbox{\tt a=b ==> b=a} then the resulting theorem might have the form -\hbox{\tt\frenchspacing ?a=?b ==> ?b=?a [!!a b. a=b ==> b=a]} +\hbox{\tt a=b ==> b=a} then the resulting theorem has the form +\hbox{\verb'?a=?b ==> ?b=?a [!!a b. a=b ==> b=a]'} \end{ttdescription} \subsection{Building a theory} \label{BuildingATheory} \index{theories!constructing|bold} \begin{ttbox} -pure_thy: theory -merge_theories: theory * theory -> theory -extend_theory: theory -> string -> \(\cdots\) -> theory +pure_thy : theory +merge_theories : theory * theory -> theory +extend_theory : theory -> string -> \(\cdots\) -> theory \end{ttbox} \begin{ttdescription} \item[\ttindexbold{pure_thy}] contains just the types, constants, and syntax @@ -414,7 +414,7 @@ \hbox{\tt extend_theory $thy$} or \hbox{\tt merge_theories ($thy@1$, $thy@2$)}. \item[\ttindexbold{stamps_of_thy} $thy$]\index{signatures} -returns the stamps of the signature associated with~$thy$. +returns the \rmindex{stamps} of the signature associated with~$thy$. \item[\ttindexbold{sign_of} $thy$] returns the signature associated with~$thy$. It is useful with functions @@ -470,7 +470,7 @@ is the {\bf application} of~$t$ to~$u$. \end{ttdescription} Application is written as an infix operator to aid readability. -Here is an \ML\ pattern to recognize first-order formulae of +Here is an \ML\ pattern to recognize \FOL{} formulae of the form~$A\imp B$, binding the subformulae to~$A$ and~$B$: \begin{ttbox} Const("Trueprop",_) $ (Const("op -->",_) $ A $ B) @@ -496,7 +496,7 @@ the number 0. A well-formed term does not contain any loose variables. \item[\ttindexbold{incr_boundvars} $j$] - increases a term's dangling bound variables by the offset~$j$. This + increases a term's dangling bound variables by the offset~$j$. This is required when moving a subterm into a context where it is enclosed by a different number of abstractions. Bound variables with a matching abstraction are unaffected. @@ -510,7 +510,7 @@ substitutes into $u$, which should be the body of an abstraction. It replaces each occurrence of the outermost bound variable by a free variable. The free variable has type~$T$ and its name is a variant - of~$a$ choosen to be distinct from all constants and from all variables + of~$a$ chosen to be distinct from all constants and from all variables free in~$u$. \item[$t$ \ttindexbold{aconv} $u$]

--- a/doc-src/Ref/thm.tex Fri Apr 22 18:08:57 1994 +0200 +++ b/doc-src/Ref/thm.tex Fri Apr 22 18:18:37 1994 +0200 @@ -92,7 +92,7 @@ conclusion of $thm@1$ with the first premise of~$thm@2$. \item[\tt {$[thm@1,\ldots,thm@n]$} MRS $thm$] \indexbold{*MRS} - uses {\tt RLN} to resolve $thm@i$ against premise~$i$ of $thm$, for + uses {\tt RSN} to resolve $thm@i$ against premise~$i$ of $thm$, for $i=n$, \ldots,~1. This applies $thm@n$, \ldots, $thm@1$ to the first $n$ premises of $thm$. Because the theorems are used from right to left, it does not matter if the $thm@i$ create new premises. {\tt MRS} is useful @@ -169,15 +169,15 @@ \subsection{Miscellaneous forward rules} \index{theorems!standardizing} \begin{ttbox} -standard : thm -> thm -zero_var_indexes : thm -> thm -make_elim : thm -> thm +standard : thm -> thm +zero_var_indexes : thm -> thm +make_elim : thm -> thm rule_by_tactic : tactic -> thm -> thm \end{ttbox} \begin{ttdescription} \item[\ttindexbold{standard} $thm$] puts $thm$ into the standard form of object-rules. It discharges all -meta-hypotheses, replaces free variables by schematic variables, and +meta-assumptions, replaces free variables by schematic variables, and renames schematic variables to have subscript zero. \item[\ttindexbold{zero_var_indexes} $thm$] @@ -228,7 +228,7 @@ returns the flex-flex constraints of $thm$. \item[\ttindexbold{stamps_of_thm} $thm$] -returns the stamps of the signature associated with~$thm$. +returns the \rmindex{stamps} of the signature associated with~$thm$. \item[\ttindexbold{dest_state} $(thm,i)$] decomposes $thm$ as a tuple containing a list of flex-flex constraints, a @@ -237,7 +237,7 @@ \item[\ttindexbold{rep_thm} $thm$] decomposes $thm$ as a record containing the statement of~$thm$, its list of -meta-hypotheses, the maximum subscript of its unknowns, and its signature. +meta-assumptions, the maximum subscript of its unknowns, and its signature. \end{ttdescription} @@ -284,12 +284,12 @@ \index{meta-assumptions} The meta-logic uses natural deduction. Each theorem may depend on -meta-hypotheses, or assumptions. Certain rules, such as $({\Imp}I)$, +meta-level assumptions. Certain rules, such as $({\Imp}I)$, discharge assumptions; in most other rules, the conclusion depends on all of the assumptions of the premises. Formally, the system works with assertions of the form \[ \phi \quad [\phi@1,\ldots,\phi@n], \] -where $\phi@1$,~\ldots,~$\phi@n$ are the hypotheses. Do not confuse +where $\phi@1$,~\ldots,~$\phi@n$ are the assumptions. Do not confuse meta-level assumptions with the object-level assumptions in a subgoal, which are represented in the meta-logic using~$\Imp$. @@ -299,7 +299,7 @@ incompatible. \index{meta-implication} -The {\em implication\/} rules are $({\Imp}I)$ +The {\bf implication} rules are $({\Imp}I)$ and $({\Imp}E)$: \[ \infer[({\Imp}I)]{\phi\Imp \psi}{\infer*{\psi}{[\phi]}} \qquad \infer[({\Imp}E)]{\psi}{\phi\Imp \psi & \phi} \] @@ -311,7 +311,7 @@ \qquad \infer[({\equiv}E)]{\psi}{\phi\equiv \psi & \phi} \] -The {\em equality\/} rules are reflexivity, symmetry, and transitivity: +The {\bf equality} rules are reflexivity, symmetry, and transitivity: \[ {a\equiv a}\,(refl) \qquad \infer[(sym)]{b\equiv a}{a\equiv b} \qquad \infer[(trans)]{a\equiv c}{a\equiv b & b\equiv c} \] @@ -324,14 +324,14 @@ {((\lambda x.a)(b)) \equiv a[b/x]} \qquad \infer[(ext)]{f\equiv g}{f(x) \equiv g(x)} \] -The {\it abstraction\/} and {\it combination\/} rules permit the conversion -of subterms:\footnote{Abstraction holds if $x$ is not free in the +The {\bf abstraction} and {\bf combination} rules let conversions be +applied to subterms:\footnote{Abstraction holds if $x$ is not free in the assumptions.} \[ \infer[(abs)]{(\lambda x.a) \equiv (\lambda x.b)}{a\equiv b} \qquad \infer[(comb)]{f(a)\equiv g(b)}{f\equiv g & a\equiv b} \] \index{meta-quantifiers} -The {\em universal quantification\/} rules are $(\Forall I)$ and $(\Forall +The {\bf universal quantification} rules are $(\Forall I)$ and $(\Forall E)$:\footnote{$(\Forall I)$ holds if $x$ is not free in the assumptions.} \[ \infer[(\Forall I)]{\Forall x.\phi}{\phi} \qquad \infer[(\Forall E)]{\phi[b/x]}{\Forall x.\phi} \] @@ -344,9 +344,9 @@ \end{ttbox} \begin{ttdescription} \item[\ttindexbold{assume} $ct$] -makes the theorem \(\phi \quad[\phi]\), where $\phi$ is the value of~$ct$. +makes the theorem \(\phi \;[\phi]\), where $\phi$ is the value of~$ct$. The rule checks that $ct$ has type $prop$ and contains no unknowns, which -are not allowed in hypotheses. +are not allowed in assumptions. \end{ttdescription} \subsection{Implication rules} @@ -361,15 +361,16 @@ \begin{ttdescription} \item[\ttindexbold{implies_intr} $ct$ $thm$] is $({\Imp}I)$, where $ct$ is the assumption to discharge, say~$\phi$. It -maps the premise $\psi\quad[\phi]$ to the conclusion $\phi\Imp\psi$. The -rule checks that $ct$ has type $prop$. +maps the premise~$\psi$ to the conclusion $\phi\Imp\psi$, removing all +occurrences of~$\phi$ from the assumptions. The rule checks that $ct$ has +type $prop$. \item[\ttindexbold{implies_intr_list} $cts$ $thm$] applies $({\Imp}I)$ repeatedly, on every element of the list~$cts$. \item[\ttindexbold{implies_intr_hyps} $thm$] -applies $({\Imp}I)$ to discharge all the hypotheses of~$thm$. It maps the -premise $\phi \quad [\phi@1,\ldots,\phi@n]$ to the conclusion +applies $({\Imp}I)$ to discharge all the hypotheses (assumptions) of~$thm$. +It maps the premise $\phi \; [\phi@1,\ldots,\phi@n]$ to the conclusion $\List{\phi@1,\ldots,\phi@n}\Imp\phi$. \item[\ttindexbold{implies_elim} $thm@1$ $thm@2$] @@ -390,8 +391,10 @@ \end{ttbox} \begin{ttdescription} \item[\ttindexbold{equal_intr} $thm@1$ $thm@2$] -applies $({\equiv}I)$ to $thm@1$ and~$thm@2$. It maps the premises -$\psi\quad[\phi]$ and $\phi\quad[\psi]$ to the conclusion~$\phi\equiv\psi$. +applies $({\equiv}I)$ to $thm@1$ and~$thm@2$. It maps the premises~$\psi$ +and~$\phi$ to the conclusion~$\phi\equiv\psi$; the assumptions are those of +the first premise with~$\phi$ removed, plus those of +the second premise with~$\psi$ removed. \item[\ttindexbold{equal_elim} $thm@1$ $thm@2$] applies $({\equiv}E)$ to $thm@1$ and~$thm@2$. It maps the premises @@ -436,14 +439,14 @@ \item[\ttindexbold{extensional} $thm$] maps the premise $f(x) \equiv g(x)$ to the conclusion $f\equiv g$. Parameter~$x$ is taken from the premise. It may be an unknown or a free -variable (provided it does not occur in the hypotheses); it must not occur +variable (provided it does not occur in the assumptions); it must not occur in $f$ or~$g$. \item[\ttindexbold{abstract_rule} $v$ $x$ $thm$] maps the premise $a\equiv b$ to the conclusion $(\lambda x.a) \equiv (\lambda x.b)$, abstracting over all occurrences (if any!) of~$x$. Parameter~$x$ is supplied as a cterm. It may be an unknown or a free -variable (provided it does not occur in the hypotheses). In the +variable (provided it does not occur in the assumptions). In the conclusion, the bound variable is named~$v$. \item[\ttindexbold{combination} $thm@1$ $thm@2$] @@ -465,7 +468,7 @@ applies $({\Forall}I)$, abstracting over all occurrences (if any!) of~$x$. The rule maps the premise $\phi$ to the conclusion $\Forall x.\phi$. Parameter~$x$ is supplied as a cterm. It may be an unknown or a free -variable (provided it does not occur in the hypotheses). +variable (provided it does not occur in the assumptions). \item[\ttindexbold{forall_intr_list} $xs$ $thm$] applies $({\Forall}I)$ repeatedly, on every element of the list~$xs$. @@ -592,7 +595,7 @@ analogous to {\tt RS}\@. For example, suppose that $thm@1$ is $a=b\Imp b=a$, a symmetry rule, and -that $thm@2$ is $\List{P\Imp Q; \neg Q} \Imp\neg P)$, which is the +that $thm@2$ is $\List{P\Imp Q; \neg Q} \Imp\neg P$, which is the principle of contrapositives. Then the result would be the derived rule $\neg(b=a)\Imp\neg(a=b)$.