Theory Master_Theorem

(*
    Author:   Benedikt Seidl
    License:  BSD
*)

section ‹The Master Theorem›

theory Master_Theorem
imports
  Advice After
begin

subsection ‹Checking @{term "X ⊆ 𝒢ℱ φ w"} and @{term "Y ⊆ ℱ𝒢 φ w"}›

lemma X_𝒢ℱ_Y_ℱ𝒢:
  assumes
    X_μ: "X ⊆ subformulasμ φ"
  and
    Y_ν: "Y ⊆ subformulasν φ"
  and
    X_GF: "∀ψ ∈ X. w ⊨n Gn (Fn ψ[Y]μ)"
  and
    Y_FG: "∀ψ ∈ Y. w ⊨n Fn (Gn ψ[X]ν)"
  shows
    "X ⊆ 𝒢ℱ φ w ∧ Y ⊆ ℱ𝒢 φ w"
proof -
  ― ‹Custom induction rule with @{term size} as a partial order›
  note induct = finite_ranking_induct[where f = size]

  have "finite (X ∪ Y)"
    using subformulasμ_finite subformulasν_finite X_μ Y_ν finite_subset
    by blast+

  then show ?thesis
    using assms
  proof (induction "X ∪ Y" arbitrary: X Y φ rule: induct)
    case (insert ψ S)

    note IH = insert(3)
    note insert_S = ‹insert ψ S = X ∪ Y›
    note X_μ = ‹X ⊆ subformulasμ φ›
    note Y_ν = ‹Y ⊆ subformulasν φ›
    note X_GF = ‹∀ψ ∈ X. w ⊨n Gn (Fn ψ[Y]μ)›
    note Y_FG = ‹∀ψ ∈ Y. w ⊨n Fn (Gn ψ[X]ν)›

    from X_μ Y_ν have "X ∩ Y = {}"
      using subformulasμν_disjoint by fast

    from insert_S X_μ Y_ν have "ψ ∈ subfrmlsn φ"
      using subformulasμ_subfrmlsn subformulasν_subfrmlsn by blast

    show ?case
    proof (cases "ψ ∉ S", cases "ψ ∈ X")
      assume "ψ ∉ S" and "ψ ∈ X"

      {
        ― ‹Show @{term "X - {ψ} ⊆ 𝒢ℱ φ w"} and @{term "Y ⊆ ℱ𝒢 φ w"}›

        then have "ψ ∉ Y"
          using ‹X ∩ Y = {}› by auto
        then have "S = (X - {ψ}) ∪ Y"
          using insert_S ‹ψ ∉ S› by fast

        moreover

        have "∀ψ' ∈ Y. ψ'[X - {ψ}]ν = ψ'[X]ν"
          using GF_advice_minus_size insert(1,2,4) ‹ψ ∉ Y› by fast

        ultimately have "X - {ψ} ⊆ 𝒢ℱ φ w" and "Y ⊆ ℱ𝒢 φ w"
          using IH[of "X - {ψ}" Y φ] X_μ Y_ν X_GF Y_FG by auto
      }

      moreover

      {
        ― ‹Show @{term "ψ ∈ 𝒢ℱ φ w"}›

        have "w ⊨n Gn (Fn ψ[Y]μ)"
          using X_GF ‹ψ ∈ X› by simp
        then have "∃∞i. suffix i w ⊨n ψ[Y]μ"
          unfolding GF_Inf_many by simp

        moreover

        from Y_ν have "finite Y"
          using subformulasν_finite finite_subset by auto

        have "∀φ ∈ Y. w ⊨n Fn (Gn φ)"
          using ‹Y ⊆ ℱ𝒢 φ w› by (blast dest: ℱ𝒢_elim)
        then have "∀φ ∈ Y. ∀∞i. suffix i w ⊨n Gn φ"
          using FG_suffix_G by blast
        then have "∀∞i. ∀φ ∈ Y. suffix i w ⊨n Gn φ"
          using ‹finite Y› eventually_ball_finite by fast

        ultimately

        have "∃∞i. suffix i w ⊨n ψ[Y]μ ∧ (∀φ ∈ Y. suffix i w ⊨n Gn φ)"
          using INFM_conjI by auto
        then have "∃∞i. suffix i w ⊨n ψ"
          by (elim frequently_elim1) (metis FG_advice_b2_helper)
        then have "w ⊨n Gn (Fn ψ)"
          unfolding GF_Inf_many by simp
        then have "ψ ∈ 𝒢ℱ φ w"
          unfolding 𝒢ℱ_semantics using ‹ψ ∈ X› X_μ by auto
      }

      ultimately show ?thesis
        by auto
    next
      assume "ψ ∉ S" and "ψ ∉ X"
      then have "ψ ∈ Y"
        using insert by fast

      {
        ― ‹Show @{term "X ⊆ 𝒢ℱ φ w"} and @{term "Y - {ψ} ⊆ ℱ𝒢 φ w"}›

        then have "S ∩ X = X"
          using insert ‹ψ ∉ X› by fast
        then have "S = X ∪ (Y - {ψ})"
          using insert_S ‹ψ ∉ S› by fast

        moreover

        have "∀ψ' ∈ X. ψ'[Y - {ψ}]μ = ψ'[Y]μ"
          using FG_advice_minus_size insert(1,2,4) ‹ψ ∉ X› by fast

        ultimately have "X ⊆ 𝒢ℱ φ w" and "Y - {ψ} ⊆ ℱ𝒢 φ w"
          using IH[of X "Y - {ψ}" φ] X_μ Y_ν X_GF Y_FG by auto
      }

      moreover

      {
        ― ‹Show @{term "ψ ∈ ℱ𝒢 φ w"}›

        have "w ⊨n Fn (Gn ψ[X]ν)"
          using Y_FG ‹ψ ∈ Y› by simp
        then have "∀∞i. suffix i w ⊨n ψ[X]ν"
          unfolding FG_Alm_all by simp

        moreover

        have "∀φ ∈ X. w ⊨n Gn (Fn φ)"
          using ‹X ⊆ 𝒢ℱ φ w› by (blast dest: 𝒢ℱ_elim)
        then have "∀∞i. ∀φ ∈ X. suffix i w ⊨n Gn (Fn φ)"
          by simp

        ultimately

        have "∀∞i. suffix i w ⊨n ψ[X]ν ∧ (∀φ ∈ X. suffix i w ⊨n Gn (Fn φ))"
          using MOST_conjI by auto
        then have "∀∞i. suffix i w ⊨n ψ"
          by (elim MOST_mono) (metis GF_advice_a2_helper)
        then have "w ⊨n Fn (Gn ψ)"
          unfolding FG_Alm_all by simp
        then have "ψ ∈ ℱ𝒢 φ w"
          unfolding ℱ𝒢_semantics using ‹ψ ∈ Y› Y_ν by auto
      }

      ultimately show ?thesis
        by auto
    next
      assume "¬ ψ ∉ S"
      then have "S = X ∪ Y"
        using insert by fast
      then show ?thesis
        using insert by auto
    qed
  qed fast
qed


lemma 𝒢ℱ_implies_GF:
  "∀ψ ∈ 𝒢ℱ φ w. w ⊨n Gn (Fn ψ[ℱ𝒢 φ w]μ)"
proof safe
  fix ψ
  assume "ψ ∈ 𝒢ℱ φ w"

  then have "∃∞i. suffix i w ⊨n ψ"
    using 𝒢ℱ_elim GF_Inf_many by blast

  moreover

  have "ψ ∈ subfrmlsn φ"
    using ‹ψ ∈ 𝒢ℱ φ w› 𝒢ℱ_subfrmlsn by blast

  then have "⋀i w. ℱ𝒢 ψ (suffix i w) ⊆ ℱ𝒢 φ w"
    using ℱ𝒢_suffix ℱ𝒢_subset by blast

  ultimately have "∃∞i. suffix i w ⊨n ψ[ℱ𝒢 φ w]μ"
    by (elim frequently_elim1) (metis FG_advice_b1)

  then show "w ⊨n Gn (Fn ψ[ℱ𝒢 φ w]μ)"
    unfolding GF_Inf_many by simp
qed


lemma ℱ𝒢_implies_FG:
  "∀ψ ∈ ℱ𝒢 φ w. w ⊨n Fn (Gn ψ[𝒢ℱ φ w]ν)"
proof safe
  fix ψ
  assume "ψ ∈ ℱ𝒢 φ w"

  then have "∀∞i. suffix i w ⊨n ψ"
    using ℱ𝒢_elim FG_Alm_all by blast

  moreover

  {
    have "ψ ∈ subfrmlsn φ"
      using ‹ψ ∈ ℱ𝒢 φ w› ℱ𝒢_subfrmlsn by blast

    moreover have "∀∞i. 𝒢ℱ ψ (suffix i w) = ℱ ψ (suffix i w)"
      using suffix_μ_stable unfolding μ_stable_def by blast

    ultimately have "∀∞i. ℱ ψ (suffix i w) ⊆ 𝒢ℱ φ w"
      unfolding MOST_nat_le by (metis 𝒢ℱ_subset 𝒢ℱ_suffix)
  }

  ultimately have "∀∞i. ℱ ψ (suffix i w) ⊆ 𝒢ℱ φ w ∧ suffix i w ⊨n ψ"
    using eventually_conj by auto

  then have "∀∞i. suffix i w ⊨n ψ[𝒢ℱ φ w]ν"
    using GF_advice_a1 by (elim eventually_mono) auto

  then show "w ⊨n Fn (Gn ψ[𝒢ℱ φ w]ν)"
    unfolding FG_Alm_all by simp
qed


subsection ‹Putting the pieces together: The Master Theorem›

theorem master_theorem_ltr:
  assumes
    "w ⊨n φ"
  obtains X and Y where
    "X ⊆ subformulasμ φ"
  and
    "Y ⊆ 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]ν)"
proof
  show "𝒢ℱ φ w ⊆ subformulasμ φ"
    by (rule 𝒢ℱ_subformulasμ)
next
  show "ℱ𝒢 φ w ⊆ subformulasν φ"
    by (rule ℱ𝒢_subformulasν)
next
  obtain i where "𝒢ℱ φ (suffix i w) = ℱ φ (suffix i w)"
    using suffix_μ_stable unfolding MOST_nat μ_stable_def by fast
  then have "ℱ (af φ (prefix i w)) (suffix i w) ⊆ 𝒢ℱ φ w"
    using 𝒢ℱ_af ℱ_af 𝒢ℱ_suffix by fast

  moreover

  have "suffix i w ⊨n af φ (prefix i w)"
    using af_ltl_continuation ‹w ⊨n φ› by fastforce

  ultimately show "∃i. suffix i w ⊨n af φ (prefix i w)[𝒢ℱ φ w]ν"
    using GF_advice_a1 by blast
next
  show "∀ψ ∈ 𝒢ℱ φ w. w ⊨n Gn (Fn ψ[ℱ𝒢 φ w]μ)"
    by (rule 𝒢ℱ_implies_GF)
next
  show "∀ψ ∈ ℱ𝒢 φ w. w ⊨n Fn (Gn ψ[𝒢ℱ φ w]ν)"
    by (rule ℱ𝒢_implies_FG)
qed

theorem master_theorem_rtl:
  assumes
    "X ⊆ subformulasμ φ"
  and
    "Y ⊆ subformulasν φ"
  and
    1: "∃i. suffix i w ⊨n af φ (prefix i w)[X]ν"
  and
    2: "∀ψ ∈ X. w ⊨n Gn (Fn ψ[Y]μ)"
  and
    3: "∀ψ ∈ Y. w ⊨n Fn (Gn ψ[X]ν)"
  shows
    "w ⊨n φ"
proof -
  from 1 obtain i where "suffix i w ⊨n af φ (prefix i w)[X]ν"
    by blast

  moreover

  from assms have "X ⊆ 𝒢ℱ φ w"
    using X_𝒢ℱ_Y_ℱ𝒢 by blast
  then have "X ⊆ 𝒢ℱ φ (suffix i w)"
    using 𝒢ℱ_suffix by fast

  ultimately have "suffix i w ⊨n af φ (prefix i w)"
    using GF_advice_a2 𝒢ℱ_af by metis
  then show "w ⊨n φ"
    using af_ltl_continuation by force
qed

theorem master_theorem:
  "w ⊨n φ ⟷
    (∃X ⊆ subformulasμ φ.
      (∃Y ⊆ subformulasν φ.
        (∃i. suffix i w ⊨n af φ (prefix i w)[X]ν)
        ∧ (∀ψ ∈ X. w ⊨n Gn (Fn ψ[Y]μ))
        ∧ (∀ψ ∈ Y. w ⊨n Fn (Gn ψ[X]ν))))"
  by (metis master_theorem_ltr master_theorem_rtl)



subsection ‹The Master Theorem on Languages›

definition "L1 φ X = {w. ∃i. suffix i w ⊨n af φ (prefix i w)[X]ν}"

definition "L2 X Y = {w. ∀ψ ∈ X. w ⊨n Gn (Fn ψ[Y]μ)}"

definition "L3 X Y = {w. ∀ψ ∈ Y. w ⊨n Fn (Gn ψ[X]ν)}"

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

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

  then obtain X Y where "X ⊆ subformulasμ φ" and "Y ⊆ 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_ltr 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μ φ ∧ Y ⊆ subformulasν φ}"
    using ‹X ⊆ subformulasμ φ› ‹Y ⊆ subformulasν φ› by blast
next
  fix w X Y
  assume "X ⊆ subformulasμ φ" and "Y ⊆ 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_rtl by blast
qed

end