In this paper we briey discuss two constructions of the Mizar language redenitions and registrations. We focus on practical aspects of using them in Mizar texts to be eectively processed by the Mizar Verifier. We describe situations when redenitions can be and should be replaced by corresponding registrations.
Introduction which registrations should be used instead of redenitions, whenever possible. The question now is what are the situations when redenitions can be replaced by corresponding registrations. Before we answer this question, let us mention that the Mizar system provides two ways to introduce new types: not expandable (really new constructors) and expandable (shortcuts for collections of adjectives assigned to radix types) 2. Now, we can formulate a rule which denes situations when redenitions can be replaced by registrations: If the result type of a functor and the mother type of a mode to which the original type of the functor and the mode is redened is an expandable type, then such redenitions are replaceable by a functorial registration in the case of functors and by a conditional registration in the case of modes . Practical examples which depict the rule are presented in the next section. 3 3.1
Examples from the Mizar Mathematical Library Let us consider the functor Balls(x) [Sko98] which denes a family of balls in a topological space generated by a metric space:
To declare that Balls(x) constitutes a base in the space, the authors used the redenition: definition let M be non empty MetrStruct, x be Point of TopSpaceMetr(M); func Balls(x) -> Subset-Family of TopSpaceMetr(M) ... end; definition let M be non empty MetrSpace, x be Point of TopSpaceMetr(M); redefine func Balls(x) -> Basis of x; end; But, because the mode Basis of x [Try97] is dened as an expandable mode: definition let T be non empty TopStruct, x be Point of T; mode Basis of x is open x-quasi_basis Subset-Family of T; end; the redenition can be replaced by the functorial registration: registration let M be non empty MetrSpace, x be Point of TopSpaceMetr(M); cluster Balls(x) -> open x-quasi_basis; end; 3.2
To exemplify how redenitions of modes can be replaced by conditional registrations, let us consider the mode Element of D [Ban92], where D is a set containing only trees: definition let D be constituted-Trees non empty set; redefine mode Element of D -> Tree; end; Because the mode Tree [Ban90] is dened as an expandable mode: definition
mode Tree is non empty Tree-like set; end;
2In fact, there is another way to dene new types structures, but it is not relevant to the topic. the redenition can be replaced by the conditional registration: registration let D be constituted-Trees non empty set; cluster -> non empty Tree-like for Element of D; end; 3.3
To detect all cases in the Mizar Mathematical Library when redenitions of functors and modes could be replaced by corresponding registration, a special tool has been implemented by the author of the paper. In the Mizar Version 8.1.05 working with the MML Version 5.37.1267, 89 possible replacements of redenitions were found. 3 A revision [Ala11, Gra07, Pak14] of the MML was proposed to the Library Committee. [Try97] Trybulec, A.: Baire spaces, Sober spaces. Formalized Mathematics 6(2), 289294 (1997), http://fm. mizar.org/1997-6/pdf6-2/yellow_8.pdf