31 |
31 |
32 As a running example, we have chosen a rather simple package for defining |
32 As a running example, we have chosen a rather simple package for defining |
33 inductive predicates. To keep things really simple, we will not use the |
33 inductive predicates. To keep things really simple, we will not use the |
34 general Knaster-Tarski fixpoint theorem on complete lattices, which forms |
34 general Knaster-Tarski fixpoint theorem on complete lattices, which forms |
35 the basis of Isabelle's standard inductive definition package. Instead, we |
35 the basis of Isabelle's standard inductive definition package. Instead, we |
36 will use a simpler \emph{impredicative} (i.e.\ involving quantification on |
36 will describe a simpler \emph{impredicative} (i.e.\ involving quantification on |
37 predicate variables) encoding of inductive predicates. Due to its |
37 predicate variables) encoding of inductive predicates. Due to its |
38 simplicity, this package will necessarily have a reduced functionality. It |
38 simplicity, this package will necessarily have a reduced functionality. It |
39 does neither support introduction rules involving arbitrary monotone |
39 does neither support introduction rules involving arbitrary monotone |
40 operators, nor does it prove case analysis (or inversion) rules. Moreover, |
40 operators, nor does it prove case analysis rules (also called inversion rules). |
41 it only proves a weaker form of the induction principle for inductive |
41 Moreover, it only proves a weaker form of the induction principle for inductive |
42 predicates. |
42 predicates. |
43 *} |
43 *} |
44 |
44 |
45 end |
45 end |