Quelle  Strategy.thy

section ‹Positional Strategies›

theory Strategy
imports
  Main
  ParityGame
begin

subsection ‹Definitions›

text ‹
 A \emph{strategy} is simply a function from nodes to nodes
 We only consider positional strategies.
 ›
type_synonym 'a Strategy = "'a ==> 'a"

text ‹
 A \emph{valid} strategy for player @{term p} is a function assigning a successor to each node
 in @{term "VV p"}.›
definition (in ParityGame) strategy :: "Player ==> 'a Strategy ==> bool" where
  "strategy p σ ≡ ∀v ∈ VV p. ¬deadend v ⟶ v→σ v"

lemma (in ParityGame) strategyI [intro]:
  "(∧v. [ v ∈ VV p; ¬deadend v ] ==> v→σ v) ==> strategy p σ"
  unfolding strategy_def by blast

subsection ‹Strategy-Conforming Paths›

text ‹
 If @{term "path_conforms_with_strategy p P σ"} holds, then we call @{term P} a
 \emph{@{term σ}-path}.
 This means that @{term P} follows @{term σ} on all nodes of player @{term p}
 except maybe the last node on the path.
 ›
coinductive (in ParityGame) path_conforms_with_strategy
  :: "Player ==> 'a Path ==> 'a Strategy ==> bool" where
  path_conforms_LNil:  "path_conforms_with_strategy p LNil σ"
| path_conforms_LCons_LNil: "path_conforms_with_strategy p (LCons v LNil) σ"
| path_conforms_VVp: "[ v ∈ VV p; w = σ v; path_conforms_with_strategy p (LCons w Ps) σ ]
    ==> path_conforms_with_strategy p (LCons v (LCons w Ps)) σ"
| path_conforms_VVpstar: "[ v ∉ VV p; path_conforms_with_strategy p Ps σ ]
    ==> path_conforms_with_strategy p (LCons v Ps) σ"

text ‹
 Define a locale for valid maximal paths that conform to a given strategy, because we need
 this concept quite often. However, we are not yet able to add interesting lemmas to this locale.
 We will do this at the end of this section, where we have more lemmas available.
 ›
locale vmc_path = vm_path +
  fixes p σ assumes P_conforms [simp]: "path_conforms_with_strategy p P σ"

text ‹
 Similary, define a locale for valid maximal paths that conform to given strategies for both
 players.
 ›
locale vmc2_path = comp?: vmc_path G P v0 "p**" σ' + vmc_path G P v0 p σ
  for G P v0 p σ σ'


subsection ‹An Arbitrary Strategy›

context ParityGame begin

text ‹
 Define an arbitrary strategy. This is useful to define other strategies by overriding part of
 this strategy.
 ›
definition "σ_arbitrary ≡ λv. SOME w. v→w"

lemma valid_arbitrary_strategy [simp]: "strategy p σ_arbitrary" proof
  fix v assume "¬deadend v"
  thus "v → σ_arbitrary v" unfolding σ_arbitrary_def using someI_ex[of "λw. v→w"] by blast
qed

subsection ‹Valid Strategies›

lemma valid_strategy_updates: "[ strategy p σ; v0→w0 ] ==> strategy p (σ(v0 := w0))"
  unfolding strategy_def by auto

lemma valid_strategy_updates_set:
  assumes "strategy p σ" "∧v. [ v ∈ A; v ∈ VV p; ¬deadend v ] ==> v→σ' v"
  shows "strategy p (override_on σ σ' A)"
  unfolding strategy_def by (metis assms override_on_def strategy_def)

lemma valid_strategy_updates_set_strong:
  assumes "strategy p σ" "strategy p σ'"
  shows "strategy p (override_on σ σ' A)"
  using assms(1) assms(2)[unfolded strategy_def] valid_strategy_updates_set by simp

lemma subgame_strategy_stays_in_subgame:
  assumes σ: "ParityGame.strategy (subgame V') p σ"
    and "v ∈ ParityGame.VV (subgame V') p" "¬Digraph.deadend (subgame V') v"
  shows "σ v ∈ V'"
proof-
  interpret G': ParityGame "subgame V'" using subgame_ParityGame .
  have "σ v ∈ V _V'" using assms unfolding G'.strategy_def G'.edges_are_in_V(2) by blast
  thus "σ v ∈ V'" by (metis Diff_iff IntE subgame_VV Player.distinct(2))
qed

lemma valid_strategy_supergame:
  assumes σ: "strategy p σ"
    and σ': "ParityGame.strategy (subgame V') p σ'"
    and G'_no_deadends: "∧v. v ∈ V' ==> ¬Digraph.deadend (subgame V') v"
  shows "strategy p (override_on σ σ' V')" (is "strategy p ?σ")
proof
  interpret G': ParityGame "subgame V'" using subgame_ParityGame .
  fix v assume v: "v ∈ VV p" "¬deadend v"
  show "v → ?σ v" proof (cases)
    assume "v ∈ V'"
    hence "v ∈ G'.VV p" using subgame_VV ‹v ∈ VV p› by blast
    moreover have "¬G'.deadend v" using G'_no_deadends ‹v ∈ V'› by blast
    ultimately have "v → _V' σ' v" using σ' unfolding G'.strategy_def by blast
    moreover have "σ' v = ?σ v" using ‹v ∈ V'› by simp
    ultimately show ?thesis by (metis subgame_E subsetCE)
  next
    assume "v ∉ V'"
    thus ?thesis using v σ unfolding strategy_def by simp
  qed
qed

lemma valid_strategy_in_V: "[ strategy p σ; v ∈ VV p; ¬deadend v ] ==> σ v ∈ V"
  unfolding strategy_def using valid_edge_set by auto

lemma valid_strategy_only_in_V: "[ strategy p σ; ∧v. v ∈ V ==> σ v = σ' v ] ==> strategy p σ'"
  unfolding strategy_def using edges_are_in_V(1) by auto

subsection ‹Conforming Strategies›

lemma path_conforms_with_strategy_ltl [intro]:
  "path_conforms_with_strategy p P σ ==> path_conforms_with_strategy p (ltl P) σ"
  by (drule path_conforms_with_strategy.cases) (simp_all add: path_conforms_with_strategy.intros(1))

lemma path_conforms_with_strategy_drop:
  "path_conforms_with_strategy p P σ ==> path_conforms_with_strategy p (ldropn n P) σ"
  by (simp add: path_conforms_with_strategy_ltl ltl_ldrop[of "λP. path_conforms_with_strategy p P σ"])

lemma path_conforms_with_strategy_prefix:
  "path_conforms_with_strategy p P σ ==> lprefix P' P ==> path_conforms_with_strategy p P' σ"
proof (coinduction arbitrary: P P')
  case (path_conforms_with_strategy P P')
  thus ?case proof (cases rule: path_conforms_with_strategy.cases)
    case path_conforms_LNil
    thus ?thesis using path_conforms_with_strategy(2) by auto
  next
    case path_conforms_LCons_LNil
    thus ?thesis by (metis lprefix_LCons_conv lprefix_antisym lprefix_code(1) path_conforms_with_strategy(2))
  next
    case (path_conforms_VVp v w)
    thus ?thesis proof (cases)
      assume "P' ≠ LNil ∧ P' ≠ LCons v LNil"
      hence "∃Q. P' = LCons v (LCons w Q)"
        by (metis local.path_conforms_VVp(1) lprefix_LCons_conv path_conforms_with_strategy(2))
      thus ?thesis using local.path_conforms_VVp(1,3,4) path_conforms_with_strategy(2) by force
    qed auto
  next
    case (path_conforms_VVpstar v)
    thus ?thesis proof (cases)
      assume "P' ≠ LNil"
      hence "∃Q. P' = LCons v Q"
        using local.path_conforms_VVpstar(1) lprefix_LCons_conv path_conforms_with_strategy(2) by fastforce
      thus ?thesis using local.path_conforms_VVpstar path_conforms_with_strategy(2) by auto
    qed simp
  qed
qed

lemma path_conforms_with_strategy_irrelevant:
  assumes "path_conforms_with_strategy p P σ" "v ∉ lset P"
  shows "path_conforms_with_strategy p P (σ(v := w))"
  using assms apply (coinduction arbitrary: P) by (drule path_conforms_with_strategy.cases) auto

lemma path_conforms_with_strategy_irrelevant_deadend:
  assumes "path_conforms_with_strategy p P σ" "deadend v ∨ v ∉ VV p" "valid_path P"
  shows "path_conforms_with_strategy p P (σ(v := w))"
using assms proof (coinduction arbitrary: P)
  let ?σ = "σ(v := w)"
  case (path_conforms_with_strategy P)
  thus ?case proof (cases rule: path_conforms_with_strategy.cases)
    case (path_conforms_VVp v' w Ps)
    have "w = ?σ v'" proof-
      from ‹valid_path P› have "¬deadend v'"
        using local.path_conforms_VVp(1) valid_path_cons_simp by blast
      with assms(2) have "v' ≠ v" using local.path_conforms_VVp(2) by blast
      thus "w = ?σ v'" by (simp add: local.path_conforms_VVp(3))
    qed
    moreover
      have "∃P. LCons w Ps = P ∧ path_conforms_with_strategy p P σ ∧ (deadend v ∨ v ∉ VV p) ∧ valid_path P"
    proof-
      have "valid_path (LCons w Ps)"
        using local.path_conforms_VVp(1) path_conforms_with_strategy(3) valid_path_ltl' by blast
      thus ?thesis using local.path_conforms_VVp(4) path_conforms_with_strategy(2) by blast
    qed
    ultimately show ?thesis using local.path_conforms_VVp(1,2) by blast
  next
    case (path_conforms_VVpstar v' Ps)
    have "∃P. path_conforms_with_strategy p Ps σ ∧ (deadend v ∨ v ∉ VV p) ∧ valid_path Ps"
      using local.path_conforms_VVpstar(1,3) path_conforms_with_strategy(2,3) valid_path_ltl' by blast
    thus ?thesis by (simp add: local.path_conforms_VVpstar(1,2))
  qed simp_all
qed

lemma path_conforms_with_strategy_irrelevant_updates:
  assumes "path_conforms_with_strategy p P σ" "∧v. v ∈ lset P ==> σ v = σ' v"
  shows "path_conforms_with_strategy p P σ'"
using assms proof (coinduction arbitrary: P)
  case (path_conforms_with_strategy P)
  thus ?case proof (cases rule: path_conforms_with_strategy.cases)
    case (path_conforms_VVp v' w Ps)
    have "w = σ' v'" using local.path_conforms_VVp(1,3) path_conforms_with_strategy(2) by auto
    thus ?thesis using local.path_conforms_VVp(1,4) path_conforms_with_strategy(2) by auto
  qed simp_all
qed

lemma path_conforms_with_strategy_irrelevant':
  assumes "path_conforms_with_strategy p P (σ(v := w))" "v ∉ lset P"
  shows "path_conforms_with_strategy p P σ"
  by (metis assms fun_upd_triv fun_upd_upd path_conforms_with_strategy_irrelevant)

lemma path_conforms_with_strategy_irrelevant_deadend':
  assumes "path_conforms_with_strategy p P (σ(v := w))" "deadend v ∨ v ∉ VV p" "valid_path P"
  shows "path_conforms_with_strategy p P σ"
  by (metis assms fun_upd_triv fun_upd_upd path_conforms_with_strategy_irrelevant_deadend)

lemma path_conforms_with_strategy_start:
  "path_conforms_with_strategy p (LCons v (LCons w P)) σ ==> v ∈ VV p ==> σ v = w"
  by (drule path_conforms_with_strategy.cases) simp_all

lemma path_conforms_with_strategy_lappend:
  assumes
    P: "lfinite P" "¬lnull P" "path_conforms_with_strategy p P σ"
    and P': "¬lnull P'" "path_conforms_with_strategy p P' σ"
    and conforms: "llast P ∈ VV p ==> σ (llast P) = lhd P'"
  shows "path_conforms_with_strategy p (lappend P P') σ"
using assms proof (induct P rule: lfinite_induct)
  case (LCons P)
  show ?case proof (cases)
    assume "lnull (ltl P)"
    then obtain v0 where v0: "P = LCons v0 LNil"
      by (metis LCons.prems(1) lhd_LCons_ltl llist.collapse(1))
    have "path_conforms_with_strategy p (LCons (lhd P) P') σ" proof (cases)
      assume "lhd P ∈ VV p"
      moreover with v0 have "lhd P' = σ (lhd P)"
        using LCons.prems(5) by auto
      ultimately show ?thesis
        using path_conforms_VVp[of "lhd P" p "lhd P'" σ]
        by (metis (no_types) LCons.prems(4) ‹¬lnull P'› lhd_LCons_ltl)
    next
      assume "lhd P ∉ VV p"
      thus ?thesis using path_conforms_VVpstar using LCons.prems(4) v0 by blast
    qed
    thus ?thesis by (simp add: v0)
  next
    assume "¬lnull (ltl P)"
    hence *: "path_conforms_with_strategy p (lappend (ltl P) P') σ"
      by (metis LCons.hyps(3) LCons.prems(1) LCons.prems(2) LCons.prems(5) LCons.prems(5)
                assms(4) assms(5) lhd_LCons_ltl llast_LCons2 path_conforms_with_strategy_ltl)
    have "path_conforms_with_strategy p (LCons (lhd P) (lappend (ltl P) P')) σ" proof (cases)
      assume "lhd P ∈ VV p"
      moreover hence "lhd (ltl P) = σ (lhd P)"
        by (metis LCons.prems(1) LCons.prems(2) ‹¬lnull (ltl P)›
                  lhd_LCons_ltl path_conforms_with_strategy_start)
      ultimately show ?thesis
        using path_conforms_VVp[of "lhd P" p "lhd (ltl P)" σ] * ‹¬lnull (ltl P)›
        by (metis lappend_code(2) lhd_LCons_ltl)
    next
      assume "lhd P ∉ VV p"
      thus ?thesis by (simp add: "*" path_conforms_VVpstar)
    qed
    with ‹¬lnull P› show "path_conforms_with_strategy p (lappend P P') σ"
      by (metis lappend_code(2) lhd_LCons_ltl)
  qed
qed simp

lemma path_conforms_with_strategy_VVpstar:
  assumes "lset P ⊆ VV p**"
  shows "path_conforms_with_strategy p P σ"
using assms proof (coinduction arbitrary: P)
  case (path_conforms_with_strategy P)
  moreover have "∧v Ps. P = LCons v Ps ==> ?case" using path_conforms_with_strategy by auto
  ultimately show ?case by (cases "P = LNil", simp) (metis lnull_def not_lnull_conv)
qed

lemma subgame_path_conforms_with_strategy:
  assumes V': "V' ⊆ V" and P: "path_conforms_with_strategy p P σ" "lset P ⊆ V'"
  shows "ParityGame.path_conforms_with_strategy (subgame V') p P σ"
proof-
  have "lset P ⊆ V _V'" unfolding subgame_def using P(2) V' by auto
  with P(1) show ?thesis
    by (coinduction arbitrary: P rule: ParityGame.path_conforms_with_strategy.coinduct[OF subgame_ParityGame])
       (cases rule: path_conforms_with_strategy.cases, auto)
qed

lemma (in vmc_path) subgame_path_vmc_path:
  assumes V': "V' ⊆ V" and P: "lset P ⊆ V'"
  shows "vmc_path (subgame V') P v0 p σ"
proof-
  interpret G': ParityGame "subgame V'" using subgame_ParityGame by blast
  show ?thesis proof
    show "G'.valid_path P" using subgame_valid_path P_valid P by blast
    show "G'.maximal_path P" using subgame_maximal_path V' P_maximal P by blast
    show "G'.path_conforms_with_strategy p P σ"
      using subgame_path_conforms_with_strategy V' P_conforms P by blast
  qed simp_all
qed

subsection ‹Greedy Conforming Path›

text ‹
 Given a starting point and two strategies, there exists a path conforming to both strategies.
 Here we define this path. Incidentally, this also shows that the assumptions of the locales
 ‹vmc_path› and ‹vmc2_path› are satisfiable.

 We are only interested in proving the existence of such a path, so the definition
 (i.e., the implementation) and most lemmas are private.
 ›

context begin

private primcorec greedy_conforming_path :: "Player ==> 'a Strategy ==> 'a Strategy ==> 'a ==> 'a Path" where
  "greedy_conforming_path p σ σ' v0 =
    LCons v0 (if deadend v0
      then LNil
      else if v0 ∈ VV p
        then greedy_conforming_path p σ σ' (σ v0)
        else greedy_conforming_path p σ σ' (σ' v0))"

private lemma greedy_path_LNil: "greedy_conforming_path p σ σ' v0 ≠ LNil"
  using greedy_conforming_path.disc_iff llist.discI(1) by blast

private lemma greedy_path_lhd: "greedy_conforming_path p σ σ' v0 = LCons v P ==> v = v0"
  using greedy_conforming_path.code by auto

private lemma greedy_path_deadend_v0: "greedy_conforming_path p σ σ' v0 = LCons v P ==> P = LNil ⟷ deadend v0"
  by (metis (no_types, lifting) greedy_conforming_path.disc_iff
      greedy_conforming_path.simps(3) llist.disc(1) ltl_simps(2))

private corollary greedy_path_deadend_v:
  "greedy_conforming_path p σ σ' v0 = LCons v P ==> P = LNil ⟷ deadend v"
  using greedy_path_deadend_v0 greedy_path_lhd by metis
corollary greedy_path_deadend_v': "greedy_conforming_path p σ σ' v0 = LCons v LNil ==> deadend v"
  using greedy_path_deadend_v by blast

private lemma greedy_path_ltl:
  assumes "greedy_conforming_path p σ σ' v0 = LCons v P"
  shows "P = LNil ∨ P = greedy_conforming_path p σ σ' (σ v0) ∨ P = greedy_conforming_path p σ σ' (σ' v0)"
  apply (insert assms, frule greedy_path_lhd)
  apply (cases "deadend v0", simp add: greedy_conforming_path.code)
  by (metis (no_types, lifting) greedy_conforming_path.sel(2) ltl_simps(2))

private lemma greedy_path_ltl_ex:
  assumes "greedy_conforming_path p σ σ' v0 = LCons v P"
  shows "P = LNil ∨ (∃v. P = greedy_conforming_path p σ σ' v)"
  using assms greedy_path_ltl by blast

private lemma greedy_path_ltl_VVp:
  assumes "greedy_conforming_path p σ σ' v0 = LCons v0 P" "v0 ∈ VV p" "¬deadend v0"
  shows "σ v0 = lhd P"
  using assms greedy_conforming_path.code by auto

private lemma greedy_path_ltl_VVpstar:
  assumes "greedy_conforming_path p σ σ' v0 = LCons v0 P" "v0 ∈ VV p**" "¬deadend v0"
  shows "σ' v0 = lhd P"
  using assms greedy_conforming_path.code by auto

private lemma greedy_conforming_path_properties:
  assumes "v0 ∈ V" "strategy p σ" "strategy p** σ'"
  shows
        greedy_path_not_null:  "¬lnull (greedy_conforming_path p σ σ' v0)"
    and greedy_path_v0:        "greedy_conforming_path p σ σ' v0 $ 0 = v0"
    and greedy_path_valid:     "valid_path (greedy_conforming_path p σ σ' v0)"
    and greedy_path_maximal:   "maximal_path (greedy_conforming_path p σ σ' v0)"
    and greedy_path_conforms:  "path_conforms_with_strategy p (greedy_conforming_path p σ σ' v0) σ"
    and greedy_path_conforms': "path_conforms_with_strategy p** (greedy_conforming_path p σ σ' v0) σ'"
proof-
  define P where [simp]: "P = greedy_conforming_path p σ σ' v0"

  show "¬lnull P" "P $ 0 = v0" by (simp_all add: lnth_0_conv_lhd)

  {
    fix v0 assume "v0 ∈ V"
    let ?P = "greedy_conforming_path p σ σ' v0"
    assume asm: "¬(∃v. ?P = LCons v LNil)"
    obtain P' where P': "?P = LCons v0 P'" by (metis greedy_path_LNil greedy_path_lhd neq_LNil_conv)
    hence "¬deadend v0" using asm greedy_path_deadend_v0 ‹v0 ∈ V› by blast
    from P' have 1: "¬lnull P'" using asm llist.collapse(1) ‹v0 ∈ V› greedy_path_deadend_v0 by blast
    moreover from P' ‹¬deadend v0› assms(2,3) ‹v0 ∈ V›
      have "v0→lhd P'"
      unfolding strategy_def using greedy_path_ltl_VVp greedy_path_ltl_VVpstar
      by (cases "v0 ∈ VV p") auto
    moreover hence "lhd P' ∈ V" by blast
    moreover hence "∃v. P' = greedy_conforming_path p σ σ' v ∧ v ∈ V"
      by (metis P' calculation(1) greedy_conforming_path.simps(2) greedy_path_ltl_ex lnull_def)
    text ‹The conjunction of all the above.›
    ultimately
      have "∃P'. ?P = LCons v0 P' ∧ ¬lnull P' ∧ v0→lhd P' ∧ lhd P' ∈ V
        ∧ (∃v. P' = greedy_conforming_path p σ σ' v ∧ v ∈ V)"
      using P' by blast
  } note coinduction_helper = this

  show "valid_path P" using assms unfolding P_def
  proof (coinduction arbitrary: v0 rule: valid_path.coinduct)
    case (valid_path v0)
    from ‹v0 ∈ V› assms(2,3) show ?case
      using coinduction_helper[of v0] greedy_path_lhd by blast
  qed

  show "maximal_path P" using assms unfolding P_def
  proof (coinduction arbitrary: v0)
    case (maximal_path v0)
    from ‹v0 ∈ V› assms(2,3) show ?case
      using coinduction_helper[of v0] greedy_path_deadend_v' by blast
  qed

  {
    fix p'' σ'' assume p'': "(p'' = p ∧ σ'' = σ) ∨ (p'' = p** ∧ σ'' = σ')"
    moreover with assms have "strategy p'' σ''" by blast
    hence "path_conforms_with_strategy p'' P σ''" using ‹v0 ∈ V› unfolding P_def
    proof (coinduction arbitrary: v0)
      case (path_conforms_with_strategy v0)
      show ?case proof (cases "v0 ∈ VV p''")
        case True
        { assume "¬(∃v. greedy_conforming_path p σ σ' v0 = LCons v LNil)"
          with ‹v0 ∈ V› obtain P' where
            P': "greedy_conforming_path p σ σ' v0 = LCons v0 P'" "¬lnull P'" "v0→lhd P'"
                "lhd P' ∈ V" "∃v. P' = greedy_conforming_path p σ σ' v ∧ v ∈ V"
            using coinduction_helper by blast
          with ‹v0 ∈ VV p''› p'' have "σ'' v0 = lhd P'"
            using greedy_path_ltl_VVp greedy_path_ltl_VVpstar by blast
          with ‹v0 ∈ VV p''› P'(1,2,5) have ?path_conforms_VVp
            using greedy_conforming_path.code path_conforms_with_strategy(1) by fastforce
        }
        thus ?thesis by auto
      next
        case False
        thus ?thesis using coinduction_helper[of v0] path_conforms_with_strategy by auto
      qed
    qed
  }
  thus "path_conforms_with_strategy p P σ" "path_conforms_with_strategy p** P σ'" by blast+
qed

corollary strategy_conforming_path_exists:
  assumes "v0 ∈ V" "strategy p σ" "strategy p** σ'"
  obtains P where "vmc2_path G P v0 p σ σ'"
proof
  show "vmc2_path G (greedy_conforming_path p σ σ' v0) v0 p σ σ'"
    using assms by unfold_locales (simp_all add: greedy_conforming_path_properties)
qed

corollary strategy_conforming_path_exists_single:
  assumes "v0 ∈ V" "strategy p σ"
  obtains P where "vmc_path G P v0 p σ"
proof
  show "vmc_path G (greedy_conforming_path p σ σ_arbitrary v0) v0 p σ"
    using assms by unfold_locales (simp_all add: greedy_conforming_path_properties)
qed

end

end

subsection ‹Valid Maximal Conforming Paths›

text ‹Now is the time to add some lemmas to the locale ‹vmc_path›.›

context vmc_path begin
lemma Ptl_conforms [simp]: "path_conforms_with_strategy p (ltl P) σ"
  using P_conforms path_conforms_with_strategy_ltl by blast
lemma Pdrop_conforms [simp]: "path_conforms_with_strategy p (ldropn n P) σ"
  using P_conforms path_conforms_with_strategy_drop by blast
lemma prefix_conforms [simp]: "path_conforms_with_strategy p (ltake n P) σ"
  using P_conforms path_conforms_with_strategy_prefix by blast
lemma extension_conforms [simp]:
  "(v' ∈ VV p ==> σ v' = v0) ==> path_conforms_with_strategy p (LCons v' P) σ"
  by (metis P_LCons P_conforms path_conforms_VVp path_conforms_VVpstar)

lemma extension_valid_maximal_conforming:
  assumes "v'→v0" "v' ∈ VV p ==> σ v' = v0"
  shows "vmc_path G (LCons v' P) v' p σ"
  using assms by unfold_locales simp_all

lemma vmc_path_ldropn:
  assumes "enat n < llength P"
  shows "vmc_path G (ldropn n P) (P $ n) p σ"
  using assms by unfold_locales (simp_all add: lhd_ldropn)

lemma conforms_to_another_strategy:
  "path_conforms_with_strategy p P σ' ==> vmc_path G P v0 p σ'"
  using P_not_null P_valid P_maximal P_v0 by unfold_locales blast+
end

lemma (in ParityGame) valid_maximal_conforming_path_0:
  assumes "¬lnull P" "valid_path P" "maximal_path P" "path_conforms_with_strategy p P σ"
  shows "vmc_path G P (P $ 0) p σ"
  using assms by unfold_locales (simp_all add: lnth_0_conv_lhd)

subsection ‹Valid Maximal Conforming Paths with One Edge›

text ‹
 We define a locale for valid maximal conforming paths that contain at least one edge.
 This is equivalent to the first node being no deadend. This assumption allows us to prove
 much stronger lemmas about @{term "ltl P"} compared to @{term "vmc_path"}.
 ›

locale vmc_path_no_deadend = vmc_path +
  assumes v0_no_deadend [simp]: "¬deadend v0"
begin
definition "w0 ≡ lhd (ltl P)"

lemma Ptl_not_null [simp]: "¬lnull (ltl P)"
  using P_LCons P_maximal maximal_no_deadend v0_no_deadend by metis
lemma Ptl_LCons: "ltl P = LCons w0 (ltl (ltl P))" unfolding w0_def by simp
lemma P_LCons': "P = LCons v0 (LCons w0 (ltl (ltl P)))" using P_LCons Ptl_LCons by simp
lemma v0_edge_w0 [simp]: "v0→w0" using P_valid P_LCons' by (metis valid_path_edges')

lemma Ptl_0: "ltl P $ 0 = lhd (ltl P)" by (simp add: lhd_conv_lnth)
lemma P_Suc_0: "P $ Suc 0 = w0" by (simp add: P_lnth_Suc Ptl_0 w0_def)
lemma Ptl_edge [simp]: "v0 → lhd (ltl P)" by (metis P_LCons' P_valid valid_path_edges' w0_def)

lemma v0_conforms: "v0 ∈ VV p ==> σ v0 = w0"
  using path_conforms_with_strategy_start by (metis P_LCons' P_conforms)

lemma w0_V [simp]: "w0 ∈ V" by (metis Ptl_LCons Ptl_valid valid_path_cons_simp)
lemma w0_lset_P [simp]: "w0 ∈ lset P" by (metis P_LCons' lset_intros(1) lset_intros(2))

lemma vmc_path_ltl [simp]: "vmc_path G (ltl P) w0 p σ" by (unfold_locales) (simp_all add: w0_def)
end

context vmc_path begin

lemma vmc_path_lnull_ltl_no_deadend:
  "¬lnull (ltl P) ==> vmc_path_no_deadend G P v0 p σ"
  using P_0 P_no_deadends by (unfold_locales) (metis enat_ltl_Suc lnull_0_llength)

lemma vmc_path_conforms:
  assumes "enat (Suc n) < llength P" "P $ n ∈ VV p"
  shows "σ (P $ n) = P $ Suc n"
proof-
  define P' where "P' = ldropn n P"
  then interpret P': vmc_path G P' "P $ n" p σ using vmc_path_ldropn assms(1) Suc_llength by blast
  have "¬deadend (P $ n)" using assms(1) P_no_deadends by blast
  then interpret P': vmc_path_no_deadend G P' "P $ n" p σ by unfold_locales
  have "σ (P $ n) = P'.w0" using P'.v0_conforms assms(2) by blast
  thus ?thesis using P'_def P'.P_Suc_0 assms(1) by simp
qed

subsection ‹@{term lset} Induction Schemas for Paths›

text ‹Let us define an induction schema useful for proving @{term "lset P ⊆ S"}.›

lemma vmc_path_lset_induction [consumes 1, case_names base step]:
  assumes "Q P"
    and base: "v0 ∈ S"
    and step_assumption: "∧P v0. [ vmc_path_no_deadend G P v0 p σ; v0 ∈ S; Q P ]
      ==> Q (ltl P) ∧ (vmc_path_no_deadend.w0 P) ∈ S"
  shows "lset P ⊆ S"
proof
  fix v assume "v ∈ lset P"
  thus "v ∈ S" using vmc_path_axioms assms(1,2) proof (induct arbitrary: v0 rule: llist_set_induct)
    case (find P)
    then interpret vmc_path G P v0 p σ by blast
    show ?case by (simp add: find.prems(3))
  next
    case (step P v)
    then interpret vmc_path G P v0 p σ by blast
    show ?case proof (cases)
      assume "lnull (ltl P)"
      hence "P = LCons v LNil" by (metis llist.disc(2) lset_cases step.hyps(2))
      thus ?thesis using step.prems(3) P_LCons by blast
    next
      assume "¬lnull (ltl P)"
      then interpret vmc_path_no_deadend G P v0 p σ
        using vmc_path_lnull_ltl_no_deadend by blast
      show "v ∈ S"
        using step.hyps(3)
              step_assumption[OF vmc_path_no_deadend_axioms ‹v0 ∈ S› ‹Q P›]
              vmc_path_ltl
        by blast
    qed
  qed
qed

text ‹@{thm vmc_path_lset_induction} without the Q predicate.›
corollary vmc_path_lset_induction_simple [case_names base step]:
  assumes base: "v0 ∈ S"
    and step: "∧P v0. [ vmc_path_no_deadend G P v0 p σ; v0 ∈ S ]
      ==> vmc_path_no_deadend.w0 P ∈ S"
  shows "lset P ⊆ S"
  using assms vmc_path_lset_induction[of "λP. True"] by blast

text ‹Another induction schema for proving @{term "lset P ⊆ S"} based on closure properties.›

lemma vmc_path_lset_induction_closed_subset [case_names VVp VVpstar v0 disjoint]:
  assumes VVp: "∧v. [ v ∈ S; ¬deadend v; v ∈ VV p ] ==> σ v ∈ S ∪ T"
    and VVpstar: "∧v w. [ v ∈ S; ¬deadend v; v ∈ VV p** ; v→w ] ==> w ∈ S ∪ T"
    and v0: "v0 ∈ S"
    and disjoint: "lset P ∩ T = {}"
  shows "lset P ⊆ S"
using disjoint proof (induct rule: vmc_path_lset_induction)
  case (step P v0)
  interpret vmc_path_no_deadend G P v0 p σ using step.hyps(1) .
  have "lset (ltl P) ∩ T = {}" using step.hyps(3)
    by (meson disjoint_eq_subset_Compl lset_ltl order.trans)
  moreover have "w0 ∈ S ∪ T"
    using assms(1,2)[of v0] step.hyps(2) v0_no_deadend v0_conforms
    by (cases "v0 ∈ VV p") simp_all
  ultimately show ?case using step.hyps(3) w0_lset_P by blast
qed (insert v0)

end

end