# HG changeset patch # User paulson # Date 863018196 -7200 # Node ID 8c55b0f16da2098c80a7b3643ffc1c27b4bcdaba # Parent 8e956415412f1857e042155a0cf2fe8a449f93cd stylistic improvements diff -r 8e956415412f -r 8c55b0f16da2 doc-src/Logics/CTT.tex --- a/doc-src/Logics/CTT.tex Wed May 07 17:16:18 1997 +0200 +++ b/doc-src/Logics/CTT.tex Wed May 07 17:16:36 1997 +0200 @@ -669,7 +669,6 @@ \tdx{div_def} a div b == 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 \tdx{addC_succ} [| a:N; b:N |] ==> succ(a) #+ b = succ(a #+ b) : N diff -r 8e956415412f -r 8c55b0f16da2 doc-src/Logics/FOL.tex --- a/doc-src/Logics/FOL.tex Wed May 07 17:16:18 1997 +0200 +++ b/doc-src/Logics/FOL.tex Wed May 07 17:16:36 1997 +0200 @@ -196,11 +196,6 @@ \FOL{} instantiates most of Isabelle's generic packages. \begin{itemize} \item -Because it includes a general substitution rule, \FOL{} instantiates the -tactic \ttindex{hyp_subst_tac}, which substitutes for an equality -throughout a subgoal and its hypotheses. -(See {\tt FOL/ROOT.ML} for details.) -\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} use the default simpset ({\tt!simpset}), which works for @@ -215,8 +210,19 @@ \item It instantiates the classical reasoner. See~\S\ref{fol-cla-prover} for details. + +\item \FOL{} provides the tactic \ttindex{hyp_subst_tac}, which substitutes + for an equality throughout a subgoal and its hypotheses. This tactic uses + \FOL's general substitution rule. \end{itemize} +\begin{warn}\index{simplification!of conjunctions}% + Reducing $a=b\conj P(a)$ to $a=b\conj P(b)$ is sometimes advantageous. The + left part of a conjunction helps in simplifying the right part. This effect + is not available by default: it can be slow. It can be obtained by + including \ttindex{conj_cong} in a simpset, \verb$addcongs [conj_cong]$. +\end{warn} + \section{Intuitionistic proof procedures} \label{fol-int-prover} Implication elimination (the rules~{\tt mp} and~{\tt impE}) pose @@ -331,7 +337,7 @@ 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 Fast_tac} and {\tt +The classical reasoner is installed. Tactics such as {\tt Blast_tac} and {\tt Best_tac} use the default claset ({\tt!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 @@ -649,7 +655,7 @@ \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 fast_tac}. +so we use {\tt blast_tac}. \subsection{Deriving the introduction rule} @@ -665,10 +671,10 @@ {\out 1. P & Q | ~ P & R} \end{ttbox} The premises (bound to the {\ML} variable {\tt prems}) are passed as -introduction rules to \ttindex{fast_tac}. Remember that {\tt!claset} refers +introduction rules to \ttindex{blast_tac}. Remember that {\tt!claset} refers to the default classical set. \begin{ttbox} -by (fast_tac (!claset addIs prems) 1); +by (blast_tac (!claset addIs prems) 1); {\out Level 1} {\out if(P,Q,R)} {\out No subgoals!} @@ -689,14 +695,14 @@ 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 -assumption in the subgoal, so that \ttindex{fast_tac} can break it down. +assumption in the subgoal, so that \ttindex{blast_tac} can break it down. \begin{ttbox} by (cut_facts_tac [major] 1); {\out Level 1} {\out S} {\out 1. P & Q | ~ P & R ==> S} \ttbreak -by (fast_tac (!claset addIs prems) 1); +by (blast_tac (!claset addIs prems) 1); {\out Level 2} {\out S} {\out No subgoals!} @@ -789,13 +795,13 @@ AddSEs [ifE]; \end{ttbox} Now we can revert to the -initial proof state and let \ttindex{fast_tac} solve it. +initial proof state and let \ttindex{blast_tac} solve it. \begin{ttbox} choplev 0; {\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))} -by (Fast_tac 1); +by (Blast_tac 1); {\out Level 1} {\out if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))} {\out No subgoals!} @@ -807,7 +813,7 @@ {\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))} \ttbreak -by (Fast_tac 1); +by (Blast_tac 1); {\out Level 1} {\out if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))} {\out No subgoals!} @@ -816,7 +822,7 @@ \subsection{Derived rules versus definitions} Dispensing with the derived rules, we can treat $if$ as an -abbreviation, and let \ttindex{fast_tac} prove the expanded formula. Let +abbreviation, and let \ttindex{blast_tac} prove the expanded formula. Let us redo the previous proof: \begin{ttbox} choplev 0; @@ -834,9 +840,9 @@ \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 Fast_tac}.) +course, have used {\tt Blast_tac}.) \begin{ttbox} -by (fast_tac FOL_cs 1); +by (blast_tac FOL_cs 1); {\out Level 2} {\out if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))} {\out No subgoals!} @@ -858,7 +864,7 @@ {\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))} -by (Fast_tac 1); +by (Blast_tac 1); {\out by: tactic failed} \end{ttbox} This failure message is uninformative, but we can get a closer look at the @@ -889,7 +895,7 @@ {\out if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))} {\out 1. (P & Q | ~ P & R) & A | ~ (P & Q | ~ P & R) & B <->} {\out P & (Q & A | ~ Q & B) | ~ P & (R & B | ~ R & A)} -by (fast_tac FOL_cs 1); +by (blast_tac FOL_cs 1); {\out by: tactic failed} \end{ttbox} Again we apply \ttindex{step_tac}: diff -r 8e956415412f -r 8c55b0f16da2 doc-src/Logics/ZF.tex --- a/doc-src/Logics/ZF.tex Wed May 07 17:16:18 1997 +0200 +++ b/doc-src/Logics/ZF.tex Wed May 07 17:16:36 1997 +0200 @@ -65,7 +65,7 @@ $x$ is a set. -\begin{figure} +\begin{figure} \small \begin{center} \begin{tabular}{rrr} \it name &\it meta-type & \it description \\ @@ -1243,7 +1243,7 @@ have been proved. These results are fundamental to a treatment of equipollence and cardinality. -\begin{figure} +\begin{figure}\small \index{#*@{\tt\#*} symbol} \index{*div symbol} \index{*mod symbol} @@ -1293,9 +1293,8 @@ \tdx{mult_type} [| m:nat; n:nat |] ==> m #* n : nat \tdx{mult_0} 0 #* n = 0 \tdx{mult_succ} succ(m) #* n = n #+ (m #* n) -\tdx{mult_commute} [| m:nat; n:nat |] ==> m #* n = n #* m -\tdx{add_mult_dist} - [| m:nat; k:nat |] ==> (m #+ n) #* k = (m #* k) #+ (n #* k) +\tdx{mult_commute} [| m:nat; n:nat |] ==> m #* n = n #* m +\tdx{add_mult_dist} [| m:nat; k:nat |] ==> (m #+ n) #* k = (m #* k) #+ (n #* k) \tdx{mult_assoc} [| m:nat; n:nat; k:nat |] ==> (m #* n) #* k = m #* (n #* k) \tdx{mod_quo_equality} @@ -1689,24 +1688,23 @@ \end{ttbox} \medskip We could have performed this proof in one step by applying -\ttindex{Fast_tac}. Let us +\ttindex{Blast_tac}. Let us go back to the start: \begin{ttbox} choplev 0; {\out Level 0} {\out Pow(A Int B) = Pow(A) Int Pow(B)} {\out 1. Pow(A Int B) = Pow(A) Int Pow(B)} -\end{ttbox} -We must add \tdx{equalityI} as an introduction rule. -Extensionality is not used by default: many equalities can be proved -by rewriting. -\begin{ttbox} -by (fast_tac (!claset addIs [equalityI]) 1); +by (Blast_tac 1); +{\out Depth = 0} +{\out Depth = 1} +{\out Depth = 2} +{\out Depth = 3} {\out Level 1} {\out Pow(A Int B) = Pow(A) Int Pow(B)} {\out No subgoals!} \end{ttbox} -In the past this was regarded as a difficult proof, as indeed it is if all +Past researchers regarded this as a difficult proof, as indeed it is if all the symbols are replaced by their definitions. \goodbreak @@ -1765,14 +1763,31 @@ {\out Union(C) <= Union(D)} {\out No subgoals!} \end{ttbox} -Again, \ttindex{fast_tac} can prove the theorem in one -step, provided we somehow supply it with~{\tt prem}. We can either add -this premise to the assumptions using \ttindex{cut_facts_tac}, or add -\hbox{\tt prem RS subsetD} to the claset as an introduction rule. +Again, \ttindex{Blast_tac} can prove the theorem in one +step, provided we somehow supply it with~{\tt prem}. We can add +\hbox{\tt prem RS subsetD} to the claset as an introduction rule: +\begin{ttbox} +by (blast_tac (!claset addIs [prem RS subsetD]) 1); +{\out Depth = 0} +{\out Depth = 1} +{\out Depth = 2} +{\out Level 1} +{\out 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 {\tt 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{fast_tac} copes well with these. Here is +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))