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 "v0→w" "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) ‹v0→w› 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 ‹v0→w› 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