From: Andreas Lochbihler <firstname.lastname@example.org>
I'm happy to announce two new AFP entries.
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.
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 [https://arxiv.org/pdf/2104.12224.pdf].
Last updated: Sep 25 2021 at 08:21 UTC