1.1 --- a/doc-src/HOL/HOL.tex	Mon Oct 11 11:15:31 1999 +0200
     1.2 +++ b/doc-src/HOL/HOL.tex	Mon Oct 11 16:07:35 1999 +0200
     1.3 @@ -2856,6 +2856,37 @@
     1.4  \end{itemize}
     1.5  
     1.6  
     1.7 +\subsection{*Monotonicity theorems}
     1.8 +
     1.9 +Each theory contains a default set of theorems that are used in monotonicity
    1.10 +proofs. New rules can be added to this set via the \texttt{mono} attribute.
    1.11 +Theory \texttt{Inductive} shows how this is done. In general, the following
    1.12 +monotonicity theorems may be added:
    1.13 +\begin{itemize}
    1.14 +\item Theorems of the form $A\subseteq B\Imp M(A)\subseteq M(B)$, for proving
    1.15 +  monotonicity of inductive definitions whose introduction rules have premises
    1.16 +  involving terms such as $t\in M(R@i)$.
    1.17 +\item Monotonicity theorems for logical operators, which are of the general form
    1.18 +  $\List{\cdots \rightarrow \cdots;~\ldots;~\cdots \rightarrow \cdots} \Imp
    1.19 +    \cdots \rightarrow \cdots$.
    1.20 +  For example, in the case of the operator $\vee$, the corresponding theorem is
    1.21 +  \[
    1.22 +  \infer{P@1 \vee P@2 \rightarrow Q@1 \vee Q@2}
    1.23 +    {P@1 \rightarrow Q@1 & P@2 \rightarrow Q@2}
    1.24 +  \]
    1.25 +\item De Morgan style equations for reasoning about the ``polarity'' of expressions, e.g.
    1.26 +  \[
    1.27 +  (\neg \neg P) ~=~ P \qquad\qquad
    1.28 +  (\neg (P \wedge Q)) ~=~ (\neg P \vee \neg Q)
    1.29 +  \]
    1.30 +\item Equations for reducing complex operators to more primitive ones whose
    1.31 +  monotonicity can easily be proved, e.g.
    1.32 +  \[
    1.33 +  (P \rightarrow Q) ~=~ (\neg P \vee Q) \qquad\qquad
    1.34 +  \mathtt{Ball}~A~P ~\equiv~ \forall x.~x \in A \rightarrow P~x
    1.35 +  \]
    1.36 +\end{itemize}
    1.37 +
    1.38  \subsection{Example of an inductive definition}
    1.39  Two declarations, included in a theory file, define the finite powerset
    1.40  operator.  First we declare the constant~\texttt{Fin}.  Then we declare it
    1.41 @@ -2873,20 +2904,18 @@
    1.42  rule is \texttt{Fin.induct}.
    1.43  
    1.44  For another example, here is a theory file defining the accessible
    1.45 -part of a relation.  The main thing to note is the use of~\texttt{Pow} in
    1.46 -the sole introduction rule, and the corresponding mention of the rule
    1.47 -\verb|Pow_mono| in the \texttt{monos} list.  The paper
    1.48 +part of a relation.  The paper
    1.49  \cite{paulson-CADE} discusses a \ZF\ version of this example in more
    1.50  detail.
    1.51  \begin{ttbox}
    1.52 -Acc = WF + 
    1.53 -consts pred :: "['b, ('a * 'b)set] => 'a set"   (*Set of predecessors*)
    1.54 -       acc  :: "('a * 'a)set => 'a set"         (*Accessible part*)
    1.55 -defs   pred_def  "pred x r == {y. (y,x):r}"
    1.56 +Acc = WF + Inductive +
    1.57 +
    1.58 +consts acc :: "('a * 'a)set => 'a set"   (* accessible part *)
    1.59 +
    1.60  inductive "acc r"
    1.61    intrs
    1.62 -     pred "pred a r: Pow(acc r) ==> a: acc r"
    1.63 -  monos   Pow_mono
    1.64 +    accI "ALL y. (y, x) : r --> y : acc r ==> x : acc r"
    1.65 +
    1.66  end
    1.67  \end{ttbox}
    1.68  The Isabelle distribution contains many other inductive definitions.  Simple