The set of extended-real numbers R’ is the set of real numbers R extended with two additional elements, namely, the positive infinity +∞ and negative infinity -∞. Extended reals are useful in describing limiting behaviors in many mathematical fields. In particular, it is necessary to use the extended reals system to define the integration theory as otherwise the convergence theorems, like the monotone convergence and dominated convergence, would be less useful. Similarly, using extended reals for defining the measure theory allows us to define infinite measures like the sigma-finite measure. We now describe the HOL4 formalization of extended reals.
4.1.1 Type and Operators
An extended real is either a normal real number or positive infinity or negative infinity. We use Hol_datatype to define the new type extreal as follows:
val _ = Hol_datatype ‘extreal = NegInf | PosInf | Normal of real ‘
The HOL4 notation x: extreal is used to specify that the type of the variable x is extreal. The function Normal will convert a real number in HOL4 to its corresponding extended real number. For example, Normal (1: real) returns an extended real number (1: extreal). All the arithmetic operations of the real numbers need to be extended for the new type. This can be done by defining HOL4 functions over the new type and then overloading the common operators using these functions. For instance, the addition operation over the extended-real numbers can be defined using the function extreal_add as follows:
⊢∀ x y. extreal_add (Normal x) (Normal y) = (Normal x + y) ˄
extreal_add (Normal _) a = a ˄
extreal_add b (Normal _) = b ˄
extreal_add NegInf NegInf = NegInf ˄
extreal_add PosInf PosInf = PosInf
The function is left undefined when one of the operands is PosInf and the other is NegInf. The + operator is then overloaded as
val _ = overload_on (“+”, Term ‘extreal_add’);
Similarly, the other arithmetic operations have also been defined for extended reals and their corresponding operators can be overloaded in HOL4 as follows:
val _ = overload_on (“-”, Term ‘external_sub ‘);
val _ = overload_on (“*”, Term ‘external_mul ‘);
val _ = overload_on (“/”, Term ‘external_div ‘);
val _ = overload_on (“<=”, Term ‘external_le ‘);
val _ = overload_on (“<”, Term ‘external_lt ‘);
val _ = overload_on (“~”, Term ‘external_ainv ‘);
val _ = overload_on (“numeric_negate”, Term ‘external_ainv ‘);
val _ = overload_on (“inv”, Term ‘external_inv ‘);
val _ = overload_on (“abs”, Term ‘external_abs ‘);
val _ = overload_on (“logr”, Term ‘external_logr ‘);
val _ = overload_on (“lg”, Term ‘external_lg ‘);
val _ = overload_on (“exp”, Term ‘external_exp ‘);
val _ = overload_on (“pow”, Term ‘external_pow ‘);
val _ = overload_on (“sqrt”, Term ‘external_sqrt ‘);
The order relation, for example, is extended as: ∀a ∈R’, -∞ ≤ a ≤ +∞.
⊢ ∀ x y. extreal_le (Normal x) (Normal y) = (x ≤ y) ˄
extreal_le NegInf a = T ˄
extreal_le b PosInf = T ˄
extreal_le c NegInf = F ˄
extreal_le PosInf d = F
With the order shown in Definition 4.2, R’ is a complete lattice where every subset has a supremum and an infimum.