Use existing Isabelle theories

[till]

Create a bridge from CASL and HasCASL datatypes to Isabelle datatypes (e.g. Nat and Real).

• specify an isomorphism between the coded (Has)CASL type and the Isabelle type, that is, two functions between the corresponding types, plus a bunch of compatibility theorems (homomorphism equations), two for each operation.
• create two simpsets consisting homomorphism equations, one for each direction of the isomorphism (you also need to exploit bijectivity of the iso)
• transfer (Has)CASL goals into proper Isabelle goals, using one of the simpsets
• How to specify that Isabelle should be started with heap HOL-Complex?

[luecke]

What about making this more generic to use existing theories for provers. HOL/Complex is not really needed, unless we need the existence of elements dx.

[luecke]

A "real" hierarchy of datatypes in the Hets-lib would help. Before switching to Real... I would prefer to start with basic numbers. Maybe redesign the HasCASL reals...