Theory WinningStrategy

section ‹Winning Strategies›

theory WinningStrategy
imports
  Main
  Strategy
begin

context ParityGame begin

text ‹
  Here we define winning strategies.

  A strategy is winning for player @{term p} from @{term v0} if every maximal @{term σ}-path
  starting in @{term v0} is winning.
›
definition winning_strategy :: "Player ⇒ 'a Strategy ⇒ 'a ⇒ bool" where
  "winning_strategy p σ v0 ≡ ∀P. vmc_path G P v0 p σ ⟶ winning_path p P"

lemma winning_strategyI [intro]:
  assumes "⋀P. vmc_path G P v0 p σ ⟹ winning_path p P"
  shows "winning_strategy p σ v0"
  unfolding winning_strategy_def using assms by blast

lemma (in vmc_path) paths_hits_winning_strategy_is_winning:
  assumes σ: "winning_strategy p σ v"
    and v: "v ∈ lset P"
  shows "winning_path p P"
proof-
  obtain n where n: "enat n < llength P" "P $ n = v" using v by (meson in_lset_conv_lnth)
  interpret P': vmc_path G "ldropn n P" v p σ using n vmc_path_ldropn by blast
  have "winning_path p (ldropn n P)" using σ by (simp add: winning_strategy_def P'.vmc_path_axioms)
  thus ?thesis using winning_path_drop_add P_valid n(1) by blast
qed

text ‹There cannot exist winning strategies for both players for the same node.›

lemma winning_strategy_only_for_one_player:
  assumes σ: "strategy p σ" "winning_strategy p σ v"
    and σ': "strategy p** σ'" "winning_strategy p** σ' v"
    and v: "v ∈ V"
  shows "False"
proof-
  obtain P where "vmc2_path G P v p σ σ'" using assms strategy_conforming_path_exists by blast
  then interpret vmc2_path G P v p σ σ' .
  have "winning_path p P"
    using paths_hits_winning_strategy_is_winning σ(2) v0_lset_P by blast
  moreover have "winning_path p** P"
    using comp.paths_hits_winning_strategy_is_winning σ'(2) v0_lset_P by blast
  ultimately show False using P_valid paths_are_winning_for_one_player by blast
qed

subsection ‹Deadends›

lemma no_winning_strategy_on_deadends:
  assumes "v ∈ VV p" "deadend v" "strategy p σ"
  shows "¬winning_strategy p σ v"
proof-
  obtain P where "vmc_path G P v p σ" using strategy_conforming_path_exists_single assms by blast
  then interpret vmc_path G P v p σ .
  have "P = LCons v LNil" using P_deadend_v0_LCons ‹deadend v› by blast
  hence "¬winning_path p P" unfolding winning_path_def using ‹v ∈ VV p› by auto
  thus ?thesis using winning_strategy_def vmc_path_axioms by blast
qed

lemma winning_strategy_on_deadends:
  assumes "v ∈ VV p" "deadend v" "strategy p σ"
  shows "winning_strategy p** σ v"
proof
  fix P assume "vmc_path G P v p** σ"
  then interpret vmc_path G P v "p**" σ .
  have "P = LCons v LNil" using P_deadend_v0_LCons ‹deadend v› by blast
  thus "winning_path p** P" unfolding winning_path_def
    using ‹v ∈ VV p› P_valid paths_are_winning_for_one_player by auto
qed

subsection ‹Extension Theorems›

lemma strategy_extends_VVp:
  assumes v0: "v0 ∈ VV p" "¬deadend v0"
  and σ: "strategy p σ" "winning_strategy p σ v0"
  shows "winning_strategy p σ (σ v0)"
proof
  fix P assume "vmc_path G P (σ v0) p σ"
  then interpret vmc_path G P "σ v0" p σ .
  have "v0→σ v0" using v0 σ(1) strategy_def by blast
  hence "winning_path p (LCons v0 P)"
    using σ(2) extension_valid_maximal_conforming winning_strategy_def by blast
  thus "winning_path p P" using winning_path_ltl[of p "LCons v0 P"] by simp
qed

lemma strategy_extends_VVpstar:
  assumes v0: "v0 ∈ VV p**" "v0→w0"
  and σ: "winning_strategy p σ v0"
  shows "winning_strategy p σ w0"
proof
  fix P assume "vmc_path G P w0 p σ"
  then interpret vmc_path G P w0 p σ .
  have "winning_path p (LCons v0 P)"
    using extension_valid_maximal_conforming VV_impl1 σ v0 winning_strategy_def
    by auto
  thus "winning_path p P" using winning_path_ltl[of p "LCons v0 P"] by auto
qed

lemma strategy_extends_backwards_VVpstar:
  assumes v0: "v0 ∈ VV p**"
    and σ: "strategy p σ" "⋀w. v0→w ⟹ winning_strategy p σ w"
  shows "winning_strategy p σ v0"
proof
  fix P assume "vmc_path G P v0 p σ"
  then interpret vmc_path G P v0 p σ .
  show "winning_path p P" proof (cases)
    assume "deadend v0"
    thus ?thesis using P_deadend_v0_LCons winning_path_def v0 by auto
  next
    assume "¬deadend v0"
    then interpret vmc_path_no_deadend G P v0 p σ by unfold_locales
    interpret ltlP: vmc_path G "ltl P" w0 p σ using vmc_path_ltl .
    have "winning_path p (ltl P)"
      using σ(2) v0_edge_w0 vmc_path_ltl winning_strategy_def by blast
    thus "winning_path p P"
      using winning_path_LCons by (metis P_LCons' ltlP.P_LCons ltlP.P_not_null)
  qed
qed

lemma strategy_extends_backwards_VVp:
  assumes v0: "v0 ∈ VV p" "σ v0 = w" "v0→w"
    and σ: "strategy p σ" "winning_strategy p σ w"
  shows "winning_strategy p σ v0"
proof
  fix P assume "vmc_path G P v0 p σ"
  then interpret vmc_path G P v0 p σ .
  have "¬deadend v0" using ‹v0→w› by blast
  then interpret vmc_path_no_deadend G P v0 p σ by unfold_locales
  have "winning_path p (ltl P)"
    using σ(2)[unfolded winning_strategy_def] v0(1,2) v0_conforms vmc_path_ltl by presburger
  thus "winning_path p P" using winning_path_LCons by (metis P_LCons Ptl_not_null)
qed

end ― ‹context ParityGame›

end