Theory Contrasim_Set_Game

section ‹The Contrasimulation Preorder Set Game›

theory Contrasim_Set_Game
imports
  Simple_Game
  Contrasimulation
begin

datatype ('s, 'a) c_set_game_node =
  AttackerNode 's "'s set" |
  DefenderSimNode 'a 's "'s set" |
  DefenderSwapNode 's "'s set"

fun (in lts_tau) c_set_game_moves ::
  ‹('s, 'a) c_set_game_node ⇒ ('s, 'a) c_set_game_node ⇒ bool› where

  simulation_challenge:
   ‹c_set_game_moves (AttackerNode p Q) (DefenderSimNode a p1 Q0) =
     (p =⊳a p1 ∧ Q = Q0 ∧ ¬ tau a)› |

  simulation_answer:
    ‹c_set_game_moves (DefenderSimNode a p1 Q) (AttackerNode p10 Q1) =
      (p1 = p10 ∧ Q1 = dsuccs a Q)› |

  swap_challenge:
    ‹c_set_game_moves (AttackerNode p Q) (DefenderSwapNode p1 Q0) =
     (p ⇒^τ p1 ∧ Q = Q0)› |

  swap_answer:
    ‹c_set_game_moves (DefenderSwapNode p1 Q) (AttackerNode q1 P1) =
      (q1 ∈ weak_tau_succs Q ∧ P1 = {p1})› |

  c_set_game_moves_no_step:
    ‹c_set_game_moves _ _ = False›

fun c_set_game_defender_node :: ‹('s, 'a) c_set_game_node ⇒ bool› where
  ‹c_set_game_defender_node (AttackerNode _ _) = False› |
  ‹c_set_game_defender_node (DefenderSimNode _ _ _) = True› |
  ‹c_set_game_defender_node (DefenderSwapNode _ _) = True›

subsection ‹Contrasimulation Implies Winning Strategy in Set Game (Completeness)›

locale c_set_game =
  lts_tau trans τ +
  simple_game c_set_game_moves c_set_game_defender_node
for
  trans :: ‹'s ⇒ 'a ⇒ 's ⇒ bool› and
  τ :: ‹'a›
begin

fun strategy_from_mimicking_of_C ::
    ‹('s ⇒ ('s set) ⇒ bool) ⇒ ('s, 'a) c_set_game_node strategy›
  where
  
    ‹strategy_from_mimicking_of_C R ((DefenderSwapNode p1 Q)#play) = 
      (AttackerNode (SOME q1 . (∃q. (q ∈ Q ∧ q  ⇒^τ q1)) ∧ R q1 {p1}) {p1})› |
  
    ‹strategy_from_mimicking_of_C R ((DefenderSimNode a p1 Q)#play) = 
      (AttackerNode p1 (SOME Q1 . Q1 = dsuccs a Q ∧ R p1 Q1))› |
   
    ‹strategy_from_mimicking_of_C _ _ = undefined›

lemma csg_atknodes_precede_defnodes_in_plays:
  assumes 
    ‹c_set_game_defender_node n0›
    ‹(n0#play) ∈ plays (AttackerNode p0 Q0)›
  shows ‹∃p Q. (hd play) = AttackerNode p Q ∧ c_set_game_moves (hd play) n0›
proof -
  have ‹n0 ≠ AttackerNode p0 Q0› using assms by auto
  hence mov: ‹c_set_game_moves (hd play) n0› using assms(2)
    by (metis list.inject list.sel(1) plays.cases) 
  from assms(1) have def_cases: 
    ‹∃p1 Q. (∃a. n0 = DefenderSimNode a p1 Q) ∨ n0 = DefenderSwapNode p1 Q›  
    using c_set_game_defender_node.elims(2) by blast
  then obtain p1 Q where
    pQ_def: ‹(∃a. n0 = DefenderSimNode a p1 Q) ∨ n0 = DefenderSwapNode p1 Q› 
    by auto
  hence ‹∃p. (hd play) = AttackerNode p Q›
  proof (rule disjE)
    assume ‹∃a. n0 = DefenderSimNode a p1 Q›
    then obtain a where a_def: ‹n0 = DefenderSimNode a p1 Q› ..
    thus ?thesis using  c_set_game_moves.elims(2)[OF mov] c_set_game_node.distinct(5) by auto
  next 
    assume ‹n0 = DefenderSwapNode p1 Q›
    thus ?thesis using c_set_game_moves.elims(2)[OF mov] c_set_game_node.distinct(5) by auto
  qed
  thus ?thesis using mov by auto
qed

lemma csg_second_play_elem_in_play_set:
  assumes 
    ‹(n0#play) ∈ plays (AttackerNode p0 Q0)›
    ‹c_set_game_defender_node n0›
  shows
    ‹hd play ∈ set (n0 # play)›
proof - 
  from assms have ‹n0 ≠ AttackerNode p0 Q0› by auto 
  hence ‹play ∈ plays (AttackerNode p0 Q0)›
    using assms(1) plays.cases no_empty_plays by blast
  hence play_split: ‹∃x xs. play = x#xs› using no_empty_plays
    using plays.cases by blast 
  then obtain x where x_def: ‹∃xs. play = x#xs› ..
  have x_in_set: ‹x ∈ set (n0#play)› using x_def by auto
  have x_head: ‹x = hd play› using x_def by auto
  from x_in_set x_head show ‹hd play ∈ set (n0 # play)› by auto
qed

lemma csg_only_defnodes_move_to_atknodes:
  assumes  
    ‹c_set_game_moves n0 n1›
    ‹n1 = AttackerNode p Q›
  shows 
    ‹(∃Qpred a. n0 = (DefenderSimNode a p Qpred)) ∨
    (∃q Ppred. n0 = (DefenderSwapNode q Ppred) ∧ Q = {q})›
proof (cases n0 rule: c_set_game_node.exhaust)
  case (AttackerNode s T)
  hence ‹c_set_game_moves (AttackerNode s T) (AttackerNode p Q)› using assms by auto 
  hence ‹False› by simp
  then show ?thesis by auto
next
  case (DefenderSimNode a s T)
  then show ?thesis using assms by auto
next
  case (DefenderSwapNode s T)
  hence ‹c_set_game_moves (DefenderSwapNode s T) (AttackerNode p Q)› using assms by auto 
  then show ?thesis using DefenderSwapNode by auto
qed

lemma c_set_game_strategy_retains_mimicking:
  assumes
    ‹contrasimulation C›
    ‹C p0 q0›
    ‹play ∈ plays_for_0strategy
      (strategy_from_mimicking_of_C (mimicking (set_lifted C))) (AttackerNode p0 {q0})›
  shows
    ‹n = AttackerNode p Q ⟹ n ∈ set play ⟹ mimicking (set_lifted C) p Q ›
proof (induct arbitrary: n p Q rule: plays_for_0strategy.induct[OF assms(3)])
  case init: 1
  hence ‹p = p0 ∧ Q = {q0}› using init.prems(1) by auto 
  thus ‹mimicking (set_lifted C) p Q›
    using assms R_is_in_mimicking_of_R set_lifted_def by simp
next
  case p0moved: (2 n0 play) 
  hence ‹(n = strategy_from_mimicking_of_C
    (mimicking (set_lifted C)) (n0 # play)) ∨ (n ∈ set (n0#play))› by auto
  thus ?case
  proof(rule disjE)
    assume ‹n ∈ set (n0#play)›
    thus ?thesis using p0moved.prems p0moved.hyps(1,2) by blast 
  next
    assume strat: ‹n = strategy_from_mimicking_of_C
      (mimicking (set_lifted C)) (n0 # play)›
    hence ‹(∃a Qpred. n0 = DefenderSimNode a p Qpred) ∨
        (∃q Ppred. n0 = DefenderSwapNode q Ppred ∧ Q = {q})›
      using csg_only_defnodes_move_to_atknodes[OF p0moved.hyps(4), of ‹p› ‹Q›]
        p0moved.prems(1)
      by blast 
    thus ?case 
    proof (rule disjE)
      assume ‹∃a Qpred. n0 = DefenderSimNode a p Qpred›
      then obtain a Qpred where n0_def: ‹n0 = DefenderSimNode a p Qpred› by auto
      hence ‹strategy_from_mimicking_of_C (mimicking (set_lifted C)) (n0#play)
          = AttackerNode p (SOME Q1. Q1 = dsuccs a Qpred ∧ (mimicking (set_lifted C)) p Q1)›
        using strategy_from_mimicking_of_C.simps(2) by auto
      hence Q_def: ‹Q = (SOME Q1. Q1 = dsuccs a Qpred ∧ (mimicking (set_lifted C)) p Q1)›
        using strat by (simp add: p0moved.prems(1))
      have ‹∃ppred. hd play = (AttackerNode ppred Qpred) ∧ c_set_game_moves (hd play) n0› 
        using csg_atknodes_precede_defnodes_in_plays
              strategy0_plays_subset[OF p0moved.hyps(1)] assms(2,3) n0_def by force
      then obtain ppred where ppred_def: ‹hd play = (AttackerNode ppred Qpred)› 
          and ‹c_set_game_moves (hd play) n0› by auto
      hence ‹ppred =⊳a p› ‹a ≠ τ› using n0_def by auto
      hence ‹hd play ∈ set (n0 # play)› 
        using csg_second_play_elem_in_play_set strategy0_plays_subset[OF p0moved.hyps(1)]
          assms(3) n0_def
        by (simp add: assms(3))
      hence ‹mimicking (set_lifted C) ppred Qpred›
        using p0moved.hyps(2) ppred_def by blast
      hence ‹mimicking (set_lifted C) p (dsuccs a Qpred)› 
        using ‹ppred =⊳a p› assms(1,2) mimicking_of_C_guarantees_action_succ ‹a ≠ τ›
        by auto
      hence ‹∃Q. Q = (dsuccs a Qpred) ∧ mimicking (set_lifted C) p Q› by auto
      from someI_ex[OF this] show ‹mimicking (set_lifted C) p Q› 
        unfolding Q_def
        using n0_def p0moved.hyps(4) by auto
    next
      assume ‹(∃q Ppred. n0 = DefenderSwapNode q Ppred ∧ Q = {q})›
      then obtain q Ppred where
          n0_def: ‹n0 = DefenderSwapNode q Ppred› and
          Q_def: ‹Q = {q}› 
        by auto
      hence ‹strategy_from_mimicking_of_C (mimicking (set_lifted C)) (n0#play)
         = AttackerNode (SOME p1.
            (∃p. p ∈ Ppred ∧ p ⇒^τ p1) ∧ (mimicking (set_lifted C)) p1 {q}) {q}› 
        using strategy_from_mimicking_of_C.simps(1) by auto
      hence p_def: ‹p = (SOME p1.
            (∃p. p ∈ Ppred ∧ p ⇒^τ p1) ∧ (mimicking (set_lifted C)) p1 {q})› 
        using strat p0moved.prems by auto
      have ‹∃qpred. hd play = (AttackerNode qpred Ppred) ∧ c_set_game_moves (hd play) n0›
        using csg_atknodes_precede_defnodes_in_plays
          strategy0_plays_subset[OF p0moved.hyps(1)] assms(3) n0_def
        by force
      then obtain qpred where qpred_def: ‹hd play = (AttackerNode qpred Ppred)› 
        and qpred_move: ‹c_set_game_moves (hd play) n0› by auto
      hence p1: ‹player1_position (hd play)› by simp
      have qpred_q_move: ‹qpred ⇒^τ q› using qpred_def qpred_move n0_def by simp
      have ‹hd play ∈ set (n0 # play)› 
        using csg_second_play_elem_in_play_set strategy0_plays_subset[OF p0moved.hyps(1)]
          assms(3) n0_def
        by simp 
      hence ‹mimicking (set_lifted C) qpred Ppred›
        using p0moved.hyps(2) qpred_def by blast
      hence ‹∃p. p ∈ weak_tau_succs Ppred ∧ mimicking (set_lifted C) p {q}› 
        using qpred_q_move assms(1,2) mimicking_of_C_guarantees_tau_succ by blast
      hence ‹∃p. (∃p0. p0 ∈ Ppred ∧ p0 ⇒^τ  p) ∧ mimicking (set_lifted C) p {q}› 
        using weak_tau_succs_def[of ‹Ppred›] by blast
      from someI_ex[OF this] p_def have ‹mimicking (set_lifted C) p {q}› by simp
      thus ‹mimicking (set_lifted C) p Q› using Q_def by blast
    qed
  qed
next
  case p1moved: (3 n1 play n1') 
  hence ‹(n = n1') ∨ (n ∈ set (n1#play))› by auto
  thus ?case
  proof (rule disjE)
    assume ‹n ∈ set (n1#play)›
    thus ?case using p1moved.prems p1moved.hyps(1,2) by blast 
  next
    assume A1: ‹n = n1'›
    hence ‹c_set_game_defender_node n1'›
      using csg_only_defnodes_move_to_atknodes p1moved.hyps(3, 4) p1moved.prems(1)
        by fastforce
    hence ‹False› using A1 p1moved.prems(1) by auto
    thus ?case by auto
  qed
qed

lemma contrasim_set_game_complete:
  assumes
    ‹contrasimulation C›
    ‹C p0 q0›
  shows
    ‹player0_winning_strategy (strategy_from_mimicking_of_C
      (mimicking (set_lifted C))) (AttackerNode p0 {q0})›
  unfolding player0_winning_strategy_def
proof (safe)
  fix play
  assume A1: ‹play ∈ (plays_for_0strategy
    (strategy_from_mimicking_of_C (mimicking (set_lifted C))) (AttackerNode p0 {q0}))›
  thus ‹player1_wins_immediately play ⟹ False›
    unfolding player1_wins_immediately_def
  proof clarify
    assume A:
      ‹c_set_game_defender_node (hd play)›
      ‹∄p'. c_set_game_moves (hd play) p'› 
    have player0_has_succ_node:
      ‹c_set_game_defender_node (hd play) ⟹ ∃p'. c_set_game_moves (hd play) p'›
    proof (induct rule: simple_game.plays_for_0strategy.induct[OF A1])
      case init: 1
      have ‹¬c_set_game_defender_node (AttackerNode p0 {q0})› by (simp add: assms) 
      hence ‹False› using init.prems by simp
      then show ?case ..
    next
      case p0moved: (2 n0 play)
      from p0moved.hyps have ‹c_set_game_defender_node n0› by simp
      hence ‹(∃a p1 q. n0 = (DefenderSimNode a p1 q)) ∨ (∃q P. n0 = DefenderSwapNode q P)›
        by (meson c_set_game_defender_node.elims(2)) 
      hence ‹¬c_set_game_defender_node (strategy_from_mimicking_of_C
          (mimicking (set_lifted C)) (n0#play))›
        using p0moved.hyps(4) 
          c_set_game_moves.elims(2)[of ‹n0›
            ‹strategy_from_mimicking_of_C (mimicking (set_lifted C)) (n0#play)›]
        by force 
      hence ‹¬c_set_game_defender_node (hd (strategy_from_mimicking_of_C
          (mimicking (set_lifted C)) (n0 # play) # n0 # play))› 
        by simp
      hence ‹False› using p0moved.prems ..
      then show ?case ..
    next
      case p1moved: (3 n1 play n1') 
      hence ‹¬c_set_game_defender_node n1›
        using p1moved.hyps by simp
      then obtain p Q where n1_def: ‹n1 = AttackerNode p Q›
        using c_set_game_defender_node.elims(3) by auto
      hence in_mimicking: ‹mimicking (set_lifted C) p Q› 
        using c_set_game_strategy_retains_mimicking[OF assms, of ‹n1#play›, OF p1moved.hyps(1)]
        by auto
      have ‹(∃a p1. n1' = DefenderSimNode a p1 Q) ∨ (∃p1. n1' = DefenderSwapNode p1 Q)› 
        using p1moved.prems n1_def p1moved.hyps(4)
        by (metis c_set_game_defender_node.elims(2) list.sel(1)
            local.simulation_challenge local.swap_challenge)
      thus ?case
      proof (rule disjE)
        assume A: ‹∃a p1. n1' = DefenderSimNode a p1 Q›
        then obtain a p1 where n1'_def : ‹n1' = DefenderSimNode a p1 Q› by auto
        have move: ‹c_set_game_moves (AttackerNode p Q) (DefenderSimNode a p1 Q)› 
          using p1moved.hyps n1_def n1'_def by auto
        hence ‹p =⊳a p1› by auto
        hence ‹p ⇒^a p1› using steps.refl by blast 
        hence ‹mimicking (set_lifted C) p1 (dsuccs a Q)› 
          using mimicking_of_C_guarantees_action_succ move
          by (metis in_mimicking assms(1) simulation_challenge tau_tau) 
        then obtain Q1 where ‹Q1 = dsuccs a Q ∧ mimicking (set_lifted C) p1 Q1› by blast
        hence ‹c_set_game_moves n1' (AttackerNode p1 Q1)› 
          using A n1'_def by auto
        thus ‹∃a. c_set_game_moves (hd (n1' # n1 # play)) a› by auto
      next
        assume  ‹∃p1. n1' = DefenderSwapNode p1 Q›
        then obtain p1 where n1'_def: ‹n1' = DefenderSwapNode p1 Q› ..
        hence ‹c_set_game_moves (AttackerNode p Q) (DefenderSwapNode p1 Q)› 
          using p1moved.hyps(4) n1_def by auto
        hence p_succ: ‹p ⇒^τ p1› by auto
        hence ‹∃q'. q' ∈ weak_tau_succs Q ∧ mimicking (set_lifted C) q' {p1}› 
          using in_mimicking mimicking_of_C_guarantees_tau_succ assms(1) by auto
        hence ‹∃q1. q1 ∈ weak_tau_succs Q ∧ mimicking (set_lifted C) q1 {p1}› by auto
        hence ‹∃q1 P1. c_set_game_moves n1' (AttackerNode q1 P1)› using n1'_def  by auto  
        thus ‹∃a. c_set_game_moves (hd (n1' # n1 # play)) a› by auto
      qed
    qed
    hence ‹False› using A by auto
    thus ?thesis by auto
  qed
qed

lemma csg_strategy_from_mimicking_of_C_sound:
  assumes
    ‹contrasimulation C›
    ‹C p0 q0›
  shows
    ‹sound_0strategy
      (strategy_from_mimicking_of_C (mimicking (set_lifted C)))
      (AttackerNode p0 {q0})›
  unfolding sound_0strategy_def
proof (safe)
  fix n0 play
  assume A:
    ‹n0 # play ∈ plays_for_0strategy
      (strategy_from_mimicking_of_C (mimicking (set_lifted C))) (AttackerNode p0 {q0})›
    ‹c_set_game_defender_node n0›
  hence ‹(∃a p' Q. n0 = DefenderSimNode a p' Q) ∨ (∃p' Q. n0 = DefenderSwapNode p' Q)›
    by (meson c_set_game_defender_node.elims(2))
  thus ‹c_set_game_moves n0
    (strategy_from_mimicking_of_C (mimicking (set_lifted C)) (n0 # play))›
  proof(rule disjE)
    assume ‹∃a p' Q. n0 = DefenderSimNode a p' Q›
    then obtain a p' Q where n0_def: ‹n0 = DefenderSimNode a p' Q› by auto
    then obtain p where p_def: ‹hd play = AttackerNode p Q›
      using A
      by (metis csg_atknodes_precede_defnodes_in_plays simulation_challenge strategy0_plays_subset)
    hence ‹c_set_game_moves (AttackerNode p Q) (DefenderSimNode a p' Q)›
      by (metis A n0_def csg_atknodes_precede_defnodes_in_plays strategy0_plays_subset)
    hence ‹p =⊳a p'› ‹¬ tau a› by auto
    hence ‹mimicking (set_lifted C) p Q›
      using c_set_game_strategy_retains_mimicking[OF assms] A p_def
        assms(2) csg_second_play_elem_in_play_set strategy0_plays_subset
      by fastforce
    hence  ‹mimicking (set_lifted C) p' (dsuccs a Q)›
      using mimicking_of_C_guarantees_action_succ ‹¬ tau a› ‹p =⊳a p'› assms(1) tau_tau
      by blast 
    hence Q1_ex: ‹∃Q'. Q' = dsuccs a Q ∧ mimicking (set_lifted C) p' Q'› by auto
    from n0_def have strat_succ:
      ‹strategy_from_mimicking_of_C (mimicking (set_lifted C)) (n0#play)
      = (AttackerNode p'
          (SOME Q1 . Q1 = dsuccs a Q ∧ (mimicking (set_lifted C)) p' Q1))›
      by auto
    then obtain Q1 where 
      ‹AttackerNode p' (SOME Q1 . Q1 = dsuccs a Q ∧ (mimicking (set_lifted C)) p' Q1)
        = AttackerNode p' Q1›
      by blast
    hence Q1_def: ‹Q1 = (SOME Q1 . Q1 = dsuccs a Q ∧ (mimicking (set_lifted C)) p' Q1)›
      by auto
    have next_is_atk:
      ‹strategy_from_mimicking_of_C (mimicking (set_lifted C)) (n0#play)
      = (AttackerNode p' Q1)› 
      using strat_succ Q1_def by auto
    with someI_ex[OF Q1_ex] Q1_def
      have mov_cond: ‹Q1 = dsuccs a Q ∧ mimicking (set_lifted C) p' Q1›
      by blast
    have ‹c_set_game_moves n0 (AttackerNode p' Q1)› using n0_def mov_cond by auto
    thus ?thesis using next_is_atk by auto
  next 
    assume ‹∃p' Q. n0 = DefenderSwapNode p' Q›
    then obtain p' Q where n0_def: ‹n0 = DefenderSwapNode p' Q› by auto
    then obtain p where  p_def: ‹hd play = AttackerNode p Q› using A
      by (metis csg_atknodes_precede_defnodes_in_plays swap_challenge strategy0_plays_subset) 
    hence ‹c_set_game_moves (AttackerNode p Q) (DefenderSwapNode p' Q)›
      by (metis A n0_def csg_atknodes_precede_defnodes_in_plays strategy0_plays_subset)
    hence ‹p ⇒^τ p'› by auto
    hence ‹mimicking (set_lifted C) p Q›
      using c_set_game_strategy_retains_mimicking[OF assms] A p_def
        csg_second_play_elem_in_play_set strategy0_plays_subset 
      by fastforce 
    hence  ‹∃q'. q' ∈ weak_tau_succs Q ∧ mimicking (set_lifted C) q' {p'}›
      using mimicking_of_C_guarantees_tau_succ ‹p ⇒^τ p'› assms(1) by auto 
    hence q1_ex: ‹∃q1. (∃q.(q ∈ Q ∧ q  ⇒^τ q1)) ∧ mimicking (set_lifted C) q1 {p'}›
      using weak_tau_succs_def by auto
    hence strat: ‹strategy_from_mimicking_of_C (mimicking (set_lifted C)) (n0#play)
      = AttackerNode (SOME q1.
        (∃q. (q ∈ Q ∧ q  ⇒^τ q1)) ∧ (mimicking (set_lifted C)) q1 {p'}) {p'}›
      using n0_def by auto
    then obtain q1 where 
      ‹AttackerNode (SOME q1.
        (∃q. (q ∈ Q ∧ q  ⇒^τ q1)) ∧ (mimicking (set_lifted C)) q1 {p'}) {p'}
      = AttackerNode q1 {p'}› by blast
    hence q1_def:
      ‹q1 = (SOME q1 . (∃q. (q ∈ Q ∧ q  ⇒^τ q1)) ∧ (mimicking (set_lifted C)) q1 {p'})›
      by auto
    with someI_ex[OF q1_ex] have
      ‹∃q. (q ∈ Q ∧ q  ⇒^τ q1) ∧ mimicking (set_lifted C) q1 {p'}› 
      by blast
    hence ‹q1 ∈ weak_tau_succs Q ∧ {p'} = {p'}›
      using weak_tau_succs_def by auto
    thus ?thesis  using n0_def strat q1_def by auto
  qed
qed

subsection ‹Winning Strategy Implies Contrasimulation in Set Game (Soundness)›

lemma csg_move_defsimnode_to_atknode:
  assumes 
    ‹c_set_game_moves (DefenderSimNode a p Q) n0›
  shows
    ‹n0 = AttackerNode p (dsuccs a Q)›
proof - 
  have ‹∃p1 Q1. n0 = AttackerNode p1 Q1›
    by (metis assms c_set_game_defender_node.elims(2, 3) c_set_game_moves_no_step(1, 6))
  then obtain p1 Q1 where n0_def: ‹n0 = AttackerNode p1 Q1› by auto
  hence ‹p = p1› using assms local.simulation_answer by blast 
  from n0_def have ‹Q1 = dsuccs a Q› 
    using assms local.simulation_answer by blast
  thus ?thesis using ‹p = p1› n0_def by auto
qed

lemma csg_move_defswapnode_to_atknode:
  assumes 
    ‹c_set_game_moves (DefenderSwapNode p' Q) n0›
  shows
    ‹∃q'. n0 = AttackerNode q' {p'} ∧ q' ∈ weak_tau_succs Q›
proof - 
  have ‹¬c_set_game_defender_node n0› 
    using assms c_set_game_moves_no_step(3, 4) c_set_game_defender_node.elims(2)
    by metis
  hence ‹∃q1 P1. n0 = AttackerNode q1 P1›
    by (meson c_set_game_defender_node.elims(3))
  then obtain q1 P1 where n0_def: ‹n0 = AttackerNode q1 P1› by auto
  hence ‹P1 = {p'}› using assms local.swap_answer by blast 
  from n0_def have ‹q1 ∈  weak_tau_succs Q› using assms by auto
  thus ?thesis using  ‹P1 = {p'}› n0_def by simp
qed

lemma csg_defsimnode_never_stuck: 
  assumes ‹n0 = DefenderSimNode a p Q›
  shows ‹∃Q'. c_set_game_moves n0 (AttackerNode p Q')›
proof -
  have ‹c_set_game_moves (DefenderSimNode a p Q) (AttackerNode p (dsuccs a Q))› by auto
  thus ?thesis using assms by auto
qed

lemma csg_defender_can_simulate_prefix: 
  assumes 
    ‹A ≠ []›
    ‹p ⇒$A p1› 
    ‹∀a∈set A. a ≠ τ›
    ‹sound_0strategy f (AttackerNode p00 {q00})›
    ‹play ∈ plays_for_0strategy f (AttackerNode p00 {q00})›
    ‹hd play = AttackerNode p {q}›
  shows
    ‹∃play p0.
      ((DefenderSimNode (last A) p0 (dsuccs_seq_rec (rev (butlast A)) {q}))#play)
        ∈ plays_for_0strategy f (AttackerNode p00 {q00})
      ∧ word_reachable_via_delay A p p0 p1›
  using assms(1-3)
proof (induct arbitrary: p1 rule: rev_nonempty_induct[OF assms(1)])
  case single: (1 a)
  hence ‹¬tau a› using ‹∀a∈set A. a ≠ τ› by (simp add: tau_def) 
  hence ‹p ⇒$[a] p1› using single by auto
  hence p_step: ‹p ⇒^a p1› by blast
  then obtain p0 where ‹p =⊳a p0› ‹p0 ⇒^τ p1› using Cons ‹¬tau a› steps.refl by auto
  hence ‹∃n0. n0  = DefenderSimNode a p0 {q} ∧ c_set_game_moves (AttackerNode p {q}) n0›
    using assms(4) ‹¬ tau a› by simp
  hence ‹(DefenderSimNode a p0 {q})#play ∈ plays_for_0strategy f (AttackerNode p00 {q00})›
    using assms(5,6)
    by (metis c_set_game_defender_node.simps(1) list.collapse no_empty_plays 
          plays_for_0strategy.p1move strategy0_plays_subset)
  hence inplay:
    ‹(DefenderSimNode (last [a]) p0 (dsuccs_seq_rec (rev (butlast [a])) {q}))#play
      ∈ plays_for_0strategy f (AttackerNode p00 {q00})›
    by auto
  have ‹p  ⇒$(butlast [a]) p› by (simp add: steps.refl) 
  hence ‹word_reachable_via_delay [a] p p0 p1›
    using word_reachable_via_delay_def ‹p =⊳a p0› ‹p0 ⇒^τ p1› by auto
  then show ?case using inplay by auto
next
  case snoc: (2 a as)
  hence ‹¬tau a› using ‹∀a∈set A. a ≠ τ› by (simp add: tau_def) 
  then obtain a2 as2 where as_def: ‹as = as2@[a2]›
    using list_rev_split[OF snoc.hyps(1)] by auto
  have ‹∃p'. p ⇒$ as  p' ∧ p' ⇒$[a]  p1›
    using rev_seq_split[OF snoc.prems(2)] by blast
  hence ‹∃p'. p ⇒$ as  p' ∧ p' ⇒^a  p1› by blast
  hence ‹∃p'. p ⇒$ as  p' ∧ p' ⇒a  p1› using  ‹¬tau a› by simp
  then obtain p' where p'_def: ‹p ⇒$ as  p'› and p'_step: ‹p' ⇒a  p1› by auto
  then obtain p11 where  ‹p' =⊳a  p11› ‹p11 ⇒^τ p1›
    using steps.refl ‹¬ tau a› tau_tau by blast
  hence ‹∃play p0.
    DefenderSimNode (last as) p0 (dsuccs_seq_rec (rev (butlast as)) {q}) # play
      ∈ plays_for_0strategy f (AttackerNode p00 {q00})
    ∧ word_reachable_via_delay as p p0 p'›
    using p'_def snoc by auto
  then obtain play p0
    where play_def:
      ‹DefenderSimNode (last as) p0 (dsuccs_seq_rec (rev (butlast as)) {q}) # play
        ∈ plays_for_0strategy f (AttackerNode p00 {q00})›
      ‹word_reachable_via_delay as p p0 p'›
    by auto
  hence
    ‹DefenderSimNode a2 p0 (dsuccs_seq_rec (rev as2) {q}) # play
      ∈ plays_for_0strategy f (AttackerNode p00 {q00})›
    using as_def by auto
  then obtain n0 where
    n0_def: ‹n0 = DefenderSimNode a2 p0 (dsuccs_seq_rec (rev as2) {q})› and
    n0_in_play: ‹n0#play ∈ plays_for_0strategy f (AttackerNode p00 {q00})›
    by auto
  then obtain n1 where
    n1_def: ‹c_set_game_moves (DefenderSimNode a2 p0 (dsuccs_seq_rec (rev as2) {q})) n1›
    using csg_defsimnode_never_stuck by meson
  hence n1_atk: ‹n1 = AttackerNode p0 (dsuccs a2 ((dsuccs_seq_rec (rev as2) {q})))›
    using csg_move_defsimnode_to_atknode[OF n1_def] by auto
  have n1_in_play: ‹n1#n0#play ∈ plays_for_0strategy f (AttackerNode p00 {q00})›
    using n1_def n0_in_play n0_def
    by (metis assms(4) csg_move_defsimnode_to_atknode c_set_game_defender_node.simps(2)
        plays_for_0strategy.simps sound_0strategy_def)
  then obtain n0' where
    n0'_def:
      ‹n0' = DefenderSimNode a p11 (dsuccs a2 ((dsuccs_seq_rec (rev as2) {q})))› and
    n0'_mov: ‹c_set_game_moves n1 n0'›
    using p'_step n1_atk
    by (metis (no_types, lifting) ‹¬ tau a› ‹p' =⊳ a p11› word_reachable_via_delay_def
        simulation_challenge play_def(2) steps_concat tau_tau)
  hence in_play: ‹n0'#n1#n0#play ∈ plays_for_0strategy f (AttackerNode p00 {q00})›
    using n1_in_play
    by (simp add: n1_atk plays_for_0strategy.p1move) 
  hence ‹n0' = DefenderSimNode a p11 (dsuccs_seq_rec (rev (as2@[a2])) {q})›
    using n0'_def  by auto
  hence n0'_is_defSimNode: ‹n0' = DefenderSimNode a p11 (dsuccs_seq_rec (rev (as)) {q})›
    using as_def by auto
  from ‹p ⇒$ as  p'› ‹p' =⊳a  p11› ‹p11 ⇒^τ p1›
    have ‹word_reachable_via_delay (as@[a]) p p11 p1› 
    using word_reachable_via_delay_def by auto
  then show ?case using n0'_is_defSimNode in_play by auto
qed

lemma contrasim_set_game_sound: 
  assumes
    ‹player0_winning_strategy f (AttackerNode p00 {q00})›
    ‹sound_0strategy f (AttackerNode p00 {q00})›
  defines
    ‹C == λ p q . (∃ play ∈ plays_for_0strategy f (AttackerNode p00 {q00}) .
      hd play = AttackerNode p {q} ∧ (hd play = (AttackerNode p00 {q00})
      ∨ (∃P. hd (tl play) = DefenderSwapNode q P)))›
  shows
    ‹contrasimulation C›
  unfolding contrasimulation_def
proof (safe) 
  fix p q p1 A
  assume ‹∀a∈set A. a ≠ τ› ‹p ⇒$A p1› ‹C p q›
  hence ‹p ⇒$(taufree A) p1› by (simp add: weak_step_over_tau) 
  hence ‹∃ play ∈ plays_for_0strategy f (AttackerNode p00 {q00}).
      hd play = AttackerNode p {q}
      ∧ (hd play = (AttackerNode p00 {q00})
      ∨ (∃P. hd (tl play) = DefenderSwapNode q P))›
    using C_def ‹p ⇒$A p1› ‹C p q› by auto
  from this obtain play where
    play_def: ‹play ∈ plays_for_0strategy f (AttackerNode p00 {q00})› and
    play_hd: ‹hd play = AttackerNode p {q}› and
    ‹hd play = (AttackerNode p00 {q00}) ∨ (∃P. hd (tl play) = DefenderSwapNode q P)› 
    by auto
  hence ‹¬player1_wins_immediately play›
    using assms(1) player0_winning_strategy_def by auto
  hence ‹(c_set_game_defender_node (hd play) ∧
    (∄p'. c_set_game_moves (hd play) p')) ⟹ False› 
    using player1_wins_immediately_def by auto
  hence Def_not_stuck:
    ‹c_set_game_defender_node (hd play) ⟹ (∃p'. c_set_game_moves (hd play) p')› by auto
  from ‹p ⇒$A p1› ‹p ⇒$(taufree A) p1› ‹C p q›
    show ‹∃q'. q ⇒$ A q' ∧ C q' p1›
  proof (cases A rule: rev_cases)
    case Nil
    hence ‹p ⇒^τ p1› using ‹p ⇒$A p1› by auto
    hence ‹∃n0. n0 = DefenderSwapNode p1 {q}
      ∧ c_set_game_moves (AttackerNode p {q}) n0› by simp 
    from this obtain n0 where n0_def: ‹n0 = DefenderSwapNode p1 {q}› 
      and n0_move: ‹c_set_game_moves (AttackerNode p {q}) n0› by auto
    have ‹play = (hd play)#(tl play)›
      by (metis hd_Cons_tl no_empty_plays play_def strategy0_plays_subset)
    hence ‹n0#play ∈ plays_for_0strategy f (AttackerNode p00 {q00})›
      using n0_def n0_move play_def play_hd
      by (metis c_set_game_defender_node.simps(1) play_def 
          plays_for_0strategy.p1move) 
    hence ‹∃n1'. c_set_game_moves n0 n1'
        ∧ n1'#n0#play ∈ plays_for_0strategy f (AttackerNode p00 {q00})›
      using assms(2) n0_def sound_0strategy_def
      by (meson c_set_game_defender_node.simps(3) plays_for_0strategy.p0move) 
    then obtain n1' where n1'_mov: ‹c_set_game_moves n0 n1'› 
      and in_play: ‹n1'#n0#play ∈ plays_for_0strategy f (AttackerNode p00 {q00})› by auto
    hence ‹∃q1. n1' = AttackerNode q1 {p1} ∧ (q1 ∈ weak_tau_succs {q})›
      by (metis c_set_game_defender_node.elims(2, 3) c_set_game_moves_no_step(3, 4)
          swap_answer n0_def) 
    then obtain q1 where q1_def: ‹n1' = AttackerNode q1 {p1}› 
      and q_succ: ‹q1 ∈ weak_tau_succs {q}› by auto
    hence q_tau: ‹q ⇒^τ q1› using weak_tau_succs_def by auto
    from in_play q1_def n0_def have ‹C q1 p1› unfolding C_def by force 
    then show ?thesis using q_tau Nil by auto 
  next
    case (snoc as a)
    hence ‹A ≠ []› by auto
    hence ‹¬tau a› using ‹∀a∈set A. a ≠ τ› snoc  by (simp add: tau_def) 
    then obtain A_play p0 where gotoA:
      ‹DefenderSimNode (last A) p0 (dsuccs_seq_rec (rev (butlast A)) {q}) # A_play
        ∈ plays_for_0strategy f (AttackerNode p00 {q00})›
      ‹word_reachable_via_delay A p p0 p1› 
      using csg_defender_can_simulate_prefix ‹p ⇒$A p1› 
        ‹∀a∈set A. a ≠ τ› ‹A ≠ []› assms(2) play_def play_hd by meson
    then obtain Q where ‹Q = dsuccs_seq_rec (rev (butlast A)) {q}› by auto
    hence ‹∀q' ∈ Q.  q ⇒$(butlast A) q'›
      using in_dsuccs_implies_word_reachable by auto
    then obtain n0 where
      n0_def: ‹n0 = DefenderSimNode a p0 (dsuccs_seq_rec (rev as) {q})›
      by auto
    hence A_play_def: ‹n0#A_play ∈ plays_for_0strategy f (AttackerNode p00 {q00})›
      using gotoA snoc by auto
    then obtain n1 where n1_move: ‹c_set_game_moves n0 n1›
      using n0_def
      by (meson assms(2) c_set_game_defender_node.simps(2) sound_0strategy_def)
    hence ‹n1 = AttackerNode p0 (dsuccs a (dsuccs_seq_rec (rev as) {q}))› 
      using csg_move_defsimnode_to_atknode n0_def by blast
    hence ‹n1 = AttackerNode p0 (dsuccs_seq_rec (a#(rev as)) {q})›  
      using dsuccs_seq_rec.simps(2) by auto
    hence ‹n1 = AttackerNode p0 (dsuccs_seq_rec (rev (as@[a])) {q})› by auto
    hence n1_def: ‹n1 = AttackerNode p0 (dsuccs_seq_rec (rev A) {q})›
      using snoc by auto
    hence n1_in_play: ‹n1#n0#A_play ∈ plays_for_0strategy f (AttackerNode p00 {q00})›
      using n0_def A_play_def n1_move assms(2) csg_move_defsimnode_to_atknode
        plays_for_0strategy.p0move sound_0strategy_def
      by fastforce
    from ‹word_reachable_via_delay A p p0 p1› have ‹p0 ⇒^τ p1›
      using word_reachable_via_delay_def by auto
    then obtain n0' where n0'_move: ‹c_set_game_moves n1 n0'›
      and n0'_def: ‹n0' = DefenderSwapNode p1 (dsuccs_seq_rec (rev A) {q})›
      using  swap_challenge tau_tau n1_def by blast
    hence n0'_in_play:
      ‹n0'#n1#n0#A_play ∈ plays_for_0strategy f (AttackerNode p00 {q00})›
      using n1_in_play by (simp add: n1_def plays_for_0strategy.p1move) 
    then obtain n1' where n1'_move: ‹c_set_game_moves n0' n1'›
      and in_strat: ‹n1' = f(n0'#n1#n0#A_play)› 
      using Def_not_stuck n0'_def assms(2) sound_0strategy_def by auto
    then obtain q1 where q1_def: ‹q1 ∈ weak_tau_succs (dsuccs_seq_rec (rev A) {q})› 
      and n1'_def: ‹n1'  = AttackerNode q1 {p1}› using n0'_def swap_answer
      by (metis c_set_game_defender_node.cases c_set_game_moves_no_step(3, 7)) 
    hence ‹q1 ∈ {q1. ∃q0 ∈ (dsuccs_seq_rec (rev A) {q}). q0 ⇒^τ q1}› 
      using weak_tau_succs_def by auto
    also have ‹... = {q1. ∃q0 ∈ (dsuccs_seq_rec (rev A) {q}). q ⇒$A q0 ∧ q0 ⇒^τ q1}›
      using in_dsuccs_implies_word_reachable by auto
    also have ‹... ⊆ {q1. ∃q0 ∈ (dsuccs_seq_rec (rev A) {q}). q ⇒$A q1}› 
      using word_tau_concat by auto
    also have ‹... ⊆ {q1. q ⇒$A q1}› by auto
    finally have ‹q1 ∈ {q1. q ⇒$A q1}› .
    hence q_goal: ‹q ⇒$A q1› by auto
    from n1'_move in_strat have
      move_f: ‹c_set_game_moves n0' (f(n0'#n1#n0#A_play))› by auto
    hence ‹n1'#n0'#n1#n0#A_play ∈ plays_for_0strategy f (AttackerNode p00 {q00})›
      using in_strat plays_for_0strategy.p0move[OF n0'_in_play _ move_f] n0'_def by auto
    hence ‹C q1 p1› unfolding C_def using n1'_def n0'_def by force
    thus ?thesis using q_goal by auto
  qed
qed

theorem winning_strategy_in_c_set_game_iff_contrasim:
  shows
    ‹(∃ f . player0_winning_strategy f (AttackerNode p0 {q0})
      ∧ sound_0strategy f (AttackerNode p0 {q0}))
    = p0 ⊑c q0›
proof safe
  fix f
  assume
    ‹player0_winning_strategy f (AttackerNode p0 {q0})›
    ‹sound_0strategy f (AttackerNode p0 {q0})›
  hence ‹contrasimulation (λp q. ∃play ∈ plays_for_0strategy f (AttackerNode p0 {q0}).
    hd play = AttackerNode p {q} ∧
    (hd play = (AttackerNode p0 {q0}) ∨ (∃P. hd (tl play) = DefenderSwapNode q P)))›
    using contrasim_set_game_sound by blast
  thus ‹p0 ⊑c q0›
    using plays_for_0strategy.init[of ‹AttackerNode p0 {q0}› f] list.sel(1) by force
next
  fix C
  assume ‹contrasimulation C› ‹C p0 q0›
  thus
    ‹(∃f. player0_winning_strategy f (AttackerNode p0 {q0})
      ∧ sound_0strategy f (AttackerNode p0 {q0}))›
    using contrasim_set_game_complete[OF _ _]
      csg_strategy_from_mimicking_of_C_sound[OF _ _]
    by blast
qed

end
end