# HG changeset patch # User lcp # Date 767033029 -7200 # Node ID 2ca08f62df333108c6a4f5b7451f8bd7c8a7c61a # Parent 01b87a921967d101965b61b99e5727ad9f0d4935 final Springer copy diff -r 01b87a921967 -r 2ca08f62df33 doc-src/Logics/CTT.tex --- a/doc-src/Logics/CTT.tex Fri Apr 22 18:18:37 1994 +0200 +++ b/doc-src/Logics/CTT.tex Fri Apr 22 18:43:49 1994 +0200 @@ -395,8 +395,8 @@ Elimination rules have the suffix~{\tt E}\@. Computation rules, which describe the reduction of eliminators, have the suffix~{\tt C}\@. The equality versions of the rules (which permit reductions on subterms) are -called {\em long} rules; their names have the suffix~{\tt L}\@. -Introduction and computation rules often are further suffixed with +called {\bf long} rules; their names have the suffix~{\tt L}\@. +Introduction and computation rules are often further suffixed with constructor names. Figure~\ref{ctt-equality} presents the equality rules. Most of them are @@ -514,12 +514,12 @@ \end{ttbox} Blind application of {\CTT} rules seldom leads to a proof. The elimination rules, especially, create subgoals containing new unknowns. These subgoals -unify with anything, causing an undirectional search. The standard tactic +unify with anything, creating a huge search space. The standard tactic \ttindex{filt_resolve_tac} (see \iflabelundefined{filt_resolve_tac}{the {\em Reference Manual\/}}% {\S\ref{filt_resolve_tac}}) % -can reject overly flexible goals; so does the {\CTT} tactic {\tt +fails for goals that are too flexible; so does the {\CTT} tactic {\tt test_assume_tac}. Used with the tactical \ttindex{REPEAT_FIRST} they achieve a simple kind of subgoal reordering: the less flexible subgoals are attempted first. Do some single step proofs, or study the examples below, @@ -623,7 +623,7 @@ \item[\ttindexbold{safestep_tac} $thms$ $i$] attacks subgoal~$i$ using formation rules and certain other `safe' rules -(tdx{FE}, tdx{ProdI}, tdx{SumE}, tdx{PlusE}), calling +(\tdx{FE}, \tdx{ProdI}, \tdx{SumE}, \tdx{PlusE}), calling {\tt mp_tac} when appropriate. It also uses~$thms$, which are typically premises of the rule being derived. @@ -708,7 +708,6 @@ \[ a \bmod b + (a/b)\times b = a. \] Figure~\ref{ctt-arith} presents the definitions and some of the key theorems, including commutative, distributive, and associative laws. -All proofs are on the file {\tt CTT/arith.ML}. The operators~\verb'#+', \verb'-', \verb'|-|', \verb'#*', \verb'mod' and~\verb'div' stand for sum, difference, absolute difference, product, @@ -1065,7 +1064,7 @@ function $g\in \prod@{x\in A}C(x,f{\tt`}x)$. In principle, the Axiom of Choice is simple to derive in Constructive Type -Theory \cite[page~50]{martinlof84}. The following definitions work: +Theory. The following definitions work: \begin{eqnarray*} f & \equiv & {\tt fst} \circ h \\ g & \equiv & {\tt snd} \circ h diff -r 01b87a921967 -r 2ca08f62df33 doc-src/Logics/FOL.tex --- a/doc-src/Logics/FOL.tex Fri Apr 22 18:18:37 1994 +0200 +++ b/doc-src/Logics/FOL.tex Fri Apr 22 18:43:49 1994 +0200 @@ -35,9 +35,9 @@ Some intuitionistic derived rules are shown in Fig.\ts\ref{fol-int-derived}, again with their \ML\ names. These include rules for the defined symbols $\neg$, $\bimp$ and $\exists!$. Natural -deduction typically involves a combination of forwards and backwards +deduction typically involves a combination of forward and backward reasoning, particularly with the destruction rules $(\conj E)$, -$({\imp}E)$, and~$(\forall E)$. Isabelle's backwards style handles these +$({\imp}E)$, and~$(\forall E)$. Isabelle's backward style handles these rules badly, so sequent-style rules are derived to eliminate conjunctions, implications, and universal quantifiers. Used with elim-resolution, \tdx{allE} eliminates a universal quantifier while \tdx{all_dupE} @@ -45,7 +45,7 @@ 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 +See the files {\tt FOL/IFOL.thy}, {\tt FOL/IFOL.ML} and {\tt FOL/intprover.ML} for complete listings of the rules and derived rules. @@ -360,7 +360,7 @@ generally unsuitable for depth-first search. \end{ttdescription} \noindent -See the file {\tt FOL/fol.ML} for derivations of the +See the file {\tt FOL/FOL.ML} for derivations of the classical rules, and \iflabelundefined{chap:classical}{the {\em Reference Manual\/}}% {Chap.\ts\ref{chap:classical}} @@ -582,7 +582,7 @@ {\out 1. !!x. [| ALL y. ~ (ALL x. P(y) --> P(x)); P(?a) |] ==> P(x)} \end{ttbox} By the duality between $\exists$ and~$\forall$, applying~$(\forall E)$ -effectively applies~$(\exists I)$ again. +in effect applies~$(\exists I)$ again. \begin{ttbox} by (eresolve_tac [allE] 1); {\out Level 4} @@ -622,7 +622,7 @@ {\out EX y. ALL x. P(y) --> P(x)} {\out No subgoals!} \end{ttbox} -The civilized way to prove this theorem is through \ttindex{best_tac}, +The civilised way to prove this theorem is through \ttindex{best_tac}, supplying the classical version of~$(\exists I)$: \begin{ttbox} goal FOL.thy "EX y. ALL x. P(y)-->P(x)"; @@ -778,8 +778,8 @@ {\out 3. [| ~ P; if(Q,C,D) |] ==> if(Q,if(P,A,C),if(P,B,D))} {\out 4. if(Q,if(P,A,C),if(P,B,D)) ==> if(P,if(Q,A,B),if(Q,C,D))} \end{ttbox} - -In the first two subgoals, all formulae have been reduced to atoms. Now +% +In the first two subgoals, all assumptions have been reduced to atoms. Now $if$-introduction can be applied. Observe how the $if$-rules break down occurrences of $if$ when they become the outermost connective. \begin{ttbox} diff -r 01b87a921967 -r 2ca08f62df33 doc-src/Logics/LK.tex --- a/doc-src/Logics/LK.tex Fri Apr 22 18:18:37 1994 +0200 +++ b/doc-src/Logics/LK.tex Fri Apr 22 18:43:49 1994 +0200 @@ -222,7 +222,7 @@ {\tt res_inst_tac} can instantiate the variable~{\tt?P} in these rules, specifying the formula to duplicate. -See the files {\tt LK/lk.thy} and {\tt LK/lk.ML} +See the files {\tt LK/LK.thy} and {\tt LK/LK.ML} for complete listings of the rules and derived rules. @@ -296,7 +296,7 @@ \end{ttbox} Associative unification is not as efficient as it might be, in part because the representation of lists defeats some of Isabelle's internal -optimizations. The following operations implement faster rule application, +optimisations. The following operations implement faster rule application, and may have other uses. \begin{ttdescription} \item[\ttindexbold{forms_of_seq} {\it t}]