Discussion with T. Nipkow on Isabelle, Mar 1995

The discussion served to find out which parts of the Madrid wish list for NGHDL (see Section 2.2.2) could be conveniently realised within Isabelle. Using existing proof systems such as Isabelle one hopefully could provide quickly and with comparatively little manpower a reasonably convenient proof system for NGHDL.

A particular topic was the amount of support Isabelle offers for systems of (in-)equations and infix/mixfix operators (which will be important for the strongly algebraic transformational style used in Augsburg). A typical example is the theory of regular expressions (e.g. for the description of pulse shapes as in B. Möller's Madrid talk, Section 2.2) or, more generally, of Kleene algebras.

The discussion led to the following results:

• Overall, the Isabelle ZF logic seems more suitable than the Isabelle HOL logic for the following reasons: It supports sets, partiality and fixpoint theory more directly than HOL; many of the inference rules we want are already built-in there.
• Isabelle has no good support for arithmetic and inequations (in particular, no built-in decision procedures for, say, Presburger arithmetic). This may cause some trouble when reasoning about time and time intervals. Special tactics will have to be developed there.
• For refinement this causes much fewer problems, since the inequations there will be subset relations which are more directly supported by Isabelle.
• Booleans, natural numbers, integers, sets, lists, strings and tree-like recursive types (free data types) are directly supported by ZF Isabelle. Even recursion through function types can be handled provided there are no occurrences of the recursive type on the left side of the function arrow.
• The items listed in Section2.2.2 under ``user support'' are not addressed well by Isabelle. Again, one would have to write special tactics there to achieve at least a minimum of what is desired. It may be better to provide exits from suitable sublanguages of NGHDL to other tools.