--- a/CookBook/Package/Ind_General_Scheme.thy	Wed Jan 28 06:43:51 2009 +0000
+++ b/CookBook/Package/Ind_General_Scheme.thy	Thu Jan 29 09:46:17 2009 +0000
@@ -2,70 +2,81 @@
 imports Main
 begin
 
-section{* The general construction principle *}
+section{* The General Construction Principle \label{sec:ind-general-method} *}
 
 text {*
-\label{sec:ind-general-method}
-Before we start with the implementation, it is useful to describe the general
-form of inductive definitions that our package should accept. We closely follow
-the notation for inductive definitions introduced by Schwichtenberg
-\cite{Schwichtenberg-MLCF} for the Minlog system.
-Let $R_1,\ldots,R_n$ be mutually inductive predicates and $\vec{p}$ be
-parameters. Then the introduction rules for $R_1,\ldots,R_n$ may have
-the form
-\[
-\bigwedge\vec{x}_i.~\vec{A}_i \Longrightarrow \left(\bigwedge\vec{y}_{ij}.~\vec{B}_{ij} \Longrightarrow
+
+  Before we start with the implementation, it is useful to describe the general
+  form of inductive definitions that our package should accept. We closely follow
+  the notation for inductive definitions introduced by Schwichtenberg
+  \cite{Schwichtenberg-MLCF} for the Minlog system.
+  Let $R_1,\ldots,R_n$ be mutually inductive predicates and $\vec{p}$ be
+  parameters. Then the introduction rules for $R_1,\ldots,R_n$ may have
+  the form
+
+  \[
+  \bigwedge\vec{x}_i.~\vec{A}_i \Longrightarrow \left(\bigwedge\vec{y}_{ij}.~\vec{B}_{ij} \Longrightarrow
   R_{k_{ij}}~\vec{p}~\vec{s}_{ij}\right)_{j=1,\ldots,m_i} \Longrightarrow R_{l_i}~\vec{p}~\vec{t}_i
-\qquad \mbox{for\ } i=1,\ldots,r
-\]
-where $\vec{A}_i$ and $\vec{B}_{ij}$ are formulae not containing $R_1,\ldots,R_n$.
-Note that by disallowing the inductive predicates to occur in $\vec{B}_{ij}$ we make sure
-that all occurrences of the predicates in the premises of the introduction rules are
-\emph{strictly positive}. This condition guarantees the existence of predicates
-that are closed under the introduction rules shown above. The inductive predicates
-$R_1,\ldots,R_n$ can then be defined as follows:
-\[
-\begin{array}{l@ {\qquad}l}
+  \qquad \mbox{for\ } i=1,\ldots,r
+  \]
+
+  where $\vec{A}_i$ and $\vec{B}_{ij}$ are formulae not containing $R_1,\ldots,R_n$.
+  Note that by disallowing the inductive predicates to occur in $\vec{B}_{ij}$ we make sure
+  that all occurrences of the predicates in the premises of the introduction rules are
+  \emph{strictly positive}. This condition guarantees the existence of predicates
+  that are closed under the introduction rules shown above. The inductive predicates
+  $R_1,\ldots,R_n$ can then be defined as follows:
+
+  \[
+  \begin{array}{l@ {\qquad}l}
   R_i \equiv \lambda\vec{p}~\vec{z}_i.~\forall P_1 \ldots P_n.~K_1 \longrightarrow \cdots \longrightarrow K_r \longrightarrow P_i~\vec{z}_i &
   \mbox{for\ } i=1,\ldots,n \\[1.5ex]
   \mbox{where} \\
   K_i \equiv \forall\vec{x}_i.~\vec{A}_i \longrightarrow \left(\forall\vec{y}_{ij}.~\vec{B}_{ij} \longrightarrow
-    P_{k_{ij}}~\vec{s}_{ij}\right)_{j=1,\ldots,m_i} \longrightarrow P_{l_i}~\vec{t}_i &
+  P_{k_{ij}}~\vec{s}_{ij}\right)_{j=1,\ldots,m_i} \longrightarrow P_{l_i}~\vec{t}_i &
   \mbox{for\ } i=1,\ldots,r
-\end{array}
-\]
-The (weak) induction rules for the inductive predicates $R_1,\ldots,R_n$ are
-\[
-\begin{array}{l@ {\qquad}l}
+  \end{array}
+  \]
+
+  The (weak) induction rules for the inductive predicates $R_1,\ldots,R_n$ are
+
+  \[
+  \begin{array}{l@ {\qquad}l}
   R_i~\vec{p}~\vec{z}_i \Longrightarrow I_1 \Longrightarrow \cdots \Longrightarrow I_r \Longrightarrow P_i~\vec{z}_i &
   \mbox{for\ } i=1,\ldots,n \\[1.5ex]
   \mbox{where} \\
   I_i \equiv \bigwedge\vec{x}_i.~\vec{A}_i \Longrightarrow \left(\bigwedge\vec{y}_{ij}.~\vec{B}_{ij} \Longrightarrow
-    P_{k_{ij}}~\vec{s}_{ij}\right)_{j=1,\ldots,m_i} \Longrightarrow P_{l_i}~\vec{t}_i &
+  P_{k_{ij}}~\vec{s}_{ij}\right)_{j=1,\ldots,m_i} \Longrightarrow P_{l_i}~\vec{t}_i &
   \mbox{for\ } i=1,\ldots,r
-\end{array}
-\]
-Since $K_i$ and $I_i$ are equivalent modulo conversion between meta-level and object-level
-connectives, it is clear that the proof of the induction theorem is straightforward. We will
-therefore focus on the proof of the introduction rules. When proving the introduction rule
-shown above, we start by unfolding the definition of $R_1,\ldots,R_n$, which yields
-\[
-\bigwedge\vec{x}_i.~\vec{A}_i \Longrightarrow \left(\bigwedge\vec{y}_{ij}.~\vec{B}_{ij} \Longrightarrow
+  \end{array}
+  \]
+
+  Since $K_i$ and $I_i$ are equivalent modulo conversion between meta-level and object-level
+  connectives, it is clear that the proof of the induction theorem is straightforward. We will
+  therefore focus on the proof of the introduction rules. When proving the introduction rule
+  shown above, we start by unfolding the definition of $R_1,\ldots,R_n$, which yields
+
+  \[
+  \bigwedge\vec{x}_i.~\vec{A}_i \Longrightarrow \left(\bigwedge\vec{y}_{ij}.~\vec{B}_{ij} \Longrightarrow
   \forall P_1 \ldots P_n.~\vec{K} \longrightarrow P_{k_{ij}}~\vec{s}_{ij}\right)_{j=1,\ldots,m_i} \Longrightarrow \forall P_1 \ldots P_n.~\vec{K} \longrightarrow P_{l_i}~\vec{t}_i
-\]
-where $\vec{K}$ abbreviates $K_1,\ldots,K_r$. Applying the introduction rules for
-$\forall$ and $\longrightarrow$ yields a proof state in which we have to prove $P_{l_i}~\vec{t}_i$
-from the additional assumptions $\vec{K}$. When using $K_{l_i}$ (converted to meta-logic format)
-to prove $P_{l_i}~\vec{t}_i$, we get subgoals $\vec{A}_i$ that are trivially solvable by assumption,
-as well as subgoals of the form
-\[
-\bigwedge\vec{y}_{ij}.~\vec{B}_{ij} \Longrightarrow P_{k_{ij}}~\vec{s}_{ij} \qquad \mbox{for\ } j=1,\ldots,m_i
-\]
-that can be solved using the assumptions
-\[
-\bigwedge\vec{y}_{ij}.~\vec{B}_{ij} \Longrightarrow
+  \]
+
+  where $\vec{K}$ abbreviates $K_1,\ldots,K_r$. Applying the introduction rules for
+  $\forall$ and $\longrightarrow$ yields a proof state in which we have to prove $P_{l_i}~\vec{t}_i$
+  from the additional assumptions $\vec{K}$. When using $K_{l_i}$ (converted to meta-logic format)
+  to prove $P_{l_i}~\vec{t}_i$, we get subgoals $\vec{A}_i$ that are trivially solvable by assumption,
+  as well as subgoals of the form
+
+  \[
+  \bigwedge\vec{y}_{ij}.~\vec{B}_{ij} \Longrightarrow P_{k_{ij}}~\vec{s}_{ij} \qquad \mbox{for\ } j=1,\ldots,m_i
+  \]
+
+  that can be solved using the assumptions
+
+  \[
+  \bigwedge\vec{y}_{ij}.~\vec{B}_{ij} \Longrightarrow
   \forall P_1 \ldots P_n.~\vec{K} \longrightarrow P_{k_{ij}}~\vec{s}_{ij} \qquad \mbox{and} \qquad \vec{K}
-\]
+  \]
 *}
 
 end