Theory AttractorInductive

section ‹Defining the Attractor with \texttt{inductive\_set}›

theory AttractorInductive
imports
  Main
  Attractor
begin

context ParityGame begin

text ‹
  In section \ref{sec:attractor} we defined @{const attractor} manually via @{const lfp}.
  We can also define it with \texttt{inductive\_set}.  In this section, we do exactly this and
  prove that the new definition yields the same set as the old definition.
›

subsection ‹@{term attractor_inductive}›

text ‹The attractor set of a given set of nodes, defined inductively.›
inductive_set attractor_inductive :: "Player ⇒ 'a set ⇒ 'a set"
  for p :: Player and W :: "'a set" where
  Base [intro!]: "v ∈ W ⟹ v ∈ attractor_inductive p W"
| VVp: "⟦ v ∈ VV p; ∃w. v→w ∧ w ∈ attractor_inductive p W ⟧
    ⟹ v ∈ attractor_inductive p W"
| VVpstar: "⟦ v ∈ VV p**; ¬deadend v; ∀w. v→w ⟶ w ∈ attractor_inductive p W ⟧
    ⟹ v ∈ attractor_inductive p W"

text ‹
  We show that the inductive definition and the definition via least fixed point are the same.
›
lemma attractor_inductive_is_attractor:
  assumes "W ⊆ V"
  shows "attractor_inductive p W = attractor p W"
proof
  show "attractor_inductive p W ⊆ attractor p W" proof
    fix v assume "v ∈ attractor_inductive p W"
    thus "v ∈ attractor p W" proof (induct rule: attractor_inductive.induct)
      case (Base v) thus ?case using attractor_set_base by auto
    next
      case (VVp v) thus ?case using attractor_set_VVp by auto
    next
      case (VVpstar v) thus ?case using attractor_set_VVpstar by auto
    qed
  qed
  show "attractor p W ⊆ attractor_inductive p W"
  proof-
    define P where "P S ⟷ S ⊆ attractor_inductive p W" for S
    from ‹W ⊆ V› have "P (attractor p W)" proof (induct rule: attractor_set_induction)
      case (step S)
      hence "S ⊆ attractor_inductive p W" using P_def by simp
      have "W ∪ S ∪ directly_attracted p S ⊆ attractor_inductive p W" proof
        fix v assume "v ∈ W ∪ S ∪ directly_attracted p S"
        moreover
        { assume "v ∈ W" hence "v ∈ attractor_inductive p W" by blast }
        moreover
        { assume "v ∈ S" hence "v ∈ attractor_inductive p W"
            by (meson ‹S ⊆ attractor_inductive p W› rev_subsetD) }
        moreover
        { assume v_attracted: "v ∈ directly_attracted p S"
          hence "v ∈ V" using ‹S ⊆ V› attractor_step_bounded_by_V by blast
          hence "v ∈ attractor_inductive p W" proof (cases rule: VV_cases)
            assume "v ∈ VV p"
            hence "∃w. v→w ∧ w ∈ S" using v_attracted directly_attracted_def by blast
            hence "∃w. v→w ∧ w ∈ attractor_inductive p W"
              using ‹S ⊆ attractor_inductive p W› by blast
            thus ?thesis by (simp add: ‹v ∈ VV p› attractor_inductive.VVp)
          next
            assume "v ∈ VV p**"
            hence *: "∀w. v→w ⟶ w ∈ S" using v_attracted directly_attracted_def by blast
            have "¬deadend v" using v_attracted directly_attracted_def by blast
            show ?thesis proof (rule ccontr)
              assume "v ∉ attractor_inductive p W"
              hence "∃w. v→w ∧ w ∉ attractor_inductive p W"
                by (metis attractor_inductive.VVpstar ‹v ∈ VV p**› ‹¬deadend v›)
              hence "∃w. v→w ∧ w ∉ S" using ‹S ⊆ attractor_inductive p W› by (meson subsetCE)
              thus False using * by blast
            qed
          qed
        }
        ultimately show "v ∈ attractor_inductive p W" by (meson UnE)
      qed
      thus "P (W ∪ S ∪ directly_attracted p S)" using P_def by simp
    qed (simp add: P_def Sup_least)
    thus ?thesis using P_def by simp
  qed
qed

end

end