Re: [isabelle] using Isabelle programmatically

> 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?


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