6 Encoding CASL into HOL

In this section, we briefly recall the encoding from CASL into HOL from [MKK98]:

At the level of CASL basic specifications, the encoding into higher-order logic proceeds in three steps:

1. The CASL logic, subsorted partial first-order logic with sort generation constraints (SubPCFOL), is translated to subsorted first-order logic with sort generation constraints (SubCFOL) by encoding partiality via error elements living in a supersort.
2. Subsorted first-order logic with sort generation constraints (SubCFOL) is translated to first-order logic with sort generation constraints (CFOL) by encoding subsorting via injections (actually, this is built-in into the CASL semantics [CHKBM97]).
3. First-order logic with sort generation constraints (CFOL) is translated to higher-order logic (HOL) by expressing sort generation constraints via induction axioms.

These encodings are not only translations of syntax, but also have a model-theoretic counterpart³, which provides an implicit soundness and completeness proof for the re-use of HOL-theorem provers for theorem proving in the CASL logic SubPCFOL. This is also known as the "borrowing" technique of Cerioli and Meseguer [CM97] that allows to borrow theorem provers across different logics.