Theory Simple_Game

subsection ‹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›
begin

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

―‹Plays (to be precise: play prefixes) 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›
type_synonym ('s2) posstrategy = ‹'s2 ⇒ 's2›

definition strategy_from_positional :: ‹'s posstrategy ⇒ 's strategy› where
  ‹strategy_from_positional pf = (λ play. pf (hd play))›

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

definition play_continuation :: ‹'s play ⇒ 's play ⇒ bool›
  where ‹play_continuation p1 p2 ≡ (drop (length p2 - length p1) p2) = p1›

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

lemma strategy0_step:
  assumes
    ‹n0 # n1 # rest ∈ plays_for_0strategy f initial›
    ‹player0_position n1›
  shows
    ‹f (n1 # rest) = n0›
  using assms
  by (induct rule: plays_for_0strategy.cases, auto)

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

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_0strategy :: ‹'s strategy ⇒ 's ⇒ bool› where
  ‹sound_0strategy f initial ≡
    ∀ n0 play .
      n0#play ∈ plays_for_0strategy f initial ∧
      player0_position n0 ⟶ n0 ⟼♡ f (n0#play)›

definition sound_1strategy :: ‹'s strategy ⇒ 's ⇒ bool› where
  ‹sound_1strategy f initial ≡
    ∀ n1 play .
      n1#play ∈ plays_for_1strategy f initial ∧
      player1_position n1 ⟶ n1 ⟼♡ f (n1#play)›

lemma strategy0_plays_subset:
  assumes ‹play ∈ plays_for_0strategy f initial›
  shows ‹play ∈ plays initial›
  using assms by (induct rule: plays_for_0strategy.induct, auto simp add: plays.intros)
lemma strategy1_plays_subset:
  assumes ‹play ∈ plays_for_1strategy f initial›
  shows ‹play ∈ plays initial›
  using assms by (induct rule: plays_for_1strategy.induct, auto simp add: plays.intros)

lemma no_empty_plays:
  assumes ‹[] ∈ plays initial›
  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_immediately :: ‹'s play ⇒ bool› where
  ‹player1_wins_immediately play ≡ player0_position (hd play) ∧ (∄ p' . (hd play) ⟼♡ p')›

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

definition player0_wins :: ‹'s ⇒ bool› where
  ‹player0_wins s ≡ (∃ f . player0_winning_strategy f s ∧ sound_0strategy f s)›

lemma stuck_player0_win:
  assumes ‹player1_position initial› ‹(∄ p' . initial ⟼♡ p')›
  shows ‹player0_wins initial›
proof -
  have ‹⋀pl. pl ∈ plays initial ⟹ pl = [initial]›
  proof -
    fix pl
    assume ‹pl ∈ plays initial›
    thus ‹pl = [initial]› using assms(2) by (induct, auto)
  qed
  thus ?thesis using assms(1)
    by (metis list.sel(1) player0_winning_strategy_def player0_wins_def player1_wins_immediately_def
        sound_0strategy_def strategy0_plays_subset)
qed

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

end
end