Re: [isabelle] using Isabelle programmatically



On 09.04.2015 16:13, Viorel Preoteasa wrote:
>
> 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)
Lars has already written something about how to acquire a context.
Depending on what you do with the terms in your program, it might be a
good idea to use the YXML format to pass terms between Isabelle and your
program. There have been some discussions on that subject in the past.




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