Using Axiomatic Type Classes in Isabelle
Markus Wenzel · 2000
Isabelle o#ers order-sorted type classes on top of the simple types of plain Higher-Order Logic. The resulting type system is similar to that of the programming language Haskell. Its interpretation within the logic enables further application, though, apart from restricting polymorphism syntactically. In particular, the concept of Axiomatic Type Classes provides a useful light-weight mechanism for hierarchically-structured abstract theories. Subsequently, we demonstrate typical uses of Isabelle's axiomatic type classes to model basic algebraic structures. This document describes axiomatic type classes using Isabelle/Isar theories, with proofs expressed via Isar proof language elements. The new theory format greatly simplifies the arrangement of the overall development, since definitions and proofs may be freely intermixed. Users who prefer tactic scripts over structured proofs do not need to fall back on separate ML scripts, though, but may refer to Isar's tactic emulation commands. ...