Abstract

In this paper we explore the possibility of emulating the Mizar environment as close as possible inside the Isabelle logical framework. We introduce adaptations to the Isabelle/FOL object logic that correspond to the logic of Mizar, as well as Isar inner syntax notations that correspond to these of the Mizar language. We show how Isabelle types can be used to differentiate between the syntactic categories of the Mizar language, such as sets and Mizar types including modes and attributes, and show how they interact with the basic constructs of the Tarski-Grothendieck set theory. We discuss Mizar definitions and provide simple abbreviations that allow the introduction of Mizar predicates, functions, attributes and modes using the Isabelle/Pure language elements for introducing definitions and theorems. We finally consider the definite and indefinite description operators in Mizar and their use to introduce definitions by ``means’‘ and ``equals’‘. We demonstrate the usability of the environment on a sample Mizar-style formalization, with cluster inferences and ``by’‘ steps performed manually.

BibTeX

@inproceedings{CKKPJU-CPP2016,
  author    = "Cezary Kaliszyk and Karol P{\k{a}}k and Josef Urban",
  title     = "Towards a {M}izar Environment for {I}sabelle: Foundations and Language",
  booktitle = "Proceedings of the 5th {ACM} {SIGPLAN} Conference on Certified Programs
               and Proofs (CPP 2016)",
  pages     = "58--65",
  year      = 2016,
  doi       = "10.1145/2854065.2854070"
}