Isomorphisms — A Link Between the Shallow and the Deep
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.
KeywordsTheorem Prove High Order Logic Abstraction Function Concrete Classis Proof Script
Unable to display preview. Download preview PDF.
- M. J. C. Gordon and T. M. Melham, editors. Introduction to HOL: A theorem proving environment for higher order logic. Cambridge University Press, 1993.Google Scholar
- U. Hensel, M. Huisman, B. Jacobs, and H. Tews. Reasoning about classes in object-oriented languages: Logical models and tools. In C. Hankin, editor, Programming Languages and Systems-7th European Symposium on Programming, ESOP’98, LNCS 1381, pages 105–121. Springer-Verlag, 1998.CrossRefGoogle Scholar
- L. Lamport and L. C. Paulson. Should your specification language be typed? http://www.cl.cam.ac.uk/users/lcp/papers/lamport-paulson-types.ps.gz, 1997.
- B. Meyer. Reusable Software. Prentice Hall, 1994.Google Scholar
- T. Nipkow. More Church/Rosser proofs (in Isabelle/HOL). In Automated Deduction — CADE 14, LNCS 1104, pages 733–747. Springer-Verlag, 1996.Google Scholar
- S. Owre, N. Shankar, and J. M. Rushby. The PVS Specification Language. Computer Science Laboratory, 1993.Google Scholar
- T. Santen. On the semantic relation of Z and HOL. In J. Bowen and A. Fett, editors, ZUM’98: The Z Formal Specification Notation, LNCS 1493, pages 96–115. Springer-Verlag, 1998.Google Scholar
- T. Santen. A Mechanized Logical Model of Z and Object-Oriented Specification. PhDthesis, Fachbereich Informatik, Technische Universität Berlin, Germany, 1999. forthcoming.Google Scholar
- J. M. Spivey. The Z Notation — A Reference Manual. Prentice Hall, 2nd edition, 1992.Google Scholar
- H. Tej and B. Wolff. A corrected failure-divergence model for CSP in Isabelle/HOL. In J. Fitzgerald, C. B. Jones, and P. Lucas, editors, FME’97: Industrial Applications and Strengthened Foundations of Formal Methods, LNCS 1313, pages 318–337. Springer-Verlag, 1997.Google Scholar