--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Doc/Logics/document/CTT.tex Tue Aug 28 18:57:32 2012 +0200
@@ -0,0 +1,1257 @@
+\chapter{Constructive Type Theory}
+\index{Constructive Type Theory|(}
+
+\underscoreoff %this file contains _ in rule names
+
+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.
+
+Thompson's book~\cite{thompson91} gives a readable and thorough account of
+Type Theory. Nuprl is an elaborate implementation~\cite{constable86}.
+{\sc alf} is a more recent tool that allows proof terms to be edited
+directly~\cite{alf}.
+
+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 theory~\thydx{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.
+\index{assumptions!in CTT}
+
+The theory does not use polymorphism. Terms in CTT have type~\tydx{i}, the
+type of individuals. Types in CTT have type~\tydx{t}.
+
+\begin{figure} \tabcolsep=1em %wider spacing in tables
+\begin{center}
+\begin{tabular}{rrr}
+ \it name & \it meta-type & \it description \\
+ \cdx{Type} & $t \to prop$ & judgement form \\
+ \cdx{Eqtype} & $[t,t]\to prop$ & judgement form\\
+ \cdx{Elem} & $[i, t]\to prop$ & judgement form\\
+ \cdx{Eqelem} & $[i, i, t]\to prop$ & judgement form\\
+ \cdx{Reduce} & $[i, i]\to prop$ & extra judgement form\\[2ex]
+
+ \cdx{N} & $t$ & natural numbers type\\
+ \cdx{0} & $i$ & constructor\\
+ \cdx{succ} & $i\to i$ & constructor\\
+ \cdx{rec} & $[i,i,[i,i]\to i]\to i$ & eliminator\\[2ex]
+ \cdx{Prod} & $[t,i\to t]\to t$ & general product type\\
+ \cdx{lambda} & $(i\to i)\to i$ & constructor\\[2ex]
+ \cdx{Sum} & $[t, i\to t]\to t$ & general sum type\\
+ \cdx{pair} & $[i,i]\to i$ & constructor\\
+ \cdx{split} & $[i,[i,i]\to i]\to i$ & eliminator\\
+ \cdx{fst} \cdx{snd} & $i\to i$ & projections\\[2ex]
+ \cdx{inl} \cdx{inr} & $i\to i$ & constructors for $+$\\
+ \cdx{when} & $[i,i\to i, i\to i]\to i$ & eliminator for $+$\\[2ex]
+ \cdx{Eq} & $[t,i,i]\to t$ & equality type\\
+ \cdx{eq} & $i$ & constructor\\[2ex]
+ \cdx{F} & $t$ & empty type\\
+ \cdx{contr} & $i\to i$ & eliminator\\[2ex]
+ \cdx{T} & $t$ & singleton type\\
+ \cdx{tt} & $i$ & constructor
+\end{tabular}
+\end{center}
+\caption{The constants of CTT} \label{ctt-constants}
+\end{figure}
+
+
+CTT supports all of Type Theory apart from list types, well-ordering types,
+and universes. Universes could be introduced {\em\`a la Tarski}, adding new
+constants as names for types. The formulation {\em\`a la Russell}, where
+types denote themselves, is only possible if we identify the meta-types~{\tt
+ i} and~{\tt t}. Most published formulations of well-ordering types have
+difficulties involving extensionality of functions; I suggest that you use
+some other method for defining recursive types. List types are easy to
+introduce by declaring new rules.
+
+CTT uses the 1982 version of Type Theory, with extensional equality. The
+computation $a=b\in A$ and the equality $c\in Eq(A,a,b)$ are interchangeable.
+Its rewriting tactics prove theorems of the form $a=b\in A$. It could be
+modified to have intensional equality, but rewriting tactics would have to
+prove theorems of the form $c\in Eq(A,a,b)$ and the computation rules might
+require a separate simplifier.
+
+
+\begin{figure} \tabcolsep=1em %wider spacing in tables
+\index{lambda abs@$\lambda$-abstractions!in CTT}
+\begin{center}
+\begin{tabular}{llrrr}
+ \it symbol &\it name &\it meta-type & \it priority & \it description \\
+ \sdx{lam} & \cdx{lambda} & $(i\To o)\To i$ & 10 & $\lambda$-abstraction
+\end{tabular}
+\end{center}
+\subcaption{Binders}
+
+\begin{center}
+\index{*"` symbol}\index{function applications!in CTT}
+\index{*"+ symbol}
+\begin{tabular}{rrrr}
+ \it symbol & \it meta-type & \it priority & \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}
+
+\index{*"* symbol}
+\index{*"-"-"> symbol}
+\begin{center} \tt\frenchspacing
+\begin{tabular}{rrr}
+ \it external & \it internal & \it standard notation \\
+ \sdx{PROD} $x$:$A$ . $B[x]$ & Prod($A$, $\lambda x. B[x]$) &
+ \rm product $\prod@{x\in A}B[x]$ \\
+ \sdx{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}
+
+\index{*"= symbol}
+\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 Fig.\ts\ref{ctt-constants}. The infixes include
+the function application operator (sometimes called `apply'), and the 2-place
+type operators. Note that meta-level abstraction and application, $\lambda
+x.b$ and $f(a)$, differ from object-level abstraction and application,
+\hbox{\tt lam $x$. $b$} and $b{\tt`}a$. A CTT function~$f$ is simply an
+individual as far as Isabelle is concerned: its Isabelle type is~$i$, not say
+$i\To i$.
+
+The notation for~CTT (Fig.\ts\ref{ctt-syntax}) is based on that of Nordstr\"om
+et al.~\cite{nordstrom90}. The empty type is called $F$ and the one-element
+type is $T$; other finite types are built as $T+T+T$, etc.
+
+\index{*SUM symbol}\index{*PROD symbol}
+Quantification is expressed by sums $\sum@{x\in A}B[x]$ and
+products $\prod@{x\in A}B[x]$. Instead of {\tt Sum($A$,$B$)} and {\tt
+ Prod($A$,$B$)} we may write \hbox{\tt SUM $x$:$A$.\ $B[x]$} and \hbox{\tt
+ PROD $x$:$A$.\ $B[x]$}. For example, we may 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}
+\tdx{refl_type} A type ==> A = A
+\tdx{refl_elem} a : A ==> a = a : A
+
+\tdx{sym_type} A = B ==> B = A
+\tdx{sym_elem} a = b : A ==> b = a : A
+
+\tdx{trans_type} [| A = B; B = C |] ==> A = C
+\tdx{trans_elem} [| a = b : A; b = c : A |] ==> a = c : A
+
+\tdx{equal_types} [| a : A; A = B |] ==> a : B
+\tdx{equal_typesL} [| a = b : A; A = B |] ==> a = b : B
+
+\tdx{subst_type} [| a : A; !!z. z:A ==> B(z) type |] ==> B(a) type
+\tdx{subst_typeL} [| a = c : A; !!z. z:A ==> B(z) = D(z)
+ |] ==> B(a) = D(c)
+
+\tdx{subst_elem} [| a : A; !!z. z:A ==> b(z):B(z) |] ==> b(a):B(a)
+\tdx{subst_elemL} [| a = c : A; !!z. z:A ==> b(z) = d(z) : B(z)
+ |] ==> b(a) = d(c) : B(a)
+
+\tdx{refl_red} Reduce(a,a)
+\tdx{red_if_equal} a = b : A ==> Reduce(a,b)
+\tdx{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}
+\tdx{NF} N type
+
+\tdx{NI0} 0 : N
+\tdx{NI_succ} a : N ==> succ(a) : N
+\tdx{NI_succL} a = b : N ==> succ(a) = succ(b) : N
+
+\tdx{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)
+
+\tdx{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)
+
+\tdx{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)
+
+\tdx{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))
+
+\tdx{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}
+\tdx{ProdF} [| A type; !!x. x:A ==> B(x) type |] ==> PROD x:A. B(x) type
+\tdx{ProdFL} [| A = C; !!x. x:A ==> B(x) = D(x) |] ==>
+ PROD x:A. B(x) = PROD x:C. D(x)
+
+\tdx{ProdI} [| A type; !!x. x:A ==> b(x):B(x)
+ |] ==> lam x. b(x) : PROD x:A. B(x)
+\tdx{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)
+
+\tdx{ProdE} [| p : PROD x:A. B(x); a : A |] ==> p`a : B(a)
+\tdx{ProdEL} [| p=q: PROD x:A. B(x); a=b : A |] ==> p`a = q`b : B(a)
+
+\tdx{ProdC} [| a : A; !!x. x:A ==> b(x) : B(x)
+ |] ==> (lam x. b(x)) ` a = b(a) : B(a)
+
+\tdx{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\sb{x\in A}B[x]$} \label{ctt-prod}
+\end{figure}
+
+
+\begin{figure}
+\begin{ttbox}
+\tdx{SumF} [| A type; !!x. x:A ==> B(x) type |] ==> SUM x:A. B(x) type
+\tdx{SumFL} [| A = C; !!x. x:A ==> B(x) = D(x)
+ |] ==> SUM x:A. B(x) = SUM x:C. D(x)
+
+\tdx{SumI} [| a : A; b : B(a) |] ==> <a,b> : SUM x:A. B(x)
+\tdx{SumIL} [| a=c:A; b=d:B(a) |] ==> <a,b> = <c,d> : SUM x:A. B(x)
+
+\tdx{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)
+
+\tdx{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)
+
+\tdx{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>)
+
+\tdx{fst_def} fst(a) == split(a, \%x y. x)
+\tdx{snd_def} snd(a) == split(a, \%x y. y)
+\end{ttbox}
+\caption{Rules for the sum type $\sum\sb{x\in A}B[x]$} \label{ctt-sum}
+\end{figure}
+
+
+\begin{figure}
+\begin{ttbox}
+\tdx{PlusF} [| A type; B type |] ==> A+B type
+\tdx{PlusFL} [| A = C; B = D |] ==> A+B = C+D
+
+\tdx{PlusI_inl} [| a : A; B type |] ==> inl(a) : A+B
+\tdx{PlusI_inlL} [| a = c : A; B type |] ==> inl(a) = inl(c) : A+B
+
+\tdx{PlusI_inr} [| A type; b : B |] ==> inr(b) : A+B
+\tdx{PlusI_inrL} [| A type; b = d : B |] ==> inr(b) = inr(d) : A+B
+
+\tdx{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)
+
+\tdx{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)
+
+\tdx{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))
+
+\tdx{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}
+\tdx{FF} F type
+\tdx{FE} [| p: F; C type |] ==> contr(p) : C
+\tdx{FEL} [| p = q : F; C type |] ==> contr(p) = contr(q) : C
+
+\tdx{TF} T type
+\tdx{TI} tt : T
+\tdx{TE} [| p : T; c : C(tt) |] ==> c : C(p)
+\tdx{TEL} [| p = q : T; c = d : C(tt) |] ==> c = d : C(p)
+\tdx{TC} p : T ==> p = tt : T)
+\end{ttbox}
+
+\caption{Rules for types $F$ and $T$} \label{ctt-ft}
+\end{figure}
+
+
+\begin{figure}
+\begin{ttbox}
+\tdx{EqF} [| A type; a : A; b : A |] ==> Eq(A,a,b) type
+\tdx{EqFL} [| A=B; a=c: A; b=d : A |] ==> Eq(A,a,b) = Eq(B,c,d)
+\tdx{EqI} a = b : A ==> eq : Eq(A,a,b)
+\tdx{EqE} p : Eq(A,a,b) ==> a = b : A
+\tdx{EqC} p : Eq(A,a,b) ==> p = eq : Eq(A,a,b)
+\end{ttbox}
+\caption{Rules for the equality type $Eq(A,a,b)$} \label{ctt-eq}
+\end{figure}
+
+
+\begin{figure}
+\begin{ttbox}
+\tdx{replace_type} [| B = A; a : A |] ==> a : B
+\tdx{subst_eqtyparg} [| a=c : A; !!z. z:A ==> B(z) type |] ==> B(a)=B(c)
+
+\tdx{subst_prodE} [| p: Prod(A,B); a: A; !!z. z: B(a) ==> c(z): C(z)
+ |] ==> c(p`a): C(p`a)
+
+\tdx{SumIL2} [| c=a : A; d=b : B(a) |] ==> <c,d> = <a,b> : Sum(A,B)
+
+\tdx{SumE_fst} p : Sum(A,B) ==> fst(p) : A
+
+\tdx{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 {\bf long} rules; their names have the suffix~{\tt L}\@.
+Introduction and computation rules are often further suffixed with
+constructor names.
+
+Figure~\ref{ctt-equality} presents the equality rules. Most of them are
+straightforward: reflexivity, symmetry, transitivity and substitution. The
+judgement \cdx{Reduce} does not belong to Type Theory proper; it has
+been added 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 {\tt refl_red} does
+not verify that $a$ belongs to $A$.
+
+The {\tt Reduce} rules do not give rise to new theorems about the standard
+judgements. The only rule with {\tt Reduce} in a premise is
+{\tt trans_red}, whose other premise ensures that $a$ and~$b$ (and thus
+$c$) are well-typed.
+
+Figure~\ref{ctt-N} presents the rules for~$N$, the type of natural numbers.
+They include \tdx{zero_ne_succ}, which asserts $0\not=n+1$. This is
+the fourth Peano axiom and cannot be derived without universes \cite[page
+91]{martinlof84}.
+
+The constant \cdx{rec} constructs proof terms when mathematical
+induction, rule~\tdx{NE}, is applied. It can also express primitive
+recursion. Since \cdx{rec} can be applied to higher-order functions,
+it can even express Ackermann's function, which is not primitive recursive
+\cite[page~104]{thompson91}.
+
+Figure~\ref{ctt-prod} shows the rules for general product types, which
+include function types as a special case. The rules correspond to the
+predicate calculus rules for universal quantifiers and implication. They
+also permit reasoning about functions, with the rules of a typed
+$\lambda$-calculus.
+
+Figure~\ref{ctt-sum} shows the rules for general sum types, which
+include binary product types as a special case. The rules correspond to the
+predicate calculus rules for existential quantifiers and conjunction. They
+also permit reasoning about ordered pairs, with the projections
+\cdx{fst} and~\cdx{snd}.
+
+Figure~\ref{ctt-plus} shows the rules for binary sum types. They
+correspond to the predicate calculus rules for disjunction. They also
+permit reasoning about disjoint sums, with the injections \cdx{inl}
+and~\cdx{inr} and case analysis operator~\cdx{when}.
+
+Figure~\ref{ctt-ft} shows the rules for the empty and unit types, $F$
+and~$T$. They correspond to the predicate calculus rules for absurdity and
+truth.
+
+Figure~\ref{ctt-eq} shows the rules for equality types. If $a=b\in A$ is
+provable then \cdx{eq} is a canonical element of the type $Eq(A,a,b)$,
+and vice versa. These rules define extensional equality; the most recent
+versions of Type Theory use intensional equality~\cite{nordstrom90}.
+
+Figure~\ref{ctt-derived} presents the derived rules. The rule
+\tdx{subst_prodE} is derived from {\tt prodE}, and is easier to use
+in backwards proof. The rules \tdx{SumE_fst} and \tdx{SumE_snd}
+express the typing of~\cdx{fst} and~\cdx{snd}; together, they are
+roughly equivalent to~{\tt SumE} with the advantage of creating no
+parameters. Section~\ref{ctt-choice} below demonstrates these rules in a
+proof of the Axiom of 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$. The expanded form 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{ttdescription}
+\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 \tdx{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 \tdx{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 {\tt fst} and {\tt snd}.
+\end{ttdescription}
+
+
+\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, creating a huge search space. The standard tactic
+\ttindex{filt_resolve_tac}
+(see \iflabelundefined{filt_resolve_tac}{the {\em Reference Manual\/}}%
+ {\S\ref{filt_resolve_tac}})
+%
+fails for goals that are too flexible; so does the CTT tactic {\tt
+ 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{ttdescription}
+\item[\ttindexbold{test_assume_tac} $i$]
+uses {\tt 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 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{ttdescription}
+
+
+
+\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
+{\tt TSimpFun}.%
+\footnote{This should not be confused with Isabelle's main simplifier; {\tt
+ TSimpFun} is only useful for CTT and similar logics with type inference
+ rules. At present it is undocumented.}
+%
+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 \cdx{Reduce}.
+Meta-level simplification handles only definitional equality.
+\begin{ttdescription}
+\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{ttdescription}
+
+
+\section{Tactics for logical reasoning}
+Interpreting propositions as types lets CTT express statements of
+intuitionistic logic. However, Constructive Type Theory is not just another
+syntax for first-order logic. There are fundamental differences.
+
+\index{assumptions!in CTT}
+Can assumptions be deleted after use? Not every occurrence of a type
+represents a proposition, and Type Theory assumptions declare variables.
+In first-order logic, $\disj$-elimination with the assumption $P\disj Q$
+creates one subgoal assuming $P$ and another assuming $Q$, and $P\disj Q$
+can be deleted safely. 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$ when other assumptions
+refer to $z$ may render the subgoal unprovable: arguably,
+meaningless.
+
+Isabelle provides several tactics for predicate calculus reasoning in CTT:
+\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~\thydx{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{ttdescription}
+\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)$. It
+avoids information loss but obviously loops if repeated.
+
+\item[\ttindexbold{safestep_tac} $thms$ $i$]
+attacks subgoal~$i$ using formation rules and certain other `safe' rules
+(\tdx{FE}, \tdx{ProdI}, \tdx{SumE}, \tdx{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$] attempts to solve subgoal~$i$ by
+ means of 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{ttdescription}
+
+
+
+\begin{figure}
+\index{#+@{\tt\#+} symbol}
+\index{*"- symbol}
+\index{#*@{\tt\#*} symbol}
+\index{*div symbol}
+\index{*mod symbol}
+
+\index{absolute difference}
+\index{"!-"!@{\tt\char124-\char124} symbol}
+%\char124 is vertical bar. We use ! because | stopped working
+
+\begin{constants}
+ \it symbol & \it meta-type & \it priority & \it description \\
+ \tt \#* & $[i,i]\To i$ & Left 70 & multiplication \\
+ \tt div & $[i,i]\To i$ & Left 70 & division\\
+ \tt mod & $[i,i]\To i$ & Left 70 & modulus\\
+ \tt \#+ & $[i,i]\To i$ & Left 65 & addition\\
+ \tt - & $[i,i]\To i$ & Left 65 & subtraction\\
+ \verb'|-|' & $[i,i]\To i$ & Left 65 & absolute difference
+\end{constants}
+
+\begin{ttbox}
+\tdx{add_def} a#+b == rec(a, b, \%u v. succ(v))
+\tdx{diff_def} a-b == rec(b, a, \%u v. rec(v, 0, \%x y. x))
+\tdx{absdiff_def} a|-|b == (a-b) #+ (b-a)
+\tdx{mult_def} a#*b == rec(a, 0, \%u v. b #+ v)
+
+\tdx{mod_def} a mod b ==
+ rec(a, 0, \%u v. rec(succ(v) |-| b, 0, \%x y. succ(v)))
+
+\tdx{div_def} a div b ==
+ rec(a, 0, \%u v. rec(succ(u) mod b, succ(v), \%x y. v))
+
+\tdx{add_typing} [| a:N; b:N |] ==> a #+ b : N
+\tdx{addC0} b:N ==> 0 #+ b = b : N
+\tdx{addC_succ} [| a:N; b:N |] ==> succ(a) #+ b = succ(a #+ b) : N
+
+\tdx{add_assoc} [| a:N; b:N; c:N |] ==>
+ (a #+ b) #+ c = a #+ (b #+ c) : N
+
+\tdx{add_commute} [| a:N; b:N |] ==> a #+ b = b #+ a : N
+
+\tdx{mult_typing} [| a:N; b:N |] ==> a #* b : N
+\tdx{multC0} b:N ==> 0 #* b = 0 : N
+\tdx{multC_succ} [| a:N; b:N |] ==> succ(a) #* b = b #+ (a#*b) : N
+\tdx{mult_commute} [| a:N; b:N |] ==> a #* b = b #* a : N
+
+\tdx{add_mult_dist} [| a:N; b:N; c:N |] ==>
+ (a #+ b) #* c = (a #* c) #+ (b #* c) : N
+
+\tdx{mult_assoc} [| a:N; b:N; c:N |] ==>
+ (a #* b) #* c = a #* (b #* c) : N
+
+\tdx{diff_typing} [| a:N; b:N |] ==> a - b : N
+\tdx{diffC0} a:N ==> a - 0 = a : N
+\tdx{diff_0_eq_0} b:N ==> 0 - b = 0 : N
+\tdx{diff_succ_succ} [| a:N; b:N |] ==> succ(a) - succ(b) = a - b : N
+\tdx{diff_self_eq_0} a:N ==> a - a = 0 : N
+\tdx{add_inverse_diff} [| a:N; b:N; b-a=0 : N |] ==> b #+ (a-b) = a : N
+\end{ttbox}
+\caption{The theory of arithmetic} \label{ctt_arith}
+\end{figure}
+
+
+\section{A theory of arithmetic}
+\thydx{Arith} is 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 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{ttdescription}
+\item[CTT/ex/typechk.ML]
+contains simple examples of type-checking and type deduction.
+
+\item[CTT/ex/elim.ML]
+contains some examples from Martin-L\"of~\cite{martinlof84}, proved using
+{\tt pc_tac}.
+
+\item[CTT/ex/equal.ML]
+contains simple examples of rewriting.
+
+\item[CTT/ex/synth.ML]
+demonstrates the use of unknowns with some trivial examples of program
+synthesis.
+\end{ttdescription}
+
+
+\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 "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
+\tdx{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 is too flexible. It can be solved by instantiating~$\Var{A@1}$
+to any type, but most instantiations will 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 theorem}
+\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}
+Subgoal~1 is no longer flexible: we now know~$\Var{A@1}$ is the type of
+natural numbers. However, let us continue proving nontrivial subgoals.
+Subgoal~2 asks, what is the type of~0?\index{*NIO theorem}
+\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 fully determined. It is the product type
+$\prod@{x\in N}N$, which is shown as the function type $N\to N$ because
+there is no dependence on~$x$. 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 theorem}
+\begin{ttbox}
+by (assume_tac 2);
+{\out Level 4}
+{\out lam n. rec(n,0,\%x y. x) : N --> N}
+{\out 1. N type}
+\ttbreak
+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.
+
+Even if the original term is ill-typed, one can infer a type for it, but
+unprovable subgoals will be left. As an exercise, try to prove the
+following invalid goal:
+\begin{ttbox}
+Goal "lam n. rec(n, 0, \%x y. tt) : ?A";
+\end{ttbox}
+
+
+
+\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}$ stands
+for its proof term, a value of type $A$. The proof term is initially
+unknown and takes shape during the proof.
+
+Our example expresses 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)}
+\]
+By the propositions-as-types principle, this is encoded
+using~$\Sigma$ and~$+$ types. A special case of it expresses 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 the rule we must derive:
+\[ \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 begin, we bind the rule's premises --- returned by the~{\tt goal}
+command --- to the {\ML} variable~{\tt prems}.
+\begin{ttbox}
+val prems = Goal
+ "[| 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}
+The last premise involves the sum type~$\Sigma$. Since it is a premise
+rather than the assumption of a goal, it cannot be found by {\tt
+ eresolve_tac}. We could insert it (and the other atomic premise) by
+calling
+\begin{ttbox}
+cut_facts_tac prems 1;
+\end{ttbox}
+A forward proof step is more straightforward here. Let us resolve the
+$\Sigma$-elimination rule with the premises using~\ttindex{RL}. This
+inference yields one result, which we supply to {\tt
+ resolve_tac}.\index{*SumE theorem}
+\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, $x$ and~$y$. In the main goal,
+$\Var{a}$ has been instantiated with a \cdx{split} term. The
+assumption $y\in B(x) + C(x)$ is eliminated next, causing a case split and
+creating the parameter~$xa$. This inference also inserts~\cdx{when}
+into the main goal.\index{*PlusE theorem}
+\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
+a~$+$-introduction rule; since the goal assumes $xa\in B(x)$, we take the left
+injection~(\cdx{inl}).
+\index{*PlusI_inl theorem}
+\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~2 has appeared, to verify that $\sum@{x\in A}C(x)$ is a type.
+Continuing to work on subgoal~1, we apply the $\Sigma$-introduction rule.
+This instantiates the term $\Var{a@3}(x,y,xa)$; the main goal now contains
+an ordered pair, whose components are two new unknowns.%
+\index{*SumI theorem}
+\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))}
+\ttbreak
+{\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))}
+\ttbreak
+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 an example of a well-formedness subgoal~\cite{constable86}.
+Such subgoals are usually trivial; this one yields to
+\ttindex{typechk_tac}, given 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}
+This subgoal is the other case from the $+$-elimination above, and can be
+proved similarly. Quicker is to apply \ttindex{pc_tac}. The main goal
+finally gets a fully instantiated 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 the dependent types~$\Sigma$ and~$\Pi$.
+The functional takes a function~$f$ 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)$.
+
+Formally, there are three typing premises. $A$ is a type; $B$ is an
+$A$-indexed family of types; $C$ is a family of types indexed by
+$\Sigma(A,B)$. The goal is expressed using \hbox{\tt PROD f} to ensure
+that the parameter corresponding to the functional's argument is really
+called~$f$; Isabelle echoes the type using \verb|-->| because there is no
+explicit dependence upon~$f$.
+\begin{ttbox}
+val prems = Goal
+ "[| A type; !!x. x:A ==> B(x) type; \ttback
+\ttback !!z. z: (SUM x:A. B(x)) ==> C(z) type \ttback
+\ttback |] ==> ?a : PROD f: (PROD z : (SUM x:A . B(x)) . C(z)). \ttback
+\ttback (PROD x:A . PROD y:B(x) . C(<x,y>))";
+\ttbreak
+{\out Level 0}
+{\out ?a : (PROD z:SUM x:A. B(x). C(z)) -->}
+{\out (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 a chance to demonstrate \ttindex{intr_tac}. Here, the tactic
+repeatedly applies $\Pi$-introduction and proves the rather
+tiresome typing conditions.
+
+Note that $\Var{a}$ becomes instantiated to three nested
+$\lambda$-abstractions. It would be easier to read if the bound variable
+names agreed with the parameters in the subgoal. Isabelle attempts to give
+parameters the same names as corresponding bound variables in the goal, but
+this does not always work. In any event, the goal is logically correct.
+\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. !!f x y.}
+{\out [| f : PROD z:SUM x:A. B(x). C(z); x : A; y : B(x) |] ==>}
+{\out ?b7(f,x,y) : C(<x,y>)}
+\end{ttbox}
+Using $\Pi$-elimination, we solve subgoal~1 by applying the function~$f$.
+\index{*ProdE theorem}
+\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. !!f x y. [| x : A; y : B(x) |] ==> <x,y> : SUM x:A. B(x)}
+\end{ttbox}
+Finally, we verify that the argument's type is suitable 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. 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. The rules can be applied in
+countless ways, yielding many higher-order unifiers. The proof can get
+bogged down in the details. But with a careful selection of derived rules
+(recall Fig.\ts\ref{ctt-derived}) and the type-checking tactics, we can
+prove the theorem in nine steps.
+\begin{ttbox}
+val prems = Goal
+ "[| 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 h: (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
+a $\lambda$-abstraction and an ordered pair. The pair's components are
+themselves $\lambda$-abstractions and there is a subgoal for each.
+\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. !!h x.}
+{\out [| h : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>}
+{\out ?b7(h,x) : B(x)}
+\ttbreak
+{\out 2. !!h x.}
+{\out [| h : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>}
+{\out ?b8(h,x) : C(x,(lam x. ?b7(h,x)) ` x)}
+\end{ttbox}
+Subgoal~1 asks to find the choice function itself, taking $x\in A$ to some
+$\Var{b@7}(h,x)\in B(x)$. Subgoal~2 asks, given $x\in A$, for a proof
+object $\Var{b@8}(h,x)$ to witness that the choice function's argument and
+result lie in the relation~$C$. This latter task will take up most of the
+proof.
+\index{*ProdE theorem}\index{*SumE_fst theorem}\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. !!h x. x : A ==> x : A}
+{\out 2. !!h x.}
+{\out [| h : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>}
+{\out ?b8(h,x) : C(x,(lam x. fst(h ` x)) ` x)}
+\end{ttbox}
+Above, we have composed {\tt fst} with the function~$h$. Unification
+has deduced that the function must be applied to $x\in A$. We have our
+choice function.
+\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. !!h x.}
+{\out [| h : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>}
+{\out ?b8(h,x) : C(x,(lam x. fst(h ` x)) ` x)}
+\end{ttbox}
+Before we can compose {\tt snd} with~$h$, the arguments of $C$ must be
+simplified. The derived rule \tdx{replace_type} lets us replace a type
+by any equivalent type, shown below as the schematic term $\Var{A@{13}}(h,x)$:
+\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. !!h x.}
+{\out [| h : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>}
+{\out C(x,(lam x. fst(h ` x)) ` x) = ?A13(h,x)}
+\ttbreak
+{\out 2. !!h x.}
+{\out [| h : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>}
+{\out ?b8(h,x) : ?A13(h,x)}
+\end{ttbox}
+The derived rule \tdx{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. !!h x.}
+{\out [| h : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>}
+{\out (lam x. fst(h ` x)) ` x = ?c14(h,x) : ?A14(h,x)}
+\ttbreak
+{\out 2. !!h x z.}
+{\out [| h : PROD x:A. SUM y:B(x). C(x,y); x : A;}
+{\out z : ?A14(h,x) |] ==>}
+{\out C(x,z) type}
+\ttbreak
+{\out 3. !!h x.}
+{\out [| h : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>}
+{\out ?b8(h,x) : C(x,?c14(h,x))}
+\end{ttbox}
+Subgoal~1 requires simply $\beta$-contraction, which is the rule
+\tdx{ProdC}. The term $\Var{c@{14}}(h,x)$ in the last subgoal
+receives the contracted result.
+\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. !!h x.}
+{\out [| h : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>}
+{\out x : ?A15(h,x)}
+\ttbreak
+{\out 2. !!h x xa.}
+{\out [| h : PROD x:A. SUM y:B(x). C(x,y); x : A;}
+{\out xa : ?A15(h,x) |] ==>}
+{\out fst(h ` xa) : ?B15(h,x,xa)}
+\ttbreak
+{\out 3. !!h x z.}
+{\out [| h : PROD x:A. SUM y:B(x). C(x,y); x : A;}
+{\out z : ?B15(h,x,x) |] ==>}
+{\out C(x,z) type}
+\ttbreak
+{\out 4. !!h x.}
+{\out [| h : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>}
+{\out ?b8(h,x) : C(x,fst(h ` x))}
+\end{ttbox}
+Routine type-checking goals proliferate in Constructive Type Theory, but
+\ttindex{typechk_tac} quickly solves them. Note the inclusion of
+\tdx{SumE_fst} along with the premises.
+\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))}
+\ttbreak
+{\out 1. !!h x.}
+{\out [| h : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>}
+{\out ?b8(h,x) : C(x,fst(h ` x))}
+\end{ttbox}
+We are finally ready to compose {\tt snd} with~$h$.
+\index{*ProdE theorem}\index{*SumE_snd theorem}\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))}
+\ttbreak
+{\out 1. !!h x. x : A ==> x : A}
+{\out 2. !!h x. x : A ==> B(x) type}
+{\out 3. !!h 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}
+It might be instructive to compare this proof with Martin-L\"of's forward
+proof of the Axiom of Choice \cite[page~50]{martinlof84}.
+
+\index{Constructive Type Theory|)}