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
------------------------------------------------------------------------------
Dive into the World of Parallel Programming. The Go Parallel Website,
sponsored by Intel and developed in partnership with Slashdot Media, is your
hub for all things parallel software development, from weekly thought
leadership blogs to news, videos, case studies, tutorials and more. Take a
look and join the conversation now. http://goparallel.sourceforge.net/
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
