Theory Syntactic_Fragments_and_Stability

```(*
Author:   Benedikt Seidl
*)

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 true⇩n = True"
| "is_μLTL false⇩n = True"
| "is_μLTL prop⇩n(_) = True"
| "is_μLTL nprop⇩n(_) = True"
| "is_μLTL (φ and⇩n ψ) = (is_μLTL φ ∧ is_μLTL ψ)"
| "is_μLTL (φ or⇩n ψ) = (is_μLTL φ ∧ is_μLTL ψ)"
| "is_μLTL (X⇩n φ) = is_μLTL φ"
| "is_μLTL (φ U⇩n ψ) = (is_μLTL φ ∧ is_μLTL ψ)"
| "is_μLTL (φ M⇩n ψ) = (is_μLTL φ ∧ is_μLTL ψ)"
| "is_μLTL _ = False"

fun is_νLTL :: "'a ltln ⇒ bool"
where
"is_νLTL true⇩n = True"
| "is_νLTL false⇩n = True"
| "is_νLTL prop⇩n(_) = True"
| "is_νLTL nprop⇩n(_) = True"
| "is_νLTL (φ and⇩n ψ) = (is_νLTL φ ∧ is_νLTL ψ)"
| "is_νLTL (φ or⇩n ψ) = (is_νLTL φ ∧ is_νLTL ψ)"
| "is_νLTL (X⇩n φ) = is_νLTL φ"
| "is_νLTL (φ W⇩n ψ) = (is_νLTL φ ∧ is_νLTL ψ)"
| "is_νLTL (φ R⇩n ψ) = (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⇩μ (φ and⇩n ψ) = subformulas⇩μ φ ∪ subformulas⇩μ ψ"
| "subformulas⇩μ (φ or⇩n ψ) = subformulas⇩μ φ ∪ subformulas⇩μ ψ"
| "subformulas⇩μ (X⇩n φ) = subformulas⇩μ φ"
| "subformulas⇩μ (φ U⇩n ψ) = {φ U⇩n ψ} ∪ subformulas⇩μ φ ∪ subformulas⇩μ ψ"
| "subformulas⇩μ (φ R⇩n ψ) = subformulas⇩μ φ ∪ subformulas⇩μ ψ"
| "subformulas⇩μ (φ W⇩n ψ) = subformulas⇩μ φ ∪ subformulas⇩μ ψ"
| "subformulas⇩μ (φ M⇩n ψ) = {φ M⇩n ψ} ∪ subformulas⇩μ φ ∪ subformulas⇩μ ψ"
| "subformulas⇩μ _ = {}"

fun subformulas⇩ν :: "'a ltln ⇒ 'a ltln set"
where
"subformulas⇩ν (φ and⇩n ψ) = subformulas⇩ν φ ∪ subformulas⇩ν ψ"
| "subformulas⇩ν (φ or⇩n ψ) = subformulas⇩ν φ ∪ subformulas⇩ν ψ"
| "subformulas⇩ν (X⇩n φ) = subformulas⇩ν φ"
| "subformulas⇩ν (φ U⇩n ψ) = subformulas⇩ν φ ∪ subformulas⇩ν ψ"
| "subformulas⇩ν (φ R⇩n ψ) = {φ R⇩n ψ} ∪ subformulas⇩ν φ ∪ subformulas⇩ν ψ"
| "subformulas⇩ν (φ W⇩n ψ) = {φ W⇩n ψ} ∪ subformulas⇩ν φ ∪ subformulas⇩ν ψ"
| "subformulas⇩ν (φ M⇩n ψ) = subformulas⇩ν φ ∪ subformulas⇩ν ψ"
| "subformulas⇩ν _ = {}"

lemma subformulas⇩μ_semantics:
"subformulas⇩μ φ = {ψ ∈ subfrmlsn φ. ∃ψ⇩1 ψ⇩2. ψ = ψ⇩1 U⇩n ψ⇩2 ∨ ψ = ψ⇩1 M⇩n ψ⇩2}"
by (induction φ) auto

lemma subformulas⇩ν_semantics:
"subformulas⇩ν φ = {ψ ∈ subfrmlsn φ. ∃ψ⇩1 ψ⇩2. ψ = ψ⇩1 R⇩n ψ⇩2 ∨ ψ = ψ⇩1 W⇩n ψ⇩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 G⇩n (F⇩n φ) then {φ} else {}"
definition "F_singleton w φ ≡ if w ⊨⇩n F⇩n φ then {φ} else {}"

declare GF_singleton_def [simp] F_singleton_def [simp]

fun 𝒢ℱ :: "'a ltln ⇒ 'a set word ⇒ 'a ltln set"
where
"𝒢ℱ (φ and⇩n ψ) w = 𝒢ℱ φ w ∪ 𝒢ℱ ψ w"
| "𝒢ℱ (φ or⇩n ψ) w = 𝒢ℱ φ w ∪ 𝒢ℱ ψ w"
| "𝒢ℱ (X⇩n φ) w = 𝒢ℱ φ w"
| "𝒢ℱ (φ U⇩n ψ) w = GF_singleton w (φ U⇩n ψ) ∪ 𝒢ℱ φ w ∪ 𝒢ℱ ψ w"
| "𝒢ℱ (φ R⇩n ψ) w = 𝒢ℱ φ w ∪ 𝒢ℱ ψ w"
| "𝒢ℱ (φ W⇩n ψ) w = 𝒢ℱ φ w ∪ 𝒢ℱ ψ w"
| "𝒢ℱ (φ M⇩n ψ) w = GF_singleton w (φ M⇩n ψ) ∪ 𝒢ℱ φ w ∪ 𝒢ℱ ψ w"
| "𝒢ℱ _ _ = {}"

fun ℱ :: "'a ltln ⇒ 'a set word ⇒ 'a ltln set"
where
"ℱ (φ and⇩n ψ) w = ℱ φ w ∪ ℱ ψ w"
| "ℱ (φ or⇩n ψ) w = ℱ φ w ∪ ℱ ψ w"
| "ℱ (X⇩n φ) w = ℱ φ w"
| "ℱ (φ U⇩n ψ) w = F_singleton w (φ U⇩n ψ) ∪ ℱ φ w ∪ ℱ ψ w"
| "ℱ (φ R⇩n ψ) w = ℱ φ w ∪ ℱ ψ w"
| "ℱ (φ W⇩n ψ) w = ℱ φ w ∪ ℱ ψ w"
| "ℱ (φ M⇩n ψ) w = F_singleton w (φ M⇩n ψ) ∪ ℱ φ w ∪ ℱ ψ w"
| "ℱ _ _ = {}"

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

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

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

lemma ℱ_semantics':
"ℱ φ w = subformulas⇩μ φ ∩ {ψ. w ⊨⇩n F⇩n ψ}"
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 G⇩n (F⇩n ψ)"
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 F⇩n ψ"
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 G⇩n (F⇩n ψ) ⟷ suffix i w ⊨⇩n F⇩n ψ"
using Alm_all_GF_F by blast

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

then have "∀⇩∞i. {ψ ∈ subformulas⇩μ φ. suffix i w ⊨⇩n G⇩n (F⇩n ψ)} = {ψ ∈ subformulas⇩μ φ. suffix i w ⊨⇩n F⇩n ψ}"
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 F⇩n (G⇩n φ) then {φ} else {}"
definition "G_singleton w φ ≡ if w ⊨⇩n G⇩n φ then {φ} else {}"

declare FG_singleton_def [simp] G_singleton_def [simp]

fun ℱ𝒢 :: "'a ltln ⇒ 'a set word ⇒ 'a ltln set"
where
"ℱ𝒢 (φ and⇩n ψ) w = ℱ𝒢 φ w ∪ ℱ𝒢 ψ w"
| "ℱ𝒢 (φ or⇩n ψ) w = ℱ𝒢 φ w ∪ ℱ𝒢 ψ w"
| "ℱ𝒢 (X⇩n φ) w = ℱ𝒢 φ w"
| "ℱ𝒢 (φ U⇩n ψ) w = ℱ𝒢 φ w ∪ ℱ𝒢 ψ w"
| "ℱ𝒢 (φ R⇩n ψ) w = FG_singleton w (φ R⇩n ψ) ∪ ℱ𝒢 φ w ∪ ℱ𝒢 ψ w"
| "ℱ𝒢 (φ W⇩n ψ) w = FG_singleton w (φ W⇩n ψ) ∪ ℱ𝒢 φ w ∪ ℱ𝒢 ψ w"
| "ℱ𝒢 (φ M⇩n ψ) w = ℱ𝒢 φ w ∪ ℱ𝒢 ψ w"
| "ℱ𝒢 _ _ = {}"

fun 𝒢 :: "'a ltln ⇒ 'a set word ⇒ 'a ltln set"
where
"𝒢 (φ and⇩n ψ) w = 𝒢 φ w ∪ 𝒢 ψ w"
| "𝒢 (φ or⇩n ψ) w = 𝒢 φ w ∪ 𝒢 ψ w"
| "𝒢 (X⇩n φ) w = 𝒢 φ w"
| "𝒢 (φ U⇩n ψ) w = 𝒢 φ w ∪ 𝒢 ψ w"
| "𝒢 (φ R⇩n ψ) w = G_singleton w (φ R⇩n ψ) ∪ 𝒢 φ w ∪ 𝒢 ψ w"
| "𝒢 (φ W⇩n ψ) w = G_singleton w (φ W⇩n ψ) ∪ 𝒢 φ w ∪ 𝒢 ψ w"
| "𝒢 (φ M⇩n ψ) w = 𝒢 φ w ∪ 𝒢 ψ w"
| "𝒢 _ _ = {}"

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

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

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

lemma 𝒢_semantics':
"𝒢 φ w = subformulas⇩ν φ ∩ {ψ. w ⊨⇩n G⇩n ψ}"
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 F⇩n (G⇩n ψ)"
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 G⇩n ψ"
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 F⇩n (G⇩n ψ) ⟷ suffix i w ⊨⇩n G⇩n ψ"
using Alm_all_FG_G by blast

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

then have "∀⇩∞i. {ψ ∈ subformulas⇩ν φ. suffix i w ⊨⇩n F⇩n (G⇩n ψ)} = {ψ ∈ subformulas⇩ν φ. suffix i w ⊨⇩n G⇩n ψ}"
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 (φ and⇩n ψ) = List.union (subformulas⇩μ_list φ) (subformulas⇩μ_list ψ)"
| "subformulas⇩μ_list (φ or⇩n ψ) = List.union (subformulas⇩μ_list φ) (subformulas⇩μ_list ψ)"
| "subformulas⇩μ_list (X⇩n φ) = subformulas⇩μ_list φ"
| "subformulas⇩μ_list (φ U⇩n ψ) = List.insert (φ U⇩n ψ) (List.union (subformulas⇩μ_list φ) (subformulas⇩μ_list ψ))"
| "subformulas⇩μ_list (φ R⇩n ψ) = List.union (subformulas⇩μ_list φ) (subformulas⇩μ_list ψ)"
| "subformulas⇩μ_list (φ W⇩n ψ) = List.union (subformulas⇩μ_list φ) (subformulas⇩μ_list ψ)"
| "subformulas⇩μ_list (φ M⇩n ψ) = List.insert (φ M⇩n ψ) (List.union (subformulas⇩μ_list φ) (subformulas⇩μ_list ψ))"
| "subformulas⇩μ_list _ = []"

fun subformulas⇩ν_list :: "'a ltln ⇒ 'a ltln list"
where
"subformulas⇩ν_list (φ and⇩n ψ) = List.union (subformulas⇩ν_list φ) (subformulas⇩ν_list ψ)"
| "subformulas⇩ν_list (φ or⇩n ψ) = List.union (subformulas⇩ν_list φ) (subformulas⇩ν_list ψ)"
| "subformulas⇩ν_list (X⇩n φ) = subformulas⇩ν_list φ"
| "subformulas⇩ν_list (φ U⇩n ψ) = List.union (subformulas⇩ν_list φ) (subformulas⇩ν_list ψ)"
| "subformulas⇩ν_list (φ R⇩n ψ) = List.insert (φ R⇩n ψ) (List.union (subformulas⇩ν_list φ) (subformulas⇩ν_list ψ))"
| "subformulas⇩ν_list (φ W⇩n ψ) = List.insert (φ W⇩n ψ) (List.union (subformulas⇩ν_list φ) (subformulas⇩ν_list ψ))"
| "subformulas⇩ν_list (φ M⇩n ψ) = 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)

"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

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

"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)

"(xs, ys) ∈ set (advice_sets φ) ⟹ length xs ≤ card (subfrmlsn φ)"
"(xs, ys) ∈ set (advice_sets φ) ⟹ length ys ≤ card (subfrmlsn φ)"