Re: [isabelle] using Isabelle programmatically



On Fri, 10 Apr 2015, Viorel Preoteasa wrote:

Ideally I would need an API available in Python which does what I need: Simplifies a term based on a specific theory. I understand now that this API is available for Scala, and of course for SML, so in the future I may use Scala.

On the other hand, even if using SML, getting started with it does not seem easy. I tried to find the right functions for this job before posting the question to the mailing list.

Do you mean SML as a language, or Isabelle/ML as a language + library?

Getting started with Standard ML should be easy, using resources on the web or text books.

Getting started with Isabelle/ML should be easy as well, since the Isabelle Prover IDE allows to explore whatever you see, down to its actual definition. Tools are defined in Isabelle/ML, so the standard PIDE control-hover-click over Isar commands, methods, attributes etc. will show the relevant ML definitions.

Reading and understanding that needs some practice and some guidance, though. The "implementation" provides many explanations of many things, but it is not a quick-and-dirty HOWTO guide.


Depending on what you ultimately want to achieve, some decent Isabelle/ML could work out easier and more robust than tinkering with scripting languages, processes, generated sources etc.


	Makarius




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