A Consistent Foundation for Isabelle/HOL

A Correction Patch

This page presents a correction patch from the paper A Consistent Foundation for Isabelle/HOL.

The patch is supposed to be applied to Isabelle2014.
Patch

The patch can be applied by the following command provided we are in the home directory of Isabelle2014:

bash:~/Isabelle2014> patch -p1 < correction-patch-Isabelle2014

The patch can be unapplied by the following command:

bash:~/Isabelle2014> patch -p1 -R < correction-patch-Isabelle2014

There is the Example 2 from the paper with a proof of False as an Isabelle theory.
Example 2
This example does not go through after the patch is applied. This can be tested as follows:

bash:~> path/to/Isbelle2014/isabelle build -D. False

There are couple of comments on this patch (partly only for Isabelle experts):

• Basic philosophy (as described in the paper): if u = p is defined, u depends on all items in p that have a global name in the system, i.e., on constants and type constructors.
• Difference from the paper: in paper we talk about a polymorphic HOL with ad hoc overloading. In the case of Isabelle/HOL, the situation is from a technical (implementation) point view a little bit more complicated since Isabelle contains a meta-framework (Pure) and object logics implemented in this framework (e.g., HOL). Overloading of constants is defined in Pure and the cyclicity checker as well (the file defs.ML). Typedef is implemented in HOL. In the paper, we present an optimization that when we declare dependencies, we recurse only below the function type but not below other type constructors, e.g., if c = (t :: int list => nat list), we declare the following dependencies c -> int list and c -> nat list. But, as mentioned, this mechanism is a part of Pure and therefore we don't know if the underlying object logic is HOL, i.e., a logic where this optimization is admissible. Thus, we include dependencies on all subtypes in u = p, i.e., we recurse below all type constructors not only below the function type. For the above mentioned example, we declare additionally c -> int and c -> nat. From a correctness point of view, this is clearly OK since we track (possibly) more dependencies and therefore the termination in this patch implies termination of the dependency relation in the paper. From a restrictiveness point of view, this is not more restrictive for HOL (we discover the extra dependencies transitively anyway). For other logics, we argue that this is the most faithful approach (without knowing how types are defined in the particular object logic): namely, adding a dependency on everything that has a global name on the right-hand side of a definition.
• If a new type T ≈ A is defined in Isabelle/HOL, T depends on constants and types (again all of them) in A. Abs_T and Rep_T depend on T.
• The data structure (graph of dependencies) in defs.ML (the cyclicity checker) was visionarily defined in a very abstract way such that the structure doesn't know a priori that it stores dependencies of constants. This allows us to do a very minimal change to include also types: we have to only separate the name spaces of constants and type constructors, whose names serve as labels of nodes in the dependency graph. This is achieved by creating a datatype with two constructors (datatype node = NConst of string | NType of string). The rest of the logic of the data structure is untouched.
• If a constant is defined axiomatically in Isabelle, it is declared as "final" (our terminology), which means that the definition of the constant is fixed and cannot be changed by the defs command. The constant is present in the graph but doesn't have any dependencies. This enables a very useful optimization during normalization of the graph: only those dependencies are kept that lead to uninterpreted constants (whose later overloaded definitions can potentially complete a cycle in the graph) from overloading.
• The same optimization was implemented also for types: if a type is declared by the Isar command typedecl, such a type is declared to be final. If a type is introduced by typedef it is not final and dependencies are provided (but of course during the normalization of the graph they can be again reduced to empty dependencies if the type doesn't (transitively) depend on any uninterpreted constants).
• Four basic types introduced during bootstrapping of Pure are also declared as final: namely types fun, prop, itself and dummy.
• According to measurements (build of the whole Isabelle distribution and AFP), the patch doesn't have any observable impact on the speed of the system. This proves that including dependencies on all subtypes does not create a performance bottleneck.