Re: [isabelle] using Isabelle programmatically




On 04/09/2015 04:46 PM, Lars Hupel wrote:
>> How can this be done programmatically? Should I use
>> "isabelle_process" or "isabelle console"?
> First of all, there's 'Simplifier.rewrite':
>
> MLâSimplifier.rewrite @{context} @{cterm "rev []"}â
The function Simplifier.rewrite seem to be available in isabelle_process,
but I don't know how to get the context, and the term in the right
form. The actual simplifying command contains also
some lemmas that I do not necessarily want as simplification
rules.

I noticed also that there is a function for parsing terms, but it also
requires a context parameter. It seems that what I should do is:

context = ...
T = Simplifier.rewrite context (Syntax.parse_term context "...")
result =  Syntax.string_of_term context (the right hand side term of T)


>
> ... which results in
>
> val it = "rev [] â []": thm
>
> This should be an easy-enough interface to perform just what you need.
>
>
> Second, there's the question how to invoke just this bit. I think
> 'isabelle console' is out â quoting from the system manual:
>
> "Interaction works via the raw ML toplevel loop: this is neither
> Isabelle/Isar nor Isabelle/ML within the usual formal context. Some
> useful ML commands at this stage are cd, pwd, use, use_thy, use_thys."
>
> 'isabelle_process' is even more low-level.
>
> In which environment do you intend to invoke the simplifier? In some
> program of yours? Via bash? Something else? Repeatedly, or just one-off?
I need to perform this operation from within a Python program.
I use Python to produce some terms based on some specification,
and I need them simplified using Isabelle. The terms are using
definitions from the supporting theory.

Viorel




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