1 theory Ind_General_Scheme |
1 theory Ind_General_Scheme |
2 imports Main |
2 imports Main |
3 begin |
3 begin |
4 |
4 |
5 section{* The general construction principle *} |
5 section{* The General Construction Principle \label{sec:ind-general-method} *} |
6 |
6 |
7 text {* |
7 text {* |
8 \label{sec:ind-general-method} |
8 |
9 Before we start with the implementation, it is useful to describe the general |
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 |
10 form of inductive definitions that our package should accept. We closely follow |
11 the notation for inductive definitions introduced by Schwichtenberg |
11 the notation for inductive definitions introduced by Schwichtenberg |
12 \cite{Schwichtenberg-MLCF} for the Minlog system. |
12 \cite{Schwichtenberg-MLCF} for the Minlog system. |
13 Let $R_1,\ldots,R_n$ be mutually inductive predicates and $\vec{p}$ be |
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 |
14 parameters. Then the introduction rules for $R_1,\ldots,R_n$ may have |
15 the form |
15 the form |
16 \[ |
16 |
17 \bigwedge\vec{x}_i.~\vec{A}_i \Longrightarrow \left(\bigwedge\vec{y}_{ij}.~\vec{B}_{ij} \Longrightarrow |
17 \[ |
|
18 \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 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 \qquad \mbox{for\ } i=1,\ldots,r |
20 \] |
21 \] |
21 where $\vec{A}_i$ and $\vec{B}_{ij}$ are formulae not containing $R_1,\ldots,R_n$. |
22 |
22 Note that by disallowing the inductive predicates to occur in $\vec{B}_{ij}$ we make sure |
23 where $\vec{A}_i$ and $\vec{B}_{ij}$ are formulae not containing $R_1,\ldots,R_n$. |
23 that all occurrences of the predicates in the premises of the introduction rules are |
24 Note that by disallowing the inductive predicates to occur in $\vec{B}_{ij}$ we make sure |
24 \emph{strictly positive}. This condition guarantees the existence of predicates |
25 that all occurrences of the predicates in the premises of the introduction rules are |
25 that are closed under the introduction rules shown above. The inductive predicates |
26 \emph{strictly positive}. This condition guarantees the existence of predicates |
26 $R_1,\ldots,R_n$ can then be defined as follows: |
27 that are closed under the introduction rules shown above. The inductive predicates |
27 \[ |
28 $R_1,\ldots,R_n$ can then be defined as follows: |
28 \begin{array}{l@ {\qquad}l} |
29 |
|
30 \[ |
|
31 \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 & |
32 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] |
33 \mbox{for\ } i=1,\ldots,n \\[1.5ex] |
31 \mbox{where} \\ |
34 \mbox{where} \\ |
32 K_i \equiv \forall\vec{x}_i.~\vec{A}_i \longrightarrow \left(\forall\vec{y}_{ij}.~\vec{B}_{ij} \longrightarrow |
35 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 & |
36 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 |
37 \mbox{for\ } i=1,\ldots,r |
35 \end{array} |
38 \end{array} |
36 \] |
39 \] |
37 The (weak) induction rules for the inductive predicates $R_1,\ldots,R_n$ are |
40 |
38 \[ |
41 The (weak) induction rules for the inductive predicates $R_1,\ldots,R_n$ are |
39 \begin{array}{l@ {\qquad}l} |
42 |
|
43 \[ |
|
44 \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 & |
45 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] |
46 \mbox{for\ } i=1,\ldots,n \\[1.5ex] |
42 \mbox{where} \\ |
47 \mbox{where} \\ |
43 I_i \equiv \bigwedge\vec{x}_i.~\vec{A}_i \Longrightarrow \left(\bigwedge\vec{y}_{ij}.~\vec{B}_{ij} \Longrightarrow |
48 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 & |
49 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 |
50 \mbox{for\ } i=1,\ldots,r |
46 \end{array} |
51 \end{array} |
47 \] |
52 \] |
48 Since $K_i$ and $I_i$ are equivalent modulo conversion between meta-level and object-level |
53 |
49 connectives, it is clear that the proof of the induction theorem is straightforward. We will |
54 Since $K_i$ and $I_i$ are equivalent modulo conversion between meta-level and object-level |
50 therefore focus on the proof of the introduction rules. When proving the introduction rule |
55 connectives, it is clear that the proof of the induction theorem is straightforward. We will |
51 shown above, we start by unfolding the definition of $R_1,\ldots,R_n$, which yields |
56 therefore focus on the proof of the introduction rules. When proving the introduction rule |
52 \[ |
57 shown above, we start by unfolding the definition of $R_1,\ldots,R_n$, which yields |
53 \bigwedge\vec{x}_i.~\vec{A}_i \Longrightarrow \left(\bigwedge\vec{y}_{ij}.~\vec{B}_{ij} \Longrightarrow |
58 |
|
59 \[ |
|
60 \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 |
61 \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 \] |
62 \] |
56 where $\vec{K}$ abbreviates $K_1,\ldots,K_r$. Applying the introduction rules for |
63 |
57 $\forall$ and $\longrightarrow$ yields a proof state in which we have to prove $P_{l_i}~\vec{t}_i$ |
64 where $\vec{K}$ abbreviates $K_1,\ldots,K_r$. Applying the introduction rules for |
58 from the additional assumptions $\vec{K}$. When using $K_{l_i}$ (converted to meta-logic format) |
65 $\forall$ and $\longrightarrow$ yields a proof state in which we have to prove $P_{l_i}~\vec{t}_i$ |
59 to prove $P_{l_i}~\vec{t}_i$, we get subgoals $\vec{A}_i$ that are trivially solvable by assumption, |
66 from the additional assumptions $\vec{K}$. When using $K_{l_i}$ (converted to meta-logic format) |
60 as well as subgoals of the form |
67 to prove $P_{l_i}~\vec{t}_i$, we get subgoals $\vec{A}_i$ that are trivially solvable by assumption, |
61 \[ |
68 as well as subgoals of the form |
62 \bigwedge\vec{y}_{ij}.~\vec{B}_{ij} \Longrightarrow P_{k_{ij}}~\vec{s}_{ij} \qquad \mbox{for\ } j=1,\ldots,m_i |
69 |
63 \] |
70 \[ |
64 that can be solved using the assumptions |
71 \bigwedge\vec{y}_{ij}.~\vec{B}_{ij} \Longrightarrow P_{k_{ij}}~\vec{s}_{ij} \qquad \mbox{for\ } j=1,\ldots,m_i |
65 \[ |
72 \] |
66 \bigwedge\vec{y}_{ij}.~\vec{B}_{ij} \Longrightarrow |
73 |
|
74 that can be solved using the assumptions |
|
75 |
|
76 \[ |
|
77 \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} |
78 \forall P_1 \ldots P_n.~\vec{K} \longrightarrow P_{k_{ij}}~\vec{s}_{ij} \qquad \mbox{and} \qquad \vec{K} |
68 \] |
79 \] |
69 *} |
80 *} |
70 |
81 |
71 end |
82 end |