Theory Contrasim_Word_Game

section ‹The Contrasimulation Preorder Word Game›

theory Contrasim_Word_Game
imports
  Simple_Game
  Contrasimulation
begin

datatype ('s, 'a) c_word_game_node =
  AttackerNode 's 's |
  DefenderNode "'a list" 's 's

fun (in lts_tau) c_word_game_moves ::
  ‹('s, 'a) c_word_game_node ⇒ ('s, 'a) c_word_game_node ⇒ bool› where
                             
  simulation_challenge:
   ‹c_word_game_moves (AttackerNode p q) (DefenderNode A p1 q0) =
     (p ⇒$A p1 ∧ q = q0 ∧ (∀a∈set A. a ≠ τ))› |     

  simulation_answer:                        
    ‹c_word_game_moves (DefenderNode A p1 q0) (AttackerNode q1 p10) =
      (q0 ⇒$A q1 ∧ p1 = p10)› |                                             
                                             
  c_word_game_moves_no_step:               
    ‹c_word_game_moves _ _ = False›

fun c_word_game_defender_node :: ‹('s, 'a) c_word_game_node ⇒ bool› where
  ‹c_word_game_defender_node (AttackerNode _ _) = False› |
  ‹c_word_game_defender_node (DefenderNode _ _ _) = True›


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

locale c_word_game =
  lts_tau trans τ +
  simple_game c_word_game_moves c_word_game_defender_node
for
  trans :: ‹'s ⇒ 'a ⇒ 's ⇒ bool› and
  τ :: ‹'a› and 
  initial :: ‹('s, 'a) c_word_game_node› 
begin

fun strategy_from_contrasim:: ‹('s ⇒ 's ⇒ bool) ⇒ ('s, 'a) c_word_game_node strategy› where
  ‹strategy_from_contrasim R ((DefenderNode A p1 q0)#play) =
    (AttackerNode (SOME q1 . R q1 p1 ∧ q0 ⇒$A q1) p1)› |
  ‹strategy_from_contrasim _ _ = undefined›

lemma cwg_atknodes_precede_defnodes_in_plays: 
  assumes 
    ‹c_word_game_defender_node n0›
    ‹n0 = DefenderNode A p' q›
    ‹(n0#play) ∈ plays initial›
    ‹initial = AttackerNode p0 q0›
  shows ‹∃p. (hd play) = AttackerNode p q ∧ c_word_game_moves (hd play) n0›
proof -
  have ‹n0 ≠ initial› using assms (2, 4) by auto
  hence mov: ‹c_word_game_moves (hd play) n0› using assms(3)
    by (metis list.inject list.sel(1) plays.cases)     
  hence ‹∃p. (hd play) = AttackerNode p q› using assms(1 - 3)
    by (metis c_word_game_node.inject(2) c_word_game_defender_node.simps(1) c_word_game_moves.elims(2))
  thus ?thesis using mov by auto
qed

lemma cwg_second_play_elem_in_play_set : 
  assumes 
    ‹(n0#play) ∈ plays initial›
    ‹initial = AttackerNode p0 q0›
    ‹n0 = DefenderNode A p q›
  shows ‹hd play ∈ set (n0 # play)›
proof - 
  from assms(2, 3) have ‹n0 ≠ initial› by auto
  hence ‹play ∈ plays initial› 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 = hd play› using x_def by auto
  with x_in_set show ‹hd play ∈ set (n0 # play)› by auto
qed

lemma cwg_contrasim_contains_all_strat_consistent_atknodes:
  assumes 
    ‹contrasimulation R›
    ‹R p0 q0›
    ‹initial = AttackerNode p0 q0›
    ‹play ∈ plays_for_0strategy (strategy_from_contrasim R) initial›
shows ‹((AttackerNode p q) ∈ set play) ⟹ 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  ‹(AttackerNode p q) ∈ (set [initial])›
  thus ‹R p q› using assms(3, 2) by simp
next 
  case p0moved: (2 n0 play)
  hence IH:‹AttackerNode p q ∈ set (n0#play) ⟹ R p q› by simp
  from p0moved.prems have
    ‹(AttackerNode p q) ∈ set ((strategy_from_contrasim R (n0 # play))#n0#play)›
    by simp
  hence ‹(AttackerNode p q =
      (strategy_from_contrasim R (n0 # play))) ∨ (AttackerNode p q ∈ set (n0#play))›
    by simp
  thus ‹R p q›
  proof (rule disjE)
    assume ‹AttackerNode p q ∈ set (n0#play)›
    thus ‹R p q› using IH by simp
  next
    assume A: ‹AttackerNode p q = (strategy_from_contrasim R (n0 # play))›
    have ‹∃A ppred. n0 = (DefenderNode A q ppred)› 
      using p0moved.hyps(3) strategy_from_contrasim.simps(1)[of ‹R›]
      by (metis (no_types, lifting) A c_word_game_node.inject(1) 
          c_word_game_defender_node.elims(2))
    then obtain A ppred where 
      n0_def: ‹n0 = (DefenderNode A q ppred)› ‹∀a∈set A. a ≠ τ›
      by (metis assms(3) c_word_game.cwg_atknodes_precede_defnodes_in_plays
          simulation_challenge p0moved.hyps(1, 3) strategy0_plays_subset)
    hence ‹strategy_from_contrasim R (n0#play) =
        AttackerNode (SOME q1. R q1 q ∧ ppred ⇒$ A  q1) q› 
      using n0_def strategy_from_contrasim.simps(1)[of ‹R› ‹A› ‹q› ‹ppred› ‹play›] by auto
    hence p_def: ‹p = (SOME p1. R p1 q ∧ ppred ⇒$ A p1)› using A by auto
    have ‹∃qpred. hd play = (AttackerNode qpred ppred) ∧ c_word_game_moves (hd play) n0› 
      using cwg_atknodes_precede_defnodes_in_plays strategy0_plays_subset[OF p0moved.hyps(1)]
      by (simp add: assms(3) n0_def  p0moved.hyps(3)) 
    then obtain qpred where qpred_def: ‹hd play = (AttackerNode qpred ppred)› 
      and qpred_move: ‹c_word_game_moves (hd play) n0› by auto
    have qpred_q_move: ‹qpred ⇒$A q› using qpred_def qpred_move n0_def by simp
    have ‹hd play ∈ set (n0 # play)› 
      using cwg_second_play_elem_in_play_set strategy0_plays_subset[OF p0moved.hyps(1)] assms(3)
      by (auto simp add: n0_def)
    hence pred_R: ‹R qpred ppred› 
      by (simp add: qpred_def p0moved.hyps(1) p0moved.hyps(2))
    have  ‹∃ p1 . R p1 q ∧ ppred ⇒$ A p1›
     using qpred_q_move pred_R assms(1) ‹∀a∈set A. a ≠ τ›
     unfolding contrasimulation_def by blast
   from someI_ex[OF this] show ‹R p q› unfolding p_def by blast
  qed
next
  case p1moved: (3 n1 play n1')
  from p1moved.hyps have IH:‹AttackerNode p q ∈ set (n1#play) ⟹ R p q› by simp
  assume  ‹(AttackerNode p q) ∈ (set (n1'#n1#play))›
  hence ‹(AttackerNode p q = n1') ∨ (AttackerNode p q ∈ set (n1#play))› by auto
  thus ‹R p q›
  proof (rule disjE)
    assume ‹(AttackerNode p q ∈ set (n1#play))›
    thus ‹R p q› using p1moved.hyps by auto
  next
   assume A: ‹AttackerNode p q = n1'›
   from p1moved.hyps have ‹player1_position n1› by simp
   hence ‹c_word_game_defender_node n1'›
     by (metis c_word_game_defender_node.simps(2) c_word_game_moves.elims(2) p1moved.hyps(4))
   hence ‹False› using A by auto
   thus ‹R p q› ..
 qed
qed

lemma contrasim_word_game_complete:
  assumes 
    ‹contrasimulation R›
    ‹R p q› 
    ‹initial = AttackerNode p q›
  shows ‹player0_winning_strategy (strategy_from_contrasim R) initial›
    unfolding player0_winning_strategy_def 
proof (safe)
  fix play
  assume A1: ‹play ∈ plays_for_0strategy (strategy_from_contrasim R) initial›
  thus ‹player1_wins_immediately play ⟹ False›
    unfolding player1_wins_immediately_def
  proof - 
    assume A: ‹c_word_game_defender_node (hd play) ∧ (∄p'. c_word_game_moves (hd play) p')›
    have player0_has_succ_node: ‹c_word_game_defender_node (hd play) ⟹
      ∃p'. c_word_game_moves (hd play) p'›
    proof (induct rule: simple_game.plays_for_0strategy.induct[OF A1])
      case init: 1 
      from assms(3) have ‹¬c_word_game_defender_node (hd [initial])› by simp
      hence ‹False› using init.prems by simp
      then show ?case ..
    next
      case p0moved: (2 n0 play)
      from p0moved.hyps have ‹c_word_game_defender_node n0› by simp
      hence ‹∃A p1 q. n0 = (DefenderNode A p1 q)›
        by (meson c_word_game_defender_node.elims(2)) 
      hence ‹¬c_word_game_defender_node (strategy_from_contrasim R (n0#play))›
        using p0moved.hyps(4) c_word_game_moves.elims(2)
          [of ‹n0› ‹strategy_from_contrasim R (n0#play)›]
        by force 
      hence ‹False› using p0moved.prems by simp
      then show ?case ..
    next
      case p1moved: (3 n1 play n1')
      hence ‹¬c_word_game_defender_node n1› using p1moved.hyps by simp
      then obtain p q where n1_def: ‹n1 = AttackerNode p q›
        using c_word_game_defender_node.elims(3) by auto
      hence pq_in_R: ‹R p q› 
        using cwg_contrasim_contains_all_strat_consistent_atknodes[OF assms,
                of ‹n1#play›, OF p1moved.hyps(1)] 
        by auto
      have is_def: ‹c_word_game_defender_node n1'› using p1moved.prems by auto
      then obtain A p1 q0 where n1'_def: ‹n1' = DefenderNode A p1 q0›
        using c_word_game_defender_node.elims(2)[OF is_def] by auto
      hence ‹∀a∈set A. a ≠ τ› using p1moved.hyps(4) n1_def by simp
      have Move_n1_n1': ‹c_word_game_moves (AttackerNode p q) (DefenderNode A p1 q0)› 
        using p1moved.hyps n1_def n1'_def by auto
      hence same_q: ‹q0 = q› by auto
      from Move_n1_n1' have p_succ: ‹p ⇒$A p1› by auto
      from assms(1) have Contra:
          ‹⋀p q p' A. (∀a∈set A. a ≠ τ) ⟹ R p q ⟹ p ⇒$ A  p'
          ⟹ (∃q'. q ⇒$ A  q' ∧ R q' p')› 
        unfolding contrasimulation_def by auto
      hence ‹∃ q'. (q ⇒$ A q')∧ R q' p1›
        using Contra[OF ‹∀a∈set A. a ≠ τ› pq_in_R p_succ] by auto
      hence ‹∃ p1 q1. c_word_game_moves n1' (AttackerNode p1 q1)›
        using same_q n1'_def by auto
      then show ?case by auto
    qed
    thus ‹False› using A by auto
  qed
qed

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

lemma cwg_strategy_from_contrasim_sound: 
  assumes
    ‹R p0 q0›
    ‹contrasimulation R›
    ‹initial = AttackerNode p0 q0›
  shows
    ‹sound_0strategy (strategy_from_contrasim R) initial›
  unfolding sound_0strategy_def
proof (safe)
  fix n0 play
  assume A:
    ‹n0 # play ∈ plays_for_0strategy (strategy_from_contrasim R) initial›
    ‹c_word_game_defender_node n0›
  then obtain A p1 q where n0_def: ‹n0 = DefenderNode A p1 q›
    using c_word_game_defender_node.elims(2) by blast 
  then obtain p where p_def: ‹hd play = AttackerNode p q›
    using n0_def A cwg_atknodes_precede_defnodes_in_plays assms(3) strategy0_plays_subset 
    by blast
  hence ‹c_word_game_moves (AttackerNode p q) (DefenderNode A p1 q)› 
    using A n0_def 
    by (metis assms(3) cwg_atknodes_precede_defnodes_in_plays strategy0_plays_subset)
  hence mov_p_p1: ‹p ⇒$A p1› ‹∀a∈set A. a ≠ τ› by auto  
  from p_def have ‹R p q› 
    using cwg_contrasim_contains_all_strat_consistent_atknodes A assms
      cwg_second_play_elem_in_play_set n0_def strategy0_plays_subset
    by fastforce
  with mov_p_p1 have q1_def: ‹∃q1. R q1 p1 ∧ q ⇒$A q1› 
    using assms(2) unfolding contrasimulation_def by blast
  from n0_def have
    ‹strategy_from_contrasim R (n0 # play)
    = (AttackerNode (SOME q1 . R q1 p1 ∧ q ⇒$A q1) p1)›
    by auto
  then obtain q' where
    ‹AttackerNode (SOME q1 . R q1 p1 ∧ q ⇒$A q1) p1 = AttackerNode q' p1› by blast
  hence q'_def: ‹q' = (SOME q1 . R q1 p1 ∧ q ⇒$A q1)› by auto
  with someI_ex[OF q1_def] have ‹R q' p1 ∧ q ⇒$A q'› by blast
  thus ‹c_word_game_moves n0 (strategy_from_contrasim R (n0 # play))›
    using q'_def by (simp add: n0_def) 
qed

lemma contrasim_word_game_sound: 
  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
    ‹contrasimulation R›  unfolding contrasimulation_def
proof (safe) 
  fix p q p1 A
  assume A1: ‹p ⇒$A p1›
  assume A2: ‹R p q› ‹∀a∈set A. a ≠ τ›
  hence ‹∃ play . play ∈ plays_for_0strategy f initial ∧ hd play = AttackerNode p q›
    using R_def by auto
  from this obtain play where play_def:
    ‹play ∈ plays_for_0strategy f initial ∧ hd play = AttackerNode p q› ..
  from assms(1) have ‹¬player1_wins_immediately play›
    using player0_winning_strategy_def play_def by auto
  hence ‹(c_word_game_defender_node (hd play) ∧ (∄p'. c_word_game_moves (hd play) p')) 
    ⟹ False› 
    using player1_wins_immediately_def by auto
  hence Def_not_stuck: 
    ‹c_word_game_defender_node (hd play) ⟹ (∄p'. c_word_game_moves (hd play) p')
    ⟹ False› 
    by auto
  have ‹(p ⇒$A p1) ⟹ (((DefenderNode A p1 q)#play) ∈ plays_for_0strategy f initial)›
  proof -
    have ‹∃n0. n0 = DefenderNode A p1 q› by auto
    from this obtain n0 where n0_def: ‹n0 = DefenderNode A p1 q› ..
    have play_split: ‹play = (hd play)#(tl play)›
      by (metis hd_Cons_tl play_def strategy0_plays_subset no_empty_plays) 
    hence inF:‹(hd play)#(tl play) ∈ plays_for_0strategy f initial› by (simp add: play_def)
    have pl1: ‹player1_position (hd play)› by (simp add: play_def)
    have mov0:‹c_word_game_moves (hd play) (DefenderNode A p1 q)› 
      using  ‹∀a∈set A. a ≠ τ› by (auto simp add: play_def A1)
    have ‹(DefenderNode A p1 q)#(hd play)#(tl play) ∈ plays_for_0strategy f initial› 
      using plays_for_0strategy.p1move[OF inF pl1 mov0] .
    thus ‹DefenderNode A p1 q#play ∈ plays_for_0strategy f initial›
      by (simp add: sym[OF play_split])
  qed
  hence def_in_f: ‹(DefenderNode A p1 q)#play ∈ plays_for_0strategy f initial›
    by (simp add: A1)
  hence ‹¬(player1_wins_immediately (DefenderNode A p1 q#play))› 
    using assms(1) player0_winning_strategy_def by auto
  hence ‹∃n1. c_word_game_moves (DefenderNode A p1 q) n1›
    using player1_wins_immediately_def by auto
  have move_ex: ‹c_word_game_moves (DefenderNode A p1 q) (f (DefenderNode A p1 q # play))›
    using assms(2) def_in_f sound_0strategy_def by auto
  hence in_f: ‹f ((DefenderNode A p1 q) # play) # (DefenderNode A p1 q) # play
      ∈ plays_for_0strategy f initial› 
    using plays_for_0strategy.p0move[OF def_in_f] by auto
  obtain n1 where
    n1_def: ‹n1 = f (DefenderNode A p1 q # play)› and
    n1_move: ‹c_word_game_moves (DefenderNode A p1 q) n1›
    using move_ex by auto
  hence ‹∃q1. n1 = (AttackerNode q1 p1)›
    using c_word_game_moves.elims(2)[of ‹DefenderNode A p1 q› n1] by auto
  from this obtain q1 where
    q1_def: ‹n1 = (AttackerNode q1 p1)› ..
  have ‹c_word_game_moves (DefenderNode A p1 q) (AttackerNode q1 p1)›
    using q1_def move_ex n1_def by auto
  hence q1_succ: ‹q ⇒$A q1› using c_word_game_moves.simps(2) by auto
  have def: ‹c_word_game_defender_node (DefenderNode A p1 q)› by simp
  hence ‹(AttackerNode q1 p1)#(DefenderNode A p1 q)#play ∈ plays_for_0strategy f initial›
    using q1_def n1_def in_f by auto
  then obtain R_play where
    R_play_def: ‹R_play = (AttackerNode q1 p1)#(DefenderNode A p1 q)#play› and
    R_play_in_f: ‹R_play ∈ plays_for_0strategy f initial› by simp
  hence ‹(hd R_play) = AttackerNode q1 p1› by (simp add: R_play_def)
  hence ‹R q1 p1› unfolding R_def using R_play_in_f by auto
  thus ‹R p q ⟹ p ⇒$ A  p1 ⟹ ∃q1. q ⇒$ A  q1 ∧ R q1 p1› using q1_succ by auto
qed

theorem winning_strategy_in_c_word_game_iff_contrasim:
  assumes
    ‹initial = AttackerNode p q›
  shows 
    ‹(∃ f . player0_winning_strategy f initial ∧ sound_0strategy f initial)
    = (∃ C. contrasimulation C ∧ C p q)›
proof
  assume
    ‹(∃f. player0_winning_strategy f initial ∧ sound_0strategy f initial)›
  then obtain f where
    ‹contrasimulation (λp q.
      ∃play∈plays_for_0strategy f initial. hd play = AttackerNode p q)›
    using contrasim_word_game_sound 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[of _ f] by (meson list.sel(1))
  ultimately show ‹∃ C. contrasimulation C ∧ C p q› by blast
next
  assume
    ‹∃ C. contrasimulation C ∧ C p q›
  thus ‹(∃f. player0_winning_strategy f initial ∧ sound_0strategy f initial)›
    using contrasim_word_game_complete[OF _ _ assms]
         cwg_strategy_from_contrasim_sound[OF _ _ assms] by blast
qed

end                         
end