1 theory Ind_General_Scheme

     2 imports Main

     3 begin

     4 

     5 section{* The general construction principle *}

     6 

     7 text {*

     8 \label{sec:ind-general-method}

     9 Before we start with the implementation, it is useful to describe the general

    10 form of inductive definitions that our package should accept. We closely follow

    11 the notation for inductive definitions introduced by Schwichtenberg

    12 \cite{Schwichtenberg-MLCF} for the Minlog system.

    13 Let $R_1,\ldots,R_n$ be mutually inductive predicates and $\vec{p}$ be

    14 parameters. Then the introduction rules for $R_1,\ldots,R_n$ may have

    15 the form

    16 \[

    17 \bigwedge\vec{x}_i.~\vec{A}_i \Longrightarrow \left(\bigwedge\vec{y}_{ij}.~\vec{B}_{ij} \Longrightarrow

    18   R_{k_{ij}}~\vec{p}~\vec{s}_{ij}\right)_{j=1,\ldots,m_i} \Longrightarrow R_{l_i}~\vec{p}~\vec{t}_i

    19 \qquad \mbox{for\ } i=1,\ldots,r

    20 \]

    21 where $\vec{A}_i$ and $\vec{B}_{ij}$ are formulae not containing $R_1,\ldots,R_n$.

    22 Note that by disallowing the inductive predicates to occur in $\vec{B}_{ij}$ we make sure

    23 that all occurrences of the predicates in the premises of the introduction rules are

    24 \emph{strictly positive}. This condition guarantees the existence of predicates

    25 that are closed under the introduction rules shown above. The inductive predicates

    26 $R_1,\ldots,R_n$ can then be defined as follows:

    27 \[

    28 \begin{array}{l@ {\qquad}l}

    29   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 &

    30   \mbox{for\ } i=1,\ldots,n \\[1.5ex]

    31   \mbox{where} \\

    32   K_i \equiv \forall\vec{x}_i.~\vec{A}_i \longrightarrow \left(\forall\vec{y}_{ij}.~\vec{B}_{ij} \longrightarrow

    33     P_{k_{ij}}~\vec{s}_{ij}\right)_{j=1,\ldots,m_i} \longrightarrow P_{l_i}~\vec{t}_i &

    34   \mbox{for\ } i=1,\ldots,r

    35 \end{array}

    36 \]

    37 The (weak) induction rules for the inductive predicates $R_1,\ldots,R_n$ are

    38 \[

    39 \begin{array}{l@ {\qquad}l}

    40   R_i~\vec{p}~\vec{z}_i \Longrightarrow I_1 \Longrightarrow \cdots \Longrightarrow I_r \Longrightarrow P_i~\vec{z}_i &

    41   \mbox{for\ } i=1,\ldots,n \\[1.5ex]

    42   \mbox{where} \\

    43   I_i \equiv \bigwedge\vec{x}_i.~\vec{A}_i \Longrightarrow \left(\bigwedge\vec{y}_{ij}.~\vec{B}_{ij} \Longrightarrow

    44     P_{k_{ij}}~\vec{s}_{ij}\right)_{j=1,\ldots,m_i} \Longrightarrow P_{l_i}~\vec{t}_i &

    45   \mbox{for\ } i=1,\ldots,r

    46 \end{array}

    47 \]

    48 Since $K_i$ and $I_i$ are equivalent modulo conversion between meta-level and object-level

    49 connectives, it is clear that the proof of the induction theorem is straightforward. We will

    50 therefore focus on the proof of the introduction rules. When proving the introduction rule

    51 shown above, we start by unfolding the definition of $R_1,\ldots,R_n$, which yields

    52 \[

    53 \bigwedge\vec{x}_i.~\vec{A}_i \Longrightarrow \left(\bigwedge\vec{y}_{ij}.~\vec{B}_{ij} \Longrightarrow

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

    55 \]

    56 where $\vec{K}$ abbreviates $K_1,\ldots,K_r$. Applying the introduction rules for

    57 $\forall$ and $\longrightarrow$ yields a proof state in which we have to prove $P_{l_i}~\vec{t}_i$

    58 from the additional assumptions $\vec{K}$. When using $K_{l_i}$ (converted to meta-logic format)

    59 to prove $P_{l_i}~\vec{t}_i$, we get subgoals $\vec{A}_i$ that are trivially solvable by assumption,

    60 as well as subgoals of the form

    61 \[

    62 \bigwedge\vec{y}_{ij}.~\vec{B}_{ij} \Longrightarrow P_{k_{ij}}~\vec{s}_{ij} \qquad \mbox{for\ } j=1,\ldots,m_i

    63 \]

    64 that can be solved using the assumptions

    65 \[

    66 \bigwedge\vec{y}_{ij}.~\vec{B}_{ij} \Longrightarrow

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

    68 \]

    69 *}

    70 

    71 end