Email Gateway (Aug 22 2022 at 17:23): Email Gateway (Aug 22 2022 at 17:23):From: Lawrence Paulson <lp15@cam.ac.uk>
Extending the domain of division with x/0 = 0 (and also for integers) is a common choice in a great many systems, not just Isabelle/HOL but HOL Light, HOL4, MetiTarski and doubtless many other systems. They do it simply for convenience and not for any deep reason. The point is that many laws involving division will then hold unconditionally, an example being (ab)/(cd) = (a/c)*(b/d).
Another example of domain extension is that the finite sum operator yields 0 if given an infinite index set. (This has nothing to do with the sum of an infinite series, which is a limit.) Again there is no deep reason, it is simply that some simple identities involving finite summation can be proved without requiring the index set to be finite.
The technique of extending the domains of functions to simplify theorem proving goes back at least to the 1970s and the Boyer/Moore prover.
Larry Paulson
Last updated: May 06 2024 at 08:19 UTC