doc-src/Logics/CTT.tex
 changeset 9695 ec7d7f877712 parent 7159 b009afd1ace5 child 12679 8ed660138f83
equal inserted replaced
9694:13f3aaf12be2 9695:ec7d7f877712
    38     \end{array}
    38     \end{array}
    39 \]
    39 \]
    40 Assumptions can use all the judgement forms, for instance to express that
    40 Assumptions can use all the judgement forms, for instance to express that
    41 $B$ is a family of types over~$A$:
    41 $B$ is a family of types over~$A$:
    42 $\Forall x . x\in A \Imp B(x)\;{\rm type}$
    42 $\Forall x . x\in A \Imp B(x)\;{\rm type}$
    43 To justify the {\CTT} formulation it is probably best to appeal directly
    43 To justify the CTT formulation it is probably best to appeal directly to the
    44 to the semantic explanations of the rules~\cite{martinlof84}, rather than
    44 semantic explanations of the rules~\cite{martinlof84}, rather than to the
    45 to the rules themselves.  The order of assumptions no longer matters,
    45 rules themselves.  The order of assumptions no longer matters, unlike in
    46 unlike in standard Type Theory.  Contexts, which are typical of many modern
    46 standard Type Theory.  Contexts, which are typical of many modern type
    47 type theories, are difficult to represent in Isabelle.  In particular, it
    47 theories, are difficult to represent in Isabelle.  In particular, it is
    48 is difficult to enforce that all the variables in a context are distinct.
    48 difficult to enforce that all the variables in a context are distinct.
    49 \index{assumptions!in {\CTT}}
    49 \index{assumptions!in CTT}
    50
    50
    51 The theory does not use polymorphism.  Terms in {\CTT} have type~\tydx{i}, the
    51 The theory does not use polymorphism.  Terms in CTT have type~\tydx{i}, the
    52 type of individuals.  Types in {\CTT} have type~\tydx{t}.
    52 type of individuals.  Types in CTT have type~\tydx{t}.
    53
    53
    54 \begin{figure} \tabcolsep=1em  %wider spacing in tables
    54 \begin{figure} \tabcolsep=1em  %wider spacing in tables
    55 \begin{center}
    55 \begin{center}
    56 \begin{tabular}{rrr}
    56 \begin{tabular}{rrr}
    57   \it name      & \it meta-type         & \it description \\
    57   \it name      & \it meta-type         & \it description \\
    79   \cdx{contr}   & $i\to i$              & eliminator\$2ex]  79 \cdx{contr} & i\to i & eliminator\\[2ex]  80 \cdx{T} & t & singleton type\\  80 \cdx{T} & t & singleton type\\  81 \cdx{tt} & i & constructor  81 \cdx{tt} & i & constructor  82 \end{tabular}  82 \end{tabular}  83 \end{center}  83 \end{center}  84 \caption{The constants of {\CTT}} \label{ctt-constants}  84 \caption{The constants of CTT} \label{ctt-constants}  85 \end{figure}  85 \end{figure}  86   86   87   87   88 {\CTT} supports all of Type Theory apart from list types, well-ordering  88 CTT supports all of Type Theory apart from list types, well-ordering types,  89 types, and universes. Universes could be introduced {\em\a la Tarski},  89 and universes. Universes could be introduced {\em\a la Tarski}, adding new  90 adding new constants as names for types. The formulation {\em\a la  90 constants as names for types. The formulation {\em\a la Russell}, where  91 Russell}, where types denote themselves, is only possible if we identify  91 types denote themselves, is only possible if we identify the meta-types~{\tt  92 the meta-types~{\tt i} and~{\tt t}. Most published formulations of  92 i} and~{\tt t}. Most published formulations of well-ordering types have  93 well-ordering types have difficulties involving extensionality of  93 difficulties involving extensionality of functions; I suggest that you use  94 functions; I suggest that you use some other method for defining recursive  94 some other method for defining recursive types. List types are easy to  95 types. List types are easy to introduce by declaring new rules.  95 introduce by declaring new rules.  96   96   97 {\CTT} uses the 1982 version of Type Theory, with extensional equality.  97 CTT uses the 1982 version of Type Theory, with extensional equality. The  98 The computation a=b\in A and the equality c\in Eq(A,a,b) are  98 computation a=b\in A and the equality c\in Eq(A,a,b) are interchangeable.  99 interchangeable. Its rewriting tactics prove theorems of the form a=b\in  99 Its rewriting tactics prove theorems of the form a=b\in A. It could be  100 A. It could be modified to have intensional equality, but rewriting  100 modified to have intensional equality, but rewriting tactics would have to  101 tactics would have to prove theorems of the form c\in Eq(A,a,b) and the  101 prove theorems of the form c\in Eq(A,a,b) and the computation rules might  102 computation rules might require a separate simplifier.  102 require a separate simplifier.  103   103   104   104   105 \begin{figure} \tabcolsep=1em %wider spacing in tables  105 \begin{figure} \tabcolsep=1em %wider spacing in tables  106 \index{lambda abs@\lambda-abstractions!in \CTT}  106 \index{lambda abs@\lambda-abstractions!in CTT}  107 \begin{center}  107 \begin{center}  108 \begin{tabular}{llrrr}   108 \begin{tabular}{llrrr}   109 \it symbol &\it name &\it meta-type & \it priority & \it description \\  109 \it symbol &\it name &\it meta-type & \it priority & \it description \\  110 \sdx{lam} & \cdx{lambda} & (i\To o)\To i & 10 & \lambda-abstraction  110 \sdx{lam} & \cdx{lambda} & (i\To o)\To i & 10 & \lambda-abstraction  111 \end{tabular}  111 \end{tabular}  112 \end{center}  112 \end{center}  113 \subcaption{Binders}   113 \subcaption{Binders}   114   114   115 \begin{center}  115 \begin{center}  116 \index{*" symbol}\index{function applications!in \CTT}  116 \index{*" symbol}\index{function applications!in CTT}  117 \index{*"+ symbol}  117 \index{*"+ symbol}  118 \begin{tabular}{rrrr}   118 \begin{tabular}{rrrr}   119 \it symbol & \it meta-type & \it priority & \it description \\   119 \it symbol & \it meta-type & \it priority & \it description \\   120 \tt  & [i,i]\to i & Left 55 & function application\\  120 \tt  & [i,i]\to i & Left 55 & function application\\  121 \tt + & [t,t]\to t & Right 30 & sum of two types  121 \tt + & [t,t]\to t & Right 30 & sum of two types  158 & | & "< " term " , " term " >"  158 & | & "< " term " , " term " >"  159 \end{array}   159 \end{array}   160$
   160 \]
   161 \end{center}
   161 \end{center}
   162 \subcaption{Grammar}
   162 \subcaption{Grammar}
   163 \caption{Syntax of {\CTT}} \label{ctt-syntax}
   163 \caption{Syntax of CTT} \label{ctt-syntax}
   164 \end{figure}
   164 \end{figure}
   165
   165
   166 %%%%\section{Generic Packages}  typedsimp.ML????????????????
   166 %%%%\section{Generic Packages}  typedsimp.ML????????????????
   167
   167
   168
   168
   169 \section{Syntax}
   169 \section{Syntax}
   170 The constants are shown in Fig.\ts\ref{ctt-constants}.  The infixes include
   170 The constants are shown in Fig.\ts\ref{ctt-constants}.  The infixes include
   171 the function application operator (sometimes called apply'), and the
   171 the function application operator (sometimes called apply'), and the 2-place
   172 2-place type operators.  Note that meta-level abstraction and application,
   172 type operators.  Note that meta-level abstraction and application, $\lambda  173$\lambda x.b$and$f(a)$, differ from object-level abstraction and  173 x.b$ and $f(a)$, differ from object-level abstraction and application,
   174 application, \hbox{\tt lam $x$. $b$} and $b{\tt}a$.  A {\CTT}
   174 \hbox{\tt lam $x$. $b$} and $b{\tt}a$.  A CTT function~$f$ is simply an
   175 function~$f$ is simply an individual as far as Isabelle is concerned: its
   175 individual as far as Isabelle is concerned: its Isabelle type is~$i$, not say
   176 Isabelle type is~$i$, not say $i\To i$.
   176 $i\To i$.
   177
   177
   178 The notation for~{\CTT} (Fig.\ts\ref{ctt-syntax}) is based on that of
   178 The notation for~CTT (Fig.\ts\ref{ctt-syntax}) is based on that of Nordstr\"om
   179 Nordstr\"om et al.~\cite{nordstrom90}.  The empty type is called $F$ and
   179 et al.~\cite{nordstrom90}.  The empty type is called $F$ and the one-element
   180 the one-element type is $T$; other finite types are built as $T+T+T$, etc.
   180 type is $T$; other finite types are built as $T+T+T$, etc.
   181
   181
   182 \index{*SUM symbol}\index{*PROD symbol}
   182 \index{*SUM symbol}\index{*PROD symbol}
   183 Quantification is expressed by sums $\sum@{x\in A}B[x]$ and
   183 Quantification is expressed by sums $\sum@{x\in A}B[x]$ and
   184 products $\prod@{x\in A}B[x]$.  Instead of {\tt Sum($A$,$B$)} and {\tt
   184 products $\prod@{x\in A}B[x]$.  Instead of {\tt Sum($A$,$B$)} and {\tt
   185   Prod($A$,$B$)} we may write \hbox{\tt SUM $x$:$A$.\ $B[x]$} and \hbox{\tt
   185   Prod($A$,$B$)} we may write \hbox{\tt SUM $x$:$A$.\ $B[x]$} and \hbox{\tt
   385
   385
   386 \tdx{SumE_snd}  [| p: Sum(A,B);  A type;  !!x. x:A ==> B(x) type
   386 \tdx{SumE_snd}  [| p: Sum(A,B);  A type;  !!x. x:A ==> B(x) type
   387           |] ==> snd(p) : B(fst(p))
   387           |] ==> snd(p) : B(fst(p))
   388 \end{ttbox}
   388 \end{ttbox}
   389
   389
   390 \caption{Derived rules for {\CTT}} \label{ctt-derived}
   390 \caption{Derived rules for CTT} \label{ctt-derived}
   391 \end{figure}
   391 \end{figure}
   392
   392
   393
   393
   394 \section{Rules of inference}
   394 \section{Rules of inference}
   395 The rules obey the following naming conventions.  Type formation rules have
   395 The rules obey the following naming conventions.  Type formation rules have
   468
   468
   469
   469
   470 \section{Rule lists}
   470 \section{Rule lists}
   471 The Type Theory tactics provide rewriting, type inference, and logical
   471 The Type Theory tactics provide rewriting, type inference, and logical
   472 reasoning.  Many proof procedures work by repeatedly resolving certain Type
   472 reasoning.  Many proof procedures work by repeatedly resolving certain Type
   473 Theory rules against a proof state.  {\CTT} defines lists --- each with
   473 Theory rules against a proof state.  CTT defines lists --- each with
   474 type
   474 type
   475 \hbox{\tt thm list} --- of related rules.
   475 \hbox{\tt thm list} --- of related rules.
   476 \begin{ttdescription}
   476 \begin{ttdescription}
   477 \item[\ttindexbold{form_rls}]
   477 \item[\ttindexbold{form_rls}]
   478 contains formation rules for the types $N$, $\Pi$, $\Sigma$, $+$, $Eq$,
   478 contains formation rules for the types $N$, $\Pi$, $\Sigma$, $+$, $Eq$,
   512 test_assume_tac : int -> tactic
   512 test_assume_tac : int -> tactic
   513 typechk_tac     : thm list -> tactic
   513 typechk_tac     : thm list -> tactic
   514 equal_tac       : thm list -> tactic
   514 equal_tac       : thm list -> tactic
   515 intr_tac        : thm list -> tactic
   515 intr_tac        : thm list -> tactic
   516 \end{ttbox}
   516 \end{ttbox}
   517 Blind application of {\CTT} rules seldom leads to a proof.  The elimination
   517 Blind application of CTT rules seldom leads to a proof.  The elimination
   518 rules, especially, create subgoals containing new unknowns.  These subgoals
   518 rules, especially, create subgoals containing new unknowns.  These subgoals
   519 unify with anything, creating a huge search space.  The standard tactic
   519 unify with anything, creating a huge search space.  The standard tactic
   520 \ttindex{filt_resolve_tac}
   520 \ttindex{filt_resolve_tac}
   521 (see \iflabelundefined{filt_resolve_tac}{the {\em Reference Manual\/}}%
   521 (see \iflabelundefined{filt_resolve_tac}{the {\em Reference Manual\/}}%
   522         {\S\ref{filt_resolve_tac}})
   522         {\S\ref{filt_resolve_tac}})
   523 %
   523 %
   524 fails for goals that are too flexible; so does the {\CTT} tactic {\tt
   524 fails for goals that are too flexible; so does the CTT tactic {\tt
   525   test_assume_tac}.  Used with the tactical \ttindex{REPEAT_FIRST} they
   525   test_assume_tac}.  Used with the tactical \ttindex{REPEAT_FIRST} they
   526 achieve a simple kind of subgoal reordering: the less flexible subgoals are
   526 achieve a simple kind of subgoal reordering: the less flexible subgoals are
   527 attempted first.  Do some single step proofs, or study the examples below,
   527 attempted first.  Do some single step proofs, or study the examples below,
   528 to see why this is necessary.
   528 to see why this is necessary.
   529 \begin{ttdescription}
   529 \begin{ttdescription}
   561 \end{ttbox}
   561 \end{ttbox}
   562 Object-level simplification is accomplished through proof, using the {\tt
   562 Object-level simplification is accomplished through proof, using the {\tt
   563   CTT} equality rules and the built-in rewriting functor
   563   CTT} equality rules and the built-in rewriting functor
   564 {\tt TSimpFun}.%
   564 {\tt TSimpFun}.%
   565 \footnote{This should not be confused with Isabelle's main simplifier; {\tt
   565 \footnote{This should not be confused with Isabelle's main simplifier; {\tt
   566     TSimpFun} is only useful for {\CTT} and similar logics with type
   566     TSimpFun} is only useful for CTT and similar logics with type inference
   567   inference rules.  At present it is undocumented.}
   567   rules.  At present it is undocumented.}
   568 %
   568 %
   569 The rewrites include the computation rules and other equations.  The long
   569 The rewrites include the computation rules and other equations.  The long
   570 versions of the other rules permit rewriting of subterms and subtypes.
   570 versions of the other rules permit rewriting of subterms and subtypes.
   571 Also used are transitivity and the extra judgement form \cdx{Reduce}.
   571 Also used are transitivity and the extra judgement form \cdx{Reduce}.
   572 Meta-level simplification handles only definitional equality.
   572 Meta-level simplification handles only definitional equality.
   581 the assumptions.
   581 the assumptions.
   582 \end{ttdescription}
   582 \end{ttdescription}
   583
   583
   584
   584
   585 \section{Tactics for logical reasoning}
   585 \section{Tactics for logical reasoning}
   586 Interpreting propositions as types lets {\CTT} express statements of
   586 Interpreting propositions as types lets CTT express statements of
   587 intuitionistic logic.  However, Constructive Type Theory is not just
   587 intuitionistic logic.  However, Constructive Type Theory is not just another
   588 another syntax for first-order logic.  There are fundamental differences.
   588 syntax for first-order logic.  There are fundamental differences.
   589
   589
   590 \index{assumptions!in {\CTT}}
   590 \index{assumptions!in CTT}
   591 Can assumptions be deleted after use?  Not every occurrence of a type
   591 Can assumptions be deleted after use?  Not every occurrence of a type
   592 represents a proposition, and Type Theory assumptions declare variables.
   592 represents a proposition, and Type Theory assumptions declare variables.
   593 In first-order logic, $\disj$-elimination with the assumption $P\disj Q$
   593 In first-order logic, $\disj$-elimination with the assumption $P\disj Q$
   594 creates one subgoal assuming $P$ and another assuming $Q$, and $P\disj Q$
   594 creates one subgoal assuming $P$ and another assuming $Q$, and $P\disj Q$
   595 can be deleted safely.  In Type Theory, $+$-elimination with the assumption
   595 can be deleted safely.  In Type Theory, $+$-elimination with the assumption
   596 $z\in A+B$ creates one subgoal assuming $x\in A$ and another assuming $y\in  596$z\in A+B$creates one subgoal assuming$x\in A$and another assuming$y\in
   597 B$(for arbitrary$x$and$y$). Deleting$z\in A+B$when other assumptions  597 B$ (for arbitrary $x$ and $y$).  Deleting $z\in A+B$ when other assumptions
   598 refer to $z$ may render the subgoal unprovable: arguably,
   598 refer to $z$ may render the subgoal unprovable: arguably,
   599 meaningless.
   599 meaningless.
   600
   600
   601 Isabelle provides several tactics for predicate calculus reasoning in \CTT:
   601 Isabelle provides several tactics for predicate calculus reasoning in CTT:
   602 \begin{ttbox}
   602 \begin{ttbox}
   603 mp_tac       : int -> tactic
   603 mp_tac       : int -> tactic
   604 add_mp_tac   : int -> tactic
   604 add_mp_tac   : int -> tactic
   605 safestep_tac : thm list -> int -> tactic
   605 safestep_tac : thm list -> int -> tactic
   606 safe_tac     : thm list -> int -> tactic
   606 safe_tac     : thm list -> int -> tactic
   726 such that $0\leq x \leq a$ and $x\bmod b = 0$.
   726 such that $0\leq x \leq a$ and $x\bmod b = 0$.
   727
   727
   728
   728
   729
   729
   730 \section{The examples directory}
   730 \section{The examples directory}
   731 This directory contains examples and experimental proofs in {\CTT}.
   731 This directory contains examples and experimental proofs in CTT.
   732 \begin{ttdescription}
   732 \begin{ttdescription}
   733 \item[CTT/ex/typechk.ML]
   733 \item[CTT/ex/typechk.ML]
   734 contains simple examples of type-checking and type deduction.
   734 contains simple examples of type-checking and type deduction.
   735
   735
   736 \item[CTT/ex/elim.ML]
   736 \item[CTT/ex/elim.ML]