Using the encoding described in the previous section, we have built an interface from CASL to Isabelle/HOL. We have chosen Isabelle [Pau94] because it has a very small core guaranteeing correctness. Furthermore, there is over ten years of experience with it (several mathematical textbooks have been verified with Isabelle), Last but not least, Isabelle is generic, i.e. it upports quite a number of logics, and it is possible to define your own logic within Isabelle. Despite the genericity of Isabelle, we have refrained from building the CASL logic directly into Isabelle - this would violate our guideline to re-use existing tools as much as possible: we would have to set up new proof rules, and instantiate the Isabelle simplifier (a rewriting engine) and tableau prover from scratch. Instead, we re-use the Isabelle logic HOL, for which already sophisticated support is available, with the help of the encoding described in section 6.
This encoding has a clear semantical basis due to the borrowing (most other encodings into Isabelle/HOL do not have an explicit model-theoretic counterpart). However, a good semantic basis does not imply that there are no practical problems:
First, the encoding of CASL in Isabelle/HOL as described in [MKK98] produces too complex output. We had to fine-tune the output by suppressing superfluous parts (for example, trivial subsort injections), while retaining its mathematical correctness.
Another problem with borrowing is that the HOL-CASL user really works with the encoding of a CASL specification, and not with the CASL specification itself. In particular, goals and subgoals are displayed as HOL formulas, and the proof rules are of course the Isabelle/HOL proof rules. However, a typical user of the tool will probably be more familiar with CASL than with Isabelle/HOL. Therefore, we have decided to display goals and subgoals in a CASL-like syntax as much as possible. For example, an injection of a term t from a subsort s1 to a supersort s2 is displayed as t : s2, as in CASL, and not as injs1,s2(t), as the encoding would yield. In this way, we get a CASL-like display syntax of Isabelle/HOL. Let us call this display syntax "CASLish Isabelle/HOL".
However, note that the CASLish Isabelle/HOL omits some information, e.g. the information that an injection injs1,s2(t) starts from s1. In some practical example proofs, this turned out to be rather confusing (while in others, the longer form injs1,s2(t) is just tedious), and one would like to go back to the "pure Isabelle/HOL" view of the subgoals instead of using the "CASLish Isabelle/HOL". Therefore, we plan to let the user choose among several pretty printing "views" on his or her encoded CASL specification.
A related problem is that of input of goals. Goals are of course input in the CASL syntax (only during a proof, they get redisplayed in CASLish Isabelle/HOL syntax). One would like also to be able to input goals in Isabelle/HOL, for example when one needs to prove a lemma that is formulated in Isabelle/HOL. We solve this by providing Isabelle/HOL as a theory within our interface, and we parse goals that are input for this theory always with the Isabelle/HOL parser, and not with the CASL parser.
Sometimes, these two "pure" input syntaxes (the CASL and the ISabelle/HOL syntax) are not sufficient. An example is the following: In Isabelle, there are two different kinds of free variables: Object variables, which cannot be instantiated during a proof, are used for proofs of universally quantified sentences. Such variables are needed, for example, in a goal forall x,y:Nat · x*y=y*x which is automatically converted to its free form x*y=y*x by the encoding, since the free form can be better handeled in Iasbelle/HOL. The other kind of variables are meta variables, which can be instantiated during a proof, giving an informative answer substitution during the proof of an existentially quantified sentence (cf. Prolog, narrowing). For example, when trying to prove exist x:Nat · x+9=12 it makes more sense to input the goal ?x + 9 =12 and get ?x instantiated with 3 during the proof (while the goal x+9=12 is not provable, since forall x:Nat · x+9=12 is false).
We now provide the facility to input goals in CASL with both kinds of variables. We are therefore working with a mixture of CASL and Iasbelle/HOL.
In future work, we will study the semantic relationships between the different input and display syntaxes and a true combination of CASL and HOL (like higher-order CASL [HKBM98]) in more detail.