doc-src/Logics/CTT.tex
author wenzelm
Mon Aug 28 13:52:38 2000 +0200 (2000-08-28)
changeset 9695 ec7d7f877712
parent 7159 b009afd1ace5
child 12679 8ed660138f83
permissions -rw-r--r--
proper setup of iman.sty/extra.sty/ttbox.sty;
lcp@104
     1
%% $Id$
lcp@104
     2
\chapter{Constructive Type Theory}
lcp@314
     3
\index{Constructive Type Theory|(}
lcp@314
     4
paulson@7159
     5
\underscoreoff %this file contains _ in rule names
paulson@7159
     6
lcp@104
     7
Martin-L\"of's Constructive Type Theory \cite{martinlof84,nordstrom90} can
lcp@104
     8
be viewed at many different levels.  It is a formal system that embodies
lcp@104
     9
the principles of intuitionistic mathematics; it embodies the
lcp@104
    10
interpretation of propositions as types; it is a vehicle for deriving
lcp@314
    11
programs from proofs.  
lcp@314
    12
lcp@314
    13
Thompson's book~\cite{thompson91} gives a readable and thorough account of
lcp@314
    14
Type Theory.  Nuprl is an elaborate implementation~\cite{constable86}.
lcp@314
    15
{\sc alf} is a more recent tool that allows proof terms to be edited
lcp@314
    16
directly~\cite{alf}.
lcp@104
    17
lcp@104
    18
Isabelle's original formulation of Type Theory was a kind of sequent
lcp@104
    19
calculus, following Martin-L\"of~\cite{martinlof84}.  It included rules for
lcp@104
    20
building the context, namely variable bindings with their types.  A typical
lcp@104
    21
judgement was
lcp@104
    22
\[   a(x@1,\ldots,x@n)\in A(x@1,\ldots,x@n) \; 
lcp@104
    23
    [ x@1\in A@1, x@2\in A@2(x@1), \ldots, x@n\in A@n(x@1,\ldots,x@{n-1}) ]
lcp@104
    24
\]
lcp@104
    25
This sequent calculus was not satisfactory because assumptions like
lcp@104
    26
`suppose $A$ is a type' or `suppose $B(x)$ is a type for all $x$ in $A$'
lcp@104
    27
could not be formalized.  
lcp@104
    28
lcp@314
    29
The theory~\thydx{CTT} implements Constructive Type Theory, using
lcp@104
    30
natural deduction.  The judgement above is expressed using $\Forall$ and
lcp@104
    31
$\Imp$:
lcp@104
    32
\[ \begin{array}{r@{}l}
lcp@104
    33
     \Forall x@1\ldots x@n. &
lcp@111
    34
          \List{x@1\in A@1; 
lcp@111
    35
                x@2\in A@2(x@1); \cdots \; 
lcp@111
    36
                x@n\in A@n(x@1,\ldots,x@{n-1})} \Imp \\
lcp@104
    37
     &  \qquad\qquad a(x@1,\ldots,x@n)\in A(x@1,\ldots,x@n) 
lcp@104
    38
    \end{array}
lcp@104
    39
\]
lcp@104
    40
Assumptions can use all the judgement forms, for instance to express that
lcp@104
    41
$B$ is a family of types over~$A$:
lcp@104
    42
\[ \Forall x . x\in A \Imp B(x)\;{\rm type} \]
wenzelm@9695
    43
To justify the CTT formulation it is probably best to appeal directly to the
wenzelm@9695
    44
semantic explanations of the rules~\cite{martinlof84}, rather than to the
wenzelm@9695
    45
rules themselves.  The order of assumptions no longer matters, unlike in
wenzelm@9695
    46
standard Type Theory.  Contexts, which are typical of many modern type
wenzelm@9695
    47
theories, are difficult to represent in Isabelle.  In particular, it is
wenzelm@9695
    48
difficult to enforce that all the variables in a context are distinct.
wenzelm@9695
    49
\index{assumptions!in CTT}
lcp@104
    50
wenzelm@9695
    51
The theory does not use polymorphism.  Terms in CTT have type~\tydx{i}, the
wenzelm@9695
    52
type of individuals.  Types in CTT have type~\tydx{t}.
lcp@314
    53
lcp@314
    54
\begin{figure} \tabcolsep=1em  %wider spacing in tables
lcp@314
    55
\begin{center}
lcp@314
    56
\begin{tabular}{rrr} 
lcp@314
    57
  \it name      & \it meta-type         & \it description \\ 
lcp@314
    58
  \cdx{Type}    & $t \to prop$          & judgement form \\
lcp@314
    59
  \cdx{Eqtype}  & $[t,t]\to prop$       & judgement form\\
lcp@314
    60
  \cdx{Elem}    & $[i, t]\to prop$      & judgement form\\
lcp@314
    61
  \cdx{Eqelem}  & $[i, i, t]\to prop$   & judgement form\\
lcp@314
    62
  \cdx{Reduce}  & $[i, i]\to prop$      & extra judgement form\\[2ex]
lcp@104
    63
lcp@314
    64
  \cdx{N}       &     $t$               & natural numbers type\\
lcp@314
    65
  \cdx{0}       &     $i$               & constructor\\
lcp@314
    66
  \cdx{succ}    & $i\to i$              & constructor\\
lcp@314
    67
  \cdx{rec}     & $[i,i,[i,i]\to i]\to i$       & eliminator\\[2ex]
lcp@314
    68
  \cdx{Prod}    & $[t,i\to t]\to t$     & general product type\\
lcp@314
    69
  \cdx{lambda}  & $(i\to i)\to i$       & constructor\\[2ex]
lcp@314
    70
  \cdx{Sum}     & $[t, i\to t]\to t$    & general sum type\\
lcp@314
    71
  \cdx{pair}    & $[i,i]\to i$          & constructor\\
lcp@314
    72
  \cdx{split}   & $[i,[i,i]\to i]\to i$ & eliminator\\
lcp@314
    73
  \cdx{fst} \cdx{snd} & $i\to i$        & projections\\[2ex]
lcp@314
    74
  \cdx{inl} \cdx{inr} & $i\to i$        & constructors for $+$\\
lcp@314
    75
  \cdx{when}    & $[i,i\to i, i\to i]\to i$    & eliminator for $+$\\[2ex]
lcp@314
    76
  \cdx{Eq}      & $[t,i,i]\to t$        & equality type\\
lcp@314
    77
  \cdx{eq}      & $i$                   & constructor\\[2ex]
lcp@314
    78
  \cdx{F}       & $t$                   & empty type\\
lcp@314
    79
  \cdx{contr}   & $i\to i$              & eliminator\\[2ex]
lcp@314
    80
  \cdx{T}       & $t$                   & singleton type\\
lcp@314
    81
  \cdx{tt}      & $i$                   & constructor
lcp@314
    82
\end{tabular}
lcp@314
    83
\end{center}
wenzelm@9695
    84
\caption{The constants of CTT} \label{ctt-constants}
lcp@314
    85
\end{figure}
lcp@314
    86
lcp@314
    87
wenzelm@9695
    88
CTT supports all of Type Theory apart from list types, well-ordering types,
wenzelm@9695
    89
and universes.  Universes could be introduced {\em\`a la Tarski}, adding new
wenzelm@9695
    90
constants as names for types.  The formulation {\em\`a la Russell}, where
wenzelm@9695
    91
types denote themselves, is only possible if we identify the meta-types~{\tt
wenzelm@9695
    92
  i} and~{\tt t}.  Most published formulations of well-ordering types have
wenzelm@9695
    93
difficulties involving extensionality of functions; I suggest that you use
wenzelm@9695
    94
some other method for defining recursive types.  List types are easy to
wenzelm@9695
    95
introduce by declaring new rules.
lcp@104
    96
wenzelm@9695
    97
CTT uses the 1982 version of Type Theory, with extensional equality.  The
wenzelm@9695
    98
computation $a=b\in A$ and the equality $c\in Eq(A,a,b)$ are interchangeable.
wenzelm@9695
    99
Its rewriting tactics prove theorems of the form $a=b\in A$.  It could be
wenzelm@9695
   100
modified to have intensional equality, but rewriting tactics would have to
wenzelm@9695
   101
prove theorems of the form $c\in Eq(A,a,b)$ and the computation rules might
wenzelm@9695
   102
require a separate simplifier.
lcp@104
   103
lcp@104
   104
lcp@104
   105
\begin{figure} \tabcolsep=1em  %wider spacing in tables
wenzelm@9695
   106
\index{lambda abs@$\lambda$-abstractions!in CTT}
lcp@104
   107
\begin{center}
lcp@104
   108
\begin{tabular}{llrrr} 
lcp@314
   109
  \it symbol &\it name     &\it meta-type & \it priority & \it description \\
lcp@314
   110
  \sdx{lam} & \cdx{lambda}  & $(i\To o)\To i$ & 10 & $\lambda$-abstraction
lcp@104
   111
\end{tabular}
lcp@104
   112
\end{center}
lcp@104
   113
\subcaption{Binders} 
lcp@104
   114
lcp@104
   115
\begin{center}
wenzelm@9695
   116
\index{*"` symbol}\index{function applications!in CTT}
lcp@314
   117
\index{*"+ symbol}
lcp@104
   118
\begin{tabular}{rrrr} 
lcp@314
   119
  \it symbol & \it meta-type    & \it priority & \it description \\ 
lcp@111
   120
  \tt `         & $[i,i]\to i$  & Left 55       & function application\\
lcp@111
   121
  \tt +         & $[t,t]\to t$  & Right 30      & sum of two types
lcp@104
   122
\end{tabular}
lcp@104
   123
\end{center}
lcp@104
   124
\subcaption{Infixes}
lcp@104
   125
lcp@314
   126
\index{*"* symbol}
lcp@314
   127
\index{*"-"-"> symbol}
lcp@104
   128
\begin{center} \tt\frenchspacing
lcp@104
   129
\begin{tabular}{rrr} 
lcp@111
   130
  \it external                  & \it internal  & \it standard notation \\ 
paulson@5151
   131
  \sdx{PROD} $x$:$A$ . $B[x]$   &  Prod($A$, $\lambda x. B[x]$) &
lcp@111
   132
        \rm product $\prod@{x\in A}B[x]$ \\
paulson@5151
   133
  \sdx{SUM} $x$:$A$ . $B[x]$    & Sum($A$, $\lambda x. B[x]$) &
lcp@111
   134
        \rm sum $\sum@{x\in A}B[x]$ \\
paulson@5151
   135
  $A$ --> $B$     &  Prod($A$, $\lambda x. B$) &
lcp@111
   136
        \rm function space $A\to B$ \\
paulson@5151
   137
  $A$ * $B$       &  Sum($A$, $\lambda x. B$)  &
lcp@111
   138
        \rm binary product $A\times B$
lcp@104
   139
\end{tabular}
lcp@104
   140
\end{center}
lcp@104
   141
\subcaption{Translations} 
lcp@104
   142
lcp@314
   143
\index{*"= symbol}
lcp@104
   144
\begin{center}
lcp@104
   145
\dquotes
lcp@104
   146
\[ \begin{array}{rcl}
lcp@111
   147
prop    & = &  type " type"       \\
lcp@111
   148
        & | & type " = " type     \\
lcp@111
   149
        & | & term " : " type        \\
lcp@111
   150
        & | & term " = " term " : " type 
lcp@104
   151
\\[2ex]
lcp@111
   152
type    & = & \hbox{expression of type~$t$} \\
lcp@111
   153
        & | & "PROD~" id " : " type " . " type  \\
lcp@111
   154
        & | & "SUM~~" id " : " type " . " type 
lcp@104
   155
\\[2ex]
lcp@111
   156
term    & = & \hbox{expression of type~$i$} \\
lcp@111
   157
        & | & "lam " id~id^* " . " term   \\
lcp@111
   158
        & | & "< " term " , " term " >"
lcp@104
   159
\end{array} 
lcp@104
   160
\]
lcp@104
   161
\end{center}
lcp@104
   162
\subcaption{Grammar}
wenzelm@9695
   163
\caption{Syntax of CTT} \label{ctt-syntax}
lcp@104
   164
\end{figure}
lcp@104
   165
lcp@104
   166
%%%%\section{Generic Packages}  typedsimp.ML????????????????
lcp@104
   167
lcp@104
   168
lcp@104
   169
\section{Syntax}
lcp@284
   170
The constants are shown in Fig.\ts\ref{ctt-constants}.  The infixes include
wenzelm@9695
   171
the function application operator (sometimes called `apply'), and the 2-place
wenzelm@9695
   172
type operators.  Note that meta-level abstraction and application, $\lambda
wenzelm@9695
   173
x.b$ and $f(a)$, differ from object-level abstraction and application,
wenzelm@9695
   174
\hbox{\tt lam $x$. $b$} and $b{\tt`}a$.  A CTT function~$f$ is simply an
wenzelm@9695
   175
individual as far as Isabelle is concerned: its Isabelle type is~$i$, not say
wenzelm@9695
   176
$i\To i$.
lcp@104
   177
wenzelm@9695
   178
The notation for~CTT (Fig.\ts\ref{ctt-syntax}) is based on that of Nordstr\"om
wenzelm@9695
   179
et al.~\cite{nordstrom90}.  The empty type is called $F$ and the one-element
wenzelm@9695
   180
type is $T$; other finite types are built as $T+T+T$, etc.
lcp@314
   181
lcp@314
   182
\index{*SUM symbol}\index{*PROD symbol}
paulson@6072
   183
Quantification is expressed by sums $\sum@{x\in A}B[x]$ and
lcp@314
   184
products $\prod@{x\in A}B[x]$.  Instead of {\tt Sum($A$,$B$)} and {\tt
paulson@6072
   185
  Prod($A$,$B$)} we may write \hbox{\tt SUM $x$:$A$.\ $B[x]$} and \hbox{\tt
paulson@6072
   186
  PROD $x$:$A$.\ $B[x]$}.  For example, we may write
lcp@104
   187
\begin{ttbox}
lcp@284
   188
SUM y:B. PROD x:A. C(x,y)   {\rm for}   Sum(B, \%y. Prod(A, \%x. C(x,y)))
lcp@104
   189
\end{ttbox}
lcp@104
   190
The special cases as \hbox{\tt$A$*$B$} and \hbox{\tt$A$-->$B$} abbreviate
lcp@104
   191
general sums and products over a constant family.\footnote{Unlike normal
lcp@104
   192
infix operators, {\tt*} and {\tt-->} merely define abbreviations; there are
lcp@104
   193
no constants~{\tt op~*} and~\hbox{\tt op~-->}.}  Isabelle accepts these
lcp@104
   194
abbreviations in parsing and uses them whenever possible for printing.
lcp@104
   195
lcp@104
   196
lcp@104
   197
\begin{figure} 
lcp@104
   198
\begin{ttbox}
lcp@314
   199
\tdx{refl_type}         A type ==> A = A
lcp@314
   200
\tdx{refl_elem}         a : A ==> a = a : A
lcp@104
   201
lcp@314
   202
\tdx{sym_type}          A = B ==> B = A
lcp@314
   203
\tdx{sym_elem}          a = b : A ==> b = a : A
lcp@104
   204
lcp@314
   205
\tdx{trans_type}        [| A = B;  B = C |] ==> A = C
lcp@314
   206
\tdx{trans_elem}        [| a = b : A;  b = c : A |] ==> a = c : A
lcp@104
   207
lcp@314
   208
\tdx{equal_types}       [| a : A;  A = B |] ==> a : B
lcp@314
   209
\tdx{equal_typesL}      [| a = b : A;  A = B |] ==> a = b : B
lcp@104
   210
lcp@314
   211
\tdx{subst_type}        [| a : A;  !!z. z:A ==> B(z) type |] ==> B(a) type
lcp@314
   212
\tdx{subst_typeL}       [| a = c : A;  !!z. z:A ==> B(z) = D(z) 
lcp@104
   213
                  |] ==> B(a) = D(c)
lcp@104
   214
lcp@314
   215
\tdx{subst_elem}        [| a : A;  !!z. z:A ==> b(z):B(z) |] ==> b(a):B(a)
lcp@314
   216
\tdx{subst_elemL}       [| a = c : A;  !!z. z:A ==> b(z) = d(z) : B(z) 
lcp@104
   217
                  |] ==> b(a) = d(c) : B(a)
lcp@104
   218
lcp@314
   219
\tdx{refl_red}          Reduce(a,a)
lcp@314
   220
\tdx{red_if_equal}      a = b : A ==> Reduce(a,b)
lcp@314
   221
\tdx{trans_red}         [| a = b : A;  Reduce(b,c) |] ==> a = c : A
lcp@104
   222
\end{ttbox}
lcp@104
   223
\caption{General equality rules} \label{ctt-equality}
lcp@104
   224
\end{figure}
lcp@104
   225
lcp@104
   226
lcp@104
   227
\begin{figure} 
lcp@104
   228
\begin{ttbox}
lcp@314
   229
\tdx{NF}        N type
lcp@104
   230
lcp@314
   231
\tdx{NI0}       0 : N
lcp@314
   232
\tdx{NI_succ}   a : N ==> succ(a) : N
lcp@314
   233
\tdx{NI_succL}  a = b : N ==> succ(a) = succ(b) : N
lcp@104
   234
lcp@314
   235
\tdx{NE}        [| p: N;  a: C(0);  
lcp@104
   236
             !!u v. [| u: N; v: C(u) |] ==> b(u,v): C(succ(u)) 
paulson@5151
   237
          |] ==> rec(p, a, \%u v. b(u,v)) : C(p)
lcp@104
   238
lcp@314
   239
\tdx{NEL}       [| p = q : N;  a = c : C(0);  
lcp@104
   240
             !!u v. [| u: N; v: C(u) |] ==> b(u,v)=d(u,v): C(succ(u))
paulson@5151
   241
          |] ==> rec(p, a, \%u v. b(u,v)) = rec(q,c,d) : C(p)
lcp@104
   242
lcp@314
   243
\tdx{NC0}       [| a: C(0);  
lcp@104
   244
             !!u v. [| u: N; v: C(u) |] ==> b(u,v): C(succ(u))
paulson@5151
   245
          |] ==> rec(0, a, \%u v. b(u,v)) = a : C(0)
lcp@104
   246
lcp@314
   247
\tdx{NC_succ}   [| p: N;  a: C(0);  
lcp@104
   248
             !!u v. [| u: N; v: C(u) |] ==> b(u,v): C(succ(u)) 
paulson@5151
   249
          |] ==> rec(succ(p), a, \%u v. b(u,v)) =
paulson@5151
   250
                 b(p, rec(p, a, \%u v. b(u,v))) : C(succ(p))
lcp@104
   251
lcp@314
   252
\tdx{zero_ne_succ}      [| a: N;  0 = succ(a) : N |] ==> 0: F
lcp@104
   253
\end{ttbox}
lcp@104
   254
\caption{Rules for type~$N$} \label{ctt-N}
lcp@104
   255
\end{figure}
lcp@104
   256
lcp@104
   257
lcp@104
   258
\begin{figure} 
lcp@104
   259
\begin{ttbox}
paulson@5151
   260
\tdx{ProdF}     [| A type; !!x. x:A ==> B(x) type |] ==> PROD x:A. B(x) type
lcp@314
   261
\tdx{ProdFL}    [| A = C;  !!x. x:A ==> B(x) = D(x) |] ==> 
paulson@5151
   262
          PROD x:A. B(x) = PROD x:C. D(x)
lcp@104
   263
lcp@314
   264
\tdx{ProdI}     [| A type;  !!x. x:A ==> b(x):B(x)
paulson@5151
   265
          |] ==> lam x. b(x) : PROD x:A. B(x)
lcp@314
   266
\tdx{ProdIL}    [| A type;  !!x. x:A ==> b(x) = c(x) : B(x)
paulson@5151
   267
          |] ==> lam x. b(x) = lam x. c(x) : PROD x:A. B(x)
lcp@104
   268
paulson@5151
   269
\tdx{ProdE}     [| p : PROD x:A. B(x);  a : A |] ==> p`a : B(a)
paulson@5151
   270
\tdx{ProdEL}    [| p=q: PROD x:A. B(x);  a=b : A |] ==> p`a = q`b : B(a)
lcp@104
   271
lcp@314
   272
\tdx{ProdC}     [| a : A;  !!x. x:A ==> b(x) : B(x)
paulson@5151
   273
          |] ==> (lam x. b(x)) ` a = b(a) : B(a)
lcp@104
   274
paulson@5151
   275
\tdx{ProdC2}    p : PROD x:A. B(x) ==> (lam x. p`x) = p : PROD x:A. B(x)
lcp@104
   276
\end{ttbox}
lcp@314
   277
\caption{Rules for the product type $\prod\sb{x\in A}B[x]$} \label{ctt-prod}
lcp@104
   278
\end{figure}
lcp@104
   279
lcp@104
   280
lcp@104
   281
\begin{figure} 
lcp@104
   282
\begin{ttbox}
paulson@5151
   283
\tdx{SumF}      [| A type;  !!x. x:A ==> B(x) type |] ==> SUM x:A. B(x) type
lcp@314
   284
\tdx{SumFL}     [| A = C;  !!x. x:A ==> B(x) = D(x) 
paulson@5151
   285
          |] ==> SUM x:A. B(x) = SUM x:C. D(x)
lcp@104
   286
paulson@5151
   287
\tdx{SumI}      [| a : A;  b : B(a) |] ==> <a,b> : SUM x:A. B(x)
paulson@5151
   288
\tdx{SumIL}     [| a=c:A;  b=d:B(a) |] ==> <a,b> = <c,d> : SUM x:A. B(x)
lcp@104
   289
paulson@5151
   290
\tdx{SumE}      [| p: SUM x:A. B(x);  
lcp@104
   291
             !!x y. [| x:A; y:B(x) |] ==> c(x,y): C(<x,y>) 
paulson@5151
   292
          |] ==> split(p, \%x y. c(x,y)) : C(p)
lcp@104
   293
paulson@5151
   294
\tdx{SumEL}     [| p=q : SUM x:A. B(x); 
lcp@104
   295
             !!x y. [| x:A; y:B(x) |] ==> c(x,y)=d(x,y): C(<x,y>)
paulson@5151
   296
          |] ==> split(p, \%x y. c(x,y)) = split(q, \%x y. d(x,y)) : C(p)
lcp@104
   297
lcp@314
   298
\tdx{SumC}      [| a: A;  b: B(a);
lcp@104
   299
             !!x y. [| x:A; y:B(x) |] ==> c(x,y): C(<x,y>)
paulson@5151
   300
          |] ==> split(<a,b>, \%x y. c(x,y)) = c(a,b) : C(<a,b>)
lcp@104
   301
paulson@5151
   302
\tdx{fst_def}   fst(a) == split(a, \%x y. x)
paulson@5151
   303
\tdx{snd_def}   snd(a) == split(a, \%x y. y)
lcp@104
   304
\end{ttbox}
lcp@314
   305
\caption{Rules for the sum type $\sum\sb{x\in A}B[x]$} \label{ctt-sum}
lcp@104
   306
\end{figure}
lcp@104
   307
lcp@104
   308
lcp@104
   309
\begin{figure} 
lcp@104
   310
\begin{ttbox}
lcp@314
   311
\tdx{PlusF}       [| A type;  B type |] ==> A+B type
lcp@314
   312
\tdx{PlusFL}      [| A = C;  B = D |] ==> A+B = C+D
lcp@104
   313
lcp@314
   314
\tdx{PlusI_inl}   [| a : A;  B type |] ==> inl(a) : A+B
lcp@314
   315
\tdx{PlusI_inlL}  [| a = c : A;  B type |] ==> inl(a) = inl(c) : A+B
lcp@104
   316
lcp@314
   317
\tdx{PlusI_inr}   [| A type;  b : B |] ==> inr(b) : A+B
lcp@314
   318
\tdx{PlusI_inrL}  [| A type;  b = d : B |] ==> inr(b) = inr(d) : A+B
lcp@104
   319
lcp@314
   320
\tdx{PlusE}     [| p: A+B;
lcp@104
   321
             !!x. x:A ==> c(x): C(inl(x));  
lcp@104
   322
             !!y. y:B ==> d(y): C(inr(y))
paulson@5151
   323
          |] ==> when(p, \%x. c(x), \%y. d(y)) : C(p)
lcp@104
   324
lcp@314
   325
\tdx{PlusEL}    [| p = q : A+B;
lcp@104
   326
             !!x. x: A ==> c(x) = e(x) : C(inl(x));   
lcp@104
   327
             !!y. y: B ==> d(y) = f(y) : C(inr(y))
paulson@5151
   328
          |] ==> when(p, \%x. c(x), \%y. d(y)) = 
paulson@5151
   329
                 when(q, \%x. e(x), \%y. f(y)) : C(p)
lcp@104
   330
lcp@314
   331
\tdx{PlusC_inl} [| a: A;
lcp@104
   332
             !!x. x:A ==> c(x): C(inl(x));  
lcp@104
   333
             !!y. y:B ==> d(y): C(inr(y))
paulson@5151
   334
          |] ==> when(inl(a), \%x. c(x), \%y. d(y)) = c(a) : C(inl(a))
lcp@104
   335
lcp@314
   336
\tdx{PlusC_inr} [| b: B;
lcp@104
   337
             !!x. x:A ==> c(x): C(inl(x));  
lcp@104
   338
             !!y. y:B ==> d(y): C(inr(y))
paulson@5151
   339
          |] ==> when(inr(b), \%x. c(x), \%y. d(y)) = d(b) : C(inr(b))
lcp@104
   340
\end{ttbox}
lcp@104
   341
\caption{Rules for the binary sum type $A+B$} \label{ctt-plus}
lcp@104
   342
\end{figure}
lcp@104
   343
lcp@104
   344
lcp@104
   345
\begin{figure} 
lcp@104
   346
\begin{ttbox}
lcp@314
   347
\tdx{FF}        F type
lcp@314
   348
\tdx{FE}        [| p: F;  C type |] ==> contr(p) : C
lcp@314
   349
\tdx{FEL}       [| p = q : F;  C type |] ==> contr(p) = contr(q) : C
lcp@104
   350
lcp@314
   351
\tdx{TF}        T type
lcp@314
   352
\tdx{TI}        tt : T
lcp@314
   353
\tdx{TE}        [| p : T;  c : C(tt) |] ==> c : C(p)
lcp@314
   354
\tdx{TEL}       [| p = q : T;  c = d : C(tt) |] ==> c = d : C(p)
lcp@314
   355
\tdx{TC}        p : T ==> p = tt : T)
lcp@104
   356
\end{ttbox}
lcp@104
   357
lcp@314
   358
\caption{Rules for types $F$ and $T$} \label{ctt-ft}
lcp@104
   359
\end{figure}
lcp@104
   360
lcp@104
   361
lcp@104
   362
\begin{figure} 
lcp@104
   363
\begin{ttbox}
lcp@314
   364
\tdx{EqF}       [| A type;  a : A;  b : A |] ==> Eq(A,a,b) type
lcp@314
   365
\tdx{EqFL}      [| A=B;  a=c: A;  b=d : A |] ==> Eq(A,a,b) = Eq(B,c,d)
lcp@314
   366
\tdx{EqI}       a = b : A ==> eq : Eq(A,a,b)
lcp@314
   367
\tdx{EqE}       p : Eq(A,a,b) ==> a = b : A
lcp@314
   368
\tdx{EqC}       p : Eq(A,a,b) ==> p = eq : Eq(A,a,b)
lcp@314
   369
\end{ttbox}
lcp@314
   370
\caption{Rules for the equality type $Eq(A,a,b)$} \label{ctt-eq}
lcp@314
   371
\end{figure}
lcp@104
   372
lcp@314
   373
lcp@314
   374
\begin{figure} 
lcp@314
   375
\begin{ttbox}
lcp@314
   376
\tdx{replace_type}    [| B = A;  a : A |] ==> a : B
lcp@314
   377
\tdx{subst_eqtyparg}  [| a=c : A;  !!z. z:A ==> B(z) type |] ==> B(a)=B(c)
lcp@314
   378
lcp@314
   379
\tdx{subst_prodE}     [| p: Prod(A,B);  a: A;  !!z. z: B(a) ==> c(z): C(z)
lcp@104
   380
                |] ==> c(p`a): C(p`a)
lcp@104
   381
lcp@314
   382
\tdx{SumIL2}    [| c=a : A;  d=b : B(a) |] ==> <c,d> = <a,b> : Sum(A,B)
lcp@104
   383
lcp@314
   384
\tdx{SumE_fst}  p : Sum(A,B) ==> fst(p) : A
lcp@104
   385
lcp@314
   386
\tdx{SumE_snd}  [| p: Sum(A,B);  A type;  !!x. x:A ==> B(x) type
lcp@104
   387
          |] ==> snd(p) : B(fst(p))
lcp@104
   388
\end{ttbox}
lcp@104
   389
wenzelm@9695
   390
\caption{Derived rules for CTT} \label{ctt-derived}
lcp@104
   391
\end{figure}
lcp@104
   392
lcp@104
   393
lcp@104
   394
\section{Rules of inference}
lcp@104
   395
The rules obey the following naming conventions.  Type formation rules have
lcp@104
   396
the suffix~{\tt F}\@.  Introduction rules have the suffix~{\tt I}\@.
lcp@104
   397
Elimination rules have the suffix~{\tt E}\@.  Computation rules, which
lcp@104
   398
describe the reduction of eliminators, have the suffix~{\tt C}\@.  The
lcp@104
   399
equality versions of the rules (which permit reductions on subterms) are
lcp@333
   400
called {\bf long} rules; their names have the suffix~{\tt L}\@.
lcp@333
   401
Introduction and computation rules are often further suffixed with
lcp@104
   402
constructor names.
lcp@104
   403
lcp@314
   404
Figure~\ref{ctt-equality} presents the equality rules.  Most of them are
lcp@314
   405
straightforward: reflexivity, symmetry, transitivity and substitution.  The
lcp@314
   406
judgement \cdx{Reduce} does not belong to Type Theory proper; it has
lcp@314
   407
been added to implement rewriting.  The judgement ${\tt Reduce}(a,b)$ holds
lcp@314
   408
when $a=b:A$ holds.  It also holds when $a$ and $b$ are syntactically
lcp@314
   409
identical, even if they are ill-typed, because rule {\tt refl_red} does
lcp@314
   410
not verify that $a$ belongs to $A$.  
lcp@314
   411
lcp@314
   412
The {\tt Reduce} rules do not give rise to new theorems about the standard
lcp@314
   413
judgements.  The only rule with {\tt Reduce} in a premise is
lcp@314
   414
{\tt trans_red}, whose other premise ensures that $a$ and~$b$ (and thus
lcp@314
   415
$c$) are well-typed.
lcp@314
   416
lcp@314
   417
Figure~\ref{ctt-N} presents the rules for~$N$, the type of natural numbers.
lcp@314
   418
They include \tdx{zero_ne_succ}, which asserts $0\not=n+1$.  This is
lcp@314
   419
the fourth Peano axiom and cannot be derived without universes \cite[page
lcp@314
   420
91]{martinlof84}.  
lcp@314
   421
lcp@314
   422
The constant \cdx{rec} constructs proof terms when mathematical
lcp@314
   423
induction, rule~\tdx{NE}, is applied.  It can also express primitive
lcp@314
   424
recursion.  Since \cdx{rec} can be applied to higher-order functions,
lcp@314
   425
it can even express Ackermann's function, which is not primitive recursive
lcp@314
   426
\cite[page~104]{thompson91}.
lcp@104
   427
lcp@314
   428
Figure~\ref{ctt-prod} shows the rules for general product types, which
lcp@314
   429
include function types as a special case.  The rules correspond to the
lcp@314
   430
predicate calculus rules for universal quantifiers and implication.  They
lcp@314
   431
also permit reasoning about functions, with the rules of a typed
lcp@314
   432
$\lambda$-calculus.
lcp@314
   433
lcp@314
   434
Figure~\ref{ctt-sum} shows the rules for general sum types, which
lcp@314
   435
include binary product types as a special case.  The rules correspond to the
lcp@314
   436
predicate calculus rules for existential quantifiers and conjunction.  They
lcp@314
   437
also permit reasoning about ordered pairs, with the projections
lcp@314
   438
\cdx{fst} and~\cdx{snd}.
lcp@314
   439
lcp@314
   440
Figure~\ref{ctt-plus} shows the rules for binary sum types.  They
lcp@314
   441
correspond to the predicate calculus rules for disjunction.  They also
lcp@314
   442
permit reasoning about disjoint sums, with the injections \cdx{inl}
lcp@314
   443
and~\cdx{inr} and case analysis operator~\cdx{when}.
lcp@104
   444
lcp@314
   445
Figure~\ref{ctt-ft} shows the rules for the empty and unit types, $F$
lcp@314
   446
and~$T$.  They correspond to the predicate calculus rules for absurdity and
lcp@314
   447
truth.
lcp@314
   448
lcp@314
   449
Figure~\ref{ctt-eq} shows the rules for equality types.  If $a=b\in A$ is
lcp@314
   450
provable then \cdx{eq} is a canonical element of the type $Eq(A,a,b)$,
lcp@314
   451
and vice versa.  These rules define extensional equality; the most recent
lcp@314
   452
versions of Type Theory use intensional equality~\cite{nordstrom90}.
lcp@314
   453
lcp@314
   454
Figure~\ref{ctt-derived} presents the derived rules.  The rule
lcp@314
   455
\tdx{subst_prodE} is derived from {\tt prodE}, and is easier to use
lcp@314
   456
in backwards proof.  The rules \tdx{SumE_fst} and \tdx{SumE_snd}
lcp@314
   457
express the typing of~\cdx{fst} and~\cdx{snd}; together, they are
lcp@314
   458
roughly equivalent to~{\tt SumE} with the advantage of creating no
lcp@314
   459
parameters.  Section~\ref{ctt-choice} below demonstrates these rules in a
lcp@314
   460
proof of the Axiom of Choice.
lcp@104
   461
lcp@104
   462
All the rules are given in $\eta$-expanded form.  For instance, every
paulson@5151
   463
occurrence of $\lambda u\,v. b(u,v)$ could be abbreviated to~$b$ in the
lcp@314
   464
rules for~$N$.  The expanded form permits Isabelle to preserve bound
lcp@314
   465
variable names during backward proof.  Names of bound variables in the
lcp@314
   466
conclusion (here, $u$ and~$v$) are matched with corresponding bound
lcp@314
   467
variables in the premises.
lcp@104
   468
lcp@104
   469
lcp@104
   470
\section{Rule lists}
lcp@104
   471
The Type Theory tactics provide rewriting, type inference, and logical
lcp@104
   472
reasoning.  Many proof procedures work by repeatedly resolving certain Type
wenzelm@9695
   473
Theory rules against a proof state.  CTT defines lists --- each with
lcp@104
   474
type
lcp@104
   475
\hbox{\tt thm list} --- of related rules. 
lcp@314
   476
\begin{ttdescription}
lcp@104
   477
\item[\ttindexbold{form_rls}] 
lcp@104
   478
contains formation rules for the types $N$, $\Pi$, $\Sigma$, $+$, $Eq$,
lcp@104
   479
$F$, and $T$.
lcp@104
   480
lcp@104
   481
\item[\ttindexbold{formL_rls}] 
lcp@104
   482
contains long formation rules for $\Pi$, $\Sigma$, $+$, and $Eq$.  (For
lcp@314
   483
other types use \tdx{refl_type}.)
lcp@104
   484
lcp@104
   485
\item[\ttindexbold{intr_rls}] 
lcp@104
   486
contains introduction rules for the types $N$, $\Pi$, $\Sigma$, $+$, and
lcp@104
   487
$T$.
lcp@104
   488
lcp@104
   489
\item[\ttindexbold{intrL_rls}] 
lcp@104
   490
contains long introduction rules for $N$, $\Pi$, $\Sigma$, and $+$.  (For
lcp@314
   491
$T$ use \tdx{refl_elem}.)
lcp@104
   492
lcp@104
   493
\item[\ttindexbold{elim_rls}] 
lcp@104
   494
contains elimination rules for the types $N$, $\Pi$, $\Sigma$, $+$, and
lcp@104
   495
$F$.  The rules for $Eq$ and $T$ are omitted because they involve no
lcp@104
   496
eliminator.
lcp@104
   497
lcp@104
   498
\item[\ttindexbold{elimL_rls}] 
lcp@104
   499
contains long elimination rules for $N$, $\Pi$, $\Sigma$, $+$, and $F$.
lcp@104
   500
lcp@104
   501
\item[\ttindexbold{comp_rls}] 
lcp@104
   502
contains computation rules for the types $N$, $\Pi$, $\Sigma$, and $+$.
lcp@104
   503
Those for $Eq$ and $T$ involve no eliminator.
lcp@104
   504
lcp@104
   505
\item[\ttindexbold{basic_defs}] 
lcp@314
   506
contains the definitions of {\tt fst} and {\tt snd}.  
lcp@314
   507
\end{ttdescription}
lcp@104
   508
lcp@104
   509
lcp@104
   510
\section{Tactics for subgoal reordering}
lcp@104
   511
\begin{ttbox}
lcp@104
   512
test_assume_tac : int -> tactic
lcp@104
   513
typechk_tac     : thm list -> tactic
lcp@104
   514
equal_tac       : thm list -> tactic
lcp@104
   515
intr_tac        : thm list -> tactic
lcp@104
   516
\end{ttbox}
wenzelm@9695
   517
Blind application of CTT rules seldom leads to a proof.  The elimination
lcp@104
   518
rules, especially, create subgoals containing new unknowns.  These subgoals
lcp@333
   519
unify with anything, creating a huge search space.  The standard tactic
wenzelm@9695
   520
\ttindex{filt_resolve_tac}
lcp@314
   521
(see \iflabelundefined{filt_resolve_tac}{the {\em Reference Manual\/}}%
lcp@314
   522
        {\S\ref{filt_resolve_tac}})
lcp@314
   523
%
wenzelm@9695
   524
fails for goals that are too flexible; so does the CTT tactic {\tt
lcp@314
   525
  test_assume_tac}.  Used with the tactical \ttindex{REPEAT_FIRST} they
lcp@314
   526
achieve a simple kind of subgoal reordering: the less flexible subgoals are
lcp@314
   527
attempted first.  Do some single step proofs, or study the examples below,
lcp@314
   528
to see why this is necessary.
lcp@314
   529
\begin{ttdescription}
lcp@104
   530
\item[\ttindexbold{test_assume_tac} $i$] 
lcp@314
   531
uses {\tt assume_tac} to solve the subgoal by assumption, but only if
lcp@104
   532
subgoal~$i$ has the form $a\in A$ and the head of $a$ is not an unknown.
lcp@104
   533
Otherwise, it fails.
lcp@104
   534
lcp@104
   535
\item[\ttindexbold{typechk_tac} $thms$] 
lcp@104
   536
uses $thms$ with formation, introduction, and elimination rules to check
lcp@104
   537
the typing of constructions.  It is designed to solve goals of the form
lcp@975
   538
$a\in \Var{A}$, where $a$ is rigid and $\Var{A}$ is flexible; thus it
lcp@975
   539
performs type inference.  The tactic can also solve goals of
lcp@104
   540
the form $A\;\rm type$.
lcp@104
   541
lcp@104
   542
\item[\ttindexbold{equal_tac} $thms$]
lcp@104
   543
uses $thms$ with the long introduction and elimination rules to solve goals
lcp@104
   544
of the form $a=b\in A$, where $a$ is rigid.  It is intended for deriving
lcp@104
   545
the long rules for defined constants such as the arithmetic operators.  The
paulson@6170
   546
tactic can also perform type-checking.
lcp@104
   547
lcp@104
   548
\item[\ttindexbold{intr_tac} $thms$]
lcp@104
   549
uses $thms$ with the introduction rules to break down a type.  It is
lcp@104
   550
designed for goals like $\Var{a}\in A$ where $\Var{a}$ is flexible and $A$
lcp@104
   551
rigid.  These typically arise when trying to prove a proposition~$A$,
lcp@104
   552
expressed as a type.
lcp@314
   553
\end{ttdescription}
lcp@104
   554
lcp@104
   555
lcp@104
   556
lcp@104
   557
\section{Rewriting tactics}
lcp@104
   558
\begin{ttbox}
lcp@104
   559
rew_tac     : thm list -> tactic
lcp@104
   560
hyp_rew_tac : thm list -> tactic
lcp@104
   561
\end{ttbox}
lcp@104
   562
Object-level simplification is accomplished through proof, using the {\tt
lcp@314
   563
  CTT} equality rules and the built-in rewriting functor
lcp@314
   564
{\tt TSimpFun}.%
lcp@314
   565
\footnote{This should not be confused with Isabelle's main simplifier; {\tt
wenzelm@9695
   566
    TSimpFun} is only useful for CTT and similar logics with type inference
wenzelm@9695
   567
  rules.  At present it is undocumented.}
lcp@314
   568
%
lcp@314
   569
The rewrites include the computation rules and other equations.  The long
lcp@314
   570
versions of the other rules permit rewriting of subterms and subtypes.
lcp@314
   571
Also used are transitivity and the extra judgement form \cdx{Reduce}.
lcp@104
   572
Meta-level simplification handles only definitional equality.
lcp@314
   573
\begin{ttdescription}
lcp@104
   574
\item[\ttindexbold{rew_tac} $thms$]
lcp@104
   575
applies $thms$ and the computation rules as left-to-right rewrites.  It
lcp@104
   576
solves the goal $a=b\in A$ by rewriting $a$ to $b$.  If $b$ is an unknown
lcp@104
   577
then it is assigned the rewritten form of~$a$.  All subgoals are rewritten.
lcp@104
   578
lcp@104
   579
\item[\ttindexbold{hyp_rew_tac} $thms$]
lcp@104
   580
is like {\tt rew_tac}, but includes as rewrites any equations present in
lcp@104
   581
the assumptions.
lcp@314
   582
\end{ttdescription}
lcp@104
   583
lcp@104
   584
lcp@104
   585
\section{Tactics for logical reasoning}
wenzelm@9695
   586
Interpreting propositions as types lets CTT express statements of
wenzelm@9695
   587
intuitionistic logic.  However, Constructive Type Theory is not just another
wenzelm@9695
   588
syntax for first-order logic.  There are fundamental differences.
lcp@104
   589
wenzelm@9695
   590
\index{assumptions!in CTT}
lcp@314
   591
Can assumptions be deleted after use?  Not every occurrence of a type
lcp@314
   592
represents a proposition, and Type Theory assumptions declare variables.
lcp@104
   593
In first-order logic, $\disj$-elimination with the assumption $P\disj Q$
lcp@104
   594
creates one subgoal assuming $P$ and another assuming $Q$, and $P\disj Q$
lcp@314
   595
can be deleted safely.  In Type Theory, $+$-elimination with the assumption
lcp@314
   596
$z\in A+B$ creates one subgoal assuming $x\in A$ and another assuming $y\in
lcp@314
   597
B$ (for arbitrary $x$ and $y$).  Deleting $z\in A+B$ when other assumptions
lcp@314
   598
refer to $z$ may render the subgoal unprovable: arguably,
lcp@314
   599
meaningless.
lcp@314
   600
wenzelm@9695
   601
Isabelle provides several tactics for predicate calculus reasoning in CTT:
lcp@104
   602
\begin{ttbox}
lcp@104
   603
mp_tac       : int -> tactic
lcp@104
   604
add_mp_tac   : int -> tactic
lcp@104
   605
safestep_tac : thm list -> int -> tactic
lcp@104
   606
safe_tac     : thm list -> int -> tactic
lcp@104
   607
step_tac     : thm list -> int -> tactic
lcp@104
   608
pc_tac       : thm list -> int -> tactic
lcp@104
   609
\end{ttbox}
lcp@104
   610
These are loosely based on the intuitionistic proof procedures
lcp@314
   611
of~\thydx{FOL}.  For the reasons discussed above, a rule that is safe for
paulson@6170
   612
propositional reasoning may be unsafe for type-checking; thus, some of the
lcp@314
   613
`safe' tactics are misnamed.
lcp@314
   614
\begin{ttdescription}
lcp@104
   615
\item[\ttindexbold{mp_tac} $i$] 
lcp@104
   616
searches in subgoal~$i$ for assumptions of the form $f\in\Pi(A,B)$ and
lcp@104
   617
$a\in A$, where~$A$ may be found by unification.  It replaces
lcp@104
   618
$f\in\Pi(A,B)$ by $z\in B(a)$, where~$z$ is a new parameter.  The tactic
lcp@104
   619
can produce multiple outcomes for each suitable pair of assumptions.  In
lcp@104
   620
short, {\tt mp_tac} performs Modus Ponens among the assumptions.
lcp@104
   621
lcp@104
   622
\item[\ttindexbold{add_mp_tac} $i$]
lcp@314
   623
is like {\tt mp_tac}~$i$ but retains the assumption $f\in\Pi(A,B)$.  It
lcp@314
   624
avoids information loss but obviously loops if repeated.
lcp@104
   625
lcp@104
   626
\item[\ttindexbold{safestep_tac} $thms$ $i$]
lcp@104
   627
attacks subgoal~$i$ using formation rules and certain other `safe' rules
lcp@333
   628
(\tdx{FE}, \tdx{ProdI}, \tdx{SumE}, \tdx{PlusE}), calling
lcp@104
   629
{\tt mp_tac} when appropriate.  It also uses~$thms$,
lcp@104
   630
which are typically premises of the rule being derived.
lcp@104
   631
lcp@314
   632
\item[\ttindexbold{safe_tac} $thms$ $i$] attempts to solve subgoal~$i$ by
lcp@314
   633
  means of backtracking, using {\tt safestep_tac}.
lcp@104
   634
lcp@104
   635
\item[\ttindexbold{step_tac} $thms$ $i$]
lcp@104
   636
tries to reduce subgoal~$i$ using {\tt safestep_tac}, then tries unsafe
lcp@104
   637
rules.  It may produce multiple outcomes.
lcp@104
   638
lcp@104
   639
\item[\ttindexbold{pc_tac} $thms$ $i$]
lcp@104
   640
tries to solve subgoal~$i$ by backtracking, using {\tt step_tac}.
lcp@314
   641
\end{ttdescription}
lcp@104
   642
lcp@104
   643
lcp@104
   644
lcp@104
   645
\begin{figure} 
lcp@314
   646
\index{#+@{\tt\#+} symbol}
lcp@314
   647
\index{*"- symbol}
lcp@314
   648
\index{*"|"-"| symbol}
lcp@314
   649
\index{#*@{\tt\#*} symbol}
lcp@314
   650
\index{*div symbol}
lcp@314
   651
\index{*mod symbol}
lcp@314
   652
\begin{constants}
lcp@314
   653
  \it symbol  & \it meta-type & \it priority & \it description \\ 
lcp@314
   654
  \tt \#*       & $[i,i]\To i$  &  Left 70      & multiplication \\
lcp@314
   655
  \tt div       & $[i,i]\To i$  &  Left 70      & division\\
lcp@314
   656
  \tt mod       & $[i,i]\To i$  &  Left 70      & modulus\\
lcp@314
   657
  \tt \#+       & $[i,i]\To i$  &  Left 65      & addition\\
lcp@314
   658
  \tt -         & $[i,i]\To i$  &  Left 65      & subtraction\\
lcp@314
   659
  \verb'|-|'    & $[i,i]\To i$  &  Left 65      & absolute difference
lcp@314
   660
\end{constants}
lcp@104
   661
lcp@104
   662
\begin{ttbox}
paulson@5151
   663
\tdx{add_def}           a#+b  == rec(a, b, \%u v. succ(v))  
paulson@5151
   664
\tdx{diff_def}          a-b   == rec(b, a, \%u v. rec(v, 0, \%x y. x))  
lcp@314
   665
\tdx{absdiff_def}       a|-|b == (a-b) #+ (b-a)  
lcp@314
   666
\tdx{mult_def}          a#*b  == rec(a, 0, \%u v. b #+ v)  
lcp@314
   667
lcp@314
   668
\tdx{mod_def}           a mod b ==
paulson@5151
   669
                  rec(a, 0, \%u v. rec(succ(v) |-| b, 0, \%x y. succ(v)))
lcp@104
   670
lcp@314
   671
\tdx{div_def}           a div b ==
paulson@5151
   672
                  rec(a, 0, \%u v. rec(succ(u) mod b, succ(v), \%x y. v))
lcp@314
   673
lcp@314
   674
\tdx{add_typing}        [| a:N;  b:N |] ==> a #+ b : N
lcp@314
   675
\tdx{addC0}             b:N ==> 0 #+ b = b : N
lcp@314
   676
\tdx{addC_succ}         [| a:N;  b:N |] ==> succ(a) #+ b = succ(a #+ b) : N
lcp@314
   677
lcp@314
   678
\tdx{add_assoc}         [| a:N;  b:N;  c:N |] ==> 
lcp@104
   679
                  (a #+ b) #+ c = a #+ (b #+ c) : N
lcp@104
   680
lcp@314
   681
\tdx{add_commute}       [| a:N;  b:N |] ==> a #+ b = b #+ a : N
lcp@104
   682
lcp@314
   683
\tdx{mult_typing}       [| a:N;  b:N |] ==> a #* b : N
lcp@314
   684
\tdx{multC0}            b:N ==> 0 #* b = 0 : N
lcp@314
   685
\tdx{multC_succ}        [| a:N;  b:N |] ==> succ(a) #* b = b #+ (a#*b) : N
lcp@314
   686
\tdx{mult_commute}      [| a:N;  b:N |] ==> a #* b = b #* a : N
lcp@104
   687
lcp@314
   688
\tdx{add_mult_dist}     [| a:N;  b:N;  c:N |] ==> 
lcp@104
   689
                  (a #+ b) #* c = (a #* c) #+ (b #* c) : N
lcp@104
   690
lcp@314
   691
\tdx{mult_assoc}        [| a:N;  b:N;  c:N |] ==> 
lcp@104
   692
                  (a #* b) #* c = a #* (b #* c) : N
lcp@104
   693
lcp@314
   694
\tdx{diff_typing}       [| a:N;  b:N |] ==> a - b : N
lcp@314
   695
\tdx{diffC0}            a:N ==> a - 0 = a : N
lcp@314
   696
\tdx{diff_0_eq_0}       b:N ==> 0 - b = 0 : N
lcp@314
   697
\tdx{diff_succ_succ}    [| a:N;  b:N |] ==> succ(a) - succ(b) = a - b : N
lcp@314
   698
\tdx{diff_self_eq_0}    a:N ==> a - a = 0 : N
lcp@314
   699
\tdx{add_inverse_diff}  [| a:N;  b:N;  b-a=0 : N |] ==> b #+ (a-b) = a : N
wenzelm@3136
   700
\end{ttbox}
berghofe@3096
   701
\caption{The theory of arithmetic} \label{ctt_arith}
lcp@104
   702
\end{figure}
lcp@104
   703
lcp@104
   704
lcp@104
   705
\section{A theory of arithmetic}
lcp@314
   706
\thydx{Arith} is a theory of elementary arithmetic.  It proves the
lcp@104
   707
properties of addition, multiplication, subtraction, division, and
lcp@104
   708
remainder, culminating in the theorem
lcp@104
   709
\[ a \bmod b + (a/b)\times b = a. \]
berghofe@3096
   710
Figure~\ref{ctt_arith} presents the definitions and some of the key
lcp@314
   711
theorems, including commutative, distributive, and associative laws.
lcp@104
   712
lcp@111
   713
The operators~\verb'#+', \verb'-', \verb'|-|', \verb'#*', \verb'mod'
lcp@111
   714
and~\verb'div' stand for sum, difference, absolute difference, product,
lcp@104
   715
remainder and quotient, respectively.  Since Type Theory has only primitive
lcp@104
   716
recursion, some of their definitions may be obscure.  
lcp@104
   717
lcp@104
   718
The difference~$a-b$ is computed by taking $b$ predecessors of~$a$, where
paulson@5151
   719
the predecessor function is $\lambda v. {\tt rec}(v, 0, \lambda x\,y. x)$.
lcp@104
   720
lcp@111
   721
The remainder $a\bmod b$ counts up to~$a$ in a cyclic fashion, using 0
lcp@111
   722
as the successor of~$b-1$.  Absolute difference is used to test the
lcp@111
   723
equality $succ(v)=b$.
lcp@104
   724
lcp@111
   725
The quotient $a/b$ is computed by adding one for every number $x$
lcp@111
   726
such that $0\leq x \leq a$ and $x\bmod b = 0$.
lcp@104
   727
lcp@104
   728
lcp@104
   729
lcp@104
   730
\section{The examples directory}
wenzelm@9695
   731
This directory contains examples and experimental proofs in CTT.
lcp@314
   732
\begin{ttdescription}
lcp@314
   733
\item[CTT/ex/typechk.ML]
paulson@6170
   734
contains simple examples of type-checking and type deduction.
lcp@104
   735
lcp@314
   736
\item[CTT/ex/elim.ML]
lcp@104
   737
contains some examples from Martin-L\"of~\cite{martinlof84}, proved using 
lcp@104
   738
{\tt pc_tac}.
lcp@104
   739
lcp@314
   740
\item[CTT/ex/equal.ML]
lcp@104
   741
contains simple examples of rewriting.
lcp@104
   742
lcp@314
   743
\item[CTT/ex/synth.ML]
lcp@104
   744
demonstrates the use of unknowns with some trivial examples of program
lcp@104
   745
synthesis. 
lcp@314
   746
\end{ttdescription}
lcp@104
   747
lcp@104
   748
lcp@104
   749
\section{Example: type inference}
lcp@104
   750
Type inference involves proving a goal of the form $a\in\Var{A}$, where $a$
lcp@104
   751
is a term and $\Var{A}$ is an unknown standing for its type.  The type,
lcp@104
   752
initially
lcp@104
   753
unknown, takes shape in the course of the proof.  Our example is the
lcp@104
   754
predecessor function on the natural numbers.
lcp@104
   755
\begin{ttbox}
paulson@5151
   756
Goal "lam n. rec(n, 0, \%x y. x) : ?A";
lcp@104
   757
{\out Level 0}
lcp@284
   758
{\out lam n. rec(n,0,\%x y. x) : ?A}
lcp@284
   759
{\out  1. lam n. rec(n,0,\%x y. x) : ?A}
lcp@104
   760
\end{ttbox}
lcp@104
   761
Since the term is a Constructive Type Theory $\lambda$-abstraction (not to
lcp@104
   762
be confused with a meta-level abstraction), we apply the rule
lcp@314
   763
\tdx{ProdI}, for $\Pi$-introduction.  This instantiates~$\Var{A}$ to a
lcp@104
   764
product type of unknown domain and range.
lcp@104
   765
\begin{ttbox}
lcp@104
   766
by (resolve_tac [ProdI] 1);
lcp@104
   767
{\out Level 1}
lcp@284
   768
{\out lam n. rec(n,0,\%x y. x) : PROD x:?A1. ?B1(x)}
lcp@104
   769
{\out  1. ?A1 type}
lcp@284
   770
{\out  2. !!n. n : ?A1 ==> rec(n,0,\%x y. x) : ?B1(n)}
lcp@104
   771
\end{ttbox}
lcp@284
   772
Subgoal~1 is too flexible.  It can be solved by instantiating~$\Var{A@1}$
lcp@284
   773
to any type, but most instantiations will invalidate subgoal~2.  We
lcp@284
   774
therefore tackle the latter subgoal.  It asks the type of a term beginning
lcp@314
   775
with {\tt rec}, which can be found by $N$-elimination.%
lcp@314
   776
\index{*NE theorem}
lcp@104
   777
\begin{ttbox}
lcp@104
   778
by (eresolve_tac [NE] 2);
lcp@104
   779
{\out Level 2}
lcp@284
   780
{\out lam n. rec(n,0,\%x y. x) : PROD x:N. ?C2(x,x)}
lcp@104
   781
{\out  1. N type}
lcp@104
   782
{\out  2. !!n. 0 : ?C2(n,0)}
lcp@104
   783
{\out  3. !!n x y. [| x : N; y : ?C2(n,x) |] ==> x : ?C2(n,succ(x))}
lcp@104
   784
\end{ttbox}
lcp@284
   785
Subgoal~1 is no longer flexible: we now know~$\Var{A@1}$ is the type of
lcp@284
   786
natural numbers.  However, let us continue proving nontrivial subgoals.
lcp@314
   787
Subgoal~2 asks, what is the type of~0?\index{*NIO theorem}
lcp@104
   788
\begin{ttbox}
lcp@104
   789
by (resolve_tac [NI0] 2);
lcp@104
   790
{\out Level 3}
lcp@284
   791
{\out lam n. rec(n,0,\%x y. x) : N --> N}
lcp@104
   792
{\out  1. N type}
lcp@104
   793
{\out  2. !!n x y. [| x : N; y : N |] ==> x : N}
lcp@104
   794
\end{ttbox}
lcp@284
   795
The type~$\Var{A}$ is now fully determined.  It is the product type
lcp@314
   796
$\prod@{x\in N}N$, which is shown as the function type $N\to N$ because
lcp@284
   797
there is no dependence on~$x$.  But we must prove all the subgoals to show
lcp@284
   798
that the original term is validly typed.  Subgoal~2 is provable by
lcp@314
   799
assumption and the remaining subgoal falls by $N$-formation.%
lcp@314
   800
\index{*NF theorem}
lcp@104
   801
\begin{ttbox}
lcp@104
   802
by (assume_tac 2);
lcp@104
   803
{\out Level 4}
lcp@284
   804
{\out lam n. rec(n,0,\%x y. x) : N --> N}
lcp@104
   805
{\out  1. N type}
lcp@284
   806
\ttbreak
lcp@104
   807
by (resolve_tac [NF] 1);
lcp@104
   808
{\out Level 5}
lcp@284
   809
{\out lam n. rec(n,0,\%x y. x) : N --> N}
lcp@104
   810
{\out No subgoals!}
lcp@104
   811
\end{ttbox}
lcp@104
   812
Calling \ttindex{typechk_tac} can prove this theorem in one step.
lcp@104
   813
lcp@284
   814
Even if the original term is ill-typed, one can infer a type for it, but
lcp@284
   815
unprovable subgoals will be left.  As an exercise, try to prove the
lcp@284
   816
following invalid goal:
lcp@284
   817
\begin{ttbox}
paulson@5151
   818
Goal "lam n. rec(n, 0, \%x y. tt) : ?A";
lcp@284
   819
\end{ttbox}
lcp@284
   820
lcp@284
   821
lcp@104
   822
lcp@104
   823
\section{An example of logical reasoning}
lcp@104
   824
Logical reasoning in Type Theory involves proving a goal of the form
lcp@314
   825
$\Var{a}\in A$, where type $A$ expresses a proposition and $\Var{a}$ stands
lcp@314
   826
for its proof term, a value of type $A$.  The proof term is initially
lcp@314
   827
unknown and takes shape during the proof.  
lcp@314
   828
lcp@314
   829
Our example expresses a theorem about quantifiers in a sorted logic:
lcp@104
   830
\[ \infer{(\ex{x\in A}P(x)) \disj (\ex{x\in A}Q(x))}
lcp@104
   831
         {\ex{x\in A}P(x)\disj Q(x)} 
lcp@104
   832
\]
lcp@314
   833
By the propositions-as-types principle, this is encoded
lcp@314
   834
using~$\Sigma$ and~$+$ types.  A special case of it expresses a
lcp@314
   835
distributive law of Type Theory: 
lcp@104
   836
\[ \infer{(A\times B) + (A\times C)}{A\times(B+C)} \]
lcp@104
   837
Generalizing this from $\times$ to $\Sigma$, and making the typing
lcp@314
   838
conditions explicit, yields the rule we must derive:
lcp@104
   839
\[ \infer{\Var{a} \in (\sum@{x\in A} B(x)) + (\sum@{x\in A} C(x))}
lcp@104
   840
         {\hbox{$A$ type} &
lcp@104
   841
          \infer*{\hbox{$B(x)$ type}}{[x\in A]}  &
lcp@104
   842
          \infer*{\hbox{$C(x)$ type}}{[x\in A]}  &
lcp@104
   843
          p\in \sum@{x\in A} B(x)+C(x)} 
lcp@104
   844
\]
lcp@314
   845
To begin, we bind the rule's premises --- returned by the~{\tt goal}
lcp@314
   846
command --- to the {\ML} variable~{\tt prems}.
lcp@104
   847
\begin{ttbox}
paulson@5151
   848
val prems = Goal
lcp@104
   849
    "[| A type;                       \ttback
lcp@104
   850
\ttback       !!x. x:A ==> B(x) type;       \ttback
lcp@104
   851
\ttback       !!x. x:A ==> C(x) type;       \ttback
lcp@104
   852
\ttback       p: SUM x:A. B(x) + C(x)       \ttback
lcp@104
   853
\ttback    |] ==>  ?a : (SUM x:A. B(x)) + (SUM x:A. C(x))";
lcp@104
   854
{\out Level 0}
lcp@104
   855
{\out ?a : (SUM x:A. B(x)) + (SUM x:A. C(x))}
lcp@104
   856
{\out  1. ?a : (SUM x:A. B(x)) + (SUM x:A. C(x))}
lcp@114
   857
\ttbreak
lcp@111
   858
{\out val prems = ["A type  [A type]",}
lcp@111
   859
{\out              "?x : A ==> B(?x) type  [!!x. x : A ==> B(x) type]",}
lcp@111
   860
{\out              "?x : A ==> C(?x) type  [!!x. x : A ==> C(x) type]",}
lcp@111
   861
{\out              "p : SUM x:A. B(x) + C(x)  [p : SUM x:A. B(x) + C(x)]"]}
lcp@111
   862
{\out             : thm list}
lcp@104
   863
\end{ttbox}
lcp@314
   864
The last premise involves the sum type~$\Sigma$.  Since it is a premise
lcp@314
   865
rather than the assumption of a goal, it cannot be found by {\tt
lcp@314
   866
  eresolve_tac}.  We could insert it (and the other atomic premise) by
lcp@314
   867
calling
lcp@314
   868
\begin{ttbox}
lcp@314
   869
cut_facts_tac prems 1;
lcp@314
   870
\end{ttbox}
lcp@314
   871
A forward proof step is more straightforward here.  Let us resolve the
lcp@314
   872
$\Sigma$-elimination rule with the premises using~\ttindex{RL}.  This
lcp@314
   873
inference yields one result, which we supply to {\tt
lcp@314
   874
  resolve_tac}.\index{*SumE theorem}
lcp@104
   875
\begin{ttbox}
lcp@104
   876
by (resolve_tac (prems RL [SumE]) 1);
lcp@104
   877
{\out Level 1}
lcp@104
   878
{\out split(p,?c1) : (SUM x:A. B(x)) + (SUM x:A. C(x))}
lcp@104
   879
{\out  1. !!x y.}
lcp@104
   880
{\out        [| x : A; y : B(x) + C(x) |] ==>}
lcp@104
   881
{\out        ?c1(x,y) : (SUM x:A. B(x)) + (SUM x:A. C(x))}
lcp@104
   882
\end{ttbox}
lcp@284
   883
The subgoal has two new parameters, $x$ and~$y$.  In the main goal,
lcp@314
   884
$\Var{a}$ has been instantiated with a \cdx{split} term.  The
lcp@284
   885
assumption $y\in B(x) + C(x)$ is eliminated next, causing a case split and
lcp@314
   886
creating the parameter~$xa$.  This inference also inserts~\cdx{when}
lcp@314
   887
into the main goal.\index{*PlusE theorem}
lcp@104
   888
\begin{ttbox}
lcp@104
   889
by (eresolve_tac [PlusE] 1);
lcp@104
   890
{\out Level 2}
lcp@284
   891
{\out split(p,\%x y. when(y,?c2(x,y),?d2(x,y)))}
lcp@104
   892
{\out : (SUM x:A. B(x)) + (SUM x:A. C(x))}
lcp@104
   893
{\out  1. !!x y xa.}
lcp@104
   894
{\out        [| x : A; xa : B(x) |] ==>}
lcp@104
   895
{\out        ?c2(x,y,xa) : (SUM x:A. B(x)) + (SUM x:A. C(x))}
lcp@114
   896
\ttbreak
lcp@104
   897
{\out  2. !!x y ya.}
lcp@104
   898
{\out        [| x : A; ya : C(x) |] ==>}
lcp@104
   899
{\out        ?d2(x,y,ya) : (SUM x:A. B(x)) + (SUM x:A. C(x))}
lcp@104
   900
\end{ttbox}
lcp@104
   901
To complete the proof object for the main goal, we need to instantiate the
lcp@104
   902
terms $\Var{c@2}(x,y,xa)$ and $\Var{d@2}(x,y,xa)$.  We attack subgoal~1 by
lcp@314
   903
a~$+$-introduction rule; since the goal assumes $xa\in B(x)$, we take the left
lcp@314
   904
injection~(\cdx{inl}).
lcp@314
   905
\index{*PlusI_inl theorem}
lcp@104
   906
\begin{ttbox}
lcp@104
   907
by (resolve_tac [PlusI_inl] 1);
lcp@104
   908
{\out Level 3}
lcp@284
   909
{\out split(p,\%x y. when(y,\%xa. inl(?a3(x,y,xa)),?d2(x,y)))}
lcp@104
   910
{\out : (SUM x:A. B(x)) + (SUM x:A. C(x))}
lcp@104
   911
{\out  1. !!x y xa. [| x : A; xa : B(x) |] ==> ?a3(x,y,xa) : SUM x:A. B(x)}
lcp@104
   912
{\out  2. !!x y xa. [| x : A; xa : B(x) |] ==> SUM x:A. C(x) type}
lcp@114
   913
\ttbreak
lcp@104
   914
{\out  3. !!x y ya.}
lcp@104
   915
{\out        [| x : A; ya : C(x) |] ==>}
lcp@104
   916
{\out        ?d2(x,y,ya) : (SUM x:A. B(x)) + (SUM x:A. C(x))}
lcp@104
   917
\end{ttbox}
lcp@314
   918
A new subgoal~2 has appeared, to verify that $\sum@{x\in A}C(x)$ is a type.
lcp@314
   919
Continuing to work on subgoal~1, we apply the $\Sigma$-introduction rule.
lcp@314
   920
This instantiates the term $\Var{a@3}(x,y,xa)$; the main goal now contains
lcp@314
   921
an ordered pair, whose components are two new unknowns.%
lcp@314
   922
\index{*SumI theorem}
lcp@104
   923
\begin{ttbox}
lcp@104
   924
by (resolve_tac [SumI] 1);
lcp@104
   925
{\out Level 4}
lcp@284
   926
{\out split(p,\%x y. when(y,\%xa. inl(<?a4(x,y,xa),?b4(x,y,xa)>),?d2(x,y)))}
lcp@104
   927
{\out : (SUM x:A. B(x)) + (SUM x:A. C(x))}
lcp@104
   928
{\out  1. !!x y xa. [| x : A; xa : B(x) |] ==> ?a4(x,y,xa) : A}
lcp@104
   929
{\out  2. !!x y xa. [| x : A; xa : B(x) |] ==> ?b4(x,y,xa) : B(?a4(x,y,xa))}
lcp@104
   930
{\out  3. !!x y xa. [| x : A; xa : B(x) |] ==> SUM x:A. C(x) type}
lcp@104
   931
{\out  4. !!x y ya.}
lcp@104
   932
{\out        [| x : A; ya : C(x) |] ==>}
lcp@104
   933
{\out        ?d2(x,y,ya) : (SUM x:A. B(x)) + (SUM x:A. C(x))}
lcp@104
   934
\end{ttbox}
lcp@104
   935
The two new subgoals both hold by assumption.  Observe how the unknowns
lcp@104
   936
$\Var{a@4}$ and $\Var{b@4}$ are instantiated throughout the proof state.
lcp@104
   937
\begin{ttbox}
lcp@104
   938
by (assume_tac 1);
lcp@104
   939
{\out Level 5}
lcp@284
   940
{\out split(p,\%x y. when(y,\%xa. inl(<x,?b4(x,y,xa)>),?d2(x,y)))}
lcp@104
   941
{\out : (SUM x:A. B(x)) + (SUM x:A. C(x))}
lcp@284
   942
\ttbreak
lcp@104
   943
{\out  1. !!x y xa. [| x : A; xa : B(x) |] ==> ?b4(x,y,xa) : B(x)}
lcp@104
   944
{\out  2. !!x y xa. [| x : A; xa : B(x) |] ==> SUM x:A. C(x) type}
lcp@104
   945
{\out  3. !!x y ya.}
lcp@104
   946
{\out        [| x : A; ya : C(x) |] ==>}
lcp@104
   947
{\out        ?d2(x,y,ya) : (SUM x:A. B(x)) + (SUM x:A. C(x))}
lcp@284
   948
\ttbreak
lcp@104
   949
by (assume_tac 1);
lcp@104
   950
{\out Level 6}
lcp@284
   951
{\out split(p,\%x y. when(y,\%xa. inl(<x,xa>),?d2(x,y)))}
lcp@104
   952
{\out : (SUM x:A. B(x)) + (SUM x:A. C(x))}
lcp@104
   953
{\out  1. !!x y xa. [| x : A; xa : B(x) |] ==> SUM x:A. C(x) type}
lcp@104
   954
{\out  2. !!x y ya.}
lcp@104
   955
{\out        [| x : A; ya : C(x) |] ==>}
lcp@104
   956
{\out        ?d2(x,y,ya) : (SUM x:A. B(x)) + (SUM x:A. C(x))}
lcp@104
   957
\end{ttbox}
lcp@314
   958
Subgoal~1 is an example of a well-formedness subgoal~\cite{constable86}.
lcp@314
   959
Such subgoals are usually trivial; this one yields to
lcp@314
   960
\ttindex{typechk_tac}, given the current list of premises.
lcp@104
   961
\begin{ttbox}
lcp@104
   962
by (typechk_tac prems);
lcp@104
   963
{\out Level 7}
lcp@284
   964
{\out split(p,\%x y. when(y,\%xa. inl(<x,xa>),?d2(x,y)))}
lcp@104
   965
{\out : (SUM x:A. B(x)) + (SUM x:A. C(x))}
lcp@104
   966
{\out  1. !!x y ya.}
lcp@104
   967
{\out        [| x : A; ya : C(x) |] ==>}
lcp@104
   968
{\out        ?d2(x,y,ya) : (SUM x:A. B(x)) + (SUM x:A. C(x))}
lcp@104
   969
\end{ttbox}
lcp@314
   970
This subgoal is the other case from the $+$-elimination above, and can be
lcp@314
   971
proved similarly.  Quicker is to apply \ttindex{pc_tac}.  The main goal
lcp@314
   972
finally gets a fully instantiated proof object.
lcp@104
   973
\begin{ttbox}
lcp@104
   974
by (pc_tac prems 1);
lcp@104
   975
{\out Level 8}
lcp@284
   976
{\out split(p,\%x y. when(y,\%xa. inl(<x,xa>),\%y. inr(<x,y>)))}
lcp@104
   977
{\out : (SUM x:A. B(x)) + (SUM x:A. C(x))}
lcp@104
   978
{\out No subgoals!}
lcp@104
   979
\end{ttbox}
lcp@104
   980
Calling \ttindex{pc_tac} after the first $\Sigma$-elimination above also
lcp@104
   981
proves this theorem.
lcp@104
   982
lcp@104
   983
lcp@104
   984
\section{Example: deriving a currying functional}
lcp@104
   985
In simply-typed languages such as {\ML}, a currying functional has the type 
lcp@104
   986
\[ (A\times B \to C) \to (A\to (B\to C)). \]
lcp@314
   987
Let us generalize this to the dependent types~$\Sigma$ and~$\Pi$.  
lcp@284
   988
The functional takes a function~$f$ that maps $z:\Sigma(A,B)$
lcp@284
   989
to~$C(z)$; the resulting function maps $x\in A$ and $y\in B(x)$ to
lcp@284
   990
$C(\langle x,y\rangle)$.
lcp@284
   991
lcp@284
   992
Formally, there are three typing premises.  $A$ is a type; $B$ is an
lcp@284
   993
$A$-indexed family of types; $C$ is a family of types indexed by
lcp@284
   994
$\Sigma(A,B)$.  The goal is expressed using \hbox{\tt PROD f} to ensure
lcp@284
   995
that the parameter corresponding to the functional's argument is really
lcp@284
   996
called~$f$; Isabelle echoes the type using \verb|-->| because there is no
lcp@284
   997
explicit dependence upon~$f$.
lcp@104
   998
\begin{ttbox}
paulson@5151
   999
val prems = Goal
lcp@284
  1000
    "[| A type; !!x. x:A ==> B(x) type;                           \ttback
lcp@284
  1001
\ttback               !!z. z: (SUM x:A. B(x)) ==> C(z) type             \ttback
lcp@284
  1002
\ttback    |] ==> ?a : PROD f: (PROD z : (SUM x:A . B(x)) . C(z)).      \ttback
lcp@284
  1003
\ttback                     (PROD x:A . PROD y:B(x) . C(<x,y>))";
lcp@284
  1004
\ttbreak
lcp@104
  1005
{\out Level 0}
lcp@284
  1006
{\out ?a : (PROD z:SUM x:A. B(x). C(z)) -->}
lcp@284
  1007
{\out      (PROD x:A. PROD y:B(x). C(<x,y>))}
lcp@104
  1008
{\out  1. ?a : (PROD z:SUM x:A. B(x). C(z)) -->}
lcp@104
  1009
{\out          (PROD x:A. PROD y:B(x). C(<x,y>))}
lcp@114
  1010
\ttbreak
lcp@111
  1011
{\out val prems = ["A type  [A type]",}
lcp@111
  1012
{\out              "?x : A ==> B(?x) type  [!!x. x : A ==> B(x) type]",}
lcp@111
  1013
{\out              "?z : SUM x:A. B(x) ==> C(?z) type}
lcp@111
  1014
{\out               [!!z. z : SUM x:A. B(x) ==> C(z) type]"] : thm list}
lcp@104
  1015
\end{ttbox}
lcp@284
  1016
This is a chance to demonstrate \ttindex{intr_tac}.  Here, the tactic
lcp@314
  1017
repeatedly applies $\Pi$-introduction and proves the rather
lcp@284
  1018
tiresome typing conditions.  
lcp@284
  1019
lcp@284
  1020
Note that $\Var{a}$ becomes instantiated to three nested
lcp@284
  1021
$\lambda$-abstractions.  It would be easier to read if the bound variable
lcp@284
  1022
names agreed with the parameters in the subgoal.  Isabelle attempts to give
lcp@284
  1023
parameters the same names as corresponding bound variables in the goal, but
lcp@284
  1024
this does not always work.  In any event, the goal is logically correct.
lcp@104
  1025
\begin{ttbox}
lcp@104
  1026
by (intr_tac prems);
lcp@104
  1027
{\out Level 1}
lcp@104
  1028
{\out lam x xa xb. ?b7(x,xa,xb)}
lcp@104
  1029
{\out : (PROD z:SUM x:A. B(x). C(z)) --> (PROD x:A. PROD y:B(x). C(<x,y>))}
lcp@284
  1030
{\out  1. !!f x y.}
lcp@284
  1031
{\out        [| f : PROD z:SUM x:A. B(x). C(z); x : A; y : B(x) |] ==>}
lcp@284
  1032
{\out        ?b7(f,x,y) : C(<x,y>)}
lcp@104
  1033
\end{ttbox}
lcp@284
  1034
Using $\Pi$-elimination, we solve subgoal~1 by applying the function~$f$.
lcp@314
  1035
\index{*ProdE theorem}
lcp@104
  1036
\begin{ttbox}
lcp@104
  1037
by (eresolve_tac [ProdE] 1);
lcp@104
  1038
{\out Level 2}
lcp@104
  1039
{\out lam x xa xb. x ` <xa,xb>}
lcp@104
  1040
{\out : (PROD z:SUM x:A. B(x). C(z)) --> (PROD x:A. PROD y:B(x). C(<x,y>))}
lcp@284
  1041
{\out  1. !!f x y. [| x : A; y : B(x) |] ==> <x,y> : SUM x:A. B(x)}
lcp@104
  1042
\end{ttbox}
lcp@314
  1043
Finally, we verify that the argument's type is suitable for the function
lcp@314
  1044
application.  This is straightforward using introduction rules.
lcp@104
  1045
\index{*intr_tac}
lcp@104
  1046
\begin{ttbox}
lcp@104
  1047
by (intr_tac prems);
lcp@104
  1048
{\out Level 3}
lcp@104
  1049
{\out lam x xa xb. x ` <xa,xb>}
lcp@104
  1050
{\out : (PROD z:SUM x:A. B(x). C(z)) --> (PROD x:A. PROD y:B(x). C(<x,y>))}
lcp@104
  1051
{\out No subgoals!}
lcp@104
  1052
\end{ttbox}
lcp@104
  1053
Calling~\ttindex{pc_tac} would have proved this theorem in one step; it can
lcp@104
  1054
also prove an example by Martin-L\"of, related to $\disj$-elimination
lcp@104
  1055
\cite[page~58]{martinlof84}.
lcp@104
  1056
lcp@104
  1057
lcp@104
  1058
\section{Example: proving the Axiom of Choice} \label{ctt-choice}
lcp@104
  1059
Suppose we have a function $h\in \prod@{x\in A}\sum@{y\in B(x)} C(x,y)$,
lcp@104
  1060
which takes $x\in A$ to some $y\in B(x)$ paired with some $z\in C(x,y)$.
lcp@104
  1061
Interpreting propositions as types, this asserts that for all $x\in A$
lcp@104
  1062
there exists $y\in B(x)$ such that $C(x,y)$.  The Axiom of Choice asserts
lcp@104
  1063
that we can construct a function $f\in \prod@{x\in A}B(x)$ such that
lcp@104
  1064
$C(x,f{\tt`}x)$ for all $x\in A$, where the latter property is witnessed by a
lcp@104
  1065
function $g\in \prod@{x\in A}C(x,f{\tt`}x)$.
lcp@104
  1066
lcp@104
  1067
In principle, the Axiom of Choice is simple to derive in Constructive Type
lcp@333
  1068
Theory.  The following definitions work:
lcp@104
  1069
\begin{eqnarray*}
lcp@104
  1070
    f & \equiv & {\tt fst} \circ h \\
lcp@104
  1071
    g & \equiv & {\tt snd} \circ h
lcp@104
  1072
\end{eqnarray*}
lcp@314
  1073
But a completely formal proof is hard to find.  The rules can be applied in
lcp@314
  1074
countless ways, yielding many higher-order unifiers.  The proof can get
lcp@314
  1075
bogged down in the details.  But with a careful selection of derived rules
paulson@6170
  1076
(recall Fig.\ts\ref{ctt-derived}) and the type-checking tactics, we can
lcp@314
  1077
prove the theorem in nine steps.
lcp@104
  1078
\begin{ttbox}
paulson@5151
  1079
val prems = Goal
lcp@284
  1080
    "[| A type;  !!x. x:A ==> B(x) type;                    \ttback
lcp@284
  1081
\ttback       !!x y.[| x:A;  y:B(x) |] ==> C(x,y) type            \ttback
lcp@284
  1082
\ttback    |] ==> ?a : PROD h: (PROD x:A. SUM y:B(x). C(x,y)).    \ttback
lcp@284
  1083
\ttback                     (SUM f: (PROD x:A. B(x)). PROD x:A. C(x, f`x))";
lcp@104
  1084
{\out Level 0}
lcp@104
  1085
{\out ?a : (PROD x:A. SUM y:B(x). C(x,y)) -->}
lcp@104
  1086
{\out      (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))}
lcp@104
  1087
{\out  1. ?a : (PROD x:A. SUM y:B(x). C(x,y)) -->}
lcp@104
  1088
{\out          (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))}
lcp@111
  1089
\ttbreak
lcp@111
  1090
{\out val prems = ["A type  [A type]",}
lcp@111
  1091
{\out              "?x : A ==> B(?x) type  [!!x. x : A ==> B(x) type]",}
lcp@111
  1092
{\out              "[| ?x : A; ?y : B(?x) |] ==> C(?x, ?y) type}
lcp@111
  1093
{\out               [!!x y. [| x : A; y : B(x) |] ==> C(x, y) type]"]}
lcp@111
  1094
{\out             : thm list}
lcp@104
  1095
\end{ttbox}
lcp@104
  1096
First, \ttindex{intr_tac} applies introduction rules and performs routine
paulson@6170
  1097
type-checking.  This instantiates~$\Var{a}$ to a construction involving
lcp@314
  1098
a $\lambda$-abstraction and an ordered pair.  The pair's components are
lcp@314
  1099
themselves $\lambda$-abstractions and there is a subgoal for each.
lcp@104
  1100
\begin{ttbox}
lcp@104
  1101
by (intr_tac prems);
lcp@104
  1102
{\out Level 1}
lcp@104
  1103
{\out lam x. <lam xa. ?b7(x,xa),lam xa. ?b8(x,xa)>}
lcp@104
  1104
{\out : (PROD x:A. SUM y:B(x). C(x,y)) -->}
lcp@104
  1105
{\out   (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))}
lcp@114
  1106
\ttbreak
lcp@284
  1107
{\out  1. !!h x.}
lcp@284
  1108
{\out        [| h : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>}
lcp@284
  1109
{\out        ?b7(h,x) : B(x)}
lcp@114
  1110
\ttbreak
lcp@284
  1111
{\out  2. !!h x.}
lcp@284
  1112
{\out        [| h : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>}
lcp@284
  1113
{\out        ?b8(h,x) : C(x,(lam x. ?b7(h,x)) ` x)}
lcp@104
  1114
\end{ttbox}
lcp@104
  1115
Subgoal~1 asks to find the choice function itself, taking $x\in A$ to some
lcp@284
  1116
$\Var{b@7}(h,x)\in B(x)$.  Subgoal~2 asks, given $x\in A$, for a proof
lcp@284
  1117
object $\Var{b@8}(h,x)$ to witness that the choice function's argument and
lcp@284
  1118
result lie in the relation~$C$.  This latter task will take up most of the
lcp@284
  1119
proof.
lcp@314
  1120
\index{*ProdE theorem}\index{*SumE_fst theorem}\index{*RS}
lcp@104
  1121
\begin{ttbox}
lcp@104
  1122
by (eresolve_tac [ProdE RS SumE_fst] 1);
lcp@104
  1123
{\out Level 2}
lcp@104
  1124
{\out lam x. <lam xa. fst(x ` xa),lam xa. ?b8(x,xa)>}
lcp@104
  1125
{\out : (PROD x:A. SUM y:B(x). C(x,y)) -->}
lcp@104
  1126
{\out   (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))}
lcp@114
  1127
\ttbreak
lcp@284
  1128
{\out  1. !!h x. x : A ==> x : A}
lcp@284
  1129
{\out  2. !!h x.}
lcp@284
  1130
{\out        [| h : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>}
lcp@284
  1131
{\out        ?b8(h,x) : C(x,(lam x. fst(h ` x)) ` x)}
lcp@104
  1132
\end{ttbox}
lcp@314
  1133
Above, we have composed {\tt fst} with the function~$h$.  Unification
lcp@314
  1134
has deduced that the function must be applied to $x\in A$.  We have our
lcp@314
  1135
choice function.
lcp@104
  1136
\begin{ttbox}
lcp@104
  1137
by (assume_tac 1);
lcp@104
  1138
{\out Level 3}
lcp@104
  1139
{\out lam x. <lam xa. fst(x ` xa),lam xa. ?b8(x,xa)>}
lcp@104
  1140
{\out : (PROD x:A. SUM y:B(x). C(x,y)) -->}
lcp@104
  1141
{\out   (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))}
lcp@284
  1142
{\out  1. !!h x.}
lcp@284
  1143
{\out        [| h : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>}
lcp@284
  1144
{\out        ?b8(h,x) : C(x,(lam x. fst(h ` x)) ` x)}
lcp@104
  1145
\end{ttbox}
lcp@314
  1146
Before we can compose {\tt snd} with~$h$, the arguments of $C$ must be
lcp@314
  1147
simplified.  The derived rule \tdx{replace_type} lets us replace a type
lcp@284
  1148
by any equivalent type, shown below as the schematic term $\Var{A@{13}}(h,x)$:
lcp@104
  1149
\begin{ttbox}
lcp@104
  1150
by (resolve_tac [replace_type] 1);
lcp@104
  1151
{\out Level 4}
lcp@104
  1152
{\out lam x. <lam xa. fst(x ` xa),lam xa. ?b8(x,xa)>}
lcp@104
  1153
{\out : (PROD x:A. SUM y:B(x). C(x,y)) -->}
lcp@104
  1154
{\out   (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))}
lcp@114
  1155
\ttbreak
lcp@284
  1156
{\out  1. !!h x.}
lcp@284
  1157
{\out        [| h : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>}
lcp@284
  1158
{\out        C(x,(lam x. fst(h ` x)) ` x) = ?A13(h,x)}
lcp@114
  1159
\ttbreak
lcp@284
  1160
{\out  2. !!h x.}
lcp@284
  1161
{\out        [| h : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>}
lcp@284
  1162
{\out        ?b8(h,x) : ?A13(h,x)}
lcp@104
  1163
\end{ttbox}
lcp@314
  1164
The derived rule \tdx{subst_eqtyparg} lets us simplify a type's
lcp@104
  1165
argument (by currying, $C(x)$ is a unary type operator):
lcp@104
  1166
\begin{ttbox}
lcp@104
  1167
by (resolve_tac [subst_eqtyparg] 1);
lcp@104
  1168
{\out Level 5}
lcp@104
  1169
{\out lam x. <lam xa. fst(x ` xa),lam xa. ?b8(x,xa)>}
lcp@104
  1170
{\out : (PROD x:A. SUM y:B(x). C(x,y)) -->}
lcp@104
  1171
{\out   (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))}
lcp@114
  1172
\ttbreak
lcp@284
  1173
{\out  1. !!h x.}
lcp@284
  1174
{\out        [| h : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>}
lcp@284
  1175
{\out        (lam x. fst(h ` x)) ` x = ?c14(h,x) : ?A14(h,x)}
lcp@114
  1176
\ttbreak
lcp@284
  1177
{\out  2. !!h x z.}
lcp@284
  1178
{\out        [| h : PROD x:A. SUM y:B(x). C(x,y); x : A;}
lcp@284
  1179
{\out           z : ?A14(h,x) |] ==>}
lcp@104
  1180
{\out        C(x,z) type}
lcp@114
  1181
\ttbreak
lcp@284
  1182
{\out  3. !!h x.}
lcp@284
  1183
{\out        [| h : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>}
lcp@284
  1184
{\out        ?b8(h,x) : C(x,?c14(h,x))}
lcp@104
  1185
\end{ttbox}
lcp@284
  1186
Subgoal~1 requires simply $\beta$-contraction, which is the rule
lcp@314
  1187
\tdx{ProdC}.  The term $\Var{c@{14}}(h,x)$ in the last subgoal
lcp@284
  1188
receives the contracted result.
lcp@104
  1189
\begin{ttbox}
lcp@104
  1190
by (resolve_tac [ProdC] 1);
lcp@104
  1191
{\out Level 6}
lcp@104
  1192
{\out lam x. <lam xa. fst(x ` xa),lam xa. ?b8(x,xa)>}
lcp@104
  1193
{\out : (PROD x:A. SUM y:B(x). C(x,y)) -->}
lcp@104
  1194
{\out   (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))}
lcp@114
  1195
\ttbreak
lcp@284
  1196
{\out  1. !!h x.}
lcp@284
  1197
{\out        [| h : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>}
lcp@284
  1198
{\out        x : ?A15(h,x)}
lcp@114
  1199
\ttbreak
lcp@284
  1200
{\out  2. !!h x xa.}
lcp@284
  1201
{\out        [| h : PROD x:A. SUM y:B(x). C(x,y); x : A;}
lcp@284
  1202
{\out           xa : ?A15(h,x) |] ==>}
lcp@284
  1203
{\out        fst(h ` xa) : ?B15(h,x,xa)}
lcp@114
  1204
\ttbreak
lcp@284
  1205
{\out  3. !!h x z.}
lcp@284
  1206
{\out        [| h : PROD x:A. SUM y:B(x). C(x,y); x : A;}
lcp@284
  1207
{\out           z : ?B15(h,x,x) |] ==>}
lcp@104
  1208
{\out        C(x,z) type}
lcp@114
  1209
\ttbreak
lcp@284
  1210
{\out  4. !!h x.}
lcp@284
  1211
{\out        [| h : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>}
lcp@284
  1212
{\out        ?b8(h,x) : C(x,fst(h ` x))}
lcp@104
  1213
\end{ttbox}
paulson@6170
  1214
Routine type-checking goals proliferate in Constructive Type Theory, but
lcp@104
  1215
\ttindex{typechk_tac} quickly solves them.  Note the inclusion of
lcp@314
  1216
\tdx{SumE_fst} along with the premises.
lcp@104
  1217
\begin{ttbox}
lcp@104
  1218
by (typechk_tac (SumE_fst::prems));
lcp@104
  1219
{\out Level 7}
lcp@104
  1220
{\out lam x. <lam xa. fst(x ` xa),lam xa. ?b8(x,xa)>}
lcp@104
  1221
{\out : (PROD x:A. SUM y:B(x). C(x,y)) -->}
lcp@104
  1222
{\out   (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))}
lcp@284
  1223
\ttbreak
lcp@284
  1224
{\out  1. !!h x.}
lcp@284
  1225
{\out        [| h : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>}
lcp@284
  1226
{\out        ?b8(h,x) : C(x,fst(h ` x))}
lcp@104
  1227
\end{ttbox}
lcp@314
  1228
We are finally ready to compose {\tt snd} with~$h$.
lcp@314
  1229
\index{*ProdE theorem}\index{*SumE_snd theorem}\index{*RS}
lcp@104
  1230
\begin{ttbox}
lcp@104
  1231
by (eresolve_tac [ProdE RS SumE_snd] 1);
lcp@104
  1232
{\out Level 8}
lcp@104
  1233
{\out lam x. <lam xa. fst(x ` xa),lam xa. snd(x ` xa)>}
lcp@104
  1234
{\out : (PROD x:A. SUM y:B(x). C(x,y)) -->}
lcp@104
  1235
{\out   (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))}
lcp@284
  1236
\ttbreak
lcp@284
  1237
{\out  1. !!h x. x : A ==> x : A}
lcp@284
  1238
{\out  2. !!h x. x : A ==> B(x) type}
lcp@284
  1239
{\out  3. !!h x xa. [| x : A; xa : B(x) |] ==> C(x,xa) type}
lcp@104
  1240
\end{ttbox}
lcp@104
  1241
The proof object has reached its final form.  We call \ttindex{typechk_tac}
paulson@6170
  1242
to finish the type-checking.
lcp@104
  1243
\begin{ttbox}
lcp@104
  1244
by (typechk_tac prems);
lcp@104
  1245
{\out Level 9}
lcp@104
  1246
{\out lam x. <lam xa. fst(x ` xa),lam xa. snd(x ` xa)>}
lcp@104
  1247
{\out : (PROD x:A. SUM y:B(x). C(x,y)) -->}
lcp@104
  1248
{\out   (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))}
lcp@104
  1249
{\out No subgoals!}
lcp@104
  1250
\end{ttbox}
lcp@314
  1251
It might be instructive to compare this proof with Martin-L\"of's forward
lcp@314
  1252
proof of the Axiom of Choice \cite[page~50]{martinlof84}.
lcp@314
  1253
lcp@314
  1254
\index{Constructive Type Theory|)}