doc-src/Logics/CTT.tex
changeset 104 d8205bb279a7
child 111 1b3cddf41b2d
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Logics/CTT.tex	Wed Nov 10 05:00:57 1993 +0100
@@ -0,0 +1,1110 @@
+%% $Id$
+\chapter{Constructive Type Theory}
+Martin-L\"of's Constructive Type Theory \cite{martinlof84,nordstrom90} can
+be viewed at many different levels.  It is a formal system that embodies
+the principles of intuitionistic mathematics; it embodies the
+interpretation of propositions as types; it is a vehicle for deriving
+programs from proofs.  The logic is complex and many authors have attempted
+to simplify it.  Thompson~\cite{thompson91} is a readable and thorough
+account of the theory.
+
+Isabelle's original formulation of Type Theory was a kind of sequent
+calculus, following Martin-L\"of~\cite{martinlof84}.  It included rules for
+building the context, namely variable bindings with their types.  A typical
+judgement was
+\[   a(x@1,\ldots,x@n)\in A(x@1,\ldots,x@n) \; 
+    [ x@1\in A@1, x@2\in A@2(x@1), \ldots, x@n\in A@n(x@1,\ldots,x@{n-1}) ]
+\]
+This sequent calculus was not satisfactory because assumptions like
+`suppose $A$ is a type' or `suppose $B(x)$ is a type for all $x$ in $A$'
+could not be formalized.  
+
+The directory~\ttindexbold{CTT} implements Constructive Type Theory, using
+natural deduction.  The judgement above is expressed using $\Forall$ and
+$\Imp$:
+\[ \begin{array}{r@{}l}
+     \Forall x@1\ldots x@n. &
+	  \List{x@1\in A@1; 
+		x@2\in A@2(x@1); \cdots \; 
+		x@n\in A@n(x@1,\ldots,x@{n-1})} \Imp \\
+     &  \qquad\qquad a(x@1,\ldots,x@n)\in A(x@1,\ldots,x@n) 
+    \end{array}
+\]
+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.
+
+The theory has the {\ML} identifier \ttindexbold{CTT.thy}.  It does not
+use polymorphism.  Terms in {\CTT} have type~$i$, the type of individuals.
+Types in {\CTT} have type~$t$.
+
+{\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~$i$ and~$o$.  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 second simplifier.
+
+
+\begin{figure} \tabcolsep=1em  %wider spacing in tables
+\begin{center}
+\begin{tabular}{rrr} 
+  \it symbol  	& \it meta-type 	& \it description \\ 
+  \idx{Type}    & $t \to prop$		& judgement form \\
+  \idx{Eqtype}  & $[t,t]\to prop$	& judgement form\\
+  \idx{Elem}    & $[i, t]\to prop$	& judgement form\\
+  \idx{Eqelem}  & $[i, i, t]\to prop$	& judgement form\\
+  \idx{Reduce}  & $[i, i]\to prop$	& extra judgement form\\[2ex]
+
+  \idx{N}       &     $t$		& natural numbers type\\
+  \idx{0}       &     $i$		& constructor\\
+  \idx{succ}    & $i\to i$		& constructor\\
+  \idx{rec}     & $[i,i,[i,i]\to i]\to i$       & eliminator\\[2ex]
+  \idx{Prod}    & $[t,i\to t]\to t$	& general product type\\
+  \idx{lambda}  & $(i\to i)\to i$	& constructor\\[2ex]
+  \idx{Sum}     & $[t, i\to t]\to t$	& general sum type\\
+  \idx{pair}    & $[i,i]\to i$		& constructor\\
+  \idx{split}   & $[i,[i,i]\to i]\to i$	& eliminator\\
+  \idx{fst} snd & $i\to i$		& projections\\[2ex]
+  \idx{inl} inr & $i\to i$		& constructors for $+$\\
+  \idx{when}    & $[i,i\to i, i\to i]\to i$    & eliminator for $+$\\[2ex]
+  \idx{Eq}      & $[t,i,i]\to t$	& equality type\\
+  \idx{eq}      & $i$			& constructor\\[2ex]
+  \idx{F}       & $t$			& empty type\\
+  \idx{contr}   & $i\to i$		& eliminator\\[2ex]
+  \idx{T}       & $t$			& singleton type\\
+  \idx{tt}      & $i$			& constructor
+\end{tabular}
+\end{center}
+\caption{The constants of {\CTT}} \label{ctt-constants}
+\end{figure}
+
+
+\begin{figure} \tabcolsep=1em  %wider spacing in tables
+\begin{center}
+\begin{tabular}{llrrr} 
+  \it symbol &\it name	   &\it meta-type & \it precedence & \it description \\
+  \idx{lam} & \idx{lambda}  & $(i\To o)\To i$ & 10 & $\lambda$-abstraction
+\end{tabular}
+\end{center}
+\subcaption{Binders} 
+
+\begin{center}
+\indexbold{*"`}
+\indexbold{*"+}
+\begin{tabular}{rrrr} 
+  \it symbol & \it meta-type & \it precedence & \it description \\ 
+  \tt `		& $[i,i]\to i$	& Left 55 	& function application\\
+  \tt +		& $[t,t]\to t$	& Right 30 	& sum of two types
+\end{tabular}
+\end{center}
+\subcaption{Infixes}
+
+\indexbold{*"*}
+\indexbold{*"-"-">}
+\begin{center} \tt\frenchspacing
+\begin{tabular}{rrr} 
+  \it external                	& \it internal  & \it standard notation \\ 
+  \idx{PROD} $x$:$A$ . $B[x]$	&  Prod($A$, $\lambda x.B[x]$) &
+      	\rm product $\prod@{x\in A}B[x]$ \\
+  \idx{SUM} $x$:$A$ . $B[x]$	& Sum($A$, $\lambda x.B[x]$) &
+      	\rm sum $\sum@{x\in A}B[x]$ \\
+  $A$ --> $B$     &  Prod($A$, $\lambda x.B$) &
+	\rm function space $A\to B$ \\
+  $A$ * $B$       &  Sum($A$, $\lambda x.B$)  &
+	\rm binary product $A\times B$
+\end{tabular}
+\end{center}
+\subcaption{Translations} 
+
+\indexbold{*"=}
+\begin{center}
+\dquotes
+\[ \begin{array}{rcl}
+prop  	& = &  type " type"       \\
+	& | & type " = " type     \\
+	& | & term " : " type        \\
+	& | & term " = " term " : " type 
+\\[2ex]
+type  	& = & \hbox{expression of type~$t$} \\
+	& | & "PROD~" id " : " type " . " type  \\
+	& | & "SUM~~" id " : " type " . " type 
+\\[2ex]
+term  	& = & \hbox{expression of type~$i$} \\
+	& | & "lam " id~id^* " . " term   \\
+	& | & "< " term " , " term " >"
+\end{array} 
+\]
+\end{center}
+\subcaption{Grammar}
+\caption{Syntax of {\CTT}} \label{ctt-syntax}
+\end{figure}
+
+%%%%\section{Generic Packages}  typedsimp.ML????????????????
+
+
+\section{Syntax}
+The constants are shown in Figure~\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$.
+
+\indexbold{*F}\indexbold{*T}\indexbold{*SUM}\indexbold{*PROD}
+The empty type is called $F$ and the one-element type is $T$; other finite
+sets are built as $T+T+T$, etc.  The notation for~{\CTT}
+(Figure~\ref{ctt-syntax}) is based on that of Nordstr\"om et
+al.~\cite{nordstrom90}.  We can write
+\begin{ttbox}
+SUM y:B. PROD x:A. C(x,y)   {\rm for}   Sum(B, %y. Prod(A, %x. C(x,y)))
+\end{ttbox}
+The special cases as \hbox{\tt$A$*$B$} and \hbox{\tt$A$-->$B$} abbreviate
+general sums and products over a constant family.\footnote{Unlike normal
+infix operators, {\tt*} and {\tt-->} merely define abbreviations; there are
+no constants~{\tt op~*} and~\hbox{\tt op~-->}.}  Isabelle accepts these
+abbreviations in parsing and uses them whenever possible for printing.
+
+
+\begin{figure} 
+\begin{ttbox}
+\idx{refl_type}         A type ==> A = A
+\idx{refl_elem}         a : A ==> a = a : A
+
+\idx{sym_type}          A = B ==> B = A
+\idx{sym_elem}          a = b : A ==> b = a : A
+
+\idx{trans_type}        [| A = B;  B = C |] ==> A = C
+\idx{trans_elem}        [| a = b : A;  b = c : A |] ==> a = c : A
+
+\idx{equal_types}       [| a : A;  A = B |] ==> a : B
+\idx{equal_typesL}      [| a = b : A;  A = B |] ==> a = b : B
+
+\idx{subst_type}        [| a : A;  !!z. z:A ==> B(z) type |] ==> B(a) type
+\idx{subst_typeL}       [| a = c : A;  !!z. z:A ==> B(z) = D(z) 
+                  |] ==> B(a) = D(c)
+
+\idx{subst_elem}        [| a : A;  !!z. z:A ==> b(z):B(z) |] ==> b(a):B(a)
+\idx{subst_elemL}       [| a = c : A;  !!z. z:A ==> b(z) = d(z) : B(z) 
+                  |] ==> b(a) = d(c) : B(a)
+
+\idx{refl_red}          Reduce(a,a)
+\idx{red_if_equal}      a = b : A ==> Reduce(a,b)
+\idx{trans_red}         [| a = b : A;  Reduce(b,c) |] ==> a = c : A
+\end{ttbox}
+\caption{General equality rules} \label{ctt-equality}
+\end{figure}
+
+
+\begin{figure} 
+\begin{ttbox}
+\idx{NF}        N type
+
+\idx{NI0}       0 : N
+\idx{NI_succ}   a : N ==> succ(a) : N
+\idx{NI_succL}  a = b : N ==> succ(a) = succ(b) : N
+
+\idx{NE}        [| p: N;  a: C(0);  
+             !!u v. [| u: N; v: C(u) |] ==> b(u,v): C(succ(u)) 
+          |] ==> rec(p, a, %u v.b(u,v)) : C(p)
+
+\idx{NEL}       [| p = q : N;  a = c : C(0);  
+             !!u v. [| u: N; v: C(u) |] ==> b(u,v)=d(u,v): C(succ(u))
+          |] ==> rec(p, a, %u v.b(u,v)) = rec(q,c,d) : C(p)
+
+\idx{NC0}       [| a: C(0);  
+             !!u v. [| u: N; v: C(u) |] ==> b(u,v): C(succ(u))
+          |] ==> rec(0, a, %u v.b(u,v)) = a : C(0)
+
+\idx{NC_succ}   [| p: N;  a: C(0);  
+             !!u v. [| u: N; v: C(u) |] ==> b(u,v): C(succ(u)) 
+          |] ==> rec(succ(p), a, %u v.b(u,v)) =
+                 b(p, rec(p, a, %u v.b(u,v))) : C(succ(p))
+
+\idx{zero_ne_succ}      [| a: N;  0 = succ(a) : N |] ==> 0: F
+\end{ttbox}
+\caption{Rules for type~$N$} \label{ctt-N}
+\end{figure}
+
+
+\begin{figure} 
+\begin{ttbox}
+\idx{ProdF}     [| A type; !!x. x:A ==> B(x) type |] ==> PROD x:A.B(x) type
+\idx{ProdFL}    [| A = C;  !!x. x:A ==> B(x) = D(x) |] ==> 
+          PROD x:A.B(x) = PROD x:C.D(x)
+
+\idx{ProdI}     [| A type;  !!x. x:A ==> b(x):B(x)
+          |] ==> lam x.b(x) : PROD x:A.B(x)
+\idx{ProdIL}    [| A type;  !!x. x:A ==> b(x) = c(x) : B(x)
+          |] ==> lam x.b(x) = lam x.c(x) : PROD x:A.B(x)
+
+\idx{ProdE}     [| p : PROD x:A.B(x);  a : A |] ==> p`a : B(a)
+\idx{ProdEL}    [| p=q: PROD x:A.B(x);  a=b : A |] ==> p`a = q`b : B(a)
+
+\idx{ProdC}     [| a : A;  !!x. x:A ==> b(x) : B(x)
+          |] ==> (lam x.b(x)) ` a = b(a) : B(a)
+
+\idx{ProdC2}    p : PROD x:A.B(x) ==> (lam x. p`x) = p : PROD x:A.B(x)
+\end{ttbox}
+\caption{Rules for the product type $\prod@{x\in A}B[x]$} \label{ctt-prod}
+\end{figure}
+
+
+\begin{figure} 
+\begin{ttbox}
+\idx{SumF}      [| A type;  !!x. x:A ==> B(x) type |] ==> SUM x:A.B(x) type
+\idx{SumFL}     [| A = C;  !!x. x:A ==> B(x) = D(x) 
+          |] ==> SUM x:A.B(x) = SUM x:C.D(x)
+
+\idx{SumI}      [| a : A;  b : B(a) |] ==> <a,b> : SUM x:A.B(x)
+\idx{SumIL}     [| a=c:A;  b=d:B(a) |] ==> <a,b> = <c,d> : SUM x:A.B(x)
+
+\idx{SumE}      [| p: SUM x:A.B(x);  
+             !!x y. [| x:A; y:B(x) |] ==> c(x,y): C(<x,y>) 
+          |] ==> split(p, %x y.c(x,y)) : C(p)
+
+\idx{SumEL}     [| p=q : SUM x:A.B(x); 
+             !!x y. [| x:A; y:B(x) |] ==> c(x,y)=d(x,y): C(<x,y>)
+          |] ==> split(p, %x y.c(x,y)) = split(q, %x y.d(x,y)) : C(p)
+
+\idx{SumC}      [| a: A;  b: B(a);
+             !!x y. [| x:A; y:B(x) |] ==> c(x,y): C(<x,y>)
+          |] ==> split(<a,b>, %x y.c(x,y)) = c(a,b) : C(<a,b>)
+
+\idx{fst_def}   fst(a) == split(a, %x y.x)
+\idx{snd_def}   snd(a) == split(a, %x y.y)
+\end{ttbox}
+\caption{Rules for the sum type $\sum@{x\in A}B[x]$} \label{ctt-sum}
+\end{figure}
+
+
+\begin{figure} 
+\begin{ttbox}
+\idx{PlusF}       [| A type;  B type |] ==> A+B type
+\idx{PlusFL}      [| A = C;  B = D |] ==> A+B = C+D
+
+\idx{PlusI_inl}   [| a : A;  B type |] ==> inl(a) : A+B
+\idx{PlusI_inlL}  [| a = c : A;  B type |] ==> inl(a) = inl(c) : A+B
+
+\idx{PlusI_inr}   [| A type;  b : B |] ==> inr(b) : A+B
+\idx{PlusI_inrL}  [| A type;  b = d : B |] ==> inr(b) = inr(d) : A+B
+
+\idx{PlusE}     [| p: A+B;
+             !!x. x:A ==> c(x): C(inl(x));  
+             !!y. y:B ==> d(y): C(inr(y))
+          |] ==> when(p, %x.c(x), %y.d(y)) : C(p)
+
+\idx{PlusEL}    [| p = q : A+B;
+             !!x. x: A ==> c(x) = e(x) : C(inl(x));   
+             !!y. y: B ==> d(y) = f(y) : C(inr(y))
+          |] ==> when(p, %x.c(x), %y.d(y)) = 
+                 when(q, %x.e(x), %y.f(y)) : C(p)
+
+\idx{PlusC_inl} [| a: A;
+             !!x. x:A ==> c(x): C(inl(x));  
+             !!y. y:B ==> d(y): C(inr(y))
+          |] ==> when(inl(a), %x.c(x), %y.d(y)) = c(a) : C(inl(a))
+
+\idx{PlusC_inr} [| b: B;
+             !!x. x:A ==> c(x): C(inl(x));  
+             !!y. y:B ==> d(y): C(inr(y))
+          |] ==> when(inr(b), %x.c(x), %y.d(y)) = d(b) : C(inr(b))
+\end{ttbox}
+\caption{Rules for the binary sum type $A+B$} \label{ctt-plus}
+\end{figure}
+
+
+\begin{figure} 
+\begin{ttbox}
+\idx{EqF}       [| A type;  a : A;  b : A |] ==> Eq(A,a,b) type
+\idx{EqFL}      [| A=B;  a=c: A;  b=d : A |] ==> Eq(A,a,b) = Eq(B,c,d)
+\idx{EqI}       a = b : A ==> eq : Eq(A,a,b)
+\idx{EqE}       p : Eq(A,a,b) ==> a = b : A
+\idx{EqC}       p : Eq(A,a,b) ==> p = eq : Eq(A,a,b)
+\end{ttbox}
+\subcaption{The equality type $Eq(A,a,b)$} 
+
+\begin{ttbox}
+\idx{FF}        F type
+\idx{FE}        [| p: F;  C type |] ==> contr(p) : C
+\idx{FEL}       [| p = q : F;  C type |] ==> contr(p) = contr(q) : C
+\end{ttbox}
+\subcaption{The empty type $F$} 
+
+\begin{ttbox}
+\idx{TF}        T type
+\idx{TI}        tt : T
+\idx{TE}        [| p : T;  c : C(tt) |] ==> c : C(p)
+\idx{TEL}       [| p = q : T;  c = d : C(tt) |] ==> c = d : C(p)
+\idx{TC}        p : T ==> p = tt : T)
+\end{ttbox}
+\subcaption{The unit type $T$} 
+
+\caption{Rules for other {\CTT} types} \label{ctt-others}
+\end{figure}
+
+
+
+\begin{figure} 
+\begin{ttbox}
+\idx{replace_type}    [| B = A;  a : A |] ==> a : B
+\idx{subst_eqtyparg}  [| a=c : A;  !!z. z:A ==> B(z) type |] ==> B(a)=B(c)
+
+\idx{subst_prodE}     [| p: Prod(A,B);  a: A;  !!z. z: B(a) ==> c(z): C(z)
+                |] ==> c(p`a): C(p`a)
+
+\idx{SumIL2}    [| c=a : A;  d=b : B(a) |] ==> <c,d> = <a,b> : Sum(A,B)
+
+\idx{SumE_fst}  p : Sum(A,B) ==> fst(p) : A
+
+\idx{SumE_snd}  [| p: Sum(A,B);  A type;  !!x. x:A ==> B(x) type
+          |] ==> snd(p) : B(fst(p))
+\end{ttbox}
+
+\caption{Derived rules for {\CTT}} \label{ctt-derived}
+\end{figure}
+
+
+\section{Rules of inference}
+The rules obey the following naming conventions.  Type formation rules have
+the suffix~{\tt F}\@.  Introduction rules have the suffix~{\tt I}\@.
+Elimination rules have the suffix~{\tt E}\@.  Computation rules, which
+describe the reduction of eliminators, have the suffix~{\tt C}\@.  The
+equality versions of the rules (which permit reductions on subterms) are
+called {\em long} rules; their names have the suffix~{\tt L}\@.
+Introduction and computation rules often are further suffixed with
+constructor names.
+
+Figures~\ref{ctt-equality}--\ref{ctt-others} shows the rules.  Those
+for~$N$ include \ttindex{zero_ne_succ}, $0\not=n+1$: the fourth Peano axiom
+cannot be derived without universes \cite[page 91]{martinlof84}.
+Figure~\ref{ctt-sum} shows the rules for general sums, which include binary
+products as a special case, with the projections \ttindex{fst}
+and~\ttindex{snd}.
+
+The extra judgement \ttindex{Reduce} is used to implement rewriting.  The
+judgement ${\tt Reduce}(a,b)$ holds when $a=b:A$ holds.  It also holds
+when $a$ and $b$ are syntactically identical, even if they are ill-typed,
+because rule \ttindex{refl_red} does not verify that $a$ belongs to $A$.  These
+rules do not give rise to new theorems about the standard judgements ---
+note that the only rule that makes use of {\tt Reduce} is \ttindex{trans_red},
+whose first premise ensures that $a$ and $b$ (and thus $c$) are well-typed.
+
+Derived rules are shown in Figure~\ref{ctt-derived}.  The rule
+\ttindex{subst_prodE} is derived from \ttindex{prodE}, and is easier to
+use in backwards proof.  The rules \ttindex{SumE_fst} and
+\ttindex{SumE_snd} express the typing of~\ttindex{fst} and~\ttindex{snd};
+together, they are roughly equivalent to~\ttindex{SumE} with the advantage
+of creating no parameters.  These rules are demonstrated in a proof of the
+Axiom of Choice~(\S\ref{ctt-choice}).
+
+All the rules are given in $\eta$-expanded form.  For instance, every
+occurrence of $\lambda u\,v.b(u,v)$ could be abbreviated to~$b$ in the
+rules for~$N$.  This permits Isabelle to preserve bound variable names
+during backward proof.  Names of bound variables in the conclusion (here,
+$u$ and~$v$) are matched with corresponding bound variables in the premises.
+
+
+\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
+type
+\hbox{\tt thm list} --- of related rules. 
+\begin{description}
+\item[\ttindexbold{form_rls}] 
+contains formation rules for the types $N$, $\Pi$, $\Sigma$, $+$, $Eq$,
+$F$, and $T$.
+
+\item[\ttindexbold{formL_rls}] 
+contains long formation rules for $\Pi$, $\Sigma$, $+$, and $Eq$.  (For
+other types use \ttindex{refl_type}.)
+
+\item[\ttindexbold{intr_rls}] 
+contains introduction rules for the types $N$, $\Pi$, $\Sigma$, $+$, and
+$T$.
+
+\item[\ttindexbold{intrL_rls}] 
+contains long introduction rules for $N$, $\Pi$, $\Sigma$, and $+$.  (For
+$T$ use \ttindex{refl_elem}.)
+
+\item[\ttindexbold{elim_rls}] 
+contains elimination rules for the types $N$, $\Pi$, $\Sigma$, $+$, and
+$F$.  The rules for $Eq$ and $T$ are omitted because they involve no
+eliminator.
+
+\item[\ttindexbold{elimL_rls}] 
+contains long elimination rules for $N$, $\Pi$, $\Sigma$, $+$, and $F$.
+
+\item[\ttindexbold{comp_rls}] 
+contains computation rules for the types $N$, $\Pi$, $\Sigma$, and $+$.
+Those for $Eq$ and $T$ involve no eliminator.
+
+\item[\ttindexbold{basic_defs}] 
+contains the definitions of \ttindex{fst} and \ttindex{snd}.  
+\end{description}
+
+
+\section{Tactics for subgoal reordering}
+\begin{ttbox}
+test_assume_tac : int -> tactic
+typechk_tac     : thm list -> tactic
+equal_tac       : thm list -> tactic
+intr_tac        : thm list -> tactic
+\end{ttbox}
+Blind application of {\CTT} rules seldom leads to a proof.  The elimination
+rules, especially, create subgoals containing new unknowns.  These subgoals
+unify with anything, causing an undirectional search.  The standard tactic
+\ttindex{filt_resolve_tac} (see the {\em Reference Manual}) can reject
+overly flexible goals; 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, to see why this is
+necessary.
+\begin{description}
+\item[\ttindexbold{test_assume_tac} $i$] 
+uses \ttindex{assume_tac} to solve the subgoal by assumption, but only if
+subgoal~$i$ has the form $a\in A$ and the head of $a$ is not an unknown.
+Otherwise, it fails.
+
+\item[\ttindexbold{typechk_tac} $thms$] 
+uses $thms$ with formation, introduction, and elimination rules to check
+the typing of constructions.  It is designed to solve goals of the form
+$a\in \Var{A}$, where $a$ is rigid and $\Var{A}$ is flexible.  Thus it
+performs Hindley-Milner type inference.  The tactic can also solve goals of
+the form $A\;\rm type$.
+
+\item[\ttindexbold{equal_tac} $thms$]
+uses $thms$ with the long introduction and elimination rules to solve goals
+of the form $a=b\in A$, where $a$ is rigid.  It is intended for deriving
+the long rules for defined constants such as the arithmetic operators.  The
+tactic can also perform type checking.
+
+\item[\ttindexbold{intr_tac} $thms$]
+uses $thms$ with the introduction rules to break down a type.  It is
+designed for goals like $\Var{a}\in A$ where $\Var{a}$ is flexible and $A$
+rigid.  These typically arise when trying to prove a proposition~$A$,
+expressed as a type.
+\end{description}
+
+
+
+\section{Rewriting tactics}
+\begin{ttbox}
+rew_tac     : thm list -> tactic
+hyp_rew_tac : thm list -> tactic
+\end{ttbox}
+Object-level simplification is accomplished through proof, using the {\tt
+CTT} equality rules and the built-in rewriting functor
+\ttindex{TSimpFun}.\footnote{This should not be confused with {\tt
+SimpFun}, which is the main rewriting functor; {\tt TSimpFun} is only
+useful for {\CTT} and similar logics with type inference rules.}
+The rewrites include the computation rules and other equations.  The
+long versions of the other rules permit rewriting of subterms and subtypes.
+Also used are transitivity and the extra judgement form \ttindex{Reduce}.
+Meta-level simplification handles only definitional equality.
+\begin{description}
+\item[\ttindexbold{rew_tac} $thms$]
+applies $thms$ and the computation rules as left-to-right rewrites.  It
+solves the goal $a=b\in A$ by rewriting $a$ to $b$.  If $b$ is an unknown
+then it is assigned the rewritten form of~$a$.  All subgoals are rewritten.
+
+\item[\ttindexbold{hyp_rew_tac} $thms$]
+is like {\tt rew_tac}, but includes as rewrites any equations present in
+the assumptions.
+\end{description}
+
+
+\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. A key question: 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$
+creates one subgoal assuming $P$ and another assuming $Q$, and $P\disj Q$
+can be deleted.  In Type Theory, $+$-elimination with the assumption $z\in
+A+B$ creates one subgoal assuming $x\in A$ and another assuming $y\in B$
+(for arbitrary $x$ and $y$).  Deleting $z\in A+B$ may render the subgoals
+unprovable if other assumptions refer to $z$.  Some people might argue that
+such subgoals are not even meaningful.
+\begin{ttbox}
+mp_tac       : int -> tactic
+add_mp_tac   : int -> tactic
+safestep_tac : thm list -> int -> tactic
+safe_tac     : thm list -> int -> tactic
+step_tac     : thm list -> int -> tactic
+pc_tac       : thm list -> int -> tactic
+\end{ttbox}
+These are loosely based on the intuitionistic proof procedures
+of~\ttindex{FOL}.  For the reasons discussed above, a rule that is safe for
+propositional reasoning may be unsafe for type checking; thus, some of the
+``safe'' tactics are misnamed.
+\begin{description}
+\item[\ttindexbold{mp_tac} $i$] 
+searches in subgoal~$i$ for assumptions of the form $f\in\Pi(A,B)$ and
+$a\in A$, where~$A$ may be found by unification.  It replaces
+$f\in\Pi(A,B)$ by $z\in B(a)$, where~$z$ is a new parameter.  The tactic
+can produce multiple outcomes for each suitable pair of assumptions.  In
+short, {\tt mp_tac} performs Modus Ponens among the assumptions.
+
+\item[\ttindexbold{add_mp_tac} $i$]
+is like {\tt mp_tac}~$i$ but retains the assumption $f\in\Pi(A,B)$.
+
+\item[\ttindexbold{safestep_tac} $thms$ $i$]
+attacks subgoal~$i$ using formation rules and certain other `safe' rules
+(\ttindex{FE}, \ttindex{ProdI}, \ttindex{SumE}, \ttindex{PlusE}), calling
+{\tt mp_tac} when appropriate.  It also uses~$thms$,
+which are typically premises of the rule being derived.
+
+\item[\ttindexbold{safe_tac} $thms$ $i$]
+tries to solve subgoal~$i$ by backtracking, using {\tt safestep_tac}.
+
+\item[\ttindexbold{step_tac} $thms$ $i$]
+tries to reduce subgoal~$i$ using {\tt safestep_tac}, then tries unsafe
+rules.  It may produce multiple outcomes.
+
+\item[\ttindexbold{pc_tac} $thms$ $i$]
+tries to solve subgoal~$i$ by backtracking, using {\tt step_tac}.
+\end{description}
+
+
+
+\begin{figure} 
+\begin{ttbox}
+\idx{add_def}           a#+b  == rec(a, b, %u v.succ(v))  
+\idx{diff_def}          a-b   == rec(b, a, %u v.rec(v, 0, %x y.x))  
+\idx{absdiff_def}       a|-|b == (a-b) #+ (b-a)  
+\idx{mult_def}          a#*b  == rec(a, 0, %u v. b #+ v)  
+
+\idx{mod_def}   a//b == rec(a, 0,
+                      %u v. rec(succ(v) |-| b, 0, %x y.succ(v)))  
+
+\idx{quo_def}   a/b == rec(a, 0,
+                      %u v. rec(succ(u) // b, succ(v), %x y.v))
+\end{ttbox}
+\subcaption{Definitions of the operators}
+
+\begin{ttbox}
+\idx{add_typing}        [| a:N;  b:N |] ==> a #+ b : N
+\idx{addC0}             b:N ==> 0 #+ b = b : N
+\idx{addC_succ}         [| a:N;  b:N |] ==> succ(a) #+ b = succ(a #+ b) : N
+
+\idx{add_assoc}         [| a:N;  b:N;  c:N |] ==> 
+                  (a #+ b) #+ c = a #+ (b #+ c) : N
+
+\idx{add_commute}       [| a:N;  b:N |] ==> a #+ b = b #+ a : N
+
+\idx{mult_typing}       [| a:N;  b:N |] ==> a #* b : N
+\idx{multC0}            b:N ==> 0 #* b = 0 : N
+\idx{multC_succ}        [| a:N;  b:N |] ==> succ(a) #* b = b #+ (a#*b) : N
+\idx{mult_commute}      [| a:N;  b:N |] ==> a #* b = b #* a : N
+
+\idx{add_mult_dist}     [| a:N;  b:N;  c:N |] ==> 
+                  (a #+ b) #* c = (a #* c) #+ (b #* c) : N
+
+\idx{mult_assoc}        [| a:N;  b:N;  c:N |] ==> 
+                  (a #* b) #* c = a #* (b #* c) : N
+
+\idx{diff_typing}       [| a:N;  b:N |] ==> a - b : N
+\idx{diffC0}            a:N ==> a - 0 = a : N
+\idx{diff_0_eq_0}       b:N ==> 0 - b = 0 : N
+\idx{diff_succ_succ}    [| a:N;  b:N |] ==> succ(a) - succ(b) = a - b : N
+\idx{diff_self_eq_0}    a:N ==> a - a = 0 : N
+\idx{add_inverse_diff}  [| a:N;  b:N;  b-a=0 : N |] ==> b #+ (a-b) = a : N
+\end{ttbox}
+\subcaption{Some theorems of arithmetic}
+\caption{The theory of arithmetic} \label{ctt-arith}
+\end{figure}
+
+
+\section{A theory of arithmetic}
+{\CTT} contains a theory of elementary arithmetic.  It proves the
+properties of addition, multiplication, subtraction, division, and
+remainder, culminating in the theorem
+\[ a \bmod b + (a/b)\times b = a. \]
+Figure~\ref{ctt-arith} presents the definitions and some of the key
+theorems, including commutative, distributive, and associative laws.  The
+theory has the {\ML} identifier \ttindexbold{arith.thy}.  All proofs are on
+the file \ttindexbold{CTT/arith.ML}.
+
+The operators~\verb'#+', \verb'-', \verb'|-|', \verb'#*', \verb'//'
+and~\verb'/' stand for sum, difference, absolute difference, product,
+remainder and quotient, respectively.  Since Type Theory has only primitive
+recursion, some of their definitions may be obscure.  
+
+The difference~$a-b$ is computed by taking $b$ predecessors of~$a$, where
+the predecessor function is $\lambda v. {\tt rec}(v, 0, \lambda x\,y.x)$.
+
+The remainder $a//b$ counts up to~$a$ in a cyclic fashion, using 0 as the
+successor of~$b-1$.  Absolute difference is used to test the equality
+$succ(v)=b$.
+
+The quotient $a//b$ is computed by adding one for every number $x$ such
+that $0\leq x \leq a$ and $x//b = 0$.
+
+
+
+\section{The examples directory}
+This directory contains examples and experimental proofs in {\CTT}.
+\begin{description}
+\item[\ttindexbold{CTT/ex/typechk.ML}]
+contains simple examples of type checking and type deduction.
+
+\item[\ttindexbold{CTT/ex/elim.ML}]
+contains some examples from Martin-L\"of~\cite{martinlof84}, proved using 
+{\tt pc_tac}.
+
+\item[\ttindexbold{CTT/ex/equal.ML}]
+contains simple examples of rewriting.
+
+\item[\ttindexbold{CTT/ex/synth.ML}]
+demonstrates the use of unknowns with some trivial examples of program
+synthesis. 
+\end{description}
+
+
+\section{Example: type inference}
+Type inference involves proving a goal of the form $a\in\Var{A}$, where $a$
+is a term and $\Var{A}$ is an unknown standing for its type.  The type,
+initially
+unknown, takes shape in the course of the proof.  Our example is the
+predecessor function on the natural numbers.
+\begin{ttbox}
+goal CTT.thy "lam n. rec(n, 0, %x y.x) : ?A";
+{\out Level 0}
+{\out lam n. rec(n,0,%x y. x) : ?A}
+{\out  1. lam n. rec(n,0,%x y. x) : ?A}
+\end{ttbox}
+Since the term is a Constructive Type Theory $\lambda$-abstraction (not to
+be confused with a meta-level abstraction), we apply the rule
+\ttindex{ProdI}, for $\Pi$-introduction.  This instantiates~$\Var{A}$ to a
+product type of unknown domain and range.
+\begin{ttbox}
+by (resolve_tac [ProdI] 1);
+{\out Level 1}
+{\out lam n. rec(n,0,%x y. x) : PROD x:?A1. ?B1(x)}
+{\out  1. ?A1 type}
+{\out  2. !!n. n : ?A1 ==> rec(n,0,%x y. x) : ?B1(n)}
+\end{ttbox}
+Subgoal~1 can be solved by instantiating~$\Var{A@1}$ to any type, but this
+could invalidate subgoal~2.  We therefore tackle the latter subgoal.  It
+asks the type of a term beginning with {\tt rec}, which can be found by
+$N$-elimination.\index{*NE}
+\begin{ttbox}
+by (eresolve_tac [NE] 2);
+{\out Level 2}
+{\out lam n. rec(n,0,%x y. x) : PROD x:N. ?C2(x,x)}
+{\out  1. N type}
+{\out  2. !!n. 0 : ?C2(n,0)}
+{\out  3. !!n x y. [| x : N; y : ?C2(n,x) |] ==> x : ?C2(n,succ(x))}
+\end{ttbox}
+We now know~$\Var{A@1}$ is the type of natural numbers.  However, let us
+continue with subgoal~2.  What is the type of~0?\index{*NIO}
+\begin{ttbox}
+by (resolve_tac [NI0] 2);
+{\out Level 3}
+{\out lam n. rec(n,0,%x y. x) : N --> N}
+{\out  1. N type}
+{\out  2. !!n x y. [| x : N; y : N |] ==> x : N}
+\end{ttbox}
+The type~$\Var{A}$ is now determined.  It is $\prod@{n\in N}N$, which is
+equivalent to $N\to N$.  But we must prove all the subgoals to show that
+the original term is validly typed.  Subgoal~2 is provable by assumption
+and the remaining subgoal falls by $N$-formation.\index{*NF}
+\begin{ttbox}
+by (assume_tac 2);
+{\out Level 4}
+{\out lam n. rec(n,0,%x y. x) : N --> N}
+{\out  1. N type}
+by (resolve_tac [NF] 1);
+{\out Level 5}
+{\out lam n. rec(n,0,%x y. x) : N --> N}
+{\out No subgoals!}
+\end{ttbox}
+Calling \ttindex{typechk_tac} can prove this theorem in one step.
+
+
+\section{An example of logical reasoning}
+Logical reasoning in Type Theory involves proving a goal of the form
+$\Var{a}\in A$, where type $A$ expresses a proposition and $\Var{a}$ is an
+unknown standing
+for its proof term: a value of type $A$. This term is initially unknown, as
+with type inference, and takes shape during the proof.  Our example
+expresses, by propositions-as-types, a theorem about quantifiers in a
+sorted logic:
+\[ \infer{(\ex{x\in A}P(x)) \disj (\ex{x\in A}Q(x))}
+         {\ex{x\in A}P(x)\disj Q(x)} 
+\]
+It it related to a distributive law of Type Theory:
+\[ \infer{(A\times B) + (A\times C)}{A\times(B+C)} \]
+Generalizing this from $\times$ to $\Sigma$, and making the typing
+conditions explicit, yields
+\[ \infer{\Var{a} \in (\sum@{x\in A} B(x)) + (\sum@{x\in A} C(x))}
+         {\hbox{$A$ type} &
+          \infer*{\hbox{$B(x)$ type}}{[x\in A]}  &
+          \infer*{\hbox{$C(x)$ type}}{[x\in A]}  &
+          p\in \sum@{x\in A} B(x)+C(x)} 
+\]
+To derive this rule, we bind its premises --- returned by~\ttindex{goal}
+--- to the {\ML} variable~{\tt prems}.
+\begin{ttbox}
+val prems = goal CTT.thy
+    "[| A type;                       \ttback
+\ttback       !!x. x:A ==> B(x) type;       \ttback
+\ttback       !!x. x:A ==> C(x) type;       \ttback
+\ttback       p: SUM x:A. B(x) + C(x)       \ttback
+\ttback    |] ==>  ?a : (SUM x:A. B(x)) + (SUM x:A. C(x))";
+{\out Level 0}
+{\out ?a : (SUM x:A. B(x)) + (SUM x:A. C(x))}
+{\out  1. ?a : (SUM x:A. B(x)) + (SUM x:A. C(x))}
+\end{ttbox}
+One of the premises involves summation ($\Sigma$).  Since it is a premise
+rather than the assumption of a goal, it cannot be found by
+\ttindex{eresolve_tac}.  We could insert it by calling
+\hbox{\tt \ttindex{cut_facts_tac} prems 1}.   Instead, let us resolve the
+$\Sigma$-elimination rule with the premises; this yields one result, which
+we supply to \ttindex{resolve_tac}.\index{*SumE}\index{*RL}
+\begin{ttbox}
+by (resolve_tac (prems RL [SumE]) 1);
+{\out Level 1}
+{\out split(p,?c1) : (SUM x:A. B(x)) + (SUM x:A. C(x))}
+{\out  1. !!x y.}
+{\out        [| x : A; y : B(x) + C(x) |] ==>}
+{\out        ?c1(x,y) : (SUM x:A. B(x)) + (SUM x:A. C(x))}
+\end{ttbox}
+The subgoal has two new parameters.  In the main goal, $\Var{a}$ has been
+instantiated with a \ttindex{split} term.  The assumption $y\in B(x) + C(x)$ is
+eliminated next, causing a case split and a new parameter.  The main goal
+now contains~\ttindex{when}.
+\index{*PlusE}
+\begin{ttbox}
+by (eresolve_tac [PlusE] 1);
+{\out Level 2}
+{\out split(p,%x y. when(y,?c2(x,y),?d2(x,y)))}
+{\out : (SUM x:A. B(x)) + (SUM x:A. C(x))}
+{\out  1. !!x y xa.}
+{\out        [| x : A; xa : B(x) |] ==>}
+{\out        ?c2(x,y,xa) : (SUM x:A. B(x)) + (SUM x:A. C(x))}
+{\out  2. !!x y ya.}
+{\out        [| x : A; ya : C(x) |] ==>}
+{\out        ?d2(x,y,ya) : (SUM x:A. B(x)) + (SUM x:A. C(x))}
+\end{ttbox}
+To complete the proof object for the main goal, we need to instantiate the
+terms $\Var{c@2}(x,y,xa)$ and $\Var{d@2}(x,y,xa)$.  We attack subgoal~1 by
+introduction of~$+$; since it assumes $xa\in B(x)$, we take the left
+injection~(\ttindex{inl}).
+\index{*PlusI_inl}
+\begin{ttbox}
+by (resolve_tac [PlusI_inl] 1);
+{\out Level 3}
+{\out split(p,%x y. when(y,%xa. inl(?a3(x,y,xa)),?d2(x,y)))}
+{\out : (SUM x:A. B(x)) + (SUM x:A. C(x))}
+{\out  1. !!x y xa. [| x : A; xa : B(x) |] ==> ?a3(x,y,xa) : SUM x:A. B(x)}
+{\out  2. !!x y xa. [| x : A; xa : B(x) |] ==> SUM x:A. C(x) type}
+{\out  3. !!x y ya.}
+{\out        [| x : A; ya : C(x) |] ==>}
+{\out        ?d2(x,y,ya) : (SUM x:A. B(x)) + (SUM x:A. C(x))}
+\end{ttbox}
+A new subgoal has appeared, to verify that $\sum@{x\in A}C(x)$ is a type.
+Continuing with subgoal~1, we apply $\Sigma$-introduction.  The main goal
+now contains an ordered pair.
+\index{*SumI}
+\begin{ttbox}
+by (resolve_tac [SumI] 1);
+{\out Level 4}
+{\out split(p,%x y. when(y,%xa. inl(<?a4(x,y,xa),?b4(x,y,xa)>),?d2(x,y)))}
+{\out : (SUM x:A. B(x)) + (SUM x:A. C(x))}
+{\out  1. !!x y xa. [| x : A; xa : B(x) |] ==> ?a4(x,y,xa) : A}
+{\out  2. !!x y xa. [| x : A; xa : B(x) |] ==> ?b4(x,y,xa) : B(?a4(x,y,xa))}
+{\out  3. !!x y xa. [| x : A; xa : B(x) |] ==> SUM x:A. C(x) type}
+{\out  4. !!x y ya.}
+{\out        [| x : A; ya : C(x) |] ==>}
+{\out        ?d2(x,y,ya) : (SUM x:A. B(x)) + (SUM x:A. C(x))}
+\end{ttbox}
+The two new subgoals both hold by assumption.  Observe how the unknowns
+$\Var{a@4}$ and $\Var{b@4}$ are instantiated throughout the proof state.
+\begin{ttbox}
+by (assume_tac 1);
+{\out Level 5}
+{\out split(p,%x y. when(y,%xa. inl(<x,?b4(x,y,xa)>),?d2(x,y)))}
+{\out : (SUM x:A. B(x)) + (SUM x:A. C(x))}
+{\out  1. !!x y xa. [| x : A; xa : B(x) |] ==> ?b4(x,y,xa) : B(x)}
+{\out  2. !!x y xa. [| x : A; xa : B(x) |] ==> SUM x:A. C(x) type}
+{\out  3. !!x y ya.}
+{\out        [| x : A; ya : C(x) |] ==>}
+{\out        ?d2(x,y,ya) : (SUM x:A. B(x)) + (SUM x:A. C(x))}
+by (assume_tac 1);
+{\out Level 6}
+{\out split(p,%x y. when(y,%xa. inl(<x,xa>),?d2(x,y)))}
+{\out : (SUM x:A. B(x)) + (SUM x:A. C(x))}
+{\out  1. !!x y xa. [| x : A; xa : B(x) |] ==> SUM x:A. C(x) type}
+{\out  2. !!x y ya.}
+{\out        [| x : A; ya : C(x) |] ==>}
+{\out        ?d2(x,y,ya) : (SUM x:A. B(x)) + (SUM x:A. C(x))}
+\end{ttbox}
+Subgoal~1 is just type checking.  It yields to \ttindex{typechk_tac},
+supplied with the current list of premises.
+\begin{ttbox}
+by (typechk_tac prems);
+{\out Level 7}
+{\out split(p,%x y. when(y,%xa. inl(<x,xa>),?d2(x,y)))}
+{\out : (SUM x:A. B(x)) + (SUM x:A. C(x))}
+{\out  1. !!x y ya.}
+{\out        [| x : A; ya : C(x) |] ==>}
+{\out        ?d2(x,y,ya) : (SUM x:A. B(x)) + (SUM x:A. C(x))}
+\end{ttbox}
+The other case is similar.  Let us prove it by \ttindex{pc_tac}, and note
+the final proof object.
+\begin{ttbox}
+by (pc_tac prems 1);
+{\out Level 8}
+{\out split(p,%x y. when(y,%xa. inl(<x,xa>),%y. inr(<x,y>)))}
+{\out : (SUM x:A. B(x)) + (SUM x:A. C(x))}
+{\out No subgoals!}
+\end{ttbox}
+Calling \ttindex{pc_tac} after the first $\Sigma$-elimination above also
+proves this theorem.
+
+
+\section{Example: deriving a currying functional}
+In simply-typed languages such as {\ML}, a currying functional has the type 
+\[ (A\times B \to C) \to (A\to (B\to C)). \]
+Let us generalize this to~$\Sigma$ and~$\Pi$.  The argument of the
+functional is a function that maps $z:\Sigma(A,B)$ to~$C(z)$; the resulting
+function maps $x\in A$ and $y\in B(x)$ to $C(\langle x,y\rangle)$.  Here
+$B$ is a family over~$A$, while $C$ is a family over $\Sigma(A,B)$.
+\begin{ttbox}
+val prems = goal CTT.thy
+    "[| A type; !!x. x:A ==> B(x) type;                    \ttback
+\ttback               !!z. z: (SUM x:A. B(x)) ==> C(z) type |]   \ttback
+\ttback    ==> ?a : (PROD z : (SUM x:A . B(x)) . C(z))           \ttback
+\ttback         --> (PROD x:A . PROD y:B(x) . C(<x,y>))";
+{\out Level 0}
+{\out ?a : (PROD z:SUM x:A. B(x). C(z)) --> (PROD x:A. PROD y:B(x). C(<x,y>))}
+{\out  1. ?a : (PROD z:SUM x:A. B(x). C(z)) -->}
+{\out          (PROD x:A. PROD y:B(x). C(<x,y>))}
+\end{ttbox}
+This is an opportunity to demonstrate \ttindex{intr_tac}.  Here, the tactic
+repeatedly applies $\Pi$-introduction, automatically proving the rather
+tiresome typing conditions.  Note that $\Var{a}$ becomes instantiated to
+three nested $\lambda$-abstractions.
+\begin{ttbox}
+by (intr_tac prems);
+{\out Level 1}
+{\out lam x xa xb. ?b7(x,xa,xb)}
+{\out : (PROD z:SUM x:A. B(x). C(z)) --> (PROD x:A. PROD y:B(x). C(<x,y>))}
+{\out  1. !!uu x y.}
+{\out        [| uu : PROD z:SUM x:A. B(x). C(z); x : A; y : B(x) |] ==>}
+{\out        ?b7(uu,x,y) : C(<x,y>)}
+\end{ttbox}
+Using $\Pi$-elimination, we solve subgoal~1 by applying the function~$uu$.
+\index{*ProdE}
+\begin{ttbox}
+by (eresolve_tac [ProdE] 1);
+{\out Level 2}
+{\out lam x xa xb. x ` <xa,xb>}
+{\out : (PROD z:SUM x:A. B(x). C(z)) --> (PROD x:A. PROD y:B(x). C(<x,y>))}
+{\out  1. !!uu x y. [| x : A; y : B(x) |] ==> <x,y> : SUM x:A. B(x)}
+\end{ttbox}
+Finally, we exhibit a suitable argument for the function application.  This
+is straightforward using introduction rules.
+\index{*intr_tac}
+\begin{ttbox}
+by (intr_tac prems);
+{\out Level 3}
+{\out lam x xa xb. x ` <xa,xb>}
+{\out : (PROD z:SUM x:A. B(x). C(z)) --> (PROD x:A. PROD y:B(x). C(<x,y>))}
+{\out No subgoals!}
+\end{ttbox}
+Calling~\ttindex{pc_tac} would have proved this theorem in one step; it can
+also prove an example by Martin-L\"of, related to $\disj$-elimination
+\cite[page~58]{martinlof84}.
+
+
+\section{Example: proving the Axiom of Choice} \label{ctt-choice}
+Suppose we have a function $h\in \prod@{x\in A}\sum@{y\in B(x)} C(x,y)$,
+which takes $x\in A$ to some $y\in B(x)$ paired with some $z\in C(x,y)$.
+Interpreting propositions as types, this asserts that for all $x\in A$
+there exists $y\in B(x)$ such that $C(x,y)$.  The Axiom of Choice asserts
+that we can construct a function $f\in \prod@{x\in A}B(x)$ such that
+$C(x,f{\tt`}x)$ for all $x\in A$, where the latter property is witnessed by a
+function $g\in \prod@{x\in A}C(x,f{\tt`}x)$.
+
+In principle, the Axiom of Choice is simple to derive in Constructive Type
+Theory \cite[page~50]{martinlof84}.  The following definitions work:
+\begin{eqnarray*}
+    f & \equiv & {\tt fst} \circ h \\
+    g & \equiv & {\tt snd} \circ h
+\end{eqnarray*}
+But a completely formal proof is hard to find.  Many of the rules can be
+applied in a multiplicity of ways, yielding a large number of higher-order
+unifiers.  The proof can get bogged down in the details.  But with a
+careful selection of derived rules (recall Figure~\ref{ctt-derived}) and
+the type checking tactics, we can prove the theorem in nine steps.
+\begin{ttbox}
+val prems = goal CTT.thy
+    "[| A type;  !!x. x:A ==> B(x) type;              \ttback
+\ttback       !!x y.[| x:A;  y:B(x) |] ==> C(x,y) type      \ttback
+\ttback    |] ==> ?a :    (PROD x:A. SUM y:B(x). C(x,y))    \ttback
+\ttback               --> (SUM f: (PROD x:A. B(x)). PROD x:A. C(x, f`x))";
+{\out Level 0}
+{\out ?a : (PROD x:A. SUM y:B(x). C(x,y)) -->}
+{\out      (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))}
+{\out  1. ?a : (PROD x:A. SUM y:B(x). C(x,y)) -->}
+{\out          (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))}
+\end{ttbox}
+First, \ttindex{intr_tac} applies introduction rules and performs routine
+type checking.  This instantiates~$\Var{a}$ to a construction involving
+three $\lambda$-abstractions and an ordered pair.
+\begin{ttbox}
+by (intr_tac prems);
+{\out Level 1}
+{\out lam x. <lam xa. ?b7(x,xa),lam xa. ?b8(x,xa)>}
+{\out : (PROD x:A. SUM y:B(x). C(x,y)) -->}
+{\out   (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))}
+{\out  1. !!uu x.}
+{\out        [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>}
+{\out        ?b7(uu,x) : B(x)}
+{\out  2. !!uu x.}
+{\out        [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>}
+{\out        ?b8(uu,x) : C(x,(lam x. ?b7(uu,x)) ` x)}
+\end{ttbox}
+Subgoal~1 asks to find the choice function itself, taking $x\in A$ to some
+$\Var{b@7}(uu,x)\in B(x)$.  Subgoal~2 asks, given $x\in A$, for a proof
+object $\Var{b@8}(uu,x)$ to witness that the choice function's argument
+and result lie in the relation~$C$.  
+\index{*ProdE}\index{*SumE_fst}\index{*RS}
+\begin{ttbox}
+by (eresolve_tac [ProdE RS SumE_fst] 1);
+{\out Level 2}
+{\out lam x. <lam xa. fst(x ` xa),lam xa. ?b8(x,xa)>}
+{\out : (PROD x:A. SUM y:B(x). C(x,y)) -->}
+{\out   (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))}
+{\out  1. !!uu x. x : A ==> x : A}
+{\out  2. !!uu x.}
+{\out        [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>}
+{\out        ?b8(uu,x) : C(x,(lam x. fst(uu ` x)) ` x)}
+\end{ttbox}
+Above, we have composed \ttindex{fst} with the function~$h$ (named~$uu$ in
+the assumptions).  Unification has deduced that the function must be
+applied to $x\in A$.
+\begin{ttbox}
+by (assume_tac 1);
+{\out Level 3}
+{\out lam x. <lam xa. fst(x ` xa),lam xa. ?b8(x,xa)>}
+{\out : (PROD x:A. SUM y:B(x). C(x,y)) -->}
+{\out   (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))}
+{\out  1. !!uu x.}
+{\out        [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>}
+{\out        ?b8(uu,x) : C(x,(lam x. fst(uu ` x)) ` x)}
+\end{ttbox}
+Before we can compose \ttindex{snd} with~$h$, the arguments of $C$ must be
+simplified.  The derived rule \ttindex{replace_type} lets us replace a type
+by any equivalent type:
+\begin{ttbox}
+by (resolve_tac [replace_type] 1);
+{\out Level 4}
+{\out lam x. <lam xa. fst(x ` xa),lam xa. ?b8(x,xa)>}
+{\out : (PROD x:A. SUM y:B(x). C(x,y)) -->}
+{\out   (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))}
+{\out  1. !!uu x.}
+{\out        [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>}
+{\out        C(x,(lam x. fst(uu ` x)) ` x) = ?A13(uu,x)}
+{\out  2. !!uu x.}
+{\out        [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>}
+{\out        ?b8(uu,x) : ?A13(uu,x)}
+\end{ttbox}
+The derived rule \ttindex{subst_eqtyparg} lets us simplify a type's
+argument (by currying, $C(x)$ is a unary type operator):
+\begin{ttbox}
+by (resolve_tac [subst_eqtyparg] 1);
+{\out Level 5}
+{\out lam x. <lam xa. fst(x ` xa),lam xa. ?b8(x,xa)>}
+{\out : (PROD x:A. SUM y:B(x). C(x,y)) -->}
+{\out   (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))}
+{\out  1. !!uu x.}
+{\out        [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>}
+{\out        (lam x. fst(uu ` x)) ` x = ?c14(uu,x) : ?A14(uu,x)}
+{\out  2. !!uu x z.}
+{\out        [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A;}
+{\out           z : ?A14(uu,x) |] ==>}
+{\out        C(x,z) type}
+{\out  3. !!uu x.}
+{\out        [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>}
+{\out        ?b8(uu,x) : C(x,?c14(uu,x))}
+\end{ttbox}
+The rule \ttindex{ProdC} is simply $\beta$-reduction.  The term
+$\Var{c@{14}}(uu,x)$ receives the simplified form, $f{\tt`}x$.
+\begin{ttbox}
+by (resolve_tac [ProdC] 1);
+{\out Level 6}
+{\out lam x. <lam xa. fst(x ` xa),lam xa. ?b8(x,xa)>}
+{\out : (PROD x:A. SUM y:B(x). C(x,y)) -->}
+{\out   (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))}
+{\out  1. !!uu x.}
+{\out        [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==> x : ?A15(uu,x)}
+{\out  2. !!uu x xa.}
+{\out        [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A;}
+{\out           xa : ?A15(uu,x) |] ==>}
+{\out        fst(uu ` xa) : ?B15(uu,x,xa)}
+{\out  3. !!uu x z.}
+{\out        [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A;}
+{\out           z : ?B15(uu,x,x) |] ==>}
+{\out        C(x,z) type}
+{\out  4. !!uu x.}
+{\out        [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>}
+{\out        ?b8(uu,x) : C(x,fst(uu ` x))}
+\end{ttbox}
+Routine type checking goals proliferate in Constructive Type Theory, but
+\ttindex{typechk_tac} quickly solves them.  Note the inclusion of
+\ttindex{SumE_fst}.
+\begin{ttbox}
+by (typechk_tac (SumE_fst::prems));
+{\out Level 7}
+{\out lam x. <lam xa. fst(x ` xa),lam xa. ?b8(x,xa)>}
+{\out : (PROD x:A. SUM y:B(x). C(x,y)) -->}
+{\out   (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))}
+{\out  1. !!uu x.}
+{\out        [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>}
+{\out        ?b8(uu,x) : C(x,fst(uu ` x))}
+\end{ttbox}
+We are finally ready to compose \ttindex{snd} with~$h$.
+\index{*ProdE}\index{*SumE_snd}\index{*RS}
+\begin{ttbox}
+by (eresolve_tac [ProdE RS SumE_snd] 1);
+{\out Level 8}
+{\out lam x. <lam xa. fst(x ` xa),lam xa. snd(x ` xa)>}
+{\out : (PROD x:A. SUM y:B(x). C(x,y)) -->}
+{\out   (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))}
+{\out  1. !!uu x. x : A ==> x : A}
+{\out  2. !!uu x. x : A ==> B(x) type}
+{\out  3. !!uu x xa. [| x : A; xa : B(x) |] ==> C(x,xa) type}
+\end{ttbox}
+The proof object has reached its final form.  We call \ttindex{typechk_tac}
+to finish the type checking.
+\begin{ttbox}
+by (typechk_tac prems);
+{\out Level 9}
+{\out lam x. <lam xa. fst(x ` xa),lam xa. snd(x ` xa)>}
+{\out : (PROD x:A. SUM y:B(x). C(x,y)) -->}
+{\out   (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))}
+{\out No subgoals!}
+\end{ttbox}