--- a/doc-src/Logics/CTT.tex Mon Aug 28 13:50:24 2000 +0200
+++ b/doc-src/Logics/CTT.tex Mon Aug 28 13:52:38 2000 +0200
@@ -40,16 +40,16 @@
Assumptions can use all the judgement forms, for instance to express that
$B$ is a family of types over~$A$:
\[ \Forall x . x\in A \Imp B(x)\;{\rm type} \]
-To justify the {\CTT} formulation it is probably best to appeal directly
-to the semantic explanations of the rules~\cite{martinlof84}, rather than
-to the rules themselves. The order of assumptions no longer matters,
-unlike in standard Type Theory. Contexts, which are typical of many modern
-type theories, are difficult to represent in Isabelle. In particular, it
-is difficult to enforce that all the variables in a context are distinct.
-\index{assumptions!in {\CTT}}
+To justify the CTT formulation it is probably best to appeal directly to the
+semantic explanations of the rules~\cite{martinlof84}, rather than to the
+rules themselves. The order of assumptions no longer matters, unlike in
+standard Type Theory. Contexts, which are typical of many modern type
+theories, are difficult to represent in Isabelle. In particular, it is
+difficult to enforce that all the variables in a context are distinct.
+\index{assumptions!in CTT}
-The theory does not use polymorphism. Terms in {\CTT} have type~\tydx{i}, the
-type of individuals. Types in {\CTT} have type~\tydx{t}.
+The theory does not use polymorphism. Terms in CTT have type~\tydx{i}, the
+type of individuals. Types in CTT have type~\tydx{t}.
\begin{figure} \tabcolsep=1em %wider spacing in tables
\begin{center}
@@ -81,29 +81,29 @@
\cdx{tt} & $i$ & constructor
\end{tabular}
\end{center}
-\caption{The constants of {\CTT}} \label{ctt-constants}
+\caption{The constants of CTT} \label{ctt-constants}
\end{figure}
-{\CTT} supports all of Type Theory apart from list types, well-ordering
-types, and universes. Universes could be introduced {\em\`a la Tarski},
-adding new constants as names for types. The formulation {\em\`a la
- Russell}, where types denote themselves, is only possible if we identify
-the meta-types~{\tt i} and~{\tt t}. Most published formulations of
-well-ordering types have difficulties involving extensionality of
-functions; I suggest that you use some other method for defining recursive
-types. List types are easy to introduce by declaring new rules.
+CTT supports all of Type Theory apart from list types, well-ordering types,
+and universes. Universes could be introduced {\em\`a la Tarski}, adding new
+constants as names for types. The formulation {\em\`a la Russell}, where
+types denote themselves, is only possible if we identify the meta-types~{\tt
+ i} and~{\tt t}. Most published formulations of well-ordering types have
+difficulties involving extensionality of functions; I suggest that you use
+some other method for defining recursive types. List types are easy to
+introduce by declaring new rules.
-{\CTT} uses the 1982 version of Type Theory, with extensional equality.
-The computation $a=b\in A$ and the equality $c\in Eq(A,a,b)$ are
-interchangeable. Its rewriting tactics prove theorems of the form $a=b\in
-A$. It could be modified to have intensional equality, but rewriting
-tactics would have to prove theorems of the form $c\in Eq(A,a,b)$ and the
-computation rules might require a separate simplifier.
+CTT uses the 1982 version of Type Theory, with extensional equality. The
+computation $a=b\in A$ and the equality $c\in Eq(A,a,b)$ are interchangeable.
+Its rewriting tactics prove theorems of the form $a=b\in A$. It could be
+modified to have intensional equality, but rewriting tactics would have to
+prove theorems of the form $c\in Eq(A,a,b)$ and the computation rules might
+require a separate simplifier.
\begin{figure} \tabcolsep=1em %wider spacing in tables
-\index{lambda abs@$\lambda$-abstractions!in \CTT}
+\index{lambda abs@$\lambda$-abstractions!in CTT}
\begin{center}
\begin{tabular}{llrrr}
\it symbol &\it name &\it meta-type & \it priority & \it description \\
@@ -113,7 +113,7 @@
\subcaption{Binders}
\begin{center}
-\index{*"` symbol}\index{function applications!in \CTT}
+\index{*"` symbol}\index{function applications!in CTT}
\index{*"+ symbol}
\begin{tabular}{rrrr}
\it symbol & \it meta-type & \it priority & \it description \\
@@ -160,7 +160,7 @@
\]
\end{center}
\subcaption{Grammar}
-\caption{Syntax of {\CTT}} \label{ctt-syntax}
+\caption{Syntax of CTT} \label{ctt-syntax}
\end{figure}
%%%%\section{Generic Packages} typedsimp.ML????????????????
@@ -168,16 +168,16 @@
\section{Syntax}
The constants are shown in Fig.\ts\ref{ctt-constants}. The infixes include
-the function application operator (sometimes called `apply'), and the
-2-place type operators. Note that meta-level abstraction and application,
-$\lambda x.b$ and $f(a)$, differ from object-level abstraction and
-application, \hbox{\tt lam $x$. $b$} and $b{\tt`}a$. A {\CTT}
-function~$f$ is simply an individual as far as Isabelle is concerned: its
-Isabelle type is~$i$, not say $i\To i$.
+the function application operator (sometimes called `apply'), and the 2-place
+type operators. Note that meta-level abstraction and application, $\lambda
+x.b$ and $f(a)$, differ from object-level abstraction and application,
+\hbox{\tt lam $x$. $b$} and $b{\tt`}a$. A CTT function~$f$ is simply an
+individual as far as Isabelle is concerned: its Isabelle type is~$i$, not say
+$i\To i$.
-The notation for~{\CTT} (Fig.\ts\ref{ctt-syntax}) is based on that of
-Nordstr\"om et al.~\cite{nordstrom90}. The empty type is called $F$ and
-the one-element type is $T$; other finite types are built as $T+T+T$, etc.
+The notation for~CTT (Fig.\ts\ref{ctt-syntax}) is based on that of Nordstr\"om
+et al.~\cite{nordstrom90}. The empty type is called $F$ and the one-element
+type is $T$; other finite types are built as $T+T+T$, etc.
\index{*SUM symbol}\index{*PROD symbol}
Quantification is expressed by sums $\sum@{x\in A}B[x]$ and
@@ -387,7 +387,7 @@
|] ==> snd(p) : B(fst(p))
\end{ttbox}
-\caption{Derived rules for {\CTT}} \label{ctt-derived}
+\caption{Derived rules for CTT} \label{ctt-derived}
\end{figure}
@@ -470,7 +470,7 @@
\section{Rule lists}
The Type Theory tactics provide rewriting, type inference, and logical
reasoning. Many proof procedures work by repeatedly resolving certain Type
-Theory rules against a proof state. {\CTT} defines lists --- each with
+Theory rules against a proof state. CTT defines lists --- each with
type
\hbox{\tt thm list} --- of related rules.
\begin{ttdescription}
@@ -514,14 +514,14 @@
equal_tac : thm list -> tactic
intr_tac : thm list -> tactic
\end{ttbox}
-Blind application of {\CTT} rules seldom leads to a proof. The elimination
+Blind application of CTT rules seldom leads to a proof. The elimination
rules, especially, create subgoals containing new unknowns. These subgoals
unify with anything, creating a huge search space. The standard tactic
-\ttindex{filt_resolve_tac}
+\ttindex{filt_resolve_tac}
(see \iflabelundefined{filt_resolve_tac}{the {\em Reference Manual\/}}%
{\S\ref{filt_resolve_tac}})
%
-fails for goals that are too flexible; so does the {\CTT} tactic {\tt
+fails for goals that are too flexible; so does the CTT tactic {\tt
test_assume_tac}. Used with the tactical \ttindex{REPEAT_FIRST} they
achieve a simple kind of subgoal reordering: the less flexible subgoals are
attempted first. Do some single step proofs, or study the examples below,
@@ -563,8 +563,8 @@
CTT} equality rules and the built-in rewriting functor
{\tt TSimpFun}.%
\footnote{This should not be confused with Isabelle's main simplifier; {\tt
- TSimpFun} is only useful for {\CTT} and similar logics with type
- inference rules. At present it is undocumented.}
+ TSimpFun} is only useful for CTT and similar logics with type inference
+ rules. At present it is undocumented.}
%
The rewrites include the computation rules and other equations. The long
versions of the other rules permit rewriting of subterms and subtypes.
@@ -583,11 +583,11 @@
\section{Tactics for logical reasoning}
-Interpreting propositions as types lets {\CTT} express statements of
-intuitionistic logic. However, Constructive Type Theory is not just
-another syntax for first-order logic. There are fundamental differences.
+Interpreting propositions as types lets CTT express statements of
+intuitionistic logic. However, Constructive Type Theory is not just another
+syntax for first-order logic. There are fundamental differences.
-\index{assumptions!in {\CTT}}
+\index{assumptions!in CTT}
Can assumptions be deleted after use? Not every occurrence of a type
represents a proposition, and Type Theory assumptions declare variables.
In first-order logic, $\disj$-elimination with the assumption $P\disj Q$
@@ -598,7 +598,7 @@
refer to $z$ may render the subgoal unprovable: arguably,
meaningless.
-Isabelle provides several tactics for predicate calculus reasoning in \CTT:
+Isabelle provides several tactics for predicate calculus reasoning in CTT:
\begin{ttbox}
mp_tac : int -> tactic
add_mp_tac : int -> tactic
@@ -728,7 +728,7 @@
\section{The examples directory}
-This directory contains examples and experimental proofs in {\CTT}.
+This directory contains examples and experimental proofs in CTT.
\begin{ttdescription}
\item[CTT/ex/typechk.ML]
contains simple examples of type-checking and type deduction.