Stream: Archive Mirror: Isabelle Users Mailing List

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

Email Gateway (Aug 22 2022 at 11:12):

From: Viorel Preoteasa <viorel.preoteasa@aalto.fi>
Hello,

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

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

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

How can I achieve this?

Best regards,

Viorel Preoteasa

Email Gateway (Aug 22 2022 at 11:22):

From: Lars Hupel <hupel@in.tum.de>
Hello Viorel,

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

this can be achieved like so:

Proof_Context.get_thms ctxt "append.simps"

Depending on where you get these theorem names from, it might make more
sense to use the appropriate parsers which produce theorems directly (e.g.
Attrib.thms). I would strongly encourage to use those instead.

Cheers
Lars

Email Gateway (Aug 22 2022 at 11:23):

From: Makarius <makarius@sketis.net>
(NoteThatCamelCaseIsNotUsedInIsabelleSources.)

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.

Makarius

Email Gateway (Aug 22 2022 at 11:24):

From: Viorel Preoteasa <viorel.preoteasa@aalto.fi>
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

Email Gateway (Aug 22 2022 at 11:26):

From: Viorel Preoteasa <viorel.preoteasa@aalto.fi>
Hi Lars,

Thank you for your message.

On 9/1/2015 5:30 PM, Lars Hupel wrote:

Hello Viorel,

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

Proof_Context.get_thms ctxt "append.simps"

This seems to give me what I need.

Depending on where you get these theorem names from, it might make more
sense to use the appropriate parsers which produce theorems directly (e.g.
Attrib.thms). I would strongly encourage to use those instead.
The first thing th.at I run into was Attribthms , but I did not manage
to use it.

These theorems are all fixed under some declaration:

theorems MySimps = ...

and in different theories I need to use different theorems, so I will just
define MySimps to be one or another list.

Best regards,

Viorel

Email Gateway (Aug 22 2022 at 11:27):

From: Makarius <makarius@sketis.net>
That is the missing [foo only] that will probably emerge for the next
release. For now, the implementation of Named_Theorems can be taken as an
example how to do such things yourself.

An important ingredient is Local_Theory.add_thms_dynamic to expose certain
context-defined fact content to the user by a specific name. If you don't
like general Local_Theory programming interfaces, you can also do it a
global theory like this:

setup ‹Global_Theory.add_thms_dynamic (@{binding foo}, undefined)›

The "undefined" function accesses your tool-specific facts. You can
maintain that in any way you like, e.g. via Generic_Data in the context.

Makarius

Last updated: Apr 24 2024 at 08:20 UTC