Theory Simple_Game

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