Theory Syntactic_Fragments_and_Stability

(*
    Author:   Benedikt Seidl
    License:  BSD
*)

section ‹Syntactic Fragments and Stability›

theory Syntactic_Fragments_and_Stability
imports
  LTL.LTL "HOL-Library.Sublist"
begin

― ‹We use prefix and suffix on infinite words.›
hide_const Sublist.prefix Sublist.suffix

subsection ‹The fragments @{term μLTL} and @{term νLTL}›

fun is_μLTL :: "'a ltln ⇒ bool"
where
  "is_μLTL truen = True"
| "is_μLTL falsen = True"
| "is_μLTL propn(_) = True"
| "is_μLTL npropn(_) = True"
| "is_μLTL (φ andn ψ) = (is_μLTL φ ∧ is_μLTL ψ)"
| "is_μLTL (φ orn ψ) = (is_μLTL φ ∧ is_μLTL ψ)"
| "is_μLTL (Xn φ) = is_μLTL φ"
| "is_μLTL (φ Un ψ) = (is_μLTL φ ∧ is_μLTL ψ)"
| "is_μLTL (φ Mn ψ) = (is_μLTL φ ∧ is_μLTL ψ)"
| "is_μLTL _ = False"

fun is_νLTL :: "'a ltln ⇒ bool"
where
  "is_νLTL truen = True"
| "is_νLTL falsen = True"
| "is_νLTL propn(_) = True"
| "is_νLTL npropn(_) = True"
| "is_νLTL (φ andn ψ) = (is_νLTL φ ∧ is_νLTL ψ)"
| "is_νLTL (φ orn ψ) = (is_νLTL φ ∧ is_νLTL ψ)"
| "is_νLTL (Xn φ) = is_νLTL φ"
| "is_νLTL (φ Wn ψ) = (is_νLTL φ ∧ is_νLTL ψ)"
| "is_νLTL (φ Rn ψ) = (is_νLTL φ ∧ is_νLTL ψ)"
| "is_νLTL _ = False"

definition μLTL :: "'a ltln set" where
  "μLTL = {φ. is_μLTL φ}"

definition νLTL :: "'a ltln set" where
  "νLTL = {φ. is_νLTL φ}"

lemma μLTL_simp[simp]:
  "φ ∈ μLTL ⟷ is_μLTL φ"
  unfolding μLTL_def by simp

lemma νLTL_simp[simp]:
  "φ ∈ νLTL ⟷ is_νLTL φ"
  unfolding νLTL_def by simp



subsubsection ‹Subformulas in @{term μLTL} and @{term νLTL}›

fun subformulasμ :: "'a ltln ⇒ 'a ltln set"
where
  "subformulasμ (φ andn ψ) = subformulasμ φ ∪ subformulasμ ψ"
| "subformulasμ (φ orn ψ) = subformulasμ φ ∪ subformulasμ ψ"
| "subformulasμ (Xn φ) = subformulasμ φ"
| "subformulasμ (φ Un ψ) = {φ Un ψ} ∪ subformulasμ φ ∪ subformulasμ ψ"
| "subformulasμ (φ Rn ψ) = subformulasμ φ ∪ subformulasμ ψ"
| "subformulasμ (φ Wn ψ) = subformulasμ φ ∪ subformulasμ ψ"
| "subformulasμ (φ Mn ψ) = {φ Mn ψ} ∪ subformulasμ φ ∪ subformulasμ ψ"
| "subformulasμ _ = {}"

fun subformulasν :: "'a ltln ⇒ 'a ltln set"
where
  "subformulasν (φ andn ψ) = subformulasν φ ∪ subformulasν ψ"
| "subformulasν (φ orn ψ) = subformulasν φ ∪ subformulasν ψ"
| "subformulasν (Xn φ) = subformulasν φ"
| "subformulasν (φ Un ψ) = subformulasν φ ∪ subformulasν ψ"
| "subformulasν (φ Rn ψ) = {φ Rn ψ} ∪ subformulasν φ ∪ subformulasν ψ"
| "subformulasν (φ Wn ψ) = {φ Wn ψ} ∪ subformulasν φ ∪ subformulasν ψ"
| "subformulasν (φ Mn ψ) = subformulasν φ ∪ subformulasν ψ"
| "subformulasν _ = {}"

lemma subformulasμ_semantics:
  "subformulasμ φ = {ψ ∈ subfrmlsn φ. ∃ψ1 ψ2. ψ = ψ1 Un ψ2 ∨ ψ = ψ1 Mn ψ2}"
  by (induction φ) auto

lemma subformulasν_semantics:
  "subformulasν φ = {ψ ∈ subfrmlsn φ. ∃ψ1 ψ2. ψ = ψ1 Rn ψ2 ∨ ψ = ψ1 Wn ψ2}"
  by (induction φ) auto

lemma subformulasμ_subfrmlsn:
  "subformulasμ φ ⊆ subfrmlsn φ"
  by (induction φ) auto

lemma subformulasν_subfrmlsn:
  "subformulasν φ ⊆ subfrmlsn φ"
  by (induction φ) auto

lemma subformulasμ_finite:
  "finite (subformulasμ φ)"
  by (induction φ) auto

lemma subformulasν_finite:
  "finite (subformulasν φ)"
  by (induction φ) auto

lemma subformulasμ_subset:
  "ψ ∈ subfrmlsn φ ⟹ subformulasμ ψ ⊆ subformulasμ φ"
  by (induction φ) auto

lemma subformulasν_subset:
  "ψ ∈ subfrmlsn φ ⟹ subformulasν ψ ⊆ subformulasν φ"
  by (induction φ) auto

lemma subfrmlsn_μLTL:
  "φ ∈ μLTL ⟹ subfrmlsn φ ⊆ μLTL"
  by (induction φ) auto

lemma subfrmlsn_νLTL:
  "φ ∈ νLTL ⟹ subfrmlsn φ ⊆ νLTL"
  by (induction φ) auto

lemma subformulasμν_disjoint:
  "subformulasμ φ ∩ subformulasν φ = {}"
  unfolding subformulasμ_semantics subformulasν_semantics
  by fastforce

lemma subformulasμν_subfrmlsn:
  "subformulasμ φ ∪ subformulasν φ ⊆ subfrmlsn φ"
  using subformulasμ_subfrmlsn subformulasν_subfrmlsn by blast

lemma subformulasμν_card:
  "card (subformulasμ φ ∪ subformulasν φ) = card (subformulasμ φ) + card (subformulasν φ)"
  by (simp add: subformulasμν_disjoint subformulasμ_finite subformulasν_finite card_Un_disjoint)


subsection ‹Stability›

definition "GF_singleton w φ ≡ if w ⊨n Gn (Fn φ) then {φ} else {}"
definition "F_singleton w φ ≡ if w ⊨n Fn φ then {φ} else {}"

declare GF_singleton_def [simp] F_singleton_def [simp]

fun 𝒢ℱ :: "'a ltln ⇒ 'a set word ⇒ 'a ltln set"
where
  "𝒢ℱ (φ andn ψ) w = 𝒢ℱ φ w ∪ 𝒢ℱ ψ w"
| "𝒢ℱ (φ orn ψ) w = 𝒢ℱ φ w ∪ 𝒢ℱ ψ w"
| "𝒢ℱ (Xn φ) w = 𝒢ℱ φ w"
| "𝒢ℱ (φ Un ψ) w = GF_singleton w (φ Un ψ) ∪ 𝒢ℱ φ w ∪ 𝒢ℱ ψ w"
| "𝒢ℱ (φ Rn ψ) w = 𝒢ℱ φ w ∪ 𝒢ℱ ψ w"
| "𝒢ℱ (φ Wn ψ) w = 𝒢ℱ φ w ∪ 𝒢ℱ ψ w"
| "𝒢ℱ (φ Mn ψ) w = GF_singleton w (φ Mn ψ) ∪ 𝒢ℱ φ w ∪ 𝒢ℱ ψ w"
| "𝒢ℱ _ _ = {}"

fun ℱ :: "'a ltln ⇒ 'a set word ⇒ 'a ltln set"
where
  "ℱ (φ andn ψ) w = ℱ φ w ∪ ℱ ψ w"
| "ℱ (φ orn ψ) w = ℱ φ w ∪ ℱ ψ w"
| "ℱ (Xn φ) w = ℱ φ w"
| "ℱ (φ Un ψ) w = F_singleton w (φ Un ψ) ∪ ℱ φ w ∪ ℱ ψ w"
| "ℱ (φ Rn ψ) w = ℱ φ w ∪ ℱ ψ w"
| "ℱ (φ Wn ψ) w = ℱ φ w ∪ ℱ ψ w"
| "ℱ (φ Mn ψ) w = F_singleton w (φ Mn ψ) ∪ ℱ φ w ∪ ℱ ψ w"
| "ℱ _ _ = {}"


lemma 𝒢ℱ_semantics:
  "𝒢ℱ φ w = {ψ. ψ ∈ subformulasμ φ ∧ w ⊨n Gn (Fn ψ)}"
  by (induction φ) force+

lemma ℱ_semantics:
  "ℱ φ w = {ψ. ψ ∈ subformulasμ φ ∧ w ⊨n Fn ψ}"
  by (induction φ) force+

lemma 𝒢ℱ_semantics':
  "𝒢ℱ φ w = subformulasμ φ ∩ {ψ. w ⊨n Gn (Fn ψ)}"
  unfolding 𝒢ℱ_semantics by auto

lemma ℱ_semantics':
  "ℱ φ w = subformulasμ φ ∩ {ψ. w ⊨n Fn ψ}"
  unfolding ℱ_semantics by auto

lemma 𝒢ℱ_ℱ_subset:
  "𝒢ℱ φ w ⊆ ℱ φ w"
  unfolding 𝒢ℱ_semantics ℱ_semantics by force


lemma 𝒢ℱ_finite:
  "finite (𝒢ℱ φ w)"
  by (induction φ) auto

lemma 𝒢ℱ_subformulasμ:
  "𝒢ℱ φ w ⊆ subformulasμ φ"
  unfolding 𝒢ℱ_semantics by force

lemma 𝒢ℱ_subfrmlsn:
  "𝒢ℱ φ w ⊆ subfrmlsn φ"
  using 𝒢ℱ_subformulasμ subformulasμ_subfrmlsn by blast

lemma 𝒢ℱ_elim:
  "ψ ∈ 𝒢ℱ φ w ⟹ w ⊨n Gn (Fn ψ)"
  unfolding 𝒢ℱ_semantics by simp

lemma 𝒢ℱ_suffix(* [simp] *):
  "𝒢ℱ φ (suffix i w) = 𝒢ℱ φ w"
proof
  show "𝒢ℱ φ w ⊆ 𝒢ℱ φ (suffix i w)"
    unfolding 𝒢ℱ_semantics by auto
next
  show "𝒢ℱ φ (suffix i w) ⊆ 𝒢ℱ φ w"
    unfolding 𝒢ℱ_semantics GF_Inf_many
  proof auto
    fix ψ
    assume "∃∞j. suffix (i + j) w ⊨n ψ"
    then have "∃∞j. suffix (j + i) w ⊨n ψ"
      by (simp add: algebra_simps)
    then show "∃∞j. suffix j w ⊨n ψ"
      using INFM_nat_add by blast
  qed
qed

lemma 𝒢ℱ_subset:
  "ψ ∈ subfrmlsn φ ⟹ 𝒢ℱ ψ w ⊆ 𝒢ℱ φ w"
  unfolding 𝒢ℱ_semantics using subformulasμ_subset by blast


lemma ℱ_finite:
  "finite (ℱ φ w)"
  by (induction φ) auto

lemma ℱ_subformulasμ:
  "ℱ φ w ⊆ subformulasμ φ"
  unfolding ℱ_semantics by force

lemma ℱ_subfrmlsn:
  "ℱ φ w ⊆ subfrmlsn φ"
  using ℱ_subformulasμ subformulasμ_subfrmlsn by blast

lemma ℱ_elim:
  "ψ ∈ ℱ φ w ⟹ w ⊨n Fn ψ"
  unfolding ℱ_semantics by simp

lemma ℱ_suffix:
  "ℱ φ (suffix i w) ⊆ ℱ φ w"
  unfolding ℱ_semantics by auto

lemma ℱ_subset:
  "ψ ∈ subfrmlsn φ ⟹ ℱ ψ w ⊆ ℱ φ w"
  unfolding ℱ_semantics using subformulasμ_subset by blast


definition "μ_stable φ w ⟷ 𝒢ℱ φ w = ℱ φ w"

lemma suffix_μ_stable:
  "∀∞i. μ_stable φ (suffix i w)"
proof -
  have "∀ψ ∈ subformulasμ φ. ∀∞i. suffix i w ⊨n Gn (Fn ψ) ⟷ suffix i w ⊨n Fn ψ"
    using Alm_all_GF_F by blast

  then have "∀∞i. ∀ψ ∈ subformulasμ φ. suffix i w ⊨n Gn (Fn ψ) ⟷ suffix i w ⊨n Fn ψ"
    using subformulasμ_finite eventually_ball_finite by fast

  then have "∀∞i. {ψ ∈ subformulasμ φ. suffix i w ⊨n Gn (Fn ψ)} = {ψ ∈ subformulasμ φ. suffix i w ⊨n Fn ψ}"
    by (rule MOST_mono) (blast intro: Collect_cong)

  then show ?thesis
    unfolding μ_stable_def 𝒢ℱ_semantics ℱ_semantics
    by (rule MOST_mono) simp
qed

lemma μ_stable_subfrmlsn:
  "μ_stable φ w ⟹ ψ ∈ subfrmlsn φ ⟹ μ_stable ψ w"
proof -
  assume a1: "ψ ∈ subfrmlsn φ" and a2: "μ_stable φ w"
  have "subformulasμ ψ ⊆ subformulasμ φ"
    using a1 by (simp add: subformulasμ_subset)
  moreover
  have "𝒢ℱ φ w = ℱ φ w"
    using a2 by (meson μ_stable_def)
  ultimately show ?thesis
    by (metis (no_types) Un_commute ℱ_semantics' 𝒢ℱ_semantics' μ_stable_def inf_left_commute inf_sup_absorb sup.orderE)
qed

lemma μ_stable_suffix:
  "μ_stable φ w ⟹ μ_stable φ (suffix i w)"
  by (metis ℱ_suffix 𝒢ℱ_ℱ_subset 𝒢ℱ_suffix μ_stable_def subset_antisym)


definition "FG_singleton w φ ≡ if w ⊨n Fn (Gn φ) then {φ} else {}"
definition "G_singleton w φ ≡ if w ⊨n Gn φ then {φ} else {}"

declare FG_singleton_def [simp] G_singleton_def [simp]

fun ℱ𝒢 :: "'a ltln ⇒ 'a set word ⇒ 'a ltln set"
where
  "ℱ𝒢 (φ andn ψ) w = ℱ𝒢 φ w ∪ ℱ𝒢 ψ w"
| "ℱ𝒢 (φ orn ψ) w = ℱ𝒢 φ w ∪ ℱ𝒢 ψ w"
| "ℱ𝒢 (Xn φ) w = ℱ𝒢 φ w"
| "ℱ𝒢 (φ Un ψ) w = ℱ𝒢 φ w ∪ ℱ𝒢 ψ w"
| "ℱ𝒢 (φ Rn ψ) w = FG_singleton w (φ Rn ψ) ∪ ℱ𝒢 φ w ∪ ℱ𝒢 ψ w"
| "ℱ𝒢 (φ Wn ψ) w = FG_singleton w (φ Wn ψ) ∪ ℱ𝒢 φ w ∪ ℱ𝒢 ψ w"
| "ℱ𝒢 (φ Mn ψ) w = ℱ𝒢 φ w ∪ ℱ𝒢 ψ w"
| "ℱ𝒢 _ _ = {}"

fun 𝒢 :: "'a ltln ⇒ 'a set word ⇒ 'a ltln set"
where
  "𝒢 (φ andn ψ) w = 𝒢 φ w ∪ 𝒢 ψ w"
| "𝒢 (φ orn ψ) w = 𝒢 φ w ∪ 𝒢 ψ w"
| "𝒢 (Xn φ) w = 𝒢 φ w"
| "𝒢 (φ Un ψ) w = 𝒢 φ w ∪ 𝒢 ψ w"
| "𝒢 (φ Rn ψ) w = G_singleton w (φ Rn ψ) ∪ 𝒢 φ w ∪ 𝒢 ψ w"
| "𝒢 (φ Wn ψ) w = G_singleton w (φ Wn ψ) ∪ 𝒢 φ w ∪ 𝒢 ψ w"
| "𝒢 (φ Mn ψ) w = 𝒢 φ w ∪ 𝒢 ψ w"
| "𝒢 _ _ = {}"


lemma ℱ𝒢_semantics:
  "ℱ𝒢 φ w = {ψ ∈ subformulasν φ. w ⊨n Fn (Gn ψ)}"
  by (induction φ) force+

lemma 𝒢_semantics:
  "𝒢 φ w ≡ {ψ ∈ subformulasν φ. w ⊨n Gn ψ}"
  by (induction φ) force+

lemma ℱ𝒢_semantics':
  "ℱ𝒢 φ w = subformulasν φ ∩ {ψ. w ⊨n Fn (Gn ψ)}"
  unfolding ℱ𝒢_semantics by auto

lemma 𝒢_semantics':
  "𝒢 φ w = subformulasν φ ∩ {ψ. w ⊨n Gn ψ}"
  unfolding 𝒢_semantics by auto

lemma 𝒢_ℱ𝒢_subset:
  "𝒢 φ w ⊆ ℱ𝒢 φ w"
  unfolding 𝒢_semantics ℱ𝒢_semantics by force

lemma ℱ𝒢_finite:
  "finite (ℱ𝒢 φ w)"
  by (induction φ) auto

lemma ℱ𝒢_subformulasν:
  "ℱ𝒢 φ w ⊆ subformulasν φ"
  unfolding ℱ𝒢_semantics by force

lemma ℱ𝒢_subfrmlsn:
  "ℱ𝒢 φ w ⊆ subfrmlsn φ"
  using ℱ𝒢_subformulasν subformulasν_subfrmlsn by blast

lemma ℱ𝒢_elim:
  "ψ ∈ ℱ𝒢 φ w ⟹ w ⊨n Fn (Gn ψ)"
  unfolding ℱ𝒢_semantics by simp

lemma ℱ𝒢_suffix:
  "ℱ𝒢 φ (suffix i w) = ℱ𝒢 φ w"
proof
  show "ℱ𝒢 φ (suffix i w) ⊆ ℱ𝒢 φ w"
    unfolding ℱ𝒢_semantics by auto
next
  show "ℱ𝒢 φ w ⊆ ℱ𝒢 φ (suffix i w)"
    unfolding ℱ𝒢_semantics FG_Alm_all
  proof auto
    fix ψ
    assume "∀∞j. suffix j w ⊨n ψ"
    then have "∀∞j. suffix (j + i) w ⊨n ψ"
      using MOST_nat_add by meson
    then show "∀∞j. suffix (i + j) w ⊨n ψ"
      by (simp add: algebra_simps)
  qed
qed

lemma ℱ𝒢_subset:
  "ψ ∈ subfrmlsn φ ⟹ ℱ𝒢 ψ w ⊆ ℱ𝒢 φ w"
  unfolding ℱ𝒢_semantics using subformulasν_subset by blast


lemma 𝒢_finite:
  "finite (𝒢 φ w)"
  by (induction φ) auto

lemma 𝒢_subformulasν:
  "𝒢 φ w ⊆ subformulasν φ"
  unfolding 𝒢_semantics by force

lemma 𝒢_subfrmlsn:
  "𝒢 φ w ⊆ subfrmlsn φ"
  using 𝒢_subformulasν subformulasν_subfrmlsn by blast

lemma 𝒢_elim:
  "ψ ∈ 𝒢 φ w ⟹ w ⊨n Gn ψ"
  unfolding 𝒢_semantics by simp

lemma 𝒢_suffix:
  "𝒢 φ w ⊆ 𝒢 φ (suffix i w)"
  unfolding 𝒢_semantics by auto

lemma 𝒢_subset:
  "ψ ∈ subfrmlsn φ ⟹ 𝒢 ψ w ⊆ 𝒢 φ w"
  unfolding 𝒢_semantics using subformulasν_subset by blast


definition "ν_stable φ w ⟷ ℱ𝒢 φ w = 𝒢 φ w"

lemma suffix_ν_stable:
  "∀∞j. ν_stable φ (suffix j w)"
proof -
  have "∀ψ ∈ subformulasν φ. ∀∞i. suffix i w ⊨n Fn (Gn ψ) ⟷ suffix i w ⊨n Gn ψ"
    using Alm_all_FG_G by blast

  then have "∀∞i. ∀ψ ∈ subformulasν φ. suffix i w ⊨n Fn (Gn ψ) ⟷ suffix i w ⊨n Gn ψ"
    using subformulasν_finite eventually_ball_finite by fast

  then have "∀∞i. {ψ ∈ subformulasν φ. suffix i w ⊨n Fn (Gn ψ)} = {ψ ∈ subformulasν φ. suffix i w ⊨n Gn ψ}"
    by (rule MOST_mono) (blast intro: Collect_cong)

  then show ?thesis
    unfolding ν_stable_def ℱ𝒢_semantics 𝒢_semantics
    by (rule MOST_mono) simp
qed

lemma ν_stable_subfrmlsn:
  "ν_stable φ w ⟹ ψ ∈ subfrmlsn φ ⟹ ν_stable ψ w"
proof -
  assume a1: "ψ ∈ subfrmlsn φ" and a2: "ν_stable φ w"
  have "subformulasν ψ ⊆ subformulasν φ"
    using a1 by (simp add: subformulasν_subset)
  moreover
  have "ℱ𝒢 φ w = 𝒢 φ w"
    using a2 by (meson ν_stable_def)
  ultimately show ?thesis
    by (metis (no_types) Un_commute 𝒢_semantics' ℱ𝒢_semantics' ν_stable_def inf_left_commute inf_sup_absorb sup.orderE)
qed

lemma ν_stable_suffix:
  "ν_stable φ w ⟹ ν_stable φ (suffix i w)"
  by (metis ℱ𝒢_suffix 𝒢_ℱ𝒢_subset 𝒢_suffix ν_stable_def antisym_conv)


subsection ‹Definitions with Lists for Code Export›

text ‹The ‹μ›- and ‹ν›-subformulas as lists:›

fun subformulasμ_list :: "'a ltln ⇒ 'a ltln list"
where
  "subformulasμ_list (φ andn ψ) = List.union (subformulasμ_list φ) (subformulasμ_list ψ)"
| "subformulasμ_list (φ orn ψ) = List.union (subformulasμ_list φ) (subformulasμ_list ψ)"
| "subformulasμ_list (Xn φ) = subformulasμ_list φ"
| "subformulasμ_list (φ Un ψ) = List.insert (φ Un ψ) (List.union (subformulasμ_list φ) (subformulasμ_list ψ))"
| "subformulasμ_list (φ Rn ψ) = List.union (subformulasμ_list φ) (subformulasμ_list ψ)"
| "subformulasμ_list (φ Wn ψ) = List.union (subformulasμ_list φ) (subformulasμ_list ψ)"
| "subformulasμ_list (φ Mn ψ) = List.insert (φ Mn ψ) (List.union (subformulasμ_list φ) (subformulasμ_list ψ))"
| "subformulasμ_list _ = []"

fun subformulasν_list :: "'a ltln ⇒ 'a ltln list"
where
  "subformulasν_list (φ andn ψ) = List.union (subformulasν_list φ) (subformulasν_list ψ)"
| "subformulasν_list (φ orn ψ) = List.union (subformulasν_list φ) (subformulasν_list ψ)"
| "subformulasν_list (Xn φ) = subformulasν_list φ"
| "subformulasν_list (φ Un ψ) = List.union (subformulasν_list φ) (subformulasν_list ψ)"
| "subformulasν_list (φ Rn ψ) = List.insert (φ Rn ψ) (List.union (subformulasν_list φ) (subformulasν_list ψ))"
| "subformulasν_list (φ Wn ψ) = List.insert (φ Wn ψ) (List.union (subformulasν_list φ) (subformulasν_list ψ))"
| "subformulasν_list (φ Mn ψ) = List.union (subformulasν_list φ) (subformulasν_list ψ)"
| "subformulasν_list _ = []"

lemma subformulasμ_list_set:
  "set (subformulasμ_list φ) = subformulasμ φ"
  by (induction φ) auto

lemma subformulasν_list_set:
  "set (subformulasν_list φ) = subformulasν φ"
  by (induction φ) auto

lemma subformulasμ_list_distinct:
  "distinct (subformulasμ_list φ)"
  by (induction φ) auto

lemma subformulasν_list_distinct:
  "distinct (subformulasν_list φ)"
  by (induction φ) auto

lemma subformulasμ_list_length:
  "length (subformulasμ_list φ) = card (subformulasμ φ)"
  by (metis subformulasμ_list_set subformulasμ_list_distinct distinct_card)

lemma subformulasν_list_length:
  "length (subformulasν_list φ) = card (subformulasν φ)"
  by (metis subformulasν_list_set subformulasν_list_distinct distinct_card)


text ‹
  We define the list of advice sets as the product of all subsequences
  of the ‹μ›- and ‹ν›-subformulas of a formula.
›

definition advice_sets :: "'a ltln ⇒ ('a ltln list × 'a ltln list) list"
where
  "advice_sets φ = List.product (subseqs (subformulasμ_list φ)) (subseqs (subformulasν_list φ))"

lemma subset_subseq:
  "X ⊆ set ys ⟷ (∃xs. X = set xs ∧ subseq xs ys)"
  by (metis (no_types, lifting) Pow_iff image_iff in_set_subseqs subseqs_powset)

lemma subseqs_subformulasμ_list:
  "X ⊆ subformulasμ φ ⟷ (∃xs. X = set xs ∧ xs ∈ set (subseqs (subformulasμ_list φ)))"
  by (metis subset_subseq subformulasμ_list_set in_set_subseqs)

lemma subseqs_subformulasν_list:
  "Y ⊆ subformulasν φ ⟷ (∃ys. Y = set ys ∧ ys ∈ set (subseqs (subformulasν_list φ)))"
  by (metis subset_subseq subformulasν_list_set in_set_subseqs)

lemma advice_sets_subformulas:
  "X ⊆ subformulasμ φ ∧ Y ⊆ subformulasν φ ⟷ (∃xs ys. X = set xs ∧ Y = set ys ∧ (xs, ys) ∈ set (advice_sets φ))"
  unfolding advice_sets_def set_product subseqs_subformulasμ_list subseqs_subformulasν_list by blast

(* TODO add to HOL/List.thy *)
lemma subseqs_not_empty:
  "subseqs xs ≠ []"
  by (metis empty_iff list.set(1) subseqs_refl)

(* TODO add to HOL/List.thy *)
lemma product_not_empty:
  "xs ≠ [] ⟹ ys ≠ [] ⟹ List.product xs ys ≠ []"
  by (induction xs) simp_all

lemma advice_sets_not_empty:
  "advice_sets φ ≠ []"
  unfolding advice_sets_def using subseqs_not_empty product_not_empty by blast

lemma advice_sets_length:
  "length (advice_sets φ) ≤ 2 ^ card (subfrmlsn φ)"
  unfolding advice_sets_def length_product length_subseqs subformulasμ_list_length subformulasν_list_length power_add[symmetric]
  by (metis Suc_1 card_mono lessI power_increasing_iff subformulasμν_card subformulasμν_subfrmlsn subfrmlsn_finite)

lemma advice_sets_element_length:
  "(xs, ys) ∈ set (advice_sets φ) ⟹ length xs ≤ card (subfrmlsn φ)"
  "(xs, ys) ∈ set (advice_sets φ) ⟹ length ys ≤ card (subfrmlsn φ)"
  unfolding advice_sets_def set_product
  by (metis SigmaD1 card_mono in_set_subseqs list_emb_length order_trans subformulasμ_list_length subformulasμ_subfrmlsn subfrmlsn_finite)
     (metis SigmaD2 card_mono in_set_subseqs list_emb_length order_trans subformulasν_list_length subformulasν_subfrmlsn subfrmlsn_finite)

lemma advice_sets_element_subfrmlsn:
  "(xs, ys) ∈ set (advice_sets φ) ⟹ set xs ⊆ subformulasμ φ"
  "(xs, ys) ∈ set (advice_sets φ) ⟹ set ys ⊆ subformulasν φ"
  unfolding advice_sets_def set_product
  by (meson SigmaD1 subseqs_subformulasμ_list)
     (meson SigmaD2 subseqs_subformulasν_list)

end