added smp_tac
Mon, 06 Sep 1999 18:17:48 +0200
changeset 7490 9a74b57740d1
parent 7489 77d654ea31a9
child 7491 95a4af0e10a7
added smp_tac
--- a/doc-src/HOL/HOL.tex	Mon Sep 06 17:03:19 1999 +0200
+++ b/doc-src/HOL/HOL.tex	Mon Sep 06 18:17:48 1999 +0200
@@ -10,7 +10,7 @@
 Church-style higher-order logic.  Experience with the {\sc hol} system
 has demonstrated that higher-order logic is widely applicable in many
 areas of mathematics and computer science, not just hardware
-verification, {\sc hol}'s original \textit{raison d'\^etre\/}.  It is
+verification, {\sc hol}'s original \textit{raison d'{\^e}tre\/}.  It is
 weaker than {\ZF} set theory but for most applications this does not
 matter.  If you prefer {\ML} to Lisp, you will probably prefer \HOL\ 
@@ -46,7 +46,7 @@
   \it name      &\it meta-type  & \it description \\
   \cdx{Trueprop}& $bool\To prop$                & coercion to $prop$\\
-  \cdx{Not}     & $bool\To bool$                & negation ($\neg$) \\
+  \cdx{Not}     & $bool\To bool$                & negation ($\lnot$) \\
   \cdx{True}    & $bool$                        & tautology ($\top$) \\
   \cdx{False}   & $bool$                        & absurdity ($\bot$) \\
   \cdx{If}      & $[bool,\alpha,\alpha]\To\alpha$ & conditional \\
@@ -132,13 +132,13 @@
 Figure~\ref{hol-constants} lists the constants (including infixes and
 binders), while Fig.\ts\ref{hol-grammar} presents the grammar of
 higher-order logic.  Note that $a$\verb|~=|$b$ is translated to
   \HOL\ has no if-and-only-if connective; logical equivalence is expressed
   using equality.  But equality has a high priority, as befitting a
   relation, while if-and-only-if typically has the lowest priority.  Thus,
-  $\neg\neg P=P$ abbreviates $\neg\neg (P=P)$ and not $(\neg\neg P)=P$.
+  $\lnot\lnot P=P$ abbreviates $\lnot\lnot (P=P)$ and not $(\lnot\lnot P)=P$.
   When using $=$ to mean logical equivalence, enclose both operands in
@@ -157,14 +157,14 @@
 \HOL\ offers various methods for introducing new types.
-See~\S\ref{sec:HOL:Types} and~\S\ref{sec:HOL:datatype}.
+See~{\S}\ref{sec:HOL:Types} and~{\S}\ref{sec:HOL:datatype}.
 Theory \thydx{Ord} defines the syntactic class \cldx{ord} of order
 signatures; the relations $<$ and $\leq$ are polymorphic over this
 class, as are the functions \cdx{mono}, \cdx{min} and \cdx{max}, and
 the \cdx{LEAST} operator. \thydx{Ord} also defines a subclass
 \cldx{order} of \cldx{ord} which axiomatizes partially ordered types
-(w.r.t.\ $\le$).
+(w.r.t.\ $\leq$).
 Three other syntactic type classes --- \cldx{plus}, \cldx{minus} and
 \cldx{times} --- permit overloading of the operators {\tt+},\index{*"+
@@ -175,10 +175,10 @@
 If you state a goal containing overloaded functions, you may need to include
 type constraints.  Type inference may otherwise make the goal more
 polymorphic than you intended, with confusing results.  For example, the
-variables $i$, $j$ and $k$ in the goal $i \le j \Imp i \le j+k$ have type
+variables $i$, $j$ and $k$ in the goal $i \leq j \Imp i \leq j+k$ have type
 $\alpha::\{ord,plus\}$, although you may have expected them to have some
 numeric type, e.g. $nat$.  Instead you should have stated the goal as
-$(i::nat) \le j \Imp i \le j+k$, which causes all three variables to have
+$(i::nat) \leq j \Imp i \leq j+k$, which causes all three variables to have
 type $nat$.
@@ -231,12 +231,12 @@
 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
-to be the least (w.r.t.\ $\le$) $x$ such that $P~x$ holds (see
+to be the least (w.r.t.\ $\leq$) $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
 nothing useful in case there is not a unique least element satisfying
 $P$.\footnote{Class $ord$ does not require much of its instances, so
-  $\le$ need not be a well-ordering, not even an order at all!}
+  $\leq$ need not be a well-ordering, not even an order at all!}
 \medskip All these binders have priority 10.
@@ -260,7 +260,7 @@
 logical meaning.  By declaring translations, you can cause instances of the
 \texttt{case} construct to denote applications of particular case operators.
 This is what happens automatically for each \texttt{datatype} definition
 Both \texttt{if} and \texttt{case} constructs have as low a priority as
@@ -335,7 +335,7 @@
 The definitions above should never be expanded and are shown for completeness
 only.  Instead users should reason in terms of the derived rules shown below
 or, better still, using high-level tactics
 Some of the rules mention type variables; for example, \texttt{refl}
@@ -441,7 +441,14 @@
   from subgoal $i$.
 \item[\ttindexbold{case_tac} {\tt"}$P${\tt"} $i$] performs case distinction
   on $P$ for subgoal $i$: the latter is replaced by two identical subgoals
-  with the added assumptions $P$ and $\neg P$, respectively.
+  with the added assumptions $P$ and $\lnot P$, respectively.
+\item[\ttindexbold{smp_tac} $j$ $i$] applies $j$ times \texttt{spec} and then
+  \texttt{mp} in subgoal $i$, which is typically useful when forward-chaining 
+  from an induction hypothesis. As a generalization of \texttt{mp_tac}, 
+  if there are assumptions $\forall \vec{x}. P \vec{x} \imp Q \vec{x}$ and 
+  $P \vec{a}$, ($\vec{x}$ being a vector of $j$ variables)
+  then it replaces the universally quantified implication by $Q \vec{a}$. 
+  It may instantiate unknowns. It fails if it can do nothing.
@@ -592,7 +599,7 @@
 constructs.  Infix operators include union and intersection ($A\un B$
 and $A\int B$), the subset and membership relations, and the image
 operator~{\tt``}\@.  Note that $a$\verb|~:|$b$ is translated to
-$\neg(a\in b)$.  
+$\lnot(a\in b)$.  
 The $\{a@1,\ldots\}$ notation abbreviates finite sets constructed in
 the obvious manner using~\texttt{insert} and~$\{\}$:
@@ -955,7 +962,7 @@
 expressed by the theorem \tdx{split_if}:
 \Var{P}(\mbox{\tt if}~\Var{b}~{\tt then}~\Var{x}~\mbox{\tt else}~\Var{y})~=~
-((\Var{b} \to \Var{P}(\Var{x})) \land (\neg \Var{b} \to \Var{P}(\Var{y})))
+((\Var{b} \to \Var{P}(\Var{x})) \land (\lnot \Var{b} \to \Var{P}(\Var{y})))
 For example, a simple instance of $(*)$ is
@@ -992,8 +999,8 @@
 where $c$ is a constant and $rhs$ is arbitrary. Note that $(*)$ is of the
 right form because internally the left-hand side is
 $\Var{P}(\mathtt{If}~\Var{b}~\Var{x}~~\Var{y})$. Important further examples
-are splitting rules for \texttt{case} expressions (see~\S\ref{subsec:list}
+are splitting rules for \texttt{case} expressions (see~{\S}\ref{subsec:list}
 Analogous to \texttt{Addsimps} and \texttt{Delsimps}, there are also
 imperative versions of \texttt{addsplits} and \texttt{delsplits}
@@ -1117,7 +1124,7 @@
 \beta$, $\alpha + \beta$, $nat$ and $\alpha \; list$) and ways for
 introducing new types in general.  The most important type
 construction, the \texttt{datatype}, is treated separately in
 \subsection{Product and sum types}\index{*"* type}\index{*"+ type}
@@ -1225,7 +1232,7 @@
 shown.  The constructions are fairly standard and can be found in the
 respective theory files. Although the sum and product types are
 constructed manually for foundational reasons, they are represented as
-actual datatypes later (see \S\ref{subsec:datatype:rep_datatype}).
+actual datatypes later (see {\S}\ref{subsec:datatype:rep_datatype}).
 Therefore, the theory \texttt{Datatype} should be used instead of
 \texttt{Sum} or \texttt{Prod}.
@@ -1335,7 +1342,7 @@
 \texttt{nat} are part of the default simpset.
 Functions on \tydx{nat} can be defined by primitive or well-founded recursion;
-see \S\ref{sec:HOL:recursive}.  A simple example is addition.
+see {\S}\ref{sec:HOL:recursive}.  A simple example is addition.
 Here, \texttt{op +} is the name of the infix operator~\texttt{+}, following
 the standard convention.
@@ -1352,7 +1359,7 @@
 the order of the two cases.
 Both \texttt{primrec} and \texttt{case} are realized by a recursion operator
 \cdx{nat_rec}, which is available because \textit{nat} is represented as
-a datatype (see \S\ref{subsec:datatype:rep_datatype}).
+a datatype (see {\S}\ref{subsec:datatype:rep_datatype}).
 %The predecessor relation, \cdx{pred_nat}, is shown to be well-founded.
 %Recursion along this relation resembles primitive recursion, but is
@@ -1513,7 +1520,7 @@
 case $e$ of [] => $a$  |  \(x\)\#\(xs\) => b
-is defined by translation.  For details see~\S\ref{sec:HOL:datatype}. There
+is defined by translation.  For details see~{\S}\ref{sec:HOL:datatype}. There
 is also a case splitting rule \tdx{split_list_case}
@@ -1524,10 +1531,10 @@
 which can be fed to \ttindex{addsplits} just like
-\texttt{split_if} (see~\S\ref{subsec:HOL:case:splitting}).
+\texttt{split_if} (see~{\S}\ref{subsec:HOL:case:splitting}).
 \texttt{List} provides a basic library of list processing functions defined by
-primitive recursion (see~\S\ref{sec:HOL:primrec}).  The recursion equations
+primitive recursion (see~{\S}\ref{sec:HOL:primrec}).  The recursion equations
 are shown in Fig.\ts\ref{fig:HOL:list-simps}.
 \index{list@{\textit{list}} type|)}
@@ -1543,7 +1550,7 @@
   Types in \HOL\ must be non-empty; otherwise the quantifier rules would be
-  unsound, because $\exists x. x=x$ is a theorem \cite[\S7]{paulson-COLOG}.
+  unsound, because $\exists x. x=x$ is a theorem \cite[{\S}7]{paulson-COLOG}.
 A \bfindex{type definition} identifies the new type with a subset of
 an existing type.  More precisely, the new type is defined by
@@ -1699,11 +1706,11 @@
 In Isabelle/HOL record types have to be defined explicitly, fixing their field
 names and types, and their (optional) parent record (see
-\S\ref{sec:HOL:record-def}).  Afterwards, records may be formed using above
+{\S}\ref{sec:HOL:record-def}).  Afterwards, records may be formed using above
 syntax, while obeying the canonical order of fields as given by their
 declaration.  The record package also provides several operations like
-selectors and updates (see \S\ref{sec:HOL:record-ops}), together with
-characteristic properties (see \S\ref{sec:HOL:record-thms}).
+selectors and updates (see {\S}\ref{sec:HOL:record-ops}), together with
+characteristic properties (see {\S}\ref{sec:HOL:record-thms}).
 There is an example theory demonstrating most basic aspects of extensible
 records (see theory \texttt{HOL/ex/Points} in the Isabelle sources).
@@ -1891,7 +1898,7 @@
 Inductive datatypes, similar to those of \ML, frequently appear in
 applications of Isabelle/HOL.  In principle, such types could be defined by
-hand via \texttt{typedef} (see \S\ref{sec:typedef}), but this would be far too
+hand via \texttt{typedef} (see {\S}\ref{sec:typedef}), but this would be far too
 tedious.  The \ttindex{datatype} definition package of Isabelle/HOL (cf.\ 
 \cite{Berghofer-Wenzel:1999:TPHOL}) automates such chores.  It generates an
 appropriate \texttt{typedef} based on a least fixed-point construction, and
@@ -1931,7 +1938,7 @@
 \item $\tau = (\tau'@1,\ldots,\tau'@{h'})t'$, where $t'$ is
 the type constructor of an already existing datatype and $\tau'@1,\ldots,\tau'@{h'}$
 are admissible types.
-\item $\tau = \sigma \rightarrow \tau'$, where $\tau'$ is an admissible
+\item $\tau = \sigma \to \tau'$, where $\tau'$ is an admissible
 type and $\sigma$ is non-recursive (i.e. the occurrences of the newly defined
 types are {\em strictly positive})
@@ -1972,7 +1979,7 @@
 Types in HOL must be non-empty. Each of the new datatypes
-$(\alpha@1,\ldots,\alpha@h)t@j$ with $1 \le j \le n$ is non-empty iff it has a
+$(\alpha@1,\ldots,\alpha@h)t@j$ with $1 \leq j \leq n$ is non-empty iff it has a
 constructor $C^j@i$ with the following property: for all argument types
 $\tau^j@{i,i'}$ of the form $(\alpha@1,\ldots,\alpha@h)t@{j'}$ the datatype
 $(\alpha@1,\ldots,\alpha@h)t@{j'}$ is non-empty.
@@ -2014,7 +2021,7 @@
 The datatype package also provides structural induction rules.  For
 datatypes without nested recursion, this is of the following form:
-\infer{P@1~x@1 \wedge \dots \wedge P@n~x@n}
+\infer{P@1~x@1 \land \dots \land P@n~x@n}
      \Forall x@1 \dots x@{m^1@1}.
        \List{P@{s^1@{1,1}}~x@{r^1@{1,1}}; \dots;
@@ -2044,7 +2051,7 @@
      \left(r^j@{i,l^j@i},s^j@{i,l^j@i}\right)\right\} = \\[2ex]
 && \left\{(i',i'')~\left|~
-     1\leq i' \leq m^j@i \wedge 1 \leq i'' \leq n \wedge
+     1\leq i' \leq m^j@i \land 1 \leq i'' \leq n \land
        \tau^j@{i,i'} = (\alpha@1,\ldots,\alpha@h)t@{i''}\right.\right\}
@@ -2070,7 +2077,7 @@
 constructors \texttt{Nil} and \texttt{Cons}. Thus, the structural induction rule for
 \texttt{term} gets the form
-\infer{P@1~x@1 \wedge P@2~x@2}
+\infer{P@1~x@1 \land P@2~x@2}
      \Forall x.~P@1~(\mathtt{Var}~x) \\
      \Forall x@1~x@2.~P@2~x@2 \Imp P@1~(\mathtt{App}~x@1~x@2) \\
@@ -2105,7 +2112,7 @@
 where the $x@{i,j}$ are either identifiers or nested tuple patterns as in
   All constructors must be present, their order is fixed, and nested patterns
   are not supported (with the exception of tuples).  Violating this
@@ -2126,7 +2133,7 @@
 where $t@j$\texttt{_case} is the internal name of the \texttt{case}-construct.
 This theorem can be added to a simpset via \ttindex{addsplits}
 \subsubsection{The function \cdx{size}}\label{sec:HOL:size}
@@ -2456,7 +2463,7 @@
 \subsubsection{Example: Evaluation of expressions}
 Using mutual primitive recursion, we can define evaluation functions \texttt{evala}
 and \texttt{eval_bexp} for the datatypes of arithmetic and boolean expressions mentioned in
   evala :: "['a => nat, 'a aexp] => nat"
@@ -2516,7 +2523,7 @@
 \subsubsection{Example: A substitution function for terms}
 Functions on datatypes with nested recursion, such as the type
-\texttt{term} mentioned in \S\ref{subsec:datatype:basics}, are
+\texttt{term} mentioned in {\S}\ref{subsec:datatype:basics}, are
 also defined by mutual primitive recursion. A substitution
 function \texttt{subst_term} on type \texttt{term}, similar to the functions
 \texttt{substa} and \texttt{substb} described above, can
@@ -2536,7 +2543,7 @@
      subst_term f t # subst_term_list f ts"
 The recursion scheme follows the structure of the unfolded definition of type
-\texttt{term} shown in \S\ref{subsec:datatype:basics}. To prove properties of
+\texttt{term} shown in {\S}\ref{subsec:datatype:basics}. To prove properties of
 this substitution function, mutual induction is needed:
@@ -2625,7 +2632,7 @@
   Typically, $f$ takes the recursive function's arguments (as a tuple) and
   returns a result expressed in terms of the function \texttt{size}.  It is
   called a \textbf{measure function}.  Recall that \texttt{size} is overloaded
-  and is defined on all datatypes (see \S\ref{sec:HOL:size}).
+  and is defined on all datatypes (see {\S}\ref{sec:HOL:size}).
 \item $\mathop{\mathtt{inv_image}} f\;R$ is a generalisation of
   \texttt{measure}.  It specifies a relation such that $x\prec y$ iff $f(x)$
@@ -2989,7 +2996,7 @@
   procedure.  These are mostly taken from Pelletier \cite{pelletier86}.
 \item File \texttt{set.ML} proves Cantor's Theorem, which is presented in
-  \S\ref{sec:hol-cantor} below, and the Schr\"oder-Bernstein Theorem.
+  {\S}\ref{sec:hol-cantor} below, and the Schr{\"o}der-Bernstein Theorem.
 \item Theory \texttt{MT} contains Jacob Frost's formalization~\cite{frost93} of
   Milner and Tofte's coinduction example~\cite{milner-coind}.  This
--- a/src/HOL/HOL_lemmas.ML	Mon Sep 06 17:03:19 1999 +0200
+++ b/src/HOL/HOL_lemmas.ML	Mon Sep 06 18:17:48 1999 +0200
@@ -424,9 +424,22 @@
   in  CHANGED_GOAL (rtac (th' RS ssubst))
+(* combination of (spec RS spec RS ...(j times) ... spec RS mp *) 
+  fun wrong_prem (Const ("All", _) $ (Abs (_, _, t))) = wrong_prem t
+  |   wrong_prem (Bound _) = true
+  |   wrong_prem _ = false;
+  fun wrong (Const ("==>", _) $ (Const ("Trueprop", _) $ t) $ _) = wrong_prem t
+  |   wrong _ = true;
+  val filter_right = filter (fn t => not (wrong (#prop (rep_thm t))));
+  fun smp i = funpow i (fn m => filter_right ([spec] RL m)) ([mp]);
+  fun smp_tac j = EVERY'[dresolve_tac (smp j), atac]
 fun strip_tac i = REPEAT(resolve_tac [impI,allI] i); 
 (** strip ! and --> from proved goal while preserving !-bound var names **)