Theory Asymmetric_Master_Theorem

(*
    Author:   Benedikt Seidl
    License:  BSD
*)

section ‹Asymmetric Variant of the Master Theorem›

theory Asymmetric_Master_Theorem
imports
  Advice After
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.›

lemma FG_advice_b1_helper:
  "ψ ∈ 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]μ"
    using FG_advice_b1 by blast
qed

lemma FG_advice_b2_helper:
  "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ν ψ]μ"
    using FG_advice_inter_subformulas by metis

  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 ψ"
    using FG_advice_b2 by blast
qed

lemma Y_𝒢:
  assumes
    Y_ν: "Y ⊆ subformulasν φ"
  and
    Y_G_1: "∀ψ1 ψ2. ψ1 Rn ψ2 ∈ Y ⟶ suffix i w ⊨n Gn (ψ2[Y]μ)"
  and
    Y_G_2: "∀ψ1 ψ2. ψ1 Wn ψ2 ∈ Y ⟶ suffix i w ⊨n Gn (ψ1[Y]μ orn ψ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"

      note FG_advice_insert = FG_advice_insert[OF ‹ψ ∉ S›]

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

        {
          fix ψ1 ψ2
          assume "ψ1 Rn ψ2 ∈ S"

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

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

        moreover

        {
          fix ψ1 ψ2
          assume "ψ1 Wn ψ2 ∈ S"

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

          then have "suffix i w ⊨n Gn (ψ1[S]μ orn ψ2[S]μ)"
            using ‹ψ1 Wn ψ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 Gn ψ"
          using subformulasν_semantics
        proof (cases ψ)
          case (Release_ltln ψ1 ψ2)

          then have "suffix i w ⊨n Gn ψ2[insert ψ S]μ"
            using insert.prems(2) by blast
          then have "suffix i w ⊨n Gn ψ2[S]μ"
            using Release_ltln FG_advice_insert by simp
          then have "suffix i w ⊨n Gn ψ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 Gn (ψ1[insert ψ S]μ orn ψ2[insert ψ S]μ)"
            using insert.prems(3) by blast
          then have "suffix i w ⊨n Gn (ψ1 orn ψ2)[S]μ"
            using WeakUntil_ltln FG_advice_insert by simp
          then have "suffix i w ⊨n Gn (ψ1 orn ψ2)"
            using FG_advice_b2_helper[OF ‹S ⊆ 𝒢 φ (suffix i w)›, of _ "ψ1 orn ψ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 Rn ψ2 ∈ Y ⟶ suffix i w ⊨n Gn (ψ2[Y]μ)"
  and
    "∀ψ1 ψ2. ψ1 Wn ψ2 ∈ Y ⟶ suffix i w ⊨n Gn (ψ1[Y]μ orn ψ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 Rn ψ2 ∈ ?Y ⟶ suffix ?i w ⊨n Gn (ψ2[?Y]μ)"
  proof safe
    fix ψ1 ψ2
    assume "ψ1 Rn ψ2 ∈ ?Y"

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

    moreover

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

    ultimately show "suffix ?i w ⊨n Gn (ψ2 [?Y]μ)"
      using FG_advice_b1_helper by fastforce
  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 Wn ψ2 ∈ ?Y ⟶ suffix ?i w ⊨n Gn (ψ1[?Y]μ orn ψ2[?Y]μ)"
  proof safe
    fix ψ1 ψ2
    assume "ψ1 Wn ψ2 ∈ ?Y"

    then have "suffix ?i w ⊨n Gn (ψ1 Wn ψ2)"
      using Y_G 𝒢_semantics' by blast
    then have "suffix ?i w ⊨n Gn (ψ1 orn ψ2)"
      by force

    moreover

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

    ultimately show "suffix ?i w ⊨n Gn (ψ1[?Y]μ orn ψ2[?Y]μ)"
      using FG_advice_b1_helper by fastforce
  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 Rn ψ2 ∈ Y ⟶ suffix i w ⊨n Gn (ψ2[Y]μ)"
  and
    4: "∀ψ1 ψ2. ψ1 Wn ψ2 ∈ Y ⟶ suffix i w ⊨n Gn (ψ1[Y]μ orn ψ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 Rn ψ2 ∈ Y ⟶ suffix i w ⊨n Gn (ψ2[Y]μ))
      ∧ (∀ψ1 ψ2. ψ1 Wn ψ2 ∈ Y ⟶ suffix i w ⊨n Gn (ψ1[Y]μ orn ψ2[Y]μ)))"
  by (metis asymmetric_master_theorem_ltr asymmetric_master_theorem_rtl)

end