# HG changeset patch # User paulson # Date 900582601 -7200 # Node ID 1e944fe5ce96e4739014a39adbc739591af2e0e0 # Parent 6e2e9b92c301c3de71abd2c71f5bd48201c0a218 Got rid of obsolete "goal" commands. Also inserted spaces after all periods diff -r 6e2e9b92c301 -r 1e944fe5ce96 doc-src/Logics/CTT-eg.txt --- a/doc-src/Logics/CTT-eg.txt Thu Jul 16 10:35:31 1998 +0200 +++ b/doc-src/Logics/CTT-eg.txt Thu Jul 16 11:50:01 1998 +0200 @@ -6,7 +6,7 @@ (*** Type inference, from CTT/ex/typechk.ML ***) -goal CTT.thy "lam n. rec(n, 0, %x y.x) : ?A"; +Goal "lam n. rec(n, 0, %x y. x) : ?A"; by (resolve_tac [ProdI] 1); by (eresolve_tac [NE] 2); by (resolve_tac [NI0] 2); @@ -17,7 +17,7 @@ (*** Logical reasoning, from CTT/ex/elim.ML ***) -val prems = goal CTT.thy +val prems = Goal "[| A type; \ \ !!x. x:A ==> B(x) type; \ \ !!x. x:A ==> C(x) type; \ @@ -35,10 +35,10 @@ (*** Currying, from CTT/ex/elim.ML ***) -val prems = goal CTT.thy - "[| A type; !!x. x:A ==> B(x) type; \ -\ !!z. z: (SUM x:A. B(x)) ==> C(z) type \ -\ |] ==> ?a : PROD f: (PROD z : (SUM x:A . B(x)) . C(z)). \ +val prems = Goal + "[| A type; !!x. x:A ==> B(x) type; \ +\ !!z. z: (SUM x:A. B(x)) ==> C(z) type \ +\ |] ==> ?a : PROD f: (PROD z : (SUM x:A . B(x)) . C(z)). \ \ (PROD x:A . PROD y:B(x) . C())"; by (intr_tac prems); by (eresolve_tac [ProdE] 1); @@ -47,7 +47,7 @@ (*** Axiom of Choice ***) -val prems = goal CTT.thy +val prems = Goal "[| A type; !!x. x:A ==> B(x) type; \ \ !!x y.[| x:A; y:B(x) |] ==> C(x,y) type \ \ |] ==> ?a : PROD h: (PROD x:A. SUM y:B(x). C(x,y)). \ @@ -65,39 +65,11 @@ -> goal CTT.thy "lam n. rec(n, 0, %x y.x) : ?A"; -Level 0 -lam n. rec(n,0,%x y. x) : ?A - 1. lam n. rec(n,0,%x y. x) : ?A -> by (resolve_tac [ProdI] 1); -Level 1 -lam n. rec(n,0,%x y. x) : PROD x:?A1. ?B1(x) - 1. ?A1 type - 2. !!n. n : ?A1 ==> rec(n,0,%x y. x) : ?B1(n) -> by (eresolve_tac [NE] 2); -Level 2 -lam n. rec(n,0,%x y. x) : PROD x:N. ?C2(x,x) - 1. N type - 2. !!n. 0 : ?C2(n,0) - 3. !!n x y. [| x : N; y : ?C2(n,x) |] ==> x : ?C2(n,succ(x)) -> by (resolve_tac [NI0] 2); -Level 3 -lam n. rec(n,0,%x y. x) : N --> N - 1. N type - 2. !!n x y. [| x : N; y : N |] ==> x : N -> by (assume_tac 2); -Level 4 -lam n. rec(n,0,%x y. x) : N --> N - 1. N type -> by (resolve_tac [NF] 1); -Level 5 -lam n. rec(n,0,%x y. x) : N --> N -No subgoals! + +STOP_HERE; - - -> val prems = goal CTT.thy +> val prems = Goal # "[| A type; \ # \ !!x. x:A ==> B(x) type; \ # \ !!x. x:A ==> C(x) type; \ @@ -174,7 +146,7 @@ -> val prems = goal CTT.thy +> val prems = Goal # "[| A type; !!x. x:A ==> B(x) type; \ # \ !!z. z: (SUM x:A. B(x)) ==> C(z) type |] \ # \ ==> ?a : (PROD z : (SUM x:A . B(x)) . C(z)) \ @@ -204,7 +176,7 @@ -> val prems = goal CTT.thy +> val prems = Goal # "[| A type; !!x. x:A ==> B(x) type; \ # \ !!x y.[| x:A; y:B(x) |] ==> C(x,y) type \ # \ |] ==> ?a : (PROD x:A. SUM y:B(x). C(x,y)) \ 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 diff -r 6e2e9b92c301 -r 1e944fe5ce96 doc-src/Logics/FOL-eg.txt --- a/doc-src/Logics/FOL-eg.txt Thu Jul 16 10:35:31 1998 +0200 +++ b/doc-src/Logics/FOL-eg.txt Thu Jul 16 11:50:01 1998 +0200 @@ -5,8 +5,10 @@ (*** Intuitionistic examples ***) +context IFOL.thy; + (*Quantifier example from Logic&Computation*) -goal Int_Rule.thy "(EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))"; +Goal "(EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))"; by (resolve_tac [impI] 1); by (resolve_tac [allI] 1); by (resolve_tac [exI] 1); @@ -19,7 +21,7 @@ (*Example of Dyckhoff's method*) -goalw Int_Rule.thy [not_def] "~ ~ ((P-->Q) | (Q-->P))"; +Goalw [not_def] "~ ~ ((P-->Q) | (Q-->P))"; by (resolve_tac [impI] 1); by (eresolve_tac [disj_impE] 1); by (eresolve_tac [imp_impE] 1); @@ -29,87 +31,13 @@ -- goal Int_Rule.thy "(EX ay. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))"; -Level 0 -(EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y)) - 1. (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y)) -- by (resolve_tac [impI] 1); -Level 1 -(EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y)) - 1. EX y. ALL x. Q(x,y) ==> ALL x. EX y. Q(x,y) -- by (resolve_tac [allI] 1); -Level 2 -(EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y)) - 1. !!x. EX y. ALL x. Q(x,y) ==> EX y. Q(x,y) -- by (resolve_tac [exI] 1); -Level 3 -(EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y)) - 1. !!x. EX y. ALL x. Q(x,y) ==> Q(x,?y2(x)) -- by (eresolve_tac [exE] 1); -Level 4 -(EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y)) - 1. !!x y. ALL x. Q(x,y) ==> Q(x,?y2(x)) -- choplev 2; -Level 2 -(EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y)) - 1. !!x. EX y. ALL x. Q(x,y) ==> EX y. Q(x,y) -- by (eresolve_tac [exE] 1); -Level 3 -(EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y)) - 1. !!x y. ALL x. Q(x,y) ==> EX y. Q(x,y) -- by (resolve_tac [exI] 1); -Level 4 -(EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y)) - 1. !!x y. ALL x. Q(x,y) ==> Q(x,?y3(x,y)) -- by (eresolve_tac [allE] 1); -Level 5 -(EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y)) - 1. !!x y. Q(?x4(x,y),y) ==> Q(x,?y3(x,y)) -- by (assume_tac 1); -Level 6 -(EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y)) -No subgoals! - - - -> goalw Int_Rule.thy [not_def] "~ ~ ((P-->Q) | (Q-->P))"; -Level 0 -~ ~ ((P --> Q) | (Q --> P)) - 1. ((P --> Q) | (Q --> P) --> False) --> False -> by (resolve_tac [impI] 1); -Level 1 -~ ~ ((P --> Q) | (Q --> P)) - 1. (P --> Q) | (Q --> P) --> False ==> False -> by (eresolve_tac [disj_impE] 1); -Level 2 -~ ~ ((P --> Q) | (Q --> P)) - 1. [| (P --> Q) --> False; (Q --> P) --> False |] ==> False -> by (eresolve_tac [imp_impE] 1); -Level 3 -~ ~ ((P --> Q) | (Q --> P)) - 1. [| (Q --> P) --> False; P; Q --> False |] ==> Q - 2. [| (Q --> P) --> False; False |] ==> False -> by (eresolve_tac [imp_impE] 1); -Level 4 -~ ~ ((P --> Q) | (Q --> P)) - 1. [| P; Q --> False; Q; P --> False |] ==> P - 2. [| P; Q --> False; False |] ==> Q - 3. [| (Q --> P) --> False; False |] ==> False -> by (REPEAT (eresolve_tac [FalseE] 2)); -Level 5 -~ ~ ((P --> Q) | (Q --> P)) - 1. [| P; Q --> False; Q; P --> False |] ==> P -> by (assume_tac 1); -Level 6 -~ ~ ((P --> Q) | (Q --> P)) -No subgoals! - - (*** Classical examples ***) -goal cla_thy "EX y. ALL x. P(y)-->P(x)"; +context FOL.thy; + +Goal "EX y. ALL x. P(y)-->P(x)"; by (resolve_tac [exCI] 1); by (resolve_tac [allI] 1); by (resolve_tac [impI] 1); @@ -119,12 +47,12 @@ by (resolve_tac [impI] 1); by (eresolve_tac [notE] 1); by (assume_tac 1); -goal cla_thy "EX y. ALL x. P(y)-->P(x)"; -by (best_tac FOL_dup_cs 1); +Goal "EX y. ALL x. P(y)-->P(x)"; +by (Blast_tac 1); -- goal cla_thy "EX y. ALL x. P(y)-->P(x)"; +- Goal "EX y. ALL x. P(y)-->P(x)"; Level 0 EX y. ALL x. P(y) --> P(x) 1. EX y. ALL x. P(y) --> P(x) @@ -162,7 +90,7 @@ Level 8 EX y. ALL x. P(y) --> P(x) No subgoals! -- goal cla_thy "EX y. ALL x. P(y)-->P(x)"; +- Goal "EX y. ALL x. P(y)-->P(x)"; Level 0 EX y. ALL x. P(y) --> P(x) 1. EX y. ALL x. P(y) --> P(x) diff -r 6e2e9b92c301 -r 1e944fe5ce96 doc-src/Logics/FOL.tex --- a/doc-src/Logics/FOL.tex Thu Jul 16 10:35:31 1998 +0200 +++ b/doc-src/Logics/FOL.tex Thu Jul 16 11:50:01 1998 +0200 @@ -7,16 +7,16 @@ \thydx{IFOL}. Classical logic, theory \thydx{FOL}, is obtained by adding the double negation rule. Basic proof procedures are provided. The intuitionistic prover works with derived rules to simplify -implications in the assumptions. Classical~{\tt FOL} employs Isabelle's +implications in the assumptions. Classical~\texttt{FOL} employs Isabelle's classical reasoner, which simulates a sequent calculus. \section{Syntax and rules of inference} The logic is many-sorted, using Isabelle's type classes. The class of -first-order terms is called \cldx{term} and is a subclass of {\tt logic}. +first-order terms is called \cldx{term} and is a subclass of \texttt{logic}. No types of individuals are provided, but extensions can define types such -as {\tt nat::term} and type constructors such as {\tt list::(term)term} -(see the examples directory, {\tt FOL/ex}). Below, the type variable -$\alpha$ ranges over class {\tt term}; the equality symbol and quantifiers +as \texttt{nat::term} and type constructors such as \texttt{list::(term)term} +(see the examples directory, \texttt{FOL/ex}). Below, the type variable +$\alpha$ ranges over class \texttt{term}; the equality symbol and quantifiers are polymorphic (many-sorted). The type of formulae is~\tydx{o}, which belongs to class~\cldx{logic}. Figure~\ref{fol-syntax} gives the syntax. Note that $a$\verb|~=|$b$ is translated to $\neg(a=b)$. @@ -45,8 +45,8 @@ conj_impE}, etc., support the intuitionistic proof procedure (see~\S\ref{fol-int-prover}). -See the files {\tt FOL/IFOL.thy}, {\tt FOL/IFOL.ML} and -{\tt FOL/intprover.ML} for complete listings of the rules and +See the files \texttt{FOL/IFOL.thy}, \texttt{FOL/IFOL.ML} and +\texttt{FOL/intprover.ML} for complete listings of the rules and derived rules. \begin{figure} @@ -68,7 +68,7 @@ universal quantifier ($\forall$) \\ \sdx{EX} & \cdx{Ex} & $(\alpha\To o)\To o$ & 10 & existential quantifier ($\exists$) \\ - {\tt EX!} & \cdx{Ex1} & $(\alpha\To o)\To o$ & 10 & + \texttt{EX!} & \cdx{Ex1} & $(\alpha\To o)\To o$ & 10 & unique existence ($\exists!$) \end{tabular} \index{*"E"X"! symbol} @@ -108,7 +108,7 @@ \end{array} \] \subcaption{Grammar} -\caption{Syntax of {\tt FOL}} \label{fol-syntax} +\caption{Syntax of \texttt{FOL}} \label{fol-syntax} \end{figure} @@ -197,12 +197,12 @@ \begin{itemize} \item It instantiates the simplifier. Both equality ($=$) and the biconditional -($\bimp$) may be used for rewriting. Tactics such as {\tt Asm_simp_tac} and -{\tt Full_simp_tac} refer to the default simpset ({\tt simpset()}), which works for +($\bimp$) may be used for rewriting. Tactics such as \texttt{Asm_simp_tac} and +\texttt{Full_simp_tac} refer to the default simpset (\texttt{simpset()}), which works for most purposes. Named simplification sets include \ttindexbold{IFOL_ss}, for intuitionistic first-order logic, and \ttindexbold{FOL_ss}, for classical logic. See the file -{\tt FOL/simpdata.ML} for a complete listing of the simplification +\texttt{FOL/simpdata.ML} for a complete listing of the simplification rules% \iflabelundefined{sec:setting-up-simp}{}% {, and \S\ref{sec:setting-up-simp} for discussion}. @@ -225,7 +225,7 @@ \section{Intuitionistic proof procedures} \label{fol-int-prover} -Implication elimination (the rules~{\tt mp} and~{\tt impE}) pose +Implication elimination (the rules~\texttt{mp} and~\texttt{impE}) pose difficulties for automated proof. In intuitionistic logic, the assumption $P\imp Q$ cannot be treated like $\neg P\disj Q$. Given $P\imp Q$, we may use~$Q$ provided we can prove~$P$; the proof of~$P$ may require repeated @@ -239,7 +239,7 @@ \[ \infer[({\imp}E)]{Q}{P\imp Q & \infer[({\imp}E)]{P}{(P\imp Q)\imp P & P\imp Q}} \] -The theorem prover for intuitionistic logic does not use~{\tt impE}.\@ +The theorem prover for intuitionistic logic does not use~\texttt{impE}.\@ Instead, it simplifies implications using derived rules (Fig.\ts\ref{fol-int-derived}). It reduces the antecedents of implications to atoms and then uses Modus Ponens: from $P\imp Q$ and~$P$ deduce~$Q$. @@ -264,7 +264,7 @@ IntPr.fast_tac : int -> tactic IntPr.best_tac : int -> tactic \end{ttbox} -Most of these belong to the structure {\tt IntPr} and resemble the +Most of these belong to the structure \texttt{IntPr} and resemble the tactics of Isabelle's classical reasoner. \begin{ttdescription} @@ -277,30 +277,30 @@ produce multiple outcomes, enumerating all suitable pairs of assumptions. \item[\ttindexbold{eq_mp_tac} {\it i}] -is like {\tt mp_tac} {\it i}, but may not instantiate unknowns --- thus, it +is like \texttt{mp_tac} {\it i}, but may not instantiate unknowns --- thus, it is safe. \item[\ttindexbold{IntPr.safe_step_tac} $i$] performs a safe step on subgoal~$i$. This may include proof by assumption or Modus Ponens (taking -care not to instantiate unknowns), or {\tt hyp_subst_tac}. +care not to instantiate unknowns), or \texttt{hyp_subst_tac}. \item[\ttindexbold{IntPr.safe_tac}] repeatedly performs safe steps on all subgoals. It is deterministic, with at most one outcome. -\item[\ttindexbold{IntPr.inst_step_tac} $i$] is like {\tt safe_step_tac}, +\item[\ttindexbold{IntPr.inst_step_tac} $i$] is like \texttt{safe_step_tac}, but allows unknowns to be instantiated. -\item[\ttindexbold{IntPr.step_tac} $i$] tries {\tt safe_tac} or {\tt +\item[\ttindexbold{IntPr.step_tac} $i$] tries \texttt{safe_tac} or {\tt inst_step_tac}, or applies an unsafe rule. This is the basic step of the intuitionistic proof procedure. -\item[\ttindexbold{IntPr.fast_tac} $i$] applies {\tt step_tac}, using +\item[\ttindexbold{IntPr.fast_tac} $i$] applies \texttt{step_tac}, using depth-first search, to solve subgoal~$i$. -\item[\ttindexbold{IntPr.best_tac} $i$] applies {\tt step_tac}, using +\item[\ttindexbold{IntPr.best_tac} $i$] applies \texttt{step_tac}, using best-first search (guided by the size of the proof state) to solve subgoal~$i$. \end{ttdescription} -Here are some of the theorems that {\tt IntPr.fast_tac} proves +Here are some of the theorems that \texttt{IntPr.fast_tac} proves automatically. The latter three date from {\it Principia Mathematica} (*11.53, *11.55, *11.61)~\cite{principia}. \begin{ttbox} @@ -337,11 +337,11 @@ well as classical elimination rules for~$\imp$ and~$\bimp$, and the swap rule (see Fig.\ts\ref{fol-cla-derived}). -The classical reasoner is installed. Tactics such as {\tt Blast_tac} and {\tt -Best_tac} refer to the default claset ({\tt claset()}), which works for most +The classical reasoner is installed. Tactics such as \texttt{Blast_tac} and {\tt +Best_tac} refer to the default claset (\texttt{claset()}), which works for most purposes. Named clasets include \ttindexbold{prop_cs}, which includes the propositional rules, and \ttindexbold{FOL_cs}, which also includes quantifier -rules. See the file {\tt FOL/cladata.ML} for lists of the +rules. See the file \texttt{FOL/cladata.ML} for lists of the classical rules, and \iflabelundefined{chap:classical}{the {\em Reference Manual\/}}% {Chap.\ts\ref{chap:classical}} @@ -351,11 +351,15 @@ \section{An intuitionistic example} Here is a session similar to one in {\em Logic and Computation} \cite[pages~222--3]{paulson87}. Isabelle treats quantifiers differently -from {\sc lcf}-based theorem provers such as {\sc hol}. The proof begins -by entering the goal in intuitionistic logic, then applying the rule -$({\imp}I)$. +from {\sc lcf}-based theorem provers such as {\sc hol}. + +First, we specify that we are working in intuitionistic logic: \begin{ttbox} -goal IFOL.thy "(EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))"; +context IFOL.thy; +\end{ttbox} +The proof begins by entering the goal, then applying the rule $({\imp}I)$. +\begin{ttbox} +Goal "(EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))"; {\out Level 0} {\out (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))} {\out 1. (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))} @@ -375,7 +379,7 @@ {\out (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))} {\out 1. !!x. EX y. ALL x. Q(x,y) ==> EX y. Q(x,y)} \end{ttbox} -Applying $({\forall}I)$ replaces the \hbox{\tt ALL x} by \hbox{\tt!!x}, +Applying $({\forall}I)$ replaces the \texttt{ALL~x} by \hbox{\tt!!x}, changing the universal quantifier from object~($\forall$) to meta~($\Forall$). The bound variable is a {\bf parameter} of the subgoal. We now must choose between $({\exists}I)$ and $({\exists}E)$. What @@ -387,8 +391,8 @@ {\out 1. !!x. EX y. ALL x. Q(x,y) ==> Q(x,?y2(x))} \end{ttbox} The new subgoal~1 contains the function variable {\tt?y2}. Instantiating -{\tt?y2} can replace~{\tt?y2(x)} by a term containing~{\tt x}, even -though~{\tt x} is a bound variable. Now we analyse the assumption +{\tt?y2} can replace~{\tt?y2(x)} by a term containing~\texttt{x}, even +though~\texttt{x} is a bound variable. Now we analyse the assumption \(\exists y.\forall x. Q(x,y)\) using elimination rules: \begin{ttbox} by (eresolve_tac [exE] 1); @@ -396,10 +400,10 @@ {\out (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))} {\out 1. !!x y. ALL x. Q(x,y) ==> Q(x,?y2(x))} \end{ttbox} -Applying $(\exists E)$ has produced the parameter {\tt y} and stripped the +Applying $(\exists E)$ has produced the parameter \texttt{y} and stripped the existential quantifier from the assumption. But the subgoal is unprovable: -there is no way to unify {\tt ?y2(x)} with the bound variable~{\tt y}. -Using {\tt choplev} we can return to the critical point. This time we +there is no way to unify \texttt{?y2(x)} with the bound variable~\texttt{y}. +Using \texttt{choplev} we can return to the critical point. This time we apply $({\exists}E)$: \begin{ttbox} choplev 2; @@ -427,9 +431,9 @@ {\out (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))} {\out 1. !!x y. Q(?x4(x,y),y) ==> Q(x,?y3(x,y))} \end{ttbox} -The subgoal has variables {\tt ?y3} and {\tt ?x4} applied to both +The subgoal has variables \texttt{?y3} and \texttt{?x4} applied to both parameters. The obvious projection functions unify {\tt?x4(x,y)} with~{\tt -x} and \verb|?y3(x,y)| with~{\tt y}. +x} and \verb|?y3(x,y)| with~\texttt{y}. \begin{ttbox} by (assume_tac 1); {\out Level 6} @@ -440,7 +444,7 @@ ones. But proof checking is tedious; \ttindex{IntPr.fast_tac} proves the theorem in one step. \begin{ttbox} -goal IFOL.thy "(EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))"; +Goal "(EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))"; {\out Level 0} {\out (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))} {\out 1. (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))} @@ -469,7 +473,7 @@ negations to implications using the definition $\neg P\equiv P\imp\bot$. This allows use of the special implication rules. \begin{ttbox} -goalw IFOL.thy [not_def] "~ ~ ((P-->Q) | (Q-->P))"; +Goalw [not_def] "~ ~ ((P-->Q) | (Q-->P))"; {\out Level 0} {\out ~ ~ ((P --> Q) | (Q --> P))} {\out 1. ((P --> Q) | (Q --> P) --> False) --> False} @@ -525,20 +529,24 @@ {\out ~ ~ ((P --> Q) | (Q --> P))} {\out No subgoals!} \end{ttbox} -This proof is also trivial for {\tt IntPr.fast_tac}. +This proof is also trivial for \texttt{IntPr.fast_tac}. \section{A classical example} \label{fol-cla-example} To illustrate classical logic, we shall prove the theorem $\ex{y}\all{x}P(y)\imp P(x)$. Informally, the theorem can be proved as follows. Choose~$y$ such that~$\neg P(y)$, if such exists; otherwise -$\all{x}P(x)$ is true. Either way the theorem holds. +$\all{x}P(x)$ is true. Either way the theorem holds. First, we switch to +classical logic: +\begin{ttbox} +context FOL.thy; +\end{ttbox} The formal proof does not conform in any obvious way to the sketch given above. The key inference is the first one, \tdx{exCI}; this classical version of~$(\exists I)$ allows multiple instantiation of the quantifier. \begin{ttbox} -goal FOL.thy "EX y. ALL x. P(y)-->P(x)"; +Goal "EX y. ALL x. P(y)-->P(x)"; {\out Level 0} {\out EX y. ALL x. P(y) --> P(x)} {\out 1. EX y. ALL x. P(y) --> P(x)} @@ -582,7 +590,7 @@ {\out EX y. ALL x. P(y) --> P(x)} {\out 1. !!x xa. [| P(?a); ~ P(x) |] ==> P(?y3(x)) --> P(xa)} \end{ttbox} -The previous conclusion, {\tt P(x)}, has become a negated assumption. +The previous conclusion, \texttt{P(x)}, has become a negated assumption. \begin{ttbox} by (resolve_tac [impI] 1); {\out Level 6} @@ -603,15 +611,16 @@ {\out EX y. ALL x. P(y) --> P(x)} {\out No subgoals!} \end{ttbox} -The civilised way to prove this theorem is through \ttindex{deepen_tac}, +The civilised way to prove this theorem is through \ttindex{Blast_tac}, which automatically uses the classical version of~$(\exists I)$: \begin{ttbox} -goal FOL.thy "EX y. ALL x. P(y)-->P(x)"; +Goal "EX y. ALL x. P(y)-->P(x)"; {\out Level 0} {\out EX y. ALL x. P(y) --> P(x)} {\out 1. EX y. ALL x. P(y) --> P(x)} -by (Deepen_tac 0 1); +by (Blast_tac 1); {\out Depth = 0} +{\out Depth = 1} {\out Depth = 2} {\out Level 1} {\out EX y. ALL x. P(y) --> P(x)} @@ -644,7 +653,7 @@ & \infer*{S}{[\neg P,R]}} \] Having made these plans, we get down to work with Isabelle. The theory of -classical logic, {\tt FOL}, is extended with the constant +classical logic, \texttt{FOL}, is extended with the constant $if::[o,o,o]\To o$. The axiom \tdx{if_def} asserts the equation~$(if)$. \begin{ttbox} @@ -653,25 +662,33 @@ rules if_def "if(P,Q,R) == P&Q | ~P&R" end \end{ttbox} -The derivations of the introduction and elimination rules demonstrate the -methods for rewriting with definitions. Classical reasoning is required, -so we use {\tt blast_tac}. +We create the file \texttt{If.thy} containing these declarations. (This file +is on directory \texttt{FOL/ex} in the Isabelle distribution.) Typing +\begin{ttbox} +use_thy "If"; +\end{ttbox} +loads that theory and sets it to be the current context. \subsection{Deriving the introduction rule} + +The derivations of the introduction and elimination rules demonstrate the +methods for rewriting with definitions. Classical reasoning is required, +so we use \texttt{blast_tac}. + The introduction rule, given the premises $P\Imp Q$ and $\neg P\Imp R$, concludes $if(P,Q,R)$. We propose the conclusion as the main goal -using~\ttindex{goalw}, which uses {\tt if_def} to rewrite occurrences +using~\ttindex{goalw}, which uses \texttt{if_def} to rewrite occurrences of $if$ in the subgoal. \begin{ttbox} -val prems = goalw If.thy [if_def] +val prems = Goalw [if_def] "[| P ==> Q; ~ P ==> R |] ==> if(P,Q,R)"; {\out Level 0} {\out if(P,Q,R)} {\out 1. P & Q | ~ P & R} \end{ttbox} -The premises (bound to the {\ML} variable {\tt prems}) are passed as -introduction rules to \ttindex{blast_tac}. Remember that {\tt claset()} refers +The premises (bound to the {\ML} variable \texttt{prems}) are passed as +introduction rules to \ttindex{blast_tac}. Remember that \texttt{claset()} refers to the default classical set. \begin{ttbox} by (blast_tac (claset() addIs prems) 1); @@ -686,15 +703,15 @@ The elimination rule has three premises, two of which are themselves rules. The conclusion is simply $S$. \begin{ttbox} -val major::prems = goalw If.thy [if_def] +val major::prems = Goalw [if_def] "[| if(P,Q,R); [| P; Q |] ==> S; [| ~ P; R |] ==> S |] ==> S"; {\out Level 0} {\out S} {\out 1. S} \end{ttbox} The major premise contains an occurrence of~$if$, but the version returned -by \ttindex{goalw} (and bound to the {\ML} variable~{\tt major}) has the -definition expanded. Now \ttindex{cut_facts_tac} inserts~{\tt major} as an +by \ttindex{goalw} (and bound to the {\ML} variable~\texttt{major}) has the +definition expanded. Now \ttindex{cut_facts_tac} inserts~\texttt{major} as an assumption in the subgoal, so that \ttindex{blast_tac} can break it down. \begin{ttbox} by (cut_facts_tac [major] 1); @@ -712,8 +729,8 @@ \iflabelundefined{definitions}{{\em Introduction to Isabelle}}% {\S\ref{definitions}}, there are other ways of treating definitions when deriving a rule. We can start the -proof using {\tt goal}, which does not expand definitions, instead of -{\tt goalw}. We can use \ttindex{rew_tac} +proof using \texttt{goal}, which does not expand definitions, instead of +\texttt{goalw}. We can use \ttindex{rew_tac} to expand definitions in the subgoals --- perhaps after calling \ttindex{cut_facts_tac} to insert the rule's premises. We can use \ttindex{rewrite_rule}, which is a meta-inference rule, to expand @@ -729,12 +746,11 @@ if(if(P,Q,R), A, B) & \bimp & if(P,if(Q,A,B),if(R,A,B)) \end{eqnarray*} Proofs also require the classical reasoning rules and the $\bimp$ -introduction rule (called~\tdx{iffI}: do not confuse with~{\tt ifI}). +introduction rule (called~\tdx{iffI}: do not confuse with~\texttt{ifI}). To display the $if$-rules in action, let us analyse a proof step by step. \begin{ttbox} -goal If.thy - "if(P, if(Q,A,B), if(Q,C,D)) <-> if(Q, if(P,A,C), if(P,B,D))"; +Goal "if(P, if(Q,A,B), if(Q,C,D)) <-> if(Q, if(P,A,C), if(P,B,D))"; {\out Level 0} {\out if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))} {\out 1. if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))} @@ -808,7 +824,7 @@ \end{ttbox} This tactic also solves the other example. \begin{ttbox} -goal If.thy "if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,A,B))"; +Goal "if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,A,B))"; {\out Level 0} {\out if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))} {\out 1. if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))} @@ -839,8 +855,8 @@ {\out P & (Q & A | ~ Q & B) | ~ P & (R & A | ~ R & B)} \end{ttbox} We are left with a subgoal in pure first-order logic, which is why the -classical reasoner can prove it given {\tt FOL_cs} alone. (We could, of -course, have used {\tt Blast_tac}.) +classical reasoner can prove it given \texttt{FOL_cs} alone. (We could, of +course, have used \texttt{Blast_tac}.) \begin{ttbox} by (blast_tac FOL_cs 1); {\out Level 2} @@ -851,7 +867,7 @@ approach has its merits --- especially if the prover for the base logic is good --- but can be slow. In these examples, proofs using the default claset (which includes the derived rules) run about six times faster -than proofs using {\tt FOL_cs}. +than proofs using \texttt{FOL_cs}. Expanding definitions also complicates error diagnosis. Suppose we are having difficulties in proving some goal. If by expanding definitions we have @@ -860,7 +876,7 @@ Attempts at program verification often yield invalid assertions. Let us try to prove one: \begin{ttbox} -goal If.thy "if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,B,A))"; +Goal "if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,B,A))"; {\out Level 0} {\out if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))} {\out 1. if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))} diff -r 6e2e9b92c301 -r 1e944fe5ce96 doc-src/Logics/HOL.tex --- a/doc-src/Logics/HOL.tex Thu Jul 16 10:35:31 1998 +0200 +++ b/doc-src/Logics/HOL.tex Thu Jul 16 11:50:01 1998 +0200 @@ -198,26 +198,26 @@ \subsection{Binders} -Hilbert's {\bf description} operator~$\varepsilon x.P[x]$ stands for +Hilbert's {\bf description} operator~$\varepsilon x. P[x]$ stands for some~$x$ satisfying~$P$, if such exists. Since all terms in \HOL\ denote something, a description is always meaningful, but we do not know its value unless $P$ defines it uniquely. We may write -descriptions as \cdx{Eps}($\lambda x.P[x]$) or use the syntax -\hbox{\tt \at $x$.$P[x]$}. +descriptions as \cdx{Eps}($\lambda x. P[x]$) or use the syntax +\hbox{\tt \at $x$. $P[x]$}. Existential quantification is defined by -\[ \exists x.P~x \;\equiv\; P(\varepsilon x.P~x). \] -The unique existence quantifier, $\exists!x.P$, is defined in terms +\[ \exists x. P~x \;\equiv\; P(\varepsilon x. P~x). \] +The unique existence quantifier, $\exists!x. P$, is defined in terms of~$\exists$ and~$\forall$. An Isabelle binder, it admits nested -quantifications. For instance, $\exists!x\,y.P\,x\,y$ abbreviates -$\exists!x. \exists!y.P\,x\,y$; note that this does not mean that there +quantifications. For instance, $\exists!x\,y. P\,x\,y$ abbreviates +$\exists!x. \exists!y. P\,x\,y$; note that this does not mean that there exists a unique pair $(x,y)$ satisfying~$P\,x\,y$. \index{*"! symbol}\index{*"? symbol}\index{HOL system@{\sc hol} system} Quantifiers have two notations. As in Gordon's {\sc hol} system, \HOL\ uses~{\tt!}\ and~{\tt?}\ to stand for $\forall$ and $\exists$. The existential quantifier must be followed by a space; thus {\tt?x} is an -unknown, while \verb'? x.f x=y' is a quantification. Isabelle's usual +unknown, while \verb'? x. f x=y' is a quantification. Isabelle's usual notation for quantifiers, \sdx{ALL} and \sdx{EX}, is also available. Both notations are accepted for input. The {\ML} reference \ttindexbold{HOL_quantifiers} governs the output notation. If set to {\tt @@ -225,7 +225,7 @@ to \texttt{false}, then~{\tt ALL} and~{\tt EX} are displayed. If $\tau$ is a type of class \cldx{ord}, $P$ a formula and $x$ a -variable of type $\tau$, then the term \cdx{LEAST}~$x.P[x]$ is defined +variable of type $\tau$, then the term \cdx{LEAST}~$x. P[x]$ is defined to be the least (w.r.t.\ $\le$) $x$ such that $P~x$ holds (see Fig.~\ref{hol-defs}). The definition uses Hilbert's $\varepsilon$ choice operator, so \texttt{Least} is always meaningful, but may yield @@ -238,7 +238,7 @@ \begin{warn} The low priority of binders means that they need to be enclosed in parenthesis when they occur in the context of other operations. For example, -instead of $P \land \forall x.Q$ you need to write $P \land (\forall x.Q)$. +instead of $P \land \forall x. Q$ you need to write $P \land (\forall x. Q)$. \end{warn} @@ -271,11 +271,11 @@ \begin{ttbox}\makeatother \tdx{refl} t = (t::'a) \tdx{subst} [| s = t; P s |] ==> P (t::'a) -\tdx{ext} (!!x::'a. (f x :: 'b) = g x) ==> (\%x.f x) = (\%x.g x) +\tdx{ext} (!!x::'a. (f x :: 'b) = g x) ==> (\%x. f x) = (\%x. g x) \tdx{impI} (P ==> Q) ==> P-->Q \tdx{mp} [| P-->Q; P |] ==> Q \tdx{iff} (P-->Q) --> (Q-->P) --> (P=Q) -\tdx{selectI} P(x::'a) ==> P(@x.P x) +\tdx{selectI} P(x::'a) ==> P(@x. P x) \tdx{True_or_False} (P=True) | (P=False) \end{ttbox} \caption{The \texttt{HOL} rules} \label{hol-rules} @@ -299,10 +299,10 @@ \begin{figure}\hfuzz=4pt%suppress "Overfull \hbox" message \begin{ttbox}\makeatother -\tdx{True_def} True == ((\%x::bool.x)=(\%x.x)) -\tdx{All_def} All == (\%P. P = (\%x.True)) -\tdx{Ex_def} Ex == (\%P. P(@x.P x)) -\tdx{False_def} False == (!P.P) +\tdx{True_def} True == ((\%x::bool. x)=(\%x. x)) +\tdx{All_def} All == (\%P. P = (\%x. True)) +\tdx{Ex_def} Ex == (\%P. P(@x. P x)) +\tdx{False_def} False == (!P. P) \tdx{not_def} not == (\%P. P-->False) \tdx{and_def} op & == (\%P Q. !R. (P-->Q-->R) --> R) \tdx{or_def} op | == (\%P Q. !R. (P-->R) --> (Q-->R) --> R) @@ -384,18 +384,18 @@ \begin{figure} \begin{ttbox}\makeatother \tdx{allI} (!!x. P x) ==> !x. P x -\tdx{spec} !x.P x ==> P x -\tdx{allE} [| !x.P x; P x ==> R |] ==> R -\tdx{all_dupE} [| !x.P x; [| P x; !x.P x |] ==> R |] ==> R +\tdx{spec} !x. P x ==> P x +\tdx{allE} [| !x. P x; P x ==> R |] ==> R +\tdx{all_dupE} [| !x. P x; [| P x; !x. P x |] ==> R |] ==> R \tdx{exI} P x ==> ? x. P x \tdx{exE} [| ? x. P x; !!x. P x ==> Q |] ==> Q \tdx{ex1I} [| P a; !!x. P x ==> x=a |] ==> ?! x. P x -\tdx{ex1E} [| ?! x.P x; !!x. [| P x; ! y. P y --> y=x |] ==> R +\tdx{ex1E} [| ?! x. P x; !!x. [| P x; ! y. P y --> y=x |] ==> R |] ==> R -\tdx{select_equality} [| P a; !!x. P x ==> x=a |] ==> (@x.P x) = a +\tdx{select_equality} [| P a; !!x. P x ==> x=a |] ==> (@x. P x) = a \subcaption{Quantifiers and descriptions} \tdx{ccontr} (~P ==> False) ==> P @@ -403,7 +403,7 @@ \tdx{excluded_middle} ~P | P \tdx{disjCI} (~Q ==> P) ==> P|Q -\tdx{exCI} (! x. ~ P x ==> P a) ==> ? x.P x +\tdx{exCI} (! x. ~ P x ==> P a) ==> ? x. P x \tdx{impCE} [| P-->Q; ~ P ==> R; Q ==> R |] ==> R \tdx{iffCE} [| P=Q; [| P;Q |] ==> R; [| ~P; ~Q |] ==> R |] ==> R \tdx{notnotD} ~~P ==> P @@ -511,17 +511,17 @@ \it external & \it internal & \it description \\ $a$ \ttilde: $b$ & \ttilde($a$ : $b$) & \rm non-membership\\ {\ttlbrace}$a@1$, $\ldots${\ttrbrace} & insert $a@1$ $\ldots$ {\ttlbrace}{\ttrbrace} & \rm finite set \\ - {\ttlbrace}$x$.$P[x]${\ttrbrace} & Collect($\lambda x.P[x]$) & + {\ttlbrace}$x$. $P[x]${\ttrbrace} & Collect($\lambda x. P[x]$) & \rm comprehension \\ - \sdx{INT} $x$:$A$.$B[x]$ & INTER $A$ $\lambda x.B[x]$ & + \sdx{INT} $x$:$A$. $B[x]$ & INTER $A$ $\lambda x. B[x]$ & \rm intersection \\ - \sdx{UN}{\tt\ } $x$:$A$.$B[x]$ & UNION $A$ $\lambda x.B[x]$ & + \sdx{UN}{\tt\ } $x$:$A$. $B[x]$ & UNION $A$ $\lambda x. B[x]$ & \rm union \\ - \tt ! $x$:$A$.$P[x]$ or \sdx{ALL} $x$:$A$.$P[x]$ & - Ball $A$ $\lambda x.P[x]$ & + \tt ! $x$:$A$. $P[x]$ or \sdx{ALL} $x$:$A$. $P[x]$ & + Ball $A$ $\lambda x. P[x]$ & \rm bounded $\forall$ \\ - \sdx{?} $x$:$A$.$P[x]$ or \sdx{EX}{\tt\ } $x$:$A$.$P[x]$ & - Bex $A$ $\lambda x.P[x]$ & \rm bounded $\exists$ + \sdx{?} $x$:$A$. $P[x]$ or \sdx{EX}{\tt\ } $x$:$A$. $P[x]$ & + Bex $A$ $\lambda x. P[x]$ & \rm bounded $\exists$ \end{tabular} \end{center} \subcaption{Translations} @@ -596,35 +596,35 @@ \texttt{insert} \, a \, ({\tt insert} \, b \, ({\tt insert} \, c \, \{\})) \end{eqnarray*} -The set \hbox{\tt{\ttlbrace}$x$.$P[x]${\ttrbrace}} consists of all $x$ (of suitable type) +The set \hbox{\tt{\ttlbrace}$x$. $P[x]${\ttrbrace}} consists of all $x$ (of suitable type) that satisfy~$P[x]$, where $P[x]$ is a formula that may contain free occurrences of~$x$. This syntax expands to \cdx{Collect}$(\lambda -x.P[x])$. It defines sets by absolute comprehension, which is impossible +x. P[x])$. It defines sets by absolute comprehension, which is impossible in~{\ZF}; the type of~$x$ implicitly restricts the comprehension. The set theory defines two {\bf bounded quantifiers}: \begin{eqnarray*} - \forall x\in A.P[x] &\hbox{abbreviates}& \forall x. x\in A\imp P[x] \\ - \exists x\in A.P[x] &\hbox{abbreviates}& \exists x. x\in A\conj P[x] + \forall x\in A. P[x] &\hbox{abbreviates}& \forall x. x\in A\imp P[x] \\ + \exists x\in A. P[x] &\hbox{abbreviates}& \exists x. x\in A\conj P[x] \end{eqnarray*} The constants~\cdx{Ball} and~\cdx{Bex} are defined accordingly. Instead of \texttt{Ball $A$ $P$} and \texttt{Bex $A$ $P$} we may write\index{*"! symbol}\index{*"? symbol} \index{*ALL symbol}\index{*EX symbol} % -\hbox{\tt !~$x$:$A$.$P[x]$} and \hbox{\tt ?~$x$:$A$.$P[x]$}. Isabelle's +\hbox{\tt !~$x$:$A$. $P[x]$} and \hbox{\tt ?~$x$:$A$. $P[x]$}. Isabelle's usual quantifier symbols, \sdx{ALL} and \sdx{EX}, are also accepted for input. As with the primitive quantifiers, the {\ML} reference \ttindex{HOL_quantifiers} specifies which notation to use for output. Unions and intersections over sets, namely $\bigcup@{x\in A}B[x]$ and $\bigcap@{x\in A}B[x]$, are written -\sdx{UN}~\hbox{\tt$x$:$A$.$B[x]$} and -\sdx{INT}~\hbox{\tt$x$:$A$.$B[x]$}. +\sdx{UN}~\hbox{\tt$x$:$A$. $B[x]$} and +\sdx{INT}~\hbox{\tt$x$:$A$. $B[x]$}. Unions and intersections over types, namely $\bigcup@x B[x]$ and $\bigcap@x -B[x]$, are written \sdx{UN}~\hbox{\tt$x$.$B[x]$} and -\sdx{INT}~\hbox{\tt$x$.$B[x]$}. They are equivalent to the previous +B[x]$, are written \sdx{UN}~\hbox{\tt$x$. $B[x]$} and +\sdx{INT}~\hbox{\tt$x$. $B[x]$}. They are equivalent to the previous union and intersection operators when $A$ is the universal set. The operators $\bigcup A$ and $\bigcap A$ act upon sets of sets. They are @@ -635,22 +635,22 @@ \begin{figure} \underscoreon \begin{ttbox} -\tdx{mem_Collect_eq} (a : {\ttlbrace}x.P x{\ttrbrace}) = P a -\tdx{Collect_mem_eq} {\ttlbrace}x.x:A{\ttrbrace} = A +\tdx{mem_Collect_eq} (a : {\ttlbrace}x. P x{\ttrbrace}) = P a +\tdx{Collect_mem_eq} {\ttlbrace}x. x:A{\ttrbrace} = A -\tdx{empty_def} {\ttlbrace}{\ttrbrace} == {\ttlbrace}x.False{\ttrbrace} -\tdx{insert_def} insert a B == {\ttlbrace}x.x=a{\ttrbrace} Un B +\tdx{empty_def} {\ttlbrace}{\ttrbrace} == {\ttlbrace}x. False{\ttrbrace} +\tdx{insert_def} insert a B == {\ttlbrace}x. x=a{\ttrbrace} Un B \tdx{Ball_def} Ball A P == ! x. x:A --> P x \tdx{Bex_def} Bex A P == ? x. x:A & P x \tdx{subset_def} A <= B == ! x:A. x:B -\tdx{Un_def} A Un B == {\ttlbrace}x.x:A | x:B{\ttrbrace} -\tdx{Int_def} A Int B == {\ttlbrace}x.x:A & x:B{\ttrbrace} -\tdx{set_diff_def} A - B == {\ttlbrace}x.x:A & x~:B{\ttrbrace} +\tdx{Un_def} A Un B == {\ttlbrace}x. x:A | x:B{\ttrbrace} +\tdx{Int_def} A Int B == {\ttlbrace}x. x:A & x:B{\ttrbrace} +\tdx{set_diff_def} A - B == {\ttlbrace}x. x:A & x~:B{\ttrbrace} \tdx{Compl_def} Compl A == {\ttlbrace}x. ~ x:A{\ttrbrace} \tdx{INTER_def} INTER A B == {\ttlbrace}y. ! x:A. y: B x{\ttrbrace} \tdx{UNION_def} UNION A B == {\ttlbrace}y. ? x:A. y: B x{\ttrbrace} -\tdx{INTER1_def} INTER1 B == INTER {\ttlbrace}x.True{\ttrbrace} B -\tdx{UNION1_def} UNION1 B == UNION {\ttlbrace}x.True{\ttrbrace} B +\tdx{INTER1_def} INTER1 B == INTER {\ttlbrace}x. True{\ttrbrace} B +\tdx{UNION1_def} UNION1 B == UNION {\ttlbrace}x. True{\ttrbrace} B \tdx{Inter_def} Inter S == (INT x:S. x) \tdx{Union_def} Union S == (UN x:S. x) \tdx{Pow_def} Pow A == {\ttlbrace}B. B <= A{\ttrbrace} @@ -663,20 +663,20 @@ \begin{figure} \underscoreon \begin{ttbox} -\tdx{CollectI} [| P a |] ==> a : {\ttlbrace}x.P x{\ttrbrace} -\tdx{CollectD} [| a : {\ttlbrace}x.P x{\ttrbrace} |] ==> P a -\tdx{CollectE} [| a : {\ttlbrace}x.P x{\ttrbrace}; P a ==> W |] ==> W +\tdx{CollectI} [| P a |] ==> a : {\ttlbrace}x. P x{\ttrbrace} +\tdx{CollectD} [| a : {\ttlbrace}x. P x{\ttrbrace} |] ==> P a +\tdx{CollectE} [| a : {\ttlbrace}x. P x{\ttrbrace}; P a ==> W |] ==> W \tdx{ballI} [| !!x. x:A ==> P x |] ==> ! x:A. P x \tdx{bspec} [| ! x:A. P x; x:A |] ==> P x \tdx{ballE} [| ! x:A. P x; P x ==> Q; ~ x:A ==> Q |] ==> Q \tdx{bexI} [| P x; x:A |] ==> ? x:A. P x -\tdx{bexCI} [| ! x:A. ~ P x ==> P a; a:A |] ==> ? x:A.P x +\tdx{bexCI} [| ! x:A. ~ P x ==> P a; a:A |] ==> ? x:A. P x \tdx{bexE} [| ? x:A. P x; !!x. [| x:A; P x |] ==> Q |] ==> Q \subcaption{Comprehension and Bounded quantifiers} -\tdx{subsetI} (!!x.x:A ==> x:B) ==> A <= B +\tdx{subsetI} (!!x. x:A ==> x:B) ==> A <= B \tdx{subsetD} [| A <= B; c:A |] ==> c:B \tdx{subsetCE} [| A <= B; ~ (c:A) ==> P; c:B ==> P |] ==> P @@ -822,8 +822,8 @@ \tdx{Un_assoc} (A Un B) Un C = A Un (B Un C) \tdx{Un_Int_distrib} (A Int B) Un C = (A Un C) Int (B Un C) -\tdx{Compl_disjoint} A Int (Compl A) = {\ttlbrace}x.False{\ttrbrace} -\tdx{Compl_partition} A Un (Compl A) = {\ttlbrace}x.True{\ttrbrace} +\tdx{Compl_disjoint} A Int (Compl A) = {\ttlbrace}x. False{\ttrbrace} +\tdx{Compl_partition} A Un (Compl A) = {\ttlbrace}x. True{\ttrbrace} \tdx{double_complement} Compl(Compl A) = A \tdx{Compl_Un} Compl(A Un B) = (Compl A) Int (Compl B) \tdx{Compl_Int} Compl(A Int B) = (Compl A) Un (Compl B) @@ -1078,12 +1078,12 @@ In addition, it is possible to use tuples as patterns in abstractions: \begin{center} -{\tt\%($x$,$y$).$t$} \quad stands for\quad \texttt{split(\%$x$\thinspace$y$.$t$)} +{\tt\%($x$,$y$). $t$} \quad stands for\quad \texttt{split(\%$x$\thinspace$y$. $t$)} \end{center} Nested patterns are also supported. They are translated stepwise: -{\tt\%($x$,$y$,$z$).$t$} $\leadsto$ {\tt\%($x$,($y$,$z$)).$t$} $\leadsto$ -{\tt split(\%$x$.\%($y$,$z$).$t$)} $\leadsto$ \texttt{split(\%$x$.split(\%$y$ - $z$.$t$))}. The reverse translation is performed upon printing. +{\tt\%($x$,$y$,$z$). $t$} $\leadsto$ {\tt\%($x$,($y$,$z$)). $t$} $\leadsto$ +{\tt split(\%$x$.\%($y$,$z$). $t$)} $\leadsto$ \texttt{split(\%$x$. split(\%$y$ + $z$. $t$))}. The reverse translation is performed upon printing. \begin{warn} The translation between patterns and \texttt{split} is performed automatically by the parser and printer. Thus the internal and external form of a term @@ -1762,9 +1762,9 @@ We want to define the type $\alpha~mylist$.\footnote{This is just an example, there is already a list type in \HOL, of course.} To do this we have to build a new theory that contains the type definition. -We start from the basic \texttt{HOL} theory. +We start from the theory of arithmetic. \begin{ttbox} -MyList = HOL + +MyList = Arith + datatype 'a mylist = Nil | Cons 'a ('a mylist) end \end{ttbox} @@ -1773,7 +1773,7 @@ goal with $x$ quantified at the object-level. This will be stripped later using \ttindex{qed_spec_mp}. \begin{ttbox} -goal MyList.thy "!x. Cons x xs ~= xs"; +Goal "!x. Cons x xs ~= xs"; {\out Level 0} {\out ! x. Cons x xs ~= xs} {\out 1. ! x. Cons x xs ~= xs} @@ -1823,7 +1823,7 @@ notation \verb|#| for \texttt{Cons}. To do this we simply add mixfix annotations after the constructor declarations as follows: \begin{ttbox} -MyList = HOL + +MyList = Arith + datatype 'a mylist = Nil ("[]") | Cons 'a ('a mylist) (infixr "#" 70) @@ -1837,7 +1837,7 @@ This example shows a datatype that consists of 7 constructors: \begin{ttbox} -Days = Arith + +Days = Main + datatype days = Mon | Tue | Wed | Thu | Fri | Sat | Sun end \end{ttbox} @@ -1847,7 +1847,7 @@ contained among the distinctness theorems, but the simplifier can prove it thanks to rewrite rules inherited from theory \texttt{Arith}: \begin{ttbox} -goal Days.thy "Mon ~= Tue"; +Goal "Mon ~= Tue"; by (Simp_tac 1); \end{ttbox} You need not derive such inequalities explicitly: the simplifier will dispose @@ -1939,7 +1939,7 @@ \item \textit{function} is the name of the function, either as an \textit{id} or a \textit{string}. \item \textit{type} is the name of the datatype, either as an \textit{id} or - in the long form \texttt{$T$.$t$} ($T$ is the name of the theory + in the long form \texttt{$T$. $t$} ($T$ is the name of the theory where the datatype has been declared, $t$ the name of the datatype). The long form is required if the \texttt{datatype} and the {\tt primrec} sections are in different theories. @@ -1970,7 +1970,7 @@ The reduction rules for {\tt\at} become part of the default simpset, which leads to short proofs: \begin{ttbox}\underscoreon -goal Append.thy "(xs @ ys) @ zs = xs @ (ys @ zs)"; +Goal "(xs @ ys) @ zs = xs @ (ys @ zs)"; by (induct\_tac "xs" 1); by (ALLGOALS Asm\_simp\_tac); \end{ttbox} @@ -2051,10 +2051,10 @@ \end{itemize} We can use \texttt{measure} to declare Euclid's algorithm for the greatest -common divisor. The measure function, $\lambda(m,n).n$, specifies that the +common divisor. The measure function, $\lambda(m,n). n$, specifies that the recursion terminates because argument~$n$ decreases. \begin{ttbox} -recdef gcd "measure ((\%(m,n).n) ::nat*nat=>nat)" +recdef gcd "measure ((\%(m,n). n) ::nat*nat=>nat)" "gcd (m, n) = (if n=0 then m else gcd(n, m mod n))" \end{ttbox} @@ -2126,7 +2126,7 @@ Isabelle can prove the \texttt{gcd} function's termination condition automatically if supplied with the right simpset. \begin{ttbox} -recdef gcd "measure ((\%(m,n).n) ::nat*nat=>nat)" +recdef gcd "measure ((\%(m,n). n) ::nat*nat=>nat)" simpset "simpset() addsimps [mod_less_divisor, zero_less_eq]" "gcd (m, n) = (if n=0 then m else gcd(n, m mod n))" \end{ttbox} @@ -2447,10 +2447,14 @@ its powerset, some subset is outside its range. The Isabelle proof uses \HOL's set theory, with the type $\alpha\,set$ and -the operator \cdx{range}. The set~$S$ is given as an unknown instead of a +the operator \cdx{range}. +\begin{ttbox} +context Set.thy; +\end{ttbox} +The set~$S$ is given as an unknown instead of a quantified variable so that we may inspect the subset found by the proof. \begin{ttbox} -goal Set.thy "?S ~: range\thinspace(f :: 'a=>'a set)"; +Goal "?S ~: range\thinspace(f :: 'a=>'a set)"; {\out Level 0} {\out ?S ~: range f} {\out 1. ?S ~: range f} diff -r 6e2e9b92c301 -r 1e944fe5ce96 doc-src/Logics/LK-eg.txt --- a/doc-src/Logics/LK-eg.txt Thu Jul 16 10:35:31 1998 +0200 +++ b/doc-src/Logics/LK-eg.txt Thu Jul 16 11:50:01 1998 +0200 @@ -3,7 +3,9 @@ Pretty.setmargin 72; (*existing macros just allow this margin*) print_depth 0; -goal LK_Rule.thy "|- EX y. ALL x. P(y)-->P(x)"; +Context LK.thy; + +Goal "|- EX y. ALL x. P(y)-->P(x)"; by (resolve_tac [exR] 1); by (resolve_tac [allR] 1); by (resolve_tac [impR] 1); @@ -13,12 +15,12 @@ by (resolve_tac [allR] 1); by (resolve_tac [impR] 1); by (resolve_tac [basic] 1); -goal LK_Rule.thy "|- EX y. ALL x. P(y)-->P(x)"; +Goal "|- EX y. ALL x. P(y)-->P(x)"; by (best_tac LK_dup_pack 1); -goal LK_Rule.thy "|- ~ (EX x. ALL y. F(y,x) <-> ~F(y,y))"; +Goal "|- ~ (EX x. ALL y. F(y,x) <-> ~F(y,y))"; by (resolve_tac [notR] 1); by (resolve_tac [exL] 1); by (resolve_tac [allL_thin] 1); @@ -29,8 +31,10 @@ by (resolve_tac [basic] 1); +STOP_HERE; -> goal LK_Rule.thy "|- EX y. ALL x. P(y)-->P(x)"; + +> Goal "|- EX y. ALL x. P(y)-->P(x)"; Level 0 |- EX y. ALL x. P(y) --> P(x) 1. |- EX y. ALL x. P(y) --> P(x) @@ -65,7 +69,7 @@ |- EX y. ALL x. P(y) --> P(x) No subgoals! -> goal LK_Rule.thy "|- EX y. ALL x. P(y)-->P(x)"; +> Goal "|- EX y. ALL x. P(y)-->P(x)"; Level 0 |- EX y. ALL x. P(y) --> P(x) 1. |- EX y. ALL x. P(y) --> P(x) @@ -77,7 +81,7 @@ -> goal LK_Rule.thy "|- ~ (EX x. ALL y. F(y,x) <-> ~F(y,y))"; +> Goal "|- ~ (EX x. ALL y. F(y,x) <-> ~F(y,y))"; Level 0 |- ~(EX x. ALL y. F(y,x) <-> ~F(y,y)) 1. |- ~(EX x. ALL y. F(y,x) <-> ~F(y,y)) diff -r 6e2e9b92c301 -r 1e944fe5ce96 doc-src/Logics/LK.tex --- a/doc-src/Logics/LK.tex Thu Jul 16 10:35:31 1998 +0200 +++ b/doc-src/Logics/LK.tex Thu Jul 16 11:50:01 1998 +0200 @@ -23,6 +23,15 @@ logic theorem prover that is as powerful as the generic classical reasoner, except that it does not perform equality reasoning. +To work in LK, start up Isabelle specifying \texttt{Sequents} as the +object-logic. Once in Isabelle, change the context to theory \texttt{LK.thy}: +\begin{ttbox} +isabelle Sequents +context LK.thy; +\end{ttbox} +Model logic and linear logic are also available, but unfortunately they are +not documented. + \begin{figure} \begin{center} @@ -111,15 +120,15 @@ Higher-order unification includes associative unification as a special case, by an encoding that involves function composition \cite[page~37]{huet78}. To represent lists, let $C$ be a new constant. -The empty list is $\lambda x.x$, while $[t@1,t@2,\ldots,t@n]$ is +The empty list is $\lambda x. x$, while $[t@1,t@2,\ldots,t@n]$ is represented by -\[ \lambda x.C(t@1,C(t@2,\ldots,C(t@n,x))). \] +\[ \lambda x. C(t@1,C(t@2,\ldots,C(t@n,x))). \] The unifiers of this with $\lambda x.\Var{f}(\Var{g}(x))$ give all the ways of expressing $[t@1,t@2,\ldots,t@n]$ as the concatenation of two lists. Unlike orthodox associative unification, this technique can represent certain infinite sets of unifiers by flex-flex equations. But note that the term -$\lambda x.C(t,\Var{a})$ does not represent any list. Flex-flex constraints +$\lambda x. C(t,\Var{a})$ does not represent any list. Flex-flex constraints containing such garbage terms may accumulate during a proof. \index{flex-flex constraints} @@ -172,14 +181,14 @@ \tdx{FalseL} $H, False, $G |- $E -\tdx{allR} (!!x.$H|- $E, P(x), $F) ==> $H|- $E, ALL x.P(x), $F -\tdx{allL} $H, P(x), $G, ALL x.P(x) |- $E ==> $H, ALL x.P(x), $G|- $E +\tdx{allR} (!!x. $H|- $E, P(x), $F) ==> $H|- $E, ALL x. P(x), $F +\tdx{allL} $H, P(x), $G, ALL x. P(x) |- $E ==> $H, ALL x. P(x), $G|- $E -\tdx{exR} $H|- $E, P(x), $F, EX x.P(x) ==> $H|- $E, EX x.P(x), $F -\tdx{exL} (!!x.$H, P(x), $G|- $E) ==> $H, EX x.P(x), $G|- $E +\tdx{exR} $H|- $E, P(x), $F, EX x. P(x) ==> $H|- $E, EX x. P(x), $F +\tdx{exL} (!!x. $H, P(x), $G|- $E) ==> $H, EX x. P(x), $G|- $E -\tdx{The} [| $H |- $E, P(a), $F; !!x.$H, P(x) |- $E, x=a, $F |] ==> - $H |- $E, P(THE x.P(x)), $F +\tdx{The} [| $H |- $E, P(a), $F; !!x. $H, P(x) |- $E, x=a, $F |] ==> + $H |- $E, P(THE x. P(x)), $F \subcaption{Logical rules} \end{ttbox} @@ -194,11 +203,11 @@ by the representation of sequents. Type $sobj\To sobj$ represents a list of formulae. -The {\bf definite description} operator~$\iota x.P[x]$ stands for some~$a$ +The {\bf definite description} operator~$\iota x. P[x]$ stands for some~$a$ satisfying~$P[a]$, if one exists and is unique. Since all terms in \LK{} denote something, a description is always meaningful, but we do not know its value unless $P[x]$ defines it uniquely. The Isabelle notation is -\hbox{\tt THE $x$.$P[x]$}. The corresponding rule (Fig.\ts\ref{lk-rules}) +\hbox{\tt THE $x$. $P[x]$}. The corresponding rule (Fig.\ts\ref{lk-rules}) does not entail the Axiom of Choice because it requires uniqueness. Figure~\ref{lk-grammar} presents the grammar of \LK. Traditionally, @@ -241,8 +250,8 @@ \tdx{iffL} [| $H, $G |- $E, P, Q; $H, Q, P, $G |- $E |] ==> $H, P<->Q, $G |- $E -\tdx{allL_thin} $H, P(x), $G |- $E ==> $H, ALL x.P(x), $G |- $E -\tdx{exR_thin} $H |- $E, P(x), $F ==> $H |- $E, EX x.P(x), $F +\tdx{allL_thin} $H, P(x), $G |- $E ==> $H, ALL x. P(x), $G |- $E +\tdx{exR_thin} $H |- $E, P(x), $F ==> $H |- $E, EX x. P(x), $F \end{ttbox} \caption{Derived rules for {\tt LK}} \label{lk-derived} @@ -470,7 +479,7 @@ proofs are essentially the same; the key step here is to use \tdx{exR} rather than the weaker~\tdx{exR_thin}. \begin{ttbox} -goal LK.thy "|- EX y. ALL x. P(y)-->P(x)"; +Goal "|- EX y. ALL x. P(y)-->P(x)"; {\out Level 0} {\out |- EX y. ALL x. P(y) --> P(x)} {\out 1. |- EX y. ALL x. P(y) --> P(x)} @@ -517,7 +526,7 @@ {\out 1. !!x xa. P(?x), P(?x7(x)) |- P(x), P(xa)} \end{ttbox} Subgoal~1 seems to offer lots of possibilities. Actually the only useful -step is instantiating~$\Var{x@7}$ to $\lambda x.x$, +step is instantiating~$\Var{x@7}$ to $\lambda x. x$, transforming~$\Var{x@7}(x)$ into~$x$. \begin{ttbox} by (resolve_tac [basic] 1); @@ -528,7 +537,7 @@ This theorem can be proved automatically. Because it involves quantifier duplication, we employ best-first search: \begin{ttbox} -goal LK.thy "|- EX y. ALL x. P(y)-->P(x)"; +Goal "|- EX y. ALL x. P(y)-->P(x)"; {\out Level 0} {\out |- EX y. ALL x. P(y) --> P(x)} {\out 1. |- EX y. ALL x. P(y) --> P(x)} @@ -553,7 +562,7 @@ We set the main goal and move the negated formula to the left. \begin{ttbox} -goal LK.thy "|- ~ (EX x. ALL y. F(y,x) <-> ~F(y,y))"; +Goal "|- ~ (EX x. ALL y. F(y,x) <-> ~F(y,y))"; {\out Level 0} {\out |- ~ (EX x. ALL y. F(y,x) <-> ~ F(y,y))} {\out 1. |- ~ (EX x. ALL y. F(y,x) <-> ~ F(y,y))} diff -r 6e2e9b92c301 -r 1e944fe5ce96 doc-src/Logics/ZF-eg.txt --- a/doc-src/Logics/ZF-eg.txt Thu Jul 16 10:35:31 1998 +0200 +++ b/doc-src/Logics/ZF-eg.txt Thu Jul 16 11:50:01 1998 +0200 @@ -27,17 +27,17 @@ choplev 0; by (fast_tac (ZF_cs addIs [equalityI]) 1); -val [prem] = goal ZF.thy "C<=D ==> Union(C) <= Union(D)"; +Goal "C<=D ==> Union(C) <= Union(D)"; by (resolve_tac [subsetI] 1); by (eresolve_tac [UnionE] 1); by (resolve_tac [UnionI] 1); -by (resolve_tac [prem RS subsetD] 1); +by (eresolve_tac [subsetD] 1); by (assume_tac 1); by (assume_tac 1); choplev 0; by (resolve_tac [Union_least] 1); by (resolve_tac [Union_upper] 1); -by (eresolve_tac [prem RS subsetD] 1); +by (eresolve_tac [subsetD] 1); val prems = goal ZF.thy @@ -54,6 +54,19 @@ by (resolve_tac prems 1); +Goal "[| a:A; f: A->B; g: C->D; A Int C = 0 |] ==> \ +\ (f Un g)`a = f`a"; +by (resolve_tac [apply_equality] 1); +by (resolve_tac [UnI1] 1); +by (resolve_tac [apply_Pair] 1); +by (assume_tac 1); +by (assume_tac 1); +by (resolve_tac [fun_disjoint_Un] 1); +by (assume_tac 1); +by (assume_tac 1); +by (assume_tac 1); + + goal ZF.thy "f``(UN x:A. B(x)) = (UN x:A. f``B(x))"; diff -r 6e2e9b92c301 -r 1e944fe5ce96 doc-src/Logics/ZF.tex --- a/doc-src/Logics/ZF.tex Thu Jul 16 10:35:31 1998 +0200 +++ b/doc-src/Logics/ZF.tex Thu Jul 16 11:50:01 1998 +0200 @@ -195,31 +195,31 @@ <$a@1$, $\ldots$, $a@{n-1}$, $a@n$> & Pair($a@1$,\ldots,Pair($a@{n-1}$,$a@n$)\ldots) & \rm ordered $n$-tuple \\ - \ttlbrace$x$:$A . P[x]$\ttrbrace & Collect($A$,$\lambda x.P[x]$) & + \ttlbrace$x$:$A . P[x]$\ttrbrace & Collect($A$,$\lambda x. P[x]$) & \rm separation \\ - \ttlbrace$y . x$:$A$, $Q[x,y]$\ttrbrace & Replace($A$,$\lambda x\,y.Q[x,y]$) & + \ttlbrace$y . x$:$A$, $Q[x,y]$\ttrbrace & Replace($A$,$\lambda x\,y. Q[x,y]$) & \rm replacement \\ - \ttlbrace$b[x] . x$:$A$\ttrbrace & RepFun($A$,$\lambda x.b[x]$) & + \ttlbrace$b[x] . x$:$A$\ttrbrace & RepFun($A$,$\lambda x. b[x]$) & \rm functional replacement \\ \sdx{INT} $x$:$A . B[x]$ & Inter(\ttlbrace$B[x] . x$:$A$\ttrbrace) & \rm general intersection \\ \sdx{UN} $x$:$A . B[x]$ & Union(\ttlbrace$B[x] . x$:$A$\ttrbrace) & \rm general union \\ - \sdx{PROD} $x$:$A . B[x]$ & Pi($A$,$\lambda x.B[x]$) & + \sdx{PROD} $x$:$A . B[x]$ & Pi($A$,$\lambda x. B[x]$) & \rm general product \\ - \sdx{SUM} $x$:$A . B[x]$ & Sigma($A$,$\lambda x.B[x]$) & + \sdx{SUM} $x$:$A . B[x]$ & Sigma($A$,$\lambda x. B[x]$) & \rm general sum \\ - $A$ -> $B$ & Pi($A$,$\lambda x.B$) & + $A$ -> $B$ & Pi($A$,$\lambda x. B$) & \rm function space \\ - $A$ * $B$ & Sigma($A$,$\lambda x.B$) & + $A$ * $B$ & Sigma($A$,$\lambda x. B$) & \rm binary product \\ - \sdx{THE} $x . P[x]$ & The($\lambda x.P[x]$) & + \sdx{THE} $x . P[x]$ & The($\lambda x. P[x]$) & \rm definite description \\ - \sdx{lam} $x$:$A . b[x]$ & Lambda($A$,$\lambda x.b[x]$) & + \sdx{lam} $x$:$A . b[x]$ & Lambda($A$,$\lambda x. b[x]$) & \rm $\lambda$-abstraction\\[1ex] - \sdx{ALL} $x$:$A . P[x]$ & Ball($A$,$\lambda x.P[x]$) & + \sdx{ALL} $x$:$A . P[x]$ & Ball($A$,$\lambda x. P[x]$) & \rm bounded $\forall$ \\ - \sdx{EX} $x$:$A . P[x]$ & Bex($A$,$\lambda x.P[x]$) & + \sdx{EX} $x$:$A . P[x]$ & Bex($A$,$\lambda x. P[x]$) & \rm bounded $\exists$ \end{tabular} \end{center} @@ -278,17 +278,17 @@ \section{Binding operators} The constant \cdx{Collect} constructs sets by the principle of {\bf separation}. The syntax for separation is -\hbox{\tt\ttlbrace$x$:$A$.$P[x]$\ttrbrace}, where $P[x]$ is a formula +\hbox{\tt\ttlbrace$x$:$A$. $P[x]$\ttrbrace}, where $P[x]$ is a formula that may contain free occurrences of~$x$. It abbreviates the set {\tt - Collect($A$,$\lambda x.P[x]$)}, which consists of all $x\in A$ that + Collect($A$,$\lambda x. P[x]$)}, which consists of all $x\in A$ that satisfy~$P[x]$. Note that \texttt{Collect} is an unfortunate choice of name: some set theories adopt a set-formation principle, related to replacement, called collection. The constant \cdx{Replace} constructs sets by the principle of {\bf replacement}. The syntax -\hbox{\tt\ttlbrace$y$.$x$:$A$,$Q[x,y]$\ttrbrace} denotes the set {\tt - Replace($A$,$\lambda x\,y.Q[x,y]$)}, which consists of all~$y$ such +\hbox{\tt\ttlbrace$y$. $x$:$A$,$Q[x,y]$\ttrbrace} denotes the set {\tt + Replace($A$,$\lambda x\,y. Q[x,y]$)}, which consists of all~$y$ such that there exists $x\in A$ satisfying~$Q[x,y]$. The Replacement Axiom has the condition that $Q$ must be single-valued over~$A$: for all~$x\in A$ there exists at most one $y$ satisfying~$Q[x,y]$. A @@ -297,16 +297,16 @@ The constant \cdx{RepFun} expresses a special case of replacement, where $Q[x,y]$ has the form $y=b[x]$. Such a $Q$ is trivially single-valued, since it is just the graph of the meta-level -function~$\lambda x.b[x]$. The resulting set consists of all $b[x]$ +function~$\lambda x. b[x]$. The resulting set consists of all $b[x]$ for~$x\in A$. This is analogous to the \ML{} functional \texttt{map}, since it applies a function to every element of a set. The syntax is -\hbox{\tt\ttlbrace$b[x]$.$x$:$A$\ttrbrace}, which expands to {\tt - RepFun($A$,$\lambda x.b[x]$)}. +\hbox{\tt\ttlbrace$b[x]$. $x$:$A$\ttrbrace}, which expands to {\tt + RepFun($A$,$\lambda x. b[x]$)}. \index{*INT symbol}\index{*UN symbol} General unions and intersections of indexed families of sets, namely $\bigcup@{x\in A}B[x]$ and $\bigcap@{x\in A}B[x]$, -are written \hbox{\tt UN $x$:$A$.$B[x]$} and \hbox{\tt INT $x$:$A$.$B[x]$}. +are written \hbox{\tt UN $x$:$A$. $B[x]$} and \hbox{\tt INT $x$:$A$. $B[x]$}. Their meaning is expressed using \texttt{RepFun} as \[ \bigcup(\{B[x]. x\in A\}) \qquad\hbox{and}\qquad @@ -319,7 +319,7 @@ has `dependent sets') and calls for similar syntactic conventions. The constants~\cdx{Sigma} and~\cdx{Pi} construct general sums and products. Instead of \texttt{Sigma($A$,$B$)} and \texttt{Pi($A$,$B$)} we may write -\hbox{\tt SUM $x$:$A$.$B[x]$} and \hbox{\tt PROD $x$:$A$.$B[x]$}. +\hbox{\tt SUM $x$:$A$. $B[x]$} and \hbox{\tt PROD $x$:$A$. $B[x]$}. \index{*SUM symbol}\index{*PROD symbol}% The special cases as \hbox{\tt$A$*$B$} and \hbox{\tt$A$->$B$} abbreviate general sums and products over a constant family.\footnote{Unlike normal @@ -331,28 +331,28 @@ As mentioned above, whenever the axioms assert the existence and uniqueness of a set, Isabelle's set theory declares a constant for that set. These constants can express the {\bf definite description} operator~$\iota -x.P[x]$, which stands for the unique~$a$ satisfying~$P[a]$, if such exists. +x. P[x]$, which stands for the unique~$a$ satisfying~$P[a]$, if such exists. Since all terms in {\ZF} denote something, a description is always meaningful, but we do not know its value unless $P[x]$ defines it uniquely. Using the constant~\cdx{The}, we may write descriptions as {\tt - The($\lambda x.P[x]$)} or use the syntax \hbox{\tt THE $x$.$P[x]$}. + The($\lambda x. P[x]$)} or use the syntax \hbox{\tt THE $x$. $P[x]$}. \index{*lam symbol} -Function sets may be written in $\lambda$-notation; $\lambda x\in A.b[x]$ +Function sets may be written in $\lambda$-notation; $\lambda x\in A. b[x]$ stands for the set of all pairs $\pair{x,b[x]}$ for $x\in A$. In order for this to be a set, the function's domain~$A$ must be given. Using the constant~\cdx{Lambda}, we may express function sets as {\tt -Lambda($A$,$\lambda x.b[x]$)} or use the syntax \hbox{\tt lam $x$:$A$.$b[x]$}. +Lambda($A$,$\lambda x. b[x]$)} or use the syntax \hbox{\tt lam $x$:$A$. $b[x]$}. Isabelle's set theory defines two {\bf bounded quantifiers}: \begin{eqnarray*} - \forall x\in A.P[x] &\hbox{abbreviates}& \forall x. x\in A\imp P[x] \\ - \exists x\in A.P[x] &\hbox{abbreviates}& \exists x. x\in A\conj P[x] + \forall x\in A. P[x] &\hbox{abbreviates}& \forall x. x\in A\imp P[x] \\ + \exists x\in A. P[x] &\hbox{abbreviates}& \exists x. x\in A\conj P[x] \end{eqnarray*} The constants~\cdx{Ball} and~\cdx{Bex} are defined accordingly. Instead of \texttt{Ball($A$,$P$)} and \texttt{Bex($A$,$P$)} we may write -\hbox{\tt ALL $x$:$A$.$P[x]$} and \hbox{\tt EX $x$:$A$.$P[x]$}. +\hbox{\tt ALL $x$:$A$. $P[x]$} and \hbox{\tt EX $x$:$A$. $P[x]$}. %%%% ZF.thy @@ -376,7 +376,7 @@ \subcaption{The Zermelo-Fraenkel Axioms} \tdx{Replace_def} Replace(A,P) == - PrimReplace(A, \%x y. (EX!z.P(x,z)) & P(x,y)) + PrimReplace(A, \%x y. (EX!z. P(x,z)) & P(x,y)) \tdx{RepFun_def} RepFun(A,f) == {\ttlbrace}y . x:A, y=f(x)\ttrbrace \tdx{the_def} The(P) == Union({\ttlbrace}y . x:{\ttlbrace}0{\ttrbrace}, P(y){\ttrbrace}) \tdx{if_def} if(P,a,b) == THE z. P & z=a | ~P & z=b @@ -404,8 +404,8 @@ \tdx{Pair_def} == {\ttlbrace}{\ttlbrace}a,a{\ttrbrace}, {\ttlbrace}a,b{\ttrbrace}{\ttrbrace} \tdx{split_def} split(c,p) == THE y. EX a b. p= & y=c(a,b) -\tdx{fst_def} fst(A) == split(\%x y.x, p) -\tdx{snd_def} snd(A) == split(\%x y.y, p) +\tdx{fst_def} fst(A) == split(\%x y. x, p) +\tdx{snd_def} snd(A) == split(\%x y. y, p) \tdx{Sigma_def} Sigma(A,B) == UN x:A. UN y:B(x). {\ttlbrace}{\ttrbrace} \subcaption{Ordered pairs and Cartesian products} @@ -420,7 +420,7 @@ \tdx{lam_def} Lambda(A,b) == {\ttlbrace} . x:A{\ttrbrace} \tdx{apply_def} f`a == THE y. : f \tdx{Pi_def} Pi(A,B) == {\ttlbrace}f: Pow(Sigma(A,B)). ALL x:A. EX! y. : f{\ttrbrace} -\tdx{restrict_def} restrict(f,A) == lam x:A.f`x +\tdx{restrict_def} restrict(f,A) == lam x:A. f`x \subcaption{Functions and general product} \end{ttbox} \caption{Further definitions of {\ZF}} \label{zf-defs} @@ -441,7 +441,7 @@ subject to the condition that $P(x,y)$ is single-valued for all~$x\in A$. The Isabelle theory defines \cdx{Replace} to apply \cdx{PrimReplace} to the single-valued part of~$P$, namely -\[ (\exists!z.P(x,z)) \conj P(x,y). \] +\[ (\exists!z. P(x,z)) \conj P(x,y). \] Thus $y\in \texttt{Replace}(A,P)$ if and only if there is some~$x$ such that $P(x,-)$ holds uniquely for~$y$. Because the equivalence is unconditional, \texttt{Replace} is much easier to use than \texttt{PrimReplace}; it defines the @@ -493,14 +493,14 @@ (ALL x:A. P(x)) <-> (ALL x:A'. P'(x)) \tdx{bexI} [| P(x); x: A |] ==> EX x:A. P(x) -\tdx{bexCI} [| ALL x:A. ~P(x) ==> P(a); a: A |] ==> EX x:A.P(x) +\tdx{bexCI} [| ALL x:A. ~P(x) ==> P(a); a: A |] ==> EX x:A. P(x) \tdx{bexE} [| EX x:A. P(x); !!x. [| x:A; P(x) |] ==> Q |] ==> Q \tdx{bex_cong} [| A=A'; !!x. x:A' ==> P(x) <-> P'(x) |] ==> (EX x:A. P(x)) <-> (EX x:A'. P'(x)) \subcaption{Bounded quantifiers} -\tdx{subsetI} (!!x.x:A ==> x:B) ==> A <= B +\tdx{subsetI} (!!x. x:A ==> x:B) ==> A <= B \tdx{subsetD} [| A <= B; c:A |] ==> c:B \tdx{subsetCE} [| A <= B; ~(c:A) ==> P; c:B ==> P |] ==> P \tdx{subset_refl} A <= A @@ -768,7 +768,7 @@ \tdx{fst_conv} fst() = a \tdx{snd_conv} snd() = b -\tdx{split} split(\%x y.c(x,y), ) = c(a,b) +\tdx{split} split(\%x y. c(x,y), ) = c(a,b) \tdx{SigmaI} [| a:A; b:B(a) |] ==> : Sigma(A,B) @@ -803,12 +803,12 @@ In addition, it is possible to use tuples as patterns in abstractions: \begin{center} -{\tt\%<$x$,$y$>.$t$} \quad stands for\quad \texttt{split(\%$x$ $y$.$t$)} +{\tt\%<$x$,$y$>. $t$} \quad stands for\quad \texttt{split(\%$x$ $y$. $t$)} \end{center} Nested patterns are translated recursively: -{\tt\%<$x$,$y$,$z$>.$t$} $\leadsto$ {\tt\%<$x$,<$y$,$z$>>.$t$} $\leadsto$ -\texttt{split(\%$x$.\%<$y$,$z$>.$t$)} $\leadsto$ \texttt{split(\%$x$.split(\%$y$ - $z$.$t$))}. The reverse translation is performed upon printing. +{\tt\%<$x$,$y$,$z$>. $t$} $\leadsto$ {\tt\%<$x$,<$y$,$z$>>. $t$} $\leadsto$ +\texttt{split(\%$x$.\%<$y$,$z$>. $t$)} $\leadsto$ \texttt{split(\%$x$. split(\%$y$ + $z$. $t$))}. The reverse translation is performed upon printing. \begin{warn} The translation between patterns and \texttt{split} is performed automatically by the parser and printer. Thus the internal and external form of a term @@ -918,9 +918,9 @@ \tdx{lamE} [| p: (lam x:A. b(x)); !!x.[| x:A; p= |] ==> P |] ==> P -\tdx{lam_type} [| !!x. x:A ==> b(x): B(x) |] ==> (lam x:A.b(x)) : Pi(A,B) +\tdx{lam_type} [| !!x. x:A ==> b(x): B(x) |] ==> (lam x:A. b(x)) : Pi(A,B) -\tdx{beta} a : A ==> (lam x:A.b(x)) ` a = b(a) +\tdx{beta} a : A ==> (lam x:A. b(x)) ` a = b(a) \tdx{eta} f : Pi(A,B) ==> (lam x:A. f`x) = f \end{ttbox} \caption{$\lambda$-abstraction} \label{zf-lam} @@ -1274,8 +1274,8 @@ \tdx{rec_def} rec(k,a,b) == transrec(k, \%n f. nat_case(a, \%m. b(m, f`m), n)) -\tdx{add_def} m#+n == rec(m, n, \%u v.succ(v)) -\tdx{diff_def} m#-n == rec(n, m, \%u v. rec(v, 0, \%x y.x)) +\tdx{add_def} m#+n == rec(m, n, \%u v. succ(v)) +\tdx{diff_def} m#-n == rec(n, m, \%u v. rec(v, 0, \%x y. x)) \tdx{mult_def} m#*n == rec(m, 0, \%u v. n #+ v) \tdx{mod_def} m mod n == transrec(m, \%j f. if(j:n, j, f`(j#-n))) \tdx{div_def} m div n == transrec(m, \%j f. if(j:n, 0, succ(f`(j#-n)))) @@ -1375,7 +1375,7 @@ \underscoreon %%because @ is used here \begin{ttbox} \tdx{list_rec_def} list_rec(l,c,h) == - Vrec(l, \%l g.list_case(c, \%x xs. h(x, xs, g`xs), l)) + Vrec(l, \%l g. list_case(c, \%x xs. h(x, xs, g`xs), l)) \tdx{map_def} map(f,l) == list_rec(l, 0, \%x xs r. ) \tdx{length_def} length(l) == list_rec(l, 0, \%x xs r. succ(r)) @@ -1401,8 +1401,8 @@ \tdx{list_rec_Nil} list_rec(Nil,c,h) = c \tdx{list_rec_Cons} list_rec(Cons(a,l), c, h) = h(a, l, list_rec(l,c,h)) -\tdx{map_ident} l: list(A) ==> map(\%u.u, l) = l -\tdx{map_compose} l: list(A) ==> map(h, map(j,l)) = map(\%u.h(j(u)), l) +\tdx{map_ident} l: list(A) ==> map(\%u. u, l) = l +\tdx{map_compose} l: list(A) ==> map(h, map(j,l)) = map(\%u. h(j(u)), l) \tdx{map_app_distrib} xs: list(A) ==> map(h, xs@ys) = map(h,xs) @ map(h,ys) \tdx{map_type} [| l: list(A); !!x. x: A ==> h(x): B |] ==> map(h,l) : list(B) @@ -1505,8 +1505,8 @@ The extraction of rewrite rules takes set theory primitives into account. It can strip bounded universal quantifiers from a formula; for example, -${\forall x\in A.f(x)=g(x)}$ yields the conditional rewrite rule $x\in A \Imp -f(x)=g(x)$. Given $a\in\{x\in A.P(x)\}$ it extracts rewrite rules from +${\forall x\in A. f(x)=g(x)}$ yields the conditional rewrite rule $x\in A \Imp +f(x)=g(x)$. Given $a\in\{x\in A. P(x)\}$ it extracts rewrite rules from $a\in A$ and~$P(a)$. It can also break down $a\in A\int B$ and $a\in A-B$. The default simplification set contains congruence rules for @@ -1611,7 +1611,7 @@ We enter the goal and make the first step, which breaks the equation into two inclusions by extensionality:\index{*equalityI theorem} \begin{ttbox} -goal thy "Pow(A Int B) = Pow(A) Int Pow(B)"; +Goal "Pow(A Int B) = Pow(A) Int Pow(B)"; {\out Level 0} {\out Pow(A Int B) = Pow(A) Int Pow(B)} {\out 1. Pow(A Int B) = Pow(A) Int Pow(B)} @@ -1725,16 +1725,15 @@ ${C\subseteq D}$ implies $\bigcup(C)\subseteq \bigcup(D)$. To begin, we tackle the inclusion using \tdx{subsetI}: \begin{ttbox} -val [prem] = goal thy "C<=D ==> Union(C) <= Union(D)"; +Goal "C<=D ==> Union(C) <= Union(D)"; {\out Level 0} -{\out Union(C) <= Union(D)} -{\out 1. Union(C) <= Union(D)} -{\out val prem = "C <= D [C <= D]" : thm} +{\out C <= D ==> Union(C) <= Union(D)} +{\out 1. C <= D ==> Union(C) <= Union(D)} \ttbreak by (resolve_tac [subsetI] 1); {\out Level 1} -{\out Union(C) <= Union(D)} -{\out 1. !!x. x : Union(C) ==> x : Union(D)} +{\out C <= D ==> Union(C) <= Union(D)} +{\out 1. !!x. [| C <= D; x : Union(C) |] ==> x : Union(D)} \end{ttbox} Big union is like an existential quantifier --- the occurrence in the assumptions must be eliminated early, since it creates parameters. @@ -1742,8 +1741,8 @@ \begin{ttbox} by (eresolve_tac [UnionE] 1); {\out Level 2} -{\out Union(C) <= Union(D)} -{\out 1. !!x B. [| x : B; B : C |] ==> x : Union(D)} +{\out C <= D ==> Union(C) <= Union(D)} +{\out 1. !!x B. [| C <= D; x : B; B : C |] ==> x : Union(D)} \end{ttbox} Now we may apply \tdx{UnionI}, which creates an unknown involving the parameters. To show $x\in \bigcup(D)$ it suffices to show that $x$ belongs @@ -1751,58 +1750,48 @@ \begin{ttbox} by (resolve_tac [UnionI] 1); {\out Level 3} -{\out Union(C) <= Union(D)} -{\out 1. !!x B. [| x : B; B : C |] ==> ?B2(x,B) : D} -{\out 2. !!x B. [| x : B; B : C |] ==> x : ?B2(x,B)} +{\out C <= D ==> Union(C) <= Union(D)} +{\out 1. !!x B. [| C <= D; x : B; B : C |] ==> ?B2(x,B) : D} +{\out 2. !!x B. [| C <= D; x : B; B : C |] ==> x : ?B2(x,B)} \end{ttbox} -Combining \tdx{subsetD} with the premise $C\subseteq D$ yields -$\Var{a}\in C \Imp \Var{a}\in D$, which reduces subgoal~1: +Combining \tdx{subsetD} with the assumption $C\subseteq D$ yields +$\Var{a}\in C \Imp \Var{a}\in D$, which reduces subgoal~1. Note that +\texttt{eresolve_tac} has removed that assumption. \begin{ttbox} -by (resolve_tac [prem RS subsetD] 1); +by (eresolve_tac [subsetD] 1); {\out Level 4} -{\out Union(C) <= Union(D)} +{\out C <= D ==> Union(C) <= Union(D)} {\out 1. !!x B. [| x : B; B : C |] ==> ?B2(x,B) : C} -{\out 2. !!x B. [| x : B; B : C |] ==> x : ?B2(x,B)} +{\out 2. !!x B. [| C <= D; x : B; B : C |] ==> x : ?B2(x,B)} \end{ttbox} -The rest is routine. Note how~$\Var{B2}(x,B)$ is instantiated. +The rest is routine. Observe how~$\Var{B2}(x,B)$ is instantiated. \begin{ttbox} by (assume_tac 1); {\out Level 5} -{\out Union(C) <= Union(D)} -{\out 1. !!x B. [| x : B; B : C |] ==> x : B} +{\out C <= D ==> Union(C) <= Union(D)} +{\out 1. !!x B. [| C <= D; x : B; B : C |] ==> x : B} by (assume_tac 1); {\out Level 6} -{\out Union(C) <= Union(D)} +{\out C <= D ==> Union(C) <= Union(D)} {\out No subgoals!} \end{ttbox} -Again, \ttindex{Blast_tac} can prove the theorem in one -step, provided we somehow supply it with~\texttt{prem}. We can add -\hbox{\tt prem RS subsetD} to the claset as an introduction rule: +Again, \ttindex{Blast_tac} can prove the theorem in one step. \begin{ttbox} -by (blast_tac (claset() addIs [prem RS subsetD]) 1); +by (Blast_tac 1); {\out Depth = 0} {\out Depth = 1} {\out Depth = 2} {\out Level 1} -{\out Union(C) <= Union(D)} +{\out C <= D ==> Union(C) <= Union(D)} {\out No subgoals!} \end{ttbox} -As an alternative, we could add premise to the assumptions, either using -\ttindex{cut_facts_tac} or by stating the original goal using~\texttt{!!}: -\begin{ttbox} -goal thy "!!C D. C<=D ==> Union(C) <= Union(D)"; -{\out Level 0} -{\out Union(C) <= Union(D)} -{\out 1. !!C D. C <= D ==> Union(C) <= Union(D)} -by (Blast_tac 1); -\end{ttbox} The file \texttt{ZF/equalities.ML} has many similar proofs. Reasoning about general intersection can be difficult because of its anomalous behaviour on the empty set. However, \ttindex{Blast_tac} copes well with these. Here is a typical example, borrowed from Devlin~\cite[page 12]{devlin79}: \begin{ttbox} -a:C ==> (INT x:C. A(x) Int B(x)) = (INT x:C.A(x)) Int (INT x:C.B(x)) +a:C ==> (INT x:C. A(x) Int B(x)) = (INT x:C. A(x)) Int (INT x:C. B(x)) \end{ttbox} In traditional notation this is \[ a\in C \,\Imp\, \inter@{x\in C} \Bigl(A(x) \int B(x)\Bigr) = @@ -1819,88 +1808,82 @@ functions with disjoint domains~$A$ and~$C$, and if $a\in A$, then $(f\un g)`a = f`a$: \begin{ttbox} -val prems = goal thy - "[| a:A; f: A->B; g: C->D; A Int C = 0 |] ==> \ttback +Goal "[| a:A; f: A->B; g: C->D; A Int C = 0 |] ==> \ttback \ttback (f Un g)`a = f`a"; {\out Level 0} -{\out (f Un g) ` a = f ` a} -{\out 1. (f Un g) ` a = f ` a} -\end{ttbox} -Isabelle has produced the output above; the \ML{} top-level now echoes the -binding of \texttt{prems}. -\begin{ttbox} -{\out val prems = ["a : A [a : A]",} -{\out "f : A -> B [f : A -> B]",} -{\out "g : C -> D [g : C -> D]",} -{\out "A Int C = 0 [A Int C = 0]"] : thm list} +{\out [| a : A; f : A -> B; g : C -> D; A Int C = 0 |]} +{\out ==> (f Un g) ` a = f ` a} +{\out 1. [| a : A; f : A -> B; g : C -> D; A Int C = 0 |]} +{\out ==> (f Un g) ` a = f ` a} \end{ttbox} Using \tdx{apply_equality}, we reduce the equality to reasoning about ordered pairs. The second subgoal is to verify that $f\un g$ is a function. +To save space, the assumptions will be abbreviated below. \begin{ttbox} by (resolve_tac [apply_equality] 1); {\out Level 1} -{\out (f Un g) ` a = f ` a} -{\out 1. : f Un g} -{\out 2. f Un g : (PROD x:?A. ?B(x))} +{\out [| \ldots |] ==> (f Un g) ` a = f ` a} +{\out 1. [| \ldots |] ==> : f Un g} +{\out 2. [| \ldots |] ==> f Un g : (PROD x:?A. ?B(x))} \end{ttbox} We must show that the pair belongs to~$f$ or~$g$; by~\tdx{UnI1} we choose~$f$: \begin{ttbox} by (resolve_tac [UnI1] 1); {\out Level 2} -{\out (f Un g) ` a = f ` a} -{\out 1. : f} -{\out 2. f Un g : (PROD x:?A. ?B(x))} +{\out [| \ldots |] ==> (f Un g) ` a = f ` a} +{\out 1. [| \ldots |] ==> : f} +{\out 2. [| \ldots |] ==> f Un g : (PROD x:?A. ?B(x))} \end{ttbox} To show $\pair{a,f`a}\in f$ we use \tdx{apply_Pair}, which is essentially the converse of \tdx{apply_equality}: \begin{ttbox} by (resolve_tac [apply_Pair] 1); {\out Level 3} -{\out (f Un g) ` a = f ` a} -{\out 1. f : (PROD x:?A2. ?B2(x))} -{\out 2. a : ?A2} -{\out 3. f Un g : (PROD x:?A. ?B(x))} +{\out [| \ldots |] ==> (f Un g) ` a = f ` a} +{\out 1. [| \ldots |] ==> f : (PROD x:?A2. ?B2(x))} +{\out 2. [| \ldots |] ==> a : ?A2} +{\out 3. [| \ldots |] ==> f Un g : (PROD x:?A. ?B(x))} \end{ttbox} -Using the premises $f\in A\to B$ and $a\in A$, we solve the two subgoals +Using the assumptions $f\in A\to B$ and $a\in A$, we solve the two subgoals from \tdx{apply_Pair}. Recall that a $\Pi$-set is merely a generalized function space, and observe that~{\tt?A2} is instantiated to~\texttt{A}. \begin{ttbox} -by (resolve_tac prems 1); +by (assume_tac 1); {\out Level 4} -{\out (f Un g) ` a = f ` a} -{\out 1. a : A} -{\out 2. f Un g : (PROD x:?A. ?B(x))} -by (resolve_tac prems 1); +{\out [| \ldots |] ==> (f Un g) ` a = f ` a} +{\out 1. [| \ldots |] ==> a : A} +{\out 2. [| \ldots |] ==> f Un g : (PROD x:?A. ?B(x))} +by (assume_tac 1); {\out Level 5} -{\out (f Un g) ` a = f ` a} -{\out 1. f Un g : (PROD x:?A. ?B(x))} +{\out [| \ldots |] ==> (f Un g) ` a = f ` a} +{\out 1. [| \ldots |] ==> f Un g : (PROD x:?A. ?B(x))} \end{ttbox} To construct functions of the form $f\un g$, we apply \tdx{fun_disjoint_Un}: \begin{ttbox} by (resolve_tac [fun_disjoint_Un] 1); {\out Level 6} -{\out (f Un g) ` a = f ` a} -{\out 1. f : ?A3 -> ?B3} -{\out 2. g : ?C3 -> ?D3} -{\out 3. ?A3 Int ?C3 = 0} +{\out [| \ldots |] ==> (f Un g) ` a = f ` a} +{\out 1. [| \ldots |] ==> f : ?A3 -> ?B3} +{\out 2. [| \ldots |] ==> g : ?C3 -> ?D3} +{\out 3. [| \ldots |] ==> ?A3 Int ?C3 = 0} \end{ttbox} -The remaining subgoals are instances of the premises. Again, observe how +The remaining subgoals are instances of the assumptions. Again, observe how unknowns are instantiated: \begin{ttbox} -by (resolve_tac prems 1); +by (assume_tac 1); {\out Level 7} -{\out (f Un g) ` a = f ` a} -{\out 1. g : ?C3 -> ?D3} -{\out 2. A Int ?C3 = 0} -by (resolve_tac prems 1); +{\out [| \ldots |] ==> (f Un g) ` a = f ` a} +{\out 1. [| \ldots |] ==> g : ?C3 -> ?D3} +{\out 2. [| \ldots |] ==> A Int ?C3 = 0} +by (assume_tac 1); {\out Level 8} -{\out (f Un g) ` a = f ` a} -{\out 1. A Int C = 0} -by (resolve_tac prems 1); +{\out [| \ldots |] ==> (f Un g) ` a = f ` a} +{\out 1. [| \ldots |] ==> A Int C = 0} +by (assume_tac 1); {\out Level 9} -{\out (f Un g) ` a = f ` a} +{\out [| \ldots |] ==> (f Un g) ` a = f ` a} {\out No subgoals!} \end{ttbox} See the files \texttt{ZF/func.ML} and \texttt{ZF/WF.ML} for more