CookBook/Package/Ind_Intro.thy
changeset 116 c9ff326e3ce5
parent 115 039845fc96bd
child 120 c39f83d8daeb
equal deleted inserted replaced
115:039845fc96bd 116:c9ff326e3ce5
     9   {\em
     9   {\em
    10   ``My thesis is that programming is not at the bottom of the intellectual \\
    10   ``My thesis is that programming is not at the bottom of the intellectual \\
    11   pyramid, but at the top. It's creative design of the highest order. It \\
    11   pyramid, but at the top. It's creative design of the highest order. It \\
    12   isn't monkey or donkey work; rather, as Edsger Dijkstra famously \\
    12   isn't monkey or donkey work; rather, as Edsger Dijkstra famously \\
    13   claimed, it's amongst the hardest intellectual tasks ever attempted.''} \\[1ex]
    13   claimed, it's amongst the hardest intellectual tasks ever attempted.''} \\[1ex]
    14   Richard Bornat, In defence of programming \cite{Bornat-lecture}
    14   Richard Bornat, In Defence of Programming \cite{Bornat-lecture}
    15   \end{flushright}
    15   \end{flushright}
    16 
    16 
    17   \medskip
    17   \medskip
    18   HOL is based on just a few primitive constants, like equality and
    18   HOL is based on just a few primitive constants, like equality and
    19   implication, whose properties are described by axioms. All other
    19   implication, whose properties are described by axioms. All other concepts,
    20   concepts, such as inductive predicates, datatypes, or recursive functions
    20   such as inductive predicates, datatypes, or recursive functions are defined
    21   are defined in terms of those constants, and the desired properties, for
    21   in terms of those constants, and the desired properties, for example
    22   example induction theorems, or recursion equations are derived from the
    22   induction theorems, or recursion equations are derived from the definitions
    23   definitions by a formal proof. Since it would be very tedious for a user to
    23   by a formal proof. Since it would be very tedious for a user to define
    24   define complex inductive predicates or datatypes ``by hand'' just using the
    24   complex inductive predicates or datatypes ``by hand'' just using the
    25   primitive operators of higher order logic, packages have been implemented
    25   primitive operators of higher order logic, \emph{definitional packages} have
    26   automating such work. Thanks to those packages, the user can give a
    26   been implemented automating such work. Thanks to those packages, the user
    27   high-level specification, like a list of introduction rules or constructors,
    27   can give a high-level specification, for example a list of introduction
    28   and the package then does all the low-level definitions and proofs behind
    28   rules or constructors, and the package then does all the low-level
    29   the scenes. In this chapter we explain how such a package can be
    29   definitions and proofs behind the scenes. In this chapter we explain how
    30   implemented.
    30   such a package can be implemented.
    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 general
    33   inductive predicates. To keep things really simple, we will not use the general
    34   Knaster-Tarski fixpoint theorem on complete lattices, which forms the basis
    34   Knaster-Tarski fixpoint theorem on complete lattices, which forms the basis
    35   of Isabelle's standard inductive definition package.  Instead, we will use a
    35   of Isabelle's standard inductive definition package.  Instead, we will use a
    37   variables) encoding of inductive predicates suggested by Melham
    37   variables) encoding of inductive predicates suggested by Melham
    38   \cite{Melham:1992:PIR}. Due to its simplicity, this package will necessarily
    38   \cite{Melham:1992:PIR}. Due to its simplicity, this package will necessarily
    39   have a reduced functionality. It does neither support introduction rules
    39   have a reduced functionality. It does neither support introduction rules
    40   involving arbitrary monotone operators, nor does it prove case analysis (or
    40   involving arbitrary monotone operators, nor does it prove case analysis (or
    41   inversion) rules. Moreover, it only proves a weaker form of the
    41   inversion) rules. Moreover, it only proves a weaker form of the
    42   induction theorem.
    42   induction principle for inductive predicates.
    43 *}
    43 *}
    44 
    44 
    45 end
    45 end