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_Delay.thy 19.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 with Delay Formulation\<close>

theory CS_Game_Delay
imports
  Coupled_Simulation
  Simple_Game
begin

subsection \<open>The Coupled Simulation Preorder Game Using Delay Steps\<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 18 19 20 21 22 23 24 25 26 27 28 29
  \<open>('s, 'a) cs_game_node \<Rightarrow> ('s, 'a) cs_game_node \<Rightarrow> bool\<close> where
  simulation_visible_challenge:
    \<open>cs_game_moves (AttackerNode p q) (DefenderStepNode a p1 q0) =
      (\<not>tau a \<and> p \<longmapsto>a p1 \<and> q = q0)\<close> |
  simulation_internal_attacker_move:
    \<open>cs_game_moves (AttackerNode p q) (AttackerNode p1 q0) =
      (\<exists>a. tau a \<and> p \<longmapsto>a p1 \<and> q = q0)\<close> |
  simulation_answer:
    \<open>cs_game_moves (DefenderStepNode a p1 q0) (AttackerNode p11 q1) =    
      (q0 =\<rhd>a q1 \<and> p1 = p11)\<close> |
  coupling_challenge:
    \<open>cs_game_moves (AttackerNode p q) (DefenderCouplingNode p0 q0) =
      (p = p0 \<and> q = q0)\<close> |
30
  coupling_answer:
benkeks committed
31 32
    \<open>cs_game_moves (DefenderCouplingNode p0 q0) (AttackerNode q1 p00) =
      (p0 = p00 \<and> q0 \<longmapsto>* tau q1)\<close> |
33
  cs_game_moves_no_step:
benkeks committed
34
    \<open>cs_game_moves _ _ = False\<close>
35

benkeks committed
36 37 38 39
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>
40 41 42 43 44

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

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

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

benkeks committed
59
lemma defender_preceded_by_attacker:
60
  assumes
benkeks committed
61 62 63 64
    \<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>
65
proof -
benkeks committed
66 67
  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)
68
    by (metis list.sel(1) list.sel(3) plays.cases)
benkeks committed
69 70 71
  thus \<open>\<exists>p q. hd play = AttackerNode p q \<and> cs_game_moves (AttackerNode p q) n0\<close> using assms(2)
    by (metis cs_game_defender_node.elims(2,3) local.cs_game_moves_no_step(1,2,3,6))
  show \<open>play \<noteq> []\<close> using n0_not_init assms(1) plays.cases by auto
72 73
qed

benkeks committed
74 75 76 77 78 79 80 81 82
lemma defender_only_challenged_by_visible_actions:
  assumes
    \<open>initial = AttackerNode p0 q0\<close>
    \<open>(DefenderStepNode a p q) # play \<in> plays\<close>
  shows
    \<open>\<not>tau a\<close>
  using assms defender_preceded_by_attacker
  by fastforce

83 84
lemma strategy_from_coupleddsim_retains_coupledsim:
  assumes
benkeks committed
85 86 87 88
    \<open>R p0 q0\<close>
    \<open>coupled_delay_simulation R\<close>
    \<open>initial = AttackerNode p0 q0\<close>
    \<open>play \<in> plays_for_strategy (strategy_from_coupleddsim R)\<close>
89
  shows
benkeks committed
90 91
    \<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>
92 93 94 95
  using assms(4)
proof (induct arbitrary: p q rule: plays_for_strategy.induct[OF assms(4)])
  case 1
  fix p q
benkeks committed
96 97 98
  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
99 100 101
next
  case 1
  fix p q
benkeks committed
102
  assume \<open>1 < length [initial]\<close>
103
  hence False by auto
benkeks committed
104
  thus \<open>R p q\<close>  ..
105 106
next
  case (2 n0 play)
benkeks committed
107
  hence n0play_is_play: \<open>n0 # play \<in> plays\<close> using strategy_plays_subset by blast
108 109
  fix p q
  assume subassms:
benkeks committed
110 111 112
    \<open>hd (strategy_from_coupleddsim R (n0 # play) # n0 # play) = AttackerNode p q\<close>
    \<open>strategy_from_coupleddsim R (n0 # play) # n0 # play
      \<in> plays_for_strategy (strategy_from_coupleddsim R)\<close>
113
  then obtain pi qi where 
benkeks committed
114 115 116
      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)]
117
    by blast
benkeks committed
118 119 120
  hence \<open>R pi qi\<close> using 2(1,3) by simp
  have \<open>(\<exists> a . n0 = (DefenderStepNode a p qi) \<and> \<not> tau a \<and> pi \<longmapsto>a p)
    \<or> (n0 = (DefenderCouplingNode pi qi))\<close>
121
    using piqi_def(2) 2(4,5) subassms(1)
benkeks committed
122 123 124 125
    using cs_game_defender_node.elims(2) cs_game_moves.simps(1,3)
      cs_game_moves.simps(4) list.sel(1)
    by metis
  thus \<open>R p q\<close>
126 127
  proof safe
    fix a
benkeks committed
128 129 130
    assume n0_def: \<open>n0 = DefenderStepNode a p qi\<close> \<open>\<not> tau a\<close> \<open>pi \<longmapsto>a p\<close>
    have \<open>strategy_from_coupleddsim R (n0 # play) =
        (AttackerNode p (SOME q1 . R p q1 \<and> qi =\<rhd>a q1))\<close>
131
      unfolding n0_def(1) by auto
benkeks committed
132 133 134
    with subassms(1) have q_def: \<open>q = (SOME q1. R p q1 \<and> qi =\<rhd>a  q1)\<close> by auto
    have \<open>\<exists> qii . R p qii \<and> qi =\<rhd>a qii\<close>
      using n0_def(2,3) `R pi qi` `coupled_delay_simulation R`
135
      unfolding coupled_delay_simulation_def delay_simulation_def by blast
benkeks committed
136
    from someI_ex[OF this] show \<open>R p q\<close> unfolding q_def by blast
137
  next
benkeks committed
138 139 140
    assume n0_def: \<open>n0 = DefenderCouplingNode pi qi\<close>
    have \<open>strategy_from_coupleddsim R (n0 # play) =
        (AttackerNode (SOME q1 . R q1 pi \<and> qi \<longmapsto>* tau q1) pi)\<close>
141
      unfolding n0_def(1) by auto
benkeks committed
142 143
    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>
144 145
      using n0_def `R pi qi` `coupled_delay_simulation R`
      unfolding coupled_delay_simulation_def by blast
benkeks committed
146
    from someI_ex[OF this] show \<open>R p q\<close> unfolding qp_def by blast
147 148 149 150
  qed
next
  case (2 n0 play)
  fix p q
benkeks committed
151
  assume \<open>hd (tl (strategy_from_coupleddsim R (n0 # play) # n0 # play)) = AttackerNode p q\<close>
152
  hence False using 2(4) by auto
benkeks committed
153
  thus \<open>R p q\<close> ..
154 155 156
next
  case (3 n1 play n1')
  fix p q
benkeks committed
157 158 159 160 161 162 163 164
  assume \<open>hd (n1' # n1 # play) = AttackerNode p q\<close>
  then obtain p1 a where n1_spec: \<open>n1 = AttackerNode p1 q\<close> \<open>p1 \<longmapsto>a p\<close> \<open>tau a\<close>
   using 3 unfolding player1_position_def list.sel(1) 
   by (metis cs_game_defender_node.elims(3) simulation_internal_attacker_move)
  then have \<open>R p1 q\<close> using 3 by auto
  thus \<open>R p q\<close> 
    using  n1_spec(2,3) \<open>coupled_delay_simulation R\<close>
    unfolding coupled_delay_simulation_def delay_simulation_def by auto
165 166 167
next
  case (3 n1 play n1')
  fix p q
benkeks committed
168 169
  assume \<open>hd (tl (n1' # n1 # play)) = AttackerNode p q\<close>
  thus \<open>R p q\<close> using 3(1,2) by auto
170 171 172 173
qed

lemma strategy_from_coupleddsim_sound:
  assumes
benkeks committed
174 175 176
    \<open>R p0 q0\<close>
    \<open>coupled_delay_simulation R\<close>
    \<open>initial = AttackerNode p0 q0\<close>
177
  shows
benkeks committed
178
    \<open>sound_strategy (strategy_from_coupleddsim R)\<close>
179 180 181 182
  unfolding sound_strategy_def
proof clarify
  fix n0 play
  assume subassms:
benkeks committed
183 184
    \<open>n0 # play \<in> plays_for_strategy(strategy_from_coupleddsim R)\<close>
    \<open>cs_game_defender_node n0\<close>
185
  then obtain pi qi where 
benkeks committed
186 187 188
      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)]
189
      strategy_plays_subset by blast
benkeks committed
190
  hence \<open>R pi qi\<close>
191
    using strategy_from_coupleddsim_retains_coupledsim[OF assms] list.sel subassms by auto
benkeks committed
192 193
  have \<open>(\<exists> a p . n0 = (DefenderStepNode a p qi) \<and> pi \<longmapsto>a p)
    \<or> (n0 = (DefenderCouplingNode pi qi))\<close>
194
    by (metis cs_game_defender_node.elims(2)
benkeks committed
195 196
        coupling_challenge simulation_visible_challenge piqi_def(2) subassms(2))
  thus \<open>cs_game_moves n0 (strategy_from_coupleddsim R (n0 # play))\<close>
197 198 199
  proof safe
    fix a p
    assume dsn:
benkeks committed
200 201
      \<open>pi \<longmapsto>a  p\<close>
      \<open>n0 = DefenderStepNode a p qi\<close>
202
    hence qi_spec:
benkeks committed
203 204
      \<open>(strategy_from_coupleddsim R (n0 # play)) =
        AttackerNode p (SOME q1 . R p q1 \<and> qi =\<rhd>a q1)\<close>
205 206
      by simp
    then obtain qii where qii_spec:
benkeks committed
207 208 209 210 211 212 213
      \<open>AttackerNode p (SOME q1 . R p q1 \<and> qi =\<rhd>a q1) = AttackerNode p qii\<close> by blast
    have \<open>\<exists> qii . R p qii \<and> qi =\<rhd>a qii\<close>
      using dsn `R pi qi` `coupled_delay_simulation R` steps.refl 
      unfolding coupled_delay_simulation_def delay_simulation_def by blast
    from someI_ex[OF this] have \<open>R p qii \<and> qi =\<rhd>a qii\<close> using qii_spec by blast
    thus \<open>cs_game_moves (DefenderStepNode a p qi)
          (strategy_from_coupleddsim R (DefenderStepNode a p qi # play))\<close>
214 215 216
      using qi_spec qii_spec unfolding dsn(2) by auto
  next \<comment>\<open>coupling quite analogous.\<close>
    assume dcn:
benkeks committed
217
      \<open>n0 = DefenderCouplingNode pi qi\<close>
218
    hence qi_spec:
benkeks committed
219 220
      \<open>(strategy_from_coupleddsim R (n0 # play)) =
      AttackerNode (SOME q1 . R q1 pi \<and> qi \<longmapsto>* tau q1) pi\<close>
221 222
      by simp
    then obtain qii where qii_spec:
benkeks committed
223 224
      \<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>
225 226
      using dcn `R pi qi` `coupled_delay_simulation R`
      unfolding coupled_delay_simulation_def by blast
benkeks committed
227 228 229
    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_coupleddsim R (DefenderCouplingNode pi qi # play))\<close>
230 231 232 233 234 235
      using qi_spec qii_spec unfolding dcn by auto
  qed
qed

lemma coupleddsim_implies_winning_strategy:
  assumes
benkeks committed
236 237 238
    \<open>R p q\<close>
    \<open>coupled_delay_simulation R\<close>
    \<open>initial = AttackerNode p q\<close>
239
  shows
benkeks committed
240
    \<open>player0_winning_strategy (strategy_from_coupleddsim R)\<close>
241 242 243 244
  unfolding player0_winning_strategy_def
proof (clarify)
  fix play
  assume subassms:
benkeks committed
245 246 247
    \<open>play \<in> plays_for_strategy (strategy_from_coupleddsim R)\<close>
    \<open>player1_wins play\<close>
  show \<open>False\<close> using subassms
248 249 250 251 252
  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
253
    hence \<open>\<not> cs_game_defender_node (strategy_from_coupleddsim R (n0 # play))\<close>
254
      using cs_game_moves_no_step cs_game_defender_node.elims(2) by metis
benkeks committed
255
    hence \<open>\<not>  player1_wins (strategy_from_coupleddsim R (n0 # play) # n0 # play)\<close>
256 257 258 259
      unfolding player1_wins_def by auto
    thus ?case using 2(6) by auto
  next
    case (3 n1 play n1')
benkeks committed
260
    then obtain p q where n1_def: \<open>n1 = AttackerNode p q\<close>
261
      unfolding player1_position_def using cs_game_defender_node.elims(3) by blast
benkeks committed
262 263 264 265
    hence \<open>R p q\<close>
      using strategy_from_coupleddsim_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>
266
      using n1_def `cs_game_moves n1 n1'` coupling_challenge cs_game_moves_no_step(5)
benkeks committed
267 268
        simulation_visible_challenge
      by (metis cs_game_defender_node.elims(2) 3(6) list.sel(1) player1_wins_def)
269 270
    then show ?case
    proof 
benkeks committed
271
      assume \<open>(\<exists> p1 a . n1' = (DefenderStepNode a p1 q) \<and> (p \<longmapsto>a p1))\<close>
272
      then obtain p1 a where 
benkeks committed
273
        n1'_def: \<open>n1' = (DefenderStepNode a p1 q)\<close> \<open>p \<longmapsto>a p1\<close>
274
        by blast
benkeks committed
275
      hence \<open>\<exists> q1 . q =\<rhd>a q1\<close> 
276 277
        using `R p q` `coupled_delay_simulation R`
        unfolding coupled_delay_simulation_def delay_simulation_def by blast
benkeks committed
278
      hence \<open>\<exists> q1 . cs_game_moves (DefenderStepNode a p1 q) (AttackerNode p1 q1)\<close>
279 280 281 282
        by auto
      with `player1_wins (n1' # n1 # play)` show False unfolding player1_wins_def n1'_def
        by (metis list.sel(1))
    next
benkeks committed
283 284
      assume n1'_def: \<open>n1' = DefenderCouplingNode p q\<close>
      have \<open>\<exists> q1 . q \<longmapsto>*tau q1\<close> 
285 286
        using `coupled_delay_simulation R` `R p q`
        unfolding coupled_delay_simulation_def by blast
benkeks committed
287
      hence \<open>\<exists> q1 . cs_game_moves (DefenderCouplingNode p q) (AttackerNode q1 p)\<close>
288 289 290 291 292 293 294 295 296 297 298
        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_coupleddsim:
  assumes
benkeks committed
299 300
    \<open>player0_winning_strategy f\<close>
    \<open>sound_strategy f\<close>
301
  defines
benkeks committed
302
    \<open>R == \<lambda> p q . (\<exists> play \<in> plays_for_strategy f . hd play = AttackerNode p q)\<close>
303
  shows
benkeks committed
304
    \<open>coupled_delay_simulation R\<close>
305 306 307 308
  unfolding coupled_delay_simulation_def delay_simulation_def
proof safe
  fix p q p' a
  assume challenge:
benkeks committed
309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329
    \<open>R p q\<close>
    \<open>p \<longmapsto>a  p'\<close>
    \<open>tau a \<close>
  hence game_move: \<open>cs_game_moves (AttackerNode p q) (AttackerNode p' q)\<close> by auto
  have \<open>(\<exists> play \<in> plays_for_strategy f . hd play = AttackerNode p q)\<close>
    using challenge(1) assms by blast
  then obtain play where
      play_spec: \<open>AttackerNode p q # play \<in> plays_for_strategy f\<close>
    by (metis list.sel(1) simple_game.plays.cases strategy_plays_subset)
  hence interplay: \<open>(AttackerNode p' q) # AttackerNode p q # play \<in> plays_for_strategy f\<close>
    using game_move by (simp add: player1_position_def simple_game.plays_for_strategy.p1move)
  then show \<open>R p' q\<close>
    unfolding R_def list.sel by force
next
  fix p q p' a
  assume challenge:
    \<open>R p q\<close>
    \<open>p \<longmapsto>a  p'\<close>
    \<open>\<not> tau a \<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>
330 331
    using challenge(1) assms by blast
  then obtain play where
benkeks committed
332
      play_spec: \<open>AttackerNode p q # play \<in> plays_for_strategy f\<close>
333
    by (metis list.sel(1) simple_game.plays.cases strategy_plays_subset)
benkeks committed
334
  hence interplay: \<open>(DefenderStepNode a p' q) # AttackerNode p q # play \<in> plays_for_strategy f\<close>
335
    using game_move by (simp add: player1_position_def simple_game.plays_for_strategy.p1move)
benkeks committed
336
  hence \<open>\<not> player1_wins ((DefenderStepNode a p' q) # AttackerNode p q # play)\<close>
337 338
    using assms(1) unfolding player0_winning_strategy_def by blast
  then obtain n1 where n1_def:
benkeks committed
339 340
      \<open>n1 = f (DefenderStepNode a p' q # AttackerNode p q # play)\<close>
      \<open>cs_game_moves (DefenderStepNode a p' q) n1\<close>
341 342
    using interplay assms(2) unfolding player0_winning_strategy_def sound_strategy_def by simp
  obtain q' where q'_spec:
benkeks committed
343
      \<open>(AttackerNode p' q') = n1\<close> \<open>q =\<rhd>a q'\<close>
344
    using n1_def(2) by (cases n1, auto)
benkeks committed
345 346
  hence \<open>(AttackerNode p' q') # (DefenderStepNode a p' q) # AttackerNode p q # play
      \<in> plays_for_strategy f\<close>
347
    using interplay n1_def by (simp add: simple_game.plays_for_strategy.p0move)
benkeks committed
348 349
  hence \<open>R p' q'\<close> unfolding R_def by (meson list.sel(1))
  thus \<open>\<exists>q'. R p' q' \<and> q =\<rhd>a  q'\<close> using q'_spec(2) by blast
350 351 352
next
  fix p q 
  assume challenge:
benkeks committed
353 354 355
    \<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>
356 357
    using challenge assms by blast
  then obtain play where
benkeks committed
358
      play_spec: \<open>AttackerNode p q # play \<in> plays_for_strategy f\<close>
359
    by (metis list.sel(1) simple_game.plays.cases strategy_plays_subset)
benkeks committed
360 361
  hence interplay: \<open>(DefenderCouplingNode p q) # AttackerNode p q # play
      \<in> plays_for_strategy f\<close>
362
    using game_move by (simp add: player1_position_def simple_game.plays_for_strategy.p1move)
benkeks committed
363
  hence \<open>\<not> player1_wins ((DefenderCouplingNode p q) # AttackerNode p q # play)\<close>
364 365
    using assms(1) unfolding player0_winning_strategy_def by blast
  then obtain n1 where n1_def:
benkeks committed
366 367
      \<open>n1 = f (DefenderCouplingNode p q # AttackerNode p q # play)\<close>
      \<open>cs_game_moves (DefenderCouplingNode p q) n1\<close>
368 369 370
    using interplay assms(2)
    unfolding player0_winning_strategy_def sound_strategy_def by simp
  obtain q' where q'_spec:
benkeks committed
371
      \<open>(AttackerNode q' p) = n1\<close> \<open>q \<longmapsto>* tau q'\<close>
372
    using n1_def(2) by (cases n1, auto)
benkeks committed
373 374
  hence \<open>(AttackerNode q' p) # (DefenderCouplingNode p q) # AttackerNode p q # play
      \<in> plays_for_strategy f\<close>
375
    using interplay n1_def by (simp add: simple_game.plays_for_strategy.p0move)
benkeks committed
376 377
  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
378 379 380 381
qed

theorem winning_strategy_iff_coupledsim:
  assumes
benkeks committed
382
    \<open>initial = AttackerNode p q\<close>
383
  shows 
benkeks committed
384 385
    \<open>(\<exists> f . player0_winning_strategy f \<and> sound_strategy f)
    = p \<sqsubseteq>cs q\<close>
386 387
proof (rule)
  assume
benkeks committed
388
    \<open>(\<exists>f. player0_winning_strategy f \<and> sound_strategy f)\<close>
389
  then obtain f where
benkeks committed
390
    \<open>coupled_delay_simulation (\<lambda>p q. \<exists>play\<in>plays_for_strategy f. hd play = AttackerNode p q)\<close>
391
    using winning_strategy_implies_coupleddsim by blast
benkeks committed
392
  moreover have \<open>(\<lambda>p q. \<exists>play\<in>plays_for_strategy f. hd play = AttackerNode p q) p q\<close>
393
    using assms plays_for_strategy.init[of f] by (meson list.sel(1))
benkeks committed
394 395
  ultimately show \<open>p \<sqsubseteq>cs q\<close>
    unfolding coupled_sim_by_eq_coupled_delay_simulation
396 397 398
    by (metis (mono_tags, lifting))
next
  assume
benkeks committed
399 400 401
    \<open>p \<sqsubseteq>cs  q\<close>
  thus \<open>(\<exists>f. player0_winning_strategy f \<and> sound_strategy f)\<close>
    unfolding coupled_sim_by_eq_coupled_delay_simulation
402 403 404 405 406 407 408
    using coupleddsim_implies_winning_strategy[OF _ _ assms]
          strategy_from_coupleddsim_sound[OF _ _ assms] by blast
qed

end

end