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



Hi Makarius,

Thank you for your answer.

(NoteThatCamelCaseIsNotUsedInIsabelleSources.)
I was almost sure that I will make a mistake in this example. I did
think about the "ctxt" abbreviation, and it seems I got it right.

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.

I did find Attrib.thm by cotrol-click of @{thms ...}, but I did not know how to use it directly.


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 is a nice solution. Is there a way to also clear the foo content, without knowing what it contains?

Viorel




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