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 📥

CS_Game.thy 17.3 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16
section \<open>Game for Coupled Similarity\<close>

theory CS_Game
imports
  Coupled_Simulation
  Simple_Game
begin

subsection \<open>The Coupled Simulation Preorder Game\<close>

datatype ('s, 'a) cs_game_node =
  AttackerNode 's 's |
  DefenderStepNode 'a 's 's |
  DefenderCouplingNode 's 's

fun (in lts_tau) cs_game_moves ::
benkeks committed
17
  \<open>('s, 'a) cs_game_node \<Rightarrow> ('s, 'a) cs_game_node \<Rightarrow> bool\<close> where
18
  simulation_challenge:
benkeks committed
19 20
    \<open>cs_game_moves (AttackerNode p q) (DefenderStepNode a p1 q0) =
      (p \<longmapsto>a p1 \<and> q = q0)\<close> |
21
  simulation_answer: 
benkeks committed
22 23
    \<open>cs_game_moves (DefenderStepNode a p1 q0) (AttackerNode p11 q1) =
      (q0 \<Rightarrow>^a q1 \<and> p1 = p11)\<close> |
24
  coupling_challenge:
benkeks committed
25 26
    \<open>cs_game_moves (AttackerNode p q) (DefenderCouplingNode p0 q0) =
      (p = p0 \<and> q = q0)\<close> |
27
  coupling_answer:
benkeks committed
28 29
    \<open>cs_game_moves (DefenderCouplingNode p0 q0) (AttackerNode q1 p00) =
      (p0 = p00 \<and> q0 \<longmapsto>* tau q1)\<close> |
30
  cs_game_moves_no_step:
benkeks committed
31
    \<open>cs_game_moves _ _ = False\<close>
32

benkeks committed
33 34 35 36
fun cs_game_defender_node :: \<open>('s, 'a) cs_game_node \<Rightarrow> bool\<close> where
  \<open>cs_game_defender_node (AttackerNode _ _) = False\<close> |
  \<open>cs_game_defender_node (DefenderStepNode _ _ _) = True\<close> |
  \<open>cs_game_defender_node (DefenderCouplingNode _ _) = True\<close>
37 38 39 40 41

locale cs_game =
  lts_tau trans \<tau> +
  simple_game cs_game_moves cs_game_defender_node initial
for
benkeks committed
42 43 44
  trans :: \<open>'s \<Rightarrow> 'a \<Rightarrow> 's \<Rightarrow> bool\<close> and
  \<tau> :: \<open>'a\<close> and 
  initial :: \<open>('s, 'a) cs_game_node\<close>
45 46 47 48
begin

subsection \<open>Coupled Simulation Implies Winning Strategy\<close>

benkeks committed
49 50 51 52 53 54
fun strategy_from_coupledsim :: \<open>('s \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> ('s, 'a) cs_game_node strategy\<close> where
  \<open>strategy_from_coupledsim R ((DefenderStepNode a p1 q0)#play) =
    (AttackerNode p1 (SOME q1 . R p1 q1 \<and> q0 \<Rightarrow>^a q1))\<close> |
  \<open>strategy_from_coupledsim R ((DefenderCouplingNode p0 q0)#play) =
    (AttackerNode (SOME q1 . R q1 p0 \<and> q0 \<longmapsto>* tau q1) p0)\<close> |
  \<open>strategy_from_coupledsim _ _ = undefined\<close>
55

benkeks committed
56
lemma defender_preceded_by_attacker:
57
  assumes
benkeks committed
58 59 60 61
    \<open>n0 # play \<in> plays\<close>
    \<open>cs_game_defender_node n0\<close>
    \<open>initial = AttackerNode p0 q0\<close>
  shows \<open>\<exists> p q . hd play = AttackerNode p q \<and> cs_game_moves (AttackerNode p q) n0\<close> \<open>play \<noteq> []\<close>
62
proof -
benkeks committed
63 64
  have n0_not_init: \<open>n0 \<noteq> initial\<close> using assms(2,3) by auto
  hence \<open>cs_game_moves (hd play) n0\<close> using assms(1)
65
    by (metis list.sel(1) list.sel(3) plays.cases)
benkeks committed
66
  thus \<open>\<exists>p q. hd play = AttackerNode p q \<and> cs_game_moves (AttackerNode p q) n0\<close> using assms(2)
67
    by (metis cs_game_defender_node.elims(2,3) local.cs_game_moves_no_step(1,2,3,7))
benkeks committed
68
  show \<open>play \<noteq> []\<close> using n0_not_init assms(1) plays.cases by auto
69 70 71 72
qed

lemma strategy_from_coupledsim_retains_coupledsim:
  assumes
benkeks committed
73 74 75 76
    \<open>R p0 q0\<close>
    \<open>coupled_simulation R\<close>
    \<open>initial = AttackerNode p0 q0\<close>
    \<open>play \<in> plays_for_strategy (strategy_from_coupledsim R)\<close>
77
  shows
benkeks committed
78 79
    \<open>hd play = AttackerNode p q \<Longrightarrow> R p q\<close>
    \<open>length play > 1 \<Longrightarrow> hd (tl play) = AttackerNode p q \<Longrightarrow> R p q\<close>
80 81 82 83
  using assms(4)
proof (induct arbitrary: p q rule: plays_for_strategy.induct[OF assms(4)])
  case 1
  fix p q
benkeks committed
84 85 86
  assume \<open>hd [initial] = AttackerNode p q\<close>
  hence \<open>p = p0\<close> \<open>q = q0\<close> using assms(3) by auto
  thus \<open>R p q\<close> using assms(1) by simp
87 88 89
next
  case 1
  fix p q
benkeks committed
90
  assume \<open>1 < length [initial]\<close>
91
  hence False by auto
benkeks committed
92
  thus \<open>R p q\<close>  ..
93 94
next
  case (2 n0 play)
benkeks committed
95
  hence n0play_is_play: \<open>n0 # play \<in> plays\<close> using strategy_plays_subset by blast
96 97
  fix p q
  assume subassms:
benkeks committed
98 99 100
    \<open>hd (strategy_from_coupledsim R (n0 # play) # n0 # play) = AttackerNode p q\<close>
    \<open>strategy_from_coupledsim R (n0 # play) # n0 # play
      \<in> plays_for_strategy (strategy_from_coupledsim R)\<close>
101
  then obtain pi qi where 
benkeks committed
102 103 104
      piqi_def: \<open>hd (play) = AttackerNode pi qi\<close>
        \<open>cs_game_moves (AttackerNode pi qi) n0\<close> \<open>play \<noteq> []\<close>
    using defender_preceded_by_attacker[OF n0play_is_play `cs_game_defender_node n0` assms(3)]
105
    by blast
benkeks committed
106 107 108
  hence \<open>R pi qi\<close> using 2(1,3) by simp
  have \<open>(\<exists> a . n0 = (DefenderStepNode a p qi) \<and> pi \<longmapsto>a p)
    \<or> (n0 = (DefenderCouplingNode pi qi))\<close>
109 110 111
    using piqi_def(2) 2(4,5) subassms(1)
    by (metis cs_game_defender_node.elims(2) cs_game_moves.simps(2) list.sel(1)
        coupling_challenge simulation_challenge)
benkeks committed
112
  thus \<open>R p q\<close>
113 114
  proof safe
    fix a
benkeks committed
115 116 117
    assume n0_def: \<open>n0 = DefenderStepNode a p qi\<close> \<open>pi \<longmapsto>a p\<close>
    have \<open>strategy_from_coupledsim R (n0 # play) =
        (AttackerNode p (SOME q1 . R p q1 \<and> qi \<Rightarrow>^a q1))\<close>
118
      unfolding n0_def(1) by auto
benkeks committed
119 120
    with subassms(1) have q_def: \<open>q = (SOME q1. R p q1 \<and> qi \<Rightarrow>^a  q1)\<close> by auto
    have \<open>\<exists> qii . R p qii \<and> qi \<Rightarrow>^a qii\<close>
121 122
      using n0_def(2) `R pi qi` `coupled_simulation R`
      unfolding coupled_simulation_def by blast
benkeks committed
123
    from someI_ex[OF this] show \<open>R p q\<close> unfolding q_def by blast
124
  next
benkeks committed
125 126 127
    assume n0_def: \<open>n0 = DefenderCouplingNode pi qi\<close>
    have \<open>strategy_from_coupledsim R (n0 # play) =
        (AttackerNode (SOME q1 . R q1 pi \<and> qi \<longmapsto>* tau q1) pi)\<close>
128
      unfolding n0_def(1) by auto
benkeks committed
129 130
    with subassms(1) have qp_def: \<open>p = (SOME q1 . R q1 pi \<and> qi \<longmapsto>* tau q1)\<close> \<open>q = pi\<close> by auto
    have \<open>\<exists> q1 . R q1 pi \<and> qi \<longmapsto>* tau q1\<close>
131 132
      using n0_def `R pi qi` `coupled_simulation R`
      unfolding coupled_simulation_def by blast
benkeks committed
133
    from someI_ex[OF this] show \<open>R p q\<close> unfolding qp_def by blast
134 135 136 137
  qed
next
  case (2 n0 play)
  fix p q
benkeks committed
138
  assume \<open>hd (tl (strategy_from_coupledsim R (n0 # play) # n0 # play)) = AttackerNode p q\<close>
139
  hence False using 2(4) by auto
benkeks committed
140
  thus \<open>R p q\<close> ..
141 142 143
next
  case (3 n1 play n1')
  fix p q
benkeks committed
144
  assume \<open>hd (n1' # n1 # play) = AttackerNode p q\<close>
145 146
  hence False using 3(4,5) unfolding player1_position_def
    by (metis cs_game_moves_no_step(5) cs_game_defender_node.elims(3) list.sel(1))
benkeks committed
147
  thus \<open>R p q\<close> ..
148 149 150
next
  case (3 n1 play n1')
  fix p q
benkeks committed
151 152
  assume \<open>hd (tl (n1' # n1 # play)) = AttackerNode p q\<close>
  thus \<open>R p q\<close> using 3(1,2) by auto
153 154 155 156
qed

lemma strategy_from_coupledsim_sound:
  assumes
benkeks committed
157 158 159
    \<open>R p0 q0\<close>
    \<open>coupled_simulation R\<close>
    \<open>initial = AttackerNode p0 q0\<close>
160
  shows
benkeks committed
161
    \<open>sound_strategy (strategy_from_coupledsim R)\<close>
162 163 164 165
  unfolding sound_strategy_def
proof clarify
  fix n0 play
  assume subassms:
benkeks committed
166 167
    \<open>n0 # play \<in> plays_for_strategy(strategy_from_coupledsim R)\<close>
    \<open>cs_game_defender_node n0\<close>
168
  then obtain pi qi where 
benkeks committed
169 170 171
      piqi_def: \<open>hd (play) = AttackerNode pi qi\<close>
        \<open>cs_game_moves (AttackerNode pi qi) n0\<close> \<open>play \<noteq> []\<close>
    using defender_preceded_by_attacker[OF _ `cs_game_defender_node n0` assms(3)]
172
      strategy_plays_subset by blast
benkeks committed
173
  hence \<open>R pi qi\<close>
174
    using strategy_from_coupledsim_retains_coupledsim[OF assms] list.sel subassms by auto
benkeks committed
175 176
  have \<open>(\<exists> a p . n0 = (DefenderStepNode a p qi) \<and> pi \<longmapsto>a p)
    \<or> (n0 = (DefenderCouplingNode pi qi))\<close>
177 178
    by (metis cs_game_defender_node.elims(2)
        coupling_challenge simulation_challenge piqi_def(2) subassms(2))
benkeks committed
179
  thus \<open>cs_game_moves n0 (strategy_from_coupledsim R (n0 # play))\<close>
180 181 182
  proof safe
    fix a p
    assume dsn:
benkeks committed
183 184
      \<open>pi \<longmapsto>a  p\<close>
      \<open>n0 = DefenderStepNode a p qi\<close>
185
    hence qi_spec:
benkeks committed
186 187
      \<open>(strategy_from_coupledsim R (n0 # play)) =
        AttackerNode p (SOME q1 . R p q1 \<and> qi \<Rightarrow>^a q1)\<close>
188 189
      by simp
    then obtain qii where qii_spec:
benkeks committed
190 191
      \<open>AttackerNode p (SOME q1 . R p q1 \<and> qi \<Rightarrow>^a q1) = AttackerNode p qii\<close> by blast
    have \<open>\<exists> qii . R p qii \<and> qi \<Rightarrow>^a qii\<close>
192 193
      using dsn `R pi qi` `coupled_simulation R`
      unfolding coupled_simulation_def by blast
benkeks committed
194 195 196
    from someI_ex[OF this] have \<open>R p qii \<and> qi \<Rightarrow>^a qii\<close> using qii_spec by blast
    thus \<open>cs_game_moves (DefenderStepNode a p qi)
          (strategy_from_coupledsim R (DefenderStepNode a p qi # play))\<close>
197
      using qi_spec qii_spec unfolding dsn(2) by auto
benkeks committed
198
  next \<comment>\<open>coupling quite analogous.\<close>
199
    assume dcn:
benkeks committed
200
      \<open>n0 = DefenderCouplingNode pi qi\<close>
201
    hence qi_spec:
benkeks committed
202 203
      \<open>(strategy_from_coupledsim R (n0 # play)) =
      AttackerNode (SOME q1 . R q1 pi \<and> qi \<longmapsto>* tau q1) pi\<close>
204 205
      by simp
    then obtain qii where qii_spec:
benkeks committed
206 207
      \<open>AttackerNode (SOME q1 . R q1 pi \<and> qi \<longmapsto>* tau q1) pi = AttackerNode qii pi\<close> by blast
    have \<open>\<exists> qii . R qii pi \<and> qi \<longmapsto>* tau qii\<close>
208 209
      using dcn `R pi qi` `coupled_simulation R`
      unfolding coupled_simulation_def by blast
benkeks committed
210 211 212
    from someI_ex[OF this] have \<open>R qii pi \<and> qi \<longmapsto>* tau qii\<close> using qii_spec by blast
    thus \<open>cs_game_moves (DefenderCouplingNode pi qi)
        (strategy_from_coupledsim R (DefenderCouplingNode pi qi # play))\<close>
213 214 215 216 217 218
      using qi_spec qii_spec unfolding dcn by auto
  qed
qed

lemma coupledsim_implies_winning_strategy:
  assumes
benkeks committed
219 220 221
    \<open>R p q\<close>
    \<open>coupled_simulation R\<close>
    \<open>initial = AttackerNode p q\<close>
222
  shows
benkeks committed
223
    \<open>player0_winning_strategy (strategy_from_coupledsim R)\<close>
224 225 226 227
  unfolding player0_winning_strategy_def
proof (clarify)
  fix play
  assume subassms:
benkeks committed
228 229 230
    \<open>play \<in> plays_for_strategy (strategy_from_coupledsim R)\<close>
    \<open>player1_wins play\<close>
  show \<open>False\<close> using subassms
231 232 233 234 235
  proof (induct rule: simple_game.plays_for_strategy.induct[OF subassms(1)])
    case 1
    then show ?case unfolding player1_wins_def using assms(3) by auto
  next
    case (2 n0 play)
benkeks committed
236
    hence \<open>\<not> cs_game_defender_node (strategy_from_coupledsim R (n0 # play))\<close>
237
      using cs_game_moves_no_step cs_game_defender_node.elims(2) by metis
benkeks committed
238
    hence \<open>\<not>  player1_wins (strategy_from_coupledsim R (n0 # play) # n0 # play)\<close>
239 240 241 242
      unfolding player1_wins_def by auto
    thus ?case using 2(6) by auto
  next
    case (3 n1 play n1')
benkeks committed
243
    then obtain p q where n1_def: \<open>n1 = AttackerNode p q\<close>
244
      unfolding player1_position_def using cs_game_defender_node.elims(3) by blast
benkeks committed
245 246 247 248
    hence \<open>R p q\<close>
      using strategy_from_coupledsim_retains_coupledsim[OF assms, of \<open>n1 # play\<close>] 3(1) by auto
    have \<open>(\<exists> p1 a . n1' = (DefenderStepNode a p1 q) \<and> (p \<longmapsto>a p1))
        \<or> n1' = (DefenderCouplingNode p q)\<close>
249 250 251 252 253
      using n1_def `cs_game_moves n1 n1'` coupling_challenge cs_game_moves_no_step(5)
        simulation_challenge
      by (metis cs_game_defender_node.elims(2, 3))
    then show ?case
    proof 
benkeks committed
254
      assume \<open>(\<exists> p1 a . n1' = (DefenderStepNode a p1 q) \<and> (p \<longmapsto>a p1))\<close>
255
      then obtain p1 a where 
benkeks committed
256
        n1'_def: \<open>n1' = (DefenderStepNode a p1 q)\<close> \<open>p \<longmapsto>a p1\<close>
257
        by blast
benkeks committed
258
      hence \<open>\<exists> q1 . q \<Rightarrow>^a q1\<close> 
259
        using `R p q` `coupled_simulation R` unfolding coupled_simulation_def by blast
benkeks committed
260
      hence \<open>\<exists> q1 . cs_game_moves (DefenderStepNode a p1 q) (AttackerNode p1 q1)\<close>
261 262 263 264
        by auto
      with `player1_wins (n1' # n1 # play)` show False unfolding player1_wins_def n1'_def
        by (metis list.sel(1))
    next
benkeks committed
265 266
      assume n1'_def: \<open>n1' = DefenderCouplingNode p q\<close>
      have \<open>\<exists> q1 . q \<longmapsto>*tau q1\<close> 
267
        using `coupled_simulation R` `R p q` unfolding coupled_simulation_def by blast
benkeks committed
268
      hence \<open>\<exists> q1 . cs_game_moves (DefenderCouplingNode p q) (AttackerNode q1 p)\<close>
269 270 271 272 273 274 275 276 277 278 279
        by auto
      with `player1_wins (n1' # n1 # play)` show False unfolding player1_wins_def n1'_def
        by (metis list.sel(1))
    qed
  qed
qed

subsection \<open>Winning Strategy Induces Coupled Simulation\<close>

lemma winning_strategy_implies_coupledsim:
  assumes
benkeks committed
280 281
    \<open>player0_winning_strategy f\<close>
    \<open>sound_strategy f\<close>
282
  defines
benkeks committed
283
    \<open>R == \<lambda> p q . (\<exists> play \<in> plays_for_strategy f . hd play = AttackerNode p q)\<close>
284
  shows
benkeks committed
285
    \<open>coupled_simulation R\<close>
286 287 288 289
  unfolding coupled_simulation_def
proof safe
  fix p q p' a
  assume challenge:
benkeks committed
290 291 292 293
    \<open>R p q\<close>
    \<open>p \<longmapsto>a  p'\<close>
  hence game_move: \<open>cs_game_moves (AttackerNode p q) (DefenderStepNode a p' q)\<close> by auto
  have \<open>(\<exists> play \<in> plays_for_strategy f . hd play = AttackerNode p q)\<close>
294 295
    using challenge(1) assms by blast
  then obtain play where
benkeks committed
296
      play_spec: \<open>AttackerNode p q # play \<in> plays_for_strategy f\<close>
297
    by (metis list.sel(1) simple_game.plays.cases strategy_plays_subset)
benkeks committed
298
  hence interplay: \<open>(DefenderStepNode a p' q) # AttackerNode p q # play \<in> plays_for_strategy f\<close>
299
    using game_move by (simp add: player1_position_def simple_game.plays_for_strategy.p1move)
benkeks committed
300
  hence \<open>\<not> player1_wins ((DefenderStepNode a p' q) # AttackerNode p q # play)\<close>
301 302
    using assms(1) unfolding player0_winning_strategy_def by blast
  then obtain n1 where n1_def:
benkeks committed
303 304
      \<open>n1 = f (DefenderStepNode a p' q # AttackerNode p q # play)\<close>
      \<open>cs_game_moves (DefenderStepNode a p' q) n1\<close>
305 306
    using interplay assms(2) unfolding player0_winning_strategy_def sound_strategy_def by simp
  obtain q' where q'_spec:
benkeks committed
307
      \<open>(AttackerNode p' q') = n1\<close> \<open>q \<Rightarrow>^a q'\<close>
308
    using n1_def(2) by (cases n1, auto)
benkeks committed
309 310
  hence \<open>(AttackerNode p' q') # (DefenderStepNode a p' q) # AttackerNode p q # play
      \<in> plays_for_strategy f\<close>
311
    using interplay n1_def by (simp add: simple_game.plays_for_strategy.p0move)
benkeks committed
312 313
  hence \<open>R p' q'\<close> unfolding R_def by (meson list.sel(1))
  thus \<open>\<exists>q'. R p' q' \<and> q \<Rightarrow>^a  q'\<close> using q'_spec(2) by blast
314 315 316
next
  fix p q 
  assume challenge:
benkeks committed
317 318 319
    \<open>R p q\<close>
  hence game_move: \<open>cs_game_moves (AttackerNode p q) (DefenderCouplingNode p q)\<close> by auto
  have \<open>(\<exists> play \<in> plays_for_strategy f . hd play = AttackerNode p q)\<close>
320 321
    using challenge assms by blast
  then obtain play where
benkeks committed
322
      play_spec: \<open>AttackerNode p q # play \<in> plays_for_strategy f\<close>
323
    by (metis list.sel(1) simple_game.plays.cases strategy_plays_subset)
benkeks committed
324 325
  hence interplay: \<open>(DefenderCouplingNode p q) # AttackerNode p q # play
      \<in> plays_for_strategy f\<close>
326
    using game_move by (simp add: player1_position_def simple_game.plays_for_strategy.p1move)
benkeks committed
327
  hence \<open>\<not> player1_wins ((DefenderCouplingNode p q) # AttackerNode p q # play)\<close>
328 329
    using assms(1) unfolding player0_winning_strategy_def by blast
  then obtain n1 where n1_def:
benkeks committed
330 331
      \<open>n1 = f (DefenderCouplingNode p q # AttackerNode p q # play)\<close>
      \<open>cs_game_moves (DefenderCouplingNode p q) n1\<close>
332 333 334
    using interplay assms(2)
    unfolding player0_winning_strategy_def sound_strategy_def by simp
  obtain q' where q'_spec:
benkeks committed
335
      \<open>(AttackerNode q' p) = n1\<close> \<open>q \<longmapsto>* tau q'\<close>
336
    using n1_def(2) by (cases n1, auto)
benkeks committed
337 338
  hence \<open>(AttackerNode q' p) # (DefenderCouplingNode p q) # AttackerNode p q # play
      \<in> plays_for_strategy f\<close>
339
    using interplay n1_def by (simp add: simple_game.plays_for_strategy.p0move)
benkeks committed
340 341
  hence \<open>R q' p\<close> unfolding R_def by (meson list.sel(1))
  thus \<open>\<exists>q'. q \<longmapsto>* tau  q' \<and> R q' p\<close> using q'_spec(2) by blast
342 343 344 345
qed

theorem winning_strategy_iff_coupledsim:
  assumes
benkeks committed
346
    \<open>initial = AttackerNode p q\<close>
347
  shows 
benkeks committed
348 349
    \<open>(\<exists> f . player0_winning_strategy f \<and> sound_strategy f)
    = p \<sqsubseteq>cs q\<close>
350 351
proof (rule)
  assume
benkeks committed
352
    \<open>(\<exists>f. player0_winning_strategy f \<and> sound_strategy f)\<close>
353
  then obtain f where
benkeks committed
354
    \<open>coupled_simulation (\<lambda>p q. \<exists>play\<in>plays_for_strategy f. hd play = AttackerNode p q)\<close>
355
    using winning_strategy_implies_coupledsim by blast
benkeks committed
356
  moreover have \<open>(\<lambda>p q. \<exists>play\<in>plays_for_strategy f. hd play = AttackerNode p q) p q\<close>
357
    using assms plays_for_strategy.init[of f] by (meson list.sel(1))
benkeks committed
358
  ultimately show \<open>p \<sqsubseteq>cs q\<close> by blast
359 360
next
  assume
benkeks committed
361 362
    \<open>p \<sqsubseteq>cs  q\<close>
  thus \<open>(\<exists>f. player0_winning_strategy f \<and> sound_strategy f)\<close>
363 364 365 366 367 368 369
    using coupledsim_implies_winning_strategy[OF _ _ assms]
          strategy_from_coupledsim_sound[OF _ _ assms] by blast
qed

end

end