Theory Coupledsim_Game_Delay

section ‹Game for Coupled Similarity with Delay Formulation›

theory Coupledsim_Game_Delay
imports
  Coupled_Simulation
  Simple_Game
begin

subsection ‹The Coupled Simulation Preorder Game Using Delay Steps›

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

fun (in lts_tau) cs_game_moves ::
  ‹('s, 'a) cs_game_node ⇒ ('s, 'a) cs_game_node ⇒ bool› where
  simulation_visible_challenge:
    ‹cs_game_moves (AttackerNode p q) (DefenderStepNode a p1 q0) =
      (¬tau a ∧ p ⟼a p1 ∧ q = q0)› |
  simulation_internal_attacker_move:
    ‹cs_game_moves (AttackerNode p q) (AttackerNode p1 q0) =
      (∃a. tau a ∧ p ⟼a p1 ∧ q = q0)› |
  simulation_answer:
    ‹cs_game_moves (DefenderStepNode a p1 q0) (AttackerNode p11 q1) =    
      (q0 =⊳a q1 ∧ p1 = p11)› |
  coupling_challenge:
    ‹cs_game_moves (AttackerNode p q) (DefenderCouplingNode p0 q0) =
      (p = p0 ∧ q = q0)› |
  coupling_answer:
    ‹cs_game_moves (DefenderCouplingNode p0 q0) (AttackerNode q1 p00) =
      (p0 = p00 ∧ q0 ⟼* tau q1)› |
  cs_game_moves_no_step:
    ‹cs_game_moves _ _ = False›

fun cs_game_defender_node :: ‹('s, 'a) cs_game_node ⇒ bool› where
  ‹cs_game_defender_node (AttackerNode _ _) = False› |
  ‹cs_game_defender_node (DefenderStepNode _ _ _) = True› |
  ‹cs_game_defender_node (DefenderCouplingNode _ _) = True›

locale cs_game =
  lts_tau trans τ +
  simple_game cs_game_moves cs_game_defender_node
for
  trans :: ‹'s ⇒ 'a ⇒ 's ⇒ bool› ("_ ⟼_  _" [70, 70, 70] 80) and
  τ :: ‹'a›
begin

subsection ‹Coupled Simulation Implies Winning Strategy›

fun strategy_from_coupleddsim :: ‹('s ⇒ 's ⇒ bool) ⇒ ('s, 'a) cs_game_node strategy› where
  ‹strategy_from_coupleddsim R ((DefenderStepNode a p1 q0)#play) =
    (AttackerNode p1 (SOME q1 . R p1 q1 ∧ q0 =⊳a q1))› |
  ‹strategy_from_coupleddsim R ((DefenderCouplingNode p0 q0)#play) =
    (AttackerNode (SOME q1 . R q1 p0 ∧ q0 ⟼* tau q1) p0)› |
  ‹strategy_from_coupleddsim _ _ = undefined›

lemma defender_preceded_by_attacker:
  assumes
    ‹n0 # play ∈ plays (AttackerNode p0 q0)›
    ‹cs_game_defender_node n0›
  shows
    ‹∃ p q . hd play = AttackerNode p q ∧ cs_game_moves (AttackerNode p q) n0›
    ‹play ≠ []›
proof -
  have n0_not_init: ‹n0 ≠ (AttackerNode p0 q0)› using assms(2) by auto
  hence ‹cs_game_moves (hd play) n0› using assms(1)
    by (metis list.sel(1) list.sel(3) plays.cases)
  thus ‹∃p q. hd play = AttackerNode p q ∧ cs_game_moves (AttackerNode p q) n0› using assms(2)
    by (metis cs_game_defender_node.elims(2,3) local.cs_game_moves_no_step(1,2,3,6))
  show ‹play ≠ []› using n0_not_init assms(1) plays.cases by auto
qed

lemma defender_only_challenged_by_visible_actions:
  assumes
    ‹(DefenderStepNode a p q) # play ∈ plays (AttackerNode p0 q0)›
  shows
    ‹¬tau a›
  using assms defender_preceded_by_attacker
  by fastforce

lemma strategy_from_coupleddsim_retains_coupledsim:
  assumes
    ‹R p0 q0›
    ‹coupled_delay_simulation R›
    ‹initial = AttackerNode p0 q0›
    ‹play ∈ plays_for_0strategy (strategy_from_coupleddsim R) initial›
  shows
    ‹hd play = AttackerNode p q ⟹ R p q›
    ‹length play > 1 ⟹ hd (tl play) = AttackerNode p q ⟹ R p q›
  using assms(4)
proof (induct arbitrary: p q rule: plays_for_0strategy.induct[OF assms(4)])
  case 1
  fix p q
  assume ‹hd [initial] = AttackerNode p q›
  hence ‹p = p0› ‹q = q0› using assms(3) by auto
  thus ‹R p q› using assms(1) by simp
next
  case 1
  fix p q
  assume ‹1 < length [initial]›
  hence False by auto
  thus ‹R p q›  ..
next
  case (2 n0 play)
  hence n0play_is_play: ‹n0 # play ∈ plays initial› using strategy0_plays_subset by blast
  fix p q
  assume subassms:
    ‹hd (strategy_from_coupleddsim R (n0 # play) # n0 # play) = AttackerNode p q›
    ‹strategy_from_coupleddsim R (n0 # play) # n0 # play
      ∈ plays_for_0strategy (strategy_from_coupleddsim R) initial›
  then obtain pi qi where 
      piqi_def: ‹hd (play) = AttackerNode pi qi›
        ‹cs_game_moves (AttackerNode pi qi) n0› ‹play ≠ []›
    using defender_preceded_by_attacker n0play_is_play `cs_game_defender_node n0` assms(3) by blast
  hence ‹R pi qi› using 2(1,3) by simp
  have ‹(∃ a . n0 = (DefenderStepNode a p qi) ∧ ¬ tau a ∧ pi ⟼a p)
    ∨ (n0 = (DefenderCouplingNode pi qi))›
    using piqi_def(2) 2(4,5) subassms(1)
    using cs_game_defender_node.elims(2) cs_game_moves.simps(1,3)
      cs_game_moves.simps(4) list.sel(1)
    by metis
  thus ‹R p q›
  proof safe
    fix a
    assume n0_def: ‹n0 = DefenderStepNode a p qi› ‹¬ tau a› ‹pi ⟼a p›
    have ‹strategy_from_coupleddsim R (n0 # play) =
        (AttackerNode p (SOME q1 . R p q1 ∧ qi =⊳a q1))›
      unfolding n0_def(1) by auto
    with subassms(1) have q_def: ‹q = (SOME q1. R p q1 ∧ qi =⊳a  q1)› by auto
    have ‹∃ qii . R p qii ∧ qi =⊳a qii›
      using n0_def(2,3) `R pi qi` `coupled_delay_simulation R`
      unfolding coupled_delay_simulation_def delay_simulation_def by blast
    from someI_ex[OF this] show ‹R p q› unfolding q_def by blast
  next
    assume n0_def: ‹n0 = DefenderCouplingNode pi qi›
    have ‹strategy_from_coupleddsim R (n0 # play) =
        (AttackerNode (SOME q1 . R q1 pi ∧ qi ⟼* tau q1) pi)›
      unfolding n0_def(1) by auto
    with subassms(1) have qp_def:
      ‹p = (SOME q1 . R q1 pi ∧ qi ⟼* tau q1)› ‹q = pi› by auto
    have ‹∃ q1 . R q1 pi ∧ qi ⟼* tau q1›
      using n0_def `R pi qi` `coupled_delay_simulation R`
      unfolding coupled_delay_simulation_def by blast
    from someI_ex[OF this] show ‹R p q› unfolding qp_def by blast
  qed
next
  case (2 n0 play)
  fix p q
  assume ‹hd (tl (strategy_from_coupleddsim R (n0 # play) # n0 # play)) = AttackerNode p q›
  hence False using 2(4) by auto
  thus ‹R p q› ..
next
  case (3 n1 play n1')
  fix p q
  assume ‹hd (n1' # n1 # play) = AttackerNode p q›
  then obtain p1 a where n1_spec: ‹n1 = AttackerNode p1 q› ‹p1 ⟼a p› ‹tau a›
   using 3 list.sel(1) 
   by (metis cs_game_defender_node.elims(3) simulation_internal_attacker_move)
  then have ‹R p1 q› using 3 by auto
  thus ‹R p q› 
    using  n1_spec(2,3) ‹coupled_delay_simulation R›
    unfolding coupled_delay_simulation_def delay_simulation_def by auto
next
  case (3 n1 play n1')
  fix p q
  assume ‹hd (tl (n1' # n1 # play)) = AttackerNode p q›
  thus ‹R p q› using 3(1,2) by auto
qed

lemma strategy_from_coupleddsim_sound:
  assumes
    ‹R p0 q0›
    ‹coupled_delay_simulation R›
    ‹initial = AttackerNode p0 q0›
  shows
    ‹sound_0strategy (strategy_from_coupleddsim R) initial›
  unfolding sound_0strategy_def
proof clarify
  fix n0 play
  assume subassms:
    ‹n0 # play ∈ plays_for_0strategy(strategy_from_coupleddsim R) initial›
    ‹cs_game_defender_node n0›
  then obtain pi qi where
      piqi_def: ‹hd (play) = AttackerNode pi qi›
        ‹cs_game_moves (AttackerNode pi qi) n0› ‹play ≠ []›
    using defender_preceded_by_attacker `cs_game_defender_node n0` assms(3)
      strategy0_plays_subset by blast
  hence ‹R pi qi›
    using strategy_from_coupleddsim_retains_coupledsim[OF assms] list.sel subassms by auto
  have ‹(∃ a p . n0 = (DefenderStepNode a p qi) ∧ pi ⟼a p)
    ∨ (n0 = (DefenderCouplingNode pi qi))›
    by (metis cs_game_defender_node.elims(2)
        coupling_challenge simulation_visible_challenge piqi_def(2) subassms(2))
  thus ‹cs_game_moves n0 (strategy_from_coupleddsim R (n0 # play))›
  proof safe
    fix a p
    assume dsn:
      ‹pi ⟼a  p›
      ‹n0 = DefenderStepNode a p qi›
    hence qi_spec:
      ‹(strategy_from_coupleddsim R (n0 # play)) =
        AttackerNode p (SOME q1 . R p q1 ∧ qi =⊳a q1)›
      by simp
    then obtain qii where qii_spec:
      ‹AttackerNode p (SOME q1 . R p q1 ∧ qi =⊳a q1) = AttackerNode p qii› by blast
    have ‹∃ qii . R p qii ∧ qi =⊳a qii›
      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 ‹R p qii ∧ qi =⊳a qii› using qii_spec by blast
    thus ‹cs_game_moves (DefenderStepNode a p qi)
          (strategy_from_coupleddsim R (DefenderStepNode a p qi # play))›
      using qi_spec qii_spec unfolding dsn(2) by auto
  next ―‹coupling quite analogous.›
    assume dcn:
      ‹n0 = DefenderCouplingNode pi qi›
    hence qi_spec:
      ‹(strategy_from_coupleddsim R (n0 # play)) =
      AttackerNode (SOME q1 . R q1 pi ∧ qi ⟼* tau q1) pi›
      by simp
    then obtain qii where qii_spec:
      ‹AttackerNode (SOME q1 . R q1 pi ∧ qi ⟼* tau q1) pi = AttackerNode qii pi› by blast
    have ‹∃ qii . R qii pi ∧ qi ⟼* tau qii›
      using dcn `R pi qi` `coupled_delay_simulation R`
      unfolding coupled_delay_simulation_def by blast
    from someI_ex[OF this] have ‹R qii pi ∧ qi ⟼* tau qii› using qii_spec by blast
    thus ‹cs_game_moves (DefenderCouplingNode pi qi)
        (strategy_from_coupleddsim R (DefenderCouplingNode pi qi # play))›
      using qi_spec qii_spec unfolding dcn by auto
  qed
qed

lemma coupleddsim_implies_winning_strategy:
  assumes
    ‹R p q›
    ‹coupled_delay_simulation R›
    ‹initial = AttackerNode p q›
  shows
    ‹player0_winning_strategy (strategy_from_coupleddsim R) initial›
  unfolding player0_winning_strategy_def
proof (clarify)
  fix play
  assume subassms:
    ‹play ∈ plays_for_0strategy (strategy_from_coupleddsim R) initial›
    ‹player1_wins_immediately play›
  show ‹False› using subassms
  proof (induct rule: simple_game.plays_for_0strategy.induct[OF subassms(1)])
    case 1
    then show ?case unfolding player1_wins_immediately_def using assms(3) by auto
  next
    case (2 n0 play)
    hence ‹¬ cs_game_defender_node (strategy_from_coupleddsim R (n0 # play))›
      using cs_game_moves_no_step cs_game_defender_node.elims(2) by metis
    hence ‹¬  player1_wins_immediately (strategy_from_coupleddsim R (n0 # play) # n0 # play)›
      unfolding player1_wins_immediately_def by auto
    thus ?case using 2(6) by auto
  next
    case (3 n1 play n1')
    then obtain p q where n1_def: ‹n1 = AttackerNode p q›
      using cs_game_defender_node.elims(3) by blast
    hence ‹R p q›
      using strategy_from_coupleddsim_retains_coupledsim[OF assms, of ‹n1 # play›] 3(1)
      by auto
    have ‹(∃ p1 a . n1' = (DefenderStepNode a p1 q) ∧ (p ⟼a p1))
        ∨ n1' = (DefenderCouplingNode p q)›
      using n1_def `cs_game_moves n1 n1'` coupling_challenge cs_game_moves_no_step(5)
        simulation_visible_challenge "3.prems"(2) cs_game_defender_node.elims(1) list.sel(1)
      unfolding player1_wins_immediately_def
      by metis
    then show ?case
    proof 
      assume ‹(∃ p1 a . n1' = (DefenderStepNode a p1 q) ∧ (p ⟼a p1))›
      then obtain p1 a where 
        n1'_def: ‹n1' = (DefenderStepNode a p1 q)› ‹p ⟼a p1›
        by blast
      hence ‹∃ q1 . q =⊳a q1› 
        using `R p q` `coupled_delay_simulation R`
        unfolding coupled_delay_simulation_def delay_simulation_def by blast
      hence ‹∃ q1 . cs_game_moves (DefenderStepNode a p1 q) (AttackerNode p1 q1)›
        by auto
      with `player1_wins_immediately (n1' # n1 # play)` show False
        unfolding player1_wins_immediately_def n1'_def
        by (metis list.sel(1))
    next
      assume n1'_def: ‹n1' = DefenderCouplingNode p q›
      have ‹∃ q1 . q ⟼*tau q1› 
        using `coupled_delay_simulation R` `R p q`
        unfolding coupled_delay_simulation_def by blast
      hence ‹∃ q1 . cs_game_moves (DefenderCouplingNode p q) (AttackerNode q1 p)›
        by auto
      with `player1_wins_immediately (n1' # n1 # play)` show False
        unfolding player1_wins_immediately_def n1'_def
        by (metis list.sel(1))
    qed
  qed
qed

subsection ‹Winning Strategy Induces Coupled Simulation›

lemma winning_strategy_implies_coupleddsim:
  assumes
    ‹player0_winning_strategy f initial›
    ‹sound_0strategy f initial›
  defines
    ‹R == λ p q . (∃ play ∈ plays_for_0strategy f initial. hd play = AttackerNode p q)›
  shows
    ‹coupled_delay_simulation R›
  unfolding coupled_delay_simulation_def delay_simulation_def
proof safe
  fix p q p' a
  assume challenge:
    ‹R p q›
    ‹p ⟼a  p'›
    ‹tau a ›
  hence game_move: ‹cs_game_moves (AttackerNode p q) (AttackerNode p' q)› by auto
  have ‹(∃ play ∈ plays_for_0strategy f initial. hd play = AttackerNode p q)›
    using challenge(1) assms by blast
  then obtain play where
      play_spec: ‹AttackerNode p q # play ∈ plays_for_0strategy f initial›
    by (metis list.sel(1) simple_game.plays.cases strategy0_plays_subset)
  hence interplay:
      ‹(AttackerNode p' q) # AttackerNode p q # play ∈ plays_for_0strategy f initial›
    using game_move by (simp add: simple_game.plays_for_0strategy.p1move)
  then show ‹R p' q›
    unfolding R_def list.sel by force
next
  fix p q p' a
  assume challenge:
    ‹R p q›
    ‹p ⟼a  p'›
    ‹¬ tau a ›
  hence game_move: ‹cs_game_moves (AttackerNode p q) (DefenderStepNode a p' q)› by auto
  have ‹(∃ play ∈ plays_for_0strategy f initial. hd play = AttackerNode p q)›
    using challenge(1) assms by blast
  then obtain play where
      play_spec: ‹AttackerNode p q # play ∈ plays_for_0strategy f initial›
    by (metis list.sel(1) simple_game.plays.cases strategy0_plays_subset)
  hence interplay:
      ‹(DefenderStepNode a p' q) # AttackerNode p q # play ∈ plays_for_0strategy f initial›
    using game_move by (simp add: simple_game.plays_for_0strategy.p1move)
  hence ‹¬ player1_wins_immediately ((DefenderStepNode a p' q) # AttackerNode p q # play)›
    using assms(1) unfolding player0_winning_strategy_def by blast
  then obtain n1 where n1_def:
      ‹n1 = f (DefenderStepNode a p' q # AttackerNode p q # play)›
      ‹cs_game_moves (DefenderStepNode a p' q) n1›
    using interplay assms(2) unfolding player0_winning_strategy_def sound_0strategy_def by simp
  obtain q' where q'_spec:
      ‹(AttackerNode p' q') = n1› ‹q =⊳a q'›
    using n1_def(2) by (cases n1, auto)
  hence ‹(AttackerNode p' q') # (DefenderStepNode a p' q) # AttackerNode p q # play
      ∈ plays_for_0strategy f initial›
    using interplay n1_def by (simp add: simple_game.plays_for_0strategy.p0move)
  hence ‹R p' q'› unfolding R_def by (meson list.sel(1))
  thus ‹∃q'. R p' q' ∧ q =⊳a  q'› using q'_spec(2) by blast
next
  fix p q 
  assume challenge:
    ‹R p q›
  hence game_move: ‹cs_game_moves (AttackerNode p q) (DefenderCouplingNode p q)› by auto
  have ‹(∃ play ∈ plays_for_0strategy f initial . hd play = AttackerNode p q)›
    using challenge assms by blast
  then obtain play where
      play_spec: ‹AttackerNode p q # play ∈ plays_for_0strategy f initial›
    by (metis list.sel(1) simple_game.plays.cases strategy0_plays_subset)
  hence interplay: ‹(DefenderCouplingNode p q) # AttackerNode p q # play
      ∈ plays_for_0strategy f initial›
    using game_move by (simp add: simple_game.plays_for_0strategy.p1move)
  hence ‹¬ player1_wins_immediately ((DefenderCouplingNode p q) # AttackerNode p q # play)›
    using assms(1) unfolding player0_winning_strategy_def by blast
  then obtain n1 where n1_def:
      ‹n1 = f (DefenderCouplingNode p q # AttackerNode p q # play)›
      ‹cs_game_moves (DefenderCouplingNode p q) n1›
    using interplay assms(2)
    unfolding player0_winning_strategy_def sound_0strategy_def by simp
  obtain q' where q'_spec:
      ‹(AttackerNode q' p) = n1› ‹q ⟼* tau q'›
    using n1_def(2) by (cases n1, auto)
  hence ‹(AttackerNode q' p) # (DefenderCouplingNode p q) # AttackerNode p q # play
      ∈ plays_for_0strategy f initial›
    using interplay n1_def by (simp add: simple_game.plays_for_0strategy.p0move)
  hence ‹R q' p› unfolding R_def by (meson list.sel(1))
  thus ‹∃q'. q ⟼* tau  q' ∧ R q' p› using q'_spec(2) by blast
qed

theorem winning_strategy_iff_coupledsim:
  assumes
    ‹initial = AttackerNode p q›
  shows 
    ‹(∃ f . player0_winning_strategy f initial ∧ sound_0strategy f initial)
    = p ⊑cs q›
proof (rule)
  assume
    ‹(∃f. player0_winning_strategy f initial ∧ sound_0strategy f initial)›
  then obtain f where
    ‹coupled_delay_simulation (λp q. ∃play∈plays_for_0strategy f initial. hd play = AttackerNode p q)›
    using winning_strategy_implies_coupleddsim by blast
  moreover have ‹(λp q. ∃play∈plays_for_0strategy f initial. hd play = AttackerNode p q) p q›
    using assms plays_for_0strategy.init by force
  ultimately show ‹p ⊑cs q›
    unfolding coupled_sim_by_eq_coupled_delay_simulation
    by (metis (mono_tags, lifting))
next
  assume
    ‹p ⊑cs  q›
  thus ‹(∃f. player0_winning_strategy f initial ∧ sound_0strategy f initial)›
    unfolding coupled_sim_by_eq_coupled_delay_simulation
    using coupleddsim_implies_winning_strategy[OF _ _ assms]
          strategy_from_coupleddsim_sound[OF _ _ assms] by blast
qed

end
end