Theory AttractingStrategy

section ‹Attracting Strategies›

theory AttractingStrategy
imports
  Main
  Strategy
begin

text ‹Here we introduce the concept of attracting strategies.›

context ParityGame begin

subsection ‹Paths Visiting a Set›

text ‹A path that stays in ‹A› until eventually it visits ‹W›.›
definition "visits_via P A W ≡ ∃n. enat n < llength P ∧ P $ n ∈ W ∧ lset (ltake (enat n) P) ⊆ A"

lemma visits_via_monotone: "⟦ visits_via P A W; A ⊆ A' ⟧ ⟹ visits_via P A' W"
  unfolding visits_via_def by blast

lemma visits_via_visits: "visits_via P A W ⟹ lset P ∩ W ≠ {}"
  unfolding visits_via_def by (meson disjoint_iff_not_equal in_lset_conv_lnth)

lemma (in vmc_path) visits_via_trivial: "v0 ∈ W ⟹ visits_via P A W"
  unfolding visits_via_def apply (rule exI[of _ 0]) using zero_enat_def by auto

lemma visits_via_LCons:
  assumes "visits_via P A W"
  shows "visits_via (LCons v0 P) (insert v0 A) W"
proof-
  obtain n where n: "enat n < llength P" "P $ n ∈ W" "lset (ltake (enat n) P) ⊆ A"
    using assms unfolding visits_via_def by blast
  define P' where "P' = LCons v0 P"
  have "enat (Suc n) < llength P'" unfolding P'_def
    by (metis n(1) ldropn_Suc_LCons ldropn_Suc_conv_ldropn ldropn_eq_LConsD)
  moreover have "P' $ Suc n ∈ W" unfolding P'_def by (simp add: n(2))
  moreover have "lset (ltake (enat (Suc n)) P') ⊆ insert v0 A"
    using lset_ltake_Suc[of P' v0 n A] unfolding P'_def by (simp add: n(3))
  ultimately show ?thesis unfolding visits_via_def P'_def by blast
qed

lemma (in vmc_path_no_deadend) visits_via_ltl:
  assumes "visits_via P A W"
    and v0: "v0 ∉ W"
  shows "visits_via (ltl P) A W"
proof-
  obtain n where n: "enat n < llength P" "P $ n ∈ W" "lset (ltake (enat n) P) ⊆ A"
    using assms(1)[unfolded visits_via_def] by blast
  have "n ≠ 0" using v0 n(2) DiffE by force
  then obtain n' where n': "Suc n' = n" using nat.exhaust by metis
  have "∃n. enat n < llength (ltl P) ∧ (ltl P) $ n ∈ W ∧ lset (ltake (enat n) (ltl P)) ⊆ A"
    apply (rule exI[of _ n'])
    using n n' enat_Suc_ltl[of n' P] P_lnth_Suc lset_ltake_ltl[of n' P] by auto
  thus ?thesis using visits_via_def by blast
qed

lemma (in vm_path) visits_via_deadend:
  assumes "visits_via P A (deadends p)"
  shows "winning_path p** P"
  using assms visits_via_visits visits_deadend by blast

subsection ‹Attracting Strategy from a Single Node›

text ‹
  All @{term σ}-paths starting from @{term v0} visit @{term W} and until then they stay in @{term A}.
›
definition strategy_attracts_via :: "Player ⇒ 'a Strategy ⇒ 'a ⇒ 'a set ⇒ 'a set ⇒ bool" where
  "strategy_attracts_via p σ v0 A W ≡ ∀P. vmc_path G P v0 p σ ⟶ visits_via P A W"

lemma (in vmc_path) strategy_attracts_viaE:
  assumes "strategy_attracts_via p σ v0 A W"
  shows "visits_via P A W"
  using strategy_attracts_via_def assms vmc_path_axioms by blast

lemma (in vmc_path) strategy_attracts_via_SucE:
  assumes "strategy_attracts_via p σ v0 A W" "v0 ∉ W"
  shows "∃n. enat (Suc n) < llength P ∧ P $ Suc n ∈ W ∧ lset (ltake (enat (Suc n)) P) ⊆ A"
proof-
  obtain n where n: "enat n < llength P" "P $ n ∈ W" "lset (ltake (enat n) P) ⊆ A"
    using strategy_attracts_viaE[unfolded visits_via_def] assms(1) by blast
  have "n ≠ 0" using assms(2) n(2) by (metis P_0)
  thus ?thesis using n not0_implies_Suc by blast
qed

lemma (in vmc_path) strategy_attracts_via_lset:
  assumes "strategy_attracts_via p σ v0 A W"
  shows "lset P ∩ W ≠ {}"
  using assms[THEN strategy_attracts_viaE, unfolded visits_via_def]
  by (meson disjoint_iff_not_equal lset_lnth_member subset_refl)

lemma strategy_attracts_via_v0:
  assumes σ: "strategy p σ" "strategy_attracts_via p σ v0 A W"
    and v0: "v0 ∈ V"
  shows "v0 ∈ A ∪ W"
proof-
  obtain P where "vmc_path G P v0 p σ" using strategy_conforming_path_exists_single assms by blast
  then interpret vmc_path G P v0 p σ .
  obtain n where n: "enat n < llength P" "P $ n ∈ W" "lset (ltake (enat n) P) ⊆ A"
    using σ(2)[unfolded strategy_attracts_via_def visits_via_def] vmc_path_axioms by blast
  show ?thesis proof (cases "n = 0")
    case True thus ?thesis using n(2) by simp
  next
    case False
    hence "lhd (ltake (enat n) P) = lhd P" by (simp add: enat_0_iff(1))
    hence "v0 ∈ lset (ltake (enat n) P)"
      by (metis ‹n ≠ 0› P_not_null P_v0 enat_0_iff(1) llist.set_sel(1) ltake.disc(2))
    thus ?thesis using n(3) by blast
  qed
qed
corollary strategy_attracts_not_outside:
  "⟦ v0 ∈ V - A - W; strategy p σ ⟧ ⟹ ¬strategy_attracts_via p σ v0 A W"
  using strategy_attracts_via_v0 by blast


lemma strategy_attracts_viaI [intro]:
  assumes "⋀P. vmc_path G P v0 p σ ⟹ visits_via P A W"
  shows "strategy_attracts_via p σ v0 A W"
  unfolding strategy_attracts_via_def using assms by blast

lemma strategy_attracts_via_no_deadends:
  assumes "v ∈ V" "v ∈ A - W" "strategy_attracts_via p σ v A W"
  shows "¬deadend v"
proof
  assume "deadend v"
  define P where [simp]: "P = LCons v LNil"
  interpret vmc_path G P v p σ proof
    show "valid_path P" using ‹v ∈ A - W› ‹v ∈ V› valid_path_base' by auto
    show "maximal_path P" using ‹deadend v› by (simp add: maximal_path.intros(2))
    show "path_conforms_with_strategy p P σ" by (simp add: path_conforms_LCons_LNil)
  qed simp_all
  have "visits_via P A W" using assms(3) strategy_attracts_viaE by blast
  moreover have "llength P = eSuc 0" by simp
  ultimately have "P $ 0 ∈ W" by (simp add: enat_0_iff(1) visits_via_def)
  with ‹v ∈ A - W› show False by auto
qed

lemma attractor_strategy_on_extends:
  "⟦ strategy_attracts_via p σ v0 A W; A ⊆ A' ⟧ ⟹ strategy_attracts_via p σ v0 A' W"
  unfolding strategy_attracts_via_def using visits_via_monotone by blast

lemma strategy_attracts_via_trivial: "v0 ∈ W ⟹ strategy_attracts_via p σ v0 A W"
proof
  fix P assume "v0 ∈ W" "vmc_path G P v0 p σ"
  then interpret vmc_path G P v0 p σ by blast
  show "visits_via P A W" using visits_via_trivial using ‹v0 ∈ W› by blast
qed

lemma strategy_attracts_via_successor:
  assumes σ: "strategy p σ" "strategy_attracts_via p σ v0 A W"
    and v0: "v0 ∈ A - W"
    and w0: "v0→w0" "v0 ∈ VV p ⟹ σ v0 = w0"
  shows "strategy_attracts_via p σ w0 A W"
proof
  fix P assume "vmc_path G P w0 p σ"
  then interpret vmc_path G P w0 p σ .
  define P' where [simp]: "P' = LCons v0 P"
  then interpret P': vmc_path G P' v0 p σ
    using extension_valid_maximal_conforming w0 by blast
  interpret P': vmc_path_no_deadend G P' v0 p σ using ‹v0→w0› by unfold_locales blast
  have "visits_via P' A W" using σ(2) P'.strategy_attracts_viaE by blast
  thus "visits_via P A W" using P'.visits_via_ltl v0 by simp
qed

lemma strategy_attracts_VVp:
  assumes σ: "strategy p σ" "strategy_attracts_via p σ v0 A W"
    and v: "v0 ∈ A - W" "v0 ∈ VV p" "¬deadend v0"
  shows "σ v0 ∈ A ∪ W"
proof-
  have "v0→σ v0" using σ(1)[unfolded strategy_def] v(2,3) by blast
  hence "strategy_attracts_via p σ (σ v0) A W"
    using strategy_attracts_via_successor σ v(1) by blast
  thus ?thesis using strategy_attracts_via_v0 ‹v0→σ v0› σ(1) by blast
qed

lemma strategy_attracts_VVpstar:
  assumes "strategy p σ" "strategy_attracts_via p σ v0 A W"
    and "v0 ∈ A - W" "v0 ∉ VV p" "w0 ∈ V - A - W"
  shows "¬v0 → w0"
  by (metis assms strategy_attracts_not_outside strategy_attracts_via_successor)

subsection ‹Attracting strategy from a set of nodes›

text ‹
  All @{term σ}-paths starting from @{term A} visit @{term W} and until then they stay in @{term A}.
›
definition strategy_attracts :: "Player ⇒ 'a Strategy ⇒ 'a set ⇒ 'a set ⇒ bool" where
  "strategy_attracts p σ A W ≡ ∀v0 ∈ A. strategy_attracts_via p σ v0 A W"

lemma (in vmc_path) strategy_attractsE:
  assumes "strategy_attracts p σ A W" "v0 ∈ A"
  shows "visits_via P A W"
  using assms(1)[unfolded strategy_attracts_def] assms(2) strategy_attracts_viaE by blast

lemma strategy_attractsI [intro]:
  assumes "⋀P v. ⟦ v ∈ A; vmc_path G P v p σ ⟧ ⟹ visits_via P A W"
  shows "strategy_attracts p σ A W"
  unfolding strategy_attracts_def using assms by blast

lemma (in vmc_path) strategy_attracts_lset:
  assumes "strategy_attracts p σ A W" "v0 ∈ A"
  shows "lset P ∩ W ≠ {}"
  using assms(1)[unfolded strategy_attracts_def] assms(2) strategy_attracts_via_lset(1)[of A W]
  by blast

lemma strategy_attracts_empty [simp]: "strategy_attracts p σ {} W" by blast

lemma strategy_attracts_invalid_path:
  assumes P: "P = LCons v (LCons w P')" "v ∈ A - W" "w ∉ A ∪ W"
  shows "¬visits_via P A W" (is "¬?A")
proof
  assume ?A
  then obtain n where n: "enat n < llength P" "P $ n ∈ W" "lset (ltake (enat n) P) ⊆ A"
    unfolding visits_via_def by blast
  have "n ≠ 0" using ‹v ∈ A - W› n(2) P(1) DiffD2 by force
  moreover have "n ≠ Suc 0" using ‹w ∉ A ∪ W› n(2) P(1) by auto
  ultimately have "Suc (Suc 0) ≤ n" by presburger
  hence "lset (ltake (enat (Suc (Suc 0))) P) ⊆ A" using n(3)
    by (meson contra_subsetD enat_ord_simps(1) lset_ltake_prefix lset_lnth_member lset_subset)
  moreover have "enat (Suc 0) < llength (ltake (eSuc (eSuc 0)) P)" proof-
    have *: "enat (Suc (Suc 0)) < llength P"
      using ‹Suc (Suc 0) ≤ n› n(1) by (meson enat_ord_simps(2) le_less_linear less_le_trans neq_iff)
    have "llength (ltake (enat (Suc (Suc 0))) P) = min (enat (Suc (Suc 0))) (llength P)" by simp
    hence "llength (ltake (enat (Suc (Suc 0))) P) = enat (Suc (Suc 0))"
      using * by (simp add: min_absorb1)
    thus ?thesis by (simp add: eSuc_enat zero_enat_def)
  qed
  ultimately have "ltake (enat (Suc (Suc 0))) P $ Suc 0 ∈ A" by (simp add: lset_lnth_member)
  hence "P $ Suc 0 ∈ A" by (simp add: lnth_ltake)
  thus False using P(1,3) by auto
qed

text ‹
  If @{term A} is an attractor set of @{term W} and an edge leaves @{term A} without going through
  @{term W}, then @{term v} belongs to @{term "VV p"} and the attractor strategy @{term σ} avoids
  this edge.  All other cases give a contradiction.
›
lemma strategy_attracts_does_not_leave:
  assumes σ: "strategy_attracts p σ A W" "strategy p σ"
    and v: "v→w" "v ∈ A - W" "w ∉ A ∪ W"
  shows "v ∈ VV p ∧ σ v ≠ w"
proof (rule ccontr)
  assume contra: "¬(v ∈ VV p ∧ σ v ≠ w)"
  (* Define a strategy for p** which tries to take this edge. *)
  define σ' where "σ' = σ_arbitrary(v := w)"
  hence "strategy p** σ'" using ‹v→w› by (simp add: valid_strategy_updates)
  then obtain P where P: "vmc2_path G P v p σ σ'"
    using ‹v→w› strategy_conforming_path_exists σ(2) by blast
  then interpret vmc2_path G P v p σ σ' .
  interpret vmc_path_no_deadend G P v p σ using ‹v→w› by unfold_locales blast
  interpret comp: vmc_path_no_deadend G P v "p**" σ' using ‹v→w› by unfold_locales blast
  have "w = w0" using contra σ'_def v0_conforms comp.v0_conforms by (cases "v ∈ VV p") auto
  hence "¬visits_via P A W"
    using strategy_attracts_invalid_path[of P v w "ltl (ltl P)"] v(2,3) P_LCons' by simp
  thus False by (meson DiffE σ(1) strategy_attractsE v(2))
qed

text ‹
  Given an attracting strategy @{term σ}, we can turn every strategy @{term σ'} into an attracting
  strategy by overriding @{term σ'} on a suitable subset of the nodes.  This also means that
  an attracting strategy is still attracting if we override it outside of @{term "A - W"}.
›
lemma strategy_attracts_irrelevant_override:
  assumes "strategy_attracts p σ A W" "strategy p σ" "strategy p σ'"
  shows "strategy_attracts p (override_on σ' σ (A - W)) A W"
proof (rule strategy_attractsI, rule ccontr)
  fix P v
  let ?σ = "override_on σ' σ (A - W)"
  assume "vmc_path G P v p ?σ"
  then interpret vmc_path G P v p ?σ .
  assume "v ∈ A"
  hence "P $ 0 ∈ A" using ‹v ∈ A› by simp
  moreover assume contra: "¬visits_via P A W"
  ultimately have "P $ 0 ∈ A - W" unfolding visits_via_def by (meson DiffI P_len not_less0 lset_ltake)
  have "¬lset P ⊆ A - W" proof
    assume "lset P ⊆ A - W"
    hence "⋀v. v ∈ lset P ⟹ override_on σ' σ (A - W) v = σ v" by auto
    hence "path_conforms_with_strategy p P σ"
      using path_conforms_with_strategy_irrelevant_updates[OF P_conforms] by blast
    hence "vmc_path G P (P $ 0) p σ"
      using conforms_to_another_strategy P_0 by blast
    thus False
      using contra ‹P $ 0 ∈ A› assms(1)
      by (meson vmc_path.strategy_attractsE)
  qed
  hence "∃n. enat n < llength P ∧ P $ n ∉ A - W" by (meson lset_subset)
  then obtain n where n: "enat n < llength P ∧ P $ n ∉ A - W"
    "⋀i. i < n ⟹ ¬(enat i < llength P ∧ P $ i ∉ A - W)"
    using ex_least_nat_le[of "λn. enat n < llength P ∧ P $ n ∉ A - W"] by blast
  hence n_min: "⋀i. i < n ⟹ P $ i ∈ A - W"
    using dual_order.strict_trans enat_ord_simps(2) by blast
  have "n ≠ 0" using ‹P $ 0 ∈ A - W› n(1) by meson
  then obtain n' where n': "Suc n' = n" using not0_implies_Suc by blast
  hence "P $ n' ∈ A - W" using n_min by blast
  moreover have "P $ n' → P $ Suc n'" using P_valid n(1) n' valid_path_edges by blast
  moreover have "P $ Suc n' ∉ A ∪ W" proof-
    have "P $ n ∉ W" using contra n(1) n_min unfolding visits_via_def
      by (meson Diff_subset lset_ltake subsetCE)
    thus ?thesis using n(1) n' by blast
  qed
  ultimately have "P $ n' ∈ VV p ∧ σ (P $ n') ≠ P $ Suc n'"
    using strategy_attracts_does_not_leave[of p σ A W "P $ n'" "P $ Suc n'"]
          assms(1,2) by blast
  thus False
    using n(1) n' vmc_path_conforms ‹P $ n' ∈ A - W› by (metis override_on_apply_in)
qed

lemma strategy_attracts_trivial [simp]: "strategy_attracts p σ W W"
  by (simp add: strategy_attracts_def strategy_attracts_via_trivial)

text ‹If a @{term σ}-conforming path @{term P} hits an attractor @{term A}, it will visit @{term W}.›
lemma (in vmc_path) attracted_path:
  assumes "W ⊆ V"
    and σ: "strategy_attracts p σ A W"
    and P_hits_A: "lset P ∩ A ≠ {}"
  shows "lset P ∩ W ≠ {}"
proof-
  obtain n where n: "enat n < llength P" "P $ n ∈ A" using P_hits_A by (meson lset_intersect_lnth)
  define P' where "P' = ldropn n P"
  interpret vmc_path G P' "P $ n" p σ unfolding P'_def using vmc_path_ldropn n(1) by blast
  have "visits_via P' A W" using σ n(2) strategy_attractsE by blast
  thus ?thesis unfolding P'_def using visits_via_visits in_lset_ldropnD[of _ n P] by blast
qed

lemma attracted_strategy_step:
  assumes σ: "strategy p σ" "strategy_attracts p σ A W"
    and v0: "¬deadend v0" "v0 ∈ A - W" "v0 ∈ VV p"
  shows "σ v0 ∈ A ∪ W"
  by (metis DiffD1 strategy_attracts_VVp assms strategy_attracts_def)

lemma (in vmc_path_no_deadend) attracted_path_step:
  assumes σ: "strategy_attracts p σ A W"
    and v0: "v0 ∈ A - W"
  shows "w0 ∈ A ∪ W"
  by (metis (no_types) DiffD1 P_LCons' σ strategy_attractsE strategy_attracts_invalid_path v0)

end ― ‹context ParityGame›

end