Partizan Games in Isabelle/HOLZf

摘要

Partizan Games (PGs) were invented by John H. Conway and are described in his book On Numbers and Games. We formalize PGs in Higher Order Logic extended with ZF axioms (HOLZP) using Isabelle, a mechanical proof assistant. We show that PGs can be defined as the unique fixpoint of a function that arises naturally from Conway's original definition. While the construction of PGs in HOLZF relies heavily on the ZF axioms, operations on PGs are defined on a game type that hides its set theoretic origins. A polymorphic type of sets that are not bigger than ZF sets facilitates this. We formalize the induction principle that Conway uses throughout his proofs about games, and prove its correctness. For these purposes we examine how the notions of well-foundedness in HOL and ZF are related in HOLZF. Finally, games (modulo equality) are added to Isabelle's numeric types by showing that they are an instance of the axiomatic type class of partially ordered abelian groups.