Support definitions that are local to a theory

[myreen]

I would like to be able to write local on some definitions:

Definition foo_def[local]:
  foo n = n + 1:num
End

The intended meaning is the same as writing:

Definition foo_def:
  foo n = n + 1:num
End

...
                
val _ = (delete_const "foo"; export_theory());

[myreen]

The delete_const at the end there might be a bit too destructive since some people give HOL the entire script file (including the export_theory line) when starting their session.

My main wish is that the local definitions are as absent as possible from the perspective of other theories.

[konrad-slind]

Deletion of constants and invalidation of definitions is a big change to the HOL logic. I have no problem with it being an informal aspect of working with HOL, especially when working in a scratch theory. But it would be nice to have it formally verified in something like the Candle setting.

Half-baked thought: maybe export_theory() could be refined into a kind of "conservative extension" inference rule which only retains material in the current theory segment that has types and constants drawn from (A) the ancestry or (B) the "segment signature", which lists out the types and constants one wants to keep from the current theory segment.

[konrad-slind]

Or one could take a complementary approach and list out the "segment co-signature" which enumerates the types and constants one wants to suppress.