# HG changeset patch # User paulson # Date 852733045 -3600 # Node ID 82ec47e0a8d3538c036ad616dc230747c51d61f5 # Parent 5d45c2094ff622954afb64514b9818488c67de3a New discussion of implicit simpsets & clasets diff -r 5d45c2094ff6 -r 82ec47e0a8d3 doc-src/Logics/FOL.tex --- a/doc-src/Logics/FOL.tex Wed Jan 08 15:12:44 1997 +0100 +++ b/doc-src/Logics/FOL.tex Wed Jan 08 15:17:25 1997 +0100 @@ -193,18 +193,20 @@ \section{Generic packages} -\FOL{} instantiates most of Isabelle's generic packages; -see {\tt FOL/ROOT.ML} for details. +\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. \ttindexbold{IFOL_ss} is the simplification -set for intuitionistic first-order logic, while \ttindexbold{FOL_ss} is the -simplification set for classical logic. Both equality ($=$) and the -biconditional ($\bimp$) may be used for rewriting. See the file +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 +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 rules% \iflabelundefined{sec:setting-up-simp}{}% @@ -329,30 +331,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 set up for \FOL, as the -structure~{\tt Cla}. This structure is open, so \ML{} identifiers -such as {\tt step_tac}, {\tt fast_tac}, {\tt best_tac}, etc., refer to it. -Single-step proofs can be performed, using \ttindex{swap_res_tac} to deal -with negated assumptions.\index{assumptions!negated} - -{\FOL} defines the following classical rule sets: -\begin{ttbox} -prop_cs : claset -FOL_cs : claset -\end{ttbox} -\begin{ttdescription} -\item[\ttindexbold{prop_cs}] contains the propositional rules, namely -those for~$\top$, $\bot$, $\conj$, $\disj$, $\neg$, $\imp$ and~$\bimp$, -along with the rule~{\tt refl}. - -\item[\ttindexbold{FOL_cs}] -extends {\tt prop_cs} with the safe rules {\tt allI} and~{\tt exE} -and the unsafe rules {\tt allE} and~{\tt exI}, as well as rules for -unique existence. Search using this is incomplete since quantified -formulae are used at most once. -\end{ttdescription} -\noindent -See the file {\tt FOL/FOL.ML} for derivations of the +The classical reasoner is installed. Tactics such as {\tt Fast_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 +rules. See the file {\tt FOL/cladata.ML} for lists of the classical rules, and \iflabelundefined{chap:classical}{the {\em Reference Manual\/}}% {Chap.\ts\ref{chap:classical}} @@ -621,7 +604,7 @@ {\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 FOL_cs 0 1); +by (Deepen_tac 0 1); {\out Depth = 0} {\out Depth = 2} {\out Level 1} @@ -682,9 +665,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}: +introduction rules to \ttindex{fast_tac}. Remember that {\tt!claset} refers +to the default classical set. \begin{ttbox} -by (fast_tac (FOL_cs addIs prems) 1); +by (fast_tac (!claset addIs prems) 1); {\out Level 1} {\out if(P,Q,R)} {\out No subgoals!} @@ -712,7 +696,7 @@ {\out S} {\out 1. P & Q | ~ P & R ==> S} \ttbreak -by (fast_tac (FOL_cs addIs prems) 1); +by (fast_tac (!claset addIs prems) 1); {\out Level 2} {\out S} {\out No subgoals!} @@ -723,7 +707,7 @@ {\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{rewrite_goals_tac} +{\tt 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 @@ -797,17 +781,21 @@ {\out 6. if(Q,if(P,A,C),if(P,B,D)) ==> if(P,if(Q,A,B),if(Q,C,D))} \end{ttbox} Where do we stand? The first subgoal holds by assumption; the second and -third, by contradiction. This is getting tedious. Let us revert to the -initial proof state and let \ttindex{fast_tac} solve it. The classical -rule set {\tt if_cs} contains the rules of~{\FOL} plus the derived rules +third, by contradiction. This is getting tedious. We could use the classical +reasoner, but first let us extend the default claset with the derived rules for~$if$. \begin{ttbox} +AddSIs [ifI]; +AddSEs [ifE]; +\end{ttbox} +Now we can revert to the +initial proof state and let \ttindex{fast_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))} -val if_cs = FOL_cs addSIs [ifI] addSEs[ifE]; -by (fast_tac if_cs 1); +by (Fast_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!} @@ -819,7 +807,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 if_cs 1); +by (Fast_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!} @@ -838,13 +826,15 @@ \end{ttbox} This time, simply unfold using the definition of $if$: \begin{ttbox} -by (rewrite_goals_tac [if_def]); +by (rewtac if_def); {\out Level 1} {\out if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))} {\out 1. (P & Q | ~ P & R) & A | ~ (P & Q | ~ P & R) & B <->} {\out P & (Q & A | ~ Q & B) | ~ P & (R & A | ~ R & B)} \end{ttbox} -We are left with a subgoal in pure first-order logic: +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}.) \begin{ttbox} by (fast_tac FOL_cs 1); {\out Level 2} @@ -853,8 +843,9 @@ \end{ttbox} Expanding definitions reduces the extended logic to the base logic. This approach has its merits --- especially if the prover for the base logic is -good --- but can be slow. In these examples, proofs using {\tt if_cs} (the -derived rules) run about six times faster than proofs using {\tt FOL_cs}. +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}. Expanding definitions also complicates error diagnosis. Suppose we are having difficulties in proving some goal. If by expanding definitions we have @@ -867,13 +858,13 @@ {\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 FOL_cs 1); +by (Fast_tac 1); {\out by: tactic failed} \end{ttbox} This failure message is uninformative, but we can get a closer look at the situation by applying \ttindex{step_tac}. \begin{ttbox} -by (REPEAT (step_tac if_cs 1)); +by (REPEAT (Step_tac 1)); {\out Level 1} {\out if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))} {\out 1. [| A; ~ P; R; ~ P; R |] ==> B} @@ -893,7 +884,7 @@ {\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))} \ttbreak -by (rewrite_goals_tac [if_def]); +by (rewtac if_def); {\out Level 1} {\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 <->} diff -r 5d45c2094ff6 -r 82ec47e0a8d3 doc-src/Logics/HOL.tex --- a/doc-src/Logics/HOL.tex Wed Jan 08 15:12:44 1997 +0100 +++ b/doc-src/Logics/HOL.tex Wed Jan 08 15:17:25 1997 +0100 @@ -838,8 +838,7 @@ \section{Generic packages} -\HOL\ instantiates most of Isabelle's generic packages; -see {\tt HOL/ROOT.ML} for details. +\HOL\ instantiates most of Isabelle's generic packages. \subsection{Substitution and simplification} @@ -847,10 +846,12 @@ tactic {\tt hyp_subst_tac}, which substitutes for an equality throughout a subgoal and its hypotheses. -It instantiates the simplifier, defining~\ttindexbold{HOL_ss} as the -simplification set for higher-order logic. Equality~($=$), which also -expresses logical equivalence, may be used for rewriting. See the file {\tt -HOL/simpdata.ML} for a complete listing of the simplification rules. +It instantiates the simplifier. Tactics such as {\tt Asm_simp_tac} and {\tt +Full_simp_tac} use the default simpset ({\tt!simpset}), which works for most +purposes. A minimal simplification set for higher-order logic +is~\ttindexbold{HOL_ss}. Equality~($=$), which also expresses logical +equivalence, may be used for rewriting. See the file {\tt HOL/simpdata.ML} +for a complete listing of the simplification rules. See \iflabelundefined{chap:classical}{the {\em Reference Manual\/}}% {Chaps.\ts\ref{substitution} and~\ref{simp-chap}} for details of substitution @@ -881,32 +882,14 @@ well as classical elimination rules for~$\imp$ and~$\bimp$, and the swap rule; recall Fig.\ts\ref{hol-lemmas2} above. -The classical reasoner is set up as the structure -{\tt Classical}. This structure is open, so {\ML} identifiers such -as {\tt step_tac}, {\tt fast_tac}, {\tt best_tac}, etc., refer to it. -\HOL\ defines the following classical rule sets: -\begin{ttbox} -prop_cs : claset -HOL_cs : claset -set_cs : claset -\end{ttbox} -\begin{ttdescription} -\item[\ttindexbold{prop_cs}] contains the propositional rules, namely -those for~$\top$, $\bot$, $\conj$, $\disj$, $\neg$, $\imp$ and~$\bimp$, -along with the rule~{\tt refl}. - -\item[\ttindexbold{HOL_cs}] extends {\tt prop_cs} with the safe rules - {\tt allI} and~{\tt exE} and the unsafe rules {\tt allE} - and~{\tt exI}, as well as rules for unique existence. Search using - this classical set is incomplete: quantified formulae are used at most - once. - -\item[\ttindexbold{set_cs}] extends {\tt HOL_cs} with rules for the bounded - quantifiers, subsets, comprehensions, unions and intersections, - complements, finite sets, images and ranges. -\end{ttdescription} -\noindent -See \iflabelundefined{chap:classical}{the {\em Reference Manual\/}}% +The classical reasoner is installed. Tactics such as {\tt Fast_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, \ttindexbold{HOL_cs}, which also includes quantifier +rules, and \ttindexbold{set_cs}, which also includes rules for subsets, +comprehensions, unions and intersections, etc. See the file +{\tt HOL/cladata.ML} for lists of the classical rules, and +\iflabelundefined{chap:classical}{the {\em Reference Manual\/}}% {Chap.\ts\ref{chap:classical}} for more discussion of classical proof methods. @@ -1537,9 +1520,8 @@ end \end{ttbox} After loading the theory (\verb$use_thy "MyList"$), we can prove -$Cons~x~xs\neq xs$. First we build a suitable simpset for the simplifier: +$Cons~x~xs\neq xs$. \begin{ttbox} -val mylist_ss = HOL_ss addsimps MyList.list.simps; goal MyList.thy "!x. Cons x xs ~= xs"; {\out Level 0} {\out ! x. Cons x xs ~= xs} @@ -1555,19 +1537,20 @@ {\out ! x. Cons x list ~= list ==>} {\out ! x. Cons x (Cons a list) ~= Cons a list} \end{ttbox} -The first subgoal can be proved with the simplifier and the distinctness -axioms which are part of \verb$mylist_ss$. +The first subgoal can be proved using the simplifier. +Isabelle has already added the freeness properties of lists to the +default simplification set. \begin{ttbox} -by (simp_tac mylist_ss 1); +by (Simp_tac 1); {\out Level 2} {\out ! x. Cons x xs ~= xs} {\out 1. !!a list.} {\out ! x. Cons x list ~= list ==>} {\out ! x. Cons x (Cons a list) ~= Cons a list} \end{ttbox} -Using the freeness axioms we can quickly prove the remaining goal. +Similarly, we prove the remaining goal. \begin{ttbox} -by (asm_simp_tac mylist_ss 1); +by (Asm_simp_tac 1); {\out Level 3} {\out ! x. Cons x xs ~= xs} {\out No subgoals!} @@ -1575,7 +1558,7 @@ Because both subgoals were proved by almost the same tactic we could have done that in one step using \begin{ttbox} -by (ALLGOALS (asm_simp_tac mylist_ss)); +by (ALLGOALS Asm_simp_tac); \end{ttbox} @@ -1604,17 +1587,17 @@ end \end{ttbox} Because there are more than four constructors, the theory must be based on -{\tt Arith}. Inequality is defined via a function \verb|days_ord|. Although -the expression \verb|Mo ~= Tu| is not directly contained in {\tt distinct}, -it can be proved by the simplifier if \verb$arith_ss$ is used: +{\tt Arith}. Inequality is defined via a function \verb|days_ord|. +The expression \verb|Mo ~= Tu| is not directly contained in {\tt distinct}, +but the simplifier can prove it thanks to rewrite rules inherited from theory +{\tt Arith}. \begin{ttbox} -val days_ss = arith_ss addsimps Days.days.simps; +goal Days.thy "Mo ~= Tu"; +by (Simp_tac 1); +\end{ttbox} +You need not derive such inequalities explicitly: the simplifier will dispose +of them automatically. -goal Days.thy "Mo ~= Tu"; -by (simp_tac days_ss 1); -\end{ttbox} -Note that usually it is not necessary to derive these inequalities explicitly -because the simplifier will dispose of them automatically. \subsection{Primitive recursive functions} \label{sec:HOL:primrec} @@ -1688,7 +1671,7 @@ as theorems from an explicit definition of the recursive function in terms of a recursion operator on the datatype. -The primitive recursive function can also use infix or mixfix syntax: +The primitive recursive function can have infix or mixfix syntax: \begin{ttbox} Append = MyList + consts "@" :: ['a list,'a list] => 'a list (infixr 60) @@ -1699,13 +1682,13 @@ \end{ttbox} The reduction rules become part of the ML structure \verb$Append$ and can -be used to prove theorems about the function: +be used to prove theorems about the function. The defining equations for +primitive recursive functions are automatically provided to the simplifier +(via the default simpset). \begin{ttbox} -val append_ss = HOL_ss addsimps [Append.app_Nil,Append.app_Cons]; - goal Append.thy "(xs @ ys) @ zs = xs @ (ys @ zs)"; by (MyList.list.induct_tac "xs" 1); -by (ALLGOALS(asm_simp_tac append_ss)); +by (ALLGOALS Asm_simp_tac); \end{ttbox} %Note that underdefined primitive recursive functions are allowed: diff -r 5d45c2094ff6 -r 82ec47e0a8d3 doc-src/Logics/ZF.tex --- a/doc-src/Logics/ZF.tex Wed Jan 08 15:12:44 1997 +0100 +++ b/doc-src/Logics/ZF.tex Wed Jan 08 15:17:25 1997 +0100 @@ -19,11 +19,13 @@ Thus, we may even regard set theory as a computational logic, loosely inspired by Martin-L\"of's Type Theory. -Because {\ZF} is an extension of {\FOL}, it provides the same packages, -namely {\tt hyp_subst_tac}, the simplifier, and the classical reasoner. -The main simplification set is called {\tt ZF_ss}. Several -classical rule sets are defined, including {\tt lemmas_cs}, -{\tt upair_cs} and~{\tt ZF_cs}. +Because {\ZF} is an extension of {\FOL}, it provides the same packages, namely +{\tt hyp_subst_tac}, the simplifier, and the classical reasoner. The default +simpset and claset are usually satisfactory. Named simpsets include +\ttindexbold{ZF_ss} (basic set theory rules) and \ttindexbold{rank_ss} (for +proving termination of well-founded recursion). Named clasets sets include +\ttindexbold{ZF_cs} (basic set theory) and \ttindexbold{le_cs} (useful for +reasoning about the relations $<$ and $\le$). {\tt ZF} has a flexible package for handling inductive definitions, such as inference systems, and datatype definitions, such as lists and @@ -1503,11 +1505,11 @@ 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 simplification set \ttindexbold{ZF_ss} contains congruence rules for +The default simplification set contains congruence rules for all the binding operators of {\ZF}\@. It contains all the conversion rules, such as {\tt fst} and {\tt snd}, as well as the rewrites -shown in Fig.\ts\ref{zf-simpdata}. - +shown in Fig.\ts\ref{zf-simpdata}. See the file +{\tt ZF/simpdata.ML} for a fuller list. \begin{figure} \begin{eqnarray*} @@ -1521,7 +1523,7 @@ (\forall x \in \emptyset. P(x)) & \bimp & \top\\ (\forall x \in A. \top) & \bimp & \top \end{eqnarray*} -\caption{Rewrite rules for set theory} \label{zf-simpdata} +\caption{Some rewrite rules for set theory} \label{zf-simpdata} \end{figure} @@ -1598,7 +1600,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 ZF.thy "Pow(A Int B) = Pow(A) Int Pow(B)"; +goal thy "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)} @@ -1687,7 +1689,7 @@ \end{ttbox} \medskip We could have performed this proof in one step by applying -\ttindex{fast_tac} with the classical rule set \ttindex{ZF_cs}. Let us +\ttindex{Fast_tac}. Let us go back to the start: \begin{ttbox} choplev 0; @@ -1695,11 +1697,11 @@ {\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} to {\tt ZF_cs} as an introduction rule. -Extensionality is not used by default because many equalities can be proved +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 (ZF_cs addIs [equalityI]) 1); +by (fast_tac (!claset addIs [equalityI]) 1); {\out Level 1} {\out Pow(A Int B) = Pow(A) Int Pow(B)} {\out No subgoals!} @@ -1713,7 +1715,7 @@ ${C\subseteq D}$ implies $\bigcup(C)\subseteq \bigcup(D)$. To begin, we tackle the inclusion using \tdx{subsetI}: \begin{ttbox} -val [prem] = goal ZF.thy "C<=D ==> Union(C) <= Union(D)"; +val [prem] = goal thy "C<=D ==> Union(C) <= Union(D)"; {\out Level 0} {\out Union(C) <= Union(D)} {\out 1. Union(C) <= Union(D)} @@ -1763,10 +1765,10 @@ {\out Union(C) <= Union(D)} {\out No subgoals!} \end{ttbox} -Again, \ttindex{fast_tac} with \ttindex{ZF_cs} can do this proof in one +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 \ttindex{ZF_cs} as an introduction rule. +\hbox{\tt prem RS subsetD} to the claset as an introduction rule. The file {\tt ZF/equalities.ML} has many similar proofs. Reasoning about general intersection can be difficult because of its anomalous behaviour on @@ -1790,7 +1792,7 @@ functions with disjoint domains~$A$ and~$C$, and if $a\in A$, then $(f\un g)`a = f`a$: \begin{ttbox} -val prems = goal ZF.thy +val prems = goal thy "[| a:A; f: A->B; g: C->D; A Int C = 0 |] ==> \ttback \ttback (f Un g)`a = f`a"; {\out Level 0} diff -r 5d45c2094ff6 -r 82ec47e0a8d3 doc-src/Logics/logics.bbl --- a/doc-src/Logics/logics.bbl Wed Jan 08 15:12:44 1997 +0100 +++ b/doc-src/Logics/logics.bbl Wed Jan 08 15:17:25 1997 +0100 @@ -165,9 +165,8 @@ \bibitem{paulson-CADE} Lawrence~C. Paulson. \newblock A fixedpoint approach to implementing (co)inductive definitions. -\newblock In Alan Bundy, editor, {\em Automated Deduction --- {CADE}-12}, LNAI - 814, pages 148--161. Springer, 1994. -\newblock 12th international conference. +\newblock In Alan Bundy, editor, {\em Automated Deduction --- {CADE}-12 + International Conference}, LNAI 814, pages 148--161. Springer, 1994. \bibitem{paulson-set-II} Lawrence~C. Paulson. @@ -177,7 +176,7 @@ \bibitem{paulson-coind} Lawrence~C. Paulson. \newblock Mechanizing coinduction and corecursion in higher-order logic. -\newblock {\em Journal of Logic and Computation}, 1996. +\newblock {\em Journal of Logic and Computation}, 7(2), March 1997. \newblock In press. \bibitem{paulson-COLOG}