# Theory Asymmetric_Master_Theorem

```(*
Author:   Benedikt Seidl
*)

section ‹Asymmetric Variant of the Master Theorem›

theory Asymmetric_Master_Theorem
imports
begin

text ‹This variant of the Master Theorem fixes only a subset @{term Y}
of @{term νLTL} subformulas and all conditions depend on the
index @{term i}. While this does not lead to a simple DRA construction,
but can be used to build NBAs and LDBAs.›

"ψ ∈ subfrmlsn φ ⟹ suffix i w ⊨⇩n ψ ⟹ suffix i w ⊨⇩n ψ[ℱ𝒢 φ w]⇩μ"
proof -
assume "ψ ∈ subfrmlsn φ"

then have "ℱ𝒢 ψ (suffix i w) ⊆ ℱ𝒢 φ w"
using ℱ𝒢_suffix subformulas⇩ν_subset unfolding ℱ𝒢_semantics' by fast

moreover

assume "suffix i w ⊨⇩n ψ"

ultimately show "suffix i w ⊨⇩n ψ[ℱ𝒢 φ w]⇩μ"
qed

"S ⊆ 𝒢 φ (suffix i w) ⟹ i ≤ j ⟹ suffix j w ⊨⇩n ψ[S]⇩μ ⟹ suffix j w ⊨⇩n ψ"
proof -
fix i j
assume "S ⊆ 𝒢 φ (suffix i w)" and "i ≤ j" and "suffix j w ⊨⇩n ψ[S]⇩μ"

then have "suffix j w ⊨⇩n ψ[S ∩ subformulas⇩ν ψ]⇩μ"

moreover

have "S ∩ subformulas⇩ν ψ ⊆ 𝒢 ψ (suffix i w)"
using ‹S ⊆ 𝒢 φ (suffix i w)› unfolding 𝒢_semantics' by blast
then have "S ∩ subformulas⇩ν ψ ⊆ 𝒢 ψ (suffix j w)"
using 𝒢_suffix ‹i ≤ j› inf.absorb_iff2 le_Suc_ex by fastforce

ultimately show "suffix j w ⊨⇩n ψ"
qed

lemma Y_𝒢:
assumes
Y_ν: "Y ⊆ subformulas⇩ν φ"
and
Y_G_1: "∀ψ⇩1 ψ⇩2. ψ⇩1 R⇩n ψ⇩2 ∈ Y ⟶ suffix i w ⊨⇩n G⇩n (ψ⇩2[Y]⇩μ)"
and
Y_G_2: "∀ψ⇩1 ψ⇩2. ψ⇩1 W⇩n ψ⇩2 ∈ Y ⟶ suffix i w ⊨⇩n G⇩n (ψ⇩1[Y]⇩μ or⇩n ψ⇩2[Y]⇩μ)"
shows
"Y ⊆ 𝒢 φ (suffix i w)"
proof -
― ‹Custom induction rule with @{term size} as a partial order›
note induct = finite_ranking_induct[where f = size]

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

then show ?thesis
using assms
proof (induction Y rule: induct)
case (insert ψ S)

show ?case
proof (cases "ψ ∉ S")
assume "ψ ∉ S"

{
― ‹Show @{term "S ⊆ 𝒢 φ (suffix i w)"}›

{
fix ψ⇩1 ψ⇩2
assume "ψ⇩1 R⇩n ψ⇩2 ∈ S"

then have "suffix i w ⊨⇩n G⇩n ψ⇩2[insert ψ S]⇩μ"
using insert(5) by blast

then have "suffix i w ⊨⇩n G⇩n ψ⇩2[S]⇩μ"
using ‹ψ⇩1 R⇩n ψ⇩2 ∈ S› FG_advice_insert insert.hyps(2)
by fastforce
}

moreover

{
fix ψ⇩1 ψ⇩2
assume "ψ⇩1 W⇩n ψ⇩2 ∈ S"

then have "suffix i w ⊨⇩n G⇩n (ψ⇩1[insert ψ S]⇩μ or⇩n ψ⇩2[insert ψ S]⇩μ)"
using insert(6) by blast

then have "suffix i w ⊨⇩n G⇩n (ψ⇩1[S]⇩μ or⇩n ψ⇩2[S]⇩μ)"
using ‹ψ⇩1 W⇩n ψ⇩2 ∈ S› FG_advice_insert insert.hyps(2)
by fastforce
}

ultimately

have "S ⊆ 𝒢 φ (suffix i w)"
using insert.IH insert.prems(1) by blast
}

moreover

{
― ‹Show @{term "ψ ∈ 𝒢 φ (suffix i w)"}›

have "ψ ∈ subformulas⇩ν φ"
using insert.prems(1) by fast
then have "suffix i w ⊨⇩n G⇩n ψ"
using subformulas⇩ν_semantics
proof (cases ψ)
case (Release_ltln ψ⇩1 ψ⇩2)

then have "suffix i w ⊨⇩n G⇩n ψ⇩2[insert ψ S]⇩μ"
using insert.prems(2) by blast
then have "suffix i w ⊨⇩n G⇩n ψ⇩2[S]⇩μ"
then have "suffix i w ⊨⇩n G⇩n ψ⇩2"
using FG_advice_b2_helper[OF ‹S ⊆ 𝒢 φ (suffix i w)›] by auto
then show ?thesis
using Release_ltln globally_release
by blast
next
case (WeakUntil_ltln ψ⇩1 ψ⇩2)

then have "suffix i w ⊨⇩n G⇩n (ψ⇩1[insert ψ S]⇩μ or⇩n ψ⇩2[insert ψ S]⇩μ)"
using insert.prems(3) by blast
then have "suffix i w ⊨⇩n G⇩n (ψ⇩1 or⇩n ψ⇩2)[S]⇩μ"
then have "suffix i w ⊨⇩n G⇩n (ψ⇩1 or⇩n ψ⇩2)"
using FG_advice_b2_helper[OF ‹S ⊆ 𝒢 φ (suffix i w)›, of _ "ψ⇩1 or⇩n ψ⇩2"]
by force
then show ?thesis
unfolding WeakUntil_ltln semantics_ltln.simps
by (metis order_refl suffix_suffix)
qed fast+

then have "ψ ∈ 𝒢 φ (suffix i w)"
unfolding 𝒢_semantics using ‹ψ ∈ subformulas⇩ν φ›
by simp
}

ultimately show ?thesis
by blast
next
assume "¬ ψ ∉ S"
then have "insert ψ S = S"
by auto
then show ?thesis
using insert by simp
qed
qed simp
qed

theorem asymmetric_master_theorem_ltr:
assumes
"w ⊨⇩n φ"
obtains Y and i where
"Y ⊆ subformulas⇩ν φ"
and
"suffix i w ⊨⇩n af φ (prefix i w)[Y]⇩μ"
and
"∀ψ⇩1 ψ⇩2. ψ⇩1 R⇩n ψ⇩2 ∈ Y ⟶ suffix i w ⊨⇩n G⇩n (ψ⇩2[Y]⇩μ)"
and
"∀ψ⇩1 ψ⇩2. ψ⇩1 W⇩n ψ⇩2 ∈ Y ⟶ suffix i w ⊨⇩n G⇩n (ψ⇩1[Y]⇩μ or⇩n ψ⇩2[Y]⇩μ)"
proof
let ?Y = "ℱ𝒢 φ w"

show "?Y ⊆ subformulas⇩ν φ"
by (rule ℱ𝒢_subformulas⇩ν)
next
let ?Y = "ℱ𝒢 φ w"
let ?i = "SOME i. ?Y = 𝒢 φ (suffix i w)"

have "suffix ?i w ⊨⇩n af φ (prefix ?i w)"
using af_ltl_continuation ‹w ⊨⇩n φ› by fastforce
then show "suffix ?i w ⊨⇩n af φ (prefix ?i w)[?Y]⇩μ"
by (metis ℱ𝒢_suffix FG_advice_b1 ℱ𝒢_af order_refl)
next
let ?Y = "ℱ𝒢 φ w"
let ?i = "SOME i. ?Y = 𝒢 φ (suffix i w)"

have "∃i. ?Y = 𝒢 φ (suffix i w)"
using suffix_ν_stable ℱ𝒢_suffix unfolding ν_stable_def MOST_nat
by fast
then have Y_G: "?Y = 𝒢 φ (suffix ?i w)"
by (metis (mono_tags, lifting) someI_ex)

show "∀ψ⇩1 ψ⇩2. ψ⇩1 R⇩n ψ⇩2 ∈ ?Y ⟶ suffix ?i w ⊨⇩n G⇩n (ψ⇩2[?Y]⇩μ)"
proof safe
fix ψ⇩1 ψ⇩2
assume "ψ⇩1 R⇩n ψ⇩2 ∈ ?Y"

then have "suffix ?i w ⊨⇩n G⇩n (ψ⇩1 R⇩n ψ⇩2)"
using Y_G 𝒢_semantics' by blast
then have "suffix ?i w ⊨⇩n G⇩n ψ⇩2"
by force

moreover

have "ψ⇩2 ∈ subfrmlsn φ"
using ℱ𝒢_subfrmlsn ‹ψ⇩1 R⇩n ψ⇩2 ∈ ?Y› subfrmlsn_subset by force

ultimately show "suffix ?i w ⊨⇩n G⇩n (ψ⇩2 [?Y]⇩μ)"
qed
next
let ?Y = "ℱ𝒢 φ w"
let ?i = "SOME i. ?Y = 𝒢 φ (suffix i w)"

have "∃i. ?Y = 𝒢 φ (suffix i w)"
using suffix_ν_stable ℱ𝒢_suffix unfolding ν_stable_def MOST_nat
by fast
then have Y_G: "?Y = 𝒢 φ (suffix ?i w)"
by (rule someI_ex)

show "∀ψ⇩1 ψ⇩2. ψ⇩1 W⇩n ψ⇩2 ∈ ?Y ⟶ suffix ?i w ⊨⇩n G⇩n (ψ⇩1[?Y]⇩μ or⇩n ψ⇩2[?Y]⇩μ)"
proof safe
fix ψ⇩1 ψ⇩2
assume "ψ⇩1 W⇩n ψ⇩2 ∈ ?Y"

then have "suffix ?i w ⊨⇩n G⇩n (ψ⇩1 W⇩n ψ⇩2)"
using Y_G 𝒢_semantics' by blast
then have "suffix ?i w ⊨⇩n G⇩n (ψ⇩1 or⇩n ψ⇩2)"
by force

moreover

have "ψ⇩1 ∈ subfrmlsn φ" and "ψ⇩2 ∈ subfrmlsn φ"
using ℱ𝒢_subfrmlsn ‹ψ⇩1 W⇩n ψ⇩2 ∈ ?Y› subfrmlsn_subset by force+

ultimately show "suffix ?i w ⊨⇩n G⇩n (ψ⇩1[?Y]⇩μ or⇩n ψ⇩2[?Y]⇩μ)"
qed
qed

theorem asymmetric_master_theorem_rtl:
assumes
1: "Y ⊆ subformulas⇩ν φ"
and
2: "suffix i w ⊨⇩n af φ (prefix i w)[Y]⇩μ"
and
3: "∀ψ⇩1 ψ⇩2. ψ⇩1 R⇩n ψ⇩2 ∈ Y ⟶ suffix i w ⊨⇩n G⇩n (ψ⇩2[Y]⇩μ)"
and
4: "∀ψ⇩1 ψ⇩2. ψ⇩1 W⇩n ψ⇩2 ∈ Y ⟶ suffix i w ⊨⇩n G⇩n (ψ⇩1[Y]⇩μ or⇩n ψ⇩2[Y]⇩μ)"
shows
"w ⊨⇩n φ"
proof -
have "suffix i w ⊨⇩n af φ (prefix i w)"
by (metis assms Y_𝒢 FG_advice_b2 𝒢_af)

then show "w ⊨⇩n φ"
using af_ltl_continuation by force
qed

theorem asymmetric_master_theorem:
"w ⊨⇩n φ ⟷
(∃i. ∃Y ⊆ subformulas⇩ν φ.
suffix i w ⊨⇩n af φ (prefix i w)[Y]⇩μ
∧ (∀ψ⇩1 ψ⇩2. ψ⇩1 R⇩n ψ⇩2 ∈ Y ⟶ suffix i w ⊨⇩n G⇩n (ψ⇩2[Y]⇩μ))
∧ (∀ψ⇩1 ψ⇩2. ψ⇩1 W⇩n ψ⇩2 ∈ Y ⟶ suffix i w ⊨⇩n G⇩n (ψ⇩1[Y]⇩μ or⇩n ψ⇩2[Y]⇩μ)))"
by (metis asymmetric_master_theorem_ltr asymmetric_master_theorem_rtl)

end
```