- Documented monotonicity theorems.
- Tuned accessible part example.
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