theory Ind_General_Scheme

imports Main

begin

section{* The general construction principle *}

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

  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}

  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 &

  \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}

  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 &

  \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

  \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

  \forall P_1 \ldots P_n.~\vec{K} \longrightarrow P_{k_{ij}}~\vec{s}_{ij} \qquad \mbox{and} \qquad \vec{K}

\]

*}

end