1.1 --- a/doc-src/Logics/CTT.tex Thu Jul 16 10:35:31 1998 +0200
1.2 +++ b/doc-src/Logics/CTT.tex Thu Jul 16 11:50:01 1998 +0200
1.3 @@ -126,13 +126,13 @@
1.4 \begin{center} \tt\frenchspacing
1.5 \begin{tabular}{rrr}
1.6 \it external & \it internal & \it standard notation \\
1.7 - \sdx{PROD} $x$:$A$ . $B[x]$ & Prod($A$, $\lambda x.B[x]$) &
1.8 + \sdx{PROD} $x$:$A$ . $B[x]$ & Prod($A$, $\lambda x. B[x]$) &
1.9 \rm product $\prod@{x\in A}B[x]$ \\
1.10 - \sdx{SUM} $x$:$A$ . $B[x]$ & Sum($A$, $\lambda x.B[x]$) &
1.11 + \sdx{SUM} $x$:$A$ . $B[x]$ & Sum($A$, $\lambda x. B[x]$) &
1.12 \rm sum $\sum@{x\in A}B[x]$ \\
1.13 - $A$ --> $B$ & Prod($A$, $\lambda x.B$) &
1.14 + $A$ --> $B$ & Prod($A$, $\lambda x. B$) &
1.15 \rm function space $A\to B$ \\
1.16 - $A$ * $B$ & Sum($A$, $\lambda x.B$) &
1.17 + $A$ * $B$ & Sum($A$, $\lambda x. B$) &
1.18 \rm binary product $A\times B$
1.19 \end{tabular}
1.20 \end{center}
1.21 @@ -169,7 +169,7 @@
1.22 the function application operator (sometimes called `apply'), and the
1.23 2-place type operators. Note that meta-level abstraction and application,
1.24 $\lambda x.b$ and $f(a)$, differ from object-level abstraction and
1.25 -application, \hbox{\tt lam $x$.$b$} and $b{\tt`}a$. A {\CTT}
1.26 +application, \hbox{\tt lam $x$. $b$} and $b{\tt`}a$. A {\CTT}
1.27 function~$f$ is simply an individual as far as Isabelle is concerned: its
1.28 Isabelle type is~$i$, not say $i\To i$.
1.29
1.30 @@ -180,8 +180,8 @@
1.31 \index{*SUM symbol}\index{*PROD symbol}
1.32 Quantification is expressed using general sums $\sum@{x\in A}B[x]$ and
1.33 products $\prod@{x\in A}B[x]$. Instead of {\tt Sum($A$,$B$)} and {\tt
1.34 - Prod($A$,$B$)} we may write \hbox{\tt SUM $x$:$A$.$B[x]$} and \hbox{\tt
1.35 - PROD $x$:$A$.$B[x]$}. For example, we may write
1.36 + Prod($A$,$B$)} we may write \hbox{\tt SUM $x$:$A$. $B[x]$} and \hbox{\tt
1.37 + PROD $x$:$A$. $B[x]$}. For example, we may write
1.38 \begin{ttbox}
1.39 SUM y:B. PROD x:A. C(x,y) {\rm for} Sum(B, \%y. Prod(A, \%x. C(x,y)))
1.40 \end{ttbox}
1.41 @@ -232,20 +232,20 @@
1.42
1.43 \tdx{NE} [| p: N; a: C(0);
1.44 !!u v. [| u: N; v: C(u) |] ==> b(u,v): C(succ(u))
1.45 - |] ==> rec(p, a, \%u v.b(u,v)) : C(p)
1.46 + |] ==> rec(p, a, \%u v. b(u,v)) : C(p)
1.47
1.48 \tdx{NEL} [| p = q : N; a = c : C(0);
1.49 !!u v. [| u: N; v: C(u) |] ==> b(u,v)=d(u,v): C(succ(u))
1.50 - |] ==> rec(p, a, \%u v.b(u,v)) = rec(q,c,d) : C(p)
1.51 + |] ==> rec(p, a, \%u v. b(u,v)) = rec(q,c,d) : C(p)
1.52
1.53 \tdx{NC0} [| a: C(0);
1.54 !!u v. [| u: N; v: C(u) |] ==> b(u,v): C(succ(u))
1.55 - |] ==> rec(0, a, \%u v.b(u,v)) = a : C(0)
1.56 + |] ==> rec(0, a, \%u v. b(u,v)) = a : C(0)
1.57
1.58 \tdx{NC_succ} [| p: N; a: C(0);
1.59 !!u v. [| u: N; v: C(u) |] ==> b(u,v): C(succ(u))
1.60 - |] ==> rec(succ(p), a, \%u v.b(u,v)) =
1.61 - b(p, rec(p, a, \%u v.b(u,v))) : C(succ(p))
1.62 + |] ==> rec(succ(p), a, \%u v. b(u,v)) =
1.63 + b(p, rec(p, a, \%u v. b(u,v))) : C(succ(p))
1.64
1.65 \tdx{zero_ne_succ} [| a: N; 0 = succ(a) : N |] ==> 0: F
1.66 \end{ttbox}
1.67 @@ -255,22 +255,22 @@
1.68
1.69 \begin{figure}
1.70 \begin{ttbox}
1.71 -\tdx{ProdF} [| A type; !!x. x:A ==> B(x) type |] ==> PROD x:A.B(x) type
1.72 +\tdx{ProdF} [| A type; !!x. x:A ==> B(x) type |] ==> PROD x:A. B(x) type
1.73 \tdx{ProdFL} [| A = C; !!x. x:A ==> B(x) = D(x) |] ==>
1.74 - PROD x:A.B(x) = PROD x:C.D(x)
1.75 + PROD x:A. B(x) = PROD x:C. D(x)
1.76
1.77 \tdx{ProdI} [| A type; !!x. x:A ==> b(x):B(x)
1.78 - |] ==> lam x.b(x) : PROD x:A.B(x)
1.79 + |] ==> lam x. b(x) : PROD x:A. B(x)
1.80 \tdx{ProdIL} [| A type; !!x. x:A ==> b(x) = c(x) : B(x)
1.81 - |] ==> lam x.b(x) = lam x.c(x) : PROD x:A.B(x)
1.82 + |] ==> lam x. b(x) = lam x. c(x) : PROD x:A. B(x)
1.83
1.84 -\tdx{ProdE} [| p : PROD x:A.B(x); a : A |] ==> p`a : B(a)
1.85 -\tdx{ProdEL} [| p=q: PROD x:A.B(x); a=b : A |] ==> p`a = q`b : B(a)
1.86 +\tdx{ProdE} [| p : PROD x:A. B(x); a : A |] ==> p`a : B(a)
1.87 +\tdx{ProdEL} [| p=q: PROD x:A. B(x); a=b : A |] ==> p`a = q`b : B(a)
1.88
1.89 \tdx{ProdC} [| a : A; !!x. x:A ==> b(x) : B(x)
1.90 - |] ==> (lam x.b(x)) ` a = b(a) : B(a)
1.91 + |] ==> (lam x. b(x)) ` a = b(a) : B(a)
1.92
1.93 -\tdx{ProdC2} p : PROD x:A.B(x) ==> (lam x. p`x) = p : PROD x:A.B(x)
1.94 +\tdx{ProdC2} p : PROD x:A. B(x) ==> (lam x. p`x) = p : PROD x:A. B(x)
1.95 \end{ttbox}
1.96 \caption{Rules for the product type $\prod\sb{x\in A}B[x]$} \label{ctt-prod}
1.97 \end{figure}
1.98 @@ -278,27 +278,27 @@
1.99
1.100 \begin{figure}
1.101 \begin{ttbox}
1.102 -\tdx{SumF} [| A type; !!x. x:A ==> B(x) type |] ==> SUM x:A.B(x) type
1.103 +\tdx{SumF} [| A type; !!x. x:A ==> B(x) type |] ==> SUM x:A. B(x) type
1.104 \tdx{SumFL} [| A = C; !!x. x:A ==> B(x) = D(x)
1.105 - |] ==> SUM x:A.B(x) = SUM x:C.D(x)
1.106 + |] ==> SUM x:A. B(x) = SUM x:C. D(x)
1.107
1.108 -\tdx{SumI} [| a : A; b : B(a) |] ==> <a,b> : SUM x:A.B(x)
1.109 -\tdx{SumIL} [| a=c:A; b=d:B(a) |] ==> <a,b> = <c,d> : SUM x:A.B(x)
1.110 +\tdx{SumI} [| a : A; b : B(a) |] ==> <a,b> : SUM x:A. B(x)
1.111 +\tdx{SumIL} [| a=c:A; b=d:B(a) |] ==> <a,b> = <c,d> : SUM x:A. B(x)
1.112
1.113 -\tdx{SumE} [| p: SUM x:A.B(x);
1.114 +\tdx{SumE} [| p: SUM x:A. B(x);
1.115 !!x y. [| x:A; y:B(x) |] ==> c(x,y): C(<x,y>)
1.116 - |] ==> split(p, \%x y.c(x,y)) : C(p)
1.117 + |] ==> split(p, \%x y. c(x,y)) : C(p)
1.118
1.119 -\tdx{SumEL} [| p=q : SUM x:A.B(x);
1.120 +\tdx{SumEL} [| p=q : SUM x:A. B(x);
1.121 !!x y. [| x:A; y:B(x) |] ==> c(x,y)=d(x,y): C(<x,y>)
1.122 - |] ==> split(p, \%x y.c(x,y)) = split(q, \%x y.d(x,y)) : C(p)
1.123 + |] ==> split(p, \%x y. c(x,y)) = split(q, \%x y. d(x,y)) : C(p)
1.124
1.125 \tdx{SumC} [| a: A; b: B(a);
1.126 !!x y. [| x:A; y:B(x) |] ==> c(x,y): C(<x,y>)
1.127 - |] ==> split(<a,b>, \%x y.c(x,y)) = c(a,b) : C(<a,b>)
1.128 + |] ==> split(<a,b>, \%x y. c(x,y)) = c(a,b) : C(<a,b>)
1.129
1.130 -\tdx{fst_def} fst(a) == split(a, \%x y.x)
1.131 -\tdx{snd_def} snd(a) == split(a, \%x y.y)
1.132 +\tdx{fst_def} fst(a) == split(a, \%x y. x)
1.133 +\tdx{snd_def} snd(a) == split(a, \%x y. y)
1.134 \end{ttbox}
1.135 \caption{Rules for the sum type $\sum\sb{x\in A}B[x]$} \label{ctt-sum}
1.136 \end{figure}
1.137 @@ -318,23 +318,23 @@
1.138 \tdx{PlusE} [| p: A+B;
1.139 !!x. x:A ==> c(x): C(inl(x));
1.140 !!y. y:B ==> d(y): C(inr(y))
1.141 - |] ==> when(p, \%x.c(x), \%y.d(y)) : C(p)
1.142 + |] ==> when(p, \%x. c(x), \%y. d(y)) : C(p)
1.143
1.144 \tdx{PlusEL} [| p = q : A+B;
1.145 !!x. x: A ==> c(x) = e(x) : C(inl(x));
1.146 !!y. y: B ==> d(y) = f(y) : C(inr(y))
1.147 - |] ==> when(p, \%x.c(x), \%y.d(y)) =
1.148 - when(q, \%x.e(x), \%y.f(y)) : C(p)
1.149 + |] ==> when(p, \%x. c(x), \%y. d(y)) =
1.150 + when(q, \%x. e(x), \%y. f(y)) : C(p)
1.151
1.152 \tdx{PlusC_inl} [| a: A;
1.153 !!x. x:A ==> c(x): C(inl(x));
1.154 !!y. y:B ==> d(y): C(inr(y))
1.155 - |] ==> when(inl(a), \%x.c(x), \%y.d(y)) = c(a) : C(inl(a))
1.156 + |] ==> when(inl(a), \%x. c(x), \%y. d(y)) = c(a) : C(inl(a))
1.157
1.158 \tdx{PlusC_inr} [| b: B;
1.159 !!x. x:A ==> c(x): C(inl(x));
1.160 !!y. y:B ==> d(y): C(inr(y))
1.161 - |] ==> when(inr(b), \%x.c(x), \%y.d(y)) = d(b) : C(inr(b))
1.162 + |] ==> when(inr(b), \%x. c(x), \%y. d(y)) = d(b) : C(inr(b))
1.163 \end{ttbox}
1.164 \caption{Rules for the binary sum type $A+B$} \label{ctt-plus}
1.165 \end{figure}
1.166 @@ -458,7 +458,7 @@
1.167 proof of the Axiom of Choice.
1.168
1.169 All the rules are given in $\eta$-expanded form. For instance, every
1.170 -occurrence of $\lambda u\,v.b(u,v)$ could be abbreviated to~$b$ in the
1.171 +occurrence of $\lambda u\,v. b(u,v)$ could be abbreviated to~$b$ in the
1.172 rules for~$N$. The expanded form permits Isabelle to preserve bound
1.173 variable names during backward proof. Names of bound variables in the
1.174 conclusion (here, $u$ and~$v$) are matched with corresponding bound
1.175 @@ -658,16 +658,16 @@
1.176 \end{constants}
1.177
1.178 \begin{ttbox}
1.179 -\tdx{add_def} a#+b == rec(a, b, \%u v.succ(v))
1.180 -\tdx{diff_def} a-b == rec(b, a, \%u v.rec(v, 0, \%x y.x))
1.181 +\tdx{add_def} a#+b == rec(a, b, \%u v. succ(v))
1.182 +\tdx{diff_def} a-b == rec(b, a, \%u v. rec(v, 0, \%x y. x))
1.183 \tdx{absdiff_def} a|-|b == (a-b) #+ (b-a)
1.184 \tdx{mult_def} a#*b == rec(a, 0, \%u v. b #+ v)
1.185
1.186 \tdx{mod_def} a mod b ==
1.187 - rec(a, 0, \%u v. rec(succ(v) |-| b, 0, \%x y.succ(v)))
1.188 + rec(a, 0, \%u v. rec(succ(v) |-| b, 0, \%x y. succ(v)))
1.189
1.190 \tdx{div_def} a div b ==
1.191 - rec(a, 0, \%u v. rec(succ(u) mod b, succ(v), \%x y.v))
1.192 + rec(a, 0, \%u v. rec(succ(u) mod b, succ(v), \%x y. v))
1.193
1.194 \tdx{add_typing} [| a:N; b:N |] ==> a #+ b : N
1.195 \tdx{addC0} b:N ==> 0 #+ b = b : N
1.196 @@ -714,7 +714,7 @@
1.197 recursion, some of their definitions may be obscure.
1.198
1.199 The difference~$a-b$ is computed by taking $b$ predecessors of~$a$, where
1.200 -the predecessor function is $\lambda v. {\tt rec}(v, 0, \lambda x\,y.x)$.
1.201 +the predecessor function is $\lambda v. {\tt rec}(v, 0, \lambda x\,y. x)$.
1.202
1.203 The remainder $a\bmod b$ counts up to~$a$ in a cyclic fashion, using 0
1.204 as the successor of~$b-1$. Absolute difference is used to test the
1.205 @@ -751,7 +751,7 @@
1.206 unknown, takes shape in the course of the proof. Our example is the
1.207 predecessor function on the natural numbers.
1.208 \begin{ttbox}
1.209 -goal CTT.thy "lam n. rec(n, 0, \%x y.x) : ?A";
1.210 +Goal "lam n. rec(n, 0, \%x y. x) : ?A";
1.211 {\out Level 0}
1.212 {\out lam n. rec(n,0,\%x y. x) : ?A}
1.213 {\out 1. lam n. rec(n,0,\%x y. x) : ?A}
1.214 @@ -813,7 +813,7 @@
1.215 unprovable subgoals will be left. As an exercise, try to prove the
1.216 following invalid goal:
1.217 \begin{ttbox}
1.218 -goal CTT.thy "lam n. rec(n, 0, \%x y.tt) : ?A";
1.219 +Goal "lam n. rec(n, 0, \%x y. tt) : ?A";
1.220 \end{ttbox}
1.221
1.222
1.223 @@ -843,7 +843,7 @@
1.224 To begin, we bind the rule's premises --- returned by the~{\tt goal}
1.225 command --- to the {\ML} variable~{\tt prems}.
1.226 \begin{ttbox}
1.227 -val prems = goal CTT.thy
1.228 +val prems = Goal
1.229 "[| A type; \ttback
1.230 \ttback !!x. x:A ==> B(x) type; \ttback
1.231 \ttback !!x. x:A ==> C(x) type; \ttback
1.232 @@ -994,7 +994,7 @@
1.233 called~$f$; Isabelle echoes the type using \verb|-->| because there is no
1.234 explicit dependence upon~$f$.
1.235 \begin{ttbox}
1.236 -val prems = goal CTT.thy
1.237 +val prems = Goal
1.238 "[| A type; !!x. x:A ==> B(x) type; \ttback
1.239 \ttback !!z. z: (SUM x:A. B(x)) ==> C(z) type \ttback
1.240 \ttback |] ==> ?a : PROD f: (PROD z : (SUM x:A . B(x)) . C(z)). \ttback
1.241 @@ -1074,7 +1074,7 @@
1.242 (recall Fig.\ts\ref{ctt-derived}) and the type checking tactics, we can
1.243 prove the theorem in nine steps.
1.244 \begin{ttbox}
1.245 -val prems = goal CTT.thy
1.246 +val prems = Goal
1.247 "[| A type; !!x. x:A ==> B(x) type; \ttback
1.248 \ttback !!x y.[| x:A; y:B(x) |] ==> C(x,y) type \ttback
1.249 \ttback |] ==> ?a : PROD h: (PROD x:A. SUM y:B(x). C(x,y)). \ttback