Theory Attractor

section ‹Attractor Sets›
text ‹\label{sec:attractor}›

theory Attractor
imports
  Main
  AttractingStrategy
begin

text ‹Here we define the @{term p}-attractor of a set of nodes.›

context ParityGame begin

text ‹We define the conditions for a node to be directly attracted from a given set.›
definition directly_attracted :: "Player ⇒ 'a set ⇒ 'a set" where
  "directly_attracted p S ≡ {v ∈ V - S. ¬deadend v ∧
      (v ∈ VV p   ⟶ (∃w. v→w ∧ w ∈ S))
    ∧ (v ∈ VV p** ⟶ (∀w. v→w ⟶ w ∈ S))}"

abbreviation "attractor_step p W S ≡ W ∪ S ∪ directly_attracted p S"

text ‹The ‹p›-attractor set of ‹W›, defined as a least fixed point.›
definition attractor :: "Player ⇒ 'a set ⇒ 'a set" where
  "attractor p W = lfp (attractor_step p W)"

subsection ‹@{const directly_attracted}›

text ‹Show a few basic properties of @{const directly_attracted}.›
lemma directly_attracted_disjoint     [simp]: "directly_attracted p W ∩ W = {}"
  and directly_attracted_empty        [simp]: "directly_attracted p {} = {}"
  and directly_attracted_V_empty      [simp]: "directly_attracted p V = {}"
  and directly_attracted_bounded_by_V [simp]: "directly_attracted p W ⊆ V"
  and directly_attracted_contains_no_deadends [elim]: "v ∈ directly_attracted p W ⟹ ¬deadend v"
  unfolding directly_attracted_def by blast+

subsection ‹‹attractor_step››

lemma attractor_step_empty: "attractor_step p {} {} = {}"
  and attractor_step_bounded_by_V: "⟦ W ⊆ V; S ⊆ V ⟧ ⟹ attractor_step p W S ⊆ V"
  by simp_all

text ‹
  The definition of @{const attractor} uses @{const lfp}.  For this to be well-defined, we
  need show that ‹attractor_step› is monotone.
›

lemma attractor_step_mono: "mono (attractor_step p W)"
  unfolding directly_attracted_def by (rule monoI) auto

subsection ‹Basic Properties of an Attractor›

lemma attractor_unfolding: "attractor p W = attractor_step p W (attractor p W)"
  unfolding attractor_def using attractor_step_mono lfp_unfold by blast
lemma attractor_lowerbound: "attractor_step p W S ⊆ S ⟹ attractor p W ⊆ S"
  unfolding attractor_def using attractor_step_mono by (simp add: lfp_lowerbound)
lemma attractor_set_non_empty: "W ≠ {} ⟹ attractor p W ≠ {}"
  and attractor_set_base: "W ⊆ attractor p W"
  using attractor_unfolding by auto
lemma attractor_in_V: "W ⊆ V ⟹ attractor p W ⊆ V"
  using attractor_lowerbound attractor_step_bounded_by_V by auto

subsection ‹Attractor Set Extensions›

lemma attractor_set_VVp:
  assumes "v ∈ VV p" "v→w" "w ∈ attractor p W"
  shows "v ∈ attractor p W"
  apply (subst attractor_unfolding) unfolding directly_attracted_def using assms by auto

lemma attractor_set_VVpstar:
  assumes "¬deadend v" "⋀w. v→w ⟹ w ∈ attractor p W"
  shows "v ∈ attractor p W"
  apply (subst attractor_unfolding) unfolding directly_attracted_def using assms by auto

subsection ‹Removing an Attractor›

lemma removing_attractor_induces_no_deadends:
  assumes "v ∈ S - attractor p W" "v→w" "w ∈ S" "⋀w. ⟦ v ∈ VV p**; v→w ⟧ ⟹ w ∈ S"
  shows "∃w ∈ S - attractor p W. v→w"
proof-
  have "v ∈ V" using ‹v→w› by blast
  thus ?thesis proof (cases rule: VV_cases)
    assume "v ∈ VV p"
    thus ?thesis using attractor_set_VVp assms by blast
  next
    assume "v ∈ VV p**"
    thus ?thesis using attractor_set_VVpstar assms by (metis Diff_iff edges_are_in_V(2))
  qed
qed

text ‹Removing the attractor sets of deadends leaves a subgame without deadends.›

lemma subgame_without_deadends:
  assumes V'_def: "V' = V - attractor p (deadends p**) - attractor p** (deadends p****)"
    (is "V' = V - ?A - ?B")
    and v: "v ∈ V⇘subgame V'⇙"
  shows "¬Digraph.deadend (subgame V') v"
proof (cases)
  assume "deadend v"
  have v: "v ∈ V - ?A - ?B" using v unfolding V'_def subgame_def by simp
  { fix p' assume "v ∈ VV p'**"
    hence "v ∈ attractor p' (deadends p'**)"
      using ‹deadend v› attractor_set_base[of "deadends p'**" p']
      unfolding deadends_def by blast
    hence False using v by (cases p'; cases p) auto
  }
  thus ?thesis using v by blast
next
  assume "¬deadend v"
  have v: "v ∈ V - ?A - ?B" using v unfolding V'_def subgame_def by simp
  define G' where "G' = subgame V'"
  interpret G': ParityGame G' unfolding G'_def using subgame_ParityGame .
  show ?thesis proof
    assume "Digraph.deadend (subgame V') v"
    hence "G'.deadend v" unfolding G'_def .
    have all_in_attractor: "⋀w. v→w ⟹ w ∈ ?A ∨ w ∈ ?B" proof (rule ccontr)
      fix w
      assume "v→w" "¬(w ∈ ?A ∨ w ∈ ?B)"
      hence "w ∈ V'" unfolding V'_def by blast
      hence "w ∈ V⇘G'⇙" unfolding G'_def subgame_def using ‹v→w› by auto
      hence "v →⇘G'⇙ w" using ‹v→w› assms(2) unfolding G'_def subgame_def by auto
      thus False using ‹G'.deadend v› using ‹w ∈ V⇘G'⇙› by blast
    qed
    { fix p' assume "v ∈ VV p'"
      { assume "∃w. v→w ∧ w ∈ attractor p' (deadends p'**)"
        hence "v ∈ attractor p' (deadends p'**)" using ‹v ∈ VV p'› attractor_set_VVp by blast
        hence False using v by (cases p'; cases p) auto
      }
      hence "⋀w. v→w ⟹ w ∈ attractor p'** (deadends p'****)"
        using all_in_attractor by (cases p'; cases p) auto
      hence "v ∈ attractor p'** (deadends p'****)"
        using ‹¬deadend v› ‹v ∈ VV p'› attractor_set_VVpstar by auto
      hence False using v by (cases p'; cases p) auto
    }
    thus False using v by blast
  qed
qed

subsection ‹Attractor Set Induction›

lemma mono_restriction_is_mono: "mono f ⟹ mono (λS. f (S ∩ V))"
  unfolding mono_def by (meson inf_mono monoD subset_refl)

text ‹
  Here we prove a powerful induction schema for @{term attractor}.  Being able to prove this is the
  only reason why we do not use \texttt{inductive\_set} to define the attractor set.

  See also \url{https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2015-October/msg00123.html}
›
lemma attractor_set_induction [consumes 1, case_names step union]:
  assumes "W ⊆ V"
    and step: "⋀S. S ⊆ V ⟹ P S ⟹ P (attractor_step p W S)"
    and union: "⋀M. ∀S ∈ M. S ⊆ V ∧ P S ⟹ P (⋃M)"
  shows "P (attractor p W)"
proof-
  let ?P = "λS. P (S ∩ V)"
  let ?f = "λS. attractor_step p W (S ∩ V)"
  let ?A = "lfp ?f"
  let ?B = "lfp (attractor_step p W)"
  have f_mono: "mono ?f"
    using mono_restriction_is_mono[of "attractor_step p W"] attractor_step_mono by simp
  have P_A: "?P ?A" proof (rule lfp_ordinal_induct_set)
    show "⋀S. ?P S ⟹ ?P (W ∪ (S ∩ V) ∪ directly_attracted p (S ∩ V))"
      by (metis assms(1) attractor_step_bounded_by_V inf.absorb1 inf_le2 local.step)
    show "⋀M. ∀S ∈ M. ?P S ⟹ ?P (⋃M)" proof-
      fix M
      let ?M = "{S ∩ V | S. S ∈ M}"
      assume "∀S∈M. ?P S"
      hence "∀S ∈ ?M. S ⊆ V ∧ P S" by auto
      hence *: "P (⋃?M)" by (simp add: union)
      have "⋃?M = (⋃M) ∩ V" by blast
      thus "?P (⋃M)" using * by auto
    qed
  qed (insert f_mono)

  have *: "W ∪ (V ∩ V) ∪ directly_attracted p (V ∩ V) ⊆ V"
    using ‹W ⊆ V› attractor_step_bounded_by_V by auto
  have "?A ⊆ V" "?B ⊆ V" using * by (simp_all add: lfp_lowerbound)

  have "?A = ?f ?A" using f_mono lfp_unfold by blast
  hence "?A = W ∪ (?A ∩ V) ∪ directly_attracted p (?A ∩ V)" using ‹?A ⊆ V› by simp
  hence *: "attractor_step p W ?A ⊆ ?A" using ‹?A ⊆ V› inf.absorb1 by fastforce

  have "?B = attractor_step p W ?B" using attractor_step_mono lfp_unfold by blast
  hence "?f ?B ⊆ ?B" using ‹?B ⊆ V› by (metis (no_types, lifting) equalityD2 le_iff_inf)

  have "?A = ?B" proof
    show "?A ⊆ ?B" using ‹?f ?B ⊆ ?B› by (simp add: lfp_lowerbound)
    show "?B ⊆ ?A" using * by (simp add: lfp_lowerbound)
  qed
  hence "?P ?B" using P_A by (simp add: attractor_def)
  thus ?thesis using ‹?B ⊆ V› by (simp add: attractor_def le_iff_inf)
qed

end ― ‹context ParityGame›

end