doc-src/Logics/CTT.tex
 changeset 111 1b3cddf41b2d parent 104 d8205bb279a7 child 114 96c627d2815e
--- a/doc-src/Logics/CTT.tex	Thu Nov 11 12:44:43 1993 +0100
+++ b/doc-src/Logics/CTT.tex	Thu Nov 11 13:18:49 1993 +0100
@@ -24,9 +24,9 @@
$\Imp$:
$\begin{array}{r@{}l} \Forall x@1\ldots x@n. & - \List{x@1\in A@1; - x@2\in A@2(x@1); \cdots \; - x@n\in A@n(x@1,\ldots,x@{n-1})} \Imp \\ + \List{x@1\in A@1; + x@2\in A@2(x@1); \cdots \; + x@n\in A@n(x@1,\ldots,x@{n-1})} \Imp \\ & \qquad\qquad a(x@1,\ldots,x@n)\in A(x@1,\ldots,x@n) \end{array}$
@@ -64,31 +64,31 @@
\begin{figure} \tabcolsep=1em  %wider spacing in tables
\begin{center}
\begin{tabular}{rrr}
-  \it symbol  	& \it meta-type 	& \it description \\
-  \idx{Type}    & $t \to prop$		& judgement form \\
-  \idx{Eqtype}  & $[t,t]\to prop$	& judgement form\\
-  \idx{Elem}    & $[i, t]\to prop$	& judgement form\\
-  \idx{Eqelem}  & $[i, i, t]\to prop$	& judgement form\\
-  \idx{Reduce}  & $[i, i]\to prop$	& extra judgement form\$2ex] + \it symbol & \it meta-type & \it description \\ + \idx{Type} & t \to prop & judgement form \\ + \idx{Eqtype} & [t,t]\to prop & judgement form\\ + \idx{Elem} & [i, t]\to prop & judgement form\\ + \idx{Eqelem} & [i, i, t]\to prop & judgement form\\ + \idx{Reduce} & [i, i]\to prop & extra judgement form\\[2ex] - \idx{N} & t & natural numbers type\\ - \idx{0} & i & constructor\\ - \idx{succ} & i\to i & constructor\\ + \idx{N} & t & natural numbers type\\ + \idx{0} & i & constructor\\ + \idx{succ} & i\to i & constructor\\ \idx{rec} & [i,i,[i,i]\to i]\to i & eliminator\\[2ex] - \idx{Prod} & [t,i\to t]\to t & general product type\\ - \idx{lambda} & (i\to i)\to i & constructor\\[2ex] - \idx{Sum} & [t, i\to t]\to t & general sum type\\ - \idx{pair} & [i,i]\to i & constructor\\ - \idx{split} & [i,[i,i]\to i]\to i & eliminator\\ - \idx{fst} snd & i\to i & projections\\[2ex] - \idx{inl} inr & i\to i & constructors for +\\ + \idx{Prod} & [t,i\to t]\to t & general product type\\ + \idx{lambda} & (i\to i)\to i & constructor\\[2ex] + \idx{Sum} & [t, i\to t]\to t & general sum type\\ + \idx{pair} & [i,i]\to i & constructor\\ + \idx{split} & [i,[i,i]\to i]\to i & eliminator\\ + \idx{fst} snd & i\to i & projections\\[2ex] + \idx{inl} inr & i\to i & constructors for +\\ \idx{when} & [i,i\to i, i\to i]\to i & eliminator for +\\[2ex] - \idx{Eq} & [t,i,i]\to t & equality type\\ - \idx{eq} & i & constructor\\[2ex] - \idx{F} & t & empty type\\ - \idx{contr} & i\to i & eliminator\\[2ex] - \idx{T} & t & singleton type\\ - \idx{tt} & i & constructor + \idx{Eq} & [t,i,i]\to t & equality type\\ + \idx{eq} & i & constructor\\[2ex] + \idx{F} & t & empty type\\ + \idx{contr} & i\to i & eliminator\\[2ex] + \idx{T} & t & singleton type\\ + \idx{tt} & i & constructor \end{tabular} \end{center} \caption{The constants of {\CTT}} \label{ctt-constants} @@ -98,7 +98,7 @@ \begin{figure} \tabcolsep=1em %wider spacing in tables \begin{center} \begin{tabular}{llrrr} - \it symbol &\it name &\it meta-type & \it precedence & \it description \\ + \it symbol &\it name &\it meta-type & \it precedence & \it description \\ \idx{lam} & \idx{lambda} & (i\To o)\To i & 10 & \lambda-abstraction \end{tabular} \end{center} @@ -109,8 +109,8 @@ \indexbold{*"+} \begin{tabular}{rrrr} \it symbol & \it meta-type & \it precedence & \it description \\ - \tt  & [i,i]\to i & Left 55 & function application\\ - \tt + & [t,t]\to t & Right 30 & sum of two types + \tt  & [i,i]\to i & Left 55 & function application\\ + \tt + & [t,t]\to t & Right 30 & sum of two types \end{tabular} \end{center} \subcaption{Infixes} @@ -119,15 +119,15 @@ \indexbold{*"-"-">} \begin{center} \tt\frenchspacing \begin{tabular}{rrr} - \it external & \it internal & \it standard notation \\ - \idx{PROD} x:A . B[x] & Prod(A, \lambda x.B[x]) & - \rm product \prod@{x\in A}B[x] \\ - \idx{SUM} x:A . B[x] & Sum(A, \lambda x.B[x]) & - \rm sum \sum@{x\in A}B[x] \\ + \it external & \it internal & \it standard notation \\ + \idx{PROD} x:A . B[x] & Prod(A, \lambda x.B[x]) & + \rm product \prod@{x\in A}B[x] \\ + \idx{SUM} x:A . B[x] & Sum(A, \lambda x.B[x]) & + \rm sum \sum@{x\in A}B[x] \\ A --> B & Prod(A, \lambda x.B) & - \rm function space A\to B \\ + \rm function space A\to B \\ A * B & Sum(A, \lambda x.B) & - \rm binary product A\times B + \rm binary product A\times B \end{tabular} \end{center} \subcaption{Translations} @@ -136,18 +136,18 @@ \begin{center} \dquotes \[ \begin{array}{rcl} -prop & = & type " type" \\ - & | & type " = " type \\ - & | & term " : " type \\ - & | & term " = " term " : " type +prop & = & type " type" \\ + & | & type " = " type \\ + & | & term " : " type \\ + & | & term " = " term " : " type \\[2ex] -type & = & \hbox{expression of type~t} \\ - & | & "PROD~" id " : " type " . " type \\ - & | & "SUM~~" id " : " type " . " type +type & = & \hbox{expression of type~t} \\ + & | & "PROD~" id " : " type " . " type \\ + & | & "SUM~~" id " : " type " . " type \\[2ex] -term & = & \hbox{expression of type~i} \\ - & | & "lam " id~id^* " . " term \\ - & | & "< " term " , " term " >" +term & = & \hbox{expression of type~i} \\ + & | & "lam " id~id^* " . " term \\ + & | & "< " term " , " term " >" \end{array}$
\end{center}
@@ -594,11 +594,11 @@
\idx{absdiff_def}       a|-|b == (a-b) #+ (b-a)
\idx{mult_def}          a#*b  == rec(a, 0, %u v. b #+ v)

-\idx{mod_def}   a//b == rec(a, 0,
+\idx{mod_def}   a mod b == rec(a, 0,
%u v. rec(succ(v) |-| b, 0, %x y.succ(v)))

-\idx{quo_def}   a/b == rec(a, 0,
-                      %u v. rec(succ(u) // b, succ(v), %x y.v))
+\idx{div_def}   a div b == rec(a, 0,
+                      %u v. rec(succ(u) mod b, succ(v), %x y.v))
\end{ttbox}
\subcaption{Definitions of the operators}

@@ -645,20 +645,20 @@
theory has the {\ML} identifier \ttindexbold{arith.thy}.  All proofs are on
the file \ttindexbold{CTT/arith.ML}.

-The operators~\verb'#+', \verb'-', \verb'|-|', \verb'#*', \verb'//'
-and~\verb'/' stand for sum, difference, absolute difference, product,
+The operators~\verb'#+', \verb'-', \verb'|-|', \verb'#*', \verb'mod'
+and~\verb'div' stand for sum, difference, absolute difference, product,
remainder and quotient, respectively.  Since Type Theory has only primitive
recursion, some of their definitions may be obscure.

The difference~$a-b$ is computed by taking $b$ predecessors of~$a$, where
the predecessor function is $\lambda v. {\tt rec}(v, 0, \lambda x\,y.x)$.

-The remainder $a//b$ counts up to~$a$ in a cyclic fashion, using 0 as the
-successor of~$b-1$.  Absolute difference is used to test the equality
-$succ(v)=b$.
+The remainder $a\bmod b$ counts up to~$a$ in a cyclic fashion, using 0
+as the successor of~$b-1$.  Absolute difference is used to test the
+equality $succ(v)=b$.

-The quotient $a//b$ is computed by adding one for every number $x$ such
-that $0\leq x \leq a$ and $x//b = 0$.
+The quotient $a/b$ is computed by adding one for every number $x$
+such that $0\leq x \leq a$ and $x\bmod b = 0$.

@@ -775,6 +775,11 @@
{\out Level 0}
{\out ?a : (SUM x:A. B(x)) + (SUM x:A. C(x))}
{\out  1. ?a : (SUM x:A. B(x)) + (SUM x:A. C(x))}
+{\out val prems = ["A type  [A type]",}
+{\out              "?x : A ==> B(?x) type  [!!x. x : A ==> B(x) type]",}
+{\out              "?x : A ==> C(?x) type  [!!x. x : A ==> C(x) type]",}
+{\out              "p : SUM x:A. B(x) + C(x)  [p : SUM x:A. B(x) + C(x)]"]}
+{\out             : thm list}
\end{ttbox}
One of the premises involves summation ($\Sigma$).  Since it is a premise
rather than the assumption of a goal, it cannot be found by
@@ -901,6 +906,10 @@
{\out ?a : (PROD z:SUM x:A. B(x). C(z)) --> (PROD x:A. PROD y:B(x). C(<x,y>))}
{\out  1. ?a : (PROD z:SUM x:A. B(x). C(z)) -->}
{\out          (PROD x:A. PROD y:B(x). C(<x,y>))}
+{\out val prems = ["A type  [A type]",}
+{\out              "?x : A ==> B(?x) type  [!!x. x : A ==> B(x) type]",}
+{\out              "?z : SUM x:A. B(x) ==> C(?z) type}
+{\out               [!!z. z : SUM x:A. B(x) ==> C(z) type]"] : thm list}
\end{ttbox}
This is an opportunity to demonstrate \ttindex{intr_tac}.  Here, the tactic
repeatedly applies $\Pi$-introduction, automatically proving the rather
@@ -970,6 +979,12 @@
{\out      (SUM f:PROD x:A. B(x). PROD x:A. C(x,f  x))}
{\out  1. ?a : (PROD x:A. SUM y:B(x). C(x,y)) -->}
{\out          (SUM f:PROD x:A. B(x). PROD x:A. C(x,f  x))}
+\ttbreak
+{\out val prems = ["A type  [A type]",}
+{\out              "?x : A ==> B(?x) type  [!!x. x : A ==> B(x) type]",}
+{\out              "[| ?x : A; ?y : B(?x) |] ==> C(?x, ?y) type}
+{\out               [!!x y. [| x : A; y : B(x) |] ==> C(x, y) type]"]}
+{\out             : thm list}
\end{ttbox}
First, \ttindex{intr_tac} applies introduction rules and performs routine
type checking.  This instantiates~$\Var{a}$ to a construction involving