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