1.1 --- a/doc-src/Logics/CTT.tex Thu Nov 11 12:44:43 1993 +0100
1.2 +++ b/doc-src/Logics/CTT.tex Thu Nov 11 13:18:49 1993 +0100
1.3 @@ -24,9 +24,9 @@
1.4 $\Imp$:
1.5 \[ \begin{array}{r@{}l}
1.6 \Forall x@1\ldots x@n. &
1.7 - \List{x@1\in A@1;
1.8 - x@2\in A@2(x@1); \cdots \;
1.9 - x@n\in A@n(x@1,\ldots,x@{n-1})} \Imp \\
1.10 + \List{x@1\in A@1;
1.11 + x@2\in A@2(x@1); \cdots \;
1.12 + x@n\in A@n(x@1,\ldots,x@{n-1})} \Imp \\
1.13 & \qquad\qquad a(x@1,\ldots,x@n)\in A(x@1,\ldots,x@n)
1.14 \end{array}
1.15 \]
1.16 @@ -64,31 +64,31 @@
1.17 \begin{figure} \tabcolsep=1em %wider spacing in tables
1.18 \begin{center}
1.19 \begin{tabular}{rrr}
1.20 - \it symbol & \it meta-type & \it description \\
1.21 - \idx{Type} & $t \to prop$ & judgement form \\
1.22 - \idx{Eqtype} & $[t,t]\to prop$ & judgement form\\
1.23 - \idx{Elem} & $[i, t]\to prop$ & judgement form\\
1.24 - \idx{Eqelem} & $[i, i, t]\to prop$ & judgement form\\
1.25 - \idx{Reduce} & $[i, i]\to prop$ & extra judgement form\\[2ex]
1.26 + \it symbol & \it meta-type & \it description \\
1.27 + \idx{Type} & $t \to prop$ & judgement form \\
1.28 + \idx{Eqtype} & $[t,t]\to prop$ & judgement form\\
1.29 + \idx{Elem} & $[i, t]\to prop$ & judgement form\\
1.30 + \idx{Eqelem} & $[i, i, t]\to prop$ & judgement form\\
1.31 + \idx{Reduce} & $[i, i]\to prop$ & extra judgement form\\[2ex]
1.32
1.33 - \idx{N} & $t$ & natural numbers type\\
1.34 - \idx{0} & $i$ & constructor\\
1.35 - \idx{succ} & $i\to i$ & constructor\\
1.36 + \idx{N} & $t$ & natural numbers type\\
1.37 + \idx{0} & $i$ & constructor\\
1.38 + \idx{succ} & $i\to i$ & constructor\\
1.39 \idx{rec} & $[i,i,[i,i]\to i]\to i$ & eliminator\\[2ex]
1.40 - \idx{Prod} & $[t,i\to t]\to t$ & general product type\\
1.41 - \idx{lambda} & $(i\to i)\to i$ & constructor\\[2ex]
1.42 - \idx{Sum} & $[t, i\to t]\to t$ & general sum type\\
1.43 - \idx{pair} & $[i,i]\to i$ & constructor\\
1.44 - \idx{split} & $[i,[i,i]\to i]\to i$ & eliminator\\
1.45 - \idx{fst} snd & $i\to i$ & projections\\[2ex]
1.46 - \idx{inl} inr & $i\to i$ & constructors for $+$\\
1.47 + \idx{Prod} & $[t,i\to t]\to t$ & general product type\\
1.48 + \idx{lambda} & $(i\to i)\to i$ & constructor\\[2ex]
1.49 + \idx{Sum} & $[t, i\to t]\to t$ & general sum type\\
1.50 + \idx{pair} & $[i,i]\to i$ & constructor\\
1.51 + \idx{split} & $[i,[i,i]\to i]\to i$ & eliminator\\
1.52 + \idx{fst} snd & $i\to i$ & projections\\[2ex]
1.53 + \idx{inl} inr & $i\to i$ & constructors for $+$\\
1.54 \idx{when} & $[i,i\to i, i\to i]\to i$ & eliminator for $+$\\[2ex]
1.55 - \idx{Eq} & $[t,i,i]\to t$ & equality type\\
1.56 - \idx{eq} & $i$ & constructor\\[2ex]
1.57 - \idx{F} & $t$ & empty type\\
1.58 - \idx{contr} & $i\to i$ & eliminator\\[2ex]
1.59 - \idx{T} & $t$ & singleton type\\
1.60 - \idx{tt} & $i$ & constructor
1.61 + \idx{Eq} & $[t,i,i]\to t$ & equality type\\
1.62 + \idx{eq} & $i$ & constructor\\[2ex]
1.63 + \idx{F} & $t$ & empty type\\
1.64 + \idx{contr} & $i\to i$ & eliminator\\[2ex]
1.65 + \idx{T} & $t$ & singleton type\\
1.66 + \idx{tt} & $i$ & constructor
1.67 \end{tabular}
1.68 \end{center}
1.69 \caption{The constants of {\CTT}} \label{ctt-constants}
1.70 @@ -98,7 +98,7 @@
1.71 \begin{figure} \tabcolsep=1em %wider spacing in tables
1.72 \begin{center}
1.73 \begin{tabular}{llrrr}
1.74 - \it symbol &\it name &\it meta-type & \it precedence & \it description \\
1.75 + \it symbol &\it name &\it meta-type & \it precedence & \it description \\
1.76 \idx{lam} & \idx{lambda} & $(i\To o)\To i$ & 10 & $\lambda$-abstraction
1.77 \end{tabular}
1.78 \end{center}
1.79 @@ -109,8 +109,8 @@
1.80 \indexbold{*"+}
1.81 \begin{tabular}{rrrr}
1.82 \it symbol & \it meta-type & \it precedence & \it description \\
1.83 - \tt ` & $[i,i]\to i$ & Left 55 & function application\\
1.84 - \tt + & $[t,t]\to t$ & Right 30 & sum of two types
1.85 + \tt ` & $[i,i]\to i$ & Left 55 & function application\\
1.86 + \tt + & $[t,t]\to t$ & Right 30 & sum of two types
1.87 \end{tabular}
1.88 \end{center}
1.89 \subcaption{Infixes}
1.90 @@ -119,15 +119,15 @@
1.91 \indexbold{*"-"-">}
1.92 \begin{center} \tt\frenchspacing
1.93 \begin{tabular}{rrr}
1.94 - \it external & \it internal & \it standard notation \\
1.95 - \idx{PROD} $x$:$A$ . $B[x]$ & Prod($A$, $\lambda x.B[x]$) &
1.96 - \rm product $\prod@{x\in A}B[x]$ \\
1.97 - \idx{SUM} $x$:$A$ . $B[x]$ & Sum($A$, $\lambda x.B[x]$) &
1.98 - \rm sum $\sum@{x\in A}B[x]$ \\
1.99 + \it external & \it internal & \it standard notation \\
1.100 + \idx{PROD} $x$:$A$ . $B[x]$ & Prod($A$, $\lambda x.B[x]$) &
1.101 + \rm product $\prod@{x\in A}B[x]$ \\
1.102 + \idx{SUM} $x$:$A$ . $B[x]$ & Sum($A$, $\lambda x.B[x]$) &
1.103 + \rm sum $\sum@{x\in A}B[x]$ \\
1.104 $A$ --> $B$ & Prod($A$, $\lambda x.B$) &
1.105 - \rm function space $A\to B$ \\
1.106 + \rm function space $A\to B$ \\
1.107 $A$ * $B$ & Sum($A$, $\lambda x.B$) &
1.108 - \rm binary product $A\times B$
1.109 + \rm binary product $A\times B$
1.110 \end{tabular}
1.111 \end{center}
1.112 \subcaption{Translations}
1.113 @@ -136,18 +136,18 @@
1.114 \begin{center}
1.115 \dquotes
1.116 \[ \begin{array}{rcl}
1.117 -prop & = & type " type" \\
1.118 - & | & type " = " type \\
1.119 - & | & term " : " type \\
1.120 - & | & term " = " term " : " type
1.121 +prop & = & type " type" \\
1.122 + & | & type " = " type \\
1.123 + & | & term " : " type \\
1.124 + & | & term " = " term " : " type
1.125 \\[2ex]
1.126 -type & = & \hbox{expression of type~$t$} \\
1.127 - & | & "PROD~" id " : " type " . " type \\
1.128 - & | & "SUM~~" id " : " type " . " type
1.129 +type & = & \hbox{expression of type~$t$} \\
1.130 + & | & "PROD~" id " : " type " . " type \\
1.131 + & | & "SUM~~" id " : " type " . " type
1.132 \\[2ex]
1.133 -term & = & \hbox{expression of type~$i$} \\
1.134 - & | & "lam " id~id^* " . " term \\
1.135 - & | & "< " term " , " term " >"
1.136 +term & = & \hbox{expression of type~$i$} \\
1.137 + & | & "lam " id~id^* " . " term \\
1.138 + & | & "< " term " , " term " >"
1.139 \end{array}
1.140 \]
1.141 \end{center}
1.142 @@ -594,11 +594,11 @@
1.143 \idx{absdiff_def} a|-|b == (a-b) #+ (b-a)
1.144 \idx{mult_def} a#*b == rec(a, 0, %u v. b #+ v)
1.145
1.146 -\idx{mod_def} a//b == rec(a, 0,
1.147 +\idx{mod_def} a mod b == rec(a, 0,
1.148 %u v. rec(succ(v) |-| b, 0, %x y.succ(v)))
1.149
1.150 -\idx{quo_def} a/b == rec(a, 0,
1.151 - %u v. rec(succ(u) // b, succ(v), %x y.v))
1.152 +\idx{div_def} a div b == rec(a, 0,
1.153 + %u v. rec(succ(u) mod b, succ(v), %x y.v))
1.154 \end{ttbox}
1.155 \subcaption{Definitions of the operators}
1.156
1.157 @@ -645,20 +645,20 @@
1.158 theory has the {\ML} identifier \ttindexbold{arith.thy}. All proofs are on
1.159 the file \ttindexbold{CTT/arith.ML}.
1.160
1.161 -The operators~\verb'#+', \verb'-', \verb'|-|', \verb'#*', \verb'//'
1.162 -and~\verb'/' stand for sum, difference, absolute difference, product,
1.163 +The operators~\verb'#+', \verb'-', \verb'|-|', \verb'#*', \verb'mod'
1.164 +and~\verb'div' stand for sum, difference, absolute difference, product,
1.165 remainder and quotient, respectively. Since Type Theory has only primitive
1.166 recursion, some of their definitions may be obscure.
1.167
1.168 The difference~$a-b$ is computed by taking $b$ predecessors of~$a$, where
1.169 the predecessor function is $\lambda v. {\tt rec}(v, 0, \lambda x\,y.x)$.
1.170
1.171 -The remainder $a//b$ counts up to~$a$ in a cyclic fashion, using 0 as the
1.172 -successor of~$b-1$. Absolute difference is used to test the equality
1.173 -$succ(v)=b$.
1.174 +The remainder $a\bmod b$ counts up to~$a$ in a cyclic fashion, using 0
1.175 +as the successor of~$b-1$. Absolute difference is used to test the
1.176 +equality $succ(v)=b$.
1.177
1.178 -The quotient $a//b$ is computed by adding one for every number $x$ such
1.179 -that $0\leq x \leq a$ and $x//b = 0$.
1.180 +The quotient $a/b$ is computed by adding one for every number $x$
1.181 +such that $0\leq x \leq a$ and $x\bmod b = 0$.
1.182
1.183
1.184
1.185 @@ -775,6 +775,11 @@
1.186 {\out Level 0}
1.187 {\out ?a : (SUM x:A. B(x)) + (SUM x:A. C(x))}
1.188 {\out 1. ?a : (SUM x:A. B(x)) + (SUM x:A. C(x))}
1.189 +{\out val prems = ["A type [A type]",}
1.190 +{\out "?x : A ==> B(?x) type [!!x. x : A ==> B(x) type]",}
1.191 +{\out "?x : A ==> C(?x) type [!!x. x : A ==> C(x) type]",}
1.192 +{\out "p : SUM x:A. B(x) + C(x) [p : SUM x:A. B(x) + C(x)]"]}
1.193 +{\out : thm list}
1.194 \end{ttbox}
1.195 One of the premises involves summation ($\Sigma$). Since it is a premise
1.196 rather than the assumption of a goal, it cannot be found by
1.197 @@ -901,6 +906,10 @@
1.198 {\out ?a : (PROD z:SUM x:A. B(x). C(z)) --> (PROD x:A. PROD y:B(x). C(<x,y>))}
1.199 {\out 1. ?a : (PROD z:SUM x:A. B(x). C(z)) -->}
1.200 {\out (PROD x:A. PROD y:B(x). C(<x,y>))}
1.201 +{\out val prems = ["A type [A type]",}
1.202 +{\out "?x : A ==> B(?x) type [!!x. x : A ==> B(x) type]",}
1.203 +{\out "?z : SUM x:A. B(x) ==> C(?z) type}
1.204 +{\out [!!z. z : SUM x:A. B(x) ==> C(z) type]"] : thm list}
1.205 \end{ttbox}
1.206 This is an opportunity to demonstrate \ttindex{intr_tac}. Here, the tactic
1.207 repeatedly applies $\Pi$-introduction, automatically proving the rather
1.208 @@ -970,6 +979,12 @@
1.209 {\out (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))}
1.210 {\out 1. ?a : (PROD x:A. SUM y:B(x). C(x,y)) -->}
1.211 {\out (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))}
1.212 +\ttbreak
1.213 +{\out val prems = ["A type [A type]",}
1.214 +{\out "?x : A ==> B(?x) type [!!x. x : A ==> B(x) type]",}
1.215 +{\out "[| ?x : A; ?y : B(?x) |] ==> C(?x, ?y) type}
1.216 +{\out [!!x y. [| x : A; y : B(x) |] ==> C(x, y) type]"]}
1.217 +{\out : thm list}
1.218 \end{ttbox}
1.219 First, \ttindex{intr_tac} applies introduction rules and performs routine
1.220 type checking. This instantiates~$\Var{a}$ to a construction involving