Theory AttractorStrategy

section ‹Attractor Strategies›

theory AttractorStrategy
imports
  Main
  Attractor UniformStrategy
begin

text ‹This section proves that every attractor set has an attractor strategy.›

context ParityGame begin

lemma strategy_attracts_extends_VVp:
  assumes σ: "strategy p σ" "strategy_attracts p σ S W"
    and v0: "v0  VV p" "v0  directly_attracted p S" "v0  S"
  shows "σ. strategy p σ  strategy_attracts_via p σ v0 (insert v0 S) W"
proof-
  from v0(1,2) obtain w where "v0w" "w  S" using directly_attracted_def by blast
  from w  S σ(2) have "strategy_attracts_via p σ w S W" unfolding strategy_attracts_def by blast
  let  = "σ(v0 := w)" ― ‹Extend @{term σ} to the new node.›
  have "strategy p " using σ(1) v0w valid_strategy_updates by blast
  moreover have "strategy_attracts_via p  v0 (insert v0 S) W" proof
    fix P
    assume "vmc_path G P v0 p "
    then interpret vmc_path G P v0 p  .
    have "¬deadend v0" using v0w by blast
    then interpret vmc_path_no_deadend G P v0 p  by unfold_locales

    define P'' where [simp]: "P'' = ltl P"
    have "lhd P'' = w" using v0(1) v0_conforms w0_def by auto
    hence "vmc_path G P'' w p " using vmc_path_ltl by (simp add: w0_def)

    have *: "v0  S - W" using v0  S by blast
    have "override_on (σ(v0 := w)) σ (S - W) = "
      by (rule ext) (metis * fun_upd_def override_on_def)
    hence "strategy_attracts p  S W"
      using strategy_attracts_irrelevant_override[OF σ(2,1) strategy p ] by simp
    hence "strategy_attracts_via p  w S W" unfolding strategy_attracts_def
      using w  S by blast
    hence "visits_via P'' S W" unfolding strategy_attracts_via_def
      using vmc_path G P'' w p  by blast
    thus "visits_via P (insert v0 S) W"
      using visits_via_LCons[of "ltl P" S W v0] P_LCons by simp
  qed
  ultimately show ?thesis by blast
qed

lemma strategy_attracts_extends_VVpstar:
  assumes σ: "strategy_attracts p σ S W"
    and v0: "v0  VV p" "v0  directly_attracted p S"
  shows "strategy_attracts_via p σ v0 (insert v0 S) W"
proof
  fix P
  assume "vmc_path G P v0 p σ"
  then interpret vmc_path G P v0 p σ .
  have "¬deadend v0" using v0(2) directly_attracted_contains_no_deadends by blast
  then interpret vmc_path_no_deadend G P v0 p σ by unfold_locales
  have "visits_via (ltl P) S W"
    using vmc_path.strategy_attractsE[OF vmc_path_ltl σ] v0 directly_attracted_def by simp
  thus "visits_via P (insert v0 S) W" using visits_via_LCons[of "ltl P" S W v0] P_LCons by simp
qed

lemma attractor_has_strategy_single:
  assumes "W  V"
    and v0_def: "v0  attractor p W" (is "_  ?A")
  shows "σ. strategy p σ  strategy_attracts_via p σ v0 ?A W"
using assms proof (induct arbitrary: v0 rule: attractor_set_induction)
  case (step S)
  have "v0  W  σ. strategy p σ  strategy_attracts_via p σ v0 {} W"
    using strategy_attracts_via_trivial valid_arbitrary_strategy by blast
  moreover {
    assume *: "v0  directly_attracted p S" "v0  S"
    from assms(1) step.hyps(1) step.hyps(2)
      have "σ. strategy p σ  strategy_attracts p σ S W"
      using merge_attractor_strategies by auto
    with *
      have "σ. strategy p σ  strategy_attracts_via p σ v0 (insert v0 S) W"
      using strategy_attracts_extends_VVp strategy_attracts_extends_VVpstar by blast
  }
  ultimately show ?case
    using step.prems step.hyps(2)
    attractor_strategy_on_extends[of p _ v0 "insert v0 S" W "W  S  directly_attracted p S"]
    attractor_strategy_on_extends[of p _ v0 "S"           W "W  S  directly_attracted p S"]
    attractor_strategy_on_extends[of p _ v0 "{}"          W "W  S  directly_attracted p S"]
    by blast
next
  case (union M)
  hence "S. S  M  v0  S" by blast
  thus ?case by (meson Union_upper attractor_strategy_on_extends union.hyps)
qed

subsection ‹Existence›

text ‹Prove that every attractor set has an attractor strategy.›

theorem attractor_has_strategy:
  assumes "W  V"
  shows "σ. strategy p σ  strategy_attracts p σ (attractor p W) W"
proof-
  let ?A = "attractor p W"
  have "?A  V" by (simp add: W  V attractor_in_V)
  moreover
    have "v. v  ?A  σ. strategy p σ  strategy_attracts_via p σ v ?A W"
    using W  V attractor_has_strategy_single by blast
  ultimately show ?thesis using merge_attractor_strategies W  V by blast
qed

end ― ‹context ParityGame›

end