theory Ind_General_Scheme+
−
imports Main+
−
begin+
−
+
−
section{* The General Construction Principle \label{sec:ind-general-method} *}+
−
+
−
text {*+
−
  +
−
  The point of these examples is to get a feeling what the automatic proofs +
−
  should do in order to solve all inductive definitions we throw at them. For this +
−
  it is instructive to look at the general construction principle +
−
  of inductive definitions, which we shall do in the next section.+
−
+
−
  Before we start with the implementation, it is useful to describe the general+
−
  form of inductive definitions that our package should accept.+
−
  Suppose $R_1,\ldots,R_n$ be mutually inductive predicates and $\vec{p}$ be+
−
  some fixed 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. Then the definitions of the +
−
  inductive predicates $R_1,\ldots,R_n$ is:+
−
+
−
  \[+
−
  \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 induction principles 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 goal 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 the 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}+
−
  \]+
−
+
−
  What remains is to implement these proofs generically.+
−
*}+
−
+
−
end+
−