Theory Basic_Contrasim_Game
theory Basic_Contrasim_Game
imports
Simple_Game
Contrasimulation
begin
subsection ‹The Basic Contrasimulation Preorder Game›
datatype ('s, 'a) c_basic_game_node =
AttackerNode 's 's |
DefenderNode "'a list" 's 's
fun (in lts_tau) c_game_moves ::
‹('s, 'a) c_basic_game_node ⇒ ('s, 'a) c_basic_game_node ⇒ bool› where
simulation_challenge:
‹c_game_moves (AttackerNode p q) (DefenderNode A p1 q0) =
(p ⇒$A p1 ∧ q = q0 ∧ (∀a∈set A. a ≠ τ))› |
simulation_answer:
‹c_game_moves (DefenderNode A p1 q0) (AttackerNode q1 p10) =
(q0 ⇒$A q1 ∧ p1 = p10)› |
c_game_moves_no_step:
‹c_game_moves _ _ = False›
fun c_game_defender_node :: ‹('s, 'a) c_basic_game_node ⇒ bool› where
‹c_game_defender_node (AttackerNode _ _) = False› |
‹c_game_defender_node (DefenderNode _ _ _) = True›
subsection ‹Contrasimulation Implies Winning Strategy (Completeness)›
locale c_basic_game =
lts_tau trans τ +
simple_game c_game_moves c_game_defender_node initial
for
trans :: ‹'s ⇒ 'a ⇒ 's ⇒ bool› and
τ :: ‹'a› and
initial :: ‹('s, 'a) c_basic_game_node›
begin
fun strategy_from_contrasim :: ‹('s ⇒ 's ⇒ bool) ⇒ ('s, 'a) c_basic_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 basic_defender_pred_is_attacker:
assumes
‹c_game_defender_node n0›
‹n0 = DefenderNode A p' q›
‹(n0#play) ∈ plays›
‹initial = AttackerNode p0 q0›
shows ‹∃p. (hd play) = AttackerNode p q ∧ c_game_moves (hd play) n0›
proof -
have ‹n0 ≠ initial› using assms (2, 4) by auto
hence mov: ‹c_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_basic_game_node.inject(2) c_game_defender_node.simps(1) c_game_moves.elims(2))
thus ?thesis using mov by auto
qed
lemma second_elem_in_play_set :
assumes
‹(n0#play) ∈ plays›
‹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› 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 basic_game_all_f_consistent_atk_pos_in_R:
assumes
‹contrasim R›
‹R p0 q0›
‹initial = AttackerNode p0 q0›
‹play ∈ plays_for_strategy (strategy_from_contrasim R)›
shows ‹((AttackerNode p q) ∈ set play) ⟹ R p q›
using assms(4)
proof (induct arbitrary: p q rule: plays_for_strategy.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_basic_game_node.inject(1) c_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_basic_game.basic_defender_pred_is_attacker simulation_challenge p0moved.hyps(1, 3) strategy_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_game_moves (hd play) n0›
using basic_defender_pred_is_attacker strategy_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_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 second_elem_in_play_set strategy_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 contrasim_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_game_defender_node n1'›
by (metis c_game_defender_node.simps(2) c_game_moves.elims(2) p1moved.hyps(4) player1_position_def)
hence ‹False› using A by auto
thus ‹R p q› ..
qed
qed
lemma basic_contrasim_game_complete:
assumes
‹contrasim R›
‹R p q›
‹initial = AttackerNode p q›
shows ‹player0_winning_strategy (strategy_from_contrasim R)›
unfolding player0_winning_strategy_def
proof (safe)
fix play
assume A1: ‹play ∈ (plays_for_strategy (strategy_from_contrasim R))›
thus ‹player1_wins play ⟹ False›
unfolding player1_wins_def
proof -
assume A: ‹c_game_defender_node (hd play) ∧ (∄p'. c_game_moves (hd play) p')›
have player0_has_succ_node: ‹c_game_defender_node (hd play) ⟹ ∃p'. c_game_moves (hd play) p'›
proof (induct rule: simple_game.plays_for_strategy.induct[OF A1])
case init: 1
from assms(3) have ‹¬c_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_game_defender_node n0› by simp
hence ‹∃A p1 q. n0 = (DefenderNode A p1 q)›
by (meson c_game_defender_node.elims(2))
hence ‹¬c_game_defender_node (strategy_from_contrasim R (n0#play))›
using p0moved.hyps(4) c_game_moves.elims(2)[of ‹n0› ‹strategy_from_contrasim R (n0#play)›]
by force
hence ‹¬c_game_defender_node (hd (strategy_from_contrasim R (n0 # play) # n0 # play))›
by simp
hence ‹False› using p0moved.prems ..
then show ?case ..
next
case p1moved: (3 n1 play n1')
hence ‹¬c_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_game_defender_node.elims(3) by auto
hence pq_in_R: ‹R p q›
using basic_game_all_f_consistent_atk_pos_in_R[OF assms, of ‹n1#play›, OF p1moved.hyps(1)]
by auto
have is_def: ‹c_game_defender_node n1'› using p1moved.prems by auto
then obtain A p1 q0 where n1'_def: ‹n1' = DefenderNode A p1 q0›
using c_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_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 contrasim_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_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
lemma strategy_from_contrasim_sound :
assumes
‹R p0 q0›
‹contrasim R›
‹initial = AttackerNode p0 q0›
shows
‹sound_strategy (strategy_from_contrasim R)›
unfolding sound_strategy_def
proof (safe)
fix n0 play
assume A:
‹n0 # play ∈ plays_for_strategy (strategy_from_contrasim R)›
‹c_game_defender_node n0›
then obtain A p1 q where n0_def: ‹n0 = DefenderNode A p1 q›
using c_game_defender_node.elims(2) by blast
then obtain p where p_def: ‹hd play = AttackerNode p q›
using n0_def A basic_defender_pred_is_attacker assms(3) strategy_plays_subset by blast
hence ‹c_game_moves (AttackerNode p q) (DefenderNode A p1 q)›
using A n0_def by (metis assms(3) basic_defender_pred_is_attacker strategy_plays_subset)
hence mov_p_p1: ‹p ⇒$A p1› ‹∀a∈set A. a ≠ τ› by auto
from p_def have ‹R p q›
using basic_game_all_f_consistent_atk_pos_in_R A assms
second_elem_in_play_set n0_def strategy_plays_subset
by fastforce
with mov_p_p1 have q1_def: ‹∃q1. R q1 p1 ∧ q ⇒$A q1›
using assms(2) unfolding contrasim_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_game_moves n0 (strategy_from_contrasim R (n0 # play))› using q'_def by (simp add: n0_def)
qed
lemma basic_contrasim_game_sound:
assumes
‹player0_winning_strategy f›
‹sound_strategy f›
defines
‹R == λ p q . (∃ play ∈ plays_for_strategy f . hd play = AttackerNode p q)›
shows
‹contrasim R› unfolding contrasim_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_strategy f ∧ hd play = AttackerNode p q› using R_def by auto
from this obtain play where play_def: ‹play ∈ plays_for_strategy f ∧ hd play = AttackerNode p q› ..
from assms(1) have ‹¬player1_wins play› using player0_winning_strategy_def play_def by auto
hence ‹(c_game_defender_node (hd play) ∧ (∄p'. c_game_moves (hd play) p')) ⟹ False›
using player1_wins_def by auto
hence Def_not_stuck: ‹c_game_defender_node (hd play) ⟹ (∄p'. c_game_moves (hd play) p') ⟹ False›
by auto
have ‹(p ⇒$A p1) ⟹ (((DefenderNode A p1 q)#play) ∈ plays_for_strategy f)›
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 strategy_plays_subset no_empty_plays)
hence inF:‹(hd play)#(tl play) ∈ plays_for_strategy f› by (simp add: play_def)
have pl1: ‹player1_position (hd play)› by (simp add: play_def player1_position_def)
have mov0:‹c_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_strategy f›
using plays_for_strategy.p1move[OF inF pl1 mov0] .
thus ‹DefenderNode A p1 q#play ∈ plays_for_strategy f› by (simp add: sym[OF play_split])
qed
hence def_in_f: ‹(DefenderNode A p1 q)#play ∈ plays_for_strategy f› by (simp add: A1)
hence ‹¬(player1_wins (DefenderNode A p1 q#play))›
using assms(1) player0_winning_strategy_def by auto
hence ‹∃n1. c_game_moves (DefenderNode A p1 q) n1› using player1_wins_def by auto
have move_ex: ‹c_game_moves (DefenderNode A p1 q) (f (DefenderNode A p1 q # play))›
using assms(2) def_in_f sound_strategy_def by auto
hence in_f: ‹f ((DefenderNode A p1 q) # play) # (DefenderNode A p1 q) # play ∈ plays_for_strategy f›
using plays_for_strategy.p0move[OF def_in_f] by auto
obtain n1 where n1_def: ‹n1 = f (DefenderNode A p1 q # play)›
and n1_move: ‹c_game_moves (DefenderNode A p1 q) n1› using move_ex by auto
hence ‹∃q1. n1 = (AttackerNode q1 p1)›
using c_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_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_game_moves.simps(2) by auto
have def: ‹c_game_defender_node (DefenderNode A p1 q)› by simp
hence ‹(AttackerNode q1 p1)#(DefenderNode A p1 q)#play ∈ plays_for_strategy f›
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_strategy f› 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_basic_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)›
using basic_contrasim_game_sound by blast
moreover have ‹(λp q. ∃play∈plays_for_strategy f. hd play = AttackerNode p q) 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 basic_contrasim_game_complete[OF _ _ assms]
strategy_from_contrasim_sound[OF _ _ assms] by blast
qed
end
end