diff -r 6e2e9b92c301 -r 1e944fe5ce96 doc-src/Logics/CTT.tex --- a/doc-src/Logics/CTT.tex Thu Jul 16 10:35:31 1998 +0200 +++ b/doc-src/Logics/CTT.tex Thu Jul 16 11:50:01 1998 +0200 @@ -126,13 +126,13 @@ \begin{center} \tt\frenchspacing \begin{tabular}{rrr} \it external & \it internal & \it standard notation \\ - \sdx{PROD} $x$:$A$ . $B[x]$ & Prod($A$, $\lambda x.B[x]$) & + \sdx{PROD} $x$:$A$ . $B[x]$ & Prod($A$, $\lambda x. B[x]$) & \rm product $\prod@{x\in A}B[x]$ \\ - \sdx{SUM} $x$:$A$ . $B[x]$ & Sum($A$, $\lambda x.B[x]$) & + \sdx{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$) & + $A$ --> $B$ & Prod($A$, $\lambda x. B$) & \rm function space $A\to B$ \\ - $A$ * $B$ & Sum($A$, $\lambda x.B$) & + $A$ * $B$ & Sum($A$, $\lambda x. B$) & \rm binary product $A\times B$ \end{tabular} \end{center} @@ -169,7 +169,7 @@ the function application operator (sometimes called `apply'), and the 2-place type operators. Note that meta-level abstraction and application, $\lambda x.b$ and $f(a)$, differ from object-level abstraction and -application, \hbox{\tt lam $x$.$b$} and $b{\tt`}a$. A {\CTT} +application, \hbox{\tt lam $x$. $b$} and $b{\tt`}a$. A {\CTT} function~$f$ is simply an individual as far as Isabelle is concerned: its Isabelle type is~$i$, not say $i\To i$. @@ -180,8 +180,8 @@ \index{*SUM symbol}\index{*PROD symbol} Quantification is expressed using general sums $\sum@{x\in A}B[x]$ and products $\prod@{x\in A}B[x]$. Instead of {\tt Sum($A$,$B$)} and {\tt - Prod($A$,$B$)} we may write \hbox{\tt SUM $x$:$A$.$B[x]$} and \hbox{\tt - PROD $x$:$A$.$B[x]$}. For example, we may write + Prod($A$,$B$)} we may write \hbox{\tt SUM $x$:$A$. $B[x]$} and \hbox{\tt + PROD $x$:$A$. $B[x]$}. For example, we may write \begin{ttbox} SUM y:B. PROD x:A. C(x,y) {\rm for} Sum(B, \%y. Prod(A, \%x. C(x,y))) \end{ttbox} @@ -232,20 +232,20 @@ \tdx{NE} [| p: N; a: C(0); !!u v. [| u: N; v: C(u) |] ==> b(u,v): C(succ(u)) - |] ==> rec(p, a, \%u v.b(u,v)) : C(p) + |] ==> rec(p, a, \%u v. b(u,v)) : C(p) \tdx{NEL} [| p = q : N; a = c : C(0); !!u v. [| u: N; v: C(u) |] ==> b(u,v)=d(u,v): C(succ(u)) - |] ==> rec(p, a, \%u v.b(u,v)) = rec(q,c,d) : C(p) + |] ==> rec(p, a, \%u v. b(u,v)) = rec(q,c,d) : C(p) \tdx{NC0} [| a: C(0); !!u v. [| u: N; v: C(u) |] ==> b(u,v): C(succ(u)) - |] ==> rec(0, a, \%u v.b(u,v)) = a : C(0) + |] ==> rec(0, a, \%u v. b(u,v)) = a : C(0) \tdx{NC_succ} [| p: N; a: C(0); !!u v. [| u: N; v: C(u) |] ==> b(u,v): C(succ(u)) - |] ==> rec(succ(p), a, \%u v.b(u,v)) = - b(p, rec(p, a, \%u v.b(u,v))) : C(succ(p)) + |] ==> rec(succ(p), a, \%u v. b(u,v)) = + b(p, rec(p, a, \%u v. b(u,v))) : C(succ(p)) \tdx{zero_ne_succ} [| a: N; 0 = succ(a) : N |] ==> 0: F \end{ttbox} @@ -255,22 +255,22 @@ \begin{figure} \begin{ttbox} -\tdx{ProdF} [| A type; !!x. x:A ==> B(x) type |] ==> PROD x:A.B(x) type +\tdx{ProdF} [| A type; !!x. x:A ==> B(x) type |] ==> PROD x:A. B(x) type \tdx{ProdFL} [| A = C; !!x. x:A ==> B(x) = D(x) |] ==> - PROD x:A.B(x) = PROD x:C.D(x) + PROD x:A. B(x) = PROD x:C. D(x) \tdx{ProdI} [| A type; !!x. x:A ==> b(x):B(x) - |] ==> lam x.b(x) : PROD x:A.B(x) + |] ==> lam x. b(x) : PROD x:A. B(x) \tdx{ProdIL} [| A type; !!x. x:A ==> b(x) = c(x) : B(x) - |] ==> lam x.b(x) = lam x.c(x) : PROD x:A.B(x) + |] ==> lam x. b(x) = lam x. c(x) : PROD x:A. B(x) -\tdx{ProdE} [| p : PROD x:A.B(x); a : A |] ==> p`a : B(a) -\tdx{ProdEL} [| p=q: PROD x:A.B(x); a=b : A |] ==> p`a = q`b : B(a) +\tdx{ProdE} [| p : PROD x:A. B(x); a : A |] ==> p`a : B(a) +\tdx{ProdEL} [| p=q: PROD x:A. B(x); a=b : A |] ==> p`a = q`b : B(a) \tdx{ProdC} [| a : A; !!x. x:A ==> b(x) : B(x) - |] ==> (lam x.b(x)) ` a = b(a) : B(a) + |] ==> (lam x. b(x)) ` a = b(a) : B(a) -\tdx{ProdC2} p : PROD x:A.B(x) ==> (lam x. p`x) = p : PROD x:A.B(x) +\tdx{ProdC2} p : PROD x:A. B(x) ==> (lam x. p`x) = p : PROD x:A. B(x) \end{ttbox} \caption{Rules for the product type $\prod\sb{x\in A}B[x]$} \label{ctt-prod} \end{figure} @@ -278,27 +278,27 @@ \begin{figure} \begin{ttbox} -\tdx{SumF} [| A type; !!x. x:A ==> B(x) type |] ==> SUM x:A.B(x) type +\tdx{SumF} [| A type; !!x. x:A ==> B(x) type |] ==> SUM x:A. B(x) type \tdx{SumFL} [| A = C; !!x. x:A ==> B(x) = D(x) - |] ==> SUM x:A.B(x) = SUM x:C.D(x) + |] ==> SUM x:A. B(x) = SUM x:C. D(x) -\tdx{SumI} [| a : A; b : B(a) |] ==> : SUM x:A.B(x) -\tdx{SumIL} [| a=c:A; b=d:B(a) |] ==> = : SUM x:A.B(x) +\tdx{SumI} [| a : A; b : B(a) |] ==> : SUM x:A. B(x) +\tdx{SumIL} [| a=c:A; b=d:B(a) |] ==> = : SUM x:A. B(x) -\tdx{SumE} [| p: SUM x:A.B(x); +\tdx{SumE} [| p: SUM x:A. B(x); !!x y. [| x:A; y:B(x) |] ==> c(x,y): C() - |] ==> split(p, \%x y.c(x,y)) : C(p) + |] ==> split(p, \%x y. c(x,y)) : C(p) -\tdx{SumEL} [| p=q : SUM x:A.B(x); +\tdx{SumEL} [| p=q : SUM x:A. B(x); !!x y. [| x:A; y:B(x) |] ==> c(x,y)=d(x,y): C() - |] ==> split(p, \%x y.c(x,y)) = split(q, \%x y.d(x,y)) : C(p) + |] ==> split(p, \%x y. c(x,y)) = split(q, \%x y. d(x,y)) : C(p) \tdx{SumC} [| a: A; b: B(a); !!x y. [| x:A; y:B(x) |] ==> c(x,y): C() - |] ==> split(, \%x y.c(x,y)) = c(a,b) : C() + |] ==> split(, \%x y. c(x,y)) = c(a,b) : C() -\tdx{fst_def} fst(a) == split(a, \%x y.x) -\tdx{snd_def} snd(a) == split(a, \%x y.y) +\tdx{fst_def} fst(a) == split(a, \%x y. x) +\tdx{snd_def} snd(a) == split(a, \%x y. y) \end{ttbox} \caption{Rules for the sum type $\sum\sb{x\in A}B[x]$} \label{ctt-sum} \end{figure} @@ -318,23 +318,23 @@ \tdx{PlusE} [| p: A+B; !!x. x:A ==> c(x): C(inl(x)); !!y. y:B ==> d(y): C(inr(y)) - |] ==> when(p, \%x.c(x), \%y.d(y)) : C(p) + |] ==> when(p, \%x. c(x), \%y. d(y)) : C(p) \tdx{PlusEL} [| p = q : A+B; !!x. x: A ==> c(x) = e(x) : C(inl(x)); !!y. y: B ==> d(y) = f(y) : C(inr(y)) - |] ==> when(p, \%x.c(x), \%y.d(y)) = - when(q, \%x.e(x), \%y.f(y)) : C(p) + |] ==> when(p, \%x. c(x), \%y. d(y)) = + when(q, \%x. e(x), \%y. f(y)) : C(p) \tdx{PlusC_inl} [| a: A; !!x. x:A ==> c(x): C(inl(x)); !!y. y:B ==> d(y): C(inr(y)) - |] ==> when(inl(a), \%x.c(x), \%y.d(y)) = c(a) : C(inl(a)) + |] ==> when(inl(a), \%x. c(x), \%y. d(y)) = c(a) : C(inl(a)) \tdx{PlusC_inr} [| b: B; !!x. x:A ==> c(x): C(inl(x)); !!y. y:B ==> d(y): C(inr(y)) - |] ==> when(inr(b), \%x.c(x), \%y.d(y)) = d(b) : C(inr(b)) + |] ==> when(inr(b), \%x. c(x), \%y. d(y)) = d(b) : C(inr(b)) \end{ttbox} \caption{Rules for the binary sum type $A+B$} \label{ctt-plus} \end{figure} @@ -458,7 +458,7 @@ proof of the Axiom of Choice. All the rules are given in $\eta$-expanded form. For instance, every -occurrence of $\lambda u\,v.b(u,v)$ could be abbreviated to~$b$ in the +occurrence of $\lambda u\,v. b(u,v)$ could be abbreviated to~$b$ in the rules for~$N$. The expanded form permits Isabelle to preserve bound variable names during backward proof. Names of bound variables in the conclusion (here, $u$ and~$v$) are matched with corresponding bound @@ -658,16 +658,16 @@ \end{constants} \begin{ttbox} -\tdx{add_def} a#+b == rec(a, b, \%u v.succ(v)) -\tdx{diff_def} a-b == rec(b, a, \%u v.rec(v, 0, \%x y.x)) +\tdx{add_def} a#+b == rec(a, b, \%u v. succ(v)) +\tdx{diff_def} a-b == rec(b, a, \%u v. rec(v, 0, \%x y. x)) \tdx{absdiff_def} a|-|b == (a-b) #+ (b-a) \tdx{mult_def} a#*b == rec(a, 0, \%u v. b #+ v) \tdx{mod_def} a mod b == - rec(a, 0, \%u v. rec(succ(v) |-| b, 0, \%x y.succ(v))) + rec(a, 0, \%u v. rec(succ(v) |-| b, 0, \%x y. succ(v))) \tdx{div_def} a div b == - rec(a, 0, \%u v. rec(succ(u) mod b, succ(v), \%x y.v)) + rec(a, 0, \%u v. rec(succ(u) mod b, succ(v), \%x y. v)) \tdx{add_typing} [| a:N; b:N |] ==> a #+ b : N \tdx{addC0} b:N ==> 0 #+ b = b : N @@ -714,7 +714,7 @@ 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 predecessor function is $\lambda v. {\tt rec}(v, 0, \lambda x\,y. x)$. 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 @@ -751,7 +751,7 @@ unknown, takes shape in the course of the proof. Our example is the predecessor function on the natural numbers. \begin{ttbox} -goal CTT.thy "lam n. rec(n, 0, \%x y.x) : ?A"; +Goal "lam n. rec(n, 0, \%x y. x) : ?A"; {\out Level 0} {\out lam n. rec(n,0,\%x y. x) : ?A} {\out 1. lam n. rec(n,0,\%x y. x) : ?A} @@ -813,7 +813,7 @@ unprovable subgoals will be left. As an exercise, try to prove the following invalid goal: \begin{ttbox} -goal CTT.thy "lam n. rec(n, 0, \%x y.tt) : ?A"; +Goal "lam n. rec(n, 0, \%x y. tt) : ?A"; \end{ttbox} @@ -843,7 +843,7 @@ To begin, we bind the rule's premises --- returned by the~{\tt goal} command --- to the {\ML} variable~{\tt prems}. \begin{ttbox} -val prems = goal CTT.thy +val prems = Goal "[| A type; \ttback \ttback !!x. x:A ==> B(x) type; \ttback \ttback !!x. x:A ==> C(x) type; \ttback @@ -994,7 +994,7 @@ called~$f$; Isabelle echoes the type using \verb|-->| because there is no explicit dependence upon~$f$. \begin{ttbox} -val prems = goal CTT.thy +val prems = Goal "[| A type; !!x. x:A ==> B(x) type; \ttback \ttback !!z. z: (SUM x:A. B(x)) ==> C(z) type \ttback \ttback |] ==> ?a : PROD f: (PROD z : (SUM x:A . B(x)) . C(z)). \ttback @@ -1074,7 +1074,7 @@ (recall Fig.\ts\ref{ctt-derived}) and the type checking tactics, we can prove the theorem in nine steps. \begin{ttbox} -val prems = goal CTT.thy +val prems = Goal "[| A type; !!x. x:A ==> B(x) type; \ttback \ttback !!x y.[| x:A; y:B(x) |] ==> C(x,y) type \ttback \ttback |] ==> ?a : PROD h: (PROD x:A. SUM y:B(x). C(x,y)). \ttback