Isomorphisms – a link between the shallow and the deep

Abstract

We present a theory of isomorphisms between typed sets in Isabelle/HOL. Those isomorphisms can serve to link a shallow embedding with a theory that defines certain concepts directly in HOL. Thus, it becomes possible to use the advantage of a shallow embedding that it allows for efficient proofs about concrete terms of the embedded formalism with the advantage of a deeper theory that establishes general abstract propositions about the key concepts of the embedded formalism as theorems in HOL.