Re: [isabelle] using Isabelle programmatically



Thank you Lars,

This is exactly what I need. I tested it with both
isabelle console and isabelle_process, and it works
in the same way.

Best regards,

Viorel

On 04/09/2015 06:46 PM, Lars Hupel wrote:
>> Second, there's the question how to invoke just this bit. I think
>> 'isabelle console' is out â quoting from the system manual:
> This assessment was wrong. It is possible with 'isabelle console':
>
> $ bin/isabelle console
>> val commit = fn: unit -> bool
> val it = (): unit
> ML> val thy = Thy_Info.get_theory "Main";
> val thy = ...: theory
>
> From there on, you can obtain a context:
>
> ML> val ctxt = Proof_Context.init_global thy;
> val ctxt = <context>: Proof.context
>
> Now you can read a term (not just parse!):
>
> ML> val t = Syntax.read_term ctxt "rev []";
> val t =
>    Const ("List.rev", "'a List.list => 'a List.list") $
>      Const ("List.list.Nil", "'a List.list"): term
>
> ... and rewrite:
>
> ML> Simplifier.rewrite ctxt (cterm_of thy t) |> Thm.rhs_of;
> val it = "[]": cterm
>
> Does that help?
>
>
> Cheers
> Lars





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