doc-src/Logics/CTT.tex
 changeset 9695 ec7d7f877712 parent 7159 b009afd1ace5 child 12679 8ed660138f83
--- 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
contains simple examples of type-checking and type deduction.