Formalized Mathematics    (ISSN 0777-4028)
Volume 4, Number 1 (1993): pdf, ps, dvi.
  1. Katarzyna Zawadzka. The Product and the Determinant of Matrices with Entries in a Field, Formalized Mathematics 4(1), pages 1-8, 1993. MML Identifier: MATRIX_3
    Summary: Concerned with a generalization of concepts introduced in \cite{MATRIX_1.ABS}, i.e. there are introduced the sum and the product of matrices of any dimension of elements of any field.
  2. Yuji Sakai, Jaroslaw Kotowicz. Introduction to Theory of Rearrangement, Formalized Mathematics 4(1), pages 9-13, 1993. MML Identifier: REARRAN1
    Summary: An introduction to the rearrangement theory for finite functions (e.g. with the finite domain and codomain). The notion of generators and cogenerators of finite sets (equivalent to the order in the language of finite sequences) has been defined. The notion of rearrangement for a function into finite set is presented. Some basic properties of these notions have been proved.
  3. Andrzej Trybulec. Many-sorted Sets, Formalized Mathematics 4(1), pages 15-22, 1993. MML Identifier: PBOOLE
    Summary: The article deals with parameterized families of sets. When treated in a similar way as sets (due to systematic overloading notation used for sets) they are called many sorted sets. For instance, if $x$ and $X$ are two many-sorted sets (with the same set of indices $I$) then relation $x \in X$ is defined as $\forall_{i \in I} x_i \in X_i$.\par I was prompted by a remark in a paper by Tarlecki and Wirsing: ``Throughout the paper we deal with many-sorted sets, functions, relations etc. ... We feel free to use any standard set-theoretic notation without explicit use of indices'' \cite[p.~97]{Tar-Wir1}. The aim of this work was to check the feasibility of such approach in Mizar. It works.\par Let us observe some peculiarities: \begin{itemize} \item[-] empty set (i.e. the many sorted set with empty set of indices) belongs to itself (theorem 133), \item[-] we get two different inclusions $X \subseteq Y$ iff $\forall_{i \in I} X_i \subseteq Y_i$ and $X \sqsubseteq Y$ iff $\forall_x x \in X \Rightarrow x \in Y$ equivalent only for sets that yield non empty values. \end{itemize} Therefore the care is advised.
  4. Ewa Burakowska. Subalgebras of the Universal Algebra. Lattices of Subalgebras, Formalized Mathematics 4(1), pages 23-27, 1993. MML Identifier: UNIALG_2
    Summary: Introduces a definition of a subalgebra of a universal algebra. A notion of similar algebras and basic operations on subalgebras such as a subalgebra generated by a set, the intersection and the sum of two subalgebras were introduced. Some basic facts concerning the above notions have been proved. The article also contains the definition of a lattice of subalgebras of a universal algebra.
  5. Bogdan Nowak, Andrzej Trybulec. Hahn-Banach Theorem, Formalized Mathematics 4(1), pages 29-34, 1993. MML Identifier: HAHNBAN
    Summary: We prove a version of Hahn-Banach Theorem.
  6. Jolanta Kamienska, Jaroslaw Stanislaw Walijewski. Homomorphisms of Lattices, Finite Join and Finite Meet, Formalized Mathematics 4(1), pages 35-40, 1993. MML Identifier: LATTICE4
    Summary:
  7. Jolanta Kamienska. Representation Theorem for Heyting Lattices, Formalized Mathematics 4(1), pages 41-45, 1993. MML Identifier: OPENLATT
    Summary:
  8. Jaroslaw Stanislaw Walijewski. Representation Theorem for Boolean Algebras, Formalized Mathematics 4(1), pages 45-50, 1993. MML Identifier: LOPCLSET
    Summary:
  9. Andrzej Trybulec, Yatsuka Nakamura. Some Remarks on the Simple Concrete Model of Computer, Formalized Mathematics 4(1), pages 51-56, 1993. MML Identifier: AMI_3
    Summary: We prove some results on {\bf SCM} needed for the proof of the correctness of Euclid's algorithm. We introduce the following concepts: \begin{itemize} \item[-] starting finite partial state (Start-At$(l)$), then assigns to the instruction counter an instruction location (and consists only of this assignment), \item[-] programmed finite partial state, that consists of the instructions (to be more precise, a finite partial state with the domain consisting of instruction locations). \end{itemize} We define for a total state $s$ what it means that $s$ starts at $l$ (the value of the instruction counter in the state $s$ is $l$) and $s$ halts at $l$ (the halt instruction is assigned to $l$ in the state $s$). Similar notions are defined for finite partial states.
  10. Andrzej Trybulec, Yatsuka Nakamura. Euclid's Algorithm, Formalized Mathematics 4(1), pages 57-60, 1993. MML Identifier: AMI_4
    Summary: The main goal of the paper is to prove the correctness of the Euclid's algorithm for {\bf SCM}. We define the Euclid's algorithm and describe the natural semantics of it. Eventually we prove that the Euclid's algorithm computes the Euclid's function. Let us observe that the Euclid's function is defined as a function mapping finite partial states to finite partial states of {\bf SCM} rather than pairs of integers to integers.
  11. Grzegorz Bancerek, Piotr Rudnicki. Development of Terminology for \bf SCM, Formalized Mathematics 4(1), pages 61-67, 1993. MML Identifier: SCM_1
    Summary: We develop a higher level terminology for the {\bf SCM} machine defined by Nakamura and Trybulec in \cite{AMI_1.ABS}. Among numerous technical definitions and lemmas we define a complexity measure of a halting state of {\bf SCM} and a loader for {\bf SCM} for arbitrary finite sequence of instructions. In order to test the introduced terminology we discuss properties of eight shortest halting programs, one for each instruction.
  12. Grzegorz Bancerek, Piotr Rudnicki. Two Programs for \bf SCM. Part I -- Preliminaries, Formalized Mathematics 4(1), pages 69-72, 1993. MML Identifier: PRE_FF
    Summary: In two articles (this one and \cite{FIB_FUSC.ABS}) we discuss correctness of two short programs for the {\bf SCM} machine: one computes Fibonacci numbers and the other computes the {\em fusc} function of Dijkstra \cite{DIJKSTRA}. The limitations of current Mizar implementation rendered it impossible to present the correctness proofs for the programs in one article. This part is purely technical and contains a number of very specific lemmas about integer division, floor, exponentiation and logarithms. The formal definitions of the Fibonacci sequence and the {\em fusc} function may be of general interest.
  13. Grzegorz Bancerek, Piotr Rudnicki. Two Programs for \bf SCM. Part II -- Programs, Formalized Mathematics 4(1), pages 73-75, 1993. MML Identifier: FIB_FUSC
    Summary: We prove the correctness of two short programs for the {\bf SCM} machine: one computes Fibonacci numbers and the other computes the {\em fusc} function of Dijkstra \cite{DIJKSTRA}. The formal definitions of these functions can be found in \cite{PRE_FF.ABS}. We prove the total correctness of the programs in two ways: by conducting inductions on computations and inductions on input data. In addition we characterize the concrete complexity of the programs as defined in \cite{SCM_1.ABS}.
  14. Grzegorz Bancerek. Joining of Decorated Trees, Formalized Mathematics 4(1), pages 77-82, 1993. MML Identifier: TREES_4
    Summary: This is the continuation of the sequence of articles on trees (see \cite{TREES_1.ABS}, \cite{TREES_2.ABS}, \cite{TREES_3.ABS}). The main goal is to introduce joining operations on decorated trees corresponding with operations introduced in \cite{TREES_3.ABS}. We will also introduce the operation of substitution. In the last section we dealt with trees decorated by Cartesian product, i.e. we showed some lemmas on joining operations applied to such trees.
  15. Takaya Nishiyama, Yasuho Mizuhara. Binary Arithmetics, Formalized Mathematics 4(1), pages 83-86, 1993. MML Identifier: BINARITH
    Summary: Formalizes the basic concepts of binary arithmetic and its related operations. We present the definitions for the following logical operators: 'or' and 'xor' (exclusive or) and include in this article some theorems concerning these operators. We also introduce the concept of an $n$-bit register. Such registers are used in the definition of binary unsigned arithmetic presented in this article. Theorems on the relationships of such concepts to the operations of natural numbers are also given.
  16. Pauline N. Kawamoto, Yasushi Fuwa, Yatsuka Nakamura. Basic Concepts for Petri Nets with Boolean Markings, Formalized Mathematics 4(1), pages 87-90, 1993. MML Identifier: BOOLMARK
    Summary: Contains basic concepts for Petri nets with Boolean markings and the firability$\slash$firing of single transitions as well as sequences of transitions \cite{Nakamura:5}. The concept of a Boolean marking is introduced as a mapping of a Boolean TRUE$\slash$FALSE to each of the places in a place$\slash$transition net. This simplifies the conventional definitions of the firability and firing of a transition. One note of caution in this article - the definition of firing a transition does not require that the transition be firable. Therefore, it is advisable to check that transitions ARE firable before firing them.
  17. Grzegorz Bancerek, Piotr Rudnicki. On Defining Functions on Trees, Formalized Mathematics 4(1), pages 91-101, 1993. MML Identifier: DTCONSTR
    Summary: The continuation of the sequence of articles on trees (see \cite{TREES_1.ABS}, \cite{TREES_2.ABS}, \cite{TREES_3.ABS}, \cite{TREES_4.ABS}) and on context-free grammars (\cite{LANG1.ABS}). We define the set of complete parse trees for a given context-free grammar. Next we define the scheme of induction for the set and the scheme of defining functions by induction on the set. For each symbol of a context-free grammar we define the terminal, the pretraversal, and the posttraversal languages. The introduced terminology is tested on the example of Peano naturals.
  18. Beata Madras. Product of Family of Universal Algebras, Formalized Mathematics 4(1), pages 103-108, 1993. MML Identifier: PRALG_1
    Summary: The product of two algebras, trivial algebra determined by an empty set and product of a family of algebras are defined. Some basic properties are shown.
  19. Malgorzata Korolkiewicz. Homomorphisms of Algebras. Quotient Universal Algebra, Formalized Mathematics 4(1), pages 109-113, 1993. MML Identifier: ALG_1
    Summary: The first part introduces homomorphisms of universal algebras and their basic properties. The second is concerned with the construction of a quotient universal algebra. The first isomorphism theorem is proved.
  20. Beata Perkowska. Free Universal Algebra Construction, Formalized Mathematics 4(1), pages 115-120, 1993. MML Identifier: FREEALG
    Summary: A construction of the free universal algebra with fixed signature and a given set of generators.
  21. Agnieszka Banachowicz, Anna Winnicka. Complex Sequences, Formalized Mathematics 4(1), pages 121-124, 1993. MML Identifier: COMSEQ_1
    Summary: Definitions of complex sequence and operations on sequences (multiplication of sequences and multiplication by a complex number, addition, subtraction, division and absolute value of sequence) are given. We followed \cite{SEQ_1.ABS}.
  22. Zbigniew Karno. Maximal Discrete Subspaces of Almost Discrete Topological Spaces, Formalized Mathematics 4(1), pages 125-135, 1993. MML Identifier: TEX_2
    Summary: Let $X$ be a topological space and let $D$ be a subset of $X$. $D$ is said to be {\em discrete}\/ provided for every subset $A$ of $X$ such that $A \subseteq D$ there is an open subset $G$ of $X$ such that $A = D \cap G$\/ (comp. e.g., \cite{KURAT:2}). A discrete subset $M$ of $X$ is said to be {\em maximal discrete}\/ provided for every discrete subset $D$ of $X$ if $M \subseteq D$ then $M = D$. A subspace of $X$ is {\em discrete}\/ ({\em maximal discrete}) iff its carrier is discrete (maximal discrete) in $X$.\par Our purpose is to list a number of properties of discrete and maximal discrete sets in Mizar formalism. In particular, we show here that {\em if $D$ is dense and discrete then $D$ is maximal discrete}; moreover, {\em if $D$ is open and maximal discrete then $D$ is dense}. We discuss also the problem of the existence of maximal discrete subsets in a topological space.\par To present the main results we first recall a definition of a class of topological spaces considered herein. A topological space $X$ is called {\em almost discrete}\/ if every open subset of $X$ is closed; equivalently, if every closed subset of $X$ is open. Such spaces were investigated in Mizar formalism in \cite{TDLAT_3.ABS} and \cite{TEX_1.ABS}. We show here that {\em every almost discrete space contains a maximal discrete subspace and every such subspace is a retract of the enveloping space}. Moreover, {\em if $X_{0}$ is a maximal discrete subspace of an almost discrete space $X$ and $r : X \rightarrow X_{0}$ is a continuous retraction, then $r^{-1}(x) = \overline{\{x\}}$ for every point $x$ of $X$ belonging to $X_{0}$}. This fact is a specialization, in the case of almost discrete spaces, of the theorem of M.H. Stone that every topological space can be made into a $T_{0}$-space by suitable identification of points (see \cite{STONE:3}).
  23. Zbigniew Karno. On Nowhere and Everywhere Dense Subspaces of Topological Spaces, Formalized Mathematics 4(1), pages 137-146, 1993. MML Identifier: TEX_3
    Summary: Let $X$ be a topological space and let $X_{0}$ be a subspace of $X$ with the carrier $A$. $X_{0}$ is called {\em boundary}\/ ({\em dense}) in $X$ if $A$ is boundary (dense), i.e., ${\rm Int}\,A = \emptyset$ ($\overline{A} =$ the carrier of $X$); $X_{0}$ is called {\em nowhere dense}\/ ({\em everywhere dense}) in $X$ if $A$ is nowhere dense (everywhere dense), i.e., ${\rm Int}\,\overline{A} = \emptyset$ ($\overline{{\rm Int}\,A} =$ the carrier of $X$) (see \cite{TOPS_3.ABS} and comp. \cite{KURAT:2}).\par Our purpose is to list, using Mizar formalism, a number of properties of such subspaces, mostly in non-discrete (non-almost-discrete) spaces (comp. \cite{TOPS_3.ABS}). Recall that $X$ is called {\em discrete}\/ if every subset of $X$ is open (closed); $X$ is called {\em almost discrete}\/ if every open subset of $X$ is closed; equivalently, if every closed subset of $X$ is open (see \cite{TDLAT_3.ABS}, \cite{TEX_1.ABS} and comp. \cite{KURAT:2},\cite{KURAT:3}). We have the following characterization of non-discrete spaces: {\em $X$ is non-discrete iff there exists a boundary subspace in $X$}. Hence, {\em $X$ is non-discrete iff there exists a dense proper subspace in $X$}. We have the following analogous characterization of non-almost-discrete spaces: {\em $X$ is non-almost-discrete iff there exists a nowhere dense subspace in $X$}. Hence, {\em $X$ is non-almost-discrete iff there exists an everywhere dense proper subspace in $X$}.\par Note that some interdependencies between boundary, dense, nowhere and everywhere dense subspaces are also indicated. These have the form of observations in the text and they correspond to the existential and to the conditional clusters in the Mizar System. These clusters guarantee the existence and ensure the extension of types supported automatically by the Mizar System.