Theory Contrasim_Set_Game
theory Contrasim_Set_Game
imports
Simple_Game
Contrasimulation
begin
subsection ‹The Contrasimulation Preorder Set Game›
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 (Completeness)›
locale c_set_game =
lts_tau trans τ +
simple_game c_set_game_moves c_set_game_defender_node initial
for
trans :: ‹'s ⇒ 'a ⇒ 's ⇒ bool› and
τ :: ‹'a› and
initial :: ‹('s, 'a) c_set_game_node›
begin
fun strategy_from_F_of_C :: ‹('s ⇒ ('s set) ⇒ bool) ⇒ ('s, 'a) c_set_game_node strategy›
where
‹strategy_from_F_of_C R ((DefenderSwapNode p1 Q)#play) =
(AttackerNode (SOME q1 . (∃q. (q ∈ Q ∧ q ⇒^τ q1)) ∧ R q1 {p1}) {p1})› |
‹strategy_from_F_of_C R ((DefenderSimNode a p1 Q)#play) =
(AttackerNode p1 (SOME Q1 . Q1 = dsuccs a Q ∧ R p1 Q1))› |
‹strategy_from_F_of_C _ _ = undefined›
lemma set_defender_pred_is_attacker:
assumes
‹c_set_game_defender_node n0›
‹(n0#play) ∈ plays›
‹initial = AttackerNode p0 Q0›
shows ‹∃p Q. (hd play) = AttackerNode p Q ∧ c_set_game_moves (hd play) n0›
proof -
have ‹n0 ≠ initial› using assms (1, 3) 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 second_elem_in_play_set :
assumes
‹(n0#play) ∈ plays›
‹initial = AttackerNode p0 Q0›
‹c_set_game_defender_node n0›
shows ‹hd play ∈ set (n0 # play)›
proof -
from assms(2, 3) have ‹n0 ≠ initial›by auto
hence ‹play ∈ plays› 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 def_sim_or_swap_before_atkNode:
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 set_game_strategy_retains_F:
assumes
‹contrasim C›
‹C p0 q0›
‹initial = AttackerNode p0 {q0}›
‹play ∈ plays_for_strategy (strategy_from_F_of_C (F (set_type C)))›
shows ‹n = AttackerNode p Q ⟹ n ∈ set play ⟹ F (set_type C) p Q ›
proof (induct arbitrary: n p Q rule: plays_for_strategy.induct[OF assms(4)])
case init: 1
hence ‹n = initial› by auto
hence ‹p = p0 ∧ Q = {q0}› using assms(3) init.prems(1) by auto
thus ‹F (set_type C) p Q› using assms R_is_in_F_of_R set_type_def by simp
next
case p0moved: (2 n0 play)
hence ‹(n = strategy_from_F_of_C (F (set_type 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_F_of_C (F (set_type C)) (n0 # play)›
hence ‹(∃a Qpred. n0 = DefenderSimNode a p Qpred) ∨ (∃q Ppred. n0 = DefenderSwapNode q Ppred ∧ Q = {q})›
using def_sim_or_swap_before_atkNode[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_F_of_C (F (set_type C)) (n0#play)
= AttackerNode p (SOME Q1. Q1 = dsuccs a Qpred ∧ (F (set_type C)) p Q1)›
using strategy_from_F_of_C.simps(2) by auto
hence Q_def: ‹Q = (SOME Q1. Q1 = dsuccs a Qpred ∧ (F (set_type 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 set_defender_pred_is_attacker strategy_plays_subset[OF p0moved.hyps(1)]
assms(3, 4) 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 second_elem_in_play_set strategy_plays_subset[OF p0moved.hyps(1)] assms(3) n0_def
by (simp add: assms(4))
hence ‹F (set_type C) ppred Qpred› using p0moved.hyps(2) ppred_def by blast
hence ‹F (set_type C) p (dsuccs a Qpred)›
using ‹ppred =⊳a p› assms(1,2,4) F_of_C_guarantees_action_succ ‹a ≠ τ› by auto
hence ‹∃Q. Q = (dsuccs a Qpred) ∧ F (set_type C) p Q› by auto
from someI_ex[OF this] show ‹F (set_type 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_F_of_C (F (set_type C)) (n0#play)
= AttackerNode (SOME p1. (∃p. p ∈ Ppred ∧ p ⇒^τ p1) ∧ (F (set_type C)) p1 {q}) {q}›
using strategy_from_F_of_C.simps(1) by auto
hence p_def: ‹p = (SOME p1. (∃p. p ∈ Ppred ∧ p ⇒^τ p1) ∧ (F (set_type C)) p1 {q})›
using strat p0moved.prems by auto
have ‹∃qpred. hd play = (AttackerNode qpred Ppred) ∧ c_set_game_moves (hd play) n0›
using set_defender_pred_is_attacker strategy_plays_subset[OF p0moved.hyps(1)]
assms(3, 4) 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 add: player1_position_def)
have qpred_q_move: ‹qpred ⇒^τ q› using qpred_def qpred_move n0_def by simp
have ‹hd play ∈ set (n0 # play)›
using second_elem_in_play_set strategy_plays_subset[OF p0moved.hyps(1)] assms(3) n0_def
by (simp add: assms(4))
hence ‹F (set_type C) qpred Ppred› using p0moved.hyps(2) qpred_def by blast
hence ‹∃p. p ∈ weak_tau_succs Ppred ∧ F (set_type C) p {q}›
using qpred_q_move assms(1,2) F_of_C_guarantees_tau_succ by blast
hence ‹∃p. (∃p0. p0 ∈ Ppred ∧ p0 ⇒^τ p) ∧ F (set_type C) p {q}›
using weak_tau_succs_def[of ‹Ppred›] by blast
from someI_ex[OF this] p_def have ‹F (set_type C) p {q}› by simp
thus ‹F (set_type 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 def_sim_or_swap_before_atkNode p1moved.hyps(3, 4) p1moved.prems(1)
player1_position_def by fastforce
hence ‹False› using A1 p1moved.prems(1) by auto
thus ?case by auto
qed
qed
lemma set_contrasim_game_complete:
assumes
‹contrasim C›
‹C p0 q0›
‹initial = AttackerNode p0 {q0}›
shows ‹player0_winning_strategy (strategy_from_F_of_C (F (set_type C)))›
unfolding player0_winning_strategy_def
proof (safe)
fix play
assume A1: ‹play ∈ (plays_for_strategy (strategy_from_F_of_C (F (set_type C))))›
thus ‹player1_wins play ⟹ False›
unfolding player1_wins_def
proof -
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_strategy.induct[OF A1])
case init: 1
have ‹¬c_set_game_defender_node (hd [initial])› 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_F_of_C (F (set_type C)) (n0#play))›
using p0moved.hyps(4)
c_set_game_moves.elims(2)[of ‹n0› ‹strategy_from_F_of_C (F (set_type C)) (n0#play)›]
by force
hence ‹¬c_set_game_defender_node (hd (strategy_from_F_of_C (F (set_type 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 and player1_position_def 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_F: ‹F (set_type C) p Q›
using set_game_strategy_retains_F[OF assms(1-3), 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 ‹F (set_type C) p1 (dsuccs a Q)›
using F_of_C_guarantees_action_succ move
by (metis in_F assms(1) simulation_challenge tau_tau)
then obtain Q1 where ‹Q1 = dsuccs a Q ∧ F (set_type 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 ∧ F (set_type C) q' {p1}›
using in_F F_of_C_guarantees_tau_succ assms(1) by auto
hence ‹∃q1. q1 ∈ weak_tau_succs Q ∧ F (set_type 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 strategy_from_F_of_C_sound :
assumes
‹contrasim C›
‹C p0 q0›
‹initial = AttackerNode p0 {q0}›
shows
‹sound_strategy (strategy_from_F_of_C (F (set_type C)))›
unfolding sound_strategy_def
proof (safe)
fix n0 play
assume A:
‹n0 # play ∈ plays_for_strategy (strategy_from_F_of_C (F (set_type C)))›
‹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_F_of_C (F (set_type 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 assms(3) set_defender_pred_is_attacker simulation_challenge strategy_plays_subset)
hence ‹c_set_game_moves (AttackerNode p Q) (DefenderSimNode a p' Q)›
by (metis A n0_def assms(3) set_defender_pred_is_attacker strategy_plays_subset)
hence ‹p =⊳a p'› ‹¬ tau a› by auto
hence ‹F (set_type C) p Q›
using set_game_strategy_retains_F[OF assms] A p_def
assms(3) second_elem_in_play_set strategy_plays_subset
by fastforce
hence ‹F (set_type C) p' (dsuccs a Q)›
using F_of_C_guarantees_action_succ ‹¬ tau a› ‹p =⊳a p'› assms(1) tau_tau by blast
hence Q1_ex: ‹∃Q'. Q' = dsuccs a Q ∧ F (set_type C) p' Q'› by auto
from n0_def have st: ‹strategy_from_F_of_C (F (set_type C)) (n0#play) =
(AttackerNode p' (SOME Q1 . Q1 = dsuccs a Q ∧ (F (set_type C)) p' Q1))› by auto
then obtain Q1 where
‹AttackerNode p' (SOME Q1 . Q1 = dsuccs a Q ∧ (F (set_type C)) p' Q1) = AttackerNode p' Q1›
by blast
hence Q1_def: ‹Q1 = (SOME Q1 . Q1 = dsuccs a Q ∧ (F (set_type C)) p' Q1)›
by auto
have next_is_atk: ‹strategy_from_F_of_C (F (set_type C)) (n0#play) = (AttackerNode p' Q1)›
using st Q1_def by auto
with someI_ex[OF Q1_ex] Q1_def have mov_cond: ‹Q1 = dsuccs a Q ∧ F (set_type 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 assms(3) set_defender_pred_is_attacker swap_challenge strategy_plays_subset)
hence ‹c_set_game_moves (AttackerNode p Q) (DefenderSwapNode p' Q)›
by (metis A n0_def assms(3) set_defender_pred_is_attacker strategy_plays_subset)
hence ‹p ⇒^τ p'› by auto
hence ‹F (set_type C) p Q›
using set_game_strategy_retains_F[OF assms] A p_def
assms(3) second_elem_in_play_set strategy_plays_subset
by fastforce
hence ‹∃q'. q' ∈ weak_tau_succs Q ∧ F (set_type C) q' {p'}›
using F_of_C_guarantees_tau_succ ‹p ⇒^τ p'› assms(1) by auto
hence q1_ex: ‹∃q1. (∃q.(q ∈ Q ∧ q ⇒^τ q1)) ∧ F (set_type C) q1 {p'}› using weak_tau_succs_def by auto
hence strat: ‹strategy_from_F_of_C (F (set_type C)) (n0#play) =
AttackerNode (SOME q1 . (∃q. (q ∈ Q ∧ q ⇒^τ q1)) ∧ (F (set_type C)) q1 {p'}) {p'}›
using n0_def by auto
then obtain q1 where
‹AttackerNode (SOME q1 . (∃q. (q ∈ Q ∧ q ⇒^τ q1)) ∧ (F (set_type C)) q1 {p'}) {p'}
= AttackerNode q1 {p'}› by blast
hence q1_def: ‹q1 = (SOME q1 . (∃q. (q ∈ Q ∧ q ⇒^τ q1)) ∧ (F (set_type C)) q1 {p'})›
by auto
with someI_ex[OF q1_ex] have X: ‹∃q. (q ∈ Q ∧ q ⇒^τ q1) ∧ F (set_type 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 (Soundness)›
lemma move_DefSim_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) c_set_game_defender_node.elims(3) local.c_set_game_moves_no_step(1) local.c_set_game_moves_no_step(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 def_never_stuck_on_sim_pos:
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 def_sim_pos_with_prefix_in_play:
assumes
‹A ≠ []›
‹p ⇒$A p1›
‹∀a∈set A. a ≠ τ›
‹sound_strategy f›
‹play ∈ plays_for_strategy f›
‹hd play = AttackerNode p {q}›
shows ‹∃play p0. ((DefenderSimNode (last A) p0 (dsuccs_seq_rec (rev (butlast A)) {q}))#play)
∈ plays_for_strategy f ∧ 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_strategy f› using assms(5,6)
by (metis c_set_game_defender_node.simps(1) list.collapse no_empty_plays
player1_position_def plays_for_strategy.p1move strategy_plays_subset)
hence inplay: ‹((DefenderSimNode (last [a]) p0 (dsuccs_seq_rec (rev (butlast [a])) {q}))#play) ∈ plays_for_strategy f›
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_strategy f ∧ 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_strategy f› ‹word_reachable_via_delay as p p0 p'› by auto
hence ‹DefenderSimNode a2 p0 (dsuccs_seq_rec (rev as2) {q}) # play
∈ plays_for_strategy f› 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_strategy f› by auto
then obtain n1
where n1_def: ‹c_set_game_moves (DefenderSimNode a2 p0 (dsuccs_seq_rec (rev as2) {q})) n1›
using def_never_stuck_on_sim_pos by meson
hence n1_atk: ‹n1 = AttackerNode p0 (dsuccs a2 ((dsuccs_seq_rec (rev as2) {q})))›
using move_DefSim_to_AtkNode[OF n1_def] by auto
have n1_in_play: ‹n1#n0#play ∈ plays_for_strategy f› using n1_def n0_in_play n0_def
by (metis assms(4) move_DefSim_to_AtkNode c_set_game_defender_node.simps(2)
plays_for_strategy.simps sound_strategy_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_strategy f› using n1_in_play
by (simp add: n1_atk player1_position_def plays_for_strategy.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 set_contrasim_game_sound:
assumes
‹player0_winning_strategy f›
‹sound_strategy f›
defines
‹C == λ p q . (∃ play ∈ plays_for_strategy f . hd play = AttackerNode p {q} ∧ (hd play = initial ∨ (∃P. hd (tl play) = DefenderSwapNode q P)))›
shows
‹contrasim C› unfolding contrasim_def
proof (safe)
fix p q p1 A
assume ‹∀a∈set A. a ≠ τ› ‹p ⇒$A p1› and ‹C p q›
hence ‹p ⇒$(taufree A) p1› by (simp add: weak_step_over_tau)
hence ‹(∃ play ∈ plays_for_strategy f . hd play = AttackerNode p {q} ∧ (hd play = initial ∨ (∃P. hd (tl play) = DefenderSwapNode q P)))›
using C_def ‹p ⇒$A p1› and ‹C p q› by auto
from this obtain play where play_def: ‹play ∈ plays_for_strategy f›
and play_hd: ‹hd play = AttackerNode p {q}›
and ‹hd play = initial ∨ (∃P. hd (tl play) = DefenderSwapNode q P)›
by auto
hence ‹¬player1_wins 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_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 strategy_plays_subset)
hence ‹n0#play ∈ plays_for_strategy f› using n0_def n0_move play_def play_hd
by (metis c_set_game_defender_node.simps(1) play_def
player1_position_def plays_for_strategy.p1move)
hence ‹∃n1'. c_set_game_moves n0 n1' ∧ n1'#n0#play ∈ plays_for_strategy f›
using assms(2) n0_def sound_strategy_def
by (meson c_set_game_defender_node.simps(3) plays_for_strategy.p0move)
then obtain n1' where n1'_mov: ‹c_set_game_moves n0 n1'›
and in_play: ‹n1'#n0#play ∈ plays_for_strategy f› 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_strategy f› ‹word_reachable_via_delay A p p0 p1›
using def_sim_pos_with_prefix_in_play ‹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_strategy f› 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_strategy_def)
hence ‹n1 = AttackerNode p0 (dsuccs a (dsuccs_seq_rec (rev as) {q}))›
using move_DefSim_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_strategy f›
using n0_def A_play_def n1_move assms(2) move_DefSim_to_AtkNode
plays_for_strategy.p0move sound_strategy_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_strategy f›
using n1_in_play by (simp add: n1_def player1_position_def plays_for_strategy.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_strategy_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
by (metis c_set_game_defender_node.cases c_set_game_moves_no_step(3, 7) swap_answer)
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_strategy f›
using in_strat plays_for_strategy.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_set_game_iff_contrasim:
assumes
‹initial = AttackerNode p {q}›
shows
‹(∃ f . player0_winning_strategy f ∧ sound_strategy f) = (∃ C. contrasim C ∧ C p q)›
proof
assume
‹(∃f. player0_winning_strategy f ∧ sound_strategy f)›
then obtain f where
‹contrasim
(λp q. ∃play∈plays_for_strategy f.
hd play = AttackerNode p {q} ∧
(hd play = initial ∨ (∃P. hd (tl play) = DefenderSwapNode q P)))›
using set_contrasim_game_sound by blast
moreover have ‹(λp q. ∃play∈plays_for_strategy f.
hd play = AttackerNode p {q} ∧
(hd play = initial ∨ (∃P. hd (tl play) = DefenderSwapNode q P))) p q›
using assms plays_for_strategy.init[of f] by (meson list.sel(1))
ultimately show ‹∃ C. contrasim C ∧ C p q› by blast
next
assume
‹∃ C. contrasim C ∧ C p q›
thus ‹(∃f. player0_winning_strategy f ∧ sound_strategy f)›
using set_contrasim_game_complete[OF _ _ assms]
strategy_from_F_of_C_sound[OF _ _ assms] by blast
qed
end
end