When encoding CASL structured specification into Isabelle, the problem arises that the structuring mechanism of CASL and Isabelle are rather different. In particular, Isabelle's mechanisms are considerably weaker: Extensions and unions of specifications are available in Isabelle (though the union is defined is a slightly different way), while for CASL's renamings, hidings, and generic specifications, nothing similar is available in Isabelle.
Currently, we solve this problem by just flattening structured specifications to basic specifications, that is, we literally carry out all the renamings, unions etc. Hidings can be treated by renaming the symbol which shall be hidden with a unique name that cannot be input by the user.
However, this is not very satisfactory, since flattening destroys the structural information of a specification and thus makes theorem proving in the specification harder. In some cases, the loss of structural information makes it practically infeasible to do proofs which are doable when the structuring is kept. Therefore, we have asked the Isabelle implementors to improve Isabelle's structuring mechanisms, and they have promised to do something in this direction.
In principle, an alternative way would be to use a deep encoding of CASL, which means to directly describe the semantics of CASL within higher-order logic. However, this is not very nice, since theorem proving in a deep encoding is relatively far away from proving in the encoded logic. In contrast, we use a shallow encoding, where proving in the encoding comes close to proving in the encoded logic. The advantage of a deep encoding would be that one can prove meta-properties about the semantics of CASL, but in our view, this does not outweigh the disadvantages.
An exceptional case are CASL's free specifications. One can hardly expect to implement them in a logic-independent way, since they depend on an involved construction in the model categories of the logic. All that one can expect here is to simulate the semantics of free specifications in a particular logic within higher-order logic, along the lines of [Sch94b, Sch94a].
Encoding of architectural specifications is beyond the scope of this paper - it will be dealt with elsewhere.
Figure 4: The web interface of the HOL-CASL system
As described in the previous section, libraries are an orthogonal matter. However, there is one important incompatibility between CASL and Isabelle at this point: CASL text files may contain libraries consisting of several specifications, while Isabelle text files always consist of exactly one Isabelle theory. We solve this problem by just splitting a CASL library into small files containing one specification each, and feeding these files into Isabelle. Or course, we also have to maintain the information associating a CASL library with the split files.
