An Interpretation of Isabelle/HOL in HOL Light

We define an interpretation of the Isabelle/HOL logic in HOL Light and its metalanguage, OCaml. Some aspects of the Isabelle logic are not representable directly in the HOL Light object logic. The interpretation thus takes the form of a set of elaboration rules, where features of the Isabelle logic that cannot be represented directly are elaborated to functors in OCaml. We demonstrate the effectiveness of the interpretation via an implementation, translating a significant part of the Isabelle standard library into HOL Light.

• Type: Conference
• Year: 2006
• Where: CADE
• Authors: Sean McLaughlin
• Keywords: Automated Reasoning, CADE 2006, HOL Light, HOL Light Object, Isabelle Logic