# Theory Simple_Game

theory Simple_Game
imports Main
```section ‹Simple Games›

theory Simple_Game
imports
Main
begin

text ‹Simple games are games where player0 wins all infinite plays.›
locale simple_game =
fixes
game_move :: ‹'s ⇒ 's ⇒ bool› ("_ ⟼♡ _" [70, 70] 80) and
player0_position :: ‹'s ⇒ bool› and
initial :: 's
begin

definition player1_position :: ‹'s ⇒ bool›
where ‹player1_position s ≡ ¬ player0_position s›

―‹plays (to be precise: play p refixes) are lists. we model them
with the most recent move at the beginning. (for our purpose it's enough to consider finite plays)›
type_synonym ('s2) play = ‹'s2 list›
type_synonym ('s2) strategy = ‹'s2 play ⇒ 's2›

inductive_set plays :: ‹'s play set› where
‹[initial] ∈ plays› |
‹p#play ∈ plays ⟹ p ⟼♡ p' ⟹ p'#p#play ∈ plays›

―‹plays for a given player 0 strategy›
inductive_set plays_for_strategy :: ‹'s strategy ⇒ 's play set› for f where
init: ‹[initial] ∈ plays_for_strategy f› |
p0move: ‹n0#play ∈ plays_for_strategy f ⟹ player0_position n0 ⟹ n0 ⟼♡ f (n0#play)
⟹ (f (n0#play))#n0#play ∈ plays_for_strategy f› |
p1move: ‹n1#play ∈ plays_for_strategy f ⟹ player1_position n1 ⟹ n1 ⟼♡ n1'
⟹ n1'#n1#play ∈ plays_for_strategy f›

lemma strategy_step:
assumes
‹n0 # n1 # rest ∈ plays_for_strategy f›
‹player0_position n1›
shows
‹f (n1 # rest) = n0›
using assms
by (induct rule: plays_for_strategy.cases, auto simp add: simple_game.player1_position_def)

definition positional_strategy :: ‹'s strategy ⇒ bool› where
‹positional_strategy f ≡ ∀r1 r2 n. f (n # r1) = f (n # r2)›

text ‹a strategy is sound if it only decides on enabled transitions.›
definition sound_strategy :: ‹'s strategy ⇒ bool› where
‹sound_strategy f ≡
∀ n0 play . n0#play ∈ plays_for_strategy f ∧ player0_position n0 ⟶ n0 ⟼♡ f (n0#play)›

lemma strategy_plays_subset:
assumes ‹play ∈ plays_for_strategy f›
shows ‹play ∈ plays›
using assms by (induct rule: plays_for_strategy.induct, auto simp add: plays.intros)

lemma no_empty_plays:
assumes ‹[] ∈ plays›
shows ‹False›
using assms plays.cases by blast

text ‹player1 wins a play if the play has reached a deadlock where it's player0's turn›

definition player1_wins :: ‹'s play ⇒ bool› where
‹player1_wins play ≡ player0_position (hd play) ∧ (∄ p' . (hd play) ⟼♡ p')›

definition player0_winning_strategy :: ‹'s strategy ⇒ bool› where
‹player0_winning_strategy f ≡ (∀ play ∈ plays_for_strategy f . ¬ player1_wins play)›

end

end
```