%% $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 mod b == rec(a, 0,

                       %u v. rec(succ(v) |-| b, 0, %x y.succ(v)))  

 \idx{div_def}   a div b == rec(a, 0,

                       %u v. rec(succ(u) mod 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'mod'

 and~\verb'div' 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\bmod 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\bmod 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))}

 \ttbreak

 {\out val prems = ["A type  [A type]",}

 {\out              "?x : A ==> B(?x) type  [!!x. x : A ==> B(x) type]",}

 {\out              "?x : A ==> C(?x) type  [!!x. x : A ==> C(x) type]",}

 {\out              "p : SUM x:A. B(x) + C(x)  [p : SUM x:A. B(x) + C(x)]"]}

 {\out             : thm list}

 \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))}

 \ttbreak

 {\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}

 \ttbreak

 {\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>))}

 \ttbreak

 {\out val prems = ["A type  [A type]",}

 {\out              "?x : A ==> B(?x) type  [!!x. x : A ==> B(x) type]",}

 {\out              "?z : SUM x:A. B(x) ==> C(?z) type}

 {\out               [!!z. z : SUM x:A. B(x) ==> C(z) type]"] : thm list}

 \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))}

 \ttbreak

 {\out val prems = ["A type  [A type]",}

 {\out              "?x : A ==> B(?x) type  [!!x. x : A ==> B(x) type]",}

 {\out              "[| ?x : A; ?y : B(?x) |] ==> C(?x, ?y) type}

 {\out               [!!x y. [| x : A; y : B(x) |] ==> C(x, y) type]"]}

 {\out             : thm list}

 \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))}

 \ttbreak

 {\out  1. !!uu x.}

 {\out        [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>}

 {\out        ?b7(uu,x) : B(x)}

 \ttbreak

 {\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))}

 \ttbreak

 {\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))}

 \ttbreak

 {\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)}

 \ttbreak

 {\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))}

 \ttbreak

 {\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)}

 \ttbreak

 {\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}

 \ttbreak

 {\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))}

 \ttbreak

 {\out  1. !!uu x.}

 {\out        [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==> x : ?A15(uu,x)}

 \ttbreak

 {\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)}

 \ttbreak

 {\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}

 \ttbreak

 {\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}