%\documentstyle[a4]{article} \documentclass{article} \usepackage{a4} \title{\bf Mizar: An Impression} \author{Freek Wiedijk\\ Nijmegen University\\ {\tt }} \date{} \begin{document} \maketitle \begin{abstract} \noindent This note presents an introduction to the Mizar system, followed by a brief comparison between Mizar and Coq. Appended are a Mizar grammar and an annotated example of a complete Mizar article. \end{abstract} \section{What It Is} Mizar is a system for representing mathematical proof in a computer such that a program can check the correctness. It has been developed by Andrzej Trybulec and his team in Bialystok, Poland since about 1973. The Mizar language is quite close to the language of informal mathematics (`the mathematical vernacular'). Mizar is based on a ZF-like set theory with classical first order logic. Part of the Mizar project is the development of a large database of mathematics which currently numbers 587 `articles' taking 41 megabytes (even without the proofs it's 6 megabytes). A major project currently underway is the translation to Mizar (under direction of Grzegorz Bancerek) of a real mathematics book: `A Compendium of Continuous Lattices' \cite{gie:hof:kei:law:mis:sco:80}. Mizar has had a number of dialects. `Mizar MSE' (also called `baby Mizar') is a toy language not meant for real applications. The current implementation of the full Mizar language is called `PC Mizar'. It's written in Turbo/Borland Pascal and runs only under DOS/Windows. Functionally it's basically one program, `\verb|mizf|', that non-interactively checks a Mizar file for its correctness. The Mizar system doesn't have much documentation. The text that most resembles a manual% \footnote{An electronic version of this manual is available on the World Wide Web at the address {\tt }} is `An Outline of PC Mizar' by Micha{\l} Muzalewski \cite{muz:93}. A way to explore the Mizar language that works surprisingly well is to study the Mizar syntax (see appendix \ref{grammar} on page \pageref{grammar} for a context free grammar) and for specific constructions to search the Mizar library for examples. \section{Definitions} A Mizar article consists of an `\verb|environ|' header which indicates what other articles from the Mizar library it refers to, followed by a sequence of definitions and theorems. A definition has the general shape: \begin{verse} \verb|definition|\\ \verb| let |{\it arguments\/}\verb|;|\\ \verb| assume |{\it preconditions\/}\verb|;|\\ \verb| func |{\it pattern\/}\verb| -> |{\it type\/}\verb| means :|{\it label\/}\verb|: |{\it statement\/}\verb|;|\\ \verb| |{\it correctness proof\/}\\ \verb|end;| \end{verse} The {\it pattern\/} presents the way the operation is written (both normal function notation and operator notation are possible; and not all arguments need to be present in the pattern: Mizar supports implicit arguments). In the defining {\it statement\/} the defined object is referred to as `\verb|it|'. The correctness proof has to show existence and uniqueness of the defined object given the preconditions. A definition of the form: \begin{verse} \verb|func |{\it pattern\/}\verb| -> |{\it type\/}\verb| means :|{\it label\/}\verb|:|\\ \verb| it = |{\it expression\/}\verb|;| \end{verse} \noindent can be abbreviated as: \begin{verse} \verb|func |{\it pattern\/}\verb| -> |{\it type\/}\verb| equals :|{\it label\/}\verb|: |{\it expression\/}\verb|;| \end{verse} Here is an example of a definition, the definition of `\verb|log|' (from article `\verb|POWER|'): \begin{verse} \verb|reserve a,b for Real;|\\ \verb|definition|\\ \verb| let a,b;|\\ \verb| assume A1: a>0 & a<>1 and A2: b>0;|\\ \verb| func log(a,b) -> Real means|\\ \verb|:Def3: a to_power it = b;|\\ \verb| existence|\\ {\it 251 lines of existence proof omitted\/}\\ \verb| uniqueness by A1,Th57;|\\ \verb|end;| \end{verse} \noindent (The `\verb|reserve|' statement reserves variables for a certain type: the type of a reserved variable needn't be given. So because of the `\verb|reserve|' statement in the first line, the `\verb|let a,b|' means `\verb|let a,b be Real|'.) And here is the definition of subtraction (from `\verb|REAL_1|'): \begin{verse} \verb|reserve x,y for Real;|\\ \verb|definition|\\ \verb| let x,y;|\\ \verb| func x-y -> Real equals :Def3: x+(-y);|\\ \verb| correctness;|\\ \verb|end;| \end{verse} \noindent (The `\verb|correctness|' at the end is an abbreviation of all elements of the correctness proof that are left to be proved: for a definition with `\verb|means|' these are `\verb|existence|' and `\verb|uniqueness|'; and for a definition with `\verb|equals|' it's `{\tt co\-her\-ence}', which says that the object has the correct type. In this example correctness is obvious, so there's no `\verb|by|' justification needed.) Apart from `\verb|func|' definitions for functions, Mizar has `\verb|pred|' definitions for predicates and `\verb|mode|' and `\verb|attr|' definitions for types (for an explanation of Mizar types, see section \ref{types} below). These are syntactically rather similar to the `\verb|func|' definitions and will not be explained in detail. In the definition of functions and predicates synonyms and antonyms can be given and properties like commutativity, symmetry, reflexivity and irreflexivity can be indicated. The Mizar system will magically `know' about these things, and variations on the same expression will behave like they are merely syntactic variants. For instance because the definition of $\leq$ (in `\verb|ARYTM|') is: \begin{verse} \verb|definition|\\ \verb| let x,y be Element of REAL;|\\ \verb| pred x |$\leq$\verb| y means|\\ {\it 6 lines of definition\/}\\ {\it 89 lines of correctness proof\/}\\ \verb| synonym y |$\geq$\verb| x;|\\ \verb| antonym y < x;|\\ \verb| antonym x > y;|\\ \verb|end;| \end{verse} \noindent it doesn't matter whether one writes \verb|x < y| or \verb|y > x|. Also it means that theorems about \verb|<| often also are usable (probably with a contraposition of an implication) to prove statements about $\geq$. \section{Theorems} The major part of a Mizar article consists of theorems (just like the major part of a computer program source consists of procedures/functions). A theorem has the shape: \begin{verse} \verb|theorem |{\it label\/}\verb|: |{\it statement\/}\\ \verb|proof|\\ \verb| |{\it proof steps\/}\\ \verb|end;| \end{verse} An example of a theorem (from article `\verb|IRRAT_1|'): \begin{verse} \verb|theorem T2:|\\ \verb| ex x, y st x is irrational & y is irrational &|\\ \verb| x.^.y is rational|\\ \verb|proof|\\ \verb| set w = |$\surd$\verb|2;|\\ \verb| H1: w is irrational by INT_2:44,T1;|\\ \verb| w>0 by AXIOMS:22,SQUARE_1:84;|\\ \verb| then (w.^.w).^.w = w.^.(w|$\bullet$\verb|w) by POWER:38|\\ \verb| .= w.^.(w|${}^2$\verb|) by SQUARE_1:58|\\ \verb| .= w.^.2 by SQUARE_1:88|\\ \verb| .= w|${}^2$\verb| by POWER:53|\\ \verb| .= 2 by SQUARE_1:88;|\\ \verb| then H2: (w.^.w).^.w is rational by RAT_1:8;|\\ \verb| per cases;|\\ \verb| suppose H3: w.^.w is rational;|\\ \verb| take w, w;|\\ \verb| thus thesis by H1,H3;|\\ \verb| suppose H4: w.^.w is irrational;|\\ \verb| take w.^.w, w;|\\ \verb| thus thesis by H1,H2,H4;|\\ \verb|end;| \end{verse} (Note that Mizar uses `high ASCII' characters, like `$\surd$', `$\bullet$' and `${}^2$' which in the DOS character set have ASCII codes 251, 249 and 253.) Various elements in this example will be discussed below. Mizar statements are those of the language of first order logic (using the keywords `\verb|contradiction|', `\verb|not|', `\verb|&|', `\verb|or|', `\verb|implies|', `\verb|iff|', `{\tt for }{\ldots} {\tt holds}' and `{\tt ex }{\ldots} {\tt st}'). The atomic formulas of this language either are instances of predicates (often written as an infix operator, with `\verb|=|' being one of the most important), or statements stating that an expression `\verb|is|' a type or adjective. The only slight deviation from this is that a combination of a universal quantification and an implication is usually not written as: \begin{verse} \verb|for |{\it variable\/}\verb| holds (|{\it statement\/}\verb| implies |{\it statement\/}\verb|)| \end{verse} \noindent but as: \begin{verse} \verb|for |{\it variable\/}\verb| st |{\it statement\/}\verb| holds |{\it statement\/} \end{verse} A source of confusion might be that Mizar has both `\verb|&|' versus `\verb|and|' and `\verb|st|' versus `{\tt such that}'. The first variants are syntax of first order formulas, the second variants are keywords that are part of Mizar statements. Another `duplication' is that Mizar has defined `\verb|func|' functions (Mizar calls those defined operations `functors'), versus functions in the underlying set theory (sets of Kuratowski pairs). An application of the first kind of function is written \verb|f(x)| while that of the second kind is \verb|f.x| (with an infix dot operator). A third such `duplication' is between `{\tt x $\in$ X}' and `{\tt x is Element of X}'. The first is the primitive binary predicate from set theory, the second is a typing statement (saying that `\verb|x|' has type `{\tt Element of X}'). For each set, `{\tt Element of}' gives the type of its elements. For instance: `\verb|REAL|' is a set, but `\verb|Real|' which is defined to be `{\tt Element of REAL}' is a type. So it is `{\tt x $\in$ REAL}', but `{\tt x is Real}' or `{\tt x is Element of REAL}'. A Mizar proof consists of a list of proof steps. Such a proof step basically has the shape: \begin{verse} {\it label\/}\verb|: |{\it statement\/}\verb| by |{\it labels\/}\verb|;| \end{verse} For instance, an example of a Mizar proof step is: \begin{verse} \verb|H1: w is irrational by INT_2:44,T1;| \end{verse} Here the statement is `{\tt w is irrational}', it's labeled `\verb|H1|', and it's a consequence of the statements labeled `\verb|INT_2:44|' and `\verb|T1|', which are: \begin{verse} \verb|:: INT_2:44|\\ \verb| 2 is prime| \end{verse} \noindent (the 44th theorem from article `\verb|INT_2|') and: \begin{verse} \verb|T1: p is prime implies sqrt p is irrational| \end{verse} \noindent (which was proved earlier in the same file). A label in the list after the `\verb|by|' keyword either is a label from an earlier theorem or proof step in the same file, or it's a reference to a theorem from a different Mizar article. In the latter case it looks like: \begin{verse} {\it article name\/}\verb|:|{\it sequence number\/} \end{verse} \noindent (so while `local' references are by name, `outside' references are by number). One can look up these sequence numbers by browsing the `abstract' files of the library, which are the articles in which automatically proofs have been removed and sequence numbers have been inserted. Instead of referring to the label of the immediately preceding step, one may also prefix the proof step with the keyword `\verb|then|'. So: \begin{verse} \verb|A: |{\it statement\/}\verb| by |{\it labels\/}\verb|;|\\ \verb|B: |{\it next statement\/}\verb| by A,|{\it more labels\/}\verb|;| \end{verse} \noindent can be written as: \begin{verse} {\it statement\/}\verb| by |{\it labels\/}\verb|;|\\ \verb|then B: |{\it next statement\/}\verb| by |{\it more labels\/}\verb|;| \end{verse} Apart from these kind of steps (called `diffuse' reasoning steps) there are steps that relate to the statement that's being proved (`skeleton' steps). At each moment there is a `current' statement that has to be proved: the skeleton steps transform that statement. For instance suppose that the statement to be proved looks like: \begin{verse} \verb|A implies B & C| \end{verse} Then the following skeleton proves it, using the `\verb|assume|' and `\verb|thus|' skeleton steps: \begin{verse} \verb|assume |{\it label\/}\verb|: A;|\\ {\it diffuse steps\/}\\ \verb|thus B by |{\it labels\/}\verb|;|\\ {\it more diffuse steps\/}\\ \verb|thus C by |{\it labels\/}\verb|;| \end{verse} After the `\verb|assume|' step the statement to be proved has been reduced to \verb|B & C|. And after the first `\verb|thus|' it has become \verb|C|. The combination `{\tt then thus}' isn't syntactically correct: it is written as `\verb|hence|'. So `\verb|hence|' means that the statement follows from the previous step (`\verb|then|') and that it is part of what was to be proved (`\verb|thus|'). So at each moment in a Mizar proof there's a statement that's left to be proved. This statement may be referred to by the keyword `\verb|thesis|'. Often a proof or subproof ends with `{\tt hence thesis}' (the Mizar library contains this construction 36885 times). The `\verb|assume|' and `\verb|thus|' steps correspond in the system of natural deduction to implication introduction and conjunction introduction. Other skeleton steps are: \begin{itemize} \item{`\verb|let|'} for universal introduction: \begin{verse} \verb|let |{\it variable\/}\verb| be |{\it type\/}\verb|;| \end{verse} \item{`\verb|consider|'} for existential elimination: \begin{verse} \verb|consider |{\it variable\/}\verb| being |{\it type\/}\verb| such that |{\it properties\/}\\ \verb| by |{\it labels\/}\verb|;| \end{verse} \noindent (the statements referred to by the {\it labels\/} have to justify the appropriate existential statement) \item{`\verb|take|'} for existential introduction: \begin{verse} \verb|take |{\it expression\/}\verb|;| \end{verse} \item{`{\tt per cases}'} for disjunction elimination: \begin{verse} \verb|per cases by |{\it labels\/}\verb|;|\\ \verb|suppose |{\it label\/}\verb|: |{\it statement\/}\verb|;|\\ \verb| |{\it proof for the first case\/}\\ \verb|suppose |{\it label\/}\verb|: |{\it another statement\/}\verb|;|\\ \verb| |{\it proof for the second case\/}\\ {\it more cases\/} \end{verse} \end{itemize} Not all natural deduction rules have a Mizar skeleton step for a counterpart: some are handled as a diffuse step. In Mizar a proof can contain subproofs. The part of a proof step of the form: \begin{verse} {\it \ldots\/}\verb| by |{\it labels\/}\verb|;| \end{verse} \noindent is called its justification. It is not full first order provability, but some weaker variant that can be decided quickly (approximately: in only one of the premises universal quantors may be instantiated; on the other hand it's quite good at reasoning from type information, at applying equalities, and at deducing existential statements). This `\verb|by|' justification sometimes isn't sufficient: so a statement also may also be justified by a full proof in the form: \begin{verse} {\it label\/}\verb|: |{\it statement\/}\\ \verb|proof|\\ \verb| |{\it proof steps\/}\\ \verb|end;| \end{verse} Note that there is no semicolon after the {\it statement\/} (that semicolon would count for an `empty' justification). In the case that a full proof like this is given, the statement can be omitted with the `\verb|now| \ldots \verb|end|' construction: \begin{verse} {\it label\/}\verb|:|\\ \verb|now|\\ \verb| |{\it proof steps\/}\\ \verb|end;| \end{verse} In that case the statement that is proved (that the {\it label\/} refers to) is `calculated' from the proof. Mizar also has support for equational reasoning. One can write: \begin{verse} {\it label\/}\verb|: |{\it expression\/}\verb| = |{\it expression\/}\verb| by |{\it labels\/}\\ \verb| .= |{\it expression\/}\verb| by |{\it labels\/}\\ \verb| |{\it more steps\/}\\ \verb| .= |{\it expression\/}\verb| by |{\it labels\/}\verb|;| \end{verse} The transitivity of these equalities is handled automatically: the {\it label\/} will refer to the equality of the initial and final expressions. And Mizar supports higher order statements. When invoking such a `\verb|scheme|' its name is not put after the keyword `\verb|by|' but after the keyword `\verb|from|', and it takes arguments. These arguments are {\it not\/} the `higher order parameters' which are between braces in the definition of the scheme (those are determined automatically), but instead the `conditions' after the `\verb|provided|'. The \verb|scheme| for doing induction on natural numbers is defined (in article `\verb|NAT_1|') by: \begin{verse} \verb|scheme Ind { P[Nat] } :|\\ \verb| for k holds P[k]|\\ \verb|provided|\\ \verb| A1: P[0] and|\\ \verb| A2: for k st P[k] holds P[k+1]|\\ {\it 16 lines of proof omitted\/} \end{verse} \noindent (the square brackets mean that P is a predicate: functions are written with round brackets; even when such a parameter function is a constant those brackets have to be written). The `\verb|Ind|' scheme then is applied like: \begin{verse} {\it label\/}\verb|: |{\it statement\/}\verb| from Ind(|{\it label\/}\verb|,|{\it label\/}\verb|);| \end{verse} \noindent in which the two labels refer to the instances of the two `\verb|provided|' statements that this scheme needs (which of course are the base and induction step cases). \section{Syntax} Expressions in a Mizar text look rather mathematical. This is caused by two things: the Mizar library uses the high ASCII part of the DOS character set (which contains lots of `mathematical' symbols) and in Mizar-expressions various styles of operators are allowed (prefix, postfix, infix and `bracket-like'). The Mizar lexical syntax isn't fixed. In fact, a Mizar article generally consists of two files: the article file (with a name ending with `\verb|.miz|') and the vocabulary file (ending with `\verb|.voc|'; which has to be in a subdirectory called `\verb|dict|' in order for the system to be able to find it). This last kind of file presents lexical elements. It contains both the `identifiers' from the definitions as well as the operator symbols. Such a vocabulary file contains for each lexical element a line that starts with a capital letter giving the lexical category of the symbol (the symbols for functions, predicates, modes, etc. all have {\it different\/} lexical categories), then the symbol itself and then possibly a priority. So the Mizar library really consists of a number of articles together with a number of vocabularies. The articles can be browsed in source format, but the vocabularies are only present in `compiled' form. The program `{\tt findvoc -w}' is used to find out from which vocabulary a specific symbol comes. For instance the command: \begin{verse} \verb|findvoc -w .| \end{verse} \noindent has as output: \begin{verse} \verb|vocabulary: FUNC|\\ \verb|O. 100| \end{verse} \noindent which tells us that `\verb|.|' is an operator symbol (at the lexical level there's no difference between infix, prefix or postfix operators, so it can be used in all three ways) from the vocabulary `\verb|FUNC|' and that it has priority $100$ (if there are multiple definitions of a `\verb|.|' operator they {\it all\/} have this priority). For the analysis of the expression: \begin{verse} \verb|f.x| \end{verse} \noindent three aspects can be distinguished: the lexical analysis (there are three tokens: `\verb|f|', `\verb|.|' and `\verb|x|'), the way the expression has to be parsed (the pattern from: \begin{verse} \verb|reserve x for set;|\\ \verb|reserve f for Function;|\\ \verb|definition|\\ \verb| let f,x;|\\ \verb| func f.x -> set means|\\ \verb|:: FUNCT_1:def 4|\\ \verb| [x,it] |$\in$\verb| f if x |$\in$\verb| dom f otherwise it = 0;|\\ \verb|end;| \end{verse} \noindent is the one that applies here) and the `notion' that it refers to (the `meaning' of the `\verb|.|' operator). These three aspects correspond exactly to the `\verb|vocabulary|', `\verb|notation|' and `\verb|constructors|' directives in the `\verb|environ|' header of an article. So in order to be able to process this `\verb|f.x|' expression correctly, the directives: \begin{verse} \verb|vocabulary FUNC;|\\ \verb|notation FUNCT_1;|\\ \verb|constructors FUNCT_1;| \end{verse} \noindent have to be present. Note that, although often the names of a vocabulary and the article it belongs to are identical, this need not be the case (here it's \verb|FUNC| versus \verb|FUNCT_1|): the `name spaces' of article names and vocabulary names are separate. Although it's quite hard to get the `\verb|environ|' header of an article right, these three directives are the ones that are most difficult to understand. The `\verb|theorems|', `\verb|schemes|' and `\verb|clusters|' directives are straightforward: in order to be able to use a theorem, scheme or cluster from an article, the name of that article has to be present in the appropriate directive. The `\verb|definitions|' directive is {\it only\/} about definitional expansion (what in type theory is called `delta reduction'). This directive says that the Mizar system is allowed to `unfold' all definitions from the articles that are listed. The theorems (with `\verb|def|' in front of the number) that stem from definitions are {\it theorems\/}, and the relevant directive for them is the `\verb|theorems|' directive. The `\verb|definitions|' directive is used rarely. The `\verb|requirements|' directive currently has only one possible instance: \begin{verse} \verb|requirements ARYTM;| \end{verse} It means that the Mizar system will `know' about natural numbers and about some identities and inequalities between them. For instance the inequality \begin{verse} \verb|1<>0;| \end{verse} \noindent doesn't need any justification when the \verb|ARYTM| requirement is present. A Mizar operator can take more than two arguments, but in that case brackets have to be around them and commas in between. So legal postfix operators are: \begin{verse} \verb|x f|\\ \verb|(x) f|\\ \verb|(x,y) f|\\ {\it \ldots\/} \end{verse} \noindent and for instance a legal infix operator is: \begin{verse} \verb|(x,y) f (z,v,w)| \end{verse} Note that the `ordinary' function application notation fits this para\-digm. Function identifiers and operator symbols have type `\verb|O|' in a vocabulary file. In Mizar also bracket-like notation is allowed: for this the vocabulary types `\verb|K|' and `\verb|L|' are present. Because `\verb|<*|' has type `\verb|K|' and `\verb|*>|' has type `\verb|L|' (both from vocabulary `\verb|FINSEQ|'), the expression: \begin{verse} \verb|<* x *>| \end{verse} \noindent is a legal pattern (it denotes a one element finite sequence). \section{Types}\label{types} Although the semantics of Mizar is untyped set theory (the axioms of Mizar are the ZF axioms plus a rather strong axiom -- which implies the axiom of choice -- about the existence of arbitrarily large unreachable cardinals), the language itself is typed. But the types are a property of the expressions of the language, not of the objects (the sets) which those expressions refer to, so the language is not based on `type theory'. Types are used to disambiguate expressions (operators can be overloaded and are determined by the types of their arguments) and for reasoning. Mizar typings are either written as: \begin{verse} {\it variable\/}\verb| be |{\it type\/} \end{verse} \noindent or as: \begin{verse} {\it variable\/}\verb| being |{\it type\/} \end{verse} \noindent (in a `\verb|let|' one probably would use the first and in a `\verb|for|' one would use the second: but both variants may be used everywhere). Mizar types are built from `modes' and `attributes'. A Mizar type is an instance of a mode (which is a parametrised type), possibly prefixed with a number of adjectives (an adjective is an attribute or the negation of an attribute). For instance, in the type: \begin{verse} \verb|non empty Subset of NAT| \end{verse} \noindent the mode `\verb|Subset|' is applied to the expression `\verb|NAT|' (which denotes the set of natural numbers) giving the type `{\tt Subset of NAT}'. To this type then the adjective `{\tt non empty}' has been added, which is the negation of the attribute `\verb|empty|'. Every Mizar type has an ancestor type. This leads to a tree-like type hierarchy of which the root type is `\verb|Any|' (or its synonym `\verb|set|'). At every node of this tree there is a `Boolean algebra'-like structure given by the adjectives. The Mizar system knows how to `widen' types following this structure. In Mizar it's possible to give an expression some explicit type. For this there is the `\verb|reconsider|' construction, which is a variant of the `\verb|set|' statement. The way to locally name an expression in Mizar is: \begin{verse} \verb|set |{\it variable\/}\verb| = |{\it expression\/}\verb|;| \end{verse} After this, {\it variable\/} behaves like {\it expression\/} has been substituted for it everywhere. A `\verb|reconsider|' is like that, only then the {\it expression\/} gets a different type. It looks like: \begin{verse} \verb|reconsider |{\it variable\/}\verb| = |{\it expression\/}\verb| as |{\it type\/}\\ \verb| by |{\it labels\/}\verb|;| \end{verse} (Note that the `\verb|consider|' and `\verb|reconsider|' statements are not related: the first uses an existential statement to find a new object with some properties, the second `\verb|casts|' an already known object given by an expression to some type.) The type machinery of Mizar is rather well developed. In particular Mizar has so-called `clusters' to be able to automatically deduce extra type information: clusters allow the Mizar system to manipulate sets of adjectives. There are three kind of cluster definitions: the first kind states that some combination of adjectives gives a non-empty type (this needs to be known to the system, because Mizar types all have to be provably non-empty), the second kind tells that some combination of adjectives implies other adjectives, and the third kind tells that an expression of some shape has some adjectives. An example of the first kind of cluster (from article `\verb|HIDDEN|') is: \begin{verse} \verb|definition|\\ \verb| cluster non empty set;|\\ \verb|end;| \end{verse} \noindent (there's no proof because `\verb|HIDDEN|' and `\verb|TARSKI|' are the two `special' articles which supply the axiomatics of Mizar). It states that the type `{\tt non empty set}' is inhabited. If this cluster weren't known, something like: \begin{verse} \verb|let X be non empty set;| \end{verse} \noindent wouldn't be allowed, because in that case the system wouldn't know that `{\tt non empty set}' is a properly non-empty type. An example of the second kind of cluster statement (from `\verb|BINTREE1|') is: \begin{verse} \verb|definition|\\ \verb| cluster binary -> finite-order Tree;|\\ {\it 28 lines of proof omitted\/}\\ \verb|end;| \end{verse} This says that every expression that has type `{\tt binary Tree}' has the adjective `\verb|finite-order|' as well (so it really has the more informative type `{\tt binary finite-order Tree}'). A third kind of cluster (from `\verb|ABIAN|'): \begin{verse} \verb|definition|\\ \verb| let i be even Integer;|\\ \verb| cluster i+1 -> odd;|\\ {\it 5 lines of proof omitted\/}\\ \verb|end;| \end{verse} This last kind of cluster is very powerful, because lots of properties of expressions can be derived automatically with it, but it sometimes significantly slows down the system. Mizar has the `\verb|redefine|' statement, which means that an operation can have multiple definitions in which all but the first one have a `\verb|redefine|' keyword added. Those redefinitions may be underspecified (all other information is copied from the original definition), they may be defined on a smaller set of arguments, but they do have to be proved `compatible' with the original definition. This can be used to give the same operation multiple types. For instance because of (from `\verb|NAT_1|'): \begin{verse} \verb|reserve k,n for Nat;|\\ \verb|definition|\\ \verb| let n,k;|\\ \verb| redefine func n+k -> Nat;|\\ {\it 18 lines of proof omitted\/}\\ \verb|end;| \end{verse} \noindent the Mizar system knows that the sum of two natural numbers will be a natural number (because the `redefined' version of the operation is syntactically selected when the arguments are natural numbers: for that the articles in the `\verb|notation|' directive have to be in the proper order) even although the addition operation originally was defined for real numbers (and in that definition has type \verb|Real|). But because of the `\verb|redefine|', although the redefinition has type \verb|Nat|, all existing theorems about the original operation of type \verb|Real| still apply for it as well. \section{Semantics} The semantics of Mizar is fairly straightforward. Mizar is about ZF style set theory with first order logic. However, there is the subtlety of undefined expressions. The semantics of Mizar `solves' the problem of undefined expressions in a way that leads to some unexpected properties. Firstly it means that types are {\it not\/} only `syntactic sugar' coding predicates (instead they `mean' something on the level of the semantics). And secondly it means that the axiom of choice is provable from the way Mizar implements first order logic. A Mizar `\verb|func|' operation can have preconditions. The proof that the operation is well defined uses these preconditions. However, when {\it applying\/} such an operation there is no need to prove that the preconditions hold: they may be false. So, while for instance a precondition of division is that the denominator has to be unequal to zero, one is allowed to write expressions like \verb|1/0|. The semantics of Mizar doesn't tell anything about the result of applying an operation for which the preconditions fail. If the preconditions are true, the defining statement from the definition is guaranteed to hold; but when the preconditions are false, you don't know anything. So \verb|1/0| is an unknown object. A different way of looking at this is that the function that maps Mizar expressions to their meaning isn't unique: on `undefined' expressions it can take any value. The one exception to this rule is that the {\it type\/} of an undefined expression still has to apply. So, although we don't know what \verb|1/0| is, we {\it do\/} know that it has to be a real number (as the division operation has type `\verb|Real|'). So the defining statement (which is a predicate on the object that's being defined) is not relevant when the preconditions fail, but the type is. This difference in semantical treatment of unary predicates and types coding those predicates is clear from the following example. Let `{\tt some\-thing}' be some (irrelevant) statement. Then write: \begin{verse} \verb|reserve X for set;| \end{verse} \begin{verse} \verb|definition|\\ \verb| let X;|\\ \verb| assume A: contradiction;|\\ \verb| func choice(X) -> Element of X means|\\ \verb|:Def_choice: something;|\\ \verb| correctness by A;|\\ \verb|end;| \end{verse} \begin{verse} \verb|definition|\\ \verb| let X;|\\ \verb| assume A: contradiction;|\\ \verb| func choice1(X) means|\\ \verb|:Def_choice1: it is Element of X & something;|\\ \verb| correctness by A;|\\ \verb|end;| \end{verse} (Because the precondition is `\verb|contradiction|' of course these operations are well defined whenever the preconditions hold.) The `\verb|choice|' and `\verb|choice1|' functions seem minor variations of each other. But because of the way the semantics treats undefined expressions we can prove: \begin{verse} \verb|theorem AC:|\\ \verb| choice(X) is Element of X;| \end{verse} \noindent but we {\it can't\/} prove: \begin{verse} \verb|theorem AC1:|\\ \verb| choice1(X) is Element of X|\\ \verb|proof|\\ \verb| thus thesis by Def_choice1;|\\ \verb|::> *4|\\ \verb|end;| \end{verse} \noindent (The \verb|*4| line is the error message that the `\verb|mizf|' checker inserts in the file, number \verb|4| meaning that the `\verb|by|' inference doesn't hold. It is explained by the Mizar checker as `{\tt This inference is not accepted}'.) Note that theorem `\verb|AC|' gives a `uniform' axiom of choice. (The axiom of choice also follows from Mizar's set-theoretical axioms, but it clearly already is `hard wired' in the way Mizar treats first order logic.) The meaning of the type `{\tt Element of X}' when \verb|X| is an empty set, is some unknown but non-empty class (all Mizar types are non-empty). In Mizar the statement: \begin{verse} \verb|ex x st x is Element of |$\emptyset$\\ \end{verse} \noindent (stating that there exists some {\tt `Element of $\emptyset$'}) is provable (`{\tt consider x be\-ing El\-e\-ment of $\emptyset$; take x;}'). But the seemingly contradictory statement: \begin{verse} \verb|not ex x st x |$\in$\verb| |$\emptyset$ \end{verse} \noindent is provable as well, because it's a theorem of ZF. (This does {\it not\/} mean that the semantics of Mizar isn't sound, but just that `{\tt Element of}' has a strange interpretation.) One would expect the definition of the `\verb|Element|' mode (in `\verb|HIDDEN|') to have precondition `{\tt X is non empty}', but this is not the case. In order to `build' mathematical structures, Mizar also has `\verb|struct|' types. They are defined like: \begin{verse} \verb|struct(|{\it ancestor struct\/}\verb|) |{\it struct name\/}\verb| (#|\\ \verb| |{\it field name\/}\verb| -> |{\it type\/}\verb|,|\\ \verb| |{\it field name\/}\verb| -> |{\it type\/}\verb|,|\\ \verb| |{\it more fields\/}\\ \verb| |{\it field name\/}\verb| -> |{\it type\/}\\ \verb|#)| \end{verse} \noindent (The `\verb|(#|' and `\verb|#)|' brackets may be replaced with high ASCII characters looking like `\verb|<|$\!$\verb|<|' and `\verb|>|$\!$\verb|>|': in fact this notation is the more common one.) An object of such a \verb|struct| type is then written like: \begin{verse} {\it struct name\/}\verb| (# |{\it value\/}\verb|,|{\it value\/}\verb|, |{\it \ldots\/}\verb| |{\it value\/}\verb| #)| \end{verse} \noindent and a field is selected from a \verb|struct| by: \begin{verse} \verb|the |{\it field name\/}\verb| of |{\it struct expression\/} \end{verse} As an example of a \verb|struct|, here is the way topological spaces are introduced in Mizar (from articles `\verb|STRUCT_0|' and `\verb|PRE_TOPC|'): \begin{verse} \verb|struct 1-sorted (#|\\ \verb| carrier -> set|\\ \verb|#);| \end{verse} \begin{verse} \verb|struct(1-sorted) TopStruct (#|\\ \verb| carrier -> set,|\\ \verb| topology -> Subset-Family of the carrier|\\ \verb|#);| \end{verse} \begin{verse} \verb|definition|\\ \verb| let IT be TopStruct;|\\ \verb| attr IT is TopSpace-like means|\\ \verb| the carrier of IT |$\in$\verb| the topology of IT &|\\ \verb| (for a being Subset-Family of the carrier of IT|\\ \verb| st a c= the topology of IT|\\ \verb| holds union a |$\in$\verb| the topology of IT) &|\\ \verb| (for a,b being Subset of the carrier of IT st|\\ \verb| a |$\in$\verb| the topology of IT & b |$\in$\verb| the topology of IT|\\ \verb| holds a |$\cap$\verb| b |$\in$\verb| the topology of IT); |\\ \verb|end;| \end{verse} \begin{verse} \verb|definition|\\ \verb| mode TopSpace is TopSpace-like TopStruct;|\\ \verb|end;| \end{verse} The {\it specific\/} semantics of structs in terms of the underlying set theory is not really interesting: some ad hoc coding will do the job (choosing some set for the field names and interpreting the \verb|struct| as a partial function from that set will work). Because of the way \verb|struct| types widen, an object will also be of a \verb|struct| type if it has {\it more\/} fields than is required by the definition. The adjective `\verb|strict|' means that such extra fields should be absent. \section{Comparison To Coq} The Mizar system is quite dissimilar to systems from the LCF tradition like Coq. We here will compare Mizar specifically to Coq, but a similar comparison holds to other LCF-like systems like HOL, Nuprl, Isabelle, etc. The most striking difference between Mizar and Coq is that Mizar is a batch checker which checks a whole file at a time (the `\verb|@proof|' keyword gives some control in this respect by allowing one to suppress the checking of specific proofs), while Coq is an interactive system (this is similar to the difference in spirit between compiled and interpreted programming languages). One of the places that this shows is in the readability of the formalizations: a Coq file is just a long list of `commands', so it has a linear structure and the commands aren't designed for readability, while a Mizar text has much more structure and is quite accessible without having to `run' the file. Another difference is that Mizar doesn't have `proof objects': the system doesn't reduce its correctness to the correctness of a small `kernel' that only knows about a few primitives. There also is a difference in the kind of logic in the two systems: Coq's kernel is based on `type theory' which naturally has a constructive logic, while Mizar is very much a classical system. The Mizar project has {\it more\/} automation than Coq and it has {\it less\/} automation. The step used most in Mizar is the `\verb|by|' inference; in Coq the common tactics are more elementary than that. The `\verb|by|' inference knows how to reason with types, it is able to use equalities and it's able to logically combine the information from many statements (the maximum: 22 statements in `\verb|GENEALG1|'). While it's not full first order inference its power is close to the kind of reasoning steps a human would take (the Mizar system has the `\verb|relinfer|' program to eliminate superfluous steps, and running it shows that `\verb|by|' is more powerful than one tends to expect). So for the majority of the steps Mizar is more powerful than Coq. On the other hand, the Coq system isn't `closed', it can be extended with arbitrarily powerful `tactics'. These tactics, like `\verb|Omega|' and `\verb|Ring|', are able to solve involved domain specific tasks and don't have a Mizar counterpart. Also, the Coq system is able to `reflect' on algorithms: it's able to state an algorithm {\it inside\/} the system, to prove that it is correct, and then to execute it, making it possible to extend the system `from within'. This also is a reason that Coq is, in a sense, more powerful than Mizar. Another difference between Mizar and Coq is that Coq mainly reasons backwards from the statement that is to be proved, while Mizar reasons forwards. Basically the Mizar `skeleton' steps correspond to the Coq tactics and reduce the statement that's to be proved, while the `diffuse' steps reason forward from already known statements. Most of the steps in a Mizar proof are diffuse steps. A difference that's not so much a difference between the languages or systems, as well as a difference between the projects, is that the Mizar project has given a big priority to the development of a large and organized library. The Mizar system intentionally makes it hard to create projects of more than a few files (it is possible, but the system gets slow), stimulating Mizar users to submit their work for integration into the Mizar library. And the Mizar library is continuously being reorganized and changed by the Mizar group (the `library committee'), turning it into a structured and consistent whole. This wouldn't be possible if they didn't `own' the files. Here's an example of a change that has been made to the Mizar library at some time. In the Mizar library the real numbers are constructed from the rational numbers as Dedekind cuts. But in the construction of the set `\verb|REAL|' it `cuts out' the copy of the rationals and `glues in' the `original' rationals (similarly the integers are glued inside the rationals and the natural numbers glued inside the integers). That way the natural numbers are a subset of the reals but also the natural numbers are the {\it natural\/} natural numbers, i.e., the finite ordinals. So the real number $0$ is the natural number $0$ is the empty set. This cutting-and-pasting of sets of numbers is a `hack', but it also is quite nice. The complex numbers don't contain the real numbers in this fashion yet, but a change like this `to put the real numbers inside the complex numbers' has been planned. So the Mizar library is significantly more well developed than the Coq library. For instance it already contains a full construction of the real numbers (the Coq library only has the real numbers axiomatically) with lots of properties proved. (On the other hand, the Mizar library currently doesn't yet contain a definition of the rather elementary notion of `polynomial' so it's not {\it that\/} rich yet.) Also Mizar is much more mathematical than Coq. Mizar is primarily about abstract mathematics while Coq has much more a focus on topics from computer science like proving functional programs correct. Yet another difference: Coq is much more `mainstream science' than Mizar. Mizar is an old-fashioned system that not many people know (if we take the fair assumption that every Mizar user has written an article for the Mizar library then there are 117 people in the world knowing Mizar), there is hardly any documentation about it and it doesn't run on the usual platform for this kind of system (which is a Sun running Unix). On the other hand Coq actively follows the theoretical developments from the type theory community, it's well known, has many users, is well documented and is available for all major platforms. John Harrrison has written a `Mizar mode' for HOL. To create a Mizar interface for a LCF style prover like HOL or Coq, one has to write a tactic that is able to do `\verb|by|' inference (Harrison decided to implement full first order provability, which is more powerful but less efficient), and one has to write a parser for the Mizar syntax. Because the semantics and the type systems of Mizar and Coq are not the same, there are differences there to be bridged too. Having a system that combines the strengths of Mizar and Coq will be nice (it will be a `Mizar' that has proof objects) but doing it by `enhancing' Coq will be rather inelegant (there will be duplications of functionality) and inefficient. And really, from the point of view of the mathematically inclined user Mizar already contains everything that one needs. \begin{thebibliography}{1} \bibitem{gie:hof:kei:law:mis:sco:80} G.~Gierz, K.H. Hofmann, K.~Keimel, J.D. Lawson, M.~Mislove, and D.S. Scott. \newblock {\em A Compendium of Continuous Lattices}. \newblock Springer-Verlag, Berlin, Heidelberg, New York, 1980. \bibitem{kot:mad:kor:92} J.~Kotowicz, B.~Madras, and M.~Korolkiewicz. \newblock Basic notation of universal algebra. \newblock {\em Journal of Formalized Mathematics}, 4, 1992. \bibitem{muz:93} M.~Muzalewski. \newblock {\em An Outline of PC Mizar}. \newblock Fondation Philippe le Hodey, Brussels, 1993. \end{thebibliography} \appendix \section{How To Run Mizar} Select three directories: \begin{itemize} \item {\it distdir\/}: to unzip the Mizar distribution in \item {\it mizardir\/}: for the installed Mizar system \item {\it workdir\/}: for your articles \end{itemize} \noindent The recommended choice for {\it mizardir\/} is `{\tt C:\verb|\|MIZAR}', although everything works fine if you put it elsewhere. To install the Mizar system, get the zipped installation files from: \begin{verse} {\tt } \end{verse} \noindent (the `{\it version\/}' of the system described in this note is `\verb|5-3.07|'). Unzip them all inside {\it distdir\/}. Then run the \verb|install| command: \begin{verse} {\tt {\it distdir\/}\verb|\|install {\it distdir\/}\verb|\| {\it mizardir\/}} \end{verse} \noindent This installs everything apart from the sources of the Mizar library in `{\tt {\it mizar\-dir\/}\verb|\|MML}'. These sources are really not very important (not even for reference to the library: the abstracts in `{\tt {\it mizardir\/}\verb|\|ABSTR}' are much more suitable for that). To unpack the sources of the Mizar library too, run the `{\tt FM{\it number\/}.EXE}' files from {\it distdir\/} inside `{\tt {\it mizardir\/}\verb|\|MML}'. Now add: \begin{verse} {\tt set mizfiles={\it mizardir\/}} \end{verse} \noindent to the appropriate `{\tt AUTOEXEC.BAT}' file, add {\it mizardir\/} to the DOS search \verb|PATH|, and the installation will be complete. To write an article create two subdirectories: \begin{itemize} \item {\tt {\it workdir\/}\verb|\|TEXT} \item {\tt {\it workdir\/}\verb|\|DICT} \end{itemize} Supposing the name of the article you'll be going to work on is `\verb|FOO|', then create: \begin{itemize} \item {\tt {\it workdir\/}\verb|\|TEXT\verb|\|FOO.MIZ} \item {\tt {\it workdir\/}\verb|\|DICT\verb|\|FOO.VOC} \end{itemize} which are your article and vocabulary files. To check the article for correctness, \verb|cd| to {\it workdir\/} and run the command: \begin{verse} \verb|mizf text\foo| \end{verse} \noindent (the \verb|mizf| checker will add the suffix `\verb|.miz|' by itself). This will check the file, and will put the error messages {\it inside\/} the checked file (so it might be necessary to close the file in the editor before running the `\verb|mizf|' command). \section{Grammar}\label{grammar} \begin{flushleft} {\it Mizar-Article\/} =\\* \quad `\verb|environ|'\\* \quad\quad \{ `\verb|vocabulary|' {\it File-Name-List\/} `\verb|;|' $|$\\* \quad\quad\quad ( `\verb|notation|' $|$\\* \quad\quad\quad\quad `\verb|constructors|' $|$\\* \quad\quad\quad\quad `\verb|clusters|' $|$\\* \quad\quad\quad\quad `\verb|definitions|' $|$\\* \quad\quad\quad\quad `\verb|theorems|' $|$\\* \quad\quad\quad\quad `\verb|schemes|' ) {\it File-Name-List\/} `\verb|;|' $|$\\* \quad\quad\quad `\verb|requirements|' {\it File-Name-List\/} `\verb|;|' \}\\* \quad ( `\verb|begin|' \{ {\it Text-Item\/} \} ) \{ \ldots \} .\smallskip {\it Text-Item\/} =\\* \quad `\verb|reserve|' {\it Identifier-List\/} `\verb|for|' {\it Type-Expression-List\/} `\verb|;|' $|$\\ \quad `\verb|definition|'\\* \quad\quad \{ {\it Definition-Item\/} \}\\* \quad\quad [ `\verb|redefine|' \{ {\it Definition-Item\/} \} ]\\* \quad\quad `\verb|end|' `\verb|;|' $|$\\ \quad {\it Structure-Definition\/} $|$\\ \quad `\verb|theorem|' {\it Proposition\/} {\it Justification\/} `\verb|;|' $|$\\ \quad [ `\verb|scheme|' ] {\it Identifier\/}\\* \quad\quad `\verb|{|' ( {\it Identifier-List\/} `\verb|[|' {\it Type-Expression-List\/} `\verb|]|' $|$\\* \quad\quad\quad\quad {\it Identifier-List\/} `\verb|(|' {\it Type-Expression-List\/} `\verb|)|' `\verb|->|' {\it Type-Expression\/} )\\* \quad\quad\quad\quad \{ `\verb|,|' \ldots \} `\verb|}|'\\* \quad\quad `\verb|:|' {\it Formula-Expression\/}\\* \quad\quad [ `\verb|provided|' {\it Proposition\/} \{ `\verb|and|' \ldots \} ]\\* \quad\quad {\it Justification\/} `\verb|;|' $|$\\ \quad {\it Auxiliary-Item\/} $|$\\ \quad `\verb|canceled|' [ {\it Numeral\/} ] `\verb|;|' .\smallskip {\it Definition-Item\/} =\\* \quad {\it Assumption\/} $|$\\ \quad {\it Auxiliary-Item\/} $|$\\ \quad {\it Structure-Definition\/} $|$\\ \quad `\verb|mode|' \verb|M|{\it -Symbol\/} [ `\verb|of|' {\it Identifier-List\/} ]\\* \quad\quad ( [ `\verb|->|' {\it Type-Expression\/} ] [ `\verb|means|' {\it Definiens\/} ] `\verb|;|'\\* \quad\quad\quad\quad {\it Correctness-Conditions\/} $|$\\* \quad\quad\quad `\verb|is|' {\it Type-Expression\/} `\verb|;|' )\\* \quad\quad \{ `\verb|synonym|' \verb|M|{\it -Symbol\/} [ `\verb|of|' {\it Identifier-List\/} ] `\verb|;|' \} $|$\\ \quad `\verb|func|' {\it Functor-Pattern\/} [ `\verb|->|' {\it Type-Expression\/} ]\\* \quad\quad [ ( `\verb|means|' $|$ `\verb|equals|' ) {\it Definiens\/} ] `\verb|;|'\\* \quad\quad {\it Correctness-Conditions\/}\\* \quad\quad \{ `\verb|commutativity|' {\it Justification\/} `\verb|;|' \}\\* \quad\quad \{ `\verb|synonym|' {\it Functor-Pattern\/} `\verb|;|' \} $|$\\ \quad `\verb|pred|' {\it Predicate-Pattern\/} [ `\verb|means|' {\it Definiens\/} ] `\verb|;|'\\* \quad\quad {\it Correctness-Conditions\/}\\* \quad\quad \{ `\verb|symmetry|' {\it Justification\/} `\verb|;|' $|$\\* \quad\quad\quad `\verb|connectedness|' {\it Justification\/} `\verb|;|' $|$\\* \quad\quad\quad `\verb|reflexivity|' {\it Justification\/} `\verb|;|' $|$\\* \quad\quad\quad `\verb|irreflexivity|' {\it Justification\/} `\verb|;|' \}\\* \quad\quad \{ ( `\verb|synonym|' $|$ `\verb|antonym|' ) {\it Predicate-Pattern\/} `\verb|;|' \} $|$\\ \quad `\verb|attr|' {\it Identifier\/} `\verb|is|' \verb|V|{\it -Symbol\/} `\verb|means|' {\it Definiens\/} `\verb|;|'\\* \quad\quad [ {\it Correctness-Conditions\/} ]\\* \quad\quad \{ ( `\verb|synonym|' $|$ `\verb|antonym|' )\\* \quad\quad\quad ( {\it Identifier\/} `\verb|is|' \verb|V|{\it -Symbol\/} $|$ {\it Predicate-Pattern\/} ) `\verb|;|' \} $|$\\ \quad `\verb|canceled|' [ {\it Numeral\/} ] $|$\\ \quad `\verb|cluster|' {\it Adjective-Cluster\/} {\it Type-Expression\/} `\verb|;|' {\it Correctness-Conditions\/} $|$\\ \quad `\verb|cluster|' {\it Adjective-Cluster\/} `\verb|->|' {\it Adjective-Cluster\/} {\it Type-Expression\/} `\verb|;|'\\* \quad\quad {\it Correctness-Conditions\/} $|$\\ \quad `\verb|cluster|' {\it Term-Expression\/} `\verb|->|' {\it Adjective-Cluster\/} `\verb|;|'\\* \quad\quad {\it Correctness-Conditions\/} .\smallskip {\it Structure-Definition\/} =\\* \quad `\verb|struct|' [ `\verb|(|' {\it Type-Expression-List\/} `\verb|)|' ] \verb|G|{\it -Symbol\/} [ `\verb|over|' {\it Identifier-List\/} ]\\* \quad\quad `\verb|(#|' ( \verb|U|{\it -Symbol\/} \{ `\verb|,|' \ldots \} `\verb|->|' {\it Type-Expression\/} ) \{ `\verb|,|' \ldots \} `\verb|#)|' `\verb|;|' .\smallskip {\it Definiens\/} =\\* \quad [ `\verb|:|' {\it Identifier\/} `\verb|:|' ] ( {\it Formula-Expression\/} $|$ {\it Term-Expression\/} ) $|$\\ \quad [ `\verb|:|' {\it Identifier\/} `\verb|:|' ]\\* \quad\quad ( ( {\it Formula-Expression\/} $|$ {\it Term-Expression\/} ) `\verb|if|' {\it Formula-Expression\/} )\\* \quad\quad \{ `\verb|,|' \ldots \}\\* \quad\quad [ `\verb|otherwise|' ( {\it Formula-Expression\/} $|$ {\it Term-Expression\/} ) ] .\smallskip {\it Functor-Pattern\/} =\\* \quad [ {\it Functor-Loci\/} ] \verb|O|{\it -Symbol\/} [ {\it Functor-Loci\/} ] $|$\\ \quad \verb|K|{\it -Symbol\/} {\it Identifier-List\/} \verb|L|{\it -Symbol\/} .\smallskip {\it Functor-Loci\/} =\\* \quad {\it Identifier\/} $|$\\ \quad `\verb|(|' {\it Identifier-List\/} `\verb|)|' .\smallskip {\it Predicate-Pattern\/} = [ {\it Identifier-List\/} ] \verb|R|{\it -Symbol\/} [ {\it Identifier-List\/} ] .\smallskip {\it Correctness-Conditions\/} =\\* \quad \{ `\verb|existence|' {\it Justification\/} `\verb|;|' $|$\\* \quad\quad `\verb|uniqueness|' {\it Justification\/} `\verb|;|' $|$\\* \quad\quad `\verb|coherence|' {\it Justification\/} `\verb|;|' $|$\\* \quad\quad `\verb|compatibility|' {\it Justification\/} `\verb|;|' $|$\\* \quad\quad `\verb|consistency|' {\it Justification\/} `\verb|;|' \}\\* \quad [ `\verb|correctness|' {\it Justification\/} `\verb|;|' ] .\smallskip {\it Justification\/} =\\* \quad {\it Simple-Justification\/} $|$\\ \quad ( `\verb|proof|' $|$ `\verb|@proof|' ) {\it Reasoning\/} `\verb|end|' .\smallskip {\it Reasoning\/} =\\* \quad \{ {\it Reasoning-Item\/} \}\\* \quad\quad [ `\verb|per|' `\verb|cases|' {\it Simple-Justification\/} `\verb|;|'\\* \quad\quad ( ( `\verb|case|' ( {\it Proposition\/} $|$ {\it Conditions\/} ) `\verb|;|' \{ {\it Reasoning-Item\/} \} )\\* \quad\quad\quad\quad \{ \ldots \} $|$\\* \quad\quad\quad ( `\verb|suppose|' ( {\it Proposition\/} $|$ {\it Conditions\/} ) `\verb|;|' \{ {\it Reasoning-Item\/} \} )\\* \quad\quad\quad\quad \{ \ldots \} ) ] .\smallskip {\it Reasoning-Item\/} =\\* \quad {\it Auxiliary-Item\/} $|$\\ \quad {\it Assumption\/} $|$\\ \quad ( `\verb|thus|' $|$ `\verb|hence|' ) {\it Statement\/} $|$\\ \quad `\verb|take|' ( {\it Term-Expression\/} $|$ {\it Identifier\/} `\verb|=|' {\it Term-Expression\/} ) \{ `\verb|,|' \ldots \} `\verb|;|' .\smallskip {\it Auxiliary-Item\/} =\\* \quad [ `\verb|then|' ] {\it Statement\/} $|$\\ \quad `\verb|set|' ( {\it Identifier\/} `\verb|=|' {\it Term-Expression\/} ) \{ `\verb|,|' \ldots \} `\verb|;|' $|$\\ \quad `\verb|deffunc|' {\it Identifier\/} `\verb|(|' [ {\it Type-Expression-List\/} ] `\verb|)|' `\verb|=|' {\it Term-Expression\/} $|$\\ \quad `\verb|defpred|' {\it Identifier\/} `\verb|[|' [ {\it Type-Expression-List\/} ] `\verb|]|' `\verb|means|'\\* \quad\quad {\it Formula-Expression\/} .\smallskip {\it Assumption\/} =\\* \quad ( `\verb|let|' $|$ `\verb|given|' ) {\it Qualified-Variables\/} [ `\verb|such|' {\it Conditions\/} ] `\verb|;|' $|$\\ \quad `\verb|assume|' ( {\it Proposition\/} $|$ {\it Conditions\/} ) `\verb|;|' .\smallskip {\it Statement\/} =\\* \quad [ `\verb|then|' ]\\* \quad\quad ( {\it Proposition\/} {\it Justification\/} `\verb|;|' $|$\\* \quad\quad\quad `\verb|consider|' {\it Qualified-Variables\/} [ `\verb|such|' {\it Conditions\/} ]\\* \quad\quad\quad\quad {\it Simple-Justification\/} `\verb|;|' $|$\\* \quad\quad\quad `\verb|reconsider|'\\* \quad\quad\quad\quad ( {\it Identifier\/} `\verb|=|' {\it Term-Expression\/} $|$ {\it Identifier\/} ) \{ `\verb|,|' \ldots \}\\* \quad\quad\quad\quad `\verb|as|' {\it Type-Expression\/} {\it Simple-Justification\/} `\verb|;|' $|$\\* \quad\quad\quad {\it Term-Expression\/} `\verb|=|' {\it Term-Expression\/} {\it Simple-Justification\/}\\* \quad\quad\quad\quad `\verb|.=|' ( {\it Term-Expression\/} {\it Simple-Justification\/} ) \{ `\verb|.=|' \ldots \} ) $|$\\ \quad [ {\it Identifier\/} `\verb|:|' ] `\verb|now|' {\it Reasoning\/} `\verb|end|' `\verb|;|' .\smallskip {\it Simple-Justification\/} =\\* \quad [ `\verb|by|' {\it Reference\/} \{ `\verb|,|' \ldots \} ] $|$\\ \quad `\verb|from|' {\it Identifier\/} [ `\verb|(|' {\it Reference\/} \{ `\verb|,|' \ldots \} `\verb|)|' ] .\smallskip {\it Reference\/} =\\* \quad {\it Identifier\/} $|$\\ \quad {\it File-Name\/} `\verb|:|' ( {\it Numeral\/} $|$ `\verb|def|' {\it Numeral\/} ) \{ `\verb|,|' \ldots \} .\smallskip {\it Conditions\/} = `\verb|that|' {\it Proposition\/} \{ `\verb|and|' \ldots \} .\smallskip {\it Proposition\/} = [ {\it Identifier\/} `\verb|:|' ] {\it Formula-Expression\/} .\smallskip {\it Formula-Expression\/} =\\* \quad `\verb|(|' {\it Formula-Expression\/} `\verb|)|' $|$\\ \quad [ {\it Term-Expression-List\/} ] \verb|R|{\it -Symbol\/} [ {\it Term-Expression-List\/} ] $|$\\ \quad {\it Identifier\/} [ `\verb|[|' {\it Term-Expression-List\/} `\verb|]|' ] $|$\\ \quad {\it Term-Expression\/} `\verb|is|' \{ [ `\verb|non|' ] \verb|V|{\it -Symbol\/} \} $|$\\ \quad {\it Term-Expression\/} `\verb|is|' {\it Type-Expression\/} $|$\\ \quad {\it Quantified-Formula-Expression\/} $|$\\ \quad {\it Formula-Expression\/} `\verb|&|' {\it Formula-Expression\/} $|$\\ \quad {\it Formula-Expression\/} `\verb|or|' {\it Formula-Expression\/} $|$\\ \quad {\it Formula-Expression\/} `\verb|implies|' {\it Formula-Expression\/} $|$\\ \quad {\it Formula-Expression\/} `\verb|iff|' {\it Formula-Expression\/} $|$\\ \quad `\verb|not|' {\it Formula-Expression\/} $|$\\ \quad `\verb|contradiction|' $|$\\ \quad `\verb|thesis|' .\smallskip {\it Quantified-Formula-Expression\/} =\\* \quad `\verb|for|' {\it Qualified-Variables\/} [ `\verb|st|' {\it Formula-Expression\/} ]\\* \quad\quad ( `\verb|holds|' {\it Formula-Expression\/} $|$ {\it Quantified-Formula-Expression\/} ) $|$\\ \quad `\verb|ex|' {\it Qualified-Variables\/} `\verb|st|' {\it Formula-Expression\/} .\smallskip {\it Qualified-Variables\/} =\\* \quad {\it Identifier-List\/} $|$\\ \quad ( {\it Identifier-List\/} ( `\verb|being|' $|$ `\verb|be|' ) {\it Type-Expression\/} ) \{ `\verb|,|' \ldots \}\\* \quad\quad [ `\verb|,|' {\it Identifier-List\/} ] .\smallskip {\it Type-Expression\/} =\\* \quad `\verb|(|' {\it Type-Expression\/} `\verb|)|' $|$\\ \quad {\it Adjective-Cluster\/} \verb|M|{\it -Symbol\/} [ `\verb|of|' {\it Term-Expression-List\/} ] $|$\\ \quad {\it Adjective-Cluster\/} \verb|G|{\it -Symbol\/} [ `\verb|over|' {\it Term-Expression-List\/} ] .\smallskip {\it Adjective-Cluster\/} = \{ [ `\verb|non|' ] \verb|V|{\it -Symbol\/} \} .\smallskip {\it Term-Expression\/} =\\* \quad `\verb|(|' {\it Term-Expression\/} `\verb|)|' $|$\\ \quad [ {\it Arguments\/} ] \verb|O|{\it -Symbol\/} [ {\it Arguments\/} ] $|$\\ \quad \verb|K|{\it -Symbol\/} {\it Term-Expression-List\/} \verb|L|{\it -Symbol\/} $|$\\ \quad {\it Identifier\/} `\verb|(|' [ {\it Term-Expression-List\/} ] `\verb|)|' $|$\\ \quad \verb|G|{\it -Symbol\/} `\verb|(#|' {\it Term-Expression-List\/} `\verb|#)|' $|$\\ \quad {\it Identifier\/} $|$\\ \quad `\verb|{|' {\it Term-Expression\/}\\* \quad\quad\quad [ ( `\verb|where|' {\it Identifier-List\/} `\verb|is|' {\it Type-Expression\/} ) \{ `\verb|,|' \ldots \} ]\\* \quad\quad\quad `\verb|:|' {\it Formula-Expression\/} `\verb|}|' $|$\\ \quad {\it Numeral\/} $|$\\ \quad {\it Term-Expression\/} `\verb|qua|' {\it Type-Expression\/} $|$\\ \quad `\verb|the|' \verb|U|{\it -Symbol\/} `\verb|of|' {\it Term-Expression\/} $|$\\ \quad `\verb|the|' \verb|U|{\it -Symbol\/} $|$\\ \quad `\verb|$1|' $|$ `\verb|$2|' $|$ `\verb|$3|' $|$ `\verb|$4|' $|$ `\verb|$5|' $|$ `\verb|$6|' $|$ `\verb|$7|' $|$ `\verb|$8|' $|$\\ \quad `\verb|it|' .\smallskip {\it Arguments\/} =\\* \quad {\it Term-Expression\/} $|$\\ \quad `\verb|(|' {\it Term-Expression-List\/} `\verb|)|' .\bigskip {\it File-Name-List\/} = {\it File-Name\/} \{ `\verb|,|' \ldots \} .\smallskip {\it Identifier-List\/} = {\it Identifier\/} \{ `\verb|,|' \ldots \} .\smallskip {\it Type-Expression-List\/} = {\it Type-Expression\/} \{ `\verb|,|' \ldots \} .\smallskip {\it Term-Expression-List\/} = {\it Term-Expression\/} \{ `\verb|,|' \ldots \} . \end{flushleft} \section{Axioms} Here are the undefined notions and axioms of the Mizar system: everything in the Mizar library is defined and proved from just this. (This is the content of articles `\verb|HIDDEN|' and `\verb|TARSKI|'. Axiom `\verb|TARSKI:8|' was omitted because it's derivable from `{\tt TARSKI:def 5}'.) \begin{flushleft}\footnotesize\smallskip \verb|definition mode Any; synonym set; end;|\\ \verb|reserve x,y,z,u for Any, N,M,X,Y,Z for set;| \smallskip \verb|definition let x,y; pred x = y; reflexivity; symmetry; antonym x <> y; end;| \smallskip \verb|definition let x,X; pred x |$\in$\verb| X; antisymmetry; end;| \smallskip \verb|definition let X; attr X is empty; end;|\\ \verb|definition cluster empty set; cluster non empty set; end;| \smallskip \verb|definition func |$\emptyset$\verb| -> empty set; end;| \smallskip \verb|definition let X; mode Element of X; end;| \smallskip \verb|definition let X; func bool X -> non empty set; end;| \smallskip \verb|definition let X; mode Subset of X is Element of bool X; end;| \smallskip \verb|definition let X be non empty set; cluster non empty Subset of X; end;| \smallskip \verb|definition let X,Y; pred X c= Y; reflexivity; end;| \smallskip \verb|definition let D be non empty set, X be non empty Subset of D;|\\ \verb| redefine mode Element of X -> Element of D;|\\ \verb|end;| \bigskip \verb|theorem (for x holds x |$\in$\verb| X iff x |$\in$\verb| Y) implies X = Y;| \smallskip \verb|definition let y; func {y} -> set means x |$\in$\verb| it iff x = y;|\\ \verb| let z; func {y,z} -> set means x |$\in$\verb| it iff x = y or x = z;|\\ \verb| commutativity;|\\ \verb|end;|\\ \verb|definition let y; cluster {y} -> non empty;|\\ \verb| let z; cluster {y,z} -> non empty;|\\ \verb|end;| \smallskip \verb|definition let X,Y; redefine pred X c= Y means x |$\in$\verb| X implies x |$\in$\verb| Y; end;| \smallskip \verb|definition let X;|\\ \verb| func union X -> set means x |$\in$\verb| it iff ex Y st x |$\in$\verb| Y & Y |$\in$\verb| X;|\\ \verb|end;| \smallskip \verb|theorem X = bool Y iff for Z holds Z |$\in$\verb| X iff Z c= Y;| \smallskip \verb|theorem x |$\in$\verb| X implies ex Y st Y |$\in$\verb| X & not ex x st x |$\in$\verb| X & x |$\in$\verb| Y;| \smallskip \verb|scheme Fraenkel {A()->set, P[Any,Any]}:|\\ \verb| ex X st for x holds x |$\in$\verb| X iff ex y st y |$\in$\verb| A() & P[y,x]|\\ \verb| provided|\\ \verb| for x,y,z st P[x,y] & P[x,z] holds y = z;| \smallskip \verb|definition let x,y; func [x,y] equals {{x,y},{x}}; end;|\\ %\verb|theorem [x,y] = {{x,y},{x}};| \smallskip \verb|definition let X,Y;|\\ \verb| pred X |$\approx$\verb| Y means ex Z st|\\ \verb| (for x st x |$\in$\verb| X ex y st y |$\in$\verb| Y & [x,y] |$\in$\verb| Z) &|\\ \verb| (for y st y |$\in$\verb| Y ex x st x |$\in$\verb| X & [x,y] |$\in$\verb| Z) &|\\ \verb| for x,y,z,u st [x,y] |$\in$\verb| Z & [z,u] |$\in$\verb| Z holds x = z iff y = u;|\\ \verb|end;| \smallskip \verb|:: |{\it Axiom der unerreichbaren Mengen\/}\\ \verb|theorem ex M st N |$\in$\verb| M &|\\ \verb| (for X,Y holds X |$\in$\verb| M & Y c= X implies Y |$\in$\verb| M) &|\\ \verb| (for X holds X |$\in$\verb| M implies bool X |$\in$\verb| M) &|\\ \verb| (for X holds X c= M implies X |$\approx$\verb| M or X |$\in$\verb| M);|\\ \end{flushleft} \newcounter{lineno} \newcommand{\lineno}{\addtocounter{lineno}{1}% \makebox[0pt][l]{% %\hspace{\textwidth}\qquad \makebox[0pt][r]{\tiny\bf\thelineno \quad }}% %\quad } \newcommand{\lineinc}{\addtocounter{lineno}{1}} \section{Complete Example} Here is an example of a complete Mizar text: it's the article `\verb|UNIALG_1|' from the Mizar library, article number 303 by Jaros{\l}aw Kotowicz, Beata Madras and Ma{\l}gorzata Korolkiewicz \cite{kot:mad:kor:92}. It defines the type `{\tt Univer\-sal\verb|_Algebra|}' (together with the notions of `\verb|arity|' and `\verb|signature|') which is the Mizar implementation of `one-sorted algebras' from the theory of universal algebra. We both give here the `abstract' file `\verb|UNIALG_1.ABS|' as well as the full Mizar article `\verb|UNIALG_1.MIZ|'. Interspersed are explanations. Sometimes the explanations contain Mizar text from other articles: the main text of the `\verb|UNIALG_1|' article can be recognized because it is not indented and because it has line numbers in the left margin. \subsection{Abstract} In order to find out what's in an article from the Mizar library, one generally only looks at its `abstract' file. This is generated automatically from the full article. In it all proofs have been removed and `sequence numbers' like `\verb|UNIALG_1:5|' for the theorems and `\verb|UNIALG_1:def 11|' for the definitions have been inserted automatically. \begin{flushleft}\footnotesize \lineno\verb|:: Basic Notation of Universal Algebra|\\ \lineno\verb|:: by Jaros{\l}aw Kotowicz, Beata Madras and Ma{\l}gorzata Korolkiewicz|\\ \lineno\verb|::|\\ \lineno\verb|:: Received December 29, 1992|\\ \lineno\verb|:: Copyright (c) 1992 Association of Mizar Users| \lineinc \medskip \lineno\verb|environ| \lineinc \medskip \lineno\verb| vocabulary UNIALG, PFUNC1, FINSEQ, FUNC_REL, FUNC, FINITER2, PBOOLE, UNIALG_D;|\\ \lineno\verb| notation ARYTM, NAT_1, STRUCT_0, TARSKI, RELAT_1, FUNCT_1, FINSEQ_1, FUNCOP_1,|\\ \lineno\verb| PARTFUN1, ZF_REFLE;|\\ \lineno\verb| clusters TARSKI, FINSEQ_1, RELSET_1, STRUCT_0, ARYTM, PARTFUN1, FUNCOP_1;|\\ \lineno\verb| constructors FINSEQ_4, STRUCT_0, ZF_REFLE, FUNCOP_1, PARTFUN1;|\\ \lineno\verb| requirements ARYTM;| \lineinc \lineinc \end{flushleft} This is the `\verb|environ|' header of the article. It mentions the various vocabularies (in the `\verb|vocabulary|' directive)\ and articles (in the `\verb|notation|', `\verb|clusters|' and `\verb|constructors|' directives) from the Mizar library that the article uses. The only special items in this header are the vocabulary `\verb|UNIALG|' which is the one that's `special' to this article, and the `\verb|ARYTM|' label, which is neither a vocabulary name nor an article name. The vocabulary file `\verb|UNIALG.VOC|' is not explicitely present in the Mizar distribution but only as part of the `compiled' vocabulary library `\verb|MML.VCB|'. However, it can be printed with the command `{\tt listvoc UNIALG}': \begin{verse}\footnotesize \verb|GUAStr|\\ \verb|Ucharact|\\ \verb|Vhomogeneous|\\ \verb|Vquasi_total|\\ \verb|Vpartial|\\ \verb|OOpers 128|\\ \verb|MUniversal_Algebra|\\ \verb|Oarity 128|\\ \verb|Osignature| \end{verse} These are the `\verb|func|' (`\verb|O|'), `\verb|mode|' (`\verb|M|'), `\verb|attr|' (`\verb|V|'), `\verb|struct|' (`\verb|G|') and `\verb|struct| field' (`\verb|U|') symbols which are `new' to this article. These symbols correspond to the definitions from lines 62, 63, 75, 82, 105, /, 142, 150 and 161 of the abstract, and lines 153, 154, 176, 182, 257, /, 343, 351 and 395 of the full article. The operation `\verb|Opers|' does not appear in this article, but is defined in article `\verb|UNIALG_2|' (both articles share the vocabulary). \begin{flushleft}\footnotesize\medskip \lineno\verb|begin| \lineinc \lineinc \end{flushleft} A Mizar article consists of one or more `sections', each of which starts with `\verb|begin|' (there is no corresponding `\verb|end|'). This article only has one section. \begin{flushleft}\footnotesize\medskip \lineno\verb|reserve A for set,|\\ \lineno\verb| a for Element of A,|\\ \lineno\verb| x,y for FinSequence of A,|\\ \lineno\verb| h for PartFunc of A*,A ,|\\ \lineno\verb| n,m for Nat,|\\ \lineno\verb| z for set;| \lineinc \end{flushleft} These reservations are straight-forward: note that some of them only can be used when there's an `\verb|A|' in scope. The most interesting type from this list is that of `\verb|h|': \begin{verse}\footnotesize \verb|PartFunc of A*,A| \end{verse} The postfix operator `\verb|*|' is defined in article `\verb|FINSEQ_1|' (the easiest way to determine this is to click on it in the web version% \footnote{{\tt }} of the Mizar library) as: \begin{verse}\footnotesize \verb|definition let D be set;|\\ \verb| func D* -> set means x |$\in$\verb| it iff x is FinSequence of D;|\\ \verb|end;| \end{verse} \noindent (definitions as presented here are taken from the abstracts and so don't contain proofs), with the operator symbol `\verb|*|' defined in \verb|vocabulary| `\verb|FINSEQ|' as: \begin{verse}\footnotesize \verb|O* 128| \end{verse} \noindent while the \verb|mode| `\verb|FinSequence|' comes from the same article: \begin{verse}\footnotesize \verb|definition let n;|\\ \verb| func Seg n -> set equals { k : 1 |$\le$\verb| k & k |$\le$\verb| n };|\\ \verb|end;| \verb|definition let IT be Relation;|\\ \verb| attr IT is FinSequence-like means ex n st dom IT = Seg n;|\\ \verb|end;| \verb|definition|\\ \verb| mode FinSequence is FinSequence-like Function;|\\ \verb|end;| \verb|definition let D be set;|\\ \verb| mode FinSequence of D -> FinSequence means rng it c= D;|\\ \verb|end;| \end{verse} The `\verb|PartFunc|' \verb|mode| is defined in article `\verb|PARTFUN1|' as: \begin{verse}\footnotesize \verb|definition let X,Y;|\\ \verb| mode PartFunc of X,Y is Function-like Relation of X,Y;|\\ \verb|end;| \end{verse} \noindent so `\verb|PartFunc of A*,A|' means `partial function from \verb|A*| to \verb|A|'. The general way to name a mode is: \begin{verse}\footnotesize {\it mode-name\/}{\tt{} of }{\it parameter\/}\verb|,|{\it parameter\/}\verb|,|\ldots \end{verse} \noindent which explains the slightly unnatural syntax. \begin{flushleft}\footnotesize\medskip \lineno\verb|definition let A;|\\ \lineno\verb| let IT be PartFunc of A*,A;|\\ \lineno\verb|attr IT is homogeneous means|\\ \lineno\verb|:: UNIALG_1:def 1 |\\ \lineno\verb| for x,y st x |$\in$\verb| dom IT & y |$\in$\verb| dom IT holds len x = len y;|\\ \lineno\verb|end;| \lineinc \medskip \lineno\verb|definition let A;|\\ \lineno\verb| let IT be PartFunc of A*,A;|\\ \lineno\verb|attr IT is quasi_total means|\\ \lineno\verb|:: UNIALG_1:def 2|\\ \lineno\verb| for x,y st len x = len y & x |$\in$\verb| dom IT holds y |$\in$\verb| dom IT;|\\ \lineno\verb|end;| \lineinc \medskip \lineno\verb|definition let A be non empty set;|\\ \lineno\verb|cluster homogeneous quasi_total non empty PartFunc of A*,A;|\\ \lineno\verb|end;| \lineinc \end{flushleft} This cluster states that the type: \begin{verse}\footnotesize \verb|homogeneous quasi_total non empty PartFunc of A*,A| \end{verse} \noindent is inhabited. It is needed (because Mizar types have to be non-empty) to be allowed to use the adjectives `\verb|homogeneous|', `\verb|quasi_total|' and `{\tt non empty}' (alone or in combination) with types of the form `{\tt PartFunc of A*,A}'. Without it for instance the types: \begin{verse}\footnotesize \verb|homogeneous quasi_total non empty PartFunc of A*,A| \verb|homogeneous non empty PartFunc of A*,A| \verb|homogeneous non empty|\\ \verb| PartFunc of (the carrier of U)*,the carrier of U| \end{verse} \noindent in lines 50, 149 and 165-166 of this abstract wouldn't be legal (in the proofs there appear 11 more types like this). \begin{flushleft}\footnotesize\medskip \lineno\verb|theorem :: UNIALG_1:1 |\\ \lineno\verb|h is non empty iff dom h <> |$\emptyset$\verb|;| \lineinc \medskip \lineno\verb|theorem :: UNIALG_1:2 |\\ \lineno\verb|for A being non empty set, a being Element of A|\\ \lineno\verb|holds {<|$\emptyset$\verb|>A} -->a is homogeneous quasi_total non empty PartFunc of A*,A;| \lineinc \end{flushleft} The operator \verb|<|$\emptyset$\verb|>A| denotes the empty finite sequence with elements of type \verb|A|. It is defined in article `\verb|FINSEQ_1|' as: \begin{verse}\footnotesize \verb|definition redefine func |$\emptyset$\verb|; synonym <|$\emptyset$\verb|>; end;| \verb|definition let D be set;|\\ \verb| func <|$\emptyset$\verb|>(D) -> empty FinSequence of D equals <|$\emptyset$\verb|>;|\\ \verb|end;| \end{verse} \noindent where the operator symbol `\verb|<|$\emptyset$\verb|>|' is from vocabulary `\verb|FINSEQ|': \begin{verse}\footnotesize \verb|O<|$\emptyset$\verb|> 254| \end{verse} In this, `$\emptyset$' is the name of the empty set as introduced in article `\verb|HIDDEN|': \begin{verse}\footnotesize \verb|definition|\\ \verb| func |$\emptyset$\verb| -> empty set;|\\ \verb|end;| \end{verse} \noindent and vocabulary `\verb|HIDDEN|': \begin{verse}\footnotesize \verb|O|$\emptyset$\verb| 128| \end{verse} \noindent (Because `\verb|HIDDEN|' is one of the two files presenting the axioms of the Mizar system there is no `\verb|means|' or `\verb|equals|' in this definition. Also, the `\verb|HIDDEN|' article and the `\verb|HIDDEN|' vocabulary are always present and so they don't need to be listed in the `\verb|environ|' header of the article.) The braces `\verb|{| \ldots\verb|}|' denote the one element set. It is defined in article `\verb|TARSKI|': \begin{verse}\footnotesize \verb|definition let y;|\\ \verb| func {y} -> set means x |$\in$\verb| it iff x = y;|\\ \verb|end;| \end{verse} \noindent The symbols `\verb|{|' and `\verb|}|' occur on their own in the Mizar syntax too, and are not in a vocabulary. The infix operator `\verb|-->|' creates a constant function on a set. It is defined in article `\verb|FUNCOP_1|': \begin{verse}\footnotesize \verb|definition let A, a be set;|\\ \verb| func A --> a -> set equals [:A, {a}:];|\\ \verb|end;| \end{verse} \noindent and vocabulary `\verb|FINITER2|': \begin{verse}\footnotesize \verb|O--> 16| \end{verse} \noindent Here \verb|[:| \ldots\verb|:]| is the Cartesian product from article `\verb|ZFMISC_1|': \begin{verse}\footnotesize \verb|definition let X1,X2;|\\ \verb| func [: X1,X2 :] means|\\ \verb| z |$\in$\verb| it iff ex x,y st x |$\in$\verb| X1 & y |$\in$\verb| X2 & z = [x,y];|\\ \verb|end;| \end{verse} \noindent and `\verb|[| \ldots\verb|]|' is the Kuratowski pair from article `\verb|TARSKI|': \begin{verse}\footnotesize \verb|definition|\\ \verb| func [x,y] equals {{x,y},{x}};|\\ \verb|end;| \end{verse} \begin{flushleft}\footnotesize\medskip \lineno\verb|theorem :: UNIALG_1:3 |\\ \lineno\verb|for A being non empty set, a being Element of A|\\ \lineno\verb| holds {<|$\emptyset$\verb|>A} -->a is Element of PFuncs(A*,A);| \lineinc \end{flushleft} The \verb|func| `\verb|PFuncs|' is defined in article `\verb|PARTFUN1|': \begin{verse}\footnotesize \verb|definition let X,Y;|\\ \verb| func PFuncs(X,Y) -> set means|\\ \verb| x |$\in$\verb| it iff|\\ \verb| ex f being Function st x = f & dom f c= X & rng f c= Y;|\\ \verb|end;| \end{verse} \begin{flushleft}\footnotesize\medskip \lineno\verb|definition let A;|\\ \lineno\verb| mode PFuncFinSequence of A -> FinSequence of PFuncs(A*,A) means|\\ \lineno\verb|:: UNIALG_1:def 3|\\ \lineno\verb| not contradiction;|\\ \lineno\verb|end;| \lineinc \end{flushleft} Despite what the official Mizar grammar (appendix \ref{grammar} on page \pageref{grammar}) suggests, the redundant characterization `{\tt means not contradiction}' may not be omitted. \begin{flushleft}\footnotesize\medskip \lineno\verb|struct (1-sorted) UAStr |$\langle\!\langle$\verb| carrier -> set,|\\ \lineno\verb| charact -> PFuncFinSequence of the carrier|$\rangle\!\rangle$\verb|;| \lineinc \end{flushleft} So the \verb|struct| `\verb|UAStr|' that underlies the implementation of the notion of `algebra' in Mizar has two fields: `\verb|carrier|' which is the `sort' of the algebra, and `\verb|charact|' which is the sequence of `functions' of the algebra. The ancestor \verb|struct| `\verb|1-sorted|' is defined in article `\verb|STRUCT_0|': \begin{verse}\footnotesize \verb|definition|\\ \verb| struct 1-sorted |$\langle\!\langle$\verb|carrier -> set|$\rangle\!\rangle$\verb|;|\\ \verb|end;| \end{verse} \begin{flushleft}\footnotesize\medskip \lineno\verb|definition|\\ \lineno\verb| cluster non empty strict UAStr;|\\ \lineno\verb|end;| \lineinc \end{flushleft} This cluster states that there exists a {\tt non empty strict UAStr}. It is not used in this article. Note that because the type `\verb|UAStr|' widens to `\verb|1-sorted|', which is narrower than `\verb|set|', the adjective `{\tt non empty}' refers to the definition: \begin{verse}\footnotesize \verb|definition let S be 1-sorted;|\\ \verb| attr S is empty means the carrier of S is empty;|\\ \verb|end;| \end{verse} \noindent from article `\verb|STRUCT_0|', instead of to the definition: \begin{verse}\footnotesize \verb|definition let X be set;|\\ \verb| attr X is empty;|\\ \verb|end;| \end{verse} \noindent from article `\verb|HIDDEN|'. \begin{flushleft}\footnotesize\medskip \lineno\verb|definition let D be non empty set, c be PFuncFinSequence of D;|\\ \lineno\verb| cluster UAStr |$\langle\!\langle$\verb|D,c |$\rangle\!\rangle$\verb| -> non empty;|\\ \lineno\verb|end;| \lineinc \end{flushleft} This cluster causes expressions of the shape `\verb|UAStr|$\langle\!\langle$\verb|D,c|$\rangle\!\rangle$', with \verb|D| having the adjective `{\tt non empty}', to gain the adjective `{\tt non empty}' too. It is used in line 323 of the article. \begin{flushleft}\footnotesize\medskip \lineno\verb|definition let A;|\\ \lineno\verb| let IT be PFuncFinSequence of A;|\\ \lineno\verb|attr IT is homogeneous means|\\ \lineno\verb|:: UNIALG_1:def 4 |\\ \lineno\verb| for n,h st n |$\in$\verb| dom IT & h = IT.n holds h is homogeneous;|\\ \lineno\verb|end;| \lineinc \medskip \lineno\verb|definition let A;|\\ \lineno\verb| let IT be PFuncFinSequence of A;|\\ \lineno\verb|attr IT is quasi_total means|\\ \lineno\verb|:: UNIALG_1:def 5 |\\ \lineno\verb| for n,h st n |$\in$\verb| dom IT & h = IT.n holds h is quasi_total;|\\ \lineno\verb|end;| \lineinc \medskip \lineno\verb|definition let F be Function;|\\ \lineno\verb|redefine attr F is non-empty means|\\ \lineno\verb|:: UNIALG_1:def 6 |\\ \lineno\verb| for n being set st n |$\in$\verb| dom F holds F.n is non empty;|\\ \lineno\verb|end;| \lineinc \end{flushleft} The \verb|attr| `\verb|non-empty|' was defined in article `\verb|ZF_REFLE|' as: \begin{verse}\footnotesize \verb|definition let F be Function;|\\ \verb| attr F is non-empty means not |$\emptyset$\verb| |$\in$\verb| rng F;|\\ \verb|end;| \end{verse} The redefinition that's given here has to be equivalent to this (it is allowed to have a more specific parameter type though, although here that's not the case). Both the original definition and the redefinition are used in exactly the same way. This new definition is used in lines 242--250 of the full article (because the proof there is of the `expanded' form of the definition: Mizar expands definitions from the article itself, and from articles in the `\verb|definitions|' \verb|environ| directive). Also its `definitional theorem' (`\verb|Def6|') is referred to in lines 301, 413 and 452 of the full article. \begin{flushleft}\footnotesize\medskip \lineno\verb|definition let A be non empty set; let x be Element of PFuncs(A*,A);|\\ \lineno\verb| redefine|\\ \lineno\verb| func <*x*> -> PFuncFinSequence of A;|\\ \lineno\verb|end;| \lineinc \end{flushleft} This redefines the `\verb|<*| \ldots\verb|*>|' operator from article `\verb|FINSEQ_1|': \begin{verse}\footnotesize \verb|definition let x;|\\ \verb| func <*x*> -> set equals { [1,x] };|\\ \verb|end;| \end{verse} This operator is used to write sequences of length one. The redefinition doesn't give a new characterization of this \verb|func| (so it `inherits' the original one), but it does change its {\it type.\/} Without it, adjectives like `\verb|homogeneous|' and `\verb|quasi_total|' wouldn't be applicable to expressions of the form `\verb|<*x*>|', like for instance in line 123 of the abstract. \begin{flushleft}\footnotesize\medskip \lineno\verb|definition let A be non empty set;|\\ \lineno\verb|cluster homogeneous quasi_total non-empty PFuncFinSequence of A;|\\ \lineno\verb|end;| \lineinc \end{flushleft} This cluster is not used in this article. \begin{flushleft}\footnotesize\medskip \lineno\verb|reserve U for UAStr;| \lineinc \medskip \lineno\verb|definition let IT be UAStr;|\\ \lineno\verb|attr IT is partial means|\\ \lineno\verb|:: UNIALG_1:def 7 |\\ \lineno\verb| the charact of IT is homogeneous;|\\ \lineno\verb|attr IT is quasi_total means|\\ \lineno\verb|:: UNIALG_1:def 8 |\\ \lineno\verb| the charact of IT is quasi_total;|\\ \lineno\verb|attr IT is non-empty means|\\ \lineno\verb|:: UNIALG_1:def 9 |\\ \lineno\verb| the charact of IT <> <|$\emptyset$\verb|> & the charact of IT is non-empty;|\\ \lineno\verb|end;| \lineinc \medskip \lineno\verb|reserve A for non empty set,|\\ \lineno\verb| h for PartFunc of A*,A ,|\\ \lineno\verb| x,y for FinSequence of A,|\\ \lineno\verb| a for Element of A;| \lineinc \end{flushleft} These reservations are identical to those from lines 20--23, apart that after this, `\verb|A|' has the adjective `{\tt non empty}'. \begin{flushleft}\footnotesize\medskip \lineno\verb|theorem :: UNIALG_1:4 |\\ \lineno\verb|for x be Element of PFuncs(A*,A) st x = {<|$\emptyset$\verb|>A} --> a holds|\\ \lineno\verb| <*x*> is homogeneous quasi_total non-empty;| \lineinc \medskip \lineno\verb|definition|\\ \lineno\verb| cluster quasi_total partial non-empty strict non empty UAStr;|\\ \lineno\verb|end;| \lineinc \end{flushleft} This cluster is used five times in this article to establish the correctness of a type. For example it's used in the definition of the \verb|mode| `\verb|Universal_Algebra|' in line 142 of this abstract. \begin{flushleft}\footnotesize\medskip \lineno\verb|definition let U be partial UAStr;|\\ \lineno\verb| cluster the charact of U -> homogeneous;|\\ \lineno\verb|end;| \lineinc \medskip \lineno\verb|definition let U be quasi_total UAStr;|\\ \lineno\verb| cluster the charact of U -> quasi_total;|\\ \lineno\verb|end;| \lineinc \medskip \lineno\verb|definition let U be non-empty UAStr;|\\ \lineno\verb| cluster the charact of U -> non-empty non empty;|\\ \lineno\verb|end;| \lineinc \end{flushleft} The `{\tt non empty}' means that there is at least one function in an algebra, the `\verb|non-empty|' means that these functions all are not empty. \begin{flushleft}\footnotesize\medskip \lineno\verb|definition|\\ \lineno\verb|mode Universal_Algebra is quasi_total partial non-empty non empty UAStr;|\\ \lineno\verb|end;| \lineinc \medskip \lineno\verb|reserve U for partial non-empty non empty UAStr;| \lineinc \medskip \lineno\verb|definition|\\ \lineno\verb| let A;|\\ \lineno\verb| let f be homogeneous non empty PartFunc of A*,A;|\\ \lineno\verb|func arity(f) -> Nat means|\\ \lineno\verb|:: UNIALG_1:def 10|\\ \lineno\verb| x |$\in$\verb| dom f implies it = len x;|\\ \lineno\verb|end;| \lineinc \end{flushleft} Note that the argument `\verb|A|' of this \verb|func| is an implicit argument: it's not present in the {\tt no\-ta\-tion} `{\tt arity f}'. \begin{flushleft}\footnotesize\medskip \lineno\verb|theorem :: UNIALG_1:5 |\\ \lineno\verb|for U holds for n st n|$\in$\verb|dom the charact of(U) holds|\\ \lineno\verb| (the charact of(U)).n is|\\ \lineno\verb| PartFunc of (the carrier of U)*,the carrier of U;| \lineinc \medskip \lineno\verb|definition let U;|\\ \lineno\verb|func signature(U) ->FinSequence of NAT means|\\ \lineno\verb|:: UNIALG_1:def 11|\\ \lineno\verb| len it = len the charact of(U) &|\\ \lineno\verb| for n st n |$\in$\verb| dom it holds|\\ \lineno\verb| for h be homogeneous non empty|\\ \lineno\verb| PartFunc of (the carrier of U )*,the carrier of U|\\ \lineno\verb| st h = (the charact of(U)).n|\\ \lineno\verb| holds it.n = arity(h);|\\ \lineno\verb|end;| \end{flushleft} \subsection{Article} \setcounter{lineno}{0} \begin{flushleft}\footnotesize \lineno\verb|:: Basic Notation of Universal Algebra|\\ \lineno\verb|:: by Jaros{\l}aw Kotowicz, Beata Madras and Ma{\l}gorzata Korolkiewicz|\\ \lineno\verb|::|\\ \lineno\verb|:: Received December 29, 1992|\\ \lineno\verb|:: Copyright (c) 1992 Association of Mizar Users| \lineinc \medskip \lineno\verb|environ| \lineinc \medskip \lineno\verb| vocabulary UNIALG, PFUNC1, FINSEQ, FUNC_REL, FUNC, FINITER2, PBOOLE, UNIALG_D;|\\ \lineno\verb| constructors FINSEQ_4, STRUCT_0, ZF_REFLE, FUNCOP_1, PARTFUN1;|\\ \lineno\verb| requirements ARYTM;|\\ \lineno\verb| notation ARYTM, NAT_1, STRUCT_0, TARSKI, RELAT_1, FUNCT_1, FINSEQ_1, FUNCOP_1,|\\ \lineno\verb| PARTFUN1, ZF_REFLE;|\\ \lineno\verb| clusters TARSKI, FINSEQ_1, RELSET_1, STRUCT_0, ARYTM, PARTFUN1, FUNCOP_1;|\\ \lineno\verb| definitions TARSKI, STRUCT_0, ZF_REFLE;|\\ \lineno\verb| theorems TARSKI, FUNCT_1, PARTFUN1, FINSEQ_1, FUNCOP_1, RELAT_1, RELSET_1,|\\ \lineno\verb| FINSEQ_3, ZF_REFLE;|\\ \lineno\verb| schemes MATRIX_2;| \lineinc \end{flushleft} The `\verb|definitions|', `\verb|theorems|' and `\verb|schemes|' directives were not in the abstract because they are only relevant to the proofs. They also contain names of articles from the library. The last two list articles from which \verb|theorems| and \verb|schemes| are used. The `\verb|definitions|' directive from line 15 applies to 9 places in the article: \begin{itemize} \item The proofs in lines 50--54, 56--60, 93--97, 99--103, 131--135 and 137--141. These proofs are of statements involving the inclusion operator `\verb|c=|', but the proofs prove a universally quantified formula. The `\verb|c=|' operator is defined in article `\verb|TARSKI|' ({\it re\/}defined really, because the `\verb|c=|' operator is originally introduced without definition in article `\verb|HIDDEN|') as: \begin{verse}\footnotesize \verb|definition let X,Y;|\\ \verb| redefine pred X c= Y means x |$\in$\verb| X implies x |$\in$\verb| Y;|\\ \verb|end;| \end{verse} \noindent and so with a `{\tt definitions TARSKI;}' directive the `\verb|c=|' statement will be expanded to a suitable universal formula. \item The `{\tt thus the carrier of UAStr$\langle\!\langle$D,c$\rangle\!\rangle$ is non empty;}' in lines 161 and 170. Here the statement to be proved is about a \verb|struct|, but the statement that is supplied is about {\tt the carrier of} that \verb|struct|. In order for this to be correct a `{\tt definitions STRUCT\verb|_|0;}' has to make the definition of `\verb|empty|' on structs transparent: \begin{verse}\footnotesize \verb|definition let S be 1-sorted;|\\ \verb| attr S is empty means the carrier of S is empty;|\\ \verb|end;| \end{verse} \item The proof `{\tt assume $\emptyset$ $\in$ rng F;} {\dots} {\tt hence contradiction by A2;}' in lines 199--201. It proves `{\tt not $\emptyset$ $\in$ rng F}', but the statement it is supposed to prove really is `{\tt F is non-empty}'. So the directive `{\tt definitions ZF\verb|_|REFLE;}' is needed to make the definition: \begin{verse}\footnotesize \verb|definition let F be Function;|\\ \verb| attr F is non-empty means not |$\emptyset$\verb| |$\in$\verb| rng F;|\\ \verb|end;| \end{verse} transparent. \end{itemize} \noindent It is `\verb|Analyzer|' (the type checking phase of the Mizar checker) that needs these definitional expansions, instead of `\verb|Checker|' (which checks the logical correctness of the inferences). \begin{flushleft}\footnotesize\medskip \lineno\verb|begin| \lineinc \lineinc \medskip \lineno\verb|reserve A for set,|\\ \lineno\verb| a for Element of A,|\\ \lineno\verb| x,y for FinSequence of A,|\\ \lineno\verb| h for PartFunc of A*,A ,|\\ \lineno\verb| n,m for Nat,|\\ \lineno\verb| z for set;| \lineinc \medskip \lineno\verb|definition let A;|\\ \lineno\verb| let IT be PartFunc of A*,A;|\\ \lineno\verb|attr IT is homogeneous means :Def1:|\\ \lineno\verb| for x,y st x |$\in$\verb| dom IT & y |$\in$\verb| dom IT holds len x = len y;|\\ \lineno\verb|end;| \lineinc \end{flushleft} Note that this \verb|definition| is referred to (because of the label on line 32) as `\verb|Def1|' in this article (on line 364), but (the label on line 30 of the abstract) as `{\tt UNIALG\verb|_|1:def 1}' in the other articles (specifically: articles `\verb|ALG_1|', `\verb|FREEALG|' and `\verb|PRALG_1|'). Similarly the \verb|theorem| from lines 83--84 is referred to as `\verb|Th1|' in this article (lines 121, 357 and 372), but as `{\tt UNIALG\verb|_|1:1}' (line 45 of the abstract) in the others (`\verb|ALG_1|', `\verb|MSSUBLAT|', `\verb|PRALG_1|' and `\verb|UNIALG_2|'). \begin{flushleft}\footnotesize\medskip \lineno\verb|definition let A;|\\ \lineno\verb| let IT be PartFunc of A*,A;|\\ \lineno\verb|attr IT is quasi_total means|\\ \lineno\verb| for x,y st len x = len y & x |$\in$\verb| dom IT holds y |$\in$\verb| dom IT;|\\ \lineno\verb|end;| \lineinc \medskip \end{flushleft} The following definition and its proof will be annotated in more detail than the remainder of the Mizar text. The proof (lines 45--80) is the really same as the proof of \verb|theorem| `\verb|Th2|' (lines 89--122 on page \pageref{th2}), so it can be read there without interruptions. \begin{flushleft}\footnotesize \lineno\verb|definition let A be non empty set;|\\ \lineno\verb|cluster homogeneous quasi_total non empty PartFunc of A*,A;| \end{flushleft} This cluster states that the type: \begin{verse}\footnotesize \verb|homogeneous quasi_total non empty PartFunc of A*,A| \end{verse} \noindent is inhabited. It should be present if one wants to use the adjectives `{\tt ho\-mo\-ge\-neous}', `{\tt quasi\verb|_|total}' or `{\tt non empty}' with types of the form `{\tt PartFunc of A*,A}'. \begin{flushleft}\footnotesize \lineno\verb| existence| \end{flushleft} Because a `\verb|cluster|' of this kind states the non-emptyness of a type, its correctness condition is an `\verb|existence|' statement. This statement is: \begin{verse}\footnotesize \verb|ex f being PartFunc of A*,A st|\\ \verb| f is homogeneous & f is quasi_total & f is non empty| \end{verse} \begin{flushleft}\footnotesize \lineno\verb| proof|\\ \lineno\verb| consider a be Element of A;| \end{flushleft} A `\verb|consider|' step needs an existential statement as a justification. In this case it is: \begin{verse}\footnotesize \verb|ex a be Element of A| \end{verse} \noindent (this isn't a full Mizar formula: append `{\tt st not contradiction}' to complete it). Because Mizar types all are non-empty an existential statement of this kind is evident: so the `\verb|consider|' needs no justification. The property of `\verb|A|' that (from line 42): \begin{verse}\footnotesize \verb|A is non empty| \end{verse} \noindent isn't used here: the `\verb|consider|' step also would have been valid if `\verb|A|' had just been a `\verb|set|'. However, in that case: \begin{verse}\footnotesize \verb|a |$\in$\verb| A| \end{verse} \noindent would not have been true (it is built into the Mizar system that when `{\tt A is non empty}' it follows from `{\tt a is Element of A}' that `{\tt a $\in$ A}'), and then the `\verb|hence|' step in line 59 would have failed. \begin{flushleft}\footnotesize \lineno\verb| set f = {<|$\emptyset$\verb|>A} -->a;| \end{flushleft} This is a local definition of a constant `\verb|f|': all occurrences of `\verb|f|' after this will be expanded to `{\tt \verb|{|<$\emptyset$>A\verb|}|-->a}'. The `\verb|f|' that's defined here is a function that has as domain the set `{\tt \verb|{|<$\emptyset$>A\verb|}|}' which it maps to the constant `\verb|a|'. This domain consist of just the sequence of zero length: it is the set $\verb|A|^0$. So we have that: $$\verb|f|: \verb|A|^0 \rightarrow \verb|A|,\quad \langle\rangle \mapsto \verb|a|$$ and so this \verb|f| is the `nullary' function on \verb|A| which represents the constant \verb|a|. \begin{flushleft}\footnotesize \lineno\verb| A1: dom f = {<|$\emptyset$\verb|>A} & rng f = {a} by FUNCOP_1:14;| \end{flushleft} This statement expands to: \begin{verse}\footnotesize \verb|A1: dom ({<|$\emptyset$\verb|>A}-->a) = {<|$\emptyset$\verb|>A} & rng ({<|$\emptyset$\verb|>A}-->a) = {a}| \end{verse} \noindent which follows from the type of `\verb|A|' from line 42: \begin{verse}\footnotesize \verb|A is non empty set| \end{verse} \noindent the type of `$\emptyset$' from article `\verb|HIDDEN|': \begin{verse}\footnotesize \verb|definition|\\ \verb| func |$\emptyset$\verb| -> empty set;|\\ \verb|end;| \end{verse} \noindent and: \begin{verse}\footnotesize \verb|theorem :: FUNCOP_1:14|\\ \verb| A <> |$\emptyset$\verb| implies dom (A --> x) = A & rng (A --> x) = {x};| \end{verse} \begin{flushleft}\footnotesize \lineno\verb| A2: dom f c= A*| \end{flushleft} Because of the `\verb|definitions TARSKI;|' directive from line 15, this expands according to: \begin{verse}\footnotesize \verb|definition let X,Y; redefine pred X c= Y means|\\ \verb|:: TARSKI:def 3|\\ \verb| x |$\in$\verb| X implies x |$\in$\verb| Y;|\\ \verb|end;| \end{verse} \noindent to: \begin{verse}\footnotesize \verb|A2: for z being set st z |$\in$\verb| dom f holds z |$\in$\verb| A*| \end{verse} \begin{flushleft}\footnotesize \lineno\verb| proof| \end{flushleft} Here starts a `local' subproof of the statement `\verb|A2|'. \begin{flushleft}\footnotesize \lineno\verb| let z; assume z |$\in$\verb| dom f; then| \end{flushleft} The `\verb|let|' and `\verb|assume|' skeleton steps correspond to the `\verb|for| {\ldots}' and `\verb|st| {\ldots} \verb|holds|' parts of the statement. After these steps: \begin{verse}\footnotesize \verb|z |$\in$\verb| A*| \end{verse} \noindent is left to be proved. \begin{flushleft}\footnotesize \lineno\verb| z = <|$\emptyset$\verb|>A by TARSKI:def 1,A1;| \end{flushleft} The statement: \begin{verse}\footnotesize \verb|z = <|$\emptyset$\verb|>A| \end{verse} \noindent follows from (because of the `\verb|then|' at the end of line 51): \begin{verse}\footnotesize \verb|z |$\in$\verb| dom f| \end{verse} \noindent and: \begin{verse}\footnotesize \verb|A1: dom f = {<|$\emptyset$\verb|>A} & rng f = {a}| \end{verse} \noindent and: \begin{verse}\footnotesize \verb|definition let y; func {y} -> set means|\\ \verb|:: TARSKI:def 1|\\ \verb| x |$\in$\verb| it iff x = y;|\\ \verb|end| \end{verse} \begin{flushleft}\footnotesize \lineno\verb| hence thesis by FINSEQ_1:65;| \end{flushleft} The statement that is left to be proved: \begin{verse}\footnotesize \verb|z |$\in$\verb| A*| \end{verse} \noindent now follows from (the `\verb|hence|' includes a `\verb|then|'): \begin{verse}\footnotesize \verb|z = <|$\emptyset$\verb|>A| \end{verse} \noindent and the type of \verb|<|$\emptyset$\verb|>A| given by: \begin{verse}\footnotesize \verb|definition let D be set;|\\ \verb| func <|$\emptyset$\verb|>(D) -> empty FinSequence of D equals|\\ \verb| :: FINSEQ_1:def 6|\\ \verb| <|$\emptyset$\verb|>;|\\ \verb|end;| \end{verse} \noindent and: \begin{verse}\footnotesize \verb|theorem :: FINSEQ_1:65|\\ \verb| x |$\in$\verb| D* iff x is FinSequence of D;| \end{verse} \begin{flushleft}\footnotesize \lineno\verb| end;| \end{flushleft} {\ldots} and that completes the subproof. \begin{flushleft}\footnotesize \lineno\verb| rng f c= A|\\ \lineno\verb| proof|\\ \lineno\verb| let z; assume z |$\in$\verb| rng f; then|\\ \lineno\verb| z = a by A1,TARSKI:def 1;|\\ \lineno\verb| hence thesis;|\\ \lineno\verb| end; then| \end{flushleft} This subproof is similar to the previous one. The step in line 59 uses that: \begin{verse}\footnotesize \verb|a |$\in$\verb| A| \end{verse} \noindent This was explained in the text following the `\verb|consider|' in line 46. \begin{flushleft}\footnotesize \lineno\verb| reconsider f as PartFunc of A*,A by RELSET_1:11,A2;| \end{flushleft} After this \verb|reconsider| `\verb|f|' will keep the same meaning (it will still expand to `{\tt \verb|{|<$\emptyset$>A\verb|}|-->a}'), but its {\it type\/} will have become `{\tt PartFunc of A*,A}'. In order to justify this, one has to prove: \begin{verse}\footnotesize \verb|f is PartFunc of A*,A| \end{verse} \noindent which because of the definition of `\verb|f|' and the definition of \verb|mode| `\verb|PartFunc|': \begin{verse}\footnotesize \verb|definition let X,Y;|\\ \verb| mode PartFunc of X,Y is Function-like Relation of X,Y;|\\ \verb|end;| \end{verse} \noindent `expands' to: \begin{verse}\footnotesize \verb|{<|$\emptyset$\verb|>A}-->a is Function-like Relation of A*,A| \end{verse} \noindent This follows from: \begin{verse}\footnotesize \verb|A2: dom f c= A*| \end{verse} \noindent and (`\verb|then|' on line 60): \begin{verse}\footnotesize \verb|rng f c= A| \end{verse} \noindent and (from article `\verb|FUNCOP_1|'): \begin{verse}\footnotesize \verb|definition let A, z be set;|\\ \verb| cluster A --> z -> Function-like Relation-like;|\\ \verb|end;| \end{verse} \noindent and (from article `\verb|RELAT_1|'): \begin{verse}\footnotesize \verb|definition|\\ \verb| mode Relation is Relation-like set;|\\ \verb|end;| \end{verse} \noindent and: \begin{verse}\footnotesize \verb|theorem :: RELSET_1:11|\\ \verb| for R being Relation st dom R c= X & rng R c= Y holds|\\ \verb| R is Relation of X,Y;| \end{verse} \begin{flushleft}\footnotesize \lineno\verb| A3: f is homogeneous| \end{flushleft} This statement expands, because of the definition in lines 30--34, to: \begin{verse}\footnotesize \verb|A3: for x,y being FinSequence of A st x |$\in$\verb| dom f & y |$\in$\verb| dom f holds|\\ \verb| len x = len y| \end{verse} \begin{flushleft}\footnotesize \lineno\verb| proof|\\ \lineno\verb| let x,y be FinSequence of A; assume|\\ \lineno\verb| x |$\in$\verb| dom f & y |$\in$\verb| dom f; then| \end{flushleft} After this, the statement left to be proved is: \begin{verse}\footnotesize \verb|len x = len y| \end{verse} \begin{flushleft}\footnotesize \lineno\verb| x = <|$\emptyset$\verb|>A & y = <|$\emptyset$\verb|>A by TARSKI:def 1,A1;|\\ \end{flushleft} The statement: \begin{verse}\footnotesize \verb|x = <|$\emptyset$\verb|>A & y = <|$\emptyset$\verb|>A| \end{verse} \noindent follows from (`\verb|then|' in line 65): \begin{verse}\footnotesize \verb|x |$\in$\verb| dom f & y |$\in$\verb| dom f| \end{verse} \noindent and: \begin{verse}\footnotesize \verb|A1: dom f = {<|$\emptyset$\verb|>A} & rng f = {a}| \end{verse} \noindent and: \begin{verse}\footnotesize \verb|definition let y; func {y} -> set means|\\ \verb|:: TARSKI:def 1|\\ \verb| x |$\in$\verb| it iff x = y;|\\ \verb|end| \end{verse} \begin{flushleft}\footnotesize \lineno\verb| hence thesis;| \end{flushleft} Because (`\verb|hence|' refers to the previous statement): \begin{verse}\footnotesize \verb|x = <|$\emptyset$\verb|>A & y = <|$\emptyset$\verb|>A| \end{verse} \noindent the \verb|thesis| left to be proved: \begin{verse}\footnotesize \verb|len x = len y| \end{verse} \noindent is equivalent to: \begin{verse}\footnotesize \verb|len <|$\emptyset$\verb|>A = len <|$\emptyset$\verb|>A| \end{verse} \noindent which is true by reflexivity (equational reasoning is built into the Mizar system). \begin{flushleft}\footnotesize \lineno\verb| end;|\\ \lineno\verb| A4: f is quasi_total| \end{flushleft} This statement expands, because of the definition in lines 36--40, to: \begin{verse}\footnotesize \verb|for x,y being FinSequence of A st len x = len y & x |$\in$\verb| dom f holds|\\ \verb| y |$\in$\verb| dom f| \end{verse} \begin{flushleft}\footnotesize \lineno\verb| proof|\\ \lineno\verb| let x,y be FinSequence of A; assume|\\ \lineno\verb| A5: len x = len y & x |$\in$\verb| dom f; then| \end{flushleft} After this, the statement left to be proved is: \begin{verse}\footnotesize \verb|y |$\in$\verb| dom f| \end{verse} \begin{flushleft}\footnotesize \lineno\verb| x = <|$\emptyset$\verb|>A by TARSKI:def 1,A1; then| \end{flushleft} The statement: \begin{verse}\footnotesize \verb|x = <|$\emptyset$\verb|>A| \end{verse} \noindent follows from: \begin{verse}\footnotesize \verb|A1: dom f = {<|$\emptyset$\verb|>A} & rng f = {a}| \end{verse} \noindent and (`\verb|then|' in line 72): \begin{verse}\footnotesize \verb|len x = len y & x |$\in$\verb| dom f| \end{verse} \noindent and: \begin{verse}\footnotesize \verb|definition let y; func {y} -> set means|\\ \verb|:: TARSKI:def 1|\\ \verb| x |$\in$\verb| it iff x = y;|\\ \verb|end| \end{verse} \begin{flushleft}\footnotesize \lineno\verb| len x = 0 by FINSEQ_1:32; then| \end{flushleft} The statement: \begin{verse}\footnotesize \verb|len x = 0| \end{verse} \noindent follows from (`\verb|then|' in line 73): \begin{verse}\footnotesize \verb|x = <|$\emptyset$\verb|>A| \end{verse} \noindent and: \begin{verse}\footnotesize \verb|theorem :: FINSEQ_1:32|\\ \verb| p=<|$\emptyset$\verb|>(D) iff len p = 0;| \end{verse} \begin{flushleft}\footnotesize \lineno\verb| y = <|$\emptyset$\verb|>A by FINSEQ_1:32,A5;| \end{flushleft} The statement: \begin{verse}\footnotesize \verb|y = <|$\emptyset$\verb|>A| \end{verse} \noindent follows from: \begin{verse}\footnotesize \verb|A5: len x = len y & x |$\in$\verb| dom f| \end{verse} \noindent and (`\verb|then|' in line 74): \begin{verse}\footnotesize \verb|len x = 0| \end{verse} \noindent and: \begin{verse}\footnotesize \verb|theorem :: FINSEQ_1:32|\\ \verb| p=<|$\emptyset$\verb|>(D) iff len p = 0;| \end{verse} \begin{flushleft}\footnotesize \lineno\verb| hence thesis by A1,TARSKI:def 1;| \end{flushleft} The \verb|thesis| left to be proved: \begin{verse}\footnotesize \verb|y |$\in$\verb| dom f| \end{verse} \noindent follows from (`\verb|hence|'): \begin{verse}\footnotesize \verb|y = <|$\emptyset$\verb|>A| \end{verse} \noindent and: \begin{verse}\footnotesize \verb|A1: dom f = {<|$\emptyset$\verb|>A} & rng f = {a}| \end{verse} \noindent and: \begin{verse}\footnotesize \verb|definition let y; func {y} -> set means|\\ \verb|:: TARSKI:def 1|\\ \verb| x |$\in$\verb| it iff x = y;|\\ \verb|end| \end{verse} \begin{flushleft}\footnotesize \lineno\verb| end;|\\ \lineno\verb| f is non empty by RELAT_1:60,FUNCOP_1:14;| \end{flushleft} The statement: \begin{verse}\footnotesize \verb|f is non empty| \end{verse} \noindent expands to: \begin{verse}\footnotesize \verb|{<|$\emptyset$\verb|>A}-->a is non empty| \end{verse} \noindent which follows from: \begin{verse}\footnotesize \verb|theorem :: RELAT_1:60|\\ \verb| dom |$\emptyset$\verb| = |$\emptyset$\verb| & rng |$\emptyset$\verb| = |$\emptyset$\verb|;| \end{verse} \noindent and: \begin{verse}\footnotesize \verb|theorem :: FUNCOP_1:14|\\ \verb| A <> |$\emptyset$\verb| implies dom (A --> x) = A & rng (A --> x) = {x};| \end{verse} \noindent and the cluster (from article `\verb|TARSKI|'): \begin{verse}\footnotesize \verb|definition let y;|\\ \verb| cluster {y} -> non empty;|\\ \verb|end;| \end{verse} The knowledge that: \begin{verse}\footnotesize \verb|A is empty implies A = |$\emptyset$ \end{verse} \noindent is built into the Mizar reasoner. \begin{flushleft}\footnotesize \lineno\verb| hence thesis by A3,A4;| \end{flushleft} The \verb|thesis| to be proved is: \begin{verse}\footnotesize \verb|ex f being PartFunc of A*,A st|\\ \verb| f is homogeneous & f is quasi_total & f is non empty| \end{verse} This follows from the fact that for the specific `defined' \verb|f| from lines 47 and 61 we know that: \begin{verse}\footnotesize \verb|f is homogeneous & f is quasi_total & f is non empty| \end{verse} \noindent which follows from: \begin{verse}\footnotesize \verb|A3: f is homogeneous| \end{verse} \noindent and: \begin{verse}\footnotesize \verb|A4: f is quasi_total| \end{verse} \noindent and (`\verb|hence|'): \begin{verse}\footnotesize \verb|f is non empty| \end{verse} Note that Mizar is able to figure out the introduction of the existential quantifier \verb|ex| by itself, without having to be told that `\verb|f|' is the witnessing object. \begin{flushleft}\footnotesize \lineno\verb| end;| \end{flushleft} This finishes the annotated proof. \begin{flushleft}\footnotesize \lineno\verb|end;| \lineinc \medskip \lineno\verb|theorem Th1:|\\ \lineno\verb|h is non empty iff dom h <> |$\emptyset$\verb| by RELAT_1:64,RELAT_1:60;| \lineinc \medskip \lineno\verb|theorem Th2:|\\ \lineno\verb|for A being non empty set, a being Element of A|\\ \lineno\verb|holds {<|$\emptyset$\verb|>A} -->a is homogeneous quasi_total non empty PartFunc of A*,A| \end{flushleft} Note that this theorem already has been proved inside the proof of the \verb|cluster| (lines 47, 61, 62, 69 and 78), but that the \verb|cluster| has to be present in order to state the theorem. \begin{flushleft}\footnotesize \lineno\verb| proof let A be non empty set, a be Element of A;|\label{th2}\\ \lineno\verb| set f = {<|$\emptyset$\verb|>A} -->a;|\\ \lineno\verb| A1: dom f = {<|$\emptyset$\verb|>A} & rng f = {a} by FUNCOP_1:14;|\\ \lineno\verb| A2: dom f c= A*|\\ \lineno\verb| proof|\\ \lineno\verb| let z; assume z |$\in$\verb| dom f; then|\\ \lineno\verb| z = <|$\emptyset$\verb|>A by TARSKI:def 1,A1;|\\ \lineno\verb| hence thesis by FINSEQ_1:65;|\\ \lineno\verb| end;|\\ \lineno\verb| rng f c= A|\\ \lineno\verb| proof|\\ \lineno\verb| let z; assume z |$\in$\verb| rng f; then|\\ \lineno\verb| z = a by A1,TARSKI:def 1;|\\ \lineno\verb| hence thesis;|\\ \lineno\verb| end; then|\\ \lineno\verb| reconsider f as PartFunc of A*,A by RELSET_1:11,A2;|\\ \lineno\verb| A3: f is homogeneous|\\ \lineno\verb| proof|\\ \lineno\verb| let x,y be FinSequence of A; assume|\\ \lineno\verb| x |$\in$\verb| dom f & y |$\in$\verb| dom f; then|\\ \lineno\verb| x = <|$\emptyset$\verb|>A & y = <|$\emptyset$\verb|>A by TARSKI:def 1,A1;|\\ \lineno\verb| hence thesis;|\\ \lineno\verb| end;|\\ \lineno\verb| A4: f is quasi_total|\\ \lineno\verb| proof|\\ \lineno\verb| let x,y be FinSequence of A; assume|\\ \lineno\verb| A5: len x = len y & x |$\in$\verb| dom f; then|\\ \lineno\verb| x = <|$\emptyset$\verb|>A by TARSKI:def 1,A1; then|\\ \lineno\verb| len x = 0 by FINSEQ_1:32; then|\\ \lineno\verb| y = <|$\emptyset$\verb|>A by FINSEQ_1:32,A5;|\\ \lineno\verb| hence thesis by A1,TARSKI:def 1;|\\ \lineno\verb| end;|\\ \lineno\verb| thus thesis by A3,A4,A1,Th1;|\\ \lineno\verb| end;| \lineinc \medskip \lineno\verb|theorem Th3:|\\ \lineno\verb|for A being non empty set, a being Element of A|\\ \lineno\verb| holds {<|$\emptyset$\verb|>A} -->a is Element of PFuncs(A*,A)|\\ \lineno\verb| proof let A be non empty set, a be Element of A;|\\ \lineno\verb| set f = {<|$\emptyset$\verb|>A} -->a;|\\ \lineno\verb| A1: dom f = {<|$\emptyset$\verb|>A} & rng f = {a} by FUNCOP_1:14;|\\ \lineno\verb| A2: dom f c= A*|\\ \lineno\verb| proof|\\ \lineno\verb| let z; assume z |$\in$\verb| dom f; then|\\ \lineno\verb| z = <|$\emptyset$\verb|>A by TARSKI:def 1,A1;|\\ \lineno\verb| hence thesis by FINSEQ_1:65;|\\ \lineno\verb| end;|\\ \lineno\verb| rng f c= A|\\ \lineno\verb| proof|\\ \lineno\verb| let z; assume z |$\in$\verb| rng f; then|\\ \lineno\verb| z = a by A1,TARSKI:def 1;|\\ \lineno\verb| hence thesis;|\\ \lineno\verb| end; then|\\ \lineno\verb| reconsider f as PartFunc of A*,A by RELSET_1:11,A2;|\\ \lineno\verb| f |$\in$\verb| PFuncs(A*,A) by PARTFUN1:119;|\\ \lineno\verb| hence {<|$\emptyset$\verb|>A} -->a is Element of PFuncs(A*,A);|\\ \lineno\verb| end;| \lineinc \medskip \lineno\verb|definition let A;|\\ \lineno\verb| mode PFuncFinSequence of A -> FinSequence of PFuncs(A*,A) means|\\ \lineno\verb|:Def3: not contradiction;|\\ \lineno\verb| existence;| \end{flushleft} The correctness condition of a \verb|mode| definition is the non-emptiness of the defined type, which is an `\verb|existence|' statement. In this case this statement becomes: \begin{verse}\footnotesize \verb|ex c being FinSequence of PFuncs(A*,A) st not contradiction| \end{verse} Because Mizar types all are non-empty, the existence of a `\verb|c|' of the appropriate type is obvious, and of course it satisfies `{\tt not contradiction}'. So this statement needs no justification. \begin{flushleft}\footnotesize \lineno\verb|end;| \lineinc \medskip \lineno\verb|struct (1-sorted) UAStr |$\langle\!\langle$\verb| carrier -> set,|\\ \lineno\verb| charact -> PFuncFinSequence of the carrier|$\rangle\!\rangle$\verb|;| \lineinc \medskip \lineno\verb|definition|\\ \lineno\verb| cluster non empty strict UAStr;|\\ \lineno\verb| existence|\\ \lineno\verb| proof consider D being non empty set, c being PFuncFinSequence of D;|\\ \lineno\verb| take UAStr |$\langle\!\langle$\verb|D,c |$\rangle\!\rangle$\verb|;|\\ \lineno\verb| thus the carrier of UAStr |$\langle\!\langle$\verb|D,c |$\rangle\!\rangle$\verb| is non empty;|\\ \lineno\verb| thus thesis;|\\ \lineno\verb| end;|\\ \lineno\verb|end;| \lineinc \medskip \lineno\verb|definition let D be non empty set, c be PFuncFinSequence of D;|\\ \lineno\verb| cluster UAStr |$\langle\!\langle$\verb|D,c |$\rangle\!\rangle$\verb| -> non empty;|\\ \lineno\verb| coherence| \end{flushleft} The \verb|correctness| condition of a \verb|cluster| of this kind is called `\verb|coherence|'. Here, of course, it is: \begin{verse}\footnotesize \verb|UAStr|$\langle\!\langle$\verb|D,c|$\rangle\!\rangle$\verb| is non empty| \end{verse} Because of the `\verb|definitions STRUCT_0;|' directive in line 15 this expands to: \begin{verse}\footnotesize \verb|the carrier of UAStr|$\langle\!\langle$\verb|D,c|$\rangle\!\rangle$\verb| is non empty| \end{verse} \noindent which reduces to: \begin{verse}\footnotesize \verb|D is non empty| \end{verse} \noindent which follows from the type of `\verb|D|' in line 166. \begin{flushleft}\footnotesize \lineno\verb| proof|\\ \lineno\verb| thus the carrier of UAStr |$\langle\!\langle$\verb|D,c |$\rangle\!\rangle$\verb| is non empty;|\\ \lineno\verb| end;|\\ \lineno\verb|end;| \lineinc \medskip \lineno\verb|definition let A;|\\ \lineno\verb| let IT be PFuncFinSequence of A;|\\ \lineno\verb|attr IT is homogeneous means :Def4:|\\ \lineno\verb| for n,h st n |$\in$\verb| dom IT & h = IT.n holds h is homogeneous;|\\ \lineno\verb|end;| \lineinc \medskip \lineno\verb|definition let A;|\\ \lineno\verb| let IT be PFuncFinSequence of A;|\\ \lineno\verb|attr IT is quasi_total means :Def5:|\\ \lineno\verb| for n,h st n |$\in$\verb| dom IT & h = IT.n holds h is quasi_total;|\\ \lineno\verb|end;| \lineinc \medskip \lineno\verb|definition let F be Function;|\\ \lineno\verb|redefine attr F is non-empty means :Def6:|\\ \lineno\verb| for n being set st n |$\in$\verb| dom F holds F.n is non empty;|\\ \lineno\verb| compatibility| \end{flushleft} The \verb|correctness| condition for the redefinition of a `\verb|pred|' or `\verb|attr|' is called `\verb|compatibility|'. In this case, it is: \begin{verse}\footnotesize \verb|F is non empty iff |\\ \verb| for n being set st n |$\in$\verb| dom F holds F.n is non empty| \end{verse} In this statement and its proof `{\tt non empty}' still has the `old' definition, which is: \begin{verse}\footnotesize \verb|definition let F be Function;|\\ \verb| attr F is non-empty means|\\ \verb| :: ZF_REFLE:def 4|\\ \verb| not |$\emptyset$\verb| |$\in$\verb| rng F;|\\ \verb|end;| \end{verse} \begin{flushleft}\footnotesize \lineno\verb| proof|\\ \lineno\verb| hereby assume F is non-empty; then| \end{flushleft} The `\verb|hereby|' keyword behaves like the combination of `\verb|thus|' and `\verb|now|' (this construction is not in the official Mizar grammar from appendix \ref{grammar} on page \pageref{grammar}). \begin{flushleft}\footnotesize \lineno\verb|A1: not |$\emptyset$\verb| |$\in$\verb| rng F by ZF_REFLE:def 4;|\\ \lineno\verb| let i be set;|\\ \lineno\verb| assume i |$\in$\verb| dom F;|\\ \lineno\verb| hence F.i is non empty by A1,FUNCT_1:11;|\\ \lineno\verb| end;|\\ \lineno\verb| assume |\\ \lineno\verb|A2: for n being set st n |$\in$\verb| dom F holds F.n is non empty;|\\ \lineno\verb| assume |$\emptyset$\verb| |$\in$\verb| rng F;|\\ \lineno\verb| then ex i being set st i |$\in$\verb| dom F & F.i = |$\emptyset$\verb| by FUNCT_1:11;|\\ \lineno\verb| hence contradiction by A2;|\\ \lineno\verb| end;|\\ \lineno\verb|end;| \lineinc \medskip \lineno\verb|definition let A be non empty set; let x be Element of PFuncs(A*,A);|\\ \lineno\verb| redefine|\\ \lineno\verb| func <*x*> -> PFuncFinSequence of A;|\\ \lineno\verb| coherence| \end{flushleft} The \verb|correctness| conditions for the redefinition of a `\verb|func|', are `\verb|coherence|' in case the type changes, and `\verb|compatibility|' in case the `definition' changes. In this case only the first applies and the condition of course is: \begin{verse}\footnotesize \verb|<*x*> is PFuncFinSequence| \end{verse} \begin{flushleft}\footnotesize \lineno\verb| proof|\\ \lineno\verb| <*x*> is FinSequence of PFuncs(A*,A);|\\ \lineno\verb| hence thesis by Def3;|\\ \lineno\verb| end;|\\ \lineno\verb|end;| \lineinc \medskip \lineno\verb|definition let A be non empty set;|\\ \lineno\verb|cluster homogeneous quasi_total non-empty PFuncFinSequence of A;|\\ \lineno\verb| existence|\\ \lineno\verb| proof|\\ \lineno\verb| consider a being Element of A;|\\ \lineno\verb| reconsider f = {<|$\emptyset$\verb|>A} -->a as PartFunc of A*,A by Th2;|\\ \lineno\verb| reconsider f as Element of PFuncs(A*,A) by PARTFUN1:119;|\\ \lineno\verb| take <*f*>;|\\ \lineno\verb| thus <*f*> is homogeneous|\\ \lineno\verb| proof|\\ \lineno\verb| let n; let h be PartFunc of A*,A; assume|\\ \lineno\verb| A1: n |$\in$\verb| dom <*f*> & h =<*f*>.n; |\\ \lineno\verb| then n |$\in$\verb| {1} by FINSEQ_1:4,FINSEQ_1:def 8; then|\\ \lineno\verb| h = <*f*>.1 by A1,TARSKI:def 1; |\\ \lineno\verb| then h = f & f is homogeneous PartFunc of A*,A by Th2,FINSEQ_1:def 8;|\\ \lineno\verb| hence thesis;|\\ \lineno\verb| end;|\\ \lineno\verb| thus <*f*> is quasi_total|\\ \lineno\verb| proof|\\ \lineno\verb| let n; let h be PartFunc of A*,A; assume|\\ \lineno\verb| A2: n |$\in$\verb| dom <*f*> & h =<*f*>.n; |\\ \lineno\verb| then n |$\in$\verb| {1} by FINSEQ_1:4,FINSEQ_1:def 8; then|\\ \lineno\verb| h = <*f*>.1 by A2,TARSKI:def 1; |\\ \lineno\verb| then h = f & f is quasi_total PartFunc of A*,A by Th2,FINSEQ_1:def 8;|\\ \lineno\verb| hence thesis;|\\ \lineno\verb| end;|\\ \lineno\verb| thus <*f*> is non-empty|\\ \lineno\verb| proof|\\ \lineno\verb| let n be set; assume|\\ \lineno\verb| A3: n |$\in$\verb| dom <*f*>;|\\ \lineno\verb| then reconsider n as Nat; |\\ \lineno\verb| n |$\in$\verb| {1} by FINSEQ_1:4,A3,FINSEQ_1:def 8; then|\\ \lineno\verb| n = 1 by TARSKI:def 1; then|\\ \lineno\verb| <*f*>.n=f by FINSEQ_1:def 8; |\\ \lineno\verb| hence thesis by Th2;|\\ \lineno\verb| end;|\\ \lineno\verb| end;|\\ \lineno\verb|end;| \lineinc \medskip \lineno\verb|reserve U for UAStr;| \lineinc \medskip \lineno\verb|definition let IT be UAStr;|\\ \lineno\verb|attr IT is partial means :Def7:|\\ \lineno\verb| the charact of IT is homogeneous;|\\ \lineno\verb|attr IT is quasi_total means :Def8:|\\ \lineno\verb| the charact of IT is quasi_total;|\\ \lineno\verb|attr IT is non-empty means :Def9:|\\ \lineno\verb| the charact of IT <> <|$\emptyset$\verb|> & the charact of IT is non-empty;|\\ \lineno\verb|end;| \lineinc \medskip \lineno\verb|reserve A for non empty set,|\\ \lineno\verb| h for PartFunc of A*,A ,|\\ \lineno\verb| x,y for FinSequence of A,|\\ \lineno\verb| a for Element of A;| \lineinc \medskip \lineno\verb|theorem Th4:|\\ \lineno\verb|for x be Element of PFuncs(A*,A) st x = {<|$\emptyset$\verb|>A} --> a holds|\\ \lineno\verb| <*x*> is homogeneous quasi_total non-empty|\\ \lineno\verb| proof let x be Element of PFuncs(A*,A) such that|\\ \lineno\verb| A1: x = {<|$\emptyset$\verb|>A} --> a;|\\ \end{flushleft} The `\verb|let| {\ldots} \verb|such that|' construction corresponds to a `\verb|for| {\ldots} \verb|st|' in the statement, so it is equivalent to a `\verb|let|' followed by an `\verb|assume|'. \begin{flushleft}\footnotesize \lineno\verb| reconsider f=x as PartFunc of A*,A by PARTFUN1:121;|\\ \lineno\verb| A2: for n,h st n |$\in$\verb| dom <*x*> & h = <*x*>.n holds h is homogeneous|\\ \lineno\verb| proof let n,h; assume|\\ \lineno\verb| A3: n |$\in$\verb| dom <*x*> & h =<*x*>.n;|\\ \lineno\verb| then n |$\in$\verb| {1} by FINSEQ_1:4,FINSEQ_1:def 8; then|\\ \lineno\verb| h = <*x*>.1 by A3,TARSKI:def 1;|\\ \lineno\verb| then h = x & f is homogeneous PartFunc of A*,A by Th2,A1,FINSEQ_1:def 8;|\\ \lineno\verb| hence thesis;|\\ \lineno\verb| end;|\\ \lineno\verb| A4: for n,h st n |$\in$\verb| dom <*x*> & h = <*x*>.n holds h is quasi_total|\\ \lineno\verb| proof let n,h; assume|\\ \lineno\verb| A5: n |$\in$\verb| dom <*x*> & h =<*x*>.n;|\\ \lineno\verb| then n |$\in$\verb| {1} by FINSEQ_1:4,FINSEQ_1:def 8; then|\\ \lineno\verb| h = <*x*>.1 by A5,TARSKI:def 1;|\\ \lineno\verb| then h = x & f is quasi_total PartFunc of A*,A by Th2,A1,FINSEQ_1:def 8;|\\ \lineno\verb| hence thesis;|\\ \lineno\verb| end;|\\ \lineno\verb| for n being set st n |$\in$\verb| dom <*x*> holds <*x*>.n is non empty|\\ \lineno\verb| proof let n be set; assume|\\ \lineno\verb| n |$\in$\verb| dom <*x*>;|\\ \lineno\verb| then n |$\in$\verb| {1} by FINSEQ_1:4,FINSEQ_1:def 8; then|\\ \lineno\verb| <*x*>.n = <*x*>.1 by TARSKI:def 1;|\\ \lineno\verb| then <*x*>.n = x & f is non empty PartFunc of A*,A by Th2,A1|\\ \lineno\verb|,FINSEQ_1:def 8;|\\ \lineno\verb| hence thesis;|\\ \lineno\verb| end;|\\ \lineno\verb| hence thesis by A2,A4,Def6,Def5,Def4;|\\ \lineno\verb| end;| \lineinc \medskip \lineno\verb|definition|\\ \lineno\verb| cluster quasi_total partial non-empty strict non empty UAStr;|\\ \lineno\verb| existence|\\ \lineno\verb| proof|\\ \lineno\verb| consider A be non empty set;|\\ \lineno\verb| consider a be Element of A;|\\ \lineno\verb| set f = {<|$\emptyset$\verb|>A} --> a;|\\ \lineno\verb| reconsider w = f as Element of PFuncs(A*,A) by Th3;|\\ \lineno\verb| set U = UAStr |$\langle\!\langle$\verb| A, <*w*> |$\rangle\!\rangle$\verb|;|\\ \lineno\verb| take U;|\\ \lineno\verb| A1: the charact of(U) is quasi_total &|\\ \lineno\verb| the charact of(U) is homogeneous & the charact of(U) is non-empty|\\ \lineno\verb| by Th4;|\\ \lineno\verb| the charact of(U) <> <|$\emptyset$\verb|>|\\ \lineno\verb| proof assume A2: the charact of(U) = <|$\emptyset$\verb|>;|\\ \lineno\verb| A3: len(the charact of(U)) = 1 by FINSEQ_1:56;|\\ \lineno\verb| len (<|$\emptyset$\verb|>) = 0 by FINSEQ_1:25;|\\ \lineno\verb| hence contradiction by A3,A2;|\\ \lineno\verb| end;|\\ \lineno\verb| hence thesis by A1,Def9,Def8,Def7;|\\ \lineno\verb| end;|\\ \lineno\verb|end;| \lineinc \medskip \lineno\verb|definition let U be partial UAStr;|\\ \lineno\verb| cluster the charact of U -> homogeneous;|\\ \lineno\verb| coherence by Def7;|\\ \lineno\verb|end;| \lineinc \medskip \lineno\verb|definition let U be quasi_total UAStr;|\\ \lineno\verb| cluster the charact of U -> quasi_total;|\\ \lineno\verb| coherence by Def8;|\\ \lineno\verb|end;| \lineinc \medskip \lineno\verb|definition let U be non-empty UAStr;|\\ \lineno\verb| cluster the charact of U -> non-empty non empty;|\\ \lineno\verb| coherence by Def9;|\\ \lineno\verb|end;| \lineinc \medskip \lineno\verb|definition|\\ \lineno\verb|mode Universal_Algebra is quasi_total partial non-empty non empty UAStr;|\\ \lineno\verb|end;| \lineinc \medskip \lineno\verb|reserve U for partial non-empty non empty UAStr;| \lineinc \medskip \lineno\verb|definition|\\ \lineno\verb| let A;|\\ \lineno\verb| let f be homogeneous non empty PartFunc of A*,A;|\\ \lineno\verb|func arity(f) -> Nat means|\\ \lineno\verb| x |$\in$\verb| dom f implies it = len x;|\\ \lineno\verb| existence| \end{flushleft} The \verb|correctness| conditions of the \verb|definition| of a \verb|func| consists of an `{\tt ex\-is\-tence}' and a `\verb|uniqueness|' part. In this case the `{\tt existence}' condition is: \begin{verse}\footnotesize \verb|ex n st|\\ \verb| for x st x |$\in$\verb| dom f holds n = len x| \end{verse} \begin{flushleft}\footnotesize \lineno\verb| proof|\\ \lineno\verb| ex n st for x st x |$\in$\verb| dom f holds n = len x|\\ \lineno\verb| proof|\\ \lineno\verb|A1: dom f <> |$\emptyset$\verb| by Th1;|\\ \lineno\verb| consider x being Element of dom f;|\\ \lineno\verb| dom f c= A* by RELSET_1:12; then|\\ \lineno\verb| x |$\in$\verb| A* by A1,TARSKI:def 3; then|\\ \lineno\verb| reconsider x as FinSequence of A by FINSEQ_1:65;|\\ \lineno\verb| take n = len x;|\\ \lineno\verb| let y; assume y |$\in$\verb| dom f;|\\ \lineno\verb| hence n = len y by Def1;|\\ \lineno\verb| end;|\\ \lineno\verb| hence thesis;|\\ \lineno\verb| end;|\\ \lineno\verb| uniqueness| \end{flushleft} The `\verb|uniqueness|' condition is: \begin{verse}\footnotesize \verb|for n,m st|\\ \verb| (for x st x |$\in$\verb| dom f holds n = len x) &|\\ \verb| (for x st x |$\in$\verb| dom f holds m = len x) holds|\\ \verb| n = m| \end{verse} \begin{flushleft}\footnotesize \lineno\verb| proof|\\ \lineno\verb| let n,m such that A2: (for x st x |$\in$\verb| dom f holds n = len x) &|\\ \lineno\verb| for x st x |$\in$\verb| dom f holds m = len x;|\\ \lineno\verb|A3: dom f <> |$\emptyset$\verb| by Th1;|\\ \lineno\verb| consider x being Element of dom f;|\\ \lineno\verb| dom f c= A* by RELSET_1:12; then|\\ \lineno\verb| x |$\in$\verb| A* by A3,TARSKI:def 3; then|\\ \lineno\verb| reconsider x as FinSequence of A by FINSEQ_1:65;|\\ \lineno\verb| n = len x & m = len x by A3,A2;|\\ \lineno\verb| hence thesis;|\\ \lineno\verb| end;|\\ \lineno\verb|end;| \lineinc \medskip \lineno\verb|theorem Th5:|\\ \lineno\verb|for U holds for n st n|$\in$\verb|dom the charact of(U) holds|\\ \lineno\verb| (the charact of(U)).n is|\\ \lineno\verb| PartFunc of (the carrier of U)*,the carrier of U|\\ \lineno\verb| proof let U,n;|\\ \lineno\verb| set pu = PFuncs((the carrier of U)*, the carrier of U),|\\ \lineno\verb| o = the charact of(U); assume|\\ \lineno\verb| n|$\in$\verb|dom o; then|\\ \lineno\verb| o.n |$\in$\verb| rng o & rng o c= pu by FUNCT_1:12,FINSEQ_1:def 4; |\\ \lineno\verb|hence thesis by PARTFUN1:121;|\\ \lineno\verb| end;| \lineinc \medskip \lineno\verb|definition let U;|\\ \lineno\verb|func signature(U) ->FinSequence of NAT means|\\ \lineno\verb| len it = len the charact of(U) &|\\ \lineno\verb| for n st n |$\in$\verb| dom it holds|\\ \lineno\verb| for h be homogeneous non empty|\\ \lineno\verb| PartFunc of (the carrier of U )*,the carrier of U|\\ \lineno\verb| st h = (the charact of(U)).n|\\ \lineno\verb| holds it.n = arity(h);|\\ \lineno\verb| existence|\\ \lineno\verb| proof|\\ \lineno\verb| defpred P[Nat,set] means|\\ \lineno\verb| for h be homogeneous non empty|\\ \lineno\verb| PartFunc of (the carrier of U )*,the carrier of U|\\ \lineno\verb| st h = (the charact of(U)).$1|\\ \lineno\verb| holds $2 = arity(h);| \end{flushleft} A `\verb|defpred|' defines a `local' predicate: it's like `\verb|set|', but for predicates instead of expressions. It's expanded everywhere (this one is used in lines 415 and 419). The arguments are in the `body' referred to as `\verb|$1|', `\verb|$2|', {\ldots} Because the highest index allowed is `\verb|$8|', a `\verb|deffunc|' or `\verb|defpred|' takes at most eight arguments. \begin{flushleft}\footnotesize \lineno\verb| A1: now let m; assume|\\ \lineno\verb| m|$\in$\verb| Seg len the charact of(U); then|\\ \lineno\verb| m|$\in$\verb| dom the charact of(U) by FINSEQ_1:def 3; then|\\ \lineno\verb| reconsider H=(the charact of(U)).m as homogeneous non empty|\\ \lineno\verb| PartFunc of (the carrier of U )*,the carrier of U by Th5,Def4,Def6;|\\ \lineno\verb| take n=arity(H);|\\ \lineno\verb| thus P[m,n];|\\ \lineno\verb| end;|\\ \lineno\verb| consider p be FinSequence of NAT such that|\\ \lineno\verb| A2: dom p = Seg(len the charact of(U)) and|\\ \lineno\verb| A3: for m st m |$\in$\verb| Seg(len the charact of(U)) holds P[m,p.m] from SeqDEx(A1);| \end{flushleft} The `\verb|SeqDEx|' \verb|scheme| from article `\verb|MATRIX_2|' is defined as: \begin{verse}\footnotesize \verb|scheme SeqDEx{D()->non empty set,A()->Nat,P[set,set]}:| \verb| ex p being FinSequence of D() st dom p = Seg A() &|\\ \verb| for k st k |$\in$\verb| Seg A() holds P[k,p.k]| \verb|provided| \verb| for k st k |$\in$\verb| Seg A() ex x being Element of D() st P[k,x];| \end{verse} \noindent (Note that references to schemes are by name instead of by number: the Mizar library contains 546 schemes, less than the number of articles.) It is used here to derive: \begin{verse}\footnotesize \verb|ex p be FinSequence of NAT st|\\ \verb| dom p = Seg(len the charact of(U)) &|\\ \verb| for m st m |$\in$\verb| Seg(len the charact of(U)) holds P[m,p.m]| \end{verse} \noindent (which is needed for the `\verb|consider|' statement), from: \begin{verse}\footnotesize \verb|A1: for m st m|$\in$\verb| Seg len the charact of(U) holds ex n st P[m,n]| \end{verse} \noindent So in this case the instantiation of the \verb|scheme| is: \begin{verse}\footnotesize \makebox[6em][r]{{\tt D()}}\quad$\rightarrow$\quad\verb|NAT|\\ \makebox[6em][r]{{\tt A()}}\quad$\rightarrow$\quad\verb|len the charact of U|\\ \makebox[6em][r]{{\tt P[k,x]}}\quad$\rightarrow$\quad\verb|P[k,x]| \end{verse} \noindent This substitution is not given explicitely, but is found by matching the `argument' `\verb|A1|' with the `condition' after the `\verb|provided|' in the \verb|scheme|, and the statement to be proved with the `conclusion' of the scheme. \begin{flushleft}\footnotesize \lineno\verb| take p;|\\ \lineno\verb|Seg len the charact of(U) = dom the charact of(U) by FINSEQ_1: def 3;|\\ \lineno\verb| hence A4: len p = len the charact of(U) by A2,FINSEQ_3:31;|\\ \lineno\verb| let n; assume|\\ \lineno\verb| n |$\in$\verb| dom p; then|\\ \lineno\verb| A5: n |$\in$\verb| Seg(len the charact of(U)) by FINSEQ_1:def 3,A4;|\\ \lineno\verb| let h be homogeneous non empty|\\ \lineno\verb| PartFunc of (the carrier of U )*,the carrier of U; assume|\\ \lineno\verb| h = (the charact of U).n;|\\ \lineno\verb| hence p.n = arity(h) by A5,A3;|\\ \lineno\verb| end;|\\ \lineno\verb| uniqueness|\\ \lineno\verb| proof|\\ \lineno\verb| let x,y be FinSequence of NAT; assume that|\\ \lineno\verb| A6: len x = len the charact of(U) and|\\ \lineno\verb| A7: for n st n |$\in$\verb| dom x holds for h be homogeneous non empty|\\ \lineno\verb| PartFunc of (the carrier of U )*,the carrier of U|\\ \lineno\verb| st h = (the charact of(U)).n|\\ \lineno\verb| holds x.n = arity(h) and|\\ \lineno\verb| A8: len y = len the charact of(U) and|\\ \lineno\verb| A9: for n st n |$\in$\verb| dom y holds for h be homogeneous non empty|\\ \lineno\verb| PartFunc of (the carrier of U )*,the carrier of U|\\ \lineno\verb| st h = (the charact of(U)).n|\\ \lineno\verb| holds y.n = arity(h);|\\ \lineno\verb| now let m; assume|\\ \lineno\verb| 1|$\le$\verb|m & m|$\le$\verb|len x; then|\\ \lineno\verb| m |$\in$\verb| Seg len x by FINSEQ_1:3; then|\\ \lineno\verb| m |$\in$\verb| dom x by FINSEQ_1:def 3;|\\ \lineno\verb| then A10: m |$\in$\verb| dom the charact of(U) & m|$\in$\verb|dom x & m|$\in$\verb|dom y|\\ \lineno\verb| by A6,A8,FINSEQ_3:31;|\\ \lineno\verb| then reconsider h=(the charact of(U)).m|\\ \lineno\verb| as homogeneous non empty|\\ \lineno\verb| PartFunc of (the carrier of U )*,the carrier of U by Th5,Def4,Def6;|\\ \lineno\verb| x.m=arity(h) & y.m=arity(h) by A7,A9,A10;|\\ \lineno\verb| hence x.m=y.m;|\\ \lineno\verb| end;|\\ \lineno\verb| hence thesis by A6,A8,FINSEQ_1:18;|\\ \lineno\verb| end;|\\ \lineno\verb|end;| \end{flushleft} \end{document}