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