Email Gateway (Aug 22 2022 at 20:58): Email Gateway (Aug 22 2022 at 20:58):From: Peter Lammich <lammich@in.tum.de>
Hi List,
I recently ran into the functions Thm.trim_context and Thm.transfer'',
they are used, e.g., to store and retrieve named_theorems.
However, I cannot find any documentation. What do these functions do?
Email Gateway (Aug 22 2022 at 21:04):From: Makarius <makarius@sketis.net>
Documentation is indeed missing, I will have to do it for the Isabelle2020
release.
Generally, when you retrieve stored thms from the (theory) context, you need
to make sure that they "belong" to the current background theory: Thm.transfer
was introduced for that a long time ago (but tools sometimes "forgot" that).
More recently, I have added Thm.trim_context to trim down the current theory
certificate to its core purpose: to identify the theory, without all its
context data. This helps to avoid a certain forms of memory leak: there could
be 10^5 or 10^6 intermediate theory values that are not needed later on, due
to the mandatory Thm.transfer applied later.
In Isabelle2019 and afterwards, more and more tools do Thm.trim_context to
save memory, but also as reminder that a proper Thm.transfer is required to
revive the retrieved thm: after Thm.trim_context you get an exception on
Thm.theory_of_thm if you forget Thm.transfer.
Makarius
Last updated: Apr 18 2024 at 20:16 UTC