Theory Restricted_Master_Theorem

(*
    Author:   Salomon Sickert
    Author:   Benedikt Seidl
    License:  BSD
*)

section ‹Master Theorem with Reduced Subformulas›

theory Restricted_Master_Theorem
imports
  Master_Theorem
begin

subsection ‹Restricted Set of Subformulas›

fun restricted_subformulas_inner :: "'a ltln ⇒ 'a ltln set"
where
  "restricted_subformulas_inner (φ andn ψ) = restricted_subformulas_inner φ ∪ restricted_subformulas_inner ψ"
| "restricted_subformulas_inner (φ orn ψ) = restricted_subformulas_inner φ ∪ restricted_subformulas_inner ψ"
| "restricted_subformulas_inner (Xn φ) = restricted_subformulas_inner φ"
| "restricted_subformulas_inner (φ Un ψ) = subformulasν (φ Un ψ) ∪ subformulasμ (φ Un ψ)"
| "restricted_subformulas_inner (φ Rn ψ) = restricted_subformulas_inner φ ∪ restricted_subformulas_inner ψ"
| "restricted_subformulas_inner (φ Wn ψ) = restricted_subformulas_inner φ ∪ restricted_subformulas_inner ψ"
| "restricted_subformulas_inner (φ Mn ψ) = subformulasν (φ Mn ψ) ∪ subformulasμ (φ Mn ψ)"
| "restricted_subformulas_inner _ = {}"

fun restricted_subformulas :: "'a ltln ⇒ 'a ltln set"
where
  "restricted_subformulas (φ andn ψ) = restricted_subformulas φ ∪ restricted_subformulas ψ"
| "restricted_subformulas (φ orn ψ) = restricted_subformulas φ ∪ restricted_subformulas ψ"
| "restricted_subformulas (Xn φ) = restricted_subformulas φ"
| "restricted_subformulas (φ Un ψ) = restricted_subformulas φ ∪ restricted_subformulas ψ"
| "restricted_subformulas (φ Rn ψ) = restricted_subformulas φ ∪ restricted_subformulas_inner ψ"
| "restricted_subformulas (φ Wn ψ) = restricted_subformulas_inner φ ∪ restricted_subformulas ψ"
| "restricted_subformulas (φ Mn ψ) = restricted_subformulas φ ∪ restricted_subformulas ψ"
| "restricted_subformulas _ = {}"

lemma GF_advice_restricted_subformulas_inner:
  "restricted_subformulas_inner (φ[X]ν) = {}"
  by (induction φ) simp_all

lemma GF_advice_restricted_subformulas:
  "restricted_subformulas (φ[X]ν) = {}"
  by (induction φ) (simp_all add: GF_advice_restricted_subformulas_inner)

lemma restricted_subformulas_inner_subset:
  "restricted_subformulas_inner φ ⊆ subformulasν φ ∪ subformulasμ φ"
  by (induction φ) auto

lemma restricted_subformulas_subset':
  "restricted_subformulas φ ⊆ restricted_subformulas_inner φ"
  by (induction φ) (insert restricted_subformulas_inner_subset, auto)

lemma restricted_subformulas_subset:
  "restricted_subformulas φ ⊆ subformulasν φ ∪ subformulasμ φ"
  using restricted_subformulas_inner_subset restricted_subformulas_subset' by auto

lemma restricted_subformulas_size:
  "ψ ∈ restricted_subformulas φ ⟹ size ψ < size φ"
proof -
  have "⋀φ. restricted_subformulas_inner φ ⊆ subfrmlsn φ"
    using restricted_subformulas_inner_subset subformulasμν_subfrmlsn by blast

  then have inner: "⋀ψ φ. ψ ∈ restricted_subformulas_inner φ ⟹ size ψ ≤ size φ"
    using subfrmlsn_size dual_order.strict_implies_order
    by blast

  show "ψ ∈ restricted_subformulas φ ⟹ size ψ < size φ"
    by (induction φ arbitrary: ψ) (fastforce dest: inner)+
qed

lemma restricted_subformulas_notin:
  "φ ∉ restricted_subformulas φ"
  using restricted_subformulas_size by auto

lemma restricted_subformulas_superset:
  "ψ ∈ restricted_subformulas φ ⟹ subformulasν ψ ∪ subformulasμ ψ ⊆ restricted_subformulas φ"
proof -
  assume "ψ ∈ restricted_subformulas φ"

  then obtain χ x where
    "ψ ∈ restricted_subformulas_inner χ" and "(x Rn χ) ∈ subformulasν φ ∨ (χ Wn x) ∈ subformulasν φ "
    by (induction φ) auto

  moreover

  have "⋀ψ1 ψ2. (ψ1 Rn ψ2) ∈ subformulasν φ ⟹ restricted_subformulas_inner ψ2 ⊆ restricted_subformulas φ"
    "⋀ψ1 ψ2. (ψ1 Wn ψ2) ∈ subformulasν φ ⟹ restricted_subformulas_inner ψ1 ⊆ restricted_subformulas φ"
    by (induction φ) (simp_all; insert restricted_subformulas_subset', blast)+

  moreover

  have "subformulasν ψ ∪ subformulasμ ψ ⊆  restricted_subformulas_inner χ"
    using ‹ψ ∈ restricted_subformulas_inner χ›
  proof (induction χ)
    case (Until_ltln χ1 χ2)
    then show ?case
      apply (cases "ψ = χ1 Un χ2")
       apply auto[1]
      apply simp
      apply (cases "ψ ∈ subformulasν χ1")
       apply (meson le_supI1 le_supI2 subformulasμ_subset subformulasν_subfrmlsn subformulasν_subset subset_eq subset_insertI2)
      apply (cases "ψ ∈ subformulasν χ2")
       apply (meson le_supI1 le_supI2 subformulasμ_subset subformulasν_subfrmlsn subformulasν_subset subset_eq subset_insertI2)
      apply (cases "ψ ∈ subformulasμ χ1")
       apply (metis (no_types, opaque_lifting) Un_insert_right subformulasμ_subfrmlsn subformulasμ_subset subformulasν_subset subsetD sup.coboundedI2 sup_commute)
      apply simp
      by (metis (no_types, opaque_lifting) Un_insert_right subformulasμ_subfrmlsn subformulasμ_subset subformulasν_subset subsetD sup.coboundedI2 sup_commute)
  next
    case (Release_ltln χ1 χ2)
    then show ?case by simp blast
  next
    case (WeakUntil_ltln χ1 χ2)
    then show ?case by simp blast
  next
    case (StrongRelease_ltln χ1 χ2)
    then show ?case
      apply (cases "ψ = χ1 Mn χ2")
       apply auto[1]
      apply simp
      apply (cases "ψ ∈ subformulasν χ1")
       apply (meson le_supI1 le_supI2 subformulasμ_subset subformulasν_subfrmlsn subformulasν_subset subset_eq subset_insertI2)
      apply (cases "ψ ∈ subformulasν χ2")
       apply (meson le_supI1 le_supI2 subformulasμ_subset subformulasν_subfrmlsn subformulasν_subset subset_eq subset_insertI2)
      apply (cases "ψ ∈ subformulasμ χ1")
       apply (metis (no_types, opaque_lifting) Un_insert_right subformulasμ_subfrmlsn subformulasμ_subset subformulasν_subset subsetD sup.coboundedI2 sup_commute)
      apply simp
      by (metis (no_types, opaque_lifting) Un_insert_right subformulasμ_subfrmlsn subformulasμ_subset subformulasν_subset subsetD sup.coboundedI2 sup_commute)
  qed auto

  ultimately

  show "subformulasν ψ ∪ subformulasμ ψ ⊆ restricted_subformulas φ"
    by blast
qed

lemma restricted_subformulas_W_μ:
  "subformulasμ φ ⊆ restricted_subformulas (φ Wn ψ)"
  by (induction φ) auto

lemma restricted_subformulas_R_μ:
  "subformulasμ ψ ⊆ restricted_subformulas (φ Rn ψ)"
  by (induction ψ) auto

lemma restrict_af_letter:
  "restricted_subformulas (af_letter φ σ) = restricted_subformulas φ"
proof (induction φ)
  case (Release_ltln φ1 φ2)
  then show ?case
    using restricted_subformulas_subset' by simp blast
next
  case (WeakUntil_ltln φ1 φ2)
  then show ?case
    using restricted_subformulas_subset' by simp blast
qed auto

lemma restrict_af:
  "restricted_subformulas (af φ w) = restricted_subformulas φ"
  by (induction w rule: rev_induct) (auto simp: restrict_af_letter)


subsection ‹Restricted Master Theorem / Lemmas›

lemma delay_2:
  assumes "μ_stable φ w"
  assumes "w ⊨n φ"
  shows "∃i. suffix i w ⊨n af φ (prefix i w)[{ψ. w ⊨n Gn (Fn ψ)} ∩ restricted_subformulas φ]ν"
  using assms
proof (induction φ arbitrary: w)
  case (Prop_ltln x)
  then show ?case
    by (metis GF_advice.simps(10) GF_advice_af prefix_suffix)
next
  case (Nprop_ltln x)
  then show ?case
    by (metis GF_advice.simps(11) GF_advice_af prefix_suffix)
next
  case (And_ltln φ1 φ2)

  let ?X  = "{ψ. w ⊨n Gn (Fn ψ)} ∩ restricted_subformulas (φ1 andn φ2)"
  let ?X1 = "{ψ. w ⊨n Gn (Fn ψ)} ∩ restricted_subformulas φ1"
  let ?X2 = "{ψ. w ⊨n Gn (Fn ψ)} ∩ restricted_subformulas φ2"

  have "?X1 ⊆ ?X" and "?X2 ⊆ ?X"
    by auto

  moreover

  obtain i j where "suffix i w ⊨n af φ1 (prefix i w)[?X1]ν"
    and "suffix j w ⊨n af φ2 (prefix j w)[?X2]ν"
    using μ_stable_subfrmlsn[OF ‹μ_stable (φ1 andn φ2) w›] And_ltln by fastforce

  ultimately

  obtain k where "suffix k w ⊨n af φ1 (prefix k w)[?X]ν"
    and "suffix k w ⊨n af φ2 (prefix k w)[?X]ν"
    using GF_advice_sync_and GF_advice_monotone by blast

  thus ?case
    unfolding af_decompose semantics_ltln.simps(5) GF_advice.simps by blast
next
  case (Or_ltln φ1 φ2)
  let ?X  = "{ψ. w ⊨n Gn (Fn ψ)} ∩ restricted_subformulas (φ1 andn φ2)"
  let ?X1 = "{ψ. w ⊨n Gn (Fn ψ)} ∩ restricted_subformulas φ1"
  let ?X2 = "{ψ. w ⊨n Gn (Fn ψ)} ∩ restricted_subformulas φ2"

  have "?X1 ⊆ ?X" and "?X2 ⊆ ?X"
    by auto

  moreover

  obtain i j where "suffix i w ⊨n af φ1 (prefix i w)[?X1]ν ∨ suffix j w ⊨n af φ2 (prefix j w)[?X2]ν"
    using μ_stable_subfrmlsn[OF ‹μ_stable (φ1 orn φ2) w›] Or_ltln by fastforce

  ultimately

  obtain k where "suffix k w ⊨n af φ1 (prefix k w)[?X]ν ∨ suffix k w ⊨n af φ2 (prefix k w)[?X]ν"
    using GF_advice_monotone by blast

  thus ?case
    unfolding af_decompose semantics_ltln.simps(6) GF_advice.simps by auto
next
  case (Next_ltln φ)
  then have stable: "μ_stable φ (suffix 1 w)"
    and suffix: "suffix 1 w ⊨n φ"
    using ℱ_suffix 𝒢ℱ_ℱ_subset 𝒢ℱ_suffix
    by (simp_all add: μ_stable_def) fast
  show ?case
    by (metis (no_types, lifting) Next_ltln.IH[OF stable suffix, unfolded suffix_suffix prefix_suffix_subsequence GF_suffix] One_nat_def add.commute af_simps(3) foldl_Nil foldl_append restricted_subformulas.simps(3) subsequence_append subsequence_singleton)
next
  case (Until_ltln φ1 φ2)
  let ?X  = "{ψ. w ⊨n Gn (Fn ψ)} ∩ restricted_subformulas (φ1 Un φ2)"
  let ?X1 = "{ψ. w ⊨n Gn (Fn ψ)} ∩ restricted_subformulas φ1"
  let ?X2 = "{ψ. w ⊨n Gn (Fn ψ)} ∩ restricted_subformulas φ2"

  have stable_1: "⋀i. μ_stable φ1 (suffix i w)"
    and stable_2: "⋀i. μ_stable φ2 (suffix i w)"
    using μ_stable_subfrmlsn[OF Until_ltln.prems(1)] by (simp add: μ_stable_suffix)+

  obtain i where "⋀j. j < i ⟹ suffix j w ⊨n φ1" and "suffix i w ⊨n φ2"
    using Until_ltln by auto

  then have "⋀j. j < i ⟹ ∃k. suffix (j + k) w ⊨n af φ1 (w [j → k + j])[?X1]ν"
    and "∃k. suffix (i + k) w ⊨n af φ2 (w [i → k + i])[?X2]ν"
    using Until_ltln.IH(1)[OF stable_1, unfolded suffix_suffix prefix_suffix_subsequence GF_suffix]
    using Until_ltln.IH(2)[OF stable_2, unfolded suffix_suffix prefix_suffix_subsequence GF_suffix]
    by blast+

  moreover

  have "?X1 ⊆ ?X"
    and "?X2 ⊆ ?X"
    by auto

  ultimately

  obtain k where "k ≥ i"
    and "suffix k w ⊨n af φ2 (w [i → k])[?X]ν"
    and "⋀j. j < i ⟹ suffix k w ⊨n af φ1 (w [j → k])[?X]ν"
    using GF_advice_sync_less[of i w φ1 ?X φ2] GF_advice_monotone[of _ ?X] by meson

  hence "suffix (Suc k) w ⊨n af (φ1 Un φ2) (prefix (Suc k) w)[?X]ν"
    by (rule af_subsequence_U_GF_advice)

  then show ?case
    by blast
next
  case (WeakUntil_ltln φ1 φ2)

  let ?X  = "{ψ. w ⊨n Gn (Fn ψ)} ∩ restricted_subformulas (φ1 Wn φ2)"
  let ?X1 = "{ψ. w ⊨n Gn (Fn ψ)} ∩ restricted_subformulas φ1"
  let ?X2 = "{ψ. w ⊨n Gn (Fn ψ)} ∩ restricted_subformulas φ2"

  have stable_1: "⋀i. μ_stable φ1 (suffix i w)"
    and stable_2: "⋀i. μ_stable φ2 (suffix i w)"
    using μ_stable_subfrmlsn[OF WeakUntil_ltln.prems(1)] by (simp add: μ_stable_suffix)+

  {
    assume Until_ltln: "w ⊨n φ1 Un φ2"
    then obtain i where "⋀j. j < i ⟹ suffix j w ⊨n φ1" and "suffix i w ⊨n φ2"
      by auto

    then have "⋀j. j < i ⟹ ∃k. suffix (j + k) w ⊨n af φ1 (w [j → k + j])[?X1]ν"
      and "∃k. suffix (i + k) w ⊨n af φ2 (w [i → k + i])[?X2]ν"
      using WeakUntil_ltln.IH(1)[OF stable_1, unfolded suffix_suffix prefix_suffix_subsequence GF_suffix]
      using WeakUntil_ltln.IH(2)[OF stable_2, unfolded suffix_suffix prefix_suffix_subsequence GF_suffix]
      by blast+

    moreover

    have "?X1 ⊆ ?X"
      and "?X2 ⊆ ?X"
      using restricted_subformulas_subset' by force+

    ultimately

    obtain k where "k ≥ i"
      and "suffix k w ⊨n af φ2 (w [i → k])[?X]ν"
      and "⋀j. j < i ⟹ suffix k w ⊨n af φ1 (w [j → k])[?X]ν"
      using GF_advice_sync_less[of i w φ1 ?X φ2] GF_advice_monotone[of _ ?X] by meson

    hence "suffix (Suc k) w ⊨n af (φ1 Wn φ2) (prefix (Suc k) w)[?X]ν"
      by (rule af_subsequence_W_GF_advice)
    hence ?case
      by blast
  }
  moreover
  {
    assume Globally_ltln: "w ⊨n Gn φ1"

    {
      fix j
      have "suffix j w ⊨n φ1"
        using Globally_ltln by simp
      then have "suffix j w ⊨n φ1[{ψ. w ⊨n Gn (Fn ψ)}]ν"
        by (metis stable_1 GF_advice_a1 𝒢ℱ_suffix μ_stable_def 𝒢ℱ_elim mem_Collect_eq subsetI)
      then have "suffix j w ⊨n φ1[?X]ν"
        by (metis GF_advice_inter restricted_subformulas_W_μ le_infI2)
    }

    then have "w ⊨n (φ1 Wn φ2)[?X]ν"
      by simp
    then have ?case
      using GF_advice_af_2 by blast
  }
  ultimately
  show ?case
    using WeakUntil_ltln.prems(2) ltln_weak_to_strong(1) by blast
next
  case (Release_ltln φ1 φ2)

  let ?X  = "{ψ. w ⊨n Gn (Fn ψ)} ∩ restricted_subformulas (φ1 Rn φ2)"
  let ?X1 = "{ψ. w ⊨n Gn (Fn ψ)} ∩ restricted_subformulas φ1"
  let ?X2 = "{ψ. w ⊨n Gn (Fn ψ)} ∩ restricted_subformulas φ2"

  have stable_1: "⋀i. μ_stable φ1 (suffix i w)"
    and stable_2: "⋀i. μ_stable φ2 (suffix i w)"
    using μ_stable_subfrmlsn[OF Release_ltln.prems(1)] by (simp add: μ_stable_suffix)+

  {
    assume Until_ltln: "w ⊨n φ1 Mn φ2"
    then obtain i where "⋀j. j ≤ i ⟹ suffix j w ⊨n φ2" and "suffix i w ⊨n φ1"
      by auto

    then have "⋀j. j ≤ i ⟹ ∃k. suffix (j + k) w ⊨n af φ2 (w [j → k + j])[?X2]ν"
      and "∃k. suffix (i + k) w ⊨n af φ1 (w [i → k + i])[?X1]ν"
      using Release_ltln.IH(1)[OF stable_1, unfolded suffix_suffix prefix_suffix_subsequence GF_suffix]
      using Release_ltln.IH(2)[OF stable_2, unfolded suffix_suffix prefix_suffix_subsequence GF_suffix]
      by blast+

    moreover

    have "?X1 ⊆ ?X"
      and "?X2 ⊆ ?X"
      using restricted_subformulas_subset' by force+

    ultimately

    obtain k where "k ≥ i"
      and "suffix k w ⊨n af φ1 (w [i → k])[?X]ν"
      and "⋀j. j ≤ i ⟹ suffix k w ⊨n af φ2 (w [j → k])[?X]ν"
      using GF_advice_sync_lesseq[of i w φ2 ?X φ1] GF_advice_monotone[of _ ?X] by meson

    hence "suffix (Suc k) w ⊨n af (φ1 Rn φ2) (prefix (Suc k) w)[?X]ν"
      by (rule af_subsequence_R_GF_advice)
    hence ?case
      by blast
  }
  moreover
  {
    assume Globally_ltln: "w ⊨n Gn φ2"

    {
      fix j
      have "suffix j w ⊨n φ2"
        using Globally_ltln by simp
      then have "suffix j w ⊨n φ2[{ψ. w ⊨n Gn (Fn ψ)}]ν"
        by (metis stable_2 GF_advice_a1 𝒢ℱ_suffix μ_stable_def 𝒢ℱ_elim mem_Collect_eq subsetI)
      then have "suffix j w ⊨n φ2[?X]ν"
        by (metis GF_advice_inter restricted_subformulas_R_μ le_infI2)
    }

    then have "w ⊨n (φ1 Rn φ2)[?X]ν"
      by simp
    then have ?case
      using GF_advice_af_2 by blast
  }
  ultimately
  show ?case
    using Release_ltln.prems(2) ltln_weak_to_strong(3) by blast
next
  case (StrongRelease_ltln φ1 φ2)

  let ?X  = "{ψ. w ⊨n Gn (Fn ψ)} ∩ restricted_subformulas (φ1 Mn φ2)"
  let ?X1 = "{ψ. w ⊨n Gn (Fn ψ)} ∩ restricted_subformulas φ1"
  let ?X2 = "{ψ. w ⊨n Gn (Fn ψ)} ∩ restricted_subformulas φ2"

  have stable_1: "⋀i. μ_stable φ1 (suffix i w)"
    and stable_2: "⋀i. μ_stable φ2 (suffix i w)"
    using μ_stable_subfrmlsn[OF StrongRelease_ltln.prems(1)] by (simp add: μ_stable_suffix)+

  obtain i where "⋀j. j ≤ i ⟹ suffix j w ⊨n φ2" and "suffix i w ⊨n φ1"
    using StrongRelease_ltln by auto

  then have "⋀j. j ≤ i ⟹ ∃k. suffix (j + k) w ⊨n af φ2 (w [j → k + j])[?X2]ν"
    and "∃k. suffix (i + k) w ⊨n af φ1 (w [i → k + i])[?X1]ν"
    using StrongRelease_ltln.IH(1)[OF stable_1, unfolded suffix_suffix prefix_suffix_subsequence GF_suffix]
    using StrongRelease_ltln.IH(2)[OF stable_2, unfolded suffix_suffix prefix_suffix_subsequence GF_suffix]
    by blast+

  moreover

  have "?X1 ⊆ ?X"
    and "?X2 ⊆ ?X"
    by auto

  ultimately

  obtain k where "k ≥ i"
    and "suffix k w ⊨n af φ1 (w [i → k])[?X]ν"
    and "⋀j. j ≤ i ⟹ suffix k w ⊨n af φ2 (w [j → k])[?X]ν"
    using GF_advice_sync_lesseq[of i w φ2 ?X φ1] GF_advice_monotone[of _ ?X] by meson

  hence "suffix (Suc k) w ⊨n af (φ1 Mn φ2) (prefix (Suc k) w)[?X]ν"
    by (rule af_subsequence_M_GF_advice)

  then show ?case
    by blast
qed simp+

theorem master_theorem_restricted:
  "w ⊨n φ ⟷
    (∃X ⊆ subformulasμ φ ∩ restricted_subformulas φ.
       (∃Y ⊆ subformulasν φ ∩ restricted_subformulas φ.
         (∃i. (suffix i w ⊨n af φ (prefix i w)[X]ν)
          ∧ (∀ψ ∈ X. w ⊨n Gn (Fn ψ[Y]μ))
          ∧ (∀ψ ∈ Y. w ⊨n Fn (Gn ψ[X]ν)))))"
  (is "?lhs ⟷ ?rhs")
proof
  assume ?lhs

  obtain i where "μ_stable φ (suffix i w)"
   by (metis MOST_nat less_Suc_eq suffix_μ_stable)

  hence stable: "μ_stable (af φ (prefix i w)) (suffix i w)"
    by (simp add: ℱ_af 𝒢ℱ_af μ_stable_def)

  let ?φ' = "af φ (prefix i w)"
  let ?X' = "𝒢ℱ φ w ∩ restricted_subformulas φ"
  let ?Y' = "ℱ𝒢 φ w ∩ restricted_subformulas φ"

  have 1: "suffix i w ⊨n ?φ'"
    using ‹?lhs› af_ltl_continuation by force

  have 2: "⋀j. af (af φ (prefix i w)) (prefix j (suffix i w)) = af φ (prefix (i + j) w)"
    by (simp add: subsequence_append)

  have 3: "𝒢ℱ φ w = 𝒢ℱ φ (suffix i w)"
    using 𝒢ℱ_af 𝒢ℱ_suffix by blast

  have "∃j. suffix (i + j) w ⊨n af (?φ') (prefix j (suffix i w))[?X']ν"
    using delay_2[OF stable 1] unfolding suffix_suffix 2 restrict_af 3 unfolding 𝒢ℱ_semantics'
    by (metis (no_types, lifting) GF_advice_inter_subformulas af_subformulasμ inf_assoc inf_commute)

  hence "∃i. suffix i w ⊨n af φ (prefix i w)[?X']ν"
    using 2 by auto

  moreover

  {
    fix ψ
    have "⋀X. ψ ∈ restricted_subformulas φ ⟹ ψ[X ∩ restricted_subformulas φ]μ = ψ[X]μ"
      by (metis le_supE restricted_subformulas_superset FG_advice_inter inf.coboundedI2)
    hence "ψ ∈ ?X' ⟹  w ⊨n Gn (Fn ψ[?Y']μ)"
      using 𝒢ℱ_implies_GF by force
  }

  moreover

  {
    fix ψ
    have "⋀X. ψ ∈ restricted_subformulas φ ⟹ ψ[X ∩ restricted_subformulas φ]ν = ψ[X]ν"
      by (metis le_supE restricted_subformulas_superset GF_advice_inter inf.coboundedI2)
    hence "ψ ∈ ?Y' ⟹ w ⊨n Fn (Gn ψ[?X']ν)"
      using ℱ𝒢_implies_FG by force
  }

  moreover

  have "?X' ⊆ subformulasμ φ ∩ restricted_subformulas φ"
    using 𝒢ℱ_subformulasμ by blast

  moreover

  have "?Y' ⊆ subformulasν φ ∩ restricted_subformulas φ"
    using ℱ𝒢_subformulasν by blast

  ultimately show ?rhs
    by meson
qed (insert master_theorem, fast)


corollary master_theorem_restricted_language:
  "language_ltln φ = ⋃ {L1 φ X ∩ L2 X Y ∩ L3 X Y | X Y. X ⊆ subformulasμ φ ∩ restricted_subformulas φ ∧ Y ⊆ subformulasν φ ∩ restricted_subformulas φ}"
proof safe
  fix w
  assume "w ∈ language_ltln φ"

  then have "w ⊨n φ"
    unfolding language_ltln_def by simp

  then obtain X Y where
        1: "X ⊆ subformulasμ φ ∩ restricted_subformulas φ"
    and 2: "Y ⊆ subformulasν φ ∩ restricted_subformulas φ"
    and "∃i. suffix i w ⊨n af φ (prefix i w)[X]ν"
    and "∀ψ ∈ X. w ⊨n Gn (Fn ψ[Y]μ)"
    and "∀ψ ∈ Y. w ⊨n Fn (Gn ψ[X]ν)"
    using master_theorem_restricted by metis

  then have "w ∈ L1 φ X" and "w ∈ L2 X Y" and "w ∈ L3 X Y"
    unfolding L1_def L2_def L3_def by simp+

  then show "w ∈ ⋃ {L1 φ X ∩ L2 X Y ∩ L3 X Y | X Y. X ⊆ subformulasμ φ ∩ restricted_subformulas φ ∧ Y ⊆ subformulasν φ ∩ restricted_subformulas φ}"
    using 1 2 by blast
next
  fix w X Y
  assume "X ⊆ subformulasμ φ ∩ restricted_subformulas φ" and "Y ⊆ subformulasν φ ∩ restricted_subformulas φ"
    and "w ∈ L1 φ X" and "w ∈ L2 X Y" and "w ∈ L3 X Y"

  then show "w ∈ language_ltln φ"
    unfolding language_ltln_def L1_def L2_def L3_def
    using master_theorem_restricted by blast
qed


subsection ‹Definitions with Lists for Code Export›

definition restricted_advice_sets :: "'a ltln ⇒ ('a ltln list × 'a ltln list) list"
where
  "restricted_advice_sets φ = List.product (subseqs (List.filter (λx. x ∈ restricted_subformulas φ) (subformulasμ_list φ))) (subseqs (List.filter (λx. x ∈ restricted_subformulas φ) (subformulasν_list φ)))"

lemma subseqs_subformulasμ_restricted_list:
  "X ⊆ subformulasμ φ ∩ restricted_subformulas φ ⟷ (∃xs. X = set xs ∧ xs ∈ set (subseqs (List.filter (λx. x ∈ restricted_subformulas φ) (subformulasμ_list φ))))"
  by (metis in_set_subseqs inf_commute inter_set_filter subformulasμ_list_set subset_subseq)

lemma subseqs_subformulasν_restricted_list:
  "Y ⊆ subformulasν φ ∩ restricted_subformulas φ ⟷ (∃ys. Y = set ys ∧ ys ∈ set (subseqs (List.filter (λx. x ∈ restricted_subformulas φ) (subformulasν_list φ))))"
  by (metis in_set_subseqs inf_commute inter_set_filter subformulasν_list_set subset_subseq)

lemma restricted_advice_sets_subformulas:
  "X ⊆ subformulasμ φ ∩ restricted_subformulas φ ∧ Y ⊆ subformulasν φ ∩ restricted_subformulas φ ⟷ (∃xs ys. X = set xs ∧ Y = set ys ∧ (xs, ys) ∈ set (restricted_advice_sets φ))"
  unfolding restricted_advice_sets_def set_product subseqs_subformulasμ_restricted_list subseqs_subformulasν_restricted_list by blast

lemma restricted_advice_sets_not_empty:
  "restricted_advice_sets φ ≠ []"
  unfolding restricted_advice_sets_def using subseqs_not_empty product_not_empty by blast

end