Theory Equivalence_Games
section ‹Reachability Games›
theory Equivalence_Games
imports Strong_Equivalences
begin
text ‹
A game is an unlabeled graph where vertices are partitioned into
defender and attacker positions.
›
locale game =
fixes
game_move :: ‹'g ⇒ 'g ⇒ bool› (infix ‹↣› 80) and
defender_position :: ‹'g ⇒ bool›
begin
abbreviation ‹attacker_position g ≡ ¬defender_position g›
abbreviation ‹options g ≡ {g'. g ↣ g'}›
text ‹Each player loses at a position if it were their turn but they are stuck.›
definition ‹defender_loses g ≡ defender_position g ∧ options g = {}›
definition ‹attacker_loses g ≡ attacker_position g ∧ options g = {}›
text ‹
A (positional) strategy is a function to select among the options at a
position. That only possible moves are valid choices cannot be expressed in
a HOL type. We express this by soundness predicates for attacker/defender
strategies.
›
type_synonym ('g0) strategy = ‹'g0 ⇒ 'g0›
definition ‹sound_defender_strategy strat g ≡
defender_position g ∧ options g ≠ {} ⟶ strat g ∈ options g›
definition ‹sound_attacker_strategy strat g ≡
attacker_position g ∧ options g ≠ {} ⟶ strat g ∈ options g›
text ‹
A play (fragment) is a sequence of game positions that follow a path of game
moves.
›
inductive play :: ‹'g list ⇒ bool› where
init: ‹play [g]› |
step: ‹play (g # (g' # gg))› if ‹g ↣ g'› ‹play (g' # gg)›
text ‹We have defined plays in a way where there are no empty plays.›
lemma no_empty_play:
assumes ‹play []›
shows ‹False›
using assms play.cases by blast
text ‹
A play follows a defender strategy if every every defender-controlled move
obeys the strategy. (The type here, does not really ensure the position
sequences to be plays and the strategies to be sound. This information
should come from the context.)›
fun play_follows_defender_strategy :: ‹'g list ⇒ ('g ⇒ 'g) ⇒ bool›
where
‹play_follows_defender_strategy (g0 # g1 # pl) strat =
((if defender_position g0 then strat g0 = g1 else True)
∧ play_follows_defender_strategy (g1 # pl) strat)› |
‹play_follows_defender_strategy _ _ = True›
lemma play_extension:
assumes
‹last pl ↣ g'›
‹play pl›
shows
‹play (pl @ [g'])›
using assms no_empty_play
by (induct pl, auto,
smt (verit, del_insts) append_Cons append_self_conv2
list.sel(3) play.simps)
lemma play_follows_defender_strategy_extension_atk:
assumes
‹play_follows_defender_strategy pl strat›
‹last pl ↣ g'›
‹attacker_position (last pl)›
shows
‹play_follows_defender_strategy (pl @ [g']) strat›
using assms
by (induct pl, auto, smt (z3) append_self_conv2 hd_append list.distinct(1)
list.sel(1,3) play_follows_defender_strategy.elims(1))
lemma play_follows_defender_strategy_extension_dfn:
assumes
‹play_follows_defender_strategy pl strat›
‹defender_position (last pl)›
shows
‹play_follows_defender_strategy (pl @ [strat (last pl)]) strat›
using assms
by (induct pl, force, smt (z3) append_Cons append_Nil
game.play_follows_defender_strategy.simps(3) last.simps
list.inject play_follows_defender_strategy.elims(1))
fun play_follows_attacker_strategy :: ‹'g list ⇒ ('g ⇒ 'g) ⇒ bool›
where
‹play_follows_attacker_strategy (g0 # g1 # pl) strat =
((if attacker_position g0 then strat g0 = g1 else True)
∧ play_follows_attacker_strategy (g1 # pl) strat)›
| ‹play_follows_attacker_strategy _ _ = True›
text ‹
A defender strategy is winning from a position if all plays following the
strategy from there only lead to positions where the defender has moves
and the strategy is sound. (In particular, the defender also wins if the
game goes on forever.)
›
definition defender_winning_strategy :: ‹'g strategy ⇒ 'g ⇒ bool›
where ‹defender_winning_strategy def_strat g ≡
(∀pl. play pl ∧ hd pl = g ∧ play_follows_defender_strategy pl def_strat
⟶ sound_defender_strategy def_strat (last pl) ∧ ¬defender_loses (last pl))›
end
section ‹The Bisimulation Game›