Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Two new AFP entries: Gale-Stewart games and Is...

view this post on Zulip Email Gateway (Apr 28 2021 at 08:36):

From: Andreas Lochbihler <>
I'm happy to announce two new AFP entries.

  1. Gale-Stewart Games
    by Sebastiaan Joosten

This is a formalisation of the main result of Gale and Stewart from 1953, showing that
closed finite games are determined. This property is now known as the Gale Stewart
Theorem. While the original paper shows some additional theorems as well, we only
formalize this main result, but do so in a somewhat general way. We formalize games of a
fixed arbitrary length, including infinite length, using co-inductive lists, and show that
defensive strategies exist unless the other player is winning. For closed games, defensive
strategies are winning for the closed player, proving that such games are determined. For
finite games, which are a special case in our formalisation, all games are closed.

  1. Isabelle's Metalogic: Formalization and Proof Checker
    by Tobias Nipkow and Simon Roßkopf

In this entry we formalize Isabelle's metalogic in Isabelle/HOL. Furthermore, we define a
language of proof terms and an executable proof checker and prove its soundness wrt. the
metalogic. The formalization is intentionally kept close to the Isabelle
implementation(for example using de Brujin indices) to enable easy integration of
generated code with the Isabelle system without a complicated translation layer. The
formalization is described in our CADE 28 paper [].


Last updated: Jul 15 2022 at 23:21 UTC