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›
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›
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