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 Higher order logic, as implemented in Isabelle/HOL, is based on just a few |
18 HOL is based on just a few primitive constants, like equality, implication, |
19 primitive constants, like equality, implication, and the description |
19 and the description operator, whose properties are described as axioms. All |
20 operator, whose properties are described as axioms. All other concepts, such |
20 other concepts, such as inductive predicates, datatypes, or recursive |
21 as inductive predicates, datatypes, or recursive functions are defined in |
21 functions are defined in terms of those constants, and the desired |
22 terms of those constants, and the desired properties, for example induction |
22 properties, for example induction theorems, or recursion equations are |
23 theorems, or recursion equations are derived from the definitions by a |
23 derived from the definitions by a formal proof. Since it would be very |
24 formal proof. Since it would be very tedious for a user to define complex |
24 tedious for a user to define complex inductive predicates or datatypes ``by |
25 inductive predicates or datatypes ``by hand'' just using the primitive |
25 hand'' just using the primitive operators of higher order logic, |
26 operators of higher order logic, Isabelle/HOL already contains a number of |
26 Isabelle/HOL already contains a number of packages automating such |
27 packages automating such work. Thanks to those packages, the user can give a |
27 work. Thanks to those packages, the user can give a high-level |
28 high-level specification, like a list of introduction rules or constructors, |
28 specification, like a list of introduction rules or constructors, and the |
29 and the package then does all the low-level definitions and proofs behind |
29 package then does all the low-level definitions and proofs behind the |
30 the scenes. In this chapter we explain how such a package can be |
30 scenes. In this chapter we explain how such a package can be implemented. |
31 implemented. |
31 |
32 |
32 |
33 %The packages are written in Standard ML, the implementation |
33 %The packages are written in Standard ML, the implementation |
34 %language of Isabelle, and can be invoked by the user from within theory documents |
34 %language of Isabelle, and can be invoked by the user from within theory documents |
35 %written in the Isabelle/Isar language via specific commands. Most of the time, |
35 %written in the Isabelle/Isar language via specific commands. Most of the time, |
36 %when using Isabelle for applications, users do not have to worry about the inner |
36 %when using Isabelle for applications, users do not have to worry about the inner |