Re: [isabelle] SMT integration to Isabelle/HOL

On Mon, 16 Apr 2012, Shuling Wang wrote:

I find that our use of Isabelle/HOL needs to go to the ML level, e.g., defining tactics, and SMT integration mentioned above. But it is very difficult for me to understand the ML implemental theories of Isabelle/HOL.

The ML tools of Isabelle/HOL are indeed quite complex, but this does not mean that one should be afraid of Isabelle/ML in general. Isabelle/Isar and Isabelle/ML are tightly integrated, and I usually do not speak of a separate "ML level". It is more like the Yin and Yang (阴阳) of Isabelle.

Can you please give me some directions to learn them, or any documents especially about the oracle and tactics faculties of Isabelle?

The isar-ref manual section 5.11 explains oracles and points to some basic example in ~~/src/HOL/ex/Iff_Oracle.thy which can be taken as a starting point to warm-up with Isabelle/ML and Isabelle/Isar intermixed.

This is best used with the Isabelle/jEdit Prover IDE. I.e. you start "isabelle jedit" and open the Iff_Oracle.thy file. ML that is directly embedded into theory sources is marked up with inferred type information and hyperlinks for identifiers in the ML text. This greatly helps to navigate ML sources, but it does not work yet for external ML files.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.