This directory defines the star type constructor for non-standard extensions of types. It generalizes the hypreal, hypnat, and hcomplex types defined by the HOL-Complex theory. This development reuses several files from that theory, and also uses generalized forms of some of its definitions and proofs.
Most concepts in the theory are defined in terms of two basic functions: star_of is an injective function for lifting standard values into a non-standard type, and Ifun is for defining "internal" functions. Another fundamental constant is infnat, which has the property of being distinct from star_of n for all natural numbers n.
star_of :: 'a => 'a star
Ifun :: ('a => 'b) star => ('a star => 'b star)
infnat :: nat star
Using Ifun and star_of, we can define non-standard lifted versions for functions and predicates of any arity.
Proofs in the theory derive from a few properties of these basic operations, together with the transfer principle. The transfer principle is a meta-mathematical theorem, which says that many propositions over non-standard types are logically equivalent to corresponding propositions over standard types.
In this theory, the transfer principle is implemented as a proof tactic. When applied to an appropriate subgoal, it replaces the subgoal with a logically equivalent one that does not refer to the star type constructor. The tactic produces a proof of the equivalence; it does not generate any new axioms.