Hello. What is the preferred way to define functions only for some values? For example, as in arithmetic$DIV in HOL?:
⊢ ∀n. 0 < n ⇒ ∀k. k = k DIV n * n + k MOD n ∧ k MOD n < n)
Here nothing is asserted for the value of DIV for n = 0, thus it is
“undefined” in some sense. I know that this can be done with
“new_specification” but proving _trivial_ existence theorems seems like
something that should be automatized.
I am writing a formalization of elementary topology[1]. I have to define
the concept of the interior, closure, etc. Currently I use total
definitions. I am thinking that it may be more elegant to use a partial
definition like the above.
For example, currently I have the definition:
interior To X r ⇔
is_topo To ∧ X ⊆ space To ∧ r ∈ space To ∧
∃Y. r ∈ Y ∧ Y ⊆ X ∧ Y open_in To
I want to change this to:
is_topo To ∧ X ⊆ space To ⇒
interior To X = ⋃ {Y | Y ⊆ X ∧ Y open_in To}
Is there some expected difficulty with this under-specification?
Thanks.
[1] <https://puszcza.gnu.org.ua/projects/hol-proofs/> (work in progress).
--
Do not eat animals; respect them as you respect people.
https://duckduckgo.com/?q=how+to+(become+OR+eat)+vegan
signature.asc
Description: OpenPGP digital signature
------------------------------------------------------------------------------ Check out the vibrant tech community on one of the world's most engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
