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 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'" unfolding G'_
def subgame_def
using ‹v→w› by auto
hence "v →' w" using ‹v→w› assms(
2)
unfolding G'_
def subgame_def
by auto
thus False
using ‹G'.deadend v› using ‹w ∈ V'› 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
