(* 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}G⇩_{n}(F⇩_{n}ψ[Y]⇩_{μ})" and Y_FG: "∀ψ ∈ Y. w ⊨⇩_{n}F⇩_{n}(G⇩_{n}ψ[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}G⇩_{n}(F⇩_{n}ψ[Y]⇩_{μ})› note Y_FG = ‹∀ψ ∈ Y. w ⊨⇩_{n}F⇩_{n}(G⇩_{n}ψ[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}G⇩_{n}(F⇩_{n}ψ[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}F⇩_{n}(G⇩_{n}φ)" using ‹Y ⊆ ℱ𝒢 φ w› by (blast dest: ℱ𝒢_elim) then have "∀φ ∈ Y. ∀⇩_{∞}i. suffix i w ⊨⇩_{n}G⇩_{n}φ" using FG_suffix_G by blast then have "∀⇩_{∞}i. ∀φ ∈ Y. suffix i w ⊨⇩_{n}G⇩_{n}φ" using ‹finite Y› eventually_ball_finite by fast ultimately have "∃⇩_{∞}i. suffix i w ⊨⇩_{n}ψ[Y]⇩_{μ}∧ (∀φ ∈ Y. suffix i w ⊨⇩_{n}G⇩_{n}φ)" 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}G⇩_{n}(F⇩_{n}ψ)" 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}F⇩_{n}(G⇩_{n}ψ[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}G⇩_{n}(F⇩_{n}φ)" using ‹X ⊆ 𝒢ℱ φ w› by (blast dest: 𝒢ℱ_elim) then have "∀⇩_{∞}i. ∀φ ∈ X. suffix i w ⊨⇩_{n}G⇩_{n}(F⇩_{n}φ)" by simp ultimately have "∀⇩_{∞}i. suffix i w ⊨⇩_{n}ψ[X]⇩_{ν}∧ (∀φ ∈ X. suffix i w ⊨⇩_{n}G⇩_{n}(F⇩_{n}φ))" 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}F⇩_{n}(G⇩_{n}ψ)" 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}G⇩_{n}(F⇩_{n}ψ[ℱ𝒢 φ 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}G⇩_{n}(F⇩_{n}ψ[ℱ𝒢 φ w]⇩_{μ})" unfolding GF_Inf_many by simp qed lemma ℱ𝒢_implies_FG: "∀ψ ∈ ℱ𝒢 φ w. w ⊨⇩_{n}F⇩_{n}(G⇩_{n}ψ[𝒢ℱ φ 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}F⇩_{n}(G⇩_{n}ψ[𝒢ℱ φ 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}G⇩_{n}(F⇩_{n}ψ[Y]⇩_{μ})" and "∀ψ ∈ Y. w ⊨⇩_{n}F⇩_{n}(G⇩_{n}ψ[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}G⇩_{n}(F⇩_{n}ψ[ℱ𝒢 φ w]⇩_{μ})" by (rule 𝒢ℱ_implies_GF) next show "∀ψ ∈ ℱ𝒢 φ w. w ⊨⇩_{n}F⇩_{n}(G⇩_{n}ψ[𝒢ℱ φ 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}G⇩_{n}(F⇩_{n}ψ[Y]⇩_{μ})" and 3: "∀ψ ∈ Y. w ⊨⇩_{n}F⇩_{n}(G⇩_{n}ψ[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}G⇩_{n}(F⇩_{n}ψ[Y]⇩_{μ})) ∧ (∀ψ ∈ Y. w ⊨⇩_{n}F⇩_{n}(G⇩_{n}ψ[X]⇩_{ν}))))" by (metis master_theorem_ltr master_theorem_rtl) subsection ‹The Master Theorem on Languages› definition "L⇩_{1}φ X = {w. ∃i. suffix i w ⊨⇩_{n}af φ (prefix i w)[X]⇩_{ν}}" definition "L⇩_{2}X Y = {w. ∀ψ ∈ X. w ⊨⇩_{n}G⇩_{n}(F⇩_{n}ψ[Y]⇩_{μ})}" definition "L⇩_{3}X Y = {w. ∀ψ ∈ Y. w ⊨⇩_{n}F⇩_{n}(G⇩_{n}ψ[X]⇩_{ν})}" corollary master_theorem_language: "language_ltln φ = ⋃ {L⇩_{1}φ X ∩ L⇩_{2}X Y ∩ L⇩_{3}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}G⇩_{n}(F⇩_{n}ψ[Y]⇩_{μ})" and "∀ψ ∈ Y. w ⊨⇩_{n}F⇩_{n}(G⇩_{n}ψ[X]⇩_{ν})" using master_theorem_ltr by metis then have "w ∈ L⇩_{1}φ X" and "w ∈ L⇩_{2}X Y" and "w ∈ L⇩_{3}X Y" unfolding L⇩_{1}_def L⇩_{2}_def L⇩_{3}_def by simp+ then show "w ∈ ⋃ {L⇩_{1}φ X ∩ L⇩_{2}X Y ∩ L⇩_{3}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 ∈ L⇩_{1}φ X" and "w ∈ L⇩_{2}X Y" and "w ∈ L⇩_{3}X Y" then show "w ∈ language_ltln φ" unfolding language_ltln_def L⇩_{1}_def L⇩_{2}_def L⇩_{3}_def using master_theorem_rtl by blast qed end