equal
deleted
inserted
replaced
3 begin |
3 begin |
4 |
4 |
5 section{* The General Construction Principle \label{sec:ind-general-method} *} |
5 section{* The General Construction Principle \label{sec:ind-general-method} *} |
6 |
6 |
7 text {* |
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. |
8 |
13 |
9 Before we start with the implementation, it is useful to describe the general |
14 Before we start with the implementation, it is useful to describe the general |
10 form of inductive definitions that our package should accept. |
15 form of inductive definitions that our package should accept. |
11 Suppose $R_1,\ldots,R_n$ be mutually inductive predicates and $\vec{p}$ be |
16 Suppose $R_1,\ldots,R_n$ be mutually inductive predicates and $\vec{p}$ be |
12 some fixed parameters. Then the introduction rules for $R_1,\ldots,R_n$ may have |
17 some fixed parameters. Then the introduction rules for $R_1,\ldots,R_n$ may have |