Use existing Isabelle theories

[sternk]

Reported by till and assigned to luecke Migrated from http://trac.informatik.uni-bremen.de:8080/hets/ticket/357

---

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?

[sternk]

Comment by luecke Migrated from http://trac.informatik.uni-bremen.de:8080/hets/ticket/357#comment:4

---

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.

[sternk]

Comment by luecke Migrated from http://trac.informatik.uni-bremen.de:8080/hets/ticket/357#comment:7

---

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...