Re: [isabelle] Obtaining a list of theorems in ML

On Tue, 1 Sep 2015, Viorel Preoteasa wrote:

I am interested in obtaining the theorems declared in a certain context.
I know that I can get these theorems from the current context using
anti-quotations @{thms MyTh}. However this is not satisfactory because
I need these theorems from a dynamic context which is passed as an
argument to a function.

So I need a function "GetMyThms ctxt" which does exactly the same
as @{thms MyTh}, but for ctxt parameter, and not the current context.

theorems MyTh = exI exE

val my_ths = @{thms MyTh};
val ctxt = @{context}

fun GetMyThms ctxt = ..;
val my_thsa = GetMyThms ctxt;


What the @{thms} does exactly can be explored by following its definition in Isabelle/ML (using C-hover-click in the Prover IDE). The main thing is Attrib.thm; it has relatives like Attrib.eval_thms (rarely used in practice) and Proof_Context.get_fact.

That does dynamic evaluation of fact names and attribute expressions at runtime. Normally you don't want to do that under program control -- it used to be called "fishing" in the past, but that technique is no longer seen today, because there are usually better ways.

For example, dynamically changing facts can be managed like this in Isabelle2015:

  named_theorems foo

  ML âfun get_foo ctxt = Named_Theorems.get ctxt @{named_theorems foo}â

The user can now use attributes [foo add] or [foo del]. Your tool can use get_foo to see the current content in a given context.


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