[Hol-info] Question: Internal HOL4 resource usage when using prove, store_thm, and Define

[Jiaqi T. <tan...@cm...>]

Hi,

I have some questions regarding the internals of HOL4, and whether there
are any internal resources (memory/storage) used when certain functions are
used.

1. If I use prove or TAC_PROOF, and a theorem is successfully proved, is
the theorem automatically saved in internal HOL4 storage? I would believe
it is not stored, unless I assigned it to a variable with val my_thm =
prove(...). In this case, if I just use prove() (or TAC_PROOF) without
saving the result to a variable, does this mean that one command later on
the interactive shell, the prove theorem will no longer use any resources?
(i.e. after val it has been overwritten).

2. If I use store_thm instead, then this would consume resources in HOL4's
internal memory? After I call store_thm, suppose I don't need the theorem
any more, is there any way to reclaim the internal storage used?

3. Similarly for Define, are the theorems which described the Define-d
function stored internally in HOL4 storage? Suppose I do "Define ``MY_FUNC
= 1``", and I do not store the definition theorem in a variable, does the
definition still get stored internally in HOL4? And is there any way to
clear/remove the definition later to reclaim space if so?

In general, if I am Define-ing a large number of functions for temporary
use (e.g. rewriting away a large expression), but I do not need them after
a certain point in the code, are there any internal HOL4 memory/resources
used, and is there any way to reclaim these resources later?

Thank you in advance!

Regards,
Jiaqi