1 theory Ind_General_Scheme

     2 imports Main

     3 begin

     4 

     5 section{* The General Construction Principle \label{sec:ind-general-method} *}

     6 

     7 text {*

     8   

     9   The point of these examples is to get a feeling what the automatic proofs 

    10   should do in order to solve all inductive definitions we throw at them. For this 

    11   it is instructive to look at the general construction principle 

    12   of inductive definitions, which we shall do in the next section.

    13 

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

    15   form of inductive definitions that our package should accept.

    16   Suppose $R_1,\ldots,R_n$ be mutually inductive predicates and $\vec{p}$ be

    17   some fixed parameters. Then the introduction rules for $R_1,\ldots,R_n$ may have

    18   the form

    19 

    20   \[

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

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

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

    24   \]

    25 

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

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

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

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

    30   that are closed under the introduction rules shown above. Then the definitions of the 

    31   inductive predicates $R_1,\ldots,R_n$ is:

    32 

    33   \[

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

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

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

    37   \mbox{where} \\

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

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

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

    41   \end{array}

    42   \]

    43 

    44   The induction principles for the inductive predicates $R_1,\ldots,R_n$ are

    45 

    46   \[

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

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

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

    50   \mbox{where} \\

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

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

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

    54   \end{array}

    55   \]

    56 

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

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

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

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

    61 

    62   \[

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

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

    65   \]

    66 

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

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

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

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

    71   as well as subgoals of the form

    72 

    73   \[

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

    75   \]

    76 

    77   that can be solved using the assumptions

    78 

    79   \[

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

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

    82   \]

    83 

    84   What remains is to implement these proofs generically.

    85 *}

    86 

    87 end