This GitLab instance reached the end of its service life. It won't be possible to create new users or projects.

Please read the deprecation notice for more information concerning the deprecation timeline

Visit migration.git.tu-berlin.de (internal network only) to import your old projects to the new GitLab platform 📥

Simple_Game.thy 3.35 KB
Newer Older
1 2 3 4 5 6 7 8 9 10
section \<open>Simple Games\<close>

theory Simple_Game
imports
  Main
begin

text \<open>Simple games are games where player0 wins all infinite plays.\<close>
locale simple_game =
fixes
benkeks committed
11 12
  game_move :: \<open>'s \<Rightarrow> 's \<Rightarrow> bool\<close> ("_ \<longmapsto>\<heartsuit> _" [70, 70] 80) and
  player0_position :: \<open>'s \<Rightarrow> bool\<close> and
13 14 15
  initial :: 's
begin

benkeks committed
16 17
definition player1_position :: \<open>'s \<Rightarrow> bool\<close>
  where \<open>player1_position s \<equiv> \<not> player0_position s\<close>
18

benkeks committed
19
\<comment>\<open>plays (to be precise: play p refixes) are lists. we model them 
20
  with the most recent move at the beginning. (for our purpose it's enough to consider finite plays)\<close>
benkeks committed
21 22
type_synonym ('s2) play = \<open>'s2 list\<close>
type_synonym ('s2) strategy = \<open>'s2 play \<Rightarrow> 's2\<close>
23

benkeks committed
24 25 26
inductive_set plays :: \<open>'s play set\<close> where
  \<open>[initial] \<in> plays\<close> |
  \<open>p#play \<in> plays \<Longrightarrow> p \<longmapsto>\<heartsuit> p' \<Longrightarrow> p'#p#play \<in> plays\<close>
27

benkeks committed
28
\<comment>\<open>plays for a given player 0 strategy\<close>
benkeks committed
29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46
inductive_set plays_for_strategy :: \<open>'s strategy \<Rightarrow> 's play set\<close> for f where
  init: \<open>[initial] \<in> plays_for_strategy f\<close> |
  p0move: \<open>n0#play \<in> plays_for_strategy f \<Longrightarrow> player0_position n0 \<Longrightarrow> n0 \<longmapsto>\<heartsuit> f (n0#play)
    \<Longrightarrow> (f (n0#play))#n0#play \<in> plays_for_strategy f\<close> |
  p1move: \<open>n1#play \<in> plays_for_strategy f \<Longrightarrow> player1_position n1 \<Longrightarrow> n1 \<longmapsto>\<heartsuit> n1'
    \<Longrightarrow> n1'#n1#play \<in> plays_for_strategy f\<close>

lemma strategy_step:
  assumes
    \<open>n0 # n1 # rest \<in> plays_for_strategy f\<close>
    \<open>player0_position n1\<close>
  shows
    \<open>f (n1 # rest) = n0\<close>
  using assms
  by (induct rule: plays_for_strategy.cases, auto simp add: simple_game.player1_position_def)

definition positional_strategy :: \<open>'s strategy \<Rightarrow> bool\<close> where
  \<open>positional_strategy f \<equiv> \<forall>r1 r2 n. f (n # r1) = f (n # r2)\<close>
47 48

text \<open>a strategy is sound if it only decides on enabled transitions.\<close>
benkeks committed
49 50 51
definition sound_strategy :: \<open>'s strategy \<Rightarrow> bool\<close> where
  \<open>sound_strategy f \<equiv>
    \<forall> n0 play . n0#play \<in> plays_for_strategy f \<and> player0_position n0 \<longrightarrow> n0 \<longmapsto>\<heartsuit> f (n0#play)\<close>
52 53

lemma strategy_plays_subset:
benkeks committed
54 55
  assumes \<open>play \<in> plays_for_strategy f\<close>
  shows \<open>play \<in> plays\<close>
56 57 58
  using assms by (induct rule: plays_for_strategy.induct, auto simp add: plays.intros)

lemma no_empty_plays:
benkeks committed
59 60
  assumes \<open>[] \<in> plays\<close>
  shows \<open>False\<close> 
61 62
  using assms plays.cases by blast

benkeks committed
63
text \<open>player1 wins a play if the play has reached a deadlock where it's player0's turn\<close>
64

benkeks committed
65 66
definition player1_wins :: \<open>'s play \<Rightarrow> bool\<close> where
  \<open>player1_wins play \<equiv> player0_position (hd play) \<and> (\<nexists> p' . (hd play) \<longmapsto>\<heartsuit> p')\<close>
67

benkeks committed
68 69
definition player0_winning_strategy :: \<open>'s strategy \<Rightarrow> bool\<close> where
  \<open>player0_winning_strategy f \<equiv> (\<forall> play \<in> plays_for_strategy f . \<not> player1_wins play)\<close>
70 71 72 73

end

end